%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL654+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 01:10:39 PM UTC 2026
% Result : Theorem 0.18s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL654+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.48 % Computer : n015.cluster.edu
% 0.18/0.48 % Model : x86_64 x86_64
% 0.18/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.48 % Memory : 8046.5625MB
% 0.18/0.48 % OS : Linux 6.8.0-71-generic
% 0.18/0.48 % CPULimit : 300
% 0.18/0.48 % WCLimit : 300
% 0.18/0.48 % DateTime : Mon Sep 21 00:50:07 UTC 2026
% 0.18/0.49 % CPUTime :
% 0.18/0.50 % Drodi V4.1.1
% 0.18/0.51 % Refutation found
% 0.18/0.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.51 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.51 fof(f1,axiom,(
% 0.18/0.51 (! [X] : r1(X,X) )),
% 0.18/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.51 fof(f2,conjecture,(
% 0.18/0.51 ~ (? [X] :~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p1(Y) ) )))& p1(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) )))& ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| $false ) )))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) )) )),
% 0.18/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.51 fof(f3,negated_conjecture,(
% 0.18/0.51 ~(~ (? [X] :~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p1(Y) ) )))& p1(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) )))& ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| $false ) )))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) )) ))),
% 0.18/0.51 inference(negated_conjecture,[status(cth)],[f2])).
% 0.18/0.51 fof(f4,plain,(
% 0.18/0.51 ![X0]: (r1(X0,X0))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f1])).
% 0.18/0.51 fof(f5,plain,(
% 0.18/0.51 ?[X]: (((((![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&p1(Y)))))|~p1(Y))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&~p1(X)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))&(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|p1(X)))))))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y)))))))))&(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&$true)))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(?[Y]: (r1(X,Y)&~p1(Y))))))&(![X]: (~r1(Y,X)|p1(X))))))),
% 0.18/0.51 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.18/0.51 fof(f6,plain,(
% 0.18/0.51 ?[X]: (((((![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&p1(Y)))))|~p1(Y))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&~p1(X)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))&(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|p1(X)))))))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y)))))))))&(![Y]: (~r1(X,Y)|((?[X]: r1(Y,X))&$true))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(?[Y]: (r1(X,Y)&~p1(Y))))))&(![X]: (~r1(Y,X)|p1(X))))))),
% 0.18/0.51 inference(miniscoping,[status(thm)],[f5])).
% 0.18/0.51 fof(f7,plain,(
% 0.18/0.51 (((((![Y]: (~r1(sK0_skl,Y)|((![X]: (~r1(Y,X)|(r1(X,sK1_skl(X,Y))&p1(sK1_skl(X,Y)))))|~p1(Y))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(r1(Y,sK2_skl(Y,X,Y))&~p1(sK2_skl(Y,X,Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|((![X]: (~r1(Y,X)|(r1(X,sK3_skl(X,Y))&(![X]: (~r1(sK3_skl(X,Y),X)|p1(X))))))|(![X]: (~r1(Y,X)|(r1(X,sK4_skl(X,Y))&~p1(sK4_skl(X,Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(r1(Y,sK5_skl(Y))&$true))))&((r1(sK0_skl,sK6_skl)&(r1(sK6_skl,sK7_skl)&(r1(sK7_skl,sK8_skl)&~p1(sK8_skl))))&(![X]: (~r1(sK6_skl,X)|p1(X)))))),
% 0.18/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl(X,Y)),skolemize(X,sK2_skl(Y,X,Y)),skolemize(Y,sK3_skl(X,Y)),skolemize(Y,sK4_skl(X,Y)),skolemize(X,sK5_skl(Y)),skolemize(Y,sK6_skl),skolemize(X,sK7_skl),skolemize(Y,sK8_skl)],[f6])).
% 0.18/0.51 fof(f8,plain,(
% 0.18/0.51 ?[X]: (((((![Y]: (~r1(sK0_skl,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK1_skl(X,Y))&p1(sK1_skl(X,Y))))))|~p1(Y))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,sK2_skl(Y,X,Y))&~p1(sK2_skl(Y,X,Y))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK3_skl(X,Y))&(![X]: (~r1(sK3_skl(X,Y),X)|p1(X)))))))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK4_skl(X,Y))&~p1(sK4_skl(X,Y))))))))))&(![Y]: (~r1(sK0_skl,Y)|(?[X]: r1(Y,sK5_skl(Y))))))&(?[Y]: ((r1(sK0_skl,sK6_skl)&(?[X]: (r1(sK6_skl,sK7_skl)&(?[Y]: (r1(sK7_skl,sK8_skl)&~p1(sK8_skl))))))&(![X]: (~r1(sK6_skl,X)|p1(X))))))),
% 0.18/0.51 inference(true_and_false_simplification,[status(thm)],[f7])).
% 0.18/0.51 fof(f11,plain,(
% 0.18/0.51 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|r1(X2,sK2_skl(X2,X1,X0))|~r1(X1,X3)|p1(X3))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/0.51 fof(f12,plain,(
% 0.18/0.51 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~p1(sK2_skl(X2,X1,X0))|~r1(X1,X3)|p1(X3))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/0.51 fof(f13,plain,(
% 0.18/0.51 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|r1(X1,sK3_skl(X1,X0))|~r1(X0,X2)|r1(X2,sK4_skl(X2,X0)))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/0.51 fof(f14,plain,(
% 0.18/0.51 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|r1(X1,sK3_skl(X1,X0))|~r1(X0,X2)|~p1(sK4_skl(X2,X0)))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/0.51 fof(f15,plain,(
% 0.18/0.51 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(sK3_skl(X1,X0),X2)|p1(X2)|~r1(X0,X3)|r1(X3,sK4_skl(X3,X0)))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/0.51 fof(f16,plain,(
% 0.18/0.51 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(sK3_skl(X1,X0),X2)|p1(X2)|~r1(X0,X3)|~p1(sK4_skl(X3,X0)))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/0.51 fof(f18,plain,(
% 0.18/0.51 r1(sK0_skl,sK6_skl)),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/0.51 fof(f19,plain,(
% 0.18/0.51 r1(sK6_skl,sK7_skl)),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/0.51 fof(f20,plain,(
% 0.18/0.51 r1(sK7_skl,sK8_skl)),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/0.51 fof(f21,plain,(
% 0.18/0.51 ~p1(sK8_skl)),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/0.51 fof(f22,plain,(
% 0.18/0.51 ![X0]: (~r1(sK6_skl,X0)|p1(X0))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/0.51 fof(f34,definition,(
% 0.18/0.51 sQ2_spl <=> (r1(sK0_skl,sK6_skl))),
% 0.18/0.51 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.18/0.51 fof(f36,plain,(
% 0.18/0.51 ~r1(sK0_skl,sK6_skl)|sQ2_spl),
% 0.18/0.51 inference(component_clause,[status(thm)],[f34])).
% 0.18/0.51 fof(f41,plain,(
% 0.18/0.51 $false|sQ2_spl),
% 0.18/0.51 inference(forward_subsumption_resolution,[status(thm)],[f36,f18])).
% 0.18/0.51 fof(f42,plain,(
% 0.18/0.51 sQ2_spl),
% 0.18/0.51 inference(contradiction_clause,[status(thm)],[f41])).
% 0.18/0.51 fof(f60,definition,(
% 0.18/0.51 sQ7_spl <=> (r1(sK6_skl,sK6_skl))),
% 0.18/0.51 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.18/0.51 fof(f62,plain,(
% 0.18/0.51 ~r1(sK6_skl,sK6_skl)|sQ7_spl),
% 0.18/0.51 inference(component_clause,[status(thm)],[f60])).
% 0.18/0.51 fof(f67,plain,(
% 0.18/0.51 $false|sQ7_spl),
% 0.18/0.51 inference(forward_subsumption_resolution,[status(thm)],[f62,f4])).
% 0.18/0.51 fof(f68,plain,(
% 0.18/0.51 sQ7_spl),
% 0.18/0.51 inference(contradiction_clause,[status(thm)],[f67])).
% 0.18/0.51 fof(f79,definition,(
% 0.18/0.51 ![X0]: (sQ11_spl <=> (~r1(sK0_skl,X0)|~r1(X0,sK0_skl)))),
% 0.18/0.51 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.18/0.51 fof(f80,plain,(
% 0.18/0.51 ![X0]: (~r1(sK0_skl,X0)|~r1(X0,sK0_skl)|~sQ11_spl)),
% 0.18/0.51 inference(component_clause,[status(thm)],[f79])).
% 0.18/0.51 fof(f86,definition,(
% 0.18/0.51 ![X0]: (sQ13_spl <=> (~r1(sK0_skl,X0)|~r1(X0,sK6_skl)))),
% 0.18/0.51 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.18/0.51 fof(f87,plain,(
% 0.18/0.51 ![X0]: (~r1(sK0_skl,X0)|~r1(X0,sK6_skl)|~sQ13_spl)),
% 0.18/0.51 inference(component_clause,[status(thm)],[f86])).
% 0.18/0.51 fof(f93,plain,(
% 0.18/0.51 ~r1(sK0_skl,sK0_skl)|~sQ13_spl),
% 0.18/0.51 inference(resolution,[status(thm)],[f87,f18])).
% 0.18/0.51 fof(f95,plain,(
% 0.18/0.51 $false|~sQ13_spl),
% 0.18/0.51 inference(forward_subsumption_resolution,[status(thm)],[f93,f4])).
% 0.18/0.51 fof(f96,plain,(
% 0.18/0.51 ~sQ13_spl),
% 0.18/0.51 inference(contradiction_clause,[status(thm)],[f95])).
% 0.18/0.51 fof(f97,plain,(
% 0.18/0.51 ~r1(sK0_skl,sK0_skl)|~sQ11_spl),
% 0.18/0.51 inference(resolution,[status(thm)],[f80,f4])).
% 0.18/0.51 fof(f98,plain,(
% 0.18/0.51 $false|~sQ11_spl),
% 0.18/0.51 inference(forward_subsumption_resolution,[status(thm)],[f97,f4])).
% 0.18/0.51 fof(f99,plain,(
% 0.18/0.51 ~sQ11_spl),
% 0.18/0.51 inference(contradiction_clause,[status(thm)],[f98])).
% 0.18/0.51 fof(f103,plain,(
% 0.18/0.51 ![X0,X1]: (~r1(sK6_skl,X0)|r1(X0,sK3_skl(X0,sK6_skl))|~r1(sK6_skl,X1)|r1(X1,sK4_skl(X1,sK6_skl)))),
% 0.18/0.51 inference(resolution,[status(thm)],[f13,f18])).
% 0.18/0.51 fof(f108,definition,(
% 0.18/0.51 ![X0]: (sQ15_spl <=> (~r1(sK6_skl,X0)|r1(X0,sK3_skl(X0,sK6_skl))))),
% 0.18/0.51 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.18/0.51 fof(f109,plain,(
% 0.18/0.51 ![X0]: (~r1(sK6_skl,X0)|r1(X0,sK3_skl(X0,sK6_skl))|~sQ15_spl)),
% 0.18/0.51 inference(component_clause,[status(thm)],[f108])).
% 0.18/0.51 fof(f111,definition,(
% 0.18/0.51 ![X1]: (sQ16_spl <=> (~r1(sK6_skl,X1)|r1(X1,sK4_skl(X1,sK6_skl))))),
% 0.18/0.51 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.18/0.51 fof(f112,plain,(
% 0.18/0.51 ![X0]: (~r1(sK6_skl,X0)|r1(X0,sK4_skl(X0,sK6_skl))|~sQ16_spl)),
% 0.18/0.51 inference(component_clause,[status(thm)],[f111])).
% 0.18/0.51 fof(f114,plain,(
% 0.18/0.51 sQ15_spl|sQ16_spl),
% 0.18/0.51 inference(split_clause,[status(thm)],[f103,f108,f111])).
% 0.18/0.51 fof(f131,definition,(
% 0.18/0.51 sQ22_spl <=> (r1(sK0_skl,sK0_skl))),
% 0.18/0.51 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.18/0.51 fof(f133,plain,(
% 0.18/0.51 ~r1(sK0_skl,sK0_skl)|sQ22_spl),
% 0.18/0.51 inference(component_clause,[status(thm)],[f131])).
% 0.18/0.51 fof(f142,plain,(
% 0.18/0.51 $false|sQ22_spl),
% 0.18/0.51 inference(forward_subsumption_resolution,[status(thm)],[f133,f4])).
% 0.18/0.51 fof(f143,plain,(
% 0.18/0.51 sQ22_spl),
% 0.18/0.51 inference(contradiction_clause,[status(thm)],[f142])).
% 0.18/0.51 fof(f160,plain,(
% 0.18/0.51 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(sK3_skl(X1,X0),X2)|p1(X2)|~r1(X0,sK6_skl)|p1(sK4_skl(sK6_skl,X0)))),
% 0.18/0.51 inference(resolution,[status(thm)],[f15,f22])).
% 0.18/0.51 fof(f162,plain,(
% 0.18/0.51 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(sK3_skl(X1,X0),X2)|p1(X2)|~r1(X0,sK6_skl))),
% 0.18/0.51 inference(forward_subsumption_resolution,[status(thm)],[f160,f16])).
% 0.18/0.51 fof(f221,plain,(
% 0.18/0.51 ~r1(sK6_skl,sK6_skl)|p1(sK4_skl(sK6_skl,sK6_skl))|~sQ16_spl),
% 0.18/0.51 inference(resolution,[status(thm)],[f112,f22])).
% 0.18/0.51 fof(f233,definition,(
% 0.18/0.51 sQ42_spl <=> (p1(sK4_skl(sK6_skl,sK6_skl)))),
% 0.18/0.51 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.18/0.51 fof(f234,plain,(
% 0.18/0.51 p1(sK4_skl(sK6_skl,sK6_skl))|~sQ42_spl),
% 0.18/0.51 inference(component_clause,[status(thm)],[f233])).
% 0.18/0.51 fof(f236,plain,(
% 0.18/0.51 ~sQ7_spl|sQ42_spl|~sQ16_spl),
% 0.18/0.51 inference(split_clause,[status(thm)],[f221,f60,f233,f111])).
% 0.18/0.51 fof(f238,plain,(
% 0.18/0.51 ![X0]: (~r1(sK0_skl,sK6_skl)|~r1(sK6_skl,X0)|r1(X0,sK3_skl(X0,sK6_skl))|~r1(sK6_skl,sK6_skl)|~sQ42_spl)),
% 0.18/0.51 inference(resolution,[status(thm)],[f234,f14])).
% 0.18/0.51 fof(f239,definition,(
% 0.18/0.51 ![X0,X1]: (sQ43_spl <=> (~r1(sK6_skl,X0)|~r1(sK3_skl(X0,sK6_skl),X1)|p1(X1)))),
% 0.18/0.51 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.18/0.51 fof(f240,plain,(
% 0.18/0.51 ![X0,X1]: (~r1(sK6_skl,X0)|~r1(sK3_skl(X0,sK6_skl),X1)|p1(X1)|~sQ43_spl)),
% 0.18/0.51 inference(component_clause,[status(thm)],[f239])).
% 0.18/0.51 fof(f243,plain,(
% 0.18/0.51 ~sQ2_spl|sQ15_spl|~sQ7_spl|~sQ42_spl),
% 0.18/0.51 inference(split_clause,[status(thm)],[f238,f34,f108,f60,f233])).
% 0.18/0.51 fof(f265,plain,(
% 0.18/0.51 ![X0,X1,X2,X3]: (~r1(sK6_skl,X0)|p1(sK2_skl(sK3_skl(X0,sK6_skl),X1,X2))|~r1(sK0_skl,X2)|~r1(X2,X1)|~r1(X1,sK3_skl(X0,sK6_skl))|~r1(X1,X3)|p1(X3)|~sQ43_spl)),
% 0.18/0.51 inference(resolution,[status(thm)],[f240,f11])).
% 0.18/0.51 fof(f268,plain,(
% 0.18/0.51 ![X0,X1,X2,X3]: (~r1(sK6_skl,X0)|~r1(sK0_skl,X1)|~r1(X1,X2)|~r1(X2,sK3_skl(X0,sK6_skl))|~r1(X2,X3)|p1(X3)|~sQ43_spl)),
% 0.18/0.51 inference(forward_subsumption_resolution,[status(thm)],[f265,f12])).
% 0.18/0.51 fof(f295,plain,(
% 0.18/0.51 ![X0,X1]: (~r1(sK0_skl,sK6_skl)|~r1(sK6_skl,X0)|~r1(sK3_skl(X0,sK6_skl),X1)|p1(X1))),
% 0.18/0.51 inference(resolution,[status(thm)],[f162,f4])).
% 0.18/0.51 fof(f300,plain,(
% 0.18/0.51 ~sQ2_spl|sQ43_spl),
% 0.18/0.51 inference(split_clause,[status(thm)],[f295,f34,f239])).
% 0.18/0.51 fof(f386,plain,(
% 0.18/0.51 ![X0,X1,X2]: (~r1(sK6_skl,X0)|~r1(sK0_skl,X1)|~r1(X1,X0)|~r1(X0,X2)|p1(X2)|~r1(sK6_skl,X0)|~sQ43_spl|~sQ15_spl)),
% 0.18/0.51 inference(resolution,[status(thm)],[f268,f109])).
% 0.18/0.51 fof(f388,plain,(
% 0.18/0.51 ![X0,X1,X2]: (~r1(sK6_skl,X0)|~r1(sK0_skl,X1)|~r1(X1,X0)|~r1(X0,X2)|p1(X2)|~sQ43_spl|~sQ15_spl)),
% 0.18/0.51 inference(duplicate_literals_removal,[status(thm)],[f386])).
% 0.18/0.51 fof(f389,plain,(
% 0.18/0.51 ![X0,X1]: (~r1(sK6_skl,X0)|~r1(sK6_skl,X0)|~r1(X0,X1)|p1(X1)|~sQ43_spl|~sQ15_spl)),
% 0.18/0.51 inference(resolution,[status(thm)],[f388,f18])).
% 0.18/0.51 fof(f401,plain,(
% 0.18/0.51 ![X0,X1]: (~r1(sK6_skl,X0)|~r1(X0,X1)|p1(X1)|~sQ43_spl|~sQ15_spl)),
% 0.18/0.51 inference(duplicate_literals_removal,[status(thm)],[f389])).
% 0.18/0.51 fof(f430,plain,(
% 0.18/0.51 ![X0]: (~r1(sK7_skl,X0)|p1(X0)|~sQ43_spl|~sQ15_spl)),
% 0.18/0.51 inference(resolution,[status(thm)],[f401,f19])).
% 0.18/0.51 fof(f476,plain,(
% 0.18/0.51 p1(sK8_skl)|~sQ43_spl|~sQ15_spl),
% 0.18/0.51 inference(resolution,[status(thm)],[f430,f20])).
% 0.18/0.51 fof(f487,plain,(
% 0.18/0.51 $false|~sQ43_spl|~sQ15_spl),
% 0.18/0.51 inference(forward_subsumption_resolution,[status(thm)],[f476,f21])).
% 0.18/0.51 fof(f488,plain,(
% 0.18/0.51 ~sQ43_spl|~sQ15_spl),
% 0.18/0.51 inference(contradiction_clause,[status(thm)],[f487])).
% 0.18/0.51 fof(f489,plain,(
% 0.18/0.51 $false),
% 0.18/0.51 inference(sat_refutation,[status(thm)],[f42,f68,f96,f99,f114,f143,f236,f243,f300,f488])).
% 0.18/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/0.57 % Elapsed time: 0.074237 seconds
% 0.23/0.57 % CPU time: 0.105354 seconds
% 0.23/0.57 % Total memory used: 5.431 MB
% 0.23/0.57 % Net memory used: 5.315 MB
%------------------------------------------------------------------------------