%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN719-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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:48:43 EDT 2024
% Result : Unsatisfiable 0.78s 1.00s
% Output : Refutation 0.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 9
% Syntax : Number of clauses : 17 ( 10 unt; 0 nHn; 12 RR)
% Number of literals : 31 ( 0 equ; 15 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 15 con; 0-2 aty)
% Number of variables : 24 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(not_p68_46,negated_conjecture,
~ p68(f19(f21(c83,c77),c79),c81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p68_46) ).
cnf(p67_42,negated_conjecture,
p67(f16(c80,c81),c82),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p67_42) ).
cnf(p66_41,negated_conjecture,
p66(f12(c78,c77),c79),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p66_41) ).
cnf(p14_45,negated_conjecture,
p14(f23(f26(c84,c85),X44),X44),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p14_45) ).
cnf(p14_38,negated_conjecture,
p14(X39,X39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p14_38) ).
cnf(p14_90,negated_conjecture,
( p14(X355,X353)
| ~ p14(X354,X355)
| ~ p14(X354,X353) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p14_90) ).
cnf(c115,plain,
( p14(X361,X362)
| ~ p14(X362,X361) ),
inference(resolution,[status(thm)],[p14_90,p14_38]) ).
cnf(c120,plain,
p14(X377,f23(f26(c84,c85),X377)),
inference(resolution,[status(thm)],[c115,p14_45]) ).
cnf(p70_43,negated_conjecture,
p70(f30(c88,X43),f38(c85,X42)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p70_43) ).
cnf(p69_52,negated_conjecture,
( p69(f36(c86,X56),X55)
| ~ p70(X55,X56) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p69_52) ).
cnf(c2,plain,
p69(f36(c86,f38(c85,X448)),f30(c88,X447)),
inference(resolution,[status(thm)],[p69_52,p70_43]) ).
cnf(p68_126,negated_conjecture,
( p68(f19(f21(c83,c77),X682),X684)
| ~ p67(f16(c80,X683),c82)
| ~ p66(f12(c78,c77),X682)
| ~ p14(X684,f23(f26(c84,X685),X683))
| ~ p69(f36(c86,f38(X685,f40(f42(f44(f46(c87,X682),X684),X685),X683))),f30(c88,f32(c89,f8(c75,c76)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p68_126) ).
cnf(c226,plain,
( p68(f19(f21(c83,c77),X848),X846)
| ~ p67(f16(c80,X847),c82)
| ~ p66(f12(c78,c77),X848)
| ~ p14(X846,f23(f26(c84,c85),X847)) ),
inference(resolution,[status(thm)],[p68_126,c2]) ).
cnf(c394,plain,
( p68(f19(f21(c83,c77),X1432),X1433)
| ~ p67(f16(c80,X1433),c82)
| ~ p66(f12(c78,c77),X1432) ),
inference(resolution,[status(thm)],[c226,c120]) ).
cnf(c928,plain,
( p68(f19(f21(c83,c77),c79),X1434)
| ~ p67(f16(c80,X1434),c82) ),
inference(resolution,[status(thm)],[c394,p66_41]) ).
cnf(c929,plain,
p68(f19(f21(c83,c77),c79),c81),
inference(resolution,[status(thm)],[c928,p67_42]) ).
cnf(c935,plain,
$false,
inference(resolution,[status(thm)],[c929,not_p68_46]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN719-1 : TPTP v8.1.2. Released v2.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n015.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 : Wed May 8 19:56:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.78/1.00 % Version: 1.5
% 0.78/1.00 % SZS status Unsatisfiable
% 0.78/1.00 % SZS output start CNFRefutation
% See solution above
% 0.78/1.00
% 0.78/1.00 % Initial clauses : 126
% 0.78/1.00 % Processed clauses : 340
% 0.78/1.00 % Factors computed : 40
% 0.78/1.00 % Resolvents computed: 897
% 0.78/1.00 % Tautologies deleted: 2
% 0.78/1.00 % Forward subsumed : 300
% 0.78/1.00 % Backward subsumed : 0
% 0.78/1.00 % -------- CPU Time ---------
% 0.78/1.00 % User time : 0.635 s
% 0.78/1.00 % System time : 0.017 s
% 0.78/1.00 % Total time : 0.652 s
%------------------------------------------------------------------------------