%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRA008+2 : 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 : n026.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 4.43s 1.10s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRA008+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n026.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % 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 18:24:51 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.43 % Drodi V4.1.1
% 4.43/1.10 % Refutation found
% 4.43/1.10 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.43/1.10 % SZS output start CNFRefutation for theBenchmark
% 4.43/1.10 fof(f1,axiom,(
% 4.43/1.10 (! [E] :( edge(E)=> head_of(E) != tail_of(E) ) )),
% 4.43/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.43/1.10 fof(f8,axiom,(
% 4.43/1.10 (! [E1,E2] :( sequential(E1,E2)<=> ( edge(E1)& edge(E2)& E1 != E2& head_of(E1) = tail_of(E2) ) ) )),
% 4.43/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.43/1.10 fof(f13,axiom,(
% 4.43/1.10 (! [E1,E2,E3] :( triangle(E1,E2,E3)<=> ( edge(E1)& edge(E2)& edge(E3)& sequential(E1,E2)& sequential(E2,E3)& sequential(E3,E1) ) ) )),
% 4.43/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.43/1.10 fof(f18,lemma,(
% 4.43/1.10 ( complete=> (! [V1,V2,E1,E2,P] :( ( shortest_path(V1,V2,P)& precedes(E1,E2,P) )=> (? [E3] :( edge(E3)& tail_of(E3) = head_of(E2)& head_of(E3) = tail_of(E1) ) )) )) ),
% 4.43/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.43/1.10 fof(f19,conjecture,(
% 4.43/1.10 ( complete=> (! [V1,V2,E1,E2,P] :( ( shortest_path(V1,V2,P)& precedes(E1,E2,P)& sequential(E1,E2) )=> (? [E3] : triangle(E1,E2,E3) )) )) ),
% 4.43/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.43/1.10 fof(f20,negated_conjecture,(
% 4.43/1.10 ~(( complete=> (! [V1,V2,E1,E2,P] :( ( shortest_path(V1,V2,P)& precedes(E1,E2,P)& sequential(E1,E2) )=> (? [E3] : triangle(E1,E2,E3) )) )) )),
% 4.43/1.10 inference(negated_conjecture,[status(cth)],[f19])).
% 4.43/1.10 fof(f21,plain,(
% 4.43/1.10 ![E]: (~edge(E)|~head_of(E)=tail_of(E))),
% 4.43/1.10 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 4.43/1.10 fof(f22,plain,(
% 4.43/1.10 ![X0]: (~edge(X0)|~head_of(X0)=tail_of(X0))),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f21])).
% 4.43/1.10 fof(f61,plain,(
% 4.43/1.10 ![E1,E2]: ((~sequential(E1,E2)|(((edge(E1)&edge(E2))&~E1=E2)&head_of(E1)=tail_of(E2)))&(sequential(E1,E2)|(((~edge(E1)|~edge(E2))|E1=E2)|~head_of(E1)=tail_of(E2))))),
% 4.43/1.10 inference(NNF_transformation,[status(thm)],[f8])).
% 4.43/1.10 fof(f62,plain,(
% 4.43/1.10 (![E1,E2]: (~sequential(E1,E2)|(((edge(E1)&edge(E2))&~E1=E2)&head_of(E1)=tail_of(E2))))&(![E1,E2]: (sequential(E1,E2)|(((~edge(E1)|~edge(E2))|E1=E2)|~head_of(E1)=tail_of(E2))))),
% 4.43/1.10 inference(miniscoping,[status(thm)],[f61])).
% 4.43/1.10 fof(f63,plain,(
% 4.43/1.10 ![X0,X1]: (~sequential(X0,X1)|edge(X0))),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f62])).
% 4.43/1.10 fof(f64,plain,(
% 4.43/1.10 ![X0,X1]: (~sequential(X0,X1)|edge(X1))),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f62])).
% 4.43/1.10 fof(f67,plain,(
% 4.43/1.10 ![X0,X1]: (sequential(X0,X1)|~edge(X0)|~edge(X1)|X0=X1|~head_of(X0)=tail_of(X1))),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f62])).
% 4.43/1.10 fof(f94,plain,(
% 4.43/1.10 ![E1,E2,E3]: ((~triangle(E1,E2,E3)|(((((edge(E1)&edge(E2))&edge(E3))&sequential(E1,E2))&sequential(E2,E3))&sequential(E3,E1)))&(triangle(E1,E2,E3)|(((((~edge(E1)|~edge(E2))|~edge(E3))|~sequential(E1,E2))|~sequential(E2,E3))|~sequential(E3,E1))))),
% 4.43/1.10 inference(NNF_transformation,[status(thm)],[f13])).
% 4.43/1.10 fof(f95,plain,(
% 4.43/1.10 (![E1,E2,E3]: (~triangle(E1,E2,E3)|(((((edge(E1)&edge(E2))&edge(E3))&sequential(E1,E2))&sequential(E2,E3))&sequential(E3,E1))))&(![E1,E2,E3]: (triangle(E1,E2,E3)|(((((~edge(E1)|~edge(E2))|~edge(E3))|~sequential(E1,E2))|~sequential(E2,E3))|~sequential(E3,E1))))),
% 4.43/1.10 inference(miniscoping,[status(thm)],[f94])).
% 4.43/1.10 fof(f102,plain,(
% 4.43/1.10 ![X0,X1,X2]: (triangle(X0,X1,X2)|~edge(X0)|~edge(X1)|~edge(X2)|~sequential(X0,X1)|~sequential(X1,X2)|~sequential(X2,X0))),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f95])).
% 4.43/1.10 fof(f117,plain,(
% 4.43/1.10 ~complete|(![V1,V2,E1,E2,P]: ((~shortest_path(V1,V2,P)|~precedes(E1,E2,P))|(?[E3]: ((edge(E3)&tail_of(E3)=head_of(E2))&head_of(E3)=tail_of(E1)))))),
% 4.43/1.10 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 4.43/1.10 fof(f118,plain,(
% 4.43/1.10 ~complete|(![E1,E2]: ((![P]: ((![V1,V2]: ~shortest_path(V1,V2,P))|~precedes(E1,E2,P)))|(?[E3]: ((edge(E3)&tail_of(E3)=head_of(E2))&head_of(E3)=tail_of(E1)))))),
% 4.43/1.10 inference(miniscoping,[status(thm)],[f117])).
% 4.43/1.10 fof(f119,plain,(
% 4.43/1.10 ~complete|(![E1,E2]: ((![P]: ((![V1,V2]: ~shortest_path(V1,V2,P))|~precedes(E1,E2,P)))|((edge(sK8_skl(E2,E1))&tail_of(sK8_skl(E2,E1))=head_of(E2))&head_of(sK8_skl(E2,E1))=tail_of(E1))))),
% 4.43/1.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(E3,sK8_skl(E2,E1))],[f118])).
% 4.43/1.10 fof(f120,plain,(
% 4.43/1.10 ![X0,X1,X2,X3,X4]: (~complete|~shortest_path(X0,X1,X2)|~precedes(X3,X4,X2)|edge(sK8_skl(X4,X3)))),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f119])).
% 4.43/1.10 fof(f121,plain,(
% 4.43/1.10 ![X0,X1,X2,X3,X4]: (~complete|~shortest_path(X0,X1,X2)|~precedes(X3,X4,X2)|tail_of(sK8_skl(X4,X3))=head_of(X4))),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f119])).
% 4.43/1.10 fof(f122,plain,(
% 4.43/1.10 ![X0,X1,X2,X3,X4]: (~complete|~shortest_path(X0,X1,X2)|~precedes(X3,X4,X2)|head_of(sK8_skl(X4,X3))=tail_of(X3))),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f119])).
% 4.43/1.10 fof(f123,plain,(
% 4.43/1.10 (complete&(?[V1,V2,E1,E2,P]: (((shortest_path(V1,V2,P)&precedes(E1,E2,P))&sequential(E1,E2))&(![E3]: ~triangle(E1,E2,E3)))))),
% 4.43/1.10 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 4.43/1.10 fof(f124,plain,(
% 4.43/1.10 complete&(?[E1,E2]: (((?[P]: ((?[V1,V2]: shortest_path(V1,V2,P))&precedes(E1,E2,P)))&sequential(E1,E2))&(![E3]: ~triangle(E1,E2,E3))))),
% 4.43/1.10 inference(miniscoping,[status(thm)],[f123])).
% 4.43/1.10 fof(f125,plain,(
% 4.43/1.10 complete&(((shortest_path(sK12_skl,sK13_skl,sK11_skl)&precedes(sK9_skl,sK10_skl,sK11_skl))&sequential(sK9_skl,sK10_skl))&(![E3]: ~triangle(sK9_skl,sK10_skl,E3)))),
% 4.43/1.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(E1,sK9_skl),skolemize(E2,sK10_skl),skolemize(P,sK11_skl),skolemize(V1,sK12_skl),skolemize(V2,sK13_skl)],[f124])).
% 4.43/1.10 fof(f126,plain,(
% 4.43/1.10 complete),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f125])).
% 4.43/1.10 fof(f127,plain,(
% 4.43/1.10 shortest_path(sK12_skl,sK13_skl,sK11_skl)),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f125])).
% 4.43/1.10 fof(f128,plain,(
% 4.43/1.10 precedes(sK9_skl,sK10_skl,sK11_skl)),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f125])).
% 4.43/1.10 fof(f129,plain,(
% 4.43/1.10 sequential(sK9_skl,sK10_skl)),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f125])).
% 4.43/1.10 fof(f130,plain,(
% 4.43/1.10 ![X0]: (~triangle(sK9_skl,sK10_skl,X0))),
% 4.43/1.10 inference(cnf_transformation,[status(thm)],[f125])).
% 4.43/1.10 fof(f151,plain,(
% 4.43/1.10 edge(sK9_skl)),
% 4.43/1.10 inference(resolution,[status(thm)],[f63,f129])).
% 4.43/1.10 fof(f166,plain,(
% 4.43/1.10 edge(sK10_skl)),
% 4.43/1.10 inference(resolution,[status(thm)],[f64,f129])).
% 4.43/1.10 fof(f201,plain,(
% 4.43/1.10 ![X0,X1,X2]: (triangle(X0,X1,X2)|~edge(X0)|~edge(X1)|~sequential(X0,X1)|~sequential(X1,X2)|~sequential(X2,X0))),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f102,f64])).
% 4.43/1.10 fof(f202,plain,(
% 4.43/1.10 ![X0,X1]: (triangle(X0,sK10_skl,X1)|~edge(X0)|~sequential(X0,sK10_skl)|~sequential(sK10_skl,X1)|~sequential(X1,X0))),
% 4.43/1.10 inference(resolution,[status(thm)],[f201,f166])).
% 4.43/1.10 fof(f204,plain,(
% 4.43/1.10 ![X0,X1]: (triangle(X0,sK10_skl,X1)|~sequential(X0,sK10_skl)|~sequential(sK10_skl,X1)|~sequential(X1,X0))),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f202,f64])).
% 4.43/1.10 fof(f337,plain,(
% 4.43/1.10 ![X0,X1,X2,X3,X4]: (~shortest_path(X0,X1,X2)|~precedes(X3,X4,X2)|edge(sK8_skl(X4,X3)))),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f120,f126])).
% 4.43/1.10 fof(f338,plain,(
% 4.43/1.10 ![X0,X1]: (~precedes(X0,X1,sK11_skl)|edge(sK8_skl(X1,X0)))),
% 4.43/1.10 inference(resolution,[status(thm)],[f337,f127])).
% 4.43/1.10 fof(f339,plain,(
% 4.43/1.10 ![X0,X1,X2,X3,X4]: (~shortest_path(X0,X1,X2)|~precedes(X3,X4,X2)|tail_of(sK8_skl(X4,X3))=head_of(X4))),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f121,f126])).
% 4.43/1.10 fof(f340,plain,(
% 4.43/1.10 ![X0,X1]: (~precedes(X0,X1,sK11_skl)|tail_of(sK8_skl(X1,X0))=head_of(X1))),
% 4.43/1.10 inference(resolution,[status(thm)],[f339,f127])).
% 4.43/1.10 fof(f341,plain,(
% 4.43/1.10 ![X0,X1,X2,X3,X4]: (~shortest_path(X0,X1,X2)|~precedes(X3,X4,X2)|head_of(sK8_skl(X4,X3))=tail_of(X3))),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f122,f126])).
% 4.43/1.10 fof(f342,plain,(
% 4.43/1.10 ![X0,X1]: (~precedes(X0,X1,sK11_skl)|head_of(sK8_skl(X1,X0))=tail_of(X0))),
% 4.43/1.10 inference(resolution,[status(thm)],[f341,f127])).
% 4.43/1.10 fof(f355,plain,(
% 4.43/1.10 edge(sK8_skl(sK10_skl,sK9_skl))),
% 4.43/1.10 inference(resolution,[status(thm)],[f338,f128])).
% 4.43/1.10 fof(f356,plain,(
% 4.43/1.10 tail_of(sK8_skl(sK10_skl,sK9_skl))=head_of(sK10_skl)),
% 4.43/1.10 inference(resolution,[status(thm)],[f340,f128])).
% 4.43/1.10 fof(f357,plain,(
% 4.43/1.10 head_of(sK8_skl(sK10_skl,sK9_skl))=tail_of(sK9_skl)),
% 4.43/1.10 inference(resolution,[status(thm)],[f342,f128])).
% 4.43/1.10 fof(f368,plain,(
% 4.43/1.10 sequential(sK10_skl,sK8_skl(sK10_skl,sK9_skl))|~edge(sK10_skl)|~edge(sK8_skl(sK10_skl,sK9_skl))|sK10_skl=sK8_skl(sK10_skl,sK9_skl)),
% 4.43/1.10 inference(resolution,[status(thm)],[f356,f67])).
% 4.43/1.10 fof(f373,plain,(
% 4.43/1.10 ~edge(sK8_skl(sK10_skl,sK9_skl))|~head_of(sK8_skl(sK10_skl,sK9_skl))=head_of(sK10_skl)),
% 4.43/1.10 inference(paramodulation,[status(thm)],[f356,f22])).
% 4.43/1.10 fof(f376,plain,(
% 4.43/1.10 sequential(sK10_skl,sK8_skl(sK10_skl,sK9_skl))|~edge(sK8_skl(sK10_skl,sK9_skl))|sK10_skl=sK8_skl(sK10_skl,sK9_skl)),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f368,f166])).
% 4.43/1.10 fof(f378,plain,(
% 4.43/1.10 ~head_of(sK8_skl(sK10_skl,sK9_skl))=head_of(sK10_skl)),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f373,f355])).
% 4.43/1.10 fof(f379,plain,(
% 4.43/1.10 sequential(sK8_skl(sK10_skl,sK9_skl),sK9_skl)|~edge(sK8_skl(sK10_skl,sK9_skl))|~edge(sK9_skl)|sK8_skl(sK10_skl,sK9_skl)=sK9_skl),
% 4.43/1.10 inference(resolution,[status(thm)],[f357,f67])).
% 4.43/1.10 fof(f387,plain,(
% 4.43/1.10 sequential(sK8_skl(sK10_skl,sK9_skl),sK9_skl)|~edge(sK9_skl)|sK8_skl(sK10_skl,sK9_skl)=sK9_skl),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f379,f355])).
% 4.43/1.10 fof(f395,plain,(
% 4.43/1.10 ~tail_of(sK9_skl)=head_of(sK10_skl)),
% 4.43/1.10 inference(forward_demodulation,[status(thm)],[f357,f378])).
% 4.43/1.10 fof(f1103,plain,(
% 4.43/1.10 sequential(sK10_skl,sK8_skl(sK10_skl,sK9_skl))|sK10_skl=sK8_skl(sK10_skl,sK9_skl)),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f376,f355])).
% 4.43/1.10 fof(f1105,plain,(
% 4.43/1.10 ![X0]: (sK10_skl=sK8_skl(sK10_skl,sK9_skl)|triangle(X0,sK10_skl,sK8_skl(sK10_skl,sK9_skl))|~sequential(X0,sK10_skl)|~sequential(sK8_skl(sK10_skl,sK9_skl),X0))),
% 4.43/1.10 inference(resolution,[status(thm)],[f1103,f204])).
% 4.43/1.10 fof(f1145,plain,(
% 4.43/1.10 sequential(sK8_skl(sK10_skl,sK9_skl),sK9_skl)|sK8_skl(sK10_skl,sK9_skl)=sK9_skl),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f387,f151])).
% 4.43/1.10 fof(f3175,plain,(
% 4.43/1.10 sK10_skl=sK8_skl(sK10_skl,sK9_skl)|triangle(sK9_skl,sK10_skl,sK8_skl(sK10_skl,sK9_skl))|~sequential(sK9_skl,sK10_skl)|sK8_skl(sK10_skl,sK9_skl)=sK9_skl),
% 4.43/1.10 inference(resolution,[status(thm)],[f1105,f1145])).
% 4.43/1.10 fof(f3176,plain,(
% 4.43/1.10 sK10_skl=sK8_skl(sK10_skl,sK9_skl)|~sequential(sK9_skl,sK10_skl)|sK8_skl(sK10_skl,sK9_skl)=sK9_skl),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f3175,f130])).
% 4.43/1.10 fof(f3544,plain,(
% 4.43/1.10 sK10_skl=sK8_skl(sK10_skl,sK9_skl)|sK8_skl(sK10_skl,sK9_skl)=sK9_skl),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f3176,f129])).
% 4.43/1.10 fof(f3579,plain,(
% 4.43/1.10 head_of(sK10_skl)=tail_of(sK9_skl)|sK8_skl(sK10_skl,sK9_skl)=sK9_skl),
% 4.43/1.10 inference(paramodulation,[status(thm)],[f3544,f357])).
% 4.43/1.10 fof(f3588,plain,(
% 4.43/1.10 sK8_skl(sK10_skl,sK9_skl)=sK9_skl),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f3579,f395])).
% 4.43/1.10 fof(f3636,plain,(
% 4.43/1.10 tail_of(sK9_skl)=head_of(sK10_skl)),
% 4.43/1.10 inference(backward_demodulation,[status(thm)],[f3588,f356])).
% 4.43/1.10 fof(f3677,plain,(
% 4.43/1.10 $false),
% 4.43/1.10 inference(forward_subsumption_resolution,[status(thm)],[f3636,f395])).
% 4.43/1.10 % SZS output end CNFRefutation for theBenchmark.p
% 3.86/1.14 % Elapsed time: 0.704076 seconds
% 3.86/1.14 % CPU time: 5.324956 seconds
% 3.86/1.14 % Total memory used: 162.803 MB
% 3.86/1.14 % Net memory used: 157.873 MB
%------------------------------------------------------------------------------