1(* ========================================================================= *) 2(* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6(* ========================================================================= *) 7(* A type of problems. *) 8(* ========================================================================= *) 9 10type problem = 11 {name : string, 12 comments : string list, 13 goal : Formula.quotation}; 14 15(* ========================================================================= *) 16(* Helper functions. *) 17(* ========================================================================= *) 18 19local 20 fun mkCollection collection = "Collection: " ^ collection; 21 22 fun mkProblem collection description (problem : problem) : problem = 23 let 24 val {name,comments,goal} = problem 25 val comments = if List.null comments then [] else "" :: comments 26 val comments = "Description: " ^ description :: comments 27 val comments = mkCollection collection :: comments 28 in 29 {name = name, comments = comments, goal = goal} 30 end; 31in 32 fun isCollection collection {name = _, comments, goal = _} = 33 Useful.mem (mkCollection collection) comments; 34 35 fun mkProblems collection description problems = 36 List.map (mkProblem collection description) problems; 37end; 38 39(* ========================================================================= *) 40(* The collection of problems. *) 41(* ========================================================================= *) 42 43val problems : problem list = 44 45(* ========================================================================= *) 46(* Problems without equality. *) 47(* ========================================================================= *) 48 49mkProblems "nonequality" "Problems without equality from various sources" [ 50 51(* ------------------------------------------------------------------------- *) 52(* Trivia (some of which demonstrate ex-bugs in provers). *) 53(* ------------------------------------------------------------------------- *) 54 55{name = "TRUE", 56 comments = [], 57 goal = ` 58T`}, 59 60{name = "SIMPLE", 61 comments = [], 62 goal = ` 63!x y. ?z. p x \/ p y ==> p z`}, 64 65{name = "CYCLIC", 66 comments = [], 67 goal = ` 68(!x. p (g (c x))) ==> ?z. p (g z)`}, 69 70{name = "MICHAEL_NORRISH_BUG", 71 comments = [], 72 goal = ` 73(!x. ?y. f y x x) ==> ?z. f z 0 0`}, 74 75{name = "RELATION_COMPOSITION", 76 comments = [], 77 goal = ` 78(!x. ?y. p x y) /\ (!x. ?y. q x y) /\ 79(!x y z. p x y /\ q y z ==> r x z) ==> !x. ?y. r x y`}, 80 81{name = "TOBIAS_NIPKOW", 82 comments = [], 83 goal = ` 84(!x y. p x y ==> f x = f y) /\ (!x. f (g x) = f x) /\ p (g a) (g b) ==> 85f a = f b`}, 86 87{name = "SLEDGEHAMMER", 88 comments = ["From Tobias Nipkow: A ==> A takes 1 minute in sledgehammer."], 89 goal = ` 90(!x y z t. 91 x @ y = z @ t <=> 92 ?u. x = z @ u /\ u @ y = t \/ x @ u = z /\ y = u @ t) ==> 93!x y z t. 94 x @ y = z @ t <=> ?u. x = z @ u /\ u @ y = t \/ x @ u = z /\ y = u @ t`}, 95 96{name = "SPLITTING_UNSOUNDNESS", 97 comments = ["A trivial example to illustrate a bug spotted by", 98 "Geoff Sutcliffe in Dec 2008."], 99 goal = ` 100(!x. p x /\ q x ==> F) ==> !x. p x ==> !x. q x ==> F`}, 101 102(* ------------------------------------------------------------------------- *) 103(* Propositional Logic. *) 104(* ------------------------------------------------------------------------- *) 105 106{name = "PROP_1", 107 comments = [], 108 goal = ` 109p ==> q <=> ~q ==> ~p`}, 110 111{name = "PROP_2", 112 comments = [], 113 goal = ` 114~~p <=> p`}, 115 116{name = "PROP_3", 117 comments = [], 118 goal = ` 119~(p ==> q) ==> q ==> p`}, 120 121{name = "PROP_4", 122 comments = [], 123 goal = ` 124~p ==> q <=> ~q ==> p`}, 125 126{name = "PROP_5", 127 comments = [], 128 goal = ` 129(p \/ q ==> p \/ r) ==> p \/ (q ==> r)`}, 130 131{name = "PROP_6", 132 comments = [], 133 goal = ` 134p \/ ~p`}, 135 136{name = "PROP_7", 137 comments = [], 138 goal = ` 139p \/ ~~~p`}, 140 141{name = "PROP_8", 142 comments = [], 143 goal = ` 144((p ==> q) ==> p) ==> p`}, 145 146{name = "PROP_9", 147 comments = [], 148 goal = ` 149(p \/ q) /\ (~p \/ q) /\ (p \/ ~q) ==> ~(~q \/ ~q)`}, 150 151{name = "PROP_10", 152 comments = [], 153 goal = ` 154(q ==> r) /\ (r ==> p /\ q) /\ (p ==> q /\ r) ==> (p <=> q)`}, 155 156{name = "PROP_11", 157 comments = [], 158 goal = ` 159p <=> p`}, 160 161{name = "PROP_12", 162 comments = [], 163 goal = ` 164((p <=> q) <=> r) <=> p <=> q <=> r`}, 165 166{name = "PROP_13", 167 comments = [], 168 goal = ` 169p \/ q /\ r <=> (p \/ q) /\ (p \/ r)`}, 170 171{name = "PROP_14", 172 comments = [], 173 goal = ` 174(p <=> q) <=> (q \/ ~p) /\ (~q \/ p)`}, 175 176{name = "PROP_15", 177 comments = [], 178 goal = ` 179p ==> q <=> ~p \/ q`}, 180 181{name = "PROP_16", 182 comments = [], 183 goal = ` 184(p ==> q) \/ (q ==> p)`}, 185 186{name = "PROP_17", 187 comments = [], 188 goal = ` 189p /\ (q ==> r) ==> s <=> (~p \/ q \/ s) /\ (~p \/ ~r \/ s)`}, 190 191{name = "MATHS4_EXAMPLE", 192 comments = [], 193 goal = ` 194(a \/ ~k ==> g) /\ (g ==> q) /\ ~q ==> k`}, 195 196{name = "LOGICPROOF_1996", 197 comments = [], 198 goal = ` 199(p ==> r) /\ (~p ==> ~q) /\ (p \/ q) ==> p /\ r`}, 200 201{name = "XOR_ASSOC", 202 comments = [], 203 goal = ` 204~(~(p <=> q) <=> r) <=> ~(p <=> ~(q <=> r))`}, 205 206{name = "ALL_3_CLAUSES", 207 comments = [], 208 goal = ` 209(p \/ q \/ r) /\ (p \/ q \/ ~r) /\ (p \/ ~q \/ r) /\ (p \/ ~q \/ ~r) /\ 210(~p \/ q \/ r) /\ (~p \/ q \/ ~r) /\ (~p \/ ~q \/ r) /\ 211(~p \/ ~q \/ ~r) ==> F`}, 212 213{name = "CLAUSE_SIMP", 214 comments = [], 215 goal = ` 216(lit ==> clause) ==> (lit \/ clause <=> clause)`}, 217 218{name = "SPLIT_NOT_IFF", 219 comments = ["A way to split a goal that looks like ~(p <=> q)"], 220 goal = ` 221~(p <=> q) <=> (p ==> ~q) /\ (q ==> ~p)`}, 222 223(* ------------------------------------------------------------------------- *) 224(* Monadic Predicate Logic. *) 225(* ------------------------------------------------------------------------- *) 226 227{name = "P18", 228 comments = ["The drinker's principle."], 229 goal = ` 230?very_popular_guy. !whole_pub. drinks very_popular_guy ==> drinks whole_pub`}, 231 232{name = "P19", 233 comments = [], 234 goal = ` 235?x. !y z. (p y ==> q z) ==> p x ==> q x`}, 236 237{name = "P20", 238 comments = [], 239 goal = ` 240(!x y. ?z. !w. p x /\ q y ==> r z /\ u w) /\ (!x y. p x /\ q y) ==> ?z. r z`}, 241 242{name = "P21", 243 comments = [], 244 goal = ` 245(?x. p ==> q x) /\ (?x. q x ==> p) ==> ?x. p <=> q x`}, 246 247{name = "P22", 248 comments = [], 249 goal = ` 250(!x. p <=> q x) ==> (p <=> !x. q x)`}, 251 252{name = "P23", 253 comments = [], 254 goal = ` 255(!x. p \/ q x) <=> p \/ !x. q x`}, 256 257{name = "P24", 258 comments = [], 259 goal = ` 260~(?x. u x /\ q x) /\ (!x. p x ==> q x \/ r x) /\ ~(?x. p x ==> ?x. q x) /\ 261(!x. q x /\ r x ==> u x) ==> ?x. p x /\ r x`}, 262 263{name = "P25", 264 comments = [], 265 goal = ` 266(?x. p x) /\ (!x. u x ==> ~g x /\ r x) /\ (!x. p x ==> g x /\ u x) /\ 267((!x. p x ==> q x) \/ ?x. q x /\ p x) ==> ?x. q x /\ p x`}, 268 269{name = "P26", 270 comments = [], 271 goal = ` 272((?x. p x) <=> ?x. q x) /\ (!x y. p x /\ q y ==> (r x <=> u y)) ==> 273((!x. p x ==> r x) <=> !x. q x ==> u x)`}, 274 275{name = "P27", 276 comments = [], 277 goal = ` 278(?x. p x /\ ~q x) /\ (!x. p x ==> r x) /\ (!x. u x /\ s x ==> p x) /\ 279(?x. r x /\ ~q x) ==> (!x. u x ==> ~r x) ==> !x. u x ==> ~s x`}, 280 281{name = "P28", 282 comments = [], 283 goal = ` 284(!x. p x ==> !x. q x) /\ ((!x. q x \/ r x) ==> ?x. q x /\ r x) /\ 285((?x. r x) ==> !x. l x ==> m x) ==> !x. p x /\ l x ==> m x`}, 286 287{name = "P29", 288 comments = [], 289 goal = ` 290(?x. p x) /\ (?x. g x) ==> 291((!x. p x ==> h x) /\ (!x. g x ==> j x) <=> 292 !x y. p x /\ g y ==> h x /\ j y)`}, 293 294{name = "P30", 295 comments = [], 296 goal = ` 297(!x. p x \/ g x ==> ~h x) /\ (!x. (g x ==> ~u x) ==> p x /\ h x) ==> 298!x. u x`}, 299 300{name = "P31", 301 comments = [], 302 goal = ` 303~(?x. p x /\ (g x \/ h x)) /\ (?x. q x /\ p x) /\ (!x. ~h x ==> j x) ==> 304?x. q x /\ j x`}, 305 306{name = "P32", 307 comments = [], 308 goal = ` 309(!x. p x /\ (g x \/ h x) ==> q x) /\ (!x. q x /\ h x ==> j x) /\ 310(!x. r x ==> h x) ==> !x. p x /\ r x ==> j x`}, 311 312{name = "P33", 313 comments = [], 314 goal = ` 315(!x. p a /\ (p x ==> p b) ==> p c) <=> 316(!x. p a ==> p x \/ p c) /\ (p a ==> p b ==> p c)`}, 317 318{name = "P34", 319 comments = 320["This gives rise to 5184 clauses when naively converted to CNF!"], 321 goal = ` 322((?x. !y. p x <=> p y) <=> (?x. q x) <=> !y. q y) <=> 323(?x. !y. q x <=> q y) <=> (?x. p x) <=> !y. p y`}, 324 325{name = "P35", 326 comments = [], 327 goal = ` 328?x y. p x y ==> !x y. p x y`}, 329 330(* ------------------------------------------------------------------------- *) 331(* Predicate logic without functions. *) 332(* ------------------------------------------------------------------------- *) 333 334{name = "P36", 335 comments = [], 336 goal = ` 337(!x. ?y. p x y) /\ (!x. ?y. g x y) /\ 338(!x y. p x y \/ g x y ==> !z. p y z \/ g y z ==> h x z) ==> !x. ?y. h x y`}, 339 340{name = "P37", 341 comments = [], 342 goal = ` 343(!z. ?w. !x. ?y. (p x z ==> p y w) /\ p y z /\ (p y w ==> ?v. q v w)) /\ 344(!x z. ~p x z ==> ?y. q y z) /\ ((?x y. q x y) ==> !x. r x x) ==> 345!x. ?y. r x y`}, 346 347{name = "P38", 348 comments = [], 349 goal = ` 350(!x. p a /\ (p x ==> ?y. p y /\ r x y) ==> ?z w. p z /\ r x w /\ r w z) <=> 351!x. 352 (~p a \/ p x \/ ?z w. p z /\ r x w /\ r w z) /\ 353 (~p a \/ ~(?y. p y /\ r x y) \/ ?z w. p z /\ r x w /\ r w z)`}, 354 355{name = "P39", 356 comments = [], 357 goal = ` 358~?x. !y. p y x <=> ~p y y`}, 359 360{name = "P40", 361 comments = [], 362 goal = ` 363(?y. !x. p x y <=> p x x) ==> ~!x. ?y. !z. p z y <=> ~p z x`}, 364 365{name = "P41", 366 comments = [], 367 goal = ` 368(!z. ?y. !x. p x y <=> p x z /\ ~p x x) ==> ~?z. !x. p x z`}, 369 370{name = "P42", 371 comments = [], 372 goal = ` 373~?y. !x. p x y <=> ~?z. p x z /\ p z x`}, 374 375{name = "P43", 376 comments = [], 377 goal = ` 378(!x y. q x y <=> !z. p z x <=> p z y) ==> !x y. q x y <=> q y x`}, 379 380{name = "P44", 381 comments = [], 382 goal = ` 383(!x. p x ==> (?y. g y /\ h x y) /\ ?y. g y /\ ~h x y) /\ 384(?x. j x /\ !y. g y ==> h x y) ==> ?x. j x /\ ~p x`}, 385 386{name = "P45", 387 comments = [], 388 goal = ` 389(!x. p x /\ (!y. g y /\ h x y ==> j x y) ==> !y. g y /\ h x y ==> r y) /\ 390~(?y. l y /\ r y) /\ 391(?x. p x /\ (!y. h x y ==> l y) /\ !y. g y /\ h x y ==> j x y) ==> 392?x. p x /\ ~?y. g y /\ h x y`}, 393 394{name = "P46", 395 comments = [], 396 goal = ` 397(!x. p x /\ (!y. p y /\ h y x ==> g y) ==> g x) /\ 398((?x. p x /\ ~g x) ==> ?x. p x /\ ~g x /\ !y. p y /\ ~g y ==> j x y) /\ 399(!x y. p x /\ p y /\ h x y ==> ~j y x) ==> !x. p x ==> g x`}, 400 401{name = "P50", 402 comments = [], 403 goal = ` 404(!x. f0 a x \/ !y. f0 x y) ==> ?x. !y. f0 x y`}, 405 406{name = "LOGICPROOF_L10", 407 comments = [], 408 goal = ` 409!x. ?y. ~(P y x <=> ~P y y)`}, 410 411{name = "BARBER", 412 comments = ["One resolution of the barber paradox"], 413 goal = ` 414(!x. man x ==> (shaves barber x <=> ~shaves x x)) ==> ~man barber`}, 415 416(* ------------------------------------------------------------------------- *) 417(* Full predicate logic. *) 418(* ------------------------------------------------------------------------- *) 419 420{name = "LOGICPROOF_1999", 421 comments = ["A non-theorem."], 422 goal = ` 423(?x. p x /\ q x) ==> ?x. p (f x x) \/ !y. q y`}, 424 425{name = "P55", 426 comments = ["Example from Manthey and Bry, CADE-9. [JRH]"], 427 goal = ` 428lives agatha /\ lives butler /\ lives charles /\ 429(killed agatha agatha \/ killed butler agatha \/ killed charles agatha) /\ 430(!x y. killed x y ==> hates x y /\ ~richer x y) /\ 431(!x. hates agatha x ==> ~hates charles x) /\ 432(hates agatha agatha /\ hates agatha charles) /\ 433(!x. lives x /\ ~richer x agatha ==> hates butler x) /\ 434(!x. hates agatha x ==> hates butler x) /\ 435(!x. ~hates x agatha \/ ~hates x butler \/ ~hates x charles) ==> 436killed agatha agatha /\ ~killed butler agatha /\ ~killed charles agatha`}, 437 438{name = "P57", 439 comments = [], 440 goal = ` 441p (f a b) (f b c) /\ p (f b c) (f a c) /\ 442(!x y z. p x y /\ p y z ==> p x z) ==> p (f a b) (f a c)`}, 443 444{name = "P58", 445 comments = ["See info-hol 1498 [JRH]"], 446 goal = ` 447!x. ?v w. !y z. p x /\ q y ==> (p v \/ r w) /\ (r z ==> q v)`}, 448 449{name = "P59", 450 comments = [], 451 goal = ` 452(!x. p x <=> ~p (f x)) ==> ?x. p x /\ ~p (f x)`}, 453 454{name = "P60", 455 comments = [], 456 goal = ` 457!x. p x (f x) <=> ?y. (!z. p z y ==> p z (f x)) /\ p x y`}, 458 459(* ------------------------------------------------------------------------- *) 460(* From Gilmore's classic paper. *) 461(* ------------------------------------------------------------------------- *) 462 463{name = "GILMORE_1", 464 comments = 465["Amazingly, this still seems non-trivial... in HOL [MESON_TAC] it", 466 "works at depth 45! [JRH]", 467 "Confirmed (depth=45, inferences=263702, time=148s), though if", 468 "lemmaizing is used then a lemma is discovered at depth 29 that allows", 469 "a much quicker proof (depth=30, inferences=10039, time=5.5s)."], 470 goal = ` 471?x. !y z. 472 (f y ==> g y <=> f x) /\ (f y ==> h y <=> g x) /\ 473 ((f y ==> g y) ==> h y <=> h x) ==> f z /\ g z /\ h z`}, 474 475{name = "GILMORE_2", 476 comments = 477["This is not valid, according to Gilmore. [JRH]", 478 "Confirmed: ordered resolution quickly saturates."], 479 goal = ` 480?x y. !z. 481 (f x z <=> f z y) /\ (f z y <=> f z z) /\ (f x y <=> f y x) ==> 482 (f x y <=> f x z)`}, 483 484{name = "GILMORE_3", 485 comments = [], 486 goal = ` 487?x. !y z. 488 ((f y z ==> g y ==> h x) ==> f x x) /\ ((f z x ==> g x) ==> h z) /\ 489 f x y ==> f z z`}, 490 491{name = "GILMORE_4", 492 comments = [], 493 goal = ` 494?x y. !z. (f x y ==> f y z /\ f z z) /\ (f x y /\ g x y ==> g x z /\ g z z)`}, 495 496{name = "GILMORE_5", 497 comments = [], 498 goal = ` 499(!x. ?y. f x y \/ f y x) /\ (!x y. f y x ==> f y y) ==> ?z. f z z`}, 500 501{name = "GILMORE_6", 502 comments = [], 503 goal = ` 504!x. ?y. 505 (?w. !v. f w x ==> g v w /\ g w x) ==> 506 (?w. !v. f w y ==> g v w /\ g w y) \/ 507 !z v. ?w. g v z \/ h w y z ==> g z w`}, 508 509{name = "GILMORE_7", 510 comments = [], 511 goal = ` 512(!x. k x ==> ?y. l y /\ (f x y ==> g x y)) /\ 513(?z. k z /\ !w. l w ==> f z w) ==> ?v w. k v /\ l w /\ g v w`}, 514 515{name = "GILMORE_8", 516 comments = [], 517 goal = ` 518?x. !y z. 519 ((f y z ==> g y ==> !w. ?v. h w v x) ==> f x x) /\ 520 ((f z x ==> g x) ==> !w. ?v. h w v z) /\ f x y ==> f z z`}, 521 522{name = "GILMORE_9", 523 comments = 524["Model elimination (in HOL):", 525 "- With lemmaizing: (depth=18, inferences=15632, time=21s)", 526 "- Without: gave up waiting after (depth=25, inferences=2125072, ...)"], 527 goal = ` 528!x. ?y. !z. 529 ((!w. ?v. f y w v /\ g y w /\ ~h y x) ==> 530 (!w. ?v. f x w v /\ g z u /\ ~h x z) ==> 531 !w. ?v. f x w v /\ g y w /\ ~h x y) /\ 532 ((!w. ?v. f x w v /\ g y w /\ ~h x y) ==> 533 ~(!w. ?v. f x w v /\ g z w /\ ~h x z) ==> 534 (!w. ?v. f y w v /\ g y w /\ ~h y x) /\ 535 !w. ?v. f z w v /\ g y w /\ ~h z y)`}, 536 537{name = "GILMORE_9a", 538 comments = 539["Translation of Gilmore procedure using separate definitions. [JRH]"], 540 goal = ` 541(!x y. p x y <=> !w. ?v. f x w v /\ g y w /\ ~h x y) ==> 542!x. ?y. !z. 543 (p y x ==> p x z ==> p x y) /\ (p x y ==> ~p x z ==> p y x /\ p z y)`}, 544 545{name = "BAD_CONNECTIONS", 546 comments = 547["The interesting example where connections make the proof longer. [JRH]"], 548 goal = ` 549~a /\ (a \/ b) /\ (c \/ d) /\ (~b \/ e \/ f) /\ (~c \/ ~e) /\ (~c \/ ~f) /\ 550(~b \/ g \/ h) /\ (~d \/ ~g) /\ (~d \/ ~h) ==> F`}, 551 552{name = "LOS", 553 comments = 554["The classic Los puzzle. (Clausal version MSC006-1 in the TPTP library.)", 555 "Note: this is actually in the decidable AE subset, though that doesn't", 556 "yield a very efficient proof. [JRH]"], 557 goal = ` 558(!x y z. p x y ==> p y z ==> p x z) /\ 559(!x y z. q x y ==> q y z ==> q x z) /\ (!x y. q x y ==> q y x) /\ 560(!x y. p x y \/ q x y) ==> (!x y. p x y) \/ !x y. q x y`}, 561 562{name = "STEAM_ROLLER", 563 comments = [], 564 goal = ` 565((!x. p1 x ==> p0 x) /\ ?x. p1 x) /\ ((!x. p2 x ==> p0 x) /\ ?x. p2 x) /\ 566((!x. p3 x ==> p0 x) /\ ?x. p3 x) /\ ((!x. p4 x ==> p0 x) /\ ?x. p4 x) /\ 567((!x. p5 x ==> p0 x) /\ ?x. p5 x) /\ ((?x. q1 x) /\ !x. q1 x ==> q0 x) /\ 568(!x. 569 p0 x ==> 570 (!y. q0 y ==> r x y) \/ 571 !y. p0 y /\ s0 y x /\ (?z. q0 z /\ r y z) ==> r x y) /\ 572(!x y. p3 y /\ (p5 x \/ p4 x) ==> s0 x y) /\ 573(!x y. p3 x /\ p2 y ==> s0 x y) /\ (!x y. p2 x /\ p1 y ==> s0 x y) /\ 574(!x y. p1 x /\ (p2 y \/ q1 y) ==> ~r x y) /\ 575(!x y. p3 x /\ p4 y ==> r x y) /\ (!x y. p3 x /\ p5 y ==> ~r x y) /\ 576(!x. p4 x \/ p5 x ==> ?y. q0 y /\ r x y) ==> 577?x y. p0 x /\ p0 y /\ ?z. q1 z /\ r y z /\ r x y`}, 578 579{name = "MODEL_COMPLETENESS", 580 comments = ["An incestuous example used to establish completeness", 581 "characterization. [JRH]"], 582 goal = ` 583(!w x. sentence x ==> holds w x \/ holds w (not x)) /\ 584(!w x. ~(holds w x /\ holds w (not x))) ==> 585((!x. 586 sentence x ==> 587 (!w. models w s ==> holds w x) \/ 588 !w. models w s ==> holds w (not x)) <=> 589 !w v. 590 models w s /\ models v s ==> 591 !x. sentence x ==> (holds w x <=> holds v x))`} 592 593] @ 594 595(* ========================================================================= *) 596(* Problems with equality. *) 597(* ========================================================================= *) 598 599mkProblems "equality" "Equality problems from various sources" [ 600 601(* ------------------------------------------------------------------------- *) 602(* Trivia (some of which demonstrate ex-bugs in the prover). *) 603(* ------------------------------------------------------------------------- *) 604 605{name = "REFLEXIVITY", 606 comments = [], 607 goal = ` 608c = c`}, 609 610{name = "SYMMETRY", 611 comments = [], 612 goal = ` 613!x y. x = y ==> y = x`}, 614 615{name = "TRANSITIVITY", 616 comments = [], 617 goal = ` 618!x y z. x = y /\ y = z ==> x = z`}, 619 620{name = "TRANS_SYMM", 621 comments = [], 622 goal = ` 623!x y z. x = y /\ y = z ==> z = x`}, 624 625{name = "SUBSTITUTIVITY", 626 comments = [], 627 goal = ` 628!x y. f x /\ x = y ==> f y`}, 629 630{name = "CYCLIC_SUBSTITUTION_BUG", 631 comments = [], 632 goal = ` 633!y. (!x. y = g (c x)) ==> ?z. y = g z`}, 634 635{name = "JUDITA_1", 636 comments = [], 637 goal = ` 638~(a = b) /\ (!x. x = c) ==> F`}, 639 640{name = "JUDITA_2", 641 comments = [], 642 goal = ` 643~(a = b) /\ (!x y. x = y) ==> F`}, 644 645{name = "JUDITA_3", 646 comments = [], 647 goal = ` 648p a /\ ~p b /\ (!x. x = c) ==> F`}, 649 650{name = "JUDITA_4", 651 comments = [], 652 goal = ` 653p a /\ ~p b /\ (!x y. x = y) ==> F`}, 654 655{name = "JUDITA_5", 656 comments = [], 657 goal = ` 658p a /\ p b /\ ~(a = b) /\ ~p c /\ (!x. x = a \/ x = d) ==> F`}, 659 660{name = "INJECTIVITY_1", 661 comments = [], 662 goal = ` 663(!x y. f x = f y ==> x = y) /\ f a = f b ==> a = b`}, 664 665{name = "INJECTIVITY_2", 666 comments = [], 667 goal = ` 668(!x y. g (f x) = g (f y) ==> x = y) /\ f a = f b ==> a = b`}, 669 670{name = "SELF_REWRITE", 671 comments = [], 672 goal = ` 673f (g (h c)) = h c /\ g (h c) = b /\ f b = a /\ (!x. ~(a = h x)) ==> F`}, 674 675{name = "EQUALITY_ORDERING", 676 comments = ["Positive resolution saturates if equality literals are", 677 "ordered like other literals, instead of considering their", 678 "left and right sides."], 679 goal = ` 680p a /\ q a /\ q b /\ r b /\ (~p c \/ c = a) /\ (~r c \/ c = b) /\ 681(!x. ~q x \/ p x \/ r x) /\ (~p c \/ ~q c) /\ (~q c \/ ~r c) /\ 682(c = b \/ p c \/ q c) /\ (~p b \/ c = a \/ q c) ==> F`}, 683 684(* ------------------------------------------------------------------------- *) 685(* Simple equality problems. *) 686(* ------------------------------------------------------------------------- *) 687 688{name = "P48", 689 comments = [], 690 goal = ` 691(a = b \/ c = d) /\ (a = c \/ b = d) ==> a = d \/ b = c`}, 692 693{name = "P49", 694 comments = [], 695 goal = ` 696(?x y. !z. z = x \/ z = y) /\ p a /\ p b /\ ~(a = b) ==> !x. p x`}, 697 698{name = "P51", 699 comments = [], 700 goal = ` 701(?z w. !x y. f0 x y <=> x = z /\ y = w) ==> 702?z. !x. (?w. !y. f0 x y <=> y = w) <=> x = z`}, 703 704{name = "P52", 705 comments = [], 706 goal = ` 707(?z w. !x y. f0 x y <=> x = z /\ y = w) ==> 708?w. !y. (?z. !x. f0 x y <=> x = z) <=> y = w`}, 709 710{name = "UNSKOLEMIZED_MELHAM", 711 comments = ["The Melham problem after an inverse skolemization step."], 712 goal = ` 713(!x y. g x = g y ==> f x = f y) ==> !y. ?w. !x. y = g x ==> w = f x`}, 714 715{name = "CONGRUENCE_CLOSURE_EXAMPLE", 716 comments = ["The example always given for congruence closure."], 717 goal = ` 718!x. f (f (f (f (f x)))) = x /\ f (f (f x)) = x ==> f x = x`}, 719 720{name = "EWD_1", 721 comments = 722["A simple example (see EWD1266a and the application to Morley's", 723 "theorem). [JRH]"], 724 goal = ` 725(!x. f x ==> g x) /\ (?x. f x) /\ (!x y. g x /\ g y ==> x = y) ==> 726!y. g y ==> f y`}, 727 728{name = "EWD_2", 729 comments = [], 730 goal = ` 731(!x. f (f x) = f x) /\ (!x. ?y. f y = x) ==> !x. f x = x`}, 732 733{name = "JIA", 734 comments = ["Needs only the K combinator"], 735 goal = ` 736(!x y. k . x . y = x) /\ (!v. P (v . a) a) /\ (!w. Q (w . b) b) ==> 737!z. ?x y. P (z . x . y) x /\ Q (z . x . y) y`}, 738 739{name = "WISHNU", 740 comments = ["Wishnu Prasetya's example. [JRH]"], 741 goal = ` 742(?x. x = f (g x) /\ !x'. x' = f (g x') ==> x = x') <=> 743?y. y = g (f y) /\ !y'. y' = g (f y') ==> y = y'`}, 744 745{name = "AGATHA", 746 comments = ["An equality version of the Agatha puzzle. [JRH]"], 747 goal = ` 748(?x. lives x /\ killed x agatha) /\ 749(lives agatha /\ lives butler /\ lives charles) /\ 750(!x. lives x ==> x = agatha \/ x = butler \/ x = charles) /\ 751(!x y. killed x y ==> hates x y) /\ (!x y. killed x y ==> ~richer x y) /\ 752(!x. hates agatha x ==> ~hates charles x) /\ 753(!x. ~(x = butler) ==> hates agatha x) /\ 754(!x. ~richer x agatha ==> hates butler x) /\ 755(!x. hates agatha x ==> hates butler x) /\ (!x. ?y. ~hates x y) /\ 756~(agatha = butler) ==> 757killed agatha agatha /\ ~killed butler agatha /\ ~killed charles agatha`}, 758 759{name = "DIVIDES_9_1", 760 comments = [], 761 goal = ` 762(!x y. x * y = y * x) /\ (!x y z. x * y * z = x * (y * z)) /\ 763(!x y. divides x y <=> ?z. y = z * x) ==> 764!x y z. divides x y ==> divides x (z * y)`}, 765 766{name = "DIVIDES_9_2", 767 comments = [], 768 goal = ` 769(!x y. x * y = y * x) /\ (!x y z. x * y * z = x * (y * z)) /\ 770(!x y. divides x y <=> ?z. z * x = y) ==> 771!x y z. divides x y ==> divides x (z * y)`}, 772 773{name = "XOR_COUNT_COMMUTATIVE", 774 comments = ["The xor literal counting function in Normalize is commutative."], 775 goal = ` 776(!x y. x + y = y + x) /\ (!x y z. x + (y + z) = x + y + z) /\ 777(!x y. x * y = y * x) /\ (!x y z. x * (y * z) = x * y * z) /\ 778pl = p1 * p2 + n1 * n2 /\ nl = p1 * n2 + n1 * p2 /\ 779pr = p2 * p1 + n2 * n1 /\ nr = p2 * n1 + n2 * p1 ==> pl = pr /\ nl = nr`}, 780 781{name = "XOR_COUNT_ASSOCIATIVE", 782 comments = ["The xor literal counting function in Normalize is associative."], 783 goal = ` 784(!x y. x + y = y + x) /\ (!x y z. x + (y + z) = x + y + z) /\ 785(!x y. x * y = y * x) /\ (!x y z. x * (y * z) = x * y * z) /\ 786px = p1 * p2 + n1 * n2 /\ nx = p1 * n2 + n1 * p2 /\ 787pl = px * p3 + nx * n3 /\ nl = px * n3 + nx * p3 /\ 788py = p2 * p3 + n2 * n3 /\ ny = p2 * n3 + n2 * p3 /\ 789pr = p1 * py + n1 * ny /\ nr = p1 * ny + n1 * py ==> pl = pr /\ nl = nr`}, 790 791{name = "REVERSE_REVERSE", 792 comments = ["Proving the goal", 793 " !l. finite l ==> rev (rev l) = l", 794 "after first generalizing it to", 795 " !l k. finite l /\\ finite k ==> rev (rev l @ k) = rev k @ l", 796 "and then applying list induction."], 797 goal = ` 798finite nil /\ (!h t. finite (h :: t) <=> finite t) /\ 799(!l1 l2. finite (l1 @ l2) <=> finite l1 /\ finite l2) /\ 800(!l. nil @ l = l) /\ (!h t l. (h :: t) @ l = h :: t @ l) /\ 801rev nil = nil /\ (!h t. rev (h :: t) = rev t @ h :: nil) /\ 802(!l. l @ nil = l) /\ (!l1 l2 l3. l1 @ l2 @ l3 = (l1 @ l2) @ l3) ==> 803(!k. finite k ==> rev (rev nil @ k) = rev k @ nil) /\ 804!t. 805 finite t ==> (!k. finite k ==> rev (rev t @ k) = rev k @ t) ==> 806 !h k. finite k ==> rev (rev (h :: t) @ k) = rev k @ h :: t`}, 807 808(* ------------------------------------------------------------------------- *) 809(* Group theory examples. *) 810(* ------------------------------------------------------------------------- *) 811 812{name = "GROUP_INVERSE_INVERSE", 813 comments = [], 814 goal = ` 815(!x y z. x * (y * z) = x * y * z) /\ (!x. e * x = x) /\ 816(!x. i x * x = e) ==> !x. i (i x) = x`}, 817 818{name = "GROUP_RIGHT_INVERSE", 819 comments = ["Size 18, 61814 seconds. [JRH]"], 820 goal = ` 821(!x y z. x * (y * z) = x * y * z) /\ (!x. e * x = x) /\ 822(!x. i x * x = e) ==> !x. x * i x = e`}, 823 824{name = "GROUP_RIGHT_IDENTITY", 825 comments = [], 826 goal = ` 827(!x y z. x * (y * z) = x * y * z) /\ (!x. e * x = x) /\ 828(!x. i x * x = e) ==> !x. x * e = x`}, 829 830{name = "GROUP_IDENTITY_EQUIV", 831 comments = [], 832 goal = ` 833(!x y z. x * (y * z) = x * y * z) /\ (!x. e * x = x) /\ 834(!x. i x * x = e) ==> !x. x * x = x <=> x = e`}, 835 836{name = "KLEIN_GROUP_COMMUTATIVE", 837 comments = [], 838 goal = ` 839(!x y z. x * (y * z) = x * y * z) /\ (!x. e * x = x) /\ (!x. x * e = x) /\ 840(!x. x * x = e) ==> !x y. x * y = y * x`}, 841 842{name = "DOUBLE_DISTRIB", 843 comments = ["From a John Harrison post to hol-info on 2008-04-15"], 844 goal = ` 845(!x y z. x * y * z = x * z * (y * z)) /\ 846(!x y z. z * (x * y) = z * x * (z * y)) ==> 847!a b c. a * b * (c * a) = a * c * (b * a)`}, 848 849(* ------------------------------------------------------------------------- *) 850(* Ring theory examples. *) 851(* ------------------------------------------------------------------------- *) 852 853{name = "CONWAY_2", 854 comments = ["From a John Harrison post to hol-info on 2008-04-15"], 855 goal = ` 856(!x. 0 + x = x) /\ (!x y. x + y = y + x) /\ 857(!x y z. x + (y + z) = x + y + z) /\ (!x. 1 * x = x) /\ (!x. x * 1 = x) /\ 858(!x y z. x * (y * z) = x * y * z) /\ (!x. 0 * x = 0) /\ (!x. x * 0 = 0) /\ 859(!x y z. x * (y + z) = x * y + x * z) /\ 860(!x y z. (x + y) * z = x * z + y * z) /\ 861(!x y. star (x * y) = 1 + x * star (y * x) * y) /\ 862(!x y. star (x + y) = star (star (x) * y) * star (x)) ==> 863!a. star (star (star (star (a)))) = star (star (star (a)))`}, 864 865{name = "JACOBSON_2", 866 comments = [], 867 goal = ` 868(!x. 0 + x = x) /\ (!x. x + 0 = x) /\ (!x. ~x + x = 0) /\ 869(!x. x + ~x = 0) /\ (!x y z. x + (y + z) = x + y + z) /\ 870(!x y. x + y = y + x) /\ (!x y z. x * (y * z) = x * y * z) /\ 871(!x y z. x * (y + z) = x * y + x * z) /\ 872(!x y z. (x + y) * z = x * z + y * z) /\ (!x. x * x = x) ==> 873!x y. x * y = y * x`}, 874 875{name = "JACOBSON_3", 876 comments = [], 877 goal = ` 878(!x. 0 + x = x) /\ (!x. x + 0 = x) /\ (!x. ~x + x = 0) /\ 879(!x. x + ~x = 0) /\ (!x y z. x + (y + z) = x + y + z) /\ 880(!x y. x + y = y + x) /\ (!x y z. x * (y * z) = x * y * z) /\ 881(!x y z. x * (y + z) = x * y + x * z) /\ 882(!x y z. (x + y) * z = x * z + y * z) /\ (!x. x * (x * x) = x) ==> 883!x y. x * y = y * x`}, 884 885(* ------------------------------------------------------------------------- *) 886(* Set theory examples. *) 887(* ------------------------------------------------------------------------- *) 888 889{name = "UNION_2_SUBSET", 890 comments = [], 891 goal = ` 892(!x y. subset x y ==> subset y x ==> x = y) /\ 893(!x y. (!z. member z x ==> member z y) ==> subset x y) /\ 894(!x y z. member z (x + y) <=> member z x \/ member z y) ==> 895!x y. subset (x + y) (y + x)`}, 896 897{name = "UNION_2", 898 comments = [], 899 goal = ` 900(!x y. subset x y ==> subset y x ==> x = y) /\ 901(!x y. (!z. member z x ==> member z y) ==> subset x y) /\ 902(!x y z. member z (x + y) <=> member z x \/ member z y) ==> 903!x y. x + y = y + x`}, 904 905{name = "UNION_3_SUBSET", 906 comments = ["From an email from Tobias Nipkow, 4 Nov 2008.", 907 "The Isabelle version of metis diverges on this goal"], 908 goal = ` 909(!x y. subset x y ==> subset y x ==> x = y) /\ 910(!x y. (!z. member z x ==> member z y) ==> subset x y) /\ 911(!x y z. member z (x + y) <=> member z x \/ member z y) ==> 912!x y z. subset (x + y + z) (z + y + x)`}, 913 914{name = "UNION_3", 915 comments = ["From an email from Tobias Nipkow, 28 Oct 2008.", 916 "The Isabelle version of metis diverges on this goal"], 917 goal = ` 918(!x y. subset x y ==> subset y x ==> x = y) /\ 919(!x y. (!z. member z x ==> member z y) ==> subset x y) /\ 920(!x y z. member z (x + y) <=> member z x \/ member z y) ==> 921!x y z. x + y + z = z + y + x`}] @ 922 923(* ========================================================================= *) 924(* Some sample problems from the TPTP archive. *) 925(* Note: for brevity some relation/function names have been shortened. *) 926(* ========================================================================= *) 927 928mkProblems "tptp" "Sample problems from the TPTP collection" 929 930[ 931 932{name = "ALG005-1", 933 comments = [], 934 goal = ` 935(!x y. x + (y + x) = x) /\ (!x y. x + (x + y) = y + (y + x)) /\ 936(!x y z. x + y + z = x + z + (y + z)) /\ (!x y. x * y = x + (x + y)) ==> 937~(a * b * c = a * (b * c)) ==> F`}, 938 939{name = "ALG006-1", 940 comments = [], 941 goal = ` 942(!x y. x + (y + x) = x) /\ (!x y. x + (x + y) = y + (y + x)) /\ 943(!x y z. x + y + z = x + z + (y + z)) ==> ~(a + c + b = a + b + c) ==> F`}, 944 945{name = "BOO021-1", 946 comments = [], 947 goal = ` 948(!x y. (x + y) * y = y) /\ (!x y z. x * (y + z) = y * x + z * x) /\ 949(!x. x + i x = 1) /\ (!x y. x * y + y = y) /\ 950(!x y z. x + y * z = (y + x) * (z + x)) /\ (!x. x * i x = 0) ==> 951~(b * a = a * b) ==> F`}, 952 953{name = "COL058-2", 954 comments = [], 955 goal = ` 956(!x y. r (r 0 x) y = r x (r y y)) ==> 957~(r (r (r 0 (r (r 0 (r 0 0)) (r 0 (r 0 0)))) (r 0 (r 0 0))) 958 (r (r 0 (r (r 0 (r 0 0)) (r 0 (r 0 0)))) (r 0 (r 0 0))) = 959 r (r 0 (r (r 0 (r 0 0)) (r 0 (r 0 0)))) (r 0 (r 0 0))) ==> F`}, 960 961{name = "COL060-3", 962 comments = [], 963 goal = ` 964(!x y z. b . x . y . z = x . (y . z)) /\ (!x y. t . x . y = y . x) ==> 965~(b . (b . (t . b) . b) . t . x . y . z = y . (x . z)) ==> F`}, 966 967{name = "GEO002-4", 968 comments = [], 969 goal = ` 970(!x y z v. ~between x y z \/ ~between y v z \/ between x y v) /\ 971(!x y z. ~equidistant x y z z \/ x == y) /\ 972(!x y z v w. 973 ~between x y z \/ ~between v z w \/ 974 between x (outer_pasch y x v w z) v) /\ 975(!x y z v w. 976 ~between x y z \/ ~between v z w \/ 977 between w y (outer_pasch y x v w z)) /\ 978(!x y z v. between x y (extension x y z v)) /\ 979(!x y z v. equidistant x (extension y x z v) z v) /\ 980(!x y z v. ~(x == y) \/ ~between z v x \/ between z v y) ==> 981~between a a b ==> F`}, 982 983{name = "GEO036-2", 984 comments = [], 985 goal = ` 986(!x y. equidistant x y y x) /\ 987(!x y z x' y' z'. 988 ~equidistant x y z x' \/ ~equidistant x y y' z' \/ 989 equidistant z x' y' z') /\ (!x y z. ~equidistant x y z z \/ x = y) /\ 990(!x y z v. between x y (extension x y z v)) /\ 991(!x y z v. equidistant x (extension y x z v) z v) /\ 992(!x y z v w x' y' z'. 993 ~equidistant x y z v \/ ~equidistant y w v x' \/ 994 ~equidistant x y' z z' \/ ~equidistant y y' v z' \/ ~between x y w \/ 995 ~between z v x' \/ x = y \/ equidistant w y' x' z') /\ 996(!x y. ~between x y x \/ x = y) /\ 997(!x y z v w. 998 ~between x y z \/ ~between v w z \/ 999 between y (inner_pasch x y z w v) v) /\ 1000(!x y z v w. 1001 ~between x y z \/ ~between v w z \/ 1002 between w (inner_pasch x y z w v) x) /\ 1003~between lower_dimension_point_1 lower_dimension_point_2 1004 lower_dimension_point_3 /\ 1005~between lower_dimension_point_2 lower_dimension_point_3 1006 lower_dimension_point_1 /\ 1007~between lower_dimension_point_3 lower_dimension_point_1 1008 lower_dimension_point_2 /\ 1009(!x y z v w. 1010 ~equidistant x y x z \/ ~equidistant v y v z \/ ~equidistant w y w z \/ 1011 between x v w \/ between v w x \/ between w x v \/ y = z) /\ 1012(!x y z v w. 1013 ~between x y z \/ ~between v y w \/ x = y \/ 1014 between x v (euclid1 x v y w z)) /\ 1015(!x y z v w. 1016 ~between x y z \/ ~between v y w \/ x = y \/ 1017 between x w (euclid2 x v y w z)) /\ 1018(!x y z v w. 1019 ~between x y z \/ ~between v y w \/ x = y \/ 1020 between (euclid1 x v y w z) z (euclid2 x v y w z)) /\ 1021(!x y z x' y' z'. 1022 ~equidistant x y x z \/ ~equidistant x x' x y' \/ ~between x y x' \/ 1023 ~between y z' x' \/ between z (continuous x y z z' x' y') y') /\ 1024(!x y z x' y' z'. 1025 ~equidistant x y x z \/ ~equidistant x x' x y' \/ ~between x y x' \/ 1026 ~between y z' x' \/ equidistant x z' x (continuous x y z z' x' y')) /\ 1027(!x y z v. ~(x = y) \/ ~between x z v \/ between y z v) /\ 1028(!x y z v. ~(x = y) \/ ~between z x v \/ between z y v) /\ 1029(!x y z v. ~(x = y) \/ ~between z v x \/ between z v y) /\ 1030(!x y z v w. ~(x = y) \/ ~equidistant x z v w \/ equidistant y z v w) /\ 1031(!x y z v w. ~(x = y) \/ ~equidistant z x v w \/ equidistant z y v w) /\ 1032(!x y z v w. ~(x = y) \/ ~equidistant z v x w \/ equidistant z v y w) /\ 1033(!x y z v w. ~(x = y) \/ ~equidistant z v w x \/ equidistant z v w y) /\ 1034(!x y z x' y' z'. 1035 ~(x = y) \/ inner_pasch x z x' y' z' = inner_pasch y z x' y' z') /\ 1036(!x y z x' y' z'. 1037 ~(x = y) \/ inner_pasch z x x' y' z' = inner_pasch z y x' y' z') /\ 1038(!x y z x' y' z'. 1039 ~(x = y) \/ inner_pasch z x' x y' z' = inner_pasch z x' y y' z') /\ 1040(!x y z x' y' z'. 1041 ~(x = y) \/ inner_pasch z x' y' x z' = inner_pasch z x' y' y z') /\ 1042(!x y z x' y' z'. 1043 ~(x = y) \/ inner_pasch z x' y' z' x = inner_pasch z x' y' z' y) /\ 1044(!x y z x' y' z'. 1045 ~(x = y) \/ euclid1 x z x' y' z' = euclid1 y z x' y' z') /\ 1046(!x y z x' y' z'. 1047 ~(x = y) \/ euclid1 z x x' y' z' = euclid1 z y x' y' z') /\ 1048(!x y z x' y' z'. 1049 ~(x = y) \/ euclid1 z x' x y' z' = euclid1 z x' y y' z') /\ 1050(!x y z x' y' z'. 1051 ~(x = y) \/ euclid1 z x' y' x z' = euclid1 z x' y' y z') /\ 1052(!x y z x' y' z'. 1053 ~(x = y) \/ euclid1 z x' y' z' x = euclid1 z x' y' z' y) /\ 1054(!x y z x' y' z'. 1055 ~(x = y) \/ euclid2 x z x' y' z' = euclid2 y z x' y' z') /\ 1056(!x y z x' y' z'. 1057 ~(x = y) \/ euclid2 z x x' y' z' = euclid2 z y x' y' z') /\ 1058(!x y z x' y' z'. 1059 ~(x = y) \/ euclid2 z x' x y' z' = euclid2 z x' y y' z') /\ 1060(!x y z x' y' z'. 1061 ~(x = y) \/ euclid2 z x' y' x z' = euclid2 z x' y' y z') /\ 1062(!x y z x' y' z'. 1063 ~(x = y) \/ euclid2 z x' y' z' x = euclid2 z x' y' z' y) /\ 1064(!x y z v w. ~(x = y) \/ extension x z v w = extension y z v w) /\ 1065(!x y z v w. ~(x = y) \/ extension z x v w = extension z y v w) /\ 1066(!x y z v w. ~(x = y) \/ extension z v x w = extension z v y w) /\ 1067(!x y z v w. ~(x = y) \/ extension z v w x = extension z v w y) /\ 1068(!x y z v w x' y'. 1069 ~(x = y) \/ continuous x z v w x' y' = continuous y z v w x' y') /\ 1070(!x y z v w x' y'. 1071 ~(x = y) \/ continuous z x v w x' y' = continuous z y v w x' y') /\ 1072(!x y z v w x' y'. 1073 ~(x = y) \/ continuous z v x w x' y' = continuous z v y w x' y') /\ 1074(!x y z v w x' y'. 1075 ~(x = y) \/ continuous z v w x x' y' = continuous z v w y x' y') /\ 1076(!x y z v w x' y'. 1077 ~(x = y) \/ continuous z v w x' x y' = continuous z v w x' y y') /\ 1078(!x y z v w x' y'. 1079 ~(x = y) \/ continuous z v w x' y' x = continuous z v w x' y' y) ==> 1080lower_dimension_point_1 = lower_dimension_point_2 \/ 1081lower_dimension_point_2 = lower_dimension_point_3 \/ 1082lower_dimension_point_1 = lower_dimension_point_3 ==> F`}, 1083 1084{name = "GRP010-4", 1085 comments = [], 1086 goal = ` 1087(!x. x = x) /\ (!x y. ~(x = y) \/ y = x) /\ 1088(!x y z. ~(x = y) \/ ~(y = z) \/ x = z) /\ (!x y. ~(x = y) \/ i x = i y) /\ 1089(!x y z. ~(x = y) \/ x * z = y * z) /\ 1090(!x y z. ~(x = y) \/ z * x = z * y) /\ (!x y z. x * y * z = x * (y * z)) /\ 1091(!x. 1 * x = x) /\ (!x. i x * x = 1) /\ c * b = 1 ==> ~(b * c = 1) ==> F`}, 1092 1093{name = "GRP057-1", 1094 comments = [], 1095 goal = ` 1096(!x. x = x) /\ (!x y. ~(x = y) \/ y = x) /\ 1097(!x y z. ~(x = y) \/ ~(y = z) \/ x = z) /\ 1098(!x y z v. x * i (i (i y * (i x * z)) * v * i (y * v)) = z) /\ 1099(!x y. ~(x = y) \/ i x = i y) /\ (!x y z. ~(x = y) \/ x * z = y * z) /\ 1100(!x y z. ~(x = y) \/ z * x = z * y) ==> 1101~(i a1 * a1 = i b1 * b1) \/ ~(i b2 * b2 * a2 = a2) \/ 1102~(a3 * b3 * c3 = a3 * (b3 * c3)) ==> F`}, 1103 1104{name = "GRP086-1", 1105 comments = ["Bug check: used to be unsolvable without sticky constraints"], 1106 goal = ` 1107(!x. x = x) /\ (!x y. ~(x = y) \/ y = x) /\ 1108(!x y z. ~(x = y) \/ ~(y = z) \/ x = z) /\ 1109(!x y z. x * (y * z * i (x * z)) = y) /\ (!x y. ~(x = y) \/ i x = i y) /\ 1110(!x y z. ~(x = y) \/ x * z = y * z) /\ 1111(!x y z. ~(x = y) \/ z * x = z * y) ==> 1112(!x y. 1113 ~(i a1 * a1 = i b1 * b1) \/ ~(i b2 * b2 * a2 = a2) \/ 1114 ~(a3 * b3 * c3 = a3 * (b3 * c3)) \/ ~(x * y = y * x)) ==> F`}, 1115 1116{name = "GRP104-1", 1117 comments = [], 1118 goal = ` 1119(!x. x = x) /\ (!x y. ~(x = y) \/ y = x) /\ 1120(!x y z. ~(x = y) \/ ~(y = z) \/ x = z) /\ 1121(!x y z. 1122 double_divide x 1123 (inverse 1124 (double_divide 1125 (inverse (double_divide (double_divide x y) (inverse z))) y)) = 1126 z) /\ (!x y. x * y = inverse (double_divide y x)) /\ 1127(!x y. ~(x = y) \/ inverse x = inverse y) /\ 1128(!x y z. ~(x = y) \/ x * z = y * z) /\ 1129(!x y z. ~(x = y) \/ z * x = z * y) /\ 1130(!x y z. ~(x = y) \/ double_divide x z = double_divide y z) /\ 1131(!x y z. ~(x = y) \/ double_divide z x = double_divide z y) ==> 1132(!x y. 1133 ~(inverse a1 * a1 = inverse b1 * b1) \/ ~(inverse b2 * b2 * a2 = a2) \/ 1134 ~(a3 * b3 * c3 = a3 * (b3 * c3)) \/ ~(x * y = y * x)) ==> F`}, 1135 1136{name = "GRP128-4.003", 1137 comments = [], 1138 goal = ` 1139(!x y. 1140 ~elt x \/ ~elt y \/ product e_1 x y \/ product e_2 x y \/ 1141 product e_3 x y) /\ 1142(!x y. 1143 ~elt x \/ ~elt y \/ product x e_1 y \/ product x e_2 y \/ 1144 product x e_3 y) /\ elt e_1 /\ elt e_2 /\ elt e_3 /\ ~(e_1 == e_2) /\ 1145~(e_1 == e_3) /\ ~(e_2 == e_1) /\ ~(e_2 == e_3) /\ ~(e_3 == e_1) /\ 1146~(e_3 == e_2) /\ 1147(!x y. 1148 ~elt x \/ ~elt y \/ product x y e_1 \/ product x y e_2 \/ 1149 product x y e_3) /\ 1150(!x y z v. ~product x y z \/ ~product x y v \/ z == v) /\ 1151(!x y z v. ~product x y z \/ ~product x v z \/ y == v) /\ 1152(!x y z v. ~product x y z \/ ~product v y z \/ x == v) ==> 1153(!x y z v. product x y z \/ ~product x z v \/ ~product z y v) /\ 1154(!x y z v. product x y z \/ ~product v x z \/ ~product v y x) /\ 1155(!x y z v. ~product x y z \/ ~product z y v \/ product x z v) ==> F`}, 1156 1157{name = "HEN006-3", 1158 comments = [], 1159 goal = ` 1160(!x. x = x) /\ (!x y. ~(x = y) \/ y = x) /\ 1161(!x y z. ~(x = y) \/ ~(y = z) \/ x = z) /\ 1162(!x y. ~(x <= y) \/ x / y = 0) /\ (!x y. ~(x / y = 0) \/ x <= y) /\ 1163(!x y. x / y <= x) /\ (!x y z. x / y / (z / y) <= x / z / y) /\ 1164(!x. 0 <= x) /\ (!x y. ~(x <= y) \/ ~(y <= x) \/ x = y) /\ (!x. x <= 1) /\ 1165(!x y z. ~(x = y) \/ x / z = y / z) /\ 1166(!x y z. ~(x = y) \/ z / x = z / y) /\ 1167(!x y z. ~(x = y) \/ ~(x <= z) \/ y <= z) /\ 1168(!x y z. ~(x = y) \/ ~(z <= x) \/ z <= y) /\ a / b <= d ==> 1169~(a / d <= b) ==> F`}, 1170 1171{name = "LAT005-3", 1172 comments = ["SAM's lemma"], 1173 goal = ` 1174(!x. x = x) /\ (!x y. ~(x = y) \/ y = x) /\ 1175(!x y z. ~(x = y) \/ ~(y = z) \/ x = z) /\ (!x. meet x x = x) /\ 1176(!x. join x x = x) /\ (!x y. meet x (join x y) = x) /\ 1177(!x y. join x (meet x y) = x) /\ (!x y. meet x y = meet y x) /\ 1178(!x y. join x y = join y x) /\ 1179(!x y z. meet (meet x y) z = meet x (meet y z)) /\ 1180(!x y z. join (join x y) z = join x (join y z)) /\ 1181(!x y z. ~(x = y) \/ join x z = join y z) /\ 1182(!x y z. ~(x = y) \/ join z x = join z y) /\ 1183(!x y z. ~(x = y) \/ meet x z = meet y z) /\ 1184(!x y z. ~(x = y) \/ meet z x = meet z y) /\ (!x. meet x 0 = 0) /\ 1185(!x. join x 0 = x) /\ (!x. meet x 1 = x) /\ (!x. join x 1 = 1) /\ 1186(!x y z. ~(meet x y = x) \/ meet y (join x z) = join x (meet z y)) /\ 1187(!x y. ~complement x y \/ meet x y = 0) /\ 1188(!x y. ~complement x y \/ join x y = 1) /\ 1189(!x y. ~(meet x y = 0) \/ ~(join x y = 1) \/ complement x y) /\ 1190(!x y z. ~(x = y) \/ ~complement x z \/ complement y z) /\ 1191(!x y z. ~(x = y) \/ ~complement z x \/ complement z y) /\ 1192complement r1 (join a b) /\ complement r2 (meet a b) ==> 1193~(r1 = meet (join r1 (meet r2 b)) (join r1 (meet r2 a))) ==> F`}, 1194 1195{name = "LCL009-1", 1196 comments = [], 1197 goal = ` 1198(!x y. ~p (x - y) \/ ~p x \/ p y) /\ 1199(!x y z. p (x - y - (z - y - (x - z)))) ==> 1200~p (a - b - c - (a - (b - c))) ==> F`}, 1201 1202{name = "LCL087-1", 1203 comments = 1204["Solved quickly by resolution when NOT tracking term-ordering constraints."], 1205 goal = ` 1206(!x y. ~p (implies x y) \/ ~p x \/ p y) /\ 1207(!x y z v w. 1208 p 1209 (implies (implies (implies x y) (implies z v)) 1210 (implies w (implies (implies v x) (implies z x))))) ==> 1211~p (implies a (implies b a)) ==> F`}, 1212 1213{name = "LCL107-1", 1214 comments = ["A very small problem that's tricky to prove."], 1215 goal = ` 1216(!x y. ~p (x - y) \/ ~p x \/ p y) /\ 1217(!x y z v w x' y'. 1218 p 1219 (x - y - z - (v - w - (x' - w - (x' - v) - y')) - 1220 (z - (y - x - y')))) ==> ~p (a - b - c - (e - b - (a - e - c))) ==> F`}, 1221 1222{name = "LCL187-1", 1223 comments = [], 1224 goal = ` 1225(!x. axiom (or (not (or x x)) x)) /\ (!x y. axiom (or (not x) (or y x))) /\ 1226(!x y. axiom (or (not (or x y)) (or y x))) /\ 1227(!x y z. axiom (or (not (or x (or y z))) (or y (or x z)))) /\ 1228(!x y z. axiom (or (not (or (not x) y)) (or (not (or z x)) (or z y)))) /\ 1229(!x. theorem x \/ ~axiom x) /\ 1230(!x y. theorem x \/ ~axiom (or (not y) x) \/ ~theorem y) /\ 1231(!x y z. 1232 theorem (or (not x) y) \/ ~axiom (or (not x) z) \/ 1233 ~theorem (or (not z) y)) ==> 1234~theorem (or (not p) (or (not (not p)) q)) ==> F`}, 1235 1236{name = "LDA007-3", 1237 comments = [], 1238 goal = ` 1239(!x. x = x) /\ (!x y. ~(x = y) \/ y = x) /\ 1240(!x y z. ~(x = y) \/ ~(y = z) \/ x = z) /\ 1241(!x y z. f x (f y z) = f (f x y) (f x z)) /\ 1242(!x y z. ~(x = y) \/ f x z = f y z) /\ 1243(!x y z. ~(x = y) \/ f z x = f z y) /\ tt = f t t /\ ts = f t s /\ 1244tt_ts = f tt ts /\ tk = f t k /\ tsk = f ts k ==> 1245~(f t tsk = f tt_ts tk) ==> F`}, 1246 1247{name = "NUM001-1", 1248 comments = [], 1249 goal = ` 1250(!x. x == x) /\ (!x y z. ~(x == y) \/ ~(y == z) \/ x == z) /\ 1251(!x y. x + y == y + x) /\ (!x y z. x + (y + z) == x + y + z) /\ 1252(!x y. x + y - y == x) /\ (!x y. x == x + y - y) /\ 1253(!x y z. x - y + z == x + z - y) /\ (!x y z. x + y - z == x - z + y) /\ 1254(!x y z v. ~(x == y) \/ ~(z == x + v) \/ z == y + v) /\ 1255(!x y z v. ~(x == y) \/ ~(z == v + x) \/ z == v + y) /\ 1256(!x y z v. ~(x == y) \/ ~(z == x - v) \/ z == y - v) /\ 1257(!x y z v. ~(x == y) \/ ~(z == v - x) \/ z == v - y) ==> 1258~(a + b + c == a + (b + c)) ==> F`}, 1259 1260{name = "NUM014-1", 1261 comments = [], 1262 goal = ` 1263(!x. product x x (square x)) /\ 1264(!x y z. ~product x y z \/ product y x z) /\ 1265(!x y z. ~product x y z \/ divides x z) /\ 1266(!x y z v. 1267 ~prime x \/ ~product y z v \/ ~divides x v \/ divides x y \/ 1268 divides x z) /\ prime a /\ product a (square c) (square b) ==> 1269~divides a b ==> F`}, 1270 1271{name = "PUZ001-1", 1272 comments = [], 1273 goal = ` 1274lives agatha /\ lives butler /\ lives charles /\ 1275(!x y. ~killed x y \/ ~richer x y) /\ 1276(!x. ~hates agatha x \/ ~hates charles x) /\ 1277(!x. ~hates x agatha \/ ~hates x butler \/ ~hates x charles) /\ 1278hates agatha agatha /\ hates agatha charles /\ 1279(!x y. ~killed x y \/ hates x y) /\ 1280(!x. ~hates agatha x \/ hates butler x) /\ 1281(!x. ~lives x \/ richer x agatha \/ hates butler x) ==> 1282killed butler agatha \/ killed charles agatha ==> F`}, 1283 1284{name = "PUZ011-1", 1285 comments = 1286["Curiosity: solved trivially by meson without cache cutting, but not with."], 1287 goal = ` 1288ocean atlantic /\ ocean indian /\ borders atlantic brazil /\ 1289borders atlantic uruguay /\ borders atlantic venesuela /\ 1290borders atlantic zaire /\ borders atlantic nigeria /\ 1291borders atlantic angola /\ borders indian india /\ 1292borders indian pakistan /\ borders indian iran /\ borders indian somalia /\ 1293borders indian kenya /\ borders indian tanzania /\ south_american brazil /\ 1294south_american uruguay /\ south_american venesuela /\ african zaire /\ 1295african nigeria /\ african angola /\ african somalia /\ african kenya /\ 1296african tanzania /\ asian india /\ asian pakistan /\ asian iran ==> 1297(!x y z. 1298 ~ocean x \/ ~borders x y \/ ~african y \/ ~borders x z \/ ~asian z) ==> 1299F`}, 1300 1301{name = "PUZ020-1", 1302 comments = [], 1303 goal = ` 1304(!x. x = x) /\ (!x y. ~(x = y) \/ y = x) /\ 1305(!x y z. ~(x = y) \/ ~(y = z) \/ x = z) /\ 1306(!x y. ~(x = y) \/ statement_by x = statement_by y) /\ 1307(!x. ~person x \/ knight x \/ knave x) /\ 1308(!x. ~person x \/ ~knight x \/ ~knave x) /\ 1309(!x y. ~says x y \/ a_truth y \/ ~a_truth y) /\ 1310(!x y. ~says x y \/ ~(x = y)) /\ (!x y. ~says x y \/ y = statement_by x) /\ 1311(!x y. ~person x \/ ~(x = statement_by y)) /\ 1312(!x. ~person x \/ ~a_truth (statement_by x) \/ knight x) /\ 1313(!x. ~person x \/ a_truth (statement_by x) \/ knave x) /\ 1314(!x y. ~(x = y) \/ ~knight x \/ knight y) /\ 1315(!x y. ~(x = y) \/ ~knave x \/ knave y) /\ 1316(!x y. ~(x = y) \/ ~person x \/ person y) /\ 1317(!x y z. ~(x = y) \/ ~says x z \/ says y z) /\ 1318(!x y z. ~(x = y) \/ ~says z x \/ says z y) /\ 1319(!x y. ~(x = y) \/ ~a_truth x \/ a_truth y) /\ 1320(!x y. ~knight x \/ ~says x y \/ a_truth y) /\ 1321(!x y. ~knave x \/ ~says x y \/ ~a_truth y) /\ person husband /\ 1322person wife /\ ~(husband = wife) /\ says husband (statement_by husband) /\ 1323(~a_truth (statement_by husband) \/ ~knight husband \/ knight wife) /\ 1324(a_truth (statement_by husband) \/ ~knight husband) /\ 1325(a_truth (statement_by husband) \/ knight wife) /\ 1326(~knight wife \/ a_truth (statement_by husband)) ==> ~knight husband ==> F`}, 1327 1328{name = "ROB002-1", 1329 comments = [], 1330 goal = ` 1331(!x. x = x) /\ (!x y. ~(x = y) \/ y = x) /\ 1332(!x y z. ~(x = y) \/ ~(y = z) \/ x = z) /\ (!x y. x + y = y + x) /\ 1333(!x y z. x + y + z = x + (y + z)) /\ 1334(!x y. negate (negate (x + y) + negate (x + negate y)) = x) /\ 1335(!x y z. ~(x = y) \/ x + z = y + z) /\ 1336(!x y z. ~(x = y) \/ z + x = z + y) /\ 1337(!x y. ~(x = y) \/ negate x = negate y) /\ (!x. negate (negate x) = x) ==> 1338~(negate (a + negate b) + negate (negate a + negate b) = b) ==> F`} 1339 1340] @ 1341 1342(* ========================================================================= *) 1343(* Some problems from HOL. *) 1344(* ========================================================================= *) 1345 1346mkProblems "hol" "HOL subgoals sent to MESON_TAC" [ 1347 1348{name = "Coder_4_0", 1349 comments = [], 1350 goal = ` 1351(!x y. 1352 x = y \/ ~{x . (EXT_POINT . x . y)} \/ ~{y . (EXT_POINT . x . y)}) /\ 1353(!x y. x = y \/ {x . (EXT_POINT . x . y)} \/ {y . (EXT_POINT . x . y)}) /\ 1354(!x y. x = y \/ ~(x . (EXT_POINT . x . y) = y . (EXT_POINT . x . y))) /\ 1355(!x y. ~{x} \/ ~(x = y) \/ {y}) /\ ~{existential . (K . falsity)} /\ 1356{existential . (K . truth)} /\ ~{universal . (K . falsity)} /\ 1357{universal . (K . truth)} /\ ~{falsity} /\ {truth} /\ 1358(!x y z. ~(APPEND . x . y = APPEND . z . y) \/ x = z) /\ 1359(!x y z. ~(APPEND . x . y = APPEND . x . z) \/ y = z) ==> 1360{wf_encoder . p . e} /\ (!x. e . x = f . x \/ ~{p . x}) /\ 1361{wf_encoder . p . f} /\ {p . q} /\ {p . q'} /\ 1362APPEND . (f . q) . r = APPEND . (f . q') . r' /\ q = q' /\ ~(r' = r) ==> F`}, 1363 1364{name = "DeepSyntax_47", 1365 comments = [], 1366 goal = ` 1367(!x y z v. ~(x = y) \/ ~(z = v) \/ int_add x z = int_add y v) /\ 1368(!x y. ~(x = y) \/ int_neg x = int_neg y) /\ 1369(!x y. ~(x = y) \/ int_of_num x = int_of_num y) /\ 1370(!x y z v. ~(x = y) \/ ~(z = v) \/ int_lt y v \/ ~int_lt x z) /\ 1371(!x y z v. ~(x = y) \/ ~(z = v) \/ eval_form y v \/ ~eval_form x z) /\ 1372(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1373(!x y z v. 1374 int_lt (int_add x y) (int_add z v) \/ ~int_lt x z \/ ~int_lt y v) /\ 1375(!x. int_add x (int_of_num 0) = x) /\ 1376(!x. int_add x (int_neg x) = int_of_num 0) /\ 1377(!x y z. int_add x (int_add y z) = int_add (int_add x y) z) ==> 1378int_lt (int_neg d) (int_of_num 0) /\ eval_form g x /\ 1379int_lt (int_add x d) i /\ ~int_lt x i ==> F`}, 1380 1381{name = "divides_9", 1382 comments = [], 1383 goal = ` 1384(!x y z v. ~(x = y) \/ ~(z = v) \/ x * z = y * v) /\ 1385(!x y z v. ~(x = y) \/ ~(z = v) \/ divides y v \/ ~divides x z) /\ 1386(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1387(!x y z. x * (y * z) = x * y * z) /\ (!x y. x * y = y * x) /\ 1388(!x y. ~divides x y \/ y = gv1556 x y * x) /\ 1389(!x y z. divides x y \/ ~(y = z * x)) ==> 1390divides gv1546 gv1547 /\ ~divides gv1546 (gv1547 * gv1548) ==> F`}, 1391 1392{name = "Encode_28", 1393 comments = [], 1394 goal = ` 1395(!x y z v. ~(x = y) \/ ~(z = v) \/ MOD x z = MOD y v) /\ 1396(!x y z v. ~(x = y) \/ ~(z = v) \/ x * z = y * v) /\ 1397(!x y z v. ~(x = y) \/ ~(z = v) \/ x + z = y + v) /\ 1398(!x y. ~(x = y) \/ NUMERAL x = NUMERAL y) /\ 1399(!x y. ~(x = y) \/ BIT2 x = BIT2 y) /\ 1400(!x y z v. ~(x = y) \/ ~(z = v) \/ EXP x z = EXP y v) /\ 1401(!x y z v. ~(x = y) \/ ~(z = v) \/ DIV x z = DIV y v) /\ 1402(!x y. ~(x = y) \/ BIT1 x = BIT1 y) /\ 1403(!x y z v. ~(x = y) \/ ~(z = v) \/ y < v \/ ~(x < z)) /\ 1404(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1405(!x y. x * y = y * x) /\ 1406(!x y z. MOD (MOD x (y * z)) y = MOD x y \/ ~(0 < y) \/ ~(0 < z)) ==> 1407(!x. 1408 MOD x (NUMERAL (BIT2 ZERO)) = 0 \/ 1409 MOD x (NUMERAL (BIT2 ZERO)) = NUMERAL (BIT1 ZERO)) /\ 1410MOD 1411 (DIV x (NUMERAL (BIT2 ZERO)) * NUMERAL (BIT2 ZERO) + 1412 MOD x (NUMERAL (BIT2 ZERO))) 1413 (NUMERAL (BIT2 ZERO) * EXP (NUMERAL (BIT2 ZERO)) m) = 1414MOD 1415 (DIV y (NUMERAL (BIT2 ZERO)) * NUMERAL (BIT2 ZERO) + 1416 MOD y (NUMERAL (BIT2 ZERO))) 1417 (NUMERAL (BIT2 ZERO) * EXP (NUMERAL (BIT2 ZERO)) m) /\ 14180 < EXP (NUMERAL (BIT2 ZERO)) m /\ 0 < NUMERAL (BIT2 ZERO) /\ 1419(!x y. 1420 ~(MOD (x * NUMERAL (BIT2 ZERO) + MOD (x) (NUMERAL (BIT2 ZERO))) 1421 (NUMERAL (BIT2 ZERO)) = 1422 MOD (y * NUMERAL (BIT2 ZERO) + MOD (y) (NUMERAL (BIT2 ZERO))) 1423 (NUMERAL (BIT2 ZERO)))) ==> F`}, 1424 1425{name = "euclid_4", 1426 comments = [], 1427 goal = ` 1428(!x y z v. ~(x = y) \/ ~(z = v) \/ x * z = y * v) /\ 1429(!x y z v. ~(x = y) \/ ~(z = v) \/ divides y v \/ ~divides x z) /\ 1430(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1431(!x y z. x * (y * z) = x * y * z) /\ 1432(!x y. ~divides x y \/ y = x * gv5371 x y) /\ 1433(!x y z. divides x y \/ ~(y = x * z)) ==> 1434divides gv5316 gv5317 /\ divides gv5315 gv5316 /\ 1435~divides gv5315 gv5317 ==> F`}, 1436 1437{name = "euclid_8", 1438 comments = [], 1439 goal = ` 1440(!x y z v. ~(x = y) \/ ~(z = v) \/ x * z = y * v) /\ 1441(!x y z v. ~(x = y) \/ ~(z = v) \/ divides y v \/ ~divides x z) /\ 1442(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1443(!x y. x * y = y * x) /\ (!x y z. x * (y * z) = x * y * z) /\ 1444(!x y. ~divides x y \/ y = x * gv7050 x y) /\ 1445(!x y z. divides x y \/ ~(y = x * z)) ==> 1446divides gv7000 gv7001 /\ ~divides gv7000 (gv7002 * gv7001) ==> F`}, 1447 1448{name = "extra_arith_6", 1449 comments = [], 1450 goal = ` 1451(!x y z v. ~(x = y) \/ ~(z = v) \/ x * z = y * v) /\ 1452(!x y. ~(x = y) \/ SUC x = SUC y) /\ 1453(!x y z v. ~(x = y) \/ ~(z = v) \/ y < v \/ ~(x < z)) /\ 1454(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1455(!x y z. ~(SUC x * y = SUC x * z) \/ y = z) /\ 1456(!x y z. SUC x * y = SUC x * z \/ ~(y = z)) /\ 1457(!x y z. x * (y * z) = x * y * z) /\ (!x y. x * y = y * x) ==> 1458SUC n * b = q * (SUC n * a) /\ 0 < SUC n /\ ~(b = q * a) ==> F`}, 1459 1460{name = "extra_real_5", 1461 comments = [], 1462 goal = ` 1463~{existential . (K . falsity)} /\ {existential . (K . truth)} /\ 1464~{universal . (K . falsity)} /\ {universal . (K . truth)} /\ ~{falsity} /\ 1465{truth} ==> 1466(!x y z v. 1467 {real_lt . x . (sup . P)} \/ ~{P . y} \/ ~{real_lt . x . y} \/ 1468 ~{P . z} \/ ~{real_lte . (gv6327 . v) . v}) /\ 1469(!x y z. 1470 ~{real_lt . x . (sup . P)} \/ {P . (gv6327 . x)} \/ ~{P . y} \/ 1471 ~{real_lte . (gv6327 . z) . z}) /\ 1472(!x y z. 1473 ~{real_lt . x . (sup . P)} \/ {real_lt . x . (gv6327 . x)} \/ 1474 ~{P . y} \/ ~{real_lte . (gv6327 . z) . z}) /\ 1475(!x y z. 1476 ~{real_lt . x . (sup . P)} \/ {real_lt . x . (gv6327 . x)} \/ 1477 ~{P . y} \/ {P . (gv6327 . z)}) /\ 1478(!x y z. 1479 ~{real_lt . x . (sup . P)} \/ {P . (gv6327 . x)} \/ ~{P . y} \/ 1480 {P . (gv6327 . z)}) /\ 1481(!x y z v. 1482 {real_lt . x . (sup . P)} \/ ~{P . y} \/ ~{real_lt . x . y} \/ 1483 ~{P . z} \/ {P . (gv6327 . v)}) /\ {P . x} /\ 1484(!x. {real_lte . x . z} \/ ~{P . x}) /\ 1485(!x. 1486 {real_lt . (gv6328 . x) . (gv6329 . x)} \/ 1487 {real_lt . (gv6328 . x) . x}) /\ 1488(!x. {P . (gv6329 . x)} \/ {real_lt . (gv6328 . x) . x}) /\ 1489(!x y. 1490 ~{real_lt . (gv6328 . x) . y} \/ ~{P . y} \/ 1491 ~{real_lt . (gv6328 . x) . x}) ==> F`}, 1492 1493{name = "gcd_19", 1494 comments = [], 1495 goal = ` 1496(!x y z v. ~(x = y) \/ ~(z = v) \/ x + z = y + v) /\ 1497(!x y z v. ~(x = y) \/ ~(z = v) \/ x * z = y * v) /\ 1498(!x y. ~(x = y) \/ NUMERAL x = NUMERAL y) /\ 1499(!x y. ~(x = y) \/ BIT1 x = BIT1 y) /\ (!x y. ~(x = y) \/ SUC x = SUC y) /\ 1500(!x y z v. ~(x = y) \/ ~(z = v) \/ y <= v \/ ~(x <= z)) /\ 1501(!x y z v. ~(x = y) \/ ~(z = v) \/ divides y v \/ ~divides x z) /\ 1502(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1503(!x y z. x * (y + z) = x * y + x * z) /\ (!x y. x + SUC y = SUC (x + y)) /\ 1504(!x y. SUC x + y = SUC (x + y)) /\ (!x. x + 0 = x) /\ (!x. 0 + x = x) /\ 1505(!x y. x * SUC y = x + x * y) /\ (!x y. SUC x * y = x * y + y) /\ 1506(!x. x * NUMERAL (BIT1 ZERO) = x) /\ (!x. NUMERAL (BIT1 ZERO) * x = x) /\ 1507(!x. x * 0 = 0) /\ (!x. 0 * x = 0) /\ (!x y z. x + (y + z) = x + y + z) /\ 1508(!x y z. divides x y \/ ~divides x z \/ ~divides x (z + y)) ==> 1509~(x + z <= x) /\ divides c (d * SUC x) /\ divides c (d * SUC (x + z)) /\ 1510~divides c (d * z) ==> F`}, 1511 1512{name = "gcd_20", 1513 comments = [], 1514 goal = ` 1515(!x y z v. ~(x = y) \/ ~(z = v) \/ x + z = y + v) /\ 1516(!x y z v. ~(x = y) \/ ~(z = v) \/ x * z = y * v) /\ 1517(!x y. ~(x = y) \/ NUMERAL x = NUMERAL y) /\ 1518(!x y. ~(x = y) \/ BIT1 x = BIT1 y) /\ (!x y. ~(x = y) \/ SUC x = SUC y) /\ 1519(!x y z v. ~(x = y) \/ ~(z = v) \/ y <= v \/ ~(x <= z)) /\ 1520(!x y z v. ~(x = y) \/ ~(z = v) \/ divides y v \/ ~divides x z) /\ 1521(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1522(!x y z. x * (y + z) = x * y + x * z) /\ (!x y. x + SUC y = SUC (x + y)) /\ 1523(!x y. SUC x + y = SUC (x + y)) /\ (!x. x + 0 = x) /\ (!x. 0 + x = x) /\ 1524(!x y. x * SUC y = x + x * y) /\ (!x y. SUC x * y = x * y + y) /\ 1525(!x. x * NUMERAL (BIT1 ZERO) = x) /\ (!x. NUMERAL (BIT1 ZERO) * x = x) /\ 1526(!x. x * 0 = 0) /\ (!x. 0 * x = 0) /\ (!x y z. x + (y + z) = x + y + z) /\ 1527(!x y z. divides x y \/ ~divides x z \/ ~divides x (z + y)) ==> 1528y <= y + z /\ divides c (d * SUC (y + z)) /\ divides c (d * SUC y) /\ 1529~divides c (d * z) ==> F`}, 1530 1531{name = "gcd_21", 1532 comments = [], 1533 goal = ` 1534(!x y z v. ~(x = y) \/ ~(z = v) \/ x + z = y + v) /\ 1535(!x y z v. ~(x = y) \/ ~(z = v) \/ x * z = y * v) /\ 1536(!x y. ~(x = y) \/ NUMERAL x = NUMERAL y) /\ 1537(!x y. ~(x = y) \/ BIT1 x = BIT1 y) /\ (!x y. ~(x = y) \/ SUC x = SUC y) /\ 1538(!x y z v. ~(x = y) \/ ~(z = v) \/ divides y v \/ ~divides x z) /\ 1539(!x y z v. ~(x = y) \/ ~(z = v) \/ y <= v \/ ~(x <= z)) /\ 1540(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1541(!x y z. x * (y + z) = x * y + x * z) /\ (!x y. x + SUC y = SUC (x + y)) /\ 1542(!x y. SUC x + y = SUC (x + y)) /\ (!x. x + 0 = x) /\ (!x. 0 + x = x) /\ 1543(!x y. x * SUC y = x + x * y) /\ (!x y. SUC x * y = x * y + y) /\ 1544(!x. x * NUMERAL (BIT1 ZERO) = x) /\ (!x. NUMERAL (BIT1 ZERO) * x = x) /\ 1545(!x. x * 0 = 0) /\ (!x. 0 * x = 0) /\ (!x y z. x + (y + z) = x + y + z) /\ 1546(!x y z. divides x y \/ ~divides x z \/ ~divides x (z + y)) ==> 1547divides c (d * SUC y) /\ y <= y + z /\ divides c (d * SUC (y + z)) /\ 1548~divides c (d * z) ==> F`}, 1549 1550{name = "int_arith_6", 1551 comments = [], 1552 goal = ` 1553(!x y z v. ~(x = y) \/ ~(z = v) \/ int_mul x z = int_mul y v) /\ 1554(!x y. ~(x = y) \/ int_of_num x = int_of_num y) /\ 1555(!x y z v. ~(x = y) \/ ~(z = v) \/ int_lt y v \/ ~int_lt x z) /\ 1556(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1557(!x y. int_mul x y = int_mul y x) /\ (!x. ~int_lt x x) /\ 1558(!x y z. ~(int_mul x y = int_mul z y) \/ y = int_of_num 0 \/ x = z) /\ 1559(!x y z. int_mul x y = int_mul z y \/ ~(y = int_of_num 0)) /\ 1560(!x y z. int_mul x y = int_mul z y \/ ~(x = z)) ==> 1561int_lt (int_of_num 0) gv1085 /\ 1562int_mul gv1085 gv1086 = int_mul gv1085 gv1087 /\ ~(gv1086 = gv1087) ==> F`}, 1563 1564{name = "int_arith_139", 1565 comments = [], 1566 goal = ` 1567(!x y z v. ~(x = y) \/ ~(z = v) \/ int_add x z = int_add y v) /\ 1568(!x y. ~(x = y) \/ int_of_num x = int_of_num y) /\ 1569(!x y z v. ~(x = y) \/ ~(z = v) \/ int_le y v \/ ~int_le x z) /\ 1570(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1571(!x. int_add (int_of_num 0) x = x) /\ 1572(!x y z v. 1573 int_le (int_add x y) (int_add z v) \/ ~int_le x z \/ ~int_le y v) /\ 1574(!x y z. int_add x (int_add y z) = int_add (int_add x y) z) /\ 1575(!x y. int_add x y = int_add y x) /\ 1576(!x y z. ~int_le (int_add x y) (int_add x z) \/ int_le y z) /\ 1577(!x y z. int_le (int_add x y) (int_add x z) \/ ~int_le y z) ==> 1578int_le x y /\ int_le (int_of_num 0) (int_add c x) /\ 1579~int_le (int_of_num 0) (int_add c y) ==> F`}, 1580 1581{name = "llist_69", 1582 comments = [], 1583 goal = ` 1584(!x y. ~(x = y) \/ LTL x = LTL y) /\ (!x y. ~(x = y) \/ SOME x = SOME y) /\ 1585(!x y. ~(x = y) \/ LHD x = LHD y) /\ 1586(!x y z v. ~(x = y) \/ ~(z = v) \/ LCONS x z = LCONS y v) /\ 1587(!x y. ~(x = y) \/ g x = g y) /\ (!x y. ~(x = y) \/ THE x = THE y) /\ 1588(!x y z v. ~(x = y) \/ ~(z = v) \/ LNTH z x = LNTH v y) /\ 1589(!x y z v. ~(x = y) \/ ~(z = v) \/ LDROP z x = LDROP v y) /\ 1590(!x y. ~(x = y) \/ SUC x = SUC y) /\ 1591(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1592(!x y z. ~(x = LCONS y z) \/ LTL x = SOME z) /\ 1593(!x y z. ~(x = LCONS y z) \/ LHD x = SOME y) /\ 1594(!x y z. x = LCONS y z \/ ~(LHD x = SOME y) \/ ~(LTL x = SOME z)) ==> 1595LTL (g (LCONS LNIL t)) = 1596SOME (g (LCONS (THE (LTL (THE (LNTH n t)))) (THE (LDROP (SUC n) t)))) /\ 1597LHD (g (LCONS LNIL t)) = SOME (THE (LHD (THE (LNTH n t)))) /\ 1598LHD (g t) = SOME (THE (LHD (THE (LNTH n t)))) /\ 1599LTL (g t) = 1600SOME (g (LCONS (THE (LTL (THE (LNTH n t)))) (THE (LDROP (SUC n) t)))) /\ 1601~(g (LCONS LNIL t) = g t) ==> F`}, 1602 1603{name = "MachineTransition_0", 1604 comments = [], 1605 goal = ` 1606(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1607(!x y. 1608 x = y \/ ~{x . (EXT_POINT . x . y)} \/ ~{y . (EXT_POINT . x . y)}) /\ 1609(!x y. x = y \/ {x . (EXT_POINT . x . y)} \/ {y . (EXT_POINT . x . y)}) /\ 1610(!x y. x = y \/ ~(x . (EXT_POINT . x . y) = y . (EXT_POINT . x . y))) /\ 1611(!x y. ~{x} \/ ~(x = y) \/ {y}) /\ 1612(!x y z v. ~(x = y) \/ ~(z = v) \/ x . z = y . v) /\ 1613~{existential . (K . falsity)} /\ {existential . (K . truth)} /\ 1614~{universal . (K . falsity)} /\ {universal . (K . truth)} /\ ~{falsity} /\ 1615{truth} /\ Eq = equality /\ 1616(!x y z. ~{Next . x . y . z} \/ {x . (pair . (gv940 . x . y . z) . z)}) /\ 1617(!x y z. ~{Next . x . y . z} \/ {y . (gv940 . x . y . z)}) /\ 1618(!x y z v. {Next . x . y . z} \/ ~{y . v} \/ ~{x . (pair . v . z)}) /\ 1619(!x y z. ~{Prev . x . y . z} \/ {y . (gv935 . x . y . z)}) /\ 1620(!x y z. ~{Prev . x . y . z} \/ {x . (pair . z . (gv935 . x . y . z))}) /\ 1621(!x y z v. {Prev . x . y . z} \/ ~{x . (pair . z . v)} \/ ~{y . v}) ==> 1622{Next . gv914 . (Eq . gv915) . gv916} /\ 1623~{Prev . gv914 . (Eq . gv916) . gv915} ==> F`}, 1624 1625{name = "MachineTransition_2_1", 1626 comments = [], 1627 goal = ` 1628(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1629(!x y. 1630 x = y \/ ~{x . (EXT_POINT . x . y)} \/ ~{y . (EXT_POINT . x . y)}) /\ 1631(!x y. x = y \/ {x . (EXT_POINT . x . y)} \/ {y . (EXT_POINT . x . y)}) /\ 1632(!x y. x = y \/ ~(x . (EXT_POINT . x . y) = y . (EXT_POINT . x . y))) /\ 1633(!x y. ~{x} \/ ~(x = y) \/ {y}) /\ 1634(!x y z v. ~(x = y) \/ ~(z = v) \/ x . z = y . v) /\ 1635~{existential . (K . falsity)} /\ {existential . (K . truth)} /\ 1636~{universal . (K . falsity)} /\ {universal . (K . truth)} /\ ~{falsity} /\ 1637{truth} /\ 1638(!x y z. ReachIn . x . (Next . x . y) . z = ReachIn . x . y . (SUC . z)) /\ 1639(!x y z. ~{Next . x . y . z} \/ {x . (pair . (gv5488 . x . y . z) . z)}) /\ 1640(!x y z. ~{Next . x . y . z} \/ {y . (gv5488 . x . y . z)}) /\ 1641(!x y z v. {Next . x . y . z} \/ ~{y . v} \/ ~{x . (pair . v . z)}) /\ 1642(!x y z. ReachIn . x . y . (SUC . z) = Next . x . (ReachIn . x . y . z)) /\ 1643(!x y. ReachIn . x . y . 0 = y) ==> 1644{ReachIn . R . (Next . R . B) . gv5278 . state} /\ 1645(!x. ~{ReachIn . R . B . gv5278 . x} \/ ~{R . (pair . x . state)}) ==> F`}, 1646 1647{name = "MachineTransition_52", 1648 comments = [], 1649 goal = ` 1650(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1651(!x y. 1652 x = y \/ ~{x . (EXT_POINT . x . y)} \/ ~{y . (EXT_POINT . x . y)}) /\ 1653(!x y. x = y \/ {x . (EXT_POINT . x . y)} \/ {y . (EXT_POINT . x . y)}) /\ 1654(!x y. x = y \/ ~(x . (EXT_POINT . x . y) = y . (EXT_POINT . x . y))) /\ 1655(!x y. ~{x} \/ ~(x = y) \/ {y}) /\ 1656(!x y z v. ~(x = y) \/ ~(z = v) \/ x . z = y . v) /\ 1657~{existential . (K . falsity)} /\ {existential . (K . truth)} /\ 1658~{universal . (K . falsity)} /\ {universal . (K . truth)} /\ ~{falsity} /\ 1659{truth} /\ 1660(!x y z. 1661 {(<=) . (gv7028 . x . y . z) . (add . x . (NUMERAL . (BIT1 . ZERO)))} \/ 1662 z . (add . x . (NUMERAL . (BIT1 . ZERO))) = 1663 y . (add . x . (NUMERAL . (BIT1 . ZERO)))) /\ 1664(!x y z. 1665 ~(x . (gv7028 . y . z . x) = z . (gv7028 . y . z . x)) \/ 1666 x . (add . y . (NUMERAL . (BIT1 . ZERO))) = 1667 z . (add . y . (NUMERAL . (BIT1 . ZERO)))) /\ 1668(!x y z v. 1669 ~(x . (gv7028 . y . z . x) = z . (gv7028 . y . z . x)) \/ 1670 x . v = z . v \/ ~{(<=) . v . y}) /\ 1671(!x y z v. 1672 {(<=) . (gv7028 . x . y . z) . (add . x . (NUMERAL . (BIT1 . ZERO)))} \/ 1673 z . v = y . v \/ ~{(<=) . v . x}) /\ 1674(!x y z v. 1675 ~{(<=) . x . (add . y . (NUMERAL . (BIT1 . ZERO)))} \/ z . x = v . x \/ 1676 ~(z . (gv7027 . y . v . z) = v . (gv7027 . y . v . z)) \/ 1677 ~(z . (add . y . (NUMERAL . (BIT1 . ZERO))) = 1678 v . (add . y . (NUMERAL . (BIT1 . ZERO))))) /\ 1679(!x y z v. 1680 ~{(<=) . x . (add . y . (NUMERAL . (BIT1 . ZERO)))} \/ z . x = v . x \/ 1681 {(<=) . (gv7027 . y . v . z) . y} \/ 1682 ~(z . (add . y . (NUMERAL . (BIT1 . ZERO))) = 1683 v . (add . y . (NUMERAL . (BIT1 . ZERO))))) ==> 1684({FinPath . (pair . R . s) . f2 . n} \/ 1685 ~{FinPath . (pair . R . s) . f1 . n} \/ ~(f1 . gv7034 = f2 . gv7034)) /\ 1686(~{FinPath . (pair . R . s) . f2 . n} \/ 1687 {FinPath . (pair . R . s) . f1 . n} \/ ~(f1 . gv7034 = f2 . gv7034)) /\ 1688(~{FinPath . (pair . R . s) . f2 . n} \/ 1689 {FinPath . (pair . R . s) . f1 . n} \/ {(<=) . gv7034 . n}) /\ 1690({FinPath . (pair . R . s) . f2 . n} \/ 1691 ~{FinPath . (pair . R . s) . f1 . n} \/ {(<=) . gv7034 . n}) /\ 1692(!x. 1693 f1 . x = f2 . x \/ 1694 ~{(<=) . x . (add . n . (NUMERAL . (BIT1 . ZERO)))}) /\ 1695{FinPath . (pair . R . s) . f2 . n} /\ 1696{R . (pair . (f2 . n) . (f2 . (add . n . (NUMERAL . (BIT1 . ZERO)))))} /\ 1697~{FinPath . (pair . R . s) . f1 . n} ==> F`}, 1698 1699{name = "measure_138", 1700 comments = [], 1701 goal = ` 1702(!x y z. ~SUBSET x y \/ IN z y \/ ~IN z x) /\ 1703(!x y. SUBSET x y \/ IN (gv122874 x y) x) /\ 1704(!x y. SUBSET x y \/ ~IN (gv122874 x y) y) /\ 1705(!x. sigma_algebra (sigma x)) /\ (!x y z. ~IN x (INTER y z) \/ IN x z) /\ 1706(!x y z. ~IN x (INTER y z) \/ IN x y) /\ 1707(!x y z. IN x (INTER y z) \/ ~IN x y \/ ~IN x z) /\ 1708(!x y. 1709 ~sigma_algebra x \/ IN (BIGUNION y) x \/ ~countable y \/ ~SUBSET y x) /\ 1710(!x y. ~sigma_algebra x \/ IN (COMPL y) x \/ ~IN y x) /\ 1711(!x. ~sigma_algebra x \/ IN EMPTY x) /\ 1712(!x. 1713 sigma_algebra x \/ ~IN EMPTY x \/ ~IN (COMPL (gv122851 x)) x \/ 1714 SUBSET (gv122852 x) x) /\ 1715(!x. 1716 sigma_algebra x \/ ~IN EMPTY x \/ IN (gv122851 x) x \/ 1717 SUBSET (gv122852 x) x) /\ 1718(!x. 1719 sigma_algebra x \/ ~IN EMPTY x \/ IN (gv122851 x) x \/ 1720 countable (gv122852 x)) /\ 1721(!x. 1722 sigma_algebra x \/ ~IN EMPTY x \/ ~IN (COMPL (gv122851 x)) x \/ 1723 countable (gv122852 x)) /\ 1724(!x. 1725 sigma_algebra x \/ ~IN EMPTY x \/ IN (gv122851 x) x \/ 1726 ~IN (BIGUNION (gv122852 x)) x) /\ 1727(!x. 1728 sigma_algebra x \/ ~IN EMPTY x \/ ~IN (COMPL (gv122851 x)) x \/ 1729 ~IN (BIGUNION (gv122852 x)) x) ==> 1730SUBSET c (INTER p (sigma a)) /\ 1731(!x. IN (BIGUNION x) p \/ ~countable x \/ ~SUBSET x (INTER p (sigma a))) /\ 1732SUBSET a p /\ IN EMPTY p /\ 1733(!x. IN (COMPL x) p \/ ~IN x (INTER p (sigma a))) /\ countable c /\ 1734~IN (BIGUNION c) (sigma a) ==> F`}, 1735 1736{name = "Omega_13", 1737 comments = [], 1738 goal = ` 1739(!x y z v. ~(x = y) \/ ~(z = v) \/ int_mul x z = int_mul y v) /\ 1740(!x y. ~(x = y) \/ int_of_num x = int_of_num y) /\ 1741(!x y z v. ~(x = y) \/ ~(z = v) \/ evalupper y v \/ ~evalupper x z) /\ 1742(!x y z v. ~(x = y) \/ ~(z = v) \/ int_lt y v \/ ~int_lt x z) /\ 1743(!x y z v. ~(x = y) \/ ~(z = v) \/ int_le y v \/ ~int_le x z) /\ 1744(!x y z v. ~(x = y) \/ ~(z = v) \/ y < v \/ ~(x < z)) /\ 1745(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1746(!x y. ~int_le x y \/ int_lt x y \/ x = y) /\ 1747(!x y. int_le x y \/ ~int_lt x y) /\ (!x y. int_le x y \/ ~(x = y)) /\ 1748(!x y z. 1749 int_lt x y \/ 1750 ~int_lt (int_mul (int_of_num z) x) (int_mul (int_of_num z) y) \/ 1751 ~(0 < z)) /\ 1752(!x y z. 1753 ~int_lt x y \/ 1754 int_lt (int_mul (int_of_num z) x) (int_mul (int_of_num z) y) \/ 1755 ~(0 < z)) /\ (!x y z. int_lt x y \/ ~int_le x z \/ ~int_lt z y) ==> 1756(!x y. evalupper x uppers \/ ~evalupper y uppers \/ ~int_lt x y) /\ 1757int_le (int_mul (int_of_num p_1) x) p_2 /\ evalupper x uppers /\ 1758int_lt y x /\ 0 < p_1 /\ ~int_le (int_mul (int_of_num p_1) y) p_2 ==> F`}, 1759 1760{name = "Omega_71", 1761 comments = [], 1762 goal = ` 1763(!x y z v. ~(x = y) \/ ~(z = v) \/ int_mul x z = int_mul y v) /\ 1764(!x y. ~(x = y) \/ int_of_num x = int_of_num y) /\ 1765(!x y z v. ~(x = y) \/ ~(z = v) \/ x * z = y * v) /\ 1766(!x y z v. ~(x = y) \/ ~(z = v) \/ int_add x z = int_add y v) /\ 1767(!x y. ~(x = y) \/ NUMERAL x = NUMERAL y) /\ 1768(!x y. ~(x = y) \/ BIT1 x = BIT1 y) /\ 1769(!x y z v. ~(x = y) \/ ~(z = v) \/ (x, z) = (y, v)) /\ 1770(!x y z v. ~(x = y) \/ ~(z = v) \/ evallower y v \/ ~evallower x z) /\ 1771(!x y z v. ~(x = y) \/ ~(z = v) \/ y < v \/ ~(x < z)) /\ 1772(!x y z v. ~(x = y) \/ ~(z = v) \/ rshadow_row v y \/ ~rshadow_row z x) /\ 1773(!x y z v. 1774 ~(x = y) \/ ~(z = v) \/ dark_shadow_cond_row v y \/ 1775 ~dark_shadow_cond_row z x) /\ 1776(!x y z v. ~(x = y) \/ ~(z = v) \/ int_le y v \/ ~int_le x z) /\ 1777(!x y z v. ~(x = y) \/ ~(z = v) \/ EVERY y v \/ ~EVERY x z) /\ 1778(!x y z v. ~(x = y) \/ ~(z = v) \/ int_lt y v \/ ~int_lt x z) /\ 1779(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1780(!x y. int_mul x y = int_mul y x) /\ 1781(!x y z. int_mul x (int_mul y z) = int_mul (int_mul x y) z) /\ 1782(!x y z. 1783 int_le x y \/ 1784 ~int_le (int_mul (int_of_num z) x) (int_mul (int_of_num z) y) \/ 1785 ~(0 < z)) /\ 1786(!x y z. 1787 ~int_le x y \/ 1788 int_le (int_mul (int_of_num z) x) (int_mul (int_of_num z) y) \/ 1789 ~(0 < z)) ==> 1790(!x y z. 1791 evallower (gv6249 x y z) lowers \/ ~(0 < y) \/ ~evallower x lowers \/ 1792 ~rshadow_row (y, z) lowers \/ ~dark_shadow_cond_row (y, z) lowers) /\ 1793(!x y z. 1794 int_le (int_mul (int_of_num x) (gv6249 y x z)) z \/ ~(0 < x) \/ 1795 ~evallower y lowers \/ ~rshadow_row (x, z) lowers \/ 1796 ~dark_shadow_cond_row (x, z) lowers) /\ 0 < c /\ 1797int_le R (int_mul (int_of_num d) x) /\ evallower x lowers /\ 0 < d /\ 1798EVERY fst_nzero lowers /\ 1799int_le (int_mul (int_of_num c) R) (int_mul (int_of_num d) L) /\ 1800rshadow_row (c, L) lowers /\ dark_shadow_cond_row (c, L) lowers /\ 1801(!x. 1802 ~int_lt (int_mul (int_of_num d) L) 1803 (int_mul (int_of_num (c * d)) 1804 (int_add x (int_of_num (NUMERAL (BIT1 ZERO))))) \/ 1805 ~int_lt (int_mul (int_of_num (c * d)) x) (int_mul (int_of_num c) R)) /\ 1806int_le (int_mul (int_of_num c) y) L /\ evallower y lowers /\ 1807int_le (int_mul (int_of_num (c * d)) y) (int_mul (int_of_num d) L) /\ 1808int_le (int_mul (int_of_num c) R) (int_mul (int_of_num (c * d)) x) /\ 1809int_lt (int_mul (int_of_num (c * d)) y) (int_mul (int_of_num c) R) /\ 18100 < c * d /\ 1811int_le (int_mul (int_of_num c) R) (int_mul (int_of_num (c * d)) j) /\ 1812int_le (int_mul (int_of_num (c * d)) j) (int_mul (int_of_num d) L) /\ 1813int_le (int_mul (int_mul (int_of_num c) (int_of_num d)) j) 1814 (int_mul (int_of_num d) L) /\ ~int_le (int_mul (int_of_num c) j) L ==> F`}, 1815 1816{name = "pred_set_1", 1817 comments = ["Small problem that's hard for ordered resolution"], 1818 goal = ` 1819(!x y z. ~(x <= y) \/ p z y \/ ~p z x) /\ (!x y. x <= y \/ ~p (a x y) y) /\ 1820(!x y. x <= y \/ p (a x y) x) /\ (!x y z. ~p x (y * z) \/ p x z) /\ 1821(!x y z. ~p x (y * z) \/ p x y) /\ 1822(!x y z. p x (y * z) \/ ~p x y \/ ~p x z) ==> 1823b <= c /\ b <= d /\ ~(b <= c * d) ==> F`}, 1824 1825{name = "pred_set_54_1", 1826 comments = [], 1827 goal = ` 1828(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1829(!x y. 1830 x = y \/ ~{x . (EXT_POINT . x . y)} \/ ~{y . (EXT_POINT . x . y)}) /\ 1831(!x y. x = y \/ {x . (EXT_POINT . x . y)} \/ {y . (EXT_POINT . x . y)}) /\ 1832(!x y. x = y \/ ~(x . (EXT_POINT . x . y) = y . (EXT_POINT . x . y))) /\ 1833(!x y. ~{x} \/ ~(x = y) \/ {y}) /\ 1834(!x y z v. ~(x = y) \/ ~(z = v) \/ x . z = y . v) /\ 1835~{existential . (K . falsity)} /\ {existential . (K . truth)} /\ 1836~{universal . (K . falsity)} /\ {universal . (K . truth)} /\ ~{falsity} /\ 1837{truth} /\ 1838(!x y z. ~{IN . x . (INSERT . y . z)} \/ x = y \/ {IN . x . z}) /\ 1839(!x y z. {IN . x . (INSERT . y . z)} \/ ~(x = y)) /\ 1840(!x y z. {IN . x . (INSERT . y . z)} \/ ~{IN . x . z}) ==> 1841(!x y z. f . x . (f . y . z) = f . y . (f . x . z)) /\ 1842(!x y z. 1843 ITSET . f . (INSERT . x . y) . z = 1844 ITSET . f . (DELETE . y . x) . (f . x . z) \/ 1845 ~{less_than . (CARD . y) . v} \/ ~{FINITE . y}) /\ v = CARD . s /\ 1846{FINITE . s} /\ REST . (INSERT . x . s) = t /\ 1847CHOICE . (INSERT . x . s) = y /\ ~{IN . y . t} /\ ~{IN . x . s} /\ 1848INSERT . x . s = INSERT . y . t /\ ~(x = y) /\ ~{IN . x . t} ==> F`}, 1849 1850{name = "prob_44", 1851 comments = [], 1852 goal = ` 1853(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1854(!x y. 1855 x = y \/ ~{x . (EXT_POINT . x . y)} \/ ~{y . (EXT_POINT . x . y)}) /\ 1856(!x y. x = y \/ {x . (EXT_POINT . x . y)} \/ {y . (EXT_POINT . x . y)}) /\ 1857(!x y. x = y \/ ~(x . (EXT_POINT . x . y) = y . (EXT_POINT . x . y))) /\ 1858(!x y. ~{x} \/ ~(x = y) \/ {y}) /\ 1859(!x y z v. ~(x = y) \/ ~(z = v) \/ x . z = y . v) /\ 1860~{existential . (K . falsity)} /\ {existential . (K . truth)} /\ 1861~{universal . (K . falsity)} /\ {universal . (K . truth)} /\ ~{falsity} /\ 1862{truth} ==> 1863(!x y z. 1864 ~{IN . x . (prefix_set . x')} \/ ~{IN . x . (prefix_set . (x))} \/ 1865 ~{IN . y . c} \/ ~{IN . (gv24939 . y) . (prefix_set . (x))} \/ 1866 ~{IN . (gv24939 . y) . (prefix_set . y)} \/ 1867 ~{IN . (gv24940 . z) . (prefix_set . z)} \/ 1868 ~{IN . (gv24940 . z) . (prefix_set . x')} \/ ~{IN . z . c}) /\ 1869(!x y z. 1870 ~{IN . x . (prefix_set . x')} \/ ~{IN . x . (prefix_set . (x))} \/ 1871 ~{IN . y . c} \/ {IN . (gv24939 . y) . (prefix_set . (x))} \/ 1872 {IN . (gv24939 . y) . (prefix_set . y)} \/ 1873 ~{IN . (gv24940 . z) . (prefix_set . z)} \/ 1874 ~{IN . (gv24940 . z) . (prefix_set . x')} \/ ~{IN . z . c}) /\ 1875(!x y z. 1876 ~{IN . x . (prefix_set . x')} \/ ~{IN . x . (prefix_set . (x))} \/ 1877 ~{IN . y . c} \/ {IN . (gv24939 . y) . (prefix_set . (x))} \/ 1878 {IN . (gv24939 . y) . (prefix_set . y)} \/ 1879 {IN . (gv24940 . z) . (prefix_set . z)} \/ 1880 {IN . (gv24940 . z) . (prefix_set . x')} \/ ~{IN . z . c}) /\ 1881(!x y z. 1882 ~{IN . x . (prefix_set . x')} \/ ~{IN . x . (prefix_set . (x))} \/ 1883 ~{IN . y . c} \/ ~{IN . (gv24939 . y) . (prefix_set . (x))} \/ 1884 ~{IN . (gv24939 . y) . (prefix_set . y)} \/ 1885 {IN . (gv24940 . z) . (prefix_set . z)} \/ 1886 {IN . (gv24940 . z) . (prefix_set . x')} \/ ~{IN . z . c}) /\ 1887{IN . x' . c} /\ 1888{IN . (PREIMAGE . ((o) . SND . f) . s) . (events . bern)} /\ 1889(!x y. 1890 f . x = 1891 pair . (FST . (f . (prefix_seq . y))) . (sdrop . (LENGTH . y) . x) \/ 1892 ~{IN . y . c} \/ ~{IN . x . (prefix_set . y)}) /\ 1893{IN . ((o) . SND . f) . 1894 (measurable . (events . bern) . (events . bern))} /\ 1895{countable . (range . ((o) . FST . f))} /\ 1896{IN . ((o) . FST . f) . (measurable . (events . bern) . UNIV)} /\ 1897{prefix_cover . c} /\ {IN . s . (events . bern)} /\ {IN . x . c} /\ 1898({IN . x'' . (prefix_set . x)} \/ {IN . x'' . (prefix_set . x')}) /\ 1899(~{IN . x'' . (prefix_set . x)} \/ ~{IN . x'' . (prefix_set . x')}) /\ 1900{IN . x''' . (prefix_set . x)} /\ {IN . x''' . (prefix_set . x')} ==> F`}, 1901 1902{name = "prob_53", 1903 comments = [], 1904 goal = ` 1905(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 1906(!x y. 1907 x = y \/ ~{x . (EXT_POINT . x . y)} \/ ~{y . (EXT_POINT . x . y)}) /\ 1908(!x y. x = y \/ {x . (EXT_POINT . x . y)} \/ {y . (EXT_POINT . x . y)}) /\ 1909(!x y. x = y \/ ~(x . (EXT_POINT . x . y) = y . (EXT_POINT . x . y))) /\ 1910(!x y. ~{x} \/ ~(x = y) \/ {y}) /\ 1911(!x y z v. ~(x = y) \/ ~(z = v) \/ x . z = y . v) /\ 1912~{existential . (K . falsity)} /\ {existential . (K . truth)} /\ 1913~{universal . (K . falsity)} /\ {universal . (K . truth)} /\ ~{falsity} /\ 1914{truth} ==> 1915(!x y z. 1916 ~{IN . x . (prefix_set . x''')} \/ ~{IN . x . (prefix_set . x'')} \/ 1917 ~{IN . y . c} \/ ~{IN . (gv39280 . y) . (prefix_set . x'')} \/ 1918 ~{IN . (gv39280 . y) . (prefix_set . y)} \/ 1919 ~{IN . (gv39280 . z) . (prefix_set . z)} \/ 1920 ~{IN . (gv39280 . z) . (prefix_set . x''')} \/ ~{IN . z . c}) /\ 1921(!x y z. 1922 ~{IN . x . (prefix_set . x''')} \/ ~{IN . x . (prefix_set . x'')} \/ 1923 ~{IN . y . c} \/ {IN . (gv39280 . y) . (prefix_set . x'')} \/ 1924 {IN . (gv39280 . y) . (prefix_set . y)} \/ 1925 ~{IN . (gv39280 . z) . (prefix_set . z)} \/ 1926 ~{IN . (gv39280 . z) . (prefix_set . x''')} \/ ~{IN . z . c}) /\ 1927(!x y z. 1928 ~{IN . x . (prefix_set . x''')} \/ ~{IN . x . (prefix_set . x'')} \/ 1929 ~{IN . y . c} \/ {IN . (gv39280 . y) . (prefix_set . x'')} \/ 1930 {IN . (gv39280 . y) . (prefix_set . y)} \/ 1931 {IN . (gv39280 . z) . (prefix_set . z)} \/ 1932 {IN . (gv39280 . z) . (prefix_set . x''')} \/ ~{IN . z . c}) /\ 1933(!x y z. 1934 ~{IN . x . (prefix_set . x''')} \/ ~{IN . x . (prefix_set . x'')} \/ 1935 ~{IN . y . c} \/ ~{IN . (gv39280 . y) . (prefix_set . x'')} \/ 1936 ~{IN . (gv39280 . y) . (prefix_set . y)} \/ 1937 {IN . (gv39280 . z) . (prefix_set . z)} \/ 1938 {IN . (gv39280 . z) . (prefix_set . x''')} \/ ~{IN . z . c}) /\ 1939{IN . x''' . c} /\ 1940{IN . (PREIMAGE . ((o) . SND . f) . x') . (events . bern)} /\ 1941{IN . x' . (events . bern)} /\ {prefix_cover . c} /\ 1942{IN . ((o) . FST . f) . (measurable . (events . bern) . UNIV)} /\ 1943{countable . (range . ((o) . FST . f))} /\ 1944{IN . ((o) . SND . f) . 1945 (measurable . (events . bern) . (events . bern))} /\ 1946(!x y. 1947 f . x = 1948 pair . (FST . (f . (prefix_seq . y))) . (sdrop . (LENGTH . y) . x) \/ 1949 ~{IN . y . c} \/ ~{IN . x . (prefix_set . y)}) /\ 1950{IN . (PREIMAGE . ((o) . FST . f) . x) . (events . bern)} /\ 1951{IN . x'' . c} /\ 1952({IN . x'''' . (prefix_set . x'')} \/ 1953 {IN . x'''' . (prefix_set . x''')}) /\ 1954(~{IN . x'''' . (prefix_set . x'')} \/ 1955 ~{IN . x'''' . (prefix_set . x''')}) /\ 1956{IN . x''''' . (prefix_set . x'')} /\ 1957{IN . x''''' . (prefix_set . x''')} ==> F`}, 1958 1959{name = "prob_extra_22", 1960 comments = [], 1961 goal = ` 1962~{existential . (K . falsity)} /\ {existential . (K . truth)} /\ 1963~{universal . (K . falsity)} /\ {universal . (K . truth)} /\ ~{falsity} /\ 1964{truth} ==> 1965{P . x} /\ (!x. {real_lte . x . z} \/ ~{P . x}) /\ 1966(!x y z v. 1967 {real_lt . x . (sup . P)} \/ ~{P . y} \/ ~{real_lt . x . y} \/ 1968 ~{P . z} \/ ~{real_lte . (gv13960 . v) . v}) /\ 1969(!x y z. 1970 ~{real_lt . x . (sup . P)} \/ {P . (gv13960 . x)} \/ ~{P . y} \/ 1971 ~{real_lte . (gv13960 . z) . z}) /\ 1972(!x y z. 1973 ~{real_lt . x . (sup . P)} \/ {real_lt . x . (gv13960 . x)} \/ 1974 ~{P . y} \/ ~{real_lte . (gv13960 . z) . z}) /\ 1975(!x y z. 1976 ~{real_lt . x . (sup . P)} \/ {real_lt . x . (gv13960 . x)} \/ 1977 ~{P . y} \/ {P . (gv13960 . z)}) /\ 1978(!x y z. 1979 ~{real_lt . x . (sup . P)} \/ {P . (gv13960 . x)} \/ ~{P . y} \/ 1980 {P . (gv13960 . z)}) /\ 1981(!x y z v. 1982 {real_lt . x . (sup . P)} \/ ~{P . y} \/ ~{real_lt . x . y} \/ 1983 ~{P . z} \/ {P . (gv13960 . v)}) /\ 1984(!x. 1985 {real_lt . (gv13925 . x) . (gv13926 . x)} \/ 1986 {real_lt . (gv13925 . x) . x}) /\ 1987(!x. {P . (gv13926 . x)} \/ {real_lt . (gv13925 . x) . x}) /\ 1988(!x y. 1989 ~{real_lt . (gv13925 . x) . y} \/ ~{P . y} \/ 1990 ~{real_lt . (gv13925 . x) . x}) ==> F`}, 1991 1992{name = "root2_2", 1993 comments = [], 1994 goal = ` 1995(!x y z v. ~(x = y) \/ ~(z = v) \/ x * z = y * v) /\ 1996(!x y. ~(x = y) \/ NUMERAL x = NUMERAL y) /\ 1997(!x y. ~(x = y) \/ BIT2 x = BIT2 y) /\ 1998(!x y z v. ~(x = y) \/ ~(z = v) \/ EXP x z = EXP y v) /\ 1999(!x y z v. ~(x = y) \/ ~(z = v) \/ y < v \/ ~(x < z)) /\ 2000(!x y. ~(x = y) \/ EVEN y \/ ~EVEN x) /\ 2001(!x y z. ~(x = y) \/ ~(x = z) \/ y = z) /\ (!x. x = x) /\ 2002(!x y. 2003 ~(EXP (NUMERAL (BIT2 ZERO) * x) (NUMERAL (BIT2 ZERO)) = 2004 NUMERAL (BIT2 ZERO) * EXP y (NUMERAL (BIT2 ZERO))) \/ 2005 NUMERAL (BIT2 ZERO) * EXP x (NUMERAL (BIT2 ZERO)) = 2006 EXP y (NUMERAL (BIT2 ZERO))) /\ 2007(!x y. 2008 EXP (NUMERAL (BIT2 ZERO) * x) (NUMERAL (BIT2 ZERO)) = 2009 NUMERAL (BIT2 ZERO) * EXP y (NUMERAL (BIT2 ZERO)) \/ 2010 ~(NUMERAL (BIT2 ZERO) * EXP x (NUMERAL (BIT2 ZERO)) = 2011 EXP y (NUMERAL (BIT2 ZERO)))) /\ 2012(!x. ~EVEN x \/ x = NUMERAL (BIT2 ZERO) * gv4671 x) /\ 2013(!x y. EVEN x \/ ~(x = NUMERAL (BIT2 ZERO) * y)) /\ 2014(!x y. ~EVEN (x * y) \/ EVEN x \/ EVEN y) /\ 2015(!x y. EVEN (x * y) \/ ~EVEN x) /\ (!x y. EVEN (x * y) \/ ~EVEN y) /\ 2016(!x. EXP x (NUMERAL (BIT2 ZERO)) = x * x) /\ 2017(!x. EVEN (NUMERAL (BIT2 ZERO) * x)) ==> 2018EXP (NUMERAL (BIT2 ZERO) * k) (NUMERAL (BIT2 ZERO)) = 2019NUMERAL (BIT2 ZERO) * EXP n (NUMERAL (BIT2 ZERO)) /\ 2020(!x y. 2021 ~(EXP x (NUMERAL (BIT2 ZERO)) = 2022 NUMERAL (BIT2 ZERO) * EXP y (NUMERAL (BIT2 ZERO))) \/ x = 0 \/ 2023 ~(x < NUMERAL (BIT2 ZERO) * k)) /\ 2024(!x y. 2025 ~(EXP x (NUMERAL (BIT2 ZERO)) = 2026 NUMERAL (BIT2 ZERO) * EXP y (NUMERAL (BIT2 ZERO))) \/ y = 0 \/ 2027 ~(x < NUMERAL (BIT2 ZERO) * k)) /\ 2028(!x. ~(n = NUMERAL (BIT2 ZERO) * x)) ==> F`}, 2029 2030{name = "TermRewriting_13", 2031 comments = [], 2032 goal = ` 2033~{existential . (K . falsity)} /\ {existential . (K . truth)} /\ 2034~{universal . (K . falsity)} /\ {universal . (K . truth)} /\ ~{falsity} /\ 2035{truth} /\ 2036(!x y z v. 2037 ~{RTC . x . y . z} \/ {RTC . x . v . z} \/ ~{RTC . x . v . y}) ==> 2038{WCR . R} /\ {SN . R} /\ 2039(!x y z. 2040 ~{RTC . R . x . y} \/ ~{RTC . R . x . z} \/ 2041 {RTC . R . y . (gv1300 . x . z . y)} \/ ~{TC . R . (x) . x}) /\ 2042(!x y z. 2043 ~{RTC . R . x . y} \/ ~{RTC . R . x . z} \/ 2044 {RTC . R . z . (gv1300 . x . z . y)} \/ ~{TC . R . (x) . x}) /\ 2045{RTC . R . x . y} /\ {RTC . R . x . z} /\ {R . x . y1} /\ 2046{RTC . R . y1 . y} /\ {R . x . z1} /\ {RTC . R . z1 . z} /\ 2047{RTC . R . y1 . x0} /\ {RTC . R . z1 . x0} /\ {TC . R . x . y1} /\ 2048{TC . R . x . z1} /\ {RTC . R . y . y2} /\ {RTC . R . x0 . y2} /\ 2049{RTC . R . z . z2} /\ {RTC . R . x0 . z2} /\ {TC . R . x . x0} /\ 2050(!x. ~{RTC . R . y . x} \/ ~{RTC . R . z . x}) ==> F`} 2051 2052]; 2053