%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX191-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 : n021.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 128.63s 90.44s
% Output : CNFRefutation 134.63s
% 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,
propm4(X1) = impl(eq2(opt(d(X1)),x(y(x2,y(x2,x2)),y(x2,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(propm4(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,
propm4(X1) = impl(eq2(opt(d(X1)),x(y(x2,y(x2,x2)),y(x2,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(propm4(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
| propm4(X1) = propm4(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(propm4(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_261,plain,
addNat(z,X1) = X1,
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_262,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(scs_inference,[],[i_0_179,i_0_200]) ).
cnf(i_0_263,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_264,plain,
fail12(X1,X2) = fail22(X1,X2),
inference(rename_variables,[],[i_0_179]) ).
cnf(i_0_265,plain,
fail3(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_180]) ).
cnf(i_0_268,plain,
fail(X1,n(z)) = X1,
inference(rename_variables,[],[i_0_186]) ).
cnf(i_0_274,plain,
fail22(X1,X2) = fail32(X1,X2),
inference(rename_variables,[],[i_0_181]) ).
cnf(i_0_277,plain,
fail1(X1,X2) = fail(X1,X2),
inference(scs_inference,[],[i_0_182,i_0_200]) ).
cnf(i_0_281,plain,
opt(x(n(z),X1)) = X1,
inference(rename_variables,[],[i_0_169]) ).
cnf(i_0_284,plain,
fail12(n(s(z)),X1) = X1,
inference(rename_variables,[],[i_0_176]) ).
cnf(i_0_288,plain,
btrue = eq3(X1,X1),
inference(scs_inference,[],[i_0_188,i_0_200]) ).
cnf(i_0_291,plain,
addNat(X1,mulNat(X2,X1)) = mulNat(s(X2),X1),
inference(scs_inference,[],[i_0_152,i_0_200]) ).
cnf(i_0_295,plain,
fail22(X1,n(s(z))) = X1,
inference(rename_variables,[],[i_0_177]) ).
cnf(i_0_299,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_302,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(scs_inference,[],[i_0_138,i_0_200]) ).
cnf(i_0_304,plain,
addNat(z,X1) = X1,
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_307,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(scs_inference,[],[i_0_139,i_0_200]) ).
cnf(i_0_310,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_140,i_0_200]) ).
cnf(i_0_312,plain,
fail(X1,n(z)) = X1,
inference(rename_variables,[],[i_0_186]) ).
cnf(i_0_320,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(scs_inference,[],[i_0_141,i_0_200]) ).
cnf(i_0_340,plain,
opt(x(n(z),X1)) = X1,
inference(rename_variables,[],[i_0_169]) ).
cnf(i_0_343,plain,
fail12(n(s(z)),X1) = X1,
inference(rename_variables,[],[i_0_176]) ).
cnf(i_0_347,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_142,i_0_200]) ).
cnf(i_0_350,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(scs_inference,[],[i_0_143,i_0_200]) ).
cnf(i_0_366,plain,
fail22(X1,n(s(z))) = X1,
inference(rename_variables,[],[i_0_177]) ).
cnf(i_0_369,plain,
impl(btrue,X1) = X1,
inference(rename_variables,[],[i_0_190]) ).
cnf(i_0_373,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_144,i_0_200]) ).
cnf(i_0_380,plain,
addNat(z,X1) = X1,
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_383,plain,
fail(X1,n(z)) = X1,
inference(rename_variables,[],[i_0_186]) ).
cnf(i_0_386,plain,
n(mulNat(X1,X2)) = fail32(n(X1),n(X2)),
inference(scs_inference,[],[i_0_153,i_0_200]) ).
cnf(i_0_390,plain,
opt(n(X1)) = n(X1),
inference(rename_variables,[],[i_0_187]) ).
cnf(i_0_394,plain,
n(addNat(X1,X2)) = fail1(n(X1),n(X2)),
inference(scs_inference,[],[i_0_154,i_0_200]) ).
cnf(i_0_397,plain,
x(d(X1),d(X2)) = d(x(X1,X2)),
inference(scs_inference,[],[i_0_155,i_0_200]) ).
cnf(i_0_405,plain,
s(addNat(X1,X2)) = addNat(s(X1),X2),
inference(scs_inference,[],[i_0_157,i_0_200]) ).
cnf(i_0_413,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_415,plain,
x(opt(n(X1)),opt(X2)) = aux(n(X1),X2,bfalse),
inference(scs_inference,[],[i_0_134,i_0_200]) ).
cnf(i_0_424,plain,
y(n(s(s(z))),opt(X1)) = aux(X1,X2,btrue),
inference(scs_inference,[],[i_0_129,i_0_200]) ).
cnf(i_0_431,plain,
z = mulNat(z,X1),
inference(scs_inference,[],[i_0_194,i_0_200]) ).
cnf(i_0_436,plain,
bfalse = eq3(btrue,bfalse),
inference(scs_inference,[],[i_0_196,i_0_200]) ).
cnf(i_0_445,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(scs_inference,[],[i_0_173,i_0_200]) ).
cnf(i_0_447,plain,
fail32(X1,n(z)) = fail22(X1,n(z)),
inference(scs_inference,[],[i_0_174,i_0_200]) ).
cnf(i_0_470,plain,
y(opt(n(X1)),opt(X2)) = fail32(n(X1),X2),
inference(scs_inference,[],[i_0_156,i_0_200]) ).
cnf(i_0_476,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(scs_inference,[],[i_0_162,i_0_200]) ).
cnf(i_0_478,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(scs_inference,[],[i_0_163,i_0_200]) ).
cnf(i_0_497,plain,
y(opt(X1),opt(X2)) = fail32(X1,X2),
inference(scs_inference,[],[i_0_170,i_0_200]) ).
cnf(i_0_508,plain,
aux(X1,X2,eq2(X1,X2)) = fail1(X1,X2),
inference(scs_inference,[],[i_0_137,i_0_200]) ).
cnf(i_0_520,plain,
x(opt(X1),opt(X2)) = aux(X1,X2,bfalse),
inference(scs_inference,[],[i_0_147,i_0_200]) ).
cnf(i_0_522,plain,
X1 = opt(X1),
inference(scs_inference,[],[i_0_198,i_0_200]) ).
cnf(i_0_528,plain,
n(z) = d(n(X1)),
inference(scs_inference,[],[i_0_192,i_0_200]) ).
cnf(i_0_530,plain,
n(z) = fail3(X1,n(z)),
inference(scs_inference,[],[i_0_183,i_0_200]) ).
cnf(i_0_544,plain,
n(s(z)) = d(X1),
inference(scs_inference,[],[i_0_197,i_0_200]) ).
cnf(i_0_546,plain,
opt(n(X1)) = n(X1),
inference(rename_variables,[],[i_0_187]) ).
cnf(i_0_549,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_564,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_566,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_583,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_585,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_606,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_608,plain,
opt(n(X1)) = n(X1),
inference(rename_variables,[],[i_0_187]) ).
cnf(i_0_631,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_634,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(scs_inference,[],[i_0_119,i_0_200]) ).
cnf(i_0_648,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(scs_inference,[],[i_0_120,i_0_200]) ).
cnf(i_0_651,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(scs_inference,[],[i_0_121,i_0_200]) ).
cnf(i_0_668,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(scs_inference,[],[i_0_122,i_0_200]) ).
cnf(i_0_710,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(scs_inference,[],[i_0_123,i_0_200]) ).
cnf(i_0_719,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_731,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(scs_inference,[],[i_0_150,i_0_200]) ).
cnf(i_0_733,plain,
fail1(X1,n(s(X2))) = fail(X1,n(s(X2))),
inference(scs_inference,[],[i_0_151,i_0_200]) ).
cnf(i_0_752,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_755,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_773,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_776,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_798,plain,
fail(n(s(X1)),X2) = opt(x(n(s(X1)),X2)),
inference(scs_inference,[],[i_0_132,i_0_200]) ).
cnf(i_0_801,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(scs_inference,[],[i_0_133,i_0_200]) ).
cnf(i_0_847,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(scs_inference,[],[i_0_180,i_0_200]) ).
cnf(i_0_863,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(scs_inference,[],[i_0_181,i_0_200]) ).
cnf(i_0_868,plain,
btrue = eq2(X1,X1),
inference(scs_inference,[],[i_0_189,i_0_200]) ).
cnf(i_0_871,plain,
X1 = opt(x(n(z),X1)),
inference(scs_inference,[],[i_0_169,i_0_200]) ).
cnf(i_0_878,plain,
X1 = fail12(n(s(z)),X1),
inference(scs_inference,[],[i_0_176,i_0_200]) ).
cnf(i_0_927,plain,
X1 = fail22(X1,n(s(z))),
inference(scs_inference,[],[i_0_177,i_0_200]) ).
cnf(i_0_983,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_997,plain,
X1 = addNat(z,X1),
inference(scs_inference,[],[i_0_191,i_0_200]) ).
cnf(i_0_1309,plain,
n(X1) = opt(n(X1)),
inference(scs_inference,[],[i_0_187,i_0_200]) ).
cnf(i_0_1312,plain,
X1 = fail(X1,n(z)),
inference(scs_inference,[],[i_0_186,i_0_200]) ).
cnf(i_0_2002,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_2004,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_2808,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_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_266,plain,
fail22(X1,X1) = fail3(X1,X1),
inference(scs_inference,[],[i_0_263,i_0_200]) ).
cnf(i_0_267,plain,
fail(fail3(X1,X1),n(z)) = fail22(X1,X1),
inference(scs_inference,[],[i_0_263,i_0_186,i_0_200,i_0_201]) ).
cnf(i_0_271,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_262]) ).
cnf(i_0_292,plain,
impl(bfalse,X1) = eq3(X2,X2),
inference(scs_inference,[],[i_0_288,i_0_152,i_0_193,i_0_200,i_0_201]) ).
cnf(i_0_303,plain,
addNat(z,y(opt(x(X1,X2)),opt(X3))) = fail32(x(X1,X2),X3),
inference(scs_inference,[],[i_0_299,i_0_138,i_0_191,i_0_200,i_0_201]) ).
cnf(i_0_311,plain,
fail(btrue,n(z)) = eq3(X1,X1),
inference(scs_inference,[],[i_0_288,i_0_140,i_0_186,i_0_200,i_0_201]) ).
cnf(i_0_315,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_310]) ).
cnf(i_0_316,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_302]) ).
cnf(i_0_321,plain,
fail22(y(X1,X2),x(X3,X4)) = fail3(y(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_307,i_0_310,i_0_141,i_0_200,i_0_201]) ).
cnf(i_0_322,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_310]) ).
cnf(i_0_323,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(rename_variables,[],[i_0_307]) ).
cnf(i_0_326,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_320]) ).
cnf(i_0_327,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_302]) ).
cnf(i_0_330,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_320]) ).
cnf(i_0_331,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(rename_variables,[],[i_0_307]) ).
cnf(i_0_334,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_310]) ).
cnf(i_0_335,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_262]) ).
cnf(i_0_351,plain,
y(opt(x(X1,X2)),opt(x(X3,X4))) = fail22(x(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_347,i_0_299,i_0_143,i_0_200,i_0_201]) ).
cnf(i_0_352,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_353,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_299]) ).
cnf(i_0_356,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_350]) ).
cnf(i_0_357,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_299]) ).
cnf(i_0_420,plain,
addNat(X1,mulNat(X2,X1)) = mulNat(s(X2),X1),
inference(rename_variables,[],[i_0_291]) ).
cnf(i_0_421,plain,
s(addNat(X1,X2)) = addNat(s(X1),X2),
inference(rename_variables,[],[i_0_405]) ).
cnf(i_0_427,plain,
s(addNat(X1,X2)) = addNat(s(X1),X2),
inference(rename_variables,[],[i_0_405]) ).
cnf(i_0_430,plain,
y(n(s(s(z))),opt(X1)) = aux(X1,X2,btrue),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_438,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_302]) ).
cnf(i_0_448,plain,
fail32(n(z),x(X1,X2)) = fail12(n(z),x(X1,X2)),
inference(scs_inference,[],[i_0_445,i_0_347,i_0_174,i_0_200,i_0_201]) ).
cnf(i_0_449,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_445]) ).
cnf(i_0_450,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_453,plain,
fail32(X1,n(z)) = fail22(X1,n(z)),
inference(rename_variables,[],[i_0_447]) ).
cnf(i_0_454,plain,
n(mulNat(X1,X2)) = fail32(n(X1),n(X2)),
inference(rename_variables,[],[i_0_386]) ).
cnf(i_0_457,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_445]) ).
cnf(i_0_458,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_350]) ).
cnf(i_0_461,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_445]) ).
cnf(i_0_462,plain,
fail32(X1,n(z)) = fail22(X1,n(z)),
inference(rename_variables,[],[i_0_447]) ).
cnf(i_0_471,plain,
eq2(x(X1,X2),n(X3)) = eq3(btrue,bfalse),
inference(scs_inference,[],[i_0_436,i_0_156,i_0_158,i_0_200,i_0_201]) ).
cnf(i_0_479,plain,
fail1(X1,x(X2,X3)) = opt(x(X1,x(X2,X3))),
inference(scs_inference,[],[i_0_373,i_0_476,i_0_163,i_0_200,i_0_201]) ).
cnf(i_0_480,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(rename_variables,[],[i_0_476]) ).
cnf(i_0_481,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_373]) ).
cnf(i_0_484,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(rename_variables,[],[i_0_478]) ).
cnf(i_0_487,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(rename_variables,[],[i_0_476]) ).
cnf(i_0_501,plain,
y(opt(X1),opt(X2)) = fail32(X1,X2),
inference(rename_variables,[],[i_0_497]) ).
cnf(i_0_512,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_513,plain,
aux(X1,X2,eq2(X1,X2)) = fail1(X1,X2),
inference(rename_variables,[],[i_0_508]) ).
cnf(i_0_523,plain,
eq2(y(X1,X2),X3) = eq3(btrue,bfalse),
inference(scs_inference,[],[i_0_436,i_0_198,i_0_166,i_0_200,i_0_201]) ).
cnf(i_0_531,plain,
fail3(X1,n(z)) = d(n(X2)),
inference(scs_inference,[],[i_0_528,i_0_183,i_0_200,i_0_201]) ).
cnf(i_0_536,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(rename_variables,[],[i_0_478]) ).
cnf(i_0_545,plain,
opt(n(z)) = d(n(X1)),
inference(scs_inference,[],[i_0_528,i_0_197,i_0_187,i_0_200,i_0_201]) ).
cnf(i_0_554,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_373]) ).
cnf(i_0_571,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_373]) ).
cnf(i_0_572,plain,
aux(x(X1,X2),X3,eq2(x(X1,X2),X3)) = fail1(x(X1,X2),X3),
inference(rename_variables,[],[i_0_566]) ).
cnf(i_0_575,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_576,plain,
aux(x(X1,X2),X3,eq2(x(X1,X2),X3)) = fail1(x(X1,X2),X3),
inference(rename_variables,[],[i_0_566]) ).
cnf(i_0_588,plain,
aux(y(X1,X2),X3,eq2(y(X1,X2),X3)) = fail1(y(X1,X2),X3),
inference(rename_variables,[],[i_0_583]) ).
cnf(i_0_591,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_592,plain,
aux(y(X1,X2),X3,eq2(y(X1,X2),X3)) = fail1(y(X1,X2),X3),
inference(rename_variables,[],[i_0_583]) ).
cnf(i_0_599,plain,
aux(X1,X2,eq2(X1,X2)) = fail1(X1,X2),
inference(rename_variables,[],[i_0_508]) ).
cnf(i_0_603,plain,
aux(x(X1,X2),X3,eq2(x(X1,X2),X3)) = fail1(x(X1,X2),X3),
inference(rename_variables,[],[i_0_566]) ).
cnf(i_0_607,plain,
opt(n(z)) = fail3(X1,n(z)),
inference(scs_inference,[],[i_0_530,i_0_117,i_0_187,i_0_200,i_0_201]) ).
cnf(i_0_611,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_628,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_299]) ).
cnf(i_0_635,plain,
y(opt(n(X1)),opt(y(X2,X3))) = fail22(n(X1),y(X2,X3)),
inference(scs_inference,[],[i_0_631,i_0_350,i_0_119,i_0_200,i_0_201]) ).
cnf(i_0_636,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_350]) ).
cnf(i_0_639,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_634]) ).
cnf(i_0_640,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_373]) ).
cnf(i_0_643,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_634]) ).
cnf(i_0_652,plain,
fail1(y(X1,X2),x(X3,X4)) = opt(x(y(X1,X2),x(X3,X4))),
inference(scs_inference,[],[i_0_648,i_0_373,i_0_121,i_0_200,i_0_201]) ).
cnf(i_0_653,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_648]) ).
cnf(i_0_654,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_373]) ).
cnf(i_0_657,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_651]) ).
cnf(i_0_660,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_648]) ).
cnf(i_0_664,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_651]) ).
cnf(i_0_670,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_651]) ).
cnf(i_0_674,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_668]) ).
cnf(i_0_680,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_668]) ).
cnf(i_0_681,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_320]) ).
cnf(i_0_689,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_310]) ).
cnf(i_0_701,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_651]) ).
cnf(i_0_714,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(rename_variables,[],[i_0_710]) ).
cnf(i_0_721,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(rename_variables,[],[i_0_710]) ).
cnf(i_0_725,plain,
eq2(n(X1),n(X2)) = eq2(n(s(X1)),n(s(X2))),
inference(rename_variables,[],[i_0_719]) ).
cnf(i_0_728,plain,
eq2(n(X1),n(X2)) = eq2(n(s(X1)),n(s(X2))),
inference(rename_variables,[],[i_0_719]) ).
cnf(i_0_734,plain,
fail22(y(X1,X2),n(s(X3))) = fail3(y(X1,X2),n(s(X3))),
inference(scs_inference,[],[i_0_731,i_0_307,i_0_151,i_0_200,i_0_201]) ).
cnf(i_0_735,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_731]) ).
cnf(i_0_736,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(rename_variables,[],[i_0_307]) ).
cnf(i_0_739,plain,
fail1(X1,n(s(X2))) = fail(X1,n(s(X2))),
inference(rename_variables,[],[i_0_733]) ).
cnf(i_0_740,plain,
n(addNat(X1,X2)) = fail1(n(X1),n(X2)),
inference(rename_variables,[],[i_0_394]) ).
cnf(i_0_743,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_731]) ).
cnf(i_0_744,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_262]) ).
cnf(i_0_756,plain,
fail(x(X1,X2),x(X3,X4)) = aux(x(x(X1,X2),X3),X4,bfalse),
inference(scs_inference,[],[i_0_752,i_0_634,i_0_128,i_0_200,i_0_201]) ).
cnf(i_0_757,plain,
opt(x(X1,x(X2,X3))) = aux(x(X1,X2),X3,bfalse),
inference(rename_variables,[],[i_0_752]) ).
cnf(i_0_758,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_634]) ).
cnf(i_0_761,plain,
opt(x(X1,x(X2,X3))) = aux(x(X1,X2),X3,bfalse),
inference(rename_variables,[],[i_0_752]) ).
cnf(i_0_762,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_648]) ).
cnf(i_0_778,plain,
fail22(n(s(s(X1))),X2) = fail12(n(s(s(X1))),X2),
inference(rename_variables,[],[i_0_773]) ).
cnf(i_0_782,plain,
fail32(X1,n(s(s(X2)))) = fail22(X1,n(s(s(X2)))),
inference(rename_variables,[],[i_0_776]) ).
cnf(i_0_783,plain,
y(opt(X1),opt(X2)) = fail32(X1,X2),
inference(rename_variables,[],[i_0_497]) ).
cnf(i_0_786,plain,
fail22(n(s(s(X1))),X2) = fail12(n(s(s(X1))),X2),
inference(rename_variables,[],[i_0_773]) ).
cnf(i_0_787,plain,
fail32(X1,n(s(s(X2)))) = fail22(X1,n(s(s(X2)))),
inference(rename_variables,[],[i_0_776]) ).
cnf(i_0_802,plain,
fail1(n(s(X1)),n(s(X2))) = opt(x(n(s(X1)),n(s(X2)))),
inference(scs_inference,[],[i_0_798,i_0_733,i_0_133,i_0_200,i_0_201]) ).
cnf(i_0_803,plain,
fail(n(s(X1)),X2) = opt(x(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_798]) ).
cnf(i_0_804,plain,
fail1(X1,n(s(X2))) = fail(X1,n(s(X2))),
inference(rename_variables,[],[i_0_733]) ).
cnf(i_0_807,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_801]) ).
cnf(i_0_808,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_731]) ).
cnf(i_0_811,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_801]) ).
cnf(i_0_821,plain,
eq2(X1,X2) = eq2(y(X3,X1),y(X3,X2)),
inference(scs_inference,[],[i_0_239,i_0_200]) ).
cnf(i_0_830,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_801]) ).
cnf(i_0_852,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(rename_variables,[],[i_0_847]) ).
cnf(i_0_855,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(rename_variables,[],[i_0_847]) ).
cnf(i_0_867,plain,
eq2(n(X1),n(X2)) = eq2(n(s(X1)),n(s(X2))),
inference(rename_variables,[],[i_0_719]) ).
cnf(i_0_872,plain,
eq3(X1,X1) = eq2(X2,X2),
inference(scs_inference,[],[i_0_868,i_0_188,i_0_169,i_0_200,i_0_201]) ).
cnf(i_0_879,plain,
fail32(n(s(s(X1))),X2) = fail12(n(s(s(X1))),X2),
inference(scs_inference,[],[i_0_863,i_0_773,i_0_176,i_0_200,i_0_201]) ).
cnf(i_0_880,plain,
fail22(n(s(s(X1))),X2) = fail12(n(s(s(X1))),X2),
inference(rename_variables,[],[i_0_773]) ).
cnf(i_0_881,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(rename_variables,[],[i_0_863]) ).
cnf(i_0_884,plain,
opt(x(X1,x(X2,X3))) = aux(x(X1,X2),X3,bfalse),
inference(rename_variables,[],[i_0_752]) ).
cnf(i_0_885,plain,
X1 = opt(x(n(z),X1)),
inference(rename_variables,[],[i_0_871]) ).
cnf(i_0_906,plain,
fail32(X1,n(z)) = fail22(X1,n(z)),
inference(rename_variables,[],[i_0_447]) ).
cnf(i_0_910,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(rename_variables,[],[i_0_476]) ).
cnf(i_0_911,plain,
fail1(X1,n(s(X2))) = fail(X1,n(s(X2))),
inference(rename_variables,[],[i_0_733]) ).
cnf(i_0_922,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(rename_variables,[],[i_0_847]) ).
cnf(i_0_923,plain,
X1 = fail12(n(s(z)),X1),
inference(rename_variables,[],[i_0_878]) ).
cnf(i_0_931,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_302]) ).
cnf(i_0_932,plain,
X1 = fail22(X1,n(s(z))),
inference(rename_variables,[],[i_0_927]) ).
cnf(i_0_935,plain,
fail22(n(s(s(X1))),X2) = fail12(n(s(s(X1))),X2),
inference(rename_variables,[],[i_0_773]) ).
cnf(i_0_936,plain,
X1 = fail22(X1,n(s(z))),
inference(rename_variables,[],[i_0_927]) ).
cnf(i_0_957,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_731]) ).
cnf(i_0_960,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_801]) ).
cnf(i_0_969,plain,
opt(x(X1,x(X2,X3))) = aux(x(X1,X2),X3,bfalse),
inference(rename_variables,[],[i_0_752]) ).
cnf(i_0_970,plain,
fail(n(s(X1)),X2) = opt(x(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_798]) ).
cnf(i_0_995,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_668]) ).
cnf(i_0_1007,plain,
addNat(X1,mulNat(X2,X1)) = mulNat(s(X2),X1),
inference(rename_variables,[],[i_0_291]) ).
cnf(i_0_1008,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_997]) ).
cnf(i_0_1011,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_310]) ).
cnf(i_0_1012,plain,
X1 = fail12(n(s(z)),X1),
inference(rename_variables,[],[i_0_878]) ).
cnf(i_0_1031,plain,
X1 = fail22(X1,n(s(z))),
inference(rename_variables,[],[i_0_927]) ).
cnf(i_0_1043,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_997]) ).
cnf(i_0_1059,plain,
z = mulNat(z,X1),
inference(rename_variables,[],[i_0_431]) ).
cnf(i_0_1107,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_997]) ).
cnf(i_0_1119,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_651]) ).
cnf(i_0_1122,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_731]) ).
cnf(i_0_1125,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_801]) ).
cnf(i_0_1140,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_651]) ).
cnf(i_0_1143,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_731]) ).
cnf(i_0_1158,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_801]) ).
cnf(i_0_1161,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_651]) ).
cnf(i_0_1170,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_801]) ).
cnf(i_0_1173,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_651]) ).
cnf(i_0_1194,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_801]) ).
cnf(i_0_1197,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_1206,plain,
fail3(n(s(X1)),X2) = opt(y(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_801]) ).
cnf(i_0_1227,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(rename_variables,[],[i_0_710]) ).
cnf(i_0_1230,plain,
n(mulNat(X1,X2)) = fail32(n(X1),n(X2)),
inference(rename_variables,[],[i_0_386]) ).
cnf(i_0_1239,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(rename_variables,[],[i_0_863]) ).
cnf(i_0_1243,plain,
fail32(X1,n(z)) = fail22(X1,n(z)),
inference(rename_variables,[],[i_0_447]) ).
cnf(i_0_1254,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_320]) ).
cnf(i_0_1257,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_299]) ).
cnf(i_0_1314,plain,
n(X1) = opt(n(X1)),
inference(rename_variables,[],[i_0_1309]) ).
cnf(i_0_1317,plain,
n(X1) = opt(n(X1)),
inference(rename_variables,[],[i_0_1309]) ).
cnf(i_0_1320,plain,
fail(n(s(X1)),X2) = opt(x(n(s(X1)),X2)),
inference(rename_variables,[],[i_0_798]) ).
cnf(i_0_1324,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_634]) ).
cnf(i_0_1325,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_1312]) ).
cnf(i_0_1328,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(rename_variables,[],[i_0_476]) ).
cnf(i_0_1329,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_1312]) ).
cnf(i_0_1378,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_634]) ).
cnf(i_0_1425,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_1546,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_1587,plain,
X1 = opt(x(n(z),X1)),
inference(rename_variables,[],[i_0_871]) ).
cnf(i_0_2053,plain,
eq2(x(x(y(X1,X2),X3),X4),x(x(x(X5,X6),X7),X8)) = bfalse,
inference(scs_inference,[],[i_0_2002,i_0_135]) ).
cnf(i_0_2055,plain,
eq2(y(x(y(X1,X2),X3),X4),y(x(x(X5,X6),X7),X8)) = bfalse,
inference(scs_inference,[],[i_0_2002,i_0_135,i_0_136]) ).
cnf(i_0_2366,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_2575,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_1312]) ).
cnf(i_0_2625,plain,
X1 = opt(x(n(z),X1)),
inference(rename_variables,[],[i_0_871]) ).
cnf(i_0_2663,plain,
n(X1) = opt(n(X1)),
inference(rename_variables,[],[i_0_1309]) ).
cnf(i_0_2674,plain,
X1 = fail12(n(s(z)),X1),
inference(rename_variables,[],[i_0_878]) ).
cnf(i_0_2712,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_2725,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_997]) ).
cnf(i_0_2761,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_1312]) ).
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_269,plain,
fail22(X1,X1) = fail(fail3(X1,X1),n(z)),
inference(scs_inference,[],[i_0_267,i_0_200]) ).
cnf(i_0_270,plain,
fail(fail3(X1,X1),n(z)) = fail12(X1,X1),
inference(scs_inference,[],[i_0_262,i_0_267,i_0_200,i_0_201]) ).
cnf(i_0_293,plain,
eq3(X1,X1) = impl(bfalse,X2),
inference(scs_inference,[],[i_0_292,i_0_200]) ).
cnf(i_0_294,plain,
fail22(addNat(X1,mulNat(X2,X1)),n(s(z))) = mulNat(s(X2),X1),
inference(scs_inference,[],[i_0_291,i_0_292,i_0_177,i_0_200,i_0_201]) ).
cnf(i_0_305,plain,
fail32(x(X1,X2),X3) = addNat(z,y(opt(x(X1,X2)),opt(X3))),
inference(scs_inference,[],[i_0_303,i_0_200]) ).
cnf(i_0_306,plain,
eq3(X1,X1) = eq3(X2,X2),
inference(scs_inference,[],[i_0_288,i_0_303,i_0_188,i_0_200,i_0_201]) ).
cnf(i_0_313,plain,
eq3(X1,X1) = fail(btrue,n(z)),
inference(scs_inference,[],[i_0_311,i_0_200]) ).
cnf(i_0_314,plain,
fail22(x(X1,X2),x(X3,X4)) = fail3(x(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_302,i_0_310,i_0_311,i_0_200,i_0_201]) ).
cnf(i_0_324,plain,
fail3(y(X1,X2),x(X3,X4)) = fail22(y(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_321,i_0_200]) ).
cnf(i_0_325,plain,
fail22(x(X1,X2),y(X3,X4)) = fail3(x(X1,X2),y(X3,X4)),
inference(scs_inference,[],[i_0_320,i_0_302,i_0_321,i_0_200,i_0_201]) ).
cnf(i_0_354,plain,
fail22(x(X1,X2),x(X3,X4)) = y(opt(x(X1,X2)),opt(x(X3,X4))),
inference(scs_inference,[],[i_0_351,i_0_200]) ).
cnf(i_0_355,plain,
y(opt(x(X1,X2)),opt(y(X3,X4))) = fail22(x(X1,X2),y(X3,X4)),
inference(scs_inference,[],[i_0_350,i_0_299,i_0_351,i_0_200,i_0_201]) ).
cnf(i_0_451,plain,
fail12(n(z),x(X1,X2)) = fail32(n(z),x(X1,X2)),
inference(scs_inference,[],[i_0_448,i_0_200]) ).
cnf(i_0_452,plain,
n(mulNat(X1,z)) = fail22(n(X1),n(z)),
inference(scs_inference,[],[i_0_447,i_0_386,i_0_448,i_0_200,i_0_201]) ).
cnf(i_0_472,plain,
eq3(btrue,bfalse) = eq2(x(X1,X2),n(X3)),
inference(scs_inference,[],[i_0_471,i_0_200]) ).
cnf(i_0_473,plain,
eq2(y(X1,X2),n(X3)) = eq3(btrue,bfalse),
inference(scs_inference,[],[i_0_436,i_0_471,i_0_159,i_0_200,i_0_201]) ).
cnf(i_0_482,plain,
opt(x(X1,x(X2,X3))) = fail1(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_479,i_0_200]) ).
cnf(i_0_483,plain,
fail22(X1,X1) = opt(y(X1,X1)),
inference(scs_inference,[],[i_0_266,i_0_478,i_0_479,i_0_200,i_0_201]) ).
cnf(i_0_524,plain,
eq3(btrue,bfalse) = eq2(y(X1,X2),X3),
inference(scs_inference,[],[i_0_523,i_0_200]) ).
cnf(i_0_525,plain,
eq2(X1,x(X2,X3)) = eq3(btrue,bfalse),
inference(scs_inference,[],[i_0_436,i_0_523,i_0_167,i_0_200,i_0_201]) ).
cnf(i_0_532,plain,
d(n(X1)) = fail3(X2,n(z)),
inference(scs_inference,[],[i_0_531,i_0_200]) ).
cnf(i_0_533,plain,
opt(y(n(z),X1)) = fail3(X2,n(z)),
inference(scs_inference,[],[i_0_530,i_0_531,i_0_164,i_0_200,i_0_201]) ).
cnf(i_0_547,plain,
d(n(X1)) = opt(n(z)),
inference(scs_inference,[],[i_0_545,i_0_200]) ).
cnf(i_0_548,plain,
d(n(X1)) = d(n(X2)),
inference(scs_inference,[],[i_0_528,i_0_545,i_0_192,i_0_200,i_0_201]) ).
cnf(i_0_609,plain,
fail3(X1,n(z)) = opt(n(z)),
inference(scs_inference,[],[i_0_607,i_0_200]) ).
cnf(i_0_610,plain,
y(opt(n(X1)),opt(x(X2,X3))) = fail22(n(X1),x(X2,X3)),
inference(scs_inference,[],[i_0_606,i_0_347,i_0_607,i_0_200,i_0_201]) ).
cnf(i_0_622,plain,
addNat(z,y(opt(x(X1,X2)),opt(X3))) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_637,plain,
fail22(n(X1),y(X2,X3)) = y(opt(n(X1)),opt(y(X2,X3))),
inference(scs_inference,[],[i_0_635,i_0_200]) ).
cnf(i_0_638,plain,
fail1(x(X1,X2),x(X3,X4)) = opt(x(x(X1,X2),x(X3,X4))),
inference(scs_inference,[],[i_0_634,i_0_373,i_0_635,i_0_200,i_0_201]) ).
cnf(i_0_650,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_655,plain,
opt(x(y(X1,X2),x(X3,X4))) = fail1(y(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_652,i_0_200]) ).
cnf(i_0_737,plain,
fail3(y(X1,X2),n(s(X3))) = fail22(y(X1,X2),n(s(X3))),
inference(scs_inference,[],[i_0_734,i_0_200]) ).
cnf(i_0_738,plain,
n(addNat(X1,s(X2))) = fail(n(X1),n(s(X2))),
inference(scs_inference,[],[i_0_394,i_0_733,i_0_734,i_0_200,i_0_201]) ).
cnf(i_0_759,plain,
aux(x(x(X1,X2),X3),X4,bfalse) = fail(x(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_756,i_0_200]) ).
cnf(i_0_760,plain,
fail(y(X1,X2),x(X3,X4)) = aux(x(y(X1,X2),X3),X4,bfalse),
inference(scs_inference,[],[i_0_752,i_0_648,i_0_756,i_0_200,i_0_201]) ).
cnf(i_0_805,plain,
opt(x(n(s(X1)),n(s(X2)))) = fail1(n(s(X1)),n(s(X2))),
inference(scs_inference,[],[i_0_802,i_0_200]) ).
cnf(i_0_806,plain,
fail12(n(s(X1)),n(s(X2))) = opt(y(n(s(X1)),n(s(X2)))),
inference(scs_inference,[],[i_0_801,i_0_731,i_0_802,i_0_200,i_0_201]) ).
cnf(i_0_873,plain,
eq2(X1,X1) = eq3(X2,X2),
inference(scs_inference,[],[i_0_872,i_0_200]) ).
cnf(i_0_874,plain,
impl(bfalse,X1) = eq2(X2,X2),
inference(scs_inference,[],[i_0_868,i_0_872,i_0_193,i_0_200,i_0_201]) ).
cnf(i_0_882,plain,
fail12(n(s(s(X1))),X2) = fail32(n(s(s(X1))),X2),
inference(scs_inference,[],[i_0_879,i_0_200]) ).
cnf(i_0_883,plain,
x(X1,X2) = aux(x(n(z),X1),X2,bfalse),
inference(scs_inference,[],[i_0_871,i_0_752,i_0_879,i_0_200,i_0_201]) ).
cnf(i_0_1628,plain,
eq2(X1,X2) = eq2(y(X3,X1),y(X3,X2)),
inference(rename_variables,[],[i_0_821]) ).
cnf(i_0_2256,plain,
eq2(X1,X2) = eq2(y(X3,X1),y(X3,X2)),
inference(rename_variables,[],[i_0_821]) ).
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_254,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_272,plain,
fail12(X1,X1) = fail(fail3(X1,X1),n(z)),
inference(scs_inference,[],[i_0_270,i_0_200]) ).
cnf(i_0_273,plain,
fail(fail3(X1,X1),n(z)) = fail32(X1,X1),
inference(scs_inference,[],[i_0_270,i_0_267,i_0_181,i_0_200,i_0_201]) ).
cnf(i_0_296,plain,
mulNat(s(X1),X2) = fail22(addNat(X2,mulNat(X1,X2)),n(s(z))),
inference(scs_inference,[],[i_0_294,i_0_200]) ).
cnf(i_0_297,plain,
btrue = impl(bfalse,X1),
inference(scs_inference,[],[i_0_293,i_0_288,i_0_294,i_0_200,i_0_201]) ).
cnf(i_0_298,plain,
eq3(X1,X1) = impl(bfalse,X2),
inference(rename_variables,[],[i_0_293]) ).
cnf(i_0_308,plain,
y(opt(x(X1,X2)),opt(X3)) = addNat(z,y(opt(x(X1,X2)),opt(X3))),
inference(scs_inference,[],[i_0_305,i_0_299,i_0_139,i_0_200,i_0_201]) ).
cnf(i_0_309,plain,
fail32(x(X1,X2),X3) = addNat(z,y(opt(x(X1,X2)),opt(X3))),
inference(rename_variables,[],[i_0_305]) ).
cnf(i_0_317,plain,
fail3(x(X1,X2),x(X3,X4)) = fail22(x(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_314,i_0_200]) ).
cnf(i_0_318,plain,
btrue = fail(btrue,n(z)),
inference(scs_inference,[],[i_0_313,i_0_288,i_0_314,i_0_200,i_0_201]) ).
cnf(i_0_319,plain,
eq3(X1,X1) = fail(btrue,n(z)),
inference(rename_variables,[],[i_0_313]) ).
cnf(i_0_328,plain,
fail3(x(X1,X2),y(X3,X4)) = fail22(x(X1,X2),y(X3,X4)),
inference(scs_inference,[],[i_0_325,i_0_200]) ).
cnf(i_0_329,plain,
fail22(y(X1,X2),y(X3,X4)) = fail3(y(X1,X2),y(X3,X4)),
inference(scs_inference,[],[i_0_307,i_0_320,i_0_325,i_0_200,i_0_201]) ).
cnf(i_0_358,plain,
fail22(x(X1,X2),y(X3,X4)) = y(opt(x(X1,X2)),opt(y(X3,X4))),
inference(scs_inference,[],[i_0_355,i_0_200]) ).
cnf(i_0_360,plain,
fail22(x(X1,X2),x(X3,X4)) = y(opt(x(X1,X2)),opt(x(X3,X4))),
inference(rename_variables,[],[i_0_354]) ).
cnf(i_0_402,plain,
eq3(X1,X1) = fail(btrue,n(z)),
inference(rename_variables,[],[i_0_313]) ).
cnf(i_0_417,plain,
eq3(X1,X1) = impl(bfalse,X2),
inference(rename_variables,[],[i_0_293]) ).
cnf(i_0_455,plain,
fail22(n(X1),n(z)) = n(mulNat(X1,z)),
inference(scs_inference,[],[i_0_452,i_0_200]) ).
cnf(i_0_456,plain,
fail32(n(z),y(X1,X2)) = fail12(n(z),y(X1,X2)),
inference(scs_inference,[],[i_0_350,i_0_445,i_0_452,i_0_200,i_0_201]) ).
cnf(i_0_474,plain,
eq3(btrue,bfalse) = eq2(y(X1,X2),n(X3)),
inference(scs_inference,[],[i_0_473,i_0_200]) ).
cnf(i_0_475,plain,
bfalse = eq2(x(X1,X2),n(X3)),
inference(scs_inference,[],[i_0_472,i_0_436,i_0_473,i_0_200,i_0_201]) ).
cnf(i_0_485,plain,
opt(y(X1,X1)) = fail22(X1,X1),
inference(scs_inference,[],[i_0_483,i_0_200]) ).
cnf(i_0_526,plain,
eq3(btrue,bfalse) = eq2(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_525,i_0_200]) ).
cnf(i_0_527,plain,
bfalse = eq2(y(X1,X2),X3),
inference(scs_inference,[],[i_0_524,i_0_436,i_0_525,i_0_200,i_0_201]) ).
cnf(i_0_534,plain,
fail3(X1,n(z)) = opt(y(n(z),X2)),
inference(scs_inference,[],[i_0_533,i_0_200]) ).
cnf(i_0_535,plain,
d(n(X1)) = opt(y(X2,n(z))),
inference(scs_inference,[],[i_0_532,i_0_478,i_0_533,i_0_200,i_0_201]) ).
cnf(i_0_537,plain,
d(n(X1)) = fail3(X2,n(z)),
inference(rename_variables,[],[i_0_532]) ).
cnf(i_0_551,plain,
d(n(X1)) = opt(n(z)),
inference(rename_variables,[],[i_0_547]) ).
cnf(i_0_557,plain,
d(n(X1)) = opt(n(z)),
inference(rename_variables,[],[i_0_547]) ).
cnf(i_0_612,plain,
fail22(n(X1),x(X2,X3)) = y(opt(n(X1)),opt(x(X2,X3))),
inference(scs_inference,[],[i_0_610,i_0_200]) ).
cnf(i_0_641,plain,
opt(x(x(X1,X2),x(X3,X4))) = fail1(x(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_638,i_0_200]) ).
cnf(i_0_647,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_695,plain,
fail32(x(X1,X2),X3) = addNat(z,y(opt(x(X1,X2)),opt(X3))),
inference(rename_variables,[],[i_0_305]) ).
cnf(i_0_741,plain,
fail(n(X1),n(s(X2))) = n(addNat(X1,s(X2))),
inference(scs_inference,[],[i_0_738,i_0_200]) ).
cnf(c_0_938,plain,
fail22(X1,X2) = fail12(X1,X2),
i_0_262 ).
cnf(c_0_939,plain,
fail3(X1,X2) = fail12(X1,X2),
i_0_265 ).
cnf(c_0_940,plain,
fail22(X1,X2) = fail32(X1,X2),
i_0_274 ).
cnf(c_0_941,plain,
fail3(X1,X2) = opt(y(X1,X2)),
i_0_478 ).
cnf(c_0_942,plain,
X1 = opt(X1),
i_0_522 ).
cnf(c_0_943,plain,
X1 = fail22(X1,n(s(z))),
i_0_927 ).
cnf(c_0_944,plain,
fail32(X1,X2) = fail3(X1,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_938,c_0_939]),c_0_940]) ).
cnf(c_0_945,plain,
fail3(X1,X2) = y(X1,X2),
inference(rw,[status(thm)],[c_0_941,c_0_942]) ).
cnf(c_0_946,plain,
n(z) = d(n(X1)),
i_0_528 ).
cnf(c_0_947,plain,
n(s(z)) = d(X1),
i_0_544 ).
cnf(c_0_948,plain,
n(z) = fail3(X1,n(z)),
i_0_530 ).
cnf(c_0_949,plain,
X1 = y(X1,n(s(z))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_943,c_0_940]),c_0_944]),c_0_945]) ).
cnf(c_0_950,plain,
n(z) = n(s(z)),
inference(rw,[status(thm)],[c_0_946,c_0_947]) ).
cnf(c_0_951,plain,
n(z) = y(X1,n(z)),
inference(rw,[status(thm)],[c_0_948,c_0_945]) ).
cnf(c_0_952,negated_conjecture,
eq3(propm4(X1),bfalse) != btrue,
i_0_175 ).
cnf(c_0_953,plain,
n(z) = X1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_949,c_0_950]),c_0_951]) ).
cnf(c_0_954,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_952,c_0_953]),c_0_953]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX191-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.11 % 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.13/0.32 % Computer : n021.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Tue May 5 07:55:25 EDT 2026
% 0.13/0.32 % CPUTime :
% 0.13/0.33 % start to proof: theBenchmark
% 128.63/90.44 % Version : CSE_E---1.7
% 128.63/90.44 % Problem : theBenchmark.p
% 128.63/90.44 % SZS status Unsatisfiable for theBenchmark.p
% 128.63/90.44 % SZS output start CNFRefutation
% See solution above
% 134.63/96.48 % Total time : 90.090s
%------------------------------------------------------------------------------