%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS006-1 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:26 EDT 2024
% Result : Satisfiable 0.54s 0.72s
% Output : Saturation 0.54s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_5,negated_conjecture,
c(u4r1(exist)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_5) ).
cnf(clause_6,axiom,
( s2least(X2)
| ~ c(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6) ).
cnf(c0,plain,
s2least(u4r1(exist)),
inference(resolution,[status(thm)],[clause_6,clause_5]) ).
cnf(clause_10,axiom,
( s(X11,u1r2(X11))
| ~ s2least(X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_10) ).
cnf(c8,plain,
s(u4r1(exist),u1r2(u4r1(exist))),
inference(resolution,[status(thm)],[clause_10,c0]) ).
cnf(clause_14,axiom,
( equalish(X21,X20)
| ~ s1most(X19)
| ~ s(X19,X21)
| ~ s(X19,X20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_14) ).
cnf(clause_8,axiom,
( ~ s2least(X7)
| ~ equalish(u1r2(X7),u1r1(X7)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_8) ).
cnf(clause_16,axiom,
( s1most(X12)
| s(X12,u3r1(X12)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16) ).
cnf(clause_9,axiom,
( s(X9,u1r1(X9))
| ~ s2least(X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_9) ).
cnf(c6,plain,
s(u4r1(exist),u1r1(u4r1(exist))),
inference(resolution,[status(thm)],[clause_9,c0]) ).
cnf(c35,plain,
( equalish(X112,u1r1(u4r1(exist)))
| ~ s1most(u4r1(exist))
| ~ s(u4r1(exist),X112) ),
inference(resolution,[status(thm)],[c6,clause_14]) ).
cnf(c146,plain,
( equalish(u1r2(u4r1(exist)),u1r1(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c35,c8]) ).
cnf(c187,plain,
( equalish(u1r2(u4r1(exist)),u1r1(u4r1(exist)))
| s(u4r1(exist),u3r1(u4r1(exist))) ),
inference(resolution,[status(thm)],[c146,clause_16]) ).
cnf(c242,plain,
( s(u4r1(exist),u3r1(u4r1(exist)))
| ~ s2least(u4r1(exist)) ),
inference(resolution,[status(thm)],[c187,clause_8]) ).
cnf(c250,plain,
s(u4r1(exist),u3r1(u4r1(exist))),
inference(resolution,[status(thm)],[c242,c0]) ).
cnf(c255,plain,
( equalish(X168,u3r1(u4r1(exist)))
| ~ s1most(u4r1(exist))
| ~ s(u4r1(exist),X168) ),
inference(resolution,[status(thm)],[c250,clause_14]) ).
cnf(c325,plain,
( equalish(u1r2(u4r1(exist)),u3r1(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c255,c8]) ).
cnf(clause_17,axiom,
( s1most(X16)
| s(X16,u3r2(X16)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_17) ).
cnf(c185,plain,
( equalish(u1r2(u4r1(exist)),u1r1(u4r1(exist)))
| s(u4r1(exist),u3r2(u4r1(exist))) ),
inference(resolution,[status(thm)],[c146,clause_17]) ).
cnf(c220,plain,
( s(u4r1(exist),u3r2(u4r1(exist)))
| ~ s2least(u4r1(exist)) ),
inference(resolution,[status(thm)],[c185,clause_8]) ).
cnf(c228,plain,
s(u4r1(exist),u3r2(u4r1(exist))),
inference(resolution,[status(thm)],[c220,c0]) ).
cnf(c323,plain,
( equalish(u3r2(u4r1(exist)),u3r1(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c255,c228]) ).
cnf(c320,plain,
( equalish(u1r1(u4r1(exist)),u3r1(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c255,c6]) ).
cnf(c233,plain,
( equalish(X166,u3r2(u4r1(exist)))
| ~ s1most(u4r1(exist))
| ~ s(u4r1(exist),X166) ),
inference(resolution,[status(thm)],[c228,clause_14]) ).
cnf(c296,plain,
( equalish(u3r1(u4r1(exist)),u3r2(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c233,c250]) ).
cnf(c295,plain,
( equalish(u1r2(u4r1(exist)),u3r2(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c233,c8]) ).
cnf(c290,plain,
( equalish(u1r1(u4r1(exist)),u3r2(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c233,c6]) ).
cnf(c256,plain,
( equalish(u3r1(u4r1(exist)),u1r1(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c250,c35]) ).
cnf(c44,plain,
( equalish(X161,u1r2(u4r1(exist)))
| ~ s1most(u4r1(exist))
| ~ s(u4r1(exist),X161) ),
inference(resolution,[status(thm)],[c8,clause_14]) ).
cnf(c254,plain,
( equalish(u3r1(u4r1(exist)),u1r2(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c250,c44]) ).
cnf(c16,plain,
( equalish(X33,X33)
| ~ s1most(X32)
| ~ s(X32,X33) ),
inference(factor,[status(thm)],[clause_14]) ).
cnf(c252,plain,
( equalish(u3r1(u4r1(exist)),u3r1(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c250,c16]) ).
cnf(c234,plain,
( equalish(u3r2(u4r1(exist)),u1r1(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c228,c35]) ).
cnf(c232,plain,
( equalish(u3r2(u4r1(exist)),u1r2(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c228,c44]) ).
cnf(c230,plain,
( equalish(u3r2(u4r1(exist)),u3r2(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c228,c16]) ).
cnf(c176,plain,
( equalish(u1r1(u4r1(exist)),u1r2(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c44,c6]) ).
cnf(c43,plain,
( equalish(u1r2(u4r1(exist)),u1r2(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c8,c16]) ).
cnf(clause_2,negated_conjecture,
r1most(exist),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2) ).
cnf(clause_1,negated_conjecture,
e(exist),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1) ).
cnf(clause_19,axiom,
( r(X17,u4r2(X17))
| ~ e(X17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_19) ).
cnf(c14,plain,
r(exist,u4r2(exist)),
inference(resolution,[status(thm)],[clause_19,clause_1]) ).
cnf(clause_3,negated_conjecture,
r(exist,u4r1(exist)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3) ).
cnf(clause_24,axiom,
( equalish(X43,X42)
| ~ r1most(X41)
| ~ r(X41,X43)
| ~ r(X41,X42) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_24) ).
cnf(c66,plain,
( equalish(X126,u4r1(exist))
| ~ r1most(exist)
| ~ r(exist,X126) ),
inference(resolution,[status(thm)],[clause_24,clause_3]) ).
cnf(c163,plain,
( equalish(u4r2(exist),u4r1(exist))
| ~ r1most(exist) ),
inference(resolution,[status(thm)],[c66,c14]) ).
cnf(c165,plain,
equalish(u4r2(exist),u4r1(exist)),
inference(resolution,[status(thm)],[c163,clause_2]) ).
cnf(c65,plain,
( equalish(X123,u4r2(exist))
| ~ r1most(exist)
| ~ r(exist,X123) ),
inference(resolution,[status(thm)],[clause_24,c14]) ).
cnf(c157,plain,
( equalish(u4r1(exist),u4r2(exist))
| ~ r1most(exist) ),
inference(resolution,[status(thm)],[c65,clause_3]) ).
cnf(c158,plain,
equalish(u4r1(exist),u4r2(exist)),
inference(resolution,[status(thm)],[c157,clause_2]) ).
cnf(clause_23,axiom,
( e(X34)
| ~ r1most(X34)
| ~ r(X34,X35)
| ~ c(X35)
| ~ r(X34,X36)
| ~ d(X36) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_23) ).
cnf(c37,plain,
( e(X117)
| ~ r1most(X117)
| ~ r(X117,X116)
| ~ c(X116)
| ~ d(X116) ),
inference(factor,[status(thm)],[clause_23]) ).
cnf(c34,plain,
( equalish(u1r1(u4r1(exist)),u1r1(u4r1(exist)))
| ~ s1most(u4r1(exist)) ),
inference(resolution,[status(thm)],[c6,c16]) ).
cnf(clause_13,axiom,
( d(X5)
| ~ s1most(X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_13) ).
cnf(clause_15,axiom,
( s1most(X27)
| ~ equalish(u3r2(X27),u3r1(X27)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_15) ).
cnf(clause_11,axiom,
( s2least(X13)
| equalish(X15,X14)
| ~ s(X13,X15)
| ~ s(X13,X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_11) ).
cnf(c11,plain,
( s2least(X51)
| equalish(X50,u3r1(X51))
| ~ s(X51,X50)
| s1most(X51) ),
inference(resolution,[status(thm)],[clause_11,clause_16]) ).
cnf(c71,plain,
( s2least(X66)
| equalish(u3r2(X66),u3r1(X66))
| s1most(X66) ),
inference(resolution,[status(thm)],[c11,clause_17]) ).
cnf(c100,plain,
( s2least(X69)
| s1most(X69) ),
inference(resolution,[status(thm)],[c71,clause_15]) ).
cnf(c105,plain,
( s2least(X71)
| d(X71) ),
inference(resolution,[status(thm)],[c100,clause_13]) ).
cnf(c110,plain,
( d(X85)
| s(X85,u1r2(X85)) ),
inference(resolution,[status(thm)],[c105,clause_10]) ).
cnf(c108,plain,
( d(X84)
| s(X84,u1r1(X84)) ),
inference(resolution,[status(thm)],[c105,clause_9]) ).
cnf(c104,plain,
( s1most(X83)
| s(X83,u1r2(X83)) ),
inference(resolution,[status(thm)],[c100,clause_10]) ).
cnf(c102,plain,
( s1most(X80)
| s(X80,u1r1(X80)) ),
inference(resolution,[status(thm)],[c100,clause_9]) ).
cnf(clause_7,axiom,
( c(X3)
| ~ s2least(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_7) ).
cnf(c103,plain,
( s1most(X70)
| c(X70) ),
inference(resolution,[status(thm)],[c100,clause_7]) ).
cnf(c106,plain,
( c(X72)
| d(X72) ),
inference(resolution,[status(thm)],[c103,clause_13]) ).
cnf(c62,plain,
( equalish(X45,X45)
| ~ r1most(X44)
| ~ r(X44,X45) ),
inference(factor,[status(thm)],[clause_24]) ).
cnf(c70,plain,
( equalish(u4r1(exist),u4r1(exist))
| ~ r1most(exist) ),
inference(resolution,[status(thm)],[c62,clause_3]) ).
cnf(c94,plain,
equalish(u4r1(exist),u4r1(exist)),
inference(resolution,[status(thm)],[c70,clause_2]) ).
cnf(c69,plain,
( equalish(u4r2(exist),u4r2(exist))
| ~ r1most(exist) ),
inference(resolution,[status(thm)],[c62,c14]) ).
cnf(c91,plain,
equalish(u4r2(exist),u4r2(exist)),
inference(resolution,[status(thm)],[c69,clause_2]) ).
cnf(c10,plain,
( s2least(X31)
| equalish(X30,X30)
| ~ s(X31,X30) ),
inference(factor,[status(thm)],[clause_11]) ).
cnf(clause_25,axiom,
( r1most(X29)
| ~ equalish(u5r2(X29),u5r1(X29)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_25) ).
cnf(c12,plain,
( s(X25,u3r2(X25))
| d(X25) ),
inference(resolution,[status(thm)],[clause_17,clause_13]) ).
cnf(c9,plain,
( s(X24,u3r1(X24))
| d(X24) ),
inference(resolution,[status(thm)],[clause_16,clause_13]) ).
cnf(clause_27,axiom,
( r1most(X23)
| r(X23,u5r2(X23)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_27) ).
cnf(clause_26,axiom,
( r1most(X22)
| r(X22,u5r1(X22)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_26) ).
cnf(clause_21,axiom,
( r(X18,u4r1(X18))
| ~ e(X18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_21) ).
cnf(clause_20,axiom,
( c(u4r1(X10))
| ~ e(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_20) ).
cnf(clause_18,axiom,
( d(u4r2(X8))
| ~ e(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18) ).
cnf(clause_4,negated_conjecture,
d(u4r2(exist)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4) ).
cnf(clause_12,axiom,
( s1most(X4)
| ~ d(X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_12) ).
cnf(c1,plain,
s1most(u4r2(exist)),
inference(resolution,[status(thm)],[clause_12,clause_4]) ).
cnf(clause_22,axiom,
( r1most(X6)
| ~ e(X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_22) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : KRS006-1 : TPTP v8.1.2. Released v2.0.0.
% 0.11/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n029.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 00:07:53 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.54/0.72 % Version: 1.5
% 0.54/0.72 % SZS status Satisfiable
% 0.54/0.72 % SZS output start Saturation
% See solution above
% 0.54/0.72
% 0.54/0.72 % Initial clauses : 27
% 0.54/0.72 % Processed clauses : 97
% 0.54/0.72 % Factors computed : 4
% 0.54/0.72 % Resolvents computed: 344
% 0.54/0.72 % Tautologies deleted: 36
% 0.54/0.72 % Forward subsumed : 242
% 0.54/0.72 % Backward subsumed : 23
% 0.54/0.72 % -------- CPU Time ---------
% 0.54/0.72 % User time : 0.346 s
% 0.54/0.72 % System time : 0.018 s
% 0.54/0.72 % Total time : 0.364 s
%------------------------------------------------------------------------------