%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWX224-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n024.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:37 PM UTC 2026
% Result : Unsatisfiable 11.62s 11.89s
% Output : CNFRefutation 11.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 40
% Syntax : Number of clauses : 129 ( 72 unt; 0 nHn; 80 RR)
% Number of literals : 214 ( 213 equ; 89 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 : 21 ( 21 usr; 6 con; 0-4 aty)
% Number of variables : 213 ( 16 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_009,axiom,
tc(X,app(F,X2,Tx),Z) = andb(tc(X,F,arr(Tx,Z)),tc(X,X2,Tx)) ).
cnf(axiom_010,axiom,
tc(X,lam(E),arr(Tx2,T1)) = tc(cons(Tx2,X),E,T1) ).
cnf(axiom_014,axiom,
tc(X,var(X3),Z) = aux(X,Z,X3,index(X,X3)) ).
cnf(axiom_015,axiom,
sat_synth_w(X) = notb(tc(nil,X,arr(arr(a,arr(a,b)),arr(a,b)))) ).
cnf(axiom_028,axiom,
( eq(X,Z) != btrue
| eq(arr(X,Y),arr(Z,X2)) = eq(Y,X2) ) ).
cnf(axiom_046,axiom,
eq(X,X) = btrue ).
cnf(axiom_049,axiom,
eq4(X,X) = btrue ).
cnf(goal,negated_conjecture,
eq4(sat_synth_w(X),bfalse) != btrue ).
cnf(refute_0_0,plain,
eq4(sat_synth_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_w(lam(X_87)) = notb(tc(nil,lam(X_87),arr(arr(a,arr(a,b)),arr(a,b)))),
inference(subst,[],[axiom_015:[bind(X,$fot(lam(X_87)))]]) ).
cnf(refute_0_2,plain,
tc(nil,lam(X_87),arr(arr(a,arr(a,b)),arr(a,b))) = tc(cons(arr(a,arr(a,b)),nil),X_87,arr(a,b)),
inference(subst,[],[axiom_010:[bind(E,$fot(X_87)),bind(T1,$fot(arr(a,b))),bind(Tx2,$fot(arr(a,arr(a,b)))),bind(X,$fot(nil))]]) ).
cnf(refute_0_3,plain,
( sat_synth_w(lam(X_87)) != notb(tc(nil,lam(X_87),arr(arr(a,arr(a,b)),arr(a,b))))
| tc(nil,lam(X_87),arr(arr(a,arr(a,b)),arr(a,b))) != tc(cons(arr(a,arr(a,b)),nil),X_87,arr(a,b))
| sat_synth_w(lam(X_87)) = notb(tc(cons(arr(a,arr(a,b)),nil),X_87,arr(a,b))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_w(lam(X_87)),notb(tc(nil,lam(X_87),arr(arr(a,arr(a,b)),arr(a,b))))) ),[1,0],$fot(tc(cons(arr(a,arr(a,b)),nil),X_87,arr(a,b)))]]) ).
cnf(refute_0_4,plain,
( sat_synth_w(lam(X_87)) != notb(tc(nil,lam(X_87),arr(arr(a,arr(a,b)),arr(a,b))))
| sat_synth_w(lam(X_87)) = notb(tc(cons(arr(a,arr(a,b)),nil),X_87,arr(a,b))) ),
inference(resolve,[$cnf( $equal(tc(nil,lam(X_87),arr(arr(a,arr(a,b)),arr(a,b))),tc(cons(arr(a,arr(a,b)),nil),X_87,arr(a,b))) )],[refute_0_2,refute_0_3]) ).
cnf(refute_0_5,plain,
sat_synth_w(lam(X_87)) = notb(tc(cons(arr(a,arr(a,b)),nil),X_87,arr(a,b))),
inference(resolve,[$cnf( $equal(sat_synth_w(lam(X_87)),notb(tc(nil,lam(X_87),arr(arr(a,arr(a,b)),arr(a,b))))) )],[refute_0_1,refute_0_4]) ).
cnf(refute_0_6,plain,
sat_synth_w(lam(lam(E))) = notb(tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b))),
inference(subst,[],[refute_0_5:[bind(X_87,$fot(lam(E)))]]) ).
cnf(refute_0_7,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_010:[bind(T1,$fot(b)),bind(Tx2,$fot(a)),bind(X,$fot(cons(arr(a,arr(a,b)),nil)))]]) ).
cnf(refute_0_8,plain,
( sat_synth_w(lam(lam(E))) != notb(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)
| sat_synth_w(lam(lam(E))) = notb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b)) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_w(lam(lam(E))),notb(tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))) ),[1,0],$fot(tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b))]]) ).
cnf(refute_0_9,plain,
( sat_synth_w(lam(lam(E))) != notb(tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))
| sat_synth_w(lam(lam(E))) = notb(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_7,refute_0_8]) ).
cnf(refute_0_10,plain,
sat_synth_w(lam(lam(E))) = notb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),E,b)),
inference(resolve,[$cnf( $equal(sat_synth_w(lam(lam(E))),notb(tc(cons(arr(a,arr(a,b)),nil),lam(E),arr(a,b)))) )],[refute_0_6,refute_0_9]) ).
cnf(refute_0_11,plain,
sat_synth_w(lam(lam(app(X_1372,var(zero),a)))) = notb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_1372,var(zero),a),b)),
inference(subst,[],[refute_0_10:[bind(E,$fot(app(X_1372,var(zero),a)))]]) ).
cnf(refute_0_12,plain,
tc(cons(Z,Xs),app(X_110,var(zero),X_111),X_114) = andb(tc(cons(Z,Xs),X_110,arr(X_111,X_114)),tc(cons(Z,Xs),var(zero),X_111)),
inference(subst,[],[axiom_009:[bind(F,$fot(X_110)),bind(Tx,$fot(X_111)),bind(X,$fot(cons(Z,Xs))),bind(X2,$fot(var(zero))),bind(Z,$fot(X_114))]]) ).
cnf(refute_0_13,plain,
tc(cons(Z,Xs),var(zero),X_58) = aux(cons(Z,Xs),X_58,zero,index(cons(Z,Xs),zero)),
inference(subst,[],[axiom_014:[bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(zero)),bind(Z,$fot(X_58))]]) ).
cnf(refute_0_14,plain,
( index(cons(Z,Xs),zero) != just(Z)
| tc(cons(Z,Xs),var(zero),X_58) != aux(cons(Z,Xs),X_58,zero,index(cons(Z,Xs),zero))
| tc(cons(Z,Xs),var(zero),X_58) = aux(cons(Z,Xs),X_58,zero,just(Z)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_58),aux(cons(Z,Xs),X_58,zero,index(cons(Z,Xs),zero))) ),[1,3],$fot(just(Z))]]) ).
cnf(refute_0_15,plain,
( tc(cons(Z,Xs),var(zero),X_58) != aux(cons(Z,Xs),X_58,zero,index(cons(Z,Xs),zero))
| tc(cons(Z,Xs),var(zero),X_58) = aux(cons(Z,Xs),X_58,zero,just(Z)) ),
inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(Z)) )],[axiom_005,refute_0_14]) ).
cnf(refute_0_16,plain,
tc(cons(Z,Xs),var(zero),X_58) = aux(cons(Z,Xs),X_58,zero,just(Z)),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_58),aux(cons(Z,Xs),X_58,zero,index(cons(Z,Xs),zero))) )],[refute_0_13,refute_0_15]) ).
cnf(refute_0_17,plain,
aux(cons(Z,Xs),X_58,zero,just(Z)) = eq(Z,X_58),
inference(subst,[],[axiom_001:[bind(Tx3,$fot(Z)),bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(zero)),bind(Z,$fot(X_58))]]) ).
cnf(refute_0_18,plain,
( aux(cons(Z,Xs),X_58,zero,just(Z)) != eq(Z,X_58)
| tc(cons(Z,Xs),var(zero),X_58) != aux(cons(Z,Xs),X_58,zero,just(Z))
| tc(cons(Z,Xs),var(zero),X_58) = eq(Z,X_58) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_58),aux(cons(Z,Xs),X_58,zero,just(Z))) ),[1],$fot(eq(Z,X_58))]]) ).
cnf(refute_0_19,plain,
( tc(cons(Z,Xs),var(zero),X_58) != aux(cons(Z,Xs),X_58,zero,just(Z))
| tc(cons(Z,Xs),var(zero),X_58) = eq(Z,X_58) ),
inference(resolve,[$cnf( $equal(aux(cons(Z,Xs),X_58,zero,just(Z)),eq(Z,X_58)) )],[refute_0_17,refute_0_18]) ).
cnf(refute_0_20,plain,
tc(cons(Z,Xs),var(zero),X_58) = eq(Z,X_58),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_58),aux(cons(Z,Xs),X_58,zero,just(Z))) )],[refute_0_16,refute_0_19]) ).
cnf(refute_0_21,plain,
tc(cons(Z,Xs),var(zero),X_111) = eq(Z,X_111),
inference(subst,[],[refute_0_20:[bind(X_58,$fot(X_111))]]) ).
cnf(refute_0_22,plain,
( tc(cons(Z,Xs),app(X_110,var(zero),X_111),X_114) != andb(tc(cons(Z,Xs),X_110,arr(X_111,X_114)),tc(cons(Z,Xs),var(zero),X_111))
| tc(cons(Z,Xs),var(zero),X_111) != eq(Z,X_111)
| tc(cons(Z,Xs),app(X_110,var(zero),X_111),X_114) = andb(tc(cons(Z,Xs),X_110,arr(X_111,X_114)),eq(Z,X_111)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),app(X_110,var(zero),X_111),X_114),andb(tc(cons(Z,Xs),X_110,arr(X_111,X_114)),tc(cons(Z,Xs),var(zero),X_111))) ),[1,1],$fot(eq(Z,X_111))]]) ).
cnf(refute_0_23,plain,
( tc(cons(Z,Xs),app(X_110,var(zero),X_111),X_114) != andb(tc(cons(Z,Xs),X_110,arr(X_111,X_114)),tc(cons(Z,Xs),var(zero),X_111))
| tc(cons(Z,Xs),app(X_110,var(zero),X_111),X_114) = andb(tc(cons(Z,Xs),X_110,arr(X_111,X_114)),eq(Z,X_111)) ),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_111),eq(Z,X_111)) )],[refute_0_21,refute_0_22]) ).
cnf(refute_0_24,plain,
tc(cons(Z,Xs),app(X_110,var(zero),X_111),X_114) = andb(tc(cons(Z,Xs),X_110,arr(X_111,X_114)),eq(Z,X_111)),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),app(X_110,var(zero),X_111),X_114),andb(tc(cons(Z,Xs),X_110,arr(X_111,X_114)),tc(cons(Z,Xs),var(zero),X_111))) )],[refute_0_12,refute_0_23]) ).
cnf(refute_0_25,plain,
tc(cons(X_1330,X_1327),app(X_1329,var(zero),X_1330),X_1331) = andb(tc(cons(X_1330,X_1327),X_1329,arr(X_1330,X_1331)),eq(X_1330,X_1330)),
inference(subst,[],[refute_0_24:[bind(Xs,$fot(X_1327)),bind(Z,$fot(X_1330)),bind(X_110,$fot(X_1329)),bind(X_111,$fot(X_1330)),bind(X_114,$fot(X_1331))]]) ).
cnf(refute_0_26,plain,
eq(X_1330,X_1330) = btrue,
inference(subst,[],[axiom_046:[bind(X,$fot(X_1330))]]) ).
cnf(refute_0_27,plain,
( eq(X_1330,X_1330) != btrue
| tc(cons(X_1330,X_1327),app(X_1329,var(zero),X_1330),X_1331) != andb(tc(cons(X_1330,X_1327),X_1329,arr(X_1330,X_1331)),eq(X_1330,X_1330))
| tc(cons(X_1330,X_1327),app(X_1329,var(zero),X_1330),X_1331) = andb(tc(cons(X_1330,X_1327),X_1329,arr(X_1330,X_1331)),btrue) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_1330,X_1327),app(X_1329,var(zero),X_1330),X_1331),andb(tc(cons(X_1330,X_1327),X_1329,arr(X_1330,X_1331)),eq(X_1330,X_1330))) ),[1,1],$fot(btrue)]]) ).
cnf(refute_0_28,plain,
( tc(cons(X_1330,X_1327),app(X_1329,var(zero),X_1330),X_1331) != andb(tc(cons(X_1330,X_1327),X_1329,arr(X_1330,X_1331)),eq(X_1330,X_1330))
| tc(cons(X_1330,X_1327),app(X_1329,var(zero),X_1330),X_1331) = andb(tc(cons(X_1330,X_1327),X_1329,arr(X_1330,X_1331)),btrue) ),
inference(resolve,[$cnf( $equal(eq(X_1330,X_1330),btrue) )],[refute_0_26,refute_0_27]) ).
cnf(refute_0_29,plain,
tc(cons(X_1330,X_1327),app(X_1329,var(zero),X_1330),X_1331) = andb(tc(cons(X_1330,X_1327),X_1329,arr(X_1330,X_1331)),btrue),
inference(resolve,[$cnf( $equal(tc(cons(X_1330,X_1327),app(X_1329,var(zero),X_1330),X_1331),andb(tc(cons(X_1330,X_1327),X_1329,arr(X_1330,X_1331)),eq(X_1330,X_1330))) )],[refute_0_25,refute_0_28]) ).
cnf(refute_0_30,plain,
tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_1372,var(zero),a),b) = andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_1372,arr(a,b)),btrue),
inference(subst,[],[refute_0_29:[bind(X_1327,$fot(cons(arr(a,arr(a,b)),nil))),bind(X_1329,$fot(X_1372)),bind(X_1330,$fot(a)),bind(X_1331,$fot(b))]]) ).
cnf(refute_0_31,plain,
( sat_synth_w(lam(lam(app(X_1372,var(zero),a)))) != notb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_1372,var(zero),a),b))
| tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_1372,var(zero),a),b) != andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_1372,arr(a,b)),btrue)
| sat_synth_w(lam(lam(app(X_1372,var(zero),a)))) = notb(andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_1372,arr(a,b)),btrue)) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_w(lam(lam(app(X_1372,var(zero),a)))),notb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_1372,var(zero),a),b))) ),[1,0],$fot(andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_1372,arr(a,b)),btrue))]]) ).
cnf(refute_0_32,plain,
( sat_synth_w(lam(lam(app(X_1372,var(zero),a)))) != notb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_1372,var(zero),a),b))
| sat_synth_w(lam(lam(app(X_1372,var(zero),a)))) = notb(andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_1372,arr(a,b)),btrue)) ),
inference(resolve,[$cnf( $equal(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_1372,var(zero),a),b),andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_1372,arr(a,b)),btrue)) )],[refute_0_30,refute_0_31]) ).
cnf(refute_0_33,plain,
sat_synth_w(lam(lam(app(X_1372,var(zero),a)))) = notb(andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),X_1372,arr(a,b)),btrue)),
inference(resolve,[$cnf( $equal(sat_synth_w(lam(lam(app(X_1372,var(zero),a)))),notb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(X_1372,var(zero),a),b))) )],[refute_0_11,refute_0_32]) ).
cnf(refute_0_34,plain,
sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),X_5432),var(zero),a)))) = notb(andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_5432),arr(a,b)),btrue)),
inference(subst,[],[refute_0_33:[bind(X_1372,$fot(app(var(suc(zero)),var(zero),X_5432)))]]) ).
cnf(refute_0_35,plain,
tc(cons(X_1328,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_1330),X_1331) = andb(tc(cons(X_1328,cons(Z,Xs)),var(suc(zero)),arr(X_1330,X_1331)),eq(X_1328,X_1330)),
inference(subst,[],[refute_0_24:[bind(Xs,$fot(cons(Z,Xs))),bind(Z,$fot(X_1328)),bind(X_110,$fot(var(suc(zero)))),bind(X_111,$fot(X_1330)),bind(X_114,$fot(X_1331))]]) ).
cnf(refute_0_36,plain,
tc(cons(X_67,X_66),var(suc(X_65)),Z) = aux(cons(X_67,X_66),Z,suc(X_65),index(cons(X_67,X_66),suc(X_65))),
inference(subst,[],[axiom_014:[bind(X,$fot(cons(X_67,X_66))),bind(X3,$fot(suc(X_65)))]]) ).
cnf(refute_0_37,plain,
index(cons(X_67,X_66),suc(X_65)) = index(X_66,X_65),
inference(subst,[],[axiom_006:[bind(N,$fot(X_65)),bind(Xs,$fot(X_66)),bind(Z,$fot(X_67))]]) ).
cnf(refute_0_38,plain,
( index(cons(X_67,X_66),suc(X_65)) != index(X_66,X_65)
| tc(cons(X_67,X_66),var(suc(X_65)),Z) != aux(cons(X_67,X_66),Z,suc(X_65),index(cons(X_67,X_66),suc(X_65)))
| tc(cons(X_67,X_66),var(suc(X_65)),Z) = aux(cons(X_67,X_66),Z,suc(X_65),index(X_66,X_65)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_67,X_66),var(suc(X_65)),Z),aux(cons(X_67,X_66),Z,suc(X_65),index(cons(X_67,X_66),suc(X_65)))) ),[1,3],$fot(index(X_66,X_65))]]) ).
cnf(refute_0_39,plain,
( tc(cons(X_67,X_66),var(suc(X_65)),Z) != aux(cons(X_67,X_66),Z,suc(X_65),index(cons(X_67,X_66),suc(X_65)))
| tc(cons(X_67,X_66),var(suc(X_65)),Z) = aux(cons(X_67,X_66),Z,suc(X_65),index(X_66,X_65)) ),
inference(resolve,[$cnf( $equal(index(cons(X_67,X_66),suc(X_65)),index(X_66,X_65)) )],[refute_0_37,refute_0_38]) ).
cnf(refute_0_40,plain,
tc(cons(X_67,X_66),var(suc(X_65)),Z) = aux(cons(X_67,X_66),Z,suc(X_65),index(X_66,X_65)),
inference(resolve,[$cnf( $equal(tc(cons(X_67,X_66),var(suc(X_65)),Z),aux(cons(X_67,X_66),Z,suc(X_65),index(cons(X_67,X_66),suc(X_65)))) )],[refute_0_36,refute_0_39]) ).
cnf(refute_0_41,plain,
tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76) = aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),index(cons(Z,Xs),zero)),
inference(subst,[],[refute_0_40:[bind(Z,$fot(X_76)),bind(X_65,$fot(zero)),bind(X_66,$fot(cons(Z,Xs))),bind(X_67,$fot(X_79))]]) ).
cnf(refute_0_42,plain,
( index(cons(Z,Xs),zero) != just(Z)
| tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76) != aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),index(cons(Z,Xs),zero))
| tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76) = aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),just(Z)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76),aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),index(cons(Z,Xs),zero))) ),[1,3],$fot(just(Z))]]) ).
cnf(refute_0_43,plain,
( tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76) != aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),index(cons(Z,Xs),zero))
| tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76) = aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),just(Z)) ),
inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(Z)) )],[axiom_005,refute_0_42]) ).
cnf(refute_0_44,plain,
tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76) = aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),just(Z)),
inference(resolve,[$cnf( $equal(tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76),aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),index(cons(Z,Xs),zero))) )],[refute_0_41,refute_0_43]) ).
cnf(refute_0_45,plain,
aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),just(Z)) = eq(Z,X_76),
inference(subst,[],[axiom_001:[bind(Tx3,$fot(Z)),bind(X,$fot(cons(X_79,cons(Z,Xs)))),bind(X3,$fot(suc(zero))),bind(Z,$fot(X_76))]]) ).
cnf(refute_0_46,plain,
( aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),just(Z)) != eq(Z,X_76)
| tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76) != aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),just(Z))
| tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76) = eq(Z,X_76) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76),aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),just(Z))) ),[1],$fot(eq(Z,X_76))]]) ).
cnf(refute_0_47,plain,
( tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76) != aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),just(Z))
| tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76) = eq(Z,X_76) ),
inference(resolve,[$cnf( $equal(aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),just(Z)),eq(Z,X_76)) )],[refute_0_45,refute_0_46]) ).
cnf(refute_0_48,plain,
tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76) = eq(Z,X_76),
inference(resolve,[$cnf( $equal(tc(cons(X_79,cons(Z,Xs)),var(suc(zero)),X_76),aux(cons(X_79,cons(Z,Xs)),X_76,suc(zero),just(Z))) )],[refute_0_44,refute_0_47]) ).
cnf(refute_0_49,plain,
tc(cons(X_1328,cons(Z,Xs)),var(suc(zero)),arr(X_1330,X_1331)) = eq(Z,arr(X_1330,X_1331)),
inference(subst,[],[refute_0_48:[bind(X_76,$fot(arr(X_1330,X_1331))),bind(X_79,$fot(X_1328))]]) ).
cnf(refute_0_50,plain,
( tc(cons(X_1328,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_1330),X_1331) != andb(tc(cons(X_1328,cons(Z,Xs)),var(suc(zero)),arr(X_1330,X_1331)),eq(X_1328,X_1330))
| tc(cons(X_1328,cons(Z,Xs)),var(suc(zero)),arr(X_1330,X_1331)) != eq(Z,arr(X_1330,X_1331))
| tc(cons(X_1328,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_1330),X_1331) = andb(eq(Z,arr(X_1330,X_1331)),eq(X_1328,X_1330)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_1328,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_1330),X_1331),andb(tc(cons(X_1328,cons(Z,Xs)),var(suc(zero)),arr(X_1330,X_1331)),eq(X_1328,X_1330))) ),[1,0],$fot(eq(Z,arr(X_1330,X_1331)))]]) ).
cnf(refute_0_51,plain,
( tc(cons(X_1328,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_1330),X_1331) != andb(tc(cons(X_1328,cons(Z,Xs)),var(suc(zero)),arr(X_1330,X_1331)),eq(X_1328,X_1330))
| tc(cons(X_1328,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_1330),X_1331) = andb(eq(Z,arr(X_1330,X_1331)),eq(X_1328,X_1330)) ),
inference(resolve,[$cnf( $equal(tc(cons(X_1328,cons(Z,Xs)),var(suc(zero)),arr(X_1330,X_1331)),eq(Z,arr(X_1330,X_1331))) )],[refute_0_49,refute_0_50]) ).
cnf(refute_0_52,plain,
tc(cons(X_1328,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_1330),X_1331) = andb(eq(Z,arr(X_1330,X_1331)),eq(X_1328,X_1330)),
inference(resolve,[$cnf( $equal(tc(cons(X_1328,cons(Z,Xs)),app(var(suc(zero)),var(zero),X_1330),X_1331),andb(tc(cons(X_1328,cons(Z,Xs)),var(suc(zero)),arr(X_1330,X_1331)),eq(X_1328,X_1330))) )],[refute_0_35,refute_0_51]) ).
cnf(refute_0_53,plain,
tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_5432),arr(a,b)) = andb(eq(arr(a,arr(a,b)),arr(X_5432,arr(a,b))),eq(a,X_5432)),
inference(subst,[],[refute_0_52:[bind(Xs,$fot(nil)),bind(Z,$fot(arr(a,arr(a,b)))),bind(X_1328,$fot(a)),bind(X_1330,$fot(X_5432)),bind(X_1331,$fot(arr(a,b)))]]) ).
cnf(refute_0_54,plain,
( sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),X_5432),var(zero),a)))) != notb(andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_5432),arr(a,b)),btrue))
| tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_5432),arr(a,b)) != andb(eq(arr(a,arr(a,b)),arr(X_5432,arr(a,b))),eq(a,X_5432))
| sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),X_5432),var(zero),a)))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(X_5432,arr(a,b))),eq(a,X_5432)),btrue)) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),X_5432),var(zero),a)))),notb(andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_5432),arr(a,b)),btrue))) ),[1,0,0],$fot(andb(eq(arr(a,arr(a,b)),arr(X_5432,arr(a,b))),eq(a,X_5432)))]]) ).
cnf(refute_0_55,plain,
( sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),X_5432),var(zero),a)))) != notb(andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_5432),arr(a,b)),btrue))
| sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),X_5432),var(zero),a)))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(X_5432,arr(a,b))),eq(a,X_5432)),btrue)) ),
inference(resolve,[$cnf( $equal(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_5432),arr(a,b)),andb(eq(arr(a,arr(a,b)),arr(X_5432,arr(a,b))),eq(a,X_5432))) )],[refute_0_53,refute_0_54]) ).
cnf(refute_0_56,plain,
sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),X_5432),var(zero),a)))) = notb(andb(andb(eq(arr(a,arr(a,b)),arr(X_5432,arr(a,b))),eq(a,X_5432)),btrue)),
inference(resolve,[$cnf( $equal(sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),X_5432),var(zero),a)))),notb(andb(tc(cons(a,cons(arr(a,arr(a,b)),nil)),app(var(suc(zero)),var(zero),X_5432),arr(a,b)),btrue))) )],[refute_0_34,refute_0_55]) ).
cnf(refute_0_57,plain,
sat_synth_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_56:[bind(X_5432,$fot(a))]]) ).
cnf(refute_0_58,plain,
eq(a,a) = btrue,
inference(subst,[],[axiom_046:[bind(X,$fot(a))]]) ).
cnf(refute_0_59,plain,
( eq(a,a) != btrue
| sat_synth_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_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_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_60,plain,
( sat_synth_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_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_58,refute_0_59]) ).
cnf(refute_0_61,plain,
sat_synth_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_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_57,refute_0_60]) ).
cnf(refute_0_62,plain,
andb(btrue,btrue) = btrue,
inference(subst,[],[axiom_007:[bind(Q,$fot(btrue))]]) ).
cnf(refute_0_63,plain,
eq(b,b) = btrue,
inference(subst,[],[axiom_046:[bind(X,$fot(b))]]) ).
cnf(refute_0_64,plain,
( eq(X_1952,X_1952) != btrue
| eq(arr(X_1952,X_1951),arr(X_1952,X_1950)) = eq(X_1951,X_1950) ),
inference(subst,[],[axiom_028:[bind(X,$fot(X_1952)),bind(X2,$fot(X_1950)),bind(Y,$fot(X_1951)),bind(Z,$fot(X_1952))]]) ).
cnf(refute_0_65,plain,
eq(X_1952,X_1952) = btrue,
inference(subst,[],[axiom_046:[bind(X,$fot(X_1952))]]) ).
cnf(refute_0_66,plain,
( btrue != btrue
| eq(X_1952,X_1952) != btrue
| eq(X_1952,X_1952) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(eq(X_1952,X_1952),btrue) ),[1],$fot(btrue)]]) ).
cnf(refute_0_67,plain,
( btrue != btrue
| eq(X_1952,X_1952) = btrue ),
inference(resolve,[$cnf( $equal(eq(X_1952,X_1952),btrue) )],[refute_0_65,refute_0_66]) ).
cnf(refute_0_68,plain,
( btrue != btrue
| eq(arr(X_1952,X_1951),arr(X_1952,X_1950)) = eq(X_1951,X_1950) ),
inference(resolve,[$cnf( $equal(eq(X_1952,X_1952),btrue) )],[refute_0_67,refute_0_64]) ).
cnf(refute_0_69,plain,
btrue = btrue,
introduced(tautology,[refl,[$fot(btrue)]]) ).
cnf(refute_0_70,plain,
eq(arr(X_1952,X_1951),arr(X_1952,X_1950)) = eq(X_1951,X_1950),
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_69,refute_0_68]) ).
cnf(refute_0_71,plain,
eq(arr(a,b),arr(a,b)) = eq(b,b),
inference(subst,[],[refute_0_70:[bind(X_1950,$fot(b)),bind(X_1951,$fot(b)),bind(X_1952,$fot(a))]]) ).
cnf(refute_0_72,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_73,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_74,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_72,refute_0_73]) ).
cnf(refute_0_75,plain,
( Y0 != X0
| Y0 != Z0
| X0 = Z0 ),
introduced(tautology,[equality,[$cnf( $equal(Y0,Z0) ),[0],$fot(X0)]]) ).
cnf(refute_0_76,plain,
( X0 != Y0
| Y0 != Z0
| X0 = Z0 ),
inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_74,refute_0_75]) ).
cnf(refute_0_77,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_76:[bind(X0,$fot(eq(arr(a,b),arr(a,b)))),bind(Y0,$fot(eq(b,b))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_78,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_71,refute_0_77]) ).
cnf(refute_0_79,plain,
eq(arr(a,b),arr(a,b)) = btrue,
inference(resolve,[$cnf( $equal(eq(b,b),btrue) )],[refute_0_63,refute_0_78]) ).
cnf(refute_0_80,plain,
eq(arr(a,arr(a,b)),arr(a,arr(a,b))) = eq(arr(a,b),arr(a,b)),
inference(subst,[],[refute_0_70:[bind(X_1950,$fot(arr(a,b))),bind(X_1951,$fot(arr(a,b))),bind(X_1952,$fot(a))]]) ).
cnf(refute_0_81,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_76:[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_82,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_80,refute_0_81]) ).
cnf(refute_0_83,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_79,refute_0_82]) ).
cnf(refute_0_84,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_85,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_86,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_84,refute_0_85]) ).
cnf(refute_0_87,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_83,refute_0_86]) ).
cnf(refute_0_88,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_76:[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_89,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_87,refute_0_88]) ).
cnf(refute_0_90,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_62,refute_0_89]) ).
cnf(refute_0_91,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_92,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_93,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_91,refute_0_92]) ).
cnf(refute_0_94,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_90,refute_0_93]) ).
cnf(refute_0_95,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_76:[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_96,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_94,refute_0_95]) ).
cnf(refute_0_97,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_62,refute_0_96]) ).
cnf(refute_0_98,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_99,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_100,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_98,refute_0_99]) ).
cnf(refute_0_101,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_97,refute_0_100]) ).
cnf(refute_0_102,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_76:[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_103,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_101,refute_0_102]) ).
cnf(refute_0_104,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_103]) ).
cnf(refute_0_105,plain,
( notb(andb(andb(eq(arr(a,arr(a,b)),arr(a,arr(a,b))),btrue),btrue)) != bfalse
| sat_synth_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_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_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_106,plain,
( sat_synth_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_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_104,refute_0_105]) ).
cnf(refute_0_107,plain,
sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) = bfalse,
inference(resolve,[$cnf( $equal(sat_synth_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_61,refute_0_106]) ).
cnf(refute_0_108,plain,
( eq4(bfalse,bfalse) != btrue
| sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))) != bfalse
| eq4(sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( ~ $equal(eq4(sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),bfalse),btrue) ),[0,0],$fot(bfalse)]]) ).
cnf(refute_0_109,plain,
( eq4(bfalse,bfalse) != btrue
| eq4(sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),bfalse) = btrue ),
inference(resolve,[$cnf( $equal(sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),bfalse) )],[refute_0_107,refute_0_108]) ).
cnf(refute_0_110,plain,
eq4(bfalse,bfalse) != btrue,
inference(resolve,[$cnf( $equal(eq4(sat_synth_w(lam(lam(app(app(var(suc(zero)),var(zero),a),var(zero),a)))),bfalse),btrue) )],[refute_0_109,refute_0_0]) ).
cnf(refute_0_111,plain,
eq4(bfalse,bfalse) = btrue,
inference(subst,[],[axiom_049:[bind(X,$fot(bfalse))]]) ).
cnf(refute_0_112,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_113,plain,
( btrue != btrue
| eq4(bfalse,bfalse) = btrue ),
inference(resolve,[$cnf( $equal(eq4(bfalse,bfalse),btrue) )],[refute_0_111,refute_0_112]) ).
cnf(refute_0_114,plain,
btrue != btrue,
inference(resolve,[$cnf( $equal(eq4(bfalse,bfalse),btrue) )],[refute_0_113,refute_0_110]) ).
cnf(refute_0_115,plain,
$false,
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_69,refute_0_114]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : SWX224-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.07 % Command : metis --show proof --show saturation %s
% 0.07/0.25 % Computer : n024.cluster.edu
% 0.07/0.25 % Model : x86_64 x86_64
% 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.25 % Memory : 8042.1875MB
% 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.25 % CPULimit : 300
% 0.07/0.25 % WCLimit : 300
% 0.07/0.25 % DateTime : Tue May 5 07:41:26 EDT 2026
% 0.07/0.26 % CPUTime :
% 0.07/0.26 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 11.62/11.89 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.62/11.89
% 11.62/11.89 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 11.73/11.91
%------------------------------------------------------------------------------