Metis---2.4.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : SWX221-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n028.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:36 PM UTC 2026

% Result   : Unsatisfiable 27.86s 28.11s
% Output   : CNFRefutation 27.96s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   26
%            Number of leaves      :   77
% Syntax   : Number of clauses     :  239 ( 128 unt;   0 nHn; 139 RR)
%            Number of literals    :  405 ( 404 equ; 170 neg)
%            Maximal clause size   :    3 (   1 avg)
%            Maximal term depth    :   11 (   2 avg)
%            Number of predicates  :    3 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :   23 (  23 usr;   7 con; 0-4 aty)
%            Number of variables   :  422 (  43 sgn)

% Comments : 
%------------------------------------------------------------------------------
cnf(axiom_001,axiom,
    aux(X,Z,X3,just(Tx3)) = eq(Tx3,Z) ).

cnf(axiom_002,axiom,
    notb(btrue) = bfalse ).

cnf(axiom_005,axiom,
    index(cons(Z,Xs),zero) = just(Z) ).

cnf(axiom_006,axiom,
    index(cons(Z,Xs),suc(N)) = index(Xs,N) ).

cnf(axiom_007,axiom,
    andb(btrue,Q) = Q ).

cnf(axiom_010,axiom,
    nf(app(app(X,X3,X4),Z,X2)) = andb(nf(app(X,X3,X4)),nf(Z)) ).

cnf(axiom_011,axiom,
    nf(app(var(X),Z,X2)) = andb(nf(var(X)),nf(Z)) ).

cnf(axiom_012,axiom,
    nf(lam(E)) = nf(E) ).

cnf(axiom_013,axiom,
    nf(var(X4)) = btrue ).

cnf(axiom_014,axiom,
    tc(X,app(F,X2,Tx),Z) = andb(tc(X,F,arr(Tx,Z)),tc(X,X2,Tx)) ).

cnf(axiom_015,axiom,
    tc(X,lam(E),arr(Tx2,T1)) = tc(cons(Tx2,X),E,T1) ).

cnf(axiom_019,axiom,
    tc(X,var(X3),Z) = aux(X,Z,X3,index(X,X3)) ).

cnf(axiom_020,axiom,
    sat_synth_nf_flip(X) = notb(andb(nf(X),tc(nil,X,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) ).

cnf(axiom_033,axiom,
    ( eq(X,Z) != btrue
    | eq(arr(X,Y),arr(Z,X2)) = eq(Y,X2) ) ).

cnf(axiom_051,axiom,
    eq(X,X) = btrue ).

cnf(axiom_054,axiom,
    eq4(X,X) = btrue ).

cnf(goal,negated_conjecture,
    eq4(sat_synth_nf_flip(X),bfalse) != btrue ).

cnf(refute_0_0,plain,
    eq4(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),bfalse) != btrue,
    inference(subst,[],[goal:[bind(X,$fot(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))))]]) ).

cnf(refute_0_1,plain,
    sat_synth_nf_flip(lam(E)) = notb(andb(nf(lam(E)),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))),
    inference(subst,[],[axiom_020:[bind(X,$fot(lam(E)))]]) ).

cnf(refute_0_2,plain,
    ( nf(lam(E)) != nf(E)
    | sat_synth_nf_flip(lam(E)) != notb(andb(nf(lam(E)),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))))
    | sat_synth_nf_flip(lam(E)) = notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) ),
    introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_flip(lam(E)),notb(andb(nf(lam(E)),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))))) ),[1,0,0],$fot(nf(E))]]) ).

cnf(refute_0_3,plain,
    ( sat_synth_nf_flip(lam(E)) != notb(andb(nf(lam(E)),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))))
    | sat_synth_nf_flip(lam(E)) = notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) ),
    inference(resolve,[$cnf( $equal(nf(lam(E)),nf(E)) )],[axiom_012,refute_0_2]) ).

cnf(refute_0_4,plain,
    sat_synth_nf_flip(lam(E)) = notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))),
    inference(resolve,[$cnf( $equal(sat_synth_nf_flip(lam(E)),notb(andb(nf(lam(E)),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))))) )],[refute_0_1,refute_0_3]) ).

cnf(refute_0_5,plain,
    tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))) = tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c))),
    inference(subst,[],[axiom_015:[bind(T1,$fot(arr(b,arr(a,c)))),bind(Tx2,$fot(arr(a,arr(b,c)))),bind(X,$fot(nil))]]) ).

cnf(refute_0_6,plain,
    andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))) = andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))),
    introduced(tautology,[refl,[$fot(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))))]]) ).

cnf(refute_0_7,plain,
    ( andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))) != andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))
    | tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))) != tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c)))
    | andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))) = andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c)))) ),
    introduced(tautology,[equality,[$cnf( $equal(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))),andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) ),[1,1],$fot(tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c))))]]) ).

cnf(refute_0_8,plain,
    ( tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))) != tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c)))
    | andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))) = andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c)))) ),
    inference(resolve,[$cnf( $equal(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))),andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) )],[refute_0_6,refute_0_7]) ).

cnf(refute_0_9,plain,
    andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))) = andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c)))),
    inference(resolve,[$cnf( $equal(tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c)))) )],[refute_0_5,refute_0_8]) ).

cnf(refute_0_10,plain,
    notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) = notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))),
    introduced(tautology,[refl,[$fot(notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))))]]) ).

cnf(refute_0_11,plain,
    ( andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))) != andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c))))
    | notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) != notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))))
    | notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) = notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c))))) ),
    introduced(tautology,[equality,[$cnf( $equal(notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))),notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))))) ),[1,0],$fot(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c)))))]]) ).

cnf(refute_0_12,plain,
    ( andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))) != andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c))))
    | notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) = notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c))))) ),
    inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))),notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))))) )],[refute_0_10,refute_0_11]) ).

cnf(refute_0_13,plain,
    notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) = notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c))))),
    inference(resolve,[$cnf( $equal(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))),andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c))))) )],[refute_0_9,refute_0_12]) ).

cnf(refute_0_14,plain,
    ( notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) != notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c)))))
    | sat_synth_nf_flip(lam(E)) != notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))))
    | sat_synth_nf_flip(lam(E)) = notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c))))) ),
    introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_flip(lam(E)),notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))))) ),[1],$fot(notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c))))))]]) ).

cnf(refute_0_15,plain,
    ( sat_synth_nf_flip(lam(E)) != notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))))
    | sat_synth_nf_flip(lam(E)) = notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c))))) ),
    inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))),notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c)))))) )],[refute_0_13,refute_0_14]) ).

cnf(refute_0_16,plain,
    sat_synth_nf_flip(lam(E)) = notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),E,arr(b,arr(a,c))))),
    inference(resolve,[$cnf( $equal(sat_synth_nf_flip(lam(E)),notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))))) )],[refute_0_4,refute_0_15]) ).

cnf(refute_0_17,plain,
    sat_synth_nf_flip(lam(lam(E))) = notb(andb(nf(lam(E)),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))),
    inference(subst,[],[refute_0_16:[bind(E,$fot(lam(E)))]]) ).

cnf(refute_0_18,plain,
    ( nf(lam(E)) != nf(E)
    | sat_synth_nf_flip(lam(lam(E))) != notb(andb(nf(lam(E)),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))))
    | sat_synth_nf_flip(lam(lam(E))) = notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))) ),
    introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_flip(lam(lam(E))),notb(andb(nf(lam(E)),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))))) ),[1,0,0],$fot(nf(E))]]) ).

cnf(refute_0_19,plain,
    ( sat_synth_nf_flip(lam(lam(E))) != notb(andb(nf(lam(E)),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))))
    | sat_synth_nf_flip(lam(lam(E))) = notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))) ),
    inference(resolve,[$cnf( $equal(nf(lam(E)),nf(E)) )],[axiom_012,refute_0_18]) ).

cnf(refute_0_20,plain,
    sat_synth_nf_flip(lam(lam(E))) = notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))),
    inference(resolve,[$cnf( $equal(sat_synth_nf_flip(lam(lam(E))),notb(andb(nf(lam(E)),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))))) )],[refute_0_17,refute_0_19]) ).

cnf(refute_0_21,plain,
    tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))) = tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)),
    inference(subst,[],[axiom_015:[bind(T1,$fot(arr(a,c))),bind(Tx2,$fot(b)),bind(X,$fot(cons(arr(a,arr(b,c)),nil)))]]) ).

cnf(refute_0_22,plain,
    andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))) = andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))),
    introduced(tautology,[refl,[$fot(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))))]]) ).

cnf(refute_0_23,plain,
    ( andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))) != andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))
    | tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))) != tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))
    | andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))) = andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))) ),
    introduced(tautology,[equality,[$cnf( $equal(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))),andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))) ),[1,1],$fot(tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)))]]) ).

cnf(refute_0_24,plain,
    ( tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))) != tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))
    | andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))) = andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))) ),
    inference(resolve,[$cnf( $equal(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))),andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))) )],[refute_0_22,refute_0_23]) ).

cnf(refute_0_25,plain,
    andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))) = andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))),
    inference(resolve,[$cnf( $equal(tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))) )],[refute_0_21,refute_0_24]) ).

cnf(refute_0_26,plain,
    notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))) = notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))),
    introduced(tautology,[refl,[$fot(notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))))]]) ).

