%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN738-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:46 EDT 2024
% Result : Satisfiable 0.42s 0.62s
% Output : Saturation 0.42s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssRr(X2,skf1(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause21,negated_conjecture,
( ~ ssRr(X158,X157)
| ~ ssPv3(X157)
| ~ ssRr(X158,X156)
| ~ ssPv1(X156)
| ~ ssRr(X158,X155)
| ~ ssPv7(X158)
| ssPv7(X155) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c67,plain,
( ~ ssRr(X215,X216)
| ~ ssPv3(X216)
| ~ ssRr(X215,X217)
| ~ ssPv1(X217)
| ~ ssPv7(X215)
| ssPv7(X217) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c94,plain,
( ~ ssRr(X239,X240)
| ~ ssPv3(X240)
| ~ ssPv1(skf1(X239))
| ~ ssPv7(X239)
| ssPv7(skf1(X239)) ),
inference(resolution,[status(thm)],[c67,clause1]) ).
cnf(clause20,negated_conjecture,
( ~ ssRr(X145,X144)
| ~ ssPv6(X144)
| ~ ssRr(X145,X143)
| ~ ssPv3(X143)
| ~ ssRr(X145,X142)
| ~ ssPv4(X145)
| ssPv5(X142) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c60,plain,
( ~ ssRr(X192,X190)
| ~ ssPv6(X190)
| ~ ssRr(X192,X191)
| ~ ssPv3(X191)
| ~ ssPv4(X192)
| ssPv5(X191) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c83,plain,
( ~ ssRr(X233,X234)
| ~ ssPv6(X234)
| ~ ssPv3(skf1(X233))
| ~ ssPv4(X233)
| ssPv5(skf1(X233)) ),
inference(resolution,[status(thm)],[c60,clause1]) ).
cnf(clause19,negated_conjecture,
( ~ ssRr(X128,X127)
| ~ ssPv5(X127)
| ~ ssRr(X128,X126)
| ~ ssRr(X128,X125)
| ~ ssPv5(X128)
| ssPv6(X126)
| ssPv4(X125) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c53,plain,
( ~ ssRr(X161,X159)
| ~ ssPv5(X159)
| ~ ssRr(X161,X160)
| ~ ssPv5(X161)
| ssPv6(X160)
| ssPv4(X160) ),
inference(factor,[status(thm)],[clause19]) ).
cnf(c70,plain,
( ~ ssRr(X226,X227)
| ~ ssPv5(X227)
| ~ ssPv5(X226)
| ssPv6(skf1(X226))
| ssPv4(skf1(X226)) ),
inference(resolution,[status(thm)],[c53,clause1]) ).
cnf(c68,plain,
( ~ ssRr(X219,X218)
| ~ ssPv3(X218)
| ~ ssRr(X219,X220)
| ~ ssPv1(X220)
| ~ ssPv7(X219)
| ssPv7(skf1(X219)) ),
inference(resolution,[status(thm)],[clause21,clause1]) ).
cnf(c95,plain,
( ~ ssRr(X223,X224)
| ~ ssPv3(X224)
| ~ ssPv1(X224)
| ~ ssPv7(X223)
| ssPv7(skf1(X223)) ),
inference(factor,[status(thm)],[c68]) ).
cnf(c61,plain,
( ~ ssRr(X207,X208)
| ~ ssPv6(X208)
| ~ ssRr(X207,X206)
| ~ ssPv3(X206)
| ~ ssPv4(X207)
| ssPv5(skf1(X207)) ),
inference(resolution,[status(thm)],[clause20,clause1]) ).
cnf(c90,plain,
( ~ ssRr(X212,X213)
| ~ ssPv6(X213)
| ~ ssPv3(X213)
| ~ ssPv4(X212)
| ssPv5(skf1(X212)) ),
inference(factor,[status(thm)],[c61]) ).
cnf(c66,plain,
( ~ ssRr(X201,X203)
| ~ ssPv3(X203)
| ~ ssRr(X201,X202)
| ~ ssPv1(X202)
| ~ ssPv7(X201)
| ssPv7(X203) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c87,plain,
( ~ ssRr(X205,X204)
| ~ ssPv3(X204)
| ~ ssPv1(X204)
| ~ ssPv7(X205)
| ssPv7(X204) ),
inference(factor,[status(thm)],[c66]) ).
cnf(c89,plain,
( ~ ssPv3(skf1(X211))
| ~ ssPv1(skf1(X211))
| ~ ssPv7(X211)
| ssPv7(skf1(X211)) ),
inference(resolution,[status(thm)],[c87,clause1]) ).
cnf(c88,plain,
( ~ ssRr(X209,X210)
| ~ ssPv3(X210)
| ~ ssPv1(skf1(X209))
| ~ ssPv7(X209)
| ssPv7(X210) ),
inference(resolution,[status(thm)],[c66,clause1]) ).
cnf(c54,plain,
( ~ ssRr(X194,X193)
| ~ ssPv5(X193)
| ~ ssRr(X194,X195)
| ~ ssPv5(X194)
| ssPv6(X195)
| ssPv4(skf1(X194)) ),
inference(resolution,[status(thm)],[clause19,clause1]) ).
cnf(c84,plain,
( ~ ssRr(X199,X198)
| ~ ssPv5(X198)
| ~ ssPv5(X199)
| ssPv6(X198)
| ssPv4(skf1(X199)) ),
inference(factor,[status(thm)],[c54]) ).
cnf(clause18,negated_conjecture,
( ~ ssRr(X115,X114)
| ~ ssPv6(X114)
| ~ ssRr(X115,X113)
| ~ ssRr(X115,X112)
| ~ ssPv3(X115)
| ssPv8(X113)
| ssPv6(X112) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c47,plain,
( ~ ssRr(X181,X183)
| ~ ssPv6(X183)
| ~ ssRr(X181,X182)
| ~ ssPv3(X181)
| ssPv8(X182)
| ssPv6(skf1(X181)) ),
inference(resolution,[status(thm)],[clause18,clause1]) ).
cnf(c79,plain,
( ~ ssRr(X188,X187)
| ~ ssPv6(X187)
| ~ ssPv3(X188)
| ssPv8(X187)
| ssPv6(skf1(X188)) ),
inference(factor,[status(thm)],[c47]) ).
cnf(c59,plain,
( ~ ssRr(X178,X177)
| ~ ssPv6(X177)
| ~ ssRr(X178,X176)
| ~ ssPv3(X176)
| ~ ssPv4(X178)
| ssPv5(X177) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c76,plain,
( ~ ssRr(X179,X180)
| ~ ssPv6(X180)
| ~ ssPv3(X180)
| ~ ssPv4(X179)
| ssPv5(X180) ),
inference(factor,[status(thm)],[c59]) ).
cnf(c78,plain,
( ~ ssPv6(skf1(X186))
| ~ ssPv3(skf1(X186))
| ~ ssPv4(X186)
| ssPv5(skf1(X186)) ),
inference(resolution,[status(thm)],[c76,clause1]) ).
cnf(c77,plain,
( ~ ssRr(X184,X185)
| ~ ssPv6(X185)
| ~ ssPv3(skf1(X184))
| ~ ssPv4(X184)
| ssPv5(X185) ),
inference(resolution,[status(thm)],[c59,clause1]) ).
cnf(clause17,negated_conjecture,
( ~ ssRr(X111,X110)
| ~ ssPv7(X110)
| ~ ssRr(X111,X109)
| ~ ssRr(X111,X108)
| ssPv8(X109)
| ssPv3(X108)
| ssPv4(X111) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c44,plain,
( ~ ssRr(X169,X170)
| ~ ssPv7(X170)
| ~ ssRr(X169,X171)
| ssPv8(X171)
| ssPv3(skf1(X169))
| ssPv4(X169) ),
inference(resolution,[status(thm)],[clause17,clause1]) ).
cnf(c73,plain,
( ~ ssRr(X174,X173)
| ~ ssPv7(X173)
| ssPv8(X173)
| ssPv3(skf1(X174))
| ssPv4(X174) ),
inference(factor,[status(thm)],[c44]) ).
cnf(c46,plain,
( ~ ssRr(X137,X139)
| ~ ssPv6(X139)
| ~ ssRr(X137,X138)
| ~ ssPv3(X137)
| ssPv8(X138)
| ssPv6(X138) ),
inference(factor,[status(thm)],[clause18]) ).
cnf(c58,plain,
( ~ ssRr(X167,X168)
| ~ ssPv6(X168)
| ~ ssPv3(X167)
| ssPv8(skf1(X167))
| ssPv6(skf1(X167)) ),
inference(resolution,[status(thm)],[c46,clause1]) ).
cnf(c43,plain,
( ~ ssRr(X131,X129)
| ~ ssPv7(X129)
| ~ ssRr(X131,X130)
| ssPv8(X130)
| ssPv3(X130)
| ssPv4(X131) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c56,plain,
( ~ ssRr(X164,X165)
| ~ ssPv7(X165)
| ssPv8(skf1(X164))
| ssPv3(skf1(X164))
| ssPv4(X164) ),
inference(resolution,[status(thm)],[c43,clause1]) ).
cnf(c52,plain,
( ~ ssRr(X148,X147)
| ~ ssPv5(X147)
| ~ ssRr(X148,X146)
| ~ ssPv5(X148)
| ssPv6(X146)
| ssPv4(X147) ),
inference(factor,[status(thm)],[clause19]) ).
cnf(c62,plain,
( ~ ssRr(X150,X149)
| ~ ssPv5(X149)
| ~ ssPv5(X150)
| ssPv6(X149)
| ssPv4(X149) ),
inference(factor,[status(thm)],[c52]) ).
cnf(c64,plain,
( ~ ssPv5(skf1(X153))
| ~ ssPv5(X153)
| ssPv6(skf1(X153))
| ssPv4(skf1(X153)) ),
inference(resolution,[status(thm)],[c62,clause1]) ).
cnf(c63,plain,
( ~ ssRr(X151,X152)
| ~ ssPv5(X152)
| ~ ssPv5(X151)
| ssPv6(skf1(X151))
| ssPv4(X152) ),
inference(resolution,[status(thm)],[c52,clause1]) ).
cnf(c42,plain,
( ~ ssRr(X118,X116)
| ~ ssPv7(X116)
| ~ ssRr(X118,X117)
| ssPv8(X117)
| ssPv3(X116)
| ssPv4(X118) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c48,plain,
( ~ ssRr(X120,X119)
| ~ ssPv7(X119)
| ssPv8(X119)
| ssPv3(X119)
| ssPv4(X120) ),
inference(factor,[status(thm)],[c42]) ).
cnf(c50,plain,
( ~ ssPv7(skf1(X123))
| ssPv8(skf1(X123))
| ssPv3(skf1(X123))
| ssPv4(X123) ),
inference(resolution,[status(thm)],[c48,clause1]) ).
cnf(c49,plain,
( ~ ssRr(X122,X121)
| ~ ssPv7(X121)
| ssPv8(skf1(X122))
| ssPv3(X121)
| ssPv4(X122) ),
inference(resolution,[status(thm)],[c42,clause1]) ).
cnf(clause16,negated_conjecture,
( ~ ssRr(X100,X99)
| ~ ssPv4(X99)
| ~ ssRr(X100,X98)
| ~ ssPv3(X98)
| ~ ssPv4(X100)
| ~ ssPv8(X100) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c40,plain,
( ~ ssRr(X106,X107)
| ~ ssPv4(X107)
| ~ ssPv3(skf1(X106))
| ~ ssPv4(X106)
| ~ ssPv8(X106) ),
inference(resolution,[status(thm)],[clause16,clause1]) ).
cnf(clause15,negated_conjecture,
( ~ ssRr(X89,X88)
| ~ ssPv5(X88)
| ~ ssRr(X89,X87)
| ~ ssPv2(X87)
| ~ ssPv2(X89)
| ssPv7(X89) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c36,plain,
( ~ ssRr(X104,X105)
| ~ ssPv5(X105)
| ~ ssPv2(skf1(X104))
| ~ ssPv2(X104)
| ssPv7(X104) ),
inference(resolution,[status(thm)],[clause15,clause1]) ).
cnf(c39,plain,
( ~ ssRr(X101,X102)
| ~ ssPv4(X102)
| ~ ssPv3(X102)
| ~ ssPv4(X101)
| ~ ssPv8(X101) ),
inference(factor,[status(thm)],[clause16]) ).
cnf(c41,plain,
( ~ ssPv4(skf1(X103))
| ~ ssPv3(skf1(X103))
| ~ ssPv4(X103)
| ~ ssPv8(X103) ),
inference(resolution,[status(thm)],[c39,clause1]) ).
cnf(clause14,negated_conjecture,
( ~ ssRr(X86,X85)
| ~ ssPv3(X85)
| ~ ssRr(X86,X84)
| ~ ssPv2(X84)
| ~ ssPv1(X86)
| ssPv8(X86) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c34,plain,
( ~ ssRr(X96,X97)
| ~ ssPv3(X97)
| ~ ssPv2(skf1(X96))
| ~ ssPv1(X96)
| ssPv8(X96) ),
inference(resolution,[status(thm)],[clause14,clause1]) ).
cnf(c35,plain,
( ~ ssRr(X92,X93)
| ~ ssPv5(X93)
| ~ ssPv2(X93)
| ~ ssPv2(X92)
| ssPv7(X92) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c38,plain,
( ~ ssPv5(skf1(X95))
| ~ ssPv2(skf1(X95))
| ~ ssPv2(X95)
| ssPv7(X95) ),
inference(resolution,[status(thm)],[c35,clause1]) ).
cnf(c33,plain,
( ~ ssRr(X90,X91)
| ~ ssPv3(X91)
| ~ ssPv2(X91)
| ~ ssPv1(X90)
| ssPv8(X90) ),
inference(factor,[status(thm)],[clause14]) ).
cnf(c37,plain,
( ~ ssPv3(skf1(X94))
| ~ ssPv2(skf1(X94))
| ~ ssPv1(X94)
| ssPv8(X94) ),
inference(resolution,[status(thm)],[c33,clause1]) ).
cnf(clause13,negated_conjecture,
( ~ ssRr(X77,X76)
| ~ ssPv7(X76)
| ~ ssRr(X77,X75)
| ~ ssPv1(X77)
| ~ ssPv2(X77)
| ssPv4(X75) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(c30,plain,
( ~ ssRr(X82,X81)
| ~ ssPv7(X81)
| ~ ssPv1(X82)
| ~ ssPv2(X82)
| ssPv4(skf1(X82)) ),
inference(resolution,[status(thm)],[clause13,clause1]) ).
cnf(c29,plain,
( ~ ssRr(X78,X79)
| ~ ssPv7(X79)
| ~ ssPv1(X78)
| ~ ssPv2(X78)
| ssPv4(X79) ),
inference(factor,[status(thm)],[clause13]) ).
cnf(c31,plain,
( ~ ssPv7(skf1(X80))
| ~ ssPv1(X80)
| ~ ssPv2(X80)
| ssPv4(skf1(X80)) ),
inference(resolution,[status(thm)],[c29,clause1]) ).
cnf(clause12,negated_conjecture,
( ~ ssRr(X67,X66)
| ~ ssPv3(X66)
| ~ ssRr(X67,X65)
| ~ ssPv1(X67)
| ~ ssPv6(X67)
| ssPv7(X65) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c26,plain,
( ~ ssRr(X72,X73)
| ~ ssPv3(X73)
| ~ ssPv1(X72)
| ~ ssPv6(X72)
| ssPv7(skf1(X72)) ),
inference(resolution,[status(thm)],[clause12,clause1]) ).
cnf(c25,plain,
( ~ ssRr(X69,X70)
| ~ ssPv3(X70)
| ~ ssPv1(X69)
| ~ ssPv6(X69)
| ssPv7(X70) ),
inference(factor,[status(thm)],[clause12]) ).
cnf(c27,plain,
( ~ ssPv3(skf1(X71))
| ~ ssPv1(X71)
| ~ ssPv6(X71)
| ssPv7(skf1(X71)) ),
inference(resolution,[status(thm)],[c25,clause1]) ).
cnf(clause11,negated_conjecture,
( ~ ssRr(X56,X55)
| ~ ssPv7(X55)
| ~ ssRr(X56,X54)
| ~ ssPv3(X56)
| ~ ssPv8(X56)
| ssPv7(X54) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c22,plain,
( ~ ssRr(X63,X64)
| ~ ssPv7(X64)
| ~ ssPv3(X63)
| ~ ssPv8(X63)
| ssPv7(skf1(X63)) ),
inference(resolution,[status(thm)],[clause11,clause1]) ).
cnf(clause10,negated_conjecture,
( ~ ssRr(X51,X50)
| ~ ssPv7(X50)
| ~ ssRr(X51,X49)
| ~ ssPv3(X51)
| ~ ssPv8(X51)
| ssPv8(X49) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c19,plain,
( ~ ssRr(X60,X61)
| ~ ssPv7(X61)
| ~ ssPv3(X60)
| ~ ssPv8(X60)
| ssPv8(skf1(X60)) ),
inference(resolution,[status(thm)],[clause10,clause1]) ).
cnf(c18,plain,
( ~ ssRr(X53,X52)
| ~ ssPv7(X52)
| ~ ssPv3(X53)
| ~ ssPv8(X53)
| ssPv8(X52) ),
inference(factor,[status(thm)],[clause10]) ).
cnf(c20,plain,
( ~ ssPv7(skf1(X57))
| ~ ssPv3(X57)
| ~ ssPv8(X57)
| ssPv8(skf1(X57)) ),
inference(resolution,[status(thm)],[c18,clause1]) ).
cnf(clause9,negated_conjecture,
( ~ ssRr(X43,X42)
| ~ ssPv6(X42)
| ~ ssRr(X43,X41)
| ~ ssPv4(X43)
| ~ ssPv5(X43)
| ssPv6(X41) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c16,plain,
( ~ ssRr(X46,X47)
| ~ ssPv6(X47)
| ~ ssPv4(X46)
| ~ ssPv5(X46)
| ssPv6(skf1(X46)) ),
inference(resolution,[status(thm)],[clause9,clause1]) ).
cnf(clause8,negated_conjecture,
( ~ ssRr(X32,X31)
| ~ ssPv8(X31)
| ~ ssRr(X32,X30)
| ~ ssPv4(X30)
| ssPv5(X32)
| ssPv7(X32) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c12,plain,
( ~ ssRr(X39,X40)
| ~ ssPv8(X40)
| ~ ssPv4(skf1(X39))
| ssPv5(X39)
| ssPv7(X39) ),
inference(resolution,[status(thm)],[clause8,clause1]) ).
cnf(clause7,negated_conjecture,
( ~ ssRr(X22,X21)
| ~ ssRr(X22,X20)
| ~ ssPv4(X22)
| ssPv5(X21)
| ssPv3(X20)
| ssPv5(X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(c8,plain,
( ~ ssRr(X36,X37)
| ~ ssPv4(X36)
| ssPv5(X37)
| ssPv3(skf1(X36))
| ssPv5(X36) ),
inference(resolution,[status(thm)],[clause7,clause1]) ).
cnf(c11,plain,
( ~ ssRr(X33,X34)
| ~ ssPv8(X34)
| ~ ssPv4(X34)
| ssPv5(X33)
| ssPv7(X33) ),
inference(factor,[status(thm)],[clause8]) ).
cnf(c13,plain,
( ~ ssPv8(skf1(X35))
| ~ ssPv4(skf1(X35))
| ssPv5(X35)
| ssPv7(X35) ),
inference(resolution,[status(thm)],[c11,clause1]) ).
cnf(clause6,negated_conjecture,
( ~ ssRr(X17,X16)
| ~ ssPv3(X16)
| ~ ssRr(X17,X15)
| ssPv5(X15)
| ssPv6(X17)
| ssPv8(X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c5,plain,
( ~ ssRr(X27,X28)
| ~ ssPv3(X28)
| ssPv5(skf1(X27))
| ssPv6(X27)
| ssPv8(X27) ),
inference(resolution,[status(thm)],[clause6,clause1]) ).
cnf(c7,plain,
( ~ ssRr(X24,X25)
| ~ ssPv4(X24)
| ssPv5(X25)
| ssPv3(X25)
| ssPv5(X24) ),
inference(factor,[status(thm)],[clause7]) ).
cnf(c9,plain,
( ~ ssPv4(X26)
| ssPv5(skf1(X26))
| ssPv3(skf1(X26))
| ssPv5(X26) ),
inference(resolution,[status(thm)],[c7,clause1]) ).
cnf(c4,plain,
( ~ ssRr(X19,X18)
| ~ ssPv3(X18)
| ssPv5(X18)
| ssPv6(X19)
| ssPv8(X19) ),
inference(factor,[status(thm)],[clause6]) ).
cnf(c6,plain,
( ~ ssPv3(skf1(X23))
| ssPv5(skf1(X23))
| ssPv6(X23)
| ssPv8(X23) ),
inference(resolution,[status(thm)],[c4,clause1]) ).
cnf(clause5,negated_conjecture,
( ~ ssRr(X13,X12)
| ~ ssPv7(X12)
| ~ ssPv3(X13)
| ~ ssPv4(X13)
| ssPv6(X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c3,plain,
( ~ ssPv7(skf1(X14))
| ~ ssPv3(X14)
| ~ ssPv4(X14)
| ssPv6(X14) ),
inference(resolution,[status(thm)],[clause5,clause1]) ).
cnf(clause4,negated_conjecture,
( ~ ssRr(X10,X9)
| ~ ssPv3(X9)
| ~ ssPv2(X10)
| ssPv1(X10)
| ssPv7(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(c2,plain,
( ~ ssPv3(skf1(X11))
| ~ ssPv2(X11)
| ssPv1(X11)
| ssPv7(X11) ),
inference(resolution,[status(thm)],[clause4,clause1]) ).
cnf(clause3,negated_conjecture,
( ~ ssRr(X7,X6)
| ~ ssPv5(X7)
| ~ ssPv8(X7)
| ssPv2(X6)
| ssPv2(X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c1,plain,
( ~ ssPv5(X8)
| ~ ssPv8(X8)
| ssPv2(skf1(X8))
| ssPv2(X8) ),
inference(resolution,[status(thm)],[clause3,clause1]) ).
cnf(clause2,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssPv3(X3)
| ~ ssPv8(X4)
| ssPv4(X4)
| ssPv5(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(c0,plain,
( ~ ssPv3(skf1(X5))
| ~ ssPv8(X5)
| ssPv4(X5)
| ssPv5(X5) ),
inference(resolution,[status(thm)],[clause2,clause1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN738-1 : TPTP v8.1.2. Released v2.5.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n028.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 20:28:52 EDT 2024
% 0.19/0.34 % CPUTime :
% 0.42/0.62 % Version: 1.5
% 0.42/0.62 % SZS status Satisfiable
% 0.42/0.62 % SZS output start Saturation
% See solution above
% 0.42/0.62
% 0.42/0.62 % Initial clauses : 21
% 0.42/0.62 % Processed clauses : 90
% 0.42/0.62 % Factors computed : 35
% 0.42/0.62 % Resolvents computed: 64
% 0.42/0.62 % Tautologies deleted: 8
% 0.42/0.62 % Forward subsumed : 22
% 0.42/0.62 % Backward subsumed : 0
% 0.42/0.62 % -------- CPU Time ---------
% 0.42/0.62 % User time : 0.264 s
% 0.42/0.62 % System time : 0.019 s
% 0.42/0.62 % Total time : 0.283 s
%------------------------------------------------------------------------------