%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PHI014+1 : TPTP v9.3.1. Released v7.2.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 01:58:09 PM UTC 2026
% Result : Theorem 0.09s 5.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI014+1 : TPTP v9.3.1. Released v7.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n015.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Mon Sep 21 03:33:41 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 0.09/5.40 % Refutation found
% 0.09/5.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/5.40 % SZS output start CNFRefutation for theBenchmark
% 0.09/5.40 fof(f1,axiom,(
% 0.09/5.40 (! [F] :( property(F)=> ( (? [Y] :( object(Y)& is_the(Y,F) ))=> (! [Z] :( object(Z)=> ( is_the(Z,F)=> exemplifies_property(F,Z) ) ) )) ) )),
% 0.09/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/5.40 fof(f2,axiom,(
% 0.09/5.40 (! [X,F] :( is_the(X,F)=> ( property(F)& object(X) ) ) )),
% 0.09/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/5.40 fof(f3,axiom,(
% 0.09/5.40 (! [X] :( object(X)=> ( exemplifies_property(none_greater,X)<=> ( exemplifies_property(conceivable,X)& ~ (? [Y] :( object(Y)& exemplifies_relation(greater_than,Y,X)& exemplifies_property(conceivable,Y) ) )) ) ) )),
% 0.09/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/5.40 fof(f4,axiom,(
% 0.09/5.40 (! [X] :( object(X)=> ( ( is_the(X,none_greater)& ~ exemplifies_property(existence,X) )=> (? [Y] :( object(Y)& exemplifies_relation(greater_than,Y,X)& exemplifies_property(conceivable,Y) ) )) ) )),
% 0.09/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/5.40 fof(f5,axiom,(
% 0.09/5.40 is_the(god,none_greater) ),
% 0.09/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/5.40 fof(f6,conjecture,(
% 0.09/5.40 exemplifies_property(existence,god) ),
% 0.09/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/5.40 fof(f7,negated_conjecture,(
% 0.09/5.40 ~(exemplifies_property(existence,god) )),
% 0.09/5.40 inference(negated_conjecture,[status(cth)],[f6])).
% 0.09/5.40 fof(f8,plain,(
% 0.09/5.40 ![F]: (~property(F)|((![Y]: (~object(Y)|~is_the(Y,F)))|(![Z]: (~object(Z)|(~is_the(Z,F)|exemplifies_property(F,Z))))))),
% 0.09/5.40 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.09/5.40 fof(f9,plain,(
% 0.09/5.40 ![X0,X1,X2]: (~property(X0)|~object(X1)|~is_the(X1,X0)|~object(X2)|~is_the(X2,X0)|exemplifies_property(X0,X2))),
% 0.09/5.40 inference(cnf_transformation,[status(thm)],[f8])).
% 0.09/5.40 fof(f10,plain,(
% 0.09/5.40 ![X,F]: (~is_the(X,F)|(property(F)&object(X)))),
% 0.09/5.40 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.09/5.40 fof(f11,plain,(
% 0.09/5.40 ![X0,X1]: (~is_the(X0,X1)|property(X1))),
% 0.09/5.40 inference(cnf_transformation,[status(thm)],[f10])).
% 0.09/5.40 fof(f12,plain,(
% 0.09/5.40 ![X0,X1]: (~is_the(X0,X1)|object(X0))),
% 0.09/5.40 inference(cnf_transformation,[status(thm)],[f10])).
% 0.09/5.40 fof(f13,plain,(
% 0.09/5.40 ![X]: (~object(X)|(exemplifies_property(none_greater,X)<=>(exemplifies_property(conceivable,X)&(![Y]: ((~object(Y)|~exemplifies_relation(greater_than,Y,X))|~exemplifies_property(conceivable,Y))))))),
% 0.09/5.40 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.09/5.40 fof(f14,plain,(
% 0.09/5.40 ![X]: (~object(X)|((~exemplifies_property(none_greater,X)|(exemplifies_property(conceivable,X)&(![Y]: ((~object(Y)|~exemplifies_relation(greater_than,Y,X))|~exemplifies_property(conceivable,Y)))))&(exemplifies_property(none_greater,X)|(~exemplifies_property(conceivable,X)|(?[Y]: ((object(Y)&exemplifies_relation(greater_than,Y,X))&exemplifies_property(conceivable,Y)))))))),
% 0.09/5.40 inference(NNF_transformation,[status(thm)],[f13])).
% 0.09/5.40 fof(f15,plain,(
% 0.09/5.40 ![X]: (~object(X)|((~exemplifies_property(none_greater,X)|(exemplifies_property(conceivable,X)&(![Y]: ((~object(Y)|~exemplifies_relation(greater_than,Y,X))|~exemplifies_property(conceivable,Y)))))&(exemplifies_property(none_greater,X)|(~exemplifies_property(conceivable,X)|((object(sK0_skl(X))&exemplifies_relation(greater_than,sK0_skl(X),X))&exemplifies_property(conceivable,sK0_skl(X)))))))),
% 0.09/5.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y,sK0_skl(X))],[f14])).
% 0.09/5.40 fof(f17,plain,(
% 0.09/5.40 ![X0,X1]: (~object(X0)|~exemplifies_property(none_greater,X0)|~object(X1)|~exemplifies_relation(greater_than,X1,X0)|~exemplifies_property(conceivable,X1))),
% 0.09/5.40 inference(cnf_transformation,[status(thm)],[f15])).
% 0.09/5.40 fof(f21,plain,(
% 0.09/5.40 ![X]: (~object(X)|((~is_the(X,none_greater)|exemplifies_property(existence,X))|(?[Y]: ((object(Y)&exemplifies_relation(greater_than,Y,X))&exemplifies_property(conceivable,Y)))))),
% 0.09/5.40 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.09/5.40 fof(f22,plain,(
% 0.09/5.40 ![X]: (~object(X)|((~is_the(X,none_greater)|exemplifies_property(existence,X))|((object(sK1_skl(X))&exemplifies_relation(greater_than,sK1_skl(X),X))&exemplifies_property(conceivable,sK1_skl(X)))))),
% 0.09/5.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y,sK1_skl(X))],[f21])).
% 0.09/5.40 fof(f23,plain,(
% 0.09/5.40 ![X0]: (~object(X0)|~is_the(X0,none_greater)|exemplifies_property(existence,X0)|object(sK1_skl(X0)))),
% 0.09/5.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.09/5.40 fof(f24,plain,(
% 0.09/5.40 ![X0]: (~object(X0)|~is_the(X0,none_greater)|exemplifies_property(existence,X0)|exemplifies_relation(greater_than,sK1_skl(X0),X0))),
% 0.09/5.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.09/5.40 fof(f25,plain,(
% 0.09/5.40 ![X0]: (~object(X0)|~is_the(X0,none_greater)|exemplifies_property(existence,X0)|exemplifies_property(conceivable,sK1_skl(X0)))),
% 0.09/5.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.09/5.40 fof(f26,plain,(
% 0.09/5.40 is_the(god,none_greater)),
% 0.09/5.40 inference(cnf_transformation,[status(thm)],[f5])).
% 0.09/5.40 fof(f27,plain,(
% 0.09/5.40 ~exemplifies_property(existence,god)),
% 0.09/5.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.09/5.40 fof(f28,plain,(
% 0.09/5.40 ![X0,X1,X2]: (~object(X0)|~is_the(X0,X1)|~object(X2)|~is_the(X2,X1)|exemplifies_property(X1,X2))),
% 0.09/5.40 inference(backward_subsumption_resolution,[status(thm)],[f9,f11])).
% 0.09/5.40 fof(f29,plain,(
% 0.09/5.40 ![X0]: (~is_the(X0,none_greater)|exemplifies_property(existence,X0)|object(sK1_skl(X0)))),
% 0.09/5.40 inference(forward_subsumption_resolution,[status(thm)],[f23,f12])).
% 0.09/5.40 fof(f30,plain,(
% 0.09/5.40 ![X0]: (~is_the(X0,none_greater)|exemplifies_property(existence,X0)|exemplifies_relation(greater_than,sK1_skl(X0),X0))),
% 0.09/5.40 inference(forward_subsumption_resolution,[status(thm)],[f24,f12])).
% 0.09/5.40 fof(f31,plain,(
% 0.09/5.40 ![X0]: (~is_the(X0,none_greater)|exemplifies_property(existence,X0)|exemplifies_property(conceivable,sK1_skl(X0)))),
% 0.09/5.40 inference(forward_subsumption_resolution,[status(thm)],[f25,f12])).
% 0.09/5.40 fof(f32,plain,(
% 0.09/5.40 ![X0,X1,X2]: (~is_the(X0,X1)|~object(X2)|~is_the(X2,X1)|exemplifies_property(X1,X2))),
% 0.09/5.40 inference(forward_subsumption_resolution,[status(thm)],[f28,f12])).
% 0.09/5.40 fof(f34,plain,(
% 0.09/5.40 object(god)),
% 0.09/5.40 inference(resolution,[status(thm)],[f12,f26])).
% 0.09/5.40 fof(f35,plain,(
% 0.09/5.40 ![X0]: (~is_the(X0,none_greater)|~object(god)|exemplifies_property(none_greater,god))),
% 0.09/5.40 inference(resolution,[status(thm)],[f32,f26])).
% 0.09/5.40 fof(f36,definition,(
% 0.09/5.40 ![X0]: (sQ0_spl <=> (~is_the(X0,none_greater)))),
% 0.09/5.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.09/5.40 fof(f37,plain,(
% 0.09/5.40 ![X0]: (~is_the(X0,none_greater)|~sQ0_spl)),
% 0.09/5.40 inference(component_clause,[status(thm)],[f36])).
% 0.09/5.40 fof(f39,definition,(
% 0.09/5.40 sQ1_spl <=> (object(god))),
% 0.09/5.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.09/5.40 fof(f41,plain,(
% 0.09/5.40 ~object(god)|sQ1_spl),
% 0.09/5.40 inference(component_clause,[status(thm)],[f39])).
% 0.09/5.40 fof(f42,definition,(
% 0.09/5.40 sQ2_spl <=> (exemplifies_property(none_greater,god))),
% 0.09/5.40 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.09/5.40 fof(f43,plain,(
% 0.09/5.40 exemplifies_property(none_greater,god)|~sQ2_spl),
% 0.09/5.40 inference(component_clause,[status(thm)],[f42])).
% 0.09/5.40 fof(f45,plain,(
% 0.09/5.40 sQ0_spl|~sQ1_spl|sQ2_spl),
% 0.09/5.40 inference(split_clause,[status(thm)],[f35,f36,f39,f42])).
% 0.09/5.40 fof(f51,plain,(
% 0.09/5.40 $false|sQ1_spl),
% 0.09/5.40 inference(forward_subsumption_resolution,[status(thm)],[f41,f34])).
% 0.09/5.40 fof(f52,plain,(
% 0.09/5.40 sQ1_spl),
% 0.09/5.40 inference(contradiction_clause,[status(thm)],[f51])).
% 0.09/5.40 fof(f53,plain,(
% 0.09/5.40 $false|~sQ0_spl),
% 0.09/5.40 inference(backward_subsumption_resolution,[status(thm)],[f26,f37])).
% 0.09/5.40 fof(f54,plain,(
% 0.09/5.40 ~sQ0_spl),
% 0.09/5.40 inference(contradiction_clause,[status(thm)],[f53])).
% 0.09/5.40 fof(f61,plain,(
% 0.09/5.40 ![X0]: (~object(god)|~object(X0)|~exemplifies_relation(greater_than,X0,god)|~exemplifies_property(conceivable,X0)|~sQ2_spl)),
% 0.09/5.40 inference(resolution,[status(thm)],[f17,f43])).
% 0.09/5.40 fof(f62,definition,(
% 0.09/5.40 ![X0]: (sQ4_spl <=> (~object(X0)|~exemplifies_relation(greater_than,X0,god)|~exemplifies_property(conceivable,X0)))),
% 0.09/5.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.09/5.40 fof(f63,plain,(
% 0.09/5.40 ![X0]: (~object(X0)|~exemplifies_relation(greater_than,X0,god)|~exemplifies_property(conceivable,X0)|~sQ4_spl)),
% 0.09/5.40 inference(component_clause,[status(thm)],[f62])).
% 0.09/5.40 fof(f65,plain,(
% 0.09/5.40 ~sQ1_spl|sQ4_spl|~sQ2_spl),
% 0.09/5.40 inference(split_clause,[status(thm)],[f61,f39,f62,f42])).
% 0.09/5.40 fof(f67,plain,(
% 0.09/5.40 ~object(sK1_skl(god))|~exemplifies_property(conceivable,sK1_skl(god))|~is_the(god,none_greater)|exemplifies_property(existence,god)|~sQ4_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f63,f30])).
% 0.13/5.40 fof(f75,definition,(
% 0.13/5.40 sQ7_spl <=> (object(sK1_skl(god)))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f77,plain,(
% 0.13/5.40 ~object(sK1_skl(god))|sQ7_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f75])).
% 0.13/5.40 fof(f78,definition,(
% 0.13/5.40 sQ8_spl <=> (exemplifies_property(conceivable,sK1_skl(god)))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f80,plain,(
% 0.13/5.40 ~exemplifies_property(conceivable,sK1_skl(god))|sQ8_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f78])).
% 0.13/5.40 fof(f81,definition,(
% 0.13/5.40 sQ9_spl <=> (is_the(god,none_greater))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f83,plain,(
% 0.13/5.40 ~is_the(god,none_greater)|sQ9_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f81])).
% 0.13/5.40 fof(f84,definition,(
% 0.13/5.40 sQ10_spl <=> (exemplifies_property(existence,god))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f85,plain,(
% 0.13/5.40 exemplifies_property(existence,god)|~sQ10_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f84])).
% 0.13/5.40 fof(f87,plain,(
% 0.13/5.40 ~sQ7_spl|~sQ8_spl|~sQ9_spl|sQ10_spl|~sQ4_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f67,f75,f78,f81,f84,f62])).
% 0.13/5.40 fof(f88,plain,(
% 0.13/5.40 $false|~sQ10_spl),
% 0.13/5.40 inference(forward_subsumption_resolution,[status(thm)],[f85,f27])).
% 0.13/5.40 fof(f89,plain,(
% 0.13/5.40 ~sQ10_spl),
% 0.13/5.40 inference(contradiction_clause,[status(thm)],[f88])).
% 0.13/5.40 fof(f90,plain,(
% 0.13/5.40 $false|sQ9_spl),
% 0.13/5.40 inference(forward_subsumption_resolution,[status(thm)],[f83,f26])).
% 0.13/5.40 fof(f91,plain,(
% 0.13/5.40 sQ9_spl),
% 0.13/5.40 inference(contradiction_clause,[status(thm)],[f90])).
% 0.13/5.40 fof(f92,plain,(
% 0.13/5.40 ~is_the(god,none_greater)|exemplifies_property(existence,god)|sQ7_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f77,f29])).
% 0.13/5.40 fof(f93,plain,(
% 0.13/5.40 ~sQ9_spl|sQ10_spl|sQ7_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f92,f81,f84,f75])).
% 0.13/5.40 fof(f94,plain,(
% 0.13/5.40 ~is_the(god,none_greater)|exemplifies_property(existence,god)|sQ8_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f80,f31])).
% 0.13/5.40 fof(f95,plain,(
% 0.13/5.40 ~sQ9_spl|sQ10_spl|sQ8_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f94,f81,f84,f78])).
% 0.13/5.40 fof(f96,plain,(
% 0.13/5.40 $false),
% 0.13/5.40 inference(sat_refutation,[status(thm)],[f45,f52,f54,f65,f87,f89,f91,f93,f95])).
% 0.13/5.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/5.43 % Elapsed time: 0.043443 seconds
% 0.13/5.43 % CPU time: 0.114173 seconds
% 0.13/5.43 % Total memory used: 17.113 MB
% 0.13/5.43 % Net memory used: 16.706 MB
%------------------------------------------------------------------------------