%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP496-1 : TPTP v8.1.2. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:54 EDT 2024
% Result : Unsatisfiable 0.84s 1.03s
% Output : Refutation 0.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 10
% Syntax : Number of clauses : 30 ( 20 unt; 0 nHn; 12 RR)
% Number of literals : 42 ( 41 equ; 13 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 : 49 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_these_axioms_1,negated_conjecture,
multiply(inverse(a1),a1) != identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_1) ).
cnf(symmetry,axiom,
( X4 != X3
| X3 = X4 ),
theory(equality) ).
cnf(transitivity,axiom,
( X19 != X17
| X17 != X18
| X19 = X18 ),
theory(equality) ).
cnf(identity,axiom,
identity = double_divide(X7,inverse(X7)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity) ).
cnf(c2,axiom,
( X24 != X23
| inverse(X24) = inverse(X23) ),
theory(equality) ).
cnf(c19,plain,
inverse(identity) = inverse(double_divide(X62,inverse(X62))),
inference(resolution,[status(thm)],[c2,identity]) ).
cnf(multiply,axiom,
multiply(X16,X15) = double_divide(double_divide(X15,X16),identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiply) ).
cnf(inverse,axiom,
inverse(X6) = double_divide(X6,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inverse) ).
cnf(c4,plain,
double_divide(X11,identity) = inverse(X11),
inference(resolution,[status(thm)],[inverse,symmetry]) ).
cnf(c16,plain,
( X42 != double_divide(X43,identity)
| X42 = inverse(X43) ),
inference(resolution,[status(thm)],[transitivity,c4]) ).
cnf(c52,plain,
multiply(X47,X46) = inverse(double_divide(X46,X47)),
inference(resolution,[status(thm)],[c16,multiply]) ).
cnf(c60,plain,
inverse(double_divide(X51,X52)) = multiply(X52,X51),
inference(resolution,[status(thm)],[c52,symmetry]) ).
cnf(c68,plain,
( X126 != inverse(double_divide(X125,X127))
| X126 = multiply(X127,X125) ),
inference(resolution,[status(thm)],[c60,transitivity]) ).
cnf(c267,plain,
inverse(identity) = multiply(inverse(X136),X136),
inference(resolution,[status(thm)],[c68,c19]) ).
cnf(c314,plain,
( X257 != inverse(identity)
| X257 = multiply(inverse(X258),X258) ),
inference(resolution,[status(thm)],[c267,transitivity]) ).
cnf(single_axiom,axiom,
double_divide(double_divide(identity,double_divide(X10,double_divide(X9,identity))),double_divide(double_divide(X9,double_divide(X8,X10)),identity)) = X8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
cnf(c14,plain,
( X71 != double_divide(double_divide(identity,double_divide(X70,double_divide(X69,identity))),double_divide(double_divide(X69,double_divide(X68,X70)),identity))
| X71 = X68 ),
inference(resolution,[status(thm)],[transitivity,single_axiom]) ).
cnf(c5,plain,
double_divide(X12,inverse(X12)) = identity,
inference(resolution,[status(thm)],[identity,symmetry]) ).
cnf(c13,plain,
( X35 != double_divide(X36,inverse(X36))
| X35 = identity ),
inference(resolution,[status(thm)],[transitivity,c5]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c0,axiom,
( X28 != X26
| X27 != X29
| double_divide(X28,X27) = double_divide(X26,X29) ),
theory(equality) ).
cnf(c31,plain,
( X150 != X151
| double_divide(X150,double_divide(X152,identity)) = double_divide(X151,inverse(X152)) ),
inference(resolution,[status(thm)],[c0,c4]) ).
cnf(c384,plain,
double_divide(X295,double_divide(X296,identity)) = double_divide(X295,inverse(X296)),
inference(resolution,[status(thm)],[c31,reflexivity]) ).
cnf(c1454,plain,
double_divide(X297,double_divide(X297,identity)) = identity,
inference(resolution,[status(thm)],[c384,c13]) ).
cnf(c1469,plain,
identity = double_divide(X298,double_divide(X298,identity)),
inference(resolution,[status(thm)],[c1454,symmetry]) ).
cnf(c1496,plain,
identity = double_divide(identity,identity),
inference(resolution,[status(thm)],[c1469,c14]) ).
cnf(c1526,plain,
identity = inverse(identity),
inference(resolution,[status(thm)],[c1496,c16]) ).
cnf(c1594,plain,
identity = multiply(inverse(X307),X307),
inference(resolution,[status(thm)],[c1526,c314]) ).
cnf(c1742,plain,
multiply(inverse(X308),X308) = identity,
inference(resolution,[status(thm)],[c1594,symmetry]) ).
cnf(c1766,plain,
$false,
inference(resolution,[status(thm)],[c1742,prove_these_axioms_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP496-1 : TPTP v8.1.2. Released v2.6.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n027.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 04:15:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.84/1.03 % Version: 1.5
% 0.84/1.03 % SZS status Unsatisfiable
% 0.84/1.03 % SZS output start CNFRefutation
% See solution above
% 0.84/1.03
% 0.84/1.03 % Initial clauses : 11
% 0.84/1.03 % Processed clauses : 104
% 0.84/1.03 % Factors computed : 3
% 0.84/1.03 % Resolvents computed: 1776
% 0.84/1.03 % Tautologies deleted: 2
% 0.84/1.03 % Forward subsumed : 78
% 0.84/1.03 % Backward subsumed : 0
% 0.84/1.03 % -------- CPU Time ---------
% 0.84/1.03 % User time : 0.679 s
% 0.84/1.03 % System time : 0.010 s
% 0.84/1.03 % Total time : 0.689 s
%------------------------------------------------------------------------------