%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SYN237-1 : TPTP v9.2.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n031.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 : Tue May 5 05:36:32 PM UTC 2026
% Result : Unsatisfiable 0.32s 1.61s
% Output : CNFRefutation 0.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 362
% Syntax : Number of clauses : 725 ( 79 unt; 0 nHn; 711 RR)
% Number of literals : 2071 ( 0 equ;1348 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 49 ( 48 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 1228 ( 316 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(rule_096,axiom,
( q1(X1,X1,X1)
| ~ n1(X2,X3,X3)
| ~ p0(X2,X4)
| ~ m1(X1,X3,X2)
| ~ q1(X4,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_096) ).
cnf(rule_182,axiom,
( q2(X1,X2,X1)
| ~ p1(X1,X1,X3)
| ~ n1(X2,X1,X3)
| ~ q2(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_182) ).
cnf(rule_051,axiom,
( n1(X1,X1,X1)
| ~ m1(c,X1,X2)
| ~ m0(b,X2,c)
| ~ n1(X2,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_051) ).
cnf(rule_162,axiom,
( p2(b,c,c)
| ~ p1(X1,b,b)
| ~ n1(e,e,X1)
| ~ q1(e,c,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_162) ).
cnf(rule_295,axiom,
( q4(X1,X2)
| ~ k3(X3,X3,X1)
| ~ q2(X4,X2,X1)
| ~ m3(X4,X5,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_295) ).
cnf(rule_128,axiom,
( k2(X1,X1)
| ~ n1(e,d,X1)
| ~ m1(X1,e,X1)
| ~ q1(X1,X1,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_128) ).
cnf(rule_225,axiom,
( m3(X1,X2,X1)
| ~ m0(X3,X3,X2)
| ~ l2(X4,X1)
| ~ m0(X1,X4,X4)
| ~ s2(X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_225) ).
cnf(rule_292,axiom,
( p4(X1,X1,X1)
| ~ k3(X2,X3,X3)
| ~ n4(X1,X3)
| ~ p1(X3,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_292) ).
cnf(rule_262,axiom,
( r3(X1,X1,X1)
| ~ p1(X2,X3,X1)
| ~ l2(X3,X2)
| ~ r3(X1,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_262) ).
cnf(rule_146,axiom,
( p2(X1,X2,X2)
| ~ p1(X1,X3,X4)
| ~ l1(X3,X4)
| ~ p2(X1,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_146) ).
cnf(rule_152,axiom,
( p2(X1,X2,X2)
| ~ n1(X3,X2,X3)
| ~ p0(X1,X2)
| ~ p2(X1,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_152) ).
cnf(rule_138,axiom,
( n2(a)
| ~ m1(b,a,e)
| ~ k1(c)
| ~ n1(e,a,e)
| ~ q1(c,a,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_138) ).
cnf(rule_187,axiom,
( q2(X1,X2,X1)
| ~ r1(X2)
| ~ m0(X3,X4,X1)
| ~ k0(X2)
| ~ q2(X2,X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_187) ).
cnf(rule_024,axiom,
( m1(X1,a,X2)
| ~ m0(a,X3,a)
| ~ q0(X1,X2)
| ~ m1(X2,c,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_024) ).
cnf(rule_269,axiom,
( r3(a,a,e)
| ~ k2(a,a)
| ~ q2(X1,e,X1)
| ~ m2(b)
| ~ m3(a,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_269) ).
cnf(rule_243,axiom,
( p3(X1,d,e)
| ~ l3(b,e)
| ~ p2(d,b,c)
| ~ n3(X1)
| ~ q2(X1,d,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_243) ).
cnf(rule_158,axiom,
( p2(X1,X1,X2)
| ~ q1(c,X1,X3)
| ~ s1(c)
| ~ s0(e)
| ~ p2(X1,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_158) ).
cnf(rule_268,axiom,
( r3(X1,X1,X2)
| ~ m2(X2)
| ~ m3(X3,b,X1)
| ~ r3(X2,X4,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_268) ).
cnf(rule_185,axiom,
( q2(X1,X1,X1)
| ~ n1(X2,d,X3)
| ~ k1(X1)
| ~ q2(X3,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_185) ).
cnf(rule_200,axiom,
( k3(X1,X1,X1)
| ~ p2(X2,X3,e)
| ~ s1(X2)
| ~ k3(X1,X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_200) ).
cnf(rule_290,axiom,
( p4(X1,X1,X1)
| ~ m3(X2,X3,X1)
| ~ p4(X1,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_290) ).
cnf(rule_288,axiom,
( p4(X1,X2,X2)
| ~ r3(X2,X2,X1)
| ~ p4(X3,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_288) ).
cnf(rule_271,axiom,
( r3(X1,X1,X1)
| ~ p3(X2,X1,X3)
| ~ r3(X2,X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_271) ).
cnf(rule_251,axiom,
( p3(X1,X2,X2)
| ~ m3(X2,X3,X4)
| ~ p2(X1,X2,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_251) ).
cnf(rule_196,axiom,
( k3(X1,X1,X1)
| ~ p2(X2,X3,X2)
| ~ m1(X1,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_196) ).
cnf(rule_165,axiom,
( p2(X1,X1,X1)
| ~ q1(X2,X3,X2)
| ~ p2(X2,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_165) ).
cnf(rule_169,axiom,
( p2(X1,X1,X1)
| ~ q1(X2,X2,X2)
| ~ p1(X1,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_169) ).
cnf(rule_148,axiom,
( p2(X1,X1,X1)
| ~ m1(X2,X3,X1)
| ~ p2(X2,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_148) ).
cnf(rule_082,axiom,
( p1(X1,X2,X3)
| ~ m0(X3,X1,X4)
| ~ p1(X3,X1,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_082) ).
cnf(rule_062,axiom,
( n1(X1,X1,X1)
| ~ m0(X2,X2,X3)
| ~ n1(X2,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_062) ).
cnf(rule_059,axiom,
( n1(X1,X1,X2)
| ~ m0(X3,X4,X4)
| ~ m0(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_059) ).
cnf(rule_016,axiom,
( m1(X1,X2,X2)
| ~ m1(X3,X2,X1)
| ~ m1(X3,X4,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_016) ).
cnf(rule_263,axiom,
( r3(X1,X1,X1)
| ~ m0(d,X2,X1)
| ~ r3(X1,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_263) ).
cnf(rule_160,axiom,
( p2(X1,X1,X1)
| ~ m1(a,a,X2)
| ~ p2(a,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_160) ).
cnf(rule_107,axiom,
( q1(e,X1,X1)
| ~ m0(X1,d,X1)
| ~ m0(e,d,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_107) ).
cnf(rule_156,axiom,
( p2(X1,e,X2)
| ~ n1(e,X1,a)
| ~ q1(a,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_156) ).
cnf(rule_254,axiom,
( p3(e,b,e)
| ~ m3(e,X1,e)
| ~ q2(X1,X1,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_254) ).
cnf(rule_134,axiom,
( l2(X1,X1)
| ~ m0(X2,X1,X3)
| ~ m1(X3,X2,X2)
| ~ p0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_134) ).
cnf(rule_111,axiom,
( q1(d,d,c)
| ~ m0(c,b,a)
| ~ m1(c,d,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_111) ).
cnf(rule_226,axiom,
( m3(X1,X1,X1)
| ~ k2(X2,X3)
| ~ m3(X1,X3,X1)
| ~ n0(X3,a)
| ~ l2(a,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_226) ).
cnf(rule_273,axiom,
( s3(X1,X2)
| ~ q2(X3,X1,X3)
| ~ s2(X1)
| ~ m0(X3,X4,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_273) ).
cnf(rule_276,axiom,
( k4(e)
| ~ q3(X1,X1)
| ~ q1(a,a,X2)
| ~ r3(X1,e,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_276) ).
cnf(rule_316,axiom,
( n5(X1,X1)
| ~ p4(X2,X1,X1)
| ~ s1(X1)
| ~ p4(b,b,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_316) ).
cnf(rule_216,axiom,
( l3(X1,X1)
| ~ p1(X1,X1,X2)
| ~ p2(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_216) ).
cnf(rule_319,axiom,
( p5(X1,X2,X2)
| ~ l2(X1,X3)
| ~ p5(X1,X3,X1)
| ~ m4(X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_319) ).
cnf(rule_245,axiom,
( p3(X1,X1,X1)
| ~ l1(X2,X2)
| ~ l3(X2,X1)
| ~ p3(X3,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_245) ).
cnf(rule_202,axiom,
( k3(X1,X1,X2)
| ~ q0(X3,X2)
| ~ k2(X1,X4)
| ~ k3(X2,X5,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_202) ).
cnf(rule_209,axiom,
( k3(X1,X1,X1)
| ~ m2(X2)
| ~ l1(X3,X4)
| ~ s2(X1)
| ~ k3(X3,X4,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_209) ).
cnf(rule_052,axiom,
( n1(X1,X1,X1)
| ~ m0(X2,X2,X2)
| ~ k1(X1)
| ~ s0(X1)
| ~ p0(X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_052) ).
cnf(rule_144,axiom,
( p2(b,c,a)
| ~ r0(e)
| ~ n1(c,X1,X1)
| ~ p0(b,X1)
| ~ k2(c,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_144) ).
cnf(rule_108,axiom,
( q1(X1,X1,X1)
| ~ p0(X2,X3)
| ~ p1(X1,b,b)
| ~ q0(b,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_108) ).
cnf(rule_289,axiom,
( p4(X1,X1,X1)
| ~ l4(X1)
| ~ n0(X1,X2)
| ~ p4(X3,X4,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_289) ).
cnf(rule_261,axiom,
( r3(X1,X1,X1)
| ~ l1(X2,X3)
| ~ n1(X3,X3,X3)
| ~ r2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_261) ).
cnf(rule_272,axiom,
( r3(X1,X2,X3)
| ~ k2(X2,X3)
| ~ r2(X3)
| ~ r3(X3,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_272) ).
cnf(rule_192,axiom,
( k3(X1,X2,X1)
| ~ s1(X2)
| ~ p2(X3,X2,X4)
| ~ n0(X1,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_192) ).
cnf(rule_164,axiom,
( p2(X1,X1,X1)
| ~ p0(X1,X1)
| ~ r1(X2)
| ~ p2(X3,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_164) ).
cnf(rule_091,axiom,
( p1(X1,X1,X1)
| ~ q0(X2,X3)
| ~ k1(X4)
| ~ n1(X2,X1,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_091) ).
cnf(rule_080,axiom,
( p1(X1,X1,X1)
| ~ n0(X2,X2)
| ~ l0(X3)
| ~ n1(X2,X4,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_080) ).
cnf(rule_081,axiom,
( p1(X1,X1,X1)
| ~ m1(X2,X3,X1)
| ~ q0(X3,X4)
| ~ l0(X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_081) ).
cnf(rule_042,axiom,
( n1(X1,X1,X1)
| ~ m0(X2,X3,X2)
| ~ k0(X1)
| ~ q0(X4,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_042) ).
cnf(rule_054,axiom,
( n1(X1,X2,X2)
| ~ l0(X3)
| ~ l1(X3,X1)
| ~ n1(X1,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_054) ).
cnf(rule_168,axiom,
( p2(a,c,b)
| ~ l1(e,c)
| ~ l2(e,b)
| ~ r1(e)
| ~ m1(d,a,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_168) ).
cnf(rule_282,axiom,
( n4(d,d)
| ~ k3(c,c,e)
| ~ q1(d,d,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_282) ).
cnf(rule_307,axiom,
( n5(X1,X2)
| ~ q4(X3,X4)
| ~ n4(X1,X4)
| ~ p4(X5,X5,X2)
| ~ n5(X5,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_307) ).
cnf(rule_089,axiom,
( p1(d,d,X1)
| ~ s0(X1)
| ~ n1(c,d,X1)
| ~ r0(d)
| ~ n0(c,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_089) ).
cnf(rule_270,axiom,
( r3(X1,b,X1)
| ~ r0(X1)
| ~ p2(b,X1,b)
| ~ l2(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_270) ).
cnf(rule_101,axiom,
( q1(X1,X1,X1)
| ~ k1(X1)
| ~ q0(X1,b)
| ~ p1(b,b,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_101) ).
cnf(rule_178,axiom,
( q2(X1,X1,X1)
| ~ q0(X2,X1)
| ~ n1(X2,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_178) ).
cnf(rule_171,axiom,
( p2(X1,X1,X1)
| ~ n1(X2,X2,X2)
| ~ p0(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_171) ).
cnf(rule_033,axiom,
( m1(X1,X1,X1)
| ~ q0(X2,X2)
| ~ m1(X3,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_033) ).
cnf(rule_118,axiom,
( q1(X1,X1,X1)
| ~ p0(b,d)
| ~ s0(b)
| ~ n1(X2,d,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_118) ).
cnf(rule_241,axiom,
( p3(X1,X2,X3)
| ~ q2(X4,d,X1)
| ~ k2(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_241) ).
cnf(rule_163,axiom,
( p2(X1,X1,X1)
| ~ q1(X2,c,X2)
| ~ k2(X1,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_163) ).
cnf(rule_084,axiom,
( p1(X1,X1,X1)
| ~ m0(b,X2,b)
| ~ l1(X1,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_084) ).
cnf(rule_247,axiom,
( p3(X1,X1,X1)
| ~ n2(X1)
| ~ q2(X2,X3,X1)
| ~ s1(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_247) ).
cnf(rule_228,axiom,
( m3(X1,X2,X2)
| ~ n2(X1)
| ~ m2(X2)
| ~ m3(X3,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_228) ).
cnf(rule_201,axiom,
( k3(X1,X1,X2)
| ~ p1(X2,X3,X1)
| ~ m2(X4)
| ~ m2(X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_201) ).
cnf(rule_099,axiom,
( q1(X1,X2,X2)
| ~ k0(X3)
| ~ l0(X1)
| ~ q1(X2,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_099) ).
cnf(rule_028,axiom,
( m1(X1,X1,X1)
| ~ l0(X1)
| ~ k0(X1)
| ~ m0(X1,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_028) ).
cnf(rule_166,axiom,
( p2(a,X1,d)
| ~ n0(X1,d)
| ~ m1(a,X1,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_166) ).
cnf(rule_071,axiom,
( p1(X1,X2,X1)
| ~ l0(X3)
| ~ p1(X2,X4,X1)
| ~ s0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_071) ).
cnf(rule_230,axiom,
( m3(c,b,d)
| ~ l1(d,b)
| ~ m2(d)
| ~ q2(b,c,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_230) ).
cnf(rule_203,axiom,
( k3(d,d,d)
| ~ p1(a,d,b)
| ~ r2(a)
| ~ l2(e,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_203) ).
cnf(rule_180,axiom,
( q2(d,a,a)
| ~ q2(d,c,a)
| ~ s1(c)
| ~ q0(e,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_180) ).
cnf(rule_055,axiom,
( n1(d,e,e)
| ~ p0(d,d)
| ~ n1(e,e,e)
| ~ r0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_055) ).
cnf(rule_060,axiom,
( n1(d,d,b)
| ~ q0(b,e)
| ~ m1(d,e,e)
| ~ k0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_060) ).
cnf(rule_193,axiom,
( k3(X1,X1,X1)
| ~ s1(X1)
| ~ q2(d,X2,d)
| ~ s2(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_193) ).
cnf(rule_285,axiom,
( p4(X1,X1,X2)
| ~ r0(X1)
| ~ r3(X2,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_285) ).
cnf(rule_248,axiom,
( p3(X1,X1,X1)
| ~ p2(X2,X1,X1)
| ~ n3(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_248) ).
cnf(rule_250,axiom,
( p3(X1,X1,X1)
| ~ k1(X1)
| ~ q2(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_250) ).
cnf(rule_242,axiom,
( p3(X1,X2,X3)
| ~ r2(X2)
| ~ k3(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_242) ).
cnf(rule_235,axiom,
( m3(X1,X1,X2)
| ~ r2(X2)
| ~ k3(X1,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_235) ).
cnf(rule_213,axiom,
( k3(X1,X1,X1)
| ~ r1(X1)
| ~ p2(X2,X3,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_213) ).
cnf(rule_179,axiom,
( q2(X1,X1,X1)
| ~ k1(X2)
| ~ n1(X1,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_179) ).
cnf(rule_177,axiom,
( q2(X1,X2,X2)
| ~ k0(X2)
| ~ p1(X1,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_177) ).
cnf(rule_114,axiom,
( q1(X1,X1,X1)
| ~ m0(X1,X1,X2)
| ~ k0(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_114) ).
cnf(rule_098,axiom,
( q1(X1,X1,X1)
| ~ s0(X1)
| ~ m0(X2,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_098) ).
cnf(rule_113,axiom,
( q1(X1,X1,X2)
| ~ r0(X3)
| ~ m1(X1,X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_113) ).
cnf(rule_086,axiom,
( p1(X1,X1,X1)
| ~ l0(X1)
| ~ m0(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_086) ).
cnf(rule_046,axiom,
( n1(X1,X1,X1)
| ~ m1(X2,X3,X1)
| ~ k0(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_046) ).
cnf(rule_015,axiom,
( m1(X1,X2,X2)
| ~ l0(X3)
| ~ m0(X2,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_015) ).
cnf(rule_143,axiom,
( p2(c,e,e)
| ~ l1(c,b)
| ~ q1(e,e,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_143) ).
cnf(rule_078,axiom,
( p1(d,d,b)
| ~ p0(d,b)
| ~ m0(e,a,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_078) ).
cnf(rule_031,axiom,
( m1(c,a,c)
| ~ r0(e)
| ~ m0(a,e,c)
| ~ r0(X1)
| ~ k0(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_031) ).
cnf(rule_155,axiom,
( p2(X1,X2,X2)
| ~ k1(X3)
| ~ p2(e,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_155) ).
cnf(rule_123,axiom,
( q1(X1,X1,X1)
| ~ m0(c,X1,X1)
| ~ r0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_123) ).
cnf(rule_064,axiom,
( p1(X1,X1,X1)
| ~ m0(X2,X3,b)
| ~ l0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_064) ).
cnf(rule_083,axiom,
( p1(X1,b,X2)
| ~ m1(X1,X2,b)
| ~ k0(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_083) ).
cnf(rule_040,axiom,
( n1(X1,e,e)
| ~ m0(X1,X2,e)
| ~ k1(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_040) ).
cnf(rule_145,axiom,
( p2(e,X1,X2)
| ~ r0(e)
| ~ p1(X1,X2,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_145) ).
cnf(rule_149,axiom,
( p2(X1,X1,d)
| ~ r1(a)
| ~ m0(X2,X1,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_149) ).
cnf(rule_321,axiom,
( p5(b,b,b)
| ~ p4(X1,X1,X2)
| ~ k5(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_321) ).
cnf(rule_291,axiom,
( p4(X1,X1,X1)
| ~ p3(X2,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_291) ).
cnf(rule_287,axiom,
( p4(X1,X2,X1)
| ~ k3(X1,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_287) ).
cnf(rule_267,axiom,
( r3(X1,X2,X1)
| ~ p2(X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_267) ).
cnf(rule_238,axiom,
( m3(X1,X1,X1)
| ~ p2(X1,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_238) ).
cnf(rule_205,axiom,
( k3(X1,X1,X1)
| ~ p2(X2,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_205) ).
cnf(rule_206,axiom,
( k3(X1,X2,X1)
| ~ p2(X2,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_206) ).
cnf(rule_181,axiom,
( q2(X1,X1,X1)
| ~ p1(X1,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_181) ).
cnf(rule_154,axiom,
( p2(X1,X1,X1)
| ~ q1(X1,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_154) ).
cnf(rule_150,axiom,
( p2(X1,X1,X1)
| ~ m1(X2,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_150) ).
cnf(rule_176,axiom,
( p2(X1,X2,X1)
| ~ m1(X2,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_176) ).
cnf(rule_122,axiom,
( q1(X1,X1,X1)
| ~ m0(X1,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_122) ).
cnf(rule_121,axiom,
( q1(X1,X1,X1)
| ~ m0(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_121) ).
cnf(rule_110,axiom,
( q1(X1,X1,X1)
| ~ m0(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_110) ).
cnf(rule_006,axiom,
( m1(X1,X1,X1)
| ~ m0(X2,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_006) ).
cnf(rule_025,axiom,
( m1(X1,X1,X1)
| ~ m0(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_025) ).
cnf(rule_014,axiom,
( m1(X1,X1,X1)
| ~ m0(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_014) ).
cnf(rule_005,axiom,
( m1(X1,X2,X1)
| ~ m0(X2,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_005) ).
cnf(rule_237,axiom,
( m3(X1,c,X1)
| ~ s2(c)
| ~ q2(X1,c,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_237) ).
cnf(rule_036,axiom,
( n1(X1,X1,X2)
| ~ m0(b,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_036) ).
cnf(rule_184,axiom,
( q2(X1,X1,X1)
| ~ q1(X2,c,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_184) ).
cnf(rule_041,axiom,
( n1(e,e,X1)
| ~ s0(b)
| ~ m1(b,X1,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_041) ).
cnf(rule_294,axiom,
( p4(c,c,X1)
| ~ n3(a)
| ~ m3(X1,c,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_294) ).
cnf(rule_234,axiom,
( m3(X1,e,e)
| ~ n2(e)
| ~ p2(X1,e,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_234) ).
cnf(rule_141,axiom,
( p2(X1,a,X1)
| ~ q1(X1,a,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_141) ).
cnf(rule_039,axiom,
( n1(X1,c,X1)
| ~ m0(X2,X1,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_039) ).
cnf(rule_153,axiom,
( p2(X1,X1,X1)
| ~ n1(d,d,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_153) ).
cnf(rule_103,axiom,
( q1(X1,X1,X1)
| ~ m0(X1,c,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_103) ).
cnf(rule_170,axiom,
( p2(X1,e,X1)
| ~ n1(X1,e,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_170) ).
cnf(rule_087,axiom,
( p1(a,b,a)
| ~ r0(b)
| ~ p1(a,a,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_087) ).
cnf(rule_259,axiom,
( q3(X1,X1)
| ~ m0(X2,d,X2)
| ~ k1(X1)
| ~ r2(d)
| ~ q3(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_259) ).
cnf(rule_257,axiom,
( q3(X1,X2)
| ~ n1(X3,X1,X2)
| ~ s2(X1)
| ~ q3(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_257) ).
cnf(rule_133,axiom,
( l2(X1,X1)
| ~ p0(X2,X2)
| ~ s1(X3)
| ~ m0(X4,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_133) ).
cnf(rule_127,axiom,
( k2(X1,X2)
| ~ m1(X3,X2,X1)
| ~ k1(X4)
| ~ k2(X4,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_127) ).
cnf(rule_003,axiom,
( l1(X1,X2)
| ~ p0(X3,X1)
| ~ r0(X4)
| ~ m0(X2,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_003) ).
cnf(rule_229,axiom,
( m3(b,b,b)
| ~ q2(a,b,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_229) ).
cnf(rule_172,axiom,
( p2(a,a,a)
| ~ p1(e,e,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_172) ).
cnf(rule_161,axiom,
( p2(d,b,b)
| ~ p1(d,b,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_161) ).
cnf(rule_077,axiom,
( p1(c,e,b)
| ~ m0(b,c,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_077) ).
cnf(rule_308,axiom,
( n5(X1,X1)
| ~ m0(X2,X1,X2)
| ~ n5(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_308) ).
cnf(rule_281,axiom,
( n4(X1,X2)
| ~ p3(X1,X2,X2)
| ~ n4(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_281) ).
cnf(rule_256,axiom,
( q3(X1,X1)
| ~ p2(X2,X1,X1)
| ~ q3(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_256) ).
cnf(rule_255,axiom,
( q3(X1,X2)
| ~ q2(X3,X1,X2)
| ~ n0(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_255) ).
cnf(rule_222,axiom,
( l3(X1,X1)
| ~ k3(X2,X1,X1)
| ~ l2(X3,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_222) ).
cnf(rule_293,axiom,
( p4(X1,X1,X1)
| ~ q3(X2,X3)
| ~ n4(X3,X1)
| ~ l3(X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_293) ).
cnf(rule_065,axiom,
( p1(X1,X1,X1)
| ~ l1(X2,X2)
| ~ p0(X1,X2)
| ~ n0(X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_065) ).
cnf(rule_010,axiom,
( m1(X1,X1,c)
| ~ n0(X2,X2)
| ~ l1(c,c)
| ~ p0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_010) ).
cnf(rule_104,axiom,
( q1(X1,X2,X1)
| ~ l0(X1)
| ~ r0(X3)
| ~ p0(X4,X1)
| ~ q0(X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_104) ).
cnf(rule_317,axiom,
( n5(d,X1)
| ~ k3(d,X1,a)
| ~ n4(X1,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_317) ).
cnf(rule_124,axiom,
( r1(X1)
| ~ q0(X1,X2)
| ~ s0(d)
| ~ q1(d,X2,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_124) ).
cnf(rule_299,axiom,
( s4(X1)
| ~ p3(X2,X3,X4)
| ~ l1(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_299) ).
cnf(rule_142,axiom,
( p2(X1,X1,X1)
| ~ k1(X2)
| ~ k0(X2)
| ~ l2(a,X2)
| ~ k2(X1,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_142) ).
cnf(rule_312,axiom,
( n5(b,e)
| ~ r3(d,b,c)
| ~ n4(b,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_312) ).
cnf(rule_297,axiom,
( q4(b,b)
| ~ k3(c,e,b)
| ~ l1(b,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_297) ).
cnf(rule_283,axiom,
( n4(e,e)
| ~ l3(b,a)
| ~ p3(b,e,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_283) ).
cnf(rule_303,axiom,
( m5(X1,X2)
| ~ r0(X1)
| ~ p4(X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_303) ).
cnf(rule_284,axiom,
( n4(X1,X1)
| ~ k4(X2)
| ~ m3(X1,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_284) ).
cnf(rule_215,axiom,
( l3(X1,X2)
| ~ r0(X1)
| ~ p2(X1,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_215) ).
cnf(rule_109,axiom,
( q1(X1,X1,X2)
| ~ p0(X3,X3)
| ~ q0(X2,X1)
| ~ k1(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_109) ).
cnf(rule_019,axiom,
( m1(X1,X2,c)
| ~ r0(c)
| ~ s0(d)
| ~ q0(X2,d)
| ~ p0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_019) ).
cnf(rule_047,axiom,
( n1(X1,d,X2)
| ~ p0(X2,X2)
| ~ r0(X1)
| ~ l1(X2,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_047) ).
cnf(rule_129,axiom,
( k2(X1,X1)
| ~ q1(X2,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_129) ).
cnf(rule_252,axiom,
( p3(X1,X1,X1)
| ~ q0(X2,X1)
| ~ k2(X3,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_252) ).
cnf(rule_092,axiom,
( q1(X1,X2,X1)
| ~ n0(X3,X2)
| ~ p0(X4,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_092) ).
cnf(rule_058,axiom,
( n1(X1,X1,X1)
| ~ l1(X2,X1)
| ~ n0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_058) ).
cnf(rule_044,axiom,
( n1(X1,X2,X1)
| ~ p0(X1,X1)
| ~ p0(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_044) ).
cnf(rule_018,axiom,
( m1(X1,X1,X1)
| ~ q0(X2,X3)
| ~ q0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_018) ).
cnf(rule_224,axiom,
( l3(d,c)
| ~ s2(d)
| ~ k3(a,c,a)
| ~ r0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_224) ).
cnf(rule_227,axiom,
( m3(X1,X1,X1)
| ~ q0(X2,X3)
| ~ s0(X4)
| ~ s2(X3)
| ~ r2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_227) ).
cnf(rule_038,axiom,
( n1(X1,X1,X1)
| ~ n0(X1,X1)
| ~ q0(a,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_038) ).
cnf(rule_300,axiom,
( k5(X1)
| ~ s4(X2)
| ~ r3(X3,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_300) ).
cnf(rule_278,axiom,
( l4(X1)
| ~ m0(X2,X1,X1)
| ~ l4(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_278) ).
cnf(rule_140,axiom,
( n2(e)
| ~ r1(b)
| ~ r0(e)
| ~ p1(b,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_140) ).
cnf(rule_073,axiom,
( p1(X1,X1,X1)
| ~ n0(e,b)
| ~ k0(b)
| ~ k0(X1)
| ~ k1(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_073) ).
cnf(rule_037,axiom,
( n1(X1,X2,X1)
| ~ p0(X3,X1)
| ~ l0(X2)
| ~ r0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_037) ).
cnf(rule_009,axiom,
( m1(X1,X1,X1)
| ~ s0(X2)
| ~ r0(X2)
| ~ q0(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_009) ).
cnf(rule_189,axiom,
( s2(X1)
| ~ q2(b,X1,b)
| ~ s1(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_189) ).
cnf(rule_277,axiom,
( l4(X1)
| ~ p3(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_277) ).
cnf(rule_240,axiom,
( n3(X1)
| ~ p2(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_240) ).
cnf(rule_137,axiom,
( n2(X1)
| ~ p1(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_137) ).
cnf(rule_311,axiom,
( n5(d,d)
| ~ p4(c,d,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_311) ).
cnf(rule_053,axiom,
( n1(a,X1,b)
| ~ p0(X1,d)
| ~ p0(a,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_053) ).
cnf(rule_034,axiom,
( m1(X1,X2,X2)
| ~ k1(a)
| ~ k1(X2)
| ~ q0(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_034) ).
cnf(rule_026,axiom,
( m1(X1,X1,X1)
| ~ l0(X1)
| ~ l0(X2)
| ~ p0(X2,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_026) ).
cnf(rule_183,axiom,
( q2(X1,c,X2)
| ~ k1(X2)
| ~ l0(c)
| ~ l2(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_183) ).
cnf(rule_050,axiom,
( n1(X1,X2,X1)
| ~ s0(b)
| ~ l0(X1)
| ~ p0(b,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_050) ).
cnf(rule_301,axiom,
( k5(b)
| ~ s4(e)
| ~ n1(b,b,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_301) ).
cnf(rule_027,axiom,
( m1(b,b,b)
| ~ q0(c,d)
| ~ l1(a,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_027) ).
cnf(rule_318,axiom,
( p5(X1,X1,X2)
| ~ s4(X2)
| ~ l2(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_318) ).
cnf(rule_320,axiom,
( p5(X1,X2,X1)
| ~ q4(X2,X3)
| ~ s1(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_320) ).
cnf(rule_286,axiom,
( p4(X1,X1,X1)
| ~ q3(X2,X3)
| ~ n3(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_286) ).
cnf(rule_232,axiom,
( m3(X1,X1,X1)
| ~ l2(X1,X1)
| ~ n2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_232) ).
cnf(rule_074,axiom,
( p1(X1,X1,X2)
| ~ p0(X2,X1)
| ~ r0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_074) ).
cnf(rule_043,axiom,
( n1(X1,X1,X1)
| ~ k1(X1)
| ~ p0(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_043) ).
cnf(rule_011,axiom,
( m1(X1,X1,X2)
| ~ k0(X1)
| ~ n0(X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_011) ).
cnf(rule_007,axiom,
( m1(X1,X2,X1)
| ~ p0(X3,X2)
| ~ r0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_007) ).
cnf(rule_029,axiom,
( m1(X1,X2,X1)
| ~ p0(X1,X2)
| ~ s0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_029) ).
cnf(prove_this,negated_conjecture,
~ m1(X1,X1,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
cnf(rule_260,axiom,
( r3(X1,X2,X2)
| ~ s2(X2)
| ~ l2(c,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_260) ).
cnf(rule_231,axiom,
( m3(X1,X2,X1)
| ~ r2(X1)
| ~ k2(c,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_231) ).
cnf(rule_063,axiom,
( p1(X1,X1,X2)
| ~ n0(d,X1)
| ~ k0(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_063) ).
cnf(rule_197,axiom,
( k3(X1,X1,X1)
| ~ l2(X2,b)
| ~ k1(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_197) ).
cnf(rule_105,axiom,
( q1(X1,X1,X2)
| ~ s0(X1)
| ~ p0(X2,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_105) ).
cnf(rule_017,axiom,
( m1(X1,X1,X1)
| ~ s0(X1)
| ~ q0(X2,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_017) ).
cnf(rule_208,axiom,
( k3(X1,X1,X1)
| ~ r2(c)
| ~ l1(b,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_208) ).
cnf(rule_265,axiom,
( r3(X1,X1,X1)
| ~ l2(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_265) ).
cnf(rule_246,axiom,
( p3(X1,X1,X1)
| ~ l2(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_246) ).
cnf(rule_194,axiom,
( k3(X1,X1,X2)
| ~ k2(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_194) ).
cnf(rule_186,axiom,
( q2(X1,X1,X2)
| ~ l1(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_186) ).
cnf(rule_175,axiom,
( p2(X1,X1,X1)
| ~ l1(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_175) ).
cnf(rule_100,axiom,
( q1(X1,X1,X1)
| ~ n0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_100) ).
cnf(rule_093,axiom,
( q1(X1,X1,X1)
| ~ q0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_093) ).
cnf(rule_095,axiom,
( q1(X1,X2,X2)
| ~ p0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_095) ).
cnf(rule_085,axiom,
( p1(X1,X1,X1)
| ~ p0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_085) ).
cnf(rule_066,axiom,
( p1(X1,X1,X1)
| ~ n0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_066) ).
cnf(rule_067,axiom,
( p1(X1,X1,X1)
| ~ q0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_067) ).
cnf(rule_069,axiom,
( p1(X1,X1,X2)
| ~ p0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_069) ).
cnf(rule_013,axiom,
( m1(X1,X1,X1)
| ~ q0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_013) ).
cnf(rule_157,axiom,
( p2(X1,X1,X1)
| ~ l1(X1,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_157) ).
cnf(rule_195,axiom,
( k3(c,c,c)
| ~ s2(e)
| ~ k2(c,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_195) ).
cnf(rule_147,axiom,
( p2(e,c,c)
| ~ r1(d)
| ~ l1(e,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_147) ).
cnf(rule_211,axiom,
( k3(X1,X1,X1)
| ~ l0(X1)
| ~ r2(e)
| ~ r0(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_211) ).
cnf(rule_079,axiom,
( p1(X1,X1,X1)
| ~ k0(e)
| ~ k1(X1)
| ~ l0(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_079) ).
cnf(rule_249,axiom,
( p3(X1,X1,X1)
| ~ k1(X1)
| ~ n2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_249) ).
cnf(rule_233,axiom,
( m3(X1,X1,X1)
| ~ n2(X1)
| ~ m2(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_233) ).
cnf(rule_167,axiom,
( p2(X1,X1,X1)
| ~ s1(X1)
| ~ k1(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_167) ).
cnf(rule_173,axiom,
( p2(X1,X1,X1)
| ~ r1(X2)
| ~ r0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_173) ).
cnf(rule_102,axiom,
( q1(X1,X1,X1)
| ~ k0(X1)
| ~ l0(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_102) ).
cnf(rule_072,axiom,
( p1(X1,X1,X1)
| ~ s0(X2)
| ~ s0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_072) ).
cnf(rule_061,axiom,
( n1(X1,X1,X1)
| ~ k0(X1)
| ~ s0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_061) ).
cnf(rule_021,axiom,
( m1(X1,X2,X1)
| ~ l0(X1)
| ~ k0(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_021) ).
cnf(rule_035,axiom,
( m1(X1,X2,X1)
| ~ r0(X1)
| ~ l0(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_035) ).
cnf(rule_253,axiom,
( p3(b,c,b)
| ~ k2(c,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_253) ).
cnf(rule_239,axiom,
( m3(b,b,b)
| ~ l2(a,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_239) ).
cnf(rule_070,axiom,
( p1(c,c,c)
| ~ p0(a,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_070) ).
cnf(rule_075,axiom,
( p1(a,a,a)
| ~ p0(b,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_075) ).
cnf(rule_045,axiom,
( n1(d,d,d)
| ~ q0(d,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_045) ).
cnf(rule_219,axiom,
( l3(X1,X1)
| ~ n2(X2)
| ~ l1(X3,X1)
| ~ l3(X3,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_219) ).
cnf(rule_174,axiom,
( p2(X1,X1,X1)
| ~ n2(X1)
| ~ k1(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_174) ).
cnf(rule_112,axiom,
( q1(X1,X1,X1)
| ~ k1(X1)
| ~ s0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_112) ).
cnf(rule_310,axiom,
( n5(X1,X1)
| ~ p0(X1,X2)
| ~ m4(X3,X3)
| ~ k5(d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_310) ).
cnf(rule_131,axiom,
( l2(X1,X2)
| ~ s1(X1)
| ~ n0(e,X2)
| ~ l2(X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_131) ).
cnf(rule_094,axiom,
( q1(b,e,e)
| ~ s0(e)
| ~ k0(b)
| ~ l0(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_094) ).
cnf(rule_119,axiom,
( q1(X1,b,b)
| ~ s0(X1)
| ~ s0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_119) ).
cnf(rule_264,axiom,
( r3(X1,X1,X1)
| ~ s2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_264) ).
cnf(rule_266,axiom,
( r3(X1,X1,X1)
| ~ r2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_266) ).
cnf(rule_244,axiom,
( p3(X1,X1,X1)
| ~ n2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_244) ).
cnf(rule_236,axiom,
( m3(X1,X1,X1)
| ~ n2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_236) ).
cnf(rule_210,axiom,
( k3(X1,X1,X1)
| ~ n2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_210) ).
cnf(rule_212,axiom,
( k3(X1,X1,X1)
| ~ m2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_212) ).
cnf(rule_159,axiom,
( p2(X1,X1,X1)
| ~ k1(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_159) ).
cnf(rule_116,axiom,
( q1(X1,X1,X1)
| ~ r0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_116) ).
cnf(rule_106,axiom,
( q1(X1,X1,X1)
| ~ s0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_106) ).
cnf(rule_097,axiom,
( q1(X1,X1,X1)
| ~ s0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_097) ).
cnf(rule_068,axiom,
( p1(X1,X1,X1)
| ~ k0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_068) ).
cnf(rule_057,axiom,
( n1(X1,X1,X1)
| ~ r0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_057) ).
cnf(rule_032,axiom,
( m1(X1,X1,X1)
| ~ s0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_032) ).
cnf(rule_198,axiom,
( k3(c,c,c)
| ~ k0(a)
| ~ r2(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_198) ).
cnf(rule_151,axiom,
( p2(d,d,d)
| ~ k1(d)
| ~ s0(d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_151) ).
cnf(rule_117,axiom,
( q1(d,d,d)
| ~ k0(e)
| ~ s0(d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_117) ).
cnf(rule_090,axiom,
( p1(e,e,e)
| ~ r0(e)
| ~ k0(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_090) ).
cnf(rule_056,axiom,
( n1(a,a,a)
| ~ l0(a)
| ~ r0(a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_056) ).
cnf(rule_023,axiom,
( m1(a,a,a)
| ~ l0(a)
| ~ s0(d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_023) ).
cnf(rule_279,axiom,
( m4(X1,X2)
| ~ l2(X3,X2)
| ~ s3(a,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_279) ).
cnf(rule_298,axiom,
( r4(X1)
| ~ n3(X1)
| ~ q3(X2,X3)
| ~ p0(X4,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_298) ).
cnf(rule_214,axiom,
( k3(c,c,c)
| ~ r2(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_214) ).
cnf(rule_204,axiom,
( k3(a,a,a)
| ~ r2(a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_204) ).
cnf(rule_115,axiom,
( q1(b,b,b)
| ~ l0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_115) ).
cnf(rule_120,axiom,
( q1(b,b,b)
| ~ r0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_120) ).
cnf(rule_088,axiom,
( p1(a,a,a)
| ~ l0(a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_088) ).
cnf(rule_049,axiom,
( n1(c,c,c)
| ~ l0(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_049) ).
cnf(rule_020,axiom,
( m1(c,c,c)
| ~ l0(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_020) ).
cnf(rule_008,axiom,
( m1(b,b,b)
| ~ l0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_008) ).
cnf(rule_030,axiom,
( m1(e,e,e)
| ~ r0(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_030) ).
cnf(rule_012,axiom,
( m1(e,e,e)
| ~ r0(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_012) ).
cnf(rule_022,axiom,
( m1(e,e,e)
| ~ s0(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_022) ).
cnf(axiom_19,axiom,
m0(X1,d,X2),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_19) ).
cnf(axiom_12,axiom,
m0(a,X1,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_12) ).
cnf(rule_296,axiom,
( q4(X1,X1)
| ~ r1(X1)
| ~ l4(X2)
| ~ q4(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_296) ).
cnf(rule_258,axiom,
( q3(X1,X1)
| ~ r2(X1)
| ~ s1(X2)
| ~ l2(X3,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_258) ).
cnf(rule_004,axiom,
( l1(X1,X1)
| ~ k1(X1)
| ~ l0(X2)
| ~ l1(X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_004) ).
cnf(axiom_16,axiom,
m0(c,b,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_16) ).
cnf(axiom_31,axiom,
m0(b,b,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_31) ).
cnf(axiom_38,axiom,
m0(b,a,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_38) ).
cnf(axiom_23,axiom,
m0(a,e,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_23) ).
cnf(axiom_27,axiom,
m0(e,b,c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_27) ).
cnf(axiom_4,axiom,
m0(e,d,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_4) ).
cnf(axiom_8,axiom,
m0(e,d,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_8) ).
cnf(axiom_35,axiom,
m0(d,e,c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_35) ).
cnf(rule_330,axiom,
( s5(X1)
| ~ k4(X1)
| ~ s3(X1,X2)
| ~ l5(X3)
| ~ s5(X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_330) ).
cnf(rule_220,axiom,
( l3(X1,X1)
| ~ s2(X2)
| ~ l1(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_220) ).
cnf(rule_274,axiom,
( k4(c)
| ~ n0(c,d)
| ~ q3(e,b)
| ~ n3(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_274) ).
cnf(rule_305,axiom,
( m5(X1,X1)
| ~ s4(X1)
| ~ m4(e,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_305) ).
cnf(rule_325,axiom,
( q5(X1,X1)
| ~ q4(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_325) ).
cnf(rule_326,axiom,
( q5(X1,X1)
| ~ m4(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_326) ).
cnf(rule_313,axiom,
( n5(X1,X1)
| ~ q4(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_313) ).
cnf(rule_309,axiom,
( n5(X1,X1)
| ~ n4(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_309) ).
cnf(rule_002,axiom,
( l1(X1,X1)
| ~ n0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_002) ).
cnf(rule_302,axiom,
( l5(X1)
| ~ q4(X2,X2)
| ~ k1(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_302) ).
cnf(rule_135,axiom,
( m2(X1)
| ~ s0(X1)
| ~ l1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_135) ).
cnf(rule_126,axiom,
( s1(X1)
| ~ q0(X1,X2)
| ~ s1(X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_126) ).
cnf(rule_327,axiom,
( r5(X1,X2)
| ~ s4(X1)
| ~ k0(b)
| ~ n3(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_327) ).
cnf(rule_223,axiom,
( l3(c,c)
| ~ k2(b,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_223) ).
cnf(rule_221,axiom,
( l3(d,d)
| ~ k2(a,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_221) ).
cnf(rule_130,axiom,
( k2(e,e)
| ~ l1(e,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_130) ).
cnf(rule_322,axiom,
( q5(X1,X2)
| ~ s4(X1)
| ~ m2(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_322) ).
cnf(rule_315,axiom,
( n5(X1,X1)
| ~ s1(X1)
| ~ k4(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_315) ).
cnf(rule_306,axiom,
( m5(X1,X1)
| ~ s4(X2)
| ~ r0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_306) ).
cnf(rule_125,axiom,
( s1(X1)
| ~ p0(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_125) ).
cnf(rule_001,axiom,
( k1(X1)
| ~ n0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_001) ).
cnf(rule_217,axiom,
( l3(X1,X1)
| ~ n2(X1)
| ~ m2(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_217) ).
cnf(rule_139,axiom,
( n2(c)
| ~ l1(e,c)
| ~ k0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_139) ).
cnf(rule_328,axiom,
( r5(X1,X1)
| ~ k4(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_328) ).
cnf(rule_324,axiom,
( q5(X1,X1)
| ~ l4(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_324) ).
cnf(rule_314,axiom,
( n5(X1,X1)
| ~ r4(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_314) ).
cnf(rule_304,axiom,
( m5(X1,X1)
| ~ k4(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_304) ).
cnf(rule_218,axiom,
( l3(X1,X1)
| ~ r2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_218) ).
cnf(rule_329,axiom,
( s5(X1)
| ~ l4(X1)
| ~ r4(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_329) ).
cnf(rule_188,axiom,
( r2(X1)
| ~ r1(X1)
| ~ l0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_188) ).
cnf(rule_323,axiom,
( q5(a,a)
| ~ r4(a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_323) ).
cnf(axiom_14,axiom,
p0(b,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_14) ).
cnf(axiom_17,axiom,
q0(X1,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_17) ).
cnf(rule_191,axiom,
( s2(d)
| ~ r1(d)
| ~ s1(d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_191) ).
cnf(rule_190,axiom,
( s2(d)
| ~ s1(a)
| ~ s0(d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_190) ).
cnf(axiom_18,axiom,
p0(c,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_18) ).
cnf(axiom_22,axiom,
p0(b,c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_22) ).
cnf(axiom_10,axiom,
p0(b,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_10) ).
cnf(axiom_34,axiom,
n0(c,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_34) ).
cnf(axiom_37,axiom,
n0(b,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_37) ).
cnf(axiom_15,axiom,
n0(a,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_15) ).
cnf(axiom_11,axiom,
n0(e,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_11) ).
cnf(axiom_30,axiom,
n0(e,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_30) ).
cnf(axiom_26,axiom,
n0(d,c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_26) ).
cnf(axiom_7,axiom,
n0(d,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_7) ).
cnf(axiom_3,axiom,
n0(d,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_3) ).
cnf(axiom_6,axiom,
q0(b,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_6) ).
cnf(axiom_21,axiom,
q0(b,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_21) ).
cnf(axiom_36,axiom,
q0(a,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_36) ).
cnf(axiom_2,axiom,
q0(e,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_2) ).
cnf(axiom_33,axiom,
q0(d,c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_33) ).
cnf(axiom_29,axiom,
q0(d,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_29) ).
cnf(axiom_25,axiom,
q0(d,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_25) ).
cnf(rule_136,axiom,
( m2(b)
| ~ k1(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_136) ).
cnf(axiom_32,axiom,
k0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_32) ).
cnf(axiom_28,axiom,
k0(e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_28) ).
cnf(axiom_24,axiom,
l0(c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_24) ).
cnf(axiom_20,axiom,
l0(a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_20) ).
cnf(axiom_9,axiom,
r0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_9) ).
cnf(axiom_13,axiom,
r0(e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_13) ).
cnf(axiom_5,axiom,
s0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_5) ).
cnf(axiom_1,axiom,
s0(d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_1) ).
cnf(i_0_362,axiom,
( q1(X1,X1,X1)
| ~ n1(X2,X3,X3)
| ~ p0(X2,X4)
| ~ m1(X1,X3,X2)
| ~ q1(X4,X2,X3) ),
rule_096,
[final] ).
cnf(i_0_363,axiom,
( q2(X1,X2,X1)
| ~ p1(X1,X1,X3)
| ~ n1(X2,X1,X3)
| ~ q2(X2,X3,X1) ),
rule_182,
[final] ).
cnf(i_0_364,axiom,
( n1(X1,X1,X1)
| ~ m1(c,X1,X2)
| ~ m0(b,X2,c)
| ~ n1(X2,X1,X2) ),
rule_051,
[final] ).
cnf(i_0_365,axiom,
( p2(b,c,c)
| ~ p1(X1,b,b)
| ~ n1(e,e,X1)
| ~ q1(e,c,X1) ),
rule_162,
[final] ).
cnf(i_0_366,axiom,
( q4(X1,X2)
| ~ k3(X3,X3,X1)
| ~ q2(X4,X2,X1)
| ~ m3(X4,X5,X4) ),
rule_295,
[final] ).
cnf(i_0_367,axiom,
( k2(X1,X1)
| ~ n1(e,d,X1)
| ~ m1(X1,e,X1)
| ~ q1(X1,X1,d) ),
rule_128,
[final] ).
cnf(i_0_368,axiom,
( m3(X1,X2,X1)
| ~ m0(X3,X3,X2)
| ~ l2(X4,X1)
| ~ m0(X1,X4,X4)
| ~ s2(X3) ),
rule_225,
[final] ).
cnf(i_0_369,axiom,
( p4(X1,X1,X1)
| ~ k3(X2,X3,X3)
| ~ n4(X1,X3)
| ~ p1(X3,X2,X1) ),
rule_292,
[final] ).
cnf(i_0_370,axiom,
( r3(X1,X1,X1)
| ~ p1(X2,X3,X1)
| ~ l2(X3,X2)
| ~ r3(X1,X2,X1) ),
rule_262,
[final] ).
cnf(i_0_371,axiom,
( p2(X1,X2,X2)
| ~ p1(X1,X3,X4)
| ~ l1(X3,X4)
| ~ p2(X1,X2,X1) ),
rule_146,
[final] ).
cnf(i_0_372,axiom,
( p2(X1,X2,X2)
| ~ n1(X3,X2,X3)
| ~ p0(X1,X2)
| ~ p2(X1,X2,X1) ),
rule_152,
[final] ).
cnf(i_0_373,axiom,
( n2(a)
| ~ m1(b,a,e)
| ~ k1(c)
| ~ n1(e,a,e)
| ~ q1(c,a,d) ),
rule_138,
[final] ).
cnf(i_0_374,axiom,
( q2(X1,X2,X1)
| ~ r1(X2)
| ~ m0(X3,X4,X1)
| ~ k0(X2)
| ~ q2(X2,X2,X2) ),
rule_187,
[final] ).
cnf(i_0_375,axiom,
( m1(X1,a,X2)
| ~ m0(a,X3,a)
| ~ q0(X1,X2)
| ~ m1(X2,c,X2) ),
rule_024,
[final] ).
cnf(i_0_376,axiom,
( r3(a,a,e)
| ~ k2(a,a)
| ~ q2(X1,e,X1)
| ~ m2(b)
| ~ m3(a,X1,X1) ),
rule_269,
[final] ).
cnf(i_0_377,axiom,
( p3(X1,d,e)
| ~ l3(b,e)
| ~ p2(d,b,c)
| ~ n3(X1)
| ~ q2(X1,d,X1) ),
rule_243,
[final] ).
cnf(i_0_378,axiom,
( p2(X1,X1,X2)
| ~ q1(c,X1,X3)
| ~ s1(c)
| ~ s0(e)
| ~ p2(X1,X3,X1) ),
rule_158,
[final] ).
cnf(i_0_379,axiom,
( r3(X1,X1,X2)
| ~ m2(X2)
| ~ m3(X3,b,X1)
| ~ r3(X2,X4,X4) ),
rule_268,
[final] ).
cnf(i_0_380,axiom,
( q2(X1,X1,X1)
| ~ n1(X2,d,X3)
| ~ k1(X1)
| ~ q2(X3,X3,X2) ),
rule_185,
[final] ).
cnf(i_0_381,axiom,
( k3(X1,X1,X1)
| ~ p2(X2,X3,e)
| ~ s1(X2)
| ~ k3(X1,X2,X2) ),
rule_200,
[final] ).
cnf(i_0_382,axiom,
( p4(X1,X1,X1)
| ~ m3(X2,X3,X1)
| ~ p4(X1,X3,X1) ),
rule_290,
[final] ).
cnf(i_0_383,axiom,
( p4(X1,X2,X2)
| ~ r3(X2,X2,X1)
| ~ p4(X3,X3,X4) ),
rule_288,
[final] ).
cnf(i_0_384,axiom,
( r3(X1,X1,X1)
| ~ p3(X2,X1,X3)
| ~ r3(X2,X2,X2) ),
rule_271,
[final] ).
cnf(i_0_385,axiom,
( p3(X1,X2,X2)
| ~ m3(X2,X3,X4)
| ~ p2(X1,X2,X4) ),
rule_251,
[final] ).
cnf(i_0_386,axiom,
( k3(X1,X1,X1)
| ~ p2(X2,X3,X2)
| ~ m1(X1,X1,X3) ),
rule_196,
[final] ).
cnf(i_0_387,axiom,
( p2(X1,X1,X1)
| ~ q1(X2,X3,X2)
| ~ p2(X2,X2,X3) ),
rule_165,
[final] ).
cnf(i_0_388,axiom,
( p2(X1,X1,X1)
| ~ q1(X2,X2,X2)
| ~ p1(X1,X3,X1) ),
rule_169,
[final] ).
cnf(i_0_389,axiom,
( p2(X1,X1,X1)
| ~ m1(X2,X3,X1)
| ~ p2(X2,X1,X2) ),
rule_148,
[final] ).
cnf(i_0_390,axiom,
( p1(X1,X2,X3)
| ~ m0(X3,X1,X4)
| ~ p1(X3,X1,X4) ),
rule_082,
[final] ).
cnf(i_0_391,axiom,
( n1(X1,X1,X1)
| ~ m0(X2,X2,X3)
| ~ n1(X2,X1,X2) ),
rule_062,
[final] ).
cnf(i_0_392,axiom,
( n1(X1,X1,X2)
| ~ m0(X3,X4,X4)
| ~ m0(X2,X3,X1) ),
rule_059,
[final] ).
cnf(i_0_393,axiom,
( m1(X1,X2,X2)
| ~ m1(X3,X2,X1)
| ~ m1(X3,X4,X2) ),
rule_016,
[final] ).
cnf(i_0_394,axiom,
( r3(X1,X1,X1)
| ~ m0(d,X2,X1)
| ~ r3(X1,X1,X2) ),
rule_263,
[final] ).
cnf(i_0_395,axiom,
( p2(X1,X1,X1)
| ~ m1(a,a,X2)
| ~ p2(a,X3,X1) ),
rule_160,
[final] ).
cnf(i_0_396,axiom,
( q1(e,X1,X1)
| ~ m0(X1,d,X1)
| ~ m0(e,d,X1) ),
rule_107,
[final] ).
cnf(i_0_397,axiom,
( p2(X1,e,X2)
| ~ n1(e,X1,a)
| ~ q1(a,X2,X1) ),
rule_156,
[final] ).
cnf(i_0_398,axiom,
( p3(e,b,e)
| ~ m3(e,X1,e)
| ~ q2(X1,X1,b) ),
rule_254,
[final] ).
cnf(i_0_399,axiom,
( l2(X1,X1)
| ~ m0(X2,X1,X3)
| ~ m1(X3,X2,X2)
| ~ p0(X2,X1) ),
rule_134,
[final] ).
cnf(i_0_400,axiom,
( q1(d,d,c)
| ~ m0(c,b,a)
| ~ m1(c,d,a) ),
rule_111,
[final] ).
cnf(i_0_401,axiom,
( m3(X1,X1,X1)
| ~ k2(X2,X3)
| ~ m3(X1,X3,X1)
| ~ n0(X3,a)
| ~ l2(a,a) ),
rule_226,
[final] ).
cnf(i_0_402,axiom,
( s3(X1,X2)
| ~ q2(X3,X1,X3)
| ~ s2(X1)
| ~ m0(X3,X4,X2) ),
rule_273,
[final] ).
cnf(i_0_403,axiom,
( k4(e)
| ~ q3(X1,X1)
| ~ q1(a,a,X2)
| ~ r3(X1,e,X2) ),
rule_276,
[final] ).
cnf(i_0_404,axiom,
( n5(X1,X1)
| ~ p4(X2,X1,X1)
| ~ s1(X1)
| ~ p4(b,b,X3) ),
rule_316,
[final] ).
cnf(i_0_405,axiom,
( l3(X1,X1)
| ~ p1(X1,X1,X2)
| ~ p2(X2,X3,X1) ),
rule_216,
[final] ).
cnf(i_0_406,axiom,
( p5(X1,X2,X2)
| ~ l2(X1,X3)
| ~ p5(X1,X3,X1)
| ~ m4(X3,X2) ),
rule_319,
[final] ).
cnf(i_0_407,axiom,
( p3(X1,X1,X1)
| ~ l1(X2,X2)
| ~ l3(X2,X1)
| ~ p3(X3,X3,X2) ),
rule_245,
[final] ).
cnf(i_0_408,axiom,
( k3(X1,X1,X2)
| ~ q0(X3,X2)
| ~ k2(X1,X4)
| ~ k3(X2,X5,X4) ),
rule_202,
[final] ).
cnf(i_0_409,axiom,
( k3(X1,X1,X1)
| ~ m2(X2)
| ~ l1(X3,X4)
| ~ s2(X1)
| ~ k3(X3,X4,X3) ),
rule_209,
[final] ).
cnf(i_0_410,axiom,
( n1(X1,X1,X1)
| ~ m0(X2,X2,X2)
| ~ k1(X1)
| ~ s0(X1)
| ~ p0(X3,X2) ),
rule_052,
[final] ).
cnf(i_0_411,axiom,
( p2(b,c,a)
| ~ r0(e)
| ~ n1(c,X1,X1)
| ~ p0(b,X1)
| ~ k2(c,a) ),
rule_144,
[final] ).
cnf(i_0_412,axiom,
( q1(X1,X1,X1)
| ~ p0(X2,X3)
| ~ p1(X1,b,b)
| ~ q0(b,b) ),
rule_108,
[final] ).
cnf(i_0_413,axiom,
( p4(X1,X1,X1)
| ~ l4(X1)
| ~ n0(X1,X2)
| ~ p4(X3,X4,X3) ),
rule_289,
[final] ).
cnf(i_0_414,axiom,
( r3(X1,X1,X1)
| ~ l1(X2,X3)
| ~ n1(X3,X3,X3)
| ~ r2(X1) ),
rule_261,
[final] ).
cnf(i_0_415,axiom,
( r3(X1,X2,X3)
| ~ k2(X2,X3)
| ~ r2(X3)
| ~ r3(X3,X1,X1) ),
rule_272,
[final] ).
cnf(i_0_416,axiom,
( k3(X1,X2,X1)
| ~ s1(X2)
| ~ p2(X3,X2,X4)
| ~ n0(X1,X4) ),
rule_192,
[final] ).
cnf(i_0_417,axiom,
( p2(X1,X1,X1)
| ~ p0(X1,X1)
| ~ r1(X2)
| ~ p2(X3,X2,X1) ),
rule_164,
[final] ).
cnf(i_0_418,axiom,
( p1(X1,X1,X1)
| ~ q0(X2,X3)
| ~ k1(X4)
| ~ n1(X2,X1,X5) ),
rule_091,
[final] ).
cnf(i_0_419,axiom,
( p1(X1,X1,X1)
| ~ n0(X2,X2)
| ~ l0(X3)
| ~ n1(X2,X4,X1) ),
rule_080,
[final] ).
cnf(i_0_420,axiom,
( p1(X1,X1,X1)
| ~ m1(X2,X3,X1)
| ~ q0(X3,X4)
| ~ l0(X5) ),
rule_081,
[final] ).
cnf(i_0_421,axiom,
( n1(X1,X1,X1)
| ~ m0(X2,X3,X2)
| ~ k0(X1)
| ~ q0(X4,X3) ),
rule_042,
[final] ).
cnf(i_0_422,axiom,
( n1(X1,X2,X2)
| ~ l0(X3)
| ~ l1(X3,X1)
| ~ n1(X1,X2,X1) ),
rule_054,
[final] ).
cnf(i_0_423,axiom,
( p2(a,c,b)
| ~ l1(e,c)
| ~ l2(e,b)
| ~ r1(e)
| ~ m1(d,a,c) ),
rule_168,
[final] ).
cnf(i_0_424,axiom,
( n4(d,d)
| ~ k3(c,c,e)
| ~ q1(d,d,d) ),
rule_282,
[final] ).
cnf(i_0_425,axiom,
( n5(X1,X2)
| ~ q4(X3,X4)
| ~ n4(X1,X4)
| ~ p4(X5,X5,X2)
| ~ n5(X5,X2) ),
rule_307,
[final] ).
cnf(i_0_426,axiom,
( p1(d,d,X1)
| ~ s0(X1)
| ~ n1(c,d,X1)
| ~ r0(d)
| ~ n0(c,X1) ),
rule_089,
[final] ).
cnf(i_0_427,axiom,
( r3(X1,b,X1)
| ~ r0(X1)
| ~ p2(b,X1,b)
| ~ l2(X1,X1) ),
rule_270,
[final] ).
cnf(i_0_428,axiom,
( q1(X1,X1,X1)
| ~ k1(X1)
| ~ q0(X1,b)
| ~ p1(b,b,X1) ),
rule_101,
[final] ).
cnf(i_0_429,axiom,
( q2(X1,X1,X1)
| ~ q0(X2,X1)
| ~ n1(X2,X1,X3) ),
rule_178,
[final] ).
cnf(i_0_430,axiom,
( p2(X1,X1,X1)
| ~ n1(X2,X2,X2)
| ~ p0(X1,X1) ),
rule_171,
[final] ).
cnf(i_0_431,axiom,
( m1(X1,X1,X1)
| ~ q0(X2,X2)
| ~ m1(X3,X2,X1) ),
rule_033,
[final] ).
cnf(i_0_432,axiom,
( q1(X1,X1,X1)
| ~ p0(b,d)
| ~ s0(b)
| ~ n1(X2,d,X1) ),
rule_118,
[final] ).
cnf(i_0_433,axiom,
( p3(X1,X2,X3)
| ~ q2(X4,d,X1)
| ~ k2(X2,X3) ),
rule_241,
[final] ).
cnf(i_0_434,axiom,
( p2(X1,X1,X1)
| ~ q1(X2,c,X2)
| ~ k2(X1,c) ),
rule_163,
[final] ).
cnf(i_0_435,axiom,
( p1(X1,X1,X1)
| ~ m0(b,X2,b)
| ~ l1(X1,b) ),
rule_084,
[final] ).
cnf(i_0_436,axiom,
( p3(X1,X1,X1)
| ~ n2(X1)
| ~ q2(X2,X3,X1)
| ~ s1(X2) ),
rule_247,
[final] ).
cnf(i_0_437,axiom,
( m3(X1,X2,X2)
| ~ n2(X1)
| ~ m2(X2)
| ~ m3(X3,X1,X3) ),
rule_228,
[final] ).
cnf(i_0_438,axiom,
( k3(X1,X1,X2)
| ~ p1(X2,X3,X1)
| ~ m2(X4)
| ~ m2(X3) ),
rule_201,
[final] ).
cnf(i_0_439,axiom,
( q1(X1,X2,X2)
| ~ k0(X3)
| ~ l0(X1)
| ~ q1(X2,X2,X3) ),
rule_099,
[final] ).
cnf(i_0_440,axiom,
( m1(X1,X1,X1)
| ~ l0(X1)
| ~ k0(X1)
| ~ m0(X1,X1,X1) ),
rule_028,
[final] ).
cnf(i_0_441,axiom,
( p2(a,X1,d)
| ~ n0(X1,d)
| ~ m1(a,X1,d) ),
rule_166,
[final] ).
cnf(i_0_442,axiom,
( p1(X1,X2,X1)
| ~ l0(X3)
| ~ p1(X2,X4,X1)
| ~ s0(b) ),
rule_071,
[final] ).
cnf(i_0_443,axiom,
( m3(c,b,d)
| ~ l1(d,b)
| ~ m2(d)
| ~ q2(b,c,d) ),
rule_230,
[final] ).
cnf(i_0_444,axiom,
( k3(d,d,d)
| ~ p1(a,d,b)
| ~ r2(a)
| ~ l2(e,b) ),
rule_203,
[final] ).
cnf(i_0_445,axiom,
( q2(d,a,a)
| ~ q2(d,c,a)
| ~ s1(c)
| ~ q0(e,c) ),
rule_180,
[final] ).
cnf(i_0_446,axiom,
( n1(d,e,e)
| ~ p0(d,d)
| ~ n1(e,e,e)
| ~ r0(b) ),
rule_055,
[final] ).
cnf(i_0_447,axiom,
( n1(d,d,b)
| ~ q0(b,e)
| ~ m1(d,e,e)
| ~ k0(b) ),
rule_060,
[final] ).
cnf(i_0_448,axiom,
( k3(X1,X1,X1)
| ~ s1(X1)
| ~ q2(d,X2,d)
| ~ s2(X2) ),
rule_193,
[final] ).
cnf(i_0_449,axiom,
( p4(X1,X1,X2)
| ~ r0(X1)
| ~ r3(X2,X1,X2) ),
rule_285,
[final] ).
cnf(i_0_450,axiom,
( p3(X1,X1,X1)
| ~ p2(X2,X1,X1)
| ~ n3(X1) ),
rule_248,
[final] ).
cnf(i_0_451,axiom,
( p3(X1,X1,X1)
| ~ k1(X1)
| ~ q2(X2,X3,X1) ),
rule_250,
[final] ).
cnf(i_0_452,axiom,
( p3(X1,X2,X3)
| ~ r2(X2)
| ~ k3(X2,X3,X1) ),
rule_242,
[final] ).
cnf(i_0_453,axiom,
( m3(X1,X1,X2)
| ~ r2(X2)
| ~ k3(X1,X2,X1) ),
rule_235,
[final] ).
cnf(i_0_454,axiom,
( k3(X1,X1,X1)
| ~ r1(X1)
| ~ p2(X2,X3,X3) ),
rule_213,
[final] ).
cnf(i_0_455,axiom,
( q2(X1,X1,X1)
| ~ k1(X2)
| ~ n1(X1,X1,X2) ),
rule_179,
[final] ).
cnf(i_0_456,axiom,
( q2(X1,X2,X2)
| ~ k0(X2)
| ~ p1(X1,X1,X1) ),
rule_177,
[final] ).
cnf(i_0_457,axiom,
( q1(X1,X1,X1)
| ~ m0(X1,X1,X2)
| ~ k0(X2) ),
rule_114,
[final] ).
cnf(i_0_458,axiom,
( q1(X1,X1,X1)
| ~ s0(X1)
| ~ m0(X2,X2,X3) ),
rule_098,
[final] ).
cnf(i_0_459,axiom,
( q1(X1,X1,X2)
| ~ r0(X3)
| ~ m1(X1,X2,X2) ),
rule_113,
[final] ).
cnf(i_0_460,axiom,
( p1(X1,X1,X1)
| ~ l0(X1)
| ~ m0(X2,X3,X1) ),
rule_086,
[final] ).
cnf(i_0_461,axiom,
( n1(X1,X1,X1)
| ~ m1(X2,X3,X1)
| ~ k0(X2) ),
rule_046,
[final] ).
cnf(i_0_462,axiom,
( m1(X1,X2,X2)
| ~ l0(X3)
| ~ m0(X2,X2,X1) ),
rule_015,
[final] ).
cnf(i_0_463,axiom,
( p2(c,e,e)
| ~ l1(c,b)
| ~ q1(e,e,e) ),
rule_143,
[final] ).
cnf(i_0_464,axiom,
( p1(d,d,b)
| ~ p0(d,b)
| ~ m0(e,a,a) ),
rule_078,
[final] ).
cnf(i_0_465,axiom,
( m1(c,a,c)
| ~ r0(e)
| ~ m0(a,e,c)
| ~ r0(X1)
| ~ k0(e) ),
rule_031,
[final] ).
cnf(i_0_466,axiom,
( p2(X1,X2,X2)
| ~ k1(X3)
| ~ p2(e,X1,X2) ),
rule_155,
[final] ).
cnf(i_0_467,axiom,
( q1(X1,X1,X1)
| ~ m0(c,X1,X1)
| ~ r0(X1) ),
rule_123,
[final] ).
cnf(i_0_468,axiom,
( p1(X1,X1,X1)
| ~ m0(X2,X3,b)
| ~ l0(X1) ),
rule_064,
[final] ).
cnf(i_0_469,axiom,
( p1(X1,b,X2)
| ~ m1(X1,X2,b)
| ~ k0(X2) ),
rule_083,
[final] ).
cnf(i_0_470,axiom,
( n1(X1,e,e)
| ~ m0(X1,X2,e)
| ~ k1(X1) ),
rule_040,
[final] ).
cnf(i_0_471,axiom,
( p2(e,X1,X2)
| ~ r0(e)
| ~ p1(X1,X2,e) ),
rule_145,
[final] ).
cnf(i_0_472,axiom,
( p2(X1,X1,d)
| ~ r1(a)
| ~ m0(X2,X1,d) ),
rule_149,
[final] ).
cnf(i_0_473,axiom,
( p5(b,b,b)
| ~ p4(X1,X1,X2)
| ~ k5(b) ),
rule_321,
[final] ).
cnf(i_0_474,axiom,
( p4(X1,X1,X1)
| ~ p3(X2,X2,X1) ),
rule_291,
[final] ).
cnf(i_0_475,axiom,
( p4(X1,X2,X1)
| ~ k3(X1,X1,X2) ),
rule_287,
[final] ).
cnf(i_0_476,axiom,
( r3(X1,X2,X1)
| ~ p2(X1,X3,X2) ),
rule_267,
[final] ).
cnf(i_0_477,axiom,
( m3(X1,X1,X1)
| ~ p2(X1,X1,X1) ),
rule_238,
[final] ).
cnf(i_0_478,axiom,
( k3(X1,X1,X1)
| ~ p2(X2,X1,X1) ),
rule_205,
[final] ).
cnf(i_0_479,axiom,
( k3(X1,X2,X1)
| ~ p2(X2,X1,X1) ),
rule_206,
[final] ).
cnf(i_0_480,axiom,
( q2(X1,X1,X1)
| ~ p1(X1,X1,X1) ),
rule_181,
[final] ).
cnf(i_0_481,axiom,
( p2(X1,X1,X1)
| ~ q1(X1,X1,X1) ),
rule_154,
[final] ).
cnf(i_0_482,axiom,
( p2(X1,X1,X1)
| ~ m1(X2,X2,X1) ),
rule_150,
[final] ).
cnf(i_0_483,axiom,
( p2(X1,X2,X1)
| ~ m1(X2,X1,X2) ),
rule_176,
[final] ).
cnf(i_0_484,axiom,
( q1(X1,X1,X1)
| ~ m0(X1,X2,X1) ),
rule_122,
[final] ).
cnf(i_0_485,axiom,
( q1(X1,X1,X1)
| ~ m0(X2,X3,X1) ),
rule_121,
[final] ).
cnf(i_0_486,axiom,
( q1(X1,X1,X1)
| ~ m0(X2,X3,X1) ),
rule_110,
[final] ).
cnf(i_0_487,axiom,
( m1(X1,X1,X1)
| ~ m0(X2,X2,X1) ),
rule_006,
[final] ).
cnf(i_0_488,axiom,
( m1(X1,X1,X1)
| ~ m0(X2,X3,X1) ),
rule_025,
[final] ).
cnf(i_0_489,axiom,
( m1(X1,X1,X1)
| ~ m0(X2,X3,X1) ),
rule_014,
[final] ).
cnf(i_0_490,axiom,
( m1(X1,X2,X1)
| ~ m0(X2,X2,X1) ),
rule_005,
[final] ).
cnf(i_0_491,axiom,
( m3(X1,c,X1)
| ~ s2(c)
| ~ q2(X1,c,c) ),
rule_237,
[final] ).
cnf(i_0_492,axiom,
( n1(X1,X1,X2)
| ~ m0(b,X2,X1) ),
rule_036,
[final] ).
cnf(i_0_493,axiom,
( q2(X1,X1,X1)
| ~ q1(X2,c,X1) ),
rule_184,
[final] ).
cnf(i_0_494,axiom,
( n1(e,e,X1)
| ~ s0(b)
| ~ m1(b,X1,e) ),
rule_041,
[final] ).
cnf(i_0_495,axiom,
( p4(c,c,X1)
| ~ n3(a)
| ~ m3(X1,c,a) ),
rule_294,
[final] ).
cnf(i_0_496,axiom,
( m3(X1,e,e)
| ~ n2(e)
| ~ p2(X1,e,e) ),
rule_234,
[final] ).
cnf(i_0_497,axiom,
( p2(X1,a,X1)
| ~ q1(X1,a,X1) ),
rule_141,
[final] ).
cnf(i_0_498,axiom,
( n1(X1,c,X1)
| ~ m0(X2,X1,c) ),
rule_039,
[final] ).
cnf(i_0_499,axiom,
( p2(X1,X1,X1)
| ~ n1(d,d,X1) ),
rule_153,
[final] ).
cnf(i_0_500,axiom,
( q1(X1,X1,X1)
| ~ m0(X1,c,b) ),
rule_103,
[final] ).
cnf(i_0_501,axiom,
( p2(X1,e,X1)
| ~ n1(X1,e,e) ),
rule_170,
[final] ).
cnf(i_0_502,axiom,
( p1(a,b,a)
| ~ r0(b)
| ~ p1(a,a,a) ),
rule_087,
[final] ).
cnf(i_0_503,axiom,
( q3(X1,X1)
| ~ m0(X2,d,X2)
| ~ k1(X1)
| ~ r2(d)
| ~ q3(X2,X1) ),
rule_259,
[final] ).
cnf(i_0_504,axiom,
( q3(X1,X2)
| ~ n1(X3,X1,X2)
| ~ s2(X1)
| ~ q3(X2,X1) ),
rule_257,
[final] ).
cnf(i_0_505,axiom,
( l2(X1,X1)
| ~ p0(X2,X2)
| ~ s1(X3)
| ~ m0(X4,X3,X1) ),
rule_133,
[final] ).
cnf(i_0_506,axiom,
( k2(X1,X2)
| ~ m1(X3,X2,X1)
| ~ k1(X4)
| ~ k2(X4,X2) ),
rule_127,
[final] ).
cnf(i_0_507,axiom,
( l1(X1,X2)
| ~ p0(X3,X1)
| ~ r0(X4)
| ~ m0(X2,X1,X3) ),
rule_003,
[final] ).
cnf(i_0_508,axiom,
( m3(b,b,b)
| ~ q2(a,b,a) ),
rule_229,
[final] ).
cnf(i_0_509,axiom,
( p2(a,a,a)
| ~ p1(e,e,a) ),
rule_172,
[final] ).
cnf(i_0_510,axiom,
( p2(d,b,b)
| ~ p1(d,b,e) ),
rule_161,
[final] ).
cnf(i_0_511,axiom,
( p1(c,e,b)
| ~ m0(b,c,e) ),
rule_077,
[final] ).
cnf(i_0_512,axiom,
( n5(X1,X1)
| ~ m0(X2,X1,X2)
| ~ n5(X2,X1) ),
rule_308,
[final] ).
cnf(i_0_513,axiom,
( n4(X1,X2)
| ~ p3(X1,X2,X2)
| ~ n4(X1,X1) ),
rule_281,
[final] ).
cnf(i_0_514,axiom,
( q3(X1,X1)
| ~ p2(X2,X1,X1)
| ~ q3(X2,X1) ),
rule_256,
[final] ).
cnf(i_0_515,axiom,
( q3(X1,X2)
| ~ q2(X3,X1,X2)
| ~ n0(X3,X1) ),
rule_255,
[final] ).
cnf(i_0_516,axiom,
( l3(X1,X1)
| ~ k3(X2,X1,X1)
| ~ l2(X3,X3) ),
rule_222,
[final] ).
cnf(i_0_517,axiom,
( p4(X1,X1,X1)
| ~ q3(X2,X3)
| ~ n4(X3,X1)
| ~ l3(X2,X2) ),
rule_293,
[final] ).
cnf(i_0_518,axiom,
( p1(X1,X1,X1)
| ~ l1(X2,X2)
| ~ p0(X1,X2)
| ~ n0(X2,X2) ),
rule_065,
[final] ).
cnf(i_0_519,axiom,
( m1(X1,X1,c)
| ~ n0(X2,X2)
| ~ l1(c,c)
| ~ p0(X2,X1) ),
rule_010,
[final] ).
cnf(i_0_520,axiom,
( q1(X1,X2,X1)
| ~ l0(X1)
| ~ r0(X3)
| ~ p0(X4,X1)
| ~ q0(X2,X2) ),
rule_104,
[final] ).
cnf(i_0_521,axiom,
( n5(d,X1)
| ~ k3(d,X1,a)
| ~ n4(X1,d) ),
rule_317,
[final] ).
cnf(i_0_522,axiom,
( r1(X1)
| ~ q0(X1,X2)
| ~ s0(d)
| ~ q1(d,X2,d) ),
rule_124,
[final] ).
cnf(i_0_523,axiom,
( s4(X1)
| ~ p3(X2,X3,X4)
| ~ l1(X1,X3) ),
rule_299,
[final] ).
cnf(i_0_524,axiom,
( p2(X1,X1,X1)
| ~ k1(X2)
| ~ k0(X2)
| ~ l2(a,X2)
| ~ k2(X1,a) ),
rule_142,
[final] ).
cnf(i_0_525,axiom,
( n5(b,e)
| ~ r3(d,b,c)
| ~ n4(b,e) ),
rule_312,
[final] ).
cnf(i_0_526,axiom,
( q4(b,b)
| ~ k3(c,e,b)
| ~ l1(b,c) ),
rule_297,
[final] ).
cnf(i_0_527,axiom,
( n4(e,e)
| ~ l3(b,a)
| ~ p3(b,e,a) ),
rule_283,
[final] ).
cnf(i_0_528,axiom,
( m5(X1,X2)
| ~ r0(X1)
| ~ p4(X1,X3,X2) ),
rule_303,
[final] ).
cnf(i_0_529,axiom,
( n4(X1,X1)
| ~ k4(X2)
| ~ m3(X1,X1,X1) ),
rule_284,
[final] ).
cnf(i_0_530,axiom,
( l3(X1,X2)
| ~ r0(X1)
| ~ p2(X1,X2,X1) ),
rule_215,
[final] ).
cnf(i_0_531,axiom,
( q1(X1,X1,X2)
| ~ p0(X3,X3)
| ~ q0(X2,X1)
| ~ k1(X1) ),
rule_109,
[final] ).
cnf(i_0_532,axiom,
( m1(X1,X2,c)
| ~ r0(c)
| ~ s0(d)
| ~ q0(X2,d)
| ~ p0(X1,X2) ),
rule_019,
[final] ).
cnf(i_0_533,axiom,
( n1(X1,d,X2)
| ~ p0(X2,X2)
| ~ r0(X1)
| ~ l1(X2,d) ),
rule_047,
[final] ).
cnf(i_0_534,axiom,
( k2(X1,X1)
| ~ q1(X2,X1,X1) ),
rule_129,
[final] ).
cnf(i_0_535,axiom,
( p3(X1,X1,X1)
| ~ q0(X2,X1)
| ~ k2(X3,X3) ),
rule_252,
[final] ).
cnf(i_0_536,axiom,
( q1(X1,X2,X1)
| ~ n0(X3,X2)
| ~ p0(X4,X1) ),
rule_092,
[final] ).
cnf(i_0_537,axiom,
( n1(X1,X1,X1)
| ~ l1(X2,X1)
| ~ n0(X2,X1) ),
rule_058,
[final] ).
cnf(i_0_538,axiom,
( n1(X1,X2,X1)
| ~ p0(X1,X1)
| ~ p0(X2,X3) ),
rule_044,
[final] ).
cnf(i_0_539,axiom,
( m1(X1,X1,X1)
| ~ q0(X2,X3)
| ~ q0(X2,X1) ),
rule_018,
[final] ).
cnf(i_0_540,axiom,
( l3(d,c)
| ~ s2(d)
| ~ k3(a,c,a)
| ~ r0(b) ),
rule_224,
[final] ).
cnf(i_0_541,axiom,
( m3(X1,X1,X1)
| ~ q0(X2,X3)
| ~ s0(X4)
| ~ s2(X3)
| ~ r2(X1) ),
rule_227,
[final] ).
cnf(i_0_542,axiom,
( n1(X1,X1,X1)
| ~ n0(X1,X1)
| ~ q0(a,X1) ),
rule_038,
[final] ).
cnf(i_0_543,axiom,
( k5(X1)
| ~ s4(X2)
| ~ r3(X3,X1,X1) ),
rule_300,
[final] ).
cnf(i_0_544,axiom,
( l4(X1)
| ~ m0(X2,X1,X1)
| ~ l4(X2) ),
rule_278,
[final] ).
cnf(i_0_545,axiom,
( n2(e)
| ~ r1(b)
| ~ r0(e)
| ~ p1(b,X1,X2) ),
rule_140,
[final] ).
cnf(i_0_546,axiom,
( p1(X1,X1,X1)
| ~ n0(e,b)
| ~ k0(b)
| ~ k0(X1)
| ~ k1(X2) ),
rule_073,
[final] ).
cnf(i_0_547,axiom,
( n1(X1,X2,X1)
| ~ p0(X3,X1)
| ~ l0(X2)
| ~ r0(X1) ),
rule_037,
[final] ).
cnf(i_0_548,axiom,
( m1(X1,X1,X1)
| ~ s0(X2)
| ~ r0(X2)
| ~ q0(X3,X1) ),
rule_009,
[final] ).
cnf(i_0_549,axiom,
( s2(X1)
| ~ q2(b,X1,b)
| ~ s1(b) ),
rule_189,
[final] ).
cnf(i_0_550,axiom,
( l4(X1)
| ~ p3(X2,X3,X1) ),
rule_277,
[final] ).
cnf(i_0_551,axiom,
( n3(X1)
| ~ p2(X2,X3,X1) ),
rule_240,
[final] ).
cnf(i_0_552,axiom,
( n2(X1)
| ~ p1(X2,X3,X1) ),
rule_137,
[final] ).
cnf(i_0_553,axiom,
( n5(d,d)
| ~ p4(c,d,c) ),
rule_311,
[final] ).
cnf(i_0_554,axiom,
( n1(a,X1,b)
| ~ p0(X1,d)
| ~ p0(a,b) ),
rule_053,
[final] ).
cnf(i_0_555,axiom,
( m1(X1,X2,X2)
| ~ k1(a)
| ~ k1(X2)
| ~ q0(X1,X1) ),
rule_034,
[final] ).
cnf(i_0_556,axiom,
( m1(X1,X1,X1)
| ~ l0(X1)
| ~ l0(X2)
| ~ p0(X2,d) ),
rule_026,
[final] ).
cnf(i_0_557,axiom,
( q2(X1,c,X2)
| ~ k1(X2)
| ~ l0(c)
| ~ l2(X2,X1) ),
rule_183,
[final] ).
cnf(i_0_558,axiom,
( n1(X1,X2,X1)
| ~ s0(b)
| ~ l0(X1)
| ~ p0(b,X2) ),
rule_050,
[final] ).
cnf(i_0_559,axiom,
( k5(b)
| ~ s4(e)
| ~ n1(b,b,b) ),
rule_301,
[final] ).
cnf(i_0_560,axiom,
( m1(b,b,b)
| ~ q0(c,d)
| ~ l1(a,b) ),
rule_027,
[final] ).
cnf(i_0_561,axiom,
( p5(X1,X1,X2)
| ~ s4(X2)
| ~ l2(X1,X1) ),
rule_318,
[final] ).
cnf(i_0_562,axiom,
( p5(X1,X2,X1)
| ~ q4(X2,X3)
| ~ s1(X1) ),
rule_320,
[final] ).
cnf(i_0_563,axiom,
( p4(X1,X1,X1)
| ~ q3(X2,X3)
| ~ n3(X1) ),
rule_286,
[final] ).
cnf(i_0_564,axiom,
( m3(X1,X1,X1)
| ~ l2(X1,X1)
| ~ n2(X1) ),
rule_232,
[final] ).
cnf(i_0_565,axiom,
( p1(X1,X1,X2)
| ~ p0(X2,X1)
| ~ r0(X1) ),
rule_074,
[final] ).
cnf(i_0_566,axiom,
( n1(X1,X1,X1)
| ~ k1(X1)
| ~ p0(X1,X1) ),
rule_043,
[final] ).
cnf(i_0_567,axiom,
( m1(X1,X1,X2)
| ~ k0(X1)
| ~ n0(X2,X2) ),
rule_011,
[final] ).
cnf(i_0_568,axiom,
( m1(X1,X2,X1)
| ~ p0(X3,X2)
| ~ r0(X1) ),
rule_007,
[final] ).
cnf(i_0_569,axiom,
( m1(X1,X2,X1)
| ~ p0(X1,X2)
| ~ s0(X1) ),
rule_029,
[final] ).
cnf(i_0_570,negated_conjecture,
~ m1(X1,X1,e),
prove_this,
[final] ).
cnf(i_0_571,axiom,
( r3(X1,X2,X2)
| ~ s2(X2)
| ~ l2(c,X1) ),
rule_260,
[final] ).
cnf(i_0_572,axiom,
( m3(X1,X2,X1)
| ~ r2(X1)
| ~ k2(c,X2) ),
rule_231,
[final] ).
cnf(i_0_573,axiom,
( p1(X1,X1,X2)
| ~ n0(d,X1)
| ~ k0(X2) ),
rule_063,
[final] ).
cnf(i_0_574,axiom,
( k3(X1,X1,X1)
| ~ l2(X2,b)
| ~ k1(X1) ),
rule_197,
[final] ).
cnf(i_0_575,axiom,
( q1(X1,X1,X2)
| ~ s0(X1)
| ~ p0(X2,d) ),
rule_105,
[final] ).
cnf(i_0_576,axiom,
( m1(X1,X1,X1)
| ~ s0(X1)
| ~ q0(X2,d) ),
rule_017,
[final] ).
cnf(i_0_577,axiom,
( k3(X1,X1,X1)
| ~ r2(c)
| ~ l1(b,X1) ),
rule_208,
[final] ).
cnf(i_0_578,axiom,
( r3(X1,X1,X1)
| ~ l2(X2,X1) ),
rule_265,
[final] ).
cnf(i_0_579,axiom,
( p3(X1,X1,X1)
| ~ l2(X1,X1) ),
rule_246,
[final] ).
cnf(i_0_580,axiom,
( k3(X1,X1,X2)
| ~ k2(X2,X1) ),
rule_194,
[final] ).
cnf(i_0_581,axiom,
( q2(X1,X1,X2)
| ~ l1(X2,X1) ),
rule_186,
[final] ).
cnf(i_0_582,axiom,
( p2(X1,X1,X1)
| ~ l1(X2,X1) ),
rule_175,
[final] ).
cnf(i_0_583,axiom,
( q1(X1,X1,X1)
| ~ n0(X2,X1) ),
rule_100,
[final] ).
cnf(i_0_584,axiom,
( q1(X1,X1,X1)
| ~ q0(X2,X1) ),
rule_093,
[final] ).
cnf(i_0_585,axiom,
( q1(X1,X2,X2)
| ~ p0(X2,X1) ),
rule_095,
[final] ).
cnf(i_0_586,axiom,
( p1(X1,X1,X1)
| ~ p0(X2,X1) ),
rule_085,
[final] ).
cnf(i_0_587,axiom,
( p1(X1,X1,X1)
| ~ n0(X2,X1) ),
rule_066,
[final] ).
cnf(i_0_588,axiom,
( p1(X1,X1,X1)
| ~ q0(X2,X1) ),
rule_067,
[final] ).
cnf(i_0_589,axiom,
( p1(X1,X1,X2)
| ~ p0(X2,X1) ),
rule_069,
[final] ).
cnf(i_0_590,axiom,
( m1(X1,X1,X1)
| ~ q0(X2,X1) ),
rule_013,
[final] ).
cnf(i_0_591,axiom,
( p2(X1,X1,X1)
| ~ l1(X1,d) ),
rule_157,
[final] ).
cnf(i_0_592,axiom,
( k3(c,c,c)
| ~ s2(e)
| ~ k2(c,e) ),
rule_195,
[final] ).
cnf(i_0_593,axiom,
( p2(e,c,c)
| ~ r1(d)
| ~ l1(e,c) ),
rule_147,
[final] ).
cnf(i_0_594,axiom,
( k3(X1,X1,X1)
| ~ l0(X1)
| ~ r2(e)
| ~ r0(e) ),
rule_211,
[final] ).
cnf(i_0_595,axiom,
( p1(X1,X1,X1)
| ~ k0(e)
| ~ k1(X1)
| ~ l0(c) ),
rule_079,
[final] ).
cnf(i_0_596,axiom,
( p3(X1,X1,X1)
| ~ k1(X1)
| ~ n2(X1) ),
rule_249,
[final] ).
cnf(i_0_597,axiom,
( m3(X1,X1,X1)
| ~ n2(X1)
| ~ m2(X2) ),
rule_233,
[final] ).
cnf(i_0_598,axiom,
( p2(X1,X1,X1)
| ~ s1(X1)
| ~ k1(X1) ),
rule_167,
[final] ).
cnf(i_0_599,axiom,
( p2(X1,X1,X1)
| ~ r1(X2)
| ~ r0(X1) ),
rule_173,
[final] ).
cnf(i_0_600,axiom,
( q1(X1,X1,X1)
| ~ k0(X1)
| ~ l0(X2) ),
rule_102,
[final] ).
cnf(i_0_601,axiom,
( p1(X1,X1,X1)
| ~ s0(X2)
| ~ s0(X1) ),
rule_072,
[final] ).
cnf(i_0_602,axiom,
( n1(X1,X1,X1)
| ~ k0(X1)
| ~ s0(X1) ),
rule_061,
[final] ).
cnf(i_0_603,axiom,
( m1(X1,X2,X1)
| ~ l0(X1)
| ~ k0(X2) ),
rule_021,
[final] ).
cnf(i_0_604,axiom,
( m1(X1,X2,X1)
| ~ r0(X1)
| ~ l0(X2) ),
rule_035,
[final] ).
cnf(i_0_605,axiom,
( p3(b,c,b)
| ~ k2(c,b) ),
rule_253,
[final] ).
cnf(i_0_606,axiom,
( m3(b,b,b)
| ~ l2(a,b) ),
rule_239,
[final] ).
cnf(i_0_607,axiom,
( p1(c,c,c)
| ~ p0(a,c) ),
rule_070,
[final] ).
cnf(i_0_608,axiom,
( p1(a,a,a)
| ~ p0(b,a) ),
rule_075,
[final] ).
cnf(i_0_609,axiom,
( n1(d,d,d)
| ~ q0(d,d) ),
rule_045,
[final] ).
cnf(i_0_610,axiom,
( l3(X1,X1)
| ~ n2(X2)
| ~ l1(X3,X1)
| ~ l3(X3,X3) ),
rule_219,
[final] ).
cnf(i_0_611,axiom,
( p2(X1,X1,X1)
| ~ n2(X1)
| ~ k1(e) ),
rule_174,
[final] ).
cnf(i_0_612,axiom,
( q1(X1,X1,X1)
| ~ k1(X1)
| ~ s0(b) ),
rule_112,
[final] ).
cnf(i_0_613,axiom,
( n5(X1,X1)
| ~ p0(X1,X2)
| ~ m4(X3,X3)
| ~ k5(d) ),
rule_310,
[final] ).
cnf(i_0_614,axiom,
( l2(X1,X2)
| ~ s1(X1)
| ~ n0(e,X2)
| ~ l2(X2,X2) ),
rule_131,
[final] ).
cnf(i_0_615,axiom,
( q1(b,e,e)
| ~ s0(e)
| ~ k0(b)
| ~ l0(c) ),
rule_094,
[final] ).
cnf(i_0_616,axiom,
( q1(X1,b,b)
| ~ s0(X1)
| ~ s0(b) ),
rule_119,
[final] ).
cnf(i_0_617,axiom,
( r3(X1,X1,X1)
| ~ s2(X1) ),
rule_264,
[final] ).
cnf(i_0_618,axiom,
( r3(X1,X1,X1)
| ~ r2(X1) ),
rule_266,
[final] ).
cnf(i_0_619,axiom,
( p3(X1,X1,X1)
| ~ n2(X1) ),
rule_244,
[final] ).
cnf(i_0_620,axiom,
( m3(X1,X1,X1)
| ~ n2(X1) ),
rule_236,
[final] ).
cnf(i_0_621,axiom,
( k3(X1,X1,X1)
| ~ n2(X1) ),
rule_210,
[final] ).
cnf(i_0_622,axiom,
( k3(X1,X1,X1)
| ~ m2(X1) ),
rule_212,
[final] ).
cnf(i_0_623,axiom,
( p2(X1,X1,X1)
| ~ k1(X1) ),
rule_159,
[final] ).
cnf(i_0_624,axiom,
( q1(X1,X1,X1)
| ~ r0(X1) ),
rule_116,
[final] ).
cnf(i_0_625,axiom,
( q1(X1,X1,X1)
| ~ s0(X1) ),
rule_106,
[final] ).
cnf(i_0_626,axiom,
( q1(X1,X1,X1)
| ~ s0(X1) ),
rule_097,
[final] ).
cnf(i_0_627,axiom,
( p1(X1,X1,X1)
| ~ k0(X1) ),
rule_068,
[final] ).
cnf(i_0_628,axiom,
( n1(X1,X1,X1)
| ~ r0(X1) ),
rule_057,
[final] ).
cnf(i_0_629,axiom,
( m1(X1,X1,X1)
| ~ s0(X1) ),
rule_032,
[final] ).
cnf(i_0_630,axiom,
( k3(c,c,c)
| ~ k0(a)
| ~ r2(c) ),
rule_198,
[final] ).
cnf(i_0_631,axiom,
( p2(d,d,d)
| ~ k1(d)
| ~ s0(d) ),
rule_151,
[final] ).
cnf(i_0_632,axiom,
( q1(d,d,d)
| ~ k0(e)
| ~ s0(d) ),
rule_117,
[final] ).
cnf(i_0_633,axiom,
( p1(e,e,e)
| ~ r0(e)
| ~ k0(e) ),
rule_090,
[final] ).
cnf(i_0_634,axiom,
( n1(a,a,a)
| ~ l0(a)
| ~ r0(a) ),
rule_056,
[final] ).
cnf(i_0_635,axiom,
( m1(a,a,a)
| ~ l0(a)
| ~ s0(d) ),
rule_023,
[final] ).
cnf(i_0_636,axiom,
( m4(X1,X2)
| ~ l2(X3,X2)
| ~ s3(a,X1) ),
rule_279,
[final] ).
cnf(i_0_637,axiom,
( r4(X1)
| ~ n3(X1)
| ~ q3(X2,X3)
| ~ p0(X4,X1) ),
rule_298,
[final] ).
cnf(i_0_638,axiom,
( k3(c,c,c)
| ~ r2(c) ),
rule_214,
[final] ).
cnf(i_0_639,axiom,
( k3(a,a,a)
| ~ r2(a) ),
rule_204,
[final] ).
cnf(i_0_640,axiom,
( q1(b,b,b)
| ~ l0(b) ),
rule_115,
[final] ).
cnf(i_0_641,axiom,
( q1(b,b,b)
| ~ r0(b) ),
rule_120,
[final] ).
cnf(i_0_642,axiom,
( p1(a,a,a)
| ~ l0(a) ),
rule_088,
[final] ).
cnf(i_0_643,axiom,
( n1(c,c,c)
| ~ l0(c) ),
rule_049,
[final] ).
cnf(i_0_644,axiom,
( m1(c,c,c)
| ~ l0(c) ),
rule_020,
[final] ).
cnf(i_0_645,axiom,
( m1(b,b,b)
| ~ l0(b) ),
rule_008,
[final] ).
cnf(i_0_646,axiom,
( m1(e,e,e)
| ~ r0(e) ),
rule_030,
[final] ).
cnf(i_0_647,axiom,
( m1(e,e,e)
| ~ r0(e) ),
rule_012,
[final] ).
cnf(i_0_648,axiom,
( m1(e,e,e)
| ~ s0(e) ),
rule_022,
[final] ).
cnf(i_0_649,axiom,
m0(X1,d,X2),
axiom_19,
[final] ).
cnf(i_0_650,axiom,
m0(a,X1,a),
axiom_12,
[final] ).
cnf(i_0_651,axiom,
( q4(X1,X1)
| ~ r1(X1)
| ~ l4(X2)
| ~ q4(X2,X3) ),
rule_296,
[final] ).
cnf(i_0_652,axiom,
( q3(X1,X1)
| ~ r2(X1)
| ~ s1(X2)
| ~ l2(X3,X3) ),
rule_258,
[final] ).
cnf(i_0_653,axiom,
( l1(X1,X1)
| ~ k1(X1)
| ~ l0(X2)
| ~ l1(X2,X2) ),
rule_004,
[final] ).
cnf(i_0_654,axiom,
m0(c,b,a),
axiom_16,
[final] ).
cnf(i_0_655,axiom,
m0(b,b,e),
axiom_31,
[final] ).
cnf(i_0_656,axiom,
m0(b,a,a),
axiom_38,
[final] ).
cnf(i_0_657,axiom,
m0(a,e,e),
axiom_23,
[final] ).
cnf(i_0_658,axiom,
m0(e,b,c),
axiom_27,
[final] ).
cnf(i_0_659,axiom,
m0(e,d,a),
axiom_4,
[final] ).
cnf(i_0_660,axiom,
m0(e,d,e),
axiom_8,
[final] ).
cnf(i_0_661,axiom,
m0(d,e,c),
axiom_35,
[final] ).
cnf(i_0_662,axiom,
( s5(X1)
| ~ k4(X1)
| ~ s3(X1,X2)
| ~ l5(X3)
| ~ s5(X3) ),
rule_330,
[final] ).
cnf(i_0_663,axiom,
( l3(X1,X1)
| ~ s2(X2)
| ~ l1(X1,X1) ),
rule_220,
[final] ).
cnf(i_0_664,axiom,
( k4(c)
| ~ n0(c,d)
| ~ q3(e,b)
| ~ n3(e) ),
rule_274,
[final] ).
cnf(i_0_665,axiom,
( m5(X1,X1)
| ~ s4(X1)
| ~ m4(e,e) ),
rule_305,
[final] ).
cnf(i_0_666,axiom,
( q5(X1,X1)
| ~ q4(X1,X1) ),
rule_325,
[final] ).
cnf(i_0_667,axiom,
( q5(X1,X1)
| ~ m4(X1,X1) ),
rule_326,
[final] ).
cnf(i_0_668,axiom,
( n5(X1,X1)
| ~ q4(X2,X1) ),
rule_313,
[final] ).
cnf(i_0_669,axiom,
( n5(X1,X1)
| ~ n4(X2,X1) ),
rule_309,
[final] ).
cnf(i_0_670,axiom,
( l1(X1,X1)
| ~ n0(X2,X1) ),
rule_002,
[final] ).
cnf(i_0_671,axiom,
( l5(X1)
| ~ q4(X2,X2)
| ~ k1(X1) ),
rule_302,
[final] ).
cnf(i_0_672,axiom,
( m2(X1)
| ~ s0(X1)
| ~ l1(X2,X3) ),
rule_135,
[final] ).
cnf(i_0_673,axiom,
( s1(X1)
| ~ q0(X1,X2)
| ~ s1(X3) ),
rule_126,
[final] ).
cnf(i_0_674,axiom,
( r5(X1,X2)
| ~ s4(X1)
| ~ k0(b)
| ~ n3(X2) ),
rule_327,
[final] ).
cnf(i_0_675,axiom,
( l3(c,c)
| ~ k2(b,c) ),
rule_223,
[final] ).
cnf(i_0_676,axiom,
( l3(d,d)
| ~ k2(a,d) ),
rule_221,
[final] ).
cnf(i_0_677,axiom,
( k2(e,e)
| ~ l1(e,e) ),
rule_130,
[final] ).
cnf(i_0_678,axiom,
( q5(X1,X2)
| ~ s4(X1)
| ~ m2(X2) ),
rule_322,
[final] ).
cnf(i_0_679,axiom,
( n5(X1,X1)
| ~ s1(X1)
| ~ k4(X1) ),
rule_315,
[final] ).
cnf(i_0_680,axiom,
( m5(X1,X1)
| ~ s4(X2)
| ~ r0(X1) ),
rule_306,
[final] ).
cnf(i_0_681,axiom,
( s1(X1)
| ~ p0(X1,X1) ),
rule_125,
[final] ).
cnf(i_0_682,axiom,
( k1(X1)
| ~ n0(X2,X1) ),
rule_001,
[final] ).
cnf(i_0_683,axiom,
( l3(X1,X1)
| ~ n2(X1)
| ~ m2(b) ),
rule_217,
[final] ).
cnf(i_0_684,axiom,
( n2(c)
| ~ l1(e,c)
| ~ k0(b) ),
rule_139,
[final] ).
cnf(i_0_685,axiom,
( r5(X1,X1)
| ~ k4(X1) ),
rule_328,
[final] ).
cnf(i_0_686,axiom,
( q5(X1,X1)
| ~ l4(X1) ),
rule_324,
[final] ).
cnf(i_0_687,axiom,
( n5(X1,X1)
| ~ r4(X1) ),
rule_314,
[final] ).
cnf(i_0_688,axiom,
( m5(X1,X1)
| ~ k4(X1) ),
rule_304,
[final] ).
cnf(i_0_689,axiom,
( l3(X1,X1)
| ~ r2(X1) ),
rule_218,
[final] ).
cnf(i_0_690,axiom,
( s5(X1)
| ~ l4(X1)
| ~ r4(X2) ),
rule_329,
[final] ).
cnf(i_0_691,axiom,
( r2(X1)
| ~ r1(X1)
| ~ l0(X1) ),
rule_188,
[final] ).
cnf(i_0_692,axiom,
( q5(a,a)
| ~ r4(a) ),
rule_323,
[final] ).
cnf(i_0_693,axiom,
p0(b,X1),
axiom_14,
[final] ).
cnf(i_0_694,axiom,
q0(X1,d),
axiom_17,
[final] ).
cnf(i_0_695,axiom,
( s2(d)
| ~ r1(d)
| ~ s1(d) ),
rule_191,
[final] ).
cnf(i_0_696,axiom,
( s2(d)
| ~ s1(a)
| ~ s0(d) ),
rule_190,
[final] ).
cnf(i_0_697,axiom,
p0(c,b),
axiom_18,
[final] ).
cnf(i_0_698,axiom,
p0(b,c),
axiom_22,
[final] ).
cnf(i_0_699,axiom,
p0(b,d),
axiom_10,
[final] ).
cnf(i_0_700,axiom,
n0(c,d),
axiom_34,
[final] ).
cnf(i_0_701,axiom,
n0(b,a),
axiom_37,
[final] ).
cnf(i_0_702,axiom,
n0(a,b),
axiom_15,
[final] ).
cnf(i_0_703,axiom,
n0(e,b),
axiom_11,
[final] ).
cnf(i_0_704,axiom,
n0(e,e),
axiom_30,
[final] ).
cnf(i_0_705,axiom,
n0(d,c),
axiom_26,
[final] ).
cnf(i_0_706,axiom,
n0(d,b),
axiom_7,
[final] ).
cnf(i_0_707,axiom,
n0(d,e),
axiom_3,
[final] ).
cnf(i_0_708,axiom,
q0(b,b),
axiom_6,
[final] ).
cnf(i_0_709,axiom,
q0(b,e),
axiom_21,
[final] ).
cnf(i_0_710,axiom,
q0(a,b),
axiom_36,
[final] ).
cnf(i_0_711,axiom,
q0(e,d),
axiom_2,
[final] ).
cnf(i_0_712,axiom,
q0(d,c),
axiom_33,
[final] ).
cnf(i_0_713,axiom,
q0(d,b),
axiom_29,
[final] ).
cnf(i_0_714,axiom,
q0(d,d),
axiom_25,
[final] ).
cnf(i_0_715,axiom,
( m2(b)
| ~ k1(b) ),
rule_136,
[final] ).
cnf(i_0_716,axiom,
k0(b),
axiom_32,
[final] ).
cnf(i_0_717,axiom,
k0(e),
axiom_28,
[final] ).
cnf(i_0_718,axiom,
l0(c),
axiom_24,
[final] ).
cnf(i_0_719,axiom,
l0(a),
axiom_20,
[final] ).
cnf(i_0_720,axiom,
r0(b),
axiom_9,
[final] ).
cnf(i_0_721,axiom,
r0(e),
axiom_13,
[final] ).
cnf(i_0_722,axiom,
s0(b),
axiom_5,
[final] ).
cnf(i_0_723,axiom,
s0(d),
axiom_1,
[final] ).
cnf(i_0_724,plain,
$false,
inference(scs_inference,[],[i_0_570,i_0_649,i_0_489]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN237-1 : TPTP v9.2.1. Released v1.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n031.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 08:24:54 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 0.32/1.61 % Version : CSE_E---1.7
% 0.32/1.61 % Problem : theBenchmark.p
% 0.32/1.61 % SZS status Unsatisfiable for theBenchmark.p
% 0.32/1.61 % SZS output start CNFRefutation
% See solution above
% 0.32/1.63 % Total time : 1.273s
%------------------------------------------------------------------------------