%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWX222+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 07:04:36 PM UTC 2026
% Result : Theorem 0.39s 0.58s
% Output : CNFRefutation 0.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 9
% Syntax : Number of formulae : 58 ( 22 unt; 0 def)
% Number of atoms : 109 ( 31 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 104 ( 53 ~; 35 |; 6 &)
% ( 9 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 116 ( 15 sgn 56 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_026,axiom,
! [E] :
( nf(lam(E))
<=> nf(E) ) ).
fof(axiom_027,axiom,
! [X4] : nf(var(X4)) ).
fof(axiom_029,axiom,
! [Z,Xs] : index(cons(Z,Xs),zero) = just(Z) ).
fof(axiom_033,axiom,
! [X,E,Tx2,T1] :
( tc(X,lam(E),arr(Tx2,T1))
<=> tc(cons(Tx2,X),E,T1) ) ).
fof(axiom_035,axiom,
! [X,Z,X3,Tx3] :
( index(X,X3) = just(Tx3)
=> ( tc(X,var(X3),Z)
<=> Tx3 = Z ) ) ).
fof(goal_036,conjecture,
? [E] :
( nf(E)
& tc(nil,E,arr(a,arr(b,b))) ) ).
fof(subgoal_0,plain,
? [E] :
( nf(E)
& tc(nil,E,arr(a,arr(b,b))) ),
inference(strip,[],[goal_036]) ).
fof(negate_0_0,plain,
~ ? [E] :
( nf(E)
& tc(nil,E,arr(a,arr(b,b))) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
! [E] :
( ~ nf(E)
| ~ tc(nil,E,arr(a,arr(b,b))) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,plain,
! [E] :
( ~ nf(E)
| ~ tc(nil,E,arr(a,arr(b,b))) ),
inference(specialize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [E,T1,Tx2,X] :
( ~ tc(X,lam(E),arr(Tx2,T1))
<=> ~ tc(cons(Tx2,X),E,T1) ),
inference(canonicalize,[],[axiom_033]) ).
fof(normalize_0_3,plain,
! [E,T1,Tx2,X] :
( ~ tc(X,lam(E),arr(Tx2,T1))
<=> ~ tc(cons(Tx2,X),E,T1) ),
inference(specialize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [E,T1,Tx2,X] :
( ( ~ tc(X,lam(E),arr(Tx2,T1))
| tc(cons(Tx2,X),E,T1) )
& ( ~ tc(cons(Tx2,X),E,T1)
| tc(X,lam(E),arr(Tx2,T1)) ) ),
inference(clausify,[],[normalize_0_3]) ).
fof(normalize_0_5,plain,
! [E,T1,Tx2,X] :
( ~ tc(cons(Tx2,X),E,T1)
| tc(X,lam(E),arr(Tx2,T1)) ),
inference(conjunct,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [Tx3,X,X3,Z] :
( index(X,X3) != just(Tx3)
| ( Tx3 != Z
<=> ~ tc(X,var(X3),Z) ) ),
inference(canonicalize,[],[axiom_035]) ).
fof(normalize_0_7,plain,
! [Tx3,X,X3,Z] :
( index(X,X3) != just(Tx3)
| ( Tx3 != Z
<=> ~ tc(X,var(X3),Z) ) ),
inference(specialize,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
! [Tx3,X,X3,Z] :
( ( Tx3 != Z
| index(X,X3) != just(Tx3)
| tc(X,var(X3),Z) )
& ( index(X,X3) != just(Tx3)
| ~ tc(X,var(X3),Z)
| Tx3 = Z ) ),
inference(clausify,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
! [Tx3,X,X3,Z] :
( Tx3 != Z
| index(X,X3) != just(Tx3)
| tc(X,var(X3),Z) ),
inference(conjunct,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
! [Xs,Z] : index(cons(Z,Xs),zero) = just(Z),
inference(canonicalize,[],[axiom_029]) ).
fof(normalize_0_11,plain,
! [Xs,Z] : index(cons(Z,Xs),zero) = just(Z),
inference(specialize,[],[normalize_0_10]) ).
fof(normalize_0_12,plain,
! [E] :
( ~ nf(E)
<=> ~ nf(lam(E)) ),
inference(canonicalize,[],[axiom_026]) ).
fof(normalize_0_13,plain,
! [E] :
( ~ nf(E)
<=> ~ nf(lam(E)) ),
inference(specialize,[],[normalize_0_12]) ).
fof(normalize_0_14,plain,
! [E] :
( ( ~ nf(E)
| nf(lam(E)) )
& ( ~ nf(lam(E))
| nf(E) ) ),
inference(clausify,[],[normalize_0_13]) ).
fof(normalize_0_15,plain,
! [E] :
( ~ nf(E)
| nf(lam(E)) ),
inference(conjunct,[],[normalize_0_14]) ).
fof(normalize_0_16,plain,
! [X4] : nf(var(X4)),
inference(canonicalize,[],[axiom_027]) ).
fof(normalize_0_17,plain,
! [X4] : nf(var(X4)),
inference(specialize,[],[normalize_0_16]) ).
cnf(refute_0_0,plain,
( ~ nf(E)
| ~ tc(nil,E,arr(a,arr(b,b))) ),
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_1,plain,
( ~ nf(lam(lam(var(zero))))
| ~ tc(nil,lam(lam(var(zero))),arr(a,arr(b,b))) ),
inference(subst,[],[refute_0_0:[bind(E,$fot(lam(lam(var(zero)))))]]) ).
cnf(refute_0_2,plain,
( ~ tc(cons(Tx2,X),E,T1)
| tc(X,lam(E),arr(Tx2,T1)) ),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_3,plain,
( ~ tc(cons(Tx2,X),lam(var(zero)),arr(X_334,X_334))
| tc(X,lam(lam(var(zero))),arr(Tx2,arr(X_334,X_334))) ),
inference(subst,[],[refute_0_2:[bind(E,$fot(lam(var(zero)))),bind(T1,$fot(arr(X_334,X_334)))]]) ).
cnf(refute_0_4,plain,
( Tx3 != Z
| index(X,X3) != just(Tx3)
| tc(X,var(X3),Z) ),
inference(canonicalize,[],[normalize_0_9]) ).
cnf(refute_0_5,plain,
( Z != Z
| index(X,X3) != just(Z)
| tc(X,var(X3),Z) ),
inference(subst,[],[refute_0_4:[bind(Tx3,$fot(Z))]]) ).
cnf(refute_0_6,plain,
Z = Z,
introduced(tautology,[refl,[$fot(Z)]]) ).
cnf(refute_0_7,plain,
( index(X,X3) != just(Z)
| tc(X,var(X3),Z) ),
inference(resolve,[$cnf( $equal(Z,Z) )],[refute_0_6,refute_0_5]) ).
cnf(refute_0_8,plain,
( index(cons(Z,Xs),zero) != just(X_104)
| tc(cons(Z,Xs),var(zero),X_104) ),
inference(subst,[],[refute_0_7:[bind(X,$fot(cons(Z,Xs))),bind(X3,$fot(zero)),bind(Z,$fot(X_104))]]) ).
cnf(refute_0_9,plain,
index(cons(Z,Xs),zero) = just(Z),
inference(canonicalize,[],[normalize_0_11]) ).
cnf(refute_0_10,plain,
( index(cons(Z,Xs),zero) != just(Z)
| just(Z) != just(X_104)
| index(cons(Z,Xs),zero) = just(X_104) ),
introduced(tautology,[equality,[$cnf( ~ $equal(index(cons(Z,Xs),zero),just(X_104)) ),[0],$fot(just(Z))]]) ).
cnf(refute_0_11,plain,
( just(Z) != just(X_104)
| index(cons(Z,Xs),zero) = just(X_104) ),
inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(Z)) )],[refute_0_9,refute_0_10]) ).
cnf(refute_0_12,plain,
( just(Z) != just(X_104)
| tc(cons(Z,Xs),var(zero),X_104) ),
inference(resolve,[$cnf( $equal(index(cons(Z,Xs),zero),just(X_104)) )],[refute_0_11,refute_0_8]) ).
cnf(refute_0_13,plain,
( just(X_104) != just(X_104)
| tc(cons(X_104,Xs),var(zero),X_104) ),
inference(subst,[],[refute_0_12:[bind(Z,$fot(X_104))]]) ).
cnf(refute_0_14,plain,
just(X_104) = just(X_104),
introduced(tautology,[refl,[$fot(just(X_104))]]) ).
cnf(refute_0_15,plain,
tc(cons(X_104,Xs),var(zero),X_104),
inference(resolve,[$cnf( $equal(just(X_104),just(X_104)) )],[refute_0_14,refute_0_13]) ).
cnf(refute_0_16,plain,
tc(cons(X_331,X_333),var(zero),X_331),
inference(subst,[],[refute_0_15:[bind(Xs,$fot(X_333)),bind(X_104,$fot(X_331))]]) ).
cnf(refute_0_17,plain,
( ~ tc(cons(X_331,X_333),var(zero),X_331)
| tc(X_333,lam(var(zero)),arr(X_331,X_331)) ),
inference(subst,[],[refute_0_2:[bind(E,$fot(var(zero))),bind(T1,$fot(X_331)),bind(Tx2,$fot(X_331)),bind(X,$fot(X_333))]]) ).
cnf(refute_0_18,plain,
tc(X_333,lam(var(zero)),arr(X_331,X_331)),
inference(resolve,[$cnf( tc(cons(X_331,X_333),var(zero),X_331) )],[refute_0_16,refute_0_17]) ).
cnf(refute_0_19,plain,
tc(cons(Tx2,X),lam(var(zero)),arr(X_334,X_334)),
inference(subst,[],[refute_0_18:[bind(X_331,$fot(X_334)),bind(X_333,$fot(cons(Tx2,X)))]]) ).
cnf(refute_0_20,plain,
tc(X,lam(lam(var(zero))),arr(Tx2,arr(X_334,X_334))),
inference(resolve,[$cnf( tc(cons(Tx2,X),lam(var(zero)),arr(X_334,X_334)) )],[refute_0_19,refute_0_3]) ).
cnf(refute_0_21,plain,
tc(nil,lam(lam(var(zero))),arr(a,arr(b,b))),
inference(subst,[],[refute_0_20:[bind(Tx2,$fot(a)),bind(X,$fot(nil)),bind(X_334,$fot(b))]]) ).
cnf(refute_0_22,plain,
~ nf(lam(lam(var(zero)))),
inference(resolve,[$cnf( tc(nil,lam(lam(var(zero))),arr(a,arr(b,b))) )],[refute_0_21,refute_0_1]) ).
cnf(refute_0_23,plain,
( ~ nf(E)
| nf(lam(E)) ),
inference(canonicalize,[],[normalize_0_15]) ).
cnf(refute_0_24,plain,
( ~ nf(lam(var(X_29)))
| nf(lam(lam(var(X_29)))) ),
inference(subst,[],[refute_0_23:[bind(E,$fot(lam(var(X_29))))]]) ).
cnf(refute_0_25,plain,
nf(var(X4)),
inference(canonicalize,[],[normalize_0_17]) ).
cnf(refute_0_26,plain,
( ~ nf(var(X4))
| nf(lam(var(X4))) ),
inference(subst,[],[refute_0_23:[bind(E,$fot(var(X4)))]]) ).
cnf(refute_0_27,plain,
nf(lam(var(X4))),
inference(resolve,[$cnf( nf(var(X4)) )],[refute_0_25,refute_0_26]) ).
cnf(refute_0_28,plain,
nf(lam(var(X_29))),
inference(subst,[],[refute_0_27:[bind(X4,$fot(X_29))]]) ).
cnf(refute_0_29,plain,
nf(lam(lam(var(X_29)))),
inference(resolve,[$cnf( nf(lam(var(X_29))) )],[refute_0_28,refute_0_24]) ).
cnf(refute_0_30,plain,
nf(lam(lam(var(zero)))),
inference(subst,[],[refute_0_29:[bind(X_29,$fot(zero))]]) ).
cnf(refute_0_31,plain,
$false,
inference(resolve,[$cnf( nf(lam(lam(var(zero)))) )],[refute_0_30,refute_0_22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX222+1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.12 % Command : metis --show proof --show saturation %s
% 0.15/0.33 % Computer : n010.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:32:51 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.39/0.58 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.58
% 0.39/0.58 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.39/0.58
%------------------------------------------------------------------------------