%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN720-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:01:19 PM UTC 2026
% Result : Satisfiable 6.08s 1.65s
% Output : Saturation 7.35s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u374,axiom,
( ~ s3(X0,X1)
| s5(X0)
| ~ k4(X0) ) ).
cnf(u381,axiom,
( s5(X0)
| ~ l4(X0) ) ).
cnf(u385,axiom,
k5(b) ).
cnf(u393,axiom,
p5(b,b,b) ).
cnf(u400,axiom,
( n5(X0,X0)
| ~ s1(X0)
| ~ p4(X1,X0,X0) ) ).
cnf(u404,axiom,
n4(b,e) ).
cnf(u408,axiom,
r3(d,b,c) ).
cnf(u413,axiom,
n5(b,e) ).
cnf(u417,axiom,
p4(c,d,c) ).
cnf(u422,axiom,
n5(d,d) ).
cnf(u426,axiom,
k5(d) ).
cnf(u433,axiom,
( n5(X0,X0)
| ~ p0(X0,X1) ) ).
cnf(u440,axiom,
( ~ k1(X0)
| l5(X0) ) ).
cnf(u444,axiom,
n1(b,b,b) ).
cnf(u448,axiom,
s4(e) ).
cnf(u456,axiom,
( ~ r3(X2,X0,X0)
| k5(X0) ) ).
cnf(u463,axiom,
( r4(X0)
| ~ p0(X3,X0)
| ~ n3(X0) ) ).
cnf(u468,axiom,
~ l1(b,c) ).
cnf(u472,axiom,
~ k3(c,e,b) ).
cnf(u476,axiom,
q4(b,b) ).
cnf(u483,axiom,
( q4(X0,X0)
| ~ r1(X0) ) ).
cnf(u487,axiom,
n3(a) ).
cnf(u491,axiom,
( ~ m3(X0,c,a)
| p4(c,c,X0) ) ).
cnf(u498,axiom,
( p4(X0,X0,X0)
| ~ n0(X0,X1)
| ~ l4(X0) ) ).
cnf(u502,axiom,
( ~ r3(X1,X1,X0)
| p4(X0,X1,X1) ) ).
cnf(u506,axiom,
( p4(X0,X0,X0)
| ~ n3(X0) ) ).
cnf(u513,axiom,
( n4(X0,X0)
| ~ m3(X0,X0,X0) ) ).
cnf(u518,axiom,
~ p3(b,e,a) ).
cnf(u521,axiom,
l3(b,a) ).
cnf(u530,axiom,
q1(d,d,d) ).
cnf(u534,axiom,
k3(c,c,e) ).
cnf(u539,axiom,
n4(d,d) ).
cnf(u547,axiom,
k4(e) ).
cnf(u551,axiom,
n3(e) ).
cnf(u555,axiom,
q3(e,b) ).
cnf(u559,axiom,
n0(c,d) ).
cnf(u564,axiom,
k4(c) ).
cnf(u568,axiom,
m2(b) ).
cnf(u575,axiom,
k2(a,a) ).
cnf(u580,axiom,
r3(a,a,e) ).
cnf(u585,axiom,
~ r2(d) ).
cnf(u598,axiom,
( q3(X0,X0)
| ~ r2(X0) ) ).
cnf(u606,axiom,
p3(e,b,e) ).
cnf(u610,axiom,
k2(c,b) ).
cnf(u615,axiom,
p3(b,c,b) ).
cnf(u622,axiom,
( p3(X0,X0,X0)
| ~ q0(X1,X0) ) ).
cnf(u627,axiom,
~ p2(d,b,c) ).
cnf(u630,axiom,
l3(b,e) ).
cnf(u638,axiom,
l2(a,b) ).
cnf(u643,axiom,
m3(b,b,b) ).
cnf(u647,axiom,
s2(c) ).
cnf(u651,axiom,
( ~ q2(X0,c,c)
| m3(X0,c,X0) ) ).
cnf(u655,axiom,
n2(e) ).
cnf(u659,axiom,
( ~ p2(X0,e,e)
| m3(X0,e,e) ) ).
cnf(u663,axiom,
q2(b,c,d) ).
cnf(u667,axiom,
m2(d) ).
cnf(u671,axiom,
l1(d,b) ).
cnf(u676,axiom,
m3(c,b,d) ).
cnf(u680,axiom,
q2(a,b,a) ).
cnf(u691,axiom,
( ~ r2(X0)
| m3(X0,X0,X0) ) ).
cnf(u695,axiom,
l2(a,a) ).
cnf(u699,axiom,
( m3(X0,X0,X0)
| ~ n0(X2,a)
| ~ m3(X0,X2,X0)
| ~ k2(X1,X2) ) ).
cnf(u703,axiom,
r0(b) ).
cnf(u707,axiom,
k3(a,c,a) ).
cnf(u711,axiom,
s2(d) ).
cnf(u716,axiom,
l3(d,c) ).
cnf(u720,axiom,
k2(b,c) ).
cnf(u725,axiom,
l3(c,c) ).
cnf(u729,axiom,
( ~ k3(X1,X0,X0)
| l3(X0,X0) ) ).
cnf(u733,axiom,
k2(a,d) ).
cnf(u738,axiom,
l3(d,d) ).
cnf(u745,axiom,
( ~ l1(X0,X0)
| l3(X0,X0) ) ).
cnf(u752,axiom,
( ~ l3(X2,X2)
| l3(X0,X0)
| ~ l1(X2,X0) ) ).
cnf(u756,axiom,
( l3(X0,X0)
| ~ n2(X0) ) ).
cnf(u760,axiom,
r2(c) ).
cnf(u765,axiom,
k3(c,c,c) ).
cnf(u772,axiom,
( k3(X0,X0,X0)
| ~ r1(X0) ) ).
cnf(u776,axiom,
r0(e) ).
cnf(u781,axiom,
~ r2(e) ).
cnf(u794,axiom,
( k3(X0,X0,X0)
| ~ s2(X0) ) ).
cnf(u798,axiom,
( k3(X0,X0,X0)
| ~ l1(b,X0) ) ).
cnf(u802,axiom,
r2(a) ).
cnf(u807,axiom,
k3(a,a,a) ).
cnf(u820,axiom,
k3(d,d,d) ).
cnf(u824,axiom,
( ~ p1(X1,X2,X0)
| ~ m2(X2)
| k3(X0,X0,X1) ) ).
cnf(u829,axiom,
~ k0(a) ).
cnf(u836,axiom,
( k3(X0,X0,X0)
| ~ k1(X0) ) ).
cnf(u840,axiom,
k2(c,e) ).
cnf(u844,axiom,
s2(e) ).
cnf(u852,axiom,
( k3(X0,X0,X0)
| ~ s1(X0) ) ).
cnf(u856,axiom,
s1(d) ).
cnf(u865,axiom,
s0(d) ).
cnf(u869,axiom,
s1(a) ).
cnf(u874,axiom,
s1(b) ).
cnf(u878,axiom,
( ~ q2(b,X0,b)
| s2(X0) ) ).
cnf(u885,axiom,
( q2(X0,X0,X0)
| ~ k1(X0) ) ).
cnf(u889,axiom,
l0(c) ).
cnf(u893,axiom,
( ~ l2(X1,X0)
| q2(X0,c,X1)
| ~ k1(X1) ) ).
cnf(u898,axiom,
~ q0(e,c) ).
cnf(u901,axiom,
s1(c) ).
cnf(u914,axiom,
k1(e) ).
cnf(u918,axiom,
( ~ n2(X0)
| p2(X0,X0,X0) ) ).
cnf(u925,axiom,
( p2(X0,X0,X0)
| ~ r0(X0) ) ).
cnf(u929,axiom,
p1(e,e,a) ).
cnf(u934,axiom,
p2(a,a,a) ).
cnf(u941,axiom,
( ~ p0(X0,X0)
| p2(X0,X0,X0) ) ).
cnf(u948,axiom,
( ~ p1(X0,X2,X0)
| p2(X0,X0,X0) ) ).
cnf(u952,axiom,
m1(d,a,c) ).
cnf(u961,axiom,
~ l1(e,c) ).
cnf(u972,axiom,
p2(X0,X0,X0) ).
cnf(u979,axiom,
( ~ k2(X0,c)
| p2(X0,X0,X0) ) ).
cnf(u987,axiom,
p2(b,c,c) ).
cnf(u991,axiom,
p1(d,b,e) ).
cnf(u996,axiom,
p2(d,b,b) ).
cnf(u1003,axiom,
( ~ p2(a,X2,X0)
| p2(X0,X0,X0) ) ).
cnf(u1008,axiom,
~ s0(e) ).
cnf(u1018,axiom,
( ~ p2(e,X0,X1)
| p2(X0,X1,X1) ) ).
cnf(u1022,axiom,
r1(a) ).
cnf(u1026,axiom,
( ~ m0(X1,X0,d)
| p2(X0,X0,d) ) ).
cnf(u1031,axiom,
p2(e,c,c) ).
cnf(u1035,axiom,
( ~ p1(X0,X1,e)
| p2(e,X0,X1) ) ).
cnf(u1039,axiom,
k2(c,a) ).
cnf(u1047,axiom,
p2(b,c,a) ).
cnf(u1051,axiom,
q1(e,e,e) ).
cnf(u1056,axiom,
~ l1(c,b) ).
cnf(u1060,axiom,
p2(c,e,e) ).
cnf(u1067,axiom,
( p2(X0,X0,X0)
| ~ k2(X0,a) ) ).
cnf(u1074,axiom,
r1(b) ).
cnf(u1079,axiom,
k0(b) ).
cnf(u1084,axiom,
n2(c) ).
cnf(u1092,axiom,
n1(e,a,e) ).
cnf(u1096,axiom,
k1(c) ).
cnf(u1100,axiom,
m1(b,a,e) ).
cnf(u1105,axiom,
n2(a) ).
cnf(u1109,axiom,
k1(b) ).
cnf(u1117,axiom,
( ~ s0(X0)
| m2(X0) ) ).
cnf(u1124,axiom,
( l2(X0,X0)
| ~ s1(X2)
| ~ m0(X3,X2,X0) ) ).
cnf(u1128,axiom,
l1(e,e) ).
cnf(u1133,axiom,
k2(e,e) ).
cnf(u1137,axiom,
( ~ q0(X0,X1)
| s1(X0) ) ).
cnf(u1141,axiom,
( ~ q1(d,X1,d)
| r1(X0)
| ~ q0(X0,X1) ) ).
cnf(u1146,axiom,
q1(b,b,b) ).
cnf(u1150,axiom,
s0(b) ).
cnf(u1154,axiom,
( ~ s0(X0)
| q1(X0,b,b) ) ).
cnf(u1158,axiom,
p0(b,d) ).
cnf(u1162,axiom,
( ~ n1(X1,d,X0)
| q1(X0,X0,X0) ) ).
cnf(u1166,axiom,
k0(e) ).
cnf(u1172,axiom,
~ l0(b) ).
cnf(u1179,axiom,
( ~ m1(X0,X1,X1)
| q1(X0,X0,X1) ) ).
cnf(u1183,axiom,
( ~ k1(X0)
| q1(X0,X0,X0) ) ).
cnf(u1188,axiom,
~ m1(c,d,a) ).
cnf(u1191,axiom,
m0(c,b,a) ).
cnf(u1200,axiom,
( ~ q0(X1,X0)
| ~ k1(X0)
| q1(X0,X0,X1) ) ).
cnf(u1204,axiom,
q0(b,b) ).
cnf(u1211,axiom,
( ~ p1(X0,b,b)
| q1(X0,X0,X0) ) ).
cnf(u1215,axiom,
( ~ p0(X3,X0)
| ~ q0(X1,X1)
| q1(X0,X1,X0)
| ~ l0(X0) ) ).
cnf(u1222,axiom,
( ~ k0(X0)
| q1(X0,X0,X0) ) ).
cnf(u1231,axiom,
( ~ n1(X1,X0,X4)
| ~ q0(X1,X2)
| p1(X0,X0,X0) ) ).
cnf(u1236,axiom,
p1(e,e,e) ).
cnf(u1241,axiom,
~ r0(d) ).
cnf(u1248,axiom,
l0(a) ).
cnf(u1253,axiom,
p1(a,a,a) ).
cnf(u1258,axiom,
p1(a,b,a) ).
cnf(u1265,axiom,
( ~ l1(X0,b)
| p1(X0,X0,X0) ) ).
cnf(u1269,axiom,
( ~ m1(X1,X2,X0)
| ~ q0(X2,X3)
| p1(X0,X0,X0) ) ).
cnf(u1273,axiom,
( ~ n1(X1,X3,X0)
| ~ n0(X1,X1)
| p1(X0,X0,X0) ) ).
cnf(u1277,axiom,
( ~ k1(X0)
| p1(X0,X0,X0) ) ).
cnf(u1286,axiom,
~ p0(d,b) ).
cnf(u1295,axiom,
~ m0(b,c,e) ).
cnf(u1303,axiom,
n0(e,b) ).
cnf(u1307,axiom,
( ~ k0(X0)
| p1(X0,X0,X0) ) ).
cnf(u1311,axiom,
( ~ s0(X0)
| p1(X0,X0,X0) ) ).
cnf(u1315,axiom,
( ~ p1(X1,X3,X0)
| p1(X0,X1,X0) ) ).
cnf(u1323,axiom,
( ~ l0(X0)
| p1(X0,X0,X0) ) ).
cnf(u1327,axiom,
m1(d,e,e) ).
cnf(u1331,axiom,
q0(b,e) ).
cnf(u1336,axiom,
n1(d,d,b) ).
cnf(u1340,axiom,
n1(e,e,e) ).
cnf(u1345,axiom,
~ p0(d,d) ).
cnf(u1349,axiom,
n1(d,e,e) ).
cnf(u1354,axiom,
~ p0(a,b) ).
cnf(u1364,axiom,
( ~ k1(X0)
| ~ s0(X0)
| n1(X0,X0,X0) ) ).
cnf(u1368,axiom,
( n1(X0,X1,X0)
| ~ p0(b,X1)
| ~ l0(X0) ) ).
cnf(u1373,axiom,
n1(c,c,c) ).
cnf(u1377,axiom,
q0(d,d) ).
cnf(u1382,axiom,
n1(d,d,d) ).
cnf(u1389,axiom,
( ~ k0(X0)
| n1(X0,X0,X0) ) ).
cnf(u1393,axiom,
( ~ m1(b,X0,e)
| n1(e,e,X0) ) ).
cnf(u1397,axiom,
k1(a) ).
cnf(u1401,axiom,
( ~ q0(X0,X0)
| m1(X0,X1,X1)
| ~ k1(X1) ) ).
cnf(u1406,axiom,
~ m0(a,e,c) ).
cnf(u1415,axiom,
m1(e,e,e) ).
cnf(u1420,axiom,
~ l1(a,b) ).
cnf(u1428,axiom,
m1(b,b,b) ).
cnf(u1432,axiom,
( ~ p0(X1,d)
| ~ l0(X1) ) ).
cnf(u1442,axiom,
( ~ m1(X1,c,X1)
| m1(X0,a,X1)
| ~ q0(X0,X1) ) ).
cnf(u1447,axiom,
m1(a,a,a) ).
cnf(u1452,axiom,
m1(c,c,c) ).
cnf(u1457,axiom,
~ r0(c) ).
cnf(u1464,axiom,
( ~ m0(X1,X1,X0)
| m1(X0,X1,X1) ) ).
cnf(u1469,axiom,
l1(c,c) ).
cnf(u1473,axiom,
( ~ p0(X1,X0)
| ~ n0(X1,X1)
| m1(X0,X0,c) ) ).
cnf(u1481,axiom,
( ~ k1(X0)
| l1(X0,X0) ) ).
cnf(u1485,axiom,
( ~ m0(X1,X0,X2)
| l1(X0,X1)
| ~ p0(X2,X0) ) ).
cnf(u2391,axiom,
~ r0(a) ).
cnf(u2742,axiom,
~ r2(b) ).
cnf(u2807,axiom,
~ n0(c,c) ).
cnf(u2811,axiom,
q3(c,c) ).
cnf(u2816,axiom,
~ n0(b,b) ).
cnf(u2820,axiom,
q3(b,b) ).
cnf(u2829,axiom,
q3(e,e) ).
cnf(u2835,axiom,
~ n0(a,a) ).
cnf(u2839,axiom,
q3(a,a) ).
cnf(u2845,axiom,
~ n0(e,c) ).
cnf(u2855,axiom,
~ n0(d,d) ).
cnf(u2859,axiom,
q3(d,d) ).
cnf(u2898,axiom,
~ q3(e,c) ).
cnf(u2948,axiom,
k3(e,e,c) ).
cnf(u2952,axiom,
~ m2(c) ).
cnf(u2957,axiom,
k3(b,b,c) ).
cnf(u2975,axiom,
n4(b,b) ).
cnf(u2980,axiom,
n4(b,c) ).
cnf(u3005,axiom,
~ p0(e,e) ).
cnf(u3015,axiom,
~ p0(c,e) ).
cnf(u3026,axiom,
l1(d,X0) ).
cnf(u3157,axiom,
~ n0(b,c) ).
cnf(u3584,axiom,
p1(b,X0,c) ).
cnf(u3588,axiom,
~ m0(c,b,c) ).
cnf(u3596,axiom,
~ m0(c,c,e) ).
cnf(u3601,axiom,
~ m0(c,c,b) ).
cnf(u3606,axiom,
~ m0(c,c,c) ).
cnf(u3614,axiom,
~ m0(b,c,b) ).
cnf(u3618,axiom,
p1(b,X0,a) ).
cnf(u3632,axiom,
~ m0(e,b,b) ).
cnf(u3640,axiom,
~ m0(e,c,e) ).
cnf(u3645,axiom,
~ m0(e,b,e) ).
cnf(u3653,axiom,
~ m0(e,e,e) ).
cnf(u3661,axiom,
~ m0(d,b,b) ).
cnf(u3684,axiom,
k3(a,a,X1) ).
cnf(u3740,axiom,
k3(X1,X1,d) ).
cnf(u3852,axiom,
~ k0(c) ).
cnf(u3859,axiom,
( ~ l0(X1)
| q1(X1,d,d) ) ).
cnf(u3868,axiom,
~ k0(d) ).
cnf(u3902,axiom,
k3(d,d,e) ).
cnf(u3960,axiom,
k2(b,a) ).
cnf(u3965,axiom,
k2(e,a) ).
cnf(u3973,axiom,
k2(e,b) ).
cnf(u3978,axiom,
k2(a,e) ).
cnf(u3983,axiom,
k2(a,b) ).
cnf(u3991,axiom,
k2(e,c) ).
cnf(u4001,axiom,
k2(X0,d) ).
cnf(u4304,axiom,
p2(a,e,c) ).
cnf(u4307,axiom,
n1(e,a,a) ).
cnf(u4313,axiom,
p2(a,e,b) ).
cnf(u4318,axiom,
p2(a,e,d) ).
cnf(u4327,axiom,
~ n1(e,d,a) ).
cnf(u4336,axiom,
~ n1(e,b,a) ).
cnf(u4492,axiom,
q3(b,a) ).
cnf(u4496,axiom,
s2(a) ).
cnf(u4501,axiom,
q3(a,b) ).
cnf(u4508,axiom,
~ q3(e,a) ).
cnf(u4518,axiom,
~ q3(b,c) ).
cnf(u4526,axiom,
q3(b,d) ).
cnf(u4531,axiom,
q3(d,b) ).
cnf(u4732,axiom,
n1(c,X1,X1) ).
cnf(u4743,axiom,
( ~ l1(X0,b)
| ~ l0(X0) ) ).
cnf(u4752,axiom,
n1(a,X1,X1) ).
cnf(u4761,axiom,
n1(e,c,c) ).
cnf(u4769,axiom,
n1(d,c,c) ).
cnf(u5312,axiom,
( ~ k2(X1,e)
| k3(X1,X1,c) ) ).
cnf(u5319,axiom,
( ~ k2(X1,b)
| k3(X1,X1,c) ) ).
cnf(u5323,axiom,
( ~ k2(X1,c)
| k3(X1,X1,c) ) ).
cnf(u5330,axiom,
( ~ k2(X1,c)
| k3(X1,X1,b) ) ).
cnf(u5337,axiom,
( ~ k2(X1,b)
| k3(X1,X1,b) ) ).
cnf(u5345,axiom,
( ~ k2(X1,a)
| k3(X1,X1,b) ) ).
cnf(u5349,axiom,
( ~ k2(X1,e)
| k3(X1,X1,b) ) ).
cnf(u5357,axiom,
~ q0(X0,a) ).
cnf(u5368,axiom,
( ~ k2(X1,c)
| k3(X1,X1,e) ) ).
cnf(u5375,axiom,
( ~ k2(X1,b)
| k3(X1,X1,e) ) ).
cnf(u5379,axiom,
( ~ k2(X1,a)
| k3(X1,X1,e) ) ).
cnf(u5383,axiom,
( ~ k2(X1,e)
| k3(X1,X1,e) ) ).
cnf(u5391,axiom,
k3(X1,X1,b) ).
cnf(u5599,axiom,
~ m2(a) ).
cnf(u5607,axiom,
~ m2(e) ).
cnf(u5726,axiom,
p2(c,b,b) ).
cnf(u5734,axiom,
p2(b,a,a) ).
cnf(u5742,axiom,
p2(a,b,b) ).
cnf(u5750,axiom,
p2(e,a,a) ).
cnf(u5834,axiom,
p2(X1,e,e) ).
cnf(u5941,axiom,
p2(c,a,a) ).
cnf(u5952,axiom,
p2(X1,a,a) ).
cnf(u6046,axiom,
p2(X1,b,b) ).
cnf(u6222,axiom,
q4(b,c) ).
cnf(u6498,axiom,
~ n1(b,d,c) ).
cnf(u6509,axiom,
~ n1(e,b,b) ).
cnf(u6521,axiom,
~ n0(e,a) ).
cnf(u6982,axiom,
~ n0(d,a) ).
cnf(u7026,axiom,
( ~ q4(X0,X1)
| n5(X2,a)
| ~ n4(X2,X1) ) ).
cnf(u7035,axiom,
( ~ q4(X0,X1)
| n5(X2,c)
| ~ n4(X2,X1) ) ).
cnf(u7049,axiom,
( ~ q4(X0,X1)
| n5(X2,d)
| ~ n4(X2,X1) ) ).
cnf(u7060,axiom,
n5(e,b) ).
cnf(u7064,axiom,
( ~ q4(X0,X1)
| n5(X2,b)
| ~ n4(X2,X1) ) ).
cnf(u7083,axiom,
( ~ q4(X0,X1)
| n5(X2,e)
| ~ n4(X2,X1) ) ).
cnf(u7197,axiom,
m3(a,X0,a) ).
cnf(u3879,axiom,
q1(a,d,d) ).
cnf(rule_210,axiom,
( ~ n2(X0)
| k3(X0,X0,X0) ) ).
cnf(u6721,axiom,
( p3(e,e,X0)
| ~ k1(X0) ) ).
cnf(u5646,axiom,
r3(b,b,d) ).
cnf(u2445,axiom,
k5(c) ).
cnf(u1877,axiom,
l3(X0,X0) ).
cnf(u2706,axiom,
q2(X0,e,e) ).
cnf(u2544,axiom,
m1(b,e,e) ).
cnf(u2328,axiom,
r3(e,b,e) ).
cnf(rule_238,axiom,
( ~ p2(X0,X0,X0)
| m3(X0,X0,X0) ) ).
cnf(u2323,axiom,
p1(b,b,e) ).
cnf(u6904,axiom,
( ~ k0(X0)
| q2(c,X0,c) ) ).
cnf(rule_319,axiom,
( ~ p5(X0,X2,X0)
| ~ l2(X0,X2)
| p5(X0,X1,X1)
| ~ m4(X2,X1) ) ).
cnf(u1944,axiom,
m1(X0,d,X0) ).
cnf(u6792,axiom,
q2(a,e,a) ).
cnf(u5650,axiom,
p4(d,c,c) ).
cnf(u2203,axiom,
p2(a,e,e) ).
cnf(u4398,axiom,
m3(e,d,d) ).
cnf(u3733,axiom,
p2(e,d,X0) ).
cnf(u1821,axiom,
n2(X0) ).
cnf(rule_257,axiom,
( ~ n1(X2,X0,X1)
| q3(X0,X1)
| ~ s2(X0)
| ~ q3(X1,X0) ) ).
cnf(u2089,axiom,
r3(c,c,c) ).
cnf(u4915,axiom,
( ~ n0(X0,c)
| k3(X0,e,X0) ) ).
cnf(u3134,axiom,
r3(e,c,c) ).
cnf(u3220,axiom,
p3(d,c,c) ).
cnf(axiom_38,axiom,
m0(b,a,a) ).
cnf(u3373,axiom,
( ~ q0(X0,b)
| m1(X0,a,b) ) ).
cnf(rule_122,axiom,
( ~ m0(X0,X1,X0)
| q1(X0,X0,X0) ) ).
cnf(u3127,axiom,
( ~ s2(X0)
| r3(b,X0,X0) ) ).
cnf(rule_096,axiom,
( ~ q1(X3,X1,X2)
| ~ n1(X1,X2,X2)
| ~ p0(X1,X3)
| ~ m1(X0,X2,X1)
| q1(X0,X0,X0) ) ).
cnf(u1825,axiom,
k3(X0,X0,X0) ).
cnf(rule_255,axiom,
( ~ q2(X2,X0,X1)
| q3(X0,X1)
| ~ n0(X2,X0) ) ).
cnf(u3720,axiom,
p1(a,X0,b) ).
cnf(u5067,axiom,
p3(c,b,b) ).
cnf(u1698,axiom,
n3(d) ).
cnf(rule_038,axiom,
( ~ n0(X0,X0)
| n1(X0,X0,X0)
| ~ q0(a,X0) ) ).
cnf(u2996,axiom,
( ~ p0(a,X0)
| l1(X0,a) ) ).
cnf(u1715,axiom,
l3(b,b) ).
cnf(u7102,axiom,
( ~ n4(X0,X1)
| n5(X0,X2) ) ).
cnf(rule_187,axiom,
( ~ q2(X1,X1,X1)
| ~ r1(X1)
| ~ m0(X2,X3,X0)
| ~ k0(X1)
| q2(X0,X1,X0) ) ).
cnf(u1947,axiom,
( ~ l0(X0)
| m1(X0,b,X0) ) ).
cnf(u2350,axiom,
p2(e,e,c) ).
cnf(u3501,axiom,
k3(b,b,a) ).
cnf(u3001,axiom,
~ p0(a,a) ).
cnf(u2207,axiom,
m3(c,e,e) ).
cnf(u3496,axiom,
p1(a,b,b) ).
cnf(u3625,axiom,
p1(a,X0,a) ).
cnf(u3244,axiom,
( p3(X0,c,c)
| ~ l1(X0,d) ) ).
cnf(rule_013,axiom,
( ~ q0(X1,X0)
| m1(X0,X0,X0) ) ).
cnf(u4930,axiom,
( ~ n0(X0,d)
| k3(X0,e,X0) ) ).
cnf(u1967,axiom,
n1(e,e,b) ).
cnf(rule_268,axiom,
( ~ r3(X1,X3,X3)
| ~ m2(X1)
| ~ m3(X2,b,X0)
| r3(X0,X0,X1) ) ).
cnf(u2361,axiom,
q1(d,d,b) ).
cnf(u4919,axiom,
( ~ n0(X0,b)
| k3(X0,b,X0) ) ).
cnf(u1693,axiom,
k3(b,b,b) ).
cnf(u4913,axiom,
( ~ n0(X0,e)
| k3(X0,e,X0) ) ).
cnf(rule_141,axiom,
( ~ q1(X0,a,X0)
| p2(X0,a,X0) ) ).
cnf(u5189,axiom,
( ~ m0(b,X1,X0)
| s3(c,X0) ) ).
cnf(u2874,axiom,
q3(c,d) ).
cnf(u1710,axiom,
l4(e) ).
cnf(rule_040,axiom,
( ~ m0(X0,X1,e)
| n1(X0,e,e)
| ~ k1(X0) ) ).
cnf(u2645,axiom,
q1(X0,a,X0) ).
cnf(u2700,axiom,
( ~ k0(X0)
| q2(c,X0,X0) ) ).
cnf(u4447,axiom,
( ~ p2(X0,c,e)
| p3(X0,c,c) ) ).
cnf(u1865,axiom,
s2(b) ).
cnf(u6285,axiom,
( ~ q2(X0,X1,d)
| q4(d,X1) ) ).
cnf(u5625,axiom,
r3(c,c,b) ).
cnf(rule_295,axiom,
( ~ m3(X3,X4,X3)
| ~ k3(X2,X2,X0)
| ~ q2(X3,X1,X0)
| q4(X0,X1) ) ).
cnf(u6059,axiom,
k3(b,X0,b) ).
cnf(u3125,axiom,
l2(X0,b) ).
cnf(u2756,axiom,
p3(c,c,e) ).
cnf(u6851,axiom,
p4(c,e,e) ).
cnf(u2646,axiom,
q1(X0,d,X0) ).
cnf(u3663,axiom,
p1(d,X0,d) ).
cnf(u4452,axiom,
( ~ p2(X0,c,b)
| p3(X0,c,c) ) ).
cnf(u1949,axiom,
m1(c,b,c) ).
cnf(rule_285,axiom,
( ~ r3(X1,X0,X1)
| ~ r0(X0)
| p4(X0,X0,X1) ) ).
cnf(u2128,axiom,
n5(X0,X0) ).
cnf(rule_308,axiom,
( ~ m0(X1,X0,X1)
| n5(X0,X0)
| ~ n5(X1,X0) ) ).
cnf(rule_028,axiom,
( ~ m0(X0,X0,X0)
| ~ l0(X0)
| ~ k0(X0)
| m1(X0,X0,X0) ) ).
cnf(u1953,axiom,
m1(X0,X0,X0) ).
cnf(rule_166,axiom,
( ~ m1(a,X0,d)
| ~ n0(X0,d)
| p2(a,X0,d) ) ).
cnf(u6614,axiom,
r3(a,b,c) ).
cnf(u4824,axiom,
p4(b,b,a) ).
cnf(u6214,axiom,
( ~ q2(c,X0,e)
| q4(e,X0) ) ).
cnf(u3791,axiom,
k3(X0,d,X0) ).
cnf(u4964,axiom,
m3(b,b,a) ).
cnf(rule_051,axiom,
( ~ n1(X1,X0,X1)
| ~ m1(c,X0,X1)
| ~ m0(b,X1,c)
| n1(X0,X0,X0) ) ).
cnf(rule_192,axiom,
( ~ p2(X2,X1,X3)
| ~ s1(X1)
| k3(X0,X1,X0)
| ~ n0(X0,X3) ) ).
cnf(u2407,axiom,
r3(c,b,b) ).
cnf(u3882,axiom,
q1(c,e,e) ).
cnf(rule_156,axiom,
( ~ q1(a,X1,X0)
| ~ n1(e,X0,a)
| p2(X0,e,X1) ) ).
cnf(u3430,axiom,
( ~ m1(b,b,X0)
| m1(X0,b,b) ) ).
cnf(u4430,axiom,
( ~ p2(X0,e,a)
| p3(X0,e,e) ) ).
cnf(u4552,axiom,
q3(b,e) ).
cnf(rule_057,axiom,
( ~ r0(X0)
| n1(X0,X0,X0) ) ).
cnf(u2657,axiom,
p2(X0,a,X0) ).
cnf(u2412,axiom,
( ~ l1(X0,e)
| s4(X0) ) ).
cnf(u4984,axiom,
k3(a,e,a) ).
cnf(u2405,axiom,
( ~ s2(X0)
| r3(c,X0,X0) ) ).
cnf(u3434,axiom,
( ~ m1(c,c,X0)
| m1(X0,c,c) ) ).
cnf(u6090,axiom,
p4(b,b,X0) ).
cnf(u4441,axiom,
( ~ p2(X0,b,d)
| p3(X0,b,b) ) ).
cnf(u4096,axiom,
( p3(X0,e,b)
| ~ l1(X0,d) ) ).
cnf(u4571,axiom,
p3(b,e,e) ).
cnf(u3816,axiom,
p3(a,a,d) ).
cnf(u2431,axiom,
s4(c) ).
cnf(u5131,axiom,
r3(c,b,c) ).
cnf(u2794,axiom,
( ~ n0(X0,c)
| q3(c,X0)
| ~ k1(X0) ) ).
cnf(rule_218,axiom,
( l3(X0,X0)
| ~ r2(X0) ) ).
cnf(u2533,axiom,
m1(d,b,b) ).
cnf(rule_066,axiom,
( ~ n0(X1,X0)
| p1(X0,X0,X0) ) ).
cnf(u3562,axiom,
( ~ m0(X0,X0,b)
| p1(X0,X1,X0) ) ).
cnf(u5847,axiom,
p3(X0,e,e) ).
cnf(u1753,axiom,
p3(d,d,d) ).
cnf(axiom_7,axiom,
n0(d,b) ).
cnf(u2562,axiom,
n1(b,e,e) ).
cnf(u5908,axiom,
( ~ l1(X0,b)
| p2(X0,a,a) ) ).
cnf(u4970,axiom,
( ~ p2(X0,d,c)
| p3(X0,d,d) ) ).
cnf(u1659,axiom,
m1(d,d,d) ).
cnf(u5083,axiom,
( ~ k2(X0,X1)
| ~ r2(X1)
| r3(X1,X0,X1) ) ).
cnf(u5866,axiom,
n4(X0,e) ).
cnf(rule_194,axiom,
( ~ k2(X1,X0)
| k3(X0,X0,X1) ) ).
cnf(u2302,axiom,
r3(b,e,b) ).
cnf(u6175,axiom,
( ~ k3(X0,X0,X1)
| ~ q2(e,X2,X1)
| q4(X1,X2) ) ).
cnf(u4039,axiom,
( p3(X0,a,e)
| ~ l1(X0,d) ) ).
cnf(u3576,axiom,
( ~ m0(b,X0,b)
| p1(X0,X1,b) ) ).
cnf(rule_007,axiom,
( ~ p0(X2,X1)
| m1(X0,X1,X0)
| ~ r0(X0) ) ).
cnf(rule_235,axiom,
( ~ k3(X0,X1,X0)
| ~ r2(X1)
| m3(X0,X0,X1) ) ).
cnf(u2508,axiom,
r4(c) ).
cnf(u2275,axiom,
( ~ r0(X0)
| m1(X0,X1,X0) ) ).
cnf(u3057,axiom,
n4(X0,X0) ).
cnf(u2696,axiom,
( ~ k0(X0)
| q2(e,X0,X0) ) ).
cnf(u7156,axiom,
( ~ m0(X0,X1,X1)
| ~ l2(X1,X0)
| m3(X0,e,X0) ) ).
cnf(rule_225,axiom,
( ~ m0(X2,X2,X1)
| m3(X0,X1,X0)
| ~ l2(X3,X0)
| ~ m0(X0,X3,X3)
| ~ s2(X2) ) ).
cnf(u1534,axiom,
( ~ l0(X0)
| n1(X0,X1,X0) ) ).
cnf(rule_095,axiom,
( ~ p0(X1,X0)
| q1(X0,X1,X1) ) ).
cnf(u4224,axiom,
( ~ k1(X0)
| k3(X0,X0,e) ) ).
cnf(rule_241,axiom,
( ~ q2(X3,d,X0)
| p3(X0,X1,X2)
| ~ k2(X1,X2) ) ).
cnf(u2442,axiom,
k5(e) ).
cnf(u6180,axiom,
( ~ k3(X0,X0,X1)
| ~ q2(a,X2,X1)
| q4(X1,X2) ) ).
cnf(u6727,axiom,
p3(e,a,e) ).
cnf(u3118,axiom,
( q2(e,c,X0)
| ~ k1(X0) ) ).
cnf(u2435,axiom,
s4(b) ).
cnf(axiom_22,axiom,
p0(b,c) ).
cnf(u6685,axiom,
q4(e,d) ).
cnf(rule_106,axiom,
( ~ s0(X0)
| q1(X0,X0,X0) ) ).
cnf(u4391,axiom,
m3(c,b,b) ).
cnf(u7087,axiom,
( ~ q4(X0,X1)
| ~ n4(X2,X1)
| n5(X2,X3) ) ).
cnf(u3100,axiom,
( ~ l0(X0)
| n1(b,X0,b) ) ).
cnf(u3219,axiom,
p3(d,b,b) ).
cnf(u6950,axiom,
( ~ n1(X0,d,X0)
| q2(d,X0,d) ) ).
cnf(u1701,axiom,
n3(b) ).
cnf(u4425,axiom,
( ~ p2(X0,d,d)
| p3(X0,d,d) ) ).
cnf(u2701,axiom,
q2(e,b,b) ).
cnf(u1823,axiom,
p3(X0,X0,X0) ).
cnf(u2074,axiom,
r3(X0,X0,X0) ).
cnf(u3115,axiom,
l2(X0,e) ).
cnf(u2699,axiom,
( ~ k0(X0)
| q2(b,X0,X0) ) ).
cnf(u4422,axiom,
( ~ p2(X0,X1,X1)
| p3(X0,X1,X1) ) ).
cnf(u1688,axiom,
p2(c,c,c) ).
cnf(u3239,axiom,
( p3(X0,X1,X1)
| ~ l1(X0,d) ) ).
cnf(u2097,axiom,
p4(a,a,a) ).
cnf(u6706,axiom,
( ~ m0(X0,X1,X2)
| q2(X2,b,X2) ) ).
cnf(axiom_35,axiom,
m0(d,e,c) ).
cnf(rule_202,axiom,
( ~ k3(X1,X4,X3)
| ~ q0(X2,X1)
| ~ k2(X0,X3)
| k3(X0,X0,X1) ) ).
cnf(rule_281,axiom,
( ~ p3(X0,X1,X1)
| n4(X0,X1)
| ~ n4(X0,X0) ) ).
cnf(u1951,axiom,
m1(c,e,c) ).
cnf(u3243,axiom,
( p3(X0,b,b)
| ~ l1(X0,d) ) ).
cnf(u4397,axiom,
m3(e,b,b) ).
cnf(u3383,axiom,
n1(e,e,a) ).
cnf(u5074,axiom,
p3(a,b,b) ).
cnf(u6957,axiom,
( ~ l1(X0,a)
| q3(a,X0)
| ~ n0(X0,a) ) ).
cnf(rule_125,axiom,
( ~ p0(X0,X0)
| s1(X0) ) ).
cnf(u2734,axiom,
m3(e,e,c) ).
cnf(rule_279,axiom,
( ~ s3(a,X0)
| ~ l2(X2,X1)
| m4(X0,X1) ) ).
cnf(u2968,axiom,
p4(b,e,b) ).
cnf(u6704,axiom,
( ~ m0(X1,X2,X3)
| ~ k0(X0)
| q2(X3,X0,X3) ) ).
cnf(u1971,axiom,
n1(e,c,e) ).
cnf(rule_152,axiom,
( ~ p2(X0,X1,X0)
| ~ n1(X2,X1,X2)
| ~ p0(X0,X1)
| p2(X0,X1,X1) ) ).
cnf(u2216,axiom,
k3(e,a,e) ).
cnf(u5183,axiom,
( ~ m0(b,X1,X0)
| s3(b,X0) ) ).
cnf(u6970,axiom,
q2(d,a,d) ).
cnf(u4709,axiom,
( ~ q0(X0,X0)
| q1(X1,X0,X1)
| ~ l0(X1) ) ).
cnf(u3908,axiom,
q1(e,X0,X0) ).
cnf(rule_123,axiom,
( ~ m0(c,X0,X0)
| q1(X0,X0,X0)
| ~ r0(X0) ) ).
cnf(u6477,axiom,
( ~ p1(X0,X0,c)
| ~ n1(e,X0,c)
| q2(X0,e,X0)
| ~ k1(X0) ) ).
cnf(u6902,axiom,
( ~ k0(X0)
| q2(X1,X0,X1) ) ).
cnf(u6293,axiom,
( ~ q2(X0,X1,b)
| q4(b,X1) ) ).
cnf(rule_150,axiom,
( ~ m1(X1,X1,X0)
| p2(X0,X0,X0) ) ).
cnf(u3515,axiom,
( ~ m0(X1,b,X0)
| n1(X0,X0,X1) ) ).
cnf(u5405,axiom,
p4(X0,b,X0) ).
cnf(u3775,axiom,
l3(e,d) ).
cnf(u2636,axiom,
( ~ n0(X0,X1)
| q1(X2,X1,X2) ) ).
cnf(rule_037,axiom,
( ~ p0(X2,X0)
| n1(X0,X1,X0)
| ~ l0(X1)
| ~ r0(X0) ) ).
cnf(rule_320,axiom,
( p5(X0,X1,X0)
| ~ q4(X1,X2)
| ~ s1(X0) ) ).
cnf(u3518,axiom,
n1(c,c,e) ).
cnf(u3407,axiom,
( ~ m1(d,e,X0)
| m1(X0,e,e) ) ).
cnf(u4034,axiom,
( ~ r2(X0)
| m3(X0,e,X0) ) ).
cnf(u7234,axiom,
( ~ m2(X0)
| r3(e,e,X0) ) ).
cnf(u4826,axiom,
~ l0(d) ).
cnf(u6876,axiom,
q4(a,b) ).
cnf(u4442,axiom,
( ~ p2(X0,b,e)
| p3(X0,b,b) ) ).
cnf(u4162,axiom,
m3(a,e,a) ).
cnf(rule_035,axiom,
( ~ l0(X1)
| ~ r0(X0)
| m1(X0,X1,X0) ) ).
cnf(u3249,axiom,
( ~ l1(X0,d)
| n4(X0,d) ) ).
cnf(u7013,axiom,
( ~ n5(b,X3)
| ~ n4(X2,X1)
| n5(X2,X3)
| ~ q4(X0,X1) ) ).
cnf(u5573,axiom,
( ~ m3(X1,b,X2)
| ~ m2(X0)
| r3(X2,X2,X0) ) ).
cnf(rule_290,axiom,
( ~ p4(X0,X2,X0)
| ~ m3(X1,X2,X0)
| p4(X0,X0,X0) ) ).
cnf(rule_062,axiom,
( ~ n1(X1,X0,X1)
| ~ m0(X1,X1,X2)
| n1(X0,X0,X0) ) ).
cnf(u4944,axiom,
( ~ n0(X0,X1)
| k3(X0,e,X0) ) ).
cnf(u5974,axiom,
k3(a,X0,a) ).
cnf(u3672,axiom,
p1(X0,X1,a) ).
cnf(u4969,axiom,
m3(d,d,c) ).
cnf(u3522,axiom,
n1(a,a,b) ).
cnf(u2641,axiom,
q1(X0,c,X0) ).
cnf(u6612,axiom,
r3(a,e,c) ).
cnf(rule_309,axiom,
( ~ n4(X1,X0)
| n5(X0,X0) ) ).
cnf(u3686,axiom,
( ~ m0(d,X0,d)
| p1(X0,X1,d) ) ).
cnf(u2920,axiom,
p4(e,e,c) ).
cnf(u2246,axiom,
p1(c,b,c) ).
cnf(u3418,axiom,
( ~ m1(e,b,X0)
| m1(X0,b,b) ) ).
cnf(u3128,axiom,
( q2(b,c,X0)
| ~ k1(X0) ) ).
cnf(u2132,axiom,
n5(c,c) ).
cnf(u1549,axiom,
k1(d) ).
cnf(u4400,axiom,
m3(X0,d,d) ).
cnf(rule_292,axiom,
( ~ k3(X1,X2,X2)
| p4(X0,X0,X0)
| ~ n4(X0,X2)
| ~ p1(X2,X1,X0) ) ).
cnf(u2415,axiom,
( ~ l1(X0,c)
| s4(X0) ) ).
cnf(u4941,axiom,
( ~ n0(X1,d)
| k3(X1,X0,X1) ) ).
cnf(u4168,axiom,
m3(a,d,a) ).
cnf(u6482,axiom,
( ~ p1(X0,X0,c)
| ~ n1(b,X0,c)
| q2(X0,b,X0)
| ~ k1(X0) ) ).
cnf(rule_307,axiom,
( ~ p4(X4,X4,X1)
| ~ q4(X2,X3)
| ~ n4(X0,X3)
| n5(X0,X1)
| ~ n5(X4,X1) ) ).
cnf(u2524,axiom,
q1(d,d,X0) ).
cnf(u4814,axiom,
r3(a,b,a) ).
cnf(u7167,axiom,
m3(d,e,d) ).
cnf(u4036,axiom,
p3(d,c,e) ).
cnf(u6881,axiom,
q4(c,b) ).
cnf(u1737,axiom,
n2(b) ).
cnf(u2413,axiom,
( ~ l1(X0,a)
| s4(X0) ) ).
cnf(u1751,axiom,
n2(d) ).
cnf(u2468,axiom,
q2(e,c,e) ).
cnf(u6525,axiom,
q4(b,a) ).
cnf(u3030,axiom,
l1(b,e) ).
cnf(rule_178,axiom,
( ~ n1(X1,X0,X2)
| ~ q0(X1,X0)
| q2(X0,X0,X0) ) ).
cnf(u6080,axiom,
( ~ r2(X0)
| m3(b,b,X0) ) ).
cnf(u2036,axiom,
q2(X0,X0,X0) ).
cnf(rule_153,axiom,
( ~ n1(d,d,X0)
| p2(X0,X0,X0) ) ).
cnf(u4582,axiom,
n4(a,e) ).
cnf(u1754,axiom,
m3(d,d,d) ).
cnf(u2284,axiom,
p2(X0,e,X0) ).
cnf(u5099,axiom,
( ~ k2(X0,c)
| r3(b,X0,c) ) ).
cnf(rule_159,axiom,
( ~ k1(X0)
| p2(X0,X0,X0) ) ).
cnf(u2697,axiom,
( ~ k0(X0)
| q2(a,X0,X0) ) ).
cnf(u4593,axiom,
n4(e,d) ).
cnf(u7182,axiom,
m3(e,a,e) ).
cnf(u6627,axiom,
r3(c,b,a) ).
cnf(u1791,axiom,
( ~ m0(X3,X2,X0)
| l2(X0,X0) ) ).
cnf(u2547,axiom,
m1(b,c,c) ).
cnf(u5630,axiom,
p4(b,d,d) ).
cnf(u3456,axiom,
q1(c,c,a) ).
cnf(u4099,axiom,
( p3(X0,a,b)
| ~ l1(X0,d) ) ).
cnf(u7163,axiom,
m3(b,e,b) ).
cnf(u6734,axiom,
p3(e,c,e) ).
cnf(axiom_29,axiom,
q0(d,b) ).
cnf(u4124,axiom,
p3(d,e,c) ).
cnf(axiom_19,axiom,
m0(X0,d,X1) ).
cnf(rule_246,axiom,
( p3(X0,X0,X0)
| ~ l2(X0,X0) ) ).
cnf(u4092,axiom,
( p3(X0,c,b)
| ~ l1(X0,d) ) ).
cnf(u2318,axiom,
( ~ k0(X0)
| p1(b,b,X0) ) ).
cnf(u5909,axiom,
( ~ l1(X0,X0)
| p2(X0,a,a) ) ).
cnf(u2440,axiom,
( ~ l2(X1,X0)
| k5(X0) ) ).
cnf(u6853,axiom,
q2(X0,b,X0) ).
cnf(u4396,axiom,
m3(a,d,d) ).
cnf(u3212,axiom,
( ~ k2(X1,X2)
| p3(X0,X1,X2)
| ~ l1(X0,d) ) ).
cnf(u2443,axiom,
k5(a) ).
cnf(rule_265,axiom,
( r3(X0,X0,X0)
| ~ l2(X1,X0) ) ).
cnf(u5026,axiom,
( ~ p2(X0,d,a)
| p3(X0,d,d) ) ).
cnf(rule_236,axiom,
( ~ n2(X0)
| m3(X0,X0,X0) ) ).
cnf(u1827,axiom,
n3(X0) ).
cnf(u1702,axiom,
n3(c) ).
cnf(u6798,axiom,
( ~ n0(X0,e)
| q3(e,X0) ) ).
cnf(axiom_17,axiom,
q0(X0,d) ).
cnf(u3475,axiom,
( ~ m1(e,a,X0)
| m1(X0,a,a) ) ).
cnf(u2342,axiom,
p1(e,c,e) ).
cnf(rule_263,axiom,
( ~ r3(X0,X0,X1)
| ~ m0(d,X1,X0)
| r3(X0,X0,X0) ) ).
cnf(u6309,axiom,
( q4(X0,c)
| ~ k1(X0) ) ).
cnf(u2364,axiom,
( l3(X0,b)
| ~ r0(X0) ) ).
cnf(u3371,axiom,
( ~ q0(X0,e)
| m1(X0,a,e) ) ).
cnf(u4014,axiom,
k3(d,d,X0) ).
cnf(u3488,axiom,
m1(a,b,b) ).
cnf(u4394,axiom,
m3(b,d,d) ).
cnf(u1961,axiom,
( ~ r0(X0)
| m1(X0,c,X0) ) ).
cnf(u2620,axiom,
p1(e,b,b) ).
cnf(rule_021,axiom,
( ~ k0(X1)
| ~ l0(X0)
| m1(X0,X1,X0) ) ).
cnf(rule_107,axiom,
( ~ m0(e,d,X0)
| ~ m0(X0,d,X0)
| q1(e,X0,X0) ) ).
cnf(u4252,axiom,
k2(b,e) ).
cnf(u5155,axiom,
( ~ r2(X0)
| r3(X0,b,X0)
| ~ k1(X0) ) ).
cnf(u3374,axiom,
( ~ q0(X0,c)
| m1(X0,a,c) ) ).
cnf(u6736,axiom,
p3(e,c,b) ).
cnf(u2096,axiom,
p4(e,e,e) ).
cnf(u3391,axiom,
m1(d,a,b) ).
cnf(u3728,axiom,
( ~ m0(d,X0,X1)
| p1(X0,X2,d) ) ).
cnf(rule_134,axiom,
( ~ m1(X2,X1,X1)
| ~ m0(X1,X0,X2)
| l2(X0,X0)
| ~ p0(X1,X0) ) ).
cnf(u5645,axiom,
r3(c,c,d) ).
cnf(u6182,axiom,
( ~ k3(X0,X0,X1)
| ~ q2(b,X2,X1)
| q4(X1,X2) ) ).
cnf(u4392,axiom,
m3(c,d,d) ).
cnf(u2570,axiom,
n1(c,e,e) ).
cnf(u4921,axiom,
( ~ n0(X0,b)
| k3(X0,e,X0) ) ).
cnf(u1684,axiom,
p2(d,d,d) ).
cnf(u3883,axiom,
q1(a,e,e) ).
cnf(u3502,axiom,
p4(b,a,b) ).
cnf(u3694,axiom,
p4(a,X0,a) ).
cnf(u4920,axiom,
( ~ n0(X0,b)
| k3(X0,a,X0) ) ).
cnf(rule_063,axiom,
( ~ n0(d,X0)
| p1(X0,X0,X1)
| ~ k0(X1) ) ).
cnf(u6213,axiom,
( ~ q2(c,X0,b)
| q4(b,X0) ) ).
cnf(u4013,axiom,
p3(d,X0,d) ).
cnf(rule_025,axiom,
( ~ m0(X1,X2,X0)
| m1(X0,X0,X0) ) ).
cnf(u4922,axiom,
( ~ n0(X0,a)
| k3(X0,c,X0) ) ).
cnf(u4020,axiom,
p4(d,X0,d) ).
cnf(rule_046,axiom,
( ~ m1(X1,X2,X0)
| n1(X0,X0,X0)
| ~ k0(X1) ) ).
cnf(u4539,axiom,
q3(d,c) ).
cnf(u1975,axiom,
q1(X0,X0,X0) ).
cnf(rule_293,axiom,
( ~ n4(X2,X0)
| ~ q3(X1,X2)
| p4(X0,X0,X0)
| ~ l3(X1,X1) ) ).
cnf(u6855,axiom,
q2(c,b,c) ).
cnf(rule_036,axiom,
( ~ m0(b,X1,X0)
| n1(X0,X0,X1) ) ).
cnf(u2637,axiom,
( ~ n0(X0,X1)
| q1(c,X1,c) ) ).
cnf(u1721,axiom,
q1(d,b,b) ).
cnf(u4951,axiom,
m3(b,b,c) ).
cnf(u2399,axiom,
l3(e,a) ).
cnf(rule_291,axiom,
( ~ p3(X1,X1,X0)
| p4(X0,X0,X0) ) ).
cnf(u3412,axiom,
( ~ m1(d,c,X0)
| m1(X0,c,c) ) ).
cnf(u2131,axiom,
n5(a,a) ).
cnf(u3798,axiom,
( p4(X0,X0,e)
| ~ r0(X0) ) ).
cnf(rule_314,axiom,
( ~ r4(X0)
| n5(X0,X0) ) ).
cnf(u7238,axiom,
p4(d,e,e) ).
cnf(rule_164,axiom,
( ~ p2(X2,X1,X0)
| ~ p0(X0,X0)
| ~ r1(X1)
| p2(X0,X0,X0) ) ).
cnf(u5882,axiom,
p4(e,e,X0) ).
cnf(u4804,axiom,
r3(a,c,a) ).
cnf(u5666,axiom,
( ~ m2(X0)
| r3(b,b,X0) ) ).
cnf(rule_065,axiom,
( ~ l1(X1,X1)
| p1(X0,X0,X0)
| ~ p0(X0,X1)
| ~ n0(X1,X1) ) ).
cnf(u5696,axiom,
( p5(X0,X3,X3)
| ~ m4(X1,X0)
| ~ q4(X1,X2)
| ~ l2(X0,X1)
| ~ m4(X0,X3) ) ).
cnf(u6235,axiom,
l5(c) ).
cnf(u2014,axiom,
p2(b,e,b) ).
cnf(u1616,axiom,
l1(a,a) ).
cnf(u6907,axiom,
( ~ k0(X0)
| q2(e,X0,e) ) ).
cnf(u2514,axiom,
m3(a,c,a) ).
cnf(u2020,axiom,
p2(c,b,c) ).
cnf(u2214,axiom,
r3(a,e,a) ).
cnf(u1757,axiom,
l4(d) ).
cnf(u4266,axiom,
( p3(d,b,X0)
| ~ k1(X0) ) ).
cnf(u2410,axiom,
( ~ l1(X0,X1)
| s4(X0) ) ).
cnf(u2496,axiom,
( ~ p0(X3,X0)
| r4(X0) ) ).
cnf(u5841,axiom,
m3(X0,e,e) ).
cnf(rule_318,axiom,
( p5(X0,X0,X1)
| ~ s4(X1)
| ~ l2(X0,X0) ) ).
cnf(u2403,axiom,
( ~ r2(X0)
| m3(X0,c,X0) ) ).
cnf(rule_074,axiom,
( ~ p0(X1,X0)
| p1(X0,X0,X1)
| ~ r0(X0) ) ).
cnf(rule_148,axiom,
( ~ p2(X1,X0,X1)
| ~ m1(X1,X2,X0)
| p2(X0,X0,X0) ) ).
cnf(u3886,axiom,
q1(c,a,a) ).
cnf(u5850,axiom,
k3(e,X0,e) ).
cnf(u4468,axiom,
( ~ q3(X1,X0)
| ~ s2(X0)
| q3(X0,X1) ) ).
cnf(u4569,axiom,
p3(a,e,e) ).
cnf(u1756,axiom,
l4(b) ).
cnf(u2018,axiom,
p2(e,a,e) ).
cnf(u5678,axiom,
( p5(X0,X1,X1)
| ~ m4(X0,X1)
| ~ s4(X0) ) ).
cnf(u4978,axiom,
p3(a,a,b) ).
cnf(u1847,axiom,
k2(d,d) ).
cnf(u6013,axiom,
( ~ l1(X0,b)
| p2(X0,b,b) ) ).
cnf(u5104,axiom,
r3(b,e,c) ).
cnf(u4424,axiom,
( ~ p2(X0,X1,d)
| p3(X0,X1,X1) ) ).
cnf(u5192,axiom,
s3(c,X0) ).
cnf(rule_181,axiom,
( ~ p1(X0,X0,X0)
| q2(X0,X0,X0) ) ).
cnf(u5488,axiom,
p4(X0,c,X0) ).
cnf(u3145,axiom,
r3(b,c,c) ).
cnf(u3214,axiom,
( ~ k2(X0,X1)
| p3(d,X0,X1) ) ).
cnf(u4076,axiom,
r3(b,a,b) ).
cnf(u2430,axiom,
s4(a) ).
cnf(u6909,axiom,
( ~ k0(X0)
| q2(a,X0,a) ) ).
cnf(u4487,axiom,
( ~ q3(c,X0)
| ~ s2(X0)
| q3(X0,c) ) ).
cnf(u4429,axiom,
( ~ p2(X0,e,c)
| p3(X0,e,e) ) ).
cnf(u4466,axiom,
n4(c,e) ).
cnf(u5491,axiom,
( ~ r2(X0)
| p3(c,X0,X0) ) ).
cnf(axiom_3,axiom,
n0(d,e) ).
cnf(rule_103,axiom,
( ~ m0(X0,c,b)
| q1(X0,X0,X0) ) ).
cnf(u6678,axiom,
q2(e,b,e) ).
cnf(rule_249,axiom,
( ~ n2(X0)
| ~ k1(X0)
| p3(X0,X0,X0) ) ).
cnf(u3457,axiom,
( ~ m1(c,a,X0)
| m1(X0,a,a) ) ).
cnf(u6539,axiom,
r3(c,a,a) ).
cnf(axiom_30,axiom,
n0(e,e) ).
cnf(rule_206,axiom,
( ~ p2(X1,X0,X0)
| k3(X0,X1,X0) ) ).
cnf(u2563,axiom,
n1(a,e,e) ).
cnf(u5964,axiom,
r3(c,a,c) ).
cnf(rule_271,axiom,
( ~ r3(X1,X1,X1)
| ~ p3(X1,X0,X2)
| r3(X0,X0,X0) ) ).
cnf(rule_093,axiom,
( ~ q0(X1,X0)
| q1(X0,X0,X0) ) ).
cnf(u6624,axiom,
r3(c,e,a) ).
cnf(rule_247,axiom,
( ~ q2(X1,X2,X0)
| ~ n2(X0)
| p3(X0,X0,X0)
| ~ s1(X1) ) ).
cnf(u4390,axiom,
( ~ m2(X1)
| m3(X0,X1,X1) ) ).
cnf(u6707,axiom,
( ~ m0(X0,X1,X2)
| q2(X2,e,X2) ) ).
cnf(u4123,axiom,
( p3(X0,e,c)
| ~ l1(X0,d) ) ).
cnf(u3939,axiom,
( ~ k2(X1,X0)
| ~ k1(X1)
| k2(b,X0) ) ).
cnf(u6295,axiom,
( ~ l1(X0,X1)
| q4(X0,X1) ) ).
cnf(rule_272,axiom,
( ~ r3(X2,X0,X0)
| ~ k2(X1,X2)
| ~ r2(X2)
| r3(X0,X1,X2) ) ).
cnf(rule_005,axiom,
( ~ m0(X1,X1,X0)
| m1(X0,X1,X0) ) ).
cnf(u2265,axiom,
m1(X0,d,d) ).
cnf(u4450,axiom,
( ~ p2(X0,c,d)
| p3(X0,c,c) ) ).
cnf(u3723,axiom,
( ~ m0(b,X0,c)
| p1(X0,X1,b) ) ).
cnf(u5014,axiom,
p3(a,a,c) ).
cnf(u5408,axiom,
( ~ r2(X0)
| p3(b,X0,X0) ) ).
cnf(rule_260,axiom,
( ~ l2(c,X0)
| ~ s2(X1)
| r3(X0,X1,X1) ) ).
cnf(u3712,axiom,
p1(d,X0,b) ).
cnf(u6500,axiom,
q2(e,a,e) ).
cnf(axiom_18,axiom,
p0(c,b) ).
cnf(u5590,axiom,
( ~ m3(X0,b,X1)
| r3(X1,X1,b) ) ).
cnf(u2340,axiom,
p1(c,c,e) ).
cnf(u6713,axiom,
q4(e,b) ).
cnf(u5665,axiom,
( ~ m2(X0)
| r3(c,c,X0) ) ).
cnf(u2309,axiom,
m1(b,b,e) ).
cnf(u2960,axiom,
k3(c,c,b) ).
cnf(u3743,axiom,
r3(d,b,d) ).
cnf(u4130,axiom,
p3(e,c,c) ).
cnf(u2465,axiom,
( q2(X0,c,X0)
| ~ k1(X0) ) ).
cnf(u1685,axiom,
p2(e,e,e) ).
cnf(u6302,axiom,
q4(e,c) ).
cnf(u2213,axiom,
m3(a,e,e) ).
cnf(u2208,axiom,
r3(c,e,c) ).
cnf(u6807,axiom,
q4(c,e) ).
cnf(u5078,axiom,
n4(a,b) ).
cnf(u7115,axiom,
n5(X0,X1) ).
cnf(u1836,axiom,
q1(c,b,b) ).
cnf(u6233,axiom,
l5(a) ).
cnf(u5979,axiom,
r3(X0,a,X0) ).
cnf(u6205,axiom,
( ~ q2(c,X0,d)
| q4(d,X0) ) ).
cnf(u4258,axiom,
( p3(X0,b,e)
| ~ l1(X0,d) ) ).
cnf(rule_131,axiom,
( ~ l2(X1,X1)
| ~ s1(X0)
| ~ n0(e,X1)
| l2(X0,X1) ) ).
cnf(u3491,axiom,
q1(a,a,b) ).
cnf(rule_277,axiom,
( ~ p3(X1,X2,X0)
| l4(X0) ) ).
cnf(u3217,axiom,
p3(d,e,e) ).
cnf(rule_264,axiom,
( ~ s2(X0)
| r3(X0,X0,X0) ) ).
cnf(u7221,axiom,
m3(e,X0,e) ).
cnf(rule_047,axiom,
( ~ l1(X1,d)
| ~ p0(X1,X1)
| ~ r0(X0)
| n1(X0,d,X1) ) ).
cnf(u7181,axiom,
m3(d,a,d) ).
cnf(u7190,axiom,
( ~ l2(d,X0)
| m3(X0,X1,X0) ) ).
cnf(u1964,axiom,
m1(e,c,e) ).
cnf(u3768,axiom,
r3(e,X0,e) ).
cnf(rule_137,axiom,
( ~ p1(X1,X2,X0)
| n2(X0) ) ).
cnf(u1962,axiom,
( ~ r0(X0)
| m1(X0,a,X0) ) ).
cnf(u7194,axiom,
m3(b,X0,b) ).
cnf(u2529,axiom,
( ~ k1(X0)
| m1(b,X0,X0) ) ).
cnf(u4444,axiom,
( ~ p2(X0,b,b)
| p3(X0,b,b) ) ).
cnf(u2485,axiom,
( ~ l0(X0)
| r2(X0) ) ).
cnf(rule_018,axiom,
( ~ q0(X1,X2)
| m1(X0,X0,X0)
| ~ q0(X1,X0) ) ).
cnf(u3514,axiom,
( ~ m0(X1,a,X0)
| n1(X0,X0,X1) ) ).
cnf(u5196,axiom,
s3(b,X0) ).
cnf(u4427,axiom,
( ~ p2(X0,e,d)
| p3(X0,e,e) ) ).
cnf(u4927,axiom,
( ~ n0(X0,a)
| k3(X0,e,X0) ) ).
cnf(u7173,axiom,
( ~ l2(d,X0)
| m3(X0,a,X0) ) ).
cnf(u2398,axiom,
l3(e,c) ).
cnf(u5112,axiom,
p4(c,b,b) ).
cnf(rule_146,axiom,
( ~ p2(X0,X1,X0)
| ~ p1(X0,X2,X3)
| ~ l1(X2,X3)
| p2(X0,X1,X1) ) ).
cnf(u3806,axiom,
( p4(X0,X0,d)
| ~ r0(X0) ) ).
cnf(u6796,axiom,
q4(X0,e) ).
cnf(u3923,axiom,
( ~ k2(X1,X0)
| ~ k1(X1)
| k2(e,X0) ) ).
cnf(u3810,axiom,
( ~ r2(X0)
| p3(X0,X0,d) ) ).
cnf(u3142,axiom,
m3(e,c,e) ).
cnf(u2381,axiom,
l3(b,c) ).
cnf(u6728,axiom,
p3(e,a,b) ).
cnf(u2642,axiom,
q1(X0,e,X0) ).
cnf(u5652,axiom,
p4(d,b,b) ).
cnf(u3263,axiom,
( ~ l1(X0,d)
| n4(X0,a) ) ).
cnf(u4939,axiom,
( ~ n0(X1,X0)
| k3(X1,X0,X1) ) ).
cnf(u6074,axiom,
n4(X0,b) ).
cnf(u4928,axiom,
( ~ n0(X0,a)
| k3(X0,a,X0) ) ).
cnf(u1617,axiom,
l1(d,d) ).
cnf(u4700,axiom,
r3(b,c,b) ).
cnf(u2270,axiom,
q1(X0,X0,d) ).
cnf(u3270,axiom,
( ~ l1(X0,d)
| n4(X0,X1) ) ).
cnf(u2509,axiom,
r4(b) ).
cnf(rule_177,axiom,
( ~ p1(X0,X0,X0)
| ~ k0(X1)
| q2(X0,X1,X1) ) ).
cnf(rule_315,axiom,
( ~ k4(X0)
| ~ s1(X0)
| n5(X0,X0) ) ).
cnf(u4961,axiom,
k3(b,a,b) ).
cnf(u1739,axiom,
p3(b,b,b) ).
cnf(u4943,axiom,
( ~ n0(X0,X1)
| k3(X0,a,X0) ) ).
cnf(rule_058,axiom,
( ~ l1(X1,X0)
| n1(X0,X0,X0)
| ~ n0(X1,X0) ) ).
cnf(u6733,axiom,
p3(e,b,c) ).
cnf(u7240,axiom,
p4(b,e,e) ).
cnf(u2130,axiom,
n5(e,e) ).
cnf(u3417,axiom,
( ~ m1(e,e,X0)
| m1(X0,e,e) ) ).
cnf(u2267,axiom,
m1(e,b,b) ).
cnf(u2926,axiom,
( ~ m2(X0)
| k3(b,b,X0) ) ).
cnf(u5201,axiom,
s3(d,X0) ).
cnf(rule_175,axiom,
( ~ l1(X1,X0)
| p2(X0,X0,X0) ) ).
cnf(u1735,axiom,
p1(b,b,b) ).
cnf(u5025,axiom,
m3(d,d,a) ).
cnf(u2515,axiom,
p4(c,c,a) ).
cnf(rule_186,axiom,
( q2(X0,X0,X1)
| ~ l1(X1,X0) ) ).
cnf(u1813,axiom,
p1(c,c,b) ).
cnf(u5187,axiom,
( ~ m0(X1,X2,X0)
| s3(c,X0)
| ~ k1(X1) ) ).
cnf(u1764,axiom,
n1(c,X0,c) ).
cnf(u2411,axiom,
( ~ l1(X0,d)
| s4(X0) ) ).
cnf(u4057,axiom,
( ~ r2(X0)
| m3(X0,a,X0) ) ).
cnf(u2013,axiom,
p2(a,e,a) ).
cnf(u5482,axiom,
k3(X0,X0,c) ).
cnf(u2281,axiom,
p2(X0,b,X0) ).
cnf(u6872,axiom,
( ~ n0(X0,b)
| q3(b,X0) ) ).
cnf(u2414,axiom,
( ~ l1(X0,b)
| s4(X0) ) ).
cnf(u7159,axiom,
( ~ l2(d,X0)
| m3(X0,e,X0) ) ).
cnf(u1747,axiom,
m3(c,c,c) ).
cnf(u3065,axiom,
q3(e,d) ).
cnf(u2271,axiom,
q1(e,e,b) ).
cnf(u4058,axiom,
( p3(X0,c,a)
| ~ l1(X0,d) ) ).
cnf(u2017,axiom,
p2(b,a,b) ).
cnf(rule_215,axiom,
( ~ p2(X0,X1,X0)
| ~ r0(X0)
| l3(X0,X1) ) ).
cnf(u2304,axiom,
k3(e,b,e) ).
cnf(u4966,axiom,
k3(d,c,d) ).
cnf(u4994,axiom,
( ~ r2(X0)
| m3(c,c,X0) ) ).
cnf(u4064,axiom,
( p3(X0,b,a)
| ~ l1(X0,d) ) ).
cnf(u3703,axiom,
n4(X0,a) ).
cnf(u3104,axiom,
( ~ r0(X0)
| n1(X0,a,X0) ) ).
cnf(axiom_14,axiom,
p0(b,X0) ).
cnf(u6836,axiom,
( ~ k2(X0,c)
| r3(e,X0,c) ) ).
cnf(u2923,axiom,
p4(b,b,e) ).
cnf(u4097,axiom,
p3(d,e,b) ).
cnf(u4378,axiom,
( ~ m2(X0)
| m3(e,X0,X0) ) ).
cnf(rule_205,axiom,
( ~ p2(X1,X0,X0)
| k3(X0,X0,X0) ) ).
cnf(rule_231,axiom,
( ~ k2(c,X1)
| ~ r2(X0)
| m3(X0,X1,X0) ) ).
cnf(u6468,axiom,
( ~ p1(X0,X0,X1)
| ~ n1(X1,X0,X1)
| q2(X0,X1,X0)
| ~ l1(X0,X1) ) ).
cnf(u2959,axiom,
k3(e,e,b) ).
cnf(axiom_12,axiom,
m0(a,X0,a) ).
cnf(u6787,axiom,
q2(c,e,c) ).
cnf(u6622,axiom,
( ~ k2(X0,a)
| r3(c,X0,a) ) ).
cnf(u5705,axiom,
( ~ p1(X0,X1,X2)
| ~ l1(X1,X2)
| p2(X0,b,b) ) ).
cnf(u6537,axiom,
r3(b,a,a) ).
cnf(u4040,axiom,
p3(d,a,e) ).
cnf(axiom_27,axiom,
m0(e,b,c) ).
cnf(u2507,axiom,
r4(X0) ).
cnf(u4395,axiom,
m3(a,b,b) ).
cnf(u2127,axiom,
( ~ p4(X1,X0,X0)
| n5(X0,X0) ) ).
cnf(rule_244,axiom,
( ~ n2(X0)
| p3(X0,X0,X0) ) ).
cnf(u3824,axiom,
( ~ k0(X0)
| ~ l0(X1)
| q1(X1,X0,X0) ) ).
cnf(u3713,axiom,
( ~ m0(d,X0,b)
| p1(X0,X1,d) ) ).
cnf(u2324,axiom,
p2(e,b,b) ).
cnf(u4431,axiom,
( ~ p2(X0,e,b)
| p3(X0,e,e) ) ).
cnf(u6489,axiom,
( ~ n1(X0,b,b)
| q2(b,X0,b) ) ).
cnf(rule_245,axiom,
( ~ p3(X2,X2,X1)
| ~ l1(X1,X1)
| ~ l3(X1,X0)
| p3(X0,X0,X0) ) ).
cnf(rule_267,axiom,
( ~ p2(X0,X2,X1)
| r3(X0,X1,X0) ) ).
cnf(rule_251,axiom,
( ~ m3(X1,X2,X3)
| p3(X0,X1,X1)
| ~ p2(X0,X1,X3) ) ).
cnf(u6718,axiom,
p3(e,X0,X0) ).
cnf(u1814,axiom,
p1(b,b,c) ).
cnf(u5663,axiom,
( ~ m2(X0)
| r3(a,a,X0) ) ).
cnf(rule_242,axiom,
( ~ k3(X1,X2,X0)
| ~ r2(X1)
| p3(X0,X1,X2) ) ).
cnf(u2545,axiom,
m1(b,a,a) ).
cnf(u2040,axiom,
q2(b,b,b) ).
cnf(u4916,axiom,
( ~ n0(X0,c)
| k3(X0,c,X0) ) ).
cnf(rule_092,axiom,
( ~ p0(X3,X0)
| ~ n0(X2,X1)
| q1(X0,X1,X0) ) ).
cnf(u2575,axiom,
( ~ p0(X0,X0)
| n1(X0,b,X0) ) ).
cnf(u2790,axiom,
( ~ l1(X1,X0)
| ~ n0(X0,X0)
| q3(X0,X1) ) ).
cnf(u4379,axiom,
( ~ m2(X0)
| m3(d,X0,X0) ) ).
cnf(rule_002,axiom,
( ~ n0(X1,X0)
| l1(X0,X0) ) ).
cnf(u6674,axiom,
q2(e,d,e) ).
cnf(u2576,axiom,
( ~ p0(X0,X0)
| n1(X0,c,X0) ) ).
cnf(axiom_31,axiom,
m0(b,b,e) ).
cnf(u1818,axiom,
p1(X0,X0,X0) ).
cnf(u2348,axiom,
k3(c,e,c) ).
cnf(u5643,axiom,
r3(a,a,d) ).
cnf(u6283,axiom,
( ~ q2(X0,X1,X2)
| q4(X2,X1) ) ).
cnf(rule_248,axiom,
( ~ p2(X1,X0,X0)
| p3(X0,X0,X0)
| ~ n3(X0) ) ).
cnf(u1824,axiom,
m3(X0,X0,X0) ).
cnf(u4265,axiom,
( p3(X1,b,X0)
| ~ k1(X0)
| ~ l1(X1,d) ) ).
cnf(u3763,axiom,
p2(e,e,d) ).
cnf(u4377,axiom,
( ~ m2(X0)
| m3(a,X0,X0) ) ).
cnf(u1948,axiom,
( ~ l0(X0)
| m1(X0,e,X0) ) ).
cnf(u6538,axiom,
r3(e,a,a) ).
cnf(u2221,axiom,
p4(e,a,a) ).
cnf(u7177,axiom,
m3(b,a,b) ).
cnf(u6719,axiom,
p3(e,X0,d) ).
cnf(u2704,axiom,
q2(a,e,e) ).
cnf(rule_121,axiom,
( ~ m0(X1,X2,X0)
| q1(X0,X0,X0) ) ).
cnf(u1946,axiom,
m1(e,b,e) ).
cnf(u2099,axiom,
p4(c,c,c) ).
cnf(u1854,axiom,
k2(b,b) ).
cnf(u5677,axiom,
( p5(X0,X2,X2)
| ~ l2(X0,X1)
| ~ m4(X1,X2)
| ~ q4(X1,X3) ) ).
cnf(u1952,axiom,
m1(a,e,a) ).
cnf(u2365,axiom,
( l3(X0,e)
| ~ r0(X0) ) ).
cnf(u2495,axiom,
s5(X0) ).
cnf(u1925,axiom,
l2(X0,X0) ).
cnf(u5664,axiom,
( ~ m2(X0)
| r3(d,d,X0) ) ).
cnf(u6229,axiom,
q4(X0,X0) ).
cnf(u5801,axiom,
( ~ l1(X0,b)
| p2(X0,e,e) ) ).
cnf(u6203,axiom,
( ~ q2(c,X0,X1)
| q4(X1,X0) ) ).
cnf(u2982,axiom,
p4(b,d,b) ).
cnf(u7158,axiom,
( ~ m0(X0,X2,X2)
| ~ l2(X2,X0)
| m3(X0,X1,X0) ) ).
cnf(u2482,axiom,
r1(X0) ).
cnf(u4926,axiom,
( ~ n0(X0,a)
| k3(X0,b,X0) ) ).
cnf(rule_061,axiom,
( ~ k0(X0)
| n1(X0,X0,X0)
| ~ s0(X0) ) ).
cnf(u1708,axiom,
p3(a,a,a) ).
cnf(u1725,axiom,
q1(a,a,a) ).
cnf(u3512,axiom,
( ~ m0(X1,X2,X0)
| n1(X0,X0,X1) ) ).
cnf(rule_033,axiom,
( ~ m1(X2,X1,X0)
| ~ q0(X1,X1)
| m1(X0,X0,X0) ) ).
cnf(u6724,axiom,
p3(e,e,b) ).
cnf(u6971,axiom,
q2(d,c,d) ).
cnf(u5872,axiom,
( ~ r2(X0)
| m3(e,e,X0) ) ).
cnf(u3404,axiom,
( ~ m1(X0,X0,X1)
| m1(X1,X0,X0) ) ).
cnf(u4035,axiom,
( p3(X0,c,e)
| ~ l1(X0,d) ) ).
cnf(u1615,axiom,
l1(b,b) ).
cnf(rule_101,axiom,
( ~ p1(b,b,X0)
| ~ k1(X0)
| ~ q0(X0,b)
| q1(X0,X0,X0) ) ).
cnf(rule_299,axiom,
( ~ p3(X1,X2,X3)
| s4(X0)
| ~ l1(X0,X2) ) ).
cnf(u7235,axiom,
r3(e,e,d) ).
cnf(u3408,axiom,
( ~ m1(d,a,X0)
| m1(X0,a,a) ) ).
cnf(u6490,axiom,
( ~ n1(X0,e,e)
| q2(e,X0,e) ) ).
cnf(u6743,axiom,
n4(e,X0) ).
cnf(u4566,axiom,
p3(e,b,b) ).
cnf(u4965,axiom,
( ~ p2(X0,b,a)
| p3(X0,b,b) ) ).
cnf(u6843,axiom,
r3(e,e,c) ).
cnf(u4166,axiom,
m3(a,b,a) ).
cnf(u1869,axiom,
r3(b,b,b) ).
cnf(u5704,axiom,
( ~ p1(X0,X1,X2)
| ~ l1(X1,X2)
| p2(X0,a,a) ) ).
cnf(u5802,axiom,
( ~ l1(X0,X0)
| p2(X0,e,e) ) ).
cnf(u6244,axiom,
q4(d,c) ).
cnf(u4942,axiom,
( ~ n0(X0,X1)
| k3(X0,b,X0) ) ).
cnf(u4234,axiom,
( k2(b,X0)
| ~ k1(X0) ) ).
cnf(u3421,axiom,
( ~ m1(a,a,X0)
| m1(X0,a,a) ) ).
cnf(rule_170,axiom,
( ~ n1(X0,e,e)
| p2(X0,e,X0) ) ).
cnf(u5855,axiom,
r3(X0,e,X0) ).
cnf(u2921,axiom,
p4(e,e,b) ).
cnf(u4564,axiom,
p3(e,d,d) ).
cnf(u1765,axiom,
n1(a,X0,a) ).
cnf(u3854,axiom,
( ~ l0(X0)
| q1(X0,a,a) ) ).
cnf(u6239,axiom,
( ~ l1(X0,c)
| q4(X0,c) ) ).
cnf(u1746,axiom,
p3(c,c,c) ).
cnf(u3425,axiom,
( ~ m1(b,e,X0)
| m1(X0,e,e) ) ).
cnf(u5494,axiom,
p4(X0,e,X0) ).
cnf(u4044,axiom,
p4(e,a,e) ).
cnf(u5004,axiom,
( ~ p2(X0,c,a)
| p3(X0,c,c) ) ).
cnf(rule_176,axiom,
( ~ m1(X1,X0,X1)
| p2(X0,X1,X0) ) ).
cnf(u4453,axiom,
( ~ p2(X0,c,c)
| p3(X0,c,c) ) ).
cnf(u6559,axiom,
m4(X0,X1) ).
cnf(u4042,axiom,
p4(e,c,e) ).
cnf(u5147,axiom,
( ~ r2(X0)
| r3(X0,e,X0)
| ~ k1(X0) ) ).
cnf(u2523,axiom,
q1(b,b,a) ).
cnf(u2015,axiom,
p2(c,e,c) ).
cnf(u4041,axiom,
k3(e,e,a) ).
cnf(u3795,axiom,
m3(d,e,e) ).
cnf(u4712,axiom,
( ~ q0(X0,X0)
| q1(c,X0,c) ) ).
cnf(u7112,axiom,
( ~ n4(X0,c)
| n5(X0,X1) ) ).
cnf(u3674,axiom,
( ~ m0(X0,X1,a)
| p1(X1,X2,X0) ) ).
cnf(rule_059,axiom,
( ~ m0(X2,X3,X3)
| n1(X0,X0,X1)
| ~ m0(X1,X2,X0) ) ).
cnf(u2037,axiom,
q2(d,d,d) ).
cnf(u3815,axiom,
p3(c,c,d) ).
cnf(u2922,axiom,
p4(e,e,a) ).
cnf(u3697,axiom,
p3(X0,a,a) ).
cnf(rule_086,axiom,
( ~ m0(X1,X2,X0)
| ~ l0(X0)
| p1(X0,X0,X0) ) ).
cnf(rule_216,axiom,
( ~ p2(X1,X2,X0)
| ~ p1(X0,X0,X1)
| l3(X0,X0) ) ).
cnf(u5084,axiom,
( ~ l2(X2,X1)
| ~ r2(X1)
| r3(X1,X0,X1)
| ~ k2(X0,X1) ) ).
cnf(u3035,axiom,
( ~ n0(X0,X0)
| q3(X0,d) ) ).
cnf(u6064,axiom,
r3(X0,b,X0) ).
cnf(u2041,axiom,
q2(c,c,c) ).
cnf(u5648,axiom,
p4(d,a,a) ).
cnf(u3454,axiom,
m1(c,a,a) ).
cnf(u1927,axiom,
l2(c,c) ).
cnf(rule_228,axiom,
( ~ m3(X2,X0,X2)
| ~ n2(X0)
| ~ m2(X1)
| m3(X0,X1,X1) ) ).
cnf(u2308,axiom,
( ~ k0(X0)
| m1(X0,X0,e) ) ).
cnf(u2694,axiom,
( ~ k0(X0)
| q2(X1,X0,X0) ) ).
cnf(rule_128,axiom,
( ~ q1(X0,X0,d)
| ~ n1(e,d,X0)
| ~ m1(X0,e,X0)
| k2(X0,X0) ) ).
cnf(u4093,axiom,
p3(d,c,b) ).
cnf(axiom_15,axiom,
n0(a,b) ).
cnf(u2024,axiom,
p2(e,c,e) ).
cnf(axiom_36,axiom,
q0(a,b) ).
cnf(u4996,axiom,
p3(c,c,X0) ).
cnf(u4091,axiom,
( ~ r2(X0)
| m3(X0,b,X0) ) ).
cnf(u2965,axiom,
p3(b,c,c) ).
cnf(u4376,axiom,
( ~ m2(X0)
| m3(b,X0,X0) ) ).
cnf(u4104,axiom,
p4(b,c,b) ).
cnf(rule_262,axiom,
( ~ r3(X0,X1,X0)
| ~ p1(X1,X2,X0)
| ~ l2(X2,X1)
| r3(X0,X0,X0) ) ).
cnf(u2695,axiom,
( ~ k0(X0)
| q2(d,X0,X0) ) ).
cnf(u6681,axiom,
( ~ k2(X0,X1)
| p3(e,X0,X1) ) ).
cnf(rule_099,axiom,
( ~ q1(X1,X1,X2)
| ~ k0(X2)
| ~ l0(X0)
| q1(X0,X1,X1) ) ).
cnf(u2332,axiom,
p2(e,e,b) ).
cnf(u2963,axiom,
p4(c,b,c) ).
cnf(u6725,axiom,
p3(e,e,c) ).
cnf(u2330,axiom,
k3(b,e,b) ).
cnf(u4375,axiom,
( ~ m2(X0)
| m3(c,X0,X0) ) ).
cnf(u2325,axiom,
p1(e,b,e) ).
cnf(u5020,axiom,
k3(d,a,d) ).
cnf(u5015,axiom,
m3(a,a,c) ).
cnf(axiom_26,axiom,
n0(d,c) ).
cnf(u3747,axiom,
k3(b,d,b) ).
cnf(u6294,axiom,
( ~ q2(X0,X1,e)
| q4(e,X1) ) ).
cnf(rule_127,axiom,
( ~ m1(X2,X1,X0)
| k2(X0,X1)
| ~ k1(X3)
| ~ k2(X3,X1) ) ).
cnf(rule_011,axiom,
( ~ n0(X1,X1)
| ~ k0(X0)
| m1(X0,X0,X1) ) ).
cnf(rule_105,axiom,
( ~ p0(X1,d)
| ~ s0(X0)
| q1(X0,X0,X1) ) ).
cnf(u1930,axiom,
l2(e,e) ).
cnf(u2705,axiom,
q2(X0,b,b) ).
cnf(u2210,axiom,
k3(e,c,e) ).
cnf(u5275,axiom,
( ~ k2(X2,X1)
| ~ q0(X0,X1)
| k3(X2,X2,X1) ) ).
cnf(u3750,axiom,
p4(b,b,d) ).
cnf(u3893,axiom,
p1(e,X0,d) ).
cnf(rule_266,axiom,
( ~ r2(X0)
| r3(X0,X0,X0) ) ).
cnf(rule_116,axiom,
( ~ r0(X0)
| q1(X0,X0,X0) ) ).
cnf(rule_182,axiom,
( ~ q2(X1,X2,X0)
| ~ p1(X0,X0,X2)
| ~ n1(X1,X0,X2)
| q2(X0,X1,X0) ) ).
cnf(u4222,axiom,
( p3(X1,e,X0)
| ~ k1(X0)
| ~ l1(X1,d) ) ).
cnf(u4423,axiom,
( ~ p2(X0,X1,b)
| p3(X0,X1,X1) ) ).
cnf(u3103,axiom,
( ~ r0(X0)
| n1(X0,c,X0) ) ).
cnf(u3218,axiom,
p3(d,a,a) ).
cnf(u6812,axiom,
r3(c,e,e) ).
cnf(u1966,axiom,
m1(e,a,e) ).
cnf(u3133,axiom,
r3(e,b,b) ).
cnf(u2966,axiom,
p4(e,b,e) ).
cnf(rule_114,axiom,
( ~ m0(X0,X0,X1)
| q1(X0,X0,X0)
| ~ k0(X1) ) ).
cnf(u3114,axiom,
( ~ n0(e,X1)
| l2(X0,X1) ) ).
cnf(u3241,axiom,
( p3(X0,e,e)
| ~ l1(X0,d) ) ).
cnf(u1972,axiom,
n1(b,c,b) ).
cnf(u1709,axiom,
r3(d,d,d) ).
cnf(u3102,axiom,
n1(b,a,b) ).
cnf(u1970,axiom,
n1(d,c,d) ).
cnf(u1690,axiom,
k3(e,e,e) ).
cnf(rule_270,axiom,
( ~ p2(b,X0,b)
| ~ r0(X0)
| r3(X0,b,X0)
| ~ l2(X0,X0) ) ).
cnf(u1707,axiom,
p3(e,e,e) ).
cnf(u2744,axiom,
m3(e,e,a) ).
cnf(u4167,axiom,
m3(c,d,c) ).
cnf(u3766,axiom,
p2(d,X0,X0) ).
cnf(u1696,axiom,
m3(e,e,e) ).
cnf(u6723,axiom,
p3(e,e,a) ).
cnf(u3242,axiom,
( p3(X0,a,a)
| ~ l1(X0,d) ) ).
cnf(u1713,axiom,
l3(e,e) ).
cnf(u3516,axiom,
n1(X0,X0,X1) ).
cnf(u2621,axiom,
p1(d,b,b) ).
cnf(u1727,axiom,
q1(c,c,c) ).
cnf(u4918,axiom,
( ~ n0(X0,b)
| k3(X0,c,X0) ) ).
cnf(u3036,axiom,
( ~ n0(d,X0)
| n1(X0,X0,X0) ) ).
cnf(u4165,axiom,
m3(c,b,c) ).
cnf(u3392,axiom,
m1(a,a,b) ).
cnf(rule_196,axiom,
( ~ p2(X1,X2,X1)
| k3(X0,X0,X0)
| ~ m1(X0,X0,X2) ) ).
cnf(u4432,axiom,
( ~ p2(X0,e,e)
| p3(X0,e,e) ) ).
cnf(u3470,axiom,
m1(e,a,a) ).
cnf(u3256,axiom,
( ~ l1(X0,d)
| n4(X0,e) ) ).
cnf(u6951,axiom,
( q2(X0,a,X0)
| ~ l1(X0,a) ) ).
cnf(u5860,axiom,
( ~ p2(X0,X1,e)
| p3(X0,X1,X1) ) ).
cnf(u5169,axiom,
( ~ m0(X0,X2,X1)
| ~ s2(X0)
| s3(X0,X1) ) ).
cnf(u7006,axiom,
( ~ n5(e,X3)
| ~ n4(X2,X1)
| n5(X2,X3)
| ~ q4(X0,X1) ) ).
cnf(u4820,axiom,
r3(a,d,a) ).
cnf(rule_032,axiom,
( ~ s0(X0)
| m1(X0,X0,X0) ) ).
cnf(rule_154,axiom,
( ~ q1(X0,X0,X0)
| p2(X0,X0,X0) ) ).
cnf(u4973,axiom,
k3(a,b,a) ).
cnf(u2239,axiom,
p1(b,X0,b) ).
cnf(u5185,axiom,
( ~ m0(e,X1,X0)
| s3(c,X0) ) ).
cnf(u1732,axiom,
p1(d,d,d) ).
cnf(u6731,axiom,
p3(e,b,a) ).
cnf(u6319,axiom,
q4(b,e) ).
cnf(rule_287,axiom,
( ~ k3(X0,X0,X1)
| p4(X0,X1,X0) ) ).
cnf(u3904,axiom,
p4(d,e,d) ).
cnf(u4704,axiom,
p3(c,c,b) ).
cnf(u4163,axiom,
m3(c,a,c) ).
cnf(u5574,axiom,
( ~ m3(X1,b,X2)
| ~ m2(X0)
| r3(X2,X2,X0)
| ~ l2(X3,X0) ) ).
cnf(u1736,axiom,
p1(c,c,c) ).
cnf(u6234,axiom,
l5(b) ).
cnf(u3411,axiom,
( ~ m1(d,b,X0)
| m1(X0,b,b) ) ).
cnf(u5987,axiom,
( ~ r2(X0)
| m3(a,a,X0) ) ).
cnf(u6616,axiom,
r3(a,c,c) ).
cnf(u4119,axiom,
( p3(X0,b,c)
| ~ l1(X0,d) ) ).
cnf(u3779,axiom,
p4(X0,d,X0) ).
cnf(u7220,axiom,
m3(d,X0,d) ).
cnf(u3431,axiom,
( ~ m1(b,c,X0)
| m1(X0,c,c) ) ).
cnf(u6633,axiom,
p4(a,c,c) ).
cnf(rule_043,axiom,
( ~ p0(X0,X0)
| ~ k1(X0)
| n1(X0,X0,X0) ) ).
cnf(u2406,axiom,
r3(c,d,d) ).
cnf(u2021,axiom,
p2(a,b,a) ).
cnf(u4971,axiom,
k3(d,b,d) ).
cnf(u4267,axiom,
( ~ k1(X0)
| k3(X0,X0,b) ) ).
cnf(u5119,axiom,
r3(d,c,c) ).
cnf(rule_200,axiom,
( ~ k3(X0,X1,X1)
| ~ p2(X1,X2,e)
| ~ s1(X1)
| k3(X0,X0,X0) ) ).
cnf(u6555,axiom,
( ~ k2(X0,c)
| r3(a,X0,c) ) ).
cnf(u6173,axiom,
( ~ k3(X0,X0,X1)
| ~ q2(d,X2,X1)
| q4(X1,X2) ) ).
cnf(u4960,axiom,
( ~ p2(X0,b,c)
| p3(X0,b,b) ) ).
cnf(rule_085,axiom,
( ~ p0(X1,X0)
| p1(X0,X0,X0) ) ).
cnf(u4100,axiom,
p3(d,a,b) ).
cnf(rule_317,axiom,
( ~ k3(d,X0,a)
| n5(d,X0)
| ~ n4(X0,d) ) ).
cnf(u2534,axiom,
m1(d,c,c) ).
cnf(u2039,axiom,
q2(a,a,a) ).
cnf(u6315,axiom,
q4(d,X0) ).
cnf(u5388,axiom,
( ~ q0(X0,X1)
| k3(X2,X2,X1) ) ).
cnf(u3855,axiom,
( ~ l0(X0)
| q1(X0,e,e) ) ).
cnf(u5100,axiom,
( ~ k2(X0,c)
| r3(d,X0,c) ) ).
cnf(u3563,axiom,
( ~ m0(X0,X0,X0)
| p1(X0,X1,X0) ) ).
cnf(u3162,axiom,
m3(b,c,b) ).
cnf(u5990,axiom,
p3(a,a,X0) ).
cnf(u7103,axiom,
( ~ n4(X0,d)
| n5(X0,X1) ) ).
cnf(rule_083,axiom,
( ~ m1(X0,X1,b)
| p1(X0,b,X1)
| ~ k0(X1) ) ).
cnf(u2279,axiom,
m1(e,X0,e) ).
cnf(u4134,axiom,
n4(e,c) ).
cnf(u5102,axiom,
( ~ k2(X0,a)
| r3(a,X0,a) ) ).
cnf(u7157,axiom,
( ~ m0(X0,X1,X1)
| ~ l2(X1,X0)
| m3(X0,a,X0) ) ).
cnf(rule_188,axiom,
( ~ r1(X0)
| r2(X0)
| ~ l0(X0) ) ).
cnf(rule_157,axiom,
( ~ l1(X0,d)
| p2(X0,X0,X0) ) ).
cnf(u6056,axiom,
p3(X0,b,b) ).
cnf(u4462,axiom,
p3(c,e,e) ).
cnf(u6870,axiom,
q4(X0,b) ).
cnf(u4399,axiom,
m3(X0,b,b) ).
cnf(u2038,axiom,
q2(e,e,e) ).
cnf(u2439,axiom,
k5(X0) ).
cnf(u6014,axiom,
( ~ l1(X0,X0)
| p2(X0,b,b) ) ).
cnf(u2962,axiom,
k3(b,b,d) ).
cnf(axiom_33,axiom,
q0(d,c) ).
cnf(u6501,axiom,
q2(b,a,b) ).
cnf(rule_250,axiom,
( ~ q2(X1,X2,X0)
| ~ k1(X0)
| p3(X0,X0,X0) ) ).
cnf(u2703,axiom,
q2(a,b,b) ).
cnf(rule_100,axiom,
( ~ n0(X1,X0)
| q1(X0,X0,X0) ) ).
cnf(u3097,axiom,
( ~ l0(X1)
| n1(X0,X1,X0)
| ~ r0(X0) ) ).
cnf(u1828,axiom,
l4(X0) ).
cnf(u2094,axiom,
p4(X0,X0,X0) ).
cnf(u2559,axiom,
( ~ k1(X0)
| n1(X0,e,e) ) ).
cnf(u4120,axiom,
p3(d,b,c) ).
cnf(rule_001,axiom,
( ~ n0(X1,X0)
| k1(X0) ) ).
cnf(u5632,axiom,
p4(b,c,c) ).
cnf(u6292,axiom,
( ~ q2(X0,X1,c)
| q4(c,X1) ) ).
cnf(rule_256,axiom,
( ~ p2(X1,X0,X0)
| q3(X0,X0)
| ~ q3(X1,X0) ) ).
cnf(u3117,axiom,
( ~ s2(X0)
| r3(e,X0,X0) ) ).
cnf(u5115,axiom,
r3(d,e,c) ).
cnf(u3895,axiom,
( ~ m0(e,X0,d)
| p1(X0,X1,e) ) ).
cnf(u5497,axiom,
( ~ r2(X0)
| p3(e,X0,X0) ) ).
cnf(u6802,axiom,
q4(a,e) ).
cnf(u3225,axiom,
n4(d,X0) ).
cnf(u2291,axiom,
p2(b,e,e) ).
cnf(rule_278,axiom,
( ~ m0(X1,X0,X0)
| l4(X0)
| ~ l4(X1) ) ).
cnf(axiom_37,axiom,
n0(b,a) ).
cnf(u4128,axiom,
p4(c,e,c) ).
cnf(rule_129,axiom,
( ~ q1(X1,X0,X0)
| k2(X0,X0) ) ).
cnf(u2346,axiom,
r3(e,c,e) ).
cnf(u2432,axiom,
s4(d) ).
cnf(u3215,axiom,
p3(d,X0,X0) ).
cnf(u5002,axiom,
m3(c,c,a) ).
cnf(u2961,axiom,
k3(b,b,e) ).
cnf(u4204,axiom,
( k2(e,X0)
| ~ k1(X0) ) ).
cnf(u2082,axiom,
r3(a,a,a) ).
cnf(u1697,axiom,
m3(a,a,a) ).
cnf(u3474,axiom,
q1(e,e,a) ).
cnf(u3878,axiom,
q1(c,d,d) ).
cnf(u1837,axiom,
q1(b,c,c) ).
cnf(u1711,axiom,
l4(a) ).
cnf(u4914,axiom,
( ~ n0(X0,c)
| k3(X0,b,X0) ) ).
cnf(u5485,axiom,
k3(X0,X0,e) ).
cnf(u2528,axiom,
( ~ k1(X0)
| m1(d,X0,X0) ) ).
cnf(u3730,axiom,
p1(X0,d,X0) ).
cnf(u1835,axiom,
q1(X0,b,b) ).
cnf(rule_016,axiom,
( ~ m1(X2,X3,X1)
| ~ m1(X2,X1,X0)
| m1(X0,X1,X1) ) ).
cnf(u2360,axiom,
( ~ s0(X0)
| q1(X0,X0,b) ) ).
cnf(u2095,axiom,
p4(d,d,d) ).
cnf(u3132,axiom,
r3(e,d,d) ).
cnf(u5703,axiom,
( ~ p1(X0,X1,X2)
| ~ l1(X1,X2)
| p2(X0,e,e) ) ).
cnf(u5181,axiom,
( ~ m0(c,X1,X0)
| s3(c,X0) ) ).
cnf(u4426,axiom,
( ~ p2(X0,d,e)
| p3(X0,d,d) ) ).
cnf(u1965,axiom,
m1(b,a,b) ).
cnf(u3240,axiom,
( p3(X0,d,d)
| ~ l1(X0,d) ) ).
cnf(u6207,axiom,
( ~ q2(c,X0,a)
| q4(a,X0) ) ).
cnf(u1714,axiom,
l3(a,a) ).
cnf(u4223,axiom,
( p3(d,e,X0)
| ~ k1(X0) ) ).
cnf(u6212,axiom,
( ~ q2(c,X0,c)
| q4(c,X0) ) ).
cnf(u5106,axiom,
r3(b,b,c) ).
cnf(u4012,axiom,
( p3(X0,X1,d)
| ~ l1(X0,d) ) ).
cnf(u1963,axiom,
m1(b,c,b) ).
cnf(u6845,axiom,
r3(e,b,c) ).
cnf(u3143,axiom,
r3(b,d,d) ).
cnf(u6638,axiom,
q2(b,c,b) ).
cnf(u3772,axiom,
k3(d,e,d) ).
cnf(u1969,axiom,
n1(X0,X0,d) ).
cnf(u6729,axiom,
( p3(e,b,X0)
| ~ k1(X0) ) ).
cnf(rule_039,axiom,
( ~ m0(X1,X0,c)
| n1(X0,c,X0) ) ).
cnf(u1687,axiom,
p2(b,b,b) ).
cnf(u4016,axiom,
( ~ r2(X0)
| m3(X0,d,X0) ) ).
cnf(u1983,axiom,
k2(X0,X0) ).
cnf(u4948,axiom,
k3(b,c,b) ).
cnf(u6735,axiom,
p3(e,c,a) ).
cnf(u4551,axiom,
q3(d,e) ).
cnf(u4577,axiom,
n4(e,b) ).
cnf(u6810,axiom,
r3(b,e,e) ).
cnf(rule_029,axiom,
( ~ p0(X0,X1)
| m1(X0,X1,X0)
| ~ s0(X0) ) ).
cnf(u2638,axiom,
( ~ n0(X0,X1)
| q1(b,X1,b) ) ).
cnf(rule_167,axiom,
( ~ s1(X0)
| p2(X0,X0,X0)
| ~ k1(X0) ) ).
cnf(rule_313,axiom,
( ~ q4(X1,X0)
| n5(X0,X0) ) ).
cnf(u4935,axiom,
( ~ n0(X0,e)
| k3(X0,c,X0) ) ).
cnf(u5186,axiom,
( ~ m0(d,X1,X0)
| s3(d,X0) ) ).
cnf(u4991,axiom,
k3(c,X0,c) ).
cnf(u2644,axiom,
q1(X0,b,X0) ).
cnf(u1750,axiom,
l4(c) ).
cnf(u6231,axiom,
l5(d) ).
cnf(u4697,axiom,
k3(c,b,c) ).
cnf(u3523,axiom,
n1(a,a,c) ).
cnf(u6232,axiom,
l5(e) ).
cnf(u6187,axiom,
( ~ k3(X0,X0,X1)
| ~ q2(c,X2,X1)
| q4(X1,X2) ) ).
cnf(u5624,axiom,
r3(d,d,b) ).
cnf(u4936,axiom,
( ~ n0(X0,e)
| k3(X0,a,X0) ) ).
cnf(u5628,axiom,
p4(b,a,a) ).
cnf(rule_054,axiom,
( ~ n1(X0,X1,X0)
| ~ l0(X2)
| ~ l1(X2,X0)
| n1(X0,X1,X1) ) ).
cnf(rule_184,axiom,
( ~ q1(X1,c,X0)
| q2(X0,X0,X0) ) ).
cnf(u3789,axiom,
( ~ q3(d,X0)
| q3(X0,X0) ) ).
cnf(u2248,axiom,
p1(b,c,b) ).
cnf(u1853,axiom,
k2(c,c) ).
cnf(u2009,axiom,
p2(d,X0,d) ).
cnf(u2668,axiom,
( l3(X0,a)
| ~ r0(X0) ) ).
cnf(rule_069,axiom,
( ~ p0(X1,X0)
| p1(X0,X0,X1) ) ).
cnf(u6287,axiom,
( ~ q2(X0,X1,a)
| q4(a,X1) ) ).
cnf(u3787,axiom,
r3(d,X0,d) ).
cnf(u3422,axiom,
( ~ m1(a,b,X0)
| m1(X0,b,b) ) ).
cnf(u4062,axiom,
p3(d,e,a) ).
cnf(u2023,axiom,
p2(b,c,b) ).
cnf(rule_044,axiom,
( ~ p0(X1,X2)
| ~ p0(X0,X0)
| n1(X0,X1,X0) ) ).
cnf(u4259,axiom,
p3(d,b,e) ).
cnf(u1950,axiom,
m1(a,b,a) ).
cnf(u3426,axiom,
( ~ m1(b,a,X0)
| m1(X0,a,a) ) ).
cnf(rule_067,axiom,
( ~ q0(X1,X0)
| p1(X0,X0,X0) ) ).
cnf(u5679,axiom,
( p5(b,X0,X0)
| ~ m4(b,X0) ) ).
cnf(u2277,axiom,
( ~ r0(X0)
| m1(X0,b,X0) ) ).
cnf(u5206,axiom,
( s3(X0,X1)
| ~ s2(X0) ) ).
cnf(u5623,axiom,
r3(a,a,b) ).
cnf(u2532,axiom,
m1(d,a,a) ).
cnf(u4987,axiom,
p3(a,a,e) ).
cnf(u4061,axiom,
( p3(X0,e,a)
| ~ l1(X0,d) ) ).
cnf(u2791,axiom,
( ~ n0(X0,X0)
| q3(X0,X0) ) ).
cnf(u1585,axiom,
s1(X0) ).
cnf(u4059,axiom,
p3(d,c,a) ).
cnf(u2278,axiom,
m1(b,X0,b) ).
cnf(u5613,axiom,
( ~ m3(X0,b,X1)
| r3(X1,X1,d) ) ).
cnf(u2551,axiom,
q1(b,b,c) ).
cnf(rule_273,axiom,
( ~ q2(X2,X0,X2)
| s3(X0,X1)
| ~ s2(X0)
| ~ m0(X2,X3,X1) ) ).
cnf(u4065,axiom,
p3(d,b,a) ).
cnf(u5071,axiom,
n4(c,b) ).
cnf(u4478,axiom,
( ~ q3(a,X0)
| ~ s2(X0)
| q3(X0,a) ) ).
cnf(u2301,axiom,
m3(b,e,e) ).
cnf(u2319,axiom,
( ~ k0(X0)
| p1(c,c,X0) ) ).
cnf(u6514,axiom,
q4(e,a) ).
cnf(u3718,axiom,
p1(d,X0,X1) ).
cnf(u2079,axiom,
r3(e,e,e) ).
cnf(u5136,axiom,
p4(b,b,c) ).
cnf(u4161,axiom,
m3(c,e,c) ).
cnf(u2549,axiom,
q1(b,b,e) ).
cnf(rule_082,axiom,
( ~ p1(X2,X0,X3)
| ~ m0(X2,X0,X3)
| p1(X0,X1,X2) ) ).
cnf(u6169,axiom,
( ~ k3(X0,X0,X1)
| ~ q2(X2,X3,X1)
| q4(X1,X3) ) ).
cnf(rule_212,axiom,
( ~ m2(X0)
| k3(X0,X0,X0) ) ).
cnf(u6785,axiom,
q2(X0,e,X0) ).
cnf(u1812,axiom,
p1(X0,X0,b) ).
cnf(rule_179,axiom,
( ~ n1(X0,X0,X1)
| ~ k1(X1)
| q2(X0,X0,X0) ) ).
cnf(u2317,axiom,
( ~ k0(X0)
| p1(e,e,X0) ) ).
cnf(u7236,axiom,
r3(e,e,b) ).
cnf(axiom_23,axiom,
m0(a,e,e) ).
cnf(u5101,axiom,
( ~ k2(X0,c)
| r3(c,X0,c) ) ).
cnf(u6629,axiom,
r3(c,c,a) ).
cnf(u4175,axiom,
~ l1(b,d) ).
cnf(rule_240,axiom,
( ~ p2(X1,X2,X0)
| n3(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN720-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.17 % Computer : n017.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Mon Sep 28 16:44:21 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.21 Running first-order theorem proving
% 0.07/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.08/1.65 % (3697634)Input is clausal, will run a generic CNF schedule.
% 6.08/1.65 % (3697734)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2763407789:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.08/1.65 % (3697740)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3822083232:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.08/1.65 % (3697741)dis-21_1_sil=8000:lcm=predicate:random_seed=3194453284:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 6.08/1.65 % (3697735)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1686605272:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.08/1.65 % (3697738)lrs+10_1_sil=8000:sp=occurrence:random_seed=1177597633:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.08/1.65 % (3697738)Refutation not found, incomplete strategy
% 6.08/1.65 % (3697738)------------------------------
% 6.08/1.65 % (3697738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.08/1.65 % (3697738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.08/1.65 % (3697738)CaDiCaL version: 2.1.3
% 6.08/1.65 % (3697738)Termination reason: Refutation not found, incomplete strategy
% 6.08/1.65 % (3697738)Time elapsed: 0.001 s
% 6.08/1.65 % (3697738)Peak memory usage: 86 MB
% 6.08/1.65 % (3697738)Instructions burned: 1 (million)
% 6.08/1.65 % (3697741)Refutation not found, incomplete strategy
% 6.08/1.65 % (3697741)------------------------------
% 6.08/1.65 % (3697741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.08/1.65 % (3697741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.08/1.65 % (3697741)CaDiCaL version: 2.1.3
% 6.08/1.65 % (3697741)Termination reason: Refutation not found, incomplete strategy
% 6.08/1.65 % (3697741)Time elapsed: 0.001 s
% 6.08/1.65 % (3697741)Peak memory usage: 86 MB
% 6.08/1.65 % (3697741)Instructions burned: 1 (million)
% 6.08/1.65 % (3697739)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4120219027:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.08/1.65 % (3697739)Refutation not found, incomplete strategy
% 6.08/1.65 % (3697739)------------------------------
% 6.08/1.65 % (3697739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.08/1.65 % (3697739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.08/1.65 % (3697739)CaDiCaL version: 2.1.3
% 6.08/1.65 % (3697739)Termination reason: Refutation not found, incomplete strategy
% 6.08/1.65 % (3697739)Time elapsed: 0.001 s
% 6.08/1.65 % (3697739)Peak memory usage: 86 MB
% 6.08/1.65 % (3697739)Instructions burned: 1 (million)
% 6.08/1.65 % (3697732)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=3944364208:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.08/1.65 % (3697740)Refutation not found, incomplete strategy
% 6.08/1.65 % (3697740)------------------------------
% 6.08/1.65 % (3697740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.08/1.65 % (3697740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.08/1.65 % (3697740)CaDiCaL version: 2.1.3
% 6.08/1.65 % (3697740)Termination reason: Refutation not found, incomplete strategy
% 6.08/1.65 % (3697740)Time elapsed: 0.051 s
% 6.08/1.65 % (3697740)Peak memory usage: 89 MB
% 6.08/1.65 % (3697740)Instructions burned: 62 (million)
% 6.08/1.65 % (3697741)------------------------------
% 6.08/1.65 % (3697741)------------------------------
% 6.08/1.65 % (3697738)------------------------------
% 6.08/1.65 % (3697738)------------------------------
% 6.08/1.65 % (3697739)------------------------------
% 6.08/1.65 % (3697739)------------------------------
% 6.08/1.65 % (3697740)------------------------------
% 6.08/1.65 % (3697740)------------------------------
% 6.08/1.65 % (3697816)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3721779461:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 6.08/1.65 % (3697816)Refutation not found, incomplete strategy
% 6.08/1.65 % (3697816)------------------------------
% 6.08/1.65 % (3697816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.08/1.65 % (3697816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.08/1.65 % (3697816)CaDiCaL version: 2.1.3
% 6.08/1.65 % (3697816)Termination reason: Refutation not found, incomplete strategy
% 6.08/1.65 % (3697816)Time elapsed: 0.001 s
% 6.08/1.65 % (3697816)Peak memory usage: 86 MB
% 6.08/1.65 % (3697816)Instructions burned: 2 (million)
% 6.08/1.65 % (3697814)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=4116101208:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 6.08/1.65 % (3697814)Refutation not found, incomplete strategy
% 6.08/1.65 % (3697814)------------------------------
% 6.08/1.65 % (3697814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.08/1.65 % (3697814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.08/1.65 % (3697814)CaDiCaL version: 2.1.3
% 6.08/1.65 % (3697814)Termination reason: Refutation not found, incomplete strategy
% 6.08/1.65 % (3697814)Time elapsed: 0.001 s
% 6.08/1.65 % (3697814)Peak memory usage: 86 MB
% 6.08/1.65 % (3697814)Instructions burned: 1 (million)
% 6.08/1.65 % (3697817)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3718830043:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 6.08/1.65 % (3697817)Refutation not found, incomplete strategy
% 6.08/1.65 % (3697817)------------------------------
% 6.08/1.65 % (3697817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.08/1.65 % (3697817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.08/1.65 % (3697817)CaDiCaL version: 2.1.3
% 6.08/1.65 % (3697817)Termination reason: Refutation not found, incomplete strategy
% 6.08/1.65 % (3697817)Time elapsed: 0.001 s
% 6.08/1.65 % (3697817)Peak memory usage: 86 MB
% 6.08/1.65 % (3697817)Instructions burned: 1 (million)
% 6.08/1.65 % (3697836)lrs+10_64_to=lpo:sil=8000:random_seed=1776976108:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 6.08/1.65 % (3697816)------------------------------
% 6.08/1.65 % (3697816)------------------------------
% 6.08/1.65 % (3697836)First to succeed.
% 6.08/1.65 % (3697836)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3697634"
% 6.08/1.65 % (3697734)Refutation not found, incomplete strategy
% 6.08/1.65 % (3697734)------------------------------
% 6.08/1.65 % (3697734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.08/1.65 % (3697734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.08/1.65 % (3697734)CaDiCaL version: 2.1.3
% 6.08/1.65 % (3697734)Termination reason: Refutation not found, incomplete strategy
% 6.08/1.65 % (3697734)Time elapsed: 0.677 s
% 6.08/1.65 % (3697734)Peak memory usage: 131 MB
% 6.08/1.65 % (3697734)Instructions burned: 1314 (million)
% 6.08/1.65 % (3697911)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1856874817:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 6.08/1.65 % (3697814)------------------------------
% 6.08/1.65 % (3697814)------------------------------
% 6.08/1.65 % (3697817)------------------------------
% 6.08/1.65 % (3697817)------------------------------
% 6.08/1.65 % (3697911)Refutation not found, incomplete strategy
% 6.08/1.65 % (3697911)------------------------------
% 6.08/1.65 % (3697911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.08/1.65 % (3697911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.08/1.65 % (3697911)CaDiCaL version: 2.1.3
% 6.08/1.65 % (3697911)Termination reason: Refutation not found, incomplete strategy
% 6.08/1.65 % (3697911)Time elapsed: 0.027 s
% 6.08/1.65 % (3697911)Peak memory usage: 89 MB
% 6.08/1.65 % (3697911)Instructions burned: 70 (million)
% 6.08/1.65 % SZS status Satisfiable for theBenchmark
% 6.08/1.65 % SZS output start Saturation.
% See solution above
% 7.35/1.75 % SZS output start Definitions and Model Updates.
% 7.35/1.75 for all inputs,
% 7.35/1.75 define m5(X0,X1) := $true
% 7.35/1.75 for all inputs,
% 7.35/1.75 define q5(X0,X1) := $true
% 7.35/1.75 for all inputs,
% 7.35/1.75 define r5(X0,X1) := $true
% 7.35/1.75 % SZS output end Definitions and Model Updates.
% 7.35/1.75 % (3697836)------------------------------
% 7.35/1.75 % (3697836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.35/1.75 % (3697836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.35/1.75 % (3697836)CaDiCaL version: 2.1.3
% 7.35/1.75 % (3697836)Termination reason: Satisfiable
% 7.35/1.75 % (3697836)Time elapsed: 0.078 s
% 7.35/1.75 % (3697836)Peak memory usage: 90 MB
% 7.35/1.75 % (3697836)Instructions burned: 113 (million)
% 7.35/1.75 % (3697836)------------------------------
% 7.35/1.75 % (3697836)------------------------------
% 7.35/1.75 % (3697634)Success in time 0.981 s
% 7.35/1.75 % Vampire exiting
%------------------------------------------------------------------------------