============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3295 was started by mccune on cleo.thornwood, Wed Nov 22 11:21:52 2006 The command was "/home/mccune/bin/prover9 -f gtsax.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file gtsax.in formulas(sos). y * (z * (((u * u') * (x * z)') * y))' = x # label(gt_sax). end_of_list. formulas(goals). (x * y) * z = x * (y * z) # label(associativity). x * x' = y * y' # label(inverse). x * (y * y') = x # label(identity). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (x * y) * z = x * (y * z) # label(associativity) # label(goal). [goal]. 2 x * x' = y * y' # label(inverse) # label(goal). [goal]. 3 x * (y * y') = x # label(identity) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x * (y * (((z * z') * (u * y)') * x))' = u # label(gt_sax). [assumption]. (c1 * c2) * c3 != c1 * (c2 * c3) # label(associativity). [deny(1)]. c4 * c4' != c5 * c5' # label(inverse). [deny(2)]. c6 * (c7 * c7') != c6 # label(identity). [deny(3)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label associativity to answer in negative clause % copying label inverse to answer in negative clause % copying label identity to answer in negative clause % assign(max_proofs, 3). % (Horn set with more than one neg. clause) Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, *, ' ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 4 x * (y * (((z * z') * (u * y)') * x))' = u # label(gt_sax). [assumption]. 5 (c1 * c2) * c3 != c1 * (c2 * c3) # label(associativity) # answer(associativity). [deny(1)]. 7 c5 * c5' != c4 * c4' # answer(inverse). [copy(6),flip(a)]. 8 c6 * (c7 * c7') != c6 # label(identity) # answer(identity). [deny(3)]. end_of_list. formulas(demodulators). 4 x * (y * (((z * z') * (u * y)') * x))' = u # label(gt_sax). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=18): 4 x * (y * (((z * z') * (u * y)') * x))' = u # label(gt_sax). [assumption]. given #2 (I,wt=11): 5 (c1 * c2) * c3 != c1 * (c2 * c3) # label(associativity) # answer(associativity). [deny(1)]. given #3 (I,wt=9): 7 c5 * c5' != c4 * c4' # answer(inverse). [copy(6),flip(a)]. given #4 (I,wt=8): 8 c6 * (c7 * c7') != c6 # label(identity) # answer(identity). [deny(3)]. given #5 (T,wt=23): 10 x * ((((y * y') * (z * u)') * (v * v')) * (z * x))' = u. [para(4(a,1),4(a,1,2,1,2,1))]. given #6 (A,wt=29): 9 x * ((y * (((z * z') * (u * y)') * v))' * (((w * w') * u') * x))' = v. [para(4(a,1),4(a,1,2,1,2,1,2,1))]. given #7 (F,wt=28): 13 ((x * x') * (y * z)') * (u * u') = v * ((y * (w * w')) * (z * v))'. [para(10(a,1),4(a,1,2,1,2,1)),flip(a)]. given #8 (F,wt=22): 45 x * ((y * ((z * (u * u')) * (v * y))') * (z * x))' = v. [para(13(a,1),10(a,1,2,1,1))]. given #9 (T,wt=23): 39 (x * x') * (y * (z * ((u * (v * v')) * (y * z))'))' = u. [para(13(a,1),4(a,1,2,1,2))]. given #10 (T,wt=18): 111 x * (((y * y') * ((z * z') * x)') * u) = u. [para(39(a,1),9(a,1,2,1,2)),rewrite(101(22))]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: inverse. % Length of proof is 12. % Level of proof is 7. % Maximum clause weight is 29. % Given clauses 10. 2 x * x' = y * y' # label(inverse) # label(goal). [goal]. 4 x * (y * (((z * z') * (u * y)') * x))' = u # label(gt_sax). [assumption]. 6 c4 * c4' != c5 * c5' # label(inverse) # answer(inverse). [deny(2)]. 7 c5 * c5' != c4 * c4' # answer(inverse). [copy(6),flip(a)]. 9 x * ((y * (((z * z') * (u * y)') * v))' * (((w * w') * u') * x))' = v. [para(4(a,1),4(a,1,2,1,2,1,2,1))]. 10 x * ((((y * y') * (z * u)') * (v * v')) * (z * x))' = u. [para(4(a,1),4(a,1,2,1,2,1))]. 13 ((x * x') * (y * z)') * (u * u') = v * ((y * (w * w')) * (z * v))'. [para(10(a,1),4(a,1,2,1,2,1)),flip(a)]. 39 (x * x') * (y * (z * ((u * (v * v')) * (y * z))'))' = u. [para(13(a,1),4(a,1,2,1,2))]. 101 (x * (y * ((z * (u * u')) * (x * y))'))' * (v' * z)' = v. [para(39(a,1),4(a,1,2,1,2))]. 111 x * (((y * y') * ((z * z') * x)') * u) = u. [para(39(a,1),9(a,1,2,1,2)),rewrite(101(22))]. 125 x * x' = y * y'. [para(111(a,1),4(a,1,2,1))]. 126 $F # answer(inverse). [resolve(125,a,7,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 6x 7 given #11 (A,wt=29): 11 (x * (((y * y') * (z * x)') * ((u * u') * (v * w)')))' * (w * z)' = v. [para(4(a,1),4(a,1,2,1,2))]. given #12 (F,wt=9): 125 x * x' = y * y'. [para(111(a,1),4(a,1,2,1))]. given #13 (F,wt=8): 203 c6 * (x * x') != c6 # answer(identity). [para(125(a,1),8(a,1,2))]. given #14 (T,wt=14): 202 x * (y' * ((z * z') * x))' = y. [para(125(a,1),4(a,1,2,1,2,1))]. given #15 (T,wt=14): 218 (x * x')' * ((y * y') * z) = z. [para(125(a,1),111(a,1,2,1))]. given #16 (A,wt=34): 12 x * (((((y * y') * (z * u)') * (v * v')) * (z * w))' * (((v6 * v6') * u') * x))' = w. [para(10(a,1),4(a,1,2,1,2,1,2,1))]. given #17 (F,wt=15): 226 ((x * x') * ((y * y') * c6)')' != c6 # answer(identity). [para(111(a,1),203(a,1))]. given #18 (F,wt=16): 253 (x * x')' * (y' * (z * z'))' = y. [para(125(a,1),202(a,1,2,1,2))]. given #19 (T,wt=16): 278 (x * x')' = (y * y')' * (z * z'). [para(125(a,1),218(a,1,2)),flip(a)]. given #20 (T,wt=11): 407 (x * x')' = (y * y')'. [para(278(a,2),218(a,1))]. given #21 (A,wt=34): 14 ((((x * x') * (y * z)') * (u * u')) * (y * ((v * v') * (w * v6)')))' * (v6 * z)' = w. [para(10(a,1),4(a,1,2,1,2))]. given #22 (F,wt=14): 441 c6 * ((x * x') * (y * y')') != c6 # answer(identity). [para(407(a,1),203(a,1,2,2))]. given #23 (F,wt=19): 403 c6 * ((x * x') * ((y * y')' * (z * z'))) != c6 # answer(identity). [para(278(a,1),203(a,1,2,2))]. given #24 (T,wt=15): 440 (x * x') * (y * y')' = z * z'. [para(407(a,1),125(a,1,2))]. given #25 (T,wt=15): 561 ((x * x')' * y) * (z' * y)' = z. [para(440(a,2),11(a,1,1,1,2,2,2,1)),rewrite(129(18))]. given #26 (A,wt=34): 15 (x * (((y * y') * (z * x)') * u))' = v * ((((w * w') * z') * (v6 * v6')) * (u * v))'. [para(4(a,1),10(a,1,2,1,1,1,2,1)),flip(a)]. given #27 (F,wt=20): 533 c6 * (((x * x') * (y * y')') * (z * z')') != c6 # answer(identity). [para(407(a,1),441(a,1,2,1,2))]. given #28 (F,wt=20): 534 c6 * ((x * x') * ((y * y') * (z * z')')') != c6 # answer(identity). [para(407(a,1),441(a,1,2,2,1,2))]. given #29 (T,wt=15): 691 (x * x') * y' = (z * z') * y'. [para(15(a,2),39(a,1,2,1,2)),rewrite(4(11))]. given #30 (T,wt=16): 578 x * ((y * y')'' * (z * x))' = z'. [para(561(a,1),4(a,1,2,1,2,1))]. given #31 (A,wt=34): 16 (x * (((y * y') * (z * x)') * u))' * ((((v * v') * (u * w)') * (v6 * v6')) * z)' = w. [para(4(a,1),10(a,1,2,1,2))]. given #32 (F,wt=21): 446 (((x * x') * (y * y')') * ((z * z') * c6)')' != c6 # answer(identity). [para(407(a,1),226(a,1,1,1,2))]. given #33 (F,wt=21): 447 ((x * x') * (((y * y') * (z * z')') * c6)')' != c6 # answer(identity). [para(407(a,1),226(a,1,1,2,1,1,2))]. given #34 (T,wt=16): 621 x * (y' * (x' * (z * z'))')' = y. [para(253(a,1),561(a,1,1))]. given #35 (T,wt=9): 1122 x * (y * y')' = x. [back_rewrite(635),rewrite(1070(6),1044(6))]. given #36 (A,wt=39): 17 ((((x * x') * (y * z)') * (u * u')) * (y * v))' = w * ((((v6 * v6') * z') * (v7 * v7')) * (v * w))'. [para(10(a,1),10(a,1,2,1,1,1,2,1)),flip(a)]. given #37 (F,wt=24): 538 c6 * ((x * x') * (((y * y')' * (z * z')) * (u * u'))) != c6 # answer(identity). [para(278(a,1),403(a,1,2,2,1))]. given #38 (F,wt=29): 1439 c6 * ((x * x') * ((((y * y')' * (z * z')) * (u * u')) * (v * v'))) != c6 # answer(identity). [para(278(a,1),538(a,1,2,2,1,1))]. given #39 (T,wt=10): 1167 x'' = x * (y * y'). [back_rewrite(1114),rewrite(1122(6))]. ============================== PROOF ================================= % Proof 2 at 0.21 (+ 0.02) seconds: identity. % Length of proof is 34. % Level of proof is 18. % Maximum clause weight is 34. % Given clauses 39. 3 x * (y * y') = x # label(identity) # label(goal). [goal]. 4 x * (y * (((z * z') * (u * y)') * x))' = u # label(gt_sax). [assumption]. 8 c6 * (c7 * c7') != c6 # label(identity) # answer(identity). [deny(3)]. 9 x * ((y * (((z * z') * (u * y)') * v))' * (((w * w') * u') * x))' = v. [para(4(a,1),4(a,1,2,1,2,1,2,1))]. 10 x * ((((y * y') * (z * u)') * (v * v')) * (z * x))' = u. [para(4(a,1),4(a,1,2,1,2,1))]. 11 (x * (((y * y') * (z * x)') * ((u * u') * (v * w)')))' * (w * z)' = v. [para(4(a,1),4(a,1,2,1,2))]. 13 ((x * x') * (y * z)') * (u * u') = v * ((y * (w * w')) * (z * v))'. [para(10(a,1),4(a,1,2,1,2,1)),flip(a)]. 15 (x * (((y * y') * (z * x)') * u))' = v * ((((w * w') * z') * (v6 * v6')) * (u * v))'. [para(4(a,1),10(a,1,2,1,1,1,2,1)),flip(a)]. 39 (x * x') * (y * (z * ((u * (v * v')) * (y * z))'))' = u. [para(13(a,1),4(a,1,2,1,2))]. 101 (x * (y * ((z * (u * u')) * (x * y))'))' * (v' * z)' = v. [para(39(a,1),4(a,1,2,1,2))]. 111 x * (((y * y') * ((z * z') * x)') * u) = u. [para(39(a,1),9(a,1,2,1,2)),rewrite(101(22))]. 125 x * x' = y * y'. [para(111(a,1),4(a,1,2,1))]. 129 (x * (((y * y') * (z * x)') * ((u * u') * ((v * v') * w)')))' = w * z. [para(4(a,1),111(a,1,2)),flip(a)]. 202 x * (y' * ((z * z') * x))' = y. [para(125(a,1),4(a,1,2,1,2,1))]. 203 c6 * (x * x') != c6 # answer(identity). [para(125(a,1),8(a,1,2))]. 205 x * (((y * y') * (z * z')) * (u * x))' = u'. [para(125(a,1),10(a,1,2,1,1,1))]. 218 (x * x')' * ((y * y') * z) = z. [para(125(a,1),111(a,1,2,1))]. 253 (x * x')' * (y' * (z * z'))' = y. [para(125(a,1),202(a,1,2,1,2))]. 278 (x * x')' = (y * y')' * (z * z'). [para(125(a,1),218(a,1,2)),flip(a)]. 407 (x * x')' = (y * y')'. [para(278(a,2),218(a,1))]. 440 (x * x') * (y * y')' = z * z'. [para(407(a,1),125(a,1,2))]. 561 ((x * x')' * y) * (z' * y)' = z. [para(440(a,2),11(a,1,1,1,2,2,2,1)),rewrite(129(18))]. 621 x * (y' * (x' * (z * z'))')' = y. [para(253(a,1),561(a,1,1))]. 635 ((x * x')' * y'') * ((z * z') * (u * u')')' = y. [para(440(a,2),561(a,1,2,1))]. 691 (x * x') * y' = (z * z') * y'. [para(15(a,2),39(a,1,2,1,2)),rewrite(4(11))]. 837 ((x * x') * ((y * y') * z')') * (u * u') = z''. [para(691(a,1),13(a,1,1,2,1)),rewrite(205(21))]. 1044 (x * x') * (y * z')' = z * y'. [para(4(a,1),621(a,1,2,1)),flip(a)]. 1070 (x * x')' * y'' = y. [para(218(a,1),621(a,1,2,1,2,1)),rewrite(1044(10))]. 1114 x'' = (x * (y * y')') * (z * z'). [back_rewrite(837),rewrite(1044(8)),flip(a)]. 1122 x * (y * y')' = x. [back_rewrite(635),rewrite(1070(6),1044(6))]. 1167 x'' = x * (y * y'). [back_rewrite(1114),rewrite(1122(6))]. 1508 c6'' != c6 # answer(identity). [para(1167(a,2),203(a,1))]. 1511 x'' = x. [para(1167(a,2),202(a,1,2,1)),rewrite(1070(8))]. 1512 $F # answer(identity). [resolve(1511,a,1508,a)]. ============================== end of proof ========================== % Redundant proof: 1540 $F # answer(identity). [resolve(1539,a,203,a)]. % Redundant proof: 1592 $F # answer(identity). [resolve(1591,a,1132,a)]. % Redundant proof: 1593 $F # answer(identity). [para(1167(a,1),538(a,1,2,2,1,1,1,2)),rewrite(1539(7),1539(9),1539(9),1577(7),1539(4)),xx(a)]. % Redundant proof: 1595 $F # answer(identity). [para(1167(a,2),538(a,1,2,2,1)),rewrite(1511(7),1539(9),1122(7),1539(4)),xx(a)]. % Redundant proof: 1596 $F # answer(identity). [para(1167(a,2),538(a,1,2,2)),rewrite(1539(9),1511(7),1122(7),1539(4)),xx(a)]. % Redundant proof: 1597 $F # answer(identity). [para(1167(a,1),1439(a,1,2,2,1,1,1,1,2)),rewrite(1539(7),1539(9),1539(9),1539(9),1577(7),1539(4)),xx(a)]. % Redundant proof: 1598 $F # answer(identity). [para(1167(a,2),1439(a,1,2,2,1,1)),rewrite(1511(7),1539(9),1539(9),1122(7),1539(4)),xx(a)]. % Redundant proof: 1599 $F # answer(identity). [para(1167(a,2),1439(a,1,2,2,1)),rewrite(1539(9),1511(7),1539(9),1122(7),1539(4)),xx(a)]. % Redundant proof: 1600 $F # answer(identity). [para(1167(a,2),1439(a,1,2,2)),rewrite(1539(9),1539(9),1511(7),1122(7),1539(4)),xx(a)]. % Redundant proof: 1602 $F # answer(identity). [resolve(1601,a,1591,a)]. % Redundant proof: 1605 $F # answer(identity). [back_rewrite(226),rewrite(1566(8),1511(3)),xx(a)]. % Redundant proof: 1618 $F # answer(identity). [back_rewrite(1508),rewrite(1511(3)),xx(a)]. % Redundant proof: 1631 $F # answer(identity). [resolve(1630,a,1591,a)]. % Redundant proof: 1680 $F # answer(identity). [back_rewrite(1448),rewrite(1626(6),1511(5),1539(8),1539(8),1539(8),1539(8),1539(6),1539(4)),xx(a)]. % Redundant proof: 1681 $F # answer(identity). [back_rewrite(1439),rewrite(1626(6),1511(5),1539(8),1539(8),1539(8),1539(6),1539(4)),xx(a)]. % Redundant proof: 1683 $F # answer(identity). [back_rewrite(788),rewrite(1626(6),1511(5),1626(9),1656(11),1637(9),1630(10),1672(11),1630(11),1539(11),1626(11),1626(9),1511(12),1637(11),1630(12),1682(10),1601(8),1539(6),1539(4)),xx(a)]. % Redundant proof: 1687 $F # answer(identity). [back_rewrite(538),rewrite(1626(6),1511(5),1539(8),1539(8),1539(6),1539(4)),xx(a)]. % Redundant proof: 1688 $F # answer(identity). [back_rewrite(1527),rewrite(1539(6),1678(6),1672(5),1630(5),1511(3)),xx(a)]. % Redundant proof: 1689 $F # answer(identity). [back_rewrite(1526),rewrite(1539(4),1656(6),1672(5),1632(5),1511(3)),xx(a)]. % Redundant proof: 1690 $F # answer(identity). [back_rewrite(1507),rewrite(1539(5),1601(4)),xx(a)]. % Redundant proof: 1691 $F # answer(identity). [back_rewrite(1455),rewrite(1626(7),1656(9),1539(9),1637(8),1632(7),1672(9),1630(9),1539(9),1626(9),1626(7),1511(10),1637(9),1630(10),1682(8),1626(6),1511(6),1539(8),1539(8),1539(8),1601(6),1539(4)),xx(a)]. % Redundant proof: 1692 $F # answer(identity). [back_rewrite(1450),rewrite(1626(7),1656(9),1637(7),1630(8),1672(9),1630(9),1539(9),1626(9),1626(7),1511(10),1637(9),1630(10),1682(8),1626(6),1511(6),1539(8),1539(8),1539(8),1601(6),1539(4)),xx(a)]. % Redundant proof: 1693 $F # answer(identity). [back_rewrite(1445),rewrite(1626(7),1656(9),1539(9),1637(8),1632(7),1672(9),1630(9),1539(9),1626(9),1626(7),1511(10),1637(9),1630(10),1682(8),1626(6),1511(6),1539(8),1539(8),1601(6),1539(4)),xx(a)]. % Redundant proof: 1694 $F # answer(identity). [back_rewrite(1441),rewrite(1626(7),1656(9),1637(7),1630(8),1672(9),1630(9),1539(9),1626(9),1626(7),1511(10),1637(9),1630(10),1682(8),1626(6),1511(6),1539(8),1539(8),1601(6),1539(4)),xx(a)]. ============================== PROOF ================================= % Proof 3 at 0.29 (+ 0.02) seconds: associativity. % Length of proof is 67. % Level of proof is 27. % Maximum clause weight is 66. % Given clauses 39. 1 (x * y) * z = x * (y * z) # label(associativity) # label(goal). [goal]. 4 x * (y * (((z * z') * (u * y)') * x))' = u # label(gt_sax). [assumption]. 5 (c1 * c2) * c3 != c1 * (c2 * c3) # label(associativity) # answer(associativity). [deny(1)]. 9 x * ((y * (((z * z') * (u * y)') * v))' * (((w * w') * u') * x))' = v. [para(4(a,1),4(a,1,2,1,2,1,2,1))]. 10 x * ((((y * y') * (z * u)') * (v * v')) * (z * x))' = u. [para(4(a,1),4(a,1,2,1,2,1))]. 11 (x * (((y * y') * (z * x)') * ((u * u') * (v * w)')))' * (w * z)' = v. [para(4(a,1),4(a,1,2,1,2))]. 13 ((x * x') * (y * z)') * (u * u') = v * ((y * (w * w')) * (z * v))'. [para(10(a,1),4(a,1,2,1,2,1)),flip(a)]. 14 ((((x * x') * (y * z)') * (u * u')) * (y * ((v * v') * (w * v6)')))' * (v6 * z)' = w. [para(10(a,1),4(a,1,2,1,2))]. 15 (x * (((y * y') * (z * x)') * u))' = v * ((((w * w') * z') * (v6 * v6')) * (u * v))'. [para(4(a,1),10(a,1,2,1,1,1,2,1)),flip(a)]. 16 (x * (((y * y') * (z * x)') * u))' * ((((v * v') * (u * w)') * (v6 * v6')) * z)' = w. [para(4(a,1),10(a,1,2,1,2))]. 17 ((((x * x') * (y * z)') * (u * u')) * (y * v))' = w * ((((v6 * v6') * z') * (v7 * v7')) * (v * w))'. [para(10(a,1),10(a,1,2,1,1,1,2,1)),flip(a)]. 39 (x * x') * (y * (z * ((u * (v * v')) * (y * z))'))' = u. [para(13(a,1),4(a,1,2,1,2))]. 101 (x * (y * ((z * (u * u')) * (x * y))'))' * (v' * z)' = v. [para(39(a,1),4(a,1,2,1,2))]. 111 x * (((y * y') * ((z * z') * x)') * u) = u. [para(39(a,1),9(a,1,2,1,2)),rewrite(101(22))]. 125 x * x' = y * y'. [para(111(a,1),4(a,1,2,1))]. 129 (x * (((y * y') * (z * x)') * ((u * u') * ((v * v') * w)')))' = w * z. [para(4(a,1),111(a,1,2)),flip(a)]. 202 x * (y' * ((z * z') * x))' = y. [para(125(a,1),4(a,1,2,1,2,1))]. 205 x * (((y * y') * (z * z')) * (u * x))' = u'. [para(125(a,1),10(a,1,2,1,1,1))]. 218 (x * x')' * ((y * y') * z) = z. [para(125(a,1),111(a,1,2,1))]. 253 (x * x')' * (y' * (z * z'))' = y. [para(125(a,1),202(a,1,2,1,2))]. 278 (x * x')' = (y * y')' * (z * z'). [para(125(a,1),218(a,1,2)),flip(a)]. 390 (x * x') * ((y * (z * z')) * (u * u')')'' = y. [para(278(a,2),39(a,1,2,1,2,2,1,2)),rewrite(218(17))]. 407 (x * x')' = (y * y')'. [para(278(a,2),218(a,1))]. 440 (x * x') * (y * y')' = z * z'. [para(407(a,1),125(a,1,2))]. 561 ((x * x')' * y) * (z' * y)' = z. [para(440(a,2),11(a,1,1,1,2,2,2,1)),rewrite(129(18))]. 578 x * ((y * y')'' * (z * x))' = z'. [para(561(a,1),4(a,1,2,1,2,1))]. 621 x * (y' * (x' * (z * z'))')' = y. [para(253(a,1),561(a,1,1))]. 635 ((x * x')' * y'') * ((z * z') * (u * u')')' = y. [para(440(a,2),561(a,1,2,1))]. 691 (x * x') * y' = (z * z') * y'. [para(15(a,2),39(a,1,2,1,2)),rewrite(4(11))]. 837 ((x * x') * ((y * y') * z')') * (u * u') = z''. [para(691(a,1),13(a,1,1,2,1)),rewrite(205(21))]. 859 ((x * x')'' * (y * ((z * z') * (u * v)')))' = w * ((v * y')' * (((v6 * v6') * u') * w))'. [para(578(a,1),9(a,1,2,1,1,1,2)),flip(a)]. 1044 (x * x') * (y * z')' = z * y'. [para(4(a,1),621(a,1,2,1)),flip(a)]. 1061 (x' * (((y * y') * ((z * z') * u)')' * (v * v'))')' = u * x. [para(621(a,1),111(a,1,2)),flip(a)]. 1070 (x * x')' * y'' = y. [para(218(a,1),621(a,1,2,1,2,1)),rewrite(1044(10))]. 1114 x'' = (x * (y * y')') * (z * z'). [back_rewrite(837),rewrite(1044(8)),flip(a)]. 1122 x * (y * y')' = x. [back_rewrite(635),rewrite(1070(6),1044(6))]. 1167 x'' = x * (y * y'). [back_rewrite(1114),rewrite(1122(6))]. 1189 (x * x') * (y * (z * z'))'' = y. [back_rewrite(390),rewrite(1122(9))]. 1358 ((((x * x') * (((((y * y') * (z * u)') * (v * v')) * (z * ((w * w') * (v6 * v7)')))' * v8)') * (v9 * v9')) * v6)' = v10 * ((((v11 * v11') * v8') * (v12 * v12')) * ((v7 * u)' * v10))'. [para(14(a,1),17(a,1,1,2))]. 1371 (x * ((((y * y') * (z * u)') * (v * v')) * (z * w))')' = v6 * ((((v7 * v7') * v8') * (v9 * v9')) * (((((v10 * v10') * u') * (v11 * v11')) * (w * ((v12 * v12') * (v8 * x)')))' * v6))'. [para(17(a,2),15(a,1,1,2))]. 1398 ((((x * x') * (y * z)') * (u * u')) * v')' = w * ((((v6 * v6') * z') * (v7 * v7')) * (((v8 * v8')'' * (v * y))' * w))'. [para(578(a,1),17(a,1,1,2))]. 1412 ((((x * x') * y') * (z * z')) * ((u * (((v * v') * (w * u)') * v6))' * v7))' = v8 * ((((v9 * v9') * ((((v10 * v10') * (v6 * y)') * (v11 * v11')) * w)'') * (v12 * v12')) * (v7 * v8))'. [para(16(a,1),17(a,1,1,1,1,2,1))]. 1418 ((((x * x') * y') * (z * z')) * (u * v))' = w * ((((v6 * v6') * (y' * (u' * (v7 * v7'))')'') * (v8 * v8')) * (v * w))'. [para(621(a,1),17(a,1,1,1,1,2,1))]. 1468 x' * (((y * y') * (x * z)') * (u * u'))''' = z. [para(1167(a,2),10(a,1,2,1))]. 1472 x * (((y * y') * (((z * z') * u''') * v))' * (((w * w') * u') * x))' = v. [para(1167(a,2),9(a,1,2,1,1,1,2,1,2,1))]. 1474 ((x * x') * (y * z)')' = u * (z''' * (((v * v') * y') * u))'. [para(1167(a,2),9(a,1,2,1,1,1)),flip(a)]. 1480 ((x * x') * (y * z)')'' = u * ((y * (v * v')) * (z * u))'. [para(1167(a,2),13(a,1))]. 1482 ((x * x') * (y * z)') * (u * u') = v * (y'' * (z * v))'. [para(1167(a,2),13(a,2,2,1,1))]. 1484 x' * (y * (z * z'))''' = ((u * u') * (y * x)') * (v * v'). [para(1167(a,2),13(a,2,2,1)),flip(a)]. 1511 x'' = x. [para(1167(a,2),202(a,1,2,1)),rewrite(1070(8))]. 1539 x * (y * y') = x. [para(407(a,1),1167(a,2,2,2)),rewrite(1511(2),1122(6)),flip(a)]. 1566 (x * x') * ((y * y') * z)' = z'. [para(1167(a,2),578(a,1,2,1,2)),rewrite(1511(6),1511(6))]. 1604 (x' * y')' = y * x. [back_rewrite(1061),rewrite(1566(8),1511(3),1539(4))]. 1624 (x * x') * (y * z)' = z' * y'. [back_rewrite(1484),rewrite(1539(4),1511(3),1539(11)),flip(a)]. 1625 x * (y * (z * x))' = z' * y'. [back_rewrite(1482),rewrite(1624(5),1539(6),1511(5)),flip(a)]. 1626 (x * y)' = y' * x'. [back_rewrite(1480),rewrite(1624(5),1604(4),1539(5),1625(6))]. 1628 x * ((x' * y) * z) = y * z. [back_rewrite(1474),rewrite(1626(4),1626(7),1626(4),1511(2),1511(2),1626(4),1511(3),1539(4),1511(3),1626(9),1626(7),1626(7),1511(4),1626(5),1511(4),1539(5),1511(5)),flip(a)]. 1630 x * (x' * y) = y. [back_rewrite(1472),rewrite(1511(6),1626(9),1626(6),1626(6),1511(3),1626(4),1511(3),1539(4),1626(5),1511(4),1539(5),1626(9),1626(6),1626(6),1511(3),1626(4),1511(3),1539(4),1626(5),1511(5),1628(6))]. 1632 x' * (x * y) = y. [back_rewrite(1468),rewrite(1626(5),1539(10),1626(8),1626(5),1511(3),1511(3),1626(5),1511(4),1539(5),1626(3),1626(5),1511(3),1511(3))]. 1637 (x' * y') * z = x' * (y' * z). [back_rewrite(1418),rewrite(1539(7),1626(7),1626(2),1626(8),1511(5),1626(6),1511(5),1539(6),1539(11),1511(9),1626(9),1511(9),1626(9),1511(9),1539(12),1626(12),1626(6),1626(13),1626(10),1511(10),1626(12),1511(11),1539(12),1628(11))]. 1638 (x' * (y' * z)) * u = x' * ((y' * z) * u). [back_rewrite(1412),rewrite(1539(7),1626(8),1626(13),1626(12),1626(12),1626(9),1511(7),1511(7),1626(9),1511(8),1539(9),1626(12),1626(7),1626(7),1511(3),1626(5),1626(3),1511(6),1637(5),1630(6),1626(9),1511(6),1626(7),1511(6),1539(7),1626(11),1539(16),1626(15),1626(15),1626(12),1511(10),1511(10),1626(12),1511(11),1539(12),1626(11),1626(9),1511(12),1637(11),1539(15),1626(15),1626(7),1626(16),1626(13),1626(11),1511(11),1511(12),1626(14),1511(13),1539(14),1637(12),1630(13))]. 1642 x * (((x' * y) * z) * u) = y * (z * u). [back_rewrite(1398),rewrite(1626(4),1539(9),1626(9),1511(2),1626(7),1626(4),1511(2),1511(2),1626(4),1511(3),1539(4),1539(9),1626(9),1511(8),1626(9),1511(8),1626(11),1626(8),1626(12),1511(11),1539(12),1637(10),1626(12),1626(7),1626(5),1511(5),1511(6),1626(10),1511(7),1626(8),1511(7),1539(8)),flip(a)]. 1656 (x * x') * y = y. [back_rewrite(1189),rewrite(1539(5),1511(4))]. 1672 (x * y) * z' = x * (y * z'). [back_rewrite(859),rewrite(1626(3),1511(2),1626(3),1511(2),1626(6),1656(8),1656(7),1626(5),1626(4),1511(2),1511(2),1626(6),1511(5),1656(9),1626(9),1626(6),1511(6),1626(8),1511(7),1628(9))]. 1700 (x' * (y * (z' * u'))) * u = x' * (y * z'). [back_rewrite(1371),rewrite(1626(4),1656(6),1539(6),1637(5),1632(4),1626(3),1511(3),1626(4),1626(3),1511(3),1672(4),1672(8),1630(8),1539(8),1672(9),1630(9),1539(9),1626(10),1656(12),1626(12),1626(10),1626(9),1511(7),1511(7),1672(8),1511(10),1626(12),1626(10),1626(10),1626(10),1626(9),1511(8),1672(10),1511(14),1638(13),1630(14)),flip(a)]. 1701 (x * y) * z = x * (y * z). [back_rewrite(1358),rewrite(1626(6),1656(8),1539(8),1626(9),1656(11),1637(10),1632(9),1626(8),1626(6),1511(4),1511(4),1511(5),1626(6),1626(6),1626(6),1656(10),1539(10),1700(8),1626(6),1626(4),1511(2),1511(2),1511(3),1672(6),1630(6),1539(6),1626(5),1637(7),1626(9),1626(7),1626(5),1511(5),1511(6),1511(7),1642(7))]. 1702 $F # answer(associativity). [resolve(1701,a,5,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=39. Generated=3483. Kept=1671. proofs=3. Usable=21. Sos=680. Demods=530. Limbo=138, Disabled=835. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=1792. Back_subsumed=2. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=977 (0 lex), Back_demodulated=828. Back_unit_deleted=0. Demod_attempts=88703. Demod_rewrites=9918. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.60. User_CPU=0.29, System_CPU=0.02, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 3 proofs. Process 3295 exit (max_proofs) Wed Nov 22 11:21:53 2006