%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU229+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 02:22:04 PM UTC 2026
% Result : Theorem 19.18s 2.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU229+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n015.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 06:04:05 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 19.18/2.91 % Refutation found
% 19.18/2.91 % SZS status Theorem for theBenchmark: Theorem is valid
% 19.18/2.91 % SZS output start CNFRefutation for theBenchmark
% 19.18/2.91 fof(f5,axiom,(
% 19.18/2.91 (! [A,B,C,D] :( D = unordered_triple(A,B,C)<=> (! [E] :( in(E,D)<=> ~ ( E != A& E != B& E != C ) ) )) )),
% 19.18/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.18/2.91 fof(f9,axiom,(
% 19.18/2.91 (! [A] :(? [B] : element(B,A) ))),
% 19.18/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.18/2.91 fof(f23,axiom,(
% 19.18/2.91 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 19.18/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.18/2.91 fof(f24,conjecture,(
% 19.18/2.91 (! [A,B,C] :~ ( in(A,B)& in(B,C)& in(C,A) ) )),
% 19.18/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.18/2.91 fof(f25,negated_conjecture,(
% 19.18/2.91 ~((! [A,B,C] :~ ( in(A,B)& in(B,C)& in(C,A) ) ))),
% 19.18/2.91 inference(negated_conjecture,[status(cth)],[f24])).
% 19.18/2.91 fof(f27,axiom,(
% 19.18/2.91 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 19.18/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.18/2.91 fof(f28,axiom,(
% 19.18/2.91 (! [A,B] :~ ( in(A,B)& (! [C] :~ ( in(C,B)& (! [D] :~ ( in(D,B)& in(D,C) ) )) )) )),
% 19.18/2.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.18/2.91 fof(f40,plain,(
% 19.18/2.91 ![A,B,C,D]: (D=unordered_triple(A,B,C)<=>(![E]: (in(E,D)<=>((E=A|E=B)|E=C))))),
% 19.18/2.91 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 19.18/2.91 fof(f41,definition,(
% 19.18/2.91 ![A,B,C,E]: (sP0_prd(E,C,B,A)<=>((E=A|E=B)|E=C))),
% 19.18/2.91 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 19.18/2.91 fof(f42,plain,(
% 19.18/2.91 ![A,B,C,D]: (D=unordered_triple(A,B,C)<=>(![E]: (in(E,D)<=>sP0_prd(E,C,B,A))))),
% 19.18/2.91 inference(formula_renaming,[status(thm)],[f40,f41])).
% 19.18/2.91 fof(f43,plain,(
% 19.18/2.91 ![A,B,C,D]: ((~D=unordered_triple(A,B,C)|(![E]: ((~in(E,D)|sP0_prd(E,C,B,A))&(in(E,D)|~sP0_prd(E,C,B,A)))))&(D=unordered_triple(A,B,C)|(?[E]: ((~in(E,D)|~sP0_prd(E,C,B,A))&(in(E,D)|sP0_prd(E,C,B,A))))))),
% 19.18/2.91 inference(NNF_transformation,[status(thm)],[f42])).
% 19.18/2.91 fof(f44,plain,(
% 19.18/2.91 (![A,B,C,D]: (~D=unordered_triple(A,B,C)|((![E]: (~in(E,D)|sP0_prd(E,C,B,A)))&(![E]: (in(E,D)|~sP0_prd(E,C,B,A))))))&(![A,B,C,D]: (D=unordered_triple(A,B,C)|(?[E]: ((~in(E,D)|~sP0_prd(E,C,B,A))&(in(E,D)|sP0_prd(E,C,B,A))))))),
% 19.18/2.91 inference(miniscoping,[status(thm)],[f43])).
% 19.18/2.91 fof(f45,plain,(
% 19.18/2.91 (![A,B,C,D]: (~D=unordered_triple(A,B,C)|((![E]: (~in(E,D)|sP0_prd(E,C,B,A)))&(![E]: (in(E,D)|~sP0_prd(E,C,B,A))))))&(![A,B,C,D]: (D=unordered_triple(A,B,C)|((~in(sK0_skl(D,C,B,A),D)|~sP0_prd(sK0_skl(D,C,B,A),C,B,A))&(in(sK0_skl(D,C,B,A),D)|sP0_prd(sK0_skl(D,C,B,A),C,B,A)))))),
% 19.18/2.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(E,sK0_skl(D,C,B,A))],[f44])).
% 19.18/2.91 fof(f46,plain,(
% 19.18/2.91 ![X0,X1,X2,X3,X4]: (~X0=unordered_triple(X1,X2,X3)|~in(X4,X0)|sP0_prd(X4,X3,X2,X1))),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f45])).
% 19.18/2.91 fof(f47,plain,(
% 19.18/2.91 ![X0,X1,X2,X3,X4]: (~X0=unordered_triple(X1,X2,X3)|in(X4,X0)|~sP0_prd(X4,X3,X2,X1))),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f45])).
% 19.18/2.91 fof(f50,plain,(
% 19.18/2.91 ![A]: element(sK1_skl(A),A)),
% 19.18/2.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f9])).
% 19.18/2.91 fof(f51,plain,(
% 19.18/2.91 ![X0]: (element(sK1_skl(X0),X0))),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f50])).
% 19.18/2.91 fof(f88,plain,(
% 19.18/2.91 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 19.18/2.91 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 19.18/2.91 fof(f89,plain,(
% 19.18/2.91 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f88])).
% 19.18/2.91 fof(f90,plain,(
% 19.18/2.91 (?[A,B,C]: ((in(A,B)&in(B,C))&in(C,A)))),
% 19.18/2.91 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 19.18/2.91 fof(f91,plain,(
% 19.18/2.91 ?[A,C]: ((?[B]: (in(A,B)&in(B,C)))&in(C,A))),
% 19.18/2.91 inference(miniscoping,[status(thm)],[f90])).
% 19.18/2.91 fof(f92,plain,(
% 19.18/2.91 ((in(sK11_skl,sK13_skl)&in(sK13_skl,sK12_skl))&in(sK12_skl,sK11_skl))),
% 19.18/2.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl]),skolemize(A,sK11_skl),skolemize(C,sK12_skl),skolemize(B,sK13_skl)],[f91])).
% 19.18/2.91 fof(f93,plain,(
% 19.18/2.91 in(sK11_skl,sK13_skl)),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f92])).
% 19.18/2.91 fof(f94,plain,(
% 19.18/2.91 in(sK13_skl,sK12_skl)),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f92])).
% 19.18/2.91 fof(f95,plain,(
% 19.18/2.91 in(sK12_skl,sK11_skl)),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f92])).
% 19.18/2.91 fof(f98,plain,(
% 19.18/2.91 ![A,B]: (~in(A,B)|~empty(B))),
% 19.18/2.91 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 19.18/2.91 fof(f99,plain,(
% 19.18/2.91 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 19.18/2.91 inference(miniscoping,[status(thm)],[f98])).
% 19.18/2.91 fof(f100,plain,(
% 19.18/2.91 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f99])).
% 19.18/2.91 fof(f101,plain,(
% 19.18/2.91 ![A,B]: (~in(A,B)|(?[C]: (in(C,B)&(![D]: (~in(D,B)|~in(D,C))))))),
% 19.18/2.91 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 19.18/2.91 fof(f102,plain,(
% 19.18/2.91 ![B]: ((![A]: ~in(A,B))|(?[C]: (in(C,B)&(![D]: (~in(D,B)|~in(D,C))))))),
% 19.18/2.91 inference(miniscoping,[status(thm)],[f101])).
% 19.18/2.91 fof(f103,plain,(
% 19.18/2.91 ![B]: ((![A]: ~in(A,B))|(in(sK14_skl(B),B)&(![D]: (~in(D,B)|~in(D,sK14_skl(B))))))),
% 19.18/2.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(C,sK14_skl(B))],[f102])).
% 19.18/2.91 fof(f104,plain,(
% 19.18/2.91 ![X0,X1]: (~in(X0,X1)|in(sK14_skl(X1),X1))),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f103])).
% 19.18/2.91 fof(f105,plain,(
% 19.18/2.91 ![X0,X1,X2]: (~in(X0,X1)|~in(X2,X1)|~in(X2,sK14_skl(X1)))),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f103])).
% 19.18/2.91 fof(f109,plain,(
% 19.18/2.91 ![A,B,C,E]: ((~sP0_prd(E,C,B,A)|((E=A|E=B)|E=C))&(sP0_prd(E,C,B,A)|((~E=A&~E=B)&~E=C)))),
% 19.18/2.91 inference(NNF_transformation,[status(thm)],[f41])).
% 19.18/2.91 fof(f110,plain,(
% 19.18/2.91 (![A,B,C,E]: (~sP0_prd(E,C,B,A)|((E=A|E=B)|E=C)))&(![A,B,C,E]: (sP0_prd(E,C,B,A)|((~E=A&~E=B)&~E=C)))),
% 19.18/2.91 inference(miniscoping,[status(thm)],[f109])).
% 19.18/2.91 fof(f111,plain,(
% 19.18/2.91 ![X0,X1,X2,X3]: (~sP0_prd(X0,X1,X2,X3)|X0=X3|X0=X2|X0=X1)),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f110])).
% 19.18/2.91 fof(f112,plain,(
% 19.18/2.91 ![X0,X1,X2,X3]: (sP0_prd(X0,X1,X2,X3)|~X0=X3)),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f110])).
% 19.18/2.91 fof(f113,plain,(
% 19.18/2.91 ![X0,X1,X2,X3]: (sP0_prd(X0,X1,X2,X3)|~X0=X2)),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f110])).
% 19.18/2.91 fof(f114,plain,(
% 19.18/2.91 ![X0,X1,X2,X3]: (sP0_prd(X0,X1,X2,X3)|~X0=X1)),
% 19.18/2.91 inference(cnf_transformation,[status(thm)],[f110])).
% 19.18/2.91 fof(f115,plain,(
% 19.18/2.91 ![X0,X1,X2,X3]: (~in(X0,unordered_triple(X1,X2,X3))|sP0_prd(X0,X3,X2,X1))),
% 19.18/2.91 inference(destructive_equality_resolution,[status(thm)],[f46])).
% 19.18/2.91 fof(f116,plain,(
% 19.18/2.91 ![X0,X1,X2,X3]: (in(X0,unordered_triple(X1,X2,X3))|~sP0_prd(X0,X3,X2,X1))),
% 19.18/2.91 inference(destructive_equality_resolution,[status(thm)],[f47])).
% 19.18/2.91 fof(f117,plain,(
% 19.18/2.91 ![X0,X1,X2]: (sP0_prd(X0,X1,X2,X0))),
% 19.18/2.91 inference(destructive_equality_resolution,[status(thm)],[f112])).
% 19.18/2.91 fof(f118,plain,(
% 19.18/2.91 ![X0,X1,X2]: (sP0_prd(X0,X1,X0,X2))),
% 19.18/2.91 inference(destructive_equality_resolution,[status(thm)],[f113])).
% 19.18/2.91 fof(f119,plain,(
% 19.18/2.91 ![X0,X1,X2]: (sP0_prd(X0,X0,X1,X2))),
% 19.18/2.91 inference(destructive_equality_resolution,[status(thm)],[f114])).
% 19.18/2.91 fof(f159,plain,(
% 19.18/2.91 ![X0,X1,X2]: (in(X0,unordered_triple(X0,X1,X2)))),
% 19.18/2.91 inference(resolution,[status(thm)],[f117,f116])).
% 19.18/2.91 fof(f160,plain,(
% 19.18/2.91 ![X0,X1,X2]: (in(X0,unordered_triple(X1,X0,X2)))),
% 19.18/2.91 inference(resolution,[status(thm)],[f118,f116])).
% 19.18/2.91 fof(f161,plain,(
% 19.18/2.91 ![X0,X1,X2]: (in(X0,unordered_triple(X1,X2,X0)))),
% 19.18/2.91 inference(resolution,[status(thm)],[f119,f116])).
% 19.18/2.91 fof(f174,plain,(
% 19.18/2.91 ![X0,X1,X2]: (~empty(unordered_triple(X0,X1,X2)))),
% 19.18/2.91 inference(resolution,[status(thm)],[f159,f100])).
% 19.18/2.91 fof(f178,plain,(
% 19.18/2.91 ![X0]: (empty(X0)|in(sK1_skl(X0),X0))),
% 19.18/2.91 inference(resolution,[status(thm)],[f89,f51])).
% 19.18/2.91 fof(f231,plain,(
% 19.18/2.91 ![X0,X1,X2]: (empty(unordered_triple(X0,X1,X2))|sP0_prd(sK1_skl(unordered_triple(X0,X1,X2)),X2,X1,X0))),
% 19.18/2.91 inference(resolution,[status(thm)],[f178,f115])).
% 19.18/2.91 fof(f232,plain,(
% 19.18/2.91 ![X0]: (empty(X0)|in(sK14_skl(X0),X0))),
% 19.18/2.91 inference(resolution,[status(thm)],[f178,f104])).
% 19.18/2.91 fof(f236,plain,(
% 19.18/2.91 ![X0,X1,X2]: (sP0_prd(sK1_skl(unordered_triple(X0,X1,X2)),X2,X1,X0))),
% 19.18/2.91 inference(forward_subsumption_resolution,[status(thm)],[f231,f174])).
% 19.18/2.91 fof(f238,plain,(
% 19.18/2.91 ![X0,X1,X2]: (empty(unordered_triple(X0,X1,X2))|sP0_prd(sK14_skl(unordered_triple(X0,X1,X2)),X2,X1,X0))),
% 19.18/2.91 inference(resolution,[status(thm)],[f232,f115])).
% 19.18/2.91 fof(f243,plain,(
% 19.18/2.91 ![X0,X1,X2]: (sP0_prd(sK14_skl(unordered_triple(X0,X1,X2)),X2,X1,X0))),
% 19.18/2.91 inference(forward_subsumption_resolution,[status(thm)],[f238,f174])).
% 19.18/2.91 fof(f252,plain,(
% 19.18/2.91 ![X0,X1,X2]: (in(sK1_skl(unordered_triple(X0,X1,X2)),unordered_triple(X0,X1,X2)))),
% 19.18/2.93 inference(resolution,[status(thm)],[f236,f116])).
% 19.18/2.93 fof(f253,plain,(
% 19.18/2.93 ![X0,X1,X2]: (sK14_skl(unordered_triple(X0,X1,X2))=X0|sK14_skl(unordered_triple(X0,X1,X2))=X1|sK14_skl(unordered_triple(X0,X1,X2))=X2)),
% 19.18/2.93 inference(resolution,[status(thm)],[f243,f111])).
% 19.18/2.93 fof(f360,plain,(
% 19.18/2.93 ![X0,X1,X2,X3,X4]: (~in(X0,unordered_triple(X1,X2,X3))|~in(X4,unordered_triple(X1,X2,X3))|~in(X4,X1)|sK14_skl(unordered_triple(X1,X2,X3))=X2|sK14_skl(unordered_triple(X1,X2,X3))=X3)),
% 19.18/2.93 inference(paramodulation,[status(thm)],[f253,f105])).
% 19.18/2.93 fof(f1055,plain,(
% 19.18/2.93 ![X0,X1,X2,X3]: (~in(X0,unordered_triple(X1,X2,X3))|~in(X3,X1)|sK14_skl(unordered_triple(X1,X2,X3))=X2|sK14_skl(unordered_triple(X1,X2,X3))=X3)),
% 19.18/2.93 inference(resolution,[status(thm)],[f360,f161])).
% 19.18/2.93 fof(f3629,plain,(
% 19.18/2.93 ![X0,X1,X2]: (~in(X0,X1)|sK14_skl(unordered_triple(X1,X2,X0))=X2|sK14_skl(unordered_triple(X1,X2,X0))=X0)),
% 19.18/2.93 inference(resolution,[status(thm)],[f1055,f252])).
% 19.18/2.93 fof(f3731,plain,(
% 19.18/2.93 ![X0]: (sK14_skl(unordered_triple(sK11_skl,X0,sK12_skl))=X0|sK14_skl(unordered_triple(sK11_skl,X0,sK12_skl))=sK12_skl)),
% 19.18/2.93 inference(resolution,[status(thm)],[f3629,f95])).
% 19.18/2.93 fof(f3773,plain,(
% 19.18/2.93 ![X0,X1,X2]: (~in(X0,unordered_triple(sK11_skl,X1,sK12_skl))|~in(X2,unordered_triple(sK11_skl,X1,sK12_skl))|~in(X2,X1)|sK14_skl(unordered_triple(sK11_skl,X1,sK12_skl))=sK12_skl)),
% 19.18/2.93 inference(paramodulation,[status(thm)],[f3731,f105])).
% 19.18/2.93 fof(f9150,plain,(
% 19.18/2.93 ![X0,X1]: (~in(X0,unordered_triple(sK11_skl,X1,sK12_skl))|~in(sK11_skl,X1)|sK14_skl(unordered_triple(sK11_skl,X1,sK12_skl))=sK12_skl)),
% 19.18/2.93 inference(resolution,[status(thm)],[f3773,f159])).
% 19.18/2.93 fof(f9688,plain,(
% 19.18/2.93 ![X0]: (~in(sK11_skl,X0)|sK14_skl(unordered_triple(sK11_skl,X0,sK12_skl))=sK12_skl)),
% 19.18/2.93 inference(resolution,[status(thm)],[f9150,f252])).
% 19.18/2.93 fof(f9714,plain,(
% 19.18/2.93 sK14_skl(unordered_triple(sK11_skl,sK13_skl,sK12_skl))=sK12_skl),
% 19.18/2.93 inference(resolution,[status(thm)],[f9688,f93])).
% 19.18/2.93 fof(f9764,plain,(
% 19.18/2.93 ![X0,X1]: (~in(X0,unordered_triple(sK11_skl,sK13_skl,sK12_skl))|~in(X1,unordered_triple(sK11_skl,sK13_skl,sK12_skl))|~in(X1,sK12_skl))),
% 19.18/2.93 inference(paramodulation,[status(thm)],[f9714,f105])).
% 19.18/2.93 fof(f10379,plain,(
% 19.18/2.93 ![X0]: (~in(X0,unordered_triple(sK11_skl,sK13_skl,sK12_skl))|~in(sK13_skl,sK12_skl))),
% 19.18/2.93 inference(resolution,[status(thm)],[f9764,f160])).
% 19.18/2.93 fof(f10388,plain,(
% 19.18/2.93 ![X0]: (~in(X0,unordered_triple(sK11_skl,sK13_skl,sK12_skl)))),
% 19.18/2.93 inference(forward_subsumption_resolution,[status(thm)],[f10379,f94])).
% 19.18/2.93 fof(f10389,plain,(
% 19.18/2.93 $false),
% 19.18/2.93 inference(resolution,[status(thm)],[f10388,f252])).
% 19.18/2.93 % SZS output end CNFRefutation for theBenchmark.p
% 19.18/2.95 % Elapsed time: 2.502025 seconds
% 19.18/2.95 % CPU time: 19.471385 seconds
% 19.18/2.95 % Total memory used: 223.196 MB
% 19.18/2.95 % Net memory used: 205.698 MB
%------------------------------------------------------------------------------