%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWX222-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n031.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 0.19s 0.42s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 40
% Syntax : Number of clauses : 99 ( 55 unt; 0 nHn; 68 RR)
% Number of literals : 166 ( 165 equ; 71 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 6 con; 0-4 aty)
% Number of variables : 87 ( 7 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_007,axiom,
andb(btrue,Q) = Q ).
cnf(axiom_012,axiom,
nf(lam(E)) = nf(E) ).
cnf(axiom_013,axiom,
nf(var(X4)) = btrue ).
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_k(X) = notb(andb(nf(X),tc(nil,X,arr(a,arr(b,b))))) ).
cnf(axiom_051,axiom,
eq(X,X) = btrue ).
cnf(axiom_054,axiom,
eq4(X,X) = btrue ).
cnf(goal,negated_conjecture,
eq4(sat_synth_nf_k(X),bfalse) != btrue ).
cnf(refute_0_0,plain,
eq4(sat_synth_nf_k(lam(lam(var(zero)))),bfalse) != btrue,
inference(subst,[],[goal:[bind(X,$fot(lam(lam(var(zero)))))]]) ).
cnf(refute_0_1,plain,
sat_synth_nf_k(lam(E)) = notb(andb(nf(lam(E)),tc(nil,lam(E),arr(a,arr(b,b))))),
inference(subst,[],[axiom_020:[bind(X,$fot(lam(E)))]]) ).
cnf(refute_0_2,plain,
( nf(lam(E)) != nf(E)
| sat_synth_nf_k(lam(E)) != notb(andb(nf(lam(E)),tc(nil,lam(E),arr(a,arr(b,b)))))
| sat_synth_nf_k(lam(E)) = notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_k(lam(E)),notb(andb(nf(lam(E)),tc(nil,lam(E),arr(a,arr(b,b)))))) ),[1,0,0],$fot(nf(E))]]) ).
cnf(refute_0_3,plain,
( sat_synth_nf_k(lam(E)) != notb(andb(nf(lam(E)),tc(nil,lam(E),arr(a,arr(b,b)))))
| sat_synth_nf_k(lam(E)) = notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))) ),
inference(resolve,[$cnf( $equal(nf(lam(E)),nf(E)) )],[axiom_012,refute_0_2]) ).
cnf(refute_0_4,plain,
sat_synth_nf_k(lam(E)) = notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))),
inference(resolve,[$cnf( $equal(sat_synth_nf_k(lam(E)),notb(andb(nf(lam(E)),tc(nil,lam(E),arr(a,arr(b,b)))))) )],[refute_0_1,refute_0_3]) ).
cnf(refute_0_5,plain,
tc(nil,lam(E),arr(a,arr(b,b))) = tc(cons(a,nil),E,arr(b,b)),
inference(subst,[],[axiom_015:[bind(T1,$fot(arr(b,b))),bind(Tx2,$fot(a)),bind(X,$fot(nil))]]) ).
cnf(refute_0_6,plain,
andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))) = andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))),
introduced(tautology,[refl,[$fot(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))))]]) ).
cnf(refute_0_7,plain,
( andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))) != andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))
| tc(nil,lam(E),arr(a,arr(b,b))) != tc(cons(a,nil),E,arr(b,b))
| andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))) = andb(nf(E),tc(cons(a,nil),E,arr(b,b))) ),
introduced(tautology,[equality,[$cnf( $equal(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))),andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))) ),[1,1],$fot(tc(cons(a,nil),E,arr(b,b)))]]) ).
cnf(refute_0_8,plain,
( tc(nil,lam(E),arr(a,arr(b,b))) != tc(cons(a,nil),E,arr(b,b))
| andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))) = andb(nf(E),tc(cons(a,nil),E,arr(b,b))) ),
inference(resolve,[$cnf( $equal(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))),andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))) )],[refute_0_6,refute_0_7]) ).
cnf(refute_0_9,plain,
andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))) = andb(nf(E),tc(cons(a,nil),E,arr(b,b))),
inference(resolve,[$cnf( $equal(tc(nil,lam(E),arr(a,arr(b,b))),tc(cons(a,nil),E,arr(b,b))) )],[refute_0_5,refute_0_8]) ).
cnf(refute_0_10,plain,
notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))) = notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))),
introduced(tautology,[refl,[$fot(notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))))]]) ).
cnf(refute_0_11,plain,
( andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))) != andb(nf(E),tc(cons(a,nil),E,arr(b,b)))
| notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))) != notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))))
| notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))) = notb(andb(nf(E),tc(cons(a,nil),E,arr(b,b)))) ),
introduced(tautology,[equality,[$cnf( $equal(notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))),notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))))) ),[1,0],$fot(andb(nf(E),tc(cons(a,nil),E,arr(b,b))))]]) ).
cnf(refute_0_12,plain,
( andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))) != andb(nf(E),tc(cons(a,nil),E,arr(b,b)))
| notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))) = notb(andb(nf(E),tc(cons(a,nil),E,arr(b,b)))) ),
inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))),notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))))) )],[refute_0_10,refute_0_11]) ).
cnf(refute_0_13,plain,
notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))) = notb(andb(nf(E),tc(cons(a,nil),E,arr(b,b)))),
inference(resolve,[$cnf( $equal(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))),andb(nf(E),tc(cons(a,nil),E,arr(b,b)))) )],[refute_0_9,refute_0_12]) ).
cnf(refute_0_14,plain,
( notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))) != notb(andb(nf(E),tc(cons(a,nil),E,arr(b,b))))
| sat_synth_nf_k(lam(E)) != notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))))
| sat_synth_nf_k(lam(E)) = notb(andb(nf(E),tc(cons(a,nil),E,arr(b,b)))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_k(lam(E)),notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))))) ),[1],$fot(notb(andb(nf(E),tc(cons(a,nil),E,arr(b,b)))))]]) ).
cnf(refute_0_15,plain,
( sat_synth_nf_k(lam(E)) != notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))))
| sat_synth_nf_k(lam(E)) = notb(andb(nf(E),tc(cons(a,nil),E,arr(b,b)))) ),
inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b))))),notb(andb(nf(E),tc(cons(a,nil),E,arr(b,b))))) )],[refute_0_13,refute_0_14]) ).
cnf(refute_0_16,plain,
sat_synth_nf_k(lam(E)) = notb(andb(nf(E),tc(cons(a,nil),E,arr(b,b)))),
inference(resolve,[$cnf( $equal(sat_synth_nf_k(lam(E)),notb(andb(nf(E),tc(nil,lam(E),arr(a,arr(b,b)))))) )],[refute_0_4,refute_0_15]) ).
cnf(refute_0_17,plain,
sat_synth_nf_k(lam(lam(E))) = notb(andb(nf(lam(E)),tc(cons(a,nil),lam(E),arr(b,b)))),
inference(subst,[],[refute_0_16:[bind(E,$fot(lam(E)))]]) ).
cnf(refute_0_18,plain,
( nf(lam(E)) != nf(E)
| sat_synth_nf_k(lam(lam(E))) != notb(andb(nf(lam(E)),tc(cons(a,nil),lam(E),arr(b,b))))
| sat_synth_nf_k(lam(lam(E))) = notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_k(lam(lam(E))),notb(andb(nf(lam(E)),tc(cons(a,nil),lam(E),arr(b,b))))) ),[1,0,0],$fot(nf(E))]]) ).
cnf(refute_0_19,plain,
( sat_synth_nf_k(lam(lam(E))) != notb(andb(nf(lam(E)),tc(cons(a,nil),lam(E),arr(b,b))))
| sat_synth_nf_k(lam(lam(E))) = notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))) ),
inference(resolve,[$cnf( $equal(nf(lam(E)),nf(E)) )],[axiom_012,refute_0_18]) ).
cnf(refute_0_20,plain,
sat_synth_nf_k(lam(lam(E))) = notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))),
inference(resolve,[$cnf( $equal(sat_synth_nf_k(lam(lam(E))),notb(andb(nf(lam(E)),tc(cons(a,nil),lam(E),arr(b,b))))) )],[refute_0_17,refute_0_19]) ).
cnf(refute_0_21,plain,
tc(cons(a,nil),lam(E),arr(b,b)) = tc(cons(b,cons(a,nil)),E,b),
inference(subst,[],[axiom_015:[bind(T1,$fot(b)),bind(Tx2,$fot(b)),bind(X,$fot(cons(a,nil)))]]) ).
cnf(refute_0_22,plain,
andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))) = andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))),
introduced(tautology,[refl,[$fot(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))))]]) ).
cnf(refute_0_23,plain,
( andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))) != andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))
| tc(cons(a,nil),lam(E),arr(b,b)) != tc(cons(b,cons(a,nil)),E,b)
| andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))) = andb(nf(E),tc(cons(b,cons(a,nil)),E,b)) ),
introduced(tautology,[equality,[$cnf( $equal(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))),andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))) ),[1,1],$fot(tc(cons(b,cons(a,nil)),E,b))]]) ).
cnf(refute_0_24,plain,
( tc(cons(a,nil),lam(E),arr(b,b)) != tc(cons(b,cons(a,nil)),E,b)
| andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))) = andb(nf(E),tc(cons(b,cons(a,nil)),E,b)) ),
inference(resolve,[$cnf( $equal(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))),andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))) )],[refute_0_22,refute_0_23]) ).
cnf(refute_0_25,plain,
andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))) = andb(nf(E),tc(cons(b,cons(a,nil)),E,b)),
inference(resolve,[$cnf( $equal(tc(cons(a,nil),lam(E),arr(b,b)),tc(cons(b,cons(a,nil)),E,b)) )],[refute_0_21,refute_0_24]) ).
cnf(refute_0_26,plain,
notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))) = notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))),
introduced(tautology,[refl,[$fot(notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))))]]) ).
cnf(refute_0_27,plain,
( andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))) != andb(nf(E),tc(cons(b,cons(a,nil)),E,b))
| notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))) != notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))))
| notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))) = notb(andb(nf(E),tc(cons(b,cons(a,nil)),E,b))) ),
introduced(tautology,[equality,[$cnf( $equal(notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))),notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))))) ),[1,0],$fot(andb(nf(E),tc(cons(b,cons(a,nil)),E,b)))]]) ).
cnf(refute_0_28,plain,
( andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))) != andb(nf(E),tc(cons(b,cons(a,nil)),E,b))
| notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))) = notb(andb(nf(E),tc(cons(b,cons(a,nil)),E,b))) ),
inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))),notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))))) )],[refute_0_26,refute_0_27]) ).
cnf(refute_0_29,plain,
notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))) = notb(andb(nf(E),tc(cons(b,cons(a,nil)),E,b))),
inference(resolve,[$cnf( $equal(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))),andb(nf(E),tc(cons(b,cons(a,nil)),E,b))) )],[refute_0_25,refute_0_28]) ).
cnf(refute_0_30,plain,
( notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))) != notb(andb(nf(E),tc(cons(b,cons(a,nil)),E,b)))
| sat_synth_nf_k(lam(lam(E))) != notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))))
| sat_synth_nf_k(lam(lam(E))) = notb(andb(nf(E),tc(cons(b,cons(a,nil)),E,b))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_k(lam(lam(E))),notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))))) ),[1],$fot(notb(andb(nf(E),tc(cons(b,cons(a,nil)),E,b))))]]) ).
cnf(refute_0_31,plain,
( sat_synth_nf_k(lam(lam(E))) != notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))))
| sat_synth_nf_k(lam(lam(E))) = notb(andb(nf(E),tc(cons(b,cons(a,nil)),E,b))) ),
inference(resolve,[$cnf( $equal(notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b)))),notb(andb(nf(E),tc(cons(b,cons(a,nil)),E,b)))) )],[refute_0_29,refute_0_30]) ).
cnf(refute_0_32,plain,
sat_synth_nf_k(lam(lam(E))) = notb(andb(nf(E),tc(cons(b,cons(a,nil)),E,b))),
inference(resolve,[$cnf( $equal(sat_synth_nf_k(lam(lam(E))),notb(andb(nf(E),tc(cons(a,nil),lam(E),arr(b,b))))) )],[refute_0_20,refute_0_31]) ).
cnf(refute_0_33,plain,
sat_synth_nf_k(lam(lam(var(zero)))) = notb(andb(nf(var(zero)),tc(cons(b,cons(a,nil)),var(zero),b))),
inference(subst,[],[refute_0_32:[bind(E,$fot(var(zero)))]]) ).
cnf(refute_0_34,plain,
tc(cons(Z,Xs),var(zero),X_79) = aux(cons(Z,Xs),X_79,zero,index(cons(Z,Xs),zero)),
inference(subst,[],[axiom_019:[bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(zero)),bind(Z,$fot(X_79))]]) ).
cnf(refute_0_35,plain,
( index(cons(Z,Xs),zero) != just(Z)
| tc(cons(Z,Xs),var(zero),X_79) != aux(cons(Z,Xs),X_79,zero,index(cons(Z,Xs),zero))
| tc(cons(Z,Xs),var(zero),X_79) = aux(cons(Z,Xs),X_79,zero,just(Z)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_79),aux(cons(Z,Xs),X_79,zero,index(cons(Z,Xs),zero))) ),[1,3],$fot(just(Z))]]) ).
cnf(refute_0_36,plain,
( tc(cons(Z,Xs),var(zero),X_79) != aux(cons(Z,Xs),X_79,zero,index(cons(Z,Xs),zero))
| tc(cons(Z,Xs),var(zero),X_79) = aux(cons(Z,Xs),X_79,zero,just(Z)) ),
inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(Z)) )],[axiom_005,refute_0_35]) ).
cnf(refute_0_37,plain,
tc(cons(Z,Xs),var(zero),X_79) = aux(cons(Z,Xs),X_79,zero,just(Z)),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_79),aux(cons(Z,Xs),X_79,zero,index(cons(Z,Xs),zero))) )],[refute_0_34,refute_0_36]) ).
cnf(refute_0_38,plain,
aux(cons(Z,Xs),X_79,zero,just(Z)) = eq(Z,X_79),
inference(subst,[],[axiom_001:[bind(Tx3,$fot(Z)),bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(zero)),bind(Z,$fot(X_79))]]) ).
cnf(refute_0_39,plain,
( aux(cons(Z,Xs),X_79,zero,just(Z)) != eq(Z,X_79)
| tc(cons(Z,Xs),var(zero),X_79) != aux(cons(Z,Xs),X_79,zero,just(Z))
| tc(cons(Z,Xs),var(zero),X_79) = eq(Z,X_79) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_79),aux(cons(Z,Xs),X_79,zero,just(Z))) ),[1],$fot(eq(Z,X_79))]]) ).
cnf(refute_0_40,plain,
( tc(cons(Z,Xs),var(zero),X_79) != aux(cons(Z,Xs),X_79,zero,just(Z))
| tc(cons(Z,Xs),var(zero),X_79) = eq(Z,X_79) ),
inference(resolve,[$cnf( $equal(aux(cons(Z,Xs),X_79,zero,just(Z)),eq(Z,X_79)) )],[refute_0_38,refute_0_39]) ).
cnf(refute_0_41,plain,
tc(cons(Z,Xs),var(zero),X_79) = eq(Z,X_79),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_79),aux(cons(Z,Xs),X_79,zero,just(Z))) )],[refute_0_37,refute_0_40]) ).
cnf(refute_0_42,plain,
tc(cons(b,cons(a,nil)),var(zero),b) = eq(b,b),
inference(subst,[],[refute_0_41:[bind(Xs,$fot(cons(a,nil))),bind(Z,$fot(b)),bind(X_79,$fot(b))]]) ).
cnf(refute_0_43,plain,
( sat_synth_nf_k(lam(lam(var(zero)))) != notb(andb(nf(var(zero)),tc(cons(b,cons(a,nil)),var(zero),b)))
| tc(cons(b,cons(a,nil)),var(zero),b) != eq(b,b)
| sat_synth_nf_k(lam(lam(var(zero)))) = notb(andb(nf(var(zero)),eq(b,b))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_k(lam(lam(var(zero)))),notb(andb(nf(var(zero)),tc(cons(b,cons(a,nil)),var(zero),b)))) ),[1,0,1],$fot(eq(b,b))]]) ).
cnf(refute_0_44,plain,
( sat_synth_nf_k(lam(lam(var(zero)))) != notb(andb(nf(var(zero)),tc(cons(b,cons(a,nil)),var(zero),b)))
| sat_synth_nf_k(lam(lam(var(zero)))) = notb(andb(nf(var(zero)),eq(b,b))) ),
inference(resolve,[$cnf( $equal(tc(cons(b,cons(a,nil)),var(zero),b),eq(b,b)) )],[refute_0_42,refute_0_43]) ).
cnf(refute_0_45,plain,
sat_synth_nf_k(lam(lam(var(zero)))) = notb(andb(nf(var(zero)),eq(b,b))),
inference(resolve,[$cnf( $equal(sat_synth_nf_k(lam(lam(var(zero)))),notb(andb(nf(var(zero)),tc(cons(b,cons(a,nil)),var(zero),b)))) )],[refute_0_33,refute_0_44]) ).
cnf(refute_0_46,plain,
andb(btrue,btrue) = btrue,
inference(subst,[],[axiom_007:[bind(Q,$fot(btrue))]]) ).
cnf(refute_0_47,plain,
eq(b,b) = btrue,
inference(subst,[],[axiom_051:[bind(X,$fot(b))]]) ).
cnf(refute_0_48,plain,
andb(btrue,eq(b,b)) = andb(btrue,eq(b,b)),
introduced(tautology,[refl,[$fot(andb(btrue,eq(b,b)))]]) ).
cnf(refute_0_49,plain,
( andb(btrue,eq(b,b)) != andb(btrue,eq(b,b))
| eq(b,b) != btrue
| andb(btrue,eq(b,b)) = andb(btrue,btrue) ),
introduced(tautology,[equality,[$cnf( $equal(andb(btrue,eq(b,b)),andb(btrue,eq(b,b))) ),[1,1],$fot(btrue)]]) ).
cnf(refute_0_50,plain,
( eq(b,b) != btrue
| andb(btrue,eq(b,b)) = andb(btrue,btrue) ),
inference(resolve,[$cnf( $equal(andb(btrue,eq(b,b)),andb(btrue,eq(b,b))) )],[refute_0_48,refute_0_49]) ).
cnf(refute_0_51,plain,
andb(btrue,eq(b,b)) = andb(btrue,btrue),
inference(resolve,[$cnf( $equal(eq(b,b),btrue) )],[refute_0_47,refute_0_50]) ).
cnf(refute_0_52,plain,
nf(var(zero)) = btrue,
inference(subst,[],[axiom_013:[bind(X4,$fot(zero))]]) ).
cnf(refute_0_53,plain,
andb(nf(var(zero)),eq(b,b)) = andb(nf(var(zero)),eq(b,b)),
introduced(tautology,[refl,[$fot(andb(nf(var(zero)),eq(b,b)))]]) ).
cnf(refute_0_54,plain,
( andb(nf(var(zero)),eq(b,b)) != andb(nf(var(zero)),eq(b,b))
| nf(var(zero)) != btrue
| andb(nf(var(zero)),eq(b,b)) = andb(btrue,eq(b,b)) ),
introduced(tautology,[equality,[$cnf( $equal(andb(nf(var(zero)),eq(b,b)),andb(nf(var(zero)),eq(b,b))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_55,plain,
( nf(var(zero)) != btrue
| andb(nf(var(zero)),eq(b,b)) = andb(btrue,eq(b,b)) ),
inference(resolve,[$cnf( $equal(andb(nf(var(zero)),eq(b,b)),andb(nf(var(zero)),eq(b,b))) )],[refute_0_53,refute_0_54]) ).
cnf(refute_0_56,plain,
andb(nf(var(zero)),eq(b,b)) = andb(btrue,eq(b,b)),
inference(resolve,[$cnf( $equal(nf(var(zero)),btrue) )],[refute_0_52,refute_0_55]) ).
cnf(refute_0_57,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_58,plain,
( X0 != X0
| X0 != Y
| Y = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y)]]) ).
cnf(refute_0_59,plain,
( X0 != Y
| Y = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_57,refute_0_58]) ).
cnf(refute_0_60,plain,
( Y != X0
| Y != Z0
| X0 = Z0 ),
introduced(tautology,[equality,[$cnf( $equal(Y,Z0) ),[0],$fot(X0)]]) ).
cnf(refute_0_61,plain,
( X0 != Y
| Y != Z0
| X0 = Z0 ),
inference(resolve,[$cnf( $equal(Y,X0) )],[refute_0_59,refute_0_60]) ).
cnf(refute_0_62,plain,
( andb(btrue,eq(b,b)) != andb(btrue,btrue)
| andb(nf(var(zero)),eq(b,b)) != andb(btrue,eq(b,b))
| andb(nf(var(zero)),eq(b,b)) = andb(btrue,btrue) ),
inference(subst,[],[refute_0_61:[bind(X0,$fot(andb(nf(var(zero)),eq(b,b)))),bind(Y,$fot(andb(btrue,eq(b,b)))),bind(Z0,$fot(andb(btrue,btrue)))]]) ).
cnf(refute_0_63,plain,
( andb(btrue,eq(b,b)) != andb(btrue,btrue)
| andb(nf(var(zero)),eq(b,b)) = andb(btrue,btrue) ),
inference(resolve,[$cnf( $equal(andb(nf(var(zero)),eq(b,b)),andb(btrue,eq(b,b))) )],[refute_0_56,refute_0_62]) ).
cnf(refute_0_64,plain,
andb(nf(var(zero)),eq(b,b)) = andb(btrue,btrue),
inference(resolve,[$cnf( $equal(andb(btrue,eq(b,b)),andb(btrue,btrue)) )],[refute_0_51,refute_0_63]) ).
cnf(refute_0_65,plain,
( andb(btrue,btrue) != btrue
| andb(nf(var(zero)),eq(b,b)) != andb(btrue,btrue)
| andb(nf(var(zero)),eq(b,b)) = btrue ),
inference(subst,[],[refute_0_61:[bind(X0,$fot(andb(nf(var(zero)),eq(b,b)))),bind(Y,$fot(andb(btrue,btrue))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_66,plain,
( andb(btrue,btrue) != btrue
| andb(nf(var(zero)),eq(b,b)) = btrue ),
inference(resolve,[$cnf( $equal(andb(nf(var(zero)),eq(b,b)),andb(btrue,btrue)) )],[refute_0_64,refute_0_65]) ).
cnf(refute_0_67,plain,
andb(nf(var(zero)),eq(b,b)) = btrue,
inference(resolve,[$cnf( $equal(andb(btrue,btrue),btrue) )],[refute_0_46,refute_0_66]) ).
cnf(refute_0_68,plain,
notb(andb(nf(var(zero)),eq(b,b))) = notb(andb(nf(var(zero)),eq(b,b))),
introduced(tautology,[refl,[$fot(notb(andb(nf(var(zero)),eq(b,b))))]]) ).
cnf(refute_0_69,plain,
( andb(nf(var(zero)),eq(b,b)) != btrue
| notb(andb(nf(var(zero)),eq(b,b))) != notb(andb(nf(var(zero)),eq(b,b)))
| notb(andb(nf(var(zero)),eq(b,b))) = notb(btrue) ),
introduced(tautology,[equality,[$cnf( $equal(notb(andb(nf(var(zero)),eq(b,b))),notb(andb(nf(var(zero)),eq(b,b)))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_70,plain,
( andb(nf(var(zero)),eq(b,b)) != btrue
| notb(andb(nf(var(zero)),eq(b,b))) = notb(btrue) ),
inference(resolve,[$cnf( $equal(notb(andb(nf(var(zero)),eq(b,b))),notb(andb(nf(var(zero)),eq(b,b)))) )],[refute_0_68,refute_0_69]) ).
cnf(refute_0_71,plain,
notb(andb(nf(var(zero)),eq(b,b))) = notb(btrue),
inference(resolve,[$cnf( $equal(andb(nf(var(zero)),eq(b,b)),btrue) )],[refute_0_67,refute_0_70]) ).
cnf(refute_0_72,plain,
( notb(andb(nf(var(zero)),eq(b,b))) != notb(btrue)
| notb(btrue) != bfalse
| notb(andb(nf(var(zero)),eq(b,b))) = bfalse ),
inference(subst,[],[refute_0_61:[bind(X0,$fot(notb(andb(nf(var(zero)),eq(b,b))))),bind(Y,$fot(notb(btrue))),bind(Z0,$fot(bfalse))]]) ).
cnf(refute_0_73,plain,
( notb(btrue) != bfalse
| notb(andb(nf(var(zero)),eq(b,b))) = bfalse ),
inference(resolve,[$cnf( $equal(notb(andb(nf(var(zero)),eq(b,b))),notb(btrue)) )],[refute_0_71,refute_0_72]) ).
cnf(refute_0_74,plain,
notb(andb(nf(var(zero)),eq(b,b))) = bfalse,
inference(resolve,[$cnf( $equal(notb(btrue),bfalse) )],[axiom_002,refute_0_73]) ).
cnf(refute_0_75,plain,
( notb(andb(nf(var(zero)),eq(b,b))) != bfalse
| sat_synth_nf_k(lam(lam(var(zero)))) != notb(andb(nf(var(zero)),eq(b,b)))
| sat_synth_nf_k(lam(lam(var(zero)))) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_nf_k(lam(lam(var(zero)))),notb(andb(nf(var(zero)),eq(b,b)))) ),[1],$fot(bfalse)]]) ).
cnf(refute_0_76,plain,
( sat_synth_nf_k(lam(lam(var(zero)))) != notb(andb(nf(var(zero)),eq(b,b)))
| sat_synth_nf_k(lam(lam(var(zero)))) = bfalse ),
inference(resolve,[$cnf( $equal(notb(andb(nf(var(zero)),eq(b,b))),bfalse) )],[refute_0_74,refute_0_75]) ).
cnf(refute_0_77,plain,
sat_synth_nf_k(lam(lam(var(zero)))) = bfalse,
inference(resolve,[$cnf( $equal(sat_synth_nf_k(lam(lam(var(zero)))),notb(andb(nf(var(zero)),eq(b,b)))) )],[refute_0_45,refute_0_76]) ).
cnf(refute_0_78,plain,
( eq4(bfalse,bfalse) != btrue
| sat_synth_nf_k(lam(lam(var(zero)))) != bfalse
| eq4(sat_synth_nf_k(lam(lam(var(zero)))),bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( ~ $equal(eq4(sat_synth_nf_k(lam(lam(var(zero)))),bfalse),btrue) ),[0,0],$fot(bfalse)]]) ).
cnf(refute_0_79,plain,
( eq4(bfalse,bfalse) != btrue
| eq4(sat_synth_nf_k(lam(lam(var(zero)))),bfalse) = btrue ),
inference(resolve,[$cnf( $equal(sat_synth_nf_k(lam(lam(var(zero)))),bfalse) )],[refute_0_77,refute_0_78]) ).
cnf(refute_0_80,plain,
eq4(bfalse,bfalse) != btrue,
inference(resolve,[$cnf( $equal(eq4(sat_synth_nf_k(lam(lam(var(zero)))),bfalse),btrue) )],[refute_0_79,refute_0_0]) ).
cnf(refute_0_81,plain,
eq4(bfalse,bfalse) = btrue,
inference(subst,[],[axiom_054:[bind(X,$fot(bfalse))]]) ).
cnf(refute_0_82,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_83,plain,
( btrue != btrue
| eq4(bfalse,bfalse) = btrue ),
inference(resolve,[$cnf( $equal(eq4(bfalse,bfalse),btrue) )],[refute_0_81,refute_0_82]) ).
cnf(refute_0_84,plain,
btrue != btrue,
inference(resolve,[$cnf( $equal(eq4(bfalse,bfalse),btrue) )],[refute_0_83,refute_0_80]) ).
cnf(refute_0_85,plain,
btrue = btrue,
introduced(tautology,[refl,[$fot(btrue)]]) ).
cnf(refute_0_86,plain,
$false,
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_85,refute_0_84]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX222-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : metis --show proof --show saturation %s
% 0.15/0.33 % Computer : n031.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 12:36:38 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.19/0.42 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.42
% 0.19/0.42 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.19/0.44
%------------------------------------------------------------------------------