%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX193-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n002.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:41 PM UTC 2026
% Result : Unsatisfiable 115.77s 78.90s
% Output : CNFRefutation 120.76s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_93)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_007,axiom,
fail1(n(X1),x(X2,X3)) = fail2(n(X1),x(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_007) ).
cnf(axiom_005,axiom,
fail2(X1,X2) = aux(X1,X2,eq2(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_005) ).
cnf(axiom_008,axiom,
fail1(n(X1),y(X2,X3)) = fail2(n(X1),y(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_008) ).
cnf(axiom_010,axiom,
fail1(x(X1,X2),X3) = fail2(x(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_010) ).
cnf(axiom_011,axiom,
fail1(y(X1,X2),X3) = fail2(y(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_011) ).
cnf(axiom_020,axiom,
fail32(n(X1),x(X2,X3)) = fail4(n(X1),x(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_020) ).
cnf(axiom_018,axiom,
fail4(X1,X2) = y(opt(X1),opt(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_018) ).
cnf(axiom_021,axiom,
fail32(n(X1),y(X2,X3)) = fail4(n(X1),y(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_021) ).
cnf(axiom_024,axiom,
fail32(x(X1,X2),X3) = fail4(x(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_024) ).
cnf(axiom_009,axiom,
fail1(n(X1),x2) = fail2(n(X1),x2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_009) ).
cnf(axiom_012,axiom,
fail1(x2,X1) = fail2(x2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_012) ).
cnf(axiom_085,axiom,
eq(s(X1),s(X2)) = eq(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_085) ).
cnf(axiom_068,axiom,
eq2(n(X1),n(X2)) = eq(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_068) ).
cnf(axiom_022,axiom,
fail32(n(X1),x2) = fail4(n(X1),x2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_022) ).
cnf(axiom_025,axiom,
fail32(x2,X1) = fail4(x2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_025) ).
cnf(axiom_086,axiom,
eq(s(X1),z) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_086) ).
cnf(axiom_087,axiom,
eq(z,s(X1)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_087) ).
cnf(axiom_088,axiom,
eq(X1,X1) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_088) ).
cnf(axiom_065,axiom,
propm6(X1) = impl(eq2(opt(d(X1)),x(y(x2,y(x2,y(x2,y(x2,x2)))),y(x2,x(y(x2,y(x2,y(x2,x2))),y(x2,x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))))))),eq3(btrue,bfalse)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_065) ).
cnf(axiom_001,axiom,
aux(x(X1,X2),X3,bfalse) = opt(x(X1,x(X2,X3))),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',axiom_003) ).
cnf(axiom_055,axiom,
opt(x(x(X1,X2),X3)) = fail(x(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_055) ).
cnf(axiom_056,axiom,
opt(x(y(X1,X2),X3)) = fail(y(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_056) ).
cnf(axiom_060,axiom,
opt(y(x(X1,X2),X3)) = fail3(x(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_060) ).
cnf(axiom_061,axiom,
opt(y(y(X1,X2),X3)) = fail3(y(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_061) ).
cnf(axiom_023,axiom,
fail32(y(X1,X2),X3) = opt(y(X1,y(X2,X3))),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',axiom_047) ).
cnf(axiom_032,axiom,
fail12(n(s(s(X1))),X2) = fail22(n(s(s(X1))),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_032) ).
cnf(axiom_026,axiom,
fail22(X1,n(s(s(X2)))) = fail32(X1,n(s(s(X2)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_026) ).
cnf(axiom,axiom,
aux(X1,X2,btrue) = y(n(s(s(z))),opt(X1)),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',axiom_072) ).
cnf(axiom_053,axiom,
opt(x(n(s(X1)),X2)) = fail(n(s(X1)),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_053) ).
cnf(axiom_058,axiom,
opt(y(n(s(X1)),X2)) = fail3(n(s(X1)),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_058) ).
cnf(axiom_002,axiom,
aux(n(X1),X2,bfalse) = x(opt(n(X1)),opt(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_002) ).
cnf(axiom_069,axiom,
( eq2(x(X1,X3),x(X2,X4)) = bfalse
| eq2(X1,X2) != bfalse ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_069) ).
cnf(axiom_071,axiom,
( eq2(y(X1,X3),y(X2,X4)) = bfalse
| eq2(X1,X2) != bfalse ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_071) ).
cnf(axiom_035,axiom,
fail12(x(X1,X2),X3) = fail22(x(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_035) ).
cnf(axiom_036,axiom,
fail12(y(X1,X2),X3) = fail22(y(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_036) ).
cnf(axiom_040,axiom,
fail3(X1,x(X2,X3)) = fail12(X1,x(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_040) ).
cnf(axiom_041,axiom,
fail3(X1,y(X2,X3)) = fail12(X1,y(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_041) ).
cnf(axiom_029,axiom,
fail22(X1,x(X2,X3)) = fail32(X1,x(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_029) ).
cnf(axiom_030,axiom,
fail22(X1,y(X2,X3)) = fail32(X1,y(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_030) ).
cnf(axiom_015,axiom,
fail(X1,x(X2,X3)) = fail1(X1,x(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_015) ).
cnf(axiom_016,axiom,
fail(X1,y(X2,X3)) = fail1(X1,y(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_016) ).
cnf(axiom_004,axiom,
aux(x2,X1,bfalse) = x(opt(x2),opt(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_004) ).
cnf(axiom_077,axiom,
eq2(x(X1,X2),y(X3,X4)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_077) ).
cnf(axiom_080,axiom,
eq2(y(X1,X2),x(X3,X4)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_080) ).
cnf(axiom_038,axiom,
fail3(X1,n(s(X2))) = fail12(X1,n(s(X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_038) ).
cnf(axiom_013,axiom,
fail(X1,n(s(X2))) = fail1(X1,n(s(X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_013) ).
cnf(axiom_051,axiom,
mulNat(s(X1),X2) = addNat(X2,mulNat(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_051) ).
cnf(axiom_019,axiom,
fail32(n(X1),n(X2)) = n(mulNat(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_019) ).
cnf(axiom_006,axiom,
fail1(n(X1),n(X2)) = n(addNat(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_006) ).
cnf(axiom_046,axiom,
d(x(X1,X2)) = x(d(X1),d(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_046) ).
cnf(axiom_049,axiom,
addNat(s(X1),X2) = s(addNat(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_049) ).
cnf(axiom_076,axiom,
eq2(x(X1,X2),n(X3)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_076) ).
cnf(axiom_079,axiom,
eq2(y(X1,X2),n(X3)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_079) ).
cnf(axiom_073,axiom,
eq2(n(X1),x(X2,X3)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_073) ).
cnf(axiom_074,axiom,
eq2(n(X1),y(X2,X3)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_074) ).
cnf(axiom_057,axiom,
opt(x(x2,X1)) = fail(x2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_057) ).
cnf(axiom_062,axiom,
opt(y(x2,X1)) = fail3(x2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_062) ).
cnf(axiom_059,axiom,
opt(y(n(z),X1)) = n(z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_059) ).
cnf(axiom_078,axiom,
eq2(x(X1,X2),x2) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_078) ).
cnf(axiom_081,axiom,
eq2(y(X1,X2),x2) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_081) ).
cnf(axiom_083,axiom,
eq2(x2,x(X1,X2)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_083) ).
cnf(axiom_084,axiom,
eq2(x2,y(X1,X2)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_084) ).
cnf(axiom_054,axiom,
opt(x(n(z),X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_054) ).
cnf(axiom_034,axiom,
fail12(n(z),X1) = fail22(n(z),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_034) ).
cnf(axiom_028,axiom,
fail22(X1,n(z)) = fail32(X1,n(z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_028) ).
cnf(goal,negated_conjecture,
eq3(propm6(X1),bfalse) != btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
cnf(axiom_033,axiom,
fail12(n(s(z)),X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_033) ).
cnf(axiom_027,axiom,
fail22(X1,n(s(z))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_027) ).
cnf(axiom_037,axiom,
fail12(x2,X1) = fail22(x2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_037) ).
cnf(axiom_042,axiom,
fail3(X1,x2) = fail12(X1,x2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_042) ).
cnf(axiom_031,axiom,
fail22(X1,x2) = fail32(X1,x2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_031) ).
cnf(axiom_017,axiom,
fail(X1,x2) = fail1(X1,x2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_017) ).
cnf(axiom_039,axiom,
fail3(X1,n(z)) = n(z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_039) ).
cnf(axiom_075,axiom,
eq2(n(X1),x2) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_075) ).
cnf(axiom_082,axiom,
eq2(x2,n(X1)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_082) ).
cnf(axiom_014,axiom,
fail(X1,n(z)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_014) ).
cnf(axiom_063,axiom,
opt(n(X1)) = n(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_063) ).
cnf(axiom_090,axiom,
eq3(X1,X1) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_090) ).
cnf(axiom_089,axiom,
eq2(X1,X1) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_089) ).
cnf(axiom_043,axiom,
impl(btrue,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_043) ).
cnf(axiom_050,axiom,
addNat(z,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_050) ).
cnf(axiom_045,axiom,
d(n(X1)) = n(z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_045) ).
cnf(axiom_044,axiom,
impl(bfalse,X1) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_044) ).
cnf(axiom_052,axiom,
mulNat(z,X1) = z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_052) ).
cnf(axiom_066,axiom,
eq3(bfalse,btrue) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_066) ).
cnf(axiom_067,axiom,
eq3(btrue,bfalse) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_067) ).
cnf(axiom_048,axiom,
d(x2) = n(s(z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_048) ).
cnf(axiom_064,axiom,
opt(x2) = x2,
file('/export/starexec/sandbox/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,
propm6(X1) = impl(eq2(opt(d(X1)),x(y(x2,y(x2,y(x2,y(x2,x2)))),y(x2,x(y(x2,y(x2,y(x2,x2))),y(x2,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(propm6(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
| propm6(X1) = propm6(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(propm6(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_262,plain,
X1 = addNat(z,X1),
inference(scs_inference,[],[i_0_191,i_0_200]) ).
cnf(i_0_274,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(scs_inference,[],[i_0_179,i_0_200]) ).
cnf(i_0_277,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(scs_inference,[],[i_0_180,i_0_200]) ).
cnf(i_0_290,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(scs_inference,[],[i_0_181,i_0_200]) ).
cnf(i_0_328,plain,
fail1(X1,X2) = fail(X1,X2),
inference(scs_inference,[],[i_0_182,i_0_200]) ).
cnf(i_0_338,plain,
btrue = eq3(X1,X1),
inference(scs_inference,[],[i_0_188,i_0_200]) ).
cnf(i_0_369,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_396,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(scs_inference,[],[i_0_138,i_0_200]) ).
cnf(i_0_417,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(scs_inference,[],[i_0_139,i_0_200]) ).
cnf(i_0_444,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_140,i_0_200]) ).
cnf(i_0_483,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(scs_inference,[],[i_0_141,i_0_200]) ).
cnf(i_0_486,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_142,i_0_200]) ).
cnf(i_0_521,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(scs_inference,[],[i_0_143,i_0_200]) ).
cnf(i_0_525,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(scs_inference,[],[i_0_144,i_0_200]) ).
cnf(i_0_539,plain,
fail1(X1,y(X2,X3)) = fail(X1,y(X2,X3)),
inference(scs_inference,[],[i_0_145,i_0_200]) ).
cnf(i_0_551,plain,
n(mulNat(X1,X2)) = fail32(n(X1),n(X2)),
inference(scs_inference,[],[i_0_153,i_0_200]) ).
cnf(i_0_554,plain,
n(addNat(X1,X2)) = fail1(n(X1),n(X2)),
inference(scs_inference,[],[i_0_154,i_0_200]) ).
cnf(i_0_566,plain,
x(d(X1),d(X2)) = d(x(X1,X2)),
inference(scs_inference,[],[i_0_155,i_0_200]) ).
cnf(i_0_569,plain,
s(addNat(X1,X2)) = addNat(s(X1),X2),
inference(scs_inference,[],[i_0_157,i_0_200]) ).
cnf(i_0_600,plain,
n(X1) = opt(n(X1)),
inference(scs_inference,[],[i_0_187,i_0_200]) ).
cnf(i_0_603,plain,
X1 = fail(X1,n(z)),
inference(scs_inference,[],[i_0_186,i_0_200]) ).
cnf(i_0_615,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_625,plain,
x(opt(n(X1)),opt(X2)) = aux(n(X1),X2,bfalse),
inference(scs_inference,[],[i_0_134,i_0_200]) ).
cnf(i_0_634,plain,
y(n(s(s(z))),opt(X1)) = aux(X1,X2,btrue),
inference(scs_inference,[],[i_0_129,i_0_200]) ).
cnf(i_0_686,plain,
btrue = impl(bfalse,X1),
inference(scs_inference,[],[i_0_193,i_0_200]) ).
cnf(i_0_690,plain,
z = mulNat(z,X1),
inference(scs_inference,[],[i_0_194,i_0_200]) ).
cnf(i_0_698,plain,
bfalse = eq3(btrue,bfalse),
inference(scs_inference,[],[i_0_196,i_0_200]) ).
cnf(i_0_710,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(scs_inference,[],[i_0_173,i_0_200]) ).
cnf(i_0_761,plain,
fail32(X1,n(z)) = fail22(X1,n(z)),
inference(scs_inference,[],[i_0_174,i_0_200]) ).
cnf(i_0_764,plain,
y(opt(n(X1)),opt(X2)) = fail32(n(X1),X2),
inference(scs_inference,[],[i_0_156,i_0_200]) ).
cnf(i_0_778,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(scs_inference,[],[i_0_162,i_0_200]) ).
cnf(i_0_804,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(scs_inference,[],[i_0_163,i_0_200]) ).
cnf(i_0_808,plain,
y(opt(X1),opt(X2)) = fail32(X1,X2),
inference(scs_inference,[],[i_0_170,i_0_200]) ).
cnf(i_0_823,plain,
aux(X1,X2,eq2(X1,X2)) = fail1(X1,X2),
inference(scs_inference,[],[i_0_137,i_0_200]) ).
cnf(i_0_826,plain,
x(opt(X1),opt(X2)) = aux(X1,X2,bfalse),
inference(scs_inference,[],[i_0_147,i_0_200]) ).
cnf(i_0_847,plain,
bfalse = eq3(bfalse,btrue),
inference(scs_inference,[],[i_0_195,i_0_200]) ).
cnf(i_0_858,plain,
X1 = opt(X1),
inference(scs_inference,[],[i_0_198,i_0_200]) ).
cnf(i_0_861,plain,
n(z) = d(n(X1)),
inference(scs_inference,[],[i_0_192,i_0_200]) ).
cnf(i_0_870,plain,
n(z) = fail3(X1,n(z)),
inference(scs_inference,[],[i_0_183,i_0_200]) ).
cnf(i_0_873,plain,
n(s(z)) = d(X1),
inference(scs_inference,[],[i_0_197,i_0_200]) ).
cnf(i_0_883,plain,
bfalse = eq2(x(X1,X2),y(X3,X4)),
inference(scs_inference,[],[i_0_148,i_0_200]) ).
cnf(i_0_902,plain,
bfalse = eq2(y(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_149,i_0_200]) ).
cnf(i_0_906,plain,
bfalse = eq2(x(X1,X2),n(X3)),
inference(scs_inference,[],[i_0_158,i_0_200]) ).
cnf(i_0_916,plain,
bfalse = eq2(y(X1,X2),n(X3)),
inference(scs_inference,[],[i_0_159,i_0_200]) ).
cnf(i_0_928,plain,
bfalse = eq2(n(X1),x(X2,X3)),
inference(scs_inference,[],[i_0_160,i_0_200]) ).
cnf(i_0_938,plain,
bfalse = eq2(n(X1),y(X2,X3)),
inference(scs_inference,[],[i_0_161,i_0_200]) ).
cnf(i_0_941,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_947,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_953,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_970,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_1005,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_1009,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_1019,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_1059,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(scs_inference,[],[i_0_119,i_0_200]) ).
cnf(i_0_1089,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(scs_inference,[],[i_0_120,i_0_200]) ).
cnf(i_0_1152,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(scs_inference,[],[i_0_121,i_0_200]) ).
cnf(i_0_1155,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(scs_inference,[],[i_0_122,i_0_200]) ).
cnf(i_0_1176,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(scs_inference,[],[i_0_123,i_0_200]) ).
cnf(i_0_1315,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_1333,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(scs_inference,[],[i_0_150,i_0_200]) ).
cnf(i_0_1467,plain,
eq2(x(y(X1,X2),X3),x(X4,X5)) = bfalse,
inference(scs_inference,[],[i_0_166,i_0_135]) ).
cnf(i_0_1469,plain,
eq2(y(y(X1,X2),X3),y(X4,X5)) = bfalse,
inference(scs_inference,[],[i_0_166,i_0_135,i_0_136]) ).
cnf(i_0_1507,plain,
addNat(z,X1) = X1,
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_1508,plain,
eq2(x(X1,X2),x(x(X3,X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_167,i_0_135]) ).
cnf(i_0_1510,plain,
eq2(y(X1,X2),y(x(X3,X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_167,i_0_135,i_0_136]) ).
cnf(i_0_1549,plain,
eq2(x(X1,X2),x(y(X3,X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_168,i_0_135]) ).
cnf(i_0_1551,plain,
eq2(y(X1,X2),y(y(X3,X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_168,i_0_135,i_0_136]) ).
cnf(i_0_1589,plain,
eq2(x(n(X1),X2),x(X3,X4)) = bfalse,
inference(scs_inference,[],[i_0_184,i_0_135]) ).
cnf(i_0_1591,plain,
eq2(y(n(X1),X2),y(X3,X4)) = bfalse,
inference(scs_inference,[],[i_0_184,i_0_135,i_0_136]) ).
cnf(i_0_1629,plain,
eq2(x(X1,X2),x(n(X3),X4)) = bfalse,
inference(scs_inference,[],[i_0_185,i_0_135]) ).
cnf(i_0_1631,plain,
eq2(y(X1,X2),y(n(X3),X4)) = bfalse,
inference(scs_inference,[],[i_0_185,i_0_135,i_0_136]) ).
cnf(i_0_1877,plain,
addNat(z,X1) = X1,
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_2330,plain,
eq3(X1,X1) = btrue,
inference(rename_variables,[],[i_0_188]) ).
cnf(i_0_2561,plain,
eq3(X1,X1) = btrue,
inference(rename_variables,[],[i_0_188]) ).
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_267,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_262]) ).
cnf(i_0_282,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_283,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_274]) ).
cnf(i_0_292,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_262]) ).
cnf(i_0_359,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_262]) ).
cnf(i_0_377,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(rename_variables,[],[i_0_290]) ).
cnf(i_0_378,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_369]) ).
cnf(i_0_401,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_396]) ).
cnf(i_0_402,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(rename_variables,[],[i_0_290]) ).
cnf(i_0_411,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_412,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_396]) ).
cnf(i_0_422,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(rename_variables,[],[i_0_417]) ).
cnf(i_0_423,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(rename_variables,[],[i_0_290]) ).
cnf(i_0_430,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_450,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_444]) ).
cnf(i_0_451,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(rename_variables,[],[i_0_417]) ).
cnf(i_0_457,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_444]) ).
cnf(i_0_458,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_396]) ).
cnf(i_0_487,plain,
fail22(y(X1,X2),y(X3,X4)) = fail3(y(X1,X2),y(X3,X4)),
inference(scs_inference,[],[i_0_483,i_0_417,i_0_142,i_0_200,i_0_201]) ).
cnf(i_0_488,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_483]) ).
cnf(i_0_489,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(rename_variables,[],[i_0_417]) ).
cnf(i_0_492,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_486]) ).
cnf(i_0_493,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_369]) ).
cnf(i_0_496,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_483]) ).
cnf(i_0_497,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_274]) ).
cnf(i_0_503,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_483]) ).
cnf(i_0_504,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_396]) ).
cnf(i_0_526,plain,
y(opt(x(X1,X2)),opt(y(X3,X4))) = fail22(x(X1,X2),y(X3,X4)),
inference(scs_inference,[],[i_0_521,i_0_369,i_0_144,i_0_200,i_0_201]) ).
cnf(i_0_527,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_521]) ).
cnf(i_0_528,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_369]) ).
cnf(i_0_578,plain,
s(addNat(X1,X2)) = addNat(s(X1),X2),
inference(rename_variables,[],[i_0_569]) ).
cnf(i_0_608,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_603]) ).
cnf(i_0_611,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_603]) ).
cnf(i_0_715,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_710]) ).
cnf(i_0_716,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_486]) ).
cnf(i_0_722,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_710]) ).
cnf(i_0_723,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_521]) ).
cnf(i_0_729,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_444]) ).
cnf(i_0_730,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_710]) ).
cnf(i_0_765,plain,
n(mulNat(X1,z)) = fail22(n(X1),n(z)),
inference(scs_inference,[],[i_0_761,i_0_551,i_0_156,i_0_200,i_0_201]) ).
cnf(i_0_766,plain,
fail32(X1,n(z)) = fail22(X1,n(z)),
inference(rename_variables,[],[i_0_761]) ).
cnf(i_0_767,plain,
n(mulNat(X1,X2)) = fail32(n(X1),n(X2)),
inference(rename_variables,[],[i_0_551]) ).
cnf(i_0_773,plain,
n(X1) = opt(n(X1)),
inference(rename_variables,[],[i_0_600]) ).
cnf(i_0_780,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_710]) ).
cnf(i_0_784,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(rename_variables,[],[i_0_778]) ).
cnf(i_0_785,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_525]) ).
cnf(i_0_791,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(rename_variables,[],[i_0_778]) ).
cnf(i_0_792,plain,
fail1(X1,y(X2,X3)) = fail(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_539]) ).
cnf(i_0_798,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(rename_variables,[],[i_0_778]) ).
cnf(i_0_799,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_810,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(rename_variables,[],[i_0_804]) ).
cnf(i_0_843,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_262]) ).
cnf(i_0_948,plain,
aux(n(X1),x(X2,X3),eq2(n(X1),x(X2,X3))) = fail(n(X1),x(X2,X3)),
inference(scs_inference,[],[i_0_941,i_0_525,i_0_112,i_0_200,i_0_201]) ).
cnf(i_0_949,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_525]) ).
cnf(i_0_954,plain,
aux(n(X1),y(X2,X3),eq2(n(X1),y(X2,X3))) = fail(n(X1),y(X2,X3)),
inference(scs_inference,[],[i_0_947,i_0_539,i_0_113,i_0_200,i_0_201]) ).
cnf(i_0_955,plain,
fail1(X1,y(X2,X3)) = fail(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_539]) ).
cnf(i_0_964,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_965,plain,
aux(x(X1,X2),X3,eq2(x(X1,X2),X3)) = fail1(x(X1,X2),X3),
inference(rename_variables,[],[i_0_953]) ).
cnf(i_0_971,plain,
fail1(n(X1),x(X2,X3)) = fail(aux(n(X1),x(X2,X3),eq2(n(X1),x(X2,X3))),n(z)),
inference(scs_inference,[],[i_0_111,i_0_603,i_0_114,i_0_200,i_0_201]) ).
cnf(i_0_972,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_603]) ).
cnf(i_0_978,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_525]) ).
cnf(i_0_981,plain,
fail1(X1,y(X2,X3)) = fail(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_539]) ).
cnf(i_0_982,plain,
aux(y(X1,X2),X3,eq2(y(X1,X2),X3)) = fail1(y(X1,X2),X3),
inference(rename_variables,[],[i_0_970]) ).
cnf(i_0_988,plain,
fail(X1,X2) = opt(x(X1,X2)),
inference(rename_variables,[],[i_0_778]) ).
cnf(i_0_989,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_603]) ).
cnf(i_0_1027,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_486]) ).
cnf(i_0_1036,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_521]) ).
cnf(i_0_1039,plain,
fail12(X1,x(X2,X3)) = fail3(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_444]) ).
cnf(i_0_1042,plain,
fail12(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_483]) ).
cnf(i_0_1064,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_1059]) ).
cnf(i_0_1065,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_1068,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_1059]) ).
cnf(i_0_1069,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_525]) ).
cnf(i_0_1078,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_1059]) ).
cnf(i_0_1079,plain,
fail1(X1,y(X2,X3)) = fail(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_539]) ).
cnf(i_0_1090,plain,
x(X1,X2) = opt(x(x(X1,X2),n(z))),
inference(scs_inference,[],[i_0_1059,i_0_603,i_0_120,i_0_200,i_0_201]) ).
cnf(i_0_1091,plain,
fail(x(X1,X2),X3) = opt(x(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_1059]) ).
cnf(i_0_1092,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_603]) ).
cnf(i_0_1095,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_1089]) ).
cnf(i_0_1096,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_1108,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_1089]) ).
cnf(i_0_1109,plain,
fail1(X1,x(X2,X3)) = fail(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_525]) ).
cnf(i_0_1124,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_1089]) ).
cnf(i_0_1125,plain,
fail1(X1,y(X2,X3)) = fail(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_539]) ).
cnf(i_0_1128,plain,
fail(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_1089]) ).
cnf(i_0_1129,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_603]) ).
cnf(i_0_1157,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_1152]) ).
cnf(i_0_1160,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_1155]) ).
cnf(i_0_1163,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_1152]) ).
cnf(i_0_1166,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_1155]) ).
cnf(i_0_1169,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_369]) ).
cnf(i_0_1172,plain,
y(opt(x(X1,X2)),opt(X3)) = fail32(x(X1,X2),X3),
inference(rename_variables,[],[i_0_369]) ).
cnf(i_0_1182,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(rename_variables,[],[i_0_1176]) ).
cnf(i_0_1201,plain,
fail32(X1,x(X2,X3)) = fail22(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_486]) ).
cnf(i_0_1212,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_521]) ).
cnf(i_0_1213,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(rename_variables,[],[i_0_1176]) ).
cnf(i_0_1216,plain,
fail3(y(X1,X2),X3) = opt(y(y(X1,X2),X3)),
inference(rename_variables,[],[i_0_1155]) ).
cnf(i_0_1231,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(rename_variables,[],[i_0_804]) ).
cnf(i_0_1252,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(rename_variables,[],[i_0_1176]) ).
cnf(i_0_1285,plain,
fail3(x(X1,X2),X3) = opt(y(x(X1,X2),X3)),
inference(rename_variables,[],[i_0_1152]) ).
cnf(i_0_1311,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(rename_variables,[],[i_0_417]) ).
cnf(i_0_1338,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_1333]) ).
cnf(i_0_1339,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_274]) ).
cnf(i_0_1342,plain,
eq2(n(X1),n(X2)) = eq2(n(s(X1)),n(s(X2))),
inference(rename_variables,[],[i_0_1315]) ).
cnf(i_0_1345,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_1333]) ).
cnf(i_0_1346,plain,
fail22(x(X1,X2),X3) = fail12(x(X1,X2),X3),
inference(rename_variables,[],[i_0_396]) ).
cnf(i_0_1349,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_1333]) ).
cnf(i_0_1350,plain,
fail22(y(X1,X2),X3) = fail12(y(X1,X2),X3),
inference(rename_variables,[],[i_0_417]) ).
cnf(i_0_1359,plain,
eq2(n(X1),n(X2)) = eq2(n(s(X1)),n(s(X2))),
inference(rename_variables,[],[i_0_1315]) ).
cnf(i_0_1368,plain,
eq2(n(X1),n(X2)) = eq2(n(s(X1)),n(s(X2))),
inference(rename_variables,[],[i_0_1315]) ).
cnf(i_0_1371,plain,
fail12(X1,n(s(X2))) = fail3(X1,n(s(X2))),
inference(rename_variables,[],[i_0_1333]) ).
cnf(i_0_1372,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_710]) ).
cnf(i_0_1381,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_262]) ).
cnf(i_0_1395,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_1412,plain,
opt(y(X1,y(X2,X3))) = fail32(y(X1,X2),X3),
inference(rename_variables,[],[i_0_1176]) ).
cnf(i_0_1548,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_1749,plain,
eq2(x(x(y(X1,X2),X3),X4),x(x(X5,X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_1467,i_0_135]) ).
cnf(i_0_1751,plain,
eq2(y(x(y(X1,X2),X3),X4),y(x(X5,X6),X7)) = bfalse,
inference(scs_inference,[],[i_0_1467,i_0_135,i_0_136]) ).
cnf(i_0_2275,plain,
n(X1) = opt(n(X1)),
inference(rename_variables,[],[i_0_600]) ).
cnf(i_0_2284,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_2333,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_2428,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_2468,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_262]) ).
cnf(i_0_2516,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_2524,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_262]) ).
cnf(i_0_2564,plain,
X1 = fail(X1,n(z)),
inference(rename_variables,[],[i_0_603]) ).
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_289,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_388,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_490,plain,
fail3(y(X1,X2),y(X3,X4)) = fail22(y(X1,X2),y(X3,X4)),
inference(scs_inference,[],[i_0_487,i_0_200]) ).
cnf(i_0_491,plain,
y(opt(x(X1,X2)),opt(x(X3,X4))) = fail22(x(X1,X2),x(X3,X4)),
inference(scs_inference,[],[i_0_486,i_0_369,i_0_487,i_0_200,i_0_201]) ).
cnf(i_0_529,plain,
fail22(x(X1,X2),y(X3,X4)) = y(opt(x(X1,X2)),opt(y(X3,X4))),
inference(scs_inference,[],[i_0_526,i_0_200]) ).
cnf(i_0_768,plain,
fail22(n(X1),n(z)) = n(mulNat(X1,z)),
inference(scs_inference,[],[i_0_765,i_0_200]) ).
cnf(i_0_819,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_846,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_950,plain,
fail(n(X1),x(X2,X3)) = aux(n(X1),x(X2,X3),eq2(n(X1),x(X2,X3))),
inference(scs_inference,[],[i_0_948,i_0_200]) ).
cnf(i_0_956,plain,
fail(n(X1),y(X2,X3)) = aux(n(X1),y(X2,X3),eq2(n(X1),y(X2,X3))),
inference(scs_inference,[],[i_0_954,i_0_200]) ).
cnf(i_0_973,plain,
fail(aux(n(X1),x(X2,X3),eq2(n(X1),x(X2,X3))),n(z)) = fail1(n(X1),x(X2,X3)),
inference(scs_inference,[],[i_0_971,i_0_200]) ).
cnf(i_0_1093,plain,
opt(x(x(X1,X2),n(z))) = x(X1,X2),
inference(scs_inference,[],[i_0_1090,i_0_200]) ).
cnf(i_0_1094,plain,
fail1(y(X1,X2),X3) = opt(x(y(X1,X2),X3)),
inference(scs_inference,[],[i_0_1089,i_0_328,i_0_1090,i_0_200,i_0_201]) ).
cnf(i_0_2619,plain,
x(X1,X2) = opt(x(x(X1,X2),n(z))),
inference(rename_variables,[],[i_0_1090]) ).
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_298,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_468,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_494,plain,
fail22(x(X1,X2),x(X3,X4)) = y(opt(x(X1,X2)),opt(x(X3,X4))),
inference(scs_inference,[],[i_0_491,i_0_200]) ).
cnf(i_0_495,plain,
fail22(X1,y(X2,X3)) = fail3(X1,y(X2,X3)),
inference(scs_inference,[],[i_0_483,i_0_274,i_0_491,i_0_200,i_0_201]) ).
cnf(i_0_534,plain,
fail22(x(X1,X2),y(X3,X4)) = y(opt(x(X1,X2)),opt(y(X3,X4))),
inference(rename_variables,[],[i_0_529]) ).
cnf(i_0_637,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1097,plain,
opt(x(y(X1,X2),X3)) = fail1(y(X1,X2),X3),
inference(scs_inference,[],[i_0_1094,i_0_200]) ).
cnf(i_0_1098,plain,
opt(x(x(y(d(X1),X2),y(X1,d(X2))),n(z))) = d(y(X1,X2)),
inference(scs_inference,[],[i_0_1093,i_0_1005,i_0_1094,i_0_200,i_0_201]) ).
cnf(i_0_1099,plain,
opt(x(x(X1,X2),n(z))) = x(X1,X2),
inference(rename_variables,[],[i_0_1093]) ).
cnf(i_0_1105,plain,
opt(x(x(X1,X2),n(z))) = x(X1,X2),
inference(rename_variables,[],[i_0_1093]) ).
cnf(i_0_1112,plain,
opt(x(x(X1,X2),n(z))) = x(X1,X2),
inference(rename_variables,[],[i_0_1093]) ).
cnf(i_0_1115,plain,
opt(x(x(X1,X2),n(z))) = x(X1,X2),
inference(rename_variables,[],[i_0_1093]) ).
cnf(i_0_1121,plain,
opt(x(x(X1,X2),n(z))) = x(X1,X2),
inference(rename_variables,[],[i_0_1093]) ).
cnf(i_0_1248,plain,
fail3(y(X1,X2),y(X3,X4)) = fail22(y(X1,X2),y(X3,X4)),
inference(rename_variables,[],[i_0_490]) ).
cnf(i_0_1265,plain,
fail22(x(X1,X2),y(X3,X4)) = y(opt(x(X1,X2)),opt(y(X3,X4))),
inference(rename_variables,[],[i_0_529]) ).
cnf(i_0_1392,plain,
fail3(y(X1,X2),y(X3,X4)) = fail22(y(X1,X2),y(X3,X4)),
inference(rename_variables,[],[i_0_490]) ).
cnf(i_0_252,plain,
eq2(y(X1,x(X2,x(X3,X4))),y(X1,x(X2,x(X3,X5)))) = eq2(X4,X5),
inference(scs_inference,[],[i_0_250,i_0_200]) ).
cnf(i_0_253,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(y(X4,x(X5,y(X6,x(X7,X2)))),y(X4,x(X5,y(X6,x(X7,X3))))),
inference(scs_inference,[],[i_0_249,i_0_246,i_0_250,i_0_200,i_0_201]) ).
cnf(i_0_258,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(y(X4,x(X5,X2)),y(X4,x(X5,X3))),
inference(rename_variables,[],[i_0_249]) ).
cnf(i_0_461,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(y(X4,x(X5,X2)),y(X4,x(X5,X3))),
inference(rename_variables,[],[i_0_249]) ).
cnf(i_0_498,plain,
fail3(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(scs_inference,[],[i_0_495,i_0_200]) ).
cnf(i_0_500,plain,
fail22(x(X1,X2),x(X3,X4)) = y(opt(x(X1,X2)),opt(x(X3,X4))),
inference(rename_variables,[],[i_0_494]) ).
cnf(i_0_562,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(y(X4,x(X5,X2)),y(X4,x(X5,X3))),
inference(rename_variables,[],[i_0_249]) ).
cnf(i_0_1100,plain,
d(y(X1,X2)) = opt(x(x(y(d(X1),X2),y(X1,d(X2))),n(z))),
inference(scs_inference,[],[i_0_1098,i_0_200]) ).
cnf(i_0_2610,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,x(X5,X1))),y(X3,x(X4,x(X5,X2)))),
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_255,plain,
eq2(y(X1,x(X2,y(X3,x(X4,X5)))),y(X1,x(X2,y(X3,x(X4,X6))))) = eq2(x(X7,X5),x(X7,X6)),
inference(scs_inference,[],[i_0_253,i_0_200]) ).
cnf(i_0_256,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(X3,X4),
inference(scs_inference,[],[i_0_252,i_0_249,i_0_253,i_0_200,i_0_201]) ).
cnf(i_0_257,plain,
eq2(y(X1,x(X2,x(X3,X4))),y(X1,x(X2,x(X3,X5)))) = eq2(X4,X5),
inference(rename_variables,[],[i_0_252]) ).
cnf(i_0_261,plain,
eq2(y(X1,x(X2,x(X3,X4))),y(X1,x(X2,x(X3,X5)))) = eq2(X4,X5),
inference(rename_variables,[],[i_0_252]) ).
cnf(i_0_313,plain,
eq2(y(X1,x(X2,x(X3,X4))),y(X1,x(X2,x(X3,X5)))) = eq2(X4,X5),
inference(rename_variables,[],[i_0_252]) ).
cnf(i_0_633,plain,
eq2(y(X1,x(X2,x(X3,X4))),y(X1,x(X2,x(X3,X5)))) = eq2(X4,X5),
inference(rename_variables,[],[i_0_252]) ).
cnf(i_0_816,plain,
eq2(y(X1,x(X2,x(X3,X4))),y(X1,x(X2,x(X3,X5)))) = eq2(X4,X5),
inference(rename_variables,[],[i_0_252]) ).
cnf(i_0_1238,plain,
fail3(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_498]) ).
cnf(i_0_1320,plain,
eq2(y(X1,x(X2,x(X3,X4))),y(X1,x(X2,x(X3,X5)))) = eq2(X4,X5),
inference(rename_variables,[],[i_0_252]) ).
cnf(i_0_259,plain,
eq2(X1,X2) = eq2(x(X3,x(X4,X1)),x(X3,x(X4,X2))),
inference(scs_inference,[],[i_0_256,i_0_200]) ).
cnf(i_0_327,plain,
eq2(y(X1,x(X2,y(X3,x(X4,X5)))),y(X1,x(X2,y(X3,x(X4,X6))))) = eq2(x(X7,X5),x(X7,X6)),
inference(rename_variables,[],[i_0_255]) ).
cnf(i_0_664,plain,
eq2(y(X1,x(X2,y(X3,x(X4,X5)))),y(X1,x(X2,y(X3,x(X4,X6))))) = eq2(x(X7,X5),x(X7,X6)),
inference(rename_variables,[],[i_0_255]) ).
cnf(i_0_712,plain,
eq2(y(X1,x(X2,y(X3,x(X4,X5)))),y(X1,x(X2,y(X3,x(X4,X6))))) = eq2(x(X7,X5),x(X7,X6)),
inference(rename_variables,[],[i_0_255]) ).
cnf(i_0_264,plain,
eq2(X1,X2) = eq2(x(X3,x(X4,X1)),x(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_259]) ).
cnf(c_0_884,plain,
fail22(X1,X2) = fail12(X1,X2),
i_0_274 ).
cnf(c_0_885,plain,
fail12(X1,X2) = fail3(X1,X2),
i_0_277 ).
cnf(c_0_886,plain,
fail32(X1,X2) = fail22(X1,X2),
i_0_290 ).
cnf(c_0_887,plain,
fail3(X1,X2) = opt(y(X1,X2)),
i_0_804 ).
cnf(c_0_888,plain,
X1 = opt(X1),
i_0_858 ).
cnf(c_0_889,axiom,
fail22(X1,n(s(z))) = X1,
i_0_177 ).
cnf(c_0_890,plain,
fail32(X1,X2) = fail3(X1,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_884,c_0_885]),c_0_886]) ).
cnf(c_0_891,plain,
fail3(X1,X2) = y(X1,X2),
inference(rw,[status(thm)],[c_0_887,c_0_888]) ).
cnf(c_0_892,plain,
n(z) = d(n(X1)),
i_0_861 ).
cnf(c_0_893,plain,
n(s(z)) = d(X1),
i_0_873 ).
cnf(c_0_894,plain,
n(z) = fail3(X1,n(z)),
i_0_870 ).
cnf(c_0_895,plain,
y(X1,n(s(z))) = X1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_889,c_0_886]),c_0_890]),c_0_891]) ).
cnf(c_0_896,plain,
n(z) = n(s(z)),
inference(rw,[status(thm)],[c_0_892,c_0_893]) ).
cnf(c_0_897,plain,
n(z) = y(X1,n(z)),
inference(rw,[status(thm)],[c_0_894,c_0_891]) ).
cnf(c_0_898,negated_conjecture,
eq3(propm6(X1),bfalse) != btrue,
i_0_175 ).
cnf(c_0_899,plain,
n(z) = X1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_895,c_0_896]),c_0_897]) ).
cnf(c_0_900,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_898,c_0_899]),c_0_899]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX193-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.33 % Computer : n002.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue May 5 07:55:01 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.35 % start to proof: theBenchmark
% 115.77/78.90 % Version : CSE_E---1.7
% 115.77/78.90 % Problem : theBenchmark.p
% 115.77/78.90 % SZS status Unsatisfiable for theBenchmark.p
% 115.77/78.90 % SZS output start CNFRefutation
% See solution above
% 120.76/83.98 % Total time : 78.542s
%------------------------------------------------------------------------------