============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 26424 was started by mccune on cleo, Fri Apr 13 09:13:51 2007 The command was "/home/mccune/bin/prover9 -f gtsax.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file gtsax.in assign(max_seconds,30). 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 (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 #6 (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 #7 (T,wt=28): 24 ((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 (T,wt=22): 57 x * ((y * ((z * (u * u')) * (v * y))') * (z * x))' = v. [para(24(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(24(a,1),4(a,1,2,1,2))]. given #10 (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 #11 (T,wt=18): 107 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.02 (+ 0.00) seconds: inverse. % Length of proof is 12. % Level of proof is 7. % Maximum clause weight is 29. % Given clauses 11. 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))]. 24 ((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(24(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))]. 107 x * (((y * y') * ((z * z') * x)') * u) = u. [para(39(a,1),9(a,1,2,1,2)),rewrite(101(22))]. 160 x * x' = y * y'. [para(107(a,1),4(a,1,2,1))]. 161 $F # answer(inverse). [resolve(160,a,7,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 6x 7 given #12 (T,wt=9): 160 x * x' = y * y'. [para(107(a,1),4(a,1,2,1))]. given #13 (T,wt=14): 203 x * (y' * ((z * z') * x))' = y. [para(160(a,1),4(a,1,2,1,2,1))]. given #14 (T,wt=14): 224 (x * x')' * ((y * y') * z) = z. [para(160(a,1),107(a,1,2,1))]. given #15 (A,wt=40): 12 x * (((y * (((z * z') * (u * y)') * v))' * (((w * w') * u') * v6))' * (((v7 * v7') * v') * x))' = v6. [para(9(a,1),4(a,1,2,1,2,1,2,1))]. given #16 (F,wt=8): 204 c6 * (x * x') != c6 # answer(identity). [para(160(a,1),8(a,1,2))]. given #17 (F,wt=15): 362 ((x * x') * ((y * y') * c6)')' != c6 # answer(identity). [para(107(a,1),204(a,1))]. given #18 (T,wt=16): 253 (x * x')' * (y' * (z * z'))' = y. [para(160(a,1),203(a,1,2,1,2))]. given #19 (T,wt=16): 278 (x * x')' = (y * y')' * (z * z'). [para(160(a,1),224(a,1,2)),flip(a)]. given #20 (T,wt=11): 419 (x * x')' = (y * y')'. [para(278(a,2),224(a,1))]. given #21 (T,wt=15): 453 (x * x') * (y * y')' = z * z'. [para(419(a,1),160(a,1,2))]. given #22 (A,wt=34): 13 (x * (((y * y') * (z * x)') * u))' = v * ((((w * w') * z') * (v6 * v6')) * (u * v))'. [para(9(a,1),4(a,1,2,1,2,1)),flip(a)]. given #23 (F,wt=14): 458 c6 * ((x * x') * (y * y')') != c6 # answer(identity). [para(419(a,1),204(a,1,2,2))]. given #24 (F,wt=19): 426 c6 * ((x * x') * ((y * y')' * (z * z'))) != c6 # answer(identity). [para(278(a,1),204(a,1,2,2))]. given #25 (F,wt=20): 661 c6 * (((x * x') * (y * y')') * (z * z')') != c6 # answer(identity). [para(419(a,1),458(a,1,2,1,2))]. given #26 (F,wt=20): 662 c6 * ((x * x') * ((y * y') * (z * z')')') != c6 # answer(identity). [para(419(a,1),458(a,1,2,2,1,2))]. given #27 (T,wt=15): 485 ((x * x')' * y) * (z' * y)' = z. [para(453(a,2),11(a,1,1,1,2,2,2,1)),rewrite(164(18))]. given #28 (T,wt=15): 555 (x * x') * y' = (z * z') * y'. [para(13(a,2),39(a,1,2,1,2)),rewrite(4(11))]. given #29 (T,wt=16): 691 x * ((y * y')'' * (z * x))' = z'. [para(485(a,1),4(a,1,2,1,2,1))]. given #30 (T,wt=16): 734 x * (y' * (x' * (z * z'))')' = y. [para(253(a,1),485(a,1,1))]. given #31 (A,wt=40): 14 ((x * (((y * y') * (z * x)') * u))' * (((v * v') * z') * ((w * w') * (v6 * v7)')))' * (v7 * u)' = v6. [para(9(a,1),4(a,1,2,1,2))]. given #32 (F,wt=24): 668 c6 * ((x * x') * (((y * y')' * (z * z')) * (u * u'))) != c6 # answer(identity). [para(278(a,1),426(a,1,2,2,1))]. given #33 (F,wt=29): 1052 c6 * ((x * x') * ((((y * y')' * (z * z')) * (u * u')) * (v * v'))) != c6 # answer(identity). [para(278(a,1),668(a,1,2,2,1,1))]. given #34 (F,wt=34): 1057 c6 * ((x * x') * (((((y * y')' * (z * z')) * (u * u')) * (v * v')) * (w * w'))) != c6 # answer(identity). [para(278(a,1),1052(a,1,2,2,1,1,1))]. given #35 (F,wt=37): 617 c6 * ((x * (((y * y') * (z * x)') * u)) * (v * ((((w * w') * z') * (v6 * v6')) * (u * v))')) != c6 # answer(identity). [para(13(a,1),204(a,1,2,2))]. given #36 (T,wt=9): 889 x * (y * y')' = x. [back_rewrite(742),rewrite(859(6),833(6))]. given #37 (T,wt=10): 920 x'' = x * (y * y'). [back_rewrite(886),rewrite(889(6))]. ============================== PROOF ================================= % Proof 2 at 0.18 (+ 0.00) seconds: identity. % Length of proof is 33. % Level of proof is 18. % Maximum clause weight is 34. % Given clauses 37. 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 * (((y * y') * (z * x)') * u))' = v * ((((w * w') * z') * (v6 * v6')) * (u * v))'. [para(9(a,1),4(a,1,2,1,2,1)),flip(a)]. 24 ((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(24(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))]. 107 x * (((y * y') * ((z * z') * x)') * u) = u. [para(39(a,1),9(a,1,2,1,2)),rewrite(101(22))]. 160 x * x' = y * y'. [para(107(a,1),4(a,1,2,1))]. 164 (x * (((y * y') * (z * x)') * ((u * u') * ((v * v') * w)')))' = w * z. [para(4(a,1),107(a,1,2)),flip(a)]. 203 x * (y' * ((z * z') * x))' = y. [para(160(a,1),4(a,1,2,1,2,1))]. 204 c6 * (x * x') != c6 # answer(identity). [para(160(a,1),8(a,1,2))]. 210 x * (((y * y') * (z * z')) * (u * x))' = u'. [para(160(a,1),10(a,1,2,1,1,1))]. 224 (x * x')' * ((y * y') * z) = z. [para(160(a,1),107(a,1,2,1))]. 253 (x * x')' * (y' * (z * z'))' = y. [para(160(a,1),203(a,1,2,1,2))]. 278 (x * x')' = (y * y')' * (z * z'). [para(160(a,1),224(a,1,2)),flip(a)]. 419 (x * x')' = (y * y')'. [para(278(a,2),224(a,1))]. 453 (x * x') * (y * y')' = z * z'. [para(419(a,1),160(a,1,2))]. 485 ((x * x')' * y) * (z' * y)' = z. [para(453(a,2),11(a,1,1,1,2,2,2,1)),rewrite(164(18))]. 555 (x * x') * y' = (z * z') * y'. [para(13(a,2),39(a,1,2,1,2)),rewrite(4(11))]. 734 x * (y' * (x' * (z * z'))')' = y. [para(253(a,1),485(a,1,1))]. 742 ((x * x')' * y'') * ((z * z') * (u * u')')' = y. [para(453(a,2),485(a,1,2,1))]. 757 ((x * x') * ((y * y') * z')') * (u * u') = z''. [para(555(a,1),24(a,1,1,2,1)),rewrite(210(21))]. 833 (x * x') * (y * z')' = z * y'. [para(4(a,1),734(a,1,2,1)),flip(a)]. 859 (x * x')' * y'' = y. [para(224(a,1),734(a,1,2,1,2,1)),rewrite(833(10))]. 886 x'' = (x * (y * y')') * (z * z'). [back_rewrite(757),rewrite(833(8)),flip(a)]. 889 x * (y * y')' = x. [back_rewrite(742),rewrite(859(6),833(6))]. 920 x'' = x * (y * y'). [back_rewrite(886),rewrite(889(6))]. 1236 x'' = x. [para(920(a,2),203(a,1,2,1)),rewrite(859(8))]. 1253 $F # answer(identity). [para(920(a,2),204(a,1)),rewrite(1236(3)),xx(a)]. ============================== end of proof ========================== % Redundant proof: 1268 $F # answer(identity). [resolve(1267,a,1137,a)]. % Redundant proof: 1269 $F # answer(identity). [resolve(1267,a,204,a)]. % Redundant proof: 1299 $F # answer(identity). [resolve(1298,a,919,a)]. % Redundant proof: 1302 $F # answer(identity). [para(920(a,2),668(a,1,2,2,1)),rewrite(1236(7),1267(9),889(7),1267(4)),xx(a)]. % Redundant proof: 1303 $F # answer(identity). [para(920(a,2),668(a,1,2,2)),rewrite(1267(9),1236(7),889(7),1267(4)),xx(a)]. % Redundant proof: 1304 $F # answer(identity). [para(920(a,2),1052(a,1,2,2,1,1)),rewrite(1236(7),1267(9),1267(9),889(7),1267(4)),xx(a)]. % Redundant proof: 1305 $F # answer(identity). [para(920(a,2),1052(a,1,2,2,1)),rewrite(1267(9),1236(7),1267(9),889(7),1267(4)),xx(a)]. % Redundant proof: 1306 $F # answer(identity). [para(920(a,2),1052(a,1,2,2)),rewrite(1267(9),1267(9),1236(7),889(7),1267(4)),xx(a)]. % Redundant proof: 1307 $F # answer(identity). [para(920(a,2),1057(a,1,2,2,1,1,1)),rewrite(1236(7),1267(9),1267(9),1267(9),889(7),1267(4)),xx(a)]. % Redundant proof: 1308 $F # answer(identity). [para(920(a,2),1057(a,1,2,2,1,1)),rewrite(1267(9),1236(7),1267(9),1267(9),889(7),1267(4)),xx(a)]. % Redundant proof: 1309 $F # answer(identity). [para(920(a,2),1057(a,1,2,2,1)),rewrite(1267(9),1267(9),1236(7),1267(9),889(7),1267(4)),xx(a)]. % Redundant proof: 1310 $F # answer(identity). [para(920(a,2),1057(a,1,2,2)),rewrite(1267(9),1267(9),1267(9),1236(7),889(7),1267(4)),xx(a)]. % Redundant proof: 1317 $F # answer(identity). [para(920(a,2),617(a,1,2,1)),rewrite(1236(3),1267(8),1273(15),1267(4)),xx(a)]. % Redundant proof: 1318 $F # answer(identity). [para(920(a,2),617(a,1,2,2,2,1,1)),rewrite(1236(14),1281(18)),xx(a)]. % Redundant proof: 1323 $F # answer(identity). [resolve(1322,a,1298,a)]. % Redundant proof: 1325 $F # answer(identity). [back_rewrite(1106),rewrite(1288(19),1236(14),1281(18)),xx(a)]. % Redundant proof: 1326 $F # answer(identity). [back_rewrite(1063),rewrite(1267(13),1267(13),889(11),889(9),1267(9),889(7),1267(4)),xx(a)]. % Redundant proof: 1328 $F # answer(identity). [back_rewrite(362),rewrite(1288(8),1236(3)),xx(a)]. % Redundant proof: 1351 $F # answer(identity). [resolve(1350,a,1301,a)]. % Redundant proof: 1357 $F # answer(identity). [resolve(1356,a,1298,a)]. % Redundant proof: 1365 $F # answer(identity). [back_rewrite(1146),rewrite(1267(4),1356(4),1348(6),1236(5),1348(6),1236(5),1348(6),1236(5),1267(6),1267(6),1348(6),1348(3),1348(7),1236(6),1267(7),1356(5),1267(4)),xx(a)]. % Redundant proof: 1369 $F # answer(identity). [back_rewrite(1125),rewrite(1348(8),1236(7),1348(8),1236(7),1267(8),1340(7),1348(6),1236(5),1348(6),1236(5),1267(6),1267(6),1348(6),1348(3),1348(7),1236(6),1267(7),1356(5),1267(4)),xx(a)]. % Redundant proof: 1370 $F # answer(identity). [back_rewrite(1123),rewrite(1267(5),1236(3),1360(5),1356(4),1348(6),1236(5),1348(6),1236(5),1267(6),1267(6),1348(6),1348(3),1348(7),1236(6),1267(7),1356(5),1267(4)),xx(a)]. % Redundant proof: 1432 $F # answer(identity). [back_rewrite(1183),rewrite(1348(5),1392(7),1356(5),1408(6),1356(6),1267(6),1348(6),1236(5),1392(6),1348(5),1236(5),1356(5),1322(4)),xx(a)]. % Redundant proof: 1436 $F # answer(identity). [back_rewrite(1064),rewrite(1348(6),1236(5),1267(8),1267(8),1267(8),1267(8),1267(8),1267(6),1267(4)),xx(a)]. % Redundant proof: 1437 $F # answer(identity). [back_rewrite(1057),rewrite(1348(6),1236(5),1267(8),1267(8),1267(8),1267(8),1267(6),1267(4)),xx(a)]. % Redundant proof: 1438 $F # answer(identity). [back_rewrite(1052),rewrite(1348(6),1236(5),1267(8),1267(8),1267(8),1267(6),1267(4)),xx(a)]. % Redundant proof: 1445 $F # answer(identity). [back_rewrite(673),rewrite(1348(6),1236(5),1348(9),1392(11),1420(9),1356(10),1408(11),1356(11),1267(11),1348(11),1348(9),1236(12),1420(11),1356(12),1442(10),1322(8),1267(6),1267(4)),xx(a)]. % Redundant proof: 1446 $F # answer(identity). [back_rewrite(668),rewrite(1348(6),1236(5),1267(8),1267(8),1267(6),1267(4)),xx(a)]. % Redundant proof: 1448 $F # answer(identity). [back_rewrite(1255),rewrite(1267(6),1430(6),1408(5),1356(5),1236(3)),xx(a)]. % Redundant proof: 1449 $F # answer(identity). [back_rewrite(1254),rewrite(1267(4),1392(6),1408(5),1349(5),1236(3)),xx(a)]. % Redundant proof: 1450 $F # answer(identity). [back_rewrite(1252),rewrite(1267(5),1322(4)),xx(a)]. % Redundant proof: 1452 $F # answer(identity). [back_rewrite(1152),rewrite(1348(5),1392(7),1420(5),1356(6),1267(8),1236(6),1348(6),1236(6),1408(9),1356(9),1267(9),1348(8),1236(8),1442(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1453 $F # answer(identity). [back_rewrite(1149),rewrite(1267(6),1236(4),1348(4),1236(4),1408(7),1356(7),1442(6),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1454 $F # answer(identity). [back_rewrite(1144),rewrite(1348(5),1392(7),1420(5),1356(6),1408(9),1356(9),1267(9),1267(9),1348(8),1236(8),1392(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1457 $F # answer(identity). [resolve(1456,a,1424,a)]. % Redundant proof: 1459 $F # answer(identity). [back_rewrite(1131),rewrite(1348(5),1392(7),1420(5),1356(6),1408(7),1356(7),1348(8),1392(10),1420(8),1356(9),1408(10),1356(10),1267(10),1348(10),1348(8),1236(11),1420(10),1356(11),1442(9),1322(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1460 $F # answer(identity). [back_rewrite(1129),rewrite(1348(5),1392(7),1420(5),1356(6),1348(7),1392(9),1420(7),1356(8),1408(9),1356(9),1267(9),1348(9),1348(7),1236(10),1420(9),1356(10),1442(8),1408(7),1349(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1462 $F # answer(identity). [back_rewrite(1127),rewrite(1348(5),1392(7),1420(5),1356(6),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1348(5),1430(7),1420(5),1356(6),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1463 $F # answer(identity). [back_rewrite(1126),rewrite(1348(5),1392(7),1356(5),1408(8),1356(8),1267(8),1236(6),1392(5),1322(4)),xx(a)]. % Redundant proof: 1464 $F # answer(identity). [back_rewrite(1124),rewrite(1348(5),1392(7),1356(5),1267(6),1236(4),1408(6),1356(6),1267(6),1348(5),1236(5),1356(5),1322(4)),xx(a)]. % Redundant proof: 1465 $F # answer(identity). [back_rewrite(1122),rewrite(1348(5),1392(7),1420(5),1356(6),1348(7),1392(9),1420(7),1356(8),1348(6),1236(6),1408(9),1356(9),1442(8),1348(6),1236(6),1408(9),1356(9),1442(8),1348(6),1236(6),1408(9),1356(9),1267(9),1348(8),1236(8),1442(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1466 $F # answer(identity). [back_rewrite(1119),rewrite(1348(5),1392(7),1420(5),1356(6),1348(4),1236(4),1408(7),1356(7),1442(6),1348(4),1236(4),1408(7),1356(7),1442(6),1348(4),1236(4),1408(7),1356(7),1442(6),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1467 $F # answer(identity). [back_rewrite(1118),rewrite(1348(5),1392(7),1356(5),1392(5),1408(6),1356(6),1267(6),1348(5),1236(5),1356(5),1322(4)),xx(a)]. % Redundant proof: 1468 $F # answer(identity). [back_rewrite(1116),rewrite(1348(5),1392(7),1420(5),1356(6),1392(7),1348(6),1236(6),1408(9),1356(9),1267(9),1348(8),1236(8),1442(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1469 $F # answer(identity). [back_rewrite(1113),rewrite(1392(5),1348(4),1236(4),1408(7),1356(7),1442(6),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1470 $F # answer(identity). [back_rewrite(1112),rewrite(1348(5),1392(7),1420(5),1356(6),1408(8),1356(8),1267(8),1267(8),1236(6),1442(6),1322(4)),xx(a)]. % Redundant proof: 1471 $F # answer(identity). [back_rewrite(1111),rewrite(1267(4),1408(5),1356(5),1267(5),1348(6),1392(8),1348(6),1236(4),1236(4),1348(6),1348(4),1348(4),1236(8),1397(7),1356(5),1267(4)),xx(a)]. % Redundant proof: 1472 $F # answer(identity). [back_rewrite(1110),rewrite(1392(5),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1473 $F # answer(identity). [back_rewrite(1109),rewrite(1408(5),1356(5),1267(5),1348(10),1392(12),1420(10),1356(11),1392(9),1348(7),1236(7),1392(7),1356(5),1348(4),1236(4),1322(4)),xx(a)]. % Redundant proof: 1474 $F # answer(identity). [back_rewrite(1108),rewrite(1348(5),1392(7),1408(12),1356(12),1267(12),1408(10),1356(10),1236(8),1392(7),1359(5),1267(6),1267(4)),xx(a)]. % Redundant proof: 1475 $F # answer(identity). [back_rewrite(1107),rewrite(1348(5),1392(7),1420(5),1356(6),1392(8),1408(7),1356(7),1408(9),1356(9),1267(9),1348(8),1236(8),1442(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1476 $F # answer(identity). [back_rewrite(1105),rewrite(1392(6),1408(5),1356(5),1408(7),1356(7),1442(6),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1477 $F # answer(identity). [back_rewrite(1102),rewrite(1348(5),1392(7),1267(7),1356(5),1267(5),1348(5),1348(4),1408(7),1356(8),1356(6),1236(4),1408(6),1356(6),1267(6),1348(5),1236(5),1356(5),1322(4)),xx(a)]. % Redundant proof: 1478 $F # answer(identity). [back_rewrite(1100),rewrite(1267(4),1348(4),1348(3),1408(6),1356(7),1420(6),1349(5),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1479 $F # answer(identity). [back_rewrite(1099),rewrite(1348(5),1392(7),1420(5),1356(6),1267(6),1348(6),1348(5),1408(8),1356(9),1420(8),1349(7),1348(6),1236(6),1408(9),1356(9),1267(9),1348(8),1236(8),1442(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1481 $F # answer(identity). [back_rewrite(1096),rewrite(1267(4),1348(4),1348(3),1408(6),1356(7),1420(6),1349(5),1348(4),1236(4),1408(7),1356(7),1442(6),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1482 $F # answer(identity). [back_rewrite(1095),rewrite(1348(5),1392(7),1420(5),1356(6),1408(9),1356(9),1348(8),1236(8),1392(8),1267(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1486 $F # answer(identity). [back_rewrite(1091),rewrite(1267(4),1348(5),1392(7),1267(7),1420(5),1356(6),1267(8),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1491 $F # answer(identity). [back_rewrite(1083),rewrite(1348(5),1392(7),1420(5),1356(6),1348(7),1392(9),1267(9),1420(8),1349(7),1348(6),1236(6),1408(9),1356(9),1267(9),1348(8),1236(8),1442(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1492 $F # answer(identity). [back_rewrite(1080),rewrite(1348(5),1392(7),1267(7),1420(6),1349(5),1348(4),1236(4),1408(7),1356(7),1442(6),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1493 $F # answer(identity). [back_rewrite(1079),rewrite(1348(5),1392(7),1420(5),1356(6),1348(7),1392(9),1420(7),1356(8),1348(6),1236(6),1408(9),1356(9),1442(8),1348(6),1236(6),1408(9),1356(9),1267(9),1348(8),1236(8),1442(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1494 $F # answer(identity). [back_rewrite(1076),rewrite(1348(5),1392(7),1420(5),1356(6),1348(4),1236(4),1408(7),1356(7),1442(6),1348(4),1236(4),1408(7),1356(7),1442(6),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1495 $F # answer(identity). [back_rewrite(1075),rewrite(1348(5),1392(7),1408(10),1356(10),1267(10),1348(9),1236(8),1392(9),1420(7),1349(6),1356(5),1322(4)),xx(a)]. % Redundant proof: 1496 $F # answer(identity). [back_rewrite(1074),rewrite(1348(5),1392(7),1420(5),1356(6),1348(7),1392(9),1420(7),1356(8),1348(6),1236(6),1408(9),1356(9),1267(9),1348(8),1236(8),1442(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1497 $F # answer(identity). [back_rewrite(1072),rewrite(1348(5),1392(7),1267(7),1420(6),1349(5),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1498 $F # answer(identity). [back_rewrite(1071),rewrite(1348(5),1392(7),1420(5),1356(6),1348(4),1236(4),1408(7),1356(7),1442(6),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1499 $F # answer(identity). [back_rewrite(1066),rewrite(1348(7),1392(9),1420(7),1356(8),1408(9),1356(9),1267(9),1348(9),1348(7),1236(10),1420(9),1356(10),1442(8),1348(6),1236(6),1267(8),1267(8),1267(8),1267(8),1322(6),1267(4)),xx(a)]. % Redundant proof: 1500 $F # answer(identity). [back_rewrite(1059),rewrite(1348(7),1392(9),1420(7),1356(8),1408(9),1356(9),1267(9),1348(9),1348(7),1236(10),1420(9),1356(10),1442(8),1348(6),1236(6),1267(8),1267(8),1267(8),1322(6),1267(4)),xx(a)]. % Redundant proof: 1501 $F # answer(identity). [back_rewrite(1054),rewrite(1348(7),1392(9),1420(7),1356(8),1408(9),1356(9),1267(9),1348(9),1348(7),1236(10),1420(9),1356(10),1442(8),1348(6),1236(6),1267(8),1267(8),1322(6),1267(4)),xx(a)]. % Redundant proof: 1521 $F # answer(identity). [back_rewrite(672),rewrite(1348(7),1392(9),1420(7),1356(8),1408(9),1356(9),1267(9),1348(9),1348(7),1236(10),1420(9),1356(10),1442(8),1348(6),1236(6),1267(8),1322(6),1267(4)),xx(a)]. % Redundant proof: 1523 $F # answer(identity). [back_rewrite(619),rewrite(1348(6),1392(8),1420(6),1356(7),1408(8),1356(8),1267(8),1348(8),1348(6),1236(9),1420(8),1356(9),1442(7),1430(6),1408(5),1356(5),1236(3)),xx(a)]. % Redundant proof: 1524 $F # answer(identity). [back_rewrite(618),rewrite(1348(4),1392(6),1420(4),1356(5),1408(6),1356(6),1267(6),1348(6),1348(4),1236(7),1420(6),1356(7),1442(5),1392(6),1408(5),1349(5),1236(3)),xx(a)]. % Redundant proof: 1525 $F # answer(identity). [back_rewrite(617),rewrite(1348(5),1392(7),1420(5),1356(6),1408(7),1356(7),1267(7),1348(7),1348(5),1236(8),1420(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1535 $F # answer(identity). [back_rewrite(204),rewrite(1267(4)),xx(a)]. % Redundant proof: 1539 $F # answer(identity). [back_rewrite(1300),rewrite(1348(6),1236(6),1322(6),1267(4)),xx(a)]. % Redundant proof: 1540 $F # answer(identity). [back_rewrite(1314),rewrite(1348(5),1392(7),1527(5),1356(6),1408(7),1356(7),1322(7),1348(7),1348(5),1236(8),1527(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1541 $F # answer(identity). [back_rewrite(1301),rewrite(1322(6),1267(4)),xx(a)]. % Redundant proof: 1542 $F # answer(identity). [back_rewrite(1298),rewrite(1322(4)),xx(a)]. % Redundant proof: 1543 $F # answer(identity). [back_rewrite(1320),rewrite(1348(5),1392(7),1527(5),1356(6),1408(8),1356(8),1236(6),1442(6),1322(4)),xx(a)]. % Redundant proof: 1544 $F # answer(identity). [back_rewrite(1319),rewrite(1348(5),1392(7),1527(5),1356(6),1408(9),1356(9),1348(8),1236(8),1392(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1545 $F # answer(identity). [back_rewrite(1316),rewrite(1348(5),1392(7),1356(5),1408(6),1356(6),1392(6),1348(5),1236(5),1356(5),1322(4)),xx(a)]. % Redundant proof: 1546 $F # answer(identity). [back_rewrite(1312),rewrite(1348(5),1392(7),1527(5),1356(6),1408(7),1349(7),1348(7),1348(5),1236(8),1527(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1547 $F # answer(identity). [back_rewrite(1137),rewrite(1348(5),1392(7),1527(5),1356(6),1348(7),1392(9),1527(7),1356(8),1348(6),1236(6),1442(6),1322(4)),xx(a)]. % Redundant proof: 1548 $F # answer(identity). [back_rewrite(1084),rewrite(1348(6),1348(6),1392(9),1530(7),1356(5),1322(4)),xx(a)]. % Redundant proof: 1550 $F # answer(identity). [back_rewrite(1334),rewrite(1348(4),1348(3),1408(6),1356(7),1356(5),1408(6),1356(6),1392(6),1348(5),1236(5),1356(5),1322(4)),xx(a)]. % Redundant proof: 1551 $F # answer(identity). [back_rewrite(1315),rewrite(1408(7),1356(7),1392(6),1408(7),1356(7),1348(7),1348(5),1236(8),1527(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1552 $F # answer(identity). [back_rewrite(1311),rewrite(1348(5),1430(7),1527(5),1356(6),1408(7),1356(7),1348(7),1348(5),1236(8),1527(7),1356(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1553 $F # answer(identity). [back_rewrite(1142),rewrite(1349(4),1267(4)),xx(a)]. % Redundant proof: 1554 $F # answer(identity). [back_rewrite(1372),rewrite(1392(4),1356(4),1267(4)),xx(a)]. % Redundant proof: 1555 $F # answer(identity). [back_rewrite(1368),rewrite(1527(5),1392(10),1522(9),1442(6),1322(4)),xx(a)]. % Redundant proof: 1556 $F # answer(identity). [back_rewrite(1366),rewrite(1392(7),1527(6),1349(5),1442(6),1322(4)),xx(a)]. % Redundant proof: 1557 $F # answer(identity). [back_rewrite(1364),rewrite(1392(7),1527(5),1356(6),1442(6),1322(4)),xx(a)]. % Redundant proof: 1558 $F # answer(identity). [back_rewrite(1363),rewrite(1392(7),1527(5),1356(6),1527(8),1349(7),1442(6),1322(4)),xx(a)]. % Redundant proof: 1565 $F # answer(identity). [back_rewrite(1435),rewrite(1442(6),1442(6),1322(4)),xx(a)]. % Redundant proof: 1566 $F # answer(identity). [back_rewrite(1434),rewrite(1442(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1567 $F # answer(identity). [back_rewrite(1431),rewrite(1442(6),1322(4)),xx(a)]. % Redundant proof: 1568 $F # answer(identity). [back_rewrite(1488),rewrite(1532(9),1518(8),1322(4)),xx(a)]. % Redundant proof: 1569 $F # answer(identity). [back_rewrite(1487),rewrite(1532(9),1518(8),1442(6),1322(4)),xx(a)]. % Redundant proof: 1570 $F # answer(identity). [back_rewrite(1483),rewrite(1532(11),1518(10),1442(6),1322(4)),xx(a)]. % Redundant proof: 1571 $F # answer(identity). [back_rewrite(1484),rewrite(1522(9),1322(4)),xx(a)]. % Redundant proof: 1572 $F # answer(identity). [back_rewrite(1461),rewrite(1522(9),1442(6),1322(4)),xx(a)]. % Redundant proof: 1573 $F # answer(identity). [back_rewrite(1455),rewrite(1522(11),1442(6),1322(4)),xx(a)]. % Redundant proof: 1576 $F # answer(identity). [back_rewrite(1485),rewrite(1529(11),1532(9),1349(7),1349(5),1267(4)),xx(a)]. % Redundant proof: 1578 $F # answer(identity). [back_rewrite(1489),rewrite(1530(7),1349(5),1322(4)),xx(a)]. % Disable descendants (x means already disabled): 8x 204x 362x 426x 427x 428x 458x 459x 460x 617x 618x 619x 659x 660x 661x 662x 663x 664x 665x 666x 667x 668x 669x 670x 671x 672x 673x 674x 675x 676x 677x 678x 679x 680x 681x 682x 683x 684x 685x 686x 687x 688x 689x 1052x 1053x 1054x 1055x 1056x 1057x 1058x 1059x 1060x 1061x 1062x 1063x 1064x 1065x 1066x 1067x 1068x 1069x 1070x 1071x 1072x 1073x 1074x 1075x 1076x 1077x 1078x 1079x 1080x 1081x 1082x 1083x 1084x 1085x 1086x 1087x 1088x 1089x 1090x 1091x 1092x 1093x 1094x 1095x 1096x 1097x 1098x 1099x 1100x 1101x 1102x 1103x 1104x 1105x 1106x 1107x 1108x 1109x 1110x 1111x 1112x 1113x 1114x 1115x 1116x 1117x 1118x 1119x 1120x 1121x 1122x 1123x 1124x 1125x 1126x 1127x 1128x 1129x 1130x 1131x 1132x 1133x 1134x 1135x 1136x 1137x 1138x 1139x 1140x 1141x 1142x 1143x 1144x 1145x 1146x 1147x 1148x 1149x 1150x 1151x 1152x 1153x 1154x 1183x 1184x 1252x 1254x 1255x 1298x 1300x 1301x 1311x 1312x 1313x 1314x 1315x 1316x 1319x 1320x 1334x 1361x 1362x 1363x 1364x 1366x 1367x 1368x 1371x 1372x 1373x 1374 1431x 1433 1434x 1435x 1451 1455x 1456 1458x 1461x 1480 1483x 1484x 1485x 1487x 1488x 1489x 1490 1562 1563 1577 given #38 (T,wt=5): 1236 x'' = x. [para(920(a,2),203(a,1,2,1)),rewrite(859(8))]. given #39 (T,wt=8): 1267 x * (y * y') = x. [para(419(a,1),920(a,2,2,2)),rewrite(1236(2),889(6)),flip(a)]. given #40 (A,wt=8): 1322 x * (y' * y) = x. [para(920(a,1),920(a,2,2,2)),rewrite(1236(2),1267(4)),flip(a)]. given #41 (T,wt=8): 1349 x' * (x * y) = y. [back_rewrite(1203),rewrite(1348(5),1267(10),1348(8),1348(5),1236(3),1236(3),1348(5),1236(4),1267(5),1348(3),1348(5),1236(3),1236(3))]. given #42 (T,wt=8): 1356 x * (x' * y) = y. [back_rewrite(1193),rewrite(1236(6),1348(9),1348(6),1348(6),1236(3),1348(4),1236(3),1267(4),1348(5),1236(4),1267(5),1348(9),1348(6),1348(6),1236(3),1348(4),1236(3),1267(4),1348(5),1236(5),1354(6))]. given #43 (T,wt=8): 1430 (x' * x) * y = y. [back_rewrite(1238),rewrite(1348(3),1236(2),1267(6),1392(6))]. given #44 (T,wt=9): 1447 x' * x = y * y'. [back_rewrite(626),rewrite(1348(4),1392(6),1420(4),1356(5),1408(6),1356(6),1267(6),1348(6),1348(4),1236(7),1420(6),1356(7),1442(5),1348(3),1236(3),1348(5),1236(4),1267(7))]. given #45 (A,wt=10): 1348 (x * y)' = y' * x'. [back_rewrite(1207),rewrite(1346(5),1327(4),1267(5),1347(6))]. given #46 (T,wt=9): 1581 x' * x = y' * y. [para(1322(a,1),1349(a,1,2))]. given #47 (T,wt=12): 1354 x * ((x' * y) * z) = y * z. [back_rewrite(1195),rewrite(1348(4),1348(7),1348(4),1236(2),1236(2),1348(4),1236(3),1267(4),1236(3),1348(9),1348(7),1348(7),1236(4),1348(5),1236(4),1267(5),1236(5)),flip(a)]. ============================== PROOF ================================= % Proof 3 at 0.31 (+ 0.00) seconds: associativity. % Length of proof is 48. % Level of proof is 24. % Maximum clause weight is 34. % Given clauses 47. 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 * (((y * y') * (z * x)') * u))' = v * ((((w * w') * z') * (v6 * v6')) * (u * v))'. [para(9(a,1),4(a,1,2,1,2,1)),flip(a)]. 24 ((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(24(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))]. 107 x * (((y * y') * ((z * z') * x)') * u) = u. [para(39(a,1),9(a,1,2,1,2)),rewrite(101(22))]. 160 x * x' = y * y'. [para(107(a,1),4(a,1,2,1))]. 164 (x * (((y * y') * (z * x)') * ((u * u') * ((v * v') * w)')))' = w * z. [para(4(a,1),107(a,1,2)),flip(a)]. 203 x * (y' * ((z * z') * x))' = y. [para(160(a,1),4(a,1,2,1,2,1))]. 210 x * (((y * y') * (z * z')) * (u * x))' = u'. [para(160(a,1),10(a,1,2,1,1,1))]. 224 (x * x')' * ((y * y') * z) = z. [para(160(a,1),107(a,1,2,1))]. 253 (x * x')' * (y' * (z * z'))' = y. [para(160(a,1),203(a,1,2,1,2))]. 278 (x * x')' = (y * y')' * (z * z'). [para(160(a,1),224(a,1,2)),flip(a)]. 419 (x * x')' = (y * y')'. [para(278(a,2),224(a,1))]. 453 (x * x') * (y * y')' = z * z'. [para(419(a,1),160(a,1,2))]. 485 ((x * x')' * y) * (z' * y)' = z. [para(453(a,2),11(a,1,1,1,2,2,2,1)),rewrite(164(18))]. 555 (x * x') * y' = (z * z') * y'. [para(13(a,2),39(a,1,2,1,2)),rewrite(4(11))]. 691 x * ((y * y')'' * (z * x))' = z'. [para(485(a,1),4(a,1,2,1,2,1))]. 734 x * (y' * (x' * (z * z'))')' = y. [para(253(a,1),485(a,1,1))]. 742 ((x * x')' * y'') * ((z * z') * (u * u')')' = y. [para(453(a,2),485(a,1,2,1))]. 757 ((x * x') * ((y * y') * z')') * (u * u') = z''. [para(555(a,1),24(a,1,1,2,1)),rewrite(210(21))]. 833 (x * x') * (y * z')' = z * y'. [para(4(a,1),734(a,1,2,1)),flip(a)]. 855 (x' * (((y * y') * ((z * z') * u)')' * (v * v'))')' = u * x. [para(734(a,1),107(a,1,2)),flip(a)]. 859 (x * x')' * y'' = y. [para(224(a,1),734(a,1,2,1,2,1)),rewrite(833(10))]. 886 x'' = (x * (y * y')') * (z * z'). [back_rewrite(757),rewrite(833(8)),flip(a)]. 889 x * (y * y')' = x. [back_rewrite(742),rewrite(859(6),833(6))]. 920 x'' = x * (y * y'). [back_rewrite(886),rewrite(889(6))]. 1195 ((x * x') * (y * z)')' = u * (z''' * (((v * v') * y') * u))'. [para(920(a,2),9(a,1,2,1,1,1)),flip(a)]. 1203 x' * (((y * y') * (x * z)') * (u * u'))''' = z. [para(920(a,2),10(a,1,2,1))]. 1207 ((x * x') * (y * z)')'' = u * ((y * (v * v')) * (z * u))'. [para(920(a,2),24(a,1))]. 1209 ((x * x') * (y * z)') * (u * u') = v * (y'' * (z * v))'. [para(920(a,2),24(a,2,2,1,1))]. 1211 x' * (y * (z * z'))''' = ((u * u') * (y * x)') * (v * v'). [para(920(a,2),24(a,2,2,1)),flip(a)]. 1236 x'' = x. [para(920(a,2),203(a,1,2,1)),rewrite(859(8))]. 1267 x * (y * y') = x. [para(419(a,1),920(a,2,2,2)),rewrite(1236(2),889(6)),flip(a)]. 1288 (x * x') * ((y * y') * z)' = z'. [para(920(a,2),691(a,1,2,1,2)),rewrite(1236(6),1236(6))]. 1327 (x' * y')' = y * x. [back_rewrite(855),rewrite(1288(8),1236(3),1267(4))]. 1346 (x * x') * (y * z)' = z' * y'. [back_rewrite(1211),rewrite(1267(4),1236(3),1267(11)),flip(a)]. 1347 x * (y * (z * x))' = z' * y'. [back_rewrite(1209),rewrite(1346(5),1267(6),1236(5)),flip(a)]. 1348 (x * y)' = y' * x'. [back_rewrite(1207),rewrite(1346(5),1327(4),1267(5),1347(6))]. 1349 x' * (x * y) = y. [back_rewrite(1203),rewrite(1348(5),1267(10),1348(8),1348(5),1236(3),1236(3),1348(5),1236(4),1267(5),1348(3),1348(5),1236(3),1236(3))]. 1354 x * ((x' * y) * z) = y * z. [back_rewrite(1195),rewrite(1348(4),1348(7),1348(4),1236(2),1236(2),1348(4),1236(3),1267(4),1236(3),1348(9),1348(7),1348(7),1236(4),1348(5),1236(4),1267(5),1236(5)),flip(a)]. 1586 (x * y) * z = x * (y * z). [para(1349(a,1),1354(a,1,2,1)),flip(a)]. 1587 $F # answer(associativity). [resolve(1586,a,5,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=47. Generated=3841. Kept=1475. proofs=3. Usable=12. Sos=52. Demods=56. Limbo=2, Disabled=1412. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=2267. Back_subsumed=11. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=866 (0 lex), Back_demodulated=1387. Back_unit_deleted=0. Demod_attempts=108971. Demod_rewrites=20257. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=3.16. User_CPU=0.31, System_CPU=0.00, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 3 proofs. Process 26424 exit (max_proofs) Fri Apr 13 09:13:52 2007