%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX200+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 : Thu Sep 24 03:13:46 PM UTC 2026
% Result : Theorem 0.15s 5.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX200+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n016.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 10:37:14 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.38 % Drodi V4.1.1
% 0.15/5.40 % Refutation found
% 0.15/5.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/5.40 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.40 fof(f7,axiom,(
% 0.15/5.40 (! [Z] : ~ leqNat(s(Z),z) )),
% 0.15/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.40 fof(f9,axiom,(
% 0.15/5.40 (! [Y] : merge(nil,Y) = Y )),
% 0.15/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.40 fof(f13,axiom,(
% 0.15/5.40 ord(nil) ),
% 0.15/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.40 fof(f15,axiom,(
% 0.15/5.40 (! [Y,Y2,Xs] :( ord(cons(Y,cons(Y2,Xs)))<=> ( leqNat(Y,Y2)& ord(cons(Y2,Xs)) ) ) )),
% 0.15/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.40 fof(f16,conjecture,(
% 0.15/5.40 (? [Xs,Ys] :~ ( ord(Xs)=> ( ~ ord(Ys)=> ord(merge(Xs,Ys)) ) ) )),
% 0.15/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.40 fof(f17,negated_conjecture,(
% 0.15/5.40 ~((? [Xs,Ys] :~ ( ord(Xs)=> ( ~ ord(Ys)=> ord(merge(Xs,Ys)) ) ) ))),
% 0.15/5.40 inference(negated_conjecture,[status(cth)],[f16])).
% 0.15/5.40 fof(f24,plain,(
% 0.15/5.40 ![X0]: (~leqNat(s(X0),z))),
% 0.15/5.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.15/5.40 fof(f29,plain,(
% 0.15/5.40 ![X0]: (merge(nil,X0)=X0)),
% 0.15/5.40 inference(cnf_transformation,[status(thm)],[f9])).
% 0.15/5.40 fof(f37,plain,(
% 0.15/5.40 ord(nil)),
% 0.15/5.40 inference(cnf_transformation,[status(thm)],[f13])).
% 0.15/5.40 fof(f39,plain,(
% 0.15/5.40 ![Y,Y2,Xs]: ((~ord(cons(Y,cons(Y2,Xs)))|(leqNat(Y,Y2)&ord(cons(Y2,Xs))))&(ord(cons(Y,cons(Y2,Xs)))|(~leqNat(Y,Y2)|~ord(cons(Y2,Xs)))))),
% 0.15/5.40 inference(NNF_transformation,[status(thm)],[f15])).
% 0.15/5.40 fof(f40,plain,(
% 0.15/5.40 (![Y,Y2,Xs]: (~ord(cons(Y,cons(Y2,Xs)))|(leqNat(Y,Y2)&ord(cons(Y2,Xs)))))&(![Y,Y2,Xs]: (ord(cons(Y,cons(Y2,Xs)))|(~leqNat(Y,Y2)|~ord(cons(Y2,Xs)))))),
% 0.15/5.40 inference(miniscoping,[status(thm)],[f39])).
% 0.15/5.40 fof(f41,plain,(
% 0.15/5.40 ![X0,X1,X2]: (~ord(cons(X0,cons(X1,X2)))|leqNat(X0,X1))),
% 0.15/5.40 inference(cnf_transformation,[status(thm)],[f40])).
% 0.15/5.40 fof(f44,plain,(
% 0.15/5.40 (![Xs,Ys]: (~ord(Xs)|(ord(Ys)|ord(merge(Xs,Ys)))))),
% 0.15/5.40 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.15/5.40 fof(f45,plain,(
% 0.15/5.40 ![Xs]: (~ord(Xs)|(![Ys]: (ord(Ys)|ord(merge(Xs,Ys)))))),
% 0.15/5.40 inference(miniscoping,[status(thm)],[f44])).
% 0.15/5.40 fof(f46,plain,(
% 0.15/5.40 ![X0,X1]: (~ord(X0)|ord(X1)|ord(merge(X0,X1)))),
% 0.15/5.40 inference(cnf_transformation,[status(thm)],[f45])).
% 0.15/5.40 fof(f52,plain,(
% 0.15/5.40 ![X0]: (~ord(nil)|ord(X0)|ord(X0))),
% 0.15/5.40 inference(paramodulation,[status(thm)],[f29,f46])).
% 0.15/5.40 fof(f53,plain,(
% 0.15/5.40 ![X0]: (~ord(nil)|ord(X0))),
% 0.15/5.40 inference(duplicate_literals_removal,[status(thm)],[f52])).
% 0.15/5.40 fof(f54,plain,(
% 0.15/5.40 ![X0,X1]: (leqNat(X0,X1))),
% 0.15/5.40 inference(backward_subsumption_resolution,[status(thm)],[f41,f55])).
% 0.15/5.40 fof(f55,plain,(
% 0.15/5.40 ![X0]: (ord(X0))),
% 0.15/5.40 inference(forward_subsumption_resolution,[status(thm)],[f53,f37])).
% 0.15/5.40 fof(f58,plain,(
% 0.15/5.40 $false),
% 0.15/5.40 inference(backward_subsumption_resolution,[status(thm)],[f24,f54])).
% 0.15/5.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/5.43 % Elapsed time: 0.051078 seconds
% 0.15/5.43 % CPU time: 0.139895 seconds
% 0.15/5.43 % Total memory used: 73.106 MB
% 0.15/5.43 % Net memory used: 72.834 MB
%------------------------------------------------------------------------------