%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : BOO109+1 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:41 PM UTC 2026
% Result : Theorem 192.33s 24.78s
% Output : CNFRefutation 192.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 10
% Syntax : Number of formulae : 72 ( 11 unt; 7 def)
% Number of atoms : 154 ( 0 equ)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 194 ( 112 ~; 73 |; 1 &)
% ( 7 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 9 ( 8 usr; 8 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 160 ( 158 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [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))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [P,Q,R] :
( ( p(P)
& p(nand(P,nand(Q,R))) )
=> p(R) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,conjecture,
! [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)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,negated_conjecture,
~ ! [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)))))),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f5,plain,
! [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))))),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f6,plain,
! [P,Q,R] :
( p(R)
| ~ p(P)
| ~ p(nand(P,nand(Q,R))) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f7,plain,
! [R] :
( p(R)
| ! [P] :
( ~ p(P)
| ! [Q] : ~ p(nand(P,nand(Q,R))) ) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f8,plain,
! [X0,X1,X2] :
( p(X2)
| ~ p(X0)
| ~ p(nand(X0,nand(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f9,plain,
? [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)))))),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f10,plain,
~ 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)))))),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f9]) ).
fof(f11,plain,
~ 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)))))),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f12,plain,
! [X0,X1,X2] :
( p(nand(X0,nand(X0,X1)))
| ~ p(nand(X0,nand(X1,X2))) ),
inference(resolution,[status(thm)],[f5,f8]) ).
fof(f13,plain,
! [X0,X1,X2] :
( p(X1)
| ~ p(X0)
| ~ p(nand(X0,nand(X1,X2))) ),
inference(resolution,[status(thm)],[f12,f8]) ).
fof(f14,plain,
! [X0,X1,X2,X3] :
( p(nand(nand(X3,X2),nand(nand(X0,X3),nand(X0,X3))))
| ~ p(nand(X0,nand(X1,X2))) ),
inference(resolution,[status(thm)],[f13,f5]) ).
fof(f16,plain,
! [X0,X1,X2,X3] :
( p(nand(X0,X3))
| ~ p(nand(X3,X2))
| ~ p(nand(X0,nand(X1,X2))) ),
inference(resolution,[status(thm)],[f14,f13]) ).
fof(f20,plain,
! [X0,X1,X2,X3,X4] :
( ~ p(nand(X2,nand(X3,X4)))
| p(nand(X0,X2))
| ~ p(nand(X0,nand(X1,nand(X2,X3)))) ),
inference(resolution,[status(thm)],[f16,f12]) ).
fof(f23,plain,
! [X0,X1,X2,X3,X4] :
( ~ p(nand(X2,nand(X3,X4)))
| p(nand(X0,X2))
| ~ p(nand(X0,nand(X1,nand(X2,X2)))) ),
inference(resolution,[status(thm)],[f20,f12]) ).
fof(f24,plain,
! [X0,X1,X2,X3,X4] :
( p(nand(X0,nand(X2,nand(X3,X4))))
| ~ p(nand(X0,nand(X1,nand(nand(X2,nand(X3,X4)),nand(X2,nand(X3,X4)))))) ),
inference(resolution,[status(thm)],[f23,f5]) ).
fof(f25,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ p(nand(X4,nand(X5,X3)))
| p(nand(X0,nand(X2,X3)))
| ~ p(nand(X0,nand(X1,nand(nand(X2,X3),nand(X2,X3))))) ),
inference(resolution,[status(thm)],[f23,f14]) ).
fof(f53,plain,
! [X0,X1,X2,X3,X4] :
( ~ p(nand(nand(X0,nand(X1,X2)),nand(X4,X3)))
| p(nand(nand(nand(X0,nand(X1,X2)),X3),nand(X0,nand(X1,X2)))) ),
inference(resolution,[status(thm)],[f24,f14]) ).
fof(f59,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ p(nand(X4,nand(X3,X5)))
| p(nand(X0,nand(X2,X3)))
| ~ p(nand(X0,nand(X1,nand(nand(X2,X3),nand(X2,X3))))) ),
inference(resolution,[status(thm)],[f25,f12]) ).
fof(f104,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ p(nand(nand(X3,nand(X4,X5)),nand(X6,X7)))
| p(nand(X0,nand(X2,X3)))
| ~ p(nand(X0,nand(X1,nand(nand(X2,X3),nand(X2,X3))))) ),
inference(resolution,[status(thm)],[f59,f53]) ).
fof(f243,definition,
! [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))) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f244,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ p(nand(nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))),nand(X0,X1))) ),
inference(component_clause,[status(thm)],[f243]) ).
fof(f267,definition,
! [X1,X2] :
( sQ3_spl
<=> ~ p(nand(nand(sK1_skl,sK1_skl),nand(X1,X2))) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f268,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ p(nand(nand(sK1_skl,sK1_skl),nand(X0,X1))) ),
inference(component_clause,[status(thm)],[f267]) ).
fof(f296,plain,
! [X0,X1,X2,X3] :
( p(nand(X0,nand(X2,X3)))
| ~ p(nand(X0,nand(X1,nand(nand(X2,X3),nand(X2,X3))))) ),
inference(resolution,[status(thm)],[f104,f5]) ).
fof(f310,plain,
! [X0,X1,X2,X3] :
( ~ p(nand(nand(X0,X1),nand(X3,X2)))
| p(nand(nand(nand(X0,X1),X2),nand(X0,X1))) ),
inference(resolution,[status(thm)],[f296,f14]) ).
fof(f344,plain,
! [X0,X1,X2,X3,X4,X5] :
( p(nand(X4,nand(nand(X0,X1),X3)))
| ~ p(nand(X4,nand(X5,nand(X0,X1))))
| ~ p(nand(nand(X0,X1),nand(X2,X3))) ),
inference(resolution,[status(thm)],[f310,f16]) ).
fof(f583,plain,
! [X0,X1] :
( ~ 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))))))
| ~ 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)))))) ),
inference(resolution,[status(thm)],[f344,f11]) ).
fof(f635,definition,
! [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)))))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f636,plain,
! [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)))))) ),
inference(component_clause,[status(thm)],[f635]) ).
fof(f638,definition,
! [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)))))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f639,plain,
! [X0] :
( ~ sQ8_spl
| ~ 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)))))) ),
inference(component_clause,[status(thm)],[f638]) ).
fof(f641,plain,
( sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f583,f635,f638]) ).
fof(f647,plain,
( ~ sQ1_spl
| $false ),
inference(resolution,[status(thm)],[f244,f5]) ).
fof(f655,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f647]) ).
fof(f659,plain,
! [X0] :
( ~ sQ7_spl
| ~ 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))) ),
inference(resolution,[status(thm)],[f636,f12]) ).
fof(f665,plain,
! [X0,X1] :
( ~ sQ7_spl
| ~ p(nand(nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl))),nand(X0,X1))) ),
inference(resolution,[status(thm)],[f659,f12]) ).
fof(f669,plain,
( ~ sQ7_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f665,f243,f635]) ).
fof(f699,plain,
! [X0,X1,X2,X3] :
( ~ sQ8_spl
| ~ p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X3,nand(X0,X1))))
| ~ p(nand(nand(X0,X1),nand(X2,nand(nand(sK1_skl,sK1_skl),nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl)))))) ),
inference(resolution,[status(thm)],[f639,f344]) ).
fof(f713,plain,
! [X0,X1,X2] :
( ~ sQ8_spl
| ~ p(nand(nand(sK1_skl,sK1_skl),nand(X2,X1)))
| ~ 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)))) ),
inference(resolution,[status(thm)],[f699,f14]) ).
fof(f724,plain,
! [X0,X1,X2] :
( ~ sQ8_spl
| ~ p(nand(nand(sK1_skl,sK1_skl),nand(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)))) ),
inference(resolution,[status(thm)],[f713,f12]) ).
fof(f737,plain,
! [X0,X1,X2] :
( ~ sQ8_spl
| ~ p(nand(nand(sK1_skl,sK1_skl),nand(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))))) ),
inference(resolution,[status(thm)],[f724,f12]) ).
fof(f740,definition,
! [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))))) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f741,plain,
! [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))))) ),
inference(component_clause,[status(thm)],[f740]) ).
fof(f743,plain,
( ~ sQ8_spl
| sQ3_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f737,f740,f267,f638]) ).
fof(f754,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ p(nand(X0,nand(X1,sK1_skl))) ),
inference(resolution,[status(thm)],[f268,f14]) ).
fof(f764,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ p(nand(X0,nand(sK1_skl,X1))) ),
inference(resolution,[status(thm)],[f754,f12]) ).
fof(f768,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| ~ p(nand(nand(sK1_skl,X0),nand(X1,X2))) ),
inference(resolution,[status(thm)],[f764,f310]) ).
fof(f789,plain,
( ~ sQ3_spl
| $false ),
inference(resolution,[status(thm)],[f768,f5]) ).
fof(f797,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f789]) ).
fof(f798,plain,
! [X0,X1,X2,X3] :
( ~ sQ10_spl
| ~ p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X3,nand(X0,X1))))
| ~ p(nand(nand(X0,X1),nand(X2,nand(nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl)),nand(sK1_skl,sK1_skl))))) ),
inference(resolution,[status(thm)],[f741,f344]) ).
fof(f890,plain,
! [X0,X1,X2] :
( ~ sQ10_spl
| ~ p(nand(nand(nand(sK0_skl,sK0_skl),nand(sK0_skl,sK0_skl)),nand(X2,X1)))
| ~ p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(sK1_skl,sK1_skl),X1)))) ),
inference(resolution,[status(thm)],[f798,f14]) ).
fof(f897,plain,
! [X0,X1] :
( ~ sQ10_spl
| ~ p(nand(nand(sK0_skl,sK0_skl),nand(X1,nand(sK0_skl,sK0_skl))))
| ~ p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(sK1_skl,sK1_skl),sK0_skl)))) ),
inference(resolution,[status(thm)],[f890,f310]) ).
fof(f906,definition,
! [X0] :
( sQ15_spl
<=> ~ p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(sK1_skl,sK1_skl),sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f907,plain,
! [X0] :
( ~ sQ15_spl
| ~ p(nand(nand(sK0_skl,nand(sK1_skl,sK1_skl)),nand(X0,nand(nand(sK1_skl,sK1_skl),sK0_skl)))) ),
inference(component_clause,[status(thm)],[f906]) ).
fof(f909,definition,
! [X1] :
( sQ16_spl
<=> ~ p(nand(nand(sK0_skl,sK0_skl),nand(X1,nand(sK0_skl,sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f910,plain,
! [X0] :
( ~ sQ16_spl
| ~ p(nand(nand(sK0_skl,sK0_skl),nand(X0,nand(sK0_skl,sK0_skl)))) ),
inference(component_clause,[status(thm)],[f909]) ).
fof(f912,plain,
( ~ sQ10_spl
| sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f897,f906,f909,f740]) ).
fof(f913,plain,
! [X0] :
( ~ sQ15_spl
| ~ p(nand(nand(sK1_skl,sK1_skl),nand(X0,nand(sK1_skl,sK1_skl)))) ),
inference(resolution,[status(thm)],[f907,f14]) ).
fof(f924,plain,
! [X0] :
( ~ sQ15_spl
| ~ p(nand(nand(sK1_skl,sK1_skl),nand(nand(sK1_skl,sK1_skl),X0))) ),
inference(resolution,[status(thm)],[f913,f12]) ).
fof(f947,plain,
! [X0,X1] :
( ~ sQ15_spl
| ~ p(nand(nand(sK1_skl,sK1_skl),nand(X0,X1))) ),
inference(resolution,[status(thm)],[f924,f12]) ).
fof(f954,plain,
( ~ sQ15_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f947,f267,f906]) ).
fof(f959,plain,
! [X0] :
( ~ sQ16_spl
| ~ p(nand(nand(sK0_skl,sK0_skl),nand(nand(sK0_skl,sK0_skl),X0))) ),
inference(resolution,[status(thm)],[f910,f12]) ).
fof(f982,plain,
! [X0,X1] :
( ~ sQ16_spl
| ~ p(nand(nand(sK0_skl,sK0_skl),nand(X0,X1))) ),
inference(resolution,[status(thm)],[f959,f12]) ).
fof(f989,plain,
! [X0,X1] :
( ~ sQ16_spl
| ~ p(nand(X0,nand(X1,sK0_skl))) ),
inference(resolution,[status(thm)],[f982,f14]) ).
fof(f999,plain,
! [X0,X1] :
( ~ sQ16_spl
| ~ p(nand(X0,nand(sK0_skl,X1))) ),
inference(resolution,[status(thm)],[f989,f12]) ).
fof(f1003,plain,
! [X0,X1,X2] :
( ~ sQ16_spl
| ~ p(nand(nand(sK0_skl,X0),nand(X1,X2))) ),
inference(resolution,[status(thm)],[f999,f310]) ).
fof(f1154,plain,
( ~ sQ16_spl
| $false ),
inference(resolution,[status(thm)],[f1003,f5]) ).
fof(f1163,plain,
~ sQ16_spl,
inference(contradiction_clause,[status(thm)],[f1154]) ).
fof(f1164,plain,
$false,
inference(sat_refutation,[status(thm)],[f641,f655,f669,f743,f797,f912,f954,f1163]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO109+1 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n006.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 13:54:12 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 192.33/24.78 % Refutation found
% 192.33/24.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 192.33/24.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 81.12/26.05 % Elapsed time: 25.467057 seconds
% 81.12/26.05 % CPU time: 187.856409 seconds
% 81.12/26.05 % Total memory used: 939.177 MB
% 81.12/26.05 % Net memory used: 893.830 MB
%------------------------------------------------------------------------------