%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWX200+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:32:05 PM UTC 2026
% Result : Theorem 24.33s 3.57s
% Output : Proof 24.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 5
% Syntax : Number of formulae : 25 ( 14 unt; 0 def)
% Number of atoms : 50 ( 4 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 44 ( 19 ~; 15 |; 5 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 35 ( 5 sgn 19 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f14,axiom,
! [Y,Y2,Xs] :
( ord(cons(Y,cons(Y2,Xs)))
<=> ( ord(cons(Y2,Xs))
& leqNat(Y,Y2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_015) ).
fof(f14_nnf,plain,
! [Y,Y2,Xs] :
( ( ~ ord(cons(Y2,Xs))
| ~ leqNat(Y,Y2)
| ord(cons(Y,cons(Y2,Xs))) )
& ( ( ord(cons(Y2,Xs))
& leqNat(Y,Y2) )
| ~ ord(cons(Y,cons(Y2,Xs))) ) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [Y,Y2,Xs] :
( ( ~ ord(cons(Y2,Xs))
| ~ leqNat(Y,Y2)
| ord(cons(Y,cons(Y2,Xs))) )
& ( ( ord(cons(Y2,Xs))
& leqNat(Y,Y2) )
| ~ ord(cons(Y,cons(Y2,Xs))) ) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c15,plain,
( leqNat(X0,X1)
| ~ ord(cons(X0,cons(X1,X2))) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
fof(f8,axiom,
! [Y] : merge(nil,Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_009) ).
fof(f8_nnf,plain,
! [Y] : merge(nil,Y) = Y,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [Y] : merge(nil,Y) = Y,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c9,plain,
merge(nil,X0) = X0,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
fof(f12,axiom,
ord(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_013) ).
fof(f12_nnf,plain,
ord(nil),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c13,plain,
ord(nil),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
fof(f15,conjecture,
? [Xs,Ys] :
~ ( ord(Xs)
=> ( ~ ord(Ys)
=> ord(merge(Xs,Ys)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_016) ).
fof(f15_neg,negated_conjecture,
~ ? [Xs,Ys] :
~ ( ord(Xs)
=> ( ~ ord(Ys)
=> ord(merge(Xs,Ys)) ) ),
inference(negated_conjecture,[status(cth)],[f15]) ).
fof(f15_nnf,plain,
! [Xs,Ys] :
( ord(merge(Xs,Ys))
| ord(Ys)
| ~ ord(Xs) ),
inference(nnf_transformation,[status(thm)],[f15_neg]) ).
fof(f15_sk,plain,
! [Xs,Ys] :
( ord(merge(Xs,Ys))
| ord(Ys)
| ~ ord(Xs) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c18,plain,
( ord(merge(X0,X1))
| ord(X1)
| ~ ord(X0) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p19,plain,
( ord(merge(nil,X0))
| ord(X0) ),
inference(resolution,[status(thm)],[c13,c18]) ).
cnf(p82,plain,
( ord(X0)
| ord(X0) ),
inference(superposition,[status(thm)],[c9,p19]) ).
cnf(p120,plain,
ord(X0),
inference(factoring,[status(thm)],[p82]) ).
cnf(p124,plain,
leqNat(X0,X1),
inference(resolution,[status(thm)],[c15,p120]) ).
fof(f6,axiom,
! [Z] : ~ leqNat(s(Z),z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_007) ).
fof(f6_nnf,plain,
! [Z] : ~ leqNat(s(Z),z),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [Z] : ~ leqNat(s(Z),z),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
~ leqNat(s(X0),z),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p125,plain,
$false,
inference(resolution,[status(thm)],[p124,c6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX200+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n006.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 23:36:10 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 24.33/3.57 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.33/3.57 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------