%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN784-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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:49:00 EDT 2024
% Result : Unsatisfiable 76.22s 76.38s
% Output : Refutation 76.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 92
% Number of leaves : 31
% Syntax : Number of clauses : 349 ( 7 unt; 284 nHn; 238 RR)
% Number of literals : 1382 ( 0 equ; 536 neg)
% Maximal clause size : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 0 con; 1-1 aty)
% Number of variables : 480 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssRr(skf3(X2),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause4,negated_conjecture,
( ~ ssRr(X7,X8)
| ~ ssPv4(X8)
| ssPv2(X7)
| ssPv2(X8)
| ssPv3(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(c3,plain,
( ~ ssPv4(X11)
| ssPv2(skf3(X11))
| ssPv2(X11)
| ssPv3(X11) ),
inference(resolution,[status(thm)],[clause4,clause1]) ).
cnf(clause3,negated_conjecture,
( ~ ssRr(X4,X5)
| ssPv4(X4)
| ssPv2(X5)
| ssPv3(X5)
| ssPv4(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c1,plain,
( ssPv4(skf3(X6))
| ssPv2(X6)
| ssPv3(X6)
| ssPv4(X6) ),
inference(resolution,[status(thm)],[clause3,clause1]) ).
cnf(clause2,negated_conjecture,
ssRr(X3,skf2(X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(c0,plain,
( ssPv4(X31)
| ssPv2(skf2(X31))
| ssPv3(skf2(X31))
| ssPv4(skf2(X31)) ),
inference(resolution,[status(thm)],[clause3,clause2]) ).
cnf(c2,plain,
( ~ ssPv4(skf2(X32))
| ssPv2(X32)
| ssPv2(skf2(X32))
| ssPv3(skf2(X32)) ),
inference(resolution,[status(thm)],[clause4,clause2]) ).
cnf(c57,plain,
( ssPv2(X33)
| ssPv2(skf2(X33))
| ssPv3(skf2(X33))
| ssPv4(X33) ),
inference(resolution,[status(thm)],[c2,c0]) ).
cnf(clause10,negated_conjecture,
( ~ ssRr(X35,X36)
| ~ ssRr(X37,X36)
| ~ ssPv2(X36)
| ssPv3(X35)
| ssPv2(X37)
| ssPv3(X36) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c70,plain,
( ~ ssRr(X38,X39)
| ~ ssPv2(X39)
| ssPv3(X38)
| ssPv2(X38)
| ssPv3(X39) ),
inference(factor,[status(thm)],[clause10]) ).
cnf(c73,plain,
( ~ ssPv2(skf2(X40))
| ssPv3(X40)
| ssPv2(X40)
| ssPv3(skf2(X40)) ),
inference(resolution,[status(thm)],[c70,clause2]) ).
cnf(c76,plain,
( ssPv3(X41)
| ssPv2(X41)
| ssPv3(skf2(X41))
| ssPv4(X41) ),
inference(resolution,[status(thm)],[c73,c57]) ).
cnf(clause19,negated_conjecture,
( ~ ssRr(X120,X121)
| ~ ssPv4(X120)
| ~ ssRr(X121,X122)
| ~ ssPv3(X122)
| ssPv2(X121)
| ssPv4(X121) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c317,plain,
( ~ ssRr(X184,X183)
| ~ ssPv4(X184)
| ~ ssPv3(skf2(X183))
| ssPv2(X183)
| ssPv4(X183) ),
inference(resolution,[status(thm)],[clause19,clause2]) ).
cnf(c473,plain,
( ~ ssRr(X189,X190)
| ~ ssPv4(X189)
| ssPv2(X190)
| ssPv4(X190)
| ssPv3(X190) ),
inference(resolution,[status(thm)],[c317,c76]) ).
cnf(c486,plain,
( ~ ssPv4(skf3(X191))
| ssPv2(X191)
| ssPv4(X191)
| ssPv3(X191) ),
inference(resolution,[status(thm)],[c473,clause1]) ).
cnf(c495,plain,
( ssPv2(X192)
| ssPv4(X192)
| ssPv3(X192) ),
inference(resolution,[status(thm)],[c486,c1]) ).
cnf(c516,plain,
( ssPv2(X193)
| ssPv3(X193)
| ssPv2(skf3(X193)) ),
inference(resolution,[status(thm)],[c495,c3]) ).
cnf(clause18,negated_conjecture,
( ~ ssRr(X110,X111)
| ~ ssPv1(X110)
| ~ ssRr(X112,X111)
| ~ ssPv4(X111)
| ssPv3(X112)
| ssPv2(X111) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c301,plain,
( ~ ssRr(X114,X115)
| ~ ssPv1(X114)
| ~ ssPv4(X115)
| ssPv3(X114)
| ssPv2(X115) ),
inference(factor,[status(thm)],[clause18]) ).
cnf(c305,plain,
( ~ ssPv1(skf3(X117))
| ~ ssPv4(X117)
| ssPv3(skf3(X117))
| ssPv2(X117) ),
inference(resolution,[status(thm)],[c301,clause1]) ).
cnf(clause35,negated_conjecture,
( ~ ssRr(X267,X269)
| ~ ssPv4(X267)
| ~ ssRr(X270,X269)
| ~ ssPv2(X270)
| ~ ssRr(X268,X269)
| ssPv1(X268)
| ssPv2(X269) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c850,plain,
( ~ ssRr(X625,X626)
| ~ ssPv4(X625)
| ~ ssRr(X624,X626)
| ~ ssPv2(X624)
| ssPv1(X625)
| ssPv2(X626) ),
inference(factor,[status(thm)],[clause35]) ).
cnf(c2466,plain,
( ~ ssRr(X633,X634)
| ~ ssPv4(X633)
| ~ ssPv2(skf3(X634))
| ssPv1(X633)
| ssPv2(X634) ),
inference(resolution,[status(thm)],[c850,clause1]) ).
cnf(c2532,plain,
( ~ ssRr(X637,X636)
| ~ ssPv4(X637)
| ssPv1(X637)
| ssPv2(X636)
| ssPv3(X636) ),
inference(resolution,[status(thm)],[c2466,c516]) ).
cnf(c2545,plain,
( ~ ssPv4(skf3(X639))
| ssPv1(skf3(X639))
| ssPv2(X639)
| ssPv3(X639) ),
inference(resolution,[status(thm)],[c2532,clause1]) ).
cnf(clause15,negated_conjecture,
( ~ ssRr(X83,X84)
| ~ ssPv3(X83)
| ~ ssRr(X85,X84)
| ~ ssPv4(X84)
| ssPv4(X85)
| ssPv3(X84) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c202,plain,
( ~ ssRr(X87,X88)
| ~ ssPv3(X87)
| ~ ssPv4(X88)
| ssPv4(X87)
| ssPv3(X88) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c218,plain,
( ~ ssPv3(skf3(X91))
| ~ ssPv4(X91)
| ssPv4(skf3(X91))
| ssPv3(X91) ),
inference(resolution,[status(thm)],[c202,clause1]) ).
cnf(clause16,negated_conjecture,
( ~ ssRr(X92,X93)
| ~ ssPv4(X93)
| ~ ssRr(X92,X94)
| ~ ssPv2(X92)
| ssPv1(X94)
| ssPv3(X92) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c238,plain,
( ~ ssRr(X99,X98)
| ~ ssPv4(X98)
| ~ ssPv2(X99)
| ssPv1(X98)
| ssPv3(X99) ),
inference(factor,[status(thm)],[clause16]) ).
cnf(c271,plain,
( ~ ssPv4(X106)
| ~ ssPv2(skf3(X106))
| ssPv1(X106)
| ssPv3(skf3(X106)) ),
inference(resolution,[status(thm)],[c238,clause1]) ).
cnf(c74,plain,
( ~ ssPv2(X42)
| ssPv3(skf3(X42))
| ssPv2(skf3(X42))
| ssPv3(X42) ),
inference(resolution,[status(thm)],[c70,clause1]) ).
cnf(c529,plain,
( ssPv3(X200)
| ssPv2(skf3(X200))
| ssPv3(skf3(X200)) ),
inference(resolution,[status(thm)],[c516,c74]) ).
cnf(c596,plain,
( ssPv3(X208)
| ssPv3(skf3(X208))
| ~ ssPv4(X208)
| ssPv1(X208) ),
inference(resolution,[status(thm)],[c529,c271]) ).
cnf(clause8,negated_conjecture,
( ~ ssRr(X18,X19)
| ~ ssRr(X18,X20)
| ssPv4(X19)
| ssPv3(X20)
| ssPv3(X18)
| ssPv4(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c16,plain,
( ~ ssRr(X23,X24)
| ssPv4(X24)
| ssPv3(X24)
| ssPv3(X23)
| ssPv4(X23) ),
inference(factor,[status(thm)],[clause8]) ).
cnf(c25,plain,
( ssPv4(X26)
| ssPv3(X26)
| ssPv3(skf3(X26))
| ssPv4(skf3(X26)) ),
inference(resolution,[status(thm)],[c16,clause1]) ).
cnf(clause21,negated_conjecture,
( ~ ssRr(X137,X138)
| ~ ssPv2(X138)
| ~ ssRr(X137,X139)
| ~ ssPv2(X137)
| ~ ssPv4(X137)
| ssPv4(X139) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c398,plain,
( ~ ssRr(X141,X142)
| ~ ssPv2(X142)
| ~ ssPv2(X141)
| ~ ssPv4(X141)
| ssPv4(X142) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c402,plain,
( ~ ssPv2(X144)
| ~ ssPv2(skf3(X144))
| ~ ssPv4(skf3(X144))
| ssPv4(X144) ),
inference(resolution,[status(thm)],[c398,clause1]) ).
cnf(c414,plain,
( ~ ssPv2(X419)
| ~ ssPv2(skf3(X419))
| ssPv4(X419)
| ssPv3(X419)
| ssPv3(skf3(X419)) ),
inference(resolution,[status(thm)],[c402,c25]) ).
cnf(c1325,plain,
( ~ ssPv2(X420)
| ssPv4(X420)
| ssPv3(X420)
| ssPv3(skf3(X420)) ),
inference(resolution,[status(thm)],[c414,c529]) ).
cnf(c1341,plain,
( ssPv4(X421)
| ssPv3(X421)
| ssPv3(skf3(X421)) ),
inference(resolution,[status(thm)],[c1325,c495]) ).
cnf(c1366,plain,
( ssPv3(X422)
| ssPv3(skf3(X422))
| ssPv1(X422) ),
inference(resolution,[status(thm)],[c1341,c596]) ).
cnf(clause6,negated_conjecture,
( ~ ssRr(X13,X14)
| ~ ssPv3(X13)
| ~ ssPv4(X13)
| ssPv1(X14)
| ssPv1(X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c11,plain,
( ~ ssPv3(skf3(X48))
| ~ ssPv4(skf3(X48))
| ssPv1(X48)
| ssPv1(skf3(X48)) ),
inference(resolution,[status(thm)],[clause6,clause1]) ).
cnf(c607,plain,
( ssPv3(X247)
| ssPv3(skf3(X247))
| ssPv1(X247)
| ssPv4(skf3(X247)) ),
inference(resolution,[status(thm)],[c596,c25]) ).
cnf(c730,plain,
( ssPv3(X248)
| ssPv1(X248)
| ssPv4(skf3(X248))
| ~ ssPv4(X248) ),
inference(resolution,[status(thm)],[c607,c218]) ).
cnf(c761,plain,
( ssPv3(X253)
| ssPv1(X253)
| ssPv4(skf3(X253))
| ssPv2(X253) ),
inference(resolution,[status(thm)],[c730,c495]) ).
cnf(c787,plain,
( ssPv3(X491)
| ssPv1(X491)
| ssPv2(X491)
| ~ ssPv3(skf3(X491))
| ssPv1(skf3(X491)) ),
inference(resolution,[status(thm)],[c761,c11]) ).
cnf(c1890,plain,
( ssPv3(X492)
| ssPv1(X492)
| ssPv2(X492)
| ssPv1(skf3(X492)) ),
inference(resolution,[status(thm)],[c787,c1366]) ).
cnf(clause17,negated_conjecture,
( ~ ssRr(X101,X102)
| ~ ssPv2(X102)
| ~ ssRr(X101,X103)
| ~ ssPv1(X101)
| ssPv4(X103)
| ssPv3(X101) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c272,plain,
( ~ ssRr(X107,X108)
| ~ ssPv2(X108)
| ~ ssPv1(X107)
| ssPv4(X108)
| ssPv3(X107) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c292,plain,
( ~ ssPv2(skf2(X109))
| ~ ssPv1(X109)
| ssPv4(skf2(X109))
| ssPv3(X109) ),
inference(resolution,[status(thm)],[c272,clause2]) ).
cnf(clause27,negated_conjecture,
( ~ ssRr(X194,X196)
| ~ ssRr(X196,X197)
| ~ ssRr(X196,X195)
| ssPv1(X194)
| ssPv4(X197)
| ssPv2(X195)
| ssPv3(X196) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c546,plain,
( ~ ssRr(X568,X569)
| ~ ssRr(X569,X567)
| ssPv1(X568)
| ssPv4(X567)
| ssPv2(X567)
| ssPv3(X569) ),
inference(factor,[status(thm)],[clause27]) ).
cnf(c2425,plain,
( ~ ssRr(X768,X769)
| ssPv1(X768)
| ssPv4(skf2(X769))
| ssPv2(skf2(X769))
| ssPv3(X769) ),
inference(resolution,[status(thm)],[c546,clause2]) ).
cnf(c4213,plain,
( ssPv1(skf3(X770))
| ssPv4(skf2(X770))
| ssPv2(skf2(X770))
| ssPv3(X770) ),
inference(resolution,[status(thm)],[c2425,clause1]) ).
cnf(c4269,plain,
( ssPv1(skf3(X773))
| ssPv4(skf2(X773))
| ssPv3(X773)
| ~ ssPv1(X773) ),
inference(resolution,[status(thm)],[c4213,c292]) ).
cnf(c4317,plain,
( ssPv1(skf3(X775))
| ssPv4(skf2(X775))
| ssPv3(X775)
| ssPv2(X775) ),
inference(resolution,[status(thm)],[c4269,c1890]) ).
cnf(c4409,plain,
( ssPv4(skf2(X791))
| ssPv3(X791)
| ssPv2(X791)
| ~ ssPv4(X791)
| ssPv3(skf3(X791)) ),
inference(resolution,[status(thm)],[c4317,c305]) ).
cnf(c4779,plain,
( ssPv4(skf2(X792))
| ssPv3(X792)
| ssPv2(X792)
| ssPv3(skf3(X792)) ),
inference(resolution,[status(thm)],[c4409,c495]) ).
cnf(c4873,plain,
( ssPv4(skf2(X818))
| ssPv3(X818)
| ssPv2(X818)
| ~ ssPv4(X818)
| ssPv4(skf3(X818)) ),
inference(resolution,[status(thm)],[c4779,c218]) ).
cnf(c5026,plain,
( ssPv4(skf2(X821))
| ssPv3(X821)
| ssPv2(X821)
| ssPv4(skf3(X821)) ),
inference(resolution,[status(thm)],[c4873,c495]) ).
cnf(c518,plain,
( ssPv2(skf2(X198))
| ssPv3(skf2(X198))
| ssPv2(X198) ),
inference(resolution,[status(thm)],[c495,c2]) ).
cnf(c549,plain,
( ssPv3(skf2(X199))
| ssPv2(X199)
| ssPv3(X199) ),
inference(resolution,[status(thm)],[c518,c73]) ).
cnf(clause36,negated_conjecture,
( ~ ssRr(X276,X278)
| ~ ssRr(X278,X279)
| ~ ssPv4(X279)
| ~ ssRr(X278,X277)
| ~ ssPv3(X277)
| ssPv4(X276)
| ssPv2(X278) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c897,plain,
( ~ ssRr(X672,X673)
| ~ ssRr(X673,X674)
| ~ ssPv4(X674)
| ~ ssPv3(X674)
| ssPv4(X672)
| ssPv2(X673) ),
inference(factor,[status(thm)],[clause36]) ).
cnf(c2881,plain,
( ~ ssRr(X899,X900)
| ~ ssPv4(skf2(X900))
| ~ ssPv3(skf2(X900))
| ssPv4(X899)
| ssPv2(X900) ),
inference(resolution,[status(thm)],[c897,clause2]) ).
cnf(c5685,plain,
( ~ ssRr(X903,X902)
| ~ ssPv4(skf2(X902))
| ssPv4(X903)
| ssPv2(X902)
| ssPv3(X902) ),
inference(resolution,[status(thm)],[c2881,c549]) ).
cnf(c5723,plain,
( ~ ssRr(X907,X906)
| ssPv4(X907)
| ssPv2(X906)
| ssPv3(X906)
| ssPv4(skf3(X906)) ),
inference(resolution,[status(thm)],[c5685,c5026]) ).
cnf(c5743,plain,
( ssPv4(skf3(X908))
| ssPv2(X908)
| ssPv3(X908) ),
inference(resolution,[status(thm)],[c5723,clause1]) ).
cnf(c5749,plain,
( ssPv2(X909)
| ssPv3(X909)
| ssPv1(skf3(X909)) ),
inference(resolution,[status(thm)],[c5743,c2545]) ).
cnf(c5881,plain,
( ssPv2(X914)
| ssPv3(X914)
| ~ ssPv4(X914)
| ssPv3(skf3(X914)) ),
inference(resolution,[status(thm)],[c5749,c305]) ).
cnf(c5901,plain,
( ssPv2(X915)
| ssPv3(X915)
| ssPv3(skf3(X915)) ),
inference(resolution,[status(thm)],[c5881,c495]) ).
cnf(clause22,negated_conjecture,
( ~ ssRr(X146,X147)
| ~ ssPv3(X146)
| ~ ssRr(X147,X148)
| ~ ssPv2(X147)
| ~ ssPv3(X147)
| ssPv2(X148) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c425,plain,
( ~ ssRr(X2300,skf3(X2301))
| ~ ssPv3(X2300)
| ~ ssPv2(skf3(X2301))
| ~ ssPv3(skf3(X2301))
| ssPv2(X2301) ),
inference(resolution,[status(thm)],[clause22,clause1]) ).
cnf(c23765,plain,
( ~ ssPv3(skf3(skf3(X2302)))
| ~ ssPv2(skf3(X2302))
| ~ ssPv3(skf3(X2302))
| ssPv2(X2302) ),
inference(resolution,[status(thm)],[c425,clause1]) ).
cnf(clause20,negated_conjecture,
( ~ ssRr(X128,X129)
| ~ ssRr(X129,X130)
| ~ ssPv4(X130)
| ~ ssPv3(X129)
| ~ ssPv4(X129)
| ssPv3(X128) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c395,plain,
( ~ ssRr(X2184,skf3(X2183))
| ~ ssPv4(X2183)
| ~ ssPv3(skf3(X2183))
| ~ ssPv4(skf3(X2183))
| ssPv3(X2184) ),
inference(resolution,[status(thm)],[clause20,clause1]) ).
cnf(c21676,plain,
( ~ ssPv4(X2185)
| ~ ssPv3(skf3(X2185))
| ~ ssPv4(skf3(X2185))
| ssPv3(skf3(skf3(X2185))) ),
inference(resolution,[status(thm)],[c395,clause1]) ).
cnf(c21689,plain,
( ~ ssPv4(X2694)
| ~ ssPv3(skf3(X2694))
| ssPv3(skf3(skf3(X2694)))
| ssPv2(X2694)
| ssPv3(X2694) ),
inference(resolution,[status(thm)],[c21676,c5743]) ).
cnf(c29315,plain,
( ~ ssPv4(X2695)
| ssPv3(skf3(skf3(X2695)))
| ssPv2(X2695)
| ssPv3(X2695) ),
inference(resolution,[status(thm)],[c21689,c5901]) ).
cnf(c29433,plain,
( ssPv3(skf3(skf3(X2696)))
| ssPv2(X2696)
| ssPv3(X2696) ),
inference(resolution,[status(thm)],[c29315,c495]) ).
cnf(c29482,plain,
( ssPv2(X2698)
| ssPv3(X2698)
| ~ ssPv2(skf3(X2698))
| ~ ssPv3(skf3(X2698)) ),
inference(resolution,[status(thm)],[c29433,c23765]) ).
cnf(c29619,plain,
( ssPv2(X2700)
| ssPv3(X2700)
| ~ ssPv2(skf3(X2700)) ),
inference(resolution,[status(thm)],[c29482,c5901]) ).
cnf(c29733,plain,
( ssPv2(X2701)
| ssPv3(X2701) ),
inference(resolution,[status(thm)],[c29619,c516]) ).
cnf(c2464,plain,
( ~ ssRr(X629,X628)
| ~ ssPv4(X629)
| ~ ssPv2(X629)
| ssPv1(X629)
| ssPv2(X628) ),
inference(factor,[status(thm)],[c850]) ).
cnf(c2468,plain,
( ~ ssPv4(skf3(X641))
| ~ ssPv2(skf3(X641))
| ssPv1(skf3(X641))
| ssPv2(X641) ),
inference(resolution,[status(thm)],[c2464,clause1]) ).
cnf(c29787,plain,
( ssPv3(skf3(X2704))
| ~ ssPv4(X2704)
| ssPv1(X2704) ),
inference(resolution,[status(thm)],[c29733,c271]) ).
cnf(c304,plain,
( ~ ssPv1(X116)
| ~ ssPv4(skf2(X116))
| ssPv3(X116)
| ssPv2(skf2(X116)) ),
inference(resolution,[status(thm)],[c301,clause2]) ).
cnf(c4229,plain,
( ssPv1(skf3(X772))
| ssPv2(skf2(X772))
| ssPv3(X772)
| ~ ssPv1(X772) ),
inference(resolution,[status(thm)],[c4213,c304]) ).
cnf(c4297,plain,
( ssPv1(skf3(X776))
| ssPv2(skf2(X776))
| ssPv3(X776)
| ssPv3(skf3(X776)) ),
inference(resolution,[status(thm)],[c4229,c1366]) ).
cnf(c506,plain,
( ssPv2(skf2(X220))
| ssPv3(skf2(X220))
| ~ ssPv1(X220)
| ssPv3(X220) ),
inference(resolution,[status(thm)],[c495,c304]) ).
cnf(c851,plain,
( ~ ssRr(X663,X665)
| ~ ssPv4(X663)
| ~ ssRr(X664,X665)
| ~ ssPv2(X664)
| ssPv1(X664)
| ssPv2(X665) ),
inference(factor,[status(thm)],[clause35]) ).
cnf(c2856,plain,
( ~ ssRr(X888,skf2(X889))
| ~ ssPv4(X888)
| ~ ssPv2(X889)
| ssPv1(X889)
| ssPv2(skf2(X889)) ),
inference(resolution,[status(thm)],[c851,clause2]) ).
cnf(c5582,plain,
( ~ ssPv4(skf3(skf2(X891)))
| ~ ssPv2(X891)
| ssPv1(X891)
| ssPv2(skf2(X891)) ),
inference(resolution,[status(thm)],[c2856,clause1]) ).
cnf(c5772,plain,
( ssPv2(skf2(X920))
| ssPv3(skf2(X920))
| ~ ssPv2(X920)
| ssPv1(X920) ),
inference(resolution,[status(thm)],[c5743,c5582]) ).
cnf(c5989,plain,
( ssPv2(skf2(X921))
| ssPv3(skf2(X921))
| ssPv1(X921) ),
inference(resolution,[status(thm)],[c5772,c518]) ).
cnf(c6057,plain,
( ssPv2(skf2(X923))
| ssPv3(skf2(X923))
| ssPv3(X923) ),
inference(resolution,[status(thm)],[c5989,c506]) ).
cnf(clause38,negated_conjecture,
( ~ ssRr(X297,X299)
| ~ ssPv1(X297)
| ~ ssRr(X299,X300)
| ~ ssPv3(X300)
| ~ ssRr(X299,X298)
| ~ ssPv1(X299)
| ssPv2(X298) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c917,plain,
( ~ ssRr(X684,X685)
| ~ ssPv1(X684)
| ~ ssRr(X685,X686)
| ~ ssPv3(X686)
| ~ ssPv1(X685)
| ssPv2(X686) ),
inference(factor,[status(thm)],[clause38]) ).
cnf(c2887,plain,
( ~ ssRr(X1039,X1040)
| ~ ssPv1(X1039)
| ~ ssPv3(skf2(X1040))
| ~ ssPv1(X1040)
| ssPv2(skf2(X1040)) ),
inference(resolution,[status(thm)],[c917,clause2]) ).
cnf(c6638,plain,
( ~ ssRr(X1056,X1055)
| ~ ssPv1(X1056)
| ~ ssPv1(X1055)
| ssPv2(skf2(X1055))
| ssPv3(X1055) ),
inference(resolution,[status(thm)],[c2887,c6057]) ).
cnf(c6689,plain,
( ~ ssPv1(skf3(X1057))
| ~ ssPv1(X1057)
| ssPv2(skf2(X1057))
| ssPv3(X1057) ),
inference(resolution,[status(thm)],[c6638,clause1]) ).
cnf(c6699,plain,
( ~ ssPv1(X1061)
| ssPv2(skf2(X1061))
| ssPv3(X1061)
| ssPv3(skf3(X1061)) ),
inference(resolution,[status(thm)],[c6689,c4297]) ).
cnf(c6718,plain,
( ssPv2(skf2(X1062))
| ssPv3(X1062)
| ssPv3(skf3(X1062)) ),
inference(resolution,[status(thm)],[c6699,c1366]) ).
cnf(clause41,negated_conjecture,
( ~ ssRr(X330,X332)
| ~ ssPv2(X330)
| ~ ssRr(X332,X333)
| ~ ssPv2(X333)
| ~ ssRr(X332,X331)
| ~ ssPv1(X331)
| ~ ssPv1(X332) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(c995,plain,
( ~ ssRr(X702,X701)
| ~ ssPv2(X702)
| ~ ssRr(X701,X703)
| ~ ssPv2(X703)
| ~ ssPv1(X703)
| ~ ssPv1(X701) ),
inference(factor,[status(thm)],[clause41]) ).
cnf(c2947,plain,
( ~ ssRr(X1139,X1140)
| ~ ssPv2(X1139)
| ~ ssPv2(skf2(X1140))
| ~ ssPv1(skf2(X1140))
| ~ ssPv1(X1140) ),
inference(resolution,[status(thm)],[c995,clause2]) ).
cnf(clause23,negated_conjecture,
( ~ ssRr(X156,X157)
| ~ ssPv4(X156)
| ~ ssRr(X157,X158)
| ~ ssPv1(X157)
| ~ ssPv4(X157)
| ssPv1(X158) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c431,plain,
( ~ ssRr(X339,X340)
| ~ ssPv4(X339)
| ~ ssPv1(X340)
| ~ ssPv4(X340)
| ssPv1(skf2(X340)) ),
inference(resolution,[status(thm)],[clause23,clause2]) ).
cnf(c1017,plain,
( ~ ssPv4(skf3(X345))
| ~ ssPv1(X345)
| ~ ssPv4(X345)
| ssPv1(skf2(X345)) ),
inference(resolution,[status(thm)],[c431,clause1]) ).
cnf(c270,plain,
( ~ ssPv4(skf2(X105))
| ~ ssPv2(X105)
| ssPv1(skf2(X105))
| ssPv3(X105) ),
inference(resolution,[status(thm)],[c238,clause2]) ).
cnf(c6746,plain,
( ssPv3(X1066)
| ssPv3(skf3(X1066))
| ~ ssPv1(X1066)
| ssPv4(skf2(X1066)) ),
inference(resolution,[status(thm)],[c6718,c292]) ).
cnf(c6782,plain,
( ssPv3(X1067)
| ssPv3(skf3(X1067))
| ssPv4(skf2(X1067)) ),
inference(resolution,[status(thm)],[c6746,c1366]) ).
cnf(c6826,plain,
( ssPv3(X1071)
| ssPv3(skf3(X1071))
| ~ ssPv2(X1071)
| ssPv1(skf2(X1071)) ),
inference(resolution,[status(thm)],[c6782,c270]) ).
cnf(c6924,plain,
( ssPv3(X1072)
| ssPv3(skf3(X1072))
| ssPv1(skf2(X1072)) ),
inference(resolution,[status(thm)],[c6826,c5901]) ).
cnf(c6985,plain,
( ssPv3(X1078)
| ssPv1(skf2(X1078))
| ~ ssPv4(X1078)
| ssPv4(skf3(X1078)) ),
inference(resolution,[status(thm)],[c6924,c218]) ).
cnf(clause14,negated_conjecture,
( ~ ssRr(X73,X74)
| ~ ssPv2(X74)
| ~ ssRr(X73,X75)
| ~ ssPv1(X73)
| ssPv4(X75)
| ssPv4(X73) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c188,plain,
( ~ ssRr(X76,X77)
| ~ ssPv2(X77)
| ~ ssPv1(X76)
| ssPv4(X77)
| ssPv4(X76) ),
inference(factor,[status(thm)],[clause14]) ).
cnf(c192,plain,
( ~ ssPv2(X79)
| ~ ssPv1(skf3(X79))
| ssPv4(X79)
| ssPv4(skf3(X79)) ),
inference(resolution,[status(thm)],[c188,clause1]) ).
cnf(clause7,negated_conjecture,
( ~ ssRr(X16,X17)
| ~ ssPv2(X17)
| ~ ssPv3(X17)
| ssPv1(X16)
| ssPv1(X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(c14,plain,
( ~ ssPv2(skf2(X49))
| ~ ssPv3(skf2(X49))
| ssPv1(X49)
| ssPv1(skf2(X49)) ),
inference(resolution,[status(thm)],[clause7,clause2]) ).
cnf(c24,plain,
( ssPv4(skf2(X25))
| ssPv3(skf2(X25))
| ssPv3(X25)
| ssPv4(X25) ),
inference(resolution,[status(thm)],[c16,clause2]) ).
cnf(c401,plain,
( ~ ssPv2(skf2(X143))
| ~ ssPv2(X143)
| ~ ssPv4(X143)
| ssPv4(skf2(X143)) ),
inference(resolution,[status(thm)],[c398,clause2]) ).
cnf(c501,plain,
( ssPv4(skf2(X216))
| ssPv3(skf2(X216))
| ~ ssPv2(X216)
| ~ ssPv4(X216) ),
inference(resolution,[status(thm)],[c495,c401]) ).
cnf(c648,plain,
( ssPv4(skf2(X254))
| ssPv3(skf2(X254))
| ~ ssPv2(X254)
| ssPv3(X254) ),
inference(resolution,[status(thm)],[c501,c24]) ).
cnf(c806,plain,
( ssPv4(skf2(X255))
| ssPv3(skf2(X255))
| ssPv3(X255) ),
inference(resolution,[status(thm)],[c648,c549]) ).
cnf(c821,plain,
( ssPv3(skf2(X272))
| ssPv3(X272)
| ~ ssPv2(X272)
| ssPv1(skf2(X272)) ),
inference(resolution,[status(thm)],[c806,c270]) ).
cnf(c862,plain,
( ssPv3(skf2(X273))
| ssPv3(X273)
| ssPv1(skf2(X273)) ),
inference(resolution,[status(thm)],[c821,c549]) ).
cnf(c872,plain,
( ssPv3(X275)
| ssPv1(skf2(X275))
| ~ ssPv2(skf2(X275))
| ssPv1(X275) ),
inference(resolution,[status(thm)],[c862,c14]) ).
cnf(c4227,plain,
( ssPv1(skf3(X1874))
| ssPv2(skf2(X1874))
| ssPv3(X1874)
| ~ ssPv2(X1874)
| ssPv1(skf2(X1874)) ),
inference(resolution,[status(thm)],[c4213,c270]) ).
cnf(c17717,plain,
( ssPv1(skf3(X1875))
| ssPv2(skf2(X1875))
| ssPv3(X1875)
| ssPv1(skf2(X1875)) ),
inference(resolution,[status(thm)],[c4227,c5749]) ).
cnf(c17779,plain,
( ssPv1(skf3(X1878))
| ssPv3(X1878)
| ssPv1(skf2(X1878))
| ssPv1(X1878) ),
inference(resolution,[status(thm)],[c17717,c872]) ).
cnf(c17978,plain,
( ssPv1(skf3(X1886))
| ssPv3(X1886)
| ssPv1(skf2(X1886))
| ssPv4(skf2(X1886)) ),
inference(resolution,[status(thm)],[c17779,c4269]) ).
cnf(c18205,plain,
( ssPv1(skf3(X1887))
| ssPv3(X1887)
| ssPv1(skf2(X1887))
| ~ ssPv2(X1887) ),
inference(resolution,[status(thm)],[c17978,c270]) ).
cnf(c18333,plain,
( ssPv1(skf3(X1888))
| ssPv3(X1888)
| ssPv1(skf2(X1888)) ),
inference(resolution,[status(thm)],[c18205,c5749]) ).
cnf(c18362,plain,
( ssPv3(X1909)
| ssPv1(skf2(X1909))
| ~ ssPv2(X1909)
| ssPv4(X1909)
| ssPv4(skf3(X1909)) ),
inference(resolution,[status(thm)],[c18333,c192]) ).
cnf(c18556,plain,
( ssPv3(X1910)
| ssPv1(skf2(X1910))
| ssPv4(X1910)
| ssPv4(skf3(X1910)) ),
inference(resolution,[status(thm)],[c18362,c495]) ).
cnf(c18626,plain,
( ssPv3(X1911)
| ssPv1(skf2(X1911))
| ssPv4(skf3(X1911)) ),
inference(resolution,[status(thm)],[c18556,c6985]) ).
cnf(c18829,plain,
( ssPv3(X1912)
| ssPv1(skf2(X1912))
| ~ ssPv1(X1912)
| ~ ssPv4(X1912) ),
inference(resolution,[status(thm)],[c18626,c1017]) ).
cnf(c18705,plain,
( ssPv3(X1928)
| ssPv1(skf2(X1928))
| ssPv4(X1928)
| ~ ssPv2(X1928)
| ~ ssPv2(skf3(X1928)) ),
inference(resolution,[status(thm)],[c18556,c402]) ).
cnf(clause34,negated_conjecture,
( ~ ssRr(X258,X260)
| ~ ssPv2(X258)
| ~ ssRr(X260,X261)
| ~ ssRr(X260,X259)
| ~ ssPv4(X260)
| ssPv4(X261)
| ssPv3(X259) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c841,plain,
( ~ ssRr(X621,X620)
| ~ ssPv2(X621)
| ~ ssRr(X620,X622)
| ~ ssPv4(X620)
| ssPv4(X622)
| ssPv3(X622) ),
inference(factor,[status(thm)],[clause34]) ).
cnf(c2463,plain,
( ~ ssRr(X879,skf3(X880))
| ~ ssPv2(X879)
| ~ ssPv4(skf3(X880))
| ssPv4(X880)
| ssPv3(X880) ),
inference(resolution,[status(thm)],[c841,clause1]) ).
cnf(c5537,plain,
( ~ ssPv2(skf3(skf3(X881)))
| ~ ssPv4(skf3(X881))
| ssPv4(X881)
| ssPv3(X881) ),
inference(resolution,[status(thm)],[c2463,clause1]) ).
cnf(clause5,negated_conjecture,
( ~ ssRr(X9,X10)
| ~ ssPv1(X10)
| ~ ssPv4(X10)
| ssPv2(X9)
| ssPv2(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c5,plain,
( ~ ssPv1(X12)
| ~ ssPv4(X12)
| ssPv2(skf3(X12))
| ssPv2(X12) ),
inference(resolution,[status(thm)],[clause5,clause1]) ).
cnf(c6,plain,
( ssPv2(skf3(X22))
| ssPv2(X22)
| ssPv3(X22)
| ssPv4(skf3(X22)) ),
inference(resolution,[status(thm)],[c3,c1]) ).
cnf(c94,plain,
( ssPv3(skf3(X71))
| ssPv2(skf3(X71))
| ssPv3(X71)
| ssPv4(skf3(X71)) ),
inference(resolution,[status(thm)],[c74,c6]) ).
cnf(c235,plain,
( ~ ssPv4(X97)
| ssPv4(skf3(X97))
| ssPv3(X97)
| ssPv2(skf3(X97)) ),
inference(resolution,[status(thm)],[c218,c94]) ).
cnf(clause9,negated_conjecture,
( ~ ssRr(X27,X28)
| ~ ssRr(X28,X29)
| ~ ssPv3(X28)
| ssPv2(X27)
| ssPv4(X29)
| ssPv4(X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c44,plain,
( ~ ssRr(X522,skf3(X521))
| ~ ssPv3(skf3(X521))
| ssPv2(X522)
| ssPv4(X521)
| ssPv4(skf3(X521)) ),
inference(resolution,[status(thm)],[clause9,clause1]) ).
cnf(c1968,plain,
( ~ ssPv3(skf3(X743))
| ssPv2(skf3(skf3(X743)))
| ssPv4(X743)
| ssPv4(skf3(X743)) ),
inference(resolution,[status(thm)],[c44,clause1]) ).
cnf(c3548,plain,
( ssPv2(skf3(skf3(X744)))
| ssPv4(X744)
| ssPv4(skf3(X744))
| ssPv3(X744) ),
inference(resolution,[status(thm)],[c1968,c1341]) ).
cnf(c3607,plain,
( ssPv2(skf3(skf3(X1158)))
| ssPv4(skf3(X1158))
| ssPv3(X1158)
| ssPv2(skf3(X1158)) ),
inference(resolution,[status(thm)],[c3548,c235]) ).
cnf(c7669,plain,
( ssPv2(skf3(skf3(X1287)))
| ssPv3(X1287)
| ssPv2(skf3(X1287))
| ~ ssPv1(skf3(X1287)) ),
inference(resolution,[status(thm)],[c3607,c5]) ).
cnf(c18371,plain,
( ssPv3(X1944)
| ssPv1(skf2(X1944))
| ssPv2(skf3(skf3(X1944)))
| ssPv2(skf3(X1944)) ),
inference(resolution,[status(thm)],[c18333,c7669]) ).
cnf(c19428,plain,
( ssPv3(X2532)
| ssPv1(skf2(X2532))
| ssPv2(skf3(X2532))
| ~ ssPv4(skf3(X2532))
| ssPv4(X2532) ),
inference(resolution,[status(thm)],[c18371,c5537]) ).
cnf(c27284,plain,
( ssPv3(X2533)
| ssPv1(skf2(X2533))
| ssPv2(skf3(X2533))
| ssPv4(X2533) ),
inference(resolution,[status(thm)],[c19428,c18626]) ).
cnf(c27397,plain,
( ssPv3(X2537)
| ssPv1(skf2(X2537))
| ssPv4(X2537)
| ~ ssPv2(X2537) ),
inference(resolution,[status(thm)],[c27284,c18705]) ).
cnf(c27701,plain,
( ssPv3(X2538)
| ssPv1(skf2(X2538))
| ssPv4(X2538) ),
inference(resolution,[status(thm)],[c27397,c495]) ).
cnf(c27826,plain,
( ssPv3(X2539)
| ssPv1(skf2(X2539))
| ~ ssPv1(X2539) ),
inference(resolution,[status(thm)],[c27701,c18829]) ).
cnf(c2467,plain,
( ~ ssPv4(X630)
| ~ ssPv2(X630)
| ssPv1(X630)
| ssPv2(skf2(X630)) ),
inference(resolution,[status(thm)],[c2464,clause2]) ).
cnf(c29818,plain,
( ssPv3(X2716)
| ~ ssPv4(X2716)
| ssPv1(X2716)
| ssPv2(skf2(X2716)) ),
inference(resolution,[status(thm)],[c29733,c2467]) ).
cnf(c30137,plain,
( ssPv3(X2771)
| ssPv1(X2771)
| ssPv2(skf2(X2771))
| ssPv1(skf2(X2771)) ),
inference(resolution,[status(thm)],[c29818,c27701]) ).
cnf(c30778,plain,
( ssPv3(X2772)
| ssPv1(X2772)
| ssPv1(skf2(X2772)) ),
inference(resolution,[status(thm)],[c30137,c872]) ).
cnf(c30890,plain,
( ssPv3(X2774)
| ssPv1(skf2(X2774)) ),
inference(resolution,[status(thm)],[c30778,c27826]) ).
cnf(c30962,plain,
( ssPv3(X2914)
| ~ ssRr(X2913,X2914)
| ~ ssPv2(X2913)
| ~ ssPv2(skf2(X2914))
| ~ ssPv1(X2914) ),
inference(resolution,[status(thm)],[c30890,c2947]) ).
cnf(c32245,plain,
( ssPv3(X2945)
| ~ ssRr(X2944,X2945)
| ~ ssPv2(X2944)
| ~ ssPv1(X2945)
| ssPv3(skf3(X2945)) ),
inference(resolution,[status(thm)],[c30962,c6718]) ).
cnf(c33045,plain,
( ssPv3(X2946)
| ~ ssPv2(skf3(X2946))
| ~ ssPv1(X2946)
| ssPv3(skf3(X2946)) ),
inference(resolution,[status(thm)],[c32245,clause1]) ).
cnf(c33103,plain,
( ssPv3(X2947)
| ~ ssPv1(X2947)
| ssPv3(skf3(X2947)) ),
inference(resolution,[status(thm)],[c33045,c29733]) ).
cnf(c33112,plain,
( ssPv3(X2949)
| ssPv3(skf3(X2949)) ),
inference(resolution,[status(thm)],[c33103,c1366]) ).
cnf(clause24,negated_conjecture,
( ~ ssRr(X165,X166)
| ~ ssPv3(X166)
| ~ ssRr(X165,X167)
| ~ ssPv2(X167)
| ~ ssPv3(X165)
| ssPv4(X165) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c435,plain,
( ~ ssRr(X169,X168)
| ~ ssPv3(X168)
| ~ ssPv2(X168)
| ~ ssPv3(X169)
| ssPv4(X169) ),
inference(factor,[status(thm)],[clause24]) ).
cnf(c438,plain,
( ~ ssPv3(skf2(X170))
| ~ ssPv2(skf2(X170))
| ~ ssPv3(X170)
| ssPv4(X170) ),
inference(resolution,[status(thm)],[c435,clause2]) ).
cnf(clause26,negated_conjecture,
( ~ ssRr(X185,X186)
| ~ ssPv2(X185)
| ~ ssRr(X186,X187)
| ~ ssPv3(X187)
| ~ ssPv3(X186)
| ssPv1(X186) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c483,plain,
( ~ ssRr(X364,X365)
| ~ ssPv2(X364)
| ~ ssPv3(skf2(X365))
| ~ ssPv3(X365)
| ssPv1(X365) ),
inference(resolution,[status(thm)],[clause26,clause2]) ).
cnf(c6037,plain,
( ssPv2(skf2(X965))
| ssPv1(X965)
| ~ ssRr(X964,X965)
| ~ ssPv2(X964)
| ~ ssPv3(X965) ),
inference(resolution,[status(thm)],[c5989,c483]) ).
cnf(c6346,plain,
( ssPv2(skf2(X966))
| ssPv1(X966)
| ~ ssPv2(skf3(X966))
| ~ ssPv3(X966) ),
inference(resolution,[status(thm)],[c6037,clause1]) ).
cnf(c85,plain,
( ssPv3(X43)
| ssPv2(X43)
| ssPv3(skf2(X43))
| ssPv2(skf3(X43)) ),
inference(resolution,[status(thm)],[c76,c3]) ).
cnf(c217,plain,
( ~ ssPv3(X89)
| ~ ssPv4(skf2(X89))
| ssPv4(X89)
| ssPv3(skf2(X89)) ),
inference(resolution,[status(thm)],[c202,clause2]) ).
cnf(c43,plain,
( ~ ssRr(X61,X60)
| ~ ssPv3(X60)
| ssPv2(X61)
| ssPv4(skf2(X60))
| ssPv4(X60) ),
inference(resolution,[status(thm)],[clause9,clause2]) ).
cnf(c150,plain,
( ~ ssPv3(X62)
| ssPv2(skf3(X62))
| ssPv4(skf2(X62))
| ssPv4(X62) ),
inference(resolution,[status(thm)],[c43,clause1]) ).
cnf(c158,plain,
( ssPv2(skf3(X125))
| ssPv4(skf2(X125))
| ssPv4(X125)
| ssPv3(skf2(X125)) ),
inference(resolution,[status(thm)],[c150,c24]) ).
cnf(c327,plain,
( ssPv2(skf3(X126))
| ssPv4(X126)
| ssPv3(skf2(X126))
| ~ ssPv3(X126) ),
inference(resolution,[status(thm)],[c158,c217]) ).
cnf(c353,plain,
( ssPv2(skf3(X127))
| ssPv4(X127)
| ssPv3(skf2(X127))
| ssPv2(X127) ),
inference(resolution,[status(thm)],[c327,c85]) ).
cnf(c471,plain,
( ~ ssRr(X350,X351)
| ~ ssPv4(X350)
| ssPv2(X351)
| ssPv4(X351)
| ssPv2(skf3(X351)) ),
inference(resolution,[status(thm)],[c317,c353]) ).
cnf(c1058,plain,
( ~ ssPv4(skf3(X352))
| ssPv2(X352)
| ssPv4(X352)
| ssPv2(skf3(X352)) ),
inference(resolution,[status(thm)],[c471,clause1]) ).
cnf(c1066,plain,
( ssPv2(X354)
| ssPv4(X354)
| ssPv2(skf3(X354))
| ssPv3(skf3(X354)) ),
inference(resolution,[status(thm)],[c1058,c495]) ).
cnf(c293,plain,
( ~ ssPv2(X113)
| ~ ssPv1(skf3(X113))
| ssPv4(X113)
| ssPv3(skf3(X113)) ),
inference(resolution,[status(thm)],[c272,clause1]) ).
cnf(c15,plain,
( ~ ssPv2(X21)
| ~ ssPv3(X21)
| ssPv1(skf3(X21))
| ssPv1(X21) ),
inference(resolution,[status(thm)],[clause7,clause1]) ).
cnf(c1398,plain,
( ssPv3(skf3(X433))
| ssPv1(X433)
| ~ ssPv2(X433)
| ssPv1(skf3(X433)) ),
inference(resolution,[status(thm)],[c1366,c15]) ).
cnf(c1428,plain,
( ssPv3(skf3(X1588))
| ssPv1(X1588)
| ssPv1(skf3(X1588))
| ssPv4(X1588)
| ssPv2(skf3(X1588)) ),
inference(resolution,[status(thm)],[c1398,c1066]) ).
cnf(c13807,plain,
( ssPv3(skf3(X1589))
| ssPv1(X1589)
| ssPv4(X1589)
| ssPv2(skf3(X1589))
| ~ ssPv2(X1589) ),
inference(resolution,[status(thm)],[c1428,c293]) ).
cnf(c13979,plain,
( ssPv3(skf3(X1590))
| ssPv1(X1590)
| ssPv4(X1590)
| ssPv2(skf3(X1590)) ),
inference(resolution,[status(thm)],[c13807,c1066]) ).
cnf(c14112,plain,
( ssPv3(skf3(X1601))
| ssPv1(X1601)
| ssPv4(X1601)
| ssPv2(skf2(X1601))
| ~ ssPv3(X1601) ),
inference(resolution,[status(thm)],[c13979,c6346]) ).
cnf(c14134,plain,
( ssPv3(skf3(X1602))
| ssPv1(X1602)
| ssPv4(X1602)
| ssPv2(skf2(X1602)) ),
inference(resolution,[status(thm)],[c14112,c1366]) ).
cnf(c14361,plain,
( ssPv3(skf3(X1649))
| ssPv1(X1649)
| ssPv4(X1649)
| ~ ssPv3(skf2(X1649))
| ~ ssPv3(X1649) ),
inference(resolution,[status(thm)],[c14134,c438]) ).
cnf(c203,plain,
( ~ ssRr(X1327,skf2(X1326))
| ~ ssPv3(X1327)
| ~ ssPv4(skf2(X1326))
| ssPv4(X1326)
| ssPv3(skf2(X1326)) ),
inference(resolution,[status(thm)],[clause15,clause2]) ).
cnf(c10919,plain,
( ~ ssPv3(skf3(skf2(X1355)))
| ~ ssPv4(skf2(X1355))
| ssPv4(X1355)
| ssPv3(skf2(X1355)) ),
inference(resolution,[status(thm)],[c203,clause1]) ).
cnf(c33175,plain,
( ssPv3(skf2(X2952))
| ~ ssPv4(skf2(X2952))
| ssPv4(X2952) ),
inference(resolution,[status(thm)],[c33112,c10919]) ).
cnf(c33291,plain,
( ssPv3(skf2(X2953))
| ssPv4(X2953)
| ssPv3(X2953) ),
inference(resolution,[status(thm)],[c33175,c806]) ).
cnf(clause32,negated_conjecture,
( ~ ssRr(X240,X242)
| ~ ssPv3(X240)
| ~ ssRr(X243,X242)
| ~ ssRr(X242,X241)
| ~ ssPv3(X241)
| ssPv4(X243)
| ssPv3(X242) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c718,plain,
( ~ ssRr(X3354,X3355)
| ~ ssPv3(X3354)
| ~ ssRr(X3353,X3355)
| ~ ssPv3(skf2(X3355))
| ssPv4(X3353)
| ssPv3(X3355) ),
inference(resolution,[status(thm)],[clause32,clause2]) ).
cnf(c40610,plain,
( ~ ssRr(X3687,X3685)
| ~ ssPv3(X3687)
| ~ ssRr(X3686,X3685)
| ssPv4(X3686)
| ssPv3(X3685)
| ssPv4(X3685) ),
inference(resolution,[status(thm)],[c718,c33291]) ).
cnf(c48061,plain,
( ~ ssRr(X3689,X3688)
| ~ ssPv3(X3689)
| ssPv4(X3689)
| ssPv3(X3688)
| ssPv4(X3688) ),
inference(factor,[status(thm)],[c40610]) ).
cnf(c48064,plain,
( ~ ssPv3(X3690)
| ssPv4(X3690)
| ssPv3(skf2(X3690))
| ssPv4(skf2(X3690)) ),
inference(resolution,[status(thm)],[c48061,clause2]) ).
cnf(c48074,plain,
( ssPv4(X3691)
| ssPv3(skf2(X3691))
| ssPv4(skf2(X3691)) ),
inference(resolution,[status(thm)],[c48064,c806]) ).
cnf(c48296,plain,
( ssPv4(X3692)
| ssPv3(skf2(X3692)) ),
inference(resolution,[status(thm)],[c48074,c33175]) ).
cnf(c48402,plain,
( ssPv4(X3720)
| ssPv3(skf3(X3720))
| ssPv1(X3720)
| ~ ssPv3(X3720) ),
inference(resolution,[status(thm)],[c48296,c14361]) ).
cnf(c49234,plain,
( ssPv4(X3721)
| ssPv3(skf3(X3721))
| ssPv1(X3721) ),
inference(resolution,[status(thm)],[c48402,c33112]) ).
cnf(c49264,plain,
( ssPv3(skf3(X3722))
| ssPv1(X3722) ),
inference(resolution,[status(thm)],[c49234,c29787]) ).
cnf(clause25,negated_conjecture,
( ~ ssRr(X175,X176)
| ~ ssPv4(X175)
| ~ ssRr(X176,X177)
| ~ ssPv3(X177)
| ~ ssPv3(X176)
| ssPv1(X176) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(c462,plain,
( ~ ssRr(X349,X348)
| ~ ssPv4(X349)
| ~ ssPv3(skf2(X348))
| ~ ssPv3(X348)
| ssPv1(X348) ),
inference(resolution,[status(thm)],[clause25,clause2]) ).
cnf(c48408,plain,
( ssPv4(X3798)
| ~ ssRr(X3799,X3798)
| ~ ssPv4(X3799)
| ~ ssPv3(X3798)
| ssPv1(X3798) ),
inference(resolution,[status(thm)],[c48296,c462]) ).
cnf(c50836,plain,
( ssPv4(X3800)
| ~ ssPv4(skf3(X3800))
| ~ ssPv3(X3800)
| ssPv1(X3800) ),
inference(resolution,[status(thm)],[c48408,clause1]) ).
cnf(c437,plain,
( ~ ssRr(skf3(X2315),X2314)
| ~ ssPv3(X2314)
| ~ ssPv2(X2315)
| ~ ssPv3(skf3(X2315))
| ssPv4(skf3(X2315)) ),
inference(resolution,[status(thm)],[clause24,clause1]) ).
cnf(c23894,plain,
( ~ ssPv3(skf2(skf3(X2317)))
| ~ ssPv2(X2317)
| ~ ssPv3(skf3(X2317))
| ssPv4(skf3(X2317)) ),
inference(resolution,[status(thm)],[c437,clause2]) ).
cnf(c48399,plain,
( ssPv4(skf3(X3701))
| ~ ssPv2(X3701)
| ~ ssPv3(skf3(X3701)) ),
inference(resolution,[status(thm)],[c48296,c23894]) ).
cnf(c49387,plain,
( ssPv1(X3723)
| ssPv4(skf3(X3723))
| ~ ssPv2(X3723) ),
inference(resolution,[status(thm)],[c49264,c48399]) ).
cnf(c526,plain,
( ssPv2(X234)
| ssPv4(X234)
| ssPv2(skf3(X234))
| ssPv4(skf2(X234)) ),
inference(resolution,[status(thm)],[c495,c150]) ).
cnf(c48404,plain,
( ssPv4(X3793)
| ~ ssRr(X3792,X3793)
| ~ ssPv2(X3792)
| ~ ssPv3(X3793)
| ssPv1(X3793) ),
inference(resolution,[status(thm)],[c48296,c483]) ).
cnf(c50788,plain,
( ssPv4(X3794)
| ~ ssPv2(skf3(X3794))
| ~ ssPv3(X3794)
| ssPv1(X3794) ),
inference(resolution,[status(thm)],[c48404,clause1]) ).
cnf(c50812,plain,
( ssPv4(X3918)
| ~ ssPv3(X3918)
| ssPv1(X3918)
| ssPv2(X3918)
| ssPv4(skf2(X3918)) ),
inference(resolution,[status(thm)],[c50788,c526]) ).
cnf(c53162,plain,
( ssPv4(X3919)
| ssPv1(X3919)
| ssPv2(X3919)
| ssPv4(skf2(X3919)) ),
inference(resolution,[status(thm)],[c50812,c29733]) ).
cnf(c48401,plain,
( ssPv4(X4043)
| ~ ssRr(X4042,X4043)
| ~ ssPv4(skf2(X4043))
| ssPv4(X4042)
| ssPv2(X4043) ),
inference(resolution,[status(thm)],[c48296,c2881]) ).
cnf(c56050,plain,
( ssPv4(X4045)
| ~ ssRr(X4044,X4045)
| ssPv4(X4044)
| ssPv2(X4045)
| ssPv1(X4045) ),
inference(resolution,[status(thm)],[c48401,c53162]) ).
cnf(c56099,plain,
( ssPv4(X4046)
| ssPv4(skf3(X4046))
| ssPv2(X4046)
| ssPv1(X4046) ),
inference(resolution,[status(thm)],[c56050,clause1]) ).
cnf(c56216,plain,
( ssPv4(X4049)
| ssPv4(skf3(X4049))
| ssPv1(X4049) ),
inference(resolution,[status(thm)],[c56099,c49387]) ).
cnf(c56491,plain,
( ssPv4(X4050)
| ssPv1(X4050)
| ~ ssPv3(X4050) ),
inference(resolution,[status(thm)],[c56216,c50836]) ).
cnf(c56587,plain,
( ssPv4(skf3(X4087))
| ssPv1(skf3(X4087))
| ssPv1(X4087) ),
inference(resolution,[status(thm)],[c56491,c49264]) ).
cnf(c57788,plain,
( ssPv1(skf3(X4111))
| ssPv1(X4111)
| ~ ssPv3(skf3(X4111)) ),
inference(resolution,[status(thm)],[c56587,c11]) ).
cnf(c58401,plain,
( ssPv1(skf3(X4112))
| ssPv1(X4112) ),
inference(resolution,[status(thm)],[c57788,c49264]) ).
cnf(c48414,plain,
( ssPv4(X3705)
| ~ ssRr(X3704,X3705)
| ~ ssPv4(X3704)
| ssPv2(X3705) ),
inference(resolution,[status(thm)],[c48296,c317]) ).
cnf(c48918,plain,
( ssPv4(X3707)
| ~ ssPv4(skf3(X3707))
| ssPv2(X3707) ),
inference(resolution,[status(thm)],[c48414,clause1]) ).
cnf(c56168,plain,
( ssPv4(X4047)
| ssPv2(X4047)
| ssPv1(X4047) ),
inference(resolution,[status(thm)],[c56099,c48918]) ).
cnf(c56309,plain,
( ssPv2(skf3(X4267))
| ssPv1(skf3(X4267))
| ssPv4(X4267)
| ssPv2(X4267) ),
inference(resolution,[status(thm)],[c56168,c48918]) ).
cnf(c60669,plain,
( ssPv2(skf3(X4351))
| ssPv1(skf3(X4351))
| ssPv2(X4351)
| ~ ssPv1(X4351) ),
inference(resolution,[status(thm)],[c56309,c5]) ).
cnf(c61417,plain,
( ssPv2(skf3(X4353))
| ssPv1(skf3(X4353))
| ssPv2(X4353) ),
inference(resolution,[status(thm)],[c60669,c58401]) ).
cnf(c61463,plain,
( ssPv1(skf3(X4354))
| ssPv2(X4354)
| ~ ssPv4(skf3(X4354)) ),
inference(resolution,[status(thm)],[c61417,c2468]) ).
cnf(c400,plain,
( ~ ssRr(skf3(X2190),X2191)
| ~ ssPv2(X2191)
| ~ ssPv2(skf3(X2190))
| ~ ssPv4(skf3(X2190))
| ssPv4(X2190) ),
inference(resolution,[status(thm)],[clause21,clause1]) ).
cnf(c21826,plain,
( ~ ssPv2(skf2(skf3(X2193)))
| ~ ssPv2(skf3(X2193))
| ~ ssPv4(skf3(X2193))
| ssPv4(X2193) ),
inference(resolution,[status(thm)],[c400,clause2]) ).
cnf(clause30,negated_conjecture,
( ~ ssRr(X221,X223)
| ~ ssPv3(X223)
| ~ ssRr(X221,X224)
| ~ ssRr(X221,X222)
| ~ ssPv4(X221)
| ssPv3(X224)
| ssPv1(X222) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c662,plain,
( ~ ssRr(X594,X595)
| ~ ssPv3(X595)
| ~ ssRr(X594,X596)
| ~ ssPv4(X594)
| ssPv3(X596)
| ssPv1(X596) ),
inference(factor,[status(thm)],[clause30]) ).
cnf(c2454,plain,
( ~ ssRr(skf3(X854),X853)
| ~ ssPv3(X853)
| ~ ssPv4(skf3(X854))
| ssPv3(X854)
| ssPv1(X854) ),
inference(resolution,[status(thm)],[c662,clause1]) ).
cnf(c5283,plain,
( ~ ssPv3(skf2(skf3(X857)))
| ~ ssPv4(skf3(X857))
| ssPv3(X857)
| ssPv1(X857) ),
inference(resolution,[status(thm)],[c2454,clause2]) ).
cnf(c29837,plain,
( ssPv2(skf2(skf3(X2861)))
| ~ ssPv4(skf3(X2861))
| ssPv3(X2861)
| ssPv1(X2861) ),
inference(resolution,[status(thm)],[c29733,c5283]) ).
cnf(c226,plain,
( ~ ssPv3(X96)
| ssPv4(X96)
| ssPv3(skf2(X96))
| ssPv2(skf2(X96)) ),
inference(resolution,[status(thm)],[c217,c0]) ).
cnf(c6107,plain,
( ssPv2(skf2(X924))
| ssPv3(skf2(X924))
| ssPv4(X924) ),
inference(resolution,[status(thm)],[c6057,c226]) ).
cnf(c23926,plain,
( ~ ssPv2(X2320)
| ~ ssPv3(skf3(X2320))
| ssPv4(skf3(X2320))
| ssPv2(skf2(skf3(X2320))) ),
inference(resolution,[status(thm)],[c23894,c6107]) ).
cnf(c33178,plain,
( ssPv3(X3041)
| ~ ssPv2(X3041)
| ssPv4(skf3(X3041))
| ssPv2(skf2(skf3(X3041))) ),
inference(resolution,[status(thm)],[c33112,c23926]) ).
cnf(c35122,plain,
( ssPv3(X3042)
| ssPv4(skf3(X3042))
| ssPv2(skf2(skf3(X3042))) ),
inference(resolution,[status(thm)],[c33178,c29733]) ).
cnf(c35157,plain,
( ssPv3(X3043)
| ssPv2(skf2(skf3(X3043)))
| ssPv1(X3043) ),
inference(resolution,[status(thm)],[c35122,c29837]) ).
cnf(c56558,plain,
( ssPv4(X4082)
| ssPv1(X4082)
| ssPv2(skf2(skf3(X4082))) ),
inference(resolution,[status(thm)],[c56491,c35157]) ).
cnf(c57652,plain,
( ssPv4(X4325)
| ssPv1(X4325)
| ~ ssPv2(skf3(X4325))
| ~ ssPv4(skf3(X4325)) ),
inference(resolution,[status(thm)],[c56558,c21826]) ).
cnf(c60943,plain,
( ssPv4(X4326)
| ssPv1(X4326)
| ~ ssPv2(skf3(X4326)) ),
inference(resolution,[status(thm)],[c57652,c56216]) ).
cnf(c48723,plain,
( ssPv4(skf3(X3702))
| ~ ssPv2(X3702)
| ssPv3(X3702) ),
inference(resolution,[status(thm)],[c48399,c33112]) ).
cnf(c48824,plain,
( ssPv4(skf3(X3703))
| ssPv3(X3703) ),
inference(resolution,[status(thm)],[c48723,c29733]) ).
cnf(c48843,plain,
( ssPv3(X3807)
| ~ ssPv3(skf3(X3807))
| ssPv1(X3807)
| ssPv1(skf3(X3807)) ),
inference(resolution,[status(thm)],[c48824,c11]) ).
cnf(c50877,plain,
( ssPv3(X3808)
| ssPv1(X3808)
| ssPv1(skf3(X3808)) ),
inference(resolution,[status(thm)],[c48843,c33112]) ).
cnf(c51005,plain,
( ssPv3(X4815)
| ssPv1(X4815)
| ssPv2(skf3(skf3(X4815)))
| ssPv2(skf3(X4815)) ),
inference(resolution,[status(thm)],[c50877,c7669]) ).
cnf(c69617,plain,
( ssPv3(X4820)
| ssPv1(X4820)
| ssPv2(skf3(skf3(X4820)))
| ssPv4(X4820) ),
inference(resolution,[status(thm)],[c51005,c60943]) ).
cnf(c69803,plain,
( ssPv3(X4822)
| ssPv1(X4822)
| ssPv4(X4822)
| ~ ssPv4(skf3(X4822)) ),
inference(resolution,[status(thm)],[c69617,c5537]) ).
cnf(c70016,plain,
( ssPv3(X4823)
| ssPv1(X4823)
| ssPv4(X4823) ),
inference(resolution,[status(thm)],[c69803,c56216]) ).
cnf(c70049,plain,
( ssPv1(X4824)
| ssPv4(X4824) ),
inference(resolution,[status(thm)],[c70016,c56491]) ).
cnf(c70228,plain,
( ssPv1(skf3(X4827))
| ssPv2(X4827) ),
inference(resolution,[status(thm)],[c70049,c61463]) ).
cnf(c2888,plain,
( ~ ssRr(X1116,skf3(X1117))
| ~ ssPv1(X1116)
| ~ ssPv3(X1117)
| ~ ssPv1(skf3(X1117))
| ssPv2(X1117) ),
inference(resolution,[status(thm)],[c917,clause1]) ).
cnf(c7194,plain,
( ~ ssPv1(skf3(skf3(X1118)))
| ~ ssPv3(X1118)
| ~ ssPv1(skf3(X1118))
| ssPv2(X1118) ),
inference(resolution,[status(thm)],[c2888,clause1]) ).
cnf(c2426,plain,
( ~ ssRr(X835,skf3(X834))
| ssPv1(X835)
| ssPv4(X834)
| ssPv2(X834)
| ssPv3(skf3(X834)) ),
inference(resolution,[status(thm)],[c546,clause1]) ).
cnf(c5147,plain,
( ssPv1(skf3(skf3(X836)))
| ssPv4(X836)
| ssPv2(X836)
| ssPv3(skf3(X836)) ),
inference(resolution,[status(thm)],[c2426,clause1]) ).
cnf(c50964,plain,
( ssPv3(skf3(X4804))
| ssPv1(skf3(skf3(X4804)))
| ~ ssPv2(X4804)
| ssPv4(X4804) ),
inference(resolution,[status(thm)],[c50877,c293]) ).
cnf(c69032,plain,
( ssPv3(skf3(X4807))
| ssPv1(skf3(skf3(X4807)))
| ssPv4(X4807) ),
inference(resolution,[status(thm)],[c50964,c5147]) ).
cnf(c50972,plain,
( ssPv3(skf3(X4808))
| ssPv1(skf3(skf3(X4808)))
| ~ ssPv4(X4808)
| ssPv2(X4808) ),
inference(resolution,[status(thm)],[c50877,c305]) ).
cnf(c69279,plain,
( ssPv3(skf3(X4809))
| ssPv1(skf3(skf3(X4809)))
| ssPv2(X4809) ),
inference(resolution,[status(thm)],[c50972,c69032]) ).
cnf(c69356,plain,
( ssPv3(skf3(X4810))
| ssPv2(X4810)
| ~ ssPv3(X4810)
| ~ ssPv1(skf3(X4810)) ),
inference(resolution,[status(thm)],[c69279,c7194]) ).
cnf(c70322,plain,
( ssPv2(X4847)
| ssPv3(skf3(X4847))
| ~ ssPv3(X4847) ),
inference(resolution,[status(thm)],[c70228,c69356]) ).
cnf(c70989,plain,
( ssPv2(X4848)
| ssPv3(skf3(X4848)) ),
inference(resolution,[status(thm)],[c70322,c29733]) ).
cnf(c463,plain,
( ~ ssRr(X2414,skf3(X2413))
| ~ ssPv4(X2414)
| ~ ssPv3(X2413)
| ~ ssPv3(skf3(X2413))
| ssPv1(skf3(X2413)) ),
inference(resolution,[status(thm)],[clause25,clause1]) ).
cnf(c25075,plain,
( ~ ssPv4(skf3(skf3(X2415)))
| ~ ssPv3(X2415)
| ~ ssPv3(skf3(X2415))
| ssPv1(skf3(X2415)) ),
inference(resolution,[status(thm)],[c463,clause1]) ).
cnf(c4,plain,
( ~ ssPv1(skf2(X34))
| ~ ssPv4(skf2(X34))
| ssPv2(X34)
| ssPv2(skf2(X34)) ),
inference(resolution,[status(thm)],[clause5,clause2]) ).
cnf(c48917,plain,
( ssPv4(skf2(X3716))
| ~ ssPv4(X3716)
| ssPv2(skf2(X3716)) ),
inference(resolution,[status(thm)],[c48414,clause2]) ).
cnf(c53237,plain,
( ssPv1(X3924)
| ssPv2(X3924)
| ssPv4(skf2(X3924))
| ssPv2(skf2(X3924)) ),
inference(resolution,[status(thm)],[c53162,c48917]) ).
cnf(c53554,plain,
( ssPv1(X3941)
| ssPv2(X3941)
| ssPv2(skf2(X3941))
| ~ ssPv1(skf2(X3941)) ),
inference(resolution,[status(thm)],[c53237,c4]) ).
cnf(c10,plain,
( ~ ssPv3(X15)
| ~ ssPv4(X15)
| ssPv1(skf2(X15))
| ssPv1(X15) ),
inference(resolution,[status(thm)],[clause6,clause2]) ).
cnf(c56636,plain,
( ssPv4(X4061)
| ssPv1(X4061)
| ssPv1(skf2(X4061)) ),
inference(resolution,[status(thm)],[c56491,c30890]) ).
cnf(c56851,plain,
( ssPv1(X4062)
| ssPv1(skf2(X4062))
| ~ ssPv3(X4062) ),
inference(resolution,[status(thm)],[c56636,c10]) ).
cnf(c57013,plain,
( ssPv1(X4063)
| ssPv1(skf2(X4063)) ),
inference(resolution,[status(thm)],[c56851,c30890]) ).
cnf(c57087,plain,
( ssPv1(X4065)
| ssPv2(X4065)
| ssPv2(skf2(X4065)) ),
inference(resolution,[status(thm)],[c57013,c53554]) ).
cnf(c29855,plain,
( ssPv2(skf2(X2726))
| ~ ssRr(X2725,X2726)
| ~ ssPv1(X2725)
| ~ ssPv1(X2726) ),
inference(resolution,[status(thm)],[c29733,c2887]) ).
cnf(c30243,plain,
( ssPv2(skf2(X2727))
| ~ ssPv1(skf3(X2727))
| ~ ssPv1(X2727) ),
inference(resolution,[status(thm)],[c29855,clause1]) ).
cnf(c58481,plain,
( ssPv1(skf3(skf3(X4238)))
| ssPv2(skf2(X4238))
| ~ ssPv1(X4238) ),
inference(resolution,[status(thm)],[c58401,c30243]) ).
cnf(c60263,plain,
( ssPv1(skf3(skf3(X4257)))
| ssPv2(skf2(X4257))
| ssPv2(X4257) ),
inference(resolution,[status(thm)],[c58481,c57087]) ).
cnf(c60408,plain,
( ssPv2(skf2(X4347))
| ssPv2(X4347)
| ~ ssPv3(X4347)
| ~ ssPv1(skf3(X4347)) ),
inference(resolution,[status(thm)],[c60263,c7194]) ).
cnf(c70312,plain,
( ssPv2(X4841)
| ssPv2(skf2(X4841))
| ~ ssPv3(X4841) ),
inference(resolution,[status(thm)],[c70228,c60408]) ).
cnf(c70739,plain,
( ssPv2(X4842)
| ssPv2(skf2(X4842)) ),
inference(resolution,[status(thm)],[c70312,c29733]) ).
cnf(c70869,plain,
( ssPv2(X4998)
| ~ ssPv3(skf2(X4998))
| ~ ssPv3(X4998)
| ssPv4(X4998) ),
inference(resolution,[status(thm)],[c70739,c438]) ).
cnf(c72887,plain,
( ssPv2(X4999)
| ~ ssPv3(X4999)
| ssPv4(X4999) ),
inference(resolution,[status(thm)],[c70869,c48296]) ).
cnf(c72927,plain,
( ssPv2(X5000)
| ssPv4(X5000) ),
inference(resolution,[status(thm)],[c72887,c29733]) ).
cnf(c424,plain,
( ~ ssRr(X328,X329)
| ~ ssPv3(X328)
| ~ ssPv2(X329)
| ~ ssPv3(X329)
| ssPv2(skf2(X329)) ),
inference(resolution,[status(thm)],[clause22,clause2]) ).
cnf(c993,plain,
( ~ ssPv3(skf3(X334))
| ~ ssPv2(X334)
| ~ ssPv3(X334)
| ssPv2(skf2(X334)) ),
inference(resolution,[status(thm)],[c424,clause1]) ).
cnf(c29824,plain,
( ssPv2(skf3(X2762))
| ~ ssPv2(X2762)
| ~ ssPv3(X2762)
| ssPv2(skf2(X2762)) ),
inference(resolution,[status(thm)],[c29733,c993]) ).
cnf(c50934,plain,
( ssPv3(X3814)
| ssPv1(skf3(X3814))
| ssPv2(skf2(X3814)) ),
inference(resolution,[status(thm)],[c50877,c4229]) ).
cnf(c51211,plain,
( ssPv3(X3815)
| ssPv2(skf2(X3815))
| ~ ssPv1(X3815) ),
inference(resolution,[status(thm)],[c50934,c30243]) ).
cnf(c57152,plain,
( ssPv1(X4068)
| ssPv2(skf2(X4068))
| ~ ssPv4(X4068) ),
inference(resolution,[status(thm)],[c57087,c2467]) ).
cnf(c70203,plain,
( ssPv1(X4826)
| ssPv2(skf2(X4826)) ),
inference(resolution,[status(thm)],[c70049,c57152]) ).
cnf(c70256,plain,
( ssPv2(skf2(X4828))
| ssPv3(X4828) ),
inference(resolution,[status(thm)],[c70203,c51211]) ).
cnf(c70454,plain,
( ssPv2(skf2(X4907))
| ssPv2(skf3(X4907))
| ~ ssPv2(X4907) ),
inference(resolution,[status(thm)],[c70256,c29824]) ).
cnf(c71862,plain,
( ssPv2(skf2(X4908))
| ssPv2(skf3(X4908)) ),
inference(resolution,[status(thm)],[c70454,c70739]) ).
cnf(c70187,plain,
( ssPv4(skf3(X4838))
| ~ ssPv2(X4838)
| ssPv4(X4838) ),
inference(resolution,[status(thm)],[c70049,c192]) ).
cnf(c73007,plain,
( ssPv4(X5001)
| ssPv4(skf3(X5001)) ),
inference(resolution,[status(thm)],[c72927,c70187]) ).
cnf(c73076,plain,
( ssPv4(X5031)
| ~ ssPv2(X5031)
| ~ ssPv2(skf3(X5031)) ),
inference(resolution,[status(thm)],[c73007,c402]) ).
cnf(c73466,plain,
( ssPv4(X5042)
| ~ ssPv2(X5042)
| ssPv2(skf2(X5042)) ),
inference(resolution,[status(thm)],[c73076,c71862]) ).
cnf(c73565,plain,
( ssPv4(X5043)
| ssPv2(skf2(X5043)) ),
inference(resolution,[status(thm)],[c73466,c72927]) ).
cnf(c73636,plain,
( ssPv4(X5052)
| ~ ssPv3(skf2(X5052))
| ~ ssPv3(X5052) ),
inference(resolution,[status(thm)],[c73565,c438]) ).
cnf(c73687,plain,
( ssPv4(X5053)
| ~ ssPv3(X5053) ),
inference(resolution,[status(thm)],[c73636,c48296]) ).
cnf(c73740,plain,
( ssPv4(skf3(X5061))
| ssPv1(X5061) ),
inference(resolution,[status(thm)],[c73687,c49264]) ).
cnf(c73766,plain,
( ssPv1(skf3(X5189))
| ~ ssPv3(X5189)
| ~ ssPv3(skf3(X5189)) ),
inference(resolution,[status(thm)],[c73740,c25075]) ).
cnf(c2948,plain,
( ~ ssRr(X1142,skf3(X1143))
| ~ ssPv2(X1142)
| ~ ssPv2(X1143)
| ~ ssPv1(X1143)
| ~ ssPv1(skf3(X1143)) ),
inference(resolution,[status(thm)],[c995,clause1]) ).
cnf(c7341,plain,
( ~ ssPv2(skf3(skf3(X1144)))
| ~ ssPv2(X1144)
| ~ ssPv1(X1144)
| ~ ssPv1(skf3(X1144)) ),
inference(resolution,[status(thm)],[c2948,clause1]) ).
cnf(c29805,plain,
( ssPv3(skf3(skf3(X2845)))
| ~ ssPv2(X2845)
| ~ ssPv1(X2845)
| ~ ssPv1(skf3(X2845)) ),
inference(resolution,[status(thm)],[c29733,c7341]) ).
cnf(c49433,plain,
( ssPv3(skf3(skf3(X3726)))
| ~ ssPv2(X3726)
| ~ ssPv1(X3726) ),
inference(resolution,[status(thm)],[c49264,c29805]) ).
cnf(c29816,plain,
( ssPv3(skf3(skf3(X2851)))
| ~ ssPv4(skf3(X2851))
| ssPv4(X2851)
| ssPv3(X2851) ),
inference(resolution,[status(thm)],[c29733,c5537]) ).
cnf(c48874,plain,
( ssPv3(X3715)
| ssPv3(skf3(skf3(X3715)))
| ssPv4(X3715) ),
inference(resolution,[status(thm)],[c48824,c29816]) ).
cnf(c56642,plain,
( ssPv4(X4091)
| ssPv1(X4091)
| ssPv3(skf3(skf3(X4091))) ),
inference(resolution,[status(thm)],[c56491,c48874]) ).
cnf(c57938,plain,
( ssPv4(X4120)
| ssPv3(skf3(skf3(X4120)))
| ~ ssPv2(X4120) ),
inference(resolution,[status(thm)],[c56642,c49433]) ).
cnf(c72998,plain,
( ssPv4(X5003)
| ssPv3(skf3(skf3(X5003))) ),
inference(resolution,[status(thm)],[c72927,c57938]) ).
cnf(c73465,plain,
( ssPv4(X5039)
| ~ ssPv2(X5039)
| ssPv3(skf3(X5039)) ),
inference(resolution,[status(thm)],[c73076,c29733]) ).
cnf(c73484,plain,
( ssPv4(X5040)
| ssPv3(skf3(X5040)) ),
inference(resolution,[status(thm)],[c73465,c72927]) ).
cnf(c73540,plain,
( ssPv3(skf3(skf3(X5600)))
| ~ ssPv4(X5600)
| ~ ssPv3(skf3(X5600)) ),
inference(resolution,[status(thm)],[c73484,c21676]) ).
cnf(c76326,plain,
( ssPv3(skf3(skf3(X5602)))
| ~ ssPv4(X5602) ),
inference(resolution,[status(thm)],[c73540,c33112]) ).
cnf(c76353,plain,
ssPv3(skf3(skf3(X5603))),
inference(resolution,[status(thm)],[c76326,c72998]) ).
cnf(c76445,plain,
( ssPv1(skf3(skf3(X5623)))
| ~ ssPv3(skf3(X5623)) ),
inference(resolution,[status(thm)],[c76353,c73766]) ).
cnf(c76477,plain,
( ssPv1(skf3(skf3(X5628)))
| ssPv2(X5628) ),
inference(resolution,[status(thm)],[c76445,c70989]) ).
cnf(c76531,plain,
( ssPv2(X5632)
| ~ ssPv3(X5632)
| ~ ssPv1(skf3(X5632)) ),
inference(resolution,[status(thm)],[c76477,c7194]) ).
cnf(c76554,plain,
( ssPv2(X5633)
| ~ ssPv3(X5633) ),
inference(resolution,[status(thm)],[c76531,c70228]) ).
cnf(c76589,plain,
ssPv2(X5634),
inference(resolution,[status(thm)],[c76554,c29733]) ).
cnf(c70436,plain,
( ssPv3(X4902)
| ~ ssRr(X4901,X4902)
| ~ ssPv2(X4901)
| ~ ssPv1(X4902) ),
inference(resolution,[status(thm)],[c70256,c30962]) ).
cnf(c71738,plain,
( ssPv3(X4903)
| ~ ssPv2(skf3(X4903))
| ~ ssPv1(X4903) ),
inference(resolution,[status(thm)],[c70436,clause1]) ).
cnf(c76625,plain,
( ssPv3(X5638)
| ~ ssPv1(X5638) ),
inference(resolution,[status(thm)],[c76589,c71738]) ).
cnf(c76639,plain,
( ssPv3(X5657)
| ssPv1(skf3(X5657)) ),
inference(resolution,[status(thm)],[c76625,c58401]) ).
cnf(c76667,plain,
ssPv1(skf3(skf3(X5658))),
inference(resolution,[status(thm)],[c76639,c76445]) ).
cnf(c76626,plain,
( ~ ssPv2(X5684)
| ~ ssPv1(X5684)
| ~ ssPv1(skf3(X5684)) ),
inference(resolution,[status(thm)],[c76589,c7341]) ).
cnf(c76682,plain,
( ~ ssPv2(skf3(X5688))
| ~ ssPv1(skf3(X5688)) ),
inference(resolution,[status(thm)],[c76626,c76667]) ).
cnf(c76691,plain,
~ ssPv2(skf3(skf3(X5689))),
inference(resolution,[status(thm)],[c76682,c76667]) ).
cnf(c76694,plain,
$false,
inference(resolution,[status(thm)],[c76691,c76589]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SYN784-1 : TPTP v8.1.2. Released v2.5.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n020.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 20:06:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 76.22/76.38 % Version: 1.5
% 76.22/76.38 % SZS status Unsatisfiable
% 76.22/76.38 % SZS output start CNFRefutation
% See solution above
% 76.23/76.39
% 76.23/76.39 % Initial clauses : 42
% 76.23/76.39 % Processed clauses : 1375
% 76.23/76.39 % Factors computed : 98
% 76.23/76.39 % Resolvents computed: 76597
% 76.23/76.39 % Tautologies deleted: 464
% 76.23/76.39 % Forward subsumed : 3371
% 76.23/76.39 % Backward subsumed : 1308
% 76.23/76.39 % -------- CPU Time ---------
% 76.23/76.39 % User time : 75.795 s
% 76.23/76.39 % System time : 0.237 s
% 76.23/76.39 % Total time : 76.032 s
%------------------------------------------------------------------------------