%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP528-1 : TPTP v8.1.2. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:59 EDT 2024
% Result : Unsatisfiable 261.64s 261.88s
% Output : Refutation 261.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 10
% Syntax : Number of clauses : 60 ( 39 unt; 0 nHn; 19 RR)
% Number of literals : 84 ( 83 equ; 25 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 155 ( 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(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c1,axiom,
( X49 != X51
| X52 != X50
| multiply(X49,X52) = multiply(X51,X50) ),
theory(equality) ).
cnf(c56,plain,
( X56 != X57
| multiply(X56,X58) = multiply(X57,X58) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(symmetry,axiom,
( X4 != X3
| X3 = X4 ),
theory(equality) ).
cnf(c0,axiom,
( X35 != X37
| X38 != X36
| divide(X35,X38) = divide(X37,X36) ),
theory(equality) ).
cnf(c29,plain,
( X43 != X42
| divide(X43,X44) = divide(X42,X44) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(inverse,axiom,
inverse(X7) = divide(divide(X6,X6),X7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inverse) ).
cnf(c26,plain,
( X190 != X189
| divide(X190,inverse(X188)) = divide(X189,divide(divide(X191,X191),X188)) ),
inference(resolution,[status(thm)],[c0,inverse]) ).
cnf(c402,plain,
divide(X338,inverse(X336)) = divide(X338,divide(divide(X337,X337),X336)),
inference(resolution,[status(thm)],[c26,reflexivity]) ).
cnf(transitivity,axiom,
( X10 != X8
| X8 != X9
| X10 = X9 ),
theory(equality) ).
cnf(multiply,axiom,
multiply(X23,X22) = divide(X23,divide(divide(X24,X24),X22)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiply) ).
cnf(c17,plain,
divide(X107,divide(divide(X106,X106),X108)) = multiply(X107,X108),
inference(resolution,[status(thm)],[multiply,symmetry]) ).
cnf(c173,plain,
( X1673 != divide(X1674,divide(divide(X1672,X1672),X1671))
| X1673 = multiply(X1674,X1671) ),
inference(resolution,[status(thm)],[c17,transitivity]) ).
cnf(c11176,plain,
divide(X1681,inverse(X1682)) = multiply(X1681,X1682),
inference(resolution,[status(thm)],[c173,c402]) ).
cnf(c11276,plain,
multiply(X1688,X1689) = divide(X1688,inverse(X1689)),
inference(resolution,[status(thm)],[c11176,symmetry]) ).
cnf(c11385,plain,
divide(multiply(X3347,X3348),X3349) = divide(divide(X3347,inverse(X3348)),X3349),
inference(resolution,[status(thm)],[c11276,c29]) ).
cnf(c4,plain,
divide(divide(X20,X20),X21) = inverse(X21),
inference(resolution,[status(thm)],[inverse,symmetry]) ).
cnf(c13,plain,
( X62 != divide(divide(X61,X61),X63)
| X62 = inverse(X63) ),
inference(resolution,[status(thm)],[c4,transitivity]) ).
cnf(single_axiom,axiom,
divide(X12,divide(divide(X12,X11),divide(X13,X11))) = X13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
cnf(c8,plain,
( X67 != divide(X66,divide(divide(X66,X65),divide(X64,X65)))
| X67 = X64 ),
inference(resolution,[status(thm)],[single_axiom,transitivity]) ).
cnf(c1028,plain,
divide(X339,inverse(divide(X340,X339))) = X340,
inference(resolution,[status(thm)],[c402,c8]) ).
cnf(c1041,plain,
X344 = divide(X345,inverse(divide(X344,X345))),
inference(resolution,[status(thm)],[c1028,symmetry]) ).
cnf(c1084,plain,
X349 = inverse(inverse(divide(X349,divide(X348,X348)))),
inference(resolution,[status(thm)],[c1041,c13]) ).
cnf(c1096,plain,
inverse(inverse(divide(X350,divide(X351,X351)))) = X350,
inference(resolution,[status(thm)],[c1084,symmetry]) ).
cnf(c1106,plain,
( X577 != inverse(inverse(divide(X576,divide(X578,X578))))
| X577 = X576 ),
inference(resolution,[status(thm)],[c1096,transitivity]) ).
cnf(c2,axiom,
( X17 != X18
| inverse(X17) = inverse(X18) ),
theory(equality) ).
cnf(c9,plain,
X32 = divide(X34,divide(divide(X34,X33),divide(X32,X33))),
inference(resolution,[status(thm)],[single_axiom,symmetry]) ).
cnf(c24,plain,
inverse(X172) = inverse(divide(X170,divide(divide(X170,X171),divide(X172,X171)))),
inference(resolution,[status(thm)],[c9,c2]) ).
cnf(c345,plain,
inverse(inverse(X4141)) = inverse(inverse(divide(X4140,divide(divide(X4140,X4142),divide(X4141,X4142))))),
inference(resolution,[status(thm)],[c24,c2]) ).
cnf(c38091,plain,
inverse(inverse(X4143)) = X4143,
inference(resolution,[status(thm)],[c345,c1106]) ).
cnf(c38216,plain,
( X4197 != inverse(inverse(X4196))
| X4197 = X4196 ),
inference(resolution,[status(thm)],[c38091,transitivity]) ).
cnf(c39184,plain,
divide(divide(X4276,X4276),inverse(X4277)) = X4277,
inference(resolution,[status(thm)],[c38216,c4]) ).
cnf(c41371,plain,
( X6081 != divide(divide(X6080,X6080),inverse(X6079))
| X6081 = X6079 ),
inference(resolution,[status(thm)],[c39184,transitivity]) ).
cnf(c31,plain,
( X266 != X263
| divide(X266,X264) = divide(X263,divide(X265,divide(divide(X265,X267),divide(X264,X267)))) ),
inference(resolution,[status(thm)],[c0,c9]) ).
cnf(c671,plain,
divide(X8844,X8843) = divide(X8844,divide(X8842,divide(divide(X8842,X8841),divide(X8843,X8841)))),
inference(resolution,[status(thm)],[c31,reflexivity]) ).
cnf(c126197,plain,
divide(X10300,X10302) = divide(divide(X10300,divide(X10302,X10301)),X10301),
inference(resolution,[status(thm)],[c671,c8]) ).
cnf(c154364,plain,
divide(divide(X10309,inverse(X10308)),X10309) = X10308,
inference(resolution,[status(thm)],[c126197,c41371]) ).
cnf(c154854,plain,
( X11237 != divide(divide(X11236,inverse(X11235)),X11236)
| X11237 = X11235 ),
inference(resolution,[status(thm)],[c154364,transitivity]) ).
cnf(c176448,plain,
divide(multiply(X11253,X11254),X11253) = X11254,
inference(resolution,[status(thm)],[c154854,c11385]) ).
cnf(c178064,plain,
X11267 = divide(multiply(X11268,X11267),X11268),
inference(resolution,[status(thm)],[c176448,symmetry]) ).
cnf(c179456,plain,
multiply(X12718,X12716) = multiply(divide(multiply(X12717,X12718),X12717),X12716),
inference(resolution,[status(thm)],[c178064,c56]) ).
cnf(c11261,plain,
( X1798 != divide(X1796,inverse(X1797))
| X1798 = multiply(X1796,X1797) ),
inference(resolution,[status(thm)],[c11176,transitivity]) ).
cnf(c38,plain,
divide(inverse(X240),X241) = divide(divide(divide(X242,X242),X240),X241),
inference(resolution,[status(thm)],[c29,inverse]) ).
cnf(c526,plain,
inverse(divide(inverse(X6641),X6639)) = inverse(divide(divide(divide(X6640,X6640),X6641),X6639)),
inference(resolution,[status(thm)],[c38,c2]) ).
cnf(c78,plain,
inverse(divide(divide(divide(X274,X274),X275),divide(X276,X275))) = X276,
inference(resolution,[status(thm)],[c8,inverse]) ).
cnf(c713,plain,
( X9449 != inverse(divide(divide(divide(X9447,X9447),X9448),divide(X9446,X9448)))
| X9449 = X9446 ),
inference(resolution,[status(thm)],[c78,transitivity]) ).
cnf(c137762,plain,
inverse(divide(inverse(X9491),divide(X9490,X9491))) = X9490,
inference(resolution,[status(thm)],[c713,c526]) ).
cnf(c138084,plain,
X9492 = inverse(divide(inverse(X9493),divide(X9492,X9493))),
inference(resolution,[status(thm)],[c137762,symmetry]) ).
cnf(c154441,plain,
divide(divide(X10311,X10310),X10311) = inverse(X10310),
inference(resolution,[status(thm)],[c126197,c13]) ).
cnf(c155011,plain,
( X11594 != divide(divide(X11592,X11593),X11592)
| X11594 = inverse(X11593) ),
inference(resolution,[status(thm)],[c154441,transitivity]) ).
cnf(c189818,plain,
divide(X11627,X11628) = inverse(divide(X11628,X11627)),
inference(resolution,[status(thm)],[c155011,c126197]) ).
cnf(c190872,plain,
inverse(divide(X11653,X11652)) = divide(X11652,X11653),
inference(resolution,[status(thm)],[c189818,symmetry]) ).
cnf(c191333,plain,
( X13568 != inverse(divide(X13569,X13567))
| X13568 = divide(X13567,X13569) ),
inference(resolution,[status(thm)],[c190872,transitivity]) ).
cnf(c259090,plain,
X13609 = divide(divide(X13609,X13610),inverse(X13610)),
inference(resolution,[status(thm)],[c191333,c138084]) ).
cnf(c259907,plain,
X13622 = multiply(divide(X13622,X13621),X13621),
inference(resolution,[status(thm)],[c259090,c11261]) ).
cnf(c260195,plain,
multiply(divide(X13631,X13632),X13632) = X13631,
inference(resolution,[status(thm)],[c259907,symmetry]) ).
cnf(c260597,plain,
( X13812 != multiply(divide(X13811,X13810),X13810)
| X13812 = X13811 ),
inference(resolution,[status(thm)],[c260195,transitivity]) ).
cnf(c268506,plain,
multiply(X13874,X13875) = multiply(X13875,X13874),
inference(resolution,[status(thm)],[c260597,c179456]) ).
cnf(c269424,plain,
$false,
inference(resolution,[status(thm)],[c268506,prove_these_axioms_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP528-1 : TPTP v8.1.2. Bugfixed v2.7.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n026.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 04:39:23 EDT 2024
% 0.14/0.34 % CPUTime :
% 261.64/261.88 % Version: 1.5
% 261.64/261.88 % SZS status Unsatisfiable
% 261.64/261.88 % SZS output start CNFRefutation
% See solution above
% 261.64/261.88
% 261.64/261.88 % Initial clauses : 10
% 261.64/261.88 % Processed clauses : 1781
% 261.64/261.88 % Factors computed : 3
% 261.64/261.88 % Resolvents computed: 269761
% 261.64/261.88 % Tautologies deleted: 2
% 261.64/261.88 % Forward subsumed : 3635
% 261.64/261.88 % Backward subsumed : 8
% 261.64/261.88 % -------- CPU Time ---------
% 261.64/261.88 % User time : 260.885 s
% 261.64/261.88 % System time : 0.634 s
% 261.64/261.88 % Total time : 261.519 s
%------------------------------------------------------------------------------