%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRA005+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:31:01 PM UTC 2026
% Result : Theorem 0.13s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRA005+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n008.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 20 18:18:40 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.39 % Refutation found
% 0.13/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.39 fof(f12,axiom,(
% 0.13/0.39 (! [V1,V2,E1,E2,P] :( ( shortest_path(V1,V2,P)& precedes(E1,E2,P) )=> ( ~ (? [E3] :( tail_of(E3) = tail_of(E1)& head_of(E3) = head_of(E2) ))& ~ precedes(E2,E1,P) ) ) )),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f18,conjecture,(
% 0.13/0.39 (! [V1,V2,E1,E2,P] :( ( shortest_path(V1,V2,P)& precedes(E1,E2,P) )=> ~ (? [E3] :( edge(E3)& tail_of(E3) = tail_of(E1)& head_of(E3) = head_of(E2) ) )) )),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f19,negated_conjecture,(
% 0.13/0.39 ~((! [V1,V2,E1,E2,P] :( ( shortest_path(V1,V2,P)& precedes(E1,E2,P) )=> ~ (? [E3] :( edge(E3)& tail_of(E3) = tail_of(E1)& head_of(E3) = head_of(E2) ) )) ))),
% 0.13/0.39 inference(negated_conjecture,[status(cth)],[f18])).
% 0.13/0.39 fof(f89,plain,(
% 0.13/0.39 ![V1,V2,E1,E2,P]: ((~shortest_path(V1,V2,P)|~precedes(E1,E2,P))|((![E3]: (~tail_of(E3)=tail_of(E1)|~head_of(E3)=head_of(E2)))&~precedes(E2,E1,P)))),
% 0.13/0.39 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.13/0.39 fof(f90,plain,(
% 0.13/0.39 ![E1,E2,P]: (((![V1,V2]: ~shortest_path(V1,V2,P))|~precedes(E1,E2,P))|((![E3]: (~tail_of(E3)=tail_of(E1)|~head_of(E3)=head_of(E2)))&~precedes(E2,E1,P)))),
% 0.13/0.39 inference(miniscoping,[status(thm)],[f89])).
% 0.13/0.39 fof(f91,plain,(
% 0.13/0.39 ![X0,X1,X2,X3,X4,X5]: (~shortest_path(X0,X1,X2)|~precedes(X3,X4,X2)|~tail_of(X5)=tail_of(X3)|~head_of(X5)=head_of(X4))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f90])).
% 0.13/0.39 fof(f116,plain,(
% 0.13/0.39 (?[V1,V2,E1,E2,P]: ((shortest_path(V1,V2,P)&precedes(E1,E2,P))&(?[E3]: ((edge(E3)&tail_of(E3)=tail_of(E1))&head_of(E3)=head_of(E2)))))),
% 0.13/0.39 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.13/0.39 fof(f117,plain,(
% 0.13/0.39 ?[E1,E2]: ((?[P]: ((?[V1,V2]: shortest_path(V1,V2,P))&precedes(E1,E2,P)))&(?[E3]: ((edge(E3)&tail_of(E3)=tail_of(E1))&head_of(E3)=head_of(E2))))),
% 0.13/0.39 inference(miniscoping,[status(thm)],[f116])).
% 0.13/0.39 fof(f118,plain,(
% 0.13/0.39 ((shortest_path(sK11_skl,sK12_skl,sK10_skl)&precedes(sK8_skl,sK9_skl,sK10_skl))&((edge(sK13_skl)&tail_of(sK13_skl)=tail_of(sK8_skl))&head_of(sK13_skl)=head_of(sK9_skl)))),
% 0.13/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(E1,sK8_skl),skolemize(E2,sK9_skl),skolemize(P,sK10_skl),skolemize(V1,sK11_skl),skolemize(V2,sK12_skl),skolemize(E3,sK13_skl)],[f117])).
% 0.13/0.39 fof(f119,plain,(
% 0.13/0.39 shortest_path(sK11_skl,sK12_skl,sK10_skl)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f118])).
% 0.13/0.39 fof(f120,plain,(
% 0.13/0.39 precedes(sK8_skl,sK9_skl,sK10_skl)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f118])).
% 0.13/0.39 fof(f122,plain,(
% 0.13/0.39 tail_of(sK13_skl)=tail_of(sK8_skl)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f118])).
% 0.13/0.39 fof(f123,plain,(
% 0.13/0.39 head_of(sK13_skl)=head_of(sK9_skl)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f118])).
% 0.13/0.39 fof(f171,definition,(
% 0.13/0.39 ![X0,X1]: (sQ7_spl <=> (~shortest_path(X0,X1,sK10_skl)))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f172,plain,(
% 0.13/0.39 ![X0,X1]: (~shortest_path(X0,X1,sK10_skl)|~sQ7_spl)),
% 0.13/0.39 inference(component_clause,[status(thm)],[f171])).
% 0.13/0.39 fof(f185,plain,(
% 0.13/0.39 $false|~sQ7_spl),
% 0.13/0.39 inference(backward_subsumption_resolution,[status(thm)],[f119,f172])).
% 0.13/0.39 fof(f186,plain,(
% 0.13/0.39 ~sQ7_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f185])).
% 0.13/0.39 fof(f258,plain,(
% 0.13/0.39 ![X0,X1,X2]: (~shortest_path(X0,X1,sK10_skl)|~tail_of(X2)=tail_of(sK8_skl)|~head_of(X2)=head_of(sK9_skl))),
% 0.13/0.39 inference(resolution,[status(thm)],[f91,f120])).
% 0.13/0.39 fof(f259,definition,(
% 0.13/0.39 ![X2]: (sQ21_spl <=> (~tail_of(X2)=tail_of(sK8_skl)|~head_of(X2)=head_of(sK9_skl)))),
% 0.13/0.39 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.39 fof(f260,plain,(
% 0.13/0.39 ![X0]: (~tail_of(X0)=tail_of(sK8_skl)|~head_of(X0)=head_of(sK9_skl)|~sQ21_spl)),
% 0.13/0.39 inference(component_clause,[status(thm)],[f259])).
% 0.13/0.39 fof(f262,plain,(
% 0.13/0.39 sQ7_spl|sQ21_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f258,f171,f259])).
% 0.13/0.39 fof(f263,plain,(
% 0.13/0.39 ![X0]: (~tail_of(X0)=tail_of(sK13_skl)|~head_of(X0)=head_of(sK9_skl)|~sQ21_spl)),
% 0.13/0.39 inference(forward_demodulation,[status(thm)],[f122,f260])).
% 0.13/0.39 fof(f264,plain,(
% 0.13/0.39 ![X0]: (~tail_of(X0)=tail_of(sK13_skl)|~head_of(X0)=head_of(sK13_skl)|~sQ21_spl)),
% 0.13/0.39 inference(forward_demodulation,[status(thm)],[f123,f263])).
% 0.13/0.39 fof(f267,plain,(
% 0.13/0.39 ~tail_of(sK13_skl)=tail_of(sK13_skl)|~sQ21_spl),
% 0.13/0.39 inference(equality_resolution,[status(thm)],[f264])).
% 0.13/0.39 fof(f275,plain,(
% 0.13/0.39 $false|~sQ21_spl),
% 0.13/0.39 inference(trivial_equality_resolution,[status(thm)],[f267])).
% 0.13/0.39 fof(f276,plain,(
% 0.13/0.39 ~sQ21_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f275])).
% 0.13/0.39 fof(f277,plain,(
% 0.13/0.39 $false),
% 0.13/0.39 inference(sat_refutation,[status(thm)],[f186,f262,f276])).
% 0.13/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.41 % Elapsed time: 0.050572 seconds
% 0.13/0.41 % CPU time: 0.145890 seconds
% 0.13/0.41 % Total memory used: 84.562 MB
% 0.13/0.41 % Net memory used: 84.489 MB
%------------------------------------------------------------------------------