cnf(refute_0_27,plain,
    ( andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))) != andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)))
    | notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))) != notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))))
    | notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))) = notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)))) ),
    introduced(tautology,[equality,[$cnf( $equal(notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))),notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))))) ),[1,0],$fot(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))))]]) ).

cnf(refute_0_28,plain,
    ( andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))) != andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)))
    | notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))) = notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)))) ),
    inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))),notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))))) )],[refute_0_26,refute_0_27]) ).

cnf(refute_0_29,plain,
    notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))) = notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)))),
    inference(resolve,[$cnf( $equal(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))),andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)))) )],[refute_0_25,refute_0_28]) ).

cnf(refute_0_30,plain,
    ( notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))) != notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))))
    | sat_synth_nf_flip(lam(lam(E))) != notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))))
    | sat_synth_nf_flip(lam(lam(E))) = notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)))) ),
    introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_flip(lam(lam(E))),notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))))) ),[1],$fot(notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)))))]]) ).

cnf(refute_0_31,plain,
    ( sat_synth_nf_flip(lam(lam(E))) != notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))))
    | sat_synth_nf_flip(lam(lam(E))) = notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)))) ),
    inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))),notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))))) )],[refute_0_29,refute_0_30]) ).

cnf(refute_0_32,plain,
    sat_synth_nf_flip(lam(lam(E))) = notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)))),
    inference(resolve,[$cnf( $equal(sat_synth_nf_flip(lam(lam(E))),notb(andb(nf(E),tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))))) )],[refute_0_20,refute_0_31]) ).

cnf(refute_0_33,plain,
    sat_synth_nf_flip(lam(lam(lam(E)))) = notb(andb(nf(lam(E)),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))),
    inference(subst,[],[refute_0_32:[bind(E,$fot(lam(E)))]]) ).

cnf(refute_0_34,plain,
    ( nf(lam(E)) != nf(E)
    | sat_synth_nf_flip(lam(lam(lam(E)))) != notb(andb(nf(lam(E)),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))))
    | sat_synth_nf_flip(lam(lam(lam(E)))) = notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))) ),
    introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(E)))),notb(andb(nf(lam(E)),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))))) ),[1,0,0],$fot(nf(E))]]) ).

cnf(refute_0_35,plain,
    ( sat_synth_nf_flip(lam(lam(lam(E)))) != notb(andb(nf(lam(E)),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))))
    | sat_synth_nf_flip(lam(lam(lam(E)))) = notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))) ),
    inference(resolve,[$cnf( $equal(nf(lam(E)),nf(E)) )],[axiom_012,refute_0_34]) ).

cnf(refute_0_36,plain,
    sat_synth_nf_flip(lam(lam(lam(E)))) = notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))),
    inference(resolve,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(E)))),notb(andb(nf(lam(E)),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))))) )],[refute_0_33,refute_0_35]) ).

cnf(refute_0_37,plain,
    tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)) = tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c),
    inference(subst,[],[axiom_015:[bind(T1,$fot(c)),bind(Tx2,$fot(a)),bind(X,$fot(cons(b,cons(arr(a,arr(b,c)),nil))))]]) ).

cnf(refute_0_38,plain,
    andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))) = andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))),
    introduced(tautology,[refl,[$fot(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))))]]) ).

cnf(refute_0_39,plain,
    ( andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))) != andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))
    | tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)) != tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)
    | andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))) = andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)) ),
    introduced(tautology,[equality,[$cnf( $equal(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))),andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))) ),[1,1],$fot(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c))]]) ).

cnf(refute_0_40,plain,
    ( tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)) != tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)
    | andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))) = andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)) ),
    inference(resolve,[$cnf( $equal(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))),andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))) )],[refute_0_38,refute_0_39]) ).

cnf(refute_0_41,plain,
    andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))) = andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)),
    inference(resolve,[$cnf( $equal(tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)) )],[refute_0_37,refute_0_40]) ).

cnf(refute_0_42,plain,
    notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))) = notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))),
    introduced(tautology,[refl,[$fot(notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))))]]) ).

cnf(refute_0_43,plain,
    ( andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))) != andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c))
    | notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))) != notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))))
    | notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))) = notb(andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c))) ),
    introduced(tautology,[equality,[$cnf( $equal(notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))),notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))))) ),[1,0],$fot(andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)))]]) ).

cnf(refute_0_44,plain,
    ( andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))) != andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c))
    | notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))) = notb(andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c))) ),
    inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))),notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))))) )],[refute_0_42,refute_0_43]) ).

cnf(refute_0_45,plain,
    notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))) = notb(andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c))),
    inference(resolve,[$cnf( $equal(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))),andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c))) )],[refute_0_41,refute_0_44]) ).

cnf(refute_0_46,plain,
    ( notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))) != notb(andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)))
    | sat_synth_nf_flip(lam(lam(lam(E)))) != notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))))
    | sat_synth_nf_flip(lam(lam(lam(E)))) = notb(andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c))) ),
    introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(E)))),notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))))) ),[1],$fot(notb(andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c))))]]) ).

cnf(refute_0_47,plain,
    ( sat_synth_nf_flip(lam(lam(lam(E)))) != notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))))
    | sat_synth_nf_flip(lam(lam(lam(E)))) = notb(andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c))) ),
    inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))),notb(andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)))) )],[refute_0_45,refute_0_46]) ).

cnf(refute_0_48,plain,
    sat_synth_nf_flip(lam(lam(lam(E)))) = notb(andb(nf(E),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c))),
    inference(resolve,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(E)))),notb(andb(nf(E),tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))))) )],[refute_0_36,refute_0_47]) ).

cnf(refute_0_49,plain,
    sat_synth_nf_flip(lam(lam(lam(app(X_2408,var(suc(zero)),b))))) = notb(andb(nf(app(X_2408,var(suc(zero)),b)),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_2408,var(suc(zero)),b),c))),
    inference(subst,[],[refute_0_48:[bind(E,$fot(app(X_2408,var(suc(zero)),b)))]]) ).

cnf(refute_0_50,plain,
    tc(cons(X_127,cons(Z,Xs)),app(X_181,var(suc(zero)),X_182),X_185) = andb(tc(cons(X_127,cons(Z,Xs)),X_181,arr(X_182,X_185)),tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_182)),
    inference(subst,[],[axiom_014:[bind(F,$fot(X_181)),bind(Tx,$fot(X_182)),bind(X,$fot(cons(X_127,cons(Z,Xs)))),bind(X2,$fot(var(suc(zero)))),bind(Z,$fot(X_185))]]) ).

cnf(refute_0_51,plain,
    tc(cons(Z,Xs),var(suc(N)),X_78) = aux(cons(Z,Xs),X_78,suc(N),index(cons(Z,Xs),suc(N))),
    inference(subst,[],[axiom_019:[bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(suc(N))),bind(Z,$fot(X_78))]]) ).

cnf(refute_0_52,plain,
    ( index(cons(Z,Xs),suc(N)) != index(Xs,N)
    | tc(cons(Z,Xs),var(suc(N)),X_78) != aux(cons(Z,Xs),X_78,suc(N),index(cons(Z,Xs),suc(N)))
    | tc(cons(Z,Xs),var(suc(N)),X_78) = aux(cons(Z,Xs),X_78,suc(N),index(Xs,N)) ),
    introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),var(suc(N)),X_78),aux(cons(Z,Xs),X_78,suc(N),index(cons(Z,Xs),suc(N)))) ),[1,3],$fot(index(Xs,N))]]) ).

cnf(refute_0_53,plain,
    ( tc(cons(Z,Xs),var(suc(N)),X_78) != aux(cons(Z,Xs),X_78,suc(N),index(cons(Z,Xs),suc(N)))
    | tc(cons(Z,Xs),var(suc(N)),X_78) = aux(cons(Z,Xs),X_78,suc(N),index(Xs,N)) ),
    inference(resolve,[$cnf( $equal(index(cons(Z,Xs),suc(N)),index(Xs,N)) )],[axiom_006,refute_0_52]) ).

cnf(refute_0_54,plain,
    tc(cons(Z,Xs),var(suc(N)),X_78) = aux(cons(Z,Xs),X_78,suc(N),index(Xs,N)),
    inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(suc(N)),X_78),aux(cons(Z,Xs),X_78,suc(N),index(cons(Z,Xs),suc(N)))) )],[refute_0_51,refute_0_53]) ).

cnf(refute_0_55,plain,
    tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128) = aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),index(cons(Z,Xs),zero)),
    inference(subst,[],[refute_0_54:[bind(N,$fot(zero)),bind(Xs,$fot(cons(Z,Xs))),bind(Z,$fot(X_127)),bind(X_78,$fot(X_128))]]) ).

cnf(refute_0_56,plain,
    ( index(cons(Z,Xs),zero) != just(Z)
    | tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128) != aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),index(cons(Z,Xs),zero))
    | tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128) = aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),just(Z)) ),
    introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128),aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),index(cons(Z,Xs),zero))) ),[1,3],$fot(just(Z))]]) ).

cnf(refute_0_57,plain,
    ( tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128) != aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),index(cons(Z,Xs),zero))
    | tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128) = aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),just(Z)) ),
    inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(Z)) )],[axiom_005,refute_0_56]) ).

