%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYO579+1 : TPTP v8.1.0. Released v5.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n014.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 : 600s
% DateTime : Thu Jul 21 19:54:47 EDT 2022
% Result : CounterSatisfiable 0.19s 0.54s
% Output : Saturation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 1502)
% Comments :
%------------------------------------------------------------------------------
cnf(1521,plain,
~ b48_buttercup10104(skc109),
inference(ems,[status(thm)],[115,1512,104]),
[iquote('0:EmS:115.0,115.1,1512.0,104.1')] ).
cnf(1520,plain,
~ b48_buttercup10110(skc109),
inference(ems,[status(thm)],[115,1512,105]),
[iquote('0:EmS:115.0,115.1,1512.0,105.1')] ).
cnf(1519,plain,
~ b48_buttercup10108(skc109),
inference(ems,[status(thm)],[115,1512,106]),
[iquote('0:EmS:115.0,115.1,1512.0,106.1')] ).
cnf(1518,plain,
~ b48_buttercup10102(skc109),
inference(ems,[status(thm)],[115,1512,109]),
[iquote('0:EmS:115.0,115.1,1512.0,109.1')] ).
cnf(1512,plain,
k04_buttercup10620(skc109),
inference(ems,[status(thm)],[129,1502,41]),
[iquote('0:EmS:129.0,129.1,1502.0,41.0')] ).
cnf(1485,plain,
~ b48_buttercup10104(skc95),
inference(ems,[status(thm)],[115,1476,104]),
[iquote('0:EmS:115.0,115.1,1476.0,104.1')] ).
cnf(1484,plain,
~ b48_buttercup10110(skc95),
inference(ems,[status(thm)],[115,1476,105]),
[iquote('0:EmS:115.0,115.1,1476.0,105.1')] ).
cnf(1483,plain,
~ b48_buttercup10108(skc95),
inference(ems,[status(thm)],[115,1476,106]),
[iquote('0:EmS:115.0,115.1,1476.0,106.1')] ).
cnf(1482,plain,
~ b48_buttercup10102(skc95),
inference(ems,[status(thm)],[115,1476,109]),
[iquote('0:EmS:115.0,115.1,1476.0,109.1')] ).
cnf(1476,plain,
k04_buttercup10620(skc95),
inference(ems,[status(thm)],[129,1466,31]),
[iquote('0:EmS:129.0,129.1,1466.0,31.0')] ).
cnf(1437,plain,
( ~ k04_buttercup10619(u)
| ~ b48_buttercup10111(u) ),
inference(mrr,[status(thm)],[1372,157,156,154,153,483]),
[iquote('1:MRR:1372.2,1372.3,1372.4,1372.5,1372.6,157.0,156.0,154.0,153.0,483.1')] ).
cnf(978,plain,
( ~ k04_buttercup10619(u)
| b48_buttercup10110(u)
| b48_buttercup10109(u)
| b48_buttercup10108(u)
| b48_buttercup10104(u)
| b48_buttercup10102(u)
| k04_buttercup10620(u) ),
inference(mrr,[status(thm)],[977,111]),
[iquote('0:MRR:977.4,111.0')] ).
cnf(1348,plain,
( ~ k04_buttercup10619(skc58)
| b48_buttercup10102(skc58)
| b48_buttercup10104(skc58)
| b48_buttercup10107(skc58)
| b48_buttercup10108(skc58)
| b48_buttercup10110(skc58) ),
inference(sor,[status(thm)],[828,99]),
[iquote('0:SoR:828.0,99.1')] ).
cnf(1338,plain,
( ~ k04_buttercup10619(skc76)
| b48_buttercup10102(skc76)
| b48_buttercup10104(skc76)
| b48_buttercup10107(skc76)
| b48_buttercup10108(skc76)
| b48_buttercup10110(skc76) ),
inference(sor,[status(thm)],[827,99]),
[iquote('0:SoR:827.0,99.1')] ).
cnf(1326,plain,
( ~ k04_buttercup10619(skc81)
| b48_buttercup10102(skc81)
| b48_buttercup10104(skc81)
| b48_buttercup10107(skc81)
| b48_buttercup10108(skc81)
| b48_buttercup10110(skc81) ),
inference(sor,[status(thm)],[826,99]),
[iquote('0:SoR:826.0,99.1')] ).
cnf(1045,plain,
( ~ k04_buttercup10619(skc66)
| b48_buttercup10110(skc66)
| b48_buttercup10109(skc66)
| b48_buttercup10108(skc66)
| b48_buttercup10107(skc66)
| b48_buttercup10104(skc66)
| b48_buttercup10102(skc66) ),
inference(sor,[status(thm)],[818,99]),
[iquote('0:SoR:818.0,99.1')] ).
cnf(1314,plain,
( ~ k04_buttercup10619(skc90)
| b48_buttercup10102(skc90)
| b48_buttercup10104(skc90)
| b48_buttercup10107(skc90)
| b48_buttercup10108(skc90)
| b48_buttercup10110(skc90) ),
inference(sor,[status(thm)],[823,99]),
[iquote('0:SoR:823.0,99.1')] ).
cnf(1293,plain,
( ~ k04_buttercup10619(skc96)
| b48_buttercup10102(skc96)
| b48_buttercup10104(skc96)
| b48_buttercup10107(skc96)
| b48_buttercup10108(skc96)
| b48_buttercup10110(skc96) ),
inference(sor,[status(thm)],[822,99]),
[iquote('0:SoR:822.0,99.1')] ).
cnf(1355,plain,
~ k04_buttercup10100(skc58),
inference(mrr,[status(thm)],[1354,700,694,880,671,681]),
[iquote('1:MRR:1354.1,1354.2,1354.3,1354.4,1354.5,700.0,694.0,880.0,671.0,681.0')] ).
cnf(1345,plain,
~ k04_buttercup10100(skc76),
inference(mrr,[status(thm)],[1344,700,694,880,671,681]),
[iquote('1:MRR:1344.1,1344.2,1344.3,1344.4,1344.5,700.0,694.0,880.0,671.0,681.0')] ).
cnf(828,plain,
( ~ b48_buttercup10098(skc58)
| b48_buttercup10102(skc58)
| b48_buttercup10104(skc58)
| b48_buttercup10107(skc58)
| b48_buttercup10108(skc58)
| b48_buttercup10110(skc58) ),
inference(mrr,[status(thm)],[812,394]),
[iquote('0:MRR:812.5,394.0')] ).
cnf(827,plain,
( ~ b48_buttercup10098(skc76)
| b48_buttercup10102(skc76)
| b48_buttercup10104(skc76)
| b48_buttercup10107(skc76)
| b48_buttercup10108(skc76)
| b48_buttercup10110(skc76) ),
inference(mrr,[status(thm)],[811,393]),
[iquote('0:MRR:811.5,393.0')] ).
cnf(1333,plain,
~ k04_buttercup10100(skc81),
inference(mrr,[status(thm)],[1332,700,694,880,671,681]),
[iquote('1:MRR:1332.1,1332.2,1332.3,1332.4,1332.5,700.0,694.0,880.0,671.0,681.0')] ).
cnf(826,plain,
( ~ b48_buttercup10098(skc81)
| b48_buttercup10102(skc81)
| b48_buttercup10104(skc81)
| b48_buttercup10107(skc81)
| b48_buttercup10108(skc81)
| b48_buttercup10110(skc81) ),
inference(mrr,[status(thm)],[810,392]),
[iquote('0:MRR:810.5,392.0')] ).
cnf(1321,plain,
~ k04_buttercup10100(skc90),
inference(mrr,[status(thm)],[1320,700,694,880,671,681]),
[iquote('1:MRR:1320.1,1320.2,1320.3,1320.4,1320.5,700.0,694.0,880.0,671.0,681.0')] ).
cnf(823,plain,
( ~ b48_buttercup10098(skc90)
| b48_buttercup10102(skc90)
| b48_buttercup10104(skc90)
| b48_buttercup10107(skc90)
| b48_buttercup10108(skc90)
| b48_buttercup10110(skc90) ),
inference(mrr,[status(thm)],[808,390]),
[iquote('0:MRR:808.5,390.0')] ).
cnf(1306,plain,
( ~ k04_buttercup10622(skc83)
| b48_buttercup10108(skc83)
| b48_buttercup10104(skc83)
| b48_buttercup10102(skc83) ),
inference(mrr,[status(thm)],[1305,115]),
[iquote('2:MRR:1305.4,115.0')] ).
cnf(1290,plain,
( ~ k04_buttercup10619(skc83)
| b48_buttercup10108(skc83)
| b48_buttercup10104(skc83)
| b48_buttercup10102(skc83)
| k04_buttercup10620(skc83) ),
inference(mrr,[status(thm)],[1288,111]),
[iquote('2:MRR:1288.2,111.0')] ).
cnf(1300,plain,
~ k04_buttercup10100(skc96),
inference(mrr,[status(thm)],[1299,700,694,880,671,681]),
[iquote('1:MRR:1299.1,1299.2,1299.3,1299.4,1299.5,700.0,694.0,880.0,671.0,681.0')] ).
cnf(1289,plain,
~ b48_buttercup10110(skc83),
inference(mrr,[status(thm)],[1286,150,149,148,147]),
[iquote('2:MRR:1286.1,1286.2,1286.3,1286.4,150.0,149.0,148.0,147.0')] ).
cnf(822,plain,
( ~ b48_buttercup10098(skc96)
| b48_buttercup10102(skc96)
| b48_buttercup10104(skc96)
| b48_buttercup10107(skc96)
| b48_buttercup10108(skc96)
| b48_buttercup10110(skc96) ),
inference(mrr,[status(thm)],[807,389]),
[iquote('0:MRR:807.5,389.0')] ).
cnf(1281,plain,
~ b48_buttercup10111(skc103),
inference(mrr,[status(thm)],[1277,157,156,154,153]),
[iquote('1:MRR:1277.1,1277.2,1277.3,1277.4,157.0,156.0,154.0,153.0')] ).
cnf(976,plain,
( b48_buttercup10110(skc103)
| b48_buttercup10109(skc103)
| b48_buttercup10108(skc103)
| b48_buttercup10104(skc103)
| b48_buttercup10102(skc103) ),
inference(mrr,[status(thm)],[975,407]),
[iquote('0:MRR:975.3,407.0')] ).
cnf(836,plain,
( b48_buttercup10102(skc101)
| b48_buttercup10104(skc101)
| b48_buttercup10107(skc101)
| b48_buttercup10108(skc101)
| b48_buttercup10110(skc101) ),
inference(mrr,[status(thm)],[835,537]),
[iquote('0:MRR:835.4,537.0')] ).
cnf(834,plain,
( b48_buttercup10102(skc71)
| b48_buttercup10104(skc71)
| b48_buttercup10107(skc71)
| b48_buttercup10108(skc71)
| b48_buttercup10110(skc71) ),
inference(mrr,[status(thm)],[833,535]),
[iquote('0:MRR:833.4,535.0')] ).
cnf(832,plain,
( b48_buttercup10102(skc73)
| b48_buttercup10104(skc73)
| b48_buttercup10107(skc73)
| b48_buttercup10108(skc73)
| b48_buttercup10110(skc73) ),
inference(mrr,[status(thm)],[831,533]),
[iquote('0:MRR:831.4,533.0')] ).
cnf(830,plain,
( b48_buttercup10102(skc65)
| b48_buttercup10104(skc65)
| b48_buttercup10107(skc65)
| b48_buttercup10108(skc65)
| b48_buttercup10110(skc65) ),
inference(mrr,[status(thm)],[829,531]),
[iquote('0:MRR:829.4,531.0')] ).
cnf(825,plain,
( b48_buttercup10102(skc88)
| b48_buttercup10104(skc88)
| b48_buttercup10107(skc88)
| b48_buttercup10108(skc88)
| b48_buttercup10110(skc88) ),
inference(mrr,[status(thm)],[824,391]),
[iquote('0:MRR:824.4,391.0')] ).
cnf(1244,plain,
~ b48_buttercup10111(skc94),
inference(mrr,[status(thm)],[1240,157,156,154]),
[iquote('1:MRR:1240.1,1240.2,1240.3,157.0,156.0,154.0')] ).
cnf(821,plain,
( b48_buttercup10102(skc67)
| b48_buttercup10104(skc67)
| b48_buttercup10107(skc67)
| b48_buttercup10108(skc67)
| b48_buttercup10110(skc67) ),
inference(mrr,[status(thm)],[820,529]),
[iquote('0:MRR:820.4,529.0')] ).
cnf(974,plain,
( b48_buttercup10110(skc94)
| b48_buttercup10109(skc94)
| b48_buttercup10108(skc94)
| b48_buttercup10104(skc94) ),
inference(mrr,[status(thm)],[973,406,63]),
[iquote('0:MRR:973.3,973.5,406.0,63.0')] ).
cnf(1237,plain,
~ b48_buttercup10111(skc87),
inference(mrr,[status(thm)],[1233,157,154,153]),
[iquote('1:MRR:1233.1,1233.2,1233.3,157.0,154.0,153.0')] ).
cnf(972,plain,
( b48_buttercup10110(skc87)
| b48_buttercup10109(skc87)
| b48_buttercup10104(skc87)
| b48_buttercup10102(skc87) ),
inference(mrr,[status(thm)],[971,59,405]),
[iquote('0:MRR:971.2,971.3,59.0,405.0')] ).
cnf(1230,plain,
~ b48_buttercup10111(skc85),
inference(mrr,[status(thm)],[1226,157,156,153]),
[iquote('1:MRR:1226.1,1226.2,1226.3,157.0,156.0,153.0')] ).
cnf(968,plain,
( b48_buttercup10110(skc85)
| b48_buttercup10109(skc85)
| b48_buttercup10108(skc85)
| b48_buttercup10102(skc85) ),
inference(mrr,[status(thm)],[967,403,57]),
[iquote('0:MRR:967.3,967.4,403.0,57.0')] ).
cnf(1222,plain,
~ b48_buttercup10109(skc86),
inference(mrr,[status(thm)],[1217,142,141]),
[iquote('2:MRR:1217.1,1217.2,142.0,141.0')] ).
cnf(1221,plain,
~ b48_buttercup10111(skc86),
inference(mrr,[status(thm)],[1216,154,153]),
[iquote('2:MRR:1216.1,1216.2,154.0,153.0')] ).
cnf(1176,plain,
( b48_buttercup10108(skc86)
| b48_buttercup10104(skc86)
| b48_buttercup10102(skc86) ),
inference(mrr,[status(thm)],[1175,404]),
[iquote('2:MRR:1175.1,404.0')] ).
cnf(1210,plain,
~ b48_buttercup10109(skc102),
inference(ems,[status(thm)],[880,1199,97]),
[iquote('0:EmS:880.0,880.1,1199.0,97.1')] ).
cnf(1053,plain,
( ~ k04_buttercup10100(skc66)
| b48_buttercup10109(skc66) ),
inference(mrr,[status(thm)],[1051,681,671,880,694,700]),
[iquote('1:MRR:1051.1,1051.3,1051.4,1051.5,1051.6,681.0,671.0,880.0,694.0,700.0')] ).
cnf(1209,plain,
~ b48_buttercup10111(skc102),
inference(ems,[status(thm)],[880,1199,101]),
[iquote('0:EmS:880.0,880.1,1199.0,101.1')] ).
cnf(1199,plain,
b48_buttercup10107(skc102),
inference(ems,[status(thm)],[484,923,34]),
[iquote('0:EmS:484.0,484.1,923.0,34.0')] ).
cnf(1052,plain,
~ b48_buttercup10111(skc66),
inference(mrr,[status(thm)],[1043,158,157,156,155,154,153]),
[iquote('0:MRR:1043.1,1043.2,1043.3,1043.4,1043.5,1043.6,158.0,157.0,156.0,155.0,154.0,153.0')] ).
cnf(1026,plain,
~ b48_buttercup10109(skc109),
inference(ems,[status(thm)],[880,41,97]),
[iquote('0:EmS:880.0,880.1,41.0,97.1')] ).
cnf(1025,plain,
~ b48_buttercup10109(skc95),
inference(ems,[status(thm)],[880,31,97]),
[iquote('0:EmS:880.0,880.1,31.0,97.1')] ).
cnf(1023,plain,
~ b48_buttercup10111(skc109),
inference(ems,[status(thm)],[880,41,101]),
[iquote('0:EmS:880.0,880.1,41.0,101.1')] ).
cnf(1022,plain,
~ b48_buttercup10111(skc95),
inference(ems,[status(thm)],[880,31,101]),
[iquote('0:EmS:880.0,880.1,31.0,101.1')] ).
cnf(1020,plain,
~ k04_buttercup10622(skc111),
inference(sor,[status(thm)],[996,88]),
[iquote('0:SoR:996.0,88.1')] ).
cnf(1018,plain,
~ b48_buttercup10109(skc107),
inference(ems,[status(thm)],[700,39,97]),
[iquote('0:EmS:700.0,700.1,39.0,97.1')] ).
cnf(1017,plain,
~ b48_buttercup10109(skc89),
inference(ems,[status(thm)],[700,27,97]),
[iquote('0:EmS:700.0,700.1,27.0,97.1')] ).
cnf(1016,plain,
~ b48_buttercup10111(skc107),
inference(ems,[status(thm)],[700,39,101]),
[iquote('0:EmS:700.0,700.1,39.0,101.1')] ).
cnf(1015,plain,
~ b48_buttercup10111(skc89),
inference(ems,[status(thm)],[700,27,101]),
[iquote('0:EmS:700.0,700.1,27.0,101.1')] ).
cnf(1014,plain,
~ k04_buttercup10622(skc105),
inference(sor,[status(thm)],[966,88]),
[iquote('0:SoR:966.0,88.1')] ).
cnf(1116,plain,
( ~ k04_buttercup10622(u)
| b48_buttercup10110(u)
| b48_buttercup10108(u)
| b48_buttercup10107(u)
| b48_buttercup10104(u)
| b48_buttercup10102(u) ),
inference(spt,[],[843]),
[iquote('2:Spt:843.1,843.2,843.3,843.4,843.5,843.6')] ).
cnf(1012,plain,
~ b48_buttercup10109(skc108),
inference(ems,[status(thm)],[694,40,97]),
[iquote('0:EmS:694.0,694.1,40.0,97.1')] ).
cnf(1011,plain,
~ b48_buttercup10109(skc57),
inference(ems,[status(thm)],[694,5,97]),
[iquote('0:EmS:694.0,694.1,5.0,97.1')] ).
cnf(1010,plain,
~ b48_buttercup10111(skc108),
inference(ems,[status(thm)],[694,40,101]),
[iquote('0:EmS:694.0,694.1,40.0,101.1')] ).
cnf(1009,plain,
~ b48_buttercup10111(skc57),
inference(ems,[status(thm)],[694,5,101]),
[iquote('0:EmS:694.0,694.1,5.0,101.1')] ).
cnf(1006,plain,
~ b48_buttercup10109(skc106),
inference(ems,[status(thm)],[681,38,97]),
[iquote('1:EmS:681.0,681.1,38.0,97.1')] ).
cnf(1005,plain,
~ b48_buttercup10109(skc80),
inference(ems,[status(thm)],[681,20,97]),
[iquote('1:EmS:681.0,681.1,20.0,97.1')] ).
cnf(1004,plain,
~ b48_buttercup10111(skc106),
inference(ems,[status(thm)],[681,38,101]),
[iquote('1:EmS:681.0,681.1,38.0,101.1')] ).
cnf(1003,plain,
~ b48_buttercup10111(skc80),
inference(ems,[status(thm)],[681,20,101]),
[iquote('1:EmS:681.0,681.1,20.0,101.1')] ).
cnf(818,plain,
( ~ b48_buttercup10098(skc66)
| b48_buttercup10110(skc66)
| b48_buttercup10109(skc66)
| b48_buttercup10108(skc66)
| b48_buttercup10107(skc66)
| b48_buttercup10104(skc66)
| b48_buttercup10102(skc66) ),
inference(res,[status(thm),theory(equality)],[181,47]),
[iquote('0:Res:181.1,47.0')] ).
cnf(1000,plain,
~ b48_buttercup10109(skc110),
inference(ems,[status(thm)],[671,42,97]),
[iquote('0:EmS:671.0,671.1,42.0,97.1')] ).
cnf(999,plain,
~ b48_buttercup10109(skc75),
inference(ems,[status(thm)],[671,17,97]),
[iquote('0:EmS:671.0,671.1,17.0,97.1')] ).
cnf(998,plain,
~ b48_buttercup10111(skc110),
inference(ems,[status(thm)],[671,42,101]),
[iquote('0:EmS:671.0,671.1,42.0,101.1')] ).
cnf(997,plain,
~ b48_buttercup10111(skc75),
inference(ems,[status(thm)],[671,17,101]),
[iquote('0:EmS:671.0,671.1,17.0,101.1')] ).
cnf(880,plain,
( ~ b48_buttercup10107(u)
| ~ k04_buttercup10100(u) ),
inference(mrr,[status(thm)],[615,879]),
[iquote('0:MRR:615.2,879.0')] ).
cnf(996,plain,
~ k04_buttercup10619(skc111),
inference(mrr,[status(thm)],[995,434]),
[iquote('0:MRR:995.1,434.0')] ).
cnf(992,plain,
~ b48_buttercup10104(skc111),
inference(ems,[status(thm)],[505,43,104]),
[iquote('0:EmS:505.0,505.1,43.0,104.1')] ).
cnf(989,plain,
~ b48_buttercup10110(skc111),
inference(ems,[status(thm)],[505,43,105]),
[iquote('0:EmS:505.0,505.1,43.0,105.1')] ).
cnf(986,plain,
~ b48_buttercup10108(skc111),
inference(ems,[status(thm)],[505,43,106]),
[iquote('0:EmS:505.0,505.1,43.0,106.1')] ).
cnf(700,plain,
( ~ b48_buttercup10102(u)
| ~ k04_buttercup10100(u) ),
inference(mrr,[status(thm)],[625,699]),
[iquote('0:MRR:625.2,699.0')] ).
cnf(983,plain,
~ b48_buttercup10102(skc111),
inference(ems,[status(thm)],[505,43,109]),
[iquote('0:EmS:505.0,505.1,43.0,109.1')] ).
cnf(966,plain,
~ k04_buttercup10619(skc105),
inference(mrr,[status(thm)],[960,414]),
[iquote('0:MRR:960.1,414.0')] ).
cnf(956,plain,
~ b48_buttercup10104(skc105),
inference(ems,[status(thm)],[504,37,104]),
[iquote('0:EmS:504.0,504.1,37.0,104.1')] ).
cnf(952,plain,
~ b48_buttercup10110(skc105),
inference(ems,[status(thm)],[504,37,105]),
[iquote('0:EmS:504.0,504.1,37.0,105.1')] ).
cnf(694,plain,
( ~ b48_buttercup10104(u)
| ~ k04_buttercup10100(u) ),
inference(mrr,[status(thm)],[635,693]),
[iquote('0:MRR:635.2,693.1')] ).
cnf(948,plain,
~ b48_buttercup10108(skc105),
inference(ems,[status(thm)],[504,37,106]),
[iquote('0:EmS:504.0,504.1,37.0,106.1')] ).
cnf(944,plain,
~ b48_buttercup10102(skc105),
inference(ems,[status(thm)],[504,37,109]),
[iquote('0:EmS:504.0,504.1,37.0,109.1')] ).
cnf(865,plain,
~ k04_buttercup10619(skc63),
inference(mrr,[status(thm)],[864,413]),
[iquote('0:MRR:864.1,413.0')] ).
cnf(863,plain,
~ b48_buttercup10104(skc63),
inference(sor,[status(thm)],[759,104]),
[iquote('0:SoR:759.0,104.1')] ).
cnf(681,plain,
( ~ b48_buttercup10110(u)
| ~ k04_buttercup10100(u) ),
inference(mrr,[status(thm)],[648,680]),
[iquote('1:MRR:648.2,680.0')] ).
cnf(862,plain,
~ b48_buttercup10110(skc63),
inference(sor,[status(thm)],[759,105]),
[iquote('0:SoR:759.0,105.1')] ).
cnf(861,plain,
~ b48_buttercup10108(skc63),
inference(sor,[status(thm)],[759,106]),
[iquote('0:SoR:759.0,106.1')] ).
cnf(860,plain,
~ b48_buttercup10102(skc63),
inference(sor,[status(thm)],[759,109]),
[iquote('0:SoR:759.0,109.1')] ).
cnf(858,plain,
~ k04_buttercup10619(skc69),
inference(mrr,[status(thm)],[857,433]),
[iquote('0:MRR:857.1,433.0')] ).
cnf(671,plain,
( ~ b48_buttercup10108(u)
| ~ k04_buttercup10100(u) ),
inference(mrr,[status(thm)],[662,670]),
[iquote('0:MRR:662.2,670.1')] ).
cnf(856,plain,
~ b48_buttercup10104(skc69),
inference(sor,[status(thm)],[752,104]),
[iquote('0:SoR:752.0,104.1')] ).
cnf(855,plain,
~ b48_buttercup10110(skc69),
inference(sor,[status(thm)],[752,105]),
[iquote('0:SoR:752.0,105.1')] ).
cnf(854,plain,
~ b48_buttercup10108(skc69),
inference(sor,[status(thm)],[752,106]),
[iquote('0:SoR:752.0,106.1')] ).
cnf(853,plain,
~ b48_buttercup10102(skc69),
inference(sor,[status(thm)],[752,109]),
[iquote('0:SoR:752.0,109.1')] ).
cnf(505,plain,
( ~ b48_buttercup10109(u)
| ~ k04_buttercup10622(u) ),
inference(ems,[status(thm)],[116,97,88]),
[iquote('0:EmS:116.0,116.1,97.1,88.1')] ).
cnf(747,plain,
~ k04_buttercup10619(skc100),
inference(mrr,[status(thm)],[746,502]),
[iquote('0:MRR:746.1,502.0')] ).
cnf(745,plain,
~ b48_buttercup10104(skc100),
inference(sor,[status(thm)],[523,104]),
[iquote('0:SoR:523.0,104.1')] ).
cnf(744,plain,
~ b48_buttercup10110(skc100),
inference(sor,[status(thm)],[523,105]),
[iquote('0:SoR:523.0,105.1')] ).
cnf(743,plain,
~ b48_buttercup10108(skc100),
inference(sor,[status(thm)],[523,106]),
[iquote('0:SoR:523.0,106.1')] ).
cnf(504,plain,
( ~ b48_buttercup10111(u)
| ~ k04_buttercup10622(u) ),
inference(ems,[status(thm)],[116,101,88]),
[iquote('0:EmS:116.0,116.1,101.1,88.1')] ).
cnf(742,plain,
~ b48_buttercup10102(skc100),
inference(sor,[status(thm)],[523,109]),
[iquote('0:SoR:523.0,109.1')] ).
cnf(741,plain,
~ k04_buttercup10619(skc97),
inference(mrr,[status(thm)],[726,501]),
[iquote('0:MRR:726.1,501.0')] ).
cnf(740,plain,
~ k04_buttercup10619(skc99),
inference(mrr,[status(thm)],[725,500]),
[iquote('0:MRR:725.1,500.0')] ).
cnf(739,plain,
~ k04_buttercup10619(skc91),
inference(mrr,[status(thm)],[724,499]),
[iquote('0:MRR:724.1,499.0')] ).
cnf(484,plain,
( ~ b48_buttercup10109(u)
| ~ k04_buttercup10620(u) ),
inference(ems,[status(thm)],[116,97,87]),
[iquote('0:EmS:116.0,116.1,97.1,87.1')] ).
cnf(738,plain,
~ k04_buttercup10619(skc93),
inference(mrr,[status(thm)],[723,498]),
[iquote('0:MRR:723.1,498.0')] ).
cnf(737,plain,
~ k04_buttercup10619(skc82),
inference(mrr,[status(thm)],[722,497]),
[iquote('0:MRR:722.1,497.0')] ).
cnf(736,plain,
~ k04_buttercup10619(skc84),
inference(mrr,[status(thm)],[721,496]),
[iquote('0:MRR:721.1,496.0')] ).
cnf(735,plain,
~ k04_buttercup10619(skc77),
inference(mrr,[status(thm)],[720,495]),
[iquote('0:MRR:720.1,495.0')] ).
cnf(483,plain,
( ~ b48_buttercup10111(u)
| ~ k04_buttercup10620(u) ),
inference(ems,[status(thm)],[116,101,87]),
[iquote('0:EmS:116.0,116.1,101.1,87.1')] ).
cnf(734,plain,
~ k04_buttercup10619(skc79),
inference(mrr,[status(thm)],[719,494]),
[iquote('0:MRR:719.1,494.0')] ).
cnf(733,plain,
~ k04_buttercup10619(skc74),
inference(mrr,[status(thm)],[718,493]),
[iquote('0:MRR:718.1,493.0')] ).
cnf(732,plain,
~ k04_buttercup10619(skc62),
inference(mrr,[status(thm)],[717,492]),
[iquote('0:MRR:717.1,492.0')] ).
cnf(731,plain,
~ k04_buttercup10619(skc59),
inference(mrr,[status(thm)],[716,491]),
[iquote('0:MRR:716.1,491.0')] ).
cnf(730,plain,
~ k04_buttercup10619(skc61),
inference(mrr,[status(thm)],[715,490]),
[iquote('0:MRR:715.1,490.0')] ).
cnf(729,plain,
~ k04_buttercup10619(skc64),
inference(mrr,[status(thm)],[713,341]),
[iquote('0:MRR:713.1,341.0')] ).
cnf(728,plain,
~ k04_buttercup10619(skc68),
inference(mrr,[status(thm)],[712,340]),
[iquote('0:MRR:712.1,340.0')] ).
cnf(727,plain,
~ k04_buttercup10619(skc70),
inference(mrr,[status(thm)],[711,339]),
[iquote('0:MRR:711.1,339.0')] ).
cnf(708,plain,
~ b48_buttercup10104(skc97),
inference(sor,[status(thm)],[522,104]),
[iquote('0:SoR:522.0,104.1')] ).
cnf(707,plain,
~ b48_buttercup10110(skc97),
inference(sor,[status(thm)],[522,105]),
[iquote('0:SoR:522.0,105.1')] ).
cnf(706,plain,
~ b48_buttercup10108(skc97),
inference(sor,[status(thm)],[522,106]),
[iquote('0:SoR:522.0,106.1')] ).
cnf(887,plain,
~ skC1,
inference(ems,[status(thm)],[693,5]),
[iquote('0:EmS:693.0,5.0')] ).
cnf(705,plain,
~ b48_buttercup10102(skc97),
inference(sor,[status(thm)],[522,109]),
[iquote('0:SoR:522.0,109.1')] ).
cnf(704,plain,
~ b48_buttercup10104(skc99),
inference(sor,[status(thm)],[521,104]),
[iquote('0:SoR:521.0,104.1')] ).
cnf(703,plain,
~ b48_buttercup10110(skc99),
inference(sor,[status(thm)],[521,105]),
[iquote('0:SoR:521.0,105.1')] ).
cnf(885,plain,
~ skC7,
inference(ems,[status(thm)],[670,17]),
[iquote('0:EmS:670.0,17.0')] ).
cnf(702,plain,
~ b48_buttercup10108(skc99),
inference(sor,[status(thm)],[521,106]),
[iquote('0:SoR:521.0,106.1')] ).
cnf(701,plain,
~ b48_buttercup10102(skc99),
inference(sor,[status(thm)],[521,109]),
[iquote('0:SoR:521.0,109.1')] ).
cnf(698,plain,
~ b48_buttercup10104(skc91),
inference(sor,[status(thm)],[520,104]),
[iquote('0:SoR:520.0,104.1')] ).
cnf(883,plain,
~ skC9,
inference(ems,[status(thm)],[647,20]),
[iquote('0:EmS:647.0,20.0')] ).
cnf(697,plain,
~ b48_buttercup10110(skc91),
inference(sor,[status(thm)],[520,105]),
[iquote('0:SoR:520.0,105.1')] ).
cnf(696,plain,
~ b48_buttercup10108(skc91),
inference(sor,[status(thm)],[520,106]),
[iquote('0:SoR:520.0,106.1')] ).
cnf(695,plain,
~ b48_buttercup10102(skc91),
inference(sor,[status(thm)],[520,109]),
[iquote('0:SoR:520.0,109.1')] ).
cnf(881,plain,
~ skC11,
inference(ems,[status(thm)],[624,27]),
[iquote('0:EmS:624.0,27.0')] ).
cnf(685,plain,
~ b48_buttercup10104(skc93),
inference(sor,[status(thm)],[519,104]),
[iquote('0:SoR:519.0,104.1')] ).
cnf(684,plain,
~ b48_buttercup10110(skc93),
inference(sor,[status(thm)],[519,105]),
[iquote('0:SoR:519.0,105.1')] ).
cnf(683,plain,
~ b48_buttercup10108(skc93),
inference(sor,[status(thm)],[519,106]),
[iquote('0:SoR:519.0,106.1')] ).
cnf(879,plain,
~ skC13,
inference(ems,[status(thm)],[611,34]),
[iquote('0:EmS:611.0,34.0')] ).
cnf(682,plain,
~ b48_buttercup10102(skc93),
inference(sor,[status(thm)],[519,109]),
[iquote('0:SoR:519.0,109.1')] ).
cnf(679,plain,
~ b48_buttercup10104(skc82),
inference(sor,[status(thm)],[518,104]),
[iquote('0:SoR:518.0,104.1')] ).
cnf(678,plain,
~ b48_buttercup10110(skc82),
inference(sor,[status(thm)],[518,105]),
[iquote('0:SoR:518.0,105.1')] ).
cnf(876,plain,
~ skC3,
inference(ems,[status(thm)],[597,9]),
[iquote('0:EmS:597.0,9.0')] ).
cnf(677,plain,
~ b48_buttercup10108(skc82),
inference(sor,[status(thm)],[518,106]),
[iquote('0:SoR:518.0,106.1')] ).
cnf(676,plain,
~ b48_buttercup10102(skc82),
inference(sor,[status(thm)],[518,109]),
[iquote('0:SoR:518.0,109.1')] ).
cnf(675,plain,
~ b48_buttercup10104(skc84),
inference(sor,[status(thm)],[517,104]),
[iquote('0:SoR:517.0,104.1')] ).
cnf(871,plain,
~ skC5,
inference(ems,[status(thm)],[568,839]),
[iquote('0:EmS:568.0,839.0')] ).
cnf(674,plain,
~ b48_buttercup10110(skc84),
inference(sor,[status(thm)],[517,105]),
[iquote('0:SoR:517.0,105.1')] ).
cnf(673,plain,
~ b48_buttercup10108(skc84),
inference(sor,[status(thm)],[517,106]),
[iquote('0:SoR:517.0,106.1')] ).
cnf(672,plain,
~ b48_buttercup10102(skc84),
inference(sor,[status(thm)],[517,109]),
[iquote('0:SoR:517.0,109.1')] ).
cnf(660,plain,
~ b48_buttercup10104(skc77),
inference(sor,[status(thm)],[516,104]),
[iquote('0:SoR:516.0,104.1')] ).
cnf(659,plain,
~ b48_buttercup10110(skc77),
inference(sor,[status(thm)],[516,105]),
[iquote('0:SoR:516.0,105.1')] ).
cnf(658,plain,
~ b48_buttercup10108(skc77),
inference(sor,[status(thm)],[516,106]),
[iquote('0:SoR:516.0,106.1')] ).
cnf(657,plain,
~ b48_buttercup10102(skc77),
inference(sor,[status(thm)],[516,109]),
[iquote('0:SoR:516.0,109.1')] ).
cnf(656,plain,
~ b48_buttercup10104(skc79),
inference(sor,[status(thm)],[515,104]),
[iquote('0:SoR:515.0,104.1')] ).
cnf(655,plain,
~ b48_buttercup10110(skc79),
inference(sor,[status(thm)],[515,105]),
[iquote('0:SoR:515.0,105.1')] ).
cnf(654,plain,
~ b48_buttercup10108(skc79),
inference(sor,[status(thm)],[515,106]),
[iquote('0:SoR:515.0,106.1')] ).
cnf(653,plain,
~ b48_buttercup10102(skc79),
inference(sor,[status(thm)],[515,109]),
[iquote('0:SoR:515.0,109.1')] ).
cnf(652,plain,
~ b48_buttercup10104(skc74),
inference(sor,[status(thm)],[514,104]),
[iquote('0:SoR:514.0,104.1')] ).
cnf(651,plain,
~ b48_buttercup10110(skc74),
inference(sor,[status(thm)],[514,105]),
[iquote('0:SoR:514.0,105.1')] ).
cnf(650,plain,
~ b48_buttercup10108(skc74),
inference(sor,[status(thm)],[514,106]),
[iquote('0:SoR:514.0,106.1')] ).
cnf(649,plain,
~ b48_buttercup10102(skc74),
inference(sor,[status(thm)],[514,109]),
[iquote('0:SoR:514.0,109.1')] ).
cnf(639,plain,
~ b48_buttercup10104(skc62),
inference(sor,[status(thm)],[513,104]),
[iquote('0:SoR:513.0,104.1')] ).
cnf(638,plain,
~ b48_buttercup10110(skc62),
inference(sor,[status(thm)],[513,105]),
[iquote('0:SoR:513.0,105.1')] ).
cnf(637,plain,
~ b48_buttercup10108(skc62),
inference(sor,[status(thm)],[513,106]),
[iquote('0:SoR:513.0,106.1')] ).
cnf(636,plain,
~ b48_buttercup10102(skc62),
inference(sor,[status(thm)],[513,109]),
[iquote('0:SoR:513.0,109.1')] ).
cnf(633,plain,
~ b48_buttercup10104(skc59),
inference(sor,[status(thm)],[512,104]),
[iquote('0:SoR:512.0,104.1')] ).
cnf(632,plain,
~ b48_buttercup10110(skc59),
inference(sor,[status(thm)],[512,105]),
[iquote('0:SoR:512.0,105.1')] ).
cnf(631,plain,
~ b48_buttercup10108(skc59),
inference(sor,[status(thm)],[512,106]),
[iquote('0:SoR:512.0,106.1')] ).
cnf(630,plain,
~ b48_buttercup10102(skc59),
inference(sor,[status(thm)],[512,109]),
[iquote('0:SoR:512.0,109.1')] ).
cnf(629,plain,
~ b48_buttercup10104(skc61),
inference(sor,[status(thm)],[511,104]),
[iquote('0:SoR:511.0,104.1')] ).
cnf(759,plain,
~ k04_buttercup10622(skc63),
inference(mrr,[status(thm)],[757,88]),
[iquote('0:MRR:757.1,88.1')] ).
cnf(628,plain,
~ b48_buttercup10110(skc61),
inference(sor,[status(thm)],[511,105]),
[iquote('0:SoR:511.0,105.1')] ).
cnf(627,plain,
~ b48_buttercup10108(skc61),
inference(sor,[status(thm)],[511,106]),
[iquote('0:SoR:511.0,106.1')] ).
cnf(626,plain,
~ b48_buttercup10102(skc61),
inference(sor,[status(thm)],[511,109]),
[iquote('0:SoR:511.0,109.1')] ).
cnf(616,plain,
~ b48_buttercup10107(skc100),
inference(sor,[status(thm)],[502,111]),
[iquote('0:SoR:502.0,111.1')] ).
cnf(752,plain,
~ k04_buttercup10622(skc69),
inference(mrr,[status(thm)],[750,88]),
[iquote('0:MRR:750.1,88.1')] ).
cnf(613,plain,
~ b48_buttercup10107(skc97),
inference(sor,[status(thm)],[501,111]),
[iquote('0:SoR:501.0,111.1')] ).
cnf(612,plain,
~ b48_buttercup10107(skc99),
inference(sor,[status(thm)],[500,111]),
[iquote('0:SoR:500.0,111.1')] ).
cnf(603,plain,
~ b48_buttercup10107(skc91),
inference(sor,[status(thm)],[499,111]),
[iquote('0:SoR:499.0,111.1')] ).
cnf(839,plain,
b48_buttercup10109(skc74),
inference(mrr,[status(thm)],[838,651,650,652,649]),
[iquote('0:MRR:838.0,838.2,838.3,838.4,651.0,650.0,652.0,649.0')] ).
cnf(181,axiom,
( ~ b48_buttercup10098(u)
| b48_buttercup10111(u)
| b48_buttercup10110(u)
| b48_buttercup10109(u)
| b48_buttercup10108(u)
| b48_buttercup10107(u)
| b48_buttercup10104(u)
| b48_buttercup10102(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(602,plain,
~ b48_buttercup10107(skc93),
inference(sor,[status(thm)],[498,111]),
[iquote('0:SoR:498.0,111.1')] ).
cnf(601,plain,
~ b48_buttercup10107(skc82),
inference(sor,[status(thm)],[497,111]),
[iquote('0:SoR:497.0,111.1')] ).
cnf(600,plain,
~ b48_buttercup10107(skc84),
inference(sor,[status(thm)],[496,111]),
[iquote('0:SoR:496.0,111.1')] ).
cnf(574,plain,
~ b48_buttercup10107(skc77),
inference(sor,[status(thm)],[495,111]),
[iquote('0:SoR:495.0,111.1')] ).
cnf(573,plain,
~ b48_buttercup10107(skc79),
inference(sor,[status(thm)],[494,111]),
[iquote('0:SoR:494.0,111.1')] ).
cnf(572,plain,
~ b48_buttercup10107(skc74),
inference(sor,[status(thm)],[493,111]),
[iquote('0:SoR:493.0,111.1')] ).
cnf(571,plain,
~ b48_buttercup10107(skc62),
inference(sor,[status(thm)],[492,111]),
[iquote('0:SoR:492.0,111.1')] ).
cnf(545,plain,
~ b48_buttercup10107(skc59),
inference(sor,[status(thm)],[491,111]),
[iquote('0:SoR:491.0,111.1')] ).
cnf(570,plain,
( ~ b48_buttercup10109(u)
| ~ k04_buttercup10619(u)
| ~ k04_buttercup10619(v)
| b48_buttercup10109(v) ),
inference(mrr,[status(thm)],[543,568]),
[iquote('0:MRR:543.3,568.1')] ).
cnf(544,plain,
~ b48_buttercup10107(skc61),
inference(sor,[status(thm)],[490,111]),
[iquote('0:SoR:490.0,111.1')] ).
cnf(537,plain,
~ b48_buttercup10109(skc101),
inference(ems,[status(thm)],[116,97,33]),
[iquote('0:EmS:116.0,116.1,97.1,33.0')] ).
cnf(536,plain,
~ b48_buttercup10111(skc101),
inference(ems,[status(thm)],[116,101,33]),
[iquote('0:EmS:116.0,116.1,101.1,33.0')] ).
cnf(535,plain,
~ b48_buttercup10109(skc71),
inference(ems,[status(thm)],[116,97,12]),
[iquote('0:EmS:116.0,116.1,97.1,12.0')] ).
cnf(534,plain,
~ b48_buttercup10111(skc71),
inference(ems,[status(thm)],[116,101,12]),
[iquote('0:EmS:116.0,116.1,101.1,12.0')] ).
cnf(533,plain,
~ b48_buttercup10109(skc73),
inference(ems,[status(thm)],[116,97,11]),
[iquote('0:EmS:116.0,116.1,97.1,11.0')] ).
cnf(532,plain,
~ b48_buttercup10111(skc73),
inference(ems,[status(thm)],[116,101,11]),
[iquote('0:EmS:116.0,116.1,101.1,11.0')] ).
cnf(531,plain,
~ b48_buttercup10109(skc65),
inference(ems,[status(thm)],[116,97,8]),
[iquote('0:EmS:116.0,116.1,97.1,8.0')] ).
cnf(569,plain,
( ~ b48_buttercup10109(u)
| ~ k04_buttercup10619(u)
| ~ k04_buttercup10619(skc69) ),
inference(mrr,[status(thm)],[542,568]),
[iquote('0:MRR:542.3,568.1')] ).
cnf(530,plain,
~ b48_buttercup10111(skc65),
inference(ems,[status(thm)],[116,101,8]),
[iquote('0:EmS:116.0,116.1,101.1,8.0')] ).
cnf(529,plain,
~ b48_buttercup10109(skc67),
inference(ems,[status(thm)],[116,97,7]),
[iquote('0:EmS:116.0,116.1,97.1,7.0')] ).
cnf(528,plain,
~ b48_buttercup10111(skc67),
inference(ems,[status(thm)],[116,101,7]),
[iquote('0:EmS:116.0,116.1,101.1,7.0')] ).
cnf(523,plain,
~ k04_buttercup10622(skc100),
inference(ems,[status(thm)],[116,32,88]),
[iquote('0:EmS:116.0,116.1,32.0,88.1')] ).
cnf(166,axiom,
( ~ k04_buttercup10619(u)
| k04_buttercup10622(u)
| k04_buttercup10620(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(522,plain,
~ k04_buttercup10622(skc97),
inference(ems,[status(thm)],[116,30,88]),
[iquote('0:EmS:116.0,116.1,30.0,88.1')] ).
cnf(521,plain,
~ k04_buttercup10622(skc99),
inference(ems,[status(thm)],[116,29,88]),
[iquote('0:EmS:116.0,116.1,29.0,88.1')] ).
cnf(699,plain,
~ skC10,
inference(mrr,[status(thm)],[82,695]),
[iquote('0:MRR:82.1,695.0')] ).
cnf(520,plain,
~ k04_buttercup10622(skc91),
inference(ems,[status(thm)],[116,26,88]),
[iquote('0:EmS:116.0,116.1,26.0,88.1')] ).
cnf(519,plain,
~ k04_buttercup10622(skc93),
inference(ems,[status(thm)],[116,25,88]),
[iquote('0:EmS:116.0,116.1,25.0,88.1')] ).
cnf(680,plain,
~ skC8,
inference(mrr,[status(thm)],[79,678]),
[iquote('0:MRR:79.1,678.0')] ).
cnf(518,plain,
~ k04_buttercup10622(skc82),
inference(ems,[status(thm)],[116,19,88]),
[iquote('0:EmS:116.0,116.1,19.0,88.1')] ).
cnf(517,plain,
~ k04_buttercup10622(skc84),
inference(ems,[status(thm)],[116,18,88]),
[iquote('0:EmS:116.0,116.1,18.0,88.1')] ).
cnf(661,plain,
~ skC6,
inference(mrr,[status(thm)],[76,658]),
[iquote('0:MRR:76.1,658.0')] ).
cnf(516,plain,
~ k04_buttercup10622(skc77),
inference(ems,[status(thm)],[116,16,88]),
[iquote('0:EmS:116.0,116.1,16.0,88.1')] ).
cnf(515,plain,
~ k04_buttercup10622(skc79),
inference(ems,[status(thm)],[116,15,88]),
[iquote('0:EmS:116.0,116.1,15.0,88.1')] ).
cnf(514,plain,
~ k04_buttercup10622(skc74),
inference(ems,[status(thm)],[116,14,88]),
[iquote('0:EmS:116.0,116.1,14.0,88.1')] ).
cnf(513,plain,
~ k04_buttercup10622(skc62),
inference(ems,[status(thm)],[116,6,88]),
[iquote('0:EmS:116.0,116.1,6.0,88.1')] ).
cnf(634,plain,
~ skC0,
inference(mrr,[status(thm)],[67,633]),
[iquote('0:MRR:67.1,633.0')] ).
cnf(512,plain,
~ k04_buttercup10622(skc59),
inference(ems,[status(thm)],[116,4,88]),
[iquote('0:EmS:116.0,116.1,4.0,88.1')] ).
cnf(511,plain,
~ k04_buttercup10622(skc61),
inference(ems,[status(thm)],[116,3,88]),
[iquote('0:EmS:116.0,116.1,3.0,88.1')] ).
cnf(502,plain,
~ k04_buttercup10620(skc100),
inference(ems,[status(thm)],[116,32,87]),
[iquote('0:EmS:116.0,116.1,32.0,87.1')] ).
cnf(614,plain,
~ skC12,
inference(mrr,[status(thm)],[85,613]),
[iquote('0:MRR:85.1,613.0')] ).
cnf(501,plain,
~ k04_buttercup10620(skc97),
inference(ems,[status(thm)],[116,30,87]),
[iquote('0:EmS:116.0,116.1,30.0,87.1')] ).
cnf(500,plain,
~ k04_buttercup10620(skc99),
inference(ems,[status(thm)],[116,29,87]),
[iquote('0:EmS:116.0,116.1,29.0,87.1')] ).
cnf(499,plain,
~ k04_buttercup10620(skc91),
inference(ems,[status(thm)],[116,26,87]),
[iquote('0:EmS:116.0,116.1,26.0,87.1')] ).
cnf(498,plain,
~ k04_buttercup10620(skc93),
inference(ems,[status(thm)],[116,25,87]),
[iquote('0:EmS:116.0,116.1,25.0,87.1')] ).
cnf(497,plain,
~ k04_buttercup10620(skc82),
inference(ems,[status(thm)],[116,19,87]),
[iquote('0:EmS:116.0,116.1,19.0,87.1')] ).
cnf(496,plain,
~ k04_buttercup10620(skc84),
inference(ems,[status(thm)],[116,18,87]),
[iquote('0:EmS:116.0,116.1,18.0,87.1')] ).
cnf(495,plain,
~ k04_buttercup10620(skc77),
inference(ems,[status(thm)],[116,16,87]),
[iquote('0:EmS:116.0,116.1,16.0,87.1')] ).
cnf(494,plain,
~ k04_buttercup10620(skc79),
inference(ems,[status(thm)],[116,15,87]),
[iquote('0:EmS:116.0,116.1,15.0,87.1')] ).
cnf(493,plain,
~ k04_buttercup10620(skc74),
inference(ems,[status(thm)],[116,14,87]),
[iquote('0:EmS:116.0,116.1,14.0,87.1')] ).
cnf(492,plain,
~ k04_buttercup10620(skc62),
inference(ems,[status(thm)],[116,6,87]),
[iquote('0:EmS:116.0,116.1,6.0,87.1')] ).
cnf(491,plain,
~ k04_buttercup10620(skc59),
inference(ems,[status(thm)],[116,4,87]),
[iquote('0:EmS:116.0,116.1,4.0,87.1')] ).
cnf(490,plain,
~ k04_buttercup10620(skc61),
inference(ems,[status(thm)],[116,3,87]),
[iquote('0:EmS:116.0,116.1,3.0,87.1')] ).
cnf(541,plain,
~ skC4,
inference(mrr,[status(thm)],[73,535]),
[iquote('0:MRR:73.1,535.0')] ).
cnf(538,plain,
~ skC2,
inference(mrr,[status(thm)],[70,530]),
[iquote('0:MRR:70.1,530.0')] ).
cnf(116,axiom,
( ~ k04_buttercup10100(u)
| ~ k04_buttercup10619(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(477,plain,
~ b48_buttercup10107(skc107),
inference(sor,[status(thm)],[473,111]),
[iquote('0:SoR:473.0,111.1')] ).
cnf(476,plain,
~ b48_buttercup10107(skc89),
inference(sor,[status(thm)],[472,111]),
[iquote('0:SoR:472.0,111.1')] ).
cnf(474,plain,
~ b48_buttercup10107(skc108),
inference(sor,[status(thm)],[468,111]),
[iquote('0:SoR:468.0,111.1')] ).
cnf(123,axiom,
( ~ b48_buttercup10102(u)
| ~ b48_buttercup10104(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(473,plain,
~ k04_buttercup10620(skc107),
inference(ems,[status(thm)],[129,39,110]),
[iquote('0:EmS:129.0,129.1,39.0,110.1')] ).
cnf(472,plain,
~ k04_buttercup10620(skc89),
inference(ems,[status(thm)],[129,27,110]),
[iquote('0:EmS:129.0,129.1,27.0,110.1')] ).
cnf(469,plain,
~ b48_buttercup10107(skc57),
inference(sor,[status(thm)],[467,111]),
[iquote('0:SoR:467.0,111.1')] ).
cnf(468,plain,
~ k04_buttercup10620(skc108),
inference(ems,[status(thm)],[130,40,110]),
[iquote('0:EmS:130.0,130.1,40.0,110.1')] ).
cnf(129,axiom,
( ~ b48_buttercup10102(u)
| ~ b48_buttercup10107(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(467,plain,
~ k04_buttercup10620(skc57),
inference(ems,[status(thm)],[130,5,110]),
[iquote('0:EmS:130.0,130.1,5.0,110.1')] ).
cnf(130,axiom,
( ~ b48_buttercup10104(u)
| ~ b48_buttercup10107(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(135,axiom,
( ~ b48_buttercup10102(u)
| ~ b48_buttercup10108(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(458,plain,
~ b48_buttercup10107(skc110),
inference(sor,[status(thm)],[456,111]),
[iquote('0:SoR:456.0,111.1')] ).
cnf(457,plain,
~ b48_buttercup10107(skc75),
inference(sor,[status(thm)],[455,111]),
[iquote('0:SoR:455.0,111.1')] ).
cnf(136,axiom,
( ~ b48_buttercup10104(u)
| ~ b48_buttercup10108(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(456,plain,
~ k04_buttercup10620(skc110),
inference(ems,[status(thm)],[137,110,42]),
[iquote('0:EmS:137.0,137.1,110.1,42.0')] ).
cnf(455,plain,
~ k04_buttercup10620(skc75),
inference(ems,[status(thm)],[137,110,17]),
[iquote('0:EmS:137.0,137.1,110.1,17.0')] ).
cnf(137,axiom,
( ~ b48_buttercup10107(u)
| ~ b48_buttercup10108(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(147,axiom,
( ~ b48_buttercup10102(u)
| ~ b48_buttercup10110(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(446,plain,
~ b48_buttercup10107(skc106),
inference(sor,[status(thm)],[444,111]),
[iquote('0:SoR:444.0,111.1')] ).
cnf(148,axiom,
( ~ b48_buttercup10104(u)
| ~ b48_buttercup10110(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(445,plain,
~ b48_buttercup10107(skc80),
inference(sor,[status(thm)],[443,111]),
[iquote('0:SoR:443.0,111.1')] ).
cnf(444,plain,
~ k04_buttercup10620(skc106),
inference(ems,[status(thm)],[149,110,38]),
[iquote('0:EmS:149.0,149.1,110.1,38.0')] ).
cnf(443,plain,
~ k04_buttercup10620(skc80),
inference(ems,[status(thm)],[149,110,20]),
[iquote('0:EmS:149.0,149.1,110.1,20.0')] ).
cnf(149,axiom,
( ~ b48_buttercup10107(u)
| ~ b48_buttercup10110(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(150,axiom,
( ~ b48_buttercup10108(u)
| ~ b48_buttercup10110(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(151,axiom,
( ~ b48_buttercup10109(u)
| ~ b48_buttercup10110(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(141,axiom,
( ~ b48_buttercup10102(u)
| ~ b48_buttercup10109(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(142,axiom,
( ~ b48_buttercup10104(u)
| ~ b48_buttercup10109(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(436,plain,
~ b48_buttercup10107(skc111),
inference(sor,[status(thm)],[434,111]),
[iquote('0:SoR:434.0,111.1')] ).
cnf(435,plain,
~ b48_buttercup10107(skc69),
inference(sor,[status(thm)],[433,111]),
[iquote('0:SoR:433.0,111.1')] ).
cnf(434,plain,
~ k04_buttercup10620(skc111),
inference(ems,[status(thm)],[143,110,43]),
[iquote('0:EmS:143.0,143.1,110.1,43.0')] ).
cnf(433,plain,
~ k04_buttercup10620(skc69),
inference(ems,[status(thm)],[143,110,13]),
[iquote('0:EmS:143.0,143.1,110.1,13.0')] ).
cnf(143,axiom,
( ~ b48_buttercup10107(u)
| ~ b48_buttercup10109(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(144,axiom,
( ~ b48_buttercup10108(u)
| ~ b48_buttercup10109(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(381,plain,
( b48_buttercup10111(skc56)
| b48_buttercup10109(skc56) ),
inference(mrr,[status(thm)],[378,374,376]),
[iquote('1:MRR:378.2,378.3,374.0,376.0')] ).
cnf(421,plain,
~ b48_buttercup10107(skc105),
inference(sor,[status(thm)],[414,111]),
[iquote('0:SoR:414.0,111.1')] ).
cnf(420,plain,
~ b48_buttercup10107(skc63),
inference(sor,[status(thm)],[413,111]),
[iquote('0:SoR:413.0,111.1')] ).
cnf(416,plain,
~ k04_buttercup10620(skc103),
inference(sor,[status(thm)],[407,110]),
[iquote('0:SoR:407.0,110.1')] ).
cnf(153,axiom,
( ~ b48_buttercup10102(u)
| ~ b48_buttercup10111(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(415,plain,
~ k04_buttercup10620(skc94),
inference(sor,[status(thm)],[406,110]),
[iquote('0:SoR:406.0,110.1')] ).
cnf(414,plain,
~ k04_buttercup10620(skc105),
inference(ems,[status(thm)],[155,110,37]),
[iquote('0:EmS:155.0,155.1,110.1,37.0')] ).
cnf(413,plain,
~ k04_buttercup10620(skc63),
inference(ems,[status(thm)],[155,110,9]),
[iquote('0:EmS:155.0,155.1,110.1,9.0')] ).
cnf(410,plain,
~ k04_buttercup10620(skc87),
inference(sor,[status(thm)],[405,110]),
[iquote('0:SoR:405.0,110.1')] ).
cnf(154,axiom,
( ~ b48_buttercup10104(u)
| ~ b48_buttercup10111(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(409,plain,
~ k04_buttercup10620(skc86),
inference(sor,[status(thm)],[404,110]),
[iquote('0:SoR:404.0,110.1')] ).
cnf(408,plain,
~ k04_buttercup10620(skc85),
inference(sor,[status(thm)],[403,110]),
[iquote('0:SoR:403.0,110.1')] ).
cnf(407,plain,
~ b48_buttercup10107(skc103),
inference(ems,[status(thm)],[115,111,35]),
[iquote('0:EmS:115.0,115.1,111.1,35.0')] ).
cnf(406,plain,
~ b48_buttercup10107(skc94),
inference(ems,[status(thm)],[115,111,28]),
[iquote('0:EmS:115.0,115.1,111.1,28.0')] ).
cnf(155,axiom,
( ~ b48_buttercup10107(u)
| ~ b48_buttercup10111(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(405,plain,
~ b48_buttercup10107(skc87),
inference(ems,[status(thm)],[115,111,23]),
[iquote('0:EmS:115.0,115.1,111.1,23.0')] ).
cnf(404,plain,
~ b48_buttercup10107(skc86),
inference(ems,[status(thm)],[115,111,22]),
[iquote('0:EmS:115.0,115.1,111.1,22.0')] ).
cnf(403,plain,
~ b48_buttercup10107(skc85),
inference(ems,[status(thm)],[115,111,21]),
[iquote('0:EmS:115.0,115.1,111.1,21.0')] ).
cnf(402,plain,
~ b48_buttercup10104(skc102),
inference(ems,[status(thm)],[115,34,104]),
[iquote('0:EmS:115.0,115.1,34.0,104.1')] ).
cnf(156,axiom,
( ~ b48_buttercup10108(u)
| ~ b48_buttercup10111(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(400,plain,
~ b48_buttercup10110(skc102),
inference(ems,[status(thm)],[115,34,105]),
[iquote('0:EmS:115.0,115.1,34.0,105.1')] ).
cnf(398,plain,
~ b48_buttercup10108(skc102),
inference(ems,[status(thm)],[115,34,106]),
[iquote('0:EmS:115.0,115.1,34.0,106.1')] ).
cnf(396,plain,
~ b48_buttercup10102(skc102),
inference(ems,[status(thm)],[115,34,109]),
[iquote('0:EmS:115.0,115.1,34.0,109.1')] ).
cnf(394,plain,
~ b48_buttercup10109(skc58),
inference(res,[status(thm),theory(equality)],[97,45]),
[iquote('0:Res:97.1,45.0')] ).
cnf(158,axiom,
( ~ b48_buttercup10110(u)
| ~ b48_buttercup10111(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(393,plain,
~ b48_buttercup10109(skc76),
inference(res,[status(thm),theory(equality)],[97,54]),
[iquote('0:Res:97.1,54.0')] ).
cnf(392,plain,
~ b48_buttercup10109(skc81),
inference(res,[status(thm),theory(equality)],[97,56]),
[iquote('0:Res:97.1,56.0')] ).
cnf(391,plain,
~ b48_buttercup10109(skc88),
inference(res,[status(thm),theory(equality)],[97,60]),
[iquote('0:Res:97.1,60.0')] ).
cnf(390,plain,
~ b48_buttercup10109(skc90),
inference(res,[status(thm),theory(equality)],[97,62]),
[iquote('0:Res:97.1,62.0')] ).
cnf(157,axiom,
( ~ b48_buttercup10109(u)
| ~ b48_buttercup10111(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(389,plain,
~ b48_buttercup10109(skc96),
inference(res,[status(thm),theory(equality)],[97,65]),
[iquote('0:Res:97.1,65.0')] ).
cnf(388,plain,
~ b48_buttercup10111(skc58),
inference(res,[status(thm),theory(equality)],[101,45]),
[iquote('0:Res:101.1,45.0')] ).
cnf(387,plain,
~ b48_buttercup10111(skc76),
inference(res,[status(thm),theory(equality)],[101,54]),
[iquote('0:Res:101.1,54.0')] ).
cnf(386,plain,
~ b48_buttercup10111(skc81),
inference(res,[status(thm),theory(equality)],[101,56]),
[iquote('0:Res:101.1,56.0')] ).
cnf(115,axiom,
( ~ k04_buttercup10620(u)
| ~ k04_buttercup10622(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(385,plain,
~ b48_buttercup10111(skc88),
inference(res,[status(thm),theory(equality)],[101,60]),
[iquote('0:Res:101.1,60.0')] ).
cnf(384,plain,
~ b48_buttercup10111(skc90),
inference(res,[status(thm),theory(equality)],[101,62]),
[iquote('0:Res:101.1,62.0')] ).
cnf(383,plain,
~ b48_buttercup10111(skc96),
inference(res,[status(thm),theory(equality)],[101,65]),
[iquote('0:Res:101.1,65.0')] ).
cnf(376,plain,
~ b48_buttercup10104(skc56),
inference(sor,[status(thm)],[347,104]),
[iquote('0:SoR:347.0,104.1')] ).
cnf(97,axiom,
( ~ b48_buttercup10109(u)
| k04_buttercup10100(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(375,plain,
~ b48_buttercup10110(skc56),
inference(sor,[status(thm)],[347,105]),
[iquote('0:SoR:347.0,105.1')] ).
cnf(374,plain,
~ b48_buttercup10108(skc56),
inference(sor,[status(thm)],[347,106]),
[iquote('0:SoR:347.0,106.1')] ).
cnf(373,plain,
~ b48_buttercup10102(skc56),
inference(sor,[status(thm)],[347,109]),
[iquote('0:SoR:347.0,109.1')] ).
cnf(372,plain,
~ b48_buttercup10104(skc64),
inference(sor,[status(thm)],[350,104]),
[iquote('0:SoR:350.0,104.1')] ).
cnf(101,axiom,
( ~ b48_buttercup10111(u)
| k04_buttercup10100(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(371,plain,
~ b48_buttercup10110(skc64),
inference(sor,[status(thm)],[350,105]),
[iquote('0:SoR:350.0,105.1')] ).
cnf(370,plain,
~ b48_buttercup10108(skc64),
inference(sor,[status(thm)],[350,106]),
[iquote('0:SoR:350.0,106.1')] ).
cnf(369,plain,
~ b48_buttercup10102(skc64),
inference(sor,[status(thm)],[350,109]),
[iquote('0:SoR:350.0,109.1')] ).
cnf(368,plain,
~ b48_buttercup10104(skc68),
inference(sor,[status(thm)],[349,104]),
[iquote('0:SoR:349.0,104.1')] ).
cnf(367,plain,
~ b48_buttercup10110(skc68),
inference(sor,[status(thm)],[349,105]),
[iquote('0:SoR:349.0,105.1')] ).
cnf(366,plain,
~ b48_buttercup10108(skc68),
inference(sor,[status(thm)],[349,106]),
[iquote('0:SoR:349.0,106.1')] ).
cnf(365,plain,
~ b48_buttercup10102(skc68),
inference(sor,[status(thm)],[349,109]),
[iquote('0:SoR:349.0,109.1')] ).
cnf(364,plain,
~ b48_buttercup10104(skc70),
inference(sor,[status(thm)],[348,104]),
[iquote('0:SoR:348.0,104.1')] ).
cnf(363,plain,
~ b48_buttercup10110(skc70),
inference(sor,[status(thm)],[348,105]),
[iquote('0:SoR:348.0,105.1')] ).
cnf(362,plain,
~ b48_buttercup10108(skc70),
inference(sor,[status(thm)],[348,106]),
[iquote('0:SoR:348.0,106.1')] ).
cnf(361,plain,
~ b48_buttercup10102(skc70),
inference(sor,[status(thm)],[348,109]),
[iquote('0:SoR:348.0,109.1')] ).
cnf(357,plain,
~ b48_buttercup10107(skc64),
inference(sor,[status(thm)],[341,111]),
[iquote('0:SoR:341.0,111.1')] ).
cnf(347,plain,
~ k04_buttercup10622(skc56),
inference(sor,[status(thm)],[193,88]),
[iquote('0:SoR:193.0,88.1')] ).
cnf(350,plain,
~ k04_buttercup10622(skc64),
inference(res,[status(thm),theory(equality)],[88,48]),
[iquote('0:Res:88.1,48.0')] ).
cnf(349,plain,
~ k04_buttercup10622(skc68),
inference(res,[status(thm),theory(equality)],[88,49]),
[iquote('0:Res:88.1,49.0')] ).
cnf(348,plain,
~ k04_buttercup10622(skc70),
inference(res,[status(thm),theory(equality)],[88,51]),
[iquote('0:Res:88.1,51.0')] ).
cnf(352,plain,
~ b48_buttercup10110(skc56),
inference(spt,[],[351,182,328]),
[iquote('1:Spt:351.0,182.1,328.0')] ).
cnf(346,plain,
~ b48_buttercup10107(skc68),
inference(sor,[status(thm)],[340,111]),
[iquote('0:SoR:340.0,111.1')] ).
cnf(345,plain,
~ b48_buttercup10107(skc70),
inference(sor,[status(thm)],[339,111]),
[iquote('0:SoR:339.0,111.1')] ).
cnf(343,plain,
~ b48_buttercup10107(skc56),
inference(sor,[status(thm)],[338,111]),
[iquote('0:SoR:338.0,111.1')] ).
cnf(341,plain,
~ k04_buttercup10620(skc64),
inference(res,[status(thm),theory(equality)],[87,48]),
[iquote('0:Res:87.1,48.0')] ).
cnf(88,axiom,
( ~ k04_buttercup10622(u)
| k04_buttercup10619(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(340,plain,
~ k04_buttercup10620(skc68),
inference(res,[status(thm),theory(equality)],[87,49]),
[iquote('0:Res:87.1,49.0')] ).
cnf(339,plain,
~ k04_buttercup10620(skc70),
inference(res,[status(thm),theory(equality)],[87,51]),
[iquote('0:Res:87.1,51.0')] ).
cnf(338,plain,
~ k04_buttercup10620(skc56),
inference(sor,[status(thm)],[193,87]),
[iquote('0:SoR:193.0,87.1')] ).
cnf(337,plain,
~ b48_buttercup10107(skc98),
inference(sor,[status(thm)],[335,111]),
[iquote('0:SoR:335.0,111.1')] ).
cnf(87,axiom,
( ~ k04_buttercup10620(u)
| k04_buttercup10619(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(335,plain,
~ k04_buttercup10620(skc98),
inference(res,[status(thm),theory(equality)],[110,64]),
[iquote('0:Res:110.1,64.0')] ).
cnf(110,axiom,
( ~ k04_buttercup10620(u)
| b48_buttercup10107(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(107,axiom,
( ~ k04_buttercup10100(u)
| b48_buttercup10098(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(89,axiom,
( ~ b48_buttercup10102(u)
| b48_buttercup10098(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(90,axiom,
( ~ b48_buttercup10104(u)
| b48_buttercup10098(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(91,axiom,
( ~ b48_buttercup10107(u)
| b48_buttercup10098(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(92,axiom,
( ~ b48_buttercup10108(u)
| b48_buttercup10098(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(94,axiom,
( ~ b48_buttercup10110(u)
| b48_buttercup10098(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(99,axiom,
( ~ k04_buttercup10619(u)
| b48_buttercup10098(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(93,axiom,
( ~ b48_buttercup10109(u)
| b48_buttercup10098(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(95,axiom,
( ~ b48_buttercup10111(u)
| b48_buttercup10098(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(104,axiom,
( ~ b48_buttercup10104(u)
| k04_buttercup10622(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(105,axiom,
( ~ b48_buttercup10110(u)
| k04_buttercup10622(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(106,axiom,
( ~ b48_buttercup10108(u)
| k04_buttercup10622(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(109,axiom,
( ~ b48_buttercup10102(u)
| k04_buttercup10622(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(111,axiom,
( ~ b48_buttercup10107(u)
| k04_buttercup10620(u) ),
file('SYO579+1.p',unknown),
[] ).
cnf(193,plain,
~ k04_buttercup10619(skc56),
inference(res,[status(thm),theory(equality)],[1,116]),
[iquote('0:Res:1.0,116.1')] ).
cnf(45,axiom,
~ k04_buttercup10100(skc58),
file('SYO579+1.p',unknown),
[] ).
cnf(54,axiom,
~ k04_buttercup10100(skc76),
file('SYO579+1.p',unknown),
[] ).
cnf(56,axiom,
~ k04_buttercup10100(skc81),
file('SYO579+1.p',unknown),
[] ).
cnf(60,axiom,
~ k04_buttercup10100(skc88),
file('SYO579+1.p',unknown),
[] ).
cnf(62,axiom,
~ k04_buttercup10100(skc90),
file('SYO579+1.p',unknown),
[] ).
cnf(65,axiom,
~ k04_buttercup10100(skc96),
file('SYO579+1.p',unknown),
[] ).
cnf(44,axiom,
~ b48_buttercup10104(skc60),
file('SYO579+1.p',unknown),
[] ).
cnf(48,axiom,
~ k04_buttercup10619(skc64),
file('SYO579+1.p',unknown),
[] ).
cnf(49,axiom,
~ k04_buttercup10619(skc68),
file('SYO579+1.p',unknown),
[] ).
cnf(51,axiom,
~ k04_buttercup10619(skc70),
file('SYO579+1.p',unknown),
[] ).
cnf(53,axiom,
~ b48_buttercup10108(skc78),
file('SYO579+1.p',unknown),
[] ).
cnf(55,axiom,
~ b48_buttercup10110(skc83),
file('SYO579+1.p',unknown),
[] ).
cnf(57,axiom,
~ b48_buttercup10104(skc85),
file('SYO579+1.p',unknown),
[] ).
cnf(58,axiom,
~ b48_buttercup10110(skc86),
file('SYO579+1.p',unknown),
[] ).
cnf(59,axiom,
~ b48_buttercup10108(skc87),
file('SYO579+1.p',unknown),
[] ).
cnf(61,axiom,
~ b48_buttercup10102(skc92),
file('SYO579+1.p',unknown),
[] ).
cnf(63,axiom,
~ b48_buttercup10102(skc94),
file('SYO579+1.p',unknown),
[] ).
cnf(64,axiom,
~ b48_buttercup10107(skc98),
file('SYO579+1.p',unknown),
[] ).
cnf(46,axiom,
~ b48_buttercup10109(skc62),
file('SYO579+1.p',unknown),
[] ).
cnf(47,axiom,
~ b48_buttercup10111(skc66),
file('SYO579+1.p',unknown),
[] ).
cnf(50,axiom,
~ b48_buttercup10109(skc72),
file('SYO579+1.p',unknown),
[] ).
cnf(52,axiom,
~ b48_buttercup10111(skc74),
file('SYO579+1.p',unknown),
[] ).
cnf(1,axiom,
k04_buttercup10100(skc56),
file('SYO579+1.p',unknown),
[] ).
cnf(3,axiom,
k04_buttercup10100(skc61),
file('SYO579+1.p',unknown),
[] ).
cnf(4,axiom,
k04_buttercup10100(skc59),
file('SYO579+1.p',unknown),
[] ).
cnf(6,axiom,
k04_buttercup10100(skc62),
file('SYO579+1.p',unknown),
[] ).
cnf(14,axiom,
k04_buttercup10100(skc74),
file('SYO579+1.p',unknown),
[] ).
cnf(15,axiom,
k04_buttercup10100(skc79),
file('SYO579+1.p',unknown),
[] ).
cnf(16,axiom,
k04_buttercup10100(skc77),
file('SYO579+1.p',unknown),
[] ).
cnf(18,axiom,
k04_buttercup10100(skc84),
file('SYO579+1.p',unknown),
[] ).
cnf(19,axiom,
k04_buttercup10100(skc82),
file('SYO579+1.p',unknown),
[] ).
cnf(25,axiom,
k04_buttercup10100(skc93),
file('SYO579+1.p',unknown),
[] ).
cnf(26,axiom,
k04_buttercup10100(skc91),
file('SYO579+1.p',unknown),
[] ).
cnf(29,axiom,
k04_buttercup10100(skc99),
file('SYO579+1.p',unknown),
[] ).
cnf(30,axiom,
k04_buttercup10100(skc97),
file('SYO579+1.p',unknown),
[] ).
cnf(32,axiom,
k04_buttercup10100(skc100),
file('SYO579+1.p',unknown),
[] ).
cnf(5,axiom,
b48_buttercup10104(skc57),
file('SYO579+1.p',unknown),
[] ).
cnf(7,axiom,
k04_buttercup10619(skc67),
file('SYO579+1.p',unknown),
[] ).
cnf(8,axiom,
k04_buttercup10619(skc65),
file('SYO579+1.p',unknown),
[] ).
cnf(11,axiom,
k04_buttercup10619(skc73),
file('SYO579+1.p',unknown),
[] ).
cnf(12,axiom,
k04_buttercup10619(skc71),
file('SYO579+1.p',unknown),
[] ).
cnf(17,axiom,
b48_buttercup10108(skc75),
file('SYO579+1.p',unknown),
[] ).
cnf(20,axiom,
b48_buttercup10110(skc80),
file('SYO579+1.p',unknown),
[] ).
cnf(27,axiom,
b48_buttercup10102(skc89),
file('SYO579+1.p',unknown),
[] ).
cnf(31,axiom,
b48_buttercup10107(skc95),
file('SYO579+1.p',unknown),
[] ).
cnf(33,axiom,
k04_buttercup10619(skc101),
file('SYO579+1.p',unknown),
[] ).
cnf(38,axiom,
b48_buttercup10110(skc106),
file('SYO579+1.p',unknown),
[] ).
cnf(39,axiom,
b48_buttercup10102(skc107),
file('SYO579+1.p',unknown),
[] ).
cnf(40,axiom,
b48_buttercup10104(skc108),
file('SYO579+1.p',unknown),
[] ).
cnf(41,axiom,
b48_buttercup10107(skc109),
file('SYO579+1.p',unknown),
[] ).
cnf(42,axiom,
b48_buttercup10108(skc110),
file('SYO579+1.p',unknown),
[] ).
cnf(9,axiom,
b48_buttercup10111(skc63),
file('SYO579+1.p',unknown),
[] ).
cnf(13,axiom,
b48_buttercup10109(skc69),
file('SYO579+1.p',unknown),
[] ).
cnf(37,axiom,
b48_buttercup10111(skc105),
file('SYO579+1.p',unknown),
[] ).
cnf(43,axiom,
b48_buttercup10109(skc111),
file('SYO579+1.p',unknown),
[] ).
cnf(2,axiom,
b48_buttercup10098(skc56),
file('SYO579+1.p',unknown),
[] ).
cnf(10,axiom,
b48_buttercup10098(skc68),
file('SYO579+1.p',unknown),
[] ).
cnf(24,axiom,
b48_buttercup10098(skc88),
file('SYO579+1.p',unknown),
[] ).
cnf(36,axiom,
b48_buttercup10098(skc104),
file('SYO579+1.p',unknown),
[] ).
cnf(21,axiom,
k04_buttercup10622(skc85),
file('SYO579+1.p',unknown),
[] ).
cnf(22,axiom,
k04_buttercup10622(skc86),
file('SYO579+1.p',unknown),
[] ).
cnf(23,axiom,
k04_buttercup10622(skc87),
file('SYO579+1.p',unknown),
[] ).
cnf(28,axiom,
k04_buttercup10622(skc94),
file('SYO579+1.p',unknown),
[] ).
cnf(35,axiom,
k04_buttercup10622(skc103),
file('SYO579+1.p',unknown),
[] ).
cnf(34,axiom,
k04_buttercup10620(skc102),
file('SYO579+1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYO579+1 : TPTP v8.1.0. Released v5.5.0.
% 0.11/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n014.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sat Jul 9 13:55:50 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.54
% 0.19/0.54 SPASS V 3.9
% 0.19/0.54 SPASS beiseite: Completion found.
% 0.19/0.54 % SZS status CounterSatisfiable
% 0.19/0.54 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.54 SPASS derived 1091 clauses, backtracked 11 clauses, performed 3 splits and kept 659 clauses.
% 0.19/0.54 SPASS allocated 98647 KBytes.
% 0.19/0.54 SPASS spent 0:00:00.20 on the problem.
% 0.19/0.54 0:00:00.04 for the input.
% 0.19/0.54 0:00:00.04 for the FLOTTER CNF translation.
% 0.19/0.54 0:00:00.01 for inferences.
% 0.19/0.54 0:00:00.00 for the backtracking.
% 0.19/0.54 0:00:00.07 for the reduction.
% 0.19/0.54
% 0.19/0.54
% 0.19/0.54 The saturated set of worked-off clauses is :
% 0.19/0.54 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------