%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRA010+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:02 PM UTC 2026
% Result : Theorem 0.11s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA010+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n018.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 20 18:25:28 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 0.11/0.41 % Refutation found
% 0.11/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.41 fof(f16,axiom,(
% 0.11/0.41 (! [P,V1,V2] :( ( path(V1,V2,P)& (! [E1,E2] :( ( on_path(E1,P)& on_path(E2,P)& sequential(E1,E2) )=> (? [E3] : triangle(E1,E2,E3) )) ))=> number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) )),
% 0.11/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.41 fof(f18,conjecture,(
% 0.11/0.41 ( complete=> (! [P,V1,V2] :( ( path(V1,V2,P)& (! [E1,E2] :( ( on_path(E1,P)& on_path(E2,P)& sequential(E1,E2) )=> (? [E3] : triangle(E1,E2,E3) )) ))=> number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) )) ),
% 0.11/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.41 fof(f19,negated_conjecture,(
% 0.11/0.41 ~(( complete=> (! [P,V1,V2] :( ( path(V1,V2,P)& (! [E1,E2] :( ( on_path(E1,P)& on_path(E2,P)& sequential(E1,E2) )=> (? [E3] : triangle(E1,E2,E3) )) ))=> number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) )) )),
% 0.11/0.41 inference(negated_conjecture,[status(cth)],[f18])).
% 0.11/0.41 fof(f108,plain,(
% 0.11/0.41 ![P,V1,V2]: ((~path(V1,V2,P)|(?[E1,E2]: (((on_path(E1,P)&on_path(E2,P))&sequential(E1,E2))&(![E3]: ~triangle(E1,E2,E3)))))|number_of_in(sequential_pairs,P)=number_of_in(triangles,P))),
% 0.11/0.41 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.11/0.41 fof(f109,plain,(
% 0.11/0.41 ![P]: (((![V1,V2]: ~path(V1,V2,P))|(?[E1,E2]: (((on_path(E1,P)&on_path(E2,P))&sequential(E1,E2))&(![E3]: ~triangle(E1,E2,E3)))))|number_of_in(sequential_pairs,P)=number_of_in(triangles,P))),
% 0.11/0.41 inference(miniscoping,[status(thm)],[f108])).
% 0.11/0.41 fof(f110,plain,(
% 0.11/0.41 ![P]: (((![V1,V2]: ~path(V1,V2,P))|(((on_path(sK6_skl(P),P)&on_path(sK7_skl(P),P))&sequential(sK6_skl(P),sK7_skl(P)))&(![E3]: ~triangle(sK6_skl(P),sK7_skl(P),E3))))|number_of_in(sequential_pairs,P)=number_of_in(triangles,P))),
% 0.11/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(E1,sK6_skl(P)),skolemize(E2,sK7_skl(P))],[f109])).
% 0.11/0.41 fof(f111,plain,(
% 0.11/0.41 ![X0,X1,X2]: (~path(X0,X1,X2)|on_path(sK6_skl(X2),X2)|number_of_in(sequential_pairs,X2)=number_of_in(triangles,X2))),
% 0.11/0.41 inference(cnf_transformation,[status(thm)],[f110])).
% 0.11/0.41 fof(f112,plain,(
% 0.11/0.41 ![X0,X1,X2]: (~path(X0,X1,X2)|on_path(sK7_skl(X2),X2)|number_of_in(sequential_pairs,X2)=number_of_in(triangles,X2))),
% 0.11/0.41 inference(cnf_transformation,[status(thm)],[f110])).
% 0.11/0.41 fof(f113,plain,(
% 0.11/0.41 ![X0,X1,X2]: (~path(X0,X1,X2)|sequential(sK6_skl(X2),sK7_skl(X2))|number_of_in(sequential_pairs,X2)=number_of_in(triangles,X2))),
% 0.11/0.41 inference(cnf_transformation,[status(thm)],[f110])).
% 0.11/0.41 fof(f114,plain,(
% 0.11/0.41 ![X0,X1,X2,X3]: (~path(X0,X1,X2)|~triangle(sK6_skl(X2),sK7_skl(X2),X3)|number_of_in(sequential_pairs,X2)=number_of_in(triangles,X2))),
% 0.11/0.41 inference(cnf_transformation,[status(thm)],[f110])).
% 0.11/0.41 fof(f116,plain,(
% 0.11/0.41 (complete&(?[P,V1,V2]: ((path(V1,V2,P)&(![E1,E2]: (((~on_path(E1,P)|~on_path(E2,P))|~sequential(E1,E2))|(?[E3]: triangle(E1,E2,E3)))))&~number_of_in(sequential_pairs,P)=number_of_in(triangles,P))))),
% 0.11/0.41 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.11/0.41 fof(f117,plain,(
% 0.11/0.41 complete&(?[P]: (((?[V1,V2]: path(V1,V2,P))&(![E1,E2]: (((~on_path(E1,P)|~on_path(E2,P))|~sequential(E1,E2))|(?[E3]: triangle(E1,E2,E3)))))&~number_of_in(sequential_pairs,P)=number_of_in(triangles,P)))),
% 0.11/0.41 inference(miniscoping,[status(thm)],[f116])).
% 0.11/0.41 fof(f118,plain,(
% 0.11/0.41 complete&((path(sK9_skl,sK10_skl,sK8_skl)&(![E1,E2]: (((~on_path(E1,sK8_skl)|~on_path(E2,sK8_skl))|~sequential(E1,E2))|triangle(E1,E2,sK11_skl(E2,E1)))))&~number_of_in(sequential_pairs,sK8_skl)=number_of_in(triangles,sK8_skl))),
% 0.11/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl,sK11_skl]),skolemize(P,sK8_skl),skolemize(V1,sK9_skl),skolemize(V2,sK10_skl),skolemize(E3,sK11_skl(E2,E1))],[f117])).
% 0.11/0.41 fof(f120,plain,(
% 0.11/0.41 path(sK9_skl,sK10_skl,sK8_skl)),
% 0.11/0.41 inference(cnf_transformation,[status(thm)],[f118])).
% 0.11/0.41 fof(f121,plain,(
% 0.11/0.41 ![X0,X1]: (~on_path(X0,sK8_skl)|~on_path(X1,sK8_skl)|~sequential(X0,X1)|triangle(X0,X1,sK11_skl(X1,X0)))),
% 0.11/0.41 inference(cnf_transformation,[status(thm)],[f118])).
% 0.11/0.41 fof(f122,plain,(
% 0.11/0.41 ~number_of_in(sequential_pairs,sK8_skl)=number_of_in(triangles,sK8_skl)),
% 0.11/0.41 inference(cnf_transformation,[status(thm)],[f118])).
% 0.11/0.41 fof(f151,plain,(
% 0.11/0.41 on_path(sK6_skl(sK8_skl),sK8_skl)|number_of_in(sequential_pairs,sK8_skl)=number_of_in(triangles,sK8_skl)),
% 0.11/0.41 inference(resolution,[status(thm)],[f111,f120])).
% 0.11/0.41 fof(f152,plain,(
% 0.11/0.41 on_path(sK6_skl(sK8_skl),sK8_skl)),
% 0.11/0.41 inference(forward_subsumption_resolution,[status(thm)],[f151,f122])).
% 0.11/0.41 fof(f153,plain,(
% 0.11/0.41 on_path(sK7_skl(sK8_skl),sK8_skl)|number_of_in(sequential_pairs,sK8_skl)=number_of_in(triangles,sK8_skl)),
% 0.11/0.41 inference(resolution,[status(thm)],[f112,f120])).
% 0.11/0.41 fof(f154,plain,(
% 0.11/0.41 on_path(sK7_skl(sK8_skl),sK8_skl)),
% 0.11/0.41 inference(forward_subsumption_resolution,[status(thm)],[f153,f122])).
% 0.11/0.41 fof(f155,plain,(
% 0.11/0.41 sequential(sK6_skl(sK8_skl),sK7_skl(sK8_skl))|number_of_in(sequential_pairs,sK8_skl)=number_of_in(triangles,sK8_skl)),
% 0.11/0.41 inference(resolution,[status(thm)],[f113,f120])).
% 0.11/0.41 fof(f156,plain,(
% 0.11/0.41 sequential(sK6_skl(sK8_skl),sK7_skl(sK8_skl))),
% 0.11/0.41 inference(forward_subsumption_resolution,[status(thm)],[f155,f122])).
% 0.11/0.41 fof(f164,plain,(
% 0.11/0.41 ![X0]: (~on_path(X0,sK8_skl)|~sequential(X0,sK7_skl(sK8_skl))|triangle(X0,sK7_skl(sK8_skl),sK11_skl(sK7_skl(sK8_skl),X0)))),
% 0.11/0.41 inference(resolution,[status(thm)],[f154,f121])).
% 0.11/0.41 fof(f179,plain,(
% 0.11/0.41 ~on_path(sK6_skl(sK8_skl),sK8_skl)|triangle(sK6_skl(sK8_skl),sK7_skl(sK8_skl),sK11_skl(sK7_skl(sK8_skl),sK6_skl(sK8_skl)))),
% 0.11/0.41 inference(resolution,[status(thm)],[f164,f156])).
% 0.11/0.41 fof(f180,plain,(
% 0.11/0.41 triangle(sK6_skl(sK8_skl),sK7_skl(sK8_skl),sK11_skl(sK7_skl(sK8_skl),sK6_skl(sK8_skl)))),
% 0.11/0.41 inference(forward_subsumption_resolution,[status(thm)],[f179,f152])).
% 0.11/0.41 fof(f225,plain,(
% 0.11/0.41 ![X0,X1]: (~path(X0,X1,sK8_skl)|number_of_in(sequential_pairs,sK8_skl)=number_of_in(triangles,sK8_skl))),
% 0.11/0.41 inference(resolution,[status(thm)],[f180,f114])).
% 0.11/0.41 fof(f233,plain,(
% 0.11/0.41 ![X0,X1]: (~path(X0,X1,sK8_skl))),
% 0.11/0.41 inference(forward_subsumption_resolution,[status(thm)],[f225,f122])).
% 0.11/0.41 fof(f234,plain,(
% 0.11/0.41 $false),
% 0.11/0.41 inference(backward_subsumption_resolution,[status(thm)],[f120,f233])).
% 0.11/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/0.44 % Elapsed time: 0.064747 seconds
% 0.11/0.44 % CPU time: 0.227345 seconds
% 0.11/0.44 % Total memory used: 57.233 MB
% 0.11/0.44 % Net memory used: 57.107 MB
%------------------------------------------------------------------------------