cnf(refute_0_58,plain,
    tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128) = aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),just(Z)),
    inference(resolve,[$cnf( $equal(tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128),aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),index(cons(Z,Xs),zero))) )],[refute_0_55,refute_0_57]) ).

cnf(refute_0_59,plain,
    aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),just(Z)) = eq(Z,X_128),
    inference(subst,[],[axiom_001:[bind(Tx3,$fot(Z)),bind(X,$fot(cons(X_127,cons(Z,Xs)))),bind(X3,$fot(suc(zero))),bind(Z,$fot(X_128))]]) ).

cnf(refute_0_60,plain,
    ( aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),just(Z)) != eq(Z,X_128)
    | tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128) != aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),just(Z))
    | tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128) = eq(Z,X_128) ),
    introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128),aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),just(Z))) ),[1],$fot(eq(Z,X_128))]]) ).

cnf(refute_0_61,plain,
    ( tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128) != aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),just(Z))
    | tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128) = eq(Z,X_128) ),
    inference(resolve,[$cnf( $equal(aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),just(Z)),eq(Z,X_128)) )],[refute_0_59,refute_0_60]) ).

cnf(refute_0_62,plain,
    tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128) = eq(Z,X_128),
    inference(resolve,[$cnf( $equal(tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_128),aux(cons(X_127,cons(Z,Xs)),X_128,suc(zero),just(Z))) )],[refute_0_58,refute_0_61]) ).

cnf(refute_0_63,plain,
    tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_182) = eq(Z,X_182),
    inference(subst,[],[refute_0_62:[bind(X_128,$fot(X_182))]]) ).

cnf(refute_0_64,plain,
    ( tc(cons(X_127,cons(Z,Xs)),app(X_181,var(suc(zero)),X_182),X_185) != andb(tc(cons(X_127,cons(Z,Xs)),X_181,arr(X_182,X_185)),tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_182))
    | tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_182) != eq(Z,X_182)
    | tc(cons(X_127,cons(Z,Xs)),app(X_181,var(suc(zero)),X_182),X_185) = andb(tc(cons(X_127,cons(Z,Xs)),X_181,arr(X_182,X_185)),eq(Z,X_182)) ),
    introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_127,cons(Z,Xs)),app(X_181,var(suc(zero)),X_182),X_185),andb(tc(cons(X_127,cons(Z,Xs)),X_181,arr(X_182,X_185)),tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_182))) ),[1,1],$fot(eq(Z,X_182))]]) ).

cnf(refute_0_65,plain,
    ( tc(cons(X_127,cons(Z,Xs)),app(X_181,var(suc(zero)),X_182),X_185) != andb(tc(cons(X_127,cons(Z,Xs)),X_181,arr(X_182,X_185)),tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_182))
    | tc(cons(X_127,cons(Z,Xs)),app(X_181,var(suc(zero)),X_182),X_185) = andb(tc(cons(X_127,cons(Z,Xs)),X_181,arr(X_182,X_185)),eq(Z,X_182)) ),
    inference(resolve,[$cnf( $equal(tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_182),eq(Z,X_182)) )],[refute_0_63,refute_0_64]) ).

cnf(refute_0_66,plain,
    tc(cons(X_127,cons(Z,Xs)),app(X_181,var(suc(zero)),X_182),X_185) = andb(tc(cons(X_127,cons(Z,Xs)),X_181,arr(X_182,X_185)),eq(Z,X_182)),
    inference(resolve,[$cnf( $equal(tc(cons(X_127,cons(Z,Xs)),app(X_181,var(suc(zero)),X_182),X_185),andb(tc(cons(X_127,cons(Z,Xs)),X_181,arr(X_182,X_185)),tc(cons(X_127,cons(Z,Xs)),var(suc(zero)),X_182))) )],[refute_0_50,refute_0_65]) ).

cnf(refute_0_67,plain,
    tc(cons(X_1209,cons(X_1211,X_1207)),app(X_1210,var(suc(zero)),X_1211),X_1212) = andb(tc(cons(X_1209,cons(X_1211,X_1207)),X_1210,arr(X_1211,X_1212)),eq(X_1211,X_1211)),
    inference(subst,[],[refute_0_66:[bind(Xs,$fot(X_1207)),bind(Z,$fot(X_1211)),bind(X_127,$fot(X_1209)),bind(X_181,$fot(X_1210)),bind(X_182,$fot(X_1211)),bind(X_185,$fot(X_1212))]]) ).

cnf(refute_0_68,plain,
    eq(X_1211,X_1211) = btrue,
    inference(subst,[],[axiom_051:[bind(X,$fot(X_1211))]]) ).

cnf(refute_0_69,plain,
    ( eq(X_1211,X_1211) != btrue
    | tc(cons(X_1209,cons(X_1211,X_1207)),app(X_1210,var(suc(zero)),X_1211),X_1212) != andb(tc(cons(X_1209,cons(X_1211,X_1207)),X_1210,arr(X_1211,X_1212)),eq(X_1211,X_1211))
    | tc(cons(X_1209,cons(X_1211,X_1207)),app(X_1210,var(suc(zero)),X_1211),X_1212) = andb(tc(cons(X_1209,cons(X_1211,X_1207)),X_1210,arr(X_1211,X_1212)),btrue) ),
    introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_1209,cons(X_1211,X_1207)),app(X_1210,var(suc(zero)),X_1211),X_1212),andb(tc(cons(X_1209,cons(X_1211,X_1207)),X_1210,arr(X_1211,X_1212)),eq(X_1211,X_1211))) ),[1,1],$fot(btrue)]]) ).

cnf(refute_0_70,plain,
    ( tc(cons(X_1209,cons(X_1211,X_1207)),app(X_1210,var(suc(zero)),X_1211),X_1212) != andb(tc(cons(X_1209,cons(X_1211,X_1207)),X_1210,arr(X_1211,X_1212)),eq(X_1211,X_1211))
    | tc(cons(X_1209,cons(X_1211,X_1207)),app(X_1210,var(suc(zero)),X_1211),X_1212) = andb(tc(cons(X_1209,cons(X_1211,X_1207)),X_1210,arr(X_1211,X_1212)),btrue) ),
    inference(resolve,[$cnf( $equal(eq(X_1211,X_1211),btrue) )],[refute_0_68,refute_0_69]) ).

cnf(refute_0_71,plain,
    tc(cons(X_1209,cons(X_1211,X_1207)),app(X_1210,var(suc(zero)),X_1211),X_1212) = andb(tc(cons(X_1209,cons(X_1211,X_1207)),X_1210,arr(X_1211,X_1212)),btrue),
    inference(resolve,[$cnf( $equal(tc(cons(X_1209,cons(X_1211,X_1207)),app(X_1210,var(suc(zero)),X_1211),X_1212),andb(tc(cons(X_1209,cons(X_1211,X_1207)),X_1210,arr(X_1211,X_1212)),eq(X_1211,X_1211))) )],[refute_0_67,refute_0_70]) ).

cnf(refute_0_72,plain,
    tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_2408,var(suc(zero)),b),c) = andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_2408,arr(b,c)),btrue),
    inference(subst,[],[refute_0_71:[bind(X_1207,$fot(cons(arr(a,arr(b,c)),nil))),bind(X_1209,$fot(a)),bind(X_1210,$fot(X_2408)),bind(X_1211,$fot(b)),bind(X_1212,$fot(c))]]) ).

cnf(refute_0_73,plain,
    ( sat_synth_nf_flip(lam(lam(lam(app(X_2408,var(suc(zero)),b))))) != notb(andb(nf(app(X_2408,var(suc(zero)),b)),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_2408,var(suc(zero)),b),c)))
    | tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_2408,var(suc(zero)),b),c) != andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_2408,arr(b,c)),btrue)
    | sat_synth_nf_flip(lam(lam(lam(app(X_2408,var(suc(zero)),b))))) = notb(andb(nf(app(X_2408,var(suc(zero)),b)),andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_2408,arr(b,c)),btrue))) ),
    introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(app(X_2408,var(suc(zero)),b))))),notb(andb(nf(app(X_2408,var(suc(zero)),b)),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_2408,var(suc(zero)),b),c)))) ),[1,0,1],$fot(andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_2408,arr(b,c)),btrue))]]) ).

cnf(refute_0_74,plain,
    ( sat_synth_nf_flip(lam(lam(lam(app(X_2408,var(suc(zero)),b))))) != notb(andb(nf(app(X_2408,var(suc(zero)),b)),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_2408,var(suc(zero)),b),c)))
    | sat_synth_nf_flip(lam(lam(lam(app(X_2408,var(suc(zero)),b))))) = notb(andb(nf(app(X_2408,var(suc(zero)),b)),andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_2408,arr(b,c)),btrue))) ),
    inference(resolve,[$cnf( $equal(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_2408,var(suc(zero)),b),c),andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_2408,arr(b,c)),btrue)) )],[refute_0_72,refute_0_73]) ).

cnf(refute_0_75,plain,
    sat_synth_nf_flip(lam(lam(lam(app(X_2408,var(suc(zero)),b))))) = notb(andb(nf(app(X_2408,var(suc(zero)),b)),andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_2408,arr(b,c)),btrue))),
    inference(resolve,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(app(X_2408,var(suc(zero)),b))))),notb(andb(nf(app(X_2408,var(suc(zero)),b)),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_2408,var(suc(zero)),b),c)))) )],[refute_0_49,refute_0_74]) ).

