%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP022-2 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:22:48 EDT 2024
% Result : Unsatisfiable 30.82s 31.07s
% Output : Refutation 30.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 9
% Syntax : Number of clauses : 23 ( 14 unt; 0 nHn; 9 RR)
% Number of literals : 34 ( 33 equ; 12 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 46 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_inverse_of_inverse_is_original,negated_conjecture,
inverse(inverse(a)) != a,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_inverse_of_inverse_is_original) ).
cnf(associativity,axiom,
multiply(multiply(X14,X15),X16) = multiply(X14,multiply(X15,X16)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',associativity) ).
cnf(transitivity,axiom,
( X21 != X22
| X22 != X23
| X21 = X23 ),
theory(equality) ).
cnf(c22,plain,
( X73 != multiply(multiply(X71,X72),X70)
| X73 = multiply(X71,multiply(X72,X70)) ),
inference(resolution,[status(thm)],[transitivity,associativity]) ).
cnf(symmetry,axiom,
( X5 != X6
| X6 = X5 ),
theory(equality) ).
cnf(left_identity,axiom,
multiply(identity,X3) = X3,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_identity) ).
cnf(c19,plain,
( X41 != multiply(identity,X40)
| X41 = X40 ),
inference(resolution,[status(thm)],[transitivity,left_identity]) ).
cnf(right_inverse,axiom,
multiply(X13,inverse(X13)) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_inverse) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c0,axiom,
( X34 != X35
| X32 != X33
| multiply(X34,X32) = multiply(X35,X33) ),
theory(equality) ).
cnf(c46,plain,
( X140 != X141
| multiply(X140,X139) = multiply(X141,X139) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c598,plain,
multiply(multiply(X1137,inverse(X1137)),X1136) = multiply(identity,X1136),
inference(resolution,[status(thm)],[c46,right_inverse]) ).
cnf(c20976,plain,
multiply(multiply(X1139,inverse(X1139)),X1138) = X1138,
inference(resolution,[status(thm)],[c598,c19]) ).
cnf(c21050,plain,
X1141 = multiply(multiply(X1140,inverse(X1140)),X1141),
inference(resolution,[status(thm)],[c20976,symmetry]) ).
cnf(c21180,plain,
X1147 = multiply(X1146,multiply(inverse(X1146),X1147)),
inference(resolution,[status(thm)],[c21050,c22]) ).
cnf(right_identity,axiom,
multiply(X4,identity) = X4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_identity) ).
cnf(c21,plain,
( X51 != multiply(X50,identity)
| X51 = X50 ),
inference(resolution,[status(thm)],[transitivity,right_identity]) ).
cnf(c44,plain,
( X127 != X128
| multiply(X127,multiply(X129,inverse(X129))) = multiply(X128,identity) ),
inference(resolution,[status(thm)],[c0,right_inverse]) ).
cnf(c448,plain,
multiply(X994,multiply(X995,inverse(X995))) = multiply(X994,identity),
inference(resolution,[status(thm)],[c44,reflexivity]) ).
cnf(c17140,plain,
multiply(X999,multiply(X998,inverse(X998))) = X999,
inference(resolution,[status(thm)],[c448,c21]) ).
cnf(c17285,plain,
( X2163 != multiply(X2161,multiply(X2162,inverse(X2162)))
| X2163 = X2161 ),
inference(resolution,[status(thm)],[c17140,transitivity]) ).
cnf(c47615,plain,
inverse(inverse(X2168)) = X2168,
inference(resolution,[status(thm)],[c17285,c21180]) ).
cnf(c47817,plain,
$false,
inference(resolution,[status(thm)],[c47615,prove_inverse_of_inverse_is_original]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP022-2 : TPTP v8.1.2. Released v1.0.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n012.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 05:01:22 EDT 2024
% 0.13/0.34 % CPUTime :
% 30.82/31.07 % Version: 1.5
% 30.82/31.07 % SZS status Unsatisfiable
% 30.82/31.07 % SZS output start CNFRefutation
% See solution above
% 30.82/31.07
% 30.82/31.07 % Initial clauses : 11
% 30.82/31.07 % Processed clauses : 760
% 30.82/31.07 % Factors computed : 2
% 30.82/31.07 % Resolvents computed: 47887
% 30.82/31.07 % Tautologies deleted: 2
% 30.82/31.07 % Forward subsumed : 1659
% 30.82/31.07 % Backward subsumed : 48
% 30.82/31.07 % -------- CPU Time ---------
% 30.82/31.07 % User time : 30.605 s
% 30.82/31.07 % System time : 0.116 s
% 30.82/31.07 % Total time : 30.721 s
%------------------------------------------------------------------------------