%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO147+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:53 PM UTC 2026
% Result : Theorem 0.08s 15.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO147+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/15.62 % CPULimit : 300
% 0.08/15.62 % WCLimit : 300
% 0.08/15.62 % DateTime : Sun Sep 20 12:30:37 UTC 2026
% 0.08/15.62 % CPUTime :
% 0.08/15.64 % Drodi V4.1.1
% 0.08/15.67 % Refutation found
% 0.08/15.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/15.67 % SZS output start CNFRefutation for theBenchmark
% 0.08/15.67 fof(f28,axiom,(
% 0.08/15.67 (! [X,Y,P] :( connect(X,Y,P)<=> once(at_the_same_time(at(X,P),at(Y,P))) ) )),
% 0.08/15.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/15.67 fof(f32,axiom,(
% 0.08/15.67 (! [A,B] :( once(at_the_same_time(A,B))=> ( once(A)& once(B) ) ) )),
% 0.08/15.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/15.67 fof(f33,axiom,(
% 0.08/15.67 (! [X,P] :( once(at(X,P))<=> incident_o(P,trajectory_of(X)) ) )),
% 0.08/15.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/15.67 fof(f34,axiom,(
% 0.08/15.67 (! [X] :(? [O] : trajectory_of(X) = O ))),
% 0.08/15.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/15.67 fof(f37,conjecture,(
% 0.08/15.67 (! [P,X,Y] :( connect(X,Y,P)=> ( incident_o(P,trajectory_of(X))& incident_o(P,trajectory_of(Y)) ) ) )),
% 0.08/15.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/15.67 fof(f38,negated_conjecture,(
% 0.08/15.67 ~((! [P,X,Y] :( connect(X,Y,P)=> ( incident_o(P,trajectory_of(X))& incident_o(P,trajectory_of(Y)) ) ) ))),
% 0.08/15.67 inference(negated_conjecture,[status(cth)],[f37])).
% 0.08/15.67 fof(f197,plain,(
% 0.08/15.67 ![X,Y,P]: ((~connect(X,Y,P)|once(at_the_same_time(at(X,P),at(Y,P))))&(connect(X,Y,P)|~once(at_the_same_time(at(X,P),at(Y,P)))))),
% 0.08/15.67 inference(NNF_transformation,[status(thm)],[f28])).
% 0.08/15.67 fof(f198,plain,(
% 0.08/15.67 (![X,Y,P]: (~connect(X,Y,P)|once(at_the_same_time(at(X,P),at(Y,P)))))&(![X,Y,P]: (connect(X,Y,P)|~once(at_the_same_time(at(X,P),at(Y,P)))))),
% 0.08/15.67 inference(miniscoping,[status(thm)],[f197])).
% 0.08/15.67 fof(f199,plain,(
% 0.08/15.67 ![X0,X1,X2]: (~connect(X0,X1,X2)|once(at_the_same_time(at(X0,X2),at(X1,X2))))),
% 0.08/15.67 inference(cnf_transformation,[status(thm)],[f198])).
% 0.08/15.67 fof(f211,plain,(
% 0.08/15.67 ![A,B]: (~once(at_the_same_time(A,B))|(once(A)&once(B)))),
% 0.08/15.67 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.08/15.67 fof(f212,plain,(
% 0.08/15.67 ![X0,X1]: (~once(at_the_same_time(X0,X1))|once(X0))),
% 0.08/15.67 inference(cnf_transformation,[status(thm)],[f211])).
% 0.08/15.67 fof(f213,plain,(
% 0.08/15.67 ![X0,X1]: (~once(at_the_same_time(X0,X1))|once(X1))),
% 0.08/15.67 inference(cnf_transformation,[status(thm)],[f211])).
% 0.08/15.67 fof(f214,plain,(
% 0.08/15.67 ![X,P]: ((~once(at(X,P))|incident_o(P,trajectory_of(X)))&(once(at(X,P))|~incident_o(P,trajectory_of(X))))),
% 0.08/15.67 inference(NNF_transformation,[status(thm)],[f33])).
% 0.08/15.67 fof(f215,plain,(
% 0.08/15.67 (![X,P]: (~once(at(X,P))|incident_o(P,trajectory_of(X))))&(![X,P]: (once(at(X,P))|~incident_o(P,trajectory_of(X))))),
% 0.08/15.67 inference(miniscoping,[status(thm)],[f214])).
% 0.08/15.67 fof(f216,plain,(
% 0.08/15.67 ![X0,X1]: (~once(at(X0,X1))|incident_o(X1,trajectory_of(X0)))),
% 0.08/15.67 inference(cnf_transformation,[status(thm)],[f215])).
% 0.08/15.67 fof(f218,plain,(
% 0.08/15.67 ![X]: trajectory_of(X)=sK24_skl(X)),
% 0.08/15.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(O,sK24_skl(X))],[f34])).
% 0.08/15.67 fof(f219,plain,(
% 0.08/15.67 ![X0]: (trajectory_of(X0)=sK24_skl(X0))),
% 0.08/15.67 inference(cnf_transformation,[status(thm)],[f218])).
% 0.08/15.67 fof(f225,plain,(
% 0.08/15.67 (?[P,X,Y]: (connect(X,Y,P)&(~incident_o(P,trajectory_of(X))|~incident_o(P,trajectory_of(Y)))))),
% 0.08/15.67 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.08/15.67 fof(f226,plain,(
% 0.08/15.67 (connect(sK27_skl,sK28_skl,sK26_skl)&(~incident_o(sK26_skl,trajectory_of(sK27_skl))|~incident_o(sK26_skl,trajectory_of(sK28_skl))))),
% 0.08/15.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl,sK28_skl]),skolemize(P,sK26_skl),skolemize(X,sK27_skl),skolemize(Y,sK28_skl)],[f225])).
% 0.08/15.67 fof(f227,plain,(
% 0.08/15.67 connect(sK27_skl,sK28_skl,sK26_skl)),
% 0.08/15.67 inference(cnf_transformation,[status(thm)],[f226])).
% 0.08/15.67 fof(f228,plain,(
% 0.08/15.67 ~incident_o(sK26_skl,trajectory_of(sK27_skl))|~incident_o(sK26_skl,trajectory_of(sK28_skl))),
% 0.08/15.67 inference(cnf_transformation,[status(thm)],[f226])).
% 0.08/15.67 fof(f229,definition,(
% 0.08/15.67 sQ0_spl <=> (incident_o(sK26_skl,trajectory_of(sK27_skl)))),
% 0.08/15.67 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.08/15.67 fof(f231,plain,(
% 0.08/15.67 ~incident_o(sK26_skl,trajectory_of(sK27_skl))|sQ0_spl),
% 0.08/15.67 inference(component_clause,[status(thm)],[f229])).
% 0.08/15.67 fof(f232,definition,(
% 0.08/15.67 sQ1_spl <=> (incident_o(sK26_skl,trajectory_of(sK28_skl)))),
% 0.08/15.67 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.08/15.67 fof(f234,plain,(
% 0.08/15.67 ~incident_o(sK26_skl,trajectory_of(sK28_skl))|sQ1_spl),
% 0.08/15.68 inference(component_clause,[status(thm)],[f232])).
% 0.08/15.68 fof(f235,plain,(
% 0.08/15.68 ~sQ0_spl|~sQ1_spl),
% 0.08/15.68 inference(split_clause,[status(thm)],[f228,f229,f232])).
% 0.08/15.68 fof(f243,plain,(
% 0.08/15.68 once(at_the_same_time(at(sK27_skl,sK26_skl),at(sK28_skl,sK26_skl)))),
% 0.08/15.68 inference(resolution,[status(thm)],[f199,f227])).
% 0.08/15.68 fof(f256,plain,(
% 0.08/15.68 ~incident_o(sK26_skl,sK24_skl(sK27_skl))|sQ0_spl),
% 0.08/15.68 inference(backward_demodulation,[status(thm)],[f219,f231])).
% 0.08/15.68 fof(f259,plain,(
% 0.08/15.68 ![X0,X1]: (~once(at(X0,X1))|incident_o(X1,sK24_skl(X0)))),
% 0.08/15.68 inference(backward_demodulation,[status(thm)],[f219,f216])).
% 0.08/15.68 fof(f300,plain,(
% 0.08/15.68 once(at(sK27_skl,sK26_skl))),
% 0.08/15.68 inference(resolution,[status(thm)],[f212,f243])).
% 0.08/15.68 fof(f302,plain,(
% 0.08/15.68 incident_o(sK26_skl,sK24_skl(sK27_skl))),
% 0.08/15.68 inference(resolution,[status(thm)],[f300,f259])).
% 0.08/15.68 fof(f304,plain,(
% 0.08/15.68 $false|sQ0_spl),
% 0.08/15.68 inference(forward_subsumption_resolution,[status(thm)],[f302,f256])).
% 0.08/15.68 fof(f305,plain,(
% 0.08/15.68 sQ0_spl),
% 0.08/15.68 inference(contradiction_clause,[status(thm)],[f304])).
% 0.08/15.68 fof(f306,plain,(
% 0.08/15.68 ~incident_o(sK26_skl,sK24_skl(sK28_skl))|sQ1_spl),
% 0.08/15.68 inference(forward_demodulation,[status(thm)],[f219,f234])).
% 0.08/15.68 fof(f312,plain,(
% 0.08/15.68 once(at(sK28_skl,sK26_skl))),
% 0.08/15.68 inference(resolution,[status(thm)],[f213,f243])).
% 0.08/15.68 fof(f314,plain,(
% 0.08/15.68 incident_o(sK26_skl,sK24_skl(sK28_skl))),
% 0.08/15.68 inference(resolution,[status(thm)],[f312,f259])).
% 0.08/15.68 fof(f316,plain,(
% 0.08/15.68 $false|sQ1_spl),
% 0.08/15.68 inference(forward_subsumption_resolution,[status(thm)],[f314,f306])).
% 0.08/15.68 fof(f317,plain,(
% 0.08/15.68 sQ1_spl),
% 0.08/15.68 inference(contradiction_clause,[status(thm)],[f316])).
% 0.08/15.68 fof(f318,plain,(
% 0.08/15.68 $false),
% 0.08/15.68 inference(sat_refutation,[status(thm)],[f235,f305,f317])).
% 0.08/15.68 % SZS output end CNFRefutation for theBenchmark.p
% 0.34/15.71 % Elapsed time: 0.069969 seconds
% 0.34/15.71 % CPU time: 0.166447 seconds
% 0.34/15.71 % Total memory used: 105.753 MB
% 0.34/15.71 % Net memory used: 105.610 MB
%------------------------------------------------------------------------------