%------------------------------------------------------------------------------
% 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 : n011.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 : Theorem 0.75s 0.92s
% Output : CNFRefutation 0.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 27
% Syntax : Number of formulae : 124 ( 64 unt; 0 def)
% Number of atoms : 211 ( 180 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 176 ( 89 ~; 76 |; 1 &)
% ( 3 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 216 ( 11 sgn 59 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
! [X,X2] : head(cons(X,X2)) = X ).
fof(axiom_002,axiom,
! [X,X2] : tail(cons(X,X2)) = X2 ).
fof(axiom_005,axiom,
! [X] : z != s(X) ).
fof(axiom_006,axiom,
! [Y] : leqNat(z,Y) ).
fof(axiom_008,axiom,
! [Z,M] :
( leqNat(s(Z),s(M))
<=> leqNat(Z,M) ) ).
fof(axiom_009,axiom,
! [Y] : merge(nil,Y) = Y ).
fof(axiom_010,axiom,
! [Z,Xs] : merge(cons(Z,Xs),nil) = cons(Z,Xs) ).
fof(axiom_011,axiom,
! [Z,Xs,Y2,Ys] :
( leqNat(Z,Y2)
=> merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Z,merge(Xs,cons(Y2,Ys))) ) ).
fof(goal_013,conjecture,
? [Xs,Ys,Zs] :
~ ( merge(Xs,Ys) = merge(Ys,Xs)
=> ( merge(Xs,Zs) = merge(Zs,Xs)
=> merge(Ys,Zs) = merge(Zs,Ys) ) ) ).
fof(subgoal_0,plain,
? [Xs,Ys,Zs] :
~ ( merge(Xs,Ys) = merge(Ys,Xs)
=> ( merge(Xs,Zs) = merge(Zs,Xs)
=> merge(Ys,Zs) = merge(Zs,Ys) ) ),
inference(strip,[],[goal_013]) ).
fof(negate_0_0,plain,
~ ? [Xs,Ys,Zs] :
~ ( merge(Xs,Ys) = merge(Ys,Xs)
=> ( merge(Xs,Zs) = merge(Zs,Xs)
=> merge(Ys,Zs) = merge(Zs,Ys) ) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
! [X,X2] : head(cons(X,X2)) = X,
inference(canonicalize,[],[axiom_001]) ).
fof(normalize_0_1,plain,
! [X,X2] : head(cons(X,X2)) = X,
inference(specialize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [Y] : leqNat(z,Y),
inference(canonicalize,[],[axiom_006]) ).
fof(normalize_0_3,plain,
! [Y] : leqNat(z,Y),
inference(specialize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [Xs,Y2,Z] :
( ~ leqNat(Z,Y2)
| ! [Ys] : merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Z,merge(Xs,cons(Y2,Ys))) ),
inference(canonicalize,[],[axiom_011]) ).
fof(normalize_0_5,plain,
! [Xs,Y2,Z] :
( ~ leqNat(Z,Y2)
| ! [Ys] : merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Z,merge(Xs,cons(Y2,Ys))) ),
inference(specialize,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [Xs,Y2,Ys,Z] :
( ~ leqNat(Z,Y2)
| merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Z,merge(Xs,cons(Y2,Ys))) ),
inference(clausify,[],[normalize_0_5]) ).
fof(normalize_0_7,plain,
! [X,X2] : tail(cons(X,X2)) = X2,
inference(canonicalize,[],[axiom_002]) ).
fof(normalize_0_8,plain,
! [X,X2] : tail(cons(X,X2)) = X2,
inference(specialize,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
! [M,Z] :
( ~ leqNat(Z,M)
<=> ~ leqNat(s(Z),s(M)) ),
inference(canonicalize,[],[axiom_008]) ).
fof(normalize_0_10,plain,
! [M,Z] :
( ~ leqNat(Z,M)
<=> ~ leqNat(s(Z),s(M)) ),
inference(specialize,[],[normalize_0_9]) ).
fof(normalize_0_11,plain,
! [M,Z] :
( ( ~ leqNat(Z,M)
| leqNat(s(Z),s(M)) )
& ( ~ leqNat(s(Z),s(M))
| leqNat(Z,M) ) ),
inference(clausify,[],[normalize_0_10]) ).
fof(normalize_0_12,plain,
! [M,Z] :
( ~ leqNat(Z,M)
| leqNat(s(Z),s(M)) ),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
! [Xs,Ys,Zs] :
( merge(Xs,Ys) != merge(Ys,Xs)
| merge(Xs,Zs) != merge(Zs,Xs)
| merge(Ys,Zs) = merge(Zs,Ys) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_14,plain,
! [Xs,Ys,Zs] :
( merge(Xs,Ys) != merge(Ys,Xs)
| merge(Xs,Zs) != merge(Zs,Xs)
| merge(Ys,Zs) = merge(Zs,Ys) ),
inference(specialize,[],[normalize_0_13]) ).
fof(normalize_0_15,plain,
! [Xs,Z] : merge(cons(Z,Xs),nil) = cons(Z,Xs),
inference(canonicalize,[],[axiom_010]) ).
fof(normalize_0_16,plain,
! [Xs,Z] : merge(cons(Z,Xs),nil) = cons(Z,Xs),
inference(specialize,[],[normalize_0_15]) ).
fof(normalize_0_17,plain,
! [Y] : merge(nil,Y) = Y,
inference(canonicalize,[],[axiom_009]) ).
fof(normalize_0_18,plain,
! [Y] : merge(nil,Y) = Y,
inference(specialize,[],[normalize_0_17]) ).
fof(normalize_0_19,plain,
! [X] : z != s(X),
inference(canonicalize,[],[axiom_005]) ).
fof(normalize_0_20,plain,
! [X] : z != s(X),
inference(specialize,[],[normalize_0_19]) ).
cnf(refute_0_0,plain,
head(cons(X,X2)) = X,
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_1,plain,
head(cons(s(z),cons(z,X_170))) = s(z),
inference(subst,[],[refute_0_0:[bind(X,$fot(s(z))),bind(X2,$fot(cons(z,X_170)))]]) ).
cnf(refute_0_2,plain,
leqNat(z,Y),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_3,plain,
leqNat(z,X_90),
inference(subst,[],[refute_0_2:[bind(Y,$fot(X_90))]]) ).
cnf(refute_0_4,plain,
( ~ leqNat(Z,Y2)
| merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Z,merge(Xs,cons(Y2,Ys))) ),
inference(canonicalize,[],[normalize_0_6]) ).
cnf(refute_0_5,plain,
( ~ leqNat(z,X_90)
| merge(cons(z,X_89),cons(X_90,X_91)) = cons(z,merge(X_89,cons(X_90,X_91))) ),
inference(subst,[],[refute_0_4:[bind(Xs,$fot(X_89)),bind(Y2,$fot(X_90)),bind(Ys,$fot(X_91)),bind(Z,$fot(z))]]) ).
cnf(refute_0_6,plain,
merge(cons(z,X_89),cons(X_90,X_91)) = cons(z,merge(X_89,cons(X_90,X_91))),
inference(resolve,[$cnf( leqNat(z,X_90) )],[refute_0_3,refute_0_5]) ).
cnf(refute_0_7,plain,
merge(cons(z,X_89),cons(s(z),nil)) = cons(z,merge(X_89,cons(s(z),nil))),
inference(subst,[],[refute_0_6:[bind(X_90,$fot(s(z))),bind(X_91,$fot(nil))]]) ).
cnf(refute_0_8,plain,
tail(cons(X,X2)) = X2,
inference(canonicalize,[],[normalize_0_8]) ).
cnf(refute_0_9,plain,
tail(cons(s(z),merge(X_164,cons(s(z),nil)))) = merge(X_164,cons(s(z),nil)),
inference(subst,[],[refute_0_8:[bind(X,$fot(s(z))),bind(X2,$fot(merge(X_164,cons(s(z),nil))))]]) ).
cnf(refute_0_10,plain,
leqNat(z,X_13),
inference(subst,[],[refute_0_2:[bind(Y,$fot(X_13))]]) ).
cnf(refute_0_11,plain,
( ~ leqNat(Z,M)
| leqNat(s(Z),s(M)) ),
inference(canonicalize,[],[normalize_0_12]) ).
cnf(refute_0_12,plain,
( ~ leqNat(z,X_13)
| leqNat(s(z),s(X_13)) ),
inference(subst,[],[refute_0_11:[bind(M,$fot(X_13)),bind(Z,$fot(z))]]) ).
cnf(refute_0_13,plain,
leqNat(s(z),s(X_13)),
inference(resolve,[$cnf( leqNat(z,X_13) )],[refute_0_10,refute_0_12]) ).
cnf(refute_0_14,plain,
( ~ leqNat(s(z),s(X_13))
| merge(cons(s(z),X_89),cons(s(X_13),X_91)) = cons(s(z),merge(X_89,cons(s(X_13),X_91))) ),
inference(subst,[],[refute_0_4:[bind(Xs,$fot(X_89)),bind(Y2,$fot(s(X_13))),bind(Ys,$fot(X_91)),bind(Z,$fot(s(z)))]]) ).
cnf(refute_0_15,plain,
merge(cons(s(z),X_89),cons(s(X_13),X_91)) = cons(s(z),merge(X_89,cons(s(X_13),X_91))),
inference(resolve,[$cnf( leqNat(s(z),s(X_13)) )],[refute_0_13,refute_0_14]) ).
cnf(refute_0_16,plain,
merge(cons(s(z),X_89),cons(s(z),X_91)) = cons(s(z),merge(X_89,cons(s(z),X_91))),
inference(subst,[],[refute_0_15:[bind(X_13,$fot(z))]]) ).
cnf(refute_0_17,plain,
( merge(Xs,Ys) != merge(Ys,Xs)
| merge(Xs,Zs) != merge(Zs,Xs)
| merge(Ys,Zs) = merge(Zs,Ys) ),
inference(canonicalize,[],[normalize_0_14]) ).
cnf(refute_0_18,plain,
( merge(nil,X_131) != merge(X_131,nil)
| merge(nil,cons(Z,Xs)) != merge(cons(Z,Xs),nil)
| merge(X_131,cons(Z,Xs)) = merge(cons(Z,Xs),X_131) ),
inference(subst,[],[refute_0_17:[bind(Xs,$fot(nil)),bind(Ys,$fot(X_131)),bind(Zs,$fot(cons(Z,Xs)))]]) ).
cnf(refute_0_19,plain,
merge(cons(Z,Xs),nil) = cons(Z,Xs),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_20,plain,
( merge(cons(Z,Xs),nil) != cons(Z,Xs)
| merge(nil,cons(Z,Xs)) != cons(Z,Xs)
| merge(nil,cons(Z,Xs)) = merge(cons(Z,Xs),nil) ),
introduced(tautology,[equality,[$cnf( ~ $equal(merge(nil,cons(Z,Xs)),merge(cons(Z,Xs),nil)) ),[1],$fot(cons(Z,Xs))]]) ).
cnf(refute_0_21,plain,
( merge(nil,cons(Z,Xs)) != cons(Z,Xs)
| merge(nil,cons(Z,Xs)) = merge(cons(Z,Xs),nil) ),
inference(resolve,[$cnf( $equal(merge(cons(Z,Xs),nil),cons(Z,Xs)) )],[refute_0_19,refute_0_20]) ).
cnf(refute_0_22,plain,
( merge(nil,X_131) != merge(X_131,nil)
| merge(nil,cons(Z,Xs)) != cons(Z,Xs)
| merge(X_131,cons(Z,Xs)) = merge(cons(Z,Xs),X_131) ),
inference(resolve,[$cnf( $equal(merge(nil,cons(Z,Xs)),merge(cons(Z,Xs),nil)) )],[refute_0_21,refute_0_18]) ).
cnf(refute_0_23,plain,
merge(nil,Y) = Y,
inference(canonicalize,[],[normalize_0_18]) ).
cnf(refute_0_24,plain,
merge(nil,cons(Z,Xs)) = cons(Z,Xs),
inference(subst,[],[refute_0_23:[bind(Y,$fot(cons(Z,Xs)))]]) ).
cnf(refute_0_25,plain,
( cons(Z,Xs) != cons(Z,Xs)
| merge(nil,cons(Z,Xs)) != cons(Z,Xs)
| merge(nil,cons(Z,Xs)) = cons(Z,Xs) ),
introduced(tautology,[equality,[$cnf( $equal(merge(nil,cons(Z,Xs)),cons(Z,Xs)) ),[0,1],$fot(cons(Z,Xs))]]) ).
cnf(refute_0_26,plain,
( cons(Z,Xs) != cons(Z,Xs)
| merge(nil,cons(Z,Xs)) = cons(Z,Xs) ),
inference(resolve,[$cnf( $equal(merge(nil,cons(Z,Xs)),cons(Z,Xs)) )],[refute_0_24,refute_0_25]) ).
cnf(refute_0_27,plain,
( cons(Z,Xs) != cons(Z,Xs)
| merge(nil,X_131) != merge(X_131,nil)
| merge(X_131,cons(Z,Xs)) = merge(cons(Z,Xs),X_131) ),
inference(resolve,[$cnf( $equal(merge(nil,cons(Z,Xs)),cons(Z,Xs)) )],[refute_0_26,refute_0_22]) ).
cnf(refute_0_28,plain,
merge(nil,X_131) = X_131,
inference(subst,[],[refute_0_23:[bind(Y,$fot(X_131))]]) ).
cnf(refute_0_29,plain,
( X_131 != merge(X_131,nil)
| merge(nil,X_131) != X_131
| merge(nil,X_131) = merge(X_131,nil) ),
introduced(tautology,[equality,[$cnf( $equal(merge(nil,X_131),X_131) ),[1],$fot(merge(X_131,nil))]]) ).
cnf(refute_0_30,plain,
( X_131 != merge(X_131,nil)
| merge(nil,X_131) = merge(X_131,nil) ),
inference(resolve,[$cnf( $equal(merge(nil,X_131),X_131) )],[refute_0_28,refute_0_29]) ).
cnf(refute_0_31,plain,
( X_131 != merge(X_131,nil)
| cons(Z,Xs) != cons(Z,Xs)
| merge(X_131,cons(Z,Xs)) = merge(cons(Z,Xs),X_131) ),
inference(resolve,[$cnf( $equal(merge(nil,X_131),merge(X_131,nil)) )],[refute_0_30,refute_0_27]) ).
cnf(refute_0_32,plain,
cons(Z,Xs) = cons(Z,Xs),
introduced(tautology,[refl,[$fot(cons(Z,Xs))]]) ).
cnf(refute_0_33,plain,
( X_131 != merge(X_131,nil)
| merge(X_131,cons(Z,Xs)) = merge(cons(Z,Xs),X_131) ),
inference(resolve,[$cnf( $equal(cons(Z,Xs),cons(Z,Xs)) )],[refute_0_32,refute_0_31]) ).
cnf(refute_0_34,plain,
( cons(Z,Xs) != merge(cons(Z,Xs),nil)
| merge(cons(Z,Xs),cons(X_134,X_133)) = merge(cons(X_134,X_133),cons(Z,Xs)) ),
inference(subst,[],[refute_0_33:[bind(Xs,$fot(X_133)),bind(Z,$fot(X_134)),bind(X_131,$fot(cons(Z,Xs)))]]) ).
cnf(refute_0_35,plain,
( cons(Z,Xs) != cons(Z,Xs)
| merge(cons(Z,Xs),nil) != cons(Z,Xs)
| cons(Z,Xs) = merge(cons(Z,Xs),nil) ),
introduced(tautology,[equality,[$cnf( ~ $equal(cons(Z,Xs),merge(cons(Z,Xs),nil)) ),[1],$fot(cons(Z,Xs))]]) ).
cnf(refute_0_36,plain,
( cons(Z,Xs) != cons(Z,Xs)
| cons(Z,Xs) = merge(cons(Z,Xs),nil) ),
inference(resolve,[$cnf( $equal(merge(cons(Z,Xs),nil),cons(Z,Xs)) )],[refute_0_19,refute_0_35]) ).
cnf(refute_0_37,plain,
( cons(Z,Xs) != cons(Z,Xs)
| merge(cons(Z,Xs),cons(X_134,X_133)) = merge(cons(X_134,X_133),cons(Z,Xs)) ),
inference(resolve,[$cnf( $equal(cons(Z,Xs),merge(cons(Z,Xs),nil)) )],[refute_0_36,refute_0_34]) ).
cnf(refute_0_38,plain,
merge(cons(Z,Xs),cons(X_134,X_133)) = merge(cons(X_134,X_133),cons(Z,Xs)),
inference(resolve,[$cnf( $equal(cons(Z,Xs),cons(Z,Xs)) )],[refute_0_32,refute_0_37]) ).
cnf(refute_0_39,plain,
merge(cons(s(z),X_89),cons(s(X_13),X_91)) = merge(cons(s(X_13),X_91),cons(s(z),X_89)),
inference(subst,[],[refute_0_38:[bind(Xs,$fot(X_89)),bind(Z,$fot(s(z))),bind(X_133,$fot(X_91)),bind(X_134,$fot(s(X_13)))]]) ).
cnf(refute_0_40,plain,
( merge(cons(s(z),X_89),cons(s(X_13),X_91)) != cons(s(z),merge(X_89,cons(s(X_13),X_91)))
| merge(cons(s(z),X_89),cons(s(X_13),X_91)) != merge(cons(s(X_13),X_91),cons(s(z),X_89))
| merge(cons(s(X_13),X_91),cons(s(z),X_89)) = cons(s(z),merge(X_89,cons(s(X_13),X_91))) ),
introduced(tautology,[equality,[$cnf( $equal(merge(cons(s(z),X_89),cons(s(X_13),X_91)),cons(s(z),merge(X_89,cons(s(X_13),X_91)))) ),[0],$fot(merge(cons(s(X_13),X_91),cons(s(z),X_89)))]]) ).
cnf(refute_0_41,plain,
( merge(cons(s(z),X_89),cons(s(X_13),X_91)) != cons(s(z),merge(X_89,cons(s(X_13),X_91)))
| merge(cons(s(X_13),X_91),cons(s(z),X_89)) = cons(s(z),merge(X_89,cons(s(X_13),X_91))) ),
inference(resolve,[$cnf( $equal(merge(cons(s(z),X_89),cons(s(X_13),X_91)),merge(cons(s(X_13),X_91),cons(s(z),X_89))) )],[refute_0_39,refute_0_40]) ).
cnf(refute_0_42,plain,
merge(cons(s(X_13),X_91),cons(s(z),X_89)) = cons(s(z),merge(X_89,cons(s(X_13),X_91))),
inference(resolve,[$cnf( $equal(merge(cons(s(z),X_89),cons(s(X_13),X_91)),cons(s(z),merge(X_89,cons(s(X_13),X_91)))) )],[refute_0_15,refute_0_41]) ).
cnf(refute_0_43,plain,
merge(cons(s(z),X_89),cons(s(z),X_91)) = cons(s(z),merge(X_91,cons(s(z),X_89))),
inference(subst,[],[refute_0_42:[bind(X_13,$fot(z)),bind(X_89,$fot(X_91)),bind(X_91,$fot(X_89))]]) ).
cnf(refute_0_44,plain,
( merge(cons(s(z),X_89),cons(s(z),X_91)) != cons(s(z),merge(X_89,cons(s(z),X_91)))
| merge(cons(s(z),X_89),cons(s(z),X_91)) != cons(s(z),merge(X_91,cons(s(z),X_89)))
| cons(s(z),merge(X_91,cons(s(z),X_89))) = cons(s(z),merge(X_89,cons(s(z),X_91))) ),
introduced(tautology,[equality,[$cnf( $equal(merge(cons(s(z),X_89),cons(s(z),X_91)),cons(s(z),merge(X_89,cons(s(z),X_91)))) ),[0],$fot(cons(s(z),merge(X_91,cons(s(z),X_89))))]]) ).
cnf(refute_0_45,plain,
( merge(cons(s(z),X_89),cons(s(z),X_91)) != cons(s(z),merge(X_89,cons(s(z),X_91)))
| cons(s(z),merge(X_91,cons(s(z),X_89))) = cons(s(z),merge(X_89,cons(s(z),X_91))) ),
inference(resolve,[$cnf( $equal(merge(cons(s(z),X_89),cons(s(z),X_91)),cons(s(z),merge(X_91,cons(s(z),X_89)))) )],[refute_0_43,refute_0_44]) ).
cnf(refute_0_46,plain,
cons(s(z),merge(X_91,cons(s(z),X_89))) = cons(s(z),merge(X_89,cons(s(z),X_91))),
inference(resolve,[$cnf( $equal(merge(cons(s(z),X_89),cons(s(z),X_91)),cons(s(z),merge(X_89,cons(s(z),X_91)))) )],[refute_0_16,refute_0_45]) ).
cnf(refute_0_47,plain,
cons(s(z),merge(nil,cons(s(z),X_162))) = cons(s(z),merge(X_162,cons(s(z),nil))),
inference(subst,[],[refute_0_46:[bind(X_89,$fot(X_162)),bind(X_91,$fot(nil))]]) ).
cnf(refute_0_48,plain,
merge(nil,cons(s(z),X_162)) = cons(s(z),X_162),
inference(subst,[],[refute_0_23:[bind(Y,$fot(cons(s(z),X_162)))]]) ).
cnf(refute_0_49,plain,
( cons(s(z),merge(nil,cons(s(z),X_162))) != cons(s(z),merge(X_162,cons(s(z),nil)))
| merge(nil,cons(s(z),X_162)) != cons(s(z),X_162)
| cons(s(z),cons(s(z),X_162)) = cons(s(z),merge(X_162,cons(s(z),nil))) ),
introduced(tautology,[equality,[$cnf( $equal(cons(s(z),merge(nil,cons(s(z),X_162))),cons(s(z),merge(X_162,cons(s(z),nil)))) ),[0,1],$fot(cons(s(z),X_162))]]) ).
cnf(refute_0_50,plain,
( cons(s(z),merge(nil,cons(s(z),X_162))) != cons(s(z),merge(X_162,cons(s(z),nil)))
| cons(s(z),cons(s(z),X_162)) = cons(s(z),merge(X_162,cons(s(z),nil))) ),
inference(resolve,[$cnf( $equal(merge(nil,cons(s(z),X_162)),cons(s(z),X_162)) )],[refute_0_48,refute_0_49]) ).
cnf(refute_0_51,plain,
cons(s(z),cons(s(z),X_162)) = cons(s(z),merge(X_162,cons(s(z),nil))),
inference(resolve,[$cnf( $equal(cons(s(z),merge(nil,cons(s(z),X_162))),cons(s(z),merge(X_162,cons(s(z),nil)))) )],[refute_0_47,refute_0_50]) ).
cnf(refute_0_52,plain,
cons(s(z),cons(s(z),X_164)) = cons(s(z),merge(X_164,cons(s(z),nil))),
inference(subst,[],[refute_0_51:[bind(X_162,$fot(X_164))]]) ).
cnf(refute_0_53,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_54,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_55,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_53,refute_0_54]) ).
cnf(refute_0_56,plain,
( cons(s(z),cons(s(z),X_164)) != cons(s(z),merge(X_164,cons(s(z),nil)))
| cons(s(z),merge(X_164,cons(s(z),nil))) = cons(s(z),cons(s(z),X_164)) ),
inference(subst,[],[refute_0_55:[bind(X0,$fot(cons(s(z),cons(s(z),X_164)))),bind(Y0,$fot(cons(s(z),merge(X_164,cons(s(z),nil)))))]]) ).
cnf(refute_0_57,plain,
cons(s(z),merge(X_164,cons(s(z),nil))) = cons(s(z),cons(s(z),X_164)),
inference(resolve,[$cnf( $equal(cons(s(z),cons(s(z),X_164)),cons(s(z),merge(X_164,cons(s(z),nil)))) )],[refute_0_52,refute_0_56]) ).
cnf(refute_0_58,plain,
( cons(s(z),merge(X_164,cons(s(z),nil))) != cons(s(z),cons(s(z),X_164))
| tail(cons(s(z),merge(X_164,cons(s(z),nil)))) != merge(X_164,cons(s(z),nil))
| tail(cons(s(z),cons(s(z),X_164))) = merge(X_164,cons(s(z),nil)) ),
introduced(tautology,[equality,[$cnf( $equal(tail(cons(s(z),merge(X_164,cons(s(z),nil)))),merge(X_164,cons(s(z),nil))) ),[0,0],$fot(cons(s(z),cons(s(z),X_164)))]]) ).
cnf(refute_0_59,plain,
( tail(cons(s(z),merge(X_164,cons(s(z),nil)))) != merge(X_164,cons(s(z),nil))
| tail(cons(s(z),cons(s(z),X_164))) = merge(X_164,cons(s(z),nil)) ),
inference(resolve,[$cnf( $equal(cons(s(z),merge(X_164,cons(s(z),nil))),cons(s(z),cons(s(z),X_164))) )],[refute_0_57,refute_0_58]) ).
cnf(refute_0_60,plain,
tail(cons(s(z),cons(s(z),X_164))) = merge(X_164,cons(s(z),nil)),
inference(resolve,[$cnf( $equal(tail(cons(s(z),merge(X_164,cons(s(z),nil)))),merge(X_164,cons(s(z),nil))) )],[refute_0_9,refute_0_59]) ).
cnf(refute_0_61,plain,
tail(cons(s(z),cons(s(z),X_164))) = cons(s(z),X_164),
inference(subst,[],[refute_0_8:[bind(X,$fot(s(z))),bind(X2,$fot(cons(s(z),X_164)))]]) ).
cnf(refute_0_62,plain,
( tail(cons(s(z),cons(s(z),X_164))) != cons(s(z),X_164)
| tail(cons(s(z),cons(s(z),X_164))) != merge(X_164,cons(s(z),nil))
| cons(s(z),X_164) = merge(X_164,cons(s(z),nil)) ),
introduced(tautology,[equality,[$cnf( $equal(tail(cons(s(z),cons(s(z),X_164))),merge(X_164,cons(s(z),nil))) ),[0],$fot(cons(s(z),X_164))]]) ).
cnf(refute_0_63,plain,
( tail(cons(s(z),cons(s(z),X_164))) != merge(X_164,cons(s(z),nil))
| cons(s(z),X_164) = merge(X_164,cons(s(z),nil)) ),
inference(resolve,[$cnf( $equal(tail(cons(s(z),cons(s(z),X_164))),cons(s(z),X_164)) )],[refute_0_61,refute_0_62]) ).
cnf(refute_0_64,plain,
cons(s(z),X_164) = merge(X_164,cons(s(z),nil)),
inference(resolve,[$cnf( $equal(tail(cons(s(z),cons(s(z),X_164))),merge(X_164,cons(s(z),nil))) )],[refute_0_60,refute_0_63]) ).
cnf(refute_0_65,plain,
cons(s(z),cons(z,X_89)) = merge(cons(z,X_89),cons(s(z),nil)),
inference(subst,[],[refute_0_64:[bind(X_164,$fot(cons(z,X_89)))]]) ).
cnf(refute_0_66,plain,
( cons(s(z),cons(z,X_89)) != merge(cons(z,X_89),cons(s(z),nil))
| merge(cons(z,X_89),cons(s(z),nil)) = cons(s(z),cons(z,X_89)) ),
inference(subst,[],[refute_0_55:[bind(X0,$fot(cons(s(z),cons(z,X_89)))),bind(Y0,$fot(merge(cons(z,X_89),cons(s(z),nil))))]]) ).
cnf(refute_0_67,plain,
merge(cons(z,X_89),cons(s(z),nil)) = cons(s(z),cons(z,X_89)),
inference(resolve,[$cnf( $equal(cons(s(z),cons(z,X_89)),merge(cons(z,X_89),cons(s(z),nil))) )],[refute_0_65,refute_0_66]) ).
cnf(refute_0_68,plain,
( merge(cons(z,X_89),cons(s(z),nil)) != cons(s(z),cons(z,X_89))
| merge(cons(z,X_89),cons(s(z),nil)) != cons(z,merge(X_89,cons(s(z),nil)))
| cons(s(z),cons(z,X_89)) = cons(z,merge(X_89,cons(s(z),nil))) ),
introduced(tautology,[equality,[$cnf( $equal(merge(cons(z,X_89),cons(s(z),nil)),cons(z,merge(X_89,cons(s(z),nil)))) ),[0],$fot(cons(s(z),cons(z,X_89)))]]) ).
cnf(refute_0_69,plain,
( merge(cons(z,X_89),cons(s(z),nil)) != cons(z,merge(X_89,cons(s(z),nil)))
| cons(s(z),cons(z,X_89)) = cons(z,merge(X_89,cons(s(z),nil))) ),
inference(resolve,[$cnf( $equal(merge(cons(z,X_89),cons(s(z),nil)),cons(s(z),cons(z,X_89))) )],[refute_0_67,refute_0_68]) ).
cnf(refute_0_70,plain,
cons(s(z),cons(z,X_89)) = cons(z,merge(X_89,cons(s(z),nil))),
inference(resolve,[$cnf( $equal(merge(cons(z,X_89),cons(s(z),nil)),cons(z,merge(X_89,cons(s(z),nil)))) )],[refute_0_7,refute_0_69]) ).
cnf(refute_0_71,plain,
( cons(s(z),X_164) != merge(X_164,cons(s(z),nil))
| merge(X_164,cons(s(z),nil)) = cons(s(z),X_164) ),
inference(subst,[],[refute_0_55:[bind(X0,$fot(cons(s(z),X_164))),bind(Y0,$fot(merge(X_164,cons(s(z),nil))))]]) ).
cnf(refute_0_72,plain,
merge(X_164,cons(s(z),nil)) = cons(s(z),X_164),
inference(resolve,[$cnf( $equal(cons(s(z),X_164),merge(X_164,cons(s(z),nil))) )],[refute_0_64,refute_0_71]) ).
cnf(refute_0_73,plain,
merge(X_89,cons(s(z),nil)) = cons(s(z),X_89),
inference(subst,[],[refute_0_72:[bind(X_164,$fot(X_89))]]) ).
cnf(refute_0_74,plain,
cons(z,merge(X_89,cons(s(z),nil))) = cons(z,merge(X_89,cons(s(z),nil))),
introduced(tautology,[refl,[$fot(cons(z,merge(X_89,cons(s(z),nil))))]]) ).
cnf(refute_0_75,plain,
( cons(z,merge(X_89,cons(s(z),nil))) != cons(z,merge(X_89,cons(s(z),nil)))
| merge(X_89,cons(s(z),nil)) != cons(s(z),X_89)
| cons(z,merge(X_89,cons(s(z),nil))) = cons(z,cons(s(z),X_89)) ),
introduced(tautology,[equality,[$cnf( $equal(cons(z,merge(X_89,cons(s(z),nil))),cons(z,merge(X_89,cons(s(z),nil)))) ),[1,1],$fot(cons(s(z),X_89))]]) ).
cnf(refute_0_76,plain,
( merge(X_89,cons(s(z),nil)) != cons(s(z),X_89)
| cons(z,merge(X_89,cons(s(z),nil))) = cons(z,cons(s(z),X_89)) ),
inference(resolve,[$cnf( $equal(cons(z,merge(X_89,cons(s(z),nil))),cons(z,merge(X_89,cons(s(z),nil)))) )],[refute_0_74,refute_0_75]) ).
cnf(refute_0_77,plain,
cons(z,merge(X_89,cons(s(z),nil))) = cons(z,cons(s(z),X_89)),
inference(resolve,[$cnf( $equal(merge(X_89,cons(s(z),nil)),cons(s(z),X_89)) )],[refute_0_73,refute_0_76]) ).
cnf(refute_0_78,plain,
( cons(s(z),cons(z,X_89)) != cons(z,merge(X_89,cons(s(z),nil)))
| cons(z,merge(X_89,cons(s(z),nil))) != cons(z,cons(s(z),X_89))
| cons(s(z),cons(z,X_89)) = cons(z,cons(s(z),X_89)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(cons(s(z),cons(z,X_89)),cons(z,cons(s(z),X_89))) ),[0],$fot(cons(z,merge(X_89,cons(s(z),nil))))]]) ).
cnf(refute_0_79,plain,
( cons(s(z),cons(z,X_89)) != cons(z,merge(X_89,cons(s(z),nil)))
| cons(s(z),cons(z,X_89)) = cons(z,cons(s(z),X_89)) ),
inference(resolve,[$cnf( $equal(cons(z,merge(X_89,cons(s(z),nil))),cons(z,cons(s(z),X_89))) )],[refute_0_77,refute_0_78]) ).
cnf(refute_0_80,plain,
cons(s(z),cons(z,X_89)) = cons(z,cons(s(z),X_89)),
inference(resolve,[$cnf( $equal(cons(s(z),cons(z,X_89)),cons(z,merge(X_89,cons(s(z),nil)))) )],[refute_0_70,refute_0_79]) ).
cnf(refute_0_81,plain,
cons(s(z),cons(z,X_170)) = cons(z,cons(s(z),X_170)),
inference(subst,[],[refute_0_80:[bind(X_89,$fot(X_170))]]) ).
cnf(refute_0_82,plain,
( cons(s(z),cons(z,X_170)) != cons(z,cons(s(z),X_170))
| head(cons(s(z),cons(z,X_170))) != s(z)
| head(cons(z,cons(s(z),X_170))) = s(z) ),
introduced(tautology,[equality,[$cnf( $equal(head(cons(s(z),cons(z,X_170))),s(z)) ),[0,0],$fot(cons(z,cons(s(z),X_170)))]]) ).
cnf(refute_0_83,plain,
( head(cons(s(z),cons(z,X_170))) != s(z)
| head(cons(z,cons(s(z),X_170))) = s(z) ),
inference(resolve,[$cnf( $equal(cons(s(z),cons(z,X_170)),cons(z,cons(s(z),X_170))) )],[refute_0_81,refute_0_82]) ).
cnf(refute_0_84,plain,
head(cons(z,cons(s(z),X_170))) = s(z),
inference(resolve,[$cnf( $equal(head(cons(s(z),cons(z,X_170))),s(z)) )],[refute_0_1,refute_0_83]) ).
cnf(refute_0_85,plain,
head(cons(z,cons(s(z),X_170))) = z,
inference(subst,[],[refute_0_0:[bind(X,$fot(z)),bind(X2,$fot(cons(s(z),X_170)))]]) ).
cnf(refute_0_86,plain,
( head(cons(z,cons(s(z),X_170))) != s(z)
| head(cons(z,cons(s(z),X_170))) != z
| z = s(z) ),
introduced(tautology,[equality,[$cnf( $equal(head(cons(z,cons(s(z),X_170))),s(z)) ),[0],$fot(z)]]) ).
cnf(refute_0_87,plain,
( head(cons(z,cons(s(z),X_170))) != s(z)
| z = s(z) ),
inference(resolve,[$cnf( $equal(head(cons(z,cons(s(z),X_170))),z) )],[refute_0_85,refute_0_86]) ).
cnf(refute_0_88,plain,
z = s(z),
inference(resolve,[$cnf( $equal(head(cons(z,cons(s(z),X_170))),s(z)) )],[refute_0_84,refute_0_87]) ).
cnf(refute_0_89,plain,
z != s(X),
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_90,plain,
z != s(z),
inference(subst,[],[refute_0_89:[bind(X,$fot(z))]]) ).
cnf(refute_0_91,plain,
$false,
inference(resolve,[$cnf( $equal(z,s(z)) )],[refute_0_88,refute_0_90]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX199+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : metis --show proof --show saturation %s
% 0.16/0.33 % Computer : n011.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 11:11:32 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.75/0.92 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.75/0.92
% 0.75/0.92 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 0.75/0.93
%------------------------------------------------------------------------------