%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS016-1 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:28 EDT 2024
% Result : Satisfiable 30.88s 31.10s
% Output : Saturation 30.88s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_11,axiom,
( r1most(X7)
| r(X7,u1r2(X7)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_11) ).
cnf(clause_8,axiom,
( equalish(X27,X26)
| ~ r1most(X28)
| ~ r(X28,X27)
| ~ r(X28,X26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_8) ).
cnf(c19,plain,
( equalish(X30,X30)
| ~ r1most(X29)
| ~ r(X29,X30) ),
inference(factor,[status(thm)],[clause_8]) ).
cnf(clause_6,axiom,
( c(X18)
| s(X18,u0r1(X18))
| r(X18,u0r1(X18))
| ~ r1most(X18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6) ).
cnf(c15,plain,
( c(X50)
| s(X50,u0r1(X50))
| r(X50,u0r1(X50))
| r(X50,u1r2(X50)) ),
inference(resolution,[status(thm)],[clause_6,clause_11]) ).
cnf(c71,plain,
( c(X139)
| s(X139,u0r1(X139))
| r(X139,u1r2(X139))
| equalish(u0r1(X139),u0r1(X139))
| ~ r1most(X139) ),
inference(resolution,[status(thm)],[c15,c19]) ).
cnf(c257,plain,
( c(X142)
| s(X142,u0r1(X142))
| r(X142,u1r2(X142))
| equalish(u0r1(X142),u0r1(X142)) ),
inference(resolution,[status(thm)],[c71,clause_11]) ).
cnf(clause_3,axiom,
( s(X5,X4)
| ~ c(X5)
| ~ r(X5,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3) ).
cnf(clause_17,axiom,
( s1most(X15)
| ~ equalish(u3r2(X15),u3r1(X15)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_17) ).
cnf(clause_19,axiom,
( s1most(X9)
| s(X9,u3r2(X9)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_19) ).
cnf(clause_4,axiom,
( r(X11,X10)
| ~ c(X11)
| ~ s(X11,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4) ).
cnf(c5,plain,
( r(X22,u3r2(X22))
| ~ c(X22)
| s1most(X22) ),
inference(resolution,[status(thm)],[clause_4,clause_19]) ).
cnf(c63,plain,
( s(X115,u0r1(X115))
| r(X115,u0r1(X115))
| r(X115,u1r2(X115))
| r(X115,u3r2(X115))
| s1most(X115) ),
inference(resolution,[status(thm)],[c15,c5]) ).
cnf(clause_18,axiom,
( s1most(X8)
| s(X8,u3r1(X8)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18) ).
cnf(c4,plain,
( r(X21,u3r1(X21))
| ~ c(X21)
| s1most(X21) ),
inference(resolution,[status(thm)],[clause_4,clause_18]) ).
cnf(c64,plain,
( s(X119,u0r1(X119))
| r(X119,u0r1(X119))
| r(X119,u1r2(X119))
| r(X119,u3r1(X119))
| s1most(X119) ),
inference(resolution,[status(thm)],[c15,c4]) ).
cnf(c214,plain,
( s(X542,u0r1(X542))
| r(X542,u0r1(X542))
| r(X542,u1r2(X542))
| s1most(X542)
| equalish(X543,u3r1(X542))
| ~ r1most(X542)
| ~ r(X542,X543) ),
inference(resolution,[status(thm)],[c64,clause_8]) ).
cnf(c2960,plain,
( s(X654,u0r1(X654))
| r(X654,u0r1(X654))
| r(X654,u1r2(X654))
| s1most(X654)
| equalish(u3r2(X654),u3r1(X654))
| ~ r1most(X654) ),
inference(resolution,[status(thm)],[c214,c63]) ).
cnf(c3641,plain,
( s(X656,u0r1(X656))
| r(X656,u0r1(X656))
| r(X656,u1r2(X656))
| s1most(X656)
| equalish(u3r2(X656),u3r1(X656)) ),
inference(resolution,[status(thm)],[c2960,clause_11]) ).
cnf(c3733,plain,
( s(X657,u0r1(X657))
| r(X657,u0r1(X657))
| r(X657,u1r2(X657))
| s1most(X657) ),
inference(resolution,[status(thm)],[c3641,clause_17]) ).
cnf(clause_16,axiom,
( equalish(X34,X33)
| ~ s1most(X35)
| ~ s(X35,X34)
| ~ s(X35,X33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16) ).
cnf(c24,plain,
( equalish(X37,X37)
| ~ s1most(X36)
| ~ s(X36,X37) ),
inference(factor,[status(thm)],[clause_16]) ).
cnf(clause_14,axiom,
( d(X16)
| s(X16,u2r1(X16))
| ~ s1most(X16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_14) ).
cnf(c3787,plain,
( s(X680,u0r1(X680))
| r(X680,u0r1(X680))
| r(X680,u1r2(X680))
| d(X680)
| s(X680,u2r1(X680)) ),
inference(resolution,[status(thm)],[c3733,clause_14]) ).
cnf(c4007,plain,
( s(X830,u0r1(X830))
| r(X830,u0r1(X830))
| r(X830,u1r2(X830))
| d(X830)
| equalish(u2r1(X830),u2r1(X830))
| ~ s1most(X830) ),
inference(resolution,[status(thm)],[c3787,c24]) ).
cnf(c5227,plain,
( s(X831,u0r1(X831))
| r(X831,u0r1(X831))
| r(X831,u1r2(X831))
| d(X831)
| equalish(u2r1(X831),u2r1(X831)) ),
inference(resolution,[status(thm)],[c4007,c3733]) ).
cnf(c5249,plain,
( s(X834,u0r1(X834))
| r(X834,u1r2(X834))
| d(X834)
| equalish(u2r1(X834),u2r1(X834))
| ~ c(X834) ),
inference(resolution,[status(thm)],[c5227,clause_3]) ).
cnf(c5299,plain,
( s(X839,u0r1(X839))
| r(X839,u1r2(X839))
| d(X839)
| equalish(u2r1(X839),u2r1(X839))
| equalish(u0r1(X839),u0r1(X839)) ),
inference(resolution,[status(thm)],[c5249,c257]) ).
cnf(clause_10,axiom,
( r1most(X6)
| r(X6,u1r1(X6)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_10) ).
cnf(c16,plain,
( c(X59)
| s(X59,u0r1(X59))
| r(X59,u0r1(X59))
| r(X59,u1r1(X59)) ),
inference(resolution,[status(thm)],[clause_6,clause_10]) ).
cnf(c85,plain,
( c(X183)
| s(X183,u0r1(X183))
| r(X183,u1r1(X183))
| equalish(u0r1(X183),u0r1(X183))
| ~ r1most(X183) ),
inference(resolution,[status(thm)],[c16,c19]) ).
cnf(c473,plain,
( c(X184)
| s(X184,u0r1(X184))
| r(X184,u1r1(X184))
| equalish(u0r1(X184),u0r1(X184)) ),
inference(resolution,[status(thm)],[c85,clause_10]) ).
cnf(c77,plain,
( s(X162,u0r1(X162))
| r(X162,u0r1(X162))
| r(X162,u1r1(X162))
| r(X162,u3r2(X162))
| s1most(X162) ),
inference(resolution,[status(thm)],[c16,c5]) ).
cnf(c78,plain,
( s(X167,u0r1(X167))
| r(X167,u0r1(X167))
| r(X167,u1r1(X167))
| r(X167,u3r1(X167))
| s1most(X167) ),
inference(resolution,[status(thm)],[c16,c4]) ).
cnf(c432,plain,
( s(X1069,u0r1(X1069))
| r(X1069,u0r1(X1069))
| r(X1069,u1r1(X1069))
| s1most(X1069)
| equalish(X1070,u3r1(X1069))
| ~ r1most(X1069)
| ~ r(X1069,X1070) ),
inference(resolution,[status(thm)],[c78,clause_8]) ).
cnf(c7764,plain,
( s(X1072,u0r1(X1072))
| r(X1072,u0r1(X1072))
| r(X1072,u1r1(X1072))
| s1most(X1072)
| equalish(u3r2(X1072),u3r1(X1072))
| ~ r1most(X1072) ),
inference(resolution,[status(thm)],[c432,c77]) ).
cnf(c7856,plain,
( s(X1073,u0r1(X1073))
| r(X1073,u0r1(X1073))
| r(X1073,u1r1(X1073))
| s1most(X1073)
| equalish(u3r2(X1073),u3r1(X1073)) ),
inference(resolution,[status(thm)],[c7764,clause_10]) ).
cnf(c7949,plain,
( s(X1074,u0r1(X1074))
| r(X1074,u0r1(X1074))
| r(X1074,u1r1(X1074))
| s1most(X1074) ),
inference(resolution,[status(thm)],[c7856,clause_17]) ).
cnf(c8031,plain,
( s(X1098,u0r1(X1098))
| r(X1098,u0r1(X1098))
| r(X1098,u1r1(X1098))
| d(X1098)
| s(X1098,u2r1(X1098)) ),
inference(resolution,[status(thm)],[c7949,clause_14]) ).
cnf(c8241,plain,
( s(X1226,u0r1(X1226))
| r(X1226,u0r1(X1226))
| r(X1226,u1r1(X1226))
| d(X1226)
| equalish(u2r1(X1226),u2r1(X1226))
| ~ s1most(X1226) ),
inference(resolution,[status(thm)],[c8031,c24]) ).
cnf(c8732,plain,
( s(X1228,u0r1(X1228))
| r(X1228,u0r1(X1228))
| r(X1228,u1r1(X1228))
| d(X1228)
| equalish(u2r1(X1228),u2r1(X1228)) ),
inference(resolution,[status(thm)],[c8241,c7949]) ).
cnf(c8763,plain,
( s(X1230,u0r1(X1230))
| r(X1230,u1r1(X1230))
| d(X1230)
| equalish(u2r1(X1230),u2r1(X1230))
| ~ c(X1230) ),
inference(resolution,[status(thm)],[c8732,clause_3]) ).
cnf(c8825,plain,
( s(X1235,u0r1(X1235))
| r(X1235,u1r1(X1235))
| d(X1235)
| equalish(u2r1(X1235),u2r1(X1235))
| equalish(u0r1(X1235),u0r1(X1235)) ),
inference(resolution,[status(thm)],[c8763,c473]) ).
cnf(c8864,plain,
( s(X4115,u0r1(X4115))
| d(X4115)
| equalish(u2r1(X4115),u2r1(X4115))
| equalish(u0r1(X4115),u0r1(X4115))
| equalish(X4116,u1r1(X4115))
| ~ r1most(X4115)
| ~ r(X4115,X4116) ),
inference(resolution,[status(thm)],[c8825,clause_8]) ).
cnf(c12788,plain,
( s(X4118,u0r1(X4118))
| d(X4118)
| equalish(u2r1(X4118),u2r1(X4118))
| equalish(u0r1(X4118),u0r1(X4118))
| equalish(u1r2(X4118),u1r1(X4118))
| ~ r1most(X4118) ),
inference(resolution,[status(thm)],[c8864,c5299]) ).
cnf(c5326,plain,
( s(X3985,u0r1(X3985))
| d(X3985)
| equalish(u2r1(X3985),u2r1(X3985))
| equalish(u0r1(X3985),u0r1(X3985))
| equalish(X3986,u1r2(X3985))
| ~ r1most(X3985)
| ~ r(X3985,X3986) ),
inference(resolution,[status(thm)],[c5299,clause_8]) ).
cnf(c12711,plain,
( s(X3987,u0r1(X3987))
| d(X3987)
| equalish(u2r1(X3987),u2r1(X3987))
| equalish(u0r1(X3987),u0r1(X3987))
| equalish(u1r1(X3987),u1r2(X3987))
| ~ r1most(X3987) ),
inference(resolution,[status(thm)],[c5326,c8825]) ).
cnf(c8,plain,
( d(X38)
| s(X38,u2r1(X38))
| s(X38,u3r2(X38)) ),
inference(resolution,[status(thm)],[clause_14,clause_19]) ).
cnf(c82,plain,
( c(X180)
| r(X180,u0r1(X180))
| r(X180,u1r1(X180))
| equalish(X179,u0r1(X180))
| ~ s1most(X180)
| ~ s(X180,X179) ),
inference(resolution,[status(thm)],[c16,clause_16]) ).
cnf(c468,plain,
( c(X1317)
| r(X1317,u0r1(X1317))
| r(X1317,u1r1(X1317))
| equalish(u2r1(X1317),u0r1(X1317))
| ~ s1most(X1317)
| d(X1317)
| s(X1317,u3r2(X1317)) ),
inference(resolution,[status(thm)],[c82,c8]) ).
cnf(c8952,plain,
( c(X1318)
| r(X1318,u0r1(X1318))
| r(X1318,u1r1(X1318))
| equalish(u2r1(X1318),u0r1(X1318))
| d(X1318)
| s(X1318,u3r2(X1318)) ),
inference(resolution,[status(thm)],[c468,clause_19]) ).
cnf(clause_7,axiom,
( c(X24)
| ~ r1most(X24)
| ~ r(X24,u0r1(X24))
| ~ s(X24,u0r1(X24)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_7) ).
cnf(clause_15,axiom,
( d(X17)
| r(X17,u2r1(X17))
| ~ s1most(X17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_15) ).
cnf(c11,plain,
( d(X42)
| r(X42,u2r1(X42))
| s(X42,u3r2(X42)) ),
inference(resolution,[status(thm)],[clause_15,clause_19]) ).
cnf(c86,plain,
( c(X186)
| s(X186,u0r1(X186))
| r(X186,u1r1(X186))
| equalish(X187,u0r1(X186))
| ~ r1most(X186)
| ~ r(X186,X187) ),
inference(resolution,[status(thm)],[c16,clause_8]) ).
cnf(c523,plain,
( c(X1505)
| s(X1505,u0r1(X1505))
| r(X1505,u1r1(X1505))
| equalish(u2r1(X1505),u0r1(X1505))
| ~ r1most(X1505)
| d(X1505)
| s(X1505,u3r2(X1505)) ),
inference(resolution,[status(thm)],[c86,c11]) ).
cnf(c9622,plain,
( c(X1506)
| s(X1506,u0r1(X1506))
| r(X1506,u1r1(X1506))
| equalish(u2r1(X1506),u0r1(X1506))
| d(X1506)
| s(X1506,u3r2(X1506)) ),
inference(resolution,[status(thm)],[c523,clause_10]) ).
cnf(c9673,plain,
( c(X2456)
| r(X2456,u1r1(X2456))
| equalish(u2r1(X2456),u0r1(X2456))
| d(X2456)
| s(X2456,u3r2(X2456))
| ~ r1most(X2456)
| ~ r(X2456,u0r1(X2456)) ),
inference(resolution,[status(thm)],[c9622,clause_7]) ).
cnf(c11628,plain,
( c(X2457)
| r(X2457,u1r1(X2457))
| equalish(u2r1(X2457),u0r1(X2457))
| d(X2457)
| s(X2457,u3r2(X2457))
| ~ r1most(X2457) ),
inference(resolution,[status(thm)],[c9673,c8952]) ).
cnf(c11633,plain,
( c(X2458)
| r(X2458,u1r1(X2458))
| equalish(u2r1(X2458),u0r1(X2458))
| d(X2458)
| s(X2458,u3r2(X2458)) ),
inference(resolution,[status(thm)],[c11628,clause_10]) ).
cnf(c11724,plain,
( c(X2484)
| r(X2484,u1r1(X2484))
| equalish(u2r1(X2484),u0r1(X2484))
| d(X2484)
| equalish(X2483,u3r2(X2484))
| ~ s1most(X2484)
| ~ s(X2484,X2483) ),
inference(resolution,[status(thm)],[c11633,clause_16]) ).
cnf(c11850,plain,
( c(X3646)
| r(X3646,u1r1(X3646))
| equalish(u2r1(X3646),u0r1(X3646))
| d(X3646)
| equalish(u0r1(X3646),u3r2(X3646))
| ~ s1most(X3646)
| r(X3646,u0r1(X3646)) ),
inference(resolution,[status(thm)],[c11724,c16]) ).
cnf(c9,plain,
( d(X41)
| s(X41,u2r1(X41))
| s(X41,u3r1(X41)) ),
inference(resolution,[status(thm)],[clause_14,clause_18]) ).
cnf(c470,plain,
( c(X1329)
| r(X1329,u0r1(X1329))
| r(X1329,u1r1(X1329))
| equalish(u2r1(X1329),u0r1(X1329))
| ~ s1most(X1329)
| d(X1329)
| s(X1329,u3r1(X1329)) ),
inference(resolution,[status(thm)],[c82,c9]) ).
cnf(c9064,plain,
( c(X1330)
| r(X1330,u0r1(X1330))
| r(X1330,u1r1(X1330))
| equalish(u2r1(X1330),u0r1(X1330))
| d(X1330)
| s(X1330,u3r1(X1330)) ),
inference(resolution,[status(thm)],[c470,clause_18]) ).
cnf(c12,plain,
( d(X43)
| r(X43,u2r1(X43))
| s(X43,u3r1(X43)) ),
inference(resolution,[status(thm)],[clause_15,clause_18]) ).
cnf(c515,plain,
( c(X1475)
| s(X1475,u0r1(X1475))
| r(X1475,u1r1(X1475))
| equalish(u2r1(X1475),u0r1(X1475))
| ~ r1most(X1475)
| d(X1475)
| s(X1475,u3r1(X1475)) ),
inference(resolution,[status(thm)],[c86,c12]) ).
cnf(c9510,plain,
( c(X1476)
| s(X1476,u0r1(X1476))
| r(X1476,u1r1(X1476))
| equalish(u2r1(X1476),u0r1(X1476))
| d(X1476)
| s(X1476,u3r1(X1476)) ),
inference(resolution,[status(thm)],[c515,clause_10]) ).
cnf(c9561,plain,
( c(X2395)
| r(X2395,u1r1(X2395))
| equalish(u2r1(X2395),u0r1(X2395))
| d(X2395)
| s(X2395,u3r1(X2395))
| ~ r1most(X2395)
| ~ r(X2395,u0r1(X2395)) ),
inference(resolution,[status(thm)],[c9510,clause_7]) ).
cnf(c11296,plain,
( c(X2396)
| r(X2396,u1r1(X2396))
| equalish(u2r1(X2396),u0r1(X2396))
| d(X2396)
| s(X2396,u3r1(X2396))
| ~ r1most(X2396) ),
inference(resolution,[status(thm)],[c9561,c9064]) ).
cnf(c11299,plain,
( c(X2397)
| r(X2397,u1r1(X2397))
| equalish(u2r1(X2397),u0r1(X2397))
| d(X2397)
| s(X2397,u3r1(X2397)) ),
inference(resolution,[status(thm)],[c11296,clause_10]) ).
cnf(c11388,plain,
( c(X2422)
| r(X2422,u1r1(X2422))
| equalish(u2r1(X2422),u0r1(X2422))
| d(X2422)
| equalish(X2421,u3r1(X2422))
| ~ s1most(X2422)
| ~ s(X2422,X2421) ),
inference(resolution,[status(thm)],[c11299,clause_16]) ).
cnf(c11517,plain,
( c(X3611)
| r(X3611,u1r1(X3611))
| equalish(u2r1(X3611),u0r1(X3611))
| d(X3611)
| equalish(u0r1(X3611),u3r1(X3611))
| ~ s1most(X3611)
| r(X3611,u0r1(X3611)) ),
inference(resolution,[status(thm)],[c11388,c16]) ).
cnf(c68,plain,
( c(X132)
| r(X132,u0r1(X132))
| r(X132,u1r2(X132))
| equalish(X131,u0r1(X132))
| ~ s1most(X132)
| ~ s(X132,X131) ),
inference(resolution,[status(thm)],[c15,clause_16]) ).
cnf(c241,plain,
( c(X637)
| r(X637,u0r1(X637))
| r(X637,u1r2(X637))
| equalish(u2r1(X637),u0r1(X637))
| ~ s1most(X637)
| d(X637)
| s(X637,u3r1(X637)) ),
inference(resolution,[status(thm)],[c68,c9]) ).
cnf(c3590,plain,
( c(X812)
| r(X812,u0r1(X812))
| r(X812,u1r2(X812))
| equalish(u2r1(X812),u0r1(X812))
| d(X812)
| s(X812,u3r1(X812)) ),
inference(resolution,[status(thm)],[c241,clause_18]) ).
cnf(c72,plain,
( c(X144)
| s(X144,u0r1(X144))
| r(X144,u1r2(X144))
| equalish(X145,u0r1(X144))
| ~ r1most(X144)
| ~ r(X144,X145) ),
inference(resolution,[status(thm)],[c15,clause_8]) ).
cnf(c306,plain,
( c(X797)
| s(X797,u0r1(X797))
| r(X797,u1r2(X797))
| equalish(u2r1(X797),u0r1(X797))
| ~ r1most(X797)
| d(X797)
| s(X797,u3r1(X797)) ),
inference(resolution,[status(thm)],[c72,c12]) ).
cnf(c5060,plain,
( c(X908)
| s(X908,u0r1(X908))
| r(X908,u1r2(X908))
| equalish(u2r1(X908),u0r1(X908))
| d(X908)
| s(X908,u3r1(X908)) ),
inference(resolution,[status(thm)],[c306,clause_11]) ).
cnf(c5804,plain,
( c(X2084)
| r(X2084,u1r2(X2084))
| equalish(u2r1(X2084),u0r1(X2084))
| d(X2084)
| s(X2084,u3r1(X2084))
| ~ r1most(X2084)
| ~ r(X2084,u0r1(X2084)) ),
inference(resolution,[status(thm)],[c5060,clause_7]) ).
cnf(c10761,plain,
( c(X2086)
| r(X2086,u1r2(X2086))
| equalish(u2r1(X2086),u0r1(X2086))
| d(X2086)
| s(X2086,u3r1(X2086))
| ~ r1most(X2086) ),
inference(resolution,[status(thm)],[c5804,c3590]) ).
cnf(c10765,plain,
( c(X2087)
| r(X2087,u1r2(X2087))
| equalish(u2r1(X2087),u0r1(X2087))
| d(X2087)
| s(X2087,u3r1(X2087)) ),
inference(resolution,[status(thm)],[c10761,clause_11]) ).
cnf(c10853,plain,
( c(X2110)
| r(X2110,u1r2(X2110))
| equalish(u2r1(X2110),u0r1(X2110))
| d(X2110)
| equalish(X2109,u3r1(X2110))
| ~ s1most(X2110)
| ~ s(X2110,X2109) ),
inference(resolution,[status(thm)],[c10765,clause_16]) ).
cnf(c10960,plain,
( c(X3568)
| r(X3568,u1r2(X3568))
| equalish(u2r1(X3568),u0r1(X3568))
| d(X3568)
| equalish(u0r1(X3568),u3r1(X3568))
| ~ s1most(X3568)
| r(X3568,u0r1(X3568)) ),
inference(resolution,[status(thm)],[c10853,c15]) ).
cnf(c239,plain,
( c(X625)
| r(X625,u0r1(X625))
| r(X625,u1r2(X625))
| equalish(u2r1(X625),u0r1(X625))
| ~ s1most(X625)
| d(X625)
| s(X625,u3r2(X625)) ),
inference(resolution,[status(thm)],[c68,c8]) ).
cnf(c3523,plain,
( c(X811)
| r(X811,u0r1(X811))
| r(X811,u1r2(X811))
| equalish(u2r1(X811),u0r1(X811))
| d(X811)
| s(X811,u3r2(X811)) ),
inference(resolution,[status(thm)],[c239,clause_19]) ).
cnf(c303,plain,
( c(X785)
| s(X785,u0r1(X785))
| r(X785,u1r2(X785))
| equalish(u2r1(X785),u0r1(X785))
| ~ r1most(X785)
| d(X785)
| s(X785,u3r2(X785)) ),
inference(resolution,[status(thm)],[c72,c11]) ).
cnf(c5012,plain,
( c(X907)
| s(X907,u0r1(X907))
| r(X907,u1r2(X907))
| equalish(u2r1(X907),u0r1(X907))
| d(X907)
| s(X907,u3r2(X907)) ),
inference(resolution,[status(thm)],[c303,clause_11]) ).
cnf(c5728,plain,
( c(X2024)
| r(X2024,u1r2(X2024))
| equalish(u2r1(X2024),u0r1(X2024))
| d(X2024)
| s(X2024,u3r2(X2024))
| ~ r1most(X2024)
| ~ r(X2024,u0r1(X2024)) ),
inference(resolution,[status(thm)],[c5012,clause_7]) ).
cnf(c10157,plain,
( c(X2025)
| r(X2025,u1r2(X2025))
| equalish(u2r1(X2025),u0r1(X2025))
| d(X2025)
| s(X2025,u3r2(X2025))
| ~ r1most(X2025) ),
inference(resolution,[status(thm)],[c5728,c3523]) ).
cnf(c10162,plain,
( c(X2026)
| r(X2026,u1r2(X2026))
| equalish(u2r1(X2026),u0r1(X2026))
| d(X2026)
| s(X2026,u3r2(X2026)) ),
inference(resolution,[status(thm)],[c10157,clause_11]) ).
cnf(c10249,plain,
( c(X2049)
| r(X2049,u1r2(X2049))
| equalish(u2r1(X2049),u0r1(X2049))
| d(X2049)
| equalish(X2048,u3r2(X2049))
| ~ s1most(X2049)
| ~ s(X2049,X2048) ),
inference(resolution,[status(thm)],[c10162,clause_16]) ).
cnf(c10347,plain,
( c(X3526)
| r(X3526,u1r2(X3526))
| equalish(u2r1(X3526),u0r1(X3526))
| d(X3526)
| equalish(u0r1(X3526),u3r2(X3526))
| ~ s1most(X3526)
| r(X3526,u0r1(X3526)) ),
inference(resolution,[status(thm)],[c10249,c15]) ).
cnf(c9160,plain,
( c(X3453)
| r(X3453,u0r1(X3453))
| r(X3453,u1r1(X3453))
| equalish(u2r1(X3453),u0r1(X3453))
| d(X3453)
| equalish(u3r1(X3453),u0r1(X3453))
| ~ s1most(X3453) ),
inference(resolution,[status(thm)],[c9064,c82]) ).
cnf(c9051,plain,
( c(X3444)
| r(X3444,u0r1(X3444))
| r(X3444,u1r1(X3444))
| equalish(u2r1(X3444),u0r1(X3444))
| d(X3444)
| equalish(u3r2(X3444),u0r1(X3444))
| ~ s1most(X3444) ),
inference(resolution,[status(thm)],[c8952,c82]) ).
cnf(c57,plain,
( d(X109)
| s(X109,u3r1(X109))
| equalish(X110,u2r1(X109))
| ~ r1most(X109)
| ~ r(X109,X110) ),
inference(resolution,[status(thm)],[c12,clause_8]) ).
cnf(c41,plain,
( d(X92)
| s(X92,u3r1(X92))
| equalish(X91,u2r1(X92))
| ~ s1most(X92)
| ~ s(X92,X91) ),
inference(resolution,[status(thm)],[c9,clause_16]) ).
cnf(c137,plain,
( d(X277)
| s(X277,u3r1(X277))
| equalish(u0r1(X277),u2r1(X277))
| ~ s1most(X277)
| c(X277)
| r(X277,u0r1(X277))
| r(X277,u1r2(X277)) ),
inference(resolution,[status(thm)],[c41,c15]) ).
cnf(c1008,plain,
( d(X565)
| s(X565,u3r1(X565))
| equalish(u0r1(X565),u2r1(X565))
| c(X565)
| r(X565,u0r1(X565))
| r(X565,u1r2(X565)) ),
inference(resolution,[status(thm)],[c137,clause_18]) ).
cnf(c3239,plain,
( d(X566)
| s(X566,u3r1(X566))
| equalish(u0r1(X566),u2r1(X566))
| c(X566)
| r(X566,u1r2(X566))
| ~ r1most(X566) ),
inference(resolution,[status(thm)],[c1008,c57]) ).
cnf(c3269,plain,
( d(X568)
| s(X568,u3r1(X568))
| equalish(u0r1(X568),u2r1(X568))
| c(X568)
| r(X568,u1r2(X568)) ),
inference(resolution,[status(thm)],[c3239,clause_11]) ).
cnf(c3278,plain,
( d(X980)
| equalish(u0r1(X980),u2r1(X980))
| c(X980)
| r(X980,u1r2(X980))
| equalish(X979,u3r1(X980))
| ~ s1most(X980)
| ~ s(X980,X979) ),
inference(resolution,[status(thm)],[c3269,clause_16]) ).
cnf(c6467,plain,
( d(X3286)
| equalish(u0r1(X3286),u2r1(X3286))
| c(X3286)
| r(X3286,u1r2(X3286))
| equalish(u0r1(X3286),u3r1(X3286))
| ~ s1most(X3286)
| r(X3286,u0r1(X3286)) ),
inference(resolution,[status(thm)],[c3278,c15]) ).
cnf(c133,plain,
( d(X271)
| s(X271,u3r1(X271))
| equalish(u0r1(X271),u2r1(X271))
| ~ s1most(X271)
| c(X271)
| r(X271,u0r1(X271))
| r(X271,u1r1(X271)) ),
inference(resolution,[status(thm)],[c41,c16]) ).
cnf(c1001,plain,
( d(X552)
| s(X552,u3r1(X552))
| equalish(u0r1(X552),u2r1(X552))
| c(X552)
| r(X552,u0r1(X552))
| r(X552,u1r1(X552)) ),
inference(resolution,[status(thm)],[c133,clause_18]) ).
cnf(c3096,plain,
( d(X553)
| s(X553,u3r1(X553))
| equalish(u0r1(X553),u2r1(X553))
| c(X553)
| r(X553,u1r1(X553))
| ~ r1most(X553) ),
inference(resolution,[status(thm)],[c1001,c57]) ).
cnf(c3127,plain,
( d(X554)
| s(X554,u3r1(X554))
| equalish(u0r1(X554),u2r1(X554))
| c(X554)
| r(X554,u1r1(X554)) ),
inference(resolution,[status(thm)],[c3096,clause_10]) ).
cnf(c3135,plain,
( d(X970)
| equalish(u0r1(X970),u2r1(X970))
| c(X970)
| r(X970,u1r1(X970))
| equalish(X969,u3r1(X970))
| ~ s1most(X970)
| ~ s(X970,X969) ),
inference(resolution,[status(thm)],[c3127,clause_16]) ).
cnf(c6307,plain,
( d(X3275)
| equalish(u0r1(X3275),u2r1(X3275))
| c(X3275)
| r(X3275,u1r1(X3275))
| equalish(u0r1(X3275),u3r1(X3275))
| ~ s1most(X3275)
| r(X3275,u0r1(X3275)) ),
inference(resolution,[status(thm)],[c3135,c16]) ).
cnf(c49,plain,
( d(X101)
| s(X101,u3r2(X101))
| equalish(X102,u2r1(X101))
| ~ r1most(X101)
| ~ r(X101,X102) ),
inference(resolution,[status(thm)],[c11,clause_8]) ).
cnf(c32,plain,
( d(X72)
| s(X72,u3r2(X72))
| equalish(X71,u2r1(X72))
| ~ s1most(X72)
| ~ s(X72,X71) ),
inference(resolution,[status(thm)],[c8,clause_16]) ).
cnf(c110,plain,
( d(X235)
| s(X235,u3r2(X235))
| equalish(u0r1(X235),u2r1(X235))
| ~ s1most(X235)
| c(X235)
| r(X235,u0r1(X235))
| r(X235,u1r2(X235)) ),
inference(resolution,[status(thm)],[c32,c15]) ).
cnf(c798,plain,
( d(X537)
| s(X537,u3r2(X537))
| equalish(u0r1(X537),u2r1(X537))
| c(X537)
| r(X537,u0r1(X537))
| r(X537,u1r2(X537)) ),
inference(resolution,[status(thm)],[c110,clause_19]) ).
cnf(c2866,plain,
( d(X538)
| s(X538,u3r2(X538))
| equalish(u0r1(X538),u2r1(X538))
| c(X538)
| r(X538,u1r2(X538))
| ~ r1most(X538) ),
inference(resolution,[status(thm)],[c798,c49]) ).
cnf(c2896,plain,
( d(X539)
| s(X539,u3r2(X539))
| equalish(u0r1(X539),u2r1(X539))
| c(X539)
| r(X539,u1r2(X539)) ),
inference(resolution,[status(thm)],[c2866,clause_11]) ).
cnf(c2905,plain,
( d(X959)
| equalish(u0r1(X959),u2r1(X959))
| c(X959)
| r(X959,u1r2(X959))
| equalish(X958,u3r2(X959))
| ~ s1most(X959)
| ~ s(X959,X958) ),
inference(resolution,[status(thm)],[c2896,clause_16]) ).
cnf(c6092,plain,
( d(X3256)
| equalish(u0r1(X3256),u2r1(X3256))
| c(X3256)
| r(X3256,u1r2(X3256))
| equalish(u0r1(X3256),u3r2(X3256))
| ~ s1most(X3256)
| r(X3256,u0r1(X3256)) ),
inference(resolution,[status(thm)],[c2905,c15]) ).
cnf(c106,plain,
( d(X229)
| s(X229,u3r2(X229))
| equalish(u0r1(X229),u2r1(X229))
| ~ s1most(X229)
| c(X229)
| r(X229,u0r1(X229))
| r(X229,u1r1(X229)) ),
inference(resolution,[status(thm)],[c32,c16]) ).
cnf(c787,plain,
( d(X522)
| s(X522,u3r2(X522))
| equalish(u0r1(X522),u2r1(X522))
| c(X522)
| r(X522,u0r1(X522))
| r(X522,u1r1(X522)) ),
inference(resolution,[status(thm)],[c106,clause_19]) ).
cnf(c2640,plain,
( d(X525)
| s(X525,u3r2(X525))
| equalish(u0r1(X525),u2r1(X525))
| c(X525)
| r(X525,u1r1(X525))
| ~ r1most(X525) ),
inference(resolution,[status(thm)],[c787,c49]) ).
cnf(c2757,plain,
( d(X526)
| s(X526,u3r2(X526))
| equalish(u0r1(X526),u2r1(X526))
| c(X526)
| r(X526,u1r1(X526)) ),
inference(resolution,[status(thm)],[c2640,clause_10]) ).
cnf(c2765,plain,
( d(X949)
| equalish(u0r1(X949),u2r1(X949))
| c(X949)
| r(X949,u1r1(X949))
| equalish(X948,u3r2(X949))
| ~ s1most(X949)
| ~ s(X949,X948) ),
inference(resolution,[status(thm)],[c2757,clause_16]) ).
cnf(c5932,plain,
( d(X3244)
| equalish(u0r1(X3244),u2r1(X3244))
| c(X3244)
| r(X3244,u1r1(X3244))
| equalish(u0r1(X3244),u3r2(X3244))
| ~ s1most(X3244)
| r(X3244,u0r1(X3244)) ),
inference(resolution,[status(thm)],[c2765,c16]) ).
cnf(c5208,plain,
( c(X3163)
| r(X3163,u0r1(X3163))
| r(X3163,u1r2(X3163))
| equalish(u2r1(X3163),u0r1(X3163))
| d(X3163)
| equalish(u3r1(X3163),u0r1(X3163))
| ~ s1most(X3163) ),
inference(resolution,[status(thm)],[c3590,c68]) ).
cnf(c5134,plain,
( c(X3155)
| r(X3155,u0r1(X3155))
| r(X3155,u1r2(X3155))
| equalish(u2r1(X3155),u0r1(X3155))
| d(X3155)
| equalish(u3r2(X3155),u0r1(X3155))
| ~ s1most(X3155) ),
inference(resolution,[status(thm)],[c3523,c68]) ).
cnf(c3209,plain,
( d(X3027)
| equalish(u0r1(X3027),u2r1(X3027))
| c(X3027)
| r(X3027,u0r1(X3027))
| r(X3027,u1r2(X3027))
| equalish(u3r1(X3027),u0r1(X3027))
| ~ s1most(X3027) ),
inference(resolution,[status(thm)],[c1008,c68]) ).
cnf(c3063,plain,
( d(X3011)
| equalish(u0r1(X3011),u2r1(X3011))
| c(X3011)
| r(X3011,u0r1(X3011))
| r(X3011,u1r1(X3011))
| equalish(u3r1(X3011),u0r1(X3011))
| ~ s1most(X3011) ),
inference(resolution,[status(thm)],[c1001,c82]) ).
cnf(c2838,plain,
( d(X2997)
| equalish(u0r1(X2997),u2r1(X2997))
| c(X2997)
| r(X2997,u0r1(X2997))
| r(X2997,u1r2(X2997))
| equalish(u3r2(X2997),u0r1(X2997))
| ~ s1most(X2997) ),
inference(resolution,[status(thm)],[c798,c68]) ).
cnf(c2609,plain,
( d(X2983)
| equalish(u0r1(X2983),u2r1(X2983))
| c(X2983)
| r(X2983,u0r1(X2983))
| r(X2983,u1r1(X2983))
| equalish(u3r2(X2983),u0r1(X2983))
| ~ s1most(X2983) ),
inference(resolution,[status(thm)],[c787,c82]) ).
cnf(c8854,plain,
( s(X2864,u0r1(X2864))
| d(X2864)
| equalish(u2r1(X2864),u2r1(X2864))
| equalish(u0r1(X2864),u0r1(X2864))
| equalish(u1r1(X2864),u1r1(X2864))
| ~ r1most(X2864) ),
inference(resolution,[status(thm)],[c8825,c19]) ).
cnf(c8791,plain,
( s(X2857,u0r1(X2857))
| r(X2857,u0r1(X2857))
| d(X2857)
| equalish(u2r1(X2857),u2r1(X2857))
| equalish(X2858,u1r1(X2857))
| ~ r1most(X2857)
| ~ r(X2857,X2858) ),
inference(resolution,[status(thm)],[c8732,clause_8]) ).
cnf(c12558,plain,
( s(X2859,u0r1(X2859))
| r(X2859,u0r1(X2859))
| d(X2859)
| equalish(u2r1(X2859),u2r1(X2859))
| equalish(u1r2(X2859),u1r1(X2859))
| ~ r1most(X2859) ),
inference(resolution,[status(thm)],[c8791,c5227]) ).
cnf(c8768,plain,
( s(X2854,u0r1(X2854))
| r(X2854,u1r1(X2854))
| d(X2854)
| equalish(u2r1(X2854),u2r1(X2854))
| equalish(X2855,u0r1(X2854))
| ~ r1most(X2854)
| ~ r(X2854,X2855) ),
inference(resolution,[status(thm)],[c8732,clause_8]) ).
cnf(c30,plain,
( d(X65)
| s(X65,u3r2(X65))
| equalish(u2r1(X65),u2r1(X65))
| ~ s1most(X65) ),
inference(resolution,[status(thm)],[c8,c24]) ).
cnf(c94,plain,
( d(X66)
| s(X66,u3r2(X66))
| equalish(u2r1(X66),u2r1(X66)) ),
inference(resolution,[status(thm)],[c30,clause_19]) ).
cnf(c8748,plain,
( r(X2848,u0r1(X2848))
| r(X2848,u1r1(X2848))
| d(X2848)
| equalish(u2r1(X2848),u2r1(X2848))
| equalish(X2847,u0r1(X2848))
| ~ s1most(X2848)
| ~ s(X2848,X2847) ),
inference(resolution,[status(thm)],[c8732,clause_16]) ).
cnf(c12446,plain,
( r(X2850,u0r1(X2850))
| r(X2850,u1r1(X2850))
| d(X2850)
| equalish(u2r1(X2850),u2r1(X2850))
| equalish(u3r2(X2850),u0r1(X2850))
| ~ s1most(X2850) ),
inference(resolution,[status(thm)],[c8748,c94]) ).
cnf(c39,plain,
( d(X82)
| s(X82,u3r1(X82))
| equalish(u2r1(X82),u2r1(X82))
| ~ s1most(X82) ),
inference(resolution,[status(thm)],[c9,c24]) ).
cnf(c123,plain,
( d(X83)
| s(X83,u3r1(X83))
| equalish(u2r1(X83),u2r1(X83)) ),
inference(resolution,[status(thm)],[c39,clause_18]) ).
cnf(c12444,plain,
( r(X2849,u0r1(X2849))
| r(X2849,u1r1(X2849))
| d(X2849)
| equalish(u2r1(X2849),u2r1(X2849))
| equalish(u3r1(X2849),u0r1(X2849))
| ~ s1most(X2849) ),
inference(resolution,[status(thm)],[c8748,c123]) ).
cnf(c7974,plain,
( s(X1076,u0r1(X1076))
| r(X1076,u1r1(X1076))
| s1most(X1076)
| ~ c(X1076) ),
inference(resolution,[status(thm)],[c7949,clause_3]) ).
cnf(c8060,plain,
( s(X1080,u0r1(X1080))
| r(X1080,u1r1(X1080))
| s1most(X1080)
| equalish(u0r1(X1080),u0r1(X1080)) ),
inference(resolution,[status(thm)],[c7974,c473]) ).
cnf(c8128,plain,
( s(X1149,u0r1(X1149))
| r(X1149,u1r1(X1149))
| equalish(u0r1(X1149),u0r1(X1149))
| d(X1149)
| r(X1149,u2r1(X1149)) ),
inference(resolution,[status(thm)],[c8060,clause_15]) ).
cnf(c8627,plain,
( s(X2844,u0r1(X2844))
| r(X2844,u1r1(X2844))
| equalish(u0r1(X2844),u0r1(X2844))
| d(X2844)
| equalish(X2845,u2r1(X2844))
| ~ r1most(X2844)
| ~ r(X2844,X2845) ),
inference(resolution,[status(thm)],[c8128,clause_8]) ).
cnf(c3753,plain,
( s(X659,u0r1(X659))
| r(X659,u1r2(X659))
| s1most(X659)
| ~ c(X659) ),
inference(resolution,[status(thm)],[c3733,clause_3]) ).
cnf(c3818,plain,
( s(X663,u0r1(X663))
| r(X663,u1r2(X663))
| s1most(X663)
| equalish(u0r1(X663),u0r1(X663)) ),
inference(resolution,[status(thm)],[c3753,c257]) ).
cnf(c3861,plain,
( s(X732,u0r1(X732))
| r(X732,u1r2(X732))
| equalish(u0r1(X732),u0r1(X732))
| d(X732)
| r(X732,u2r1(X732)) ),
inference(resolution,[status(thm)],[c3818,clause_15]) ).
cnf(c8604,plain,
( s(X2839,u0r1(X2839))
| equalish(u0r1(X2839),u0r1(X2839))
| d(X2839)
| r(X2839,u2r1(X2839))
| equalish(X2840,u1r1(X2839))
| ~ r1most(X2839)
| ~ r(X2839,X2840) ),
inference(resolution,[status(thm)],[c8128,clause_8]) ).
cnf(c12355,plain,
( s(X2843,u0r1(X2843))
| equalish(u0r1(X2843),u0r1(X2843))
| d(X2843)
| r(X2843,u2r1(X2843))
| equalish(u1r2(X2843),u1r1(X2843))
| ~ r1most(X2843) ),
inference(resolution,[status(thm)],[c8604,c3861]) ).
cnf(c8127,plain,
( s(X1147,u0r1(X1147))
| r(X1147,u1r1(X1147))
| equalish(u0r1(X1147),u0r1(X1147))
| d(X1147)
| s(X1147,u2r1(X1147)) ),
inference(resolution,[status(thm)],[c8060,clause_14]) ).
cnf(c8572,plain,
( s(X2835,u0r1(X2835))
| r(X2835,u1r1(X2835))
| equalish(u0r1(X2835),u0r1(X2835))
| d(X2835)
| equalish(X2834,u2r1(X2835))
| ~ s1most(X2835)
| ~ s(X2835,X2834) ),
inference(resolution,[status(thm)],[c8127,clause_16]) ).
cnf(c3859,plain,
( s(X730,u0r1(X730))
| r(X730,u1r2(X730))
| equalish(u0r1(X730),u0r1(X730))
| d(X730)
| s(X730,u2r1(X730)) ),
inference(resolution,[status(thm)],[c3818,clause_14]) ).
cnf(c8552,plain,
( s(X2829,u0r1(X2829))
| equalish(u0r1(X2829),u0r1(X2829))
| d(X2829)
| s(X2829,u2r1(X2829))
| equalish(X2830,u1r1(X2829))
| ~ r1most(X2829)
| ~ r(X2829,X2830) ),
inference(resolution,[status(thm)],[c8127,clause_8]) ).
cnf(c12253,plain,
( s(X2831,u0r1(X2831))
| equalish(u0r1(X2831),u0r1(X2831))
| d(X2831)
| s(X2831,u2r1(X2831))
| equalish(u1r2(X2831),u1r1(X2831))
| ~ r1most(X2831) ),
inference(resolution,[status(thm)],[c8552,c3859]) ).
cnf(c5319,plain,
( s(X2767,u0r1(X2767))
| d(X2767)
| equalish(u2r1(X2767),u2r1(X2767))
| equalish(u0r1(X2767),u0r1(X2767))
| equalish(u1r2(X2767),u1r2(X2767))
| ~ r1most(X2767) ),
inference(resolution,[status(thm)],[c5299,c19]) ).
cnf(c5268,plain,
( s(X2760,u0r1(X2760))
| r(X2760,u0r1(X2760))
| d(X2760)
| equalish(u2r1(X2760),u2r1(X2760))
| equalish(X2761,u1r2(X2760))
| ~ r1most(X2760)
| ~ r(X2760,X2761) ),
inference(resolution,[status(thm)],[c5227,clause_8]) ).
cnf(c12192,plain,
( s(X2763,u0r1(X2763))
| r(X2763,u0r1(X2763))
| d(X2763)
| equalish(u2r1(X2763),u2r1(X2763))
| equalish(u1r1(X2763),u1r2(X2763))
| ~ r1most(X2763) ),
inference(resolution,[status(thm)],[c5268,c8732]) ).
cnf(c5252,plain,
( s(X2756,u0r1(X2756))
| r(X2756,u1r2(X2756))
| d(X2756)
| equalish(u2r1(X2756),u2r1(X2756))
| equalish(X2757,u0r1(X2756))
| ~ r1most(X2756)
| ~ r(X2756,X2757) ),
inference(resolution,[status(thm)],[c5227,clause_8]) ).
cnf(c5236,plain,
( r(X2750,u0r1(X2750))
| r(X2750,u1r2(X2750))
| d(X2750)
| equalish(u2r1(X2750),u2r1(X2750))
| equalish(X2749,u0r1(X2750))
| ~ s1most(X2750)
| ~ s(X2750,X2749) ),
inference(resolution,[status(thm)],[c5227,clause_16]) ).
cnf(c12078,plain,
( r(X2754,u0r1(X2754))
| r(X2754,u1r2(X2754))
| d(X2754)
| equalish(u2r1(X2754),u2r1(X2754))
| equalish(u3r2(X2754),u0r1(X2754))
| ~ s1most(X2754) ),
inference(resolution,[status(thm)],[c5236,c94]) ).
cnf(c12076,plain,
( r(X2753,u0r1(X2753))
| r(X2753,u1r2(X2753))
| d(X2753)
| equalish(u2r1(X2753),u2r1(X2753))
| equalish(u3r1(X2753),u0r1(X2753))
| ~ s1most(X2753) ),
inference(resolution,[status(thm)],[c5236,c123]) ).
cnf(c4758,plain,
( s(X2726,u0r1(X2726))
| r(X2726,u1r2(X2726))
| equalish(u0r1(X2726),u0r1(X2726))
| d(X2726)
| equalish(X2727,u2r1(X2726))
| ~ r1most(X2726)
| ~ r(X2726,X2727) ),
inference(resolution,[status(thm)],[c3861,clause_8]) ).
cnf(c4742,plain,
( s(X2722,u0r1(X2722))
| equalish(u0r1(X2722),u0r1(X2722))
| d(X2722)
| r(X2722,u2r1(X2722))
| equalish(X2723,u1r2(X2722))
| ~ r1most(X2722)
| ~ r(X2722,X2723) ),
inference(resolution,[status(thm)],[c3861,clause_8]) ).
cnf(c11966,plain,
( s(X2724,u0r1(X2724))
| equalish(u0r1(X2724),u0r1(X2724))
| d(X2724)
| r(X2724,u2r1(X2724))
| equalish(u1r1(X2724),u1r2(X2724))
| ~ r1most(X2724) ),
inference(resolution,[status(thm)],[c4742,c8128]) ).
cnf(c4718,plain,
( s(X2717,u0r1(X2717))
| r(X2717,u1r2(X2717))
| equalish(u0r1(X2717),u0r1(X2717))
| d(X2717)
| equalish(X2716,u2r1(X2717))
| ~ s1most(X2717)
| ~ s(X2717,X2716) ),
inference(resolution,[status(thm)],[c3859,clause_16]) ).
cnf(c4705,plain,
( s(X2712,u0r1(X2712))
| equalish(u0r1(X2712),u0r1(X2712))
| d(X2712)
| s(X2712,u2r1(X2712))
| equalish(X2713,u1r2(X2712))
| ~ r1most(X2712)
| ~ r(X2712,X2713) ),
inference(resolution,[status(thm)],[c3859,clause_8]) ).
cnf(c11908,plain,
( s(X2715,u0r1(X2715))
| equalish(u0r1(X2715),u0r1(X2715))
| d(X2715)
| s(X2715,u2r1(X2715))
| equalish(u1r1(X2715),u1r2(X2715))
| ~ r1most(X2715) ),
inference(resolution,[status(thm)],[c4705,c8127]) ).
cnf(c11842,plain,
( c(X2485)
| r(X2485,u1r1(X2485))
| equalish(u2r1(X2485),u0r1(X2485))
| d(X2485)
| equalish(u3r1(X2485),u3r2(X2485))
| ~ s1most(X2485) ),
inference(resolution,[status(thm)],[c11724,c11299]) ).
cnf(c11691,plain,
( c(X2477)
| equalish(u2r1(X2477),u0r1(X2477))
| d(X2477)
| s(X2477,u3r2(X2477))
| equalish(X2478,u1r1(X2477))
| ~ r1most(X2477)
| ~ r(X2477,X2478) ),
inference(resolution,[status(thm)],[c11633,clause_8]) ).
cnf(c11785,plain,
( c(X2482)
| equalish(u2r1(X2482),u0r1(X2482))
| d(X2482)
| s(X2482,u3r2(X2482))
| equalish(u1r2(X2482),u1r1(X2482))
| ~ r1most(X2482) ),
inference(resolution,[status(thm)],[c11691,c10162]) ).
cnf(c11781,plain,
( c(X2481)
| equalish(u2r1(X2481),u0r1(X2481))
| d(X2481)
| s(X2481,u3r2(X2481))
| equalish(u2r1(X2481),u1r1(X2481))
| ~ r1most(X2481) ),
inference(resolution,[status(thm)],[c11691,c11]) ).
cnf(c11715,plain,
( c(X2470)
| r(X2470,u1r1(X2470))
| equalish(u2r1(X2470),u0r1(X2470))
| d(X2470)
| equalish(u3r2(X2470),u3r1(X2470))
| ~ s1most(X2470) ),
inference(resolution,[status(thm)],[c11633,c11388]) ).
cnf(c11713,plain,
( c(X2469)
| r(X2469,u1r1(X2469))
| equalish(u2r1(X2469),u0r1(X2469))
| d(X2469)
| equalish(u3r2(X2469),u3r2(X2469))
| ~ s1most(X2469) ),
inference(resolution,[status(thm)],[c11633,c24]) ).
cnf(c10221,plain,
( c(X2044)
| equalish(u2r1(X2044),u0r1(X2044))
| d(X2044)
| s(X2044,u3r2(X2044))
| equalish(X2045,u1r2(X2044))
| ~ r1most(X2044)
| ~ r(X2044,X2045) ),
inference(resolution,[status(thm)],[c10162,clause_8]) ).
cnf(c11708,plain,
( c(X2468)
| equalish(u2r1(X2468),u0r1(X2468))
| d(X2468)
| s(X2468,u3r2(X2468))
| equalish(u1r1(X2468),u1r2(X2468))
| ~ r1most(X2468) ),
inference(resolution,[status(thm)],[c11633,c10221]) ).
cnf(c11687,plain,
( c(X2466)
| equalish(u2r1(X2466),u0r1(X2466))
| d(X2466)
| s(X2466,u3r2(X2466))
| equalish(u1r1(X2466),u2r1(X2466))
| ~ r1most(X2466) ),
inference(resolution,[status(thm)],[c11633,c49]) ).
cnf(c11678,plain,
( c(X2465)
| equalish(u2r1(X2465),u0r1(X2465))
| d(X2465)
| s(X2465,u3r2(X2465))
| equalish(u1r1(X2465),u1r1(X2465))
| ~ r1most(X2465) ),
inference(resolution,[status(thm)],[c11633,c19]) ).
cnf(c11357,plain,
( c(X2415)
| equalish(u2r1(X2415),u0r1(X2415))
| d(X2415)
| s(X2415,u3r1(X2415))
| equalish(X2416,u1r1(X2415))
| ~ r1most(X2415)
| ~ r(X2415,X2416) ),
inference(resolution,[status(thm)],[c11299,clause_8]) ).
cnf(c11419,plain,
( c(X2419)
| equalish(u2r1(X2419),u0r1(X2419))
| d(X2419)
| s(X2419,u3r1(X2419))
| equalish(u2r1(X2419),u1r1(X2419))
| ~ r1most(X2419) ),
inference(resolution,[status(thm)],[c11357,c12]) ).
cnf(c11418,plain,
( c(X2417)
| equalish(u2r1(X2417),u0r1(X2417))
| d(X2417)
| s(X2417,u3r1(X2417))
| equalish(u1r2(X2417),u1r1(X2417))
| ~ r1most(X2417) ),
inference(resolution,[status(thm)],[c11357,c10765]) ).
cnf(c11378,plain,
( c(X2408)
| r(X2408,u1r1(X2408))
| equalish(u2r1(X2408),u0r1(X2408))
| d(X2408)
| equalish(u3r1(X2408),u3r1(X2408))
| ~ s1most(X2408) ),
inference(resolution,[status(thm)],[c11299,c24]) ).
cnf(c10824,plain,
( c(X2105)
| equalish(u2r1(X2105),u0r1(X2105))
| d(X2105)
| s(X2105,u3r1(X2105))
| equalish(X2106,u1r2(X2105))
| ~ r1most(X2105)
| ~ r(X2105,X2106) ),
inference(resolution,[status(thm)],[c10765,clause_8]) ).
cnf(c11362,plain,
( c(X2407)
| equalish(u2r1(X2407),u0r1(X2407))
| d(X2407)
| s(X2407,u3r1(X2407))
| equalish(u1r1(X2407),u1r2(X2407))
| ~ r1most(X2407) ),
inference(resolution,[status(thm)],[c11299,c10824]) ).
cnf(c11354,plain,
( c(X2406)
| equalish(u2r1(X2406),u0r1(X2406))
| d(X2406)
| s(X2406,u3r1(X2406))
| equalish(u1r1(X2406),u2r1(X2406))
| ~ r1most(X2406) ),
inference(resolution,[status(thm)],[c11299,c57]) ).
cnf(c11344,plain,
( c(X2404)
| equalish(u2r1(X2404),u0r1(X2404))
| d(X2404)
| s(X2404,u3r1(X2404))
| equalish(u1r1(X2404),u1r1(X2404))
| ~ r1most(X2404) ),
inference(resolution,[status(thm)],[c11299,c19]) ).
cnf(c10942,plain,
( c(X2112)
| r(X2112,u1r2(X2112))
| equalish(u2r1(X2112),u0r1(X2112))
| d(X2112)
| equalish(u3r2(X2112),u3r1(X2112))
| ~ s1most(X2112) ),
inference(resolution,[status(thm)],[c10853,c10162]) ).
cnf(c10888,plain,
( c(X2108)
| equalish(u2r1(X2108),u0r1(X2108))
| d(X2108)
| s(X2108,u3r1(X2108))
| equalish(u2r1(X2108),u1r2(X2108))
| ~ r1most(X2108) ),
inference(resolution,[status(thm)],[c10824,c12]) ).
cnf(c10857,plain,
( c(X2098)
| r(X2098,u1r2(X2098))
| equalish(u2r1(X2098),u0r1(X2098))
| d(X2098)
| equalish(u3r1(X2098),u3r2(X2098))
| ~ s1most(X2098) ),
inference(resolution,[status(thm)],[c10765,c10249]) ).
cnf(c10844,plain,
( c(X2096)
| r(X2096,u1r2(X2096))
| equalish(u2r1(X2096),u0r1(X2096))
| d(X2096)
| equalish(u3r1(X2096),u3r1(X2096))
| ~ s1most(X2096) ),
inference(resolution,[status(thm)],[c10765,c24]) ).
cnf(c10821,plain,
( c(X2095)
| equalish(u2r1(X2095),u0r1(X2095))
| d(X2095)
| s(X2095,u3r1(X2095))
| equalish(u1r2(X2095),u2r1(X2095))
| ~ r1most(X2095) ),
inference(resolution,[status(thm)],[c10765,c57]) ).
cnf(c10811,plain,
( c(X2094)
| equalish(u2r1(X2094),u0r1(X2094))
| d(X2094)
| s(X2094,u3r1(X2094))
| equalish(u1r2(X2094),u1r2(X2094))
| ~ r1most(X2094) ),
inference(resolution,[status(thm)],[c10765,c19]) ).
cnf(c10294,plain,
( c(X2046)
| equalish(u2r1(X2046),u0r1(X2046))
| d(X2046)
| s(X2046,u3r2(X2046))
| equalish(u2r1(X2046),u1r2(X2046))
| ~ r1most(X2046) ),
inference(resolution,[status(thm)],[c10221,c11]) ).
cnf(c10240,plain,
( c(X2037)
| r(X2037,u1r2(X2037))
| equalish(u2r1(X2037),u0r1(X2037))
| d(X2037)
| equalish(u3r2(X2037),u3r2(X2037))
| ~ s1most(X2037) ),
inference(resolution,[status(thm)],[c10162,c24]) ).
cnf(c10217,plain,
( c(X2034)
| equalish(u2r1(X2034),u0r1(X2034))
| d(X2034)
| s(X2034,u3r2(X2034))
| equalish(u1r2(X2034),u2r1(X2034))
| ~ r1most(X2034) ),
inference(resolution,[status(thm)],[c10162,c49]) ).
cnf(c10208,plain,
( c(X2033)
| equalish(u2r1(X2033),u0r1(X2033))
| d(X2033)
| s(X2033,u3r2(X2033))
| equalish(u1r2(X2033),u1r2(X2033))
| ~ r1most(X2033) ),
inference(resolution,[status(thm)],[c10162,c19]) ).
cnf(c8859,plain,
( s(X1659,u0r1(X1659))
| d(X1659)
| equalish(u2r1(X1659),u2r1(X1659))
| equalish(u0r1(X1659),u0r1(X1659))
| s(X1659,u1r1(X1659))
| ~ c(X1659) ),
inference(resolution,[status(thm)],[c8825,clause_3]) ).
cnf(c8781,plain,
( s(X1655,u0r1(X1655))
| r(X1655,u0r1(X1655))
| d(X1655)
| equalish(u2r1(X1655),u2r1(X1655))
| equalish(u1r1(X1655),u1r1(X1655))
| ~ r1most(X1655) ),
inference(resolution,[status(thm)],[c8732,c19]) ).
cnf(c128,plain,
( d(X153)
| equalish(u2r1(X153),u2r1(X153))
| equalish(X152,u3r1(X153))
| ~ s1most(X153)
| ~ s(X153,X152) ),
inference(resolution,[status(thm)],[c123,clause_16]) ).
cnf(c8743,plain,
( r(X1653,u0r1(X1653))
| r(X1653,u1r1(X1653))
| d(X1653)
| equalish(u2r1(X1653),u2r1(X1653))
| equalish(u0r1(X1653),u3r1(X1653))
| ~ s1most(X1653) ),
inference(resolution,[status(thm)],[c8732,c128]) ).
cnf(c100,plain,
( d(X138)
| equalish(u2r1(X138),u2r1(X138))
| equalish(X137,u3r2(X138))
| ~ s1most(X138)
| ~ s(X138,X137) ),
inference(resolution,[status(thm)],[c94,clause_16]) ).
cnf(c8739,plain,
( r(X1650,u0r1(X1650))
| r(X1650,u1r1(X1650))
| d(X1650)
| equalish(u2r1(X1650),u2r1(X1650))
| equalish(u0r1(X1650),u3r2(X1650))
| ~ s1most(X1650) ),
inference(resolution,[status(thm)],[c8732,c100]) ).
cnf(c8594,plain,
( s(X1643,u0r1(X1643))
| equalish(u0r1(X1643),u0r1(X1643))
| d(X1643)
| r(X1643,u2r1(X1643))
| equalish(u1r1(X1643),u1r1(X1643))
| ~ r1most(X1643) ),
inference(resolution,[status(thm)],[c8128,c19]) ).
cnf(c8542,plain,
( s(X1641,u0r1(X1641))
| equalish(u0r1(X1641),u0r1(X1641))
| d(X1641)
| s(X1641,u2r1(X1641))
| equalish(u1r1(X1641),u1r1(X1641))
| ~ r1most(X1641) ),
inference(resolution,[status(thm)],[c8127,c19]) ).
cnf(c8032,plain,
( s(X1102,u0r1(X1102))
| r(X1102,u0r1(X1102))
| r(X1102,u1r1(X1102))
| d(X1102)
| r(X1102,u2r1(X1102)) ),
inference(resolution,[status(thm)],[c7949,clause_15]) ).
cnf(c8365,plain,
( s(X1633,u0r1(X1633))
| r(X1633,u0r1(X1633))
| r(X1633,u1r1(X1633))
| d(X1633)
| equalish(X1634,u2r1(X1633))
| ~ r1most(X1633)
| ~ r(X1633,X1634) ),
inference(resolution,[status(thm)],[c8032,clause_8]) ).
cnf(c3789,plain,
( s(X684,u0r1(X684))
| r(X684,u0r1(X684))
| r(X684,u1r2(X684))
| d(X684)
| r(X684,u2r1(X684)) ),
inference(resolution,[status(thm)],[c3733,clause_15]) ).
cnf(c8340,plain,
( s(X1628,u0r1(X1628))
| r(X1628,u0r1(X1628))
| d(X1628)
| r(X1628,u2r1(X1628))
| equalish(X1629,u1r1(X1628))
| ~ r1most(X1628)
| ~ r(X1628,X1629) ),
inference(resolution,[status(thm)],[c8032,clause_8]) ).
cnf(c10024,plain,
( s(X1630,u0r1(X1630))
| r(X1630,u0r1(X1630))
| d(X1630)
| r(X1630,u2r1(X1630))
| equalish(u1r2(X1630),u1r1(X1630))
| ~ r1most(X1630) ),
inference(resolution,[status(thm)],[c8340,c3789]) ).
cnf(c8316,plain,
( s(X1625,u0r1(X1625))
| r(X1625,u1r1(X1625))
| d(X1625)
| r(X1625,u2r1(X1625))
| equalish(X1626,u0r1(X1625))
| ~ r1most(X1625)
| ~ r(X1625,X1626) ),
inference(resolution,[status(thm)],[c8032,clause_8]) ).
cnf(c8249,plain,
( s(X1620,u0r1(X1620))
| r(X1620,u0r1(X1620))
| r(X1620,u1r1(X1620))
| d(X1620)
| equalish(X1619,u2r1(X1620))
| ~ s1most(X1620)
| ~ s(X1620,X1619) ),
inference(resolution,[status(thm)],[c8031,clause_16]) ).
cnf(c8226,plain,
( s(X1614,u0r1(X1614))
| r(X1614,u0r1(X1614))
| d(X1614)
| s(X1614,u2r1(X1614))
| equalish(X1615,u1r1(X1614))
| ~ r1most(X1614)
| ~ r(X1614,X1615) ),
inference(resolution,[status(thm)],[c8031,clause_8]) ).
cnf(c9862,plain,
( s(X1618,u0r1(X1618))
| r(X1618,u0r1(X1618))
| d(X1618)
| s(X1618,u2r1(X1618))
| equalish(u1r2(X1618),u1r1(X1618))
| ~ r1most(X1618) ),
inference(resolution,[status(thm)],[c8226,c3787]) ).
cnf(c8202,plain,
( s(X1611,u0r1(X1611))
| r(X1611,u1r1(X1611))
| d(X1611)
| s(X1611,u2r1(X1611))
| equalish(X1612,u0r1(X1611))
| ~ r1most(X1611)
| ~ r(X1611,X1612) ),
inference(resolution,[status(thm)],[c8031,clause_8]) ).
cnf(c5323,plain,
( s(X1516,u0r1(X1516))
| d(X1516)
| equalish(u2r1(X1516),u2r1(X1516))
| equalish(u0r1(X1516),u0r1(X1516))
| s(X1516,u1r2(X1516))
| ~ c(X1516) ),
inference(resolution,[status(thm)],[c5299,clause_3]) ).
cnf(c5261,plain,
( s(X1513,u0r1(X1513))
| r(X1513,u0r1(X1513))
| d(X1513)
| equalish(u2r1(X1513),u2r1(X1513))
| equalish(u1r2(X1513),u1r2(X1513))
| ~ r1most(X1513) ),
inference(resolution,[status(thm)],[c5227,c19]) ).
cnf(c5234,plain,
( r(X1510,u0r1(X1510))
| r(X1510,u1r2(X1510))
| d(X1510)
| equalish(u2r1(X1510),u2r1(X1510))
| equalish(u0r1(X1510),u3r1(X1510))
| ~ s1most(X1510) ),
inference(resolution,[status(thm)],[c5227,c128]) ).
cnf(c5230,plain,
( r(X1503,u0r1(X1503))
| r(X1503,u1r2(X1503))
| d(X1503)
| equalish(u2r1(X1503),u2r1(X1503))
| equalish(u0r1(X1503),u3r2(X1503))
| ~ s1most(X1503) ),
inference(resolution,[status(thm)],[c5227,c100]) ).
cnf(c4735,plain,
( s(X1482,u0r1(X1482))
| equalish(u0r1(X1482),u0r1(X1482))
| d(X1482)
| r(X1482,u2r1(X1482))
| equalish(u1r2(X1482),u1r2(X1482))
| ~ r1most(X1482) ),
inference(resolution,[status(thm)],[c3861,c19]) ).
cnf(c4698,plain,
( s(X1474,u0r1(X1474))
| equalish(u0r1(X1474),u0r1(X1474))
| d(X1474)
| s(X1474,u2r1(X1474))
| equalish(u1r2(X1474),u1r2(X1474))
| ~ r1most(X1474) ),
inference(resolution,[status(thm)],[c3859,c19]) ).
cnf(c4157,plain,
( s(X1455,u0r1(X1455))
| r(X1455,u0r1(X1455))
| r(X1455,u1r2(X1455))
| d(X1455)
| equalish(X1456,u2r1(X1455))
| ~ r1most(X1455)
| ~ r(X1455,X1456) ),
inference(resolution,[status(thm)],[c3789,clause_8]) ).
cnf(c4139,plain,
( s(X1450,u0r1(X1450))
| r(X1450,u0r1(X1450))
| d(X1450)
| r(X1450,u2r1(X1450))
| equalish(X1451,u1r2(X1450))
| ~ r1most(X1450)
| ~ r(X1450,X1451) ),
inference(resolution,[status(thm)],[c3789,clause_8]) ).
cnf(c9437,plain,
( s(X1454,u0r1(X1454))
| r(X1454,u0r1(X1454))
| d(X1454)
| r(X1454,u2r1(X1454))
| equalish(u1r1(X1454),u1r2(X1454))
| ~ r1most(X1454) ),
inference(resolution,[status(thm)],[c4139,c8032]) ).
cnf(c4122,plain,
( s(X1447,u0r1(X1447))
| r(X1447,u1r2(X1447))
| d(X1447)
| r(X1447,u2r1(X1447))
| equalish(X1448,u0r1(X1447))
| ~ r1most(X1447)
| ~ r(X1447,X1448) ),
inference(resolution,[status(thm)],[c3789,clause_8]) ).
cnf(c4012,plain,
( s(X1442,u0r1(X1442))
| r(X1442,u0r1(X1442))
| r(X1442,u1r2(X1442))
| d(X1442)
| equalish(X1441,u2r1(X1442))
| ~ s1most(X1442)
| ~ s(X1442,X1441) ),
inference(resolution,[status(thm)],[c3787,clause_16]) ).
cnf(c3997,plain,
( s(X1437,u0r1(X1437))
| r(X1437,u0r1(X1437))
| d(X1437)
| s(X1437,u2r1(X1437))
| equalish(X1438,u1r2(X1437))
| ~ r1most(X1437)
| ~ r(X1437,X1438) ),
inference(resolution,[status(thm)],[c3787,clause_8]) ).
cnf(c9243,plain,
( s(X1439,u0r1(X1439))
| r(X1439,u0r1(X1439))
| d(X1439)
| s(X1439,u2r1(X1439))
| equalish(u1r1(X1439),u1r2(X1439))
| ~ r1most(X1439) ),
inference(resolution,[status(thm)],[c3997,c8031]) ).
cnf(c3980,plain,
( s(X1433,u0r1(X1433))
| r(X1433,u1r2(X1433))
| d(X1433)
| s(X1433,u2r1(X1433))
| equalish(X1434,u0r1(X1433))
| ~ r1most(X1433)
| ~ r(X1433,X1434) ),
inference(resolution,[status(thm)],[c3787,clause_8]) ).
cnf(c8786,plain,
( s(X1266,u0r1(X1266))
| r(X1266,u0r1(X1266))
| d(X1266)
| equalish(u2r1(X1266),u2r1(X1266))
| s(X1266,u1r1(X1266))
| ~ c(X1266) ),
inference(resolution,[status(thm)],[c8732,clause_3]) ).
cnf(c8599,plain,
( s(X1262,u0r1(X1262))
| equalish(u0r1(X1262),u0r1(X1262))
| d(X1262)
| r(X1262,u2r1(X1262))
| s(X1262,u1r1(X1262))
| ~ c(X1262) ),
inference(resolution,[status(thm)],[c8128,clause_3]) ).
cnf(c8547,plain,
( s(X1256,u0r1(X1256))
| equalish(u0r1(X1256),u0r1(X1256))
| d(X1256)
| s(X1256,u2r1(X1256))
| s(X1256,u1r1(X1256))
| ~ c(X1256) ),
inference(resolution,[status(thm)],[c8127,clause_3]) ).
cnf(c8331,plain,
( s(X1245,u0r1(X1245))
| r(X1245,u0r1(X1245))
| d(X1245)
| r(X1245,u2r1(X1245))
| equalish(u1r1(X1245),u1r1(X1245))
| ~ r1most(X1245) ),
inference(resolution,[status(thm)],[c8032,c19]) ).
cnf(c8838,plain,
( r(X1236,u1r1(X1236))
| d(X1236)
| equalish(u2r1(X1236),u2r1(X1236))
| equalish(u0r1(X1236),u0r1(X1236))
| ~ s1most(X1236) ),
inference(resolution,[status(thm)],[c8825,c24]) ).
cnf(c8751,plain,
( r(X1229,u0r1(X1229))
| r(X1229,u1r1(X1229))
| d(X1229)
| equalish(u2r1(X1229),u2r1(X1229))
| ~ c(X1229) ),
inference(resolution,[status(thm)],[c8732,clause_4]) ).
cnf(c8217,plain,
( s(X1225,u0r1(X1225))
| r(X1225,u0r1(X1225))
| d(X1225)
| s(X1225,u2r1(X1225))
| equalish(u1r1(X1225),u1r1(X1225))
| ~ r1most(X1225) ),
inference(resolution,[status(thm)],[c8031,c19]) ).
cnf(c8336,plain,
( s(X1188,u0r1(X1188))
| r(X1188,u0r1(X1188))
| d(X1188)
| r(X1188,u2r1(X1188))
| s(X1188,u1r1(X1188))
| ~ c(X1188) ),
inference(resolution,[status(thm)],[c8032,clause_3]) ).
cnf(c8222,plain,
( s(X1183,u0r1(X1183))
| r(X1183,u0r1(X1183))
| d(X1183)
| s(X1183,u2r1(X1183))
| s(X1183,u1r1(X1183))
| ~ c(X1183) ),
inference(resolution,[status(thm)],[c8031,clause_3]) ).
cnf(c8098,plain,
( s(X1177,u0r1(X1177))
| s1most(X1177)
| equalish(u0r1(X1177),u0r1(X1177))
| equalish(X1178,u1r1(X1177))
| ~ r1most(X1177)
| ~ r(X1177,X1178) ),
inference(resolution,[status(thm)],[c8060,clause_8]) ).
cnf(c8656,plain,
( s(X1179,u0r1(X1179))
| s1most(X1179)
| equalish(u0r1(X1179),u0r1(X1179))
| equalish(u1r2(X1179),u1r1(X1179))
| ~ r1most(X1179) ),
inference(resolution,[status(thm)],[c8098,c3818]) ).
cnf(c3845,plain,
( s(X765,u0r1(X765))
| s1most(X765)
| equalish(u0r1(X765),u0r1(X765))
| equalish(X766,u1r2(X765))
| ~ r1most(X765)
| ~ r(X765,X766) ),
inference(resolution,[status(thm)],[c3818,clause_8]) ).
cnf(c8109,plain,
( s(X1129,u0r1(X1129))
| s1most(X1129)
| equalish(u0r1(X1129),u0r1(X1129))
| equalish(u1r1(X1129),u1r2(X1129))
| ~ r1most(X1129) ),
inference(resolution,[status(thm)],[c8060,c3845]) ).
cnf(c8089,plain,
( s(X1128,u0r1(X1128))
| s1most(X1128)
| equalish(u0r1(X1128),u0r1(X1128))
| equalish(u1r1(X1128),u1r1(X1128))
| ~ r1most(X1128) ),
inference(resolution,[status(thm)],[c8060,c19]) ).
cnf(c8002,plain,
( s(X1123,u0r1(X1123))
| r(X1123,u0r1(X1123))
| s1most(X1123)
| equalish(X1124,u1r1(X1123))
| ~ r1most(X1123)
| ~ r(X1123,X1124) ),
inference(resolution,[status(thm)],[c7949,clause_8]) ).
cnf(c8476,plain,
( s(X1125,u0r1(X1125))
| r(X1125,u0r1(X1125))
| s1most(X1125)
| equalish(u1r2(X1125),u1r1(X1125))
| ~ r1most(X1125) ),
inference(resolution,[status(thm)],[c8002,c3733]) ).
cnf(c7978,plain,
( s(X1120,u0r1(X1120))
| r(X1120,u1r1(X1120))
| s1most(X1120)
| equalish(X1121,u0r1(X1120))
| ~ r1most(X1120)
| ~ r(X1120,X1121) ),
inference(resolution,[status(thm)],[c7949,clause_8]) ).
cnf(c8312,plain,
( s(X1104,u0r1(X1104))
| r(X1104,u1r1(X1104))
| d(X1104)
| r(X1104,u2r1(X1104))
| ~ c(X1104) ),
inference(resolution,[status(thm)],[c8032,clause_3]) ).
cnf(c8300,plain,
( r(X1103,u0r1(X1103))
| r(X1103,u1r1(X1103))
| d(X1103)
| r(X1103,u2r1(X1103))
| ~ c(X1103) ),
inference(resolution,[status(thm)],[c8032,clause_4]) ).
cnf(c8198,plain,
( s(X1101,u0r1(X1101))
| r(X1101,u1r1(X1101))
| d(X1101)
| s(X1101,u2r1(X1101))
| ~ c(X1101) ),
inference(resolution,[status(thm)],[c8031,clause_3]) ).
cnf(c8186,plain,
( r(X1100,u0r1(X1100))
| r(X1100,u1r1(X1100))
| d(X1100)
| s(X1100,u2r1(X1100))
| ~ c(X1100) ),
inference(resolution,[status(thm)],[c8031,clause_4]) ).
cnf(c8094,plain,
( s(X1096,u0r1(X1096))
| s1most(X1096)
| equalish(u0r1(X1096),u0r1(X1096))
| s(X1096,u1r1(X1096))
| ~ c(X1096) ),
inference(resolution,[status(thm)],[c8060,clause_3]) ).
cnf(c3773,plain,
( s(X710,u0r1(X710))
| r(X710,u0r1(X710))
| s1most(X710)
| equalish(X711,u1r2(X710))
| ~ r1most(X710)
| ~ r(X710,X711) ),
inference(resolution,[status(thm)],[c3733,clause_8]) ).
cnf(c8007,plain,
( s(X1092,u0r1(X1092))
| r(X1092,u0r1(X1092))
| s1most(X1092)
| equalish(u1r1(X1092),u1r2(X1092))
| ~ r1most(X1092) ),
inference(resolution,[status(thm)],[c7949,c3773]) ).
cnf(c7993,plain,
( s(X1091,u0r1(X1091))
| r(X1091,u0r1(X1091))
| s1most(X1091)
| equalish(u1r1(X1091),u1r1(X1091))
| ~ r1most(X1091) ),
inference(resolution,[status(thm)],[c7949,c19]) ).
cnf(c7998,plain,
( s(X1085,u0r1(X1085))
| r(X1085,u0r1(X1085))
| s1most(X1085)
| s(X1085,u1r1(X1085))
| ~ c(X1085) ),
inference(resolution,[status(thm)],[c7949,clause_3]) ).
cnf(c7962,plain,
( r(X1075,u0r1(X1075))
| r(X1075,u1r1(X1075))
| s1most(X1075)
| ~ c(X1075) ),
inference(resolution,[status(thm)],[c7949,clause_4]) ).
cnf(c3309,plain,
( d(X984)
| s(X984,u3r1(X984))
| equalish(u0r1(X984),u2r1(X984))
| c(X984)
| equalish(X985,u1r2(X984))
| ~ r1most(X984)
| ~ r(X984,X985) ),
inference(resolution,[status(thm)],[c3269,clause_8]) ).
cnf(c6613,plain,
( d(X988)
| s(X988,u3r1(X988))
| equalish(u0r1(X988),u2r1(X988))
| c(X988)
| equalish(u1r1(X988),u1r2(X988))
| ~ r1most(X988) ),
inference(resolution,[status(thm)],[c3309,c3127]) ).
cnf(c6558,plain,
( d(X986)
| s(X986,u3r1(X986))
| equalish(u0r1(X986),u2r1(X986))
| c(X986)
| equalish(u2r1(X986),u1r2(X986))
| ~ r1most(X986) ),
inference(resolution,[status(thm)],[c3309,c12]) ).
cnf(c6495,plain,
( d(X983)
| equalish(u0r1(X983),u2r1(X983))
| c(X983)
| r(X983,u1r2(X983))
| equalish(u3r2(X983),u3r1(X983))
| ~ s1most(X983) ),
inference(resolution,[status(thm)],[c3278,c2896]) ).
cnf(c3166,plain,
( d(X973)
| s(X973,u3r1(X973))
| equalish(u0r1(X973),u2r1(X973))
| c(X973)
| equalish(X974,u1r1(X973))
| ~ r1most(X973)
| ~ r(X973,X974) ),
inference(resolution,[status(thm)],[c3127,clause_8]) ).
cnf(c6418,plain,
( d(X977)
| s(X977,u3r1(X977))
| equalish(u0r1(X977),u2r1(X977))
| c(X977)
| equalish(u1r2(X977),u1r1(X977))
| ~ r1most(X977) ),
inference(resolution,[status(thm)],[c3166,c3269]) ).
cnf(c6381,plain,
( d(X976)
| s(X976,u3r1(X976))
| equalish(u0r1(X976),u2r1(X976))
| c(X976)
| equalish(u2r1(X976),u1r1(X976))
| ~ r1most(X976) ),
inference(resolution,[status(thm)],[c3166,c12]) ).
cnf(c6310,plain,
( d(X972)
| equalish(u0r1(X972),u2r1(X972))
| c(X972)
| r(X972,u1r1(X972))
| equalish(u3r2(X972),u3r1(X972))
| ~ s1most(X972) ),
inference(resolution,[status(thm)],[c3135,c2757]) ).
cnf(c2935,plain,
( d(X963)
| s(X963,u3r2(X963))
| equalish(u0r1(X963),u2r1(X963))
| c(X963)
| equalish(X964,u1r2(X963))
| ~ r1most(X963)
| ~ r(X963,X964) ),
inference(resolution,[status(thm)],[c2896,clause_8]) ).
cnf(c6246,plain,
( d(X968)
| s(X968,u3r2(X968))
| equalish(u0r1(X968),u2r1(X968))
| c(X968)
| equalish(u1r1(X968),u1r2(X968))
| ~ r1most(X968) ),
inference(resolution,[status(thm)],[c2935,c2757]) ).
cnf(c6208,plain,
( d(X966)
| s(X966,u3r2(X966))
| equalish(u0r1(X966),u2r1(X966))
| c(X966)
| equalish(u2r1(X966),u1r2(X966))
| ~ r1most(X966) ),
inference(resolution,[status(thm)],[c2935,c11]) ).
cnf(c6090,plain,
( d(X961)
| equalish(u0r1(X961),u2r1(X961))
| c(X961)
| r(X961,u1r2(X961))
| equalish(u3r1(X961),u3r2(X961))
| ~ s1most(X961) ),
inference(resolution,[status(thm)],[c2905,c3269]) ).
cnf(c2795,plain,
( d(X953)
| s(X953,u3r2(X953))
| equalish(u0r1(X953),u2r1(X953))
| c(X953)
| equalish(X954,u1r1(X953))
| ~ r1most(X953)
| ~ r(X953,X954) ),
inference(resolution,[status(thm)],[c2757,clause_8]) ).
cnf(c6031,plain,
( d(X956)
| s(X956,u3r2(X956))
| equalish(u0r1(X956),u2r1(X956))
| c(X956)
| equalish(u2r1(X956),u1r1(X956))
| ~ r1most(X956) ),
inference(resolution,[status(thm)],[c2795,c11]) ).
cnf(c5994,plain,
( d(X955)
| s(X955,u3r2(X955))
| equalish(u0r1(X955),u2r1(X955))
| c(X955)
| equalish(u1r2(X955),u1r1(X955))
| ~ r1most(X955) ),
inference(resolution,[status(thm)],[c2795,c2896]) ).
cnf(c5929,plain,
( d(X950)
| equalish(u0r1(X950),u2r1(X950))
| c(X950)
| r(X950,u1r1(X950))
| equalish(u3r1(X950),u3r2(X950))
| ~ s1most(X950) ),
inference(resolution,[status(thm)],[c2765,c3127]) ).
cnf(c5265,plain,
( s(X918,u0r1(X918))
| r(X918,u0r1(X918))
| d(X918)
| equalish(u2r1(X918),u2r1(X918))
| s(X918,u1r2(X918))
| ~ c(X918) ),
inference(resolution,[status(thm)],[c5227,clause_3]) ).
cnf(c4739,plain,
( s(X896,u0r1(X896))
| equalish(u0r1(X896),u0r1(X896))
| d(X896)
| r(X896,u2r1(X896))
| s(X896,u1r2(X896))
| ~ c(X896) ),
inference(resolution,[status(thm)],[c3861,clause_3]) ).
cnf(c4702,plain,
( s(X890,u0r1(X890))
| equalish(u0r1(X890),u0r1(X890))
| d(X890)
| s(X890,u2r1(X890))
| s(X890,u1r2(X890))
| ~ c(X890) ),
inference(resolution,[status(thm)],[c3859,clause_3]) ).
cnf(c4132,plain,
( s(X850,u0r1(X850))
| r(X850,u0r1(X850))
| d(X850)
| r(X850,u2r1(X850))
| equalish(u1r2(X850),u1r2(X850))
| ~ r1most(X850) ),
inference(resolution,[status(thm)],[c3789,c19]) ).
cnf(c5307,plain,
( r(X840,u1r2(X840))
| d(X840)
| equalish(u2r1(X840),u2r1(X840))
| equalish(u0r1(X840),u0r1(X840))
| ~ s1most(X840) ),
inference(resolution,[status(thm)],[c5299,c24]) ).
cnf(c5238,plain,
( r(X832,u0r1(X832))
| r(X832,u1r2(X832))
| d(X832)
| equalish(u2r1(X832),u2r1(X832))
| ~ c(X832) ),
inference(resolution,[status(thm)],[c5227,clause_4]) ).
cnf(c3990,plain,
( s(X829,u0r1(X829))
| r(X829,u0r1(X829))
| d(X829)
| s(X829,u2r1(X829))
| equalish(u1r2(X829),u1r2(X829))
| ~ r1most(X829) ),
inference(resolution,[status(thm)],[c3787,c19]) ).
cnf(c4136,plain,
( s(X774,u0r1(X774))
| r(X774,u0r1(X774))
| d(X774)
| r(X774,u2r1(X774))
| s(X774,u1r2(X774))
| ~ c(X774) ),
inference(resolution,[status(thm)],[c3789,clause_3]) ).
cnf(c3994,plain,
( s(X770,u0r1(X770))
| r(X770,u0r1(X770))
| d(X770)
| s(X770,u2r1(X770))
| s(X770,u1r2(X770))
| ~ c(X770) ),
inference(resolution,[status(thm)],[c3787,clause_3]) ).
cnf(c3838,plain,
( s(X713,u0r1(X713))
| s1most(X713)
| equalish(u0r1(X713),u0r1(X713))
| equalish(u1r2(X713),u1r2(X713))
| ~ r1most(X713) ),
inference(resolution,[status(thm)],[c3818,c19]) ).
cnf(c3756,plain,
( s(X706,u0r1(X706))
| r(X706,u1r2(X706))
| s1most(X706)
| equalish(X707,u0r1(X706))
| ~ r1most(X706)
| ~ r(X706,X707) ),
inference(resolution,[status(thm)],[c3733,clause_8]) ).
cnf(c4119,plain,
( s(X686,u0r1(X686))
| r(X686,u1r2(X686))
| d(X686)
| r(X686,u2r1(X686))
| ~ c(X686) ),
inference(resolution,[status(thm)],[c3789,clause_3]) ).
cnf(c4108,plain,
( r(X685,u0r1(X685))
| r(X685,u1r2(X685))
| d(X685)
| r(X685,u2r1(X685))
| ~ c(X685) ),
inference(resolution,[status(thm)],[c3789,clause_4]) ).
cnf(c3977,plain,
( s(X682,u0r1(X682))
| r(X682,u1r2(X682))
| d(X682)
| s(X682,u2r1(X682))
| ~ c(X682) ),
inference(resolution,[status(thm)],[c3787,clause_3]) ).
cnf(c3966,plain,
( r(X681,u0r1(X681))
| r(X681,u1r2(X681))
| d(X681)
| s(X681,u2r1(X681))
| ~ c(X681) ),
inference(resolution,[status(thm)],[c3787,clause_4]) ).
cnf(c3842,plain,
( s(X678,u0r1(X678))
| s1most(X678)
| equalish(u0r1(X678),u0r1(X678))
| s(X678,u1r2(X678))
| ~ c(X678) ),
inference(resolution,[status(thm)],[c3818,clause_3]) ).
cnf(c3766,plain,
( s(X674,u0r1(X674))
| r(X674,u0r1(X674))
| s1most(X674)
| equalish(u1r2(X674),u1r2(X674))
| ~ r1most(X674) ),
inference(resolution,[status(thm)],[c3733,c19]) ).
cnf(c3770,plain,
( s(X668,u0r1(X668))
| r(X668,u0r1(X668))
| s1most(X668)
| s(X668,u1r2(X668))
| ~ c(X668) ),
inference(resolution,[status(thm)],[c3733,clause_3]) ).
cnf(c3742,plain,
( r(X658,u0r1(X658))
| r(X658,u1r2(X658))
| s1most(X658)
| ~ c(X658) ),
inference(resolution,[status(thm)],[c3733,clause_4]) ).
cnf(c3308,plain,
( d(X577)
| s(X577,u3r1(X577))
| equalish(u0r1(X577),u2r1(X577))
| c(X577)
| equalish(u1r2(X577),u2r1(X577))
| ~ r1most(X577) ),
inference(resolution,[status(thm)],[c3269,c57]) ).
cnf(c3301,plain,
( d(X576)
| s(X576,u3r1(X576))
| equalish(u0r1(X576),u2r1(X576))
| c(X576)
| equalish(u1r2(X576),u1r2(X576))
| ~ r1most(X576) ),
inference(resolution,[status(thm)],[c3269,c19]) ).
cnf(c3273,plain,
( d(X575)
| equalish(u0r1(X575),u2r1(X575))
| c(X575)
| r(X575,u1r2(X575))
| equalish(u3r1(X575),u3r1(X575))
| ~ s1most(X575) ),
inference(resolution,[status(thm)],[c3269,c24]) ).
cnf(c3165,plain,
( d(X564)
| s(X564,u3r1(X564))
| equalish(u0r1(X564),u2r1(X564))
| c(X564)
| equalish(u1r1(X564),u2r1(X564))
| ~ r1most(X564) ),
inference(resolution,[status(thm)],[c3127,c57]) ).
cnf(c3158,plain,
( d(X563)
| s(X563,u3r1(X563))
| equalish(u0r1(X563),u2r1(X563))
| c(X563)
| equalish(u1r1(X563),u1r1(X563))
| ~ r1most(X563) ),
inference(resolution,[status(thm)],[c3127,c19]) ).
cnf(c3130,plain,
( d(X562)
| equalish(u0r1(X562),u2r1(X562))
| c(X562)
| r(X562,u1r1(X562))
| equalish(u3r1(X562),u3r1(X562))
| ~ s1most(X562) ),
inference(resolution,[status(thm)],[c3127,c24]) ).
cnf(c2933,plain,
( d(X550)
| s(X550,u3r2(X550))
| equalish(u0r1(X550),u2r1(X550))
| c(X550)
| equalish(u1r2(X550),u2r1(X550))
| ~ r1most(X550) ),
inference(resolution,[status(thm)],[c2896,c49]) ).
cnf(c2928,plain,
( d(X548)
| s(X548,u3r2(X548))
| equalish(u0r1(X548),u2r1(X548))
| c(X548)
| equalish(u1r2(X548),u1r2(X548))
| ~ r1most(X548) ),
inference(resolution,[status(thm)],[c2896,c19]) ).
cnf(c2900,plain,
( d(X547)
| equalish(u0r1(X547),u2r1(X547))
| c(X547)
| r(X547,u1r2(X547))
| equalish(u3r2(X547),u3r2(X547))
| ~ s1most(X547) ),
inference(resolution,[status(thm)],[c2896,c24]) ).
cnf(c2793,plain,
( d(X535)
| s(X535,u3r2(X535))
| equalish(u0r1(X535),u2r1(X535))
| c(X535)
| equalish(u1r1(X535),u2r1(X535))
| ~ r1most(X535) ),
inference(resolution,[status(thm)],[c2757,c49]) ).
cnf(c2788,plain,
( d(X534)
| s(X534,u3r2(X534))
| equalish(u0r1(X534),u2r1(X534))
| c(X534)
| equalish(u1r1(X534),u1r1(X534))
| ~ r1most(X534) ),
inference(resolution,[status(thm)],[c2757,c19]) ).
cnf(c2760,plain,
( d(X533)
| equalish(u0r1(X533),u2r1(X533))
| c(X533)
| r(X533,u1r1(X533))
| equalish(u3r2(X533),u3r2(X533))
| ~ s1most(X533) ),
inference(resolution,[status(thm)],[c2757,c24]) ).
cnf(c484,plain,
( c(X185)
| r(X185,u1r1(X185))
| equalish(u0r1(X185),u0r1(X185))
| ~ s1most(X185) ),
inference(resolution,[status(thm)],[c473,c24]) ).
cnf(c504,plain,
( c(X190)
| r(X190,u1r1(X190))
| equalish(u0r1(X190),u0r1(X190))
| s(X190,u3r2(X190)) ),
inference(resolution,[status(thm)],[c484,clause_19]) ).
cnf(c566,plain,
( c(X368)
| equalish(u0r1(X368),u0r1(X368))
| s(X368,u3r2(X368))
| equalish(X369,u1r1(X368))
| ~ r1most(X368)
| ~ r(X368,X369) ),
inference(resolution,[status(thm)],[c504,clause_8]) ).
cnf(c1761,plain,
( c(X446)
| equalish(u0r1(X446),u0r1(X446))
| s(X446,u3r2(X446))
| equalish(u2r1(X446),u1r1(X446))
| ~ r1most(X446)
| d(X446) ),
inference(resolution,[status(thm)],[c566,c11]) ).
cnf(c502,plain,
( c(X189)
| r(X189,u1r1(X189))
| equalish(u0r1(X189),u0r1(X189))
| s(X189,u3r1(X189)) ),
inference(resolution,[status(thm)],[c484,clause_18]) ).
cnf(c540,plain,
( c(X361)
| equalish(u0r1(X361),u0r1(X361))
| s(X361,u3r1(X361))
| equalish(X362,u1r1(X361))
| ~ r1most(X361)
| ~ r(X361,X362) ),
inference(resolution,[status(thm)],[c502,clause_8]) ).
cnf(c1671,plain,
( c(X439)
| equalish(u0r1(X439),u0r1(X439))
| s(X439,u3r1(X439))
| equalish(u2r1(X439),u1r1(X439))
| ~ r1most(X439)
| d(X439) ),
inference(resolution,[status(thm)],[c540,c12]) ).
cnf(c274,plain,
( c(X143)
| r(X143,u1r2(X143))
| equalish(u0r1(X143),u0r1(X143))
| ~ s1most(X143) ),
inference(resolution,[status(thm)],[c257,c24]) ).
cnf(c290,plain,
( c(X148)
| r(X148,u1r2(X148))
| equalish(u0r1(X148),u0r1(X148))
| s(X148,u3r2(X148)) ),
inference(resolution,[status(thm)],[c274,clause_19]) ).
cnf(c339,plain,
( c(X340)
| equalish(u0r1(X340),u0r1(X340))
| s(X340,u3r2(X340))
| equalish(X341,u1r2(X340))
| ~ r1most(X340)
| ~ r(X340,X341) ),
inference(resolution,[status(thm)],[c290,clause_8]) ).
cnf(c1527,plain,
( c(X428)
| equalish(u0r1(X428),u0r1(X428))
| s(X428,u3r2(X428))
| equalish(u2r1(X428),u1r2(X428))
| ~ r1most(X428)
| d(X428) ),
inference(resolution,[status(thm)],[c339,c11]) ).
cnf(c288,plain,
( c(X147)
| r(X147,u1r2(X147))
| equalish(u0r1(X147),u0r1(X147))
| s(X147,u3r1(X147)) ),
inference(resolution,[status(thm)],[c274,clause_18]) ).
cnf(c316,plain,
( c(X333)
| equalish(u0r1(X333),u0r1(X333))
| s(X333,u3r1(X333))
| equalish(X334,u1r2(X333))
| ~ r1most(X333)
| ~ r(X333,X334) ),
inference(resolution,[status(thm)],[c288,clause_8]) ).
cnf(c1437,plain,
( c(X422)
| equalish(u0r1(X422),u0r1(X422))
| s(X422,u3r1(X422))
| equalish(u2r1(X422),u1r2(X422))
| ~ r1most(X422)
| d(X422) ),
inference(resolution,[status(thm)],[c316,c12]) ).
cnf(c570,plain,
( c(X399)
| equalish(u0r1(X399),u0r1(X399))
| s(X399,u3r2(X399))
| d(X399)
| equalish(u1r1(X399),u2r1(X399))
| ~ r1most(X399) ),
inference(resolution,[status(thm)],[c504,c49]) ).
cnf(c545,plain,
( c(X398)
| equalish(u0r1(X398),u0r1(X398))
| s(X398,u3r1(X398))
| d(X398)
| equalish(u1r1(X398),u2r1(X398))
| ~ r1most(X398) ),
inference(resolution,[status(thm)],[c502,c57]) ).
cnf(c343,plain,
( c(X397)
| equalish(u0r1(X397),u0r1(X397))
| s(X397,u3r2(X397))
| d(X397)
| equalish(u1r2(X397),u2r1(X397))
| ~ r1most(X397) ),
inference(resolution,[status(thm)],[c290,c49]) ).
cnf(c321,plain,
( c(X396)
| equalish(u0r1(X396),u0r1(X396))
| s(X396,u3r1(X396))
| d(X396)
| equalish(u1r2(X396),u2r1(X396))
| ~ r1most(X396) ),
inference(resolution,[status(thm)],[c288,c57]) ).
cnf(c1751,plain,
( c(X370)
| equalish(u0r1(X370),u0r1(X370))
| s(X370,u3r2(X370))
| equalish(u1r2(X370),u1r1(X370))
| ~ r1most(X370) ),
inference(resolution,[status(thm)],[c566,c290]) ).
cnf(c1679,plain,
( c(X363)
| equalish(u0r1(X363),u0r1(X363))
| s(X363,u3r1(X363))
| equalish(u1r2(X363),u1r1(X363))
| ~ r1most(X363) ),
inference(resolution,[status(thm)],[c540,c288]) ).
cnf(c494,plain,
( c(X356)
| s(X356,u0r1(X356))
| equalish(u0r1(X356),u0r1(X356))
| equalish(X357,u1r1(X356))
| ~ r1most(X356)
| ~ r(X356,X357) ),
inference(resolution,[status(thm)],[c473,clause_8]) ).
cnf(c1623,plain,
( c(X360)
| s(X360,u0r1(X360))
| equalish(u0r1(X360),u0r1(X360))
| equalish(u1r2(X360),u1r1(X360))
| ~ r1most(X360) ),
inference(resolution,[status(thm)],[c494,c257]) ).
cnf(c1523,plain,
( c(X343)
| equalish(u0r1(X343),u0r1(X343))
| s(X343,u3r2(X343))
| equalish(u1r1(X343),u1r2(X343))
| ~ r1most(X343) ),
inference(resolution,[status(thm)],[c339,c504]) ).
cnf(c1472,plain,
( c(X336)
| equalish(u0r1(X336),u0r1(X336))
| s(X336,u3r1(X336))
| equalish(u1r1(X336),u1r2(X336))
| ~ r1most(X336) ),
inference(resolution,[status(thm)],[c316,c502]) ).
cnf(c282,plain,
( c(X328)
| s(X328,u0r1(X328))
| equalish(u0r1(X328),u0r1(X328))
| equalish(X329,u1r2(X328))
| ~ r1most(X328)
| ~ r(X328,X329) ),
inference(resolution,[status(thm)],[c257,clause_8]) ).
cnf(c1361,plain,
( c(X330)
| s(X330,u0r1(X330))
| equalish(u0r1(X330),u0r1(X330))
| equalish(u1r1(X330),u1r2(X330))
| ~ r1most(X330) ),
inference(resolution,[status(thm)],[c282,c473]) ).
cnf(c569,plain,
( c(X270)
| equalish(u0r1(X270),u0r1(X270))
| s(X270,u3r2(X270))
| equalish(u1r1(X270),u1r1(X270))
| ~ r1most(X270) ),
inference(resolution,[status(thm)],[c504,c19]) ).
cnf(c543,plain,
( c(X268)
| equalish(u0r1(X268),u0r1(X268))
| s(X268,u3r1(X268))
| equalish(u1r1(X268),u1r1(X268))
| ~ r1most(X268) ),
inference(resolution,[status(thm)],[c502,c19]) ).
cnf(c497,plain,
( c(X267)
| s(X267,u0r1(X267))
| equalish(u0r1(X267),u0r1(X267))
| equalish(u1r1(X267),u1r1(X267))
| ~ r1most(X267) ),
inference(resolution,[status(thm)],[c473,c19]) ).
cnf(c342,plain,
( c(X257)
| equalish(u0r1(X257),u0r1(X257))
| s(X257,u3r2(X257))
| equalish(u1r2(X257),u1r2(X257))
| ~ r1most(X257) ),
inference(resolution,[status(thm)],[c290,c19]) ).
cnf(c319,plain,
( c(X255)
| equalish(u0r1(X255),u0r1(X255))
| s(X255,u3r1(X255))
| equalish(u1r2(X255),u1r2(X255))
| ~ r1most(X255) ),
inference(resolution,[status(thm)],[c288,c19]) ).
cnf(c284,plain,
( c(X254)
| s(X254,u0r1(X254))
| equalish(u0r1(X254),u0r1(X254))
| equalish(u1r2(X254),u1r2(X254))
| ~ r1most(X254) ),
inference(resolution,[status(thm)],[c257,c19]) ).
cnf(clause_12,axiom,
( ~ d(X14)
| ~ r(X14,X13)
| ~ s(X14,X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_12) ).
cnf(c575,plain,
( c(X238)
| r(X238,u1r1(X238))
| equalish(u0r1(X238),u0r1(X238))
| ~ d(X238)
| ~ r(X238,u3r2(X238)) ),
inference(resolution,[status(thm)],[c504,clause_12]) ).
cnf(c549,plain,
( c(X234)
| r(X234,u1r1(X234))
| equalish(u0r1(X234),u0r1(X234))
| ~ d(X234)
| ~ r(X234,u3r1(X234)) ),
inference(resolution,[status(thm)],[c502,clause_12]) ).
cnf(c485,plain,
( c(X226)
| r(X226,u1r1(X226))
| equalish(u0r1(X226),u0r1(X226))
| ~ d(X226)
| ~ r(X226,u0r1(X226)) ),
inference(resolution,[status(thm)],[c473,clause_12]) ).
cnf(c347,plain,
( c(X222)
| r(X222,u1r2(X222))
| equalish(u0r1(X222),u0r1(X222))
| ~ d(X222)
| ~ r(X222,u3r2(X222)) ),
inference(resolution,[status(thm)],[c290,clause_12]) ).
cnf(c324,plain,
( c(X219)
| r(X219,u1r2(X219))
| equalish(u0r1(X219),u0r1(X219))
| ~ d(X219)
| ~ r(X219,u3r1(X219)) ),
inference(resolution,[status(thm)],[c288,clause_12]) ).
cnf(c275,plain,
( c(X210)
| r(X210,u1r2(X210))
| equalish(u0r1(X210),u0r1(X210))
| ~ d(X210)
| ~ r(X210,u0r1(X210)) ),
inference(resolution,[status(thm)],[c257,clause_12]) ).
cnf(c363,plain,
( d(X155)
| equalish(u2r1(X155),u2r1(X155))
| equalish(u3r2(X155),u3r1(X155))
| ~ s1most(X155) ),
inference(resolution,[status(thm)],[c128,c94]) ).
cnf(c242,plain,
( d(X140)
| equalish(u2r1(X140),u2r1(X140))
| equalish(u3r1(X140),u3r2(X140))
| ~ s1most(X140) ),
inference(resolution,[status(thm)],[c100,c123]) ).
cnf(c126,plain,
( d(X116)
| equalish(u2r1(X116),u2r1(X116))
| equalish(u3r1(X116),u3r1(X116))
| ~ s1most(X116) ),
inference(resolution,[status(thm)],[c123,c24]) ).
cnf(c98,plain,
( d(X114)
| equalish(u2r1(X114),u2r1(X114))
| equalish(u3r2(X114),u3r2(X114))
| ~ s1most(X114) ),
inference(resolution,[status(thm)],[c94,c24]) ).
cnf(c129,plain,
( d(X100)
| equalish(u2r1(X100),u2r1(X100))
| r(X100,u3r1(X100))
| ~ c(X100) ),
inference(resolution,[status(thm)],[c123,clause_4]) ).
cnf(c101,plain,
( d(X95)
| equalish(u2r1(X95),u2r1(X95))
| r(X95,u3r2(X95))
| ~ c(X95) ),
inference(resolution,[status(thm)],[c94,clause_4]) ).
cnf(c62,plain,
( d(X76)
| r(X76,u2r1(X76))
| r(X76,u3r1(X76))
| ~ c(X76) ),
inference(resolution,[status(thm)],[c12,clause_4]) ).
cnf(c54,plain,
( d(X73)
| r(X73,u2r1(X73))
| r(X73,u3r2(X73))
| ~ c(X73) ),
inference(resolution,[status(thm)],[c11,clause_4]) ).
cnf(c46,plain,
( d(X68)
| s(X68,u2r1(X68))
| r(X68,u3r1(X68))
| ~ c(X68) ),
inference(resolution,[status(thm)],[c9,clause_4]) ).
cnf(c37,plain,
( d(X61)
| s(X61,u2r1(X61))
| r(X61,u3r2(X61))
| ~ c(X61) ),
inference(resolution,[status(thm)],[c8,clause_4]) ).
cnf(clause_9,axiom,
( r1most(X12)
| ~ equalish(u1r2(X12),u1r1(X12)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_9) ).
cnf(clause_2,negated_conjecture,
d(exist),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2) ).
cnf(clause_13,axiom,
( s1most(X3)
| ~ d(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_13) ).
cnf(c1,plain,
s1most(exist),
inference(resolution,[status(thm)],[clause_13,clause_2]) ).
cnf(clause_1,negated_conjecture,
c(exist),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1) ).
cnf(clause_5,axiom,
( r1most(X2)
| ~ c(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_5) ).
cnf(c0,plain,
r1most(exist),
inference(resolution,[status(thm)],[clause_5,clause_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : KRS016-1 : TPTP v8.1.2. Released v2.0.0.
% 0.09/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n021.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Thu May 9 00:15:38 EDT 2024
% 0.15/0.37 % CPUTime :
% 30.88/31.10 % Version: 1.5
% 30.88/31.10 % SZS status Satisfiable
% 30.88/31.10 % SZS output start Saturation
% See solution above
% 30.88/31.12
% 30.88/31.12 % Initial clauses : 19
% 30.88/31.12 % Processed clauses : 489
% 30.88/31.12 % Factors computed : 2
% 30.88/31.12 % Resolvents computed: 12815
% 30.88/31.12 % Tautologies deleted: 941
% 30.88/31.12 % Forward subsumed : 11406
% 30.88/31.12 % Backward subsumed : 184
% 30.88/31.12 % -------- CPU Time ---------
% 30.88/31.12 % User time : 30.685 s
% 30.88/31.12 % System time : 0.062 s
% 30.88/31.12 % Total time : 30.747 s
%------------------------------------------------------------------------------