%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP029-2 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:50 EDT 2024
% Result : Unsatisfiable 0.73s 0.88s
% Output : Refutation 0.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 10
% Syntax : Number of clauses : 24 ( 11 unt; 0 nHn; 13 RR)
% Number of literals : 46 ( 0 equ; 23 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 : 4 ( 4 usr; 1 con; 0-2 aty)
% Number of variables : 56 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_there_is_a_right_identity,negated_conjecture,
~ product(not_right_identity(X16),X16,not_right_identity(X16)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_there_is_a_right_identity) ).
cnf(left_identity,axiom,
product(identity,X3,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_identity) ).
cnf(associativity2,axiom,
( ~ product(X82,X86,X83)
| ~ product(X86,X87,X85)
| ~ product(X82,X85,X84)
| product(X83,X87,X84) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity2) ).
cnf(c55,plain,
( ~ product(X249,X248,X247)
| ~ product(X248,X246,X248)
| product(X247,X246,X247) ),
inference(factor,[status(thm)],[associativity2]) ).
cnf(c550,plain,
( ~ product(X321,identity,X322)
| product(X322,identity,X322) ),
inference(resolution,[status(thm)],[c55,left_identity]) ).
cnf(left_inverse,axiom,
product(inverse(X12),X12,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_inverse) ).
cnf(symmetry,axiom,
( ~ equalish(X4,X5)
| equalish(X5,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry) ).
cnf(total_function1,axiom,
product(X7,X8,multiply(X7,X8)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',total_function1) ).
cnf(total_function2,axiom,
( ~ product(X59,X60,X61)
| ~ product(X59,X60,X62)
| equalish(X61,X62) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',total_function2) ).
cnf(c22,plain,
( ~ product(identity,X67,X66)
| equalish(X66,X67) ),
inference(resolution,[status(thm)],[total_function2,left_identity]) ).
cnf(c24,plain,
equalish(multiply(identity,X69),X69),
inference(resolution,[status(thm)],[c22,total_function1]) ).
cnf(c26,plain,
equalish(X70,multiply(identity,X70)),
inference(resolution,[status(thm)],[c24,symmetry]) ).
cnf(product_substitution3,axiom,
( ~ equalish(X47,X48)
| ~ product(X50,X49,X47)
| product(X50,X49,X48) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_substitution3) ).
cnf(c17,plain,
( ~ equalish(identity,X104)
| product(inverse(X105),X105,X104) ),
inference(resolution,[status(thm)],[product_substitution3,left_inverse]) ).
cnf(c77,plain,
product(inverse(X150),X150,multiply(identity,identity)),
inference(resolution,[status(thm)],[c17,c26]) ).
cnf(associativity1,axiom,
( ~ product(X71,X75,X72)
| ~ product(X75,X76,X74)
| ~ product(X72,X76,X73)
| product(X71,X74,X73) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity1) ).
cnf(product_substitution1,axiom,
( ~ equalish(X30,X31)
| ~ product(X30,X33,X32)
| product(X31,X33,X32) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_substitution1) ).
cnf(c7,plain,
( ~ equalish(identity,X39)
| product(X39,X38,X38) ),
inference(resolution,[status(thm)],[product_substitution1,left_identity]) ).
cnf(c42,plain,
product(multiply(identity,identity),X89,X89),
inference(resolution,[status(thm)],[c26,c7]) ).
cnf(c65,plain,
( ~ product(X331,X329,multiply(identity,identity))
| ~ product(X329,X330,X332)
| product(X331,X332,X330) ),
inference(resolution,[status(thm)],[c42,associativity1]) ).
cnf(c838,plain,
( ~ product(X387,X386,X388)
| product(inverse(X387),X388,X386) ),
inference(resolution,[status(thm)],[c65,c77]) ).
cnf(c1153,plain,
product(inverse(inverse(X392)),identity,X392),
inference(resolution,[status(thm)],[c838,left_inverse]) ).
cnf(c1198,plain,
product(X393,identity,X393),
inference(resolution,[status(thm)],[c1153,c550]) ).
cnf(c1244,plain,
$false,
inference(resolution,[status(thm)],[c1198,prove_there_is_a_right_identity]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : GRP029-2 : TPTP v8.1.2. Released v1.0.0.
% 0.15/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.37 % Computer : n011.cluster.edu
% 0.16/0.37 % Model : x86_64 x86_64
% 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.37 % Memory : 8042.1875MB
% 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.37 % CPULimit : 300
% 0.16/0.37 % WCLimit : 300
% 0.16/0.37 % DateTime : Thu May 9 04:30:23 EDT 2024
% 0.16/0.37 % CPUTime :
% 0.73/0.88 % Version: 1.5
% 0.73/0.88 % SZS status Unsatisfiable
% 0.73/0.88 % SZS output start CNFRefutation
% See solution above
% 0.73/0.88
% 0.73/0.88 % Initial clauses : 16
% 0.73/0.88 % Processed clauses : 118
% 0.73/0.88 % Factors computed : 20
% 0.73/0.88 % Resolvents computed: 1227
% 0.73/0.88 % Tautologies deleted: 9
% 0.73/0.88 % Forward subsumed : 146
% 0.73/0.88 % Backward subsumed : 2
% 0.73/0.88 % -------- CPU Time ---------
% 0.73/0.88 % User time : 0.498 s
% 0.73/0.88 % System time : 0.011 s
% 0.73/0.88 % Total time : 0.509 s
%------------------------------------------------------------------------------