%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU382+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:29 PM UTC 2026
% Result : Theorem 8.95s 2.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU382+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n012.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 06:17:22 UTC 2026
% 0.11/0.35 % CPUTime :
% 0.11/0.45 % Drodi V4.1.1
% 8.95/2.03 % Refutation found
% 8.95/2.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.95/2.03 % SZS output start CNFRefutation for theBenchmark
% 8.95/2.03 fof(f534,axiom,(
% 8.95/2.03 (! [A] : k1_pcomps_1(A) = powerset(A) )),
% 8.95/2.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.95/2.03 fof(f672,lemma,(
% 8.95/2.03 (! [A] :( the_carrier(incl_POSet(A)) = A& the_InternalRel(incl_POSet(A)) = inclusion_order(A) ) )),
% 8.95/2.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.95/2.03 fof(f777,conjecture,(
% 8.95/2.03 (! [A] : the_carrier(boole_POSet(A)) = powerset(A) )),
% 8.95/2.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.95/2.03 fof(f778,negated_conjecture,(
% 8.95/2.03 ~((! [A] : the_carrier(boole_POSet(A)) = powerset(A) ))),
% 8.95/2.03 inference(negated_conjecture,[status(cth)],[f777])).
% 8.95/2.03 fof(f781,lemma,(
% 8.95/2.03 (! [A] : boole_POSet(A) = incl_POSet(powerset(A)) )),
% 8.95/2.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.95/2.03 fof(f3435,plain,(
% 8.95/2.03 ![X0]: (k1_pcomps_1(X0)=powerset(X0))),
% 8.95/2.03 inference(cnf_transformation,[status(thm)],[f534])).
% 8.95/2.03 fof(f4234,plain,(
% 8.95/2.03 (![A]: the_carrier(incl_POSet(A))=A)&(![A]: the_InternalRel(incl_POSet(A))=inclusion_order(A))),
% 8.95/2.03 inference(miniscoping,[status(thm)],[f672])).
% 8.95/2.03 fof(f4235,plain,(
% 8.95/2.03 ![X0]: (the_carrier(incl_POSet(X0))=X0)),
% 8.95/2.03 inference(cnf_transformation,[status(thm)],[f4234])).
% 8.95/2.03 fof(f4584,plain,(
% 8.95/2.03 (?[A]: ~the_carrier(boole_POSet(A))=powerset(A))),
% 8.95/2.03 inference(pre_NNF_transformation,[status(thm)],[f778])).
% 8.95/2.03 fof(f4585,plain,(
% 8.95/2.03 ~the_carrier(boole_POSet(sK463_skl))=powerset(sK463_skl)),
% 8.95/2.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK463_skl]),skolemize(A,sK463_skl)],[f4584])).
% 8.95/2.03 fof(f4586,plain,(
% 8.95/2.03 ~the_carrier(boole_POSet(sK463_skl))=powerset(sK463_skl)),
% 8.95/2.03 inference(cnf_transformation,[status(thm)],[f4585])).
% 8.95/2.03 fof(f4594,plain,(
% 8.95/2.03 ![X0]: (boole_POSet(X0)=incl_POSet(powerset(X0)))),
% 8.95/2.03 inference(cnf_transformation,[status(thm)],[f781])).
% 8.95/2.03 fof(f7595,plain,(
% 8.95/2.03 ~the_carrier(boole_POSet(sK463_skl))=k1_pcomps_1(sK463_skl)),
% 8.95/2.03 inference(backward_demodulation,[status(thm)],[f3435,f4586])).
% 8.95/2.03 fof(f11116,plain,(
% 8.95/2.03 ![X0]: (boole_POSet(X0)=incl_POSet(k1_pcomps_1(X0)))),
% 8.95/2.03 inference(forward_demodulation,[status(thm)],[f3435,f4594])).
% 8.95/2.03 fof(f11122,plain,(
% 8.95/2.03 ![X0]: (the_carrier(boole_POSet(X0))=k1_pcomps_1(X0))),
% 8.95/2.03 inference(paramodulation,[status(thm)],[f11116,f4235])).
% 8.95/2.03 fof(f20008,plain,(
% 8.95/2.03 ~k1_pcomps_1(sK463_skl)=k1_pcomps_1(sK463_skl)),
% 8.95/2.03 inference(backward_demodulation,[status(thm)],[f11122,f7595])).
% 8.95/2.03 fof(f20109,plain,(
% 8.95/2.03 $false),
% 8.95/2.03 inference(trivial_equality_resolution,[status(thm)],[f20008])).
% 8.95/2.03 % SZS output end CNFRefutation for theBenchmark.p
% 8.95/2.04 % Elapsed time: 1.667661 seconds
% 8.95/2.04 % CPU time: 12.352018 seconds
% 8.95/2.04 % Total memory used: 351.247 MB
% 8.95/2.04 % Net memory used: 340.781 MB
%------------------------------------------------------------------------------