%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRA004+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 : n009.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.15s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA004+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.37 % Computer : n009.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 18:17:42 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 0.15/0.42 % Refutation found
% 0.15/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.42 fof(f6,axiom,(
% 0.15/0.42 (! [V1,V2,P,E] :( ( path(V1,V2,P)& on_path(E,P) )=> ( edge(E)& in_path(head_of(E),P)& in_path(tail_of(E),P) ) ) )),
% 0.15/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.42 fof(f8,axiom,(
% 0.15/0.42 (! [E1,E2] :( sequential(E1,E2)<=> ( edge(E1)& edge(E2)& E1 != E2& head_of(E1) = tail_of(E2) ) ) )),
% 0.15/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.42 fof(f9,axiom,(
% 0.15/0.42 (! [P,V1,V2] :( path(V1,V2,P)=> (! [E1,E2] :( precedes(E1,E2,P)<= ( on_path(E1,P)& on_path(E2,P)& ( sequential(E1,E2)| (? [E3] :( sequential(E1,E3)& precedes(E3,E2,P) ) )) ) ) )) )),
% 0.15/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.42 fof(f10,axiom,(
% 0.15/0.42 (! [P,V1,V2] :( path(V1,V2,P)=> (! [E1,E2] :( precedes(E1,E2,P)=> ( on_path(E1,P)& on_path(E2,P)& ( sequential(E1,E2)<~> (? [E3] :( sequential(E1,E3)& precedes(E3,E2,P) ) )) ) ) )) )),
% 0.15/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.42 fof(f11,axiom,(
% 0.15/0.42 (! [V1,V2,SP] :( shortest_path(V1,V2,SP)<=> ( path(V1,V2,SP)& V1 != V2& (! [P] :( path(V1,V2,P)=> less_or_equal(length_of(SP),length_of(P)) ) )) ) )),
% 0.15/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.42 fof(f12,axiom,(
% 0.15/0.42 (! [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.15/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.42 fof(f18,conjecture,(
% 0.15/0.42 (! [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) ))& head_of(E2) != tail_of(E1)& head_of(E2) != head_of(E1) ) ) )),
% 0.15/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.42 fof(f19,negated_conjecture,(
% 0.15/0.42 ~((! [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) ))& head_of(E2) != tail_of(E1)& head_of(E2) != head_of(E1) ) ) ))),
% 0.15/0.42 inference(negated_conjecture,[status(cth)],[f18])).
% 0.15/0.42 fof(f49,plain,(
% 0.15/0.42 ![V1,V2,P,E]: ((~path(V1,V2,P)|~on_path(E,P))|((edge(E)&in_path(head_of(E),P))&in_path(tail_of(E),P)))),
% 0.15/0.42 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.15/0.42 fof(f50,plain,(
% 0.15/0.42 ![P,E]: (((![V1,V2]: ~path(V1,V2,P))|~on_path(E,P))|((edge(E)&in_path(head_of(E),P))&in_path(tail_of(E),P)))),
% 0.15/0.42 inference(miniscoping,[status(thm)],[f49])).
% 0.15/0.42 fof(f51,plain,(
% 0.15/0.42 ![X0,X1,X2,X3]: (~path(X0,X1,X2)|~on_path(X3,X2)|edge(X3))),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f50])).
% 0.15/0.42 fof(f60,plain,(
% 0.15/0.42 ![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))))),
% 0.15/0.42 inference(NNF_transformation,[status(thm)],[f8])).
% 0.15/0.42 fof(f61,plain,(
% 0.15/0.42 (![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))))),
% 0.15/0.42 inference(miniscoping,[status(thm)],[f60])).
% 0.15/0.42 fof(f66,plain,(
% 0.15/0.42 ![X0,X1]: (sequential(X0,X1)|~edge(X0)|~edge(X1)|X0=X1|~head_of(X0)=tail_of(X1))),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f61])).
% 0.15/0.42 fof(f67,plain,(
% 0.15/0.42 ![P,V1,V2]: (~path(V1,V2,P)|(![E1,E2]: (precedes(E1,E2,P)|((~on_path(E1,P)|~on_path(E2,P))|(~sequential(E1,E2)&(![E3]: (~sequential(E1,E3)|~precedes(E3,E2,P))))))))),
% 0.15/0.42 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.15/0.42 fof(f68,plain,(
% 0.15/0.42 ![P]: ((![V1,V2]: ~path(V1,V2,P))|(![E1,E2]: (precedes(E1,E2,P)|((~on_path(E1,P)|~on_path(E2,P))|(~sequential(E1,E2)&(![E3]: (~sequential(E1,E3)|~precedes(E3,E2,P))))))))),
% 0.15/0.42 inference(miniscoping,[status(thm)],[f67])).
% 0.15/0.42 fof(f69,plain,(
% 0.15/0.42 ![X0,X1,X2,X3,X4]: (~path(X0,X1,X2)|precedes(X3,X4,X2)|~on_path(X3,X2)|~on_path(X4,X2)|~sequential(X3,X4))),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f68])).
% 0.15/0.42 fof(f71,plain,(
% 0.15/0.42 ![P,V1,V2]: (~path(V1,V2,P)|(![E1,E2]: (~precedes(E1,E2,P)|((on_path(E1,P)&on_path(E2,P))&(sequential(E1,E2)<~>(?[E3]: (sequential(E1,E3)&precedes(E3,E2,P))))))))),
% 0.15/0.42 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.15/0.42 fof(f72,plain,(
% 0.15/0.42 ![P,V1,V2]: (~path(V1,V2,P)|(![E1,E2]: (~precedes(E1,E2,P)|((on_path(E1,P)&on_path(E2,P))&((sequential(E1,E2)|(?[E3]: (sequential(E1,E3)&precedes(E3,E2,P))))&(~sequential(E1,E2)|(![E3]: (~sequential(E1,E3)|~precedes(E3,E2,P)))))))))),
% 0.15/0.42 inference(NNF_transformation,[status(thm)],[f71])).
% 0.15/0.42 fof(f73,plain,(
% 0.15/0.42 ![P]: ((![V1,V2]: ~path(V1,V2,P))|(![E1,E2]: (~precedes(E1,E2,P)|((on_path(E1,P)&on_path(E2,P))&((sequential(E1,E2)|(?[E3]: (sequential(E1,E3)&precedes(E3,E2,P))))&(~sequential(E1,E2)|(![E3]: (~sequential(E1,E3)|~precedes(E3,E2,P)))))))))),
% 0.15/0.42 inference(miniscoping,[status(thm)],[f72])).
% 0.15/0.42 fof(f74,plain,(
% 0.15/0.42 ![P]: ((![V1,V2]: ~path(V1,V2,P))|(![E1,E2]: (~precedes(E1,E2,P)|((on_path(E1,P)&on_path(E2,P))&((sequential(E1,E2)|(sequential(E1,sK4_skl(E2,E1,P))&precedes(sK4_skl(E2,E1,P),E2,P)))&(~sequential(E1,E2)|(![E3]: (~sequential(E1,E3)|~precedes(E3,E2,P)))))))))),
% 0.15/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(E3,sK4_skl(E2,E1,P))],[f73])).
% 0.15/0.42 fof(f75,plain,(
% 0.15/0.42 ![X0,X1,X2,X3,X4]: (~path(X0,X1,X2)|~precedes(X3,X4,X2)|on_path(X3,X2))),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f74])).
% 0.15/0.42 fof(f76,plain,(
% 0.15/0.42 ![X0,X1,X2,X3,X4]: (~path(X0,X1,X2)|~precedes(X3,X4,X2)|on_path(X4,X2))),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f74])).
% 0.15/0.42 fof(f80,plain,(
% 0.15/0.42 ![V1,V2,SP]: (shortest_path(V1,V2,SP)<=>((path(V1,V2,SP)&~V1=V2)&(![P]: (~path(V1,V2,P)|less_or_equal(length_of(SP),length_of(P))))))),
% 0.15/0.42 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.15/0.42 fof(f81,plain,(
% 0.15/0.42 ![V1,V2,SP]: ((~shortest_path(V1,V2,SP)|((path(V1,V2,SP)&~V1=V2)&(![P]: (~path(V1,V2,P)|less_or_equal(length_of(SP),length_of(P))))))&(shortest_path(V1,V2,SP)|((~path(V1,V2,SP)|V1=V2)|(?[P]: (path(V1,V2,P)&~less_or_equal(length_of(SP),length_of(P)))))))),
% 0.15/0.42 inference(NNF_transformation,[status(thm)],[f80])).
% 0.15/0.42 fof(f82,plain,(
% 0.15/0.42 (![V1,V2,SP]: (~shortest_path(V1,V2,SP)|((path(V1,V2,SP)&~V1=V2)&(![P]: (~path(V1,V2,P)|less_or_equal(length_of(SP),length_of(P)))))))&(![V1,V2,SP]: (shortest_path(V1,V2,SP)|((~path(V1,V2,SP)|V1=V2)|(?[P]: (path(V1,V2,P)&~less_or_equal(length_of(SP),length_of(P)))))))),
% 0.15/0.42 inference(miniscoping,[status(thm)],[f81])).
% 0.15/0.42 fof(f83,plain,(
% 0.15/0.42 (![V1,V2,SP]: (~shortest_path(V1,V2,SP)|((path(V1,V2,SP)&~V1=V2)&(![P]: (~path(V1,V2,P)|less_or_equal(length_of(SP),length_of(P)))))))&(![V1,V2,SP]: (shortest_path(V1,V2,SP)|((~path(V1,V2,SP)|V1=V2)|(path(V1,V2,sK5_skl(SP,V2,V1))&~less_or_equal(length_of(SP),length_of(sK5_skl(SP,V2,V1)))))))),
% 0.15/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(P,sK5_skl(SP,V2,V1))],[f82])).
% 0.15/0.42 fof(f84,plain,(
% 0.15/0.42 ![X0,X1,X2]: (~shortest_path(X0,X1,X2)|path(X0,X1,X2))),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f83])).
% 0.15/0.42 fof(f89,plain,(
% 0.15/0.42 ![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.15/0.42 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.15/0.42 fof(f90,plain,(
% 0.15/0.42 ![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.15/0.42 inference(miniscoping,[status(thm)],[f89])).
% 0.15/0.42 fof(f91,plain,(
% 0.15/0.42 ![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.15/0.42 inference(cnf_transformation,[status(thm)],[f90])).
% 0.15/0.42 fof(f92,plain,(
% 0.15/0.42 ![X0,X1,X2,X3,X4]: (~shortest_path(X0,X1,X2)|~precedes(X3,X4,X2)|~precedes(X4,X3,X2))),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f90])).
% 0.15/0.42 fof(f116,plain,(
% 0.15/0.42 (?[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)))|head_of(E2)=tail_of(E1))|head_of(E2)=head_of(E1))))),
% 0.15/0.42 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.15/0.42 fof(f117,plain,(
% 0.15/0.42 ?[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)))|head_of(E2)=tail_of(E1))|head_of(E2)=head_of(E1)))),
% 0.15/0.42 inference(miniscoping,[status(thm)],[f116])).
% 0.15/0.42 fof(f118,plain,(
% 0.15/0.42 ((shortest_path(sK11_skl,sK12_skl,sK10_skl)&precedes(sK8_skl,sK9_skl,sK10_skl))&(((tail_of(sK13_skl)=tail_of(sK8_skl)&head_of(sK13_skl)=head_of(sK9_skl))|head_of(sK9_skl)=tail_of(sK8_skl))|head_of(sK9_skl)=head_of(sK8_skl)))),
% 0.15/0.42 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.15/0.42 fof(f119,plain,(
% 0.15/0.42 shortest_path(sK11_skl,sK12_skl,sK10_skl)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f118])).
% 0.15/0.42 fof(f120,plain,(
% 0.15/0.42 precedes(sK8_skl,sK9_skl,sK10_skl)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f118])).
% 0.15/0.42 fof(f121,plain,(
% 0.15/0.42 tail_of(sK13_skl)=tail_of(sK8_skl)|head_of(sK9_skl)=tail_of(sK8_skl)|head_of(sK9_skl)=head_of(sK8_skl)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f118])).
% 0.15/0.42 fof(f122,plain,(
% 0.15/0.42 head_of(sK13_skl)=head_of(sK9_skl)|head_of(sK9_skl)=tail_of(sK8_skl)|head_of(sK9_skl)=head_of(sK8_skl)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f118])).
% 0.15/0.43 fof(f152,definition,(
% 0.15/0.43 sQ5_spl <=> (tail_of(sK13_skl)=tail_of(sK8_skl))),
% 0.15/0.43 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.15/0.43 fof(f153,plain,(
% 0.15/0.43 tail_of(sK13_skl)=tail_of(sK8_skl)|~sQ5_spl),
% 0.15/0.43 inference(component_clause,[status(thm)],[f152])).
% 0.15/0.43 fof(f155,definition,(
% 0.15/0.43 sQ6_spl <=> (head_of(sK9_skl)=tail_of(sK8_skl))),
% 0.15/0.43 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/0.43 fof(f156,plain,(
% 0.15/0.43 head_of(sK9_skl)=tail_of(sK8_skl)|~sQ6_spl),
% 0.15/0.43 inference(component_clause,[status(thm)],[f155])).
% 0.15/0.43 fof(f158,definition,(
% 0.15/0.43 sQ7_spl <=> (head_of(sK9_skl)=head_of(sK8_skl))),
% 0.15/0.43 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/0.43 fof(f159,plain,(
% 0.15/0.43 head_of(sK9_skl)=head_of(sK8_skl)|~sQ7_spl),
% 0.15/0.43 inference(component_clause,[status(thm)],[f158])).
% 0.15/0.43 fof(f161,plain,(
% 0.15/0.43 sQ5_spl|sQ6_spl|sQ7_spl),
% 0.15/0.43 inference(split_clause,[status(thm)],[f121,f152,f155,f158])).
% 0.15/0.43 fof(f162,definition,(
% 0.15/0.43 sQ8_spl <=> (head_of(sK13_skl)=head_of(sK9_skl))),
% 0.15/0.43 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/0.43 fof(f165,plain,(
% 0.15/0.43 sQ8_spl|sQ6_spl|sQ7_spl),
% 0.15/0.43 inference(split_clause,[status(thm)],[f122,f162,f155,f158])).
% 0.15/0.43 fof(f181,definition,(
% 0.15/0.43 ![X0,X1]: (sQ9_spl <=> (~path(X0,X1,sK10_skl)))),
% 0.15/0.43 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.15/0.43 fof(f182,plain,(
% 0.15/0.43 ![X0,X1]: (~path(X0,X1,sK10_skl)|~sQ9_spl)),
% 0.15/0.43 inference(component_clause,[status(thm)],[f181])).
% 0.15/0.43 fof(f199,plain,(
% 0.15/0.43 path(sK11_skl,sK12_skl,sK10_skl)),
% 0.15/0.43 inference(resolution,[status(thm)],[f84,f119])).
% 0.15/0.43 fof(f200,plain,(
% 0.15/0.43 $false|~sQ9_spl),
% 0.15/0.43 inference(forward_subsumption_resolution,[status(thm)],[f199,f182])).
% 0.15/0.43 fof(f201,plain,(
% 0.15/0.43 ~sQ9_spl),
% 0.15/0.43 inference(contradiction_clause,[status(thm)],[f200])).
% 0.15/0.43 fof(f202,plain,(
% 0.15/0.43 ![X0,X1,X2]: (~precedes(X0,X1,sK10_skl)|~tail_of(X2)=tail_of(X0)|~head_of(X2)=head_of(X1))),
% 0.15/0.43 inference(resolution,[status(thm)],[f91,f119])).
% 0.15/0.43 fof(f203,plain,(
% 0.15/0.43 ![X0,X1]: (~precedes(X0,X1,sK10_skl)|~precedes(X1,X0,sK10_skl))),
% 0.15/0.43 inference(resolution,[status(thm)],[f92,f119])).
% 0.15/0.43 fof(f211,definition,(
% 0.15/0.43 sQ16_spl <=> (edge(sK9_skl))),
% 0.15/0.43 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.15/0.43 fof(f213,plain,(
% 0.15/0.43 ~edge(sK9_skl)|sQ16_spl),
% 0.15/0.43 inference(component_clause,[status(thm)],[f211])).
% 0.15/0.43 fof(f216,definition,(
% 0.15/0.43 sQ17_spl <=> (edge(sK8_skl))),
% 0.15/0.43 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.15/0.43 fof(f218,plain,(
% 0.15/0.43 ~edge(sK8_skl)|sQ17_spl),
% 0.15/0.43 inference(component_clause,[status(thm)],[f216])).
% 0.15/0.43 fof(f240,plain,(
% 0.15/0.43 ![X0]: (~on_path(X0,sK10_skl)|edge(X0))),
% 0.15/0.43 inference(resolution,[status(thm)],[f199,f51])).
% 0.15/0.43 fof(f260,plain,(
% 0.15/0.43 ~precedes(sK9_skl,sK8_skl,sK10_skl)),
% 0.15/0.43 inference(resolution,[status(thm)],[f203,f120])).
% 0.15/0.43 fof(f305,plain,(
% 0.15/0.43 sequential(sK9_skl,sK8_skl)|~edge(sK9_skl)|~edge(sK8_skl)|sK9_skl=sK8_skl|~sQ6_spl),
% 0.15/0.43 inference(resolution,[status(thm)],[f66,f156])).
% 0.15/0.43 fof(f307,definition,(
% 0.15/0.43 sQ30_spl <=> (sequential(sK9_skl,sK8_skl))),
% 0.15/0.43 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.15/0.43 fof(f308,plain,(
% 0.15/0.43 sequential(sK9_skl,sK8_skl)|~sQ30_spl),
% 0.15/0.43 inference(component_clause,[status(thm)],[f307])).
% 0.15/0.43 fof(f310,definition,(
% 0.15/0.43 sQ31_spl <=> (sK9_skl=sK8_skl)),
% 0.15/0.43 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.15/0.43 fof(f311,plain,(
% 0.15/0.43 sK9_skl=sK8_skl|~sQ31_spl),
% 0.15/0.43 inference(component_clause,[status(thm)],[f310])).
% 0.15/0.43 fof(f313,plain,(
% 0.15/0.43 sQ30_spl|~sQ16_spl|~sQ17_spl|sQ31_spl|~sQ6_spl),
% 0.15/0.43 inference(split_clause,[status(thm)],[f305,f307,f211,f216,f310,f155])).
% 0.15/0.43 fof(f323,plain,(
% 0.15/0.43 precedes(sK8_skl,sK8_skl,sK10_skl)|~sQ31_spl),
% 0.15/0.43 inference(backward_demodulation,[status(thm)],[f311,f120])).
% 0.15/0.43 fof(f328,plain,(
% 0.15/0.43 ~precedes(sK8_skl,sK8_skl,sK10_skl)|~sQ31_spl),
% 0.15/0.43 inference(backward_demodulation,[status(thm)],[f311,f260])).
% 0.15/0.43 fof(f359,plain,(
% 0.15/0.43 ![X0]: (~tail_of(X0)=tail_of(sK8_skl)|~head_of(X0)=head_of(sK9_skl))),
% 0.15/0.43 inference(resolution,[status(thm)],[f120,f202])).
% 0.15/0.43 fof(f376,plain,(
% 0.15/0.43 ![X0,X1]: (precedes(X0,X1,sK10_skl)|~on_path(X0,sK10_skl)|~on_path(X1,sK10_skl)|~sequential(X0,X1))),
% 0.15/0.43 inference(resolution,[status(thm)],[f69,f199])).
% 0.15/0.43 fof(f377,plain,(
% 0.15/0.43 ![X0,X1]: (~path(X0,X1,sK10_skl)|on_path(sK8_skl,sK10_skl))),
% 0.15/0.43 inference(resolution,[status(thm)],[f75,f120])).
% 0.15/0.43 fof(f378,definition,(
% 0.15/0.43 sQ35_spl <=> (on_path(sK8_skl,sK10_skl))),
% 0.15/0.43 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.15/0.43 fof(f379,plain,(
% 0.15/0.43 on_path(sK8_skl,sK10_skl)|~sQ35_spl),
% 0.15/0.43 inference(component_clause,[status(thm)],[f378])).
% 0.15/0.43 fof(f381,plain,(
% 0.15/0.43 sQ9_spl|sQ35_spl),
% 0.15/0.43 inference(split_clause,[status(thm)],[f377,f181,f378])).
% 0.15/0.43 fof(f382,plain,(
% 0.15/0.43 ![X0,X1]: (~path(X0,X1,sK10_skl)|on_path(sK9_skl,sK10_skl))),
% 0.15/0.43 inference(resolution,[status(thm)],[f76,f120])).
% 0.15/0.43 fof(f383,definition,(
% 0.15/0.43 sQ36_spl <=> (on_path(sK9_skl,sK10_skl))),
% 0.15/0.43 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.15/0.43 fof(f384,plain,(
% 0.15/0.43 on_path(sK9_skl,sK10_skl)|~sQ36_spl),
% 0.15/0.43 inference(component_clause,[status(thm)],[f383])).
% 0.15/0.43 fof(f386,plain,(
% 0.15/0.43 sQ9_spl|sQ36_spl),
% 0.15/0.43 inference(split_clause,[status(thm)],[f382,f181,f383])).
% 0.15/0.43 fof(f390,plain,(
% 0.15/0.43 edge(sK8_skl)|~sQ35_spl),
% 0.15/0.43 inference(resolution,[status(thm)],[f379,f240])).
% 0.15/0.43 fof(f391,plain,(
% 0.15/0.43 $false|sQ17_spl|~sQ35_spl),
% 0.15/0.43 inference(forward_subsumption_resolution,[status(thm)],[f390,f218])).
% 0.15/0.43 fof(f392,plain,(
% 0.15/0.43 sQ17_spl|~sQ35_spl),
% 0.15/0.43 inference(contradiction_clause,[status(thm)],[f391])).
% 0.15/0.43 fof(f404,plain,(
% 0.15/0.43 edge(sK9_skl)|~sQ36_spl),
% 0.15/0.43 inference(resolution,[status(thm)],[f384,f240])).
% 0.15/0.43 fof(f405,plain,(
% 0.15/0.43 $false|sQ16_spl|~sQ36_spl),
% 0.15/0.43 inference(forward_subsumption_resolution,[status(thm)],[f404,f213])).
% 0.15/0.43 fof(f406,plain,(
% 0.15/0.43 sQ16_spl|~sQ36_spl),
% 0.15/0.43 inference(contradiction_clause,[status(thm)],[f405])).
% 0.15/0.43 fof(f593,plain,(
% 0.15/0.43 ~head_of(sK13_skl)=head_of(sK9_skl)|~sQ5_spl),
% 0.15/0.43 inference(resolution,[status(thm)],[f359,f153])).
% 0.15/0.43 fof(f595,plain,(
% 0.15/0.43 ~head_of(sK8_skl)=head_of(sK9_skl)),
% 0.15/0.43 inference(equality_resolution,[status(thm)],[f359])).
% 0.15/0.43 fof(f596,plain,(
% 0.15/0.43 ~sQ8_spl|~sQ5_spl),
% 0.15/0.43 inference(split_clause,[status(thm)],[f593,f162,f152])).
% 0.15/0.43 fof(f603,plain,(
% 0.15/0.43 $false|~sQ7_spl),
% 0.15/0.43 inference(forward_subsumption_resolution,[status(thm)],[f159,f595])).
% 0.15/0.43 fof(f604,plain,(
% 0.15/0.43 ~sQ7_spl),
% 0.15/0.43 inference(contradiction_clause,[status(thm)],[f603])).
% 0.15/0.43 fof(f617,plain,(
% 0.15/0.43 precedes(sK9_skl,sK8_skl,sK10_skl)|~on_path(sK9_skl,sK10_skl)|~on_path(sK8_skl,sK10_skl)|~sQ30_spl),
% 0.15/0.43 inference(resolution,[status(thm)],[f308,f376])).
% 0.15/0.43 fof(f623,definition,(
% 0.15/0.43 sQ63_spl <=> (precedes(sK9_skl,sK8_skl,sK10_skl))),
% 0.15/0.43 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.15/0.43 fof(f624,plain,(
% 0.15/0.43 precedes(sK9_skl,sK8_skl,sK10_skl)|~sQ63_spl),
% 0.15/0.43 inference(component_clause,[status(thm)],[f623])).
% 0.15/0.43 fof(f626,plain,(
% 0.15/0.43 sQ63_spl|~sQ36_spl|~sQ35_spl|~sQ30_spl),
% 0.15/0.43 inference(split_clause,[status(thm)],[f617,f623,f383,f378,f307])).
% 0.15/0.43 fof(f637,plain,(
% 0.15/0.43 $false|~sQ63_spl),
% 0.15/0.43 inference(forward_subsumption_resolution,[status(thm)],[f624,f260])).
% 0.15/0.43 fof(f638,plain,(
% 0.15/0.43 ~sQ63_spl),
% 0.15/0.43 inference(contradiction_clause,[status(thm)],[f637])).
% 0.15/0.43 fof(f640,plain,(
% 0.15/0.43 $false|~sQ31_spl),
% 0.15/0.44 inference(forward_subsumption_resolution,[status(thm)],[f328,f323])).
% 0.15/0.44 fof(f641,plain,(
% 0.15/0.44 ~sQ31_spl),
% 0.15/0.44 inference(contradiction_clause,[status(thm)],[f640])).
% 0.15/0.44 fof(f642,plain,(
% 0.15/0.44 $false),
% 0.15/0.44 inference(sat_refutation,[status(thm)],[f161,f165,f201,f313,f381,f386,f392,f406,f596,f604,f626,f638,f641])).
% 0.15/0.44 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.46 % Elapsed time: 0.081222 seconds
% 0.15/0.46 % CPU time: 0.294353 seconds
% 0.15/0.46 % Total memory used: 62.128 MB
% 0.15/0.46 % Net memory used: 61.922 MB
%------------------------------------------------------------------------------