%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : BOO109+1 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.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 : Tue Sep 29 09:36:04 AM UTC 2026
% Result : Theorem 15.58s 3.04s
% Output : Refutation 17.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 78
% Syntax : Number of formulae : 463 ( 87 unt; 75 def)
% Number of atoms : 1185 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1624 ( 902 ~; 645 |; 1 &)
% ( 75 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 77 ( 76 usr; 76 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 926 ( 0 sgn 924 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [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))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wajsbergs_axiom) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( p(nand(X0,nand(X1,X2)))
& p(X0) )
=> p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',modus_ponens_for_nand) ).
fof(f3,conjecture,
! [X0,X1] : p(nand(nand(X0,nand(X1,X1)),nand(nand(nand(X1,X1),nand(nand(X0,X0),nand(X0,X0))),nand(nand(X1,X1),nand(nand(X0,X0),nand(X0,X0)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tautology) ).
fof(f4,negated_conjecture,
~ ! [X0,X1] : p(nand(nand(X0,nand(X1,X1)),nand(nand(nand(X1,X1),nand(nand(X0,X0),nand(X0,X0))),nand(nand(X1,X1),nand(nand(X0,X0),nand(X0,X0)))))),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f5,plain,
! [X0,X1,X2] :
( p(X2)
| ~ p(nand(X0,nand(X1,X2)))
| ~ p(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f6,plain,
! [X0,X1,X2] :
( p(X2)
| ~ p(nand(X0,nand(X1,X2)))
| ~ p(X0) ),
inference(flattening,[],[f5]) ).
fof(f7,plain,
? [X0,X1] : ~ p(nand(nand(X0,nand(X1,X1)),nand(nand(nand(X1,X1),nand(nand(X0,X0),nand(X0,X0))),nand(nand(X1,X1),nand(nand(X0,X0),nand(X0,X0)))))),
inference(ennf_transformation,[],[f4]) ).
fof(f8,plain,
~ p(nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))))),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f7]) ).
fof(f9,plain,
! [X2,X3,X0,X1] : 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,[],[f1]) ).
fof(f10,plain,
! [X2,X0,X1] :
( p(X2)
| ~ p(nand(X0,nand(X1,X2)))
| ~ p(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f11,plain,
~ p(nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))))),
inference(cnf_transformation,[],[f8]) ).
fof(f13,definition,
( spl2_1
<=> p(nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))))) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f15,plain,
( ~ p(nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| spl2_1 ),
inference(avatar_component_clause,[],[f13]) ).
fof(f16,plain,
~ spl2_1,
inference(avatar_split_clause,[],[f11,f13]) ).
fof(f17,plain,
( ! [X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))
| ~ p(X0) )
| spl2_1 ),
inference(resolution,[],[f15,f10]) ).
fof(f19,definition,
( spl2_2
<=> ! [X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))
| ~ p(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f20,plain,
( ! [X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))
| ~ p(X0) )
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f19]) ).
fof(f21,plain,
( spl2_2
| spl2_1 ),
inference(avatar_split_clause,[],[f17,f13,f19]) ).
fof(f22,plain,
( ! [X2,X3,X0,X1] :
( ~ p(X0)
| ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))))
| ~ p(X1) )
| ~ spl2_2 ),
inference(resolution,[],[f20,f10]) ).
fof(f24,definition,
( spl2_3
<=> ! [X0,X3,X2,X1] :
( ~ p(X0)
| ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))))
| ~ p(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
fof(f25,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))))
| ~ p(X0)
| ~ p(X1) )
| ~ spl2_3 ),
inference(avatar_component_clause,[],[f24]) ).
fof(f26,plain,
( spl2_3
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f22,f19,f24]) ).
fof(f28,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X2,nand(X3,nand(X1,nand(X4,nand(X0,nand(X5,nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))))))
| ~ p(X2) )
| ~ spl2_3 ),
inference(resolution,[],[f25,f10]) ).
fof(f39,definition,
( spl2_6
<=> ! [X2,X3,X4,X0,X5,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X2,nand(X3,nand(X1,nand(X4,nand(X0,nand(X5,nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))))))
| ~ p(X2) ) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f40,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(nand(X2,nand(X3,nand(X1,nand(X4,nand(X0,nand(X5,nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))))))
| ~ p(X1)
| ~ p(X0)
| ~ p(X2) )
| ~ spl2_6 ),
inference(avatar_component_clause,[],[f39]) ).
fof(f41,plain,
( spl2_6
| ~ spl2_3 ),
inference(avatar_split_clause,[],[f28,f24,f39]) ).
fof(f42,plain,
( ! [X2,X3,X0,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X0,nand(nand(X1,nand(X2,nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))),X3))) )
| ~ spl2_6 ),
inference(resolution,[],[f40,f9]) ).
fof(f45,definition,
( spl2_7
<=> ! [X0,X3,X2,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X0,nand(nand(X1,nand(X2,nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))),X3))) ) ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
fof(f46,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(nand(X1,nand(X2,nand(nand(sK0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))),X3)))
| ~ p(X1)
| ~ p(X0) )
| ~ spl2_7 ),
inference(avatar_component_clause,[],[f45]) ).
fof(f47,plain,
( spl2_7
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f42,f39,f45]) ).
fof(f48,plain,
( ! [X0,X1] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X0))
| ~ p(nand(nand(sK0,nand(sK1,sK1)),nand(X1,X0))) )
| ~ spl2_7 ),
inference(resolution,[],[f46,f9]) ).
fof(f51,definition,
( spl2_8
<=> ! [X0,X1] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X0))
| ~ p(nand(nand(sK0,nand(sK1,sK1)),nand(X1,X0))) ) ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
fof(f52,plain,
( ! [X0,X1] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X0))
| ~ p(nand(nand(sK0,nand(sK1,sK1)),nand(X1,X0))) )
| ~ spl2_8 ),
inference(avatar_component_clause,[],[f51]) ).
fof(f53,plain,
( spl2_8
| ~ spl2_7 ),
inference(avatar_split_clause,[],[f48,f45,f51]) ).
fof(f55,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(nand(sK0,nand(sK1,sK1)),nand(X0,X1)))
| ~ p(nand(X2,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X1))))
| ~ p(X2) )
| ~ spl2_8 ),
inference(resolution,[],[f52,f10]) ).
fof(f64,definition,
( spl2_10
<=> ! [X0,X3,X2,X1] :
( ~ p(nand(nand(sK0,nand(sK1,sK1)),nand(X0,X1)))
| ~ p(nand(X2,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X1))))
| ~ p(X2) ) ),
introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition]) ).
fof(f65,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X2,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X1))))
| ~ p(nand(nand(sK0,nand(sK1,sK1)),nand(X0,X1)))
| ~ p(X2) )
| ~ spl2_10 ),
inference(avatar_component_clause,[],[f64]) ).
fof(f66,plain,
( spl2_10
| ~ spl2_8 ),
inference(avatar_split_clause,[],[f55,f51,f64]) ).
fof(f67,plain,
( ! [X2,X0,X1] :
( ~ p(nand(nand(sK0,nand(sK1,sK1)),nand(X0,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X1))))
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X1,X2))) )
| ~ spl2_10 ),
inference(resolution,[],[f65,f9]) ).
fof(f70,definition,
( spl2_11
<=> ! [X2,X0,X1] :
( ~ p(nand(nand(sK0,nand(sK1,sK1)),nand(X0,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X1))))
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition]) ).
fof(f71,plain,
( ! [X2,X0,X1] :
( ~ p(nand(nand(sK0,nand(sK1,sK1)),nand(X0,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X1))))
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X1,X2))) )
| ~ spl2_11 ),
inference(avatar_component_clause,[],[f70]) ).
fof(f72,plain,
( spl2_11
| ~ spl2_10 ),
inference(avatar_split_clause,[],[f67,f64,f70]) ).
fof(f73,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X0,X1)))
| ~ p(nand(X2,nand(X3,nand(nand(sK0,nand(sK1,sK1)),nand(X4,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X0))))))
| ~ p(X2) )
| ~ spl2_11 ),
inference(resolution,[],[f71,f10]) ).
fof(f114,definition,
( spl2_19
<=> ! [X2,X4,X0,X3,X1] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X0,X1)))
| ~ p(nand(X2,nand(X3,nand(nand(sK0,nand(sK1,sK1)),nand(X4,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X0))))))
| ~ p(X2) ) ),
introduced(definition,[new_symbols(definition,[spl2_19])],[avatar_definition]) ).
fof(f115,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X2,nand(X3,nand(nand(sK0,nand(sK1,sK1)),nand(X4,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X0))))))
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X0,X1)))
| ~ p(X2) )
| ~ spl2_19 ),
inference(avatar_component_clause,[],[f114]) ).
fof(f116,plain,
( spl2_19
| ~ spl2_11 ),
inference(avatar_split_clause,[],[f73,f70,f114]) ).
fof(f118,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X0,X1)))
| ~ p(X2)
| ~ p(nand(X3,nand(X4,nand(X2,nand(X5,nand(nand(sK0,nand(sK1,sK1)),nand(X6,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X0))))))))
| ~ p(X3) )
| ~ spl2_19 ),
inference(resolution,[],[f115,f10]) ).
fof(f153,definition,
( spl2_26
<=> ! [X5,X3,X4,X0,X6,X2,X1] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X0,X1)))
| ~ p(X2)
| ~ p(nand(X3,nand(X4,nand(X2,nand(X5,nand(nand(sK0,nand(sK1,sK1)),nand(X6,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X0))))))))
| ~ p(X3) ) ),
introduced(definition,[new_symbols(definition,[spl2_26])],[avatar_definition]) ).
fof(f154,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(nand(X3,nand(X4,nand(X2,nand(X5,nand(nand(sK0,nand(sK1,sK1)),nand(X6,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X0))))))))
| ~ p(X2)
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X0,X1)))
| ~ p(X3) )
| ~ spl2_26 ),
inference(avatar_component_clause,[],[f153]) ).
fof(f155,plain,
( spl2_26
| ~ spl2_19 ),
inference(avatar_split_clause,[],[f118,f114,f153]) ).
fof(f156,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(X0)
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X1,X2)))
| ~ p(nand(X0,nand(nand(nand(sK0,nand(sK1,sK1)),nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X1))),X4))) )
| ~ spl2_26 ),
inference(resolution,[],[f154,f9]) ).
fof(f159,definition,
( spl2_27
<=> ! [X4,X0,X3,X2,X1] :
( ~ p(X0)
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X1,X2)))
| ~ p(nand(X0,nand(nand(nand(sK0,nand(sK1,sK1)),nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X1))),X4))) ) ),
introduced(definition,[new_symbols(definition,[spl2_27])],[avatar_definition]) ).
fof(f160,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X0,nand(nand(nand(sK0,nand(sK1,sK1)),nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),X1))),X4)))
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X1,X2)))
| ~ p(X0) )
| ~ spl2_27 ),
inference(avatar_component_clause,[],[f159]) ).
fof(f161,plain,
( spl2_27
| ~ spl2_26 ),
inference(avatar_split_clause,[],[f156,f153,f159]) ).
fof(f162,plain,
( ! [X0,X1] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X0)))
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X1,nand(sK1,sK1)))) )
| ~ spl2_27 ),
inference(resolution,[],[f160,f9]) ).
fof(f165,definition,
( spl2_28
<=> ! [X1] : ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X1,nand(sK1,sK1)))) ),
introduced(definition,[new_symbols(definition,[spl2_28])],[avatar_definition]) ).
fof(f166,plain,
( ! [X1] : ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X1,nand(sK1,sK1))))
| ~ spl2_28 ),
inference(avatar_component_clause,[],[f165]) ).
fof(f168,definition,
( spl2_29
<=> ! [X0] : ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X0))) ),
introduced(definition,[new_symbols(definition,[spl2_29])],[avatar_definition]) ).
fof(f169,plain,
( ! [X0] : ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X0)))
| ~ spl2_29 ),
inference(avatar_component_clause,[],[f168]) ).
fof(f170,plain,
( spl2_28
| spl2_29
| ~ spl2_27 ),
inference(avatar_split_clause,[],[f162,f159,f168,f165]) ).
fof(f171,plain,
( ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X2)))))
| ~ p(X0) )
| ~ spl2_29 ),
inference(resolution,[],[f169,f10]) ).
fof(f173,definition,
( spl2_30
<=> ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X2)))))
| ~ p(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_30])],[avatar_definition]) ).
fof(f174,plain,
( ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X2)))))
| ~ p(X0) )
| ~ spl2_30 ),
inference(avatar_component_clause,[],[f173]) ).
fof(f175,plain,
( spl2_30
| ~ spl2_29 ),
inference(avatar_split_clause,[],[f171,f168,f173]) ).
fof(f176,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(X0)
| ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X4)))))))
| ~ p(X1) )
| ~ spl2_30 ),
inference(resolution,[],[f174,f10]) ).
fof(f178,definition,
( spl2_31
<=> ! [X4,X0,X3,X2,X1] :
( ~ p(X0)
| ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X4)))))))
| ~ p(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_31])],[avatar_definition]) ).
fof(f179,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X4)))))))
| ~ p(X0)
| ~ p(X1) )
| ~ spl2_31 ),
inference(avatar_component_clause,[],[f178]) ).
fof(f180,plain,
( spl2_31
| ~ spl2_30 ),
inference(avatar_split_clause,[],[f176,f173,f178]) ).
fof(f182,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X2,nand(X3,nand(X1,nand(X4,nand(X0,nand(X5,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X6)))))))))
| ~ p(X2) )
| ~ spl2_31 ),
inference(resolution,[],[f179,f10]) ).
fof(f271,definition,
( spl2_48
<=> ! [X5,X3,X4,X2,X0,X6,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X2,nand(X3,nand(X1,nand(X4,nand(X0,nand(X5,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X6)))))))))
| ~ p(X2) ) ),
introduced(definition,[new_symbols(definition,[spl2_48])],[avatar_definition]) ).
fof(f272,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(nand(X2,nand(X3,nand(X1,nand(X4,nand(X0,nand(X5,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X6)))))))))
| ~ p(X1)
| ~ p(X0)
| ~ p(X2) )
| ~ spl2_48 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f273,plain,
( spl2_48
| ~ spl2_31 ),
inference(avatar_split_clause,[],[f182,f178,f271]) ).
fof(f274,plain,
( ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X2,nand(sK1,sK1))))))
| ~ p(X0) )
| ~ spl2_28 ),
inference(resolution,[],[f166,f10]) ).
fof(f276,definition,
( spl2_49
<=> ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X2,nand(sK1,sK1))))))
| ~ p(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_49])],[avatar_definition]) ).
fof(f277,plain,
( ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X2,nand(sK1,sK1))))))
| ~ p(X0) )
| ~ spl2_49 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f278,plain,
( spl2_49
| ~ spl2_28 ),
inference(avatar_split_clause,[],[f274,f165,f276]) ).
fof(f287,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X0,nand(nand(X1,nand(X2,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X3)))),X4))) )
| ~ spl2_48 ),
inference(resolution,[],[f272,f9]) ).
fof(f290,definition,
( spl2_51
<=> ! [X2,X4,X0,X3,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X0,nand(nand(X1,nand(X2,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X3)))),X4))) ) ),
introduced(definition,[new_symbols(definition,[spl2_51])],[avatar_definition]) ).
fof(f291,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X0,nand(nand(X1,nand(X2,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(sK0,X3)))),X4)))
| ~ p(X1)
| ~ p(X0) )
| ~ spl2_51 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f292,plain,
( spl2_51
| ~ spl2_48 ),
inference(avatar_split_clause,[],[f287,f271,f290]) ).
fof(f293,plain,
( ! [X2,X0,X1] :
( ~ p(nand(nand(sK0,X0),X1))
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X2,X1))) )
| ~ spl2_51 ),
inference(resolution,[],[f291,f9]) ).
fof(f296,definition,
( spl2_52
<=> ! [X2,X0,X1] :
( ~ p(nand(nand(sK0,X0),X1))
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X2,X1))) ) ),
introduced(definition,[new_symbols(definition,[spl2_52])],[avatar_definition]) ).
fof(f297,plain,
( ! [X2,X0,X1] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X2,X1)))
| ~ p(nand(nand(sK0,X0),X1)) )
| ~ spl2_52 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f298,plain,
( spl2_52
| ~ spl2_51 ),
inference(avatar_split_clause,[],[f293,f290,f296]) ).
fof(f316,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(X0)
| ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X4,nand(sK1,sK1))))))))
| ~ p(X1) )
| ~ spl2_49 ),
inference(resolution,[],[f277,f10]) ).
fof(f321,definition,
( spl2_55
<=> ! [X4,X0,X3,X2,X1] :
( ~ p(X0)
| ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X4,nand(sK1,sK1))))))))
| ~ p(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_55])],[avatar_definition]) ).
fof(f322,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X4,nand(sK1,sK1))))))))
| ~ p(X0)
| ~ p(X1) )
| ~ spl2_55 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f323,plain,
( spl2_55
| ~ spl2_49 ),
inference(avatar_split_clause,[],[f316,f276,f321]) ).
fof(f325,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X2,nand(X3,nand(X1,nand(X4,nand(X0,nand(X5,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X6,nand(sK1,sK1))))))))))
| ~ p(X2) )
| ~ spl2_55 ),
inference(resolution,[],[f322,f10]) ).
fof(f338,definition,
( spl2_58
<=> ! [X5,X3,X4,X2,X0,X6,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X2,nand(X3,nand(X1,nand(X4,nand(X0,nand(X5,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X6,nand(sK1,sK1))))))))))
| ~ p(X2) ) ),
introduced(definition,[new_symbols(definition,[spl2_58])],[avatar_definition]) ).
fof(f339,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(nand(X2,nand(X3,nand(X1,nand(X4,nand(X0,nand(X5,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X6,nand(sK1,sK1))))))))))
| ~ p(X1)
| ~ p(X0)
| ~ p(X2) )
| ~ spl2_58 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f340,plain,
( spl2_58
| ~ spl2_55 ),
inference(avatar_split_clause,[],[f325,f321,f338]) ).
fof(f341,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X0,nand(nand(X1,nand(X2,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X3,nand(sK1,sK1))))),X4))) )
| ~ spl2_58 ),
inference(resolution,[],[f339,f9]) ).
fof(f344,definition,
( spl2_59
<=> ! [X2,X4,X0,X3,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X0,nand(nand(X1,nand(X2,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X3,nand(sK1,sK1))))),X4))) ) ),
introduced(definition,[new_symbols(definition,[spl2_59])],[avatar_definition]) ).
fof(f345,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X0,nand(nand(X1,nand(X2,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X3,nand(sK1,sK1))))),X4)))
| ~ p(X1)
| ~ p(X0) )
| ~ spl2_59 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f346,plain,
( spl2_59
| ~ spl2_58 ),
inference(avatar_split_clause,[],[f341,f338,f344]) ).
fof(f347,plain,
( ! [X2,X0,X1] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),X1))
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X2,X1))) )
| ~ spl2_59 ),
inference(resolution,[],[f345,f9]) ).
fof(f350,definition,
( spl2_60
<=> ! [X2,X0,X1] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),X1))
| ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X2,X1))) ) ),
introduced(definition,[new_symbols(definition,[spl2_60])],[avatar_definition]) ).
fof(f351,plain,
( ! [X2,X0,X1] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X2,X1)))
| ~ p(nand(nand(X0,nand(sK1,sK1)),X1)) )
| ~ spl2_60 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f352,plain,
( spl2_60
| ~ spl2_59 ),
inference(avatar_split_clause,[],[f347,f344,f350]) ).
fof(f356,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(nand(sK0,X0),X1))
| ~ p(nand(X2,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X4,X1)))))
| ~ p(X2) )
| ~ spl2_52 ),
inference(resolution,[],[f297,f10]) ).
fof(f372,definition,
( spl2_62
<=> ! [X2,X4,X0,X3,X1] :
( ~ p(nand(nand(sK0,X0),X1))
| ~ p(nand(X2,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X4,X1)))))
| ~ p(X2) ) ),
introduced(definition,[new_symbols(definition,[spl2_62])],[avatar_definition]) ).
fof(f373,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X2,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X4,X1)))))
| ~ p(nand(nand(sK0,X0),X1))
| ~ p(X2) )
| ~ spl2_62 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f374,plain,
( spl2_62
| ~ spl2_52 ),
inference(avatar_split_clause,[],[f356,f296,f372]) ).
fof(f391,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),X1))
| ~ p(nand(X2,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X4,X1)))))
| ~ p(X2) )
| ~ spl2_60 ),
inference(resolution,[],[f351,f10]) ).
fof(f415,definition,
( spl2_65
<=> ! [X2,X4,X0,X3,X1] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),X1))
| ~ p(nand(X2,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X4,X1)))))
| ~ p(X2) ) ),
introduced(definition,[new_symbols(definition,[spl2_65])],[avatar_definition]) ).
fof(f416,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X2,nand(X3,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X4,X1)))))
| ~ p(nand(nand(X0,nand(sK1,sK1)),X1))
| ~ p(X2) )
| ~ spl2_65 ),
inference(avatar_component_clause,[],[f415]) ).
fof(f417,plain,
( spl2_65
| ~ spl2_60 ),
inference(avatar_split_clause,[],[f391,f350,f415]) ).
fof(f461,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(nand(nand(sK0,X0),X1))
| ~ p(X2)
| ~ p(nand(X3,nand(X4,nand(X2,nand(X5,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X6,X1)))))))
| ~ p(X3) )
| ~ spl2_62 ),
inference(resolution,[],[f373,f10]) ).
fof(f467,definition,
( spl2_68
<=> ! [X5,X3,X4,X0,X6,X2,X1] :
( ~ p(nand(nand(sK0,X0),X1))
| ~ p(X2)
| ~ p(nand(X3,nand(X4,nand(X2,nand(X5,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X6,X1)))))))
| ~ p(X3) ) ),
introduced(definition,[new_symbols(definition,[spl2_68])],[avatar_definition]) ).
fof(f468,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(nand(X3,nand(X4,nand(X2,nand(X5,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X6,X1)))))))
| ~ p(X2)
| ~ p(nand(nand(sK0,X0),X1))
| ~ p(X3) )
| ~ spl2_68 ),
inference(avatar_component_clause,[],[f467]) ).
fof(f469,plain,
( spl2_68
| ~ spl2_62 ),
inference(avatar_split_clause,[],[f461,f372,f467]) ).
fof(f511,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),X1))
| ~ p(X2)
| ~ p(nand(X3,nand(X4,nand(X2,nand(X5,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X6,X1)))))))
| ~ p(X3) )
| ~ spl2_65 ),
inference(resolution,[],[f416,f10]) ).
fof(f515,definition,
( spl2_71
<=> ! [X5,X3,X4,X0,X6,X2,X1] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),X1))
| ~ p(X2)
| ~ p(nand(X3,nand(X4,nand(X2,nand(X5,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X6,X1)))))))
| ~ p(X3) ) ),
introduced(definition,[new_symbols(definition,[spl2_71])],[avatar_definition]) ).
fof(f516,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(nand(X3,nand(X4,nand(X2,nand(X5,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X6,X1)))))))
| ~ p(X2)
| ~ p(nand(nand(X0,nand(sK1,sK1)),X1))
| ~ p(X3) )
| ~ spl2_71 ),
inference(avatar_component_clause,[],[f515]) ).
fof(f517,plain,
( spl2_71
| ~ spl2_65 ),
inference(avatar_split_clause,[],[f511,f415,f515]) ).
fof(f542,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(X0)
| ~ p(nand(nand(X1,nand(sK1,sK1)),X2))
| ~ p(nand(X0,nand(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X3,X2)),X4))) )
| ~ spl2_71 ),
inference(resolution,[],[f516,f9]) ).
fof(f545,definition,
( spl2_73
<=> ! [X4,X0,X3,X2,X1] :
( ~ p(X0)
| ~ p(nand(nand(X1,nand(sK1,sK1)),X2))
| ~ p(nand(X0,nand(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X3,X2)),X4))) ) ),
introduced(definition,[new_symbols(definition,[spl2_73])],[avatar_definition]) ).
fof(f546,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X0,nand(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X3,X2)),X4)))
| ~ p(nand(nand(X1,nand(sK1,sK1)),X2))
| ~ p(X0) )
| ~ spl2_73 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f547,plain,
( spl2_73
| ~ spl2_71 ),
inference(avatar_split_clause,[],[f542,f515,f545]) ).
fof(f561,plain,
( ! [X2,X0,X1] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(X1,nand(X2,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))))) )
| ~ spl2_73 ),
inference(resolution,[],[f546,f9]) ).
fof(f564,definition,
( spl2_75
<=> ! [X2,X0,X1] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(X1,nand(X2,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))))) ) ),
introduced(definition,[new_symbols(definition,[spl2_75])],[avatar_definition]) ).
fof(f565,plain,
( ! [X2,X0,X1] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(X1,nand(X2,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))))) )
| ~ spl2_75 ),
inference(avatar_component_clause,[],[f564]) ).
fof(f566,plain,
( spl2_75
| ~ spl2_73 ),
inference(avatar_split_clause,[],[f561,f545,f564]) ).
fof(f578,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(X2,nand(X3,nand(nand(X4,nand(sK1,sK1)),nand(X0,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))
| ~ p(X2) )
| ~ spl2_75 ),
inference(resolution,[],[f565,f10]) ).
fof(f584,definition,
( spl2_77
<=> ! [X2,X4,X0,X3,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(X2,nand(X3,nand(nand(X4,nand(sK1,sK1)),nand(X0,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))
| ~ p(X2) ) ),
introduced(definition,[new_symbols(definition,[spl2_77])],[avatar_definition]) ).
fof(f585,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X2,nand(X3,nand(nand(X4,nand(sK1,sK1)),nand(X0,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))
| ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(X2) )
| ~ spl2_77 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f586,plain,
( spl2_77
| ~ spl2_75 ),
inference(avatar_split_clause,[],[f578,f564,f584]) ).
fof(f616,plain,
( ! [X2,X0,X1] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(nand(X0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X2))) )
| ~ spl2_77 ),
inference(resolution,[],[f585,f9]) ).
fof(f619,definition,
( spl2_79
<=> ! [X2,X0,X1] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(nand(X0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X2))) ) ),
introduced(definition,[new_symbols(definition,[spl2_79])],[avatar_definition]) ).
fof(f620,plain,
( ! [X2,X0,X1] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X2)))
| ~ p(nand(nand(X0,nand(sK1,sK1)),nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))))) )
| ~ spl2_79 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f621,plain,
( spl2_79
| ~ spl2_77 ),
inference(avatar_split_clause,[],[f616,f584,f619]) ).
fof(f649,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(X2,nand(X3,nand(nand(X0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X4)))))
| ~ p(X2) )
| ~ spl2_79 ),
inference(resolution,[],[f620,f10]) ).
fof(f824,plain,
( ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ p(X0)
| ~ p(nand(nand(sK0,X1),X2))
| ~ p(X3)
| ~ p(nand(X4,nand(X5,nand(X3,nand(X6,nand(X0,nand(X7,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X8,X2)))))))))
| ~ p(X4) )
| ~ spl2_68 ),
inference(resolution,[],[f468,f10]) ).
fof(f882,definition,
( spl2_98
<=> ! [X2,X4,X0,X3,X1] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(X2,nand(X3,nand(nand(X0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X4)))))
| ~ p(X2) ) ),
introduced(definition,[new_symbols(definition,[spl2_98])],[avatar_definition]) ).
fof(f883,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X2,nand(X3,nand(nand(X0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X4)))))
| ~ p(nand(nand(X0,nand(sK1,sK1)),nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(X2) )
| ~ spl2_98 ),
inference(avatar_component_clause,[],[f882]) ).
fof(f884,plain,
( spl2_98
| ~ spl2_79 ),
inference(avatar_split_clause,[],[f649,f619,f882]) ).
fof(f885,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(X2)
| ~ p(nand(X3,nand(X4,nand(X2,nand(X5,nand(nand(X0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X6)))))))
| ~ p(X3) )
| ~ spl2_98 ),
inference(resolution,[],[f883,f10]) ).
fof(f887,definition,
( spl2_99
<=> ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ p(X0)
| ~ p(nand(nand(sK0,X1),X2))
| ~ p(X3)
| ~ p(nand(X4,nand(X5,nand(X3,nand(X6,nand(X0,nand(X7,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X8,X2)))))))))
| ~ p(X4) ) ),
introduced(definition,[new_symbols(definition,[spl2_99])],[avatar_definition]) ).
fof(f888,plain,
( ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ p(nand(X4,nand(X5,nand(X3,nand(X6,nand(X0,nand(X7,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X8,X2)))))))))
| ~ p(nand(nand(sK0,X1),X2))
| ~ p(X3)
| ~ p(X0)
| ~ p(X4) )
| ~ spl2_99 ),
inference(avatar_component_clause,[],[f887]) ).
fof(f889,plain,
( spl2_99
| ~ spl2_68 ),
inference(avatar_split_clause,[],[f824,f467,f887]) ).
fof(f890,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(nand(nand(sK0,X0),X1))
| ~ p(X2)
| ~ p(X3)
| ~ p(nand(X2,nand(nand(X3,nand(X4,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X5,X1)))),X6))) )
| ~ spl2_99 ),
inference(resolution,[],[f888,f9]) ).
fof(f893,definition,
( spl2_100
<=> ! [X5,X6,X4,X0,X3,X2,X1] :
( ~ p(nand(nand(sK0,X0),X1))
| ~ p(X2)
| ~ p(X3)
| ~ p(nand(X2,nand(nand(X3,nand(X4,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X5,X1)))),X6))) ) ),
introduced(definition,[new_symbols(definition,[spl2_100])],[avatar_definition]) ).
fof(f894,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(nand(X2,nand(nand(X3,nand(X4,nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X5,X1)))),X6)))
| ~ p(X2)
| ~ p(X3)
| ~ p(nand(nand(sK0,X0),X1)) )
| ~ spl2_100 ),
inference(avatar_component_clause,[],[f893]) ).
fof(f895,plain,
( spl2_100
| ~ spl2_99 ),
inference(avatar_split_clause,[],[f890,f887,f893]) ).
fof(f896,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X0,X1)))
| ~ p(nand(nand(X2,X3),X1))
| ~ p(nand(nand(sK0,X4),X3)) )
| ~ spl2_100 ),
inference(resolution,[],[f894,f9]) ).
fof(f899,definition,
( spl2_101
<=> ! [X4,X0,X3,X2,X1] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X0,X1)))
| ~ p(nand(nand(X2,X3),X1))
| ~ p(nand(nand(sK0,X4),X3)) ) ),
introduced(definition,[new_symbols(definition,[spl2_101])],[avatar_definition]) ).
fof(f900,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))),nand(X0,X1)))
| ~ p(nand(nand(X2,X3),X1))
| ~ p(nand(nand(sK0,X4),X3)) )
| ~ spl2_101 ),
inference(avatar_component_clause,[],[f899]) ).
fof(f901,plain,
( spl2_101
| ~ spl2_100 ),
inference(avatar_split_clause,[],[f896,f893,f899]) ).
fof(f954,definition,
( spl2_111
<=> ! [X5,X3,X4,X0,X6,X2,X1] :
( ~ p(nand(nand(X0,nand(sK1,sK1)),nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(X2)
| ~ p(nand(X3,nand(X4,nand(X2,nand(X5,nand(nand(X0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X6)))))))
| ~ p(X3) ) ),
introduced(definition,[new_symbols(definition,[spl2_111])],[avatar_definition]) ).
fof(f955,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(nand(X3,nand(X4,nand(X2,nand(X5,nand(nand(X0,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X6)))))))
| ~ p(X2)
| ~ p(nand(nand(X0,nand(sK1,sK1)),nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(X3) )
| ~ spl2_111 ),
inference(avatar_component_clause,[],[f954]) ).
fof(f956,plain,
( spl2_111
| ~ spl2_98 ),
inference(avatar_split_clause,[],[f885,f882,f954]) ).
fof(f957,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(X0)
| ~ p(nand(nand(X1,nand(sK1,sK1)),nand(X2,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(X0,nand(nand(nand(X1,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X3)),X4))) )
| ~ spl2_111 ),
inference(resolution,[],[f955,f9]) ).
fof(f960,definition,
( spl2_112
<=> ! [X4,X0,X3,X2,X1] :
( ~ p(X0)
| ~ p(nand(nand(X1,nand(sK1,sK1)),nand(X2,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(X0,nand(nand(nand(X1,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X3)),X4))) ) ),
introduced(definition,[new_symbols(definition,[spl2_112])],[avatar_definition]) ).
fof(f961,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X0,nand(nand(nand(X1,nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X3)),X4)))
| ~ p(nand(nand(X1,nand(sK1,sK1)),nand(X2,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(X0) )
| ~ spl2_112 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f962,plain,
( spl2_112
| ~ spl2_111 ),
inference(avatar_split_clause,[],[f957,f954,f960]) ).
fof(f963,plain,
( ! [X0,X1] :
( ~ p(nand(nand(nand(nand(sK0,sK0),nand(sK0,sK0)),nand(sK1,sK1)),nand(X0,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(nand(sK1,sK1),nand(X1,nand(sK1,sK1)))) )
| ~ spl2_112 ),
inference(resolution,[],[f961,f9]) ).
fof(f966,definition,
( spl2_113
<=> ! [X1] : ~ p(nand(nand(sK1,sK1),nand(X1,nand(sK1,sK1)))) ),
introduced(definition,[new_symbols(definition,[spl2_113])],[avatar_definition]) ).
fof(f967,plain,
( ! [X1] : ~ p(nand(nand(sK1,sK1),nand(X1,nand(sK1,sK1))))
| ~ spl2_113 ),
inference(avatar_component_clause,[],[f966]) ).
fof(f969,definition,
( spl2_114
<=> ! [X0] : ~ p(nand(nand(nand(nand(sK0,sK0),nand(sK0,sK0)),nand(sK1,sK1)),nand(X0,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))))) ),
introduced(definition,[new_symbols(definition,[spl2_114])],[avatar_definition]) ).
fof(f970,plain,
( ! [X0] : ~ p(nand(nand(nand(nand(sK0,sK0),nand(sK0,sK0)),nand(sK1,sK1)),nand(X0,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ spl2_114 ),
inference(avatar_component_clause,[],[f969]) ).
fof(f971,plain,
( spl2_113
| spl2_114
| ~ spl2_112 ),
inference(avatar_split_clause,[],[f963,f960,f969,f966]) ).
fof(f972,plain,
( ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(X2,nand(sK1,sK1))))))
| ~ p(X0) )
| ~ spl2_113 ),
inference(resolution,[],[f967,f10]) ).
fof(f974,definition,
( spl2_115
<=> ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(X2,nand(sK1,sK1))))))
| ~ p(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_115])],[avatar_definition]) ).
fof(f975,plain,
( ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(X2,nand(sK1,sK1))))))
| ~ p(X0) )
| ~ spl2_115 ),
inference(avatar_component_clause,[],[f974]) ).
fof(f976,plain,
( spl2_115
| ~ spl2_113 ),
inference(avatar_split_clause,[],[f972,f966,f974]) ).
fof(f977,plain,
( ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(nand(nand(sK0,sK0),nand(sK0,sK0)),nand(sK1,sK1)),nand(X2,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))
| ~ p(X0) )
| ~ spl2_114 ),
inference(resolution,[],[f970,f10]) ).
fof(f979,definition,
( spl2_116
<=> ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(nand(nand(sK0,sK0),nand(sK0,sK0)),nand(sK1,sK1)),nand(X2,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))
| ~ p(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_116])],[avatar_definition]) ).
fof(f980,plain,
( ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(nand(nand(sK0,sK0),nand(sK0,sK0)),nand(sK1,sK1)),nand(X2,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))))
| ~ p(X0) )
| ~ spl2_116 ),
inference(avatar_component_clause,[],[f979]) ).
fof(f981,plain,
( spl2_116
| ~ spl2_114 ),
inference(avatar_split_clause,[],[f977,f969,f979]) ).
fof(f982,plain,
( ! [X0] : ~ p(nand(nand(nand(nand(sK0,sK0),nand(sK0,sK0)),nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X0)))
| ~ spl2_116 ),
inference(resolution,[],[f980,f9]) ).
fof(f985,definition,
( spl2_117
<=> ! [X0] : ~ p(nand(nand(nand(nand(sK0,sK0),nand(sK0,sK0)),nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X0))) ),
introduced(definition,[new_symbols(definition,[spl2_117])],[avatar_definition]) ).
fof(f986,plain,
( ! [X0] : ~ p(nand(nand(nand(nand(sK0,sK0),nand(sK0,sK0)),nand(sK1,sK1)),nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),X0)))
| ~ spl2_117 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f987,plain,
( spl2_117
| ~ spl2_116 ),
inference(avatar_split_clause,[],[f982,f979,f985]) ).
fof(f994,plain,
( ! [X0] : ~ p(nand(nand(sK1,sK1),nand(nand(sK1,sK1),X0)))
| ~ spl2_115 ),
inference(resolution,[],[f975,f9]) ).
fof(f997,definition,
( spl2_119
<=> ! [X0] : ~ p(nand(nand(sK1,sK1),nand(nand(sK1,sK1),X0))) ),
introduced(definition,[new_symbols(definition,[spl2_119])],[avatar_definition]) ).
fof(f998,plain,
( ! [X0] : ~ p(nand(nand(sK1,sK1),nand(nand(sK1,sK1),X0)))
| ~ spl2_119 ),
inference(avatar_component_clause,[],[f997]) ).
fof(f999,plain,
( spl2_119
| ~ spl2_115 ),
inference(avatar_split_clause,[],[f994,f974,f997]) ).
fof(f1000,plain,
( ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(nand(sK1,sK1),X2)))))
| ~ p(X0) )
| ~ spl2_119 ),
inference(resolution,[],[f998,f10]) ).
fof(f1002,definition,
( spl2_120
<=> ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(nand(sK1,sK1),X2)))))
| ~ p(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_120])],[avatar_definition]) ).
fof(f1003,plain,
( ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(nand(sK1,sK1),X2)))))
| ~ p(X0) )
| ~ spl2_120 ),
inference(avatar_component_clause,[],[f1002]) ).
fof(f1004,plain,
( spl2_120
| ~ spl2_119 ),
inference(avatar_split_clause,[],[f1000,f997,f1002]) ).
fof(f1005,plain,
( ! [X0,X1] : ~ p(nand(nand(sK1,sK1),nand(X0,X1)))
| ~ spl2_120 ),
inference(resolution,[],[f1003,f9]) ).
fof(f1008,definition,
( spl2_121
<=> ! [X0,X1] : ~ p(nand(nand(sK1,sK1),nand(X0,X1))) ),
introduced(definition,[new_symbols(definition,[spl2_121])],[avatar_definition]) ).
fof(f1009,plain,
( ! [X0,X1] : ~ p(nand(nand(sK1,sK1),nand(X0,X1)))
| ~ spl2_121 ),
inference(avatar_component_clause,[],[f1008]) ).
fof(f1010,plain,
( spl2_121
| ~ spl2_120 ),
inference(avatar_split_clause,[],[f1005,f1002,f1008]) ).
fof(f1011,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(X2,X3)))))
| ~ p(X0) )
| ~ spl2_121 ),
inference(resolution,[],[f1009,f10]) ).
fof(f1013,definition,
( spl2_122
<=> ! [X0,X3,X2,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(X2,X3)))))
| ~ p(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_122])],[avatar_definition]) ).
fof(f1014,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(X2,X3)))))
| ~ p(X0) )
| ~ spl2_122 ),
inference(avatar_component_clause,[],[f1013]) ).
fof(f1015,plain,
( spl2_122
| ~ spl2_121 ),
inference(avatar_split_clause,[],[f1011,f1008,f1013]) ).
fof(f1017,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(X0)
| ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(nand(sK1,sK1),nand(X4,X5)))))))
| ~ p(X1) )
| ~ spl2_122 ),
inference(resolution,[],[f1014,f10]) ).
fof(f1027,definition,
( spl2_125
<=> ! [X2,X4,X0,X5,X3,X1] :
( ~ p(X0)
| ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(nand(sK1,sK1),nand(X4,X5)))))))
| ~ p(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_125])],[avatar_definition]) ).
fof(f1028,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(nand(sK1,sK1),nand(X4,X5)))))))
| ~ p(X0)
| ~ p(X1) )
| ~ spl2_125 ),
inference(avatar_component_clause,[],[f1027]) ).
fof(f1029,plain,
( spl2_125
| ~ spl2_122 ),
inference(avatar_split_clause,[],[f1017,f1013,f1027]) ).
fof(f1030,plain,
( ! [X2,X3,X0,X1] :
( ~ p(X0)
| ~ p(nand(X0,nand(nand(nand(sK1,sK1),nand(X1,X2)),X3))) )
| ~ spl2_125 ),
inference(resolution,[],[f1028,f9]) ).
fof(f1033,definition,
( spl2_126
<=> ! [X0,X3,X2,X1] :
( ~ p(X0)
| ~ p(nand(X0,nand(nand(nand(sK1,sK1),nand(X1,X2)),X3))) ) ),
introduced(definition,[new_symbols(definition,[spl2_126])],[avatar_definition]) ).
fof(f1034,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(nand(nand(sK1,sK1),nand(X1,X2)),X3)))
| ~ p(X0) )
| ~ spl2_126 ),
inference(avatar_component_clause,[],[f1033]) ).
fof(f1035,plain,
( spl2_126
| ~ spl2_125 ),
inference(avatar_split_clause,[],[f1030,f1027,f1033]) ).
fof(f1036,plain,
( ! [X0,X1] : ~ p(nand(X0,nand(X1,sK1)))
| ~ spl2_126 ),
inference(resolution,[],[f1034,f9]) ).
fof(f1039,definition,
( spl2_127
<=> ! [X0,X1] : ~ p(nand(X0,nand(X1,sK1))) ),
introduced(definition,[new_symbols(definition,[spl2_127])],[avatar_definition]) ).
fof(f1040,plain,
( ! [X0,X1] : ~ p(nand(X0,nand(X1,sK1)))
| ~ spl2_127 ),
inference(avatar_component_clause,[],[f1039]) ).
fof(f1041,plain,
( spl2_127
| ~ spl2_126 ),
inference(avatar_split_clause,[],[f1036,f1033,f1039]) ).
fof(f1042,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(X2,nand(X3,sK1)))))
| ~ p(X0) )
| ~ spl2_127 ),
inference(resolution,[],[f1040,f10]) ).
fof(f1044,definition,
( spl2_128
<=> ! [X0,X3,X2,X1] :
( ~ p(nand(X0,nand(X1,nand(X2,nand(X3,sK1)))))
| ~ p(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_128])],[avatar_definition]) ).
fof(f1045,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(X2,nand(X3,sK1)))))
| ~ p(X0) )
| ~ spl2_128 ),
inference(avatar_component_clause,[],[f1044]) ).
fof(f1046,plain,
( spl2_128
| ~ spl2_127 ),
inference(avatar_split_clause,[],[f1042,f1039,f1044]) ).
fof(f1047,plain,
( ! [X0,X1] : ~ p(nand(X0,nand(sK1,X1)))
| ~ spl2_128 ),
inference(resolution,[],[f1045,f9]) ).
fof(f1050,definition,
( spl2_129
<=> ! [X0,X1] : ~ p(nand(X0,nand(sK1,X1))) ),
introduced(definition,[new_symbols(definition,[spl2_129])],[avatar_definition]) ).
fof(f1051,plain,
( ! [X0,X1] : ~ p(nand(X0,nand(sK1,X1)))
| ~ spl2_129 ),
inference(avatar_component_clause,[],[f1050]) ).
fof(f1052,plain,
( spl2_129
| ~ spl2_128 ),
inference(avatar_split_clause,[],[f1047,f1044,f1050]) ).
fof(f1053,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(X2,nand(sK1,X3)))))
| ~ p(X0) )
| ~ spl2_129 ),
inference(resolution,[],[f1051,f10]) ).
fof(f1055,definition,
( spl2_130
<=> ! [X0,X3,X2,X1] :
( ~ p(nand(X0,nand(X1,nand(X2,nand(sK1,X3)))))
| ~ p(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_130])],[avatar_definition]) ).
fof(f1056,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(X2,nand(sK1,X3)))))
| ~ p(X0) )
| ~ spl2_130 ),
inference(avatar_component_clause,[],[f1055]) ).
fof(f1057,plain,
( spl2_130
| ~ spl2_129 ),
inference(avatar_split_clause,[],[f1053,f1050,f1055]) ).
fof(f1059,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(X0)
| ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(X4,nand(sK1,X5)))))))
| ~ p(X1) )
| ~ spl2_130 ),
inference(resolution,[],[f1056,f10]) ).
fof(f1072,definition,
( spl2_133
<=> ! [X2,X4,X0,X5,X3,X1] :
( ~ p(X0)
| ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(X4,nand(sK1,X5)))))))
| ~ p(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_133])],[avatar_definition]) ).
fof(f1073,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(nand(X1,nand(X2,nand(X0,nand(X3,nand(X4,nand(sK1,X5)))))))
| ~ p(X0)
| ~ p(X1) )
| ~ spl2_133 ),
inference(avatar_component_clause,[],[f1072]) ).
fof(f1074,plain,
( spl2_133
| ~ spl2_130 ),
inference(avatar_split_clause,[],[f1059,f1055,f1072]) ).
fof(f1075,plain,
( ! [X2,X3,X0,X1] :
( ~ p(X0)
| ~ p(nand(X0,nand(nand(X1,nand(sK1,X2)),X3))) )
| ~ spl2_133 ),
inference(resolution,[],[f1073,f9]) ).
fof(f1078,definition,
( spl2_134
<=> ! [X0,X3,X2,X1] :
( ~ p(X0)
| ~ p(nand(X0,nand(nand(X1,nand(sK1,X2)),X3))) ) ),
introduced(definition,[new_symbols(definition,[spl2_134])],[avatar_definition]) ).
fof(f1079,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(nand(X1,nand(sK1,X2)),X3)))
| ~ p(X0) )
| ~ spl2_134 ),
inference(avatar_component_clause,[],[f1078]) ).
fof(f1080,plain,
( spl2_134
| ~ spl2_133 ),
inference(avatar_split_clause,[],[f1075,f1072,f1078]) ).
fof(f1081,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(X0)
| ~ p(nand(X1,nand(X2,nand(X0,nand(nand(X3,nand(sK1,X4)),X5)))))
| ~ p(X1) )
| ~ spl2_134 ),
inference(resolution,[],[f1079,f10]) ).
fof(f1098,definition,
( spl2_138
<=> ! [X2,X4,X0,X5,X3,X1] :
( ~ p(X0)
| ~ p(nand(X1,nand(X2,nand(X0,nand(nand(X3,nand(sK1,X4)),X5)))))
| ~ p(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_138])],[avatar_definition]) ).
fof(f1099,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(nand(X1,nand(X2,nand(X0,nand(nand(X3,nand(sK1,X4)),X5)))))
| ~ p(X0)
| ~ p(X1) )
| ~ spl2_138 ),
inference(avatar_component_clause,[],[f1098]) ).
fof(f1100,plain,
( spl2_138
| ~ spl2_134 ),
inference(avatar_split_clause,[],[f1081,f1078,f1098]) ).
fof(f1102,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X2,nand(X3,nand(X1,nand(X4,nand(X0,nand(nand(X5,nand(sK1,X6)),X7)))))))
| ~ p(X2) )
| ~ spl2_138 ),
inference(resolution,[],[f1099,f10]) ).
fof(f1123,definition,
( spl2_142
<=> ! [X5,X3,X4,X2,X0,X6,X1,X7] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X2,nand(X3,nand(X1,nand(X4,nand(X0,nand(nand(X5,nand(sK1,X6)),X7)))))))
| ~ p(X2) ) ),
introduced(definition,[new_symbols(definition,[spl2_142])],[avatar_definition]) ).
fof(f1124,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ p(nand(X2,nand(X3,nand(X1,nand(X4,nand(X0,nand(nand(X5,nand(sK1,X6)),X7)))))))
| ~ p(X1)
| ~ p(X0)
| ~ p(X2) )
| ~ spl2_142 ),
inference(avatar_component_clause,[],[f1123]) ).
fof(f1125,plain,
( spl2_142
| ~ spl2_138 ),
inference(avatar_split_clause,[],[f1102,f1098,f1123]) ).
fof(f1126,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X0,nand(nand(X1,nand(nand(X2,nand(sK1,X3)),X4)),X5))) )
| ~ spl2_142 ),
inference(resolution,[],[f1124,f9]) ).
fof(f1129,definition,
( spl2_143
<=> ! [X2,X3,X4,X0,X5,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(nand(X0,nand(nand(X1,nand(nand(X2,nand(sK1,X3)),X4)),X5))) ) ),
introduced(definition,[new_symbols(definition,[spl2_143])],[avatar_definition]) ).
fof(f1130,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(nand(X0,nand(nand(X1,nand(nand(X2,nand(sK1,X3)),X4)),X5)))
| ~ p(X1)
| ~ p(X0) )
| ~ spl2_143 ),
inference(avatar_component_clause,[],[f1129]) ).
fof(f1131,plain,
( spl2_143
| ~ spl2_142 ),
inference(avatar_split_clause,[],[f1126,f1123,f1129]) ).
fof(f1132,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(nand(sK1,X0),X1))
| ~ p(nand(X2,nand(X3,X1))) )
| ~ spl2_143 ),
inference(resolution,[],[f1130,f9]) ).
fof(f1135,definition,
( spl2_144
<=> ! [X2,X0,X1,X3] :
( ~ p(nand(nand(sK1,X0),X1))
| ~ p(nand(X2,nand(X3,X1))) ) ),
introduced(definition,[new_symbols(definition,[spl2_144])],[avatar_definition]) ).
fof(f1136,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(nand(sK1,X0),X1))
| ~ p(nand(X2,nand(X3,X1))) )
| ~ spl2_144 ),
inference(avatar_component_clause,[],[f1135]) ).
fof(f1137,plain,
( spl2_144
| ~ spl2_143 ),
inference(avatar_split_clause,[],[f1132,f1129,f1135]) ).
fof(f1138,plain,
( ! [X2,X3,X0,X1,X4] : ~ p(nand(X0,nand(X1,nand(nand(nand(X2,X3),nand(nand(sK1,X2),nand(sK1,X2))),nand(sK1,nand(sK1,X4))))))
| ~ spl2_144 ),
inference(resolution,[],[f1136,f9]) ).
fof(f1145,definition,
( spl2_146
<=> ! [X4,X0,X3,X2,X1] : ~ p(nand(X0,nand(X1,nand(nand(nand(X2,X3),nand(nand(sK1,X2),nand(sK1,X2))),nand(sK1,nand(sK1,X4)))))) ),
introduced(definition,[new_symbols(definition,[spl2_146])],[avatar_definition]) ).
fof(f1146,plain,
( ! [X2,X3,X0,X1,X4] : ~ p(nand(X0,nand(X1,nand(nand(nand(X2,X3),nand(nand(sK1,X2),nand(sK1,X2))),nand(sK1,nand(sK1,X4))))))
| ~ spl2_146 ),
inference(avatar_component_clause,[],[f1145]) ).
fof(f1147,plain,
( spl2_146
| ~ spl2_144 ),
inference(avatar_split_clause,[],[f1138,f1135,f1145]) ).
fof(f1222,definition,
( spl2_159
<=> ! [X0,X3,X2,X1] : p(nand(nand(X0,nand(X1,X2)),nand(nand(nand(X3,X2),nand(nand(X0,X3),nand(X0,X3))),nand(X0,nand(X0,X1))))) ),
introduced(definition,[new_symbols(definition,[spl2_159])],[avatar_definition]) ).
fof(f1223,plain,
( ! [X2,X3,X0,X1] : p(nand(nand(X0,nand(X1,X2)),nand(nand(nand(X3,X2),nand(nand(X0,X3),nand(X0,X3))),nand(X0,nand(X0,X1)))))
| ~ spl2_159 ),
inference(avatar_component_clause,[],[f1222]) ).
fof(f1224,plain,
spl2_159,
inference(avatar_split_clause,[],[f9,f1222]) ).
fof(f1225,plain,
( ! [X2,X0,X1] :
( p(nand(X0,nand(X0,X1)))
| ~ p(nand(X0,nand(X1,X2))) )
| ~ spl2_159 ),
inference(resolution,[],[f1223,f10]) ).
fof(f1228,definition,
( spl2_160
<=> ! [X2,X0,X1] :
( p(nand(X0,nand(X0,X1)))
| ~ p(nand(X0,nand(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[spl2_160])],[avatar_definition]) ).
fof(f1229,plain,
( ! [X2,X0,X1] :
( ~ p(nand(X0,nand(X1,X2)))
| p(nand(X0,nand(X0,X1))) )
| ~ spl2_160 ),
inference(avatar_component_clause,[],[f1228]) ).
fof(f1230,plain,
( spl2_160
| ~ spl2_159 ),
inference(avatar_split_clause,[],[f1225,f1222,f1228]) ).
fof(f1231,plain,
( ! [X2,X3,X0,X1] : p(nand(nand(X0,nand(X1,X2)),nand(nand(X0,nand(X1,X2)),nand(nand(X3,X2),nand(nand(X0,X3),nand(X0,X3))))))
| ~ spl2_159
| ~ spl2_160 ),
inference(resolution,[],[f1229,f1223]) ).
fof(f1234,definition,
( spl2_161
<=> ! [X0,X3,X2,X1] : p(nand(nand(X0,nand(X1,X2)),nand(nand(X0,nand(X1,X2)),nand(nand(X3,X2),nand(nand(X0,X3),nand(X0,X3)))))) ),
introduced(definition,[new_symbols(definition,[spl2_161])],[avatar_definition]) ).
fof(f1235,plain,
( ! [X2,X3,X0,X1] : p(nand(nand(X0,nand(X1,X2)),nand(nand(X0,nand(X1,X2)),nand(nand(X3,X2),nand(nand(X0,X3),nand(X0,X3))))))
| ~ spl2_161 ),
inference(avatar_component_clause,[],[f1234]) ).
fof(f1236,plain,
( spl2_161
| ~ spl2_159
| ~ spl2_160 ),
inference(avatar_split_clause,[],[f1231,f1228,f1222,f1234]) ).
fof(f1297,plain,
( ! [X2,X0,X1] : p(nand(nand(X0,nand(X1,X2)),nand(nand(X0,nand(X1,X2)),nand(X0,nand(X1,X2)))))
| ~ spl2_160
| ~ spl2_161 ),
inference(resolution,[],[f1235,f1229]) ).
fof(f1298,plain,
( ! [X2,X3,X0,X1] :
( p(nand(nand(X0,X1),nand(nand(X2,X0),nand(X2,X0))))
| ~ p(nand(X2,nand(X3,X1))) )
| ~ spl2_161 ),
inference(resolution,[],[f1235,f10]) ).
fof(f1307,definition,
( spl2_163
<=> ! [X0,X3,X2,X1] :
( p(nand(nand(X0,X1),nand(nand(X2,X0),nand(X2,X0))))
| ~ p(nand(X2,nand(X3,X1))) ) ),
introduced(definition,[new_symbols(definition,[spl2_163])],[avatar_definition]) ).
fof(f1308,plain,
( ! [X2,X3,X0,X1] :
( p(nand(nand(X0,X1),nand(nand(X2,X0),nand(X2,X0))))
| ~ p(nand(X2,nand(X3,X1))) )
| ~ spl2_163 ),
inference(avatar_component_clause,[],[f1307]) ).
fof(f1309,plain,
( spl2_163
| ~ spl2_161 ),
inference(avatar_split_clause,[],[f1298,f1234,f1307]) ).
fof(f1316,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(nand(X2,X3),nand(X0,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(nand(sK0,X4),X3)) )
| ~ spl2_101
| ~ spl2_163 ),
inference(resolution,[],[f1308,f900]) ).
fof(f1321,plain,
( ! [X0] : ~ p(nand(nand(sK1,sK1),nand(X0,nand(sK1,sK1))))
| ~ spl2_117
| ~ spl2_163 ),
inference(resolution,[],[f1308,f986]) ).
fof(f1387,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(X1,X2)))
| p(nand(nand(X3,X2),nand(nand(X3,X2),nand(X0,X3)))) )
| ~ spl2_160
| ~ spl2_163 ),
inference(resolution,[],[f1308,f1229]) ).
fof(f1388,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(X1,X2)))
| p(nand(X0,X3))
| ~ p(nand(X3,X2)) )
| ~ spl2_163 ),
inference(resolution,[],[f1308,f10]) ).
fof(f1392,definition,
( spl2_164
<=> ! [X0,X3,X2,X1] :
( ~ p(nand(X0,nand(X1,X2)))
| p(nand(nand(X3,X2),nand(nand(X3,X2),nand(X0,X3)))) ) ),
introduced(definition,[new_symbols(definition,[spl2_164])],[avatar_definition]) ).
fof(f1393,plain,
( ! [X2,X3,X0,X1] :
( p(nand(nand(X3,X2),nand(nand(X3,X2),nand(X0,X3))))
| ~ p(nand(X0,nand(X1,X2))) )
| ~ spl2_164 ),
inference(avatar_component_clause,[],[f1392]) ).
fof(f1394,plain,
( spl2_164
| ~ spl2_160
| ~ spl2_163 ),
inference(avatar_split_clause,[],[f1387,f1307,f1228,f1392]) ).
fof(f1556,definition,
( spl2_166
<=> ! [X0,X3,X2,X1] :
( ~ p(nand(X0,nand(X1,X2)))
| p(nand(X0,X3))
| ~ p(nand(X3,X2)) ) ),
introduced(definition,[new_symbols(definition,[spl2_166])],[avatar_definition]) ).
fof(f1557,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(X1,X2)))
| p(nand(X0,X3))
| ~ p(nand(X3,X2)) )
| ~ spl2_166 ),
inference(avatar_component_clause,[],[f1556]) ).
fof(f1558,plain,
( spl2_166
| ~ spl2_163 ),
inference(avatar_split_clause,[],[f1388,f1307,f1556]) ).
fof(f1560,definition,
( spl2_167
<=> ! [X2,X0,X1] : p(nand(nand(X0,nand(X1,X2)),nand(nand(X0,nand(X1,X2)),nand(X0,nand(X1,X2))))) ),
introduced(definition,[new_symbols(definition,[spl2_167])],[avatar_definition]) ).
fof(f1561,plain,
( ! [X2,X0,X1] : p(nand(nand(X0,nand(X1,X2)),nand(nand(X0,nand(X1,X2)),nand(X0,nand(X1,X2)))))
| ~ spl2_167 ),
inference(avatar_component_clause,[],[f1560]) ).
fof(f1562,plain,
( spl2_167
| ~ spl2_160
| ~ spl2_161 ),
inference(avatar_split_clause,[],[f1297,f1234,f1228,f1560]) ).
fof(f1607,plain,
( $false
| ~ spl2_146
| ~ spl2_167 ),
inference(resolution,[],[f1561,f1146]) ).
fof(f1635,plain,
( ~ spl2_146
| ~ spl2_167 ),
inference(avatar_contradiction_clause,[],[f1607]) ).
fof(f1707,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(X1,X2)))
| p(nand(nand(X3,X2),nand(nand(X3,X2),nand(X3,X2)))) )
| ~ spl2_160
| ~ spl2_164 ),
inference(resolution,[],[f1393,f1229]) ).
fof(f1712,definition,
( spl2_168
<=> ! [X0,X3,X2,X1] :
( ~ p(nand(X0,nand(X1,X2)))
| p(nand(nand(X3,X2),nand(nand(X3,X2),nand(X3,X2)))) ) ),
introduced(definition,[new_symbols(definition,[spl2_168])],[avatar_definition]) ).
fof(f1713,plain,
( ! [X2,X3,X0,X1] :
( p(nand(nand(X3,X2),nand(nand(X3,X2),nand(X3,X2))))
| ~ p(nand(X0,nand(X1,X2))) )
| ~ spl2_168 ),
inference(avatar_component_clause,[],[f1712]) ).
fof(f1714,plain,
( spl2_168
| ~ spl2_160
| ~ spl2_164 ),
inference(avatar_split_clause,[],[f1707,f1392,f1228,f1712]) ).
fof(f1792,plain,
( ! [X2,X3,X0,X1] :
( p(nand(nand(X0,nand(X1,X2)),X3))
| ~ p(nand(X3,nand(X0,nand(X1,X2)))) )
| ~ spl2_166
| ~ spl2_167 ),
inference(resolution,[],[f1557,f1561]) ).
fof(f1814,plain,
( spl2_113
| ~ spl2_117
| ~ spl2_163 ),
inference(avatar_split_clause,[],[f1321,f1307,f985,f966]) ).
fof(f1816,definition,
( spl2_172
<=> ! [X0,X3,X2,X1] :
( p(nand(nand(X0,nand(X1,X2)),X3))
| ~ p(nand(X3,nand(X0,nand(X1,X2)))) ) ),
introduced(definition,[new_symbols(definition,[spl2_172])],[avatar_definition]) ).
fof(f1817,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X3,nand(X0,nand(X1,X2))))
| p(nand(nand(X0,nand(X1,X2)),X3)) )
| ~ spl2_172 ),
inference(avatar_component_clause,[],[f1816]) ).
fof(f1818,plain,
( spl2_172
| ~ spl2_166
| ~ spl2_167 ),
inference(avatar_split_clause,[],[f1792,f1560,f1556,f1816]) ).
fof(f1819,plain,
( ! [X2,X3,X0,X1] : p(nand(nand(nand(nand(X0,X1),nand(nand(X2,X0),nand(X2,X0))),nand(X2,nand(X2,X3))),nand(X2,nand(X3,X1))))
| ~ spl2_159
| ~ spl2_172 ),
inference(resolution,[],[f1817,f1223]) ).
fof(f1827,definition,
( spl2_173
<=> ! [X0,X3,X2,X1] : p(nand(nand(nand(nand(X0,X1),nand(nand(X2,X0),nand(X2,X0))),nand(X2,nand(X2,X3))),nand(X2,nand(X3,X1)))) ),
introduced(definition,[new_symbols(definition,[spl2_173])],[avatar_definition]) ).
fof(f1828,plain,
( ! [X2,X3,X0,X1] : p(nand(nand(nand(nand(X0,X1),nand(nand(X2,X0),nand(X2,X0))),nand(X2,nand(X2,X3))),nand(X2,nand(X3,X1))))
| ~ spl2_173 ),
inference(avatar_component_clause,[],[f1827]) ).
fof(f1829,plain,
( spl2_173
| ~ spl2_159
| ~ spl2_172 ),
inference(avatar_split_clause,[],[f1819,f1816,f1222,f1827]) ).
fof(f2045,definition,
( spl2_181
<=> ! [X4,X0,X3,X2,X1] :
( ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(nand(X2,X3),nand(X0,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(nand(sK0,X4),X3)) ) ),
introduced(definition,[new_symbols(definition,[spl2_181])],[avatar_definition]) ).
fof(f2046,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(nand(nand(X2,X3),nand(X0,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(X0,nand(X1,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(nand(sK0,X4),X3)) )
| ~ spl2_181 ),
inference(avatar_component_clause,[],[f2045]) ).
fof(f2047,plain,
( spl2_181
| ~ spl2_101
| ~ spl2_163 ),
inference(avatar_split_clause,[],[f1316,f1307,f899,f2045]) ).
fof(f2162,plain,
( ! [X0,X1] :
( ~ p(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(X0,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ p(nand(nand(sK0,X1),nand(nand(sK0,sK0),nand(sK0,sK0)))) )
| ~ spl2_167
| ~ spl2_181 ),
inference(resolution,[],[f2046,f1561]) ).
fof(f2171,definition,
( spl2_187
<=> ! [X1] : ~ p(nand(nand(sK0,X1),nand(nand(sK0,sK0),nand(sK0,sK0)))) ),
introduced(definition,[new_symbols(definition,[spl2_187])],[avatar_definition]) ).
fof(f2172,plain,
( ! [X1] : ~ p(nand(nand(sK0,X1),nand(nand(sK0,sK0),nand(sK0,sK0))))
| ~ spl2_187 ),
inference(avatar_component_clause,[],[f2171]) ).
fof(f2174,definition,
( spl2_188
<=> ! [X0] : ~ p(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(X0,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0)))))) ),
introduced(definition,[new_symbols(definition,[spl2_188])],[avatar_definition]) ).
fof(f2175,plain,
( ! [X0] : ~ p(nand(nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))),nand(X0,nand(nand(sK1,sK1),nand(nand(sK0,sK0),nand(sK0,sK0))))))
| ~ spl2_188 ),
inference(avatar_component_clause,[],[f2174]) ).
fof(f2176,plain,
( spl2_187
| spl2_188
| ~ spl2_167
| ~ spl2_181 ),
inference(avatar_split_clause,[],[f2162,f2045,f1560,f2174,f2171]) ).
fof(f2177,plain,
( $false
| ~ spl2_167
| ~ spl2_188 ),
inference(resolution,[],[f2175,f1561]) ).
fof(f2181,plain,
( ~ spl2_167
| ~ spl2_188 ),
inference(avatar_contradiction_clause,[],[f2177]) ).
fof(f2184,plain,
( ! [X0,X1] : ~ p(nand(X0,nand(X1,sK0)))
| ~ spl2_168
| ~ spl2_187 ),
inference(resolution,[],[f2172,f1713]) ).
fof(f2187,definition,
( spl2_189
<=> ! [X0,X1] : ~ p(nand(X0,nand(X1,sK0))) ),
introduced(definition,[new_symbols(definition,[spl2_189])],[avatar_definition]) ).
fof(f2188,plain,
( ! [X0,X1] : ~ p(nand(X0,nand(X1,sK0)))
| ~ spl2_189 ),
inference(avatar_component_clause,[],[f2187]) ).
fof(f2189,plain,
( spl2_189
| ~ spl2_168
| ~ spl2_187 ),
inference(avatar_split_clause,[],[f2184,f2171,f1712,f2187]) ).
fof(f2191,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(X2,nand(X3,sK0)))))
| ~ p(X0) )
| ~ spl2_189 ),
inference(resolution,[],[f2188,f10]) ).
fof(f2268,definition,
( spl2_199
<=> ! [X0,X3,X2,X1] :
( ~ p(nand(X0,nand(X1,nand(X2,nand(X3,sK0)))))
| ~ p(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_199])],[avatar_definition]) ).
fof(f2269,plain,
( ! [X2,X3,X0,X1] :
( ~ p(nand(X0,nand(X1,nand(X2,nand(X3,sK0)))))
| ~ p(X0) )
| ~ spl2_199 ),
inference(avatar_component_clause,[],[f2268]) ).
fof(f2270,plain,
( spl2_199
| ~ spl2_189 ),
inference(avatar_split_clause,[],[f2191,f2187,f2268]) ).
fof(f2271,plain,
( ! [X0,X1] : ~ p(nand(X0,nand(sK0,X1)))
| ~ spl2_159
| ~ spl2_199 ),
inference(resolution,[],[f2269,f1223]) ).
fof(f2281,definition,
( spl2_200
<=> ! [X0,X1] : ~ p(nand(X0,nand(sK0,X1))) ),
introduced(definition,[new_symbols(definition,[spl2_200])],[avatar_definition]) ).
fof(f2282,plain,
( ! [X0,X1] : ~ p(nand(X0,nand(sK0,X1)))
| ~ spl2_200 ),
inference(avatar_component_clause,[],[f2281]) ).
fof(f2283,plain,
( spl2_200
| ~ spl2_159
| ~ spl2_199 ),
inference(avatar_split_clause,[],[f2271,f2268,f1222,f2281]) ).
fof(f2284,plain,
( $false
| ~ spl2_173
| ~ spl2_200 ),
inference(resolution,[],[f2282,f1828]) ).
fof(f2287,plain,
( ~ spl2_173
| ~ spl2_200 ),
inference(avatar_contradiction_clause,[],[f2284]) ).
cnf(s1,plain,
~ spl2_1,
inference(sat_conversion,[],[f16]) ).
cnf(s2,plain,
( spl2_1
| spl2_2 ),
inference(sat_conversion,[],[f21]) ).
cnf(s3,plain,
( ~ spl2_2
| spl2_3 ),
inference(sat_conversion,[],[f26]) ).
cnf(s6,plain,
( ~ spl2_3
| spl2_6 ),
inference(sat_conversion,[],[f41]) ).
cnf(s7,plain,
( ~ spl2_6
| spl2_7 ),
inference(sat_conversion,[],[f47]) ).
cnf(s8,plain,
( ~ spl2_7
| spl2_8 ),
inference(sat_conversion,[],[f53]) ).
cnf(s10,plain,
( ~ spl2_8
| spl2_10 ),
inference(sat_conversion,[],[f66]) ).
cnf(s11,plain,
( ~ spl2_10
| spl2_11 ),
inference(sat_conversion,[],[f72]) ).
cnf(s19,plain,
( ~ spl2_11
| spl2_19 ),
inference(sat_conversion,[],[f116]) ).
cnf(s26,plain,
( ~ spl2_19
| spl2_26 ),
inference(sat_conversion,[],[f155]) ).
cnf(s27,plain,
( ~ spl2_26
| spl2_27 ),
inference(sat_conversion,[],[f161]) ).
cnf(s28,plain,
( ~ spl2_27
| spl2_28
| spl2_29 ),
inference(sat_conversion,[],[f170]) ).
cnf(s29,plain,
( ~ spl2_29
| spl2_30 ),
inference(sat_conversion,[],[f175]) ).
cnf(s30,plain,
( ~ spl2_30
| spl2_31 ),
inference(sat_conversion,[],[f180]) ).
cnf(s46,plain,
( ~ spl2_31
| spl2_48 ),
inference(sat_conversion,[],[f273]) ).
cnf(s47,plain,
( ~ spl2_28
| spl2_49 ),
inference(sat_conversion,[],[f278]) ).
cnf(s49,plain,
( ~ spl2_48
| spl2_51 ),
inference(sat_conversion,[],[f292]) ).
cnf(s50,plain,
( ~ spl2_51
| spl2_52 ),
inference(sat_conversion,[],[f298]) ).
cnf(s56,plain,
( ~ spl2_49
| spl2_55 ),
inference(sat_conversion,[],[f323]) ).
cnf(s59,plain,
( ~ spl2_55
| spl2_58 ),
inference(sat_conversion,[],[f340]) ).
cnf(s60,plain,
( ~ spl2_58
| spl2_59 ),
inference(sat_conversion,[],[f346]) ).
cnf(s61,plain,
( ~ spl2_59
| spl2_60 ),
inference(sat_conversion,[],[f352]) ).
cnf(s67,plain,
( ~ spl2_52
| spl2_62 ),
inference(sat_conversion,[],[f374]) ).
cnf(s78,plain,
( ~ spl2_60
| spl2_65 ),
inference(sat_conversion,[],[f417]) ).
cnf(s92,plain,
( ~ spl2_62
| spl2_68 ),
inference(sat_conversion,[],[f469]) ).
cnf(s104,plain,
( ~ spl2_65
| spl2_71 ),
inference(sat_conversion,[],[f517]) ).
cnf(s112,plain,
( ~ spl2_71
| spl2_73 ),
inference(sat_conversion,[],[f547]) ).
cnf(s118,plain,
( ~ spl2_73
| spl2_75 ),
inference(sat_conversion,[],[f566]) ).
cnf(s124,plain,
( ~ spl2_75
| spl2_77 ),
inference(sat_conversion,[],[f586]) ).
cnf(s134,plain,
( ~ spl2_77
| spl2_79 ),
inference(sat_conversion,[],[f621]) ).
cnf(s192,plain,
( ~ spl2_79
| spl2_98 ),
inference(sat_conversion,[],[f884]) ).
cnf(s193,plain,
( ~ spl2_68
| spl2_99 ),
inference(sat_conversion,[],[f889]) ).
cnf(s194,plain,
( ~ spl2_99
| spl2_100 ),
inference(sat_conversion,[],[f895]) ).
cnf(s195,plain,
( ~ spl2_100
| spl2_101 ),
inference(sat_conversion,[],[f901]) ).
cnf(s205,plain,
( ~ spl2_98
| spl2_111 ),
inference(sat_conversion,[],[f956]) ).
cnf(s206,plain,
( ~ spl2_111
| spl2_112 ),
inference(sat_conversion,[],[f962]) ).
cnf(s207,plain,
( ~ spl2_112
| spl2_113
| spl2_114 ),
inference(sat_conversion,[],[f971]) ).
cnf(s208,plain,
( ~ spl2_113
| spl2_115 ),
inference(sat_conversion,[],[f976]) ).
cnf(s209,plain,
( ~ spl2_114
| spl2_116 ),
inference(sat_conversion,[],[f981]) ).
cnf(s210,plain,
( ~ spl2_116
| spl2_117 ),
inference(sat_conversion,[],[f987]) ).
cnf(s212,plain,
( ~ spl2_115
| spl2_119 ),
inference(sat_conversion,[],[f999]) ).
cnf(s213,plain,
( ~ spl2_119
| spl2_120 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s214,plain,
( ~ spl2_120
| spl2_121 ),
inference(sat_conversion,[],[f1010]) ).
cnf(s215,plain,
( ~ spl2_121
| spl2_122 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s218,plain,
( ~ spl2_122
| spl2_125 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s219,plain,
( ~ spl2_125
| spl2_126 ),
inference(sat_conversion,[],[f1035]) ).
cnf(s220,plain,
( ~ spl2_126
| spl2_127 ),
inference(sat_conversion,[],[f1041]) ).
cnf(s221,plain,
( ~ spl2_127
| spl2_128 ),
inference(sat_conversion,[],[f1046]) ).
cnf(s222,plain,
( ~ spl2_128
| spl2_129 ),
inference(sat_conversion,[],[f1052]) ).
cnf(s223,plain,
( ~ spl2_129
| spl2_130 ),
inference(sat_conversion,[],[f1057]) ).
cnf(s226,plain,
( ~ spl2_130
| spl2_133 ),
inference(sat_conversion,[],[f1074]) ).
cnf(s227,plain,
( ~ spl2_133
| spl2_134 ),
inference(sat_conversion,[],[f1080]) ).
cnf(s231,plain,
( ~ spl2_134
| spl2_138 ),
inference(sat_conversion,[],[f1100]) ).
cnf(s235,plain,
( ~ spl2_138
| spl2_142 ),
inference(sat_conversion,[],[f1125]) ).
cnf(s236,plain,
( ~ spl2_142
| spl2_143 ),
inference(sat_conversion,[],[f1131]) ).
cnf(s237,plain,
( ~ spl2_143
| spl2_144 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s239,plain,
( ~ spl2_144
| spl2_146 ),
inference(sat_conversion,[],[f1147]) ).
cnf(s253,plain,
spl2_159,
inference(sat_conversion,[],[f1224]) ).
cnf(s254,plain,
( ~ spl2_159
| spl2_160 ),
inference(sat_conversion,[],[f1230]) ).
cnf(s255,plain,
( ~ spl2_159
| ~ spl2_160
| spl2_161 ),
inference(sat_conversion,[],[f1236]) ).
cnf(s258,plain,
( ~ spl2_161
| spl2_163 ),
inference(sat_conversion,[],[f1309]) ).
cnf(s259,plain,
( ~ spl2_160
| ~ spl2_163
| spl2_164 ),
inference(sat_conversion,[],[f1394]) ).
cnf(s266,plain,
( ~ spl2_163
| spl2_166 ),
inference(sat_conversion,[],[f1558]) ).
cnf(s267,plain,
( ~ spl2_160
| ~ spl2_161
| spl2_167 ),
inference(sat_conversion,[],[f1562]) ).
cnf(s268,plain,
( ~ spl2_146
| ~ spl2_167 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s269,plain,
( ~ spl2_160
| ~ spl2_164
| spl2_168 ),
inference(sat_conversion,[],[f1714]) ).
cnf(s275,plain,
( spl2_113
| ~ spl2_117
| ~ spl2_163 ),
inference(sat_conversion,[],[f1814]) ).
cnf(s276,plain,
( ~ spl2_166
| ~ spl2_167
| spl2_172 ),
inference(sat_conversion,[],[f1818]) ).
cnf(s277,plain,
( ~ spl2_159
| ~ spl2_172
| spl2_173 ),
inference(sat_conversion,[],[f1829]) ).
cnf(s285,plain,
( ~ spl2_101
| ~ spl2_163
| spl2_181 ),
inference(sat_conversion,[],[f2047]) ).
cnf(s291,plain,
( ~ spl2_167
| ~ spl2_181
| spl2_187
| spl2_188 ),
inference(sat_conversion,[],[f2176]) ).
cnf(s292,plain,
( ~ spl2_167
| ~ spl2_188 ),
inference(sat_conversion,[],[f2181]) ).
cnf(s293,plain,
( ~ spl2_168
| ~ spl2_187
| spl2_189 ),
inference(sat_conversion,[],[f2189]) ).
cnf(s303,plain,
( ~ spl2_189
| spl2_199 ),
inference(sat_conversion,[],[f2270]) ).
cnf(s304,plain,
( ~ spl2_159
| ~ spl2_199
| spl2_200 ),
inference(sat_conversion,[],[f2283]) ).
cnf(s305,plain,
( ~ spl2_173
| ~ spl2_200 ),
inference(sat_conversion,[],[f2287]) ).
cnf(s309,plain,
spl2_160,
inference(rat,[],[s254,s253]) ).
cnf(s311,plain,
spl2_161,
inference(rat,[],[s255,s253,s309]) ).
cnf(s313,plain,
spl2_167,
inference(rat,[],[s267,s309,s311]) ).
cnf(s315,plain,
spl2_163,
inference(rat,[],[s258,s311]) ).
cnf(s317,plain,
~ spl2_188,
inference(rat,[],[s292,s313]) ).
cnf(s318,plain,
~ spl2_146,
inference(rat,[],[s268,s313]) ).
cnf(s320,plain,
spl2_166,
inference(rat,[],[s266,s315]) ).
cnf(s321,plain,
spl2_164,
inference(rat,[],[s259,s309,s315]) ).
cnf(s322,plain,
spl2_172,
inference(rat,[],[s276,s313,s320]) ).
cnf(s325,plain,
spl2_168,
inference(rat,[],[s269,s309,s321]) ).
cnf(s326,plain,
spl2_173,
inference(rat,[],[s277,s253,s322]) ).
cnf(s329,plain,
~ spl2_200,
inference(rat,[],[s305,s326]) ).
cnf(s332,plain,
~ spl2_199,
inference(rat,[],[s304,s253,s329]) ).
cnf(s334,plain,
~ spl2_189,
inference(rat,[],[s303,s332]) ).
cnf(s335,plain,
~ spl2_187,
inference(rat,[],[s293,s325,s334]) ).
cnf(s336,plain,
~ spl2_181,
inference(rat,[],[s291,s317,s313,s335]) ).
cnf(s337,plain,
~ spl2_101,
inference(rat,[],[s285,s315,s336]) ).
cnf(s347,plain,
~ spl2_144,
inference(rat,[],[s239,s318]) ).
cnf(s348,plain,
~ spl2_143,
inference(rat,[],[s237,s347]) ).
cnf(s349,plain,
~ spl2_142,
inference(rat,[],[s236,s348]) ).
cnf(s350,plain,
~ spl2_138,
inference(rat,[],[s235,s349]) ).
cnf(s351,plain,
~ spl2_134,
inference(rat,[],[s231,s350]) ).
cnf(s352,plain,
~ spl2_133,
inference(rat,[],[s227,s351]) ).
cnf(s353,plain,
~ spl2_130,
inference(rat,[],[s226,s352]) ).
cnf(s354,plain,
~ spl2_129,
inference(rat,[],[s223,s353]) ).
cnf(s355,plain,
~ spl2_128,
inference(rat,[],[s222,s354]) ).
cnf(s356,plain,
~ spl2_127,
inference(rat,[],[s221,s355]) ).
cnf(s359,plain,
~ spl2_126,
inference(rat,[],[s220,s356]) ).
cnf(s360,plain,
~ spl2_125,
inference(rat,[],[s219,s359]) ).
cnf(s361,plain,
~ spl2_122,
inference(rat,[],[s218,s360]) ).
cnf(s362,plain,
~ spl2_121,
inference(rat,[],[s215,s361]) ).
cnf(s363,plain,
~ spl2_120,
inference(rat,[],[s214,s362]) ).
cnf(s364,plain,
~ spl2_119,
inference(rat,[],[s213,s363]) ).
cnf(s365,plain,
~ spl2_115,
inference(rat,[],[s212,s364]) ).
cnf(s366,plain,
~ spl2_113,
inference(rat,[],[s208,s365]) ).
cnf(s367,plain,
~ spl2_117,
inference(rat,[],[s275,s315,s366]) ).
cnf(s368,plain,
~ spl2_116,
inference(rat,[],[s210,s367]) ).
cnf(s369,plain,
~ spl2_114,
inference(rat,[],[s209,s368]) ).
cnf(s370,plain,
~ spl2_112,
inference(rat,[],[s207,s369,s366]) ).
cnf(s371,plain,
~ spl2_111,
inference(rat,[],[s206,s370]) ).
cnf(s372,plain,
~ spl2_98,
inference(rat,[],[s205,s371]) ).
cnf(s373,plain,
~ spl2_100,
inference(rat,[],[s195,s337]) ).
cnf(s374,plain,
~ spl2_99,
inference(rat,[],[s194,s373]) ).
cnf(s375,plain,
~ spl2_68,
inference(rat,[],[s193,s374]) ).
cnf(s376,plain,
~ spl2_79,
inference(rat,[],[s192,s372]) ).
cnf(s379,plain,
~ spl2_77,
inference(rat,[],[s134,s376]) ).
cnf(s380,plain,
~ spl2_75,
inference(rat,[],[s124,s379]) ).
cnf(s381,plain,
~ spl2_73,
inference(rat,[],[s118,s380]) ).
cnf(s382,plain,
~ spl2_71,
inference(rat,[],[s112,s381]) ).
cnf(s383,plain,
~ spl2_65,
inference(rat,[],[s104,s382]) ).
cnf(s384,plain,
~ spl2_62,
inference(rat,[],[s92,s375]) ).
cnf(s385,plain,
~ spl2_60,
inference(rat,[],[s78,s383]) ).
cnf(s388,plain,
~ spl2_52,
inference(rat,[],[s67,s384]) ).
cnf(s392,plain,
~ spl2_59,
inference(rat,[],[s61,s385]) ).
cnf(s393,plain,
~ spl2_58,
inference(rat,[],[s60,s392]) ).
cnf(s394,plain,
~ spl2_55,
inference(rat,[],[s59,s393]) ).
cnf(s395,plain,
~ spl2_49,
inference(rat,[],[s56,s394]) ).
cnf(s396,plain,
~ spl2_51,
inference(rat,[],[s50,s388]) ).
cnf(s397,plain,
~ spl2_48,
inference(rat,[],[s49,s396]) ).
cnf(s398,plain,
~ spl2_28,
inference(rat,[],[s47,s395]) ).
cnf(s402,plain,
~ spl2_31,
inference(rat,[],[s46,s397]) ).
cnf(s403,plain,
~ spl2_30,
inference(rat,[],[s30,s402]) ).
cnf(s404,plain,
~ spl2_29,
inference(rat,[],[s29,s403]) ).
cnf(s408,plain,
~ spl2_27,
inference(rat,[],[s28,s404,s398]) ).
cnf(s409,plain,
~ spl2_26,
inference(rat,[],[s27,s408]) ).
cnf(s410,plain,
~ spl2_19,
inference(rat,[],[s26,s409]) ).
cnf(s411,plain,
~ spl2_11,
inference(rat,[],[s19,s410]) ).
cnf(s412,plain,
~ spl2_10,
inference(rat,[],[s11,s411]) ).
cnf(s413,plain,
~ spl2_8,
inference(rat,[],[s10,s412]) ).
cnf(s414,plain,
~ spl2_7,
inference(rat,[],[s8,s413]) ).
cnf(s415,plain,
~ spl2_6,
inference(rat,[],[s7,s414]) ).
cnf(s416,plain,
~ spl2_3,
inference(rat,[],[s6,s415]) ).
cnf(s417,plain,
~ spl2_2,
inference(rat,[],[s3,s416]) ).
cnf(s418,plain,
spl2_1,
inference(rat,[],[s2,s417]) ).
cnf(s419,plain,
$false,
inference(rat,[],[s1,s418]) ).
fof(f2288,plain,
$false,
inference(avatar_sat_refutation,[],[s419]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO109+1 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n016.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 21:16:04 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.58/3.03 % (4019375)Detected formulas, will run a generic FOF schedule.
% 15.58/3.03 % (4019401)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2749983355:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 15.58/3.03 % (4019401)Refutation not found, incomplete strategy
% 15.58/3.03 % (4019401)------------------------------
% 15.58/3.03 % (4019401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.03 % (4019401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.03 % (4019401)CaDiCaL version: 2.1.3
% 15.58/3.03 % (4019401)Termination reason: Refutation not found, incomplete strategy
% 15.58/3.03 % (4019401)Time elapsed: 0.001 s
% 15.58/3.03 % (4019401)Peak memory usage: 88 MB
% 15.58/3.03 % (4019404)dis-21_1_sil=8000:lcm=predicate:random_seed=2979585677:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 15.58/3.03 % (4019399)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4287795950:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 15.58/3.03 % (4019400)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=4068265511:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 15.58/3.03 % (4019402)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4240866530:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 15.58/3.03 % (4019398)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2803077794:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 15.58/3.03 % (4019403)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3807788184:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 15.58/3.03 % (4019404)Instruction limit reached!
% 15.58/3.03 % (4019404)------------------------------
% 15.58/3.03 % (4019404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.03 % (4019404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.03 % (4019404)CaDiCaL version: 2.1.3
% 15.58/3.03 % (4019404)Termination reason: Instruction limit
% 15.58/3.03 % (4019404)Termination phase: Saturation
% 15.58/3.03 % (4019404)Time elapsed: 0.082 s
% 15.58/3.03 % (4019404)Peak memory usage: 89 MB
% 15.58/3.03 % (4019404)Instructions burned: 129 (million)
% 15.58/3.03 % (4019402)Instruction limit reached!
% 15.58/3.03 % (4019402)------------------------------
% 15.58/3.03 % (4019402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.03 % (4019402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.03 % (4019402)CaDiCaL version: 2.1.3
% 15.58/3.03 % (4019402)Termination reason: Instruction limit
% 15.58/3.03 % (4019402)Termination phase: Saturation
% 15.58/3.03 % (4019402)Time elapsed: 0.109 s
% 15.58/3.03 % (4019402)Peak memory usage: 88 MB
% 15.58/3.03 % (4019402)Instructions burned: 119 (million)
% 15.58/3.03 % (4019403)Instruction limit reached!
% 15.58/3.03 % (4019403)------------------------------
% 15.58/3.03 % (4019403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.03 % (4019403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.03 % (4019403)CaDiCaL version: 2.1.3
% 15.58/3.03 % (4019403)Termination reason: Instruction limit
% 15.58/3.03 % (4019403)Termination phase: Saturation
% 15.58/3.03 % (4019403)Time elapsed: 0.132 s
% 15.58/3.03 % (4019403)Peak memory usage: 89 MB
% 15.58/3.03 % (4019403)Instructions burned: 139 (million)
% 15.58/3.03 % (4019401)------------------------------
% 15.58/3.03 % (4019401)------------------------------
% 15.58/3.03 % (4019422)lrs+10_1_sil=8000:sp=occurrence:random_seed=3707967641:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 15.58/3.03 % (4019431)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3374946463:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 15.58/3.03 % (4019427)lrs+10_1_sil=32000:urr=on:br=off:random_seed=805645017:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 15.58/3.03 % (4019429)lrs+1011_1_sil=32000:sp=occurrence:random_seed=463706908:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 15.58/3.03 % (4019431)Instruction limit reached!
% 15.58/3.03 % (4019431)------------------------------
% 15.58/3.03 % (4019431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.03 % (4019431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.03 % (4019431)CaDiCaL version: 2.1.3
% 15.58/3.03 % (4019431)Termination reason: Instruction limit
% 15.58/3.03 % (4019431)Termination phase: Saturation
% 15.58/3.03 % (4019431)Time elapsed: 0.101 s
% 15.58/3.03 % (4019431)Peak memory usage: 89 MB
% 15.58/3.03 % (4019431)Instructions burned: 249 (million)
% 15.58/3.03 % (4019427)Instruction limit reached!
% 15.58/3.03 % (4019427)------------------------------
% 15.58/3.03 % (4019427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.03 % (4019427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.03 % (4019427)CaDiCaL version: 2.1.3
% 15.58/3.03 % (4019427)Termination reason: Instruction limit
% 15.58/3.03 % (4019427)Termination phase: Saturation
% 15.58/3.03 % (4019427)Time elapsed: 0.144 s
% 15.58/3.03 % (4019427)Peak memory usage: 89 MB
% 15.58/3.03 % (4019427)Instructions burned: 158 (million)
% 15.58/3.03 % (4019422)Instruction limit reached!
% 15.58/3.03 % (4019422)------------------------------
% 15.58/3.03 % (4019422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.03 % (4019422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.03 % (4019422)CaDiCaL version: 2.1.3
% 15.58/3.03 % (4019422)Termination reason: Instruction limit
% 15.58/3.03 % (4019422)Termination phase: Saturation
% 15.58/3.03 % (4019422)Time elapsed: 0.264 s
% 15.58/3.03 % (4019422)Peak memory usage: 91 MB
% 15.58/3.03 % (4019422)Instructions burned: 285 (million)
% 15.58/3.03 % (4019439)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=654221140:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 15.58/3.03 % (4019439)Refutation not found, incomplete strategy
% 15.58/3.03 % (4019439)------------------------------
% 15.58/3.03 % (4019439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.03 % (4019439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.03 % (4019439)CaDiCaL version: 2.1.3
% 15.58/3.03 % (4019439)Termination reason: Refutation not found, incomplete strategy
% 15.58/3.03 % (4019439)Time elapsed: 0.001 s
% 15.58/3.03 % (4019439)Peak memory usage: 87 MB
% 15.58/3.03 % (4019441)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3238175922:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 15.58/3.03 % (4019442)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3299334132:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 15.58/3.03 % (4019429)Instruction limit reached!
% 15.58/3.03 % (4019429)------------------------------
% 15.58/3.03 % (4019429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.03 % (4019429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.03 % (4019429)CaDiCaL version: 2.1.3
% 15.58/3.03 % (4019429)Termination reason: Instruction limit
% 15.58/3.03 % (4019429)Termination phase: Saturation
% 15.58/3.03 % (4019429)Time elapsed: 0.349 s
% 15.58/3.03 % (4019429)Peak memory usage: 90 MB
% 15.58/3.03 % (4019429)Instructions burned: 325 (million)
% 15.58/3.03 % (4019442)Instruction limit reached!
% 15.58/3.03 % (4019442)------------------------------
% 15.58/3.03 % (4019442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.03 % (4019442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.03 % (4019442)CaDiCaL version: 2.1.3
% 15.58/3.03 % (4019442)Termination reason: Instruction limit
% 15.58/3.03 % (4019442)Termination phase: Saturation
% 15.58/3.03 % (4019442)Time elapsed: 0.079 s
% 15.58/3.03 % (4019442)Peak memory usage: 89 MB
% 15.58/3.03 % (4019442)Instructions burned: 113 (million)
% 15.58/3.03 % (4019439)------------------------------
% 15.58/3.03 % (4019439)------------------------------
% 15.58/3.03 % (4019450)lrs+10_1_sil=8000:sp=occurrence:random_seed=224757794:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 15.58/3.03 % (4019448)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1271564667:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 15.58/3.03 % (4019449)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1359792847:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 15.58/3.04 % (4019448)Instruction limit reached!
% 15.58/3.04 % (4019448)------------------------------
% 15.58/3.04 % (4019448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.04 % (4019448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.04 % (4019448)CaDiCaL version: 2.1.3
% 15.58/3.04 % (4019448)Termination reason: Instruction limit
% 15.58/3.04 % (4019448)Termination phase: Saturation
% 15.58/3.04 % (4019448)Time elapsed: 0.124 s
% 15.58/3.04 % (4019448)Peak memory usage: 89 MB
% 15.58/3.04 % (4019448)Instructions burned: 127 (million)
% 15.58/3.04 % (4019449)Instruction limit reached!
% 15.58/3.04 % (4019449)------------------------------
% 15.58/3.04 % (4019449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.04 % (4019449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.04 % (4019449)CaDiCaL version: 2.1.3
% 15.58/3.04 % (4019449)Termination reason: Instruction limit
% 15.58/3.04 % (4019449)Termination phase: Saturation
% 15.58/3.04 % (4019449)Time elapsed: 0.114 s
% 15.58/3.04 % (4019449)Peak memory usage: 89 MB
% 15.58/3.04 % (4019449)Instructions burned: 114 (million)
% 15.58/3.04 % (4019457)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=216411425:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 15.58/3.04 % (4019455)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4284281158:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi)
% 15.58/3.04 % (4019455)Refutation not found, incomplete strategy
% 15.58/3.04 % (4019455)------------------------------
% 15.58/3.04 % (4019455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.04 % (4019455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.04 % (4019455)CaDiCaL version: 2.1.3
% 15.58/3.04 % (4019455)Termination reason: Refutation not found, incomplete strategy
% 15.58/3.04 % (4019455)Time elapsed: 0.002 s
% 15.58/3.04 % (4019455)Peak memory usage: 88 MB
% 15.58/3.04 % (4019450)Instruction limit reached!
% 15.58/3.04 % (4019450)------------------------------
% 15.58/3.04 % (4019450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.04 % (4019450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.04 % (4019450)CaDiCaL version: 2.1.3
% 15.58/3.04 % (4019450)Termination reason: Instruction limit
% 15.58/3.04 % (4019450)Termination phase: Saturation
% 15.58/3.04 % (4019450)Time elapsed: 0.475 s
% 15.58/3.04 % (4019450)Peak memory usage: 95 MB
% 15.58/3.04 % (4019450)Instructions burned: 907 (million)
% 15.58/3.04 % (4019462)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3120986966:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 15.58/3.04 % (4019455)------------------------------
% 15.58/3.04 % (4019455)------------------------------
% 15.58/3.04 % (4019462)Instruction limit reached!
% 15.58/3.04 % (4019462)------------------------------
% 15.58/3.04 % (4019462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.04 % (4019462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.04 % (4019462)CaDiCaL version: 2.1.3
% 15.58/3.04 % (4019462)Termination reason: Instruction limit
% 15.58/3.04 % (4019462)Termination phase: Saturation
% 15.58/3.04 % (4019462)Time elapsed: 0.124 s
% 15.58/3.04 % (4019462)Peak memory usage: 88 MB
% 15.58/3.04 % (4019462)Instructions burned: 135 (million)
% 15.58/3.04 % (4019400)First to succeed.
% 15.58/3.04 % (4019400)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4019375"
% 15.58/3.04 % (4019466)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4166682000:st=8:i=592:sd=3:ep=RST:ss=axioms_2981 on theBenchmark for (2981ds/592Mi)
% 15.58/3.04 % (4019466)Refutation not found, incomplete strategy
% 15.58/3.04 % (4019466)------------------------------
% 15.58/3.04 % (4019466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.58/3.04 % (4019466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.58/3.04 % (4019466)CaDiCaL version: 2.1.3
% 15.58/3.04 % (4019466)Termination reason: Refutation not found, incomplete strategy
% 15.58/3.04 % (4019466)Time elapsed: 0.002 s
% 15.58/3.04 % (4019466)Peak memory usage: 88 MB
% 15.58/3.04 % (4019468)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=747072816:st=3:i=13193:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/13193Mi)
% 15.58/3.04 % (4019400)Refutation found. Thanks to Tanya!
% 15.58/3.04 % SZS status Theorem for theBenchmark
% 15.58/3.04 % SZS output start Proof for theBenchmark
% See solution above
% 17.50/3.36 % (4019400)------------------------------
% 17.50/3.36 % (4019400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.50/3.36 % (4019400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.50/3.36 % (4019400)CaDiCaL version: 2.1.3
% 17.50/3.36 % (4019400)Termination reason: Refutation
% 17.50/3.36 % (4019400)Time elapsed: 1.720 s
% 17.50/3.36 % (4019400)Peak memory usage: 135 MB
% 17.50/3.36 % (4019400)Instructions burned: 1682 (million)
% 17.50/3.36 % (4019400)------------------------------
% 17.50/3.36 % (4019400)------------------------------
% 17.50/3.36 % (4019375)Success in time 2.378 s
% 17.50/3.36 % Vampire exiting
%------------------------------------------------------------------------------