%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN686-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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 2.75s 2.96s
% Output : Refutation 2.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 16
% Syntax : Number of clauses : 49 ( 27 unt; 0 nHn; 37 RR)
% Number of literals : 80 ( 0 equ; 32 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-2 aty)
% Number of variables : 61 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(not_p30_22,negated_conjecture,
~ p30(f10(f12(c39,f7(c33,c34)),c35),c41),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p30_22) ).
cnf(p4_5,negated_conjecture,
p4(X6,X6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p4_5) ).
cnf(p30_39,negated_conjecture,
( p30(X145,X144)
| ~ p4(X143,X144)
| ~ p9(X142,X145)
| ~ p30(X142,X143) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p30_39) ).
cnf(p30_21,negated_conjecture,
p30(f10(f12(c39,c36),c37),c41),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p30_21) ).
cnf(c60,plain,
( p30(X327,X326)
| ~ p4(c41,X326)
| ~ p9(f10(f12(c39,c36),c37),X327) ),
inference(resolution,[status(thm)],[p30_39,p30_21]) ).
cnf(p4_27,negated_conjecture,
( p4(X51,X50)
| ~ p4(X52,X51)
| ~ p4(X52,X50) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p4_27) ).
cnf(c15,plain,
( p4(X56,X55)
| ~ p4(X55,X56) ),
inference(resolution,[status(thm)],[p4_27,p4_5]) ).
cnf(p4_19,negated_conjecture,
p4(f5(c32,c36),c37),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p4_19) ).
cnf(c14,plain,
( p4(X149,c37)
| ~ p4(f5(c32,c36),X149) ),
inference(resolution,[status(thm)],[p4_27,p4_19]) ).
cnf(p2_12,negated_conjecture,
p2(X13,X13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_12) ).
cnf(p3_6,negated_conjecture,
p3(X7,X7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_6) ).
cnf(p3_28,negated_conjecture,
( p3(X57,X58)
| ~ p3(X59,X57)
| ~ p3(X59,X58) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_28) ).
cnf(c21,plain,
( p3(X64,X63)
| ~ p3(X63,X64) ),
inference(resolution,[status(thm)],[p3_28,p3_6]) ).
cnf(p3_18,negated_conjecture,
p3(c42,f7(c33,c34)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_18) ).
cnf(c25,plain,
p3(f7(c33,c34),c42),
inference(resolution,[status(thm)],[c21,p3_18]) ).
cnf(p3_17,negated_conjecture,
p3(c36,f7(c33,c34)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_17) ).
cnf(c23,plain,
p3(f7(c33,c34),c36),
inference(resolution,[status(thm)],[c21,p3_17]) ).
cnf(c32,plain,
( p3(X164,c36)
| ~ p3(f7(c33,c34),X164) ),
inference(resolution,[status(thm)],[c23,p3_28]) ).
cnf(c74,plain,
p3(c42,c36),
inference(resolution,[status(thm)],[c32,c25]) ).
cnf(c79,plain,
p3(c36,c42),
inference(resolution,[status(thm)],[c74,c21]) ).
cnf(p4_50,negated_conjecture,
( p4(f5(X246,X247),f5(X245,X248))
| ~ p2(X246,X245)
| ~ p3(X247,X248) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p4_50) ).
cnf(c150,plain,
( p4(f5(X303,c36),f5(X304,c42))
| ~ p2(X303,X304) ),
inference(resolution,[status(thm)],[p4_50,c79]) ).
cnf(c227,plain,
p4(f5(X305,c36),f5(X305,c42)),
inference(resolution,[status(thm)],[c150,p2_12]) ).
cnf(c234,plain,
p4(f5(c32,c42),c37),
inference(resolution,[status(thm)],[c227,c14]) ).
cnf(c241,plain,
( p4(X314,c37)
| ~ p4(f5(c32,c42),X314) ),
inference(resolution,[status(thm)],[c234,p4_27]) ).
cnf(p4_20,negated_conjecture,
p4(f5(c32,f7(c33,c34)),c35),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p4_20) ).
cnf(c13,plain,
( p4(X321,c35)
| ~ p4(f5(c32,f7(c33,c34)),X321) ),
inference(resolution,[status(thm)],[p4_27,p4_20]) ).
cnf(c147,plain,
( p4(f5(X483,f7(c33,c34)),f5(X484,c42))
| ~ p2(X483,X484) ),
inference(resolution,[status(thm)],[p4_50,c25]) ).
cnf(c429,plain,
p4(f5(X487,f7(c33,c34)),f5(X487,c42)),
inference(resolution,[status(thm)],[c147,p2_12]) ).
cnf(c439,plain,
p4(f5(c32,c42),c35),
inference(resolution,[status(thm)],[c429,c13]) ).
cnf(c440,plain,
p4(c35,c37),
inference(resolution,[status(thm)],[c439,c241]) ).
cnf(c456,plain,
p4(c37,c35),
inference(resolution,[status(thm)],[c440,c15]) ).
cnf(p9_41,negated_conjecture,
( p9(f10(X160,X162),f10(X161,X159))
| ~ p4(X162,X159)
| ~ p8(X160,X161) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p9_41) ).
cnf(p11_1,negated_conjecture,
p11(X2,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p11_1) ).
cnf(p8_51,negated_conjecture,
( p8(f12(X258,X256),f12(X259,X257))
| ~ p11(X258,X259)
| ~ p3(X256,X257) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p8_51) ).
cnf(c171,plain,
( p8(f12(X333,c36),f12(X334,c42))
| ~ p11(X333,X334) ),
inference(resolution,[status(thm)],[p8_51,c79]) ).
cnf(c277,plain,
p8(f12(X336,c36),f12(X336,c42)),
inference(resolution,[status(thm)],[c171,p11_1]) ).
cnf(c281,plain,
( p9(f10(f12(X963,c36),X961),f10(f12(X963,c42),X962))
| ~ p4(X961,X962) ),
inference(resolution,[status(thm)],[c277,p9_41]) ).
cnf(c1403,plain,
p9(f10(f12(X1432,c36),c37),f10(f12(X1432,c42),c35)),
inference(resolution,[status(thm)],[c281,c456]) ).
cnf(c2615,plain,
( p30(f10(f12(c39,c42),c35),X1433)
| ~ p4(c41,X1433) ),
inference(resolution,[status(thm)],[c1403,c60]) ).
cnf(c2620,plain,
p30(f10(f12(c39,c42),c35),c41),
inference(resolution,[status(thm)],[c2615,p4_5]) ).
cnf(c2621,plain,
( p30(X2086,X2085)
| ~ p4(c41,X2085)
| ~ p9(f10(f12(c39,c42),c35),X2086) ),
inference(resolution,[status(thm)],[c2620,p30_39]) ).
cnf(c170,plain,
( p8(f12(X540,c42),f12(X541,f7(c33,c34)))
| ~ p11(X540,X541) ),
inference(resolution,[status(thm)],[p8_51,p3_18]) ).
cnf(c612,plain,
p8(f12(X622,c42),f12(X622,f7(c33,c34))),
inference(resolution,[status(thm)],[c170,p11_1]) ).
cnf(c717,plain,
( p9(f10(f12(X2164,c42),X2162),f10(f12(X2164,f7(c33,c34)),X2163))
| ~ p4(X2162,X2163) ),
inference(resolution,[status(thm)],[c612,p9_41]) ).
cnf(c4874,plain,
p9(f10(f12(X2406,c42),X2407),f10(f12(X2406,f7(c33,c34)),X2407)),
inference(resolution,[status(thm)],[c717,p4_5]) ).
cnf(c5608,plain,
( p30(f10(f12(c39,f7(c33,c34)),c35),X2465)
| ~ p4(c41,X2465) ),
inference(resolution,[status(thm)],[c4874,c2621]) ).
cnf(c5745,plain,
p30(f10(f12(c39,f7(c33,c34)),c35),c41),
inference(resolution,[status(thm)],[c5608,p4_5]) ).
cnf(c5746,plain,
$false,
inference(resolution,[status(thm)],[c5745,not_p30_22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN686-1 : TPTP v8.1.2. Released v2.5.0.
% 0.12/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n027.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 20:27:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 2.75/2.96 % Version: 1.5
% 2.75/2.96 % SZS status Unsatisfiable
% 2.75/2.96 % SZS output start CNFRefutation
% See solution above
% 2.75/2.96
% 2.75/2.96 % Initial clauses : 58
% 2.75/2.96 % Processed clauses : 752
% 2.75/2.96 % Factors computed : 16
% 2.75/2.96 % Resolvents computed: 5732
% 2.75/2.96 % Tautologies deleted: 1
% 2.75/2.96 % Forward subsumed : 911
% 2.75/2.96 % Backward subsumed : 0
% 2.75/2.96 % -------- CPU Time ---------
% 2.75/2.96 % User time : 2.601 s
% 2.75/2.96 % System time : 0.024 s
% 2.75/2.96 % Total time : 2.625 s
%------------------------------------------------------------------------------