%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN759-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:48:48 EDT 2024
% Result : Unsatisfiable 45.29s 45.50s
% Output : Refutation 45.34s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssRr(X2,skf1(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause10,negated_conjecture,
( ~ ssRr(X103,X102)
| ~ ssPv4(X102)
| ~ ssRr(X101,X103)
| ~ ssRr(X101,X100)
| ~ ssPv2(X100)
| ~ ssPv3(X101)
| ssPv1(X101) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c55,plain,
( ~ ssRr(X124,X123)
| ~ ssPv4(X123)
| ~ ssRr(X125,X124)
| ~ ssPv2(X124)
| ~ ssPv3(X125)
| ssPv1(X125) ),
inference(factor,[status(thm)],[clause10]) ).
cnf(c68,plain,
( ~ ssRr(skf1(X135),X136)
| ~ ssPv4(X136)
| ~ ssPv2(skf1(X135))
| ~ ssPv3(X135)
| ssPv1(X135) ),
inference(resolution,[status(thm)],[c55,clause1]) ).
cnf(c76,plain,
( ~ ssPv4(skf1(skf1(X137)))
| ~ ssPv2(skf1(X137))
| ~ ssPv3(X137)
| ssPv1(X137) ),
inference(resolution,[status(thm)],[c68,clause1]) ).
cnf(clause8,negated_conjecture,
( ~ ssRr(X78,X77)
| ~ ssRr(X76,X78)
| ~ ssRr(X76,X75)
| ~ ssPv3(X75)
| ~ ssPv4(X76)
| ssPv4(X77)
| ssPv1(X76) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c41,plain,
( ~ ssRr(X96,X95)
| ~ ssRr(X94,X96)
| ~ ssPv3(X96)
| ~ ssPv4(X94)
| ssPv4(X95)
| ssPv1(X94) ),
inference(factor,[status(thm)],[clause8]) ).
cnf(c52,plain,
( ~ ssRr(skf1(X117),X118)
| ~ ssPv3(skf1(X117))
| ~ ssPv4(X117)
| ssPv4(X118)
| ssPv1(X117) ),
inference(resolution,[status(thm)],[c41,clause1]) ).
cnf(c64,plain,
( ~ ssPv3(skf1(X119))
| ~ ssPv4(X119)
| ssPv4(skf1(skf1(X119)))
| ssPv1(X119) ),
inference(resolution,[status(thm)],[c52,clause1]) ).
cnf(clause36,negated_conjecture,
( ~ ssRr(X500,X498)
| ~ ssPv2(X498)
| ~ ssRr(X501,X500)
| ~ ssRr(X502,X499)
| ~ ssPv1(X499)
| ~ ssRr(X501,X502)
| ~ ssRr(X501,X503)
| ssPv4(X503)
| ssPv2(X501) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c325,plain,
( ~ ssRr(X2105,X2101)
| ~ ssPv2(X2101)
| ~ ssRr(X2104,X2105)
| ~ ssRr(X2102,X2103)
| ~ ssPv1(X2103)
| ~ ssRr(X2104,X2102)
| ssPv4(X2105)
| ssPv2(X2104) ),
inference(factor,[status(thm)],[clause36]) ).
cnf(c4487,plain,
( ~ ssRr(X2324,X2326)
| ~ ssPv2(X2326)
| ~ ssRr(X2325,X2324)
| ~ ssRr(X2324,X2323)
| ~ ssPv1(X2323)
| ssPv4(X2324)
| ssPv2(X2325) ),
inference(factor,[status(thm)],[c325]) ).
cnf(c5809,plain,
( ~ ssRr(X2329,X2328)
| ~ ssPv2(X2328)
| ~ ssRr(X2327,X2329)
| ~ ssPv1(X2328)
| ssPv4(X2329)
| ssPv2(X2327) ),
inference(factor,[status(thm)],[c4487]) ).
cnf(c5813,plain,
( ~ ssRr(skf1(X2337),X2338)
| ~ ssPv2(X2338)
| ~ ssPv1(X2338)
| ssPv4(skf1(X2337))
| ssPv2(X2337) ),
inference(resolution,[status(thm)],[c5809,clause1]) ).
cnf(c5817,plain,
( ~ ssPv2(skf1(skf1(X2343)))
| ~ ssPv1(skf1(skf1(X2343)))
| ssPv4(skf1(X2343))
| ssPv2(X2343) ),
inference(resolution,[status(thm)],[c5813,clause1]) ).
cnf(clause30,negated_conjecture,
( ~ ssRr(X396,X394)
| ~ ssRr(X397,X396)
| ~ ssRr(X398,X395)
| ~ ssRr(X397,X398)
| ~ ssRr(X397,X399)
| ssPv3(X394)
| ssPv2(X395)
| ssPv1(X399)
| ssPv4(X397) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c250,plain,
( ~ ssRr(X1528,X1527)
| ~ ssRr(X1525,X1528)
| ~ ssRr(X1524,X1526)
| ~ ssRr(X1525,X1524)
| ssPv3(X1527)
| ssPv2(X1526)
| ssPv1(X1528)
| ssPv4(X1525) ),
inference(factor,[status(thm)],[clause30]) ).
cnf(c3149,plain,
( ~ ssRr(X1571,X1572)
| ~ ssRr(X1573,X1571)
| ~ ssRr(X1571,X1570)
| ssPv3(X1572)
| ssPv2(X1570)
| ssPv1(X1571)
| ssPv4(X1573) ),
inference(factor,[status(thm)],[c250]) ).
cnf(c3175,plain,
( ~ ssRr(X1575,X1574)
| ~ ssRr(X1576,X1575)
| ssPv3(X1574)
| ssPv2(X1574)
| ssPv1(X1575)
| ssPv4(X1576) ),
inference(factor,[status(thm)],[c3149]) ).
cnf(c3179,plain,
( ~ ssRr(skf1(X1585),X1586)
| ssPv3(X1586)
| ssPv2(X1586)
| ssPv1(skf1(X1585))
| ssPv4(X1585) ),
inference(resolution,[status(thm)],[c3175,clause1]) ).
cnf(c3181,plain,
( ssPv3(skf1(skf1(X1596)))
| ssPv2(skf1(skf1(X1596)))
| ssPv1(skf1(X1596))
| ssPv4(X1596) ),
inference(resolution,[status(thm)],[c3179,clause1]) ).
cnf(clause35,negated_conjecture,
( ~ ssRr(X481,X479)
| ~ ssPv3(X479)
| ~ ssRr(X482,X481)
| ~ ssRr(X483,X480)
| ~ ssRr(X482,X483)
| ~ ssRr(X482,X484)
| ssPv2(X480)
| ssPv1(X484)
| ssPv4(X482) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c314,plain,
( ~ ssRr(X2028,X2025)
| ~ ssPv3(X2025)
| ~ ssRr(X2026,X2028)
| ~ ssRr(X2029,X2027)
| ~ ssRr(X2026,X2029)
| ssPv2(X2027)
| ssPv1(X2028)
| ssPv4(X2026) ),
inference(factor,[status(thm)],[clause35]) ).
cnf(c4414,plain,
( ~ ssRr(X2097,X2095)
| ~ ssPv3(X2095)
| ~ ssRr(X2094,X2097)
| ~ ssRr(X2097,X2096)
| ssPv2(X2096)
| ssPv1(X2097)
| ssPv4(X2094) ),
inference(factor,[status(thm)],[c314]) ).
cnf(c4481,plain,
( ~ ssRr(X2099,X2100)
| ~ ssPv3(X2100)
| ~ ssRr(X2098,X2099)
| ssPv2(X2100)
| ssPv1(X2099)
| ssPv4(X2098) ),
inference(factor,[status(thm)],[c4414]) ).
cnf(c4485,plain,
( ~ ssRr(skf1(X2109),X2110)
| ~ ssPv3(X2110)
| ssPv2(X2110)
| ssPv1(skf1(X2109))
| ssPv4(X2109) ),
inference(resolution,[status(thm)],[c4481,clause1]) ).
cnf(c4490,plain,
( ~ ssPv3(skf1(skf1(X2121)))
| ssPv2(skf1(skf1(X2121)))
| ssPv1(skf1(X2121))
| ssPv4(X2121) ),
inference(resolution,[status(thm)],[c4485,clause1]) ).
cnf(c4520,plain,
( ssPv2(skf1(skf1(X2122)))
| ssPv1(skf1(X2122))
| ssPv4(X2122) ),
inference(resolution,[status(thm)],[c4490,c3181]) ).
cnf(clause37,negated_conjecture,
( ~ ssRr(X517,X515)
| ~ ssPv3(X515)
| ~ ssRr(X518,X517)
| ~ ssRr(X519,X516)
| ~ ssPv2(X516)
| ~ ssRr(X518,X519)
| ~ ssRr(X518,X520)
| ssPv1(X520)
| ssPv4(X518) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c336,plain,
( ~ ssRr(X2156,X2159)
| ~ ssPv3(X2159)
| ~ ssRr(X2158,X2156)
| ~ ssRr(X2157,X2155)
| ~ ssPv2(X2155)
| ~ ssRr(X2158,X2157)
| ssPv1(X2156)
| ssPv4(X2158) ),
inference(factor,[status(thm)],[clause37]) ).
cnf(c5227,plain,
( ~ ssRr(X2493,X2494)
| ~ ssPv3(X2494)
| ~ ssRr(X2491,X2493)
| ~ ssRr(X2493,X2492)
| ~ ssPv2(X2492)
| ssPv1(X2493)
| ssPv4(X2491) ),
inference(factor,[status(thm)],[c336]) ).
cnf(c7018,plain,
( ~ ssRr(X2499,X2500)
| ~ ssPv3(X2500)
| ~ ssRr(X2501,X2499)
| ~ ssPv2(X2500)
| ssPv1(X2499)
| ssPv4(X2501) ),
inference(factor,[status(thm)],[c5227]) ).
cnf(c7025,plain,
( ~ ssRr(skf1(X2513),X2514)
| ~ ssPv3(X2514)
| ~ ssPv2(X2514)
| ssPv1(skf1(X2513))
| ssPv4(X2513) ),
inference(resolution,[status(thm)],[c7018,clause1]) ).
cnf(c7032,plain,
( ~ ssPv3(skf1(skf1(X2519)))
| ~ ssPv2(skf1(skf1(X2519)))
| ssPv1(skf1(X2519))
| ssPv4(X2519) ),
inference(resolution,[status(thm)],[c7025,clause1]) ).
cnf(c7133,plain,
( ~ ssPv3(skf1(skf1(X2520)))
| ssPv1(skf1(X2520))
| ssPv4(X2520) ),
inference(resolution,[status(thm)],[c7032,c4520]) ).
cnf(clause25,negated_conjecture,
( ~ ssRr(X323,X321)
| ~ ssPv2(X321)
| ~ ssRr(X324,X323)
| ~ ssRr(X325,X322)
| ~ ssRr(X324,X325)
| ~ ssPv1(X324)
| ssPv3(X322)
| ssPv4(X324) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(c182,plain,
( ~ ssRr(X923,X924)
| ~ ssPv2(X924)
| ~ ssRr(X921,X923)
| ~ ssRr(X923,X922)
| ~ ssPv1(X921)
| ssPv3(X922)
| ssPv4(X921) ),
inference(factor,[status(thm)],[clause25]) ).
cnf(c833,plain,
( ~ ssRr(X925,X927)
| ~ ssPv2(X927)
| ~ ssRr(X926,X925)
| ~ ssPv1(X926)
| ssPv3(X927)
| ssPv4(X926) ),
inference(factor,[status(thm)],[c182]) ).
cnf(c837,plain,
( ~ ssRr(skf1(X929),X930)
| ~ ssPv2(X930)
| ~ ssPv1(X929)
| ssPv3(X930)
| ssPv4(X929) ),
inference(resolution,[status(thm)],[c833,clause1]) ).
cnf(c838,plain,
( ~ ssPv2(skf1(skf1(X938)))
| ~ ssPv1(X938)
| ssPv3(skf1(skf1(X938)))
| ssPv4(X938) ),
inference(resolution,[status(thm)],[c837,clause1]) ).
cnf(c3221,plain,
( ssPv3(skf1(skf1(X1597)))
| ssPv1(skf1(X1597))
| ssPv4(X1597)
| ~ ssPv1(X1597) ),
inference(resolution,[status(thm)],[c3181,c838]) ).
cnf(clause23,negated_conjecture,
( ~ ssRr(X294,X292)
| ~ ssPv2(X292)
| ~ ssRr(X295,X294)
| ~ ssRr(X296,X293)
| ~ ssRr(X295,X296)
| ~ ssPv2(X295)
| ssPv3(X293)
| ssPv1(X295) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c166,plain,
( ~ ssRr(X830,X832)
| ~ ssPv2(X832)
| ~ ssRr(X831,X830)
| ~ ssRr(X830,X833)
| ~ ssPv2(X831)
| ssPv3(X833)
| ssPv1(X831) ),
inference(factor,[status(thm)],[clause23]) ).
cnf(c742,plain,
( ~ ssRr(X834,X836)
| ~ ssPv2(X836)
| ~ ssRr(X835,X834)
| ~ ssPv2(X835)
| ssPv3(X836)
| ssPv1(X835) ),
inference(factor,[status(thm)],[c166]) ).
cnf(c746,plain,
( ~ ssRr(skf1(X838),X839)
| ~ ssPv2(X839)
| ~ ssPv2(X838)
| ssPv3(X839)
| ssPv1(X838) ),
inference(resolution,[status(thm)],[c742,clause1]) ).
cnf(c747,plain,
( ~ ssPv2(skf1(skf1(X846)))
| ~ ssPv2(X846)
| ssPv3(skf1(skf1(X846)))
| ssPv1(X846) ),
inference(resolution,[status(thm)],[c746,clause1]) ).
cnf(c3220,plain,
( ssPv3(skf1(skf1(X1598)))
| ssPv1(skf1(X1598))
| ssPv4(X1598)
| ~ ssPv2(X1598)
| ssPv1(X1598) ),
inference(resolution,[status(thm)],[c3181,c747]) ).
cnf(clause5,negated_conjecture,
( ~ ssRr(X40,X39)
| ~ ssRr(X38,X40)
| ~ ssRr(X38,X37)
| ~ ssPv3(X37)
| ssPv2(X39)
| ssPv2(X38)
| ssPv4(X38) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c19,plain,
( ~ ssRr(X48,X49)
| ~ ssRr(X50,X48)
| ~ ssPv3(X48)
| ssPv2(X49)
| ssPv2(X50)
| ssPv4(X50) ),
inference(factor,[status(thm)],[clause5]) ).
cnf(c25,plain,
( ~ ssRr(skf1(X66),X67)
| ~ ssPv3(skf1(X66))
| ssPv2(X67)
| ssPv2(X66)
| ssPv4(X66) ),
inference(resolution,[status(thm)],[c19,clause1]) ).
cnf(c35,plain,
( ~ ssPv3(skf1(X68))
| ssPv2(skf1(skf1(X68)))
| ssPv2(X68)
| ssPv4(X68) ),
inference(resolution,[status(thm)],[c25,clause1]) ).
cnf(clause6,negated_conjecture,
( ~ ssRr(X54,X53)
| ~ ssRr(X52,X54)
| ~ ssRr(X52,X51)
| ~ ssPv3(X52)
| ssPv3(X53)
| ssPv3(X51)
| ssPv4(X52) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c27,plain,
( ~ ssRr(X70,X71)
| ~ ssRr(X69,X70)
| ~ ssPv3(X69)
| ssPv3(X71)
| ssPv3(X70)
| ssPv4(X69) ),
inference(factor,[status(thm)],[clause6]) ).
cnf(c38,plain,
( ~ ssRr(skf1(X84),X85)
| ~ ssPv3(X84)
| ssPv3(X85)
| ssPv3(skf1(X84))
| ssPv4(X84) ),
inference(resolution,[status(thm)],[c27,clause1]) ).
cnf(c45,plain,
( ~ ssPv3(X86)
| ssPv3(skf1(skf1(X86)))
| ssPv3(skf1(X86))
| ssPv4(X86) ),
inference(resolution,[status(thm)],[c38,clause1]) ).
cnf(clause2,negated_conjecture,
( ~ ssRr(X6,X5)
| ~ ssRr(X4,X6)
| ~ ssRr(X4,X3)
| ssPv1(X5)
| ssPv2(X3)
| ssPv2(X4)
| ssPv3(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(c1,plain,
( ~ ssRr(X11,X10)
| ~ ssRr(X12,X11)
| ssPv1(X10)
| ssPv2(X11)
| ssPv2(X12)
| ssPv3(X12) ),
inference(factor,[status(thm)],[clause2]) ).
cnf(c5,plain,
( ~ ssRr(skf1(X18),X19)
| ssPv1(X19)
| ssPv2(skf1(X18))
| ssPv2(X18)
| ssPv3(X18) ),
inference(resolution,[status(thm)],[c1,clause1]) ).
cnf(c9,plain,
( ssPv1(skf1(skf1(X20)))
| ssPv2(skf1(X20))
| ssPv2(X20)
| ssPv3(X20) ),
inference(resolution,[status(thm)],[c5,clause1]) ).
cnf(clause13,negated_conjecture,
( ~ ssRr(X140,X138)
| ~ ssPv1(X138)
| ~ ssRr(X141,X140)
| ~ ssRr(X141,X142)
| ~ ssRr(X141,X139)
| ssPv3(X142)
| ssPv2(X139)
| ssPv1(X141) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(c78,plain,
( ~ ssRr(X340,X342)
| ~ ssPv1(X342)
| ~ ssRr(X341,X340)
| ~ ssRr(X341,X343)
| ssPv3(X343)
| ssPv2(X340)
| ssPv1(X341) ),
inference(factor,[status(thm)],[clause13]) ).
cnf(c193,plain,
( ~ ssRr(X348,X349)
| ~ ssPv1(X349)
| ~ ssRr(X347,X348)
| ssPv3(X348)
| ssPv2(X348)
| ssPv1(X347) ),
inference(factor,[status(thm)],[c78]) ).
cnf(c197,plain,
( ~ ssRr(skf1(X360),X361)
| ~ ssPv1(X361)
| ssPv3(skf1(X360))
| ssPv2(skf1(X360))
| ssPv1(X360) ),
inference(resolution,[status(thm)],[c193,clause1]) ).
cnf(c204,plain,
( ~ ssPv1(skf1(skf1(X362)))
| ssPv3(skf1(X362))
| ssPv2(skf1(X362))
| ssPv1(X362) ),
inference(resolution,[status(thm)],[c197,clause1]) ).
cnf(c205,plain,
( ssPv3(skf1(X368))
| ssPv2(skf1(X368))
| ssPv1(X368)
| ssPv2(X368)
| ssPv3(X368) ),
inference(resolution,[status(thm)],[c204,c9]) ).
cnf(clause17,negated_conjecture,
( ~ ssRr(X204,X202)
| ~ ssRr(X205,X204)
| ~ ssRr(X205,X206)
| ~ ssPv2(X206)
| ~ ssRr(X205,X203)
| ~ ssPv4(X205)
| ssPv3(X202)
| ssPv3(X203) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c110,plain,
( ~ ssRr(X546,X543)
| ~ ssRr(X545,X546)
| ~ ssRr(X545,X544)
| ~ ssPv2(X544)
| ~ ssPv4(X545)
| ssPv3(X543)
| ssPv3(X546) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c350,plain,
( ~ ssRr(X556,X555)
| ~ ssRr(X557,X556)
| ~ ssPv2(X556)
| ~ ssPv4(X557)
| ssPv3(X555)
| ssPv3(X556) ),
inference(factor,[status(thm)],[c110]) ).
cnf(c358,plain,
( ~ ssRr(skf1(X562),X563)
| ~ ssPv2(skf1(X562))
| ~ ssPv4(X562)
| ssPv3(X563)
| ssPv3(skf1(X562)) ),
inference(resolution,[status(thm)],[c350,clause1]) ).
cnf(c363,plain,
( ~ ssPv2(skf1(X570))
| ~ ssPv4(X570)
| ssPv3(skf1(skf1(X570)))
| ssPv3(skf1(X570)) ),
inference(resolution,[status(thm)],[c358,clause1]) ).
cnf(c371,plain,
( ~ ssPv4(X1201)
| ssPv3(skf1(skf1(X1201)))
| ssPv3(skf1(X1201))
| ssPv1(X1201)
| ssPv2(X1201)
| ssPv3(X1201) ),
inference(resolution,[status(thm)],[c363,c205]) ).
cnf(clause16,negated_conjecture,
( ~ ssRr(X187,X185)
| ~ ssPv4(X185)
| ~ ssRr(X188,X187)
| ~ ssRr(X189,X186)
| ~ ssRr(X188,X189)
| ssPv3(X186)
| ssPv1(X188)
| ssPv2(X188) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c103,plain,
( ~ ssRr(X510,X508)
| ~ ssPv4(X508)
| ~ ssRr(X511,X510)
| ~ ssRr(X510,X509)
| ssPv3(X509)
| ssPv1(X511)
| ssPv2(X511) ),
inference(factor,[status(thm)],[clause16]) ).
cnf(c330,plain,
( ~ ssRr(X513,X514)
| ~ ssPv4(X514)
| ~ ssRr(X512,X513)
| ssPv3(X514)
| ssPv1(X512)
| ssPv2(X512) ),
inference(factor,[status(thm)],[c103]) ).
cnf(c334,plain,
( ~ ssRr(skf1(X522),X523)
| ~ ssPv4(X523)
| ssPv3(X523)
| ssPv1(X522)
| ssPv2(X522) ),
inference(resolution,[status(thm)],[c330,clause1]) ).
cnf(c340,plain,
( ~ ssPv4(skf1(skf1(X526)))
| ssPv3(skf1(skf1(X526)))
| ssPv1(X526)
| ssPv2(X526) ),
inference(resolution,[status(thm)],[c334,clause1]) ).
cnf(clause14,negated_conjecture,
( ~ ssRr(X157,X155)
| ~ ssRr(X158,X157)
| ~ ssRr(X158,X159)
| ~ ssPv2(X159)
| ~ ssRr(X158,X156)
| ssPv4(X155)
| ssPv3(X156)
| ssPv4(X158) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c87,plain,
( ~ ssRr(X421,X419)
| ~ ssRr(X422,X421)
| ~ ssRr(X422,X420)
| ~ ssPv2(X420)
| ssPv4(X419)
| ssPv3(X421)
| ssPv4(X422) ),
inference(factor,[status(thm)],[clause14]) ).
cnf(c269,plain,
( ~ ssRr(X432,X433)
| ~ ssRr(X434,X432)
| ~ ssPv2(X432)
| ssPv4(X433)
| ssPv3(X432)
| ssPv4(X434) ),
inference(factor,[status(thm)],[c87]) ).
cnf(c278,plain,
( ~ ssRr(skf1(X439),X440)
| ~ ssPv2(skf1(X439))
| ssPv4(X440)
| ssPv3(skf1(X439))
| ssPv4(X439) ),
inference(resolution,[status(thm)],[c269,clause1]) ).
cnf(c283,plain,
( ~ ssPv2(skf1(X441))
| ssPv4(skf1(skf1(X441)))
| ssPv3(skf1(X441))
| ssPv4(X441) ),
inference(resolution,[status(thm)],[c278,clause1]) ).
cnf(c286,plain,
( ssPv4(skf1(skf1(X1187)))
| ssPv3(skf1(X1187))
| ssPv4(X1187)
| ssPv1(X1187)
| ssPv2(X1187)
| ssPv3(X1187) ),
inference(resolution,[status(thm)],[c283,c205]) ).
cnf(c1246,plain,
( ssPv3(skf1(X1337))
| ssPv4(X1337)
| ssPv1(X1337)
| ssPv2(X1337)
| ssPv3(X1337)
| ssPv3(skf1(skf1(X1337))) ),
inference(resolution,[status(thm)],[c286,c340]) ).
cnf(c1893,plain,
( ssPv3(skf1(X1341))
| ssPv1(X1341)
| ssPv2(X1341)
| ssPv3(X1341)
| ssPv3(skf1(skf1(X1341))) ),
inference(resolution,[status(thm)],[c1246,c371]) ).
cnf(clause11,negated_conjecture,
( ~ ssRr(X114,X112)
| ~ ssRr(X115,X114)
| ~ ssRr(X116,X113)
| ~ ssRr(X115,X116)
| ~ ssPv1(X115)
| ssPv3(X112)
| ssPv2(X113)
| ssPv3(X115) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c61,plain,
( ~ ssRr(X240,X241)
| ~ ssRr(X242,X240)
| ~ ssRr(X240,X239)
| ~ ssPv1(X242)
| ssPv3(X241)
| ssPv2(X239)
| ssPv3(X242) ),
inference(factor,[status(thm)],[clause11]) ).
cnf(c134,plain,
( ~ ssRr(X245,X243)
| ~ ssRr(X244,X245)
| ~ ssPv1(X244)
| ssPv3(X243)
| ssPv2(X243)
| ssPv3(X244) ),
inference(factor,[status(thm)],[c61]) ).
cnf(c138,plain,
( ~ ssRr(skf1(X252),X253)
| ~ ssPv1(X252)
| ssPv3(X253)
| ssPv2(X253)
| ssPv3(X252) ),
inference(resolution,[status(thm)],[c134,clause1]) ).
cnf(c143,plain,
( ~ ssPv1(X256)
| ssPv3(skf1(skf1(X256)))
| ssPv2(skf1(skf1(X256)))
| ssPv3(X256) ),
inference(resolution,[status(thm)],[c138,clause1]) ).
cnf(c1944,plain,
( ssPv3(skf1(X1342))
| ssPv4(X1342)
| ssPv1(X1342)
| ssPv2(X1342)
| ssPv3(skf1(skf1(X1342))) ),
inference(resolution,[status(thm)],[c1246,c45]) ).
cnf(c2086,plain,
( ssPv4(X1348)
| ssPv1(X1348)
| ssPv2(X1348)
| ssPv3(skf1(skf1(X1348)))
| ssPv2(skf1(skf1(X1348))) ),
inference(resolution,[status(thm)],[c1944,c35]) ).
cnf(c2305,plain,
( ssPv4(X1353)
| ssPv2(X1353)
| ssPv3(skf1(skf1(X1353)))
| ssPv2(skf1(skf1(X1353)))
| ssPv3(X1353) ),
inference(resolution,[status(thm)],[c2086,c143]) ).
cnf(c2441,plain,
( ssPv4(X1354)
| ssPv2(X1354)
| ssPv3(skf1(skf1(X1354)))
| ssPv3(X1354)
| ~ ssPv1(X1354) ),
inference(resolution,[status(thm)],[c2305,c838]) ).
cnf(c2476,plain,
( ssPv4(X1355)
| ssPv2(X1355)
| ssPv3(skf1(skf1(X1355)))
| ssPv3(X1355)
| ssPv3(skf1(X1355)) ),
inference(resolution,[status(thm)],[c2441,c1893]) ).
cnf(c2570,plain,
( ssPv4(X1356)
| ssPv2(X1356)
| ssPv3(skf1(skf1(X1356)))
| ssPv3(skf1(X1356)) ),
inference(resolution,[status(thm)],[c2476,c45]) ).
cnf(c2671,plain,
( ssPv4(X1357)
| ssPv2(X1357)
| ssPv3(skf1(skf1(X1357)))
| ssPv2(skf1(skf1(X1357))) ),
inference(resolution,[status(thm)],[c2570,c35]) ).
cnf(c3306,plain,
( ssPv3(skf1(skf1(X1609)))
| ssPv1(skf1(X1609))
| ssPv4(X1609)
| ssPv1(X1609)
| ssPv3(skf1(X1609)) ),
inference(resolution,[status(thm)],[c3220,c2570]) ).
cnf(c3422,plain,
( ssPv3(skf1(skf1(X1610)))
| ssPv1(skf1(X1610))
| ssPv4(X1610)
| ssPv3(skf1(X1610)) ),
inference(resolution,[status(thm)],[c3306,c3221]) ).
cnf(c7214,plain,
( ssPv1(skf1(X2526))
| ssPv4(X2526)
| ssPv3(skf1(X2526)) ),
inference(resolution,[status(thm)],[c7133,c3422]) ).
cnf(c7225,plain,
( ssPv4(skf1(X2577))
| ssPv3(skf1(skf1(X2577)))
| ~ ssPv2(skf1(skf1(X2577)))
| ssPv2(X2577) ),
inference(resolution,[status(thm)],[c7214,c5817]) ).
cnf(c8221,plain,
( ssPv4(skf1(X2578))
| ssPv3(skf1(skf1(X2578)))
| ssPv2(X2578)
| ssPv4(X2578) ),
inference(resolution,[status(thm)],[c7225,c2671]) ).
cnf(c8292,plain,
( ssPv4(skf1(X2697))
| ssPv3(skf1(skf1(X2697)))
| ssPv4(X2697)
| ssPv1(skf1(X2697))
| ssPv1(X2697) ),
inference(resolution,[status(thm)],[c8221,c3220]) ).
cnf(c9330,plain,
( ssPv4(skf1(X2700))
| ssPv3(skf1(skf1(X2700)))
| ssPv4(X2700)
| ssPv1(skf1(X2700)) ),
inference(resolution,[status(thm)],[c8292,c3221]) ).
cnf(c9453,plain,
( ssPv4(skf1(X2702))
| ssPv4(X2702)
| ssPv1(skf1(X2702)) ),
inference(resolution,[status(thm)],[c9330,c7133]) ).
cnf(clause22,negated_conjecture,
( ~ ssRr(X278,X276)
| ~ ssRr(X279,X278)
| ~ ssRr(X280,X277)
| ~ ssRr(X279,X280)
| ~ ssPv1(X279)
| ~ ssPv4(X279)
| ssPv3(X276)
| ssPv2(X277) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c156,plain,
( ~ ssRr(X795,X796)
| ~ ssRr(X793,X795)
| ~ ssRr(X795,X794)
| ~ ssPv1(X793)
| ~ ssPv4(X793)
| ssPv3(X796)
| ssPv2(X794) ),
inference(factor,[status(thm)],[clause22]) ).
cnf(c661,plain,
( ~ ssRr(X797,X799)
| ~ ssRr(X798,X797)
| ~ ssPv1(X798)
| ~ ssPv4(X798)
| ssPv3(X799)
| ssPv2(X799) ),
inference(factor,[status(thm)],[c156]) ).
cnf(c665,plain,
( ~ ssRr(skf1(X801),X802)
| ~ ssPv1(X801)
| ~ ssPv4(X801)
| ssPv3(X802)
| ssPv2(X802) ),
inference(resolution,[status(thm)],[c661,clause1]) ).
cnf(c666,plain,
( ~ ssPv1(X806)
| ~ ssPv4(X806)
| ssPv3(skf1(skf1(X806)))
| ssPv2(skf1(skf1(X806))) ),
inference(resolution,[status(thm)],[c665,clause1]) ).
cnf(c2687,plain,
( ssPv2(X1363)
| ssPv3(skf1(skf1(X1363)))
| ssPv2(skf1(skf1(X1363)))
| ~ ssPv1(X1363) ),
inference(resolution,[status(thm)],[c2671,c666]) ).
cnf(clause33,negated_conjecture,
( ~ ssRr(X444,X442)
| ~ ssPv1(X442)
| ~ ssRr(X445,X444)
| ~ ssRr(X446,X443)
| ~ ssRr(X445,X446)
| ~ ssRr(X445,X447)
| ssPv4(X443)
| ssPv3(X447)
| ssPv1(X445) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c289,plain,
( ~ ssRr(X1843,X1842)
| ~ ssPv1(X1842)
| ~ ssRr(X1841,X1843)
| ~ ssRr(X1840,X1839)
| ~ ssRr(X1841,X1840)
| ssPv4(X1839)
| ssPv3(X1843)
| ssPv1(X1841) ),
inference(factor,[status(thm)],[clause33]) ).
cnf(c4056,plain,
( ~ ssRr(X1900,X1901)
| ~ ssPv1(X1901)
| ~ ssRr(X1898,X1900)
| ~ ssRr(X1900,X1899)
| ssPv4(X1899)
| ssPv3(X1900)
| ssPv1(X1898) ),
inference(factor,[status(thm)],[c289]) ).
cnf(c4122,plain,
( ~ ssRr(X1902,X1904)
| ~ ssPv1(X1904)
| ~ ssRr(X1903,X1902)
| ssPv4(X1904)
| ssPv3(X1902)
| ssPv1(X1903) ),
inference(factor,[status(thm)],[c4056]) ).
cnf(c4126,plain,
( ~ ssRr(skf1(X1914),X1915)
| ~ ssPv1(X1915)
| ssPv4(X1915)
| ssPv3(skf1(X1914))
| ssPv1(X1914) ),
inference(resolution,[status(thm)],[c4122,clause1]) ).
cnf(c4132,plain,
( ~ ssPv1(skf1(skf1(X1928)))
| ssPv4(skf1(skf1(X1928)))
| ssPv3(skf1(X1928))
| ssPv1(X1928) ),
inference(resolution,[status(thm)],[c4126,clause1]) ).
cnf(c9572,plain,
( ssPv4(skf1(skf1(X2708)))
| ssPv4(skf1(X2708))
| ssPv3(skf1(X2708))
| ssPv1(X2708) ),
inference(resolution,[status(thm)],[c9453,c4132]) ).
cnf(c9638,plain,
( ssPv4(skf1(skf1(X2709)))
| ssPv4(skf1(X2709))
| ssPv1(X2709)
| ~ ssPv4(X2709) ),
inference(resolution,[status(thm)],[c9572,c64]) ).
cnf(clause32,negated_conjecture,
( ~ ssRr(X428,X426)
| ~ ssPv3(X426)
| ~ ssRr(X429,X428)
| ~ ssRr(X430,X427)
| ~ ssRr(X429,X430)
| ~ ssRr(X429,X431)
| ssPv4(X427)
| ssPv2(X431)
| ssPv2(X429) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c273,plain,
( ~ ssRr(X1699,X1702)
| ~ ssPv3(X1702)
| ~ ssRr(X1698,X1699)
| ~ ssRr(X1701,X1700)
| ~ ssRr(X1698,X1701)
| ssPv4(X1700)
| ssPv2(X1699)
| ssPv2(X1698) ),
inference(factor,[status(thm)],[clause32]) ).
cnf(c3588,plain,
( ~ ssRr(X1761,X1763)
| ~ ssPv3(X1763)
| ~ ssRr(X1764,X1761)
| ~ ssRr(X1761,X1762)
| ssPv4(X1762)
| ssPv2(X1761)
| ssPv2(X1764) ),
inference(factor,[status(thm)],[c273]) ).
cnf(c3619,plain,
( ~ ssRr(X1771,X1772)
| ~ ssPv3(X1772)
| ~ ssRr(X1770,X1771)
| ssPv4(X1772)
| ssPv2(X1771)
| ssPv2(X1770) ),
inference(factor,[status(thm)],[c3588]) ).
cnf(c3625,plain,
( ~ ssRr(skf1(X1774),X1775)
| ~ ssPv3(X1775)
| ssPv4(X1775)
| ssPv2(skf1(X1774))
| ssPv2(X1774) ),
inference(resolution,[status(thm)],[c3619,clause1]) ).
cnf(c3626,plain,
( ~ ssPv3(skf1(skf1(X1784)))
| ssPv4(skf1(skf1(X1784)))
| ssPv2(skf1(X1784))
| ssPv2(X1784) ),
inference(resolution,[status(thm)],[c3625,clause1]) ).
cnf(c3647,plain,
( ssPv4(skf1(skf1(X1785)))
| ssPv2(skf1(X1785))
| ssPv2(X1785)
| ssPv4(X1785)
| ssPv3(skf1(X1785)) ),
inference(resolution,[status(thm)],[c3626,c2570]) ).
cnf(c3694,plain,
( ssPv4(skf1(skf1(X1786)))
| ssPv2(X1786)
| ssPv4(X1786)
| ssPv3(skf1(X1786)) ),
inference(resolution,[status(thm)],[c3647,c283]) ).
cnf(c3830,plain,
( ssPv4(skf1(skf1(X1791)))
| ssPv2(X1791)
| ssPv4(X1791)
| ssPv2(skf1(skf1(X1791))) ),
inference(resolution,[status(thm)],[c3694,c35]) ).
cnf(c9559,plain,
( ssPv4(skf1(skf1(X2816)))
| ssPv4(skf1(X2816))
| ~ ssPv2(skf1(skf1(X2816)))
| ssPv2(X2816) ),
inference(resolution,[status(thm)],[c9453,c5817]) ).
cnf(c10287,plain,
( ssPv4(skf1(skf1(X2817)))
| ssPv4(skf1(X2817))
| ssPv2(X2817)
| ssPv4(X2817) ),
inference(resolution,[status(thm)],[c9559,c3830]) ).
cnf(c10413,plain,
( ssPv4(skf1(skf1(X2818)))
| ssPv4(skf1(X2818))
| ssPv2(X2818)
| ssPv1(X2818) ),
inference(resolution,[status(thm)],[c10287,c9638]) ).
cnf(c10442,plain,
( ssPv4(skf1(X2819))
| ssPv2(X2819)
| ssPv1(X2819)
| ssPv3(skf1(skf1(X2819))) ),
inference(resolution,[status(thm)],[c10413,c340]) ).
cnf(c10579,plain,
( ssPv4(skf1(X2890))
| ssPv2(X2890)
| ssPv3(skf1(skf1(X2890)))
| ssPv2(skf1(skf1(X2890))) ),
inference(resolution,[status(thm)],[c10442,c2687]) ).
cnf(c11413,plain,
( ssPv4(skf1(X2891))
| ssPv2(X2891)
| ssPv3(skf1(skf1(X2891))) ),
inference(resolution,[status(thm)],[c10579,c7225]) ).
cnf(clause41,negated_conjecture,
( ~ ssRr(X585,X583)
| ~ ssPv4(X583)
| ~ ssRr(X586,X585)
| ~ ssRr(X587,X584)
| ~ ssPv3(X584)
| ~ ssRr(X586,X587)
| ~ ssRr(X586,X588)
| ssPv4(X588)
| ssPv2(X586) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(c380,plain,
( ~ ssRr(X2481,X2483)
| ~ ssPv4(X2483)
| ~ ssRr(X2484,X2481)
| ~ ssRr(X2480,X2482)
| ~ ssPv3(X2482)
| ~ ssRr(X2484,X2480)
| ssPv4(X2481)
| ssPv2(X2484) ),
inference(factor,[status(thm)],[clause41]) ).
cnf(c7015,plain,
( ~ ssRr(X3561,X3563)
| ~ ssPv4(X3563)
| ~ ssRr(X3562,X3561)
| ~ ssRr(X3561,X3560)
| ~ ssPv3(X3560)
| ssPv4(X3561)
| ssPv2(X3562) ),
inference(factor,[status(thm)],[c380]) ).
cnf(c16912,plain,
( ~ ssRr(X3564,X3565)
| ~ ssPv4(X3565)
| ~ ssRr(X3566,X3564)
| ~ ssPv3(X3565)
| ssPv4(X3564)
| ssPv2(X3566) ),
inference(factor,[status(thm)],[c7015]) ).
cnf(c16916,plain,
( ~ ssRr(skf1(X3571),X3572)
| ~ ssPv4(X3572)
| ~ ssPv3(X3572)
| ssPv4(skf1(X3571))
| ssPv2(X3571) ),
inference(resolution,[status(thm)],[c16912,clause1]) ).
cnf(c16917,plain,
( ~ ssPv4(skf1(skf1(X3576)))
| ~ ssPv3(skf1(skf1(X3576)))
| ssPv4(skf1(X3576))
| ssPv2(X3576) ),
inference(resolution,[status(thm)],[c16916,clause1]) ).
cnf(c17022,plain,
( ~ ssPv4(skf1(skf1(X3577)))
| ssPv4(skf1(X3577))
| ssPv2(X3577) ),
inference(resolution,[status(thm)],[c16917,c11413]) ).
cnf(c17074,plain,
( ssPv4(skf1(X3587))
| ssPv2(X3587)
| ssPv1(skf1(skf1(X3587))) ),
inference(resolution,[status(thm)],[c17022,c9453]) ).
cnf(c17509,plain,
( ssPv4(skf1(X3589))
| ssPv2(X3589)
| ~ ssPv2(skf1(skf1(X3589))) ),
inference(resolution,[status(thm)],[c17074,c5817]) ).
cnf(c17069,plain,
( ssPv4(skf1(X3580))
| ssPv2(X3580)
| ssPv1(X3580) ),
inference(resolution,[status(thm)],[c17022,c10413]) ).
cnf(clause28,negated_conjecture,
( ~ ssRr(X365,X363)
| ~ ssPv4(X363)
| ~ ssRr(X366,X365)
| ~ ssRr(X366,X367)
| ~ ssPv4(X367)
| ~ ssRr(X366,X364)
| ~ ssPv3(X364)
| ssPv2(X366) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c207,plain,
( ~ ssRr(X1106,X1105)
| ~ ssPv4(X1105)
| ~ ssRr(X1104,X1106)
| ~ ssRr(X1104,X1107)
| ~ ssPv4(X1107)
| ~ ssPv3(X1106)
| ssPv2(X1104) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c1039,plain,
( ~ ssRr(X1120,X1121)
| ~ ssPv4(X1121)
| ~ ssRr(X1119,X1120)
| ~ ssPv4(skf1(X1119))
| ~ ssPv3(X1120)
| ssPv2(X1119) ),
inference(resolution,[status(thm)],[c207,clause1]) ).
cnf(c17034,plain,
( ssPv4(skf1(X3579))
| ssPv2(X3579)
| ssPv4(X3579) ),
inference(resolution,[status(thm)],[c17022,c10287]) ).
cnf(c17106,plain,
( ssPv2(X3633)
| ssPv4(X3633)
| ~ ssRr(X3632,X3634)
| ~ ssPv4(X3634)
| ~ ssRr(X3633,X3632)
| ~ ssPv3(X3632) ),
inference(resolution,[status(thm)],[c17034,c1039]) ).
cnf(c17783,plain,
( ssPv2(X3696)
| ssPv4(X3696)
| ~ ssRr(skf1(X3696),X3697)
| ~ ssPv4(X3697)
| ~ ssPv3(skf1(X3696)) ),
inference(resolution,[status(thm)],[c17106,clause1]) ).
cnf(c17969,plain,
( ssPv2(X3698)
| ssPv4(X3698)
| ~ ssPv4(skf1(skf1(X3698)))
| ~ ssPv3(skf1(X3698)) ),
inference(resolution,[status(thm)],[c17783,clause1]) ).
cnf(c17990,plain,
( ssPv2(X3742)
| ssPv4(X3742)
| ~ ssPv3(skf1(X3742))
| ssPv2(skf1(X3742))
| ssPv1(skf1(X3742)) ),
inference(resolution,[status(thm)],[c17969,c17069]) ).
cnf(c18296,plain,
( ssPv2(X3743)
| ssPv4(X3743)
| ssPv2(skf1(X3743))
| ssPv1(skf1(X3743)) ),
inference(resolution,[status(thm)],[c17990,c7214]) ).
cnf(c18337,plain,
( ssPv4(X4064)
| ssPv2(skf1(X4064))
| ssPv1(skf1(X4064))
| ssPv3(skf1(skf1(X4064)))
| ssPv1(X4064) ),
inference(resolution,[status(thm)],[c18296,c3220]) ).
cnf(c21482,plain,
( ssPv4(X4069)
| ssPv2(skf1(X4069))
| ssPv1(skf1(X4069))
| ssPv3(skf1(skf1(X4069))) ),
inference(resolution,[status(thm)],[c18337,c3221]) ).
cnf(c21699,plain,
( ssPv4(X4070)
| ssPv2(skf1(X4070))
| ssPv1(skf1(X4070)) ),
inference(resolution,[status(thm)],[c21482,c7133]) ).
cnf(clause39,negated_conjecture,
( ~ ssRr(X549,X547)
| ~ ssPv3(X547)
| ~ ssRr(X550,X549)
| ~ ssRr(X551,X548)
| ~ ssRr(X550,X551)
| ~ ssRr(X550,X552)
| ~ ssPv1(X552)
| ssPv4(X548)
| ssPv4(X550) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c353,plain,
( ~ ssRr(X2276,X2280)
| ~ ssPv3(X2280)
| ~ ssRr(X2278,X2276)
| ~ ssRr(X2279,X2277)
| ~ ssRr(X2278,X2279)
| ~ ssPv1(X2276)
| ssPv4(X2277)
| ssPv4(X2278) ),
inference(factor,[status(thm)],[clause39]) ).
cnf(c5714,plain,
( ~ ssRr(X3426,X3428)
| ~ ssPv3(X3428)
| ~ ssRr(X3427,X3426)
| ~ ssRr(X3426,X3425)
| ~ ssPv1(X3426)
| ssPv4(X3425)
| ssPv4(X3427) ),
inference(factor,[status(thm)],[c353]) ).
cnf(c15331,plain,
( ~ ssRr(X3431,X3432)
| ~ ssPv3(X3432)
| ~ ssRr(X3433,X3431)
| ~ ssPv1(X3431)
| ssPv4(X3432)
| ssPv4(X3433) ),
inference(factor,[status(thm)],[c5714]) ).
cnf(c15335,plain,
( ~ ssRr(skf1(X3436),X3437)
| ~ ssPv3(X3437)
| ~ ssPv1(skf1(X3436))
| ssPv4(X3437)
| ssPv4(X3436) ),
inference(resolution,[status(thm)],[c15331,clause1]) ).
cnf(c15511,plain,
( ~ ssPv3(skf1(skf1(X3442)))
| ~ ssPv1(skf1(X3442))
| ssPv4(skf1(skf1(X3442)))
| ssPv4(X3442) ),
inference(resolution,[status(thm)],[c15335,clause1]) ).
cnf(clause7,negated_conjecture,
( ~ ssRr(X65,X64)
| ~ ssRr(X63,X65)
| ~ ssRr(X63,X62)
| ~ ssPv4(X62)
| ~ ssPv1(X63)
| ssPv3(X64)
| ssPv2(X63) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(c33,plain,
( ~ ssRr(X80,X82)
| ~ ssRr(X81,X80)
| ~ ssPv4(X80)
| ~ ssPv1(X81)
| ssPv3(X82)
| ssPv2(X81) ),
inference(factor,[status(thm)],[clause7]) ).
cnf(c44,plain,
( ~ ssRr(skf1(X98),X99)
| ~ ssPv4(skf1(X98))
| ~ ssPv1(X98)
| ssPv3(X99)
| ssPv2(X98) ),
inference(resolution,[status(thm)],[c33,clause1]) ).
cnf(c53,plain,
( ~ ssPv4(skf1(X104))
| ~ ssPv1(X104)
| ssPv3(skf1(skf1(X104)))
| ssPv2(X104) ),
inference(resolution,[status(thm)],[c44,clause1]) ).
cnf(c11439,plain,
( ssPv2(X2892)
| ssPv3(skf1(skf1(X2892)))
| ~ ssPv1(X2892) ),
inference(resolution,[status(thm)],[c11413,c53]) ).
cnf(clause24,negated_conjecture,
( ~ ssRr(X308,X306)
| ~ ssPv3(X306)
| ~ ssRr(X309,X308)
| ~ ssRr(X310,X307)
| ~ ssPv2(X307)
| ~ ssRr(X309,X310)
| ssPv1(X309)
| ssPv3(X309) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c174,plain,
( ~ ssRr(X863,X862)
| ~ ssPv3(X862)
| ~ ssRr(X861,X863)
| ~ ssRr(X863,X864)
| ~ ssPv2(X864)
| ssPv1(X861)
| ssPv3(X861) ),
inference(factor,[status(thm)],[clause24]) ).
cnf(c774,plain,
( ~ ssRr(X866,X865)
| ~ ssPv3(X865)
| ~ ssRr(X867,X866)
| ~ ssPv2(X865)
| ssPv1(X867)
| ssPv3(X867) ),
inference(factor,[status(thm)],[c174]) ).
cnf(c778,plain,
( ~ ssRr(skf1(X870),X871)
| ~ ssPv3(X871)
| ~ ssPv2(X871)
| ssPv1(X870)
| ssPv3(X870) ),
inference(resolution,[status(thm)],[c774,clause1]) ).
cnf(c786,plain,
( ~ ssPv3(skf1(skf1(X874)))
| ~ ssPv2(skf1(skf1(X874)))
| ssPv1(X874)
| ssPv3(X874) ),
inference(resolution,[status(thm)],[c778,clause1]) ).
cnf(clause15,negated_conjecture,
( ~ ssRr(X172,X170)
| ~ ssRr(X173,X172)
| ~ ssRr(X173,X174)
| ~ ssPv3(X174)
| ~ ssRr(X173,X171)
| ssPv2(X170)
| ssPv2(X171)
| ssPv4(X173) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c94,plain,
( ~ ssRr(X459,X460)
| ~ ssRr(X458,X459)
| ~ ssRr(X458,X457)
| ~ ssPv3(X457)
| ssPv2(X460)
| ssPv2(X459)
| ssPv4(X458) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c297,plain,
( ~ ssRr(X470,X471)
| ~ ssRr(X469,X470)
| ~ ssPv3(X470)
| ssPv2(X471)
| ssPv2(X470)
| ssPv4(X469) ),
inference(factor,[status(thm)],[c94]) ).
cnf(c305,plain,
( ~ ssRr(skf1(X476),X477)
| ~ ssPv3(skf1(X476))
| ssPv2(X477)
| ssPv2(skf1(X476))
| ssPv4(X476) ),
inference(resolution,[status(thm)],[c297,clause1]) ).
cnf(c309,plain,
( ~ ssPv3(skf1(X478))
| ssPv2(skf1(skf1(X478)))
| ssPv2(skf1(X478))
| ssPv4(X478) ),
inference(resolution,[status(thm)],[c305,clause1]) ).
cnf(clause3,negated_conjecture,
( ~ ssRr(X16,X15)
| ~ ssRr(X14,X16)
| ~ ssRr(X14,X13)
| ~ ssPv1(X13)
| ssPv1(X15)
| ssPv3(X14)
| ssPv4(X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c7,plain,
( ~ ssRr(X24,X23)
| ~ ssRr(X25,X24)
| ~ ssPv1(X24)
| ssPv1(X23)
| ssPv3(X25)
| ssPv4(X25) ),
inference(factor,[status(thm)],[clause3]) ).
cnf(c11,plain,
( ~ ssRr(skf1(X31),X32)
| ~ ssPv1(skf1(X31))
| ssPv1(X32)
| ssPv3(X31)
| ssPv4(X31) ),
inference(resolution,[status(thm)],[c7,clause1]) ).
cnf(c15,plain,
( ~ ssPv1(skf1(X33))
| ssPv1(skf1(skf1(X33)))
| ssPv3(X33)
| ssPv4(X33) ),
inference(resolution,[status(thm)],[c11,clause1]) ).
cnf(c4548,plain,
( ssPv1(skf1(X2134))
| ssPv4(X2134)
| ~ ssPv3(skf1(skf1(X2134)))
| ssPv1(X2134)
| ssPv3(X2134) ),
inference(resolution,[status(thm)],[c4520,c786]) ).
cnf(c4689,plain,
( ssPv1(skf1(X2140))
| ssPv4(X2140)
| ssPv1(X2140)
| ssPv3(X2140)
| ssPv3(skf1(X2140)) ),
inference(resolution,[status(thm)],[c4548,c3422]) ).
cnf(c4707,plain,
( ssPv4(X2142)
| ssPv1(X2142)
| ssPv3(X2142)
| ssPv3(skf1(X2142))
| ssPv1(skf1(skf1(X2142))) ),
inference(resolution,[status(thm)],[c4689,c15]) ).
cnf(c4885,plain,
( ssPv4(X2143)
| ssPv1(X2143)
| ssPv3(X2143)
| ssPv3(skf1(X2143))
| ssPv2(skf1(X2143)) ),
inference(resolution,[status(thm)],[c4707,c204]) ).
cnf(c4975,plain,
( ssPv4(X2160)
| ssPv1(X2160)
| ssPv3(X2160)
| ssPv2(skf1(X2160))
| ssPv2(skf1(skf1(X2160))) ),
inference(resolution,[status(thm)],[c4885,c309]) ).
cnf(c5336,plain,
( ssPv4(X2162)
| ssPv1(X2162)
| ssPv3(X2162)
| ssPv2(skf1(X2162))
| ~ ssPv3(skf1(skf1(X2162))) ),
inference(resolution,[status(thm)],[c4975,c786]) ).
cnf(c216,plain,
( ssPv2(skf1(X1146))
| ssPv1(X1146)
| ssPv2(X1146)
| ssPv3(X1146)
| ~ ssPv4(X1146)
| ssPv4(skf1(skf1(X1146))) ),
inference(resolution,[status(thm)],[c205,c64]) ).
cnf(clause26,negated_conjecture,
( ~ ssRr(X336,X334)
| ~ ssPv1(X334)
| ~ ssRr(X337,X336)
| ~ ssRr(X337,X338)
| ~ ssPv4(X338)
| ~ ssRr(X337,X335)
| ~ ssPv3(X335)
| ssPv2(X337) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c189,plain,
( ~ ssRr(X983,X984)
| ~ ssPv1(X984)
| ~ ssRr(X985,X983)
| ~ ssRr(X985,X986)
| ~ ssPv4(X986)
| ~ ssPv3(X983)
| ssPv2(X985) ),
inference(factor,[status(thm)],[clause26]) ).
cnf(c880,plain,
( ~ ssRr(X991,X992)
| ~ ssPv1(X992)
| ~ ssRr(X990,X991)
| ~ ssPv4(X991)
| ~ ssPv3(X991)
| ssPv2(X990) ),
inference(factor,[status(thm)],[c189]) ).
cnf(c884,plain,
( ~ ssRr(skf1(X1001),X1002)
| ~ ssPv1(X1002)
| ~ ssPv4(skf1(X1001))
| ~ ssPv3(skf1(X1001))
| ssPv2(X1001) ),
inference(resolution,[status(thm)],[c880,clause1]) ).
cnf(c891,plain,
( ~ ssPv1(skf1(skf1(X1003)))
| ~ ssPv4(skf1(X1003))
| ~ ssPv3(skf1(X1003))
| ssPv2(X1003) ),
inference(resolution,[status(thm)],[c884,clause1]) ).
cnf(c897,plain,
( ~ ssPv4(skf1(X1004))
| ~ ssPv3(skf1(X1004))
| ssPv2(X1004)
| ssPv2(skf1(X1004))
| ssPv3(X1004) ),
inference(resolution,[status(thm)],[c891,c9]) ).
cnf(c904,plain,
( ~ ssPv4(skf1(X1005))
| ssPv2(X1005)
| ssPv2(skf1(X1005))
| ssPv3(X1005)
| ssPv1(X1005) ),
inference(resolution,[status(thm)],[c897,c205]) ).
cnf(c5847,plain,
( ~ ssPv2(skf1(skf1(X2347)))
| ssPv4(skf1(X2347))
| ssPv2(X2347)
| ssPv2(skf1(X2347))
| ssPv3(X2347) ),
inference(resolution,[status(thm)],[c5817,c9]) ).
cnf(c5893,plain,
( ssPv4(skf1(X2348))
| ssPv2(X2348)
| ssPv2(skf1(X2348))
| ssPv3(X2348)
| ssPv4(X2348)
| ssPv1(X2348) ),
inference(resolution,[status(thm)],[c5847,c4975]) ).
cnf(c5920,plain,
( ssPv2(X2349)
| ssPv2(skf1(X2349))
| ssPv3(X2349)
| ssPv4(X2349)
| ssPv1(X2349) ),
inference(resolution,[status(thm)],[c5893,c904]) ).
cnf(c6142,plain,
( ssPv2(X2355)
| ssPv2(skf1(X2355))
| ssPv3(X2355)
| ssPv1(X2355)
| ssPv4(skf1(skf1(X2355))) ),
inference(resolution,[status(thm)],[c5920,c216]) ).
cnf(c6282,plain,
( ssPv2(X2359)
| ssPv2(skf1(X2359))
| ssPv3(X2359)
| ssPv1(X2359)
| ssPv3(skf1(skf1(X2359))) ),
inference(resolution,[status(thm)],[c6142,c340]) ).
cnf(c11532,plain,
( ssPv2(X2899)
| ssPv3(skf1(skf1(X2899)))
| ssPv2(skf1(X2899))
| ssPv3(X2899) ),
inference(resolution,[status(thm)],[c11439,c6282]) ).
cnf(c5318,plain,
( ssPv4(X3183)
| ssPv1(X3183)
| ssPv3(X3183)
| ssPv2(skf1(X3183))
| ~ ssPv2(X3183)
| ssPv3(skf1(skf1(X3183))) ),
inference(resolution,[status(thm)],[c4975,c747]) ).
cnf(c13723,plain,
( ssPv4(X3190)
| ssPv1(X3190)
| ssPv3(X3190)
| ssPv2(skf1(X3190))
| ssPv3(skf1(skf1(X3190))) ),
inference(resolution,[status(thm)],[c5318,c11532]) ).
cnf(c13945,plain,
( ssPv4(X3191)
| ssPv1(X3191)
| ssPv3(X3191)
| ssPv2(skf1(X3191)) ),
inference(resolution,[status(thm)],[c13723,c5336]) ).
cnf(c17538,plain,
( ssPv4(skf1(X3612))
| ssPv2(X3612)
| ssPv1(skf1(X3612))
| ssPv3(skf1(X3612)) ),
inference(resolution,[status(thm)],[c17509,c13945]) ).
cnf(c17707,plain,
( ssPv4(skf1(skf1(X3824)))
| ssPv2(skf1(X3824))
| ssPv1(skf1(skf1(X3824)))
| ssPv2(X3824) ),
inference(resolution,[status(thm)],[c17538,c3626]) ).
cnf(c881,plain,
( ~ ssRr(X999,X1000)
| ~ ssPv1(X1000)
| ~ ssRr(X998,X999)
| ~ ssPv4(skf1(X998))
| ~ ssPv3(X999)
| ssPv2(X998) ),
inference(resolution,[status(thm)],[c189,clause1]) ).
cnf(c11489,plain,
( ssPv4(skf1(X2912))
| ssPv2(X2912)
| ssPv4(skf1(skf1(X2912)))
| ssPv2(skf1(X2912)) ),
inference(resolution,[status(thm)],[c11413,c3626]) ).
cnf(c17050,plain,
( ssPv4(skf1(X3581))
| ssPv2(X3581)
| ssPv2(skf1(X3581)) ),
inference(resolution,[status(thm)],[c17022,c11489]) ).
cnf(c17254,plain,
( ssPv2(X3781)
| ssPv2(skf1(X3781))
| ~ ssRr(X3780,X3782)
| ~ ssPv1(X3782)
| ~ ssRr(X3781,X3780)
| ~ ssPv3(X3780) ),
inference(resolution,[status(thm)],[c17050,c881]) ).
cnf(c19068,plain,
( ssPv2(X3836)
| ssPv2(skf1(X3836))
| ~ ssRr(skf1(X3836),X3837)
| ~ ssPv1(X3837)
| ~ ssPv3(skf1(X3836)) ),
inference(resolution,[status(thm)],[c17254,clause1]) ).
cnf(c19348,plain,
( ssPv2(X3841)
| ssPv2(skf1(X3841))
| ~ ssPv1(skf1(skf1(X3841)))
| ~ ssPv3(skf1(X3841)) ),
inference(resolution,[status(thm)],[c19068,clause1]) ).
cnf(c19385,plain,
( ssPv2(X3848)
| ssPv2(skf1(X3848))
| ~ ssPv3(skf1(X3848))
| ssPv4(skf1(skf1(X3848))) ),
inference(resolution,[status(thm)],[c19348,c17707]) ).
cnf(c19254,plain,
( ssPv4(skf1(skf1(X4138)))
| ssPv2(skf1(X4138))
| ssPv2(X4138)
| ssPv3(skf1(X4138))
| ssPv1(X4138) ),
inference(resolution,[status(thm)],[c17707,c4132]) ).
cnf(c22121,plain,
( ssPv4(skf1(skf1(X4139)))
| ssPv2(skf1(X4139))
| ssPv2(X4139)
| ssPv1(X4139) ),
inference(resolution,[status(thm)],[c19254,c19385]) ).
cnf(c22205,plain,
( ssPv2(skf1(X4146))
| ssPv2(X4146)
| ssPv1(X4146)
| ssPv3(skf1(skf1(X4146))) ),
inference(resolution,[status(thm)],[c22121,c340]) ).
cnf(c22416,plain,
( ssPv2(skf1(X4147))
| ssPv2(X4147)
| ssPv3(skf1(skf1(X4147))) ),
inference(resolution,[status(thm)],[c22205,c11439]) ).
cnf(c22493,plain,
( ssPv2(X4160)
| ssPv3(skf1(skf1(X4160)))
| ~ ssPv4(X4160)
| ssPv3(skf1(X4160)) ),
inference(resolution,[status(thm)],[c22416,c363]) ).
cnf(c22877,plain,
( ssPv2(X4164)
| ssPv3(skf1(skf1(X4164)))
| ssPv3(skf1(X4164)) ),
inference(resolution,[status(thm)],[c22493,c2570]) ).
cnf(clause44,negated_conjecture,
( ~ ssRr(X638,X636)
| ~ ssPv3(X636)
| ~ ssRr(X639,X638)
| ~ ssRr(X640,X637)
| ~ ssPv1(X637)
| ~ ssRr(X639,X640)
| ~ ssRr(X639,X641)
| ~ ssPv1(X639)
| ssPv3(X641) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
cnf(c420,plain,
( ~ ssRr(X2726,X2723)
| ~ ssPv3(X2723)
| ~ ssRr(X2725,X2726)
| ~ ssRr(X2722,X2724)
| ~ ssPv1(X2724)
| ~ ssRr(X2725,X2722)
| ~ ssPv1(X2725)
| ssPv3(X2726) ),
inference(factor,[status(thm)],[clause44]) ).
cnf(c9870,plain,
( ~ ssRr(X4677,X4678)
| ~ ssPv3(X4678)
| ~ ssRr(X4679,X4677)
| ~ ssRr(X4677,X4676)
| ~ ssPv1(X4676)
| ~ ssPv1(X4679)
| ssPv3(X4677) ),
inference(factor,[status(thm)],[c420]) ).
cnf(c25506,plain,
( ~ ssRr(X4684,X4683)
| ~ ssPv3(X4683)
| ~ ssRr(X4685,X4684)
| ~ ssPv1(X4683)
| ~ ssPv1(X4685)
| ssPv3(X4684) ),
inference(factor,[status(thm)],[c9870]) ).
cnf(c25510,plain,
( ~ ssRr(skf1(X4687),X4688)
| ~ ssPv3(X4688)
| ~ ssPv1(X4688)
| ~ ssPv1(X4687)
| ssPv3(skf1(X4687)) ),
inference(resolution,[status(thm)],[c25506,clause1]) ).
cnf(c25511,plain,
( ~ ssPv3(skf1(skf1(X4695)))
| ~ ssPv1(skf1(skf1(X4695)))
| ~ ssPv1(X4695)
| ssPv3(skf1(X4695)) ),
inference(resolution,[status(thm)],[c25510,clause1]) ).
cnf(c25578,plain,
( ~ ssPv3(skf1(skf1(X4739)))
| ~ ssPv1(X4739)
| ssPv3(skf1(X4739))
| ssPv4(skf1(X4739))
| ssPv2(X4739) ),
inference(resolution,[status(thm)],[c25511,c17074]) ).
cnf(c26230,plain,
( ~ ssPv1(X4740)
| ssPv3(skf1(X4740))
| ssPv4(skf1(X4740))
| ssPv2(X4740) ),
inference(resolution,[status(thm)],[c25578,c22877]) ).
cnf(c26268,plain,
( ssPv3(skf1(X4741))
| ssPv4(skf1(X4741))
| ssPv2(X4741) ),
inference(resolution,[status(thm)],[c26230,c17069]) ).
cnf(c26328,plain,
( ssPv4(skf1(skf1(X4752)))
| ssPv2(skf1(X4752))
| ~ ssPv1(skf1(X4752))
| ssPv4(X4752) ),
inference(resolution,[status(thm)],[c26268,c15511]) ).
cnf(c26401,plain,
( ssPv4(skf1(skf1(X4753)))
| ssPv2(skf1(X4753))
| ssPv4(X4753) ),
inference(resolution,[status(thm)],[c26328,c21699]) ).
cnf(clause46,negated_conjecture,
( ~ ssRr(X668,X666)
| ~ ssPv4(X666)
| ~ ssRr(X669,X668)
| ~ ssRr(X670,X667)
| ~ ssPv2(X667)
| ~ ssRr(X669,X670)
| ~ ssRr(X669,X671)
| ~ ssPv1(X671)
| ssPv4(X669) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
cnf(c440,plain,
( ~ ssRr(X2865,X2867)
| ~ ssPv4(X2867)
| ~ ssRr(X2866,X2865)
| ~ ssRr(X2863,X2864)
| ~ ssPv2(X2864)
| ~ ssRr(X2866,X2863)
| ~ ssPv1(X2865)
| ssPv4(X2866) ),
inference(factor,[status(thm)],[clause46]) ).
cnf(c11295,plain,
( ~ ssRr(X5210,X5208)
| ~ ssPv4(X5208)
| ~ ssRr(X5209,X5210)
| ~ ssRr(X5210,X5207)
| ~ ssPv2(X5207)
| ~ ssPv1(X5210)
| ssPv4(X5209) ),
inference(factor,[status(thm)],[c440]) ).
cnf(c29678,plain,
( ~ ssRr(X5211,X5212)
| ~ ssPv4(X5212)
| ~ ssRr(X5213,X5211)
| ~ ssPv2(X5212)
| ~ ssPv1(X5211)
| ssPv4(X5213) ),
inference(factor,[status(thm)],[c11295]) ).
cnf(c29682,plain,
( ~ ssRr(skf1(X5219),X5220)
| ~ ssPv4(X5220)
| ~ ssPv2(X5220)
| ~ ssPv1(skf1(X5219))
| ssPv4(X5219) ),
inference(resolution,[status(thm)],[c29678,clause1]) ).
cnf(c29684,plain,
( ~ ssPv4(skf1(skf1(X5224)))
| ~ ssPv2(skf1(skf1(X5224)))
| ~ ssPv1(skf1(X5224))
| ssPv4(X5224) ),
inference(resolution,[status(thm)],[c29682,clause1]) ).
cnf(c17256,plain,
( ssPv2(X3785)
| ssPv2(skf1(X3785))
| ~ ssRr(X3784,X3786)
| ~ ssPv4(X3786)
| ~ ssRr(X3785,X3784)
| ~ ssPv3(X3784) ),
inference(resolution,[status(thm)],[c17050,c1039]) ).
cnf(c19070,plain,
( ssPv2(X3889)
| ssPv2(skf1(X3889))
| ~ ssRr(skf1(X3889),X3890)
| ~ ssPv4(X3890)
| ~ ssPv3(skf1(X3889)) ),
inference(resolution,[status(thm)],[c17256,clause1]) ).
cnf(c19761,plain,
( ssPv2(X3893)
| ssPv2(skf1(X3893))
| ~ ssPv4(skf1(skf1(X3893)))
| ~ ssPv3(skf1(X3893)) ),
inference(resolution,[status(thm)],[c19070,clause1]) ).
cnf(c22556,plain,
( ssPv2(skf1(X4148))
| ssPv2(X4148)
| ssPv4(skf1(skf1(X4148))) ),
inference(resolution,[status(thm)],[c22416,c3626]) ).
cnf(c22660,plain,
( ssPv2(skf1(X4150))
| ssPv2(X4150)
| ~ ssPv3(skf1(X4150)) ),
inference(resolution,[status(thm)],[c22556,c19761]) ).
cnf(c4951,plain,
( ssPv4(X2202)
| ssPv1(X2202)
| ssPv3(skf1(X2202))
| ssPv2(skf1(X2202))
| ssPv3(skf1(skf1(X2202))) ),
inference(resolution,[status(thm)],[c4885,c45]) ).
cnf(c19360,plain,
( ssPv2(X3842)
| ssPv2(skf1(X3842))
| ~ ssPv3(skf1(X3842))
| ssPv3(X3842) ),
inference(resolution,[status(thm)],[c19348,c9]) ).
cnf(c19407,plain,
( ssPv2(skf1(X4290))
| ssPv2(skf1(skf1(X4290)))
| ssPv3(skf1(X4290))
| ssPv4(X4290)
| ssPv1(X4290) ),
inference(resolution,[status(thm)],[c19360,c4951]) ).
cnf(c23298,plain,
( ssPv2(skf1(X4291))
| ssPv2(skf1(skf1(X4291)))
| ssPv4(X4291)
| ssPv1(X4291) ),
inference(resolution,[status(thm)],[c19407,c309]) ).
cnf(c29758,plain,
( ~ ssPv4(skf1(skf1(X5226)))
| ~ ssPv1(skf1(X5226))
| ssPv4(X5226)
| ssPv2(skf1(X5226))
| ssPv1(X5226) ),
inference(resolution,[status(thm)],[c29684,c23298]) ).
cnf(c29841,plain,
( ~ ssPv1(skf1(X5228))
| ssPv4(X5228)
| ssPv2(skf1(X5228))
| ssPv1(X5228) ),
inference(resolution,[status(thm)],[c29758,c26401]) ).
cnf(c29904,plain,
( ssPv4(X5229)
| ssPv2(skf1(X5229))
| ssPv1(X5229) ),
inference(resolution,[status(thm)],[c29841,c21699]) ).
cnf(clause43,negated_conjecture,
( ~ ssRr(X619,X617)
| ~ ssPv4(X617)
| ~ ssRr(X620,X619)
| ~ ssRr(X621,X618)
| ~ ssRr(X620,X621)
| ~ ssRr(X620,X622)
| ~ ssPv4(X622)
| ssPv3(X618)
| ssPv1(X620) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(c405,plain,
( ~ ssRr(X2647,X2651)
| ~ ssPv4(X2651)
| ~ ssRr(X2649,X2647)
| ~ ssRr(X2648,X2650)
| ~ ssRr(X2649,X2648)
| ~ ssPv4(X2647)
| ssPv3(X2650)
| ssPv1(X2649) ),
inference(factor,[status(thm)],[clause43]) ).
cnf(c8723,plain,
( ~ ssRr(X4610,X4612)
| ~ ssPv4(X4612)
| ~ ssRr(X4611,X4610)
| ~ ssRr(X4610,X4613)
| ~ ssPv4(X4610)
| ssPv3(X4613)
| ssPv1(X4611) ),
inference(factor,[status(thm)],[c405]) ).
cnf(c25087,plain,
( ~ ssRr(X4614,X4615)
| ~ ssPv4(X4615)
| ~ ssRr(X4616,X4614)
| ~ ssPv4(X4614)
| ssPv3(X4615)
| ssPv1(X4616) ),
inference(factor,[status(thm)],[c8723]) ).
cnf(c25091,plain,
( ~ ssRr(skf1(X4623),X4624)
| ~ ssPv4(X4624)
| ~ ssPv4(skf1(X4623))
| ssPv3(X4624)
| ssPv1(X4623) ),
inference(resolution,[status(thm)],[c25087,clause1]) ).
cnf(c25092,plain,
( ~ ssPv4(skf1(skf1(X4629)))
| ~ ssPv4(skf1(X4629))
| ssPv3(skf1(skf1(X4629)))
| ssPv1(X4629) ),
inference(resolution,[status(thm)],[c25091,clause1]) ).
cnf(c26340,plain,
( ssPv3(skf1(skf1(X4779)))
| ssPv2(skf1(X4779))
| ~ ssPv4(skf1(X4779))
| ssPv1(X4779) ),
inference(resolution,[status(thm)],[c26268,c25092]) ).
cnf(c26787,plain,
( ssPv3(skf1(skf1(X4882)))
| ssPv2(skf1(X4882))
| ssPv1(X4882)
| ssPv1(skf1(skf1(X4882))) ),
inference(resolution,[status(thm)],[c26340,c7214]) ).
cnf(c27370,plain,
( ssPv3(skf1(skf1(X4883)))
| ssPv2(skf1(X4883))
| ssPv1(X4883)
| ssPv3(skf1(X4883)) ),
inference(resolution,[status(thm)],[c26787,c204]) ).
cnf(c27418,plain,
( ssPv2(skf1(X4889))
| ssPv1(X4889)
| ssPv3(skf1(X4889))
| ssPv2(skf1(skf1(X4889))) ),
inference(resolution,[status(thm)],[c27370,c22660]) ).
cnf(c27732,plain,
( ssPv2(skf1(X5035))
| ssPv1(X5035)
| ssPv3(skf1(X5035))
| ~ ssPv3(skf1(skf1(X5035)))
| ssPv3(X5035) ),
inference(resolution,[status(thm)],[c27418,c786]) ).
cnf(c29192,plain,
( ssPv2(skf1(X5036))
| ssPv1(X5036)
| ssPv3(skf1(X5036))
| ssPv3(X5036) ),
inference(resolution,[status(thm)],[c27732,c27370]) ).
cnf(clause20,negated_conjecture,
( ~ ssRr(X249,X247)
| ~ ssPv3(X247)
| ~ ssRr(X250,X249)
| ~ ssRr(X250,X251)
| ~ ssPv3(X251)
| ~ ssRr(X250,X248)
| ssPv1(X248)
| ssPv1(X250) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c140,plain,
( ~ ssRr(X708,X707)
| ~ ssPv3(X707)
| ~ ssRr(X709,X708)
| ~ ssRr(X709,X706)
| ~ ssPv3(X706)
| ssPv1(X708)
| ssPv1(X709) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c464,plain,
( ~ ssRr(X715,X714)
| ~ ssPv3(X714)
| ~ ssRr(X713,X715)
| ~ ssPv3(X715)
| ssPv1(X715)
| ssPv1(X713) ),
inference(factor,[status(thm)],[c140]) ).
cnf(c468,plain,
( ~ ssRr(skf1(X730),X731)
| ~ ssPv3(X731)
| ~ ssPv3(skf1(X730))
| ssPv1(skf1(X730))
| ssPv1(X730) ),
inference(resolution,[status(thm)],[c464,clause1]) ).
cnf(c480,plain,
( ~ ssPv3(skf1(skf1(X732)))
| ~ ssPv3(skf1(X732))
| ssPv1(skf1(X732))
| ssPv1(X732) ),
inference(resolution,[status(thm)],[c468,clause1]) ).
cnf(c372,plain,
( ~ ssPv4(X2457)
| ssPv3(skf1(skf1(X2457)))
| ssPv3(skf1(X2457))
| ssPv2(skf1(skf1(X2457)))
| ssPv1(skf1(X2457)) ),
inference(resolution,[status(thm)],[c363,c205]) ).
cnf(c6887,plain,
( ssPv3(skf1(skf1(X3539)))
| ssPv3(skf1(X3539))
| ssPv2(skf1(skf1(X3539)))
| ssPv1(skf1(X3539)) ),
inference(resolution,[status(thm)],[c372,c3422]) ).
cnf(c16363,plain,
( ssPv3(skf1(skf1(X3543)))
| ssPv3(skf1(X3543))
| ssPv1(skf1(X3543))
| ~ ssPv2(X3543)
| ssPv1(X3543) ),
inference(resolution,[status(thm)],[c6887,c747]) ).
cnf(c22930,plain,
( ssPv3(skf1(skf1(X4207)))
| ssPv3(skf1(X4207))
| ssPv1(skf1(X4207))
| ssPv1(X4207) ),
inference(resolution,[status(thm)],[c22877,c16363]) ).
cnf(clause12,negated_conjecture,
( ~ ssRr(X128,X126)
| ~ ssRr(X129,X128)
| ~ ssRr(X130,X127)
| ~ ssRr(X129,X130)
| ~ ssPv3(X129)
| ssPv4(X126)
| ssPv1(X127)
| ssPv4(X129) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c70,plain,
( ~ ssRr(X286,X287)
| ~ ssRr(X288,X286)
| ~ ssRr(X286,X285)
| ~ ssPv3(X288)
| ssPv4(X287)
| ssPv1(X285)
| ssPv4(X288) ),
inference(factor,[status(thm)],[clause12]) ).
cnf(c160,plain,
( ~ ssRr(X289,X290)
| ~ ssRr(X291,X289)
| ~ ssPv3(X291)
| ssPv4(X290)
| ssPv1(X290)
| ssPv4(X291) ),
inference(factor,[status(thm)],[c70]) ).
cnf(c164,plain,
( ~ ssRr(skf1(X298),X299)
| ~ ssPv3(X298)
| ssPv4(X299)
| ssPv1(X299)
| ssPv4(X298) ),
inference(resolution,[status(thm)],[c160,clause1]) ).
cnf(c169,plain,
( ~ ssPv3(X302)
| ssPv4(skf1(skf1(X302)))
| ssPv1(skf1(skf1(X302)))
| ssPv4(X302) ),
inference(resolution,[status(thm)],[c164,clause1]) ).
cnf(c7243,plain,
( ssPv4(X2530)
| ssPv3(skf1(X2530))
| ssPv1(skf1(skf1(X2530)))
| ssPv3(X2530) ),
inference(resolution,[status(thm)],[c7214,c15]) ).
cnf(c7381,plain,
( ssPv4(X2638)
| ssPv3(skf1(X2638))
| ssPv1(skf1(skf1(X2638)))
| ssPv4(skf1(skf1(X2638))) ),
inference(resolution,[status(thm)],[c7243,c169]) ).
cnf(c8543,plain,
( ssPv4(X2642)
| ssPv3(skf1(X2642))
| ssPv4(skf1(skf1(X2642)))
| ssPv1(X2642) ),
inference(resolution,[status(thm)],[c7381,c4132]) ).
cnf(c8640,plain,
( ssPv4(X2644)
| ssPv3(skf1(X2644))
| ssPv1(X2644)
| ~ ssPv2(skf1(X2644))
| ~ ssPv3(X2644) ),
inference(resolution,[status(thm)],[c8543,c76]) ).
cnf(c29978,plain,
( ssPv4(X5231)
| ssPv1(X5231)
| ssPv3(skf1(X5231))
| ~ ssPv3(X5231) ),
inference(resolution,[status(thm)],[c29904,c8640]) ).
cnf(c30141,plain,
( ssPv4(skf1(X5329))
| ssPv1(skf1(X5329))
| ssPv3(skf1(skf1(X5329)))
| ssPv1(X5329) ),
inference(resolution,[status(thm)],[c29978,c22930]) ).
cnf(c30761,plain,
( ssPv1(skf1(X5344))
| ssPv3(skf1(skf1(X5344)))
| ssPv1(X5344)
| ssPv2(skf1(X5344)) ),
inference(resolution,[status(thm)],[c30141,c26340]) ).
cnf(c30979,plain,
( ssPv1(skf1(X5349))
| ssPv1(X5349)
| ssPv2(skf1(X5349))
| ~ ssPv3(skf1(X5349)) ),
inference(resolution,[status(thm)],[c30761,c480]) ).
cnf(c31091,plain,
( ssPv1(skf1(X5350))
| ssPv1(X5350)
| ssPv2(skf1(X5350))
| ssPv3(X5350) ),
inference(resolution,[status(thm)],[c30979,c29192]) ).
cnf(clause9,negated_conjecture,
( ~ ssRr(X90,X89)
| ~ ssPv2(X89)
| ~ ssRr(X88,X90)
| ~ ssRr(X88,X87)
| ~ ssPv1(X87)
| ~ ssPv4(X88)
| ssPv3(X88) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c48,plain,
( ~ ssRr(X110,X109)
| ~ ssPv2(X109)
| ~ ssRr(X108,X110)
| ~ ssPv1(X110)
| ~ ssPv4(X108)
| ssPv3(X108) ),
inference(factor,[status(thm)],[clause9]) ).
cnf(c59,plain,
( ~ ssRr(skf1(X132),X133)
| ~ ssPv2(X133)
| ~ ssPv1(skf1(X132))
| ~ ssPv4(X132)
| ssPv3(X132) ),
inference(resolution,[status(thm)],[c48,clause1]) ).
cnf(c73,plain,
( ~ ssPv2(skf1(skf1(X134)))
| ~ ssPv1(skf1(X134))
| ~ ssPv4(X134)
| ssPv3(X134) ),
inference(resolution,[status(thm)],[c59,clause1]) ).
cnf(c22703,plain,
( ssPv2(skf1(skf1(X4152)))
| ssPv2(skf1(X4152))
| ssPv2(X4152) ),
inference(resolution,[status(thm)],[c22660,c22416]) ).
cnf(c29785,plain,
( ~ ssPv4(skf1(skf1(X5493)))
| ~ ssPv1(skf1(X5493))
| ssPv4(X5493)
| ssPv2(skf1(X5493))
| ssPv2(X5493) ),
inference(resolution,[status(thm)],[c29684,c22703]) ).
cnf(c31852,plain,
( ~ ssPv1(skf1(X5494))
| ssPv4(X5494)
| ssPv2(skf1(X5494))
| ssPv2(X5494) ),
inference(resolution,[status(thm)],[c29785,c26401]) ).
cnf(c31920,plain,
( ssPv4(X5495)
| ssPv2(skf1(X5495))
| ssPv2(X5495) ),
inference(resolution,[status(thm)],[c31852,c21699]) ).
cnf(c31982,plain,
( ssPv4(skf1(X5549))
| ssPv2(skf1(X5549))
| ~ ssPv1(skf1(X5549))
| ~ ssPv4(X5549)
| ssPv3(X5549) ),
inference(resolution,[status(thm)],[c31920,c73]) ).
cnf(c32354,plain,
( ssPv4(skf1(X5554))
| ssPv2(skf1(X5554))
| ~ ssPv4(X5554)
| ssPv3(X5554)
| ssPv1(X5554) ),
inference(resolution,[status(thm)],[c31982,c31091]) ).
cnf(c32419,plain,
( ssPv4(skf1(X5555))
| ssPv2(skf1(X5555))
| ssPv3(X5555)
| ssPv1(X5555) ),
inference(resolution,[status(thm)],[c32354,c29904]) ).
cnf(c32446,plain,
( ssPv2(skf1(X5556))
| ssPv3(X5556)
| ssPv1(X5556)
| ssPv3(skf1(skf1(X5556))) ),
inference(resolution,[status(thm)],[c32419,c26340]) ).
cnf(c32691,plain,
( ssPv2(skf1(X5696))
| ssPv3(X5696)
| ssPv3(skf1(skf1(X5696)))
| ssPv2(skf1(skf1(X5696))) ),
inference(resolution,[status(thm)],[c32446,c143]) ).
cnf(c33759,plain,
( ssPv2(skf1(X5712))
| ssPv3(X5712)
| ssPv3(skf1(skf1(X5712)))
| ~ ssPv1(X5712)
| ssPv4(X5712) ),
inference(resolution,[status(thm)],[c32691,c838]) ).
cnf(c33960,plain,
( ssPv2(skf1(X5713))
| ssPv3(X5713)
| ssPv3(skf1(skf1(X5713)))
| ssPv4(X5713) ),
inference(resolution,[status(thm)],[c33759,c29904]) ).
cnf(c34054,plain,
( ssPv2(skf1(X5728))
| ssPv3(skf1(skf1(X5728)))
| ssPv4(X5728)
| ssPv3(skf1(X5728)) ),
inference(resolution,[status(thm)],[c33960,c45]) ).
cnf(c34384,plain,
( ssPv2(skf1(X5736))
| ssPv4(X5736)
| ssPv3(skf1(X5736))
| ssPv2(skf1(skf1(X5736))) ),
inference(resolution,[status(thm)],[c34054,c22660]) ).
cnf(c34551,plain,
( ssPv2(skf1(X5737))
| ssPv4(X5737)
| ssPv2(skf1(skf1(X5737))) ),
inference(resolution,[status(thm)],[c34384,c309]) ).
cnf(c34677,plain,
( ssPv2(skf1(X5763))
| ssPv4(X5763)
| ~ ssPv4(skf1(skf1(X5763)))
| ~ ssPv1(skf1(X5763)) ),
inference(resolution,[status(thm)],[c34551,c29684]) ).
cnf(c35127,plain,
( ssPv2(skf1(X5766))
| ssPv4(X5766)
| ~ ssPv1(skf1(X5766)) ),
inference(resolution,[status(thm)],[c34677,c26401]) ).
cnf(c35191,plain,
( ssPv2(skf1(X5767))
| ssPv4(X5767) ),
inference(resolution,[status(thm)],[c35127,c21699]) ).
cnf(c35229,plain,
( ssPv4(skf1(X5768))
| ssPv2(X5768) ),
inference(resolution,[status(thm)],[c35191,c17509]) ).
cnf(c35219,plain,
( ssPv4(skf1(X5857))
| ~ ssPv2(X5857)
| ssPv3(skf1(skf1(X5857)))
| ssPv1(X5857) ),
inference(resolution,[status(thm)],[c35191,c747]) ).
cnf(c35483,plain,
( ssPv4(skf1(X5858))
| ssPv3(skf1(skf1(X5858)))
| ssPv1(X5858) ),
inference(resolution,[status(thm)],[c35219,c35229]) ).
cnf(c35240,plain,
( ssPv4(skf1(X5878))
| ~ ssPv3(skf1(skf1(X5878)))
| ssPv1(X5878)
| ssPv3(X5878) ),
inference(resolution,[status(thm)],[c35191,c786]) ).
cnf(c35885,plain,
( ssPv4(skf1(X5879))
| ssPv1(X5879)
| ssPv3(X5879) ),
inference(resolution,[status(thm)],[c35240,c35483]) ).
cnf(c35975,plain,
( ssPv4(skf1(skf1(X5919)))
| ssPv1(skf1(X5919))
| ~ ssPv4(X5919)
| ssPv1(X5919) ),
inference(resolution,[status(thm)],[c35885,c64]) ).
cnf(c26470,plain,
( ssPv4(skf1(skf1(X4758)))
| ssPv4(X4758)
| ssPv3(skf1(X4758)) ),
inference(resolution,[status(thm)],[c26401,c283]) ).
cnf(c33745,plain,
( ssPv2(skf1(X5698))
| ssPv3(X5698)
| ssPv2(skf1(skf1(X5698))) ),
inference(resolution,[status(thm)],[c32691,c22660]) ).
cnf(c33872,plain,
( ssPv2(skf1(X5699))
| ssPv3(X5699)
| ~ ssPv1(skf1(X5699))
| ~ ssPv4(X5699) ),
inference(resolution,[status(thm)],[c33745,c73]) ).
cnf(clause34,negated_conjecture,
( ~ ssRr(X465,X463)
| ~ ssRr(X466,X465)
| ~ ssRr(X467,X464)
| ~ ssRr(X466,X467)
| ~ ssRr(X466,X468)
| ~ ssPv2(X468)
| ssPv2(X463)
| ssPv1(X464)
| ssPv4(X466) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c300,plain,
( ~ ssRr(X1908,X1906)
| ~ ssRr(X1905,X1908)
| ~ ssRr(X1907,X1909)
| ~ ssRr(X1905,X1907)
| ~ ssPv2(X1908)
| ssPv2(X1906)
| ssPv1(X1909)
| ssPv4(X1905) ),
inference(factor,[status(thm)],[clause34]) ).
cnf(c4128,plain,
( ~ ssRr(X1984,X1985)
| ~ ssRr(X1982,X1984)
| ~ ssRr(X1984,X1983)
| ~ ssPv2(X1984)
| ssPv2(X1985)
| ssPv1(X1983)
| ssPv4(X1982) ),
inference(factor,[status(thm)],[c300]) ).
cnf(c4248,plain,
( ~ ssRr(X1986,X1987)
| ~ ssRr(X1988,X1986)
| ~ ssPv2(X1986)
| ssPv2(X1987)
| ssPv1(X1987)
| ssPv4(X1988) ),
inference(factor,[status(thm)],[c4128]) ).
cnf(c4252,plain,
( ~ ssRr(skf1(X1996),X1997)
| ~ ssPv2(skf1(X1996))
| ssPv2(X1997)
| ssPv1(X1997)
| ssPv4(X1996) ),
inference(resolution,[status(thm)],[c4248,clause1]) ).
cnf(c4254,plain,
( ~ ssPv2(skf1(X2003))
| ssPv2(skf1(skf1(X2003)))
| ssPv1(skf1(skf1(X2003)))
| ssPv4(X2003) ),
inference(resolution,[status(thm)],[c4252,clause1]) ).
cnf(c34625,plain,
( ssPv4(X5741)
| ssPv2(skf1(skf1(X5741)))
| ssPv1(skf1(skf1(X5741))) ),
inference(resolution,[status(thm)],[c34551,c4254]) ).
cnf(c34851,plain,
( ssPv4(X5965)
| ssPv2(skf1(skf1(X5965)))
| ssPv3(skf1(X5965))
| ~ ssPv4(skf1(X5965)) ),
inference(resolution,[status(thm)],[c34625,c33872]) ).
cnf(c36650,plain,
( ssPv4(X5966)
| ssPv2(skf1(skf1(X5966)))
| ssPv3(skf1(X5966)) ),
inference(resolution,[status(thm)],[c34851,c35191]) ).
cnf(c36708,plain,
( ssPv4(X6216)
| ssPv3(skf1(X6216))
| ~ ssPv4(skf1(skf1(X6216)))
| ~ ssPv1(skf1(X6216)) ),
inference(resolution,[status(thm)],[c36650,c29684]) ).
cnf(c37789,plain,
( ssPv4(X6217)
| ssPv3(skf1(X6217))
| ~ ssPv1(skf1(X6217)) ),
inference(resolution,[status(thm)],[c36708,c26470]) ).
cnf(c37809,plain,
( ssPv4(X6218)
| ssPv3(skf1(X6218)) ),
inference(resolution,[status(thm)],[c37789,c7214]) ).
cnf(c35232,plain,
( ssPv4(skf1(X6061))
| ~ ssPv4(skf1(skf1(X6061)))
| ~ ssPv1(skf1(X6061))
| ssPv4(X6061) ),
inference(resolution,[status(thm)],[c35191,c29684]) ).
cnf(c35215,plain,
( ssPv4(skf1(X5856))
| ~ ssPv1(X5856)
| ssPv3(skf1(skf1(X5856)))
| ssPv4(X5856) ),
inference(resolution,[status(thm)],[c35191,c838]) ).
cnf(c35580,plain,
( ssPv4(skf1(X5862))
| ssPv3(skf1(skf1(X5862)))
| ssPv4(X5862) ),
inference(resolution,[status(thm)],[c35483,c35215]) ).
cnf(c35759,plain,
( ssPv4(skf1(X6126))
| ssPv4(X6126)
| ~ ssPv1(skf1(X6126))
| ssPv4(skf1(skf1(X6126))) ),
inference(resolution,[status(thm)],[c35580,c15511]) ).
cnf(c37309,plain,
( ssPv4(skf1(X6127))
| ssPv4(X6127)
| ssPv4(skf1(skf1(X6127))) ),
inference(resolution,[status(thm)],[c35759,c9453]) ).
cnf(c37358,plain,
( ssPv4(skf1(X6128))
| ssPv4(X6128)
| ~ ssPv1(skf1(X6128)) ),
inference(resolution,[status(thm)],[c37309,c35232]) ).
cnf(c37384,plain,
( ssPv4(skf1(X6129))
| ssPv4(X6129) ),
inference(resolution,[status(thm)],[c37358,c9453]) ).
cnf(c37399,plain,
( ssPv4(skf1(X6147))
| ~ ssPv2(skf1(X6147))
| ~ ssPv3(X6147)
| ssPv1(X6147) ),
inference(resolution,[status(thm)],[c37384,c76]) ).
cnf(c37443,plain,
( ssPv4(skf1(skf1(X6344)))
| ~ ssPv3(skf1(X6344))
| ssPv1(skf1(X6344))
| ssPv4(X6344) ),
inference(resolution,[status(thm)],[c37399,c4520]) ).
cnf(c38512,plain,
( ssPv4(skf1(skf1(X6345)))
| ssPv1(skf1(X6345))
| ssPv4(X6345) ),
inference(resolution,[status(thm)],[c37443,c37809]) ).
cnf(c38577,plain,
( ssPv4(skf1(skf1(X6349)))
| ssPv1(skf1(X6349))
| ssPv1(X6349) ),
inference(resolution,[status(thm)],[c38512,c35975]) ).
cnf(c38615,plain,
( ssPv1(skf1(X6357))
| ssPv1(X6357)
| ~ ssPv2(skf1(X6357))
| ~ ssPv3(X6357) ),
inference(resolution,[status(thm)],[c38577,c76]) ).
cnf(c31962,plain,
( ssPv2(skf1(skf1(X5653)))
| ssPv2(skf1(X5653))
| ssPv3(skf1(skf1(X5653)))
| ssPv1(X5653) ),
inference(resolution,[status(thm)],[c31920,c26340]) ).
cnf(c33208,plain,
( ssPv2(skf1(X5656))
| ssPv3(skf1(skf1(X5656)))
| ssPv1(X5656)
| ~ ssPv2(X5656) ),
inference(resolution,[status(thm)],[c31962,c747]) ).
cnf(c33499,plain,
( ssPv2(skf1(X5657))
| ssPv3(skf1(skf1(X5657)))
| ssPv1(X5657) ),
inference(resolution,[status(thm)],[c33208,c22416]) ).
cnf(c35280,plain,
( ssPv2(X5820)
| ~ ssRr(X5819,X5821)
| ~ ssPv4(X5821)
| ~ ssRr(X5820,X5819)
| ~ ssPv3(X5819) ),
inference(resolution,[status(thm)],[c35229,c1039]) ).
cnf(c35360,plain,
( ssPv2(X5843)
| ~ ssRr(skf1(X5843),X5844)
| ~ ssPv4(X5844)
| ~ ssPv3(skf1(X5843)) ),
inference(resolution,[status(thm)],[c35280,clause1]) ).
cnf(c35395,plain,
( ssPv2(X5846)
| ~ ssPv4(skf1(skf1(X5846)))
| ~ ssPv3(skf1(X5846)) ),
inference(resolution,[status(thm)],[c35360,clause1]) ).
cnf(c35277,plain,
( ssPv2(X5815)
| ~ ssRr(X5814,X5816)
| ~ ssPv1(X5816)
| ~ ssRr(X5815,X5814)
| ~ ssPv3(X5814) ),
inference(resolution,[status(thm)],[c35229,c881]) ).
cnf(c35358,plain,
( ssPv2(X5838)
| ~ ssRr(skf1(X5838),X5839)
| ~ ssPv1(X5839)
| ~ ssPv3(skf1(X5838)) ),
inference(resolution,[status(thm)],[c35277,clause1]) ).
cnf(c35366,plain,
( ssPv2(X5840)
| ~ ssPv1(skf1(skf1(X5840)))
| ~ ssPv3(skf1(X5840)) ),
inference(resolution,[status(thm)],[c35358,clause1]) ).
cnf(c38535,plain,
( ssPv1(skf1(X6351))
| ssPv4(X6351)
| ssPv2(X6351)
| ~ ssPv3(skf1(X6351)) ),
inference(resolution,[status(thm)],[c38512,c35395]) ).
cnf(c38693,plain,
( ssPv1(skf1(X6352))
| ssPv4(X6352)
| ssPv2(X6352) ),
inference(resolution,[status(thm)],[c38535,c37809]) ).
cnf(c38768,plain,
( ssPv1(skf1(X6401))
| ssPv4(X6401)
| ssPv3(skf1(skf1(X6401)))
| ssPv1(X6401) ),
inference(resolution,[status(thm)],[c38693,c3220]) ).
cnf(c39677,plain,
( ssPv1(skf1(X6406))
| ssPv4(X6406)
| ssPv3(skf1(skf1(X6406))) ),
inference(resolution,[status(thm)],[c38768,c3221]) ).
cnf(c39807,plain,
( ssPv1(skf1(X6407))
| ssPv4(X6407) ),
inference(resolution,[status(thm)],[c39677,c7133]) ).
cnf(c39861,plain,
( ssPv4(X6408)
| ssPv1(skf1(skf1(X6408)))
| ssPv3(X6408) ),
inference(resolution,[status(thm)],[c39807,c15]) ).
cnf(c56,plain,
( ~ ssRr(X225,X223)
| ~ ssPv4(X223)
| ~ ssRr(X224,X225)
| ~ ssPv2(skf1(X224))
| ~ ssPv3(X224)
| ssPv1(X224) ),
inference(resolution,[status(thm)],[clause10,clause1]) ).
cnf(c29990,plain,
( ssPv4(X5287)
| ssPv1(X5287)
| ~ ssRr(X5288,X5289)
| ~ ssPv4(X5289)
| ~ ssRr(X5287,X5288)
| ~ ssPv3(X5287) ),
inference(resolution,[status(thm)],[c29904,c56]) ).
cnf(c30344,plain,
( ssPv4(X5291)
| ssPv1(X5291)
| ~ ssRr(skf1(X5291),X5292)
| ~ ssPv4(X5292)
| ~ ssPv3(X5291) ),
inference(resolution,[status(thm)],[c29990,clause1]) ).
cnf(c30345,plain,
( ssPv4(X5293)
| ssPv1(X5293)
| ~ ssPv4(skf1(skf1(X5293)))
| ~ ssPv3(X5293) ),
inference(resolution,[status(thm)],[c30344,clause1]) ).
cnf(c39951,plain,
( ssPv4(X6449)
| ssPv1(skf1(skf1(X6449)))
| ssPv4(skf1(skf1(X6449))) ),
inference(resolution,[status(thm)],[c39861,c169]) ).
cnf(c40094,plain,
( ssPv4(X6450)
| ssPv1(skf1(skf1(X6450)))
| ssPv1(X6450)
| ~ ssPv3(X6450) ),
inference(resolution,[status(thm)],[c39951,c30345]) ).
cnf(c40108,plain,
( ssPv4(X6451)
| ssPv1(skf1(skf1(X6451)))
| ssPv1(X6451) ),
inference(resolution,[status(thm)],[c40094,c39861]) ).
cnf(c40169,plain,
( ssPv4(X6452)
| ssPv1(X6452)
| ssPv2(X6452)
| ~ ssPv3(skf1(X6452)) ),
inference(resolution,[status(thm)],[c40108,c35366]) ).
cnf(c40202,plain,
( ssPv4(X6453)
| ssPv1(X6453)
| ssPv2(X6453) ),
inference(resolution,[status(thm)],[c40169,c37809]) ).
cnf(clause29,negated_conjecture,
( ~ ssRr(X382,X380)
| ~ ssPv3(X380)
| ~ ssRr(X383,X382)
| ~ ssRr(X383,X384)
| ~ ssPv4(X384)
| ~ ssRr(X383,X381)
| ~ ssPv3(X381)
| ~ ssPv1(X383) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c241,plain,
( ~ ssRr(X1155,X1154)
| ~ ssPv3(X1154)
| ~ ssRr(X1156,X1155)
| ~ ssRr(X1156,X1157)
| ~ ssPv4(X1157)
| ~ ssPv3(X1155)
| ~ ssPv1(X1156) ),
inference(factor,[status(thm)],[clause29]) ).
cnf(c1213,plain,
( ~ ssRr(X1166,X1165)
| ~ ssPv3(X1165)
| ~ ssRr(X1164,X1166)
| ~ ssPv4(skf1(X1164))
| ~ ssPv3(X1166)
| ~ ssPv1(X1164) ),
inference(resolution,[status(thm)],[c241,clause1]) ).
cnf(c35288,plain,
( ssPv2(X6089)
| ~ ssRr(X6091,X6090)
| ~ ssPv3(X6090)
| ~ ssRr(X6089,X6091)
| ~ ssPv3(X6091)
| ~ ssPv1(X6089) ),
inference(resolution,[status(thm)],[c35229,c1213]) ).
cnf(c37270,plain,
( ssPv2(X6312)
| ~ ssRr(skf1(X6312),X6313)
| ~ ssPv3(X6313)
| ~ ssPv3(skf1(X6312))
| ~ ssPv1(X6312) ),
inference(resolution,[status(thm)],[c35288,clause1]) ).
cnf(c38435,plain,
( ssPv2(X6314)
| ~ ssPv3(skf1(skf1(X6314)))
| ~ ssPv3(skf1(X6314))
| ~ ssPv1(X6314) ),
inference(resolution,[status(thm)],[c37270,clause1]) ).
cnf(c40241,plain,
( ssPv4(X6457)
| ssPv2(X6457)
| ssPv3(skf1(skf1(X6457))) ),
inference(resolution,[status(thm)],[c40202,c11439]) ).
cnf(c40340,plain,
( ssPv4(X6459)
| ssPv2(X6459)
| ~ ssPv3(skf1(X6459))
| ~ ssPv1(X6459) ),
inference(resolution,[status(thm)],[c40241,c38435]) ).
cnf(c40364,plain,
( ssPv4(X6460)
| ssPv2(X6460)
| ~ ssPv1(X6460) ),
inference(resolution,[status(thm)],[c40340,c37809]) ).
cnf(c40391,plain,
( ssPv4(X6461)
| ssPv2(X6461) ),
inference(resolution,[status(thm)],[c40364,c40202]) ).
cnf(c40422,plain,
( ssPv4(skf1(X6463))
| ~ ssPv3(X6463)
| ssPv1(X6463) ),
inference(resolution,[status(thm)],[c40391,c37399]) ).
cnf(c40455,plain,
( ssPv4(skf1(X6464))
| ssPv1(X6464) ),
inference(resolution,[status(thm)],[c40422,c35885]) ).
cnf(c40471,plain,
( ssPv1(skf1(X6470))
| ssPv2(X6470)
| ~ ssPv3(skf1(X6470)) ),
inference(resolution,[status(thm)],[c40455,c35395]) ).
cnf(c40510,plain,
( ssPv1(skf1(skf1(X6484)))
| ssPv2(skf1(X6484))
| ssPv1(X6484) ),
inference(resolution,[status(thm)],[c40471,c33499]) ).
cnf(c40629,plain,
( ssPv2(skf1(X6485))
| ssPv1(X6485)
| ssPv3(skf1(X6485)) ),
inference(resolution,[status(thm)],[c40510,c204]) ).
cnf(c40752,plain,
( ssPv2(skf1(X6490))
| ssPv1(X6490)
| ssPv1(skf1(X6490)) ),
inference(resolution,[status(thm)],[c40629,c30979]) ).
cnf(c40828,plain,
( ssPv1(X6491)
| ssPv1(skf1(X6491))
| ~ ssPv3(X6491) ),
inference(resolution,[status(thm)],[c40752,c38615]) ).
cnf(c38624,plain,
( ssPv1(skf1(X6381))
| ssPv1(X6381)
| ssPv3(skf1(skf1(X6381)))
| ssPv2(X6381) ),
inference(resolution,[status(thm)],[c38577,c340]) ).
cnf(c39274,plain,
( ssPv1(skf1(X6383))
| ssPv3(skf1(skf1(X6383)))
| ssPv2(X6383) ),
inference(resolution,[status(thm)],[c38624,c11439]) ).
cnf(c40685,plain,
( ssPv1(skf1(X6731))
| ssPv3(skf1(skf1(X6731)))
| ~ ssPv2(X6731)
| ssPv1(X6731) ),
inference(resolution,[status(thm)],[c40629,c747]) ).
cnf(c42178,plain,
( ssPv1(skf1(X6732))
| ssPv3(skf1(skf1(X6732)))
| ssPv1(X6732) ),
inference(resolution,[status(thm)],[c40685,c39274]) ).
cnf(c32730,plain,
( ssPv2(skf1(X5559))
| ssPv3(X5559)
| ssPv1(X5559)
| ssPv2(skf1(skf1(X5559))) ),
inference(resolution,[status(thm)],[c32446,c22660]) ).
cnf(c32888,plain,
( ssPv2(skf1(X5560))
| ssPv3(X5560)
| ssPv1(X5560)
| ~ ssPv3(skf1(skf1(X5560))) ),
inference(resolution,[status(thm)],[c32730,c786]) ).
cnf(c32927,plain,
( ssPv2(skf1(X5561))
| ssPv3(X5561)
| ssPv1(X5561) ),
inference(resolution,[status(thm)],[c32888,c32446]) ).
cnf(c42234,plain,
( ssPv1(skf1(X6733))
| ssPv1(X6733)
| ~ ssPv3(skf1(X6733)) ),
inference(resolution,[status(thm)],[c42178,c480]) ).
cnf(c42264,plain,
( ssPv1(skf1(X6738))
| ssPv1(X6738)
| ssPv2(skf1(skf1(X6738))) ),
inference(resolution,[status(thm)],[c42234,c32927]) ).
cnf(c42344,plain,
( ssPv1(skf1(X6808))
| ssPv1(X6808)
| ~ ssPv3(skf1(skf1(X6808)))
| ssPv3(X6808) ),
inference(resolution,[status(thm)],[c42264,c786]) ).
cnf(c42525,plain,
( ssPv1(skf1(X6809))
| ssPv1(X6809)
| ssPv3(X6809) ),
inference(resolution,[status(thm)],[c42344,c42178]) ).
cnf(c42582,plain,
( ssPv1(skf1(X6813))
| ssPv1(X6813) ),
inference(resolution,[status(thm)],[c42525,c40828]) ).
cnf(c39854,plain,
( ssPv4(skf1(X7090))
| ~ ssPv3(skf1(skf1(X7090)))
| ~ ssPv1(X7090)
| ssPv3(skf1(X7090)) ),
inference(resolution,[status(thm)],[c39807,c25511]) ).
cnf(c43184,plain,
( ssPv4(skf1(X7091))
| ~ ssPv1(X7091)
| ssPv3(skf1(X7091)) ),
inference(resolution,[status(thm)],[c39854,c37809]) ).
cnf(c43208,plain,
( ssPv4(skf1(X7093))
| ssPv3(skf1(X7093)) ),
inference(resolution,[status(thm)],[c43184,c40455]) ).
cnf(c43240,plain,
( ssPv3(skf1(skf1(X7095)))
| ssPv1(X7095)
| ssPv2(X7095) ),
inference(resolution,[status(thm)],[c43208,c340]) ).
cnf(c43306,plain,
( ssPv3(skf1(skf1(X7096)))
| ssPv2(X7096) ),
inference(resolution,[status(thm)],[c43240,c11439]) ).
cnf(c43346,plain,
( ssPv2(X7097)
| ~ ssPv3(skf1(X7097))
| ~ ssPv1(X7097) ),
inference(resolution,[status(thm)],[c43306,c38435]) ).
cnf(c43391,plain,
( ssPv2(skf1(X7106))
| ~ ssPv1(skf1(X7106))
| ssPv1(X7106) ),
inference(resolution,[status(thm)],[c43346,c33499]) ).
cnf(c43410,plain,
( ssPv2(skf1(X7107))
| ssPv1(X7107) ),
inference(resolution,[status(thm)],[c43391,c42582]) ).
cnf(c43252,plain,
( ssPv4(skf1(skf1(X7130)))
| ~ ssPv1(skf1(X7130))
| ssPv4(X7130) ),
inference(resolution,[status(thm)],[c43208,c15511]) ).
cnf(c43556,plain,
( ssPv4(skf1(skf1(X7131)))
| ssPv4(X7131) ),
inference(resolution,[status(thm)],[c43252,c40455]) ).
cnf(c35216,plain,
( ssPv4(skf1(X5787))
| ~ ssPv1(skf1(X5787))
| ~ ssPv4(X5787)
| ssPv3(X5787) ),
inference(resolution,[status(thm)],[c35191,c73]) ).
cnf(c43565,plain,
( ssPv4(X7133)
| ssPv1(X7133)
| ~ ssPv3(X7133) ),
inference(resolution,[status(thm)],[c43556,c30345]) ).
cnf(c43588,plain,
( ssPv4(skf1(X7136))
| ssPv1(skf1(X7136)) ),
inference(resolution,[status(thm)],[c43565,c43208]) ).
cnf(c43655,plain,
( ssPv4(skf1(X7140))
| ~ ssPv4(X7140)
| ssPv3(X7140) ),
inference(resolution,[status(thm)],[c43588,c35216]) ).
cnf(c43662,plain,
( ssPv4(skf1(X7141))
| ssPv3(X7141) ),
inference(resolution,[status(thm)],[c43655,c37384]) ).
cnf(c43707,plain,
( ssPv4(skf1(skf1(X7157)))
| ~ ssPv4(X7157)
| ssPv1(X7157) ),
inference(resolution,[status(thm)],[c43662,c64]) ).
cnf(c43732,plain,
( ssPv4(skf1(skf1(X7158)))
| ssPv1(X7158) ),
inference(resolution,[status(thm)],[c43707,c43556]) ).
cnf(c43741,plain,
( ssPv1(X7167)
| ~ ssPv2(skf1(X7167))
| ~ ssPv3(X7167) ),
inference(resolution,[status(thm)],[c43732,c76]) ).
cnf(c43802,plain,
( ssPv1(X7171)
| ~ ssPv3(X7171) ),
inference(resolution,[status(thm)],[c43741,c43410]) ).
cnf(c43234,plain,
( ssPv3(skf1(skf1(X7118)))
| ~ ssPv4(skf1(X7118))
| ssPv1(X7118) ),
inference(resolution,[status(thm)],[c43208,c25092]) ).
cnf(c43506,plain,
( ssPv3(skf1(skf1(X7121)))
| ssPv1(X7121) ),
inference(resolution,[status(thm)],[c43234,c37809]) ).
cnf(c43551,plain,
( ssPv3(skf1(skf1(X7304)))
| ssPv2(skf1(skf1(X7304)))
| ssPv3(X7304) ),
inference(resolution,[status(thm)],[c43506,c143]) ).
cnf(c43957,plain,
( ssPv3(skf1(skf1(X7306)))
| ssPv3(X7306)
| ~ ssPv1(X7306)
| ssPv4(X7306) ),
inference(resolution,[status(thm)],[c43551,c838]) ).
cnf(c43984,plain,
( ssPv3(skf1(skf1(X7307)))
| ssPv3(X7307)
| ssPv4(X7307) ),
inference(resolution,[status(thm)],[c43957,c43506]) ).
cnf(clause45,negated_conjecture,
( ~ ssRr(X653,X651)
| ~ ssPv3(X651)
| ~ ssRr(X654,X653)
| ~ ssRr(X655,X652)
| ~ ssRr(X654,X655)
| ~ ssRr(X654,X656)
| ~ ssPv3(X656)
| ~ ssPv2(X654)
| ssPv2(X652) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
cnf(c429,plain,
( ~ ssRr(X2786,X2783)
| ~ ssPv3(X2783)
| ~ ssRr(X2784,X2786)
| ~ ssRr(X2787,X2785)
| ~ ssRr(X2784,X2787)
| ~ ssPv3(X2786)
| ~ ssPv2(X2784)
| ssPv2(X2785) ),
inference(factor,[status(thm)],[clause45]) ).
cnf(c10259,plain,
( ~ ssRr(X5117,X5119)
| ~ ssPv3(X5119)
| ~ ssRr(X5120,X5117)
| ~ ssRr(X5117,X5118)
| ~ ssPv3(X5117)
| ~ ssPv2(X5120)
| ssPv2(X5118) ),
inference(factor,[status(thm)],[c429]) ).
cnf(c29413,plain,
( ~ ssRr(X5122,X5123)
| ~ ssPv3(X5123)
| ~ ssRr(X5121,X5122)
| ~ ssPv3(X5122)
| ~ ssPv2(X5121)
| ssPv2(X5123) ),
inference(factor,[status(thm)],[c10259]) ).
cnf(c29417,plain,
( ~ ssRr(skf1(X5128),X5129)
| ~ ssPv3(X5129)
| ~ ssPv3(skf1(X5128))
| ~ ssPv2(X5128)
| ssPv2(X5129) ),
inference(resolution,[status(thm)],[c29413,clause1]) ).
cnf(c29418,plain,
( ~ ssPv3(skf1(skf1(X5134)))
| ~ ssPv3(skf1(X5134))
| ~ ssPv2(X5134)
| ssPv2(skf1(skf1(X5134))) ),
inference(resolution,[status(thm)],[c29417,clause1]) ).
cnf(c43535,plain,
( ssPv1(X7408)
| ~ ssPv3(skf1(X7408))
| ~ ssPv2(X7408)
| ssPv2(skf1(skf1(X7408))) ),
inference(resolution,[status(thm)],[c43506,c29418]) ).
cnf(c44086,plain,
( ssPv1(X7409)
| ~ ssPv2(X7409)
| ssPv2(skf1(skf1(X7409)))
| ssPv4(X7409) ),
inference(resolution,[status(thm)],[c43535,c37809]) ).
cnf(c44098,plain,
( ssPv1(X7410)
| ssPv2(skf1(skf1(X7410)))
| ssPv4(X7410) ),
inference(resolution,[status(thm)],[c44086,c40391]) ).
cnf(c44134,plain,
( ssPv1(X7417)
| ssPv4(X7417)
| ~ ssPv3(skf1(skf1(X7417)))
| ssPv3(X7417) ),
inference(resolution,[status(thm)],[c44098,c786]) ).
cnf(c44180,plain,
( ssPv1(X7418)
| ssPv4(X7418)
| ssPv3(X7418) ),
inference(resolution,[status(thm)],[c44134,c43984]) ).
cnf(c44205,plain,
( ssPv1(X7422)
| ssPv4(X7422) ),
inference(resolution,[status(thm)],[c44180,c43802]) ).
cnf(c43688,plain,
( ssPv4(skf1(skf1(X7154)))
| ssPv2(X7154)
| ~ ssPv1(X7154) ),
inference(resolution,[status(thm)],[c43662,c43346]) ).
cnf(c43751,plain,
( ssPv4(skf1(skf1(X7159)))
| ssPv2(X7159) ),
inference(resolution,[status(thm)],[c43732,c43688]) ).
cnf(c43767,plain,
( ssPv2(X7160)
| ~ ssPv3(skf1(X7160)) ),
inference(resolution,[status(thm)],[c43751,c35395]) ).
cnf(c43945,plain,
( ssPv2(skf1(skf1(X7370)))
| ssPv3(X7370)
| ssPv1(skf1(skf1(X7370))) ),
inference(resolution,[status(thm)],[c43551,c43802]) ).
cnf(c43809,plain,
( ssPv1(skf1(skf1(X7178)))
| ssPv2(X7178) ),
inference(resolution,[status(thm)],[c43802,c43306]) ).
cnf(c43821,plain,
( ssPv2(X7452)
| ~ ssPv3(skf1(skf1(X7452)))
| ~ ssPv1(X7452)
| ssPv3(skf1(X7452)) ),
inference(resolution,[status(thm)],[c43809,c25511]) ).
cnf(c44280,plain,
( ssPv2(X7454)
| ~ ssPv1(X7454)
| ssPv3(skf1(X7454)) ),
inference(resolution,[status(thm)],[c43821,c43306]) ).
cnf(c44297,plain,
( ssPv2(skf1(skf1(X7612)))
| ssPv3(skf1(skf1(skf1(X7612))))
| ssPv3(X7612) ),
inference(resolution,[status(thm)],[c44280,c43945]) ).
cnf(c44517,plain,
( ssPv2(skf1(skf1(X7614)))
| ssPv3(X7614) ),
inference(resolution,[status(thm)],[c44297,c43767]) ).
cnf(c44541,plain,
( ssPv3(X7616)
| ~ ssPv1(skf1(X7616))
| ~ ssPv4(X7616) ),
inference(resolution,[status(thm)],[c44517,c73]) ).
cnf(c44597,plain,
( ssPv3(X7631)
| ~ ssPv4(X7631)
| ssPv1(X7631) ),
inference(resolution,[status(thm)],[c44541,c42582]) ).
cnf(c44708,plain,
( ssPv3(X7632)
| ssPv1(X7632) ),
inference(resolution,[status(thm)],[c44597,c44205]) ).
cnf(c44723,plain,
ssPv1(X7633),
inference(resolution,[status(thm)],[c44708,c43802]) ).
cnf(c37407,plain,
( ssPv4(X6330)
| ~ ssRr(X6332,X6331)
| ~ ssPv3(X6331)
| ~ ssRr(X6330,X6332)
| ~ ssPv3(X6332)
| ~ ssPv1(X6330) ),
inference(resolution,[status(thm)],[c37384,c1213]) ).
cnf(c38461,plain,
( ssPv4(X6975)
| ~ ssRr(skf1(X6975),X6976)
| ~ ssPv3(X6976)
| ~ ssPv3(skf1(X6975))
| ~ ssPv1(X6975) ),
inference(resolution,[status(thm)],[c37407,clause1]) ).
cnf(c42977,plain,
( ssPv4(X6977)
| ~ ssPv3(skf1(skf1(X6977)))
| ~ ssPv3(skf1(X6977))
| ~ ssPv1(X6977) ),
inference(resolution,[status(thm)],[c38461,clause1]) ).
cnf(c44004,plain,
( ssPv3(X7313)
| ssPv4(X7313)
| ~ ssPv3(skf1(X7313))
| ~ ssPv1(X7313) ),
inference(resolution,[status(thm)],[c43984,c42977]) ).
cnf(c44026,plain,
( ssPv3(X7314)
| ssPv4(X7314)
| ~ ssPv1(X7314) ),
inference(resolution,[status(thm)],[c44004,c37809]) ).
cnf(c44195,plain,
( ssPv4(X7419)
| ssPv3(X7419) ),
inference(resolution,[status(thm)],[c44180,c44026]) ).
cnf(c44739,plain,
( ssPv3(X7636)
| ~ ssPv4(X7636) ),
inference(resolution,[status(thm)],[c44723,c44541]) ).
cnf(c44746,plain,
ssPv3(X7637),
inference(resolution,[status(thm)],[c44739,c44195]) ).
cnf(c44752,plain,
( ssPv4(X7664)
| ~ ssPv3(skf1(X7664))
| ~ ssPv1(X7664) ),
inference(resolution,[status(thm)],[c44746,c42977]) ).
cnf(c44754,plain,
( ssPv4(X7665)
| ~ ssPv1(X7665) ),
inference(resolution,[status(thm)],[c44752,c44746]) ).
cnf(c44755,plain,
ssPv4(X7666),
inference(resolution,[status(thm)],[c44754,c44723]) ).
cnf(c1212,plain,
( ~ ssRr(X1162,X1160)
| ~ ssPv3(X1160)
| ~ ssRr(X1161,X1162)
| ~ ssPv4(X1162)
| ~ ssPv3(X1162)
| ~ ssPv1(X1161) ),
inference(factor,[status(thm)],[c241]) ).
cnf(c1215,plain,
( ~ ssRr(skf1(X1171),X1172)
| ~ ssPv3(X1172)
| ~ ssPv4(skf1(X1171))
| ~ ssPv3(skf1(X1171))
| ~ ssPv1(X1171) ),
inference(resolution,[status(thm)],[c1212,clause1]) ).
cnf(c1224,plain,
( ~ ssPv3(skf1(skf1(X1173)))
| ~ ssPv4(skf1(X1173))
| ~ ssPv3(skf1(X1173))
| ~ ssPv1(X1173) ),
inference(resolution,[status(thm)],[c1215,clause1]) ).
cnf(c44751,plain,
( ~ ssPv4(skf1(X7702))
| ~ ssPv3(skf1(X7702))
| ~ ssPv1(X7702) ),
inference(resolution,[status(thm)],[c44746,c1224]) ).
cnf(c44759,plain,
( ~ ssPv4(skf1(X7703))
| ~ ssPv1(X7703) ),
inference(resolution,[status(thm)],[c44751,c44746]) ).
cnf(c44760,plain,
~ ssPv1(X7704),
inference(resolution,[status(thm)],[c44759,c44755]) ).
cnf(c44761,plain,
$false,
inference(resolution,[status(thm)],[c44760,c44723]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN759-1 : TPTP v8.1.2. Released v2.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n004.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 19:47:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 45.29/45.50 % Version: 1.5
% 45.29/45.50 % SZS status Unsatisfiable
% 45.29/45.50 % SZS output start CNFRefutation
% See solution above
% 45.34/45.51
% 45.34/45.51 % Initial clauses : 51
% 45.34/45.51 % Processed clauses : 1552
% 45.34/45.51 % Factors computed : 1108
% 45.34/45.51 % Resolvents computed: 43654
% 45.34/45.51 % Tautologies deleted: 572
% 45.34/45.51 % Forward subsumed : 3009
% 45.34/45.51 % Backward subsumed : 1546
% 45.34/45.51 % -------- CPU Time ---------
% 45.34/45.51 % User time : 45.007 s
% 45.34/45.51 % System time : 0.156 s
% 45.34/45.51 % Total time : 45.163 s
%------------------------------------------------------------------------------