%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO581+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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 : Tue Sep 29 02:31:43 PM UTC 2026
% Result : CounterSatisfiable 0.23s 0.39s
% Output : Saturation 0.74s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u3091,negated_conjecture,
( ~ b48_buttercup10305(X4)
| k04_buttercup10303(X4) ) ).
cnf(u3108,negated_conjecture,
~ b48_buttercup10305(sK481) ).
cnf(u3113,negated_conjecture,
k04_buttercup10303(sK481) ).
cnf(u3118,axiom,
( ~ b48_buttercup10421(X2)
| ~ k04_buttercup10419(X2) ) ).
cnf(u3121,axiom,
~ sP23 ).
cnf(u3129,axiom,
~ sP22 ).
cnf(u3187,axiom,
( ~ b48_buttercup10102(X2)
| ~ k04_buttercup10100(X2) ) ).
cnf(u3190,axiom,
~ sP21 ).
cnf(u3198,axiom,
~ sP20 ).
cnf(u3256,axiom,
( ~ b48_buttercup10289(X2)
| ~ k04_buttercup10282(X2) ) ).
cnf(u3259,axiom,
~ sP19 ).
cnf(u3267,axiom,
~ sP18 ).
cnf(u3325,axiom,
( ~ b48_buttercup10208(X2)
| ~ k04_buttercup10204(X2) ) ).
cnf(u3328,axiom,
~ sP17 ).
cnf(u3336,axiom,
~ sP16 ).
cnf(u3394,axiom,
( ~ b48_buttercup10214(X2)
| ~ k04_buttercup10204(X2) ) ).
cnf(u3397,axiom,
~ sP15 ).
cnf(u3405,axiom,
~ sP14 ).
cnf(u3463,axiom,
( ~ b48_buttercup10110(X2)
| ~ k04_buttercup10100(X2) ) ).
cnf(u3466,axiom,
~ sP13 ).
cnf(u3474,axiom,
~ sP12 ).
cnf(u3532,axiom,
( ~ b48_buttercup10104(X2)
| ~ k04_buttercup10100(X2) ) ).
cnf(u3535,axiom,
~ sP11 ).
cnf(u3543,axiom,
~ sP10 ).
cnf(u3601,axiom,
( ~ b48_buttercup10107(X2)
| ~ k04_buttercup10100(X2) ) ).
cnf(u3604,axiom,
~ sP9 ).
cnf(u3612,axiom,
~ sP8 ).
cnf(u3670,axiom,
( ~ b48_buttercup10108(X2)
| ~ k04_buttercup10100(X2) ) ).
cnf(u3673,axiom,
~ sP7 ).
cnf(u3681,axiom,
~ sP6 ).
cnf(u3739,axiom,
( ~ b48_buttercup10109(X2)
| ~ k04_buttercup10619(X2) ) ).
cnf(u3742,axiom,
~ sP5 ).
cnf(u3750,axiom,
~ sP4 ).
cnf(u3808,axiom,
( ~ b48_buttercup10111(X2)
| ~ k04_buttercup10619(X2) ) ).
cnf(u3811,axiom,
~ sP3 ).
cnf(u3819,axiom,
~ sP2 ).
cnf(u3877,axiom,
( ~ b48_buttercup10029(X2)
| ~ k04_buttercup10026(X2) ) ).
cnf(u3880,axiom,
~ sP1 ).
cnf(u3888,axiom,
~ sP0 ).
cnf(u4302,axiom,
k04_buttercup10639(sK323) ).
cnf(u2680,axiom,
( ~ k04_buttercup10611(X0)
| b48_buttercup10609(X0) ) ).
cnf(u4842,axiom,
b48_buttercup10217(sK296) ).
cnf(u4204,axiom,
k04_buttercup10012(sK121) ).
cnf(u2903,axiom,
k04_buttercup10347(sK305) ).
cnf(u4651,axiom,
k04_buttercup10369(sK324) ).
cnf(u4897,axiom,
k04_buttercup10012(sK341) ).
cnf(u2917,axiom,
b48_buttercup10442(sK319) ).
cnf(u5123,axiom,
k04_buttercup10012(sK473) ).
cnf(u4192,axiom,
k04_buttercup10012(sK160) ).
cnf(u4189,axiom,
k04_buttercup10012(sK278) ).
cnf(u4655,axiom,
k04_buttercup10619(sK434) ).
cnf(u2850,axiom,
k04_buttercup10482(sK252) ).
cnf(u2504,axiom,
( ~ b48_buttercup10143(X0)
| k04_buttercup10147(X0) ) ).
cnf(u4494,axiom,
k04_buttercup10449(sK361) ).
cnf(u4177,axiom,
k04_buttercup10012(sK215) ).
cnf(u2036,axiom,
( ~ k04_buttercup10622(X0)
| k04_buttercup10619(X0) ) ).
cnf(u2120,axiom,
( ~ k04_buttercup10626(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2596,axiom,
( ~ b48_buttercup10326(X0)
| k04_buttercup10329(X0) ) ).
cnf(u4636,axiom,
b48_buttercup10381(sK240) ).
cnf(u2583,axiom,
k04_buttercup10364(sK133) ).
cnf(u4768,axiom,
b48_buttercup10405(sK259) ).
cnf(u2048,axiom,
( ~ k04_buttercup10252(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2402,axiom,
~ b48_buttercup10109(sK84) ).
cnf(u2948,axiom,
b48_buttercup10068(sK350) ).
cnf(u2802,axiom,
k04_buttercup10622(sK204) ).
cnf(u2233,axiom,
( ~ b48_buttercup10466(X0)
| k04_buttercup10464(X0) ) ).
cnf(u4298,axiom,
k04_buttercup10643(sK460) ).
cnf(u3017,axiom,
b48_buttercup10133(sK419) ).
cnf(u2564,axiom,
( ~ b48_buttercup10092(X0)
| k04_buttercup10096(X0) ) ).
cnf(u2161,axiom,
( ~ b48_buttercup10374(X0)
| b48_buttercup10367(X0) ) ).
cnf(u3983,axiom,
k04_buttercup10234(sK195) ).
cnf(u2580,axiom,
b48_buttercup10440(sK134) ).
cnf(u2620,axiom,
( ~ k04_buttercup10053(X0)
| b48_buttercup10029(X0) ) ).
cnf(u2899,axiom,
k04_buttercup10453(sK301) ).
cnf(u2624,axiom,
( ~ k04_buttercup10453(X0)
| b48_buttercup10451(X0) ) ).
cnf(u3047,axiom,
b48_buttercup10344(sK449) ).
cnf(u4423,axiom,
k04_buttercup10635(sK462) ).
cnf(u2000,axiom,
( ~ k04_buttercup10342(X0)
| k04_buttercup10337(X0) ) ).
cnf(u2222,axiom,
( ~ b48_buttercup10227(X0)
| k04_buttercup10225(X0) ) ).
cnf(u4354,axiom,
k04_buttercup10296(sK452) ).
cnf(u2975,axiom,
b48_buttercup10398(sK377) ).
cnf(u2282,axiom,
( ~ k04_buttercup10389(X0)
| b48_buttercup10386(X0) ) ).
cnf(u4823,axiom,
k04_buttercup10181(sK477) ).
cnf(u2862,axiom,
k04_buttercup10135(sK264) ).
cnf(u4539,axiom,
b48_buttercup10143(sK246) ).
cnf(u2079,axiom,
( ~ k04_buttercup10181(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4358,axiom,
k04_buttercup10293(sK453) ).
cnf(u2565,axiom,
( ~ k04_buttercup10097(X0)
| b48_buttercup10381(X0) ) ).
cnf(u2922,axiom,
b48_buttercup10367(sK324) ).
cnf(u2444,axiom,
~ k04_buttercup10516(sK92) ).
cnf(u2132,axiom,
( ~ b48_buttercup10229(X0)
| b48_buttercup10222(X0) ) ).
cnf(u2625,axiom,
( ~ b48_buttercup10451(X0)
| k04_buttercup10453(X0) ) ).
cnf(u2060,axiom,
( ~ k04_buttercup10026(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2414,axiom,
( ~ k04_buttercup10333(X0)
| b48_buttercup10332(X0) ) ).
cnf(u2814,axiom,
k04_buttercup10517(sK216) ).
cnf(u4596,axiom,
b48_buttercup10604(sK236) ).
cnf(u4646,axiom,
b48_buttercup10367(sK199) ).
cnf(u2117,axiom,
( ~ k04_buttercup10608(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4645,axiom,
b48_buttercup10367(sK183) ).
cnf(u2742,axiom,
~ b48_buttercup10422(sK161) ).
cnf(u3020,axiom,
b48_buttercup10231(sK422) ).
cnf(u4777,axiom,
b48_buttercup10130(sK143) ).
cnf(u2173,axiom,
( ~ b48_buttercup10154(X0)
| b48_buttercup10150(X0) ) ).
cnf(u4212,axiom,
k04_buttercup10012(sK184) ).
cnf(u2177,axiom,
( ~ b48_buttercup10160(X0)
| b48_buttercup10150(X0) ) ).
cnf(u4584,axiom,
b48_buttercup10054(sK261) ).
cnf(u2434,axiom,
k04_buttercup10064(sK89) ).
cnf(u4633,axiom,
k04_buttercup10096(sK386) ).
cnf(u4781,axiom,
k04_buttercup10132(sK418) ).
cnf(u2971,axiom,
b48_buttercup10154(sK373) ).
cnf(u4766,axiom,
k04_buttercup10404(sK393) ).
cnf(u4200,axiom,
k04_buttercup10012(sK234) ).
cnf(u4197,axiom,
k04_buttercup10012(sK222) ).
cnf(u4663,axiom,
b48_buttercup10322(sK253) ).
cnf(u4011,axiom,
k04_buttercup10619(sK122) ).
cnf(u4069,axiom,
k04_buttercup10012(sK263) ).
cnf(u2934,axiom,
b48_buttercup10075(sK336) ).
cnf(u4055,axiom,
k04_buttercup10012(sK139) ).
cnf(u4185,axiom,
k04_buttercup10012(sK269) ).
cnf(u2044,axiom,
( ~ k04_buttercup10221(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2637,axiom,
~ b48_buttercup10574(sK142) ).
cnf(u4644,axiom,
b48_buttercup10542(sK270) ).
cnf(u4318,axiom,
b48_buttercup10150(sK226) ).
cnf(u4513,axiom,
k04_buttercup10559(sK388) ).
cnf(u2936,axiom,
b48_buttercup10474(sK338) ).
cnf(u4170,axiom,
k04_buttercup10012(sK207) ).
cnf(u4548,axiom,
k04_buttercup10012(sK346) ).
cnf(u4460,axiom,
k04_buttercup10347(sK476) ).
cnf(u4592,axiom,
k04_buttercup10057(sK461) ).
cnf(u4174,axiom,
k04_buttercup10012(sK237) ).
cnf(u4306,axiom,
k04_buttercup10252(sK401) ).
cnf(u4593,axiom,
k04_buttercup10057(sK468) ).
cnf(u4060,axiom,
k04_buttercup10012(sK305) ).
cnf(u2008,axiom,
( ~ k04_buttercup10546(X0)
| k04_buttercup10544(X0) ) ).
cnf(u2760,axiom,
k04_buttercup10419(sK168) ).
cnf(u5036,axiom,
k04_buttercup10012(sK412) ).
cnf(u4193,axiom,
k04_buttercup10012(sK235) ).
cnf(u5253,axiom,
k04_buttercup10012(sK464) ).
cnf(u4419,axiom,
k04_buttercup10337(sK449) ).
cnf(u4066,axiom,
k04_buttercup10012(sK275) ).
cnf(u3052,axiom,
b48_buttercup10119(sK454) ).
cnf(u4366,axiom,
b48_buttercup10493(sK232) ).
cnf(u5024,axiom,
k04_buttercup10012(sK407) ).
cnf(u2304,axiom,
k04_buttercup10486(sK47) ).
cnf(u2215,axiom,
~ b48_buttercup10154(sK27) ).
cnf(u4088,axiom,
k04_buttercup10012(sK240) ).
cnf(u3058,axiom,
b48_buttercup10642(sK460) ).
cnf(u4182,axiom,
k04_buttercup10012(sK295) ).
cnf(u4016,axiom,
k04_buttercup10012(sK175) ).
cnf(u1997,axiom,
( ~ k04_buttercup10051(X0)
| k04_buttercup10048(X0) ) ).
cnf(u2820,axiom,
k04_buttercup10593(sK222) ).
cnf(u2674,axiom,
k04_buttercup10172(sK150) ).
cnf(u2952,axiom,
b48_buttercup10386(sK354) ).
cnf(u2105,axiom,
( ~ k04_buttercup10516(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2643,axiom,
( ~ b48_buttercup10405(X0)
| k04_buttercup10406(X0) ) ).
cnf(u2889,axiom,
k04_buttercup10298(sK291) ).
cnf(u2791,axiom,
k04_buttercup10506(sK193) ).
cnf(u4167,axiom,
k04_buttercup10012(sK123) ).
cnf(u4299,axiom,
b48_buttercup10640(sK294) ).
cnf(u2719,axiom,
~ b48_buttercup10344(sK158) ).
cnf(u2538,axiom,
( ~ b48_buttercup10604(X0)
| k04_buttercup10602(X0) ) ).
cnf(u2094,axiom,
( ~ k04_buttercup10437(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4283,axiom,
b48_buttercup10299(sK291) ).
cnf(u2847,axiom,
k04_buttercup10400(sK249) ).
cnf(u2226,axiom,
( ~ k04_buttercup10234(X0)
| b48_buttercup10231(X0) ) ).
cnf(u4303,axiom,
b48_buttercup10636(sK227) ).
cnf(u2154,axiom,
( ~ b48_buttercup10167(X0)
| b48_buttercup10161(X0) ) ).
cnf(u2700,axiom,
k04_buttercup10095(sK154) ).
cnf(u4969,axiom,
b48_buttercup10427(sK271) ).
cnf(u4411,axiom,
b48_buttercup10353(sK303) ).
cnf(u2985,axiom,
b48_buttercup10313(sK387) ).
cnf(u2388,axiom,
k04_buttercup10100(sK78) ).
cnf(u2030,axiom,
( ~ k04_buttercup10061(X0)
| k04_buttercup10057(X0) ) ).
cnf(u5186,axiom,
b48_buttercup10417(sK465) ).
cnf(u5086,axiom,
k04_buttercup10012(sK396) ).
cnf(u4716,axiom,
k04_buttercup10053(sK432) ).
cnf(u2316,axiom,
( ~ b48_buttercup10549(X0)
| k04_buttercup10551(X0) ) ).
cnf(u2211,axiom,
( ~ b48_buttercup10531(X0)
| k04_buttercup10535(X0) ) ).
cnf(u5245,axiom,
k04_buttercup10012(sK342) ).
cnf(u4973,axiom,
k04_buttercup10504(sK307) ).
cnf(u4859,axiom,
b48_buttercup10474(sK47) ).
cnf(u2139,axiom,
( ~ b48_buttercup10344(X0)
| b48_buttercup10334(X0) ) ).
cnf(u3070,axiom,
b48_buttercup10227(sK472) ).
cnf(u2287,axiom,
( ~ b48_buttercup10383(X0)
| k04_buttercup10382(X0) ) ).
cnf(u4025,axiom,
k04_buttercup10012(sK300) ).
cnf(u2773,axiom,
k04_buttercup10184(sK175) ).
cnf(u2793,axiom,
k04_buttercup10236(sK195) ).
cnf(u2686,axiom,
( ~ b48_buttercup10217(X0)
| k04_buttercup10219(X0) ) ).
cnf(u4468,axiom,
b48_buttercup10421(sK216) ).
cnf(u3969,axiom,
k04_buttercup10449(sK103) ).
cnf(u2614,axiom,
( ~ b48_buttercup10046(X0)
| k04_buttercup10048(X0) ) ).
cnf(u2892,axiom,
k04_buttercup10641(sK294) ).
cnf(u2787,axiom,
k04_buttercup10639(sK189) ).
cnf(u2268,axiom,
~ b48_buttercup10022(sK42) ).
cnf(u5303,axiom,
k04_buttercup10012(sK467) ).
cnf(u4525,axiom,
k04_buttercup10139(sK406) ).
cnf(u2829,axiom,
k04_buttercup10397(sK231) ).
cnf(u2715,axiom,
k04_buttercup10190(sK157) ).
cnf(u2961,axiom,
b48_buttercup10269(sK363) ).
cnf(u5222,axiom,
k04_buttercup10012(sK336) ).
cnf(u2550,axiom,
k04_buttercup10622(sK122) ).
cnf(u4653,axiom,
k04_buttercup10369(sK342) ).
cnf(u2843,axiom,
k04_buttercup10053(sK245) ).
cnf(u2997,axiom,
b48_buttercup10121(sK399) ).
cnf(u4638,axiom,
b48_buttercup10542(sK269) ).
cnf(u4272,axiom,
b48_buttercup10054(sK352) ).
cnf(u2253,axiom,
( ~ b48_buttercup10076(X0)
| k04_buttercup10079(X0) ) ).
cnf(u2166,axiom,
( ~ b48_buttercup10320(X0)
| b48_buttercup10313(X0) ) ).
cnf(u5158,axiom,
k04_buttercup10012(sK448) ).
cnf(u2298,axiom,
( ~ k04_buttercup10492(X0)
| b48_buttercup10490(X0) ) ).
cnf(u4626,axiom,
k04_buttercup10012(sK475) ).
cnf(u3078,axiom,
b48_buttercup10479(sK480) ).
cnf(u4254,axiom,
b48_buttercup10367(sK342) ).
cnf(u5082,axiom,
k04_buttercup10012(sK395) ).
cnf(u4788,axiom,
k04_buttercup10012(sK389) ).
cnf(u4883,axiom,
k04_buttercup10470(sK355) ).
cnf(u2039,axiom,
( ~ k04_buttercup10517(X0)
| k04_buttercup10516(X0) ) ).
cnf(u4562,axiom,
b48_buttercup10161(sK148) ).
cnf(u2953,axiom,
b48_buttercup10469(sK355) ).
cnf(u4464,axiom,
k04_buttercup10064(sK332) ).
cnf(u4916,axiom,
b48_buttercup10186(sK50) ).
cnf(u4178,axiom,
k04_buttercup10012(sK91) ).
cnf(u4054,axiom,
k04_buttercup10012(sK88) ).
cnf(u4175,axiom,
k04_buttercup10012(sK192) ).
cnf(u5184,axiom,
b48_buttercup10417(sK440) ).
cnf(u2973,axiom,
b48_buttercup10159(sK375) ).
cnf(u3991,axiom,
k04_buttercup10635(sK189) ).
cnf(u4695,axiom,
b48_buttercup10046(sK179) ).
cnf(u4163,axiom,
k04_buttercup10012(sK197) ).
cnf(u4908,axiom,
b48_buttercup10496(sK237) ).
cnf(u4820,axiom,
k04_buttercup10204(sK443) ).
cnf(u4013,axiom,
k04_buttercup10504(sK193) ).
cnf(u2983,axiom,
b48_buttercup10604(sK385) ).
cnf(u2710,axiom,
~ b48_buttercup10261(sK155) ).
cnf(u4491,axiom,
k04_buttercup10555(sK441) ).
cnf(u2038,axiom,
( ~ k04_buttercup10142(X0)
| k04_buttercup10139(X0) ) ).
cnf(u3982,axiom,
k04_buttercup10593(sK236) ).
cnf(u5196,axiom,
k04_buttercup10012(sK361) ).
cnf(u2087,axiom,
( ~ k04_buttercup10397(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4292,axiom,
k04_buttercup10303(sK457) ).
cnf(u2930,axiom,
b48_buttercup10070(sK332) ).
cnf(u4495,axiom,
k04_buttercup10464(sK455) ).
cnf(u4426,axiom,
b48_buttercup10632(sK189) ).
cnf(u5309,axiom,
k04_buttercup10012(sK416) ).
cnf(u2068,axiom,
( ~ k04_buttercup10095(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2200,axiom,
( ~ k04_buttercup10643(X0)
| b48_buttercup10642(X0) ) ).
cnf(u5011,axiom,
~ k04_buttercup10026(sK432) ).
cnf(u4647,axiom,
b48_buttercup10367(sK201) ).
cnf(u2663,axiom,
( ~ b48_buttercup10170(X0)
| k04_buttercup10172(X0) ) ).
cnf(u5009,axiom,
~ k04_buttercup10619(sK458) ).
cnf(u2128,axiom,
( ~ b48_buttercup10307(X0)
| b48_buttercup10300(X0) ) ).
cnf(u2551,axiom,
( ~ b48_buttercup10110(X0)
| k04_buttercup10622(X0) ) ).
cnf(u4571,axiom,
k04_buttercup10012(sK351) ).
cnf(u2591,axiom,
~ b48_buttercup10362(sK136) ).
cnf(u2482,axiom,
( ~ k04_buttercup10559(X0)
| b48_buttercup10562(X0) ) ).
cnf(u3028,axiom,
b48_buttercup10021(sK430) ).
cnf(u3988,axiom,
k04_buttercup10293(sK288) ).
cnf(u2410,axiom,
( ~ b48_buttercup10353(X0)
| k04_buttercup10356(X0) ) ).
cnf(u2185,axiom,
( ~ b48_buttercup10562(X0)
| b48_buttercup10552(X0) ) ).
cnf(u4155,axiom,
k04_buttercup10012(sK33) ).
cnf(u2098,axiom,
( ~ k04_buttercup10473(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2644,axiom,
~ b48_buttercup10133(sK143) ).
cnf(u4148,axiom,
k04_buttercup10012(sK282) ).
cnf(u4063,axiom,
k04_buttercup10012(sK43) ).
cnf(u4280,axiom,
b48_buttercup10515(sK358) ).
cnf(u2313,axiom,
k04_buttercup10190(sK50) ).
cnf(u2979,axiom,
b48_buttercup10082(sK381) ).
cnf(u4615,axiom,
k04_buttercup10626(sK341) ).
cnf(u2704,axiom,
( ~ k04_buttercup10371(X0)
| b48_buttercup10370(X0) ) ).
cnf(u4989,axiom,
~ k04_buttercup10204(sK348) ).
cnf(u2302,axiom,
( ~ b48_buttercup10487(X0)
| k04_buttercup10486(X0) ) ).
cnf(u3055,axiom,
b48_buttercup10300(sK457) ).
cnf(u2083,axiom,
( ~ k04_buttercup10382(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4284,axiom,
k04_buttercup10298(sK379) ).
cnf(u4010,axiom,
k04_buttercup10619(sK121) ).
cnf(u4265,axiom,
b48_buttercup10563(sK404) ).
cnf(u4731,axiom,
b48_buttercup10446(sK34) ).
cnf(u2942,axiom,
b48_buttercup10370(sK344) ).
cnf(u2159,axiom,
( ~ b48_buttercup10604(X0)
| b48_buttercup10589(X0) ) ).
cnf(u2193,axiom,
( ~ k04_buttercup10298(X0)
| b48_buttercup10299(X0) ) ).
cnf(u2047,axiom,
( ~ k04_buttercup10244(X0)
| k04_buttercup10012(X0) ) ).
cnf(u5096,axiom,
k04_buttercup10012(sK338) ).
cnf(u2645,axiom,
k04_buttercup10132(sK143) ).
cnf(u3002,axiom,
b48_buttercup10574(sK404) ).
cnf(u2777,axiom,
k04_buttercup10049(sK179) ).
cnf(u5099,axiom,
k04_buttercup10012(sK339) ).
cnf(u4269,axiom,
b48_buttercup10150(sK375) ).
cnf(u2212,axiom,
~ b48_buttercup10156(sK26) ).
cnf(u2705,axiom,
( ~ b48_buttercup10370(X0)
| k04_buttercup10371(X0) ) ).
cnf(u2739,axiom,
( ~ b48_buttercup10575(X0)
| k04_buttercup10578(X0) ) ).
cnf(u2618,axiom,
( ~ b48_buttercup10050(X0)
| k04_buttercup10051(X0) ) ).
cnf(u2140,axiom,
( ~ b48_buttercup10348(X0)
| b48_buttercup10334(X0) ) ).
cnf(u2547,axiom,
( ~ k04_buttercup10626(X0)
| b48_buttercup10624(X0) ) ).
cnf(u4068,axiom,
k04_buttercup10012(sK262) ).
cnf(u2587,axiom,
k04_buttercup10364(sK135) ).
cnf(u2494,axiom,
( ~ b48_buttercup10085(X0)
| k04_buttercup10139(X0) ) ).
cnf(u2833,axiom,
k04_buttercup10567(sK235) ).
cnf(u2475,axiom,
~ b48_buttercup10454(sK103) ).
cnf(u2766,axiom,
b48_buttercup10417(sK173) ).
cnf(u4767,axiom,
k04_buttercup10449(sK455) ).
cnf(u2422,axiom,
~ b48_buttercup10075(sK86) ).
cnf(u2197,axiom,
~ b48_buttercup10307(sK25) ).
cnf(u2694,axiom,
( ~ b48_buttercup10474(X0)
| k04_buttercup10477(X0) ) ).
cnf(u4144,axiom,
k04_buttercup10012(sK171) ).
cnf(u2125,axiom,
( ~ b48_buttercup10050(X0)
| b48_buttercup10046(X0) ) ).
cnf(u4499,axiom,
k04_buttercup10462(sK359) ).
cnf(u4446,axiom,
k04_buttercup10012(sK401) ).
cnf(u3051,axiom,
b48_buttercup10291(sK453) ).
cnf(u4959,axiom,
b48_buttercup10034(sK276) ).
cnf(u2246,axiom,
( ~ k04_buttercup10397(X0)
| b48_buttercup10394(X0) ) ).
cnf(u4019,axiom,
k04_buttercup10012(sK157) ).
cnf(u4503,axiom,
b48_buttercup10563(sK160) ).
cnf(u4720,axiom,
k04_buttercup10213(sK467) ).
cnf(u4718,axiom,
b48_buttercup10210(sK300) ).
cnf(u4091,axiom,
k04_buttercup10012(sK84) ).
cnf(u5183,axiom,
k04_buttercup10012(sK405) ).
cnf(u4545,axiom,
b48_buttercup10589(sK221) ).
cnf(u2886,axiom,
k04_buttercup10296(sK288) ).
cnf(u4877,axiom,
k04_buttercup10473(sK339) ).
cnf(u5189,axiom,
b48_buttercup10446(sK362) ).
cnf(u1996,axiom,
( ~ k04_buttercup10049(X0)
| k04_buttercup10048(X0) ) ).
cnf(u4250,axiom,
b48_buttercup10115(sK398) ).
cnf(u4579,axiom,
b48_buttercup10054(sK89) ).
cnf(u4890,axiom,
k04_buttercup10619(sK438) ).
cnf(u2857,axiom,
k04_buttercup10406(sK259) ).
cnf(u2855,axiom,
k04_buttercup10089(sK257) ).
cnf(u4363,axiom,
b48_buttercup10072(sK194) ).
cnf(u4665,axiom,
k04_buttercup10325(sK403) ).
cnf(u4725,axiom,
k04_buttercup10453(sK470) ).
cnf(u3065,axiom,
b48_buttercup10210(sK467) ).
cnf(u2025,axiom,
( ~ k04_buttercup10033(X0)
| k04_buttercup10026(X0) ) ).
cnf(u5137,axiom,
k04_buttercup10012(sK399) ).
cnf(u3080,negated_conjecture,
k04_buttercup10303(sK483) ).
cnf(u5067,axiom,
k04_buttercup10012(sK306) ).
cnf(u5012,axiom,
~ k04_buttercup10026(sK245) ).
cnf(u2295,axiom,
( ~ b48_buttercup10072(X0)
| k04_buttercup10074(X0) ) ).
cnf(u4939,axiom,
b48_buttercup10121(sK250) ).
cnf(u2072,axiom,
( ~ k04_buttercup10132(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4277,axiom,
b48_buttercup10552(sK390) ).
cnf(u4040,axiom,
k04_buttercup10012(sK25) ).
cnf(u5179,axiom,
k04_buttercup10012(sK431) ).
cnf(u3010,axiom,
b48_buttercup10402(sK412) ).
cnf(u2423,axiom,
k04_buttercup10064(sK86) ).
cnf(u3968,axiom,
k04_buttercup10449(sK35) ).
cnf(u5255,axiom,
k04_buttercup10012(sK463) ).
cnf(u2900,axiom,
k04_buttercup10190(sK302) ).
cnf(u2869,axiom,
k04_buttercup10430(sK271) ).
cnf(u3032,axiom,
b48_buttercup10102(sK434) ).
cnf(u4536,axiom,
k04_buttercup10012(sK356) ).
cnf(u4141,axiom,
k04_buttercup10012(sK167) ).
cnf(u2057,axiom,
( ~ k04_buttercup10337(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2723,axiom,
( ~ b48_buttercup10115(X0)
| k04_buttercup10117(X0) ) ).
cnf(u2969,axiom,
b48_buttercup10150(sK371) ).
cnf(u4733,axiom,
b48_buttercup10446(sK103) ).
cnf(u4152,axiom,
k04_buttercup10012(sK30) ).
cnf(u2799,axiom,
k04_buttercup10373(sK201) ).
cnf(u2851,axiom,
k04_buttercup10325(sK253) ).
cnf(u4544,axiom,
b48_buttercup10589(sK222) ).
cnf(u2728,axiom,
( ~ b48_buttercup10120(X0)
| k04_buttercup10117(X0) ) ).
cnf(u2174,axiom,
( ~ b48_buttercup10156(X0)
| b48_buttercup10150(X0) ) ).
cnf(u2927,axiom,
b48_buttercup10173(sK329) ).
cnf(u2178,axiom,
( ~ b48_buttercup10058(X0)
| b48_buttercup10054(X0) ) ).
cnf(u4706,axiom,
k04_buttercup10049(sK463) ).
cnf(u4156,axiom,
k04_buttercup10012(sK34) ).
cnf(u4662,axiom,
k04_buttercup10012(sK458) ).
cnf(u4137,axiom,
k04_buttercup10012(sK259) ).
cnf(u2234,axiom,
~ b48_buttercup10467(sK32) ).
cnf(u2521,axiom,
~ b48_buttercup10158(sK116) ).
cnf(u4756,axiom,
k04_buttercup10012(sK410) ).
cnf(u5275,axiom,
b48_buttercup10446(sK455) ).
cnf(u4968,axiom,
k04_buttercup10012(sK421) ).
cnf(u4710,axiom,
k04_buttercup10012(sK308) ).
cnf(u2874,axiom,
k04_buttercup10028(sK276) ).
cnf(u2649,axiom,
( ~ b48_buttercup10134(X0)
| k04_buttercup10132(X0) ) ).
cnf(u2291,axiom,
( ~ b48_buttercup10291(X0)
| k04_buttercup10293(X0) ) ).
cnf(u5008,axiom,
k04_buttercup10204(sK467) ).
cnf(u2528,axiom,
k04_buttercup10153(sK118) ).
cnf(u5134,axiom,
k04_buttercup10012(sK456) ).
cnf(u4273,axiom,
b48_buttercup10054(sK350) ).
cnf(u4126,axiom,
k04_buttercup10012(sK203) ).
cnf(u2219,axiom,
( ~ b48_buttercup10150(X0)
| k04_buttercup10153(X0) ) ).
cnf(u3022,axiom,
b48_buttercup10548(sK424) ).
cnf(u4258,axiom,
b48_buttercup10313(sK391) ).
cnf(u2419,axiom,
( ~ b48_buttercup10289(X0)
| k04_buttercup10628(X0) ) ).
cnf(u4400,axiom,
k04_buttercup10437(sK426) ).
cnf(u2638,axiom,
k04_buttercup10567(sK142) ).
cnf(u4114,axiom,
k04_buttercup10012(sK146) ).
cnf(u2069,axiom,
( ~ k04_buttercup10100(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4262,axiom,
b48_buttercup10632(sK431) ).
cnf(u2566,axiom,
( ~ b48_buttercup10381(X0)
| k04_buttercup10097(X0) ) ).
cnf(u2972,axiom,
b48_buttercup10013(sK374) ).
cnf(u4243,axiom,
b48_buttercup10542(sK424) ).
cnf(u2740,axiom,
( ~ k04_buttercup10430(X0)
| b48_buttercup10427(X0) ) ).
cnf(u2129,axiom,
( ~ b48_buttercup10308(X0)
| b48_buttercup10300(X0) ) ).
cnf(u2795,axiom,
k04_buttercup10470(sK197) ).
cnf(u3041,axiom,
b48_buttercup10220(sK443) ).
cnf(u4893,axiom,
b48_buttercup10370(sK203) ).
cnf(u4012,axiom,
k04_buttercup10619(sK204) ).
cnf(u2502,axiom,
( ~ b48_buttercup10220(X0)
| k04_buttercup10206(X0) ) ).
cnf(u4805,axiom,
b48_buttercup10170(sK150) ).
cnf(u4247,axiom,
b48_buttercup10161(sK311) ).
cnf(u2923,axiom,
b48_buttercup10421(sK325) ).
cnf(u2033,axiom,
( ~ k04_buttercup10074(X0)
| k04_buttercup10057(X0) ) ).
cnf(u4062,axiom,
k04_buttercup10012(sK42) ).
cnf(u2118,axiom,
( ~ k04_buttercup10611(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2533,axiom,
( ~ b48_buttercup10058(X0)
| k04_buttercup10061(X0) ) ).
cnf(u4933,axiom,
b48_buttercup10115(sK290) ).
cnf(u4375,axiom,
k04_buttercup10486(sK367) ).
cnf(u3963,axiom,
k04_buttercup10449(sK30) ).
cnf(u4506,axiom,
k04_buttercup10012(sK378) ).
cnf(u4049,axiom,
k04_buttercup10012(sK253) ).
cnf(u4228,axiom,
b48_buttercup10186(sK469) ).
cnf(u5049,axiom,
k04_buttercup10012(sK418) ).
cnf(u4122,axiom,
k04_buttercup10012(sK188) ).
cnf(u4488,axiom,
b48_buttercup10552(sK279) ).
cnf(u4149,axiom,
k04_buttercup10012(sK271) ).
cnf(u4485,axiom,
k04_buttercup10529(sK410) ).
cnf(u4627,axiom,
k04_buttercup10486(sK335) ).
cnf(u2216,axiom,
k04_buttercup10153(sK27) ).
cnf(u4107,axiom,
k04_buttercup10012(sK117) ).
cnf(u4255,axiom,
b48_buttercup10367(sK340) ).
cnf(u3053,axiom,
b48_buttercup10454(sK455) ).
cnf(u4420,axiom,
k04_buttercup10337(sK450) ).
cnf(u5153,axiom,
k04_buttercup10012(sK370) ).
cnf(u4021,axiom,
k04_buttercup10012(sK178) ).
cnf(u4801,axiom,
k04_buttercup10172(sK329) ).
cnf(u2712,axiom,
( ~ k04_buttercup10499(X0)
| b48_buttercup10496(X0) ) ).
cnf(u4386,axiom,
k04_buttercup10622(sK434) ).
cnf(u5293,axiom,
k04_buttercup10012(sK349) ).
cnf(u4236,axiom,
b48_buttercup10440(sK319) ).
cnf(u4093,axiom,
k04_buttercup10012(sK159) ).
cnf(u5102,axiom,
k04_buttercup10012(sK355) ).
cnf(u4929,axiom,
k04_buttercup10347(sK449) ).
cnf(u4018,axiom,
k04_buttercup10012(sK50) ).
cnf(u5283,axiom,
k04_buttercup10012(sK443) ).
cnf(u2167,axiom,
( ~ b48_buttercup10173(X0)
| b48_buttercup10170(X0) ) ).
cnf(u4224,axiom,
b48_buttercup10222(sK448) ).
cnf(u4349,axiom,
b48_buttercup10269(sK214) ).
cnf(u4687,axiom,
k04_buttercup10506(sK307) ).
cnf(u2882,axiom,
k04_buttercup10225(sK284) ).
cnf(u4360,axiom,
k04_buttercup10293(sK379) ).
cnf(u4812,axiom,
k04_buttercup10012(sK406) ).
cnf(u4477,axiom,
k04_buttercup10516(sK465) ).
cnf(u2904,axiom,
b48_buttercup10169(sK306) ).
cnf(u4408,axiom,
k04_buttercup10012(sK364) ).
cnf(u2280,axiom,
( ~ k04_buttercup10586(X0)
| b48_buttercup10582(X0) ) ).
cnf(u2595,axiom,
( ~ k04_buttercup10329(X0)
| b48_buttercup10326(X0) ) ).
cnf(u2832,axiom,
k04_buttercup10608(sK234) ).
cnf(u2743,axiom,
k04_buttercup10419(sK161) ).
cnf(u4800,axiom,
k04_buttercup10012(sK377) ).
cnf(u2208,axiom,
( ~ k04_buttercup10252(X0)
| b48_buttercup10248(X0) ) ).
cnf(u2503,axiom,
( ~ k04_buttercup10147(X0)
| b48_buttercup10143(X0) ) ).
cnf(u2412,axiom,
k04_buttercup10337(sK85) ).
cnf(u2671,axiom,
k04_buttercup10164(sK149) ).
cnf(u2842,axiom,
k04_buttercup10449(sK244) ).
cnf(u3977,axiom,
k04_buttercup10544(sK269) ).
cnf(u2559,axiom,
( ~ b48_buttercup10478(X0)
| k04_buttercup10486(X0) ) ).
cnf(u2019,axiom,
( ~ k04_buttercup10296(X0)
| k04_buttercup10293(X0) ) ).
cnf(u2490,axiom,
( ~ k04_buttercup10142(X0)
| b48_buttercup10085(X0) ) ).
cnf(u5291,axiom,
k04_buttercup10012(sK335) ).
cnf(u2050,axiom,
( ~ k04_buttercup10293(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2724,axiom,
( ~ k04_buttercup10125(X0)
| b48_buttercup10121(X0) ) ).
cnf(u4984,axiom,
k04_buttercup10012(sK313) ).
cnf(u2106,axiom,
( ~ k04_buttercup10524(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2652,axiom,
( ~ k04_buttercup10316(X0)
| b48_buttercup10313(X0) ) ).
cnf(u3059,axiom,
b48_buttercup10054(sK461) ).
cnf(u2784,axiom,
k04_buttercup10631(sK186) ).
cnf(u4583,axiom,
b48_buttercup10054(sK213) ).
cnf(u2321,axiom,
~ b48_buttercup10102(sK51) ).
cnf(u2254,axiom,
( ~ k04_buttercup10084(X0)
| b48_buttercup10082(X0) ) ).
cnf(u4451,axiom,
k04_buttercup10012(sK315) ).
cnf(u2163,axiom,
( ~ b48_buttercup10294(X0)
| b48_buttercup10291(X0) ) ).
cnf(u4090,axiom,
k04_buttercup10012(sK78) ).
cnf(u5235,axiom,
k04_buttercup10012(sK423) ).
cnf(u2091,axiom,
( ~ k04_buttercup10419(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2894,axiom,
k04_buttercup10219(sK296) ).
cnf(u4130,axiom,
k04_buttercup10012(sK208) ).
cnf(u2239,axiom,
( ~ b48_buttercup10456(X0)
| k04_buttercup10464(X0) ) ).
cnf(u1999,axiom,
( ~ k04_buttercup10097(X0)
| k04_buttercup10095(X0) ) ).
cnf(u4518,axiom,
k04_buttercup10400(sK377) ).
cnf(u3075,axiom,
b48_buttercup10180(sK477) ).
cnf(u2725,axiom,
( ~ b48_buttercup10121(X0)
| k04_buttercup10125(X0) ) ).
cnf(u2954,axiom,
b48_buttercup10019(sK356) ).
cnf(u2292,axiom,
( ~ k04_buttercup10067(X0)
| b48_buttercup10065(X0) ) ).
cnf(u4134,axiom,
k04_buttercup10012(sK105) ).
cnf(u2844,axiom,
k04_buttercup10147(sK246) ).
cnf(u4115,axiom,
k04_buttercup10012(sK150) ).
cnf(u2220,axiom,
~ b48_buttercup10227(sK28) ).
cnf(u2499,axiom,
b48_buttercup10446(sK108) ).
cnf(u2667,axiom,
~ b48_buttercup10166(sK148) ).
cnf(u2446,axiom,
( ~ k04_buttercup10516(X0)
| b48_buttercup10417(X0) ) ).
cnf(u2913,axiom,
b48_buttercup10531(sK315) ).
cnf(u2555,axiom,
k04_buttercup10486(sK123) ).
cnf(u4209,axiom,
k04_buttercup10012(sK200) ).
cnf(u5301,axiom,
k04_buttercup10012(sK384) ).
cnf(u2277,axiom,
~ k04_buttercup10026(sK45) ).
cnf(u4119,axiom,
k04_buttercup10012(sK133) ).
cnf(u4809,axiom,
k04_buttercup10172(sK328) ).
cnf(u2205,axiom,
( ~ b48_buttercup10638(X0)
| k04_buttercup10639(X0) ) ).
cnf(u4244,axiom,
b48_buttercup10402(sK409) ).
cnf(u2405,axiom,
( ~ k04_buttercup10437(X0)
| b48_buttercup10434(X0) ) ).
cnf(u4447,axiom,
b48_buttercup10629(sK186) ).
cnf(u2796,axiom,
k04_buttercup10473(sK198) ).
cnf(u4378,axiom,
k04_buttercup10190(sK471) ).
cnf(u4813,axiom,
k04_buttercup10164(sK306) ).
cnf(u4100,axiom,
k04_buttercup10012(sK106) ).
cnf(u4232,axiom,
b48_buttercup10334(sK449) ).
cnf(u4229,axiom,
b48_buttercup10130(sK419) ).
cnf(u2880,axiom,
k04_buttercup10425(sK282) ).
cnf(u4941,axiom,
k04_buttercup10012(sK324) ).
cnf(u5006,axiom,
~ k04_buttercup10619(sK439) ).
cnf(u4043,negated_conjecture,
k04_buttercup10012(sK366) ).
cnf(u5060,axiom,
k04_buttercup10012(sK329) ).
cnf(u4357,axiom,
b48_buttercup10291(sK291) ).
cnf(u2966,axiom,
b48_buttercup10261(sK368) ).
cnf(u4828,axiom,
k04_buttercup10244(sK408) ).
cnf(u4345,axiom,
b48_buttercup10582(sK205) ).
cnf(u2797,axiom,
k04_buttercup10376(sK199) ).
cnf(u4676,axiom,
b48_buttercup10542(sK268) ).
cnf(u4127,axiom,
k04_buttercup10012(sK211) ).
cnf(u5220,axiom,
k04_buttercup10012(sK333) ).
cnf(u4006,axiom,
k04_buttercup10555(sK278) ).
cnf(u4473,axiom,
k04_buttercup10516(sK357) ).
cnf(u2925,axiom,
b48_buttercup10179(sK327) ).
cnf(u4492,axiom,
k04_buttercup10555(sK390) ).
cnf(u4334,axiom,
b48_buttercup10086(sK257) ).
cnf(u4323,axiom,
b48_buttercup10231(sK195) ).
cnf(u4628,axiom,
k04_buttercup10012(sK471) ).
cnf(u2584,axiom,
b48_buttercup10440(sK132) ).
cnf(u4108,axiom,
k04_buttercup10012(sK118) ).
cnf(u3965,axiom,
k04_buttercup10449(sK32) ).
cnf(u2935,axiom,
b48_buttercup10076(sK337) ).
cnf(u4480,axiom,
b48_buttercup10417(sK217) ).
cnf(u4880,axiom,
b48_buttercup10469(sK197) ).
cnf(u4790,axiom,
k04_buttercup10316(sK391) ).
cnf(u4096,axiom,
k04_buttercup10012(sK143) ).
cnf(u4750,axiom,
b48_buttercup10411(sK243) ).
cnf(u4221,axiom,
b48_buttercup10300(sK364) ).
cnf(u4225,axiom,
b48_buttercup10222(sK447) ).
cnf(u4664,axiom,
k04_buttercup10012(sK439) ).
cnf(u2536,axiom,
~ k04_buttercup10000(sK119) ).
cnf(u4684,axiom,
k04_buttercup10012(sK374) ).
cnf(u5056,axiom,
k04_buttercup10012(sK436) ).
cnf(u2247,axiom,
( ~ b48_buttercup10394(X0)
| k04_buttercup10397(X0) ) ).
cnf(u2612,axiom,
( ~ b48_buttercup10507(X0)
| k04_buttercup10510(X0) ) ).
cnf(u2152,axiom,
( ~ b48_buttercup10410(X0)
| b48_buttercup10402(X0) ) ).
cnf(u2409,axiom,
( ~ k04_buttercup10356(X0)
| b48_buttercup10353(X0) ) ).
cnf(u4342,axiom,
k04_buttercup10016(sK356) ).
cnf(u4672,axiom,
k04_buttercup10342(sK384) ).
cnf(u2080,axiom,
( ~ k04_buttercup10364(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4048,axiom,
k04_buttercup10012(sK298) ).
cnf(u4335,axiom,
k04_buttercup10089(sK392) ).
cnf(u2306,axiom,
( ~ k04_buttercup10200(X0)
| b48_buttercup10199(X0) ) ).
cnf(u2980,axiom,
b48_buttercup10493(sK382) ).
cnf(u2431,axiom,
k04_buttercup10347(sK88) ).
cnf(u4372,axiom,
k04_buttercup10492(sK383) ).
cnf(u4982,axiom,
~ k04_buttercup10100(sK434) ).
cnf(u2137,axiom,
( ~ b48_buttercup10134(X0)
| b48_buttercup10130(X0) ) ).
cnf(u4330,axiom,
b48_buttercup10394(sK231) ).
cnf(u2905,axiom,
b48_buttercup10502(sK307) ).
cnf(u3049,axiom,
b48_buttercup10186(sK451) ).
cnf(u4327,axiom,
k04_buttercup10464(sK361) ).
cnf(u2065,axiom,
( ~ k04_buttercup10079(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4015,axiom,
k04_buttercup10516(sK216) ).
cnf(u2931,axiom,
b48_buttercup10072(sK333) ).
cnf(u2656,axiom,
~ b48_buttercup10308(sK145) ).
cnf(u2951,axiom,
b48_buttercup10381(sK353) ).
cnf(u4455,axiom,
b48_buttercup10176(sK304) ).
cnf(u2032,axiom,
( ~ k04_buttercup10067(X0)
| k04_buttercup10057(X0) ) ).
cnf(u4087,axiom,
k04_buttercup10012(sK239) ).
cnf(u2126,axiom,
( ~ b48_buttercup10052(X0)
| b48_buttercup10046(X0) ) ).
cnf(u4315,axiom,
b48_buttercup10150(sK116) ).
cnf(u3007,axiom,
b48_buttercup10405(sK409) ).
cnf(u4057,axiom,
k04_buttercup10012(sK267) ).
cnf(u3962,axiom,
k04_buttercup10449(sK218) ).
cnf(u2186,axiom,
( ~ b48_buttercup10518(X0)
| b48_buttercup10515(X0) ) ).
cnf(u4746,axiom,
k04_buttercup10516(sK325) ).
cnf(u2111,axiom,
( ~ k04_buttercup10555(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2548,axiom,
( ~ b48_buttercup10624(X0)
| k04_buttercup10626(X0) ) ).
cnf(u2529,axiom,
( ~ b48_buttercup10159(X0)
| k04_buttercup10153(X0) ) ).
cnf(u4836,axiom,
k04_buttercup10012(sK326) ).
cnf(u2597,axiom,
( ~ k04_buttercup10325(X0)
| b48_buttercup10322(X0) ) ).
cnf(u2821,axiom,
k04_buttercup10619(sK223) ).
cnf(u2476,axiom,
k04_buttercup10464(sK103) ).
cnf(u2243,axiom,
k04_buttercup10464(sK35) ).
cnf(u2164,axiom,
( ~ b48_buttercup10299(X0)
| b48_buttercup10291(X0) ) ).
cnf(u2657,axiom,
k04_buttercup10303(sK145) ).
cnf(u2299,axiom,
( ~ b48_buttercup10490(X0)
| k04_buttercup10492(X0) ) ).
cnf(u5129,axiom,
k04_buttercup10012(sK451) ).
cnf(u2092,axiom,
( ~ k04_buttercup10424(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2021,axiom,
( ~ k04_buttercup10637(X0)
| k04_buttercup10635(X0) ) ).
cnf(u4553,axiom,
k04_buttercup10153(sK376) ).
cnf(u5019,axiom,
k04_buttercup10012(sK321) ).
cnf(u3076,axiom,
b48_buttercup10572(sK478) ).
cnf(u2718,axiom,
( ~ b48_buttercup10186(X0)
| k04_buttercup10190(X0) ) ).
cnf(u4368,axiom,
k04_buttercup10495(sK382) ).
cnf(u2149,axiom,
( ~ b48_buttercup10545(X0)
| b48_buttercup10542(X0) ) ).
cnf(u2646,axiom,
( ~ b48_buttercup10133(X0)
| k04_buttercup10132(X0) ) ).
cnf(u3061,axiom,
b48_buttercup10052(sK463) ).
cnf(u2778,axiom,
k04_buttercup10048(sK180) ).
cnf(u2077,axiom,
( ~ k04_buttercup10164(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4116,axiom,
k04_buttercup10012(sK191) ).
cnf(u2209,axiom,
( ~ b48_buttercup10248(X0)
| k04_buttercup10252(X0) ) ).
cnf(u4020,axiom,
k04_buttercup10012(sK302) ).
cnf(u2711,axiom,
~ b48_buttercup10260(sK156) ).
cnf(u4104,axiom,
k04_buttercup10012(sK26) ).
cnf(u4092,axiom,
k04_buttercup10012(sK277) ).
cnf(u4685,axiom,
b48_buttercup10502(sK193) ).
cnf(u4892,axiom,
k04_buttercup10619(sK435) ).
cnf(u3003,axiom,
b48_buttercup10521(sK405) ).
cnf(u4798,axiom,
k04_buttercup10012(sK327) ).
cnf(u4304,axiom,
k04_buttercup10637(sK431) ).
cnf(u4202,axiom,
k04_buttercup10012(sK51) ).
cnf(u4101,axiom,
k04_buttercup10012(sK187) ).
cnf(u2198,axiom,
k04_buttercup10303(sK25) ).
cnf(u2541,axiom,
~ b48_buttercup10108(sK120) ).
cnf(u4932,axiom,
b48_buttercup10115(sK159) ).
cnf(u4786,axiom,
b48_buttercup10313(sK298) ).
cnf(u2838,axiom,
k04_buttercup10097(sK240) ).
cnf(u4217,axiom,
b48_buttercup10046(sK464) ).
cnf(u2669,axiom,
( ~ b48_buttercup10166(X0)
| k04_buttercup10164(X0) ) ).
cnf(u4417,axiom,
k04_buttercup10337(sK420) ).
cnf(u2840,axiom,
k04_buttercup10252(sK242) ).
cnf(u4364,axiom,
k04_buttercup10074(sK333) ).
cnf(u2557,axiom,
~ b48_buttercup10478(sK124) ).
cnf(u4496,axiom,
k04_buttercup10449(sK360) ).
cnf(u4206,axiom,
k04_buttercup10012(sK204) ).
cnf(u4338,axiom,
b48_buttercup10082(sK177) ).
cnf(u2018,axiom,
( ~ k04_buttercup10376(X0)
| k04_buttercup10369(X0) ) ).
cnf(u4352,axiom,
k04_buttercup10382(sK351) ).
cnf(u4585,axiom,
b48_buttercup10054(sK293) ).
cnf(u2040,axiom,
( ~ k04_buttercup10184(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2792,axiom,
k04_buttercup10074(sK194) ).
cnf(u4794,axiom,
b48_buttercup10309(sK238) ).
cnf(u4045,negated_conjecture,
k04_buttercup10012(sK483) ).
cnf(u4097,axiom,
k04_buttercup10012(sK144) ).
cnf(u4912,axiom,
k04_buttercup10190(sK473) ).
cnf(u2408,axiom,
( ~ b48_buttercup10013(X0)
| k04_buttercup10016(X0) ) ).
cnf(u3970,axiom,
k04_buttercup10449(sK219) ).
cnf(u4650,axiom,
k04_buttercup10544(sK424) ).
cnf(u2119,axiom,
( ~ k04_buttercup10619(X0)
| k04_buttercup10012(X0) ) ).
cnf(u3971,axiom,
k04_buttercup10477(sK252) ).
cnf(u3992,axiom,
k04_buttercup10635(sK294) ).
cnf(u2962,axiom,
b48_buttercup10307(sK364) ).
cnf(u4214,axiom,
k04_buttercup10012(sK227) ).
cnf(u5173,axiom,
k04_buttercup10012(sK462) ).
cnf(u2029,axiom,
( ~ k04_buttercup10219(X0)
| k04_buttercup10204(X0) ) ).
cnf(u2852,axiom,
k04_buttercup10581(sK254) ).
cnf(u5141,axiom,
k04_buttercup10012(sK478) ).
cnf(u2984,axiom,
b48_buttercup10092(sK386) ).
cnf(u2675,axiom,
( ~ b48_buttercup10174(X0)
| k04_buttercup10172(X0) ) ).
cnf(u2912,axiom,
b48_buttercup10332(sK314) ).
cnf(u2695,axiom,
( ~ k04_buttercup10473(X0)
| b48_buttercup10471(X0) ) ).
cnf(u4199,axiom,
k04_buttercup10012(sK236) ).
cnf(u2288,axiom,
( ~ k04_buttercup10296(X0)
| b48_buttercup10294(X0) ) ).
cnf(u4331,axiom,
k04_buttercup10397(sK378) ).
cnf(u4976,axiom,
k04_buttercup10419(sK448) ).
cnf(u2442,axiom,
k04_buttercup10516(sK91) ).
cnf(u4187,axiom,
k04_buttercup10012(sK280) ).
cnf(u2879,axiom,
k04_buttercup10221(sK281) ).
cnf(u2130,axiom,
( ~ b48_buttercup10227(X0)
| b48_buttercup10222(X0) ) ).
cnf(u2804,axiom,
k04_buttercup10628(sK206) ).
cnf(u4312,axiom,
k04_buttercup10153(sK373) ).
cnf(u2058,axiom,
( ~ k04_buttercup10356(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2732,axiom,
( ~ k04_buttercup10039(X0)
| b48_buttercup10035(X0) ) ).
cnf(u3011,axiom,
b48_buttercup10353(sK413) ).
cnf(u4775,axiom,
k04_buttercup10132(sK417) ).
cnf(u2420,axiom,
( ~ k04_buttercup10631(X0)
| b48_buttercup10629(X0) ) ).
cnf(u5218,axiom,
k04_buttercup10012(sK332) ).
cnf(u2348,axiom,
( ~ k04_buttercup10620(X0)
| b48_buttercup10107(X0) ) ).
cnf(u2115,axiom,
( ~ k04_buttercup10586(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4316,axiom,
b48_buttercup10150(sK117) ).
cnf(u4042,axiom,
k04_buttercup10012(sK220) ).
cnf(u4297,axiom,
b48_buttercup10642(sK292) ).
cnf(u4763,axiom,
k04_buttercup10012(sK441) ).
cnf(u2171,axiom,
( ~ b48_buttercup10640(X0)
| b48_buttercup10632(X0) ) ).
cnf(u2974,axiom,
b48_buttercup10158(sK376) ).
cnf(u2191,axiom,
k04_buttercup10303(sK24) ).
cnf(u4381,axiom,
k04_buttercup10551(sK425) ).
cnf(u2805,axiom,
k04_buttercup10486(sK207) ).
cnf(u3034,axiom,
b48_buttercup10309(sK436) ).
cnf(u2590,axiom,
( ~ b48_buttercup10367(X0)
| k04_buttercup10369(X0) ) ).
cnf(u4301,axiom,
b48_buttercup10638(sK189) ).
cnf(u4001,axiom,
k04_buttercup10057(sK89) ).
cnf(u2244,axiom,
b48_buttercup10458(sK34) ).
cnf(u4886,axiom,
k04_buttercup10095(sK386) ).
cnf(u4744,axiom,
k04_buttercup10445(sK318) ).
cnf(u2933,axiom,
b48_buttercup10478(sK335) ).
cnf(u2691,axiom,
b48_buttercup10222(sK153) ).
cnf(u2650,axiom,
( ~ k04_buttercup10132(X0)
| b48_buttercup10130(X0) ) ).
cnf(u2300,axiom,
~ b48_buttercup10487(sK46) ).
cnf(u5207,axiom,
k04_buttercup10012(sK369) ).
cnf(u2026,axiom,
( ~ k04_buttercup10425(X0)
| k04_buttercup10424(X0) ) ).
cnf(u4429,axiom,
k04_buttercup10635(sK323) ).
cnf(u2861,axiom,
k04_buttercup10039(sK263) ).
cnf(u2526,axiom,
( ~ b48_buttercup10160(X0)
| k04_buttercup10153(X0) ) ).
cnf(u2993,axiom,
b48_buttercup10609(sK395) ).
cnf(u2507,axiom,
~ k04_buttercup10004(sK109) ).
cnf(u4286,axiom,
b48_buttercup10300(sK25) ).
cnf(u5058,axiom,
k04_buttercup10012(sK479) ).
cnf(u4622,axiom,
k04_buttercup10482(sK480) ).
cnf(u3964,axiom,
k04_buttercup10449(sK31) ).
cnf(u4915,axiom,
b48_buttercup10186(sK49) ).
cnf(u4051,axiom,
k04_buttercup10012(sK266) ).
cnf(u2875,axiom,
k04_buttercup10100(sK277) ).
cnf(u4670,axiom,
b48_buttercup10605(sK286) ).
cnf(u4176,axiom,
k04_buttercup10012(sK193) ).
cnf(u2285,axiom,
( ~ b48_buttercup10269(X0)
| k04_buttercup10385(X0) ) ).
cnf(u4874,axiom,
b48_buttercup10471(sK198) ).
cnf(u4639,axiom,
k04_buttercup10097(sK353) ).
cnf(u2485,axiom,
k04_buttercup10400(sK104) ).
cnf(u2413,axiom,
( ~ b48_buttercup10334(X0)
| k04_buttercup10337(X0) ) ).
cnf(u4658,axiom,
b48_buttercup10326(sK251) ).
cnf(u3973,axiom,
k04_buttercup10477(sK47) ).
cnf(u4911,axiom,
k04_buttercup10012(sK353) ).
cnf(u4752,axiom,
b48_buttercup10410(sK256) ).
cnf(u3046,axiom,
b48_buttercup10228(sK448) ).
cnf(u3014,axiom,
b48_buttercup10031(sK416) ).
cnf(u4210,axiom,
k04_buttercup10012(sK206) ).
cnf(u4986,axiom,
~ k04_buttercup10282(sK206) ).
cnf(u4014,axiom,
k04_buttercup10139(sK209) ).
cnf(u4086,axiom,
k04_buttercup10012(sK154) ).
cnf(u3005,axiom,
b48_buttercup10570(sK407) ).
cnf(u4023,axiom,
k04_buttercup10012(sK224) ).
cnf(u2697,axiom,
( ~ k04_buttercup10470(X0)
| b48_buttercup10469(X0) ) ).
cnf(u4618,axiom,
k04_buttercup10622(sK459) ).
cnf(u4195,axiom,
k04_buttercup10012(sK254) ).
cnf(u5090,axiom,
~ k04_buttercup10204(sK281) ).
cnf(u4558,axiom,
k04_buttercup10153(sK375) ).
cnf(u2887,axiom,
k04_buttercup10293(sK289) ).
cnf(u4523,axiom,
k04_buttercup10142(sK406) ).
cnf(u4757,axiom,
k04_buttercup10567(sK404) ).
cnf(u4470,axiom,
k04_buttercup10517(sK325) ).
cnf(u5228,axiom,
k04_buttercup10012(sK468) ).
cnf(u4778,axiom,
b48_buttercup10130(sK144) ).
cnf(u5297,axiom,
k04_buttercup10012(sK435) ).
cnf(u2834,axiom,
k04_buttercup10602(sK236) ).
cnf(u4527,axiom,
k04_buttercup10012(sK381) ).
cnf(u4458,axiom,
k04_buttercup10351(sK331) ).
cnf(u2100,axiom,
( ~ k04_buttercup10492(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2020,axiom,
( ~ k04_buttercup10298(X0)
| k04_buttercup10293(X0) ) ).
cnf(u2202,axiom,
( ~ k04_buttercup10641(X0)
| b48_buttercup10640(X0) ) ).
cnf(u2567,axiom,
~ k04_buttercup10100(sK126) ).
cnf(u2160,axiom,
( ~ b48_buttercup10370(X0)
| b48_buttercup10367(X0) ) ).
cnf(u4703,axiom,
b48_buttercup10052(sK179) ).
cnf(u2623,axiom,
( ~ b48_buttercup10210(X0)
| k04_buttercup10213(X0) ) ).
cnf(u3060,axiom,
b48_buttercup10640(sK462) ).
cnf(u2786,axiom,
k04_buttercup10364(sK188) ).
cnf(u2314,axiom,
( ~ b48_buttercup10195(X0)
| k04_buttercup10190(X0) ) ).
cnf(u2217,axiom,
( ~ b48_buttercup10154(X0)
| k04_buttercup10153(X0) ) ).
cnf(u4039,axiom,
k04_buttercup10012(sK24) ).
cnf(u4765,axiom,
k04_buttercup10404(sK409) ).
cnf(u4207,axiom,
k04_buttercup10012(sK223) ).
cnf(u4095,axiom,
k04_buttercup10012(sK250) ).
cnf(u4184,axiom,
k04_buttercup10012(sK268) ).
cnf(u2604,axiom,
~ b48_buttercup10343(sK139) ).
cnf(u2883,axiom,
k04_buttercup10181(sK285) ).
cnf(u4572,axiom,
b48_buttercup10058(sK213) ).
cnf(u2736,axiom,
( ~ k04_buttercup10028(X0)
| b48_buttercup10034(X0) ) ).
cnf(u3031,axiom,
b48_buttercup10456(sK433) ).
cnf(u4648,axiom,
b48_buttercup10367(sK203) ).
cnf(u2206,axiom,
( ~ k04_buttercup10637(X0)
| b48_buttercup10636(X0) ) ).
cnf(u2959,axiom,
b48_buttercup10466(sK361) ).
cnf(u4188,axiom,
k04_buttercup10012(sK279) ).
cnf(u4169,axiom,
k04_buttercup10012(sK196) ).
cnf(u4635,axiom,
k04_buttercup10012(sK425) ).
cnf(u2846,axiom,
k04_buttercup10004(sK248) ).
cnf(u2063,axiom,
( ~ k04_buttercup10053(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4799,axiom,
k04_buttercup10303(sK479) ).
cnf(u2500,axiom,
( ~ k04_buttercup10135(X0)
| b48_buttercup10446(X0) ) ).
cnf(u5000,axiom,
~ k04_buttercup10100(sK437) ).
cnf(u2677,axiom,
( ~ b48_buttercup10180(X0)
| k04_buttercup10181(X0) ) ).
cnf(u4742,axiom,
b48_buttercup10443(sK185) ).
cnf(u2906,axiom,
b48_buttercup10289(sK308) ).
cnf(u2772,axiom,
k04_buttercup10282(sK174) ).
cnf(u4173,axiom,
k04_buttercup10012(sK232) ).
cnf(u2116,axiom,
( ~ k04_buttercup10593(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4305,axiom,
b48_buttercup10248(sK242) ).
cnf(u2737,axiom,
( ~ b48_buttercup10034(X0)
| k04_buttercup10028(X0) ) ).
cnf(u2251,axiom,
( ~ b48_buttercup10086(X0)
| k04_buttercup10089(X0) ) ).
cnf(u4290,negated_conjecture,
b48_buttercup10300(sK481) ).
cnf(u2172,axiom,
( ~ b48_buttercup10574(X0)
| b48_buttercup10563(X0) ) ).
cnf(u2619,axiom,
~ k04_buttercup10053(sK140) ).
cnf(u4918,axiom,
b48_buttercup10186(sK302) ).
cnf(u2865,axiom,
k04_buttercup10337(sK267) ).
cnf(u2798,axiom,
k04_buttercup10626(sK200) ).
cnf(u2229,axiom,
k04_buttercup10464(sK30) ).
cnf(u4759,axiom,
b48_buttercup10402(sK258) ).
cnf(u2726,axiom,
~ b48_buttercup10120(sK159) ).
cnf(u3013,axiom,
b48_buttercup10035(sK415) ).
cnf(u2157,axiom,
( ~ b48_buttercup10120(X0)
| b48_buttercup10115(X0) ) ).
cnf(u2289,axiom,
( ~ b48_buttercup10294(X0)
| k04_buttercup10296(X0) ) ).
cnf(u4923,axiom,
k04_buttercup10190(sK451) ).
cnf(u4934,axiom,
k04_buttercup10012(sK316) ).
cnf(u4531,axiom,
b48_buttercup10446(sK264) ).
cnf(u4044,negated_conjecture,
k04_buttercup10012(sK481) ).
cnf(u4478,axiom,
k04_buttercup10012(sK472) ).
cnf(u2955,axiom,
b48_buttercup10515(sK357) ).
cnf(u4946,axiom,
k04_buttercup10567(sK478) ).
cnf(u4275,axiom,
b48_buttercup10054(sK333) ).
cnf(u2278,axiom,
( ~ k04_buttercup10581(X0)
| b48_buttercup10579(X0) ) ).
cnf(u5305,axiom,
k04_buttercup10012(sK470) ).
cnf(u5093,axiom,
k04_buttercup10012(sK348) ).
cnf(u4535,axiom,
b48_buttercup10013(sK356) ).
cnf(u4624,axiom,
k04_buttercup10486(sK349) ).
cnf(u3995,axiom,
k04_buttercup10424(sK282) ).
cnf(u4466,axiom,
k04_buttercup10064(sK350) ).
cnf(u2918,axiom,
b48_buttercup10632(sK320) ).
cnf(u2028,axiom,
( ~ k04_buttercup10213(X0)
| k04_buttercup10204(X0) ) ).
cnf(u4282,axiom,
b48_buttercup10515(sK405) ).
cnf(u2497,axiom,
( ~ k04_buttercup10135(X0)
| b48_buttercup10458(X0) ) ).
cnf(u3958,axiom,
k04_buttercup10337(sK158) ).
cnf(u3972,axiom,
k04_buttercup10477(sK46) ).
cnf(u2920,axiom,
b48_buttercup10362(sK322) ).
cnf(u4831,axiom,
b48_buttercup10609(sK229) ).
cnf(u4954,axiom,
b48_buttercup10031(sK262) ).
cnf(u4858,axiom,
b48_buttercup10474(sK46) ).
cnf(u4476,axiom,
k04_buttercup10516(sK440) ).
cnf(u5198,axiom,
k04_buttercup10012(sK360) ).
cnf(u4580,axiom,
b48_buttercup10054(sK90) ).
cnf(u5185,axiom,
k04_buttercup10012(sK440) ).
cnf(u4629,axiom,
k04_buttercup10095(sK353) ).
cnf(u5296,axiom,
k04_buttercup10012(sK438) ).
cnf(u4761,axiom,
b48_buttercup10402(sK256) ).
cnf(u4053,axiom,
k04_buttercup10012(sK87) ).
cnf(u5169,axiom,
k04_buttercup10012(sK449) ).
cnf(u5089,axiom,
k04_buttercup10204(sK466) ).
cnf(u2488,axiom,
k04_buttercup10400(sK105) ).
cnf(u4050,axiom,
k04_buttercup10012(sK251) ).
cnf(u3068,axiom,
b48_buttercup10451(sK470) ).
cnf(u2416,axiom,
( ~ k04_buttercup10635(X0)
| b48_buttercup10632(X0) ) ).
cnf(u2199,axiom,
( ~ b48_buttercup10307(X0)
| k04_buttercup10303(X0) ) ).
cnf(u4971,axiom,
k04_buttercup10430(sK442) ).
cnf(u2104,axiom,
( ~ k04_buttercup10510(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4181,axiom,
k04_buttercup10012(sK299) ).
cnf(u4072,axiom,
k04_buttercup10012(sK297) ).
cnf(u3042,axiom,
b48_buttercup10222(sK444) ).
cnf(u4162,axiom,
k04_buttercup10012(sK301) ).
cnf(u4158,axiom,
k04_buttercup10012(sK103) ).
cnf(u4009,axiom,
k04_buttercup10619(sK120) ).
cnf(u2932,axiom,
b48_buttercup10507(sK334) ).
cnf(u2658,axiom,
( ~ b48_buttercup10308(X0)
| k04_buttercup10303(X0) ) ).
cnf(u3064,axiom,
b48_buttercup10217(sK466) ).
cnf(u2089,axiom,
( ~ k04_buttercup10404(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2627,axiom,
( ~ b48_buttercup10446(X0)
| k04_buttercup10449(X0) ) ).
cnf(u4642,axiom,
k04_buttercup10364(sK316) ).
cnf(u2992,axiom,
b48_buttercup10411(sK394) ).
cnf(u2775,axiom,
k04_buttercup10084(sK177) ).
cnf(u2240,axiom,
b48_buttercup10458(sK36) ).
cnf(u4917,axiom,
b48_buttercup10186(sK157) ).
cnf(u3967,axiom,
k04_buttercup10449(sK34) ).
cnf(u4497,axiom,
b48_buttercup10460(sK218) ).
cnf(u2703,axiom,
( ~ b48_buttercup10378(X0)
| k04_buttercup10380(X0) ) ).
cnf(u4444,axiom,
k04_buttercup10628(sK308) ).
cnf(u4146,axiom,
k04_buttercup10012(sK241) ).
cnf(u2522,axiom,
k04_buttercup10153(sK116) ).
cnf(u2078,axiom,
( ~ k04_buttercup10172(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2831,axiom,
k04_buttercup10492(sK233) ).
cnf(u2210,axiom,
( ~ k04_buttercup10535(X0)
| b48_buttercup10531(X0) ) ).
cnf(u4610,axiom,
k04_buttercup10622(sK435) ).
cnf(u2138,axiom,
( ~ b48_buttercup10343(X0)
| b48_buttercup10334(X0) ) ).
cnf(u2553,axiom,
( ~ b48_buttercup10479(X0)
| k04_buttercup10482(X0) ) ).
cnf(u5307,axiom,
k04_buttercup10012(sK466) ).
cnf(u2014,axiom,
( ~ k04_buttercup10236(X0)
| k04_buttercup10234(X0) ) ).
cnf(u2481,axiom,
( ~ b48_buttercup10563(X0)
| k04_buttercup10567(X0) ) ).
cnf(u4872,axiom,
k04_buttercup10477(sK480) ).
cnf(u4546,axiom,
b48_buttercup10589(sK236) ).
cnf(u2428,axiom,
k04_buttercup10347(sK87) ).
cnf(u2195,axiom,
( ~ k04_buttercup10303(X0)
| b48_buttercup10300(X0) ) ).
cnf(u2432,axiom,
( ~ b48_buttercup10348(X0)
| k04_buttercup10347(X0) ) ).
cnf(u2609,axiom,
( ~ k04_buttercup10506(X0)
| b48_buttercup10502(X0) ) ).
cnf(u2123,axiom,
( ~ k04_buttercup10635(X0)
| k04_buttercup10012(X0) ) ).
cnf(u3054,axiom,
b48_buttercup10115(sK456) ).
cnf(u2034,axiom,
( ~ k04_buttercup10559(X0)
| k04_buttercup10555(X0) ) ).
cnf(u2271,axiom,
~ b48_buttercup10021(sK43) ).
cnf(u2323,axiom,
( ~ b48_buttercup10102(X0)
| k04_buttercup10622(X0) ) ).
cnf(u4550,axiom,
k04_buttercup10593(sK369) ).
cnf(u4154,axiom,
k04_buttercup10012(sK32) ).
cnf(u2960,axiom,
b48_buttercup10465(sK362) ).
cnf(u2670,axiom,
~ b48_buttercup10167(sK149) ).
cnf(u4094,axiom,
k04_buttercup10012(sK290) ).
cnf(u4081,axiom,
k04_buttercup10012(sK293) ).
cnf(u2101,axiom,
( ~ k04_buttercup10495(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4166,axiom,
k04_buttercup10012(sK47) ).
cnf(u2598,axiom,
( ~ b48_buttercup10322(X0)
| k04_buttercup10325(X0) ) ).
cnf(u3004,axiom,
b48_buttercup10085(sK406) ).
cnf(u2771,axiom,
k04_buttercup10419(sK171) ).
cnf(u2730,axiom,
k04_buttercup10567(sK160) ).
cnf(u2252,axiom,
( ~ k04_buttercup10079(X0)
| b48_buttercup10076(X0) ) ).
cnf(u2699,axiom,
~ b48_buttercup10092(sK154) ).
cnf(u2945,axiom,
b48_buttercup10378(sK347) ).
cnf(u5304,axiom,
b48_buttercup10446(sK470) ).
cnf(u4475,axiom,
k04_buttercup10516(sK405) ).
cnf(u4403,axiom,
b48_buttercup10013(sK42) ).
cnf(u2534,axiom,
( ~ k04_buttercup10057(X0)
| b48_buttercup10054(X0) ) ).
cnf(u4837,axiom,
b48_buttercup10214(sK234) ).
cnf(u4279,axiom,
b48_buttercup10515(sK440) ).
cnf(u2827,axiom,
k04_buttercup10611(sK229) ).
cnf(u2150,axiom,
( ~ b48_buttercup10548(X0)
| b48_buttercup10542(X0) ) ).
cnf(u2437,axiom,
k04_buttercup10064(sK90) ).
cnf(u4851,axiom,
b48_buttercup10222(sK28) ).
cnf(u4876,axiom,
k04_buttercup10012(sK461) ).
cnf(u2493,axiom,
k04_buttercup10139(sK106) ).
cnf(u2981,axiom,
b48_buttercup10490(sK383) ).
cnf(u4260,axiom,
b48_buttercup10170(sK329) ).
cnf(u2632,axiom,
( ~ b48_buttercup10570(X0)
| k04_buttercup10567(X0) ) ).
cnf(u4953,axiom,
k04_buttercup10012(sK403) ).
cnf(u2621,axiom,
( ~ b48_buttercup10029(X0)
| k04_buttercup10053(X0) ) ).
cnf(u2023,axiom,
( ~ k04_buttercup10641(X0)
| k04_buttercup10635(X0) ) ).
cnf(u5298,axiom,
k04_buttercup10012(sK459) ).
cnf(u4517,axiom,
k04_buttercup10012(sK392) ).
cnf(u4654,axiom,
k04_buttercup10369(sK344) ).
cnf(u4139,axiom,
k04_buttercup10012(sK243) ).
cnf(u4287,axiom,
b48_buttercup10300(sK145) ).
cnf(u4555,axiom,
k04_buttercup10012(sK354) ).
cnf(u4038,axiom,
k04_buttercup10012(sK291) ).
cnf(u5310,axiom,
k04_buttercup10012(sK414) ).
cnf(u2957,axiom,
b48_buttercup10460(sK359) ).
cnf(u4452,axiom,
k04_buttercup10064(sK336) ).
cnf(u3975,axiom,
k04_buttercup10477(sK124) ).
cnf(u4833,axiom,
k04_buttercup10012(sK376) ).
cnf(u2744,axiom,
( ~ b48_buttercup10422(X0)
| k04_buttercup10419(X0) ) ).
cnf(u4268,axiom,
b48_buttercup10150(sK376) ).
cnf(u3079,negated_conjecture,
b48_buttercup10305(sK483) ).
cnf(u3997,axiom,
k04_buttercup10204(sK300) ).
cnf(u5079,axiom,
k04_buttercup10012(sK408) ).
cnf(u2967,axiom,
b48_buttercup10596(sK369) ).
cnf(u4715,axiom,
k04_buttercup10012(sK345) ).
cnf(u4961,axiom,
k04_buttercup10337(sK384) ).
cnf(u4000,axiom,
k04_buttercup10057(sK86) ).
cnf(u2441,axiom,
~ b48_buttercup10515(sK91) ).
cnf(u5187,axiom,
k04_buttercup10012(sK465) ).
cnf(u2022,axiom,
( ~ k04_buttercup10639(X0)
| k04_buttercup10635(X0) ) ).
cnf(u2071,axiom,
( ~ k04_buttercup10125(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4256,axiom,
b48_buttercup10291(sK452) ).
cnf(u2294,axiom,
( ~ k04_buttercup10074(X0)
| b48_buttercup10072(X0) ) ).
cnf(u4253,axiom,
b48_buttercup10367(sK344) ).
cnf(u4816,axiom,
k04_buttercup10164(sK311) ).
cnf(u2914,axiom,
b48_buttercup10441(sK316) ).
cnf(u4696,axiom,
b48_buttercup10046(sK297) ).
cnf(u4844,axiom,
k04_buttercup10219(sK466) ).
cnf(u4785,axiom,
b48_buttercup10313(sK138) ).
cnf(u2052,axiom,
( ~ k04_buttercup10312(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2184,axiom,
( ~ b48_buttercup10561(X0)
| b48_buttercup10552(X0) ) ).
cnf(u4700,axiom,
k04_buttercup10048(sK464) ).
cnf(u2873,axiom,
k04_buttercup10026(sK275) ).
cnf(u2647,axiom,
~ b48_buttercup10134(sK144) ).
cnf(u2112,axiom,
( ~ k04_buttercup10567(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2535,axiom,
( ~ b48_buttercup10054(X0)
| k04_buttercup10057(X0) ) ).
cnf(u2717,axiom,
( ~ k04_buttercup10190(X0)
| b48_buttercup10186(X0) ) ).
cnf(u5295,axiom,
k04_buttercup10012(sK480) ).
cnf(u3012,axiom,
b48_buttercup10034(sK414) ).
cnf(u5272,axiom,
k04_buttercup10012(sK409) ).
cnf(u5014,axiom,
k04_buttercup10449(sK470) ).
cnf(u4867,axiom,
k04_buttercup10477(sK335) ).
cnf(u2297,axiom,
( ~ b48_buttercup10493(X0)
| k04_buttercup10495(X0) ) ).
cnf(u4147,axiom,
k04_buttercup10012(sK283) ).
cnf(u5195,axiom,
b48_buttercup10446(sK361) ).
cnf(u2082,axiom,
( ~ k04_buttercup10380(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2628,axiom,
( ~ k04_buttercup10445(X0)
| b48_buttercup10443(X0) ) ).
cnf(u4047,axiom,
k04_buttercup10012(sK138) ).
cnf(u2425,axiom,
( ~ k04_buttercup10351(X0)
| b48_buttercup10176(X0) ) ).
cnf(u2963,axiom,
b48_buttercup10616(sK365) ).
cnf(u4151,axiom,
k04_buttercup10012(sK185) ).
cnf(u2688,axiom,
( ~ b48_buttercup10208(X0)
| k04_buttercup10221(X0) ) ).
cnf(u4487,axiom,
k04_buttercup10012(sK422) ).
cnf(u2286,axiom,
( ~ k04_buttercup10382(X0)
| b48_buttercup10383(X0) ) ).
cnf(u4418,axiom,
k04_buttercup10337(sK446) ).
cnf(u3039,axiom,
b48_buttercup10552(sK441) ).
cnf(u2067,axiom,
( ~ k04_buttercup10089(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4003,axiom,
k04_buttercup10057(sK212) ).
cnf(u2926,axiom,
b48_buttercup10170(sK328) ).
cnf(u2143,axiom,
( ~ b48_buttercup10442(X0)
| b48_buttercup10440(X0) ) ).
cnf(u2031,axiom,
( ~ k04_buttercup10064(X0)
| k04_buttercup10057(X0) ) ).
cnf(u4481,axiom,
b48_buttercup10417(sK216) ).
cnf(u2629,axiom,
( ~ b48_buttercup10443(X0)
| k04_buttercup10445(X0) ) ).
cnf(u2986,axiom,
b48_buttercup10562(sK388) ).
cnf(u2508,axiom,
~ k04_buttercup10012(sK110) ).
cnf(u3953,axiom,
k04_buttercup10095(sK240) ).
cnf(u2196,axiom,
( ~ b48_buttercup10300(X0)
| k04_buttercup10303(X0) ) ).
cnf(u2689,axiom,
~ k04_buttercup10221(sK152) ).
cnf(u2876,axiom,
k04_buttercup10559(sK278) ).
cnf(u4132,axiom,
k04_buttercup10012(sK231) ).
cnf(u2602,axiom,
( ~ k04_buttercup10342(X0)
| b48_buttercup10605(X0) ) ).
cnf(u2124,axiom,
( ~ k04_buttercup10643(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2531,axiom,
( ~ b48_buttercup10161(X0)
| k04_buttercup10164(X0) ) ).
cnf(u4336,axiom,
b48_buttercup10076(sK190) ).
cnf(u5168,axiom,
k04_buttercup10012(sK446) ).
cnf(u2478,axiom,
( ~ k04_buttercup10462(X0)
| b48_buttercup10460(X0) ) ).
cnf(u2817,axiom,
k04_buttercup10464(sK219) ).
cnf(u5278,axiom,
k04_buttercup10012(sK359) ).
cnf(u4234,axiom,
b48_buttercup10334(sK476) ).
cnf(u2406,axiom,
( ~ b48_buttercup10434(X0)
| k04_buttercup10437(X0) ) ).
cnf(u2181,axiom,
( ~ b48_buttercup10070(X0)
| b48_buttercup10054(X0) ) ).
cnf(u2806,axiom,
k04_buttercup10389(sK208) ).
cnf(u2237,axiom,
~ b48_buttercup10456(sK33) ).
cnf(u4276,axiom,
b48_buttercup10054(sK336) ).
cnf(u2241,axiom,
~ k04_buttercup10464(sK36) ).
cnf(u2309,axiom,
~ b48_buttercup10193(sK49) ).
cnf(u4479,axiom,
b48_buttercup10417(sK91) ).
cnf(u4052,axiom,
k04_buttercup10012(sK85) ).
cnf(u3035,axiom,
b48_buttercup10107(sK437) ).
cnf(u4830,axiom,
k04_buttercup10012(sK343) ).
cnf(u4264,axiom,
b48_buttercup10632(sK462) ).
cnf(u2479,axiom,
( ~ b48_buttercup10460(X0)
| k04_buttercup10462(X0) ) ).
cnf(u4261,axiom,
b48_buttercup10170(sK330) ).
cnf(u4727,axiom,
b48_buttercup10446(sK30) ).
cnf(u2524,axiom,
~ b48_buttercup10160(sK117) ).
cnf(u4075,axiom,
k04_buttercup10012(sK89) ).
cnf(u4660,axiom,
k04_buttercup10619(sK437) ).
cnf(u4389,axiom,
b48_buttercup10107(sK287) ).
cnf(u2998,axiom,
b48_buttercup10326(sK400) ).
cnf(u4249,axiom,
b48_buttercup10115(sK454) ).
cnf(u4355,axiom,
b48_buttercup10291(sK289) ).
cnf(u2701,axiom,
( ~ b48_buttercup10092(X0)
| k04_buttercup10095(X0) ) ).
cnf(u4708,axiom,
b48_buttercup10050(sK297) ).
cnf(u4159,axiom,
k04_buttercup10012(sK218) ).
cnf(u3994,axiom,
k04_buttercup10026(sK262) ).
cnf(u4377,axiom,
k04_buttercup10200(sK475) ).
cnf(u5065,axiom,
k04_buttercup10012(sK328) ).
cnf(u4238,axiom,
b48_buttercup10474(sK480) ).
cnf(u4705,axiom,
k04_buttercup10012(sK320) ).
cnf(u2616,axiom,
( ~ b48_buttercup10052(X0)
| k04_buttercup10049(X0) ) ).
cnf(u2937,axiom,
b48_buttercup10471(sK339) ).
cnf(u4140,axiom,
k04_buttercup10012(sK161) ).
cnf(u5083,axiom,
~ k04_buttercup10204(sK234) ).
cnf(u2839,axiom,
k04_buttercup10419(sK241) ).
cnf(u4512,axiom,
k04_buttercup10012(sK365) ).
cnf(u4980,axiom,
~ k04_buttercup10419(sK216) ).
cnf(u2626,axiom,
( ~ k04_buttercup10449(X0)
| b48_buttercup10446(X0) ) ).
cnf(u4694,axiom,
b48_buttercup10046(sK180) ).
cnf(u4128,axiom,
k04_buttercup10012(sK210) ).
cnf(u4630,axiom,
k04_buttercup10012(sK469) ).
cnf(u2009,axiom,
( ~ k04_buttercup10547(X0)
| k04_buttercup10544(X0) ) ).
cnf(u4125,axiom,
k04_buttercup10012(sK201) ).
cnf(u2698,axiom,
( ~ b48_buttercup10469(X0)
| k04_buttercup10470(X0) ) ).
cnf(u4257,axiom,
b48_buttercup10291(sK379) ).
cnf(u4751,axiom,
k04_buttercup10415(sK394) ).
cnf(u4483,axiom,
b48_buttercup10526(sK295) ).
cnf(u3966,axiom,
k04_buttercup10449(sK33) ).
cnf(u4430,axiom,
b48_buttercup10632(sK184) ).
cnf(u2279,axiom,
( ~ b48_buttercup10579(X0)
| k04_buttercup10581(X0) ) ).
cnf(u4113,axiom,
k04_buttercup10012(sK176) ).
cnf(u2056,axiom,
( ~ k04_buttercup10333(X0)
| k04_buttercup10012(X0) ) ).
cnf(u3040,axiom,
b48_buttercup10427(sK442) ).
cnf(u4246,axiom,
b48_buttercup10161(sK310) ).
cnf(u2407,axiom,
( ~ k04_buttercup10016(X0)
| b48_buttercup10013(X0) ) ).
cnf(u4089,axiom,
k04_buttercup10012(sK273) ).
cnf(u2884,axiom,
k04_buttercup10342(sK286) ).
cnf(u5144,axiom,
k04_buttercup10012(sK415) ).
cnf(u2738,axiom,
( ~ k04_buttercup10578(X0)
| b48_buttercup10575(X0) ) ).
cnf(u3016,axiom,
b48_buttercup10130(sK418) ).
cnf(u2169,axiom,
( ~ b48_buttercup10636(X0)
| b48_buttercup10632(X0) ) ).
cnf(u2707,axiom,
( ~ b48_buttercup10377(X0)
| k04_buttercup10373(X0) ) ).
cnf(u2944,axiom,
b48_buttercup10582(sK346) ).
cnf(u4231,axiom,
b48_buttercup10334(sK450) ).
cnf(u2097,axiom,
( ~ k04_buttercup10470(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2853,axiom,
k04_buttercup10244(sK255) ).
cnf(u2835,axiom,
k04_buttercup10499(sK237) ).
cnf(u4080,axiom,
k04_buttercup10012(sK261) ).
cnf(u2560,axiom,
~ b48_buttercup10381(sK125) ).
cnf(u4359,axiom,
k04_buttercup10293(sK452) ).
cnf(u2158,axiom,
( ~ b48_buttercup10596(X0)
| b48_buttercup10589(X0) ) ).
cnf(u4347,axiom,
b48_buttercup10386(sK208) ).
cnf(u2911,axiom,
b48_buttercup10046(sK313) ).
cnf(u4661,axiom,
k04_buttercup10329(sK400) ).
cnf(u4899,axiom,
k04_buttercup10619(sK459) ).
cnf(u4227,axiom,
b48_buttercup10186(sK471) ).
cnf(u2218,axiom,
( ~ k04_buttercup10153(X0)
| b48_buttercup10150(X0) ) ).
cnf(u2505,axiom,
( ~ k04_buttercup10593(X0)
| b48_buttercup10589(X0) ) ).
cnf(u5033,axiom,
k04_buttercup10012(sK404) ).
cnf(u4333,axiom,
k04_buttercup10391(sK365) ).
cnf(u2433,axiom,
~ b48_buttercup10070(sK89) ).
cnf(u5180,axiom,
b48_buttercup10417(sK358) ).
cnf(u2858,axiom,
k04_buttercup10578(sK260) ).
cnf(u2633,axiom,
( ~ k04_buttercup10415(X0)
| b48_buttercup10411(X0) ) ).
cnf(u2275,axiom,
k04_buttercup10016(sK44) ).
cnf(u4935,axiom,
k04_buttercup10117(sK456) ).
cnf(u5170,axiom,
k04_buttercup10012(sK450) ).
cnf(u2561,axiom,
k04_buttercup10095(sK125) ).
cnf(u2203,axiom,
( ~ b48_buttercup10640(X0)
| k04_buttercup10641(X0) ) ).
cnf(u4136,axiom,
k04_buttercup10012(sK258) ).
cnf(u4898,axiom,
b48_buttercup10377(sK201) ).
cnf(u2403,axiom,
k04_buttercup10100(sK84) ).
cnf(u2350,axiom,
~ k04_buttercup10619(sK62) ).
cnf(u5150,axiom,
k04_buttercup10026(sK414) ).
cnf(u4532,axiom,
b48_buttercup10013(sK430) ).
cnf(u4033,axiom,
k04_buttercup10012(sK255) ).
cnf(u4669,axiom,
k04_buttercup10012(sK426) ).
cnf(u2053,axiom,
( ~ k04_buttercup10316(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2678,axiom,
( ~ k04_buttercup10244(X0)
| b48_buttercup10240(X0) ) ).
cnf(u2956,axiom,
b48_buttercup10519(sK358) ).
cnf(u4713,axiom,
b48_buttercup10029(sK245) ).
cnf(u2810,axiom,
k04_buttercup10064(sK212) ).
cnf(u2109,axiom,
( ~ k04_buttercup10544(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4589,axiom,
k04_buttercup10057(sK336) ).
cnf(u2113,axiom,
( ~ k04_buttercup10578(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2779,axiom,
k04_buttercup10535(sK181) ).
cnf(u3025,axiom,
b48_buttercup10417(sK427) ).
cnf(u4520,axiom,
b48_buttercup10085(sK209) ).
cnf(u4005,axiom,
k04_buttercup10057(sK194) ).
cnf(u5267,axiom,
b48_buttercup10417(sK325) ).
cnf(u2907,axiom,
b48_buttercup10161(sK309) ).
cnf(u2017,axiom,
( ~ k04_buttercup10373(X0)
| k04_buttercup10369(X0) ) ).
cnf(u4133,axiom,
k04_buttercup10012(sK104) ).
cnf(u2230,axiom,
( ~ b48_buttercup10465(X0)
| k04_buttercup10464(X0) ) ).
cnf(u2774,axiom,
k04_buttercup10164(sK176) ).
cnf(u4964,axiom,
b48_buttercup10575(sK260) ).
cnf(u4690,axiom,
b48_buttercup10507(sK215) ).
cnf(u2870,axiom,
k04_buttercup10238(sK272) ).
cnf(u2589,axiom,
( ~ k04_buttercup10369(X0)
| b48_buttercup10367(X0) ) ).
cnf(u4121,axiom,
k04_buttercup10012(sK136) ).
cnf(u4314,axiom,
b48_buttercup10150(sK27) ).
cnf(u4449,axiom,
k04_buttercup10631(sK345) ).
cnf(u2872,axiom,
k04_buttercup10437(sK274) ).
cnf(u4396,axiom,
k04_buttercup10100(sK439) ).
cnf(u4528,axiom,
b48_buttercup10458(sK264) ).
cnf(u4110,axiom,
k04_buttercup10012(sK147) ).
cnf(u4692,axiom,
k04_buttercup10510(sK334) ).
cnf(u4242,axiom,
b48_buttercup10542(sK423) ).
cnf(u5073,axiom,
k04_buttercup10012(sK330) ).
cnf(u4384,axiom,
b48_buttercup10548(sK270) ).
cnf(u3037,axiom,
b48_buttercup10109(sK439) ).
cnf(u2696,axiom,
( ~ b48_buttercup10471(X0)
| k04_buttercup10473(X0) ) ).
cnf(u4698,axiom,
k04_buttercup10012(sK314) ).
cnf(u4077,axiom,
k04_buttercup10012(sK194) ).
cnf(u4129,axiom,
k04_buttercup10012(sK214) ).
cnf(u2312,axiom,
~ b48_buttercup10195(sK50) ).
cnf(u4002,axiom,
k04_buttercup10057(sK90) ).
cnf(u4502,axiom,
b48_buttercup10563(sK142) ).
cnf(u2151,axiom,
( ~ b48_buttercup10405(X0)
| b48_buttercup10402(X0) ) ).
cnf(u4186,axiom,
k04_buttercup10012(sK270) ).
cnf(u3996,axiom,
k04_buttercup10204(sK224) ).
cnf(u4024,axiom,
k04_buttercup10012(sK281) ).
cnf(u2994,axiom,
b48_buttercup10214(sK396) ).
cnf(u4118,axiom,
k04_buttercup10012(sK132) ).
cnf(u4862,axiom,
b48_buttercup10474(sK196) ).
cnf(u3952,axiom,
k04_buttercup10095(sK239) ).
cnf(u4490,axiom,
k04_buttercup10449(sK362) ).
cnf(u4962,axiom,
k04_buttercup10028(sK414) ).
cnf(u4910,axiom,
k04_buttercup10499(sK380) ).
cnf(u2610,axiom,
( ~ b48_buttercup10502(X0)
| k04_buttercup10506(X0) ) ).
cnf(u2888,axiom,
k04_buttercup10117(sK290) ).
cnf(u4106,axiom,
k04_buttercup10012(sK116) ).
cnf(u4046,axiom,
k04_buttercup10012(sK238) ).
cnf(u2816,axiom,
k04_buttercup10462(sK218) ).
cnf(u2727,axiom,
k04_buttercup10117(sK159) ).
cnf(u4103,axiom,
k04_buttercup10012(sK246) ).
cnf(u4235,axiom,
b48_buttercup10440(sK316) ).
cnf(u2655,axiom,
( ~ b48_buttercup10309(X0)
| k04_buttercup10312(X0) ) ).
cnf(u2546,axiom,
( ~ b48_buttercup10104(X0)
| k04_buttercup10622(X0) ) ).
cnf(u2543,axiom,
( ~ b48_buttercup10108(X0)
| k04_buttercup10622(X0) ) ).
cnf(u2003,axiom,
( ~ k04_buttercup10453(X0)
| k04_buttercup10449(X0) ) ).
cnf(u2474,axiom,
( ~ b48_buttercup10552(X0)
| k04_buttercup10555(X0) ) ).
cnf(u2249,axiom,
( ~ b48_buttercup10616(X0)
| k04_buttercup10391(X0) ) ).
cnf(u4219,negated_conjecture,
b48_buttercup10300(sK483) ).
cnf(u2162,axiom,
( ~ b48_buttercup10377(X0)
| b48_buttercup10367(X0) ) ).
cnf(u4239,axiom,
b48_buttercup10474(sK349) ).
cnf(u2826,axiom,
k04_buttercup10012(sK228) ).
cnf(u4344,axiom,
k04_buttercup10581(sK411) ).
cnf(u4382,axiom,
b48_buttercup10545(sK269) ).
cnf(u2090,axiom,
( ~ k04_buttercup10415(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2636,axiom,
( ~ b48_buttercup10410(X0)
| k04_buttercup10408(X0) ) ).
cnf(u3043,axiom,
b48_buttercup10422(sK445) ).
cnf(u2768,axiom,
~ b48_buttercup10417(sK172) ).
cnf(u5053,axiom,
k04_buttercup10012(sK387) ).
cnf(u2305,axiom,
( ~ b48_buttercup10489(X0)
| k04_buttercup10486(X0) ) ).
cnf(u2147,axiom,
( ~ b48_buttercup10487(X0)
| b48_buttercup10474(X0) ) ).
cnf(u4348,axiom,
k04_buttercup10389(sK354) ).
cnf(u4083,axiom,
k04_buttercup10012(sK177) ).
cnf(u4329,axiom,
k04_buttercup10464(sK433) ).
cnf(u2075,axiom,
( ~ k04_buttercup10147(X0)
| k04_buttercup10012(X0) ) ).
cnf(u3006,axiom,
b48_buttercup10240(sK408) ).
cnf(u2223,axiom,
~ b48_buttercup10229(sK29) ).
cnf(u4370,axiom,
b48_buttercup10490(sK233) ).
cnf(u2709,axiom,
( ~ b48_buttercup10374(X0)
| k04_buttercup10376(X0) ) ).
cnf(u4457,axiom,
k04_buttercup10012(sK373) ).
cnf(u3066,axiom,
b48_buttercup10058(sK468) ).
cnf(u2622,axiom,
( ~ k04_buttercup10213(X0)
| b48_buttercup10210(X0) ) ).
cnf(u4404,axiom,
b48_buttercup10013(sK43) ).
cnf(u4906,axiom,
k04_buttercup10376(sK342) ).
cnf(u2276,axiom,
( ~ b48_buttercup10019(X0)
| k04_buttercup10016(X0) ) ).
cnf(u2769,axiom,
k04_buttercup10419(sK172) ).
cnf(u2828,axiom,
k04_buttercup10016(sK230) ).
cnf(u2682,axiom,
~ k04_buttercup10608(sK151) ).
cnf(u2204,axiom,
( ~ k04_buttercup10639(X0)
| b48_buttercup10638(X0) ) ).
cnf(u2651,axiom,
( ~ b48_buttercup10130(X0)
| k04_buttercup10132(X0) ) ).
cnf(u2558,axiom,
k04_buttercup10486(sK124) ).
cnf(u2897,axiom,
k04_buttercup10524(sK299) ).
cnf(u4392,axiom,
k04_buttercup10620(sK437) ).
cnf(u4074,axiom,
k04_buttercup10012(sK86) ).
cnf(u5171,axiom,
k04_buttercup10012(sK476) ).
cnf(u2486,axiom,
( ~ b48_buttercup10179(X0)
| k04_buttercup10400(X0) ) ).
cnf(u5139,axiom,
k04_buttercup10012(sK398) ).
cnf(u2758,axiom,
~ k04_buttercup10419(sK169) ).
cnf(u4208,axiom,
k04_buttercup10012(sK287) ).
cnf(u2189,axiom,
( ~ b48_buttercup10521(X0)
| b48_buttercup10515(X0) ) ).
cnf(u2921,axiom,
b48_buttercup10638(sK323) ).
cnf(u2102,axiom,
( ~ k04_buttercup10499(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2389,axiom,
( ~ b48_buttercup10111(X0)
| k04_buttercup10100(X0) ) ).
cnf(u2780,axiom,
k04_buttercup10204(sK182) ).
cnf(u4563,axiom,
b48_buttercup10161(sK149) ).
cnf(u2317,axiom,
( ~ k04_buttercup10546(X0)
| b48_buttercup10545(X0) ) ).
cnf(u4974,axiom,
k04_buttercup10419(sK445) ).
cnf(u4510,axiom,
b48_buttercup10562(sK278) ).
cnf(u4729,axiom,
b48_buttercup10446(sK32) ).
cnf(u5268,axiom,
k04_buttercup10012(sK325) ).
cnf(u3961,axiom,
k04_buttercup10449(sK301) ).
cnf(u4652,axiom,
k04_buttercup10369(sK340) ).
cnf(u4567,axiom,
k04_buttercup10164(sK309) ).
cnf(u2729,axiom,
~ b48_buttercup10572(sK160) ).
cnf(u4498,axiom,
k04_buttercup10449(sK433) ).
cnf(u5247,axiom,
k04_buttercup10012(sK344) ).
cnf(u2950,axiom,
b48_buttercup10065(sK352) ).
cnf(u5076,axiom,
k04_buttercup10012(sK477) ).
cnf(u4590,axiom,
k04_buttercup10057(sK350) ).
cnf(u5156,axiom,
k04_buttercup10012(sK442) ).
cnf(u2781,axiom,
k04_buttercup10369(sK183) ).
cnf(u4319,axiom,
k04_buttercup10153(sK371) ).
cnf(u3990,axiom,
k04_buttercup10635(sK227) ).
cnf(u4995,axiom,
~ k04_buttercup10100(sK459) ).
cnf(u2909,axiom,
b48_buttercup10167(sK311) ).
cnf(u4839,axiom,
k04_buttercup10012(sK375) ).
cnf(u2011,axiom,
( ~ k04_buttercup10408(X0)
| k04_buttercup10404(X0) ) ).
cnf(u4099,axiom,
k04_buttercup10012(sK264) ).
cnf(u2924,axiom,
b48_buttercup10160(sK326) ).
cnf(u3949,negated_conjecture,
k04_buttercup10303(sK366) ).
cnf(u2919,axiom,
b48_buttercup10446(sK321) ).
cnf(u4427,axiom,
k04_buttercup10333(sK314) ).
cnf(u4575,axiom,
k04_buttercup10061(sK468) ).
cnf(u4789,axiom,
k04_buttercup10316(sK387) ).
cnf(u4374,axiom,
k04_buttercup10486(sK397) ).
cnf(u2615,axiom,
( ~ k04_buttercup10049(X0)
| b48_buttercup10052(X0) ) ).
cnf(u4190,axiom,
k04_buttercup10012(sK141) ).
cnf(u5164,axiom,
k04_buttercup10012(sK452) ).
cnf(u4300,axiom,
k04_buttercup10641(sK462) ).
cnf(u2866,axiom,
k04_buttercup10544(sK268) ).
cnf(u4362,axiom,
k04_buttercup10067(sK352) ).
cnf(u3072,axiom,
b48_buttercup10458(sK474) ).
cnf(u2448,axiom,
( ~ b48_buttercup10526(X0)
| k04_buttercup10529(X0) ) ).
cnf(u4949,axiom,
b48_buttercup10035(sK263) ).
cnf(u5003,axiom,
k04_buttercup10012(sK432) ).
cnf(u2136,axiom,
( ~ b48_buttercup10133(X0)
| b48_buttercup10130(X0) ) ).
cnf(u4341,axiom,
k04_buttercup10016(sK430) ).
cnf(u2599,axiom,
~ b48_buttercup10320(sK138) ).
cnf(u2064,axiom,
( ~ k04_buttercup10057(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2487,axiom,
~ b48_buttercup10398(sK105) ).
cnf(u4041,axiom,
k04_buttercup10012(sK145) ).
cnf(u2418,axiom,
( ~ k04_buttercup10628(X0)
| b48_buttercup10289(X0) ) ).
cnf(u2964,axiom,
b48_buttercup10305(sK366) ).
cnf(u2415,axiom,
( ~ b48_buttercup10332(X0)
| k04_buttercup10333(X0) ) ).
cnf(u2690,axiom,
~ k04_buttercup10225(sK153) ).
cnf(u2121,axiom,
( ~ k04_buttercup10628(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4071,axiom,
k04_buttercup10012(sK179) ).
cnf(u3024,axiom,
b48_buttercup10434(sK426) ).
cnf(u4797,axiom,
k04_buttercup10312(sK436) ).
cnf(u4111,axiom,
k04_buttercup10012(sK148) ).
cnf(u2049,axiom,
( ~ k04_buttercup10282(X0)
| k04_buttercup10012(X0) ) ).
cnf(u3999,axiom,
k04_buttercup10057(sK213) ).
cnf(u4216,axiom,
k04_buttercup10012(sK292) ).
cnf(u2915,axiom,
b48_buttercup10440(sK317) ).
cnf(u2640,axiom,
( ~ k04_buttercup10404(X0)
| b48_buttercup10402(X0) ) ).
cnf(u3063,axiom,
b48_buttercup10520(sK465) ).
cnf(u2016,axiom,
( ~ k04_buttercup10371(X0)
| k04_buttercup10369(X0) ) ).
cnf(u2238,axiom,
k04_buttercup10464(sK33) ).
cnf(u2991,axiom,
b48_buttercup10410(sK393) ).
cnf(u2242,axiom,
~ b48_buttercup10458(sK35) ).
cnf(u4770,axiom,
k04_buttercup10406(sK409) ).
cnf(u3955,axiom,
k04_buttercup10337(sK87) ).
cnf(u5241,axiom,
k04_buttercup10012(sK424) ).
cnf(u4201,axiom,
k04_buttercup10012(sK229) ).
cnf(u4667,axiom,
k04_buttercup10316(sK402) ).
cnf(u2878,axiom,
k04_buttercup10551(sK280) ).
cnf(u2095,axiom,
( ~ k04_buttercup10445(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2532,axiom,
( ~ k04_buttercup10061(X0)
| b48_buttercup10058(X0) ) ).
cnf(u2581,axiom,
~ k04_buttercup10364(sK134) ).
cnf(u2938,axiom,
b48_buttercup10377(sK340) ).
cnf(u2713,axiom,
( ~ b48_buttercup10496(X0)
| k04_buttercup10499(X0) ) ).
cnf(u4998,axiom,
~ k04_buttercup10100(sK435) ).
cnf(u4205,axiom,
k04_buttercup10012(sK122) ).
cnf(u2148,axiom,
( ~ b48_buttercup10489(X0)
| b48_buttercup10474(X0) ) ).
cnf(u4337,axiom,
k04_buttercup10079(sK337) ).
cnf(u2641,axiom,
( ~ b48_buttercup10402(X0)
| k04_buttercup10404(X0) ) ).
cnf(u2283,axiom,
( ~ b48_buttercup10386(X0)
| k04_buttercup10389(X0) ) ).
cnf(u4322,axiom,
b48_buttercup10231(sK202) ).
cnf(u2076,axiom,
( ~ k04_buttercup10153(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2483,axiom,
( ~ b48_buttercup10562(X0)
| k04_buttercup10559(X0) ) ).
cnf(u2005,axiom,
( ~ k04_buttercup10464(X0)
| k04_buttercup10449(X0) ) ).
cnf(u2430,axiom,
~ b48_buttercup10348(sK88) ).
cnf(u2411,axiom,
~ b48_buttercup10334(sK85) ).
cnf(u2702,axiom,
( ~ k04_buttercup10380(X0)
| b48_buttercup10378(X0) ) ).
cnf(u2133,axiom,
( ~ b48_buttercup10191(X0)
| b48_buttercup10186(X0) ) ).
cnf(u4326,axiom,
k04_buttercup10464(sK362) ).
cnf(u2630,axiom,
~ b48_buttercup10570(sK141) ).
cnf(u3036,axiom,
b48_buttercup10108(sK438) ).
cnf(u4691,axiom,
k04_buttercup10012(sK420) ).
cnf(u2762,axiom,
k04_buttercup10419(sK167) ).
cnf(u2061,axiom,
( ~ k04_buttercup10039(X0)
| k04_buttercup10012(X0) ) ).
cnf(u5224,axiom,
k04_buttercup10012(sK350) ).
cnf(u4966,axiom,
k04_buttercup10578(sK370) ).
cnf(u4085,axiom,
k04_buttercup10012(sK125) ).
cnf(u4821,axiom,
b48_buttercup10180(sK285) ).
cnf(u4311,axiom,
k04_buttercup10153(sK372) ).
cnf(u2987,axiom,
b48_buttercup10563(sK389) ).
cnf(u5140,axiom,
b48_buttercup10563(sK478) ).
cnf(u4734,axiom,
b48_buttercup10446(sK218) ).
cnf(u4004,axiom,
k04_buttercup10057(sK261) ).
cnf(u4356,axiom,
b48_buttercup10291(sK288) ).
cnf(u2182,axiom,
( ~ b48_buttercup10072(X0)
| b48_buttercup10054(X0) ) ).
cnf(u5209,axiom,
k04_buttercup10012(sK385) ).
cnf(u4560,axiom,
k04_buttercup10012(sK363) ).
cnf(u4656,axiom,
k04_buttercup10364(sK322) ).
cnf(u4027,axiom,
k04_buttercup10012(sK29) ).
cnf(u2525,axiom,
k04_buttercup10153(sK117) ).
cnf(u4032,axiom,
k04_buttercup10012(sK272) ).
cnf(u2822,axiom,
k04_buttercup10206(sK224) ).
cnf(u3960,axiom,
k04_buttercup10337(sK304) ).
cnf(u4739,axiom,
k04_buttercup10449(sK108) ).
cnf(u2653,axiom,
( ~ b48_buttercup10313(X0)
| k04_buttercup10316(X0) ) ).
cnf(u4076,axiom,
k04_buttercup10012(sK90) ).
cnf(u2824,axiom,
k04_buttercup10153(sK226) ).
cnf(u4549,axiom,
k04_buttercup10593(sK343) ).
cnf(u4394,axiom,
k04_buttercup10100(sK458) ).
cnf(u4171,axiom,
k04_buttercup10012(sK252) ).
cnf(u2002,axiom,
( ~ k04_buttercup10351(X0)
| k04_buttercup10337(X0) ) ).
cnf(u4561,axiom,
b48_buttercup10161(sK147) ).
cnf(u5230,axiom,
k04_buttercup10012(sK397) ).
cnf(u5166,axiom,
k04_buttercup10012(sK379) ).
cnf(u2024,axiom,
( ~ k04_buttercup10028(X0)
| k04_buttercup10026(X0) ) ).
cnf(u4804,axiom,
b48_buttercup10170(sK146) ).
cnf(u2776,axiom,
k04_buttercup10200(sK178) ).
cnf(u5243,axiom,
k04_buttercup10012(sK340) ).
cnf(u4747,axiom,
k04_buttercup10567(sK407) ).
cnf(u4082,axiom,
k04_buttercup10012(sK190) ).
cnf(u2320,axiom,
( ~ b48_buttercup10548(X0)
| k04_buttercup10547(X0) ) ).
cnf(u2231,axiom,
~ b48_buttercup10466(sK31) ).
cnf(u4288,axiom,
b48_buttercup10300(sK220) ).
cnf(u4213,axiom,
k04_buttercup10012(sK189) ).
cnf(u3976,axiom,
k04_buttercup10477(sK207) ).
cnf(u2946,axiom,
b48_buttercup10208(sK348) ).
cnf(u5194,axiom,
k04_buttercup10012(sK388) ).
cnf(u4806,axiom,
b48_buttercup10170(sK191) ).
cnf(u2013,axiom,
( ~ k04_buttercup10602(X0)
| k04_buttercup10593(X0) ) ).
cnf(u4541,axiom,
k04_buttercup10012(sK411) ).
cnf(u2836,axiom,
k04_buttercup10312(sK238) ).
cnf(u4289,negated_conjecture,
b48_buttercup10300(sK366) ).
cnf(u2562,axiom,
( ~ b48_buttercup10381(X0)
| k04_buttercup10095(X0) ) ).
cnf(u2968,axiom,
b48_buttercup10575(sK370) ).
cnf(u4472,axiom,
k04_buttercup10012(sK371) ).
cnf(u2659,axiom,
~ b48_buttercup10173(sK146) ).
cnf(u4860,axiom,
b48_buttercup10474(sK123) ).
cnf(u2896,axiom,
k04_buttercup10316(sK298) ).
cnf(u2807,axiom,
k04_buttercup10142(sK209) ).
cnf(u2272,axiom,
k04_buttercup10016(sK43) ).
cnf(u4529,axiom,
b48_buttercup10013(sK429) ).
cnf(u2735,axiom,
( ~ b48_buttercup10031(X0)
| k04_buttercup10033(X0) ) ).
cnf(u2498,axiom,
~ k04_buttercup10135(sK108) ).
cnf(u2427,axiom,
~ b48_buttercup10352(sK87) ).
cnf(u2554,axiom,
~ b48_buttercup10483(sK123) ).
cnf(u3001,axiom,
b48_buttercup10322(sK403) ).
cnf(u2110,axiom,
( ~ k04_buttercup10551(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2863,axiom,
k04_buttercup10132(sK265) ).
cnf(u2114,axiom,
( ~ k04_buttercup10581(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2788,axiom,
k04_buttercup10079(sK190) ).
cnf(u2601,axiom,
( ~ b48_buttercup10320(X0)
| k04_buttercup10316(X0) ) ).
cnf(u2170,axiom,
( ~ b48_buttercup10638(X0)
| b48_buttercup10632(X0) ) ).
cnf(u2716,axiom,
( ~ b48_buttercup10191(X0)
| k04_buttercup10190(X0) ) ).
cnf(u4948,axiom,
k04_buttercup10012(sK400) ).
cnf(u2404,axiom,
( ~ b48_buttercup10109(X0)
| k04_buttercup10100(X0) ) ).
cnf(u2046,axiom,
( ~ k04_buttercup10234(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4474,axiom,
k04_buttercup10516(sK358) ).
cnf(u4578,axiom,
b48_buttercup10054(sK86) ).
cnf(u2585,axiom,
k04_buttercup10364(sK132) ).
cnf(u2227,axiom,
( ~ b48_buttercup10231(X0)
| k04_buttercup10234(X0) ) ).
cnf(u2809,axiom,
k04_buttercup10380(sK211) ).
cnf(u4035,axiom,
k04_buttercup10012(sK174) ).
cnf(u5200,axiom,
k04_buttercup10012(sK433) ).
cnf(u2155,axiom,
( ~ b48_buttercup10169(X0)
| b48_buttercup10161(X0) ) ).
cnf(u2958,axiom,
b48_buttercup10467(sK360) ).
cnf(u4194,axiom,
k04_buttercup10012(sK260) ).
cnf(u2303,axiom,
~ b48_buttercup10489(sK47) ).
cnf(u4582,axiom,
b48_buttercup10054(sK212) ).
cnf(u2789,axiom,
k04_buttercup10172(sK191) ).
cnf(u3018,axiom,
b48_buttercup10334(sK420) ).
cnf(u3985,axiom,
k04_buttercup10369(sK203) ).
cnf(u4198,axiom,
k04_buttercup10012(sK221) ).
cnf(u2908,axiom,
b48_buttercup10166(sK310) ).
cnf(u2803,axiom,
k04_buttercup10586(sK205) ).
cnf(u4179,axiom,
k04_buttercup10012(sK217) ).
cnf(u2284,axiom,
( ~ k04_buttercup10385(X0)
| b48_buttercup10269(X0) ) ).
cnf(u2010,axiom,
( ~ k04_buttercup10406(X0)
| k04_buttercup10404(X0) ) ).
cnf(u2845,axiom,
k04_buttercup10000(sK247) ).
cnf(u2731,axiom,
( ~ b48_buttercup10572(X0)
| k04_buttercup10567(X0) ) ).
cnf(u2664,axiom,
~ b48_buttercup10169(sK147) ).
cnf(u2977,axiom,
b48_buttercup10299(sK379) ).
cnf(u3957,axiom,
k04_buttercup10337(sK139) ).
cnf(u2438,axiom,
( ~ b48_buttercup10068(X0)
| k04_buttercup10064(X0) ) ).
cnf(u4183,axiom,
k04_buttercup10012(sK181) ).
cnf(u2859,axiom,
k04_buttercup10067(sK261) ).
cnf(u2269,axiom,
k04_buttercup10016(sK42) ).
cnf(u4308,axiom,
b48_buttercup10531(sK181) ).
cnf(u2054,axiom,
( ~ k04_buttercup10325(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4869,axiom,
k04_buttercup10477(sK349) ).
cnf(u5044,axiom,
k04_buttercup10012(sK417) ).
cnf(u4442,axiom,
b48_buttercup10289(sK206) ).
cnf(u4944,axiom,
k04_buttercup10117(sK398) ).
cnf(u4164,axiom,
k04_buttercup10012(sK198) ).
cnf(u4296,axiom,
k04_buttercup10303(sK364) ).
cnf(u4985,axiom,
~ k04_buttercup10282(sK308) ).
cnf(u2318,axiom,
( ~ b48_buttercup10545(X0)
| k04_buttercup10546(X0) ) ).
cnf(u4848,axiom,
k04_buttercup10221(sK348) ).
cnf(u4591,axiom,
k04_buttercup10057(sK352) ).
cnf(u4421,axiom,
k04_buttercup10337(sK476) ).
cnf(u3030,axiom,
b48_buttercup10029(sK432) ).
cnf(u2676,axiom,
( ~ k04_buttercup10181(X0)
| b48_buttercup10180(X0) ) ).
cnf(u4740,axiom,
k04_buttercup10449(sK321) ).
cnf(u2473,axiom,
( ~ k04_buttercup10555(X0)
| b48_buttercup10552(X0) ) ).
cnf(u4191,axiom,
k04_buttercup10012(sK142) ).
cnf(u4405,axiom,
b48_buttercup10013(sK44) ).
cnf(u4070,axiom,
k04_buttercup10012(sK180) ).
cnf(u4537,axiom,
k04_buttercup10206(sK443) ).
cnf(u2989,axiom,
b48_buttercup10318(sK391) ).
cnf(u4556,axiom,
k04_buttercup10153(sK326) ).
cnf(u4007,axiom,
k04_buttercup10619(sK287) ).
cnf(u4737,axiom,
b48_buttercup10446(sK301) ).
cnf(u2648,axiom,
k04_buttercup10132(sK144) ).
cnf(u3998,axiom,
k04_buttercup10204(sK296) ).
cnf(u4172,axiom,
k04_buttercup10012(sK233) ).
cnf(u4029,axiom,
k04_buttercup10012(sK296) ).
cnf(u2999,axiom,
b48_buttercup10248(sK401) ).
cnf(u4619,axiom,
k04_buttercup10477(sK397) ).
cnf(u3954,axiom,
k04_buttercup10337(sK286) ).
cnf(u2103,axiom,
( ~ k04_buttercup10504(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4160,axiom,
k04_buttercup10012(sK219) ).
cnf(u4285,axiom,
b48_buttercup10300(sK24) ).
cnf(u2818,axiom,
k04_buttercup10303(sK220) ).
cnf(u4728,axiom,
b48_buttercup10446(sK31) ).
cnf(u4748,axiom,
b48_buttercup10417(sK357) ).
cnf(u4413,axiom,
k04_buttercup10012(sK460) ).
cnf(u2084,axiom,
( ~ k04_buttercup10385(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2004,axiom,
( ~ k04_buttercup10462(X0)
| k04_buttercup10449(X0) ) ).
cnf(u2885,axiom,
k04_buttercup10620(sK287) ).
cnf(u4732,axiom,
b48_buttercup10446(sK35) ).
cnf(u2679,axiom,
( ~ b48_buttercup10240(X0)
| k04_buttercup10244(X0) ) ).
cnf(u4736,axiom,
b48_buttercup10446(sK244) ).
cnf(u2144,axiom,
( ~ b48_buttercup10478(X0)
| b48_buttercup10474(X0) ) ).
cnf(u2439,axiom,
( ~ k04_buttercup10517(X0)
| b48_buttercup10421(X0) ) ).
cnf(u5199,axiom,
b48_buttercup10446(sK433) ).
cnf(u2607,axiom,
( ~ k04_buttercup10544(X0)
| b48_buttercup10542(X0) ) ).
cnf(u3044,axiom,
b48_buttercup10348(sK446) ).
cnf(u2495,axiom,
~ k04_buttercup10135(sK107) ).
cnf(u2770,axiom,
b48_buttercup10417(sK171) ).
cnf(u2426,axiom,
( ~ b48_buttercup10176(X0)
| k04_buttercup10351(X0) ) ).
cnf(u2201,axiom,
( ~ b48_buttercup10642(X0)
| k04_buttercup10643(X0) ) ).
cnf(u2660,axiom,
k04_buttercup10172(sK146) ).
cnf(u4084,axiom,
k04_buttercup10012(sK257) ).
cnf(u4943,axiom,
k04_buttercup10012(sK322) ).
cnf(u2588,axiom,
( ~ b48_buttercup10441(X0)
| k04_buttercup10364(X0) ) ).
cnf(u2995,axiom,
b48_buttercup10487(sK397) ).
cnf(u2720,axiom,
k04_buttercup10347(sK158) ).
cnf(u3015,axiom,
b48_buttercup10134(sK417) ).
cnf(u2190,axiom,
~ b48_buttercup10305(sK24) ).
cnf(u4079,axiom,
k04_buttercup10012(sK213) ).
cnf(u3071,axiom,
b48_buttercup10191(sK473) ).
cnf(u2099,axiom,
( ~ k04_buttercup10477(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4891,axiom,
k04_buttercup10380(sK347) ).
cnf(u4026,axiom,
k04_buttercup10012(sK28) ).
cnf(u2250,axiom,
( ~ k04_buttercup10089(X0)
| b48_buttercup10086(X0) ) ).
cnf(u2830,axiom,
k04_buttercup10495(sK232) ).
cnf(u4507,axiom,
k04_buttercup10567(sK389) ).
cnf(u2175,axiom,
( ~ b48_buttercup10158(X0)
| b48_buttercup10150(X0) ) ).
cnf(u4454,axiom,
k04_buttercup10012(sK372) ).
cnf(u2661,axiom,
( ~ b48_buttercup10173(X0)
| k04_buttercup10172(X0) ) ).
cnf(u2890,axiom,
k04_buttercup10643(sK292) ).
cnf(u2540,axiom,
( ~ b48_buttercup10596(X0)
| k04_buttercup10599(X0) ) ).
cnf(u2228,axiom,
~ b48_buttercup10465(sK30) ).
cnf(u2721,axiom,
( ~ b48_buttercup10344(X0)
| k04_buttercup10347(X0) ) ).
cnf(u2027,axiom,
( ~ k04_buttercup10206(X0)
| k04_buttercup10204(X0) ) ).
cnf(u2156,axiom,
( ~ b48_buttercup10119(X0)
| b48_buttercup10115(X0) ) ).
cnf(u2435,axiom,
( ~ b48_buttercup10070(X0)
| k04_buttercup10064(X0) ) ).
cnf(u4951,axiom,
k04_buttercup10039(sK415) ).
cnf(u2603,axiom,
( ~ b48_buttercup10605(X0)
| k04_buttercup10342(X0) ) ).
cnf(u5197,axiom,
b48_buttercup10446(sK360) ).
cnf(u2849,axiom,
k04_buttercup10329(sK251) ).
cnf(u2491,axiom,
( ~ b48_buttercup10085(X0)
| k04_buttercup10142(X0) ) ).
cnf(u2782,axiom,
k04_buttercup10635(sK184) ).
cnf(u4689,axiom,
k04_buttercup10012(sK413) ).
cnf(u4564,axiom,
b48_buttercup10161(sK176) ).
cnf(u2310,axiom,
k04_buttercup10190(sK49) ).
cnf(u2213,axiom,
k04_buttercup10153(sK26) ).
cnf(u4613,axiom,
b48_buttercup10624(sK200) ).
cnf(u2556,axiom,
( ~ b48_buttercup10483(X0)
| k04_buttercup10486(X0) ) ).
cnf(u2141,axiom,
( ~ b48_buttercup10352(X0)
| b48_buttercup10334(X0) ) ).
cnf(u4180,axiom,
k04_buttercup10012(sK216) ).
cnf(u2273,axiom,
( ~ b48_buttercup10021(X0)
| k04_buttercup10016(X0) ) ).
cnf(u4438,axiom,
k04_buttercup10635(sK431) ).
cnf(u4383,axiom,
k04_buttercup10546(sK423) ).
cnf(u4037,axiom,
k04_buttercup10012(sK288) ).
cnf(u3073,axiom,
b48_buttercup10199(sK475) ).
cnf(u4749,axiom,
k04_buttercup10012(sK357) ).
cnf(u3067,axiom,
b48_buttercup10195(sK469) ).
cnf(u2757,axiom,
b48_buttercup10222(sK169) ).
cnf(u4168,axiom,
k04_buttercup10012(sK124) ).
cnf(u4165,axiom,
k04_buttercup10012(sK46) ).
cnf(u4631,axiom,
b48_buttercup10092(sK239) ).
cnf(u5274,axiom,
k04_buttercup10012(sK393) ).
cnf(u3979,axiom,
k04_buttercup10404(sK259) ).
cnf(u4850,axiom,
k04_buttercup10012(sK309) ).
cnf(u2902,axiom,
k04_buttercup10351(sK304) ).
cnf(u4281,axiom,
b48_buttercup10515(sK465) ).
cnf(u2012,axiom,
( ~ k04_buttercup10599(X0)
| k04_buttercup10593(X0) ) ).
cnf(u4641,axiom,
k04_buttercup10544(sK423) ).
cnf(u2733,axiom,
( ~ b48_buttercup10035(X0)
| k04_buttercup10039(X0) ) ).
cnf(u4612,axiom,
k04_buttercup10012(sK382) ).
cnf(u4409,axiom,
k04_buttercup10016(sK374) ).
cnf(u2634,axiom,
( ~ b48_buttercup10411(X0)
| k04_buttercup10415(X0) ) ).
cnf(u2864,axiom,
k04_buttercup10333(sK266) ).
cnf(u4270,axiom,
b48_buttercup10150(sK326) ).
cnf(u2871,axiom,
k04_buttercup10095(sK273) ).
cnf(u4416,axiom,
b48_buttercup10632(sK294) ).
cnf(u2681,axiom,
( ~ b48_buttercup10609(X0)
| k04_buttercup10611(X0) ) ).
cnf(u5004,axiom,
~ k04_buttercup10100(sK438) ).
cnf(u5192,axiom,
k04_buttercup10012(sK390) ).
cnf(u2041,axiom,
( ~ k04_buttercup10190(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4760,axiom,
b48_buttercup10402(sK259) ).
cnf(u4157,axiom,
k04_buttercup10012(sK35) ).
cnf(u4942,axiom,
k04_buttercup10125(sK399) ).
cnf(u4161,axiom,
k04_buttercup10012(sK244) ).
cnf(u4889,axiom,
b48_buttercup10378(sK211) ).
cnf(u4515,axiom,
k04_buttercup10400(sK327) ).
cnf(u4620,axiom,
b48_buttercup10479(sK252) ).
cnf(u4462,axiom,
k04_buttercup10347(sK446) ).
cnf(u4992,axiom,
~ k04_buttercup10204(sK396) ).
cnf(u4533,axiom,
k04_buttercup10012(sK430) ).
cnf(u2183,axiom,
( ~ b48_buttercup10075(X0)
| b48_buttercup10054(X0) ) ).
cnf(u4145,axiom,
k04_buttercup10012(sK172) ).
cnf(u4846,axiom,
b48_buttercup10208(sK281) ).
cnf(u2088,axiom,
( ~ k04_buttercup10400(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4056,axiom,
k04_buttercup10012(sK158) ).
cnf(u3026,axiom,
b48_buttercup10143(sK428) ).
cnf(u4278,axiom,
b48_buttercup10552(sK388) ).
cnf(u4608,axiom,
k04_buttercup10622(sK438) ).
cnf(u2311,axiom,
( ~ b48_buttercup10193(X0)
| k04_buttercup10190(X0) ) ).
cnf(u3984,axiom,
k04_buttercup10234(sK272) ).
cnf(u5023,axiom,
b48_buttercup10563(sK407) ).
cnf(u2062,axiom,
( ~ k04_buttercup10048(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2608,axiom,
( ~ b48_buttercup10542(X0)
| k04_buttercup10544(X0) ) ).
cnf(u2916,axiom,
b48_buttercup10443(sK318) ).
cnf(u5176,axiom,
k04_buttercup10012(sK323) ).
cnf(u2642,axiom,
( ~ k04_buttercup10406(X0)
| b48_buttercup10405(X0) ) ).
cnf(u3048,axiom,
b48_buttercup10343(sK450) ).
cnf(u2073,axiom,
( ~ k04_buttercup10135(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4266,axiom,
b48_buttercup10150(sK373) ).
cnf(u2976,axiom,
b48_buttercup10394(sK378) ).
cnf(u2759,axiom,
~ b48_buttercup10222(sK168) ).
cnf(u4263,axiom,
b48_buttercup10632(sK323) ).
cnf(u3956,axiom,
k04_buttercup10337(sK88) ).
cnf(u2815,axiom,
k04_buttercup10516(sK217) ).
cnf(u2867,axiom,
k04_buttercup10546(sK269) ).
cnf(u2592,axiom,
k04_buttercup10364(sK136) ).
cnf(u2506,axiom,
( ~ b48_buttercup10589(X0)
| k04_buttercup10593(X0) ) ).
cnf(u4350,axiom,
k04_buttercup10385(sK363) ).
cnf(u4251,axiom,
b48_buttercup10589(sK369) ).
cnf(u2943,axiom,
b48_buttercup10629(sK345) ).
cnf(u2194,axiom,
( ~ b48_buttercup10299(X0)
| k04_buttercup10298(X0) ) ).
cnf(u4979,axiom,
~ k04_buttercup10419(sK325) ).
cnf(u4343,axiom,
b48_buttercup10579(sK254) ).
cnf(u4034,axiom,
k04_buttercup10012(sK242) ).
cnf(u2122,axiom,
( ~ k04_buttercup10631(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2537,axiom,
( ~ k04_buttercup10602(X0)
| b48_buttercup10604(X0) ) ).
cnf(u3008,axiom,
b48_buttercup10526(sK410) ).
cnf(u4379,axiom,
k04_buttercup10190(sK469) ).
cnf(u2484,axiom,
~ b48_buttercup10179(sK104) ).
cnf(u1998,axiom,
( ~ k04_buttercup10096(X0)
| k04_buttercup10095(X0) ) ).
cnf(u3029,axiom,
b48_buttercup10636(sK431) ).
cnf(u2665,axiom,
k04_buttercup10164(sK147) ).
cnf(u2179,axiom,
( ~ b48_buttercup10065(X0)
| b48_buttercup10054(X0) ) ).
cnf(u2544,axiom,
~ b48_buttercup10104(sK121) ).
cnf(u2593,axiom,
( ~ b48_buttercup10362(X0)
| k04_buttercup10364(X0) ) ).
cnf(u2235,axiom,
k04_buttercup10464(sK32) ).
cnf(u3038,axiom,
b48_buttercup10518(sK440) ).
cnf(u2255,axiom,
( ~ b48_buttercup10082(X0)
| k04_buttercup10084(X0) ) ).
cnf(u5280,axiom,
k04_buttercup10012(sK391) ).
cnf(u2307,axiom,
( ~ b48_buttercup10199(X0)
| k04_buttercup10200(X0) ) ).
cnf(u4489,axiom,
b48_buttercup10552(sK278) ).
cnf(u2654,axiom,
( ~ k04_buttercup10312(X0)
| b48_buttercup10309(X0) ) ).
cnf(u5182,axiom,
b48_buttercup10417(sK405) ).
cnf(u4436,axiom,
k04_buttercup10635(sK320) ).
cnf(u4065,axiom,
k04_buttercup10012(sK230) ).
cnf(u2085,axiom,
( ~ k04_buttercup10389(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2582,axiom,
~ b48_buttercup10440(sK133) ).
cnf(u2988,axiom,
b48_buttercup10561(sK390) ).
cnf(u4617,axiom,
k04_buttercup10012(sK383) ).
cnf(u2714,axiom,
~ b48_buttercup10191(sK157) ).
cnf(u4581,axiom,
b48_buttercup10054(sK194) ).
cnf(u4493,axiom,
k04_buttercup10555(sK388) ).
cnf(u2145,axiom,
( ~ b48_buttercup10479(X0)
| b48_buttercup10474(X0) ) ).
cnf(u2811,axiom,
k04_buttercup10061(sK213) ).
cnf(u3057,axiom,
b48_buttercup10110(sK459) ).
cnf(u4424,axiom,
b48_buttercup10332(sK266) ).
cnf(u4324,axiom,
b48_buttercup10231(sK272) ).
cnf(u5190,axiom,
k04_buttercup10012(sK362) ).
cnf(u4028,axiom,
k04_buttercup10012(sK284) ).
cnf(u4621,axiom,
k04_buttercup10477(sK367) ).
cnf(u2939,axiom,
b48_buttercup10624(sK341) ).
cnf(u2761,axiom,
b48_buttercup10222(sK167) ).
cnf(u4346,axiom,
k04_buttercup10586(sK346) ).
cnf(u4240,axiom,
b48_buttercup10474(sK397) ).
cnf(u4078,axiom,
k04_buttercup10012(sK212) ).
cnf(u5106,axiom,
k04_buttercup10012(sK347) ).
cnf(u2134,axiom,
( ~ b48_buttercup10193(X0)
| b48_buttercup10186(X0) ) ).
cnf(u2549,axiom,
~ b48_buttercup10110(sK122) ).
cnf(u2477,axiom,
( ~ b48_buttercup10454(X0)
| k04_buttercup10464(X0) ) ).
cnf(u4868,axiom,
k04_buttercup10477(sK338) ).
cnf(u4722,axiom,
k04_buttercup10337(sK331) ).
cnf(u4153,axiom,
k04_buttercup10012(sK31) ).
cnf(u2605,axiom,
k04_buttercup10347(sK139) ).
cnf(u2232,axiom,
k04_buttercup10464(sK31) ).
cnf(u2007,axiom,
( ~ k04_buttercup10486(X0)
| k04_buttercup10477(X0) ) ).
cnf(u2965,axiom,
b48_buttercup10489(sK367) ).
cnf(u4353,axiom,
b48_buttercup10294(sK288) ).
cnf(u2841,axiom,
k04_buttercup10415(sK243) ).
cnf(u4432,axiom,
b48_buttercup10632(sK227) ).
cnf(u4142,axiom,
k04_buttercup10012(sK168) ).
cnf(u2684,axiom,
( ~ b48_buttercup10214(X0)
| k04_buttercup10608(X0) ) ).
cnf(u4274,axiom,
b48_buttercup10054(sK332) ).
cnf(u3951,axiom,
k04_buttercup10048(sK297) ).
cnf(u3069,axiom,
b48_buttercup10193(sK471) ).
cnf(u5001,axiom,
~ k04_buttercup10100(sK287) ).
cnf(u4259,axiom,
b48_buttercup10313(sK402) ).
cnf(u4138,axiom,
k04_buttercup10012(sK256) ).
cnf(u4730,axiom,
b48_buttercup10446(sK33) ).
cnf(u3981,axiom,
k04_buttercup10593(sK221) ).
cnf(u4587,axiom,
k04_buttercup10057(sK332) ).
cnf(u2006,axiom,
( ~ k04_buttercup10482(X0)
| k04_buttercup10477(X0) ) ).
cnf(u4534,axiom,
b48_buttercup10220(sK224) ).
cnf(u4864,axiom,
b48_buttercup10474(sK252) ).
cnf(u2070,axiom,
( ~ k04_buttercup10117(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2055,axiom,
( ~ k04_buttercup10329(X0)
| k04_buttercup10012(X0) ) ).
cnf(u3993,axiom,
k04_buttercup10026(sK276) ).
cnf(u2898,axiom,
k04_buttercup10213(sK300) ).
cnf(u4150,axiom,
k04_buttercup10012(sK274) ).
cnf(u4522,axiom,
k04_buttercup10012(sK337) ).
cnf(u4863,axiom,
b48_buttercup10474(sK207) ).
cnf(u5277,axiom,
b48_buttercup10446(sK359) ).
cnf(u2296,axiom,
( ~ k04_buttercup10495(X0)
| b48_buttercup10493(X0) ) ).
cnf(u2611,axiom,
( ~ k04_buttercup10510(X0)
| b48_buttercup10507(X0) ) ).
cnf(u2848,axiom,
k04_buttercup10125(sK250) ).
cnf(u2631,axiom,
k04_buttercup10567(sK141) ).
cnf(u4135,axiom,
k04_buttercup10012(sK249) ).
cnf(u2224,axiom,
k04_buttercup10225(sK29) ).
cnf(u4267,axiom,
b48_buttercup10150(sK372) ).
cnf(u3074,axiom,
b48_buttercup10352(sK476) ).
cnf(u2687,axiom,
( ~ k04_buttercup10221(X0)
| b48_buttercup10208(X0) ) ).
cnf(u4501,axiom,
b48_buttercup10563(sK141) ).
cnf(u4551,axiom,
k04_buttercup10593(sK385) ).
cnf(u2447,axiom,
( ~ k04_buttercup10529(X0)
| b48_buttercup10526(X0) ) ).
cnf(u2035,axiom,
( ~ k04_buttercup10620(X0)
| k04_buttercup10619(X0) ) ).
cnf(u2281,axiom,
( ~ b48_buttercup10582(X0)
| k04_buttercup10586(X0) ) ).
cnf(u4123,axiom,
k04_buttercup10012(sK183) ).
cnf(u2066,axiom,
( ~ k04_buttercup10084(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4271,axiom,
b48_buttercup10054(sK468) ).
cnf(u4402,axiom,
k04_buttercup10012(sK457) ).
cnf(u4036,axiom,
k04_buttercup10012(sK289) ).
cnf(u4248,axiom,
b48_buttercup10161(sK306) ).
cnf(u2668,axiom,
k04_buttercup10164(sK148) ).
cnf(u2947,axiom,
b48_buttercup10483(sK349) ).
cnf(u4711,axiom,
k04_buttercup10051(sK464) ).
cnf(u2800,axiom,
k04_buttercup10234(sK202) ).
cnf(u4957,axiom,
k04_buttercup10033(sK416) ).
cnf(u2783,axiom,
k04_buttercup10445(sK185) ).
cnf(u2270,axiom,
( ~ b48_buttercup10022(X0)
| k04_buttercup10016(X0) ) ).
cnf(u3023,axiom,
b48_buttercup10549(sK425) ).
cnf(u2051,axiom,
( ~ k04_buttercup10303(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4252,axiom,
b48_buttercup10589(sK385) ).
cnf(u3978,axiom,
k04_buttercup10544(sK270) ).
cnf(u4233,axiom,
b48_buttercup10334(sK446) ).
cnf(u4699,axiom,
k04_buttercup10048(sK313) ).
cnf(u2107,axiom,
( ~ k04_buttercup10529(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2910,axiom,
b48_buttercup10260(sK312) ).
cnf(u2127,axiom,
( ~ b48_buttercup10305(X0)
| b48_buttercup10300(X0) ) ).
cnf(u4339,axiom,
k04_buttercup10084(sK381) ).
cnf(u2015,axiom,
( ~ k04_buttercup10238(X0)
| k04_buttercup10234(X0) ) ).
cnf(u2741,axiom,
( ~ b48_buttercup10427(X0)
| k04_buttercup10430(X0) ) ).
cnf(u4361,axiom,
b48_buttercup10065(sK261) ).
cnf(u2970,axiom,
b48_buttercup10156(sK372) ).
cnf(u4237,axiom,
b48_buttercup10474(sK335) ).
cnf(u3950,axiom,
k04_buttercup10048(sK179) ).
cnf(u2180,axiom,
( ~ b48_buttercup10068(X0)
| b48_buttercup10054(X0) ) ).
cnf(u2801,axiom,
k04_buttercup10371(sK203) ).
cnf(u4680,axiom,
k04_buttercup10544(sK421) ).
cnf(u2860,axiom,
k04_buttercup10033(sK262) ).
cnf(u2586,axiom,
~ b48_buttercup10441(sK135) ).
cnf(u2236,axiom,
( ~ b48_buttercup10467(X0)
| k04_buttercup10464(X0) ) ).
cnf(u2683,axiom,
( ~ k04_buttercup10608(X0)
| b48_buttercup10214(X0) ) ).
cnf(u2929,axiom,
b48_buttercup10176(sK331) ).
cnf(u2443,axiom,
( ~ b48_buttercup10515(X0)
| k04_buttercup10516(X0) ) ).
cnf(u4131,axiom,
k04_buttercup10012(sK225) ).
cnf(u2293,axiom,
( ~ b48_buttercup10065(X0)
| k04_buttercup10067(X0) ) ).
cnf(u2790,axiom,
k04_buttercup10504(sK192) ).
cnf(u4112,axiom,
k04_buttercup10012(sK149) ).
cnf(u2221,axiom,
k04_buttercup10225(sK28) ).
cnf(u4978,axiom,
k04_buttercup10012(sK334) ).
cnf(u5256,axiom,
k04_buttercup10012(sK331) ).
cnf(u2421,axiom,
( ~ b48_buttercup10629(X0)
| k04_buttercup10631(X0) ) ).
cnf(u2785,axiom,
k04_buttercup10139(sK187) ).
cnf(u2812,axiom,
k04_buttercup10385(sK214) ).
cnf(u4595,axiom,
k04_buttercup10012(sK453) ).
cnf(u2349,axiom,
( ~ b48_buttercup10107(X0)
| k04_buttercup10620(X0) ) ).
cnf(u5071,axiom,
k04_buttercup10012(sK311) ).
cnf(u4542,axiom,
k04_buttercup10147(sK428) ).
cnf(u3019,axiom,
b48_buttercup10542(sK421) ).
cnf(u5300,axiom,
k04_buttercup10012(sK454) ).
cnf(u4599,axiom,
k04_buttercup10602(sK385) ).
cnf(u4398,axiom,
b48_buttercup10434(sK274) ).
cnf(u4059,axiom,
k04_buttercup10012(sK304) ).
cnf(u4530,axiom,
k04_buttercup10012(sK429) ).
cnf(u2982,axiom,
b48_buttercup10605(sK384) ).
cnf(u2813,axiom,
k04_buttercup10510(sK215) ).
cnf(u5103,axiom,
k04_buttercup10012(sK386) ).
cnf(u5042,axiom,
k04_buttercup10012(sK419) ).
cnf(u4022,axiom,
k04_buttercup10012(sK182) ).
cnf(u4222,axiom,
b48_buttercup10300(sK479) ).
cnf(u5027,axiom,
k04_buttercup10012(sK394) ).
cnf(u2941,axiom,
b48_buttercup10589(sK343) ).
cnf(u3987,axiom,
k04_buttercup10369(sK199) ).
cnf(u3959,axiom,
k04_buttercup10337(sK305) ).
cnf(u2043,axiom,
( ~ k04_buttercup10204(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4380,axiom,
b48_buttercup10549(sK280) ).
cnf(u2600,axiom,
k04_buttercup10316(sK138) ).
cnf(u4852,axiom,
b48_buttercup10222(sK29) ).
cnf(u2823,axiom,
k04_buttercup10391(sK225) ).
cnf(u4900,axiom,
k04_buttercup10373(sK340) ).
cnf(u5249,axiom,
k04_buttercup10012(sK437) ).
cnf(u4406,axiom,
b48_buttercup10013(sK230) ).
cnf(u4825,axiom,
k04_buttercup10012(sK428) ).
cnf(u5181,axiom,
k04_buttercup10012(sK358) ).
cnf(u4840,axiom,
k04_buttercup10608(sK396) ).
cnf(u2552,axiom,
( ~ k04_buttercup10482(X0)
| b48_buttercup10479(X0) ) ).
cnf(u2825,axiom,
k04_buttercup10637(sK227) ).
cnf(u4903,axiom,
b48_buttercup10374(sK199) ).
cnf(u2480,axiom,
( ~ k04_buttercup10567(X0)
| b48_buttercup10563(X0) ) ).
cnf(u4814,axiom,
k04_buttercup10164(sK310) ).
cnf(u2168,axiom,
( ~ b48_buttercup10174(X0)
| b48_buttercup10170(X0) ) ).
cnf(u4245,axiom,
b48_buttercup10402(sK393) ).
cnf(u2096,axiom,
( ~ k04_buttercup10449(X0)
| k04_buttercup10012(X0) ) ).
cnf(u3033,axiom,
b48_buttercup10104(sK435) ).
cnf(u2322,axiom,
k04_buttercup10622(sK51) ).
cnf(u2996,axiom,
b48_buttercup10120(sK398) ).
cnf(u2319,axiom,
( ~ k04_buttercup10547(X0)
| b48_buttercup10548(X0) ) ).
cnf(u2722,axiom,
( ~ k04_buttercup10117(X0)
| b48_buttercup10115(X0) ) ).
cnf(u4218,axiom,
b48_buttercup10046(sK463) ).
cnf(u4504,axiom,
b48_buttercup10563(sK235) ).
cnf(u2153,axiom,
( ~ b48_buttercup10166(X0)
| b48_buttercup10161(X0) ) ).
cnf(u3056,axiom,
b48_buttercup10111(sK458) ).
cnf(u4701,axiom,
k04_buttercup10048(sK463) ).
cnf(u4143,axiom,
k04_buttercup10012(sK170) ).
cnf(u2081,axiom,
( ~ k04_buttercup10369(X0)
| k04_buttercup10012(X0) ) ).
cnf(u4073,axiom,
k04_buttercup10012(sK245) ).
cnf(u4120,axiom,
k04_buttercup10012(sK135) ).
cnf(u2767,axiom,
~ k04_buttercup10419(sK173) ).
cnf(u4754,axiom,
k04_buttercup10408(sK393) ).
cnf(u2819,axiom,
k04_buttercup10599(sK221) ).
cnf(u2672,axiom,
( ~ b48_buttercup10167(X0)
| k04_buttercup10164(X0) ) ).
cnf(u4064,axiom,
k04_buttercup10012(sK44) ).
cnf(u4895,axiom,
k04_buttercup10371(sK344) ).
cnf(u2142,axiom,
( ~ b48_buttercup10441(X0)
| b48_buttercup10440(X0) ) ).
cnf(u2895,axiom,
k04_buttercup10051(sK297) ).
cnf(u2274,axiom,
~ b48_buttercup10019(sK44) ).
cnf(u4674,axiom,
k04_buttercup10347(sK450) ).
cnf(u4124,axiom,
k04_buttercup10012(sK199) ).
cnf(u2837,axiom,
k04_buttercup10096(sK239) ).
cnf(u4105,axiom,
k04_buttercup10012(sK27) ).
cnf(u4109,axiom,
k04_buttercup10012(sK226) ).
cnf(u2436,axiom,
~ b48_buttercup10068(sK90) ).
cnf(u2545,axiom,
k04_buttercup10622(sK121) ).
cnf(u4936,axiom,
k04_buttercup10117(sK454) ).
cnf(u2613,axiom,
( ~ k04_buttercup10048(X0)
| b48_buttercup10046(X0) ) ).
cnf(u4723,axiom,
b48_buttercup10451(sK301) ).
cnf(u4605,axiom,
k04_buttercup10599(sK369) ).
cnf(u2492,axiom,
~ b48_buttercup10085(sK106) ).
cnf(u3045,axiom,
b48_buttercup10229(sK447) ).
cnf(u2496,axiom,
b48_buttercup10458(sK107) ).
cnf(u4241,axiom,
b48_buttercup10474(sK367) ).
cnf(u2673,axiom,
~ b48_buttercup10174(sK150) ).
cnf(u2187,axiom,
( ~ b48_buttercup10519(X0)
| b48_buttercup10515(X0) ) ).
cnf(u4226,axiom,
b48_buttercup10186(sK473) ).
cnf(u2108,axiom,
( ~ k04_buttercup10535(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2387,axiom,
~ b48_buttercup10111(sK78) ).
cnf(u2037,axiom,
( ~ k04_buttercup10506(X0)
| k04_buttercup10504(X0) ) ).
cnf(u4853,axiom,
b48_buttercup10222(sK284) ).
cnf(u2315,axiom,
( ~ k04_buttercup10551(X0)
| b48_buttercup10549(X0) ) ).
cnf(u2734,axiom,
( ~ k04_buttercup10033(X0)
| b48_buttercup10031(X0) ) ).
cnf(u2165,axiom,
( ~ b48_buttercup10318(X0)
| b48_buttercup10313(X0) ) ).
cnf(u4230,axiom,
b48_buttercup10130(sK417) ).
cnf(u2662,axiom,
( ~ k04_buttercup10172(X0)
| b48_buttercup10170(X0) ) ).
cnf(u2949,axiom,
b48_buttercup10383(sK351) ).
cnf(u2794,axiom,
k04_buttercup10477(sK196) ).
cnf(u2093,axiom,
( ~ k04_buttercup10430(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2225,axiom,
( ~ b48_buttercup10229(X0)
| k04_buttercup10225(X0) ) ).
cnf(u2763,axiom,
~ b48_buttercup10228(sK170) ).
cnf(u3009,axiom,
b48_buttercup10579(sK411) ).
cnf(u3077,axiom,
b48_buttercup10308(sK479) ).
cnf(u3980,axiom,
k04_buttercup10404(sK256) ).
cnf(u4414,axiom,
k04_buttercup10356(sK413) ).
cnf(u2891,axiom,
k04_buttercup10057(sK293) ).
cnf(u2001,axiom,
( ~ k04_buttercup10347(X0)
| k04_buttercup10337(X0) ) ).
cnf(u4735,axiom,
b48_buttercup10446(sK219) ).
cnf(u2214,axiom,
( ~ b48_buttercup10156(X0)
| k04_buttercup10153(X0) ) ).
cnf(u2501,axiom,
( ~ k04_buttercup10206(X0)
| b48_buttercup10220(X0) ) ).
cnf(u4861,axiom,
b48_buttercup10474(sK124) ).
cnf(u2708,axiom,
( ~ k04_buttercup10376(X0)
| b48_buttercup10374(X0) ) ).
cnf(u4602,axiom,
b48_buttercup10596(sK221) ).
cnf(u2440,axiom,
( ~ b48_buttercup10421(X0)
| k04_buttercup10517(X0) ) ).
cnf(u2854,axiom,
k04_buttercup10408(sK256) ).
cnf(u5157,axiom,
k04_buttercup10012(sK445) ).
cnf(u5017,axiom,
k04_buttercup10012(sK108) ).
cnf(u2685,axiom,
( ~ k04_buttercup10219(X0)
| b48_buttercup10217(X0) ) ).
cnf(u2856,axiom,
k04_buttercup10404(sK258) ).
cnf(u4031,axiom,
k04_buttercup10012(sK195) ).
cnf(u4203,axiom,
k04_buttercup10012(sK120) ).
cnf(u4351,axiom,
b48_buttercup10383(sK210) ).
cnf(u4834,axiom,
k04_buttercup10611(sK395) ).
cnf(u3021,axiom,
b48_buttercup10545(sK423) ).
cnf(u5121,axiom,
k04_buttercup10012(sK380) ).
cnf(u5276,axiom,
k04_buttercup10012(sK455) ).
cnf(u2808,axiom,
k04_buttercup10382(sK210) ).
cnf(u4117,axiom,
k04_buttercup10012(sK285) ).
cnf(u4211,axiom,
k04_buttercup10012(sK186) ).
cnf(u4332,axiom,
b48_buttercup10616(sK225) ).
cnf(u4061,axiom,
k04_buttercup10012(sK303) ).
cnf(u4321,axiom,
k04_buttercup10225(sK447) ).
cnf(u4779,axiom,
b48_buttercup10130(sK265) ).
cnf(u5022,axiom,
k04_buttercup10012(sK318) ).
cnf(u2424,axiom,
( ~ b48_buttercup10075(X0)
| k04_buttercup10064(X0) ) ).
cnf(u3986,axiom,
k04_buttercup10369(sK201) ).
cnf(u2135,axiom,
( ~ b48_buttercup10195(X0)
| b48_buttercup10186(X0) ) ).
cnf(u4320,axiom,
k04_buttercup10225(sK472) ).
cnf(u2706,axiom,
( ~ k04_buttercup10373(X0)
| b48_buttercup10377(X0) ) ).
cnf(u4385,axiom,
k04_buttercup10547(sK424) ).
cnf(u4317,axiom,
b48_buttercup10150(sK118) ).
cnf(u4008,axiom,
k04_buttercup10619(sK51) ).
cnf(u2978,axiom,
b48_buttercup10496(sK380) ).
cnf(u3989,axiom,
k04_buttercup10293(sK291) ).
cnf(u5226,axiom,
k04_buttercup10012(sK352) ).
cnf(u2901,axiom,
k04_buttercup10356(sK303) ).
cnf(u2045,axiom,
( ~ k04_buttercup10225(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2868,axiom,
k04_buttercup10547(sK270) ).
cnf(u4310,axiom,
k04_buttercup10535(sK315) ).
cnf(u2594,axiom,
~ k04_buttercup10282(sK137) ).
cnf(u3000,axiom,
b48_buttercup10320(sK402) ).
cnf(u4376,axiom,
b48_buttercup10199(sK178) ).
cnf(u2248,axiom,
( ~ k04_buttercup10391(X0)
| b48_buttercup10616(X0) ) ).
cnf(u2563,axiom,
( ~ k04_buttercup10096(X0)
| b48_buttercup10092(X0) ) ).
cnf(u4764,axiom,
k04_buttercup10404(sK412) ).
cnf(u2928,axiom,
b48_buttercup10174(sK330) ).
cnf(u2176,axiom,
( ~ b48_buttercup10159(X0)
| b48_buttercup10150(X0) ) ).
cnf(u2639,axiom,
( ~ b48_buttercup10574(X0)
| k04_buttercup10567(X0) ) ).
cnf(u2530,axiom,
( ~ k04_buttercup10164(X0)
| b48_buttercup10161(X0) ) ).
cnf(u2527,axiom,
~ b48_buttercup10159(sK118) ).
cnf(u5069,axiom,
k04_buttercup10012(sK310) ).
cnf(u5232,axiom,
k04_buttercup10012(sK367) ).
cnf(u2146,axiom,
( ~ b48_buttercup10483(X0)
| b48_buttercup10474(X0) ) ).
cnf(u2692,axiom,
( ~ k04_buttercup10225(X0)
| b48_buttercup10222(X0) ) ).
cnf(u2074,axiom,
( ~ k04_buttercup10139(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2489,axiom,
( ~ b48_buttercup10398(X0)
| k04_buttercup10400(X0) ) ).
cnf(u3027,axiom,
b48_buttercup10022(sK429) ).
cnf(u2308,axiom,
~ k04_buttercup10204(sK48) ).
cnf(u2417,axiom,
( ~ b48_buttercup10632(X0)
| k04_buttercup10635(X0) ) ).
cnf(u2445,axiom,
b48_buttercup10417(sK92) ).
cnf(u4482,axiom,
k04_buttercup10012(sK447) ).
cnf(u4956,axiom,
k04_buttercup10012(sK402) ).
cnf(u2617,axiom,
( ~ k04_buttercup10051(X0)
| b48_buttercup10050(X0) ) ).
cnf(u2131,axiom,
( ~ b48_buttercup10228(X0)
| b48_buttercup10222(X0) ) ).
cnf(u4058,axiom,
k04_buttercup10012(sK286) ).
cnf(u2059,axiom,
( ~ k04_buttercup10016(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2990,axiom,
b48_buttercup10086(sK392) ).
cnf(u4098,axiom,
k04_buttercup10012(sK265) ).
cnf(u2207,axiom,
( ~ b48_buttercup10636(X0)
| k04_buttercup10637(X0) ) ).
cnf(u5147,axiom,
k04_buttercup10026(sK416) ).
cnf(u2693,axiom,
( ~ k04_buttercup10477(X0)
| b48_buttercup10474(X0) ) ).
cnf(u3050,axiom,
b48_buttercup10294(sK452) ).
cnf(u2606,axiom,
( ~ b48_buttercup10343(X0)
| k04_buttercup10347(X0) ) ).
cnf(u4017,axiom,
k04_buttercup10012(sK49) ).
cnf(u4102,axiom,
k04_buttercup10012(sK209) ).
cnf(u2940,axiom,
b48_buttercup10374(sK342) ).
cnf(u4067,axiom,
k04_buttercup10012(sK276) ).
cnf(u2666,axiom,
( ~ b48_buttercup10169(X0)
| k04_buttercup10164(X0) ) ).
cnf(u2188,axiom,
( ~ b48_buttercup10520(X0)
| b48_buttercup10515(X0) ) ).
cnf(u2042,axiom,
( ~ k04_buttercup10200(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2877,axiom,
k04_buttercup10555(sK279) ).
cnf(u2635,axiom,
( ~ k04_buttercup10408(X0)
| b48_buttercup10410(X0) ) ).
cnf(u2542,axiom,
k04_buttercup10622(sK120) ).
cnf(u2881,axiom,
k04_buttercup10424(sK283) ).
cnf(u2523,axiom,
( ~ b48_buttercup10158(X0)
| k04_buttercup10153(X0) ) ).
cnf(u2245,axiom,
k04_buttercup10464(sK34) ).
cnf(u4773,axiom,
k04_buttercup10132(sK419) ).
cnf(u4215,axiom,
k04_buttercup10012(sK294) ).
cnf(u2301,axiom,
k04_buttercup10486(sK46) ).
cnf(u4340,axiom,
k04_buttercup10016(sK429) ).
cnf(u2086,axiom,
( ~ k04_buttercup10391(X0)
| k04_buttercup10012(X0) ) ).
cnf(u2764,axiom,
k04_buttercup10419(sK170) ).
cnf(u4818,axiom,
k04_buttercup10172(sK330) ).
cnf(u2429,axiom,
( ~ b48_buttercup10352(X0)
| k04_buttercup10347(X0) ) ).
cnf(u2290,axiom,
( ~ k04_buttercup10293(X0)
| b48_buttercup10291(X0) ) ).
cnf(u4196,axiom,
k04_buttercup10012(sK205) ).
cnf(u4328,axiom,
k04_buttercup10464(sK360) ).
cnf(u4325,axiom,
k04_buttercup10234(sK422) ).
cnf(u5302,axiom,
k04_buttercup10012(sK307) ).
cnf(u4815,axiom,
k04_buttercup10449(sK264) ).
cnf(u2539,axiom,
( ~ k04_buttercup10599(X0)
| b48_buttercup10596(X0) ) ).
cnf(u4030,axiom,
k04_buttercup10012(sK202) ).
cnf(u3062,axiom,
b48_buttercup10050(sK464) ).
cnf(u4826,axiom,
b48_buttercup10240(sK255) ).
cnf(u4313,axiom,
b48_buttercup10150(sK26) ).
cnf(u2765,axiom,
( ~ b48_buttercup10228(X0)
| k04_buttercup10419(X0) ) ).
cnf(u4772,axiom,
k04_buttercup10449(sK359) ).
cnf(u4223,axiom,
b48_buttercup10222(sK472) ).
cnf(u3974,axiom,
k04_buttercup10477(sK123) ).
cnf(u2893,axiom,
k04_buttercup10529(sK295) ).
cnf(u4588,axiom,
k04_buttercup10057(sK333) ).
cnf(u5248,axiom,
k04_buttercup10012(sK434) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SYO581+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.24 % Computer : n013.cluster.edu
% 0.11/0.24 % Model : x86_64 x86_64
% 0.11/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.24 % Memory : 8046.5625MB
% 0.11/0.24 % OS : Linux 6.8.0-71-generic
% 0.11/0.24 % CPULimit : 300
% 0.11/0.24 % WCLimit : 300
% 0.11/0.24 % DateTime : Mon Sep 28 17:48:36 UTC 2026
% 0.11/0.25 % CPUTime :
% 0.11/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.23/0.29 Running first-order model finding
% 0.23/0.29 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.23/0.39 % (1393245)Will run a generic schedule for satisfiability detection.
% 0.23/0.39 % (1393253)% WARNING: option uhcvi not known.
% 0.23/0.39 % (1393255)dis+10_1_sil=32000:sp=arity:random_seed=2572715748:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.23/0.39 % (1393253)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1270418424:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.23/0.39 % (1393252)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3486203666_2999 on theBenchmark for (2999ds/0Mi)
% 0.23/0.39 % (1393258)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1066055258:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.23/0.39 % (1393254)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=637484791:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.23/0.39 % (1393256)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3963969649:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.23/0.39 % (1393257)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=509081597:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.23/0.39 % (1393255) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1393245-1393255"...
% 0.23/0.39 % (1393255)...printing done.
% 0.23/0.39 % SZS status CounterSatisfiable for theBenchmark
% 0.23/0.39 % SZS output start Saturation.
% See solution above
% 0.74/0.43 % SZS output start Definitions and Model Updates.
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10612(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10279(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10275(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10277(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10276(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10278(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10274(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10247(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10024(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10268(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10267(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10266(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10606(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10433(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10522(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10201(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10182(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10530(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10197(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10450(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10196(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10420(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10514(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10513(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10512(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10198(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10098(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10646(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10272(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10365(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10273(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10271(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10007(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define k04_buttercup10259(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10358(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define k04_buttercup10255(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10253(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define k04_buttercup10042(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10045(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define k04_buttercup10044(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10043(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define k04_buttercup10539(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10538(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define k04_buttercup10540(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10541(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define k04_buttercup10360(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10359(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define k04_buttercup10286(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10283(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define k04_buttercup10357(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10361(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define k04_buttercup10288(X0) := $true
% 0.74/0.43 for all inputs,
% 0.74/0.43 define b48_buttercup10290(X0) := $true
% 0.74/0.43 for all groundings,
% 0.74/0.43 whenever b48_buttercup10290(X0) is true, set k04_buttercup10288(X0) to true
% 0.74/0.43 for all groundings,
% 0.74/0.43 whenever b48_buttercup10361(X0) is true, set k04_buttercup10357(X0) to true
% 0.74/0.43 for all groundings,
% 0.74/0.43 whenever b48_buttercup10283(X0) is true, set k04_buttercup10286(X0) to true
% 0.74/0.43 for all groundings,
% 0.74/0.43 whenever b48_buttercup10359(X0) is true, set k04_buttercup10360(X0) to true
% 0.74/0.43 for all groundings,
% 0.74/0.43 whenever b48_buttercup10541(X0) is true, set k04_buttercup10540(X0) to true
% 0.74/0.43 for all groundings,
% 0.74/0.43 whenever b48_buttercup10538(X0) is true, set k04_buttercup10539(X0) to true
% 0.74/0.43 for all groundings,
% 0.74/0.43 whenever b48_buttercup10043(X0) is true, set k04_buttercup10044(X0) to true
% 0.74/0.43 for all groundings,
% 0.74/0.43 whenever b48_buttercup10045(X0) is true, set k04_buttercup10042(X0) to true
% 0.74/0.43 for all groundings,
% 0.74/0.43 whenever b48_buttercup10253(X0) is true, set k04_buttercup10255(X0) to true
% 0.74/0.43 % SZS output end Definitions and Model Updates.
% 0.74/0.43 % (1393255)------------------------------
% 0.74/0.43 % (1393255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.43 % (1393255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.43 % (1393255)CaDiCaL version: 2.1.3
% 0.74/0.43 % (1393255)Termination reason: Satisfiable
% 0.74/0.43 % (1393255)Time elapsed: 0.040 s
% 0.74/0.43 % (1393255)Peak memory usage: 14 MB
% 0.74/0.43 % (1393255)Instructions burned: 67 (million)
% 0.74/0.43 % (1393245)Success in time 0.087 s
% 0.74/0.43 % Vampire exiting
%------------------------------------------------------------------------------