%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP004-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:44 EDT 2024
% Result : Unsatisfiable 0.55s 0.70s
% Output : Refutation 0.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 5
% Syntax : Number of clauses : 28 ( 12 unt; 0 nHn; 19 RR)
% Number of literals : 55 ( 0 equ; 28 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-1 aty)
% Number of variables : 64 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_there_is_a_right_inverse,negated_conjecture,
~ product(a,X3,identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_there_is_a_right_inverse) ).
cnf(left_inverse,axiom,
product(inverse(X4),X4,identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_inverse) ).
cnf(associativity2,axiom,
( ~ product(X17,X18,X14)
| ~ product(X18,X19,X16)
| ~ product(X17,X16,X15)
| product(X14,X19,X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity2) ).
cnf(left_identity,axiom,
product(identity,X2,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_identity) ).
cnf(associativity1,axiom,
( ~ product(X8,X9,X5)
| ~ product(X9,X10,X7)
| ~ product(X5,X10,X6)
| product(X8,X7,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity1) ).
cnf(c2,plain,
( ~ product(X31,X29,identity)
| ~ product(X29,X32,X30)
| product(X31,X30,X32) ),
inference(resolution,[status(thm)],[associativity1,left_identity]) ).
cnf(c17,plain,
( ~ product(X43,inverse(X44),identity)
| product(X43,identity,X44) ),
inference(resolution,[status(thm)],[c2,left_inverse]) ).
cnf(c28,plain,
product(inverse(inverse(X45)),identity,X45),
inference(resolution,[status(thm)],[c17,left_inverse]) ).
cnf(c6,plain,
( ~ product(X51,X49,X50)
| ~ product(X49,X48,X49)
| product(X50,X48,X50) ),
inference(factor,[status(thm)],[associativity2]) ).
cnf(c43,plain,
( ~ product(X54,identity,X53)
| product(X53,identity,X53) ),
inference(resolution,[status(thm)],[c6,left_identity]) ).
cnf(c46,plain,
product(X55,identity,X55),
inference(resolution,[status(thm)],[c43,c28]) ).
cnf(c54,plain,
( ~ product(X217,X219,X218)
| ~ product(X219,X216,identity)
| product(X218,X216,X217) ),
inference(resolution,[status(thm)],[c46,associativity2]) ).
cnf(c328,plain,
( ~ product(X235,inverse(X236),X237)
| product(X237,X236,X235) ),
inference(resolution,[status(thm)],[c54,left_inverse]) ).
cnf(c8,plain,
( ~ product(identity,X66,X65)
| ~ product(X66,X63,X64)
| product(X65,X63,X64) ),
inference(resolution,[status(thm)],[associativity2,left_identity]) ).
cnf(c67,plain,
( ~ product(identity,X81,X82)
| product(X82,identity,X81) ),
inference(resolution,[status(thm)],[c8,c46]) ).
cnf(c1,plain,
( ~ product(X22,X24,X24)
| ~ product(X24,X25,X23)
| product(X22,X23,X23) ),
inference(factor,[status(thm)],[associativity1]) ).
cnf(c11,plain,
( ~ product(X28,identity,identity)
| product(X28,X27,X27) ),
inference(resolution,[status(thm)],[c1,left_identity]) ).
cnf(c14,plain,
product(inverse(identity),X34,X34),
inference(resolution,[status(thm)],[c11,left_inverse]) ).
cnf(c9,plain,
( ~ product(inverse(X77),X79,X78)
| ~ product(X79,X76,X77)
| product(X78,X76,identity) ),
inference(resolution,[status(thm)],[associativity2,left_inverse]) ).
cnf(c78,plain,
( ~ product(X89,X88,X89)
| product(identity,X88,identity) ),
inference(resolution,[status(thm)],[c9,left_inverse]) ).
cnf(c88,plain,
product(identity,inverse(identity),identity),
inference(resolution,[status(thm)],[c78,c14]) ).
cnf(c97,plain,
product(identity,identity,inverse(identity)),
inference(resolution,[status(thm)],[c88,c67]) ).
cnf(c22,plain,
( ~ product(X110,X108,inverse(identity))
| ~ product(X108,X111,X109)
| product(X110,X109,X111) ),
inference(resolution,[status(thm)],[c14,associativity1]) ).
cnf(c129,plain,
( ~ product(identity,X113,X114)
| product(identity,X114,X113) ),
inference(resolution,[status(thm)],[c22,c97]) ).
cnf(c384,plain,
product(identity,X242,inverse(inverse(X242))),
inference(resolution,[status(thm)],[c328,left_inverse]) ).
cnf(c400,plain,
product(identity,inverse(inverse(X251)),X251),
inference(resolution,[status(thm)],[c384,c129]) ).
cnf(c444,plain,
product(X256,inverse(X256),identity),
inference(resolution,[status(thm)],[c400,c328]) ).
cnf(c488,plain,
$false,
inference(resolution,[status(thm)],[c444,prove_there_is_a_right_inverse]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP004-1 : TPTP v8.1.2. Released v1.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n026.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 03:42:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.55/0.70 % Version: 1.5
% 0.55/0.70 % SZS status Unsatisfiable
% 0.55/0.70 % SZS output start CNFRefutation
% See solution above
% 0.55/0.70
% 0.55/0.70 % Initial clauses : 5
% 0.55/0.70 % Processed clauses : 71
% 0.55/0.70 % Factors computed : 20
% 0.55/0.70 % Resolvents computed: 473
% 0.55/0.70 % Tautologies deleted: 19
% 0.55/0.70 % Forward subsumed : 128
% 0.55/0.70 % Backward subsumed : 9
% 0.55/0.70 % -------- CPU Time ---------
% 0.55/0.70 % User time : 0.345 s
% 0.55/0.70 % System time : 0.010 s
% 0.55/0.70 % Total time : 0.355 s
%------------------------------------------------------------------------------