%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO148+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 : n008.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.15s 0.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO148+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n008.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sun Sep 20 12:31:11 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.45 % Drodi V4.1.1
% 0.15/0.47 % Refutation found
% 0.15/0.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.47 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.47 fof(f28,axiom,(
% 0.15/0.47 (! [X,Y,P] :( connect(X,Y,P)<=> once(at_the_same_time(at(X,P),at(Y,P))) ) )),
% 0.15/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.47 fof(f34,axiom,(
% 0.15/0.47 (! [X] :(? [O] : trajectory_of(X) = O ))),
% 0.15/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.47 fof(f35,axiom,(
% 0.15/0.47 (! [P1,P2,Q1,Q2,X,Y] :( ( once(at_the_same_time(at(X,P1),at(Y,P2)))& once(at_the_same_time(at(X,Q1),at(Y,Q2))) )=> ~ ( ordered_by(trajectory_of(X),P1,Q1)& ordered_by(trajectory_of(Y),Q2,P2) ) ) )),
% 0.15/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.47 fof(f37,conjecture,(
% 0.15/0.47 (! [P,X,Y] :( connect(X,Y,P)=> (! [Q1,Q2] :( ( ordered_by(trajectory_of(Y),Q2,P)& ordered_by(trajectory_of(X),P,Q1) )=> ~ once(at_the_same_time(at(X,Q1),at(Y,Q2))) ) )) )),
% 0.15/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.47 fof(f38,negated_conjecture,(
% 0.15/0.47 ~((! [P,X,Y] :( connect(X,Y,P)=> (! [Q1,Q2] :( ( ordered_by(trajectory_of(Y),Q2,P)& ordered_by(trajectory_of(X),P,Q1) )=> ~ once(at_the_same_time(at(X,Q1),at(Y,Q2))) ) )) ))),
% 0.15/0.47 inference(negated_conjecture,[status(cth)],[f37])).
% 0.15/0.47 fof(f197,plain,(
% 0.15/0.47 ![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.15/0.47 inference(NNF_transformation,[status(thm)],[f28])).
% 0.15/0.47 fof(f198,plain,(
% 0.15/0.47 (![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.15/0.47 inference(miniscoping,[status(thm)],[f197])).
% 0.15/0.47 fof(f199,plain,(
% 0.15/0.47 ![X0,X1,X2]: (~connect(X0,X1,X2)|once(at_the_same_time(at(X0,X2),at(X1,X2))))),
% 0.15/0.47 inference(cnf_transformation,[status(thm)],[f198])).
% 0.15/0.47 fof(f218,plain,(
% 0.15/0.47 ![X]: trajectory_of(X)=sK24_skl(X)),
% 0.15/0.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(O,sK24_skl(X))],[f34])).
% 0.15/0.47 fof(f219,plain,(
% 0.15/0.47 ![X0]: (trajectory_of(X0)=sK24_skl(X0))),
% 0.15/0.47 inference(cnf_transformation,[status(thm)],[f218])).
% 0.15/0.47 fof(f220,plain,(
% 0.15/0.47 ![P1,P2,Q1,Q2,X,Y]: ((~once(at_the_same_time(at(X,P1),at(Y,P2)))|~once(at_the_same_time(at(X,Q1),at(Y,Q2))))|(~ordered_by(trajectory_of(X),P1,Q1)|~ordered_by(trajectory_of(Y),Q2,P2)))),
% 0.15/0.47 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.15/0.47 fof(f221,plain,(
% 0.15/0.47 ![X0,X1,X2,X3,X4,X5]: (~once(at_the_same_time(at(X0,X1),at(X2,X3)))|~once(at_the_same_time(at(X0,X4),at(X2,X5)))|~ordered_by(trajectory_of(X0),X1,X4)|~ordered_by(trajectory_of(X2),X5,X3))),
% 0.15/0.47 inference(cnf_transformation,[status(thm)],[f220])).
% 0.15/0.47 fof(f225,plain,(
% 0.15/0.47 (?[P,X,Y]: (connect(X,Y,P)&(?[Q1,Q2]: ((ordered_by(trajectory_of(Y),Q2,P)&ordered_by(trajectory_of(X),P,Q1))&once(at_the_same_time(at(X,Q1),at(Y,Q2)))))))),
% 0.15/0.47 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.15/0.47 fof(f226,plain,(
% 0.15/0.47 (connect(sK27_skl,sK28_skl,sK26_skl)&((ordered_by(trajectory_of(sK28_skl),sK30_skl,sK26_skl)&ordered_by(trajectory_of(sK27_skl),sK26_skl,sK29_skl))&once(at_the_same_time(at(sK27_skl,sK29_skl),at(sK28_skl,sK30_skl)))))),
% 0.15/0.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl,sK28_skl,sK29_skl,sK30_skl]),skolemize(P,sK26_skl),skolemize(X,sK27_skl),skolemize(Y,sK28_skl),skolemize(Q1,sK29_skl),skolemize(Q2,sK30_skl)],[f225])).
% 0.15/0.47 fof(f227,plain,(
% 0.15/0.47 connect(sK27_skl,sK28_skl,sK26_skl)),
% 0.15/0.47 inference(cnf_transformation,[status(thm)],[f226])).
% 0.15/0.47 fof(f228,plain,(
% 0.15/0.47 ordered_by(trajectory_of(sK28_skl),sK30_skl,sK26_skl)),
% 0.15/0.47 inference(cnf_transformation,[status(thm)],[f226])).
% 0.15/0.47 fof(f229,plain,(
% 0.15/0.47 ordered_by(trajectory_of(sK27_skl),sK26_skl,sK29_skl)),
% 0.15/0.47 inference(cnf_transformation,[status(thm)],[f226])).
% 0.15/0.47 fof(f230,plain,(
% 0.15/0.47 once(at_the_same_time(at(sK27_skl,sK29_skl),at(sK28_skl,sK30_skl)))),
% 0.15/0.47 inference(cnf_transformation,[status(thm)],[f226])).
% 0.15/0.47 fof(f248,plain,(
% 0.15/0.47 once(at_the_same_time(at(sK27_skl,sK26_skl),at(sK28_skl,sK26_skl)))),
% 0.15/0.47 inference(resolution,[status(thm)],[f199,f227])).
% 0.15/0.47 fof(f251,plain,(
% 0.15/0.47 ordered_by(sK24_skl(sK27_skl),sK26_skl,sK29_skl)),
% 0.15/0.47 inference(backward_demodulation,[status(thm)],[f219,f229])).
% 0.15/0.47 fof(f254,plain,(
% 0.15/0.47 ordered_by(sK24_skl(sK28_skl),sK30_skl,sK26_skl)),
% 0.15/0.48 inference(backward_demodulation,[status(thm)],[f219,f228])).
% 0.15/0.48 fof(f387,plain,(
% 0.15/0.48 ![X0,X1,X2,X3,X4,X5]: (~once(at_the_same_time(at(X0,X1),at(X2,X3)))|~once(at_the_same_time(at(X0,X4),at(X2,X5)))|~ordered_by(sK24_skl(X0),X1,X4)|~ordered_by(trajectory_of(X2),X5,X3))),
% 0.15/0.48 inference(forward_demodulation,[status(thm)],[f219,f221])).
% 0.15/0.48 fof(f388,plain,(
% 0.15/0.48 ![X0,X1,X2,X3,X4,X5]: (~once(at_the_same_time(at(X0,X1),at(X2,X3)))|~once(at_the_same_time(at(X0,X4),at(X2,X5)))|~ordered_by(sK24_skl(X0),X1,X4)|~ordered_by(sK24_skl(X2),X5,X3))),
% 0.15/0.48 inference(forward_demodulation,[status(thm)],[f219,f387])).
% 0.15/0.48 fof(f392,plain,(
% 0.15/0.48 ![X0,X1]: (~once(at_the_same_time(at(sK27_skl,X0),at(sK28_skl,X1)))|~ordered_by(sK24_skl(sK27_skl),X0,sK29_skl)|~ordered_by(sK24_skl(sK28_skl),sK30_skl,X1))),
% 0.15/0.48 inference(resolution,[status(thm)],[f388,f230])).
% 0.15/0.48 fof(f497,plain,(
% 0.15/0.48 ~ordered_by(sK24_skl(sK27_skl),sK26_skl,sK29_skl)|~ordered_by(sK24_skl(sK28_skl),sK30_skl,sK26_skl)),
% 0.15/0.48 inference(resolution,[status(thm)],[f392,f248])).
% 0.15/0.48 fof(f499,definition,(
% 0.15/0.48 sQ6_spl <=> (ordered_by(sK24_skl(sK27_skl),sK26_skl,sK29_skl))),
% 0.15/0.48 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/0.48 fof(f501,plain,(
% 0.15/0.48 ~ordered_by(sK24_skl(sK27_skl),sK26_skl,sK29_skl)|sQ6_spl),
% 0.15/0.48 inference(component_clause,[status(thm)],[f499])).
% 0.15/0.48 fof(f502,definition,(
% 0.15/0.48 sQ7_spl <=> (ordered_by(sK24_skl(sK28_skl),sK30_skl,sK26_skl))),
% 0.15/0.48 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/0.48 fof(f504,plain,(
% 0.15/0.48 ~ordered_by(sK24_skl(sK28_skl),sK30_skl,sK26_skl)|sQ7_spl),
% 0.15/0.48 inference(component_clause,[status(thm)],[f502])).
% 0.15/0.48 fof(f505,plain,(
% 0.15/0.48 ~sQ6_spl|~sQ7_spl),
% 0.15/0.48 inference(split_clause,[status(thm)],[f497,f499,f502])).
% 0.15/0.48 fof(f513,plain,(
% 0.15/0.48 $false|sQ6_spl),
% 0.15/0.48 inference(forward_subsumption_resolution,[status(thm)],[f501,f251])).
% 0.15/0.48 fof(f514,plain,(
% 0.15/0.48 sQ6_spl),
% 0.15/0.48 inference(contradiction_clause,[status(thm)],[f513])).
% 0.15/0.48 fof(f515,plain,(
% 0.15/0.48 $false|sQ7_spl),
% 0.15/0.48 inference(forward_subsumption_resolution,[status(thm)],[f504,f254])).
% 0.15/0.48 fof(f516,plain,(
% 0.15/0.48 sQ7_spl),
% 0.15/0.48 inference(contradiction_clause,[status(thm)],[f515])).
% 0.15/0.48 fof(f517,plain,(
% 0.15/0.48 $false),
% 0.15/0.48 inference(sat_refutation,[status(thm)],[f505,f514,f516])).
% 0.15/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.54 % Elapsed time: 0.108475 seconds
% 0.15/0.54 % CPU time: 0.176193 seconds
% 0.15/0.54 % Total memory used: 23.860 MB
% 0.15/0.54 % Net memory used: 23.774 MB
%------------------------------------------------------------------------------