============================== Prover9 =============================== Prover9 (32) version 2009-02A, February 2009. Process 11616 was started by mccune on cleo, Wed Feb 25 09:33:12 2009 The command was "/home/mccune/bin/prover9 -f gt.in ND.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 ND.in formulas(sos). (x @ y) * z = z * (x @ y). end_of_list. formulas(sos). (A @ C) * (B @ C) != A * B @ C # answer(D). 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 = z * (x @ y). [assumption]. (A @ C) * (B @ C) != A * B @ C # answer(D). [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 = z * (x @ y). [assumption]. kept: 7 (A @ C) * (B @ C) != A * B @ C # answer(D). [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 = z * (x @ y). [assumption]. 7 (A @ C) * (B @ C) != A * B @ C # answer(D). [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)]. 6 (x @ y) * z = z * (x @ y). [assumption]. % (lex-dep) 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 = z * (x @ y). [assumption]. given #6 (I,wt=13): 7 (A @ C) * (B @ C) != A * B @ C # answer(D). [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): 33 e' = e. [para(11(a,1),5(a,2)),rewrite([2(5),3(4),31(4)])]. given #10 (T,wt=5): 24 x @ x = e. [para(8(a,1),5(a,1,2)),rewrite([3(2)]),flip(a)]. given #11 (T,wt=5): 31 x * e = x. [back_rewrite(22),rewrite([28(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=19): 47 A' * C' * A * C * (B @ C) != A * B @ C # answer(D). [para(9(a,2),7(a,1))]. given #14 (T,wt=5): 34 x @ e = e. [para(33(a,1),5(a,1,2,1)),rewrite([31(4),2(3),3(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): 18 (x @ y) @ z = e. [para(6(a,1),5(a,1,2,2)),rewrite([8(6),6(4,R),17(4)]),flip(a)]. given #17 (T,wt=7): 19 x @ (y @ z) = e. [para(6(a,2),5(a,1,2,2)),rewrite([8(6),3(2)]),flip(a)]. 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): 73 x @ x * x = e. [para(10(a,1),10(a,1,2)),rewrite([3(2),33(2),71(3),2(4),3(4),11(5)])]. given #20 (T,wt=9): 28 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. given #21 (T,wt=5): 83 x'' = x. [para(28(a,1),31(a,1)),rewrite([31(2)]),flip(a)]. given #22 (T,wt=6): 77 x * x' = e. [para(28(a,1),3(a,1))]. given #23 (A,wt=15): 14 (x @ y) * z * u = z * (x @ y) * u. [para(6(a,1),1(a,1,1)),rewrite([1(3)]),flip(a)]. given #24 (T,wt=6): 87 x @ x' = e. [para(83(a,1),12(a,1,1))]. given #25 (T,wt=8): 82 x * x' * y = y. [para(28(a,1),8(a,1))]. given #26 (T,wt=10): 88 x * y * (x * y)' = e. [para(77(a,1),1(a,1)),flip(a)]. given #27 (T,wt=9): 123 x * (y * x)' = y'. [para(88(a,1),8(a,1,2)),rewrite([31(3)]),flip(a)]. given #28 (A,wt=15): 15 x * (y @ z) * u = x * u * (y @ z). [para(6(a,1),1(a,2,2)),rewrite([1(3)])]. given #29 (T,wt=8): 139 (x @ y)' = y @ x. [para(9(a,2),123(a,1,2,1)),rewrite([138(7),138(5),138(3),138(2),1(5),83(7),1(6),1(5),83(8),1(7),1(6),1(5),5(6),82(4)]),flip(a)]. given #30 (T,wt=9): 144 (x @ y) * (y @ x) = e. [back_rewrite(128),rewrite([138(5),138(4),139(4),1(6),82(7),110(5)])]. given #31 (T,wt=9): 154 x @ y * x = x @ y. [back_rewrite(75),rewrite([138(2),1(5),5(5)]),flip(a)]. given #32 (T,wt=9): 175 x * y @ x = y @ x. [back_rewrite(71),rewrite([154(4)])]. given #33 (A,wt=15): 16 (x @ y) * z * u = z * u * (x @ y). [para(6(a,1),1(a,2)),rewrite([1(3),1(6)])]. given #34 (F,wt=19): 230 A' * C' * (B @ C) * A * C != A * B @ C # answer(D). [para(16(a,2),47(a,1,2,2))]. given #35 (F,wt=25): 241 A' * C' * B' * C' * B * C * A * C != A * B @ C # answer(D). [para(9(a,2),230(a,1,2,2))]. given #36 (T,wt=8): 217 x @ y' = y @ x. [para(8(a,1),175(a,1,1)),rewrite([215(5)])]. given #37 (T,wt=8): 219 x' @ y = y @ x. [para(82(a,1),175(a,1,1)),rewrite([214(4)]),flip(a)]. given #38 (T,wt=9): 213 x * y @ y = x @ y. [para(154(a,1),139(a,1,1)),rewrite([139(2)]),flip(a)]. given #39 (T,wt=9): 220 x @ x * y = x @ y. [para(175(a,1),139(a,1,1)),rewrite([139(2)]),flip(a)]. given #40 (A,wt=12): 27 x' * (y @ z) * x = y @ z. [para(6(a,2),8(a,1,2))]. given #41 (F,wt=14): 244 (B @ C) * (C @ A') != A * B @ C # answer(D). [para(217(a,2),7(a,1,1)),rewrite([6(8,R)])]. given #42 (F,wt=14): 245 (A @ C) * (C @ B') != A * B @ C # answer(D). [para(217(a,2),7(a,1,2))]. given #43 (F,wt=14): 268 C' @ A * B != (A @ C) * (B @ C) # answer(D). [para(219(a,2),7(a,2)),flip(a)]. given #44 (F,wt=15): 246 C @ B' * A' != (A @ C) * (B @ C) # answer(D). [para(217(a,2),7(a,2)),rewrite([138(12)]),flip(a)]. given #45 (T,wt=9): 262 x' @ y' = x @ y. [para(217(a,1),217(a,2))]. given #46 (T,wt=9): 280 x' @ y = x @ y'. [para(219(a,1),217(a,1))]. given #47 (T,wt=10): 138 (x * y)' = y' * x'. [para(123(a,1),8(a,1,2)),flip(a)]. given #48 (T,wt=10): 173 x * y @ y' = y @ x. [back_rewrite(91),rewrite([154(5)])]. given #49 (A,wt=12): 29 x' * y * x = y * (y @ x). [back_rewrite(25),rewrite([28(4)]),flip(a)]. given #50 (F,wt=15): 296 (C @ A') * (C @ B') != A * B @ C # answer(D). [para(217(a,2),244(a,1,1)),rewrite([6(9,R)])]. given #51 (F,wt=15): 298 C' @ A * B != (B @ C) * (C @ A') # answer(D). [para(219(a,2),244(a,2)),flip(a)]. given #52 (F,wt=15): 300 C' @ A * B != (A @ C) * (C @ B') # answer(D). [para(219(a,2),245(a,2)),flip(a)]. given #53 (F,wt=16): 297 C @ B' * A' != (B @ C) * (C @ A') # answer(D). [para(217(a,2),244(a,2)),rewrite([138(13)]),flip(a)]. given #54 (T,wt=10): 215 x * y @ x' = x @ y. [back_rewrite(206),rewrite([213(5)])]. given #55 (T,wt=10): 255 (x @ y) * (x' @ y) = e. [para(217(a,1),144(a,1,1))]. given #56 (T,wt=10): 256 (x @ y) * (x @ y') = e. [para(217(a,2),144(a,1,1)),rewrite([6(4,R)])]. given #57 (T,wt=10): 287 x' @ y * x = y @ x. [para(213(a,1),219(a,2))]. given #58 (A,wt=21): 35 x * y' * z' * y * z * u = x * (y @ z) * u. [para(9(a,1),1(a,2,2)),rewrite([1(7)])]. given #59 (F,wt=16): 299 C @ B' * A' != (A @ C) * (C @ B') # answer(D). [para(217(a,2),245(a,2)),rewrite([138(13)]),flip(a)]. given #60 (F,wt=16): 301 B' * A' @ C' != (A @ C) * (B @ C) # answer(D). [para(219(a,2),268(a,1)),rewrite([138(4)])]. given #61 (F,wt=16): 362 C' @ A * B != (C @ A') * (C @ B') # answer(D). [para(219(a,2),296(a,2)),flip(a)]. given #62 (F,wt=17): 361 C @ B' * A' != (C @ A') * (C @ B') # answer(D). [para(217(a,2),296(a,2)),rewrite([138(14)]),flip(a)]. given #63 (T,wt=10): 346 x' * y * x @ y = e. [para(29(a,2),175(a,1,1)),rewrite([18(6)])]. given #64 (T,wt=10): 354 x @ y' * x * y = e. [para(29(a,2),220(a,1,2)),rewrite([19(6)])]. given #65 (T,wt=10): 432 x * y * x' @ y = e. [para(83(a,1),346(a,1,1,1))]. given #66 (T,wt=10): 447 x @ y * x * y' = e. [para(83(a,1),354(a,1,2,1))]. given #67 (A,wt=13): 38 x' * y * x = y * (x @ y'). [para(3(a,1),9(a,1,2,2,2)),rewrite([31(5),28(4),6(6)])]. given #68 (F,wt=17): 364 B' * A' @ C' != (B @ C) * (C @ A') # answer(D). [para(219(a,2),298(a,1)),rewrite([138(4)])]. given #69 (F,wt=17): 366 B' * A' @ C' != (A @ C) * (C @ B') # answer(D). [para(219(a,2),300(a,1)),rewrite([138(4)])]. given #70 (F,wt=18): 426 B' * A' @ C' != (C @ A') * (C @ B') # answer(D). [para(219(a,2),362(a,1)),rewrite([138(4)])]. given #71 (F,wt=20): 249 A' * C' * A * C * (C @ B') != A * B @ C # answer(D). [para(217(a,2),47(a,1,2,2,2,2))]. given #72 (T,wt=11): 130 x' * y' @ x * y = e. [back_rewrite(60),rewrite([124(8),3(8)]),flip(a)]. given #73 (T,wt=9): 510 x * y @ y * x = e. [para(130(a,1),217(a,2)),rewrite([138(5),83(3),83(3)])]. given #74 (T,wt=11): 164 x' @ x * y = x' @ y. [back_rewrite(30),rewrite([138(2),1(4),80(5)]),flip(a)]. given #75 (T,wt=11): 169 (x @ y) * z * (y @ x) = z. [back_rewrite(111),rewrite([139(3)])]. given #76 (A,wt=22): 41 x' * y * x * (y @ z) = (x @ y') * z' * y * z. [para(5(a,1),9(a,1,2,2,2)),rewrite([28(6)])]. given #77 (F,wt=20): 272 A' * C' * A * C * (B @ C) != C' @ A * B # answer(D). [para(219(a,2),47(a,2))]. given #78 (F,wt=20): 279 A' * C' * (B @ C) * A * C != C' @ A * B # answer(D). [para(219(a,2),230(a,2))]. given #79 (F,wt=20): 295 B' * C' * B * C * (C @ A') != A * B @ C # answer(D). [para(9(a,2),244(a,1))]. given #80 (F,wt=19): 579 B' * C' * B * C * (A @ C) != A * B @ C # answer(D). [para(217(a,1),295(a,1,2,2,2,2))]. given #81 (T,wt=11): 174 x * y' @ y = y' @ x. [back_rewrite(74),rewrite([154(7)])]. given #82 (T,wt=11): 191 x @ (y @ z) * u = x @ u. [back_rewrite(152),rewrite([188(8),5(5)]),flip(a)]. given #83 (T,wt=11): 192 (x @ y) * z @ u = z @ u. [back_rewrite(151),rewrite([188(9),5(5)]),flip(a)]. given #84 (T,wt=11): 198 x * (y @ z) @ u = x @ u. [back_rewrite(64),rewrite([192(3)]),flip(a)]. given #85 (A,wt=17): 44 x' * y' * x * y * z = z * (x @ y). [para(9(a,2),6(a,1))]. given #86 (F,wt=19): 629 C' * A * C * (B @ C) * A' != A * B @ C # answer(D). [para(44(a,2),244(a,1)),rewrite([83(5),6(10,R)])]. given #87 (F,wt=19): 630 C' * B * C * (A @ C) * B' != A * B @ C # answer(D). [para(44(a,2),245(a,1)),rewrite([83(5),6(10,R)])]. given #88 (F,wt=19): 660 C' * A * (B @ C) * C * A' != A * B @ C # answer(D). [para(14(a,2),629(a,1,2,2))]. given #89 (F,wt=19): 662 C' * B * (A @ C) * C * B' != A * B @ C # answer(D). [para(14(a,2),630(a,1,2,2))]. given #90 (T,wt=11): 199 x @ y * (z @ u) = x @ y. [back_rewrite(179),rewrite([198(3)]),flip(a)]. given #91 (T,wt=11): 202 (x @ y) * (y @ x) * z = z. [para(139(a,1),8(a,1,1))]. given #92 (T,wt=11): 214 x' * y @ x = x' @ y. [back_rewrite(211),rewrite([213(3)]),flip(a)]. given #93 (T,wt=11): 257 x @ x' * y = y @ x'. [para(217(a,1),175(a,1))]. given #94 (A,wt=21): 46 x' * y' * x * (z @ u) * y = (x @ y) * (z @ u). [para(6(a,2),9(a,1,2,2,2))]. given #95 (F,wt=19): 664 C' * (B @ C) * A * C * A' != A * B @ C # answer(D). [para(14(a,2),660(a,1,2))]. given #96 (F,wt=19): 668 C' * (A @ C) * B * C * B' != A * B @ C # answer(D). [para(14(a,2),662(a,1,2))]. given #97 (F,wt=20): 360 C' * A * C * A' * (C @ B') != A * B @ C # answer(D). [para(9(a,2),296(a,1)),rewrite([83(5)])]. given #98 (F,wt=20): 499 A' * C' * A * B * C * B' != A * B @ C # answer(D). [para(29(a,2),249(a,1,2,2,2)),rewrite([83(8)])]. given #99 (T,wt=11): 286 x @ y * x' = y @ x'. [para(213(a,1),217(a,1)),flip(a)]. given #100 (T,wt=11): 312 (x @ y') * (y @ x') = e. [para(280(a,1),144(a,1,1))]. given #101 (T,wt=11): 313 (x' @ y) * (y' @ x) = e. [para(280(a,2),144(a,1,1))]. given #102 (T,wt=11): 319 x * y @ y' * x' = e. [para(138(a,1),87(a,1,2))]. given #103 (A,wt=16): 48 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite([28(5)]),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.12 (+ 0.00) seconds: D. % Length of proof is 37. % Level of proof is 14. % Maximum clause weight is 21. % Given clauses 103. 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 = z * (x @ y). [assumption]. 7 (A @ C) * (B @ C) != A * B @ C # answer(D). [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))]. 22 x'' * e = x. [para(3(a,1),8(a,1,2))]. 28 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. 31 x * e = x. [back_rewrite(22),rewrite([28(4)])]. 46 x' * y' * x * (z @ u) * y = (x @ y) * (z @ u). [para(6(a,2),9(a,1,2,2,2))]. 48 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite([28(5)]),flip(a)]. 69 (x * y)' * y * x = x * y @ x. [para(8(a,1),10(a,1,2))]. 71 x * y @ x = y @ x * y. [para(9(a,1),10(a,1,2)),rewrite([8(3),6(4),8(5),8(5)])]. 75 (x * y)' * y * x = y @ x * y. [back_rewrite(69),rewrite([71(6)])]. 77 x * x' = e. [para(28(a,1),3(a,1))]. 82 x * x' * y = y. [para(28(a,1),8(a,1))]. 83 x'' = x. [para(28(a,1),31(a,1)),rewrite([31(2)]),flip(a)]. 88 x * y * (x * y)' = e. [para(77(a,1),1(a,1)),flip(a)]. 123 x * (y * x)' = y'. [para(88(a,1),8(a,1,2)),rewrite([31(3)]),flip(a)]. 138 (x * y)' = y' * x'. [para(123(a,1),8(a,1,2)),flip(a)]. 139 (x @ y)' = y @ x. [para(9(a,2),123(a,1,2,1)),rewrite([138(7),138(5),138(3),138(2),1(5),83(7),1(6),1(5),83(8),1(7),1(6),1(5),5(6),82(4)]),flip(a)]. 154 x @ y * x = x @ y. [back_rewrite(75),rewrite([138(2),1(5),5(5)]),flip(a)]. 175 x * y @ x = y @ x. [back_rewrite(71),rewrite([154(4)])]. 206 x * y @ x' = x * y @ y. [para(8(a,1),154(a,1,2)),flip(a)]. 213 x * y @ y = x @ y. [para(154(a,1),139(a,1,1)),rewrite([139(2)]),flip(a)]. 215 x * y @ x' = x @ y. [back_rewrite(206),rewrite([213(5)])]. 217 x @ y' = y @ x. [para(8(a,1),175(a,1,1)),rewrite([215(5)])]. 244 (B @ C) * (C @ A') != A * B @ C # answer(D). [para(217(a,2),7(a,1,1)),rewrite([6(8,R)])]. 296 (C @ A') * (C @ B') != A * B @ C # answer(D). [para(217(a,2),244(a,1,1)),rewrite([6(9,R)])]. 316 x' * y' * z' * x * z * y = x @ z * y. [para(138(a,1),5(a,1,2,1)),rewrite([1(7)])]. 361 C @ B' * A' != (C @ A') * (C @ B') # answer(D). [para(217(a,2),296(a,2)),rewrite([138(14)]),flip(a)]. 825 x @ y * z = (x @ z) * (x @ y). [para(48(a,2),46(a,1,2,2)),rewrite([316(8)])]. 826 $F # answer(D). [resolve(825,a,361,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=103. Generated=5498. Kept=824. proofs=1. Usable=93. Sos=463. Demods=266. Limbo=83, Disabled=190. Hints=0. Kept_by_rule=0, Deleted_by_rule=189. Forward_subsumed=4485. Back_subsumed=11. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=418 (2 lex), Back_demodulated=173. Back_unit_deleted=0. Demod_attempts=69942. Demod_rewrites=13475. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.71. User_CPU=0.12, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11616 exit (max_proofs) Wed Feb 25 09:33:12 2009