============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 10640 was started by mccune on cleo.thornwood, Sat Aug 12 20:57:37 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. end_of_list. formulas(sos). (A * B) * C != A * (B * C) # answer(associativity). A * A' != B * B' # answer(inverse). A * (B * B') != A # answer(identity). 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 * z') * (u * y)') * x))' = u. [assumption]. (A * B) * C != A * (B * C) # answer(associativity). [assumption]. A * A' != B * B' # answer(inverse). [assumption]. A * (B * B') != A # answer(identity). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 3). % (Horn set with more than one neg. clause) WARNING, because the following pair of denials share constants, some of the denials or their descendents may be subsumed, preventing the target number of proofs from being found. (A * B) * C != A * (B * C) # answer(associativity). [assumption]. A * A' != B * B' # answer(inverse). [assumption]. WARNING, because the following pair of denials share constants, some of the denials or their descendents may be subsumed, preventing the target number of proofs from being found. (A * B) * C != A * (B * C) # answer(associativity). [assumption]. A * (B * B') != A # answer(identity). [assumption]. WARNING, because the following pair of denials share constants, some of the denials or their descendents may be subsumed, preventing the target number of proofs from being found. A * A' != B * B' # answer(inverse). [assumption]. A * (B * B') != A # answer(identity). [assumption]. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ A, B, C, *, ' ]). 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). 1 x * (y * (((z * z') * (u * y)') * x))' = u. [assumption]. 2 (A * B) * C != A * (B * C) # answer(associativity). [assumption]. 4 B * B' != A * A' # answer(inverse). [copy(3),flip(a)]. 5 A * (B * B') != A # answer(identity). [assumption]. end_of_list. formulas(demodulators). 1 x * (y * (((z * z') * (u * y)') * x))' = u. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=18): 1 x * (y * (((z * z') * (u * y)') * x))' = u. [assumption]. given #2 (I,wt=11): 2 (A * B) * C != A * (B * C) # answer(associativity). [assumption]. given #3 (I,wt=9): 4 B * B' != A * A' # answer(inverse). [copy(3),flip(a)]. given #4 (I,wt=8): 5 A * (B * B') != A # answer(identity). [assumption]. given #5 (T,wt=23): 7 x * ((((y * y') * (z * u)') * (v * v')) * (z * x))' = u. [para(1(a,1),1(a,1,2,1,2,1))]. given #6 (A,wt=29): 6 x * ((y * (((z * z') * (u * y)') * v))' * (((w * w') * u') * x))' = v. [para(1(a,1),1(a,1,2,1,2,1,2,1))]. given #7 (F,wt=28): 10 ((x * x') * (y * z)') * (u * u') = v * ((y * (w * w')) * (z * v))'. [para(7(a,1),1(a,1,2,1,2,1)),flip(a)]. given #8 (F,wt=22): 42 x * ((y * ((z * (u * u')) * (v * y))') * (z * x))' = v. [para(10(a,1),7(a,1,2,1,1))]. given #9 (T,wt=23): 36 (x * x') * (y * (z * ((u * (v * v')) * (y * z))'))' = u. [para(10(a,1),1(a,1,2,1,2))]. given #10 (T,wt=18): 108 x * (((y * y') * ((z * z') * x)') * u) = u. [para(36(a,1),6(a,1,2,1,2)),rewrite(98(22))]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: inverse. % Length of proof is 11. % Level of proof is 7. % Maximum clause weight is 29. % Given clauses 10. 1 x * (y * (((z * z') * (u * y)') * x))' = u. [assumption]. 3 A * A' != B * B' # answer(inverse). [assumption]. 4 B * B' != A * A' # answer(inverse). [copy(3),flip(a)]. 6 x * ((y * (((z * z') * (u * y)') * v))' * (((w * w') * u') * x))' = v. [para(1(a,1),1(a,1,2,1,2,1,2,1))]. 7 x * ((((y * y') * (z * u)') * (v * v')) * (z * x))' = u. [para(1(a,1),1(a,1,2,1,2,1))]. 10 ((x * x') * (y * z)') * (u * u') = v * ((y * (w * w')) * (z * v))'. [para(7(a,1),1(a,1,2,1,2,1)),flip(a)]. 36 (x * x') * (y * (z * ((u * (v * v')) * (y * z))'))' = u. [para(10(a,1),1(a,1,2,1,2))]. 98 (x * (y * ((z * (u * u')) * (x * y))'))' * (v' * z)' = v. [para(36(a,1),1(a,1,2,1,2))]. 108 x * (((y * y') * ((z * z') * x)') * u) = u. [para(36(a,1),6(a,1,2,1,2)),rewrite(98(22))]. 122 x * x' = y * y'. [para(108(a,1),1(a,1,2,1))]. 123 $F # answer(inverse). [resolve(122,a,4,a)]. ============================== end of proof ========================== % Disable descendants: 3x 4 given #11 (A,wt=29): 8 (x * (((y * y') * (z * x)') * ((u * u') * (v * w)')))' * (w * z)' = v. [para(1(a,1),1(a,1,2,1,2))]. given #12 (F,wt=9): 122 x * x' = y * y'. [para(108(a,1),1(a,1,2,1))]. given #13 (F,wt=8): 200 A * (x * x') != A # answer(identity). [para(122(a,1),5(a,1,2))]. given #14 (T,wt=14): 199 x * (y' * ((z * z') * x))' = y. [para(122(a,1),1(a,1,2,1,2,1))]. given #15 (T,wt=14): 215 (x * x')' * ((y * y') * z) = z. [para(122(a,1),108(a,1,2,1))]. given #16 (A,wt=34): 9 x * (((((y * y') * (z * u)') * (v * v')) * (z * w))' * (((v6 * v6') * u') * x))' = w. [para(7(a,1),1(a,1,2,1,2,1,2,1))]. given #17 (F,wt=15): 223 ((x * x') * ((y * y') * A)')' != A # answer(identity). [para(108(a,1),200(a,1))]. given #18 (F,wt=16): 250 (x * x')' * (y' * (z * z'))' = y. [para(122(a,1),199(a,1,2,1,2))]. given #19 (T,wt=16): 275 (x * x')' = (y * y')' * (z * z'). [para(122(a,1),215(a,1,2)),flip(a)]. given #20 (T,wt=11): 404 (x * x')' = (y * y')'. [para(275(a,2),215(a,1))]. given #21 (A,wt=34): 11 ((((x * x') * (y * z)') * (u * u')) * (y * ((v * v') * (w * v6)')))' * (v6 * z)' = w. [para(7(a,1),1(a,1,2,1,2))]. given #22 (F,wt=14): 438 A * ((x * x') * (y * y')') != A # answer(identity). [para(404(a,1),200(a,1,2,2))]. given #23 (F,wt=19): 400 A * ((x * x') * ((y * y')' * (z * z'))) != A # answer(identity). [para(275(a,1),200(a,1,2,2))]. given #24 (T,wt=15): 437 (x * x') * (y * y')' = z * z'. [para(404(a,1),122(a,1,2))]. given #25 (T,wt=15): 558 ((x * x')' * y) * (z' * y)' = z. [para(437(a,2),8(a,1,1,1,2,2,2,1)),rewrite(126(18))]. given #26 (A,wt=34): 12 (x * (((y * y') * (z * x)') * u))' = v * ((((w * w') * z') * (v6 * v6')) * (u * v))'. [para(1(a,1),7(a,1,2,1,1,1,2,1)),flip(a)]. given #27 (F,wt=20): 530 A * (((x * x') * (y * y')') * (z * z')') != A # answer(identity). [para(404(a,1),438(a,1,2,1,2))]. given #28 (F,wt=20): 531 A * ((x * x') * ((y * y') * (z * z')')') != A # answer(identity). [para(404(a,1),438(a,1,2,2,1,2))]. given #29 (T,wt=15): 688 (x * x') * y' = (z * z') * y'. [para(12(a,2),36(a,1,2,1,2)),rewrite(1(11))]. given #30 (T,wt=16): 575 x * ((y * y')'' * (z * x))' = z'. [para(558(a,1),1(a,1,2,1,2,1))]. given #31 (A,wt=34): 13 (x * (((y * y') * (z * x)') * u))' * ((((v * v') * (u * w)') * (v6 * v6')) * z)' = w. [para(1(a,1),7(a,1,2,1,2))]. given #32 (F,wt=21): 443 (((x * x') * (y * y')') * ((z * z') * A)')' != A # answer(identity). [para(404(a,1),223(a,1,1,1,2))]. given #33 (F,wt=21): 444 ((x * x') * (((y * y') * (z * z')') * A)')' != A # answer(identity). [para(404(a,1),223(a,1,1,2,1,1,2))]. given #34 (T,wt=16): 618 x * (y' * (x' * (z * z'))')' = y. [para(250(a,1),558(a,1,1))]. given #35 (T,wt=9): 1119 x * (y * y')' = x. [back_rewrite(632),rewrite(1067(6),1041(6))]. given #36 (A,wt=39): 14 ((((x * x') * (y * z)') * (u * u')) * (y * v))' = w * ((((v6 * v6') * z') * (v7 * v7')) * (v * w))'. [para(7(a,1),7(a,1,2,1,1,1,2,1)),flip(a)]. given #37 (F,wt=24): 535 A * ((x * x') * (((y * y')' * (z * z')) * (u * u'))) != A # answer(identity). [para(275(a,1),400(a,1,2,2,1))]. given #38 (F,wt=29): 1436 A * ((x * x') * ((((y * y')' * (z * z')) * (u * u')) * (v * v'))) != A # answer(identity). [para(275(a,1),535(a,1,2,2,1,1))]. given #39 (T,wt=10): 1164 x'' = x * (y * y'). [back_rewrite(1111),rewrite(1119(6))]. ============================== PROOF ================================= % Proof 2 at 0.23 (+ 0.01) seconds: identity. % Length of proof is 33. % Level of proof is 18. % Maximum clause weight is 34. % Given clauses 39. 1 x * (y * (((z * z') * (u * y)') * x))' = u. [assumption]. 5 A * (B * B') != A # answer(identity). [assumption]. 6 x * ((y * (((z * z') * (u * y)') * v))' * (((w * w') * u') * x))' = v. [para(1(a,1),1(a,1,2,1,2,1,2,1))]. 7 x * ((((y * y') * (z * u)') * (v * v')) * (z * x))' = u. [para(1(a,1),1(a,1,2,1,2,1))]. 8 (x * (((y * y') * (z * x)') * ((u * u') * (v * w)')))' * (w * z)' = v. [para(1(a,1),1(a,1,2,1,2))]. 10 ((x * x') * (y * z)') * (u * u') = v * ((y * (w * w')) * (z * v))'. [para(7(a,1),1(a,1,2,1,2,1)),flip(a)]. 12 (x * (((y * y') * (z * x)') * u))' = v * ((((w * w') * z') * (v6 * v6')) * (u * v))'. [para(1(a,1),7(a,1,2,1,1,1,2,1)),flip(a)]. 36 (x * x') * (y * (z * ((u * (v * v')) * (y * z))'))' = u. [para(10(a,1),1(a,1,2,1,2))]. 98 (x * (y * ((z * (u * u')) * (x * y))'))' * (v' * z)' = v. [para(36(a,1),1(a,1,2,1,2))]. 108 x * (((y * y') * ((z * z') * x)') * u) = u. [para(36(a,1),6(a,1,2,1,2)),rewrite(98(22))]. 122 x * x' = y * y'. [para(108(a,1),1(a,1,2,1))]. 126 (x * (((y * y') * (z * x)') * ((u * u') * ((v * v') * w)')))' = w * z. [para(1(a,1),108(a,1,2)),flip(a)]. 199 x * (y' * ((z * z') * x))' = y. [para(122(a,1),1(a,1,2,1,2,1))]. 200 A * (x * x') != A # answer(identity). [para(122(a,1),5(a,1,2))]. 202 x * (((y * y') * (z * z')) * (u * x))' = u'. [para(122(a,1),7(a,1,2,1,1,1))]. 215 (x * x')' * ((y * y') * z) = z. [para(122(a,1),108(a,1,2,1))]. 250 (x * x')' * (y' * (z * z'))' = y. [para(122(a,1),199(a,1,2,1,2))]. 275 (x * x')' = (y * y')' * (z * z'). [para(122(a,1),215(a,1,2)),flip(a)]. 404 (x * x')' = (y * y')'. [para(275(a,2),215(a,1))]. 437 (x * x') * (y * y')' = z * z'. [para(404(a,1),122(a,1,2))]. 558 ((x * x')' * y) * (z' * y)' = z. [para(437(a,2),8(a,1,1,1,2,2,2,1)),rewrite(126(18))]. 618 x * (y' * (x' * (z * z'))')' = y. [para(250(a,1),558(a,1,1))]. 632 ((x * x')' * y'') * ((z * z') * (u * u')')' = y. [para(437(a,2),558(a,1,2,1))]. 688 (x * x') * y' = (z * z') * y'. [para(12(a,2),36(a,1,2,1,2)),rewrite(1(11))]. 834 ((x * x') * ((y * y') * z')') * (u * u') = z''. [para(688(a,1),10(a,1,1,2,1)),rewrite(202(21))]. 1041 (x * x') * (y * z')' = z * y'. [para(1(a,1),618(a,1,2,1)),flip(a)]. 1067 (x * x')' * y'' = y. [para(215(a,1),618(a,1,2,1,2,1)),rewrite(1041(10))]. 1111 x'' = (x * (y * y')') * (z * z'). [back_rewrite(834),rewrite(1041(8)),flip(a)]. 1119 x * (y * y')' = x. [back_rewrite(632),rewrite(1067(6),1041(6))]. 1164 x'' = x * (y * y'). [back_rewrite(1111),rewrite(1119(6))]. 1505 A'' != A # answer(identity). [para(1164(a,2),200(a,1))]. 1508 x'' = x. [para(1164(a,2),199(a,1,2,1)),rewrite(1067(8))]. 1509 $F # answer(identity). [resolve(1508,a,1505,a)]. ============================== end of proof ========================== % Redundant proof: 1537 $F # answer(identity). [resolve(1536,a,200,a)]. % Redundant proof: 1589 $F # answer(identity). [resolve(1588,a,1129,a)]. % Redundant proof: 1590 $F # answer(identity). [para(1164(a,1),535(a,1,2,2,1,1,1,2)),rewrite(1536(7),1536(9),1536(9),1574(7),1536(4)),xx(a)]. % Redundant proof: 1592 $F # answer(identity). [para(1164(a,2),535(a,1,2,2,1)),rewrite(1508(7),1536(9),1119(7),1536(4)),xx(a)]. % Redundant proof: 1593 $F # answer(identity). [para(1164(a,2),535(a,1,2,2)),rewrite(1536(9),1508(7),1119(7),1536(4)),xx(a)]. % Redundant proof: 1594 $F # answer(identity). [para(1164(a,1),1436(a,1,2,2,1,1,1,1,2)),rewrite(1536(7),1536(9),1536(9),1536(9),1574(7),1536(4)),xx(a)]. % Redundant proof: 1595 $F # answer(identity). [para(1164(a,2),1436(a,1,2,2,1,1)),rewrite(1508(7),1536(9),1536(9),1119(7),1536(4)),xx(a)]. % Redundant proof: 1596 $F # answer(identity). [para(1164(a,2),1436(a,1,2,2,1)),rewrite(1536(9),1508(7),1536(9),1119(7),1536(4)),xx(a)]. % Redundant proof: 1597 $F # answer(identity). [para(1164(a,2),1436(a,1,2,2)),rewrite(1536(9),1536(9),1508(7),1119(7),1536(4)),xx(a)]. % Redundant proof: 1599 $F # answer(identity). [resolve(1598,a,1588,a)]. % Redundant proof: 1602 $F # answer(identity). [back_rewrite(223),rewrite(1563(8),1508(3)),xx(a)]. % Redundant proof: 1615 $F # answer(identity). [back_rewrite(1505),rewrite(1508(3)),xx(a)]. % Redundant proof: 1628 $F # answer(identity). [resolve(1627,a,1588,a)]. % Redundant proof: 1677 $F # answer(identity). [back_rewrite(1445),rewrite(1623(6),1508(5),1536(8),1536(8),1536(8),1536(8),1536(6),1536(4)),xx(a)]. % Redundant proof: 1678 $F # answer(identity). [back_rewrite(1436),rewrite(1623(6),1508(5),1536(8),1536(8),1536(8),1536(6),1536(4)),xx(a)]. % Redundant proof: 1680 $F # answer(identity). [back_rewrite(785),rewrite(1623(6),1508(5),1623(9),1653(11),1634(9),1627(10),1669(11),1627(11),1536(11),1623(11),1623(9),1508(12),1634(11),1627(12),1679(10),1598(8),1536(6),1536(4)),xx(a)]. % Redundant proof: 1684 $F # answer(identity). [back_rewrite(535),rewrite(1623(6),1508(5),1536(8),1536(8),1536(6),1536(4)),xx(a)]. % Redundant proof: 1685 $F # answer(identity). [back_rewrite(1524),rewrite(1536(6),1675(6),1669(5),1627(5),1508(3)),xx(a)]. % Redundant proof: 1686 $F # answer(identity). [back_rewrite(1523),rewrite(1536(4),1653(6),1669(5),1629(5),1508(3)),xx(a)]. % Redundant proof: 1687 $F # answer(identity). [back_rewrite(1504),rewrite(1536(5),1598(4)),xx(a)]. % Redundant proof: 1688 $F # answer(identity). [back_rewrite(1452),rewrite(1623(7),1653(9),1536(9),1634(8),1629(7),1669(9),1627(9),1536(9),1623(9),1623(7),1508(10),1634(9),1627(10),1679(8),1623(6),1508(6),1536(8),1536(8),1536(8),1598(6),1536(4)),xx(a)]. % Redundant proof: 1689 $F # answer(identity). [back_rewrite(1447),rewrite(1623(7),1653(9),1634(7),1627(8),1669(9),1627(9),1536(9),1623(9),1623(7),1508(10),1634(9),1627(10),1679(8),1623(6),1508(6),1536(8),1536(8),1536(8),1598(6),1536(4)),xx(a)]. % Redundant proof: 1690 $F # answer(identity). [back_rewrite(1442),rewrite(1623(7),1653(9),1536(9),1634(8),1629(7),1669(9),1627(9),1536(9),1623(9),1623(7),1508(10),1634(9),1627(10),1679(8),1623(6),1508(6),1536(8),1536(8),1598(6),1536(4)),xx(a)]. % Redundant proof: 1691 $F # answer(identity). [back_rewrite(1438),rewrite(1623(7),1653(9),1634(7),1627(8),1669(9),1627(9),1536(9),1623(9),1623(7),1508(10),1634(9),1627(10),1679(8),1623(6),1508(6),1536(8),1536(8),1598(6),1536(4)),xx(a)]. ============================== PROOF ================================= % Proof 3 at 0.31 (+ 0.01) seconds: associativity. % Length of proof is 66. % Level of proof is 27. % Maximum clause weight is 66. % Given clauses 39. 1 x * (y * (((z * z') * (u * y)') * x))' = u. [assumption]. 2 (A * B) * C != A * (B * C) # answer(associativity). [assumption]. 6 x * ((y * (((z * z') * (u * y)') * v))' * (((w * w') * u') * x))' = v. [para(1(a,1),1(a,1,2,1,2,1,2,1))]. 7 x * ((((y * y') * (z * u)') * (v * v')) * (z * x))' = u. [para(1(a,1),1(a,1,2,1,2,1))]. 8 (x * (((y * y') * (z * x)') * ((u * u') * (v * w)')))' * (w * z)' = v. [para(1(a,1),1(a,1,2,1,2))]. 10 ((x * x') * (y * z)') * (u * u') = v * ((y * (w * w')) * (z * v))'. [para(7(a,1),1(a,1,2,1,2,1)),flip(a)]. 11 ((((x * x') * (y * z)') * (u * u')) * (y * ((v * v') * (w * v6)')))' * (v6 * z)' = w. [para(7(a,1),1(a,1,2,1,2))]. 12 (x * (((y * y') * (z * x)') * u))' = v * ((((w * w') * z') * (v6 * v6')) * (u * v))'. [para(1(a,1),7(a,1,2,1,1,1,2,1)),flip(a)]. 13 (x * (((y * y') * (z * x)') * u))' * ((((v * v') * (u * w)') * (v6 * v6')) * z)' = w. [para(1(a,1),7(a,1,2,1,2))]. 14 ((((x * x') * (y * z)') * (u * u')) * (y * v))' = w * ((((v6 * v6') * z') * (v7 * v7')) * (v * w))'. [para(7(a,1),7(a,1,2,1,1,1,2,1)),flip(a)]. 36 (x * x') * (y * (z * ((u * (v * v')) * (y * z))'))' = u. [para(10(a,1),1(a,1,2,1,2))]. 98 (x * (y * ((z * (u * u')) * (x * y))'))' * (v' * z)' = v. [para(36(a,1),1(a,1,2,1,2))]. 108 x * (((y * y') * ((z * z') * x)') * u) = u. [para(36(a,1),6(a,1,2,1,2)),rewrite(98(22))]. 122 x * x' = y * y'. [para(108(a,1),1(a,1,2,1))]. 126 (x * (((y * y') * (z * x)') * ((u * u') * ((v * v') * w)')))' = w * z. [para(1(a,1),108(a,1,2)),flip(a)]. 199 x * (y' * ((z * z') * x))' = y. [para(122(a,1),1(a,1,2,1,2,1))]. 202 x * (((y * y') * (z * z')) * (u * x))' = u'. [para(122(a,1),7(a,1,2,1,1,1))]. 215 (x * x')' * ((y * y') * z) = z. [para(122(a,1),108(a,1,2,1))]. 250 (x * x')' * (y' * (z * z'))' = y. [para(122(a,1),199(a,1,2,1,2))]. 275 (x * x')' = (y * y')' * (z * z'). [para(122(a,1),215(a,1,2)),flip(a)]. 387 (x * x') * ((y * (z * z')) * (u * u')')'' = y. [para(275(a,2),36(a,1,2,1,2,2,1,2)),rewrite(215(17))]. 404 (x * x')' = (y * y')'. [para(275(a,2),215(a,1))]. 437 (x * x') * (y * y')' = z * z'. [para(404(a,1),122(a,1,2))]. 558 ((x * x')' * y) * (z' * y)' = z. [para(437(a,2),8(a,1,1,1,2,2,2,1)),rewrite(126(18))]. 575 x * ((y * y')'' * (z * x))' = z'. [para(558(a,1),1(a,1,2,1,2,1))]. 618 x * (y' * (x' * (z * z'))')' = y. [para(250(a,1),558(a,1,1))]. 632 ((x * x')' * y'') * ((z * z') * (u * u')')' = y. [para(437(a,2),558(a,1,2,1))]. 688 (x * x') * y' = (z * z') * y'. [para(12(a,2),36(a,1,2,1,2)),rewrite(1(11))]. 834 ((x * x') * ((y * y') * z')') * (u * u') = z''. [para(688(a,1),10(a,1,1,2,1)),rewrite(202(21))]. 856 ((x * x')'' * (y * ((z * z') * (u * v)')))' = w * ((v * y')' * (((v6 * v6') * u') * w))'. [para(575(a,1),6(a,1,2,1,1,1,2)),flip(a)]. 1041 (x * x') * (y * z')' = z * y'. [para(1(a,1),618(a,1,2,1)),flip(a)]. 1058 (x' * (((y * y') * ((z * z') * u)')' * (v * v'))')' = u * x. [para(618(a,1),108(a,1,2)),flip(a)]. 1067 (x * x')' * y'' = y. [para(215(a,1),618(a,1,2,1,2,1)),rewrite(1041(10))]. 1111 x'' = (x * (y * y')') * (z * z'). [back_rewrite(834),rewrite(1041(8)),flip(a)]. 1119 x * (y * y')' = x. [back_rewrite(632),rewrite(1067(6),1041(6))]. 1164 x'' = x * (y * y'). [back_rewrite(1111),rewrite(1119(6))]. 1186 (x * x') * (y * (z * z'))'' = y. [back_rewrite(387),rewrite(1119(9))]. 1355 ((((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(11(a,1),14(a,1,1,2))]. 1368 (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(14(a,2),12(a,1,1,2))]. 1395 ((((x * x') * (y * z)') * (u * u')) * v')' = w * ((((v6 * v6') * z') * (v7 * v7')) * (((v8 * v8')'' * (v * y))' * w))'. [para(575(a,1),14(a,1,1,2))]. 1409 ((((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(13(a,1),14(a,1,1,1,1,2,1))]. 1415 ((((x * x') * y') * (z * z')) * (u * v))' = w * ((((v6 * v6') * (y' * (u' * (v7 * v7'))')'') * (v8 * v8')) * (v * w))'. [para(618(a,1),14(a,1,1,1,1,2,1))]. 1465 x' * (((y * y') * (x * z)') * (u * u'))''' = z. [para(1164(a,2),7(a,1,2,1))]. 1469 x * (((y * y') * (((z * z') * u''') * v))' * (((w * w') * u') * x))' = v. [para(1164(a,2),6(a,1,2,1,1,1,2,1,2,1))]. 1471 ((x * x') * (y * z)')' = u * (z''' * (((v * v') * y') * u))'. [para(1164(a,2),6(a,1,2,1,1,1)),flip(a)]. 1477 ((x * x') * (y * z)')'' = u * ((y * (v * v')) * (z * u))'. [para(1164(a,2),10(a,1))]. 1479 ((x * x') * (y * z)') * (u * u') = v * (y'' * (z * v))'. [para(1164(a,2),10(a,2,2,1,1))]. 1481 x' * (y * (z * z'))''' = ((u * u') * (y * x)') * (v * v'). [para(1164(a,2),10(a,2,2,1)),flip(a)]. 1508 x'' = x. [para(1164(a,2),199(a,1,2,1)),rewrite(1067(8))]. 1536 x * (y * y') = x. [para(404(a,1),1164(a,2,2,2)),rewrite(1508(2),1119(6)),flip(a)]. 1563 (x * x') * ((y * y') * z)' = z'. [para(1164(a,2),575(a,1,2,1,2)),rewrite(1508(6),1508(6))]. 1601 (x' * y')' = y * x. [back_rewrite(1058),rewrite(1563(8),1508(3),1536(4))]. 1621 (x * x') * (y * z)' = z' * y'. [back_rewrite(1481),rewrite(1536(4),1508(3),1536(11)),flip(a)]. 1622 x * (y * (z * x))' = z' * y'. [back_rewrite(1479),rewrite(1621(5),1536(6),1508(5)),flip(a)]. 1623 (x * y)' = y' * x'. [back_rewrite(1477),rewrite(1621(5),1601(4),1536(5),1622(6))]. 1625 x * ((x' * y) * z) = y * z. [back_rewrite(1471),rewrite(1623(4),1623(7),1623(4),1508(2),1508(2),1623(4),1508(3),1536(4),1508(3),1623(9),1623(7),1623(7),1508(4),1623(5),1508(4),1536(5),1508(5)),flip(a)]. 1627 x * (x' * y) = y. [back_rewrite(1469),rewrite(1508(6),1623(9),1623(6),1623(6),1508(3),1623(4),1508(3),1536(4),1623(5),1508(4),1536(5),1623(9),1623(6),1623(6),1508(3),1623(4),1508(3),1536(4),1623(5),1508(5),1625(6))]. 1629 x' * (x * y) = y. [back_rewrite(1465),rewrite(1623(5),1536(10),1623(8),1623(5),1508(3),1508(3),1623(5),1508(4),1536(5),1623(3),1623(5),1508(3),1508(3))]. 1634 (x' * y') * z = x' * (y' * z). [back_rewrite(1415),rewrite(1536(7),1623(7),1623(2),1623(8),1508(5),1623(6),1508(5),1536(6),1536(11),1508(9),1623(9),1508(9),1623(9),1508(9),1536(12),1623(12),1623(6),1623(13),1623(10),1508(10),1623(12),1508(11),1536(12),1625(11))]. 1635 (x' * (y' * z)) * u = x' * ((y' * z) * u). [back_rewrite(1409),rewrite(1536(7),1623(8),1623(13),1623(12),1623(12),1623(9),1508(7),1508(7),1623(9),1508(8),1536(9),1623(12),1623(7),1623(7),1508(3),1623(5),1623(3),1508(6),1634(5),1627(6),1623(9),1508(6),1623(7),1508(6),1536(7),1623(11),1536(16),1623(15),1623(15),1623(12),1508(10),1508(10),1623(12),1508(11),1536(12),1623(11),1623(9),1508(12),1634(11),1536(15),1623(15),1623(7),1623(16),1623(13),1623(11),1508(11),1508(12),1623(14),1508(13),1536(14),1634(12),1627(13))]. 1639 x * (((x' * y) * z) * u) = y * (z * u). [back_rewrite(1395),rewrite(1623(4),1536(9),1623(9),1508(2),1623(7),1623(4),1508(2),1508(2),1623(4),1508(3),1536(4),1536(9),1623(9),1508(8),1623(9),1508(8),1623(11),1623(8),1623(12),1508(11),1536(12),1634(10),1623(12),1623(7),1623(5),1508(5),1508(6),1623(10),1508(7),1623(8),1508(7),1536(8)),flip(a)]. 1653 (x * x') * y = y. [back_rewrite(1186),rewrite(1536(5),1508(4))]. 1669 (x * y) * z' = x * (y * z'). [back_rewrite(856),rewrite(1623(3),1508(2),1623(3),1508(2),1623(6),1653(8),1653(7),1623(5),1623(4),1508(2),1508(2),1623(6),1508(5),1653(9),1623(9),1623(6),1508(6),1623(8),1508(7),1625(9))]. 1697 (x' * (y * (z' * u'))) * u = x' * (y * z'). [back_rewrite(1368),rewrite(1623(4),1653(6),1536(6),1634(5),1629(4),1623(3),1508(3),1623(4),1623(3),1508(3),1669(4),1669(8),1627(8),1536(8),1669(9),1627(9),1536(9),1623(10),1653(12),1623(12),1623(10),1623(9),1508(7),1508(7),1669(8),1508(10),1623(12),1623(10),1623(10),1623(10),1623(9),1508(8),1669(10),1508(14),1635(13),1627(14)),flip(a)]. 1698 (x * y) * z = x * (y * z). [back_rewrite(1355),rewrite(1623(6),1653(8),1536(8),1623(9),1653(11),1634(10),1629(9),1623(8),1623(6),1508(4),1508(4),1508(5),1623(6),1623(6),1623(6),1653(10),1536(10),1697(8),1623(6),1623(4),1508(2),1508(2),1508(3),1669(6),1627(6),1536(6),1623(5),1634(7),1623(9),1623(7),1623(5),1508(5),1508(6),1508(7),1639(7))]. 1699 $F # answer(associativity). [resolve(1698,a,2,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.40. User_CPU=0.31, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 3 proofs. Process 10640 exit (max_proofs) Sat Aug 12 20:57:37 2006