%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP117-1 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:01 EDT 2024
% Result : Unsatisfiable 1.64s 1.83s
% Output : Refutation 1.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 6
% Syntax : Number of clauses : 30 ( 19 unt; 0 nHn; 9 RR)
% Number of literals : 43 ( 42 equ; 14 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 : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 100 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_order3,negated_conjecture,
multiply(a,identity) != a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_order3) ).
cnf(symmetry,axiom,
( X4 != X3
| X3 = X4 ),
theory(equality) ).
cnf(transitivity,axiom,
( X8 != X7
| X7 != X6
| X8 = X6 ),
theory(equality) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c0,axiom,
( X16 != X15
| X17 != X18
| multiply(X16,X17) = multiply(X15,X18) ),
theory(equality) ).
cnf(c7,plain,
( X25 != X27
| multiply(X25,X26) = multiply(X27,X26) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(single_axiom,axiom,
multiply(X11,multiply(multiply(X11,multiply(multiply(X11,X10),X9)),multiply(identity,multiply(X9,X9)))) = X10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
cnf(c5,plain,
( X33 != multiply(X36,multiply(multiply(X36,multiply(multiply(X36,X35),X34)),multiply(identity,multiply(X34,X34))))
| X33 = X35 ),
inference(resolution,[status(thm)],[single_axiom,transitivity]) ).
cnf(c4,plain,
X22 = multiply(X24,multiply(multiply(X24,multiply(multiply(X24,X22),X23)),multiply(identity,multiply(X23,X23)))),
inference(resolution,[status(thm)],[single_axiom,symmetry]) ).
cnf(c16,plain,
multiply(X53,X56) = multiply(multiply(X54,multiply(multiply(X54,multiply(multiply(X54,X53),X55)),multiply(identity,multiply(X55,X55)))),X56),
inference(resolution,[status(thm)],[c7,c4]) ).
cnf(c34,plain,
( X214 != X215
| multiply(X214,multiply(X211,X212)) = multiply(X215,multiply(multiply(X213,multiply(multiply(X213,multiply(multiply(X213,X211),X216)),multiply(identity,multiply(X216,X216)))),X212)) ),
inference(resolution,[status(thm)],[c16,c0]) ).
cnf(c222,plain,
multiply(X227,multiply(X225,X228)) = multiply(X227,multiply(multiply(X226,multiply(multiply(X226,multiply(multiply(X226,X225),X229)),multiply(identity,multiply(X229,X229)))),X228)),
inference(resolution,[status(thm)],[c34,reflexivity]) ).
cnf(c247,plain,
multiply(X230,multiply(X232,multiply(identity,multiply(multiply(identity,multiply(X231,X231)),multiply(identity,multiply(X231,X231)))))) = multiply(multiply(X230,X232),X231),
inference(resolution,[status(thm)],[c222,c5]) ).
cnf(c263,plain,
multiply(multiply(X233,X235),X234) = multiply(X233,multiply(X235,multiply(identity,multiply(multiply(identity,multiply(X234,X234)),multiply(identity,multiply(X234,X234)))))),
inference(resolution,[status(thm)],[c247,symmetry]) ).
cnf(c275,plain,
multiply(multiply(X236,multiply(X236,multiply(multiply(X236,X238),multiply(identity,multiply(X237,X237))))),X237) = X238,
inference(resolution,[status(thm)],[c263,c5]) ).
cnf(c297,plain,
multiply(multiply(multiply(X276,multiply(X276,multiply(multiply(X276,X275),multiply(identity,multiply(X277,X277))))),X277),X278) = multiply(X275,X278),
inference(resolution,[status(thm)],[c275,c7]) ).
cnf(c393,plain,
( X333 != multiply(multiply(multiply(X332,multiply(X332,multiply(multiply(X332,X334),multiply(identity,multiply(X335,X335))))),X335),X331)
| X333 = multiply(X334,X331) ),
inference(resolution,[status(thm)],[c297,transitivity]) ).
cnf(c269,plain,
( X461 != multiply(X463,multiply(X464,multiply(identity,multiply(multiply(identity,multiply(X462,X462)),multiply(identity,multiply(X462,X462))))))
| X461 = multiply(multiply(X463,X464),X462) ),
inference(resolution,[status(thm)],[c247,transitivity]) ).
cnf(c8,plain,
( X40 != X41
| multiply(X40,multiply(X39,multiply(multiply(X39,multiply(multiply(X39,X38),X42)),multiply(identity,multiply(X42,X42))))) = multiply(X41,X38) ),
inference(resolution,[status(thm)],[c0,single_axiom]) ).
cnf(c21,plain,
multiply(X66,multiply(X64,multiply(multiply(X64,multiply(multiply(X64,X65),X67)),multiply(identity,multiply(X67,X67))))) = multiply(X66,X65),
inference(resolution,[status(thm)],[c8,reflexivity]) ).
cnf(c57,plain,
( X491 != X492
| multiply(X491,multiply(X490,multiply(X489,multiply(multiply(X489,multiply(multiply(X489,X488),X487)),multiply(identity,multiply(X487,X487)))))) = multiply(X492,multiply(X490,X488)) ),
inference(resolution,[status(thm)],[c21,c0]) ).
cnf(c984,plain,
multiply(X495,multiply(X497,multiply(X496,multiply(multiply(X496,multiply(multiply(X496,X494),X493)),multiply(identity,multiply(X493,X493)))))) = multiply(X495,multiply(X497,X494)),
inference(resolution,[status(thm)],[c57,reflexivity]) ).
cnf(c1013,plain,
multiply(X501,multiply(X505,X503)) = multiply(X501,multiply(X505,multiply(X504,multiply(multiply(X504,multiply(multiply(X504,X503),X502)),multiply(identity,multiply(X502,X502)))))),
inference(resolution,[status(thm)],[c984,symmetry]) ).
cnf(c1033,plain,
multiply(X507,multiply(X506,X508)) = multiply(multiply(X507,X506),multiply(identity,X508)),
inference(resolution,[status(thm)],[c1013,c269]) ).
cnf(c1075,plain,
( X515 != multiply(X517,multiply(X516,X518))
| X515 = multiply(multiply(X517,X516),multiply(identity,X518)) ),
inference(resolution,[status(thm)],[c1033,transitivity]) ).
cnf(c1135,plain,
X764 = multiply(multiply(X765,multiply(X765,multiply(multiply(X765,X764),X766))),multiply(identity,multiply(identity,multiply(X766,X766)))),
inference(resolution,[status(thm)],[c1075,c4]) ).
cnf(c2300,plain,
X942 = multiply(multiply(multiply(X941,multiply(X941,multiply(multiply(X941,X942),multiply(identity,multiply(X943,X943))))),identity),X943),
inference(resolution,[status(thm)],[c1135,c269]) ).
cnf(c3500,plain,
X944 = multiply(X944,identity),
inference(resolution,[status(thm)],[c2300,c393]) ).
cnf(c3546,plain,
multiply(X945,identity) = X945,
inference(resolution,[status(thm)],[c3500,symmetry]) ).
cnf(c3578,plain,
$false,
inference(resolution,[status(thm)],[c3546,prove_order3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP117-1 : TPTP v8.1.2. Released v1.2.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n003.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 9 04:12:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 1.64/1.83 % Version: 1.5
% 1.64/1.83 % SZS status Unsatisfiable
% 1.64/1.83 % SZS output start CNFRefutation
% See solution above
% 1.64/1.83
% 1.64/1.83 % Initial clauses : 6
% 1.64/1.83 % Processed clauses : 135
% 1.64/1.83 % Factors computed : 2
% 1.64/1.83 % Resolvents computed: 3611
% 1.64/1.83 % Tautologies deleted: 2
% 1.64/1.83 % Forward subsumed : 112
% 1.64/1.83 % Backward subsumed : 1
% 1.64/1.83 % -------- CPU Time ---------
% 1.64/1.83 % User time : 1.463 s
% 1.64/1.83 % System time : 0.022 s
% 1.64/1.83 % Total time : 1.485 s
%------------------------------------------------------------------------------