%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PHI023+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 01:58:10 PM UTC 2026
% Result : Theorem 0.10s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI023+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 03:25:43 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 0.10/0.41 % Refutation found
% 0.10/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.41 fof(f1,axiom,(
% 0.10/0.41 (! [X] :( selfCaused(X)<=> ( essenceInvExistence(X)& natureConcOnlyByExistence(X) ) ) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f3,axiom,(
% 0.10/0.41 (! [X] :( substance(X)<=> ( inItself(X)& conceivedThruItself(X) ) ) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f6,axiom,(
% 0.10/0.41 (! [X] :( god(X)<=> ( being(X)& absolutelyInfinite(X) ) ) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f7,axiom,(
% 0.10/0.41 (! [X,Y] :( absolutelyInfinite(X)<=> ( substance(X)& constInInfAttributes(X)& ( attributeOf(Y,X)=> ( expressesEternalEssentiality(Y)& expressesInfiniteEssentiality(Y) ) ) ) ) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f18,axiom,(
% 0.10/0.41 (! [X] :( inItself(X)=> selfCaused(X) ) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f19,axiom,(
% 0.10/0.41 (! [X] :( being(X)=> hasEssence(X) ) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f20,axiom,(
% 0.10/0.41 (! [X] :( ( essenceInvExistence(X)& hasEssence(X) )=> exists(X) ) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f21,conjecture,(
% 0.10/0.41 (! [X] :( god(X)=> exists(X) ) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f22,negated_conjecture,(
% 0.10/0.41 ~((! [X] :( god(X)=> exists(X) ) ))),
% 0.10/0.41 inference(negated_conjecture,[status(cth)],[f21])).
% 0.10/0.41 fof(f23,plain,(
% 0.10/0.41 ![X]: ((~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X)))&(selfCaused(X)|(~essenceInvExistence(X)|~natureConcOnlyByExistence(X))))),
% 0.10/0.41 inference(NNF_transformation,[status(thm)],[f1])).
% 0.10/0.41 fof(f24,plain,(
% 0.10/0.41 (![X]: (~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X))))&(![X]: (selfCaused(X)|(~essenceInvExistence(X)|~natureConcOnlyByExistence(X))))),
% 0.10/0.41 inference(miniscoping,[status(thm)],[f23])).
% 0.10/0.41 fof(f25,plain,(
% 0.10/0.41 ![X0]: (~selfCaused(X0)|essenceInvExistence(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f24])).
% 0.10/0.41 fof(f33,plain,(
% 0.10/0.41 ![X]: ((~substance(X)|(inItself(X)&conceivedThruItself(X)))&(substance(X)|(~inItself(X)|~conceivedThruItself(X))))),
% 0.10/0.41 inference(NNF_transformation,[status(thm)],[f3])).
% 0.10/0.41 fof(f34,plain,(
% 0.10/0.41 (![X]: (~substance(X)|(inItself(X)&conceivedThruItself(X))))&(![X]: (substance(X)|(~inItself(X)|~conceivedThruItself(X))))),
% 0.10/0.41 inference(miniscoping,[status(thm)],[f33])).
% 0.10/0.41 fof(f35,plain,(
% 0.10/0.41 ![X0]: (~substance(X0)|inItself(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f34])).
% 0.10/0.41 fof(f50,plain,(
% 0.10/0.41 ![X]: ((~god(X)|(being(X)&absolutelyInfinite(X)))&(god(X)|(~being(X)|~absolutelyInfinite(X))))),
% 0.10/0.41 inference(NNF_transformation,[status(thm)],[f6])).
% 0.10/0.41 fof(f51,plain,(
% 0.10/0.41 (![X]: (~god(X)|(being(X)&absolutelyInfinite(X))))&(![X]: (god(X)|(~being(X)|~absolutelyInfinite(X))))),
% 0.10/0.41 inference(miniscoping,[status(thm)],[f50])).
% 0.10/0.41 fof(f52,plain,(
% 0.10/0.41 ![X0]: (~god(X0)|being(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f51])).
% 0.10/0.41 fof(f53,plain,(
% 0.10/0.41 ![X0]: (~god(X0)|absolutelyInfinite(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f51])).
% 0.10/0.41 fof(f55,plain,(
% 0.10/0.41 ![X,Y]: (absolutelyInfinite(X)<=>((substance(X)&constInInfAttributes(X))&(~attributeOf(Y,X)|(expressesEternalEssentiality(Y)&expressesInfiniteEssentiality(Y)))))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.10/0.41 fof(f56,plain,(
% 0.10/0.41 ![X,Y]: ((~absolutelyInfinite(X)|((substance(X)&constInInfAttributes(X))&(~attributeOf(Y,X)|(expressesEternalEssentiality(Y)&expressesInfiniteEssentiality(Y)))))&(absolutelyInfinite(X)|((~substance(X)|~constInInfAttributes(X))|(attributeOf(Y,X)&(~expressesEternalEssentiality(Y)|~expressesInfiniteEssentiality(Y))))))),
% 0.10/0.41 inference(NNF_transformation,[status(thm)],[f55])).
% 0.10/0.41 fof(f57,plain,(
% 0.10/0.41 (![X]: (~absolutelyInfinite(X)|((substance(X)&constInInfAttributes(X))&(![Y]: (~attributeOf(Y,X)|(expressesEternalEssentiality(Y)&expressesInfiniteEssentiality(Y)))))))&(![X]: (absolutelyInfinite(X)|((~substance(X)|~constInInfAttributes(X))|((![Y]: attributeOf(Y,X))&(![Y]: (~expressesEternalEssentiality(Y)|~expressesInfiniteEssentiality(Y)))))))),
% 0.10/0.41 inference(miniscoping,[status(thm)],[f56])).
% 0.10/0.41 fof(f58,plain,(
% 0.10/0.41 ![X0]: (~absolutelyInfinite(X0)|substance(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f57])).
% 0.10/0.41 fof(f112,plain,(
% 0.10/0.41 ![X]: (~inItself(X)|selfCaused(X))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.10/0.41 fof(f113,plain,(
% 0.10/0.41 ![X0]: (~inItself(X0)|selfCaused(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f112])).
% 0.10/0.41 fof(f114,plain,(
% 0.10/0.41 ![X]: (~being(X)|hasEssence(X))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.10/0.41 fof(f115,plain,(
% 0.10/0.41 ![X0]: (~being(X0)|hasEssence(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f114])).
% 0.10/0.41 fof(f116,plain,(
% 0.10/0.41 ![X]: ((~essenceInvExistence(X)|~hasEssence(X))|exists(X))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.10/0.41 fof(f117,plain,(
% 0.10/0.41 ![X0]: (~essenceInvExistence(X0)|~hasEssence(X0)|exists(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f116])).
% 0.10/0.41 fof(f118,plain,(
% 0.10/0.41 (?[X]: (god(X)&~exists(X)))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.10/0.41 fof(f119,plain,(
% 0.10/0.41 (god(sK0_skl)&~exists(sK0_skl))),
% 0.10/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X,sK0_skl)],[f118])).
% 0.10/0.41 fof(f120,plain,(
% 0.10/0.41 god(sK0_skl)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f119])).
% 0.10/0.41 fof(f121,plain,(
% 0.10/0.41 ~exists(sK0_skl)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f119])).
% 0.10/0.41 fof(f124,plain,(
% 0.10/0.41 absolutelyInfinite(sK0_skl)),
% 0.10/0.41 inference(resolution,[status(thm)],[f53,f120])).
% 0.10/0.41 fof(f125,plain,(
% 0.10/0.41 being(sK0_skl)),
% 0.10/0.41 inference(resolution,[status(thm)],[f52,f120])).
% 0.10/0.41 fof(f126,plain,(
% 0.10/0.41 substance(sK0_skl)),
% 0.10/0.41 inference(resolution,[status(thm)],[f58,f124])).
% 0.10/0.41 fof(f128,plain,(
% 0.10/0.41 inItself(sK0_skl)),
% 0.10/0.41 inference(resolution,[status(thm)],[f126,f35])).
% 0.10/0.41 fof(f131,plain,(
% 0.10/0.41 selfCaused(sK0_skl)),
% 0.10/0.41 inference(resolution,[status(thm)],[f113,f128])).
% 0.10/0.41 fof(f133,plain,(
% 0.10/0.41 essenceInvExistence(sK0_skl)),
% 0.10/0.41 inference(resolution,[status(thm)],[f131,f25])).
% 0.10/0.41 fof(f136,plain,(
% 0.10/0.41 hasEssence(sK0_skl)),
% 0.10/0.41 inference(resolution,[status(thm)],[f115,f125])).
% 0.10/0.41 fof(f138,plain,(
% 0.10/0.41 ~hasEssence(sK0_skl)|exists(sK0_skl)),
% 0.10/0.41 inference(resolution,[status(thm)],[f117,f133])).
% 0.10/0.41 fof(f140,plain,(
% 0.10/0.41 exists(sK0_skl)),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f138,f136])).
% 0.10/0.41 fof(f141,plain,(
% 0.10/0.41 $false),
% 0.10/0.41 inference(backward_subsumption_resolution,[status(thm)],[f121,f140])).
% 0.10/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.46 % Elapsed time: 0.064845 seconds
% 0.10/0.46 % CPU time: 0.174571 seconds
% 0.10/0.46 % Total memory used: 81.755 MB
% 0.10/0.46 % Net memory used: 81.714 MB
%------------------------------------------------------------------------------