%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX192-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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:34:41 PM UTC 2026
% Result : Unsatisfiable 124.14s 87.48s
% Output : CNFRefutation 130.54s
% 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,
propm5(X1) = impl(eq2(opt(d(X1)),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(propm5(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,
propm5(X1) = impl(eq2(opt(d(X1)),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(propm5(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
| propm5(X1) = propm5(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(propm5(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_323,plain,
X1 = addNat(z,X1),
inference(scs_inference,[],[i_0_191,i_0_200]) ).
cnf(i_0_335,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(scs_inference,[],[i_0_179,i_0_200]) ).
cnf(i_0_338,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(scs_inference,[],[i_0_180,i_0_200]) ).
cnf(i_0_371,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(scs_inference,[],[i_0_181,i_0_200]) ).
cnf(i_0_381,plain,
fail1(X1,X2) = fail(X1,X2),
inference(scs_inference,[],[i_0_182,i_0_200]) ).
cnf(i_0_536,plain,
btrue = eq3(X1,X1),
inference(scs_inference,[],[i_0_188,i_0_200]) ).
cnf(i_0_648,plain,
fail22(X1,x(X2,X3)) = fail32(X1,x(X2,X3)),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_668,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(scs_inference,[],[i_0_143,i_0_200]) ).
cnf(i_0_854,plain,
fail(X1,n(z)) = X1,
inference(rename_variables,[],[i_0_186]) ).
cnf(i_0_855,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_894,plain,
btrue = impl(bfalse,X1),
inference(scs_inference,[],[i_0_193,i_0_200]) ).
cnf(i_0_895,plain,
eq3(propm5(X1),bfalse) != impl(bfalse,X2),
inference(scs_inference,[],[i_0_175,i_0_193,i_0_200,i_0_201]) ).
cnf(i_0_896,plain,
z = mulNat(z,X1),
inference(scs_inference,[],[i_0_194,i_0_200]) ).
cnf(i_0_898,plain,
mulNat(z,X1) = z,
inference(rename_variables,[],[i_0_194]) ).
cnf(i_0_937,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_957,plain,
bfalse = eq3(btrue,bfalse),
inference(scs_inference,[],[i_0_196,i_0_200]) ).
cnf(i_0_977,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(scs_inference,[],[i_0_173,i_0_200]) ).
cnf(i_0_1066,plain,
y(opt(n(X1)),opt(X2)) = fail32(n(X1),X2),
inference(scs_inference,[],[i_0_156,i_0_200]) ).
cnf(i_0_1113,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(scs_inference,[],[i_0_163,i_0_200]) ).
cnf(i_0_1152,plain,
y(opt(X1),opt(X2)) = fail32(X1,X2),
inference(scs_inference,[],[i_0_170,i_0_200]) ).
cnf(i_0_1232,plain,
fail1(X1,X2) = aux(X1,X2,eq2(X1,X2)),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_1247,plain,
x(opt(X1),opt(X2)) = aux(X1,X2,bfalse),
inference(scs_inference,[],[i_0_147,i_0_200]) ).
cnf(i_0_1250,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_1327,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_1329,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_1367,plain,
eq2(x(x(X1,X2),X3),x(n(X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_158,i_0_135]) ).
cnf(i_0_1369,plain,
eq2(y(x(X1,X2),X3),y(n(X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_158,i_0_135,i_0_136]) ).
cnf(i_0_1408,plain,
eq2(x(y(X1,X2),X3),x(n(X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_159,i_0_135]) ).
cnf(i_0_1410,plain,
eq2(y(y(X1,X2),X3),y(n(X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_159,i_0_135,i_0_136]) ).
cnf(i_0_1449,plain,
eq2(x(n(X1),X2),x(x(X3,X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_160,i_0_135]) ).
cnf(i_0_1451,plain,
eq2(y(n(X1),X2),y(x(X3,X4),X5)) = bfalse,
inference(scs_inference,[],[i_0_160,i_0_135,i_0_136]) ).
cnf(i_0_1791,plain,
impl(btrue,X1) = X1,
inference(rename_variables,[],[i_0_190]) ).
cnf(i_0_1939,plain,
eq3(X1,X1) = btrue,
inference(rename_variables,[],[i_0_188]) ).
cnf(i_0_1992,plain,
addNat(z,X1) = X1,
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_2032,plain,
impl(btrue,X1) = X1,
inference(rename_variables,[],[i_0_190]) ).
cnf(i_0_2172,plain,
opt(x(n(z),X1)) = X1,
inference(rename_variables,[],[i_0_169]) ).
cnf(i_0_2181,plain,
fail12(n(s(z)),X1) = X1,
inference(rename_variables,[],[i_0_176]) ).
cnf(i_0_2220,plain,
fail22(X1,n(s(z))) = X1,
inference(rename_variables,[],[i_0_177]) ).
cnf(i_0_2231,plain,
addNat(z,X1) = X1,
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_2281,plain,
addNat(z,X1) = X1,
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_2331,plain,
impl(btrue,X1) = X1,
inference(rename_variables,[],[i_0_190]) ).
cnf(i_0_2420,plain,
addNat(z,X1) = X1,
inference(rename_variables,[],[i_0_191]) ).
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_328,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_343,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(rename_variables,[],[i_0_338]) ).
cnf(i_0_344,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_335]) ).
cnf(i_0_389,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_556,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_598,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(rename_variables,[],[i_0_371]) ).
cnf(i_0_615,plain,
fail32(X1,X2) = fail22(X1,X2),
inference(rename_variables,[],[i_0_371]) ).
cnf(i_0_624,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_628,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_335]) ).
cnf(i_0_632,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_335]) ).
cnf(i_0_638,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_642,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_335]) ).
cnf(i_0_670,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_683,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_668]) ).
cnf(i_0_716,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_719,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_764,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_776,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_788,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_800,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_812,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_824,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_869,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_881,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_981,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_977]) ).
cnf(i_0_982,plain,
fail32(X1,y(X2,X3)) = fail22(X1,y(X2,X3)),
inference(rename_variables,[],[i_0_668]) ).
cnf(i_0_985,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(rename_variables,[],[i_0_338]) ).
cnf(i_0_986,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_977]) ).
cnf(i_0_990,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_977]) ).
cnf(i_0_994,plain,
fail22(n(z),X1) = fail12(n(z),X1),
inference(rename_variables,[],[i_0_977]) ).
cnf(i_0_1000,plain,
fail12(X1,X2) = fail3(X1,X2),
inference(rename_variables,[],[i_0_338]) ).
cnf(i_0_1101,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_1105,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_381]) ).
cnf(i_0_1109,plain,
fail1(X1,X2) = fail(X1,X2),
inference(rename_variables,[],[i_0_381]) ).
cnf(i_0_1118,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(rename_variables,[],[i_0_1113]) ).
cnf(i_0_1127,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(rename_variables,[],[i_0_1113]) ).
cnf(i_0_1130,plain,
fail3(X1,X2) = opt(y(X1,X2)),
inference(rename_variables,[],[i_0_1113]) ).
cnf(i_0_1142,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_335]) ).
cnf(i_0_1160,plain,
y(opt(X1),opt(X2)) = fail32(X1,X2),
inference(rename_variables,[],[i_0_1152]) ).
cnf(i_0_1172,plain,
y(opt(X1),opt(X2)) = fail32(X1,X2),
inference(rename_variables,[],[i_0_1152]) ).
cnf(i_0_1175,plain,
fail22(X1,X2) = fail12(X1,X2),
inference(rename_variables,[],[i_0_335]) ).
cnf(i_0_1205,plain,
y(opt(X1),opt(X2)) = fail32(X1,X2),
inference(rename_variables,[],[i_0_1152]) ).
cnf(i_0_1264,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_1276,plain,
X1 = addNat(z,X1),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_1331,plain,
propm5(btrue) = propm5(impl(bfalse,X1)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202]) ).
cnf(i_0_1332,plain,
n(btrue) = n(impl(bfalse,X1)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203]) ).
cnf(i_0_1333,plain,
aux(btrue,X1,X2) = aux(impl(bfalse,X3),X1,X2),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204]) ).
cnf(i_0_1334,plain,
aux(X1,btrue,X2) = aux(X1,impl(bfalse,X3),X2),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205]) ).
cnf(i_0_1335,plain,
aux(X1,X2,btrue) = aux(X1,X2,impl(bfalse,X3)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206]) ).
cnf(i_0_1336,plain,
fail32(btrue,X1) = fail32(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207]) ).
cnf(i_0_1337,plain,
fail32(X1,btrue) = fail32(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208]) ).
cnf(i_0_1338,plain,
fail(btrue,X1) = fail(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209]) ).
cnf(i_0_1339,plain,
fail(X1,btrue) = fail(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210]) ).
cnf(i_0_1340,plain,
fail3(btrue,X1) = fail3(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211]) ).
cnf(i_0_1341,plain,
fail3(X1,btrue) = fail3(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212]) ).
cnf(i_0_1342,plain,
fail12(btrue,X1) = fail12(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213]) ).
cnf(i_0_1343,plain,
fail12(X1,btrue) = fail12(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214]) ).
cnf(i_0_1344,plain,
s(btrue) = s(impl(bfalse,X1)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215]) ).
cnf(i_0_1345,plain,
fail22(btrue,X1) = fail22(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216]) ).
cnf(i_0_1346,plain,
fail22(X1,btrue) = fail22(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217]) ).
cnf(i_0_1347,plain,
mulNat(btrue,X1) = mulNat(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218]) ).
cnf(i_0_1348,plain,
mulNat(X1,btrue) = mulNat(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219]) ).
cnf(i_0_1349,plain,
addNat(btrue,X1) = addNat(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220]) ).
cnf(i_0_1350,plain,
addNat(X1,btrue) = addNat(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221]) ).
cnf(i_0_1351,plain,
impl(btrue,X1) = impl(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222]) ).
cnf(i_0_1352,plain,
impl(X1,btrue) = impl(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223]) ).
cnf(i_0_1353,plain,
eq2(btrue,X1) = eq2(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224]) ).
cnf(i_0_1354,plain,
eq2(X1,btrue) = eq2(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225]) ).
cnf(i_0_1355,plain,
opt(btrue) = opt(impl(bfalse,X1)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226]) ).
cnf(i_0_1356,plain,
d(btrue) = d(impl(bfalse,X1)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227]) ).
cnf(i_0_1357,plain,
x(btrue,X1) = x(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228]) ).
cnf(i_0_1358,plain,
x(X1,btrue) = x(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229]) ).
cnf(i_0_1359,plain,
y(btrue,X1) = y(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230]) ).
cnf(i_0_1360,plain,
y(X1,btrue) = y(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231]) ).
cnf(i_0_1361,plain,
fail1(btrue,X1) = fail1(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231,i_0_234]) ).
cnf(i_0_1362,plain,
fail1(X1,btrue) = fail1(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231,i_0_234,i_0_235]) ).
cnf(i_0_1363,plain,
eq3(X1,btrue) = eq3(X1,impl(bfalse,X2)),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231,i_0_234,i_0_235,i_0_233]) ).
cnf(i_0_1364,plain,
eq3(btrue,X1) = eq3(impl(bfalse,X2),X1),
inference(scs_inference,[],[i_0_894,i_0_149,i_0_135,i_0_136,i_0_202,i_0_203,i_0_204,i_0_205,i_0_206,i_0_207,i_0_208,i_0_209,i_0_210,i_0_211,i_0_212,i_0_213,i_0_214,i_0_215,i_0_216,i_0_217,i_0_218,i_0_219,i_0_220,i_0_221,i_0_222,i_0_223,i_0_224,i_0_225,i_0_226,i_0_227,i_0_228,i_0_229,i_0_230,i_0_231,i_0_234,i_0_235,i_0_233,i_0_232]) ).
cnf(i_0_1540,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_1649,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_1699,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_1845,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_1886,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_1945,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_2272,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_2377,plain,
X1 = impl(btrue,X1),
inference(rename_variables,[],[i_0_236]) ).
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_261,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_286,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_350,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_461,plain,
eq2(X1,X2) = eq2(x(X3,X1),x(X3,X2)),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_1407,plain,
eq3(X1,btrue) = eq3(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1363]) ).
cnf(i_0_1448,plain,
impl(btrue,X1) = impl(impl(bfalse,X2),X1),
inference(rename_variables,[],[i_0_1351]) ).
cnf(i_0_1535,plain,
aux(X1,btrue,X2) = aux(X1,impl(bfalse,X3),X2),
inference(rename_variables,[],[i_0_1334]) ).
cnf(i_0_1536,plain,
aux(X1,X2,btrue) = aux(X1,X2,impl(bfalse,X3)),
inference(rename_variables,[],[i_0_1335]) ).
cnf(i_0_1537,plain,
eq3(fail32(btrue,X1),X2) = eq3(fail32(impl(bfalse,X3),X1),X2),
inference(scs_inference,[],[i_0_1336,i_0_232]) ).
cnf(i_0_1544,plain,
fail32(X1,btrue) = fail32(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1337]) ).
cnf(i_0_1549,plain,
eq3(btrue,X1) = eq3(impl(bfalse,X2),X1),
inference(rename_variables,[],[i_0_1364]) ).
cnf(i_0_1588,plain,
fail(X1,btrue) = fail(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1339]) ).
cnf(i_0_1591,plain,
impl(X1,btrue) = impl(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1352]) ).
cnf(i_0_1596,plain,
fail3(X1,btrue) = fail3(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1341]) ).
cnf(i_0_1638,plain,
fail12(X1,btrue) = fail12(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1343]) ).
cnf(i_0_1641,plain,
impl(btrue,X1) = impl(impl(bfalse,X2),X1),
inference(rename_variables,[],[i_0_1351]) ).
cnf(i_0_1646,plain,
fail22(X1,btrue) = fail22(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1346]) ).
cnf(i_0_1688,plain,
mulNat(X1,btrue) = mulNat(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1348]) ).
cnf(i_0_1696,plain,
addNat(X1,btrue) = addNat(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1350]) ).
cnf(i_0_1738,plain,
eq2(X1,btrue) = eq2(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1354]) ).
cnf(i_0_1745,plain,
x(X1,btrue) = x(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1358]) ).
cnf(i_0_1788,plain,
y(X1,btrue) = y(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1360]) ).
cnf(i_0_1796,plain,
fail1(X1,btrue) = fail1(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1362]) ).
cnf(i_0_1840,plain,
impl(btrue,X1) = impl(impl(bfalse,X2),X1),
inference(rename_variables,[],[i_0_1351]) ).
cnf(i_0_1844,plain,
s(btrue) = impl(btrue,s(impl(bfalse,X1))),
inference(scs_inference,[],[i_0_1344,i_0_236,i_0_201]) ).
cnf(i_0_1885,plain,
d(btrue) = impl(btrue,d(impl(bfalse,X1))),
inference(scs_inference,[],[i_0_1356,i_0_236,i_0_201]) ).
cnf(i_0_2040,plain,
impl(btrue,X1) = impl(impl(bfalse,X2),X1),
inference(rename_variables,[],[i_0_1351]) ).
cnf(i_0_2133,plain,
eq3(btrue,X1) = eq3(impl(bfalse,X2),X1),
inference(rename_variables,[],[i_0_1364]) ).
cnf(i_0_2322,plain,
eq3(X1,btrue) = eq3(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1363]) ).
cnf(i_0_2369,plain,
impl(btrue,X1) = impl(impl(bfalse,X2),X1),
inference(rename_variables,[],[i_0_1351]) ).
cnf(i_0_2379,plain,
eq3(X1,btrue) = eq3(X1,impl(bfalse,X2)),
inference(rename_variables,[],[i_0_1363]) ).
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_300,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_325,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_449,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_488,plain,
eq2(X1,X2) = eq2(y(X3,x(X4,X1)),y(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_503,plain,
eq2(y(X1,x(X2,X3)),y(X1,x(X2,X4))) = eq2(x(X5,X3),x(X5,X4)),
inference(rename_variables,[],[i_0_247]) ).
cnf(i_0_2368,plain,
d(btrue) = impl(impl(bfalse,X1),d(impl(bfalse,X2))),
inference(scs_inference,[],[i_0_1885,i_0_1351,i_0_201]) ).
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_283,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_347,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_392,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_491,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_2376,plain,
d(btrue) = impl(btrue,impl(impl(bfalse,X1),d(impl(bfalse,X2)))),
inference(scs_inference,[],[i_0_2368,i_0_236,i_0_201]) ).
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_273,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_380,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_433,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_476,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_530,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_260,plain,
eq2(y(X1,x(X2,y(X3,x(X4,X5)))),y(X1,x(X2,y(X3,x(X4,X6))))) = eq2(x(X7,x(X8,X5)),x(X7,x(X8,X6))),
inference(scs_inference,[],[i_0_255,i_0_243,i_0_256,i_0_200,i_0_201]) ).
cnf(i_0_267,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_322,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(X3,X4),
inference(rename_variables,[],[i_0_256]) ).
cnf(i_0_407,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_262,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(y(X5,x(X6,y(X7,x(X8,X3)))),y(X5,x(X6,y(X7,x(X8,X4))))),
inference(scs_inference,[],[i_0_260,i_0_200]) ).
cnf(i_0_263,plain,
eq2(y(X1,x(X2,x(X3,X4))),y(X1,x(X2,x(X3,X5)))) = eq2(x(X6,x(X7,X4)),x(X6,x(X7,X5))),
inference(scs_inference,[],[i_0_259,i_0_252,i_0_260,i_0_200,i_0_201]) ).
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(i_0_270,plain,
eq2(X1,X2) = eq2(x(X3,x(X4,X1)),x(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_307,plain,
eq2(X1,X2) = eq2(x(X3,x(X4,X1)),x(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_420,plain,
eq2(X1,X2) = eq2(x(X3,x(X4,X1)),x(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_452,plain,
eq2(X1,X2) = eq2(x(X3,x(X4,X1)),x(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_512,plain,
eq2(X1,X2) = eq2(x(X3,x(X4,X1)),x(X3,x(X4,X2))),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_265,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(y(X5,x(X6,x(X7,X3))),y(X5,x(X6,x(X7,X4)))),
inference(scs_inference,[],[i_0_263,i_0_200]) ).
cnf(i_0_266,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(x(X5,X3),x(X5,X4)),
inference(scs_inference,[],[i_0_262,i_0_255,i_0_263,i_0_200,i_0_201]) ).
cnf(i_0_290,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(y(X5,x(X6,y(X7,x(X8,X3)))),y(X5,x(X6,y(X7,x(X8,X4))))),
inference(rename_variables,[],[i_0_262]) ).
cnf(i_0_268,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(x(X4,x(X5,X2)),x(X4,x(X5,X3))),
inference(scs_inference,[],[i_0_266,i_0_200]) ).
cnf(i_0_280,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(y(X5,x(X6,x(X7,X3))),y(X5,x(X6,x(X7,X4)))),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_304,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(y(X5,x(X6,x(X7,X3))),y(X5,x(X6,x(X7,X4)))),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_437,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(y(X5,x(X6,x(X7,X3))),y(X5,x(X6,x(X7,X4)))),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_464,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(y(X5,x(X6,x(X7,X3))),y(X5,x(X6,x(X7,X4)))),
inference(rename_variables,[],[i_0_265]) ).
cnf(i_0_272,plain,
eq2(y(X1,x(X2,x(X3,x(X4,X5)))),y(X1,x(X2,x(X3,x(X4,X6))))) = eq2(x(X7,x(X8,X5)),x(X7,x(X8,X6))),
inference(scs_inference,[],[i_0_268,i_0_252,i_0_269,i_0_200,i_0_201]) ).
cnf(i_0_277,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(x(X4,x(X5,X2)),x(X4,x(X5,X3))),
inference(rename_variables,[],[i_0_268]) ).
cnf(i_0_293,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(x(X4,x(X5,X2)),x(X4,x(X5,X3))),
inference(rename_variables,[],[i_0_268]) ).
cnf(i_0_414,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(x(X4,x(X5,X2)),x(X4,x(X5,X3))),
inference(rename_variables,[],[i_0_268]) ).
cnf(i_0_515,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(x(X4,x(X5,X2)),x(X4,x(X5,X3))),
inference(rename_variables,[],[i_0_268]) ).
cnf(i_0_274,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(y(X5,x(X6,x(X7,x(X8,X3)))),y(X5,x(X6,x(X7,x(X8,X4))))),
inference(scs_inference,[],[i_0_272,i_0_200]) ).
cnf(i_0_275,plain,
eq2(x(X1,y(X2,x(X3,x(X4,X5)))),x(X1,y(X2,x(X3,x(X4,X6))))) = eq2(x(X7,x(X8,X5)),x(X7,x(X8,X6))),
inference(scs_inference,[],[i_0_271,i_0_268,i_0_272,i_0_200,i_0_201]) ).
cnf(i_0_278,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(x(X5,y(X6,x(X7,x(X8,X3)))),x(X5,y(X6,x(X7,x(X8,X4))))),
inference(scs_inference,[],[i_0_275,i_0_200]) ).
cnf(i_0_296,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(y(X5,x(X6,x(X7,x(X8,X3)))),y(X5,x(X6,x(X7,x(X8,X4))))),
inference(rename_variables,[],[i_0_274]) ).
cnf(i_0_424,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(y(X5,x(X6,x(X7,x(X8,X3)))),y(X5,x(X6,x(X7,x(X8,X4))))),
inference(rename_variables,[],[i_0_274]) ).
cnf(i_0_288,plain,
eq2(x(X1,x(X2,x(X3,X4))),x(X1,x(X2,x(X3,X5)))) = eq2(x(X6,x(X7,X4)),x(X6,x(X7,X5))),
inference(scs_inference,[],[i_0_284,i_0_262,i_0_285,i_0_200,i_0_201]) ).
cnf(i_0_291,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(x(X5,x(X6,x(X7,X3))),x(X5,x(X6,x(X7,X4)))),
inference(scs_inference,[],[i_0_288,i_0_200]) ).
cnf(i_0_310,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(x(X5,x(X6,x(X7,X3))),x(X5,x(X6,x(X7,X4)))),
inference(rename_variables,[],[i_0_291]) ).
cnf(i_0_316,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(x(X5,x(X6,x(X7,X3))),x(X5,x(X6,x(X7,X4)))),
inference(rename_variables,[],[i_0_291]) ).
cnf(i_0_458,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(x(X5,x(X6,x(X7,X3))),x(X5,x(X6,x(X7,X4)))),
inference(rename_variables,[],[i_0_291]) ).
cnf(i_0_298,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(x(X4,x(X5,y(X6,x(X7,x(X8,X2))))),x(X4,x(X5,y(X6,x(X7,x(X8,X3)))))),
inference(scs_inference,[],[i_0_281,i_0_246,i_0_295,i_0_200,i_0_201]) ).
cnf(i_0_301,plain,
eq2(x(X1,x(X2,y(X3,x(X4,x(X5,X6))))),x(X1,x(X2,y(X3,x(X4,x(X5,X7)))))) = eq2(x(X8,X6),x(X8,X7)),
inference(scs_inference,[],[i_0_298,i_0_200]) ).
cnf(i_0_302,plain,
eq2(x(X1,x(X2,x(X3,x(X4,X5)))),x(X1,x(X2,x(X3,x(X4,X6))))) = eq2(x(X7,x(X8,X5)),x(X7,x(X8,X6))),
inference(scs_inference,[],[i_0_297,i_0_265,i_0_298,i_0_200,i_0_201]) ).
cnf(i_0_305,plain,
eq2(x(X1,x(X2,X3)),x(X1,x(X2,X4))) = eq2(x(X5,x(X6,x(X7,x(X8,X3)))),x(X5,x(X6,x(X7,x(X8,X4))))),
inference(scs_inference,[],[i_0_302,i_0_200]) ).
cnf(i_0_313,plain,
eq2(x(X1,x(X2,y(X3,x(X4,x(X5,X6))))),x(X1,x(X2,y(X3,x(X4,x(X5,X7)))))) = eq2(x(X8,X6),x(X8,X7)),
inference(rename_variables,[],[i_0_301]) ).
cnf(i_0_312,plain,
eq2(x(X1,x(X2,x(X3,X4))),x(X1,x(X2,x(X3,X5)))) = eq2(x(X6,X4),x(X6,X5)),
inference(scs_inference,[],[i_0_308,i_0_301,i_0_309,i_0_200,i_0_201]) ).
cnf(i_0_314,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(x(X4,x(X5,x(X6,X2))),x(X4,x(X5,x(X6,X3)))),
inference(scs_inference,[],[i_0_312,i_0_200]) ).
cnf(i_0_318,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(x(X4,y(X5,x(X6,x(X7,x(X8,X2))))),x(X4,y(X5,x(X6,x(X7,x(X8,X3)))))),
inference(scs_inference,[],[i_0_314,i_0_294,i_0_315,i_0_200,i_0_201]) ).
cnf(i_0_356,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(x(X4,x(X5,x(X6,X2))),x(X4,x(X5,x(X6,X3)))),
inference(rename_variables,[],[i_0_314]) ).
cnf(i_0_359,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(x(X4,x(X5,x(X6,X2))),x(X4,x(X5,x(X6,X3)))),
inference(rename_variables,[],[i_0_314]) ).
cnf(i_0_320,plain,
eq2(x(X1,y(X2,x(X3,x(X4,x(X5,X6))))),x(X1,y(X2,x(X3,x(X4,x(X5,X7)))))) = eq2(x(X8,X6),x(X8,X7)),
inference(scs_inference,[],[i_0_318,i_0_200]) ).
cnf(i_0_321,plain,
eq2(x(X1,x(X2,x(X3,X4))),x(X1,x(X2,x(X3,X5)))) = eq2(x(X6,x(X7,x(X8,X4))),x(X6,x(X7,x(X8,X5)))),
inference(scs_inference,[],[i_0_317,i_0_318,i_0_256,i_0_200,i_0_201]) ).
cnf(i_0_331,plain,
eq2(x(X1,y(X2,x(X3,x(X4,x(X5,X6))))),x(X1,y(X2,x(X3,x(X4,x(X5,X7)))))) = eq2(x(X8,X6),x(X8,X7)),
inference(rename_variables,[],[i_0_320]) ).
cnf(i_0_362,plain,
eq2(x(X1,y(X2,x(X3,x(X4,x(X5,X6))))),x(X1,y(X2,x(X3,x(X4,x(X5,X7)))))) = eq2(x(X8,X6),x(X8,X7)),
inference(rename_variables,[],[i_0_320]) ).
cnf(i_0_373,plain,
eq2(x(X1,y(X2,x(X3,x(X4,x(X5,X6))))),x(X1,y(X2,x(X3,x(X4,x(X5,X7)))))) = eq2(x(X8,X6),x(X8,X7)),
inference(rename_variables,[],[i_0_320]) ).
cnf(i_0_327,plain,
X1 = addNat(z,impl(btrue,X1)),
inference(scs_inference,[],[i_0_236,i_0_323,i_0_324,i_0_200,i_0_201]) ).
cnf(i_0_329,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(scs_inference,[],[i_0_327,i_0_200]) ).
cnf(i_0_330,plain,
eq2(y(X1,x(X2,x(X3,X4))),y(X1,x(X2,x(X3,X5)))) = eq2(x(X6,X4),x(X6,X5)),
inference(scs_inference,[],[i_0_326,i_0_320,i_0_327,i_0_200,i_0_201]) ).
cnf(i_0_1326,plain,
X1 = addNat(z,impl(btrue,X1)),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_1493,plain,
X1 = addNat(z,impl(btrue,X1)),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_1496,plain,
X1 = addNat(z,impl(btrue,X1)),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_1599,plain,
X1 = addNat(z,impl(btrue,X1)),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_1691,plain,
X1 = addNat(z,impl(btrue,X1)),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_1799,plain,
X1 = addNat(z,impl(btrue,X1)),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_1847,plain,
X1 = addNat(z,impl(btrue,X1)),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_1896,plain,
X1 = addNat(z,impl(btrue,X1)),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_2080,plain,
X1 = addNat(z,impl(btrue,X1)),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_2371,plain,
X1 = addNat(z,impl(btrue,X1)),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_332,plain,
eq2(x(X1,X2),x(X1,X3)) = eq2(y(X4,x(X5,x(X6,X2))),y(X4,x(X5,x(X6,X3)))),
inference(scs_inference,[],[i_0_330,i_0_200]) ).
cnf(i_0_333,plain,
eq3(propm5(X1),bfalse) != addNat(z,impl(btrue,btrue)),
inference(scs_inference,[],[i_0_175,i_0_329,i_0_330,i_0_200,i_0_201]) ).
cnf(i_0_334,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_337,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_339,plain,
addNat(z,impl(btrue,fail22(X1,X2))) = fail12(X1,X2),
inference(scs_inference,[],[i_0_335,i_0_329,i_0_180,i_0_200,i_0_201]) ).
cnf(i_0_340,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_377,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_386,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_541,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_562,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_568,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_585,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_607,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_618,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_621,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_635,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_645,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_655,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_658,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_673,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_722,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_728,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_761,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_767,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_770,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_773,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_779,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_782,plain,
addNat(z,impl(btrue,X1)) = X1,
inference(rename_variables,[],[i_0_329]) ).
cnf(c_0_1166,plain,
fail22(X1,X2) = fail12(X1,X2),
i_0_335 ).
cnf(c_0_1167,plain,
fail12(X1,X2) = fail3(X1,X2),
i_0_338 ).
cnf(c_0_1168,plain,
fail32(X1,X2) = fail22(X1,X2),
i_0_371 ).
cnf(c_0_1169,axiom,
fail22(X1,n(s(z))) = X1,
i_0_177 ).
cnf(c_0_1170,plain,
fail32(X1,X2) = fail3(X1,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1166,c_0_1167]),c_0_1168]) ).
cnf(c_0_1171,plain,
fail3(X1,X2) = opt(y(X1,X2)),
i_0_1113 ).
cnf(c_0_1172,plain,
y(opt(X1),opt(X2)) = fail32(X1,X2),
i_0_1152 ).
cnf(c_0_1173,axiom,
opt(n(X1)) = n(X1),
i_0_187 ).
cnf(c_0_1174,axiom,
d(x2) = n(s(z)),
i_0_197 ).
cnf(c_0_1175,plain,
opt(y(X1,n(s(z)))) = X1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1169,c_0_1168]),c_0_1170]),c_0_1171]) ).
cnf(c_0_1176,plain,
y(opt(X1),opt(X2)) = opt(y(X1,X2)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1172,c_0_1170]),c_0_1171]) ).
cnf(c_0_1177,plain,
opt(d(x2)) = d(x2),
inference(spm,[status(thm)],[c_0_1173,c_0_1174]) ).
cnf(c_0_1178,plain,
opt(y(X1,d(x2))) = X1,
inference(rw,[status(thm)],[c_0_1175,c_0_1174]) ).
cnf(c_0_1179,axiom,
eq2(y(X1,X2),x2) = bfalse,
i_0_166 ).
cnf(c_0_1180,plain,
y(opt(X1),d(x2)) = X1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1176,c_0_1177]),c_0_1178]) ).
cnf(c_0_1181,axiom,
eq2(X1,X1) = btrue,
i_0_189 ).
cnf(c_0_1182,plain,
eq2(X1,x2) = bfalse,
inference(spm,[status(thm)],[c_0_1179,c_0_1180]) ).
cnf(c_0_1183,negated_conjecture,
eq3(propm5(X1),bfalse) != btrue,
i_0_175 ).
cnf(c_0_1184,plain,
bfalse = btrue,
inference(spm,[status(thm)],[c_0_1181,c_0_1182]) ).
cnf(c_0_1185,plain,
btrue = impl(bfalse,X1),
i_0_894 ).
cnf(c_0_1186,plain,
X1 = impl(btrue,X1),
i_0_236 ).
cnf(c_0_1187,negated_conjecture,
eq3(propm5(X1),btrue) != btrue,
inference(rw,[status(thm)],[c_0_1183,c_0_1184]) ).
cnf(c_0_1188,plain,
X1 = btrue,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1185,c_0_1184]),c_0_1186]) ).
cnf(c_0_1189,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1187,c_0_1188])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX192-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.32 % Computer : n018.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue May 5 07:54:47 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 124.14/87.48 % Version : CSE_E---1.7
% 124.14/87.48 % Problem : theBenchmark.p
% 124.14/87.48 % SZS status Unsatisfiable for theBenchmark.p
% 124.14/87.48 % SZS output start CNFRefutation
% See solution above
% 130.54/93.86 % Total time : 87.136s
%------------------------------------------------------------------------------