%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWX217-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n008.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 07:04:35 PM UTC 2026
% Result : Unsatisfiable 1.03s 1.20s
% Output : CNFRefutation 1.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 184
% Syntax : Number of clauses : 568 ( 275 unt; 0 nHn; 484 RR)
% Number of literals : 997 ( 996 equ; 433 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 8 ( 3 avg)
% Number of predicates : 3 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 6 con; 0-2 aty)
% Number of variables : 170 ( 3 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
aux(Y,btrue) = cons(o,shw(half(suc(Y)))) ).
cnf(axiom_001,axiom,
aux(Y,bfalse) = cons(i,shw(half(suc(Y)))) ).
cnf(axiom_002,axiom,
notb(btrue) = bfalse ).
cnf(axiom_003,axiom,
notb(bfalse) = btrue ).
cnf(axiom_004,axiom,
half(zero) = zero ).
cnf(axiom_005,axiom,
half(suc(zero)) = zero ).
cnf(axiom_006,axiom,
half(suc(suc(N))) = suc(half(N)) ).
cnf(axiom_007,axiom,
evenNat(zero) = btrue ).
cnf(axiom_008,axiom,
evenNat(suc(N)) = notb(evenNat(N)) ).
cnf(axiom_009,axiom,
shw(zero) = nil ).
cnf(axiom_010,axiom,
shw(suc(Y)) = aux(Y,evenNat(suc(Y))) ).
cnf(axiom_011,axiom,
append(nil,Y) = Y ).
cnf(axiom_012,axiom,
append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ).
cnf(axiom_013,axiom,
addNat(zero,Y) = Y ).
cnf(axiom_014,axiom,
addNat(suc(Z),Y) = suc(addNat(Z,Y)) ).
cnf(axiom_015,axiom,
double(X) = addNat(X,X) ).
cnf(axiom_016,axiom,
rd(nil) = zero ).
cnf(axiom_017,axiom,
rd(cons(i,Xs)) = suc(double(rd(Xs))) ).
cnf(axiom_018,axiom,
rd(cons(o,Xs)) = double(rd(Xs)) ).
cnf(axiom_019,axiom,
x(X,Y) = rd(append(shw(X),shw(Y))) ).
cnf(axiom_020,axiom,
sat_comm(X,Y) = eq(x(X,Y),x(Y,X)) ).
cnf(axiom_025,axiom,
eq(suc(X),suc(Y)) = eq(X,Y) ).
cnf(axiom_026,axiom,
eq(zero,suc(X)) = bfalse ).
cnf(axiom_029,axiom,
eq2(X,X) = btrue ).
cnf(goal,negated_conjecture,
eq2(sat_comm(X,Y),bfalse) != btrue ).
cnf(refute_0_0,plain,
eq2(sat_comm(suc(zero),double(suc(zero))),bfalse) != btrue,
inference(subst,[],[goal:[bind(X,$fot(suc(zero))),bind(Y,$fot(double(suc(zero))))]]) ).
cnf(refute_0_1,plain,
sat_comm(suc(zero),double(suc(zero))) = eq(x(suc(zero),double(suc(zero))),x(double(suc(zero)),suc(zero))),
inference(subst,[],[axiom_020:[bind(X,$fot(suc(zero))),bind(Y,$fot(double(suc(zero))))]]) ).
cnf(refute_0_2,plain,
x(suc(zero),Y) = rd(append(shw(suc(zero)),shw(Y))),
inference(subst,[],[axiom_019:[bind(X,$fot(suc(zero)))]]) ).
cnf(refute_0_3,plain,
append(cons(i,nil),X_129) = cons(i,append(nil,X_129)),
inference(subst,[],[axiom_012:[bind(Xs,$fot(nil)),bind(Y,$fot(X_129)),bind(Z,$fot(i))]]) ).
cnf(refute_0_4,plain,
aux(zero,bfalse) = cons(i,shw(half(suc(zero)))),
inference(subst,[],[axiom_001:[bind(Y,$fot(zero))]]) ).
cnf(refute_0_5,plain,
( aux(zero,bfalse) != cons(i,shw(half(suc(zero))))
| half(suc(zero)) != zero
| aux(zero,bfalse) = cons(i,shw(zero)) ),
introduced(tautology,[equality,[$cnf( $equal(aux(zero,bfalse),cons(i,shw(half(suc(zero))))) ),[1,1,0],$fot(zero)]]) ).
cnf(refute_0_6,plain,
( aux(zero,bfalse) != cons(i,shw(half(suc(zero))))
| aux(zero,bfalse) = cons(i,shw(zero)) ),
inference(resolve,[$cnf( $equal(half(suc(zero)),zero) )],[axiom_005,refute_0_5]) ).
cnf(refute_0_7,plain,
aux(zero,bfalse) = cons(i,shw(zero)),
inference(resolve,[$cnf( $equal(aux(zero,bfalse),cons(i,shw(half(suc(zero))))) )],[refute_0_4,refute_0_6]) ).
cnf(refute_0_8,plain,
shw(suc(zero)) = aux(zero,evenNat(suc(zero))),
inference(subst,[],[axiom_010:[bind(Y,$fot(zero))]]) ).
cnf(refute_0_9,plain,
evenNat(suc(zero)) = notb(evenNat(zero)),
inference(subst,[],[axiom_008:[bind(N,$fot(zero))]]) ).
cnf(refute_0_10,plain,
( evenNat(suc(zero)) != notb(evenNat(zero))
| evenNat(zero) != btrue
| evenNat(suc(zero)) = notb(btrue) ),
introduced(tautology,[equality,[$cnf( $equal(evenNat(suc(zero)),notb(evenNat(zero))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_11,plain,
( evenNat(suc(zero)) != notb(evenNat(zero))
| evenNat(suc(zero)) = notb(btrue) ),
inference(resolve,[$cnf( $equal(evenNat(zero),btrue) )],[axiom_007,refute_0_10]) ).
cnf(refute_0_12,plain,
evenNat(suc(zero)) = notb(btrue),
inference(resolve,[$cnf( $equal(evenNat(suc(zero)),notb(evenNat(zero))) )],[refute_0_9,refute_0_11]) ).
cnf(refute_0_13,plain,
( evenNat(suc(zero)) != notb(btrue)
| notb(btrue) != bfalse
| evenNat(suc(zero)) = bfalse ),
introduced(tautology,[equality,[$cnf( ~ $equal(evenNat(suc(zero)),bfalse) ),[0],$fot(notb(btrue))]]) ).
cnf(refute_0_14,plain,
( evenNat(suc(zero)) != notb(btrue)
| evenNat(suc(zero)) = bfalse ),
inference(resolve,[$cnf( $equal(notb(btrue),bfalse) )],[axiom_002,refute_0_13]) ).
cnf(refute_0_15,plain,
evenNat(suc(zero)) = bfalse,
inference(resolve,[$cnf( $equal(evenNat(suc(zero)),notb(btrue)) )],[refute_0_12,refute_0_14]) ).
cnf(refute_0_16,plain,
( evenNat(suc(zero)) != bfalse
| shw(suc(zero)) != aux(zero,evenNat(suc(zero)))
| shw(suc(zero)) = aux(zero,bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(shw(suc(zero)),aux(zero,evenNat(suc(zero)))) ),[1,1],$fot(bfalse)]]) ).
cnf(refute_0_17,plain,
( shw(suc(zero)) != aux(zero,evenNat(suc(zero)))
| shw(suc(zero)) = aux(zero,bfalse) ),
inference(resolve,[$cnf( $equal(evenNat(suc(zero)),bfalse) )],[refute_0_15,refute_0_16]) ).
cnf(refute_0_18,plain,
shw(suc(zero)) = aux(zero,bfalse),
inference(resolve,[$cnf( $equal(shw(suc(zero)),aux(zero,evenNat(suc(zero)))) )],[refute_0_8,refute_0_17]) ).
cnf(refute_0_19,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_20,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_21,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_19,refute_0_20]) ).
cnf(refute_0_22,plain,
( shw(suc(zero)) != aux(zero,bfalse)
| aux(zero,bfalse) = shw(suc(zero)) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(shw(suc(zero)))),bind(Y0,$fot(aux(zero,bfalse)))]]) ).
cnf(refute_0_23,plain,
aux(zero,bfalse) = shw(suc(zero)),
inference(resolve,[$cnf( $equal(shw(suc(zero)),aux(zero,bfalse)) )],[refute_0_18,refute_0_22]) ).
cnf(refute_0_24,plain,
( aux(zero,bfalse) != cons(i,shw(zero))
| aux(zero,bfalse) != shw(suc(zero))
| shw(suc(zero)) = cons(i,shw(zero)) ),
introduced(tautology,[equality,[$cnf( $equal(aux(zero,bfalse),cons(i,shw(zero))) ),[0],$fot(shw(suc(zero)))]]) ).
cnf(refute_0_25,plain,
( aux(zero,bfalse) != cons(i,shw(zero))
| shw(suc(zero)) = cons(i,shw(zero)) ),
inference(resolve,[$cnf( $equal(aux(zero,bfalse),shw(suc(zero))) )],[refute_0_23,refute_0_24]) ).
cnf(refute_0_26,plain,
cons(i,shw(zero)) = cons(i,shw(zero)),
introduced(tautology,[refl,[$fot(cons(i,shw(zero)))]]) ).
cnf(refute_0_27,plain,
( cons(i,shw(zero)) != cons(i,shw(zero))
| shw(zero) != nil
| cons(i,shw(zero)) = cons(i,nil) ),
introduced(tautology,[equality,[$cnf( $equal(cons(i,shw(zero)),cons(i,shw(zero))) ),[1,1],$fot(nil)]]) ).
cnf(refute_0_28,plain,
( shw(zero) != nil
| cons(i,shw(zero)) = cons(i,nil) ),
inference(resolve,[$cnf( $equal(cons(i,shw(zero)),cons(i,shw(zero))) )],[refute_0_26,refute_0_27]) ).
cnf(refute_0_29,plain,
cons(i,shw(zero)) = cons(i,nil),
inference(resolve,[$cnf( $equal(shw(zero),nil) )],[axiom_009,refute_0_28]) ).
cnf(refute_0_30,plain,
( cons(i,shw(zero)) != cons(i,nil)
| shw(suc(zero)) != cons(i,shw(zero))
| shw(suc(zero)) = cons(i,nil) ),
introduced(tautology,[equality,[$cnf( $equal(shw(suc(zero)),cons(i,shw(zero))) ),[1],$fot(cons(i,nil))]]) ).
cnf(refute_0_31,plain,
( shw(suc(zero)) != cons(i,shw(zero))
| shw(suc(zero)) = cons(i,nil) ),
inference(resolve,[$cnf( $equal(cons(i,shw(zero)),cons(i,nil)) )],[refute_0_29,refute_0_30]) ).
cnf(refute_0_32,plain,
( aux(zero,bfalse) != cons(i,shw(zero))
| shw(suc(zero)) = cons(i,nil) ),
inference(resolve,[$cnf( $equal(shw(suc(zero)),cons(i,shw(zero))) )],[refute_0_25,refute_0_31]) ).
cnf(refute_0_33,plain,
shw(suc(zero)) = cons(i,nil),
inference(resolve,[$cnf( $equal(aux(zero,bfalse),cons(i,shw(zero))) )],[refute_0_7,refute_0_32]) ).
cnf(refute_0_34,plain,
( shw(suc(zero)) != cons(i,nil)
| cons(i,nil) = shw(suc(zero)) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(shw(suc(zero)))),bind(Y0,$fot(cons(i,nil)))]]) ).
cnf(refute_0_35,plain,
cons(i,nil) = shw(suc(zero)),
inference(resolve,[$cnf( $equal(shw(suc(zero)),cons(i,nil)) )],[refute_0_33,refute_0_34]) ).
cnf(refute_0_36,plain,
( cons(i,nil) != shw(suc(zero))
| append(cons(i,nil),X_129) != cons(i,append(nil,X_129))
| append(shw(suc(zero)),X_129) = cons(i,append(nil,X_129)) ),
introduced(tautology,[equality,[$cnf( $equal(append(cons(i,nil),X_129),cons(i,append(nil,X_129))) ),[0,0],$fot(shw(suc(zero)))]]) ).
cnf(refute_0_37,plain,
( append(cons(i,nil),X_129) != cons(i,append(nil,X_129))
| append(shw(suc(zero)),X_129) = cons(i,append(nil,X_129)) ),
inference(resolve,[$cnf( $equal(cons(i,nil),shw(suc(zero))) )],[refute_0_35,refute_0_36]) ).
cnf(refute_0_38,plain,
append(shw(suc(zero)),X_129) = cons(i,append(nil,X_129)),
inference(resolve,[$cnf( $equal(append(cons(i,nil),X_129),cons(i,append(nil,X_129))) )],[refute_0_3,refute_0_37]) ).
cnf(refute_0_39,plain,
append(nil,X_129) = X_129,
inference(subst,[],[axiom_011:[bind(Y,$fot(X_129))]]) ).
cnf(refute_0_40,plain,
cons(i,append(nil,X_129)) = cons(i,append(nil,X_129)),
introduced(tautology,[refl,[$fot(cons(i,append(nil,X_129)))]]) ).
cnf(refute_0_41,plain,
( cons(i,append(nil,X_129)) != cons(i,append(nil,X_129))
| append(nil,X_129) != X_129
| cons(i,append(nil,X_129)) = cons(i,X_129) ),
introduced(tautology,[equality,[$cnf( $equal(cons(i,append(nil,X_129)),cons(i,append(nil,X_129))) ),[1,1],$fot(X_129)]]) ).
cnf(refute_0_42,plain,
( append(nil,X_129) != X_129
| cons(i,append(nil,X_129)) = cons(i,X_129) ),
inference(resolve,[$cnf( $equal(cons(i,append(nil,X_129)),cons(i,append(nil,X_129))) )],[refute_0_40,refute_0_41]) ).
cnf(refute_0_43,plain,
cons(i,append(nil,X_129)) = cons(i,X_129),
inference(resolve,[$cnf( $equal(append(nil,X_129),X_129) )],[refute_0_39,refute_0_42]) ).
cnf(refute_0_44,plain,
( cons(i,append(nil,X_129)) != cons(i,X_129)
| append(shw(suc(zero)),X_129) != cons(i,append(nil,X_129))
| append(shw(suc(zero)),X_129) = cons(i,X_129) ),
introduced(tautology,[equality,[$cnf( $equal(append(shw(suc(zero)),X_129),cons(i,append(nil,X_129))) ),[1],$fot(cons(i,X_129))]]) ).
cnf(refute_0_45,plain,
( append(shw(suc(zero)),X_129) != cons(i,append(nil,X_129))
| append(shw(suc(zero)),X_129) = cons(i,X_129) ),
inference(resolve,[$cnf( $equal(cons(i,append(nil,X_129)),cons(i,X_129)) )],[refute_0_43,refute_0_44]) ).
cnf(refute_0_46,plain,
append(shw(suc(zero)),X_129) = cons(i,X_129),
inference(resolve,[$cnf( $equal(append(shw(suc(zero)),X_129),cons(i,append(nil,X_129))) )],[refute_0_38,refute_0_45]) ).
cnf(refute_0_47,plain,
append(shw(suc(zero)),shw(Y)) = cons(i,shw(Y)),
inference(subst,[],[refute_0_46:[bind(X_129,$fot(shw(Y)))]]) ).
cnf(refute_0_48,plain,
( append(shw(suc(zero)),shw(Y)) != cons(i,shw(Y))
| x(suc(zero),Y) != rd(append(shw(suc(zero)),shw(Y)))
| x(suc(zero),Y) = rd(cons(i,shw(Y))) ),
introduced(tautology,[equality,[$cnf( $equal(x(suc(zero),Y),rd(append(shw(suc(zero)),shw(Y)))) ),[1,0],$fot(cons(i,shw(Y)))]]) ).
cnf(refute_0_49,plain,
( x(suc(zero),Y) != rd(append(shw(suc(zero)),shw(Y)))
| x(suc(zero),Y) = rd(cons(i,shw(Y))) ),
inference(resolve,[$cnf( $equal(append(shw(suc(zero)),shw(Y)),cons(i,shw(Y))) )],[refute_0_47,refute_0_48]) ).
cnf(refute_0_50,plain,
x(suc(zero),Y) = rd(cons(i,shw(Y))),
inference(resolve,[$cnf( $equal(x(suc(zero),Y),rd(append(shw(suc(zero)),shw(Y)))) )],[refute_0_2,refute_0_49]) ).
cnf(refute_0_51,plain,
x(suc(zero),double(suc(zero))) = rd(cons(i,shw(double(suc(zero))))),
inference(subst,[],[refute_0_50:[bind(Y,$fot(double(suc(zero))))]]) ).
cnf(refute_0_52,plain,
aux(double(double(suc(zero))),bfalse) = cons(i,shw(half(suc(double(double(suc(zero))))))),
inference(subst,[],[axiom_001:[bind(Y,$fot(double(double(suc(zero)))))]]) ).
cnf(refute_0_53,plain,
half(suc(suc(suc(double(suc(zero)))))) = suc(half(suc(double(suc(zero))))),
inference(subst,[],[axiom_006:[bind(N,$fot(suc(double(suc(zero)))))]]) ).
cnf(refute_0_54,plain,
double(suc(X_19)) = addNat(suc(X_19),suc(X_19)),
inference(subst,[],[axiom_015:[bind(X,$fot(suc(X_19)))]]) ).
cnf(refute_0_55,plain,
addNat(suc(X_19),suc(X_19)) = suc(addNat(X_19,suc(X_19))),
inference(subst,[],[axiom_014:[bind(Y,$fot(suc(X_19))),bind(Z,$fot(X_19))]]) ).
cnf(refute_0_56,plain,
( addNat(suc(X_19),suc(X_19)) != suc(addNat(X_19,suc(X_19)))
| double(suc(X_19)) != addNat(suc(X_19),suc(X_19))
| double(suc(X_19)) = suc(addNat(X_19,suc(X_19))) ),
introduced(tautology,[equality,[$cnf( $equal(double(suc(X_19)),addNat(suc(X_19),suc(X_19))) ),[1],$fot(suc(addNat(X_19,suc(X_19))))]]) ).
cnf(refute_0_57,plain,
( double(suc(X_19)) != addNat(suc(X_19),suc(X_19))
| double(suc(X_19)) = suc(addNat(X_19,suc(X_19))) ),
inference(resolve,[$cnf( $equal(addNat(suc(X_19),suc(X_19)),suc(addNat(X_19,suc(X_19)))) )],[refute_0_55,refute_0_56]) ).
cnf(refute_0_58,plain,
double(suc(X_19)) = suc(addNat(X_19,suc(X_19))),
inference(resolve,[$cnf( $equal(double(suc(X_19)),addNat(suc(X_19),suc(X_19))) )],[refute_0_54,refute_0_57]) ).
cnf(refute_0_59,plain,
double(suc(suc(zero))) = suc(addNat(suc(zero),suc(suc(zero)))),
inference(subst,[],[refute_0_58:[bind(X_19,$fot(suc(zero)))]]) ).
cnf(refute_0_60,plain,
double(suc(zero)) = suc(addNat(zero,suc(zero))),
inference(subst,[],[refute_0_58:[bind(X_19,$fot(zero))]]) ).
cnf(refute_0_61,plain,
addNat(zero,suc(zero)) = suc(zero),
inference(subst,[],[axiom_013:[bind(Y,$fot(suc(zero)))]]) ).
cnf(refute_0_62,plain,
( addNat(zero,suc(zero)) != suc(zero)
| double(suc(zero)) != suc(addNat(zero,suc(zero)))
| double(suc(zero)) = suc(suc(zero)) ),
introduced(tautology,[equality,[$cnf( $equal(double(suc(zero)),suc(addNat(zero,suc(zero)))) ),[1,0],$fot(suc(zero))]]) ).
cnf(refute_0_63,plain,
( double(suc(zero)) != suc(addNat(zero,suc(zero)))
| double(suc(zero)) = suc(suc(zero)) ),
inference(resolve,[$cnf( $equal(addNat(zero,suc(zero)),suc(zero)) )],[refute_0_61,refute_0_62]) ).
cnf(refute_0_64,plain,
double(suc(zero)) = suc(suc(zero)),
inference(resolve,[$cnf( $equal(double(suc(zero)),suc(addNat(zero,suc(zero)))) )],[refute_0_60,refute_0_63]) ).
cnf(refute_0_65,plain,
( double(suc(zero)) != suc(suc(zero))
| suc(suc(zero)) = double(suc(zero)) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(double(suc(zero)))),bind(Y0,$fot(suc(suc(zero))))]]) ).
cnf(refute_0_66,plain,
suc(suc(zero)) = double(suc(zero)),
inference(resolve,[$cnf( $equal(double(suc(zero)),suc(suc(zero))) )],[refute_0_64,refute_0_65]) ).
cnf(refute_0_67,plain,
( double(suc(suc(zero))) != suc(addNat(suc(zero),suc(suc(zero))))
| suc(suc(zero)) != double(suc(zero))
| double(suc(suc(zero))) = suc(addNat(suc(zero),double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(double(suc(suc(zero))),suc(addNat(suc(zero),suc(suc(zero))))) ),[1,0,1],$fot(double(suc(zero)))]]) ).
cnf(refute_0_68,plain,
( double(suc(suc(zero))) != suc(addNat(suc(zero),suc(suc(zero))))
| double(suc(suc(zero))) = suc(addNat(suc(zero),double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(suc(suc(zero)),double(suc(zero))) )],[refute_0_66,refute_0_67]) ).
cnf(refute_0_69,plain,
double(suc(suc(zero))) = suc(addNat(suc(zero),double(suc(zero)))),
inference(resolve,[$cnf( $equal(double(suc(suc(zero))),suc(addNat(suc(zero),suc(suc(zero))))) )],[refute_0_59,refute_0_68]) ).
cnf(refute_0_70,plain,
double(suc(suc(zero))) = double(suc(suc(zero))),
introduced(tautology,[refl,[$fot(double(suc(suc(zero))))]]) ).
cnf(refute_0_71,plain,
( double(suc(suc(zero))) != double(suc(suc(zero)))
| suc(suc(zero)) != double(suc(zero))
| double(suc(suc(zero))) = double(double(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(double(suc(suc(zero))),double(suc(suc(zero)))) ),[1,0],$fot(double(suc(zero)))]]) ).
cnf(refute_0_72,plain,
( suc(suc(zero)) != double(suc(zero))
| double(suc(suc(zero))) = double(double(suc(zero))) ),
inference(resolve,[$cnf( $equal(double(suc(suc(zero))),double(suc(suc(zero)))) )],[refute_0_70,refute_0_71]) ).
cnf(refute_0_73,plain,
double(suc(suc(zero))) = double(double(suc(zero))),
inference(resolve,[$cnf( $equal(suc(suc(zero)),double(suc(zero))) )],[refute_0_66,refute_0_72]) ).
cnf(refute_0_74,plain,
( double(suc(suc(zero))) != double(double(suc(zero)))
| double(suc(suc(zero))) != suc(addNat(suc(zero),double(suc(zero))))
| double(double(suc(zero))) = suc(addNat(suc(zero),double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(double(suc(suc(zero))),suc(addNat(suc(zero),double(suc(zero))))) ),[0],$fot(double(double(suc(zero))))]]) ).
cnf(refute_0_75,plain,
( double(suc(suc(zero))) != suc(addNat(suc(zero),double(suc(zero))))
| double(double(suc(zero))) = suc(addNat(suc(zero),double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(double(suc(suc(zero))),double(double(suc(zero)))) )],[refute_0_73,refute_0_74]) ).
cnf(refute_0_76,plain,
addNat(zero,double(suc(zero))) = double(suc(zero)),
inference(subst,[],[axiom_013:[bind(Y,$fot(double(suc(zero))))]]) ).
cnf(refute_0_77,plain,
suc(addNat(zero,double(suc(zero)))) = suc(addNat(zero,double(suc(zero)))),
introduced(tautology,[refl,[$fot(suc(addNat(zero,double(suc(zero)))))]]) ).
cnf(refute_0_78,plain,
( addNat(zero,double(suc(zero))) != double(suc(zero))
| suc(addNat(zero,double(suc(zero)))) != suc(addNat(zero,double(suc(zero))))
| suc(addNat(zero,double(suc(zero)))) = suc(double(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(suc(addNat(zero,double(suc(zero)))),suc(addNat(zero,double(suc(zero))))) ),[1,0],$fot(double(suc(zero)))]]) ).
cnf(refute_0_79,plain,
( addNat(zero,double(suc(zero))) != double(suc(zero))
| suc(addNat(zero,double(suc(zero)))) = suc(double(suc(zero))) ),
inference(resolve,[$cnf( $equal(suc(addNat(zero,double(suc(zero)))),suc(addNat(zero,double(suc(zero))))) )],[refute_0_77,refute_0_78]) ).
cnf(refute_0_80,plain,
suc(addNat(zero,double(suc(zero)))) = suc(double(suc(zero))),
inference(resolve,[$cnf( $equal(addNat(zero,double(suc(zero))),double(suc(zero))) )],[refute_0_76,refute_0_79]) ).
cnf(refute_0_81,plain,
addNat(suc(zero),double(suc(zero))) = suc(addNat(zero,double(suc(zero)))),
inference(subst,[],[axiom_014:[bind(Y,$fot(double(suc(zero)))),bind(Z,$fot(zero))]]) ).
cnf(refute_0_82,plain,
( Y0 != X0
| Y0 != Z0
| X0 = Z0 ),
introduced(tautology,[equality,[$cnf( $equal(Y0,Z0) ),[0],$fot(X0)]]) ).
cnf(refute_0_83,plain,
( X0 != Y0
| Y0 != Z0
| X0 = Z0 ),
inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_21,refute_0_82]) ).
cnf(refute_0_84,plain,
( addNat(suc(zero),double(suc(zero))) != suc(addNat(zero,double(suc(zero))))
| suc(addNat(zero,double(suc(zero)))) != suc(double(suc(zero)))
| addNat(suc(zero),double(suc(zero))) = suc(double(suc(zero))) ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(addNat(suc(zero),double(suc(zero))))),bind(Y0,$fot(suc(addNat(zero,double(suc(zero)))))),bind(Z0,$fot(suc(double(suc(zero)))))]]) ).
cnf(refute_0_85,plain,
( suc(addNat(zero,double(suc(zero)))) != suc(double(suc(zero)))
| addNat(suc(zero),double(suc(zero))) = suc(double(suc(zero))) ),
inference(resolve,[$cnf( $equal(addNat(suc(zero),double(suc(zero))),suc(addNat(zero,double(suc(zero))))) )],[refute_0_81,refute_0_84]) ).
cnf(refute_0_86,plain,
addNat(suc(zero),double(suc(zero))) = suc(double(suc(zero))),
inference(resolve,[$cnf( $equal(suc(addNat(zero,double(suc(zero)))),suc(double(suc(zero)))) )],[refute_0_80,refute_0_85]) ).
cnf(refute_0_87,plain,
suc(addNat(suc(zero),double(suc(zero)))) = suc(addNat(suc(zero),double(suc(zero)))),
introduced(tautology,[refl,[$fot(suc(addNat(suc(zero),double(suc(zero)))))]]) ).
cnf(refute_0_88,plain,
( addNat(suc(zero),double(suc(zero))) != suc(double(suc(zero)))
| suc(addNat(suc(zero),double(suc(zero)))) != suc(addNat(suc(zero),double(suc(zero))))
| suc(addNat(suc(zero),double(suc(zero)))) = suc(suc(double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(suc(addNat(suc(zero),double(suc(zero)))),suc(addNat(suc(zero),double(suc(zero))))) ),[1,0],$fot(suc(double(suc(zero))))]]) ).
cnf(refute_0_89,plain,
( addNat(suc(zero),double(suc(zero))) != suc(double(suc(zero)))
| suc(addNat(suc(zero),double(suc(zero)))) = suc(suc(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(suc(addNat(suc(zero),double(suc(zero)))),suc(addNat(suc(zero),double(suc(zero))))) )],[refute_0_87,refute_0_88]) ).
cnf(refute_0_90,plain,
suc(addNat(suc(zero),double(suc(zero)))) = suc(suc(double(suc(zero)))),
inference(resolve,[$cnf( $equal(addNat(suc(zero),double(suc(zero))),suc(double(suc(zero)))) )],[refute_0_86,refute_0_89]) ).
cnf(refute_0_91,plain,
( double(double(suc(zero))) != suc(addNat(suc(zero),double(suc(zero))))
| suc(addNat(suc(zero),double(suc(zero)))) != suc(suc(double(suc(zero))))
| double(double(suc(zero))) = suc(suc(double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( ~ $equal(double(double(suc(zero))),suc(suc(double(suc(zero))))) ),[0],$fot(suc(addNat(suc(zero),double(suc(zero)))))]]) ).
cnf(refute_0_92,plain,
( double(double(suc(zero))) != suc(addNat(suc(zero),double(suc(zero))))
| double(double(suc(zero))) = suc(suc(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(suc(addNat(suc(zero),double(suc(zero)))),suc(suc(double(suc(zero))))) )],[refute_0_90,refute_0_91]) ).
cnf(refute_0_93,plain,
( double(suc(suc(zero))) != suc(addNat(suc(zero),double(suc(zero))))
| double(double(suc(zero))) = suc(suc(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(double(double(suc(zero))),suc(addNat(suc(zero),double(suc(zero))))) )],[refute_0_75,refute_0_92]) ).
cnf(refute_0_94,plain,
double(double(suc(zero))) = suc(suc(double(suc(zero)))),
inference(resolve,[$cnf( $equal(double(suc(suc(zero))),suc(addNat(suc(zero),double(suc(zero))))) )],[refute_0_69,refute_0_93]) ).
cnf(refute_0_95,plain,
( double(double(suc(zero))) != suc(suc(double(suc(zero))))
| suc(suc(double(suc(zero)))) = double(double(suc(zero))) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(double(double(suc(zero))))),bind(Y0,$fot(suc(suc(double(suc(zero))))))]]) ).
cnf(refute_0_96,plain,
suc(suc(double(suc(zero)))) = double(double(suc(zero))),
inference(resolve,[$cnf( $equal(double(double(suc(zero))),suc(suc(double(suc(zero))))) )],[refute_0_94,refute_0_95]) ).
cnf(refute_0_97,plain,
( half(suc(suc(suc(double(suc(zero)))))) != suc(half(suc(double(suc(zero)))))
| suc(suc(double(suc(zero)))) != double(double(suc(zero)))
| half(suc(double(double(suc(zero))))) = suc(half(suc(double(suc(zero))))) ),
introduced(tautology,[equality,[$cnf( $equal(half(suc(suc(suc(double(suc(zero)))))),suc(half(suc(double(suc(zero)))))) ),[0,0,0],$fot(double(double(suc(zero))))]]) ).
cnf(refute_0_98,plain,
( half(suc(suc(suc(double(suc(zero)))))) != suc(half(suc(double(suc(zero)))))
| half(suc(double(double(suc(zero))))) = suc(half(suc(double(suc(zero))))) ),
inference(resolve,[$cnf( $equal(suc(suc(double(suc(zero)))),double(double(suc(zero)))) )],[refute_0_96,refute_0_97]) ).
cnf(refute_0_99,plain,
half(suc(double(double(suc(zero))))) = suc(half(suc(double(suc(zero))))),
inference(resolve,[$cnf( $equal(half(suc(suc(suc(double(suc(zero)))))),suc(half(suc(double(suc(zero)))))) )],[refute_0_53,refute_0_98]) ).
cnf(refute_0_100,plain,
half(suc(suc(suc(zero)))) = suc(half(suc(zero))),
inference(subst,[],[axiom_006:[bind(N,$fot(suc(zero)))]]) ).
cnf(refute_0_101,plain,
( half(suc(suc(suc(zero)))) != suc(half(suc(zero)))
| suc(suc(zero)) != double(suc(zero))
| half(suc(double(suc(zero)))) = suc(half(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(half(suc(suc(suc(zero)))),suc(half(suc(zero)))) ),[0,0,0],$fot(double(suc(zero)))]]) ).
cnf(refute_0_102,plain,
( half(suc(suc(suc(zero)))) != suc(half(suc(zero)))
| half(suc(double(suc(zero)))) = suc(half(suc(zero))) ),
inference(resolve,[$cnf( $equal(suc(suc(zero)),double(suc(zero))) )],[refute_0_66,refute_0_101]) ).
cnf(refute_0_103,plain,
half(suc(double(suc(zero)))) = suc(half(suc(zero))),
inference(resolve,[$cnf( $equal(half(suc(suc(suc(zero)))),suc(half(suc(zero)))) )],[refute_0_100,refute_0_102]) ).
cnf(refute_0_104,plain,
suc(half(suc(zero))) = suc(half(suc(zero))),
introduced(tautology,[refl,[$fot(suc(half(suc(zero))))]]) ).
cnf(refute_0_105,plain,
( half(suc(zero)) != zero
| suc(half(suc(zero))) != suc(half(suc(zero)))
| suc(half(suc(zero))) = suc(zero) ),
introduced(tautology,[equality,[$cnf( $equal(suc(half(suc(zero))),suc(half(suc(zero)))) ),[1,0],$fot(zero)]]) ).
cnf(refute_0_106,plain,
( half(suc(zero)) != zero
| suc(half(suc(zero))) = suc(zero) ),
inference(resolve,[$cnf( $equal(suc(half(suc(zero))),suc(half(suc(zero)))) )],[refute_0_104,refute_0_105]) ).
cnf(refute_0_107,plain,
suc(half(suc(zero))) = suc(zero),
inference(resolve,[$cnf( $equal(half(suc(zero)),zero) )],[axiom_005,refute_0_106]) ).
cnf(refute_0_108,plain,
( half(suc(double(suc(zero)))) != suc(half(suc(zero)))
| suc(half(suc(zero))) != suc(zero)
| half(suc(double(suc(zero)))) = suc(zero) ),
introduced(tautology,[equality,[$cnf( ~ $equal(half(suc(double(suc(zero)))),suc(zero)) ),[0],$fot(suc(half(suc(zero))))]]) ).
cnf(refute_0_109,plain,
( half(suc(double(suc(zero)))) != suc(half(suc(zero)))
| half(suc(double(suc(zero)))) = suc(zero) ),
inference(resolve,[$cnf( $equal(suc(half(suc(zero))),suc(zero)) )],[refute_0_107,refute_0_108]) ).
cnf(refute_0_110,plain,
half(suc(double(suc(zero)))) = suc(zero),
inference(resolve,[$cnf( $equal(half(suc(double(suc(zero)))),suc(half(suc(zero)))) )],[refute_0_103,refute_0_109]) ).
cnf(refute_0_111,plain,
suc(half(suc(double(suc(zero))))) = suc(half(suc(double(suc(zero))))),
introduced(tautology,[refl,[$fot(suc(half(suc(double(suc(zero))))))]]) ).
cnf(refute_0_112,plain,
( half(suc(double(suc(zero)))) != suc(zero)
| suc(half(suc(double(suc(zero))))) != suc(half(suc(double(suc(zero)))))
| suc(half(suc(double(suc(zero))))) = suc(suc(zero)) ),
introduced(tautology,[equality,[$cnf( $equal(suc(half(suc(double(suc(zero))))),suc(half(suc(double(suc(zero)))))) ),[1,0],$fot(suc(zero))]]) ).
cnf(refute_0_113,plain,
( half(suc(double(suc(zero)))) != suc(zero)
| suc(half(suc(double(suc(zero))))) = suc(suc(zero)) ),
inference(resolve,[$cnf( $equal(suc(half(suc(double(suc(zero))))),suc(half(suc(double(suc(zero)))))) )],[refute_0_111,refute_0_112]) ).
cnf(refute_0_114,plain,
suc(half(suc(double(suc(zero))))) = suc(suc(zero)),
inference(resolve,[$cnf( $equal(half(suc(double(suc(zero)))),suc(zero)) )],[refute_0_110,refute_0_113]) ).
cnf(refute_0_115,plain,
( suc(half(suc(double(suc(zero))))) != suc(suc(zero))
| suc(suc(zero)) != double(suc(zero))
| suc(half(suc(double(suc(zero))))) = double(suc(zero)) ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(suc(half(suc(double(suc(zero))))))),bind(Y0,$fot(suc(suc(zero)))),bind(Z0,$fot(double(suc(zero))))]]) ).
cnf(refute_0_116,plain,
( suc(suc(zero)) != double(suc(zero))
| suc(half(suc(double(suc(zero))))) = double(suc(zero)) ),
inference(resolve,[$cnf( $equal(suc(half(suc(double(suc(zero))))),suc(suc(zero))) )],[refute_0_114,refute_0_115]) ).
cnf(refute_0_117,plain,
suc(half(suc(double(suc(zero))))) = double(suc(zero)),
inference(resolve,[$cnf( $equal(suc(suc(zero)),double(suc(zero))) )],[refute_0_66,refute_0_116]) ).
cnf(refute_0_118,plain,
( half(suc(double(double(suc(zero))))) != suc(half(suc(double(suc(zero)))))
| suc(half(suc(double(suc(zero))))) != double(suc(zero))
| half(suc(double(double(suc(zero))))) = double(suc(zero)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(half(suc(double(double(suc(zero))))),double(suc(zero))) ),[0],$fot(suc(half(suc(double(suc(zero))))))]]) ).
cnf(refute_0_119,plain,
( half(suc(double(double(suc(zero))))) != suc(half(suc(double(suc(zero)))))
| half(suc(double(double(suc(zero))))) = double(suc(zero)) ),
inference(resolve,[$cnf( $equal(suc(half(suc(double(suc(zero))))),double(suc(zero))) )],[refute_0_117,refute_0_118]) ).
cnf(refute_0_120,plain,
half(suc(double(double(suc(zero))))) = double(suc(zero)),
inference(resolve,[$cnf( $equal(half(suc(double(double(suc(zero))))),suc(half(suc(double(suc(zero)))))) )],[refute_0_99,refute_0_119]) ).
cnf(refute_0_121,plain,
( aux(double(double(suc(zero))),bfalse) != cons(i,shw(half(suc(double(double(suc(zero)))))))
| half(suc(double(double(suc(zero))))) != double(suc(zero))
| aux(double(double(suc(zero))),bfalse) = cons(i,shw(double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(aux(double(double(suc(zero))),bfalse),cons(i,shw(half(suc(double(double(suc(zero)))))))) ),[1,1,0],$fot(double(suc(zero)))]]) ).
cnf(refute_0_122,plain,
( aux(double(double(suc(zero))),bfalse) != cons(i,shw(half(suc(double(double(suc(zero)))))))
| aux(double(double(suc(zero))),bfalse) = cons(i,shw(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(half(suc(double(double(suc(zero))))),double(suc(zero))) )],[refute_0_120,refute_0_121]) ).
cnf(refute_0_123,plain,
aux(double(double(suc(zero))),bfalse) = cons(i,shw(double(suc(zero)))),
inference(resolve,[$cnf( $equal(aux(double(double(suc(zero))),bfalse),cons(i,shw(half(suc(double(double(suc(zero)))))))) )],[refute_0_52,refute_0_122]) ).
cnf(refute_0_124,plain,
shw(suc(suc(suc(suc(suc(zero)))))) = aux(suc(suc(suc(suc(zero)))),evenNat(suc(suc(suc(suc(suc(zero))))))),
inference(subst,[],[axiom_010:[bind(Y,$fot(suc(suc(suc(suc(zero))))))]]) ).
cnf(refute_0_125,plain,
evenNat(suc(suc(suc(suc(suc(zero)))))) = notb(evenNat(suc(suc(suc(suc(zero)))))),
inference(subst,[],[axiom_008:[bind(N,$fot(suc(suc(suc(suc(zero))))))]]) ).
cnf(refute_0_126,plain,
evenNat(suc(suc(suc(suc(zero))))) = notb(evenNat(suc(suc(suc(zero))))),
inference(subst,[],[axiom_008:[bind(N,$fot(suc(suc(suc(zero)))))]]) ).
cnf(refute_0_127,plain,
evenNat(suc(suc(suc(zero)))) = notb(evenNat(suc(suc(zero)))),
inference(subst,[],[axiom_008:[bind(N,$fot(suc(suc(zero))))]]) ).
cnf(refute_0_128,plain,
evenNat(suc(suc(zero))) = notb(evenNat(suc(zero))),
inference(subst,[],[axiom_008:[bind(N,$fot(suc(zero)))]]) ).
cnf(refute_0_129,plain,
( evenNat(suc(suc(zero))) != notb(evenNat(suc(zero)))
| evenNat(suc(zero)) != bfalse
| evenNat(suc(suc(zero))) = notb(bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(evenNat(suc(suc(zero))),notb(evenNat(suc(zero)))) ),[1,0],$fot(bfalse)]]) ).
cnf(refute_0_130,plain,
( evenNat(suc(suc(zero))) != notb(evenNat(suc(zero)))
| evenNat(suc(suc(zero))) = notb(bfalse) ),
inference(resolve,[$cnf( $equal(evenNat(suc(zero)),bfalse) )],[refute_0_15,refute_0_129]) ).
cnf(refute_0_131,plain,
evenNat(suc(suc(zero))) = notb(bfalse),
inference(resolve,[$cnf( $equal(evenNat(suc(suc(zero))),notb(evenNat(suc(zero)))) )],[refute_0_128,refute_0_130]) ).
cnf(refute_0_132,plain,
( evenNat(suc(suc(zero))) != notb(bfalse)
| notb(bfalse) != btrue
| evenNat(suc(suc(zero))) = btrue ),
introduced(tautology,[equality,[$cnf( ~ $equal(evenNat(suc(suc(zero))),btrue) ),[0],$fot(notb(bfalse))]]) ).
cnf(refute_0_133,plain,
( evenNat(suc(suc(zero))) != notb(bfalse)
| evenNat(suc(suc(zero))) = btrue ),
inference(resolve,[$cnf( $equal(notb(bfalse),btrue) )],[axiom_003,refute_0_132]) ).
cnf(refute_0_134,plain,
evenNat(suc(suc(zero))) = btrue,
inference(resolve,[$cnf( $equal(evenNat(suc(suc(zero))),notb(bfalse)) )],[refute_0_131,refute_0_133]) ).
cnf(refute_0_135,plain,
( evenNat(suc(suc(suc(zero)))) != notb(evenNat(suc(suc(zero))))
| evenNat(suc(suc(zero))) != btrue
| evenNat(suc(suc(suc(zero)))) = notb(btrue) ),
introduced(tautology,[equality,[$cnf( $equal(evenNat(suc(suc(suc(zero)))),notb(evenNat(suc(suc(zero))))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_136,plain,
( evenNat(suc(suc(suc(zero)))) != notb(evenNat(suc(suc(zero))))
| evenNat(suc(suc(suc(zero)))) = notb(btrue) ),
inference(resolve,[$cnf( $equal(evenNat(suc(suc(zero))),btrue) )],[refute_0_134,refute_0_135]) ).
cnf(refute_0_137,plain,
evenNat(suc(suc(suc(zero)))) = notb(btrue),
inference(resolve,[$cnf( $equal(evenNat(suc(suc(suc(zero)))),notb(evenNat(suc(suc(zero))))) )],[refute_0_127,refute_0_136]) ).
cnf(refute_0_138,plain,
( evenNat(suc(suc(suc(zero)))) != notb(btrue)
| notb(btrue) != bfalse
| evenNat(suc(suc(suc(zero)))) = bfalse ),
introduced(tautology,[equality,[$cnf( ~ $equal(evenNat(suc(suc(suc(zero)))),bfalse) ),[0],$fot(notb(btrue))]]) ).
cnf(refute_0_139,plain,
( evenNat(suc(suc(suc(zero)))) != notb(btrue)
| evenNat(suc(suc(suc(zero)))) = bfalse ),
inference(resolve,[$cnf( $equal(notb(btrue),bfalse) )],[axiom_002,refute_0_138]) ).
cnf(refute_0_140,plain,
evenNat(suc(suc(suc(zero)))) = bfalse,
inference(resolve,[$cnf( $equal(evenNat(suc(suc(suc(zero)))),notb(btrue)) )],[refute_0_137,refute_0_139]) ).
cnf(refute_0_141,plain,
( evenNat(suc(suc(suc(suc(zero))))) != notb(evenNat(suc(suc(suc(zero)))))
| evenNat(suc(suc(suc(zero)))) != bfalse
| evenNat(suc(suc(suc(suc(zero))))) = notb(bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(evenNat(suc(suc(suc(suc(zero))))),notb(evenNat(suc(suc(suc(zero)))))) ),[1,0],$fot(bfalse)]]) ).
cnf(refute_0_142,plain,
( evenNat(suc(suc(suc(suc(zero))))) != notb(evenNat(suc(suc(suc(zero)))))
| evenNat(suc(suc(suc(suc(zero))))) = notb(bfalse) ),
inference(resolve,[$cnf( $equal(evenNat(suc(suc(suc(zero)))),bfalse) )],[refute_0_140,refute_0_141]) ).
cnf(refute_0_143,plain,
evenNat(suc(suc(suc(suc(zero))))) = notb(bfalse),
inference(resolve,[$cnf( $equal(evenNat(suc(suc(suc(suc(zero))))),notb(evenNat(suc(suc(suc(zero)))))) )],[refute_0_126,refute_0_142]) ).
cnf(refute_0_144,plain,
( evenNat(suc(suc(suc(suc(zero))))) != notb(bfalse)
| notb(bfalse) != btrue
| evenNat(suc(suc(suc(suc(zero))))) = btrue ),
introduced(tautology,[equality,[$cnf( ~ $equal(evenNat(suc(suc(suc(suc(zero))))),btrue) ),[0],$fot(notb(bfalse))]]) ).
cnf(refute_0_145,plain,
( evenNat(suc(suc(suc(suc(zero))))) != notb(bfalse)
| evenNat(suc(suc(suc(suc(zero))))) = btrue ),
inference(resolve,[$cnf( $equal(notb(bfalse),btrue) )],[axiom_003,refute_0_144]) ).
cnf(refute_0_146,plain,
evenNat(suc(suc(suc(suc(zero))))) = btrue,
inference(resolve,[$cnf( $equal(evenNat(suc(suc(suc(suc(zero))))),notb(bfalse)) )],[refute_0_143,refute_0_145]) ).
cnf(refute_0_147,plain,
( evenNat(suc(suc(suc(suc(suc(zero)))))) != notb(evenNat(suc(suc(suc(suc(zero))))))
| evenNat(suc(suc(suc(suc(zero))))) != btrue
| evenNat(suc(suc(suc(suc(suc(zero)))))) = notb(btrue) ),
introduced(tautology,[equality,[$cnf( $equal(evenNat(suc(suc(suc(suc(suc(zero)))))),notb(evenNat(suc(suc(suc(suc(zero))))))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_148,plain,
( evenNat(suc(suc(suc(suc(suc(zero)))))) != notb(evenNat(suc(suc(suc(suc(zero))))))
| evenNat(suc(suc(suc(suc(suc(zero)))))) = notb(btrue) ),
inference(resolve,[$cnf( $equal(evenNat(suc(suc(suc(suc(zero))))),btrue) )],[refute_0_146,refute_0_147]) ).
cnf(refute_0_149,plain,
evenNat(suc(suc(suc(suc(suc(zero)))))) = notb(btrue),
inference(resolve,[$cnf( $equal(evenNat(suc(suc(suc(suc(suc(zero)))))),notb(evenNat(suc(suc(suc(suc(zero))))))) )],[refute_0_125,refute_0_148]) ).
cnf(refute_0_150,plain,
( evenNat(suc(suc(suc(suc(suc(zero)))))) != notb(btrue)
| notb(btrue) != bfalse
| evenNat(suc(suc(suc(suc(suc(zero)))))) = bfalse ),
introduced(tautology,[equality,[$cnf( ~ $equal(evenNat(suc(suc(suc(suc(suc(zero)))))),bfalse) ),[0],$fot(notb(btrue))]]) ).
cnf(refute_0_151,plain,
( evenNat(suc(suc(suc(suc(suc(zero)))))) != notb(btrue)
| evenNat(suc(suc(suc(suc(suc(zero)))))) = bfalse ),
inference(resolve,[$cnf( $equal(notb(btrue),bfalse) )],[axiom_002,refute_0_150]) ).
cnf(refute_0_152,plain,
evenNat(suc(suc(suc(suc(suc(zero)))))) = bfalse,
inference(resolve,[$cnf( $equal(evenNat(suc(suc(suc(suc(suc(zero)))))),notb(btrue)) )],[refute_0_149,refute_0_151]) ).
cnf(refute_0_153,plain,
( evenNat(suc(suc(suc(suc(suc(zero)))))) != bfalse
| shw(suc(suc(suc(suc(suc(zero)))))) != aux(suc(suc(suc(suc(zero)))),evenNat(suc(suc(suc(suc(suc(zero)))))))
| shw(suc(suc(suc(suc(suc(zero)))))) = aux(suc(suc(suc(suc(zero)))),bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(shw(suc(suc(suc(suc(suc(zero)))))),aux(suc(suc(suc(suc(zero)))),evenNat(suc(suc(suc(suc(suc(zero)))))))) ),[1,1],$fot(bfalse)]]) ).
cnf(refute_0_154,plain,
( shw(suc(suc(suc(suc(suc(zero)))))) != aux(suc(suc(suc(suc(zero)))),evenNat(suc(suc(suc(suc(suc(zero)))))))
| shw(suc(suc(suc(suc(suc(zero)))))) = aux(suc(suc(suc(suc(zero)))),bfalse) ),
inference(resolve,[$cnf( $equal(evenNat(suc(suc(suc(suc(suc(zero)))))),bfalse) )],[refute_0_152,refute_0_153]) ).
cnf(refute_0_155,plain,
shw(suc(suc(suc(suc(suc(zero)))))) = aux(suc(suc(suc(suc(zero)))),bfalse),
inference(resolve,[$cnf( $equal(shw(suc(suc(suc(suc(suc(zero)))))),aux(suc(suc(suc(suc(zero)))),evenNat(suc(suc(suc(suc(suc(zero)))))))) )],[refute_0_124,refute_0_154]) ).
cnf(refute_0_156,plain,
suc(suc(suc(zero))) = suc(suc(suc(zero))),
introduced(tautology,[refl,[$fot(suc(suc(suc(zero))))]]) ).
cnf(refute_0_157,plain,
( suc(suc(suc(zero))) != suc(suc(suc(zero)))
| suc(suc(zero)) != double(suc(zero))
| suc(suc(suc(zero))) = suc(double(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(suc(suc(suc(zero))),suc(suc(suc(zero)))) ),[1,0],$fot(double(suc(zero)))]]) ).
cnf(refute_0_158,plain,
( suc(suc(zero)) != double(suc(zero))
| suc(suc(suc(zero))) = suc(double(suc(zero))) ),
inference(resolve,[$cnf( $equal(suc(suc(suc(zero))),suc(suc(suc(zero)))) )],[refute_0_156,refute_0_157]) ).
cnf(refute_0_159,plain,
suc(suc(suc(zero))) = suc(double(suc(zero))),
inference(resolve,[$cnf( $equal(suc(suc(zero)),double(suc(zero))) )],[refute_0_66,refute_0_158]) ).
cnf(refute_0_160,plain,
suc(suc(suc(suc(zero)))) = suc(suc(suc(suc(zero)))),
introduced(tautology,[refl,[$fot(suc(suc(suc(suc(zero)))))]]) ).
cnf(refute_0_161,plain,
( suc(suc(suc(suc(zero)))) != suc(suc(suc(suc(zero))))
| suc(suc(suc(zero))) != suc(double(suc(zero)))
| suc(suc(suc(suc(zero)))) = suc(suc(double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(suc(suc(suc(suc(zero)))),suc(suc(suc(suc(zero))))) ),[1,0],$fot(suc(double(suc(zero))))]]) ).
cnf(refute_0_162,plain,
( suc(suc(suc(zero))) != suc(double(suc(zero)))
| suc(suc(suc(suc(zero)))) = suc(suc(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(suc(suc(suc(suc(zero)))),suc(suc(suc(suc(zero))))) )],[refute_0_160,refute_0_161]) ).
cnf(refute_0_163,plain,
suc(suc(suc(suc(zero)))) = suc(suc(double(suc(zero)))),
inference(resolve,[$cnf( $equal(suc(suc(suc(zero))),suc(double(suc(zero)))) )],[refute_0_159,refute_0_162]) ).
cnf(refute_0_164,plain,
suc(suc(suc(suc(suc(zero))))) = suc(suc(suc(suc(suc(zero))))),
introduced(tautology,[refl,[$fot(suc(suc(suc(suc(suc(zero))))))]]) ).
cnf(refute_0_165,plain,
( suc(suc(suc(suc(suc(zero))))) != suc(suc(suc(suc(suc(zero)))))
| suc(suc(suc(suc(zero)))) != suc(suc(double(suc(zero))))
| suc(suc(suc(suc(suc(zero))))) = suc(suc(suc(double(suc(zero))))) ),
introduced(tautology,[equality,[$cnf( $equal(suc(suc(suc(suc(suc(zero))))),suc(suc(suc(suc(suc(zero)))))) ),[1,0],$fot(suc(suc(double(suc(zero)))))]]) ).
cnf(refute_0_166,plain,
( suc(suc(suc(suc(zero)))) != suc(suc(double(suc(zero))))
| suc(suc(suc(suc(suc(zero))))) = suc(suc(suc(double(suc(zero))))) ),
inference(resolve,[$cnf( $equal(suc(suc(suc(suc(suc(zero))))),suc(suc(suc(suc(suc(zero)))))) )],[refute_0_164,refute_0_165]) ).
cnf(refute_0_167,plain,
suc(suc(suc(suc(suc(zero))))) = suc(suc(suc(double(suc(zero))))),
inference(resolve,[$cnf( $equal(suc(suc(suc(suc(zero)))),suc(suc(double(suc(zero))))) )],[refute_0_163,refute_0_166]) ).
cnf(refute_0_168,plain,
shw(suc(suc(suc(suc(suc(zero)))))) = shw(suc(suc(suc(suc(suc(zero)))))),
introduced(tautology,[refl,[$fot(shw(suc(suc(suc(suc(suc(zero)))))))]]) ).
cnf(refute_0_169,plain,
( shw(suc(suc(suc(suc(suc(zero)))))) != shw(suc(suc(suc(suc(suc(zero))))))
| suc(suc(suc(suc(suc(zero))))) != suc(suc(suc(double(suc(zero)))))
| shw(suc(suc(suc(suc(suc(zero)))))) = shw(suc(suc(suc(double(suc(zero)))))) ),
introduced(tautology,[equality,[$cnf( $equal(shw(suc(suc(suc(suc(suc(zero)))))),shw(suc(suc(suc(suc(suc(zero))))))) ),[1,0],$fot(suc(suc(suc(double(suc(zero))))))]]) ).
cnf(refute_0_170,plain,
( suc(suc(suc(suc(suc(zero))))) != suc(suc(suc(double(suc(zero)))))
| shw(suc(suc(suc(suc(suc(zero)))))) = shw(suc(suc(suc(double(suc(zero)))))) ),
inference(resolve,[$cnf( $equal(shw(suc(suc(suc(suc(suc(zero)))))),shw(suc(suc(suc(suc(suc(zero))))))) )],[refute_0_168,refute_0_169]) ).
cnf(refute_0_171,plain,
shw(suc(suc(suc(suc(suc(zero)))))) = shw(suc(suc(suc(double(suc(zero)))))),
inference(resolve,[$cnf( $equal(suc(suc(suc(suc(suc(zero))))),suc(suc(suc(double(suc(zero)))))) )],[refute_0_167,refute_0_170]) ).
cnf(refute_0_172,plain,
( shw(suc(suc(suc(suc(suc(zero)))))) != aux(suc(suc(suc(suc(zero)))),bfalse)
| shw(suc(suc(suc(suc(suc(zero)))))) != shw(suc(suc(suc(double(suc(zero))))))
| shw(suc(suc(suc(double(suc(zero)))))) = aux(suc(suc(suc(suc(zero)))),bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(shw(suc(suc(suc(suc(suc(zero)))))),aux(suc(suc(suc(suc(zero)))),bfalse)) ),[0],$fot(shw(suc(suc(suc(double(suc(zero)))))))]]) ).
cnf(refute_0_173,plain,
( shw(suc(suc(suc(suc(suc(zero)))))) != aux(suc(suc(suc(suc(zero)))),bfalse)
| shw(suc(suc(suc(double(suc(zero)))))) = aux(suc(suc(suc(suc(zero)))),bfalse) ),
inference(resolve,[$cnf( $equal(shw(suc(suc(suc(suc(suc(zero)))))),shw(suc(suc(suc(double(suc(zero))))))) )],[refute_0_171,refute_0_172]) ).
cnf(refute_0_174,plain,
aux(suc(suc(suc(suc(zero)))),bfalse) = aux(suc(suc(suc(suc(zero)))),bfalse),
introduced(tautology,[refl,[$fot(aux(suc(suc(suc(suc(zero)))),bfalse))]]) ).
cnf(refute_0_175,plain,
( aux(suc(suc(suc(suc(zero)))),bfalse) != aux(suc(suc(suc(suc(zero)))),bfalse)
| suc(suc(suc(suc(zero)))) != suc(suc(double(suc(zero))))
| aux(suc(suc(suc(suc(zero)))),bfalse) = aux(suc(suc(double(suc(zero)))),bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(aux(suc(suc(suc(suc(zero)))),bfalse),aux(suc(suc(suc(suc(zero)))),bfalse)) ),[1,0],$fot(suc(suc(double(suc(zero)))))]]) ).
cnf(refute_0_176,plain,
( suc(suc(suc(suc(zero)))) != suc(suc(double(suc(zero))))
| aux(suc(suc(suc(suc(zero)))),bfalse) = aux(suc(suc(double(suc(zero)))),bfalse) ),
inference(resolve,[$cnf( $equal(aux(suc(suc(suc(suc(zero)))),bfalse),aux(suc(suc(suc(suc(zero)))),bfalse)) )],[refute_0_174,refute_0_175]) ).
cnf(refute_0_177,plain,
aux(suc(suc(suc(suc(zero)))),bfalse) = aux(suc(suc(double(suc(zero)))),bfalse),
inference(resolve,[$cnf( $equal(suc(suc(suc(suc(zero)))),suc(suc(double(suc(zero))))) )],[refute_0_163,refute_0_176]) ).
cnf(refute_0_178,plain,
( aux(suc(suc(suc(suc(zero)))),bfalse) != aux(suc(suc(double(suc(zero)))),bfalse)
| shw(suc(suc(suc(double(suc(zero)))))) != aux(suc(suc(suc(suc(zero)))),bfalse)
| shw(suc(suc(suc(double(suc(zero)))))) = aux(suc(suc(double(suc(zero)))),bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(shw(suc(suc(suc(double(suc(zero)))))),aux(suc(suc(suc(suc(zero)))),bfalse)) ),[1],$fot(aux(suc(suc(double(suc(zero)))),bfalse))]]) ).
cnf(refute_0_179,plain,
( shw(suc(suc(suc(double(suc(zero)))))) != aux(suc(suc(suc(suc(zero)))),bfalse)
| shw(suc(suc(suc(double(suc(zero)))))) = aux(suc(suc(double(suc(zero)))),bfalse) ),
inference(resolve,[$cnf( $equal(aux(suc(suc(suc(suc(zero)))),bfalse),aux(suc(suc(double(suc(zero)))),bfalse)) )],[refute_0_177,refute_0_178]) ).
cnf(refute_0_180,plain,
( shw(suc(suc(suc(suc(suc(zero)))))) != aux(suc(suc(suc(suc(zero)))),bfalse)
| shw(suc(suc(suc(double(suc(zero)))))) = aux(suc(suc(double(suc(zero)))),bfalse) ),
inference(resolve,[$cnf( $equal(shw(suc(suc(suc(double(suc(zero)))))),aux(suc(suc(suc(suc(zero)))),bfalse)) )],[refute_0_173,refute_0_179]) ).
cnf(refute_0_181,plain,
shw(suc(suc(suc(double(suc(zero)))))) = aux(suc(suc(double(suc(zero)))),bfalse),
inference(resolve,[$cnf( $equal(shw(suc(suc(suc(suc(suc(zero)))))),aux(suc(suc(suc(suc(zero)))),bfalse)) )],[refute_0_155,refute_0_180]) ).
cnf(refute_0_182,plain,
suc(suc(suc(double(suc(zero))))) = suc(suc(suc(double(suc(zero))))),
introduced(tautology,[refl,[$fot(suc(suc(suc(double(suc(zero))))))]]) ).
cnf(refute_0_183,plain,
( suc(suc(double(suc(zero)))) != double(double(suc(zero)))
| suc(suc(suc(double(suc(zero))))) != suc(suc(suc(double(suc(zero)))))
| suc(suc(suc(double(suc(zero))))) = suc(double(double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(suc(suc(suc(double(suc(zero))))),suc(suc(suc(double(suc(zero)))))) ),[1,0],$fot(double(double(suc(zero))))]]) ).
cnf(refute_0_184,plain,
( suc(suc(double(suc(zero)))) != double(double(suc(zero)))
| suc(suc(suc(double(suc(zero))))) = suc(double(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(suc(suc(suc(double(suc(zero))))),suc(suc(suc(double(suc(zero)))))) )],[refute_0_182,refute_0_183]) ).
cnf(refute_0_185,plain,
suc(suc(suc(double(suc(zero))))) = suc(double(double(suc(zero)))),
inference(resolve,[$cnf( $equal(suc(suc(double(suc(zero)))),double(double(suc(zero)))) )],[refute_0_96,refute_0_184]) ).
cnf(refute_0_186,plain,
shw(suc(suc(suc(double(suc(zero)))))) = shw(suc(suc(suc(double(suc(zero)))))),
introduced(tautology,[refl,[$fot(shw(suc(suc(suc(double(suc(zero)))))))]]) ).
cnf(refute_0_187,plain,
( shw(suc(suc(suc(double(suc(zero)))))) != shw(suc(suc(suc(double(suc(zero))))))
| suc(suc(suc(double(suc(zero))))) != suc(double(double(suc(zero))))
| shw(suc(suc(suc(double(suc(zero)))))) = shw(suc(double(double(suc(zero))))) ),
introduced(tautology,[equality,[$cnf( $equal(shw(suc(suc(suc(double(suc(zero)))))),shw(suc(suc(suc(double(suc(zero))))))) ),[1,0],$fot(suc(double(double(suc(zero)))))]]) ).
cnf(refute_0_188,plain,
( suc(suc(suc(double(suc(zero))))) != suc(double(double(suc(zero))))
| shw(suc(suc(suc(double(suc(zero)))))) = shw(suc(double(double(suc(zero))))) ),
inference(resolve,[$cnf( $equal(shw(suc(suc(suc(double(suc(zero)))))),shw(suc(suc(suc(double(suc(zero))))))) )],[refute_0_186,refute_0_187]) ).
cnf(refute_0_189,plain,
shw(suc(suc(suc(double(suc(zero)))))) = shw(suc(double(double(suc(zero))))),
inference(resolve,[$cnf( $equal(suc(suc(suc(double(suc(zero))))),suc(double(double(suc(zero))))) )],[refute_0_185,refute_0_188]) ).
cnf(refute_0_190,plain,
( shw(suc(suc(suc(double(suc(zero)))))) != aux(suc(suc(double(suc(zero)))),bfalse)
| shw(suc(suc(suc(double(suc(zero)))))) != shw(suc(double(double(suc(zero)))))
| shw(suc(double(double(suc(zero))))) = aux(suc(suc(double(suc(zero)))),bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(shw(suc(suc(suc(double(suc(zero)))))),aux(suc(suc(double(suc(zero)))),bfalse)) ),[0],$fot(shw(suc(double(double(suc(zero))))))]]) ).
cnf(refute_0_191,plain,
( shw(suc(suc(suc(double(suc(zero)))))) != aux(suc(suc(double(suc(zero)))),bfalse)
| shw(suc(double(double(suc(zero))))) = aux(suc(suc(double(suc(zero)))),bfalse) ),
inference(resolve,[$cnf( $equal(shw(suc(suc(suc(double(suc(zero)))))),shw(suc(double(double(suc(zero)))))) )],[refute_0_189,refute_0_190]) ).
cnf(refute_0_192,plain,
aux(suc(suc(double(suc(zero)))),bfalse) = aux(suc(suc(double(suc(zero)))),bfalse),
introduced(tautology,[refl,[$fot(aux(suc(suc(double(suc(zero)))),bfalse))]]) ).
cnf(refute_0_193,plain,
( aux(suc(suc(double(suc(zero)))),bfalse) != aux(suc(suc(double(suc(zero)))),bfalse)
| suc(suc(double(suc(zero)))) != double(double(suc(zero)))
| aux(suc(suc(double(suc(zero)))),bfalse) = aux(double(double(suc(zero))),bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(aux(suc(suc(double(suc(zero)))),bfalse),aux(suc(suc(double(suc(zero)))),bfalse)) ),[1,0],$fot(double(double(suc(zero))))]]) ).
cnf(refute_0_194,plain,
( suc(suc(double(suc(zero)))) != double(double(suc(zero)))
| aux(suc(suc(double(suc(zero)))),bfalse) = aux(double(double(suc(zero))),bfalse) ),
inference(resolve,[$cnf( $equal(aux(suc(suc(double(suc(zero)))),bfalse),aux(suc(suc(double(suc(zero)))),bfalse)) )],[refute_0_192,refute_0_193]) ).
cnf(refute_0_195,plain,
aux(suc(suc(double(suc(zero)))),bfalse) = aux(double(double(suc(zero))),bfalse),
inference(resolve,[$cnf( $equal(suc(suc(double(suc(zero)))),double(double(suc(zero)))) )],[refute_0_96,refute_0_194]) ).
cnf(refute_0_196,plain,
( aux(suc(suc(double(suc(zero)))),bfalse) != aux(double(double(suc(zero))),bfalse)
| shw(suc(double(double(suc(zero))))) != aux(suc(suc(double(suc(zero)))),bfalse)
| shw(suc(double(double(suc(zero))))) = aux(double(double(suc(zero))),bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(shw(suc(double(double(suc(zero))))),aux(suc(suc(double(suc(zero)))),bfalse)) ),[1],$fot(aux(double(double(suc(zero))),bfalse))]]) ).
cnf(refute_0_197,plain,
( shw(suc(double(double(suc(zero))))) != aux(suc(suc(double(suc(zero)))),bfalse)
| shw(suc(double(double(suc(zero))))) = aux(double(double(suc(zero))),bfalse) ),
inference(resolve,[$cnf( $equal(aux(suc(suc(double(suc(zero)))),bfalse),aux(double(double(suc(zero))),bfalse)) )],[refute_0_195,refute_0_196]) ).
cnf(refute_0_198,plain,
( shw(suc(suc(suc(double(suc(zero)))))) != aux(suc(suc(double(suc(zero)))),bfalse)
| shw(suc(double(double(suc(zero))))) = aux(double(double(suc(zero))),bfalse) ),
inference(resolve,[$cnf( $equal(shw(suc(double(double(suc(zero))))),aux(suc(suc(double(suc(zero)))),bfalse)) )],[refute_0_191,refute_0_197]) ).
cnf(refute_0_199,plain,
shw(suc(double(double(suc(zero))))) = aux(double(double(suc(zero))),bfalse),
inference(resolve,[$cnf( $equal(shw(suc(suc(suc(double(suc(zero)))))),aux(suc(suc(double(suc(zero)))),bfalse)) )],[refute_0_181,refute_0_198]) ).
cnf(refute_0_200,plain,
( shw(suc(double(double(suc(zero))))) != aux(double(double(suc(zero))),bfalse)
| aux(double(double(suc(zero))),bfalse) = shw(suc(double(double(suc(zero))))) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(shw(suc(double(double(suc(zero))))))),bind(Y0,$fot(aux(double(double(suc(zero))),bfalse)))]]) ).
cnf(refute_0_201,plain,
aux(double(double(suc(zero))),bfalse) = shw(suc(double(double(suc(zero))))),
inference(resolve,[$cnf( $equal(shw(suc(double(double(suc(zero))))),aux(double(double(suc(zero))),bfalse)) )],[refute_0_199,refute_0_200]) ).
cnf(refute_0_202,plain,
( aux(double(double(suc(zero))),bfalse) != cons(i,shw(double(suc(zero))))
| aux(double(double(suc(zero))),bfalse) != shw(suc(double(double(suc(zero)))))
| shw(suc(double(double(suc(zero))))) = cons(i,shw(double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(aux(double(double(suc(zero))),bfalse),cons(i,shw(double(suc(zero))))) ),[0],$fot(shw(suc(double(double(suc(zero))))))]]) ).
cnf(refute_0_203,plain,
( aux(double(double(suc(zero))),bfalse) != cons(i,shw(double(suc(zero))))
| shw(suc(double(double(suc(zero))))) = cons(i,shw(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(aux(double(double(suc(zero))),bfalse),shw(suc(double(double(suc(zero)))))) )],[refute_0_201,refute_0_202]) ).
cnf(refute_0_204,plain,
shw(suc(double(double(suc(zero))))) = cons(i,shw(double(suc(zero)))),
inference(resolve,[$cnf( $equal(aux(double(double(suc(zero))),bfalse),cons(i,shw(double(suc(zero))))) )],[refute_0_123,refute_0_203]) ).
cnf(refute_0_205,plain,
( shw(suc(double(double(suc(zero))))) != cons(i,shw(double(suc(zero))))
| cons(i,shw(double(suc(zero)))) = shw(suc(double(double(suc(zero))))) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(shw(suc(double(double(suc(zero))))))),bind(Y0,$fot(cons(i,shw(double(suc(zero))))))]]) ).
cnf(refute_0_206,plain,
cons(i,shw(double(suc(zero)))) = shw(suc(double(double(suc(zero))))),
inference(resolve,[$cnf( $equal(shw(suc(double(double(suc(zero))))),cons(i,shw(double(suc(zero))))) )],[refute_0_204,refute_0_205]) ).
cnf(refute_0_207,plain,
( cons(i,shw(double(suc(zero)))) != shw(suc(double(double(suc(zero)))))
| x(suc(zero),double(suc(zero))) != rd(cons(i,shw(double(suc(zero)))))
| x(suc(zero),double(suc(zero))) = rd(shw(suc(double(double(suc(zero)))))) ),
introduced(tautology,[equality,[$cnf( $equal(x(suc(zero),double(suc(zero))),rd(cons(i,shw(double(suc(zero)))))) ),[1,0],$fot(shw(suc(double(double(suc(zero))))))]]) ).
cnf(refute_0_208,plain,
( x(suc(zero),double(suc(zero))) != rd(cons(i,shw(double(suc(zero)))))
| x(suc(zero),double(suc(zero))) = rd(shw(suc(double(double(suc(zero)))))) ),
inference(resolve,[$cnf( $equal(cons(i,shw(double(suc(zero)))),shw(suc(double(double(suc(zero)))))) )],[refute_0_206,refute_0_207]) ).
cnf(refute_0_209,plain,
x(suc(zero),double(suc(zero))) = rd(shw(suc(double(double(suc(zero)))))),
inference(resolve,[$cnf( $equal(x(suc(zero),double(suc(zero))),rd(cons(i,shw(double(suc(zero)))))) )],[refute_0_51,refute_0_208]) ).
cnf(refute_0_210,plain,
rd(cons(i,shw(double(suc(zero))))) = suc(double(rd(shw(double(suc(zero)))))),
inference(subst,[],[axiom_017:[bind(Xs,$fot(shw(double(suc(zero)))))]]) ).
cnf(refute_0_211,plain,
rd(cons(o,shw(half(suc(Y))))) = double(rd(shw(half(suc(Y))))),
inference(subst,[],[axiom_018:[bind(Xs,$fot(shw(half(suc(Y)))))]]) ).
cnf(refute_0_212,plain,
( aux(Y,btrue) != cons(o,shw(half(suc(Y))))
| cons(o,shw(half(suc(Y)))) = aux(Y,btrue) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(aux(Y,btrue))),bind(Y0,$fot(cons(o,shw(half(suc(Y))))))]]) ).
cnf(refute_0_213,plain,
cons(o,shw(half(suc(Y)))) = aux(Y,btrue),
inference(resolve,[$cnf( $equal(aux(Y,btrue),cons(o,shw(half(suc(Y))))) )],[axiom,refute_0_212]) ).
cnf(refute_0_214,plain,
( cons(o,shw(half(suc(Y)))) != aux(Y,btrue)
| rd(cons(o,shw(half(suc(Y))))) != double(rd(shw(half(suc(Y)))))
| rd(aux(Y,btrue)) = double(rd(shw(half(suc(Y))))) ),
introduced(tautology,[equality,[$cnf( $equal(rd(cons(o,shw(half(suc(Y))))),double(rd(shw(half(suc(Y)))))) ),[0,0],$fot(aux(Y,btrue))]]) ).
cnf(refute_0_215,plain,
( rd(cons(o,shw(half(suc(Y))))) != double(rd(shw(half(suc(Y)))))
| rd(aux(Y,btrue)) = double(rd(shw(half(suc(Y))))) ),
inference(resolve,[$cnf( $equal(cons(o,shw(half(suc(Y)))),aux(Y,btrue)) )],[refute_0_213,refute_0_214]) ).
cnf(refute_0_216,plain,
rd(aux(Y,btrue)) = double(rd(shw(half(suc(Y))))),
inference(resolve,[$cnf( $equal(rd(cons(o,shw(half(suc(Y))))),double(rd(shw(half(suc(Y)))))) )],[refute_0_211,refute_0_215]) ).
cnf(refute_0_217,plain,
rd(aux(suc(zero),btrue)) = double(rd(shw(half(suc(suc(zero)))))),
inference(subst,[],[refute_0_216:[bind(Y,$fot(suc(zero)))]]) ).
cnf(refute_0_218,plain,
( rd(aux(suc(zero),btrue)) != double(rd(shw(half(suc(suc(zero))))))
| suc(suc(zero)) != double(suc(zero))
| rd(aux(suc(zero),btrue)) = double(rd(shw(half(double(suc(zero)))))) ),
introduced(tautology,[equality,[$cnf( $equal(rd(aux(suc(zero),btrue)),double(rd(shw(half(suc(suc(zero))))))) ),[1,0,0,0,0],$fot(double(suc(zero)))]]) ).
cnf(refute_0_219,plain,
( rd(aux(suc(zero),btrue)) != double(rd(shw(half(suc(suc(zero))))))
| rd(aux(suc(zero),btrue)) = double(rd(shw(half(double(suc(zero)))))) ),
inference(resolve,[$cnf( $equal(suc(suc(zero)),double(suc(zero))) )],[refute_0_66,refute_0_218]) ).
cnf(refute_0_220,plain,
rd(aux(suc(zero),btrue)) = double(rd(shw(half(double(suc(zero)))))),
inference(resolve,[$cnf( $equal(rd(aux(suc(zero),btrue)),double(rd(shw(half(suc(suc(zero))))))) )],[refute_0_217,refute_0_219]) ).
cnf(refute_0_221,plain,
shw(suc(suc(zero))) = aux(suc(zero),evenNat(suc(suc(zero)))),
inference(subst,[],[axiom_010:[bind(Y,$fot(suc(zero)))]]) ).
cnf(refute_0_222,plain,
( evenNat(suc(suc(zero))) != btrue
| shw(suc(suc(zero))) != aux(suc(zero),evenNat(suc(suc(zero))))
| shw(suc(suc(zero))) = aux(suc(zero),btrue) ),
introduced(tautology,[equality,[$cnf( $equal(shw(suc(suc(zero))),aux(suc(zero),evenNat(suc(suc(zero))))) ),[1,1],$fot(btrue)]]) ).
cnf(refute_0_223,plain,
( shw(suc(suc(zero))) != aux(suc(zero),evenNat(suc(suc(zero))))
| shw(suc(suc(zero))) = aux(suc(zero),btrue) ),
inference(resolve,[$cnf( $equal(evenNat(suc(suc(zero))),btrue) )],[refute_0_134,refute_0_222]) ).
cnf(refute_0_224,plain,
shw(suc(suc(zero))) = aux(suc(zero),btrue),
inference(resolve,[$cnf( $equal(shw(suc(suc(zero))),aux(suc(zero),evenNat(suc(suc(zero))))) )],[refute_0_221,refute_0_223]) ).
cnf(refute_0_225,plain,
shw(suc(suc(zero))) = shw(suc(suc(zero))),
introduced(tautology,[refl,[$fot(shw(suc(suc(zero))))]]) ).
cnf(refute_0_226,plain,
( shw(suc(suc(zero))) != shw(suc(suc(zero)))
| suc(suc(zero)) != double(suc(zero))
| shw(suc(suc(zero))) = shw(double(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(shw(suc(suc(zero))),shw(suc(suc(zero)))) ),[1,0],$fot(double(suc(zero)))]]) ).
cnf(refute_0_227,plain,
( suc(suc(zero)) != double(suc(zero))
| shw(suc(suc(zero))) = shw(double(suc(zero))) ),
inference(resolve,[$cnf( $equal(shw(suc(suc(zero))),shw(suc(suc(zero)))) )],[refute_0_225,refute_0_226]) ).
cnf(refute_0_228,plain,
shw(suc(suc(zero))) = shw(double(suc(zero))),
inference(resolve,[$cnf( $equal(suc(suc(zero)),double(suc(zero))) )],[refute_0_66,refute_0_227]) ).
cnf(refute_0_229,plain,
( shw(suc(suc(zero))) != aux(suc(zero),btrue)
| shw(suc(suc(zero))) != shw(double(suc(zero)))
| shw(double(suc(zero))) = aux(suc(zero),btrue) ),
introduced(tautology,[equality,[$cnf( $equal(shw(suc(suc(zero))),aux(suc(zero),btrue)) ),[0],$fot(shw(double(suc(zero))))]]) ).
cnf(refute_0_230,plain,
( shw(suc(suc(zero))) != aux(suc(zero),btrue)
| shw(double(suc(zero))) = aux(suc(zero),btrue) ),
inference(resolve,[$cnf( $equal(shw(suc(suc(zero))),shw(double(suc(zero)))) )],[refute_0_228,refute_0_229]) ).
cnf(refute_0_231,plain,
shw(double(suc(zero))) = aux(suc(zero),btrue),
inference(resolve,[$cnf( $equal(shw(suc(suc(zero))),aux(suc(zero),btrue)) )],[refute_0_224,refute_0_230]) ).
cnf(refute_0_232,plain,
( shw(double(suc(zero))) != aux(suc(zero),btrue)
| aux(suc(zero),btrue) = shw(double(suc(zero))) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(shw(double(suc(zero))))),bind(Y0,$fot(aux(suc(zero),btrue)))]]) ).
cnf(refute_0_233,plain,
aux(suc(zero),btrue) = shw(double(suc(zero))),
inference(resolve,[$cnf( $equal(shw(double(suc(zero))),aux(suc(zero),btrue)) )],[refute_0_231,refute_0_232]) ).
cnf(refute_0_234,plain,
rd(aux(suc(zero),btrue)) = rd(aux(suc(zero),btrue)),
introduced(tautology,[refl,[$fot(rd(aux(suc(zero),btrue)))]]) ).
cnf(refute_0_235,plain,
( aux(suc(zero),btrue) != shw(double(suc(zero)))
| rd(aux(suc(zero),btrue)) != rd(aux(suc(zero),btrue))
| rd(aux(suc(zero),btrue)) = rd(shw(double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(rd(aux(suc(zero),btrue)),rd(aux(suc(zero),btrue))) ),[1,0],$fot(shw(double(suc(zero))))]]) ).
cnf(refute_0_236,plain,
( aux(suc(zero),btrue) != shw(double(suc(zero)))
| rd(aux(suc(zero),btrue)) = rd(shw(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(rd(aux(suc(zero),btrue)),rd(aux(suc(zero),btrue))) )],[refute_0_234,refute_0_235]) ).
cnf(refute_0_237,plain,
rd(aux(suc(zero),btrue)) = rd(shw(double(suc(zero)))),
inference(resolve,[$cnf( $equal(aux(suc(zero),btrue),shw(double(suc(zero)))) )],[refute_0_233,refute_0_236]) ).
cnf(refute_0_238,plain,
( rd(aux(suc(zero),btrue)) != double(rd(shw(half(double(suc(zero))))))
| rd(aux(suc(zero),btrue)) != rd(shw(double(suc(zero))))
| rd(shw(double(suc(zero)))) = double(rd(shw(half(double(suc(zero)))))) ),
introduced(tautology,[equality,[$cnf( $equal(rd(aux(suc(zero),btrue)),double(rd(shw(half(double(suc(zero))))))) ),[0],$fot(rd(shw(double(suc(zero)))))]]) ).
cnf(refute_0_239,plain,
( rd(aux(suc(zero),btrue)) != double(rd(shw(half(double(suc(zero))))))
| rd(shw(double(suc(zero)))) = double(rd(shw(half(double(suc(zero)))))) ),
inference(resolve,[$cnf( $equal(rd(aux(suc(zero),btrue)),rd(shw(double(suc(zero))))) )],[refute_0_237,refute_0_238]) ).
cnf(refute_0_240,plain,
rd(cons(i,nil)) = suc(double(rd(nil))),
inference(subst,[],[axiom_017:[bind(Xs,$fot(nil))]]) ).
cnf(refute_0_241,plain,
( rd(cons(i,nil)) != suc(double(rd(nil)))
| rd(nil) != zero
| rd(cons(i,nil)) = suc(double(zero)) ),
introduced(tautology,[equality,[$cnf( $equal(rd(cons(i,nil)),suc(double(rd(nil)))) ),[1,0,0],$fot(zero)]]) ).
cnf(refute_0_242,plain,
( rd(cons(i,nil)) != suc(double(rd(nil)))
| rd(cons(i,nil)) = suc(double(zero)) ),
inference(resolve,[$cnf( $equal(rd(nil),zero) )],[axiom_016,refute_0_241]) ).
cnf(refute_0_243,plain,
rd(cons(i,nil)) = suc(double(zero)),
inference(resolve,[$cnf( $equal(rd(cons(i,nil)),suc(double(rd(nil)))) )],[refute_0_240,refute_0_242]) ).
cnf(refute_0_244,plain,
addNat(zero,zero) = zero,
inference(subst,[],[axiom_013:[bind(Y,$fot(zero))]]) ).
cnf(refute_0_245,plain,
double(zero) = addNat(zero,zero),
inference(subst,[],[axiom_015:[bind(X,$fot(zero))]]) ).
cnf(refute_0_246,plain,
( double(zero) != addNat(zero,zero)
| addNat(zero,zero) = double(zero) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(double(zero))),bind(Y0,$fot(addNat(zero,zero)))]]) ).
cnf(refute_0_247,plain,
addNat(zero,zero) = double(zero),
inference(resolve,[$cnf( $equal(double(zero),addNat(zero,zero)) )],[refute_0_245,refute_0_246]) ).
cnf(refute_0_248,plain,
( addNat(zero,zero) != double(zero)
| addNat(zero,zero) != zero
| double(zero) = zero ),
introduced(tautology,[equality,[$cnf( $equal(addNat(zero,zero),zero) ),[0],$fot(double(zero))]]) ).
cnf(refute_0_249,plain,
( addNat(zero,zero) != zero
| double(zero) = zero ),
inference(resolve,[$cnf( $equal(addNat(zero,zero),double(zero)) )],[refute_0_247,refute_0_248]) ).
cnf(refute_0_250,plain,
double(zero) = zero,
inference(resolve,[$cnf( $equal(addNat(zero,zero),zero) )],[refute_0_244,refute_0_249]) ).
cnf(refute_0_251,plain,
suc(double(zero)) = suc(double(zero)),
introduced(tautology,[refl,[$fot(suc(double(zero)))]]) ).
cnf(refute_0_252,plain,
( double(zero) != zero
| suc(double(zero)) != suc(double(zero))
| suc(double(zero)) = suc(zero) ),
introduced(tautology,[equality,[$cnf( $equal(suc(double(zero)),suc(double(zero))) ),[1,0],$fot(zero)]]) ).
cnf(refute_0_253,plain,
( double(zero) != zero
| suc(double(zero)) = suc(zero) ),
inference(resolve,[$cnf( $equal(suc(double(zero)),suc(double(zero))) )],[refute_0_251,refute_0_252]) ).
cnf(refute_0_254,plain,
suc(double(zero)) = suc(zero),
inference(resolve,[$cnf( $equal(double(zero),zero) )],[refute_0_250,refute_0_253]) ).
cnf(refute_0_255,plain,
( rd(cons(i,nil)) != suc(double(zero))
| suc(double(zero)) != suc(zero)
| rd(cons(i,nil)) = suc(zero) ),
introduced(tautology,[equality,[$cnf( ~ $equal(rd(cons(i,nil)),suc(zero)) ),[0],$fot(suc(double(zero)))]]) ).
cnf(refute_0_256,plain,
( rd(cons(i,nil)) != suc(double(zero))
| rd(cons(i,nil)) = suc(zero) ),
inference(resolve,[$cnf( $equal(suc(double(zero)),suc(zero)) )],[refute_0_254,refute_0_255]) ).
cnf(refute_0_257,plain,
rd(cons(i,nil)) = suc(zero),
inference(resolve,[$cnf( $equal(rd(cons(i,nil)),suc(double(zero))) )],[refute_0_243,refute_0_256]) ).
cnf(refute_0_258,plain,
rd(cons(i,nil)) = rd(cons(i,nil)),
introduced(tautology,[refl,[$fot(rd(cons(i,nil)))]]) ).
cnf(refute_0_259,plain,
( cons(i,nil) != shw(suc(zero))
| rd(cons(i,nil)) != rd(cons(i,nil))
| rd(cons(i,nil)) = rd(shw(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(rd(cons(i,nil)),rd(cons(i,nil))) ),[1,0],$fot(shw(suc(zero)))]]) ).
cnf(refute_0_260,plain,
( cons(i,nil) != shw(suc(zero))
| rd(cons(i,nil)) = rd(shw(suc(zero))) ),
inference(resolve,[$cnf( $equal(rd(cons(i,nil)),rd(cons(i,nil))) )],[refute_0_258,refute_0_259]) ).
cnf(refute_0_261,plain,
rd(cons(i,nil)) = rd(shw(suc(zero))),
inference(resolve,[$cnf( $equal(cons(i,nil),shw(suc(zero))) )],[refute_0_35,refute_0_260]) ).
cnf(refute_0_262,plain,
( rd(cons(i,nil)) != rd(shw(suc(zero)))
| rd(cons(i,nil)) != suc(zero)
| rd(shw(suc(zero))) = suc(zero) ),
introduced(tautology,[equality,[$cnf( $equal(rd(cons(i,nil)),suc(zero)) ),[0],$fot(rd(shw(suc(zero))))]]) ).
cnf(refute_0_263,plain,
( rd(cons(i,nil)) != suc(zero)
| rd(shw(suc(zero))) = suc(zero) ),
inference(resolve,[$cnf( $equal(rd(cons(i,nil)),rd(shw(suc(zero)))) )],[refute_0_261,refute_0_262]) ).
cnf(refute_0_264,plain,
rd(shw(suc(zero))) = suc(zero),
inference(resolve,[$cnf( $equal(rd(cons(i,nil)),suc(zero)) )],[refute_0_257,refute_0_263]) ).
cnf(refute_0_265,plain,
half(suc(suc(double(rd(Xs))))) = suc(half(double(rd(Xs)))),
inference(subst,[],[axiom_006:[bind(N,$fot(double(rd(Xs))))]]) ).
cnf(refute_0_266,plain,
( rd(cons(i,Xs)) != suc(double(rd(Xs)))
| suc(double(rd(Xs))) = rd(cons(i,Xs)) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(rd(cons(i,Xs)))),bind(Y0,$fot(suc(double(rd(Xs)))))]]) ).
cnf(refute_0_267,plain,
suc(double(rd(Xs))) = rd(cons(i,Xs)),
inference(resolve,[$cnf( $equal(rd(cons(i,Xs)),suc(double(rd(Xs)))) )],[axiom_017,refute_0_266]) ).
cnf(refute_0_268,plain,
( half(suc(suc(double(rd(Xs))))) != suc(half(double(rd(Xs))))
| suc(double(rd(Xs))) != rd(cons(i,Xs))
| half(suc(rd(cons(i,Xs)))) = suc(half(double(rd(Xs)))) ),
introduced(tautology,[equality,[$cnf( $equal(half(suc(suc(double(rd(Xs))))),suc(half(double(rd(Xs))))) ),[0,0,0],$fot(rd(cons(i,Xs)))]]) ).
cnf(refute_0_269,plain,
( half(suc(suc(double(rd(Xs))))) != suc(half(double(rd(Xs))))
| half(suc(rd(cons(i,Xs)))) = suc(half(double(rd(Xs)))) ),
inference(resolve,[$cnf( $equal(suc(double(rd(Xs))),rd(cons(i,Xs))) )],[refute_0_267,refute_0_268]) ).
cnf(refute_0_270,plain,
half(suc(rd(cons(i,Xs)))) = suc(half(double(rd(Xs)))),
inference(resolve,[$cnf( $equal(half(suc(suc(double(rd(Xs))))),suc(half(double(rd(Xs))))) )],[refute_0_265,refute_0_269]) ).
cnf(refute_0_271,plain,
half(suc(rd(cons(i,nil)))) = suc(half(double(rd(nil)))),
inference(subst,[],[refute_0_270:[bind(Xs,$fot(nil))]]) ).
cnf(refute_0_272,plain,
( cons(i,nil) != shw(suc(zero))
| half(suc(rd(cons(i,nil)))) != suc(half(double(rd(nil))))
| half(suc(rd(shw(suc(zero))))) = suc(half(double(rd(nil)))) ),
introduced(tautology,[equality,[$cnf( $equal(half(suc(rd(cons(i,nil)))),suc(half(double(rd(nil))))) ),[0,0,0,0],$fot(shw(suc(zero)))]]) ).
cnf(refute_0_273,plain,
( half(suc(rd(cons(i,nil)))) != suc(half(double(rd(nil))))
| half(suc(rd(shw(suc(zero))))) = suc(half(double(rd(nil)))) ),
inference(resolve,[$cnf( $equal(cons(i,nil),shw(suc(zero))) )],[refute_0_35,refute_0_272]) ).
cnf(refute_0_274,plain,
half(suc(rd(shw(suc(zero))))) = suc(half(double(rd(nil)))),
inference(resolve,[$cnf( $equal(half(suc(rd(cons(i,nil)))),suc(half(double(rd(nil))))) )],[refute_0_271,refute_0_273]) ).
cnf(refute_0_275,plain,
suc(rd(shw(suc(zero)))) = suc(rd(shw(suc(zero)))),
introduced(tautology,[refl,[$fot(suc(rd(shw(suc(zero)))))]]) ).
cnf(refute_0_276,plain,
( rd(shw(suc(zero))) != suc(zero)
| suc(rd(shw(suc(zero)))) != suc(rd(shw(suc(zero))))
| suc(rd(shw(suc(zero)))) = suc(suc(zero)) ),
introduced(tautology,[equality,[$cnf( $equal(suc(rd(shw(suc(zero)))),suc(rd(shw(suc(zero))))) ),[1,0],$fot(suc(zero))]]) ).
cnf(refute_0_277,plain,
( rd(shw(suc(zero))) != suc(zero)
| suc(rd(shw(suc(zero)))) = suc(suc(zero)) ),
inference(resolve,[$cnf( $equal(suc(rd(shw(suc(zero)))),suc(rd(shw(suc(zero))))) )],[refute_0_275,refute_0_276]) ).
cnf(refute_0_278,plain,
suc(rd(shw(suc(zero)))) = suc(suc(zero)),
inference(resolve,[$cnf( $equal(rd(shw(suc(zero))),suc(zero)) )],[refute_0_264,refute_0_277]) ).
cnf(refute_0_279,plain,
( suc(rd(shw(suc(zero)))) != suc(suc(zero))
| suc(suc(zero)) != double(suc(zero))
| suc(rd(shw(suc(zero)))) = double(suc(zero)) ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(suc(rd(shw(suc(zero)))))),bind(Y0,$fot(suc(suc(zero)))),bind(Z0,$fot(double(suc(zero))))]]) ).
cnf(refute_0_280,plain,
( suc(suc(zero)) != double(suc(zero))
| suc(rd(shw(suc(zero)))) = double(suc(zero)) ),
inference(resolve,[$cnf( $equal(suc(rd(shw(suc(zero)))),suc(suc(zero))) )],[refute_0_278,refute_0_279]) ).
cnf(refute_0_281,plain,
suc(rd(shw(suc(zero)))) = double(suc(zero)),
inference(resolve,[$cnf( $equal(suc(suc(zero)),double(suc(zero))) )],[refute_0_66,refute_0_280]) ).
cnf(refute_0_282,plain,
half(suc(rd(shw(suc(zero))))) = half(suc(rd(shw(suc(zero))))),
introduced(tautology,[refl,[$fot(half(suc(rd(shw(suc(zero))))))]]) ).
cnf(refute_0_283,plain,
( half(suc(rd(shw(suc(zero))))) != half(suc(rd(shw(suc(zero)))))
| suc(rd(shw(suc(zero)))) != double(suc(zero))
| half(suc(rd(shw(suc(zero))))) = half(double(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(half(suc(rd(shw(suc(zero))))),half(suc(rd(shw(suc(zero)))))) ),[1,0],$fot(double(suc(zero)))]]) ).
cnf(refute_0_284,plain,
( suc(rd(shw(suc(zero)))) != double(suc(zero))
| half(suc(rd(shw(suc(zero))))) = half(double(suc(zero))) ),
inference(resolve,[$cnf( $equal(half(suc(rd(shw(suc(zero))))),half(suc(rd(shw(suc(zero)))))) )],[refute_0_282,refute_0_283]) ).
cnf(refute_0_285,plain,
half(suc(rd(shw(suc(zero))))) = half(double(suc(zero))),
inference(resolve,[$cnf( $equal(suc(rd(shw(suc(zero)))),double(suc(zero))) )],[refute_0_281,refute_0_284]) ).
cnf(refute_0_286,plain,
( half(suc(rd(shw(suc(zero))))) != half(double(suc(zero)))
| half(suc(rd(shw(suc(zero))))) != suc(half(double(rd(nil))))
| half(double(suc(zero))) = suc(half(double(rd(nil)))) ),
introduced(tautology,[equality,[$cnf( $equal(half(suc(rd(shw(suc(zero))))),suc(half(double(rd(nil))))) ),[0],$fot(half(double(suc(zero))))]]) ).
cnf(refute_0_287,plain,
( half(suc(rd(shw(suc(zero))))) != suc(half(double(rd(nil))))
| half(double(suc(zero))) = suc(half(double(rd(nil)))) ),
inference(resolve,[$cnf( $equal(half(suc(rd(shw(suc(zero))))),half(double(suc(zero)))) )],[refute_0_285,refute_0_286]) ).
cnf(refute_0_288,plain,
double(rd(nil)) = double(rd(nil)),
introduced(tautology,[refl,[$fot(double(rd(nil)))]]) ).
cnf(refute_0_289,plain,
( double(rd(nil)) != double(rd(nil))
| rd(nil) != zero
| double(rd(nil)) = double(zero) ),
introduced(tautology,[equality,[$cnf( $equal(double(rd(nil)),double(rd(nil))) ),[1,0],$fot(zero)]]) ).
cnf(refute_0_290,plain,
( rd(nil) != zero
| double(rd(nil)) = double(zero) ),
inference(resolve,[$cnf( $equal(double(rd(nil)),double(rd(nil))) )],[refute_0_288,refute_0_289]) ).
cnf(refute_0_291,plain,
double(rd(nil)) = double(zero),
inference(resolve,[$cnf( $equal(rd(nil),zero) )],[axiom_016,refute_0_290]) ).
cnf(refute_0_292,plain,
( double(rd(nil)) != double(zero)
| double(zero) != zero
| double(rd(nil)) = zero ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(double(rd(nil)))),bind(Y0,$fot(double(zero))),bind(Z0,$fot(zero))]]) ).
cnf(refute_0_293,plain,
( double(zero) != zero
| double(rd(nil)) = zero ),
inference(resolve,[$cnf( $equal(double(rd(nil)),double(zero)) )],[refute_0_291,refute_0_292]) ).
cnf(refute_0_294,plain,
double(rd(nil)) = zero,
inference(resolve,[$cnf( $equal(double(zero),zero) )],[refute_0_250,refute_0_293]) ).
cnf(refute_0_295,plain,
half(double(rd(nil))) = half(double(rd(nil))),
introduced(tautology,[refl,[$fot(half(double(rd(nil))))]]) ).
cnf(refute_0_296,plain,
( double(rd(nil)) != zero
| half(double(rd(nil))) != half(double(rd(nil)))
| half(double(rd(nil))) = half(zero) ),
introduced(tautology,[equality,[$cnf( $equal(half(double(rd(nil))),half(double(rd(nil)))) ),[1,0],$fot(zero)]]) ).
cnf(refute_0_297,plain,
( double(rd(nil)) != zero
| half(double(rd(nil))) = half(zero) ),
inference(resolve,[$cnf( $equal(half(double(rd(nil))),half(double(rd(nil)))) )],[refute_0_295,refute_0_296]) ).
cnf(refute_0_298,plain,
half(double(rd(nil))) = half(zero),
inference(resolve,[$cnf( $equal(double(rd(nil)),zero) )],[refute_0_294,refute_0_297]) ).
cnf(refute_0_299,plain,
( half(double(rd(nil))) != half(zero)
| half(zero) != zero
| half(double(rd(nil))) = zero ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(half(double(rd(nil))))),bind(Y0,$fot(half(zero))),bind(Z0,$fot(zero))]]) ).
cnf(refute_0_300,plain,
( half(zero) != zero
| half(double(rd(nil))) = zero ),
inference(resolve,[$cnf( $equal(half(double(rd(nil))),half(zero)) )],[refute_0_298,refute_0_299]) ).
cnf(refute_0_301,plain,
half(double(rd(nil))) = zero,
inference(resolve,[$cnf( $equal(half(zero),zero) )],[axiom_004,refute_0_300]) ).
cnf(refute_0_302,plain,
suc(half(double(rd(nil)))) = suc(half(double(rd(nil)))),
introduced(tautology,[refl,[$fot(suc(half(double(rd(nil)))))]]) ).
cnf(refute_0_303,plain,
( half(double(rd(nil))) != zero
| suc(half(double(rd(nil)))) != suc(half(double(rd(nil))))
| suc(half(double(rd(nil)))) = suc(zero) ),
introduced(tautology,[equality,[$cnf( $equal(suc(half(double(rd(nil)))),suc(half(double(rd(nil))))) ),[1,0],$fot(zero)]]) ).
cnf(refute_0_304,plain,
( half(double(rd(nil))) != zero
| suc(half(double(rd(nil)))) = suc(zero) ),
inference(resolve,[$cnf( $equal(suc(half(double(rd(nil)))),suc(half(double(rd(nil))))) )],[refute_0_302,refute_0_303]) ).
cnf(refute_0_305,plain,
suc(half(double(rd(nil)))) = suc(zero),
inference(resolve,[$cnf( $equal(half(double(rd(nil))),zero) )],[refute_0_301,refute_0_304]) ).
cnf(refute_0_306,plain,
( half(double(suc(zero))) != suc(half(double(rd(nil))))
| suc(half(double(rd(nil)))) != suc(zero)
| half(double(suc(zero))) = suc(zero) ),
introduced(tautology,[equality,[$cnf( ~ $equal(half(double(suc(zero))),suc(zero)) ),[0],$fot(suc(half(double(rd(nil)))))]]) ).
cnf(refute_0_307,plain,
( half(double(suc(zero))) != suc(half(double(rd(nil))))
| half(double(suc(zero))) = suc(zero) ),
inference(resolve,[$cnf( $equal(suc(half(double(rd(nil)))),suc(zero)) )],[refute_0_305,refute_0_306]) ).
cnf(refute_0_308,plain,
( half(suc(rd(shw(suc(zero))))) != suc(half(double(rd(nil))))
| half(double(suc(zero))) = suc(zero) ),
inference(resolve,[$cnf( $equal(half(double(suc(zero))),suc(half(double(rd(nil))))) )],[refute_0_287,refute_0_307]) ).
cnf(refute_0_309,plain,
half(double(suc(zero))) = suc(zero),
inference(resolve,[$cnf( $equal(half(suc(rd(shw(suc(zero))))),suc(half(double(rd(nil))))) )],[refute_0_274,refute_0_308]) ).
cnf(refute_0_310,plain,
shw(half(double(suc(zero)))) = shw(half(double(suc(zero)))),
introduced(tautology,[refl,[$fot(shw(half(double(suc(zero)))))]]) ).
cnf(refute_0_311,plain,
( half(double(suc(zero))) != suc(zero)
| shw(half(double(suc(zero)))) != shw(half(double(suc(zero))))
| shw(half(double(suc(zero)))) = shw(suc(zero)) ),
introduced(tautology,[equality,[$cnf( $equal(shw(half(double(suc(zero)))),shw(half(double(suc(zero))))) ),[1,0],$fot(suc(zero))]]) ).
cnf(refute_0_312,plain,
( half(double(suc(zero))) != suc(zero)
| shw(half(double(suc(zero)))) = shw(suc(zero)) ),
inference(resolve,[$cnf( $equal(shw(half(double(suc(zero)))),shw(half(double(suc(zero))))) )],[refute_0_310,refute_0_311]) ).
cnf(refute_0_313,plain,
shw(half(double(suc(zero)))) = shw(suc(zero)),
inference(resolve,[$cnf( $equal(half(double(suc(zero))),suc(zero)) )],[refute_0_309,refute_0_312]) ).
cnf(refute_0_314,plain,
rd(shw(half(double(suc(zero))))) = rd(shw(half(double(suc(zero))))),
introduced(tautology,[refl,[$fot(rd(shw(half(double(suc(zero))))))]]) ).
cnf(refute_0_315,plain,
( rd(shw(half(double(suc(zero))))) != rd(shw(half(double(suc(zero)))))
| shw(half(double(suc(zero)))) != shw(suc(zero))
| rd(shw(half(double(suc(zero))))) = rd(shw(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(rd(shw(half(double(suc(zero))))),rd(shw(half(double(suc(zero)))))) ),[1,0],$fot(shw(suc(zero)))]]) ).
cnf(refute_0_316,plain,
( shw(half(double(suc(zero)))) != shw(suc(zero))
| rd(shw(half(double(suc(zero))))) = rd(shw(suc(zero))) ),
inference(resolve,[$cnf( $equal(rd(shw(half(double(suc(zero))))),rd(shw(half(double(suc(zero)))))) )],[refute_0_314,refute_0_315]) ).
cnf(refute_0_317,plain,
rd(shw(half(double(suc(zero))))) = rd(shw(suc(zero))),
inference(resolve,[$cnf( $equal(shw(half(double(suc(zero)))),shw(suc(zero))) )],[refute_0_313,refute_0_316]) ).
cnf(refute_0_318,plain,
( rd(shw(half(double(suc(zero))))) != rd(shw(suc(zero)))
| rd(shw(suc(zero))) != suc(zero)
| rd(shw(half(double(suc(zero))))) = suc(zero) ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(rd(shw(half(double(suc(zero))))))),bind(Y0,$fot(rd(shw(suc(zero))))),bind(Z0,$fot(suc(zero)))]]) ).
cnf(refute_0_319,plain,
( rd(shw(suc(zero))) != suc(zero)
| rd(shw(half(double(suc(zero))))) = suc(zero) ),
inference(resolve,[$cnf( $equal(rd(shw(half(double(suc(zero))))),rd(shw(suc(zero)))) )],[refute_0_317,refute_0_318]) ).
cnf(refute_0_320,plain,
rd(shw(half(double(suc(zero))))) = suc(zero),
inference(resolve,[$cnf( $equal(rd(shw(suc(zero))),suc(zero)) )],[refute_0_264,refute_0_319]) ).
cnf(refute_0_321,plain,
double(rd(shw(half(double(suc(zero)))))) = double(rd(shw(half(double(suc(zero)))))),
introduced(tautology,[refl,[$fot(double(rd(shw(half(double(suc(zero)))))))]]) ).
cnf(refute_0_322,plain,
( double(rd(shw(half(double(suc(zero)))))) != double(rd(shw(half(double(suc(zero))))))
| rd(shw(half(double(suc(zero))))) != suc(zero)
| double(rd(shw(half(double(suc(zero)))))) = double(suc(zero)) ),
introduced(tautology,[equality,[$cnf( $equal(double(rd(shw(half(double(suc(zero)))))),double(rd(shw(half(double(suc(zero))))))) ),[1,0],$fot(suc(zero))]]) ).
cnf(refute_0_323,plain,
( rd(shw(half(double(suc(zero))))) != suc(zero)
| double(rd(shw(half(double(suc(zero)))))) = double(suc(zero)) ),
inference(resolve,[$cnf( $equal(double(rd(shw(half(double(suc(zero)))))),double(rd(shw(half(double(suc(zero))))))) )],[refute_0_321,refute_0_322]) ).
cnf(refute_0_324,plain,
double(rd(shw(half(double(suc(zero)))))) = double(suc(zero)),
inference(resolve,[$cnf( $equal(rd(shw(half(double(suc(zero))))),suc(zero)) )],[refute_0_320,refute_0_323]) ).
cnf(refute_0_325,plain,
( double(rd(shw(half(double(suc(zero)))))) != double(suc(zero))
| rd(shw(double(suc(zero)))) != double(rd(shw(half(double(suc(zero))))))
| rd(shw(double(suc(zero)))) = double(suc(zero)) ),
introduced(tautology,[equality,[$cnf( $equal(rd(shw(double(suc(zero)))),double(rd(shw(half(double(suc(zero))))))) ),[1],$fot(double(suc(zero)))]]) ).
cnf(refute_0_326,plain,
( rd(shw(double(suc(zero)))) != double(rd(shw(half(double(suc(zero))))))
| rd(shw(double(suc(zero)))) = double(suc(zero)) ),
inference(resolve,[$cnf( $equal(double(rd(shw(half(double(suc(zero)))))),double(suc(zero))) )],[refute_0_324,refute_0_325]) ).
cnf(refute_0_327,plain,
( rd(aux(suc(zero),btrue)) != double(rd(shw(half(double(suc(zero))))))
| rd(shw(double(suc(zero)))) = double(suc(zero)) ),
inference(resolve,[$cnf( $equal(rd(shw(double(suc(zero)))),double(rd(shw(half(double(suc(zero))))))) )],[refute_0_239,refute_0_326]) ).
cnf(refute_0_328,plain,
rd(shw(double(suc(zero)))) = double(suc(zero)),
inference(resolve,[$cnf( $equal(rd(aux(suc(zero),btrue)),double(rd(shw(half(double(suc(zero))))))) )],[refute_0_220,refute_0_327]) ).
cnf(refute_0_329,plain,
( rd(cons(i,shw(double(suc(zero))))) != suc(double(rd(shw(double(suc(zero))))))
| rd(shw(double(suc(zero)))) != double(suc(zero))
| rd(cons(i,shw(double(suc(zero))))) = suc(double(double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(rd(cons(i,shw(double(suc(zero))))),suc(double(rd(shw(double(suc(zero))))))) ),[1,0,0],$fot(double(suc(zero)))]]) ).
cnf(refute_0_330,plain,
( rd(cons(i,shw(double(suc(zero))))) != suc(double(rd(shw(double(suc(zero))))))
| rd(cons(i,shw(double(suc(zero))))) = suc(double(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(rd(shw(double(suc(zero)))),double(suc(zero))) )],[refute_0_328,refute_0_329]) ).
cnf(refute_0_331,plain,
rd(cons(i,shw(double(suc(zero))))) = suc(double(double(suc(zero)))),
inference(resolve,[$cnf( $equal(rd(cons(i,shw(double(suc(zero))))),suc(double(rd(shw(double(suc(zero))))))) )],[refute_0_210,refute_0_330]) ).
cnf(refute_0_332,plain,
rd(cons(i,shw(double(suc(zero))))) = rd(cons(i,shw(double(suc(zero))))),
introduced(tautology,[refl,[$fot(rd(cons(i,shw(double(suc(zero))))))]]) ).
cnf(refute_0_333,plain,
( cons(i,shw(double(suc(zero)))) != shw(suc(double(double(suc(zero)))))
| rd(cons(i,shw(double(suc(zero))))) != rd(cons(i,shw(double(suc(zero)))))
| rd(cons(i,shw(double(suc(zero))))) = rd(shw(suc(double(double(suc(zero)))))) ),
introduced(tautology,[equality,[$cnf( $equal(rd(cons(i,shw(double(suc(zero))))),rd(cons(i,shw(double(suc(zero)))))) ),[1,0],$fot(shw(suc(double(double(suc(zero))))))]]) ).
cnf(refute_0_334,plain,
( cons(i,shw(double(suc(zero)))) != shw(suc(double(double(suc(zero)))))
| rd(cons(i,shw(double(suc(zero))))) = rd(shw(suc(double(double(suc(zero)))))) ),
inference(resolve,[$cnf( $equal(rd(cons(i,shw(double(suc(zero))))),rd(cons(i,shw(double(suc(zero)))))) )],[refute_0_332,refute_0_333]) ).
cnf(refute_0_335,plain,
rd(cons(i,shw(double(suc(zero))))) = rd(shw(suc(double(double(suc(zero)))))),
inference(resolve,[$cnf( $equal(cons(i,shw(double(suc(zero)))),shw(suc(double(double(suc(zero)))))) )],[refute_0_206,refute_0_334]) ).
cnf(refute_0_336,plain,
( rd(cons(i,shw(double(suc(zero))))) != rd(shw(suc(double(double(suc(zero))))))
| rd(cons(i,shw(double(suc(zero))))) != suc(double(double(suc(zero))))
| rd(shw(suc(double(double(suc(zero)))))) = suc(double(double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(rd(cons(i,shw(double(suc(zero))))),suc(double(double(suc(zero))))) ),[0],$fot(rd(shw(suc(double(double(suc(zero)))))))]]) ).
cnf(refute_0_337,plain,
( rd(cons(i,shw(double(suc(zero))))) != suc(double(double(suc(zero))))
| rd(shw(suc(double(double(suc(zero)))))) = suc(double(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(rd(cons(i,shw(double(suc(zero))))),rd(shw(suc(double(double(suc(zero))))))) )],[refute_0_335,refute_0_336]) ).
cnf(refute_0_338,plain,
rd(shw(suc(double(double(suc(zero)))))) = suc(double(double(suc(zero)))),
inference(resolve,[$cnf( $equal(rd(cons(i,shw(double(suc(zero))))),suc(double(double(suc(zero))))) )],[refute_0_331,refute_0_337]) ).
cnf(refute_0_339,plain,
( rd(shw(suc(double(double(suc(zero)))))) != suc(double(double(suc(zero))))
| x(suc(zero),double(suc(zero))) != rd(shw(suc(double(double(suc(zero))))))
| x(suc(zero),double(suc(zero))) = suc(double(double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(x(suc(zero),double(suc(zero))),rd(shw(suc(double(double(suc(zero))))))) ),[1],$fot(suc(double(double(suc(zero)))))]]) ).
cnf(refute_0_340,plain,
( x(suc(zero),double(suc(zero))) != rd(shw(suc(double(double(suc(zero))))))
| x(suc(zero),double(suc(zero))) = suc(double(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(rd(shw(suc(double(double(suc(zero)))))),suc(double(double(suc(zero))))) )],[refute_0_338,refute_0_339]) ).
cnf(refute_0_341,plain,
x(suc(zero),double(suc(zero))) = suc(double(double(suc(zero)))),
inference(resolve,[$cnf( $equal(x(suc(zero),double(suc(zero))),rd(shw(suc(double(double(suc(zero))))))) )],[refute_0_209,refute_0_340]) ).
cnf(refute_0_342,plain,
( sat_comm(suc(zero),double(suc(zero))) != eq(x(suc(zero),double(suc(zero))),x(double(suc(zero)),suc(zero)))
| x(suc(zero),double(suc(zero))) != suc(double(double(suc(zero))))
| sat_comm(suc(zero),double(suc(zero))) = eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_comm(suc(zero),double(suc(zero))),eq(x(suc(zero),double(suc(zero))),x(double(suc(zero)),suc(zero)))) ),[1,0],$fot(suc(double(double(suc(zero)))))]]) ).
cnf(refute_0_343,plain,
( sat_comm(suc(zero),double(suc(zero))) != eq(x(suc(zero),double(suc(zero))),x(double(suc(zero)),suc(zero)))
| sat_comm(suc(zero),double(suc(zero))) = eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))) ),
inference(resolve,[$cnf( $equal(x(suc(zero),double(suc(zero))),suc(double(double(suc(zero))))) )],[refute_0_341,refute_0_342]) ).
cnf(refute_0_344,plain,
sat_comm(suc(zero),double(suc(zero))) = eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))),
inference(resolve,[$cnf( $equal(sat_comm(suc(zero),double(suc(zero))),eq(x(suc(zero),double(suc(zero))),x(double(suc(zero)),suc(zero)))) )],[refute_0_1,refute_0_343]) ).
cnf(refute_0_345,plain,
eq(zero,suc(zero)) = bfalse,
inference(subst,[],[axiom_026:[bind(X,$fot(zero))]]) ).
cnf(refute_0_346,plain,
eq(zero,addNat(zero,suc(zero))) = eq(zero,addNat(zero,suc(zero))),
introduced(tautology,[refl,[$fot(eq(zero,addNat(zero,suc(zero))))]]) ).
cnf(refute_0_347,plain,
( addNat(zero,suc(zero)) != suc(zero)
| eq(zero,addNat(zero,suc(zero))) != eq(zero,addNat(zero,suc(zero)))
| eq(zero,addNat(zero,suc(zero))) = eq(zero,suc(zero)) ),
introduced(tautology,[equality,[$cnf( $equal(eq(zero,addNat(zero,suc(zero))),eq(zero,addNat(zero,suc(zero)))) ),[1,1],$fot(suc(zero))]]) ).
cnf(refute_0_348,plain,
( addNat(zero,suc(zero)) != suc(zero)
| eq(zero,addNat(zero,suc(zero))) = eq(zero,suc(zero)) ),
inference(resolve,[$cnf( $equal(eq(zero,addNat(zero,suc(zero))),eq(zero,addNat(zero,suc(zero)))) )],[refute_0_346,refute_0_347]) ).
cnf(refute_0_349,plain,
eq(zero,addNat(zero,suc(zero))) = eq(zero,suc(zero)),
inference(resolve,[$cnf( $equal(addNat(zero,suc(zero)),suc(zero)) )],[refute_0_61,refute_0_348]) ).
cnf(refute_0_350,plain,
( eq(zero,addNat(zero,suc(zero))) != eq(zero,suc(zero))
| eq(zero,suc(zero)) != bfalse
| eq(zero,addNat(zero,suc(zero))) = bfalse ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(eq(zero,addNat(zero,suc(zero))))),bind(Y0,$fot(eq(zero,suc(zero)))),bind(Z0,$fot(bfalse))]]) ).
cnf(refute_0_351,plain,
( eq(zero,suc(zero)) != bfalse
| eq(zero,addNat(zero,suc(zero))) = bfalse ),
inference(resolve,[$cnf( $equal(eq(zero,addNat(zero,suc(zero))),eq(zero,suc(zero))) )],[refute_0_349,refute_0_350]) ).
cnf(refute_0_352,plain,
eq(zero,addNat(zero,suc(zero))) = bfalse,
inference(resolve,[$cnf( $equal(eq(zero,suc(zero)),bfalse) )],[refute_0_345,refute_0_351]) ).
cnf(refute_0_353,plain,
eq(suc(X_21),suc(addNat(X_19,suc(X_19)))) = eq(X_21,addNat(X_19,suc(X_19))),
inference(subst,[],[axiom_025:[bind(X,$fot(X_21)),bind(Y,$fot(addNat(X_19,suc(X_19))))]]) ).
cnf(refute_0_354,plain,
( double(suc(X_19)) != suc(addNat(X_19,suc(X_19)))
| suc(addNat(X_19,suc(X_19))) = double(suc(X_19)) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(double(suc(X_19)))),bind(Y0,$fot(suc(addNat(X_19,suc(X_19)))))]]) ).
cnf(refute_0_355,plain,
suc(addNat(X_19,suc(X_19))) = double(suc(X_19)),
inference(resolve,[$cnf( $equal(double(suc(X_19)),suc(addNat(X_19,suc(X_19)))) )],[refute_0_58,refute_0_354]) ).
cnf(refute_0_356,plain,
( eq(suc(X_21),suc(addNat(X_19,suc(X_19)))) != eq(X_21,addNat(X_19,suc(X_19)))
| suc(addNat(X_19,suc(X_19))) != double(suc(X_19))
| eq(suc(X_21),double(suc(X_19))) = eq(X_21,addNat(X_19,suc(X_19))) ),
introduced(tautology,[equality,[$cnf( $equal(eq(suc(X_21),suc(addNat(X_19,suc(X_19)))),eq(X_21,addNat(X_19,suc(X_19)))) ),[0,1],$fot(double(suc(X_19)))]]) ).
cnf(refute_0_357,plain,
( eq(suc(X_21),suc(addNat(X_19,suc(X_19)))) != eq(X_21,addNat(X_19,suc(X_19)))
| eq(suc(X_21),double(suc(X_19))) = eq(X_21,addNat(X_19,suc(X_19))) ),
inference(resolve,[$cnf( $equal(suc(addNat(X_19,suc(X_19))),double(suc(X_19))) )],[refute_0_355,refute_0_356]) ).
cnf(refute_0_358,plain,
eq(suc(X_21),double(suc(X_19))) = eq(X_21,addNat(X_19,suc(X_19))),
inference(resolve,[$cnf( $equal(eq(suc(X_21),suc(addNat(X_19,suc(X_19)))),eq(X_21,addNat(X_19,suc(X_19)))) )],[refute_0_353,refute_0_357]) ).
cnf(refute_0_359,plain,
eq(suc(zero),double(suc(zero))) = eq(zero,addNat(zero,suc(zero))),
inference(subst,[],[refute_0_358:[bind(X_19,$fot(zero)),bind(X_21,$fot(zero))]]) ).
cnf(refute_0_360,plain,
eq(suc(suc(zero)),suc(Y)) = eq(suc(zero),Y),
inference(subst,[],[axiom_025:[bind(X,$fot(suc(zero)))]]) ).
cnf(refute_0_361,plain,
( eq(suc(suc(zero)),suc(Y)) != eq(suc(zero),Y)
| suc(suc(zero)) != double(suc(zero))
| eq(double(suc(zero)),suc(Y)) = eq(suc(zero),Y) ),
introduced(tautology,[equality,[$cnf( $equal(eq(suc(suc(zero)),suc(Y)),eq(suc(zero),Y)) ),[0,0],$fot(double(suc(zero)))]]) ).
cnf(refute_0_362,plain,
( eq(suc(suc(zero)),suc(Y)) != eq(suc(zero),Y)
| eq(double(suc(zero)),suc(Y)) = eq(suc(zero),Y) ),
inference(resolve,[$cnf( $equal(suc(suc(zero)),double(suc(zero))) )],[refute_0_66,refute_0_361]) ).
cnf(refute_0_363,plain,
eq(double(suc(zero)),suc(Y)) = eq(suc(zero),Y),
inference(resolve,[$cnf( $equal(eq(suc(suc(zero)),suc(Y)),eq(suc(zero),Y)) )],[refute_0_360,refute_0_362]) ).
cnf(refute_0_364,plain,
eq(double(suc(zero)),suc(double(suc(zero)))) = eq(suc(zero),double(suc(zero))),
inference(subst,[],[refute_0_363:[bind(Y,$fot(double(suc(zero))))]]) ).
cnf(refute_0_365,plain,
( eq(double(suc(zero)),suc(double(suc(zero)))) != eq(suc(zero),double(suc(zero)))
| eq(suc(zero),double(suc(zero))) != eq(zero,addNat(zero,suc(zero)))
| eq(double(suc(zero)),suc(double(suc(zero)))) = eq(zero,addNat(zero,suc(zero))) ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(eq(double(suc(zero)),suc(double(suc(zero)))))),bind(Y0,$fot(eq(suc(zero),double(suc(zero))))),bind(Z0,$fot(eq(zero,addNat(zero,suc(zero)))))]]) ).
cnf(refute_0_366,plain,
( eq(suc(zero),double(suc(zero))) != eq(zero,addNat(zero,suc(zero)))
| eq(double(suc(zero)),suc(double(suc(zero)))) = eq(zero,addNat(zero,suc(zero))) ),
inference(resolve,[$cnf( $equal(eq(double(suc(zero)),suc(double(suc(zero)))),eq(suc(zero),double(suc(zero)))) )],[refute_0_364,refute_0_365]) ).
cnf(refute_0_367,plain,
eq(double(suc(zero)),suc(double(suc(zero)))) = eq(zero,addNat(zero,suc(zero))),
inference(resolve,[$cnf( $equal(eq(suc(zero),double(suc(zero))),eq(zero,addNat(zero,suc(zero)))) )],[refute_0_359,refute_0_366]) ).
cnf(refute_0_368,plain,
eq(suc(X),suc(suc(double(suc(zero))))) = eq(X,suc(double(suc(zero)))),
inference(subst,[],[axiom_025:[bind(Y,$fot(suc(double(suc(zero)))))]]) ).
cnf(refute_0_369,plain,
( eq(suc(X),suc(suc(double(suc(zero))))) != eq(X,suc(double(suc(zero))))
| suc(suc(double(suc(zero)))) != double(double(suc(zero)))
| eq(suc(X),double(double(suc(zero)))) = eq(X,suc(double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(eq(suc(X),suc(suc(double(suc(zero))))),eq(X,suc(double(suc(zero))))) ),[0,1],$fot(double(double(suc(zero))))]]) ).
cnf(refute_0_370,plain,
( eq(suc(X),suc(suc(double(suc(zero))))) != eq(X,suc(double(suc(zero))))
| eq(suc(X),double(double(suc(zero)))) = eq(X,suc(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(suc(suc(double(suc(zero)))),double(double(suc(zero)))) )],[refute_0_96,refute_0_369]) ).
cnf(refute_0_371,plain,
eq(suc(X),double(double(suc(zero)))) = eq(X,suc(double(suc(zero)))),
inference(resolve,[$cnf( $equal(eq(suc(X),suc(suc(double(suc(zero))))),eq(X,suc(double(suc(zero))))) )],[refute_0_368,refute_0_370]) ).
cnf(refute_0_372,plain,
eq(suc(double(suc(zero))),double(double(suc(zero)))) = eq(double(suc(zero)),suc(double(suc(zero)))),
inference(subst,[],[refute_0_371:[bind(X,$fot(double(suc(zero))))]]) ).
cnf(refute_0_373,plain,
( eq(double(suc(zero)),suc(double(suc(zero)))) != eq(zero,addNat(zero,suc(zero)))
| eq(suc(double(suc(zero))),double(double(suc(zero)))) != eq(double(suc(zero)),suc(double(suc(zero))))
| eq(suc(double(suc(zero))),double(double(suc(zero)))) = eq(zero,addNat(zero,suc(zero))) ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(eq(suc(double(suc(zero))),double(double(suc(zero)))))),bind(Y0,$fot(eq(double(suc(zero)),suc(double(suc(zero)))))),bind(Z0,$fot(eq(zero,addNat(zero,suc(zero)))))]]) ).
cnf(refute_0_374,plain,
( eq(double(suc(zero)),suc(double(suc(zero)))) != eq(zero,addNat(zero,suc(zero)))
| eq(suc(double(suc(zero))),double(double(suc(zero)))) = eq(zero,addNat(zero,suc(zero))) ),
inference(resolve,[$cnf( $equal(eq(suc(double(suc(zero))),double(double(suc(zero)))),eq(double(suc(zero)),suc(double(suc(zero))))) )],[refute_0_372,refute_0_373]) ).
cnf(refute_0_375,plain,
eq(suc(double(suc(zero))),double(double(suc(zero)))) = eq(zero,addNat(zero,suc(zero))),
inference(resolve,[$cnf( $equal(eq(double(suc(zero)),suc(double(suc(zero)))),eq(zero,addNat(zero,suc(zero)))) )],[refute_0_367,refute_0_374]) ).
cnf(refute_0_376,plain,
eq(suc(suc(double(suc(zero)))),suc(Y)) = eq(suc(double(suc(zero))),Y),
inference(subst,[],[axiom_025:[bind(X,$fot(suc(double(suc(zero)))))]]) ).
cnf(refute_0_377,plain,
( eq(suc(suc(double(suc(zero)))),suc(Y)) != eq(suc(double(suc(zero))),Y)
| suc(suc(double(suc(zero)))) != double(double(suc(zero)))
| eq(double(double(suc(zero))),suc(Y)) = eq(suc(double(suc(zero))),Y) ),
introduced(tautology,[equality,[$cnf( $equal(eq(suc(suc(double(suc(zero)))),suc(Y)),eq(suc(double(suc(zero))),Y)) ),[0,0],$fot(double(double(suc(zero))))]]) ).
cnf(refute_0_378,plain,
( eq(suc(suc(double(suc(zero)))),suc(Y)) != eq(suc(double(suc(zero))),Y)
| eq(double(double(suc(zero))),suc(Y)) = eq(suc(double(suc(zero))),Y) ),
inference(resolve,[$cnf( $equal(suc(suc(double(suc(zero)))),double(double(suc(zero)))) )],[refute_0_96,refute_0_377]) ).
cnf(refute_0_379,plain,
eq(double(double(suc(zero))),suc(Y)) = eq(suc(double(suc(zero))),Y),
inference(resolve,[$cnf( $equal(eq(suc(suc(double(suc(zero)))),suc(Y)),eq(suc(double(suc(zero))),Y)) )],[refute_0_376,refute_0_378]) ).
cnf(refute_0_380,plain,
eq(double(double(suc(zero))),suc(double(double(suc(zero))))) = eq(suc(double(suc(zero))),double(double(suc(zero)))),
inference(subst,[],[refute_0_379:[bind(Y,$fot(double(double(suc(zero)))))]]) ).
cnf(refute_0_381,plain,
( eq(double(double(suc(zero))),suc(double(double(suc(zero))))) != eq(suc(double(suc(zero))),double(double(suc(zero))))
| eq(suc(double(suc(zero))),double(double(suc(zero)))) != eq(zero,addNat(zero,suc(zero)))
| eq(double(double(suc(zero))),suc(double(double(suc(zero))))) = eq(zero,addNat(zero,suc(zero))) ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(eq(double(double(suc(zero))),suc(double(double(suc(zero))))))),bind(Y0,$fot(eq(suc(double(suc(zero))),double(double(suc(zero)))))),bind(Z0,$fot(eq(zero,addNat(zero,suc(zero)))))]]) ).
cnf(refute_0_382,plain,
( eq(suc(double(suc(zero))),double(double(suc(zero)))) != eq(zero,addNat(zero,suc(zero)))
| eq(double(double(suc(zero))),suc(double(double(suc(zero))))) = eq(zero,addNat(zero,suc(zero))) ),
inference(resolve,[$cnf( $equal(eq(double(double(suc(zero))),suc(double(double(suc(zero))))),eq(suc(double(suc(zero))),double(double(suc(zero))))) )],[refute_0_380,refute_0_381]) ).
cnf(refute_0_383,plain,
eq(double(double(suc(zero))),suc(double(double(suc(zero))))) = eq(zero,addNat(zero,suc(zero))),
inference(resolve,[$cnf( $equal(eq(suc(double(suc(zero))),double(double(suc(zero)))),eq(zero,addNat(zero,suc(zero)))) )],[refute_0_375,refute_0_382]) ).
cnf(refute_0_384,plain,
( eq(double(double(suc(zero))),suc(double(double(suc(zero))))) != eq(zero,addNat(zero,suc(zero)))
| eq(zero,addNat(zero,suc(zero))) != bfalse
| eq(double(double(suc(zero))),suc(double(double(suc(zero))))) = bfalse ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(eq(double(double(suc(zero))),suc(double(double(suc(zero))))))),bind(Y0,$fot(eq(zero,addNat(zero,suc(zero))))),bind(Z0,$fot(bfalse))]]) ).
cnf(refute_0_385,plain,
( eq(zero,addNat(zero,suc(zero))) != bfalse
| eq(double(double(suc(zero))),suc(double(double(suc(zero))))) = bfalse ),
inference(resolve,[$cnf( $equal(eq(double(double(suc(zero))),suc(double(double(suc(zero))))),eq(zero,addNat(zero,suc(zero)))) )],[refute_0_383,refute_0_384]) ).
cnf(refute_0_386,plain,
eq(double(double(suc(zero))),suc(double(double(suc(zero))))) = bfalse,
inference(resolve,[$cnf( $equal(eq(zero,addNat(zero,suc(zero))),bfalse) )],[refute_0_352,refute_0_385]) ).
cnf(refute_0_387,plain,
eq(suc(X),suc(suc(double(double(suc(zero)))))) = eq(X,suc(double(double(suc(zero))))),
inference(subst,[],[axiom_025:[bind(Y,$fot(suc(double(double(suc(zero))))))]]) ).
cnf(refute_0_388,plain,
double(suc(double(suc(zero)))) = suc(addNat(double(suc(zero)),suc(double(suc(zero))))),
inference(subst,[],[refute_0_58:[bind(X_19,$fot(double(suc(zero))))]]) ).
cnf(refute_0_389,plain,
addNat(suc(suc(zero)),Y) = suc(addNat(suc(zero),Y)),
inference(subst,[],[axiom_014:[bind(Z,$fot(suc(zero)))]]) ).
cnf(refute_0_390,plain,
( addNat(suc(suc(zero)),Y) != suc(addNat(suc(zero),Y))
| suc(suc(zero)) != double(suc(zero))
| addNat(double(suc(zero)),Y) = suc(addNat(suc(zero),Y)) ),
introduced(tautology,[equality,[$cnf( $equal(addNat(suc(suc(zero)),Y),suc(addNat(suc(zero),Y))) ),[0,0],$fot(double(suc(zero)))]]) ).
cnf(refute_0_391,plain,
( addNat(suc(suc(zero)),Y) != suc(addNat(suc(zero),Y))
| addNat(double(suc(zero)),Y) = suc(addNat(suc(zero),Y)) ),
inference(resolve,[$cnf( $equal(suc(suc(zero)),double(suc(zero))) )],[refute_0_66,refute_0_390]) ).
cnf(refute_0_392,plain,
addNat(double(suc(zero)),Y) = suc(addNat(suc(zero),Y)),
inference(resolve,[$cnf( $equal(addNat(suc(suc(zero)),Y),suc(addNat(suc(zero),Y))) )],[refute_0_389,refute_0_391]) ).
cnf(refute_0_393,plain,
suc(addNat(zero,Y)) = suc(addNat(zero,Y)),
introduced(tautology,[refl,[$fot(suc(addNat(zero,Y)))]]) ).
cnf(refute_0_394,plain,
( addNat(zero,Y) != Y
| suc(addNat(zero,Y)) != suc(addNat(zero,Y))
| suc(addNat(zero,Y)) = suc(Y) ),
introduced(tautology,[equality,[$cnf( $equal(suc(addNat(zero,Y)),suc(addNat(zero,Y))) ),[1,0],$fot(Y)]]) ).
cnf(refute_0_395,plain,
( addNat(zero,Y) != Y
| suc(addNat(zero,Y)) = suc(Y) ),
inference(resolve,[$cnf( $equal(suc(addNat(zero,Y)),suc(addNat(zero,Y))) )],[refute_0_393,refute_0_394]) ).
cnf(refute_0_396,plain,
suc(addNat(zero,Y)) = suc(Y),
inference(resolve,[$cnf( $equal(addNat(zero,Y),Y) )],[axiom_013,refute_0_395]) ).
cnf(refute_0_397,plain,
addNat(suc(zero),Y) = suc(addNat(zero,Y)),
inference(subst,[],[axiom_014:[bind(Z,$fot(zero))]]) ).
cnf(refute_0_398,plain,
( addNat(suc(zero),Y) != suc(addNat(zero,Y))
| suc(addNat(zero,Y)) != suc(Y)
| addNat(suc(zero),Y) = suc(Y) ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(addNat(suc(zero),Y))),bind(Y0,$fot(suc(addNat(zero,Y)))),bind(Z0,$fot(suc(Y)))]]) ).
cnf(refute_0_399,plain,
( suc(addNat(zero,Y)) != suc(Y)
| addNat(suc(zero),Y) = suc(Y) ),
inference(resolve,[$cnf( $equal(addNat(suc(zero),Y),suc(addNat(zero,Y))) )],[refute_0_397,refute_0_398]) ).
cnf(refute_0_400,plain,
addNat(suc(zero),Y) = suc(Y),
inference(resolve,[$cnf( $equal(suc(addNat(zero,Y)),suc(Y)) )],[refute_0_396,refute_0_399]) ).
cnf(refute_0_401,plain,
suc(addNat(suc(zero),Y)) = suc(addNat(suc(zero),Y)),
introduced(tautology,[refl,[$fot(suc(addNat(suc(zero),Y)))]]) ).
cnf(refute_0_402,plain,
( addNat(suc(zero),Y) != suc(Y)
| suc(addNat(suc(zero),Y)) != suc(addNat(suc(zero),Y))
| suc(addNat(suc(zero),Y)) = suc(suc(Y)) ),
introduced(tautology,[equality,[$cnf( $equal(suc(addNat(suc(zero),Y)),suc(addNat(suc(zero),Y))) ),[1,0],$fot(suc(Y))]]) ).
cnf(refute_0_403,plain,
( addNat(suc(zero),Y) != suc(Y)
| suc(addNat(suc(zero),Y)) = suc(suc(Y)) ),
inference(resolve,[$cnf( $equal(suc(addNat(suc(zero),Y)),suc(addNat(suc(zero),Y))) )],[refute_0_401,refute_0_402]) ).
cnf(refute_0_404,plain,
suc(addNat(suc(zero),Y)) = suc(suc(Y)),
inference(resolve,[$cnf( $equal(addNat(suc(zero),Y),suc(Y)) )],[refute_0_400,refute_0_403]) ).
cnf(refute_0_405,plain,
( addNat(double(suc(zero)),Y) != suc(addNat(suc(zero),Y))
| suc(addNat(suc(zero),Y)) != suc(suc(Y))
| addNat(double(suc(zero)),Y) = suc(suc(Y)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(addNat(double(suc(zero)),Y),suc(suc(Y))) ),[0],$fot(suc(addNat(suc(zero),Y)))]]) ).
cnf(refute_0_406,plain,
( addNat(double(suc(zero)),Y) != suc(addNat(suc(zero),Y))
| addNat(double(suc(zero)),Y) = suc(suc(Y)) ),
inference(resolve,[$cnf( $equal(suc(addNat(suc(zero),Y)),suc(suc(Y))) )],[refute_0_404,refute_0_405]) ).
cnf(refute_0_407,plain,
addNat(double(suc(zero)),Y) = suc(suc(Y)),
inference(resolve,[$cnf( $equal(addNat(double(suc(zero)),Y),suc(addNat(suc(zero),Y))) )],[refute_0_392,refute_0_406]) ).
cnf(refute_0_408,plain,
addNat(double(suc(zero)),suc(double(suc(zero)))) = suc(suc(suc(double(suc(zero))))),
inference(subst,[],[refute_0_407:[bind(Y,$fot(suc(double(suc(zero)))))]]) ).
cnf(refute_0_409,plain,
( addNat(double(suc(zero)),suc(double(suc(zero)))) != suc(suc(suc(double(suc(zero)))))
| double(suc(double(suc(zero)))) != suc(addNat(double(suc(zero)),suc(double(suc(zero)))))
| double(suc(double(suc(zero)))) = suc(suc(suc(suc(double(suc(zero)))))) ),
introduced(tautology,[equality,[$cnf( $equal(double(suc(double(suc(zero)))),suc(addNat(double(suc(zero)),suc(double(suc(zero)))))) ),[1,0],$fot(suc(suc(suc(double(suc(zero))))))]]) ).
cnf(refute_0_410,plain,
( double(suc(double(suc(zero)))) != suc(addNat(double(suc(zero)),suc(double(suc(zero)))))
| double(suc(double(suc(zero)))) = suc(suc(suc(suc(double(suc(zero)))))) ),
inference(resolve,[$cnf( $equal(addNat(double(suc(zero)),suc(double(suc(zero)))),suc(suc(suc(double(suc(zero)))))) )],[refute_0_408,refute_0_409]) ).
cnf(refute_0_411,plain,
double(suc(double(suc(zero)))) = suc(suc(suc(suc(double(suc(zero)))))),
inference(resolve,[$cnf( $equal(double(suc(double(suc(zero)))),suc(addNat(double(suc(zero)),suc(double(suc(zero)))))) )],[refute_0_388,refute_0_410]) ).
cnf(refute_0_412,plain,
suc(suc(suc(suc(double(suc(zero)))))) = suc(suc(suc(suc(double(suc(zero)))))),
introduced(tautology,[refl,[$fot(suc(suc(suc(suc(double(suc(zero)))))))]]) ).
cnf(refute_0_413,plain,
( suc(suc(suc(double(suc(zero))))) != suc(double(double(suc(zero))))
| suc(suc(suc(suc(double(suc(zero)))))) != suc(suc(suc(suc(double(suc(zero))))))
| suc(suc(suc(suc(double(suc(zero)))))) = suc(suc(double(double(suc(zero))))) ),
introduced(tautology,[equality,[$cnf( $equal(suc(suc(suc(suc(double(suc(zero)))))),suc(suc(suc(suc(double(suc(zero))))))) ),[1,0],$fot(suc(double(double(suc(zero)))))]]) ).
cnf(refute_0_414,plain,
( suc(suc(suc(double(suc(zero))))) != suc(double(double(suc(zero))))
| suc(suc(suc(suc(double(suc(zero)))))) = suc(suc(double(double(suc(zero))))) ),
inference(resolve,[$cnf( $equal(suc(suc(suc(suc(double(suc(zero)))))),suc(suc(suc(suc(double(suc(zero))))))) )],[refute_0_412,refute_0_413]) ).
cnf(refute_0_415,plain,
suc(suc(suc(suc(double(suc(zero)))))) = suc(suc(double(double(suc(zero))))),
inference(resolve,[$cnf( $equal(suc(suc(suc(double(suc(zero))))),suc(double(double(suc(zero))))) )],[refute_0_185,refute_0_414]) ).
cnf(refute_0_416,plain,
( double(suc(double(suc(zero)))) != suc(suc(suc(suc(double(suc(zero))))))
| suc(suc(suc(suc(double(suc(zero)))))) != suc(suc(double(double(suc(zero)))))
| double(suc(double(suc(zero)))) = suc(suc(double(double(suc(zero))))) ),
introduced(tautology,[equality,[$cnf( ~ $equal(double(suc(double(suc(zero)))),suc(suc(double(double(suc(zero)))))) ),[0],$fot(suc(suc(suc(suc(double(suc(zero)))))))]]) ).
cnf(refute_0_417,plain,
( double(suc(double(suc(zero)))) != suc(suc(suc(suc(double(suc(zero))))))
| double(suc(double(suc(zero)))) = suc(suc(double(double(suc(zero))))) ),
inference(resolve,[$cnf( $equal(suc(suc(suc(suc(double(suc(zero)))))),suc(suc(double(double(suc(zero)))))) )],[refute_0_415,refute_0_416]) ).
cnf(refute_0_418,plain,
double(suc(double(suc(zero)))) = suc(suc(double(double(suc(zero))))),
inference(resolve,[$cnf( $equal(double(suc(double(suc(zero)))),suc(suc(suc(suc(double(suc(zero))))))) )],[refute_0_411,refute_0_417]) ).
cnf(refute_0_419,plain,
( double(suc(double(suc(zero)))) != suc(suc(double(double(suc(zero)))))
| suc(suc(double(double(suc(zero))))) = double(suc(double(suc(zero)))) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(double(suc(double(suc(zero)))))),bind(Y0,$fot(suc(suc(double(double(suc(zero)))))))]]) ).
cnf(refute_0_420,plain,
suc(suc(double(double(suc(zero))))) = double(suc(double(suc(zero)))),
inference(resolve,[$cnf( $equal(double(suc(double(suc(zero)))),suc(suc(double(double(suc(zero)))))) )],[refute_0_418,refute_0_419]) ).
cnf(refute_0_421,plain,
( eq(suc(X),suc(suc(double(double(suc(zero)))))) != eq(X,suc(double(double(suc(zero)))))
| suc(suc(double(double(suc(zero))))) != double(suc(double(suc(zero))))
| eq(suc(X),double(suc(double(suc(zero))))) = eq(X,suc(double(double(suc(zero))))) ),
introduced(tautology,[equality,[$cnf( $equal(eq(suc(X),suc(suc(double(double(suc(zero)))))),eq(X,suc(double(double(suc(zero)))))) ),[0,1],$fot(double(suc(double(suc(zero)))))]]) ).
cnf(refute_0_422,plain,
( eq(suc(X),suc(suc(double(double(suc(zero)))))) != eq(X,suc(double(double(suc(zero)))))
| eq(suc(X),double(suc(double(suc(zero))))) = eq(X,suc(double(double(suc(zero))))) ),
inference(resolve,[$cnf( $equal(suc(suc(double(double(suc(zero))))),double(suc(double(suc(zero))))) )],[refute_0_420,refute_0_421]) ).
cnf(refute_0_423,plain,
eq(suc(X),double(suc(double(suc(zero))))) = eq(X,suc(double(double(suc(zero))))),
inference(resolve,[$cnf( $equal(eq(suc(X),suc(suc(double(double(suc(zero)))))),eq(X,suc(double(double(suc(zero)))))) )],[refute_0_387,refute_0_422]) ).
cnf(refute_0_424,plain,
eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))) = eq(double(double(suc(zero))),suc(double(double(suc(zero))))),
inference(subst,[],[refute_0_423:[bind(X,$fot(double(double(suc(zero)))))]]) ).
cnf(refute_0_425,plain,
( eq(double(double(suc(zero))),suc(double(double(suc(zero))))) != bfalse
| eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))) != eq(double(double(suc(zero))),suc(double(double(suc(zero)))))
| eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))) = bfalse ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))))),bind(Y0,$fot(eq(double(double(suc(zero))),suc(double(double(suc(zero))))))),bind(Z0,$fot(bfalse))]]) ).
cnf(refute_0_426,plain,
( eq(double(double(suc(zero))),suc(double(double(suc(zero))))) != bfalse
| eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))) = bfalse ),
inference(resolve,[$cnf( $equal(eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))),eq(double(double(suc(zero))),suc(double(double(suc(zero)))))) )],[refute_0_424,refute_0_425]) ).
cnf(refute_0_427,plain,
eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))) = bfalse,
inference(resolve,[$cnf( $equal(eq(double(double(suc(zero))),suc(double(double(suc(zero))))),bfalse) )],[refute_0_386,refute_0_426]) ).
cnf(refute_0_428,plain,
x(suc(zero),suc(zero)) = rd(cons(i,shw(suc(zero)))),
inference(subst,[],[refute_0_50:[bind(Y,$fot(suc(zero)))]]) ).
cnf(refute_0_429,plain,
aux(suc(N),bfalse) = cons(i,shw(half(suc(suc(N))))),
inference(subst,[],[axiom_001:[bind(Y,$fot(suc(N)))]]) ).
cnf(refute_0_430,plain,
( aux(suc(N),bfalse) != cons(i,shw(half(suc(suc(N)))))
| half(suc(suc(N))) != suc(half(N))
| aux(suc(N),bfalse) = cons(i,shw(suc(half(N)))) ),
introduced(tautology,[equality,[$cnf( $equal(aux(suc(N),bfalse),cons(i,shw(half(suc(suc(N)))))) ),[1,1,0],$fot(suc(half(N)))]]) ).
cnf(refute_0_431,plain,
( aux(suc(N),bfalse) != cons(i,shw(half(suc(suc(N)))))
| aux(suc(N),bfalse) = cons(i,shw(suc(half(N)))) ),
inference(resolve,[$cnf( $equal(half(suc(suc(N))),suc(half(N))) )],[axiom_006,refute_0_430]) ).
cnf(refute_0_432,plain,
aux(suc(N),bfalse) = cons(i,shw(suc(half(N)))),
inference(resolve,[$cnf( $equal(aux(suc(N),bfalse),cons(i,shw(half(suc(suc(N)))))) )],[refute_0_429,refute_0_431]) ).
cnf(refute_0_433,plain,
aux(suc(zero),bfalse) = cons(i,shw(suc(half(zero)))),
inference(subst,[],[refute_0_432:[bind(N,$fot(zero))]]) ).
cnf(refute_0_434,plain,
( aux(suc(zero),bfalse) != cons(i,shw(suc(half(zero))))
| half(zero) != zero
| aux(suc(zero),bfalse) = cons(i,shw(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(aux(suc(zero),bfalse),cons(i,shw(suc(half(zero))))) ),[1,1,0,0],$fot(zero)]]) ).
cnf(refute_0_435,plain,
( aux(suc(zero),bfalse) != cons(i,shw(suc(half(zero))))
| aux(suc(zero),bfalse) = cons(i,shw(suc(zero))) ),
inference(resolve,[$cnf( $equal(half(zero),zero) )],[axiom_004,refute_0_434]) ).
cnf(refute_0_436,plain,
aux(suc(zero),bfalse) = cons(i,shw(suc(zero))),
inference(resolve,[$cnf( $equal(aux(suc(zero),bfalse),cons(i,shw(suc(half(zero))))) )],[refute_0_433,refute_0_435]) ).
cnf(refute_0_437,plain,
( aux(suc(zero),bfalse) != cons(i,shw(suc(zero)))
| cons(i,shw(suc(zero))) = aux(suc(zero),bfalse) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(aux(suc(zero),bfalse))),bind(Y0,$fot(cons(i,shw(suc(zero)))))]]) ).
cnf(refute_0_438,plain,
cons(i,shw(suc(zero))) = aux(suc(zero),bfalse),
inference(resolve,[$cnf( $equal(aux(suc(zero),bfalse),cons(i,shw(suc(zero)))) )],[refute_0_436,refute_0_437]) ).
cnf(refute_0_439,plain,
( cons(i,shw(suc(zero))) != aux(suc(zero),bfalse)
| x(suc(zero),suc(zero)) != rd(cons(i,shw(suc(zero))))
| x(suc(zero),suc(zero)) = rd(aux(suc(zero),bfalse)) ),
introduced(tautology,[equality,[$cnf( $equal(x(suc(zero),suc(zero)),rd(cons(i,shw(suc(zero))))) ),[1,0],$fot(aux(suc(zero),bfalse))]]) ).
cnf(refute_0_440,plain,
( x(suc(zero),suc(zero)) != rd(cons(i,shw(suc(zero))))
| x(suc(zero),suc(zero)) = rd(aux(suc(zero),bfalse)) ),
inference(resolve,[$cnf( $equal(cons(i,shw(suc(zero))),aux(suc(zero),bfalse)) )],[refute_0_438,refute_0_439]) ).
cnf(refute_0_441,plain,
x(suc(zero),suc(zero)) = rd(aux(suc(zero),bfalse)),
inference(resolve,[$cnf( $equal(x(suc(zero),suc(zero)),rd(cons(i,shw(suc(zero))))) )],[refute_0_428,refute_0_440]) ).
cnf(refute_0_442,plain,
rd(cons(i,shw(half(suc(X_26))))) = suc(double(rd(shw(half(suc(X_26)))))),
inference(subst,[],[axiom_017:[bind(Xs,$fot(shw(half(suc(X_26)))))]]) ).
cnf(refute_0_443,plain,
rd(aux(X_26,btrue)) = double(rd(shw(half(suc(X_26))))),
inference(subst,[],[refute_0_216:[bind(Y,$fot(X_26))]]) ).
cnf(refute_0_444,plain,
( rd(aux(X_26,btrue)) != double(rd(shw(half(suc(X_26)))))
| double(rd(shw(half(suc(X_26))))) = rd(aux(X_26,btrue)) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(rd(aux(X_26,btrue)))),bind(Y0,$fot(double(rd(shw(half(suc(X_26)))))))]]) ).
cnf(refute_0_445,plain,
double(rd(shw(half(suc(X_26))))) = rd(aux(X_26,btrue)),
inference(resolve,[$cnf( $equal(rd(aux(X_26,btrue)),double(rd(shw(half(suc(X_26)))))) )],[refute_0_443,refute_0_444]) ).
cnf(refute_0_446,plain,
( double(rd(shw(half(suc(X_26))))) != rd(aux(X_26,btrue))
| rd(cons(i,shw(half(suc(X_26))))) != suc(double(rd(shw(half(suc(X_26))))))
| rd(cons(i,shw(half(suc(X_26))))) = suc(rd(aux(X_26,btrue))) ),
introduced(tautology,[equality,[$cnf( $equal(rd(cons(i,shw(half(suc(X_26))))),suc(double(rd(shw(half(suc(X_26))))))) ),[1,0],$fot(rd(aux(X_26,btrue)))]]) ).
cnf(refute_0_447,plain,
( rd(cons(i,shw(half(suc(X_26))))) != suc(double(rd(shw(half(suc(X_26))))))
| rd(cons(i,shw(half(suc(X_26))))) = suc(rd(aux(X_26,btrue))) ),
inference(resolve,[$cnf( $equal(double(rd(shw(half(suc(X_26))))),rd(aux(X_26,btrue))) )],[refute_0_445,refute_0_446]) ).
cnf(refute_0_448,plain,
rd(cons(i,shw(half(suc(X_26))))) = suc(rd(aux(X_26,btrue))),
inference(resolve,[$cnf( $equal(rd(cons(i,shw(half(suc(X_26))))),suc(double(rd(shw(half(suc(X_26))))))) )],[refute_0_442,refute_0_447]) ).
cnf(refute_0_449,plain,
( aux(Y,bfalse) != cons(i,shw(half(suc(Y))))
| cons(i,shw(half(suc(Y)))) = aux(Y,bfalse) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(aux(Y,bfalse))),bind(Y0,$fot(cons(i,shw(half(suc(Y))))))]]) ).
cnf(refute_0_450,plain,
cons(i,shw(half(suc(Y)))) = aux(Y,bfalse),
inference(resolve,[$cnf( $equal(aux(Y,bfalse),cons(i,shw(half(suc(Y))))) )],[axiom_001,refute_0_449]) ).
cnf(refute_0_451,plain,
cons(i,shw(half(suc(X_26)))) = aux(X_26,bfalse),
inference(subst,[],[refute_0_450:[bind(Y,$fot(X_26))]]) ).
cnf(refute_0_452,plain,
rd(cons(i,shw(half(suc(X_26))))) = rd(cons(i,shw(half(suc(X_26))))),
introduced(tautology,[refl,[$fot(rd(cons(i,shw(half(suc(X_26))))))]]) ).
cnf(refute_0_453,plain,
( cons(i,shw(half(suc(X_26)))) != aux(X_26,bfalse)
| rd(cons(i,shw(half(suc(X_26))))) != rd(cons(i,shw(half(suc(X_26)))))
| rd(cons(i,shw(half(suc(X_26))))) = rd(aux(X_26,bfalse)) ),
introduced(tautology,[equality,[$cnf( $equal(rd(cons(i,shw(half(suc(X_26))))),rd(cons(i,shw(half(suc(X_26)))))) ),[1,0],$fot(aux(X_26,bfalse))]]) ).
cnf(refute_0_454,plain,
( cons(i,shw(half(suc(X_26)))) != aux(X_26,bfalse)
| rd(cons(i,shw(half(suc(X_26))))) = rd(aux(X_26,bfalse)) ),
inference(resolve,[$cnf( $equal(rd(cons(i,shw(half(suc(X_26))))),rd(cons(i,shw(half(suc(X_26)))))) )],[refute_0_452,refute_0_453]) ).
cnf(refute_0_455,plain,
rd(cons(i,shw(half(suc(X_26))))) = rd(aux(X_26,bfalse)),
inference(resolve,[$cnf( $equal(cons(i,shw(half(suc(X_26)))),aux(X_26,bfalse)) )],[refute_0_451,refute_0_454]) ).
cnf(refute_0_456,plain,
( rd(cons(i,shw(half(suc(X_26))))) != rd(aux(X_26,bfalse))
| rd(cons(i,shw(half(suc(X_26))))) != suc(rd(aux(X_26,btrue)))
| rd(aux(X_26,bfalse)) = suc(rd(aux(X_26,btrue))) ),
introduced(tautology,[equality,[$cnf( $equal(rd(cons(i,shw(half(suc(X_26))))),suc(rd(aux(X_26,btrue)))) ),[0],$fot(rd(aux(X_26,bfalse)))]]) ).
cnf(refute_0_457,plain,
( rd(cons(i,shw(half(suc(X_26))))) != suc(rd(aux(X_26,btrue)))
| rd(aux(X_26,bfalse)) = suc(rd(aux(X_26,btrue))) ),
inference(resolve,[$cnf( $equal(rd(cons(i,shw(half(suc(X_26))))),rd(aux(X_26,bfalse))) )],[refute_0_455,refute_0_456]) ).
cnf(refute_0_458,plain,
rd(aux(X_26,bfalse)) = suc(rd(aux(X_26,btrue))),
inference(resolve,[$cnf( $equal(rd(cons(i,shw(half(suc(X_26))))),suc(rd(aux(X_26,btrue)))) )],[refute_0_448,refute_0_457]) ).
cnf(refute_0_459,plain,
rd(aux(suc(zero),bfalse)) = suc(rd(aux(suc(zero),btrue))),
inference(subst,[],[refute_0_458:[bind(X_26,$fot(suc(zero)))]]) ).
cnf(refute_0_460,plain,
( aux(suc(zero),btrue) != shw(double(suc(zero)))
| rd(aux(suc(zero),bfalse)) != suc(rd(aux(suc(zero),btrue)))
| rd(aux(suc(zero),bfalse)) = suc(rd(shw(double(suc(zero))))) ),
introduced(tautology,[equality,[$cnf( $equal(rd(aux(suc(zero),bfalse)),suc(rd(aux(suc(zero),btrue)))) ),[1,0,0],$fot(shw(double(suc(zero))))]]) ).
cnf(refute_0_461,plain,
( rd(aux(suc(zero),bfalse)) != suc(rd(aux(suc(zero),btrue)))
| rd(aux(suc(zero),bfalse)) = suc(rd(shw(double(suc(zero))))) ),
inference(resolve,[$cnf( $equal(aux(suc(zero),btrue),shw(double(suc(zero)))) )],[refute_0_233,refute_0_460]) ).
cnf(refute_0_462,plain,
rd(aux(suc(zero),bfalse)) = suc(rd(shw(double(suc(zero))))),
inference(resolve,[$cnf( $equal(rd(aux(suc(zero),bfalse)),suc(rd(aux(suc(zero),btrue)))) )],[refute_0_459,refute_0_461]) ).
cnf(refute_0_463,plain,
suc(rd(shw(double(suc(zero))))) = suc(rd(shw(double(suc(zero))))),
introduced(tautology,[refl,[$fot(suc(rd(shw(double(suc(zero))))))]]) ).
cnf(refute_0_464,plain,
( rd(shw(double(suc(zero)))) != double(suc(zero))
| suc(rd(shw(double(suc(zero))))) != suc(rd(shw(double(suc(zero)))))
| suc(rd(shw(double(suc(zero))))) = suc(double(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(suc(rd(shw(double(suc(zero))))),suc(rd(shw(double(suc(zero)))))) ),[1,0],$fot(double(suc(zero)))]]) ).
cnf(refute_0_465,plain,
( rd(shw(double(suc(zero)))) != double(suc(zero))
| suc(rd(shw(double(suc(zero))))) = suc(double(suc(zero))) ),
inference(resolve,[$cnf( $equal(suc(rd(shw(double(suc(zero))))),suc(rd(shw(double(suc(zero)))))) )],[refute_0_463,refute_0_464]) ).
cnf(refute_0_466,plain,
suc(rd(shw(double(suc(zero))))) = suc(double(suc(zero))),
inference(resolve,[$cnf( $equal(rd(shw(double(suc(zero)))),double(suc(zero))) )],[refute_0_328,refute_0_465]) ).
cnf(refute_0_467,plain,
( rd(aux(suc(zero),bfalse)) != suc(rd(shw(double(suc(zero)))))
| suc(rd(shw(double(suc(zero))))) != suc(double(suc(zero)))
| rd(aux(suc(zero),bfalse)) = suc(double(suc(zero))) ),
introduced(tautology,[equality,[$cnf( ~ $equal(rd(aux(suc(zero),bfalse)),suc(double(suc(zero)))) ),[0],$fot(suc(rd(shw(double(suc(zero))))))]]) ).
cnf(refute_0_468,plain,
( rd(aux(suc(zero),bfalse)) != suc(rd(shw(double(suc(zero)))))
| rd(aux(suc(zero),bfalse)) = suc(double(suc(zero))) ),
inference(resolve,[$cnf( $equal(suc(rd(shw(double(suc(zero))))),suc(double(suc(zero)))) )],[refute_0_466,refute_0_467]) ).
cnf(refute_0_469,plain,
rd(aux(suc(zero),bfalse)) = suc(double(suc(zero))),
inference(resolve,[$cnf( $equal(rd(aux(suc(zero),bfalse)),suc(rd(shw(double(suc(zero)))))) )],[refute_0_462,refute_0_468]) ).
cnf(refute_0_470,plain,
( rd(aux(suc(zero),bfalse)) != suc(double(suc(zero)))
| x(suc(zero),suc(zero)) != rd(aux(suc(zero),bfalse))
| x(suc(zero),suc(zero)) = suc(double(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(x(suc(zero),suc(zero)),rd(aux(suc(zero),bfalse))) ),[1],$fot(suc(double(suc(zero))))]]) ).
cnf(refute_0_471,plain,
( x(suc(zero),suc(zero)) != rd(aux(suc(zero),bfalse))
| x(suc(zero),suc(zero)) = suc(double(suc(zero))) ),
inference(resolve,[$cnf( $equal(rd(aux(suc(zero),bfalse)),suc(double(suc(zero)))) )],[refute_0_469,refute_0_470]) ).
cnf(refute_0_472,plain,
x(suc(zero),suc(zero)) = suc(double(suc(zero))),
inference(resolve,[$cnf( $equal(x(suc(zero),suc(zero)),rd(aux(suc(zero),bfalse))) )],[refute_0_441,refute_0_471]) ).
cnf(refute_0_473,plain,
double(x(suc(zero),suc(zero))) = double(x(suc(zero),suc(zero))),
introduced(tautology,[refl,[$fot(double(x(suc(zero),suc(zero))))]]) ).
cnf(refute_0_474,plain,
( double(x(suc(zero),suc(zero))) != double(x(suc(zero),suc(zero)))
| x(suc(zero),suc(zero)) != suc(double(suc(zero)))
| double(x(suc(zero),suc(zero))) = double(suc(double(suc(zero)))) ),
introduced(tautology,[equality,[$cnf( $equal(double(x(suc(zero),suc(zero))),double(x(suc(zero),suc(zero)))) ),[1,0],$fot(suc(double(suc(zero))))]]) ).
cnf(refute_0_475,plain,
( x(suc(zero),suc(zero)) != suc(double(suc(zero)))
| double(x(suc(zero),suc(zero))) = double(suc(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(double(x(suc(zero),suc(zero))),double(x(suc(zero),suc(zero)))) )],[refute_0_473,refute_0_474]) ).
cnf(refute_0_476,plain,
double(x(suc(zero),suc(zero))) = double(suc(double(suc(zero)))),
inference(resolve,[$cnf( $equal(x(suc(zero),suc(zero)),suc(double(suc(zero)))) )],[refute_0_472,refute_0_475]) ).
cnf(refute_0_477,plain,
x(double(suc(zero)),Y) = rd(append(shw(double(suc(zero))),shw(Y))),
inference(subst,[],[axiom_019:[bind(X,$fot(double(suc(zero))))]]) ).
cnf(refute_0_478,plain,
append(cons(o,shw(suc(zero))),X_129) = cons(o,append(shw(suc(zero)),X_129)),
inference(subst,[],[axiom_012:[bind(Xs,$fot(shw(suc(zero)))),bind(Y,$fot(X_129)),bind(Z,$fot(o))]]) ).
cnf(refute_0_479,plain,
aux(suc(X_15),btrue) = cons(o,shw(half(suc(suc(X_15))))),
inference(subst,[],[axiom:[bind(Y,$fot(suc(X_15)))]]) ).
cnf(refute_0_480,plain,
half(suc(suc(X_15))) = suc(half(X_15)),
inference(subst,[],[axiom_006:[bind(N,$fot(X_15))]]) ).
cnf(refute_0_481,plain,
( aux(suc(X_15),btrue) != cons(o,shw(half(suc(suc(X_15)))))
| half(suc(suc(X_15))) != suc(half(X_15))
| aux(suc(X_15),btrue) = cons(o,shw(suc(half(X_15)))) ),
introduced(tautology,[equality,[$cnf( $equal(aux(suc(X_15),btrue),cons(o,shw(half(suc(suc(X_15)))))) ),[1,1,0],$fot(suc(half(X_15)))]]) ).
cnf(refute_0_482,plain,
( aux(suc(X_15),btrue) != cons(o,shw(half(suc(suc(X_15)))))
| aux(suc(X_15),btrue) = cons(o,shw(suc(half(X_15)))) ),
inference(resolve,[$cnf( $equal(half(suc(suc(X_15))),suc(half(X_15))) )],[refute_0_480,refute_0_481]) ).
cnf(refute_0_483,plain,
aux(suc(X_15),btrue) = cons(o,shw(suc(half(X_15)))),
inference(resolve,[$cnf( $equal(aux(suc(X_15),btrue),cons(o,shw(half(suc(suc(X_15)))))) )],[refute_0_479,refute_0_482]) ).
cnf(refute_0_484,plain,
aux(suc(zero),btrue) = cons(o,shw(suc(half(zero)))),
inference(subst,[],[refute_0_483:[bind(X_15,$fot(zero))]]) ).
cnf(refute_0_485,plain,
( aux(suc(zero),btrue) != cons(o,shw(suc(half(zero))))
| half(zero) != zero
| aux(suc(zero),btrue) = cons(o,shw(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(aux(suc(zero),btrue),cons(o,shw(suc(half(zero))))) ),[1,1,0,0],$fot(zero)]]) ).
cnf(refute_0_486,plain,
( aux(suc(zero),btrue) != cons(o,shw(suc(half(zero))))
| aux(suc(zero),btrue) = cons(o,shw(suc(zero))) ),
inference(resolve,[$cnf( $equal(half(zero),zero) )],[axiom_004,refute_0_485]) ).
cnf(refute_0_487,plain,
aux(suc(zero),btrue) = cons(o,shw(suc(zero))),
inference(resolve,[$cnf( $equal(aux(suc(zero),btrue),cons(o,shw(suc(half(zero))))) )],[refute_0_484,refute_0_486]) ).
cnf(refute_0_488,plain,
( aux(suc(zero),btrue) != cons(o,shw(suc(zero)))
| aux(suc(zero),btrue) != shw(double(suc(zero)))
| shw(double(suc(zero))) = cons(o,shw(suc(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(aux(suc(zero),btrue),cons(o,shw(suc(zero)))) ),[0],$fot(shw(double(suc(zero))))]]) ).
cnf(refute_0_489,plain,
( aux(suc(zero),btrue) != cons(o,shw(suc(zero)))
| shw(double(suc(zero))) = cons(o,shw(suc(zero))) ),
inference(resolve,[$cnf( $equal(aux(suc(zero),btrue),shw(double(suc(zero)))) )],[refute_0_233,refute_0_488]) ).
cnf(refute_0_490,plain,
shw(double(suc(zero))) = cons(o,shw(suc(zero))),
inference(resolve,[$cnf( $equal(aux(suc(zero),btrue),cons(o,shw(suc(zero)))) )],[refute_0_487,refute_0_489]) ).
cnf(refute_0_491,plain,
( shw(double(suc(zero))) != cons(o,shw(suc(zero)))
| cons(o,shw(suc(zero))) = shw(double(suc(zero))) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(shw(double(suc(zero))))),bind(Y0,$fot(cons(o,shw(suc(zero)))))]]) ).
cnf(refute_0_492,plain,
cons(o,shw(suc(zero))) = shw(double(suc(zero))),
inference(resolve,[$cnf( $equal(shw(double(suc(zero))),cons(o,shw(suc(zero)))) )],[refute_0_490,refute_0_491]) ).
cnf(refute_0_493,plain,
( cons(o,shw(suc(zero))) != shw(double(suc(zero)))
| append(cons(o,shw(suc(zero))),X_129) != cons(o,append(shw(suc(zero)),X_129))
| append(shw(double(suc(zero))),X_129) = cons(o,append(shw(suc(zero)),X_129)) ),
introduced(tautology,[equality,[$cnf( $equal(append(cons(o,shw(suc(zero))),X_129),cons(o,append(shw(suc(zero)),X_129))) ),[0,0],$fot(shw(double(suc(zero))))]]) ).
cnf(refute_0_494,plain,
( append(cons(o,shw(suc(zero))),X_129) != cons(o,append(shw(suc(zero)),X_129))
| append(shw(double(suc(zero))),X_129) = cons(o,append(shw(suc(zero)),X_129)) ),
inference(resolve,[$cnf( $equal(cons(o,shw(suc(zero))),shw(double(suc(zero)))) )],[refute_0_492,refute_0_493]) ).
cnf(refute_0_495,plain,
append(shw(double(suc(zero))),X_129) = cons(o,append(shw(suc(zero)),X_129)),
inference(resolve,[$cnf( $equal(append(cons(o,shw(suc(zero))),X_129),cons(o,append(shw(suc(zero)),X_129))) )],[refute_0_478,refute_0_494]) ).
cnf(refute_0_496,plain,
cons(o,append(shw(suc(zero)),X_129)) = cons(o,append(shw(suc(zero)),X_129)),
introduced(tautology,[refl,[$fot(cons(o,append(shw(suc(zero)),X_129)))]]) ).
cnf(refute_0_497,plain,
( cons(o,append(shw(suc(zero)),X_129)) != cons(o,append(shw(suc(zero)),X_129))
| append(shw(suc(zero)),X_129) != cons(i,X_129)
| cons(o,append(shw(suc(zero)),X_129)) = cons(o,cons(i,X_129)) ),
introduced(tautology,[equality,[$cnf( $equal(cons(o,append(shw(suc(zero)),X_129)),cons(o,append(shw(suc(zero)),X_129))) ),[1,1],$fot(cons(i,X_129))]]) ).
cnf(refute_0_498,plain,
( append(shw(suc(zero)),X_129) != cons(i,X_129)
| cons(o,append(shw(suc(zero)),X_129)) = cons(o,cons(i,X_129)) ),
inference(resolve,[$cnf( $equal(cons(o,append(shw(suc(zero)),X_129)),cons(o,append(shw(suc(zero)),X_129))) )],[refute_0_496,refute_0_497]) ).
cnf(refute_0_499,plain,
cons(o,append(shw(suc(zero)),X_129)) = cons(o,cons(i,X_129)),
inference(resolve,[$cnf( $equal(append(shw(suc(zero)),X_129),cons(i,X_129)) )],[refute_0_46,refute_0_498]) ).
cnf(refute_0_500,plain,
( cons(o,append(shw(suc(zero)),X_129)) != cons(o,cons(i,X_129))
| append(shw(double(suc(zero))),X_129) != cons(o,append(shw(suc(zero)),X_129))
| append(shw(double(suc(zero))),X_129) = cons(o,cons(i,X_129)) ),
introduced(tautology,[equality,[$cnf( $equal(append(shw(double(suc(zero))),X_129),cons(o,append(shw(suc(zero)),X_129))) ),[1],$fot(cons(o,cons(i,X_129)))]]) ).
cnf(refute_0_501,plain,
( append(shw(double(suc(zero))),X_129) != cons(o,append(shw(suc(zero)),X_129))
| append(shw(double(suc(zero))),X_129) = cons(o,cons(i,X_129)) ),
inference(resolve,[$cnf( $equal(cons(o,append(shw(suc(zero)),X_129)),cons(o,cons(i,X_129))) )],[refute_0_499,refute_0_500]) ).
cnf(refute_0_502,plain,
append(shw(double(suc(zero))),X_129) = cons(o,cons(i,X_129)),
inference(resolve,[$cnf( $equal(append(shw(double(suc(zero))),X_129),cons(o,append(shw(suc(zero)),X_129))) )],[refute_0_495,refute_0_501]) ).
cnf(refute_0_503,plain,
append(shw(double(suc(zero))),shw(Y)) = cons(o,cons(i,shw(Y))),
inference(subst,[],[refute_0_502:[bind(X_129,$fot(shw(Y)))]]) ).
cnf(refute_0_504,plain,
( append(shw(double(suc(zero))),shw(Y)) != cons(o,cons(i,shw(Y)))
| x(double(suc(zero)),Y) != rd(append(shw(double(suc(zero))),shw(Y)))
| x(double(suc(zero)),Y) = rd(cons(o,cons(i,shw(Y)))) ),
introduced(tautology,[equality,[$cnf( $equal(x(double(suc(zero)),Y),rd(append(shw(double(suc(zero))),shw(Y)))) ),[1,0],$fot(cons(o,cons(i,shw(Y))))]]) ).
cnf(refute_0_505,plain,
( x(double(suc(zero)),Y) != rd(append(shw(double(suc(zero))),shw(Y)))
| x(double(suc(zero)),Y) = rd(cons(o,cons(i,shw(Y)))) ),
inference(resolve,[$cnf( $equal(append(shw(double(suc(zero))),shw(Y)),cons(o,cons(i,shw(Y)))) )],[refute_0_503,refute_0_504]) ).
cnf(refute_0_506,plain,
x(double(suc(zero)),Y) = rd(cons(o,cons(i,shw(Y)))),
inference(resolve,[$cnf( $equal(x(double(suc(zero)),Y),rd(append(shw(double(suc(zero))),shw(Y)))) )],[refute_0_477,refute_0_505]) ).
cnf(refute_0_507,plain,
( x(suc(zero),Y) != rd(cons(i,shw(Y)))
| rd(cons(i,shw(Y))) = x(suc(zero),Y) ),
inference(subst,[],[refute_0_21:[bind(X0,$fot(x(suc(zero),Y))),bind(Y0,$fot(rd(cons(i,shw(Y)))))]]) ).
cnf(refute_0_508,plain,
rd(cons(i,shw(Y))) = x(suc(zero),Y),
inference(resolve,[$cnf( $equal(x(suc(zero),Y),rd(cons(i,shw(Y)))) )],[refute_0_50,refute_0_507]) ).
cnf(refute_0_509,plain,
double(rd(cons(i,shw(Y)))) = double(rd(cons(i,shw(Y)))),
introduced(tautology,[refl,[$fot(double(rd(cons(i,shw(Y)))))]]) ).
cnf(refute_0_510,plain,
( double(rd(cons(i,shw(Y)))) != double(rd(cons(i,shw(Y))))
| rd(cons(i,shw(Y))) != x(suc(zero),Y)
| double(rd(cons(i,shw(Y)))) = double(x(suc(zero),Y)) ),
introduced(tautology,[equality,[$cnf( $equal(double(rd(cons(i,shw(Y)))),double(rd(cons(i,shw(Y))))) ),[1,0],$fot(x(suc(zero),Y))]]) ).
cnf(refute_0_511,plain,
( rd(cons(i,shw(Y))) != x(suc(zero),Y)
| double(rd(cons(i,shw(Y)))) = double(x(suc(zero),Y)) ),
inference(resolve,[$cnf( $equal(double(rd(cons(i,shw(Y)))),double(rd(cons(i,shw(Y))))) )],[refute_0_509,refute_0_510]) ).
cnf(refute_0_512,plain,
double(rd(cons(i,shw(Y)))) = double(x(suc(zero),Y)),
inference(resolve,[$cnf( $equal(rd(cons(i,shw(Y))),x(suc(zero),Y)) )],[refute_0_508,refute_0_511]) ).
cnf(refute_0_513,plain,
rd(cons(o,cons(i,shw(Y)))) = double(rd(cons(i,shw(Y)))),
inference(subst,[],[axiom_018:[bind(Xs,$fot(cons(i,shw(Y))))]]) ).
cnf(refute_0_514,plain,
( double(rd(cons(i,shw(Y)))) != double(x(suc(zero),Y))
| rd(cons(o,cons(i,shw(Y)))) != double(rd(cons(i,shw(Y))))
| rd(cons(o,cons(i,shw(Y)))) = double(x(suc(zero),Y)) ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(rd(cons(o,cons(i,shw(Y)))))),bind(Y0,$fot(double(rd(cons(i,shw(Y)))))),bind(Z0,$fot(double(x(suc(zero),Y))))]]) ).
cnf(refute_0_515,plain,
( double(rd(cons(i,shw(Y)))) != double(x(suc(zero),Y))
| rd(cons(o,cons(i,shw(Y)))) = double(x(suc(zero),Y)) ),
inference(resolve,[$cnf( $equal(rd(cons(o,cons(i,shw(Y)))),double(rd(cons(i,shw(Y))))) )],[refute_0_513,refute_0_514]) ).
cnf(refute_0_516,plain,
rd(cons(o,cons(i,shw(Y)))) = double(x(suc(zero),Y)),
inference(resolve,[$cnf( $equal(double(rd(cons(i,shw(Y)))),double(x(suc(zero),Y))) )],[refute_0_512,refute_0_515]) ).
cnf(refute_0_517,plain,
( rd(cons(o,cons(i,shw(Y)))) != double(x(suc(zero),Y))
| x(double(suc(zero)),Y) != rd(cons(o,cons(i,shw(Y))))
| x(double(suc(zero)),Y) = double(x(suc(zero),Y)) ),
introduced(tautology,[equality,[$cnf( $equal(x(double(suc(zero)),Y),rd(cons(o,cons(i,shw(Y))))) ),[1],$fot(double(x(suc(zero),Y)))]]) ).
cnf(refute_0_518,plain,
( x(double(suc(zero)),Y) != rd(cons(o,cons(i,shw(Y))))
| x(double(suc(zero)),Y) = double(x(suc(zero),Y)) ),
inference(resolve,[$cnf( $equal(rd(cons(o,cons(i,shw(Y)))),double(x(suc(zero),Y))) )],[refute_0_516,refute_0_517]) ).
cnf(refute_0_519,plain,
x(double(suc(zero)),Y) = double(x(suc(zero),Y)),
inference(resolve,[$cnf( $equal(x(double(suc(zero)),Y),rd(cons(o,cons(i,shw(Y))))) )],[refute_0_506,refute_0_518]) ).
cnf(refute_0_520,plain,
x(double(suc(zero)),suc(zero)) = double(x(suc(zero),suc(zero))),
inference(subst,[],[refute_0_519:[bind(Y,$fot(suc(zero)))]]) ).
cnf(refute_0_521,plain,
( double(x(suc(zero),suc(zero))) != double(suc(double(suc(zero))))
| x(double(suc(zero)),suc(zero)) != double(x(suc(zero),suc(zero)))
| x(double(suc(zero)),suc(zero)) = double(suc(double(suc(zero)))) ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(x(double(suc(zero)),suc(zero)))),bind(Y0,$fot(double(x(suc(zero),suc(zero))))),bind(Z0,$fot(double(suc(double(suc(zero))))))]]) ).
cnf(refute_0_522,plain,
( double(x(suc(zero),suc(zero))) != double(suc(double(suc(zero))))
| x(double(suc(zero)),suc(zero)) = double(suc(double(suc(zero)))) ),
inference(resolve,[$cnf( $equal(x(double(suc(zero)),suc(zero)),double(x(suc(zero),suc(zero)))) )],[refute_0_520,refute_0_521]) ).
cnf(refute_0_523,plain,
x(double(suc(zero)),suc(zero)) = double(suc(double(suc(zero)))),
inference(resolve,[$cnf( $equal(double(x(suc(zero),suc(zero))),double(suc(double(suc(zero))))) )],[refute_0_476,refute_0_522]) ).
cnf(refute_0_524,plain,
eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))) = eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))),
introduced(tautology,[refl,[$fot(eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))))]]) ).
cnf(refute_0_525,plain,
( eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))) != eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero)))
| x(double(suc(zero)),suc(zero)) != double(suc(double(suc(zero))))
| eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))) = eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))) ),
introduced(tautology,[equality,[$cnf( $equal(eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))),eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero)))) ),[1,1],$fot(double(suc(double(suc(zero)))))]]) ).
cnf(refute_0_526,plain,
( x(double(suc(zero)),suc(zero)) != double(suc(double(suc(zero))))
| eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))) = eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))) ),
inference(resolve,[$cnf( $equal(eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))),eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero)))) )],[refute_0_524,refute_0_525]) ).
cnf(refute_0_527,plain,
eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))) = eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))),
inference(resolve,[$cnf( $equal(x(double(suc(zero)),suc(zero)),double(suc(double(suc(zero))))) )],[refute_0_523,refute_0_526]) ).
cnf(refute_0_528,plain,
( eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))) != bfalse
| eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))) != eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero)))))
| eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))) = bfalse ),
inference(subst,[],[refute_0_83:[bind(X0,$fot(eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))))),bind(Y0,$fot(eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))))),bind(Z0,$fot(bfalse))]]) ).
cnf(refute_0_529,plain,
( eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))) != bfalse
| eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))) = bfalse ),
inference(resolve,[$cnf( $equal(eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))),eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero)))))) )],[refute_0_527,refute_0_528]) ).
cnf(refute_0_530,plain,
eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))) = bfalse,
inference(resolve,[$cnf( $equal(eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))),bfalse) )],[refute_0_427,refute_0_529]) ).
cnf(refute_0_531,plain,
( eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))) != bfalse
| sat_comm(suc(zero),double(suc(zero))) != eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero)))
| sat_comm(suc(zero),double(suc(zero))) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(sat_comm(suc(zero),double(suc(zero))),eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero)))) ),[1],$fot(bfalse)]]) ).
cnf(refute_0_532,plain,
( sat_comm(suc(zero),double(suc(zero))) != eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero)))
| sat_comm(suc(zero),double(suc(zero))) = bfalse ),
inference(resolve,[$cnf( $equal(eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero))),bfalse) )],[refute_0_530,refute_0_531]) ).
cnf(refute_0_533,plain,
sat_comm(suc(zero),double(suc(zero))) = bfalse,
inference(resolve,[$cnf( $equal(sat_comm(suc(zero),double(suc(zero))),eq(suc(double(double(suc(zero)))),x(double(suc(zero)),suc(zero)))) )],[refute_0_344,refute_0_532]) ).
cnf(refute_0_534,plain,
( eq2(bfalse,bfalse) != btrue
| sat_comm(suc(zero),double(suc(zero))) != bfalse
| eq2(sat_comm(suc(zero),double(suc(zero))),bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( ~ $equal(eq2(sat_comm(suc(zero),double(suc(zero))),bfalse),btrue) ),[0,0],$fot(bfalse)]]) ).
cnf(refute_0_535,plain,
( eq2(bfalse,bfalse) != btrue
| eq2(sat_comm(suc(zero),double(suc(zero))),bfalse) = btrue ),
inference(resolve,[$cnf( $equal(sat_comm(suc(zero),double(suc(zero))),bfalse) )],[refute_0_533,refute_0_534]) ).
cnf(refute_0_536,plain,
eq2(bfalse,bfalse) != btrue,
inference(resolve,[$cnf( $equal(eq2(sat_comm(suc(zero),double(suc(zero))),bfalse),btrue) )],[refute_0_535,refute_0_0]) ).
cnf(refute_0_537,plain,
eq2(bfalse,bfalse) = btrue,
inference(subst,[],[axiom_029:[bind(X,$fot(bfalse))]]) ).
cnf(refute_0_538,plain,
( btrue != btrue
| eq2(bfalse,bfalse) != btrue
| eq2(bfalse,bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(eq2(bfalse,bfalse),btrue) ),[1],$fot(btrue)]]) ).
cnf(refute_0_539,plain,
( btrue != btrue
| eq2(bfalse,bfalse) = btrue ),
inference(resolve,[$cnf( $equal(eq2(bfalse,bfalse),btrue) )],[refute_0_537,refute_0_538]) ).
cnf(refute_0_540,plain,
btrue != btrue,
inference(resolve,[$cnf( $equal(eq2(bfalse,bfalse),btrue) )],[refute_0_539,refute_0_536]) ).
cnf(refute_0_541,plain,
btrue = btrue,
introduced(tautology,[refl,[$fot(btrue)]]) ).
cnf(refute_0_542,plain,
$false,
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_541,refute_0_540]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX217-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : metis --show proof --show saturation %s
% 0.15/0.34 % Computer : n008.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue May 5 12:15:58 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 1.03/1.20 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.03/1.20
% 1.03/1.20 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 1.03/1.26
%------------------------------------------------------------------------------