%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP046-2 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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.76s 1.92s
% Output : Refutation 1.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 9
% Syntax : Number of clauses : 27 ( 13 unt; 0 nHn; 19 RR)
% Number of literals : 50 ( 0 equ; 24 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 : 57 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_multiply_substitution1,negated_conjecture,
~ equalish(multiply(a,c),multiply(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_multiply_substitution1) ).
cnf(total_function1,axiom,
product(X4,X5,multiply(X4,X5)),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP005-0.ax',total_function1) ).
cnf(total_function2,axiom,
( ~ product(X8,X9,X7)
| ~ product(X8,X9,X6)
| equalish(X7,X6) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP005-0.ax',total_function2) ).
cnf(c2,plain,
( ~ product(X33,X34,X32)
| equalish(X32,multiply(X33,X34)) ),
inference(resolution,[status(thm)],[total_function2,total_function1]) ).
cnf(left_identity,axiom,
product(identity,X2,X2),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP005-0.ax',left_identity) ).
cnf(c1,plain,
( ~ product(identity,X21,X20)
| equalish(X20,X21) ),
inference(resolution,[status(thm)],[total_function2,left_identity]) ).
cnf(a_equals_b,plain,
equalish(a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_equals_b) ).
cnf(product_substitution3,axiom,
( ~ equalish(X40,X41)
| ~ product(X38,X39,X40)
| product(X38,X39,X41) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP005-0.ax',product_substitution3) ).
cnf(c22,plain,
( ~ equalish(X44,X43)
| product(identity,X44,X43) ),
inference(resolution,[status(thm)],[product_substitution3,left_identity]) ).
cnf(c27,plain,
product(identity,a,b),
inference(resolution,[status(thm)],[c22,a_equals_b]) ).
cnf(c33,plain,
equalish(b,a),
inference(resolution,[status(thm)],[c27,c1]) ).
cnf(associativity2,axiom,
( ~ product(X27,X28,X25)
| ~ product(X28,X26,X23)
| ~ product(X27,X23,X24)
| product(X25,X26,X24) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP005-0.ax',associativity2) ).
cnf(c14,plain,
( ~ product(X92,X91,X93)
| ~ product(X91,X90,X91)
| product(X93,X90,X93) ),
inference(factor,[status(thm)],[associativity2]) ).
cnf(c118,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/sandbox2/benchmark/Axioms/GRP005-0.ax',left_inverse) ).
cnf(associativity1,axiom,
( ~ product(X14,X15,X12)
| ~ product(X15,X13,X10)
| ~ product(X12,X13,X11)
| product(X14,X10,X11) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP005-0.ax',associativity1) ).
cnf(c6,plain,
( ~ product(X76,X74,identity)
| ~ product(X74,X77,X75)
| product(X76,X75,X77) ),
inference(resolution,[status(thm)],[associativity1,left_identity]) ).
cnf(c84,plain,
( ~ product(X249,inverse(X248),identity)
| product(X249,identity,X248) ),
inference(resolution,[status(thm)],[c6,left_inverse]) ).
cnf(c788,plain,
product(inverse(inverse(X250)),identity,X250),
inference(resolution,[status(thm)],[c84,left_inverse]) ).
cnf(c799,plain,
product(X251,identity,X251),
inference(resolution,[status(thm)],[c788,c118]) ).
cnf(c820,plain,
( ~ equalish(X262,X261)
| product(X262,identity,X261) ),
inference(resolution,[status(thm)],[c799,product_substitution3]) ).
cnf(c893,plain,
product(b,identity,a),
inference(resolution,[status(thm)],[c820,c33]) ).
cnf(c7,plain,
( ~ product(X81,X80,X79)
| ~ product(X80,X82,X83)
| product(X81,X83,multiply(X79,X82)) ),
inference(resolution,[status(thm)],[associativity1,total_function1]) ).
cnf(c103,plain,
( ~ product(X312,identity,X311)
| product(X312,X313,multiply(X311,X313)) ),
inference(resolution,[status(thm)],[c7,left_identity]) ).
cnf(c1276,plain,
product(b,X340,multiply(a,X340)),
inference(resolution,[status(thm)],[c103,c893]) ).
cnf(c1528,plain,
equalish(multiply(a,X629),multiply(b,X629)),
inference(resolution,[status(thm)],[c1276,c2]) ).
cnf(c4277,plain,
$false,
inference(resolution,[status(thm)],[c1528,prove_multiply_substitution1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GRP046-2 : TPTP v8.1.2. Released v1.0.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n003.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 04:55:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 1.76/1.92 % Version: 1.5
% 1.76/1.92 % SZS status Unsatisfiable
% 1.76/1.92 % SZS output start CNFRefutation
% See solution above
% 1.76/1.92
% 1.76/1.92 % Initial clauses : 9
% 1.76/1.92 % Processed clauses : 287
% 1.76/1.92 % Factors computed : 33
% 1.76/1.92 % Resolvents computed: 4245
% 1.76/1.92 % Tautologies deleted: 13
% 1.76/1.92 % Forward subsumed : 391
% 1.76/1.92 % Backward subsumed : 22
% 1.76/1.92 % -------- CPU Time ---------
% 1.76/1.92 % User time : 1.542 s
% 1.76/1.92 % System time : 0.023 s
% 1.76/1.92 % Total time : 1.565 s
%------------------------------------------------------------------------------