%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP554-1 : TPTP v8.1.2. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:24:02 EDT 2024
% Result : Unsatisfiable 203.91s 204.29s
% Output : Refutation 203.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 8
% Syntax : Number of clauses : 48 ( 32 unt; 0 nHn; 14 RR)
% Number of literals : 67 ( 66 equ; 20 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 7 ( 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 : 156 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_these_axioms_2,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_2) ).
cnf(symmetry,axiom,
( X3 != X4
| X4 = X3 ),
theory(equality) ).
cnf(transitivity,axiom,
( X8 != X9
| X9 != X10
| X8 = X10 ),
theory(equality) ).
cnf(multiply,axiom,
multiply(X6,X7) = divide(X6,inverse(X7)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiply) ).
cnf(c4,plain,
divide(X20,inverse(X21)) = multiply(X20,X21),
inference(resolution,[status(thm)],[multiply,symmetry]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c2,axiom,
( X50 != X49
| X48 != X47
| multiply(X50,X48) = multiply(X49,X47) ),
theory(equality) ).
cnf(c46,plain,
( X55 != X54
| multiply(X55,X56) = multiply(X54,X56) ),
inference(resolution,[status(thm)],[c2,reflexivity]) ).
cnf(c60,plain,
multiply(divide(X96,inverse(X98)),X97) = multiply(multiply(X96,X98),X97),
inference(resolution,[status(thm)],[c46,c4]) ).
cnf(c140,plain,
( X437 != multiply(divide(X436,inverse(X434)),X435)
| X437 = multiply(multiply(X436,X434),X435) ),
inference(resolution,[status(thm)],[c60,transitivity]) ).
cnf(c0,axiom,
( X36 != X35
| X34 != X33
| divide(X36,X34) = divide(X35,X33) ),
theory(equality) ).
cnf(c24,plain,
( X42 != X40
| divide(X42,X41) = divide(X40,X41) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c35,plain,
divide(divide(X73,inverse(X75)),X74) = divide(multiply(X73,X75),X74),
inference(resolution,[status(thm)],[c24,c4]) ).
cnf(c84,plain,
( X364 != divide(divide(X362,inverse(X363)),X361)
| X364 = divide(multiply(X362,X363),X361) ),
inference(resolution,[status(thm)],[c35,transitivity]) ).
cnf(single_axiom,axiom,
divide(divide(X11,inverse(divide(X13,divide(X11,X12)))),X12) = X13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
cnf(c9,plain,
( X79 != divide(divide(X78,inverse(divide(X77,divide(X78,X76)))),X76)
| X79 = X77 ),
inference(resolution,[status(thm)],[single_axiom,transitivity]) ).
cnf(c36,plain,
divide(multiply(X81,X83),X82) = divide(divide(X81,inverse(X83)),X82),
inference(resolution,[status(thm)],[c24,multiply]) ).
cnf(c92,plain,
divide(multiply(X85,divide(X84,divide(X85,X86))),X86) = X84,
inference(resolution,[status(thm)],[c36,c9]) ).
cnf(c107,plain,
( X946 != X943
| divide(X946,divide(multiply(X944,divide(X945,divide(X944,X942))),X942)) = divide(X943,X945) ),
inference(resolution,[status(thm)],[c92,c0]) ).
cnf(c3921,plain,
divide(X968,divide(multiply(X966,divide(X965,divide(X966,X967))),X967)) = divide(X968,X965),
inference(resolution,[status(thm)],[c107,reflexivity]) ).
cnf(c3989,plain,
( X3284 != divide(X3283,divide(multiply(X3280,divide(X3282,divide(X3280,X3281))),X3281))
| X3284 = divide(X3283,X3282) ),
inference(resolution,[status(thm)],[c3921,transitivity]) ).
cnf(c110,plain,
X87 = divide(multiply(X88,divide(X87,divide(X88,X89))),X89),
inference(resolution,[status(thm)],[c92,symmetry]) ).
cnf(c115,plain,
divide(X419,X420) = divide(divide(multiply(X421,divide(X419,divide(X421,X418))),X418),X420),
inference(resolution,[status(thm)],[c110,c24]) ).
cnf(c1224,plain,
divide(divide(X5452,X5454),X5456) = divide(divide(divide(multiply(X5453,divide(X5452,divide(X5453,X5455))),X5455),X5454),X5456),
inference(resolution,[status(thm)],[c115,c24]) ).
cnf(c93,plain,
divide(divide(multiply(X740,X741),X742),X743) = divide(divide(divide(X740,inverse(X741)),X742),X743),
inference(resolution,[status(thm)],[c36,c24]) ).
cnf(c2362,plain,
( X6021 != divide(divide(multiply(X6020,X6019),X6017),X6018)
| X6021 = divide(divide(divide(X6020,inverse(X6019)),X6017),X6018) ),
inference(resolution,[status(thm)],[c93,transitivity]) ).
cnf(c111,plain,
( X194 != divide(multiply(X191,divide(X192,divide(X191,X193))),X193)
| X194 = X192 ),
inference(resolution,[status(thm)],[c92,transitivity]) ).
cnf(c103,plain,
( X902 != X901
| multiply(X902,divide(multiply(X903,divide(X904,divide(X903,X900))),X900)) = multiply(X901,X904) ),
inference(resolution,[status(thm)],[c92,c2]) ).
cnf(c3636,plain,
multiply(X924,divide(multiply(X925,divide(X926,divide(X925,X923))),X923)) = multiply(X924,X926),
inference(resolution,[status(thm)],[c103,reflexivity]) ).
cnf(c3714,plain,
multiply(X928,X927) = multiply(X928,divide(multiply(X930,divide(X927,divide(X930,X929))),X929)),
inference(resolution,[status(thm)],[c3636,symmetry]) ).
cnf(c3766,plain,
divide(multiply(X6966,X6967),X6970) = divide(multiply(X6966,divide(multiply(X6968,divide(X6967,divide(X6968,X6969))),X6969)),X6970),
inference(resolution,[status(thm)],[c3714,c24]) ).
cnf(c61773,plain,
divide(multiply(X6974,X6977),X6975) = multiply(X6976,divide(X6977,divide(X6976,divide(X6974,X6975)))),
inference(resolution,[status(thm)],[c3766,c111]) ).
cnf(c61940,plain,
divide(divide(multiply(X12109,X12111),X12107),X12110) = divide(multiply(X12108,divide(X12111,divide(X12108,divide(X12109,X12107)))),X12110),
inference(resolution,[status(thm)],[c61773,c24]) ).
cnf(c137329,plain,
divide(divide(multiply(X12112,X12114),X12113),divide(X12112,X12113)) = X12114,
inference(resolution,[status(thm)],[c61940,c111]) ).
cnf(c137569,plain,
X12115 = divide(divide(multiply(X12117,X12115),X12116),divide(X12117,X12116)),
inference(resolution,[status(thm)],[c137329,symmetry]) ).
cnf(c137691,plain,
X12150 = divide(divide(divide(X12151,inverse(X12150)),X12149),divide(X12151,X12149)),
inference(resolution,[status(thm)],[c137569,c2362]) ).
cnf(c138841,plain,
divide(divide(divide(X12201,inverse(X12199)),X12200),divide(X12201,X12200)) = X12199,
inference(resolution,[status(thm)],[c137691,symmetry]) ).
cnf(c139623,plain,
( X12881 != divide(divide(divide(X12880,inverse(X12878)),X12879),divide(X12880,X12879))
| X12881 = X12878 ),
inference(resolution,[status(thm)],[c138841,transitivity]) ).
cnf(c161170,plain,
divide(divide(X14810,X14813),divide(multiply(X14811,divide(X14810,divide(X14811,inverse(X14812)))),X14813)) = X14812,
inference(resolution,[status(thm)],[c139623,c1224]) ).
cnf(c217439,plain,
X15729 = divide(divide(X15730,X15732),divide(multiply(X15731,divide(X15730,divide(X15731,inverse(X15729)))),X15732)),
inference(resolution,[status(thm)],[c161170,symmetry]) ).
cnf(c228037,plain,
X15735 = divide(divide(X15734,inverse(X15735)),X15734),
inference(resolution,[status(thm)],[c217439,c3989]) ).
cnf(c228129,plain,
X15743 = divide(multiply(X15744,X15743),X15744),
inference(resolution,[status(thm)],[c228037,c84]) ).
cnf(c228131,plain,
divide(X15753,divide(X15752,X15752)) = X15753,
inference(resolution,[status(thm)],[c228037,c9]) ).
cnf(c228693,plain,
( X15844 != divide(X15842,divide(X15843,X15843))
| X15844 = X15842 ),
inference(resolution,[status(thm)],[c228131,transitivity]) ).
cnf(c234794,plain,
X15858 = multiply(divide(X15859,X15859),X15858),
inference(resolution,[status(thm)],[c228693,c228129]) ).
cnf(c235174,plain,
X15891 = multiply(multiply(inverse(X15890),X15890),X15891),
inference(resolution,[status(thm)],[c234794,c140]) ).
cnf(c237426,plain,
multiply(multiply(inverse(X15904),X15904),X15903) = X15903,
inference(resolution,[status(thm)],[c235174,symmetry]) ).
cnf(c237952,plain,
$false,
inference(resolution,[status(thm)],[c237426,prove_these_axioms_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP554-1 : TPTP v8.1.2. Released v2.6.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n029.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 03:42:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 203.91/204.29 % Version: 1.5
% 203.91/204.29 % SZS status Unsatisfiable
% 203.91/204.29 % SZS output start CNFRefutation
% See solution above
% 203.91/204.29
% 203.91/204.29 % Initial clauses : 9
% 203.91/204.29 % Processed clauses : 1716
% 203.91/204.29 % Factors computed : 3
% 203.91/204.29 % Resolvents computed: 238210
% 203.91/204.29 % Tautologies deleted: 2
% 203.91/204.29 % Forward subsumed : 2504
% 203.91/204.29 % Backward subsumed : 8
% 203.91/204.29 % -------- CPU Time ---------
% 203.91/204.29 % User time : 203.211 s
% 203.91/204.29 % System time : 0.604 s
% 203.91/204.29 % Total time : 203.815 s
%------------------------------------------------------------------------------