%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL650+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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 01:10:37 PM UTC 2026
% Result : Theorem 0.15s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL650+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 00:45:42 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.15/0.40 % Refutation found
% 0.15/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.40 fof(f1,conjecture,(
% 0.15/0.40 ~ (? [X] :~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ( ~ p8(X)& ~ p6(X)& ~ p4(X)& ~ p2(X) ) ) )) )) )))| (! [Y] :( ~ r1(X,Y)| p5(Y) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p3(X)& ~ p1(X) )| ( p1(X)& p3(X) ) ) ) )) )))| (! [X] :( ~ r1(Y,X)| p4(X) ))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p2(X)& ~ p3(X) )| ( p3(X)& p2(X) ) ) ) )))| (! [Y] :( ~ r1(X,Y)| p3(Y) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ~ (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p1(X)& ~ p2(X) )| ( p2(X)& p1(X) ) ) ) )) )) ) )) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ( p4(X)& p3(X)& p2(X)& p1(X) ) ) )) )) )) )) )),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f2,negated_conjecture,(
% 0.15/0.40 ~(~ (? [X] :~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ( ~ p8(X)& ~ p6(X)& ~ p4(X)& ~ p2(X) ) ) )) )) )))| (! [Y] :( ~ r1(X,Y)| p5(Y) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p3(X)& ~ p1(X) )| ( p1(X)& p3(X) ) ) ) )) )))| (! [X] :( ~ r1(Y,X)| p4(X) ))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p2(X)& ~ p3(X) )| ( p3(X)& p2(X) ) ) ) )))| (! [Y] :( ~ r1(X,Y)| p3(Y) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ~ (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p1(X)& ~ p2(X) )| ( p2(X)& p1(X) ) ) ) )) )) ) )) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ( p4(X)& p3(X)& p2(X)& p1(X) ) ) )) )) )) )) ))),
% 0.15/0.40 inference(negated_conjecture,[status(cth)],[f1])).
% 0.15/0.40 fof(f3,plain,(
% 0.15/0.40 ?[X]: ((((?[Y]: (r1(X,Y)&(?[X]: (r1(Y,X)&(?[Y]: (r1(X,Y)&(?[X]: (r1(Y,X)&(((p8(X)|p6(X))|p4(X))|p2(X))))))))))&(?[Y]: (r1(X,Y)&~p5(Y))))&(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p3(X)|p1(X))&(~p1(X)|~p3(X)))))))))&(?[X]: (r1(Y,X)&~p4(X))))&(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p2(X)|p3(X))&(~p3(X)|~p2(X)))))))&(?[Y]: (r1(X,Y)&~p3(Y))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p1(X)|p2(X))&(~p2(X)|~p1(X))))))))))))))&(?[Y]: (r1(X,Y)&(?[X]: (r1(Y,X)&(?[Y]: (r1(X,Y)&(?[X]: (r1(Y,X)&(((~p4(X)|~p3(X))|~p2(X))|~p1(X)))))))))))),
% 0.15/0.40 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.15/0.40 fof(f4,plain,(
% 0.15/0.40 ((((r1(sK0_skl,sK1_skl)&(r1(sK1_skl,sK2_skl)&(r1(sK2_skl,sK3_skl)&(r1(sK3_skl,sK4_skl)&(((p8(sK4_skl)|p6(sK4_skl))|p4(sK4_skl))|p2(sK4_skl))))))&(r1(sK0_skl,sK5_skl)&~p5(sK5_skl)))&(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p3(X)|p1(X))&(~p1(X)|~p3(X)))))))))&(r1(Y,sK6_skl(Y))&~p4(sK6_skl(Y))))&(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p2(X)|p3(X))&(~p3(X)|~p2(X)))))))&(r1(X,sK7_skl(X,Y))&~p3(sK7_skl(X,Y))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p1(X)|p2(X))&(~p2(X)|~p1(X))))))))))))))&(r1(sK0_skl,sK8_skl)&(r1(sK8_skl,sK9_skl)&(r1(sK9_skl,sK10_skl)&(r1(sK10_skl,sK11_skl)&(((~p4(sK11_skl)|~p3(sK11_skl))|~p2(sK11_skl))|~p1(sK11_skl)))))))),
% 0.15/0.40 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,sK9_skl,sK10_skl,sK11_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl),skolemize(X,sK2_skl),skolemize(Y,sK3_skl),skolemize(X,sK4_skl),skolemize(Y,sK5_skl),skolemize(X,sK6_skl(Y)),skolemize(Y,sK7_skl(X,Y)),skolemize(Y,sK8_skl),skolemize(X,sK9_skl),skolemize(Y,sK10_skl),skolemize(X,sK11_skl)],[f3])).
% 0.15/0.40 fof(f5,plain,(
% 0.15/0.40 r1(sK0_skl,sK1_skl)),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.40 fof(f6,plain,(
% 0.15/0.40 r1(sK1_skl,sK2_skl)),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.40 fof(f7,plain,(
% 0.15/0.40 r1(sK2_skl,sK3_skl)),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.40 fof(f8,plain,(
% 0.15/0.40 r1(sK3_skl,sK4_skl)),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.40 fof(f12,plain,(
% 0.15/0.40 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p3(X3)|p1(X3))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.40 fof(f13,plain,(
% 0.15/0.40 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~p1(X3)|~p3(X3))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.40 fof(f16,plain,(
% 0.15/0.40 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p2(X3)|p3(X3))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.40 fof(f17,plain,(
% 0.15/0.40 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~p3(X3)|~p2(X3))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.40 fof(f20,plain,(
% 0.15/0.40 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p1(X3)|p2(X3))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.40 fof(f21,plain,(
% 0.15/0.40 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~p2(X3)|~p1(X3))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.40 fof(f36,definition,(
% 0.15/0.40 sQ3_spl <=> (p2(sK4_skl))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f54,plain,(
% 0.15/0.40 ![X0,X1,X2]: (~r1(sK1_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~p1(X2)|~p3(X2))),
% 0.15/0.40 inference(resolution,[status(thm)],[f13,f5])).
% 0.15/0.40 fof(f58,plain,(
% 0.15/0.40 ![X0,X1,X2]: (~r1(sK1_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~p3(X2)|~p2(X2))),
% 0.15/0.40 inference(resolution,[status(thm)],[f17,f5])).
% 0.15/0.40 fof(f62,plain,(
% 0.15/0.40 ![X0,X1,X2]: (~r1(sK1_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~p2(X2)|~p1(X2))),
% 0.15/0.40 inference(resolution,[status(thm)],[f21,f5])).
% 0.15/0.40 fof(f64,plain,(
% 0.15/0.40 ![X0,X1,X2]: (~r1(sK1_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p3(X2)|p1(X2))),
% 0.15/0.40 inference(resolution,[status(thm)],[f12,f5])).
% 0.15/0.40 fof(f65,plain,(
% 0.15/0.40 ![X0,X1]: (~r1(sK2_skl,X0)|~r1(X0,X1)|p3(X1)|p1(X1))),
% 0.15/0.40 inference(resolution,[status(thm)],[f64,f6])).
% 0.15/0.40 fof(f66,plain,(
% 0.15/0.40 ![X0]: (~r1(sK3_skl,X0)|p3(X0)|p1(X0))),
% 0.15/0.40 inference(resolution,[status(thm)],[f65,f7])).
% 0.15/0.40 fof(f68,plain,(
% 0.15/0.40 ![X0,X1,X2]: (~r1(sK1_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p2(X2)|p3(X2))),
% 0.15/0.40 inference(resolution,[status(thm)],[f16,f5])).
% 0.15/0.40 fof(f70,plain,(
% 0.15/0.40 ![X0,X1,X2]: (~r1(sK1_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p1(X2)|p2(X2))),
% 0.15/0.40 inference(resolution,[status(thm)],[f20,f5])).
% 0.15/0.40 fof(f71,plain,(
% 0.15/0.40 ![X0,X1]: (~r1(sK2_skl,X0)|~r1(X0,X1)|p2(X1)|p3(X1))),
% 0.15/0.40 inference(resolution,[status(thm)],[f68,f6])).
% 0.15/0.40 fof(f72,plain,(
% 0.15/0.40 ![X0,X1]: (~r1(sK2_skl,X0)|~r1(X0,X1)|p1(X1)|p2(X1))),
% 0.15/0.40 inference(resolution,[status(thm)],[f70,f6])).
% 0.15/0.40 fof(f73,plain,(
% 0.15/0.40 ![X0]: (~r1(sK3_skl,X0)|p2(X0)|p3(X0))),
% 0.15/0.40 inference(resolution,[status(thm)],[f71,f7])).
% 0.15/0.40 fof(f74,plain,(
% 0.15/0.40 ![X0]: (~r1(sK3_skl,X0)|p1(X0)|p2(X0))),
% 0.15/0.40 inference(resolution,[status(thm)],[f72,f7])).
% 0.15/0.40 fof(f75,plain,(
% 0.15/0.40 p3(sK4_skl)|p1(sK4_skl)),
% 0.15/0.40 inference(resolution,[status(thm)],[f66,f8])).
% 0.15/0.40 fof(f76,definition,(
% 0.15/0.40 sQ8_spl <=> (p3(sK4_skl))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f79,definition,(
% 0.15/0.40 sQ9_spl <=> (p1(sK4_skl))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f82,plain,(
% 0.15/0.40 sQ8_spl|sQ9_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f75,f76,f79])).
% 0.15/0.40 fof(f83,plain,(
% 0.15/0.40 p2(sK4_skl)|p3(sK4_skl)),
% 0.15/0.40 inference(resolution,[status(thm)],[f73,f8])).
% 0.15/0.40 fof(f84,plain,(
% 0.15/0.40 sQ3_spl|sQ8_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f83,f36,f76])).
% 0.15/0.40 fof(f85,plain,(
% 0.15/0.40 p1(sK4_skl)|p2(sK4_skl)),
% 0.15/0.40 inference(resolution,[status(thm)],[f74,f8])).
% 0.15/0.40 fof(f86,plain,(
% 0.15/0.40 sQ9_spl|sQ3_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f85,f79,f36])).
% 0.15/0.40 fof(f107,plain,(
% 0.15/0.40 ![X0,X1]: (~r1(sK2_skl,X0)|~r1(X0,X1)|~p1(X1)|~p3(X1))),
% 0.15/0.40 inference(resolution,[status(thm)],[f54,f6])).
% 0.15/0.40 fof(f122,plain,(
% 0.15/0.40 ![X0,X1]: (~r1(sK2_skl,X0)|~r1(X0,X1)|~p3(X1)|~p2(X1))),
% 0.15/0.40 inference(resolution,[status(thm)],[f58,f6])).
% 0.15/0.40 fof(f127,plain,(
% 0.15/0.40 ![X0,X1]: (~r1(sK2_skl,X0)|~r1(X0,X1)|~p2(X1)|~p1(X1))),
% 0.15/0.40 inference(resolution,[status(thm)],[f62,f6])).
% 0.15/0.40 fof(f136,plain,(
% 0.15/0.40 ![X0]: (~r1(sK3_skl,X0)|~p1(X0)|~p3(X0))),
% 0.15/0.40 inference(resolution,[status(thm)],[f107,f7])).
% 0.15/0.40 fof(f142,plain,(
% 0.15/0.40 ![X0]: (~r1(sK3_skl,X0)|~p3(X0)|~p2(X0))),
% 0.15/0.40 inference(resolution,[status(thm)],[f122,f7])).
% 0.15/0.40 fof(f158,plain,(
% 0.15/0.40 ~p1(sK4_skl)|~p3(sK4_skl)),
% 0.15/0.40 inference(resolution,[status(thm)],[f136,f8])).
% 0.15/0.40 fof(f159,plain,(
% 0.15/0.40 ~sQ9_spl|~sQ8_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f158,f79,f76])).
% 0.15/0.40 fof(f161,plain,(
% 0.15/0.40 ![X0]: (~r1(sK3_skl,X0)|~p2(X0)|~p1(X0))),
% 0.15/0.40 inference(resolution,[status(thm)],[f127,f7])).
% 0.15/0.40 fof(f164,plain,(
% 0.15/0.40 ~p3(sK4_skl)|~p2(sK4_skl)),
% 0.15/0.40 inference(resolution,[status(thm)],[f142,f8])).
% 0.15/0.40 fof(f165,plain,(
% 0.15/0.40 ~sQ8_spl|~sQ3_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f164,f76,f36])).
% 0.15/0.40 fof(f176,plain,(
% 0.15/0.40 ~p2(sK4_skl)|~p1(sK4_skl)),
% 0.15/0.40 inference(resolution,[status(thm)],[f161,f8])).
% 0.15/0.40 fof(f177,plain,(
% 0.15/0.40 ~sQ3_spl|~sQ9_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f176,f36,f79])).
% 0.15/0.40 fof(f178,plain,(
% 0.15/0.40 $false),
% 0.15/0.40 inference(sat_refutation,[status(thm)],[f82,f84,f86,f159,f165,f177])).
% 0.15/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.42 % Elapsed time: 0.044524 seconds
% 0.15/0.42 % CPU time: 0.137692 seconds
% 0.15/0.42 % Total memory used: 18.224 MB
% 0.15/0.42 % Net memory used: 17.918 MB
%------------------------------------------------------------------------------