%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN652-1 : TPTP v8.1.2. Released v2.5.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:48:37 EDT 2024
% Result : Unsatisfiable 0.45s 0.62s
% Output : Refutation 0.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 9
% Syntax : Number of clauses : 21 ( 14 unt; 0 nHn; 14 RR)
% Number of literals : 30 ( 0 equ; 10 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-2 aty)
% Number of variables : 25 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(not_p4_18,negated_conjecture,
~ p4(f5(c31,c33),f15(f17(c36,c31),c34)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p4_18) ).
cnf(p4_5,negated_conjecture,
p4(X6,X6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p4_5) ).
cnf(p4_23,negated_conjecture,
( p4(X51,X50)
| ~ p4(X49,X51)
| ~ p4(X49,X50) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p4_23) ).
cnf(c14,plain,
( p4(X58,X57)
| ~ p4(X57,X58) ),
inference(resolution,[status(thm)],[p4_23,p4_5]) ).
cnf(p27_17,negated_conjecture,
p27(f8(f10(c28,f13(c29,c30)),c32),c33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p27_17) ).
cnf(p4_46,negated_conjecture,
( p4(f5(c31,X237),f5(c31,X238))
| ~ p27(f8(f10(c28,f13(c29,c30)),X237),X238) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p4_46) ).
cnf(c83,plain,
p4(f5(c31,c32),f5(c31,c33)),
inference(resolution,[status(thm)],[p4_46,p27_17]) ).
cnf(c85,plain,
( p4(X244,f5(c31,c33))
| ~ p4(f5(c31,c32),X244) ),
inference(resolution,[status(thm)],[c83,p4_23]) ).
cnf(p4_34,negated_conjecture,
p4(f15(f17(c36,X132),f5(c35,X133)),f5(X132,X133)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p4_34) ).
cnf(c49,plain,
( p4(X247,f5(X248,X246))
| ~ p4(f15(f17(c36,X248),f5(c35,X246)),X247) ),
inference(resolution,[status(thm)],[p4_34,p4_23]) ).
cnf(p14_14,negated_conjecture,
p14(X15,X15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p14_14) ).
cnf(p4_16,negated_conjecture,
p4(c34,f5(c35,c32)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p4_16) ).
cnf(p4_41,negated_conjecture,
( p4(f15(X185,X186),f15(X188,X187))
| ~ p14(X185,X188)
| ~ p4(X186,X187) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p4_41) ).
cnf(c65,plain,
( p4(f15(X256,c34),f15(X255,f5(c35,c32)))
| ~ p14(X256,X255) ),
inference(resolution,[status(thm)],[p4_41,p4_16]) ).
cnf(c110,plain,
p4(f15(X257,c34),f15(X257,f5(c35,c32))),
inference(resolution,[status(thm)],[c65,p14_14]) ).
cnf(c113,plain,
p4(f15(X258,f5(c35,c32)),f15(X258,c34)),
inference(resolution,[status(thm)],[c110,c14]) ).
cnf(c116,plain,
p4(f15(f17(c36,X259),c34),f5(X259,c32)),
inference(resolution,[status(thm)],[c113,c49]) ).
cnf(c120,plain,
p4(f5(X265,c32),f15(f17(c36,X265),c34)),
inference(resolution,[status(thm)],[c116,c14]) ).
cnf(c125,plain,
p4(f15(f17(c36,c31),c34),f5(c31,c33)),
inference(resolution,[status(thm)],[c120,c85]) ).
cnf(c137,plain,
p4(f5(c31,c33),f15(f17(c36,c31),c34)),
inference(resolution,[status(thm)],[c125,c14]) ).
cnf(c155,plain,
$false,
inference(resolution,[status(thm)],[c137,not_p4_18]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SYN652-1 : TPTP v8.1.2. Released v2.5.0.
% 0.06/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 20:13:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.45/0.62 % Version: 1.5
% 0.45/0.62 % SZS status Unsatisfiable
% 0.45/0.62 % SZS output start CNFRefutation
% See solution above
% 0.45/0.62
% 0.45/0.62 % Initial clauses : 47
% 0.45/0.62 % Processed clauses : 99
% 0.45/0.62 % Factors computed : 15
% 0.45/0.62 % Resolvents computed: 144
% 0.45/0.62 % Tautologies deleted: 0
% 0.45/0.62 % Forward subsumed : 64
% 0.45/0.62 % Backward subsumed : 0
% 0.45/0.62 % -------- CPU Time ---------
% 0.45/0.62 % User time : 0.256 s
% 0.45/0.62 % System time : 0.015 s
% 0.45/0.62 % Total time : 0.271 s
%------------------------------------------------------------------------------