%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL649+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 11:54:01 AM UTC 2026
% Result : CounterSatisfiable 10.93s 2.49s
% Output : Saturation 11.98s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2517,negated_conjecture,
p101(sK731) ).
cnf(u2548,negated_conjecture,
~ p201(sK731) ).
cnf(u2553,negated_conjecture,
p202(sK731) ).
cnf(u2581,negated_conjecture,
~ p301(sK731) ).
cnf(u2585,negated_conjecture,
~ p302(sK731) ).
cnf(u2590,negated_conjecture,
p303(sK731) ).
cnf(u2615,negated_conjecture,
~ p401(sK731) ).
cnf(u2619,negated_conjecture,
~ p402(sK731) ).
cnf(u2623,negated_conjecture,
~ p403(sK731) ).
cnf(u2628,negated_conjecture,
p404(sK731) ).
cnf(u2650,negated_conjecture,
~ p501(sK731) ).
cnf(u2654,negated_conjecture,
~ p502(sK731) ).
cnf(u2658,negated_conjecture,
~ p503(sK731) ).
cnf(u2662,negated_conjecture,
~ p504(sK731) ).
cnf(u2667,negated_conjecture,
p505(sK731) ).
cnf(u2686,negated_conjecture,
~ p601(sK731) ).
cnf(u2690,negated_conjecture,
~ p602(sK731) ).
cnf(u2694,negated_conjecture,
~ p603(sK731) ).
cnf(u2698,negated_conjecture,
~ p604(sK731) ).
cnf(u2702,negated_conjecture,
~ p605(sK731) ).
cnf(u2707,negated_conjecture,
p606(sK731) ).
cnf(u2723,negated_conjecture,
~ p801(sK731) ).
cnf(u2727,negated_conjecture,
~ p802(sK731) ).
cnf(u2731,negated_conjecture,
~ p803(sK731) ).
cnf(u2735,negated_conjecture,
~ p804(sK731) ).
cnf(u2739,negated_conjecture,
~ p805(sK731) ).
cnf(u2743,negated_conjecture,
~ p806(sK731) ).
cnf(u2748,negated_conjecture,
p807(sK731) ).
cnf(u2751,negated_conjecture,
~ p808(sK731) ).
cnf(u2762,negated_conjecture,
~ p901(sK731) ).
cnf(u2766,negated_conjecture,
~ p902(sK731) ).
cnf(u2770,negated_conjecture,
~ p903(sK731) ).
cnf(u2774,negated_conjecture,
~ p904(sK731) ).
cnf(u2778,negated_conjecture,
~ p905(sK731) ).
cnf(u2782,negated_conjecture,
~ p906(sK731) ).
cnf(u2786,negated_conjecture,
~ p907(sK731) ).
cnf(u2790,negated_conjecture,
~ p908(sK731) ).
cnf(u2795,negated_conjecture,
p909(sK731) ).
cnf(u2802,negated_conjecture,
~ p1001(sK731) ).
cnf(u2806,negated_conjecture,
~ p1002(sK731) ).
cnf(u2810,negated_conjecture,
~ p1003(sK731) ).
cnf(u2814,negated_conjecture,
~ p1004(sK731) ).
cnf(u2818,negated_conjecture,
~ p1005(sK731) ).
cnf(u2822,negated_conjecture,
~ p1006(sK731) ).
cnf(u2826,negated_conjecture,
~ p1007(sK731) ).
cnf(u2831,negated_conjecture,
p1008(sK731) ).
cnf(u2834,negated_conjecture,
~ p1009(sK731) ).
cnf(u2838,negated_conjecture,
~ p1010(sK731) ).
cnf(u2843,negated_conjecture,
~ p1101(sK731) ).
cnf(u2847,negated_conjecture,
~ p1102(sK731) ).
cnf(u2851,negated_conjecture,
~ p1103(sK731) ).
cnf(u2855,negated_conjecture,
~ p1104(sK731) ).
cnf(u2859,negated_conjecture,
~ p1105(sK731) ).
cnf(u2863,negated_conjecture,
~ p1106(sK731) ).
cnf(u2867,negated_conjecture,
~ p1107(sK731) ).
cnf(u2871,negated_conjecture,
~ p1108(sK731) ).
cnf(u2875,negated_conjecture,
~ p1109(sK731) ).
cnf(u2880,negated_conjecture,
p1110(sK731) ).
cnf(u3480,negated_conjecture,
~ sP300(sK730) ).
cnf(u3484,negated_conjecture,
~ p808(sK730) ).
cnf(u3557,negated_conjecture,
p405(sK303(sK731)) ).
cnf(u3610,negated_conjecture,
~ sP299(sK730) ).
cnf(u3614,negated_conjecture,
~ p1110(sK730) ).
cnf(u3628,negated_conjecture,
~ sP298(sK730) ).
cnf(u3632,negated_conjecture,
~ p1010(sK730) ).
cnf(u3734,negated_conjecture,
~ sP275(sK730) ).
cnf(u3738,negated_conjecture,
~ p1109(sK730) ).
cnf(u3752,negated_conjecture,
~ sP274(sK730) ).
cnf(u3756,negated_conjecture,
~ p1009(sK730) ).
cnf(u3770,negated_conjecture,
~ sP273(sK730) ).
cnf(u3774,negated_conjecture,
~ p909(sK730) ).
cnf(u3905,negated_conjecture,
~ sP247(sK730) ).
cnf(u3909,negated_conjecture,
~ p1108(sK730) ).
cnf(u3923,negated_conjecture,
~ sP246(sK730) ).
cnf(u3927,negated_conjecture,
~ p1008(sK730) ).
cnf(u3941,negated_conjecture,
~ sP245(sK730) ).
cnf(u3945,negated_conjecture,
~ p908(sK730) ).
cnf(u4108,negated_conjecture,
~ p1107(sK730) ).
cnf(u4142,negated_conjecture,
~ sP216(sK730) ).
cnf(u4146,negated_conjecture,
~ p1007(sK730) ).
cnf(u4160,negated_conjecture,
~ sP215(sK730) ).
cnf(u4164,negated_conjecture,
~ p907(sK730) ).
cnf(u4178,negated_conjecture,
~ sP214(sK730) ).
cnf(u4182,negated_conjecture,
~ p807(sK730) ).
cnf(u4323,negated_conjecture,
~ sP193(sK730) ).
cnf(u4327,negated_conjecture,
~ p1106(sK730) ).
cnf(u4341,negated_conjecture,
~ sP192(sK730) ).
cnf(u4345,negated_conjecture,
~ p1006(sK730) ).
cnf(u4359,negated_conjecture,
~ sP191(sK730) ).
cnf(u4363,negated_conjecture,
~ p906(sK730) ).
cnf(u4377,negated_conjecture,
~ sP190(sK730) ).
cnf(u4381,negated_conjecture,
~ p806(sK730) ).
cnf(u4399,negated_conjecture,
~ sP189(sK730) ).
cnf(u4403,negated_conjecture,
~ p606(sK730) ).
cnf(u4717,negated_conjecture,
~ sP168(sK730) ).
cnf(u4721,negated_conjecture,
~ p1105(sK730) ).
cnf(u4735,negated_conjecture,
~ sP167(sK730) ).
cnf(u4739,negated_conjecture,
~ p1005(sK730) ).
cnf(u4753,negated_conjecture,
~ sP166(sK730) ).
cnf(u4757,negated_conjecture,
~ p905(sK730) ).
cnf(u4775,negated_conjecture,
~ sP165(sK730) ).
cnf(u4779,negated_conjecture,
~ p805(sK730) ).
cnf(u4797,negated_conjecture,
~ sP164(sK730) ).
cnf(u4801,negated_conjecture,
~ p605(sK730) ).
cnf(u4815,negated_conjecture,
~ sP163(sK730) ).
cnf(u4819,negated_conjecture,
~ p505(sK730) ).
cnf(u5319,negated_conjecture,
~ sP144(sK730) ).
cnf(u5323,negated_conjecture,
~ p1104(sK730) ).
cnf(u5337,negated_conjecture,
~ sP143(sK730) ).
cnf(u5341,negated_conjecture,
~ p1004(sK730) ).
cnf(u5359,negated_conjecture,
~ sP142(sK730) ).
cnf(u5363,negated_conjecture,
~ p904(sK730) ).
cnf(u5381,negated_conjecture,
~ sP141(sK730) ).
cnf(u5385,negated_conjecture,
~ p804(sK730) ).
cnf(u5399,negated_conjecture,
~ sP140(sK730) ).
cnf(u5403,negated_conjecture,
~ p604(sK730) ).
cnf(u5417,negated_conjecture,
~ sP139(sK730) ).
cnf(u5421,negated_conjecture,
~ p504(sK730) ).
cnf(u5435,negated_conjecture,
~ sP138(sK730) ).
cnf(u5439,negated_conjecture,
~ p404(sK730) ).
cnf(u5602,negated_conjecture,
~ sP123(sK730) ).
cnf(u5606,negated_conjecture,
~ p1103(sK730) ).
cnf(u5624,negated_conjecture,
~ sP122(sK730) ).
cnf(u5628,negated_conjecture,
~ p1003(sK730) ).
cnf(u5646,negated_conjecture,
~ sP121(sK730) ).
cnf(u5650,negated_conjecture,
~ p903(sK730) ).
cnf(u5664,negated_conjecture,
~ sP120(sK730) ).
cnf(u5668,negated_conjecture,
~ p803(sK730) ).
cnf(u5682,negated_conjecture,
~ sP119(sK730) ).
cnf(u5686,negated_conjecture,
~ p603(sK730) ).
cnf(u5700,negated_conjecture,
~ sP118(sK730) ).
cnf(u5704,negated_conjecture,
~ p503(sK730) ).
cnf(u5718,negated_conjecture,
~ sP117(sK730) ).
cnf(u5722,negated_conjecture,
~ p403(sK730) ).
cnf(u5736,negated_conjecture,
~ sP116(sK730) ).
cnf(u5740,negated_conjecture,
~ p303(sK730) ).
cnf(u5874,negated_conjecture,
~ sP107(sK730) ).
cnf(u5892,negated_conjecture,
~ sP106(sK730) ).
cnf(u5910,negated_conjecture,
~ sP105(sK730) ).
cnf(u5928,negated_conjecture,
~ sP104(sK730) ).
cnf(u5946,negated_conjecture,
~ sP103(sK730) ).
cnf(u5968,negated_conjecture,
~ sP102(sK730) ).
cnf(u5990,negated_conjecture,
~ sP101(sK730) ).
cnf(u6008,negated_conjecture,
~ sP100(sK730) ).
cnf(u6026,negated_conjecture,
~ sP99(sK730) ).
cnf(u6832,negated_conjecture,
~ sP295(sK730) ).
cnf(u6841,negated_conjecture,
p304(sK315(sK731)) ).
cnf(u6845,negated_conjecture,
~ p910(sK314(sK731)) ).
cnf(u6850,negated_conjecture,
p203(sK315(sK731)) ).
cnf(u6855,negated_conjecture,
p407(sK315(sK731)) ).
cnf(u6860,negated_conjecture,
p103(sK315(sK731)) ).
cnf(u6865,negated_conjecture,
p809(sK315(sK731)) ).
cnf(u6885,negated_conjecture,
~ sP294(sK730) ).
cnf(u6894,negated_conjecture,
p304(sK317(sK731)) ).
cnf(u6898,negated_conjecture,
~ p810(sK316(sK731)) ).
cnf(u6903,negated_conjecture,
p203(sK317(sK731)) ).
cnf(u6913,negated_conjecture,
p103(sK317(sK731)) ).
cnf(u6918,negated_conjecture,
p809(sK317(sK731)) ).
cnf(u6938,negated_conjecture,
~ sP291(sK730) ).
cnf(u6951,negated_conjecture,
~ p610(sK321(sK731)) ).
cnf(u6991,negated_conjecture,
~ sP288(sK730) ).
cnf(u7004,negated_conjecture,
~ p510(sK325(sK731)) ).
cnf(u7044,negated_conjecture,
~ sP285(sK730) ).
cnf(u7057,negated_conjecture,
~ p410(sK329(sK731)) ).
cnf(u7097,negated_conjecture,
~ sP282(sK730) ).
cnf(u7110,negated_conjecture,
~ p310(sK333(sK731)) ).
cnf(u7150,negated_conjecture,
~ sP279(sK730) ).
cnf(u7163,negated_conjecture,
~ p210(sK337(sK731)) ).
cnf(u7203,negated_conjecture,
~ sP276(sK730) ).
cnf(u7216,negated_conjecture,
~ p110(sK341(sK731)) ).
cnf(u7256,negated_conjecture,
~ sP272(sK730) ).
cnf(u7269,negated_conjecture,
~ p809(sK345(sK731)) ).
cnf(u7309,negated_conjecture,
~ sP268(sK730) ).
cnf(u7322,negated_conjecture,
~ p609(sK351(sK731)) ).
cnf(u7362,negated_conjecture,
~ sP264(sK730) ).
cnf(u7375,negated_conjecture,
~ p509(sK356(sK731)) ).
cnf(u7415,negated_conjecture,
~ sP260(sK730) ).
cnf(u7428,negated_conjecture,
~ p409(sK361(sK731)) ).
cnf(u7468,negated_conjecture,
~ sP256(sK730) ).
cnf(u7481,negated_conjecture,
~ p309(sK366(sK731)) ).
cnf(u7521,negated_conjecture,
~ sP252(sK730) ).
cnf(u7534,negated_conjecture,
~ p209(sK371(sK731)) ).
cnf(u7574,negated_conjecture,
~ sP248(sK730) ).
cnf(u7587,negated_conjecture,
~ p109(sK376(sK731)) ).
cnf(u7627,negated_conjecture,
~ sP243(sK730) ).
cnf(u7640,negated_conjecture,
~ p608(sK382(sK731)) ).
cnf(u7680,negated_conjecture,
~ sP238(sK730) ).
cnf(u7693,negated_conjecture,
~ p508(sK388(sK731)) ).
cnf(u7733,negated_conjecture,
~ sP233(sK730) ).
cnf(u7746,negated_conjecture,
~ p408(sK394(sK731)) ).
cnf(u7786,negated_conjecture,
~ sP228(sK730) ).
cnf(u7799,negated_conjecture,
~ p308(sK400(sK731)) ).
cnf(u7839,negated_conjecture,
~ sP223(sK730) ).
cnf(u7852,negated_conjecture,
~ p208(sK406(sK731)) ).
cnf(u7892,negated_conjecture,
~ sP218(sK730) ).
cnf(u7905,negated_conjecture,
~ p108(sK412(sK731)) ).
cnf(u7945,negated_conjecture,
~ sP98(sK730) ).
cnf(u7958,negated_conjecture,
~ p910(sK532(sK731)) ).
cnf(u7998,negated_conjecture,
~ p810(sK533(sK731)) ).
cnf(u8038,negated_conjecture,
~ sP97(sK730) ).
cnf(u8051,negated_conjecture,
~ p910(sK534(sK731)) ).
cnf(u8091,negated_conjecture,
~ p610(sK535(sK731)) ).
cnf(u8131,negated_conjecture,
~ sP96(sK730) ).
cnf(u8144,negated_conjecture,
~ p810(sK536(sK731)) ).
cnf(u8184,negated_conjecture,
~ p610(sK537(sK731)) ).
cnf(u8224,negated_conjecture,
~ sP95(sK730) ).
cnf(u8237,negated_conjecture,
~ p910(sK538(sK731)) ).
cnf(u8277,negated_conjecture,
~ p510(sK539(sK731)) ).
cnf(u8317,negated_conjecture,
~ sP94(sK730) ).
cnf(u8330,negated_conjecture,
~ p810(sK540(sK731)) ).
cnf(u8370,negated_conjecture,
~ p510(sK541(sK731)) ).
cnf(u8410,negated_conjecture,
~ sP93(sK730) ).
cnf(u8423,negated_conjecture,
~ p610(sK542(sK731)) ).
cnf(u8463,negated_conjecture,
~ p510(sK543(sK731)) ).
cnf(u8503,negated_conjecture,
~ sP92(sK730) ).
cnf(u8516,negated_conjecture,
~ p910(sK544(sK731)) ).
cnf(u8556,negated_conjecture,
~ p410(sK545(sK731)) ).
cnf(u8596,negated_conjecture,
~ sP91(sK730) ).
cnf(u8609,negated_conjecture,
~ p810(sK546(sK731)) ).
cnf(u8649,negated_conjecture,
~ p410(sK547(sK731)) ).
cnf(u8689,negated_conjecture,
~ sP90(sK730) ).
cnf(u8702,negated_conjecture,
~ p610(sK548(sK731)) ).
cnf(u8742,negated_conjecture,
~ p410(sK549(sK731)) ).
cnf(u8782,negated_conjecture,
~ sP89(sK730) ).
cnf(u8795,negated_conjecture,
~ p510(sK550(sK731)) ).
cnf(u8835,negated_conjecture,
~ p410(sK551(sK731)) ).
cnf(u8875,negated_conjecture,
~ sP88(sK730) ).
cnf(u8888,negated_conjecture,
~ p910(sK552(sK731)) ).
cnf(u8928,negated_conjecture,
~ p310(sK553(sK731)) ).
cnf(u8968,negated_conjecture,
~ sP87(sK730) ).
cnf(u8981,negated_conjecture,
~ p810(sK554(sK731)) ).
cnf(u9021,negated_conjecture,
~ p310(sK555(sK731)) ).
cnf(u9061,negated_conjecture,
~ sP86(sK730) ).
cnf(u9074,negated_conjecture,
~ p610(sK556(sK731)) ).
cnf(u9114,negated_conjecture,
~ p310(sK557(sK731)) ).
cnf(u9154,negated_conjecture,
~ sP85(sK730) ).
cnf(u9167,negated_conjecture,
~ p510(sK558(sK731)) ).
cnf(u9207,negated_conjecture,
~ p310(sK559(sK731)) ).
cnf(u9247,negated_conjecture,
~ sP84(sK730) ).
cnf(u9260,negated_conjecture,
~ p410(sK560(sK731)) ).
cnf(u9300,negated_conjecture,
~ p310(sK561(sK731)) ).
cnf(u9340,negated_conjecture,
~ sP83(sK730) ).
cnf(u9353,negated_conjecture,
~ p910(sK562(sK731)) ).
cnf(u9393,negated_conjecture,
~ p210(sK563(sK731)) ).
cnf(u9433,negated_conjecture,
~ sP82(sK730) ).
cnf(u9446,negated_conjecture,
~ p810(sK564(sK731)) ).
cnf(u9486,negated_conjecture,
~ p210(sK565(sK731)) ).
cnf(u9526,negated_conjecture,
~ sP81(sK730) ).
cnf(u9539,negated_conjecture,
~ p610(sK566(sK731)) ).
cnf(u9579,negated_conjecture,
~ p210(sK567(sK731)) ).
cnf(u9619,negated_conjecture,
~ sP80(sK730) ).
cnf(u9632,negated_conjecture,
~ p510(sK568(sK731)) ).
cnf(u9672,negated_conjecture,
~ p210(sK569(sK731)) ).
cnf(u9712,negated_conjecture,
~ sP79(sK730) ).
cnf(u9725,negated_conjecture,
~ p410(sK570(sK731)) ).
cnf(u9765,negated_conjecture,
~ p210(sK571(sK731)) ).
cnf(u9805,negated_conjecture,
~ sP78(sK730) ).
cnf(u9818,negated_conjecture,
~ p310(sK572(sK731)) ).
cnf(u9858,negated_conjecture,
~ p210(sK573(sK731)) ).
cnf(u9898,negated_conjecture,
~ sP77(sK730) ).
cnf(u9911,negated_conjecture,
~ p910(sK574(sK731)) ).
cnf(u9951,negated_conjecture,
~ p110(sK575(sK731)) ).
cnf(u9991,negated_conjecture,
~ sP76(sK730) ).
cnf(u10004,negated_conjecture,
~ p810(sK576(sK731)) ).
cnf(u10044,negated_conjecture,
~ p110(sK577(sK731)) ).
cnf(u10084,negated_conjecture,
~ sP75(sK730) ).
cnf(u10097,negated_conjecture,
~ p610(sK578(sK731)) ).
cnf(u10137,negated_conjecture,
~ p110(sK579(sK731)) ).
cnf(u10177,negated_conjecture,
~ sP74(sK730) ).
cnf(u10190,negated_conjecture,
~ p510(sK580(sK731)) ).
cnf(u10230,negated_conjecture,
~ p110(sK581(sK731)) ).
cnf(u10270,negated_conjecture,
~ sP73(sK730) ).
cnf(u10283,negated_conjecture,
~ p410(sK582(sK731)) ).
cnf(u10323,negated_conjecture,
~ p110(sK583(sK731)) ).
cnf(u10363,negated_conjecture,
~ sP72(sK730) ).
cnf(u10376,negated_conjecture,
~ p310(sK584(sK731)) ).
cnf(u10416,negated_conjecture,
~ p110(sK585(sK731)) ).
cnf(u10456,negated_conjecture,
~ sP71(sK730) ).
cnf(u10469,negated_conjecture,
~ p210(sK586(sK731)) ).
cnf(u10509,negated_conjecture,
~ p110(sK587(sK731)) ).
cnf(u10549,negated_conjecture,
~ sP70(sK730) ).
cnf(u10562,negated_conjecture,
~ p809(sK588(sK731)) ).
cnf(u10602,negated_conjecture,
~ p609(sK589(sK731)) ).
cnf(u10639,negated_conjecture,
~ sP69(sK730) ).
cnf(u10652,negated_conjecture,
~ p809(sK590(sK731)) ).
cnf(u10692,negated_conjecture,
~ p509(sK591(sK731)) ).
cnf(u10729,negated_conjecture,
~ sP68(sK730) ).
cnf(u10742,negated_conjecture,
~ p609(sK592(sK731)) ).
cnf(u10782,negated_conjecture,
~ p509(sK593(sK731)) ).
cnf(u10822,negated_conjecture,
~ sP67(sK730) ).
cnf(u10835,negated_conjecture,
~ p809(sK594(sK731)) ).
cnf(u10875,negated_conjecture,
~ p409(sK595(sK731)) ).
cnf(u10912,negated_conjecture,
~ sP66(sK730) ).
cnf(u10925,negated_conjecture,
~ p609(sK596(sK731)) ).
cnf(u10965,negated_conjecture,
~ p409(sK597(sK731)) ).
cnf(u11005,negated_conjecture,
~ sP65(sK730) ).
cnf(u11018,negated_conjecture,
~ p509(sK598(sK731)) ).
cnf(u11058,negated_conjecture,
~ p409(sK599(sK731)) ).
cnf(u11098,negated_conjecture,
~ sP64(sK730) ).
cnf(u11111,negated_conjecture,
~ p809(sK600(sK731)) ).
cnf(u11151,negated_conjecture,
~ p309(sK601(sK731)) ).
cnf(u11188,negated_conjecture,
~ sP63(sK730) ).
cnf(u11201,negated_conjecture,
~ p609(sK602(sK731)) ).
cnf(u11241,negated_conjecture,
~ p309(sK603(sK731)) ).
cnf(u11281,negated_conjecture,
~ sP62(sK730) ).
cnf(u11294,negated_conjecture,
~ p509(sK604(sK731)) ).
cnf(u11334,negated_conjecture,
~ p309(sK605(sK731)) ).
cnf(u11374,negated_conjecture,
~ sP61(sK730) ).
cnf(u11387,negated_conjecture,
~ p409(sK606(sK731)) ).
cnf(u11427,negated_conjecture,
~ p309(sK607(sK731)) ).
cnf(u11467,negated_conjecture,
~ sP60(sK730) ).
cnf(u11480,negated_conjecture,
~ p809(sK608(sK731)) ).
cnf(u11520,negated_conjecture,
~ p209(sK609(sK731)) ).
cnf(u11557,negated_conjecture,
~ sP59(sK730) ).
cnf(u11570,negated_conjecture,
~ p609(sK610(sK731)) ).
cnf(u11610,negated_conjecture,
~ p209(sK611(sK731)) ).
cnf(u11650,negated_conjecture,
~ sP58(sK730) ).
cnf(u11663,negated_conjecture,
~ p509(sK612(sK731)) ).
cnf(u11703,negated_conjecture,
~ p209(sK613(sK731)) ).
cnf(u11743,negated_conjecture,
~ sP57(sK730) ).
cnf(u11756,negated_conjecture,
~ p409(sK614(sK731)) ).
cnf(u11796,negated_conjecture,
~ p209(sK615(sK731)) ).
cnf(u11836,negated_conjecture,
~ sP56(sK730) ).
cnf(u11849,negated_conjecture,
~ p309(sK616(sK731)) ).
cnf(u11889,negated_conjecture,
~ p209(sK617(sK731)) ).
cnf(u11929,negated_conjecture,
~ sP55(sK730) ).
cnf(u11942,negated_conjecture,
~ p809(sK618(sK731)) ).
cnf(u11982,negated_conjecture,
~ p109(sK619(sK731)) ).
cnf(u12019,negated_conjecture,
~ sP54(sK730) ).
cnf(u12032,negated_conjecture,
~ p609(sK620(sK731)) ).
cnf(u12072,negated_conjecture,
~ p109(sK621(sK731)) ).
cnf(u12112,negated_conjecture,
~ sP53(sK730) ).
cnf(u12125,negated_conjecture,
~ p509(sK622(sK731)) ).
cnf(u12165,negated_conjecture,
~ p109(sK623(sK731)) ).
cnf(u12205,negated_conjecture,
~ sP52(sK730) ).
cnf(u12218,negated_conjecture,
~ p409(sK624(sK731)) ).
cnf(u12258,negated_conjecture,
~ p109(sK625(sK731)) ).
cnf(u12298,negated_conjecture,
~ sP51(sK730) ).
cnf(u12311,negated_conjecture,
~ p309(sK626(sK731)) ).
cnf(u12351,negated_conjecture,
~ p109(sK627(sK731)) ).
cnf(u12391,negated_conjecture,
~ sP50(sK730) ).
cnf(u12404,negated_conjecture,
~ p209(sK628(sK731)) ).
cnf(u12444,negated_conjecture,
~ p109(sK629(sK731)) ).
cnf(u12484,negated_conjecture,
~ sP49(sK730) ).
cnf(u12497,negated_conjecture,
~ p608(sK630(sK731)) ).
cnf(u12537,negated_conjecture,
~ p508(sK631(sK731)) ).
cnf(u12577,negated_conjecture,
~ sP48(sK730) ).
cnf(u12590,negated_conjecture,
~ p608(sK632(sK731)) ).
cnf(u12630,negated_conjecture,
~ p408(sK633(sK731)) ).
cnf(u12670,negated_conjecture,
~ sP47(sK730) ).
cnf(u12683,negated_conjecture,
~ p508(sK634(sK731)) ).
cnf(u12723,negated_conjecture,
~ p408(sK635(sK731)) ).
cnf(u12763,negated_conjecture,
~ sP46(sK730) ).
cnf(u12776,negated_conjecture,
~ p608(sK636(sK731)) ).
cnf(u12816,negated_conjecture,
~ p308(sK637(sK731)) ).
cnf(u12856,negated_conjecture,
~ sP45(sK730) ).
cnf(u12869,negated_conjecture,
~ p508(sK638(sK731)) ).
cnf(u12909,negated_conjecture,
~ p308(sK639(sK731)) ).
cnf(u12949,negated_conjecture,
~ sP44(sK730) ).
cnf(u12962,negated_conjecture,
~ p408(sK640(sK731)) ).
cnf(u13002,negated_conjecture,
~ p308(sK641(sK731)) ).
cnf(u13042,negated_conjecture,
~ sP43(sK730) ).
cnf(u13055,negated_conjecture,
~ p608(sK642(sK731)) ).
cnf(u13095,negated_conjecture,
~ p208(sK643(sK731)) ).
cnf(u13135,negated_conjecture,
~ sP42(sK730) ).
cnf(u13148,negated_conjecture,
~ p508(sK644(sK731)) ).
cnf(u13188,negated_conjecture,
~ p208(sK645(sK731)) ).
cnf(u13228,negated_conjecture,
~ sP41(sK730) ).
cnf(u13241,negated_conjecture,
~ p408(sK646(sK731)) ).
cnf(u13281,negated_conjecture,
~ p208(sK647(sK731)) ).
cnf(u13321,negated_conjecture,
~ sP40(sK730) ).
cnf(u13334,negated_conjecture,
~ p308(sK648(sK731)) ).
cnf(u13374,negated_conjecture,
~ p208(sK649(sK731)) ).
cnf(u13414,negated_conjecture,
~ sP39(sK730) ).
cnf(u13427,negated_conjecture,
~ p608(sK650(sK731)) ).
cnf(u13467,negated_conjecture,
~ p108(sK651(sK731)) ).
cnf(u13507,negated_conjecture,
~ sP38(sK730) ).
cnf(u13520,negated_conjecture,
~ p508(sK652(sK731)) ).
cnf(u13560,negated_conjecture,
~ p108(sK653(sK731)) ).
cnf(u13600,negated_conjecture,
~ sP37(sK730) ).
cnf(u13613,negated_conjecture,
~ p408(sK654(sK731)) ).
cnf(u13653,negated_conjecture,
~ p108(sK655(sK731)) ).
cnf(u13693,negated_conjecture,
~ sP36(sK730) ).
cnf(u13706,negated_conjecture,
~ p308(sK656(sK731)) ).
cnf(u13746,negated_conjecture,
~ p108(sK657(sK731)) ).
cnf(u13786,negated_conjecture,
~ sP35(sK730) ).
cnf(u13799,negated_conjecture,
~ p208(sK658(sK731)) ).
cnf(u13839,negated_conjecture,
~ p108(sK659(sK731)) ).
cnf(u13879,negated_conjecture,
~ sP34(sK730) ).
cnf(u13892,negated_conjecture,
~ p607(sK660(sK731)) ).
cnf(u13932,negated_conjecture,
~ p507(sK661(sK731)) ).
cnf(u13972,negated_conjecture,
~ sP33(sK730) ).
cnf(u13985,negated_conjecture,
~ p607(sK662(sK731)) ).
cnf(u14022,negated_conjecture,
~ p407(sK663(sK731)) ).
cnf(u14062,negated_conjecture,
~ sP32(sK730) ).
cnf(u14075,negated_conjecture,
~ p507(sK664(sK731)) ).
cnf(u14112,negated_conjecture,
~ p407(sK665(sK731)) ).
cnf(u14152,negated_conjecture,
~ sP31(sK730) ).
cnf(u14165,negated_conjecture,
~ p607(sK666(sK731)) ).
cnf(u14205,negated_conjecture,
~ p307(sK667(sK731)) ).
cnf(u14245,negated_conjecture,
~ sP30(sK730) ).
cnf(u14258,negated_conjecture,
~ p507(sK668(sK731)) ).
cnf(u14298,negated_conjecture,
~ p307(sK669(sK731)) ).
cnf(u14338,negated_conjecture,
~ sP29(sK730) ).
cnf(u14351,negated_conjecture,
~ p407(sK670(sK731)) ).
cnf(u14391,negated_conjecture,
~ p307(sK671(sK731)) ).
cnf(u14428,negated_conjecture,
~ sP28(sK730) ).
cnf(u14441,negated_conjecture,
~ p607(sK672(sK731)) ).
cnf(u14481,negated_conjecture,
~ p207(sK673(sK731)) ).
cnf(u14521,negated_conjecture,
~ sP27(sK730) ).
cnf(u14534,negated_conjecture,
~ p507(sK674(sK731)) ).
cnf(u14574,negated_conjecture,
~ p207(sK675(sK731)) ).
cnf(u14614,negated_conjecture,
~ sP26(sK730) ).
cnf(u14627,negated_conjecture,
~ p407(sK676(sK731)) ).
cnf(u14667,negated_conjecture,
~ p207(sK677(sK731)) ).
cnf(u14704,negated_conjecture,
~ sP25(sK730) ).
cnf(u14717,negated_conjecture,
~ p307(sK678(sK731)) ).
cnf(u14757,negated_conjecture,
~ p207(sK679(sK731)) ).
cnf(u14797,negated_conjecture,
~ sP24(sK730) ).
cnf(u14810,negated_conjecture,
~ p607(sK680(sK731)) ).
cnf(u14850,negated_conjecture,
~ p107(sK681(sK731)) ).
cnf(u14890,negated_conjecture,
~ sP23(sK730) ).
cnf(u14903,negated_conjecture,
~ p507(sK682(sK731)) ).
cnf(u14943,negated_conjecture,
~ p107(sK683(sK731)) ).
cnf(u14983,negated_conjecture,
~ sP22(sK730) ).
cnf(u14996,negated_conjecture,
~ p407(sK684(sK731)) ).
cnf(u15036,negated_conjecture,
~ p107(sK685(sK731)) ).
cnf(u15073,negated_conjecture,
~ sP21(sK730) ).
cnf(u15086,negated_conjecture,
~ p307(sK686(sK731)) ).
cnf(u15126,negated_conjecture,
~ p107(sK687(sK731)) ).
cnf(u15166,negated_conjecture,
~ sP20(sK730) ).
cnf(u15179,negated_conjecture,
~ p207(sK688(sK731)) ).
cnf(u15219,negated_conjecture,
~ p107(sK689(sK731)) ).
cnf(u15259,negated_conjecture,
~ sP19(sK730) ).
cnf(u15272,negated_conjecture,
~ p506(sK690(sK731)) ).
cnf(u15312,negated_conjecture,
~ p406(sK691(sK731)) ).
cnf(u15352,negated_conjecture,
~ sP18(sK730) ).
cnf(u15365,negated_conjecture,
~ p506(sK692(sK731)) ).
cnf(u15405,negated_conjecture,
~ p306(sK693(sK731)) ).
cnf(u15445,negated_conjecture,
~ sP17(sK730) ).
cnf(u15458,negated_conjecture,
~ p406(sK694(sK731)) ).
cnf(u15498,negated_conjecture,
~ p306(sK695(sK731)) ).
cnf(u15538,negated_conjecture,
~ sP16(sK730) ).
cnf(u15551,negated_conjecture,
~ p506(sK696(sK731)) ).
cnf(u15591,negated_conjecture,
~ p206(sK697(sK731)) ).
cnf(u15631,negated_conjecture,
~ sP15(sK730) ).
cnf(u15644,negated_conjecture,
~ p406(sK698(sK731)) ).
cnf(u15684,negated_conjecture,
~ p206(sK699(sK731)) ).
cnf(u15724,negated_conjecture,
~ sP14(sK730) ).
cnf(u15737,negated_conjecture,
~ p306(sK700(sK731)) ).
cnf(u15777,negated_conjecture,
~ p206(sK701(sK731)) ).
cnf(u15817,negated_conjecture,
~ sP13(sK730) ).
cnf(u15830,negated_conjecture,
~ p506(sK702(sK731)) ).
cnf(u15870,negated_conjecture,
~ p106(sK703(sK731)) ).
cnf(u15910,negated_conjecture,
~ sP12(sK730) ).
cnf(u15923,negated_conjecture,
~ p406(sK704(sK731)) ).
cnf(u15963,negated_conjecture,
~ p106(sK705(sK731)) ).
cnf(u16003,negated_conjecture,
~ sP11(sK730) ).
cnf(u16016,negated_conjecture,
~ p306(sK706(sK731)) ).
cnf(u16056,negated_conjecture,
~ p106(sK707(sK731)) ).
cnf(u16096,negated_conjecture,
~ sP10(sK730) ).
cnf(u16109,negated_conjecture,
~ p206(sK708(sK731)) ).
cnf(u16149,negated_conjecture,
~ p106(sK709(sK731)) ).
cnf(u16189,negated_conjecture,
~ sP9(sK730) ).
cnf(u16202,negated_conjecture,
~ p405(sK710(sK731)) ).
cnf(u16242,negated_conjecture,
~ p305(sK711(sK731)) ).
cnf(u16282,negated_conjecture,
~ sP8(sK730) ).
cnf(u16295,negated_conjecture,
~ p405(sK712(sK731)) ).
cnf(u16335,negated_conjecture,
~ p205(sK713(sK731)) ).
cnf(u16375,negated_conjecture,
~ sP7(sK730) ).
cnf(u16388,negated_conjecture,
~ p305(sK714(sK731)) ).
cnf(u16428,negated_conjecture,
~ p205(sK715(sK731)) ).
cnf(u16468,negated_conjecture,
~ sP6(sK730) ).
cnf(u16481,negated_conjecture,
~ p405(sK716(sK731)) ).
cnf(u16521,negated_conjecture,
~ p105(sK717(sK731)) ).
cnf(u16561,negated_conjecture,
~ sP5(sK730) ).
cnf(u16574,negated_conjecture,
~ p305(sK718(sK731)) ).
cnf(u16614,negated_conjecture,
~ p105(sK719(sK731)) ).
cnf(u16654,negated_conjecture,
~ sP4(sK730) ).
cnf(u16667,negated_conjecture,
~ p205(sK720(sK731)) ).
cnf(u16707,negated_conjecture,
~ p105(sK721(sK731)) ).
cnf(u16747,negated_conjecture,
~ sP3(sK730) ).
cnf(u16760,negated_conjecture,
~ p304(sK722(sK731)) ).
cnf(u16801,negated_conjecture,
~ p204(sK723(sK731)) ).
cnf(u16837,negated_conjecture,
~ sP2(sK730) ).
cnf(u16850,negated_conjecture,
~ p304(sK724(sK731)) ).
cnf(u16891,negated_conjecture,
~ p104(sK725(sK731)) ).
cnf(u16927,negated_conjecture,
~ sP1(sK730) ).
cnf(u16940,negated_conjecture,
~ p204(sK726(sK731)) ).
cnf(u16980,negated_conjecture,
~ p104(sK727(sK731)) ).
cnf(u17020,negated_conjecture,
~ sP0(sK730) ).
cnf(u17033,negated_conjecture,
~ p203(sK728(sK731)) ).
cnf(u17070,negated_conjecture,
~ p103(sK729(sK731)) ).
cnf(u1995,axiom,
( r1(X0,sK476(X0))
| ~ p905(X0)
| ~ sP154(X0) ) ).
cnf(u1639,axiom,
( ~ sP300(X0)
| sP272(X0) ) ).
cnf(u3140,negated_conjecture,
sP278(sK731) ).
cnf(u2903,negated_conjecture,
sP118(sK731) ).
cnf(u1458,axiom,
( ~ sP300(X0)
| sP14(X0) ) ).
cnf(u1730,axiom,
( ~ p410(sK327(X0))
| ~ p1010(X0)
| ~ sP286(X0) ) ).
cnf(u1958,axiom,
( ~ p106(sK458(X0))
| ~ p1006(X0)
| ~ sP172(X0) ) ).
cnf(u2908,negated_conjecture,
sP123(sK731) ).
cnf(u1789,axiom,
( r1(X0,sK364(X0))
| ~ p909(X0)
| ~ sP257(X0) ) ).
cnf(u1289,axiom,
( ~ sP300(X0)
| ~ p302(X0)
| ~ p802(X0) ) ).
cnf(u1917,axiom,
( r1(X0,sK437(X0))
| ~ p1106(X0)
| ~ sP193(X0) ) ).
cnf(u2036,axiom,
( ~ p204(sK497(X0))
| ~ p604(X0)
| ~ sP133(X0) ) ).
cnf(u2120,axiom,
( r1(X0,sK538(X0))
| ~ p510(sK539(X0))
| ~ sP95(X0) ) ).
cnf(u2048,axiom,
( ~ p104(sK503(X0))
| ~ p804(X0)
| ~ sP127(X0) ) ).
cnf(u2471,axiom,
( r1(X0,sK715(X0))
| ~ p305(sK714(X0))
| ~ sP7(X0) ) ).
cnf(u1652,axiom,
( ~ sP300(X0)
| sP74(X0) ) ).
cnf(u3169,negated_conjecture,
sP289(sK731) ).
cnf(u2948,negated_conjecture,
sP155(sK731) ).
cnf(u2399,axiom,
( r1(X0,sK679(X0))
| ~ p307(sK678(X0))
| ~ sP25(X0) ) ).
cnf(u1859,axiom,
( r1(X0,sK407(X0))
| ~ p1108(X0)
| ~ sP222(X0) ) ).
cnf(u1753,axiom,
( r1(X0,sK342(X0))
| ~ p1109(X0)
| ~ sP275(X0) ) ).
cnf(u2233,axiom,
( r1(X0,sK595(X0))
| r1(X0,sK594(X0))
| ~ sP67(X0) ) ).
cnf(u3017,negated_conjecture,
sP31(sK731) ).
cnf(u2161,axiom,
( r1(X0,sK559(X0))
| r1(X0,sK558(X0))
| ~ sP85(X0) ) ).
cnf(u1391,axiom,
( ~ sP300(X0)
| ~ p504(X0)
| ~ p904(X0) ) ).
cnf(u2312,axiom,
( r1(X0,sK634(X0))
| ~ p408(sK635(X0))
| ~ sP47(X0) ) ).
cnf(u2899,negated_conjecture,
sP114(sK731) ).
cnf(u1322,axiom,
( ~ sP300(X0)
| sP115(X0) ) ).
cnf(u3047,negated_conjecture,
sP40(sK731) ).
cnf(u2481,axiom,
( r1(X0,sK719(X0))
| r1(X0,sK718(X0))
| ~ sP5(X0) ) ).
cnf(u1822,axiom,
( ~ p508(sK385(X0))
| ~ p908(X0)
| ~ sP240(X0) ) ).
cnf(u3087,negated_conjecture,
sP248(sK731) ).
cnf(u2222,axiom,
( ~ p509(sK591(X0))
| ~ p809(sK590(X0))
| ~ sP69(X0) ) ).
cnf(u1476,axiom,
( ~ sP300(X0)
| sP186(X0) ) ).
cnf(u2975,negated_conjecture,
sP174(sK731) ).
cnf(u1653,axiom,
( ~ sP300(X0)
| sP75(X0) ) ).
cnf(u1616,axiom,
( ~ sP300(X0)
| sP256(X0) ) ).
cnf(u2282,axiom,
( ~ p109(sK621(X0))
| ~ p609(sK620(X0))
| ~ sP54(X0) ) ).
cnf(u2079,axiom,
( r1(X0,sK518(X0))
| ~ p803(X0)
| ~ sP112(X0) ) ).
cnf(u1967,axiom,
( r1(X0,sK462(X0))
| ~ p1105(X0)
| ~ sP168(X0) ) ).
cnf(u2497,axiom,
( r1(X0,sK727(X0))
| r1(X0,sK726(X0))
| ~ sP1(X0) ) ).
cnf(u1427,axiom,
( ~ sP300(X0)
| sP162(X0) ) ).
cnf(u2922,negated_conjecture,
sP134(sK731) ).
cnf(u2444,axiom,
( r1(X0,sK700(X0))
| ~ p206(sK701(X0))
| ~ sP14(X0) ) ).
cnf(u1274,axiom,
( ~ sP300(X0)
| sP104(X0) ) ).
cnf(u1374,axiom,
( ~ sP300(X0)
| sP136(X0) ) ).
cnf(u2132,axiom,
( r1(X0,sK544(X0))
| ~ p410(sK545(X0))
| ~ sP92(X0) ) ).
cnf(u1774,axiom,
( r1(X0,sK355(X0))
| ~ p509(sK356(X0))
| ~ sP264(X0) ) ).
cnf(u2267,axiom,
( r1(X0,sK613(X0))
| ~ p509(sK612(X0))
| ~ sP58(X0) ) ).
cnf(u1489,axiom,
( ~ sP300(X0)
| ~ p806(X0)
| ~ p1006(X0) ) ).
cnf(u2060,axiom,
( ~ p203(sK509(X0))
| ~ p903(X0)
| ~ sP121(X0) ) ).
cnf(u2467,axiom,
( r1(X0,sK713(X0))
| ~ p405(sK712(X0))
| ~ sP8(X0) ) ).
cnf(u1914,axiom,
( ~ p107(sK436(X0))
| ~ p807(X0)
| ~ sP194(X0) ) ).
cnf(u2097,axiom,
( r1(X0,sK527(X0))
| ~ p602(X0)
| ~ sP103(X0) ) ).
cnf(u2414,axiom,
( ~ p107(sK687(X0))
| ~ p307(sK686(X0))
| ~ sP21(X0) ) ).
cnf(u3172,negated_conjecture,
sP96(sK731) ).
cnf(u1617,axiom,
( ~ sP300(X0)
| sP64(X0) ) ).
cnf(u1333,axiom,
( ~ sP300(X0)
| ~ p303(X0)
| ~ p603(X0) ) ).
cnf(u2342,axiom,
( ~ p108(sK651(X0))
| ~ p608(sK650(X0))
| ~ sP39(X0) ) ).
cnf(u2117,axiom,
( r1(X0,sK537(X0))
| r1(X0,sK536(X0))
| ~ sP96(X0) ) ).
cnf(u3100,negated_conjecture,
sP255(sK731) ).
cnf(u1959,axiom,
( r1(X0,sK458(X0))
| ~ p1006(X0)
| ~ sP172(X0) ) ).
cnf(u1336,axiom,
( ~ sP300(X0)
| ~ p303(X0)
| ~ p1003(X0) ) ).
cnf(u2173,axiom,
( r1(X0,sK565(X0))
| r1(X0,sK564(X0))
| ~ sP82(X0) ) ).
cnf(u1801,axiom,
( r1(X0,sK372(X0))
| ~ p1109(X0)
| ~ sP251(X0) ) ).
cnf(u1590,axiom,
( ~ sP300(X0)
| ~ p808(X0)
| ~ p1108(X0) ) ).
cnf(u1864,axiom,
( ~ p108(sK410(X0))
| ~ p808(X0)
| ~ sP219(X0) ) ).
cnf(u1468,axiom,
( ~ sP300(X0)
| sP179(X0) ) ).
cnf(u1738,axiom,
( r1(X0,sK332(X0))
| ~ p310(sK333(X0))
| ~ sP282(X0) ) ).
cnf(u3085,negated_conjecture,
sP53(sK731) ).
cnf(u2971,negated_conjecture,
sP173(sK731) ).
cnf(u2294,axiom,
( ~ p109(sK627(X0))
| ~ p309(sK626(X0))
| ~ sP51(X0) ) ).
cnf(u1831,axiom,
( r1(X0,sK390(X0))
| ~ p1008(X0)
| ~ sP236(X0) ) ).
cnf(u2934,negated_conjecture,
sP5(sK731) ).
cnf(u1638,axiom,
( ~ sP300(X0)
| sP271(X0) ) ).
cnf(u2044,axiom,
( ~ p104(sK501(X0))
| ~ p1004(X0)
| ~ sP129(X0) ) ).
cnf(u1739,axiom,
( r1(X0,sK333(X0))
| r1(X0,sK332(X0))
| ~ sP282(X0) ) ).
cnf(u1807,axiom,
( r1(X0,sK376(X0))
| r1(X0,sK375(X0))
| ~ sP248(X0) ) ).
cnf(u1432,axiom,
( ~ sP300(X0)
| sP167(X0) ) ).
cnf(u1845,axiom,
( r1(X0,sK398(X0))
| ~ p808(X0)
| ~ sP229(X0) ) ).
cnf(u1271,axiom,
( ~ sP300(X0)
| sP101(X0) ) ).
cnf(u1867,axiom,
( r1(X0,sK412(X0))
| r1(X0,sK411(X0))
| ~ sP218(X0) ) ).
cnf(u1986,axiom,
( ~ p305(sK472(X0))
| ~ p605(X0)
| ~ sP158(X0) ) ).
cnf(u1517,axiom,
( ~ sP300(X0)
| sP205(X0) ) ).
cnf(u1399,axiom,
( ~ sP300(X0)
| ~ p804(X0)
| ~ p1004(X0) ) ).
cnf(u1330,axiom,
( ~ sP300(X0)
| sP123(X0) ) ).
cnf(u1602,axiom,
( ~ sP300(X0)
| sP250(X0) ) ).
cnf(u2008,axiom,
( ~ p105(sK483(X0))
| ~ p805(X0)
| ~ sP147(X0) ) ).
cnf(u1945,axiom,
( r1(X0,sK451(X0))
| ~ p606(X0)
| ~ sP179(X0) ) ).
cnf(u1661,axiom,
( ~ sP300(X0)
| sP80(X0) ) ).
cnf(u1759,axiom,
( r1(X0,sK346(X0))
| r1(X0,sK345(X0))
| ~ sP272(X0) ) ).
cnf(u3128,negated_conjecture,
sP273(sK731) ).
cnf(u2376,axiom,
( r1(X0,sK666(X0))
| ~ p307(sK667(X0))
| ~ sP31(X0) ) ).
cnf(u2304,axiom,
( r1(X0,sK630(X0))
| ~ p508(sK631(X0))
| ~ sP49(X0) ) ).
cnf(u2215,axiom,
( r1(X0,sK587(X0))
| ~ p210(sK586(X0))
| ~ sP71(X0) ) ).
cnf(u1908,axiom,
( ~ p107(sK433(X0))
| ~ p1107(X0)
| ~ sP197(X0) ) ).
cnf(u2261,axiom,
( r1(X0,sK609(X0))
| r1(X0,sK608(X0))
| ~ sP60(X0) ) ).
cnf(u3058,negated_conjecture,
sP46(sK731) ).
cnf(u3113,negated_conjecture,
sP261(sK731) ).
cnf(u1603,axiom,
( ~ sP300(X0)
| sP251(X0) ) ).
cnf(u1497,axiom,
( ~ sP300(X0)
| sP23(X0) ) ).
cnf(u1296,axiom,
( ~ sP300(X0)
| ~ p402(X0)
| ~ p902(X0) ) ).
cnf(u1997,axiom,
( r1(X0,sK477(X0))
| ~ p805(X0)
| ~ sP153(X0) ) ).
cnf(u2952,negated_conjecture,
sP158(sK731) ).
cnf(u1625,axiom,
( ~ sP300(X0)
| sP261(X0) ) ).
cnf(u2105,axiom,
( r1(X0,sK531(X0))
| ~ p202(X0)
| ~ sP99(X0) ) ).
cnf(u2889,negated_conjecture,
sP105(sK731) ).
cnf(u2256,axiom,
( r1(X0,sK606(X0))
| ~ p309(sK607(X0))
| ~ sP61(X0) ) ).
cnf(u1732,axiom,
( r1(X0,sK328(X0))
| ~ p410(sK329(X0))
| ~ sP285(X0) ) ).
cnf(u3162,negated_conjecture,
sP92(sK731) ).
cnf(u1872,axiom,
( ~ p607(sK415(X0))
| ~ p907(X0)
| ~ sP215(X0) ) ).
cnf(u2094,axiom,
( ~ p102(sK526(X0))
| ~ p802(X0)
| ~ sP104(X0) ) ).
cnf(u1348,axiom,
( ~ sP300(X0)
| ~ p503(X0)
| ~ p1103(X0) ) ).
cnf(u2226,axiom,
( ~ p509(sK593(X0))
| ~ p609(sK592(X0))
| ~ sP68(X0) ) ).
cnf(u1711,axiom,
( r1(X0,sK313(X0))
| ~ p1010(X0)
| ~ sP296(X0) ) ).
cnf(u2346,axiom,
( ~ p108(sK653(X0))
| ~ p508(sK652(X0))
| ~ sP38(X0) ) ).
cnf(u2154,axiom,
( ~ p310(sK557(X0))
| ~ p610(sK556(X0))
| ~ sP86(X0) ) ).
cnf(u2441,axiom,
( r1(X0,sK699(X0))
| r1(X0,sK698(X0))
| ~ sP15(X0) ) ).
cnf(u1530,axiom,
( ~ sP300(X0)
| sP215(X0) ) ).
cnf(u3134,negated_conjecture,
sP74(sK731) ).
cnf(u2388,axiom,
( r1(X0,sK672(X0))
| ~ p207(sK673(X0))
| ~ sP28(X0) ) ).
cnf(u2030,axiom,
( ~ p204(sK494(X0))
| ~ p1004(X0)
| ~ sP136(X0) ) ).
cnf(u2369,axiom,
( r1(X0,sK663(X0))
| r1(X0,sK662(X0))
| ~ sP33(X0) ) ).
cnf(u1299,axiom,
( ~ sP300(X0)
| ~ p502(X0)
| ~ p602(X0) ) ).
cnf(u2316,axiom,
( r1(X0,sK636(X0))
| ~ p308(sK637(X0))
| ~ sP46(X0) ) ).
cnf(u2976,negated_conjecture,
sP175(sK731) ).
cnf(u1733,axiom,
( r1(X0,sK329(X0))
| r1(X0,sK328(X0))
| ~ sP285(X0) ) ).
cnf(u1646,axiom,
( ~ sP300(X0)
| ~ p909(X0)
| ~ p1009(X0) ) ).
cnf(u2139,axiom,
( r1(X0,sK549(X0))
| ~ p610(sK548(X0))
| ~ sP90(X0) ) ).
cnf(u3070,negated_conjecture,
sP237(sK731) ).
cnf(u1361,axiom,
( ~ sP300(X0)
| sP124(X0) ) ).
cnf(u2339,axiom,
( r1(X0,sK649(X0))
| ~ p308(sK648(X0))
| ~ sP40(X0) ) ).
cnf(u1861,axiom,
( r1(X0,sK408(X0))
| ~ p1008(X0)
| ~ sP221(X0) ) ).
cnf(u1747,axiom,
( r1(X0,sK338(X0))
| ~ p1110(X0)
| ~ sP278(X0) ) ).
cnf(u3179,negated_conjecture,
sP296(sK731) ).
cnf(u1279,axiom,
( ~ sP300(X0)
| ~ p202(X0)
| ~ p402(X0) ) ).
cnf(u1460,axiom,
( ~ sP300(X0)
| sP16(X0) ) ).
cnf(u2901,negated_conjecture,
sP116(sK731) ).
cnf(u2268,axiom,
( r1(X0,sK612(X0))
| ~ p209(sK613(X0))
| ~ sP58(X0) ) ).
cnf(u1994,axiom,
( ~ p205(sK476(X0))
| ~ p905(X0)
| ~ sP154(X0) ) ).
cnf(u2480,axiom,
( r1(X0,sK718(X0))
| ~ p105(sK719(X0))
| ~ sP5(X0) ) ).
cnf(u2961,negated_conjecture,
sP167(sK731) ).
cnf(u1413,axiom,
( ~ sP300(X0)
| sP7(X0) ) ).
cnf(u1340,axiom,
( ~ sP300(X0)
| ~ p403(X0)
| ~ p803(X0) ) ).
cnf(u1610,axiom,
( ~ sP300(X0)
| sP253(X0) ) ).
cnf(u2997,negated_conjecture,
sP193(sK731) ).
cnf(u1736,axiom,
( ~ p310(sK331(X0))
| ~ p1010(X0)
| ~ sP283(X0) ) ).
cnf(u1953,axiom,
( r1(X0,sK455(X0))
| ~ p806(X0)
| ~ sP175(X0) ) ).
cnf(u2166,axiom,
( ~ p210(sK563(X0))
| ~ p910(sK562(X0))
| ~ sP83(X0) ) ).
cnf(u2453,axiom,
( r1(X0,sK705(X0))
| r1(X0,sK704(X0))
| ~ sP12(X0) ) ).
cnf(u2496,axiom,
( r1(X0,sK726(X0))
| ~ p104(sK727(X0))
| ~ sP1(X0) ) ).
cnf(u2381,axiom,
( r1(X0,sK669(X0))
| r1(X0,sK668(X0))
| ~ sP30(X0) ) ).
cnf(u3078,negated_conjecture,
sP244(sK731) ).
cnf(u1688,axiom,
( ~ sP300(X0)
| sP290(X0) ) ).
cnf(u1916,axiom,
( ~ p506(sK437(X0))
| ~ p1106(X0)
| ~ sP193(X0) ) ).
cnf(u2039,axiom,
( r1(X0,sK498(X0))
| ~ p504(X0)
| ~ sP132(X0) ) ).
cnf(u1611,axiom,
( ~ sP300(X0)
| sP254(X0) ) ).
cnf(u1304,axiom,
( ~ sP300(X0)
| ~ p602(X0)
| ~ p802(X0) ) ).
cnf(u3014,negated_conjecture,
sP201(sK731) ).
cnf(u1446,axiom,
( ~ sP300(X0)
| ~ p905(X0)
| ~ p1005(X0) ) ).
cnf(u1277,axiom,
( ~ sP300(X0)
| sP107(X0) ) ).
cnf(u1858,axiom,
( ~ p108(sK407(X0))
| ~ p1108(X0)
| ~ sP222(X0) ) ).
cnf(u2102,axiom,
( ~ p102(sK530(X0))
| ~ p302(X0)
| ~ sP100(X0) ) ).
cnf(u1740,axiom,
( ~ p210(sK334(X0))
| ~ p1110(X0)
| ~ sP281(X0) ) ).
cnf(u1850,axiom,
( ~ p208(sK402(X0))
| ~ p1008(X0)
| ~ sP226(X0) ) ).
cnf(u2973,negated_conjecture,
sP15(sK731) ).
cnf(u1405,axiom,
( ~ sP300(X0)
| sP5(X0) ) ).
cnf(u2457,axiom,
( r1(X0,sK707(X0))
| r1(X0,sK706(X0))
| ~ sP11(X0) ) ).
cnf(u1256,axiom,
( ~ sP300(X0)
| ~ p501(X0)
| ~ p901(X0) ) ).
cnf(u1817,axiom,
( r1(X0,sK382(X0))
| r1(X0,sK381(X0))
| ~ sP243(X0) ) ).
cnf(u1719,axiom,
( r1(X0,sK319(X0))
| ~ p1010(X0)
| ~ sP292(X0) ) ).
cnf(u3095,negated_conjecture,
sP59(sK731) ).
cnf(u1479,axiom,
( ~ sP300(X0)
| sP189(X0) ) ).
cnf(u2983,negated_conjecture,
sP180(sK731) ).
cnf(u1410,axiom,
( ~ sP300(X0)
| sP148(X0) ) ).
cnf(u1567,axiom,
( ~ sP300(X0)
| sP48(X0) ) ).
cnf(u2038,axiom,
( ~ p204(sK498(X0))
| ~ p504(X0)
| ~ sP132(X0) ) ).
cnf(u2965,negated_conjecture,
sP12(sK731) ).
cnf(u1241,axiom,
( ~ sP300(X0)
| ~ p301(X0)
| ~ p401(X0) ) ).
cnf(u1255,axiom,
( ~ sP300(X0)
| ~ p501(X0)
| ~ p801(X0) ) ).
cnf(u1741,axiom,
( r1(X0,sK334(X0))
| ~ p1110(X0)
| ~ sP281(X0) ) ).
cnf(u2930,negated_conjecture,
sP142(sK731) ).
cnf(u1369,axiom,
( ~ sP300(X0)
| sP131(X0) ) ).
cnf(u3136,negated_conjecture,
sP276(sK731) ).
cnf(u2068,axiom,
( ~ p203(sK513(X0))
| ~ p403(X0)
| ~ sP117(X0) ) ).
cnf(u1988,axiom,
( ~ p305(sK473(X0))
| ~ p505(X0)
| ~ sP157(X0) ) ).
cnf(u2200,axiom,
( r1(X0,sK578(X0))
| ~ p110(sK579(X0))
| ~ sP75(X0) ) ).
cnf(u2359,axiom,
( r1(X0,sK659(X0))
| ~ p208(sK658(X0))
| ~ sP35(X0) ) ).
cnf(u2128,axiom,
( r1(X0,sK542(X0))
| ~ p510(sK543(X0))
| ~ sP93(X0) ) ).
cnf(u3106,negated_conjecture,
sP257(sK731) ).
cnf(u1604,axiom,
( ~ sP300(X0)
| sP56(X0) ) ).
cnf(u3108,negated_conjecture,
sP259(sK731) ).
cnf(u2482,axiom,
( ~ p105(sK721(X0))
| ~ p205(sK720(X0))
| ~ sP4(X0) ) ).
cnf(u3028,negated_conjecture,
sP34(sK731) ).
cnf(u1744,axiom,
( r1(X0,sK336(X0))
| ~ p210(sK337(X0))
| ~ sP279(X0) ) ).
cnf(u1266,axiom,
( ~ sP300(X0)
| ~ p901(X0)
| ~ p1001(X0) ) ).
cnf(u2410,axiom,
( ~ p107(sK685(X0))
| ~ p407(sK684(X0))
| ~ sP22(X0) ) ).
cnf(u2185,axiom,
( r1(X0,sK571(X0))
| r1(X0,sK570(X0))
| ~ sP79(X0) ) ).
cnf(u1800,axiom,
( ~ p109(sK372(X0))
| ~ p1109(X0)
| ~ sP251(X0) ) ).
cnf(u2098,axiom,
( ~ p102(sK528(X0))
| ~ p502(X0)
| ~ sP102(X0) ) ).
cnf(u1583,axiom,
( ~ sP300(X0)
| sP247(X0) ) ).
cnf(u1471,axiom,
( ~ sP300(X0)
| sP182(X0) ) ).
cnf(u2385,axiom,
( r1(X0,sK671(X0))
| r1(X0,sK670(X0))
| ~ sP29(X0) ) ).
cnf(u2313,axiom,
( r1(X0,sK635(X0))
| r1(X0,sK634(X0))
| ~ sP47(X0) ) ).
cnf(u2979,negated_conjecture,
sP178(sK731) ).
cnf(u1402,axiom,
( ~ sP300(X0)
| ~ p904(X0)
| ~ p1104(X0) ) ).
cnf(u1902,axiom,
( ~ p207(sK430(X0))
| ~ p1007(X0)
| ~ sP200(X0) ) ).
cnf(u3167,negated_conjecture,
sP94(sK731) ).
cnf(u2302,axiom,
( ~ p508(sK631(X0))
| ~ p608(sK630(X0))
| ~ sP49(X0) ) ).
cnf(u3055,negated_conjecture,
sP227(sK731) ).
cnf(u2083,axiom,
( r1(X0,sK520(X0))
| ~ p503(X0)
| ~ sP110(X0) ) ).
cnf(u1605,axiom,
( ~ sP300(X0)
| sP57(X0) ) ).
cnf(u1696,axiom,
( r1(X0,sK302(X0))
| ~ p1010(X0)
| ~ sP300(X0) ) ).
cnf(u2942,negated_conjecture,
sP7(sK731) ).
cnf(u2159,axiom,
( r1(X0,sK559(X0))
| ~ p510(sK558(X0))
| ~ sP85(X0) ) ).
cnf(u2047,axiom,
( r1(X0,sK502(X0))
| ~ p904(X0)
| ~ sP128(X0) ) ).
cnf(u3123,negated_conjecture,
sP70(sK731) ).
cnf(u1507,axiom,
( ~ sP300(X0)
| sP198(X0) ) ).
cnf(u3002,negated_conjecture,
sP24(sK731) ).
cnf(u1454,axiom,
( ~ sP300(X0)
| sP170(X0) ) ).
cnf(u2212,axiom,
( r1(X0,sK584(X0))
| ~ p110(sK585(X0))
| ~ sP72(X0) ) ).
cnf(u2140,axiom,
( r1(X0,sK548(X0))
| ~ p410(sK549(X0))
| ~ sP90(X0) ) ).
cnf(u1596,axiom,
( ~ sP300(X0)
| sP52(X0) ) ).
cnf(u1866,axiom,
( r1(X0,sK411(X0))
| ~ p108(sK412(X0))
| ~ sP218(X0) ) ).
cnf(u2356,axiom,
( r1(X0,sK656(X0))
| ~ p108(sK657(X0))
| ~ sP36(X0) ) ).
cnf(u2494,axiom,
( ~ p104(sK727(X0))
| ~ p204(sK726(X0))
| ~ sP1(X0) ) ).
cnf(u2475,axiom,
( r1(X0,sK717(X0))
| ~ p405(sK716(X0))
| ~ sP6(X0) ) ).
cnf(u1697,axiom,
( r1(X0,sK301(X0))
| ~ p1110(X0)
| ~ sP300(X0) ) ).
cnf(u1285,axiom,
( ~ sP300(X0)
| ~ p202(X0)
| ~ p1102(X0) ) ).
cnf(u2422,axiom,
( ~ p406(sK691(X0))
| ~ p506(sK690(X0))
| ~ sP19(X0) ) ).
cnf(u2197,axiom,
( r1(X0,sK577(X0))
| r1(X0,sK576(X0))
| ~ sP76(X0) ) ).
cnf(u3180,negated_conjecture,
sP297(sK731) ).
cnf(u2125,axiom,
( r1(X0,sK541(X0))
| r1(X0,sK540(X0))
| ~ sP94(X0) ) ).
cnf(u1825,axiom,
( r1(X0,sK386(X0))
| ~ p808(X0)
| ~ sP239(X0) ) ).
cnf(u1575,axiom,
( ~ sP300(X0)
| sP239(X0) ) ).
cnf(u1487,axiom,
( ~ sP300(X0)
| ~ p606(X0)
| ~ p1106(X0) ) ).
cnf(u1944,axiom,
( ~ p306(sK451(X0))
| ~ p606(X0)
| ~ sP179(X0) ) ).
cnf(u1420,axiom,
( ~ sP300(X0)
| sP156(X0) ) ).
cnf(u3165,negated_conjecture,
sP93(sK731) ).
cnf(u3051,negated_conjecture,
sP223(sK731) ).
cnf(u1249,axiom,
( ~ sP300(X0)
| ~ p401(X0)
| ~ p601(X0) ) ).
cnf(u1560,axiom,
( ~ sP300(X0)
| sP46(X0) ) ).
cnf(u1783,axiom,
( r1(X0,sK361(X0))
| r1(X0,sK360(X0))
| ~ sP260(X0) ) ).
cnf(u2246,axiom,
( ~ p309(sK603(X0))
| ~ p609(sK602(X0))
| ~ sP63(X0) ) ).
cnf(u1911,axiom,
( r1(X0,sK434(X0))
| ~ p1007(X0)
| ~ sP196(X0) ) ).
cnf(u1371,axiom,
( ~ sP300(X0)
| sP133(X0) ) ).
cnf(u2886,negated_conjecture,
sP102(sK731) ).
cnf(u1318,axiom,
( ~ sP300(X0)
| sP111(X0) ) ).
cnf(u1718,axiom,
( ~ p610(sK319(X0))
| ~ p1010(X0)
| ~ sP292(X0) ) ).
cnf(u1996,axiom,
( ~ p205(sK477(X0))
| ~ p805(X0)
| ~ sP153(X0) ) ).
cnf(u2129,axiom,
( r1(X0,sK543(X0))
| r1(X0,sK542(X0))
| ~ sP93(X0) ) ).
cnf(u1288,axiom,
( ~ sP300(X0)
| ~ p302(X0)
| ~ p602(X0) ) ).
cnf(u1512,axiom,
( ~ sP300(X0)
| sP30(X0) ) ).
cnf(u1612,axiom,
( ~ sP300(X0)
| sP255(X0) ) ).
cnf(u1808,axiom,
( ~ p608(sK377(X0))
| ~ p1108(X0)
| ~ sP247(X0) ) ).
cnf(u1947,axiom,
( r1(X0,sK452(X0))
| ~ p1106(X0)
| ~ sP178(X0) ) ).
cnf(u1496,axiom,
( ~ sP300(X0)
| sP22(X0) ) ).
cnf(u1270,axiom,
( ~ sP300(X0)
| sP100(X0) ) ).
cnf(u1351,axiom,
( ~ sP300(X0)
| ~ p603(X0)
| ~ p1003(X0) ) ).
cnf(u2016,axiom,
( ~ p304(sK487(X0))
| ~ p1004(X0)
| ~ sP143(X0) ) ).
cnf(u2349,axiom,
( r1(X0,sK653(X0))
| r1(X0,sK652(X0))
| ~ sP38(X0) ) ).
cnf(u1485,axiom,
( ~ sP300(X0)
| ~ p606(X0)
| ~ p906(X0) ) ).
cnf(u1682,axiom,
( ~ sP300(X0)
| sP287(X0) ) ).
cnf(u1910,axiom,
( ~ p107(sK434(X0))
| ~ p1007(X0)
| ~ sP196(X0) ) ).
cnf(u3065,negated_conjecture,
sP48(sK731) ).
cnf(u2025,axiom,
( r1(X0,sK491(X0))
| ~ p504(X0)
| ~ sP139(X0) ) ).
cnf(u1613,axiom,
( ~ sP300(X0)
| sP61(X0) ) ).
cnf(u3080,negated_conjecture,
sP246(sK731) ).
cnf(u2456,axiom,
( r1(X0,sK706(X0))
| ~ p106(sK707(X0))
| ~ sP11(X0) ) ).
cnf(u2384,axiom,
( r1(X0,sK670(X0))
| ~ p307(sK671(X0))
| ~ sP29(X0) ) ).
cnf(u2295,axiom,
( r1(X0,sK627(X0))
| ~ p309(sK626(X0))
| ~ sP51(X0) ) ).
cnf(u1860,axiom,
( ~ p108(sK408(X0))
| ~ p1008(X0)
| ~ sP221(X0) ) ).
cnf(u1234,axiom,
( ~ sP300(X0)
| ~ p201(X0)
| ~ p401(X0) ) ).
cnf(u3010,negated_conjecture,
sP28(sK731) ).
cnf(u1683,axiom,
( ~ sP300(X0)
| sP93(X0) ) ).
cnf(u2423,axiom,
( r1(X0,sK691(X0))
| ~ p506(sK690(X0))
| ~ sP19(X0) ) ).
cnf(u1376,axiom,
( ~ sP300(X0)
| sP138(X0) ) ).
cnf(u3121,negated_conjecture,
sP267(sK731) ).
cnf(u2900,negated_conjecture,
sP115(sK731) ).
cnf(u2351,axiom,
( r1(X0,sK655(X0))
| ~ p408(sK654(X0))
| ~ sP37(X0) ) ).
cnf(u3032,negated_conjecture,
sP213(sK731) ).
cnf(u1811,axiom,
( r1(X0,sK378(X0))
| ~ p1008(X0)
| ~ sP246(X0) ) ).
cnf(u1705,axiom,
( r1(X0,sK310(X0))
| ~ p1110(X0)
| ~ sP299(X0) ) ).
cnf(u2057,axiom,
( r1(X0,sK507(X0))
| ~ p1103(X0)
| ~ sP123(X0) ) ).
cnf(u2960,negated_conjecture,
sP166(sK731) ).
cnf(u1760,axiom,
( ~ p609(sK347(X0))
| ~ p1109(X0)
| ~ sP271(X0) ) ).
cnf(u1343,axiom,
( ~ sP300(X0)
| ~ p403(X0)
| ~ p1103(X0) ) ).
cnf(u1952,axiom,
( ~ p206(sK455(X0))
| ~ p806(X0)
| ~ sP175(X0) ) ).
cnf(u2174,axiom,
( ~ p210(sK567(X0))
| ~ p610(sK566(X0))
| ~ sP81(X0) ) ).
cnf(u1428,axiom,
( ~ sP300(X0)
| sP163(X0) ) ).
cnf(u2927,negated_conjecture,
sP139(sK731) ).
cnf(u2178,axiom,
( ~ p210(sK569(X0))
| ~ p510(sK568(X0))
| ~ sP80(X0) ) ).
cnf(u1791,axiom,
( r1(X0,sK366(X0))
| r1(X0,sK365(X0))
| ~ sP256(X0) ) ).
cnf(u1251,axiom,
( ~ sP300(X0)
| ~ p401(X0)
| ~ p901(X0) ) ).
cnf(u2234,axiom,
( ~ p409(sK597(X0))
| ~ p609(sK596(X0))
| ~ sP66(X0) ) ).
cnf(u1482,axiom,
( ~ sP300(X0)
| sP192(X0) ) ).
cnf(u3086,negated_conjecture,
sP54(sK731) ).
cnf(u2468,axiom,
( r1(X0,sK712(X0))
| ~ p205(sK713(X0))
| ~ sP8(X0) ) ).
cnf(u1919,axiom,
( r1(X0,sK438(X0))
| ~ p1006(X0)
| ~ sP192(X0) ) ).
cnf(u2449,axiom,
( r1(X0,sK703(X0))
| r1(X0,sK702(X0))
| ~ sP13(X0) ) ).
cnf(u1379,axiom,
( ~ sP300(X0)
| sP141(X0) ) ).
cnf(u2396,axiom,
( r1(X0,sK676(X0))
| ~ p207(sK677(X0))
| ~ sP26(X0) ) ).
cnf(u2291,axiom,
( r1(X0,sK625(X0))
| ~ p409(sK624(X0))
| ~ sP52(X0) ) ).
cnf(u1326,axiom,
( ~ sP300(X0)
| sP119(X0) ) ).
cnf(u1726,axiom,
( r1(X0,sK324(X0))
| ~ p510(sK325(X0))
| ~ sP288(X0) ) ).
cnf(u1574,axiom,
( ~ sP300(X0)
| sP238(X0) ) ).
cnf(u3022,negated_conjecture,
sP32(sK731) ).
cnf(u1441,axiom,
( ~ sP300(X0)
| ~ p605(X0)
| ~ p1005(X0) ) ).
cnf(u2419,axiom,
( r1(X0,sK689(X0))
| ~ p207(sK688(X0))
| ~ sP20(X0) ) ).
cnf(u1941,axiom,
( r1(X0,sK449(X0))
| ~ p906(X0)
| ~ sP181(X0) ) ).
cnf(u2329,axiom,
( r1(X0,sK643(X0))
| r1(X0,sK642(X0))
| ~ sP43(X0) ) ).
cnf(u1520,axiom,
( ~ sP300(X0)
| sP206(X0) ) ).
cnf(u2347,axiom,
( r1(X0,sK653(X0))
| ~ p508(sK652(X0))
| ~ sP38(X0) ) ).
cnf(u3137,negated_conjecture,
sP76(sK731) ).
cnf(u1569,axiom,
( ~ sP300(X0)
| sP234(X0) ) ).
cnf(u1794,axiom,
( ~ p209(sK368(X0))
| ~ p1009(X0)
| ~ sP254(X0) ) ).
cnf(u1231,axiom,
( ~ sP300(X0)
| ~ p101(X0)
| ~ p1001(X0) ) ).
cnf(u2137,axiom,
( r1(X0,sK547(X0))
| r1(X0,sK546(X0))
| ~ sP91(X0) ) ).
cnf(u2972,negated_conjecture,
sP14(sK731) ).
cnf(u3041,negated_conjecture,
sP39(sK731) ).
cnf(u3109,negated_conjecture,
sP65(sK731) ).
cnf(u1493,axiom,
( ~ sP300(X0)
| ~ p1006(X0)
| ~ p1106(X0) ) ).
cnf(u1292,axiom,
( ~ sP300(X0)
| ~ p302(X0)
| ~ p1102(X0) ) ).
cnf(u1690,axiom,
( ~ sP300(X0)
| sP96(X0) ) ).
cnf(u2923,negated_conjecture,
sP135(sK731) ).
cnf(u2033,axiom,
( r1(X0,sK495(X0))
| ~ p904(X0)
| ~ sP135(X0) ) ).
cnf(u2118,axiom,
( ~ p510(sK539(X0))
| ~ p910(sK538(X0))
| ~ sP95(X0) ) ).
cnf(u1805,axiom,
( r1(X0,sK374(X0))
| ~ p909(X0)
| ~ sP249(X0) ) ).
cnf(u3158,negated_conjecture,
sP89(sK731) ).
cnf(u1768,axiom,
( ~ p509(sK352(X0))
| ~ p1109(X0)
| ~ sP267(X0) ) ).
cnf(u1868,axiom,
( ~ p607(sK413(X0))
| ~ p1107(X0)
| ~ sP217(X0) ) ).
cnf(u1244,axiom,
( ~ sP300(X0)
| ~ p301(X0)
| ~ p801(X0) ) ).
cnf(u1691,axiom,
( ~ sP300(X0)
| sP97(X0) ) ).
cnf(u1384,axiom,
( ~ sP300(X0)
| ~ p404(X0)
| ~ p604(X0) ) ).
cnf(u1526,axiom,
( ~ sP300(X0)
| sP211(X0) ) ).
cnf(u1819,axiom,
( r1(X0,sK383(X0))
| ~ p1108(X0)
| ~ sP242(X0) ) ).
cnf(u2216,axiom,
( r1(X0,sK586(X0))
| ~ p110(sK587(X0))
| ~ sP71(X0) ) ).
cnf(u1229,axiom,
( ~ sP300(X0)
| ~ p101(X0)
| ~ p801(X0) ) ).
cnf(u1938,axiom,
( ~ p306(sK448(X0))
| ~ p1006(X0)
| ~ sP182(X0) ) ).
cnf(u2895,negated_conjecture,
sP110(sK731) ).
cnf(u1880,axiom,
( ~ p507(sK419(X0))
| ~ p907(X0)
| ~ sP211(X0) ) ).
cnf(u3177,negated_conjecture,
sP295(sK731) ).
cnf(u3053,negated_conjecture,
sP225(sK731) ).
cnf(u1357,axiom,
( ~ sP300(X0)
| ~ p903(X0)
| ~ p1103(X0) ) ).
cnf(u1554,axiom,
( ~ sP300(X0)
| sP224(X0) ) ).
cnf(u2465,axiom,
( r1(X0,sK711(X0))
| r1(X0,sK710(X0))
| ~ sP9(X0) ) ).
cnf(u1897,axiom,
( r1(X0,sK427(X0))
| ~ p907(X0)
| ~ sP203(X0) ) ).
cnf(u1671,axiom,
( ~ sP300(X0)
| sP282(X0) ) ).
cnf(u3175,negated_conjecture,
sP293(sK731) ).
cnf(u1259,axiom,
( ~ sP300(X0)
| ~ p601(X0)
| ~ p801(X0) ) ).
cnf(u1490,axiom,
( ~ sP300(X0)
| ~ p806(X0)
| ~ p1106(X0) ) ).
cnf(u1990,axiom,
( ~ p205(sK474(X0))
| ~ p1105(X0)
| ~ sP156(X0) ) ).
cnf(u2386,axiom,
( ~ p207(sK673(X0))
| ~ p607(sK672(X0))
| ~ sP28(X0) ) ).
cnf(u2167,axiom,
( r1(X0,sK563(X0))
| ~ p910(sK562(X0))
| ~ sP83(X0) ) ).
cnf(u2882,negated_conjecture,
sP300(sK731) ).
cnf(u1555,axiom,
( ~ sP300(X0)
| sP225(X0) ) ).
cnf(u1449,axiom,
( ~ sP300(X0)
| sP10(X0) ) ).
cnf(u1949,axiom,
( r1(X0,sK453(X0))
| ~ p1006(X0)
| ~ sP177(X0) ) ).
cnf(u1802,axiom,
( ~ p109(sK373(X0))
| ~ p1009(X0)
| ~ sP250(X0) ) ).
cnf(u2904,negated_conjecture,
sP119(sK731) ).
cnf(u2280,axiom,
( r1(X0,sK618(X0))
| ~ p109(sK619(X0))
| ~ sP55(X0) ) ).
cnf(u2208,axiom,
( r1(X0,sK582(X0))
| ~ p110(sK583(X0))
| ~ sP73(X0) ) ).
cnf(u2477,axiom,
( r1(X0,sK717(X0))
| r1(X0,sK716(X0))
| ~ sP6(X0) ) ).
cnf(u1684,axiom,
( ~ sP300(X0)
| sP288(X0) ) ).
cnf(u2434,axiom,
( ~ p206(sK697(X0))
| ~ p506(sK696(X0))
| ~ sP16(X0) ) ).
cnf(u3114,negated_conjecture,
sP262(sK731) ).
cnf(u2019,axiom,
( r1(X0,sK488(X0))
| ~ p904(X0)
| ~ sP142(X0) ) ).
cnf(u2490,axiom,
( ~ p104(sK725(X0))
| ~ p304(sK724(X0))
| ~ sP2(X0) ) ).
cnf(u2265,axiom,
( r1(X0,sK611(X0))
| r1(X0,sK610(X0))
| ~ sP59(X0) ) ).
cnf(u2103,axiom,
( r1(X0,sK530(X0))
| ~ p302(X0)
| ~ sP100(X0) ) ).
cnf(u2050,axiom,
( ~ p104(sK504(X0))
| ~ p604(X0)
| ~ sP126(X0) ) ).
cnf(u1663,axiom,
( ~ sP300(X0)
| sP279(X0) ) ).
cnf(u1423,axiom,
( ~ sP300(X0)
| sP158(X0) ) ).
cnf(u2106,axiom,
( ~ p810(sK533(X0))
| ~ p910(sK532(X0))
| ~ sP98(X0) ) ).
cnf(u2393,axiom,
( r1(X0,sK675(X0))
| r1(X0,sK674(X0))
| ~ sP27(X0) ) ).
cnf(u3059,negated_conjecture,
sP228(sK731) ).
cnf(u1354,axiom,
( ~ sP300(X0)
| ~ p803(X0)
| ~ p1003(X0) ) ).
cnf(u2340,axiom,
( r1(X0,sK648(X0))
| ~ p208(sK649(X0))
| ~ sP40(X0) ) ).
cnf(u1982,axiom,
( ~ p305(sK470(X0))
| ~ p905(X0)
| ~ sP160(X0) ) ).
cnf(u2321,axiom,
( r1(X0,sK639(X0))
| r1(X0,sK638(X0))
| ~ sP45(X0) ) ).
cnf(u2254,axiom,
( ~ p309(sK607(X0))
| ~ p409(sK606(X0))
| ~ sP61(X0) ) ).
cnf(u2163,axiom,
( r1(X0,sK561(X0))
| ~ p410(sK560(X0))
| ~ sP84(X0) ) ).
cnf(u1685,axiom,
( ~ sP300(X0)
| sP94(X0) ) ).
cnf(u2483,axiom,
( r1(X0,sK721(X0))
| ~ p205(sK720(X0))
| ~ sP4(X0) ) ).
cnf(u1846,axiom,
( r1(X0,sK399(X0))
| ~ p308(sK400(X0))
| ~ sP228(X0) ) ).
cnf(u1598,axiom,
( ~ sP300(X0)
| sP54(X0) ) ).
cnf(u2091,axiom,
( r1(X0,sK524(X0))
| ~ p1002(X0)
| ~ sP106(X0) ) ).
cnf(u2894,negated_conjecture,
sP109(sK731) ).
cnf(u1252,axiom,
( ~ sP300(X0)
| ~ p401(X0)
| ~ p1001(X0) ) ).
cnf(u2239,axiom,
( r1(X0,sK599(X0))
| ~ p509(sK598(X0))
| ~ sP65(X0) ) ).
cnf(u1999,axiom,
( r1(X0,sK478(X0))
| ~ p605(X0)
| ~ sP152(X0) ) ).
cnf(u3075,negated_conjecture,
sP241(sK731) ).
cnf(u2954,negated_conjecture,
sP160(sK731) ).
cnf(u1534,axiom,
( ~ sP300(X0)
| ~ p807(X0)
| ~ p1007(X0) ) ).
cnf(u2292,axiom,
( r1(X0,sK624(X0))
| ~ p109(sK625(X0))
| ~ sP52(X0) ) ).
cnf(u1237,axiom,
( ~ sP300(X0)
| ~ p201(X0)
| ~ p801(X0) ) ).
cnf(u2220,axiom,
( r1(X0,sK588(X0))
| ~ p609(sK589(X0))
| ~ sP70(X0) ) ).
cnf(u1548,axiom,
( ~ sP300(X0)
| sP222(X0) ) ).
cnf(u1946,axiom,
( ~ p206(sK452(X0))
| ~ p1106(X0)
| ~ sP178(X0) ) ).
cnf(u2446,axiom,
( ~ p106(sK703(X0))
| ~ p506(sK702(X0))
| ~ sP13(X0) ) ).
cnf(u2913,negated_conjecture,
sP126(sK731) ).
cnf(u1777,axiom,
( r1(X0,sK357(X0))
| ~ p1109(X0)
| ~ sP263(X0) ) ).
cnf(u1365,axiom,
( ~ sP300(X0)
| sP128(X0) ) ).
cnf(u2374,axiom,
( ~ p307(sK667(X0))
| ~ p607(sK666(X0))
| ~ sP31(X0) ) ).
cnf(u1562,axiom,
( ~ sP300(X0)
| sP229(X0) ) ).
cnf(u2928,negated_conjecture,
sP140(sK731) ).
cnf(u1235,axiom,
( ~ sP300(X0)
| ~ p201(X0)
| ~ p501(X0) ) ).
cnf(u1905,axiom,
( r1(X0,sK431(X0))
| ~ p907(X0)
| ~ sP199(X0) ) ).
cnf(u1500,axiom,
( ~ sP300(X0)
| sP195(X0) ) ).
cnf(u1640,axiom,
( r1(X0,sK305(X0))
| ~ p909(X0)
| ~ sP300(X0) ) ).
cnf(u1863,axiom,
( r1(X0,sK409(X0))
| ~ p908(X0)
| ~ sP220(X0) ) ).
cnf(u1563,axiom,
( ~ sP300(X0)
| sP230(X0) ) ).
cnf(u1451,axiom,
( ~ sP300(X0)
| sP12(X0) ) ).
cnf(u2966,negated_conjecture,
sP13(sK731) ).
cnf(u1398,axiom,
( ~ sP300(X0)
| ~ p804(X0)
| ~ p904(X0) ) ).
cnf(u1810,axiom,
( ~ p608(sK378(X0))
| ~ p1008(X0)
| ~ sP246(X0) ) ).
cnf(u1692,axiom,
( ~ sP300(X0)
| sP292(X0) ) ).
cnf(u2925,negated_conjecture,
sP137(sK731) ).
cnf(u2027,axiom,
( r1(X0,sK492(X0))
| ~ p404(X0)
| ~ sP138(X0) ) ).
cnf(u1543,axiom,
( ~ sP300(X0)
| sP39(X0) ) ).
cnf(u1735,axiom,
( r1(X0,sK330(X0))
| ~ p1110(X0)
| ~ sP284(X0) ) ).
cnf(u1431,axiom,
( ~ sP300(X0)
| sP166(X0) ) ).
cnf(u2935,negated_conjecture,
sP6(sK731) ).
cnf(u3157,negated_conjecture,
sP284(sK731) ).
cnf(u1362,axiom,
( ~ sP300(X0)
| sP125(X0) ) ).
cnf(u1762,axiom,
( ~ p609(sK348(X0))
| ~ p1009(X0)
| ~ sP270(X0) ) ).
cnf(u1862,axiom,
( ~ p108(sK409(X0))
| ~ p908(X0)
| ~ sP220(X0) ) ).
cnf(u1693,axiom,
( ~ sP300(X0)
| sP293(X0) ) ).
cnf(u3160,negated_conjecture,
sP285(sK731) ).
cnf(u1321,axiom,
( ~ sP300(X0)
| sP114(X0) ) ).
cnf(u3088,negated_conjecture,
sP55(sK731) ).
cnf(u2464,axiom,
( r1(X0,sK710(X0))
| ~ p305(sK711(X0))
| ~ sP9(X0) ) ).
cnf(u2247,axiom,
( r1(X0,sK603(X0))
| ~ p609(sK602(X0))
| ~ sP63(X0) ) ).
cnf(u1940,axiom,
( ~ p306(sK449(X0))
| ~ p906(X0)
| ~ sP181(X0) ) ).
cnf(u2152,axiom,
( r1(X0,sK554(X0))
| ~ p310(sK555(X0))
| ~ sP87(X0) ) ).
cnf(u2344,axiom,
( r1(X0,sK650(X0))
| ~ p108(sK651(X0))
| ~ sP39(X0) ) ).
cnf(u3145,negated_conjecture,
sP279(sK731) ).
cnf(u2080,axiom,
( ~ p103(sK519(X0))
| ~ p603(X0)
| ~ sP111(X0) ) ).
cnf(u2375,axiom,
( r1(X0,sK667(X0))
| ~ p607(sK666(X0))
| ~ sP31(X0) ) ).
cnf(u1456,axiom,
( ~ sP300(X0)
| sP172(X0) ) ).
cnf(u1556,axiom,
( ~ sP300(X0)
| sP226(X0) ) ).
cnf(u3073,negated_conjecture,
sP239(sK731) ).
cnf(u2980,negated_conjecture,
sP17(sK731) ).
cnf(u2431,axiom,
( r1(X0,sK695(X0))
| ~ p406(sK694(X0))
| ~ sP17(X0) ) ).
cnf(u1891,axiom,
( r1(X0,sK424(X0))
| ~ p807(X0)
| ~ sP206(X0) ) ).
cnf(u1785,axiom,
( r1(X0,sK362(X0))
| ~ p1109(X0)
| ~ sP259(X0) ) ).
cnf(u3040,negated_conjecture,
sP38(sK731) ).
cnf(u2065,axiom,
( r1(X0,sK511(X0))
| ~ p603(X0)
| ~ sP119(X0) ) ).
cnf(u1295,axiom,
( ~ sP300(X0)
| ~ p402(X0)
| ~ p802(X0) ) ).
cnf(u2931,negated_conjecture,
sP143(sK731) ).
cnf(u2951,negated_conjecture,
sP157(sK731) ).
cnf(u2032,axiom,
( ~ p204(sK495(X0))
| ~ p904(X0)
| ~ sP135(X0) ) ).
cnf(u3119,negated_conjecture,
sP265(sK731) ).
cnf(u2126,axiom,
( ~ p510(sK543(X0))
| ~ p610(sK542(X0))
| ~ sP93(X0) ) ).
cnf(u1508,axiom,
( ~ sP300(X0)
| sP199(X0) ) ).
cnf(u3007,negated_conjecture,
sP25(sK731) ).
cnf(u2258,axiom,
( ~ p209(sK609(X0))
| ~ p809(sK608(X0))
| ~ sP60(X0) ) ).
cnf(u1743,axiom,
( r1(X0,sK335(X0))
| ~ p1010(X0)
| ~ sP280(X0) ) ).
cnf(u1885,axiom,
( r1(X0,sK421(X0))
| ~ p1107(X0)
| ~ sP209(X0) ) ).
cnf(u1648,axiom,
( ~ sP300(X0)
| ~ p1009(X0)
| ~ p1109(X0) ) ).
cnf(u2186,axiom,
( ~ p210(sK573(X0))
| ~ p310(sK572(X0))
| ~ sP78(X0) ) ).
cnf(u2111,axiom,
( r1(X0,sK535(X0))
| ~ p910(sK534(X0))
| ~ sP97(X0) ) ).
cnf(u3166,negated_conjecture,
sP288(sK731) ).
cnf(u1871,axiom,
( r1(X0,sK414(X0))
| ~ p1007(X0)
| ~ sP216(X0) ) ).
cnf(u1297,axiom,
( ~ sP300(X0)
| ~ p402(X0)
| ~ p1002(X0) ) ).
cnf(u2088,axiom,
( ~ p102(sK523(X0))
| ~ p1102(X0)
| ~ sP107(X0) ) ).
cnf(u1459,axiom,
( ~ sP300(X0)
| sP15(X0) ) ).
cnf(u2476,axiom,
( r1(X0,sK716(X0))
| ~ p105(sK717(X0))
| ~ sP6(X0) ) ).
cnf(u2243,axiom,
( r1(X0,sK601(X0))
| ~ p809(sK600(X0))
| ~ sP64(X0) ) ).
cnf(u1406,axiom,
( ~ sP300(X0)
| sP6(X0) ) ).
cnf(u2164,axiom,
( r1(X0,sK560(X0))
| ~ p310(sK561(X0))
| ~ sP84(X0) ) ).
cnf(u1678,axiom,
( ~ sP300(X0)
| sP285(X0) ) ).
cnf(u2299,axiom,
( r1(X0,sK629(X0))
| ~ p209(sK628(X0))
| ~ sP50(X0) ) ).
cnf(u1521,axiom,
( ~ sP300(X0)
| sP207(X0) ) ).
cnf(u2092,axiom,
( ~ p102(sK525(X0))
| ~ p902(X0)
| ~ sP105(X0) ) ).
cnf(u2371,axiom,
( r1(X0,sK665(X0))
| ~ p507(sK664(X0))
| ~ sP32(X0) ) ).
cnf(u2021,axiom,
( r1(X0,sK489(X0))
| ~ p804(X0)
| ~ sP141(X0) ) ).
cnf(u1472,axiom,
( ~ sP300(X0)
| sP183(X0) ) ).
cnf(u3076,negated_conjecture,
sP242(sK731) ).
cnf(u1649,axiom,
( ~ sP300(X0)
| sP71(X0) ) ).
cnf(u2149,axiom,
( r1(X0,sK553(X0))
| r1(X0,sK552(X0))
| ~ sP88(X0) ) ).
cnf(u3132,negated_conjecture,
sP72(sK731) ).
cnf(u3061,negated_conjecture,
sP230(sK731) ).
cnf(u2077,axiom,
( r1(X0,sK517(X0))
| ~ p903(X0)
| ~ sP113(X0) ) ).
cnf(u3125,negated_conjecture,
sP270(sK731) ).
cnf(u2209,axiom,
( r1(X0,sK583(X0))
| r1(X0,sK582(X0))
| ~ sP73(X0) ) ).
cnf(u2225,axiom,
( r1(X0,sK591(X0))
| r1(X0,sK590(X0))
| ~ sP69(X0) ) ).
cnf(u1896,axiom,
( ~ p307(sK427(X0))
| ~ p907(X0)
| ~ sP203(X0) ) ).
cnf(u1372,axiom,
( ~ sP300(X0)
| sP134(X0) ) ).
cnf(u3117,negated_conjecture,
sP264(sK731) ).
cnf(u3003,negated_conjecture,
sP194(sK731) ).
cnf(u1985,axiom,
( r1(X0,sK471(X0))
| ~ p805(X0)
| ~ sP159(X0) ) ).
cnf(u2198,axiom,
( ~ p110(sK579(X0))
| ~ p610(sK578(X0))
| ~ sP75(X0) ) ).
cnf(u1323,axiom,
( ~ sP300(X0)
| sP116(X0) ) ).
cnf(u2411,axiom,
( r1(X0,sK685(X0))
| ~ p407(sK684(X0))
| ~ sP22(X0) ) ).
cnf(u1542,axiom,
( ~ sP300(X0)
| sP38(X0) ) ).
cnf(u1948,axiom,
( ~ p206(sK453(X0))
| ~ p1006(X0)
| ~ sP177(X0) ) ).
cnf(u1771,axiom,
( r1(X0,sK353(X0))
| ~ p1009(X0)
| ~ sP266(X0) ) ).
cnf(u1464,axiom,
( ~ sP300(X0)
| sP177(X0) ) ).
cnf(u1478,axiom,
( ~ sP300(X0)
| sP188(X0) ) ).
cnf(u2085,axiom,
( r1(X0,sK521(X0))
| ~ p403(X0)
| ~ sP109(X0) ) ).
cnf(u1899,axiom,
( r1(X0,sK428(X0))
| ~ p807(X0)
| ~ sP202(X0) ) ).
cnf(u2018,axiom,
( ~ p304(sK488(X0))
| ~ p904(X0)
| ~ sP142(X0) ) ).
cnf(u1303,axiom,
( ~ sP300(X0)
| ~ p502(X0)
| ~ p1102(X0) ) ).
cnf(u1437,axiom,
( ~ sP300(X0)
| ~ p505(X0)
| ~ p1005(X0) ) ).
cnf(u1634,axiom,
( ~ sP300(X0)
| sP268(X0) ) ).
cnf(u2040,axiom,
( ~ p204(sK499(X0))
| ~ p404(X0)
| ~ sP131(X0) ) ).
cnf(u1977,axiom,
( r1(X0,sK467(X0))
| ~ p505(X0)
| ~ sP163(X0) ) ).
cnf(u1565,axiom,
( ~ sP300(X0)
| sP232(X0) ) ).
cnf(u2408,axiom,
( r1(X0,sK682(X0))
| ~ p107(sK683(X0))
| ~ sP23(X0) ) ).
cnf(u2336,axiom,
( r1(X0,sK646(X0))
| ~ p208(sK647(X0))
| ~ sP41(X0) ) ).
cnf(u2119,axiom,
( r1(X0,sK539(X0))
| ~ p910(sK538(X0))
| ~ sP95(X0) ) ).
cnf(u2237,axiom,
( r1(X0,sK597(X0))
| r1(X0,sK596(X0))
| ~ sP66(X0) ) ).
cnf(u1812,axiom,
( ~ p608(sK379(X0))
| ~ p908(X0)
| ~ sP245(X0) ) ).
cnf(u2360,axiom,
( r1(X0,sK658(X0))
| ~ p108(sK659(X0))
| ~ sP35(X0) ) ).
cnf(u2962,negated_conjecture,
sP168(sK731) ).
cnf(u2512,negated_conjecture,
r1(sK730,sK731) ).
cnf(u1635,axiom,
( ~ sP300(X0)
| sP70(X0) ) ).
cnf(u1529,axiom,
( ~ sP300(X0)
| sP214(X0) ) ).
cnf(u1328,axiom,
( ~ sP300(X0)
| sP121(X0) ) ).
cnf(u2029,axiom,
( r1(X0,sK493(X0))
| ~ p1104(X0)
| ~ sP137(X0) ) ).
cnf(u2984,negated_conjecture,
sP181(sK731) ).
cnf(u1657,axiom,
( ~ sP300(X0)
| sP277(X0) ) ).
cnf(u2912,negated_conjecture,
sP125(sK731) ).
cnf(u2936,negated_conjecture,
sP145(sK731) ).
cnf(u2288,axiom,
( r1(X0,sK622(X0))
| ~ p109(sK623(X0))
| ~ sP53(X0) ) ).
cnf(u3138,negated_conjecture,
sP77(sK731) ).
cnf(u1764,axiom,
( ~ p609(sK349(X0))
| ~ p909(X0)
| ~ sP269(X0) ) ).
cnf(u1904,axiom,
( ~ p207(sK431(X0))
| ~ p907(X0)
| ~ sP199(X0) ) ).
cnf(u2442,axiom,
( ~ p206(sK701(X0))
| ~ p306(sK700(X0))
| ~ sP14(X0) ) ).
cnf(u1380,axiom,
( ~ sP300(X0)
| sP142(X0) ) ).
cnf(u2130,axiom,
( ~ p410(sK545(X0))
| ~ p910(sK544(X0))
| ~ sP92(X0) ) ).
cnf(u1615,axiom,
( ~ sP300(X0)
| sP63(X0) ) ).
cnf(u1503,axiom,
( ~ sP300(X0)
| sP25(X0) ) ).
cnf(u2058,axiom,
( ~ p203(sK508(X0))
| ~ p1003(X0)
| ~ sP122(X0) ) ).
cnf(u2473,axiom,
( r1(X0,sK715(X0))
| r1(X0,sK714(X0))
| ~ sP7(X0) ) ).
cnf(u3011,negated_conjecture,
sP198(sK731) ).
cnf(u2253,axiom,
( r1(X0,sK605(X0))
| r1(X0,sK604(X0))
| ~ sP62(X0) ) ).
cnf(u2420,axiom,
( r1(X0,sK688(X0))
| ~ p107(sK689(X0))
| ~ sP20(X0) ) ).
cnf(u1934,axiom,
( ~ p406(sK446(X0))
| ~ p606(X0)
| ~ sP184(X0) ) ).
cnf(u2401,axiom,
( r1(X0,sK679(X0))
| r1(X0,sK678(X0))
| ~ sP25(X0) ) ).
cnf(u1331,axiom,
( ~ sP300(X0)
| ~ p303(X0)
| ~ p403(X0) ) ).
cnf(u2348,axiom,
( r1(X0,sK652(X0))
| ~ p108(sK653(X0))
| ~ sP38(X0) ) ).
cnf(u2115,axiom,
( r1(X0,sK537(X0))
| ~ p810(sK536(X0))
| ~ sP96(X0) ) ).
cnf(u1765,axiom,
( r1(X0,sK349(X0))
| ~ p909(X0)
| ~ sP269(X0) ) ).
cnf(u2322,axiom,
( ~ p308(sK641(X0))
| ~ p408(sK640(X0))
| ~ sP44(X0) ) ).
cnf(u2440,axiom,
( r1(X0,sK698(X0))
| ~ p206(sK699(X0))
| ~ sP15(X0) ) ).
cnf(u1728,axiom,
( ~ p410(sK326(X0))
| ~ p1110(X0)
| ~ sP287(X0) ) ).
cnf(u2171,axiom,
( r1(X0,sK565(X0))
| ~ p810(sK564(X0))
| ~ sP82(X0) ) ).
cnf(u2974,negated_conjecture,
sP16(sK731) ).
cnf(u1393,axiom,
( ~ sP300(X0)
| ~ p504(X0)
| ~ p1104(X0) ) ).
cnf(u2191,axiom,
( r1(X0,sK575(X0))
| ~ p910(sK574(X0))
| ~ sP77(X0) ) ).
cnf(u1893,axiom,
( r1(X0,sK425(X0))
| ~ p1107(X0)
| ~ sP205(X0) ) ).
cnf(u3155,negated_conjecture,
sP88(sK731) ).
cnf(u3034,negated_conjecture,
sP215(sK731) ).
cnf(u1486,axiom,
( ~ sP300(X0)
| ~ p606(X0)
| ~ p1006(X0) ) ).
cnf(u2244,axiom,
( r1(X0,sK600(X0))
| ~ p309(sK601(X0))
| ~ sP64(X0) ) ).
cnf(u2933,negated_conjecture,
sP4(sK731) ).
cnf(u2300,axiom,
( r1(X0,sK628(X0))
| ~ p109(sK629(X0))
| ~ sP50(X0) ) ).
cnf(u1628,axiom,
( ~ sP300(X0)
| sP68(X0) ) ).
cnf(u2026,axiom,
( ~ p304(sK492(X0))
| ~ p404(X0)
| ~ sP138(X0) ) ).
cnf(u2993,negated_conjecture,
sP189(sK731) ).
cnf(u1729,axiom,
( r1(X0,sK326(X0))
| ~ p1110(X0)
| ~ sP287(X0) ) ).
cnf(u1445,axiom,
( ~ sP300(X0)
| ~ p805(X0)
| ~ p1105(X0) ) ).
cnf(u2454,axiom,
( ~ p106(sK707(X0))
| ~ p306(sK706(X0))
| ~ sP11(X0) ) ).
cnf(u1642,axiom,
( r1(X0,sK303(X0))
| ~ p1109(X0)
| ~ sP300(X0) ) ).
cnf(u1798,axiom,
( r1(X0,sK370(X0))
| ~ p209(sK371(X0))
| ~ sP252(X0) ) ).
cnf(u2285,axiom,
( r1(X0,sK621(X0))
| r1(X0,sK620(X0))
| ~ sP54(X0) ) ).
cnf(u1857,axiom,
( r1(X0,sK406(X0))
| r1(X0,sK405(X0))
| ~ sP223(X0) ) ).
cnf(u2252,axiom,
( r1(X0,sK604(X0))
| ~ p309(sK605(X0))
| ~ sP62(X0) ) ).
cnf(u2070,axiom,
( ~ p203(sK514(X0))
| ~ p303(X0)
| ~ sP116(X0) ) ).
cnf(u2317,axiom,
( r1(X0,sK637(X0))
| r1(X0,sK636(X0))
| ~ sP46(X0) ) ).
cnf(u2334,axiom,
( ~ p208(sK647(X0))
| ~ p408(sK646(X0))
| ~ sP41(X0) ) ).
cnf(u2413,axiom,
( r1(X0,sK685(X0))
| r1(X0,sK684(X0))
| ~ sP22(X0) ) ).
cnf(u2365,axiom,
( r1(X0,sK661(X0))
| r1(X0,sK660(X0))
| ~ sP34(X0) ) ).
cnf(u3110,negated_conjecture,
sP66(sK731) ).
cnf(u1720,axiom,
( r1(X0,sK320(X0))
| ~ p610(sK321(X0))
| ~ sP291(X0) ) ).
cnf(u1820,axiom,
( ~ p508(sK384(X0))
| ~ p1008(X0)
| ~ sP241(X0) ) ).
cnf(u1943,axiom,
( r1(X0,sK450(X0))
| ~ p806(X0)
| ~ sP180(X0) ) ).
cnf(u1643,axiom,
( ~ sP300(X0)
| sP273(X0) ) ).
cnf(u2489,axiom,
( r1(X0,sK723(X0))
| r1(X0,sK722(X0))
| ~ sP3(X0) ) ).
cnf(u1531,axiom,
( ~ sP300(X0)
| sP216(X0) ) ).
cnf(u3046,negated_conjecture,
sP222(sK731) ).
cnf(u1350,axiom,
( ~ sP300(X0)
| ~ p603(X0)
| ~ p903(X0) ) ).
cnf(u1750,axiom,
( r1(X0,sK340(X0))
| ~ p110(sK341(X0))
| ~ sP276(X0) ) ).
cnf(u1599,axiom,
( ~ sP300(X0)
| sP248(X0) ) ).
cnf(u1890,axiom,
( ~ p407(sK424(X0))
| ~ p807(X0)
| ~ sP206(X0) ) ).
cnf(u1772,axiom,
( ~ p509(sK354(X0))
| ~ p909(X0)
| ~ sP265(X0) ) ).
cnf(u3005,negated_conjecture,
sP196(sK731) ).
cnf(u1309,axiom,
( ~ sP300(X0)
| ~ p802(X0)
| ~ p1002(X0) ) ).
cnf(u2297,axiom,
( r1(X0,sK627(X0))
| r1(X0,sK626(X0))
| ~ sP51(X0) ) ).
cnf(u1849,axiom,
( r1(X0,sK401(X0))
| ~ p1108(X0)
| ~ sP227(X0) ) ).
cnf(u1623,axiom,
( ~ sP300(X0)
| sP260(X0) ) ).
cnf(u3127,negated_conjecture,
sP272(sK731) ).
cnf(u1511,axiom,
( ~ sP300(X0)
| sP29(X0) ) ).
cnf(u2887,negated_conjecture,
sP103(sK731) ).
cnf(u1442,axiom,
( ~ sP300(X0)
| ~ p605(X0)
| ~ p1105(X0) ) ).
cnf(u1942,axiom,
( ~ p306(sK450(X0))
| ~ p806(X0)
| ~ sP180(X0) ) ).
cnf(u1273,axiom,
( ~ sP300(X0)
| sP103(X0) ) ).
cnf(u1773,axiom,
( r1(X0,sK354(X0))
| ~ p909(X0)
| ~ sP265(X0) ) ).
cnf(u1401,axiom,
( ~ sP300(X0)
| ~ p904(X0)
| ~ p1004(X0) ) ).
cnf(u3168,negated_conjecture,
sP95(sK731) ).
cnf(u2892,negated_conjecture,
sP0(sK731) ).
cnf(u2100,axiom,
( ~ p102(sK529(X0))
| ~ p402(X0)
| ~ sP101(X0) ) ).
cnf(u2020,axiom,
( ~ p304(sK489(X0))
| ~ p804(X0)
| ~ sP141(X0) ) ).
cnf(u2232,axiom,
( r1(X0,sK594(X0))
| ~ p409(sK595(X0))
| ~ sP67(X0) ) ).
cnf(u2160,axiom,
( r1(X0,sK558(X0))
| ~ p310(sK559(X0))
| ~ sP85(X0) ) ).
cnf(u2455,axiom,
( r1(X0,sK707(X0))
| ~ p306(sK706(X0))
| ~ sP11(X0) ) ).
cnf(u1821,axiom,
( r1(X0,sK384(X0))
| ~ p1008(X0)
| ~ sP241(X0) ) ).
cnf(u1636,axiom,
( ~ sP300(X0)
| sP269(X0) ) ).
cnf(u3153,negated_conjecture,
sP282(sK731) ).
cnf(u3060,negated_conjecture,
sP229(sK731) ).
cnf(u2383,axiom,
( r1(X0,sK671(X0))
| ~ p407(sK670(X0))
| ~ sP29(X0) ) ).
cnf(u1971,axiom,
( r1(X0,sK464(X0))
| ~ p905(X0)
| ~ sP166(X0) ) ).
cnf(u1737,axiom,
( r1(X0,sK331(X0))
| ~ p1010(X0)
| ~ sP283(X0) ) ).
cnf(u1375,axiom,
( ~ sP300(X0)
| sP137(X0) ) ).
cnf(u2345,axiom,
( r1(X0,sK651(X0))
| r1(X0,sK650(X0))
| ~ sP39(X0) ) ).
cnf(u2883,negated_conjecture,
sP99(sK731) ).
cnf(u1306,axiom,
( ~ sP300(X0)
| ~ p602(X0)
| ~ p1002(X0) ) ).
cnf(u3031,negated_conjecture,
sP212(sK731) ).
cnf(u1984,axiom,
( ~ p305(sK471(X0))
| ~ p805(X0)
| ~ sP159(X0) ) ).
cnf(u1606,axiom,
( ~ sP300(X0)
| sP58(X0) ) ).
cnf(u2959,negated_conjecture,
sP165(sK731) ).
cnf(u1637,axiom,
( ~ sP300(X0)
| sP270(X0) ) ).
cnf(u1600,axiom,
( ~ sP300(X0)
| sP55(X0) ) ).
cnf(u2266,axiom,
( ~ p209(sK613(X0))
| ~ p509(sK612(X0))
| ~ sP58(X0) ) ).
cnf(u2063,axiom,
( r1(X0,sK510(X0))
| ~ p803(X0)
| ~ sP120(X0) ) ).
cnf(u2364,axiom,
( r1(X0,sK660(X0))
| ~ p507(sK661(X0))
| ~ sP34(X0) ) ).
cnf(u1951,axiom,
( r1(X0,sK454(X0))
| ~ p906(X0)
| ~ sP176(X0) ) ).
cnf(u1264,axiom,
( ~ sP300(X0)
| ~ p801(X0)
| ~ p1001(X0) ) ).
cnf(u2096,axiom,
( ~ p102(sK527(X0))
| ~ p602(X0)
| ~ sP103(X0) ) ).
cnf(u1411,axiom,
( ~ sP300(X0)
| sP149(X0) ) ).
cnf(u2906,negated_conjecture,
sP121(sK731) ).
cnf(u1258,axiom,
( ~ sP300(X0)
| ~ p501(X0)
| ~ p1101(X0) ) ).
cnf(u1358,axiom,
( ~ sP300(X0)
| ~ p1003(X0)
| ~ p1103(X0) ) ).
cnf(u2116,axiom,
( r1(X0,sK536(X0))
| ~ p610(sK537(X0))
| ~ sP96(X0) ) ).
cnf(u2338,axiom,
( ~ p208(sK649(X0))
| ~ p308(sK648(X0))
| ~ sP40(X0) ) ).
cnf(u2251,axiom,
( r1(X0,sK605(X0))
| ~ p509(sK604(X0))
| ~ sP62(X0) ) ).
cnf(u1473,axiom,
( ~ sP300(X0)
| sP19(X0) ) ).
cnf(u2172,axiom,
( r1(X0,sK564(X0))
| ~ p210(sK565(X0))
| ~ sP82(X0) ) ).
cnf(u2451,axiom,
( r1(X0,sK705(X0))
| ~ p406(sK704(X0))
| ~ sP12(X0) ) ).
cnf(u1898,axiom,
( ~ p307(sK428(X0))
| ~ p807(X0)
| ~ sP202(X0) ) ).
cnf(u2398,axiom,
( ~ p207(sK679(X0))
| ~ p307(sK678(X0))
| ~ sP25(X0) ) ).
cnf(u3156,negated_conjecture,
sP283(sK731) ).
cnf(u1601,axiom,
( ~ sP300(X0)
| sP249(X0) ) ).
cnf(u1317,axiom,
( ~ sP300(X0)
| sP110(X0) ) ).
cnf(u2326,axiom,
( ~ p208(sK643(X0))
| ~ p608(sK642(X0))
| ~ sP43(X0) ) ).
cnf(u2229,axiom,
( r1(X0,sK593(X0))
| r1(X0,sK592(X0))
| ~ sP68(X0) ) ).
cnf(u3084,negated_conjecture,
sP52(sK731) ).
cnf(u3013,negated_conjecture,
sP200(sK731) ).
cnf(u2157,axiom,
( r1(X0,sK557(X0))
| r1(X0,sK556(X0))
| ~ sP86(X0) ) ).
cnf(u2289,axiom,
( r1(X0,sK623(X0))
| r1(X0,sK622(X0))
| ~ sP53(X0) ) ).
cnf(u2357,axiom,
( r1(X0,sK657(X0))
| r1(X0,sK656(X0))
| ~ sP36(X0) ) ).
cnf(u1976,axiom,
( ~ p405(sK467(X0))
| ~ p505(X0)
| ~ sP163(X0) ) ).
cnf(u1452,axiom,
( ~ sP300(X0)
| sP13(X0) ) ).
cnf(u1320,axiom,
( ~ sP300(X0)
| sP113(X0) ) ).
cnf(u2955,negated_conjecture,
sP161(sK731) ).
cnf(u2350,axiom,
( ~ p108(sK655(X0))
| ~ p408(sK654(X0))
| ~ sP37(X0) ) ).
cnf(u1592,axiom,
( ~ sP300(X0)
| ~ p908(X0)
| ~ p1108(X0) ) ).
cnf(u1840,axiom,
( ~ p308(sK396(X0))
| ~ p1008(X0)
| ~ sP231(X0) ) ).
cnf(u1815,axiom,
( r1(X0,sK380(X0))
| ~ p808(X0)
| ~ sP244(X0) ) ).
cnf(u2248,axiom,
( r1(X0,sK602(X0))
| ~ p309(sK603(X0))
| ~ sP63(X0) ) ).
cnf(u1403,axiom,
( ~ sP300(X0)
| ~ p1004(X0)
| ~ p1104(X0) ) ).
cnf(u2918,negated_conjecture,
sP3(sK731) ).
cnf(u1993,axiom,
( r1(X0,sK475(X0))
| ~ p1005(X0)
| ~ sP155(X0) ) ).
cnf(u1622,axiom,
( ~ sP300(X0)
| sP66(X0) ) ).
cnf(u2028,axiom,
( ~ p204(sK493(X0))
| ~ p1104(X0)
| ~ sP137(X0) ) ).
cnf(u1416,axiom,
( ~ sP300(X0)
| sP152(X0) ) ).
cnf(u2920,negated_conjecture,
sP132(sK731) ).
cnf(u1593,axiom,
( ~ sP300(X0)
| ~ p1008(X0)
| ~ p1108(X0) ) ).
cnf(u1979,axiom,
( r1(X0,sK468(X0))
| ~ p1105(X0)
| ~ sP162(X0) ) ).
cnf(u1383,axiom,
( ~ sP300(X0)
| ~ p404(X0)
| ~ p504(X0) ) ).
cnf(u1829,axiom,
( r1(X0,sK389(X0))
| ~ p1108(X0)
| ~ sP237(X0) ) ).
cnf(u2301,axiom,
( r1(X0,sK629(X0))
| r1(X0,sK628(X0))
| ~ sP50(X0) ) ).
cnf(u1314,axiom,
( ~ sP300(X0)
| sP0(X0) ) ).
cnf(u1714,axiom,
( r1(X0,sK317(X0))
| ~ p810(sK316(X0))
| ~ sP294(X0) ) ).
cnf(u1992,axiom,
( ~ p205(sK475(X0))
| ~ p1005(X0)
| ~ sP155(X0) ) ).
cnf(u1584,axiom,
( r1(X0,sK309(X0))
| ~ p808(X0)
| ~ sP300(X0) ) ).
cnf(u1929,axiom,
( r1(X0,sK443(X0))
| ~ p1006(X0)
| ~ sP187(X0) ) ).
cnf(u1645,axiom,
( ~ sP300(X0)
| sP275(X0) ) ).
cnf(u3112,negated_conjecture,
sP67(sK731) ).
cnf(u2402,axiom,
( ~ p107(sK681(X0))
| ~ p607(sK680(X0))
| ~ sP24(X0) ) ).
cnf(u3068,negated_conjecture,
sP235(sK731) ).
cnf(u2416,axiom,
( r1(X0,sK686(X0))
| ~ p107(sK687(X0))
| ~ sP21(X0) ) ).
cnf(u2199,axiom,
( r1(X0,sK579(X0))
| ~ p610(sK578(X0))
| ~ sP75(X0) ) ).
cnf(u1892,axiom,
( ~ p307(sK425(X0))
| ~ p1107(X0)
| ~ sP205(X0) ) ).
cnf(u2104,axiom,
( ~ p102(sK531(X0))
| ~ p202(X0)
| ~ sP99(X0) ) ).
cnf(u3042,negated_conjecture,
sP218(sK731) ).
cnf(u3097,negated_conjecture,
sP60(sK731) ).
cnf(u1715,axiom,
( r1(X0,sK317(X0))
| r1(X0,sK316(X0))
| ~ sP294(X0) ) ).
cnf(u1481,axiom,
( ~ sP300(X0)
| sP191(X0) ) ).
cnf(u1280,axiom,
( ~ sP300(X0)
| ~ p202(X0)
| ~ p502(X0) ) ).
cnf(u2932,negated_conjecture,
sP144(sK731) ).
cnf(u3064,negated_conjecture,
sP47(sK731) ).
cnf(u1843,axiom,
( r1(X0,sK397(X0))
| ~ p908(X0)
| ~ sP230(X0) ) ).
cnf(u1609,axiom,
( ~ sP300(X0)
| sP60(X0) ) ).
cnf(u2089,axiom,
( r1(X0,sK523(X0))
| ~ p1102(X0)
| ~ sP107(X0) ) ).
cnf(u2992,negated_conjecture,
sP188(sK731) ).
cnf(u2240,axiom,
( r1(X0,sK598(X0))
| ~ p409(sK599(X0))
| ~ sP65(X0) ) ).
cnf(u2325,axiom,
( r1(X0,sK641(X0))
| r1(X0,sK640(X0))
| ~ sP44(X0) ) ).
cnf(u3146,negated_conjecture,
sP82(sK731) ).
cnf(u1856,axiom,
( r1(X0,sK405(X0))
| ~ p208(sK406(X0))
| ~ sP223(X0) ) ).
cnf(u2177,axiom,
( r1(X0,sK567(X0))
| r1(X0,sK566(X0))
| ~ sP81(X0) ) ).
cnf(u2078,axiom,
( ~ p103(sK518(X0))
| ~ p803(X0)
| ~ sP112(X0) ) ).
cnf(u1670,axiom,
( ~ sP300(X0)
| sP86(X0) ) ).
cnf(u2210,axiom,
( ~ p110(sK585(X0))
| ~ p310(sK584(X0))
| ~ sP72(X0) ) ).
cnf(u1695,axiom,
( ~ sP300(X0)
| sP295(X0) ) ).
cnf(u2361,axiom,
( r1(X0,sK659(X0))
| r1(X0,sK658(X0))
| ~ sP35(X0) ) ).
cnf(u2138,axiom,
( ~ p410(sK549(X0))
| ~ p610(sK548(X0))
| ~ sP90(X0) ) ).
cnf(u1514,axiom,
( ~ sP300(X0)
| sP202(X0) ) ).
cnf(u3118,negated_conjecture,
sP69(sK731) ).
cnf(u2372,axiom,
( r1(X0,sK664(X0))
| ~ p407(sK665(X0))
| ~ sP32(X0) ) ).
cnf(u2014,axiom,
( ~ p304(sK486(X0))
| ~ p1104(X0)
| ~ sP144(X0) ) ).
cnf(u2448,axiom,
( r1(X0,sK702(X0))
| ~ p106(sK703(X0))
| ~ sP13(X0) ) ).
cnf(u1283,axiom,
( ~ sP300(X0)
| ~ p202(X0)
| ~ p902(X0) ) ).
cnf(u2428,axiom,
( r1(X0,sK692(X0))
| ~ p306(sK693(X0))
| ~ sP18(X0) ) ).
cnf(u2195,axiom,
( r1(X0,sK577(X0))
| ~ p810(sK576(X0))
| ~ sP76(X0) ) ).
cnf(u2330,axiom,
( ~ p208(sK645(X0))
| ~ p508(sK644(X0))
| ~ sP42(X0) ) ).
cnf(u2432,axiom,
( r1(X0,sK694(X0))
| ~ p306(sK695(X0))
| ~ sP17(X0) ) ).
cnf(u1630,axiom,
( ~ sP300(X0)
| sP69(X0) ) ).
cnf(u2969,negated_conjecture,
sP171(sK731) ).
cnf(u3054,negated_conjecture,
sP226(sK731) ).
cnf(u1345,axiom,
( ~ sP300(X0)
| ~ p503(X0)
| ~ p803(X0) ) ).
cnf(u2271,axiom,
( r1(X0,sK615(X0))
| ~ p409(sK614(X0))
| ~ sP57(X0) ) ).
cnf(u2323,axiom,
( r1(X0,sK641(X0))
| ~ p408(sK640(X0))
| ~ sP44(X0) ) ).
cnf(u1973,axiom,
( r1(X0,sK465(X0))
| ~ p805(X0)
| ~ sP165(X0) ) ).
cnf(u1731,axiom,
( r1(X0,sK327(X0))
| ~ p1010(X0)
| ~ sP286(X0) ) ).
cnf(u1424,axiom,
( ~ sP300(X0)
| sP159(X0) ) ).
cnf(u2131,axiom,
( r1(X0,sK545(X0))
| ~ p910(sK544(X0))
| ~ sP92(X0) ) ).
cnf(u3163,negated_conjecture,
sP286(sK731) ).
cnf(u1263,axiom,
( ~ sP300(X0)
| ~ p801(X0)
| ~ p901(X0) ) ).
cnf(u3004,negated_conjecture,
sP195(sK731) ).
cnf(u1837,axiom,
( r1(X0,sK394(X0))
| r1(X0,sK393(X0))
| ~ sP233(X0) ) ).
cnf(u2945,negated_conjecture,
sP152(sK731) ).
cnf(u1848,axiom,
( ~ p208(sK401(X0))
| ~ p1108(X0)
| ~ sP227(X0) ) ).
cnf(u1525,axiom,
( ~ sP300(X0)
| sP210(X0) ) ).
cnf(u1324,axiom,
( ~ sP300(X0)
| sP117(X0) ) ).
cnf(u1722,axiom,
( ~ p510(sK322(X0))
| ~ p1110(X0)
| ~ sP290(X0) ) ).
cnf(u1937,axiom,
( r1(X0,sK447(X0))
| ~ p1106(X0)
| ~ sP183(X0) ) ).
cnf(u2306,axiom,
( ~ p408(sK633(X0))
| ~ p608(sK632(X0))
| ~ sP48(X0) ) ).
cnf(u2150,axiom,
( ~ p310(sK555(X0))
| ~ p810(sK554(X0))
| ~ sP87(X0) ) ).
cnf(u2437,axiom,
( r1(X0,sK697(X0))
| r1(X0,sK696(X0))
| ~ sP16(X0) ) ).
cnf(u2493,axiom,
( r1(X0,sK725(X0))
| r1(X0,sK724(X0))
| ~ sP2(X0) ) ).
cnf(u2981,negated_conjecture,
sP18(sK731) ).
cnf(u1912,axiom,
( ~ p107(sK435(X0))
| ~ p907(X0)
| ~ sP195(X0) ) ).
cnf(u1672,axiom,
( ~ sP300(X0)
| sP87(X0) ) ).
cnf(u1900,axiom,
( ~ p207(sK429(X0))
| ~ p1107(X0)
| ~ sP201(X0) ) ).
cnf(u1276,axiom,
( ~ sP300(X0)
| sP106(X0) ) ).
cnf(u2023,axiom,
( r1(X0,sK490(X0))
| ~ p604(X0)
| ~ sP140(X0) ) ).
cnf(u1723,axiom,
( r1(X0,sK322(X0))
| ~ p1110(X0)
| ~ sP290(X0) ) ).
cnf(u1483,axiom,
( ~ sP300(X0)
| sP193(X0) ) ).
cnf(u2071,axiom,
( r1(X0,sK514(X0))
| ~ p303(X0)
| ~ sP116(X0) ) ).
cnf(u1430,axiom,
( ~ sP300(X0)
| sP165(X0) ) ).
cnf(u1851,axiom,
( r1(X0,sK402(X0))
| ~ p1008(X0)
| ~ sP226(X0) ) ).
cnf(u1261,axiom,
( ~ sP300(X0)
| ~ p601(X0)
| ~ p1001(X0) ) ).
cnf(u2059,axiom,
( r1(X0,sK508(X0))
| ~ p1003(X0)
| ~ sP122(X0) ) ).
cnf(u1970,axiom,
( ~ p405(sK464(X0))
| ~ p905(X0)
| ~ sP166(X0) ) ).
cnf(u2957,negated_conjecture,
sP163(sK731) ).
cnf(u1389,axiom,
( ~ sP300(X0)
| ~ p504(X0)
| ~ p604(X0) ) ).
cnf(u1586,axiom,
( r1(X0,sK307(X0))
| ~ p1008(X0)
| ~ sP300(X0) ) ).
cnf(u1298,axiom,
( ~ sP300(X0)
| ~ p402(X0)
| ~ p1102(X0) ) ).
cnf(u1240,axiom,
( ~ sP300(X0)
| ~ p201(X0)
| ~ p1101(X0) ) ).
cnf(u1703,axiom,
( ~ sP300(X0)
| ~ p1010(X0)
| ~ p1110(X0) ) ).
cnf(u1834,axiom,
( ~ p408(sK392(X0))
| ~ p808(X0)
| ~ sP234(X0) ) ).
cnf(u2967,negated_conjecture,
sP169(sK731) ).
cnf(u1522,axiom,
( ~ sP300(X0)
| sP208(X0) ) ).
cnf(u2022,axiom,
( ~ p304(sK490(X0))
| ~ p604(X0)
| ~ sP140(X0) ) ).
cnf(u1987,axiom,
( r1(X0,sK472(X0))
| ~ p605(X0)
| ~ sP158(X0) ) ).
cnf(u1225,axiom,
( ~ sP300(X0)
| ~ p101(X0)
| ~ p301(X0) ) ).
cnf(u2914,negated_conjecture,
sP127(sK731) ).
cnf(u1551,axiom,
( ~ sP300(X0)
| sP42(X0) ) ).
cnf(u1587,axiom,
( r1(X0,sK306(X0))
| ~ p1108(X0)
| ~ sP300(X0) ) ).
cnf(u1353,axiom,
( ~ sP300(X0)
| ~ p803(X0)
| ~ p903(X0) ) ).
cnf(u1981,axiom,
( r1(X0,sK469(X0))
| ~ p1005(X0)
| ~ sP161(X0) ) ).
cnf(u2052,axiom,
( ~ p104(sK505(X0))
| ~ p504(X0)
| ~ sP125(X0) ) ).
cnf(u2405,axiom,
( r1(X0,sK681(X0))
| r1(X0,sK680(X0))
| ~ sP24(X0) ) ).
cnf(u2184,axiom,
( r1(X0,sK570(X0))
| ~ p210(sK571(X0))
| ~ sP79(X0) ) ).
cnf(u2112,axiom,
( r1(X0,sK534(X0))
| ~ p610(sK535(X0))
| ~ sP97(X0) ) ).
cnf(u3090,negated_conjecture,
sP250(sK731) ).
cnf(u1716,axiom,
( ~ p610(sK318(X0))
| ~ p1110(X0)
| ~ sP293(X0) ) ).
cnf(u2466,axiom,
( ~ p205(sK713(X0))
| ~ p405(sK712(X0))
| ~ sP8(X0) ) ).
cnf(u3012,negated_conjecture,
sP199(sK731) ).
cnf(u2463,axiom,
( r1(X0,sK711(X0))
| ~ p405(sK710(X0))
| ~ sP9(X0) ) ).
cnf(u1923,axiom,
( r1(X0,sK440(X0))
| ~ p806(X0)
| ~ sP190(X0) ) ).
cnf(u2394,axiom,
( ~ p207(sK677(X0))
| ~ p407(sK676(X0))
| ~ sP26(X0) ) ).
cnf(u2343,axiom,
( r1(X0,sK651(X0))
| ~ p608(sK650(X0))
| ~ sP39(X0) ) ).
cnf(u1332,axiom,
( ~ sP300(X0)
| ~ p303(X0)
| ~ p503(X0) ) ).
cnf(u2082,axiom,
( ~ p103(sK520(X0))
| ~ p503(X0)
| ~ sP110(X0) ) ).
cnf(u1246,axiom,
( ~ sP300(X0)
| ~ p301(X0)
| ~ p1001(X0) ) ).
cnf(u1455,axiom,
( ~ sP300(X0)
| sP171(X0) ) ).
cnf(u2425,axiom,
( r1(X0,sK691(X0))
| r1(X0,sK690(X0))
| ~ sP19(X0) ) ).
cnf(u2963,negated_conjecture,
sP10(sK731) ).
cnf(u1386,axiom,
( ~ sP300(X0)
| ~ p404(X0)
| ~ p904(X0) ) ).
cnf(u1886,axiom,
( ~ p407(sK422(X0))
| ~ p1007(X0)
| ~ sP208(X0) ) ).
cnf(u2353,axiom,
( r1(X0,sK655(X0))
| r1(X0,sK654(X0))
| ~ sP37(X0) ) ).
cnf(u3151,negated_conjecture,
sP85(sK731) ).
cnf(u2286,axiom,
( ~ p109(sK623(X0))
| ~ p509(sK622(X0))
| ~ sP53(X0) ) ).
cnf(u3039,negated_conjecture,
sP37(sK731) ).
cnf(u2067,axiom,
( r1(X0,sK512(X0))
| ~ p503(X0)
| ~ sP118(X0) ) ).
cnf(u1717,axiom,
( r1(X0,sK318(X0))
| ~ p1110(X0)
| ~ sP293(X0) ) ).
cnf(u1680,axiom,
( ~ sP300(X0)
| sP92(X0) ) ).
cnf(u2926,negated_conjecture,
sP138(sK731) ).
cnf(u2143,axiom,
( r1(X0,sK551(X0))
| ~ p510(sK550(X0))
| ~ sP89(X0) ) ).
cnf(u2031,axiom,
( r1(X0,sK494(X0))
| ~ p1004(X0)
| ~ sP136(X0) ) ).
cnf(u1491,axiom,
( ~ sP300(X0)
| ~ p906(X0)
| ~ p1006(X0) ) ).
cnf(u2986,negated_conjecture,
sP183(sK731) ).
cnf(u1438,axiom,
( ~ sP300(X0)
| ~ p505(X0)
| ~ p1105(X0) ) ).
cnf(u2196,axiom,
( r1(X0,sK576(X0))
| ~ p110(sK577(X0))
| ~ sP76(X0) ) ).
cnf(u1269,axiom,
( ~ sP300(X0)
| sP99(X0) ) ).
cnf(u2124,axiom,
( r1(X0,sK540(X0))
| ~ p510(sK541(X0))
| ~ sP94(X0) ) ).
cnf(u1580,axiom,
( ~ sP300(X0)
| sP244(X0) ) ).
cnf(u1978,axiom,
( ~ p305(sK468(X0))
| ~ p1105(X0)
| ~ sP162(X0) ) ).
cnf(u2478,axiom,
( ~ p105(sK719(X0))
| ~ p305(sK718(X0))
| ~ sP5(X0) ) ).
cnf(u1681,axiom,
( ~ sP300(X0)
| sP286(X0) ) ).
cnf(u1397,axiom,
( ~ sP300(X0)
| ~ p604(X0)
| ~ p1104(X0) ) ).
cnf(u2406,axiom,
( ~ p107(sK683(X0))
| ~ p507(sK682(X0))
| ~ sP23(X0) ) ).
cnf(u1594,axiom,
( ~ sP300(X0)
| sP50(X0) ) ).
cnf(u3164,negated_conjecture,
sP287(sK731) ).
cnf(u1809,axiom,
( r1(X0,sK377(X0))
| ~ p1108(X0)
| ~ sP247(X0) ) ).
cnf(u2241,axiom,
( r1(X0,sK599(X0))
| r1(X0,sK598(X0))
| ~ sP65(X0) ) ).
cnf(u2309,axiom,
( r1(X0,sK633(X0))
| r1(X0,sK632(X0))
| ~ sP48(X0) ) ).
cnf(u2358,axiom,
( ~ p108(sK659(X0))
| ~ p208(sK658(X0))
| ~ sP35(X0) ) ).
cnf(u1532,axiom,
( ~ sP300(X0)
| sP217(X0) ) ).
cnf(u3149,negated_conjecture,
sP281(sK731) ).
cnf(u3035,negated_conjecture,
sP216(sK731) ).
cnf(u1233,axiom,
( ~ sP300(X0)
| ~ p201(X0)
| ~ p301(X0) ) ).
cnf(u1559,axiom,
( ~ sP300(X0)
| sP45(X0) ) ).
cnf(u1544,axiom,
( ~ sP300(X0)
| sP218(X0) ) ).
cnf(u2479,axiom,
( r1(X0,sK719(X0))
| ~ p305(sK718(X0))
| ~ sP5(X0) ) ).
cnf(u2427,axiom,
( r1(X0,sK693(X0))
| ~ p506(sK692(X0))
| ~ sP18(X0) ) ).
cnf(u1895,axiom,
( r1(X0,sK426(X0))
| ~ p1007(X0)
| ~ sP204(X0) ) ).
cnf(u1595,axiom,
( ~ sP300(X0)
| sP51(X0) ) ).
cnf(u1355,axiom,
( ~ sP300(X0)
| ~ p803(X0)
| ~ p1103(X0) ) ).
cnf(u2998,negated_conjecture,
sP20(sK731) ).
cnf(u1302,axiom,
( ~ sP300(X0)
| ~ p502(X0)
| ~ p1002(X0) ) ).
cnf(u1767,axiom,
( r1(X0,sK351(X0))
| r1(X0,sK350(X0))
| ~ sP268(X0) ) ).
cnf(u1702,axiom,
( ~ sP300(X0)
| sP299(X0) ) ).
cnf(u1842,axiom,
( ~ p308(sK397(X0))
| ~ p908(X0)
| ~ sP230(X0) ) ).
cnf(u1724,axiom,
( ~ p510(sK323(X0))
| ~ p1010(X0)
| ~ sP289(X0) ) ).
cnf(u1557,axiom,
( ~ sP300(X0)
| sP227(X0) ) ).
cnf(u1931,axiom,
( r1(X0,sK444(X0))
| ~ p906(X0)
| ~ sP186(X0) ) ).
cnf(u1254,axiom,
( ~ sP300(X0)
| ~ p501(X0)
| ~ p601(X0) ) ).
cnf(u1463,axiom,
( ~ sP300(X0)
| sP176(X0) ) ).
cnf(u1780,axiom,
( ~ p409(sK359(X0))
| ~ p909(X0)
| ~ sP261(X0) ) ).
cnf(u1394,axiom,
( ~ sP300(X0)
| ~ p604(X0)
| ~ p804(X0) ) ).
cnf(u1666,axiom,
( ~ sP300(X0)
| sP280(X0) ) ).
cnf(u1894,axiom,
( ~ p307(sK426(X0))
| ~ p1007(X0)
| ~ sP204(X0) ) ).
cnf(u2109,axiom,
( r1(X0,sK533(X0))
| r1(X0,sK532(X0))
| ~ sP98(X0) ) ).
cnf(u2009,axiom,
( r1(X0,sK483(X0))
| ~ p805(X0)
| ~ sP147(X0) ) ).
cnf(u1725,axiom,
( r1(X0,sK323(X0))
| ~ p1010(X0)
| ~ sP289(X0) ) ).
cnf(u2000,axiom,
( ~ p205(sK479(X0))
| ~ p505(X0)
| ~ sP151(X0) ) ).
cnf(u1282,axiom,
( ~ sP300(X0)
| ~ p202(X0)
| ~ p802(X0) ) ).
cnf(u1853,axiom,
( r1(X0,sK403(X0))
| ~ p908(X0)
| ~ sP225(X0) ) ).
cnf(u3049,negated_conjecture,
sP42(sK731) ).
cnf(u2368,axiom,
( r1(X0,sK662(X0))
| ~ p407(sK663(X0))
| ~ sP33(X0) ) ).
cnf(u2279,axiom,
( r1(X0,sK619(X0))
| ~ p809(sK618(X0))
| ~ sP55(X0) ) ).
cnf(u1972,axiom,
( ~ p405(sK465(X0))
| ~ p805(X0)
| ~ sP165(X0) ) ).
cnf(u2056,axiom,
( ~ p203(sK507(X0))
| ~ p1103(X0)
| ~ sP123(X0) ) ).
cnf(u2211,axiom,
( r1(X0,sK585(X0))
| ~ p310(sK584(X0))
| ~ sP72(X0) ) ).
cnf(u1667,axiom,
( ~ sP300(X0)
| sP281(X0) ) ).
cnf(u1360,axiom,
( ~ sP300(X0)
| sP2(X0) ) ).
cnf(u1588,axiom,
( ~ sP300(X0)
| ~ p808(X0)
| ~ p908(X0) ) ).
cnf(u3105,negated_conjecture,
sP64(sK731) ).
cnf(u2884,negated_conjecture,
sP100(sK731) ).
cnf(u2335,axiom,
( r1(X0,sK647(X0))
| ~ p408(sK646(X0))
| ~ sP41(X0) ) ).
cnf(u3016,negated_conjecture,
sP30(sK731) ).
cnf(u1795,axiom,
( r1(X0,sK368(X0))
| ~ p1009(X0)
| ~ sP254(X0) ) ).
cnf(u1689,axiom,
( ~ sP300(X0)
| sP291(X0) ) ).
cnf(u2169,axiom,
( r1(X0,sK563(X0))
| r1(X0,sK562(X0))
| ~ sP83(X0) ) ).
cnf(u2944,negated_conjecture,
sP151(sK731) ).
cnf(u1329,axiom,
( ~ sP300(X0)
| sP122(X0) ) ).
cnf(u1327,axiom,
( ~ sP300(X0)
| sP120(X0) ) ).
cnf(u1989,axiom,
( r1(X0,sK473(X0))
| ~ p505(X0)
| ~ sP157(X0) ) ).
cnf(u1936,axiom,
( ~ p306(sK447(X0))
| ~ p1106(X0)
| ~ sP183(X0) ) ).
cnf(u2158,axiom,
( ~ p310(sK559(X0))
| ~ p510(sK558(X0))
| ~ sP85(X0) ) ).
cnf(u1412,axiom,
( ~ sP300(X0)
| sP150(X0) ) ).
cnf(u2911,negated_conjecture,
sP124(sK731) ).
cnf(u2290,axiom,
( ~ p109(sK625(X0))
| ~ p409(sK624(X0))
| ~ sP52(X0) ) ).
cnf(u1589,axiom,
( ~ sP300(X0)
| ~ p808(X0)
| ~ p1008(X0) ) ).
cnf(u1552,axiom,
( ~ sP300(X0)
| sP43(X0) ) ).
cnf(u2218,axiom,
( ~ p609(sK589(X0))
| ~ p809(sK588(X0))
| ~ sP70(X0) ) ).
cnf(u2452,axiom,
( r1(X0,sK704(X0))
| ~ p106(sK705(X0))
| ~ sP12(X0) ) ).
cnf(u1903,axiom,
( r1(X0,sK430(X0))
| ~ p1007(X0)
| ~ sP200(X0) ) ).
cnf(u3052,negated_conjecture,
sP224(sK731) ).
cnf(u1363,axiom,
( ~ sP300(X0)
| sP126(X0) ) ).
cnf(u2491,axiom,
( r1(X0,sK725(X0))
| ~ p304(sK724(X0))
| ~ sP2(X0) ) ).
cnf(u2380,axiom,
( r1(X0,sK668(X0))
| ~ p307(sK669(X0))
| ~ sP30(X0) ) ).
cnf(u2275,axiom,
( r1(X0,sK617(X0))
| ~ p309(sK616(X0))
| ~ sP56(X0) ) ).
cnf(u1310,axiom,
( ~ sP300(X0)
| ~ p802(X0)
| ~ p1102(X0) ) ).
cnf(u2205,axiom,
( r1(X0,sK581(X0))
| r1(X0,sK580(X0))
| ~ sP74(X0) ) ).
cnf(u1710,axiom,
( ~ p810(sK313(X0))
| ~ p1010(X0)
| ~ sP296(X0) ) ).
cnf(u3029,negated_conjecture,
sP210(sK731) ).
cnf(u2203,axiom,
( r1(X0,sK581(X0))
| ~ p510(sK580(X0))
| ~ sP74(X0) ) ).
cnf(u1425,axiom,
( ~ sP300(X0)
| sP160(X0) ) ).
cnf(u2403,axiom,
( r1(X0,sK681(X0))
| ~ p607(sK680(X0))
| ~ sP24(X0) ) ).
cnf(u1925,axiom,
( r1(X0,sK441(X0))
| ~ p606(X0)
| ~ sP189(X0) ) ).
cnf(u1504,axiom,
( ~ sP300(X0)
| sP26(X0) ) ).
cnf(u2331,axiom,
( r1(X0,sK645(X0))
| ~ p508(sK644(X0))
| ~ sP42(X0) ) ).
cnf(u1553,axiom,
( ~ sP300(X0)
| sP223(X0) ) ).
cnf(u3020,negated_conjecture,
sP204(sK731) ).
cnf(u2053,axiom,
( r1(X0,sK505(X0))
| ~ p504(X0)
| ~ sP125(X0) ) ).
cnf(u2956,negated_conjecture,
sP162(sK731) ).
cnf(u2113,axiom,
( r1(X0,sK535(X0))
| r1(X0,sK534(X0))
| ~ sP97(X0) ) ).
cnf(u3025,negated_conjecture,
sP207(sK731) ).
cnf(u3093,negated_conjecture,
sP57(sK731) ).
cnf(u1477,axiom,
( ~ sP300(X0)
| sP187(X0) ) ).
cnf(u1404,axiom,
( ~ sP300(X0)
| sP4(X0) ) ).
cnf(u1674,axiom,
( ~ sP300(X0)
| sP283(X0) ) ).
cnf(u2907,negated_conjecture,
sP122(sK731) ).
cnf(u2017,axiom,
( r1(X0,sK487(X0))
| ~ p1004(X0)
| ~ sP143(X0) ) ).
cnf(u2230,axiom,
( ~ p409(sK595(X0))
| ~ p809(sK594(X0))
| ~ sP67(X0) ) ).
cnf(u2445,axiom,
( r1(X0,sK701(X0))
| r1(X0,sK700(X0))
| ~ sP14(X0) ) ).
cnf(u2332,axiom,
( r1(X0,sK644(X0))
| ~ p208(sK645(X0))
| ~ sP42(X0) ) ).
cnf(u3142,negated_conjecture,
sP79(sK731) ).
cnf(u1752,axiom,
( ~ p809(sK342(X0))
| ~ p1109(X0)
| ~ sP275(X0) ) ).
cnf(u1980,axiom,
( ~ p305(sK469(X0))
| ~ p1005(X0)
| ~ sP161(X0) ) ).
cnf(u1228,axiom,
( ~ sP300(X0)
| ~ p101(X0)
| ~ p601(X0) ) ).
cnf(u1675,axiom,
( ~ sP300(X0)
| sP284(X0) ) ).
cnf(u1368,axiom,
( ~ sP300(X0)
| sP3(X0) ) ).
cnf(u1510,axiom,
( ~ sP300(X0)
| sP201(X0) ) ).
cnf(u1803,axiom,
( r1(X0,sK373(X0))
| ~ p1009(X0)
| ~ sP250(X0) ) ).
cnf(u1337,axiom,
( ~ sP300(X0)
| ~ p303(X0)
| ~ p1103(X0) ) ).
cnf(u1922,axiom,
( ~ p506(sK440(X0))
| ~ p806(X0)
| ~ sP190(X0) ) ).
cnf(u1335,axiom,
( ~ sP300(X0)
| ~ p303(X0)
| ~ p903(X0) ) ).
cnf(u3037,negated_conjecture,
sP35(sK731) ).
cnf(u1469,axiom,
( ~ sP300(X0)
| sP180(X0) ) ).
cnf(u1538,axiom,
( ~ sP300(X0)
| ~ p1007(X0)
| ~ p1107(X0) ) ).
cnf(u2087,axiom,
( r1(X0,sK522(X0))
| ~ p303(X0)
| ~ sP108(X0) ) ).
cnf(u1881,axiom,
( r1(X0,sK419(X0))
| ~ p907(X0)
| ~ sP211(X0) ) ).
cnf(u1597,axiom,
( ~ sP300(X0)
| sP53(X0) ) ).
cnf(u3159,negated_conjecture,
sP90(sK731) ).
cnf(u1243,axiom,
( ~ sP300(X0)
| ~ p301(X0)
| ~ p601(X0) ) ).
cnf(u1474,axiom,
( ~ sP300(X0)
| sP184(X0) ) ).
cnf(u1550,axiom,
( ~ sP300(X0)
| sP41(X0) ) ).
cnf(u2151,axiom,
( r1(X0,sK555(X0))
| ~ p810(sK554(X0))
| ~ sP87(X0) ) ).
cnf(u2303,axiom,
( r1(X0,sK631(X0))
| ~ p608(sK630(X0))
| ~ sP49(X0) ) ).
cnf(u1844,axiom,
( ~ p308(sK398(X0))
| ~ p808(X0)
| ~ sP229(X0) ) ).
cnf(u2994,negated_conjecture,
sP190(sK731) ).
cnf(u1539,axiom,
( ~ sP300(X0)
| sP35(X0) ) ).
cnf(u1433,axiom,
( ~ sP300(X0)
| sP168(X0) ) ).
cnf(u1933,axiom,
( r1(X0,sK445(X0))
| ~ p806(X0)
| ~ sP185(X0) ) ).
cnf(u2257,axiom,
( r1(X0,sK607(X0))
| r1(X0,sK606(X0))
| ~ sP61(X0) ) ).
cnf(u2888,negated_conjecture,
sP104(sK731) ).
cnf(u2264,axiom,
( r1(X0,sK610(X0))
| ~ p209(sK611(X0))
| ~ sP59(X0) ) ).
cnf(u1311,axiom,
( ~ sP300(X0)
| ~ p902(X0)
| ~ p1002(X0) ) ).
cnf(u3083,negated_conjecture,
sP51(sK731) ).
cnf(u2192,axiom,
( r1(X0,sK574(X0))
| ~ p110(sK575(X0))
| ~ sP77(X0) ) ).
cnf(u3170,negated_conjecture,
sP290(sK731) ).
cnf(u1668,axiom,
( ~ sP300(X0)
| sP84(X0) ) ).
cnf(u2354,axiom,
( ~ p108(sK657(X0))
| ~ p308(sK656(X0))
| ~ sP36(X0) ) ).
cnf(u3098,negated_conjecture,
sP253(sK731) ).
cnf(u2003,axiom,
( r1(X0,sK480(X0))
| ~ p1105(X0)
| ~ sP150(X0) ) ).
cnf(u2474,axiom,
( ~ p105(sK717(X0))
| ~ p405(sK716(X0))
| ~ sP6(X0) ) ).
cnf(u2249,axiom,
( r1(X0,sK603(X0))
| r1(X0,sK602(X0))
| ~ sP63(X0) ) ).
cnf(u1284,axiom,
( ~ sP300(X0)
| ~ p202(X0)
| ~ p1002(X0) ) ).
cnf(u2162,axiom,
( ~ p310(sK561(X0))
| ~ p410(sK560(X0))
| ~ sP84(X0) ) ).
cnf(u2461,axiom,
( r1(X0,sK709(X0))
| r1(X0,sK708(X0))
| ~ sP10(X0) ) ).
cnf(u1647,axiom,
( ~ sP300(X0)
| ~ p909(X0)
| ~ p1109(X0) ) ).
cnf(u1535,axiom,
( ~ sP300(X0)
| ~ p807(X0)
| ~ p1107(X0) ) ).
cnf(u2090,axiom,
( ~ p102(sK524(X0))
| ~ p1002(X0)
| ~ sP106(X0) ) ).
cnf(u2377,axiom,
( r1(X0,sK667(X0))
| r1(X0,sK666(X0))
| ~ sP31(X0) ) ).
cnf(u3043,negated_conjecture,
sP219(sK731) ).
cnf(u1466,axiom,
( ~ sP300(X0)
| sP17(X0) ) ).
cnf(u2324,axiom,
( r1(X0,sK640(X0))
| ~ p308(sK641(X0))
| ~ sP44(X0) ) ).
cnf(u1966,axiom,
( ~ p405(sK462(X0))
| ~ p1105(X0)
| ~ sP168(X0) ) ).
cnf(u2305,axiom,
( r1(X0,sK631(X0))
| r1(X0,sK630(X0))
| ~ sP49(X0) ) ).
cnf(u2147,axiom,
( r1(X0,sK553(X0))
| ~ p910(sK552(X0))
| ~ sP88(X0) ) ).
cnf(u1669,axiom,
( ~ sP300(X0)
| sP85(X0) ) ).
cnf(u1582,axiom,
( ~ sP300(X0)
| sP246(X0) ) ).
cnf(u2075,axiom,
( r1(X0,sK516(X0))
| ~ p1003(X0)
| ~ sP114(X0) ) ).
cnf(u3006,negated_conjecture,
sP197(sK731) ).
cnf(u1236,axiom,
( ~ sP300(X0)
| ~ p201(X0)
| ~ p601(X0) ) ).
cnf(u2223,axiom,
( r1(X0,sK591(X0))
| ~ p809(sK590(X0))
| ~ sP69(X0) ) ).
cnf(u1797,axiom,
( r1(X0,sK369(X0))
| ~ p909(X0)
| ~ sP253(X0) ) ).
cnf(u3066,negated_conjecture,
sP233(sK731) ).
cnf(u1830,axiom,
( ~ p408(sK390(X0))
| ~ p1008(X0)
| ~ sP236(X0) ) ).
cnf(u1518,axiom,
( ~ sP300(X0)
| sP32(X0) ) ).
cnf(u2276,axiom,
( r1(X0,sK616(X0))
| ~ p209(sK617(X0))
| ~ sP56(X0) ) ).
cnf(u2366,axiom,
( ~ p407(sK663(X0))
| ~ p607(sK662(X0))
| ~ sP33(X0) ) ).
cnf(u1502,axiom,
( ~ sP300(X0)
| sP197(X0) ) ).
cnf(u2204,axiom,
( r1(X0,sK580(X0))
| ~ p110(sK581(X0))
| ~ sP74(X0) ) ).
cnf(u1660,axiom,
( ~ sP300(X0)
| sP79(X0) ) ).
cnf(u1930,axiom,
( ~ p406(sK444(X0))
| ~ p906(X0)
| ~ sP186(X0) ) ).
cnf(u2897,negated_conjecture,
sP112(sK731) ).
cnf(u1761,axiom,
( r1(X0,sK347(X0))
| ~ p1109(X0)
| ~ sP271(X0) ) ).
cnf(u1349,axiom,
( ~ sP300(X0)
| ~ p603(X0)
| ~ p803(X0) ) ).
cnf(u2429,axiom,
( r1(X0,sK693(X0))
| r1(X0,sK692(X0))
| ~ sP18(X0) ) ).
cnf(u2486,axiom,
( ~ p204(sK723(X0))
| ~ p304(sK722(X0))
| ~ sP3(X0) ) ).
cnf(u1546,axiom,
( ~ sP300(X0)
| sP220(X0) ) ).
cnf(u2189,axiom,
( r1(X0,sK573(X0))
| r1(X0,sK572(X0))
| ~ sP78(X0) ) ).
cnf(u1889,axiom,
( r1(X0,sK423(X0))
| ~ p907(X0)
| ~ sP207(X0) ) ).
cnf(u2921,negated_conjecture,
sP133(sK731) ).
cnf(u2389,axiom,
( r1(X0,sK673(X0))
| r1(X0,sK672(X0))
| ~ sP28(X0) ) ).
cnf(u1484,axiom,
( ~ sP300(X0)
| ~ p606(X0)
| ~ p806(X0) ) ).
cnf(u1624,axiom,
( ~ sP300(X0)
| sP67(X0) ) ).
cnf(u1852,axiom,
( ~ p208(sK403(X0))
| ~ p908(X0)
| ~ sP225(X0) ) ).
cnf(u1975,axiom,
( r1(X0,sK466(X0))
| ~ p605(X0)
| ~ sP164(X0) ) ).
cnf(u1547,axiom,
( ~ sP300(X0)
| sP221(X0) ) ).
cnf(u1435,axiom,
( ~ sP300(X0)
| ~ p505(X0)
| ~ p805(X0) ) ).
cnf(u2950,negated_conjecture,
sP9(sK731) ).
cnf(u1382,axiom,
( ~ sP300(X0)
| sP144(X0) ) ).
cnf(u1782,axiom,
( r1(X0,sK360(X0))
| ~ p409(sK361(X0))
| ~ sP260(X0) ) ).
cnf(u1839,axiom,
( r1(X0,sK395(X0))
| ~ p1108(X0)
| ~ sP232(X0) ) ).
cnf(u1676,axiom,
( ~ sP300(X0)
| sP89(X0) ) ).
cnf(u1527,axiom,
( ~ sP300(X0)
| sP212(X0) ) ).
cnf(u2909,negated_conjecture,
sP1(sK731) ).
cnf(u1341,axiom,
( ~ sP300(X0)
| ~ p403(X0)
| ~ p903(X0) ) ).
cnf(u2011,axiom,
( r1(X0,sK484(X0))
| ~ p605(X0)
| ~ sP146(X0) ) ).
cnf(u2499,axiom,
( r1(X0,sK729(X0))
| ~ p203(sK728(X0))
| ~ sP0(X0) ) ).
cnf(u1655,axiom,
( ~ sP300(X0)
| sP76(X0) ) ).
cnf(u2924,negated_conjecture,
sP136(sK731) ).
cnf(u1415,axiom,
( ~ sP300(X0)
| sP151(X0) ) ).
cnf(u2919,negated_conjecture,
sP131(sK731) ).
cnf(u1346,axiom,
( ~ sP300(X0)
| ~ p503(X0)
| ~ p903(X0) ) ).
cnf(u1746,axiom,
( ~ p110(sK338(X0))
| ~ p1110(X0)
| ~ sP278(X0) ) ).
cnf(u1974,axiom,
( ~ p405(sK466(X0))
| ~ p605(X0)
| ~ sP164(X0) ) ).
cnf(u1677,axiom,
( ~ sP300(X0)
| sP90(X0) ) ).
cnf(u3141,negated_conjecture,
sP78(sK731) ).
cnf(u3144,negated_conjecture,
sP81(sK731) ).
cnf(u1305,axiom,
( ~ sP300(X0)
| ~ p602(X0)
| ~ p902(X0) ) ).
cnf(u1991,axiom,
( r1(X0,sK474(X0))
| ~ p1105(X0)
| ~ sP156(X0) ) ).
cnf(u1924,axiom,
( ~ p506(sK441(X0))
| ~ p606(X0)
| ~ sP189(X0) ) ).
cnf(u2136,axiom,
( r1(X0,sK546(X0))
| ~ p410(sK547(X0))
| ~ sP91(X0) ) ).
cnf(u2219,axiom,
( r1(X0,sK589(X0))
| ~ p809(sK588(X0))
| ~ sP70(X0) ) ).
cnf(u2064,axiom,
( ~ p203(sK511(X0))
| ~ p603(X0)
| ~ sP119(X0) ) ).
cnf(u2487,axiom,
( r1(X0,sK723(X0))
| ~ p304(sK722(X0))
| ~ sP3(X0) ) ).
cnf(u1440,axiom,
( ~ sP300(X0)
| ~ p605(X0)
| ~ p905(X0) ) ).
cnf(u2418,axiom,
( ~ p107(sK689(X0))
| ~ p207(sK688(X0))
| ~ sP20(X0) ) ).
cnf(u2964,negated_conjecture,
sP11(sK731) ).
cnf(u2415,axiom,
( r1(X0,sK687(X0))
| ~ p307(sK686(X0))
| ~ sP21(X0) ) ).
cnf(u2328,axiom,
( r1(X0,sK642(X0))
| ~ p208(sK643(X0))
| ~ sP43(X0) ) ).
cnf(u1875,axiom,
( r1(X0,sK416(X0))
| ~ p807(X0)
| ~ sP214(X0) ) ).
cnf(u1769,axiom,
( r1(X0,sK352(X0))
| ~ p1109(X0)
| ~ sP267(X0) ) ).
cnf(u2121,axiom,
( r1(X0,sK539(X0))
| r1(X0,sK538(X0))
| ~ sP95(X0) ) ).
cnf(u1939,axiom,
( r1(X0,sK448(X0))
| ~ p1006(X0)
| ~ sP182(X0) ) ).
cnf(u3024,negated_conjecture,
sP206(sK731) ).
cnf(u2049,axiom,
( r1(X0,sK503(X0))
| ~ p804(X0)
| ~ sP127(X0) ) ).
cnf(u1407,axiom,
( ~ sP300(X0)
| sP145(X0) ) ).
cnf(u2915,negated_conjecture,
sP128(sK731) ).
cnf(u1338,axiom,
( ~ sP300(X0)
| ~ p403(X0)
| ~ p503(X0) ) ).
cnf(u3063,negated_conjecture,
sP232(sK731) ).
cnf(u1838,axiom,
( ~ p308(sK395(X0))
| ~ p1108(X0)
| ~ sP232(X0) ) ).
cnf(u3103,negated_conjecture,
sP63(sK731) ).
cnf(u2238,axiom,
( ~ p409(sK599(X0))
| ~ p509(sK598(X0))
| ~ sP65(X0) ) ).
cnf(u1492,axiom,
( ~ sP300(X0)
| ~ p906(X0)
| ~ p1106(X0) ) ).
cnf(u2991,negated_conjecture,
sP187(sK731) ).
cnf(u2242,axiom,
( ~ p309(sK601(X0))
| ~ p809(sK600(X0))
| ~ sP64(X0) ) ).
cnf(u1541,axiom,
( ~ sP300(X0)
| sP37(X0) ) ).
cnf(u1632,axiom,
( ~ sP300(X0)
| sP266(X0) ) ).
cnf(u2298,axiom,
( ~ p109(sK629(X0))
| ~ p209(sK628(X0))
| ~ sP50(X0) ) ).
cnf(u2095,axiom,
( r1(X0,sK526(X0))
| ~ p802(X0)
| ~ sP104(X0) ) ).
cnf(u3150,negated_conjecture,
sP84(sK731) ).
cnf(u1983,axiom,
( r1(X0,sK470(X0))
| ~ p905(X0)
| ~ sP160(X0) ) ).
cnf(u2513,negated_conjecture,
( ~ r1(sK730,X1)
| sP300(X1) ) ).
cnf(u1443,axiom,
( ~ sP300(X0)
| ~ p805(X0)
| ~ p905(X0) ) ).
cnf(u2938,negated_conjecture,
sP147(sK731) ).
cnf(u2460,axiom,
( r1(X0,sK708(X0))
| ~ p106(sK709(X0))
| ~ sP10(X0) ) ).
cnf(u1869,axiom,
( r1(X0,sK413(X0))
| ~ p1107(X0)
| ~ sP217(X0) ) ).
cnf(u1390,axiom,
( ~ sP300(X0)
| ~ p504(X0)
| ~ p804(X0) ) ).
cnf(u2148,axiom,
( r1(X0,sK552(X0))
| ~ p310(sK553(X0))
| ~ sP88(X0) ) ).
cnf(u1790,axiom,
( r1(X0,sK365(X0))
| ~ p309(sK366(X0))
| ~ sP256(X0) ) ).
cnf(u2283,axiom,
( r1(X0,sK621(X0))
| ~ p609(sK620(X0))
| ~ sP54(X0) ) ).
cnf(u1505,axiom,
( ~ sP300(X0)
| sP27(X0) ) ).
cnf(u2076,axiom,
( ~ p103(sK517(X0))
| ~ p903(X0)
| ~ sP113(X0) ) ).
cnf(u2072,axiom,
( ~ p103(sK515(X0))
| ~ p1103(X0)
| ~ sP115(X0) ) ).
cnf(u2005,axiom,
( r1(X0,sK481(X0))
| ~ p1005(X0)
| ~ sP149(X0) ) ).
cnf(u2430,axiom,
( ~ p306(sK695(X0))
| ~ p406(sK694(X0))
| ~ sP17(X0) ) ).
cnf(u1823,axiom,
( r1(X0,sK385(X0))
| ~ p908(X0)
| ~ sP240(X0) ) ).
cnf(u1633,axiom,
( ~ sP300(X0)
| sP267(X0) ) ).
cnf(u2133,axiom,
( r1(X0,sK545(X0))
| r1(X0,sK544(X0))
| ~ sP92(X0) ) ).
cnf(u3116,negated_conjecture,
sP68(sK731) ).
cnf(u3036,negated_conjecture,
sP217(sK731) ).
cnf(u2061,axiom,
( r1(X0,sK509(X0))
| ~ p903(X0)
| ~ sP121(X0) ) ).
cnf(u2193,axiom,
( r1(X0,sK575(X0))
| r1(X0,sK574(X0))
| ~ sP77(X0) ) ).
cnf(u3173,negated_conjecture,
sP97(sK731) ).
cnf(u1356,axiom,
( ~ sP300(X0)
| ~ p903(X0)
| ~ p1003(X0) ) ).
cnf(u1754,axiom,
( ~ p809(sK343(X0))
| ~ p1009(X0)
| ~ sP274(X0) ) ).
cnf(u3101,negated_conjecture,
sP61(sK731) ).
cnf(u2987,negated_conjecture,
sP19(sK731) ).
cnf(u2311,axiom,
( r1(X0,sK635(X0))
| ~ p508(sK634(X0))
| ~ sP47(X0) ) ).
cnf(u2182,axiom,
( ~ p210(sK571(X0))
| ~ p410(sK570(X0))
| ~ sP79(X0) ) ).
cnf(u1847,axiom,
( r1(X0,sK400(X0))
| r1(X0,sK399(X0))
| ~ sP228(X0) ) ).
cnf(u1307,axiom,
( ~ sP300(X0)
| ~ p602(X0)
| ~ p1102(X0) ) ).
cnf(u1654,axiom,
( ~ sP300(X0)
| sP276(X0) ) ).
cnf(u1932,axiom,
( ~ p406(sK445(X0))
| ~ p806(X0)
| ~ sP185(X0) ) ).
cnf(u1755,axiom,
( r1(X0,sK343(X0))
| ~ p1009(X0)
| ~ sP274(X0) ) ).
cnf(u1448,axiom,
( ~ sP300(X0)
| ~ p1005(X0)
| ~ p1105(X0) ) ).
cnf(u1533,axiom,
( ~ sP300(X0)
| ~ p807(X0)
| ~ p907(X0) ) ).
cnf(u2333,axiom,
( r1(X0,sK645(X0))
| r1(X0,sK644(X0))
| ~ sP42(X0) ) ).
cnf(u1775,axiom,
( r1(X0,sK356(X0))
| r1(X0,sK355(X0))
| ~ sP264(X0) ) ).
cnf(u1883,axiom,
( r1(X0,sK420(X0))
| ~ p807(X0)
| ~ sP210(X0) ) ).
cnf(u2443,axiom,
( r1(X0,sK701(X0))
| ~ p306(sK700(X0))
| ~ sP14(X0) ) ).
cnf(u2002,axiom,
( ~ p105(sK480(X0))
| ~ p1105(X0)
| ~ sP150(X0) ) ).
cnf(u1287,axiom,
( ~ sP300(X0)
| ~ p302(X0)
| ~ p502(X0) ) ).
cnf(u2069,axiom,
( r1(X0,sK513(X0))
| ~ p403(X0)
| ~ sP117(X0) ) ).
cnf(u1421,axiom,
( ~ sP300(X0)
| sP9(X0) ) ).
cnf(u2409,axiom,
( r1(X0,sK683(X0))
| r1(X0,sK682(X0))
| ~ sP23(X0) ) ).
cnf(u1618,axiom,
( ~ sP300(X0)
| sP257(X0) ) ).
cnf(u2024,axiom,
( ~ p304(sK491(X0))
| ~ p504(X0)
| ~ sP139(X0) ) ).
cnf(u1961,axiom,
( r1(X0,sK459(X0))
| ~ p906(X0)
| ~ sP171(X0) ) ).
cnf(u1549,axiom,
( ~ sP300(X0)
| sP40(X0) ) ).
cnf(u2314,axiom,
( ~ p308(sK637(X0))
| ~ p608(sK636(X0))
| ~ sP46(X0) ) ).
cnf(u2277,axiom,
( r1(X0,sK617(X0))
| r1(X0,sK616(X0))
| ~ sP56(X0) ) ).
cnf(u2392,axiom,
( r1(X0,sK674(X0))
| ~ p207(sK675(X0))
| ~ sP27(X0) ) ).
cnf(u2320,axiom,
( r1(X0,sK638(X0))
| ~ p308(sK639(X0))
| ~ sP45(X0) ) ).
cnf(u2231,axiom,
( r1(X0,sK595(X0))
| ~ p809(sK594(X0))
| ~ sP67(X0) ) ).
cnf(u1796,axiom,
( ~ p209(sK369(X0))
| ~ p909(X0)
| ~ sP253(X0) ) ).
cnf(u2946,negated_conjecture,
sP153(sK731) ).
cnf(u3129,negated_conjecture,
sP274(sK731) ).
cnf(u1619,axiom,
( ~ sP300(X0)
| sP258(X0) ) ).
cnf(u1513,axiom,
( ~ sP300(X0)
| sP31(X0) ) ).
cnf(u1312,axiom,
( ~ sP300(X0)
| ~ p902(X0)
| ~ p1102(X0) ) ).
cnf(u2013,axiom,
( r1(X0,sK485(X0))
| ~ p505(X0)
| ~ sP145(X0) ) ).
cnf(u2968,negated_conjecture,
sP170(sK731) ).
cnf(u1641,axiom,
( r1(X0,sK304(X0))
| ~ p1009(X0)
| ~ sP300(X0) ) ).
cnf(u2905,negated_conjecture,
sP120(sK731) ).
cnf(u2272,axiom,
( r1(X0,sK614(X0))
| ~ p209(sK615(X0))
| ~ sP57(X0) ) ).
cnf(u1748,axiom,
( ~ p110(sK339(X0))
| ~ p1010(X0)
| ~ sP277(X0) ) ).
cnf(u2498,axiom,
( ~ p103(sK729(X0))
| ~ p203(sK728(X0))
| ~ sP0(X0) ) ).
cnf(u2362,axiom,
( ~ p507(sK661(X0))
| ~ p607(sK660(X0))
| ~ sP34(X0) ) ).
cnf(u3178,negated_conjecture,
sP98(sK731) ).
cnf(u1888,axiom,
( ~ p407(sK423(X0))
| ~ p907(X0)
| ~ sP207(X0) ) ).
cnf(u3001,negated_conjecture,
sP23(sK731) ).
cnf(u2110,axiom,
( ~ p610(sK535(X0))
| ~ p910(sK534(X0))
| ~ sP97(X0) ) ).
cnf(u1364,axiom,
( ~ sP300(X0)
| sP127(X0) ) ).
cnf(u2114,axiom,
( ~ p610(sK537(X0))
| ~ p810(sK536(X0))
| ~ sP96(X0) ) ).
cnf(u1727,axiom,
( r1(X0,sK325(X0))
| r1(X0,sK324(X0))
| ~ sP288(X0) ) ).
cnf(u2170,axiom,
( ~ p210(sK565(X0))
| ~ p810(sK564(X0))
| ~ sP82(X0) ) ).
cnf(u1418,axiom,
( ~ sP300(X0)
| sP154(X0) ) ).
cnf(u2404,axiom,
( r1(X0,sK680(X0))
| ~ p107(sK681(X0))
| ~ sP24(X0) ) ).
cnf(u1855,axiom,
( r1(X0,sK404(X0))
| ~ p808(X0)
| ~ sP224(X0) ) ).
cnf(u2046,axiom,
( ~ p104(sK502(X0))
| ~ p904(X0)
| ~ sP128(X0) ) ).
cnf(u1315,axiom,
( ~ sP300(X0)
| sP108(X0) ) ).
cnf(u2227,axiom,
( r1(X0,sK593(X0))
| ~ p609(sK592(X0))
| ~ sP68(X0) ) ).
cnf(u1749,axiom,
( r1(X0,sK339(X0))
| ~ p1010(X0)
| ~ sP277(X0) ) ).
cnf(u3131,negated_conjecture,
sP71(sK731) ).
cnf(u1662,axiom,
( ~ sP300(X0)
| sP81(X0) ) ).
cnf(u2155,axiom,
( r1(X0,sK557(X0))
| ~ p610(sK556(X0))
| ~ sP86(X0) ) ).
cnf(u2958,negated_conjecture,
sP164(sK731) ).
cnf(u1377,axiom,
( ~ sP300(X0)
| sP139(X0) ) ).
cnf(u2355,axiom,
( r1(X0,sK657(X0))
| ~ p308(sK656(X0))
| ~ sP36(X0) ) ).
cnf(u1877,axiom,
( r1(X0,sK417(X0))
| ~ p1107(X0)
| ~ sP213(X0) ) ).
cnf(u1763,axiom,
( r1(X0,sK348(X0))
| ~ p1009(X0)
| ~ sP270(X0) ) ).
cnf(u3139,negated_conjecture,
sP277(sK731) ).
cnf(u3018,negated_conjecture,
sP202(sK731) ).
cnf(u2917,negated_conjecture,
sP130(sK731) ).
cnf(u2284,axiom,
( r1(X0,sK620(X0))
| ~ p109(sK621(X0))
| ~ sP54(X0) ) ).
cnf(u2010,axiom,
( ~ p105(sK484(X0))
| ~ p605(X0)
| ~ sP146(X0) ) ).
cnf(u2977,negated_conjecture,
sP176(sK731) ).
cnf(u1429,axiom,
( ~ sP300(X0)
| sP164(X0) ) ).
cnf(u2438,axiom,
( ~ p206(sK699(X0))
| ~ p406(sK698(X0))
| ~ sP15(X0) ) ).
cnf(u1626,axiom,
( ~ sP300(X0)
| sP262(X0) ) ).
cnf(u1969,axiom,
( r1(X0,sK463(X0))
| ~ p1005(X0)
| ~ sP167(X0) ) ).
cnf(u2054,axiom,
( ~ p104(sK506(X0))
| ~ p404(X0)
| ~ sP124(X0) ) ).
cnf(u2469,axiom,
( r1(X0,sK713(X0))
| r1(X0,sK712(X0))
| ~ sP8(X0) ) ).
cnf(u3079,negated_conjecture,
sP245(sK731) ).
cnf(u2397,axiom,
( r1(X0,sK677(X0))
| r1(X0,sK676(X0))
| ~ sP26(X0) ) ).
cnf(u3094,negated_conjecture,
sP58(sK731) ).
cnf(u1704,axiom,
( ~ p910(sK310(X0))
| ~ p1110(X0)
| ~ sP299(X0) ) ).
cnf(u1804,axiom,
( ~ p109(sK374(X0))
| ~ p909(X0)
| ~ sP249(X0) ) ).
cnf(u1291,axiom,
( ~ sP300(X0)
| ~ p302(X0)
| ~ p1002(X0) ) ).
cnf(u2318,axiom,
( ~ p308(sK639(X0))
| ~ p508(sK638(X0))
| ~ sP45(X0) ) ).
cnf(u1927,axiom,
( r1(X0,sK442(X0))
| ~ p1106(X0)
| ~ sP188(X0) ) ).
cnf(u1627,axiom,
( ~ sP300(X0)
| sP263(X0) ) ).
cnf(u1515,axiom,
( ~ sP300(X0)
| sP203(X0) ) ).
cnf(u3030,negated_conjecture,
sP211(sK731) ).
cnf(u1462,axiom,
( ~ sP300(X0)
| sP175(X0) ) ).
cnf(u1734,axiom,
( ~ p310(sK330(X0))
| ~ p1110(X0)
| ~ sP284(X0) ) ).
cnf(u1499,axiom,
( ~ sP300(X0)
| sP194(X0) ) ).
cnf(u3092,negated_conjecture,
sP56(sK731) ).
cnf(u1874,axiom,
( ~ p607(sK416(X0))
| ~ p807(X0)
| ~ sP214(X0) ) ).
cnf(u1756,axiom,
( ~ p809(sK344(X0))
| ~ p909(X0)
| ~ sP273(X0) ) ).
cnf(u2989,negated_conjecture,
sP185(sK731) ).
cnf(u1293,axiom,
( ~ sP300(X0)
| ~ p402(X0)
| ~ p502(X0) ) ).
cnf(u1272,axiom,
( ~ sP300(X0)
| sP102(X0) ) ).
cnf(u1833,axiom,
( r1(X0,sK391(X0))
| ~ p908(X0)
| ~ sP235(X0) ) ).
cnf(u1607,axiom,
( ~ sP300(X0)
| sP59(X0) ) ).
cnf(u3111,negated_conjecture,
sP260(sK731) ).
cnf(u1495,axiom,
( ~ sP300(X0)
| sP21(X0) ) ).
cnf(u2999,negated_conjecture,
sP21(sK731) ).
cnf(u1426,axiom,
( ~ sP300(X0)
| sP161(X0) ) ).
cnf(u1926,axiom,
( ~ p406(sK442(X0))
| ~ p1106(X0)
| ~ sP188(X0) ) ).
cnf(u1257,axiom,
( ~ sP300(X0)
| ~ p501(X0)
| ~ p1001(X0) ) ).
cnf(u1757,axiom,
( r1(X0,sK344(X0))
| ~ p909(X0)
| ~ sP273(X0) ) ).
cnf(u1385,axiom,
( ~ sP300(X0)
| ~ p404(X0)
| ~ p804(X0) ) ).
cnf(u3152,negated_conjecture,
sP86(sK731) ).
cnf(u2485,axiom,
( r1(X0,sK721(X0))
| r1(X0,sK720(X0))
| ~ sP4(X0) ) ).
cnf(u2084,axiom,
( ~ p103(sK521(X0))
| ~ p403(X0)
| ~ sP109(X0) ) ).
cnf(u2004,axiom,
( ~ p105(sK481(X0))
| ~ p1005(X0)
| ~ sP149(X0) ) ).
cnf(u2885,negated_conjecture,
sP101(sK731) ).
cnf(u1816,axiom,
( r1(X0,sK381(X0))
| ~ p608(sK382(X0))
| ~ sP243(X0) ) ).
cnf(u2144,axiom,
( r1(X0,sK550(X0))
| ~ p410(sK551(X0))
| ~ sP89(X0) ) ).
cnf(u2439,axiom,
( r1(X0,sK699(X0))
| ~ p406(sK698(X0))
| ~ sP15(X0) ) ).
cnf(u2379,axiom,
( r1(X0,sK669(X0))
| ~ p507(sK668(X0))
| ~ sP30(X0) ) ).
cnf(u3122,negated_conjecture,
sP268(sK731) ).
cnf(u1620,axiom,
( ~ sP300(X0)
| sP259(X0) ) ).
cnf(u3124,negated_conjecture,
sP269(sK731) ).
cnf(u2370,axiom,
( ~ p407(sK665(X0))
| ~ p507(sK664(X0))
| ~ sP32(X0) ) ).
cnf(u3044,negated_conjecture,
sP220(sK731) ).
cnf(u2495,axiom,
( r1(X0,sK727(X0))
| ~ p204(sK726(X0))
| ~ sP1(X0) ) ).
cnf(u1955,axiom,
( r1(X0,sK456(X0))
| ~ p606(X0)
| ~ sP174(X0) ) ).
cnf(u2426,axiom,
( ~ p306(sK693(X0))
| ~ p506(sK692(X0))
| ~ sP18(X0) ) ).
cnf(u2201,axiom,
( r1(X0,sK579(X0))
| r1(X0,sK578(X0))
| ~ sP75(X0) ) ).
cnf(u1278,axiom,
( ~ sP300(X0)
| ~ p202(X0)
| ~ p302(X0) ) ).
cnf(u1359,axiom,
( ~ sP300(X0)
| sP1(X0) ) ).
cnf(u2293,axiom,
( r1(X0,sK625(X0))
| r1(X0,sK624(X0))
| ~ sP52(X0) ) ).
cnf(u2995,negated_conjecture,
sP191(sK731) ).
cnf(u1290,axiom,
( ~ sP300(X0)
| ~ p302(X0)
| ~ p902(X0) ) ).
cnf(u3015,negated_conjecture,
sP29(sK731) ).
cnf(u1918,axiom,
( ~ p506(sK438(X0))
| ~ p1006(X0)
| ~ sP192(X0) ) ).
cnf(u2190,axiom,
( ~ p110(sK575(X0))
| ~ p910(sK574(X0))
| ~ sP77(X0) ) ).
cnf(u3071,negated_conjecture,
sP49(sK731) ).
cnf(u2099,axiom,
( r1(X0,sK528(X0))
| ~ p502(X0)
| ~ sP102(X0) ) ).
cnf(u1621,axiom,
( ~ sP300(X0)
| sP65(X0) ) ).
cnf(u1712,axiom,
( r1(X0,sK315(X0))
| ~ p910(sK314(X0))
| ~ sP295(X0) ) ).
cnf(u2250,axiom,
( ~ p309(sK605(X0))
| ~ p509(sK604(X0))
| ~ sP62(X0) ) ).
cnf(u2175,axiom,
( r1(X0,sK567(X0))
| ~ p610(sK566(X0))
| ~ sP81(X0) ) ).
cnf(u1935,axiom,
( r1(X0,sK446(X0))
| ~ p606(X0)
| ~ sP184(X0) ) ).
cnf(u1523,axiom,
( ~ sP300(X0)
| sP209(X0) ) ).
cnf(u2890,negated_conjecture,
sP106(sK731) ).
cnf(u1242,axiom,
( ~ sP300(X0)
| ~ p301(X0)
| ~ p501(X0) ) ).
cnf(u1470,axiom,
( ~ sP300(X0)
| sP181(X0) ) ).
cnf(u2228,axiom,
( r1(X0,sK592(X0))
| ~ p509(sK593(X0))
| ~ sP68(X0) ) ).
cnf(u1742,axiom,
( ~ p210(sK335(X0))
| ~ p1010(X0)
| ~ sP280(X0) ) ).
cnf(u1248,axiom,
( ~ sP300(X0)
| ~ p401(X0)
| ~ p501(X0) ) ).
cnf(u2156,axiom,
( r1(X0,sK556(X0))
| ~ p310(sK557(X0))
| ~ sP86(X0) ) ).
cnf(u2435,axiom,
( r1(X0,sK697(X0))
| ~ p506(sK696(X0))
| ~ sP16(X0) ) ).
cnf(u1882,axiom,
( ~ p507(sK420(X0))
| ~ p807(X0)
| ~ sP210(X0) ) ).
cnf(u2382,axiom,
( ~ p307(sK671(X0))
| ~ p407(sK670(X0))
| ~ sP29(X0) ) ).
cnf(u1591,axiom,
( ~ sP300(X0)
| ~ p908(X0)
| ~ p1008(X0) ) ).
cnf(u1713,axiom,
( r1(X0,sK315(X0))
| r1(X0,sK314(X0))
| ~ sP295(X0) ) ).
cnf(u1301,axiom,
( ~ sP300(X0)
| ~ p502(X0)
| ~ p902(X0) ) ).
cnf(u2310,axiom,
( ~ p408(sK635(X0))
| ~ p508(sK634(X0))
| ~ sP47(X0) ) ).
cnf(u2213,axiom,
( r1(X0,sK585(X0))
| r1(X0,sK584(X0))
| ~ sP72(X0) ) ).
cnf(u3120,negated_conjecture,
sP266(sK731) ).
cnf(u2141,axiom,
( r1(X0,sK549(X0))
| r1(X0,sK548(X0))
| ~ sP90(X0) ) ).
cnf(u1841,axiom,
( r1(X0,sK396(X0))
| ~ p1008(X0)
| ~ sP231(X0) ) ).
cnf(u2273,axiom,
( r1(X0,sK615(X0))
| r1(X0,sK614(X0))
| ~ sP57(X0) ) ).
cnf(u1561,axiom,
( ~ sP300(X0)
| sP228(X0) ) ).
cnf(u2341,axiom,
( r1(X0,sK649(X0))
| r1(X0,sK648(X0))
| ~ sP40(X0) ) ).
cnf(u1960,axiom,
( ~ p106(sK459(X0))
| ~ p906(X0)
| ~ sP171(X0) ) ).
cnf(u1436,axiom,
( ~ sP300(X0)
| ~ p505(X0)
| ~ p905(X0) ) ).
cnf(u2470,axiom,
( ~ p205(sK715(X0))
| ~ p305(sK714(X0))
| ~ sP7(X0) ) ).
cnf(u3181,negated_conjecture,
sP298(sK731) ).
cnf(u3067,negated_conjecture,
sP234(sK731) ).
cnf(u1265,axiom,
( ~ sP300(X0)
| ~ p801(X0)
| ~ p1101(X0) ) ).
cnf(u1576,axiom,
( ~ sP300(X0)
| sP240(X0) ) ).
cnf(u2262,axiom,
( ~ p209(sK611(X0))
| ~ p609(sK610(X0))
| ~ sP59(X0) ) ).
cnf(u1799,axiom,
( r1(X0,sK371(X0))
| r1(X0,sK370(X0))
| ~ sP252(X0) ) ).
cnf(u1387,axiom,
( ~ sP300(X0)
| ~ p404(X0)
| ~ p1004(X0) ) ).
cnf(u2902,negated_conjecture,
sP117(sK731) ).
cnf(u1334,axiom,
( ~ sP300(X0)
| ~ p303(X0)
| ~ p803(X0) ) ).
cnf(u1824,axiom,
( ~ p508(sK386(X0))
| ~ p808(X0)
| ~ sP239(X0) ) ).
cnf(u2012,axiom,
( ~ p105(sK485(X0))
| ~ p505(X0)
| ~ sP145(X0) ) ).
cnf(u2500,axiom,
( r1(X0,sK728(X0))
| ~ p103(sK729(X0))
| ~ sP0(X0) ) ).
cnf(u1528,axiom,
( ~ sP300(X0)
| sP213(X0) ) ).
cnf(u1577,axiom,
( ~ sP300(X0)
| sP241(X0) ) ).
cnf(u1239,axiom,
( ~ sP300(X0)
| ~ p201(X0)
| ~ p1001(X0) ) ).
cnf(u1963,axiom,
( r1(X0,sK460(X0))
| ~ p806(X0)
| ~ sP170(X0) ) ).
cnf(u1367,axiom,
( ~ sP300(X0)
| sP130(X0) ) ).
cnf(u1501,axiom,
( ~ sP300(X0)
| sP196(X0) ) ).
cnf(u1698,axiom,
( ~ sP300(X0)
| sP98(X0) ) ).
cnf(u2041,axiom,
( r1(X0,sK499(X0))
| ~ p404(X0)
| ~ sP131(X0) ) ).
cnf(u1629,axiom,
( ~ sP300(X0)
| sP264(X0) ) ).
cnf(u1813,axiom,
( r1(X0,sK379(X0))
| ~ p908(X0)
| ~ sP245(X0) ) ).
cnf(u3096,negated_conjecture,
sP252(sK731) ).
cnf(u2433,axiom,
( r1(X0,sK695(X0))
| r1(X0,sK694(X0))
| ~ sP17(X0) ) ).
cnf(u2472,axiom,
( r1(X0,sK714(X0))
| ~ p205(sK715(X0))
| ~ sP7(X0) ) ).
cnf(u1568,axiom,
( ~ sP300(X0)
| sP233(X0) ) ).
cnf(u2400,axiom,
( r1(X0,sK678(X0))
| ~ p207(sK679(X0))
| ~ sP25(X0) ) ).
cnf(u2183,axiom,
( r1(X0,sK571(X0))
| ~ p410(sK570(X0))
| ~ sP79(X0) ) ).
cnf(u2263,axiom,
( r1(X0,sK611(X0))
| ~ p609(sK610(X0))
| ~ sP59(X0) ) ).
cnf(u1876,axiom,
( ~ p507(sK417(X0))
| ~ p1107(X0)
| ~ sP213(X0) ) ).
cnf(u1250,axiom,
( ~ sP300(X0)
| ~ p401(X0)
| ~ p801(X0) ) ).
cnf(u3026,negated_conjecture,
sP208(sK731) ).
cnf(u3081,negated_conjecture,
sP247(sK731) ).
cnf(u1699,axiom,
( ~ sP300(X0)
| sP296(X0) ) ).
cnf(u1392,axiom,
( ~ sP300(X0)
| ~ p504(X0)
| ~ p1004(X0) ) ).
cnf(u1776,axiom,
( ~ p409(sK357(X0))
| ~ p1109(X0)
| ~ sP263(X0) ) ).
cnf(u2916,negated_conjecture,
sP129(sK731) ).
cnf(u2367,axiom,
( r1(X0,sK663(X0))
| ~ p607(sK662(X0))
| ~ sP33(X0) ) ).
cnf(u3048,negated_conjecture,
sP41(sK731) ).
cnf(u1827,axiom,
( r1(X0,sK388(X0))
| r1(X0,sK387(X0))
| ~ sP238(X0) ) ).
cnf(u1721,axiom,
( r1(X0,sK321(X0))
| r1(X0,sK320(X0))
| ~ sP291(X0) ) ).
cnf(u2073,axiom,
( r1(X0,sK515(X0))
| ~ p1103(X0)
| ~ sP115(X0) ) ).
cnf(u2985,negated_conjecture,
sP182(sK731) ).
cnf(u1968,axiom,
( ~ p405(sK463(X0))
| ~ p1005(X0)
| ~ sP167(X0) ) ).
cnf(u2062,axiom,
( ~ p203(sK510(X0))
| ~ p803(X0)
| ~ sP120(X0) ) ).
cnf(u1444,axiom,
( ~ sP300(X0)
| ~ p805(X0)
| ~ p1005(X0) ) ).
cnf(u2943,negated_conjecture,
sP8(sK731) ).
cnf(u2194,axiom,
( ~ p110(sK577(X0))
| ~ p810(sK576(X0))
| ~ sP76(X0) ) ).
cnf(u1679,axiom,
( ~ sP300(X0)
| sP91(X0) ) ).
cnf(u1267,axiom,
( ~ sP300(X0)
| ~ p901(X0)
| ~ p1101(X0) ) ).
cnf(u2122,axiom,
( ~ p510(sK541(X0))
| ~ p810(sK540(X0))
| ~ sP94(X0) ) ).
cnf(u3008,negated_conjecture,
sP26(sK731) ).
cnf(u1498,axiom,
( ~ sP300(X0)
| sP24(X0) ) ).
cnf(u3102,negated_conjecture,
sP62(sK731) ).
cnf(u2484,axiom,
( r1(X0,sK720(X0))
| ~ p105(sK721(X0))
| ~ sP4(X0) ) ).
cnf(u1998,axiom,
( ~ p205(sK478(X0))
| ~ p605(X0)
| ~ sP152(X0) ) ).
cnf(u1395,axiom,
( ~ sP300(X0)
| ~ p604(X0)
| ~ p904(X0) ) ).
cnf(u2412,axiom,
( r1(X0,sK684(X0))
| ~ p107(sK685(X0))
| ~ sP22(X0) ) ).
cnf(u2179,axiom,
( r1(X0,sK569(X0))
| ~ p510(sK568(X0))
| ~ sP80(X0) ) ).
cnf(u1262,axiom,
( ~ sP300(X0)
| ~ p601(X0)
| ~ p1101(X0) ) ).
cnf(u1342,axiom,
( ~ sP300(X0)
| ~ p403(X0)
| ~ p1003(X0) ) ).
cnf(u1614,axiom,
( ~ sP300(X0)
| sP62(X0) ) ).
cnf(u2235,axiom,
( r1(X0,sK597(X0))
| ~ p609(sK596(X0))
| ~ sP66(X0) ) ).
cnf(u3038,negated_conjecture,
sP36(sK731) ).
cnf(u1457,axiom,
( ~ sP300(X0)
| sP173(X0) ) ).
cnf(u2255,axiom,
( r1(X0,sK607(X0))
| ~ p409(sK606(X0))
| ~ sP61(X0) ) ).
cnf(u2307,axiom,
( r1(X0,sK633(X0))
| ~ p608(sK632(X0))
| ~ sP48(X0) ) ).
cnf(u1957,axiom,
( r1(X0,sK457(X0))
| ~ p1106(X0)
| ~ sP173(X0) ) ).
cnf(u1408,axiom,
( ~ sP300(X0)
| sP146(X0) ) ).
cnf(u2488,axiom,
( r1(X0,sK722(X0))
| ~ p204(sK723(X0))
| ~ sP3(X0) ) ).
cnf(u2363,axiom,
( r1(X0,sK661(X0))
| ~ p607(sK660(X0))
| ~ sP34(X0) ) ).
cnf(u1585,axiom,
( r1(X0,sK308(X0))
| ~ p908(X0)
| ~ sP300(X0) ) ).
cnf(u3147,negated_conjecture,
sP83(sK731) ).
cnf(u2953,negated_conjecture,
sP159(sK731) ).
cnf(u1247,axiom,
( ~ sP300(X0)
| ~ p301(X0)
| ~ p1101(X0) ) ).
cnf(u2988,negated_conjecture,
sP184(sK731) ).
cnf(u2145,axiom,
( r1(X0,sK551(X0))
| r1(X0,sK550(X0))
| ~ sP89(X0) ) ).
cnf(u3057,negated_conjecture,
sP45(sK731) ).
cnf(u1832,axiom,
( ~ p408(sK391(X0))
| ~ p908(X0)
| ~ sP235(X0) ) ).
cnf(u1509,axiom,
( ~ sP300(X0)
| sP200(X0) ) ).
cnf(u1308,axiom,
( ~ sP300(X0)
| ~ p802(X0)
| ~ p902(X0) ) ).
cnf(u1706,axiom,
( ~ p910(sK311(X0))
| ~ p1010(X0)
| ~ sP298(X0) ) ).
cnf(u2939,negated_conjecture,
sP148(sK731) ).
cnf(u1921,axiom,
( r1(X0,sK439(X0))
| ~ p906(X0)
| ~ sP191(X0) ) ).
cnf(u2134,axiom,
( ~ p410(sK547(X0))
| ~ p810(sK546(X0))
| ~ sP91(X0) ) ).
cnf(u1854,axiom,
( ~ p208(sK404(X0))
| ~ p808(X0)
| ~ sP224(X0) ) ).
cnf(u3174,negated_conjecture,
sP292(sK731) ).
cnf(u1784,axiom,
( ~ p309(sK362(X0))
| ~ p1109(X0)
| ~ sP259(X0) ) ).
cnf(u1884,axiom,
( ~ p407(sK421(X0))
| ~ p1107(X0)
| ~ sP209(X0) ) ).
cnf(u1260,axiom,
( ~ sP300(X0)
| ~ p601(X0)
| ~ p901(X0) ) ).
cnf(u1226,axiom,
( ~ sP300(X0)
| ~ p101(X0)
| ~ p401(X0) ) ).
cnf(u2007,axiom,
( r1(X0,sK482(X0))
| ~ p905(X0)
| ~ sP148(X0) ) ).
cnf(u1707,axiom,
( r1(X0,sK311(X0))
| ~ p1010(X0)
| ~ sP298(X0) ) ).
cnf(u1400,axiom,
( ~ sP300(X0)
| ~ p804(X0)
| ~ p1104(X0) ) ).
cnf(u1414,axiom,
( ~ sP300(X0)
| sP8(X0) ) ).
cnf(u1835,axiom,
( r1(X0,sK392(X0))
| ~ p808(X0)
| ~ sP234(X0) ) ).
cnf(u1232,axiom,
( ~ sP300(X0)
| ~ p101(X0)
| ~ p1101(X0) ) ).
cnf(u1245,axiom,
( ~ sP300(X0)
| ~ p301(X0)
| ~ p901(X0) ) ).
cnf(u1954,axiom,
( ~ p206(sK456(X0))
| ~ p606(X0)
| ~ sP174(X0) ) ).
cnf(u2269,axiom,
( r1(X0,sK613(X0))
| r1(X0,sK612(X0))
| ~ sP58(X0) ) ).
cnf(u3069,negated_conjecture,
sP236(sK731) ).
cnf(u1373,axiom,
( ~ sP300(X0)
| sP135(X0) ) ).
cnf(u1570,axiom,
( ~ sP300(X0)
| sP235(X0) ) ).
cnf(u2217,axiom,
( r1(X0,sK587(X0))
| r1(X0,sK586(X0))
| ~ sP71(X0) ) ).
cnf(u1224,axiom,
( ~ sP300(X0)
| ~ p101(X0)
| ~ p201(X0) ) ).
cnf(u1913,axiom,
( r1(X0,sK435(X0))
| ~ p907(X0)
| ~ sP195(X0) ) ).
cnf(u1687,axiom,
( ~ sP300(X0)
| sP289(X0) ) ).
cnf(u1275,axiom,
( ~ sP300(X0)
| sP105(X0) ) ).
cnf(u1506,axiom,
( ~ sP300(X0)
| sP28(X0) ) ).
cnf(u3115,negated_conjecture,
sP263(sK731) ).
cnf(u2006,axiom,
( ~ p105(sK482(X0))
| ~ p905(X0)
| ~ sP148(X0) ) ).
cnf(u2055,axiom,
( r1(X0,sK506(X0))
| ~ p404(X0)
| ~ sP124(X0) ) ).
cnf(u1818,axiom,
( ~ p508(sK383(X0))
| ~ p1108(X0)
| ~ sP242(X0) ) ).
cnf(u2898,negated_conjecture,
sP113(sK731) ).
cnf(u2206,axiom,
( ~ p110(sK583(X0))
| ~ p410(sK582(X0))
| ~ sP73(X0) ) ).
cnf(u1571,axiom,
( ~ sP300(X0)
| sP236(X0) ) ).
cnf(u1465,axiom,
( ~ sP300(X0)
| sP178(X0) ) ).
cnf(u1965,axiom,
( r1(X0,sK461(X0))
| ~ p606(X0)
| ~ sP169(X0) ) ).
cnf(u2278,axiom,
( ~ p109(sK619(X0))
| ~ p809(sK618(X0))
| ~ sP55(X0) ) ).
cnf(u2296,axiom,
( r1(X0,sK626(X0))
| ~ p109(sK627(X0))
| ~ sP51(X0) ) ).
cnf(u2224,axiom,
( r1(X0,sK590(X0))
| ~ p509(sK591(X0))
| ~ sP69(X0) ) ).
cnf(u3074,negated_conjecture,
sP240(sK731) ).
cnf(u1700,axiom,
( ~ sP300(X0)
| sP297(X0) ) ).
cnf(u2450,axiom,
( ~ p106(sK705(X0))
| ~ p406(sK704(X0))
| ~ sP12(X0) ) ).
cnf(u2447,axiom,
( r1(X0,sK703(X0))
| ~ p506(sK702(X0))
| ~ sP13(X0) ) ).
cnf(u3130,negated_conjecture,
sP275(sK731) ).
cnf(u2035,axiom,
( r1(X0,sK496(X0))
| ~ p804(X0)
| ~ sP134(X0) ) ).
cnf(u2378,axiom,
( ~ p307(sK669(X0))
| ~ p507(sK668(X0))
| ~ sP30(X0) ) ).
cnf(u2281,axiom,
( r1(X0,sK619(X0))
| r1(X0,sK618(X0))
| ~ sP55(X0) ) ).
cnf(u1316,axiom,
( ~ sP300(X0)
| sP109(X0) ) ).
cnf(u2066,axiom,
( ~ p203(sK512(X0))
| ~ p503(X0)
| ~ sP118(X0) ) ).
cnf(u1230,axiom,
( ~ sP300(X0)
| ~ p101(X0)
| ~ p901(X0) ) ).
cnf(u2395,axiom,
( r1(X0,sK677(X0))
| ~ p407(sK676(X0))
| ~ sP26(X0) ) ).
cnf(u1439,axiom,
( ~ sP300(X0)
| ~ p605(X0)
| ~ p805(X0) ) ).
cnf(u2947,negated_conjecture,
sP154(sK731) ).
cnf(u1370,axiom,
( ~ sP300(X0)
| sP132(X0) ) ).
cnf(u2327,axiom,
( r1(X0,sK643(X0))
| ~ p608(sK642(X0))
| ~ sP43(X0) ) ).
cnf(u1870,axiom,
( ~ p607(sK414(X0))
| ~ p1007(X0)
| ~ sP216(X0) ) ).
cnf(u2337,axiom,
( r1(X0,sK647(X0))
| r1(X0,sK646(X0))
| ~ sP41(X0) ) ).
cnf(u2270,axiom,
( ~ p209(sK615(X0))
| ~ p409(sK614(X0))
| ~ sP57(X0) ) ).
cnf(u3023,negated_conjecture,
sP33(sK731) ).
cnf(u2051,axiom,
( r1(X0,sK504(X0))
| ~ p604(X0)
| ~ sP126(X0) ) ).
cnf(u1701,axiom,
( ~ sP300(X0)
| sP298(X0) ) ).
cnf(u1664,axiom,
( ~ sP300(X0)
| sP82(X0) ) ).
cnf(u2107,axiom,
( r1(X0,sK533(X0))
| ~ p910(sK532(X0))
| ~ sP98(X0) ) ).
cnf(u2910,negated_conjecture,
sP2(sK731) ).
cnf(u1268,axiom,
( ~ sP300(X0)
| ~ p1001(X0)
| ~ p1101(X0) ) ).
cnf(u2127,axiom,
( r1(X0,sK543(X0))
| ~ p610(sK542(X0))
| ~ sP93(X0) ) ).
cnf(u1770,axiom,
( ~ p509(sK353(X0))
| ~ p1009(X0)
| ~ sP266(X0) ) ).
cnf(u2015,axiom,
( r1(X0,sK486(X0))
| ~ p1104(X0)
| ~ sP144(X0) ) ).
cnf(u3091,negated_conjecture,
sP251(sK731) ).
cnf(u1475,axiom,
( ~ sP300(X0)
| sP185(X0) ) ).
cnf(u2970,negated_conjecture,
sP172(sK731) ).
cnf(u1422,axiom,
( ~ sP300(X0)
| sP157(X0) ) ).
cnf(u2180,axiom,
( r1(X0,sK568(X0))
| ~ p210(sK569(X0))
| ~ sP80(X0) ) ).
cnf(u1253,axiom,
( ~ sP300(X0)
| ~ p401(X0)
| ~ p1101(X0) ) ).
cnf(u2236,axiom,
( r1(X0,sK596(X0))
| ~ p409(sK597(X0))
| ~ sP66(X0) ) ).
cnf(u1564,axiom,
( ~ sP300(X0)
| sP231(X0) ) ).
cnf(u1962,axiom,
( ~ p106(sK460(X0))
| ~ p806(X0)
| ~ sP170(X0) ) ).
cnf(u2462,axiom,
( ~ p305(sK711(X0))
| ~ p405(sK710(X0))
| ~ sP9(X0) ) ).
cnf(u2929,negated_conjecture,
sP141(sK731) ).
cnf(u1665,axiom,
( ~ sP300(X0)
| sP83(X0) ) ).
cnf(u1381,axiom,
( ~ sP300(X0)
| sP143(X0) ) ).
cnf(u2390,axiom,
( ~ p207(sK675(X0))
| ~ p507(sK674(X0))
| ~ sP27(X0) ) ).
cnf(u1578,axiom,
( ~ sP300(X0)
| sP242(X0) ) ).
cnf(u3148,negated_conjecture,
sP280(sK731) ).
cnf(u2221,axiom,
( r1(X0,sK589(X0))
| r1(X0,sK588(X0))
| ~ sP70(X0) ) ).
cnf(u1793,axiom,
( r1(X0,sK367(X0))
| ~ p1109(X0)
| ~ sP255(X0) ) ).
cnf(u2421,axiom,
( r1(X0,sK689(X0))
| r1(X0,sK688(X0))
| ~ sP20(X0) ) ).
cnf(u1516,axiom,
( ~ sP300(X0)
| sP204(X0) ) ).
cnf(u3019,negated_conjecture,
sP203(sK731) ).
cnf(u1656,axiom,
( ~ sP300(X0)
| sP77(X0) ) ).
cnf(u1879,axiom,
( r1(X0,sK418(X0))
| ~ p1007(X0)
| ~ sP212(X0) ) ).
cnf(u1579,axiom,
( ~ sP300(X0)
| sP243(X0) ) ).
cnf(u2245,axiom,
( r1(X0,sK601(X0))
| r1(X0,sK600(X0))
| ~ sP64(X0) ) ).
cnf(u1467,axiom,
( ~ sP300(X0)
| sP18(X0) ) ).
cnf(u2982,negated_conjecture,
sP179(sK731) ).
cnf(u1286,axiom,
( ~ sP300(X0)
| ~ p302(X0)
| ~ p402(X0) ) ).
cnf(u1686,axiom,
( ~ sP300(X0)
| sP95(X0) ) ).
cnf(u3072,negated_conjecture,
sP238(sK731) ).
cnf(u1826,axiom,
( r1(X0,sK387(X0))
| ~ p508(sK388(X0))
| ~ sP238(X0) ) ).
cnf(u1480,axiom,
( ~ sP300(X0)
| sP190(X0) ) ).
cnf(u1708,axiom,
( ~ p810(sK312(X0))
| ~ p1110(X0)
| ~ sP297(X0) ) ).
cnf(u1751,axiom,
( r1(X0,sK341(X0))
| r1(X0,sK340(X0))
| ~ sP276(X0) ) ).
cnf(u2941,negated_conjecture,
sP150(sK731) ).
cnf(u1540,axiom,
( ~ sP300(X0)
| sP36(X0) ) ).
cnf(u2043,axiom,
( r1(X0,sK500(X0))
| ~ p1104(X0)
| ~ sP130(X0) ) ).
cnf(u1238,axiom,
( ~ sP300(X0)
| ~ p201(X0)
| ~ p901(X0) ) ).
cnf(u1447,axiom,
( ~ sP300(X0)
| ~ p905(X0)
| ~ p1105(X0) ) ).
cnf(u1378,axiom,
( ~ sP300(X0)
| sP140(X0) ) ).
cnf(u1778,axiom,
( ~ p409(sK358(X0))
| ~ p1009(X0)
| ~ sP262(X0) ) ).
cnf(u1878,axiom,
( ~ p507(sK418(X0))
| ~ p1007(X0)
| ~ sP212(X0) ) ).
cnf(u1709,axiom,
( r1(X0,sK312(X0))
| ~ p1110(X0)
| ~ sP297(X0) ) ).
cnf(u3176,negated_conjecture,
sP294(sK731) ).
cnf(u3104,negated_conjecture,
sP256(sK731) ).
cnf(u1956,axiom,
( ~ p106(sK457(X0))
| ~ p1106(X0)
| ~ sP173(X0) ) ).
cnf(u2168,axiom,
( r1(X0,sK562(X0))
| ~ p210(sK563(X0))
| ~ sP83(X0) ) ).
cnf(u2459,axiom,
( r1(X0,sK709(X0))
| ~ p206(sK708(X0))
| ~ sP10(X0) ) ).
cnf(u3161,negated_conjecture,
sP91(sK731) ).
cnf(u1779,axiom,
( r1(X0,sK358(X0))
| ~ p1009(X0)
| ~ sP262(X0) ) ).
cnf(u2391,axiom,
( r1(X0,sK675(X0))
| ~ p507(sK674(X0))
| ~ sP27(X0) ) ).
cnf(u3033,negated_conjecture,
sP214(sK731) ).
cnf(u1344,axiom,
( ~ sP300(X0)
| ~ p503(X0)
| ~ p603(X0) ) ).
cnf(u1572,axiom,
( ~ sP300(X0)
| sP237(X0) ) ).
cnf(u3089,negated_conjecture,
sP249(sK731) ).
cnf(u2996,negated_conjecture,
sP192(sK731) ).
cnf(u2319,axiom,
( r1(X0,sK639(X0))
| ~ p508(sK638(X0))
| ~ sP45(X0) ) ).
cnf(u1907,axiom,
( r1(X0,sK432(X0))
| ~ p807(X0)
| ~ sP198(X0) ) ).
cnf(u1673,axiom,
( ~ sP300(X0)
| sP88(X0) ) ).
cnf(u2153,axiom,
( r1(X0,sK555(X0))
| r1(X0,sK554(X0))
| ~ sP87(X0) ) ).
cnf(u3056,negated_conjecture,
sP44(sK731) ).
cnf(u1300,axiom,
( ~ sP300(X0)
| ~ p502(X0)
| ~ p802(X0) ) ).
cnf(u2081,axiom,
( r1(X0,sK519(X0))
| ~ p603(X0)
| ~ sP111(X0) ) ).
cnf(u1901,axiom,
( r1(X0,sK429(X0))
| ~ p1107(X0)
| ~ sP201(X0) ) ).
cnf(u1920,axiom,
( ~ p506(sK439(X0))
| ~ p906(X0)
| ~ sP191(X0) ) ).
cnf(u3135,negated_conjecture,
sP75(sK731) ).
cnf(u2142,axiom,
( ~ p410(sK551(X0))
| ~ p510(sK550(X0))
| ~ sP89(X0) ) ).
cnf(u1524,axiom,
( ~ sP300(X0)
| sP34(X0) ) ).
cnf(u1313,axiom,
( ~ sP300(X0)
| ~ p1002(X0)
| ~ p1102(X0) ) ).
cnf(u2274,axiom,
( ~ p209(sK617(X0))
| ~ p309(sK616(X0))
| ~ sP56(X0) ) ).
cnf(u1573,axiom,
( ~ sP300(X0)
| sP49(X0) ) ).
cnf(u1536,axiom,
( ~ sP300(X0)
| ~ p907(X0)
| ~ p1007(X0) ) ).
cnf(u2202,axiom,
( ~ p110(sK581(X0))
| ~ p510(sK580(X0))
| ~ sP74(X0) ) ).
cnf(u3182,negated_conjecture,
sP299(sK731) ).
cnf(u2436,axiom,
( r1(X0,sK696(X0))
| ~ p206(sK697(X0))
| ~ sP16(X0) ) ).
cnf(u1887,axiom,
( r1(X0,sK422(X0))
| ~ p1007(X0)
| ~ sP208(X0) ) ).
cnf(u1347,axiom,
( ~ sP300(X0)
| ~ p503(X0)
| ~ p1003(X0) ) ).
cnf(u2492,axiom,
( r1(X0,sK724(X0))
| ~ p104(sK725(X0))
| ~ sP2(X0) ) ).
cnf(u2259,axiom,
( r1(X0,sK609(X0))
| ~ p809(sK608(X0))
| ~ sP60(X0) ) ).
cnf(u3045,negated_conjecture,
sP221(sK731) ).
cnf(u1294,axiom,
( ~ sP300(X0)
| ~ p402(X0)
| ~ p602(X0) ) ).
cnf(u1694,axiom,
( ~ sP300(X0)
| sP294(X0) ) ).
cnf(u2187,axiom,
( r1(X0,sK573(X0))
| ~ p310(sK572(X0))
| ~ sP78(X0) ) ).
cnf(u1409,axiom,
( ~ sP300(X0)
| sP147(X0) ) ).
cnf(u2108,axiom,
( r1(X0,sK532(X0))
| ~ p810(sK533(X0))
| ~ sP98(X0) ) ).
cnf(u2387,axiom,
( r1(X0,sK673(X0))
| ~ p607(sK672(X0))
| ~ sP28(X0) ) ).
cnf(u2037,axiom,
( r1(X0,sK497(X0))
| ~ p604(X0)
| ~ sP133(X0) ) ).
cnf(u1488,axiom,
( ~ sP300(X0)
| ~ p806(X0)
| ~ p906(X0) ) ).
cnf(u2315,axiom,
( r1(X0,sK637(X0))
| ~ p608(sK636(X0))
| ~ sP46(X0) ) ).
cnf(u1537,axiom,
( ~ sP300(X0)
| ~ p907(X0)
| ~ p1107(X0) ) ).
cnf(u2165,axiom,
( r1(X0,sK561(X0))
| r1(X0,sK560(X0))
| ~ sP84(X0) ) ).
cnf(u2949,negated_conjecture,
sP156(sK731) ).
cnf(u2093,axiom,
( r1(X0,sK525(X0))
| ~ p902(X0)
| ~ sP105(X0) ) ).
cnf(u2123,axiom,
( r1(X0,sK541(X0))
| ~ p810(sK540(X0))
| ~ sP94(X0) ) ).
cnf(u3009,negated_conjecture,
sP27(sK731) ).
cnf(u3077,negated_conjecture,
sP243(sK731) ).
cnf(u1388,axiom,
( ~ sP300(X0)
| ~ p404(X0)
| ~ p1104(X0) ) ).
cnf(u1786,axiom,
( ~ p309(sK363(X0))
| ~ p1009(X0)
| ~ sP258(X0) ) ).
cnf(u3133,negated_conjecture,
sP73(sK731) ).
cnf(u2891,negated_conjecture,
sP107(sK731) ).
cnf(u2001,axiom,
( r1(X0,sK479(X0))
| ~ p505(X0)
| ~ sP151(X0) ) ).
cnf(u2214,axiom,
( ~ p110(sK587(X0))
| ~ p210(sK586(X0))
| ~ sP71(X0) ) ).
cnf(u2501,axiom,
( r1(X0,sK729(X0))
| r1(X0,sK728(X0))
| ~ sP0(X0) ) ).
cnf(u1339,axiom,
( ~ sP300(X0)
| ~ p403(X0)
| ~ p603(X0) ) ).
cnf(u1558,axiom,
( ~ sP300(X0)
| sP44(X0) ) ).
cnf(u1964,axiom,
( ~ p106(sK461(X0))
| ~ p606(X0)
| ~ sP169(X0) ) ).
cnf(u2101,axiom,
( r1(X0,sK529(X0))
| ~ p402(X0)
| ~ sP101(X0) ) ).
cnf(u1787,axiom,
( r1(X0,sK363(X0))
| ~ p1009(X0)
| ~ sP258(X0) ) ).
cnf(u1352,axiom,
( ~ sP300(X0)
| ~ p603(X0)
| ~ p1103(X0) ) ).
cnf(u1494,axiom,
( ~ sP300(X0)
| sP20(X0) ) ).
cnf(u1915,axiom,
( r1(X0,sK436(X0))
| ~ p807(X0)
| ~ sP194(X0) ) ).
cnf(u2034,axiom,
( ~ p204(sK496(X0))
| ~ p804(X0)
| ~ sP134(X0) ) ).
cnf(u1319,axiom,
( ~ sP300(X0)
| sP112(X0) ) ).
cnf(u3021,negated_conjecture,
sP205(sK731) ).
cnf(u1453,axiom,
( ~ sP300(X0)
| sP169(X0) ) ).
cnf(u1806,axiom,
( r1(X0,sK375(X0))
| ~ p109(sK376(X0))
| ~ sP248(X0) ) ).
cnf(u1650,axiom,
( ~ sP300(X0)
| sP72(X0) ) ).
cnf(u1928,axiom,
( ~ p406(sK443(X0))
| ~ p1006(X0)
| ~ sP187(X0) ) ).
cnf(u2407,axiom,
( r1(X0,sK683(X0))
| ~ p507(sK682(X0))
| ~ sP23(X0) ) ).
cnf(u1865,axiom,
( r1(X0,sK410(X0))
| ~ p808(X0)
| ~ sP219(X0) ) ).
cnf(u1581,axiom,
( ~ sP300(X0)
| sP245(X0) ) ).
cnf(u3143,negated_conjecture,
sP80(sK731) ).
cnf(u1227,axiom,
( ~ sP300(X0)
| ~ p101(X0)
| ~ p501(X0) ) ).
cnf(u2424,axiom,
( r1(X0,sK690(X0))
| ~ p406(sK691(X0))
| ~ sP19(X0) ) ).
cnf(u2352,axiom,
( r1(X0,sK654(X0))
| ~ p108(sK655(X0))
| ~ sP37(X0) ) ).
cnf(u2135,axiom,
( r1(X0,sK547(X0))
| ~ p810(sK546(X0))
| ~ sP91(X0) ) ).
cnf(u1828,axiom,
( ~ p408(sK389(X0))
| ~ p1108(X0)
| ~ sP237(X0) ) ).
cnf(u2978,negated_conjecture,
sP177(sK731) ).
cnf(u1651,axiom,
( ~ sP300(X0)
| sP73(X0) ) ).
cnf(u1417,axiom,
( ~ sP300(X0)
| sP153(X0) ) ).
cnf(u2045,axiom,
( r1(X0,sK501(X0))
| ~ p1004(X0)
| ~ sP129(X0) ) ).
cnf(u3000,negated_conjecture,
sP22(sK731) ).
cnf(u1545,axiom,
( ~ sP300(X0)
| sP219(X0) ) ).
cnf(u2937,negated_conjecture,
sP146(sK731) ).
cnf(u2176,axiom,
( r1(X0,sK566(X0))
| ~ p210(sK567(X0))
| ~ sP81(X0) ) ).
cnf(u2287,axiom,
( r1(X0,sK623(X0))
| ~ p509(sK622(X0))
| ~ sP53(X0) ) ).
cnf(u3154,negated_conjecture,
sP87(sK731) ).
cnf(u3082,negated_conjecture,
sP50(sK731) ).
cnf(u1792,axiom,
( ~ p209(sK367(X0))
| ~ p1109(X0)
| ~ sP255(X0) ) ).
cnf(u2458,axiom,
( ~ p106(sK709(X0))
| ~ p206(sK708(X0))
| ~ sP10(X0) ) ).
cnf(u1396,axiom,
( ~ sP300(X0)
| ~ p604(X0)
| ~ p1004(X0) ) ).
cnf(u2146,axiom,
( ~ p310(sK553(X0))
| ~ p910(sK552(X0))
| ~ sP88(X0) ) ).
cnf(u1631,axiom,
( ~ sP300(X0)
| sP265(X0) ) ).
cnf(u1758,axiom,
( r1(X0,sK346(X0))
| ~ p809(sK345(X0))
| ~ sP272(X0) ) ).
cnf(u1519,axiom,
( ~ sP300(X0)
| sP33(X0) ) ).
cnf(u2074,axiom,
( ~ p103(sK516(X0))
| ~ p1003(X0)
| ~ sP114(X0) ) ).
cnf(u3027,negated_conjecture,
sP209(sK731) ).
cnf(u1450,axiom,
( ~ sP300(X0)
| sP11(X0) ) ).
cnf(u2308,axiom,
( r1(X0,sK632(X0))
| ~ p408(sK633(X0))
| ~ sP48(X0) ) ).
cnf(u1950,axiom,
( ~ p206(sK454(X0))
| ~ p906(X0)
| ~ sP176(X0) ) ).
cnf(u2417,axiom,
( r1(X0,sK687(X0))
| r1(X0,sK686(X0))
| ~ sP21(X0) ) ).
cnf(u1781,axiom,
( r1(X0,sK359(X0))
| ~ p909(X0)
| ~ sP261(X0) ) ).
cnf(u1566,axiom,
( ~ sP300(X0)
| sP47(X0) ) ).
cnf(u2990,negated_conjecture,
sP186(sK731) ).
cnf(u1281,axiom,
( ~ sP300(X0)
| ~ p202(X0)
| ~ p602(X0) ) ).
cnf(u2207,axiom,
( r1(X0,sK583(X0))
| ~ p410(sK582(X0))
| ~ sP73(X0) ) ).
cnf(u1909,axiom,
( r1(X0,sK433(X0))
| ~ p1107(X0)
| ~ sP197(X0) ) ).
cnf(u2181,axiom,
( r1(X0,sK569(X0))
| r1(X0,sK568(X0))
| ~ sP80(X0) ) ).
cnf(u3171,negated_conjecture,
sP291(sK731) ).
cnf(u3050,negated_conjecture,
sP43(sK731) ).
cnf(u3099,negated_conjecture,
sP254(sK731) ).
cnf(u2260,axiom,
( r1(X0,sK608(X0))
| ~ p209(sK609(X0))
| ~ sP60(X0) ) ).
cnf(u2940,negated_conjecture,
sP149(sK731) ).
cnf(u2188,axiom,
( r1(X0,sK572(X0))
| ~ p210(sK573(X0))
| ~ sP78(X0) ) ).
cnf(u1644,axiom,
( ~ sP300(X0)
| sP274(X0) ) ).
cnf(u2042,axiom,
( ~ p104(sK500(X0))
| ~ p1104(X0)
| ~ sP130(X0) ) ).
cnf(u1814,axiom,
( ~ p608(sK380(X0))
| ~ p808(X0)
| ~ sP244(X0) ) ).
cnf(u1745,axiom,
( r1(X0,sK337(X0))
| r1(X0,sK336(X0))
| ~ sP279(X0) ) ).
cnf(u1461,axiom,
( ~ sP300(X0)
| sP174(X0) ) ).
cnf(u3107,negated_conjecture,
sP258(sK731) ).
cnf(u1658,axiom,
( ~ sP300(X0)
| sP278(X0) ) ).
cnf(u1873,axiom,
( r1(X0,sK415(X0))
| ~ p907(X0)
| ~ sP215(X0) ) ).
cnf(u2086,axiom,
( ~ p103(sK522(X0))
| ~ p303(X0)
| ~ sP108(X0) ) ).
cnf(u2373,axiom,
( r1(X0,sK665(X0))
| r1(X0,sK664(X0))
| ~ sP32(X0) ) ).
cnf(u1434,axiom,
( ~ sP300(X0)
| ~ p505(X0)
| ~ p605(X0) ) ).
cnf(u3126,negated_conjecture,
sP271(sK731) ).
cnf(u1608,axiom,
( ~ sP300(X0)
| sP252(X0) ) ).
cnf(u1836,axiom,
( r1(X0,sK393(X0))
| ~ p408(sK394(X0))
| ~ sP233(X0) ) ).
cnf(u2896,negated_conjecture,
sP111(sK731) ).
cnf(u1659,axiom,
( ~ sP300(X0)
| sP78(X0) ) ).
cnf(u1419,axiom,
( ~ sP300(X0)
| sP155(X0) ) ).
cnf(u3062,negated_conjecture,
sP231(sK731) ).
cnf(u1366,axiom,
( ~ sP300(X0)
| sP129(X0) ) ).
cnf(u1766,axiom,
( r1(X0,sK350(X0))
| ~ p609(sK351(X0))
| ~ sP268(X0) ) ).
cnf(u1906,axiom,
( ~ p207(sK432(X0))
| ~ p807(X0)
| ~ sP198(X0) ) ).
cnf(u1788,axiom,
( ~ p309(sK364(X0))
| ~ p909(X0)
| ~ sP257(X0) ) ).
cnf(u2893,negated_conjecture,
sP108(sK731) ).
cnf(u1325,axiom,
( ~ sP300(X0)
| sP118(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL649+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n014.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 16:15:01 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.93/2.49 % (982810)Detected formulas, will run a generic FOF schedule.
% 10.93/2.49 % (982821)dis-21_1_sil=8000:lcm=predicate:random_seed=1153806259:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.93/2.49 % (982821)Instruction limit reached!
% 10.93/2.49 % (982821)------------------------------
% 10.93/2.49 % (982821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982821)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982821)Termination reason: Instruction limit
% 10.93/2.49 % (982821)Termination phase: Saturation
% 10.93/2.49 % (982821)Time elapsed: 0.040 s
% 10.93/2.49 % (982821)Peak memory usage: 92 MB
% 10.93/2.49 % (982821)Instructions burned: 130 (million)
% 10.93/2.49 % (982815)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=348896356:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.93/2.49 % (982819)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2191450998:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.93/2.49 % (982816)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3750786573:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.93/2.49 % (982820)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1089508304:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.93/2.49 % (982818)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2217756041:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.93/2.49 % (982817)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1621808971:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.93/2.49 % (982819)Instruction limit reached!
% 10.93/2.49 % (982819)------------------------------
% 10.93/2.49 % (982819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982819)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982819)Termination reason: Instruction limit
% 10.93/2.49 % (982819)Termination phase: Saturation
% 10.93/2.49 % (982819)Time elapsed: 0.053 s
% 10.93/2.49 % (982819)Peak memory usage: 90 MB
% 10.93/2.49 % (982819)Instructions burned: 120 (million)
% 10.93/2.49 % (982818)Instruction limit reached!
% 10.93/2.49 % (982818)------------------------------
% 10.93/2.49 % (982818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982818)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982818)Termination reason: Instruction limit
% 10.93/2.49 % (982818)Termination phase: Saturation
% 10.93/2.49 % (982818)Time elapsed: 0.058 s
% 10.93/2.49 % (982818)Peak memory usage: 92 MB
% 10.93/2.49 % (982818)Instructions burned: 109 (million)
% 10.93/2.49 % (982820)Instruction limit reached!
% 10.93/2.49 % (982820)------------------------------
% 10.93/2.49 % (982820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982820)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982820)Termination reason: Instruction limit
% 10.93/2.49 % (982820)Termination phase: Saturation
% 10.93/2.49 % (982820)Time elapsed: 0.078 s
% 10.93/2.49 % (982820)Peak memory usage: 92 MB
% 10.93/2.49 % (982820)Instructions burned: 140 (million)
% 10.93/2.49 % (982829)lrs+10_1_sil=8000:sp=occurrence:random_seed=4265700492:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.93/2.49 % (982829)Instruction limit reached!
% 10.93/2.49 % (982829)------------------------------
% 10.93/2.49 % (982829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982829)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982829)Termination reason: Instruction limit
% 10.93/2.49 % (982829)Termination phase: Saturation
% 10.93/2.49 % (982829)Time elapsed: 0.076 s
% 10.93/2.49 % (982829)Peak memory usage: 97 MB
% 10.93/2.49 % (982829)Instructions burned: 286 (million)
% 10.93/2.49 % (982831)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3845493329:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 10.93/2.49 % (982830)lrs+10_1_sil=32000:urr=on:br=off:random_seed=777560856:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.93/2.49 % (982832)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1562562921:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 10.93/2.49 % (982830)Refutation not found, incomplete strategy
% 10.93/2.49 % (982830)------------------------------
% 10.93/2.49 % (982830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982830)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982830)Termination reason: Refutation not found, incomplete strategy
% 10.93/2.49 % (982830)Time elapsed: 0.053 s
% 10.93/2.49 % (982830)Peak memory usage: 92 MB
% 10.93/2.49 % (982830)Instructions burned: 98 (million)
% 10.93/2.49 % (982832)Refutation not found, incomplete strategy
% 10.93/2.49 % (982832)------------------------------
% 10.93/2.49 % (982832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982832)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982832)Termination reason: Refutation not found, incomplete strategy
% 10.93/2.49 % (982832)Time elapsed: 0.060 s
% 10.93/2.49 % (982832)Peak memory usage: 92 MB
% 10.93/2.49 % (982832)Instructions burned: 110 (million)
% 10.93/2.49 % (982834)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3245272971:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 10.93/2.49 % (982831)Refutation not found, incomplete strategy
% 10.93/2.49 % (982831)------------------------------
% 10.93/2.49 % (982831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982831)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982831)Termination reason: Refutation not found, incomplete strategy
% 10.93/2.49 % (982831)Time elapsed: 0.139 s
% 10.93/2.49 % (982831)Peak memory usage: 94 MB
% 10.93/2.49 % (982831)Instructions burned: 256 (million)
% 10.93/2.49 % (982834)Instruction limit reached!
% 10.93/2.49 % (982834)------------------------------
% 10.93/2.49 % (982834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982834)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982834)Termination reason: Instruction limit
% 10.93/2.49 % (982834)Termination phase: Saturation
% 10.93/2.49 % (982834)Time elapsed: 0.074 s
% 10.93/2.49 % (982834)Peak memory usage: 93 MB
% 10.93/2.49 % (982834)Instructions burned: 295 (million)
% 10.93/2.49 % (982830)------------------------------
% 10.93/2.49 % (982830)------------------------------
% 10.93/2.49 % (982839)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=150204939:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 10.93/2.49 % (982832)------------------------------
% 10.93/2.49 % (982832)------------------------------
% 10.93/2.49 % (982831)------------------------------
% 10.93/2.49 % (982831)------------------------------
% 10.93/2.49 % (982840)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3681384125:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 10.93/2.49 % (982842)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3473620817:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 10.93/2.49 % (982840)Instruction limit reached!
% 10.93/2.49 % (982840)------------------------------
% 10.93/2.49 % (982840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982840)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982840)Termination reason: Instruction limit
% 10.93/2.49 % (982840)Termination phase: Saturation
% 10.93/2.49 % (982840)Time elapsed: 0.062 s
% 10.93/2.49 % (982840)Peak memory usage: 92 MB
% 10.93/2.49 % (982840)Instructions burned: 114 (million)
% 10.93/2.49 % (982843)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1733085802:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 10.93/2.49 % (982842)Instruction limit reached!
% 10.93/2.49 % (982842)------------------------------
% 10.93/2.49 % (982842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982842)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982842)Termination reason: Instruction limit
% 10.93/2.49 % (982842)Termination phase: Saturation
% 10.93/2.49 % (982842)Time elapsed: 0.065 s
% 10.93/2.49 % (982842)Peak memory usage: 91 MB
% 10.93/2.49 % (982842)Instructions burned: 127 (million)
% 10.93/2.49 % (982843)Refutation not found, incomplete strategy
% 10.93/2.49 % (982843)------------------------------
% 10.93/2.49 % (982843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982843)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982843)Termination reason: Refutation not found, incomplete strategy
% 10.93/2.49 % (982843)Time elapsed: 0.054 s
% 10.93/2.49 % (982843)Peak memory usage: 91 MB
% 10.93/2.49 % (982843)Instructions burned: 99 (million)
% 10.93/2.49 % (982846)lrs+10_1_sil=8000:sp=occurrence:random_seed=2166363211:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 10.93/2.49 % (982848)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4196417398:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 10.93/2.49 % (982843)------------------------------
% 10.93/2.49 % (982843)------------------------------
% 10.93/2.49 % (982848)Instruction limit reached!
% 10.93/2.49 % (982848)------------------------------
% 10.93/2.49 % (982848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982848)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982848)Termination reason: Instruction limit
% 10.93/2.49 % (982848)Termination phase: Saturation
% 10.93/2.49 % (982848)Time elapsed: 0.185 s
% 10.93/2.49 % (982848)Peak memory usage: 101 MB
% 10.93/2.49 % (982848)Instructions burned: 438 (million)
% 10.93/2.49 % (982846)First to succeed.
% 10.93/2.49 % (982846)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-982810"
% 10.93/2.49 % (982851)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3925205383:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 10.93/2.49 % (982852)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1733421672:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 10.93/2.49 % (982852)Instruction limit reached!
% 10.93/2.49 % (982852)------------------------------
% 10.93/2.49 % (982852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982852)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982852)Termination reason: Instruction limit
% 10.93/2.49 % (982852)Termination phase: Saturation
% 10.93/2.49 % (982852)Time elapsed: 0.070 s
% 10.93/2.49 % (982852)Peak memory usage: 91 MB
% 10.93/2.49 % (982852)Instructions burned: 135 (million)
% 10.93/2.49 % (982839)Instruction limit reached!
% 10.93/2.49 % (982839)------------------------------
% 10.93/2.49 % (982839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.49 % (982839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.49 % (982839)CaDiCaL version: 2.1.3
% 10.93/2.49 % (982839)Termination reason: Instruction limit
% 10.93/2.49 % (982839)Termination phase: Saturation
% 10.93/2.49 % (982839)Time elapsed: 0.817 s
% 10.93/2.49 % (982839)Peak memory usage: 156 MB
% 10.93/2.49 % (982839)Instructions burned: 2350 (million)
% 10.93/2.49 % SZS status CounterSatisfiable for theBenchmark
% 10.93/2.49 % SZS output start Saturation.
% See solution above
% 11.98/2.69 % SZS output start Definitions and Model Updates.
% 11.98/2.69 for all inputs,
% 11.98/2.69 define p701(X0) := $false
% 11.98/2.69 for all inputs,
% 11.98/2.69 define p702(X0) := $false
% 11.98/2.69 for all inputs,
% 11.98/2.69 define p703(X0) := $false
% 11.98/2.69 for all inputs,
% 11.98/2.69 define p704(X0) := $false
% 11.98/2.69 for all inputs,
% 11.98/2.69 define p705(X0) := $false
% 11.98/2.69 for all inputs,
% 11.98/2.69 define p706(X0) := $false
% 11.98/2.69 for all inputs,
% 11.98/2.69 define p708(X0) := $false
% 11.98/2.69 for all inputs,
% 11.98/2.69 define p709(X0) := $false
% 11.98/2.69 for all inputs,
% 11.98/2.69 define p710(X0) := $false
% 11.98/2.69 for all inputs,
% 11.98/2.69 define p707(X0) := $true
% 11.98/2.69 % SZS output end Definitions and Model Updates.
% 11.98/2.69 % (982846)------------------------------
% 11.98/2.69 % (982846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.98/2.69 % (982846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.98/2.69 % (982846)CaDiCaL version: 2.1.3
% 11.98/2.69 % (982846)Termination reason: Satisfiable
% 11.98/2.69 % (982846)Time elapsed: 0.285 s
% 11.98/2.69 % (982846)Peak memory usage: 102 MB
% 11.98/2.69 % (982846)Instructions burned: 583 (million)
% 11.98/2.69 % (982846)------------------------------
% 11.98/2.69 % (982846)------------------------------
% 11.98/2.69 % (982810)Success in time 1.627 s
% 11.98/2.69 % Vampire exiting
%------------------------------------------------------------------------------