cnf(refute_0_76,plain,
    sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))) = notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_3575),arr(b,c)),btrue))),
    inference(subst,[],[refute_0_75:[bind(X_2408,$fot(app(var(suc(suc(zero))),var(zero),X_3575)))]]) ).

cnf(refute_0_77,plain,
    tc(cons(Z,Xs),app(X_181,var(zero),X_182),X_185) = andb(tc(cons(Z,Xs),X_181,arr(X_182,X_185)),tc(cons(Z,Xs),var(zero),X_182)),
    inference(subst,[],[axiom_014:[bind(F,$fot(X_181)),bind(Tx,$fot(X_182)),bind(X,$fot(cons(Z,Xs))),bind(X2,$fot(var(zero))),bind(Z,$fot(X_185))]]) ).

cnf(refute_0_78,plain,
    tc(cons(Z,Xs),var(zero),X_78) = aux(cons(Z,Xs),X_78,zero,index(cons(Z,Xs),zero)),
    inference(subst,[],[axiom_019:[bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(zero)),bind(Z,$fot(X_78))]]) ).

cnf(refute_0_79,plain,
    ( index(cons(Z,Xs),zero) != just(Z)
    | tc(cons(Z,Xs),var(zero),X_78) != aux(cons(Z,Xs),X_78,zero,index(cons(Z,Xs),zero))
    | tc(cons(Z,Xs),var(zero),X_78) = aux(cons(Z,Xs),X_78,zero,just(Z)) ),
    introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_78),aux(cons(Z,Xs),X_78,zero,index(cons(Z,Xs),zero))) ),[1,3],$fot(just(Z))]]) ).

cnf(refute_0_80,plain,
    ( tc(cons(Z,Xs),var(zero),X_78) != aux(cons(Z,Xs),X_78,zero,index(cons(Z,Xs),zero))
    | tc(cons(Z,Xs),var(zero),X_78) = aux(cons(Z,Xs),X_78,zero,just(Z)) ),
    inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(Z)) )],[axiom_005,refute_0_79]) ).

cnf(refute_0_81,plain,
    tc(cons(Z,Xs),var(zero),X_78) = aux(cons(Z,Xs),X_78,zero,just(Z)),
    inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_78),aux(cons(Z,Xs),X_78,zero,index(cons(Z,Xs),zero))) )],[refute_0_78,refute_0_80]) ).

cnf(refute_0_82,plain,
    aux(cons(Z,Xs),X_78,zero,just(Z)) = eq(Z,X_78),
    inference(subst,[],[axiom_001:[bind(Tx3,$fot(Z)),bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(zero)),bind(Z,$fot(X_78))]]) ).

cnf(refute_0_83,plain,
    ( aux(cons(Z,Xs),X_78,zero,just(Z)) != eq(Z,X_78)
    | tc(cons(Z,Xs),var(zero),X_78) != aux(cons(Z,Xs),X_78,zero,just(Z))
    | tc(cons(Z,Xs),var(zero),X_78) = eq(Z,X_78) ),
    introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_78),aux(cons(Z,Xs),X_78,zero,just(Z))) ),[1],$fot(eq(Z,X_78))]]) ).

cnf(refute_0_84,plain,
    ( tc(cons(Z,Xs),var(zero),X_78) != aux(cons(Z,Xs),X_78,zero,just(Z))
    | tc(cons(Z,Xs),var(zero),X_78) = eq(Z,X_78) ),
    inference(resolve,[$cnf( $equal(aux(cons(Z,Xs),X_78,zero,just(Z)),eq(Z,X_78)) )],[refute_0_82,refute_0_83]) ).

cnf(refute_0_85,plain,
    tc(cons(Z,Xs),var(zero),X_78) = eq(Z,X_78),
    inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_78),aux(cons(Z,Xs),X_78,zero,just(Z))) )],[refute_0_81,refute_0_84]) ).

cnf(refute_0_86,plain,
    tc(cons(Z,Xs),var(zero),X_182) = eq(Z,X_182),
    inference(subst,[],[refute_0_85:[bind(X_78,$fot(X_182))]]) ).

cnf(refute_0_87,plain,
    ( tc(cons(Z,Xs),app(X_181,var(zero),X_182),X_185) != andb(tc(cons(Z,Xs),X_181,arr(X_182,X_185)),tc(cons(Z,Xs),var(zero),X_182))
    | tc(cons(Z,Xs),var(zero),X_182) != eq(Z,X_182)
    | tc(cons(Z,Xs),app(X_181,var(zero),X_182),X_185) = andb(tc(cons(Z,Xs),X_181,arr(X_182,X_185)),eq(Z,X_182)) ),
    introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),app(X_181,var(zero),X_182),X_185),andb(tc(cons(Z,Xs),X_181,arr(X_182,X_185)),tc(cons(Z,Xs),var(zero),X_182))) ),[1,1],$fot(eq(Z,X_182))]]) ).

cnf(refute_0_88,plain,
    ( tc(cons(Z,Xs),app(X_181,var(zero),X_182),X_185) != andb(tc(cons(Z,Xs),X_181,arr(X_182,X_185)),tc(cons(Z,Xs),var(zero),X_182))
    | tc(cons(Z,Xs),app(X_181,var(zero),X_182),X_185) = andb(tc(cons(Z,Xs),X_181,arr(X_182,X_185)),eq(Z,X_182)) ),
    inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_182),eq(Z,X_182)) )],[refute_0_86,refute_0_87]) ).

cnf(refute_0_89,plain,
    tc(cons(Z,Xs),app(X_181,var(zero),X_182),X_185) = andb(tc(cons(Z,Xs),X_181,arr(X_182,X_185)),eq(Z,X_182)),
    inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),app(X_181,var(zero),X_182),X_185),andb(tc(cons(Z,Xs),X_181,arr(X_182,X_185)),tc(cons(Z,Xs),var(zero),X_182))) )],[refute_0_77,refute_0_88]) ).

cnf(refute_0_90,plain,
    tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),app(var(suc(suc(zero))),var(zero),X_182),X_185) = andb(tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),var(suc(suc(zero))),arr(X_182,X_185)),eq(Z,X_182)),
    inference(subst,[],[refute_0_89:[bind(Xs,$fot(cons(X_1036,cons(X_1035,X_1034)))),bind(X_181,$fot(var(suc(suc(zero)))))]]) ).

cnf(refute_0_91,plain,
    tc(cons(X_127,cons(Z,Xs)),var(suc(suc(N))),X_128) = aux(cons(X_127,cons(Z,Xs)),X_128,suc(suc(N)),index(cons(Z,Xs),suc(N))),
    inference(subst,[],[refute_0_54:[bind(N,$fot(suc(N))),bind(Xs,$fot(cons(Z,Xs))),bind(Z,$fot(X_127)),bind(X_78,$fot(X_128))]]) ).

cnf(refute_0_92,plain,
    ( index(cons(Z,Xs),suc(N)) != index(Xs,N)
    | tc(cons(X_127,cons(Z,Xs)),var(suc(suc(N))),X_128) != aux(cons(X_127,cons(Z,Xs)),X_128,suc(suc(N)),index(cons(Z,Xs),suc(N)))
    | tc(cons(X_127,cons(Z,Xs)),var(suc(suc(N))),X_128) = aux(cons(X_127,cons(Z,Xs)),X_128,suc(suc(N)),index(Xs,N)) ),
    introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_127,cons(Z,Xs)),var(suc(suc(N))),X_128),aux(cons(X_127,cons(Z,Xs)),X_128,suc(suc(N)),index(cons(Z,Xs),suc(N)))) ),[1,3],$fot(index(Xs,N))]]) ).

cnf(refute_0_93,plain,
    ( tc(cons(X_127,cons(Z,Xs)),var(suc(suc(N))),X_128) != aux(cons(X_127,cons(Z,Xs)),X_128,suc(suc(N)),index(cons(Z,Xs),suc(N)))
    | tc(cons(X_127,cons(Z,Xs)),var(suc(suc(N))),X_128) = aux(cons(X_127,cons(Z,Xs)),X_128,suc(suc(N)),index(Xs,N)) ),
    inference(resolve,[$cnf( $equal(index(cons(Z,Xs),suc(N)),index(Xs,N)) )],[axiom_006,refute_0_92]) ).

cnf(refute_0_94,plain,
    tc(cons(X_127,cons(Z,Xs)),var(suc(suc(N))),X_128) = aux(cons(X_127,cons(Z,Xs)),X_128,suc(suc(N)),index(Xs,N)),
    inference(resolve,[$cnf( $equal(tc(cons(X_127,cons(Z,Xs)),var(suc(suc(N))),X_128),aux(cons(X_127,cons(Z,Xs)),X_128,suc(suc(N)),index(cons(Z,Xs),suc(N)))) )],[refute_0_91,refute_0_93]) ).

cnf(refute_0_95,plain,
    tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014) = aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),index(cons(Z,Xs),zero)),
    inference(subst,[],[refute_0_94:[bind(N,$fot(zero)),bind(Xs,$fot(cons(Z,Xs))),bind(Z,$fot(X_1012)),bind(X_127,$fot(X_1013)),bind(X_128,$fot(X_1014))]]) ).

