----- Prover9 July-2005E-work, 18 July 2005 ----- Process 8780 was started by mccune on theorem.mcs.anl.gov, Thu Aug 4 14:33:00 2005 The command was "prover9 -f SD-join.in". % Reading from file SD-join.in set(auto). % set(auto) -> set(auto1). % set(auto1) -> set(auto_inference). % set(auto1) -> set(fof_reduction). % set(auto1) -> set(predicate_elimination). % set(auto1) -> set(unfold_eq). % set(unfold_eq) -> assign(unfold_eq_limit, 2147483647). % set(unfold_eq) -> clear(fold_eq). % set(auto1) -> set(inverse_order). % set(auto1) -> assign(new_constants, 1). % assign(new_constants, 1) -> clear(x_proofs). % assign(new_constants, 1) -> clear(rx_proofs). % set(auto1) -> assign(lex_dep_demod_lim, 11). % set(auto1) -> set(lex_dep_demod_sane). % set(auto1) -> assign(max_weight, 100). % set(auto1) -> assign(age_part, 1). % set(auto1) -> assign(weight_part, 2). % set(auto1) -> assign(weight_neg_part, 2). % set(auto1) -> assign(sos_limit, 10000). % set(auto1) -> clear(x_proofs). % set(auto1) -> assign(stats, lots). % set(auto1) -> assign(max_megs, 200). % set(auto1) -> clear(clocks). assign(constant_weight,0). clauses(sos). x v y = y v x. x ^ y = y ^ x. (x v y) v z = x v (y v z). (x ^ y) ^ z = x ^ (y ^ z). x ^ (x v y) = x. x v (x ^ y) = x. x v x ' = 1. x ^ x ' = 0. x v y != 1 | x ^ y != 0 | x ' = y. A ^ B = A. A ' v B ' != A '. x v y != x v z | x v (y ^ z) = x v y # label(SD_join). end_of_list. % Finished reading the input. % Entering prover search function. % Assigned IDs to 12 clauses. % Predicate elimination: (none). % Relation symbol precedence: lex([ = ]). % Function symbol precedence: lex([ 0, 1, A, B, v, ^, ' ]). % After inverse_order: % Function symbol precedence: lex([ 0, 1, A, B, v, ^, ' ]). % Unfolding symbols: (none). % Auto inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) % Reasonable options, based on the structure of the clauses: % (nothing changed) % Operation v is commutative; redundancy checks enabled. % Operation ^ is commutative; redundancy checks enabled. % Operation v is associative-commutative; redundancy checks enabled. % Operation ^ is associative-commutative; redundancy checks enabled. % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 13 x v y = y v x. [input] 14 x ^ y = y ^ x. [input] 15 (x v y) v z = x v (y v z). [input] 16 (x ^ y) ^ z = x ^ (y ^ z). [input] 17 x ^ (x v y) = x. [input] 18 x v (x ^ y) = x. [input] 19 x v x ' = 1. [input] 20 x ^ x ' = 0. [input] 21 x v y != 1 | x ^ y != 0 | x ' = y. [input] 22 A ^ B = A. [input] 23 A ' v B ' != A '. [input] 24 x v y != x v z | x v (y ^ z) = x v y # label(SD_join). [input] end_of_list. clauses(demodulators). 13 x v y = y v x. [input] % (lex-dep) 14 x ^ y = y ^ x. [input] % (lex-dep) 15 (x v y) v z = x v (y v z). [input] 16 (x ^ y) ^ z = x ^ (y ^ z). [input] 17 x ^ (x v y) = x. [input] 18 x v (x ^ y) = x. [input] 19 x v x ' = 1. [input] 20 x ^ x ' = 0. [input] 22 A ^ B = A. [input] end_of_list. clauses(goals). end_of_list. % Starting search at 0.02 seconds. given #1 (wt=7): 13 x v y = y v x. [input] given #2 (wt=7): 14 x ^ y = y ^ x. [input] given #3 (wt=11): 15 (x v y) v z = x v (y v z). [input] given #4 (wt=11): 16 (x ^ y) ^ z = x ^ (y ^ z). [input] given #5 (wt=7): 17 x ^ (x v y) = x. [input] given #6 (wt=7): 18 x v (x ^ y) = x. [input] given #7 (wt=5): 19 x v x ' = 1. [input] given #8 (wt=5): 20 x ^ x ' = 0. [input] given #9 (wt=12): 21 x v y != 1 | x ^ y != 0 | x ' = y. [input] given #10 (wt=2): 22 A ^ B = A. [input] given #11 (wt=5): 23 A ' v B ' != A '. [input] given #12 (wt=16): 24 x v y != x v z | x v (y ^ z) = x v y # label(SD_join). [input] given #13 (wt=4): 39 x ^ 1 = x. [para (19 (a 1) 17 (a 1 2))] given #14 (wt=4): 42 x v 0 = x. [para (20 (a 1) 18 (a 1 2))] given #15 (wt=4): 58 1 ^ x = x. [para (39 (a 1) 14 (a 1)) flip a] given #16 (wt=11): 25 x v (y v z) = y v (x v z). [para (13 (a 1) 15 (a 1 1)) demod (15)] given #17 (wt=2): 64 1 ' = 0. [hyper (21 a 42 a b 58 a)] given #18 (wt=3): 65 1 v x = 1. [para (58 (a 1) 17 (a 1))] given #19 (wt=3): 73 x v 1 = 1. [para (65 (a 1) 13 (a 1)) flip a] given #20 (wt=2): 76 0 ' = 1. [hyper (21 a 73 a b 39 a)] given #21 (wt=11): 26 x ^ (y ^ z) = y ^ (x ^ z). [para (14 (a 1) 16 (a 1 1)) demod (16)] given #22 (wt=4): 60 0 v x = x. [para (42 (a 1) 13 (a 1)) flip a] given #23 (wt=3): 82 0 ^ x = 0. [para (60 (a 1) 17 (a 1 2))] given #24 (wt=3): 85 x ^ 0 = 0. [para (82 (a 1) 14 (a 1)) flip a] given #25 (wt=5): 35 x ^ x = x. [para (18 (a 1) 17 (a 1 2))] given #26 (wt=7): 27 x ^ (y v x) = x. [para (13 (a 1) 17 (a 1 2))] given #27 (wt=5): 36 x v x = x. [para (17 (a 1) 18 (a 1 2))] given #28 (wt=5): 51 A v B != 1 | A != 0 | A ' = B. [para (22 (a 1) 21 (b 1))] given #29 (wt=5): 75 0 != x | x ' = 1. [back_demod 59 demod (73) xx a] given #30 (wt=5): 87 1 != x | x ' = 0. [back_demod 61 demod (85) xx b] given #31 (wt=13): 28 (x v y) ^ (x v (y v z)) = x v y. [para (15 (a 1) 17 (a 1 2))] given #32 (wt=6): 49 A ^ (B ^ x) = A ^ x. [para (22 (a 1) 16 (a 1 1)) flip a] given #33 (wt=3): 114 A ^ B ' = 0. [para (20 (a 1) 49 (a 1 2)) demod (14 82) flip a] given #34 (wt=4): 113 A ^ (B v x) = A. [para (17 (a 1) 49 (a 1 2)) demod (22) flip a] given #35 (wt=4): 117 A ^ (x v B) = A. [para (27 (a 1) 49 (a 1 2)) demod (22) flip a] given #36 (wt=11): 29 x ^ ((x v y) ^ z) = x ^ z. [para (17 (a 1) 16 (a 1 1)) flip a] given #37 (wt=5): 118 A ^ (B ' ^ x) = 0. [para (114 (a 1) 16 (a 1 1)) demod (82) flip a] given #38 (wt=5): 120 A ^ (x ^ B ') = 0. [para (114 (a 1) 26 (a 1 2)) demod (85) flip a] given #39 (wt=6): 50 B ^ (x ^ A) = x ^ A. [para (22 (a 1) 16 (a 2 2)) demod (14)] given #40 (wt=4): 139 B v (x ^ A) = B. [para (50 (a 1) 18 (a 1 2))] given #41 (wt=13): 30 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para (17 (a 1) 16 (a 1)) flip a] given #42 (wt=2): 145 A v B = B. [para (58 (a 1) 139 (a 1 2)) demod (13)] given #43 (wt=4): 141 B v (A ^ x) = B. [para (14 (a 1) 139 (a 1 2))] given #44 (wt=4): 147 B != 1 | A != 0 | A ' = B. [back_demod 51 demod (145)] given #45 (wt=6): 81 A ^ (x ^ B) = x ^ A. [para (22 (a 1) 26 (a 1 2)) flip a] given #46 (wt=7): 31 x v (y ^ x) = x. [para (14 (a 1) 18 (a 1 2))] given #47 (wt=6): 119 A v B ' != 1 | B ' = A '. [para (114 (a 1) 21 (b 1)) xx b flip b] given #48 (wt=6): 123 A ^ (x v (B v y)) = A. [para (25 (a 1) 113 (a 1 2))] given #49 (wt=6): 125 A ^ (x v (y v B)) = A. [para (15 (a 1) 117 (a 1 2))] given #50 (wt=6): 143 B v (x ^ (y ^ A)) = B. [para (16 (a 1) 139 (a 1 2))] given #51 (wt=11): 32 x v ((x ^ y) v z) = x v z. [para (18 (a 1) 15 (a 1 1)) flip a] given #52 (wt=6): 156 A v (B v x) = B v x. [para (145 (a 1) 15 (a 1 1)) flip a] given #53 (wt=6): 157 B v (x v A) = x v B. [para (145 (a 1) 15 (a 2 2)) demod (13)] given #54 (wt=6): 160 A v (x v B) = x v B. [para (145 (a 1) 25 (a 1 2)) flip a] given #55 (wt=6): 168 B v (x ^ (A ^ y)) = B. [para (26 (a 1) 141 (a 1 2))] given #56 (wt=13): 33 x v (y v ((x v y) ^ z)) = x v y. [para (18 (a 1) 15 (a 1)) flip a] given #57 (wt=6): 213 B v (x v A) = B v x. [para (157 (a 2) 13 (a 1))] given #58 (wt=7): 66 x v (x ' v y) = 1. [back_demod 37 demod (65)] given #59 (wt=3): 251 B v A ' = 1. [para (66 (a 1) 160 (a 1)) demod (13) flip a] given #60 (wt=5): 252 B v (A ' v x) = 1. [para (251 (a 1) 15 (a 1 1)) demod (65) flip a] given #61 (wt=13): 34 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para (16 (a 1) 18 (a 1 2))] given #62 (wt=5): 244 A ^ (A ' v B ') != 0. [ur (21 a 66 a c 23 a_flip)] given #63 (wt=5): 256 B v (x v A ') = 1. [para (251 (a 1) 25 (a 1 2)) demod (73) flip a] given #64 (wt=6): 253 B ^ A ' != 0 | B ' = A '. [para (251 (a 1) 21 (a 1)) xx a] given #65 (wt=7): 74 x v (y v x ') = 1. [back_demod 69 demod (73)] given #66 (wt=9): 38 x v (y v (x v y) ') = 1. [para (19 (a 1) 15 (a 1)) flip a] given #67 (wt=7): 84 x ^ (x ' ^ y) = 0. [back_demod 40 demod (82)] given #68 (wt=7): 86 x ^ (y ^ x ') = 0. [back_demod 79 demod (85)] given #69 (wt=7): 130 x ^ (x v y) ' = 0. [para (20 (a 1) 29 (a 1 2)) demod (85) flip a] given #70 (wt=5): 305 A ^ (B v x) ' = 0. [para (130 (a 1) 49 (a 1 2)) demod (14 82) flip a] given #71 (wt=9): 41 x ^ (y ^ (x ^ y) ') = 0. [para (20 (a 1) 16 (a 1)) flip a] given #72 (wt=5): 306 A ^ (x v B) ' = 0. [para (160 (a 1) 130 (a 1 2 1))] given #73 (wt=7): 135 A ^ (x ^ (B ' ^ y)) = 0. [para (118 (a 1) 26 (a 1 2)) demod (85) flip a] given #74 (wt=7): 136 A ^ (x ^ (y ^ B ')) = 0. [para (16 (a 1) 120 (a 1 2))] given #75 (wt=7): 158 A v x != B | A v (B ^ x) = B. [para (145 (a 1) 24 (a 1)) demod (145) flip a] given #76 (wt=12): 43 x v y != 1 | y ^ x != 0 | y ' = x. [para (13 (a 1) 21 (a 1))] given #77 (wt=4): 342 B != 1 | A != 0 | B ' = A. [para (145 (a 1) 43 (a 1)) demod (14 22)] given #78 (wt=4): 353 B ^ A ' != 0 | B = A. [para (251 (a 1) 43 (a 1)) demod (14 338) xx a flip b] given #79 (wt=5): 327 B != 1 | A v (B ^ A ') = B. [para (19 (a 1) 158 (a 1)) flip a] given #80 (wt=5): 338 x ' ' = x. [para (19 (a 1) 43 (a 1)) demod (14 20) xx a xx b] given #81 (wt=12): 44 x v y != 1 | y ^ x != 0 | x ' = y. [para (14 (a 1) 21 (b 1))] given #82 (wt=4): 369 A v B ' != 1 | B = A. [para (114 (a 1) 44 (b 1)) demod (13 338) xx b] given #83 (wt=7): 202 x v (x ^ y) ' = 1. [para (19 (a 1) 32 (a 1 2)) demod (73) flip a] given #84 (wt=5): 392 B v (x ^ A) ' = 1. [para (50 (a 1) 202 (a 1 2 1))] given #85 (wt=5): 395 B v (A ^ x) ' = 1. [para (14 (a 1) 392 (a 1 2 1))] given #86 (wt=18): 45 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y) ' = z. [para (15 (a 1) 21 (a 1))] given #87 (wt=7): 260 B v (x v (A ' v y)) = 1. [para (252 (a 1) 25 (a 1 2)) demod (73) flip a] given #88 (wt=7): 274 B v (x v (y v A ')) = 1. [para (15 (a 1) 256 (a 1 2))] given #89 (wt=7): 300 x ^ (y v x) ' = 0. [para (13 (a 1) 130 (a 1 2 1))] given #90 (wt=7): 307 A ^ ((B v x) ' ^ y) = 0. [para (305 (a 1) 16 (a 1 1)) demod (82) flip a] given #91 (wt=18): 46 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = z. [para (16 (a 1) 21 (b 1))] given #92 (wt=7): 309 A ^ (x v (B v y)) ' = 0. [para (25 (a 1) 305 (a 1 2 1))] given #93 (wt=7): 310 A ^ (x ^ (B v y) ') = 0. [para (305 (a 1) 26 (a 1 2)) demod (85) flip a] given #94 (wt=7): 316 A ^ (x ^ (B ^ x) ') = 0. [para (41 (a 1) 49 (a 1 2)) demod (14 82) flip a] given #95 (wt=6): 550 A ^ (B ^ (A v x)) ' = 0. [para (316 (a 1) 29 (a 1)) flip a] given #96 (wt=16): 52 x v y != z v x | x v (z ^ y) = x v z. [para (13 (a 1) 24 (a 1)) flip a] given #97 (wt=6): 555 A ^ (B ^ (x v A)) ' = 0. [para (13 (a 1) 550 (a 1 2 1 2))] given #98 (wt=7): 318 A ^ (x v (y v B)) ' = 0. [para (15 (a 1) 306 (a 1 2 1))] given #99 (wt=7): 319 A ^ ((x v B) ' ^ y) = 0. [para (306 (a 1) 16 (a 1 1)) demod (82) flip a] given #100 (wt=7): 321 A ^ (x ^ (y v B) ') = 0. [para (306 (a 1) 26 (a 1 2)) demod (85) flip a] given #101 (wt=16): 53 x v y != z v x | x v (y ^ z) = x v y. [para (13 (a 1) 24 (a 2))] given #102 (wt=7): 326 x v A != B | A v (B ^ x) = B. [para (13 (a 1) 158 (a 1))] given #103 (wt=7): 331 B != 1 | A v (B ^ (A ' v x)) = B. [para (66 (a 1) 158 (a 1)) flip a] given #104 (wt=7): 332 B != 1 | A v (B ^ (x v A ')) = B. [para (74 (a 1) 158 (a 1)) flip a] given #105 (wt=7): 359 x ' v (y v x) = 1. [para (338 (a 1) 74 (a 1 2 2))] given #106 (wt=24): 54 x v (y v z) != x v (y v u) | x v (y v (z ^ u)) = x v (y v z). [para (15 (a 1) 24 (a 1)) demod (15 15 15)] given #107 (wt=7): 360 x ' ^ (y ^ x) = 0. [para (338 (a 1) 86 (a 1 2 2))] given #108 (wt=7): 385 x v (y ^ x) ' = 1. [para (14 (a 1) 202 (a 1 2 1))] given #109 (wt=7): 393 B != 1 | A v (B ^ (A ^ x) ') = B. [para (202 (a 1) 158 (a 1)) flip a] given #110 (wt=7): 396 B v ((x ^ A) ' v y) = 1. [para (392 (a 1) 15 (a 1 1)) demod (65) flip a] given #111 (wt=11): 56 x v y != 1 | x v (x ' ^ y) = 1. [para (19 (a 1) 24 (a 1)) demod (19) flip a] given #112 (wt=5): 802 B v (A ' ^ B ') = 1. [hyper (56 a 251 a) demod (14)] given #113 (wt=5): 806 B != 1 | A v (B ^ A ') = 1. [para (145 (a 1) 56 (a 1)) demod (14)] given #114 (wt=5): 812 A ' ^ B ' = B '. [hyper (21 a 802 a b 86 a) flip a] -------- Proof 1 -------- (0.24 + 0.00 seconds) -------- PROOF -------- Length of proof is 35. Maximum clause weight is 16. 13 x v y = y v x. [input] 14 x ^ y = y ^ x. [input] 15 (x v y) v z = x v (y v z). [input] 16 (x ^ y) ^ z = x ^ (y ^ z). [input] 17 x ^ (x v y) = x. [input] 18 x v (x ^ y) = x. [input] 19 x v x ' = 1. [input] 20 x ^ x ' = 0. [input] 21 x v y != 1 | x ^ y != 0 | x ' = y. [input] 22 A ^ B = A. [input] 23 A ' v B ' != A '. [input] 24 x v y != x v z | x v (y ^ z) = x v y # label(SD_join). [input] 25 x v (y v z) = y v (x v z). [para (13 (a 1) 15 (a 1 1)) demod (15)] 26 x ^ (y ^ z) = y ^ (x ^ z). [para (14 (a 1) 16 (a 1 1)) demod (16)] 37 x v (x ' v y) = 1 v y. [para (19 (a 1) 15 (a 1 1)) flip a] 39 x ^ 1 = x. [para (19 (a 1) 17 (a 1 2))] 42 x v 0 = x. [para (20 (a 1) 18 (a 1 2))] 50 B ^ (x ^ A) = x ^ A. [para (22 (a 1) 16 (a 2 2)) demod (14)] 56 x v y != 1 | x v (x ' ^ y) = 1. [para (19 (a 1) 24 (a 1)) demod (19) flip a] 58 1 ^ x = x. [para (39 (a 1) 14 (a 1)) flip a] 60 0 v x = x. [para (42 (a 1) 13 (a 1)) flip a] 65 1 v x = 1. [para (58 (a 1) 17 (a 1))] 66 x v (x ' v y) = 1. [back_demod 37 demod (65)] 79 x ^ (y ^ x ') = y ^ 0. [para (20 (a 1) 26 (a 1 2)) flip a] 82 0 ^ x = 0. [para (60 (a 1) 17 (a 1 2))] 85 x ^ 0 = 0. [para (82 (a 1) 14 (a 1)) flip a] 86 x ^ (y ^ x ') = 0. [back_demod 79 demod (85)] 139 B v (x ^ A) = B. [para (50 (a 1) 18 (a 1 2))] 145 A v B = B. [para (58 (a 1) 139 (a 1 2)) demod (13)] 160 A v (x v B) = x v B. [para (145 (a 1) 25 (a 1 2)) flip a] 251 B v A ' = 1. [para (66 (a 1) 160 (a 1)) demod (13) flip a] 802 B v (A ' ^ B ') = 1. [hyper (56 a 251 a) demod (14)] 812 A ' ^ B ' = B '. [hyper (21 a 802 a b 86 a) flip a] 814 A ' v B ' = A '. [para (812 (a 1) 18 (a 1 2))] 815 $F. [resolve (814 a 23 a)] -------- end of proof ------- Given=114. Generated=4510. Kept=802. Proofs=1. Usable=111. Sos=662. Demods=282. Goals=0. Limbo=1, Disabled=39. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=3708. Back_subsumed=2. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=289 (4 lex), Back_demodulated=25. Back_unit_deleted=0. Demod_attempts=46566. Demod_rewrites=8594. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=7768. Nonunit_bsub_feature_tests=3568. Megabytes=0.74. User_CPU=0.24, System_CPU=0.00, Wall_clock=0. THEOREM PROVED Exiting with 1 proof. Process 8780 exit (max_proofs) Thu Aug 4 14:33:00 2005