%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP047-2 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:54 EDT 2024
% Result : Unsatisfiable 1.49s 1.66s
% Output : Refutation 1.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 9
% Syntax : Number of clauses : 23 ( 11 unt; 0 nHn; 16 RR)
% Number of literals : 44 ( 0 equ; 22 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 52 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_multiply_substitution2,negated_conjecture,
~ equalish(multiply(c,a),multiply(c,b)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_multiply_substitution2) ).
cnf(total_function1,axiom,
product(X4,X5,multiply(X4,X5)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP005-0.ax',total_function1) ).
cnf(total_function2,axiom,
( ~ product(X6,X9,X7)
| ~ product(X6,X9,X8)
| equalish(X7,X8) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRP005-0.ax',total_function2) ).
cnf(c2,plain,
( ~ product(X34,X32,X33)
| equalish(X33,multiply(X34,X32)) ),
inference(resolution,[status(thm)],[total_function2,total_function1]) ).
cnf(left_identity,axiom,
product(identity,X2,X2),
file('/export/starexec/sandbox/benchmark/Axioms/GRP005-0.ax',left_identity) ).
cnf(associativity2,axiom,
( ~ product(X24,X23,X27)
| ~ product(X23,X25,X28)
| ~ product(X24,X28,X26)
| product(X27,X25,X26) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRP005-0.ax',associativity2) ).
cnf(c14,plain,
( ~ product(X92,X93,X90)
| ~ product(X93,X91,X93)
| product(X90,X91,X90) ),
inference(factor,[status(thm)],[associativity2]) ).
cnf(c117,plain,
( ~ product(X143,identity,X142)
| product(X142,identity,X142) ),
inference(resolution,[status(thm)],[c14,left_identity]) ).
cnf(left_inverse,axiom,
product(inverse(X3),X3,identity),
file('/export/starexec/sandbox/benchmark/Axioms/GRP005-0.ax',left_inverse) ).
cnf(associativity1,axiom,
( ~ product(X11,X10,X14)
| ~ product(X10,X12,X15)
| ~ product(X14,X12,X13)
| product(X11,X15,X13) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRP005-0.ax',associativity1) ).
cnf(c6,plain,
( ~ product(X76,X75,identity)
| ~ product(X75,X74,X77)
| product(X76,X77,X74) ),
inference(resolution,[status(thm)],[associativity1,left_identity]) ).
cnf(c87,plain,
( ~ product(X253,inverse(X252),identity)
| product(X253,identity,X252) ),
inference(resolution,[status(thm)],[c6,left_inverse]) ).
cnf(c782,plain,
product(inverse(inverse(X254)),identity,X254),
inference(resolution,[status(thm)],[c87,left_inverse]) ).
cnf(c783,plain,
product(X255,identity,X255),
inference(resolution,[status(thm)],[c782,c117]) ).
cnf(a_equals_b,plain,
equalish(a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_equals_b) ).
cnf(product_substitution3,axiom,
( ~ equalish(X38,X41)
| ~ product(X40,X39,X38)
| product(X40,X39,X41) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRP005-0.ax',product_substitution3) ).
cnf(c22,plain,
( ~ equalish(X43,X44)
| product(identity,X43,X44) ),
inference(resolution,[status(thm)],[product_substitution3,left_identity]) ).
cnf(c27,plain,
product(identity,a,b),
inference(resolution,[status(thm)],[c22,a_equals_b]) ).
cnf(c7,plain,
( ~ product(X82,X79,X83)
| ~ product(X79,X80,X81)
| product(X82,X81,multiply(X83,X80)) ),
inference(resolution,[status(thm)],[associativity1,total_function1]) ).
cnf(c99,plain,
( ~ product(X285,identity,X286)
| product(X285,b,multiply(X286,a)) ),
inference(resolution,[status(thm)],[c7,c27]) ).
cnf(c986,plain,
product(X321,b,multiply(X321,a)),
inference(resolution,[status(thm)],[c99,c783]) ).
cnf(c1281,plain,
equalish(multiply(X577,a),multiply(X577,b)),
inference(resolution,[status(thm)],[c986,c2]) ).
cnf(c3531,plain,
$false,
inference(resolution,[status(thm)],[c1281,prove_multiply_substitution2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : GRP047-2 : TPTP v8.1.2. Released v1.0.0.
% 0.09/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n014.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:50:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 1.49/1.66 % Version: 1.5
% 1.49/1.66 % SZS status Unsatisfiable
% 1.49/1.66 % SZS output start CNFRefutation
% See solution above
% 1.49/1.66
% 1.49/1.66 % Initial clauses : 9
% 1.49/1.66 % Processed clauses : 254
% 1.49/1.66 % Factors computed : 31
% 1.49/1.66 % Resolvents computed: 3507
% 1.49/1.66 % Tautologies deleted: 13
% 1.49/1.66 % Forward subsumed : 355
% 1.49/1.66 % Backward subsumed : 20
% 1.49/1.66 % -------- CPU Time ---------
% 1.49/1.66 % User time : 1.276 s
% 1.49/1.66 % System time : 0.022 s
% 1.49/1.66 % Total time : 1.298 s
%------------------------------------------------------------------------------