cnf(refute_0_96,plain,
    ( index(cons(Z,Xs),zero) != just(Z)
    | tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014) != aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),index(cons(Z,Xs),zero))
    | tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014) = aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),just(Z)) ),
    introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014),aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),index(cons(Z,Xs),zero))) ),[1,3],$fot(just(Z))]]) ).

cnf(refute_0_97,plain,
    ( tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014) != aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),index(cons(Z,Xs),zero))
    | tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014) = aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),just(Z)) ),
    inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(Z)) )],[axiom_005,refute_0_96]) ).

cnf(refute_0_98,plain,
    tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014) = aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),just(Z)),
    inference(resolve,[$cnf( $equal(tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014),aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),index(cons(Z,Xs),zero))) )],[refute_0_95,refute_0_97]) ).

cnf(refute_0_99,plain,
    aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),just(Z)) = eq(Z,X_1014),
    inference(subst,[],[axiom_001:[bind(Tx3,$fot(Z)),bind(X,$fot(cons(X_1013,cons(X_1012,cons(Z,Xs))))),bind(X3,$fot(suc(suc(zero)))),bind(Z,$fot(X_1014))]]) ).

cnf(refute_0_100,plain,
    ( aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),just(Z)) != eq(Z,X_1014)
    | tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014) != aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),just(Z))
    | tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014) = eq(Z,X_1014) ),
    introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014),aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),just(Z))) ),[1],$fot(eq(Z,X_1014))]]) ).

cnf(refute_0_101,plain,
    ( tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014) != aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),just(Z))
    | tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014) = eq(Z,X_1014) ),
    inference(resolve,[$cnf( $equal(aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),just(Z)),eq(Z,X_1014)) )],[refute_0_99,refute_0_100]) ).

cnf(refute_0_102,plain,
    tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014) = eq(Z,X_1014),
    inference(resolve,[$cnf( $equal(tc(cons(X_1013,cons(X_1012,cons(Z,Xs))),var(suc(suc(zero))),X_1014),aux(cons(X_1013,cons(X_1012,cons(Z,Xs))),X_1014,suc(suc(zero)),just(Z))) )],[refute_0_98,refute_0_101]) ).

cnf(refute_0_103,plain,
    tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),var(suc(suc(zero))),arr(X_182,X_185)) = eq(X_1035,arr(X_182,X_185)),
    inference(subst,[],[refute_0_102:[bind(Xs,$fot(X_1034)),bind(Z,$fot(X_1035)),bind(X_1012,$fot(X_1036)),bind(X_1013,$fot(Z)),bind(X_1014,$fot(arr(X_182,X_185)))]]) ).

cnf(refute_0_104,plain,
    ( tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),app(var(suc(suc(zero))),var(zero),X_182),X_185) != andb(tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),var(suc(suc(zero))),arr(X_182,X_185)),eq(Z,X_182))
    | tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),var(suc(suc(zero))),arr(X_182,X_185)) != eq(X_1035,arr(X_182,X_185))
    | tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),app(var(suc(suc(zero))),var(zero),X_182),X_185) = andb(eq(X_1035,arr(X_182,X_185)),eq(Z,X_182)) ),
    introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),app(var(suc(suc(zero))),var(zero),X_182),X_185),andb(tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),var(suc(suc(zero))),arr(X_182,X_185)),eq(Z,X_182))) ),[1,0],$fot(eq(X_1035,arr(X_182,X_185)))]]) ).

cnf(refute_0_105,plain,
    ( tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),app(var(suc(suc(zero))),var(zero),X_182),X_185) != andb(tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),var(suc(suc(zero))),arr(X_182,X_185)),eq(Z,X_182))
    | tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),app(var(suc(suc(zero))),var(zero),X_182),X_185) = andb(eq(X_1035,arr(X_182,X_185)),eq(Z,X_182)) ),
    inference(resolve,[$cnf( $equal(tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),var(suc(suc(zero))),arr(X_182,X_185)),eq(X_1035,arr(X_182,X_185))) )],[refute_0_103,refute_0_104]) ).

cnf(refute_0_106,plain,
    tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),app(var(suc(suc(zero))),var(zero),X_182),X_185) = andb(eq(X_1035,arr(X_182,X_185)),eq(Z,X_182)),
    inference(resolve,[$cnf( $equal(tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),app(var(suc(suc(zero))),var(zero),X_182),X_185),andb(tc(cons(Z,cons(X_1036,cons(X_1035,X_1034))),var(suc(suc(zero))),arr(X_182,X_185)),eq(Z,X_182))) )],[refute_0_90,refute_0_105]) ).

cnf(refute_0_107,plain,
    tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_3575),arr(b,c)) = andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),
    inference(subst,[],[refute_0_106:[bind(Z,$fot(a)),bind(X_1034,$fot(nil)),bind(X_1035,$fot(arr(a,arr(b,c)))),bind(X_1036,$fot(b)),bind(X_182,$fot(X_3575)),bind(X_185,$fot(arr(b,c)))]]) ).

cnf(refute_0_108,plain,
    ( sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))) != notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_3575),arr(b,c)),btrue)))
    | tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_3575),arr(b,c)) != andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575))
    | sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))) = notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))) ),
    introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))),notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_3575),arr(b,c)),btrue)))) ),[1,0,1,0],$fot(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)))]]) ).

cnf(refute_0_109,plain,
    ( sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))) != notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_3575),arr(b,c)),btrue)))
    | sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))) = notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))) ),
    inference(resolve,[$cnf( $equal(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_3575),arr(b,c)),andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575))) )],[refute_0_107,refute_0_108]) ).

cnf(refute_0_110,plain,
    sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))) = notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))),
    inference(resolve,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))),notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_3575),arr(b,c)),btrue)))) )],[refute_0_76,refute_0_109]) ).

cnf(refute_0_111,plain,
    andb(btrue,andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) = andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue),
    inference(subst,[],[axiom_007:[bind(Q,$fot(andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))]]) ).

cnf(refute_0_112,plain,
    andb(btrue,btrue) = btrue,
    inference(subst,[],[axiom_007:[bind(Q,$fot(btrue))]]) ).

cnf(refute_0_113,plain,
    nf(var(suc(zero))) = btrue,
    inference(subst,[],[axiom_013:[bind(X4,$fot(suc(zero)))]]) ).

cnf(refute_0_114,plain,
    andb(btrue,nf(var(suc(zero)))) = andb(btrue,nf(var(suc(zero)))),
    introduced(tautology,[refl,[$fot(andb(btrue,nf(var(suc(zero)))))]]) ).

cnf(refute_0_115,plain,
    ( andb(btrue,nf(var(suc(zero)))) != andb(btrue,nf(var(suc(zero))))
    | nf(var(suc(zero))) != btrue
    | andb(btrue,nf(var(suc(zero)))) = andb(btrue,btrue) ),
    introduced(tautology,[equality,[$cnf( $equal(andb(btrue,nf(var(suc(zero)))),andb(btrue,nf(var(suc(zero))))) ),[1,1],$fot(btrue)]]) ).

cnf(refute_0_116,plain,
    ( nf(var(suc(zero))) != btrue
    | andb(btrue,nf(var(suc(zero)))) = andb(btrue,btrue) ),
    inference(resolve,[$cnf( $equal(andb(btrue,nf(var(suc(zero)))),andb(btrue,nf(var(suc(zero))))) )],[refute_0_114,refute_0_115]) ).

cnf(refute_0_117,plain,
    andb(btrue,nf(var(suc(zero)))) = andb(btrue,btrue),
    inference(resolve,[$cnf( $equal(nf(var(suc(zero))),btrue) )],[refute_0_113,refute_0_116]) ).

cnf(refute_0_118,plain,
    nf(var(zero)) = btrue,
    inference(subst,[],[axiom_013:[bind(X4,$fot(zero))]]) ).

cnf(refute_0_119,plain,
    andb(nf(var(zero)),nf(var(suc(zero)))) = andb(nf(var(zero)),nf(var(suc(zero)))),
    introduced(tautology,[refl,[$fot(andb(nf(var(zero)),nf(var(suc(zero)))))]]) ).

cnf(refute_0_120,plain,
    ( andb(nf(var(zero)),nf(var(suc(zero)))) != andb(nf(var(zero)),nf(var(suc(zero))))
    | nf(var(zero)) != btrue
    | andb(nf(var(zero)),nf(var(suc(zero)))) = andb(btrue,nf(var(suc(zero)))) ),
    introduced(tautology,[equality,[$cnf( $equal(andb(nf(var(zero)),nf(var(suc(zero)))),andb(nf(var(zero)),nf(var(suc(zero))))) ),[1,0],$fot(btrue)]]) ).

cnf(refute_0_121,plain,
    ( nf(var(zero)) != btrue
    | andb(nf(var(zero)),nf(var(suc(zero)))) = andb(btrue,nf(var(suc(zero)))) ),
    inference(resolve,[$cnf( $equal(andb(nf(var(zero)),nf(var(suc(zero)))),andb(nf(var(zero)),nf(var(suc(zero))))) )],[refute_0_119,refute_0_120]) ).

