%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP529-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:59 EDT 2024
% Result : Unsatisfiable 42.59s 42.78s
% Output : Refutation 42.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 9
% Syntax : Number of clauses : 38 ( 26 unt; 0 nHn; 12 RR)
% Number of literals : 52 ( 51 equ; 15 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 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 : 86 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_these_axioms_1,negated_conjecture,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_1) ).
cnf(transitivity,axiom,
( X8 != X10
| X10 != X9
| X8 = X9 ),
theory(equality) ).
cnf(c2,axiom,
( X17 != X18
| inverse(X17) = inverse(X18) ),
theory(equality) ).
cnf(symmetry,axiom,
( X3 != X4
| X4 = X3 ),
theory(equality) ).
cnf(inverse,axiom,
inverse(X6) = divide(divide(X7,X7),X6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inverse) ).
cnf(c4,plain,
divide(divide(X20,X20),X21) = inverse(X21),
inference(resolution,[status(thm)],[inverse,symmetry]) ).
cnf(c13,plain,
inverse(divide(divide(X38,X38),X37)) = inverse(inverse(X37)),
inference(resolution,[status(thm)],[c4,c2]) ).
cnf(c11,plain,
inverse(inverse(X36)) = inverse(divide(divide(X35,X35),X36)),
inference(resolution,[status(thm)],[c2,inverse]) ).
cnf(single_axiom,axiom,
divide(divide(X11,divide(X13,X12)),divide(X11,X13)) = X12,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
cnf(c8,plain,
X32 = divide(divide(X33,divide(X34,X32)),divide(X33,X34)),
inference(resolution,[status(thm)],[single_axiom,symmetry]) ).
cnf(c15,plain,
( X39 != divide(divide(X41,X41),X40)
| X39 = inverse(X40) ),
inference(resolution,[status(thm)],[c4,transitivity]) ).
cnf(c36,plain,
X46 = inverse(divide(divide(X45,X46),X45)),
inference(resolution,[status(thm)],[c15,c8]) ).
cnf(c40,plain,
inverse(divide(divide(X51,X52),X51)) = X52,
inference(resolution,[status(thm)],[c36,symmetry]) ).
cnf(c53,plain,
( X116 != inverse(divide(divide(X118,X117),X118))
| X116 = X117 ),
inference(resolution,[status(thm)],[c40,transitivity]) ).
cnf(c194,plain,
inverse(inverse(X124)) = X124,
inference(resolution,[status(thm)],[c53,c11]) ).
cnf(c209,plain,
( X133 != inverse(inverse(X134))
| X133 = X134 ),
inference(resolution,[status(thm)],[c194,transitivity]) ).
cnf(c245,plain,
inverse(divide(divide(X155,X155),X154)) = X154,
inference(resolution,[status(thm)],[c209,c13]) ).
cnf(c338,plain,
( X448 != inverse(divide(divide(X450,X450),X449))
| X448 = X449 ),
inference(resolution,[status(thm)],[c245,transitivity]) ).
cnf(multiply,axiom,
multiply(X22,X24) = divide(X22,divide(divide(X23,X23),X24)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiply) ).
cnf(c17,plain,
divide(X82,divide(divide(X83,X83),X84)) = multiply(X82,X84),
inference(resolution,[status(thm)],[multiply,symmetry]) ).
cnf(c117,plain,
( X1054 != divide(X1056,divide(divide(X1053,X1053),X1055))
| X1054 = multiply(X1056,X1055) ),
inference(resolution,[status(thm)],[c17,transitivity]) ).
cnf(c41,plain,
inverse(X114) = inverse(inverse(divide(divide(X115,X114),X115))),
inference(resolution,[status(thm)],[c36,c2]) ).
cnf(c249,plain,
inverse(X157) = divide(divide(X158,X157),X158),
inference(resolution,[status(thm)],[c209,c41]) ).
cnf(c380,plain,
divide(divide(X177,X178),X177) = inverse(X178),
inference(resolution,[status(thm)],[c249,symmetry]) ).
cnf(c442,plain,
( X559 != divide(divide(X558,X560),X558)
| X559 = inverse(X560) ),
inference(resolution,[status(thm)],[c380,transitivity]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c0,axiom,
( X47 != X50
| X49 != X48
| divide(X47,X49) = divide(X50,X48) ),
theory(equality) ).
cnf(c44,plain,
( X58 != X59
| divide(X58,X60) = divide(X59,X60) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c377,plain,
divide(inverse(X3896),X3897) = divide(divide(divide(X3895,X3896),X3895),X3897),
inference(resolution,[status(thm)],[c249,c44]) ).
cnf(c46814,plain,
divide(inverse(X3918),divide(X3919,X3918)) = inverse(X3919),
inference(resolution,[status(thm)],[c377,c442]) ).
cnf(c47031,plain,
inverse(X3927) = divide(inverse(X3928),divide(X3927,X3928)),
inference(resolution,[status(thm)],[c46814,symmetry]) ).
cnf(c47243,plain,
inverse(divide(X3939,X3939)) = multiply(inverse(X3938),X3938),
inference(resolution,[status(thm)],[c47031,c117]) ).
cnf(c47511,plain,
multiply(inverse(X3950),X3950) = inverse(divide(X3951,X3951)),
inference(resolution,[status(thm)],[c47243,symmetry]) ).
cnf(c47525,plain,
multiply(inverse(X3953),X3953) = divide(X3952,X3952),
inference(resolution,[status(thm)],[c47511,c338]) ).
cnf(c47669,plain,
divide(X3964,X3964) = multiply(inverse(X3963),X3963),
inference(resolution,[status(thm)],[c47525,symmetry]) ).
cnf(c47874,plain,
( X5505 != divide(X5507,X5507)
| X5505 = multiply(inverse(X5506),X5506) ),
inference(resolution,[status(thm)],[c47669,transitivity]) ).
cnf(c72683,plain,
multiply(inverse(X5574),X5574) = multiply(inverse(X5575),X5575),
inference(resolution,[status(thm)],[c47874,c47525]) ).
cnf(c73908,plain,
$false,
inference(resolution,[status(thm)],[c72683,prove_these_axioms_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GRP529-1 : TPTP v8.1.2. Released v2.6.0.
% 0.04/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 03:52:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 42.59/42.78 % Version: 1.5
% 42.59/42.78 % SZS status Unsatisfiable
% 42.59/42.78 % SZS output start CNFRefutation
% See solution above
% 42.59/42.78
% 42.59/42.78 % Initial clauses : 10
% 42.59/42.78 % Processed clauses : 847
% 42.59/42.78 % Factors computed : 3
% 42.59/42.78 % Resolvents computed: 73988
% 42.59/42.78 % Tautologies deleted: 2
% 42.59/42.78 % Forward subsumed : 1482
% 42.59/42.78 % Backward subsumed : 15
% 42.59/42.78 % -------- CPU Time ---------
% 42.59/42.78 % User time : 42.200 s
% 42.59/42.78 % System time : 0.192 s
% 42.59/42.78 % Total time : 42.392 s
%------------------------------------------------------------------------------