%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWX186+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n009.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:30 PM UTC 2026
% Result : Theorem 0.15s 0.34s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 8
% Syntax : Number of formulae : 35 ( 19 unt; 0 def)
% Number of atoms : 54 ( 53 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 47 ( 28 ~; 16 |; 0 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-2 aty)
% Number of variables : 72 ( 16 sgn 24 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_003,axiom,
! [X,X2] : nil != cons(X,X2) ).
fof(axiom_006,axiom,
! [Z] : drop(s(Z),nil) = nil ).
fof(axiom_007,axiom,
! [Z,X2,X3] : drop(s(Z),cons(X2,X3)) = drop(Z,X3) ).
fof(goal_009,conjecture,
? [N,Xs,Ys] :
~ ( drop(N,Xs) = drop(N,Ys)
=> Xs = Ys ) ).
fof(subgoal_0,plain,
? [N,Xs,Ys] :
~ ( drop(N,Xs) = drop(N,Ys)
=> Xs = Ys ),
inference(strip,[],[goal_009]) ).
fof(negate_0_0,plain,
~ ? [N,Xs,Ys] :
~ ( drop(N,Xs) = drop(N,Ys)
=> Xs = Ys ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
! [N,Xs,Ys] :
( drop(N,Xs) != drop(N,Ys)
| Xs = Ys ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,plain,
! [N,Xs,Ys] :
( drop(N,Xs) != drop(N,Ys)
| Xs = Ys ),
inference(specialize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [Z] : drop(s(Z),nil) = nil,
inference(canonicalize,[],[axiom_006]) ).
fof(normalize_0_3,plain,
! [Z] : drop(s(Z),nil) = nil,
inference(specialize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [X2,X3,Z] : drop(s(Z),cons(X2,X3)) = drop(Z,X3),
inference(canonicalize,[],[axiom_007]) ).
fof(normalize_0_5,plain,
! [X2,X3,Z] : drop(s(Z),cons(X2,X3)) = drop(Z,X3),
inference(specialize,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [X,X2] : nil != cons(X,X2),
inference(canonicalize,[],[axiom_003]) ).
fof(normalize_0_7,plain,
! [X,X2] : nil != cons(X,X2),
inference(specialize,[],[normalize_0_6]) ).
cnf(refute_0_0,plain,
( drop(N,Xs) != drop(N,Ys)
| Xs = Ys ),
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_1,plain,
( drop(s(Z),nil) != drop(s(Z),X_15)
| nil = X_15 ),
inference(subst,[],[refute_0_0:[bind(N,$fot(s(Z))),bind(Xs,$fot(nil)),bind(Ys,$fot(X_15))]]) ).
cnf(refute_0_2,plain,
drop(s(Z),nil) = nil,
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_3,plain,
( drop(s(Z),nil) != nil
| nil != drop(s(Z),X_15)
| drop(s(Z),nil) = drop(s(Z),X_15) ),
introduced(tautology,[equality,[$cnf( ~ $equal(drop(s(Z),nil),drop(s(Z),X_15)) ),[0],$fot(nil)]]) ).
cnf(refute_0_4,plain,
( nil != drop(s(Z),X_15)
| drop(s(Z),nil) = drop(s(Z),X_15) ),
inference(resolve,[$cnf( $equal(drop(s(Z),nil),nil) )],[refute_0_2,refute_0_3]) ).
cnf(refute_0_5,plain,
( nil != drop(s(Z),X_15)
| nil = X_15 ),
inference(resolve,[$cnf( $equal(drop(s(Z),nil),drop(s(Z),X_15)) )],[refute_0_4,refute_0_1]) ).
cnf(refute_0_6,plain,
( nil != drop(s(X_16),cons(X2,X3))
| nil = cons(X2,X3) ),
inference(subst,[],[refute_0_5:[bind(Z,$fot(X_16)),bind(X_15,$fot(cons(X2,X3)))]]) ).
cnf(refute_0_7,plain,
drop(s(Z),cons(X2,X3)) = drop(Z,X3),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_8,plain,
drop(s(X_16),cons(X2,X3)) = drop(X_16,X3),
inference(subst,[],[refute_0_7:[bind(Z,$fot(X_16))]]) ).
cnf(refute_0_9,plain,
( drop(s(X_16),cons(X2,X3)) != drop(X_16,X3)
| nil != drop(X_16,X3)
| nil = drop(s(X_16),cons(X2,X3)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(nil,drop(s(X_16),cons(X2,X3))) ),[1],$fot(drop(X_16,X3))]]) ).
cnf(refute_0_10,plain,
( nil != drop(X_16,X3)
| nil = drop(s(X_16),cons(X2,X3)) ),
inference(resolve,[$cnf( $equal(drop(s(X_16),cons(X2,X3)),drop(X_16,X3)) )],[refute_0_8,refute_0_9]) ).
cnf(refute_0_11,plain,
( nil != drop(X_16,X3)
| nil = cons(X2,X3) ),
inference(resolve,[$cnf( $equal(nil,drop(s(X_16),cons(X2,X3))) )],[refute_0_10,refute_0_6]) ).
cnf(refute_0_12,plain,
nil != cons(X,X2),
inference(canonicalize,[],[normalize_0_7]) ).
cnf(refute_0_13,plain,
nil != cons(X2,X3),
inference(subst,[],[refute_0_12:[bind(X,$fot(X2)),bind(X2,$fot(X3))]]) ).
cnf(refute_0_14,plain,
nil != drop(X_16,X3),
inference(resolve,[$cnf( $equal(nil,cons(X2,X3)) )],[refute_0_11,refute_0_13]) ).
cnf(refute_0_15,plain,
nil != drop(s(Z),nil),
inference(subst,[],[refute_0_14:[bind(X3,$fot(nil)),bind(X_16,$fot(s(Z)))]]) ).
cnf(refute_0_16,plain,
( drop(s(Z),nil) != nil
| nil != nil
| nil = drop(s(Z),nil) ),
introduced(tautology,[equality,[$cnf( ~ $equal(nil,drop(s(Z),nil)) ),[1],$fot(nil)]]) ).
cnf(refute_0_17,plain,
( nil != nil
| nil = drop(s(Z),nil) ),
inference(resolve,[$cnf( $equal(drop(s(Z),nil),nil) )],[refute_0_2,refute_0_16]) ).
cnf(refute_0_18,plain,
nil != nil,
inference(resolve,[$cnf( $equal(nil,drop(s(Z),nil)) )],[refute_0_17,refute_0_15]) ).
cnf(refute_0_19,plain,
nil = nil,
introduced(tautology,[refl,[$fot(nil)]]) ).
cnf(refute_0_20,plain,
$false,
inference(resolve,[$cnf( $equal(nil,nil) )],[refute_0_19,refute_0_18]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX186+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 : n009.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 09:37:25 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.15/0.34 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34
% 0.15/0.34 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 0.15/0.35
%------------------------------------------------------------------------------