%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN672-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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:39 EDT 2024
% Result : Unsatisfiable 0.46s 0.69s
% Output : Refutation 0.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 10
% Syntax : Number of clauses : 19 ( 11 unt; 2 nHn; 14 RR)
% Number of literals : 32 ( 0 equ; 13 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-2 aty)
% Number of variables : 29 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(not_p30_40,negated_conjecture,
~ p30(f10(f12(c32,c33),f14(c35,c39)),f4(f7(c34,c35),c40)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p30_40) ).
cnf(p3_6,negated_conjecture,
p3(X7,X7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_6) ).
cnf(p30_39,negated_conjecture,
( p30(X164,X166)
| ~ p30(X167,X165)
| ~ p9(X167,X164)
| ~ p3(X165,X166) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p30_39) ).
cnf(c55,plain,
( p30(X170,X168)
| ~ p30(X169,X168)
| ~ p9(X169,X170) ),
inference(resolution,[status(thm)],[p30_39,p3_6]) ).
cnf(p3_37,negated_conjecture,
p3(f4(f7(c34,X162),f14(c38,X163)),f14(X162,X163)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_37) ).
cnf(p8_3,negated_conjecture,
p8(X4,X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p8_3) ).
cnf(p9_42,negated_conjecture,
( p9(f10(X182,X183),f10(X184,X185))
| ~ p3(X183,X185)
| ~ p8(X182,X184) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p9_42) ).
cnf(c61,plain,
( p9(f10(X186,X188),f10(X186,X187))
| ~ p3(X188,X187) ),
inference(resolution,[status(thm)],[p9_42,p8_3]) ).
cnf(c63,plain,
p9(f10(X298,f4(f7(c34,X297),f14(c38,X296))),f10(X298,f14(X297,X296))),
inference(resolution,[status(thm)],[c61,p3_37]) ).
cnf(c101,plain,
( p30(f10(X374,f14(X371,X373)),X372)
| ~ p30(f10(X374,f4(f7(c34,X371),f14(c38,X373))),X372) ),
inference(resolution,[status(thm)],[c63,c55]) ).
cnf(p30_54,negated_conjecture,
( p30(f10(f12(c32,c33),f4(f7(c34,c35),X292)),f4(f7(c34,c35),X293))
| ~ p30(f10(f12(c32,c33),X292),X293) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p30_54) ).
cnf(not_p3_18,negated_conjecture,
~ p3(c40,f14(c38,c39)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p3_18) ).
cnf(p31_19,negated_conjecture,
p31(f20(c36,c39),f17(c37,c40)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p31_19) ).
cnf(p3_53,negated_conjecture,
( p3(X278,f14(c38,X279))
| p30(f10(f12(c32,c33),f14(c38,X279)),X278)
| ~ p31(f20(c36,X279),f17(c37,X278)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_53) ).
cnf(c96,plain,
( p3(c40,f14(c38,c39))
| p30(f10(f12(c32,c33),f14(c38,c39)),c40) ),
inference(resolution,[status(thm)],[p3_53,p31_19]) ).
cnf(c158,plain,
p30(f10(f12(c32,c33),f14(c38,c39)),c40),
inference(resolution,[status(thm)],[c96,not_p3_18]) ).
cnf(c160,plain,
p30(f10(f12(c32,c33),f4(f7(c34,c35),f14(c38,c39))),f4(f7(c34,c35),c40)),
inference(resolution,[status(thm)],[c158,p30_54]) ).
cnf(c249,plain,
p30(f10(f12(c32,c33),f14(c35,c39)),f4(f7(c34,c35),c40)),
inference(resolution,[status(thm)],[c160,c101]) ).
cnf(c252,plain,
$false,
inference(resolution,[status(thm)],[c249,not_p30_40]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYN672-1 : TPTP v8.1.2. Released v2.5.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n009.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed May 8 20:16:53 EDT 2024
% 0.13/0.33 % CPUTime :
% 0.46/0.69 % Version: 1.5
% 0.46/0.69 % SZS status Unsatisfiable
% 0.46/0.69 % SZS output start CNFRefutation
% See solution above
% 0.46/0.69
% 0.46/0.69 % Initial clauses : 54
% 0.46/0.69 % Processed clauses : 147
% 0.46/0.69 % Factors computed : 17
% 0.46/0.69 % Resolvents computed: 238
% 0.46/0.69 % Tautologies deleted: 1
% 0.46/0.69 % Forward subsumed : 93
% 0.46/0.69 % Backward subsumed : 1
% 0.46/0.69 % -------- CPU Time ---------
% 0.46/0.69 % User time : 0.321 s
% 0.46/0.69 % System time : 0.017 s
% 0.46/0.69 % Total time : 0.338 s
%------------------------------------------------------------------------------