%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX189-1 : TPTP v9.3.0. Released v9.3.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 : n018.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:34:40 PM UTC 2026
% Result : Unsatisfiable 144.35s 98.78s
% Output : CNFRefutation 157.05s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_104)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_007,axiom,
fail1(n(X1),x(X2,X3)) = fail2(n(X1),x(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_007) ).
cnf(axiom_005,axiom,
fail2(X1,X2) = aux(X1,X2,eq2(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_005) ).
cnf(axiom_008,axiom,
fail1(n(X1),y(X2,X3)) = fail2(n(X1),y(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_008) ).
cnf(axiom_010,axiom,
fail1(x(X1,X2),X3) = fail2(x(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_010) ).
cnf(axiom_011,axiom,
fail1(y(X1,X2),X3) = fail2(y(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_011) ).
cnf(axiom_020,axiom,
fail32(n(X1),x(X2,X3)) = fail4(n(X1),x(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_020) ).
cnf(axiom_018,axiom,
fail4(X1,X2) = y(opt(X1),opt(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_018) ).
cnf(axiom_021,axiom,
fail32(n(X1),y(X2,X3)) = fail4(n(X1),y(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_021) ).
cnf(axiom_024,axiom,
fail32(x(X1,X2),X3) = fail4(x(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_024) ).
cnf(axiom_009,axiom,
fail1(n(X1),x2) = fail2(n(X1),x2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_009) ).
cnf(axiom_012,axiom,
fail1(x2,X1) = fail2(x2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_012) ).
cnf(axiom_085,axiom,
eq(s(X1),s(X2)) = eq(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_085) ).
cnf(axiom_068,axiom,
eq2(n(X1),n(X2)) = eq(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_068) ).
cnf(axiom_022,axiom,
fail32(n(X1),x2) = fail4(n(X1),x2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_022) ).
cnf(axiom_025,axiom,
fail32(x2,X1) = fail4(x2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_025) ).
cnf(axiom_086,axiom,
eq(s(X1),z) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_086) ).
cnf(axiom_087,axiom,
eq(z,s(X1)) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_087) ).
cnf(axiom_088,axiom,
eq(X1,X1) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_088) ).
cnf(axiom_065,axiom,
prop2(X1) = impl(eq2(opt(d(X1)),x(y(x2,x2),y(x2,x(x2,x2)))),eq3(btrue,bfalse)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_065) ).
cnf(axiom_001,axiom,
aux(x(X1,X2),X3,bfalse) = opt(x(X1,x(X2,X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_001) ).
cnf(axiom_003,axiom,
aux(y(X1,X2),X3,bfalse) = x(opt(y(X1,X2)),opt(X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_003) ).
cnf(axiom_055,axiom,
opt(x(x(X1,X2),X3)) = fail(x(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_055) ).
cnf(axiom_056,axiom,
opt(x(y(X1,X2),X3)) = fail(y(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_056) ).
cnf(axiom_060,axiom,
opt(y(x(X1,X2),X3)) = fail3(x(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_060) ).
cnf(axiom_061,axiom,
opt(y(y(X1,X2),X3)) = fail3(y(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_061) ).
cnf(axiom_023,axiom,
fail32(y(X1,X2),X3) = opt(y(X1,y(X2,X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_023) ).
cnf(axiom_047,axiom,
d(y(X1,X2)) = x(y(d(X1),X2),y(X1,d(X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_047) ).
cnf(axiom_032,axiom,
fail12(n(s(s(X1))),X2) = fail22(n(s(s(X1))),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_032) ).
cnf(axiom_026,axiom,
fail22(X1,n(s(s(X2)))) = fail32(X1,n(s(s(X2)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_026) ).
cnf(axiom,axiom,
aux(X1,X2,btrue) = y(n(s(s(z))),opt(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom) ).
cnf(axiom_070,axiom,
( eq2(x(X1,X3),x(X2,X4)) = eq2(X3,X4)
| eq2(X1,X2) != btrue ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_070) ).
cnf(axiom_072,axiom,
( eq2(y(X1,X3),y(X2,X4)) = eq2(X3,X4)
| eq2(X1,X2) != btrue ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_072) ).
cnf(axiom_053,axiom,
opt(x(n(s(X1)),X2)) = fail(n(s(X1)),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_053) ).
cnf(axiom_058,axiom,
opt(y(n(s(X1)),X2)) = fail3(n(s(X1)),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_058) ).
cnf(axiom_002,axiom,
aux(n(X1),X2,bfalse) = x(opt(n(X1)),opt(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_002) ).
cnf(axiom_069,axiom,
( eq2(x(X1,X3),x(X2,X4)) = bfalse
| eq2(X1,X2) != bfalse ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_069) ).
cnf(axiom_071,axiom,
( eq2(y(X1,X3),y(X2,X4)) = bfalse
| eq2(X1,X2) != bfalse ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_071) ).
cnf(axiom_035,axiom,
fail12(x(X1,X2),X3) = fail22(x(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_035) ).
cnf(axiom_036,axiom,
fail12(y(X1,X2),X3) = fail22(y(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_036) ).
cnf(axiom_040,axiom,
fail3(X1,x(X2,X3)) = fail12(X1,x(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_040) ).
cnf(axiom_041,axiom,
fail3(X1,y(X2,X3)) = fail12(X1,y(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_041) ).
cnf(axiom_029,axiom,
fail22(X1,x(X2,X3)) = fail32(X1,x(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_029) ).
cnf(axiom_030,axiom,
fail22(X1,y(X2,X3)) = fail32(X1,y(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_030) ).
cnf(axiom_015,axiom,
fail(X1,x(X2,X3)) = fail1(X1,x(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_015) ).
cnf(axiom_016,axiom,
fail(X1,y(X2,X3)) = fail1(X1,y(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_016) ).
cnf(axiom_004,axiom,
aux(x2,X1,bfalse) = x(opt(x2),opt(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_004) ).
cnf(axiom_077,axiom,
eq2(x(X1,X2),y(X3,X4)) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_077) ).
cnf(axiom_080,axiom,
eq2(y(X1,X2),x(X3,X4)) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_080) ).
cnf(axiom_038,axiom,
fail3(X1,n(s(X2))) = fail12(X1,n(s(X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_038) ).
cnf(axiom_013,axiom,
fail(X1,n(s(X2))) = fail1(X1,n(s(X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_013) ).
cnf(axiom_051,axiom,
mulNat(s(X1),X2) = addNat(X2,mulNat(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_051) ).
cnf(axiom_019,axiom,
fail32(n(X1),n(X2)) = n(mulNat(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_019) ).
cnf(axiom_006,axiom,
fail1(n(X1),n(X2)) = n(addNat(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_006) ).
cnf(axiom_046,axiom,
d(x(X1,X2)) = x(d(X1),d(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_046) ).
cnf(axiom_049,axiom,
addNat(s(X1),X2) = s(addNat(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_049) ).
cnf(axiom_076,axiom,
eq2(x(X1,X2),n(X3)) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_076) ).
cnf(axiom_079,axiom,
eq2(y(X1,X2),n(X3)) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_079) ).
cnf(axiom_073,axiom,
eq2(n(X1),x(X2,X3)) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_073) ).
cnf(axiom_074,axiom,
eq2(n(X1),y(X2,X3)) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_074) ).
cnf(axiom_057,axiom,
opt(x(x2,X1)) = fail(x2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_057) ).
cnf(axiom_062,axiom,
opt(y(x2,X1)) = fail3(x2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_062) ).
cnf(axiom_059,axiom,
opt(y(n(z),X1)) = n(z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_059) ).
cnf(axiom_078,axiom,
eq2(x(X1,X2),x2) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_078) ).
cnf(axiom_081,axiom,
eq2(y(X1,X2),x2) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_081) ).
cnf(axiom_083,axiom,
eq2(x2,x(X1,X2)) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_083) ).
cnf(axiom_084,axiom,
eq2(x2,y(X1,X2)) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_084) ).
cnf(axiom_054,axiom,
opt(x(n(z),X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_054) ).
cnf(axiom_034,axiom,
fail12(n(z),X1) = fail22(n(z),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_034) ).
cnf(axiom_028,axiom,
fail22(X1,n(z)) = fail32(X1,n(z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_028) ).
cnf(goal,negated_conjecture,
eq3(prop2(X1),bfalse) != btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
cnf(axiom_033,axiom,
fail12(n(s(z)),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_033) ).
cnf(axiom_027,axiom,
fail22(X1,n(s(z))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_027) ).
cnf(axiom_037,axiom,
fail12(x2,X1) = fail22(x2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_037) ).
cnf(axiom_042,axiom,
fail3(X1,x2) = fail12(X1,x2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_042) ).
cnf(axiom_031,axiom,
fail22(X1,x2) = fail32(X1,x2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_031) ).
cnf(axiom_017,axiom,
fail(X1,x2) = fail1(X1,x2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_017) ).
cnf(axiom_039,axiom,
fail3(X1,n(z)) = n(z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_039) ).
cnf(axiom_075,axiom,
eq2(n(X1),x2) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_075) ).
cnf(axiom_082,axiom,
eq2(x2,n(X1)) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_082) ).
cnf(axiom_014,axiom,
fail(X1,n(z)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_014) ).
cnf(axiom_063,axiom,
opt(n(X1)) = n(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_063) ).
cnf(axiom_090,axiom,
eq3(X1,X1) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_090) ).
cnf(axiom_089,axiom,
eq2(X1,X1) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_089) ).
cnf(axiom_043,axiom,
impl(btrue,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_043) ).
cnf(axiom_050,axiom,
addNat(z,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_050) ).
cnf(axiom_045,axiom,
d(n(X1)) = n(z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_045) ).
cnf(axiom_044,axiom,
impl(bfalse,X1) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_044) ).
cnf(axiom_052,axiom,
mulNat(z,X1) = z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_052) ).
cnf(axiom_066,axiom,
eq3(bfalse,btrue) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_066) ).
cnf(axiom_067,axiom,
eq3(btrue,bfalse) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_067) ).
cnf(axiom_048,axiom,
d(x2) = n(s(z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_048) ).
cnf(axiom_064,axiom,
opt(x2) = x2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_064) ).
cnf(i_0_92,axiom,
fail1(n(X1),x(X2,X3)) = fail2(n(X1),x(X2,X3)),
axiom_007 ).
cnf(i_0_93,axiom,
fail2(X1,X2) = aux(X1,X2,eq2(X1,X2)),
axiom_005 ).
cnf(i_0_94,axiom,
fail1(n(X1),y(X2,X3)) = fail2(n(X1),y(X2,X3)),
axiom_008 ).
cnf(i_0_95,axiom,
fail1(x(X1,X2),X3) = fail2(x(X1,X2),X3),
axiom_010 ).
cnf(i_0_96,axiom,
fail1(y(X1,X2),X3) = fail2(y(X1,X2),X3),
axiom_011 ).
cnf(i_0_97,axiom,
fail32(n(X1),x(X2,X3)) = fail4(n(X1),x(X2,X3)),
axiom_020 ).
cnf(i_0_98,axiom,
fail4(X1,X2) = y(opt(X1),opt(X2)),
axiom_018 ).
cnf(i_0_99,axiom,
fail32(n(X1),y(X2,X3)) = fail4(n(X1),y(X2,X3)),
axiom_021 ).
cnf(i_0_100,axiom,
fail32(x(X1,X2),X3) = fail4(x(X1,X2),X3),
axiom_024 ).
cnf(i_0_101,axiom,
fail1(n(X1),x2) = fail2(n(X1),x2),
axiom_009 ).
cnf(i_0_102,axiom,
fail1(x2,X1) = fail2(x2,X1),
axiom_012 ).
cnf(i_0_103,axiom,
eq(s(X1),s(X2)) = eq(X1,X2),
axiom_085 ).
cnf(i_0_104,axiom,
eq2(n(X1),n(X2)) = eq(X1,X2),
axiom_068 ).
cnf(i_0_105,axiom,
fail32(n(X1),x2) = fail4(n(X1),x2),
axiom_022 ).
cnf(i_0_106,axiom,
fail32(x2,X1) = fail4(x2,X1),
axiom_025 ).
cnf(i_0_107,axiom,
eq(s(X1),z) = bfalse,
axiom_086 ).
cnf(i_0_108,axiom,
eq(z,s(X1)) = bfalse,
axiom_087 ).
cnf(i_0_109,axiom,
eq(X1,X1) = btrue,
axiom_088 ).
cnf(i_0_110,axiom,
prop2(X1) = impl(eq2(opt(d(X1)),x(y(x2,x2),y(x2,x(x2,x2)))),eq3(btrue,bfalse)),
axiom_065,
[final] ).
cnf(i_0_111,plain,
fail1(n(X1),x(X2,X3)) = aux(n(X1),x(X2,X3),eq2(n(X1),x(X2,X3))),
inference(rw,[status(thm)],[i_0_92,c_0_93]),
[final] ).
cnf(i_0_112,plain,
fail1(n(X1),y(X2,X3)) = aux(n(X1),y(X2,X3),eq2(n(X1),y(X2,X3))),
inference(rw,[status(thm)],[i_0_94,c_0_93]),
[final] ).
cnf(i_0_113,plain,
fail1(x(X1,X2),X3) = aux(x(X1,X2),X3,eq2(x(X1,X2),X3)),
inference(rw,[status(thm)],[i_0_95,c_0_93]),
[final] ).
cnf(i_0_114,plain,
fail1(y(X1,X2),X3) = aux(y(X1,X2),X3,eq2(y(X1,X2),X3)),
inference(rw,[status(thm)],[i_0_96,c_0_93]),
[final] ).
cnf(i_0_115,axiom,
aux(x(X1,X2),X3,bfalse) = opt(x(X1,x(X2,X3))),
axiom_001,
[final] ).
cnf(i_0_116,axiom,
aux(y(X1,X2),X3,bfalse) = x(opt(y(X1,X2)),opt(X3)),
axiom_003,
[final] ).
cnf(i_0_117,plain,
fail32(n(X1),x(X2,X3)) = y(opt(n(X1)),opt(x(X2,X3))),
inference(rw,[status(thm)],[i_0_97,c_0_98]),
[final] ).
cnf(i_0_118,plain,
fail32(n(X1),y(X2,X3)) = y(opt(n(X1)),opt(y(X2,X3))),
inference(rw,[status(thm)],[i_0_99,c_0_98]),
[final] ).
cnf(i_0_119,axiom,
opt(x(x(X1,X2),X3)) = fail(x(X1,X2),X3),
axiom_055,
[final] ).
cnf(i_0_120,axiom,
opt(x(y(X1,X2),X3)) = fail(y(X1,X2),X3),
axiom_056,
[final] ).
cnf(i_0_121,axiom,
opt(y(x(X1,X2),X3)) = fail3(x(X1,X2),X3),
axiom_060,
[final] ).
cnf(i_0_122,axiom,
opt(y(y(X1,X2),X3)) = fail3(y(X1,X2),X3),
axiom_061,
[final] ).
cnf(i_0_123,axiom,
fail32(y(X1,X2),X3) = opt(y(X1,y(X2,X3))),
axiom_023,
[final] ).
cnf(i_0_124,axiom,
d(y(X1,X2)) = x(y(d(X1),X2),y(X1,d(X2))),
axiom_047,
[final] ).
cnf(i_0_125,plain,
fail32(x(X1,X2),X3) = y(opt(x(X1,X2)),opt(X3)),
inference(rw,[status(thm)],[i_0_100,c_0_98]),
[final] ).
cnf(i_0_126,axiom,
fail12(n(s(s(X1))),X2) = fail22(n(s(s(X1))),X2),
axiom_032,
[final] ).
cnf(i_0_127,axiom,
fail22(X1,n(s(s(X2)))) = fail32(X1,n(s(s(X2)))),
axiom_026,
[final] ).
cnf(i_0_128,plain,
fail1(n(X1),x2) = aux(n(X1),x2,eq2(n(X1),x2)),
inference(rw,[status(thm)],[i_0_101,c_0_93]),
[final] ).
cnf(i_0_129,axiom,
aux(X1,X2,btrue) = y(n(s(s(z))),opt(X1)),
axiom,
[final] ).
cnf(i_0_130,axiom,
( eq2(x(X1,X3),x(X2,X4)) = eq2(X3,X4)
| eq2(X1,X2) != btrue ),
axiom_070,
[final] ).
cnf(i_0_131,axiom,
( eq2(y(X1,X3),y(X2,X4)) = eq2(X3,X4)
| eq2(X1,X2) != btrue ),
axiom_072,
[final] ).
cnf(i_0_132,axiom,
opt(x(n(s(X1)),X2)) = fail(n(s(X1)),X2),
axiom_053,
[final] ).
cnf(i_0_133,axiom,
opt(y(n(s(X1)),X2)) = fail3(n(s(X1)),X2),
axiom_058,
[final] ).
cnf(i_0_134,axiom,
aux(n(X1),X2,bfalse) = x(opt(n(X1)),opt(X2)),
axiom_002,
[final] ).
cnf(i_0_135,axiom,
( eq2(x(X1,X3),x(X2,X4)) = bfalse
| eq2(X1,X2) != bfalse ),
axiom_069,
[final] ).
cnf(i_0_136,axiom,
( eq2(y(X1,X3),y(X2,X4)) = bfalse
| eq2(X1,X2) != bfalse ),
axiom_071,
[final] ).
cnf(i_0_137,plain,
fail1(x2,X1) = aux(x2,X1,eq2(x2,X1)),
inference(rw,[status(thm)],[i_0_102,c_0_93]),
[final] ).
cnf(i_0_138,axiom,
fail12(x(X1,X2),X3) = fail22(x(X1,X2),X3),
axiom_035,
[final] ).
cnf(i_0_139,axiom,
fail12(y(X1,X2),X3) = fail22(y(X1,X2),X3),
axiom_036,
[final] ).
cnf(i_0_140,axiom,
fail3(X1,x(X2,X3)) = fail12(X1,x(X2,X3)),
axiom_040,
[final] ).
cnf(i_0_141,axiom,
fail3(X1,y(X2,X3)) = fail12(X1,y(X2,X3)),
axiom_041,
[final] ).
cnf(i_0_142,axiom,
fail22(X1,x(X2,X3)) = fail32(X1,x(X2,X3)),
axiom_029,
[final] ).
cnf(i_0_143,axiom,
fail22(X1,y(X2,X3)) = fail32(X1,y(X2,X3)),
axiom_030,
[final] ).
cnf(i_0_144,axiom,
fail(X1,x(X2,X3)) = fail1(X1,x(X2,X3)),
axiom_015,
[final] ).
cnf(i_0_145,axiom,
fail(X1,y(X2,X3)) = fail1(X1,y(X2,X3)),
axiom_016,
[final] ).
cnf(i_0_146,plain,
eq2(n(s(X1)),n(s(X2))) = eq2(n(X1),n(X2)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_103,c_0_104]),c_0_104]),
[final] ).
cnf(i_0_147,axiom,
aux(x2,X1,bfalse) = x(opt(x2),opt(X1)),
axiom_004,
[final] ).
cnf(i_0_148,axiom,
eq2(x(X1,X2),y(X3,X4)) = bfalse,
axiom_077,
[final] ).
cnf(i_0_149,axiom,
eq2(y(X1,X2),x(X3,X4)) = bfalse,
axiom_080,
[final] ).
cnf(i_0_150,axiom,
fail3(X1,n(s(X2))) = fail12(X1,n(s(X2))),
axiom_038,
[final] ).
cnf(i_0_151,axiom,
fail(X1,n(s(X2))) = fail1(X1,n(s(X2))),
axiom_013,
[final] ).
cnf(i_0_152,axiom,
mulNat(s(X1),X2) = addNat(X2,mulNat(X1,X2)),
axiom_051,
[final] ).
cnf(i_0_153,axiom,
fail32(n(X1),n(X2)) = n(mulNat(X1,X2)),
axiom_019,
[final] ).
cnf(i_0_154,axiom,
fail1(n(X1),n(X2)) = n(addNat(X1,X2)),
axiom_006,
[final] ).
cnf(i_0_155,axiom,
d(x(X1,X2)) = x(d(X1),d(X2)),
axiom_046,
[final] ).
cnf(i_0_156,plain,
fail32(n(X1),x2) = y(opt(n(X1)),opt(x2)),
inference(rw,[status(thm)],[i_0_105,c_0_98]),
[final] ).
cnf(i_0_157,axiom,
addNat(s(X1),X2) = s(addNat(X1,X2)),
axiom_049,
[final] ).
cnf(i_0_158,axiom,
eq2(x(X1,X2),n(X3)) = bfalse,
axiom_076,
[final] ).
cnf(i_0_159,axiom,
eq2(y(X1,X2),n(X3)) = bfalse,
axiom_079,
[final] ).
cnf(i_0_160,axiom,
eq2(n(X1),x(X2,X3)) = bfalse,
axiom_073,
[final] ).
cnf(i_0_161,axiom,
eq2(n(X1),y(X2,X3)) = bfalse,
axiom_074,
[final] ).
cnf(i_0_162,axiom,
opt(x(x2,X1)) = fail(x2,X1),
axiom_057,
[final] ).
cnf(i_0_163,axiom,
opt(y(x2,X1)) = fail3(x2,X1),
axiom_062,
[final] ).
cnf(i_0_164,axiom,
opt(y(n(z),X1)) = n(z),
axiom_059,
[final] ).
cnf(i_0_165,axiom,
eq2(x(X1,X2),x2) = bfalse,
axiom_078,
[final] ).
cnf(i_0_166,axiom,
eq2(y(X1,X2),x2) = bfalse,
axiom_081,
[final] ).
cnf(i_0_167,axiom,
eq2(x2,x(X1,X2)) = bfalse,
axiom_083,
[final] ).
cnf(i_0_168,axiom,
eq2(x2,y(X1,X2)) = bfalse,
axiom_084,
[final] ).
cnf(i_0_169,axiom,
opt(x(n(z),X1)) = X1,
axiom_054,
[final] ).
cnf(i_0_170,plain,
fail32(x2,X1) = y(opt(x2),opt(X1)),
inference(rw,[status(thm)],[i_0_106,c_0_98]),
[final] ).
cnf(i_0_171,plain,
eq2(n(s(X1)),n(z)) = bfalse,
inference(rw,[status(thm)],[i_0_107,c_0_104]),
[final] ).
cnf(i_0_172,plain,
eq2(n(z),n(s(X1))) = bfalse,
inference(rw,[status(thm)],[i_0_108,c_0_104]),
[final] ).
cnf(i_0_173,axiom,
fail12(n(z),X1) = fail22(n(z),X1),
axiom_034,
[final] ).
cnf(i_0_174,axiom,
fail22(X1,n(z)) = fail32(X1,n(z)),
axiom_028,
[final] ).
cnf(i_0_175,negated_conjecture,
eq3(prop2(X1),bfalse) != btrue,
goal,
[final] ).
cnf(i_0_176,axiom,
fail12(n(s(z)),X1) = X1,
axiom_033,
[final] ).
cnf(i_0_177,axiom,
fail22(X1,n(s(z))) = X1,
axiom_027,
[final] ).
cnf(i_0_178,plain,
eq2(n(X1),n(X1)) = btrue,
inference(rw,[status(thm)],[i_0_109,c_0_104]),
[final] ).
cnf(i_0_179,axiom,
fail12(x2,X1) = fail22(x2,X1),
axiom_037,
[final] ).
cnf(i_0_180,axiom,
fail3(X1,x2) = fail12(X1,x2),
axiom_042,
[final] ).
cnf(i_0_181,axiom,
fail22(X1,x2) = fail32(X1,x2),
axiom_031,
[final] ).
cnf(i_0_182,axiom,
fail(X1,x2) = fail1(X1,x2),
axiom_017,
[final] ).
cnf(i_0_183,axiom,
fail3(X1,n(z)) = n(z),
axiom_039,
[final] ).
cnf(i_0_184,axiom,
eq2(n(X1),x2) = bfalse,
axiom_075,
[final] ).
cnf(i_0_185,axiom,
eq2(x2,n(X1)) = bfalse,
axiom_082,
[final] ).
cnf(i_0_186,axiom,
fail(X1,n(z)) = X1,
axiom_014,
[final] ).
cnf(i_0_187,axiom,
opt(n(X1)) = n(X1),
axiom_063,
[final] ).
cnf(i_0_188,axiom,
eq3(X1,X1) = btrue,
axiom_090,
[final] ).
cnf(i_0_189,axiom,
eq2(X1,X1) = btrue,
axiom_089,
[final] ).
cnf(i_0_190,axiom,
impl(btrue,X1) = X1,
axiom_043,
[final] ).
cnf(i_0_191,axiom,
addNat(z,X1) = X1,
axiom_050,
[final] ).
cnf(i_0_192,axiom,
d(n(X1)) = n(z),
axiom_045,
[final] ).
cnf(i_0_193,axiom,
impl(bfalse,X1) = btrue,
axiom_044,
[final] ).
cnf(i_0_194,axiom,
mulNat(z,X1) = z,
axiom_052,
[final] ).
cnf(i_0_195,axiom,
eq3(bfalse,btrue) = bfalse,
axiom_066,
[final] ).
cnf(i_0_196,axiom,
eq3(btrue,bfalse) = bfalse,
axiom_067,
[final] ).
cnf(i_0_197,axiom,
d(x2) = n(s(z)),
axiom_048,
[final] ).
cnf(i_0_198,axiom,
opt(x2) = x2,
axiom_064,
[final] ).
cnf(i_0_199,axiom,
X1 = X1 ).
cnf(i_0_200,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_201,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_202,axiom,
( X1 != X2
| prop2(X1) = prop2(X2) ) ).
cnf(i_0_203,axiom,
( X1 != X2
| n(X1) = n(X2) ) ).
cnf(i_0_204,axiom,
( X1 != X2
| aux(X1,X3,X4) = aux(X2,X3,X4) ) ).
cnf(i_0_205,axiom,
( X1 != X2
| aux(X3,X1,X4) = aux(X3,X2,X4) ) ).
cnf(i_0_206,axiom,
( X1 != X2
| aux(X3,X4,X1) = aux(X3,X4,X2) ) ).
cnf(i_0_207,axiom,
( X1 != X2
| fail32(X1,X3) = fail32(X2,X3) ) ).
cnf(i_0_208,axiom,
( X1 != X2
| fail32(X3,X1) = fail32(X3,X2) ) ).
cnf(i_0_209,axiom,
( X1 != X2
| fail(X1,X3) = fail(X2,X3) ) ).
cnf(i_0_210,axiom,
( X1 != X2
| fail(X3,X1) = fail(X3,X2) ) ).
cnf(i_0_211,axiom,
( X1 != X2
| fail3(X1,X3) = fail3(X2,X3) ) ).
cnf(i_0_212,axiom,
( X1 != X2
| fail3(X3,X1) = fail3(X3,X2) ) ).
cnf(i_0_213,axiom,
( X1 != X2
| fail12(X1,X3) = fail12(X2,X3) ) ).
cnf(i_0_214,axiom,
( X1 != X2
| fail12(X3,X1) = fail12(X3,X2) ) ).
cnf(i_0_215,axiom,
( X1 != X2
| s(X1) = s(X2) ) ).
cnf(i_0_216,axiom,
( X1 != X2
| fail22(X1,X3) = fail22(X2,X3) ) ).
cnf(i_0_217,axiom,
( X1 != X2
| fail22(X3,X1) = fail22(X3,X2) ) ).
cnf(i_0_218,axiom,
( X1 != X2
| mulNat(X1,X3) = mulNat(X2,X3) ) ).
cnf(i_0_219,axiom,
( X1 != X2
| mulNat(X3,X1) = mulNat(X3,X2) ) ).
cnf(i_0_220,axiom,
( X1 != X2
| addNat(X1,X3) = addNat(X2,X3) ) ).
cnf(i_0_221,axiom,
( X1 != X2
| addNat(X3,X1) = addNat(X3,X2) ) ).
cnf(i_0_222,axiom,
( X1 != X2
| impl(X1,X3) = impl(X2,X3) ) ).
cnf(i_0_223,axiom,
( X1 != X2
| impl(X3,X1) = impl(X3,X2) ) ).
cnf(i_0_224,axiom,
( X1 != X2
| eq2(X1,X3) = eq2(X2,X3) ) ).
cnf(i_0_225,axiom,
( X1 != X2
| eq2(X3,X1) = eq2(X3,X2) ) ).
cnf(i_0_226,axiom,
( X1 != X2
| opt(X1) = opt(X2) ) ).
cnf(i_0_227,axiom,
( X1 != X2
| d(X1) = d(X2) ) ).
cnf(i_0_228,axiom,
( X1 != X2
| x(X1,X3) = x(X2,X3) ) ).
cnf(i_0_229,axiom,
( X1 != X2
| x(X3,X1) = x(X3,X2) ) ).
cnf(i_0_230,axiom,
( X1 != X2
| y(X1,X3) = y(X2,X3) ) ).
cnf(i_0_231,axiom,
( X1 != X2
| y(X3,X1) = y(X3,X2) ) ).
cnf(i_0_232,axiom,
( X1 != X2
| eq3(X1,X3) = eq3(X2,X3) ) ).
cnf(i_0_233,axiom,
( X1 != X2
| eq3(X3,X1) = eq3(X3,X2) ) ).
cnf(i_0_234,axiom,
( X1 != X2
| fail1(X1,X3) = fail1(X2,X3) ) ).
cnf(i_0_235,axiom,
( X1 != X2
| fail1(X3,X1) = fail1(X3,X2) ) ).
cnf(i_0_236,plain,
X1 = impl(btrue,X1),
inference(scs_inference,[],[i_0_190,i_0_200]) ).
cnf(i_0_237,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(X2,X3),
inference(scs_inference,[],[i_0_190,i_0_189,i_0_200,i_0_130]) ).
cnf(i_0_239,plain,
eq2(y(X1,X2),y(X1,X3)) = eq2(X2,X3),
inference(scs_inference,[],[i_0_190,i_0_189,i_0_200,i_0_130,i_0_131]) ).
cnf(i_0_241,plain,
eq3(prop2(X1),bfalse) != impl(btrue,btrue),
inference(scs_inference,[],[i_0_175,i_0_190,i_0_189,i_0_200,i_0_130,i_0_131,i_0_201]) ).
cnf(i_0_242,plain,
impl(btrue,X1) = X1,
inference(rename_variables,[],[i_0_190]) ).
cnf(i_0_285,plain,
addNat(z,X1) = X1,
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_286,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(scs_inference,[],[i_0_179,i_0_200]) ).
cnf(i_0_287,plain,
fail3(X1,X1) = fail22(X1,X1),
inference(scs_inference,[],[i_0_179,i_0_180,i_0_200,i_0_201]) ).
cnf(i_0_288,plain,
fail12(X1,X2) = fail22(X1,X2),
inference(rename_variables,[],[i_0_179]) ).
cnf(i_0_289,plain,
fail3(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_180]) ).
cnf(i_0_292,plain,
fail(X1,n(z)) = X1,
inference(rename_variables,[],[i_0_186]) ).
cnf(i_0_298,plain,
fail22(X1,X2) = fail32(X1,X2),
inference(rename_variables,[],[i_0_181]) ).
cnf(i_0_301,plain,
fail1(X1,X2) = fail(X1,X2),
inference(scs_inference,[],[i_0_182,i_0_200]) ).
cnf(i_0_305,plain,
opt(x(n(z),X1)) = X1,
inference(rename_variables,[],[i_0_169]) ).
cnf(i_0_308,plain,
fail12(n(s(z)),X1) = X1,
inference(rename_variables,[],[i_0_176]) ).
cnf(i_0_312,plain,
btrue = eq3(X1,X1),
inference(scs_inference,[],[i_0_188,i_0_200]) ).
cnf(i_0_315,plain,
addNat(X1,mulNat(X2,X1)) = mulNat(s(X2),X1),
inference(scs_inference,[],[i_0_152,i_0_200]) ).
cnf(i_0_319,plain,
fail22(X1,n(s(z))) = X1,
inference(rename_variables,[],[i_0_177]) ).
cnf(i_0_323,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(scs_inference,[],[i_0_125,i_0_200]) ).
cnf(i_0_326,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(scs_inference,[],[i_0_138,i_0_200]) ).
cnf(i_0_328,plain,
addNat(z,X1) = X1,
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_331,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(scs_inference,[],[i_0_139,i_0_200]) ).
cnf(i_0_334,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_140,i_0_200]) ).
cnf(i_0_336,plain,
fail(X1,n(z)) = X1,
inference(rename_variables,[],[i_0_186]) ).
cnf(i_0_344,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(scs_inference,[],[i_0_141,i_0_200]) ).
cnf(i_0_364,plain,
opt(x(n(z),X1)) = X1,
inference(rename_variables,[],[i_0_169]) ).
cnf(i_0_367,plain,
fail12(n(s(z)),X1) = X1,
inference(rename_variables,[],[i_0_176]) ).
cnf(i_0_371,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_142,i_0_200]) ).
cnf(i_0_374,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(scs_inference,[],[i_0_143,i_0_200]) ).
cnf(i_0_390,plain,
fail22(X1,n(s(z))) = X1,
inference(rename_variables,[],[i_0_177]) ).
cnf(i_0_393,plain,
impl(btrue,X1) = X1,
inference(rename_variables,[],[i_0_190]) ).
cnf(i_0_397,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_144,i_0_200]) ).
cnf(i_0_404,plain,
addNat(z,X1) = X1,
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_407,plain,
fail(X1,n(z)) = X1,
inference(rename_variables,[],[i_0_186]) ).
cnf(i_0_410,plain,
n(mulNat(X1,X2)) = fail32(n(X1),n(X2)),
inference(scs_inference,[],[i_0_153,i_0_200]) ).
cnf(i_0_414,plain,
opt(n(X1)) = n(X1),
inference(rename_variables,[],[i_0_187]) ).
cnf(i_0_418,plain,
n(addNat(X1,X2)) = fail1(n(X1),n(X2)),
inference(scs_inference,[],[i_0_154,i_0_200]) ).
cnf(i_0_421,plain,
x(d(X1),d(X2)) = d(x(X1,X2)),
inference(scs_inference,[],[i_0_155,i_0_200]) ).
cnf(i_0_429,plain,
s(addNat(X1,X2)) = addNat(s(X1),X2),
inference(scs_inference,[],[i_0_157,i_0_200]) ).
cnf(i_0_431,plain,
impl(eq2(opt(d(X1)),x(y(X2,X2),y(X2,x(X2,X2)))),eq3(btrue,bfalse)) = prop2(X1),
inference(scs_inference,[],[i_0_110,i_0_200]) ).
cnf(i_0_437,plain,
x(opt(y(X1,X2)),opt(X3)) = aux(y(X1,X2),X3,bfalse),
inference(scs_inference,[],[i_0_116,i_0_200]) ).
cnf(i_0_439,plain,
x(opt(n(X1)),opt(X2)) = aux(n(X1),X2,bfalse),
inference(scs_inference,[],[i_0_134,i_0_200]) ).
cnf(i_0_448,plain,
y(n(s(s(z))),opt(X1)) = aux(X1,X2,btrue),
inference(scs_inference,[],[i_0_129,i_0_200]) ).
cnf(i_0_455,plain,
z = mulNat(z,X1),
inference(scs_inference,[],[i_0_194,i_0_200]) ).
cnf(i_0_460,plain,
bfalse = eq3(btrue,bfalse),
inference(scs_inference,[],[i_0_196,i_0_200]) ).
cnf(i_0_469,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(scs_inference,[],[i_0_173,i_0_200]) ).
cnf(i_0_471,plain,
fail32(X1,n(z)) = fail22(X1,n(z)),
inference(scs_inference,[],[i_0_174,i_0_200]) ).
cnf(i_0_494,plain,
y(opt(n(X1)),opt(X2)) = fail32(n(X1),X2),
inference(scs_inference,[],[i_0_156,i_0_200]) ).
cnf(i_0_500,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(scs_inference,[],[i_0_162,i_0_200]) ).
cnf(i_0_502,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(scs_inference,[],[i_0_163,i_0_200]) ).
cnf(i_0_521,plain,
y(opt(X1),opt(X2)) = fail32(X1,X2),
inference(scs_inference,[],[i_0_170,i_0_200]) ).
cnf(i_0_532,plain,
aux(X1,X2,eq2(X1,X2)) = fail1(X1,X2),
inference(scs_inference,[],[i_0_137,i_0_200]) ).
cnf(i_0_544,plain,
x(opt(X1),opt(X2)) = aux(X1,X2,bfalse),
inference(scs_inference,[],[i_0_147,i_0_200]) ).
cnf(i_0_546,plain,
X1 = opt(X1),
inference(scs_inference,[],[i_0_198,i_0_200]) ).
cnf(i_0_552,plain,
n(z) = d(n(X1)),
inference(scs_inference,[],[i_0_192,i_0_200]) ).
cnf(i_0_554,plain,
n(z) = fail3(X1,n(z)),
inference(scs_inference,[],[i_0_183,i_0_200]) ).
cnf(i_0_568,plain,
n(s(z)) = d(X1),
inference(scs_inference,[],[i_0_197,i_0_200]) ).
cnf(i_0_570,plain,
opt(n(X1)) = n(X1),
inference(rename_variables,[],[i_0_187]) ).
cnf(i_0_573,plain,
aux(n(X1),x(X2,X3),eq2(n(X1),x(X2,X3))) = fail1(n(X1),x(X2,X3)),
inference(scs_inference,[],[i_0_111,i_0_200]) ).
cnf(i_0_588,plain,
aux(n(X1),y(X2,X3),eq2(n(X1),y(X2,X3))) = fail1(n(X1),y(X2,X3)),
inference(scs_inference,[],[i_0_112,i_0_200]) ).
cnf(i_0_590,plain,
aux(x(X1,X2),X3,eq2(x(X1,X2),X3)) = fail1(x(X1,X2),X3),
inference(scs_inference,[],[i_0_113,i_0_200]) ).
cnf(i_0_607,plain,
aux(y(X1,X2),X3,eq2(y(X1,X2),X3)) = fail1(y(X1,X2),X3),
inference(scs_inference,[],[i_0_114,i_0_200]) ).
cnf(i_0_609,plain,
x(y(d(X1),X2),y(X1,d(X2))) = d(y(X1,X2)),
inference(scs_inference,[],[i_0_124,i_0_200]) ).
cnf(i_0_630,plain,
y(opt(n(X1)),opt(x(X2,X3))) = fail32(n(X1),x(X2,X3)),
inference(scs_inference,[],[i_0_117,i_0_200]) ).
cnf(i_0_632,plain,
opt(n(X1)) = n(X1),
inference(rename_variables,[],[i_0_187]) ).
cnf(i_0_673,plain,
y(opt(n(X1)),opt(y(X2,X3))) = fail32(n(X1),y(X2,X3)),
inference(scs_inference,[],[i_0_118,i_0_200]) ).
cnf(i_0_684,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(scs_inference,[],[i_0_119,i_0_200]) ).
cnf(i_0_686,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(scs_inference,[],[i_0_120,i_0_200]) ).
cnf(i_0_705,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(scs_inference,[],[i_0_121,i_0_200]) ).
cnf(i_0_708,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(scs_inference,[],[i_0_122,i_0_200]) ).
cnf(i_0_723,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(scs_inference,[],[i_0_123,i_0_200]) ).
cnf(i_0_740,plain,
eq2(n(X1),n(X2)) = eq2(n(s(X1)),n(s(X2))),
inference(scs_inference,[],[i_0_146,i_0_200]) ).
cnf(i_0_743,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(scs_inference,[],[i_0_150,i_0_200]) ).
cnf(i_0_752,plain,
fail1(X1,n(s(X2))) = fail(X1,n(s(X2))),
inference(scs_inference,[],[i_0_151,i_0_200]) ).
cnf(i_0_755,plain,
opt(x(X1,x(X2,X3))) = aux(x(X1,X2),X3,bfalse),
inference(scs_inference,[],[i_0_115,i_0_200]) ).
cnf(i_0_773,plain,
aux(n(X1),X2,eq2(n(X1),X2)) = fail1(n(X1),X2),
inference(scs_inference,[],[i_0_128,i_0_200]) ).
cnf(i_0_782,plain,
fail22(n(s(s(X1))),X2) = fail12(n(s(s(X1))),X2),
inference(scs_inference,[],[i_0_126,i_0_200]) ).
cnf(i_0_792,plain,
fail32(X1,n(s(s(X2)))) = fail22(X1,n(s(s(X2)))),
inference(scs_inference,[],[i_0_127,i_0_200]) ).
cnf(i_0_804,plain,
fail(n(s(X1)),X2) = opt(x(n(s(X1)),X2)),
inference(scs_inference,[],[i_0_132,i_0_200]) ).
cnf(i_0_813,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(scs_inference,[],[i_0_133,i_0_200]) ).
cnf(i_0_833,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(scs_inference,[],[i_0_180,i_0_200]) ).
cnf(i_0_836,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(scs_inference,[],[i_0_181,i_0_200]) ).
cnf(i_0_852,plain,
btrue = eq2(X1,X1),
inference(scs_inference,[],[i_0_189,i_0_200]) ).
cnf(i_0_862,plain,
X1 = opt(x(n(z),X1)),
inference(scs_inference,[],[i_0_169,i_0_200]) ).
cnf(i_0_865,plain,
X1 = fail12(n(s(z)),X1),
inference(scs_inference,[],[i_0_176,i_0_200]) ).
cnf(i_0_874,plain,
X1 = fail22(X1,n(s(z))),
inference(scs_inference,[],[i_0_177,i_0_200]) ).
cnf(i_0_883,plain,
X1 = addNat(z,X1),
inference(scs_inference,[],[i_0_191,i_0_200]) ).
cnf(i_0_886,plain,
n(X1) = opt(n(X1)),
inference(scs_inference,[],[i_0_187,i_0_200]) ).
cnf(i_0_897,plain,
X1 = fail(X1,n(z)),
inference(scs_inference,[],[i_0_186,i_0_200]) ).
cnf(i_0_1773,plain,
eq2(x(y(X1,X2),X3),x(x(X4,X5),X6)) = bfalse,
inference(scs_inference,[],[i_0_149,i_0_135]) ).
cnf(i_0_1775,plain,
eq2(y(y(X1,X2),X3),y(x(X4,X5),X6)) = bfalse,
inference(scs_inference,[],[i_0_149,i_0_135,i_0_136]) ).
cnf(i_0_2313,plain,
prop2(X1) = impl(eq2(opt(d(X1)),x(y(X2,X2),y(X2,x(X2,X2)))),eq3(btrue,bfalse)),
inference(rename_variables,[],[i_0_110]) ).
cnf(i_0_2395,plain,
prop2(X1) = impl(eq2(opt(d(X1)),x(y(X2,X2),y(X2,x(X2,X2)))),eq3(btrue,bfalse)),
inference(rename_variables,[],[i_0_110]) ).
cnf(i_0_2396,plain,
eq2(x(x(X1,X2),X3),x(n(X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_158,i_0_135]) ).
cnf(i_0_2398,plain,
eq2(y(x(X1,X2),X3),y(n(X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_158,i_0_135,i_0_136]) ).
cnf(i_0_2477,plain,
prop2(X1) = impl(eq2(opt(d(X1)),x(y(X2,X2),y(X2,x(X2,X2)))),eq3(btrue,bfalse)),
inference(rename_variables,[],[i_0_110]) ).
cnf(i_0_2559,plain,
prop2(X1) = impl(eq2(opt(d(X1)),x(y(X2,X2),y(X2,x(X2,X2)))),eq3(btrue,bfalse)),
inference(rename_variables,[],[i_0_110]) ).
cnf(i_0_2641,plain,
prop2(X1) = impl(eq2(opt(d(X1)),x(y(X2,X2),y(X2,x(X2,X2)))),eq3(btrue,bfalse)),
inference(rename_variables,[],[i_0_110]) ).
cnf(i_0_2722,plain,
prop2(X1) = impl(eq2(opt(d(X1)),x(y(X2,X2),y(X2,x(X2,X2)))),eq3(btrue,bfalse)),
inference(rename_variables,[],[i_0_110]) ).
cnf(i_0_2805,plain,
fail1(n(X1),x(X2,X3)) = aux(n(X1),x(X2,X3),eq2(n(X1),x(X2,X3))),
inference(rename_variables,[],[i_0_111]) ).
cnf(i_0_2889,plain,
fail1(n(X1),x(X2,X3)) = aux(n(X1),x(X2,X3),eq2(n(X1),x(X2,X3))),
inference(rename_variables,[],[i_0_111]) ).
cnf(i_0_3014,plain,
eq2(x(y(X1,X2),X3),x(n(X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_159,i_0_135]) ).
cnf(i_0_3016,plain,
eq2(y(y(X1,X2),X3),y(n(X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_159,i_0_135,i_0_136]) ).
cnf(i_0_3220,plain,
fail1(n(X1),y(X2,X3)) = aux(n(X1),y(X2,X3),eq2(n(X1),y(X2,X3))),
inference(rename_variables,[],[i_0_112]) ).
cnf(i_0_3302,plain,
fail1(n(X1),y(X2,X3)) = aux(n(X1),y(X2,X3),eq2(n(X1),y(X2,X3))),
inference(rename_variables,[],[i_0_112]) ).
cnf(i_0_3385,plain,
fail1(n(X1),y(X2,X3)) = aux(n(X1),y(X2,X3),eq2(n(X1),y(X2,X3))),
inference(rename_variables,[],[i_0_112]) ).
cnf(i_0_3469,plain,
fail1(n(X1),y(X2,X3)) = aux(n(X1),y(X2,X3),eq2(n(X1),y(X2,X3))),
inference(rename_variables,[],[i_0_112]) ).
cnf(i_0_3551,plain,
fail1(n(X1),y(X2,X3)) = aux(n(X1),y(X2,X3),eq2(n(X1),y(X2,X3))),
inference(rename_variables,[],[i_0_112]) ).
cnf(i_0_3634,plain,
fail1(n(X1),y(X2,X3)) = aux(n(X1),y(X2,X3),eq2(n(X1),y(X2,X3))),
inference(rename_variables,[],[i_0_112]) ).
cnf(i_0_3636,plain,
eq2(x(n(X1),X2),x(x(X3,X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_160,i_0_135]) ).
cnf(i_0_3638,plain,
eq2(y(n(X1),X2),y(x(X3,X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_160,i_0_135,i_0_136]) ).
cnf(i_0_3718,plain,
fail1(x(X1,X2),X3) = aux(x(X1,X2),X3,eq2(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_113]) ).
cnf(i_0_3802,plain,
fail1(x(X1,X2),X3) = aux(x(X1,X2),X3,eq2(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_113]) ).
cnf(i_0_3885,plain,
fail1(x(X1,X2),X3) = aux(x(X1,X2),X3,eq2(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_113]) ).
cnf(i_0_3968,plain,
fail1(x(X1,X2),X3) = aux(x(X1,X2),X3,eq2(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_113]) ).
cnf(i_0_4051,plain,
fail1(x(X1,X2),X3) = aux(x(X1,X2),X3,eq2(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_113]) ).
cnf(i_0_4133,plain,
fail1(y(X1,X2),X3) = aux(y(X1,X2),X3,eq2(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_114]) ).
cnf(i_0_243,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(scs_inference,[],[i_0_237,i_0_200]) ).
cnf(i_0_244,plain,
eq2(y(X1,x(X2,X3)),y(X1,x(X2,X4))) = eq2(X3,X4),
inference(scs_inference,[],[i_0_237,i_0_239,i_0_200,i_0_201]) ).
cnf(i_0_245,plain,
eq2(y(X1,X2),y(X1,X3)) = eq2(X2,X3),
inference(rename_variables,[],[i_0_239]) ).
cnf(i_0_290,plain,
fail22(X1,X1) = fail3(X1,X1),
inference(scs_inference,[],[i_0_287,i_0_200]) ).
cnf(i_0_291,plain,
fail(fail3(X1,X1),n(z)) = fail22(X1,X1),
inference(scs_inference,[],[i_0_287,i_0_186,i_0_200,i_0_201]) ).
cnf(i_0_295,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_286]) ).
cnf(i_0_316,plain,
impl(bfalse,X1) = eq3(X2,X2),
inference(scs_inference,[],[i_0_312,i_0_152,i_0_193,i_0_200,i_0_201]) ).
cnf(i_0_327,plain,
addNat(z,y(opt(x(X1,X2)),opt(X3))) = fail32(x(X1,X2),X3),
inference(scs_inference,[],[i_0_323,i_0_138,i_0_191,i_0_200,i_0_201]) ).
cnf(i_0_335,plain,
fail(btrue,n(z)) = eq3(X1,X1),
inference(scs_inference,[],[i_0_312,i_0_140,i_0_186,i_0_200,i_0_201]) ).
cnf(i_0_339,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_334]) ).
cnf(i_0_340,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_345,plain,
fail22(y(X1,X2),x(X3,X4)) = fail3(y(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_331,i_0_334,i_0_141,i_0_200,i_0_201]) ).
cnf(i_0_346,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_334]) ).
cnf(i_0_347,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(rename_variables,[],[i_0_331]) ).
cnf(i_0_350,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_344]) ).
cnf(i_0_351,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_354,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_344]) ).
cnf(i_0_355,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(rename_variables,[],[i_0_331]) ).
cnf(i_0_358,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_334]) ).
cnf(i_0_359,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_286]) ).
cnf(i_0_375,plain,
y(opt(x(X1,X2)),opt(x(X3,X4))) = fail22(x(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_371,i_0_323,i_0_143,i_0_200,i_0_201]) ).
cnf(i_0_376,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_371]) ).
cnf(i_0_377,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_380,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_374]) ).
cnf(i_0_381,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_436,plain,
impl(eq2(opt(d(X1)),x(y(X2,X2),y(X2,x(X2,X2)))),eq3(btrue,bfalse)) = prop2(X1),
inference(rename_variables,[],[i_0_431]) ).
cnf(i_0_444,plain,
addNat(X1,mulNat(X2,X1)) = mulNat(s(X2),X1),
inference(rename_variables,[],[i_0_315]) ).
cnf(i_0_445,plain,
s(addNat(X1,X2)) = addNat(s(X1),X2),
inference(rename_variables,[],[i_0_429]) ).
cnf(i_0_451,plain,
s(addNat(X1,X2)) = addNat(s(X1),X2),
inference(rename_variables,[],[i_0_429]) ).
cnf(i_0_454,plain,
y(n(s(s(z))),opt(X1)) = aux(X1,X2,btrue),
inference(rename_variables,[],[i_0_448]) ).
cnf(i_0_462,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_472,plain,
fail32(n(z),x(X1,X2)) = fail12(n(z),x(X1,X2)),
inference(scs_inference,[],[i_0_469,i_0_371,i_0_174,i_0_200,i_0_201]) ).
cnf(i_0_473,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_469]) ).
cnf(i_0_474,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_371]) ).
cnf(i_0_477,plain,
fail32(X1,n(z)) = fail22(X1,n(z)),
inference(rename_variables,[],[i_0_471]) ).
cnf(i_0_478,plain,
n(mulNat(X1,X2)) = fail32(n(X1),n(X2)),
inference(rename_variables,[],[i_0_410]) ).
cnf(i_0_481,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_469]) ).
cnf(i_0_482,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_374]) ).
cnf(i_0_485,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_469]) ).
cnf(i_0_486,plain,
fail32(X1,n(z)) = fail22(X1,n(z)),
inference(rename_variables,[],[i_0_471]) ).
cnf(i_0_495,plain,
eq2(x(X1,X2),n(X3)) = eq3(btrue,bfalse),
inference(scs_inference,[],[i_0_460,i_0_156,i_0_158,i_0_200,i_0_201]) ).
cnf(i_0_503,plain,
fail1(X1,x(X2,X3)) = opt(x(X1,x(X2,X3))),
inference(scs_inference,[],[i_0_397,i_0_500,i_0_163,i_0_200,i_0_201]) ).
cnf(i_0_504,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(rename_variables,[],[i_0_500]) ).
cnf(i_0_505,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_508,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(rename_variables,[],[i_0_502]) ).
cnf(i_0_511,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(rename_variables,[],[i_0_500]) ).
cnf(i_0_525,plain,
y(opt(X1),opt(X2)) = fail32(X1,X2),
inference(rename_variables,[],[i_0_521]) ).
cnf(i_0_536,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_301]) ).
cnf(i_0_537,plain,
aux(X1,X2,eq2(X1,X2)) = fail1(X1,X2),
inference(rename_variables,[],[i_0_532]) ).
cnf(i_0_547,plain,
eq2(y(X1,X2),X3) = eq3(btrue,bfalse),
inference(scs_inference,[],[i_0_460,i_0_198,i_0_166,i_0_200,i_0_201]) ).
cnf(i_0_555,plain,
fail3(X1,n(z)) = d(n(X2)),
inference(scs_inference,[],[i_0_552,i_0_183,i_0_200,i_0_201]) ).
cnf(i_0_560,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(rename_variables,[],[i_0_502]) ).
cnf(i_0_569,plain,
opt(n(z)) = d(n(X1)),
inference(scs_inference,[],[i_0_552,i_0_197,i_0_187,i_0_200,i_0_201]) ).
cnf(i_0_578,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_595,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_596,plain,
aux(x(X1,X2),X3,eq2(x(X1,X2),X3)) = fail1(x(X1,X2),X3),
inference(rename_variables,[],[i_0_590]) ).
cnf(i_0_599,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_301]) ).
cnf(i_0_600,plain,
aux(x(X1,X2),X3,eq2(x(X1,X2),X3)) = fail1(x(X1,X2),X3),
inference(rename_variables,[],[i_0_590]) ).
cnf(i_0_612,plain,
aux(y(X1,X2),X3,eq2(y(X1,X2),X3)) = fail1(y(X1,X2),X3),
inference(rename_variables,[],[i_0_607]) ).
cnf(i_0_615,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_301]) ).
cnf(i_0_616,plain,
aux(y(X1,X2),X3,eq2(y(X1,X2),X3)) = fail1(y(X1,X2),X3),
inference(rename_variables,[],[i_0_607]) ).
cnf(i_0_623,plain,
aux(X1,X2,eq2(X1,X2)) = fail1(X1,X2),
inference(rename_variables,[],[i_0_532]) ).
cnf(i_0_627,plain,
aux(x(X1,X2),X3,eq2(x(X1,X2),X3)) = fail1(x(X1,X2),X3),
inference(rename_variables,[],[i_0_590]) ).
cnf(i_0_631,plain,
opt(n(z)) = fail3(X1,n(z)),
inference(scs_inference,[],[i_0_554,i_0_117,i_0_187,i_0_200,i_0_201]) ).
cnf(i_0_635,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_371]) ).
cnf(i_0_650,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_653,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_656,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_334]) ).
cnf(i_0_666,plain,
aux(y(X1,X2),X3,eq2(y(X1,X2),X3)) = fail1(y(X1,X2),X3),
inference(rename_variables,[],[i_0_607]) ).
cnf(i_0_670,plain,
aux(X1,X2,eq2(X1,X2)) = fail1(X1,X2),
inference(rename_variables,[],[i_0_532]) ).
cnf(i_0_678,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_374]) ).
cnf(i_0_687,plain,
fail1(x(X1,X2),x(X3,X4)) = opt(x(x(X1,X2),x(X3,X4))),
inference(scs_inference,[],[i_0_684,i_0_397,i_0_120,i_0_200,i_0_201]) ).
cnf(i_0_688,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_684]) ).
cnf(i_0_689,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_692,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_686]) ).
cnf(i_0_696,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_686]) ).
cnf(i_0_697,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_700,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_684]) ).
cnf(i_0_710,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_705]) ).
cnf(i_0_713,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_708]) ).
cnf(i_0_717,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_705]) ).
cnf(i_0_728,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(rename_variables,[],[i_0_723]) ).
cnf(i_0_729,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_708]) ).
cnf(i_0_732,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(rename_variables,[],[i_0_723]) ).
cnf(i_0_745,plain,
eq2(n(X1),n(X2)) = eq2(n(s(X1)),n(s(X2))),
inference(rename_variables,[],[i_0_740]) ).
cnf(i_0_748,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_743]) ).
cnf(i_0_749,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(rename_variables,[],[i_0_331]) ).
cnf(i_0_754,plain,
eq2(n(X1),n(X2)) = eq2(n(s(X1)),n(s(X2))),
inference(rename_variables,[],[i_0_740]) ).
cnf(i_0_756,plain,
n(addNat(X1,s(X2))) = fail(n(X1),n(s(X2))),
inference(scs_inference,[],[i_0_418,i_0_752,i_0_115,i_0_200,i_0_201]) ).
cnf(i_0_757,plain,
fail1(X1,n(s(X2))) = fail(X1,n(s(X2))),
inference(rename_variables,[],[i_0_752]) ).
cnf(i_0_758,plain,
n(addNat(X1,X2)) = fail1(n(X1),n(X2)),
inference(rename_variables,[],[i_0_418]) ).
cnf(i_0_761,plain,
opt(x(X1,x(X2,X3))) = aux(x(X1,X2),X3,bfalse),
inference(rename_variables,[],[i_0_755]) ).
cnf(i_0_762,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_684]) ).
cnf(i_0_765,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_743]) ).
cnf(i_0_766,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_286]) ).
cnf(i_0_777,plain,
opt(x(X1,x(X2,X3))) = aux(x(X1,X2),X3,bfalse),
inference(rename_variables,[],[i_0_755]) ).
cnf(i_0_778,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_686]) ).
cnf(i_0_800,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_708]) ).
cnf(i_0_808,plain,
fail(n(s(X1)),X2) = opt(x(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_804]) ).
cnf(i_0_809,plain,
fail1(X1,n(s(X2))) = fail(X1,n(s(X2))),
inference(rename_variables,[],[i_0_752]) ).
cnf(i_0_817,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_813]) ).
cnf(i_0_822,plain,
eq2(X1,X2) = eq2(y(X3,X1),y(X3,X2)),
inference(scs_inference,[],[i_0_239,i_0_200]) ).
cnf(i_0_823,plain,
fail12(n(s(X1)),y(X2,X3)) = opt(y(n(s(X1)),y(X2,X3))),
inference(scs_inference,[],[i_0_813,i_0_344,i_0_239,i_0_200,i_0_201]) ).
cnf(i_0_824,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_813]) ).
cnf(i_0_825,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_344]) ).
cnf(i_0_837,plain,
fail22(n(s(s(X1))),X2) = fail3(n(s(s(X1))),X2),
inference(scs_inference,[],[i_0_782,i_0_833,i_0_181,i_0_200,i_0_201]) ).
cnf(i_0_838,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(rename_variables,[],[i_0_833]) ).
cnf(i_0_839,plain,
fail22(n(s(s(X1))),X2) = fail12(n(s(s(X1))),X2),
inference(rename_variables,[],[i_0_782]) ).
cnf(i_0_842,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(rename_variables,[],[i_0_836]) ).
cnf(i_0_848,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(rename_variables,[],[i_0_836]) ).
cnf(i_0_869,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(rename_variables,[],[i_0_833]) ).
cnf(i_0_870,plain,
X1 = fail12(n(s(z)),X1),
inference(rename_variables,[],[i_0_865]) ).
cnf(i_0_890,plain,
n(X1) = opt(n(X1)),
inference(rename_variables,[],[i_0_886]) ).
cnf(i_0_893,plain,
n(X1) = opt(n(X1)),
inference(rename_variables,[],[i_0_886]) ).
cnf(i_0_899,plain,
fail(n(s(X1)),X2) = opt(x(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_804]) ).
cnf(i_0_903,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_897]) ).
cnf(i_0_906,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(rename_variables,[],[i_0_723]) ).
cnf(i_0_911,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_705]) ).
cnf(i_0_913,plain,
fail22(n(s(s(X1))),n(s(X2))) = fail3(n(s(s(X1))),n(s(X2))),
inference(scs_inference,[],[i_0_782,i_0_743,i_0_201]) ).
cnf(i_0_914,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_743]) ).
cnf(i_0_915,plain,
fail22(n(s(s(X1))),X2) = fail12(n(s(s(X1))),X2),
inference(rename_variables,[],[i_0_782]) ).
cnf(i_0_916,plain,
fail3(n(s(s(X1))),n(s(X2))) = fail22(n(s(s(X1))),n(s(X2))),
inference(scs_inference,[],[i_0_782,i_0_743,i_0_201,i_0_200]) ).
cnf(i_0_918,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_813]) ).
cnf(i_0_920,plain,
x(X1,X2) = aux(x(n(z),X1),X2,bfalse),
inference(scs_inference,[],[i_0_862,i_0_755,i_0_201]) ).
cnf(i_0_921,plain,
opt(x(X1,x(X2,X3))) = aux(x(X1,X2),X3,bfalse),
inference(rename_variables,[],[i_0_755]) ).
cnf(i_0_922,plain,
X1 = opt(x(n(z),X1)),
inference(rename_variables,[],[i_0_862]) ).
cnf(i_0_923,plain,
aux(x(n(z),X1),X2,bfalse) = x(X1,X2),
inference(scs_inference,[],[i_0_862,i_0_755,i_0_201,i_0_200]) ).
cnf(i_0_949,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_708]) ).
cnf(i_0_952,plain,
fail32(X1,n(z)) = fail22(X1,n(z)),
inference(rename_variables,[],[i_0_471]) ).
cnf(i_0_955,plain,
X1 = opt(x(X1,n(z))),
inference(scs_inference,[],[i_0_897,i_0_500,i_0_201]) ).
cnf(i_0_956,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(rename_variables,[],[i_0_500]) ).
cnf(i_0_957,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_897]) ).
cnf(i_0_958,plain,
opt(x(X1,n(z))) = X1,
inference(scs_inference,[],[i_0_897,i_0_500,i_0_201,i_0_200]) ).
cnf(i_0_967,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(rename_variables,[],[i_0_833]) ).
cnf(i_0_969,plain,
mulNat(X1,z) = mulNat(s(X1),z),
inference(scs_inference,[],[i_0_883,i_0_315,i_0_201]) ).
cnf(i_0_970,plain,
addNat(X1,mulNat(X2,X1)) = mulNat(s(X2),X1),
inference(rename_variables,[],[i_0_315]) ).
cnf(i_0_971,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_883]) ).
cnf(i_0_972,plain,
mulNat(s(X1),z) = mulNat(X1,z),
inference(scs_inference,[],[i_0_883,i_0_315,i_0_201,i_0_200]) ).
cnf(i_0_978,plain,
X1 = fail22(X1,n(s(z))),
inference(rename_variables,[],[i_0_874]) ).
cnf(i_0_987,plain,
X1 = fail22(X1,n(s(z))),
inference(rename_variables,[],[i_0_874]) ).
cnf(i_0_996,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(rename_variables,[],[i_0_723]) ).
cnf(i_0_1003,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_705]) ).
cnf(i_0_1005,plain,
n(s(X1)) = fail3(n(s(z)),n(s(X1))),
inference(scs_inference,[],[i_0_865,i_0_743,i_0_201]) ).
cnf(i_0_1006,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_743]) ).
cnf(i_0_1007,plain,
X1 = fail12(n(s(z)),X1),
inference(rename_variables,[],[i_0_865]) ).
cnf(i_0_1008,plain,
fail3(n(s(z)),n(s(X1))) = n(s(X1)),
inference(scs_inference,[],[i_0_865,i_0_743,i_0_201,i_0_200]) ).
cnf(i_0_1015,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_813]) ).
cnf(i_0_1020,plain,
fail32(n(z),n(s(s(X1)))) = fail12(n(z),n(s(s(X1)))),
inference(scs_inference,[],[i_0_792,i_0_469,i_0_201]) ).
cnf(i_0_1021,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_469]) ).
cnf(i_0_1022,plain,
fail32(X1,n(s(s(X2)))) = fail22(X1,n(s(s(X2)))),
inference(rename_variables,[],[i_0_792]) ).
cnf(i_0_1023,plain,
fail12(n(z),n(s(s(X1)))) = fail32(n(z),n(s(s(X1)))),
inference(scs_inference,[],[i_0_792,i_0_469,i_0_201,i_0_200]) ).
cnf(i_0_1024,plain,
fail1(X1,n(s(X2))) = opt(x(X1,n(s(X2)))),
inference(scs_inference,[],[i_0_752,i_0_500,i_0_201]) ).
cnf(i_0_1025,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(rename_variables,[],[i_0_500]) ).
cnf(i_0_1026,plain,
fail1(X1,n(s(X2))) = fail(X1,n(s(X2))),
inference(rename_variables,[],[i_0_752]) ).
cnf(i_0_1027,plain,
opt(x(X1,n(s(X2)))) = fail1(X1,n(s(X2))),
inference(scs_inference,[],[i_0_752,i_0_500,i_0_201,i_0_200]) ).
cnf(i_0_1029,plain,
addNat(X1,mulNat(X2,X1)) = mulNat(s(X2),X1),
inference(rename_variables,[],[i_0_315]) ).
cnf(i_0_1049,plain,
fail32(x(X1,X2),n(s(s(X3)))) = fail12(x(X1,X2),n(s(s(X3)))),
inference(scs_inference,[],[i_0_792,i_0_326,i_0_201]) ).
cnf(i_0_1050,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_1051,plain,
fail32(X1,n(s(s(X2)))) = fail22(X1,n(s(s(X2)))),
inference(rename_variables,[],[i_0_792]) ).
cnf(i_0_1052,plain,
fail12(x(X1,X2),n(s(s(X3)))) = fail32(x(X1,X2),n(s(s(X3)))),
inference(scs_inference,[],[i_0_792,i_0_326,i_0_201,i_0_200]) ).
cnf(i_0_1054,plain,
addNat(X1,mulNat(X2,X1)) = mulNat(s(X2),X1),
inference(rename_variables,[],[i_0_315]) ).
cnf(i_0_1057,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_883]) ).
cnf(i_0_1059,plain,
aux(n(X1),X2,eq2(n(X1),X2)) = fail(n(X1),X2),
inference(scs_inference,[],[i_0_773,i_0_301,i_0_201]) ).
cnf(i_0_1060,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_301]) ).
cnf(i_0_1061,plain,
fail(n(X1),X2) = aux(n(X1),X2,eq2(n(X1),X2)),
inference(scs_inference,[],[i_0_773,i_0_301,i_0_201,i_0_200]) ).
cnf(i_0_1077,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_705]) ).
cnf(i_0_1114,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(rename_variables,[],[i_0_723]) ).
cnf(i_0_1120,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(rename_variables,[],[i_0_836]) ).
cnf(i_0_1124,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_1127,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_374]) ).
cnf(i_0_1195,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_1317,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_1815,plain,
eq2(x(x(y(X1,X2),X3),X4),x(x(x(X5,X6),X7),X8)) = bfalse,
inference(scs_inference,[],[i_0_1773,i_0_135]) ).
cnf(i_0_1817,plain,
eq2(y(x(y(X1,X2),X3),X4),y(x(x(X5,X6),X7),X8)) = bfalse,
inference(scs_inference,[],[i_0_1773,i_0_135,i_0_136]) ).
cnf(i_0_1857,plain,
eq2(x(y(y(X1,X2),X3),X4),x(y(x(X5,X6),X7),X8)) = bfalse,
inference(scs_inference,[],[i_0_1775,i_0_135]) ).
cnf(i_0_1859,plain,
eq2(y(y(y(X1,X2),X3),X4),y(y(x(X5,X6),X7),X8)) = bfalse,
inference(scs_inference,[],[i_0_1775,i_0_135,i_0_136]) ).
cnf(i_0_2272,plain,
X1 = opt(x(n(z),X1)),
inference(rename_variables,[],[i_0_862]) ).
cnf(i_0_2437,plain,
eq2(x(x(x(X1,X2),X3),X4),x(x(n(X5),X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_2396,i_0_135]) ).
cnf(i_0_2439,plain,
eq2(y(x(x(X1,X2),X3),X4),y(x(n(X5),X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_2396,i_0_135,i_0_136]) ).
cnf(i_0_2478,plain,
eq2(x(y(x(X1,X2),X3),X4),x(y(n(X5),X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_2398,i_0_135]) ).
cnf(i_0_2480,plain,
eq2(y(y(x(X1,X2),X3),X4),y(y(n(X5),X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_2398,i_0_135,i_0_136]) ).
cnf(i_0_2600,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_3056,plain,
eq2(x(x(y(X1,X2),X3),X4),x(x(n(X5),X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_3014,i_0_135]) ).
cnf(i_0_3058,plain,
eq2(y(x(y(X1,X2),X3),X4),y(x(n(X5),X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_3014,i_0_135,i_0_136]) ).
cnf(i_0_3096,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_883]) ).
cnf(i_0_3097,plain,
eq2(x(y(y(X1,X2),X3),X4),x(y(n(X5),X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_3016,i_0_135]) ).
cnf(i_0_3099,plain,
eq2(y(y(y(X1,X2),X3),X4),y(y(n(X5),X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_3016,i_0_135,i_0_136]) ).
cnf(i_0_3179,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_897]) ).
cnf(i_0_3678,plain,
eq2(x(x(n(X1),X2),X3),x(x(x(X4,X5),X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_3636,i_0_135]) ).
cnf(i_0_3680,plain,
eq2(y(x(n(X1),X2),X3),y(x(x(X4,X5),X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_3636,i_0_135,i_0_136]) ).
cnf(i_0_3720,plain,
eq2(x(y(n(X1),X2),X3),x(y(x(X4,X5),X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_3638,i_0_135]) ).
cnf(i_0_3722,plain,
eq2(y(y(n(X1),X2),X3),y(y(x(X4,X5),X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_3638,i_0_135,i_0_136]) ).
cnf(i_0_246,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(scs_inference,[],[i_0_244,i_0_200]) ).
cnf(i_0_247,plain,
eq2(y(X1,x(X2,X3)),y(X1,x(X2,X4))) = eq2(x(X5,X3),x(X5,X4)),
inference(scs_inference,[],[i_0_243,i_0_244,i_0_200,i_0_201]) ).
cnf(i_0_248,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_254,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_267,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_293,plain,
fail22(X1,X1) = fail(fail3(X1,X1),n(z)),
inference(scs_inference,[],[i_0_291,i_0_200]) ).
cnf(i_0_294,plain,
fail(fail3(X1,X1),n(z)) = fail12(X1,X1),
inference(scs_inference,[],[i_0_286,i_0_291,i_0_200,i_0_201]) ).
cnf(i_0_317,plain,
eq3(X1,X1) = impl(bfalse,X2),
inference(scs_inference,[],[i_0_316,i_0_200]) ).
cnf(i_0_318,plain,
fail22(addNat(X1,mulNat(X2,X1)),n(s(z))) = mulNat(s(X2),X1),
inference(scs_inference,[],[i_0_315,i_0_316,i_0_177,i_0_200,i_0_201]) ).
cnf(i_0_329,plain,
fail32(x(X1,X2),X3) = addNat(z,y(opt(x(X1,X2)),opt(X3))),
inference(scs_inference,[],[i_0_327,i_0_200]) ).
cnf(i_0_330,plain,
eq3(X1,X1) = eq3(X2,X2),
inference(scs_inference,[],[i_0_312,i_0_327,i_0_188,i_0_200,i_0_201]) ).
cnf(i_0_337,plain,
eq3(X1,X1) = fail(btrue,n(z)),
inference(scs_inference,[],[i_0_335,i_0_200]) ).
cnf(i_0_338,plain,
fail22(x(X1,X2),x(X3,X4)) = fail3(x(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_326,i_0_334,i_0_335,i_0_200,i_0_201]) ).
cnf(i_0_348,plain,
fail3(y(X1,X2),x(X3,X4)) = fail22(y(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_345,i_0_200]) ).
cnf(i_0_349,plain,
fail22(x(X1,X2),y(X3,X4)) = fail3(x(X1,X2),y(X3,X4)),
inference(scs_inference,[],[i_0_344,i_0_326,i_0_345,i_0_200,i_0_201]) ).
cnf(i_0_378,plain,
fail22(x(X1,X2),x(X3,X4)) = y(opt(x(X1,X2)),opt(x(X3,X4))),
inference(scs_inference,[],[i_0_375,i_0_200]) ).
cnf(i_0_379,plain,
y(opt(x(X1,X2)),opt(y(X3,X4))) = fail22(x(X1,X2),y(X3,X4)),
inference(scs_inference,[],[i_0_374,i_0_323,i_0_375,i_0_200,i_0_201]) ).
cnf(i_0_475,plain,
fail12(n(z),x(X1,X2)) = fail32(n(z),x(X1,X2)),
inference(scs_inference,[],[i_0_472,i_0_200]) ).
cnf(i_0_476,plain,
n(mulNat(X1,z)) = fail22(n(X1),n(z)),
inference(scs_inference,[],[i_0_471,i_0_410,i_0_472,i_0_200,i_0_201]) ).
cnf(i_0_496,plain,
eq3(btrue,bfalse) = eq2(x(X1,X2),n(X3)),
inference(scs_inference,[],[i_0_495,i_0_200]) ).
cnf(i_0_497,plain,
eq2(y(X1,X2),n(X3)) = eq3(btrue,bfalse),
inference(scs_inference,[],[i_0_460,i_0_495,i_0_159,i_0_200,i_0_201]) ).
cnf(i_0_506,plain,
opt(x(X1,x(X2,X3))) = fail1(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_503,i_0_200]) ).
cnf(i_0_507,plain,
fail22(X1,X1) = opt(y(X1,X1)),
inference(scs_inference,[],[i_0_290,i_0_502,i_0_503,i_0_200,i_0_201]) ).
cnf(i_0_548,plain,
eq3(btrue,bfalse) = eq2(y(X1,X2),X3),
inference(scs_inference,[],[i_0_547,i_0_200]) ).
cnf(i_0_549,plain,
eq2(X1,x(X2,X3)) = eq3(btrue,bfalse),
inference(scs_inference,[],[i_0_460,i_0_547,i_0_167,i_0_200,i_0_201]) ).
cnf(i_0_556,plain,
d(n(X1)) = fail3(X2,n(z)),
inference(scs_inference,[],[i_0_555,i_0_200]) ).
cnf(i_0_557,plain,
opt(y(n(z),X1)) = fail3(X2,n(z)),
inference(scs_inference,[],[i_0_554,i_0_555,i_0_164,i_0_200,i_0_201]) ).
cnf(i_0_571,plain,
d(n(X1)) = opt(n(z)),
inference(scs_inference,[],[i_0_569,i_0_200]) ).
cnf(i_0_572,plain,
d(n(X1)) = d(n(X2)),
inference(scs_inference,[],[i_0_552,i_0_569,i_0_192,i_0_200,i_0_201]) ).
cnf(i_0_633,plain,
fail3(X1,n(z)) = opt(n(z)),
inference(scs_inference,[],[i_0_631,i_0_200]) ).
cnf(i_0_634,plain,
y(opt(n(X1)),opt(x(X2,X3))) = fail22(n(X1),x(X2,X3)),
inference(scs_inference,[],[i_0_630,i_0_371,i_0_631,i_0_200,i_0_201]) ).
cnf(i_0_643,plain,
addNat(z,y(opt(x(X1,X2)),opt(X3))) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_690,plain,
opt(x(x(X1,X2),x(X3,X4))) = fail1(x(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_687,i_0_200]) ).
cnf(i_0_759,plain,
fail(n(X1),n(s(X2))) = n(addNat(X1,s(X2))),
inference(scs_inference,[],[i_0_756,i_0_200]) ).
cnf(i_0_760,plain,
fail(x(X1,X2),x(X3,X4)) = aux(x(x(X1,X2),X3),X4,bfalse),
inference(scs_inference,[],[i_0_755,i_0_684,i_0_756,i_0_200,i_0_201]) ).
cnf(i_0_826,plain,
opt(y(n(s(X1)),y(X2,X3))) = fail12(n(s(X1)),y(X2,X3)),
inference(scs_inference,[],[i_0_823,i_0_200]) ).
cnf(i_0_840,plain,
fail3(n(s(s(X1))),X2) = fail22(n(s(s(X1))),X2),
inference(scs_inference,[],[i_0_837,i_0_200]) ).
cnf(i_0_924,plain,
aux(x(n(z),d(X1)),d(X2),bfalse) = d(x(X1,X2)),
inference(scs_inference,[],[i_0_421,i_0_923,i_0_201]) ).
cnf(i_0_925,plain,
aux(x(n(z),X1),X2,bfalse) = x(X1,X2),
inference(rename_variables,[],[i_0_923]) ).
cnf(i_0_926,plain,
d(x(X1,X2)) = aux(x(n(z),d(X1)),d(X2),bfalse),
inference(scs_inference,[],[i_0_421,i_0_923,i_0_201,i_0_200]) ).
cnf(i_0_927,plain,
aux(x(n(z),y(d(X1),X2)),y(X1,d(X2)),bfalse) = d(y(X1,X2)),
inference(scs_inference,[],[i_0_609,i_0_923,i_0_201]) ).
cnf(i_0_928,plain,
aux(x(n(z),X1),X2,bfalse) = x(X1,X2),
inference(rename_variables,[],[i_0_923]) ).
cnf(i_0_929,plain,
d(y(X1,X2)) = aux(x(n(z),y(d(X1),X2)),y(X1,d(X2)),bfalse),
inference(scs_inference,[],[i_0_609,i_0_923,i_0_201,i_0_200]) ).
cnf(i_0_930,plain,
aux(x(n(z),opt(y(X1,X2))),opt(X3),bfalse) = aux(y(X1,X2),X3,bfalse),
inference(scs_inference,[],[i_0_437,i_0_923,i_0_201]) ).
cnf(i_0_931,plain,
aux(x(n(z),X1),X2,bfalse) = x(X1,X2),
inference(rename_variables,[],[i_0_923]) ).
cnf(i_0_932,plain,
aux(y(X1,X2),X3,bfalse) = aux(x(n(z),opt(y(X1,X2))),opt(X3),bfalse),
inference(scs_inference,[],[i_0_437,i_0_923,i_0_201,i_0_200]) ).
cnf(i_0_933,plain,
aux(x(n(z),opt(n(X1))),opt(X2),bfalse) = aux(n(X1),X2,bfalse),
inference(scs_inference,[],[i_0_439,i_0_923,i_0_201]) ).
cnf(i_0_934,plain,
aux(x(n(z),X1),X2,bfalse) = x(X1,X2),
inference(rename_variables,[],[i_0_923]) ).
cnf(i_0_935,plain,
aux(n(X1),X2,bfalse) = aux(x(n(z),opt(n(X1))),opt(X2),bfalse),
inference(scs_inference,[],[i_0_439,i_0_923,i_0_201,i_0_200]) ).
cnf(i_0_936,plain,
aux(x(n(z),opt(X1)),opt(X2),bfalse) = aux(X1,X2,bfalse),
inference(scs_inference,[],[i_0_544,i_0_923,i_0_201]) ).
cnf(i_0_937,plain,
aux(x(n(z),X1),X2,bfalse) = x(X1,X2),
inference(rename_variables,[],[i_0_923]) ).
cnf(i_0_938,plain,
aux(X1,X2,bfalse) = aux(x(n(z),opt(X1)),opt(X2),bfalse),
inference(scs_inference,[],[i_0_544,i_0_923,i_0_201,i_0_200]) ).
cnf(i_0_959,plain,
opt(x(X1,n(z))) = opt(X1),
inference(scs_inference,[],[i_0_958,i_0_546,i_0_201]) ).
cnf(i_0_960,plain,
opt(X1) = opt(x(X1,n(z))),
inference(scs_inference,[],[i_0_958,i_0_546,i_0_201,i_0_200]) ).
cnf(i_0_975,plain,
mulNat(s(X1),z) = mulNat(X1,z),
inference(rename_variables,[],[i_0_972]) ).
cnf(i_0_990,plain,
mulNat(s(X1),z) = mulNat(X1,z),
inference(rename_variables,[],[i_0_972]) ).
cnf(i_0_1009,plain,
fail3(n(s(z)),n(s(z))) = d(X1),
inference(scs_inference,[],[i_0_568,i_0_1008,i_0_201]) ).
cnf(i_0_1010,plain,
fail3(n(s(z)),n(s(X1))) = n(s(X1)),
inference(rename_variables,[],[i_0_1008]) ).
cnf(i_0_1011,plain,
d(X1) = fail3(n(s(z)),n(s(z))),
inference(scs_inference,[],[i_0_568,i_0_1008,i_0_201,i_0_200]) ).
cnf(i_0_1038,plain,
mulNat(s(X1),z) = mulNat(X1,z),
inference(rename_variables,[],[i_0_972]) ).
cnf(i_0_1440,plain,
eq2(X1,X2) = eq2(y(X3,X1),y(X3,X2)),
inference(rename_variables,[],[i_0_822]) ).
cnf(i_0_1899,plain,
eq2(x(x(x(y(X1,X2),X3),X4),X5),x(x(x(x(X6,X7),X8),X9),X10)) = bfalse,
inference(scs_inference,[],[i_0_1815,i_0_135]) ).
cnf(i_0_1901,plain,
eq2(y(x(x(y(X1,X2),X3),X4),X5),y(x(x(x(X6,X7),X8),X9),X10)) = bfalse,
inference(scs_inference,[],[i_0_1815,i_0_135,i_0_136]) ).
cnf(i_0_1939,plain,
eq2(X1,X2) = eq2(y(X3,X1),y(X3,X2)),
inference(rename_variables,[],[i_0_822]) ).
cnf(i_0_1940,plain,
eq2(x(y(x(y(X1,X2),X3),X4),X5),x(y(x(x(X6,X7),X8),X9),X10)) = bfalse,
inference(scs_inference,[],[i_0_1817,i_0_135]) ).
cnf(i_0_1942,plain,
eq2(y(y(x(y(X1,X2),X3),X4),X5),y(y(x(x(X6,X7),X8),X9),X10)) = bfalse,
inference(scs_inference,[],[i_0_1817,i_0_135,i_0_136]) ).
cnf(i_0_1982,plain,
eq2(x(x(y(y(X1,X2),X3),X4),X5),x(x(y(x(X6,X7),X8),X9),X10)) = bfalse,
inference(scs_inference,[],[i_0_1857,i_0_135]) ).
cnf(i_0_1984,plain,
eq2(y(x(y(y(X1,X2),X3),X4),X5),y(x(y(x(X6,X7),X8),X9),X10)) = bfalse,
inference(scs_inference,[],[i_0_1857,i_0_135,i_0_136]) ).
cnf(i_0_2024,plain,
eq2(x(y(y(y(X1,X2),X3),X4),X5),x(y(y(x(X6,X7),X8),X9),X10)) = bfalse,
inference(scs_inference,[],[i_0_1859,i_0_135]) ).
cnf(i_0_2026,plain,
eq2(y(y(y(y(X1,X2),X3),X4),X5),y(y(y(x(X6,X7),X8),X9),X10)) = bfalse,
inference(scs_inference,[],[i_0_1859,i_0_135,i_0_136]) ).
cnf(i_0_2519,plain,
eq2(x(x(x(x(X1,X2),X3),X4),X5),x(x(x(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_2437,i_0_135]) ).
cnf(i_0_2521,plain,
eq2(y(x(x(x(X1,X2),X3),X4),X5),y(x(x(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_2437,i_0_135,i_0_136]) ).
cnf(i_0_2560,plain,
eq2(x(y(x(x(X1,X2),X3),X4),X5),x(y(x(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_2439,i_0_135]) ).
cnf(i_0_2562,plain,
eq2(y(y(x(x(X1,X2),X3),X4),X5),y(y(x(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_2439,i_0_135,i_0_136]) ).
cnf(i_0_2601,plain,
eq2(x(x(y(x(X1,X2),X3),X4),X5),x(x(y(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_2478,i_0_135]) ).
cnf(i_0_2603,plain,
eq2(y(x(y(x(X1,X2),X3),X4),X5),y(x(y(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_2478,i_0_135,i_0_136]) ).
cnf(i_0_2642,plain,
eq2(x(y(y(x(X1,X2),X3),X4),X5),x(y(y(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_2480,i_0_135]) ).
cnf(i_0_2644,plain,
eq2(y(y(y(x(X1,X2),X3),X4),X5),y(y(y(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_2480,i_0_135,i_0_136]) ).
cnf(i_0_3139,plain,
eq2(x(x(x(y(X1,X2),X3),X4),X5),x(x(x(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3056,i_0_135]) ).
cnf(i_0_3141,plain,
eq2(y(x(x(y(X1,X2),X3),X4),X5),y(x(x(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3056,i_0_135,i_0_136]) ).
cnf(i_0_3180,plain,
eq2(x(y(x(y(X1,X2),X3),X4),X5),x(y(x(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3058,i_0_135]) ).
cnf(i_0_3182,plain,
eq2(y(y(x(y(X1,X2),X3),X4),X5),y(y(x(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3058,i_0_135,i_0_136]) ).
cnf(i_0_3222,plain,
eq2(x(x(y(y(X1,X2),X3),X4),X5),x(x(y(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3097,i_0_135]) ).
cnf(i_0_3224,plain,
eq2(y(x(y(y(X1,X2),X3),X4),X5),y(x(y(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3097,i_0_135,i_0_136]) ).
cnf(i_0_3262,plain,
eq2(x(y(y(y(X1,X2),X3),X4),X5),x(y(y(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3099,i_0_135]) ).
cnf(i_0_3264,plain,
eq2(y(y(y(y(X1,X2),X3),X4),X5),y(y(y(n(X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3099,i_0_135,i_0_136]) ).
cnf(i_0_3762,plain,
eq2(x(x(x(n(X1),X2),X3),X4),x(x(x(x(X5,X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3678,i_0_135]) ).
cnf(i_0_3764,plain,
eq2(y(x(x(n(X1),X2),X3),X4),y(x(x(x(X5,X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3678,i_0_135,i_0_136]) ).
cnf(i_0_3804,plain,
eq2(x(y(x(n(X1),X2),X3),X4),x(y(x(x(X5,X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3680,i_0_135]) ).
cnf(i_0_3806,plain,
eq2(y(y(x(n(X1),X2),X3),X4),y(y(x(x(X5,X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3680,i_0_135,i_0_136]) ).
cnf(i_0_3845,plain,
eq2(x(x(y(n(X1),X2),X3),X4),x(x(y(x(X5,X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3720,i_0_135]) ).
cnf(i_0_3847,plain,
eq2(y(x(y(n(X1),X2),X3),X4),y(x(y(x(X5,X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3720,i_0_135,i_0_136]) ).
cnf(i_0_3887,plain,
eq2(x(y(y(n(X1),X2),X3),X4),x(y(y(x(X5,X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3722,i_0_135]) ).
cnf(i_0_3889,plain,
eq2(y(y(y(n(X1),X2),X3),X4),y(y(y(x(X5,X6),X7),X8),X9)) = bfalse,
inference(scs_inference,[],[i_0_3722,i_0_135,i_0_136]) ).
cnf(i_0_249,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(y(X4,x(X5,X2)),y(X4,x(X5,X3))),
inference(scs_inference,[],[i_0_247,i_0_200]) ).
cnf(i_0_250,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,x(X5,X1))),y(X3,x(X4,x(X5,X2)))),
inference(scs_inference,[],[i_0_246,i_0_243,i_0_247,i_0_200,i_0_201]) ).
cnf(i_0_251,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_257,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_270,plain,
eq2(y(X1,x(X2,X3)),y(X1,x(X2,X4))) = eq2(x(X5,X3),x(X5,X4)),
inference(rename_variables,[],[i_0_247]) ).
cnf(i_0_296,plain,
fail12(X1,X1) = fail(fail3(X1,X1),n(z)),
inference(scs_inference,[],[i_0_294,i_0_200]) ).
cnf(i_0_297,plain,
fail(fail3(X1,X1),n(z)) = fail32(X1,X1),
inference(scs_inference,[],[i_0_294,i_0_291,i_0_181,i_0_200,i_0_201]) ).
cnf(i_0_320,plain,
mulNat(s(X1),X2) = fail22(addNat(X2,mulNat(X1,X2)),n(s(z))),
inference(scs_inference,[],[i_0_318,i_0_200]) ).
cnf(i_0_321,plain,
btrue = impl(bfalse,X1),
inference(scs_inference,[],[i_0_317,i_0_312,i_0_318,i_0_200,i_0_201]) ).
cnf(i_0_322,plain,
eq3(X1,X1) = impl(bfalse,X2),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_332,plain,
y(opt(x(X1,X2)),opt(X3)) = addNat(z,y(opt(x(X1,X2)),opt(X3))),
inference(scs_inference,[],[i_0_329,i_0_323,i_0_139,i_0_200,i_0_201]) ).
cnf(i_0_333,plain,
fail32(x(X1,X2),X3) = addNat(z,y(opt(x(X1,X2)),opt(X3))),
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_341,plain,
fail3(x(X1,X2),x(X3,X4)) = fail22(x(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_338,i_0_200]) ).
cnf(i_0_342,plain,
btrue = fail(btrue,n(z)),
inference(scs_inference,[],[i_0_337,i_0_312,i_0_338,i_0_200,i_0_201]) ).
cnf(i_0_343,plain,
eq3(X1,X1) = fail(btrue,n(z)),
inference(rename_variables,[],[i_0_337]) ).
cnf(i_0_352,plain,
fail3(x(X1,X2),y(X3,X4)) = fail22(x(X1,X2),y(X3,X4)),
inference(scs_inference,[],[i_0_349,i_0_200]) ).
cnf(i_0_353,plain,
fail22(y(X1,X2),y(X3,X4)) = fail3(y(X1,X2),y(X3,X4)),
inference(scs_inference,[],[i_0_331,i_0_344,i_0_349,i_0_200,i_0_201]) ).
cnf(i_0_382,plain,
fail22(x(X1,X2),y(X3,X4)) = y(opt(x(X1,X2)),opt(y(X3,X4))),
inference(scs_inference,[],[i_0_379,i_0_200]) ).
cnf(i_0_384,plain,
fail22(x(X1,X2),x(X3,X4)) = y(opt(x(X1,X2)),opt(x(X3,X4))),
inference(rename_variables,[],[i_0_378]) ).
cnf(i_0_426,plain,
eq3(X1,X1) = fail(btrue,n(z)),
inference(rename_variables,[],[i_0_337]) ).
cnf(i_0_441,plain,
eq3(X1,X1) = impl(bfalse,X2),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_479,plain,
fail22(n(X1),n(z)) = n(mulNat(X1,z)),
inference(scs_inference,[],[i_0_476,i_0_200]) ).
cnf(i_0_480,plain,
fail32(n(z),y(X1,X2)) = fail12(n(z),y(X1,X2)),
inference(scs_inference,[],[i_0_374,i_0_469,i_0_476,i_0_200,i_0_201]) ).
cnf(i_0_498,plain,
eq3(btrue,bfalse) = eq2(y(X1,X2),n(X3)),
inference(scs_inference,[],[i_0_497,i_0_200]) ).
cnf(i_0_499,plain,
bfalse = eq2(x(X1,X2),n(X3)),
inference(scs_inference,[],[i_0_496,i_0_460,i_0_497,i_0_200,i_0_201]) ).
cnf(i_0_509,plain,
opt(y(X1,X1)) = fail22(X1,X1),
inference(scs_inference,[],[i_0_507,i_0_200]) ).
cnf(i_0_550,plain,
eq3(btrue,bfalse) = eq2(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_549,i_0_200]) ).
cnf(i_0_551,plain,
bfalse = eq2(y(X1,X2),X3),
inference(scs_inference,[],[i_0_548,i_0_460,i_0_549,i_0_200,i_0_201]) ).
cnf(i_0_558,plain,
fail3(X1,n(z)) = opt(y(n(z),X2)),
inference(scs_inference,[],[i_0_557,i_0_200]) ).
cnf(i_0_559,plain,
d(n(X1)) = opt(y(X2,n(z))),
inference(scs_inference,[],[i_0_556,i_0_502,i_0_557,i_0_200,i_0_201]) ).
cnf(i_0_561,plain,
d(n(X1)) = fail3(X2,n(z)),
inference(rename_variables,[],[i_0_556]) ).
cnf(i_0_575,plain,
d(n(X1)) = opt(n(z)),
inference(rename_variables,[],[i_0_571]) ).
cnf(i_0_581,plain,
d(n(X1)) = opt(n(z)),
inference(rename_variables,[],[i_0_571]) ).
cnf(i_0_636,plain,
fail22(n(X1),x(X2,X3)) = y(opt(n(X1)),opt(x(X2,X3))),
inference(scs_inference,[],[i_0_634,i_0_200]) ).
cnf(i_0_763,plain,
aux(x(x(X1,X2),X3),X4,bfalse) = fail(x(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_760,i_0_200]) ).
cnf(i_0_764,plain,
fail22(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(scs_inference,[],[i_0_743,i_0_286,i_0_760,i_0_200,i_0_201]) ).
cnf(i_0_909,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_964,plain,
fail3(X1,n(z)) = opt(n(z)),
inference(rename_variables,[],[i_0_633]) ).
cnf(i_0_1014,plain,
d(X1) = opt(y(n(s(z)),n(s(z)))),
inference(scs_inference,[],[i_0_1011,i_0_813,i_0_201]) ).
cnf(i_0_1016,plain,
opt(y(n(s(z)),n(s(z)))) = d(X1),
inference(scs_inference,[],[i_0_1011,i_0_813,i_0_201,i_0_200]) ).
cnf(i_0_1068,plain,
d(n(X1)) = fail3(X2,n(z)),
inference(rename_variables,[],[i_0_556]) ).
cnf(i_0_1087,plain,
d(n(X1)) = opt(n(z)),
inference(rename_variables,[],[i_0_571]) ).
cnf(i_0_1097,plain,
d(n(X1)) = fail3(X2,n(z)),
inference(rename_variables,[],[i_0_556]) ).
cnf(i_0_1105,plain,
fail32(x(X1,X2),X3) = addNat(z,y(opt(x(X1,X2)),opt(X3))),
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_1155,plain,
prop2(eq3(X1,X1)) = prop2(eq3(X2,X2)),
inference(scs_inference,[],[i_0_330,i_0_202]) ).
cnf(i_0_1156,plain,
n(eq3(X1,X1)) = n(eq3(X2,X2)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203]) ).
cnf(i_0_1157,plain,
aux(eq3(X1,X1),X2,X3) = aux(eq3(X4,X4),X2,X3),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204]) ).
cnf(i_0_1158,plain,
aux(X1,eq3(X2,X2),X3) = aux(X1,eq3(X4,X4),X3),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205]) ).
cnf(i_0_1159,plain,
aux(X1,X2,eq3(X3,X3)) = aux(X1,X2,eq3(X4,X4)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206]) ).
cnf(i_0_1160,plain,
fail32(eq3(X1,X1),X2) = fail32(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207]) ).
cnf(i_0_1161,plain,
fail32(X1,eq3(X2,X2)) = fail32(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208]) ).
cnf(i_0_1162,plain,
fail(eq3(X1,X1),X2) = fail(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209]) ).
cnf(i_0_1163,plain,
fail(X1,eq3(X2,X2)) = fail(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210]) ).
cnf(i_0_1164,plain,
fail3(eq3(X1,X1),X2) = fail3(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211]) ).
cnf(i_0_1165,plain,
fail3(X1,eq3(X2,X2)) = fail3(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212]) ).
cnf(i_0_1166,plain,
fail12(eq3(X1,X1),X2) = fail12(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213]) ).
cnf(i_0_1167,plain,
fail12(X1,eq3(X2,X2)) = fail12(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214]) ).
cnf(i_0_1168,plain,
s(eq3(X1,X1)) = s(eq3(X2,X2)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215]) ).
cnf(i_0_1169,plain,
fail22(eq3(X1,X1),X2) = fail22(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216]) ).
cnf(i_0_1170,plain,
fail22(X1,eq3(X2,X2)) = fail22(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217]) ).
cnf(i_0_1171,plain,
mulNat(eq3(X1,X1),X2) = mulNat(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218]) ).
cnf(i_0_1172,plain,
mulNat(X1,eq3(X2,X2)) = mulNat(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219]) ).
cnf(i_0_1173,plain,
addNat(eq3(X1,X1),X2) = addNat(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220]) ).
cnf(i_0_1174,plain,
addNat(X1,eq3(X2,X2)) = addNat(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221]) ).
cnf(i_0_1175,plain,
impl(eq3(X1,X1),X2) = impl(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222]) ).
cnf(i_0_1176,plain,
impl(X1,eq3(X2,X2)) = impl(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223]) ).
cnf(i_0_1177,plain,
eq2(eq3(X1,X1),X2) = eq2(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224]) ).
cnf(i_0_1178,plain,
eq2(X1,eq3(X2,X2)) = eq2(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225]) ).
cnf(i_0_1179,plain,
opt(eq3(X1,X1)) = opt(eq3(X2,X2)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226]) ).
cnf(i_0_1180,plain,
d(eq3(X1,X1)) = d(eq3(X2,X2)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227]) ).
cnf(i_0_1181,plain,
x(eq3(X1,X1),X2) = x(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228]) ).
cnf(i_0_1182,plain,
x(X1,eq3(X2,X2)) = x(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229]) ).
cnf(i_0_1183,plain,
y(eq3(X1,X1),X2) = y(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230]) ).
cnf(i_0_1184,plain,
y(X1,eq3(X2,X2)) = y(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231]) ).
cnf(i_0_1185,plain,
fail1(eq3(X1,X1),X2) = fail1(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231,i_0_234]) ).
cnf(i_0_1186,plain,
fail1(X1,eq3(X2,X2)) = fail1(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231,i_0_234,i_0_235]) ).
cnf(i_0_1187,plain,
eq2(x(x(X1,X2),X3),x(y(X4,X5),X6)) = bfalse,
inference(scs_inference,[],[i_0_330,i_0_148,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231,i_0_234,i_0_235,i_0_135]) ).
cnf(i_0_1189,plain,
eq2(y(x(X1,X2),X3),y(y(X4,X5),X6)) = bfalse,
inference(scs_inference,[],[i_0_330,i_0_148,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231,i_0_234,i_0_235,i_0_135,i_0_136]) ).
cnf(i_0_1191,plain,
eq3(X1,eq3(X2,X2)) = eq3(X1,eq3(X3,X3)),
inference(scs_inference,[],[i_0_330,i_0_148,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231,i_0_234,i_0_235,i_0_135,i_0_136,i_0_233]) ).
cnf(i_0_1192,plain,
eq3(eq3(X1,X1),X2) = eq3(eq3(X3,X3),X2),
inference(scs_inference,[],[i_0_330,i_0_148,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231,i_0_234,i_0_235,i_0_135,i_0_136,i_0_233,i_0_232]) ).
cnf(i_0_1193,plain,
btrue != eq3(prop2(X1),bfalse),
inference(scs_inference,[],[i_0_175,i_0_330,i_0_148,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231,i_0_234,i_0_235,i_0_135,i_0_136,i_0_233,i_0_232,i_0_200]) ).
cnf(i_0_1194,plain,
impl(btrue,eq3(prop2(X1),bfalse)) != btrue,
inference(scs_inference,[],[i_0_175,i_0_330,i_0_236,i_0_148,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231,i_0_234,i_0_235,i_0_135,i_0_136,i_0_233,i_0_232,i_0_200,i_0_201]) ).
cnf(i_0_2066,plain,
eq2(x(x(x(x(y(X1,X2),X3),X4),X5),X6),x(x(x(x(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_1899,i_0_135]) ).
cnf(i_0_2068,plain,
eq2(y(x(x(x(y(X1,X2),X3),X4),X5),X6),y(x(x(x(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_1899,i_0_135,i_0_136]) ).
cnf(i_0_2108,plain,
eq2(x(y(x(x(y(X1,X2),X3),X4),X5),X6),x(y(x(x(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_1901,i_0_135]) ).
cnf(i_0_2110,plain,
eq2(y(y(x(x(y(X1,X2),X3),X4),X5),X6),y(y(x(x(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_1901,i_0_135,i_0_136]) ).
cnf(i_0_2150,plain,
eq2(x(x(y(x(y(X1,X2),X3),X4),X5),X6),x(x(y(x(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_1940,i_0_135]) ).
cnf(i_0_2152,plain,
eq2(y(x(y(x(y(X1,X2),X3),X4),X5),X6),y(x(y(x(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_1940,i_0_135,i_0_136]) ).
cnf(i_0_2190,plain,
eq2(x(y(y(x(y(X1,X2),X3),X4),X5),X6),x(y(y(x(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_1942,i_0_135]) ).
cnf(i_0_2192,plain,
eq2(y(y(y(x(y(X1,X2),X3),X4),X5),X6),y(y(y(x(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_1942,i_0_135,i_0_136]) ).
cnf(i_0_2232,plain,
eq2(x(x(x(y(y(X1,X2),X3),X4),X5),X6),x(x(x(y(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_1982,i_0_135]) ).
cnf(i_0_2234,plain,
eq2(y(x(x(y(y(X1,X2),X3),X4),X5),X6),y(x(x(y(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_1982,i_0_135,i_0_136]) ).
cnf(i_0_2273,plain,
eq2(x(y(x(y(y(X1,X2),X3),X4),X5),X6),x(y(x(y(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_1984,i_0_135]) ).
cnf(i_0_2275,plain,
eq2(y(y(x(y(y(X1,X2),X3),X4),X5),X6),y(y(x(y(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_1984,i_0_135,i_0_136]) ).
cnf(i_0_2314,plain,
eq2(x(x(y(y(y(X1,X2),X3),X4),X5),X6),x(x(y(y(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_2024,i_0_135]) ).
cnf(i_0_2316,plain,
eq2(y(x(y(y(y(X1,X2),X3),X4),X5),X6),y(x(y(y(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_2024,i_0_135,i_0_136]) ).
cnf(i_0_2355,plain,
eq2(x(y(y(y(y(X1,X2),X3),X4),X5),X6),x(y(y(y(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_2026,i_0_135]) ).
cnf(i_0_2357,plain,
eq2(y(y(y(y(y(X1,X2),X3),X4),X5),X6),y(y(y(y(x(X7,X8),X9),X10),X11),X12)) = bfalse,
inference(scs_inference,[],[i_0_2026,i_0_135,i_0_136]) ).
cnf(i_0_2932,plain,
eq2(x(x(y(y(x(X1,X2),X3),X4),X5),X6),x(x(y(y(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_2642,i_0_135]) ).
cnf(i_0_2934,plain,
eq2(y(x(y(y(x(X1,X2),X3),X4),X5),X6),y(x(y(y(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_2642,i_0_135,i_0_136]) ).
cnf(i_0_2974,plain,
eq2(x(y(y(y(x(X1,X2),X3),X4),X5),X6),x(y(y(y(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_2644,i_0_135]) ).
cnf(i_0_2976,plain,
eq2(y(y(y(y(x(X1,X2),X3),X4),X5),X6),y(y(y(y(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_2644,i_0_135,i_0_136]) ).
cnf(i_0_3304,plain,
eq2(x(x(x(x(y(X1,X2),X3),X4),X5),X6),x(x(x(x(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3139,i_0_135]) ).
cnf(i_0_3306,plain,
eq2(y(x(x(x(y(X1,X2),X3),X4),X5),X6),y(x(x(x(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3139,i_0_135,i_0_136]) ).
cnf(i_0_3345,plain,
eq2(x(y(x(x(y(X1,X2),X3),X4),X5),X6),x(y(x(x(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3141,i_0_135]) ).
cnf(i_0_3347,plain,
eq2(y(y(x(x(y(X1,X2),X3),X4),X5),X6),y(y(x(x(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3141,i_0_135,i_0_136]) ).
cnf(i_0_3387,plain,
eq2(x(x(y(x(y(X1,X2),X3),X4),X5),X6),x(x(y(x(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3180,i_0_135]) ).
cnf(i_0_3389,plain,
eq2(y(x(y(x(y(X1,X2),X3),X4),X5),X6),y(x(y(x(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3180,i_0_135,i_0_136]) ).
cnf(i_0_3429,plain,
eq2(x(y(y(x(y(X1,X2),X3),X4),X5),X6),x(y(y(x(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3182,i_0_135]) ).
cnf(i_0_3431,plain,
eq2(y(y(y(x(y(X1,X2),X3),X4),X5),X6),y(y(y(x(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3182,i_0_135,i_0_136]) ).
cnf(i_0_3471,plain,
eq2(x(x(x(y(y(X1,X2),X3),X4),X5),X6),x(x(x(y(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3222,i_0_135]) ).
cnf(i_0_3473,plain,
eq2(y(x(x(y(y(X1,X2),X3),X4),X5),X6),y(x(x(y(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3222,i_0_135,i_0_136]) ).
cnf(i_0_3511,plain,
eq2(x(y(x(y(y(X1,X2),X3),X4),X5),X6),x(y(x(y(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3224,i_0_135]) ).
cnf(i_0_3513,plain,
eq2(y(y(x(y(y(X1,X2),X3),X4),X5),X6),y(y(x(y(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3224,i_0_135,i_0_136]) ).
cnf(i_0_3553,plain,
eq2(x(x(y(y(y(X1,X2),X3),X4),X5),X6),x(x(y(y(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3262,i_0_135]) ).
cnf(i_0_3555,plain,
eq2(y(x(y(y(y(X1,X2),X3),X4),X5),X6),y(x(y(y(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3262,i_0_135,i_0_136]) ).
cnf(i_0_3594,plain,
eq2(x(y(y(y(y(X1,X2),X3),X4),X5),X6),x(y(y(y(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3264,i_0_135]) ).
cnf(i_0_3596,plain,
eq2(y(y(y(y(y(X1,X2),X3),X4),X5),X6),y(y(y(y(n(X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3264,i_0_135,i_0_136]) ).
cnf(i_0_3928,plain,
eq2(x(x(x(x(n(X1),X2),X3),X4),X5),x(x(x(x(x(X6,X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3762,i_0_135]) ).
cnf(i_0_3930,plain,
eq2(y(x(x(x(n(X1),X2),X3),X4),X5),y(x(x(x(x(X6,X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3762,i_0_135,i_0_136]) ).
cnf(i_0_3970,plain,
eq2(x(y(x(x(n(X1),X2),X3),X4),X5),x(y(x(x(x(X6,X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3764,i_0_135]) ).
cnf(i_0_3972,plain,
eq2(y(y(x(x(n(X1),X2),X3),X4),X5),y(y(x(x(x(X6,X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3764,i_0_135,i_0_136]) ).
cnf(i_0_4011,plain,
eq2(x(x(y(x(n(X1),X2),X3),X4),X5),x(x(y(x(x(X6,X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3804,i_0_135]) ).
cnf(i_0_4013,plain,
eq2(y(x(y(x(n(X1),X2),X3),X4),X5),y(x(y(x(x(X6,X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3804,i_0_135,i_0_136]) ).
cnf(i_0_4053,plain,
eq2(x(y(y(x(n(X1),X2),X3),X4),X5),x(y(y(x(x(X6,X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3806,i_0_135]) ).
cnf(i_0_4055,plain,
eq2(y(y(y(x(n(X1),X2),X3),X4),X5),y(y(y(x(x(X6,X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3806,i_0_135,i_0_136]) ).
cnf(i_0_4094,plain,
eq2(x(x(x(y(n(X1),X2),X3),X4),X5),x(x(x(y(x(X6,X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3845,i_0_135]) ).
cnf(i_0_4096,plain,
eq2(y(x(x(y(n(X1),X2),X3),X4),X5),y(x(x(y(x(X6,X7),X8),X9),X10),X11)) = bfalse,
inference(scs_inference,[],[i_0_3845,i_0_135,i_0_136]) ).
cnf(i_0_4098,plain,
prop2(fail1(y(X1,X2),X3)) = prop2(aux(y(X1,X2),X3,eq2(y(X1,X2),X3))),
inference(scs_inference,[],[i_0_114,i_0_3845,i_0_135,i_0_136,i_0_202]) ).
cnf(i_0_4099,plain,
n(fail1(y(X1,X2),X3)) = n(aux(y(X1,X2),X3,eq2(y(X1,X2),X3))),
inference(scs_inference,[],[i_0_114,i_0_3845,i_0_135,i_0_136,i_0_202,i_0_203]) ).
cnf(i_0_4100,plain,
aux(fail1(y(X1,X2),X3),X4,X5) = aux(aux(y(X1,X2),X3,eq2(y(X1,X2),X3)),X4,X5),
inference(scs_inference,[],[i_0_114,i_0_3845,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204]) ).
cnf(i_0_4101,plain,
aux(X1,fail1(y(X2,X3),X4),X5) = aux(X1,aux(y(X2,X3),X4,eq2(y(X2,X3),X4)),X5),
inference(scs_inference,[],[i_0_114,i_0_3845,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205]) ).
cnf(i_0_4102,plain,
aux(X1,X2,fail1(y(X3,X4),X5)) = aux(X1,X2,aux(y(X3,X4),X5,eq2(y(X3,X4),X5))),
inference(scs_inference,[],[i_0_114,i_0_3845,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206]) ).
cnf(i_0_4103,plain,
fail32(fail1(y(X1,X2),X3),X4) = fail32(aux(y(X1,X2),X3,eq2(y(X1,X2),X3)),X4),
inference(scs_inference,[],[i_0_114,i_0_3845,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207]) ).
cnf(i_0_4104,plain,
fail32(X1,fail1(y(X2,X3),X4)) = fail32(X1,aux(y(X2,X3),X4,eq2(y(X2,X3),X4))),
inference(scs_inference,[],[i_0_114,i_0_3845,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208]) ).
cnf(i_0_4105,plain,
fail(fail1(y(X1,X2),X3),X4) = fail(aux(y(X1,X2),X3,eq2(y(X1,X2),X3)),X4),
inference(scs_inference,[],[i_0_114,i_0_3845,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209]) ).
cnf(i_0_4106,plain,
fail(X1,fail1(y(X2,X3),X4)) = fail(X1,aux(y(X2,X3),X4,eq2(y(X2,X3),X4))),
inference(scs_inference,[],[i_0_114,i_0_3845,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210]) ).
cnf(i_0_4107,plain,
fail3(fail1(y(X1,X2),X3),X4) = fail3(aux(y(X1,X2),X3,eq2(y(X1,X2),X3)),X4),
inference(scs_inference,[],[i_0_114,i_0_3845,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211]) ).
cnf(c_0_1204,plain,
fail22(X1,X2) = fail12(X1,X2),
i_0_286 ).
cnf(c_0_1205,plain,
fail3(X1,X2) = fail12(X1,X2),
i_0_289 ).
cnf(c_0_1206,plain,
fail22(X1,X2) = fail32(X1,X2),
i_0_298 ).
cnf(c_0_1207,plain,
fail3(X1,X2) = opt(y(X1,X2)),
i_0_502 ).
cnf(c_0_1208,plain,
X1 = opt(X1),
i_0_546 ).
cnf(c_0_1209,plain,
X1 = fail22(X1,n(s(z))),
i_0_874 ).
cnf(c_0_1210,plain,
fail32(X1,X2) = fail3(X1,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1204,c_0_1205]),c_0_1206]) ).
cnf(c_0_1211,plain,
fail3(X1,X2) = y(X1,X2),
inference(rw,[status(thm)],[c_0_1207,c_0_1208]) ).
cnf(c_0_1212,plain,
n(z) = d(n(X1)),
i_0_552 ).
cnf(c_0_1213,plain,
n(s(z)) = d(X1),
i_0_568 ).
cnf(c_0_1214,plain,
n(z) = fail3(X1,n(z)),
i_0_554 ).
cnf(c_0_1215,plain,
X1 = y(X1,n(s(z))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1209,c_0_1206]),c_0_1210]),c_0_1211]) ).
cnf(c_0_1216,plain,
n(z) = n(s(z)),
inference(rw,[status(thm)],[c_0_1212,c_0_1213]) ).
cnf(c_0_1217,plain,
n(z) = y(X1,n(z)),
inference(rw,[status(thm)],[c_0_1214,c_0_1211]) ).
cnf(c_0_1218,plain,
btrue != eq3(prop2(X1),bfalse),
i_0_1193 ).
cnf(c_0_1219,plain,
n(z) = X1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1215,c_0_1216]),c_0_1217]) ).
cnf(c_0_1220,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1218,c_0_1219]),c_0_1219]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX189-1 : TPTP v9.3.0. Released v9.3.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.32 % Computer : n018.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Tue May 5 07:53:47 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 144.35/98.78 % Version : CSE_E---1.7
% 144.35/98.78 % Problem : theBenchmark.p
% 144.35/98.78 % SZS status Unsatisfiable for theBenchmark.p
% 144.35/98.78 % SZS output start CNFRefutation
% See solution above
% 157.05/111.42 % Total time : 98.433s
%------------------------------------------------------------------------------