%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEV664+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:33:50 PM UTC 2026
% Result : Theorem 0.66s 1.05s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEV664+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n007.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 07:32:35 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.57/0.88 % Drodi V4.1.1
% 0.66/1.05 % Refutation found
% 0.66/1.05 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.66/1.05 % SZS output start CNFRefutation for theBenchmark
% 0.66/1.05 fof(f2539,conjecture,(
% 0.66/1.05 (! [V0__P] :( cProp___24t(V0__P)=> (! [V1__Q] :( cProp___24t(V1__Q)=> ( V0__P = V1__Q=> ( p(V0__P)=> p(V1__Q) ) ) ) )) )),
% 0.66/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.66/1.05 fof(f2540,negated_conjecture,(
% 0.66/1.05 ~((! [V0__P] :( cProp___24t(V0__P)=> (! [V1__Q] :( cProp___24t(V1__Q)=> ( V0__P = V1__Q=> ( p(V0__P)=> p(V1__Q) ) ) ) )) ))),
% 0.66/1.05 inference(negated_conjecture,[status(cth)],[f2539])).
% 0.66/1.05 fof(f11253,plain,(
% 0.66/1.05 (?[V0__P]: (cProp___24t(V0__P)&(?[V1__Q]: (cProp___24t(V1__Q)&(V0__P=V1__Q&(p(V0__P)&~p(V1__Q)))))))),
% 0.66/1.05 inference(pre_NNF_transformation,[status(thm)],[f2540])).
% 0.66/1.05 fof(f11254,plain,(
% 0.66/1.05 (cProp___24t(sK1034_skl)&(cProp___24t(sK1035_skl)&(sK1034_skl=sK1035_skl&(p(sK1034_skl)&~p(sK1035_skl)))))),
% 0.66/1.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK1034_skl,sK1035_skl]),skolemize(V0__P,sK1034_skl),skolemize(V1__Q,sK1035_skl)],[f11253])).
% 0.66/1.05 fof(f11257,plain,(
% 0.66/1.05 sK1034_skl=sK1035_skl),
% 0.66/1.05 inference(cnf_transformation,[status(thm)],[f11254])).
% 0.66/1.05 fof(f11258,plain,(
% 0.66/1.05 p(sK1034_skl)),
% 0.66/1.05 inference(cnf_transformation,[status(thm)],[f11254])).
% 0.66/1.05 fof(f11259,plain,(
% 0.66/1.05 ~p(sK1035_skl)),
% 0.66/1.05 inference(cnf_transformation,[status(thm)],[f11254])).
% 0.66/1.05 fof(f13883,plain,(
% 0.66/1.05 ~p(sK1034_skl)),
% 0.66/1.05 inference(forward_demodulation,[status(thm)],[f11257,f11259])).
% 0.66/1.05 fof(f13884,plain,(
% 0.66/1.05 $false),
% 0.66/1.05 inference(forward_subsumption_resolution,[status(thm)],[f13883,f11258])).
% 0.66/1.05 % SZS output end CNFRefutation for theBenchmark.p
% 0.66/1.12 % Elapsed time: 0.674819 seconds
% 0.66/1.12 % CPU time: 1.495497 seconds
% 0.66/1.12 % Total memory used: 467.615 MB
% 0.66/1.12 % Net memory used: 464.227 MB
%------------------------------------------------------------------------------