%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN796-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:03 EDT 2024
% Result : Unsatisfiable 279.30s 279.57s
% Output : Refutation 279.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 88
% Number of leaves : 39
% Syntax : Number of clauses : 451 ( 8 unt; 379 nHn; 274 RR)
% Number of literals : 1825 ( 0 equ; 604 neg)
% Maximal clause size : 7 ( 4 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 : 608 ( 5 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssRr(skf3(X2),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(clause2,negated_conjecture,
ssRr(X3,skf2(X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
cnf(clause8,negated_conjecture,
( ~ ssRr(X20,X19)
| ~ ssRr(X19,X18)
| ssPv4(X20)
| ssPv2(X18)
| ssPv1(X19)
| ssPv2(X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
cnf(c13,plain,
( ~ ssRr(X53,X52)
| ssPv4(X53)
| ssPv2(skf2(X52))
| ssPv1(X52)
| ssPv2(X52) ),
inference(resolution,[status(thm)],[clause8,clause2]) ).
cnf(c75,plain,
( ssPv4(skf3(X58))
| ssPv2(skf2(X58))
| ssPv1(X58)
| ssPv2(X58) ),
inference(resolution,[status(thm)],[c13,clause1]) ).
cnf(clause28,negated_conjecture,
( ~ ssRr(X209,X208)
| ~ ssPv4(X208)
| ~ ssRr(X209,X207)
| ~ ssPv2(X207)
| ssPv1(X209)
| ssPv2(X209) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
cnf(c516,plain,
( ~ ssRr(X210,X211)
| ~ ssPv4(X211)
| ~ ssPv2(X211)
| ssPv1(X210)
| ssPv2(X210) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c519,plain,
( ~ ssPv4(skf2(X212))
| ~ ssPv2(skf2(X212))
| ssPv1(X212)
| ssPv2(X212) ),
inference(resolution,[status(thm)],[c516,clause2]) ).
cnf(c525,plain,
( ~ ssPv4(skf2(X214))
| ssPv1(X214)
| ssPv2(X214)
| ssPv4(skf3(X214)) ),
inference(resolution,[status(thm)],[c519,c75]) ).
cnf(clause38,negated_conjecture,
( ~ ssRr(X307,X305)
| ~ ssRr(X305,X304)
| ~ ssPv1(X304)
| ~ ssRr(X305,X306)
| ssPv4(X307)
| ssPv4(X306)
| ssPv2(X305) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
cnf(c785,plain,
( ~ ssRr(X439,X437)
| ~ ssRr(X437,X438)
| ~ ssPv1(X438)
| ssPv4(X439)
| ssPv4(X438)
| ssPv2(X437) ),
inference(factor,[status(thm)],[clause38]) ).
cnf(c1301,plain,
( ~ ssRr(X531,X530)
| ~ ssPv1(skf2(X530))
| ssPv4(X531)
| ssPv4(skf2(X530))
| ssPv2(X530) ),
inference(resolution,[status(thm)],[c785,clause2]) ).
cnf(clause5,negated_conjecture,
( ~ ssRr(X10,X9)
| ~ ssPv2(X9)
| ssPv2(X10)
| ssPv1(X9)
| ssPv4(X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(c4,plain,
( ~ ssPv2(skf2(X33))
| ssPv2(X33)
| ssPv1(skf2(X33))
| ssPv4(skf2(X33)) ),
inference(resolution,[status(thm)],[clause5,clause2]) ).
cnf(clause10,negated_conjecture,
( ~ ssRr(X37,X36)
| ~ ssPv4(X37)
| ~ ssRr(X35,X36)
| ssPv3(X35)
| ssPv3(X36)
| ssPv4(X36) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(c34,plain,
( ~ ssRr(X38,X39)
| ~ ssPv4(X38)
| ssPv3(X38)
| ssPv3(X39)
| ssPv4(X39) ),
inference(factor,[status(thm)],[clause10]) ).
cnf(c38,plain,
( ~ ssPv4(skf3(X41))
| ssPv3(skf3(X41))
| ssPv3(X41)
| ssPv4(X41) ),
inference(resolution,[status(thm)],[c34,clause1]) ).
cnf(clause11,negated_conjecture,
( ~ ssRr(X46,X45)
| ~ ssPv1(X45)
| ~ ssRr(X46,X44)
| ssPv2(X44)
| ssPv3(X46)
| ssPv4(X46) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(c58,plain,
( ~ ssRr(X48,X47)
| ~ ssPv1(X47)
| ssPv2(X47)
| ssPv3(X48)
| ssPv4(X48) ),
inference(factor,[status(thm)],[clause11]) ).
cnf(c62,plain,
( ~ ssPv1(X50)
| ssPv2(X50)
| ssPv3(skf3(X50))
| ssPv4(skf3(X50)) ),
inference(resolution,[status(thm)],[c58,clause1]) ).
cnf(clause20,negated_conjecture,
( ~ ssRr(X134,X133)
| ~ ssRr(X132,X133)
| ~ ssPv1(X133)
| ~ ssPv2(X133)
| ssPv3(X134)
| ssPv2(X132) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(c266,plain,
( ~ ssRr(X136,X135)
| ~ ssPv1(X135)
| ~ ssPv2(X135)
| ssPv3(X136)
| ssPv2(X136) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c269,plain,
( ~ ssPv1(skf2(X137))
| ~ ssPv2(skf2(X137))
| ssPv3(X137)
| ssPv2(X137) ),
inference(resolution,[status(thm)],[c266,clause2]) ).
cnf(c273,plain,
( ~ ssPv1(skf2(X197))
| ssPv3(X197)
| ssPv2(X197)
| ssPv4(skf3(X197))
| ssPv1(X197) ),
inference(resolution,[status(thm)],[c269,c75]) ).
cnf(c85,plain,
( ssPv4(skf3(X610))
| ssPv1(X610)
| ssPv2(X610)
| ssPv1(skf2(X610))
| ssPv4(skf2(X610)) ),
inference(resolution,[status(thm)],[c75,c4]) ).
cnf(c2761,plain,
( ssPv4(skf3(X611))
| ssPv1(X611)
| ssPv2(X611)
| ssPv1(skf2(X611)) ),
inference(resolution,[status(thm)],[c85,c525]) ).
cnf(c2856,plain,
( ssPv4(skf3(X613))
| ssPv1(X613)
| ssPv2(X613)
| ssPv3(X613) ),
inference(resolution,[status(thm)],[c2761,c273]) ).
cnf(c2983,plain,
( ssPv4(skf3(X614))
| ssPv2(X614)
| ssPv3(X614)
| ssPv3(skf3(X614)) ),
inference(resolution,[status(thm)],[c2856,c62]) ).
cnf(c3066,plain,
( ssPv2(X615)
| ssPv3(X615)
| ssPv3(skf3(X615))
| ssPv4(X615) ),
inference(resolution,[status(thm)],[c2983,c38]) ).
cnf(clause22,negated_conjecture,
( ~ ssRr(X153,X152)
| ~ ssPv3(X152)
| ~ ssRr(X153,X151)
| ~ ssPv1(X153)
| ssPv1(X151)
| ssPv3(X153) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
cnf(c334,plain,
( ~ ssRr(X154,X155)
| ~ ssPv3(X155)
| ~ ssPv1(X154)
| ssPv1(X155)
| ssPv3(X154) ),
inference(factor,[status(thm)],[clause22]) ).
cnf(c338,plain,
( ~ ssPv3(X157)
| ~ ssPv1(skf3(X157))
| ssPv1(X157)
| ssPv3(skf3(X157)) ),
inference(resolution,[status(thm)],[c334,clause1]) ).
cnf(clause36,negated_conjecture,
( ~ ssRr(X288,X286)
| ~ ssPv2(X286)
| ~ ssRr(X288,X285)
| ~ ssRr(X288,X287)
| ssPv4(X285)
| ssPv2(X287)
| ssPv3(X288) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
cnf(c707,plain,
( ~ ssRr(X394,X395)
| ~ ssPv2(X395)
| ~ ssRr(X394,X393)
| ssPv4(X393)
| ssPv2(X393)
| ssPv3(X394) ),
inference(factor,[status(thm)],[clause36]) ).
cnf(c1202,plain,
( ~ ssRr(skf3(X513),X512)
| ~ ssPv2(X512)
| ssPv4(X513)
| ssPv2(X513)
| ssPv3(skf3(X513)) ),
inference(resolution,[status(thm)],[c707,clause1]) ).
cnf(c1516,plain,
( ~ ssPv2(skf2(skf3(X515)))
| ssPv4(X515)
| ssPv2(X515)
| ssPv3(skf3(X515)) ),
inference(resolution,[status(thm)],[c1202,clause2]) ).
cnf(clause17,negated_conjecture,
( ~ ssRr(X106,X105)
| ~ ssPv2(X106)
| ~ ssRr(X105,X104)
| ssPv2(X104)
| ssPv1(X105)
| ssPv3(X105) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
cnf(c171,plain,
( ~ ssRr(X108,X109)
| ~ ssPv2(X108)
| ssPv2(skf2(X109))
| ssPv1(X109)
| ssPv3(X109) ),
inference(resolution,[status(thm)],[clause17,clause2]) ).
cnf(c174,plain,
( ~ ssPv2(skf3(X110))
| ssPv2(skf2(X110))
| ssPv1(X110)
| ssPv3(X110) ),
inference(resolution,[status(thm)],[c171,clause1]) ).
cnf(clause6,negated_conjecture,
( ~ ssRr(X14,X13)
| ~ ssPv4(X13)
| ssPv2(X14)
| ssPv1(X13)
| ssPv3(X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
cnf(c8,plain,
( ~ ssPv4(X15)
| ssPv2(skf3(X15))
| ssPv1(X15)
| ssPv3(X15) ),
inference(resolution,[status(thm)],[clause6,clause1]) ).
cnf(c5,plain,
( ~ ssPv2(X12)
| ssPv2(skf3(X12))
| ssPv1(X12)
| ssPv4(X12) ),
inference(resolution,[status(thm)],[clause5,clause1]) ).
cnf(clause9,negated_conjecture,
( ~ ssRr(X28,X27)
| ~ ssRr(X26,X27)
| ~ ssPv1(X27)
| ssPv4(X28)
| ssPv1(X26)
| ssPv4(X27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
cnf(c23,plain,
( ~ ssRr(X29,X30)
| ~ ssPv1(X30)
| ssPv4(X29)
| ssPv1(X29)
| ssPv4(X30) ),
inference(factor,[status(thm)],[clause9]) ).
cnf(c27,plain,
( ~ ssPv1(X32)
| ssPv4(skf3(X32))
| ssPv1(skf3(X32))
| ssPv4(X32) ),
inference(resolution,[status(thm)],[c23,clause1]) ).
cnf(c26,plain,
( ~ ssPv1(skf2(X31))
| ssPv4(X31)
| ssPv1(X31)
| ssPv4(skf2(X31)) ),
inference(resolution,[status(thm)],[c23,clause2]) ).
cnf(c2745,plain,
( ssPv4(skf3(X644))
| ssPv1(X644)
| ssPv2(X644)
| ssPv4(skf2(X644))
| ssPv4(X644) ),
inference(resolution,[status(thm)],[c85,c26]) ).
cnf(c3701,plain,
( ssPv4(skf3(X645))
| ssPv1(X645)
| ssPv2(X645)
| ssPv4(X645) ),
inference(resolution,[status(thm)],[c2745,c525]) ).
cnf(c3805,plain,
( ssPv4(skf3(X651))
| ssPv1(X651)
| ssPv4(X651)
| ssPv2(skf3(X651)) ),
inference(resolution,[status(thm)],[c3701,c5]) ).
cnf(c4107,plain,
( ssPv4(skf3(X674))
| ssPv4(X674)
| ssPv2(skf3(X674))
| ssPv1(skf3(X674)) ),
inference(resolution,[status(thm)],[c3805,c27]) ).
cnf(c5018,plain,
( ssPv4(skf3(X843))
| ssPv4(X843)
| ssPv1(skf3(X843))
| ssPv2(skf3(skf3(X843))) ),
inference(resolution,[status(thm)],[c4107,c5]) ).
cnf(c7149,plain,
( ssPv4(X853)
| ssPv1(skf3(X853))
| ssPv2(skf3(skf3(X853)))
| ssPv3(skf3(X853)) ),
inference(resolution,[status(thm)],[c5018,c8]) ).
cnf(c7772,plain,
( ssPv4(X857)
| ssPv1(skf3(X857))
| ssPv3(skf3(X857))
| ssPv2(skf2(skf3(X857))) ),
inference(resolution,[status(thm)],[c7149,c174]) ).
cnf(c8051,plain,
( ssPv4(X858)
| ssPv1(skf3(X858))
| ssPv3(skf3(X858))
| ssPv2(X858) ),
inference(resolution,[status(thm)],[c7772,c1516]) ).
cnf(c8107,plain,
( ssPv4(X861)
| ssPv3(skf3(X861))
| ssPv2(X861)
| ~ ssPv3(X861)
| ssPv1(X861) ),
inference(resolution,[status(thm)],[c8051,c338]) ).
cnf(c8185,plain,
( ssPv4(X862)
| ssPv3(skf3(X862))
| ssPv2(X862)
| ssPv1(X862) ),
inference(resolution,[status(thm)],[c8107,c3066]) ).
cnf(c8282,plain,
( ssPv4(skf2(X901))
| ssPv3(skf3(skf2(X901)))
| ssPv1(skf2(X901))
| ssPv2(X901) ),
inference(resolution,[status(thm)],[c8185,c4]) ).
cnf(clause15,negated_conjecture,
( ~ ssRr(X85,X84)
| ~ ssPv3(X85)
| ~ ssRr(X83,X84)
| ssPv4(X83)
| ssPv1(X84)
| ssPv4(X84) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
cnf(c133,plain,
( ~ ssRr(X965,skf2(X964))
| ~ ssPv3(X965)
| ssPv4(X964)
| ssPv1(skf2(X964))
| ssPv4(skf2(X964)) ),
inference(resolution,[status(thm)],[clause15,clause2]) ).
cnf(c10288,plain,
( ~ ssPv3(skf3(skf2(X1008)))
| ssPv4(X1008)
| ssPv1(skf2(X1008))
| ssPv4(skf2(X1008)) ),
inference(resolution,[status(thm)],[c133,clause1]) ).
cnf(c11305,plain,
( ssPv4(X1009)
| ssPv1(skf2(X1009))
| ssPv4(skf2(X1009))
| ssPv2(X1009) ),
inference(resolution,[status(thm)],[c10288,c8282]) ).
cnf(c11354,plain,
( ssPv4(X1048)
| ssPv4(skf2(X1048))
| ssPv2(X1048)
| ~ ssRr(X1049,X1048)
| ssPv4(X1049) ),
inference(resolution,[status(thm)],[c11305,c1301]) ).
cnf(c13027,plain,
( ssPv4(X1051)
| ssPv4(skf2(X1051))
| ssPv2(X1051)
| ssPv4(skf3(X1051)) ),
inference(resolution,[status(thm)],[c11354,clause1]) ).
cnf(clause46,negated_conjecture,
( ~ ssRr(X386,X384)
| ~ ssPv4(X386)
| ~ ssRr(X383,X384)
| ~ ssPv3(X383)
| ~ ssRr(X385,X384)
| ~ ssPv1(X385)
| ssPv2(X384) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
cnf(c1196,plain,
( ~ ssRr(X492,X493)
| ~ ssPv4(X492)
| ~ ssRr(X491,X493)
| ~ ssPv3(X491)
| ~ ssPv1(X492)
| ssPv2(X493) ),
inference(factor,[status(thm)],[clause46]) ).
cnf(c1416,plain,
( ~ ssRr(X494,X495)
| ~ ssPv4(X494)
| ~ ssPv3(X494)
| ~ ssPv1(X494)
| ssPv2(X495) ),
inference(factor,[status(thm)],[c1196]) ).
cnf(c1419,plain,
( ~ ssPv4(X496)
| ~ ssPv3(X496)
| ~ ssPv1(X496)
| ssPv2(skf2(X496)) ),
inference(resolution,[status(thm)],[c1416,clause2]) ).
cnf(clause13,negated_conjecture,
( ~ ssRr(X66,X65)
| ~ ssRr(X65,X64)
| ~ ssPv3(X65)
| ssPv4(X66)
| ssPv2(X64)
| ssPv1(X65) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
cnf(c98,plain,
( ~ ssRr(X81,X80)
| ~ ssPv3(X80)
| ssPv4(X81)
| ssPv2(skf2(X80))
| ssPv1(X80) ),
inference(resolution,[status(thm)],[clause13,clause2]) ).
cnf(c120,plain,
( ~ ssPv3(X82)
| ssPv4(skf3(X82))
| ssPv2(skf2(X82))
| ssPv1(X82) ),
inference(resolution,[status(thm)],[c98,clause1]) ).
cnf(c4142,plain,
( ssPv4(skf3(X653))
| ssPv1(X653)
| ssPv2(skf3(X653))
| ssPv3(X653) ),
inference(resolution,[status(thm)],[c3805,c8]) ).
cnf(c4289,plain,
( ssPv4(skf3(X658))
| ssPv1(X658)
| ssPv3(X658)
| ssPv2(skf2(X658)) ),
inference(resolution,[status(thm)],[c4142,c174]) ).
cnf(c4548,plain,
( ssPv4(skf3(X659))
| ssPv1(X659)
| ssPv2(skf2(X659)) ),
inference(resolution,[status(thm)],[c4289,c120]) ).
cnf(c4590,plain,
( ssPv4(skf3(X665))
| ssPv2(skf2(X665))
| ~ ssPv4(X665)
| ~ ssPv3(X665) ),
inference(resolution,[status(thm)],[c4548,c1419]) ).
cnf(clause7,negated_conjecture,
( ~ ssRr(X17,X16)
| ~ ssPv1(X17)
| ~ ssPv1(X16)
| ~ ssPv4(X16)
| ssPv2(X16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(c11,plain,
( ~ ssPv1(skf3(X22))
| ~ ssPv1(X22)
| ~ ssPv4(X22)
| ssPv2(X22) ),
inference(resolution,[status(thm)],[clause7,clause1]) ).
cnf(c4600,plain,
( ssPv4(skf3(X684))
| ssPv2(skf2(X684))
| ssPv1(skf3(X684))
| ssPv4(X684) ),
inference(resolution,[status(thm)],[c4548,c27]) ).
cnf(clause3,negated_conjecture,
( ~ ssRr(X5,X4)
| ssPv3(X4)
| ssPv1(X5)
| ssPv3(X5)
| ssPv4(X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(c1,plain,
( ssPv3(X24)
| ssPv1(skf3(X24))
| ssPv3(skf3(X24))
| ssPv4(skf3(X24)) ),
inference(resolution,[status(thm)],[clause3,clause1]) ).
cnf(c41,plain,
( ssPv3(skf3(X43))
| ssPv3(X43)
| ssPv4(X43)
| ssPv1(skf3(X43)) ),
inference(resolution,[status(thm)],[c38,c1]) ).
cnf(c132,plain,
( ~ ssRr(X86,X87)
| ~ ssPv3(X86)
| ssPv4(X86)
| ssPv1(X87)
| ssPv4(X87) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c136,plain,
( ~ ssPv3(skf3(X89))
| ssPv4(skf3(X89))
| ssPv1(X89)
| ssPv4(X89) ),
inference(resolution,[status(thm)],[c132,clause1]) ).
cnf(c148,plain,
( ssPv4(skf3(X177))
| ssPv1(X177)
| ssPv4(X177)
| ssPv3(X177)
| ssPv1(skf3(X177)) ),
inference(resolution,[status(thm)],[c136,c41]) ).
cnf(c400,plain,
( ssPv4(skf3(X178))
| ssPv4(X178)
| ssPv3(X178)
| ssPv1(skf3(X178)) ),
inference(resolution,[status(thm)],[c148,c27]) ).
cnf(clause21,negated_conjecture,
( ~ ssRr(X144,X143)
| ~ ssPv3(X144)
| ~ ssRr(X143,X142)
| ~ ssPv4(X143)
| ssPv2(X142)
| ssPv3(X143) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
cnf(c289,plain,
( ~ ssRr(X146,X147)
| ~ ssPv3(X146)
| ~ ssPv4(X147)
| ssPv2(skf2(X147))
| ssPv3(X147) ),
inference(resolution,[status(thm)],[clause21,clause2]) ).
cnf(c292,plain,
( ~ ssPv3(skf3(X148))
| ~ ssPv4(X148)
| ssPv2(skf2(X148))
| ssPv3(X148) ),
inference(resolution,[status(thm)],[c289,clause1]) ).
cnf(c299,plain,
( ~ ssPv4(X929)
| ssPv2(skf2(X929))
| ssPv3(X929)
| ssPv1(skf3(X929))
| ssPv4(skf3(X929)) ),
inference(resolution,[status(thm)],[c292,c1]) ).
cnf(c9510,plain,
( ssPv2(skf2(X930))
| ssPv3(X930)
| ssPv1(skf3(X930))
| ssPv4(skf3(X930)) ),
inference(resolution,[status(thm)],[c299,c400]) ).
cnf(c9569,plain,
( ssPv2(skf2(X934))
| ssPv1(skf3(X934))
| ssPv4(skf3(X934))
| ~ ssPv4(X934) ),
inference(resolution,[status(thm)],[c9510,c4590]) ).
cnf(c9766,plain,
( ssPv2(skf2(X935))
| ssPv1(skf3(X935))
| ssPv4(skf3(X935)) ),
inference(resolution,[status(thm)],[c9569,c4600]) ).
cnf(clause26,negated_conjecture,
( ~ ssRr(X190,X189)
| ~ ssPv2(X189)
| ~ ssRr(X190,X188)
| ~ ssPv1(X188)
| ssPv2(X190)
| ssPv3(X190) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
cnf(c455,plain,
( ~ ssRr(X193,X194)
| ~ ssPv2(X194)
| ~ ssPv1(skf2(X193))
| ssPv2(X193)
| ssPv3(X193) ),
inference(resolution,[status(thm)],[clause26,clause2]) ).
cnf(c337,plain,
( ~ ssPv3(skf2(X156))
| ~ ssPv1(X156)
| ssPv1(skf2(X156))
| ssPv3(X156) ),
inference(resolution,[status(thm)],[c334,clause2]) ).
cnf(c7,plain,
( ~ ssPv4(skf2(X34))
| ssPv2(X34)
| ssPv1(skf2(X34))
| ssPv3(skf2(X34)) ),
inference(resolution,[status(thm)],[clause6,clause2]) ).
cnf(clause4,negated_conjecture,
( ~ ssRr(X8,X7)
| ~ ssPv4(X8)
| ssPv1(X7)
| ssPv2(X8)
| ssPv3(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(c2,plain,
( ~ ssPv4(X11)
| ssPv1(skf2(X11))
| ssPv2(X11)
| ssPv3(X11) ),
inference(resolution,[status(thm)],[clause4,clause2]) ).
cnf(c11335,plain,
( ssPv1(skf2(X1014))
| ssPv4(skf2(X1014))
| ssPv2(X1014)
| ssPv3(X1014) ),
inference(resolution,[status(thm)],[c11305,c2]) ).
cnf(c11552,plain,
( ssPv1(skf2(X1020))
| ssPv2(X1020)
| ssPv3(X1020)
| ssPv3(skf2(X1020)) ),
inference(resolution,[status(thm)],[c11335,c7]) ).
cnf(c12009,plain,
( ssPv1(skf2(X1021))
| ssPv2(X1021)
| ssPv3(X1021)
| ~ ssPv1(X1021) ),
inference(resolution,[status(thm)],[c11552,c337]) ).
cnf(c12067,plain,
( ssPv1(skf2(X1028))
| ssPv2(X1028)
| ssPv3(X1028)
| ssPv4(skf3(X1028)) ),
inference(resolution,[status(thm)],[c12009,c2856]) ).
cnf(c12347,plain,
( ssPv2(X1093)
| ssPv3(X1093)
| ssPv4(skf3(X1093))
| ~ ssRr(X1093,X1094)
| ~ ssPv2(X1094) ),
inference(resolution,[status(thm)],[c12067,c455]) ).
cnf(c14094,plain,
( ssPv2(X1095)
| ssPv3(X1095)
| ssPv4(skf3(X1095))
| ~ ssPv2(skf2(X1095)) ),
inference(resolution,[status(thm)],[c12347,clause2]) ).
cnf(c14148,plain,
( ssPv2(X1100)
| ssPv3(X1100)
| ssPv4(skf3(X1100))
| ssPv1(skf3(X1100)) ),
inference(resolution,[status(thm)],[c14094,c9766]) ).
cnf(c14265,plain,
( ssPv2(X1103)
| ssPv3(X1103)
| ssPv4(skf3(X1103))
| ~ ssPv1(X1103)
| ~ ssPv4(X1103) ),
inference(resolution,[status(thm)],[c14148,c11]) ).
cnf(c61,plain,
( ~ ssPv1(skf2(X49))
| ssPv2(skf2(X49))
| ssPv3(X49)
| ssPv4(X49) ),
inference(resolution,[status(thm)],[c58,clause2]) ).
cnf(c12349,plain,
( ssPv2(X1176)
| ssPv3(X1176)
| ssPv4(skf3(X1176))
| ssPv2(skf2(X1176))
| ssPv4(X1176) ),
inference(resolution,[status(thm)],[c12067,c61]) ).
cnf(c15601,plain,
( ssPv2(X1177)
| ssPv3(X1177)
| ssPv4(skf3(X1177))
| ssPv4(X1177) ),
inference(resolution,[status(thm)],[c12349,c14094]) ).
cnf(c15736,plain,
( ssPv2(X1181)
| ssPv3(X1181)
| ssPv4(skf3(X1181))
| ~ ssPv1(X1181) ),
inference(resolution,[status(thm)],[c15601,c14265]) ).
cnf(c15898,plain,
( ssPv2(X1182)
| ssPv3(X1182)
| ssPv4(skf3(X1182)) ),
inference(resolution,[status(thm)],[c15736,c2856]) ).
cnf(c15984,plain,
( ssPv2(X1207)
| ssPv4(skf3(X1207))
| ssPv2(skf2(X1207))
| ~ ssPv4(X1207) ),
inference(resolution,[status(thm)],[c15898,c4590]) ).
cnf(c16324,plain,
( ssPv2(X1227)
| ssPv4(skf3(X1227))
| ssPv2(skf2(X1227))
| ssPv4(skf2(X1227)) ),
inference(resolution,[status(thm)],[c15984,c13027]) ).
cnf(c17082,plain,
( ssPv2(X1233)
| ssPv4(skf3(X1233))
| ssPv4(skf2(X1233))
| ssPv1(skf2(X1233)) ),
inference(resolution,[status(thm)],[c16324,c4]) ).
cnf(c17327,plain,
( ssPv2(X1932)
| ssPv4(skf3(X1932))
| ssPv4(skf2(X1932))
| ~ ssRr(X1933,X1932)
| ssPv4(X1933) ),
inference(resolution,[status(thm)],[c17082,c1301]) ).
cnf(c30370,plain,
( ssPv2(X1934)
| ssPv4(skf3(X1934))
| ssPv4(skf2(X1934)) ),
inference(resolution,[status(thm)],[c17327,clause1]) ).
cnf(c30442,plain,
( ssPv2(X1935)
| ssPv4(skf3(X1935))
| ssPv1(X1935) ),
inference(resolution,[status(thm)],[c30370,c525]) ).
cnf(clause30,negated_conjecture,
( ~ ssRr(X229,X228)
| ~ ssPv1(X228)
| ~ ssRr(X229,X227)
| ~ ssPv2(X229)
| ~ ssPv3(X229)
| ssPv4(X227) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
cnf(c564,plain,
( ~ ssRr(X231,X230)
| ~ ssPv1(X230)
| ~ ssPv2(X231)
| ~ ssPv3(X231)
| ssPv4(X230) ),
inference(factor,[status(thm)],[clause30]) ).
cnf(c568,plain,
( ~ ssPv1(X233)
| ~ ssPv2(skf3(X233))
| ~ ssPv3(skf3(X233))
| ssPv4(X233) ),
inference(resolution,[status(thm)],[c564,clause1]) ).
cnf(c3761,plain,
( ssPv4(skf3(X646))
| ssPv2(X646)
| ssPv4(X646)
| ssPv3(skf3(X646)) ),
inference(resolution,[status(thm)],[c3701,c62]) ).
cnf(c3903,plain,
( ssPv4(skf3(X735))
| ssPv2(X735)
| ssPv4(X735)
| ~ ssPv1(X735)
| ~ ssPv2(skf3(X735)) ),
inference(resolution,[status(thm)],[c3761,c568]) ).
cnf(clause25,negated_conjecture,
( ~ ssRr(X181,X180)
| ~ ssRr(X180,X179)
| ~ ssPv4(X179)
| ~ ssPv1(X180)
| ssPv2(X181)
| ssPv2(X180) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
cnf(c447,plain,
( ~ ssRr(X186,X185)
| ~ ssPv4(skf2(X185))
| ~ ssPv1(X185)
| ssPv2(X186)
| ssPv2(X185) ),
inference(resolution,[status(thm)],[clause25,clause2]) ).
cnf(c30448,plain,
( ssPv2(X1961)
| ssPv4(skf3(X1961))
| ~ ssRr(X1960,X1961)
| ~ ssPv1(X1961)
| ssPv2(X1960) ),
inference(resolution,[status(thm)],[c30370,c447]) ).
cnf(c31163,plain,
( ssPv2(X1962)
| ssPv4(skf3(X1962))
| ~ ssPv1(X1962)
| ssPv2(skf3(X1962)) ),
inference(resolution,[status(thm)],[c30448,clause1]) ).
cnf(c31235,plain,
( ssPv2(X1964)
| ssPv4(skf3(X1964))
| ssPv2(skf3(X1964)) ),
inference(resolution,[status(thm)],[c31163,c30442]) ).
cnf(c31359,plain,
( ssPv2(X1965)
| ssPv4(skf3(X1965))
| ssPv4(X1965)
| ~ ssPv1(X1965) ),
inference(resolution,[status(thm)],[c31235,c3903]) ).
cnf(c31432,plain,
( ssPv2(X1966)
| ssPv4(skf3(X1966))
| ssPv4(X1966) ),
inference(resolution,[status(thm)],[c31359,c30442]) ).
cnf(c31559,plain,
( ssPv2(X1968)
| ssPv4(skf3(X1968))
| ssPv2(skf2(X1968)) ),
inference(resolution,[status(thm)],[c31432,c15984]) ).
cnf(clause34,negated_conjecture,
( ~ ssRr(X268,X267)
| ~ ssPv2(X267)
| ~ ssRr(X268,X266)
| ~ ssPv1(X266)
| ~ ssPv1(X268)
| ~ ssPv4(X268) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
cnf(c674,plain,
( ~ ssRr(X269,X270)
| ~ ssPv2(X270)
| ~ ssPv1(X270)
| ~ ssPv1(X269)
| ~ ssPv4(X269) ),
inference(factor,[status(thm)],[clause34]) ).
cnf(c677,plain,
( ~ ssPv2(skf2(X271))
| ~ ssPv1(skf2(X271))
| ~ ssPv1(X271)
| ~ ssPv4(X271) ),
inference(resolution,[status(thm)],[c674,clause2]) ).
cnf(clause32,negated_conjecture,
( ~ ssRr(X248,X247)
| ~ ssPv2(X247)
| ~ ssRr(X248,X246)
| ~ ssPv1(X248)
| ~ ssPv3(X248)
| ssPv1(X246) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
cnf(c618,plain,
( ~ ssRr(X249,X250)
| ~ ssPv2(X250)
| ~ ssPv1(X249)
| ~ ssPv3(X249)
| ssPv1(X250) ),
inference(factor,[status(thm)],[clause32]) ).
cnf(c621,plain,
( ~ ssPv2(skf2(X251))
| ~ ssPv1(X251)
| ~ ssPv3(X251)
| ssPv1(skf2(X251)) ),
inference(resolution,[status(thm)],[c618,clause2]) ).
cnf(c74,plain,
( ssPv4(X312)
| ssPv2(skf2(skf2(X312)))
| ssPv1(skf2(X312))
| ssPv2(skf2(X312)) ),
inference(resolution,[status(thm)],[c13,clause2]) ).
cnf(c821,plain,
( ssPv4(X445)
| ssPv1(skf2(X445))
| ssPv2(skf2(X445))
| ~ ssPv4(skf2(skf2(X445))) ),
inference(resolution,[status(thm)],[c74,c519]) ).
cnf(c11352,plain,
( ssPv4(X1010)
| ssPv4(skf2(X1010))
| ssPv2(X1010)
| ssPv1(X1010) ),
inference(resolution,[status(thm)],[c11305,c26]) ).
cnf(c11479,plain,
( ssPv4(X1018)
| ssPv4(skf2(X1018))
| ssPv1(X1018)
| ssPv2(skf3(X1018)) ),
inference(resolution,[status(thm)],[c11352,c5]) ).
cnf(c11847,plain,
( ssPv4(skf2(X1024))
| ssPv1(X1024)
| ssPv2(skf3(X1024))
| ssPv3(X1024) ),
inference(resolution,[status(thm)],[c11479,c8]) ).
cnf(c12162,plain,
( ssPv4(skf2(X1030))
| ssPv1(X1030)
| ssPv3(X1030)
| ssPv2(skf2(X1030)) ),
inference(resolution,[status(thm)],[c11847,c174]) ).
cnf(c11548,plain,
( ssPv4(skf2(X1060))
| ssPv2(X1060)
| ssPv3(X1060)
| ~ ssRr(X1060,X1061)
| ~ ssPv2(X1061) ),
inference(resolution,[status(thm)],[c11335,c455]) ).
cnf(c13214,plain,
( ssPv4(skf2(X1062))
| ssPv2(X1062)
| ssPv3(X1062)
| ~ ssPv2(skf2(X1062)) ),
inference(resolution,[status(thm)],[c11548,clause2]) ).
cnf(c13219,plain,
( ssPv4(skf2(X1063))
| ssPv2(X1063)
| ssPv3(X1063)
| ssPv1(X1063) ),
inference(resolution,[status(thm)],[c13214,c12162]) ).
cnf(c13302,plain,
( ssPv2(skf2(X1111))
| ssPv3(skf2(X1111))
| ssPv1(skf2(X1111))
| ssPv4(X1111) ),
inference(resolution,[status(thm)],[c13219,c821]) ).
cnf(c14655,plain,
( ssPv2(skf2(X1112))
| ssPv3(skf2(X1112))
| ssPv4(X1112)
| ssPv3(X1112) ),
inference(resolution,[status(thm)],[c13302,c61]) ).
cnf(c0,plain,
( ssPv3(skf2(X6))
| ssPv1(X6)
| ssPv3(X6)
| ssPv4(X6) ),
inference(resolution,[status(thm)],[clause3,clause2]) ).
cnf(c9,plain,
( ssPv2(skf3(X23))
| ssPv1(X23)
| ssPv3(X23)
| ssPv3(skf2(X23)) ),
inference(resolution,[status(thm)],[c8,c0]) ).
cnf(c176,plain,
( ssPv2(skf2(X111))
| ssPv1(X111)
| ssPv3(X111)
| ssPv3(skf2(X111)) ),
inference(resolution,[status(thm)],[c174,c9]) ).
cnf(c1418,plain,
( ~ ssRr(X497,X498)
| ~ ssPv4(X497)
| ~ ssPv3(skf3(X498))
| ~ ssPv1(X497)
| ssPv2(X498) ),
inference(resolution,[status(thm)],[c1196,clause1]) ).
cnf(c3,plain,
( ~ ssPv4(skf3(X25))
| ssPv1(X25)
| ssPv2(skf3(X25))
| ssPv3(skf3(X25)) ),
inference(resolution,[status(thm)],[clause4,clause1]) ).
cnf(c82,plain,
( ssPv2(skf2(X591))
| ssPv1(X591)
| ssPv2(X591)
| ssPv2(skf3(X591))
| ssPv3(skf3(X591)) ),
inference(resolution,[status(thm)],[c75,c3]) ).
cnf(c2316,plain,
( ssPv2(skf2(X592))
| ssPv1(X592)
| ssPv2(X592)
| ssPv3(skf3(X592))
| ssPv3(X592) ),
inference(resolution,[status(thm)],[c82,c174]) ).
cnf(c2342,plain,
( ssPv1(X598)
| ssPv2(X598)
| ssPv3(skf3(X598))
| ssPv3(X598)
| ~ ssPv1(skf2(X598)) ),
inference(resolution,[status(thm)],[c2316,c269]) ).
cnf(c3200,plain,
( ssPv2(X617)
| ssPv3(X617)
| ssPv3(skf3(X617))
| ssPv1(skf2(X617)) ),
inference(resolution,[status(thm)],[c3066,c2]) ).
cnf(c3275,plain,
( ssPv2(X619)
| ssPv3(X619)
| ssPv3(skf3(X619))
| ssPv1(X619) ),
inference(resolution,[status(thm)],[c3200,c2342]) ).
cnf(c20,plain,
( ssPv3(X301)
| ssPv1(skf3(X301))
| ssPv3(skf3(X301))
| ssPv2(skf3(skf3(X301))) ),
inference(resolution,[status(thm)],[c1,c8]) ).
cnf(c172,plain,
( ~ ssRr(X1097,skf3(X1098))
| ~ ssPv2(X1097)
| ssPv2(X1098)
| ssPv1(skf3(X1098))
| ssPv3(skf3(X1098)) ),
inference(resolution,[status(thm)],[clause17,clause1]) ).
cnf(c14168,plain,
( ~ ssPv2(skf3(skf3(X1515)))
| ssPv2(X1515)
| ssPv1(skf3(X1515))
| ssPv3(skf3(X1515)) ),
inference(resolution,[status(thm)],[c172,clause1]) ).
cnf(c22060,plain,
( ssPv2(X1517)
| ssPv1(skf3(X1517))
| ssPv3(skf3(X1517))
| ssPv3(X1517) ),
inference(resolution,[status(thm)],[c14168,c20]) ).
cnf(c22170,plain,
( ssPv2(X1521)
| ssPv3(skf3(X1521))
| ssPv3(X1521)
| ~ ssPv1(X1521)
| ~ ssPv4(X1521) ),
inference(resolution,[status(thm)],[c22060,c11]) ).
cnf(c22311,plain,
( ssPv2(X1522)
| ssPv3(skf3(X1522))
| ssPv3(X1522)
| ~ ssPv1(X1522) ),
inference(resolution,[status(thm)],[c22170,c3066]) ).
cnf(c22539,plain,
( ssPv2(X1523)
| ssPv3(skf3(X1523))
| ssPv3(X1523) ),
inference(resolution,[status(thm)],[c22311,c3275]) ).
cnf(c22635,plain,
( ssPv2(X1536)
| ssPv3(X1536)
| ~ ssRr(X1537,X1536)
| ~ ssPv4(X1537)
| ~ ssPv1(X1537) ),
inference(resolution,[status(thm)],[c22539,c1418]) ).
cnf(c23010,plain,
( ssPv2(skf2(X1557))
| ssPv3(skf2(X1557))
| ~ ssPv4(X1557)
| ~ ssPv1(X1557) ),
inference(resolution,[status(thm)],[c22635,clause2]) ).
cnf(c23552,plain,
( ssPv2(skf2(X1575))
| ssPv3(skf2(X1575))
| ~ ssPv4(X1575)
| ssPv3(X1575) ),
inference(resolution,[status(thm)],[c23010,c176]) ).
cnf(c23876,plain,
( ssPv2(skf2(X1577))
| ssPv3(skf2(X1577))
| ssPv3(X1577) ),
inference(resolution,[status(thm)],[c23552,c14655]) ).
cnf(c24074,plain,
( ssPv2(skf2(X1590))
| ssPv3(X1590)
| ~ ssPv1(X1590)
| ssPv1(skf2(X1590)) ),
inference(resolution,[status(thm)],[c23876,c337]) ).
cnf(c24194,plain,
( ssPv2(skf2(X1646))
| ssPv3(X1646)
| ssPv1(skf2(X1646))
| ssPv4(skf3(X1646)) ),
inference(resolution,[status(thm)],[c24074,c4548]) ).
cnf(c25610,plain,
( ssPv2(skf2(X1686))
| ssPv1(skf2(X1686))
| ssPv4(skf3(X1686))
| ~ ssPv4(X1686) ),
inference(resolution,[status(thm)],[c24194,c4590]) ).
cnf(clause18,negated_conjecture,
( ~ ssRr(X115,X114)
| ~ ssRr(X114,X113)
| ~ ssPv2(X114)
| ~ ssPv3(X114)
| ssPv4(X115)
| ssPv2(X113) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
cnf(c207,plain,
( ~ ssRr(X117,X118)
| ~ ssPv2(X118)
| ~ ssPv3(X118)
| ssPv4(X117)
| ssPv2(skf2(X118)) ),
inference(resolution,[status(thm)],[clause18,clause2]) ).
cnf(c210,plain,
( ~ ssPv2(X119)
| ~ ssPv3(X119)
| ssPv4(skf3(X119))
| ssPv2(skf2(X119)) ),
inference(resolution,[status(thm)],[c207,clause1]) ).
cnf(c25651,plain,
( ssPv2(skf2(X1647))
| ssPv3(X1647)
| ssPv4(skf3(X1647))
| ssPv4(X1647) ),
inference(resolution,[status(thm)],[c24194,c61]) ).
cnf(c25707,plain,
( ssPv2(skf2(X1650))
| ssPv4(skf3(X1650))
| ssPv4(X1650)
| ~ ssPv2(X1650) ),
inference(resolution,[status(thm)],[c25651,c210]) ).
cnf(c31473,plain,
( ssPv4(skf3(X1967))
| ssPv4(X1967)
| ssPv2(skf2(X1967)) ),
inference(resolution,[status(thm)],[c31432,c25707]) ).
cnf(c31614,plain,
( ssPv4(skf3(X1974))
| ssPv2(skf2(X1974))
| ssPv1(skf2(X1974)) ),
inference(resolution,[status(thm)],[c31473,c25610]) ).
cnf(c31954,plain,
( ssPv4(skf3(X2012))
| ssPv1(skf2(X2012))
| ~ ssPv1(X2012)
| ~ ssPv3(X2012) ),
inference(resolution,[status(thm)],[c31614,c621]) ).
cnf(c32151,plain,
( ssPv4(skf3(X2019))
| ssPv1(skf2(X2019))
| ~ ssPv1(X2019)
| ssPv2(X2019) ),
inference(resolution,[status(thm)],[c31954,c15898]) ).
cnf(c32477,plain,
( ssPv4(skf3(X2020))
| ssPv1(skf2(X2020))
| ssPv2(X2020) ),
inference(resolution,[status(thm)],[c32151,c30442]) ).
cnf(c32545,plain,
( ssPv4(skf3(X2494))
| ssPv2(X2494)
| ~ ssPv2(skf2(X2494))
| ~ ssPv1(X2494)
| ~ ssPv4(X2494) ),
inference(resolution,[status(thm)],[c32477,c677]) ).
cnf(c42562,plain,
( ssPv4(skf3(X2495))
| ssPv2(X2495)
| ~ ssPv1(X2495)
| ~ ssPv4(X2495) ),
inference(resolution,[status(thm)],[c32545,c31559]) ).
cnf(c42716,plain,
( ssPv4(skf3(X2496))
| ssPv2(X2496)
| ~ ssPv1(X2496) ),
inference(resolution,[status(thm)],[c42562,c31432]) ).
cnf(c42833,plain,
( ssPv4(skf3(X2497))
| ssPv2(X2497) ),
inference(resolution,[status(thm)],[c42716,c30442]) ).
cnf(c1420,plain,
( ~ ssPv4(skf3(X500))
| ~ ssPv3(skf3(X500))
| ~ ssPv1(skf3(X500))
| ssPv2(X500) ),
inference(resolution,[status(thm)],[c1416,clause1]) ).
cnf(c520,plain,
( ~ ssPv4(X213)
| ~ ssPv2(X213)
| ssPv1(skf3(X213))
| ssPv2(skf3(X213)) ),
inference(resolution,[status(thm)],[c516,clause1]) ).
cnf(c31279,plain,
( ssPv4(skf3(X2063))
| ssPv2(skf3(X2063))
| ~ ssPv4(X2063)
| ssPv1(skf3(X2063)) ),
inference(resolution,[status(thm)],[c31235,c520]) ).
cnf(c33195,plain,
( ssPv4(skf3(X2064))
| ssPv2(skf3(X2064))
| ssPv1(skf3(X2064)) ),
inference(resolution,[status(thm)],[c31279,c4107]) ).
cnf(c33268,plain,
( ssPv4(skf3(X2065))
| ssPv1(skf3(X2065))
| ssPv2(skf3(skf3(X2065))) ),
inference(resolution,[status(thm)],[c33195,c5]) ).
cnf(c33337,plain,
( ssPv1(skf3(X2066))
| ssPv2(skf3(skf3(X2066)))
| ssPv3(skf3(X2066)) ),
inference(resolution,[status(thm)],[c33268,c8]) ).
cnf(c33466,plain,
( ssPv1(skf3(X2069))
| ssPv3(skf3(X2069))
| ssPv2(X2069) ),
inference(resolution,[status(thm)],[c33337,c14168]) ).
cnf(c33537,plain,
( ssPv3(skf3(X2071))
| ssPv2(X2071)
| ~ ssPv3(X2071)
| ssPv1(X2071) ),
inference(resolution,[status(thm)],[c33466,c338]) ).
cnf(c33596,plain,
( ssPv3(skf3(X2072))
| ssPv2(X2072)
| ssPv1(X2072) ),
inference(resolution,[status(thm)],[c33537,c22539]) ).
cnf(clause33,negated_conjecture,
( ~ ssRr(X258,X257)
| ~ ssPv3(X257)
| ~ ssRr(X258,X256)
| ~ ssPv1(X258)
| ~ ssPv2(X258)
| ssPv1(X256) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
cnf(c647,plain,
( ~ ssRr(X259,X260)
| ~ ssPv3(X260)
| ~ ssPv1(X259)
| ~ ssPv2(X259)
| ssPv1(X260) ),
inference(factor,[status(thm)],[clause33]) ).
cnf(c651,plain,
( ~ ssPv3(X262)
| ~ ssPv1(skf3(X262))
| ~ ssPv2(skf3(X262))
| ssPv1(X262) ),
inference(resolution,[status(thm)],[c647,clause1]) ).
cnf(c22623,plain,
( ssPv2(X1526)
| ssPv3(X1526)
| ~ ssPv4(X1526)
| ssPv2(skf2(X1526)) ),
inference(resolution,[status(thm)],[c22539,c292]) ).
cnf(c14645,plain,
( ssPv2(skf2(X1907))
| ssPv3(skf2(X1907))
| ssPv4(X1907)
| ssPv1(skf2(skf2(X1907))) ),
inference(resolution,[status(thm)],[c13302,c12009]) ).
cnf(clause19,negated_conjecture,
( ~ ssRr(X124,X123)
| ~ ssRr(X124,X122)
| ~ ssPv1(X124)
| ~ ssPv4(X124)
| ssPv4(X123)
| ssPv3(X122) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
cnf(c246,plain,
( ~ ssRr(X126,X125)
| ~ ssPv1(X126)
| ~ ssPv4(X126)
| ssPv4(X125)
| ssPv3(X125) ),
inference(factor,[status(thm)],[clause19]) ).
cnf(c250,plain,
( ~ ssPv1(skf3(X128))
| ~ ssPv4(skf3(X128))
| ssPv4(X128)
| ssPv3(X128) ),
inference(resolution,[status(thm)],[c246,clause1]) ).
cnf(c15709,plain,
( ssPv2(X1179)
| ssPv3(X1179)
| ssPv4(X1179)
| ~ ssPv1(skf3(X1179)) ),
inference(resolution,[status(thm)],[c15601,c250]) ).
cnf(c25,plain,
( ~ ssRr(X59,X60)
| ~ ssPv1(X60)
| ssPv4(X59)
| ssPv1(skf3(X60))
| ssPv4(X60) ),
inference(resolution,[status(thm)],[clause9,clause1]) ).
cnf(c93,plain,
( ~ ssPv1(skf2(X320))
| ssPv4(X320)
| ssPv1(skf3(skf2(X320)))
| ssPv4(skf2(X320)) ),
inference(resolution,[status(thm)],[c25,clause2]) ).
cnf(c11262,plain,
( ssPv4(X1040)
| ssPv1(skf2(X1040))
| ssPv4(skf2(X1040))
| ssPv2(skf2(X1040)) ),
inference(resolution,[status(thm)],[c10288,c8185]) ).
cnf(c12552,plain,
( ssPv4(X1483)
| ssPv4(skf2(X1483))
| ssPv2(skf2(X1483))
| ssPv1(skf3(skf2(X1483))) ),
inference(resolution,[status(thm)],[c11262,c93]) ).
cnf(c20971,plain,
( ssPv4(X1484)
| ssPv4(skf2(X1484))
| ssPv2(skf2(X1484))
| ssPv3(skf2(X1484)) ),
inference(resolution,[status(thm)],[c12552,c15709]) ).
cnf(c22795,plain,
( ssPv2(skf2(X2917))
| ssPv3(skf2(X2917))
| ssPv2(skf2(skf2(X2917)))
| ssPv4(X2917) ),
inference(resolution,[status(thm)],[c22623,c20971]) ).
cnf(c48214,plain,
( ssPv2(skf2(X3600))
| ssPv3(skf2(X3600))
| ssPv4(X3600)
| ~ ssPv1(skf2(skf2(X3600))) ),
inference(resolution,[status(thm)],[c22795,c269]) ).
cnf(c64177,plain,
( ssPv2(skf2(X3601))
| ssPv3(skf2(X3601))
| ssPv4(X3601) ),
inference(resolution,[status(thm)],[c48214,c14645]) ).
cnf(clause24,negated_conjecture,
( ~ ssRr(X171,X170)
| ~ ssRr(X170,X169)
| ~ ssPv2(X169)
| ~ ssPv3(X170)
| ssPv2(X171)
| ssPv2(X170) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
cnf(c368,plain,
( ~ ssRr(X175,X176)
| ~ ssPv2(skf2(X176))
| ~ ssPv3(X176)
| ssPv2(X175)
| ssPv2(X176) ),
inference(resolution,[status(thm)],[clause24,clause2]) ).
cnf(c830,plain,
( ssPv4(X313)
| ssPv2(skf2(skf2(X313)))
| ssPv2(skf2(X313))
| ssPv3(X313) ),
inference(resolution,[status(thm)],[c74,c61]) ).
cnf(c867,plain,
( ssPv4(X4730)
| ssPv2(skf2(X4730))
| ssPv3(X4730)
| ~ ssRr(X4731,skf2(X4730))
| ~ ssPv3(skf2(X4730))
| ssPv2(X4731) ),
inference(resolution,[status(thm)],[c830,c368]) ).
cnf(c101746,plain,
( ssPv4(X4732)
| ssPv2(skf2(X4732))
| ssPv3(X4732)
| ~ ssPv3(skf2(X4732))
| ssPv2(X4732) ),
inference(resolution,[status(thm)],[c867,clause2]) ).
cnf(c101755,plain,
( ssPv4(X4733)
| ssPv2(skf2(X4733))
| ssPv3(X4733)
| ssPv2(X4733) ),
inference(resolution,[status(thm)],[c101746,c64177]) ).
cnf(c101915,plain,
( ssPv2(skf2(X4734))
| ssPv3(X4734)
| ssPv2(X4734) ),
inference(resolution,[status(thm)],[c101755,c22623]) ).
cnf(c102070,plain,
( ssPv3(X4735)
| ssPv2(X4735)
| ~ ssPv1(skf2(X4735)) ),
inference(resolution,[status(thm)],[c101915,c269]) ).
cnf(c12570,plain,
( ssPv4(X1042)
| ssPv4(skf2(X1042))
| ssPv2(skf2(X1042))
| ssPv3(X1042) ),
inference(resolution,[status(thm)],[c11262,c61]) ).
cnf(c13221,plain,
( ssPv4(skf2(X1065))
| ssPv2(X1065)
| ssPv3(X1065)
| ssPv4(X1065) ),
inference(resolution,[status(thm)],[c13214,c12570]) ).
cnf(c22672,plain,
( ssPv2(X1539)
| ssPv3(X1539)
| ssPv2(skf2(X1539))
| ssPv4(skf2(X1539)) ),
inference(resolution,[status(thm)],[c22623,c13221]) ).
cnf(c23076,plain,
( ssPv2(X1540)
| ssPv3(X1540)
| ssPv4(skf2(X1540)) ),
inference(resolution,[status(thm)],[c22672,c13214]) ).
cnf(c102090,plain,
( ssPv3(X4750)
| ssPv2(X4750)
| ~ ssPv4(skf2(X4750))
| ssPv1(X4750) ),
inference(resolution,[status(thm)],[c101915,c519]) ).
cnf(c102553,plain,
( ssPv3(X4751)
| ssPv2(X4751)
| ssPv1(X4751) ),
inference(resolution,[status(thm)],[c102090,c23076]) ).
cnf(c102720,plain,
( ssPv3(X4752)
| ssPv2(X4752)
| ssPv1(skf2(X4752)) ),
inference(resolution,[status(thm)],[c102553,c12009]) ).
cnf(c102934,plain,
( ssPv3(X4753)
| ssPv2(X4753) ),
inference(resolution,[status(thm)],[c102720,c102070]) ).
cnf(c103068,plain,
( ssPv3(skf2(X5070))
| ~ ssRr(X5071,X5070)
| ~ ssPv3(X5070)
| ssPv2(X5071)
| ssPv2(X5070) ),
inference(resolution,[status(thm)],[c102934,c368]) ).
cnf(c106996,plain,
( ssPv3(skf2(X5072))
| ~ ssPv3(X5072)
| ssPv2(skf3(X5072))
| ssPv2(X5072) ),
inference(resolution,[status(thm)],[c103068,clause1]) ).
cnf(c107070,plain,
( ssPv3(skf2(X5073))
| ssPv2(skf3(X5073))
| ssPv2(X5073) ),
inference(resolution,[status(thm)],[c106996,c102934]) ).
cnf(c622,plain,
( ~ ssPv2(X252)
| ~ ssPv1(skf3(X252))
| ~ ssPv3(skf3(X252))
| ssPv1(X252) ),
inference(resolution,[status(thm)],[c618,clause1]) ).
cnf(c4076,plain,
( ssPv1(X652)
| ssPv4(X652)
| ssPv2(skf3(X652))
| ssPv3(skf3(X652)) ),
inference(resolution,[status(thm)],[c3805,c3]) ).
cnf(c4211,plain,
( ssPv1(X654)
| ssPv2(skf3(X654))
| ssPv3(skf3(X654))
| ssPv3(X654) ),
inference(resolution,[status(thm)],[c4076,c8]) ).
cnf(c270,plain,
( ~ ssPv1(X138)
| ~ ssPv2(X138)
| ssPv3(skf3(X138))
| ssPv2(skf3(X138)) ),
inference(resolution,[status(thm)],[c266,clause1]) ).
cnf(c22612,plain,
( ssPv3(skf3(X1533))
| ssPv3(X1533)
| ~ ssPv1(X1533)
| ssPv2(skf3(X1533)) ),
inference(resolution,[status(thm)],[c22539,c270]) ).
cnf(c22846,plain,
( ssPv3(skf3(X1534))
| ssPv3(X1534)
| ssPv2(skf3(X1534)) ),
inference(resolution,[status(thm)],[c22612,c4211]) ).
cnf(c33235,plain,
( ssPv2(skf3(X2202))
| ssPv1(skf3(X2202))
| ssPv1(X2202)
| ssPv3(skf3(X2202)) ),
inference(resolution,[status(thm)],[c33195,c3]) ).
cnf(c36016,plain,
( ssPv2(skf3(X2205))
| ssPv1(X2205)
| ssPv3(skf3(X2205))
| ~ ssPv3(X2205) ),
inference(resolution,[status(thm)],[c33235,c338]) ).
cnf(c36245,plain,
( ssPv2(skf3(X2206))
| ssPv1(X2206)
| ssPv3(skf3(X2206)) ),
inference(resolution,[status(thm)],[c36016,c22846]) ).
cnf(c36391,plain,
( ssPv2(skf3(X2215))
| ssPv1(X2215)
| ~ ssPv2(X2215)
| ~ ssPv1(skf3(X2215)) ),
inference(resolution,[status(thm)],[c36245,c622]) ).
cnf(c23186,plain,
( ssPv2(X1571)
| ssPv3(X1571)
| ~ ssRr(X1570,X1571)
| ~ ssPv1(X1571)
| ssPv2(X1570) ),
inference(resolution,[status(thm)],[c23076,c447]) ).
cnf(c23710,plain,
( ssPv2(skf2(X1625))
| ssPv3(skf2(X1625))
| ~ ssPv1(skf2(X1625))
| ssPv2(X1625) ),
inference(resolution,[status(thm)],[c23186,clause2]) ).
cnf(c24991,plain,
( ssPv2(skf2(X1626))
| ssPv3(skf2(X1626))
| ssPv2(X1626)
| ssPv4(X1626) ),
inference(resolution,[status(thm)],[c23710,c13302]) ).
cnf(c25064,plain,
( ssPv3(skf2(X1804))
| ssPv2(X1804)
| ssPv4(X1804)
| ~ ssPv4(skf2(X1804))
| ssPv1(X1804) ),
inference(resolution,[status(thm)],[c24991,c519]) ).
cnf(c28704,plain,
( ssPv3(skf2(X1805))
| ssPv2(X1805)
| ssPv4(X1805)
| ssPv1(X1805) ),
inference(resolution,[status(thm)],[c25064,c11352]) ).
cnf(c28810,plain,
( ssPv3(skf2(X1809))
| ssPv4(X1809)
| ssPv1(X1809)
| ssPv2(skf3(X1809)) ),
inference(resolution,[status(thm)],[c28704,c5]) ).
cnf(c107218,plain,
( ssPv3(skf2(X5183))
| ssPv2(skf3(X5183))
| ~ ssPv4(X5183)
| ssPv1(skf3(X5183)) ),
inference(resolution,[status(thm)],[c107070,c520]) ).
cnf(c109614,plain,
( ssPv3(skf2(X5203))
| ssPv2(skf3(X5203))
| ssPv1(skf3(X5203))
| ssPv1(X5203) ),
inference(resolution,[status(thm)],[c107218,c28810]) ).
cnf(c110032,plain,
( ssPv3(skf2(X5204))
| ssPv2(skf3(X5204))
| ssPv1(X5204)
| ~ ssPv2(X5204) ),
inference(resolution,[status(thm)],[c109614,c36391]) ).
cnf(c110212,plain,
( ssPv3(skf2(X5205))
| ssPv2(skf3(X5205))
| ssPv1(X5205) ),
inference(resolution,[status(thm)],[c110032,c107070]) ).
cnf(c110388,plain,
( ssPv3(skf2(X5212))
| ssPv1(X5212)
| ~ ssPv3(X5212)
| ~ ssPv1(skf3(X5212)) ),
inference(resolution,[status(thm)],[c110212,c651]) ).
cnf(clause27,negated_conjecture,
( ~ ssRr(X200,X199)
| ~ ssRr(X199,X198)
| ~ ssPv4(X198)
| ~ ssPv2(X199)
| ssPv1(X200)
| ssPv1(X199) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
cnf(c474,plain,
( ~ ssRr(X202,X203)
| ~ ssPv4(skf2(X203))
| ~ ssPv2(X203)
| ssPv1(X202)
| ssPv1(X203) ),
inference(resolution,[status(thm)],[clause27,clause2]) ).
cnf(c135,plain,
( ~ ssPv3(X88)
| ssPv4(X88)
| ssPv1(skf2(X88))
| ssPv4(skf2(X88)) ),
inference(resolution,[status(thm)],[c132,clause2]) ).
cnf(c139,plain,
( ssPv4(X907)
| ssPv1(skf2(X907))
| ssPv4(skf2(X907))
| ssPv3(skf2(X907))
| ssPv1(X907) ),
inference(resolution,[status(thm)],[c135,c0]) ).
cnf(c9073,plain,
( ssPv4(X908)
| ssPv4(skf2(X908))
| ssPv3(skf2(X908))
| ssPv1(X908) ),
inference(resolution,[status(thm)],[c139,c26]) ).
cnf(c9189,plain,
( ssPv4(X6224)
| ssPv3(skf2(X6224))
| ssPv1(X6224)
| ~ ssRr(X6223,X6224)
| ~ ssPv2(X6224)
| ssPv1(X6223) ),
inference(resolution,[status(thm)],[c9073,c474]) ).
cnf(c139943,plain,
( ssPv4(X6226)
| ssPv3(skf2(X6226))
| ssPv1(X6226)
| ~ ssPv2(X6226)
| ssPv1(skf3(X6226)) ),
inference(resolution,[status(thm)],[c9189,clause1]) ).
cnf(c140224,plain,
( ssPv4(X6227)
| ssPv3(skf2(X6227))
| ssPv1(X6227)
| ssPv1(skf3(X6227)) ),
inference(resolution,[status(thm)],[c139943,c28704]) ).
cnf(c140658,plain,
( ssPv4(X6228)
| ssPv3(skf2(X6228))
| ssPv1(X6228)
| ~ ssPv3(X6228) ),
inference(resolution,[status(thm)],[c140224,c110388]) ).
cnf(c140751,plain,
( ssPv4(X6229)
| ssPv3(skf2(X6229))
| ssPv1(X6229) ),
inference(resolution,[status(thm)],[c140658,c0]) ).
cnf(clause48,negated_conjecture,
( ~ ssRr(X410,X408)
| ~ ssPv4(X410)
| ~ ssRr(X407,X408)
| ~ ssPv2(X407)
| ~ ssRr(X408,X409)
| ~ ssPv4(X408)
| ssPv3(X409) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
cnf(c1231,plain,
( ~ ssRr(X6711,X6710)
| ~ ssPv4(X6711)
| ~ ssRr(X6709,X6710)
| ~ ssPv2(X6709)
| ~ ssPv4(X6710)
| ssPv3(skf2(X6710)) ),
inference(resolution,[status(thm)],[clause48,clause2]) ).
cnf(c151657,plain,
( ~ ssRr(X6712,X6713)
| ~ ssPv4(X6712)
| ~ ssPv2(X6712)
| ~ ssPv4(X6713)
| ssPv3(skf2(X6713)) ),
inference(factor,[status(thm)],[c1231]) ).
cnf(c151661,plain,
( ~ ssPv4(skf3(X6715))
| ~ ssPv2(skf3(X6715))
| ~ ssPv4(X6715)
| ssPv3(skf2(X6715)) ),
inference(resolution,[status(thm)],[c151657,clause1]) ).
cnf(c151869,plain,
( ~ ssPv4(skf3(X6716))
| ~ ssPv4(X6716)
| ssPv3(skf2(X6716))
| ssPv1(X6716) ),
inference(resolution,[status(thm)],[c151661,c110212]) ).
cnf(c152096,plain,
( ~ ssPv4(X6717)
| ssPv3(skf2(X6717))
| ssPv1(X6717)
| ssPv2(X6717) ),
inference(resolution,[status(thm)],[c151869,c42833]) ).
cnf(c152264,plain,
( ssPv3(skf2(X6721))
| ssPv1(X6721)
| ssPv2(X6721) ),
inference(resolution,[status(thm)],[c152096,c140751]) ).
cnf(clause50,negated_conjecture,
( ~ ssRr(X430,X428)
| ~ ssPv4(X430)
| ~ ssRr(X427,X428)
| ~ ssPv3(X427)
| ~ ssRr(X428,X429)
| ~ ssPv3(X429)
| ssPv1(X428) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
cnf(c1250,plain,
( ~ ssRr(X6779,X6780)
| ~ ssPv4(X6779)
| ~ ssRr(X6778,X6780)
| ~ ssPv3(X6778)
| ~ ssPv3(skf2(X6780))
| ssPv1(X6780) ),
inference(resolution,[status(thm)],[clause50,clause2]) ).
cnf(c154736,plain,
( ~ ssRr(X7425,X7423)
| ~ ssPv4(X7425)
| ~ ssRr(X7424,X7423)
| ~ ssPv3(X7424)
| ssPv1(X7423)
| ssPv2(X7423) ),
inference(resolution,[status(thm)],[c1250,c152264]) ).
cnf(c171410,plain,
( ~ ssRr(X7427,X7426)
| ~ ssPv4(X7427)
| ~ ssPv3(X7427)
| ssPv1(X7426)
| ssPv2(X7426) ),
inference(factor,[status(thm)],[c154736]) ).
cnf(c171414,plain,
( ~ ssPv4(skf3(X7488))
| ~ ssPv3(skf3(X7488))
| ssPv1(X7488)
| ssPv2(X7488) ),
inference(resolution,[status(thm)],[c171410,clause1]) ).
cnf(c174036,plain,
( ~ ssPv4(skf3(X7489))
| ssPv1(X7489)
| ssPv2(X7489) ),
inference(resolution,[status(thm)],[c171414,c33596]) ).
cnf(c174230,plain,
( ssPv1(X7491)
| ssPv2(X7491) ),
inference(resolution,[status(thm)],[c174036,c42833]) ).
cnf(c8117,plain,
( ssPv4(X874)
| ssPv1(skf3(X874))
| ssPv2(X874)
| ~ ssPv1(X874)
| ~ ssPv2(skf3(X874)) ),
inference(resolution,[status(thm)],[c8051,c568]) ).
cnf(c174351,plain,
( ssPv1(skf3(X7591))
| ssPv4(X7591)
| ssPv2(X7591)
| ~ ssPv1(X7591) ),
inference(resolution,[status(thm)],[c174230,c8117]) ).
cnf(c177222,plain,
( ssPv1(skf3(X7592))
| ssPv4(X7592)
| ssPv2(X7592) ),
inference(resolution,[status(thm)],[c174351,c174230]) ).
cnf(c1197,plain,
( ~ ssRr(X505,X503)
| ~ ssPv4(X505)
| ~ ssRr(X504,X503)
| ~ ssPv3(X504)
| ~ ssPv1(X504)
| ssPv2(X503) ),
inference(factor,[status(thm)],[clause46]) ).
cnf(c1512,plain,
( ~ ssRr(X567,skf2(X568))
| ~ ssPv4(X567)
| ~ ssPv3(X568)
| ~ ssPv1(X568)
| ssPv2(skf2(X568)) ),
inference(resolution,[status(thm)],[c1197,clause2]) ).
cnf(c2040,plain,
( ~ ssPv4(skf3(skf2(X571)))
| ~ ssPv3(X571)
| ~ ssPv1(X571)
| ssPv2(skf2(X571)) ),
inference(resolution,[status(thm)],[c1512,clause1]) ).
cnf(c42874,plain,
( ssPv2(skf2(X2498))
| ~ ssPv3(X2498)
| ~ ssPv1(X2498) ),
inference(resolution,[status(thm)],[c42833,c2040]) ).
cnf(c174253,plain,
( ssPv2(X7498)
| ssPv2(skf2(X7498))
| ~ ssPv3(X7498) ),
inference(resolution,[status(thm)],[c174230,c42874]) ).
cnf(c174701,plain,
( ssPv2(X7499)
| ssPv2(skf2(X7499)) ),
inference(resolution,[status(thm)],[c174253,c102934]) ).
cnf(c102698,plain,
( ssPv3(X4772)
| ssPv1(X4772)
| ssPv2(skf3(X4772))
| ssPv4(X4772) ),
inference(resolution,[status(thm)],[c102553,c5]) ).
cnf(c103321,plain,
( ssPv3(X4773)
| ssPv1(X4773)
| ssPv2(skf3(X4773)) ),
inference(resolution,[status(thm)],[c102698,c8]) ).
cnf(c103488,plain,
( ssPv3(X4775)
| ssPv1(X4775)
| ssPv2(skf2(X4775)) ),
inference(resolution,[status(thm)],[c103321,c174]) ).
cnf(c103654,plain,
( ssPv3(X4779)
| ssPv2(skf2(X4779))
| ssPv1(skf2(X4779)) ),
inference(resolution,[status(thm)],[c103488,c24074]) ).
cnf(c171413,plain,
( ~ ssPv4(X7428)
| ~ ssPv3(X7428)
| ssPv1(skf2(X7428))
| ssPv2(skf2(X7428)) ),
inference(resolution,[status(thm)],[c171410,clause2]) ).
cnf(c171542,plain,
( ~ ssPv4(X7430)
| ssPv1(skf2(X7430))
| ssPv2(skf2(X7430)) ),
inference(resolution,[status(thm)],[c171413,c103654]) ).
cnf(c12562,plain,
( ssPv4(X1041)
| ssPv4(skf2(X1041))
| ssPv2(skf2(X1041))
| ssPv1(X1041) ),
inference(resolution,[status(thm)],[c11262,c26]) ).
cnf(c31510,plain,
( ssPv2(skf2(X1995))
| ssPv4(skf2(X1995))
| ~ ssPv3(X1995)
| ~ ssPv1(X1995) ),
inference(resolution,[status(thm)],[c31432,c2040]) ).
cnf(c32061,plain,
( ssPv2(skf2(X2014))
| ssPv4(skf2(X2014))
| ~ ssPv3(X2014)
| ssPv4(X2014) ),
inference(resolution,[status(thm)],[c31510,c12562]) ).
cnf(c32260,plain,
( ssPv2(skf2(X2015))
| ssPv4(skf2(X2015))
| ssPv4(X2015) ),
inference(resolution,[status(thm)],[c32061,c12570]) ).
cnf(c171688,plain,
( ssPv1(skf2(X7432))
| ssPv2(skf2(X7432))
| ssPv4(skf2(X7432)) ),
inference(resolution,[status(thm)],[c171542,c32260]) ).
cnf(c171861,plain,
( ssPv1(skf2(X7433))
| ssPv4(skf2(X7433))
| ssPv2(X7433) ),
inference(resolution,[status(thm)],[c171688,c4]) ).
cnf(c171934,plain,
( ssPv4(skf2(X7442))
| ssPv2(X7442)
| ~ ssRr(X7443,X7442)
| ssPv4(X7443) ),
inference(resolution,[status(thm)],[c171861,c1301]) ).
cnf(c172421,plain,
( ssPv4(skf2(skf2(X7446)))
| ssPv2(skf2(X7446))
| ssPv4(X7446) ),
inference(resolution,[status(thm)],[c171934,clause2]) ).
cnf(c172453,plain,
( ssPv2(skf2(X7447))
| ssPv4(X7447)
| ssPv1(skf2(X7447)) ),
inference(resolution,[status(thm)],[c172421,c821]) ).
cnf(c172560,plain,
( ssPv2(skf2(X7449))
| ssPv1(skf2(X7449)) ),
inference(resolution,[status(thm)],[c172453,c171542]) ).
cnf(c172667,plain,
( ssPv1(skf2(X7451))
| ~ ssPv1(X7451)
| ~ ssPv3(X7451) ),
inference(resolution,[status(thm)],[c172560,c621]) ).
cnf(c173054,plain,
( ssPv1(skf2(X7455))
| ~ ssPv1(X7455)
| ssPv2(X7455) ),
inference(resolution,[status(thm)],[c172667,c102934]) ).
cnf(c174241,plain,
( ssPv2(X7492)
| ssPv1(skf2(X7492)) ),
inference(resolution,[status(thm)],[c174230,c173054]) ).
cnf(c174408,plain,
( ssPv2(X7601)
| ~ ssPv2(skf2(X7601))
| ~ ssPv1(X7601)
| ~ ssPv4(X7601) ),
inference(resolution,[status(thm)],[c174241,c677]) ).
cnf(c177483,plain,
( ssPv2(X7602)
| ~ ssPv1(X7602)
| ~ ssPv4(X7602) ),
inference(resolution,[status(thm)],[c174408,c174701]) ).
cnf(c177604,plain,
( ssPv2(X7603)
| ~ ssPv1(X7603)
| ssPv1(skf3(X7603)) ),
inference(resolution,[status(thm)],[c177483,c177222]) ).
cnf(c177642,plain,
( ssPv2(X7604)
| ssPv1(skf3(X7604)) ),
inference(resolution,[status(thm)],[c177604,c174230]) ).
cnf(c177732,plain,
( ssPv2(X7644)
| ~ ssPv4(skf3(X7644))
| ~ ssPv3(skf3(X7644)) ),
inference(resolution,[status(thm)],[c177642,c1420]) ).
cnf(clause31,negated_conjecture,
( ~ ssRr(X239,X238)
| ~ ssRr(X238,X237)
| ~ ssPv1(X237)
| ~ ssPv1(X238)
| ~ ssPv3(X238)
| ssPv3(X239) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
cnf(c592,plain,
( ~ ssRr(X241,X242)
| ~ ssPv1(skf2(X242))
| ~ ssPv1(X242)
| ~ ssPv3(X242)
| ssPv3(X241) ),
inference(resolution,[status(thm)],[clause31,clause2]) ).
cnf(c174395,plain,
( ssPv2(X7929)
| ~ ssRr(X7928,X7929)
| ~ ssPv1(X7929)
| ~ ssPv3(X7929)
| ssPv3(X7928) ),
inference(resolution,[status(thm)],[c174241,c592]) ).
cnf(c179303,plain,
( ssPv2(X7931)
| ~ ssPv1(X7931)
| ~ ssPv3(X7931)
| ssPv3(skf3(X7931)) ),
inference(resolution,[status(thm)],[c174395,clause1]) ).
cnf(c179326,plain,
( ssPv2(X7932)
| ~ ssPv1(X7932)
| ssPv3(skf3(X7932)) ),
inference(resolution,[status(thm)],[c179303,c102934]) ).
cnf(c179354,plain,
( ssPv2(X7933)
| ssPv3(skf3(X7933)) ),
inference(resolution,[status(thm)],[c179326,c174230]) ).
cnf(c179413,plain,
( ssPv2(X7934)
| ~ ssPv4(skf3(X7934)) ),
inference(resolution,[status(thm)],[c179354,c177732]) ).
cnf(c179452,plain,
ssPv2(X7935),
inference(resolution,[status(thm)],[c179413,c42833]) ).
cnf(c36500,plain,
( ssPv2(skf3(X2341))
| ssPv1(X2341)
| ~ ssPv2(X2341)
| ssPv3(skf3(skf3(X2341))) ),
inference(resolution,[status(thm)],[c36391,c33596]) ).
cnf(c33538,plain,
( ssPv3(skf3(X2073))
| ssPv2(X2073)
| ~ ssPv1(X2073)
| ~ ssPv4(X2073) ),
inference(resolution,[status(thm)],[c33466,c11]) ).
cnf(c33872,plain,
( ssPv3(skf3(skf3(X3132)))
| ssPv2(skf3(X3132))
| ~ ssPv1(skf3(X3132))
| ssPv2(X3132) ),
inference(resolution,[status(thm)],[c33538,c31235]) ).
cnf(c51213,plain,
( ssPv3(skf3(skf3(X3133)))
| ssPv2(skf3(X3133))
| ssPv2(X3133) ),
inference(resolution,[status(thm)],[c33872,c33596]) ).
cnf(c51292,plain,
( ssPv3(skf3(skf3(X3134)))
| ssPv2(skf3(X3134))
| ssPv1(X3134) ),
inference(resolution,[status(thm)],[c51213,c36500]) ).
cnf(c593,plain,
( ~ ssRr(X3173,skf3(X3174))
| ~ ssPv1(X3174)
| ~ ssPv1(skf3(X3174))
| ~ ssPv3(skf3(X3174))
| ssPv3(X3173) ),
inference(resolution,[status(thm)],[clause31,clause1]) ).
cnf(c53952,plain,
( ~ ssPv1(X3859)
| ~ ssPv1(skf3(X3859))
| ~ ssPv3(skf3(X3859))
| ssPv3(skf3(skf3(X3859))) ),
inference(resolution,[status(thm)],[c593,clause1]) ).
cnf(c70690,plain,
( ~ ssPv1(X4178)
| ~ ssPv1(skf3(X4178))
| ssPv3(skf3(skf3(X4178)))
| ssPv2(skf3(X4178)) ),
inference(resolution,[status(thm)],[c53952,c22539]) ).
cnf(c84248,plain,
( ~ ssPv1(X4179)
| ssPv3(skf3(skf3(X4179)))
| ssPv2(skf3(X4179)) ),
inference(resolution,[status(thm)],[c70690,c33596]) ).
cnf(c84318,plain,
( ssPv3(skf3(skf3(X4180)))
| ssPv2(skf3(X4180)) ),
inference(resolution,[status(thm)],[c84248,c51292]) ).
cnf(c84443,plain,
( ssPv2(skf3(X4185))
| ~ ssRr(X4186,skf3(X4185))
| ~ ssPv4(X4186)
| ~ ssPv1(X4186) ),
inference(resolution,[status(thm)],[c84318,c1418]) ).
cnf(c84501,plain,
( ssPv2(skf3(X4201))
| ~ ssPv4(skf3(skf3(X4201)))
| ~ ssPv1(skf3(skf3(X4201))) ),
inference(resolution,[status(thm)],[c84443,clause1]) ).
cnf(c177753,plain,
( ssPv2(skf3(X7611))
| ~ ssPv4(skf3(skf3(X7611))) ),
inference(resolution,[status(thm)],[c177642,c84501]) ).
cnf(c177843,plain,
ssPv2(skf3(X7613)),
inference(resolution,[status(thm)],[c177753,c42833]) ).
cnf(clause45,negated_conjecture,
( ~ ssRr(X376,X374)
| ~ ssPv2(X376)
| ~ ssRr(X374,X373)
| ~ ssPv3(X373)
| ~ ssRr(X374,X375)
| ~ ssPv2(X374)
| ssPv1(X375) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
cnf(c1171,plain,
( ~ ssRr(X486,X487)
| ~ ssPv2(X486)
| ~ ssRr(X487,X485)
| ~ ssPv3(X485)
| ~ ssPv2(X487)
| ssPv1(X485) ),
inference(factor,[status(thm)],[clause45]) ).
cnf(c1338,plain,
( ~ ssRr(X560,skf3(X561))
| ~ ssPv2(X560)
| ~ ssPv3(X561)
| ~ ssPv2(skf3(X561))
| ssPv1(X561) ),
inference(resolution,[status(thm)],[c1171,clause1]) ).
cnf(c1937,plain,
( ~ ssPv2(skf3(skf3(X563)))
| ~ ssPv3(X563)
| ~ ssPv2(skf3(X563))
| ssPv1(X563) ),
inference(resolution,[status(thm)],[c1338,clause1]) ).
cnf(c177857,plain,
( ~ ssPv3(X7615)
| ~ ssPv2(skf3(X7615))
| ssPv1(X7615) ),
inference(resolution,[status(thm)],[c177843,c1937]) ).
cnf(c177876,plain,
( ~ ssPv3(X7616)
| ssPv1(X7616) ),
inference(resolution,[status(thm)],[c177857,c177843]) ).
cnf(clause41,negated_conjecture,
( ~ ssRr(X336,X334)
| ~ ssPv1(X336)
| ~ ssRr(X334,X333)
| ~ ssRr(X334,X335)
| ~ ssPv1(X334)
| ssPv3(X333)
| ssPv1(X335) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
cnf(c1036,plain,
( ~ ssRr(X463,X464)
| ~ ssPv1(X463)
| ~ ssRr(X464,X462)
| ~ ssPv1(X464)
| ssPv3(X462)
| ssPv1(X462) ),
inference(factor,[status(thm)],[clause41]) ).
cnf(c1322,plain,
( ~ ssRr(X550,skf3(X551))
| ~ ssPv1(X550)
| ~ ssPv1(skf3(X551))
| ssPv3(X551)
| ssPv1(X551) ),
inference(resolution,[status(thm)],[c1036,clause1]) ).
cnf(c1736,plain,
( ~ ssPv1(skf3(skf3(X552)))
| ~ ssPv1(skf3(X552))
| ssPv3(X552)
| ssPv1(X552) ),
inference(resolution,[status(thm)],[c1322,clause1]) ).
cnf(clause14,negated_conjecture,
( ~ ssRr(X76,X75)
| ~ ssRr(X75,X74)
| ~ ssPv2(X75)
| ssPv1(X76)
| ssPv4(X74)
| ssPv1(X75) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
cnf(c106,plain,
( ~ ssRr(X836,skf3(X835))
| ~ ssPv2(skf3(X835))
| ssPv1(X836)
| ssPv4(X835)
| ssPv1(skf3(X835)) ),
inference(resolution,[status(thm)],[clause14,clause1]) ).
cnf(c7038,plain,
( ~ ssPv2(skf3(X852))
| ssPv1(skf3(skf3(X852)))
| ssPv4(X852)
| ssPv1(skf3(X852)) ),
inference(resolution,[status(thm)],[c106,clause1]) ).
cnf(clause12,negated_conjecture,
( ~ ssRr(X56,X55)
| ~ ssPv2(X56)
| ~ ssRr(X55,X54)
| ssPv2(X54)
| ssPv2(X55)
| ssPv3(X55) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(c78,plain,
( ~ ssRr(X755,skf3(X756))
| ~ ssPv2(X755)
| ssPv2(X756)
| ssPv2(skf3(X756))
| ssPv3(skf3(X756)) ),
inference(resolution,[status(thm)],[clause12,clause1]) ).
cnf(c5815,plain,
( ~ ssPv2(skf3(skf3(X846)))
| ssPv2(X846)
| ssPv2(skf3(X846))
| ssPv3(skf3(X846)) ),
inference(resolution,[status(thm)],[c78,clause1]) ).
cnf(c23711,plain,
( ssPv2(X1572)
| ssPv3(X1572)
| ~ ssPv1(X1572)
| ssPv2(skf3(X1572)) ),
inference(resolution,[status(thm)],[c23186,clause1]) ).
cnf(c33449,plain,
( ssPv2(skf3(skf3(X2104)))
| ssPv3(skf3(X2104))
| ssPv2(skf3(X2104)) ),
inference(resolution,[status(thm)],[c33337,c23711]) ).
cnf(c34318,plain,
( ssPv3(skf3(X2105))
| ssPv2(skf3(X2105))
| ssPv2(X2105) ),
inference(resolution,[status(thm)],[c33449,c5815]) ).
cnf(c34431,plain,
( ssPv3(skf3(X2106))
| ssPv2(skf3(X2106))
| ~ ssPv1(X2106) ),
inference(resolution,[status(thm)],[c34318,c270]) ).
cnf(c34489,plain,
( ssPv3(skf3(X2107))
| ssPv2(skf3(X2107))
| ssPv4(X2107) ),
inference(resolution,[status(thm)],[c34431,c4076]) ).
cnf(c34555,plain,
( ssPv3(skf3(X3213))
| ssPv4(X3213)
| ssPv1(skf3(skf3(X3213)))
| ssPv1(skf3(X3213)) ),
inference(resolution,[status(thm)],[c34489,c7038]) ).
cnf(c36382,plain,
( ssPv2(skf3(X2207))
| ssPv3(skf3(X2207)) ),
inference(resolution,[status(thm)],[c36245,c34431]) ).
cnf(c475,plain,
( ~ ssRr(X2576,skf3(X2577))
| ~ ssPv4(X2577)
| ~ ssPv2(skf3(X2577))
| ssPv1(X2576)
| ssPv1(skf3(X2577)) ),
inference(resolution,[status(thm)],[clause27,clause1]) ).
cnf(c44118,plain,
( ~ ssPv4(X3466)
| ~ ssPv2(skf3(X3466))
| ssPv1(skf3(skf3(X3466)))
| ssPv1(skf3(X3466)) ),
inference(resolution,[status(thm)],[c475,clause1]) ).
cnf(c59265,plain,
( ~ ssPv4(X3936)
| ssPv1(skf3(skf3(X3936)))
| ssPv1(skf3(X3936))
| ssPv3(skf3(X3936)) ),
inference(resolution,[status(thm)],[c44118,c36382]) ).
cnf(c75423,plain,
( ssPv1(skf3(skf3(X3937)))
| ssPv1(skf3(X3937))
| ssPv3(skf3(X3937)) ),
inference(resolution,[status(thm)],[c59265,c34555]) ).
cnf(c177906,plain,
( ssPv1(skf3(X7632))
| ssPv1(skf3(skf3(X7632))) ),
inference(resolution,[status(thm)],[c177876,c75423]) ).
cnf(c620,plain,
( ~ ssRr(skf3(X3335),X3334)
| ~ ssPv2(X3334)
| ~ ssPv1(skf3(X3335))
| ~ ssPv3(skf3(X3335))
| ssPv1(X3335) ),
inference(resolution,[status(thm)],[clause32,clause1]) ).
cnf(c56217,plain,
( ~ ssPv2(skf2(skf3(X3900)))
| ~ ssPv1(skf3(X3900))
| ~ ssPv3(skf3(X3900))
| ssPv1(X3900) ),
inference(resolution,[status(thm)],[c620,clause2]) ).
cnf(c33454,plain,
( ssPv1(skf3(X2122))
| ssPv3(skf3(X2122))
| ssPv2(skf2(skf3(X2122))) ),
inference(resolution,[status(thm)],[c33337,c174]) ).
cnf(c336,plain,
( ~ ssRr(skf3(X1869),X1868)
| ~ ssPv3(X1868)
| ~ ssPv1(skf3(X1869))
| ssPv1(X1869)
| ssPv3(skf3(X1869)) ),
inference(resolution,[status(thm)],[clause22,clause1]) ).
cnf(c29491,plain,
( ~ ssPv3(skf2(skf3(X3013)))
| ~ ssPv1(skf3(X3013))
| ssPv1(X3013)
| ssPv3(skf3(X3013)) ),
inference(resolution,[status(thm)],[c336,clause2]) ).
cnf(c49431,plain,
( ~ ssPv1(skf3(X3662))
| ssPv1(X3662)
| ssPv3(skf3(X3662))
| ssPv2(skf2(skf3(X3662))) ),
inference(resolution,[status(thm)],[c29491,c23876]) ).
cnf(c65896,plain,
( ssPv1(X3663)
| ssPv3(skf3(X3663))
| ssPv2(skf2(skf3(X3663))) ),
inference(resolution,[status(thm)],[c49431,c33454]) ).
cnf(c177902,plain,
( ssPv1(X7619)
| ssPv2(skf2(X7619)) ),
inference(resolution,[status(thm)],[c177876,c103488]) ).
cnf(c177943,plain,
( ssPv2(skf2(X7620))
| ~ ssPv3(X7620) ),
inference(resolution,[status(thm)],[c177902,c42874]) ).
cnf(c178012,plain,
( ssPv2(skf2(skf3(X7625)))
| ssPv1(X7625) ),
inference(resolution,[status(thm)],[c177943,c65896]) ).
cnf(c178072,plain,
( ssPv1(X7668)
| ~ ssPv1(skf3(X7668))
| ~ ssPv3(skf3(X7668)) ),
inference(resolution,[status(thm)],[c178012,c56217]) ).
cnf(c105,plain,
( ~ ssRr(X91,X90)
| ~ ssPv2(X90)
| ssPv1(X91)
| ssPv4(skf2(X90))
| ssPv1(X90) ),
inference(resolution,[status(thm)],[clause14,clause2]) ).
cnf(c157,plain,
( ~ ssPv2(X92)
| ssPv1(skf3(X92))
| ssPv4(skf2(X92))
| ssPv1(X92) ),
inference(resolution,[status(thm)],[c105,clause1]) ).
cnf(c11462,plain,
( ssPv4(X1017)
| ssPv4(skf2(X1017))
| ssPv1(X1017)
| ssPv1(skf3(X1017)) ),
inference(resolution,[status(thm)],[c11352,c157]) ).
cnf(c11752,plain,
( ssPv4(X6464)
| ssPv1(X6464)
| ssPv1(skf3(X6464))
| ~ ssRr(X6463,X6464)
| ~ ssPv2(X6464)
| ssPv1(X6463) ),
inference(resolution,[status(thm)],[c11462,c474]) ).
cnf(c144568,plain,
( ssPv4(X6466)
| ssPv1(X6466)
| ssPv1(skf3(X6466))
| ~ ssPv2(X6466) ),
inference(resolution,[status(thm)],[c11752,clause1]) ).
cnf(c174347,plain,
( ssPv1(X7507)
| ssPv4(X7507)
| ssPv1(skf3(X7507)) ),
inference(resolution,[status(thm)],[c174230,c144568]) ).
cnf(c580,plain,
( ~ ssPv1(X292)
| ~ ssPv2(skf3(X292))
| ssPv4(X292)
| ssPv3(X292)
| ssPv1(skf3(X292)) ),
inference(resolution,[status(thm)],[c568,c41]) ).
cnf(c174350,plain,
( ssPv1(skf3(X7584))
| ~ ssPv1(X7584)
| ssPv4(X7584)
| ssPv3(X7584) ),
inference(resolution,[status(thm)],[c174230,c580]) ).
cnf(c176910,plain,
( ssPv1(skf3(X7585))
| ssPv4(X7585)
| ssPv3(X7585) ),
inference(resolution,[status(thm)],[c174350,c174347]) ).
cnf(c102678,plain,
( ssPv3(skf2(X5023))
| ssPv1(skf2(X5023))
| ssPv2(X5023)
| ssPv4(skf2(X5023)) ),
inference(resolution,[status(thm)],[c102553,c4]) ).
cnf(c106686,plain,
( ssPv3(skf2(X5025))
| ssPv1(skf2(X5025))
| ssPv2(X5025) ),
inference(resolution,[status(thm)],[c102678,c7]) ).
cnf(c106794,plain,
( ssPv3(skf2(X5351))
| ssPv2(X5351)
| ~ ssPv2(skf2(X5351))
| ~ ssPv1(X5351)
| ~ ssPv4(X5351) ),
inference(resolution,[status(thm)],[c106686,c677]) ).
cnf(c111938,plain,
( ssPv3(skf2(X5352))
| ssPv2(X5352)
| ~ ssPv1(X5352)
| ~ ssPv4(X5352) ),
inference(resolution,[status(thm)],[c106794,c102934]) ).
cnf(c107210,plain,
( ssPv3(skf2(X5368))
| ssPv2(X5368)
| ssPv4(X5368)
| ssPv1(skf3(X5368))
| ~ ssPv1(X5368) ),
inference(resolution,[status(thm)],[c107070,c8117]) ).
cnf(c112181,plain,
( ssPv3(skf2(X5369))
| ssPv2(X5369)
| ssPv4(X5369)
| ssPv1(skf3(X5369)) ),
inference(resolution,[status(thm)],[c107210,c28704]) ).
cnf(c112381,plain,
( ssPv3(skf2(X5370))
| ssPv2(X5370)
| ssPv1(skf3(X5370))
| ~ ssPv1(X5370) ),
inference(resolution,[status(thm)],[c112181,c111938]) ).
cnf(c152422,plain,
( ssPv3(skf2(X6723))
| ssPv2(X6723)
| ssPv1(skf3(X6723)) ),
inference(resolution,[status(thm)],[c152264,c112381]) ).
cnf(c37,plain,
( ~ ssPv4(X40)
| ssPv3(X40)
| ssPv3(skf2(X40))
| ssPv4(skf2(X40)) ),
inference(resolution,[status(thm)],[c34,clause2]) ).
cnf(c40,plain,
( ssPv3(X42)
| ssPv3(skf2(X42))
| ssPv4(skf2(X42))
| ssPv1(X42) ),
inference(resolution,[status(thm)],[c37,c0]) ).
cnf(c567,plain,
( ~ ssPv1(skf2(X232))
| ~ ssPv2(X232)
| ~ ssPv3(X232)
| ssPv4(skf2(X232)) ),
inference(resolution,[status(thm)],[c564,clause2]) ).
cnf(c24,plain,
( ~ ssRr(X544,skf2(X545))
| ~ ssPv1(skf2(X545))
| ssPv4(X544)
| ssPv1(X545)
| ssPv4(skf2(X545)) ),
inference(resolution,[status(thm)],[clause9,clause2]) ).
cnf(c1716,plain,
( ~ ssPv1(skf2(X585))
| ssPv4(skf3(skf2(X585)))
| ssPv1(X585)
| ssPv4(skf2(X585)) ),
inference(resolution,[status(thm)],[c24,clause1]) ).
cnf(c3792,plain,
( ssPv4(skf3(skf2(X826)))
| ssPv1(skf2(X826))
| ssPv4(skf2(X826))
| ssPv2(X826) ),
inference(resolution,[status(thm)],[c3701,c4]) ).
cnf(c6632,plain,
( ssPv4(skf3(skf2(X827)))
| ssPv4(skf2(X827))
| ssPv2(X827)
| ssPv1(X827) ),
inference(resolution,[status(thm)],[c3792,c1716]) ).
cnf(c6733,plain,
( ssPv4(skf3(skf2(X849)))
| ssPv4(skf2(X849))
| ssPv1(X849)
| ssPv1(skf3(X849)) ),
inference(resolution,[status(thm)],[c6632,c157]) ).
cnf(c30585,plain,
( ssPv2(skf2(X2047))
| ssPv4(skf3(skf2(X2047)))
| ssPv3(X2047)
| ssPv4(X2047) ),
inference(resolution,[status(thm)],[c30442,c61]) ).
cnf(c32991,plain,
( ssPv2(skf2(X2191))
| ssPv4(skf3(skf2(X2191)))
| ssPv3(X2191)
| ssPv2(X2191) ),
inference(resolution,[status(thm)],[c30585,c22623]) ).
cnf(c35626,plain,
( ssPv4(skf3(skf2(X2318)))
| ssPv3(X2318)
| ssPv2(X2318)
| ~ ssPv1(skf2(X2318)) ),
inference(resolution,[status(thm)],[c32991,c269]) ).
cnf(c42911,plain,
( ssPv4(skf3(skf2(X2556)))
| ~ ssPv4(skf2(X2556))
| ssPv1(X2556)
| ssPv2(X2556) ),
inference(resolution,[status(thm)],[c42833,c519]) ).
cnf(c43807,plain,
( ssPv4(skf3(skf2(X2557)))
| ssPv1(X2557)
| ssPv2(X2557) ),
inference(resolution,[status(thm)],[c42911,c6632]) ).
cnf(c43855,plain,
( ssPv4(skf3(skf2(X2618)))
| ssPv2(X2618)
| ssPv1(skf2(X2618))
| ssPv3(X2618) ),
inference(resolution,[status(thm)],[c43807,c12009]) ).
cnf(c44539,plain,
( ssPv4(skf3(skf2(X2619)))
| ssPv2(X2619)
| ssPv3(X2619) ),
inference(resolution,[status(thm)],[c43855,c35626]) ).
cnf(c42905,plain,
( ssPv4(skf3(skf2(X3404)))
| ~ ssRr(X3405,X3404)
| ~ ssPv3(X3404)
| ssPv2(X3405)
| ssPv2(X3404) ),
inference(resolution,[status(thm)],[c42833,c368]) ).
cnf(c57990,plain,
( ssPv4(skf3(skf2(X3406)))
| ~ ssPv3(X3406)
| ssPv2(skf3(X3406))
| ssPv2(X3406) ),
inference(resolution,[status(thm)],[c42905,clause1]) ).
cnf(c58041,plain,
( ssPv4(skf3(skf2(X3407)))
| ssPv2(skf3(X3407))
| ssPv2(X3407) ),
inference(resolution,[status(thm)],[c57990,c44539]) ).
cnf(c43937,plain,
( ssPv4(skf3(skf2(X2624)))
| ssPv1(X2624)
| ssPv2(skf3(X2624))
| ssPv4(X2624) ),
inference(resolution,[status(thm)],[c43807,c5]) ).
cnf(c58208,plain,
( ssPv4(skf3(skf2(X3926)))
| ssPv2(skf3(X3926))
| ~ ssPv4(X3926)
| ssPv1(skf3(X3926)) ),
inference(resolution,[status(thm)],[c58041,c520]) ).
cnf(c74225,plain,
( ssPv4(skf3(skf2(X4231)))
| ssPv2(skf3(X4231))
| ssPv1(skf3(X4231))
| ssPv1(X4231) ),
inference(resolution,[status(thm)],[c58208,c43937]) ).
cnf(c86628,plain,
( ssPv4(skf3(skf2(X4232)))
| ssPv2(skf3(X4232))
| ssPv1(X4232)
| ~ ssPv2(X4232) ),
inference(resolution,[status(thm)],[c74225,c36391]) ).
cnf(c86763,plain,
( ssPv4(skf3(skf2(X4233)))
| ssPv2(skf3(X4233))
| ssPv1(X4233) ),
inference(resolution,[status(thm)],[c86628,c58041]) ).
cnf(c87010,plain,
( ssPv4(skf3(skf2(X4240)))
| ssPv1(X4240)
| ~ ssPv3(X4240)
| ~ ssPv1(skf3(X4240)) ),
inference(resolution,[status(thm)],[c86763,c651]) ).
cnf(c87170,plain,
( ssPv4(skf3(skf2(X4243)))
| ssPv1(X4243)
| ~ ssPv3(X4243)
| ssPv4(skf2(X4243)) ),
inference(resolution,[status(thm)],[c87010,c6733]) ).
cnf(c87241,plain,
( ssPv4(skf3(skf2(X4380)))
| ssPv1(X4380)
| ssPv4(skf2(X4380))
| ssPv3(skf2(X4380)) ),
inference(resolution,[status(thm)],[c87170,c40]) ).
cnf(c93487,plain,
( ssPv1(X4452)
| ssPv4(skf2(X4452))
| ssPv3(skf2(X4452))
| ~ ssPv1(skf3(skf2(X4452))) ),
inference(resolution,[status(thm)],[c87241,c250]) ).
cnf(c144822,plain,
( ssPv4(X6467)
| ssPv1(X6467)
| ssPv1(skf3(X6467))
| ssPv3(X6467) ),
inference(resolution,[status(thm)],[c144568,c102934]) ).
cnf(c145000,plain,
( ssPv4(skf2(X6559))
| ssPv1(skf2(X6559))
| ssPv3(skf2(X6559))
| ssPv1(X6559) ),
inference(resolution,[status(thm)],[c144822,c93487]) ).
cnf(c149699,plain,
( ssPv4(skf2(X6681))
| ssPv3(skf2(X6681))
| ssPv1(X6681)
| ~ ssPv2(X6681)
| ~ ssPv3(X6681) ),
inference(resolution,[status(thm)],[c145000,c567]) ).
cnf(c151141,plain,
( ssPv4(skf2(X6682))
| ssPv3(skf2(X6682))
| ssPv1(X6682)
| ~ ssPv2(X6682) ),
inference(resolution,[status(thm)],[c149699,c40]) ).
cnf(c152551,plain,
( ssPv3(skf2(X6725))
| ssPv1(X6725)
| ssPv4(skf2(X6725)) ),
inference(resolution,[status(thm)],[c152264,c151141]) ).
cnf(c153118,plain,
( ssPv3(skf2(X6837))
| ssPv1(X6837)
| ~ ssRr(X6836,X6837)
| ~ ssPv2(X6837)
| ssPv1(X6836) ),
inference(resolution,[status(thm)],[c152551,c474]) ).
cnf(c155916,plain,
( ssPv3(skf2(X6839))
| ssPv1(X6839)
| ~ ssPv2(X6839)
| ssPv1(skf3(X6839)) ),
inference(resolution,[status(thm)],[c153118,clause1]) ).
cnf(c156112,plain,
( ssPv3(skf2(X6840))
| ssPv1(X6840)
| ssPv1(skf3(X6840)) ),
inference(resolution,[status(thm)],[c155916,c152422]) ).
cnf(c177923,plain,
( ssPv1(skf2(X7659))
| ssPv1(X7659)
| ssPv1(skf3(X7659)) ),
inference(resolution,[status(thm)],[c177876,c156112]) ).
cnf(c174288,plain,
( ssPv2(skf3(X7501))
| ssPv1(X7501)
| ~ ssPv2(X7501) ),
inference(resolution,[status(thm)],[c174230,c36391]) ).
cnf(c174875,plain,
( ssPv2(skf3(X7503))
| ssPv1(X7503) ),
inference(resolution,[status(thm)],[c174288,c174230]) ).
cnf(c174984,plain,
( ssPv1(X7512)
| ~ ssPv3(X7512)
| ~ ssPv1(skf3(X7512)) ),
inference(resolution,[status(thm)],[c174875,c651]) ).
cnf(c175368,plain,
( ssPv1(X7513)
| ~ ssPv3(X7513)
| ssPv4(X7513) ),
inference(resolution,[status(thm)],[c174984,c174347]) ).
cnf(c175518,plain,
( ssPv1(skf3(X7561))
| ssPv4(skf3(X7561))
| ssPv3(X7561) ),
inference(resolution,[status(thm)],[c175368,c1]) ).
cnf(c177847,plain,
( ~ ssPv4(skf3(X7649))
| ~ ssPv4(X7649)
| ssPv3(skf2(X7649)) ),
inference(resolution,[status(thm)],[c177843,c151661]) ).
cnf(c178376,plain,
( ~ ssPv4(X8101)
| ssPv3(skf2(X8101))
| ssPv1(skf3(X8101))
| ssPv3(X8101) ),
inference(resolution,[status(thm)],[c177847,c175518]) ).
cnf(c179570,plain,
( ssPv3(skf2(X8102))
| ssPv1(skf3(X8102))
| ssPv3(X8102) ),
inference(resolution,[status(thm)],[c178376,c176910]) ).
cnf(c179605,plain,
( ssPv1(skf3(X8103))
| ssPv3(X8103)
| ssPv1(skf2(X8103)) ),
inference(resolution,[status(thm)],[c179570,c177876]) ).
cnf(c179658,plain,
( ssPv1(skf3(X8106))
| ssPv1(skf2(X8106))
| ~ ssPv1(X8106) ),
inference(resolution,[status(thm)],[c179605,c172667]) ).
cnf(c179691,plain,
( ssPv1(skf3(X8107))
| ssPv1(skf2(X8107)) ),
inference(resolution,[status(thm)],[c179658,c177923]) ).
cnf(c179753,plain,
( ssPv1(skf3(X8177))
| ~ ssPv2(skf2(X8177))
| ~ ssPv1(X8177)
| ~ ssPv4(X8177) ),
inference(resolution,[status(thm)],[c179691,c677]) ).
cnf(c180264,plain,
( ssPv1(skf3(X8178))
| ~ ssPv1(X8178)
| ~ ssPv4(X8178) ),
inference(resolution,[status(thm)],[c179753,c179452]) ).
cnf(c180272,plain,
( ssPv1(skf3(X8179))
| ~ ssPv1(X8179)
| ssPv3(X8179) ),
inference(resolution,[status(thm)],[c180264,c176910]) ).
cnf(c180292,plain,
( ssPv1(skf3(skf3(X8183)))
| ssPv3(skf3(X8183)) ),
inference(resolution,[status(thm)],[c180272,c177906]) ).
cnf(c180334,plain,
( ssPv1(skf3(skf3(X8209)))
| ssPv1(X8209)
| ~ ssPv1(skf3(X8209)) ),
inference(resolution,[status(thm)],[c180292,c178072]) ).
cnf(c180513,plain,
( ssPv1(skf3(skf3(X8210)))
| ssPv1(X8210) ),
inference(resolution,[status(thm)],[c180334,c177906]) ).
cnf(c180536,plain,
( ssPv1(X8211)
| ~ ssPv1(skf3(X8211))
| ssPv3(X8211) ),
inference(resolution,[status(thm)],[c180513,c1736]) ).
cnf(c180569,plain,
( ssPv1(skf3(X8216))
| ssPv3(skf3(X8216)) ),
inference(resolution,[status(thm)],[c180536,c177906]) ).
cnf(c180686,plain,
ssPv1(skf3(X8217)),
inference(resolution,[status(thm)],[c180569,c177876]) ).
cnf(c180687,plain,
( ssPv1(X8219)
| ssPv3(X8219) ),
inference(resolution,[status(thm)],[c180686,c180536]) ).
cnf(c180722,plain,
ssPv1(X8220),
inference(resolution,[status(thm)],[c180687,c177876]) ).
cnf(clause52,negated_conjecture,
( ~ ssRr(X455,X453)
| ~ ssPv2(X455)
| ~ ssRr(X452,X453)
| ~ ssPv1(X452)
| ~ ssRr(X453,X454)
| ~ ssPv1(X454)
| ~ ssPv1(X453) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
cnf(c1317,plain,
( ~ ssRr(X7133,X7134)
| ~ ssPv2(X7133)
| ~ ssRr(X7135,X7134)
| ~ ssPv1(X7135)
| ~ ssPv1(skf2(X7134))
| ~ ssPv1(X7134) ),
inference(resolution,[status(thm)],[clause52,clause2]) ).
cnf(c180725,plain,
( ~ ssRr(X8605,X8603)
| ~ ssPv2(X8605)
| ~ ssRr(X8604,X8603)
| ~ ssPv1(X8604)
| ~ ssPv1(X8603) ),
inference(resolution,[status(thm)],[c180722,c1317]) ).
cnf(c180745,plain,
( ~ ssRr(X8608,X8607)
| ~ ssPv2(X8608)
| ~ ssPv1(X8608)
| ~ ssPv1(X8607) ),
inference(factor,[status(thm)],[c180725]) ).
cnf(c180748,plain,
( ~ ssPv2(X8609)
| ~ ssPv1(X8609)
| ~ ssPv1(skf2(X8609)) ),
inference(resolution,[status(thm)],[c180745,clause2]) ).
cnf(c180750,plain,
( ~ ssPv2(X8610)
| ~ ssPv1(X8610) ),
inference(resolution,[status(thm)],[c180748,c180722]) ).
cnf(c180751,plain,
~ ssPv2(X8611),
inference(resolution,[status(thm)],[c180750,c180722]) ).
cnf(c180752,plain,
$false,
inference(resolution,[status(thm)],[c180751,c179452]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SYN796-1 : TPTP v8.1.2. Released v2.5.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n004.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:30:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 279.30/279.57 % Version: 1.5
% 279.30/279.57 % SZS status Unsatisfiable
% 279.30/279.57 % SZS output start CNFRefutation
% See solution above
% 279.30/279.59
% 279.30/279.59 % Initial clauses : 52
% 279.30/279.59 % Processed clauses : 1902
% 279.30/279.59 % Factors computed : 118
% 279.30/279.59 % Resolvents computed: 180635
% 279.30/279.59 % Tautologies deleted: 733
% 279.30/279.59 % Forward subsumed : 5313
% 279.30/279.59 % Backward subsumed : 1854
% 279.30/279.59 % -------- CPU Time ---------
% 279.30/279.59 % User time : 278.697 s
% 279.30/279.59 % System time : 0.449 s
% 279.30/279.59 % Total time : 279.146 s
%------------------------------------------------------------------------------