%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN237-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 09:09:49 AM UTC 2026
% Result : Unsatisfiable 0.13s 5.45s
% Output : Proof 0.13s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_1,axiom,
s0(d),
file('SYN001-0.ax',axiom_1) ).
cnf(axiom_2,axiom,
q0(e,d),
file('SYN001-0.ax',axiom_2) ).
cnf(axiom_3,axiom,
n0(d,e),
file('SYN001-0.ax',axiom_3) ).
cnf(axiom_4,axiom,
m0(e,d,a),
file('SYN001-0.ax',axiom_4) ).
cnf(axiom_5,axiom,
s0(b),
file('SYN001-0.ax',axiom_5) ).
cnf(axiom_6,axiom,
q0(b,b),
file('SYN001-0.ax',axiom_6) ).
cnf(axiom_7,axiom,
n0(d,b),
file('SYN001-0.ax',axiom_7) ).
cnf(axiom_8,axiom,
m0(e,d,e),
file('SYN001-0.ax',axiom_8) ).
cnf(axiom_9,axiom,
r0(b),
file('SYN001-0.ax',axiom_9) ).
cnf(axiom_10,axiom,
p0(b,d),
file('SYN001-0.ax',axiom_10) ).
cnf(axiom_11,axiom,
n0(e,b),
file('SYN001-0.ax',axiom_11) ).
cnf(axiom_12,axiom,
m0(a,X,a),
file('SYN001-0.ax',axiom_12) ).
cnf(axiom_13,axiom,
r0(e),
file('SYN001-0.ax',axiom_13) ).
cnf(axiom_14,axiom,
p0(b,X),
file('SYN001-0.ax',axiom_14) ).
cnf(axiom_15,axiom,
n0(a,b),
file('SYN001-0.ax',axiom_15) ).
cnf(axiom_16,axiom,
m0(c,b,a),
file('SYN001-0.ax',axiom_16) ).
cnf(axiom_17,axiom,
q0(X,d),
file('SYN001-0.ax',axiom_17) ).
cnf(axiom_18,axiom,
p0(c,b),
file('SYN001-0.ax',axiom_18) ).
cnf(axiom_19,axiom,
m0(X,d,Y),
file('SYN001-0.ax',axiom_19) ).
cnf(axiom_20,axiom,
l0(a),
file('SYN001-0.ax',axiom_20) ).
cnf(axiom_21,axiom,
q0(b,e),
file('SYN001-0.ax',axiom_21) ).
cnf(axiom_22,axiom,
p0(b,c),
file('SYN001-0.ax',axiom_22) ).
cnf(axiom_23,axiom,
m0(a,e,e),
file('SYN001-0.ax',axiom_23) ).
cnf(axiom_24,axiom,
l0(c),
file('SYN001-0.ax',axiom_24) ).
cnf(axiom_25,axiom,
q0(d,d),
file('SYN001-0.ax',axiom_25) ).
cnf(axiom_26,axiom,
n0(d,c),
file('SYN001-0.ax',axiom_26) ).
cnf(axiom_27,axiom,
m0(e,b,c),
file('SYN001-0.ax',axiom_27) ).
cnf(axiom_28,axiom,
k0(e),
file('SYN001-0.ax',axiom_28) ).
cnf(axiom_29,axiom,
q0(d,b),
file('SYN001-0.ax',axiom_29) ).
cnf(axiom_30,axiom,
n0(e,e),
file('SYN001-0.ax',axiom_30) ).
cnf(axiom_31,axiom,
m0(b,b,e),
file('SYN001-0.ax',axiom_31) ).
cnf(axiom_32,axiom,
k0(b),
file('SYN001-0.ax',axiom_32) ).
cnf(axiom_33,axiom,
q0(d,c),
file('SYN001-0.ax',axiom_33) ).
cnf(axiom_34,axiom,
n0(c,d),
file('SYN001-0.ax',axiom_34) ).
cnf(axiom_35,axiom,
m0(d,e,c),
file('SYN001-0.ax',axiom_35) ).
cnf(axiom_36,axiom,
q0(a,b),
file('SYN001-0.ax',axiom_36) ).
cnf(axiom_37,axiom,
n0(b,a),
file('SYN001-0.ax',axiom_37) ).
cnf(axiom_38,axiom,
m0(b,a,a),
file('SYN001-0.ax',axiom_38) ).
cnf(rule_001,axiom,
( ~ n0(J,I)
| k1(I) ),
file('SYN001-0.ax',rule_001) ).
cnf(rule_002,axiom,
( ~ n0(H,G)
| l1(G,G) ),
file('SYN001-0.ax',rule_002) ).
cnf(rule_003,axiom,
( ~ m0(D,C,E)
| ~ r0(F)
| ~ p0(E,C)
| l1(C,D) ),
file('SYN001-0.ax',rule_003) ).
cnf(rule_004,axiom,
( ~ l1(B,B)
| ~ l0(B)
| ~ k1(A)
| l1(A,A) ),
file('SYN001-0.ax',rule_004) ).
cnf(rule_005,axiom,
( ~ m0(C,C,B)
| m1(B,C,B) ),
file('SYN001-0.ax',rule_005) ).
cnf(rule_006,axiom,
( ~ m0(A,A,J)
| m1(J,J,J) ),
file('SYN001-0.ax',rule_006) ).
cnf(rule_007,axiom,
( ~ r0(G)
| ~ p0(I,H)
| m1(G,H,G) ),
file('SYN001-0.ax',rule_007) ).
cnf(rule_008,axiom,
( ~ l0(b)
| m1(b,b,b) ),
file('SYN001-0.ax',rule_008) ).
cnf(rule_009,axiom,
( ~ q0(F,D)
| ~ r0(E)
| ~ s0(E)
| m1(D,D,D) ),
file('SYN001-0.ax',rule_009) ).
cnf(rule_010,axiom,
( ~ p0(C,B)
| ~ l1(c,c)
| ~ n0(C,C)
| m1(B,B,c) ),
file('SYN001-0.ax',rule_010) ).
cnf(rule_011,axiom,
( ~ n0(A,A)
| ~ k0(J)
| m1(J,J,A) ),
file('SYN001-0.ax',rule_011) ).
cnf(rule_012,axiom,
( ~ r0(e)
| m1(e,e,e) ),
file('SYN001-0.ax',rule_012) ).
cnf(rule_013,axiom,
( ~ q0(I,H)
| m1(H,H,H) ),
file('SYN001-0.ax',rule_013) ).
cnf(rule_014,axiom,
( ~ m0(F,G,E)
| m1(E,E,E) ),
file('SYN001-0.ax',rule_014) ).
cnf(rule_015,axiom,
( ~ m0(C,C,B)
| ~ l0(D)
| m1(B,C,C) ),
file('SYN001-0.ax',rule_015) ).
cnf(rule_016,axiom,
( ~ m1(J,A,I)
| ~ m1(J,I,H)
| m1(H,I,I) ),
file('SYN001-0.ax',rule_016) ).
cnf(rule_017,axiom,
( ~ q0(G,d)
| ~ s0(F)
| m1(F,F,F) ),
file('SYN001-0.ax',rule_017) ).
cnf(rule_018,axiom,
( ~ q0(D,C)
| ~ q0(D,E)
| m1(C,C,C) ),
file('SYN001-0.ax',rule_018) ).
cnf(rule_019,axiom,
( ~ p0(A,B)
| ~ q0(B,d)
| ~ s0(d)
| ~ r0(c)
| m1(A,B,c) ),
file('SYN001-0.ax',rule_019) ).
cnf(rule_020,axiom,
( ~ l0(c)
| m1(c,c,c) ),
file('SYN001-0.ax',rule_020) ).
cnf(rule_021,axiom,
( ~ k0(J)
| ~ l0(I)
| m1(I,J,I) ),
file('SYN001-0.ax',rule_021) ).
cnf(rule_022,axiom,
( ~ s0(e)
| m1(e,e,e) ),
file('SYN001-0.ax',rule_022) ).
cnf(rule_023,axiom,
( ~ s0(d)
| ~ l0(a)
| m1(a,a,a) ),
file('SYN001-0.ax',rule_023) ).
cnf(rule_024,axiom,
( ~ m1(G,c,G)
| ~ q0(F,G)
| ~ m0(a,H,a)
| m1(F,a,G) ),
file('SYN001-0.ax',rule_024) ).
cnf(rule_025,axiom,
( ~ m0(D,E,C)
| m1(C,C,C) ),
file('SYN001-0.ax',rule_025) ).
cnf(rule_026,axiom,
( ~ p0(B,d)
| ~ l0(B)
| ~ l0(A)
| m1(A,A,A) ),
file('SYN001-0.ax',rule_026) ).
cnf(rule_027,axiom,
( ~ l1(a,b)
| ~ q0(c,d)
| m1(b,b,b) ),
file('SYN001-0.ax',rule_027) ).
cnf(rule_028,axiom,
( ~ m0(J,J,J)
| ~ k0(J)
| ~ l0(J)
| m1(J,J,J) ),
file('SYN001-0.ax',rule_028) ).
cnf(rule_029,axiom,
( ~ s0(H)
| ~ p0(H,I)
| m1(H,I,H) ),
file('SYN001-0.ax',rule_029) ).
cnf(rule_030,axiom,
( ~ r0(e)
| m1(e,e,e) ),
file('SYN001-0.ax',rule_030) ).
cnf(rule_031,axiom,
( ~ k0(e)
| ~ r0(G)
| ~ m0(a,e,c)
| ~ r0(e)
| m1(c,a,c) ),
file('SYN001-0.ax',rule_031) ).
cnf(rule_032,axiom,
( ~ s0(F)
| m1(F,F,F) ),
file('SYN001-0.ax',rule_032) ).
cnf(rule_033,axiom,
( ~ m1(E,D,C)
| ~ q0(D,D)
| m1(C,C,C) ),
file('SYN001-0.ax',rule_033) ).
cnf(rule_034,axiom,
( ~ q0(A,A)
| ~ k1(B)
| ~ k1(a)
| m1(A,B,B) ),
file('SYN001-0.ax',rule_034) ).
cnf(rule_035,axiom,
( ~ l0(J)
| ~ r0(I)
| m1(I,J,I) ),
file('SYN001-0.ax',rule_035) ).
cnf(rule_036,axiom,
( ~ m0(b,B,A)
| n1(A,A,B) ),
file('SYN001-0.ax',rule_036) ).
cnf(rule_037,axiom,
( ~ r0(H)
| ~ l0(I)
| ~ p0(J,H)
| n1(H,I,H) ),
file('SYN001-0.ax',rule_037) ).
cnf(rule_038,axiom,
( ~ q0(a,G)
| ~ n0(G,G)
| n1(G,G,G) ),
file('SYN001-0.ax',rule_038) ).
cnf(rule_039,axiom,
( ~ m0(F,E,c)
| n1(E,c,E) ),
file('SYN001-0.ax',rule_039) ).
cnf(rule_040,axiom,
( ~ k1(C)
| ~ m0(C,D,e)
| n1(C,e,e) ),
file('SYN001-0.ax',rule_040) ).
cnf(rule_041,axiom,
( ~ m1(b,B,e)
| ~ s0(b)
| n1(e,e,B) ),
file('SYN001-0.ax',rule_041) ).
cnf(rule_042,axiom,
( ~ q0(A,J)
| ~ k0(H)
| ~ m0(I,J,I)
| n1(H,H,H) ),
file('SYN001-0.ax',rule_042) ).
cnf(rule_043,axiom,
( ~ p0(G,G)
| ~ k1(G)
| n1(G,G,G) ),
file('SYN001-0.ax',rule_043) ).
cnf(rule_044,axiom,
( ~ p0(E,F)
| ~ p0(D,D)
| n1(D,E,D) ),
file('SYN001-0.ax',rule_044) ).
cnf(rule_045,axiom,
( ~ q0(d,d)
| n1(d,d,d) ),
file('SYN001-0.ax',rule_045) ).
cnf(rule_046,axiom,
( ~ k0(B)
| ~ m1(B,C,A)
| n1(A,A,A) ),
file('SYN001-0.ax',rule_046) ).
cnf(rule_047,axiom,
( ~ l1(J,d)
| ~ r0(I)
| ~ p0(J,J)
| n1(I,d,J) ),
file('SYN001-0.ax',rule_047) ).
cnf(rule_048,axiom,
( ~ n1(F,F,F)
| ~ m0(H,F,G)
| ~ m0(G,H,H)
| n1(F,F,F) ),
file('SYN001-0.ax',rule_048) ).
cnf(rule_049,axiom,
( ~ l0(c)
| n1(c,c,c) ),
file('SYN001-0.ax',rule_049) ).
cnf(rule_050,axiom,
( ~ p0(b,E)
| ~ l0(D)
| ~ s0(b)
| n1(D,E,D) ),
file('SYN001-0.ax',rule_050) ).
cnf(rule_051,axiom,
( ~ n1(C,B,C)
| ~ m0(b,C,c)
| ~ m1(c,B,C)
| n1(B,B,B) ),
file('SYN001-0.ax',rule_051) ).
cnf(rule_052,axiom,
( ~ p0(A,J)
| ~ s0(I)
| ~ k1(I)
| ~ m0(J,J,J)
| n1(I,I,I) ),
file('SYN001-0.ax',rule_052) ).
cnf(rule_053,axiom,
( ~ p0(a,b)
| ~ p0(H,d)
| n1(a,H,b) ),
file('SYN001-0.ax',rule_053) ).
cnf(rule_054,axiom,
( ~ n1(E,F,E)
| ~ l1(G,E)
| ~ l0(G)
| n1(E,F,F) ),
file('SYN001-0.ax',rule_054) ).
cnf(rule_055,axiom,
( ~ r0(b)
| ~ n1(e,e,e)
| ~ p0(d,d)
| n1(d,e,e) ),
file('SYN001-0.ax',rule_055) ).
cnf(rule_056,axiom,
( ~ r0(a)
| ~ l0(a)
| n1(a,a,a) ),
file('SYN001-0.ax',rule_056) ).
cnf(rule_057,axiom,
( ~ r0(D)
| n1(D,D,D) ),
file('SYN001-0.ax',rule_057) ).
cnf(rule_058,axiom,
( ~ n0(C,B)
| ~ l1(C,B)
| n1(B,B,B) ),
file('SYN001-0.ax',rule_058) ).
cnf(rule_059,axiom,
( ~ m0(I,J,H)
| ~ m0(J,A,A)
| n1(H,H,I) ),
file('SYN001-0.ax',rule_059) ).
cnf(rule_060,axiom,
( ~ k0(b)
| ~ m1(d,e,e)
| ~ q0(b,e)
| n1(d,d,b) ),
file('SYN001-0.ax',rule_060) ).
cnf(rule_061,axiom,
( ~ s0(G)
| ~ k0(G)
| n1(G,G,G) ),
file('SYN001-0.ax',rule_061) ).
cnf(rule_062,axiom,
( ~ n1(E,D,E)
| ~ m0(E,E,F)
| n1(D,D,D) ),
file('SYN001-0.ax',rule_062) ).
cnf(rule_063,axiom,
( ~ k0(E)
| ~ n0(d,D)
| p1(D,D,E) ),
file('SYN001-0.ax',rule_063) ).
cnf(rule_064,axiom,
( ~ l0(A)
| ~ m0(B,C,b)
| p1(A,A,A) ),
file('SYN001-0.ax',rule_064) ).
cnf(rule_065,axiom,
( ~ n0(J,J)
| ~ p0(I,J)
| ~ l1(J,J)
| p1(I,I,I) ),
file('SYN001-0.ax',rule_065) ).
cnf(rule_066,axiom,
( ~ n0(H,G)
| p1(G,G,G) ),
file('SYN001-0.ax',rule_066) ).
cnf(rule_067,axiom,
( ~ q0(F,E)
| p1(E,E,E) ),
file('SYN001-0.ax',rule_067) ).
cnf(rule_068,axiom,
( ~ k0(D)
| p1(D,D,D) ),
file('SYN001-0.ax',rule_068) ).
cnf(rule_069,axiom,
( ~ p0(C,B)
| p1(B,B,C) ),
file('SYN001-0.ax',rule_069) ).
cnf(rule_070,axiom,
( ~ p0(a,c)
| p1(c,c,c) ),
file('SYN001-0.ax',rule_070) ).
cnf(rule_071,axiom,
( ~ s0(b)
| ~ p1(I,A,H)
| ~ l0(J)
| p1(H,I,H) ),
file('SYN001-0.ax',rule_071) ).
cnf(rule_072,axiom,
( ~ s0(F)
| ~ s0(G)
| p1(F,F,F) ),
file('SYN001-0.ax',rule_072) ).
cnf(rule_073,axiom,
( ~ k1(E)
| ~ k0(D)
| ~ k0(b)
| ~ n0(e,b)
| p1(D,D,D) ),
file('SYN001-0.ax',rule_073) ).
cnf(rule_074,axiom,
( ~ r0(B)
| ~ p0(C,B)
| p1(B,B,C) ),
file('SYN001-0.ax',rule_074) ).
cnf(rule_075,axiom,
( ~ p0(b,a)
| p1(a,a,a) ),
file('SYN001-0.ax',rule_075) ).
cnf(rule_076,axiom,
( ~ s0(d)
| ~ p1(b,b,b)
| p1(b,b,b) ),
file('SYN001-0.ax',rule_076) ).
cnf(rule_077,axiom,
( ~ m0(b,c,e)
| p1(c,e,b) ),
file('SYN001-0.ax',rule_077) ).
cnf(rule_078,axiom,
( ~ m0(e,a,a)
| ~ p0(d,b)
| p1(d,d,b) ),
file('SYN001-0.ax',rule_078) ).
cnf(rule_079,axiom,
( ~ l0(c)
| ~ k1(A)
| ~ k0(e)
| p1(A,A,A) ),
file('SYN001-0.ax',rule_079) ).
cnf(rule_080,axiom,
( ~ n1(H,J,G)
| ~ l0(I)
| ~ n0(H,H)
| p1(G,G,G) ),
file('SYN001-0.ax',rule_080) ).
cnf(rule_081,axiom,
( ~ l0(F)
| ~ q0(D,E)
| ~ m1(C,D,B)
| p1(B,B,B) ),
file('SYN001-0.ax',rule_081) ).
cnf(rule_082,axiom,
( ~ p1(J,H,A)
| ~ m0(J,H,A)
| p1(H,I,J) ),
file('SYN001-0.ax',rule_082) ).
cnf(rule_083,axiom,
( ~ k0(G)
| ~ m1(F,G,b)
| p1(F,b,G) ),
file('SYN001-0.ax',rule_083) ).
cnf(rule_084,axiom,
( ~ l1(D,b)
| ~ m0(b,E,b)
| p1(D,D,D) ),
file('SYN001-0.ax',rule_084) ).
cnf(rule_085,axiom,
( ~ p0(C,B)
| p1(B,B,B) ),
file('SYN001-0.ax',rule_085) ).
cnf(rule_086,axiom,
( ~ m0(J,A,I)
| ~ l0(I)
| p1(I,I,I) ),
file('SYN001-0.ax',rule_086) ).
cnf(rule_087,axiom,
( ~ p1(a,a,a)
| ~ r0(b)
| p1(a,b,a) ),
file('SYN001-0.ax',rule_087) ).
cnf(rule_088,axiom,
( ~ l0(a)
| p1(a,a,a) ),
file('SYN001-0.ax',rule_088) ).
cnf(rule_089,axiom,
( ~ n0(c,H)
| ~ r0(d)
| ~ n1(c,d,H)
| ~ s0(H)
| p1(d,d,H) ),
file('SYN001-0.ax',rule_089) ).
cnf(rule_090,axiom,
( ~ k0(e)
| ~ r0(e)
| p1(e,e,e) ),
file('SYN001-0.ax',rule_090) ).
cnf(rule_091,axiom,
( ~ n1(D,C,G)
| ~ k1(F)
| ~ q0(D,E)
| p1(C,C,C) ),
file('SYN001-0.ax',rule_091) ).
cnf(rule_092,axiom,
( ~ p0(C,J)
| ~ n0(B,A)
| q1(J,A,J) ),
file('SYN001-0.ax',rule_092) ).
cnf(rule_093,axiom,
( ~ q0(I,H)
| q1(H,H,H) ),
file('SYN001-0.ax',rule_093) ).
cnf(rule_094,axiom,
( ~ l0(c)
| ~ k0(b)
| ~ s0(e)
| q1(b,e,e) ),
file('SYN001-0.ax',rule_094) ).
cnf(rule_095,axiom,
( ~ p0(G,F)
| q1(F,G,G) ),
file('SYN001-0.ax',rule_095) ).
cnf(rule_096,axiom,
( ~ q1(E,C,D)
| ~ m1(B,D,C)
| ~ p0(C,E)
| ~ n1(C,D,D)
| q1(B,B,B) ),
file('SYN001-0.ax',rule_096) ).
cnf(rule_097,axiom,
( ~ s0(A)
| q1(A,A,A) ),
file('SYN001-0.ax',rule_097) ).
cnf(rule_098,axiom,
( ~ m0(I,I,J)
| ~ s0(H)
| q1(H,H,H) ),
file('SYN001-0.ax',rule_098) ).
cnf(rule_099,axiom,
( ~ q1(F,F,G)
| ~ l0(E)
| ~ k0(G)
| q1(E,F,F) ),
file('SYN001-0.ax',rule_099) ).
cnf(rule_100,axiom,
( ~ n0(D,C)
| q1(C,C,C) ),
file('SYN001-0.ax',rule_100) ).
cnf(rule_101,axiom,
( ~ p1(b,b,B)
| ~ q0(B,b)
| ~ k1(B)
| q1(B,B,B) ),
file('SYN001-0.ax',rule_101) ).
cnf(rule_102,axiom,
( ~ l0(A)
| ~ k0(J)
| q1(J,J,J) ),
file('SYN001-0.ax',rule_102) ).
cnf(rule_103,axiom,
( ~ m0(I,c,b)
| q1(I,I,I) ),
file('SYN001-0.ax',rule_103) ).
cnf(rule_104,axiom,
( ~ q0(F,F)
| ~ p0(H,E)
| ~ r0(G)
| ~ l0(E)
| q1(E,F,E) ),
file('SYN001-0.ax',rule_104) ).
cnf(rule_105,axiom,
( ~ p0(D,d)
| ~ s0(C)
| q1(C,C,D) ),
file('SYN001-0.ax',rule_105) ).
cnf(rule_106,axiom,
( ~ s0(B)
| q1(B,B,B) ),
file('SYN001-0.ax',rule_106) ).
cnf(rule_107,axiom,
( ~ m0(e,d,A)
| ~ m0(A,d,A)
| q1(e,A,A) ),
file('SYN001-0.ax',rule_107) ).
cnf(rule_108,axiom,
( ~ q0(b,b)
| ~ p1(H,b,b)
| ~ p0(I,J)
| q1(H,H,H) ),
file('SYN001-0.ax',rule_108) ).
cnf(rule_109,axiom,
( ~ k1(E)
| ~ q0(F,E)
| ~ p0(G,G)
| q1(E,E,F) ),
file('SYN001-0.ax',rule_109) ).
cnf(rule_110,axiom,
( ~ m0(C,D,B)
| q1(B,B,B) ),
file('SYN001-0.ax',rule_110) ).
cnf(rule_111,axiom,
( ~ m1(c,d,a)
| ~ m0(c,b,a)
| q1(d,d,c) ),
file('SYN001-0.ax',rule_111) ).
cnf(rule_112,axiom,
( ~ s0(b)
| ~ k1(A)
| q1(A,A,A) ),
file('SYN001-0.ax',rule_112) ).
cnf(rule_113,axiom,
( ~ m1(H,I,I)
| ~ r0(J)
| q1(H,H,I) ),
file('SYN001-0.ax',rule_113) ).
cnf(rule_114,axiom,
( ~ k0(G)
| ~ m0(F,F,G)
| q1(F,F,F) ),
file('SYN001-0.ax',rule_114) ).
cnf(rule_115,axiom,
( ~ l0(b)
| q1(b,b,b) ),
file('SYN001-0.ax',rule_115) ).
cnf(rule_116,axiom,
( ~ r0(E)
| q1(E,E,E) ),
file('SYN001-0.ax',rule_116) ).
cnf(rule_117,axiom,
( ~ s0(d)
| ~ k0(e)
| q1(d,d,d) ),
file('SYN001-0.ax',rule_117) ).
cnf(rule_118,axiom,
( ~ n1(D,d,C)
| ~ s0(b)
| ~ p0(b,d)
| q1(C,C,C) ),
file('SYN001-0.ax',rule_118) ).
cnf(rule_119,axiom,
( ~ s0(b)
| ~ s0(B)
| q1(B,b,b) ),
file('SYN001-0.ax',rule_119) ).
cnf(rule_120,axiom,
( ~ r0(b)
| q1(b,b,b) ),
file('SYN001-0.ax',rule_120) ).
cnf(rule_121,axiom,
( ~ m0(J,A,I)
| q1(I,I,I) ),
file('SYN001-0.ax',rule_121) ).
cnf(rule_122,axiom,
( ~ m0(G,H,G)
| q1(G,G,G) ),
file('SYN001-0.ax',rule_122) ).
cnf(rule_123,axiom,
( ~ r0(F)
| ~ m0(c,F,F)
| q1(F,F,F) ),
file('SYN001-0.ax',rule_123) ).
cnf(rule_124,axiom,
( ~ q1(d,E,d)
| ~ s0(d)
| ~ q0(D,E)
| r1(D) ),
file('SYN001-0.ax',rule_124) ).
cnf(rule_125,axiom,
( ~ p0(I,I)
| s1(I) ),
file('SYN001-0.ax',rule_125) ).
cnf(rule_126,axiom,
( ~ s1(H)
| ~ q0(F,G)
| s1(F) ),
file('SYN001-0.ax',rule_126) ).
cnf(rule_127,axiom,
( ~ k2(F,D)
| ~ k1(F)
| ~ m1(E,D,C)
| k2(C,D) ),
file('SYN001-0.ax',rule_127) ).
cnf(rule_128,axiom,
( ~ q1(B,B,d)
| ~ m1(B,e,B)
| ~ n1(e,d,B)
| k2(B,B) ),
file('SYN001-0.ax',rule_128) ).
cnf(rule_129,axiom,
( ~ q1(A,J,J)
| k2(J,J) ),
file('SYN001-0.ax',rule_129) ).
cnf(rule_130,axiom,
( ~ l1(e,e)
| k2(e,e) ),
file('SYN001-0.ax',rule_130) ).
cnf(rule_131,axiom,
( ~ l2(E,E)
| ~ n0(e,E)
| ~ s1(D)
| l2(D,E) ),
file('SYN001-0.ax',rule_131) ).
cnf(rule_132,axiom,
( ~ l1(e,e)
| ~ l2(c,c)
| l2(c,c) ),
file('SYN001-0.ax',rule_132) ).
cnf(rule_133,axiom,
( ~ m0(C,B,J)
| ~ s1(B)
| ~ p0(A,A)
| l2(J,J) ),
file('SYN001-0.ax',rule_133) ).
cnf(rule_134,axiom,
( ~ p0(H,G)
| ~ m1(I,H,H)
| ~ m0(H,G,I)
| l2(G,G) ),
file('SYN001-0.ax',rule_134) ).
cnf(rule_135,axiom,
( ~ l1(G,H)
| ~ s0(F)
| m2(F) ),
file('SYN001-0.ax',rule_135) ).
cnf(rule_136,axiom,
( ~ k1(b)
| m2(b) ),
file('SYN001-0.ax',rule_136) ).
cnf(rule_137,axiom,
( ~ p1(B,C,A)
| n2(A) ),
file('SYN001-0.ax',rule_137) ).
cnf(rule_138,axiom,
( ~ q1(c,a,d)
| ~ n1(e,a,e)
| ~ k1(c)
| ~ m1(b,a,e)
| n2(a) ),
file('SYN001-0.ax',rule_138) ).
cnf(rule_139,axiom,
( ~ k0(b)
| ~ l1(e,c)
| n2(c) ),
file('SYN001-0.ax',rule_139) ).
cnf(rule_140,axiom,
( ~ p1(b,I,J)
| ~ r0(e)
| ~ r1(b)
| n2(e) ),
file('SYN001-0.ax',rule_140) ).
cnf(rule_141,axiom,
( ~ q1(B,a,B)
| p2(B,a,B) ),
file('SYN001-0.ax',rule_141) ).
cnf(rule_142,axiom,
( ~ k2(J,a)
| ~ l2(a,A)
| ~ k0(A)
| ~ k1(A)
| p2(J,J,J) ),
file('SYN001-0.ax',rule_142) ).
cnf(rule_143,axiom,
( ~ q1(e,e,e)
| ~ l1(c,b)
| p2(c,e,e) ),
file('SYN001-0.ax',rule_143) ).
cnf(rule_144,axiom,
( ~ k2(c,a)
| ~ p0(b,I)
| ~ n1(c,I,I)
| ~ r0(e)
| p2(b,c,a) ),
file('SYN001-0.ax',rule_144) ).
cnf(rule_145,axiom,
( ~ p1(G,H,e)
| ~ r0(e)
| p2(e,G,H) ),
file('SYN001-0.ax',rule_145) ).
cnf(rule_146,axiom,
( ~ p2(C,D,C)
| ~ l1(E,F)
| ~ p1(C,E,F)
| p2(C,D,D) ),
file('SYN001-0.ax',rule_146) ).
cnf(rule_147,axiom,
( ~ l1(e,c)
| ~ r1(d)
| p2(e,c,c) ),
file('SYN001-0.ax',rule_147) ).
cnf(rule_148,axiom,
( ~ p2(A,J,A)
| ~ m1(A,B,J)
| p2(J,J,J) ),
file('SYN001-0.ax',rule_148) ).
cnf(rule_149,axiom,
( ~ m0(I,H,d)
| ~ r1(a)
| p2(H,H,d) ),
file('SYN001-0.ax',rule_149) ).
cnf(rule_150,axiom,
( ~ m1(G,G,F)
| p2(F,F,F) ),
file('SYN001-0.ax',rule_150) ).
cnf(rule_151,axiom,
( ~ s0(d)
| ~ k1(d)
| p2(d,d,d) ),
file('SYN001-0.ax',rule_151) ).
cnf(rule_152,axiom,
( ~ p2(C,D,C)
| ~ p0(C,D)
| ~ n1(E,D,E)
| p2(C,D,D) ),
file('SYN001-0.ax',rule_152) ).
cnf(rule_153,axiom,
( ~ n1(d,d,B)
| p2(B,B,B) ),
file('SYN001-0.ax',rule_153) ).
cnf(rule_154,axiom,
( ~ q1(A,A,A)
| p2(A,A,A) ),
file('SYN001-0.ax',rule_154) ).
cnf(rule_155,axiom,
( ~ p2(e,H,I)
| ~ k1(J)
| p2(H,I,I) ),
file('SYN001-0.ax',rule_155) ).
cnf(rule_156,axiom,
( ~ q1(a,G,F)
| ~ n1(e,F,a)
| p2(F,e,G) ),
file('SYN001-0.ax',rule_156) ).
cnf(rule_157,axiom,
( ~ l1(E,d)
| p2(E,E,E) ),
file('SYN001-0.ax',rule_157) ).
cnf(rule_158,axiom,
( ~ p2(B,D,B)
| ~ s0(e)
| ~ s1(c)
| ~ q1(c,B,D)
| p2(B,B,C) ),
file('SYN001-0.ax',rule_158) ).
cnf(rule_159,axiom,
( ~ k1(A)
| p2(A,A,A) ),
file('SYN001-0.ax',rule_159) ).
cnf(rule_160,axiom,
( ~ p2(a,J,H)
| ~ m1(a,a,I)
| p2(H,H,H) ),
file('SYN001-0.ax',rule_160) ).
cnf(rule_161,axiom,
( ~ p1(d,b,e)
| p2(d,b,b) ),
file('SYN001-0.ax',rule_161) ).
cnf(rule_162,axiom,
( ~ q1(e,c,G)
| ~ n1(e,e,G)
| ~ p1(G,b,b)
| p2(b,c,c) ),
file('SYN001-0.ax',rule_162) ).
cnf(rule_163,axiom,
( ~ k2(E,c)
| ~ q1(F,c,F)
| p2(E,E,E) ),
file('SYN001-0.ax',rule_163) ).
cnf(rule_164,axiom,
( ~ p2(D,C,B)
| ~ r1(C)
| ~ p0(B,B)
| p2(B,B,B) ),
file('SYN001-0.ax',rule_164) ).
cnf(rule_165,axiom,
( ~ p2(J,J,A)
| ~ q1(J,A,J)
| p2(I,I,I) ),
file('SYN001-0.ax',rule_165) ).
cnf(rule_166,axiom,
( ~ m1(a,H,d)
| ~ n0(H,d)
| p2(a,H,d) ),
file('SYN001-0.ax',rule_166) ).
cnf(rule_167,axiom,
( ~ k1(G)
| ~ s1(G)
| p2(G,G,G) ),
file('SYN001-0.ax',rule_167) ).
cnf(rule_168,axiom,
( ~ m1(d,a,c)
| ~ r1(e)
| ~ l2(e,b)
| ~ l1(e,c)
| p2(a,c,b) ),
file('SYN001-0.ax',rule_168) ).
cnf(rule_169,axiom,
( ~ p1(D,F,D)
| ~ q1(E,E,E)
| p2(D,D,D) ),
file('SYN001-0.ax',rule_169) ).
cnf(rule_170,axiom,
( ~ n1(C,e,e)
| p2(C,e,C) ),
file('SYN001-0.ax',rule_170) ).
cnf(rule_171,axiom,
( ~ p0(A,A)
| ~ n1(B,B,B)
| p2(A,A,A) ),
file('SYN001-0.ax',rule_171) ).
cnf(rule_172,axiom,
( ~ p1(e,e,a)
| p2(a,a,a) ),
file('SYN001-0.ax',rule_172) ).
cnf(rule_173,axiom,
( ~ r0(I)
| ~ r1(J)
| p2(I,I,I) ),
file('SYN001-0.ax',rule_173) ).
cnf(rule_174,axiom,
( ~ k1(e)
| ~ n2(H)
| p2(H,H,H) ),
file('SYN001-0.ax',rule_174) ).
cnf(rule_175,axiom,
( ~ l1(G,F)
| p2(F,F,F) ),
file('SYN001-0.ax',rule_175) ).
cnf(rule_176,axiom,
( ~ m1(E,D,E)
| p2(D,E,D) ),
file('SYN001-0.ax',rule_176) ).
cnf(rule_177,axiom,
( ~ p1(E,E,E)
| ~ k0(F)
| q2(E,F,F) ),
file('SYN001-0.ax',rule_177) ).
cnf(rule_178,axiom,
( ~ n1(C,B,D)
| ~ q0(C,B)
| q2(B,B,B) ),
file('SYN001-0.ax',rule_178) ).
cnf(rule_179,axiom,
( ~ n1(J,J,A)
| ~ k1(A)
| q2(J,J,J) ),
file('SYN001-0.ax',rule_179) ).
cnf(rule_180,axiom,
( ~ q0(e,c)
| ~ s1(c)
| ~ q2(d,c,a)
| q2(d,a,a) ),
file('SYN001-0.ax',rule_180) ).
cnf(rule_181,axiom,
( ~ p1(I,I,I)
| q2(I,I,I) ),
file('SYN001-0.ax',rule_181) ).
cnf(rule_182,axiom,
( ~ q2(G,H,F)
| ~ n1(G,F,H)
| ~ p1(F,F,H)
| q2(F,G,F) ),
file('SYN001-0.ax',rule_182) ).
cnf(rule_183,axiom,
( ~ l2(E,D)
| ~ l0(c)
| ~ k1(E)
| q2(D,c,E) ),
file('SYN001-0.ax',rule_183) ).
cnf(rule_184,axiom,
( ~ q1(C,c,B)
| q2(B,B,B) ),
file('SYN001-0.ax',rule_184) ).
cnf(rule_185,axiom,
( ~ q2(A,A,J)
| ~ k1(I)
| ~ n1(J,d,A)
| q2(I,I,I) ),
file('SYN001-0.ax',rule_185) ).
cnf(rule_186,axiom,
( ~ l1(H,G)
| q2(G,G,H) ),
file('SYN001-0.ax',rule_186) ).
cnf(rule_187,axiom,
( ~ q2(D,D,D)
| ~ k0(D)
| ~ m0(E,F,C)
| ~ r1(D)
| q2(C,D,C) ),
file('SYN001-0.ax',rule_187) ).
cnf(rule_188,axiom,
( ~ l0(G)
| ~ r1(G)
| r2(G) ),
file('SYN001-0.ax',rule_188) ).
cnf(rule_189,axiom,
( ~ s1(b)
| ~ q2(b,H,b)
| s2(H) ),
file('SYN001-0.ax',rule_189) ).
cnf(rule_190,axiom,
( ~ s0(d)
| ~ s1(a)
| s2(d) ),
file('SYN001-0.ax',rule_190) ).
cnf(rule_191,axiom,
( ~ s1(d)
| ~ r1(d)
| s2(d) ),
file('SYN001-0.ax',rule_191) ).
cnf(rule_192,axiom,
( ~ n0(J,C)
| ~ p2(B,A,C)
| ~ s1(A)
| k3(J,A,J) ),
file('SYN001-0.ax',rule_192) ).
cnf(rule_193,axiom,
( ~ s2(I)
| ~ q2(d,I,d)
| ~ s1(H)
| k3(H,H,H) ),
file('SYN001-0.ax',rule_193) ).
cnf(rule_194,axiom,
( ~ k2(G,F)
| k3(F,F,G) ),
file('SYN001-0.ax',rule_194) ).
cnf(rule_195,axiom,
( ~ k2(c,e)
| ~ s2(e)
| k3(c,c,c) ),
file('SYN001-0.ax',rule_195) ).
cnf(rule_196,axiom,
( ~ m1(C,C,E)
| ~ p2(D,E,D)
| k3(C,C,C) ),
file('SYN001-0.ax',rule_196) ).
cnf(rule_197,axiom,
( ~ k1(A)
| ~ l2(B,b)
| k3(A,A,A) ),
file('SYN001-0.ax',rule_197) ).
cnf(rule_198,axiom,
( ~ r2(c)
| ~ k0(a)
| k3(c,c,c) ),
file('SYN001-0.ax',rule_198) ).
cnf(rule_199,axiom,
( ~ k3(I,J,J)
| ~ l1(J,I)
| k3(I,J,J) ),
file('SYN001-0.ax',rule_199) ).
cnf(rule_200,axiom,
( ~ k3(F,G,G)
| ~ s1(G)
| ~ p2(G,H,e)
| k3(F,F,F) ),
file('SYN001-0.ax',rule_200) ).
cnf(rule_201,axiom,
( ~ m2(D)
| ~ m2(E)
| ~ p1(C,D,B)
| k3(B,B,C) ),
file('SYN001-0.ax',rule_201) ).
cnf(rule_202,axiom,
( ~ k3(H,A,J)
| ~ k2(G,J)
| ~ q0(I,H)
| k3(G,G,H) ),
file('SYN001-0.ax',rule_202) ).
cnf(rule_203,axiom,
( ~ l2(e,b)
| ~ r2(a)
| ~ p1(a,d,b)
| k3(d,d,d) ),
file('SYN001-0.ax',rule_203) ).
cnf(rule_204,axiom,
( ~ r2(a)
| k3(a,a,a) ),
file('SYN001-0.ax',rule_204) ).
cnf(rule_205,axiom,
( ~ p2(F,E,E)
| k3(E,E,E) ),
file('SYN001-0.ax',rule_205) ).
cnf(rule_206,axiom,
( ~ p2(D,C,C)
| k3(C,D,C) ),
file('SYN001-0.ax',rule_206) ).
cnf(rule_207,axiom,
( ~ k3(A,J,B)
| ~ k3(J,J,J)
| ~ p0(A,J)
| k3(J,J,J) ),
file('SYN001-0.ax',rule_207) ).
cnf(rule_208,axiom,
( ~ l1(b,I)
| ~ r2(c)
| k3(I,I,I) ),
file('SYN001-0.ax',rule_208) ).
cnf(rule_209,axiom,
( ~ k3(G,H,G)
| ~ s2(E)
| ~ l1(G,H)
| ~ m2(F)
| k3(E,E,E) ),
file('SYN001-0.ax',rule_209) ).
cnf(rule_210,axiom,
( ~ n2(D)
| k3(D,D,D) ),
file('SYN001-0.ax',rule_210) ).
cnf(rule_211,axiom,
( ~ r0(e)
| ~ r2(e)
| ~ l0(C)
| k3(C,C,C) ),
file('SYN001-0.ax',rule_211) ).
cnf(rule_212,axiom,
( ~ m2(B)
| k3(B,B,B) ),
file('SYN001-0.ax',rule_212) ).
cnf(rule_213,axiom,
( ~ p2(J,A,A)
| ~ r1(I)
| k3(I,I,I) ),
file('SYN001-0.ax',rule_213) ).
cnf(rule_214,axiom,
( ~ r2(c)
| k3(c,c,c) ),
file('SYN001-0.ax',rule_214) ).
cnf(rule_215,axiom,
( ~ p2(G,H,G)
| ~ r0(G)
| l3(G,H) ),
file('SYN001-0.ax',rule_215) ).
cnf(rule_216,axiom,
( ~ p2(E,F,D)
| ~ p1(D,D,E)
| l3(D,D) ),
file('SYN001-0.ax',rule_216) ).
cnf(rule_217,axiom,
( ~ m2(b)
| ~ n2(C)
| l3(C,C) ),
file('SYN001-0.ax',rule_217) ).
cnf(rule_218,axiom,
( ~ r2(B)
| l3(B,B) ),
file('SYN001-0.ax',rule_218) ).
cnf(rule_219,axiom,
( ~ l3(A,A)
| ~ l1(A,I)
| ~ n2(J)
| l3(I,I) ),
file('SYN001-0.ax',rule_219) ).
cnf(rule_220,axiom,
( ~ l1(G,G)
| ~ s2(H)
| l3(G,G) ),
file('SYN001-0.ax',rule_220) ).
cnf(rule_221,axiom,
( ~ k2(a,d)
| l3(d,d) ),
file('SYN001-0.ax',rule_221) ).
cnf(rule_222,axiom,
( ~ l2(F,F)
| ~ k3(E,D,D)
| l3(D,D) ),
file('SYN001-0.ax',rule_222) ).
cnf(rule_223,axiom,
( ~ k2(b,c)
| l3(c,c) ),
file('SYN001-0.ax',rule_223) ).
cnf(rule_224,axiom,
( ~ r0(b)
| ~ k3(a,c,a)
| ~ s2(d)
| l3(d,c) ),
file('SYN001-0.ax',rule_224) ).
cnf(rule_225,axiom,
( ~ s2(B)
| ~ m0(J,C,C)
| ~ l2(C,J)
| ~ m0(B,B,A)
| m3(J,A,J) ),
file('SYN001-0.ax',rule_225) ).
cnf(rule_226,axiom,
( ~ l2(a,a)
| ~ n0(I,a)
| ~ m3(G,I,G)
| ~ k2(H,I)
| m3(G,G,G) ),
file('SYN001-0.ax',rule_226) ).
cnf(rule_227,axiom,
( ~ r2(C)
| ~ s2(E)
| ~ s0(F)
| ~ q0(D,E)
| m3(C,C,C) ),
file('SYN001-0.ax',rule_227) ).
cnf(rule_228,axiom,
( ~ m3(B,J,B)
| ~ m2(A)
| ~ n2(J)
| m3(J,A,A) ),
file('SYN001-0.ax',rule_228) ).
cnf(rule_229,axiom,
( ~ q2(a,b,a)
| m3(b,b,b) ),
file('SYN001-0.ax',rule_229) ).
cnf(rule_230,axiom,
( ~ q2(b,c,d)
| ~ m2(d)
| ~ l1(d,b)
| m3(c,b,d) ),
file('SYN001-0.ax',rule_230) ).
cnf(rule_231,axiom,
( ~ k2(c,I)
| ~ r2(H)
| m3(H,I,H) ),
file('SYN001-0.ax',rule_231) ).
cnf(rule_232,axiom,
( ~ n2(G)
| ~ l2(G,G)
| m3(G,G,G) ),
file('SYN001-0.ax',rule_232) ).
cnf(rule_233,axiom,
( ~ m2(F)
| ~ n2(E)
| m3(E,E,E) ),
file('SYN001-0.ax',rule_233) ).
cnf(rule_234,axiom,
( ~ p2(D,e,e)
| ~ n2(e)
| m3(D,e,e) ),
file('SYN001-0.ax',rule_234) ).
cnf(rule_235,axiom,
( ~ k3(B,C,B)
| ~ r2(C)
| m3(B,B,C) ),
file('SYN001-0.ax',rule_235) ).
cnf(rule_236,axiom,
( ~ n2(A)
| m3(A,A,A) ),
file('SYN001-0.ax',rule_236) ).
cnf(rule_237,axiom,
( ~ q2(J,c,c)
| ~ s2(c)
| m3(J,c,J) ),
file('SYN001-0.ax',rule_237) ).
cnf(rule_238,axiom,
( ~ p2(I,I,I)
| m3(I,I,I) ),
file('SYN001-0.ax',rule_238) ).
cnf(rule_239,axiom,
( ~ l2(a,b)
| m3(b,b,b) ),
file('SYN001-0.ax',rule_239) ).
cnf(rule_240,axiom,
( ~ p2(E,F,D)
| n3(D) ),
file('SYN001-0.ax',rule_240) ).
cnf(rule_241,axiom,
( ~ k2(D,E)
| ~ q2(F,d,C)
| p3(C,D,E) ),
file('SYN001-0.ax',rule_241) ).
cnf(rule_242,axiom,
( ~ k3(A,B,J)
| ~ r2(A)
| p3(J,A,B) ),
file('SYN001-0.ax',rule_242) ).
cnf(rule_243,axiom,
( ~ q2(I,d,I)
| ~ n3(I)
| ~ p2(d,b,c)
| ~ l3(b,e)
| p3(I,d,e) ),
file('SYN001-0.ax',rule_243) ).
cnf(rule_244,axiom,
( ~ n2(H)
| p3(H,H,H) ),
file('SYN001-0.ax',rule_244) ).
cnf(rule_245,axiom,
( ~ p3(G,G,F)
| ~ l3(F,E)
| ~ l1(F,F)
| p3(E,E,E) ),
file('SYN001-0.ax',rule_245) ).
cnf(rule_246,axiom,
( ~ l2(D,D)
| p3(D,D,D) ),
file('SYN001-0.ax',rule_246) ).
cnf(rule_247,axiom,
( ~ s1(B)
| ~ q2(B,C,A)
| ~ n2(A)
| p3(A,A,A) ),
file('SYN001-0.ax',rule_247) ).
cnf(rule_248,axiom,
( ~ n3(I)
| ~ p2(J,I,I)
| p3(I,I,I) ),
file('SYN001-0.ax',rule_248) ).
cnf(rule_249,axiom,
( ~ n2(H)
| ~ k1(H)
| p3(H,H,H) ),
file('SYN001-0.ax',rule_249) ).
cnf(rule_250,axiom,
( ~ q2(F,G,E)
| ~ k1(E)
| p3(E,E,E) ),
file('SYN001-0.ax',rule_250) ).
cnf(rule_251,axiom,
( ~ p2(A,B,D)
| ~ m3(B,C,D)
| p3(A,B,B) ),
file('SYN001-0.ax',rule_251) ).
cnf(rule_252,axiom,
( ~ k2(J,J)
| ~ q0(I,H)
| p3(H,H,H) ),
file('SYN001-0.ax',rule_252) ).
cnf(rule_253,axiom,
( ~ k2(c,b)
| p3(b,c,b) ),
file('SYN001-0.ax',rule_253) ).
cnf(rule_254,axiom,
( ~ q2(G,G,b)
| ~ m3(e,G,e)
| p3(e,b,e) ),
file('SYN001-0.ax',rule_254) ).
cnf(rule_255,axiom,
( ~ n0(I,G)
| ~ q2(I,G,H)
| q3(G,H) ),
file('SYN001-0.ax',rule_255) ).
cnf(rule_256,axiom,
( ~ q3(F,E)
| ~ p2(F,E,E)
| q3(E,E) ),
file('SYN001-0.ax',rule_256) ).
cnf(rule_257,axiom,
( ~ q3(C,B)
| ~ s2(B)
| ~ n1(D,B,C)
| q3(B,C) ),
file('SYN001-0.ax',rule_257) ).
cnf(rule_258,axiom,
( ~ l2(A,A)
| ~ s1(J)
| ~ r2(I)
| q3(I,I) ),
file('SYN001-0.ax',rule_258) ).
cnf(rule_259,axiom,
( ~ q3(H,G)
| ~ r2(d)
| ~ k1(G)
| ~ m0(H,d,H)
| q3(G,G) ),
file('SYN001-0.ax',rule_259) ).
cnf(rule_260,axiom,
( ~ l2(c,G)
| ~ s2(H)
| r3(G,H,H) ),
file('SYN001-0.ax',rule_260) ).
cnf(rule_261,axiom,
( ~ r2(D)
| ~ n1(F,F,F)
| ~ l1(E,F)
| r3(D,D,D) ),
file('SYN001-0.ax',rule_261) ).
cnf(rule_262,axiom,
( ~ r3(A,B,A)
| ~ l2(C,B)
| ~ p1(B,C,A)
| r3(A,A,A) ),
file('SYN001-0.ax',rule_262) ).
cnf(rule_263,axiom,
( ~ r3(I,I,J)
| ~ m0(d,J,I)
| r3(I,I,I) ),
file('SYN001-0.ax',rule_263) ).
cnf(rule_264,axiom,
( ~ s2(H)
| r3(H,H,H) ),
file('SYN001-0.ax',rule_264) ).
cnf(rule_265,axiom,
( ~ l2(G,F)
| r3(F,F,F) ),
file('SYN001-0.ax',rule_265) ).
cnf(rule_266,axiom,
( ~ r2(E)
| r3(E,E,E) ),
file('SYN001-0.ax',rule_266) ).
cnf(rule_267,axiom,
( ~ p2(B,D,C)
| r3(B,C,B) ),
file('SYN001-0.ax',rule_267) ).
cnf(rule_268,axiom,
( ~ r3(I,A,A)
| ~ m3(J,b,H)
| ~ m2(I)
| r3(H,H,I) ),
file('SYN001-0.ax',rule_268) ).
cnf(rule_269,axiom,
( ~ m3(a,G,G)
| ~ m2(b)
| ~ q2(G,e,G)
| ~ k2(a,a)
| r3(a,a,e) ),
file('SYN001-0.ax',rule_269) ).
cnf(rule_270,axiom,
( ~ l2(F,F)
| ~ p2(b,F,b)
| ~ r0(F)
| r3(F,b,F) ),
file('SYN001-0.ax',rule_270) ).
cnf(rule_271,axiom,
( ~ r3(D,D,D)
| ~ p3(D,C,E)
| r3(C,C,C) ),
file('SYN001-0.ax',rule_271) ).
cnf(rule_272,axiom,
( ~ r3(B,J,J)
| ~ r2(B)
| ~ k2(A,B)
| r3(J,A,B) ),
file('SYN001-0.ax',rule_272) ).
cnf(rule_273,axiom,
( ~ m0(A,B,J)
| ~ s2(I)
| ~ q2(A,I,A)
| s3(I,J) ),
file('SYN001-0.ax',rule_273) ).
cnf(rule_274,axiom,
( ~ n3(e)
| ~ q3(e,b)
| ~ n0(c,d)
| k4(c) ),
file('SYN001-0.ax',rule_274) ).
cnf(rule_275,axiom,
( ~ k4(E)
| ~ n0(G,F)
| ~ k3(F,F,F)
| k4(E) ),
file('SYN001-0.ax',rule_275) ).
cnf(rule_276,axiom,
( ~ r3(C,e,D)
| ~ q1(a,a,D)
| ~ q3(C,C)
| k4(e) ),
file('SYN001-0.ax',rule_276) ).
cnf(rule_277,axiom,
( ~ p3(A,B,J)
| l4(J) ),
file('SYN001-0.ax',rule_277) ).
cnf(rule_278,axiom,
( ~ l4(I)
| ~ m0(I,H,H)
| l4(H) ),
file('SYN001-0.ax',rule_278) ).
cnf(rule_279,axiom,
( ~ s3(a,E)
| ~ l2(G,F)
| m4(E,F) ),
file('SYN001-0.ax',rule_279) ).
cnf(rule_280,axiom,
( ~ m4(C,C)
| ~ m3(C,C,D)
| ~ p3(D,D,D)
| m4(C,C) ),
file('SYN001-0.ax',rule_280) ).
cnf(rule_281,axiom,
( ~ n4(J,J)
| ~ p3(J,A,A)
| n4(J,A) ),
file('SYN001-0.ax',rule_281) ).
cnf(rule_282,axiom,
( ~ q1(d,d,d)
| ~ k3(c,c,e)
| n4(d,d) ),
file('SYN001-0.ax',rule_282) ).
cnf(rule_283,axiom,
( ~ p3(b,e,a)
| ~ l3(b,a)
| n4(e,e) ),
file('SYN001-0.ax',rule_283) ).
cnf(rule_284,axiom,
( ~ m3(H,H,H)
| ~ k4(I)
| n4(H,H) ),
file('SYN001-0.ax',rule_284) ).
cnf(rule_285,axiom,
( ~ r3(H,G,H)
| ~ r0(G)
| p4(G,G,H) ),
file('SYN001-0.ax',rule_285) ).
cnf(rule_286,axiom,
( ~ n3(D)
| ~ q3(E,F)
| p4(D,D,D) ),
file('SYN001-0.ax',rule_286) ).
cnf(rule_287,axiom,
( ~ k3(B,B,C)
| p4(B,C,B) ),
file('SYN001-0.ax',rule_287) ).
cnf(rule_288,axiom,
( ~ p4(J,J,A)
| ~ r3(I,I,H)
| p4(H,I,I) ),
file('SYN001-0.ax',rule_288) ).
cnf(rule_289,axiom,
( ~ p4(F,G,F)
| ~ n0(D,E)
| ~ l4(D)
| p4(D,D,D) ),
file('SYN001-0.ax',rule_289) ).
cnf(rule_290,axiom,
( ~ p4(A,C,A)
| ~ m3(B,C,A)
| p4(A,A,A) ),
file('SYN001-0.ax',rule_290) ).
cnf(rule_291,axiom,
( ~ p3(J,J,I)
| p4(I,I,I) ),
file('SYN001-0.ax',rule_291) ).
cnf(rule_292,axiom,
( ~ p1(H,G,F)
| ~ n4(F,H)
| ~ k3(G,H,H)
| p4(F,F,F) ),
file('SYN001-0.ax',rule_292) ).
cnf(rule_293,axiom,
( ~ l3(D,D)
| ~ n4(E,C)
| ~ q3(D,E)
| p4(C,C,C) ),
file('SYN001-0.ax',rule_293) ).
cnf(rule_294,axiom,
( ~ m3(B,c,a)
| ~ n3(a)
| p4(c,c,B) ),
file('SYN001-0.ax',rule_294) ).
cnf(rule_295,axiom,
( ~ m3(E,F,E)
| ~ q2(E,C,B)
| ~ k3(D,D,B)
| q4(B,C) ),
file('SYN001-0.ax',rule_295) ).
cnf(rule_296,axiom,
( ~ q4(J,A)
| ~ l4(J)
| ~ r1(I)
| q4(I,I) ),
file('SYN001-0.ax',rule_296) ).
cnf(rule_297,axiom,
( ~ l1(b,c)
| ~ k3(c,e,b)
| q4(b,b) ),
file('SYN001-0.ax',rule_297) ).
cnf(rule_298,axiom,
( ~ p0(J,G)
| ~ q3(H,I)
| ~ n3(G)
| r4(G) ),
file('SYN001-0.ax',rule_298) ).
cnf(rule_299,axiom,
( ~ l1(A,C)
| ~ p3(B,C,D)
| s4(A) ),
file('SYN001-0.ax',rule_299) ).
cnf(rule_300,axiom,
( ~ r3(G,E,E)
| ~ s4(F)
| k5(E) ),
file('SYN001-0.ax',rule_300) ).
cnf(rule_301,axiom,
( ~ n1(b,b,b)
| ~ s4(e)
| k5(b) ),
file('SYN001-0.ax',rule_301) ).
cnf(rule_302,axiom,
( ~ k1(H)
| ~ q4(I,I)
| l5(H) ),
file('SYN001-0.ax',rule_302) ).
cnf(rule_303,axiom,
( ~ p4(D,F,E)
| ~ r0(D)
| m5(D,E) ),
file('SYN001-0.ax',rule_303) ).
cnf(rule_304,axiom,
( ~ k4(C)
| m5(C,C) ),
file('SYN001-0.ax',rule_304) ).
cnf(rule_305,axiom,
( ~ m4(e,e)
| ~ s4(B)
| m5(B,B) ),
file('SYN001-0.ax',rule_305) ).
cnf(rule_306,axiom,
( ~ r0(J)
| ~ s4(A)
| m5(J,J) ),
file('SYN001-0.ax',rule_306) ).
cnf(rule_307,axiom,
( ~ n5(F,C)
| ~ p4(F,F,C)
| ~ n4(B,E)
| ~ q4(D,E)
| n5(B,C) ),
file('SYN001-0.ax',rule_307) ).
cnf(rule_308,axiom,
( ~ n5(A,J)
| ~ m0(A,J,A)
| n5(J,J) ),
file('SYN001-0.ax',rule_308) ).
cnf(rule_309,axiom,
( ~ n4(I,H)
| n5(H,H) ),
file('SYN001-0.ax',rule_309) ).
cnf(rule_310,axiom,
( ~ k5(d)
| ~ m4(G,G)
| ~ p0(E,F)
| n5(E,E) ),
file('SYN001-0.ax',rule_310) ).
cnf(rule_311,axiom,
( ~ p4(c,d,c)
| n5(d,d) ),
file('SYN001-0.ax',rule_311) ).
cnf(rule_312,axiom,
( ~ n4(b,e)
| ~ r3(d,b,c)
| n5(b,e) ),
file('SYN001-0.ax',rule_312) ).
cnf(rule_313,axiom,
( ~ q4(D,C)
| n5(C,C) ),
file('SYN001-0.ax',rule_313) ).
cnf(rule_314,axiom,
( ~ r4(B)
| n5(B,B) ),
file('SYN001-0.ax',rule_314) ).
cnf(rule_315,axiom,
( ~ k4(A)
| ~ s1(A)
| n5(A,A) ),
file('SYN001-0.ax',rule_315) ).
cnf(rule_316,axiom,
( ~ p4(b,b,J)
| ~ s1(H)
| ~ p4(I,H,H)
| n5(H,H) ),
file('SYN001-0.ax',rule_316) ).
cnf(rule_317,axiom,
( ~ n4(G,d)
| ~ k3(d,G,a)
| n5(d,G) ),
file('SYN001-0.ax',rule_317) ).
cnf(rule_318,axiom,
( ~ l2(E,E)
| ~ s4(F)
| p5(E,E,F) ),
file('SYN001-0.ax',rule_318) ).
cnf(rule_319,axiom,
( ~ m4(D,C)
| ~ p5(B,D,B)
| ~ l2(B,D)
| p5(B,C,C) ),
file('SYN001-0.ax',rule_319) ).
cnf(rule_320,axiom,
( ~ s1(I)
| ~ q4(J,A)
| p5(I,J,I) ),
file('SYN001-0.ax',rule_320) ).
cnf(rule_321,axiom,
( ~ k5(b)
| ~ p4(G,G,H)
| p5(b,b,b) ),
file('SYN001-0.ax',rule_321) ).
cnf(rule_322,axiom,
( ~ m2(A)
| ~ s4(J)
| q5(J,A) ),
file('SYN001-0.ax',rule_322) ).
cnf(rule_323,axiom,
( ~ r4(a)
| q5(a,a) ),
file('SYN001-0.ax',rule_323) ).
cnf(rule_324,axiom,
( ~ l4(I)
| q5(I,I) ),
file('SYN001-0.ax',rule_324) ).
cnf(rule_325,axiom,
( ~ q4(H,H)
| q5(H,H) ),
file('SYN001-0.ax',rule_325) ).
cnf(rule_326,axiom,
( ~ m4(G,G)
| q5(G,G) ),
file('SYN001-0.ax',rule_326) ).
cnf(rule_327,axiom,
( ~ n3(D)
| ~ k0(b)
| ~ s4(C)
| r5(C,D) ),
file('SYN001-0.ax',rule_327) ).
cnf(rule_328,axiom,
( ~ k4(B)
| r5(B,B) ),
file('SYN001-0.ax',rule_328) ).
cnf(rule_329,axiom,
( ~ r4(I)
| ~ l4(H)
| s5(H) ),
file('SYN001-0.ax',rule_329) ).
cnf(rule_330,axiom,
( ~ s5(G)
| ~ l5(G)
| ~ s3(E,F)
| ~ k4(E)
| s5(E) ),
file('SYN001-0.ax',rule_330) ).
cnf(prove_this,negated_conjecture,
~ m1(X,X,e),
file('theBenchmark.p',prove_this) ).
cnf(rule_048_true,plain,
$true,
inference(clause_is_true,[status(thm)],[rule_048]) ).
cnf(rule_076_true,plain,
$true,
inference(clause_is_true,[status(thm)],[rule_076]) ).
cnf(rule_132_true,plain,
$true,
inference(clause_is_true,[status(thm)],[rule_132]) ).
cnf(rule_199_true,plain,
$true,
inference(clause_is_true,[status(thm)],[rule_199]) ).
cnf(rule_207_true,plain,
$true,
inference(clause_is_true,[status(thm)],[rule_207]) ).
cnf(rule_275_true,plain,
$true,
inference(clause_is_true,[status(thm)],[rule_275]) ).
cnf(rule_280_true,plain,
$true,
inference(clause_is_true,[status(thm)],[rule_280]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN237-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.03 This is a CNF_UNS_EPR_NEQ_HRN problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/5.36 % Computer : n020.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.36 % WCLimit : 300
% 0.08/5.36 % DateTime : Sun Sep 20 06:28:53 UTC 2026
% 0.08/5.37 % CPUTime :
% 0.13/5.45 % SZS status Unsatisfiable for theBenchmark
% 0.13/5.45 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------