%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU444+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:43 PM UTC 2026
% Result : Theorem 72.85s 24.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU444+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n009.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Mon Sep 21 06:33:26 UTC 2026
% 0.20/0.46 % CPUTime :
% 17.54/17.87 % Drodi V4.1.1
% 72.85/24.95 % Refutation found
% 72.85/24.95 % SZS status Theorem for theBenchmark: Theorem is valid
% 72.85/24.95 % SZS output start CNFRefutation for theBenchmark
% 72.85/24.95 fof(f1461,axiom,(
% 72.85/24.95 (! [A,B,C] :( m2_relset_1(C,A,B)=> ( k10_relset_1(A,B,C,A) = k5_relset_1(A,B,C)& k11_relset_1(A,B,C,B) = k4_relset_1(A,B,C) ) ) )),
% 72.85/24.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.85/24.95 fof(f71133,axiom,(
% 72.85/24.95 (! [A,B,C] :( m2_relset_1(C,B,A)=> ( k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A)& k2_funct_5(C) = k10_relset_1(B,A,C,B) ) ) )),
% 72.85/24.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.85/24.95 fof(f71138,conjecture,(
% 72.85/24.95 (! [A,B,C] :( m2_relset_1(C,B,A)=> ( k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A)& k10_relset_1(A,B,k6_relset_1(B,A,C),k10_relset_1(B,A,C,B)) = k10_relset_1(A,B,k6_relset_1(B,A,C),k2_funct_5(C)) ) ) )),
% 72.85/24.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.85/24.95 fof(f71139,negated_conjecture,(
% 72.85/24.95 ~((! [A,B,C] :( m2_relset_1(C,B,A)=> ( k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A)& k10_relset_1(A,B,k6_relset_1(B,A,C),k10_relset_1(B,A,C,B)) = k10_relset_1(A,B,k6_relset_1(B,A,C),k2_funct_5(C)) ) ) ))),
% 72.85/24.95 inference(negated_conjecture,[status(cth)],[f71138])).
% 72.85/24.95 fof(f74713,plain,(
% 72.85/24.95 ![A,B,C]: (~m2_relset_1(C,A,B)|(k10_relset_1(A,B,C,A)=k5_relset_1(A,B,C)&k11_relset_1(A,B,C,B)=k4_relset_1(A,B,C)))),
% 72.85/24.95 inference(pre_NNF_transformation,[status(thm)],[f1461])).
% 72.85/24.95 fof(f74714,plain,(
% 72.85/24.95 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|k10_relset_1(X1,X2,X0,X1)=k5_relset_1(X1,X2,X0))),
% 72.85/24.95 inference(cnf_transformation,[status(thm)],[f74713])).
% 72.85/24.95 fof(f336135,plain,(
% 72.85/24.95 ![A,B,C]: (~m2_relset_1(C,B,A)|(k1_funct_5(C)=k10_relset_1(A,B,k6_relset_1(B,A,C),A)&k2_funct_5(C)=k10_relset_1(B,A,C,B)))),
% 72.85/24.95 inference(pre_NNF_transformation,[status(thm)],[f71133])).
% 72.85/24.95 fof(f336136,plain,(
% 72.85/24.95 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|k1_funct_5(X0)=k10_relset_1(X2,X1,k6_relset_1(X1,X2,X0),X2))),
% 72.85/24.95 inference(cnf_transformation,[status(thm)],[f336135])).
% 72.85/24.95 fof(f336137,plain,(
% 72.85/24.95 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|k2_funct_5(X0)=k10_relset_1(X1,X2,X0,X1))),
% 72.85/24.95 inference(cnf_transformation,[status(thm)],[f336135])).
% 72.85/24.95 fof(f336156,plain,(
% 72.85/24.95 (?[A,B,C]: (m2_relset_1(C,B,A)&(~k1_funct_5(C)=k10_relset_1(A,B,k6_relset_1(B,A,C),A)|~k10_relset_1(A,B,k6_relset_1(B,A,C),k10_relset_1(B,A,C,B))=k10_relset_1(A,B,k6_relset_1(B,A,C),k2_funct_5(C)))))),
% 72.85/24.95 inference(pre_NNF_transformation,[status(thm)],[f71139])).
% 72.85/24.95 fof(f336157,plain,(
% 72.85/24.95 (m2_relset_1(sK23843_skl,sK23842_skl,sK23841_skl)&(~k1_funct_5(sK23843_skl)=k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),sK23841_skl)|~k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),k10_relset_1(sK23842_skl,sK23841_skl,sK23843_skl,sK23842_skl))=k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),k2_funct_5(sK23843_skl))))),
% 72.85/24.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK23841_skl,sK23842_skl,sK23843_skl]),skolemize(A,sK23841_skl),skolemize(B,sK23842_skl),skolemize(C,sK23843_skl)],[f336156])).
% 72.85/24.95 fof(f336158,plain,(
% 72.85/24.95 m2_relset_1(sK23843_skl,sK23842_skl,sK23841_skl)),
% 72.85/24.95 inference(cnf_transformation,[status(thm)],[f336157])).
% 72.85/24.95 fof(f336159,plain,(
% 72.85/24.95 ~k1_funct_5(sK23843_skl)=k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),sK23841_skl)|~k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),k10_relset_1(sK23842_skl,sK23841_skl,sK23843_skl,sK23842_skl))=k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),k2_funct_5(sK23843_skl))),
% 72.85/24.95 inference(cnf_transformation,[status(thm)],[f336157])).
% 72.85/24.95 fof(f371073,plain,(
% 72.85/24.95 k10_relset_1(sK23842_skl,sK23841_skl,sK23843_skl,sK23842_skl)=k5_relset_1(sK23842_skl,sK23841_skl,sK23843_skl)),
% 72.85/24.95 inference(resolution,[status(thm)],[f74714,f336158])).
% 72.85/24.95 fof(f371102,plain,(
% 72.85/24.95 ~k1_funct_5(sK23843_skl)=k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),sK23841_skl)|~k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),k5_relset_1(sK23842_skl,sK23841_skl,sK23843_skl))=k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),k2_funct_5(sK23843_skl))),
% 69.50/26.76 inference(backward_demodulation,[status(thm)],[f371073,f336159])).
% 69.50/26.76 fof(f373652,plain,(
% 69.50/26.76 k1_funct_5(sK23843_skl)=k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),sK23841_skl)),
% 69.50/26.76 inference(resolution,[status(thm)],[f336136,f336158])).
% 69.50/26.76 fof(f373653,plain,(
% 69.50/26.76 k2_funct_5(sK23843_skl)=k10_relset_1(sK23842_skl,sK23841_skl,sK23843_skl,sK23842_skl)),
% 69.50/26.76 inference(resolution,[status(thm)],[f336137,f336158])).
% 69.50/26.76 fof(f373883,plain,(
% 69.50/26.76 k2_funct_5(sK23843_skl)=k5_relset_1(sK23842_skl,sK23841_skl,sK23843_skl)),
% 69.50/26.76 inference(backward_demodulation,[status(thm)],[f373653,f371073])).
% 69.50/26.76 fof(f373884,plain,(
% 69.50/26.76 ~k1_funct_5(sK23843_skl)=k1_funct_5(sK23843_skl)|~k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),k5_relset_1(sK23842_skl,sK23841_skl,sK23843_skl))=k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),k2_funct_5(sK23843_skl))),
% 69.50/26.76 inference(backward_demodulation,[status(thm)],[f373652,f371102])).
% 69.50/26.76 fof(f373885,plain,(
% 69.50/26.76 ~k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),k5_relset_1(sK23842_skl,sK23841_skl,sK23843_skl))=k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),k2_funct_5(sK23843_skl))),
% 69.50/26.76 inference(trivial_equality_resolution,[status(thm)],[f373884])).
% 69.50/26.76 fof(f373987,plain,(
% 69.50/26.76 ~k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),k2_funct_5(sK23843_skl))=k10_relset_1(sK23841_skl,sK23842_skl,k6_relset_1(sK23842_skl,sK23841_skl,sK23843_skl),k2_funct_5(sK23843_skl))),
% 69.50/26.76 inference(backward_demodulation,[status(thm)],[f373883,f373885])).
% 69.50/26.76 fof(f373990,plain,(
% 69.50/26.76 $false),
% 69.50/26.76 inference(trivial_equality_resolution,[status(thm)],[f373987])).
% 69.50/26.76 % SZS output end CNFRefutation for theBenchmark.p
% 19.57/27.47 % Elapsed time: 26.018832 seconds
% 19.57/27.47 % CPU time: 75.461628 seconds
% 19.57/27.47 % Total memory used: 21.725 GB
% 19.57/27.47 % Net memory used: 21.581 GB
%------------------------------------------------------------------------------