%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN036-4 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:47:07 EDT 2024
% Result : Unsatisfiable 0.77s 1.01s
% Output : Refutation 0.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 17
% Syntax : Number of clauses : 77 ( 6 unt; 53 nHn; 24 RR)
% Number of literals : 273 ( 0 equ; 95 neg)
% Maximal clause size : 6 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-1 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-1 aty)
% Number of variables : 119 ( 90 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_1,negated_conjecture,
( ~ p(cx)
| ~ q(cw)
| p(X3)
| q(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1) ).
cnf(clause_4,negated_conjecture,
( ~ p(X8)
| ~ q(X9)
| p(cx)
| q(cw) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4) ).
cnf(clause_13,negated_conjecture,
( ~ p(X27)
| ~ p(fy5(X25))
| ~ q(X26)
| p(X24)
| q(cw) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_13) ).
cnf(c0,plain,
( ~ p(fy5(X30))
| ~ q(X29)
| p(X28)
| q(cw) ),
inference(factor,[status(thm)],[clause_13]) ).
cnf(clause_32,negated_conjecture,
( p(cx)
| p(X85)
| p(fy5(X85))
| q(cw)
| q(X84)
| q(fz5(X84)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_32) ).
cnf(c1,plain,
( p(cx)
| p(fy5(cx))
| q(cw)
| q(X86)
| q(fz5(X86)) ),
inference(factor,[status(thm)],[clause_32]) ).
cnf(c64,plain,
( p(cx)
| p(fy5(cx))
| q(cw)
| q(fz5(cw)) ),
inference(factor,[status(thm)],[c1]) ).
cnf(c121,plain,
( p(cx)
| q(cw)
| q(fz5(cw))
| ~ q(X94)
| p(X93) ),
inference(resolution,[status(thm)],[c64,c0]) ).
cnf(clause_15,negated_conjecture,
( ~ p(X46)
| p(cx)
| q(cw)
| q(X47)
| q(fz(X47)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_15) ).
cnf(c122,plain,
( p(cx)
| q(cw)
| q(fz5(cw))
| q(X113)
| q(fz(X113)) ),
inference(resolution,[status(thm)],[c64,clause_15]) ).
cnf(c353,plain,
( p(cx)
| q(cw)
| q(fz5(cw))
| q(fz(cw)) ),
inference(factor,[status(thm)],[c122]) ).
cnf(c461,plain,
( p(cx)
| q(cw)
| q(fz5(cw))
| p(X120) ),
inference(resolution,[status(thm)],[c353,c121]) ).
cnf(c486,plain,
( p(cx)
| q(cw)
| q(fz5(cw)) ),
inference(factor,[status(thm)],[c461]) ).
cnf(c552,plain,
( p(cx)
| q(cw)
| ~ p(X121) ),
inference(resolution,[status(thm)],[c486,clause_4]) ).
cnf(clause_20,negated_conjecture,
( ~ q(X53)
| p(cx)
| p(X52)
| p(fy(X52))
| q(cw) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_20) ).
cnf(c548,plain,
( p(cx)
| q(cw)
| p(X135)
| p(fy(X135)) ),
inference(resolution,[status(thm)],[c486,clause_20]) ).
cnf(c602,plain,
( p(cx)
| q(cw)
| p(X136) ),
inference(resolution,[status(thm)],[c548,c552]) ).
cnf(c605,plain,
( p(cx)
| q(cw) ),
inference(factor,[status(thm)],[c602]) ).
cnf(clause_2,negated_conjecture,
( ~ p(cx)
| ~ q(X5)
| p(X4)
| q(cw) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2) ).
cnf(clause_10,negated_conjecture,
( ~ p(cx)
| p(X44)
| q(cw)
| q(X45)
| q(fz(X45)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_10) ).
cnf(c627,plain,
( q(cw)
| p(X156)
| q(X155)
| q(fz(X155)) ),
inference(resolution,[status(thm)],[c605,clause_10]) ).
cnf(c642,plain,
( q(cw)
| p(X157)
| q(fz(cw)) ),
inference(factor,[status(thm)],[c627]) ).
cnf(c702,plain,
( q(cw)
| p(X159)
| ~ p(cx)
| p(X158) ),
inference(resolution,[status(thm)],[c642,clause_2]) ).
cnf(c708,plain,
( q(cw)
| p(X164)
| p(X165) ),
inference(resolution,[status(thm)],[c702,c605]) ).
cnf(c710,plain,
( q(cw)
| p(X166) ),
inference(factor,[status(thm)],[c708]) ).
cnf(c731,plain,
( p(X179)
| ~ p(cx)
| p(X178)
| q(X177) ),
inference(resolution,[status(thm)],[c710,clause_1]) ).
cnf(clause_3,negated_conjecture,
( ~ p(X7)
| ~ q(cw)
| p(cx)
| q(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3) ).
cnf(c630,plain,
( p(cx)
| ~ p(X137)
| q(X138) ),
inference(resolution,[status(thm)],[c605,clause_3]) ).
cnf(clause_19,negated_conjecture,
( ~ q(cw)
| p(cx)
| p(X50)
| p(fy(X50))
| q(X51) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_19) ).
cnf(c635,plain,
( p(cx)
| p(X199)
| p(fy(X199))
| q(X200) ),
inference(resolution,[status(thm)],[c605,clause_19]) ).
cnf(c744,plain,
( p(cx)
| p(fy(cx))
| q(X201) ),
inference(factor,[status(thm)],[c635]) ).
cnf(c774,plain,
( p(cx)
| q(X206)
| q(X205) ),
inference(resolution,[status(thm)],[c744,c630]) ).
cnf(c789,plain,
( p(cx)
| q(X207) ),
inference(factor,[status(thm)],[c774]) ).
cnf(c818,plain,
( q(X211)
| p(X209)
| p(X210)
| q(X208) ),
inference(resolution,[status(thm)],[c789,c731]) ).
cnf(c832,plain,
( q(X213)
| p(X212)
| p(X214) ),
inference(factor,[status(thm)],[c818]) ).
cnf(c868,plain,
( q(X216)
| p(X215) ),
inference(factor,[status(thm)],[c832]) ).
cnf(clause_5,negated_conjecture,
( ~ p(cx)
| ~ p(X14)
| ~ p(fy5(X14))
| ~ q(cw)
| q(X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
cnf(c894,plain,
( q(X358)
| ~ p(cx)
| ~ p(X356)
| ~ q(cw)
| q(X357) ),
inference(resolution,[status(thm)],[c868,clause_5]) ).
cnf(clause_6,negated_conjecture,
( ~ p(cx)
| ~ p(X31)
| ~ p(fy5(X31))
| ~ q(X32)
| q(cw) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6) ).
cnf(c738,plain,
( q(cw)
| ~ p(cx)
| ~ p(X188)
| ~ q(X187) ),
inference(resolution,[status(thm)],[c710,clause_6]) ).
cnf(clause_22,negated_conjecture,
( ~ p(cx)
| ~ p(X72)
| ~ p(fy(X72))
| q(cw)
| q(X73)
| q(fz(X73)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_22) ).
cnf(c736,plain,
( q(cw)
| ~ p(cx)
| ~ p(X497)
| q(X496)
| q(fz(X496)) ),
inference(resolution,[status(thm)],[c710,clause_22]) ).
cnf(c904,plain,
( q(cw)
| ~ p(cx)
| q(X502)
| q(fz(X502)) ),
inference(factor,[status(thm)],[c736]) ).
cnf(c906,plain,
( q(cw)
| q(X503)
| q(fz(X503))
| q(X504) ),
inference(resolution,[status(thm)],[c904,c868]) ).
cnf(c908,plain,
( q(cw)
| q(X505)
| q(fz(X505)) ),
inference(factor,[status(thm)],[c906]) ).
cnf(c931,plain,
( q(cw)
| q(fz(cw)) ),
inference(factor,[status(thm)],[c908]) ).
cnf(c949,plain,
( q(cw)
| ~ p(cx)
| ~ p(X506) ),
inference(resolution,[status(thm)],[c931,c738]) ).
cnf(c951,plain,
( q(cw)
| ~ p(cx) ),
inference(factor,[status(thm)],[c949]) ).
cnf(c953,plain,
( q(cw)
| q(X510) ),
inference(resolution,[status(thm)],[c951,c868]) ).
cnf(c954,plain,
q(cw),
inference(factor,[status(thm)],[c953]) ).
cnf(c965,plain,
( q(X540)
| ~ p(cx)
| ~ p(X538)
| q(X539) ),
inference(resolution,[status(thm)],[c954,c894]) ).
cnf(c969,plain,
( q(X541)
| ~ p(cx)
| q(X542) ),
inference(factor,[status(thm)],[c965]) ).
cnf(c971,plain,
( q(X543)
| q(X544)
| q(X545) ),
inference(resolution,[status(thm)],[c969,c868]) ).
cnf(c972,plain,
( q(X546)
| q(X547) ),
inference(factor,[status(thm)],[c971]) ).
cnf(c984,plain,
q(X548),
inference(factor,[status(thm)],[c972]) ).
cnf(clause_7,negated_conjecture,
( ~ p(cx)
| ~ q(cw)
| ~ q(X42)
| ~ q(fz5(X42))
| p(X43) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_7) ).
cnf(c992,plain,
( ~ p(cx)
| ~ q(cw)
| ~ q(X569)
| p(X568) ),
inference(resolution,[status(thm)],[c984,clause_7]) ).
cnf(c994,plain,
( ~ p(cx)
| ~ q(cw)
| p(X570) ),
inference(factor,[status(thm)],[c992]) ).
cnf(c996,plain,
( ~ p(cx)
| p(X571) ),
inference(resolution,[status(thm)],[c994,c984]) ).
cnf(clause_16,negated_conjecture,
( ~ p(X49)
| ~ q(cw)
| ~ q(X48)
| ~ q(fz5(X48))
| p(cx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_16) ).
cnf(c831,plain,
( p(cx)
| ~ p(X231)
| ~ q(cw)
| ~ q(X232) ),
inference(resolution,[status(thm)],[c789,clause_16]) ).
cnf(c895,plain,
( p(cx)
| ~ p(X236)
| ~ q(cw) ),
inference(factor,[status(thm)],[c831]) ).
cnf(c964,plain,
( p(cx)
| ~ p(X511) ),
inference(resolution,[status(thm)],[c954,c895]) ).
cnf(clause_30,negated_conjecture,
( ~ q(cw)
| ~ q(X81)
| ~ q(fz(X81))
| p(cx)
| p(X80)
| p(fy(X80)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_30) ).
cnf(c829,plain,
( p(cx)
| ~ q(cw)
| ~ q(X620)
| p(X619)
| p(fy(X619)) ),
inference(resolution,[status(thm)],[c789,clause_30]) ).
cnf(c997,plain,
( p(cx)
| ~ q(cw)
| p(X621)
| p(fy(X621)) ),
inference(factor,[status(thm)],[c829]) ).
cnf(c999,plain,
( p(cx)
| p(X627)
| p(fy(X627)) ),
inference(resolution,[status(thm)],[c997,c984]) ).
cnf(c1005,plain,
( p(cx)
| p(X628) ),
inference(resolution,[status(thm)],[c999,c964]) ).
cnf(c1006,plain,
p(cx),
inference(factor,[status(thm)],[c1005]) ).
cnf(c1011,plain,
p(X629),
inference(resolution,[status(thm)],[c1006,c996]) ).
cnf(clause_23,negated_conjecture,
( ~ p(cx)
| ~ p(X75)
| ~ p(fy5(X75))
| ~ q(cw)
| ~ q(X74)
| ~ q(fz5(X74)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_23) ).
cnf(c991,plain,
( ~ p(cx)
| ~ p(X697)
| ~ p(fy5(X697))
| ~ q(cw)
| ~ q(X696) ),
inference(resolution,[status(thm)],[c984,clause_23]) ).
cnf(c1012,plain,
( ~ p(cx)
| ~ p(X699)
| ~ q(cw)
| ~ q(X698) ),
inference(resolution,[status(thm)],[c991,c1011]) ).
cnf(c1013,plain,
( ~ p(cx)
| ~ p(X700)
| ~ q(cw) ),
inference(factor,[status(thm)],[c1012]) ).
cnf(c1015,plain,
( ~ p(cx)
| ~ p(X701) ),
inference(resolution,[status(thm)],[c1013,c984]) ).
cnf(c1016,plain,
~ p(cx),
inference(factor,[status(thm)],[c1015]) ).
cnf(c1018,plain,
$false,
inference(resolution,[status(thm)],[c1016,c1011]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SYN036-4 : TPTP v8.1.2. Released v1.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n025.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Wed May 8 20:18:53 EDT 2024
% 0.15/0.35 % CPUTime :
% 0.77/1.01 % Version: 1.5
% 0.77/1.01 % SZS status Unsatisfiable
% 0.77/1.01 % SZS output start CNFRefutation
% See solution above
% 0.77/1.01
% 0.77/1.01 % Initial clauses : 32
% 0.77/1.01 % Processed clauses : 103
% 0.77/1.01 % Factors computed : 45
% 0.77/1.01 % Resolvents computed: 974
% 0.77/1.01 % Tautologies deleted: 44
% 0.77/1.01 % Forward subsumed : 160
% 0.77/1.01 % Backward subsumed : 100
% 0.77/1.01 % -------- CPU Time ---------
% 0.77/1.01 % User time : 0.632 s
% 0.77/1.01 % System time : 0.015 s
% 0.77/1.01 % Total time : 0.647 s
%------------------------------------------------------------------------------