%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX199-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 : n010.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 : Unsatisfiable 112.74s 19.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX199-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n010.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 10:33:04 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 % Drodi V4.1.1
% 112.74/19.62 % Refutation found
% 112.74/19.62 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 112.74/19.62 % SZS output start CNFRefutation for theBenchmark
% 112.74/19.62 fof(f1,axiom,(
% 112.74/19.62 (![Z,Xs,Y2,Ys]: (aux(Z,Xs,Y2,Ys,btrue) = cons(Z,merge(Xs,cons(Y2,Ys))) ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f3,axiom,(
% 112.74/19.62 (![Y]: (leqNat(z,Y) = btrue ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f5,axiom,(
% 112.74/19.62 (![Z,M]: (leqNat(s(Z),s(M)) = leqNat(Z,M) ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f6,axiom,(
% 112.74/19.62 (![Y]: (merge(nil,Y) = Y ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f7,axiom,(
% 112.74/19.62 (![Z,Xs]: (merge(cons(Z,Xs),nil) = cons(Z,Xs) ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f8,axiom,(
% 112.74/19.62 (![Z,Xs,Y2,Ys]: (merge(cons(Z,Xs),cons(Y2,Ys)) = aux(Z,Xs,Y2,Ys,leqNat(Z,Y2)) ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f9,axiom,(
% 112.74/19.62 (![Q]: (impl(btrue,Q) = Q ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f11,axiom,(
% 112.74/19.62 (![X,Y,Z]: (prop_merge_comm(X,Y,Z) = impl(eq(merge(X,Y),merge(Y,X)),impl(eq(merge(X,Z),merge(Z,X)),eq(merge(Y,Z),merge(Z,Y)))) ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f16,axiom,(
% 112.74/19.62 (![X]: (eq2(s(X),z) = bfalse ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f17,axiom,(
% 112.74/19.62 (![X]: (eq(X,X) = btrue ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f18,axiom,(
% 112.74/19.62 (![X]: (eq2(X,X) = btrue ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f19,axiom,(
% 112.74/19.62 (![X]: (eq3(X,X) = btrue ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f20,axiom,(
% 112.74/19.62 (![X,Z,Y,X2]: (( eq2(X,Z) != bfalse| eq(cons(X,Y),cons(Z,X2)) = bfalse ) ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f21,axiom,(
% 112.74/19.62 (![X,Z,Y,X2]: (( eq2(X,Z) != btrue| eq(cons(X,Y),cons(Z,X2)) = eq(Y,X2) ) ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f24,negated_conjecture,(
% 112.74/19.62 (![X,Y,Z]: (eq3(prop_merge_comm(X,Y,Z),bfalse) != btrue ))),
% 112.74/19.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.62 fof(f25,plain,(
% 112.74/19.62 ![X0,X1,X2,X3]: (aux(X0,X1,X2,X3,btrue)=cons(X0,merge(X1,cons(X2,X3))))),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f1])).
% 112.74/19.62 fof(f27,plain,(
% 112.74/19.62 ![X0]: (leqNat(z,X0)=btrue)),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f3])).
% 112.74/19.62 fof(f29,plain,(
% 112.74/19.62 ![X0,X1]: (leqNat(s(X0),s(X1))=leqNat(X0,X1))),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f5])).
% 112.74/19.62 fof(f30,plain,(
% 112.74/19.62 ![X0]: (merge(nil,X0)=X0)),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f6])).
% 112.74/19.62 fof(f31,plain,(
% 112.74/19.62 ![X0,X1]: (merge(cons(X0,X1),nil)=cons(X0,X1))),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f7])).
% 112.74/19.62 fof(f32,plain,(
% 112.74/19.62 ![X0,X1,X2,X3]: (merge(cons(X0,X1),cons(X2,X3))=aux(X0,X1,X2,X3,leqNat(X0,X2)))),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f8])).
% 112.74/19.62 fof(f33,plain,(
% 112.74/19.62 ![X0]: (impl(btrue,X0)=X0)),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f9])).
% 112.74/19.62 fof(f35,plain,(
% 112.74/19.62 ![X0,X1,X2]: (prop_merge_comm(X0,X1,X2)=impl(eq(merge(X0,X1),merge(X1,X0)),impl(eq(merge(X0,X2),merge(X2,X0)),eq(merge(X1,X2),merge(X2,X1)))))),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f11])).
% 112.74/19.62 fof(f40,plain,(
% 112.74/19.62 ![X0]: (eq2(s(X0),z)=bfalse)),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f16])).
% 112.74/19.62 fof(f41,plain,(
% 112.74/19.62 ![X0]: (eq(X0,X0)=btrue)),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f17])).
% 112.74/19.62 fof(f42,plain,(
% 112.74/19.62 ![X0]: (eq2(X0,X0)=btrue)),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f18])).
% 112.74/19.62 fof(f43,plain,(
% 112.74/19.62 ![X0]: (eq3(X0,X0)=btrue)),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f19])).
% 112.74/19.62 fof(f44,plain,(
% 112.74/19.62 ![X,Z]: (~eq2(X,Z)=bfalse|(![Y,X2]: eq(cons(X,Y),cons(Z,X2))=bfalse))),
% 112.74/19.62 inference(miniscoping,[status(thm)],[f20])).
% 112.74/19.62 fof(f45,plain,(
% 112.74/19.62 ![X0,X1,X2,X3]: (~eq2(X0,X1)=bfalse|eq(cons(X0,X2),cons(X1,X3))=bfalse)),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f44])).
% 112.74/19.62 fof(f46,plain,(
% 112.74/19.62 ![X,Z]: (~eq2(X,Z)=btrue|(![Y,X2]: eq(cons(X,Y),cons(Z,X2))=eq(Y,X2)))),
% 112.74/19.62 inference(miniscoping,[status(thm)],[f21])).
% 112.74/19.62 fof(f47,plain,(
% 112.74/19.62 ![X0,X1,X2,X3]: (~eq2(X0,X1)=btrue|eq(cons(X0,X2),cons(X1,X3))=eq(X2,X3))),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f46])).
% 112.74/19.62 fof(f50,plain,(
% 112.74/19.62 ![X0,X1,X2]: (~eq3(prop_merge_comm(X0,X1,X2),bfalse)=btrue)),
% 112.74/19.62 inference(cnf_transformation,[status(thm)],[f24])).
% 112.74/19.62 fof(f140,plain,(
% 112.74/19.62 ![X0,X1,X2]: (prop_merge_comm(nil,X0,cons(X1,X2))=impl(eq(merge(nil,X0),merge(X0,nil)),impl(eq(merge(nil,cons(X1,X2)),cons(X1,X2)),eq(merge(X0,cons(X1,X2)),merge(cons(X1,X2),X0)))))),
% 112.74/19.62 inference(paramodulation,[status(thm)],[f31,f35])).
% 112.74/19.62 fof(f209,plain,(
% 112.74/19.62 ![X0,X1,X2]: (prop_merge_comm(nil,X0,cons(X1,X2))=impl(eq(X0,merge(X0,nil)),impl(eq(merge(nil,cons(X1,X2)),cons(X1,X2)),eq(merge(X0,cons(X1,X2)),merge(cons(X1,X2),X0)))))),
% 112.74/19.62 inference(forward_demodulation,[status(thm)],[f30,f140])).
% 112.74/19.62 fof(f210,plain,(
% 112.74/19.62 ![X0,X1,X2]: (prop_merge_comm(nil,X0,cons(X1,X2))=impl(eq(X0,merge(X0,nil)),impl(eq(cons(X1,X2),cons(X1,X2)),eq(merge(X0,cons(X1,X2)),merge(cons(X1,X2),X0)))))),
% 112.74/19.62 inference(forward_demodulation,[status(thm)],[f30,f209])).
% 112.74/19.62 fof(f211,plain,(
% 112.74/19.62 ![X0,X1,X2]: (prop_merge_comm(nil,X0,cons(X1,X2))=impl(eq(X0,merge(X0,nil)),impl(btrue,eq(merge(X0,cons(X1,X2)),merge(cons(X1,X2),X0)))))),
% 112.74/19.62 inference(forward_demodulation,[status(thm)],[f41,f210])).
% 112.74/19.62 fof(f212,plain,(
% 112.74/19.62 ![X0,X1,X2]: (prop_merge_comm(nil,X0,cons(X1,X2))=impl(eq(X0,merge(X0,nil)),eq(merge(X0,cons(X1,X2)),merge(cons(X1,X2),X0))))),
% 112.74/19.62 inference(forward_demodulation,[status(thm)],[f33,f211])).
% 112.74/19.62 fof(f245,plain,(
% 112.74/19.62 ![X0,X1,X2,X3]: (merge(cons(s(X0),X1),cons(s(X2),X3))=aux(s(X0),X1,s(X2),X3,leqNat(X0,X2)))),
% 112.74/19.62 inference(paramodulation,[status(thm)],[f29,f32])).
% 112.74/19.62 fof(f247,plain,(
% 112.74/19.62 ![X0,X1,X2]: (merge(cons(z,X0),cons(X1,X2))=aux(z,X0,X1,X2,btrue))),
% 112.74/19.62 inference(paramodulation,[status(thm)],[f27,f32])).
% 112.74/19.62 fof(f248,plain,(
% 112.74/19.62 ![X0,X1,X2]: (eq(cons(s(X0),X1),cons(z,X2))=bfalse)),
% 112.74/19.62 inference(resolution,[status(thm)],[f45,f40])).
% 112.74/19.62 fof(f472,plain,(
% 112.74/19.62 ![X0,X1,X2,X3,X4]: (eq(cons(s(X0),X1),aux(z,X2,X3,X4,btrue))=bfalse)),
% 112.74/19.62 inference(paramodulation,[status(thm)],[f25,f248])).
% 112.74/19.62 fof(f501,plain,(
% 112.74/19.62 ![X0,X1,X2]: (eq(cons(X0,X1),cons(X0,X2))=eq(X1,X2))),
% 112.74/19.62 inference(resolution,[status(thm)],[f47,f42])).
% 112.74/19.62 fof(f928,plain,(
% 112.74/19.62 ![X0,X1,X2,X3]: (prop_merge_comm(nil,cons(X0,X1),cons(X2,X3))=impl(eq(cons(X0,X1),cons(X0,X1)),eq(merge(cons(X0,X1),cons(X2,X3)),merge(cons(X2,X3),cons(X0,X1)))))),
% 112.74/19.62 inference(paramodulation,[status(thm)],[f31,f212])).
% 112.74/19.62 fof(f942,plain,(
% 112.74/19.62 ![X0,X1,X2,X3]: (prop_merge_comm(nil,cons(X0,X1),cons(X2,X3))=impl(btrue,eq(merge(cons(X0,X1),cons(X2,X3)),merge(cons(X2,X3),cons(X0,X1)))))),
% 112.74/19.62 inference(forward_demodulation,[status(thm)],[f41,f928])).
% 112.74/19.62 fof(f943,plain,(
% 112.74/19.62 ![X0,X1,X2,X3]: (prop_merge_comm(nil,cons(X0,X1),cons(X2,X3))=eq(merge(cons(X0,X1),cons(X2,X3)),merge(cons(X2,X3),cons(X0,X1))))),
% 112.74/19.62 inference(forward_demodulation,[status(thm)],[f33,f942])).
% 112.74/19.62 fof(f981,plain,(
% 112.74/19.62 ![X0,X1,X2,X3,X4]: (eq(aux(X0,X1,X2,X3,btrue),cons(X0,X4))=eq(merge(X1,cons(X2,X3)),X4))),
% 112.74/19.62 inference(paramodulation,[status(thm)],[f25,f501])).
% 112.74/19.62 fof(f2687,plain,(
% 112.74/19.62 ![X0,X1,X2,X3,X4,X5,X6]: (eq(aux(X0,X1,X2,X3,btrue),aux(X0,X4,X5,X6,btrue))=eq(merge(X1,cons(X2,X3)),merge(X4,cons(X5,X6))))),
% 112.74/19.62 inference(paramodulation,[status(thm)],[f25,f981])).
% 112.74/19.62 fof(f3124,plain,(
% 112.74/19.62 ![X0,X1,X2]: (merge(cons(s(z),X0),cons(s(X1),X2))=aux(s(z),X0,s(X1),X2,btrue))),
% 112.74/19.62 inference(paramodulation,[status(thm)],[f27,f245])).
% 112.74/19.62 fof(f4480,plain,(
% 112.74/19.62 ![X0,X1,X2]: (prop_merge_comm(nil,cons(s(X0),X1),cons(s(z),X2))=eq(merge(cons(s(X0),X1),cons(s(z),X2)),aux(s(z),X2,s(X0),X1,btrue)))),
% 112.74/19.62 inference(paramodulation,[status(thm)],[f3124,f943])).
% 112.74/19.62 fof(f119282,plain,(
% 112.74/19.62 ![X0,X1]: (prop_merge_comm(nil,cons(s(z),X0),cons(s(z),X1))=eq(aux(s(z),X0,s(z),X1,btrue),aux(s(z),X1,s(z),X0,btrue)))),
% 112.74/19.62 inference(paramodulation,[status(thm)],[f3124,f4480])).
% 112.74/19.62 fof(f119379,plain,(
% 112.74/19.62 ![X0,X1]: (prop_merge_comm(nil,cons(s(z),X0),cons(s(z),X1))=eq(merge(X0,cons(s(z),X1)),merge(X1,cons(s(z),X0))))),
% 112.74/19.62 inference(forward_demodulation,[status(thm)],[f2687,f119282])).
% 112.74/19.62 fof(f165541,plain,(
% 112.74/19.62 ![X0]: (prop_merge_comm(nil,cons(s(z),nil),cons(s(z),X0))=eq(cons(s(z),X0),merge(X0,cons(s(z),nil))))),
% 112.74/19.62 inference(paramodulation,[status(thm)],[f30,f119379])).
% 71.93/19.79 fof(f165699,plain,(
% 71.93/19.79 ![X0]: (prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X0)))=eq(cons(s(z),cons(z,X0)),aux(z,X0,s(z),nil,btrue)))),
% 71.93/19.79 inference(paramodulation,[status(thm)],[f247,f165541])).
% 71.93/19.79 fof(f165770,plain,(
% 71.93/19.79 ![X0]: (prop_merge_comm(nil,cons(s(z),nil),cons(s(z),cons(z,X0)))=bfalse)),
% 71.93/19.79 inference(forward_demodulation,[status(thm)],[f472,f165699])).
% 71.93/19.79 fof(f167176,plain,(
% 71.93/19.79 ~eq3(bfalse,bfalse)=btrue),
% 71.93/19.79 inference(paramodulation,[status(thm)],[f165770,f50])).
% 71.93/19.79 fof(f167216,plain,(
% 71.93/19.79 ~btrue=btrue),
% 71.93/19.79 inference(forward_demodulation,[status(thm)],[f43,f167176])).
% 71.93/19.79 fof(f167217,plain,(
% 71.93/19.79 $false),
% 71.93/19.79 inference(trivial_equality_resolution,[status(thm)],[f167216])).
% 71.93/19.79 % SZS output end CNFRefutation for theBenchmark.p
% 25.67/19.88 % Elapsed time: 14.502500 seconds
% 25.67/19.88 % CPU time: 114.444117 seconds
% 25.67/19.88 % Total memory used: 1.593 GB
% 25.67/19.88 % Net memory used: 1.577 GB
%------------------------------------------------------------------------------