cnf(refute_0_122,plain,
    andb(nf(var(zero)),nf(var(suc(zero)))) = andb(btrue,nf(var(suc(zero)))),
    inference(resolve,[$cnf( $equal(nf(var(zero)),btrue) )],[refute_0_118,refute_0_121]) ).

cnf(refute_0_123,plain,
    X0 = X0,
    introduced(tautology,[refl,[$fot(X0)]]) ).

cnf(refute_0_124,plain,
    ( X0 != X0
    | X0 != Y0
    | Y0 = X0 ),
    introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).

cnf(refute_0_125,plain,
    ( X0 != Y0
    | Y0 = X0 ),
    inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_123,refute_0_124]) ).

cnf(refute_0_126,plain,
    ( Y0 != X0
    | Y0 != Z0
    | X0 = Z0 ),
    introduced(tautology,[equality,[$cnf( $equal(Y0,Z0) ),[0],$fot(X0)]]) ).

cnf(refute_0_127,plain,
    ( X0 != Y0
    | Y0 != Z0
    | X0 = Z0 ),
    inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_125,refute_0_126]) ).

cnf(refute_0_128,plain,
    ( andb(btrue,nf(var(suc(zero)))) != andb(btrue,btrue)
    | andb(nf(var(zero)),nf(var(suc(zero)))) != andb(btrue,nf(var(suc(zero))))
    | andb(nf(var(zero)),nf(var(suc(zero)))) = andb(btrue,btrue) ),
    inference(subst,[],[refute_0_127:[bind(X0,$fot(andb(nf(var(zero)),nf(var(suc(zero)))))),bind(Y0,$fot(andb(btrue,nf(var(suc(zero)))))),bind(Z0,$fot(andb(btrue,btrue)))]]) ).

cnf(refute_0_129,plain,
    ( andb(btrue,nf(var(suc(zero)))) != andb(btrue,btrue)
    | andb(nf(var(zero)),nf(var(suc(zero)))) = andb(btrue,btrue) ),
    inference(resolve,[$cnf( $equal(andb(nf(var(zero)),nf(var(suc(zero)))),andb(btrue,nf(var(suc(zero))))) )],[refute_0_122,refute_0_128]) ).

cnf(refute_0_130,plain,
    andb(nf(var(zero)),nf(var(suc(zero)))) = andb(btrue,btrue),
    inference(resolve,[$cnf( $equal(andb(btrue,nf(var(suc(zero)))),andb(btrue,btrue)) )],[refute_0_117,refute_0_129]) ).

cnf(refute_0_131,plain,
    ( andb(btrue,btrue) != btrue
    | andb(nf(var(zero)),nf(var(suc(zero)))) != andb(btrue,btrue)
    | andb(nf(var(zero)),nf(var(suc(zero)))) = btrue ),
    inference(subst,[],[refute_0_127:[bind(X0,$fot(andb(nf(var(zero)),nf(var(suc(zero)))))),bind(Y0,$fot(andb(btrue,btrue))),bind(Z0,$fot(btrue))]]) ).

cnf(refute_0_132,plain,
    ( andb(btrue,btrue) != btrue
    | andb(nf(var(zero)),nf(var(suc(zero)))) = btrue ),
    inference(resolve,[$cnf( $equal(andb(nf(var(zero)),nf(var(suc(zero)))),andb(btrue,btrue)) )],[refute_0_130,refute_0_131]) ).

cnf(refute_0_133,plain,
    andb(nf(var(zero)),nf(var(suc(zero)))) = btrue,
    inference(resolve,[$cnf( $equal(andb(btrue,btrue),btrue) )],[refute_0_112,refute_0_132]) ).

cnf(refute_0_134,plain,
    nf(app(app(var(X),X_139,X_140),X_141,X_138)) = andb(nf(app(var(X),X_139,X_140)),nf(X_141)),
    inference(subst,[],[axiom_010:[bind(X,$fot(var(X))),bind(X2,$fot(X_138)),bind(X3,$fot(X_139)),bind(X4,$fot(X_140)),bind(Z,$fot(X_141))]]) ).

cnf(refute_0_135,plain,
    andb(btrue,nf(Z)) = nf(Z),
    inference(subst,[],[axiom_007:[bind(Q,$fot(nf(Z)))]]) ).

cnf(refute_0_136,plain,
    nf(var(X)) = btrue,
    inference(subst,[],[axiom_013:[bind(X4,$fot(X))]]) ).

cnf(refute_0_137,plain,
    andb(nf(var(X)),nf(Z)) = andb(nf(var(X)),nf(Z)),
    introduced(tautology,[refl,[$fot(andb(nf(var(X)),nf(Z)))]]) ).

cnf(refute_0_138,plain,
    ( andb(nf(var(X)),nf(Z)) != andb(nf(var(X)),nf(Z))
    | nf(var(X)) != btrue
    | andb(nf(var(X)),nf(Z)) = andb(btrue,nf(Z)) ),
    introduced(tautology,[equality,[$cnf( $equal(andb(nf(var(X)),nf(Z)),andb(nf(var(X)),nf(Z))) ),[1,0],$fot(btrue)]]) ).

cnf(refute_0_139,plain,
    ( nf(var(X)) != btrue
    | andb(nf(var(X)),nf(Z)) = andb(btrue,nf(Z)) ),
    inference(resolve,[$cnf( $equal(andb(nf(var(X)),nf(Z)),andb(nf(var(X)),nf(Z))) )],[refute_0_137,refute_0_138]) ).

cnf(refute_0_140,plain,
    andb(nf(var(X)),nf(Z)) = andb(btrue,nf(Z)),
    inference(resolve,[$cnf( $equal(nf(var(X)),btrue) )],[refute_0_136,refute_0_139]) ).

cnf(refute_0_141,plain,
    ( andb(btrue,nf(Z)) != nf(Z)
    | andb(nf(var(X)),nf(Z)) != andb(btrue,nf(Z))
    | andb(nf(var(X)),nf(Z)) = nf(Z) ),
    inference(subst,[],[refute_0_127:[bind(X0,$fot(andb(nf(var(X)),nf(Z)))),bind(Y0,$fot(andb(btrue,nf(Z)))),bind(Z0,$fot(nf(Z)))]]) ).

cnf(refute_0_142,plain,
    ( andb(btrue,nf(Z)) != nf(Z)
    | andb(nf(var(X)),nf(Z)) = nf(Z) ),
    inference(resolve,[$cnf( $equal(andb(nf(var(X)),nf(Z)),andb(btrue,nf(Z))) )],[refute_0_140,refute_0_141]) ).

cnf(refute_0_143,plain,
    andb(nf(var(X)),nf(Z)) = nf(Z),
    inference(resolve,[$cnf( $equal(andb(btrue,nf(Z)),nf(Z)) )],[refute_0_135,refute_0_142]) ).

cnf(refute_0_144,plain,
    ( andb(nf(var(X)),nf(Z)) != nf(Z)
    | nf(app(var(X),Z,X2)) != andb(nf(var(X)),nf(Z))
    | nf(app(var(X),Z,X2)) = nf(Z) ),
    introduced(tautology,[equality,[$cnf( $equal(nf(app(var(X),Z,X2)),andb(nf(var(X)),nf(Z))) ),[1],$fot(nf(Z))]]) ).

cnf(refute_0_145,plain,
    ( nf(app(var(X),Z,X2)) != andb(nf(var(X)),nf(Z))
    | nf(app(var(X),Z,X2)) = nf(Z) ),
    inference(resolve,[$cnf( $equal(andb(nf(var(X)),nf(Z)),nf(Z)) )],[refute_0_143,refute_0_144]) ).

cnf(refute_0_146,plain,
    nf(app(var(X),Z,X2)) = nf(Z),
    inference(resolve,[$cnf( $equal(nf(app(var(X),Z,X2)),andb(nf(var(X)),nf(Z))) )],[axiom_011,refute_0_145]) ).

cnf(refute_0_147,plain,
    nf(app(var(X),X_139,X_140)) = nf(X_139),
    inference(subst,[],[refute_0_146:[bind(X2,$fot(X_140)),bind(Z,$fot(X_139))]]) ).

cnf(refute_0_148,plain,
    ( nf(app(app(var(X),X_139,X_140),X_141,X_138)) != andb(nf(app(var(X),X_139,X_140)),nf(X_141))
    | nf(app(var(X),X_139,X_140)) != nf(X_139)
    | nf(app(app(var(X),X_139,X_140),X_141,X_138)) = andb(nf(X_139),nf(X_141)) ),
    introduced(tautology,[equality,[$cnf( $equal(nf(app(app(var(X),X_139,X_140),X_141,X_138)),andb(nf(app(var(X),X_139,X_140)),nf(X_141))) ),[1,0],$fot(nf(X_139))]]) ).

cnf(refute_0_149,plain,
    ( nf(app(app(var(X),X_139,X_140),X_141,X_138)) != andb(nf(app(var(X),X_139,X_140)),nf(X_141))
    | nf(app(app(var(X),X_139,X_140),X_141,X_138)) = andb(nf(X_139),nf(X_141)) ),
    inference(resolve,[$cnf( $equal(nf(app(var(X),X_139,X_140)),nf(X_139)) )],[refute_0_147,refute_0_148]) ).

