============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5094 was started by mccune on cleo, Tue Nov 3 09:41:54 2009 The command was "/home/mccune/LADR/bin/prover9 -f gt.in AN.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file gt.in assign(max_seconds,30). op(450,infix,@). op(400,infix_right,*). assign(eq_defs,fold). assign(max_weight,25). formulas(sos). (x * y) * z = x * y * z. e * x = x. x' * x = e. x @ y = x' * y' * x * y. end_of_list. % Reading from file AN.in formulas(sos). (x @ y) @ z = u @ (v @ w). end_of_list. formulas(sos). (A @ B) * C != C * (A @ B) # answer(N). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). (x * y) * z = x * y * z. [assumption]. e * x = x. [assumption]. x' * x = e. [assumption]. x @ y = x' * y' * x * y. [assumption]. (x @ y) @ z = u @ (w @ v5). [assumption]. (A @ B) * C != C * (A @ B) # answer(N). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ e, A, B, C, *, @, ' ]). After inverse_order: Function symbol precedence: function_order([ e, A, B, C, *, ', @ ]). Folding symbols: @/2. After fold_eq: Function symbol precedence: function_order([ e, A, B, C, @, *, ' ]). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). kept: 1 (x * y) * z = x * y * z. [assumption]. kept: 2 e * x = x. [assumption]. kept: 3 x' * x = e. [assumption]. 4 x @ y = x' * y' * x * y. [assumption]. kept: 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. kept: 6 (x @ y) @ z = u @ (w @ v5). [assumption]. kept: 7 (A @ B) * C != C * (A @ B) # answer(N). [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 (x * y) * z = x * y * z. [assumption]. 2 e * x = x. [assumption]. 3 x' * x = e. [assumption]. 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. 6 (x @ y) @ z = u @ (w @ v5). [assumption]. 7 (A @ B) * C != C * (A @ B) # answer(N). [assumption]. end_of_list. formulas(demodulators). 1 (x * y) * z = x * y * z. [assumption]. 2 e * x = x. [assumption]. 3 x' * x = e. [assumption]. 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=11): 1 (x * y) * z = x * y * z. [assumption]. given #2 (I,wt=5): 2 e * x = x. [assumption]. given #3 (I,wt=6): 3 x' * x = e. [assumption]. given #4 (I,wt=13): 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. given #5 (I,wt=11): 6 (x @ y) @ z = u @ (w @ v5). [assumption]. given #6 (I,wt=11): 7 (A @ B) * C != C * (A @ B) # answer(N). [assumption]. given #7 (A,wt=8): 8 x' * x * y = y. [para(3(a,1),1(a,1,1)),rewrite([2(2)]),flip(a)]. given #8 (T,wt=5): 11 e @ x = e. [para(2(a,1),5(a,1,2,2)),rewrite([3(4),3(4)]),flip(a)]. given #9 (T,wt=4): 27 e' = e. [para(11(a,1),5(a,2)),rewrite([2(5),3(4),25(4)])]. given #10 (T,wt=5): 20 x @ x = e. [para(8(a,1),5(a,1,2)),rewrite([3(2)]),flip(a)]. given #11 (T,wt=5): 25 x * e = x. [back_rewrite(18),rewrite([22(4)])]. given #12 (A,wt=17): 9 x' * y' * x * y * z = (x @ y) * z. [para(5(a,1),1(a,1,1)),rewrite([1(7),1(6)]),flip(a)]. given #13 (F,wt=17): 41 A' * B' * A * B * C != C * (A @ B) # answer(N). [para(9(a,2),7(a,1))]. given #14 (T,wt=5): 31 x @ e = e. [back_rewrite(29),rewrite([30(2)]),flip(a)]. given #15 (T,wt=6): 12 x' @ x = e. [para(3(a,1),5(a,1,2,2)),rewrite([8(6)]),flip(a)]. given #16 (T,wt=7): 28 x @ (y @ z) = e. [para(11(a,1),6(a,1,1)),rewrite([11(2)]),flip(a)]. given #17 (T,wt=7): 30 (x @ y) @ z = e. [para(11(a,1),6(a,2))]. given #18 (A,wt=19): 10 (x * y)' * z' * x * y * z = x * y @ z. [para(1(a,1),5(a,1,2,2))]. given #19 (T,wt=7): 61 x * x @ x = e. [para(10(a,1),10(a,1,2)),rewrite([3(2),27(2),2(4),3(4),11(5)])]. given #20 (T,wt=9): 22 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. given #21 (T,wt=5): 69 x'' = x. [para(22(a,1),25(a,1)),rewrite([25(2)]),flip(a)]. given #22 (T,wt=6): 64 x * x' = e. [para(22(a,1),3(a,1))]. given #23 (A,wt=12): 16 (x * y)' * x * y * z = z. [para(1(a,1),8(a,1,2))]. given #24 (T,wt=6): 73 x @ x' = e. [para(69(a,1),12(a,1,1))]. given #25 (T,wt=7): 82 x @ x * x = e. [para(16(a,1),5(a,1,2)),rewrite([3(2)]),flip(a)]. given #26 (T,wt=8): 68 x * x' * y = y. [para(22(a,1),8(a,1))]. given #27 (T,wt=9): 93 x' * x' @ x = e. [para(16(a,1),10(a,1)),rewrite([3(2)]),flip(a)]. given #28 (A,wt=12): 23 x' * y * x = y * (y @ x). [back_rewrite(21),rewrite([22(4)]),flip(a)]. given #29 (T,wt=9): 95 (x * y)' * x = y'. [para(64(a,1),16(a,1,2,2)),rewrite([25(4)])]. given #30 (T,wt=8): 135 (x @ y)' = y @ x. [para(23(a,2),95(a,1,1,1)),rewrite([125(4),125(2),69(5),1(4),1(5),1(4),5(5)]),flip(a)]. given #31 (T,wt=9): 139 x @ y * x = x @ y. [back_rewrite(122),rewrite([125(2),1(5),5(5)]),flip(a)]. given #32 (T,wt=8): 181 x' @ y = y @ x. [back_rewrite(177),rewrite([180(3)])]. given #33 (A,wt=21): 32 x * y' * z' * y * z * u = x * (y @ z) * u. [para(9(a,1),1(a,2,2)),rewrite([1(7)])]. given #34 (F,wt=12): 183 (B' @ A) * C != C * (A @ B) # answer(N). [para(181(a,2),7(a,1,1))]. given #35 (F,wt=12): 184 C * (B' @ A) != (A @ B) * C # answer(N). [para(181(a,2),7(a,2,2)),flip(a)]. given #36 (F,wt=13): 210 (B' @ A) * C != C * (B' @ A) # answer(N). [para(181(a,2),183(a,2,2))]. given #37 (F,wt=17): 209 B * A' * B' * A * C != C * (A @ B) # answer(N). [para(9(a,2),183(a,1)),rewrite([69(3)])]. given #38 (T,wt=8): 188 x @ y' = y @ x. [para(69(a,1),181(a,1,1)),flip(a)]. given #39 (T,wt=9): 169 x * y @ x = y @ x. [back_rewrite(119),rewrite([139(4)])]. given #40 (T,wt=9): 170 (x @ y) * (y @ x) = e. [para(135(a,1),3(a,1,1))]. given #41 (T,wt=9): 180 x * y @ y = x @ y. [para(139(a,1),135(a,1,1)),rewrite([135(2)]),flip(a)]. given #42 (A,wt=13): 35 x' * y * x = (x @ y') * y. [para(3(a,1),9(a,1,2,2,2)),rewrite([25(5),22(4)])]. given #43 (F,wt=12): 212 (B @ A') * C != C * (A @ B) # answer(N). [para(188(a,2),7(a,1,1))]. given #44 (F,wt=12): 213 C * (B @ A') != (A @ B) * C # answer(N). [para(188(a,2),7(a,2,2)),flip(a)]. given #45 (F,wt=13): 222 (B @ A') * C != C * (B @ A') # answer(N). [para(188(a,2),183(a,2,2)),rewrite([219(4)])]. given #46 (F,wt=17): 257 B' * A * B * A' * C != C * (A @ B) # answer(N). [para(9(a,2),212(a,1)),rewrite([69(5)])]. given #47 (T,wt=9): 191 x' @ y' = x @ y. [para(181(a,1),181(a,2))]. given #48 (T,wt=9): 219 x' @ y = x @ y'. [para(188(a,1),181(a,1)),flip(a)]. given #49 (T,wt=9): 228 x @ x * y = x @ y. [para(169(a,1),135(a,1,1)),rewrite([135(2)]),flip(a)]. given #50 (T,wt=10): 104 x' @ y * x = y @ x. [para(23(a,1),5(a,1,2,2)),rewrite([69(2),101(5),68(4)]),flip(a)]. given #51 (A,wt=22): 38 x' * y * x * (y @ z) = (x @ y') * z' * y * z. [para(5(a,1),9(a,1,2,2,2)),rewrite([22(6)])]. given #52 (F,wt=18): 216 A' * B' * A * B * C != C * (B @ A') # answer(N). [para(188(a,2),41(a,2,2))]. given #53 (F,wt=18): 223 B * A' * B' * A * C != C * (B @ A') # answer(N). [para(188(a,2),209(a,2,2))]. given #54 (F,wt=18): 258 B' * A * B * A' * C != C * (B @ A') # answer(N). [para(9(a,2),222(a,1)),rewrite([69(5)])]. given #55 (T,wt=10): 114 x' * y @ x = y @ x. [para(23(a,1),10(a,1,2,2)),rewrite([101(8),8(4)]),flip(a)]. given #56 (T,wt=10): 125 (x * y)' = y' * x'. [para(8(a,1),95(a,1,1,1)),flip(a)]. given #57 (T,wt=10): 168 x * y @ y' = y @ x. [back_rewrite(120),rewrite([139(5)])]. given #58 (T,wt=10): 182 x * y @ x' = x @ y. [back_rewrite(174),rewrite([180(5)])]. given #59 (A,wt=12): 40 (x' @ y) * x = x * (y @ x). [para(5(a,1),9(a,1,2)),rewrite([22(4)]),flip(a)]. given #60 (T,wt=10): 227 x' * y * x @ y = e. [para(23(a,2),169(a,1,1)),rewrite([30(6)])]. given #61 (T,wt=10): 229 x' @ x * y = y @ x. [para(169(a,1),181(a,2))]. given #62 (T,wt=10): 232 (x @ y) * (x @ y') = e. [para(181(a,1),170(a,1,1))]. given #63 (T,wt=10): 233 (x @ y') * (x @ y) = e. [para(181(a,1),170(a,1,2))]. given #64 (A,wt=16): 42 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite([22(5)]),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.05 (+ 0.00) seconds: N. % Length of proof is 44. % Level of proof is 13. % Maximum clause weight is 19.000. % Given clauses 64. 1 (x * y) * z = x * y * z. [assumption]. 2 e * x = x. [assumption]. 3 x' * x = e. [assumption]. 4 x @ y = x' * y' * x * y. [assumption]. 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. 6 (x @ y) @ z = u @ (w @ v5). [assumption]. 7 (A @ B) * C != C * (A @ B) # answer(N). [assumption]. 8 x' * x * y = y. [para(3(a,1),1(a,1,1)),rewrite([2(2)]),flip(a)]. 9 x' * y' * x * y * z = (x @ y) * z. [para(5(a,1),1(a,1,1)),rewrite([1(7),1(6)]),flip(a)]. 10 (x * y)' * z' * x * y * z = x * y @ z. [para(1(a,1),5(a,1,2,2))]. 11 e @ x = e. [para(2(a,1),5(a,1,2,2)),rewrite([3(4),3(4)]),flip(a)]. 16 (x * y)' * x * y * z = z. [para(1(a,1),8(a,1,2))]. 18 x'' * e = x. [para(3(a,1),8(a,1,2))]. 21 x'' * (x @ y) = y' * x * y. [para(5(a,1),8(a,1,2))]. 22 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. 23 x' * y * x = y * (y @ x). [back_rewrite(21),rewrite([22(4)]),flip(a)]. 25 x * e = x. [back_rewrite(18),rewrite([22(4)])]. 28 x @ (y @ z) = e. [para(11(a,1),6(a,1,1)),rewrite([11(2)]),flip(a)]. 30 (x @ y) @ z = e. [para(11(a,1),6(a,2))]. 42 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite([22(5)]),flip(a)]. 57 (x * y)' * y * x = x * y @ x. [para(8(a,1),10(a,1,2))]. 59 x' * (y * x @ y) * x = x @ y * x. [para(9(a,1),10(a,1,2)),rewrite([8(3),8(8)])]. 64 x * x' = e. [para(22(a,1),3(a,1))]. 68 x * x' * y = y. [para(22(a,1),8(a,1))]. 69 x'' = x. [para(22(a,1),25(a,1)),rewrite([25(2)]),flip(a)]. 95 (x * y)' * x = y'. [para(64(a,1),16(a,1,2,2)),rewrite([25(4)])]. 101 (x * y)' * x * z = y' * z. [para(68(a,1),16(a,1,2,2))]. 111 x' * (y @ z) * x = y @ z. [para(23(a,2),9(a,2)),rewrite([30(4),25(4),5(5)]),flip(a)]. 114 x' * y @ x = y @ x. [para(23(a,1),10(a,1,2,2)),rewrite([101(8),8(4)]),flip(a)]. 119 x * y @ x = y @ x * y. [back_rewrite(59),rewrite([111(5)])]. 122 (x * y)' * y * x = y @ x * y. [back_rewrite(57),rewrite([119(6)])]. 125 (x * y)' = y' * x'. [para(8(a,1),95(a,1,1,1)),flip(a)]. 135 (x @ y)' = y @ x. [para(23(a,2),95(a,1,1,1)),rewrite([125(4),125(2),69(5),1(4),1(5),1(4),5(5)]),flip(a)]. 139 x @ y * x = x @ y. [back_rewrite(122),rewrite([125(2),1(5),5(5)]),flip(a)]. 170 (x @ y) * (y @ x) = e. [para(135(a,1),3(a,1,1))]. 177 x' * y @ y = y @ x. [para(68(a,1),139(a,1,2)),rewrite([114(6)])]. 180 x * y @ y = x @ y. [para(139(a,1),135(a,1,1)),rewrite([135(2)]),flip(a)]. 181 x' @ y = y @ x. [back_rewrite(177),rewrite([180(3)])]. 183 (B' @ A) * C != C * (A @ B) # answer(N). [para(181(a,2),7(a,1,1))]. 188 x @ y' = y @ x. [para(69(a,1),181(a,1,1)),flip(a)]. 219 x' @ y = x @ y'. [para(188(a,1),181(a,1)),flip(a)]. 222 (B @ A') * C != C * (B @ A') # answer(N). [para(188(a,2),183(a,2,2)),rewrite([219(4)])]. 407 (x @ y) * z = z * (x @ y). [para(170(a,1),42(a,1,2,2)),rewrite([135(2),25(3),28(4),2(5)])]. 408 $F # answer(N). [resolve(407,a,222,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=64. Generated=2131. Kept=406. proofs=1. Usable=51. Sos=201. Demods=150. Limbo=32, Disabled=127. Hints=0. Kept_by_rule=0, Deleted_by_rule=127. Forward_subsumed=1598. Back_subsumed=5. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=240 (1 lex), Back_demodulated=116. Back_unit_deleted=0. Demod_attempts=25038. Demod_rewrites=4850. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.35. User_CPU=0.05, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 5094 exit (max_proofs) Tue Nov 3 09:41:54 2009