%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN720-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:48:43 EDT 2024
% Result : Satisfiable 2.62s 2.82s
% Output : Saturation 2.62s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(rule_243,axiom,
( p3(X814,d,e)
| ~ l3(b,e)
| ~ p2(d,b,c)
| ~ n3(X814)
| ~ q2(X814,d,X814) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_243) ).
cnf(axiom_14,axiom,
p0(b,X2),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_14) ).
cnf(rule_085,axiom,
( p1(X103,X103,X103)
| ~ p0(X102,X103) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_085) ).
cnf(c129,plain,
p1(X104,X104,X104),
inference(resolution,[status(thm)],[rule_085,axiom_14]) ).
cnf(axiom_34,axiom,
n0(c,d),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_34) ).
cnf(rule_001,axiom,
( k1(X7)
| ~ n0(X8,X7) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_001) ).
cnf(c5,plain,
k1(d),
inference(resolution,[status(thm)],[rule_001,axiom_34]) ).
cnf(axiom_19,axiom,
m0(X5,d,X4),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_19) ).
cnf(rule_040,axiom,
( n1(X161,e,e)
| ~ m0(X161,X162,e)
| ~ k1(X161) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_040) ).
cnf(c199,plain,
( n1(X284,e,e)
| ~ k1(X284) ),
inference(resolution,[status(thm)],[rule_040,axiom_19]) ).
cnf(c331,plain,
n1(d,e,e),
inference(resolution,[status(thm)],[c199,c5]) ).
cnf(axiom_28,axiom,
k0(e),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_28) ).
cnf(rule_177,axiom,
( q2(X511,X510,X510)
| ~ k0(X510)
| ~ p1(X511,X511,X511) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_177) ).
cnf(c523,plain,
( q2(X513,X512,X512)
| ~ k0(X512) ),
inference(resolution,[status(thm)],[rule_177,c129]) ).
cnf(c526,plain,
q2(X514,e,e),
inference(resolution,[status(thm)],[c523,axiom_28]) ).
cnf(rule_182,axiom,
( q2(X663,X661,X663)
| ~ p1(X663,X663,X662)
| ~ n1(X661,X663,X662)
| ~ q2(X661,X662,X663) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_182) ).
cnf(c754,plain,
( q2(e,X1479,e)
| ~ p1(e,e,e)
| ~ n1(X1479,e,e) ),
inference(resolution,[status(thm)],[rule_182,c526]) ).
cnf(c1962,plain,
( q2(e,d,e)
| ~ p1(e,e,e) ),
inference(resolution,[status(thm)],[c754,c331]) ).
cnf(c2247,plain,
q2(e,d,e),
inference(resolution,[status(thm)],[c1962,c129]) ).
cnf(c2249,plain,
( p3(e,d,e)
| ~ l3(b,e)
| ~ p2(d,b,c)
| ~ n3(e) ),
inference(resolution,[status(thm)],[c2247,rule_243]) ).
cnf(rule_125,axiom,
( s1(X9)
| ~ p0(X9,X9) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_125) ).
cnf(c8,plain,
s1(b),
inference(resolution,[status(thm)],[rule_125,axiom_14]) ).
cnf(axiom_17,axiom,
q0(X3,d),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_17) ).
cnf(rule_126,axiom,
( s1(X182)
| ~ q0(X182,X180)
| ~ s1(X181) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_126) ).
cnf(c220,plain,
( s1(X183)
| ~ s1(X184) ),
inference(resolution,[status(thm)],[rule_126,axiom_17]) ).
cnf(c223,plain,
s1(X185),
inference(resolution,[status(thm)],[c220,c8]) ).
cnf(axiom_11,axiom,
n0(e,b),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_11) ).
cnf(rule_131,axiom,
( l2(X537,X536)
| ~ s1(X537)
| ~ n0(e,X536)
| ~ l2(X536,X536) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_131) ).
cnf(rule_133,axiom,
( l2(X545,X545)
| ~ p0(X542,X542)
| ~ s1(X544)
| ~ m0(X543,X544,X545) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_133) ).
cnf(c571,plain,
( l2(X564,X564)
| ~ p0(X563,X563)
| ~ s1(d) ),
inference(resolution,[status(thm)],[rule_133,axiom_19]) ).
cnf(c632,plain,
( l2(X565,X565)
| ~ s1(d) ),
inference(resolution,[status(thm)],[c571,axiom_14]) ).
cnf(c633,plain,
l2(X566,X566),
inference(resolution,[status(thm)],[c632,c223]) ).
cnf(c635,plain,
( l2(X580,X579)
| ~ s1(X580)
| ~ n0(e,X579) ),
inference(resolution,[status(thm)],[c633,rule_131]) ).
cnf(c648,plain,
( l2(X581,b)
| ~ s1(X581) ),
inference(resolution,[status(thm)],[c635,axiom_11]) ).
cnf(c650,plain,
l2(X582,b),
inference(resolution,[status(thm)],[c648,c223]) ).
cnf(rule_168,axiom,
( p2(a,c,b)
| ~ l1(e,c)
| ~ l2(e,b)
| ~ r1(e)
| ~ m1(d,a,c) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_168) ).
cnf(axiom_33,axiom,
q0(d,c),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_33) ).
cnf(axiom_12,axiom,
m0(a,X6,a),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_12) ).
cnf(rule_006,axiom,
( m1(X37,X37,X37)
| ~ m0(X36,X36,X37) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_006) ).
cnf(c50,plain,
m1(X38,X38,X38),
inference(resolution,[status(thm)],[rule_006,axiom_19]) ).
cnf(rule_024,axiom,
( m1(X101,a,X99)
| ~ m0(a,X100,a)
| ~ q0(X101,X99)
| ~ m1(X99,c,X99) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_024) ).
cnf(c126,plain,
( m1(X1141,a,c)
| ~ m0(a,X1142,a)
| ~ q0(X1141,c) ),
inference(resolution,[status(thm)],[rule_024,c50]) ).
cnf(c1394,plain,
( m1(X1144,a,c)
| ~ q0(X1144,c) ),
inference(resolution,[status(thm)],[c126,axiom_12]) ).
cnf(c1396,plain,
m1(d,a,c),
inference(resolution,[status(thm)],[c1394,axiom_33]) ).
cnf(c1399,plain,
( p2(a,c,b)
| ~ l1(e,c)
| ~ l2(e,b)
| ~ r1(e) ),
inference(resolution,[status(thm)],[c1396,rule_168]) ).
cnf(c2348,plain,
( p2(a,c,b)
| ~ l1(e,c)
| ~ r1(e) ),
inference(resolution,[status(thm)],[c1399,c650]) ).
cnf(rule_210,axiom,
( k3(X39,X39,X39)
| ~ n2(X39) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_210) ).
cnf(rule_137,axiom,
( n2(X32)
| ~ p1(X34,X33,X32) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_137) ).
cnf(c130,plain,
n2(X105),
inference(resolution,[status(thm)],[c129,rule_137]) ).
cnf(c133,plain,
k3(X113,X113,X113),
inference(resolution,[status(thm)],[c130,rule_210]) ).
cnf(rule_287,axiom,
( p4(X251,X250,X251)
| ~ k3(X251,X251,X250) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_287) ).
cnf(c296,plain,
p4(X252,X252,X252),
inference(resolution,[status(thm)],[rule_287,c133]) ).
cnf(rule_288,axiom,
( p4(X938,X939,X939)
| ~ r3(X939,X939,X938)
| ~ p4(X940,X940,X937) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_288) ).
cnf(c1193,plain,
( p4(X943,X942,X942)
| ~ r3(X942,X942,X943) ),
inference(resolution,[status(thm)],[rule_288,c296]) ).
cnf(axiom_7,axiom,
n0(d,b),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_7) ).
cnf(c1,plain,
k1(b),
inference(resolution,[status(thm)],[rule_001,axiom_7]) ).
cnf(rule_136,axiom,
( m2(b)
| ~ k1(b) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_136) ).
cnf(c43,plain,
m2(b),
inference(resolution,[status(thm)],[rule_136,c1]) ).
cnf(rule_129,axiom,
( k2(X127,X127)
| ~ q1(X126,X127,X127) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_129) ).
cnf(rule_110,axiom,
( q1(X164,X164,X164)
| ~ m0(X163,X165,X164) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_110) ).
cnf(c208,plain,
q1(X166,X166,X166),
inference(resolution,[status(thm)],[rule_110,axiom_19]) ).
cnf(c211,plain,
k2(X167,X167),
inference(resolution,[status(thm)],[c208,rule_129]) ).
cnf(axiom_1,axiom,
s0(d),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_1) ).
cnf(axiom_9,axiom,
r0(b),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_9) ).
cnf(axiom_20,axiom,
l0(a),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_20) ).
cnf(rule_015,axiom,
( m1(X77,X76,X76)
| ~ l0(X78)
| ~ m0(X76,X76,X77) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_015) ).
cnf(c75,plain,
( m1(X269,d,d)
| ~ l0(X268) ),
inference(resolution,[status(thm)],[rule_015,axiom_19]) ).
cnf(c309,plain,
m1(X270,d,d),
inference(resolution,[status(thm)],[c75,axiom_20]) ).
cnf(rule_113,axiom,
( q1(X477,X477,X478)
| ~ r0(X479)
| ~ m1(X477,X478,X478) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_113) ).
cnf(c503,plain,
( q1(X483,X483,d)
| ~ r0(X484) ),
inference(resolution,[status(thm)],[rule_113,c309]) ).
cnf(c505,plain,
q1(X485,X485,d),
inference(resolution,[status(thm)],[c503,axiom_9]) ).
cnf(rule_124,axiom,
( r1(X516)
| ~ q0(X516,X515)
| ~ s0(d)
| ~ q1(d,X515,d) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_124) ).
cnf(c528,plain,
( r1(X521)
| ~ q0(X521,d)
| ~ s0(d) ),
inference(resolution,[status(thm)],[rule_124,c505]) ).
cnf(c535,plain,
( r1(X526)
| ~ s0(d) ),
inference(resolution,[status(thm)],[c528,axiom_17]) ).
cnf(c547,plain,
r1(X527),
inference(resolution,[status(thm)],[c535,axiom_1]) ).
cnf(rule_181,axiom,
( q2(X229,X229,X229)
| ~ p1(X229,X229,X229) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_181) ).
cnf(c272,plain,
q2(X230,X230,X230),
inference(resolution,[status(thm)],[rule_181,c129]) ).
cnf(rule_187,axiom,
( q2(X680,X683,X680)
| ~ r1(X683)
| ~ m0(X682,X681,X680)
| ~ k0(X683)
| ~ q2(X683,X683,X683) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_187) ).
cnf(c770,plain,
( q2(X1492,X1493,X1492)
| ~ r1(X1493)
| ~ m0(X1494,X1495,X1492)
| ~ k0(X1493) ),
inference(resolution,[status(thm)],[rule_187,c272]) ).
cnf(c1976,plain,
( q2(X1497,X1496,X1497)
| ~ r1(X1496)
| ~ k0(X1496) ),
inference(resolution,[status(thm)],[c770,axiom_19]) ).
cnf(c1979,plain,
( q2(X1498,e,X1498)
| ~ r1(e) ),
inference(resolution,[status(thm)],[c1976,axiom_28]) ).
cnf(c1981,plain,
q2(X1499,e,X1499),
inference(resolution,[status(thm)],[c1979,c547]) ).
cnf(rule_236,axiom,
( m3(X41,X41,X41)
| ~ n2(X41) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_236) ).
cnf(c131,plain,
m3(X109,X109,X109),
inference(resolution,[status(thm)],[c130,rule_236]) ).
cnf(rule_228,axiom,
( m3(X768,X766,X766)
| ~ n2(X768)
| ~ m2(X766)
| ~ m3(X767,X768,X767) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_228) ).
cnf(c947,plain,
( m3(X770,X769,X769)
| ~ n2(X770)
| ~ m2(X769) ),
inference(resolution,[status(thm)],[rule_228,c131]) ).
cnf(c949,plain,
( m3(X771,b,b)
| ~ n2(X771) ),
inference(resolution,[status(thm)],[c947,c43]) ).
cnf(c951,plain,
m3(X772,b,b),
inference(resolution,[status(thm)],[c949,c130]) ).
cnf(rule_269,axiom,
( r3(a,a,e)
| ~ k2(a,a)
| ~ q2(X887,e,X887)
| ~ m2(b)
| ~ m3(a,X887,X887) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_269) ).
cnf(c1112,plain,
( r3(a,a,e)
| ~ k2(a,a)
| ~ q2(b,e,b)
| ~ m2(b) ),
inference(resolution,[status(thm)],[rule_269,c951]) ).
cnf(c2193,plain,
( r3(a,a,e)
| ~ k2(a,a)
| ~ m2(b) ),
inference(resolution,[status(thm)],[c1112,c1981]) ).
cnf(c2379,plain,
( r3(a,a,e)
| ~ m2(b) ),
inference(resolution,[status(thm)],[c2193,c211]) ).
cnf(c2380,plain,
r3(a,a,e),
inference(resolution,[status(thm)],[c2379,c43]) ).
cnf(c2381,plain,
p4(e,a,a),
inference(resolution,[status(thm)],[c2380,c1193]) ).
cnf(rule_192,axiom,
( k3(X691,X688,X691)
| ~ s1(X688)
| ~ p2(X690,X688,X689)
| ~ n0(X691,X689) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_192) ).
cnf(axiom_13,axiom,
r0(e),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_13) ).
cnf(axiom_37,axiom,
n0(b,a),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_37) ).
cnf(c6,plain,
k1(a),
inference(resolution,[status(thm)],[rule_001,axiom_37]) ).
cnf(rule_127,axiom,
( k2(X522,X525)
| ~ m1(X524,X525,X522)
| ~ k1(X523)
| ~ k2(X523,X525) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_127) ).
cnf(c1397,plain,
( k2(c,a)
| ~ k1(X1605)
| ~ k2(X1605,a) ),
inference(resolution,[status(thm)],[c1396,rule_127]) ).
cnf(c2079,plain,
( k2(c,a)
| ~ k1(a) ),
inference(resolution,[status(thm)],[c1397,c211]) ).
cnf(c2082,plain,
k2(c,a),
inference(resolution,[status(thm)],[c2079,c6]) ).
cnf(rule_144,axiom,
( p2(b,c,a)
| ~ r0(e)
| ~ n1(c,X556,X556)
| ~ p0(b,X556)
| ~ k2(c,a) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_144) ).
cnf(axiom_24,axiom,
l0(c),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_24) ).
cnf(axiom_26,axiom,
n0(d,c),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_26) ).
cnf(rule_002,axiom,
( l1(X15,X15)
| ~ n0(X16,X15) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_002) ).
cnf(c9,plain,
l1(c,c),
inference(resolution,[status(thm)],[rule_002,axiom_26]) ).
cnf(rule_054,axiom,
( n1(X249,X248,X248)
| ~ l0(X247)
| ~ l1(X247,X249)
| ~ n1(X249,X248,X249) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_054) ).
cnf(axiom_5,axiom,
s0(b),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_5) ).
cnf(rule_050,axiom,
( n1(X224,X223,X224)
| ~ s0(b)
| ~ l0(X224)
| ~ p0(b,X223) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_050) ).
cnf(c262,plain,
( n1(X475,X474,X475)
| ~ s0(b)
| ~ l0(X475) ),
inference(resolution,[status(thm)],[rule_050,axiom_14]) ).
cnf(c496,plain,
( n1(c,X489,c)
| ~ s0(b) ),
inference(resolution,[status(thm)],[c262,axiom_24]) ).
cnf(c508,plain,
n1(c,X490,c),
inference(resolution,[status(thm)],[c496,axiom_5]) ).
cnf(c510,plain,
( n1(c,X1182,X1182)
| ~ l0(X1181)
| ~ l1(X1181,c) ),
inference(resolution,[status(thm)],[c508,rule_054]) ).
cnf(c1420,plain,
( n1(c,X1183,X1183)
| ~ l0(c) ),
inference(resolution,[status(thm)],[c510,c9]) ).
cnf(c1422,plain,
n1(c,X1184,X1184),
inference(resolution,[status(thm)],[c1420,axiom_24]) ).
cnf(c1423,plain,
( p2(b,c,a)
| ~ r0(e)
| ~ p0(b,X1953)
| ~ k2(c,a) ),
inference(resolution,[status(thm)],[c1422,rule_144]) ).
cnf(c2355,plain,
( p2(b,c,a)
| ~ r0(e)
| ~ p0(b,X1972) ),
inference(resolution,[status(thm)],[c1423,c2082]) ).
cnf(c2373,plain,
( p2(b,c,a)
| ~ r0(e) ),
inference(resolution,[status(thm)],[c2355,axiom_14]) ).
cnf(c2374,plain,
p2(b,c,a),
inference(resolution,[status(thm)],[c2373,axiom_13]) ).
cnf(c2375,plain,
( k3(X1973,c,X1973)
| ~ s1(c)
| ~ n0(X1973,a) ),
inference(resolution,[status(thm)],[c2374,rule_192]) ).
cnf(rule_135,axiom,
( m2(X197)
| ~ s0(X197)
| ~ l1(X195,X196) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_135) ).
cnf(c228,plain,
( m2(X198)
| ~ s0(X198) ),
inference(resolution,[status(thm)],[rule_135,c9]) ).
cnf(c233,plain,
m2(d),
inference(resolution,[status(thm)],[c228,axiom_1]) ).
cnf(rule_003,axiom,
( l1(X17,X20)
| ~ p0(X19,X17)
| ~ r0(X18)
| ~ m0(X20,X17,X19) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_003) ).
cnf(c22,plain,
( l1(d,X725)
| ~ p0(X727,d)
| ~ r0(X726) ),
inference(resolution,[status(thm)],[rule_003,axiom_19]) ).
cnf(c869,plain,
( l1(d,X728)
| ~ r0(X729) ),
inference(resolution,[status(thm)],[c22,axiom_14]) ).
cnf(c870,plain,
l1(d,X730),
inference(resolution,[status(thm)],[c869,axiom_9]) ).
cnf(rule_230,axiom,
( m3(c,b,d)
| ~ l1(d,b)
| ~ m2(d)
| ~ q2(b,c,d) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_230) ).
cnf(rule_183,axiom,
( q2(X669,c,X668)
| ~ k1(X668)
| ~ l0(c)
| ~ l2(X668,X669) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_183) ).
cnf(c763,plain,
( q2(b,c,X1233)
| ~ k1(X1233)
| ~ l0(c) ),
inference(resolution,[status(thm)],[rule_183,c650]) ).
cnf(c1508,plain,
( q2(b,c,X1234)
| ~ k1(X1234) ),
inference(resolution,[status(thm)],[c763,axiom_24]) ).
cnf(c1509,plain,
q2(b,c,d),
inference(resolution,[status(thm)],[c1508,c5]) ).
cnf(c1514,plain,
( m3(c,b,d)
| ~ l1(d,b)
| ~ m2(d) ),
inference(resolution,[status(thm)],[c1509,rule_230]) ).
cnf(c2370,plain,
( m3(c,b,d)
| ~ m2(d) ),
inference(resolution,[status(thm)],[c1514,c870]) ).
cnf(c2371,plain,
m3(c,b,d),
inference(resolution,[status(thm)],[c2370,c233]) ).
cnf(rule_190,axiom,
( s2(d)
| ~ s1(a)
| ~ s0(d) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_190) ).
cnf(c386,plain,
( s2(d)
| ~ s1(a) ),
inference(resolution,[status(thm)],[rule_190,axiom_1]) ).
cnf(c387,plain,
s2(d),
inference(resolution,[status(thm)],[c386,c223]) ).
cnf(rule_225,axiom,
( m3(X755,X752,X755)
| ~ m0(X754,X754,X752)
| ~ l2(X753,X755)
| ~ m0(X755,X753,X753)
| ~ s2(X754) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_225) ).
cnf(c924,plain,
( m3(a,X1638,a)
| ~ m0(X1639,X1639,X1638)
| ~ l2(a,a)
| ~ s2(X1639) ),
inference(resolution,[status(thm)],[rule_225,axiom_12]) ).
cnf(c2115,plain,
( m3(a,X1966,a)
| ~ l2(a,a)
| ~ s2(d) ),
inference(resolution,[status(thm)],[c924,axiom_19]) ).
cnf(c2365,plain,
( m3(a,X1967,a)
| ~ s2(d) ),
inference(resolution,[status(thm)],[c2115,c633]) ).
cnf(c2366,plain,
m3(a,X1968,a),
inference(resolution,[status(thm)],[c2365,c387]) ).
cnf(rule_188,axiom,
( r2(X138)
| ~ r1(X138)
| ~ l0(X138) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_188) ).
cnf(c172,plain,
( r2(a)
| ~ r1(a) ),
inference(resolution,[status(thm)],[rule_188,axiom_20]) ).
cnf(c549,plain,
r2(a),
inference(resolution,[status(thm)],[c547,c172]) ).
cnf(rule_007,axiom,
( m1(X45,X46,X45)
| ~ p0(X47,X46)
| ~ r0(X45) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_007) ).
cnf(c54,plain,
( m1(X72,X73,X72)
| ~ r0(X72) ),
inference(resolution,[status(thm)],[rule_007,axiom_14]) ).
cnf(c72,plain,
m1(e,X75,e),
inference(resolution,[status(thm)],[c54,axiom_13]) ).
cnf(c538,plain,
( k2(e,X550)
| ~ k1(X549)
| ~ k2(X549,X550) ),
inference(resolution,[status(thm)],[rule_127,c72]) ).
cnf(c586,plain,
( k2(e,X551)
| ~ k1(X551) ),
inference(resolution,[status(thm)],[c538,c211]) ).
cnf(c592,plain,
k2(e,a),
inference(resolution,[status(thm)],[c586,c6]) ).
cnf(rule_272,axiom,
( r3(X899,X897,X898)
| ~ k2(X897,X898)
| ~ r2(X898)
| ~ r3(X898,X899,X899) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_272) ).
cnf(c173,plain,
( r2(c)
| ~ r1(c) ),
inference(resolution,[status(thm)],[rule_188,axiom_24]) ).
cnf(c548,plain,
r2(c),
inference(resolution,[status(thm)],[c547,c173]) ).
cnf(rule_260,axiom,
( r3(X664,X665,X665)
| ~ s2(X665)
| ~ l2(c,X664) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_260) ).
cnf(c756,plain,
( r3(c,X666,X666)
| ~ s2(X666) ),
inference(resolution,[status(thm)],[rule_260,c633]) ).
cnf(rule_189,axiom,
( s2(X687)
| ~ q2(b,X687,b)
| ~ s1(b) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_189) ).
cnf(rule_069,axiom,
( p1(X97,X97,X96)
| ~ p0(X96,X97) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_069) ).
cnf(c122,plain,
p1(X98,X98,b),
inference(resolution,[status(thm)],[rule_069,axiom_14]) ).
cnf(c15,plain,
l1(a,a),
inference(resolution,[status(thm)],[rule_002,axiom_37]) ).
cnf(c495,plain,
( n1(a,X476,a)
| ~ s0(b) ),
inference(resolution,[status(thm)],[c262,axiom_20]) ).
cnf(c497,plain,
n1(a,X480,a),
inference(resolution,[status(thm)],[c495,axiom_5]) ).
cnf(c504,plain,
( n1(a,X1177,X1177)
| ~ l0(X1176)
| ~ l1(X1176,a) ),
inference(resolution,[status(thm)],[c497,rule_054]) ).
cnf(c1416,plain,
( n1(a,X1178,X1178)
| ~ l0(a) ),
inference(resolution,[status(thm)],[c504,c15]) ).
cnf(c1418,plain,
n1(a,X1179,X1179),
inference(resolution,[status(thm)],[c1416,axiom_20]) ).
cnf(axiom_32,axiom,
k0(b),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_32) ).
cnf(c527,plain,
q2(X517,b,b),
inference(resolution,[status(thm)],[c523,axiom_32]) ).
cnf(c755,plain,
( q2(b,X1486,b)
| ~ p1(b,b,b)
| ~ n1(X1486,b,b) ),
inference(resolution,[status(thm)],[rule_182,c527]) ).
cnf(c1969,plain,
( q2(b,a,b)
| ~ p1(b,b,b) ),
inference(resolution,[status(thm)],[c755,c1418]) ).
cnf(c2284,plain,
q2(b,a,b),
inference(resolution,[status(thm)],[c1969,c122]) ).
cnf(c2288,plain,
( s2(a)
| ~ s1(b) ),
inference(resolution,[status(thm)],[c2284,rule_189]) ).
cnf(c2291,plain,
s2(a),
inference(resolution,[status(thm)],[c2288,c223]) ).
cnf(c2294,plain,
r3(c,a,a),
inference(resolution,[status(thm)],[c2291,c756]) ).
cnf(c2301,plain,
( r3(a,X1951,c)
| ~ k2(X1951,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c2294,rule_272]) ).
cnf(c2343,plain,
( r3(a,c,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c2301,c211]) ).
cnf(c2346,plain,
r3(a,c,c),
inference(resolution,[status(thm)],[c2343,c548]) ).
cnf(c2347,plain,
( r3(c,X1954,a)
| ~ k2(X1954,a)
| ~ r2(a) ),
inference(resolution,[status(thm)],[c2346,rule_272]) ).
cnf(c2359,plain,
( r3(c,e,a)
| ~ r2(a) ),
inference(resolution,[status(thm)],[c2347,c592]) ).
cnf(c2364,plain,
r3(c,e,a),
inference(resolution,[status(thm)],[c2359,c549]) ).
cnf(c71,plain,
m1(b,X74,b),
inference(resolution,[status(thm)],[c54,axiom_9]) ).
cnf(c536,plain,
( k2(b,X540)
| ~ k1(X539)
| ~ k2(X539,X540) ),
inference(resolution,[status(thm)],[rule_127,c71]) ).
cnf(c550,plain,
( k2(b,X541)
| ~ k1(X541) ),
inference(resolution,[status(thm)],[c536,c211]) ).
cnf(c552,plain,
k2(b,a),
inference(resolution,[status(thm)],[c550,c6]) ).
cnf(c2358,plain,
( r3(c,b,a)
| ~ r2(a) ),
inference(resolution,[status(thm)],[c2347,c552]) ).
cnf(c2363,plain,
r3(c,b,a),
inference(resolution,[status(thm)],[c2358,c549]) ).
cnf(rule_303,axiom,
( m5(X457,X456)
| ~ r0(X457)
| ~ p4(X457,X455,X456) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_303) ).
cnf(c2357,plain,
( r3(c,c,a)
| ~ r2(a) ),
inference(resolution,[status(thm)],[c2347,c2082]) ).
cnf(c2360,plain,
r3(c,c,a),
inference(resolution,[status(thm)],[c2357,c549]) ).
cnf(c2361,plain,
p4(a,c,c),
inference(resolution,[status(thm)],[c2360,c1193]) ).
cnf(c2362,plain,
( m5(a,c)
| ~ r0(a) ),
inference(resolution,[status(thm)],[c2361,rule_303]) ).
cnf(rule_021,axiom,
( m1(X92,X93,X92)
| ~ l0(X92)
| ~ k0(X93) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_021) ).
cnf(c112,plain,
( m1(X160,b,X160)
| ~ l0(X160) ),
inference(resolution,[status(thm)],[rule_021,axiom_32]) ).
cnf(c197,plain,
m1(c,b,c),
inference(resolution,[status(thm)],[c112,axiom_24]) ).
cnf(c537,plain,
( k2(c,b)
| ~ k1(X1188)
| ~ k2(X1188,b) ),
inference(resolution,[status(thm)],[rule_127,c197]) ).
cnf(c1427,plain,
( k2(c,b)
| ~ k1(b) ),
inference(resolution,[status(thm)],[c537,c211]) ).
cnf(c1429,plain,
k2(c,b),
inference(resolution,[status(thm)],[c1427,c1]) ).
cnf(c758,plain,
( r3(b,X670,X670)
| ~ s2(X670) ),
inference(resolution,[status(thm)],[rule_260,c650]) ).
cnf(c2295,plain,
r3(b,a,a),
inference(resolution,[status(thm)],[c2291,c758]) ).
cnf(c2302,plain,
( r3(a,X1952,b)
| ~ k2(X1952,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c2295,rule_272]) ).
cnf(c2354,plain,
( r3(a,c,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c2302,c1429]) ).
cnf(c593,plain,
k2(e,b),
inference(resolution,[status(thm)],[c586,c1]) ).
cnf(c2352,plain,
( r3(a,e,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c2302,c593]) ).
cnf(c2351,plain,
( r3(a,b,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c2302,c211]) ).
cnf(c0,plain,
k1(c),
inference(resolution,[status(thm)],[rule_001,axiom_26]) ).
cnf(c594,plain,
k2(e,c),
inference(resolution,[status(thm)],[c586,c0]) ).
cnf(c2345,plain,
( r3(a,e,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c2301,c594]) ).
cnf(c2350,plain,
r3(a,e,c),
inference(resolution,[status(thm)],[c2345,c548]) ).
cnf(c554,plain,
k2(b,c),
inference(resolution,[status(thm)],[c550,c0]) ).
cnf(c2344,plain,
( r3(a,b,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c2301,c554]) ).
cnf(c2349,plain,
r3(a,b,c),
inference(resolution,[status(thm)],[c2344,c548]) ).
cnf(axiom_3,axiom,
n0(d,e),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_3) ).
cnf(c2,plain,
k1(e),
inference(resolution,[status(thm)],[rule_001,axiom_3]) ).
cnf(c555,plain,
k2(b,e),
inference(resolution,[status(thm)],[c550,c2]) ).
cnf(axiom_30,axiom,
n0(e,e),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_30) ).
cnf(c649,plain,
( l2(X583,e)
| ~ s1(X583) ),
inference(resolution,[status(thm)],[c635,axiom_30]) ).
cnf(c651,plain,
l2(X584,e),
inference(resolution,[status(thm)],[c649,c223]) ).
cnf(c757,plain,
( r3(e,X667,X667)
| ~ s2(X667) ),
inference(resolution,[status(thm)],[rule_260,c651]) ).
cnf(c2293,plain,
r3(e,a,a),
inference(resolution,[status(thm)],[c2291,c757]) ).
cnf(c2300,plain,
( r3(a,X1950,e)
| ~ k2(X1950,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c2293,rule_272]) ).
cnf(c2341,plain,
( r3(a,b,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c2300,c555]) ).
cnf(c111,plain,
( m1(X157,e,X157)
| ~ l0(X157) ),
inference(resolution,[status(thm)],[rule_021,axiom_28]) ).
cnf(c190,plain,
m1(c,e,c),
inference(resolution,[status(thm)],[c111,axiom_24]) ).
cnf(c546,plain,
( k2(c,e)
| ~ k1(X1210)
| ~ k2(X1210,e) ),
inference(resolution,[status(thm)],[rule_127,c190]) ).
cnf(c1475,plain,
( k2(c,e)
| ~ k1(e) ),
inference(resolution,[status(thm)],[c546,c211]) ).
cnf(c1478,plain,
k2(c,e),
inference(resolution,[status(thm)],[c1475,c2]) ).
cnf(c2340,plain,
( r3(a,c,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c2300,c1478]) ).
cnf(c2339,plain,
( r3(a,e,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c2300,c211]) ).
cnf(c591,plain,
k2(e,d),
inference(resolution,[status(thm)],[c586,c5]) ).
cnf(rule_005,axiom,
( m1(X30,X29,X30)
| ~ m0(X29,X29,X30) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_005) ).
cnf(c41,plain,
m1(X31,d,X31),
inference(resolution,[status(thm)],[rule_005,axiom_19]) ).
cnf(c539,plain,
( k2(X927,d)
| ~ k1(X926)
| ~ k2(X926,d) ),
inference(resolution,[status(thm)],[rule_127,c41]) ).
cnf(c1172,plain,
( k2(X928,d)
| ~ k1(e) ),
inference(resolution,[status(thm)],[c539,c591]) ).
cnf(c1175,plain,
k2(X929,d),
inference(resolution,[status(thm)],[c1172,c2]) ).
cnf(c759,plain,
r3(c,d,d),
inference(resolution,[status(thm)],[c756,c387]) ).
cnf(c1132,plain,
( r3(d,X1812,c)
| ~ k2(X1812,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[rule_272,c759]) ).
cnf(c2214,plain,
( r3(d,c,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c1132,c211]) ).
cnf(c2217,plain,
r3(d,c,c),
inference(resolution,[status(thm)],[c2214,c548]) ).
cnf(c2218,plain,
( r3(c,X1945,d)
| ~ k2(X1945,d)
| ~ r2(d) ),
inference(resolution,[status(thm)],[c2217,rule_272]) ).
cnf(c2337,plain,
( r3(c,X1949,d)
| ~ r2(d) ),
inference(resolution,[status(thm)],[c2218,c1175]) ).
cnf(rule_255,axiom,
( q3(X649,X650)
| ~ q2(X651,X649,X650)
| ~ n0(X651,X649) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_255) ).
cnf(rule_082,axiom,
( p1(X372,X373,X374)
| ~ m0(X374,X372,X371)
| ~ p1(X374,X372,X371) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_082) ).
cnf(c402,plain,
( p1(X382,X381,X382)
| ~ m0(X382,X382,X382) ),
inference(resolution,[status(thm)],[rule_082,c129]) ).
cnf(c413,plain,
p1(a,X383,a),
inference(resolution,[status(thm)],[c402,axiom_12]) ).
cnf(c415,plain,
( p1(X782,X781,a)
| ~ m0(a,X782,a) ),
inference(resolution,[status(thm)],[c413,rule_082]) ).
cnf(c953,plain,
p1(X783,X784,a),
inference(resolution,[status(thm)],[c415,axiom_12]) ).
cnf(c955,plain,
( p1(X787,X786,X788)
| ~ m0(X788,X787,a) ),
inference(resolution,[status(thm)],[c953,rule_082]) ).
cnf(c961,plain,
p1(d,X793,X792),
inference(resolution,[status(thm)],[c955,axiom_19]) ).
cnf(rule_186,axiom,
( q2(X134,X134,X135)
| ~ l1(X135,X134) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_186) ).
cnf(c874,plain,
q2(X733,X733,d),
inference(resolution,[status(thm)],[c870,rule_186]) ).
cnf(c876,plain,
( q2(d,X1628,d)
| ~ p1(d,d,X1628)
| ~ n1(X1628,d,X1628) ),
inference(resolution,[status(thm)],[c874,rule_182]) ).
cnf(c2103,plain,
( q2(d,a,d)
| ~ p1(d,d,a) ),
inference(resolution,[status(thm)],[c876,c497]) ).
cnf(c2332,plain,
q2(d,a,d),
inference(resolution,[status(thm)],[c2103,c961]) ).
cnf(c2336,plain,
( q3(a,d)
| ~ n0(d,a) ),
inference(resolution,[status(thm)],[c2332,rule_255]) ).
cnf(rule_156,axiom,
( p2(X607,e,X606)
| ~ n1(e,X607,a)
| ~ q1(a,X606,X607) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_156) ).
cnf(c196,plain,
m1(a,b,a),
inference(resolution,[status(thm)],[c112,axiom_20]) ).
cnf(rule_016,axiom,
( m1(X80,X81,X81)
| ~ m1(X82,X81,X80)
| ~ m1(X82,X79,X81) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_016) ).
cnf(axiom_36,axiom,
q0(a,b),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_36) ).
cnf(c124,plain,
( m1(X1134,a,b)
| ~ m0(a,X1135,a)
| ~ q0(X1134,b) ),
inference(resolution,[status(thm)],[rule_024,c71]) ).
cnf(c1377,plain,
( m1(X1136,a,b)
| ~ q0(X1136,b) ),
inference(resolution,[status(thm)],[c124,axiom_12]) ).
cnf(c1380,plain,
m1(a,a,b),
inference(resolution,[status(thm)],[c1377,axiom_36]) ).
cnf(c1387,plain,
( m1(X1597,b,b)
| ~ m1(a,b,X1597) ),
inference(resolution,[status(thm)],[c1380,rule_016]) ).
cnf(c2069,plain,
m1(a,b,b),
inference(resolution,[status(thm)],[c1387,c196]) ).
cnf(c2074,plain,
( q1(a,a,b)
| ~ r0(X1598) ),
inference(resolution,[status(thm)],[c2069,rule_113]) ).
cnf(c2075,plain,
q1(a,a,b),
inference(resolution,[status(thm)],[c2074,axiom_9]) ).
cnf(c2077,plain,
( p2(b,e,a)
| ~ n1(e,b,a) ),
inference(resolution,[status(thm)],[c2075,rule_156]) ).
cnf(c1983,plain,
( s2(e)
| ~ s1(b) ),
inference(resolution,[status(thm)],[c1981,rule_189]) ).
cnf(c1986,plain,
s2(e),
inference(resolution,[status(thm)],[c1983,c223]) ).
cnf(c1989,plain,
r3(b,e,e),
inference(resolution,[status(thm)],[c1986,c758]) ).
cnf(c1994,plain,
( r3(e,X1941,b)
| ~ k2(X1941,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c1989,rule_272]) ).
cnf(c2331,plain,
( r3(e,c,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c1994,c1429]) ).
cnf(c544,plain,
( k2(a,b)
| ~ k1(X1204)
| ~ k2(X1204,b) ),
inference(resolution,[status(thm)],[rule_127,c196]) ).
cnf(c1461,plain,
( k2(a,b)
| ~ k1(b) ),
inference(resolution,[status(thm)],[c544,c211]) ).
cnf(c1464,plain,
k2(a,b),
inference(resolution,[status(thm)],[c1461,c1]) ).
cnf(c2330,plain,
( r3(e,a,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c1994,c1464]) ).
cnf(c1988,plain,
r3(c,e,e),
inference(resolution,[status(thm)],[c1986,c756]) ).
cnf(c1992,plain,
( r3(e,X1938,c)
| ~ k2(X1938,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c1988,rule_272]) ).
cnf(c2323,plain,
( r3(e,e,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c1992,c594]) ).
cnf(c2325,plain,
r3(e,e,c),
inference(resolution,[status(thm)],[c2323,c548]) ).
cnf(c2326,plain,
p4(c,e,e),
inference(resolution,[status(thm)],[c2325,c1193]) ).
cnf(c2327,plain,
( m5(c,e)
| ~ r0(c) ),
inference(resolution,[status(thm)],[c2326,rule_303]) ).
cnf(c2322,plain,
( r3(e,b,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c1992,c554]) ).
cnf(c2324,plain,
r3(e,b,c),
inference(resolution,[status(thm)],[c2322,c548]) ).
cnf(rule_206,axiom,
( k3(X236,X237,X236)
| ~ p2(X237,X236,X236) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_206) ).
cnf(rule_071,axiom,
( p1(X314,X315,X314)
| ~ l0(X316)
| ~ p1(X315,X313,X314)
| ~ s0(b) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_071) ).
cnf(c969,plain,
( p1(X1084,d,X1084)
| ~ l0(X1085)
| ~ s0(b) ),
inference(resolution,[status(thm)],[c961,rule_071]) ).
cnf(c1322,plain,
( p1(X1086,d,X1086)
| ~ l0(X1087) ),
inference(resolution,[status(thm)],[c969,axiom_5]) ).
cnf(c1323,plain,
p1(X1089,d,X1089),
inference(resolution,[status(thm)],[c1322,axiom_20]) ).
cnf(rule_176,axiom,
( p2(X220,X219,X220)
| ~ m1(X219,X220,X219) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_176) ).
cnf(c254,plain,
p2(X222,b,X222),
inference(resolution,[status(thm)],[rule_176,c71]) ).
cnf(rule_146,axiom,
( p2(X559,X562,X562)
| ~ p1(X559,X561,X560)
| ~ l1(X561,X560)
| ~ p2(X559,X562,X559) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_146) ).
cnf(c629,plain,
( p2(X1375,b,b)
| ~ p1(X1375,X1373,X1374)
| ~ l1(X1373,X1374) ),
inference(resolution,[status(thm)],[rule_146,c254]) ).
cnf(c1741,plain,
( p2(X1448,b,b)
| ~ l1(d,X1448) ),
inference(resolution,[status(thm)],[c629,c1323]) ).
cnf(c1909,plain,
p2(X1449,b,b),
inference(resolution,[status(thm)],[c1741,c870]) ).
cnf(c1912,plain,
k3(b,X1451,b),
inference(resolution,[status(thm)],[c1909,rule_206]) ).
cnf(rule_295,axiom,
( q4(X989,X990)
| ~ k3(X988,X988,X989)
| ~ q2(X991,X990,X989)
| ~ m3(X991,X987,X991) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_295) ).
cnf(c1228,plain,
( q4(X1362,X1364)
| ~ k3(X1361,X1361,X1362)
| ~ q2(X1363,X1364,X1362) ),
inference(resolution,[status(thm)],[rule_295,c131]) ).
cnf(c2287,plain,
( q4(b,a)
| ~ k3(X1933,X1933,b) ),
inference(resolution,[status(thm)],[c2284,c1228]) ).
cnf(c2316,plain,
q4(b,a),
inference(resolution,[status(thm)],[c2287,c1912]) ).
cnf(rule_319,axiom,
( p5(X1054,X1053,X1053)
| ~ l2(X1054,X1055)
| ~ p5(X1054,X1055,X1054)
| ~ m4(X1055,X1053) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_319) ).
cnf(rule_320,axiom,
( p5(X463,X464,X463)
| ~ q4(X464,X462)
| ~ s1(X463) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_320) ).
cnf(rule_194,axiom,
( k3(X142,X142,X141)
| ~ k2(X141,X142) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_194) ).
cnf(c1181,plain,
k3(d,d,X930),
inference(resolution,[status(thm)],[c1175,rule_194]) ).
cnf(c1695,plain,
( q4(X1368,X1368)
| ~ k3(X1369,X1369,X1368) ),
inference(resolution,[status(thm)],[c1228,c272]) ).
cnf(c1726,plain,
q4(X1370,X1370),
inference(resolution,[status(thm)],[c1695,c1181]) ).
cnf(c1736,plain,
( p5(X1382,X1383,X1382)
| ~ s1(X1382) ),
inference(resolution,[status(thm)],[c1726,rule_320]) ).
cnf(c1780,plain,
p5(X1384,X1385,X1384),
inference(resolution,[status(thm)],[c1736,c223]) ).
cnf(c1781,plain,
( p5(X1572,X1571,X1571)
| ~ l2(X1572,X1570)
| ~ m4(X1570,X1571) ),
inference(resolution,[status(thm)],[c1780,rule_319]) ).
cnf(rule_279,axiom,
( m4(X673,X672)
| ~ l2(X671,X672)
| ~ s3(a,X673) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_279) ).
cnf(rule_273,axiom,
( s3(X904,X906)
| ~ q2(X903,X904,X903)
| ~ s2(X904)
| ~ m0(X903,X905,X906) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_273) ).
cnf(c1148,plain,
( s3(X908,X909)
| ~ q2(X907,X908,X907)
| ~ s2(X908) ),
inference(resolution,[status(thm)],[rule_273,axiom_19]) ).
cnf(c1155,plain,
( s3(X911,X910)
| ~ s2(X911) ),
inference(resolution,[status(thm)],[c1148,c272]) ).
cnf(c2296,plain,
s3(a,X1903),
inference(resolution,[status(thm)],[c2291,c1155]) ).
cnf(c2297,plain,
( m4(X1907,X1909)
| ~ l2(X1908,X1909) ),
inference(resolution,[status(thm)],[c2296,rule_279]) ).
cnf(c2303,plain,
m4(X1911,X1910),
inference(resolution,[status(thm)],[c2297,c633]) ).
cnf(c2307,plain,
( p5(X1922,X1923,X1923)
| ~ l2(X1922,X1921) ),
inference(resolution,[status(thm)],[c2303,c1781]) ).
cnf(c2313,plain,
p5(X1925,X1924,X1924),
inference(resolution,[status(thm)],[c2307,c633]) ).
cnf(c14,plain,
l1(d,d),
inference(resolution,[status(thm)],[rule_002,axiom_34]) ).
cnf(rule_244,axiom,
( p3(X48,X48,X48)
| ~ n2(X48) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_244) ).
cnf(c132,plain,
p3(X110,X110,X110),
inference(resolution,[status(thm)],[c130,rule_244]) ).
cnf(rule_299,axiom,
( s4(X401)
| ~ p3(X403,X402,X404)
| ~ l1(X401,X402) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_299) ).
cnf(c421,plain,
( s4(X405)
| ~ l1(X405,X406) ),
inference(resolution,[status(thm)],[rule_299,c132]) ).
cnf(c426,plain,
s4(d),
inference(resolution,[status(thm)],[c421,c14]) ).
cnf(rule_305,axiom,
( m5(X715,X715)
| ~ s4(X715)
| ~ m4(e,e) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_305) ).
cnf(c2306,plain,
( m5(X1917,X1917)
| ~ s4(X1917) ),
inference(resolution,[status(thm)],[c2303,rule_305]) ).
cnf(c2312,plain,
m5(d,d),
inference(resolution,[status(thm)],[c2306,c426]) ).
cnf(c423,plain,
s4(a),
inference(resolution,[status(thm)],[c421,c15]) ).
cnf(c2309,plain,
m5(a,a),
inference(resolution,[status(thm)],[c2306,c423]) ).
cnf(rule_059,axiom,
( n1(X273,X273,X274)
| ~ m0(X275,X272,X272)
| ~ m0(X274,X275,X273) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_059) ).
cnf(c320,plain,
( n1(X349,X349,X347)
| ~ m0(d,X348,X348) ),
inference(resolution,[status(thm)],[rule_059,axiom_19]) ).
cnf(c383,plain,
n1(X351,X351,X350),
inference(resolution,[status(thm)],[c320,axiom_19]) ).
cnf(rule_257,axiom,
( q3(X839,X838)
| ~ n1(X840,X839,X838)
| ~ s2(X839)
| ~ q3(X838,X839) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_257) ).
cnf(c1068,plain,
( q3(X843,X844)
| ~ s2(X843)
| ~ q3(X844,X843) ),
inference(resolution,[status(thm)],[rule_257,c383]) ).
cnf(axiom_15,axiom,
n0(a,b),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_15) ).
cnf(c1980,plain,
( q2(X1504,b,X1504)
| ~ r1(b) ),
inference(resolution,[status(thm)],[c1976,axiom_32]) ).
cnf(c1995,plain,
q2(X1508,b,X1508),
inference(resolution,[status(thm)],[c1980,c547]) ).
cnf(c2000,plain,
( q3(b,X1527)
| ~ n0(X1527,b) ),
inference(resolution,[status(thm)],[c1995,rule_255]) ).
cnf(c2038,plain,
q3(b,a),
inference(resolution,[status(thm)],[c2000,axiom_15]) ).
cnf(c2040,plain,
( q3(a,b)
| ~ s2(a) ),
inference(resolution,[status(thm)],[c2038,c1068]) ).
cnf(c2292,plain,
q3(a,b),
inference(resolution,[status(thm)],[c2291,c2040]) ).
cnf(c1963,plain,
( q2(e,a,e)
| ~ p1(e,e,e) ),
inference(resolution,[status(thm)],[c754,c1418]) ).
cnf(c2275,plain,
q2(e,a,e),
inference(resolution,[status(thm)],[c1963,c129]) ).
cnf(c2278,plain,
( q3(a,e)
| ~ n0(e,a) ),
inference(resolution,[status(thm)],[c2275,rule_255]) ).
cnf(c2276,plain,
( q4(e,a)
| ~ k3(X1893,X1893,e) ),
inference(resolution,[status(thm)],[c2275,c1228]) ).
cnf(c2279,plain,
q4(e,a),
inference(resolution,[status(thm)],[c2276,c1181]) ).
cnf(c2248,plain,
( q4(e,d)
| ~ k3(X1886,X1886,e) ),
inference(resolution,[status(thm)],[c2247,c1228]) ).
cnf(c2270,plain,
q4(e,d),
inference(resolution,[status(thm)],[c2248,c1181]) ).
cnf(rule_284,axiom,
( n4(X393,X393)
| ~ k4(X394)
| ~ m3(X393,X393,X393) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_284) ).
cnf(c420,plain,
( n4(X395,X395)
| ~ k4(X396) ),
inference(resolution,[status(thm)],[rule_284,c131]) ).
cnf(rule_240,axiom,
( n3(X44)
| ~ p2(X43,X42,X44) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_240) ).
cnf(rule_150,axiom,
( p2(X211,X211,X211)
| ~ m1(X210,X210,X211) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_150) ).
cnf(c251,plain,
p2(X212,X212,X212),
inference(resolution,[status(thm)],[rule_150,c50]) ).
cnf(c252,plain,
n3(X213),
inference(resolution,[status(thm)],[c251,rule_240]) ).
cnf(rule_274,axiom,
( k4(c)
| ~ n0(c,d)
| ~ q3(e,b)
| ~ n3(e) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_274) ).
cnf(axiom_18,axiom,
p0(c,b),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_18) ).
cnf(axiom_27,axiom,
m0(e,b,c),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_27) ).
cnf(c18,plain,
( l1(b,e)
| ~ p0(c,b)
| ~ r0(X1097) ),
inference(resolution,[status(thm)],[rule_003,axiom_27]) ).
cnf(c1329,plain,
( l1(b,e)
| ~ r0(X1098) ),
inference(resolution,[status(thm)],[c18,axiom_18]) ).
cnf(c1330,plain,
l1(b,e),
inference(resolution,[status(thm)],[c1329,axiom_9]) ).
cnf(c1333,plain,
q2(e,e,b),
inference(resolution,[status(thm)],[c1330,rule_186]) ).
cnf(c1336,plain,
( q3(e,b)
| ~ n0(e,e) ),
inference(resolution,[status(thm)],[c1333,rule_255]) ).
cnf(c1342,plain,
q3(e,b),
inference(resolution,[status(thm)],[c1336,axiom_30]) ).
cnf(c1344,plain,
( k4(c)
| ~ n0(c,d)
| ~ n3(e) ),
inference(resolution,[status(thm)],[c1342,rule_274]) ).
cnf(c2052,plain,
( k4(c)
| ~ n3(e) ),
inference(resolution,[status(thm)],[c1344,axiom_34]) ).
cnf(c2053,plain,
k4(c),
inference(resolution,[status(thm)],[c2052,c252]) ).
cnf(c2054,plain,
n4(X1584,X1584),
inference(resolution,[status(thm)],[c2053,c420]) ).
cnf(rule_281,axiom,
( n4(X675,X674)
| ~ p3(X675,X674,X674)
| ~ n4(X675,X675) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_281) ).
cnf(c761,plain,
( q2(X984,c,X984)
| ~ k1(X984)
| ~ l0(c) ),
inference(resolution,[status(thm)],[rule_183,c633]) ).
cnf(c1207,plain,
( q2(X985,c,X985)
| ~ k1(X985) ),
inference(resolution,[status(thm)],[c761,axiom_24]) ).
cnf(c1210,plain,
q2(b,c,b),
inference(resolution,[status(thm)],[c1207,c1]) ).
cnf(c1218,plain,
( s2(c)
| ~ s1(b) ),
inference(resolution,[status(thm)],[c1210,rule_189]) ).
cnf(c1223,plain,
s2(c),
inference(resolution,[status(thm)],[c1218,c223]) ).
cnf(rule_237,axiom,
( m3(X796,c,X796)
| ~ s2(c)
| ~ q2(X796,c,c) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_237) ).
cnf(c762,plain,
( q2(e,c,X1228)
| ~ k1(X1228)
| ~ l0(c) ),
inference(resolution,[status(thm)],[rule_183,c651]) ).
cnf(c1490,plain,
( q2(e,c,X1230)
| ~ k1(X1230) ),
inference(resolution,[status(thm)],[c762,axiom_24]) ).
cnf(c1494,plain,
q2(e,c,c),
inference(resolution,[status(thm)],[c1490,c0]) ).
cnf(c1502,plain,
( m3(e,c,e)
| ~ s2(c) ),
inference(resolution,[status(thm)],[c1494,rule_237]) ).
cnf(c1505,plain,
m3(e,c,e),
inference(resolution,[status(thm)],[c1502,c1223]) ).
cnf(rule_251,axiom,
( p3(X827,X829,X829)
| ~ m3(X829,X828,X830)
| ~ p2(X827,X829,X830) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_251) ).
cnf(c256,plain,
p2(X225,e,X225),
inference(resolution,[status(thm)],[rule_176,c72]) ).
cnf(c628,plain,
( p2(X1367,e,e)
| ~ p1(X1367,X1365,X1366)
| ~ l1(X1365,X1366) ),
inference(resolution,[status(thm)],[rule_146,c256]) ).
cnf(c1713,plain,
( p2(X1422,e,e)
| ~ l1(d,X1422) ),
inference(resolution,[status(thm)],[c628,c1323]) ).
cnf(c1871,plain,
p2(X1423,e,e),
inference(resolution,[status(thm)],[c1713,c870]) ).
cnf(c1879,plain,
( p3(X1636,e,e)
| ~ m3(e,X1635,e) ),
inference(resolution,[status(thm)],[c1871,rule_251]) ).
cnf(c2110,plain,
p3(X1637,e,e),
inference(resolution,[status(thm)],[c1879,c1505]) ).
cnf(c2113,plain,
( n4(X1642,e)
| ~ n4(X1642,X1642) ),
inference(resolution,[status(thm)],[c2110,rule_281]) ).
cnf(c2118,plain,
n4(X1643,e),
inference(resolution,[status(thm)],[c2113,c2054]) ).
cnf(rule_241,axiom,
( p3(X806,X809,X808)
| ~ q2(X807,d,X806)
| ~ k2(X809,X808) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_241) ).
cnf(c2252,plain,
( p3(e,X1876,X1877)
| ~ k2(X1876,X1877) ),
inference(resolution,[status(thm)],[c2247,rule_241]) ).
cnf(c2254,plain,
p3(e,X1878,X1878),
inference(resolution,[status(thm)],[c2252,c211]) ).
cnf(c2266,plain,
( n4(e,X1880)
| ~ n4(e,e) ),
inference(resolution,[status(thm)],[c2254,rule_281]) ).
cnf(c2268,plain,
n4(e,X1884),
inference(resolution,[status(thm)],[c2266,c2118]) ).
cnf(c2265,plain,
p3(e,c,b),
inference(resolution,[status(thm)],[c2252,c1429]) ).
cnf(c2264,plain,
p3(e,e,c),
inference(resolution,[status(thm)],[c2252,c594]) ).
cnf(c2263,plain,
p3(e,a,b),
inference(resolution,[status(thm)],[c2252,c1464]) ).
cnf(c2262,plain,
p3(e,e,a),
inference(resolution,[status(thm)],[c2252,c592]) ).
cnf(c189,plain,
m1(a,e,a),
inference(resolution,[status(thm)],[c111,axiom_20]) ).
cnf(c542,plain,
( k2(a,e)
| ~ k1(X1199)
| ~ k2(X1199,e) ),
inference(resolution,[status(thm)],[rule_127,c189]) ).
cnf(c1443,plain,
( k2(a,e)
| ~ k1(e) ),
inference(resolution,[status(thm)],[c542,c211]) ).
cnf(c1445,plain,
k2(a,e),
inference(resolution,[status(thm)],[c1443,c2]) ).
cnf(c2261,plain,
p3(e,a,e),
inference(resolution,[status(thm)],[c2252,c1445]) ).
cnf(c2260,plain,
p3(e,b,a),
inference(resolution,[status(thm)],[c2252,c552]) ).
cnf(c2259,plain,
p3(e,e,b),
inference(resolution,[status(thm)],[c2252,c593]) ).
cnf(c2257,plain,
p3(e,b,c),
inference(resolution,[status(thm)],[c2252,c554]) ).
cnf(c2256,plain,
p3(e,c,a),
inference(resolution,[status(thm)],[c2252,c2082]) ).
cnf(c2255,plain,
p3(e,c,e),
inference(resolution,[status(thm)],[c2252,c1478]) ).
cnf(c2253,plain,
p3(e,X1879,d),
inference(resolution,[status(thm)],[c2252,c1175]) ).
cnf(rule_314,axiom,
( n5(X12,X12)
| ~ r4(X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_314) ).
cnf(c1208,plain,
q2(d,c,d),
inference(resolution,[status(thm)],[c1207,c5]) ).
cnf(c1214,plain,
( q3(c,d)
| ~ n0(d,c) ),
inference(resolution,[status(thm)],[c1208,rule_255]) ).
cnf(c1238,plain,
q3(c,d),
inference(resolution,[status(thm)],[c1214,axiom_26]) ).
cnf(rule_298,axiom,
( r4(X996)
| ~ n3(X996)
| ~ q3(X997,X998)
| ~ p0(X999,X996) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_298) ).
cnf(c1246,plain,
( r4(X1000)
| ~ n3(X1000)
| ~ q3(X1001,X1002) ),
inference(resolution,[status(thm)],[rule_298,axiom_14]) ).
cnf(c1247,plain,
( r4(X1003)
| ~ n3(X1003) ),
inference(resolution,[status(thm)],[c1246,c1238]) ).
cnf(c1256,plain,
r4(X1004),
inference(resolution,[status(thm)],[c1247,c252]) ).
cnf(c1258,plain,
n5(X1005,X1005),
inference(resolution,[status(thm)],[c1256,rule_314]) ).
cnf(rule_307,axiom,
( n5(X1014,X1015)
| ~ q4(X1013,X1016)
| ~ n4(X1014,X1016)
| ~ p4(X1012,X1012,X1015)
| ~ n5(X1012,X1015) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_307) ).
cnf(c1259,plain,
( n5(X1819,X1820)
| ~ q4(X1821,X1822)
| ~ n4(X1819,X1822)
| ~ n5(X1820,X1820) ),
inference(resolution,[status(thm)],[rule_307,c296]) ).
cnf(c2231,plain,
( n5(X1823,X1826)
| ~ q4(X1824,X1825)
| ~ n4(X1823,X1825) ),
inference(resolution,[status(thm)],[c1259,c1258]) ).
cnf(c2238,plain,
( n5(X1828,X1827)
| ~ q4(X1829,X1828) ),
inference(resolution,[status(thm)],[c2231,c2054]) ).
cnf(c2240,plain,
n5(X1830,X1831),
inference(resolution,[status(thm)],[c2238,c1726]) ).
cnf(c1232,plain,
r3(b,c,c),
inference(resolution,[status(thm)],[c1223,c758]) ).
cnf(c1237,plain,
( r3(c,X1818,b)
| ~ k2(X1818,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c1232,rule_272]) ).
cnf(c2229,plain,
( r3(c,a,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c1237,c1464]) ).
cnf(c2228,plain,
( r3(c,e,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c1237,c593]) ).
cnf(c1230,plain,
r3(e,c,c),
inference(resolution,[status(thm)],[c1223,c757]) ).
cnf(c1235,plain,
( r3(c,X1815,e)
| ~ k2(X1815,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c1230,rule_272]) ).
cnf(c2226,plain,
( r3(c,a,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c1235,c1445]) ).
cnf(c2225,plain,
( r3(c,b,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c1235,c555]) ).
cnf(c2224,plain,
( r3(c,c,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c1235,c1478]) ).
cnf(c2216,plain,
( r3(d,e,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c1132,c594]) ).
cnf(c2221,plain,
r3(d,e,c),
inference(resolution,[status(thm)],[c2216,c548]) ).
cnf(c2215,plain,
( r3(d,b,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c1132,c554]) ).
cnf(c2219,plain,
r3(d,b,c),
inference(resolution,[status(thm)],[c2215,c548]) ).
cnf(c782,plain,
( s2(b)
| ~ s1(b) ),
inference(resolution,[status(thm)],[rule_189,c272]) ).
cnf(c784,plain,
s2(b),
inference(resolution,[status(thm)],[c782,c223]) ).
cnf(c787,plain,
r3(c,b,b),
inference(resolution,[status(thm)],[c784,c756]) ).
cnf(c1131,plain,
( r3(b,X1811,c)
| ~ k2(X1811,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[rule_272,c787]) ).
cnf(c2209,plain,
( r3(b,e,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c1131,c594]) ).
cnf(c2213,plain,
r3(b,e,c),
inference(resolution,[status(thm)],[c2209,c548]) ).
cnf(c2208,plain,
( r3(b,b,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c1131,c554]) ).
cnf(c2210,plain,
r3(b,b,c),
inference(resolution,[status(thm)],[c2208,c548]) ).
cnf(c2211,plain,
p4(c,b,b),
inference(resolution,[status(thm)],[c2210,c1193]) ).
cnf(c2212,plain,
( m5(c,b)
| ~ r0(c) ),
inference(resolution,[status(thm)],[c2211,rule_303]) ).
cnf(c764,plain,
r3(b,d,d),
inference(resolution,[status(thm)],[c758,c387]) ).
cnf(c1130,plain,
( r3(d,X1810,b)
| ~ k2(X1810,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[rule_272,c764]) ).
cnf(c2203,plain,
( r3(d,c,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c1130,c1429]) ).
cnf(c2202,plain,
( r3(d,a,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c1130,c1464]) ).
cnf(c2201,plain,
( r3(d,e,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c1130,c593]) ).
cnf(c2200,plain,
( r3(d,b,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c1130,c211]) ).
cnf(c760,plain,
r3(e,d,d),
inference(resolution,[status(thm)],[c757,c387]) ).
cnf(c1129,plain,
( r3(d,X1809,e)
| ~ k2(X1809,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[rule_272,c760]) ).
cnf(c2198,plain,
( r3(d,a,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c1129,c1445]) ).
cnf(c2197,plain,
( r3(d,b,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c1129,c555]) ).
cnf(c2196,plain,
( r3(d,c,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c1129,c1478]) ).
cnf(c2195,plain,
( r3(d,e,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c1129,c211]) ).
cnf(c785,plain,
r3(e,b,b),
inference(resolution,[status(thm)],[c784,c757]) ).
cnf(c1125,plain,
( r3(b,X1806,e)
| ~ k2(X1806,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[rule_272,c785]) ).
cnf(c2192,plain,
( r3(b,a,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c1125,c1445]) ).
cnf(c2191,plain,
( r3(b,b,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c1125,c555]) ).
cnf(c2190,plain,
( r3(b,c,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c1125,c1478]) ).
cnf(rule_141,axiom,
( p2(X355,a,X355)
| ~ q1(X355,a,X355) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_141) ).
cnf(rule_092,axiom,
( q1(X416,X413,X416)
| ~ n0(X415,X413)
| ~ p0(X414,X416) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_092) ).
cnf(c449,plain,
( q1(X421,X422,X421)
| ~ n0(X423,X422) ),
inference(resolution,[status(thm)],[rule_092,axiom_14]) ).
cnf(c457,plain,
q1(X436,a,X436),
inference(resolution,[status(thm)],[c449,axiom_37]) ).
cnf(c465,plain,
p2(X438,a,X438),
inference(resolution,[status(thm)],[c457,rule_141]) ).
cnf(rule_158,axiom,
( p2(X609,X609,X608)
| ~ q1(c,X609,X610)
| ~ s1(c)
| ~ s0(e)
| ~ p2(X609,X610,X609) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_158) ).
cnf(c690,plain,
( p2(X1455,X1455,X1456)
| ~ q1(c,X1455,a)
| ~ s1(c)
| ~ s0(e) ),
inference(resolution,[status(thm)],[rule_158,c465]) ).
cnf(rule_099,axiom,
( q1(X435,X434,X434)
| ~ k0(X433)
| ~ l0(X435)
| ~ q1(X434,X434,X433) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_099) ).
cnf(c2078,plain,
( q1(X1661,a,a)
| ~ k0(b)
| ~ l0(X1661) ),
inference(resolution,[status(thm)],[c2075,rule_099]) ).
cnf(c2135,plain,
( q1(c,a,a)
| ~ k0(b) ),
inference(resolution,[status(thm)],[c2078,axiom_24]) ).
cnf(c2136,plain,
q1(c,a,a),
inference(resolution,[status(thm)],[c2135,axiom_32]) ).
cnf(c2137,plain,
( p2(a,a,X1796)
| ~ s1(c)
| ~ s0(e) ),
inference(resolution,[status(thm)],[c2136,c690]) ).
cnf(axiom_31,axiom,
m0(b,b,e),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_31) ).
cnf(c926,plain,
( m3(X1652,X1651,X1652)
| ~ m0(X1653,X1653,X1651)
| ~ l2(d,X1652)
| ~ s2(X1653) ),
inference(resolution,[status(thm)],[rule_225,axiom_19]) ).
cnf(c2129,plain,
( m3(X1793,e,X1793)
| ~ l2(d,X1793)
| ~ s2(b) ),
inference(resolution,[status(thm)],[c926,axiom_31]) ).
cnf(c2127,plain,
( m3(X1792,a,X1792)
| ~ l2(d,X1792)
| ~ s2(a) ),
inference(resolution,[status(thm)],[c926,axiom_12]) ).
cnf(rule_095,axiom,
( q1(X119,X118,X118)
| ~ p0(X118,X119) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_095) ).
cnf(c143,plain,
q1(X120,b,b),
inference(resolution,[status(thm)],[rule_095,axiom_14]) ).
cnf(c685,plain,
( p2(X1428,X1428,X1427)
| ~ q1(c,X1428,X1428)
| ~ s1(c)
| ~ s0(e) ),
inference(resolution,[status(thm)],[rule_158,c251]) ).
cnf(c1896,plain,
( p2(b,b,X1775)
| ~ s1(c)
| ~ s0(e) ),
inference(resolution,[status(thm)],[c685,c143]) ).
cnf(c463,plain,
( q1(X444,X445,X445)
| ~ k0(X445)
| ~ l0(X444) ),
inference(resolution,[status(thm)],[rule_099,c208]) ).
cnf(c473,plain,
( q1(c,X451,X451)
| ~ k0(X451) ),
inference(resolution,[status(thm)],[c463,axiom_24]) ).
cnf(c478,plain,
q1(c,e,e),
inference(resolution,[status(thm)],[c473,axiom_28]) ).
cnf(c1894,plain,
( p2(e,e,X1773)
| ~ s1(c)
| ~ s0(e) ),
inference(resolution,[status(thm)],[c685,c478]) ).
cnf(c1893,plain,
( p2(c,c,X1772)
| ~ s1(c)
| ~ s0(e) ),
inference(resolution,[status(thm)],[c685,c208]) ).
cnf(rule_105,axiom,
( q1(X452,X452,X453)
| ~ s0(X452)
| ~ p0(X453,d) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_105) ).
cnf(c480,plain,
( q1(X454,X454,b)
| ~ s0(X454) ),
inference(resolution,[status(thm)],[rule_105,axiom_14]) ).
cnf(c481,plain,
q1(d,d,b),
inference(resolution,[status(thm)],[c480,axiom_1]) ).
cnf(c483,plain,
( q1(X1175,d,d)
| ~ k0(b)
| ~ l0(X1175) ),
inference(resolution,[status(thm)],[c481,rule_099]) ).
cnf(c1412,plain,
( q1(c,d,d)
| ~ k0(b) ),
inference(resolution,[status(thm)],[c483,axiom_24]) ).
cnf(c1415,plain,
q1(c,d,d),
inference(resolution,[status(thm)],[c1412,axiom_32]) ).
cnf(c1892,plain,
( p2(d,d,X1771)
| ~ s1(c)
| ~ s0(e) ),
inference(resolution,[status(thm)],[c685,c1415]) ).
cnf(rule_258,axiom,
( q3(X846,X846)
| ~ r2(X846)
| ~ s1(X847)
| ~ l2(X845,X845) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_258) ).
cnf(c1074,plain,
( q3(X849,X849)
| ~ r2(X849)
| ~ s1(X848) ),
inference(resolution,[status(thm)],[rule_258,c633]) ).
cnf(c1079,plain,
( q3(X850,X850)
| ~ r2(X850) ),
inference(resolution,[status(thm)],[c1074,c223]) ).
cnf(c1081,plain,
q3(a,a),
inference(resolution,[status(thm)],[c1079,c549]) ).
cnf(rule_276,axiom,
( k4(e)
| ~ q3(X920,X920)
| ~ q1(a,a,X921)
| ~ r3(X920,e,X921) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_276) ).
cnf(rule_267,axiom,
( r3(X242,X241,X242)
| ~ p2(X242,X243,X241) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_267) ).
cnf(c1880,plain,
r3(X1424,e,X1424),
inference(resolution,[status(thm)],[c1871,rule_267]) ).
cnf(c1883,plain,
( k4(e)
| ~ q3(X1770,X1770)
| ~ q1(a,a,X1770) ),
inference(resolution,[status(thm)],[c1880,rule_276]) ).
cnf(c2176,plain,
( k4(e)
| ~ q3(a,a) ),
inference(resolution,[status(thm)],[c1883,c457]) ).
cnf(c2180,plain,
k4(e),
inference(resolution,[status(thm)],[c2176,c1081]) ).
cnf(rule_063,axiom,
( p1(X291,X291,X290)
| ~ n0(d,X291)
| ~ k0(X290) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_063) ).
cnf(c347,plain,
( p1(b,b,X297)
| ~ k0(X297) ),
inference(resolution,[status(thm)],[rule_063,axiom_7]) ).
cnf(c353,plain,
p1(b,b,e),
inference(resolution,[status(thm)],[c347,axiom_28]) ).
cnf(c362,plain,
( p1(e,b,e)
| ~ l0(X1240)
| ~ s0(b) ),
inference(resolution,[status(thm)],[rule_071,c353]) ).
cnf(c1540,plain,
( p1(e,b,e)
| ~ l0(X1241) ),
inference(resolution,[status(thm)],[c362,axiom_5]) ).
cnf(c1541,plain,
p1(e,b,e),
inference(resolution,[status(thm)],[c1540,axiom_20]) ).
cnf(c1543,plain,
( p1(b,X1752,e)
| ~ m0(e,b,e) ),
inference(resolution,[status(thm)],[c1541,rule_082]) ).
cnf(c346,plain,
( p1(c,c,X293)
| ~ k0(X293) ),
inference(resolution,[status(thm)],[rule_063,axiom_26]) ).
cnf(c351,plain,
p1(c,c,e),
inference(resolution,[status(thm)],[c346,axiom_28]) ).
cnf(c359,plain,
( p1(e,c,e)
| ~ l0(X1236)
| ~ s0(b) ),
inference(resolution,[status(thm)],[rule_071,c351]) ).
cnf(c1524,plain,
( p1(e,c,e)
| ~ l0(X1237) ),
inference(resolution,[status(thm)],[c359,axiom_5]) ).
cnf(c1525,plain,
p1(e,c,e),
inference(resolution,[status(thm)],[c1524,axiom_20]) ).
cnf(c1527,plain,
( p1(c,X1743,e)
| ~ m0(e,c,e) ),
inference(resolution,[status(thm)],[c1525,rule_082]) ).
cnf(rule_019,axiom,
( m1(X90,X91,c)
| ~ r0(c)
| ~ s0(d)
| ~ q0(X91,d)
| ~ p0(X90,X91) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_019) ).
cnf(c106,plain,
( m1(b,X1132,c)
| ~ r0(c)
| ~ s0(d)
| ~ q0(X1132,d) ),
inference(resolution,[status(thm)],[rule_019,axiom_14]) ).
cnf(c1371,plain,
( m1(b,X1725,c)
| ~ r0(c)
| ~ s0(d) ),
inference(resolution,[status(thm)],[c106,axiom_17]) ).
cnf(c2175,plain,
( m1(b,X1726,c)
| ~ r0(c) ),
inference(resolution,[status(thm)],[c1371,axiom_1]) ).
cnf(c2128,plain,
( m3(X1663,X1664,X1663)
| ~ l2(d,X1663)
| ~ s2(d) ),
inference(resolution,[status(thm)],[c926,axiom_19]) ).
cnf(c2140,plain,
( m3(e,X1671,e)
| ~ s2(d) ),
inference(resolution,[status(thm)],[c2128,c651]) ).
cnf(c2148,plain,
m3(e,X1672,e),
inference(resolution,[status(thm)],[c2140,c387]) ).
cnf(rule_254,axiom,
( p3(e,b,e)
| ~ m3(e,X834,e)
| ~ q2(X834,X834,b) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_254) ).
cnf(c1055,plain,
( p3(e,b,e)
| ~ m3(e,b,e) ),
inference(resolution,[status(thm)],[rule_254,c272]) ).
cnf(c2174,plain,
p3(e,b,e),
inference(resolution,[status(thm)],[c1055,c2148]) ).
cnf(c1021,plain,
( p3(d,d,e)
| ~ l3(b,e)
| ~ p2(d,b,c)
| ~ n3(d) ),
inference(resolution,[status(thm)],[rule_243,c874]) ).
cnf(rule_259,axiom,
( q3(X851,X851)
| ~ m0(X852,d,X852)
| ~ k1(X851)
| ~ r2(d)
| ~ q3(X852,X851) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_259) ).
cnf(c1084,plain,
( q3(X1689,X1689)
| ~ k1(X1689)
| ~ r2(d)
| ~ q3(X1690,X1689) ),
inference(resolution,[status(thm)],[rule_259,axiom_19]) ).
cnf(c2141,plain,
( m3(b,X1677,b)
| ~ s2(d) ),
inference(resolution,[status(thm)],[c2128,c650]) ).
cnf(c2158,plain,
m3(b,X1678,b),
inference(resolution,[status(thm)],[c2141,c387]) ).
cnf(c280,plain,
r3(X244,X244,X244),
inference(resolution,[status(thm)],[rule_267,c251]) ).
cnf(rule_268,axiom,
( r3(X877,X877,X878)
| ~ m2(X878)
| ~ m3(X879,b,X877)
| ~ r3(X878,X876,X876) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_268) ).
cnf(c1104,plain,
( r3(X1347,X1347,X1349)
| ~ m2(X1349)
| ~ m3(X1348,b,X1347) ),
inference(resolution,[status(thm)],[rule_268,c280]) ).
cnf(c2149,plain,
( r3(e,e,X1673)
| ~ m2(X1673) ),
inference(resolution,[status(thm)],[c2148,c1104]) ).
cnf(c2151,plain,
r3(e,e,d),
inference(resolution,[status(thm)],[c2149,c233]) ).
cnf(c2155,plain,
p4(d,e,e),
inference(resolution,[status(thm)],[c2151,c1193]) ).
cnf(c2157,plain,
( m5(d,e)
| ~ r0(d) ),
inference(resolution,[status(thm)],[c2155,rule_303]) ).
cnf(c2150,plain,
r3(e,e,b),
inference(resolution,[status(thm)],[c2149,c43]) ).
cnf(c2153,plain,
p4(b,e,e),
inference(resolution,[status(thm)],[c2150,c1193]) ).
cnf(c2139,plain,
( m3(d,X1665,d)
| ~ s2(d) ),
inference(resolution,[status(thm)],[c2128,c633]) ).
cnf(c2142,plain,
m3(d,X1667,d),
inference(resolution,[status(thm)],[c2139,c387]) ).
cnf(c2143,plain,
( r3(d,d,X1668)
| ~ m2(X1668) ),
inference(resolution,[status(thm)],[c2142,c1104]) ).
cnf(c2144,plain,
r3(d,d,b),
inference(resolution,[status(thm)],[c2143,c43]) ).
cnf(c2146,plain,
p4(b,d,d),
inference(resolution,[status(thm)],[c2144,c1193]) ).
cnf(c1916,plain,
( p3(X1647,b,b)
| ~ m3(b,X1646,b) ),
inference(resolution,[status(thm)],[c1909,rule_251]) ).
cnf(c2123,plain,
p3(X1648,b,b),
inference(resolution,[status(thm)],[c1916,c131]) ).
cnf(c2126,plain,
( n4(X1654,b)
| ~ n4(X1654,X1654) ),
inference(resolution,[status(thm)],[c2123,rule_281]) ).
cnf(c2132,plain,
n4(X1655,b),
inference(resolution,[status(thm)],[c2126,c2054]) ).
cnf(rule_224,axiom,
( l3(d,c)
| ~ s2(d)
| ~ k3(a,c,a)
| ~ r0(b) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_224) ).
cnf(c630,plain,
( p2(X1376,a,a)
| ~ p1(X1376,X1377,X1378)
| ~ l1(X1377,X1378) ),
inference(resolution,[status(thm)],[rule_146,c465]) ).
cnf(c1764,plain,
( p2(X1404,a,a)
| ~ l1(X1404,X1404) ),
inference(resolution,[status(thm)],[c630,c129]) ).
cnf(c1821,plain,
p2(c,a,a),
inference(resolution,[status(thm)],[c1764,c9]) ).
cnf(c1827,plain,
k3(a,c,a),
inference(resolution,[status(thm)],[c1821,rule_206]) ).
cnf(c1851,plain,
( l3(d,c)
| ~ s2(d)
| ~ r0(b) ),
inference(resolution,[status(thm)],[c1827,rule_224]) ).
cnf(c2108,plain,
( l3(d,c)
| ~ s2(d) ),
inference(resolution,[status(thm)],[c1851,axiom_9]) ).
cnf(c2109,plain,
l3(d,c),
inference(resolution,[status(thm)],[c2108,c387]) ).
cnf(axiom_21,axiom,
q0(b,e),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_21) ).
cnf(c125,plain,
( m1(X1137,a,e)
| ~ m0(a,X1138,a)
| ~ q0(X1137,e) ),
inference(resolution,[status(thm)],[rule_024,c72]) ).
cnf(c1389,plain,
( m1(X1140,a,e)
| ~ q0(X1140,e) ),
inference(resolution,[status(thm)],[c125,axiom_12]) ).
cnf(c1391,plain,
m1(b,a,e),
inference(resolution,[status(thm)],[c1389,axiom_21]) ).
cnf(axiom_6,axiom,
q0(b,b),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_6) ).
cnf(rule_034,axiom,
( m1(X136,X137,X137)
| ~ k1(a)
| ~ k1(X137)
| ~ q0(X136,X136) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_034) ).
cnf(c171,plain,
( m1(b,X751,X751)
| ~ k1(a)
| ~ k1(X751) ),
inference(resolution,[status(thm)],[rule_034,axiom_6]) ).
cnf(c915,plain,
( m1(b,a,a)
| ~ k1(a) ),
inference(factor,[status(thm)],[c171]) ).
cnf(c921,plain,
m1(b,a,a),
inference(resolution,[status(thm)],[c915,c6]) ).
cnf(c928,plain,
( m1(X1283,a,a)
| ~ m1(b,a,X1283) ),
inference(resolution,[status(thm)],[c921,rule_016]) ).
cnf(c1617,plain,
m1(e,a,a),
inference(resolution,[status(thm)],[c928,c1391]) ).
cnf(c1620,plain,
( q1(e,e,a)
| ~ r0(X1285) ),
inference(resolution,[status(thm)],[c1617,rule_113]) ).
cnf(c1621,plain,
q1(e,e,a),
inference(resolution,[status(thm)],[c1620,axiom_9]) ).
cnf(c1623,plain,
( q1(X1624,e,e)
| ~ k0(a)
| ~ l0(X1624) ),
inference(resolution,[status(thm)],[c1621,rule_099]) ).
cnf(c1619,plain,
( m1(X1622,a,a)
| ~ m1(e,a,X1622) ),
inference(resolution,[status(thm)],[c1617,rule_016]) ).
cnf(c170,plain,
( m1(d,X739,X739)
| ~ k1(a)
| ~ k1(X739) ),
inference(resolution,[status(thm)],[rule_034,axiom_17]) ).
cnf(c879,plain,
( m1(d,a,a)
| ~ k1(a) ),
inference(factor,[status(thm)],[c170]) ).
cnf(c885,plain,
m1(d,a,a),
inference(resolution,[status(thm)],[c879,c6]) ).
cnf(c887,plain,
( m1(X1264,a,a)
| ~ m1(d,a,X1264) ),
inference(resolution,[status(thm)],[c885,rule_016]) ).
cnf(c1596,plain,
m1(c,a,a),
inference(resolution,[status(thm)],[c887,c1396]) ).
cnf(c1601,plain,
( q1(c,c,a)
| ~ r0(X1265) ),
inference(resolution,[status(thm)],[c1596,rule_113]) ).
cnf(c1603,plain,
q1(c,c,a),
inference(resolution,[status(thm)],[c1601,axiom_9]) ).
cnf(c1605,plain,
( q1(X1620,c,c)
| ~ k0(a)
| ~ l0(X1620) ),
inference(resolution,[status(thm)],[c1603,rule_099]) ).
cnf(c2096,plain,
( q1(a,c,c)
| ~ k0(a) ),
inference(resolution,[status(thm)],[c1605,axiom_20]) ).
cnf(c1600,plain,
( m1(X1617,a,a)
| ~ m1(c,a,X1617) ),
inference(resolution,[status(thm)],[c1596,rule_016]) ).
cnf(c1126,plain,
( r3(X900,X901,X900)
| ~ k2(X901,X900)
| ~ r2(X900) ),
inference(resolution,[status(thm)],[rule_272,c280]) ).
cnf(c2089,plain,
( r3(a,c,a)
| ~ r2(a) ),
inference(resolution,[status(thm)],[c2082,c1126]) ).
cnf(c2093,plain,
r3(a,c,a),
inference(resolution,[status(thm)],[c2089,c549]) ).
cnf(rule_231,axiom,
( m3(X598,X599,X598)
| ~ r2(X598)
| ~ k2(c,X599) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_231) ).
cnf(c2083,plain,
( m3(X1608,a,X1608)
| ~ r2(X1608) ),
inference(resolution,[status(thm)],[c2082,rule_231]) ).
cnf(c2091,plain,
m3(c,a,c),
inference(resolution,[status(thm)],[c2083,c548]) ).
cnf(c1012,plain,
( p3(d,X824,X825)
| ~ k2(X824,X825) ),
inference(resolution,[status(thm)],[rule_241,c874]) ).
cnf(c2088,plain,
p3(d,c,a),
inference(resolution,[status(thm)],[c2082,c1012]) ).
cnf(rule_010,axiom,
( m1(X64,X64,c)
| ~ n0(X63,X63)
| ~ l1(c,c)
| ~ p0(X63,X64) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_010) ).
cnf(c60,plain,
( m1(b,b,c)
| ~ n0(c,c)
| ~ l1(c,c) ),
inference(resolution,[status(thm)],[rule_010,axiom_18]) ).
cnf(c1356,plain,
( m1(b,b,c)
| ~ n0(c,c) ),
inference(resolution,[status(thm)],[c60,c9]) ).
cnf(c560,plain,
k3(c,c,b),
inference(resolution,[status(thm)],[c554,rule_194]) ).
cnf(rule_242,axiom,
( p3(X630,X628,X629)
| ~ r2(X628)
| ~ k3(X628,X629,X630) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_242) ).
cnf(c726,plain,
( p3(b,c,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[rule_242,c560]) ).
cnf(c735,plain,
p3(b,c,c),
inference(resolution,[status(thm)],[c726,c548]) ).
cnf(c765,plain,
( n4(b,c)
| ~ n4(b,b) ),
inference(resolution,[status(thm)],[rule_281,c735]) ).
cnf(c2057,plain,
n4(b,c),
inference(resolution,[status(thm)],[c2054,c765]) ).
cnf(rule_304,axiom,
( m5(X11,X11)
| ~ k4(X11) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_304) ).
cnf(c2055,plain,
m5(c,c),
inference(resolution,[status(thm)],[c2053,rule_304]) ).
cnf(rule_201,axiom,
( k3(X705,X705,X704)
| ~ p1(X704,X707,X705)
| ~ m2(X706)
| ~ m2(X707) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_201) ).
cnf(c957,plain,
( k3(a,a,X1052)
| ~ m2(X1050)
| ~ m2(X1051) ),
inference(resolution,[status(thm)],[c953,rule_201]) ).
cnf(c1297,plain,
( k3(a,a,X1057)
| ~ m2(X1056) ),
inference(factor,[status(thm)],[c957]) ).
cnf(c1305,plain,
k3(a,a,X1058),
inference(resolution,[status(thm)],[c1297,c43]) ).
cnf(c1308,plain,
( p3(X1067,a,a)
| ~ r2(a) ),
inference(resolution,[status(thm)],[c1305,rule_242]) ).
cnf(c1313,plain,
p3(X1068,a,a),
inference(resolution,[status(thm)],[c1308,c549]) ).
cnf(c1314,plain,
( n4(X1069,a)
| ~ n4(X1069,X1069) ),
inference(resolution,[status(thm)],[c1313,rule_281]) ).
cnf(c2062,plain,
n4(X1585,a),
inference(resolution,[status(thm)],[c2054,c1314]) ).
cnf(rule_285,axiom,
( p4(X684,X684,X685)
| ~ r0(X684)
| ~ r3(X685,X684,X685) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_285) ).
cnf(axiom_16,axiom,
m0(c,b,a),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_16) ).
cnf(c958,plain,
p1(b,X794,c),
inference(resolution,[status(thm)],[c955,axiom_16]) ).
cnf(c255,plain,
p2(b,c,b),
inference(resolution,[status(thm)],[rule_176,c197]) ).
cnf(c631,plain,
( p2(b,c,c)
| ~ p1(b,X1380,X1381)
| ~ l1(X1380,X1381) ),
inference(resolution,[status(thm)],[rule_146,c255]) ).
cnf(c1773,plain,
( p2(b,c,c)
| ~ l1(X1563,c) ),
inference(resolution,[status(thm)],[c631,c958]) ).
cnf(c2044,plain,
p2(b,c,c),
inference(resolution,[status(thm)],[c1773,c9]) ).
cnf(c2049,plain,
r3(b,c,b),
inference(resolution,[status(thm)],[c2044,rule_267]) ).
cnf(c2051,plain,
( p4(c,c,b)
| ~ r0(c) ),
inference(resolution,[status(thm)],[c2049,rule_285]) ).
cnf(c2036,plain,
q3(b,d),
inference(resolution,[status(thm)],[c2000,axiom_7]) ).
cnf(c2039,plain,
( q3(d,b)
| ~ s2(d) ),
inference(resolution,[status(thm)],[c2036,c1068]) ).
cnf(c2041,plain,
q3(d,b),
inference(resolution,[status(thm)],[c2039,c387]) ).
cnf(c799,plain,
( k3(X1526,c,X1526)
| ~ s1(c)
| ~ n0(X1526,b) ),
inference(resolution,[status(thm)],[rule_192,c255]) ).
cnf(c1996,plain,
( q4(X1520,b)
| ~ k3(X1519,X1519,X1520) ),
inference(resolution,[status(thm)],[c1995,c1228]) ).
cnf(c2021,plain,
q4(X1521,b),
inference(resolution,[status(thm)],[c1996,c1181]) ).
cnf(c1985,plain,
( q3(e,X1517)
| ~ n0(X1517,e) ),
inference(resolution,[status(thm)],[c1981,rule_255]) ).
cnf(c261,plain,
p2(e,c,e),
inference(resolution,[status(thm)],[rule_176,c190]) ).
cnf(c790,plain,
( k3(X1515,c,X1515)
| ~ s1(c)
| ~ n0(X1515,e) ),
inference(resolution,[status(thm)],[rule_192,c261]) ).
cnf(c1982,plain,
( q4(X1510,e)
| ~ k3(X1509,X1509,X1510) ),
inference(resolution,[status(thm)],[c1981,c1228]) ).
cnf(c2003,plain,
q4(X1511,e),
inference(resolution,[status(thm)],[c1982,c1181]) ).
cnf(c1990,plain,
s3(e,X1503),
inference(resolution,[status(thm)],[c1986,c1155]) ).
cnf(c1756,plain,
( p2(X1471,a,a)
| ~ l1(d,X1471) ),
inference(resolution,[status(thm)],[c630,c1323]) ).
cnf(c1940,plain,
p2(X1472,a,a),
inference(resolution,[status(thm)],[c1756,c870]) ).
cnf(c1943,plain,
k3(a,X1474,a),
inference(resolution,[status(thm)],[c1940,rule_206]) ).
cnf(c1956,plain,
( p3(a,a,X1481)
| ~ r2(a) ),
inference(resolution,[status(thm)],[c1943,rule_242]) ).
cnf(c1966,plain,
p3(a,a,X1482),
inference(resolution,[status(thm)],[c1956,c549]) ).
cnf(c1948,plain,
r3(X1473,a,X1473),
inference(resolution,[status(thm)],[c1940,rule_267]) ).
cnf(c1953,plain,
( p4(a,a,X1480)
| ~ r0(a) ),
inference(resolution,[status(thm)],[c1948,rule_285]) ).
cnf(rule_235,axiom,
( m3(X623,X623,X622)
| ~ r2(X622)
| ~ k3(X623,X622,X623) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_235) ).
cnf(c1957,plain,
( m3(a,a,X1476)
| ~ r2(X1476) ),
inference(resolution,[status(thm)],[c1943,rule_235]) ).
cnf(c1959,plain,
m3(a,a,c),
inference(resolution,[status(thm)],[c1957,c548]) ).
cnf(c1925,plain,
( p3(b,b,X1465)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c1912,rule_242]) ).
cnf(c1917,plain,
r3(X1450,b,X1450),
inference(resolution,[status(thm)],[c1909,rule_267]) ).
cnf(c1922,plain,
( p4(b,b,X1461)
| ~ r0(b) ),
inference(resolution,[status(thm)],[c1917,rule_285]) ).
cnf(c1935,plain,
p4(b,b,X1462),
inference(resolution,[status(thm)],[c1922,axiom_9]) ).
cnf(c1936,plain,
( m5(b,X1463)
| ~ r0(b) ),
inference(resolution,[status(thm)],[c1935,rule_303]) ).
cnf(c1938,plain,
m5(b,X1464),
inference(resolution,[status(thm)],[c1936,axiom_9]) ).
cnf(c1926,plain,
( m3(b,b,X1454)
| ~ r2(X1454) ),
inference(resolution,[status(thm)],[c1912,rule_235]) ).
cnf(c1928,plain,
m3(b,b,c),
inference(resolution,[status(thm)],[c1926,c548]) ).
cnf(c689,plain,
( p2(X1453,X1453,X1452)
| ~ q1(c,X1453,b)
| ~ s1(c)
| ~ s0(e) ),
inference(resolution,[status(thm)],[rule_158,c254]) ).
cnf(c688,plain,
( p2(X1445,X1445,X1444)
| ~ q1(c,X1445,e)
| ~ s1(c)
| ~ s0(e) ),
inference(resolution,[status(thm)],[rule_158,c256]) ).
cnf(c1875,plain,
k3(e,X1425,e),
inference(resolution,[status(thm)],[c1871,rule_206]) ).
cnf(c1888,plain,
( p3(e,e,X1440)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c1875,rule_242]) ).
cnf(c1885,plain,
( p4(e,e,X1434)
| ~ r0(e) ),
inference(resolution,[status(thm)],[c1880,rule_285]) ).
cnf(c1902,plain,
p4(e,e,X1435),
inference(resolution,[status(thm)],[c1885,axiom_13]) ).
cnf(c1903,plain,
( m5(e,X1438)
| ~ r0(e) ),
inference(resolution,[status(thm)],[c1902,rule_303]) ).
cnf(c1907,plain,
m5(e,X1439),
inference(resolution,[status(thm)],[c1903,axiom_13]) ).
cnf(rule_234,axiom,
( m3(X791,e,e)
| ~ n2(e)
| ~ p2(X791,e,e) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_234) ).
cnf(c1874,plain,
( m3(X1429,e,e)
| ~ n2(e) ),
inference(resolution,[status(thm)],[c1871,rule_234]) ).
cnf(c1897,plain,
m3(X1430,e,e),
inference(resolution,[status(thm)],[c1874,c130]) ).
cnf(c1889,plain,
( m3(e,e,X1426)
| ~ r2(X1426) ),
inference(resolution,[status(thm)],[c1875,rule_235]) ).
cnf(c451,plain,
q1(X424,c,X424),
inference(resolution,[status(thm)],[c449,axiom_26]) ).
cnf(c683,plain,
( p2(a,e,c)
| ~ n1(e,a,a) ),
inference(resolution,[status(thm)],[rule_156,c451]) ).
cnf(c1212,plain,
q2(e,c,e),
inference(resolution,[status(thm)],[c1207,c2]) ).
cnf(c1700,plain,
( q4(e,c)
| ~ k3(X1412,X1412,e) ),
inference(resolution,[status(thm)],[c1228,c1212]) ).
cnf(c1863,plain,
q4(e,c),
inference(resolution,[status(thm)],[c1700,c1181]) ).
cnf(c456,plain,
q1(X432,d,X432),
inference(resolution,[status(thm)],[c449,axiom_34]) ).
cnf(c679,plain,
( p2(a,e,d)
| ~ n1(e,a,a) ),
inference(resolution,[status(thm)],[rule_156,c456]) ).
cnf(c1493,plain,
q2(e,c,b),
inference(resolution,[status(thm)],[c1490,c1]) ).
cnf(c1697,plain,
( q4(b,c)
| ~ k3(X1409,X1409,b) ),
inference(resolution,[status(thm)],[c1228,c1493]) ).
cnf(c1859,plain,
q4(b,c),
inference(resolution,[status(thm)],[c1697,c1181]) ).
cnf(c452,plain,
q1(X428,b,X428),
inference(resolution,[status(thm)],[c449,axiom_7]) ).
cnf(c678,plain,
( p2(a,e,b)
| ~ n1(e,a,a) ),
inference(resolution,[status(thm)],[rule_156,c452]) ).
cnf(c1466,plain,
k3(b,b,a),
inference(resolution,[status(thm)],[c1464,rule_194]) ).
cnf(c1492,plain,
q2(e,c,a),
inference(resolution,[status(thm)],[c1490,c6]) ).
cnf(c1694,plain,
( q4(a,c)
| ~ k3(X1407,X1407,a) ),
inference(resolution,[status(thm)],[c1228,c1492]) ).
cnf(c1854,plain,
q4(a,c),
inference(resolution,[status(thm)],[c1694,c1466]) ).
cnf(c676,plain,
( p2(d,e,a)
| ~ n1(e,d,a) ),
inference(resolution,[status(thm)],[rule_156,c505]) ).
cnf(c1693,plain,
( q4(d,X1388)
| ~ k3(X1387,X1387,d) ),
inference(resolution,[status(thm)],[c1228,c874]) ).
cnf(c1782,plain,
q4(d,X1389),
inference(resolution,[status(thm)],[c1693,c1181]) ).
cnf(rule_302,axiom,
( l5(X255)
| ~ q4(X256,X256)
| ~ k1(X255) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_302) ).
cnf(c1737,plain,
( l5(X1379)
| ~ k1(X1379) ),
inference(resolution,[status(thm)],[c1726,rule_302]) ).
cnf(c1772,plain,
l5(e),
inference(resolution,[status(thm)],[c1737,c2]) ).
cnf(c1771,plain,
l5(c),
inference(resolution,[status(thm)],[c1737,c0]) ).
cnf(c1770,plain,
l5(b),
inference(resolution,[status(thm)],[c1737,c1]) ).
cnf(c1769,plain,
l5(a),
inference(resolution,[status(thm)],[c1737,c6]) ).
cnf(c1768,plain,
l5(d),
inference(resolution,[status(thm)],[c1737,c5]) ).
cnf(c1031,plain,
p3(d,X826,X826),
inference(resolution,[status(thm)],[c1012,c211]) ).
cnf(c1039,plain,
( n4(d,X837)
| ~ n4(d,d) ),
inference(resolution,[status(thm)],[c1031,rule_281]) ).
cnf(rule_202,axiom,
( k3(X710,X710,X714)
| ~ q0(X713,X714)
| ~ k2(X710,X711)
| ~ k3(X714,X712,X711) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_202) ).
cnf(c970,plain,
( k3(X872,X872,d)
| ~ m2(X870)
| ~ m2(X871) ),
inference(resolution,[status(thm)],[c961,rule_201]) ).
cnf(c1094,plain,
( k3(X874,X874,d)
| ~ m2(X873) ),
inference(factor,[status(thm)],[c970]) ).
cnf(c1097,plain,
k3(X875,X875,d),
inference(resolution,[status(thm)],[c1094,c43]) ).
cnf(c1102,plain,
( k3(X1317,X1317,X1319)
| ~ q0(X1318,X1319)
| ~ k2(X1317,d) ),
inference(resolution,[status(thm)],[c1097,rule_202]) ).
cnf(c1639,plain,
( k3(X1320,X1320,X1322)
| ~ q0(X1321,X1322) ),
inference(resolution,[status(thm)],[c1102,c1175]) ).
cnf(c1646,plain,
k3(X1330,X1330,e),
inference(resolution,[status(thm)],[c1639,axiom_21]) ).
cnf(rule_282,axiom,
( n4(d,d)
| ~ k3(c,c,e)
| ~ q1(d,d,d) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_282) ).
cnf(c1176,plain,
( n4(d,d)
| ~ k3(c,c,e) ),
inference(resolution,[status(thm)],[rule_282,c208]) ).
cnf(c1689,plain,
n4(d,d),
inference(resolution,[status(thm)],[c1176,c1646]) ).
cnf(c1690,plain,
n4(d,X1357),
inference(resolution,[status(thm)],[c1689,c1039]) ).
cnf(c1430,plain,
( m3(X1191,b,X1191)
| ~ r2(X1191) ),
inference(resolution,[status(thm)],[c1429,rule_231]) ).
cnf(c1438,plain,
m3(c,b,c),
inference(resolution,[status(thm)],[c1430,c548]) ).
cnf(c1671,plain,
( r3(c,c,X1353)
| ~ m2(X1353) ),
inference(resolution,[status(thm)],[c1104,c1438]) ).
cnf(c1684,plain,
r3(c,c,d),
inference(resolution,[status(thm)],[c1671,c233]) ).
cnf(c1686,plain,
p4(d,c,c),
inference(resolution,[status(thm)],[c1684,c1193]) ).
cnf(c1688,plain,
( m5(d,c)
| ~ r0(d) ),
inference(resolution,[status(thm)],[c1686,rule_303]) ).
cnf(c789,plain,
( k3(X697,X698,X697)
| ~ s1(X698)
| ~ n0(X697,X698) ),
inference(resolution,[status(thm)],[rule_192,c251]) ).
cnf(c815,plain,
( k3(b,a,b)
| ~ s1(a) ),
inference(resolution,[status(thm)],[c789,axiom_37]) ).
cnf(c829,plain,
k3(b,a,b),
inference(resolution,[status(thm)],[c815,c223]) ).
cnf(c831,plain,
( m3(b,b,a)
| ~ r2(a) ),
inference(resolution,[status(thm)],[c829,rule_235]) ).
cnf(c865,plain,
m3(b,b,a),
inference(resolution,[status(thm)],[c831,c549]) ).
cnf(c1669,plain,
( r3(a,a,X1351)
| ~ m2(X1351) ),
inference(resolution,[status(thm)],[c1104,c865]) ).
cnf(c1678,plain,
r3(a,a,d),
inference(resolution,[status(thm)],[c1669,c233]) ).
cnf(c1680,plain,
p4(d,a,a),
inference(resolution,[status(thm)],[c1678,c1193]) ).
cnf(c1682,plain,
( m5(d,a)
| ~ r0(d) ),
inference(resolution,[status(thm)],[c1680,rule_303]) ).
cnf(c1668,plain,
( r3(b,b,X1350)
| ~ m2(X1350) ),
inference(resolution,[status(thm)],[c1104,c131]) ).
cnf(c1674,plain,
r3(b,b,d),
inference(resolution,[status(thm)],[c1668,c233]) ).
cnf(c1675,plain,
p4(d,b,b),
inference(resolution,[status(thm)],[c1674,c1193]) ).
cnf(c1676,plain,
( m5(d,b)
| ~ r0(d) ),
inference(resolution,[status(thm)],[c1675,rule_303]) ).
cnf(c1683,plain,
r3(c,c,b),
inference(resolution,[status(thm)],[c1671,c43]) ).
cnf(c1685,plain,
p4(b,c,c),
inference(resolution,[status(thm)],[c1683,c1193]) ).
cnf(c1677,plain,
r3(a,a,b),
inference(resolution,[status(thm)],[c1669,c43]) ).
cnf(c1679,plain,
p4(b,a,a),
inference(resolution,[status(thm)],[c1677,c1193]) ).
cnf(axiom_29,axiom,
q0(d,b),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_29) ).
cnf(c1642,plain,
k3(X1325,X1325,b),
inference(resolution,[status(thm)],[c1639,axiom_29]) ).
cnf(c1651,plain,
( p3(b,X1340,X1340)
| ~ r2(X1340) ),
inference(resolution,[status(thm)],[c1642,rule_242]) ).
cnf(c1641,plain,
k3(X1324,X1324,c),
inference(resolution,[status(thm)],[c1639,axiom_33]) ).
cnf(c1648,plain,
( p3(c,X1338,X1338)
| ~ r2(X1338) ),
inference(resolution,[status(thm)],[c1641,rule_242]) ).
cnf(c1653,plain,
p4(X1333,e,X1333),
inference(resolution,[status(thm)],[c1646,rule_287]) ).
cnf(c1650,plain,
p4(X1332,b,X1332),
inference(resolution,[status(thm)],[c1642,rule_287]) ).
cnf(c1647,plain,
p4(X1331,c,X1331),
inference(resolution,[status(thm)],[c1641,rule_287]) ).
cnf(rule_011,axiom,
( m1(X66,X66,X65)
| ~ k0(X66)
| ~ n0(X65,X65) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_011) ).
cnf(c65,plain,
( m1(X156,X156,e)
| ~ k0(X156) ),
inference(resolution,[status(thm)],[rule_011,axiom_30]) ).
cnf(c187,plain,
m1(b,b,e),
inference(resolution,[status(thm)],[c65,axiom_32]) ).
cnf(c82,plain,
( m1(X279,X278,X278)
| ~ m1(X278,X278,X279) ),
inference(resolution,[status(thm)],[rule_016,c41]) ).
cnf(c326,plain,
m1(e,b,b),
inference(resolution,[status(thm)],[c82,c187]) ).
cnf(rule_083,axiom,
( p1(X378,b,X377)
| ~ m1(X378,X377,b)
| ~ k0(X377) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_083) ).
cnf(c407,plain,
( p1(e,b,b)
| ~ k0(b) ),
inference(resolution,[status(thm)],[rule_083,c326]) ).
cnf(c514,plain,
p1(e,b,b),
inference(resolution,[status(thm)],[c407,axiom_32]) ).
cnf(c515,plain,
( p1(b,X1314,e)
| ~ m0(e,b,b) ),
inference(resolution,[status(thm)],[c514,rule_082]) ).
cnf(rule_109,axiom,
( q1(X473,X473,X472)
| ~ p0(X471,X471)
| ~ q0(X472,X473)
| ~ k1(X473) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_109) ).
cnf(c492,plain,
( q1(d,d,X1290)
| ~ p0(X1291,X1291)
| ~ k1(d) ),
inference(resolution,[status(thm)],[rule_109,axiom_17]) ).
cnf(c1626,plain,
( q1(d,d,X1292)
| ~ k1(d) ),
inference(resolution,[status(thm)],[c492,axiom_14]) ).
cnf(c1627,plain,
q1(d,d,X1293),
inference(resolution,[status(thm)],[c1626,c5]) ).
cnf(c1629,plain,
( q1(X1295,d,d)
| ~ k0(X1294)
| ~ l0(X1295) ),
inference(resolution,[status(thm)],[c1627,rule_099]) ).
cnf(c919,plain,
( m1(b,c,c)
| ~ k1(a) ),
inference(resolution,[status(thm)],[c171,c0]) ).
cnf(c933,plain,
m1(b,c,c),
inference(resolution,[status(thm)],[c919,c6]) ).
cnf(c935,plain,
( m1(X1289,c,c)
| ~ m1(b,c,X1289) ),
inference(resolution,[status(thm)],[c933,rule_016]) ).
cnf(c884,plain,
( m1(d,e,e)
| ~ k1(a) ),
inference(resolution,[status(thm)],[c170,c2]) ).
cnf(c904,plain,
m1(d,e,e),
inference(resolution,[status(thm)],[c884,c6]) ).
cnf(c906,plain,
( m1(X1279,e,e)
| ~ m1(d,e,X1279) ),
inference(resolution,[status(thm)],[c904,rule_016]) ).
cnf(c883,plain,
( m1(d,c,c)
| ~ k1(a) ),
inference(resolution,[status(thm)],[c170,c0]) ).
cnf(c897,plain,
m1(d,c,c),
inference(resolution,[status(thm)],[c883,c6]) ).
cnf(c899,plain,
( m1(X1276,c,c)
| ~ m1(d,c,X1276) ),
inference(resolution,[status(thm)],[c897,rule_016]) ).
cnf(c882,plain,
( m1(d,b,b)
| ~ k1(a) ),
inference(resolution,[status(thm)],[c170,c1]) ).
cnf(c892,plain,
m1(d,b,b),
inference(resolution,[status(thm)],[c882,c6]) ).
cnf(c895,plain,
( m1(X1271,b,b)
| ~ m1(d,b,X1271) ),
inference(resolution,[status(thm)],[c892,rule_016]) ).
cnf(rule_094,axiom,
( q1(b,e,e)
| ~ s0(e)
| ~ k0(b)
| ~ l0(c) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_094) ).
cnf(c450,plain,
( q1(b,e,e)
| ~ s0(e)
| ~ k0(b) ),
inference(resolution,[status(thm)],[rule_094,axiom_24]) ).
cnf(c1602,plain,
( q1(b,e,e)
| ~ s0(e) ),
inference(resolution,[status(thm)],[c450,axiom_32]) ).
cnf(c798,plain,
( k3(X1255,a,X1255)
| ~ s1(a)
| ~ n0(X1255,X1254) ),
inference(resolution,[status(thm)],[rule_192,c465]) ).
cnf(c1583,plain,
( k3(d,a,d)
| ~ s1(a) ),
inference(resolution,[status(thm)],[c798,axiom_26]) ).
cnf(c1591,plain,
k3(d,a,d),
inference(resolution,[status(thm)],[c1583,c223]) ).
cnf(c1593,plain,
( m3(d,d,a)
| ~ r2(a) ),
inference(resolution,[status(thm)],[c1591,rule_235]) ).
cnf(c1595,plain,
m3(d,d,a),
inference(resolution,[status(thm)],[c1593,c549]) ).
cnf(c1592,plain,
( p3(d,d,a)
| ~ r2(d) ),
inference(resolution,[status(thm)],[c1591,rule_242]) ).
cnf(c398,plain,
( p1(c,X1252,c)
| ~ m0(c,c,e) ),
inference(resolution,[status(thm)],[rule_082,c351]) ).
cnf(c796,plain,
( k3(X1250,b,X1250)
| ~ s1(b)
| ~ n0(X1250,X1251) ),
inference(resolution,[status(thm)],[rule_192,c254]) ).
cnf(rule_037,axiom,
( n1(X146,X147,X146)
| ~ p0(X148,X146)
| ~ l0(X147)
| ~ r0(X146) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_037) ).
cnf(c183,plain,
( n1(X342,X343,X342)
| ~ l0(X343)
| ~ r0(X342) ),
inference(resolution,[status(thm)],[rule_037,axiom_14]) ).
cnf(c372,plain,
( n1(e,X345,e)
| ~ l0(X345) ),
inference(resolution,[status(thm)],[c183,axiom_13]) ).
cnf(c378,plain,
n1(e,a,e),
inference(resolution,[status(thm)],[c372,axiom_20]) ).
cnf(c381,plain,
( n1(e,a,a)
| ~ l0(X1248)
| ~ l1(X1248,e) ),
inference(resolution,[status(thm)],[c378,rule_054]) ).
cnf(c1570,plain,
( n1(e,a,a)
| ~ l0(d) ),
inference(resolution,[status(thm)],[c381,c870]) ).
cnf(c11,plain,
l1(e,e),
inference(resolution,[status(thm)],[rule_002,axiom_3]) ).
cnf(c1569,plain,
( n1(e,a,a)
| ~ l0(e) ),
inference(resolution,[status(thm)],[c381,c11]) ).
cnf(c1568,plain,
( n1(e,a,a)
| ~ l0(b) ),
inference(resolution,[status(thm)],[c381,c1330]) ).
cnf(c795,plain,
( k3(X1246,e,X1246)
| ~ s1(e)
| ~ n0(X1246,X1247) ),
inference(resolution,[status(thm)],[rule_192,c256]) ).
cnf(c371,plain,
( n1(b,X344,b)
| ~ l0(X344) ),
inference(resolution,[status(thm)],[c183,axiom_9]) ).
cnf(c373,plain,
n1(b,a,b),
inference(resolution,[status(thm)],[c371,axiom_20]) ).
cnf(c376,plain,
( n1(b,a,a)
| ~ l0(X1243)
| ~ l1(X1243,b) ),
inference(resolution,[status(thm)],[c373,rule_054]) ).
cnf(c1553,plain,
( n1(b,a,a)
| ~ l0(d) ),
inference(resolution,[status(thm)],[c376,c870]) ).
cnf(c10,plain,
l1(b,b),
inference(resolution,[status(thm)],[rule_002,axiom_7]) ).
cnf(c1552,plain,
( n1(b,a,a)
| ~ l0(b) ),
inference(resolution,[status(thm)],[c376,c10]) ).
cnf(rule_145,axiom,
( p2(e,X557,X558)
| ~ r0(e)
| ~ p1(X557,X558,e) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_145) ).
cnf(c1546,plain,
( p2(e,e,b)
| ~ r0(e) ),
inference(resolution,[status(thm)],[c1541,rule_145]) ).
cnf(c1554,plain,
p2(e,e,b),
inference(resolution,[status(thm)],[c1546,axiom_13]) ).
cnf(c1530,plain,
( p2(e,e,c)
| ~ r0(e) ),
inference(resolution,[status(thm)],[c1525,rule_145]) ).
cnf(c1547,plain,
p2(e,e,c),
inference(resolution,[status(thm)],[c1530,axiom_13]) ).
cnf(c1513,plain,
q2(b,c,e),
inference(resolution,[status(thm)],[c1508,c2]) ).
cnf(c1523,plain,
( q3(c,e)
| ~ n0(b,c) ),
inference(resolution,[status(thm)],[c1513,rule_255]) ).
cnf(c121,plain,
p1(b,b,c),
inference(resolution,[status(thm)],[rule_069,axiom_18]) ).
cnf(c360,plain,
( p1(c,b,c)
| ~ l0(X1238)
| ~ s0(b) ),
inference(resolution,[status(thm)],[rule_071,c121]) ).
cnf(c1531,plain,
( p1(c,b,c)
| ~ l0(X1239) ),
inference(resolution,[status(thm)],[c360,axiom_5]) ).
cnf(c1532,plain,
p1(c,b,c),
inference(resolution,[status(thm)],[c1531,axiom_20]) ).
cnf(c1510,plain,
q2(b,c,a),
inference(resolution,[status(thm)],[c1508,c6]) ).
cnf(c1518,plain,
( q3(c,a)
| ~ n0(b,c) ),
inference(resolution,[status(thm)],[c1510,rule_255]) ).
cnf(c1512,plain,
q2(b,c,c),
inference(resolution,[status(thm)],[c1508,c0]) ).
cnf(c1501,plain,
( q3(c,b)
| ~ n0(e,c) ),
inference(resolution,[status(thm)],[c1493,rule_255]) ).
cnf(c1499,plain,
( q3(c,a)
| ~ n0(e,c) ),
inference(resolution,[status(thm)],[c1492,rule_255]) ).
cnf(c1491,plain,
q2(e,c,d),
inference(resolution,[status(thm)],[c1490,c5]) ).
cnf(rule_166,axiom,
( p2(a,X635,d)
| ~ n0(X635,d)
| ~ m1(a,X635,d) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_166) ).
cnf(c731,plain,
( p2(a,d,d)
| ~ n0(d,d) ),
inference(resolution,[status(thm)],[rule_166,c309]) ).
cnf(c1479,plain,
( m3(X1211,e,X1211)
| ~ r2(X1211) ),
inference(resolution,[status(thm)],[c1478,rule_231]) ).
cnf(c1486,plain,
m3(c,e,c),
inference(resolution,[status(thm)],[c1479,c548]) ).
cnf(c1482,plain,
p3(d,c,e),
inference(resolution,[status(thm)],[c1478,c1012]) ).
cnf(c1471,plain,
p4(b,a,b),
inference(resolution,[status(thm)],[c1466,rule_287]) ).
cnf(c1467,plain,
p3(d,a,b),
inference(resolution,[status(thm)],[c1464,c1012]) ).
cnf(rule_039,axiom,
( n1(X159,c,X159)
| ~ m0(X158,X159,c) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_039) ).
cnf(c192,plain,
n1(b,c,b),
inference(resolution,[status(thm)],[rule_039,axiom_27]) ).
cnf(c291,plain,
( n1(b,c,c)
| ~ l0(X1202)
| ~ l1(X1202,b) ),
inference(resolution,[status(thm)],[rule_054,c192]) ).
cnf(c1460,plain,
( n1(b,c,c)
| ~ l0(d) ),
inference(resolution,[status(thm)],[c291,c870]) ).
cnf(c1459,plain,
( n1(b,c,c)
| ~ l0(b) ),
inference(resolution,[status(thm)],[c291,c10]) ).
cnf(axiom_35,axiom,
m0(d,e,c),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_35) ).
cnf(c194,plain,
n1(e,c,e),
inference(resolution,[status(thm)],[rule_039,axiom_35]) ).
cnf(c290,plain,
( n1(e,c,c)
| ~ l0(X1201)
| ~ l1(X1201,e) ),
inference(resolution,[status(thm)],[rule_054,c194]) ).
cnf(c1458,plain,
( n1(e,c,c)
| ~ l0(d) ),
inference(resolution,[status(thm)],[c290,c870]) ).
cnf(c1457,plain,
( n1(e,c,c)
| ~ l0(e) ),
inference(resolution,[status(thm)],[c290,c11]) ).
cnf(c1456,plain,
( n1(e,c,c)
| ~ l0(b) ),
inference(resolution,[status(thm)],[c290,c1330]) ).
cnf(c1447,plain,
k3(e,e,a),
inference(resolution,[status(thm)],[c1445,rule_194]) ).
cnf(c1452,plain,
p4(e,a,e),
inference(resolution,[status(thm)],[c1447,rule_287]) ).
cnf(c1448,plain,
p3(d,a,e),
inference(resolution,[status(thm)],[c1445,c1012]) ).
cnf(c193,plain,
n1(d,c,d),
inference(resolution,[status(thm)],[rule_039,axiom_19]) ).
cnf(c287,plain,
( n1(d,c,c)
| ~ l0(X1194)
| ~ l1(X1194,d) ),
inference(resolution,[status(thm)],[rule_054,c193]) ).
cnf(c1442,plain,
( n1(d,c,c)
| ~ l0(d) ),
inference(resolution,[status(thm)],[c287,c870]) ).
cnf(c1434,plain,
p3(d,c,b),
inference(resolution,[status(thm)],[c1429,c1012]) ).
cnf(rule_253,axiom,
( p3(b,c,b)
| ~ k2(c,b) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_253) ).
cnf(c1433,plain,
p3(b,c,b),
inference(resolution,[status(thm)],[c1429,rule_253]) ).
cnf(c501,plain,
( q1(e,e,b)
| ~ r0(X494) ),
inference(resolution,[status(thm)],[rule_113,c326]) ).
cnf(c511,plain,
q1(e,e,b),
inference(resolution,[status(thm)],[c501,axiom_9]) ).
cnf(c513,plain,
( q1(X1186,e,e)
| ~ k0(b)
| ~ l0(X1186) ),
inference(resolution,[status(thm)],[c511,rule_099]) ).
cnf(c1411,plain,
( q1(a,d,d)
| ~ k0(b) ),
inference(resolution,[status(thm)],[c483,axiom_20]) ).
cnf(c1413,plain,
q1(a,d,d),
inference(resolution,[status(thm)],[c1411,axiom_32]) ).
cnf(c361,plain,
( p1(b,X1160,b)
| ~ l0(X1161)
| ~ s0(b) ),
inference(resolution,[status(thm)],[rule_071,c122]) ).
cnf(c1404,plain,
( p1(b,X1162,b)
| ~ l0(X1163) ),
inference(resolution,[status(thm)],[c361,axiom_5]) ).
cnf(c1405,plain,
p1(b,X1164,b),
inference(resolution,[status(thm)],[c1404,axiom_20]) ).
cnf(c1407,plain,
( p1(X1167,X1166,b)
| ~ m0(b,X1167,b) ),
inference(resolution,[status(thm)],[c1405,rule_082]) ).
cnf(c329,plain,
( m1(X1159,b,b)
| ~ m1(e,b,X1159) ),
inference(resolution,[status(thm)],[c326,rule_016]) ).
cnf(rule_047,axiom,
( n1(X208,d,X209)
| ~ p0(X209,X209)
| ~ r0(X208)
| ~ l1(X209,d) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_047) ).
cnf(c246,plain,
( n1(X1152,d,d)
| ~ p0(d,d)
| ~ r0(X1152) ),
inference(resolution,[status(thm)],[rule_047,c14]) ).
cnf(c188,plain,
( m1(X1147,e,e)
| ~ m1(b,e,X1147) ),
inference(resolution,[status(thm)],[c187,rule_016]) ).
cnf(c1379,plain,
m1(d,a,b),
inference(resolution,[status(thm)],[c1377,axiom_29]) ).
cnf(c968,plain,
( p1(X864,X863,d)
| ~ m0(d,X864,X865) ),
inference(resolution,[status(thm)],[c961,rule_082]) ).
cnf(c1090,plain,
p1(e,X869,d),
inference(resolution,[status(thm)],[c968,axiom_35]) ).
cnf(c1091,plain,
( p1(X1124,X1123,e)
| ~ m0(e,X1124,d) ),
inference(resolution,[status(thm)],[c1090,rule_082]) ).
cnf(c61,plain,
( m1(X1116,X1116,c)
| ~ n0(b,b)
| ~ l1(c,c) ),
inference(resolution,[status(thm)],[rule_010,axiom_14]) ).
cnf(c1363,plain,
( m1(X1117,X1117,c)
| ~ n0(b,b) ),
inference(resolution,[status(thm)],[c61,c9]) ).
cnf(c23,plain,
( l1(e,d)
| ~ p0(c,e)
| ~ r0(X1104) ),
inference(resolution,[status(thm)],[rule_003,axiom_35]) ).
cnf(c972,plain,
( p1(X1103,X1102,b)
| ~ m0(b,X1103,c) ),
inference(resolution,[status(thm)],[c958,rule_082]) ).
cnf(c1343,plain,
( q3(b,e)
| ~ s2(b) ),
inference(resolution,[status(thm)],[c1342,c1068]) ).
cnf(c1345,plain,
q3(b,e),
inference(resolution,[status(thm)],[c1343,c784]) ).
cnf(axiom_38,axiom,
m0(b,a,a),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_38) ).
cnf(c21,plain,
( l1(a,b)
| ~ p0(a,a)
| ~ r0(X1101) ),
inference(resolution,[status(thm)],[rule_003,axiom_38]) ).
cnf(c1328,plain,
( p2(e,e,d)
| ~ r0(e) ),
inference(resolution,[status(thm)],[c1323,rule_145]) ).
cnf(c1337,plain,
p2(e,e,d),
inference(resolution,[status(thm)],[c1328,axiom_13]) ).
cnf(axiom_23,axiom,
m0(a,e,e),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',axiom_23) ).
cnf(c19,plain,
( l1(e,a)
| ~ p0(e,e)
| ~ r0(X1099) ),
inference(resolution,[status(thm)],[rule_003,axiom_23]) ).
cnf(c17,plain,
( l1(b,c)
| ~ p0(a,b)
| ~ r0(X1088) ),
inference(resolution,[status(thm)],[rule_003,axiom_16]) ).
cnf(rule_327,axiom,
( r5(X1070,X1071)
| ~ s4(X1070)
| ~ k0(b)
| ~ n3(X1071) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_327) ).
cnf(c1315,plain,
( r5(X1072,X1073)
| ~ s4(X1072)
| ~ k0(b) ),
inference(resolution,[status(thm)],[rule_327,c252]) ).
cnf(c1316,plain,
( r5(X1075,X1074)
| ~ s4(X1075) ),
inference(resolution,[status(thm)],[c1315,axiom_32]) ).
cnf(c1321,plain,
r5(d,X1083),
inference(resolution,[status(thm)],[c1316,c426]) ).
cnf(c424,plain,
s4(b),
inference(resolution,[status(thm)],[c421,c10]) ).
cnf(c1320,plain,
r5(b,X1082),
inference(resolution,[status(thm)],[c1316,c424]) ).
cnf(c425,plain,
s4(e),
inference(resolution,[status(thm)],[c421,c11]) ).
cnf(c1319,plain,
r5(e,X1078),
inference(resolution,[status(thm)],[c1316,c425]) ).
cnf(c1318,plain,
r5(a,X1077),
inference(resolution,[status(thm)],[c1316,c423]) ).
cnf(c422,plain,
s4(c),
inference(resolution,[status(thm)],[c421,c9]) ).
cnf(c1317,plain,
r5(c,X1076),
inference(resolution,[status(thm)],[c1316,c422]) ).
cnf(c1307,plain,
p4(a,X1060,a),
inference(resolution,[status(thm)],[c1305,rule_287]) ).
cnf(c839,plain,
( k3(b,b,X1034)
| ~ m2(X1033)
| ~ m2(X1034) ),
inference(resolution,[status(thm)],[rule_201,c122]) ).
cnf(c1283,plain,
( k3(b,b,X1035)
| ~ m2(X1035) ),
inference(factor,[status(thm)],[c839]) ).
cnf(c257,plain,
p2(d,X226,d),
inference(resolution,[status(thm)],[rule_176,c41]) ).
cnf(c792,plain,
( k3(X1027,X1026,X1027)
| ~ s1(X1026)
| ~ n0(X1027,d) ),
inference(resolution,[status(thm)],[rule_192,c257]) ).
cnf(c1272,plain,
( k3(c,X1028,c)
| ~ s1(X1028) ),
inference(resolution,[status(thm)],[c792,axiom_34]) ).
cnf(c1273,plain,
k3(c,X1029,c),
inference(resolution,[status(thm)],[c1272,c223]) ).
cnf(c1275,plain,
( p3(c,c,X1031)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c1273,rule_242]) ).
cnf(c1281,plain,
p3(c,c,X1032),
inference(resolution,[status(thm)],[c1275,c548]) ).
cnf(c1276,plain,
( m3(c,c,X1030)
| ~ r2(X1030) ),
inference(resolution,[status(thm)],[c1273,rule_235]) ).
cnf(c1279,plain,
m3(c,c,a),
inference(resolution,[status(thm)],[c1276,c549]) ).
cnf(c1222,plain,
( q3(c,e)
| ~ n0(e,c) ),
inference(resolution,[status(thm)],[c1212,rule_255]) ).
cnf(c1220,plain,
( q3(c,b)
| ~ n0(b,c) ),
inference(resolution,[status(thm)],[c1210,rule_255]) ).
cnf(rule_277,axiom,
( l4(X53)
| ~ p3(X51,X52,X53) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_277) ).
cnf(c134,plain,
l4(X111),
inference(resolution,[status(thm)],[c132,rule_277]) ).
cnf(rule_329,axiom,
( s5(X152)
| ~ l4(X152)
| ~ r4(X153) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_329) ).
cnf(c1257,plain,
( s5(X1019)
| ~ l4(X1019) ),
inference(resolution,[status(thm)],[c1256,rule_329]) ).
cnf(c1271,plain,
s5(X1020),
inference(resolution,[status(thm)],[c1257,c134]) ).
cnf(c1209,plain,
q2(a,c,a),
inference(resolution,[status(thm)],[c1207,c6]) ).
cnf(c1217,plain,
( q3(c,a)
| ~ n0(a,c) ),
inference(resolution,[status(thm)],[c1209,rule_255]) ).
cnf(c659,plain,
( m3(X600,c,X600)
| ~ r2(X600) ),
inference(resolution,[status(thm)],[rule_231,c211]) ).
cnf(c661,plain,
m3(a,c,a),
inference(resolution,[status(thm)],[c659,c549]) ).
cnf(rule_294,axiom,
( p4(c,c,X986)
| ~ n3(a)
| ~ m3(X986,c,a) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_294) ).
cnf(c1215,plain,
( p4(c,c,a)
| ~ n3(a) ),
inference(resolution,[status(thm)],[rule_294,c661]) ).
cnf(c1243,plain,
p4(c,c,a),
inference(resolution,[status(thm)],[c1215,c252]) ).
cnf(c1244,plain,
( m5(c,a)
| ~ r0(c) ),
inference(resolution,[status(thm)],[c1243,rule_303]) ).
cnf(c1239,plain,
( q3(d,c)
| ~ s2(d) ),
inference(resolution,[status(thm)],[c1238,c1068]) ).
cnf(c1240,plain,
q3(d,c),
inference(resolution,[status(thm)],[c1239,c387]) ).
cnf(c1233,plain,
s3(c,X992),
inference(resolution,[status(thm)],[c1223,c1155]) ).
cnf(c1186,plain,
( p3(X976,d,d)
| ~ r2(d) ),
inference(resolution,[status(thm)],[c1181,rule_242]) ).
cnf(c1179,plain,
( m3(X935,d,X935)
| ~ r2(X935) ),
inference(resolution,[status(thm)],[c1175,rule_231]) ).
cnf(c1191,plain,
m3(c,d,c),
inference(resolution,[status(thm)],[c1179,c548]) ).
cnf(c1185,plain,
p4(d,X932,d),
inference(resolution,[status(thm)],[c1181,rule_287]) ).
cnf(c1182,plain,
p3(d,X931,d),
inference(resolution,[status(thm)],[c1175,c1012]) ).
cnf(c1159,plain,
s3(b,X916),
inference(resolution,[status(thm)],[c1155,c784]) ).
cnf(c1158,plain,
s3(d,X912),
inference(resolution,[status(thm)],[c1155,c387]) ).
cnf(c877,plain,
( q3(X734,d)
| ~ n0(X734,X734) ),
inference(resolution,[status(thm)],[c874,rule_255]) ).
cnf(c878,plain,
q3(e,d),
inference(resolution,[status(thm)],[c877,axiom_30]) ).
cnf(rule_256,axiom,
( q3(X659,X659)
| ~ p2(X658,X659,X659)
| ~ q3(X658,X659) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_256) ).
cnf(c971,plain,
( p2(e,d,X797)
| ~ r0(e) ),
inference(resolution,[status(thm)],[c961,rule_145]) ).
cnf(c987,plain,
p2(e,d,X798),
inference(resolution,[status(thm)],[c971,axiom_13]) ).
cnf(c996,plain,
( q3(d,d)
| ~ q3(e,d) ),
inference(resolution,[status(thm)],[c987,rule_256]) ).
cnf(c1121,plain,
q3(d,d),
inference(resolution,[status(thm)],[c996,c878]) ).
cnf(c1099,plain,
p4(X881,d,X881),
inference(resolution,[status(thm)],[c1097,rule_287]) ).
cnf(c1080,plain,
q3(c,c),
inference(resolution,[status(thm)],[c1079,c548]) ).
cnf(c1072,plain,
( q3(d,e)
| ~ s2(d) ),
inference(resolution,[status(thm)],[c1068,c878]) ).
cnf(c1073,plain,
q3(d,e),
inference(resolution,[status(thm)],[c1072,c387]) ).
cnf(rule_155,axiom,
( p2(X601,X602,X602)
| ~ k1(X603)
| ~ p2(e,X601,X602) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_155) ).
cnf(c993,plain,
( p2(d,X801,X801)
| ~ k1(X800) ),
inference(resolution,[status(thm)],[c987,rule_155]) ).
cnf(c998,plain,
p2(d,X802,X802),
inference(resolution,[status(thm)],[c993,c5]) ).
cnf(c1006,plain,
k3(X811,d,X811),
inference(resolution,[status(thm)],[c998,rule_206]) ).
cnf(c1016,plain,
( m3(X833,X833,d)
| ~ r2(d) ),
inference(resolution,[status(thm)],[c1006,rule_235]) ).
cnf(c1038,plain,
p3(d,e,c),
inference(resolution,[status(thm)],[c1012,c594]) ).
cnf(c1037,plain,
p3(d,e,a),
inference(resolution,[status(thm)],[c1012,c592]) ).
cnf(c1036,plain,
p3(d,b,a),
inference(resolution,[status(thm)],[c1012,c552]) ).
cnf(c1035,plain,
p3(d,e,b),
inference(resolution,[status(thm)],[c1012,c593]) ).
cnf(c1034,plain,
p3(d,b,e),
inference(resolution,[status(thm)],[c1012,c555]) ).
cnf(c1033,plain,
p3(d,b,c),
inference(resolution,[status(thm)],[c1012,c554]) ).
cnf(rule_215,axiom,
( l3(X367,X368)
| ~ r0(X367)
| ~ p2(X367,X368,X367) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_215) ).
cnf(c989,plain,
( l3(e,d)
| ~ r0(e) ),
inference(resolution,[status(thm)],[c987,rule_215]) ).
cnf(c1029,plain,
l3(e,d),
inference(resolution,[status(thm)],[c989,axiom_13]) ).
cnf(c1009,plain,
r3(d,X812,d),
inference(resolution,[status(thm)],[c998,rule_267]) ).
cnf(c1018,plain,
( p4(X820,X820,d)
| ~ r0(X820) ),
inference(resolution,[status(thm)],[c1009,rule_285]) ).
cnf(c1015,plain,
( p3(X816,X816,d)
| ~ r2(X816) ),
inference(resolution,[status(thm)],[c1006,rule_242]) ).
cnf(c1011,plain,
( q3(X815,X815)
| ~ q3(d,X815) ),
inference(resolution,[status(thm)],[c998,rule_256]) ).
cnf(c994,plain,
r3(e,X799,e),
inference(resolution,[status(thm)],[c987,rule_267]) ).
cnf(c997,plain,
( p4(X813,X813,e)
| ~ r0(X813) ),
inference(resolution,[status(thm)],[c994,rule_285]) ).
cnf(c960,plain,
p1(a,X795,b),
inference(resolution,[status(thm)],[c955,axiom_38]) ).
cnf(c950,plain,
( m3(X773,d,d)
| ~ n2(X773) ),
inference(resolution,[status(thm)],[c947,c233]) ).
cnf(c952,plain,
m3(X774,d,d),
inference(resolution,[status(thm)],[c950,c130]) ).
cnf(c920,plain,
( m1(b,e,e)
| ~ k1(a) ),
inference(resolution,[status(thm)],[c171,c2]) ).
cnf(c940,plain,
m1(b,e,e),
inference(resolution,[status(thm)],[c920,c6]) ).
cnf(c943,plain,
( q1(b,b,e)
| ~ r0(X765) ),
inference(resolution,[status(thm)],[c940,rule_113]) ).
cnf(c944,plain,
q1(b,b,e),
inference(resolution,[status(thm)],[c943,axiom_9]) ).
cnf(c936,plain,
( q1(b,b,c)
| ~ r0(X760) ),
inference(resolution,[status(thm)],[c933,rule_113]) ).
cnf(c937,plain,
q1(b,b,c),
inference(resolution,[status(thm)],[c936,axiom_9]) ).
cnf(c929,plain,
( q1(b,b,a)
| ~ r0(X756) ),
inference(resolution,[status(thm)],[c921,rule_113]) ).
cnf(c930,plain,
q1(b,b,a),
inference(resolution,[status(thm)],[c929,axiom_9]) ).
cnf(c20,plain,
( l1(X723,a)
| ~ p0(a,X723)
| ~ r0(X724) ),
inference(resolution,[status(thm)],[rule_003,axiom_12]) ).
cnf(c811,plain,
( k3(d,e,d)
| ~ s1(e) ),
inference(resolution,[status(thm)],[c789,axiom_3]) ).
cnf(c823,plain,
k3(d,e,d),
inference(resolution,[status(thm)],[c811,c223]) ).
cnf(c825,plain,
( m3(d,d,e)
| ~ r2(e) ),
inference(resolution,[status(thm)],[c823,rule_235]) ).
cnf(c824,plain,
( p3(d,d,e)
| ~ r2(d) ),
inference(resolution,[status(thm)],[c823,rule_242]) ).
cnf(c810,plain,
( k3(d,b,d)
| ~ s1(b) ),
inference(resolution,[status(thm)],[c789,axiom_7]) ).
cnf(c820,plain,
k3(d,b,d),
inference(resolution,[status(thm)],[c810,c223]) ).
cnf(c822,plain,
( m3(d,d,b)
| ~ r2(b) ),
inference(resolution,[status(thm)],[c820,rule_235]) ).
cnf(c821,plain,
( p3(d,d,b)
| ~ r2(d) ),
inference(resolution,[status(thm)],[c820,rule_242]) ).
cnf(c809,plain,
( k3(d,c,d)
| ~ s1(c) ),
inference(resolution,[status(thm)],[c789,axiom_26]) ).
cnf(c817,plain,
k3(d,c,d),
inference(resolution,[status(thm)],[c809,c223]) ).
cnf(c819,plain,
( m3(d,d,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[c817,rule_235]) ).
cnf(c835,plain,
m3(d,d,c),
inference(resolution,[status(thm)],[c819,c548]) ).
cnf(c818,plain,
( p3(d,d,c)
| ~ r2(d) ),
inference(resolution,[status(thm)],[c817,rule_242]) ).
cnf(rule_180,axiom,
( q2(d,a,a)
| ~ q2(d,c,a)
| ~ s1(c)
| ~ q0(e,c) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_180) ).
cnf(c738,plain,
( q3(b,b)
| ~ n0(X654,b) ),
inference(resolution,[status(thm)],[rule_255,c527]) ).
cnf(c740,plain,
q3(b,b),
inference(resolution,[status(thm)],[c738,axiom_7]) ).
cnf(c736,plain,
( q3(X652,X652)
| ~ n0(X652,X652) ),
inference(resolution,[status(thm)],[rule_255,c272]) ).
cnf(c739,plain,
q3(e,e),
inference(resolution,[status(thm)],[c736,axiom_30]) ).
cnf(c663,plain,
( p2(c,e,e)
| ~ k1(X605) ),
inference(resolution,[status(thm)],[rule_155,c261]) ).
cnf(c669,plain,
p2(c,e,e),
inference(resolution,[status(thm)],[c663,c5]) ).
cnf(c674,plain,
k3(e,c,e),
inference(resolution,[status(thm)],[c669,rule_206]) ).
cnf(c711,plain,
( m3(e,e,c)
| ~ r2(c) ),
inference(resolution,[status(thm)],[rule_235,c674]) ).
cnf(c715,plain,
m3(e,e,c),
inference(resolution,[status(thm)],[c711,c548]) ).
cnf(c668,plain,
( p2(a,e,e)
| ~ k1(X618) ),
inference(resolution,[status(thm)],[rule_155,c465]) ).
cnf(c699,plain,
p2(a,e,e),
inference(resolution,[status(thm)],[c668,c5]) ).
cnf(c704,plain,
k3(e,a,e),
inference(resolution,[status(thm)],[c699,rule_206]) ).
cnf(c708,plain,
( m3(e,e,a)
| ~ r2(a) ),
inference(resolution,[status(thm)],[rule_235,c704]) ).
cnf(c714,plain,
m3(e,e,a),
inference(resolution,[status(thm)],[c708,c549]) ).
cnf(rule_152,axiom,
( p2(X587,X589,X589)
| ~ n1(X588,X589,X588)
| ~ p0(X587,X589)
| ~ p2(X587,X589,X587) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_152) ).
cnf(rule_149,axiom,
( p2(X577,X577,d)
| ~ r1(a)
| ~ m0(X578,X577,d) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_149) ).
cnf(c622,plain,
( p2(e,c,c)
| ~ r0(e) ),
inference(resolution,[status(thm)],[rule_145,c351]) ).
cnf(c641,plain,
p2(e,c,c),
inference(resolution,[status(thm)],[c622,axiom_13]) ).
cnf(rule_318,axiom,
( p5(X461,X461,X460)
| ~ s4(X460)
| ~ l2(X461,X461) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_318) ).
cnf(c634,plain,
( p5(X568,X568,X567)
| ~ s4(X567) ),
inference(resolution,[status(thm)],[c633,rule_318]) ).
cnf(c640,plain,
p5(X573,X573,d),
inference(resolution,[status(thm)],[c634,c426]) ).
cnf(c639,plain,
p5(X572,X572,b),
inference(resolution,[status(thm)],[c634,c424]) ).
cnf(c638,plain,
p5(X571,X571,e),
inference(resolution,[status(thm)],[c634,c425]) ).
cnf(c637,plain,
p5(X570,X570,a),
inference(resolution,[status(thm)],[c634,c423]) ).
cnf(c636,plain,
p5(X569,X569,c),
inference(resolution,[status(thm)],[c634,c422]) ).
cnf(c507,plain,
( q1(X505,X504,X504)
| ~ k0(d)
| ~ l0(X505) ),
inference(resolution,[status(thm)],[c505,rule_099]) ).
cnf(c521,plain,
( q1(c,X508,X508)
| ~ k0(d) ),
inference(resolution,[status(thm)],[c507,axiom_24]) ).
cnf(c520,plain,
( q1(a,X506,X506)
| ~ k0(d) ),
inference(resolution,[status(thm)],[c507,axiom_20]) ).
cnf(rule_107,axiom,
( q1(e,X458,X458)
| ~ m0(X458,d,X458)
| ~ m0(e,d,X458) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_107) ).
cnf(c486,plain,
( q1(e,X502,X502)
| ~ m0(X502,d,X502) ),
inference(resolution,[status(thm)],[rule_107,axiom_19]) ).
cnf(c518,plain,
q1(e,X503,X503),
inference(resolution,[status(thm)],[c486,axiom_19]) ).
cnf(c484,plain,
( m5(X459,X459)
| ~ r0(X459) ),
inference(resolution,[status(thm)],[rule_303,c296]) ).
cnf(c472,plain,
( q1(a,X450,X450)
| ~ k0(X450) ),
inference(resolution,[status(thm)],[c463,axiom_20]) ).
cnf(c476,plain,
q1(a,e,e),
inference(resolution,[status(thm)],[c472,axiom_28]) ).
cnf(rule_104,axiom,
( q1(X449,X448,X449)
| ~ l0(X449)
| ~ r0(X446)
| ~ p0(X447,X449)
| ~ q0(X448,X448) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_104) ).
cnf(c468,plain,
( l3(X440,a)
| ~ r0(X440) ),
inference(resolution,[status(thm)],[c465,rule_215]) ).
cnf(c453,plain,
q1(X429,e,X429),
inference(resolution,[status(thm)],[c449,axiom_3]) ).
cnf(rule_322,axiom,
( q5(X263,X262)
| ~ s4(X263)
| ~ m2(X262) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_322) ).
cnf(c299,plain,
( q5(X264,b)
| ~ s4(X264) ),
inference(resolution,[status(thm)],[rule_322,c43]) ).
cnf(c446,plain,
q5(d,b),
inference(resolution,[status(thm)],[c426,c299]) ).
cnf(c300,plain,
( q5(X267,d)
| ~ s4(X267) ),
inference(resolution,[status(thm)],[rule_322,c233]) ).
cnf(c443,plain,
q5(e,d),
inference(resolution,[status(thm)],[c425,c300]) ).
cnf(c442,plain,
q5(e,b),
inference(resolution,[status(thm)],[c425,c299]) ).
cnf(c439,plain,
q5(b,d),
inference(resolution,[status(thm)],[c424,c300]) ).
cnf(c435,plain,
q5(a,d),
inference(resolution,[status(thm)],[c423,c300]) ).
cnf(c434,plain,
q5(a,b),
inference(resolution,[status(thm)],[c423,c299]) ).
cnf(c431,plain,
q5(c,d),
inference(resolution,[status(thm)],[c422,c300]) ).
cnf(c429,plain,
q5(c,b),
inference(resolution,[status(thm)],[c422,c299]) ).
cnf(rule_300,axiom,
( k5(X326)
| ~ s4(X325)
| ~ r3(X324,X326,X326) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_300) ).
cnf(c364,plain,
( k5(X329)
| ~ s4(X330) ),
inference(resolution,[status(thm)],[rule_300,c280]) ).
cnf(c430,plain,
k5(X407),
inference(resolution,[status(thm)],[c422,c364]) ).
cnf(c400,plain,
( p1(X390,X389,X390)
| ~ m0(X390,X390,b) ),
inference(resolution,[status(thm)],[rule_082,c122]) ).
cnf(c395,plain,
( l3(b,c)
| ~ r0(b) ),
inference(resolution,[status(thm)],[rule_215,c255]) ).
cnf(c412,plain,
l3(b,c),
inference(resolution,[status(thm)],[c395,axiom_9]) ).
cnf(c391,plain,
( l3(e,c)
| ~ r0(e) ),
inference(resolution,[status(thm)],[rule_215,c261]) ).
cnf(c411,plain,
l3(e,c),
inference(resolution,[status(thm)],[c391,axiom_13]) ).
cnf(c260,plain,
p2(b,a,b),
inference(resolution,[status(thm)],[rule_176,c196]) ).
cnf(c390,plain,
( l3(b,a)
| ~ r0(b) ),
inference(resolution,[status(thm)],[rule_215,c260]) ).
cnf(c410,plain,
l3(b,a),
inference(resolution,[status(thm)],[c390,axiom_9]) ).
cnf(c258,plain,
p2(e,a,e),
inference(resolution,[status(thm)],[rule_176,c189]) ).
cnf(c388,plain,
( l3(e,a)
| ~ r0(e) ),
inference(resolution,[status(thm)],[rule_215,c258]) ).
cnf(c409,plain,
l3(e,a),
inference(resolution,[status(thm)],[c388,axiom_13]) ).
cnf(c392,plain,
( l3(d,X376)
| ~ r0(d) ),
inference(resolution,[status(thm)],[rule_215,c257]) ).
cnf(c394,plain,
( l3(X375,b)
| ~ r0(X375) ),
inference(resolution,[status(thm)],[rule_215,c254]) ).
cnf(c404,plain,
l3(e,b),
inference(resolution,[status(thm)],[c394,axiom_13]) ).
cnf(c393,plain,
( l3(X370,e)
| ~ r0(X370) ),
inference(resolution,[status(thm)],[rule_215,c256]) ).
cnf(c396,plain,
l3(b,e),
inference(resolution,[status(thm)],[c393,axiom_9]) ).
cnf(rule_077,axiom,
( p1(c,e,b)
| ~ m0(b,c,e) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_077) ).
cnf(rule_004,axiom,
( l1(X22,X22)
| ~ k1(X22)
| ~ l0(X23)
| ~ l1(X23,X23) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_004) ).
cnf(c27,plain,
( l1(X331,X331)
| ~ k1(X331)
| ~ l0(c) ),
inference(resolution,[status(thm)],[rule_004,c9]) ).
cnf(c365,plain,
( l1(X332,X332)
| ~ k1(X332) ),
inference(resolution,[status(thm)],[c27,axiom_24]) ).
cnf(rule_217,axiom,
( l3(X310,X310)
| ~ n2(X310)
| ~ m2(b) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_217) ).
cnf(c357,plain,
( l3(X311,X311)
| ~ n2(X311) ),
inference(resolution,[status(thm)],[rule_217,c43]) ).
cnf(c358,plain,
l3(X312,X312),
inference(resolution,[status(thm)],[c357,c130]) ).
cnf(c348,plain,
( p1(e,e,X298)
| ~ k0(X298) ),
inference(resolution,[status(thm)],[rule_063,axiom_3]) ).
cnf(rule_044,axiom,
( n1(X190,X189,X190)
| ~ p0(X190,X190)
| ~ p0(X189,X188) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_044) ).
cnf(c226,plain,
( n1(X289,b,X289)
| ~ p0(X289,X289) ),
inference(resolution,[status(thm)],[rule_044,axiom_14]) ).
cnf(c225,plain,
( n1(X288,c,X288)
| ~ p0(X288,X288) ),
inference(resolution,[status(thm)],[rule_044,axiom_18]) ).
cnf(c333,plain,
n1(b,e,e),
inference(resolution,[status(thm)],[c199,c1]) ).
cnf(rule_053,axiom,
( n1(a,X239,b)
| ~ p0(X239,d)
| ~ p0(a,b) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_053) ).
cnf(rule_031,axiom,
( m1(c,a,c)
| ~ r0(e)
| ~ m0(a,e,c)
| ~ r0(X128)
| ~ k0(e) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_031) ).
cnf(rule_029,axiom,
( m1(X124,X125,X124)
| ~ p0(X124,X125)
| ~ s0(X124) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_029) ).
cnf(c142,plain,
q1(b,c,c),
inference(resolution,[status(thm)],[rule_095,axiom_18]) ).
cnf(rule_324,axiom,
( q5(X13,X13)
| ~ l4(X13) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_324) ).
cnf(c135,plain,
q5(X112,X112),
inference(resolution,[status(thm)],[c134,rule_324]) ).
cnf(rule_328,axiom,
( r5(X14,X14)
| ~ k4(X14) ),
file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax',rule_328) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SYN720-1 : TPTP v8.1.2. Released v2.5.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n003.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 20:32:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 2.62/2.82 % Version: 1.5
% 2.62/2.82 % SZS status Satisfiable
% 2.62/2.82 % SZS output start Saturation
% See solution above
% 2.62/2.84
% 2.62/2.84 % Initial clauses : 368
% 2.62/2.84 % Processed clauses : 1380
% 2.62/2.84 % Factors computed : 10
% 2.62/2.84 % Resolvents computed: 2373
% 2.62/2.84 % Tautologies deleted: 20
% 2.62/2.84 % Forward subsumed : 1351
% 2.62/2.84 % Backward subsumed : 644
% 2.62/2.84 % -------- CPU Time ---------
% 2.62/2.84 % User time : 2.446 s
% 2.62/2.84 % System time : 0.018 s
% 2.62/2.84 % Total time : 2.464 s
%------------------------------------------------------------------------------