%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRA010+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 : n016.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.15s 5.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA010+2 : 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.09/5.37 % Computer : n016.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Sun Sep 20 18:25:58 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.39 % Drodi V4.1.1
% 0.15/5.47 % Refutation found
% 0.15/5.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/5.47 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.47 fof(f16,axiom,(
% 0.15/5.47 (! [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.15/5.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.47 fof(f19,conjecture,(
% 0.15/5.47 ( 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.15/5.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.47 fof(f20,negated_conjecture,(
% 0.15/5.47 ~(( 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.15/5.47 inference(negated_conjecture,[status(cth)],[f19])).
% 0.15/5.47 fof(f109,plain,(
% 0.15/5.47 ![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.15/5.47 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.15/5.47 fof(f110,plain,(
% 0.15/5.47 ![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.15/5.47 inference(miniscoping,[status(thm)],[f109])).
% 0.15/5.47 fof(f111,plain,(
% 0.15/5.47 ![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.15/5.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(E1,sK6_skl(P)),skolemize(E2,sK7_skl(P))],[f110])).
% 0.15/5.47 fof(f112,plain,(
% 0.15/5.47 ![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.15/5.47 inference(cnf_transformation,[status(thm)],[f111])).
% 0.15/5.47 fof(f113,plain,(
% 0.15/5.47 ![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.15/5.47 inference(cnf_transformation,[status(thm)],[f111])).
% 0.15/5.47 fof(f114,plain,(
% 0.15/5.47 ![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.15/5.47 inference(cnf_transformation,[status(thm)],[f111])).
% 0.15/5.47 fof(f115,plain,(
% 0.15/5.47 ![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.15/5.47 inference(cnf_transformation,[status(thm)],[f111])).
% 0.15/5.47 fof(f121,plain,(
% 0.15/5.47 (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.15/5.47 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.15/5.47 fof(f122,plain,(
% 0.15/5.47 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.15/5.47 inference(miniscoping,[status(thm)],[f121])).
% 0.15/5.47 fof(f123,plain,(
% 0.15/5.47 complete&((path(sK10_skl,sK11_skl,sK9_skl)&(![E1,E2]: (((~on_path(E1,sK9_skl)|~on_path(E2,sK9_skl))|~sequential(E1,E2))|triangle(E1,E2,sK12_skl(E2,E1)))))&~number_of_in(sequential_pairs,sK9_skl)=number_of_in(triangles,sK9_skl))),
% 0.15/5.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl]),skolemize(P,sK9_skl),skolemize(V1,sK10_skl),skolemize(V2,sK11_skl),skolemize(E3,sK12_skl(E2,E1))],[f122])).
% 0.15/5.47 fof(f125,plain,(
% 0.15/5.47 path(sK10_skl,sK11_skl,sK9_skl)),
% 0.15/5.47 inference(cnf_transformation,[status(thm)],[f123])).
% 0.15/5.47 fof(f126,plain,(
% 0.15/5.47 ![X0,X1]: (~on_path(X0,sK9_skl)|~on_path(X1,sK9_skl)|~sequential(X0,X1)|triangle(X0,X1,sK12_skl(X1,X0)))),
% 0.15/5.47 inference(cnf_transformation,[status(thm)],[f123])).
% 0.15/5.47 fof(f127,plain,(
% 0.15/5.47 ~number_of_in(sequential_pairs,sK9_skl)=number_of_in(triangles,sK9_skl)),
% 0.15/5.48 inference(cnf_transformation,[status(thm)],[f123])).
% 0.15/5.48 fof(f259,plain,(
% 0.15/5.48 on_path(sK6_skl(sK9_skl),sK9_skl)|number_of_in(sequential_pairs,sK9_skl)=number_of_in(triangles,sK9_skl)),
% 0.15/5.48 inference(resolution,[status(thm)],[f112,f125])).
% 0.15/5.48 fof(f260,plain,(
% 0.15/5.48 on_path(sK6_skl(sK9_skl),sK9_skl)),
% 0.15/5.48 inference(forward_subsumption_resolution,[status(thm)],[f259,f127])).
% 0.15/5.48 fof(f263,plain,(
% 0.15/5.48 on_path(sK7_skl(sK9_skl),sK9_skl)|number_of_in(sequential_pairs,sK9_skl)=number_of_in(triangles,sK9_skl)),
% 0.15/5.48 inference(resolution,[status(thm)],[f113,f125])).
% 0.15/5.48 fof(f264,plain,(
% 0.15/5.48 on_path(sK7_skl(sK9_skl),sK9_skl)),
% 0.15/5.48 inference(forward_subsumption_resolution,[status(thm)],[f263,f127])).
% 0.15/5.48 fof(f304,plain,(
% 0.15/5.48 sequential(sK6_skl(sK9_skl),sK7_skl(sK9_skl))|number_of_in(sequential_pairs,sK9_skl)=number_of_in(triangles,sK9_skl)),
% 0.15/5.48 inference(resolution,[status(thm)],[f114,f125])).
% 0.15/5.48 fof(f305,plain,(
% 0.15/5.48 sequential(sK6_skl(sK9_skl),sK7_skl(sK9_skl))),
% 0.15/5.48 inference(forward_subsumption_resolution,[status(thm)],[f304,f127])).
% 0.15/5.48 fof(f316,plain,(
% 0.15/5.48 ~on_path(sK6_skl(sK9_skl),sK9_skl)|~on_path(sK7_skl(sK9_skl),sK9_skl)|triangle(sK6_skl(sK9_skl),sK7_skl(sK9_skl),sK12_skl(sK7_skl(sK9_skl),sK6_skl(sK9_skl)))),
% 0.15/5.48 inference(resolution,[status(thm)],[f305,f126])).
% 0.15/5.48 fof(f320,plain,(
% 0.15/5.48 ~on_path(sK7_skl(sK9_skl),sK9_skl)|triangle(sK6_skl(sK9_skl),sK7_skl(sK9_skl),sK12_skl(sK7_skl(sK9_skl),sK6_skl(sK9_skl)))),
% 0.15/5.48 inference(forward_subsumption_resolution,[status(thm)],[f316,f260])).
% 0.15/5.48 fof(f667,plain,(
% 0.15/5.48 triangle(sK6_skl(sK9_skl),sK7_skl(sK9_skl),sK12_skl(sK7_skl(sK9_skl),sK6_skl(sK9_skl)))),
% 0.15/5.48 inference(forward_subsumption_resolution,[status(thm)],[f320,f264])).
% 0.15/5.48 fof(f668,plain,(
% 0.15/5.48 ![X0,X1]: (~path(X0,X1,sK9_skl)|number_of_in(sequential_pairs,sK9_skl)=number_of_in(triangles,sK9_skl))),
% 0.15/5.48 inference(resolution,[status(thm)],[f667,f115])).
% 0.15/5.48 fof(f675,plain,(
% 0.15/5.48 ![X0,X1]: (~path(X0,X1,sK9_skl))),
% 0.15/5.48 inference(forward_subsumption_resolution,[status(thm)],[f668,f127])).
% 0.15/5.48 fof(f713,plain,(
% 0.15/5.48 $false),
% 0.15/5.48 inference(backward_subsumption_resolution,[status(thm)],[f125,f675])).
% 0.15/5.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/5.50 % Elapsed time: 0.110865 seconds
% 0.15/5.50 % CPU time: 0.678723 seconds
% 0.15/5.50 % Total memory used: 92.093 MB
% 0.15/5.50 % Net memory used: 91.489 MB
%------------------------------------------------------------------------------