%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS007-1 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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.63s 0.79s
% Output : Saturation 0.63s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_3,axiom,
( s2least(X2)
| ~ c(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3) ).
cnf(clause_1,negated_conjecture,
e(exist),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1) ).
cnf(clause_17,axiom,
( c(u4r2(X11))
| ~ e(X11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_17) ).
cnf(c3,plain,
c(u4r2(exist)),
inference(resolution,[status(thm)],[clause_17,clause_1]) ).
cnf(c4,plain,
s2least(u4r2(exist)),
inference(resolution,[status(thm)],[c3,clause_3]) ).
cnf(clause_7,axiom,
( s(X12,u1r2(X12))
| ~ s2least(X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_7) ).
cnf(c7,plain,
s(u4r2(exist),u1r2(u4r2(exist))),
inference(resolution,[status(thm)],[clause_7,c4]) ).
cnf(clause_11,axiom,
( equalish(X24,X23)
| ~ s1most(X22)
| ~ s(X22,X24)
| ~ s(X22,X23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_11) ).
cnf(clause_5,axiom,
( ~ s2least(X5)
| ~ equalish(u1r2(X5),u1r1(X5)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
cnf(clause_13,axiom,
( s1most(X13)
| s(X13,u3r1(X13)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_13) ).
cnf(clause_6,axiom,
( s(X10,u1r1(X10))
| ~ s2least(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6) ).
cnf(c6,plain,
s(u4r2(exist),u1r1(u4r2(exist))),
inference(resolution,[status(thm)],[c4,clause_6]) ).
cnf(c33,plain,
( equalish(X106,u1r1(u4r2(exist)))
| ~ s1most(u4r2(exist))
| ~ s(u4r2(exist),X106) ),
inference(resolution,[status(thm)],[c6,clause_11]) ).
cnf(c145,plain,
( equalish(u1r2(u4r2(exist)),u1r1(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c33,c7]) ).
cnf(c220,plain,
( equalish(u1r2(u4r2(exist)),u1r1(u4r2(exist)))
| s(u4r2(exist),u3r1(u4r2(exist))) ),
inference(resolution,[status(thm)],[c145,clause_13]) ).
cnf(c265,plain,
( s(u4r2(exist),u3r1(u4r2(exist)))
| ~ s2least(u4r2(exist)) ),
inference(resolution,[status(thm)],[c220,clause_5]) ).
cnf(c278,plain,
s(u4r2(exist),u3r1(u4r2(exist))),
inference(resolution,[status(thm)],[c265,c4]) ).
cnf(c281,plain,
( equalish(X173,u3r1(u4r2(exist)))
| ~ s1most(u4r2(exist))
| ~ s(u4r2(exist),X173) ),
inference(resolution,[status(thm)],[c278,clause_11]) ).
cnf(c363,plain,
( equalish(u1r2(u4r2(exist)),u3r1(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c281,c7]) ).
cnf(clause_14,axiom,
( s1most(X14)
| s(X14,u3r2(X14)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_14) ).
cnf(c219,plain,
( equalish(u1r2(u4r2(exist)),u1r1(u4r2(exist)))
| s(u4r2(exist),u3r2(u4r2(exist))) ),
inference(resolution,[status(thm)],[c145,clause_14]) ).
cnf(c255,plain,
( s(u4r2(exist),u3r2(u4r2(exist)))
| ~ s2least(u4r2(exist)) ),
inference(resolution,[status(thm)],[c219,clause_5]) ).
cnf(c262,plain,
s(u4r2(exist),u3r2(u4r2(exist))),
inference(resolution,[status(thm)],[c255,c4]) ).
cnf(c361,plain,
( equalish(u3r2(u4r2(exist)),u3r1(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c281,c262]) ).
cnf(c358,plain,
( equalish(u1r1(u4r2(exist)),u3r1(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c281,c6]) ).
cnf(c272,plain,
( equalish(X170,u3r2(u4r2(exist)))
| ~ s1most(u4r2(exist))
| ~ s(u4r2(exist),X170) ),
inference(resolution,[status(thm)],[c262,clause_11]) ).
cnf(c333,plain,
( equalish(u1r2(u4r2(exist)),u3r2(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c272,c7]) ).
cnf(c332,plain,
( equalish(u3r1(u4r2(exist)),u3r2(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c272,c278]) ).
cnf(c328,plain,
( equalish(u1r1(u4r2(exist)),u3r2(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c272,c6]) ).
cnf(c37,plain,
( equalish(X119,u1r2(u4r2(exist)))
| ~ s1most(u4r2(exist))
| ~ s(u4r2(exist),X119) ),
inference(resolution,[status(thm)],[c7,clause_11]) ).
cnf(c286,plain,
( equalish(u3r1(u4r2(exist)),u1r2(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c278,c37]) ).
cnf(c16,plain,
( equalish(X35,X35)
| ~ s1most(X34)
| ~ s(X34,X35) ),
inference(factor,[status(thm)],[clause_11]) ).
cnf(c284,plain,
( equalish(u3r1(u4r2(exist)),u3r1(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c278,c16]) ).
cnf(c283,plain,
( equalish(u3r1(u4r2(exist)),u1r1(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c278,c33]) ).
cnf(c277,plain,
( equalish(u3r2(u4r2(exist)),u1r2(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c262,c37]) ).
cnf(c275,plain,
( equalish(u3r2(u4r2(exist)),u3r2(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c262,c16]) ).
cnf(c274,plain,
( equalish(u3r2(u4r2(exist)),u1r1(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c262,c33]) ).
cnf(c165,plain,
( equalish(u1r1(u4r2(exist)),u1r2(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c37,c6]) ).
cnf(clause_2,negated_conjecture,
~ f(exist),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2) ).
cnf(clause_22,axiom,
( f(X8)
| ~ r2least(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_22) ).
cnf(clause_16,axiom,
( r(X15,u4r3(X15))
| ~ e(X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_16) ).
cnf(c10,plain,
r(exist,u4r3(exist)),
inference(resolution,[status(thm)],[clause_16,clause_1]) ).
cnf(clause_18,axiom,
( r(X19,u4r2(X19))
| ~ e(X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_18) ).
cnf(c14,plain,
r(exist,u4r2(exist)),
inference(resolution,[status(thm)],[clause_18,clause_1]) ).
cnf(clause_26,axiom,
( r2least(X45)
| equalish(X47,X46)
| ~ r(X45,X47)
| ~ r(X45,X46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_26) ).
cnf(c65,plain,
( r2least(exist)
| equalish(X122,u4r2(exist))
| ~ r(exist,X122) ),
inference(resolution,[status(thm)],[clause_26,c14]) ).
cnf(c200,plain,
( r2least(exist)
| equalish(u4r3(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[c65,c10]) ).
cnf(c212,plain,
( equalish(u4r3(exist),u4r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[c200,clause_22]) ).
cnf(c218,plain,
equalish(u4r3(exist),u4r2(exist)),
inference(resolution,[status(thm)],[c212,clause_2]) ).
cnf(clause_19,axiom,
( r(X20,u4r1(X20))
| ~ e(X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_19) ).
cnf(c15,plain,
r(exist,u4r1(exist)),
inference(resolution,[status(thm)],[clause_19,clause_1]) ).
cnf(c199,plain,
( r2least(exist)
| equalish(u4r1(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[c65,c15]) ).
cnf(c202,plain,
( equalish(u4r1(exist),u4r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[c199,clause_22]) ).
cnf(c216,plain,
equalish(u4r1(exist),u4r2(exist)),
inference(resolution,[status(thm)],[c202,clause_2]) ).
cnf(clause_20,axiom,
( e(X37)
| ~ r(X37,X38)
| ~ r(X37,X39)
| ~ c(X39)
| ~ r(X37,X36)
| ~ d(X36) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_20) ).
cnf(c41,plain,
( e(X125)
| ~ r(X125,X124)
| ~ r(X125,X123)
| ~ c(X123)
| ~ d(X124) ),
inference(factor,[status(thm)],[clause_20]) ).
cnf(c205,plain,
( e(X126)
| ~ r(X126,X127)
| ~ c(X127)
| ~ d(X127) ),
inference(factor,[status(thm)],[c41]) ).
cnf(c64,plain,
( r2least(exist)
| equalish(X121,u4r3(exist))
| ~ r(exist,X121) ),
inference(resolution,[status(thm)],[clause_26,c10]) ).
cnf(c182,plain,
( r2least(exist)
| equalish(u4r2(exist),u4r3(exist)) ),
inference(resolution,[status(thm)],[c64,c14]) ).
cnf(c192,plain,
( equalish(u4r2(exist),u4r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[c182,clause_22]) ).
cnf(c198,plain,
equalish(u4r2(exist),u4r3(exist)),
inference(resolution,[status(thm)],[c192,clause_2]) ).
cnf(c180,plain,
( r2least(exist)
| equalish(u4r1(exist),u4r3(exist)) ),
inference(resolution,[status(thm)],[c64,c15]) ).
cnf(c183,plain,
( equalish(u4r1(exist),u4r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[c180,clause_22]) ).
cnf(c196,plain,
equalish(u4r1(exist),u4r3(exist)),
inference(resolution,[status(thm)],[c183,clause_2]) ).
cnf(c39,plain,
( equalish(u1r2(u4r2(exist)),u1r2(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c7,c16]) ).
cnf(c63,plain,
( r2least(exist)
| equalish(X118,u4r1(exist))
| ~ r(exist,X118) ),
inference(resolution,[status(thm)],[clause_26,c15]) ).
cnf(c159,plain,
( r2least(exist)
| equalish(u4r2(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[c63,c14]) ).
cnf(c173,plain,
( equalish(u4r2(exist),u4r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[c159,clause_22]) ).
cnf(c179,plain,
equalish(u4r2(exist),u4r1(exist)),
inference(resolution,[status(thm)],[c173,clause_2]) ).
cnf(c158,plain,
( r2least(exist)
| equalish(u4r3(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[c63,c10]) ).
cnf(c170,plain,
( equalish(u4r3(exist),u4r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[c158,clause_22]) ).
cnf(c177,plain,
equalish(u4r3(exist),u4r1(exist)),
inference(resolution,[status(thm)],[c170,clause_2]) ).
cnf(c35,plain,
( equalish(u1r1(u4r2(exist)),u1r1(u4r2(exist)))
| ~ s1most(u4r2(exist)) ),
inference(resolution,[status(thm)],[c6,c16]) ).
cnf(c62,plain,
( r2least(X49)
| equalish(X48,X48)
| ~ r(X49,X48) ),
inference(factor,[status(thm)],[clause_26]) ).
cnf(c68,plain,
( r2least(exist)
| equalish(u4r2(exist),u4r2(exist)) ),
inference(resolution,[status(thm)],[c62,c14]) ).
cnf(c95,plain,
( equalish(u4r2(exist),u4r2(exist))
| f(exist) ),
inference(resolution,[status(thm)],[c68,clause_22]) ).
cnf(c150,plain,
equalish(u4r2(exist),u4r2(exist)),
inference(resolution,[status(thm)],[c95,clause_2]) ).
cnf(c67,plain,
( r2least(exist)
| equalish(u4r3(exist),u4r3(exist)) ),
inference(resolution,[status(thm)],[c62,c10]) ).
cnf(c92,plain,
( equalish(u4r3(exist),u4r3(exist))
| f(exist) ),
inference(resolution,[status(thm)],[c67,clause_22]) ).
cnf(c148,plain,
equalish(u4r3(exist),u4r3(exist)),
inference(resolution,[status(thm)],[c92,clause_2]) ).
cnf(c66,plain,
( r2least(exist)
| equalish(u4r1(exist),u4r1(exist)) ),
inference(resolution,[status(thm)],[c62,c15]) ).
cnf(c89,plain,
( equalish(u4r1(exist),u4r1(exist))
| f(exist) ),
inference(resolution,[status(thm)],[c66,clause_22]) ).
cnf(c136,plain,
equalish(u4r1(exist),u4r1(exist)),
inference(resolution,[status(thm)],[c89,clause_2]) ).
cnf(clause_10,axiom,
( d(X6)
| ~ s1most(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_10) ).
cnf(clause_12,axiom,
( s1most(X30)
| ~ equalish(u3r2(X30),u3r1(X30)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_12) ).
cnf(clause_8,axiom,
( s2least(X16)
| equalish(X18,X17)
| ~ s(X16,X18)
| ~ s(X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_8) ).
cnf(c12,plain,
( s2least(X55)
| equalish(X54,u3r1(X55))
| ~ s(X55,X54)
| s1most(X55) ),
inference(resolution,[status(thm)],[clause_8,clause_13]) ).
cnf(c72,plain,
( s2least(X69)
| equalish(u3r2(X69),u3r1(X69))
| s1most(X69) ),
inference(resolution,[status(thm)],[c12,clause_14]) ).
cnf(c101,plain,
( s2least(X70)
| s1most(X70) ),
inference(resolution,[status(thm)],[c72,clause_12]) ).
cnf(c106,plain,
( s2least(X74)
| d(X74) ),
inference(resolution,[status(thm)],[c101,clause_10]) ).
cnf(c111,plain,
( d(X88)
| s(X88,u1r1(X88)) ),
inference(resolution,[status(thm)],[c106,clause_6]) ).
cnf(c110,plain,
( d(X85)
| s(X85,u1r2(X85)) ),
inference(resolution,[status(thm)],[c106,clause_7]) ).
cnf(c105,plain,
( s1most(X84)
| s(X84,u1r1(X84)) ),
inference(resolution,[status(thm)],[c101,clause_6]) ).
cnf(c104,plain,
( s1most(X83)
| s(X83,u1r2(X83)) ),
inference(resolution,[status(thm)],[c101,clause_7]) ).
cnf(clause_4,axiom,
( c(X3)
| ~ s2least(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4) ).
cnf(c103,plain,
( s1most(X71)
| c(X71) ),
inference(resolution,[status(thm)],[c101,clause_4]) ).
cnf(c107,plain,
( c(X75)
| d(X75) ),
inference(resolution,[status(thm)],[c103,clause_10]) ).
cnf(c11,plain,
( s2least(X33)
| equalish(X32,X32)
| ~ s(X33,X32) ),
inference(factor,[status(thm)],[clause_8]) ).
cnf(clause_23,axiom,
( ~ r2least(X31)
| ~ equalish(u6r2(X31),u6r1(X31)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_23) ).
cnf(c9,plain,
( s(X27,u3r2(X27))
| d(X27) ),
inference(resolution,[status(thm)],[clause_14,clause_10]) ).
cnf(c8,plain,
( s(X26,u3r1(X26))
| d(X26) ),
inference(resolution,[status(thm)],[clause_13,clause_10]) ).
cnf(clause_25,axiom,
( r(X25,u6r2(X25))
| ~ r2least(X25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_25) ).
cnf(clause_24,axiom,
( r(X21,u6r1(X21))
| ~ r2least(X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_24) ).
cnf(clause_9,axiom,
( s1most(X4)
| ~ d(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_9) ).
cnf(clause_15,axiom,
( d(u4r3(X9))
| ~ e(X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_15) ).
cnf(c0,plain,
d(u4r3(exist)),
inference(resolution,[status(thm)],[clause_15,clause_1]) ).
cnf(c1,plain,
s1most(u4r3(exist)),
inference(resolution,[status(thm)],[c0,clause_9]) ).
cnf(clause_21,axiom,
( r2least(X7)
| ~ f(X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_21) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : KRS007-1 : TPTP v8.1.2. Released v2.0.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n026.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 00:06:23 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.63/0.79 % Version: 1.5
% 0.63/0.79 % SZS status Satisfiable
% 0.63/0.79 % SZS output start Saturation
% See solution above
% 0.63/0.79
% 0.63/0.79 % Initial clauses : 26
% 0.63/0.79 % Processed clauses : 121
% 0.63/0.79 % Factors computed : 6
% 0.63/0.79 % Resolvents computed: 377
% 0.63/0.79 % Tautologies deleted: 24
% 0.63/0.79 % Forward subsumed : 264
% 0.63/0.79 % Backward subsumed : 38
% 0.63/0.79 % -------- CPU Time ---------
% 0.63/0.79 % User time : 0.431 s
% 0.63/0.79 % System time : 0.010 s
% 0.63/0.79 % Total time : 0.441 s
%------------------------------------------------------------------------------