%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS011-1 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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:28:27 EDT 2024
% Result : Satisfiable 0.50s 0.73s
% Output : Saturation 0.50s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_1,negated_conjecture,
f(exists),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1) ).
cnf(clause_45,axiom,
( f3(X10)
| ~ f(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_45) ).
cnf(c0,plain,
f3(exists),
inference(resolution,[status(thm)],[clause_45,clause_1]) ).
cnf(clause_36,axiom,
( t3(u11r4(X48),u11r5(X48))
| ~ f3(X48) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_36) ).
cnf(c22,plain,
t3(u11r4(exists),u11r5(exists)),
inference(resolution,[status(thm)],[clause_36,c0]) ).
cnf(clause_44,axiom,
( f3(X109)
| t(X111,u11r3(X111,X109))
| ~ r3(X109,X111)
| ~ t3(X111,X110)
| ~ e(X110) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_44) ).
cnf(c100,plain,
( f3(X158)
| t(u11r4(exists),u11r3(u11r4(exists),X158))
| ~ r3(X158,u11r4(exists))
| ~ e(u11r5(exists)) ),
inference(resolution,[status(thm)],[clause_44,c22]) ).
cnf(clause_43,axiom,
( f3(X106)
| t(X108,u11r2(X108,X106))
| ~ r3(X106,X108)
| ~ t3(X108,X107)
| ~ e(X107) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_43) ).
cnf(c99,plain,
( f3(X157)
| t(u11r4(exists),u11r2(u11r4(exists),X157))
| ~ r3(X157,u11r4(exists))
| ~ e(u11r5(exists)) ),
inference(resolution,[status(thm)],[clause_43,c22]) ).
cnf(clause_8,axiom,
( t(X23,X24)
| ~ t3(X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_8) ).
cnf(c24,plain,
t(u11r4(exists),u11r5(exists)),
inference(resolution,[status(thm)],[c22,clause_8]) ).
cnf(clause_37,axiom,
( equalish(X91,X92)
| equalish(X91,X90)
| equalish(X92,X90)
| ~ f3(X93)
| ~ t(u11r4(X93),X91)
| ~ t(u11r4(X93),X92)
| ~ t(u11r4(X93),X90) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_37) ).
cnf(c97,plain,
( equalish(X153,X154)
| equalish(X153,u11r5(exists))
| equalish(X154,u11r5(exists))
| ~ f3(exists)
| ~ t(u11r4(exists),X153)
| ~ t(u11r4(exists),X154) ),
inference(resolution,[status(thm)],[clause_37,c24]) ).
cnf(clause_42,axiom,
( f3(X103)
| t(X105,u11r1(X105,X103))
| ~ r3(X103,X105)
| ~ t3(X105,X104)
| ~ e(X104) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_42) ).
cnf(c98,plain,
( f3(X152)
| t(u11r4(exists),u11r1(u11r4(exists),X152))
| ~ r3(X152,u11r4(exists))
| ~ e(u11r5(exists)) ),
inference(resolution,[status(thm)],[clause_42,c22]) ).
cnf(clause_46,axiom,
( f2(X13)
| ~ f(X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_46) ).
cnf(c1,plain,
f2(exists),
inference(resolution,[status(thm)],[clause_46,clause_1]) ).
cnf(clause_26,axiom,
( t2(u10r4(X47),u10r5(X47))
| ~ f2(X47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_26) ).
cnf(c20,plain,
t2(u10r4(exists),u10r5(exists)),
inference(resolution,[status(thm)],[clause_26,c1]) ).
cnf(clause_34,axiom,
( f2(X87)
| t(X89,u10r3(X89,X87))
| ~ r2(X87,X89)
| ~ t2(X89,X88)
| ~ d(X88) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_34) ).
cnf(c92,plain,
( f2(X151)
| t(u10r4(exists),u10r3(u10r4(exists),X151))
| ~ r2(X151,u10r4(exists))
| ~ d(u10r5(exists)) ),
inference(resolution,[status(thm)],[clause_34,c20]) ).
cnf(clause_7,axiom,
( t(X21,X22)
| ~ t2(X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_7) ).
cnf(c21,plain,
t(u10r4(exists),u10r5(exists)),
inference(resolution,[status(thm)],[c20,clause_7]) ).
cnf(clause_27,axiom,
( equalish(X66,X67)
| equalish(X66,X65)
| equalish(X67,X65)
| ~ f2(X68)
| ~ t(u10r4(X68),X66)
| ~ t(u10r4(X68),X67)
| ~ t(u10r4(X68),X65) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_27) ).
cnf(c52,plain,
( equalish(X147,X148)
| equalish(X147,u10r5(exists))
| equalish(X148,u10r5(exists))
| ~ f2(exists)
| ~ t(u10r4(exists),X147)
| ~ t(u10r4(exists),X148) ),
inference(resolution,[status(thm)],[clause_27,c21]) ).
cnf(clause_33,axiom,
( f2(X84)
| t(X86,u10r2(X86,X84))
| ~ r2(X84,X86)
| ~ t2(X86,X85)
| ~ d(X85) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_33) ).
cnf(c83,plain,
( f2(X146)
| t(u10r4(exists),u10r2(u10r4(exists),X146))
| ~ r2(X146,u10r4(exists))
| ~ d(u10r5(exists)) ),
inference(resolution,[status(thm)],[clause_33,c20]) ).
cnf(clause_32,axiom,
( f2(X80)
| t(X82,u10r1(X82,X80))
| ~ r2(X80,X82)
| ~ t2(X82,X81)
| ~ d(X81) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_32) ).
cnf(c77,plain,
( f2(X145)
| t(u10r4(exists),u10r1(u10r4(exists),X145))
| ~ r2(X145,u10r4(exists))
| ~ d(u10r5(exists)) ),
inference(resolution,[status(thm)],[clause_32,c20]) ).
cnf(clause_47,axiom,
( f1(X14)
| ~ f(X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_47) ).
cnf(c2,plain,
f1(exists),
inference(resolution,[status(thm)],[clause_47,clause_1]) ).
cnf(clause_16,axiom,
( t1(u9r4(X26),u9r5(X26))
| ~ f1(X26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_16) ).
cnf(c4,plain,
t1(u9r4(exists),u9r5(exists)),
inference(resolution,[status(thm)],[clause_16,c2]) ).
cnf(clause_24,axiom,
( f1(X62)
| t(X64,u9r3(X64,X62))
| ~ r1(X62,X64)
| ~ t1(X64,X63)
| ~ c(X63) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_24) ).
cnf(c43,plain,
( f1(X144)
| t(u9r4(exists),u9r3(u9r4(exists),X144))
| ~ r1(X144,u9r4(exists))
| ~ c(u9r5(exists)) ),
inference(resolution,[status(thm)],[clause_24,c4]) ).
cnf(clause_23,axiom,
( f1(X54)
| t(X56,u9r2(X56,X54))
| ~ r1(X54,X56)
| ~ t1(X56,X55)
| ~ c(X55) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_23) ).
cnf(c26,plain,
( f1(X137)
| t(u9r4(exists),u9r2(u9r4(exists),X137))
| ~ r1(X137,u9r4(exists))
| ~ c(u9r5(exists)) ),
inference(resolution,[status(thm)],[clause_23,c4]) ).
cnf(c96,plain,
( equalish(X129,X128)
| equalish(X128,X128)
| ~ f3(X130)
| ~ t(u11r4(X130),X129)
| ~ t(u11r4(X130),X128) ),
inference(factor,[status(thm)],[clause_37]) ).
cnf(c111,plain,
( equalish(X133,X133)
| ~ f3(X132)
| ~ t(u11r4(X132),X133) ),
inference(factor,[status(thm)],[c96]) ).
cnf(c114,plain,
( equalish(u11r5(exists),u11r5(exists))
| ~ f3(exists) ),
inference(resolution,[status(thm)],[c111,c24]) ).
cnf(c115,plain,
equalish(u11r5(exists),u11r5(exists)),
inference(resolution,[status(thm)],[c114,c0]) ).
cnf(clause_22,axiom,
( f1(X49)
| t(X51,u9r1(X51,X49))
| ~ r1(X49,X51)
| ~ t1(X51,X50)
| ~ c(X50) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_22) ).
cnf(c23,plain,
( f1(X131)
| t(u9r4(exists),u9r1(u9r4(exists),X131))
| ~ r1(X131,u9r4(exists))
| ~ c(u9r5(exists)) ),
inference(resolution,[status(thm)],[clause_22,c4]) ).
cnf(c51,plain,
( equalish(X120,X122)
| equalish(X122,X122)
| ~ f2(X121)
| ~ t(u10r4(X121),X120)
| ~ t(u10r4(X121),X122) ),
inference(factor,[status(thm)],[clause_27]) ).
cnf(c105,plain,
( equalish(X126,X126)
| ~ f2(X125)
| ~ t(u10r4(X125),X126) ),
inference(factor,[status(thm)],[c51]) ).
cnf(c109,plain,
( equalish(u10r5(exists),u10r5(exists))
| ~ f2(exists) ),
inference(resolution,[status(thm)],[c105,c21]) ).
cnf(c110,plain,
equalish(u10r5(exists),u10r5(exists)),
inference(resolution,[status(thm)],[c109,c1]) ).
cnf(clause_17,axiom,
( equalish(X30,X31)
| equalish(X30,X29)
| equalish(X31,X29)
| ~ f1(X32)
| ~ t(u9r4(X32),X30)
| ~ t(u9r4(X32),X31)
| ~ t(u9r4(X32),X29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_17) ).
cnf(clause_6,axiom,
( t(X19,X20)
| ~ t1(X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6) ).
cnf(c18,plain,
t(u9r4(exists),u9r5(exists)),
inference(resolution,[status(thm)],[c4,clause_6]) ).
cnf(c19,plain,
( equalish(X124,X123)
| equalish(X124,u9r5(exists))
| equalish(X123,u9r5(exists))
| ~ f1(exists)
| ~ t(u9r4(exists),X124)
| ~ t(u9r4(exists),X123) ),
inference(resolution,[status(thm)],[c18,clause_17]) ).
cnf(c8,plain,
( equalish(X114,X113)
| equalish(X114,X114)
| equalish(X113,X114)
| ~ f1(X112)
| ~ t(u9r4(X112),X114)
| ~ t(u9r4(X112),X113) ),
inference(factor,[status(thm)],[clause_17]) ).
cnf(c101,plain,
( equalish(X116,X116)
| ~ f1(X115)
| ~ t(u9r4(X115),X116) ),
inference(factor,[status(thm)],[c8]) ).
cnf(c103,plain,
( equalish(u9r5(exists),u9r5(exists))
| ~ f1(exists) ),
inference(resolution,[status(thm)],[c101,c18]) ).
cnf(c104,plain,
equalish(u9r5(exists),u9r5(exists)),
inference(resolution,[status(thm)],[c103,c2]) ).
cnf(clause_41,axiom,
( f3(X100)
| ~ r3(X100,X102)
| ~ equalish(u11r3(X102,X100),u11r2(X102,X100))
| ~ t3(X102,X101)
| ~ e(X101) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_41) ).
cnf(clause_40,axiom,
( f3(X97)
| ~ r3(X97,X99)
| ~ equalish(u11r3(X99,X97),u11r1(X99,X97))
| ~ t3(X99,X98)
| ~ e(X98) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_40) ).
cnf(clause_39,axiom,
( f3(X94)
| ~ r3(X94,X96)
| ~ equalish(u11r2(X96,X94),u11r1(X96,X94))
| ~ t3(X96,X95)
| ~ e(X95) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_39) ).
cnf(clause_2,negated_conjecture,
~ g(exists),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2) ).
cnf(clause_50,axiom,
( g(X18)
| ~ r2least(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_50) ).
cnf(clause_5,axiom,
( r(X16,X17)
| ~ r3(X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
cnf(clause_38,axiom,
( r3(X38,u11r4(X38))
| ~ f3(X38) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_38) ).
cnf(c16,plain,
r3(exists,u11r4(exists)),
inference(resolution,[status(thm)],[clause_38,c0]) ).
cnf(c17,plain,
r(exists,u11r4(exists)),
inference(resolution,[status(thm)],[c16,clause_5]) ).
cnf(clause_4,axiom,
( r(X11,X12)
| ~ r2(X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4) ).
cnf(clause_28,axiom,
( r2(X37,u10r4(X37))
| ~ f2(X37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_28) ).
cnf(c14,plain,
r2(exists,u10r4(exists)),
inference(resolution,[status(thm)],[clause_28,c1]) ).
cnf(c15,plain,
r(exists,u10r4(exists)),
inference(resolution,[status(thm)],[c14,clause_4]) ).
cnf(clause_54,axiom,
( r2least(X57)
| equalish(X58,X59)
| ~ r(X57,X58)
| ~ r(X57,X59) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_54) ).
cnf(c30,plain,
( r2least(exists)
| equalish(X83,u10r4(exists))
| ~ r(exists,X83) ),
inference(resolution,[status(thm)],[clause_54,c15]) ).
cnf(c81,plain,
( r2least(exists)
| equalish(u11r4(exists),u10r4(exists)) ),
inference(resolution,[status(thm)],[c30,c17]) ).
cnf(c88,plain,
( equalish(u11r4(exists),u10r4(exists))
| g(exists) ),
inference(resolution,[status(thm)],[c81,clause_50]) ).
cnf(c93,plain,
equalish(u11r4(exists),u10r4(exists)),
inference(resolution,[status(thm)],[c88,clause_2]) ).
cnf(clause_3,axiom,
( r(X5,X6)
| ~ r1(X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3) ).
cnf(clause_18,axiom,
( r1(X33,u9r4(X33))
| ~ f1(X33) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_18) ).
cnf(c12,plain,
r1(exists,u9r4(exists)),
inference(resolution,[status(thm)],[clause_18,c2]) ).
cnf(c13,plain,
r(exists,u9r4(exists)),
inference(resolution,[status(thm)],[c12,clause_3]) ).
cnf(c80,plain,
( r2least(exists)
| equalish(u9r4(exists),u10r4(exists)) ),
inference(resolution,[status(thm)],[c30,c13]) ).
cnf(c85,plain,
( equalish(u9r4(exists),u10r4(exists))
| g(exists) ),
inference(resolution,[status(thm)],[c80,clause_50]) ).
cnf(c90,plain,
equalish(u9r4(exists),u10r4(exists)),
inference(resolution,[status(thm)],[c85,clause_2]) ).
cnf(c29,plain,
( r2least(exists)
| equalish(X76,u11r4(exists))
| ~ r(exists,X76) ),
inference(resolution,[status(thm)],[clause_54,c17]) ).
cnf(c68,plain,
( r2least(exists)
| equalish(u10r4(exists),u11r4(exists)) ),
inference(resolution,[status(thm)],[c29,c15]) ).
cnf(c73,plain,
( equalish(u10r4(exists),u11r4(exists))
| g(exists) ),
inference(resolution,[status(thm)],[c68,clause_50]) ).
cnf(c78,plain,
equalish(u10r4(exists),u11r4(exists)),
inference(resolution,[status(thm)],[c73,clause_2]) ).
cnf(c66,plain,
( r2least(exists)
| equalish(u9r4(exists),u11r4(exists)) ),
inference(resolution,[status(thm)],[c29,c13]) ).
cnf(c70,plain,
( equalish(u9r4(exists),u11r4(exists))
| g(exists) ),
inference(resolution,[status(thm)],[c66,clause_50]) ).
cnf(c75,plain,
equalish(u9r4(exists),u11r4(exists)),
inference(resolution,[status(thm)],[c70,clause_2]) ).
cnf(clause_31,axiom,
( f2(X77)
| ~ r2(X77,X79)
| ~ equalish(u10r3(X79,X77),u10r2(X79,X77))
| ~ t2(X79,X78)
| ~ d(X78) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_31) ).
cnf(c28,plain,
( r2least(exists)
| equalish(X69,u9r4(exists))
| ~ r(exists,X69) ),
inference(resolution,[status(thm)],[clause_54,c13]) ).
cnf(c55,plain,
( r2least(exists)
| equalish(u10r4(exists),u9r4(exists)) ),
inference(resolution,[status(thm)],[c28,c15]) ).
cnf(c60,plain,
( equalish(u10r4(exists),u9r4(exists))
| g(exists) ),
inference(resolution,[status(thm)],[c55,clause_50]) ).
cnf(c64,plain,
equalish(u10r4(exists),u9r4(exists)),
inference(resolution,[status(thm)],[c60,clause_2]) ).
cnf(clause_30,axiom,
( f2(X73)
| ~ r2(X73,X75)
| ~ equalish(u10r3(X75,X73),u10r1(X75,X73))
| ~ t2(X75,X74)
| ~ d(X74) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_30) ).
cnf(c54,plain,
( r2least(exists)
| equalish(u11r4(exists),u9r4(exists)) ),
inference(resolution,[status(thm)],[c28,c17]) ).
cnf(c57,plain,
( equalish(u11r4(exists),u9r4(exists))
| g(exists) ),
inference(resolution,[status(thm)],[c54,clause_50]) ).
cnf(c62,plain,
equalish(u11r4(exists),u9r4(exists)),
inference(resolution,[status(thm)],[c57,clause_2]) ).
cnf(clause_29,axiom,
( f2(X70)
| ~ r2(X70,X72)
| ~ equalish(u10r2(X72,X70),u10r1(X72,X70))
| ~ t2(X72,X71)
| ~ d(X71) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_29) ).
cnf(c27,plain,
( r2least(X60)
| equalish(X61,X61)
| ~ r(X60,X61) ),
inference(factor,[status(thm)],[clause_54]) ).
cnf(c33,plain,
( r2least(exists)
| equalish(u10r4(exists),u10r4(exists)) ),
inference(resolution,[status(thm)],[c27,c15]) ).
cnf(c41,plain,
( equalish(u10r4(exists),u10r4(exists))
| g(exists) ),
inference(resolution,[status(thm)],[c33,clause_50]) ).
cnf(c48,plain,
equalish(u10r4(exists),u10r4(exists)),
inference(resolution,[status(thm)],[c41,clause_2]) ).
cnf(c32,plain,
( r2least(exists)
| equalish(u11r4(exists),u11r4(exists)) ),
inference(resolution,[status(thm)],[c27,c17]) ).
cnf(c38,plain,
( equalish(u11r4(exists),u11r4(exists))
| g(exists) ),
inference(resolution,[status(thm)],[c32,clause_50]) ).
cnf(c46,plain,
equalish(u11r4(exists),u11r4(exists)),
inference(resolution,[status(thm)],[c38,clause_2]) ).
cnf(c31,plain,
( r2least(exists)
| equalish(u9r4(exists),u9r4(exists)) ),
inference(resolution,[status(thm)],[c27,c13]) ).
cnf(c35,plain,
( equalish(u9r4(exists),u9r4(exists))
| g(exists) ),
inference(resolution,[status(thm)],[c31,clause_50]) ).
cnf(c44,plain,
equalish(u9r4(exists),u9r4(exists)),
inference(resolution,[status(thm)],[c35,clause_2]) ).
cnf(clause_48,axiom,
( f(X53)
| ~ f1(X53)
| ~ f2(X53)
| ~ f3(X53) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_48) ).
cnf(clause_51,axiom,
( ~ r2least(X52)
| ~ equalish(u14r2(X52),u14r1(X52)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_51) ).
cnf(clause_21,axiom,
( f1(X44)
| ~ r1(X44,X46)
| ~ equalish(u9r3(X46,X44),u9r2(X46,X44))
| ~ t1(X46,X45)
| ~ c(X45) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_21) ).
cnf(clause_53,axiom,
( r(X43,u14r2(X43))
| ~ r2least(X43) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_53) ).
cnf(clause_52,axiom,
( r(X42,u14r1(X42))
| ~ r2least(X42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_52) ).
cnf(clause_20,axiom,
( f1(X39)
| ~ r1(X39,X41)
| ~ equalish(u9r3(X41,X39),u9r1(X41,X39))
| ~ t1(X41,X40)
| ~ c(X40) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_20) ).
cnf(clause_19,axiom,
( f1(X34)
| ~ r1(X34,X36)
| ~ equalish(u9r2(X36,X34),u9r1(X36,X34))
| ~ t1(X36,X35)
| ~ c(X35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_19) ).
cnf(clause_11,axiom,
( ~ d(X4)
| ~ e(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_11) ).
cnf(clause_35,axiom,
( e(u11r5(X28))
| ~ f3(X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_35) ).
cnf(c7,plain,
e(u11r5(exists)),
inference(resolution,[status(thm)],[clause_35,c0]) ).
cnf(c11,plain,
~ d(u11r5(exists)),
inference(resolution,[status(thm)],[c7,clause_11]) ).
cnf(clause_9,axiom,
( ~ c(X2)
| ~ e(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_9) ).
cnf(c10,plain,
~ c(u11r5(exists)),
inference(resolution,[status(thm)],[c7,clause_9]) ).
cnf(clause_10,axiom,
( ~ c(X3)
| ~ d(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_10) ).
cnf(clause_25,axiom,
( d(u10r5(X27))
| ~ f2(X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_25) ).
cnf(c5,plain,
d(u10r5(exists)),
inference(resolution,[status(thm)],[clause_25,c1]) ).
cnf(c6,plain,
~ c(u10r5(exists)),
inference(resolution,[status(thm)],[c5,clause_10]) ).
cnf(clause_15,axiom,
( c(u9r5(X25))
| ~ f1(X25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_15) ).
cnf(c3,plain,
c(u9r5(exists)),
inference(resolution,[status(thm)],[clause_15,c2]) ).
cnf(clause_49,axiom,
( r2least(X15)
| ~ g(X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_49) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS011-1 : TPTP v8.1.2. Released v2.0.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n009.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 : Thu May 9 00:05:52 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.50/0.73 % Version: 1.5
% 0.50/0.73 % SZS status Satisfiable
% 0.50/0.73 % SZS output start Saturation
% See solution above
% 0.50/0.73
% 0.50/0.73 % Initial clauses : 54
% 0.50/0.73 % Processed clauses : 127
% 0.50/0.73 % Factors computed : 13
% 0.50/0.73 % Resolvents computed: 115
% 0.50/0.73 % Tautologies deleted: 0
% 0.50/0.73 % Forward subsumed : 55
% 0.50/0.73 % Backward subsumed : 24
% 0.50/0.73 % -------- CPU Time ---------
% 0.50/0.73 % User time : 0.367 s
% 0.50/0.73 % System time : 0.015 s
% 0.50/0.73 % Total time : 0.382 s
%------------------------------------------------------------------------------