%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : SYO580+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Oct 7 11:08:49 AM UTC 2026
% Result : Theorem 1.25s 0.40s
% Output : CNFRefutation 1.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 9
% Syntax : Number of formulae : 190 ( 108 unt; 0 typ; 0 def)
% Number of atoms : 1090 ( 271 equ; 0 cnn)
% Maximal formula atoms : 12 ( 5 avg)
% Number of connectives : 1521 ( 617 ~; 282 |; 38 &; 546 @)
% ( 8 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 372 ( 369 usr; 11 con; 0-2 aty)
% Number of variables : 204 ( 0 ^; 179 !; 25 ?; 204 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_b48_buttercup10007,type,
b48_buttercup10007: $i > $o ).
thf(tp_b48_buttercup10013,type,
b48_buttercup10013: $i > $o ).
thf(tp_b48_buttercup10019,type,
b48_buttercup10019: $i > $o ).
thf(tp_b48_buttercup10021,type,
b48_buttercup10021: $i > $o ).
thf(tp_b48_buttercup10022,type,
b48_buttercup10022: $i > $o ).
thf(tp_b48_buttercup10024,type,
b48_buttercup10024: $i > $o ).
thf(tp_b48_buttercup10029,type,
b48_buttercup10029: $i > $o ).
thf(tp_b48_buttercup10031,type,
b48_buttercup10031: $i > $o ).
thf(tp_b48_buttercup10034,type,
b48_buttercup10034: $i > $o ).
thf(tp_b48_buttercup10035,type,
b48_buttercup10035: $i > $o ).
thf(tp_b48_buttercup10043,type,
b48_buttercup10043: $i > $o ).
thf(tp_b48_buttercup10045,type,
b48_buttercup10045: $i > $o ).
thf(tp_b48_buttercup10046,type,
b48_buttercup10046: $i > $o ).
thf(tp_b48_buttercup10050,type,
b48_buttercup10050: $i > $o ).
thf(tp_b48_buttercup10052,type,
b48_buttercup10052: $i > $o ).
thf(tp_b48_buttercup10054,type,
b48_buttercup10054: $i > $o ).
thf(tp_b48_buttercup10058,type,
b48_buttercup10058: $i > $o ).
thf(tp_b48_buttercup10065,type,
b48_buttercup10065: $i > $o ).
thf(tp_b48_buttercup10068,type,
b48_buttercup10068: $i > $o ).
thf(tp_b48_buttercup10070,type,
b48_buttercup10070: $i > $o ).
thf(tp_b48_buttercup10072,type,
b48_buttercup10072: $i > $o ).
thf(tp_b48_buttercup10075,type,
b48_buttercup10075: $i > $o ).
thf(tp_b48_buttercup10076,type,
b48_buttercup10076: $i > $o ).
thf(tp_b48_buttercup10082,type,
b48_buttercup10082: $i > $o ).
thf(tp_b48_buttercup10085,type,
b48_buttercup10085: $i > $o ).
thf(tp_b48_buttercup10086,type,
b48_buttercup10086: $i > $o ).
thf(tp_b48_buttercup10092,type,
b48_buttercup10092: $i > $o ).
thf(tp_b48_buttercup10098,type,
b48_buttercup10098: $i > $o ).
thf(tp_b48_buttercup10102,type,
b48_buttercup10102: $i > $o ).
thf(tp_b48_buttercup10104,type,
b48_buttercup10104: $i > $o ).
thf(tp_b48_buttercup10107,type,
b48_buttercup10107: $i > $o ).
thf(tp_b48_buttercup10108,type,
b48_buttercup10108: $i > $o ).
thf(tp_b48_buttercup10109,type,
b48_buttercup10109: $i > $o ).
thf(tp_b48_buttercup10110,type,
b48_buttercup10110: $i > $o ).
thf(tp_b48_buttercup10111,type,
b48_buttercup10111: $i > $o ).
thf(tp_b48_buttercup10115,type,
b48_buttercup10115: $i > $o ).
thf(tp_b48_buttercup10119,type,
b48_buttercup10119: $i > $o ).
thf(tp_b48_buttercup10120,type,
b48_buttercup10120: $i > $o ).
thf(tp_b48_buttercup10121,type,
b48_buttercup10121: $i > $o ).
thf(tp_b48_buttercup10130,type,
b48_buttercup10130: $i > $o ).
thf(tp_b48_buttercup10133,type,
b48_buttercup10133: $i > $o ).
thf(tp_b48_buttercup10134,type,
b48_buttercup10134: $i > $o ).
thf(tp_b48_buttercup10143,type,
b48_buttercup10143: $i > $o ).
thf(tp_b48_buttercup10150,type,
b48_buttercup10150: $i > $o ).
thf(tp_b48_buttercup10154,type,
b48_buttercup10154: $i > $o ).
thf(tp_b48_buttercup10156,type,
b48_buttercup10156: $i > $o ).
thf(tp_b48_buttercup10158,type,
b48_buttercup10158: $i > $o ).
thf(tp_b48_buttercup10159,type,
b48_buttercup10159: $i > $o ).
thf(tp_b48_buttercup10160,type,
b48_buttercup10160: $i > $o ).
thf(tp_b48_buttercup10161,type,
b48_buttercup10161: $i > $o ).
thf(tp_b48_buttercup10166,type,
b48_buttercup10166: $i > $o ).
thf(tp_b48_buttercup10167,type,
b48_buttercup10167: $i > $o ).
thf(tp_b48_buttercup10169,type,
b48_buttercup10169: $i > $o ).
thf(tp_b48_buttercup10170,type,
b48_buttercup10170: $i > $o ).
thf(tp_b48_buttercup10173,type,
b48_buttercup10173: $i > $o ).
thf(tp_b48_buttercup10174,type,
b48_buttercup10174: $i > $o ).
thf(tp_b48_buttercup10176,type,
b48_buttercup10176: $i > $o ).
thf(tp_b48_buttercup10179,type,
b48_buttercup10179: $i > $o ).
thf(tp_b48_buttercup10180,type,
b48_buttercup10180: $i > $o ).
thf(tp_b48_buttercup10182,type,
b48_buttercup10182: $i > $o ).
thf(tp_b48_buttercup10186,type,
b48_buttercup10186: $i > $o ).
thf(tp_b48_buttercup10191,type,
b48_buttercup10191: $i > $o ).
thf(tp_b48_buttercup10193,type,
b48_buttercup10193: $i > $o ).
thf(tp_b48_buttercup10195,type,
b48_buttercup10195: $i > $o ).
thf(tp_b48_buttercup10196,type,
b48_buttercup10196: $i > $o ).
thf(tp_b48_buttercup10197,type,
b48_buttercup10197: $i > $o ).
thf(tp_b48_buttercup10198,type,
b48_buttercup10198: $i > $o ).
thf(tp_b48_buttercup10199,type,
b48_buttercup10199: $i > $o ).
thf(tp_b48_buttercup10201,type,
b48_buttercup10201: $i > $o ).
thf(tp_b48_buttercup10208,type,
b48_buttercup10208: $i > $o ).
thf(tp_b48_buttercup10210,type,
b48_buttercup10210: $i > $o ).
thf(tp_b48_buttercup10214,type,
b48_buttercup10214: $i > $o ).
thf(tp_b48_buttercup10217,type,
b48_buttercup10217: $i > $o ).
thf(tp_b48_buttercup10220,type,
b48_buttercup10220: $i > $o ).
thf(tp_b48_buttercup10222,type,
b48_buttercup10222: $i > $o ).
thf(tp_b48_buttercup10227,type,
b48_buttercup10227: $i > $o ).
thf(tp_b48_buttercup10228,type,
b48_buttercup10228: $i > $o ).
thf(tp_b48_buttercup10229,type,
b48_buttercup10229: $i > $o ).
thf(tp_b48_buttercup10231,type,
b48_buttercup10231: $i > $o ).
thf(tp_b48_buttercup10240,type,
b48_buttercup10240: $i > $o ).
thf(tp_b48_buttercup10247,type,
b48_buttercup10247: $i > $o ).
thf(tp_b48_buttercup10248,type,
b48_buttercup10248: $i > $o ).
thf(tp_b48_buttercup10253,type,
b48_buttercup10253: $i > $o ).
thf(tp_b48_buttercup10260,type,
b48_buttercup10260: $i > $o ).
thf(tp_b48_buttercup10261,type,
b48_buttercup10261: $i > $o ).
thf(tp_b48_buttercup10266,type,
b48_buttercup10266: $i > $o ).
thf(tp_b48_buttercup10267,type,
b48_buttercup10267: $i > $o ).
thf(tp_b48_buttercup10268,type,
b48_buttercup10268: $i > $o ).
thf(tp_b48_buttercup10269,type,
b48_buttercup10269: $i > $o ).
thf(tp_b48_buttercup10271,type,
b48_buttercup10271: $i > $o ).
thf(tp_b48_buttercup10272,type,
b48_buttercup10272: $i > $o ).
thf(tp_b48_buttercup10273,type,
b48_buttercup10273: $i > $o ).
thf(tp_b48_buttercup10274,type,
b48_buttercup10274: $i > $o ).
thf(tp_b48_buttercup10275,type,
b48_buttercup10275: $i > $o ).
thf(tp_b48_buttercup10276,type,
b48_buttercup10276: $i > $o ).
thf(tp_b48_buttercup10277,type,
b48_buttercup10277: $i > $o ).
thf(tp_b48_buttercup10278,type,
b48_buttercup10278: $i > $o ).
thf(tp_b48_buttercup10279,type,
b48_buttercup10279: $i > $o ).
thf(tp_b48_buttercup10283,type,
b48_buttercup10283: $i > $o ).
thf(tp_b48_buttercup10289,type,
b48_buttercup10289: $i > $o ).
thf(tp_b48_buttercup10290,type,
b48_buttercup10290: $i > $o ).
thf(tp_b48_buttercup10291,type,
b48_buttercup10291: $i > $o ).
thf(tp_b48_buttercup10294,type,
b48_buttercup10294: $i > $o ).
thf(tp_b48_buttercup10299,type,
b48_buttercup10299: $i > $o ).
thf(tp_b48_buttercup10300,type,
b48_buttercup10300: $i > $o ).
thf(tp_b48_buttercup10305,type,
b48_buttercup10305: $i > $o ).
thf(tp_b48_buttercup10307,type,
b48_buttercup10307: $i > $o ).
thf(tp_b48_buttercup10308,type,
b48_buttercup10308: $i > $o ).
thf(tp_b48_buttercup10309,type,
b48_buttercup10309: $i > $o ).
thf(tp_b48_buttercup10313,type,
b48_buttercup10313: $i > $o ).
thf(tp_b48_buttercup10318,type,
b48_buttercup10318: $i > $o ).
thf(tp_b48_buttercup10320,type,
b48_buttercup10320: $i > $o ).
thf(tp_b48_buttercup10322,type,
b48_buttercup10322: $i > $o ).
thf(tp_b48_buttercup10326,type,
b48_buttercup10326: $i > $o ).
thf(tp_b48_buttercup10332,type,
b48_buttercup10332: $i > $o ).
thf(tp_b48_buttercup10334,type,
b48_buttercup10334: $i > $o ).
thf(tp_b48_buttercup10343,type,
b48_buttercup10343: $i > $o ).
thf(tp_b48_buttercup10344,type,
b48_buttercup10344: $i > $o ).
thf(tp_b48_buttercup10348,type,
b48_buttercup10348: $i > $o ).
thf(tp_b48_buttercup10352,type,
b48_buttercup10352: $i > $o ).
thf(tp_b48_buttercup10353,type,
b48_buttercup10353: $i > $o ).
thf(tp_b48_buttercup10358,type,
b48_buttercup10358: $i > $o ).
thf(tp_b48_buttercup10359,type,
b48_buttercup10359: $i > $o ).
thf(tp_b48_buttercup10361,type,
b48_buttercup10361: $i > $o ).
thf(tp_b48_buttercup10362,type,
b48_buttercup10362: $i > $o ).
thf(tp_b48_buttercup10365,type,
b48_buttercup10365: $i > $o ).
thf(tp_b48_buttercup10367,type,
b48_buttercup10367: $i > $o ).
thf(tp_b48_buttercup10370,type,
b48_buttercup10370: $i > $o ).
thf(tp_b48_buttercup10374,type,
b48_buttercup10374: $i > $o ).
thf(tp_b48_buttercup10377,type,
b48_buttercup10377: $i > $o ).
thf(tp_b48_buttercup10378,type,
b48_buttercup10378: $i > $o ).
thf(tp_b48_buttercup10381,type,
b48_buttercup10381: $i > $o ).
thf(tp_b48_buttercup10383,type,
b48_buttercup10383: $i > $o ).
thf(tp_b48_buttercup10386,type,
b48_buttercup10386: $i > $o ).
thf(tp_b48_buttercup10394,type,
b48_buttercup10394: $i > $o ).
thf(tp_b48_buttercup10398,type,
b48_buttercup10398: $i > $o ).
thf(tp_b48_buttercup10402,type,
b48_buttercup10402: $i > $o ).
thf(tp_b48_buttercup10405,type,
b48_buttercup10405: $i > $o ).
thf(tp_b48_buttercup10410,type,
b48_buttercup10410: $i > $o ).
thf(tp_b48_buttercup10411,type,
b48_buttercup10411: $i > $o ).
thf(tp_b48_buttercup10417,type,
b48_buttercup10417: $i > $o ).
thf(tp_b48_buttercup10420,type,
b48_buttercup10420: $i > $o ).
thf(tp_b48_buttercup10421,type,
b48_buttercup10421: $i > $o ).
thf(tp_b48_buttercup10422,type,
b48_buttercup10422: $i > $o ).
thf(tp_b48_buttercup10427,type,
b48_buttercup10427: $i > $o ).
thf(tp_b48_buttercup10433,type,
b48_buttercup10433: $i > $o ).
thf(tp_b48_buttercup10434,type,
b48_buttercup10434: $i > $o ).
thf(tp_b48_buttercup10440,type,
b48_buttercup10440: $i > $o ).
thf(tp_b48_buttercup10441,type,
b48_buttercup10441: $i > $o ).
thf(tp_b48_buttercup10442,type,
b48_buttercup10442: $i > $o ).
thf(tp_b48_buttercup10443,type,
b48_buttercup10443: $i > $o ).
thf(tp_b48_buttercup10446,type,
b48_buttercup10446: $i > $o ).
thf(tp_b48_buttercup10450,type,
b48_buttercup10450: $i > $o ).
thf(tp_b48_buttercup10451,type,
b48_buttercup10451: $i > $o ).
thf(tp_b48_buttercup10454,type,
b48_buttercup10454: $i > $o ).
thf(tp_b48_buttercup10456,type,
b48_buttercup10456: $i > $o ).
thf(tp_b48_buttercup10458,type,
b48_buttercup10458: $i > $o ).
thf(tp_b48_buttercup10460,type,
b48_buttercup10460: $i > $o ).
thf(tp_b48_buttercup10465,type,
b48_buttercup10465: $i > $o ).
thf(tp_b48_buttercup10466,type,
b48_buttercup10466: $i > $o ).
thf(tp_b48_buttercup10467,type,
b48_buttercup10467: $i > $o ).
thf(tp_b48_buttercup10469,type,
b48_buttercup10469: $i > $o ).
thf(tp_b48_buttercup10471,type,
b48_buttercup10471: $i > $o ).
thf(tp_b48_buttercup10474,type,
b48_buttercup10474: $i > $o ).
thf(tp_b48_buttercup10478,type,
b48_buttercup10478: $i > $o ).
thf(tp_b48_buttercup10479,type,
b48_buttercup10479: $i > $o ).
thf(tp_b48_buttercup10483,type,
b48_buttercup10483: $i > $o ).
thf(tp_b48_buttercup10487,type,
b48_buttercup10487: $i > $o ).
thf(tp_b48_buttercup10489,type,
b48_buttercup10489: $i > $o ).
thf(tp_b48_buttercup10490,type,
b48_buttercup10490: $i > $o ).
thf(tp_b48_buttercup10493,type,
b48_buttercup10493: $i > $o ).
thf(tp_b48_buttercup10496,type,
b48_buttercup10496: $i > $o ).
thf(tp_b48_buttercup10502,type,
b48_buttercup10502: $i > $o ).
thf(tp_b48_buttercup10507,type,
b48_buttercup10507: $i > $o ).
thf(tp_b48_buttercup10512,type,
b48_buttercup10512: $i > $o ).
thf(tp_b48_buttercup10513,type,
b48_buttercup10513: $i > $o ).
thf(tp_b48_buttercup10514,type,
b48_buttercup10514: $i > $o ).
thf(tp_b48_buttercup10515,type,
b48_buttercup10515: $i > $o ).
thf(tp_b48_buttercup10518,type,
b48_buttercup10518: $i > $o ).
thf(tp_b48_buttercup10519,type,
b48_buttercup10519: $i > $o ).
thf(tp_b48_buttercup10520,type,
b48_buttercup10520: $i > $o ).
thf(tp_b48_buttercup10521,type,
b48_buttercup10521: $i > $o ).
thf(tp_b48_buttercup10522,type,
b48_buttercup10522: $i > $o ).
thf(tp_b48_buttercup10526,type,
b48_buttercup10526: $i > $o ).
thf(tp_b48_buttercup10530,type,
b48_buttercup10530: $i > $o ).
thf(tp_b48_buttercup10531,type,
b48_buttercup10531: $i > $o ).
thf(tp_b48_buttercup10538,type,
b48_buttercup10538: $i > $o ).
thf(tp_b48_buttercup10541,type,
b48_buttercup10541: $i > $o ).
thf(tp_b48_buttercup10542,type,
b48_buttercup10542: $i > $o ).
thf(tp_b48_buttercup10545,type,
b48_buttercup10545: $i > $o ).
thf(tp_b48_buttercup10548,type,
b48_buttercup10548: $i > $o ).
thf(tp_b48_buttercup10549,type,
b48_buttercup10549: $i > $o ).
thf(tp_b48_buttercup10552,type,
b48_buttercup10552: $i > $o ).
thf(tp_b48_buttercup10561,type,
b48_buttercup10561: $i > $o ).
thf(tp_b48_buttercup10562,type,
b48_buttercup10562: $i > $o ).
thf(tp_b48_buttercup10563,type,
b48_buttercup10563: $i > $o ).
thf(tp_b48_buttercup10570,type,
b48_buttercup10570: $i > $o ).
thf(tp_b48_buttercup10572,type,
b48_buttercup10572: $i > $o ).
thf(tp_b48_buttercup10574,type,
b48_buttercup10574: $i > $o ).
thf(tp_b48_buttercup10575,type,
b48_buttercup10575: $i > $o ).
thf(tp_b48_buttercup10579,type,
b48_buttercup10579: $i > $o ).
thf(tp_b48_buttercup10582,type,
b48_buttercup10582: $i > $o ).
thf(tp_b48_buttercup10589,type,
b48_buttercup10589: $i > $o ).
thf(tp_b48_buttercup10596,type,
b48_buttercup10596: $i > $o ).
thf(tp_b48_buttercup10604,type,
b48_buttercup10604: $i > $o ).
thf(tp_b48_buttercup10605,type,
b48_buttercup10605: $i > $o ).
thf(tp_b48_buttercup10606,type,
b48_buttercup10606: $i > $o ).
thf(tp_b48_buttercup10609,type,
b48_buttercup10609: $i > $o ).
thf(tp_b48_buttercup10612,type,
b48_buttercup10612: $i > $o ).
thf(tp_b48_buttercup10616,type,
b48_buttercup10616: $i > $o ).
thf(tp_b48_buttercup10624,type,
b48_buttercup10624: $i > $o ).
thf(tp_b48_buttercup10629,type,
b48_buttercup10629: $i > $o ).
thf(tp_b48_buttercup10632,type,
b48_buttercup10632: $i > $o ).
thf(tp_b48_buttercup10636,type,
b48_buttercup10636: $i > $o ).
thf(tp_b48_buttercup10638,type,
b48_buttercup10638: $i > $o ).
thf(tp_b48_buttercup10640,type,
b48_buttercup10640: $i > $o ).
thf(tp_b48_buttercup10642,type,
b48_buttercup10642: $i > $o ).
thf(tp_b48_buttercup10646,type,
b48_buttercup10646: $i > $o ).
thf(tp_k04_buttercup10000,type,
k04_buttercup10000: $i > $o ).
thf(tp_k04_buttercup10004,type,
k04_buttercup10004: $i > $o ).
thf(tp_k04_buttercup10012,type,
k04_buttercup10012: $i > $o ).
thf(tp_k04_buttercup10016,type,
k04_buttercup10016: $i > $o ).
thf(tp_k04_buttercup10026,type,
k04_buttercup10026: $i > $o ).
thf(tp_k04_buttercup10028,type,
k04_buttercup10028: $i > $o ).
thf(tp_k04_buttercup10033,type,
k04_buttercup10033: $i > $o ).
thf(tp_k04_buttercup10039,type,
k04_buttercup10039: $i > $o ).
thf(tp_k04_buttercup10042,type,
k04_buttercup10042: $i > $o ).
thf(tp_k04_buttercup10044,type,
k04_buttercup10044: $i > $o ).
thf(tp_k04_buttercup10048,type,
k04_buttercup10048: $i > $o ).
thf(tp_k04_buttercup10049,type,
k04_buttercup10049: $i > $o ).
thf(tp_k04_buttercup10051,type,
k04_buttercup10051: $i > $o ).
thf(tp_k04_buttercup10053,type,
k04_buttercup10053: $i > $o ).
thf(tp_k04_buttercup10057,type,
k04_buttercup10057: $i > $o ).
thf(tp_k04_buttercup10061,type,
k04_buttercup10061: $i > $o ).
thf(tp_k04_buttercup10064,type,
k04_buttercup10064: $i > $o ).
thf(tp_k04_buttercup10067,type,
k04_buttercup10067: $i > $o ).
thf(tp_k04_buttercup10074,type,
k04_buttercup10074: $i > $o ).
thf(tp_k04_buttercup10079,type,
k04_buttercup10079: $i > $o ).
thf(tp_k04_buttercup10084,type,
k04_buttercup10084: $i > $o ).
thf(tp_k04_buttercup10089,type,
k04_buttercup10089: $i > $o ).
thf(tp_k04_buttercup10095,type,
k04_buttercup10095: $i > $o ).
thf(tp_k04_buttercup10096,type,
k04_buttercup10096: $i > $o ).
thf(tp_k04_buttercup10097,type,
k04_buttercup10097: $i > $o ).
thf(tp_k04_buttercup10100,type,
k04_buttercup10100: $i > $o ).
thf(tp_k04_buttercup10117,type,
k04_buttercup10117: $i > $o ).
thf(tp_k04_buttercup10125,type,
k04_buttercup10125: $i > $o ).
thf(tp_k04_buttercup10132,type,
k04_buttercup10132: $i > $o ).
thf(tp_k04_buttercup10135,type,
k04_buttercup10135: $i > $o ).
thf(tp_k04_buttercup10139,type,
k04_buttercup10139: $i > $o ).
thf(tp_k04_buttercup10142,type,
k04_buttercup10142: $i > $o ).
thf(tp_k04_buttercup10147,type,
k04_buttercup10147: $i > $o ).
thf(tp_k04_buttercup10153,type,
k04_buttercup10153: $i > $o ).
thf(tp_k04_buttercup10164,type,
k04_buttercup10164: $i > $o ).
thf(tp_k04_buttercup10172,type,
k04_buttercup10172: $i > $o ).
thf(tp_k04_buttercup10181,type,
k04_buttercup10181: $i > $o ).
thf(tp_k04_buttercup10184,type,
k04_buttercup10184: $i > $o ).
thf(tp_k04_buttercup10190,type,
k04_buttercup10190: $i > $o ).
thf(tp_k04_buttercup10200,type,
k04_buttercup10200: $i > $o ).
thf(tp_k04_buttercup10204,type,
k04_buttercup10204: $i > $o ).
thf(tp_k04_buttercup10206,type,
k04_buttercup10206: $i > $o ).
thf(tp_k04_buttercup10213,type,
k04_buttercup10213: $i > $o ).
thf(tp_k04_buttercup10219,type,
k04_buttercup10219: $i > $o ).
thf(tp_k04_buttercup10221,type,
k04_buttercup10221: $i > $o ).
thf(tp_k04_buttercup10225,type,
k04_buttercup10225: $i > $o ).
thf(tp_k04_buttercup10234,type,
k04_buttercup10234: $i > $o ).
thf(tp_k04_buttercup10236,type,
k04_buttercup10236: $i > $o ).
thf(tp_k04_buttercup10238,type,
k04_buttercup10238: $i > $o ).
thf(tp_k04_buttercup10244,type,
k04_buttercup10244: $i > $o ).
thf(tp_k04_buttercup10252,type,
k04_buttercup10252: $i > $o ).
thf(tp_k04_buttercup10255,type,
k04_buttercup10255: $i > $o ).
thf(tp_k04_buttercup10259,type,
k04_buttercup10259: $i > $o ).
thf(tp_k04_buttercup10282,type,
k04_buttercup10282: $i > $o ).
thf(tp_k04_buttercup10286,type,
k04_buttercup10286: $i > $o ).
thf(tp_k04_buttercup10288,type,
k04_buttercup10288: $i > $o ).
thf(tp_k04_buttercup10293,type,
k04_buttercup10293: $i > $o ).
thf(tp_k04_buttercup10296,type,
k04_buttercup10296: $i > $o ).
thf(tp_k04_buttercup10298,type,
k04_buttercup10298: $i > $o ).
thf(tp_k04_buttercup10303,type,
k04_buttercup10303: $i > $o ).
thf(tp_k04_buttercup10312,type,
k04_buttercup10312: $i > $o ).
thf(tp_k04_buttercup10316,type,
k04_buttercup10316: $i > $o ).
thf(tp_k04_buttercup10325,type,
k04_buttercup10325: $i > $o ).
thf(tp_k04_buttercup10329,type,
k04_buttercup10329: $i > $o ).
thf(tp_k04_buttercup10333,type,
k04_buttercup10333: $i > $o ).
thf(tp_k04_buttercup10337,type,
k04_buttercup10337: $i > $o ).
thf(tp_k04_buttercup10342,type,
k04_buttercup10342: $i > $o ).
thf(tp_k04_buttercup10347,type,
k04_buttercup10347: $i > $o ).
thf(tp_k04_buttercup10351,type,
k04_buttercup10351: $i > $o ).
thf(tp_k04_buttercup10356,type,
k04_buttercup10356: $i > $o ).
thf(tp_k04_buttercup10357,type,
k04_buttercup10357: $i > $o ).
thf(tp_k04_buttercup10360,type,
k04_buttercup10360: $i > $o ).
thf(tp_k04_buttercup10364,type,
k04_buttercup10364: $i > $o ).
thf(tp_k04_buttercup10369,type,
k04_buttercup10369: $i > $o ).
thf(tp_k04_buttercup10371,type,
k04_buttercup10371: $i > $o ).
thf(tp_k04_buttercup10373,type,
k04_buttercup10373: $i > $o ).
thf(tp_k04_buttercup10376,type,
k04_buttercup10376: $i > $o ).
thf(tp_k04_buttercup10380,type,
k04_buttercup10380: $i > $o ).
thf(tp_k04_buttercup10382,type,
k04_buttercup10382: $i > $o ).
thf(tp_k04_buttercup10385,type,
k04_buttercup10385: $i > $o ).
thf(tp_k04_buttercup10389,type,
k04_buttercup10389: $i > $o ).
thf(tp_k04_buttercup10391,type,
k04_buttercup10391: $i > $o ).
thf(tp_k04_buttercup10397,type,
k04_buttercup10397: $i > $o ).
thf(tp_k04_buttercup10400,type,
k04_buttercup10400: $i > $o ).
thf(tp_k04_buttercup10404,type,
k04_buttercup10404: $i > $o ).
thf(tp_k04_buttercup10406,type,
k04_buttercup10406: $i > $o ).
thf(tp_k04_buttercup10408,type,
k04_buttercup10408: $i > $o ).
thf(tp_k04_buttercup10415,type,
k04_buttercup10415: $i > $o ).
thf(tp_k04_buttercup10419,type,
k04_buttercup10419: $i > $o ).
thf(tp_k04_buttercup10424,type,
k04_buttercup10424: $i > $o ).
thf(tp_k04_buttercup10425,type,
k04_buttercup10425: $i > $o ).
thf(tp_k04_buttercup10430,type,
k04_buttercup10430: $i > $o ).
thf(tp_k04_buttercup10437,type,
k04_buttercup10437: $i > $o ).
thf(tp_k04_buttercup10445,type,
k04_buttercup10445: $i > $o ).
thf(tp_k04_buttercup10449,type,
k04_buttercup10449: $i > $o ).
thf(tp_k04_buttercup10453,type,
k04_buttercup10453: $i > $o ).
thf(tp_k04_buttercup10462,type,
k04_buttercup10462: $i > $o ).
thf(tp_k04_buttercup10464,type,
k04_buttercup10464: $i > $o ).
thf(tp_k04_buttercup10470,type,
k04_buttercup10470: $i > $o ).
thf(tp_k04_buttercup10473,type,
k04_buttercup10473: $i > $o ).
thf(tp_k04_buttercup10477,type,
k04_buttercup10477: $i > $o ).
thf(tp_k04_buttercup10482,type,
k04_buttercup10482: $i > $o ).
thf(tp_k04_buttercup10486,type,
k04_buttercup10486: $i > $o ).
thf(tp_k04_buttercup10492,type,
k04_buttercup10492: $i > $o ).
thf(tp_k04_buttercup10495,type,
k04_buttercup10495: $i > $o ).
thf(tp_k04_buttercup10499,type,
k04_buttercup10499: $i > $o ).
thf(tp_k04_buttercup10504,type,
k04_buttercup10504: $i > $o ).
thf(tp_k04_buttercup10506,type,
k04_buttercup10506: $i > $o ).
thf(tp_k04_buttercup10510,type,
k04_buttercup10510: $i > $o ).
thf(tp_k04_buttercup10516,type,
k04_buttercup10516: $i > $o ).
thf(tp_k04_buttercup10517,type,
k04_buttercup10517: $i > $o ).
thf(tp_k04_buttercup10524,type,
k04_buttercup10524: $i > $o ).
thf(tp_k04_buttercup10529,type,
k04_buttercup10529: $i > $o ).
thf(tp_k04_buttercup10535,type,
k04_buttercup10535: $i > $o ).
thf(tp_k04_buttercup10539,type,
k04_buttercup10539: $i > $o ).
thf(tp_k04_buttercup10540,type,
k04_buttercup10540: $i > $o ).
thf(tp_k04_buttercup10544,type,
k04_buttercup10544: $i > $o ).
thf(tp_k04_buttercup10546,type,
k04_buttercup10546: $i > $o ).
thf(tp_k04_buttercup10547,type,
k04_buttercup10547: $i > $o ).
thf(tp_k04_buttercup10551,type,
k04_buttercup10551: $i > $o ).
thf(tp_k04_buttercup10555,type,
k04_buttercup10555: $i > $o ).
thf(tp_k04_buttercup10559,type,
k04_buttercup10559: $i > $o ).
thf(tp_k04_buttercup10567,type,
k04_buttercup10567: $i > $o ).
thf(tp_k04_buttercup10578,type,
k04_buttercup10578: $i > $o ).
thf(tp_k04_buttercup10581,type,
k04_buttercup10581: $i > $o ).
thf(tp_k04_buttercup10586,type,
k04_buttercup10586: $i > $o ).
thf(tp_k04_buttercup10593,type,
k04_buttercup10593: $i > $o ).
thf(tp_k04_buttercup10599,type,
k04_buttercup10599: $i > $o ).
thf(tp_k04_buttercup10602,type,
k04_buttercup10602: $i > $o ).
thf(tp_k04_buttercup10608,type,
k04_buttercup10608: $i > $o ).
thf(tp_k04_buttercup10611,type,
k04_buttercup10611: $i > $o ).
thf(tp_k04_buttercup10619,type,
k04_buttercup10619: $i > $o ).
thf(tp_k04_buttercup10620,type,
k04_buttercup10620: $i > $o ).
thf(tp_k04_buttercup10622,type,
k04_buttercup10622: $i > $o ).
thf(tp_k04_buttercup10626,type,
k04_buttercup10626: $i > $o ).
thf(tp_k04_buttercup10628,type,
k04_buttercup10628: $i > $o ).
thf(tp_k04_buttercup10631,type,
k04_buttercup10631: $i > $o ).
thf(tp_k04_buttercup10635,type,
k04_buttercup10635: $i > $o ).
thf(tp_k04_buttercup10637,type,
k04_buttercup10637: $i > $o ).
thf(tp_k04_buttercup10639,type,
k04_buttercup10639: $i > $o ).
thf(tp_k04_buttercup10641,type,
k04_buttercup10641: $i > $o ).
thf(tp_k04_buttercup10643,type,
k04_buttercup10643: $i > $o ).
thf(tp_sK1_SX0,type,
sK1_SX0: $i ).
thf(tp_sK2_SX0,type,
sK2_SX0: $i ).
thf(tp_sK3_SX0,type,
sK3_SX0: $i ).
thf(tp_sK4_SX0,type,
sK4_SX0: $i ).
thf(tp_sK5_SX0,type,
sK5_SX0: $i ).
thf(tp_sK6_SX0,type,
sK6_SX0: $i ).
thf(tp_sK7_SX0,type,
sK7_SX0: $i ).
thf(tp_sK8_SX0,type,
sK8_SX0: $i ).
thf(tp_sK9_SX0,type,
sK9_SX0: $i ).
thf(137,axiom,
? [X918: $i] : ( b48_buttercup10305 @ X918 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_749) ).
thf(308,axiom,
? [X747: $i] : ( k04_buttercup10303 @ X747 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_578) ).
thf(407,axiom,
( ! [X619: $i] :
( ( b48_buttercup10308 @ X619 )
=> ( k04_buttercup10303 @ X619 ) )
& ? [X620: $i] :
( ( k04_buttercup10303 @ X620 )
& ~ ( b48_buttercup10308 @ X620 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_479) ).
thf(563,axiom,
( ! [X323: $i] :
( ( b48_buttercup10307 @ X323 )
=> ( k04_buttercup10303 @ X323 ) )
& ? [X324: $i] :
( ( k04_buttercup10303 @ X324 )
& ~ ( b48_buttercup10307 @ X324 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_323) ).
thf(564,axiom,
! [X322: $i] :
( ( k04_buttercup10303 @ X322 )
<=> ( b48_buttercup10300 @ X322 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_322) ).
thf(566,axiom,
( ! [X319: $i] :
( ( b48_buttercup10305 @ X319 )
=> ( k04_buttercup10303 @ X319 ) )
& ? [X320: $i] :
( ( k04_buttercup10303 @ X320 )
& ~ ( b48_buttercup10305 @ X320 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_320) ).
thf(754,axiom,
! [X131: $i] :
( ( b48_buttercup10305 @ X131 )
=> ( b48_buttercup10300 @ X131 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_132) ).
thf(830,axiom,
! [X55: $i] :
( ( k04_buttercup10303 @ X55 )
=> ( k04_buttercup10012 @ X55 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_56) ).
thf(886,conjecture,
( ! [X1055: $i] :
( ( b48_buttercup10305 @ X1055 )
<=> ( k04_buttercup10303 @ X1055 ) )
| ( ! [X1056: $i] :
( ( k04_buttercup10303 @ X1056 )
=> ( b48_buttercup10305 @ X1056 ) )
& ? [X1057: $i] :
( ( b48_buttercup10305 @ X1057 )
& ~ ( k04_buttercup10303 @ X1057 ) ) )
| ( ! [X1058: $i] :
( ( b48_buttercup10305 @ X1058 )
=> ( k04_buttercup10303 @ X1058 ) )
& ? [X1059: $i] :
( ( k04_buttercup10303 @ X1059 )
& ~ ( b48_buttercup10305 @ X1059 ) ) )
| ! [X1060: $i] :
( ( b48_buttercup10305 @ X1060 )
=> ~ ( k04_buttercup10303 @ X1060 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_886) ).
thf(887,negated_conjecture,
( ( ! [X1055: $i] :
( ( b48_buttercup10305 @ X1055 )
<=> ( k04_buttercup10303 @ X1055 ) )
| ( ! [X1056: $i] :
( ( k04_buttercup10303 @ X1056 )
=> ( b48_buttercup10305 @ X1056 ) )
& ? [X1057: $i] :
( ( b48_buttercup10305 @ X1057 )
& ~ ( k04_buttercup10303 @ X1057 ) ) )
| ( ! [X1058: $i] :
( ( b48_buttercup10305 @ X1058 )
=> ( k04_buttercup10303 @ X1058 ) )
& ? [X1059: $i] :
( ( k04_buttercup10303 @ X1059 )
& ~ ( b48_buttercup10305 @ X1059 ) ) )
| ! [X1060: $i] :
( ( b48_buttercup10305 @ X1060 )
=> ~ ( k04_buttercup10303 @ X1060 ) ) )
= $false ),
inference(negate_conjecture,[status(cth)],[886]) ).
thf(888,plain,
( ( ! [X1055: $i] :
( ( b48_buttercup10305 @ X1055 )
<=> ( k04_buttercup10303 @ X1055 ) )
| ( ! [X1056: $i] :
( ( k04_buttercup10303 @ X1056 )
=> ( b48_buttercup10305 @ X1056 ) )
& ? [X1057: $i] :
( ( b48_buttercup10305 @ X1057 )
& ~ ( k04_buttercup10303 @ X1057 ) ) )
| ( ! [X1058: $i] :
( ( b48_buttercup10305 @ X1058 )
=> ( k04_buttercup10303 @ X1058 ) )
& ? [X1059: $i] :
( ( k04_buttercup10303 @ X1059 )
& ~ ( b48_buttercup10305 @ X1059 ) ) )
| ! [X1060: $i] :
( ( b48_buttercup10305 @ X1060 )
=> ~ ( k04_buttercup10303 @ X1060 ) ) )
= $false ),
inference(unfold_def,[status(thm)],[887]) ).
thf(889,plain,
( ( ? [X918: $i] : ( b48_buttercup10305 @ X918 ) )
= $true ),
inference(unfold_def,[status(thm)],[137]) ).
thf(890,plain,
( ( ? [X747: $i] : ( k04_buttercup10303 @ X747 ) )
= $true ),
inference(unfold_def,[status(thm)],[308]) ).
thf(891,plain,
( ( ! [X619: $i] :
( ( b48_buttercup10308 @ X619 )
=> ( k04_buttercup10303 @ X619 ) )
& ? [X620: $i] :
( ( k04_buttercup10303 @ X620 )
& ~ ( b48_buttercup10308 @ X620 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[407]) ).
thf(892,plain,
( ( ! [X323: $i] :
( ( b48_buttercup10307 @ X323 )
=> ( k04_buttercup10303 @ X323 ) )
& ? [X324: $i] :
( ( k04_buttercup10303 @ X324 )
& ~ ( b48_buttercup10307 @ X324 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[563]) ).
thf(893,plain,
( ( ! [X322: $i] :
( ( k04_buttercup10303 @ X322 )
<=> ( b48_buttercup10300 @ X322 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[564]) ).
thf(894,plain,
( ( ! [X319: $i] :
( ( b48_buttercup10305 @ X319 )
=> ( k04_buttercup10303 @ X319 ) )
& ? [X320: $i] :
( ( k04_buttercup10303 @ X320 )
& ~ ( b48_buttercup10305 @ X320 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[566]) ).
thf(895,plain,
( ( ! [X131: $i] :
( ( b48_buttercup10305 @ X131 )
=> ( b48_buttercup10300 @ X131 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[754]) ).
thf(896,plain,
( ( ! [X55: $i] :
( ( k04_buttercup10303 @ X55 )
=> ( k04_buttercup10012 @ X55 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[830]) ).
thf(897,plain,
( ( ~ ( ! [X1055: $i] :
( ( b48_buttercup10305 @ X1055 )
<=> ( k04_buttercup10303 @ X1055 ) )
| ( ! [X1056: $i] :
( ( k04_buttercup10303 @ X1056 )
=> ( b48_buttercup10305 @ X1056 ) )
& ? [X1057: $i] :
( ( b48_buttercup10305 @ X1057 )
& ~ ( k04_buttercup10303 @ X1057 ) ) )
| ( ! [X1058: $i] :
( ( b48_buttercup10305 @ X1058 )
=> ( k04_buttercup10303 @ X1058 ) )
& ? [X1059: $i] :
( ( k04_buttercup10303 @ X1059 )
& ~ ( b48_buttercup10305 @ X1059 ) ) )
| ! [X1060: $i] :
( ( b48_buttercup10305 @ X1060 )
=> ~ ( k04_buttercup10303 @ X1060 ) ) ) )
= $true ),
inference(polarity_switch,[status(thm)],[888]) ).
thf(898,plain,
( ( ! [X55: $i] :
( ( k04_buttercup10303 @ X55 )
=> ( k04_buttercup10012 @ X55 ) ) )
= $true ),
inference(copy,[status(thm)],[896]) ).
thf(899,plain,
( ( ! [X131: $i] :
( ( b48_buttercup10305 @ X131 )
=> ( b48_buttercup10300 @ X131 ) ) )
= $true ),
inference(copy,[status(thm)],[895]) ).
thf(900,plain,
( ( ! [X319: $i] :
( ( b48_buttercup10305 @ X319 )
=> ( k04_buttercup10303 @ X319 ) )
& ? [X320: $i] :
( ( k04_buttercup10303 @ X320 )
& ~ ( b48_buttercup10305 @ X320 ) ) )
= $true ),
inference(copy,[status(thm)],[894]) ).
thf(901,plain,
( ( ! [X322: $i] :
( ( k04_buttercup10303 @ X322 )
<=> ( b48_buttercup10300 @ X322 ) ) )
= $true ),
inference(copy,[status(thm)],[893]) ).
thf(902,plain,
( ( ! [X323: $i] :
( ( b48_buttercup10307 @ X323 )
=> ( k04_buttercup10303 @ X323 ) )
& ? [X324: $i] :
( ( k04_buttercup10303 @ X324 )
& ~ ( b48_buttercup10307 @ X324 ) ) )
= $true ),
inference(copy,[status(thm)],[892]) ).
thf(903,plain,
( ( ! [X619: $i] :
( ( b48_buttercup10308 @ X619 )
=> ( k04_buttercup10303 @ X619 ) )
& ? [X620: $i] :
( ( k04_buttercup10303 @ X620 )
& ~ ( b48_buttercup10308 @ X620 ) ) )
= $true ),
inference(copy,[status(thm)],[891]) ).
thf(904,plain,
( ( ? [X747: $i] : ( k04_buttercup10303 @ X747 ) )
= $true ),
inference(copy,[status(thm)],[890]) ).
thf(905,plain,
( ( ? [X918: $i] : ( b48_buttercup10305 @ X918 ) )
= $true ),
inference(copy,[status(thm)],[889]) ).
thf(906,plain,
( ( ~ ( ! [X1055: $i] :
( ( b48_buttercup10305 @ X1055 )
<=> ( k04_buttercup10303 @ X1055 ) )
| ( ! [X1056: $i] :
( ( k04_buttercup10303 @ X1056 )
=> ( b48_buttercup10305 @ X1056 ) )
& ? [X1057: $i] :
( ( b48_buttercup10305 @ X1057 )
& ~ ( k04_buttercup10303 @ X1057 ) ) )
| ( ! [X1058: $i] :
( ( b48_buttercup10305 @ X1058 )
=> ( k04_buttercup10303 @ X1058 ) )
& ? [X1059: $i] :
( ( k04_buttercup10303 @ X1059 )
& ~ ( b48_buttercup10305 @ X1059 ) ) )
| ! [X1060: $i] :
( ( b48_buttercup10305 @ X1060 )
=> ~ ( k04_buttercup10303 @ X1060 ) ) ) )
= $true ),
inference(copy,[status(thm)],[897]) ).
thf(907,plain,
( ( ~ ! [SX0: $i] :
~ ( k04_buttercup10303 @ SX0 ) )
= $true ),
inference(unfold_def,[status(thm)],[904]) ).
thf(908,plain,
( ( ~ ! [SX0: $i] :
~ ( b48_buttercup10305 @ SX0 ) )
= $true ),
inference(unfold_def,[status(thm)],[905]) ).
thf(909,plain,
( ( ! [SX0: $i] :
( ~ ( k04_buttercup10303 @ SX0 )
| ( k04_buttercup10012 @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[898]) ).
thf(910,plain,
( ( ~ ( ! [SX0: $i] :
~ ( ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) ) )
| ~ ( ~ ! [SX0: $i] :
( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
| ~ ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
| ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ~ ( k04_buttercup10303 @ SX0 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[906]) ).
thf(911,plain,
( ( ~ ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10308 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10308 @ SX0 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[903]) ).
thf(912,plain,
( ( ~ ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[900]) ).
thf(913,plain,
( ( ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ( b48_buttercup10300 @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[899]) ).
thf(914,plain,
( ( ~ ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10307 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10307 @ SX0 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[902]) ).
thf(915,plain,
( ( ! [SX0: $i] :
~ ( ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10300 @ SX0 ) )
| ~ ( ~ ( b48_buttercup10300 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[901]) ).
thf(916,plain,
( ( ! [SX0: $i] :
~ ( k04_buttercup10303 @ SX0 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[907]) ).
thf(917,plain,
( ( ! [SX0: $i] :
~ ( b48_buttercup10305 @ SX0 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[908]) ).
thf(918,plain,
! [SV1: $i] :
( ( ~ ( k04_buttercup10303 @ SV1 )
| ( k04_buttercup10012 @ SV1 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[909]) ).
thf(919,plain,
( ( ! [SX0: $i] :
~ ( ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) ) )
| ~ ( ~ ! [SX0: $i] :
( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
| ~ ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
| ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ~ ( k04_buttercup10303 @ SX0 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[910]) ).
thf(920,plain,
( ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10308 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10308 @ SX0 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[911]) ).
thf(921,plain,
( ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[912]) ).
thf(922,plain,
! [SV2: $i] :
( ( ~ ( b48_buttercup10305 @ SV2 )
| ( b48_buttercup10300 @ SV2 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[913]) ).
thf(923,plain,
( ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10307 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10307 @ SX0 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[914]) ).
thf(924,plain,
! [SV3: $i] :
( ( ~ ( ~ ( ~ ( k04_buttercup10303 @ SV3 )
| ( b48_buttercup10300 @ SV3 ) )
| ~ ( ~ ( b48_buttercup10300 @ SV3 )
| ( k04_buttercup10303 @ SV3 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[915]) ).
thf(925,plain,
( ( ~ ( k04_buttercup10303 @ sK1_SX0 ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[916]) ).
thf(926,plain,
( ( ~ ( b48_buttercup10305 @ sK2_SX0 ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[917]) ).
thf(927,plain,
! [SV1: $i] :
( ( ( ~ ( k04_buttercup10303 @ SV1 ) )
= $true )
| ( ( k04_buttercup10012 @ SV1 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[918]) ).
thf(928,plain,
( ( ! [SX0: $i] :
~ ( ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) ) )
| ~ ( ~ ! [SX0: $i] :
( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
| ~ ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[919]) ).
thf(929,plain,
( ( ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ~ ( k04_buttercup10303 @ SX0 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[919]) ).
thf(930,plain,
( ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10308 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[920]) ).
thf(931,plain,
( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10308 @ SX0 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[920]) ).
thf(932,plain,
( ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[921]) ).
thf(933,plain,
( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[921]) ).
thf(934,plain,
! [SV2: $i] :
( ( ( ~ ( b48_buttercup10305 @ SV2 ) )
= $true )
| ( ( b48_buttercup10300 @ SV2 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[922]) ).
thf(935,plain,
( ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10307 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[923]) ).
thf(936,plain,
( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10307 @ SX0 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[923]) ).
thf(937,plain,
! [SV3: $i] :
( ( ~ ( ~ ( k04_buttercup10303 @ SV3 )
| ( b48_buttercup10300 @ SV3 ) )
| ~ ( ~ ( b48_buttercup10300 @ SV3 )
| ( k04_buttercup10303 @ SV3 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[924]) ).
thf(938,plain,
( ( k04_buttercup10303 @ sK1_SX0 )
= $true ),
inference(extcnf_not_neg,[status(thm)],[925]) ).
thf(939,plain,
( ( b48_buttercup10305 @ sK2_SX0 )
= $true ),
inference(extcnf_not_neg,[status(thm)],[926]) ).
thf(940,plain,
! [SV1: $i] :
( ( ( k04_buttercup10303 @ SV1 )
= $false )
| ( ( k04_buttercup10012 @ SV1 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[927]) ).
thf(941,plain,
( ( ! [SX0: $i] :
~ ( ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) ) )
| ~ ( ~ ! [SX0: $i] :
( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[928]) ).
thf(942,plain,
( ( ~ ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[928]) ).
thf(943,plain,
( ( ~ ( b48_buttercup10305 @ sK3_SX0 )
| ~ ( k04_buttercup10303 @ sK3_SX0 ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[929]) ).
thf(944,plain,
( ( ! [SX0: $i] :
( ~ ( b48_buttercup10308 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[930]) ).
thf(945,plain,
( ( ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10308 @ SX0 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[931]) ).
thf(946,plain,
( ( ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[932]) ).
thf(947,plain,
( ( ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[933]) ).
thf(948,plain,
! [SV2: $i] :
( ( ( b48_buttercup10305 @ SV2 )
= $false )
| ( ( b48_buttercup10300 @ SV2 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[934]) ).
thf(949,plain,
( ( ! [SX0: $i] :
( ~ ( b48_buttercup10307 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[935]) ).
thf(950,plain,
( ( ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10307 @ SX0 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[936]) ).
thf(951,plain,
! [SV3: $i] :
( ( ~ ( ~ ( k04_buttercup10303 @ SV3 )
| ( b48_buttercup10300 @ SV3 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[937]) ).
thf(952,plain,
! [SV3: $i] :
( ( ~ ( ~ ( b48_buttercup10300 @ SV3 )
| ( k04_buttercup10303 @ SV3 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[937]) ).
thf(953,plain,
( ( ! [SX0: $i] :
~ ( ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[941]) ).
thf(954,plain,
( ( ~ ( ~ ! [SX0: $i] :
( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[941]) ).
thf(955,plain,
( ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[942]) ).
thf(956,plain,
( ( ~ ( b48_buttercup10305 @ sK3_SX0 ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[943]) ).
thf(957,plain,
( ( ~ ( k04_buttercup10303 @ sK3_SX0 ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[943]) ).
thf(958,plain,
! [SV4: $i] :
( ( ~ ( b48_buttercup10308 @ SV4 )
| ( k04_buttercup10303 @ SV4 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[944]) ).
thf(959,plain,
( ( ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10308 @ SX0 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[945]) ).
thf(960,plain,
! [SV5: $i] :
( ( ~ ( b48_buttercup10305 @ SV5 )
| ( k04_buttercup10303 @ SV5 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[946]) ).
thf(961,plain,
( ( ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[947]) ).
thf(962,plain,
! [SV6: $i] :
( ( ~ ( b48_buttercup10307 @ SV6 )
| ( k04_buttercup10303 @ SV6 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[949]) ).
thf(963,plain,
( ( ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10307 @ SX0 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[950]) ).
thf(964,plain,
! [SV3: $i] :
( ( ~ ( k04_buttercup10303 @ SV3 )
| ( b48_buttercup10300 @ SV3 ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[951]) ).
thf(965,plain,
! [SV3: $i] :
( ( ~ ( b48_buttercup10300 @ SV3 )
| ( k04_buttercup10303 @ SV3 ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[952]) ).
thf(966,plain,
( ( ~ ( ~ ( ~ ( b48_buttercup10305 @ sK4_SX0 )
| ( k04_buttercup10303 @ sK4_SX0 ) )
| ~ ( ~ ( k04_buttercup10303 @ sK4_SX0 )
| ( b48_buttercup10305 @ sK4_SX0 ) ) ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[953]) ).
thf(967,plain,
( ( ~ ! [SX0: $i] :
( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) )
| ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[954]) ).
thf(968,plain,
( ( ( ~ ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) ) )
= $true )
| ( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[955]) ).
thf(969,plain,
( ( b48_buttercup10305 @ sK3_SX0 )
= $true ),
inference(extcnf_not_neg,[status(thm)],[956]) ).
thf(970,plain,
( ( k04_buttercup10303 @ sK3_SX0 )
= $true ),
inference(extcnf_not_neg,[status(thm)],[957]) ).
thf(971,plain,
! [SV4: $i] :
( ( ( ~ ( b48_buttercup10308 @ SV4 ) )
= $true )
| ( ( k04_buttercup10303 @ SV4 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[958]) ).
thf(972,plain,
( ( ~ ~ ( ~ ( k04_buttercup10303 @ sK5_SX0 )
| ~ ~ ( b48_buttercup10308 @ sK5_SX0 ) ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[959]) ).
thf(973,plain,
! [SV5: $i] :
( ( ( ~ ( b48_buttercup10305 @ SV5 ) )
= $true )
| ( ( k04_buttercup10303 @ SV5 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[960]) ).
thf(974,plain,
( ( ~ ~ ( ~ ( k04_buttercup10303 @ sK6_SX0 )
| ~ ~ ( b48_buttercup10305 @ sK6_SX0 ) ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[961]) ).
thf(975,plain,
! [SV6: $i] :
( ( ( ~ ( b48_buttercup10307 @ SV6 ) )
= $true )
| ( ( k04_buttercup10303 @ SV6 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[962]) ).
thf(976,plain,
( ( ~ ~ ( ~ ( k04_buttercup10303 @ sK7_SX0 )
| ~ ~ ( b48_buttercup10307 @ sK7_SX0 ) ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[963]) ).
thf(977,plain,
! [SV3: $i] :
( ( ( ~ ( k04_buttercup10303 @ SV3 ) )
= $true )
| ( ( b48_buttercup10300 @ SV3 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[964]) ).
thf(978,plain,
! [SV3: $i] :
( ( ( ~ ( b48_buttercup10300 @ SV3 ) )
= $true )
| ( ( k04_buttercup10303 @ SV3 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[965]) ).
thf(979,plain,
( ( ~ ( ~ ( b48_buttercup10305 @ sK4_SX0 )
| ( k04_buttercup10303 @ sK4_SX0 ) )
| ~ ( ~ ( k04_buttercup10303 @ sK4_SX0 )
| ( b48_buttercup10305 @ sK4_SX0 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[966]) ).
thf(980,plain,
( ( ( ~ ! [SX0: $i] :
( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) ) )
= $true )
| ( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[967]) ).
thf(981,plain,
( ( ( ! [SX0: $i] :
( ~ ( b48_buttercup10305 @ SX0 )
| ( k04_buttercup10303 @ SX0 ) ) )
= $false )
| ( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[968]) ).
thf(982,plain,
! [SV4: $i] :
( ( ( b48_buttercup10308 @ SV4 )
= $false )
| ( ( k04_buttercup10303 @ SV4 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[971]) ).
thf(983,plain,
( ( ~ ( ~ ( k04_buttercup10303 @ sK5_SX0 )
| ~ ~ ( b48_buttercup10308 @ sK5_SX0 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[972]) ).
thf(984,plain,
! [SV5: $i] :
( ( ( b48_buttercup10305 @ SV5 )
= $false )
| ( ( k04_buttercup10303 @ SV5 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[973]) ).
thf(985,plain,
( ( ~ ( ~ ( k04_buttercup10303 @ sK6_SX0 )
| ~ ~ ( b48_buttercup10305 @ sK6_SX0 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[974]) ).
thf(986,plain,
! [SV6: $i] :
( ( ( b48_buttercup10307 @ SV6 )
= $false )
| ( ( k04_buttercup10303 @ SV6 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[975]) ).
thf(987,plain,
( ( ~ ( ~ ( k04_buttercup10303 @ sK7_SX0 )
| ~ ~ ( b48_buttercup10307 @ sK7_SX0 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[976]) ).
thf(988,plain,
! [SV3: $i] :
( ( ( k04_buttercup10303 @ SV3 )
= $false )
| ( ( b48_buttercup10300 @ SV3 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[977]) ).
thf(989,plain,
! [SV3: $i] :
( ( ( b48_buttercup10300 @ SV3 )
= $false )
| ( ( k04_buttercup10303 @ SV3 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[978]) ).
thf(990,plain,
( ( ( ~ ( ~ ( b48_buttercup10305 @ sK4_SX0 )
| ( k04_buttercup10303 @ sK4_SX0 ) ) )
= $true )
| ( ( ~ ( ~ ( k04_buttercup10303 @ sK4_SX0 )
| ( b48_buttercup10305 @ sK4_SX0 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[979]) ).
thf(991,plain,
( ( ( ! [SX0: $i] :
( ~ ( k04_buttercup10303 @ SX0 )
| ( b48_buttercup10305 @ SX0 ) ) )
= $false )
| ( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[980]) ).
thf(992,plain,
( ( ( ~ ( b48_buttercup10305 @ sK8_SX0 )
| ( k04_buttercup10303 @ sK8_SX0 ) )
= $false )
| ( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $true ) ),
inference(extcnf_forall_neg,[status(esa)],[981]) ).
thf(993,plain,
( ( ~ ( k04_buttercup10303 @ sK5_SX0 )
| ~ ~ ( b48_buttercup10308 @ sK5_SX0 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[983]) ).
thf(994,plain,
( ( ~ ( k04_buttercup10303 @ sK6_SX0 )
| ~ ~ ( b48_buttercup10305 @ sK6_SX0 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[985]) ).
thf(995,plain,
( ( ~ ( k04_buttercup10303 @ sK7_SX0 )
| ~ ~ ( b48_buttercup10307 @ sK7_SX0 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[987]) ).
thf(996,plain,
( ( ( ~ ( b48_buttercup10305 @ sK4_SX0 )
| ( k04_buttercup10303 @ sK4_SX0 ) )
= $false )
| ( ( ~ ( ~ ( k04_buttercup10303 @ sK4_SX0 )
| ( b48_buttercup10305 @ sK4_SX0 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[990]) ).
thf(997,plain,
( ( ( ~ ( k04_buttercup10303 @ sK9_SX0 )
| ( b48_buttercup10305 @ sK9_SX0 ) )
= $false )
| ( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
= $true ) ),
inference(extcnf_forall_neg,[status(esa)],[991]) ).
thf(998,plain,
( ( ( ~ ( b48_buttercup10305 @ sK8_SX0 ) )
= $false )
| ( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[992]) ).
thf(999,plain,
( ( ( k04_buttercup10303 @ sK8_SX0 )
= $false )
| ( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[992]) ).
thf(1000,plain,
( ( ~ ( k04_buttercup10303 @ sK5_SX0 ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[993]) ).
thf(1001,plain,
( ( ~ ~ ( b48_buttercup10308 @ sK5_SX0 ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[993]) ).
thf(1002,plain,
( ( ~ ( k04_buttercup10303 @ sK6_SX0 ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[994]) ).
thf(1003,plain,
( ( ~ ~ ( b48_buttercup10305 @ sK6_SX0 ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[994]) ).
thf(1004,plain,
( ( ~ ( k04_buttercup10303 @ sK7_SX0 ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[995]) ).
thf(1005,plain,
( ( ~ ~ ( b48_buttercup10307 @ sK7_SX0 ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[995]) ).
thf(1006,plain,
( ( ( ~ ( b48_buttercup10305 @ sK4_SX0 ) )
= $false )
| ( ( ~ ( ~ ( k04_buttercup10303 @ sK4_SX0 )
| ( b48_buttercup10305 @ sK4_SX0 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[996]) ).
thf(1007,plain,
( ( ( k04_buttercup10303 @ sK4_SX0 )
= $false )
| ( ( ~ ( ~ ( k04_buttercup10303 @ sK4_SX0 )
| ( b48_buttercup10305 @ sK4_SX0 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[996]) ).
thf(1008,plain,
( ( ( ~ ( k04_buttercup10303 @ sK9_SX0 ) )
= $false )
| ( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[997]) ).
thf(1009,plain,
( ( ( b48_buttercup10305 @ sK9_SX0 )
= $false )
| ( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[997]) ).
thf(1010,plain,
( ( ( b48_buttercup10305 @ sK8_SX0 )
= $true )
| ( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[998]) ).
thf(1011,plain,
( ( ( ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $false )
| ( ( k04_buttercup10303 @ sK8_SX0 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[999]) ).
thf(1012,plain,
( ( k04_buttercup10303 @ sK5_SX0 )
= $true ),
inference(extcnf_not_neg,[status(thm)],[1000]) ).
thf(1013,plain,
( ( ~ ( b48_buttercup10308 @ sK5_SX0 ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[1001]) ).
thf(1014,plain,
( ( k04_buttercup10303 @ sK6_SX0 )
= $true ),
inference(extcnf_not_neg,[status(thm)],[1002]) ).
thf(1015,plain,
( ( ~ ( b48_buttercup10305 @ sK6_SX0 ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[1003]) ).
thf(1016,plain,
( ( k04_buttercup10303 @ sK7_SX0 )
= $true ),
inference(extcnf_not_neg,[status(thm)],[1004]) ).
thf(1017,plain,
( ( ~ ( b48_buttercup10307 @ sK7_SX0 ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[1005]) ).
thf(1018,plain,
( ( ( b48_buttercup10305 @ sK4_SX0 )
= $true )
| ( ( ~ ( ~ ( k04_buttercup10303 @ sK4_SX0 )
| ( b48_buttercup10305 @ sK4_SX0 ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[1006]) ).
thf(1019,plain,
( ( ( ~ ( k04_buttercup10303 @ sK4_SX0 )
| ( b48_buttercup10305 @ sK4_SX0 ) )
= $false )
| ( ( k04_buttercup10303 @ sK4_SX0 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[1007]) ).
thf(1020,plain,
( ( ( k04_buttercup10303 @ sK9_SX0 )
= $true )
| ( ( ~ ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[1008]) ).
thf(1021,plain,
( ( ( ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
= $false )
| ( ( b48_buttercup10305 @ sK9_SX0 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[1009]) ).
thf(1022,plain,
( ( ( ~ ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $false )
| ( ( b48_buttercup10305 @ sK8_SX0 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[1010]) ).
thf(1023,plain,
( ( ( ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $true )
| ( ( k04_buttercup10303 @ sK8_SX0 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[1011]) ).
thf(1024,plain,
( ( b48_buttercup10308 @ sK5_SX0 )
= $false ),
inference(extcnf_not_pos,[status(thm)],[1013]) ).
thf(1025,plain,
( ( b48_buttercup10305 @ sK6_SX0 )
= $false ),
inference(extcnf_not_pos,[status(thm)],[1015]) ).
thf(1026,plain,
( ( b48_buttercup10307 @ sK7_SX0 )
= $false ),
inference(extcnf_not_pos,[status(thm)],[1017]) ).
thf(1027,plain,
( ( ( ~ ( k04_buttercup10303 @ sK4_SX0 )
| ( b48_buttercup10305 @ sK4_SX0 ) )
= $false )
| ( ( b48_buttercup10305 @ sK4_SX0 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[1018]) ).
thf(1028,plain,
( ( ( ~ ( k04_buttercup10303 @ sK4_SX0 ) )
= $false )
| ( ( k04_buttercup10303 @ sK4_SX0 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[1019]) ).
thf(1029,plain,
( ( ( b48_buttercup10305 @ sK4_SX0 )
= $false )
| ( ( k04_buttercup10303 @ sK4_SX0 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[1019]) ).
thf(1030,plain,
( ( ( ~ ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
= $false )
| ( ( k04_buttercup10303 @ sK9_SX0 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[1020]) ).
thf(1031,plain,
( ( ( ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
= $true )
| ( ( b48_buttercup10305 @ sK9_SX0 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[1021]) ).
thf(1032,plain,
( ( ( ! [SX0: $i] :
~ ~ ( ~ ( k04_buttercup10303 @ SX0 )
| ~ ~ ( b48_buttercup10305 @ SX0 ) ) )
= $true )
| ( ( b48_buttercup10305 @ sK8_SX0 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[1022]) ).
thf(1033,plain,
! [SV7: $i] :
( ( ( ~ ~ ( ~ ( k04_buttercup10303 @ SV7 )
| ~ ~ ( b48_buttercup10305 @ SV7 ) ) )
= $true )
| ( ( k04_buttercup10303 @ sK8_SX0 )
= $false ) ),
inference(extcnf_forall_pos,[status(thm)],[1023]) ).
thf(1034,plain,
( ( ( ~ ( k04_buttercup10303 @ sK4_SX0 ) )
= $false )
| ( ( b48_buttercup10305 @ sK4_SX0 )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[1027]) ).
thf(1035,plain,
( ( ( b48_buttercup10305 @ sK4_SX0 )
= $false )
| ( ( b48_buttercup10305 @ sK4_SX0 )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[1027]) ).
thf(1036,plain,
( ( ( k04_buttercup10303 @ sK4_SX0 )
= $true )
| ( ( k04_buttercup10303 @ sK4_SX0 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[1028]) ).
thf(1037,plain,
( ( ( ! [SX0: $i] :
~ ~ ( ~ ( b48_buttercup10305 @ SX0 )
| ~ ~ ( k04_buttercup10303 @ SX0 ) ) )
= $true )
| ( ( k04_buttercup10303 @ sK9_SX0 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[1030]) ).
thf(1038,plain,
! [SV8: $i] :
( ( ( ~ ~ ( ~ ( b48_buttercup10305 @ SV8 )
| ~ ~ ( k04_buttercup10303 @ SV8 ) ) )
= $true )
| ( ( b48_buttercup10305 @ sK9_SX0 )
= $false ) ),
inference(extcnf_forall_pos,[status(thm)],[1031]) ).
thf(1039,plain,
! [SV9: $i] :
( ( ( ~ ~ ( ~ ( k04_buttercup10303 @ SV9 )
| ~ ~ ( b48_buttercup10305 @ SV9 ) ) )
= $true )
| ( ( b48_buttercup10305 @ sK8_SX0 )
= $true ) ),
inference(extcnf_forall_pos,[status(thm)],[1032]) ).
thf(1040,plain,
! [SV7: $i] :
( ( ( ~ ( ~ ( k04_buttercup10303 @ SV7 )
| ~ ~ ( b48_buttercup10305 @ SV7 ) ) )
= $false )
| ( ( k04_buttercup10303 @ sK8_SX0 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[1033]) ).
thf(1041,plain,
( ( ( k04_buttercup10303 @ sK4_SX0 )
= $true )
| ( ( b48_buttercup10305 @ sK4_SX0 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[1034]) ).
thf(1042,plain,
! [SV10: $i] :
( ( ( ~ ~ ( ~ ( b48_buttercup10305 @ SV10 )
| ~ ~ ( k04_buttercup10303 @ SV10 ) ) )
= $true )
| ( ( k04_buttercup10303 @ sK9_SX0 )
= $true ) ),
inference(extcnf_forall_pos,[status(thm)],[1037]) ).
thf(1043,plain,
! [SV8: $i] :
( ( ( ~ ( ~ ( b48_buttercup10305 @ SV8 )
| ~ ~ ( k04_buttercup10303 @ SV8 ) ) )
= $false )
| ( ( b48_buttercup10305 @ sK9_SX0 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[1038]) ).
thf(1044,plain,
! [SV9: $i] :
( ( ( ~ ( ~ ( k04_buttercup10303 @ SV9 )
| ~ ~ ( b48_buttercup10305 @ SV9 ) ) )
= $false )
| ( ( b48_buttercup10305 @ sK8_SX0 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[1039]) ).
thf(1045,plain,
! [SV7: $i] :
( ( ( ~ ( k04_buttercup10303 @ SV7 )
| ~ ~ ( b48_buttercup10305 @ SV7 ) )
= $true )
| ( ( k04_buttercup10303 @ sK8_SX0 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[1040]) ).
thf(1046,plain,
! [SV10: $i] :
( ( ( ~ ( ~ ( b48_buttercup10305 @ SV10 )
| ~ ~ ( k04_buttercup10303 @ SV10 ) ) )
= $false )
| ( ( k04_buttercup10303 @ sK9_SX0 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[1042]) ).
thf(1047,plain,
! [SV8: $i] :
( ( ( ~ ( b48_buttercup10305 @ SV8 )
| ~ ~ ( k04_buttercup10303 @ SV8 ) )
= $true )
| ( ( b48_buttercup10305 @ sK9_SX0 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[1043]) ).
thf(1048,plain,
! [SV9: $i] :
( ( ( ~ ( k04_buttercup10303 @ SV9 )
| ~ ~ ( b48_buttercup10305 @ SV9 ) )
= $true )
| ( ( b48_buttercup10305 @ sK8_SX0 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[1044]) ).
thf(1049,plain,
! [SV7: $i] :
( ( ( ~ ( k04_buttercup10303 @ SV7 ) )
= $true )
| ( ( ~ ~ ( b48_buttercup10305 @ SV7 ) )
= $true )
| ( ( k04_buttercup10303 @ sK8_SX0 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[1045]) ).
thf(1050,plain,
! [SV10: $i] :
( ( ( ~ ( b48_buttercup10305 @ SV10 )
| ~ ~ ( k04_buttercup10303 @ SV10 ) )
= $true )
| ( ( k04_buttercup10303 @ sK9_SX0 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[1046]) ).
thf(1051,plain,
! [SV8: $i] :
( ( ( ~ ( b48_buttercup10305 @ SV8 ) )
= $true )
| ( ( ~ ~ ( k04_buttercup10303 @ SV8 ) )
= $true )
| ( ( b48_buttercup10305 @ sK9_SX0 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[1047]) ).
thf(1052,plain,
! [SV9: $i] :
( ( ( ~ ( k04_buttercup10303 @ SV9 ) )
= $true )
| ( ( ~ ~ ( b48_buttercup10305 @ SV9 ) )
= $true )
| ( ( b48_buttercup10305 @ sK8_SX0 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[1048]) ).
thf(1053,plain,
! [SV7: $i] :
( ( ( k04_buttercup10303 @ SV7 )
= $false )
| ( ( ~ ~ ( b48_buttercup10305 @ SV7 ) )
= $true )
| ( ( k04_buttercup10303 @ sK8_SX0 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[1049]) ).
thf(1054,plain,
! [SV10: $i] :
( ( ( ~ ( b48_buttercup10305 @ SV10 ) )
= $true )
| ( ( ~ ~ ( k04_buttercup10303 @ SV10 ) )
= $true )
| ( ( k04_buttercup10303 @ sK9_SX0 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[1050]) ).
thf(1055,plain,
! [SV8: $i] :
( ( ( b48_buttercup10305 @ SV8 )
= $false )
| ( ( ~ ~ ( k04_buttercup10303 @ SV8 ) )
= $true )
| ( ( b48_buttercup10305 @ sK9_SX0 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[1051]) ).
thf(1056,plain,
! [SV9: $i] :
( ( ( k04_buttercup10303 @ SV9 )
= $false )
| ( ( ~ ~ ( b48_buttercup10305 @ SV9 ) )
= $true )
| ( ( b48_buttercup10305 @ sK8_SX0 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[1052]) ).
thf(1057,plain,
! [SV7: $i] :
( ( ( ~ ( b48_buttercup10305 @ SV7 ) )
= $false )
| ( ( k04_buttercup10303 @ SV7 )
= $false )
| ( ( k04_buttercup10303 @ sK8_SX0 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[1053]) ).
thf(1058,plain,
! [SV10: $i] :
( ( ( b48_buttercup10305 @ SV10 )
= $false )
| ( ( ~ ~ ( k04_buttercup10303 @ SV10 ) )
= $true )
| ( ( k04_buttercup10303 @ sK9_SX0 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[1054]) ).
thf(1059,plain,
! [SV8: $i] :
( ( ( ~ ( k04_buttercup10303 @ SV8 ) )
= $false )
| ( ( b48_buttercup10305 @ SV8 )
= $false )
| ( ( b48_buttercup10305 @ sK9_SX0 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[1055]) ).
thf(1060,plain,
! [SV9: $i] :
( ( ( ~ ( b48_buttercup10305 @ SV9 ) )
= $false )
| ( ( k04_buttercup10303 @ SV9 )
= $false )
| ( ( b48_buttercup10305 @ sK8_SX0 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[1056]) ).
thf(1061,plain,
! [SV7: $i] :
( ( ( b48_buttercup10305 @ SV7 )
= $true )
| ( ( k04_buttercup10303 @ SV7 )
= $false )
| ( ( k04_buttercup10303 @ sK8_SX0 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[1057]) ).
thf(1062,plain,
! [SV10: $i] :
( ( ( ~ ( k04_buttercup10303 @ SV10 ) )
= $false )
| ( ( b48_buttercup10305 @ SV10 )
= $false )
| ( ( k04_buttercup10303 @ sK9_SX0 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[1058]) ).
thf(1063,plain,
! [SV8: $i] :
( ( ( k04_buttercup10303 @ SV8 )
= $true )
| ( ( b48_buttercup10305 @ SV8 )
= $false )
| ( ( b48_buttercup10305 @ sK9_SX0 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[1059]) ).
thf(1064,plain,
! [SV9: $i] :
( ( ( b48_buttercup10305 @ SV9 )
= $true )
| ( ( k04_buttercup10303 @ SV9 )
= $false )
| ( ( b48_buttercup10305 @ sK8_SX0 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[1060]) ).
thf(1065,plain,
! [SV10: $i] :
( ( ( k04_buttercup10303 @ SV10 )
= $true )
| ( ( b48_buttercup10305 @ SV10 )
= $false )
| ( ( k04_buttercup10303 @ sK9_SX0 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[1062]) ).
thf(1066,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[938,1065,1064,1063,1061,1041,1036,1035,1029,1026,1025,1024,1016,1014,1012,989,988,986,984,982,970,969,948,940,939]) ).
thf(1067,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[1066]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO580+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.18 % Computer : n003.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Oct 6 17:44:25 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.25/0.40 ....
% 1.25/0.40
% 1.25/0.40 No.of.Axioms: 8
% 1.25/0.40
% 1.25/0.40 Length.of.Defs: 0
% 1.25/0.40
% 1.25/0.40 Contains.Choice.Funs: false
% 1.25/0.40 .........
% 1.25/0.40
% 1.25/0.40 ********************************
% 1.25/0.40 * All subproblems solved! *
% 1.25/0.40 ********************************
% 1.25/0.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:8,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:299,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:1066,loop_count:0,foatp_calls:1,translation:fof_full)
% 1.25/0.40
% 1.25/0.40 %**** Beginning of derivation protocol ****
% 1.25/0.40 % SZS output start CNFRefutation
% See solution above
% 1.25/0.40
% 1.25/0.40 %**** End of derivation protocol ****
% 1.25/0.40 %**** no. of clauses in derivation: 190 ****
% 1.25/0.40 %**** clause counter: 1066 ****
% 1.25/0.40
% 1.25/0.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:8,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:299,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:1066,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------