%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO109+1 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:06:53 PM UTC 2026
% Result : Theorem 24.17s 3.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : BOO109+1 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n013.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Mon Sep 21 13:53:51 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.43 % Drodi V4.1.1
% 24.17/3.56 % Refutation found
% 24.17/3.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 24.17/3.56 % SZS output start CNFRefutation for theBenchmark
% 24.17/3.56 fof(f1,axiom,(
% 24.17/3.56 (! [A,B,C,D] : p(nand(nand(A,nand(B,C)),nand(nand(nand(D,C),nand(nand(A,D),nand(A,D))),nand(A,nand(A,B))))) )),
% 24.17/3.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 24.17/3.56 fof(f2,axiom,(
% 24.17/3.56 (! [P,Q,R] :( ( p(nand(P,nand(Q,R)))& p(P) )=> p(R) ) )),
% 24.17/3.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 24.17/3.56 fof(f3,conjecture,(
% 24.17/3.56 (! [A,B] : p(nand(nand(A,nand(B,B)),nand(nand(nand(B,B),nand(nand(A,A),nand(A,A))),nand(nand(B,B),nand(nand(A,A),nand(A,A)))))) )),
% 24.17/3.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 24.17/3.56 fof(f4,negated_conjecture,(
% 24.17/3.56 ~((! [A,B] : p(nand(nand(A,nand(B,B)),nand(nand(nand(B,B),nand(nand(A,A),nand(A,A))),nand(nand(B,B),nand(nand(A,A),nand(A,A)))))) ))),
% 24.17/3.56 inference(negated_conjecture,[status(cth)],[f3])).
% 24.17/3.56 fof(f5,plain,(
% 24.17/3.56 ![X0,X1,X2,X3]: (p(nand(nand(X0,nand(X1,X2)),nand(nand(nand(X3,X2),nand(nand(X0,X3),nand(X0,X3))),nand(X0,nand(X0,X1))))))),
% 24.17/3.56 inference(cnf_transformation,[status(thm)],[f1])).
% 24.17/3.56 fof(f6,plain,(
% 24.17/3.56 ![P,Q,R]: ((~p(nand(P,nand(Q,R)))|~p(P))|p(R))),
% 24.17/3.56 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 24.17/3.56 fof(f7,plain,(
% 24.17/3.56 ![R]: ((![P]: ((![Q]: ~p(nand(P,nand(Q,R))))|~p(P)))|p(R))),
% 24.17/3.56 inference(miniscoping,[status(thm)],[f6])).
% 24.17/3.56 fof(f8,plain,(
% 24.17/3.56 ![X0,X1,X2]: (~p(nand(X0,nand(X1,X2)))|~p(X0)|p(X2))),
% 24.17/3.56 inference(cnf_transformation,[status(thm)],[f7])).
% 24.17/3.56 fof(f9,plain,(
% 24.17/3.56 (?[A,B]: ~p(nand(nand(A,nand(B,B)),nand(nand(nand(B,B),nand(nand(A,A),nand(A,A))),nand(nand(B,B),nand(nand(A,A),nand(A,A)))))))),
% 24.17/3.56 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 24.17/3.56 fof(f10,plain,(
% 24.17/3.56 ~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))),nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))))))),
% 24.17/3.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f9])).
% 24.17/3.56 fof(f11,plain,(
% 24.17/3.56 ~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))),nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))))))),
% 24.17/3.56 inference(cnf_transformation,[status(thm)],[f10])).
% 24.17/3.56 fof(f12,plain,(
% 24.17/3.56 ![X0,X1,X2]: (~p(nand(X0,nand(X1,X2)))|p(nand(X0,nand(X0,X1))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f5,f8])).
% 24.17/3.56 fof(f13,plain,(
% 24.17/3.56 ![X0,X1,X2]: (~p(nand(X0,nand(X1,X2)))|~p(X0)|p(X1))),
% 24.17/3.56 inference(resolution,[status(thm)],[f12,f8])).
% 24.17/3.56 fof(f14,plain,(
% 24.17/3.56 ![X0,X1,X2,X3]: (~p(nand(X0,nand(X1,X2)))|p(nand(nand(X3,X2),nand(nand(X0,X3),nand(X0,X3)))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f13,f5])).
% 24.17/3.56 fof(f16,plain,(
% 24.17/3.56 ![X0,X1,X2,X3]: (~p(nand(X0,nand(X1,X2)))|~p(nand(X3,X2))|p(nand(X0,X3)))),
% 24.17/3.56 inference(resolution,[status(thm)],[f14,f13])).
% 24.17/3.56 fof(f20,plain,(
% 24.17/3.56 ![X0,X1,X2,X3,X4]: (~p(nand(X0,nand(X1,nand(X2,X3))))|p(nand(X0,X2))|~p(nand(X2,nand(X3,X4))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f16,f12])).
% 24.17/3.56 fof(f23,plain,(
% 24.17/3.56 ![X0,X1,X2,X3,X4]: (~p(nand(X0,nand(X1,nand(X2,X2))))|p(nand(X0,X2))|~p(nand(X2,nand(X3,X4))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f20,f12])).
% 24.17/3.56 fof(f24,plain,(
% 24.17/3.56 ![X0,X1,X2,X3,X4]: (~p(nand(X0,nand(X1,nand(nand(X2,nand(X3,X4)),nand(X2,nand(X3,X4))))))|p(nand(X0,nand(X2,nand(X3,X4)))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f23,f5])).
% 24.17/3.56 fof(f25,plain,(
% 24.17/3.56 ![X0,X1,X2,X3,X4,X5]: (~p(nand(X0,nand(X1,nand(nand(X2,X3),nand(X2,X3)))))|p(nand(X0,nand(X2,X3)))|~p(nand(X4,nand(X5,X3))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f23,f14])).
% 24.17/3.56 fof(f53,plain,(
% 24.17/3.56 ![X0,X1,X2,X3,X4]: (p(nand(nand(nand(X0,nand(X1,X2)),X3),nand(X0,nand(X1,X2))))|~p(nand(nand(X0,nand(X1,X2)),nand(X4,X3))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f24,f14])).
% 24.17/3.56 fof(f59,plain,(
% 24.17/3.56 ![X0,X1,X2,X3,X4,X5]: (~p(nand(X0,nand(X1,nand(nand(X2,X3),nand(X2,X3)))))|p(nand(X0,nand(X2,X3)))|~p(nand(X4,nand(X3,X5))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f25,f12])).
% 24.17/3.56 fof(f104,plain,(
% 24.17/3.56 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~p(nand(X0,nand(X1,nand(nand(X2,X3),nand(X2,X3)))))|p(nand(X0,nand(X2,X3)))|~p(nand(nand(X3,nand(X4,X5)),nand(X6,X7))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f59,f53])).
% 24.17/3.56 fof(f243,definition,(
% 24.17/3.56 ![X1,X2]: (sQ1_spl <=> (~p(nand(nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))),nand(X1,X2)))))),
% 24.17/3.56 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 24.17/3.56 fof(f244,plain,(
% 24.17/3.56 ![X0,X1]: (~p(nand(nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))),nand(X0,X1)))|~sQ1_spl)),
% 24.17/3.56 inference(component_clause,[status(thm)],[f243])).
% 24.17/3.56 fof(f267,definition,(
% 24.17/3.56 ![X1,X2]: (sQ3_spl <=> (~p(nand(nand(sK1_skl,sK1_skl),nand(X1,X2)))))),
% 24.17/3.56 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 24.17/3.56 fof(f268,plain,(
% 24.17/3.56 ![X0,X1]: (~p(nand(nand(sK1_skl,sK1_skl),nand(X0,X1)))|~sQ3_spl)),
% 24.17/3.56 inference(component_clause,[status(thm)],[f267])).
% 24.17/3.56 fof(f296,plain,(
% 24.17/3.56 ![X0,X1,X2,X3]: (~p(nand(X0,nand(X1,nand(nand(X2,X3),nand(X2,X3)))))|p(nand(X0,nand(X2,X3))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f104,f5])).
% 24.17/3.56 fof(f310,plain,(
% 24.17/3.56 ![X0,X1,X2,X3]: (p(nand(nand(nand(X0,X1),X2),nand(X0,X1)))|~p(nand(nand(X0,X1),nand(X3,X2))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f296,f14])).
% 24.17/3.56 fof(f344,plain,(
% 24.17/3.56 ![X0,X1,X2,X3,X4,X5]: (~p(nand(nand(X0,X1),nand(X2,X3)))|~p(nand(X4,nand(X5,nand(X0,X1))))|p(nand(X4,nand(nand(X0,X1),X3))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f310,f16])).
% 24.17/3.56 fof(f583,plain,(
% 24.17/3.56 ![X0,X1]: (~p(nand(nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))),nand(X0,nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))))))|~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X1,nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl)))))))),
% 24.17/3.56 inference(resolution,[status(thm)],[f344,f11])).
% 24.17/3.56 fof(f635,definition,(
% 24.17/3.56 ![X0]: (sQ7_spl <=> (~p(nand(nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))),nand(X0,nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))))))))),
% 24.17/3.56 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 24.17/3.56 fof(f636,plain,(
% 24.17/3.56 ![X0]: (~p(nand(nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))),nand(X0,nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))))))|~sQ7_spl)),
% 24.17/3.56 inference(component_clause,[status(thm)],[f635])).
% 24.17/3.56 fof(f638,definition,(
% 24.17/3.56 ![X1]: (sQ8_spl <=> (~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X1,nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))))))))),
% 24.17/3.56 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 24.17/3.56 fof(f639,plain,(
% 24.17/3.56 ![X0]: (~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))))))|~sQ8_spl)),
% 24.17/3.56 inference(component_clause,[status(thm)],[f638])).
% 24.17/3.56 fof(f641,plain,(
% 24.17/3.56 sQ7_spl|sQ8_spl),
% 24.17/3.56 inference(split_clause,[status(thm)],[f583,f635,f638])).
% 24.17/3.56 fof(f647,plain,(
% 24.17/3.56 $false|~sQ1_spl),
% 24.17/3.56 inference(resolution,[status(thm)],[f244,f5])).
% 24.17/3.56 fof(f655,plain,(
% 24.17/3.56 ~sQ1_spl),
% 24.17/3.56 inference(contradiction_clause,[status(thm)],[f647])).
% 24.17/3.56 fof(f659,plain,(
% 24.17/3.56 ![X0]: (~p(nand(nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))),nand(nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))),X0)))|~sQ7_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f636,f12])).
% 24.17/3.56 fof(f665,plain,(
% 24.17/3.56 ![X0,X1]: (~p(nand(nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))),nand(X0,X1)))|~sQ7_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f659,f12])).
% 24.17/3.56 fof(f669,plain,(
% 24.17/3.56 sQ1_spl|~sQ7_spl),
% 24.17/3.56 inference(split_clause,[status(thm)],[f665,f243,f635])).
% 24.17/3.56 fof(f699,plain,(
% 24.17/3.56 ![X0,X1,X2,X3]: (~p(nand(nand(X0,X1),nand(X2,nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))))))|~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X3,nand(X0,X1))))|~sQ8_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f639,f344])).
% 24.17/3.56 fof(f713,plain,(
% 24.17/3.56 ![X0,X1,X2]: (~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl)),X1))))|~p(nand(nand(sK1_skl,sK1_skl),nand(X2,X1)))|~sQ8_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f699,f14])).
% 24.17/3.56 fof(f724,plain,(
% 24.17/3.56 ![X0,X1,X2]: (~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl)),X1))))|~p(nand(nand(sK1_skl,sK1_skl),nand(X1,X2)))|~sQ8_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f713,f12])).
% 24.17/3.56 fof(f737,plain,(
% 24.17/3.56 ![X0,X1,X2]: (~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl)),nand(sK1_skl,sK1_skl)))))|~p(nand(nand(sK1_skl,sK1_skl),nand(X1,X2)))|~sQ8_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f724,f12])).
% 24.17/3.56 fof(f740,definition,(
% 24.17/3.56 ![X0]: (sQ10_spl <=> (~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl)),nand(sK1_skl,sK1_skl)))))))),
% 24.17/3.56 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 24.17/3.56 fof(f741,plain,(
% 24.17/3.56 ![X0]: (~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl)),nand(sK1_skl,sK1_skl)))))|~sQ10_spl)),
% 24.17/3.56 inference(component_clause,[status(thm)],[f740])).
% 24.17/3.56 fof(f743,plain,(
% 24.17/3.56 sQ10_spl|sQ3_spl|~sQ8_spl),
% 24.17/3.56 inference(split_clause,[status(thm)],[f737,f740,f267,f638])).
% 24.17/3.56 fof(f754,plain,(
% 24.17/3.56 ![X0,X1]: (~p(nand(X0,nand(X1,sK1_skl)))|~sQ3_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f268,f14])).
% 24.17/3.56 fof(f764,plain,(
% 24.17/3.56 ![X0,X1]: (~p(nand(X0,nand(sK1_skl,X1)))|~sQ3_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f754,f12])).
% 24.17/3.56 fof(f768,plain,(
% 24.17/3.56 ![X0,X1,X2]: (~p(nand(nand(sK1_skl,X0),nand(X1,X2)))|~sQ3_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f764,f310])).
% 24.17/3.56 fof(f789,plain,(
% 24.17/3.56 $false|~sQ3_spl),
% 24.17/3.56 inference(resolution,[status(thm)],[f768,f5])).
% 24.17/3.56 fof(f797,plain,(
% 24.17/3.56 ~sQ3_spl),
% 24.17/3.56 inference(contradiction_clause,[status(thm)],[f789])).
% 24.17/3.56 fof(f798,plain,(
% 24.17/3.56 ![X0,X1,X2,X3]: (~p(nand(nand(X0,X1),nand(X2,nand(nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl)),nand(sK1_skl,sK1_skl)))))|~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X3,nand(X0,X1))))|~sQ10_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f741,f344])).
% 24.17/3.56 fof(f890,plain,(
% 24.17/3.56 ![X0,X1,X2]: (~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(sK1_skl,sK1_skl),X1))))|~p(nand(nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl)),nand(X2,X1)))|~sQ10_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f798,f14])).
% 24.17/3.56 fof(f897,plain,(
% 24.17/3.56 ![X0,X1]: (~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(sK1_skl,sK1_skl),sK0_skl))))|~p(nand(nand(sK0_skl,sK0_skl),nand(X1,nand(sK0_skl,sK0_skl))))|~sQ10_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f890,f310])).
% 24.17/3.56 fof(f906,definition,(
% 24.17/3.56 ![X0]: (sQ15_spl <=> (~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(sK1_skl,sK1_skl),sK0_skl))))))),
% 24.17/3.56 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 24.17/3.56 fof(f907,plain,(
% 24.17/3.56 ![X0]: (~p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(sK1_skl,sK1_skl),sK0_skl))))|~sQ15_spl)),
% 24.17/3.56 inference(component_clause,[status(thm)],[f906])).
% 24.17/3.56 fof(f909,definition,(
% 24.17/3.56 ![X1]: (sQ16_spl <=> (~p(nand(nand(sK0_skl,sK0_skl),nand(X1,nand(sK0_skl,sK0_skl))))))),
% 24.17/3.56 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 24.17/3.56 fof(f910,plain,(
% 24.17/3.56 ![X0]: (~p(nand(nand(sK0_skl,sK0_skl),nand(X0,nand(sK0_skl,sK0_skl))))|~sQ16_spl)),
% 24.17/3.56 inference(component_clause,[status(thm)],[f909])).
% 24.17/3.56 fof(f912,plain,(
% 24.17/3.56 sQ15_spl|sQ16_spl|~sQ10_spl),
% 24.17/3.56 inference(split_clause,[status(thm)],[f897,f906,f909,f740])).
% 24.17/3.56 fof(f913,plain,(
% 24.17/3.56 ![X0]: (~p(nand(nand(sK1_skl,sK1_skl),nand(X0,nand(sK1_skl,sK1_skl))))|~sQ15_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f907,f14])).
% 24.17/3.56 fof(f924,plain,(
% 24.17/3.56 ![X0]: (~p(nand(nand(sK1_skl,sK1_skl),nand(nand(sK1_skl,sK1_skl),X0)))|~sQ15_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f913,f12])).
% 24.17/3.56 fof(f947,plain,(
% 24.17/3.56 ![X0,X1]: (~p(nand(nand(sK1_skl,sK1_skl),nand(X0,X1)))|~sQ15_spl)),
% 24.17/3.56 inference(resolution,[status(thm)],[f924,f12])).
% 24.17/3.56 fof(f954,plain,(
% 24.17/3.56 sQ3_spl|~sQ15_spl),
% 24.17/3.56 inference(split_clause,[status(thm)],[f947,f267,f906])).
% 24.17/3.56 fof(f959,plain,(
% 24.17/3.56 ![X0]: (~p(nand(nand(sK0_skl,sK0_skl),nand(nand(sK0_skl,sK0_skl),X0)))|~sQ16_spl)),
% 24.17/3.58 inference(resolution,[status(thm)],[f910,f12])).
% 24.17/3.58 fof(f982,plain,(
% 24.17/3.58 ![X0,X1]: (~p(nand(nand(sK0_skl,sK0_skl),nand(X0,X1)))|~sQ16_spl)),
% 24.17/3.58 inference(resolution,[status(thm)],[f959,f12])).
% 24.17/3.58 fof(f989,plain,(
% 24.17/3.58 ![X0,X1]: (~p(nand(X0,nand(X1,sK0_skl)))|~sQ16_spl)),
% 24.17/3.58 inference(resolution,[status(thm)],[f982,f14])).
% 24.17/3.58 fof(f999,plain,(
% 24.17/3.58 ![X0,X1]: (~p(nand(X0,nand(sK0_skl,X1)))|~sQ16_spl)),
% 24.17/3.58 inference(resolution,[status(thm)],[f989,f12])).
% 24.17/3.58 fof(f1003,plain,(
% 24.17/3.58 ![X0,X1,X2]: (~p(nand(nand(sK0_skl,X0),nand(X1,X2)))|~sQ16_spl)),
% 24.17/3.58 inference(resolution,[status(thm)],[f999,f310])).
% 24.17/3.58 fof(f1154,plain,(
% 24.17/3.58 $false|~sQ16_spl),
% 24.17/3.58 inference(resolution,[status(thm)],[f1003,f5])).
% 24.17/3.58 fof(f1163,plain,(
% 24.17/3.58 ~sQ16_spl),
% 24.17/3.58 inference(contradiction_clause,[status(thm)],[f1154])).
% 24.17/3.58 fof(f1164,plain,(
% 24.17/3.58 $false),
% 24.17/3.58 inference(sat_refutation,[status(thm)],[f641,f655,f669,f743,f797,f912,f954,f1163])).
% 24.17/3.58 % SZS output end CNFRefutation for theBenchmark.p
% 4.54/3.64 % Elapsed time: 3.208529 seconds
% 4.54/3.64 % CPU time: 24.880526 seconds
% 4.54/3.64 % Total memory used: 316.781 MB
% 4.54/3.64 % Net memory used: 303.780 MB
%------------------------------------------------------------------------------