%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP526-1 : TPTP v8.1.2. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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:58 EDT 2024
% Result : Unsatisfiable 15.26s 15.43s
% Output : Refutation 15.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 9
% Syntax : Number of clauses : 37 ( 25 unt; 0 nHn; 12 RR)
% Number of literals : 51 ( 50 equ; 15 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 : 89 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_these_axioms_2,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_2) ).
cnf(symmetry,axiom,
( X4 != X3
| X3 = X4 ),
theory(equality) ).
cnf(transitivity,axiom,
( X9 != X8
| X8 != X10
| X9 = X10 ),
theory(equality) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(inverse,axiom,
inverse(X7) = divide(divide(X6,X6),X7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inverse) ).
cnf(c0,axiom,
( X36 != X35
| X37 != X38
| divide(X36,X37) = divide(X35,X38) ),
theory(equality) ).
cnf(c30,plain,
( X247 != X248
| divide(X247,inverse(X250)) = divide(X248,divide(divide(X249,X249),X250)) ),
inference(resolution,[status(thm)],[c0,inverse]) ).
cnf(c555,plain,
divide(X349,inverse(X348)) = divide(X349,divide(divide(X350,X350),X348)),
inference(resolution,[status(thm)],[c30,reflexivity]) ).
cnf(multiply,axiom,
multiply(X24,X22) = divide(X24,divide(divide(X23,X23),X22)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiply) ).
cnf(c17,plain,
divide(X106,divide(divide(X108,X108),X107)) = multiply(X106,X107),
inference(resolution,[status(thm)],[multiply,symmetry]) ).
cnf(c172,plain,
( X1659 != divide(X1660,divide(divide(X1661,X1661),X1658))
| X1659 = multiply(X1660,X1658) ),
inference(resolution,[status(thm)],[c17,transitivity]) ).
cnf(c11286,plain,
divide(X1683,inverse(X1684)) = multiply(X1683,X1684),
inference(resolution,[status(thm)],[c172,c555]) ).
cnf(c11370,plain,
( X1811 != divide(X1812,inverse(X1810))
| X1811 = multiply(X1812,X1810) ),
inference(resolution,[status(thm)],[c11286,transitivity]) ).
cnf(c4,plain,
divide(divide(X21,X21),X20) = inverse(X20),
inference(resolution,[status(thm)],[inverse,symmetry]) ).
cnf(c13,plain,
( X62 != divide(divide(X63,X63),X61)
| X62 = inverse(X61) ),
inference(resolution,[status(thm)],[c4,transitivity]) ).
cnf(c29,plain,
( X42 != X43
| divide(X42,X44) = divide(X43,X44) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c11347,plain,
multiply(X1692,X1691) = divide(X1692,inverse(X1691)),
inference(resolution,[status(thm)],[c11286,symmetry]) ).
cnf(c11464,plain,
divide(multiply(X3289,X3291),X3290) = divide(divide(X3289,inverse(X3291)),X3290),
inference(resolution,[status(thm)],[c11347,c29]) ).
cnf(c28028,plain,
divide(multiply(inverse(X3293),X3293),X3292) = inverse(X3292),
inference(resolution,[status(thm)],[c11464,c13]) ).
cnf(c28105,plain,
inverse(X3300) = divide(multiply(inverse(X3299),X3299),X3300),
inference(resolution,[status(thm)],[c28028,symmetry]) ).
cnf(c28574,plain,
inverse(inverse(X3307)) = multiply(multiply(inverse(X3308),X3308),X3307),
inference(resolution,[status(thm)],[c28105,c11370]) ).
cnf(c28647,plain,
multiply(multiply(inverse(X3321),X3321),X3320) = inverse(inverse(X3320)),
inference(resolution,[status(thm)],[c28574,symmetry]) ).
cnf(single_axiom,axiom,
divide(X13,divide(divide(X13,X11),divide(X12,X11))) = X12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
cnf(c8,plain,
( X64 != divide(X65,divide(divide(X65,X66),divide(X67,X66)))
| X64 = X67 ),
inference(resolution,[status(thm)],[single_axiom,transitivity]) ).
cnf(c1052,plain,
divide(X352,inverse(divide(X351,X352))) = X351,
inference(resolution,[status(thm)],[c555,c8]) ).
cnf(c1065,plain,
X353 = divide(X354,inverse(divide(X353,X354))),
inference(resolution,[status(thm)],[c1052,symmetry]) ).
cnf(c1095,plain,
X362 = inverse(inverse(divide(X362,divide(X361,X361)))),
inference(resolution,[status(thm)],[c1065,c13]) ).
cnf(c1123,plain,
inverse(inverse(divide(X363,divide(X364,X364)))) = X363,
inference(resolution,[status(thm)],[c1095,symmetry]) ).
cnf(c1154,plain,
( X587 != inverse(inverse(divide(X588,divide(X586,X586))))
| X587 = X588 ),
inference(resolution,[status(thm)],[c1123,transitivity]) ).
cnf(c2,axiom,
( X18 != X17
| inverse(X18) = inverse(X17) ),
theory(equality) ).
cnf(c9,plain,
X32 = divide(X33,divide(divide(X33,X34),divide(X32,X34))),
inference(resolution,[status(thm)],[single_axiom,symmetry]) ).
cnf(c23,plain,
inverse(X154) = inverse(divide(X156,divide(divide(X156,X155),divide(X154,X155)))),
inference(resolution,[status(thm)],[c9,c2]) ).
cnf(c301,plain,
inverse(inverse(X3483)) = inverse(inverse(divide(X3484,divide(divide(X3484,X3482),divide(X3483,X3482))))),
inference(resolution,[status(thm)],[c23,c2]) ).
cnf(c31216,plain,
inverse(inverse(X3485)) = X3485,
inference(resolution,[status(thm)],[c301,c1154]) ).
cnf(c31357,plain,
( X3540 != inverse(inverse(X3541))
| X3540 = X3541 ),
inference(resolution,[status(thm)],[c31216,transitivity]) ).
cnf(c32716,plain,
multiply(multiply(inverse(X3615),X3615),X3616) = X3616,
inference(resolution,[status(thm)],[c31357,c28647]) ).
cnf(c34324,plain,
$false,
inference(resolution,[status(thm)],[c32716,prove_these_axioms_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : GRP526-1 : TPTP v8.1.2. Released v2.6.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n007.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 04:49:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 15.26/15.43 % Version: 1.5
% 15.26/15.43 % SZS status Unsatisfiable
% 15.26/15.43 % SZS output start CNFRefutation
% See solution above
% 15.26/15.43
% 15.26/15.43 % Initial clauses : 10
% 15.26/15.43 % Processed clauses : 562
% 15.26/15.43 % Factors computed : 3
% 15.26/15.43 % Resolvents computed: 34375
% 15.26/15.43 % Tautologies deleted: 2
% 15.26/15.43 % Forward subsumed : 826
% 15.26/15.43 % Backward subsumed : 7
% 15.26/15.43 % -------- CPU Time ---------
% 15.26/15.43 % User time : 14.983 s
% 15.26/15.43 % System time : 0.089 s
% 15.26/15.43 % Total time : 15.072 s
%------------------------------------------------------------------------------