%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP512-1 : TPTP v8.1.2. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:23:56 EDT 2024
% Result : Unsatisfiable 65.24s 65.41s
% Output : Refutation 65.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 7
% Syntax : Number of clauses : 66 ( 45 unt; 0 nHn; 19 RR)
% Number of literals : 89 ( 88 equ; 24 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 195 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_these_axioms_4,negated_conjecture,
multiply(a,b) != multiply(b,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_4) ).
cnf(transitivity,axiom,
( X6 != X7
| X7 != X8
| X6 = X8 ),
theory(equality) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c0,axiom,
( X19 != X18
| X21 != X20
| multiply(X19,X21) = multiply(X18,X20) ),
theory(equality) ).
cnf(c10,plain,
( X29 != X28
| multiply(X29,X30) = multiply(X28,X30) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(single_axiom,axiom,
multiply(multiply(multiply(X12,X10),X11),inverse(multiply(X12,X11))) = X10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
cnf(c6,plain,
( X36 != multiply(multiply(multiply(X39,X37),X38),inverse(multiply(X39,X38)))
| X36 = X37 ),
inference(resolution,[status(thm)],[single_axiom,transitivity]) ).
cnf(symmetry,axiom,
( X3 != X4
| X4 = X3 ),
theory(equality) ).
cnf(c5,plain,
X24 = multiply(multiply(multiply(X22,X24),X23),inverse(multiply(X22,X23))),
inference(resolution,[status(thm)],[single_axiom,symmetry]) ).
cnf(c20,plain,
multiply(X68,X69) = multiply(multiply(multiply(multiply(X70,X68),X71),inverse(multiply(X70,X71))),X69),
inference(resolution,[status(thm)],[c10,c5]) ).
cnf(c53,plain,
multiply(X72,inverse(multiply(multiply(X73,X72),inverse(multiply(X73,X74))))) = X74,
inference(resolution,[status(thm)],[c20,c6]) ).
cnf(c61,plain,
( X105 != multiply(X104,inverse(multiply(multiply(X107,X104),inverse(multiply(X107,X106)))))
| X105 = X106 ),
inference(resolution,[status(thm)],[c53,transitivity]) ).
cnf(c21,plain,
multiply(multiply(multiply(multiply(X89,X87),X88),inverse(multiply(X89,X88))),X86) = multiply(X87,X86),
inference(resolution,[status(thm)],[c10,single_axiom]) ).
cnf(c86,plain,
( X238 != multiply(multiply(multiply(multiply(X236,X237),X239),inverse(multiply(X236,X239))),X240)
| X238 = multiply(X237,X240) ),
inference(resolution,[status(thm)],[c21,transitivity]) ).
cnf(c48,plain,
multiply(multiply(X430,X428),X429) = multiply(multiply(multiply(multiply(multiply(X431,X430),X432),inverse(multiply(X431,X432))),X428),X429),
inference(resolution,[status(thm)],[c20,c10]) ).
cnf(c1,axiom,
( X16 != X15
| inverse(X16) = inverse(X15) ),
theory(equality) ).
cnf(c13,plain,
inverse(X49) = inverse(multiply(multiply(multiply(X47,X49),X48),inverse(multiply(X47,X48)))),
inference(resolution,[status(thm)],[c5,c1]) ).
cnf(c31,plain,
( X225 != X224
| multiply(X225,inverse(X227)) = multiply(X224,inverse(multiply(multiply(multiply(X223,X227),X226),inverse(multiply(X223,X226))))) ),
inference(resolution,[status(thm)],[c13,c0]) ).
cnf(c348,plain,
multiply(X367,inverse(X368)) = multiply(X367,inverse(multiply(multiply(multiply(X366,X368),X369),inverse(multiply(X366,X369))))),
inference(resolution,[status(thm)],[c31,reflexivity]) ).
cnf(c621,plain,
multiply(multiply(multiply(multiply(multiply(X370,X372),X373),X371),inverse(multiply(X370,X373))),inverse(X372)) = X371,
inference(resolution,[status(thm)],[c348,c6]) ).
cnf(c636,plain,
( X707 != multiply(multiply(multiply(multiply(multiply(X709,X708),X710),X706),inverse(multiply(X709,X710))),inverse(X708))
| X707 = X706 ),
inference(resolution,[status(thm)],[c621,transitivity]) ).
cnf(c1747,plain,
multiply(multiply(X718,inverse(multiply(X720,X719))),inverse(X718)) = inverse(multiply(X720,X719)),
inference(resolution,[status(thm)],[c636,c48]) ).
cnf(c1788,plain,
inverse(multiply(X721,X723)) = multiply(multiply(X722,inverse(multiply(X721,X723))),inverse(X722)),
inference(resolution,[status(thm)],[c1747,symmetry]) ).
cnf(c1809,plain,
inverse(multiply(X728,X726)) = multiply(X727,inverse(multiply(multiply(X728,X727),X726))),
inference(resolution,[status(thm)],[c1788,c86]) ).
cnf(c1833,plain,
inverse(multiply(X729,inverse(multiply(X729,X730)))) = X730,
inference(resolution,[status(thm)],[c1809,c61]) ).
cnf(c1840,plain,
( X741 != inverse(multiply(X742,inverse(multiply(X742,X743))))
| X741 = X743 ),
inference(resolution,[status(thm)],[c1833,transitivity]) ).
cnf(c58,plain,
inverse(multiply(X101,inverse(multiply(multiply(X103,X101),inverse(multiply(X103,X102)))))) = inverse(X102),
inference(resolution,[status(thm)],[c53,c1]) ).
cnf(c115,plain,
( X286 != inverse(multiply(X287,inverse(multiply(multiply(X288,X287),inverse(multiply(X288,X285))))))
| X286 = inverse(X285) ),
inference(resolution,[status(thm)],[c58,transitivity]) ).
cnf(c1853,plain,
( X890 != X888
| multiply(X890,inverse(multiply(X889,inverse(multiply(X889,X891))))) = multiply(X888,X891) ),
inference(resolution,[status(thm)],[c1833,c0]) ).
cnf(c2727,plain,
multiply(X892,inverse(multiply(X893,inverse(multiply(X893,X894))))) = multiply(X892,X894),
inference(resolution,[status(thm)],[c1853,reflexivity]) ).
cnf(c2768,plain,
multiply(X896,X897) = multiply(X896,inverse(multiply(X895,inverse(multiply(X895,X897))))),
inference(resolution,[status(thm)],[c2727,symmetry]) ).
cnf(c1832,plain,
multiply(X774,inverse(multiply(multiply(X772,X774),X773))) = inverse(multiply(X772,X773)),
inference(resolution,[status(thm)],[c1809,symmetry]) ).
cnf(c2109,plain,
( X1017 != multiply(X1018,inverse(multiply(multiply(X1019,X1018),X1016)))
| X1017 = inverse(multiply(X1019,X1016)) ),
inference(resolution,[status(thm)],[c1832,transitivity]) ).
cnf(c3644,plain,
multiply(X1029,X1030) = inverse(multiply(X1028,inverse(multiply(multiply(X1028,X1029),X1030)))),
inference(resolution,[status(thm)],[c2109,c2768]) ).
cnf(c3723,plain,
multiply(X1032,inverse(multiply(X1032,X1031))) = inverse(X1031),
inference(resolution,[status(thm)],[c3644,c115]) ).
cnf(c3765,plain,
inverse(X1033) = multiply(X1034,inverse(multiply(X1034,X1033))),
inference(resolution,[status(thm)],[c3723,symmetry]) ).
cnf(c3786,plain,
inverse(inverse(X1077)) = inverse(multiply(X1078,inverse(multiply(X1078,X1077)))),
inference(resolution,[status(thm)],[c3765,c1]) ).
cnf(c4111,plain,
inverse(inverse(X1079)) = X1079,
inference(resolution,[status(thm)],[c3786,c1840]) ).
cnf(c4178,plain,
multiply(inverse(inverse(X1109)),X1110) = multiply(X1109,X1110),
inference(resolution,[status(thm)],[c4111,c10]) ).
cnf(c4655,plain,
( X1297 != multiply(inverse(inverse(X1299)),X1298)
| X1297 = multiply(X1299,X1298) ),
inference(resolution,[status(thm)],[c4178,transitivity]) ).
cnf(c4161,plain,
( X1213 != X1212
| multiply(X1213,inverse(inverse(X1214))) = multiply(X1212,X1214) ),
inference(resolution,[status(thm)],[c4111,c0]) ).
cnf(c5614,plain,
multiply(X1215,inverse(inverse(X1216))) = multiply(X1215,X1216),
inference(resolution,[status(thm)],[c4161,reflexivity]) ).
cnf(c5655,plain,
( X1408 != multiply(X1409,inverse(inverse(X1410)))
| X1408 = multiply(X1409,X1410) ),
inference(resolution,[status(thm)],[c5614,transitivity]) ).
cnf(c4144,plain,
( X1082 != inverse(inverse(X1083))
| X1082 = X1083 ),
inference(resolution,[status(thm)],[c4111,transitivity]) ).
cnf(c4221,plain,
multiply(X1124,inverse(multiply(X1124,inverse(X1123)))) = X1123,
inference(resolution,[status(thm)],[c4144,c3723]) ).
cnf(c4784,plain,
( X1359 != multiply(X1361,inverse(multiply(X1361,inverse(X1360))))
| X1359 = X1360 ),
inference(resolution,[status(thm)],[c4221,transitivity]) ).
cnf(c7538,plain,
multiply(multiply(multiply(X1588,X1589),X1590),inverse(X1589)) = multiply(X1588,X1590),
inference(resolution,[status(thm)],[c4784,c348]) ).
cnf(c9734,plain,
multiply(X1722,X1720) = multiply(multiply(multiply(X1722,X1721),X1720),inverse(X1721)),
inference(resolution,[status(thm)],[c7538,symmetry]) ).
cnf(c10551,plain,
multiply(X1768,X1767) = multiply(multiply(multiply(X1768,inverse(X1769)),X1767),X1769),
inference(resolution,[status(thm)],[c9734,c5655]) ).
cnf(c10835,plain,
multiply(multiply(X1956,X1955),inverse(multiply(X1956,inverse(X1957)))) = multiply(X1955,X1957),
inference(resolution,[status(thm)],[c10551,c86]) ).
cnf(c12839,plain,
multiply(X2079,X2078) = multiply(multiply(X2080,X2079),inverse(multiply(X2080,inverse(X2078)))),
inference(resolution,[status(thm)],[c10835,symmetry]) ).
cnf(c64,plain,
X82 = multiply(X80,inverse(multiply(multiply(X81,X80),inverse(multiply(X81,X82))))),
inference(resolution,[status(thm)],[c53,symmetry]) ).
cnf(c73,plain,
multiply(X186,X188) = multiply(multiply(X187,inverse(multiply(multiply(X189,X187),inverse(multiply(X189,X186))))),X188),
inference(resolution,[status(thm)],[c64,c10]) ).
cnf(c268,plain,
multiply(X349,inverse(multiply(X351,inverse(multiply(multiply(X348,multiply(X351,X350)),inverse(multiply(X348,X349))))))) = X350,
inference(resolution,[status(thm)],[c73,c6]) ).
cnf(c599,plain,
X419 = multiply(X417,inverse(multiply(X418,inverse(multiply(multiply(X416,multiply(X418,X419)),inverse(multiply(X416,X417))))))),
inference(resolution,[status(thm)],[c268,symmetry]) ).
cnf(c7545,plain,
X1593 = multiply(multiply(X1591,multiply(X1592,X1593)),inverse(multiply(X1591,X1592))),
inference(resolution,[status(thm)],[c4784,c599]) ).
cnf(c9773,plain,
multiply(multiply(X1733,multiply(X1732,X1734)),inverse(multiply(X1733,X1732))) = X1734,
inference(resolution,[status(thm)],[c7545,symmetry]) ).
cnf(c10621,plain,
( X4738 != multiply(multiply(X4741,multiply(X4739,X4740)),inverse(multiply(X4741,X4739)))
| X4738 = X4740 ),
inference(resolution,[status(thm)],[c9773,transitivity]) ).
cnf(c52729,plain,
multiply(multiply(inverse(X4744),X4743),X4744) = X4743,
inference(resolution,[status(thm)],[c10621,c12839]) ).
cnf(c52985,plain,
X4754 = multiply(multiply(inverse(X4753),X4754),X4753),
inference(resolution,[status(thm)],[c52729,symmetry]) ).
cnf(c53201,plain,
multiply(X5317,X5318) = multiply(multiply(multiply(inverse(X5319),X5317),X5319),X5318),
inference(resolution,[status(thm)],[c52985,c10]) ).
cnf(c62543,plain,
multiply(X5321,inverse(multiply(inverse(X5320),X5320))) = X5321,
inference(resolution,[status(thm)],[c53201,c6]) ).
cnf(c62635,plain,
( X6908 != multiply(X6909,inverse(multiply(inverse(X6910),X6910)))
| X6908 = X6909 ),
inference(resolution,[status(thm)],[c62543,transitivity]) ).
cnf(c91340,plain,
multiply(X6950,X6951) = multiply(inverse(inverse(X6951)),X6950),
inference(resolution,[status(thm)],[c62635,c12839]) ).
cnf(c92085,plain,
multiply(X6953,X6952) = multiply(X6952,X6953),
inference(resolution,[status(thm)],[c91340,c4655]) ).
cnf(c92176,plain,
$false,
inference(resolution,[status(thm)],[c92085,prove_these_axioms_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : GRP512-1 : TPTP v8.1.2. Bugfixed v2.7.0.
% 0.13/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.37 % Computer : n011.cluster.edu
% 0.14/0.37 % Model : x86_64 x86_64
% 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.37 % Memory : 8042.1875MB
% 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.37 % CPULimit : 300
% 0.14/0.37 % WCLimit : 300
% 0.14/0.37 % DateTime : Thu May 9 03:34:38 EDT 2024
% 0.14/0.37 % CPUTime :
% 65.24/65.41 % Version: 1.5
% 65.24/65.41 % SZS status Unsatisfiable
% 65.24/65.41 % SZS output start CNFRefutation
% See solution above
% 65.24/65.42
% 65.24/65.42 % Initial clauses : 7
% 65.24/65.42 % Processed clauses : 1037
% 65.24/65.42 % Factors computed : 2
% 65.24/65.42 % Resolvents computed: 92238
% 65.24/65.42 % Tautologies deleted: 2
% 65.24/65.42 % Forward subsumed : 1531
% 65.24/65.42 % Backward subsumed : 21
% 65.24/65.42 % -------- CPU Time ---------
% 65.24/65.42 % User time : 64.782 s
% 65.24/65.42 % System time : 0.260 s
% 65.24/65.42 % Total time : 65.042 s
%------------------------------------------------------------------------------