cnf(refute_0_150,plain,
    nf(app(app(var(X),X_139,X_140),X_141,X_138)) = andb(nf(X_139),nf(X_141)),
    inference(resolve,[$cnf( $equal(nf(app(app(var(X),X_139,X_140),X_141,X_138)),andb(nf(app(var(X),X_139,X_140)),nf(X_141))) )],[refute_0_134,refute_0_149]) ).

cnf(refute_0_151,plain,
    nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)) = andb(nf(var(zero)),nf(var(suc(zero)))),
    inference(subst,[],[refute_0_150:[bind(X,$fot(suc(suc(zero)))),bind(X_138,$fot(b)),bind(X_139,$fot(var(zero))),bind(X_140,$fot(X_3575)),bind(X_141,$fot(var(suc(zero))))]]) ).

cnf(refute_0_152,plain,
    ( andb(nf(var(zero)),nf(var(suc(zero)))) != btrue
    | nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)) != andb(nf(var(zero)),nf(var(suc(zero))))
    | nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)) = btrue ),
    inference(subst,[],[refute_0_127:[bind(X0,$fot(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)))),bind(Y0,$fot(andb(nf(var(zero)),nf(var(suc(zero)))))),bind(Z0,$fot(btrue))]]) ).

cnf(refute_0_153,plain,
    ( andb(nf(var(zero)),nf(var(suc(zero)))) != btrue
    | nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)) = btrue ),
    inference(resolve,[$cnf( $equal(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(nf(var(zero)),nf(var(suc(zero))))) )],[refute_0_151,refute_0_152]) ).

cnf(refute_0_154,plain,
    nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)) = btrue,
    inference(resolve,[$cnf( $equal(andb(nf(var(zero)),nf(var(suc(zero)))),btrue) )],[refute_0_133,refute_0_153]) ).

cnf(refute_0_155,plain,
    andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) = andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)),
    introduced(tautology,[refl,[$fot(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))]]) ).

cnf(refute_0_156,plain,
    ( andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) != andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))
    | nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)) != btrue
    | andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) = andb(btrue,andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) ),
    introduced(tautology,[equality,[$cnf( $equal(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)),andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))) ),[1,0],$fot(btrue)]]) ).

cnf(refute_0_157,plain,
    ( nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)) != btrue
    | andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) = andb(btrue,andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) ),
    inference(resolve,[$cnf( $equal(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)),andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))) )],[refute_0_155,refute_0_156]) ).

cnf(refute_0_158,plain,
    andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) = andb(btrue,andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)),
    inference(resolve,[$cnf( $equal(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),btrue) )],[refute_0_154,refute_0_157]) ).

cnf(refute_0_159,plain,
    ( andb(btrue,andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) != andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)
    | andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) != andb(btrue,andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))
    | andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) = andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue) ),
    inference(subst,[],[refute_0_127:[bind(X0,$fot(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))),bind(Y0,$fot(andb(btrue,andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))),bind(Z0,$fot(andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))]]) ).

cnf(refute_0_160,plain,
    ( andb(btrue,andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) != andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)
    | andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) = andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue) ),
    inference(resolve,[$cnf( $equal(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)),andb(btrue,andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))) )],[refute_0_158,refute_0_159]) ).

cnf(refute_0_161,plain,
    andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) = andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue),
    inference(resolve,[$cnf( $equal(andb(btrue,andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) )],[refute_0_111,refute_0_160]) ).

cnf(refute_0_162,plain,
    notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))) = notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))),
    introduced(tautology,[refl,[$fot(notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))))]]) ).

cnf(refute_0_163,plain,
    ( andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) != andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)
    | notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))) != notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))
    | notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) ),
    introduced(tautology,[equality,[$cnf( $equal(notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))),notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))) ),[1,0],$fot(andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))]]) ).

cnf(refute_0_164,plain,
    ( andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) != andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)
    | notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) ),
    inference(resolve,[$cnf( $equal(notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))),notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))) )],[refute_0_162,refute_0_163]) ).

cnf(refute_0_165,plain,
    notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)),
    inference(resolve,[$cnf( $equal(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) )],[refute_0_161,refute_0_164]) ).

cnf(refute_0_166,plain,
    ( notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))) != notb(andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))
    | sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))) != notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))
    | sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) ),
    introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))),notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))) ),[1],$fot(notb(andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))]]) ).

cnf(refute_0_167,plain,
    ( sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))) != notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))
    | sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)) ),
    inference(resolve,[$cnf( $equal(notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))),notb(andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue))) )],[refute_0_165,refute_0_166]) ).

cnf(refute_0_168,plain,
    sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)),
    inference(resolve,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b))))),notb(andb(nf(app(app(var(suc(suc(zero))),var(zero),X_3575),var(suc(zero)),b)),andb(andb(eq(arr(a,arr(b,c)),arr(X_3575,arr(b,c))),eq(a,X_3575)),btrue)))) )],[refute_0_110,refute_0_167]) ).

cnf(refute_0_169,plain,
    sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),eq(a,a)),btrue)),
    inference(subst,[],[refute_0_168:[bind(X_3575,$fot(a))]]) ).

cnf(refute_0_170,plain,
    eq(a,a) = btrue,
    inference(subst,[],[axiom_051:[bind(X,$fot(a))]]) ).

cnf(refute_0_171,plain,
    ( eq(a,a) != btrue
    | sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) != notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),eq(a,a)),btrue))
    | sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) ),
    introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),eq(a,a)),btrue))) ),[1,0,0,1],$fot(btrue)]]) ).

cnf(refute_0_172,plain,
    ( sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) != notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),eq(a,a)),btrue))
    | sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) ),
    inference(resolve,[$cnf( $equal(eq(a,a),btrue) )],[refute_0_170,refute_0_171]) ).

cnf(refute_0_173,plain,
    sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)),
    inference(resolve,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),eq(a,a)),btrue))) )],[refute_0_169,refute_0_172]) ).

cnf(refute_0_174,plain,
    eq(c,c) = btrue,
    inference(subst,[],[axiom_051:[bind(X,$fot(c))]]) ).

cnf(refute_0_175,plain,
    ( eq(X_1129,X_1129) != btrue
    | eq(arr(X_1129,X_1128),arr(X_1129,X_1127)) = eq(X_1128,X_1127) ),
    inference(subst,[],[axiom_033:[bind(X,$fot(X_1129)),bind(X2,$fot(X_1127)),bind(Y,$fot(X_1128)),bind(Z,$fot(X_1129))]]) ).

cnf(refute_0_176,plain,
    eq(X_1129,X_1129) = btrue,
    inference(subst,[],[axiom_051:[bind(X,$fot(X_1129))]]) ).

cnf(refute_0_177,plain,
    ( btrue != btrue
    | eq(X_1129,X_1129) != btrue
    | eq(X_1129,X_1129) = btrue ),
    introduced(tautology,[equality,[$cnf( $equal(eq(X_1129,X_1129),btrue) ),[1],$fot(btrue)]]) ).

cnf(refute_0_178,plain,
    ( btrue != btrue
    | eq(X_1129,X_1129) = btrue ),
    inference(resolve,[$cnf( $equal(eq(X_1129,X_1129),btrue) )],[refute_0_176,refute_0_177]) ).

cnf(refute_0_179,plain,
    ( btrue != btrue
    | eq(arr(X_1129,X_1128),arr(X_1129,X_1127)) = eq(X_1128,X_1127) ),
    inference(resolve,[$cnf( $equal(eq(X_1129,X_1129),btrue) )],[refute_0_178,refute_0_175]) ).

cnf(refute_0_180,plain,
    btrue = btrue,
    introduced(tautology,[refl,[$fot(btrue)]]) ).

cnf(refute_0_181,plain,
    eq(arr(X_1129,X_1128),arr(X_1129,X_1127)) = eq(X_1128,X_1127),
    inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_180,refute_0_179]) ).

cnf(refute_0_182,plain,
    eq(arr(b,c),arr(b,c)) = eq(c,c),
    inference(subst,[],[refute_0_181:[bind(X_1127,$fot(c)),bind(X_1128,$fot(c)),bind(X_1129,$fot(b))]]) ).

cnf(refute_0_183,plain,
    ( eq(arr(b,c),arr(b,c)) != eq(c,c)
    | eq(c,c) != btrue
    | eq(arr(b,c),arr(b,c)) = btrue ),
    inference(subst,[],[refute_0_127:[bind(X0,$fot(eq(arr(b,c),arr(b,c)))),bind(Y0,$fot(eq(c,c))),bind(Z0,$fot(btrue))]]) ).

cnf(refute_0_184,plain,
    ( eq(c,c) != btrue
    | eq(arr(b,c),arr(b,c)) = btrue ),
    inference(resolve,[$cnf( $equal(eq(arr(b,c),arr(b,c)),eq(c,c)) )],[refute_0_182,refute_0_183]) ).

cnf(refute_0_185,plain,
    eq(arr(b,c),arr(b,c)) = btrue,
    inference(resolve,[$cnf( $equal(eq(c,c),btrue) )],[refute_0_174,refute_0_184]) ).

