%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO087+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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 12:25:44 PM UTC 2026
% Result : Theorem 0.16s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO087+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n009.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Sun Sep 20 10:27:58 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.47 % Drodi V4.1.1
% 0.16/0.49 % Refutation found
% 0.16/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.49 fof(f1,axiom,(
% 0.16/0.49 (! [C,C1] :( part_of(C1,C)<=> (! [P] :( incident_c(P,C1)=> incident_c(P,C) ) )) )),
% 0.16/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f4,axiom,(
% 0.16/0.49 (! [P,C] :( inner_point(P,C)<=> ( incident_c(P,C)& ~ end_point(P,C) ) ) )),
% 0.16/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f5,axiom,(
% 0.16/0.49 (! [P,C,C1] :( meet(P,C,C1)<=> ( incident_c(P,C)& incident_c(P,C1)& (! [Q] :( ( incident_c(Q,C)& incident_c(Q,C1) )=> ( end_point(Q,C)& end_point(Q,C1) ) ) )) ) )),
% 0.16/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f10,axiom,(
% 0.16/0.49 (! [C] :(? [P] : inner_point(P,C) ))),
% 0.16/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f17,conjecture,(
% 0.16/0.49 (! [C1,C2] :( part_of(C1,C2)=> ~ (? [P] : meet(P,C1,C2) )) )),
% 0.16/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f18,negated_conjecture,(
% 0.16/0.49 ~((! [C1,C2] :( part_of(C1,C2)=> ~ (? [P] : meet(P,C1,C2) )) ))),
% 0.16/0.49 inference(negated_conjecture,[status(cth)],[f17])).
% 0.16/0.49 fof(f19,plain,(
% 0.16/0.49 ![C,C1]: (part_of(C1,C)<=>(![P]: (~incident_c(P,C1)|incident_c(P,C))))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.16/0.49 fof(f20,plain,(
% 0.16/0.49 ![C,C1]: ((~part_of(C1,C)|(![P]: (~incident_c(P,C1)|incident_c(P,C))))&(part_of(C1,C)|(?[P]: (incident_c(P,C1)&~incident_c(P,C)))))),
% 0.16/0.49 inference(NNF_transformation,[status(thm)],[f19])).
% 0.16/0.49 fof(f21,plain,(
% 0.16/0.49 (![C,C1]: (~part_of(C1,C)|(![P]: (~incident_c(P,C1)|incident_c(P,C)))))&(![C,C1]: (part_of(C1,C)|(?[P]: (incident_c(P,C1)&~incident_c(P,C)))))),
% 0.16/0.49 inference(miniscoping,[status(thm)],[f20])).
% 0.16/0.49 fof(f22,plain,(
% 0.16/0.49 (![C,C1]: (~part_of(C1,C)|(![P]: (~incident_c(P,C1)|incident_c(P,C)))))&(![C,C1]: (part_of(C1,C)|(incident_c(sK0_skl(C1,C),C1)&~incident_c(sK0_skl(C1,C),C))))),
% 0.16/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(P,sK0_skl(C1,C))],[f21])).
% 0.16/0.49 fof(f23,plain,(
% 0.16/0.49 ![X0,X1,X2]: (~part_of(X0,X1)|~incident_c(X2,X0)|incident_c(X2,X1))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f22])).
% 0.16/0.49 fof(f47,plain,(
% 0.16/0.49 ![P,C]: ((~inner_point(P,C)|(incident_c(P,C)&~end_point(P,C)))&(inner_point(P,C)|(~incident_c(P,C)|end_point(P,C))))),
% 0.16/0.49 inference(NNF_transformation,[status(thm)],[f4])).
% 0.16/0.49 fof(f48,plain,(
% 0.16/0.49 (![P,C]: (~inner_point(P,C)|(incident_c(P,C)&~end_point(P,C))))&(![P,C]: (inner_point(P,C)|(~incident_c(P,C)|end_point(P,C))))),
% 0.16/0.49 inference(miniscoping,[status(thm)],[f47])).
% 0.16/0.49 fof(f49,plain,(
% 0.16/0.49 ![X0,X1]: (~inner_point(X0,X1)|incident_c(X0,X1))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f48])).
% 0.16/0.49 fof(f50,plain,(
% 0.16/0.49 ![X0,X1]: (~inner_point(X0,X1)|~end_point(X0,X1))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f48])).
% 0.16/0.49 fof(f52,plain,(
% 0.16/0.49 ![P,C,C1]: (meet(P,C,C1)<=>((incident_c(P,C)&incident_c(P,C1))&(![Q]: ((~incident_c(Q,C)|~incident_c(Q,C1))|(end_point(Q,C)&end_point(Q,C1))))))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.16/0.49 fof(f53,plain,(
% 0.16/0.49 ![P,C,C1]: ((~meet(P,C,C1)|((incident_c(P,C)&incident_c(P,C1))&(![Q]: ((~incident_c(Q,C)|~incident_c(Q,C1))|(end_point(Q,C)&end_point(Q,C1))))))&(meet(P,C,C1)|((~incident_c(P,C)|~incident_c(P,C1))|(?[Q]: ((incident_c(Q,C)&incident_c(Q,C1))&(~end_point(Q,C)|~end_point(Q,C1)))))))),
% 0.16/0.49 inference(NNF_transformation,[status(thm)],[f52])).
% 0.16/0.49 fof(f54,plain,(
% 0.16/0.49 (![P,C,C1]: (~meet(P,C,C1)|((incident_c(P,C)&incident_c(P,C1))&(![Q]: ((~incident_c(Q,C)|~incident_c(Q,C1))|(end_point(Q,C)&end_point(Q,C1)))))))&(![P,C,C1]: (meet(P,C,C1)|((~incident_c(P,C)|~incident_c(P,C1))|(?[Q]: ((incident_c(Q,C)&incident_c(Q,C1))&(~end_point(Q,C)|~end_point(Q,C1)))))))),
% 0.16/0.49 inference(miniscoping,[status(thm)],[f53])).
% 0.16/0.49 fof(f55,plain,(
% 0.16/0.49 (![P,C,C1]: (~meet(P,C,C1)|((incident_c(P,C)&incident_c(P,C1))&(![Q]: ((~incident_c(Q,C)|~incident_c(Q,C1))|(end_point(Q,C)&end_point(Q,C1)))))))&(![P,C,C1]: (meet(P,C,C1)|((~incident_c(P,C)|~incident_c(P,C1))|((incident_c(sK4_skl(C1,C,P),C)&incident_c(sK4_skl(C1,C,P),C1))&(~end_point(sK4_skl(C1,C,P),C)|~end_point(sK4_skl(C1,C,P),C1))))))),
% 0.16/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(Q,sK4_skl(C1,C,P))],[f54])).
% 0.16/0.49 fof(f58,plain,(
% 0.16/0.49 ![X0,X1,X2,X3]: (~meet(X0,X1,X2)|~incident_c(X3,X1)|~incident_c(X3,X2)|end_point(X3,X1))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f55])).
% 0.16/0.49 fof(f80,plain,(
% 0.16/0.49 ![C]: inner_point(sK7_skl(C),C)),
% 0.16/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(P,sK7_skl(C))],[f10])).
% 0.16/0.49 fof(f81,plain,(
% 0.16/0.49 ![X0]: (inner_point(sK7_skl(X0),X0))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f80])).
% 0.16/0.49 fof(f104,plain,(
% 0.16/0.49 (?[C1,C2]: (part_of(C1,C2)&(?[P]: meet(P,C1,C2))))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.16/0.49 fof(f105,plain,(
% 0.16/0.49 (part_of(sK13_skl,sK14_skl)&meet(sK15_skl,sK13_skl,sK14_skl))),
% 0.16/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(C1,sK13_skl),skolemize(C2,sK14_skl),skolemize(P,sK15_skl)],[f104])).
% 0.16/0.49 fof(f106,plain,(
% 0.16/0.49 part_of(sK13_skl,sK14_skl)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f105])).
% 0.16/0.49 fof(f107,plain,(
% 0.16/0.49 meet(sK15_skl,sK13_skl,sK14_skl)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f105])).
% 0.16/0.49 fof(f114,plain,(
% 0.16/0.49 ![X0]: (~incident_c(X0,sK13_skl)|~incident_c(X0,sK14_skl)|end_point(X0,sK13_skl))),
% 0.16/0.49 inference(resolution,[status(thm)],[f58,f107])).
% 0.16/0.49 fof(f131,plain,(
% 0.16/0.49 ![X0]: (incident_c(sK7_skl(X0),X0))),
% 0.16/0.49 inference(resolution,[status(thm)],[f49,f81])).
% 0.16/0.49 fof(f133,plain,(
% 0.16/0.49 ~incident_c(sK7_skl(sK13_skl),sK14_skl)|end_point(sK7_skl(sK13_skl),sK13_skl)),
% 0.16/0.49 inference(resolution,[status(thm)],[f131,f114])).
% 0.16/0.49 fof(f134,plain,(
% 0.16/0.49 ![X0]: (~end_point(sK7_skl(X0),X0))),
% 0.16/0.49 inference(resolution,[status(thm)],[f50,f81])).
% 0.16/0.49 fof(f135,plain,(
% 0.16/0.49 ~incident_c(sK7_skl(sK13_skl),sK14_skl)),
% 0.16/0.49 inference(backward_subsumption_resolution,[status(thm)],[f133,f134])).
% 0.16/0.49 fof(f137,plain,(
% 0.16/0.49 ![X0]: (~part_of(X0,sK14_skl)|~incident_c(sK7_skl(sK13_skl),X0))),
% 0.16/0.49 inference(resolution,[status(thm)],[f135,f23])).
% 0.16/0.49 fof(f148,plain,(
% 0.16/0.49 ~incident_c(sK7_skl(sK13_skl),sK13_skl)),
% 0.16/0.49 inference(resolution,[status(thm)],[f137,f106])).
% 0.16/0.49 fof(f149,plain,(
% 0.16/0.49 $false),
% 0.16/0.49 inference(forward_subsumption_resolution,[status(thm)],[f148,f131])).
% 0.16/0.49 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.54 % Elapsed time: 0.087923 seconds
% 0.16/0.54 % CPU time: 0.133499 seconds
% 0.16/0.54 % Total memory used: 18.296 MB
% 0.16/0.54 % Net memory used: 18.253 MB
%------------------------------------------------------------------------------