%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWX220-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 07:04:35 PM UTC 2026
% Result : Unsatisfiable 111.74s 111.95s
% Output : CNFRefutation 111.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 45
% Syntax : Number of clauses : 150 ( 83 unt; 0 nHn; 90 RR)
% Number of literals : 250 ( 249 equ; 104 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 3 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 7 con; 0-4 aty)
% Number of variables : 312 ( 25 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_flip(X) = notb(tc(nil,X,arr(arr(a,arr(b,c)),arr(b,arr(a,c))))) ).
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_flip(X),bfalse) != btrue ).
cnf(refute_0_0,plain,
eq4(sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),bfalse) != btrue,
inference(subst,[],[goal:[bind(X,$fot(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))))]]) ).
cnf(refute_0_1,plain,
sat_synth_flip(lam(X_68)) = notb(tc(nil,lam(X_68),arr(arr(a,arr(b,c)),arr(b,arr(a,c))))),
inference(subst,[],[axiom_015:[bind(X,$fot(lam(X_68)))]]) ).
cnf(refute_0_2,plain,
tc(nil,lam(X_68),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))) = tc(cons(arr(a,arr(b,c)),nil),X_68,arr(b,arr(a,c))),
inference(subst,[],[axiom_010:[bind(E,$fot(X_68)),bind(T1,$fot(arr(b,arr(a,c)))),bind(Tx2,$fot(arr(a,arr(b,c)))),bind(X,$fot(nil))]]) ).
cnf(refute_0_3,plain,
( sat_synth_flip(lam(X_68)) != notb(tc(nil,lam(X_68),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))
| tc(nil,lam(X_68),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))) != tc(cons(arr(a,arr(b,c)),nil),X_68,arr(b,arr(a,c)))
| sat_synth_flip(lam(X_68)) = notb(tc(cons(arr(a,arr(b,c)),nil),X_68,arr(b,arr(a,c)))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_flip(lam(X_68)),notb(tc(nil,lam(X_68),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) ),[1,0],$fot(tc(cons(arr(a,arr(b,c)),nil),X_68,arr(b,arr(a,c))))]]) ).
cnf(refute_0_4,plain,
( sat_synth_flip(lam(X_68)) != notb(tc(nil,lam(X_68),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))
| sat_synth_flip(lam(X_68)) = notb(tc(cons(arr(a,arr(b,c)),nil),X_68,arr(b,arr(a,c)))) ),
inference(resolve,[$cnf( $equal(tc(nil,lam(X_68),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),tc(cons(arr(a,arr(b,c)),nil),X_68,arr(b,arr(a,c)))) )],[refute_0_2,refute_0_3]) ).
cnf(refute_0_5,plain,
sat_synth_flip(lam(X_68)) = notb(tc(cons(arr(a,arr(b,c)),nil),X_68,arr(b,arr(a,c)))),
inference(resolve,[$cnf( $equal(sat_synth_flip(lam(X_68)),notb(tc(nil,lam(X_68),arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))) )],[refute_0_1,refute_0_4]) ).
cnf(refute_0_6,plain,
sat_synth_flip(lam(lam(E))) = notb(tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c)))),
inference(subst,[],[refute_0_5:[bind(X_68,$fot(lam(E)))]]) ).
cnf(refute_0_7,plain,
tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))) = tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)),
inference(subst,[],[axiom_010:[bind(T1,$fot(arr(a,c))),bind(Tx2,$fot(b)),bind(X,$fot(cons(arr(a,arr(b,c)),nil)))]]) ).
cnf(refute_0_8,plain,
( sat_synth_flip(lam(lam(E))) != notb(tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))
| tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))) != tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))
| sat_synth_flip(lam(lam(E))) = notb(tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_flip(lam(lam(E))),notb(tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))) ),[1,0],$fot(tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c)))]]) ).
cnf(refute_0_9,plain,
( sat_synth_flip(lam(lam(E))) != notb(tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))
| sat_synth_flip(lam(lam(E))) = notb(tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))) ),
inference(resolve,[$cnf( $equal(tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))),tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))) )],[refute_0_7,refute_0_8]) ).
cnf(refute_0_10,plain,
sat_synth_flip(lam(lam(E))) = notb(tc(cons(b,cons(arr(a,arr(b,c)),nil)),E,arr(a,c))),
inference(resolve,[$cnf( $equal(sat_synth_flip(lam(lam(E))),notb(tc(cons(arr(a,arr(b,c)),nil),lam(E),arr(b,arr(a,c))))) )],[refute_0_6,refute_0_9]) ).
cnf(refute_0_11,plain,
sat_synth_flip(lam(lam(lam(E)))) = notb(tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c))),
inference(subst,[],[refute_0_10:[bind(E,$fot(lam(E)))]]) ).
cnf(refute_0_12,plain,
tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)) = tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c),
inference(subst,[],[axiom_010:[bind(T1,$fot(c)),bind(Tx2,$fot(a)),bind(X,$fot(cons(b,cons(arr(a,arr(b,c)),nil))))]]) ).
cnf(refute_0_13,plain,
( sat_synth_flip(lam(lam(lam(E)))) != notb(tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))
| tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)) != tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)
| sat_synth_flip(lam(lam(lam(E)))) = notb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_flip(lam(lam(lam(E)))),notb(tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))) ),[1,0],$fot(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c))]]) ).
cnf(refute_0_14,plain,
( sat_synth_flip(lam(lam(lam(E)))) != notb(tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))
| sat_synth_flip(lam(lam(lam(E)))) = notb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)) ),
inference(resolve,[$cnf( $equal(tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)),tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)) )],[refute_0_12,refute_0_13]) ).
cnf(refute_0_15,plain,
sat_synth_flip(lam(lam(lam(E)))) = notb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),E,c)),
inference(resolve,[$cnf( $equal(sat_synth_flip(lam(lam(lam(E)))),notb(tc(cons(b,cons(arr(a,arr(b,c)),nil)),lam(E),arr(a,c)))) )],[refute_0_11,refute_0_14]) ).
cnf(refute_0_16,plain,
sat_synth_flip(lam(lam(lam(app(X_6992,var(suc(zero)),b))))) = notb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_6992,var(suc(zero)),b),c)),
inference(subst,[],[refute_0_15:[bind(E,$fot(app(X_6992,var(suc(zero)),b)))]]) ).
cnf(refute_0_17,plain,
tc(cons(X_86,cons(Z,Xs)),app(X_96,var(suc(zero)),X_97),X_100) = andb(tc(cons(X_86,cons(Z,Xs)),X_96,arr(X_97,X_100)),tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_97)),
inference(subst,[],[axiom_009:[bind(F,$fot(X_96)),bind(Tx,$fot(X_97)),bind(X,$fot(cons(X_86,cons(Z,Xs)))),bind(X2,$fot(var(suc(zero)))),bind(Z,$fot(X_100))]]) ).
cnf(refute_0_18,plain,
tc(cons(Z,Xs),var(suc(N)),X_57) = aux(cons(Z,Xs),X_57,suc(N),index(cons(Z,Xs),suc(N))),
inference(subst,[],[axiom_014:[bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(suc(N))),bind(Z,$fot(X_57))]]) ).
cnf(refute_0_19,plain,
( index(cons(Z,Xs),suc(N)) != index(Xs,N)
| tc(cons(Z,Xs),var(suc(N)),X_57) != aux(cons(Z,Xs),X_57,suc(N),index(cons(Z,Xs),suc(N)))
| tc(cons(Z,Xs),var(suc(N)),X_57) = aux(cons(Z,Xs),X_57,suc(N),index(Xs,N)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),var(suc(N)),X_57),aux(cons(Z,Xs),X_57,suc(N),index(cons(Z,Xs),suc(N)))) ),[1,3],$fot(index(Xs,N))]]) ).
cnf(refute_0_20,plain,
( tc(cons(Z,Xs),var(suc(N)),X_57) != aux(cons(Z,Xs),X_57,suc(N),index(cons(Z,Xs),suc(N)))
| tc(cons(Z,Xs),var(suc(N)),X_57) = aux(cons(Z,Xs),X_57,suc(N),index(Xs,N)) ),
inference(resolve,[$cnf( $equal(index(cons(Z,Xs),suc(N)),index(Xs,N)) )],[axiom_006,refute_0_19]) ).
cnf(refute_0_21,plain,
tc(cons(Z,Xs),var(suc(N)),X_57) = aux(cons(Z,Xs),X_57,suc(N),index(Xs,N)),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(suc(N)),X_57),aux(cons(Z,Xs),X_57,suc(N),index(cons(Z,Xs),suc(N)))) )],[refute_0_18,refute_0_20]) ).
cnf(refute_0_22,plain,
tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87) = aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),index(cons(Z,Xs),zero)),
inference(subst,[],[refute_0_21:[bind(N,$fot(zero)),bind(Xs,$fot(cons(Z,Xs))),bind(Z,$fot(X_86)),bind(X_57,$fot(X_87))]]) ).
cnf(refute_0_23,plain,
( index(cons(Z,Xs),zero) != just(Z)
| tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87) != aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),index(cons(Z,Xs),zero))
| tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87) = aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),just(Z)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87),aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),index(cons(Z,Xs),zero))) ),[1,3],$fot(just(Z))]]) ).
cnf(refute_0_24,plain,
( tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87) != aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),index(cons(Z,Xs),zero))
| tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87) = aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),just(Z)) ),
inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(Z)) )],[axiom_005,refute_0_23]) ).
cnf(refute_0_25,plain,
tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87) = aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),just(Z)),
inference(resolve,[$cnf( $equal(tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87),aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),index(cons(Z,Xs),zero))) )],[refute_0_22,refute_0_24]) ).
cnf(refute_0_26,plain,
aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),just(Z)) = eq(Z,X_87),
inference(subst,[],[axiom_001:[bind(Tx3,$fot(Z)),bind(X,$fot(cons(X_86,cons(Z,Xs)))),bind(X3,$fot(suc(zero))),bind(Z,$fot(X_87))]]) ).
cnf(refute_0_27,plain,
( aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),just(Z)) != eq(Z,X_87)
| tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87) != aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),just(Z))
| tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87) = eq(Z,X_87) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87),aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),just(Z))) ),[1],$fot(eq(Z,X_87))]]) ).
cnf(refute_0_28,plain,
( tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87) != aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),just(Z))
| tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87) = eq(Z,X_87) ),
inference(resolve,[$cnf( $equal(aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),just(Z)),eq(Z,X_87)) )],[refute_0_26,refute_0_27]) ).
cnf(refute_0_29,plain,
tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87) = eq(Z,X_87),
inference(resolve,[$cnf( $equal(tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_87),aux(cons(X_86,cons(Z,Xs)),X_87,suc(zero),just(Z))) )],[refute_0_25,refute_0_28]) ).
cnf(refute_0_30,plain,
tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_97) = eq(Z,X_97),
inference(subst,[],[refute_0_29:[bind(X_87,$fot(X_97))]]) ).
cnf(refute_0_31,plain,
( tc(cons(X_86,cons(Z,Xs)),app(X_96,var(suc(zero)),X_97),X_100) != andb(tc(cons(X_86,cons(Z,Xs)),X_96,arr(X_97,X_100)),tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_97))
| tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_97) != eq(Z,X_97)
| tc(cons(X_86,cons(Z,Xs)),app(X_96,var(suc(zero)),X_97),X_100) = andb(tc(cons(X_86,cons(Z,Xs)),X_96,arr(X_97,X_100)),eq(Z,X_97)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_86,cons(Z,Xs)),app(X_96,var(suc(zero)),X_97),X_100),andb(tc(cons(X_86,cons(Z,Xs)),X_96,arr(X_97,X_100)),tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_97))) ),[1,1],$fot(eq(Z,X_97))]]) ).
cnf(refute_0_32,plain,
( tc(cons(X_86,cons(Z,Xs)),app(X_96,var(suc(zero)),X_97),X_100) != andb(tc(cons(X_86,cons(Z,Xs)),X_96,arr(X_97,X_100)),tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_97))
| tc(cons(X_86,cons(Z,Xs)),app(X_96,var(suc(zero)),X_97),X_100) = andb(tc(cons(X_86,cons(Z,Xs)),X_96,arr(X_97,X_100)),eq(Z,X_97)) ),
inference(resolve,[$cnf( $equal(tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_97),eq(Z,X_97)) )],[refute_0_30,refute_0_31]) ).
cnf(refute_0_33,plain,
tc(cons(X_86,cons(Z,Xs)),app(X_96,var(suc(zero)),X_97),X_100) = andb(tc(cons(X_86,cons(Z,Xs)),X_96,arr(X_97,X_100)),eq(Z,X_97)),
inference(resolve,[$cnf( $equal(tc(cons(X_86,cons(Z,Xs)),app(X_96,var(suc(zero)),X_97),X_100),andb(tc(cons(X_86,cons(Z,Xs)),X_96,arr(X_97,X_100)),tc(cons(X_86,cons(Z,Xs)),var(suc(zero)),X_97))) )],[refute_0_17,refute_0_32]) ).
cnf(refute_0_34,plain,
tc(cons(X_1945,cons(X_1947,X_1942)),app(X_1946,var(suc(zero)),X_1947),X_1944) = andb(tc(cons(X_1945,cons(X_1947,X_1942)),X_1946,arr(X_1947,X_1944)),eq(X_1947,X_1947)),
inference(subst,[],[refute_0_33:[bind(Xs,$fot(X_1942)),bind(Z,$fot(X_1947)),bind(X_100,$fot(X_1944)),bind(X_86,$fot(X_1945)),bind(X_96,$fot(X_1946)),bind(X_97,$fot(X_1947))]]) ).
cnf(refute_0_35,plain,
eq(X_1947,X_1947) = btrue,
inference(subst,[],[axiom_046:[bind(X,$fot(X_1947))]]) ).
cnf(refute_0_36,plain,
( eq(X_1947,X_1947) != btrue
| tc(cons(X_1945,cons(X_1947,X_1942)),app(X_1946,var(suc(zero)),X_1947),X_1944) != andb(tc(cons(X_1945,cons(X_1947,X_1942)),X_1946,arr(X_1947,X_1944)),eq(X_1947,X_1947))
| tc(cons(X_1945,cons(X_1947,X_1942)),app(X_1946,var(suc(zero)),X_1947),X_1944) = andb(tc(cons(X_1945,cons(X_1947,X_1942)),X_1946,arr(X_1947,X_1944)),btrue) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_1945,cons(X_1947,X_1942)),app(X_1946,var(suc(zero)),X_1947),X_1944),andb(tc(cons(X_1945,cons(X_1947,X_1942)),X_1946,arr(X_1947,X_1944)),eq(X_1947,X_1947))) ),[1,1],$fot(btrue)]]) ).
cnf(refute_0_37,plain,
( tc(cons(X_1945,cons(X_1947,X_1942)),app(X_1946,var(suc(zero)),X_1947),X_1944) != andb(tc(cons(X_1945,cons(X_1947,X_1942)),X_1946,arr(X_1947,X_1944)),eq(X_1947,X_1947))
| tc(cons(X_1945,cons(X_1947,X_1942)),app(X_1946,var(suc(zero)),X_1947),X_1944) = andb(tc(cons(X_1945,cons(X_1947,X_1942)),X_1946,arr(X_1947,X_1944)),btrue) ),
inference(resolve,[$cnf( $equal(eq(X_1947,X_1947),btrue) )],[refute_0_35,refute_0_36]) ).
cnf(refute_0_38,plain,
tc(cons(X_1945,cons(X_1947,X_1942)),app(X_1946,var(suc(zero)),X_1947),X_1944) = andb(tc(cons(X_1945,cons(X_1947,X_1942)),X_1946,arr(X_1947,X_1944)),btrue),
inference(resolve,[$cnf( $equal(tc(cons(X_1945,cons(X_1947,X_1942)),app(X_1946,var(suc(zero)),X_1947),X_1944),andb(tc(cons(X_1945,cons(X_1947,X_1942)),X_1946,arr(X_1947,X_1944)),eq(X_1947,X_1947))) )],[refute_0_34,refute_0_37]) ).
cnf(refute_0_39,plain,
tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_6992,var(suc(zero)),b),c) = andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_6992,arr(b,c)),btrue),
inference(subst,[],[refute_0_38:[bind(X_1942,$fot(cons(arr(a,arr(b,c)),nil))),bind(X_1944,$fot(c)),bind(X_1945,$fot(a)),bind(X_1946,$fot(X_6992)),bind(X_1947,$fot(b))]]) ).
cnf(refute_0_40,plain,
( sat_synth_flip(lam(lam(lam(app(X_6992,var(suc(zero)),b))))) != notb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_6992,var(suc(zero)),b),c))
| tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_6992,var(suc(zero)),b),c) != andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_6992,arr(b,c)),btrue)
| sat_synth_flip(lam(lam(lam(app(X_6992,var(suc(zero)),b))))) = notb(andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_6992,arr(b,c)),btrue)) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_flip(lam(lam(lam(app(X_6992,var(suc(zero)),b))))),notb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_6992,var(suc(zero)),b),c))) ),[1,0],$fot(andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_6992,arr(b,c)),btrue))]]) ).
cnf(refute_0_41,plain,
( sat_synth_flip(lam(lam(lam(app(X_6992,var(suc(zero)),b))))) != notb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_6992,var(suc(zero)),b),c))
| sat_synth_flip(lam(lam(lam(app(X_6992,var(suc(zero)),b))))) = notb(andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_6992,arr(b,c)),btrue)) ),
inference(resolve,[$cnf( $equal(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_6992,var(suc(zero)),b),c),andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_6992,arr(b,c)),btrue)) )],[refute_0_39,refute_0_40]) ).
cnf(refute_0_42,plain,
sat_synth_flip(lam(lam(lam(app(X_6992,var(suc(zero)),b))))) = notb(andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X_6992,arr(b,c)),btrue)),
inference(resolve,[$cnf( $equal(sat_synth_flip(lam(lam(lam(app(X_6992,var(suc(zero)),b))))),notb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(X_6992,var(suc(zero)),b),c))) )],[refute_0_16,refute_0_41]) ).
cnf(refute_0_43,plain,
sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_19488),var(suc(zero)),b))))) = notb(andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_19488),arr(b,c)),btrue)),
inference(subst,[],[refute_0_42:[bind(X_6992,$fot(app(var(suc(suc(zero))),var(zero),X_19488)))]]) ).
cnf(refute_0_44,plain,
tc(cons(Z,Xs),app(X_96,var(zero),X_97),X_100) = andb(tc(cons(Z,Xs),X_96,arr(X_97,X_100)),tc(cons(Z,Xs),var(zero),X_97)),
inference(subst,[],[axiom_009:[bind(F,$fot(X_96)),bind(Tx,$fot(X_97)),bind(X,$fot(cons(Z,Xs))),bind(X2,$fot(var(zero))),bind(Z,$fot(X_100))]]) ).
cnf(refute_0_45,plain,
tc(cons(Z,Xs),var(zero),X_57) = aux(cons(Z,Xs),X_57,zero,index(cons(Z,Xs),zero)),
inference(subst,[],[axiom_014:[bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(zero)),bind(Z,$fot(X_57))]]) ).
cnf(refute_0_46,plain,
( index(cons(Z,Xs),zero) != just(Z)
| tc(cons(Z,Xs),var(zero),X_57) != aux(cons(Z,Xs),X_57,zero,index(cons(Z,Xs),zero))
| tc(cons(Z,Xs),var(zero),X_57) = aux(cons(Z,Xs),X_57,zero,just(Z)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_57),aux(cons(Z,Xs),X_57,zero,index(cons(Z,Xs),zero))) ),[1,3],$fot(just(Z))]]) ).
cnf(refute_0_47,plain,
( tc(cons(Z,Xs),var(zero),X_57) != aux(cons(Z,Xs),X_57,zero,index(cons(Z,Xs),zero))
| tc(cons(Z,Xs),var(zero),X_57) = aux(cons(Z,Xs),X_57,zero,just(Z)) ),
inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(Z)) )],[axiom_005,refute_0_46]) ).
cnf(refute_0_48,plain,
tc(cons(Z,Xs),var(zero),X_57) = aux(cons(Z,Xs),X_57,zero,just(Z)),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_57),aux(cons(Z,Xs),X_57,zero,index(cons(Z,Xs),zero))) )],[refute_0_45,refute_0_47]) ).
cnf(refute_0_49,plain,
aux(cons(Z,Xs),X_57,zero,just(Z)) = eq(Z,X_57),
inference(subst,[],[axiom_001:[bind(Tx3,$fot(Z)),bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(zero)),bind(Z,$fot(X_57))]]) ).
cnf(refute_0_50,plain,
( aux(cons(Z,Xs),X_57,zero,just(Z)) != eq(Z,X_57)
| tc(cons(Z,Xs),var(zero),X_57) != aux(cons(Z,Xs),X_57,zero,just(Z))
| tc(cons(Z,Xs),var(zero),X_57) = eq(Z,X_57) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_57),aux(cons(Z,Xs),X_57,zero,just(Z))) ),[1],$fot(eq(Z,X_57))]]) ).
cnf(refute_0_51,plain,
( tc(cons(Z,Xs),var(zero),X_57) != aux(cons(Z,Xs),X_57,zero,just(Z))
| tc(cons(Z,Xs),var(zero),X_57) = eq(Z,X_57) ),
inference(resolve,[$cnf( $equal(aux(cons(Z,Xs),X_57,zero,just(Z)),eq(Z,X_57)) )],[refute_0_49,refute_0_50]) ).
cnf(refute_0_52,plain,
tc(cons(Z,Xs),var(zero),X_57) = eq(Z,X_57),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_57),aux(cons(Z,Xs),X_57,zero,just(Z))) )],[refute_0_48,refute_0_51]) ).
cnf(refute_0_53,plain,
tc(cons(Z,Xs),var(zero),X_97) = eq(Z,X_97),
inference(subst,[],[refute_0_52:[bind(X_57,$fot(X_97))]]) ).
cnf(refute_0_54,plain,
( tc(cons(Z,Xs),app(X_96,var(zero),X_97),X_100) != andb(tc(cons(Z,Xs),X_96,arr(X_97,X_100)),tc(cons(Z,Xs),var(zero),X_97))
| tc(cons(Z,Xs),var(zero),X_97) != eq(Z,X_97)
| tc(cons(Z,Xs),app(X_96,var(zero),X_97),X_100) = andb(tc(cons(Z,Xs),X_96,arr(X_97,X_100)),eq(Z,X_97)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(Z,Xs),app(X_96,var(zero),X_97),X_100),andb(tc(cons(Z,Xs),X_96,arr(X_97,X_100)),tc(cons(Z,Xs),var(zero),X_97))) ),[1,1],$fot(eq(Z,X_97))]]) ).
cnf(refute_0_55,plain,
( tc(cons(Z,Xs),app(X_96,var(zero),X_97),X_100) != andb(tc(cons(Z,Xs),X_96,arr(X_97,X_100)),tc(cons(Z,Xs),var(zero),X_97))
| tc(cons(Z,Xs),app(X_96,var(zero),X_97),X_100) = andb(tc(cons(Z,Xs),X_96,arr(X_97,X_100)),eq(Z,X_97)) ),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),var(zero),X_97),eq(Z,X_97)) )],[refute_0_53,refute_0_54]) ).
cnf(refute_0_56,plain,
tc(cons(Z,Xs),app(X_96,var(zero),X_97),X_100) = andb(tc(cons(Z,Xs),X_96,arr(X_97,X_100)),eq(Z,X_97)),
inference(resolve,[$cnf( $equal(tc(cons(Z,Xs),app(X_96,var(zero),X_97),X_100),andb(tc(cons(Z,Xs),X_96,arr(X_97,X_100)),tc(cons(Z,Xs),var(zero),X_97))) )],[refute_0_44,refute_0_55]) ).
cnf(refute_0_57,plain,
tc(cons(X_1011,cons(X_349,cons(Z,Xs))),app(var(suc(suc(zero))),var(zero),X_1014),X_1012) = andb(tc(cons(X_1011,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),arr(X_1014,X_1012)),eq(X_1011,X_1014)),
inference(subst,[],[refute_0_56:[bind(Xs,$fot(cons(X_349,cons(Z,Xs)))),bind(Z,$fot(X_1011)),bind(X_100,$fot(X_1012)),bind(X_96,$fot(var(suc(suc(zero))))),bind(X_97,$fot(X_1014))]]) ).
cnf(refute_0_58,plain,
tc(cons(X_86,cons(Z,Xs)),var(suc(suc(N))),X_87) = aux(cons(X_86,cons(Z,Xs)),X_87,suc(suc(N)),index(cons(Z,Xs),suc(N))),
inference(subst,[],[refute_0_21:[bind(N,$fot(suc(N))),bind(Xs,$fot(cons(Z,Xs))),bind(Z,$fot(X_86)),bind(X_57,$fot(X_87))]]) ).
cnf(refute_0_59,plain,
( index(cons(Z,Xs),suc(N)) != index(Xs,N)
| tc(cons(X_86,cons(Z,Xs)),var(suc(suc(N))),X_87) != aux(cons(X_86,cons(Z,Xs)),X_87,suc(suc(N)),index(cons(Z,Xs),suc(N)))
| tc(cons(X_86,cons(Z,Xs)),var(suc(suc(N))),X_87) = aux(cons(X_86,cons(Z,Xs)),X_87,suc(suc(N)),index(Xs,N)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_86,cons(Z,Xs)),var(suc(suc(N))),X_87),aux(cons(X_86,cons(Z,Xs)),X_87,suc(suc(N)),index(cons(Z,Xs),suc(N)))) ),[1,3],$fot(index(Xs,N))]]) ).
cnf(refute_0_60,plain,
( tc(cons(X_86,cons(Z,Xs)),var(suc(suc(N))),X_87) != aux(cons(X_86,cons(Z,Xs)),X_87,suc(suc(N)),index(cons(Z,Xs),suc(N)))
| tc(cons(X_86,cons(Z,Xs)),var(suc(suc(N))),X_87) = aux(cons(X_86,cons(Z,Xs)),X_87,suc(suc(N)),index(Xs,N)) ),
inference(resolve,[$cnf( $equal(index(cons(Z,Xs),suc(N)),index(Xs,N)) )],[axiom_006,refute_0_59]) ).
cnf(refute_0_61,plain,
tc(cons(X_86,cons(Z,Xs)),var(suc(suc(N))),X_87) = aux(cons(X_86,cons(Z,Xs)),X_87,suc(suc(N)),index(Xs,N)),
inference(resolve,[$cnf( $equal(tc(cons(X_86,cons(Z,Xs)),var(suc(suc(N))),X_87),aux(cons(X_86,cons(Z,Xs)),X_87,suc(suc(N)),index(cons(Z,Xs),suc(N)))) )],[refute_0_58,refute_0_60]) ).
cnf(refute_0_62,plain,
tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351) = aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),index(cons(Z,Xs),zero)),
inference(subst,[],[refute_0_61:[bind(N,$fot(zero)),bind(Xs,$fot(cons(Z,Xs))),bind(Z,$fot(X_349)),bind(X_86,$fot(X_350)),bind(X_87,$fot(X_351))]]) ).
cnf(refute_0_63,plain,
( index(cons(Z,Xs),zero) != just(Z)
| tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351) != aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),index(cons(Z,Xs),zero))
| tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351) = aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),just(Z)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351),aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),index(cons(Z,Xs),zero))) ),[1,3],$fot(just(Z))]]) ).
cnf(refute_0_64,plain,
( tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351) != aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),index(cons(Z,Xs),zero))
| tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351) = aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),just(Z)) ),
inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(Z)) )],[axiom_005,refute_0_63]) ).
cnf(refute_0_65,plain,
tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351) = aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),just(Z)),
inference(resolve,[$cnf( $equal(tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351),aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),index(cons(Z,Xs),zero))) )],[refute_0_62,refute_0_64]) ).
cnf(refute_0_66,plain,
aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),just(Z)) = eq(Z,X_351),
inference(subst,[],[axiom_001:[bind(Tx3,$fot(Z)),bind(X,$fot(cons(X_350,cons(X_349,cons(Z,Xs))))),bind(X3,$fot(suc(suc(zero)))),bind(Z,$fot(X_351))]]) ).
cnf(refute_0_67,plain,
( aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),just(Z)) != eq(Z,X_351)
| tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351) != aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),just(Z))
| tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351) = eq(Z,X_351) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351),aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),just(Z))) ),[1],$fot(eq(Z,X_351))]]) ).
cnf(refute_0_68,plain,
( tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351) != aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),just(Z))
| tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351) = eq(Z,X_351) ),
inference(resolve,[$cnf( $equal(aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),just(Z)),eq(Z,X_351)) )],[refute_0_66,refute_0_67]) ).
cnf(refute_0_69,plain,
tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351) = eq(Z,X_351),
inference(resolve,[$cnf( $equal(tc(cons(X_350,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),X_351),aux(cons(X_350,cons(X_349,cons(Z,Xs))),X_351,suc(suc(zero)),just(Z))) )],[refute_0_65,refute_0_68]) ).
cnf(refute_0_70,plain,
tc(cons(X_1011,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),arr(X_1014,X_1012)) = eq(Z,arr(X_1014,X_1012)),
inference(subst,[],[refute_0_69:[bind(X_350,$fot(X_1011)),bind(X_351,$fot(arr(X_1014,X_1012)))]]) ).
cnf(refute_0_71,plain,
( tc(cons(X_1011,cons(X_349,cons(Z,Xs))),app(var(suc(suc(zero))),var(zero),X_1014),X_1012) != andb(tc(cons(X_1011,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),arr(X_1014,X_1012)),eq(X_1011,X_1014))
| tc(cons(X_1011,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),arr(X_1014,X_1012)) != eq(Z,arr(X_1014,X_1012))
| tc(cons(X_1011,cons(X_349,cons(Z,Xs))),app(var(suc(suc(zero))),var(zero),X_1014),X_1012) = andb(eq(Z,arr(X_1014,X_1012)),eq(X_1011,X_1014)) ),
introduced(tautology,[equality,[$cnf( $equal(tc(cons(X_1011,cons(X_349,cons(Z,Xs))),app(var(suc(suc(zero))),var(zero),X_1014),X_1012),andb(tc(cons(X_1011,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),arr(X_1014,X_1012)),eq(X_1011,X_1014))) ),[1,0],$fot(eq(Z,arr(X_1014,X_1012)))]]) ).
cnf(refute_0_72,plain,
( tc(cons(X_1011,cons(X_349,cons(Z,Xs))),app(var(suc(suc(zero))),var(zero),X_1014),X_1012) != andb(tc(cons(X_1011,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),arr(X_1014,X_1012)),eq(X_1011,X_1014))
| tc(cons(X_1011,cons(X_349,cons(Z,Xs))),app(var(suc(suc(zero))),var(zero),X_1014),X_1012) = andb(eq(Z,arr(X_1014,X_1012)),eq(X_1011,X_1014)) ),
inference(resolve,[$cnf( $equal(tc(cons(X_1011,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),arr(X_1014,X_1012)),eq(Z,arr(X_1014,X_1012))) )],[refute_0_70,refute_0_71]) ).
cnf(refute_0_73,plain,
tc(cons(X_1011,cons(X_349,cons(Z,Xs))),app(var(suc(suc(zero))),var(zero),X_1014),X_1012) = andb(eq(Z,arr(X_1014,X_1012)),eq(X_1011,X_1014)),
inference(resolve,[$cnf( $equal(tc(cons(X_1011,cons(X_349,cons(Z,Xs))),app(var(suc(suc(zero))),var(zero),X_1014),X_1012),andb(tc(cons(X_1011,cons(X_349,cons(Z,Xs))),var(suc(suc(zero))),arr(X_1014,X_1012)),eq(X_1011,X_1014))) )],[refute_0_57,refute_0_72]) ).
cnf(refute_0_74,plain,
tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_19488),arr(b,c)) = andb(eq(arr(a,arr(b,c)),arr(X_19488,arr(b,c))),eq(a,X_19488)),
inference(subst,[],[refute_0_73:[bind(Xs,$fot(nil)),bind(Z,$fot(arr(a,arr(b,c)))),bind(X_1011,$fot(a)),bind(X_1012,$fot(arr(b,c))),bind(X_1014,$fot(X_19488)),bind(X_349,$fot(b))]]) ).
cnf(refute_0_75,plain,
( sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_19488),var(suc(zero)),b))))) != notb(andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_19488),arr(b,c)),btrue))
| tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_19488),arr(b,c)) != andb(eq(arr(a,arr(b,c)),arr(X_19488,arr(b,c))),eq(a,X_19488))
| sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_19488),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(X_19488,arr(b,c))),eq(a,X_19488)),btrue)) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_19488),var(suc(zero)),b))))),notb(andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_19488),arr(b,c)),btrue))) ),[1,0,0],$fot(andb(eq(arr(a,arr(b,c)),arr(X_19488,arr(b,c))),eq(a,X_19488)))]]) ).
cnf(refute_0_76,plain,
( sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_19488),var(suc(zero)),b))))) != notb(andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_19488),arr(b,c)),btrue))
| sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_19488),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(X_19488,arr(b,c))),eq(a,X_19488)),btrue)) ),
inference(resolve,[$cnf( $equal(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_19488),arr(b,c)),andb(eq(arr(a,arr(b,c)),arr(X_19488,arr(b,c))),eq(a,X_19488))) )],[refute_0_74,refute_0_75]) ).
cnf(refute_0_77,plain,
sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_19488),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(X_19488,arr(b,c))),eq(a,X_19488)),btrue)),
inference(resolve,[$cnf( $equal(sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),X_19488),var(suc(zero)),b))))),notb(andb(tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),app(var(suc(suc(zero))),var(zero),X_19488),arr(b,c)),btrue))) )],[refute_0_43,refute_0_76]) ).
cnf(refute_0_78,plain,
sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),eq(a,a)),btrue)),
inference(subst,[],[refute_0_77:[bind(X_19488,$fot(a))]]) ).
cnf(refute_0_79,plain,
eq(a,a) = btrue,
inference(subst,[],[axiom_046:[bind(X,$fot(a))]]) ).
cnf(refute_0_80,plain,
( eq(a,a) != btrue
| sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) != notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),eq(a,a)),btrue))
| sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),eq(a,a)),btrue))) ),[1,0,0,1],$fot(btrue)]]) ).
cnf(refute_0_81,plain,
( sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) != notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),eq(a,a)),btrue))
| sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) ),
inference(resolve,[$cnf( $equal(eq(a,a),btrue) )],[refute_0_79,refute_0_80]) ).
cnf(refute_0_82,plain,
sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)),
inference(resolve,[$cnf( $equal(sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),eq(a,a)),btrue))) )],[refute_0_78,refute_0_81]) ).
cnf(refute_0_83,plain,
andb(btrue,btrue) = btrue,
inference(subst,[],[axiom_007:[bind(Q,$fot(btrue))]]) ).
cnf(refute_0_84,plain,
eq(c,c) = btrue,
inference(subst,[],[axiom_046:[bind(X,$fot(c))]]) ).
cnf(refute_0_85,plain,
( eq(X_1633,X_1633) != btrue
| eq(arr(X_1633,X_1632),arr(X_1633,X_1631)) = eq(X_1632,X_1631) ),
inference(subst,[],[axiom_028:[bind(X,$fot(X_1633)),bind(X2,$fot(X_1631)),bind(Y,$fot(X_1632)),bind(Z,$fot(X_1633))]]) ).
cnf(refute_0_86,plain,
eq(X_1633,X_1633) = btrue,
inference(subst,[],[axiom_046:[bind(X,$fot(X_1633))]]) ).
cnf(refute_0_87,plain,
( btrue != btrue
| eq(X_1633,X_1633) != btrue
| eq(X_1633,X_1633) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(eq(X_1633,X_1633),btrue) ),[1],$fot(btrue)]]) ).
cnf(refute_0_88,plain,
( btrue != btrue
| eq(X_1633,X_1633) = btrue ),
inference(resolve,[$cnf( $equal(eq(X_1633,X_1633),btrue) )],[refute_0_86,refute_0_87]) ).
cnf(refute_0_89,plain,
( btrue != btrue
| eq(arr(X_1633,X_1632),arr(X_1633,X_1631)) = eq(X_1632,X_1631) ),
inference(resolve,[$cnf( $equal(eq(X_1633,X_1633),btrue) )],[refute_0_88,refute_0_85]) ).
cnf(refute_0_90,plain,
btrue = btrue,
introduced(tautology,[refl,[$fot(btrue)]]) ).
cnf(refute_0_91,plain,
eq(arr(X_1633,X_1632),arr(X_1633,X_1631)) = eq(X_1632,X_1631),
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_90,refute_0_89]) ).
cnf(refute_0_92,plain,
eq(arr(b,c),arr(b,c)) = eq(c,c),
inference(subst,[],[refute_0_91:[bind(X_1631,$fot(c)),bind(X_1632,$fot(c)),bind(X_1633,$fot(b))]]) ).
cnf(refute_0_93,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_94,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_95,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_93,refute_0_94]) ).
cnf(refute_0_96,plain,
( Y0 != X0
| Y0 != Z0
| X0 = Z0 ),
introduced(tautology,[equality,[$cnf( $equal(Y0,Z0) ),[0],$fot(X0)]]) ).
cnf(refute_0_97,plain,
( X0 != Y0
| Y0 != Z0
| X0 = Z0 ),
inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_95,refute_0_96]) ).
cnf(refute_0_98,plain,
( eq(arr(b,c),arr(b,c)) != eq(c,c)
| eq(c,c) != btrue
| eq(arr(b,c),arr(b,c)) = btrue ),
inference(subst,[],[refute_0_97:[bind(X0,$fot(eq(arr(b,c),arr(b,c)))),bind(Y0,$fot(eq(c,c))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_99,plain,
( eq(c,c) != btrue
| eq(arr(b,c),arr(b,c)) = btrue ),
inference(resolve,[$cnf( $equal(eq(arr(b,c),arr(b,c)),eq(c,c)) )],[refute_0_92,refute_0_98]) ).
cnf(refute_0_100,plain,
eq(arr(b,c),arr(b,c)) = btrue,
inference(resolve,[$cnf( $equal(eq(c,c),btrue) )],[refute_0_84,refute_0_99]) ).
cnf(refute_0_101,plain,
eq(arr(a,arr(b,c)),arr(a,arr(b,c))) = eq(arr(b,c),arr(b,c)),
inference(subst,[],[refute_0_91:[bind(X_1631,$fot(arr(b,c))),bind(X_1632,$fot(arr(b,c))),bind(X_1633,$fot(a))]]) ).
cnf(refute_0_102,plain,
( eq(arr(a,arr(b,c)),arr(a,arr(b,c))) != eq(arr(b,c),arr(b,c))
| eq(arr(b,c),arr(b,c)) != btrue
| eq(arr(a,arr(b,c)),arr(a,arr(b,c))) = btrue ),
inference(subst,[],[refute_0_97:[bind(X0,$fot(eq(arr(a,arr(b,c)),arr(a,arr(b,c))))),bind(Y0,$fot(eq(arr(b,c),arr(b,c)))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_103,plain,
( eq(arr(b,c),arr(b,c)) != btrue
| eq(arr(a,arr(b,c)),arr(a,arr(b,c))) = btrue ),
inference(resolve,[$cnf( $equal(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),eq(arr(b,c),arr(b,c))) )],[refute_0_101,refute_0_102]) ).
cnf(refute_0_104,plain,
eq(arr(a,arr(b,c)),arr(a,arr(b,c))) = btrue,
inference(resolve,[$cnf( $equal(eq(arr(b,c),arr(b,c)),btrue) )],[refute_0_100,refute_0_103]) ).
cnf(refute_0_105,plain,
andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),
introduced(tautology,[refl,[$fot(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue))]]) ).
cnf(refute_0_106,plain,
( andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) != andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue)
| eq(arr(a,arr(b,c)),arr(a,arr(b,c))) != btrue
| andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = andb(btrue,btrue) ),
introduced(tautology,[equality,[$cnf( $equal(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue)) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_107,plain,
( eq(arr(a,arr(b,c)),arr(a,arr(b,c))) != btrue
| andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = andb(btrue,btrue) ),
inference(resolve,[$cnf( $equal(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue)) )],[refute_0_105,refute_0_106]) ).
cnf(refute_0_108,plain,
andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = andb(btrue,btrue),
inference(resolve,[$cnf( $equal(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) )],[refute_0_104,refute_0_107]) ).
cnf(refute_0_109,plain,
( andb(btrue,btrue) != btrue
| andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) != andb(btrue,btrue)
| andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = btrue ),
inference(subst,[],[refute_0_97:[bind(X0,$fot(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue))),bind(Y0,$fot(andb(btrue,btrue))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_110,plain,
( andb(btrue,btrue) != btrue
| andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = btrue ),
inference(resolve,[$cnf( $equal(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),andb(btrue,btrue)) )],[refute_0_108,refute_0_109]) ).
cnf(refute_0_111,plain,
andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) = btrue,
inference(resolve,[$cnf( $equal(andb(btrue,btrue),btrue) )],[refute_0_83,refute_0_110]) ).
cnf(refute_0_112,plain,
andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue),
introduced(tautology,[refl,[$fot(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))]]) ).
cnf(refute_0_113,plain,
( andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) != andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)
| andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) != btrue
| andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = andb(btrue,btrue) ),
introduced(tautology,[equality,[$cnf( $equal(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue),andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_114,plain,
( andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue) != btrue
| andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = andb(btrue,btrue) ),
inference(resolve,[$cnf( $equal(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue),andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) )],[refute_0_112,refute_0_113]) ).
cnf(refute_0_115,plain,
andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = andb(btrue,btrue),
inference(resolve,[$cnf( $equal(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) )],[refute_0_111,refute_0_114]) ).
cnf(refute_0_116,plain,
( andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) != andb(btrue,btrue)
| andb(btrue,btrue) != btrue
| andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = btrue ),
inference(subst,[],[refute_0_97:[bind(X0,$fot(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))),bind(Y0,$fot(andb(btrue,btrue))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_117,plain,
( andb(btrue,btrue) != btrue
| andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = btrue ),
inference(resolve,[$cnf( $equal(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue),andb(btrue,btrue)) )],[refute_0_115,refute_0_116]) ).
cnf(refute_0_118,plain,
andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) = btrue,
inference(resolve,[$cnf( $equal(andb(btrue,btrue),btrue) )],[refute_0_83,refute_0_117]) ).
cnf(refute_0_119,plain,
notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)),
introduced(tautology,[refl,[$fot(notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)))]]) ).
cnf(refute_0_120,plain,
( andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) != btrue
| notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) != notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))
| notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = notb(btrue) ),
introduced(tautology,[equality,[$cnf( $equal(notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)),notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_121,plain,
( andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue) != btrue
| notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = notb(btrue) ),
inference(resolve,[$cnf( $equal(notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)),notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))) )],[refute_0_119,refute_0_120]) ).
cnf(refute_0_122,plain,
notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = notb(btrue),
inference(resolve,[$cnf( $equal(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue),btrue) )],[refute_0_118,refute_0_121]) ).
cnf(refute_0_123,plain,
( notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) != notb(btrue)
| notb(btrue) != bfalse
| notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = bfalse ),
inference(subst,[],[refute_0_97:[bind(X0,$fot(notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)))),bind(Y0,$fot(notb(btrue))),bind(Z0,$fot(bfalse))]]) ).
cnf(refute_0_124,plain,
( notb(btrue) != bfalse
| notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = bfalse ),
inference(resolve,[$cnf( $equal(notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)),notb(btrue)) )],[refute_0_122,refute_0_123]) ).
cnf(refute_0_125,plain,
notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) = bfalse,
inference(resolve,[$cnf( $equal(notb(btrue),bfalse) )],[axiom_002,refute_0_124]) ).
cnf(refute_0_126,plain,
( notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)) != bfalse
| sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) != notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))
| sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))) ),[1],$fot(bfalse)]]) ).
cnf(refute_0_127,plain,
( sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) != notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))
| sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = bfalse ),
inference(resolve,[$cnf( $equal(notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue)),bfalse) )],[refute_0_125,refute_0_126]) ).
cnf(refute_0_128,plain,
sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) = bfalse,
inference(resolve,[$cnf( $equal(sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),notb(andb(andb(eq(arr(a,arr(b,c)),arr(a,arr(b,c))),btrue),btrue))) )],[refute_0_82,refute_0_127]) ).
cnf(refute_0_129,plain,
( eq4(bfalse,bfalse) != btrue
| sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))) != bfalse
| eq4(sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( ~ $equal(eq4(sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),bfalse),btrue) ),[0,0],$fot(bfalse)]]) ).
cnf(refute_0_130,plain,
( eq4(bfalse,bfalse) != btrue
| eq4(sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),bfalse) = btrue ),
inference(resolve,[$cnf( $equal(sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),bfalse) )],[refute_0_128,refute_0_129]) ).
cnf(refute_0_131,plain,
eq4(bfalse,bfalse) != btrue,
inference(resolve,[$cnf( $equal(eq4(sat_synth_flip(lam(lam(lam(app(app(var(suc(suc(zero))),var(zero),a),var(suc(zero)),b))))),bfalse),btrue) )],[refute_0_130,refute_0_0]) ).
cnf(refute_0_132,plain,
eq4(bfalse,bfalse) = btrue,
inference(subst,[],[axiom_049:[bind(X,$fot(bfalse))]]) ).
cnf(refute_0_133,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_134,plain,
( btrue != btrue
| eq4(bfalse,bfalse) = btrue ),
inference(resolve,[$cnf( $equal(eq4(bfalse,bfalse),btrue) )],[refute_0_132,refute_0_133]) ).
cnf(refute_0_135,plain,
btrue != btrue,
inference(resolve,[$cnf( $equal(eq4(bfalse,bfalse),btrue) )],[refute_0_134,refute_0_131]) ).
cnf(refute_0_136,plain,
$false,
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_90,refute_0_135]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX220-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 : n014.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:27:51 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 111.74/111.95 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 111.74/111.95
% 111.74/111.95 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 111.74/111.96
%------------------------------------------------------------------------------