cnf(refute_0_186,plain,
    eq(arr(a,arr(b,c)),arr(a,arr(b,c))) = eq(arr(b,c),arr(b,c)),
    inference(subst,[],[refute_0_181:[bind(X_1127,$fot(arr(b,c))),bind(X_1128,$fot(arr(b,c))),bind(X_1129,$fot(a))]]) ).

cnf(refute_0_187,plain,
    ( eq(arr(a,arr(b,c)),arr(a,arr(b,c))) != eq(arr(b,c),arr(b,c))
    | eq(arr(b,c),arr(b,c)) != btrue
    | eq(arr(a,arr(b,c)),arr(a,arr(b,c))) = btrue ),
    inference(subst,[],[refute_0_127:[bind(X0,$fot(eq(arr(a,arr(b,c)),arr(a,arr(b,c))))),bind(Y0,$fot(eq(arr(b,c),arr(b,c)))),bind(Z0,$fot(btrue))]]) ).

cnf(refute_0_188,plain,
    ( eq(arr(b,c),arr(b,c)) != btrue
    | eq(arr(a,arr(b,c)),arr(a,arr(b,c))) = btrue ),
    inference(resolve,[$cnf( $equal(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),eq(arr(b,c),arr(b,c))) )],[refute_0_186,refute_0_187]) ).

cnf(refute_0_189,plain,
    eq(arr(a,arr(b,c)),arr(a,arr(b,c))) = btrue,
    inference(resolve,[$cnf( $equal(eq(arr(b,c),arr(b,c)),btrue) )],[refute_0_185,refute_0_188]) ).

cnf(refute_0_190,plain,
    andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),
    introduced(tautology,[refl,[$fot(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue))]]) ).

cnf(refute_0_191,plain,
    ( andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) != andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue)
    | eq(arr(a,arr(b,c)),arr(a,arr(b,c))) != btrue
    | andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = andb(btrue,btrue) ),
    introduced(tautology,[equality,[$cnf( $equal(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue)) ),[1,0],$fot(btrue)]]) ).

cnf(refute_0_192,plain,
    ( eq(arr(a,arr(b,c)),arr(a,arr(b,c))) != btrue
    | andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = andb(btrue,btrue) ),
    inference(resolve,[$cnf( $equal(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue)) )],[refute_0_190,refute_0_191]) ).

cnf(refute_0_193,plain,
    andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = andb(btrue,btrue),
    inference(resolve,[$cnf( $equal(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) )],[refute_0_189,refute_0_192]) ).

cnf(refute_0_194,plain,
    ( andb(btrue,btrue) != btrue
    | andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) != andb(btrue,btrue)
    | andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = btrue ),
    inference(subst,[],[refute_0_127:[bind(X0,$fot(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue))),bind(Y0,$fot(andb(btrue,btrue))),bind(Z0,$fot(btrue))]]) ).

cnf(refute_0_195,plain,
    ( andb(btrue,btrue) != btrue
    | andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = btrue ),
    inference(resolve,[$cnf( $equal(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),andb(btrue,btrue)) )],[refute_0_193,refute_0_194]) ).

cnf(refute_0_196,plain,
    andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = btrue,
    inference(resolve,[$cnf( $equal(andb(btrue,btrue),btrue) )],[refute_0_112,refute_0_195]) ).

cnf(refute_0_197,plain,
    andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue),
    introduced(tautology,[refl,[$fot(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))]]) ).

cnf(refute_0_198,plain,
    ( andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) != andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)
    | andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) != btrue
    | andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = andb(btrue,btrue) ),
    introduced(tautology,[equality,[$cnf( $equal(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue),andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) ),[1,0],$fot(btrue)]]) ).

cnf(refute_0_199,plain,
    ( andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) != btrue
    | andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = andb(btrue,btrue) ),
    inference(resolve,[$cnf( $equal(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue),andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) )],[refute_0_197,refute_0_198]) ).

cnf(refute_0_200,plain,
    andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = andb(btrue,btrue),
    inference(resolve,[$cnf( $equal(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) )],[refute_0_196,refute_0_199]) ).

cnf(refute_0_201,plain,
    ( andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) != andb(btrue,btrue)
    | andb(btrue,btrue) != btrue
    | andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = btrue ),
    inference(subst,[],[refute_0_127:[bind(X0,$fot(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))),bind(Y0,$fot(andb(btrue,btrue))),bind(Z0,$fot(btrue))]]) ).

cnf(refute_0_202,plain,
    ( andb(btrue,btrue) != btrue
    | andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = btrue ),
    inference(resolve,[$cnf( $equal(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue),andb(btrue,btrue)) )],[refute_0_200,refute_0_201]) ).

cnf(refute_0_203,plain,
    andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = btrue,
    inference(resolve,[$cnf( $equal(andb(btrue,btrue),btrue) )],[refute_0_112,refute_0_202]) ).

cnf(refute_0_204,plain,
    notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)),
    introduced(tautology,[refl,[$fot(notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)))]]) ).

cnf(refute_0_205,plain,
    ( andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) != btrue
    | notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) != notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))
    | notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = notb(btrue) ),
    introduced(tautology,[equality,[$cnf( $equal(notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)),notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))) ),[1,0],$fot(btrue)]]) ).

cnf(refute_0_206,plain,
    ( andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) != btrue
    | notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = notb(btrue) ),
    inference(resolve,[$cnf( $equal(notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)),notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))) )],[refute_0_204,refute_0_205]) ).

cnf(refute_0_207,plain,
    notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = notb(btrue),
    inference(resolve,[$cnf( $equal(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue),btrue) )],[refute_0_203,refute_0_206]) ).

cnf(refute_0_208,plain,
    ( notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) != notb(btrue)
    | notb(btrue) != bfalse
    | notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = bfalse ),
    inference(subst,[],[refute_0_127:[bind(X0,$fot(notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)))),bind(Y0,$fot(notb(btrue))),bind(Z0,$fot(bfalse))]]) ).

cnf(refute_0_209,plain,
    ( notb(btrue) != bfalse
    | notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = bfalse ),
    inference(resolve,[$cnf( $equal(notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)),notb(btrue)) )],[refute_0_207,refute_0_208]) ).

cnf(refute_0_210,plain,
    notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = bfalse,
    inference(resolve,[$cnf( $equal(notb(btrue),bfalse) )],[axiom_002,refute_0_209]) ).

cnf(refute_0_211,plain,
    ( notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) != bfalse
    | sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) != notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))
    | sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = bfalse ),
    introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))) ),[1],$fot(bfalse)]]) ).

cnf(refute_0_212,plain,
    ( sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) != notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))
    | sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = bfalse ),
    inference(resolve,[$cnf( $equal(notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)),bfalse) )],[refute_0_210,refute_0_211]) ).

cnf(refute_0_213,plain,
    sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = bfalse,
    inference(resolve,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))) )],[refute_0_173,refute_0_212]) ).

cnf(refute_0_214,plain,
    ( eq4(bfalse,bfalse) != btrue
    | sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) != bfalse
    | eq4(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),bfalse) = btrue ),
    introduced(tautology,[equality,[$cnf( ~ $equal(eq4(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),bfalse),btrue) ),[0,0],$fot(bfalse)]]) ).

cnf(refute_0_215,plain,
    ( eq4(bfalse,bfalse) != btrue
    | eq4(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),bfalse) = btrue ),
    inference(resolve,[$cnf( $equal(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),bfalse) )],[refute_0_213,refute_0_214]) ).

cnf(refute_0_216,plain,
    eq4(bfalse,bfalse) != btrue,
    inference(resolve,[$cnf( $equal(eq4(sat_synth_nf_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),bfalse),btrue) )],[refute_0_215,refute_0_0]) ).

cnf(refute_0_217,plain,
    eq4(bfalse,bfalse) = btrue,
    inference(subst,[],[axiom_054:[bind(X,$fot(bfalse))]]) ).

cnf(refute_0_218,plain,
    ( btrue != btrue
    | eq4(bfalse,bfalse) != btrue
    | eq4(bfalse,bfalse) = btrue ),
    introduced(tautology,[equality,[$cnf( $equal(eq4(bfalse,bfalse),btrue) ),[1],$fot(btrue)]]) ).

cnf(refute_0_219,plain,
    ( btrue != btrue
    | eq4(bfalse,bfalse) = btrue ),
    inference(resolve,[$cnf( $equal(eq4(bfalse,bfalse),btrue) )],[refute_0_217,refute_0_218]) ).

cnf(refute_0_220,plain,
    btrue != btrue,
    inference(resolve,[$cnf( $equal(eq4(bfalse,bfalse),btrue) )],[refute_0_219,refute_0_216]) ).

cnf(refute_0_221,plain,
    $false,
    inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_180,refute_0_220]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : SWX221-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12  % Command  : metis --show proof --show saturation %s
% 0.15/0.33  % Computer : n028.cluster.edu
% 0.15/0.33  % Model    : x86_64 x86_64
% 0.15/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33  % Memory   : 8042.1875MB
% 0.15/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33  % CPULimit : 300
% 0.15/0.33  % WCLimit  : 300
% 0.15/0.33  % DateTime : Tue May  5 12:31:15 EDT 2026
% 0.15/0.33  % CPUTime  : 
% 0.15/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 27.86/28.11  % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.86/28.11  
% 27.86/28.11  % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 27.96/28.14  
%------------------------------------------------------------------------------