%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWX223-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 07:04:36 PM UTC 2026
% Result : Unsatisfiable 4.86s 5.08s
% Output : CNFRefutation 4.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 67
% Syntax : Number of clauses : 206 ( 111 unt; 0 nHn; 122 RR)
% Number of literals : 348 ( 347 equ; 146 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 3 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 6 con; 0-4 aty)
% Number of variables : 312 ( 34 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_w(X) = notb(andb(nf(X),tc(nil,X,arr(arr(a,arr(a,b)),arr(a,b))))) ).
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_w(X),bfalse) != btrue ).
cnf(refute_0_0,plain,
eq4(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),bfalse) != btrue,
inference(subst,[],[goal:[bind(X,$fot(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))))]]) ).
cnf(refute_0_1,plain,
sat_synth_nf_w(lam(E)) = notb(andb(nf(lam(E)),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))),
inference(subst,[],[axiom_020:[bind(X,$fot(lam(E)))]]) ).
cnf(refute_0_2,plain,
( nf(lam(E)) != nf(E)
| sat_synth_nf_w(lam(E)) != notb(andb(nf(lam(E)),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))))
| sat_synth_nf_w(lam(E)) = notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_w(lam(E)),notb(andb(nf(lam(E)),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))))) ),[1,0,0],$fot(nf(E))]]) ).
cnf(refute_0_3,plain,
( sat_synth_nf_w(lam(E)) != notb(andb(nf(lam(E)),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))))
| sat_synth_nf_w(lam(E)) = notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))) ),
inference(resolve,[$cnf( $equal(nf(lam(E)),nf(E)) )],[axiom_012,refute_0_2]) ).
cnf(refute_0_4,plain,
sat_synth_nf_w(lam(E)) = notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))),
inference(resolve,[$cnf( $equal(sat_synth_nf_w(lam(E)),notb(andb(nf(lam(E)),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))))) )],[refute_0_1,refute_0_3]) ).
cnf(refute_0_5,plain,
tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))) = tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b)),
inference(subst,[],[axiom_015:[bind(T1,$fot(arr(a,b))),bind(Tx2,$fot(arr(a,arr(a,b)))),bind(X,$fot(nil))]]) ).
cnf(refute_0_6,plain,
andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))) = andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))),
introduced(tautology,[refl,[$fot(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))))]]) ).
cnf(refute_0_7,plain,
( andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))) != andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))
| tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))) != tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b))
| andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))) = andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b))) ),
introduced(tautology,[equality,[$cnf( $equal(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))),andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))) ),[1,1],$fot(tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b)))]]) ).
cnf(refute_0_8,plain,
( tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))) != tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b))
| andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))) = andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b))) ),
inference(resolve,[$cnf( $equal(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))),andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))) )],[refute_0_6,refute_0_7]) ).
cnf(refute_0_9,plain,
andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))) = andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b))),
inference(resolve,[$cnf( $equal(tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b))) )],[refute_0_5,refute_0_8]) ).
cnf(refute_0_10,plain,
notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))) = notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))),
introduced(tautology,[refl,[$fot(notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))))]]) ).
cnf(refute_0_11,plain,
( andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))) != andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b)))
| notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))) != notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))))
| notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))) = notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b)))) ),
introduced(tautology,[equality,[$cnf( $equal(notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))),notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))))) ),[1,0],$fot(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b))))]]) ).
cnf(refute_0_12,plain,
( andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))) != andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b)))
| notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))) = notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b)))) ),
inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))),notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))))) )],[refute_0_10,refute_0_11]) ).
cnf(refute_0_13,plain,
notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))) = notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b)))),
inference(resolve,[$cnf( $equal(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))),andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b)))) )],[refute_0_9,refute_0_12]) ).
cnf(refute_0_14,plain,
( notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))) != notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b))))
| sat_synth_nf_w(lam(E)) != notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))))
| sat_synth_nf_w(lam(E)) = notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b)))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_w(lam(E)),notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))))) ),[1],$fot(notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b)))))]]) ).
cnf(refute_0_15,plain,
( sat_synth_nf_w(lam(E)) != notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))))
| sat_synth_nf_w(lam(E)) = notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b)))) ),
inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b))))),notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b))))) )],[refute_0_13,refute_0_14]) ).
cnf(refute_0_16,plain,
sat_synth_nf_w(lam(E)) = notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),E,arr(a,b)))),
inference(resolve,[$cnf( $equal(sat_synth_nf_w(lam(E)),notb(andb(nf(E),tc(nil,lam(E),arr(arr(a,arr(a,b)),arr(a,b)))))) )],[refute_0_4,refute_0_15]) ).
cnf(refute_0_17,plain,
sat_synth_nf_w(lam(lam(E))) = notb(andb(nf(lam(E)),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))),
inference(subst,[],[refute_0_16:[bind(E,$fot(lam(E)))]]) ).
cnf(refute_0_18,plain,
( nf(lam(E)) != nf(E)
| sat_synth_nf_w(lam(lam(E))) != notb(andb(nf(lam(E)),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))))
| sat_synth_nf_w(lam(lam(E))) = notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_w(lam(lam(E))),notb(andb(nf(lam(E)),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))))) ),[1,0,0],$fot(nf(E))]]) ).
cnf(refute_0_19,plain,
( sat_synth_nf_w(lam(lam(E))) != notb(andb(nf(lam(E)),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))))
| sat_synth_nf_w(lam(lam(E))) = notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))) ),
inference(resolve,[$cnf( $equal(nf(lam(E)),nf(E)) )],[axiom_012,refute_0_18]) ).
cnf(refute_0_20,plain,
sat_synth_nf_w(lam(lam(E))) = notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))),
inference(resolve,[$cnf( $equal(sat_synth_nf_w(lam(lam(E))),notb(andb(nf(lam(E)),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))))) )],[refute_0_17,refute_0_19]) ).
cnf(refute_0_21,plain,
tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)) = tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b),
inference(subst,[],[axiom_015:[bind(T1,$fot(b)),bind(Tx2,$fot(a)),bind(X,$fot(cons(arr(a,arr(a,b)),nil)))]]) ).
cnf(refute_0_22,plain,
andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))) = andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))),
introduced(tautology,[refl,[$fot(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))))]]) ).
cnf(refute_0_23,plain,
( andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))) != andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))
| tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)) != tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b)
| andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))) = andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b)) ),
introduced(tautology,[equality,[$cnf( $equal(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))),andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))) ),[1,1],$fot(tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b))]]) ).
cnf(refute_0_24,plain,
( tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)) != tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b)
| andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))) = andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b)) ),
inference(resolve,[$cnf( $equal(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))),andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))) )],[refute_0_22,refute_0_23]) ).
cnf(refute_0_25,plain,
andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))) = andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b)),
inference(resolve,[$cnf( $equal(tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b)) )],[refute_0_21,refute_0_24]) ).
cnf(refute_0_26,plain,
notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))) = notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))),
introduced(tautology,[refl,[$fot(notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))))]]) ).
cnf(refute_0_27,plain,
( andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))) != andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b))
| notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))) != notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))))
| notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))) = notb(andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b))) ),
introduced(tautology,[equality,[$cnf( $equal(notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))),notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))))) ),[1,0],$fot(andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b)))]]) ).
cnf(refute_0_28,plain,
( andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))) != andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b))
| notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))) = notb(andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b))) ),
inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))),notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))))) )],[refute_0_26,refute_0_27]) ).
cnf(refute_0_29,plain,
notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))) = notb(andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b))),
inference(resolve,[$cnf( $equal(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))),andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b))) )],[refute_0_25,refute_0_28]) ).
cnf(refute_0_30,plain,
( notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))) != notb(andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b)))
| sat_synth_nf_w(lam(lam(E))) != notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))))
| sat_synth_nf_w(lam(lam(E))) = notb(andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_w(lam(lam(E))),notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))))) ),[1],$fot(notb(andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b))))]]) ).
cnf(refute_0_31,plain,
( sat_synth_nf_w(lam(lam(E))) != notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))))
| sat_synth_nf_w(lam(lam(E))) = notb(andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b))) ),
inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))),notb(andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b)))) )],[refute_0_29,refute_0_30]) ).
cnf(refute_0_32,plain,
sat_synth_nf_w(lam(lam(E))) = notb(andb(nf(E),tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b))),
inference(resolve,[$cnf( $equal(sat_synth_nf_w(lam(lam(E))),notb(andb(nf(E),tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))))) )],[refute_0_20,refute_0_31]) ).
cnf(refute_0_33,plain,
sat_synth_nf_w(lam(lam(app(X_872,var(zero),a)))) = notb(andb(nf(app(X_872,var(zero),a)),tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_872,var(zero),a),b))),
inference(subst,[],[refute_0_32:[bind(E,$fot(app(X_872,var(zero),a)))]]) ).
cnf(refute_0_34,plain,
tc(cons(Z,Xs),app(X_200,var(zero),X_201),X_204) = andb(tc(cons(Z,Xs),X_200,arr(X_201,X_204)),tc(cons(Z,Xs),var(zero),X_201)),
inference(subst,[],[axiom_014:[bind(F,$fot(X_200)),bind(Tx,$fot(X_201)),bind(X,$fot(cons(Z,Xs))),bind(X2,$fot(var(zero))),bind(Z,$fot(X_204))]]) ).
cnf(refute_0_35,plain,
tc(cons(Z,Xs),var(zero),X_70) = aux(cons(Z,Xs),X_70,zero,index(cons(Z,Xs),zero)),
inference(subst,[],[axiom_019:[bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(zero)),bind(Z,$fot(X_70))]]) ).
cnf(refute_0_36,plain,
( index(cons(Z,Xs),zero) != just(Z)
| tc(cons(Z,Xs),var(zero),X_70) != aux(cons(Z,Xs),X_70,zero,index(cons(Z,Xs),zero))
| tc(cons(Z,Xs),var(zero),X_70) = aux(cons(Z,Xs),X_70,zero,just(Z)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_70),aux(cons(Z,Xs),X_70,zero,index(cons(Z,Xs),zero))) ),[1,3],$fot(just(Z))]]) ).
cnf(refute_0_37,plain,
( tc(cons(Z,Xs),var(zero),X_70) != aux(cons(Z,Xs),X_70,zero,index(cons(Z,Xs),zero))
| tc(cons(Z,Xs),var(zero),X_70) = aux(cons(Z,Xs),X_70,zero,just(Z)) ),
inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(Z)) )],[axiom_005,refute_0_36]) ).
cnf(refute_0_38,plain,
tc(cons(Z,Xs),var(zero),X_70) = aux(cons(Z,Xs),X_70,zero,just(Z)),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_70),aux(cons(Z,Xs),X_70,zero,index(cons(Z,Xs),zero))) )],[refute_0_35,refute_0_37]) ).
cnf(refute_0_39,plain,
aux(cons(Z,Xs),X_70,zero,just(Z)) = eq(Z,X_70),
inference(subst,[],[axiom_001:[bind(Tx3,$fot(Z)),bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(zero)),bind(Z,$fot(X_70))]]) ).
cnf(refute_0_40,plain,
( aux(cons(Z,Xs),X_70,zero,just(Z)) != eq(Z,X_70)
| tc(cons(Z,Xs),var(zero),X_70) != aux(cons(Z,Xs),X_70,zero,just(Z))
| tc(cons(Z,Xs),var(zero),X_70) = eq(Z,X_70) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_70),aux(cons(Z,Xs),X_70,zero,just(Z))) ),[1],$fot(eq(Z,X_70))]]) ).
cnf(refute_0_41,plain,
( tc(cons(Z,Xs),var(zero),X_70) != aux(cons(Z,Xs),X_70,zero,just(Z))
| tc(cons(Z,Xs),var(zero),X_70) = eq(Z,X_70) ),
inference(resolve,[$cnf( $equal(aux(cons(Z,Xs),X_70,zero,just(Z)),eq(Z,X_70)) )],[refute_0_39,refute_0_40]) ).
cnf(refute_0_42,plain,
tc(cons(Z,Xs),var(zero),X_70) = eq(Z,X_70),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_70),aux(cons(Z,Xs),X_70,zero,just(Z))) )],[refute_0_38,refute_0_41]) ).
cnf(refute_0_43,plain,
tc(cons(Z,Xs),var(zero),X_201) = eq(Z,X_201),
inference(subst,[],[refute_0_42:[bind(X_70,$fot(X_201))]]) ).
cnf(refute_0_44,plain,
( tc(cons(Z,Xs),app(X_200,var(zero),X_201),X_204) != andb(tc(cons(Z,Xs),X_200,arr(X_201,X_204)),tc(cons(Z,Xs),var(zero),X_201))
| tc(cons(Z,Xs),var(zero),X_201) != eq(Z,X_201)
| tc(cons(Z,Xs),app(X_200,var(zero),X_201),X_204) = andb(tc(cons(Z,Xs),X_200,arr(X_201,X_204)),eq(Z,X_201)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),app(X_200,var(zero),X_201),X_204),andb(tc(cons(Z,Xs),X_200,arr(X_201,X_204)),tc(cons(Z,Xs),var(zero),X_201))) ),[1,1],$fot(eq(Z,X_201))]]) ).
cnf(refute_0_45,plain,
( tc(cons(Z,Xs),app(X_200,var(zero),X_201),X_204) != andb(tc(cons(Z,Xs),X_200,arr(X_201,X_204)),tc(cons(Z,Xs),var(zero),X_201))
| tc(cons(Z,Xs),app(X_200,var(zero),X_201),X_204) = andb(tc(cons(Z,Xs),X_200,arr(X_201,X_204)),eq(Z,X_201)) ),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_201),eq(Z,X_201)) )],[refute_0_43,refute_0_44]) ).
cnf(refute_0_46,plain,
tc(cons(Z,Xs),app(X_200,var(zero),X_201),X_204) = andb(tc(cons(Z,Xs),X_200,arr(X_201,X_204)),eq(Z,X_201)),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),app(X_200,var(zero),X_201),X_204),andb(tc(cons(Z,Xs),X_200,arr(X_201,X_204)),tc(cons(Z,Xs),var(zero),X_201))) )],[refute_0_34,refute_0_45]) ).
cnf(refute_0_47,plain,
tc(cons(X_839,X_836),app(X_838,var(zero),X_839),X_840) = andb(tc(cons(X_839,X_836),X_838,arr(X_839,X_840)),eq(X_839,X_839)),
inference(subst,[],[refute_0_46:[bind(Xs,$fot(X_836)),bind(Z,$fot(X_839)),bind(X_200,$fot(X_838)),bind(X_201,$fot(X_839)),bind(X_204,$fot(X_840))]]) ).
cnf(refute_0_48,plain,
eq(X_839,X_839) = btrue,
inference(subst,[],[axiom_051:[bind(X,$fot(X_839))]]) ).
cnf(refute_0_49,plain,
( eq(X_839,X_839) != btrue
| tc(cons(X_839,X_836),app(X_838,var(zero),X_839),X_840) != andb(tc(cons(X_839,X_836),X_838,arr(X_839,X_840)),eq(X_839,X_839))
| tc(cons(X_839,X_836),app(X_838,var(zero),X_839),X_840) = andb(tc(cons(X_839,X_836),X_838,arr(X_839,X_840)),btrue) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_839,X_836),app(X_838,var(zero),X_839),X_840),andb(tc(cons(X_839,X_836),X_838,arr(X_839,X_840)),eq(X_839,X_839))) ),[1,1],$fot(btrue)]]) ).
cnf(refute_0_50,plain,
( tc(cons(X_839,X_836),app(X_838,var(zero),X_839),X_840) != andb(tc(cons(X_839,X_836),X_838,arr(X_839,X_840)),eq(X_839,X_839))
| tc(cons(X_839,X_836),app(X_838,var(zero),X_839),X_840) = andb(tc(cons(X_839,X_836),X_838,arr(X_839,X_840)),btrue) ),
inference(resolve,[$cnf( $equal(eq(X_839,X_839),btrue) )],[refute_0_48,refute_0_49]) ).
cnf(refute_0_51,plain,
tc(cons(X_839,X_836),app(X_838,var(zero),X_839),X_840) = andb(tc(cons(X_839,X_836),X_838,arr(X_839,X_840)),btrue),
inference(resolve,[$cnf( $equal(tc(cons(X_839,X_836),app(X_838,var(zero),X_839),X_840),andb(tc(cons(X_839,X_836),X_838,arr(X_839,X_840)),eq(X_839,X_839))) )],[refute_0_47,refute_0_50]) ).
cnf(refute_0_52,plain,
tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_872,var(zero),a),b) = andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_872,arr(a,b)),btrue),
inference(subst,[],[refute_0_51:[bind(X_836,$fot(cons(arr(a,arr(a,b)),nil))),bind(X_838,$fot(X_872)),bind(X_839,$fot(a)),bind(X_840,$fot(b))]]) ).
cnf(refute_0_53,plain,
( sat_synth_nf_w(lam(lam(app(X_872,var(zero),a)))) != notb(andb(nf(app(X_872,var(zero),a)),tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_872,var(zero),a),b)))
| tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_872,var(zero),a),b) != andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_872,arr(a,b)),btrue)
| sat_synth_nf_w(lam(lam(app(X_872,var(zero),a)))) = notb(andb(nf(app(X_872,var(zero),a)),andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_872,arr(a,b)),btrue))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_w(lam(lam(app(X_872,var(zero),a)))),notb(andb(nf(app(X_872,var(zero),a)),tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_872,var(zero),a),b)))) ),[1,0,1],$fot(andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_872,arr(a,b)),btrue))]]) ).
cnf(refute_0_54,plain,
( sat_synth_nf_w(lam(lam(app(X_872,var(zero),a)))) != notb(andb(nf(app(X_872,var(zero),a)),tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_872,var(zero),a),b)))
| sat_synth_nf_w(lam(lam(app(X_872,var(zero),a)))) = notb(andb(nf(app(X_872,var(zero),a)),andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_872,arr(a,b)),btrue))) ),
inference(resolve,[$cnf( $equal(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_872,var(zero),a),b),andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_872,arr(a,b)),btrue)) )],[refute_0_52,refute_0_53]) ).
cnf(refute_0_55,plain,
sat_synth_nf_w(lam(lam(app(X_872,var(zero),a)))) = notb(andb(nf(app(X_872,var(zero),a)),andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_872,arr(a,b)),btrue))),
inference(resolve,[$cnf( $equal(sat_synth_nf_w(lam(lam(app(X_872,var(zero),a)))),notb(andb(nf(app(X_872,var(zero),a)),tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_872,var(zero),a),b)))) )],[refute_0_33,refute_0_54]) ).
cnf(refute_0_56,plain,
sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))) = notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_1779),arr(a,b)),btrue))),
inference(subst,[],[refute_0_55:[bind(X_872,$fot(app(var(suc(zero)),var(zero),X_1779)))]]) ).
cnf(refute_0_57,plain,
tc(cons(X_837,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_839),X_840) = andb(tc(cons(X_837,cons(Z,Xs)),var(suc(zero)),arr(X_839,X_840)),eq(X_837,X_839)),
inference(subst,[],[refute_0_46:[bind(Xs,$fot(cons(Z,Xs))),bind(Z,$fot(X_837)),bind(X_200,$fot(var(suc(zero)))),bind(X_201,$fot(X_839)),bind(X_204,$fot(X_840))]]) ).
cnf(refute_0_58,plain,
tc(cons(X_80,X_79),var(suc(X_78)),Z) = aux(cons(X_80,X_79),Z,suc(X_78),index(cons(X_80,X_79),suc(X_78))),
inference(subst,[],[axiom_019:[bind(X,$fot(cons(X_80,X_79))),bind(X3,$fot(suc(X_78)))]]) ).
cnf(refute_0_59,plain,
index(cons(X_80,X_79),suc(X_78)) = index(X_79,X_78),
inference(subst,[],[axiom_006:[bind(N,$fot(X_78)),bind(Xs,$fot(X_79)),bind(Z,$fot(X_80))]]) ).
cnf(refute_0_60,plain,
( index(cons(X_80,X_79),suc(X_78)) != index(X_79,X_78)
| tc(cons(X_80,X_79),var(suc(X_78)),Z) != aux(cons(X_80,X_79),Z,suc(X_78),index(cons(X_80,X_79),suc(X_78)))
| tc(cons(X_80,X_79),var(suc(X_78)),Z) = aux(cons(X_80,X_79),Z,suc(X_78),index(X_79,X_78)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_80,X_79),var(suc(X_78)),Z),aux(cons(X_80,X_79),Z,suc(X_78),index(cons(X_80,X_79),suc(X_78)))) ),[1,3],$fot(index(X_79,X_78))]]) ).
cnf(refute_0_61,plain,
( tc(cons(X_80,X_79),var(suc(X_78)),Z) != aux(cons(X_80,X_79),Z,suc(X_78),index(cons(X_80,X_79),suc(X_78)))
| tc(cons(X_80,X_79),var(suc(X_78)),Z) = aux(cons(X_80,X_79),Z,suc(X_78),index(X_79,X_78)) ),
inference(resolve,[$cnf( $equal(index(cons(X_80,X_79),suc(X_78)),index(X_79,X_78)) )],[refute_0_59,refute_0_60]) ).
cnf(refute_0_62,plain,
tc(cons(X_80,X_79),var(suc(X_78)),Z) = aux(cons(X_80,X_79),Z,suc(X_78),index(X_79,X_78)),
inference(resolve,[$cnf( $equal(tc(cons(X_80,X_79),var(suc(X_78)),Z),aux(cons(X_80,X_79),Z,suc(X_78),index(cons(X_80,X_79),suc(X_78)))) )],[refute_0_58,refute_0_61]) ).
cnf(refute_0_63,plain,
tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92) = aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),index(cons(Z,Xs),zero)),
inference(subst,[],[refute_0_62:[bind(Z,$fot(X_92)),bind(X_78,$fot(zero)),bind(X_79,$fot(cons(Z,Xs))),bind(X_80,$fot(X_95))]]) ).
cnf(refute_0_64,plain,
( index(cons(Z,Xs),zero) != just(Z)
| tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92) != aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),index(cons(Z,Xs),zero))
| tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92) = aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),just(Z)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92),aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),index(cons(Z,Xs),zero))) ),[1,3],$fot(just(Z))]]) ).
cnf(refute_0_65,plain,
( tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92) != aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),index(cons(Z,Xs),zero))
| tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92) = aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),just(Z)) ),
inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(Z)) )],[axiom_005,refute_0_64]) ).
cnf(refute_0_66,plain,
tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92) = aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),just(Z)),
inference(resolve,[$cnf( $equal(tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92),aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),index(cons(Z,Xs),zero))) )],[refute_0_63,refute_0_65]) ).
cnf(refute_0_67,plain,
aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),just(Z)) = eq(Z,X_92),
inference(subst,[],[axiom_001:[bind(Tx3,$fot(Z)),bind(X,$fot(cons(X_95,cons(Z,Xs)))),bind(X3,$fot(suc(zero))),bind(Z,$fot(X_92))]]) ).
cnf(refute_0_68,plain,
( aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),just(Z)) != eq(Z,X_92)
| tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92) != aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),just(Z))
| tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92) = eq(Z,X_92) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92),aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),just(Z))) ),[1],$fot(eq(Z,X_92))]]) ).
cnf(refute_0_69,plain,
( tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92) != aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),just(Z))
| tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92) = eq(Z,X_92) ),
inference(resolve,[$cnf( $equal(aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),just(Z)),eq(Z,X_92)) )],[refute_0_67,refute_0_68]) ).
cnf(refute_0_70,plain,
tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92) = eq(Z,X_92),
inference(resolve,[$cnf( $equal(tc(cons(X_95,cons(Z,Xs)),var(suc(zero)),X_92),aux(cons(X_95,cons(Z,Xs)),X_92,suc(zero),just(Z))) )],[refute_0_66,refute_0_69]) ).
cnf(refute_0_71,plain,
tc(cons(X_837,cons(Z,Xs)),var(suc(zero)),arr(X_839,X_840)) = eq(Z,arr(X_839,X_840)),
inference(subst,[],[refute_0_70:[bind(X_92,$fot(arr(X_839,X_840))),bind(X_95,$fot(X_837))]]) ).
cnf(refute_0_72,plain,
( tc(cons(X_837,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_839),X_840) != andb(tc(cons(X_837,cons(Z,Xs)),var(suc(zero)),arr(X_839,X_840)),eq(X_837,X_839))
| tc(cons(X_837,cons(Z,Xs)),var(suc(zero)),arr(X_839,X_840)) != eq(Z,arr(X_839,X_840))
| tc(cons(X_837,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_839),X_840) = andb(eq(Z,arr(X_839,X_840)),eq(X_837,X_839)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_837,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_839),X_840),andb(tc(cons(X_837,cons(Z,Xs)),var(suc(zero)),arr(X_839,X_840)),eq(X_837,X_839))) ),[1,0],$fot(eq(Z,arr(X_839,X_840)))]]) ).
cnf(refute_0_73,plain,
( tc(cons(X_837,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_839),X_840) != andb(tc(cons(X_837,cons(Z,Xs)),var(suc(zero)),arr(X_839,X_840)),eq(X_837,X_839))
| tc(cons(X_837,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_839),X_840) = andb(eq(Z,arr(X_839,X_840)),eq(X_837,X_839)) ),
inference(resolve,[$cnf( $equal(tc(cons(X_837,cons(Z,Xs)),var(suc(zero)),arr(X_839,X_840)),eq(Z,arr(X_839,X_840))) )],[refute_0_71,refute_0_72]) ).
cnf(refute_0_74,plain,
tc(cons(X_837,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_839),X_840) = andb(eq(Z,arr(X_839,X_840)),eq(X_837,X_839)),
inference(resolve,[$cnf( $equal(tc(cons(X_837,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_839),X_840),andb(tc(cons(X_837,cons(Z,Xs)),var(suc(zero)),arr(X_839,X_840)),eq(X_837,X_839))) )],[refute_0_57,refute_0_73]) ).
cnf(refute_0_75,plain,
tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_1779),arr(a,b)) = andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),
inference(subst,[],[refute_0_74:[bind(Xs,$fot(nil)),bind(Z,$fot(arr(a,arr(a,b)))),bind(X_837,$fot(a)),bind(X_839,$fot(X_1779)),bind(X_840,$fot(arr(a,b)))]]) ).
cnf(refute_0_76,plain,
( sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))) != notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_1779),arr(a,b)),btrue)))
| tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_1779),arr(a,b)) != andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779))
| sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))) = notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))),notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_1779),arr(a,b)),btrue)))) ),[1,0,1,0],$fot(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)))]]) ).
cnf(refute_0_77,plain,
( sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))) != notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_1779),arr(a,b)),btrue)))
| sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))) = notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))) ),
inference(resolve,[$cnf( $equal(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_1779),arr(a,b)),andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779))) )],[refute_0_75,refute_0_76]) ).
cnf(refute_0_78,plain,
sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))) = notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))),
inference(resolve,[$cnf( $equal(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))),notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_1779),arr(a,b)),btrue)))) )],[refute_0_56,refute_0_77]) ).
cnf(refute_0_79,plain,
andb(btrue,andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) = andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue),
inference(subst,[],[axiom_007:[bind(Q,$fot(andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))]]) ).
cnf(refute_0_80,plain,
andb(btrue,btrue) = btrue,
inference(subst,[],[axiom_007:[bind(Q,$fot(btrue))]]) ).
cnf(refute_0_81,plain,
nf(var(zero)) = btrue,
inference(subst,[],[axiom_013:[bind(X4,$fot(zero))]]) ).
cnf(refute_0_82,plain,
andb(btrue,nf(var(zero))) = andb(btrue,nf(var(zero))),
introduced(tautology,[refl,[$fot(andb(btrue,nf(var(zero))))]]) ).
cnf(refute_0_83,plain,
( andb(btrue,nf(var(zero))) != andb(btrue,nf(var(zero)))
| nf(var(zero)) != btrue
| andb(btrue,nf(var(zero))) = andb(btrue,btrue) ),
introduced(tautology,[equality,[$cnf( $equal(andb(btrue,nf(var(zero))),andb(btrue,nf(var(zero)))) ),[1,1],$fot(btrue)]]) ).
cnf(refute_0_84,plain,
( nf(var(zero)) != btrue
| andb(btrue,nf(var(zero))) = andb(btrue,btrue) ),
inference(resolve,[$cnf( $equal(andb(btrue,nf(var(zero))),andb(btrue,nf(var(zero)))) )],[refute_0_82,refute_0_83]) ).
cnf(refute_0_85,plain,
andb(btrue,nf(var(zero))) = andb(btrue,btrue),
inference(resolve,[$cnf( $equal(nf(var(zero)),btrue) )],[refute_0_81,refute_0_84]) ).
cnf(refute_0_86,plain,
andb(nf(var(zero)),nf(var(zero))) = andb(nf(var(zero)),nf(var(zero))),
introduced(tautology,[refl,[$fot(andb(nf(var(zero)),nf(var(zero))))]]) ).
cnf(refute_0_87,plain,
( andb(nf(var(zero)),nf(var(zero))) != andb(nf(var(zero)),nf(var(zero)))
| nf(var(zero)) != btrue
| andb(nf(var(zero)),nf(var(zero))) = andb(btrue,nf(var(zero))) ),
introduced(tautology,[equality,[$cnf( $equal(andb(nf(var(zero)),nf(var(zero))),andb(nf(var(zero)),nf(var(zero)))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_88,plain,
( nf(var(zero)) != btrue
| andb(nf(var(zero)),nf(var(zero))) = andb(btrue,nf(var(zero))) ),
inference(resolve,[$cnf( $equal(andb(nf(var(zero)),nf(var(zero))),andb(nf(var(zero)),nf(var(zero)))) )],[refute_0_86,refute_0_87]) ).
cnf(refute_0_89,plain,
andb(nf(var(zero)),nf(var(zero))) = andb(btrue,nf(var(zero))),
inference(resolve,[$cnf( $equal(nf(var(zero)),btrue) )],[refute_0_81,refute_0_88]) ).
cnf(refute_0_90,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_91,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_92,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_90,refute_0_91]) ).
cnf(refute_0_93,plain,
( Y0 != X0
| Y0 != Z0
| X0 = Z0 ),
introduced(tautology,[equality,[$cnf( $equal(Y0,Z0) ),[0],$fot(X0)]]) ).
cnf(refute_0_94,plain,
( X0 != Y0
| Y0 != Z0
| X0 = Z0 ),
inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_92,refute_0_93]) ).
cnf(refute_0_95,plain,
( andb(btrue,nf(var(zero))) != andb(btrue,btrue)
| andb(nf(var(zero)),nf(var(zero))) != andb(btrue,nf(var(zero)))
| andb(nf(var(zero)),nf(var(zero))) = andb(btrue,btrue) ),
inference(subst,[],[refute_0_94:[bind(X0,$fot(andb(nf(var(zero)),nf(var(zero))))),bind(Y0,$fot(andb(btrue,nf(var(zero))))),bind(Z0,$fot(andb(btrue,btrue)))]]) ).
cnf(refute_0_96,plain,
( andb(btrue,nf(var(zero))) != andb(btrue,btrue)
| andb(nf(var(zero)),nf(var(zero))) = andb(btrue,btrue) ),
inference(resolve,[$cnf( $equal(andb(nf(var(zero)),nf(var(zero))),andb(btrue,nf(var(zero)))) )],[refute_0_89,refute_0_95]) ).
cnf(refute_0_97,plain,
andb(nf(var(zero)),nf(var(zero))) = andb(btrue,btrue),
inference(resolve,[$cnf( $equal(andb(btrue,nf(var(zero))),andb(btrue,btrue)) )],[refute_0_85,refute_0_96]) ).
cnf(refute_0_98,plain,
( andb(btrue,btrue) != btrue
| andb(nf(var(zero)),nf(var(zero))) != andb(btrue,btrue)
| andb(nf(var(zero)),nf(var(zero))) = btrue ),
inference(subst,[],[refute_0_94:[bind(X0,$fot(andb(nf(var(zero)),nf(var(zero))))),bind(Y0,$fot(andb(btrue,btrue))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_99,plain,
( andb(btrue,btrue) != btrue
| andb(nf(var(zero)),nf(var(zero))) = btrue ),
inference(resolve,[$cnf( $equal(andb(nf(var(zero)),nf(var(zero))),andb(btrue,btrue)) )],[refute_0_97,refute_0_98]) ).
cnf(refute_0_100,plain,
andb(nf(var(zero)),nf(var(zero))) = btrue,
inference(resolve,[$cnf( $equal(andb(btrue,btrue),btrue) )],[refute_0_80,refute_0_99]) ).
cnf(refute_0_101,plain,
nf(app(app(var(X),X_118,X_119),X_120,X_117)) = andb(nf(app(var(X),X_118,X_119)),nf(X_120)),
inference(subst,[],[axiom_010:[bind(X,$fot(var(X))),bind(X2,$fot(X_117)),bind(X3,$fot(X_118)),bind(X4,$fot(X_119)),bind(Z,$fot(X_120))]]) ).
cnf(refute_0_102,plain,
andb(btrue,nf(Z)) = nf(Z),
inference(subst,[],[axiom_007:[bind(Q,$fot(nf(Z)))]]) ).
cnf(refute_0_103,plain,
nf(var(X)) = btrue,
inference(subst,[],[axiom_013:[bind(X4,$fot(X))]]) ).
cnf(refute_0_104,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_105,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_106,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_104,refute_0_105]) ).
cnf(refute_0_107,plain,
andb(nf(var(X)),nf(Z)) = andb(btrue,nf(Z)),
inference(resolve,[$cnf( $equal(nf(var(X)),btrue) )],[refute_0_103,refute_0_106]) ).
cnf(refute_0_108,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_94:[bind(X0,$fot(andb(nf(var(X)),nf(Z)))),bind(Y0,$fot(andb(btrue,nf(Z)))),bind(Z0,$fot(nf(Z)))]]) ).
cnf(refute_0_109,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_107,refute_0_108]) ).
cnf(refute_0_110,plain,
andb(nf(var(X)),nf(Z)) = nf(Z),
inference(resolve,[$cnf( $equal(andb(btrue,nf(Z)),nf(Z)) )],[refute_0_102,refute_0_109]) ).
cnf(refute_0_111,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_112,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_110,refute_0_111]) ).
cnf(refute_0_113,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_112]) ).
cnf(refute_0_114,plain,
nf(app(var(X),X_118,X_119)) = nf(X_118),
inference(subst,[],[refute_0_113:[bind(X2,$fot(X_119)),bind(Z,$fot(X_118))]]) ).
cnf(refute_0_115,plain,
( nf(app(app(var(X),X_118,X_119),X_120,X_117)) != andb(nf(app(var(X),X_118,X_119)),nf(X_120))
| nf(app(var(X),X_118,X_119)) != nf(X_118)
| nf(app(app(var(X),X_118,X_119),X_120,X_117)) = andb(nf(X_118),nf(X_120)) ),
introduced(tautology,[equality,[$cnf( $equal(nf(app(app(var(X),X_118,X_119),X_120,X_117)),andb(nf(app(var(X),X_118,X_119)),nf(X_120))) ),[1,0],$fot(nf(X_118))]]) ).
cnf(refute_0_116,plain,
( nf(app(app(var(X),X_118,X_119),X_120,X_117)) != andb(nf(app(var(X),X_118,X_119)),nf(X_120))
| nf(app(app(var(X),X_118,X_119),X_120,X_117)) = andb(nf(X_118),nf(X_120)) ),
inference(resolve,[$cnf( $equal(nf(app(var(X),X_118,X_119)),nf(X_118)) )],[refute_0_114,refute_0_115]) ).
cnf(refute_0_117,plain,
nf(app(app(var(X),X_118,X_119),X_120,X_117)) = andb(nf(X_118),nf(X_120)),
inference(resolve,[$cnf( $equal(nf(app(app(var(X),X_118,X_119),X_120,X_117)),andb(nf(app(var(X),X_118,X_119)),nf(X_120))) )],[refute_0_101,refute_0_116]) ).
cnf(refute_0_118,plain,
nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)) = andb(nf(var(zero)),nf(var(zero))),
inference(subst,[],[refute_0_117:[bind(X,$fot(suc(zero))),bind(X_117,$fot(a)),bind(X_118,$fot(var(zero))),bind(X_119,$fot(X_1779)),bind(X_120,$fot(var(zero)))]]) ).
cnf(refute_0_119,plain,
( andb(nf(var(zero)),nf(var(zero))) != btrue
| nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)) != andb(nf(var(zero)),nf(var(zero)))
| nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)) = btrue ),
inference(subst,[],[refute_0_94:[bind(X0,$fot(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))),bind(Y0,$fot(andb(nf(var(zero)),nf(var(zero))))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_120,plain,
( andb(nf(var(zero)),nf(var(zero))) != btrue
| nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)) = btrue ),
inference(resolve,[$cnf( $equal(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(nf(var(zero)),nf(var(zero)))) )],[refute_0_118,refute_0_119]) ).
cnf(refute_0_121,plain,
nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)) = btrue,
inference(resolve,[$cnf( $equal(andb(nf(var(zero)),nf(var(zero))),btrue) )],[refute_0_100,refute_0_120]) ).
cnf(refute_0_122,plain,
andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) = andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)),
introduced(tautology,[refl,[$fot(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))]]) ).
cnf(refute_0_123,plain,
( andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) != andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))
| nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)) != btrue
| andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) = andb(btrue,andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) ),
introduced(tautology,[equality,[$cnf( $equal(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)),andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_124,plain,
( nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)) != btrue
| andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) = andb(btrue,andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) ),
inference(resolve,[$cnf( $equal(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)),andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))) )],[refute_0_122,refute_0_123]) ).
cnf(refute_0_125,plain,
andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) = andb(btrue,andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)),
inference(resolve,[$cnf( $equal(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),btrue) )],[refute_0_121,refute_0_124]) ).
cnf(refute_0_126,plain,
( andb(btrue,andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) != andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)
| andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) != andb(btrue,andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))
| andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) = andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue) ),
inference(subst,[],[refute_0_94:[bind(X0,$fot(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))),bind(Y0,$fot(andb(btrue,andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))),bind(Z0,$fot(andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))]]) ).
cnf(refute_0_127,plain,
( andb(btrue,andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) != andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)
| andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) = andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue) ),
inference(resolve,[$cnf( $equal(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)),andb(btrue,andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))) )],[refute_0_125,refute_0_126]) ).
cnf(refute_0_128,plain,
andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) = andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue),
inference(resolve,[$cnf( $equal(andb(btrue,andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) )],[refute_0_79,refute_0_127]) ).
cnf(refute_0_129,plain,
notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))) = notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))),
introduced(tautology,[refl,[$fot(notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))))]]) ).
cnf(refute_0_130,plain,
( andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) != andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)
| notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))) != notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))
| notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) ),
introduced(tautology,[equality,[$cnf( $equal(notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))),notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))) ),[1,0],$fot(andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))]]) ).
cnf(refute_0_131,plain,
( andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) != andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)
| notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) ),
inference(resolve,[$cnf( $equal(notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))),notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))) )],[refute_0_129,refute_0_130]) ).
cnf(refute_0_132,plain,
notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)),
inference(resolve,[$cnf( $equal(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) )],[refute_0_128,refute_0_131]) ).
cnf(refute_0_133,plain,
( notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))) != notb(andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))
| sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))) != notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))
| sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))),notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))) ),[1],$fot(notb(andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))]]) ).
cnf(refute_0_134,plain,
( sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))) != notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))
| sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)) ),
inference(resolve,[$cnf( $equal(notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))),notb(andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue))) )],[refute_0_132,refute_0_133]) ).
cnf(refute_0_135,plain,
sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)),
inference(resolve,[$cnf( $equal(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)))),notb(andb(nf(app(app(var(suc(zero)),var(zero),X_1779),var(zero),a)),andb(andb(eq(arr(a,arr(a,b)),arr(X_1779,arr(a,b))),eq(a,X_1779)),btrue)))) )],[refute_0_78,refute_0_134]) ).
cnf(refute_0_136,plain,
sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),eq(a,a)),btrue)),
inference(subst,[],[refute_0_135:[bind(X_1779,$fot(a))]]) ).
cnf(refute_0_137,plain,
eq(a,a) = btrue,
inference(subst,[],[axiom_051:[bind(X,$fot(a))]]) ).
cnf(refute_0_138,plain,
( eq(a,a) != btrue
| sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) != notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),eq(a,a)),btrue))
| sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),eq(a,a)),btrue))) ),[1,0,0,1],$fot(btrue)]]) ).
cnf(refute_0_139,plain,
( sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) != notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),eq(a,a)),btrue))
| sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) ),
inference(resolve,[$cnf( $equal(eq(a,a),btrue) )],[refute_0_137,refute_0_138]) ).
cnf(refute_0_140,plain,
sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)),
inference(resolve,[$cnf( $equal(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),eq(a,a)),btrue))) )],[refute_0_136,refute_0_139]) ).
cnf(refute_0_141,plain,
eq(b,b) = btrue,
inference(subst,[],[axiom_051:[bind(X,$fot(b))]]) ).
cnf(refute_0_142,plain,
( eq(X_1032,X_1032) != btrue
| eq(arr(X_1032,X_1031),arr(X_1032,X_1030)) = eq(X_1031,X_1030) ),
inference(subst,[],[axiom_033:[bind(X,$fot(X_1032)),bind(X2,$fot(X_1030)),bind(Y,$fot(X_1031)),bind(Z,$fot(X_1032))]]) ).
cnf(refute_0_143,plain,
eq(X_1032,X_1032) = btrue,
inference(subst,[],[axiom_051:[bind(X,$fot(X_1032))]]) ).
cnf(refute_0_144,plain,
( btrue != btrue
| eq(X_1032,X_1032) != btrue
| eq(X_1032,X_1032) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(eq(X_1032,X_1032),btrue) ),[1],$fot(btrue)]]) ).
cnf(refute_0_145,plain,
( btrue != btrue
| eq(X_1032,X_1032) = btrue ),
inference(resolve,[$cnf( $equal(eq(X_1032,X_1032),btrue) )],[refute_0_143,refute_0_144]) ).
cnf(refute_0_146,plain,
( btrue != btrue
| eq(arr(X_1032,X_1031),arr(X_1032,X_1030)) = eq(X_1031,X_1030) ),
inference(resolve,[$cnf( $equal(eq(X_1032,X_1032),btrue) )],[refute_0_145,refute_0_142]) ).
cnf(refute_0_147,plain,
btrue = btrue,
introduced(tautology,[refl,[$fot(btrue)]]) ).
cnf(refute_0_148,plain,
eq(arr(X_1032,X_1031),arr(X_1032,X_1030)) = eq(X_1031,X_1030),
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_147,refute_0_146]) ).
cnf(refute_0_149,plain,
eq(arr(a,b),arr(a,b)) = eq(b,b),
inference(subst,[],[refute_0_148:[bind(X_1030,$fot(b)),bind(X_1031,$fot(b)),bind(X_1032,$fot(a))]]) ).
cnf(refute_0_150,plain,
( eq(arr(a,b),arr(a,b)) != eq(b,b)
| eq(b,b) != btrue
| eq(arr(a,b),arr(a,b)) = btrue ),
inference(subst,[],[refute_0_94:[bind(X0,$fot(eq(arr(a,b),arr(a,b)))),bind(Y0,$fot(eq(b,b))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_151,plain,
( eq(b,b) != btrue
| eq(arr(a,b),arr(a,b)) = btrue ),
inference(resolve,[$cnf( $equal(eq(arr(a,b),arr(a,b)),eq(b,b)) )],[refute_0_149,refute_0_150]) ).
cnf(refute_0_152,plain,
eq(arr(a,b),arr(a,b)) = btrue,
inference(resolve,[$cnf( $equal(eq(b,b),btrue) )],[refute_0_141,refute_0_151]) ).
cnf(refute_0_153,plain,
eq(arr(a,arr(a,b)),arr(a,arr(a,b))) = eq(arr(a,b),arr(a,b)),
inference(subst,[],[refute_0_148:[bind(X_1030,$fot(arr(a,b))),bind(X_1031,$fot(arr(a,b))),bind(X_1032,$fot(a))]]) ).
cnf(refute_0_154,plain,
( eq(arr(a,arr(a,b)),arr(a,arr(a,b))) != eq(arr(a,b),arr(a,b))
| eq(arr(a,b),arr(a,b)) != btrue
| eq(arr(a,arr(a,b)),arr(a,arr(a,b))) = btrue ),
inference(subst,[],[refute_0_94:[bind(X0,$fot(eq(arr(a,arr(a,b)),arr(a,arr(a,b))))),bind(Y0,$fot(eq(arr(a,b),arr(a,b)))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_155,plain,
( eq(arr(a,b),arr(a,b)) != btrue
| eq(arr(a,arr(a,b)),arr(a,arr(a,b))) = btrue ),
inference(resolve,[$cnf( $equal(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),eq(arr(a,b),arr(a,b))) )],[refute_0_153,refute_0_154]) ).
cnf(refute_0_156,plain,
eq(arr(a,arr(a,b)),arr(a,arr(a,b))) = btrue,
inference(resolve,[$cnf( $equal(eq(arr(a,b),arr(a,b)),btrue) )],[refute_0_152,refute_0_155]) ).
cnf(refute_0_157,plain,
andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue) = andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),
introduced(tautology,[refl,[$fot(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue))]]) ).
cnf(refute_0_158,plain,
( andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue) != andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue)
| eq(arr(a,arr(a,b)),arr(a,arr(a,b))) != btrue
| andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue) = andb(btrue,btrue) ),
introduced(tautology,[equality,[$cnf( $equal(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue)) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_159,plain,
( eq(arr(a,arr(a,b)),arr(a,arr(a,b))) != btrue
| andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue) = andb(btrue,btrue) ),
inference(resolve,[$cnf( $equal(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue)) )],[refute_0_157,refute_0_158]) ).
cnf(refute_0_160,plain,
andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue) = andb(btrue,btrue),
inference(resolve,[$cnf( $equal(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue) )],[refute_0_156,refute_0_159]) ).
cnf(refute_0_161,plain,
( andb(btrue,btrue) != btrue
| andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue) != andb(btrue,btrue)
| andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue) = btrue ),
inference(subst,[],[refute_0_94:[bind(X0,$fot(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue))),bind(Y0,$fot(andb(btrue,btrue))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_162,plain,
( andb(btrue,btrue) != btrue
| andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue) = btrue ),
inference(resolve,[$cnf( $equal(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),andb(btrue,btrue)) )],[refute_0_160,refute_0_161]) ).
cnf(refute_0_163,plain,
andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue) = btrue,
inference(resolve,[$cnf( $equal(andb(btrue,btrue),btrue) )],[refute_0_80,refute_0_162]) ).
cnf(refute_0_164,plain,
andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue) = andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue),
introduced(tautology,[refl,[$fot(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue))]]) ).
cnf(refute_0_165,plain,
( andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue) != andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)
| andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue) != btrue
| andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue) = andb(btrue,btrue) ),
introduced(tautology,[equality,[$cnf( $equal(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue),andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_166,plain,
( andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue) != btrue
| andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue) = andb(btrue,btrue) ),
inference(resolve,[$cnf( $equal(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue),andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) )],[refute_0_164,refute_0_165]) ).
cnf(refute_0_167,plain,
andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue) = andb(btrue,btrue),
inference(resolve,[$cnf( $equal(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue) )],[refute_0_163,refute_0_166]) ).
cnf(refute_0_168,plain,
( andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue) != andb(btrue,btrue)
| andb(btrue,btrue) != btrue
| andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue) = btrue ),
inference(subst,[],[refute_0_94:[bind(X0,$fot(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue))),bind(Y0,$fot(andb(btrue,btrue))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_169,plain,
( andb(btrue,btrue) != btrue
| andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue) = btrue ),
inference(resolve,[$cnf( $equal(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue),andb(btrue,btrue)) )],[refute_0_167,refute_0_168]) ).
cnf(refute_0_170,plain,
andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue) = btrue,
inference(resolve,[$cnf( $equal(andb(btrue,btrue),btrue) )],[refute_0_80,refute_0_169]) ).
cnf(refute_0_171,plain,
notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)),
introduced(tautology,[refl,[$fot(notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)))]]) ).
cnf(refute_0_172,plain,
( andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue) != btrue
| notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) != notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue))
| notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) = notb(btrue) ),
introduced(tautology,[equality,[$cnf( $equal(notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)),notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_173,plain,
( andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue) != btrue
| notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) = notb(btrue) ),
inference(resolve,[$cnf( $equal(notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)),notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue))) )],[refute_0_171,refute_0_172]) ).
cnf(refute_0_174,plain,
notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) = notb(btrue),
inference(resolve,[$cnf( $equal(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue),btrue) )],[refute_0_170,refute_0_173]) ).
cnf(refute_0_175,plain,
( notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) != notb(btrue)
| notb(btrue) != bfalse
| notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) = bfalse ),
inference(subst,[],[refute_0_94:[bind(X0,$fot(notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)))),bind(Y0,$fot(notb(btrue))),bind(Z0,$fot(bfalse))]]) ).
cnf(refute_0_176,plain,
( notb(btrue) != bfalse
| notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) = bfalse ),
inference(resolve,[$cnf( $equal(notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)),notb(btrue)) )],[refute_0_174,refute_0_175]) ).
cnf(refute_0_177,plain,
notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) = bfalse,
inference(resolve,[$cnf( $equal(notb(btrue),bfalse) )],[axiom_002,refute_0_176]) ).
cnf(refute_0_178,plain,
( notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) != bfalse
| sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) != notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue))
| sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue))) ),[1],$fot(bfalse)]]) ).
cnf(refute_0_179,plain,
( sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) != notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue))
| sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) = bfalse ),
inference(resolve,[$cnf( $equal(notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)),bfalse) )],[refute_0_177,refute_0_178]) ).
cnf(refute_0_180,plain,
sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) = bfalse,
inference(resolve,[$cnf( $equal(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue))) )],[refute_0_140,refute_0_179]) ).
cnf(refute_0_181,plain,
( eq4(bfalse,bfalse) != btrue
| sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) != bfalse
| eq4(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( ~ $equal(eq4(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),bfalse),btrue) ),[0,0],$fot(bfalse)]]) ).
cnf(refute_0_182,plain,
( eq4(bfalse,bfalse) != btrue
| eq4(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),bfalse) = btrue ),
inference(resolve,[$cnf( $equal(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),bfalse) )],[refute_0_180,refute_0_181]) ).
cnf(refute_0_183,plain,
eq4(bfalse,bfalse) != btrue,
inference(resolve,[$cnf( $equal(eq4(sat_synth_nf_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),bfalse),btrue) )],[refute_0_182,refute_0_0]) ).
cnf(refute_0_184,plain,
eq4(bfalse,bfalse) = btrue,
inference(subst,[],[axiom_054:[bind(X,$fot(bfalse))]]) ).
cnf(refute_0_185,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_186,plain,
( btrue != btrue
| eq4(bfalse,bfalse) = btrue ),
inference(resolve,[$cnf( $equal(eq4(bfalse,bfalse),btrue) )],[refute_0_184,refute_0_185]) ).
cnf(refute_0_187,plain,
btrue != btrue,
inference(resolve,[$cnf( $equal(eq4(bfalse,bfalse),btrue) )],[refute_0_186,refute_0_183]) ).
cnf(refute_0_188,plain,
$false,
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_147,refute_0_187]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX223-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : metis --show proof --show saturation %s
% 0.18/0.34 % Computer : n021.cluster.edu
% 0.18/0.34 % Model : x86_64 x86_64
% 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34 % Memory : 8042.1875MB
% 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34 % CPULimit : 300
% 0.18/0.34 % WCLimit : 300
% 0.18/0.34 % DateTime : Tue May 5 12:38:25 EDT 2026
% 0.18/0.34 % CPUTime :
% 0.18/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 4.86/5.08 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.86/5.08
% 4.86/5.08 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 4.86/5.11
%------------------------------------------------------------------------------