%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN386+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:19:32 PM UTC 2026
% Result : Theorem 0.14s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN386+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n011.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 10:52:42 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.40 fof(f1,conjecture,(
% 0.14/0.40 ( ( (! [X] :(? [Y] : big_f(X,Y)))& (? [X] :(! [E] :(? [N] :(! [W] :( big_s(N,W)=> big_d(W,X,E) )))))& (! [E] :(? [D] :(! [A,B] :( big_d(A,B,D)=> (! [Y,Z] :( ( big_f(A,Y)& big_f(B,Z) )=> big_d(Y,Z,E) ) )) ))))=> (? [Y] :(! [E] :(? [M] :(! [W] :( big_s(M,W)=> (! [Z] :( big_f(W,Z)=> big_d(Z,Y,E) ) )) ))))) ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f2,negated_conjecture,(
% 0.14/0.40 ~(( ( (! [X] :(? [Y] : big_f(X,Y)))& (? [X] :(! [E] :(? [N] :(! [W] :( big_s(N,W)=> big_d(W,X,E) )))))& (! [E] :(? [D] :(! [A,B] :( big_d(A,B,D)=> (! [Y,Z] :( ( big_f(A,Y)& big_f(B,Z) )=> big_d(Y,Z,E) ) )) ))))=> (? [Y] :(! [E] :(? [M] :(! [W] :( big_s(M,W)=> (! [Z] :( big_f(W,Z)=> big_d(Z,Y,E) ) )) ))))) )),
% 0.14/0.40 inference(negated_conjecture,[status(cth)],[f1])).
% 0.14/0.40 fof(f3,plain,(
% 0.14/0.40 ((((![X]: ?[Y]: big_f(X,Y))&(?[X]: ![E]: ?[N]: ![W]: (~big_s(N,W)|big_d(W,X,E))))&(![E]: ?[D]: ![A,B]: (~big_d(A,B,D)|(![Y,Z]: ((~big_f(A,Y)|~big_f(B,Z))|big_d(Y,Z,E))))))&(![Y]: ?[E]: ![M]: ?[W]: (big_s(M,W)&(?[Z]: (big_f(W,Z)&~big_d(Z,Y,E))))))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.14/0.40 fof(f4,plain,(
% 0.14/0.40 (((![X]: big_f(X,sK0_skl(X)))&![E]: ![W]: (~big_s(sK2_skl(E),W)|big_d(W,sK1_skl,E)))&(![E]: ![A,B]: (~big_d(A,B,sK3_skl(E))|(![Y,Z]: ((~big_f(A,Y)|~big_f(B,Z))|big_d(Y,Z,E))))))&(![Y]: ![M]: (big_s(M,sK5_skl(M,Y))&(big_f(sK5_skl(M,Y),sK6_skl(M,Y))&~big_d(sK6_skl(M,Y),Y,sK4_skl(Y)))))),
% 0.14/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl]),skolemize(Y,sK0_skl(X)),skolemize(X,sK1_skl),skolemize(N,sK2_skl(E)),skolemize(D,sK3_skl(E)),skolemize(E,sK4_skl(Y)),skolemize(W,sK5_skl(M,Y)),skolemize(Z,sK6_skl(M,Y))],[f3])).
% 0.14/0.40 fof(f5,plain,(
% 0.14/0.40 ![X0]: (big_f(X0,sK0_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.40 fof(f6,plain,(
% 0.14/0.40 ![X0,X1]: (~big_s(sK2_skl(X0),X1)|big_d(X1,sK1_skl,X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.40 fof(f7,plain,(
% 0.14/0.40 ![X0,X1,X2,X3,X4]: (~big_d(X0,X1,sK3_skl(X2))|~big_f(X0,X3)|~big_f(X1,X4)|big_d(X3,X4,X2))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.40 fof(f8,plain,(
% 0.14/0.40 ![X0,X1]: (big_s(X0,sK5_skl(X0,X1)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.40 fof(f9,plain,(
% 0.14/0.40 ![X0,X1]: (big_f(sK5_skl(X0,X1),sK6_skl(X0,X1)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.40 fof(f10,plain,(
% 0.14/0.40 ![X0,X1]: (~big_d(sK6_skl(X0,X1),X1,sK4_skl(X1)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.40 fof(f11,plain,(
% 0.14/0.40 ![X0,X1]: (big_d(sK5_skl(sK2_skl(X0),X1),sK1_skl,X0))),
% 0.14/0.40 inference(resolution,[status(thm)],[f8,f6])).
% 0.14/0.40 fof(f12,plain,(
% 0.14/0.40 ![X0,X1,X2,X3]: (~big_f(sK5_skl(sK2_skl(sK3_skl(X0)),X1),X2)|~big_f(sK1_skl,X3)|big_d(X2,X3,X0))),
% 0.14/0.40 inference(resolution,[status(thm)],[f11,f7])).
% 0.14/0.40 fof(f13,plain,(
% 0.14/0.40 ![X0,X1,X2]: (~big_f(sK1_skl,X0)|big_d(sK6_skl(sK2_skl(sK3_skl(X1)),X2),X0,X1))),
% 0.14/0.40 inference(resolution,[status(thm)],[f12,f9])).
% 0.14/0.40 fof(f15,plain,(
% 0.14/0.40 ![X0,X1]: (big_d(sK6_skl(sK2_skl(sK3_skl(X0)),X1),sK0_skl(sK1_skl),X0))),
% 0.14/0.40 inference(resolution,[status(thm)],[f13,f5])).
% 0.14/0.40 fof(f16,plain,(
% 0.14/0.40 $false),
% 0.14/0.40 inference(resolution,[status(thm)],[f15,f10])).
% 0.14/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.44 % Elapsed time: 0.051963 seconds
% 0.14/0.44 % CPU time: 0.146044 seconds
% 0.14/0.44 % Total memory used: 55.506 MB
% 0.14/0.44 % Net memory used: 54.897 MB
%------------------------------------------------------------------------------