%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWX199-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n025.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:32 PM UTC 2026
% Result : Unsatisfiable 2.74s 2.93s
% Output : CNFRefutation 2.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 53
% Syntax : Number of clauses : 166 ( 91 unt; 0 nHn; 71 RR)
% Number of literals : 275 ( 274 equ; 113 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 : 14 ( 14 usr; 4 con; 0-5 aty)
% Number of variables : 413 ( 32 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
aux(Z,Xs,Y2,Ys,btrue) = cons(Z,merge(Xs,cons(Y2,Ys))) ).
cnf(axiom_002,axiom,
leqNat(z,Y) = btrue ).
cnf(axiom_004,axiom,
leqNat(s(Z),s(M)) = leqNat(Z,M) ).
cnf(axiom_005,axiom,
merge(nil,Y) = Y ).
cnf(axiom_006,axiom,
merge(cons(Z,Xs),nil) = cons(Z,Xs) ).
cnf(axiom_007,axiom,
merge(cons(Z,Xs),cons(Y2,Ys)) = aux(Z,Xs,Y2,Ys,leqNat(Z,Y2)) ).
cnf(axiom_008,axiom,
impl(btrue,Q) = Q ).
cnf(axiom_010,axiom,
prop_merge_comm(X,Y,Z) = impl(eq(merge(X,Y),merge(Y,X)),impl(eq(merge(X,Z),merge(Z,X)),eq(merge(Y,Z),merge(Z,Y)))) ).
cnf(axiom_015,axiom,
eq2(s(X),z) = bfalse ).
cnf(axiom_016,axiom,
eq(X,X) = btrue ).
cnf(axiom_017,axiom,
eq2(X,X) = btrue ).
cnf(axiom_018,axiom,
eq3(X,X) = btrue ).
cnf(axiom_019,axiom,
( eq2(X,Z) != bfalse
| eq(cons(X,Y),cons(Z,X2)) = bfalse ) ).
cnf(axiom_020,axiom,
( eq2(X,Z) != btrue
| eq(cons(X,Y),cons(Z,X2)) = eq(Y,X2) ) ).
cnf(goal,negated_conjecture,
eq3(prop_merge_comm(X,Y,Z),bfalse) != btrue ).
cnf(refute_0_0,plain,
eq3(prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_994))),bfalse) != btrue,
inference(subst,[],[goal:[bind(X,$fot(nil)),bind(Y,$fot(cons(s(z),nil))),bind(Z,$fot(cons(s(z),cons(z,X_994))))]]) ).
cnf(refute_0_1,plain,
prop_merge_comm(nil,cons(Z,Xs),X_92) = impl(eq(merge(nil,cons(Z,Xs)),merge(cons(Z,Xs),nil)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),
inference(subst,[],[axiom_010:[bind(X,$fot(nil)),bind(Y,$fot(cons(Z,Xs))),bind(Z,$fot(X_92))]]) ).
cnf(refute_0_2,plain,
( merge(cons(Z,Xs),nil) != cons(Z,Xs)
| prop_merge_comm(nil,cons(Z,Xs),X_92) != impl(eq(merge(nil,cons(Z,Xs)),merge(cons(Z,Xs),nil)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))
| prop_merge_comm(nil,cons(Z,Xs),X_92) = impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) ),
introduced(tautology,[equality,[$cnf( $equal(prop_merge_comm(nil,cons(Z,Xs),X_92),impl(eq(merge(nil,cons(Z,Xs)),merge(cons(Z,Xs),nil)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))) ),[1,0,1],$fot(cons(Z,Xs))]]) ).
cnf(refute_0_3,plain,
( prop_merge_comm(nil,cons(Z,Xs),X_92) != impl(eq(merge(nil,cons(Z,Xs)),merge(cons(Z,Xs),nil)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))
| prop_merge_comm(nil,cons(Z,Xs),X_92) = impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) ),
inference(resolve,[$cnf( $equal(merge(cons(Z,Xs),nil),cons(Z,Xs)) )],[axiom_006,refute_0_2]) ).
cnf(refute_0_4,plain,
prop_merge_comm(nil,cons(Z,Xs),X_92) = impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),
inference(resolve,[$cnf( $equal(prop_merge_comm(nil,cons(Z,Xs),X_92),impl(eq(merge(nil,cons(Z,Xs)),merge(cons(Z,Xs),nil)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))) )],[refute_0_1,refute_0_3]) ).
cnf(refute_0_5,plain,
impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))),
inference(subst,[],[axiom_008:[bind(Q,$fot(impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))))]]) ).
cnf(refute_0_6,plain,
merge(nil,X_92) = X_92,
inference(subst,[],[axiom_005:[bind(Y,$fot(X_92))]]) ).
cnf(refute_0_7,plain,
eq(merge(nil,X_92),merge(X_92,nil)) = eq(merge(nil,X_92),merge(X_92,nil)),
introduced(tautology,[refl,[$fot(eq(merge(nil,X_92),merge(X_92,nil)))]]) ).
cnf(refute_0_8,plain,
( eq(merge(nil,X_92),merge(X_92,nil)) != eq(merge(nil,X_92),merge(X_92,nil))
| merge(nil,X_92) != X_92
| eq(merge(nil,X_92),merge(X_92,nil)) = eq(X_92,merge(X_92,nil)) ),
introduced(tautology,[equality,[$cnf( $equal(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(nil,X_92),merge(X_92,nil))) ),[1,0],$fot(X_92)]]) ).
cnf(refute_0_9,plain,
( merge(nil,X_92) != X_92
| eq(merge(nil,X_92),merge(X_92,nil)) = eq(X_92,merge(X_92,nil)) ),
inference(resolve,[$cnf( $equal(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(nil,X_92),merge(X_92,nil))) )],[refute_0_7,refute_0_8]) ).
cnf(refute_0_10,plain,
eq(merge(nil,X_92),merge(X_92,nil)) = eq(X_92,merge(X_92,nil)),
inference(resolve,[$cnf( $equal(merge(nil,X_92),X_92) )],[refute_0_6,refute_0_9]) ).
cnf(refute_0_11,plain,
impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) = impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))),
introduced(tautology,[refl,[$fot(impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))]]) ).
cnf(refute_0_12,plain,
( eq(merge(nil,X_92),merge(X_92,nil)) != eq(X_92,merge(X_92,nil))
| impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) != impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))
| impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) = impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) ),
introduced(tautology,[equality,[$cnf( $equal(impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) ),[1,0],$fot(eq(X_92,merge(X_92,nil)))]]) ).
cnf(refute_0_13,plain,
( eq(merge(nil,X_92),merge(X_92,nil)) != eq(X_92,merge(X_92,nil))
| impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) = impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) ),
inference(resolve,[$cnf( $equal(impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) )],[refute_0_11,refute_0_12]) ).
cnf(refute_0_14,plain,
impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) = impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))),
inference(resolve,[$cnf( $equal(eq(merge(nil,X_92),merge(X_92,nil)),eq(X_92,merge(X_92,nil))) )],[refute_0_10,refute_0_13]) ).
cnf(refute_0_15,plain,
impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),
introduced(tautology,[refl,[$fot(impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))))]]) ).
cnf(refute_0_16,plain,
( impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) != impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))
| impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) != impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))
| impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) ),
introduced(tautology,[equality,[$cnf( $equal(impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))) ),[1,1],$fot(impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))]]) ).
cnf(refute_0_17,plain,
( impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) != impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))
| impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) ),
inference(resolve,[$cnf( $equal(impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))) )],[refute_0_15,refute_0_16]) ).
cnf(refute_0_18,plain,
impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),
inference(resolve,[$cnf( $equal(impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))),impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) )],[refute_0_14,refute_0_17]) ).
cnf(refute_0_19,plain,
eq(cons(Z,Xs),cons(Z,Xs)) = btrue,
inference(subst,[],[axiom_016:[bind(X,$fot(cons(Z,Xs)))]]) ).
cnf(refute_0_20,plain,
merge(nil,cons(Z,Xs)) = cons(Z,Xs),
inference(subst,[],[axiom_005:[bind(Y,$fot(cons(Z,Xs)))]]) ).
cnf(refute_0_21,plain,
eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)) = eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),
introduced(tautology,[refl,[$fot(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)))]]) ).
cnf(refute_0_22,plain,
( eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)) != eq(merge(nil,cons(Z,Xs)),cons(Z,Xs))
| merge(nil,cons(Z,Xs)) != cons(Z,Xs)
| eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)) = eq(cons(Z,Xs),cons(Z,Xs)) ),
introduced(tautology,[equality,[$cnf( $equal(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),eq(merge(nil,cons(Z,Xs)),cons(Z,Xs))) ),[1,0],$fot(cons(Z,Xs))]]) ).
cnf(refute_0_23,plain,
( merge(nil,cons(Z,Xs)) != cons(Z,Xs)
| eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)) = eq(cons(Z,Xs),cons(Z,Xs)) ),
inference(resolve,[$cnf( $equal(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),eq(merge(nil,cons(Z,Xs)),cons(Z,Xs))) )],[refute_0_21,refute_0_22]) ).
cnf(refute_0_24,plain,
eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)) = eq(cons(Z,Xs),cons(Z,Xs)),
inference(resolve,[$cnf( $equal(merge(nil,cons(Z,Xs)),cons(Z,Xs)) )],[refute_0_20,refute_0_23]) ).
cnf(refute_0_25,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_26,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_27,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_25,refute_0_26]) ).
cnf(refute_0_28,plain,
( Y0 != X0
| Y0 != Z0
| X0 = Z0 ),
introduced(tautology,[equality,[$cnf( $equal(Y0,Z0) ),[0],$fot(X0)]]) ).
cnf(refute_0_29,plain,
( X0 != Y0
| Y0 != Z0
| X0 = Z0 ),
inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_27,refute_0_28]) ).
cnf(refute_0_30,plain,
( eq(cons(Z,Xs),cons(Z,Xs)) != btrue
| eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)) != eq(cons(Z,Xs),cons(Z,Xs))
| eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)) = btrue ),
inference(subst,[],[refute_0_29:[bind(X0,$fot(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)))),bind(Y0,$fot(eq(cons(Z,Xs),cons(Z,Xs)))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_31,plain,
( eq(cons(Z,Xs),cons(Z,Xs)) != btrue
| eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)) = btrue ),
inference(resolve,[$cnf( $equal(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),eq(cons(Z,Xs),cons(Z,Xs))) )],[refute_0_24,refute_0_30]) ).
cnf(refute_0_32,plain,
eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)) = btrue,
inference(resolve,[$cnf( $equal(eq(cons(Z,Xs),cons(Z,Xs)),btrue) )],[refute_0_19,refute_0_31]) ).
cnf(refute_0_33,plain,
impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),
introduced(tautology,[refl,[$fot(impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))))]]) ).
cnf(refute_0_34,plain,
( eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)) != btrue
| impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) != impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))
| impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) ),
introduced(tautology,[equality,[$cnf( $equal(impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_35,plain,
( eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)) != btrue
| impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) ),
inference(resolve,[$cnf( $equal(impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))) )],[refute_0_33,refute_0_34]) ).
cnf(refute_0_36,plain,
impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),
inference(resolve,[$cnf( $equal(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),btrue) )],[refute_0_32,refute_0_35]) ).
cnf(refute_0_37,plain,
( impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) != impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))
| impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) != impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))
| impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) ),
inference(subst,[],[refute_0_29:[bind(X0,$fot(impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))))),bind(Y0,$fot(impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))))),bind(Z0,$fot(impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))))]]) ).
cnf(refute_0_38,plain,
( impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) != impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))
| impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) ),
inference(resolve,[$cnf( $equal(impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))) )],[refute_0_36,refute_0_37]) ).
cnf(refute_0_39,plain,
impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),
inference(resolve,[$cnf( $equal(impl(btrue,impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))) )],[refute_0_18,refute_0_38]) ).
cnf(refute_0_40,plain,
( impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) != impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))
| impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) != impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))
| impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) ),
inference(subst,[],[refute_0_29:[bind(X0,$fot(impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))))),bind(Y0,$fot(impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))))),bind(Z0,$fot(impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))))]]) ).
cnf(refute_0_41,plain,
( impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) != impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))
| impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) ),
inference(resolve,[$cnf( $equal(impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))) )],[refute_0_39,refute_0_40]) ).
cnf(refute_0_42,plain,
impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) = impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))),
inference(resolve,[$cnf( $equal(impl(btrue,impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) )],[refute_0_5,refute_0_41]) ).
cnf(refute_0_43,plain,
( impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) != impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))
| prop_merge_comm(nil,cons(Z,Xs),X_92) != impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))
| prop_merge_comm(nil,cons(Z,Xs),X_92) = impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) ),
introduced(tautology,[equality,[$cnf( $equal(prop_merge_comm(nil,cons(Z,Xs),X_92),impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))) ),[1],$fot(impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))]]) ).
cnf(refute_0_44,plain,
( prop_merge_comm(nil,cons(Z,Xs),X_92) != impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))
| prop_merge_comm(nil,cons(Z,Xs),X_92) = impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))) ),
inference(resolve,[$cnf( $equal(impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))),impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs))))) )],[refute_0_42,refute_0_43]) ).
cnf(refute_0_45,plain,
prop_merge_comm(nil,cons(Z,Xs),X_92) = impl(eq(X_92,merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))),
inference(resolve,[$cnf( $equal(prop_merge_comm(nil,cons(Z,Xs),X_92),impl(eq(merge(nil,cons(Z,Xs)),cons(Z,Xs)),impl(eq(merge(nil,X_92),merge(X_92,nil)),eq(merge(cons(Z,Xs),X_92),merge(X_92,cons(Z,Xs)))))) )],[refute_0_4,refute_0_44]) ).
cnf(refute_0_46,plain,
prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)) = impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(merge(cons(s(z),X_144),cons(s(X_75),X_78)),merge(cons(s(X_75),X_78),cons(s(z),X_144)))),
inference(subst,[],[refute_0_45:[bind(Xs,$fot(X_144)),bind(Z,$fot(s(z))),bind(X_92,$fot(cons(s(X_75),X_78)))]]) ).
cnf(refute_0_47,plain,
merge(cons(s(Z),X_30),cons(s(M),X_32)) = aux(s(Z),X_30,s(M),X_32,leqNat(s(Z),s(M))),
inference(subst,[],[axiom_007:[bind(Xs,$fot(X_30)),bind(Y2,$fot(s(M))),bind(Ys,$fot(X_32)),bind(Z,$fot(s(Z)))]]) ).
cnf(refute_0_48,plain,
( leqNat(s(Z),s(M)) != leqNat(Z,M)
| merge(cons(s(Z),X_30),cons(s(M),X_32)) != aux(s(Z),X_30,s(M),X_32,leqNat(s(Z),s(M)))
| merge(cons(s(Z),X_30),cons(s(M),X_32)) = aux(s(Z),X_30,s(M),X_32,leqNat(Z,M)) ),
introduced(tautology,[equality,[$cnf( $equal(merge(cons(s(Z),X_30),cons(s(M),X_32)),aux(s(Z),X_30,s(M),X_32,leqNat(s(Z),s(M)))) ),[1,4],$fot(leqNat(Z,M))]]) ).
cnf(refute_0_49,plain,
( merge(cons(s(Z),X_30),cons(s(M),X_32)) != aux(s(Z),X_30,s(M),X_32,leqNat(s(Z),s(M)))
| merge(cons(s(Z),X_30),cons(s(M),X_32)) = aux(s(Z),X_30,s(M),X_32,leqNat(Z,M)) ),
inference(resolve,[$cnf( $equal(leqNat(s(Z),s(M)),leqNat(Z,M)) )],[axiom_004,refute_0_48]) ).
cnf(refute_0_50,plain,
merge(cons(s(Z),X_30),cons(s(M),X_32)) = aux(s(Z),X_30,s(M),X_32,leqNat(Z,M)),
inference(resolve,[$cnf( $equal(merge(cons(s(Z),X_30),cons(s(M),X_32)),aux(s(Z),X_30,s(M),X_32,leqNat(s(Z),s(M)))) )],[refute_0_47,refute_0_49]) ).
cnf(refute_0_51,plain,
merge(cons(s(z),X_77),cons(s(X_75),X_78)) = aux(s(z),X_77,s(X_75),X_78,leqNat(z,X_75)),
inference(subst,[],[refute_0_50:[bind(M,$fot(X_75)),bind(Z,$fot(z)),bind(X_30,$fot(X_77)),bind(X_32,$fot(X_78))]]) ).
cnf(refute_0_52,plain,
leqNat(z,X_75) = btrue,
inference(subst,[],[axiom_002:[bind(Y,$fot(X_75))]]) ).
cnf(refute_0_53,plain,
( leqNat(z,X_75) != btrue
| merge(cons(s(z),X_77),cons(s(X_75),X_78)) != aux(s(z),X_77,s(X_75),X_78,leqNat(z,X_75))
| merge(cons(s(z),X_77),cons(s(X_75),X_78)) = aux(s(z),X_77,s(X_75),X_78,btrue) ),
introduced(tautology,[equality,[$cnf( $equal(merge(cons(s(z),X_77),cons(s(X_75),X_78)),aux(s(z),X_77,s(X_75),X_78,leqNat(z,X_75))) ),[1,4],$fot(btrue)]]) ).
cnf(refute_0_54,plain,
( merge(cons(s(z),X_77),cons(s(X_75),X_78)) != aux(s(z),X_77,s(X_75),X_78,leqNat(z,X_75))
| merge(cons(s(z),X_77),cons(s(X_75),X_78)) = aux(s(z),X_77,s(X_75),X_78,btrue) ),
inference(resolve,[$cnf( $equal(leqNat(z,X_75),btrue) )],[refute_0_52,refute_0_53]) ).
cnf(refute_0_55,plain,
merge(cons(s(z),X_77),cons(s(X_75),X_78)) = aux(s(z),X_77,s(X_75),X_78,btrue),
inference(resolve,[$cnf( $equal(merge(cons(s(z),X_77),cons(s(X_75),X_78)),aux(s(z),X_77,s(X_75),X_78,leqNat(z,X_75))) )],[refute_0_51,refute_0_54]) ).
cnf(refute_0_56,plain,
merge(cons(s(z),X_144),cons(s(X_75),X_78)) = aux(s(z),X_144,s(X_75),X_78,btrue),
inference(subst,[],[refute_0_55:[bind(X_77,$fot(X_144))]]) ).
cnf(refute_0_57,plain,
( merge(cons(s(z),X_144),cons(s(X_75),X_78)) != aux(s(z),X_144,s(X_75),X_78,btrue)
| prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)) != impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(merge(cons(s(z),X_144),cons(s(X_75),X_78)),merge(cons(s(X_75),X_78),cons(s(z),X_144))))
| prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)) = impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) ),
introduced(tautology,[equality,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)),impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(merge(cons(s(z),X_144),cons(s(X_75),X_78)),merge(cons(s(X_75),X_78),cons(s(z),X_144))))) ),[1,1,0],$fot(aux(s(z),X_144,s(X_75),X_78,btrue))]]) ).
cnf(refute_0_58,plain,
( prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)) != impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(merge(cons(s(z),X_144),cons(s(X_75),X_78)),merge(cons(s(X_75),X_78),cons(s(z),X_144))))
| prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)) = impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) ),
inference(resolve,[$cnf( $equal(merge(cons(s(z),X_144),cons(s(X_75),X_78)),aux(s(z),X_144,s(X_75),X_78,btrue)) )],[refute_0_56,refute_0_57]) ).
cnf(refute_0_59,plain,
prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)) = impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))),
inference(resolve,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)),impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(merge(cons(s(z),X_144),cons(s(X_75),X_78)),merge(cons(s(X_75),X_78),cons(s(z),X_144))))) )],[refute_0_46,refute_0_58]) ).
cnf(refute_0_60,plain,
impl(btrue,eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) = eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))),
inference(subst,[],[axiom_008:[bind(Q,$fot(eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))))]]) ).
cnf(refute_0_61,plain,
eq(cons(s(X_75),X_78),cons(s(X_75),X_78)) = btrue,
inference(subst,[],[axiom_016:[bind(X,$fot(cons(s(X_75),X_78)))]]) ).
cnf(refute_0_62,plain,
merge(cons(s(X_75),X_78),nil) = cons(s(X_75),X_78),
inference(subst,[],[axiom_006:[bind(Xs,$fot(X_78)),bind(Z,$fot(s(X_75)))]]) ).
cnf(refute_0_63,plain,
eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)) = eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),
introduced(tautology,[refl,[$fot(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)))]]) ).
cnf(refute_0_64,plain,
( eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)) != eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil))
| merge(cons(s(X_75),X_78),nil) != cons(s(X_75),X_78)
| eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)) = eq(cons(s(X_75),X_78),cons(s(X_75),X_78)) ),
introduced(tautology,[equality,[$cnf( $equal(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil))) ),[1,1],$fot(cons(s(X_75),X_78))]]) ).
cnf(refute_0_65,plain,
( merge(cons(s(X_75),X_78),nil) != cons(s(X_75),X_78)
| eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)) = eq(cons(s(X_75),X_78),cons(s(X_75),X_78)) ),
inference(resolve,[$cnf( $equal(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil))) )],[refute_0_63,refute_0_64]) ).
cnf(refute_0_66,plain,
eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)) = eq(cons(s(X_75),X_78),cons(s(X_75),X_78)),
inference(resolve,[$cnf( $equal(merge(cons(s(X_75),X_78),nil),cons(s(X_75),X_78)) )],[refute_0_62,refute_0_65]) ).
cnf(refute_0_67,plain,
( eq(cons(s(X_75),X_78),cons(s(X_75),X_78)) != btrue
| eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)) != eq(cons(s(X_75),X_78),cons(s(X_75),X_78))
| eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)) = btrue ),
inference(subst,[],[refute_0_29:[bind(X0,$fot(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)))),bind(Y0,$fot(eq(cons(s(X_75),X_78),cons(s(X_75),X_78)))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_68,plain,
( eq(cons(s(X_75),X_78),cons(s(X_75),X_78)) != btrue
| eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)) = btrue ),
inference(resolve,[$cnf( $equal(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(cons(s(X_75),X_78),cons(s(X_75),X_78))) )],[refute_0_66,refute_0_67]) ).
cnf(refute_0_69,plain,
eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)) = btrue,
inference(resolve,[$cnf( $equal(eq(cons(s(X_75),X_78),cons(s(X_75),X_78)),btrue) )],[refute_0_61,refute_0_68]) ).
cnf(refute_0_70,plain,
impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) = impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))),
introduced(tautology,[refl,[$fot(impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))))]]) ).
cnf(refute_0_71,plain,
( eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)) != btrue
| impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) != impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))))
| impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) = impl(btrue,eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) ),
introduced(tautology,[equality,[$cnf( $equal(impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))),impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_72,plain,
( eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)) != btrue
| impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) = impl(btrue,eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) ),
inference(resolve,[$cnf( $equal(impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))),impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))))) )],[refute_0_70,refute_0_71]) ).
cnf(refute_0_73,plain,
impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) = impl(btrue,eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))),
inference(resolve,[$cnf( $equal(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),btrue) )],[refute_0_69,refute_0_72]) ).
cnf(refute_0_74,plain,
( impl(btrue,eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) != eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))
| impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) != impl(btrue,eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))))
| impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) = eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))) ),
inference(subst,[],[refute_0_29:[bind(X0,$fot(impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))))),bind(Y0,$fot(impl(btrue,eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))))),bind(Z0,$fot(eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))))]]) ).
cnf(refute_0_75,plain,
( impl(btrue,eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) != eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))
| impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) = eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))) ),
inference(resolve,[$cnf( $equal(impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))),impl(btrue,eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))))) )],[refute_0_73,refute_0_74]) ).
cnf(refute_0_76,plain,
impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) = eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))),
inference(resolve,[$cnf( $equal(impl(btrue,eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) )],[refute_0_60,refute_0_75]) ).
cnf(refute_0_77,plain,
( impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) != eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))
| prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)) != impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))))
| prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)) = eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))) ),
introduced(tautology,[equality,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)),impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))))) ),[1],$fot(eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))))]]) ).
cnf(refute_0_78,plain,
( prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)) != impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))))
| prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)) = eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))) ),
inference(resolve,[$cnf( $equal(impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144)))) )],[refute_0_76,refute_0_77]) ).
cnf(refute_0_79,plain,
prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)) = eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))),
inference(resolve,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),X_144),cons(s(X_75),X_78)),impl(eq(cons(s(X_75),X_78),merge(cons(s(X_75),X_78),nil)),eq(aux(s(z),X_144,s(X_75),X_78,btrue),merge(cons(s(X_75),X_78),cons(s(z),X_144))))) )],[refute_0_59,refute_0_78]) ).
cnf(refute_0_80,plain,
prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)) = eq(aux(s(z),X_845,s(z),X_847,btrue),merge(cons(s(z),X_847),cons(s(z),X_845))),
inference(subst,[],[refute_0_79:[bind(X_144,$fot(X_845)),bind(X_75,$fot(z)),bind(X_78,$fot(X_847))]]) ).
cnf(refute_0_81,plain,
merge(cons(s(z),X_847),cons(s(z),X_845)) = aux(s(z),X_847,s(z),X_845,btrue),
inference(subst,[],[refute_0_55:[bind(X_75,$fot(z)),bind(X_77,$fot(X_847)),bind(X_78,$fot(X_845))]]) ).
cnf(refute_0_82,plain,
( merge(cons(s(z),X_847),cons(s(z),X_845)) != aux(s(z),X_847,s(z),X_845,btrue)
| prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)) != eq(aux(s(z),X_845,s(z),X_847,btrue),merge(cons(s(z),X_847),cons(s(z),X_845)))
| prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)) = eq(aux(s(z),X_845,s(z),X_847,btrue),aux(s(z),X_847,s(z),X_845,btrue)) ),
introduced(tautology,[equality,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)),eq(aux(s(z),X_845,s(z),X_847,btrue),merge(cons(s(z),X_847),cons(s(z),X_845)))) ),[1,1],$fot(aux(s(z),X_847,s(z),X_845,btrue))]]) ).
cnf(refute_0_83,plain,
( prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)) != eq(aux(s(z),X_845,s(z),X_847,btrue),merge(cons(s(z),X_847),cons(s(z),X_845)))
| prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)) = eq(aux(s(z),X_845,s(z),X_847,btrue),aux(s(z),X_847,s(z),X_845,btrue)) ),
inference(resolve,[$cnf( $equal(merge(cons(s(z),X_847),cons(s(z),X_845)),aux(s(z),X_847,s(z),X_845,btrue)) )],[refute_0_81,refute_0_82]) ).
cnf(refute_0_84,plain,
prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)) = eq(aux(s(z),X_845,s(z),X_847,btrue),aux(s(z),X_847,s(z),X_845,btrue)),
inference(resolve,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)),eq(aux(s(z),X_845,s(z),X_847,btrue),merge(cons(s(z),X_847),cons(s(z),X_845)))) )],[refute_0_80,refute_0_83]) ).
cnf(refute_0_85,plain,
( eq2(X_508,X_508) != btrue
| eq(cons(X_508,X_507),cons(X_508,X_506)) = eq(X_507,X_506) ),
inference(subst,[],[axiom_020:[bind(X,$fot(X_508)),bind(X2,$fot(X_506)),bind(Y,$fot(X_507)),bind(Z,$fot(X_508))]]) ).
cnf(refute_0_86,plain,
eq2(X_508,X_508) = btrue,
inference(subst,[],[axiom_017:[bind(X,$fot(X_508))]]) ).
cnf(refute_0_87,plain,
( btrue != btrue
| eq2(X_508,X_508) != btrue
| eq2(X_508,X_508) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(eq2(X_508,X_508),btrue) ),[1],$fot(btrue)]]) ).
cnf(refute_0_88,plain,
( btrue != btrue
| eq2(X_508,X_508) = btrue ),
inference(resolve,[$cnf( $equal(eq2(X_508,X_508),btrue) )],[refute_0_86,refute_0_87]) ).
cnf(refute_0_89,plain,
( btrue != btrue
| eq(cons(X_508,X_507),cons(X_508,X_506)) = eq(X_507,X_506) ),
inference(resolve,[$cnf( $equal(eq2(X_508,X_508),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(cons(X_508,X_507),cons(X_508,X_506)) = eq(X_507,X_506),
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_90,refute_0_89]) ).
cnf(refute_0_92,plain,
eq(cons(X_511,merge(Xs,cons(Y2,Ys))),cons(X_511,X_509)) = eq(merge(Xs,cons(Y2,Ys)),X_509),
inference(subst,[],[refute_0_91:[bind(X_506,$fot(X_509)),bind(X_507,$fot(merge(Xs,cons(Y2,Ys)))),bind(X_508,$fot(X_511))]]) ).
cnf(refute_0_93,plain,
aux(X_511,Xs,Y2,Ys,btrue) = cons(X_511,merge(Xs,cons(Y2,Ys))),
inference(subst,[],[axiom:[bind(Z,$fot(X_511))]]) ).
cnf(refute_0_94,plain,
( aux(X_511,Xs,Y2,Ys,btrue) != cons(X_511,merge(Xs,cons(Y2,Ys)))
| cons(X_511,merge(Xs,cons(Y2,Ys))) = aux(X_511,Xs,Y2,Ys,btrue) ),
inference(subst,[],[refute_0_27:[bind(X0,$fot(aux(X_511,Xs,Y2,Ys,btrue))),bind(Y0,$fot(cons(X_511,merge(Xs,cons(Y2,Ys)))))]]) ).
cnf(refute_0_95,plain,
cons(X_511,merge(Xs,cons(Y2,Ys))) = aux(X_511,Xs,Y2,Ys,btrue),
inference(resolve,[$cnf( $equal(aux(X_511,Xs,Y2,Ys,btrue),cons(X_511,merge(Xs,cons(Y2,Ys)))) )],[refute_0_93,refute_0_94]) ).
cnf(refute_0_96,plain,
( cons(X_511,merge(Xs,cons(Y2,Ys))) != aux(X_511,Xs,Y2,Ys,btrue)
| eq(cons(X_511,merge(Xs,cons(Y2,Ys))),cons(X_511,X_509)) != eq(merge(Xs,cons(Y2,Ys)),X_509)
| eq(aux(X_511,Xs,Y2,Ys,btrue),cons(X_511,X_509)) = eq(merge(Xs,cons(Y2,Ys)),X_509) ),
introduced(tautology,[equality,[$cnf( $equal(eq(cons(X_511,merge(Xs,cons(Y2,Ys))),cons(X_511,X_509)),eq(merge(Xs,cons(Y2,Ys)),X_509)) ),[0,0],$fot(aux(X_511,Xs,Y2,Ys,btrue))]]) ).
cnf(refute_0_97,plain,
( eq(cons(X_511,merge(Xs,cons(Y2,Ys))),cons(X_511,X_509)) != eq(merge(Xs,cons(Y2,Ys)),X_509)
| eq(aux(X_511,Xs,Y2,Ys,btrue),cons(X_511,X_509)) = eq(merge(Xs,cons(Y2,Ys)),X_509) ),
inference(resolve,[$cnf( $equal(cons(X_511,merge(Xs,cons(Y2,Ys))),aux(X_511,Xs,Y2,Ys,btrue)) )],[refute_0_95,refute_0_96]) ).
cnf(refute_0_98,plain,
eq(aux(X_511,Xs,Y2,Ys,btrue),cons(X_511,X_509)) = eq(merge(Xs,cons(Y2,Ys)),X_509),
inference(resolve,[$cnf( $equal(eq(cons(X_511,merge(Xs,cons(Y2,Ys))),cons(X_511,X_509)),eq(merge(Xs,cons(Y2,Ys)),X_509)) )],[refute_0_92,refute_0_97]) ).
cnf(refute_0_99,plain,
eq(aux(X_540,X_536,X_537,X_538,btrue),cons(X_540,merge(Xs,cons(Y2,Ys)))) = eq(merge(X_536,cons(X_537,X_538)),merge(Xs,cons(Y2,Ys))),
inference(subst,[],[refute_0_98:[bind(Xs,$fot(X_536)),bind(Y2,$fot(X_537)),bind(Ys,$fot(X_538)),bind(X_509,$fot(merge(Xs,cons(Y2,Ys)))),bind(X_511,$fot(X_540))]]) ).
cnf(refute_0_100,plain,
aux(X_540,Xs,Y2,Ys,btrue) = cons(X_540,merge(Xs,cons(Y2,Ys))),
inference(subst,[],[axiom:[bind(Z,$fot(X_540))]]) ).
cnf(refute_0_101,plain,
( aux(X_540,Xs,Y2,Ys,btrue) != cons(X_540,merge(Xs,cons(Y2,Ys)))
| cons(X_540,merge(Xs,cons(Y2,Ys))) = aux(X_540,Xs,Y2,Ys,btrue) ),
inference(subst,[],[refute_0_27:[bind(X0,$fot(aux(X_540,Xs,Y2,Ys,btrue))),bind(Y0,$fot(cons(X_540,merge(Xs,cons(Y2,Ys)))))]]) ).
cnf(refute_0_102,plain,
cons(X_540,merge(Xs,cons(Y2,Ys))) = aux(X_540,Xs,Y2,Ys,btrue),
inference(resolve,[$cnf( $equal(aux(X_540,Xs,Y2,Ys,btrue),cons(X_540,merge(Xs,cons(Y2,Ys)))) )],[refute_0_100,refute_0_101]) ).
cnf(refute_0_103,plain,
( cons(X_540,merge(Xs,cons(Y2,Ys))) != aux(X_540,Xs,Y2,Ys,btrue)
| eq(aux(X_540,X_536,X_537,X_538,btrue),cons(X_540,merge(Xs,cons(Y2,Ys)))) != eq(merge(X_536,cons(X_537,X_538)),merge(Xs,cons(Y2,Ys)))
| eq(aux(X_540,X_536,X_537,X_538,btrue),aux(X_540,Xs,Y2,Ys,btrue)) = eq(merge(X_536,cons(X_537,X_538)),merge(Xs,cons(Y2,Ys))) ),
introduced(tautology,[equality,[$cnf( $equal(eq(aux(X_540,X_536,X_537,X_538,btrue),cons(X_540,merge(Xs,cons(Y2,Ys)))),eq(merge(X_536,cons(X_537,X_538)),merge(Xs,cons(Y2,Ys)))) ),[0,1],$fot(aux(X_540,Xs,Y2,Ys,btrue))]]) ).
cnf(refute_0_104,plain,
( eq(aux(X_540,X_536,X_537,X_538,btrue),cons(X_540,merge(Xs,cons(Y2,Ys)))) != eq(merge(X_536,cons(X_537,X_538)),merge(Xs,cons(Y2,Ys)))
| eq(aux(X_540,X_536,X_537,X_538,btrue),aux(X_540,Xs,Y2,Ys,btrue)) = eq(merge(X_536,cons(X_537,X_538)),merge(Xs,cons(Y2,Ys))) ),
inference(resolve,[$cnf( $equal(cons(X_540,merge(Xs,cons(Y2,Ys))),aux(X_540,Xs,Y2,Ys,btrue)) )],[refute_0_102,refute_0_103]) ).
cnf(refute_0_105,plain,
eq(aux(X_540,X_536,X_537,X_538,btrue),aux(X_540,Xs,Y2,Ys,btrue)) = eq(merge(X_536,cons(X_537,X_538)),merge(Xs,cons(Y2,Ys))),
inference(resolve,[$cnf( $equal(eq(aux(X_540,X_536,X_537,X_538,btrue),cons(X_540,merge(Xs,cons(Y2,Ys)))),eq(merge(X_536,cons(X_537,X_538)),merge(Xs,cons(Y2,Ys)))) )],[refute_0_99,refute_0_104]) ).
cnf(refute_0_106,plain,
eq(aux(s(z),X_845,s(z),X_847,btrue),aux(s(z),X_847,s(z),X_845,btrue)) = eq(merge(X_845,cons(s(z),X_847)),merge(X_847,cons(s(z),X_845))),
inference(subst,[],[refute_0_105:[bind(Xs,$fot(X_847)),bind(Y2,$fot(s(z))),bind(Ys,$fot(X_845)),bind(X_536,$fot(X_845)),bind(X_537,$fot(s(z))),bind(X_538,$fot(X_847)),bind(X_540,$fot(s(z)))]]) ).
cnf(refute_0_107,plain,
( eq(aux(s(z),X_845,s(z),X_847,btrue),aux(s(z),X_847,s(z),X_845,btrue)) != eq(merge(X_845,cons(s(z),X_847)),merge(X_847,cons(s(z),X_845)))
| prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)) != eq(aux(s(z),X_845,s(z),X_847,btrue),aux(s(z),X_847,s(z),X_845,btrue))
| prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)) = eq(merge(X_845,cons(s(z),X_847)),merge(X_847,cons(s(z),X_845))) ),
introduced(tautology,[equality,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)),eq(aux(s(z),X_845,s(z),X_847,btrue),aux(s(z),X_847,s(z),X_845,btrue))) ),[1],$fot(eq(merge(X_845,cons(s(z),X_847)),merge(X_847,cons(s(z),X_845))))]]) ).
cnf(refute_0_108,plain,
( prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)) != eq(aux(s(z),X_845,s(z),X_847,btrue),aux(s(z),X_847,s(z),X_845,btrue))
| prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)) = eq(merge(X_845,cons(s(z),X_847)),merge(X_847,cons(s(z),X_845))) ),
inference(resolve,[$cnf( $equal(eq(aux(s(z),X_845,s(z),X_847,btrue),aux(s(z),X_847,s(z),X_845,btrue)),eq(merge(X_845,cons(s(z),X_847)),merge(X_847,cons(s(z),X_845)))) )],[refute_0_106,refute_0_107]) ).
cnf(refute_0_109,plain,
prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)) = eq(merge(X_845,cons(s(z),X_847)),merge(X_847,cons(s(z),X_845))),
inference(resolve,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),X_845),cons(s(z),X_847)),eq(aux(s(z),X_845,s(z),X_847,btrue),aux(s(z),X_847,s(z),X_845,btrue))) )],[refute_0_84,refute_0_108]) ).
cnf(refute_0_110,plain,
prop_merge_comm(nil,cons(s(z),nil),cons(s(z),X_992)) = eq(merge(nil,cons(s(z),X_992)),merge(X_992,cons(s(z),nil))),
inference(subst,[],[refute_0_109:[bind(X_845,$fot(nil)),bind(X_847,$fot(X_992))]]) ).
cnf(refute_0_111,plain,
merge(nil,cons(s(z),X_992)) = cons(s(z),X_992),
inference(subst,[],[axiom_005:[bind(Y,$fot(cons(s(z),X_992)))]]) ).
cnf(refute_0_112,plain,
( merge(nil,cons(s(z),X_992)) != cons(s(z),X_992)
| prop_merge_comm(nil,cons(s(z),nil),cons(s(z),X_992)) != eq(merge(nil,cons(s(z),X_992)),merge(X_992,cons(s(z),nil)))
| prop_merge_comm(nil,cons(s(z),nil),cons(s(z),X_992)) = eq(cons(s(z),X_992),merge(X_992,cons(s(z),nil))) ),
introduced(tautology,[equality,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),nil),cons(s(z),X_992)),eq(merge(nil,cons(s(z),X_992)),merge(X_992,cons(s(z),nil)))) ),[1,0],$fot(cons(s(z),X_992))]]) ).
cnf(refute_0_113,plain,
( prop_merge_comm(nil,cons(s(z),nil),cons(s(z),X_992)) != eq(merge(nil,cons(s(z),X_992)),merge(X_992,cons(s(z),nil)))
| prop_merge_comm(nil,cons(s(z),nil),cons(s(z),X_992)) = eq(cons(s(z),X_992),merge(X_992,cons(s(z),nil))) ),
inference(resolve,[$cnf( $equal(merge(nil,cons(s(z),X_992)),cons(s(z),X_992)) )],[refute_0_111,refute_0_112]) ).
cnf(refute_0_114,plain,
prop_merge_comm(nil,cons(s(z),nil),cons(s(z),X_992)) = eq(cons(s(z),X_992),merge(X_992,cons(s(z),nil))),
inference(resolve,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),nil),cons(s(z),X_992)),eq(merge(nil,cons(s(z),X_992)),merge(X_992,cons(s(z),nil)))) )],[refute_0_110,refute_0_113]) ).
cnf(refute_0_115,plain,
prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))) = eq(cons(s(z),cons(z,X_30)),merge(cons(z,X_30),cons(s(z),nil))),
inference(subst,[],[refute_0_114:[bind(X_992,$fot(cons(z,X_30)))]]) ).
cnf(refute_0_116,plain,
merge(cons(z,X_30),cons(X_31,X_32)) = aux(z,X_30,X_31,X_32,leqNat(z,X_31)),
inference(subst,[],[axiom_007:[bind(Xs,$fot(X_30)),bind(Y2,$fot(X_31)),bind(Ys,$fot(X_32)),bind(Z,$fot(z))]]) ).
cnf(refute_0_117,plain,
leqNat(z,X_31) = btrue,
inference(subst,[],[axiom_002:[bind(Y,$fot(X_31))]]) ).
cnf(refute_0_118,plain,
( leqNat(z,X_31) != btrue
| merge(cons(z,X_30),cons(X_31,X_32)) != aux(z,X_30,X_31,X_32,leqNat(z,X_31))
| merge(cons(z,X_30),cons(X_31,X_32)) = aux(z,X_30,X_31,X_32,btrue) ),
introduced(tautology,[equality,[$cnf( $equal(merge(cons(z,X_30),cons(X_31,X_32)),aux(z,X_30,X_31,X_32,leqNat(z,X_31))) ),[1,4],$fot(btrue)]]) ).
cnf(refute_0_119,plain,
( merge(cons(z,X_30),cons(X_31,X_32)) != aux(z,X_30,X_31,X_32,leqNat(z,X_31))
| merge(cons(z,X_30),cons(X_31,X_32)) = aux(z,X_30,X_31,X_32,btrue) ),
inference(resolve,[$cnf( $equal(leqNat(z,X_31),btrue) )],[refute_0_117,refute_0_118]) ).
cnf(refute_0_120,plain,
merge(cons(z,X_30),cons(X_31,X_32)) = aux(z,X_30,X_31,X_32,btrue),
inference(resolve,[$cnf( $equal(merge(cons(z,X_30),cons(X_31,X_32)),aux(z,X_30,X_31,X_32,leqNat(z,X_31))) )],[refute_0_116,refute_0_119]) ).
cnf(refute_0_121,plain,
merge(cons(z,X_30),cons(s(z),nil)) = aux(z,X_30,s(z),nil,btrue),
inference(subst,[],[refute_0_120:[bind(X_31,$fot(s(z))),bind(X_32,$fot(nil))]]) ).
cnf(refute_0_122,plain,
( merge(cons(z,X_30),cons(s(z),nil)) != aux(z,X_30,s(z),nil,btrue)
| prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))) != eq(cons(s(z),cons(z,X_30)),merge(cons(z,X_30),cons(s(z),nil)))
| prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))) = eq(cons(s(z),cons(z,X_30)),aux(z,X_30,s(z),nil,btrue)) ),
introduced(tautology,[equality,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))),eq(cons(s(z),cons(z,X_30)),merge(cons(z,X_30),cons(s(z),nil)))) ),[1,1],$fot(aux(z,X_30,s(z),nil,btrue))]]) ).
cnf(refute_0_123,plain,
( prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))) != eq(cons(s(z),cons(z,X_30)),merge(cons(z,X_30),cons(s(z),nil)))
| prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))) = eq(cons(s(z),cons(z,X_30)),aux(z,X_30,s(z),nil,btrue)) ),
inference(resolve,[$cnf( $equal(merge(cons(z,X_30),cons(s(z),nil)),aux(z,X_30,s(z),nil,btrue)) )],[refute_0_121,refute_0_122]) ).
cnf(refute_0_124,plain,
prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))) = eq(cons(s(z),cons(z,X_30)),aux(z,X_30,s(z),nil,btrue)),
inference(resolve,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))),eq(cons(s(z),cons(z,X_30)),merge(cons(z,X_30),cons(s(z),nil)))) )],[refute_0_115,refute_0_123]) ).
cnf(refute_0_125,plain,
( eq2(s(X),z) != bfalse
| eq(cons(s(X),X_268),cons(z,X_267)) = bfalse ),
inference(subst,[],[axiom_019:[bind(X,$fot(s(X))),bind(X2,$fot(X_267)),bind(Y,$fot(X_268)),bind(Z,$fot(z))]]) ).
cnf(refute_0_126,plain,
( bfalse != bfalse
| eq2(s(X),z) != bfalse
| eq2(s(X),z) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(eq2(s(X),z),bfalse) ),[1],$fot(bfalse)]]) ).
cnf(refute_0_127,plain,
( bfalse != bfalse
| eq2(s(X),z) = bfalse ),
inference(resolve,[$cnf( $equal(eq2(s(X),z),bfalse) )],[axiom_015,refute_0_126]) ).
cnf(refute_0_128,plain,
( bfalse != bfalse
| eq(cons(s(X),X_268),cons(z,X_267)) = bfalse ),
inference(resolve,[$cnf( $equal(eq2(s(X),z),bfalse) )],[refute_0_127,refute_0_125]) ).
cnf(refute_0_129,plain,
bfalse = bfalse,
introduced(tautology,[refl,[$fot(bfalse)]]) ).
cnf(refute_0_130,plain,
eq(cons(s(X),X_268),cons(z,X_267)) = bfalse,
inference(resolve,[$cnf( $equal(bfalse,bfalse) )],[refute_0_129,refute_0_128]) ).
cnf(refute_0_131,plain,
eq(cons(s(X_270),X_272),cons(z,merge(Xs,cons(Y2,Ys)))) = bfalse,
inference(subst,[],[refute_0_130:[bind(X,$fot(X_270)),bind(X_267,$fot(merge(Xs,cons(Y2,Ys)))),bind(X_268,$fot(X_272))]]) ).
cnf(refute_0_132,plain,
aux(z,Xs,Y2,Ys,btrue) = cons(z,merge(Xs,cons(Y2,Ys))),
inference(subst,[],[axiom:[bind(Z,$fot(z))]]) ).
cnf(refute_0_133,plain,
( aux(z,Xs,Y2,Ys,btrue) != cons(z,merge(Xs,cons(Y2,Ys)))
| cons(z,merge(Xs,cons(Y2,Ys))) = aux(z,Xs,Y2,Ys,btrue) ),
inference(subst,[],[refute_0_27:[bind(X0,$fot(aux(z,Xs,Y2,Ys,btrue))),bind(Y0,$fot(cons(z,merge(Xs,cons(Y2,Ys)))))]]) ).
cnf(refute_0_134,plain,
cons(z,merge(Xs,cons(Y2,Ys))) = aux(z,Xs,Y2,Ys,btrue),
inference(resolve,[$cnf( $equal(aux(z,Xs,Y2,Ys,btrue),cons(z,merge(Xs,cons(Y2,Ys)))) )],[refute_0_132,refute_0_133]) ).
cnf(refute_0_135,plain,
( cons(z,merge(Xs,cons(Y2,Ys))) != aux(z,Xs,Y2,Ys,btrue)
| eq(cons(s(X_270),X_272),cons(z,merge(Xs,cons(Y2,Ys)))) != bfalse
| eq(cons(s(X_270),X_272),aux(z,Xs,Y2,Ys,btrue)) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(eq(cons(s(X_270),X_272),cons(z,merge(Xs,cons(Y2,Ys)))),bfalse) ),[0,1],$fot(aux(z,Xs,Y2,Ys,btrue))]]) ).
cnf(refute_0_136,plain,
( eq(cons(s(X_270),X_272),cons(z,merge(Xs,cons(Y2,Ys)))) != bfalse
| eq(cons(s(X_270),X_272),aux(z,Xs,Y2,Ys,btrue)) = bfalse ),
inference(resolve,[$cnf( $equal(cons(z,merge(Xs,cons(Y2,Ys))),aux(z,Xs,Y2,Ys,btrue)) )],[refute_0_134,refute_0_135]) ).
cnf(refute_0_137,plain,
eq(cons(s(X_270),X_272),aux(z,Xs,Y2,Ys,btrue)) = bfalse,
inference(resolve,[$cnf( $equal(eq(cons(s(X_270),X_272),cons(z,merge(Xs,cons(Y2,Ys)))),bfalse) )],[refute_0_131,refute_0_136]) ).
cnf(refute_0_138,plain,
eq(cons(s(z),cons(z,X_30)),aux(z,X_30,s(z),nil,btrue)) = bfalse,
inference(subst,[],[refute_0_137:[bind(Xs,$fot(X_30)),bind(Y2,$fot(s(z))),bind(Ys,$fot(nil)),bind(X_270,$fot(z)),bind(X_272,$fot(cons(z,X_30)))]]) ).
cnf(refute_0_139,plain,
( eq(cons(s(z),cons(z,X_30)),aux(z,X_30,s(z),nil,btrue)) != bfalse
| prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))) != eq(cons(s(z),cons(z,X_30)),aux(z,X_30,s(z),nil,btrue))
| prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))),eq(cons(s(z),cons(z,X_30)),aux(z,X_30,s(z),nil,btrue))) ),[1],$fot(bfalse)]]) ).
cnf(refute_0_140,plain,
( prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))) != eq(cons(s(z),cons(z,X_30)),aux(z,X_30,s(z),nil,btrue))
| prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))) = bfalse ),
inference(resolve,[$cnf( $equal(eq(cons(s(z),cons(z,X_30)),aux(z,X_30,s(z),nil,btrue)),bfalse) )],[refute_0_138,refute_0_139]) ).
cnf(refute_0_141,plain,
prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))) = bfalse,
inference(resolve,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_30))),eq(cons(s(z),cons(z,X_30)),aux(z,X_30,s(z),nil,btrue))) )],[refute_0_124,refute_0_140]) ).
cnf(refute_0_142,plain,
prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_994))) = bfalse,
inference(subst,[],[refute_0_141:[bind(X_30,$fot(X_994))]]) ).
cnf(refute_0_143,plain,
( eq3(bfalse,bfalse) != btrue
| prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_994))) != bfalse
| eq3(prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_994))),bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( ~ $equal(eq3(prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_994))),bfalse),btrue) ),[0,0],$fot(bfalse)]]) ).
cnf(refute_0_144,plain,
( eq3(bfalse,bfalse) != btrue
| eq3(prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_994))),bfalse) = btrue ),
inference(resolve,[$cnf( $equal(prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_994))),bfalse) )],[refute_0_142,refute_0_143]) ).
cnf(refute_0_145,plain,
eq3(bfalse,bfalse) != btrue,
inference(resolve,[$cnf( $equal(eq3(prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X_994))),bfalse),btrue) )],[refute_0_144,refute_0_0]) ).
cnf(refute_0_146,plain,
eq3(bfalse,bfalse) = btrue,
inference(subst,[],[axiom_018:[bind(X,$fot(bfalse))]]) ).
cnf(refute_0_147,plain,
( btrue != btrue
| eq3(bfalse,bfalse) != btrue
| eq3(bfalse,bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(eq3(bfalse,bfalse),btrue) ),[1],$fot(btrue)]]) ).
cnf(refute_0_148,plain,
( btrue != btrue
| eq3(bfalse,bfalse) = btrue ),
inference(resolve,[$cnf( $equal(eq3(bfalse,bfalse),btrue) )],[refute_0_146,refute_0_147]) ).
cnf(refute_0_149,plain,
btrue != btrue,
inference(resolve,[$cnf( $equal(eq3(bfalse,bfalse),btrue) )],[refute_0_148,refute_0_145]) ).
cnf(refute_0_150,plain,
$false,
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_90,refute_0_149]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SWX199-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.14 % Command : metis --show proof --show saturation %s
% 0.17/0.35 % Computer : n025.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Tue May 5 11:13:43 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 2.74/2.93 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.74/2.93
% 2.74/2.93 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 2.74/2.96
%------------------------------------------------------------------------------