%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO468+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:52:44 AM UTC 2026
% Result : Theorem 96.66s 18.65s
% Output : Refutation 112.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 59
% Syntax : Number of formulae : 425 ( 123 unt; 49 def)
% Number of atoms : 1124 ( 188 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1305 ( 606 ~; 643 |; 36 &)
% ( 14 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 16 ( 14 usr; 14 prp; 0-2 aty)
% Number of functors : 58 ( 58 usr; 53 con; 0-3 aty)
% Number of variables : 324 ( 0 sgn 315 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f43,axiom,
~ p(s(bool,f0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSsrboolo_notu_falseu_isu_true) ).
fof(f97,axiom,
! [X0] :
( s(bool,X0) = s(bool,t)
| s(bool,X0) = s(bool,f0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aBOOLu_CASESu_AX) ).
fof(f1650,axiom,
! [X0,X1,X2] : s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(X0,fun(fun(X0,bool),bool)),in),s(X0,X2))),s(fun(X0,bool),X1))) = s(bool,i(s(fun(X0,bool),X1),s(X0,X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aIN) ).
fof(f1888,axiom,
! [X0,X1,X2] :
( ( p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2))))
& p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(fun(X0,bool),fun(fun(X0,bool),bool)),subset),s(fun(X0,bool),X1))),s(fun(X0,bool),X2)))) )
=> p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aFINITEu_SUBSET) ).
fof(f1890,axiom,
! [X0,X1,X2] :
( p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),i(s(fun(fun(X0,bool),fun(X0,bool)),i(s(fun(fun(X0,bool),fun(fun(X0,bool),fun(X0,bool))),union),s(fun(X0,bool),X1))),s(fun(X0,bool),X2))))))
<=> ( p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X1))))
& p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aFINITEu_UNION) ).
fof(f1938,axiom,
! [X0,X1,X2] :
( p(s(bool,i(s(fun(num,bool),i(s(fun(fun(X0,bool),fun(num,bool)),hasu_size),s(fun(X0,bool),X1))),s(num,X2))))
=> s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X1))) = s(num,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aHASu_SIZEu_CARD) ).
fof(f1944,axiom,
! [X0,X1] : s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X1))) = s(bool,i(s(fun(num,bool),i(s(fun(fun(X0,bool),fun(num,bool)),hasu_size),s(fun(X0,bool),X1))),s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X1))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aFINITEu_HASu_SIZE) ).
fof(f1948,axiom,
! [X0,X1,X2] :
( ( p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(fun(X0,bool),fun(fun(X0,bool),bool)),subset),s(fun(X0,bool),X1))),s(fun(X0,bool),X2))))
& p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2)))) )
=> p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X1))))),s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X2)))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aCARDu_SUBSET) ).
fof(f3373,axiom,
! [X0,X1,X2] :
( ( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X2))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),independent),s(fun(cart(real,X0),bool),X1))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X2)))))) )
=> ? [X3] :
( p(s(bool,i(s(fun(num,bool),i(s(fun(fun(cart(real,X0),bool),fun(num,bool)),hasu_size),s(fun(cart(real,X0),bool),X3))),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X2))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),X3))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X3))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool))),union),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),X2))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3)))))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aEXCHANGEu_LEMMA) ).
fof(f3374,conjecture,
! [X0,X1,X2] :
( ( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X2))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),independent),s(fun(cart(real,X0),bool),X1))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X2)))))) )
=> ( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X1))))
& p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X1))))),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X2)))))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aINDEPENDENTu_SPANu_BOUND) ).
fof(f3375,negated_conjecture,
~ ! [X0,X1,X2] :
( ( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X2))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),independent),s(fun(cart(real,X0),bool),X1))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X2)))))) )
=> ( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X1))))
& p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X1))))),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X2)))))) ) ),
inference(negated_conjecture,[status(cth)],[f3374]) ).
fof(f4811,plain,
! [X0,X1,X2] :
( p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(fun(X0,bool),fun(fun(X0,bool),bool)),subset),s(fun(X0,bool),X1))),s(fun(X0,bool),X2)))) ),
inference(ennf_transformation,[],[f1888]) ).
fof(f4812,plain,
! [X0,X1,X2] :
( p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(fun(X0,bool),fun(fun(X0,bool),bool)),subset),s(fun(X0,bool),X1))),s(fun(X0,bool),X2)))) ),
inference(flattening,[],[f4811]) ).
fof(f4869,plain,
! [X0,X1,X2] :
( s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X1))) = s(num,X2)
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(fun(X0,bool),fun(num,bool)),hasu_size),s(fun(X0,bool),X1))),s(num,X2)))) ),
inference(ennf_transformation,[],[f1938]) ).
fof(f4879,plain,
! [X0,X1,X2] :
( p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X1))))),s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X2))))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(fun(X0,bool),fun(fun(X0,bool),bool)),subset),s(fun(X0,bool),X1))),s(fun(X0,bool),X2))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2)))) ),
inference(ennf_transformation,[],[f1948]) ).
fof(f4880,plain,
! [X0,X1,X2] :
( p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X1))))),s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X2))))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(fun(X0,bool),fun(fun(X0,bool),bool)),subset),s(fun(X0,bool),X1))),s(fun(X0,bool),X2))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2)))) ),
inference(flattening,[],[f4879]) ).
fof(f6247,plain,
! [X0,X1,X2] :
( ? [X3] :
( p(s(bool,i(s(fun(num,bool),i(s(fun(fun(cart(real,X0),bool),fun(num,bool)),hasu_size),s(fun(cart(real,X0),bool),X3))),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X2))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),X3))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X3))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool))),union),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),X2))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3)))))) )
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X2))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),independent),s(fun(cart(real,X0),bool),X1))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X2)))))) ),
inference(ennf_transformation,[],[f3373]) ).
fof(f6248,plain,
! [X0,X1,X2] :
( ? [X3] :
( p(s(bool,i(s(fun(num,bool),i(s(fun(fun(cart(real,X0),bool),fun(num,bool)),hasu_size),s(fun(cart(real,X0),bool),X3))),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X2))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),X3))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X3))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool))),union),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),X2))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3)))))) )
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X2))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),independent),s(fun(cart(real,X0),bool),X1))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X2)))))) ),
inference(flattening,[],[f6247]) ).
fof(f6249,plain,
? [X0,X1,X2] :
( ( ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X1))))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X1))))),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X2)))))) )
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X2))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),independent),s(fun(cart(real,X0),bool),X1))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X2)))))) ),
inference(ennf_transformation,[],[f3375]) ).
fof(f6250,plain,
? [X0,X1,X2] :
( ( ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X1))))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X1))))),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X2)))))) )
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X2))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),independent),s(fun(cart(real,X0),bool),X1))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X2)))))) ),
inference(flattening,[],[f6249]) ).
fof(f8172,plain,
! [X0,X1,X2] :
( ( p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),i(s(fun(fun(X0,bool),fun(X0,bool)),i(s(fun(fun(X0,bool),fun(fun(X0,bool),fun(X0,bool))),union),s(fun(X0,bool),X1))),s(fun(X0,bool),X2))))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2)))) )
& ( ( p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X1))))
& p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2)))) )
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),i(s(fun(fun(X0,bool),fun(X0,bool)),i(s(fun(fun(X0,bool),fun(fun(X0,bool),fun(X0,bool))),union),s(fun(X0,bool),X1))),s(fun(X0,bool),X2)))))) ) ),
inference(nnf_transformation,[],[f1890]) ).
fof(f8173,plain,
! [X0,X1,X2] :
( ( p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),i(s(fun(fun(X0,bool),fun(X0,bool)),i(s(fun(fun(X0,bool),fun(fun(X0,bool),fun(X0,bool))),union),s(fun(X0,bool),X1))),s(fun(X0,bool),X2))))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2)))) )
& ( ( p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X1))))
& p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2)))) )
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),i(s(fun(fun(X0,bool),fun(X0,bool)),i(s(fun(fun(X0,bool),fun(fun(X0,bool),fun(X0,bool))),union),s(fun(X0,bool),X1))),s(fun(X0,bool),X2)))))) ) ),
inference(flattening,[],[f8172]) ).
fof(f10295,plain,
! [X0,X1,X2] :
( ( p(s(bool,i(s(fun(num,bool),i(s(fun(fun(cart(real,X0),bool),fun(num,bool)),hasu_size),s(fun(cart(real,X0),bool),sK4202(X0,X1,X2)))),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X2))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),sK4202(X0,X1,X2)))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),sK4202(X0,X1,X2)))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool))),union),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),X2))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),sK4202(X0,X1,X2))))))) )
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X2))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),independent),s(fun(cart(real,X0),bool),X1))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X2)))))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4202]),skolemize(X3,sK4202(X0,X1,X2))],[f6248]) ).
fof(f10296,plain,
( ( ~ p(s(bool,i(s(fun(fun(cart(real,sK4203),bool),bool),finite),s(fun(cart(real,sK4203),bool),sK4204))))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(cart(real,sK4203),bool),num),card),s(fun(cart(real,sK4203),bool),sK4204))))),s(num,i(s(fun(fun(cart(real,sK4203),bool),num),card),s(fun(cart(real,sK4203),bool),sK4205)))))) )
& p(s(bool,i(s(fun(fun(cart(real,sK4203),bool),bool),finite),s(fun(cart(real,sK4203),bool),sK4205))))
& p(s(bool,i(s(fun(fun(cart(real,sK4203),bool),bool),independent),s(fun(cart(real,sK4203),bool),sK4204))))
& p(s(bool,i(s(fun(fun(cart(real,sK4203),bool),bool),i(s(fun(fun(cart(real,sK4203),bool),fun(fun(cart(real,sK4203),bool),bool)),subset),s(fun(cart(real,sK4203),bool),sK4204))),s(fun(cart(real,sK4203),bool),i(s(fun(fun(cart(real,sK4203),bool),fun(cart(real,sK4203),bool)),span),s(fun(cart(real,sK4203),bool),sK4205)))))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4203,sK4204,sK4205]),skolemize(X0,sK4203),skolemize(X1,sK4204),skolemize(X2,sK4205)],[f6250]) ).
fof(f10463,plain,
~ p(s(bool,f0)),
inference(cnf_transformation,[],[f43]) ).
fof(f10695,plain,
! [X0] :
( s(bool,X0) = s(bool,f0)
| s(bool,t) = s(bool,X0) ),
inference(cnf_transformation,[],[f97]) ).
fof(f13195,plain,
! [X2,X0,X1] : s(bool,i(s(fun(X0,bool),X1),s(X0,X2))) = s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(X0,fun(fun(X0,bool),bool)),in),s(X0,X2))),s(fun(X0,bool),X1))),
inference(cnf_transformation,[],[f1650]) ).
fof(f13862,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(fun(X0,bool),fun(fun(X0,bool),bool)),subset),s(fun(X0,bool),X1))),s(fun(X0,bool),X2))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2))))
| p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X1)))) ),
inference(cnf_transformation,[],[f4812]) ).
fof(f13866,plain,
! [X2,X0,X1] :
( p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),i(s(fun(fun(X0,bool),fun(X0,bool)),i(s(fun(fun(X0,bool),fun(fun(X0,bool),fun(X0,bool))),union),s(fun(X0,bool),X1))),s(fun(X0,bool),X2))))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2)))) ),
inference(cnf_transformation,[],[f8173]) ).
fof(f14038,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(num,bool),i(s(fun(fun(X0,bool),fun(num,bool)),hasu_size),s(fun(X0,bool),X1))),s(num,X2))))
| s(num,X2) = s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X1))) ),
inference(cnf_transformation,[],[f4869]) ).
fof(f14057,plain,
! [X0,X1] : s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X1))) = s(bool,i(s(fun(num,bool),i(s(fun(fun(X0,bool),fun(num,bool)),hasu_size),s(fun(X0,bool),X1))),s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X1))))),
inference(cnf_transformation,[],[f1944]) ).
fof(f14065,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(fun(X0,bool),fun(fun(X0,bool),bool)),subset),s(fun(X0,bool),X1))),s(fun(X0,bool),X2))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X1))))),s(num,i(s(fun(fun(X0,bool),num),card),s(fun(X0,bool),X2))))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),X2)))) ),
inference(cnf_transformation,[],[f4880]) ).
fof(f17692,plain,
! [X2,X0,X1] :
( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),sK4202(X0,X1,X2)))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool))),union),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),X2))))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X2))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),independent),s(fun(cart(real,X0),bool),X1))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X2)))))) ),
inference(cnf_transformation,[],[f10295]) ).
fof(f17693,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X2))))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X2))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),independent),s(fun(cart(real,X0),bool),X1))))
| p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),sK4202(X0,X1,X2))))) ),
inference(cnf_transformation,[],[f10295]) ).
fof(f17694,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X2))))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),finite),s(fun(cart(real,X0),bool),X2))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),independent),s(fun(cart(real,X0),bool),X1))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(cart(real,X0),bool),fun(num,bool)),hasu_size),s(fun(cart(real,X0),bool),sK4202(X0,X1,X2)))),s(num,i(s(fun(fun(cart(real,X0),bool),num),card),s(fun(cart(real,X0),bool),X2)))))) ),
inference(cnf_transformation,[],[f10295]) ).
fof(f17695,plain,
p(s(bool,i(s(fun(fun(cart(real,sK4203),bool),bool),i(s(fun(fun(cart(real,sK4203),bool),fun(fun(cart(real,sK4203),bool),bool)),subset),s(fun(cart(real,sK4203),bool),sK4204))),s(fun(cart(real,sK4203),bool),i(s(fun(fun(cart(real,sK4203),bool),fun(cart(real,sK4203),bool)),span),s(fun(cart(real,sK4203),bool),sK4205)))))),
inference(cnf_transformation,[],[f10296]) ).
fof(f17696,plain,
p(s(bool,i(s(fun(fun(cart(real,sK4203),bool),bool),independent),s(fun(cart(real,sK4203),bool),sK4204)))),
inference(cnf_transformation,[],[f10296]) ).
fof(f17697,plain,
p(s(bool,i(s(fun(fun(cart(real,sK4203),bool),bool),finite),s(fun(cart(real,sK4203),bool),sK4205)))),
inference(cnf_transformation,[],[f10296]) ).
fof(f17698,plain,
( ~ p(s(bool,i(s(fun(fun(cart(real,sK4203),bool),bool),finite),s(fun(cart(real,sK4203),bool),sK4204))))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(cart(real,sK4203),bool),num),card),s(fun(cart(real,sK4203),bool),sK4204))))),s(num,i(s(fun(fun(cart(real,sK4203),bool),num),card),s(fun(cart(real,sK4203),bool),sK4205)))))) ),
inference(cnf_transformation,[],[f10296]) ).
fof(f17699,definition,
sF4206 = cart(real,sK4203),
introduced(definition,[new_symbols(definition,[sF4206])],[function_definition]) ).
fof(f17700,plain,
cart(real,sK4203) = sF4206,
inference(reorient_equations,[],[f17699]) ).
fof(f17701,definition,
sF4207 = fun(sF4206,bool),
introduced(definition,[new_symbols(definition,[sF4207])],[function_definition]) ).
fof(f17702,plain,
fun(sF4206,bool) = sF4207,
inference(reorient_equations,[],[f17701]) ).
fof(f17703,definition,
sF4208 = fun(sF4207,bool),
introduced(definition,[new_symbols(definition,[sF4208])],[function_definition]) ).
fof(f17704,plain,
fun(sF4207,bool) = sF4208,
inference(reorient_equations,[],[f17703]) ).
fof(f17705,definition,
sF4209 = s(sF4208,finite),
introduced(definition,[new_symbols(definition,[sF4209])],[function_definition]) ).
fof(f17706,plain,
s(sF4208,finite) = sF4209,
inference(reorient_equations,[],[f17705]) ).
fof(f17707,definition,
sF4210 = s(sF4207,sK4204),
introduced(definition,[new_symbols(definition,[sF4210])],[function_definition]) ).
fof(f17708,plain,
s(sF4207,sK4204) = sF4210,
inference(reorient_equations,[],[f17707]) ).
fof(f17709,definition,
sF4211 = i(sF4209,sF4210),
introduced(definition,[new_symbols(definition,[sF4211])],[function_definition]) ).
fof(f17710,plain,
i(sF4209,sF4210) = sF4211,
inference(reorient_equations,[],[f17709]) ).
fof(f17711,definition,
sF4212 = s(bool,sF4211),
introduced(definition,[new_symbols(definition,[sF4212])],[function_definition]) ).
fof(f17712,plain,
s(bool,sF4211) = sF4212,
inference(reorient_equations,[],[f17711]) ).
fof(f17713,definition,
sF4213 = fun(num,bool),
introduced(definition,[new_symbols(definition,[sF4213])],[function_definition]) ).
fof(f17714,plain,
fun(num,bool) = sF4213,
inference(reorient_equations,[],[f17713]) ).
fof(f17715,definition,
sF4214 = fun(num,sF4213),
introduced(definition,[new_symbols(definition,[sF4214])],[function_definition]) ).
fof(f17716,plain,
fun(num,sF4213) = sF4214,
inference(reorient_equations,[],[f17715]) ).
fof(f17717,definition,
sF4215 = s(sF4214,l_a_),
introduced(definition,[new_symbols(definition,[sF4215])],[function_definition]) ).
fof(f17718,plain,
s(sF4214,l_a_) = sF4215,
inference(reorient_equations,[],[f17717]) ).
fof(f17719,definition,
sF4216 = fun(sF4207,num),
introduced(definition,[new_symbols(definition,[sF4216])],[function_definition]) ).
fof(f17720,plain,
fun(sF4207,num) = sF4216,
inference(reorient_equations,[],[f17719]) ).
fof(f17721,definition,
sF4217 = s(sF4216,card),
introduced(definition,[new_symbols(definition,[sF4217])],[function_definition]) ).
fof(f17722,plain,
s(sF4216,card) = sF4217,
inference(reorient_equations,[],[f17721]) ).
fof(f17723,definition,
sF4218 = i(sF4217,sF4210),
introduced(definition,[new_symbols(definition,[sF4218])],[function_definition]) ).
fof(f17724,plain,
i(sF4217,sF4210) = sF4218,
inference(reorient_equations,[],[f17723]) ).
fof(f17725,definition,
sF4219 = s(num,sF4218),
introduced(definition,[new_symbols(definition,[sF4219])],[function_definition]) ).
fof(f17726,plain,
s(num,sF4218) = sF4219,
inference(reorient_equations,[],[f17725]) ).
fof(f17727,definition,
sF4220 = i(sF4215,sF4219),
introduced(definition,[new_symbols(definition,[sF4220])],[function_definition]) ).
fof(f17728,plain,
i(sF4215,sF4219) = sF4220,
inference(reorient_equations,[],[f17727]) ).
fof(f17729,definition,
sF4221 = s(sF4213,sF4220),
introduced(definition,[new_symbols(definition,[sF4221])],[function_definition]) ).
fof(f17730,plain,
s(sF4213,sF4220) = sF4221,
inference(reorient_equations,[],[f17729]) ).
fof(f17731,definition,
sF4222 = s(sF4207,sK4205),
introduced(definition,[new_symbols(definition,[sF4222])],[function_definition]) ).
fof(f17732,plain,
s(sF4207,sK4205) = sF4222,
inference(reorient_equations,[],[f17731]) ).
fof(f17733,definition,
sF4223 = i(sF4217,sF4222),
introduced(definition,[new_symbols(definition,[sF4223])],[function_definition]) ).
fof(f17734,plain,
i(sF4217,sF4222) = sF4223,
inference(reorient_equations,[],[f17733]) ).
fof(f17735,definition,
sF4224 = s(num,sF4223),
introduced(definition,[new_symbols(definition,[sF4224])],[function_definition]) ).
fof(f17736,plain,
s(num,sF4223) = sF4224,
inference(reorient_equations,[],[f17735]) ).
fof(f17737,definition,
sF4225 = i(sF4221,sF4224),
introduced(definition,[new_symbols(definition,[sF4225])],[function_definition]) ).
fof(f17738,plain,
i(sF4221,sF4224) = sF4225,
inference(reorient_equations,[],[f17737]) ).
fof(f17739,definition,
sF4226 = s(bool,sF4225),
introduced(definition,[new_symbols(definition,[sF4226])],[function_definition]) ).
fof(f17740,plain,
s(bool,sF4225) = sF4226,
inference(reorient_equations,[],[f17739]) ).
fof(f17741,plain,
( ~ p(sF4212)
| ~ p(sF4226) ),
inference(definition_folding,[],[f17698,f17740,f17738,f17736,f17734,f17732,f17702,f17700,f17722,f17720,f17702,f17700,f17730,f17728,f17726,f17724,f17708,f17702,f17700,f17722,f17720,f17702,f17700,f17718,f17716,f17714,f17714,f17712,f17710,f17708,f17702,f17700,f17706,f17704,f17702,f17700]) ).
fof(f17742,definition,
sF4227 = i(sF4209,sF4222),
introduced(definition,[new_symbols(definition,[sF4227])],[function_definition]) ).
fof(f17743,plain,
i(sF4209,sF4222) = sF4227,
inference(reorient_equations,[],[f17742]) ).
fof(f17744,definition,
sF4228 = s(bool,sF4227),
introduced(definition,[new_symbols(definition,[sF4228])],[function_definition]) ).
fof(f17745,plain,
s(bool,sF4227) = sF4228,
inference(reorient_equations,[],[f17744]) ).
fof(f17746,plain,
p(sF4228),
inference(definition_folding,[],[f17697,f17745,f17743,f17732,f17702,f17700,f17706,f17704,f17702,f17700]) ).
fof(f17747,definition,
sF4229 = s(sF4208,independent),
introduced(definition,[new_symbols(definition,[sF4229])],[function_definition]) ).
fof(f17748,plain,
s(sF4208,independent) = sF4229,
inference(reorient_equations,[],[f17747]) ).
fof(f17749,definition,
sF4230 = i(sF4229,sF4210),
introduced(definition,[new_symbols(definition,[sF4230])],[function_definition]) ).
fof(f17750,plain,
i(sF4229,sF4210) = sF4230,
inference(reorient_equations,[],[f17749]) ).
fof(f17751,definition,
sF4231 = s(bool,sF4230),
introduced(definition,[new_symbols(definition,[sF4231])],[function_definition]) ).
fof(f17752,plain,
s(bool,sF4230) = sF4231,
inference(reorient_equations,[],[f17751]) ).
fof(f17753,plain,
p(sF4231),
inference(definition_folding,[],[f17696,f17752,f17750,f17708,f17702,f17700,f17748,f17704,f17702,f17700]) ).
fof(f17754,definition,
sF4232 = fun(sF4207,sF4208),
introduced(definition,[new_symbols(definition,[sF4232])],[function_definition]) ).
fof(f17755,plain,
fun(sF4207,sF4208) = sF4232,
inference(reorient_equations,[],[f17754]) ).
fof(f17756,definition,
sF4233 = s(sF4232,subset),
introduced(definition,[new_symbols(definition,[sF4233])],[function_definition]) ).
fof(f17757,plain,
s(sF4232,subset) = sF4233,
inference(reorient_equations,[],[f17756]) ).
fof(f17758,definition,
sF4234 = i(sF4233,sF4210),
introduced(definition,[new_symbols(definition,[sF4234])],[function_definition]) ).
fof(f17759,plain,
i(sF4233,sF4210) = sF4234,
inference(reorient_equations,[],[f17758]) ).
fof(f17760,definition,
sF4235 = s(sF4208,sF4234),
introduced(definition,[new_symbols(definition,[sF4235])],[function_definition]) ).
fof(f17761,plain,
s(sF4208,sF4234) = sF4235,
inference(reorient_equations,[],[f17760]) ).
fof(f17762,definition,
sF4236 = fun(sF4207,sF4207),
introduced(definition,[new_symbols(definition,[sF4236])],[function_definition]) ).
fof(f17763,plain,
fun(sF4207,sF4207) = sF4236,
inference(reorient_equations,[],[f17762]) ).
fof(f17764,definition,
sF4237 = s(sF4236,span),
introduced(definition,[new_symbols(definition,[sF4237])],[function_definition]) ).
fof(f17765,plain,
s(sF4236,span) = sF4237,
inference(reorient_equations,[],[f17764]) ).
fof(f17766,definition,
sF4238 = i(sF4237,sF4222),
introduced(definition,[new_symbols(definition,[sF4238])],[function_definition]) ).
fof(f17767,plain,
i(sF4237,sF4222) = sF4238,
inference(reorient_equations,[],[f17766]) ).
fof(f17768,definition,
sF4239 = s(sF4207,sF4238),
introduced(definition,[new_symbols(definition,[sF4239])],[function_definition]) ).
fof(f17769,plain,
s(sF4207,sF4238) = sF4239,
inference(reorient_equations,[],[f17768]) ).
fof(f17770,definition,
sF4240 = i(sF4235,sF4239),
introduced(definition,[new_symbols(definition,[sF4240])],[function_definition]) ).
fof(f17771,plain,
i(sF4235,sF4239) = sF4240,
inference(reorient_equations,[],[f17770]) ).
fof(f17772,definition,
sF4241 = s(bool,sF4240),
introduced(definition,[new_symbols(definition,[sF4241])],[function_definition]) ).
fof(f17773,plain,
s(bool,sF4240) = sF4241,
inference(reorient_equations,[],[f17772]) ).
fof(f17774,plain,
p(sF4241),
inference(definition_folding,[],[f17695,f17773,f17771,f17769,f17767,f17732,f17702,f17700,f17765,f17763,f17702,f17700,f17702,f17700,f17702,f17700,f17761,f17759,f17708,f17702,f17700,f17757,f17755,f17704,f17702,f17700,f17702,f17700,f17704,f17702,f17700]) ).
fof(f17793,definition,
( spl4242_1
<=> p(sF4226) ),
introduced(definition,[new_symbols(definition,[spl4242_1])],[avatar_definition]) ).
fof(f17797,definition,
( spl4242_2
<=> p(sF4212) ),
introduced(definition,[new_symbols(definition,[spl4242_2])],[avatar_definition]) ).
fof(f17798,plain,
( p(sF4212)
| ~ spl4242_2 ),
inference(avatar_component_clause,[],[f17797]) ).
fof(f17799,plain,
( ~ p(sF4212)
| spl4242_2 ),
inference(avatar_component_clause,[],[f17797]) ).
fof(f17800,plain,
( ~ spl4242_1
| ~ spl4242_2 ),
inference(avatar_split_clause,[],[f17741,f17797,f17793]) ).
fof(f18144,definition,
( spl4242_63
<=> p(s(bool,f0)) ),
introduced(definition,[new_symbols(definition,[spl4242_63])],[avatar_definition]) ).
fof(f18145,plain,
( ~ p(s(bool,f0))
| spl4242_63 ),
inference(avatar_component_clause,[],[f18144]) ).
fof(f19107,plain,
~ spl4242_63,
inference(avatar_split_clause,[],[f10463,f18144]) ).
fof(f20474,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(superposition,[],[f17694,f17700]) ).
fof(f20480,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,X0))),s(sF4207,i(s(fun(sF4207,sF4207),span),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f20474,f17702]) ).
fof(f20486,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,X0))),s(sF4207,i(s(sF4236,span),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f20480,f17763]) ).
fof(f20488,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f20486,f17765]) ).
fof(f20489,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(s(fun(sF4207,sF4208),subset),s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f20488,f17704]) ).
fof(f20490,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(s(sF4232,subset),s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f20489,f17755]) ).
fof(f20491,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f20490,f17757]) ).
fof(f20492,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f20491,f17702]) ).
fof(f20493,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,finite),s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f20492,f17704]) ).
fof(f20494,plain,
! [X0,X1] :
( ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f20493,f17706]) ).
fof(f20495,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),independent),s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f20494,f17702]) ).
fof(f20496,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,independent),s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f20495,f17704]) ).
fof(f20497,plain,
! [X0,X1] :
( ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(fun(sF4206,bool),fun(num,bool)),hasu_size),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(num,i(s(fun(fun(sF4206,bool),num),card),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f20496,f17748]) ).
fof(f20498,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(num,bool),i(s(fun(sF4207,fun(num,bool)),hasu_size),s(sF4207,sK4202(sK4203,X0,X1)))),s(num,i(s(fun(sF4207,num),card),s(sF4207,X1))))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f20497,f17702]) ).
fof(f20499,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(num,bool),i(s(fun(sF4207,fun(num,bool)),hasu_size),s(sF4207,sK4202(sK4203,X0,X1)))),s(num,i(s(sF4216,card),s(sF4207,X1))))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f20498,f17720]) ).
fof(f20500,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(num,bool),i(s(fun(sF4207,fun(num,bool)),hasu_size),s(sF4207,sK4202(sK4203,X0,X1)))),s(num,i(sF4217,s(sF4207,X1))))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f20499,f17722]) ).
fof(f20501,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,X0,X1)))),s(num,i(sF4217,s(sF4207,X1))))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f20500,f17714]) ).
fof(f20659,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(superposition,[],[f17693,f17700]) ).
fof(f20664,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,X0))),s(sF4207,i(s(fun(sF4207,sF4207),span),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20659,f17702]) ).
fof(f20666,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,X0))),s(sF4207,i(s(sF4236,span),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20664,f17763]) ).
fof(f20667,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20666,f17765]) ).
fof(f20668,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(s(fun(sF4207,sF4208),subset),s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20667,f17704]) ).
fof(f20669,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(s(sF4232,subset),s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20668,f17755]) ).
fof(f20670,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20669,f17757]) ).
fof(f20671,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20670,f17702]) ).
fof(f20672,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,finite),s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20671,f17704]) ).
fof(f20673,plain,
! [X0,X1] :
( ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20672,f17706]) ).
fof(f20674,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),independent),s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20673,f17702]) ).
fof(f20675,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,independent),s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20674,f17704]) ).
fof(f20676,plain,
! [X0,X1] :
( ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20675,f17748]) ).
fof(f20677,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,X0))),s(sF4207,sK4202(sK4203,X0,X1)))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f20676,f17702]) ).
fof(f20678,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4208,i(s(fun(sF4207,sF4208),subset),s(sF4207,X0))),s(sF4207,sK4202(sK4203,X0,X1)))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f20677,f17704]) ).
fof(f20679,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4208,i(s(sF4232,subset),s(sF4207,X0))),s(sF4207,sK4202(sK4203,X0,X1)))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f20678,f17755]) ).
fof(f20680,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,sK4202(sK4203,X0,X1))))) ),
inference(forward_demodulation,[],[f20679,f17757]) ).
fof(f21875,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),sK4202(sK4203,X0,X1)))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),fun(sF4206,bool))),union),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1)))))) ),
inference(superposition,[],[f17692,f17700]) ).
fof(f21880,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(fun(sF4207,sF4207),i(s(fun(sF4207,fun(sF4207,sF4207)),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f21875,f17702]) ).
fof(f21883,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f21880,f17763]) ).
fof(f21884,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4208,i(s(fun(sF4207,sF4208),subset),s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f21883,f17704]) ).
fof(f21885,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4208,i(s(sF4232,subset),s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f21884,f17755]) ).
fof(f21886,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),finite),s(fun(sF4206,bool),X1))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f21885,f17757]) ).
fof(f21887,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f21886,f17702]) ).
fof(f21888,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,finite),s(sF4207,X1))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f21887,f17704]) ).
fof(f21889,plain,
! [X0,X1] :
( ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),independent),s(fun(sF4206,bool),X0))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f21888,f17706]) ).
fof(f21890,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),independent),s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f21889,f17702]) ).
fof(f21891,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,independent),s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f21890,f17704]) ).
fof(f21892,plain,
! [X0,X1] :
( ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(fun(sF4206,bool),bool),i(s(fun(fun(sF4206,bool),fun(fun(sF4206,bool),bool)),subset),s(fun(sF4206,bool),X0))),s(fun(sF4206,bool),i(s(fun(fun(sF4206,bool),fun(sF4206,bool)),span),s(fun(sF4206,bool),X1)))))) ),
inference(forward_demodulation,[],[f21891,f17748]) ).
fof(f21893,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,X0))),s(sF4207,i(s(fun(sF4207,sF4207),span),s(sF4207,X1))))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f21892,f17702]) ).
fof(f21894,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,X0))),s(sF4207,i(s(sF4236,span),s(sF4207,X1))))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f21893,f17763]) ).
fof(f21895,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f21894,f17765]) ).
fof(f21896,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(s(fun(sF4207,sF4208),subset),s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f21895,f17704]) ).
fof(f21897,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(s(sF4232,subset),s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f21896,f17755]) ).
fof(f21898,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,X0,X1)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f21897,f17757]) ).
fof(f22401,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(num,bool),i(s(fun(sF4207,fun(num,bool)),hasu_size),s(sF4207,X0))),s(num,X1))))
| s(num,X1) = s(num,i(s(fun(sF4207,num),card),s(sF4207,X0))) ),
inference(superposition,[],[f14038,f17702]) ).
fof(f22409,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,X0))),s(num,X1))))
| s(num,X1) = s(num,i(s(fun(sF4207,num),card),s(sF4207,X0))) ),
inference(forward_demodulation,[],[f22401,f17714]) ).
fof(f22411,plain,
! [X0,X1] :
( s(num,X1) = s(num,i(s(sF4216,card),s(sF4207,X0)))
| ~ p(s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,X0))),s(num,X1)))) ),
inference(forward_demodulation,[],[f22409,f17720]) ).
fof(f22412,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,X0))),s(num,X1))))
| s(num,X1) = s(num,i(sF4217,s(sF4207,X0))) ),
inference(forward_demodulation,[],[f22411,f17722]) ).
fof(f22414,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X1))),s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4229,s(sF4207,X1))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| s(num,i(sF4217,s(sF4207,X0))) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,X1,X0)))) ),
inference(resolution,[],[f22412,f20501]) ).
fof(f22485,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| s(num,i(sF4217,s(sF4207,X0))) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,X0)))) ),
inference(superposition,[],[f22414,f17708]) ).
fof(f22527,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4208,sF4234),s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| s(num,i(sF4217,s(sF4207,X0))) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,X0)))) ),
inference(forward_demodulation,[],[f22485,f17759]) ).
fof(f22533,plain,
! [X0] :
( ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| s(num,i(sF4217,s(sF4207,X0))) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,X0)))) ),
inference(forward_demodulation,[],[f22527,f17761]) ).
fof(f22537,plain,
! [X0] :
( ~ p(s(bool,sF4230))
| ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| s(num,i(sF4217,s(sF4207,X0))) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,X0)))) ),
inference(forward_demodulation,[],[f22533,f17750]) ).
fof(f22539,plain,
! [X0] :
( ~ p(sF4231)
| ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| s(num,i(sF4217,s(sF4207,X0))) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,X0)))) ),
inference(forward_demodulation,[],[f22537,f17752]) ).
fof(f22541,plain,
! [X0] :
( ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| s(num,i(sF4217,s(sF4207,X0))) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,X0)))) ),
inference(forward_subsumption_resolution,[],[f22539,f17753]) ).
fof(f22553,plain,
( ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,sF4222)))))
| ~ p(s(bool,i(sF4209,sF4222)))
| s(num,i(sF4217,sF4222)) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,sK4205)))) ),
inference(superposition,[],[f22541,f17732]) ).
fof(f22562,plain,
( ~ p(s(bool,i(sF4235,s(sF4207,sF4238))))
| ~ p(s(bool,i(sF4209,sF4222)))
| s(num,i(sF4217,sF4222)) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,sK4205)))) ),
inference(forward_demodulation,[],[f22553,f17767]) ).
fof(f22568,plain,
( ~ p(s(bool,i(sF4235,sF4239)))
| ~ p(s(bool,i(sF4209,sF4222)))
| s(num,i(sF4217,sF4222)) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,sK4205)))) ),
inference(forward_demodulation,[],[f22562,f17769]) ).
fof(f22572,plain,
( ~ p(s(bool,sF4240))
| ~ p(s(bool,i(sF4209,sF4222)))
| s(num,i(sF4217,sF4222)) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,sK4205)))) ),
inference(forward_demodulation,[],[f22568,f17771]) ).
fof(f22576,plain,
( ~ p(sF4241)
| ~ p(s(bool,i(sF4209,sF4222)))
| s(num,i(sF4217,sF4222)) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,sK4205)))) ),
inference(forward_demodulation,[],[f22572,f17773]) ).
fof(f22579,plain,
( ~ p(s(bool,i(sF4209,sF4222)))
| s(num,i(sF4217,sF4222)) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,sK4205)))) ),
inference(forward_subsumption_resolution,[],[f22576,f17774]) ).
fof(f22581,plain,
( ~ p(s(bool,sF4227))
| s(num,i(sF4217,sF4222)) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,sK4205)))) ),
inference(forward_demodulation,[],[f22579,f17743]) ).
fof(f22583,plain,
( ~ p(sF4228)
| s(num,i(sF4217,sF4222)) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,sK4205)))) ),
inference(forward_demodulation,[],[f22581,f17745]) ).
fof(f22584,plain,
s(num,i(sF4217,sF4222)) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,sK4205)))),
inference(forward_subsumption_resolution,[],[f22583,f17746]) ).
fof(f22585,plain,
s(num,sF4223) = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,sK4205)))),
inference(forward_demodulation,[],[f22584,f17734]) ).
fof(f22586,plain,
sF4224 = s(num,i(sF4217,s(sF4207,sK4202(sK4203,sK4204,sK4205)))),
inference(forward_demodulation,[],[f22585,f17736]) ).
fof(f22612,definition,
( spl4242_267
<=> p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
introduced(definition,[new_symbols(definition,[spl4242_267])],[avatar_definition]) ).
fof(f22613,plain,
( p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| ~ spl4242_267 ),
inference(avatar_component_clause,[],[f22612]) ).
fof(f22614,plain,
( ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| spl4242_267 ),
inference(avatar_component_clause,[],[f22612]) ).
fof(f23104,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,X0))),s(sF4207,X1))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(sF4207,num),card),s(sF4207,X0))))),s(num,i(s(fun(sF4207,num),card),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(superposition,[],[f14065,f17702]) ).
fof(f23109,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(s(fun(sF4207,sF4208),subset),s(sF4207,X0))),s(sF4207,X1))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(sF4207,num),card),s(sF4207,X0))))),s(num,i(s(fun(sF4207,num),card),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f23104,f17704]) ).
fof(f23119,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(s(sF4232,subset),s(sF4207,X0))),s(sF4207,X1))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(sF4207,num),card),s(sF4207,X0))))),s(num,i(s(fun(sF4207,num),card),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f23109,f17755]) ).
fof(f23128,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1))))
| p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(sF4207,num),card),s(sF4207,X0))))),s(num,i(s(fun(sF4207,num),card),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f23119,f17757]) ).
fof(f23137,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(sF4216,card),s(sF4207,X0))))),s(num,i(s(sF4216,card),s(sF4207,X1))))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f23128,f17720]) ).
fof(f23139,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(sF4217,s(sF4207,X0))))),s(num,i(sF4217,s(sF4207,X1))))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f23137,f17722]) ).
fof(f23140,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4213,i(s(fun(num,sF4213),l_a_),s(num,i(sF4217,s(sF4207,X0))))),s(num,i(sF4217,s(sF4207,X1))))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f23139,f17714]) ).
fof(f23141,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4213,i(s(sF4214,l_a_),s(num,i(sF4217,s(sF4207,X0))))),s(num,i(sF4217,s(sF4207,X1))))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f23140,f17716]) ).
fof(f23142,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4213,i(sF4215,s(num,i(sF4217,s(sF4207,X0))))),s(num,i(sF4217,s(sF4207,X1))))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f23141,f17718]) ).
fof(f23143,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,finite),s(sF4207,X1))))
| p(s(bool,i(s(sF4213,i(sF4215,s(num,i(sF4217,s(sF4207,X0))))),s(num,i(sF4217,s(sF4207,X1))))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f23142,f17704]) ).
fof(f23144,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4213,i(sF4215,s(num,i(sF4217,s(sF4207,X0))))),s(num,i(sF4217,s(sF4207,X1))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f23143,f17706]) ).
fof(f23158,plain,
! [X0] :
( p(s(bool,i(s(sF4213,i(sF4215,s(num,i(sF4217,sF4210)))),s(num,i(sF4217,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,X0)))) ),
inference(superposition,[],[f23144,f17708]) ).
fof(f23176,plain,
! [X0] :
( p(s(bool,i(s(sF4213,i(sF4215,s(num,sF4218))),s(num,i(sF4217,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f23158,f17724]) ).
fof(f23180,plain,
! [X0] :
( p(s(bool,i(s(sF4213,i(sF4215,sF4219)),s(num,i(sF4217,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f23176,f17726]) ).
fof(f23183,plain,
! [X0] :
( p(s(bool,i(s(sF4213,sF4220),s(num,i(sF4217,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f23180,f17728]) ).
fof(f23186,plain,
! [X0] :
( p(s(bool,i(sF4221,s(num,i(sF4217,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f23183,f17730]) ).
fof(f23188,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4208,sF4234),s(sF4207,X0))))
| p(s(bool,i(sF4221,s(num,i(sF4217,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f23186,f17759]) ).
fof(f23189,plain,
! [X0] :
( p(s(bool,i(sF4221,s(num,i(sF4217,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4235,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f23188,f17761]) ).
fof(f23322,plain,
( p(s(bool,i(sF4221,sF4224)))
| ~ p(s(bool,i(sF4235,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(superposition,[],[f23189,f22586]) ).
fof(f24119,plain,
! [X0] : s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0))) = s(bool,i(s(fun(num,bool),i(s(fun(sF4207,fun(num,bool)),hasu_size),s(sF4207,X0))),s(num,i(s(fun(sF4207,num),card),s(sF4207,X0))))),
inference(superposition,[],[f14057,f17702]) ).
fof(f24123,plain,
! [X0] : s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0))) = s(bool,i(s(fun(num,bool),i(s(fun(sF4207,fun(num,bool)),hasu_size),s(sF4207,X0))),s(num,i(s(sF4216,card),s(sF4207,X0))))),
inference(forward_demodulation,[],[f24119,f17720]) ).
fof(f24125,plain,
! [X0] : s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0))) = s(bool,i(s(fun(num,bool),i(s(fun(sF4207,fun(num,bool)),hasu_size),s(sF4207,X0))),s(num,i(sF4217,s(sF4207,X0))))),
inference(forward_demodulation,[],[f24123,f17722]) ).
fof(f24126,plain,
! [X0] : s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0))) = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,X0))),s(num,i(sF4217,s(sF4207,X0))))),
inference(forward_demodulation,[],[f24125,f17714]) ).
fof(f24127,plain,
! [X0] : s(bool,i(s(sF4208,finite),s(sF4207,X0))) = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,X0))),s(num,i(sF4217,s(sF4207,X0))))),
inference(forward_demodulation,[],[f24126,f17704]) ).
fof(f24128,plain,
! [X0] : s(bool,i(sF4209,s(sF4207,X0))) = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,X0))),s(num,i(sF4217,s(sF4207,X0))))),
inference(forward_demodulation,[],[f24127,f17706]) ).
fof(f24139,plain,
s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205)))) = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,sK4205)))),sF4224)),
inference(superposition,[],[f24128,f22586]) ).
fof(f24435,plain,
! [X0] :
( p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,sK4204,X0)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),s(sF4207,X0))))))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,i(sF4237,s(sF4207,X0)))))) ),
inference(superposition,[],[f21898,f17708]) ).
fof(f24453,plain,
! [X0] :
( ~ p(s(bool,sF4230))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,sK4204,X0)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,i(sF4237,s(sF4207,X0)))))) ),
inference(forward_demodulation,[],[f24435,f17750]) ).
fof(f24459,plain,
! [X0] :
( ~ p(sF4231)
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,sK4204,X0)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,i(sF4237,s(sF4207,X0)))))) ),
inference(forward_demodulation,[],[f24453,f17752]) ).
fof(f24462,plain,
! [X0] :
( p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,sK4204,X0)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,i(sF4237,s(sF4207,X0)))))) ),
inference(forward_subsumption_resolution,[],[f24459,f17753]) ).
fof(f24464,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4208,sF4234),s(sF4207,i(sF4237,s(sF4207,X0))))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,sK4204,X0)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f24462,f17759]) ).
fof(f24466,plain,
! [X0] :
( p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,sK4202(sK4203,sK4204,X0)))),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),s(sF4207,X0))))))
| ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f24464,f17761]) ).
fof(f25147,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,i(s(fun(sF4207,sF4207),i(s(fun(sF4207,fun(sF4207,sF4207)),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(superposition,[],[f13866,f17702]) ).
fof(f25151,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f25147,f17763]) ).
fof(f25152,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4208,finite),s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f25151,f17704]) ).
fof(f25153,plain,
! [X0,X1] :
( p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f25152,f17706]) ).
fof(f25154,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,finite),s(sF4207,X0))))
| p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f25153,f17704]) ).
fof(f25155,plain,
! [X0,X1] :
( ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f25154,f17706]) ).
fof(f25156,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,finite),s(sF4207,X1))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1)))))) ),
inference(forward_demodulation,[],[f25155,f17704]) ).
fof(f25157,plain,
! [X0,X1] :
( p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),s(sF4207,X1))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f25156,f17706]) ).
fof(f25176,plain,
! [X0] :
( p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),sF4222)))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,sF4222))) ),
inference(superposition,[],[f25157,f17732]) ).
fof(f25178,plain,
! [X0] :
( ~ p(s(bool,sF4227))
| p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),sF4222)))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f25176,f17743]) ).
fof(f25182,plain,
! [X0] :
( ~ p(sF4228)
| p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),sF4222)))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f25178,f17745]) ).
fof(f25186,plain,
! [X0] :
( p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),s(sF4207,X0))),sF4222)))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0)))) ),
inference(forward_subsumption_resolution,[],[f25182,f17746]) ).
fof(f25195,plain,
( p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),sF4222)))))
| ~ p(s(bool,i(sF4209,sF4210))) ),
inference(superposition,[],[f25186,f17708]) ).
fof(f25199,plain,
( ~ p(s(bool,sF4211))
| p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),sF4222))))) ),
inference(forward_demodulation,[],[f25195,f17710]) ).
fof(f25201,plain,
( ~ p(sF4212)
| p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),sF4222))))) ),
inference(forward_demodulation,[],[f25199,f17712]) ).
fof(f27185,plain,
! [X0] : s(bool,i(s(fun(sF4207,bool),X0),sF4210)) = s(bool,i(s(fun(fun(sF4207,bool),bool),i(s(fun(sF4207,fun(fun(sF4207,bool),bool)),in),sF4210)),s(fun(sF4207,bool),X0))),
inference(superposition,[],[f13195,f17708]) ).
fof(f27186,plain,
! [X0] : s(bool,i(s(fun(sF4207,bool),X0),sF4222)) = s(bool,i(s(fun(fun(sF4207,bool),bool),i(s(fun(sF4207,fun(fun(sF4207,bool),bool)),in),sF4222)),s(fun(sF4207,bool),X0))),
inference(superposition,[],[f13195,f17732]) ).
fof(f27187,plain,
! [X0] : s(bool,i(s(fun(sF4207,bool),X0),sF4239)) = s(bool,i(s(fun(fun(sF4207,bool),bool),i(s(fun(sF4207,fun(fun(sF4207,bool),bool)),in),sF4239)),s(fun(sF4207,bool),X0))),
inference(superposition,[],[f13195,f17769]) ).
fof(f27220,plain,
! [X0] : s(bool,i(s(sF4208,X0),sF4239)) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4239)),s(sF4208,X0))),
inference(forward_demodulation,[],[f27187,f17704]) ).
fof(f27221,plain,
! [X0] : s(bool,i(s(sF4208,X0),sF4222)) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4222)),s(sF4208,X0))),
inference(forward_demodulation,[],[f27186,f17704]) ).
fof(f27222,plain,
! [X0] : s(bool,i(s(sF4208,X0),sF4210)) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4210)),s(sF4208,X0))),
inference(forward_demodulation,[],[f27185,f17704]) ).
fof(f27233,plain,
s(bool,i(sF4209,sF4222)) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4222)),sF4209)),
inference(superposition,[],[f27221,f17706]) ).
fof(f27237,plain,
s(bool,sF4227) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4222)),sF4209)),
inference(forward_demodulation,[],[f27233,f17743]) ).
fof(f27238,plain,
sF4228 = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4222)),sF4209)),
inference(forward_demodulation,[],[f27237,f17745]) ).
fof(f27241,plain,
s(bool,i(sF4235,sF4239)) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4239)),sF4235)),
inference(superposition,[],[f27220,f17761]) ).
fof(f27244,plain,
s(bool,sF4240) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4239)),sF4235)),
inference(forward_demodulation,[],[f27241,f17771]) ).
fof(f27245,plain,
sF4241 = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4239)),sF4235)),
inference(forward_demodulation,[],[f27244,f17773]) ).
fof(f27247,plain,
s(bool,i(sF4209,sF4210)) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4210)),sF4209)),
inference(superposition,[],[f27222,f17706]) ).
fof(f27249,plain,
s(bool,i(sF4229,sF4210)) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4210)),sF4229)),
inference(superposition,[],[f27222,f17748]) ).
fof(f27251,plain,
s(bool,sF4230) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4210)),sF4229)),
inference(forward_demodulation,[],[f27249,f17750]) ).
fof(f27252,plain,
s(bool,sF4211) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4210)),sF4209)),
inference(forward_demodulation,[],[f27247,f17710]) ).
fof(f27253,plain,
sF4231 = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4210)),sF4229)),
inference(forward_demodulation,[],[f27251,f17752]) ).
fof(f27254,plain,
sF4212 = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4210)),sF4209)),
inference(forward_demodulation,[],[f27252,f17712]) ).
fof(f27889,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,sK4202(sK4203,sK4204,X0))))) ),
inference(superposition,[],[f20680,f17708]) ).
fof(f27901,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,sF4222)))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,sF4222)))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,sK4202(sK4203,X0,sK4205))))) ),
inference(superposition,[],[f20680,f17732]) ).
fof(f27912,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,sF4238))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,sF4222)))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,sK4202(sK4203,X0,sK4205))))) ),
inference(forward_demodulation,[],[f27901,f17767]) ).
fof(f27917,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4208,sF4234),s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,sK4202(sK4203,sK4204,X0))))) ),
inference(forward_demodulation,[],[f27889,f17759]) ).
fof(f27920,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),sF4239)))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,sF4222)))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,sK4202(sK4203,X0,sK4205))))) ),
inference(forward_demodulation,[],[f27912,f17769]) ).
fof(f27923,plain,
! [X0] :
( ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,sK4202(sK4203,sK4204,X0))))) ),
inference(forward_demodulation,[],[f27917,f17761]) ).
fof(f27925,plain,
! [X0] :
( ~ p(s(bool,sF4227))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),sF4239)))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,sK4202(sK4203,X0,sK4205))))) ),
inference(forward_demodulation,[],[f27920,f17743]) ).
fof(f27927,plain,
! [X0] :
( ~ p(s(bool,sF4230))
| ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,sK4202(sK4203,sK4204,X0))))) ),
inference(forward_demodulation,[],[f27923,f17750]) ).
fof(f27928,plain,
! [X0] :
( ~ p(sF4228)
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),sF4239)))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,sK4202(sK4203,X0,sK4205))))) ),
inference(forward_demodulation,[],[f27925,f17745]) ).
fof(f27929,plain,
! [X0] :
( ~ p(sF4231)
| ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,sK4202(sK4203,sK4204,X0))))) ),
inference(forward_demodulation,[],[f27927,f17752]) ).
fof(f27930,plain,
! [X0] :
( p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,sK4202(sK4203,X0,sK4205)))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),sF4239))) ),
inference(forward_subsumption_resolution,[],[f27928,f17746]) ).
fof(f27931,plain,
! [X0] :
( ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,sK4202(sK4203,sK4204,X0))))) ),
inference(forward_subsumption_resolution,[],[f27929,f17753]) ).
fof(f27932,plain,
! [X0] :
( p(s(bool,i(s(sF4208,sF4234),s(sF4207,sK4202(sK4203,sK4204,X0)))))
| ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f27931,f17759]) ).
fof(f27933,plain,
! [X0] :
( ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| p(s(bool,i(sF4235,s(sF4207,sK4202(sK4203,sK4204,X0)))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f27932,f17761]) ).
fof(f27944,plain,
( ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,sF4222)))))
| p(s(bool,i(sF4235,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| ~ p(s(bool,i(sF4209,sF4222))) ),
inference(superposition,[],[f27933,f17732]) ).
fof(f27954,plain,
( ~ p(s(bool,i(sF4235,s(sF4207,sF4238))))
| p(s(bool,i(sF4235,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| ~ p(s(bool,i(sF4209,sF4222))) ),
inference(forward_demodulation,[],[f27944,f17767]) ).
fof(f27960,plain,
( ~ p(s(bool,i(sF4235,sF4239)))
| p(s(bool,i(sF4235,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| ~ p(s(bool,i(sF4209,sF4222))) ),
inference(forward_demodulation,[],[f27954,f17769]) ).
fof(f27964,plain,
( ~ p(s(bool,sF4240))
| p(s(bool,i(sF4235,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| ~ p(s(bool,i(sF4209,sF4222))) ),
inference(forward_demodulation,[],[f27960,f17771]) ).
fof(f27968,plain,
( ~ p(sF4241)
| p(s(bool,i(sF4235,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| ~ p(s(bool,i(sF4209,sF4222))) ),
inference(forward_demodulation,[],[f27964,f17773]) ).
fof(f27971,plain,
( p(s(bool,i(sF4235,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| ~ p(s(bool,i(sF4209,sF4222))) ),
inference(forward_subsumption_resolution,[],[f27968,f17774]) ).
fof(f27973,plain,
( ~ p(s(bool,sF4227))
| p(s(bool,i(sF4235,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(forward_demodulation,[],[f27971,f17743]) ).
fof(f27975,plain,
( ~ p(sF4228)
| p(s(bool,i(sF4235,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(forward_demodulation,[],[f27973,f17745]) ).
fof(f27977,plain,
p(s(bool,i(sF4235,s(sF4207,sK4202(sK4203,sK4204,sK4205))))),
inference(forward_subsumption_resolution,[],[f27975,f17746]) ).
fof(f28266,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(sF4207,bool),i(s(fun(sF4207,fun(sF4207,bool)),subset),s(sF4207,X0))),s(sF4207,X1))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1))))
| p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0)))) ),
inference(superposition,[],[f13862,f17702]) ).
fof(f28271,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(s(fun(sF4207,sF4208),subset),s(sF4207,X0))),s(sF4207,X1))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1))))
| p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f28266,f17704]) ).
fof(f28273,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(s(sF4232,subset),s(sF4207,X0))),s(sF4207,X1))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1))))
| p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f28271,f17755]) ).
fof(f28274,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1))))
| ~ p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X1))))
| p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f28273,f17757]) ).
fof(f28275,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,finite),s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1))))
| p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f28274,f17704]) ).
fof(f28276,plain,
! [X0,X1] :
( ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1))))
| p(s(bool,i(s(fun(sF4207,bool),finite),s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f28275,f17706]) ).
fof(f28277,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4208,finite),s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1)))) ),
inference(forward_demodulation,[],[f28276,f17704]) ).
fof(f28278,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,X1))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| p(s(bool,i(sF4209,s(sF4207,X0)))) ),
inference(forward_demodulation,[],[f28277,f17706]) ).
fof(f28318,plain,
! [X0] :
( ~ p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),s(sF4207,X0))))))
| p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,X0)))))
| ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0)))) ),
inference(resolution,[],[f28278,f24466]) ).
fof(f28322,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),sF4239)))
| p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,X0,sK4205))))) ),
inference(resolution,[],[f28278,f27930]) ).
fof(f29084,plain,
( ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),sF4239)))
| p(s(bool,i(sF4209,sF4210)))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(superposition,[],[f28322,f17708]) ).
fof(f30379,plain,
( ~ p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),sF4222)))))
| p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,sF4222)))))
| ~ p(s(bool,i(sF4209,sF4222))) ),
inference(superposition,[],[f28318,f17732]) ).
fof(f31381,plain,
! [X0,X1] :
( p(s(bool,f0))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| s(bool,t) = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,X0,X1)))),s(num,i(sF4217,s(sF4207,X1))))) ),
inference(superposition,[],[f20501,f10695]) ).
fof(f31549,plain,
( s(bool,f0) = sF4228
| s(bool,t) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4222)),sF4209)) ),
inference(superposition,[],[f27238,f10695]) ).
fof(f31550,plain,
( s(bool,f0) = sF4212
| s(bool,t) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4210)),sF4209)) ),
inference(superposition,[],[f27254,f10695]) ).
fof(f31609,plain,
( s(bool,f0) = sF4231
| s(bool,t) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4210)),sF4229)) ),
inference(superposition,[],[f27253,f10695]) ).
fof(f31611,plain,
( s(bool,f0) = sF4241
| s(bool,t) = s(bool,i(s(fun(sF4208,bool),i(s(fun(sF4207,fun(sF4208,bool)),in),sF4239)),sF4235)) ),
inference(superposition,[],[f27245,f10695]) ).
fof(f31660,plain,
( s(bool,t) = sF4241
| s(bool,f0) = sF4241 ),
inference(forward_demodulation,[],[f31611,f27245]) ).
fof(f31661,plain,
( s(bool,t) = sF4231
| s(bool,f0) = sF4231 ),
inference(forward_demodulation,[],[f31609,f27253]) ).
fof(f31677,plain,
( s(bool,t) = sF4212
| s(bool,f0) = sF4212 ),
inference(forward_demodulation,[],[f31550,f27254]) ).
fof(f31678,plain,
( s(bool,t) = sF4228
| s(bool,f0) = sF4228 ),
inference(forward_demodulation,[],[f31549,f27238]) ).
fof(f31750,plain,
( ! [X0,X1] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,s(sF4207,X0))),s(sF4207,i(sF4237,s(sF4207,X1))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X1))))
| ~ p(s(bool,i(sF4229,s(sF4207,X0))))
| s(bool,t) = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,X0,X1)))),s(num,i(sF4217,s(sF4207,X1))))) )
| spl4242_63 ),
inference(forward_subsumption_resolution,[],[f31381,f18145]) ).
fof(f31839,definition,
( spl4242_379
<=> s(bool,t) = sF4241 ),
introduced(definition,[new_symbols(definition,[spl4242_379])],[avatar_definition]) ).
fof(f31841,plain,
( s(bool,t) = sF4241
| ~ spl4242_379 ),
inference(avatar_component_clause,[],[f31839]) ).
fof(f31843,definition,
( spl4242_380
<=> s(bool,f0) = sF4241 ),
introduced(definition,[new_symbols(definition,[spl4242_380])],[avatar_definition]) ).
fof(f31845,plain,
( s(bool,f0) = sF4241
| ~ spl4242_380 ),
inference(avatar_component_clause,[],[f31843]) ).
fof(f31848,definition,
( spl4242_381
<=> s(bool,t) = sF4231 ),
introduced(definition,[new_symbols(definition,[spl4242_381])],[avatar_definition]) ).
fof(f31850,plain,
( s(bool,t) = sF4231
| ~ spl4242_381 ),
inference(avatar_component_clause,[],[f31848]) ).
fof(f31852,definition,
( spl4242_382
<=> s(bool,f0) = sF4231 ),
introduced(definition,[new_symbols(definition,[spl4242_382])],[avatar_definition]) ).
fof(f31854,plain,
( s(bool,f0) = sF4231
| ~ spl4242_382 ),
inference(avatar_component_clause,[],[f31852]) ).
fof(f31857,definition,
( spl4242_383
<=> s(bool,t) = sF4228 ),
introduced(definition,[new_symbols(definition,[spl4242_383])],[avatar_definition]) ).
fof(f31859,plain,
( s(bool,t) = sF4228
| ~ spl4242_383 ),
inference(avatar_component_clause,[],[f31857]) ).
fof(f31861,definition,
( spl4242_384
<=> s(bool,f0) = sF4228 ),
introduced(definition,[new_symbols(definition,[spl4242_384])],[avatar_definition]) ).
fof(f31863,plain,
( s(bool,f0) = sF4228
| ~ spl4242_384 ),
inference(avatar_component_clause,[],[f31861]) ).
fof(f31875,definition,
( spl4242_387
<=> s(bool,t) = sF4212 ),
introduced(definition,[new_symbols(definition,[spl4242_387])],[avatar_definition]) ).
fof(f31877,plain,
( s(bool,t) = sF4212
| ~ spl4242_387 ),
inference(avatar_component_clause,[],[f31875]) ).
fof(f31879,definition,
( spl4242_388
<=> s(bool,f0) = sF4212 ),
introduced(definition,[new_symbols(definition,[spl4242_388])],[avatar_definition]) ).
fof(f31881,plain,
( s(bool,f0) = sF4212
| ~ spl4242_388 ),
inference(avatar_component_clause,[],[f31879]) ).
fof(f31897,plain,
( spl4242_380
| spl4242_379 ),
inference(avatar_split_clause,[],[f31660,f31839,f31843]) ).
fof(f31898,plain,
( spl4242_382
| spl4242_381 ),
inference(avatar_split_clause,[],[f31661,f31848,f31852]) ).
fof(f31902,plain,
( spl4242_388
| spl4242_387 ),
inference(avatar_split_clause,[],[f31677,f31875,f31879]) ).
fof(f31903,plain,
( spl4242_384
| spl4242_383 ),
inference(avatar_split_clause,[],[f31678,f31857,f31861]) ).
fof(f41685,plain,
( sF4228 = sF4231
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_demodulation,[],[f31859,f31850]) ).
fof(f42916,plain,
( ~ p(sF4241)
| spl4242_63
| ~ spl4242_380 ),
inference(superposition,[],[f18145,f31845]) ).
fof(f42919,plain,
( $false
| spl4242_63
| ~ spl4242_380 ),
inference(forward_subsumption_resolution,[],[f42916,f17774]) ).
fof(f42920,plain,
( spl4242_63
| ~ spl4242_380 ),
inference(avatar_contradiction_clause,[],[f42919]) ).
fof(f44294,plain,
( ! [X0] :
( ~ p(s(bool,i(s(sF4208,i(sF4233,sF4210)),s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(sF4229,sF4210)))
| s(bool,t) = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,X0)))),s(num,i(sF4217,s(sF4207,X0))))) )
| spl4242_63 ),
inference(superposition,[],[f31750,f17708]) ).
fof(f44333,plain,
( ! [X0] :
( ~ p(s(bool,i(s(sF4208,sF4234),s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(sF4229,sF4210)))
| s(bool,t) = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,X0)))),s(num,i(sF4217,s(sF4207,X0))))) )
| spl4242_63 ),
inference(forward_demodulation,[],[f44294,f17759]) ).
fof(f44347,plain,
( ! [X0] :
( ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| ~ p(s(bool,i(sF4229,sF4210)))
| s(bool,t) = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,X0)))),s(num,i(sF4217,s(sF4207,X0))))) )
| spl4242_63 ),
inference(forward_demodulation,[],[f44333,f17761]) ).
fof(f44358,plain,
( ! [X0] :
( ~ p(s(bool,sF4230))
| ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| s(bool,t) = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,X0)))),s(num,i(sF4217,s(sF4207,X0))))) )
| spl4242_63 ),
inference(forward_demodulation,[],[f44347,f17750]) ).
fof(f44361,plain,
( ! [X0] :
( ~ p(sF4231)
| ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| s(bool,t) = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,X0)))),s(num,i(sF4217,s(sF4207,X0))))) )
| spl4242_63 ),
inference(forward_demodulation,[],[f44358,f17752]) ).
fof(f44363,plain,
( ! [X0] :
( ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0))))
| s(bool,t) = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,X0)))),s(num,i(sF4217,s(sF4207,X0))))) )
| spl4242_63 ),
inference(forward_subsumption_resolution,[],[f44361,f17753]) ).
fof(f44365,plain,
( ! [X0] :
( sF4231 = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,X0)))),s(num,i(sF4217,s(sF4207,X0)))))
| ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0)))) )
| spl4242_63
| ~ spl4242_381 ),
inference(forward_demodulation,[],[f44363,f31850]) ).
fof(f44367,plain,
( ! [X0] :
( ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,s(sF4207,X0))))))
| sF4228 = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,X0)))),s(num,i(sF4217,s(sF4207,X0)))))
| ~ p(s(bool,i(sF4209,s(sF4207,X0)))) )
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_demodulation,[],[f44365,f41685]) ).
fof(f44379,plain,
( ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,sF4222)))))
| sF4228 = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,sK4205)))),s(num,i(sF4217,sF4222))))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(superposition,[],[f44367,f17732]) ).
fof(f44393,plain,
( ~ p(s(bool,i(sF4235,s(sF4207,sF4238))))
| sF4228 = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,sK4205)))),s(num,i(sF4217,sF4222))))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_demodulation,[],[f44379,f17767]) ).
fof(f44399,plain,
( ~ p(s(bool,i(sF4235,sF4239)))
| sF4228 = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,sK4205)))),s(num,i(sF4217,sF4222))))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_demodulation,[],[f44393,f17769]) ).
fof(f44402,plain,
( ~ p(s(bool,sF4240))
| sF4228 = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,sK4205)))),s(num,i(sF4217,sF4222))))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_demodulation,[],[f44399,f17771]) ).
fof(f44405,plain,
( ~ p(sF4241)
| sF4228 = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,sK4205)))),s(num,i(sF4217,sF4222))))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_demodulation,[],[f44402,f17773]) ).
fof(f44408,plain,
( sF4228 = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,sK4205)))),s(num,i(sF4217,sF4222))))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_subsumption_resolution,[],[f44405,f17774]) ).
fof(f44411,plain,
( sF4228 = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,sK4205)))),s(num,sF4223)))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_demodulation,[],[f44408,f17734]) ).
fof(f44412,plain,
( sF4228 = s(bool,i(s(sF4213,i(s(fun(sF4207,sF4213),hasu_size),s(sF4207,sK4202(sK4203,sK4204,sK4205)))),sF4224))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_demodulation,[],[f44411,f17736]) ).
fof(f44413,plain,
( sF4228 = s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_demodulation,[],[f44412,f24139]) ).
fof(f44414,plain,
( ~ p(s(bool,sF4227))
| sF4228 = s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_demodulation,[],[f44413,f17743]) ).
fof(f44415,plain,
( ~ p(sF4228)
| sF4228 = s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_demodulation,[],[f44414,f17745]) ).
fof(f44416,plain,
( sF4228 = s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_subsumption_resolution,[],[f44415,f17746]) ).
fof(f44588,plain,
( ~ p(s(bool,i(s(sF4208,sF4234),sF4239)))
| p(s(bool,i(sF4209,sF4210)))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(forward_demodulation,[],[f29084,f17759]) ).
fof(f44615,plain,
( ~ p(s(bool,i(sF4235,sF4239)))
| p(s(bool,i(sF4209,sF4210)))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(forward_demodulation,[],[f44588,f17761]) ).
fof(f44642,plain,
( ~ p(s(bool,sF4240))
| p(s(bool,i(sF4209,sF4210)))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(forward_demodulation,[],[f44615,f17771]) ).
fof(f44652,plain,
( ~ p(sF4241)
| p(s(bool,i(sF4209,sF4210)))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(forward_demodulation,[],[f44642,f17773]) ).
fof(f44655,definition,
( spl4242_441
<=> p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),sF4222))))) ),
introduced(definition,[new_symbols(definition,[spl4242_441])],[avatar_definition]) ).
fof(f44656,plain,
( p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),sF4222)))))
| ~ spl4242_441 ),
inference(avatar_component_clause,[],[f44655]) ).
fof(f44657,plain,
( ~ p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),sF4222)))))
| spl4242_441 ),
inference(avatar_component_clause,[],[f44655]) ).
fof(f44677,plain,
( p(s(bool,i(sF4209,sF4210)))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(forward_subsumption_resolution,[],[f44652,f17774]) ).
fof(f44682,plain,
( p(s(bool,sF4211))
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(forward_demodulation,[],[f44677,f17710]) ).
fof(f44684,plain,
( p(sF4212)
| ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(forward_demodulation,[],[f44682,f17712]) ).
fof(f44685,plain,
( ~ p(s(bool,i(sF4229,sF4210)))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| spl4242_2 ),
inference(forward_subsumption_resolution,[],[f44684,f17799]) ).
fof(f44686,plain,
( ~ p(s(bool,sF4230))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| spl4242_2 ),
inference(forward_demodulation,[],[f44685,f17750]) ).
fof(f44687,plain,
( ~ p(sF4231)
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| spl4242_2 ),
inference(forward_demodulation,[],[f44686,f17752]) ).
fof(f44688,plain,
( ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| spl4242_2 ),
inference(forward_subsumption_resolution,[],[f44687,f17753]) ).
fof(f44689,plain,
( ~ p(sF4228)
| spl4242_2
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_demodulation,[],[f44688,f44416]) ).
fof(f44690,plain,
( $false
| spl4242_2
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(forward_subsumption_resolution,[],[f44689,f17746]) ).
fof(f44691,plain,
( spl4242_2
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(avatar_contradiction_clause,[],[f44690]) ).
fof(f44716,plain,
( p(s(bool,i(sF4209,s(sF4207,i(s(sF4236,i(s(fun(sF4207,sF4236),union),sF4210)),sF4222)))))
| ~ spl4242_2 ),
inference(forward_subsumption_resolution,[],[f25201,f17798]) ).
fof(f44896,plain,
( p(s(bool,i(sF4221,sF4224)))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(forward_subsumption_resolution,[],[f23322,f27977]) ).
fof(f44929,plain,
( $false
| ~ spl4242_2
| spl4242_441 ),
inference(forward_subsumption_resolution,[],[f44716,f44657]) ).
fof(f44930,plain,
( ~ spl4242_2
| spl4242_441 ),
inference(avatar_contradiction_clause,[],[f44929]) ).
fof(f45003,plain,
( p(s(bool,sF4225))
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(forward_demodulation,[],[f44896,f17738]) ).
fof(f45060,plain,
( p(sF4226)
| ~ p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205))))) ),
inference(forward_demodulation,[],[f45003,f17740]) ).
fof(f45140,plain,
( sF4212 = sF4231
| ~ spl4242_382
| ~ spl4242_388 ),
inference(forward_demodulation,[],[f31881,f31854]) ).
fof(f45447,plain,
( p(sF4226)
| ~ spl4242_267 ),
inference(forward_subsumption_resolution,[],[f45060,f22613]) ).
fof(f45484,plain,
( spl4242_1
| ~ spl4242_267 ),
inference(avatar_split_clause,[],[f45447,f22612,f17793]) ).
fof(f45575,plain,
( p(sF4212)
| ~ spl4242_382
| ~ spl4242_388 ),
inference(superposition,[],[f17753,f45140]) ).
fof(f45576,plain,
( $false
| spl4242_2
| ~ spl4242_382
| ~ spl4242_388 ),
inference(forward_subsumption_resolution,[],[f45575,f17799]) ).
fof(f45577,plain,
( spl4242_2
| ~ spl4242_382
| ~ spl4242_388 ),
inference(avatar_contradiction_clause,[],[f45576]) ).
fof(f46345,plain,
( sF4212 = sF4241
| ~ spl4242_379
| ~ spl4242_387 ),
inference(forward_demodulation,[],[f31877,f31841]) ).
fof(f46487,plain,
( p(sF4212)
| ~ spl4242_379
| ~ spl4242_387 ),
inference(superposition,[],[f17774,f46345]) ).
fof(f46488,plain,
( $false
| spl4242_2
| ~ spl4242_379
| ~ spl4242_387 ),
inference(forward_subsumption_resolution,[],[f46487,f17799]) ).
fof(f46489,plain,
( spl4242_2
| ~ spl4242_379
| ~ spl4242_387 ),
inference(avatar_contradiction_clause,[],[f46488]) ).
fof(f46527,plain,
( sF4212 = sF4228
| ~ spl4242_384
| ~ spl4242_388 ),
inference(forward_demodulation,[],[f31863,f31881]) ).
fof(f46608,plain,
( p(sF4212)
| ~ spl4242_384
| ~ spl4242_388 ),
inference(superposition,[],[f17746,f46527]) ).
fof(f46609,plain,
( $false
| spl4242_2
| ~ spl4242_384
| ~ spl4242_388 ),
inference(forward_subsumption_resolution,[],[f46608,f17799]) ).
fof(f46610,plain,
( spl4242_2
| ~ spl4242_384
| ~ spl4242_388 ),
inference(avatar_contradiction_clause,[],[f46609]) ).
fof(f46625,plain,
( p(s(bool,i(sF4209,s(sF4207,sK4202(sK4203,sK4204,sK4205)))))
| ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,sF4222)))))
| ~ p(s(bool,i(sF4209,sF4222)))
| ~ spl4242_441 ),
inference(forward_subsumption_resolution,[],[f30379,f44656]) ).
fof(f46836,plain,
( ~ p(s(bool,i(sF4235,s(sF4207,i(sF4237,sF4222)))))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_267
| ~ spl4242_441 ),
inference(forward_subsumption_resolution,[],[f46625,f22614]) ).
fof(f46923,plain,
( ~ p(s(bool,i(sF4235,s(sF4207,sF4238))))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_267
| ~ spl4242_441 ),
inference(forward_demodulation,[],[f46836,f17767]) ).
fof(f47011,plain,
( ~ p(s(bool,i(sF4235,sF4239)))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_267
| ~ spl4242_441 ),
inference(forward_demodulation,[],[f46923,f17769]) ).
fof(f47066,plain,
( ~ p(s(bool,sF4240))
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_267
| ~ spl4242_441 ),
inference(forward_demodulation,[],[f47011,f17771]) ).
fof(f47097,plain,
( ~ p(sF4241)
| ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_267
| ~ spl4242_441 ),
inference(forward_demodulation,[],[f47066,f17773]) ).
fof(f47107,plain,
( ~ p(s(bool,i(sF4209,sF4222)))
| spl4242_267
| ~ spl4242_441 ),
inference(forward_subsumption_resolution,[],[f47097,f17774]) ).
fof(f47111,plain,
( ~ p(s(bool,sF4227))
| spl4242_267
| ~ spl4242_441 ),
inference(forward_demodulation,[],[f47107,f17743]) ).
fof(f47113,plain,
( ~ p(sF4228)
| spl4242_267
| ~ spl4242_441 ),
inference(forward_demodulation,[],[f47111,f17745]) ).
fof(f47114,plain,
( $false
| spl4242_267
| ~ spl4242_441 ),
inference(forward_subsumption_resolution,[],[f47113,f17746]) ).
fof(f47115,plain,
( spl4242_267
| ~ spl4242_441 ),
inference(avatar_contradiction_clause,[],[f47114]) ).
cnf(s1,plain,
( ~ spl4242_1
| ~ spl4242_2 ),
inference(sat_conversion,[],[f17800]) ).
cnf(s199,plain,
~ spl4242_63,
inference(sat_conversion,[],[f19107]) ).
cnf(s391,plain,
( spl4242_379
| spl4242_380 ),
inference(sat_conversion,[],[f31897]) ).
cnf(s392,plain,
( spl4242_381
| spl4242_382 ),
inference(sat_conversion,[],[f31898]) ).
cnf(s396,plain,
( spl4242_387
| spl4242_388 ),
inference(sat_conversion,[],[f31902]) ).
cnf(s397,plain,
( spl4242_383
| spl4242_384 ),
inference(sat_conversion,[],[f31903]) ).
cnf(s443,plain,
( spl4242_63
| ~ spl4242_380 ),
inference(sat_conversion,[],[f42920]) ).
cnf(s466,plain,
( spl4242_2
| spl4242_63
| ~ spl4242_381
| ~ spl4242_383 ),
inference(sat_conversion,[],[f44691]) ).
cnf(s477,plain,
( ~ spl4242_2
| spl4242_441 ),
inference(sat_conversion,[],[f44930]) ).
cnf(s488,plain,
( spl4242_1
| ~ spl4242_267 ),
inference(sat_conversion,[],[f45484]) ).
cnf(s491,plain,
( spl4242_2
| ~ spl4242_382
| ~ spl4242_388 ),
inference(sat_conversion,[],[f45577]) ).
cnf(s527,plain,
( spl4242_2
| ~ spl4242_379
| ~ spl4242_387 ),
inference(sat_conversion,[],[f46489]) ).
cnf(s529,plain,
( spl4242_2
| ~ spl4242_384
| ~ spl4242_388 ),
inference(sat_conversion,[],[f46610]) ).
cnf(s533,plain,
( spl4242_267
| ~ spl4242_441 ),
inference(sat_conversion,[],[f47115]) ).
cnf(s537,plain,
~ spl4242_380,
inference(rat,[],[s443,s199]) ).
cnf(s539,plain,
spl4242_379,
inference(rat,[],[s391,s537]) ).
cnf(s546,plain,
( ~ spl4242_388
| spl4242_2 ),
inference(rat,[],[s466,s392,s397,s491,s529,s199]) ).
cnf(s547,plain,
spl4242_2,
inference(rat,[],[s546,s396,s527,s539]) ).
cnf(s548,plain,
spl4242_441,
inference(rat,[],[s477,s547]) ).
cnf(s551,plain,
~ spl4242_1,
inference(rat,[],[s1,s547]) ).
cnf(s552,plain,
spl4242_267,
inference(rat,[],[s533,s548]) ).
cnf(s561,plain,
$false,
inference(rat,[],[s488,s552,s551]) ).
fof(f47116,plain,
$false,
inference(avatar_sat_refutation,[],[s561]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO468+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 08:17:40 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 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
% 21.90/5.96 % (195176)Detected formulas, will run a generic FOF schedule.
% 21.90/5.96 % (195184)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2153921634:i=109:sd=1:ins=1:gsp=on:ss=axioms_2981 on theBenchmark for (2981ds/109Mi)
% 21.90/5.96 % (195181)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=3480546765:i=141193_2981 on theBenchmark for (2981ds/141193Mi)
% 21.90/5.96 % (195182)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=141248231:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2981 on theBenchmark for (2981ds/134677Mi)
% 21.90/5.96 % (195183)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=364988663:i=141695:sd=1:nm=32:gsp=on:ss=included_2981 on theBenchmark for (2981ds/141695Mi)
% 21.90/5.96 % (195186)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2113882518:s2a=on:i=139:gtg=position_2981 on theBenchmark for (2981ds/139Mi)
% 21.90/5.96 % (195185)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3716737634:i=119:av=off:ss=axioms_2981 on theBenchmark for (2981ds/119Mi)
% 21.90/5.96 % (195187)dis-21_1_sil=8000:lcm=predicate:random_seed=1397694757:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2981 on theBenchmark for (2981ds/129Mi)
% 21.90/5.96 % (195184)Instruction limit reached!
% 21.90/5.96 % (195184)------------------------------
% 21.90/5.96 % (195184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.90/5.96 % (195184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.90/5.96 % (195184)CaDiCaL version: 2.1.3
% 21.90/5.96 % (195184)Termination reason: Instruction limit
% 21.90/5.96 % (195184)Termination phase: Preprocessing 3
% 21.90/5.96 % (195184)Time elapsed: 0.093 s
% 21.90/5.96 % (195184)Peak memory usage: 92 MB
% 21.90/5.96 % (195184)Instructions burned: 110 (million)
% 21.90/5.96 % (195186)Instruction limit reached!
% 21.90/5.96 % (195186)------------------------------
% 21.90/5.96 % (195186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.90/5.96 % (195186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.90/5.96 % (195186)CaDiCaL version: 2.1.3
% 21.90/5.96 % (195186)Termination reason: Instruction limit
% 21.90/5.96 % (195186)Termination phase: Property scanning
% 21.90/5.96 % (195186)Time elapsed: 0.104 s
% 21.90/5.96 % (195186)Peak memory usage: 90 MB
% 21.90/5.96 % (195186)Instructions burned: 140 (million)
% 21.90/5.96 % (195185)Instruction limit reached!
% 21.90/5.96 % (195185)------------------------------
% 21.90/5.96 % (195185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.90/5.96 % (195185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.90/5.96 % (195185)CaDiCaL version: 2.1.3
% 21.90/5.96 % (195185)Termination reason: Instruction limit
% 21.90/5.96 % (195185)Termination phase: Preprocessing 1
% 21.90/5.96 % (195185)Time elapsed: 0.106 s
% 21.90/5.96 % (195185)Peak memory usage: 90 MB
% 21.90/5.96 % (195185)Instructions burned: 120 (million)
% 21.90/5.96 % (195187)Instruction limit reached!
% 21.90/5.96 % (195187)------------------------------
% 21.90/5.96 % (195187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.90/5.96 % (195187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.90/5.96 % (195187)CaDiCaL version: 2.1.3
% 21.90/5.96 % (195187)Termination reason: Instruction limit
% 21.90/5.96 % (195187)Termination phase: SInE selection
% 21.90/5.96 % (195187)Time elapsed: 0.102 s
% 21.90/5.96 % (195187)Peak memory usage: 90 MB
% 21.90/5.96 % (195187)Instructions burned: 129 (million)
% 21.90/5.96 % (195195)lrs+10_1_sil=8000:sp=occurrence:random_seed=185230392:i=285:sd=3:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/285Mi)
% 21.90/5.96 % (195197)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2436727603:i=325:sd=1:ss=axioms:sgt=32_2977 on theBenchmark for (2977ds/325Mi)
% 21.90/5.96 % (195196)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2333802572:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/157Mi)
% 21.90/5.96 % (195198)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=3638025423:s2a=on:i=248:s2at=1.23:gtg=position_2977 on theBenchmark for (2977ds/248Mi)
% 21.90/5.96 % (195196)Instruction limit reached!
% 21.90/5.96 % (195196)------------------------------
% 34.66/7.68 % (195196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.66/7.68 % (195196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.66/7.68 % (195196)CaDiCaL version: 2.1.3
% 34.66/7.68 % (195196)Termination reason: Instruction limit
% 34.66/7.68 % (195196)Termination phase: Property scanning
% 34.66/7.68 % (195196)Time elapsed: 0.117 s
% 34.66/7.68 % (195196)Peak memory usage: 90 MB
% 34.66/7.68 % (195196)Instructions burned: 157 (million)
% 34.66/7.68 % (195198)Instruction limit reached!
% 34.66/7.68 % (195198)------------------------------
% 34.66/7.68 % (195198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.66/7.68 % (195198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.66/7.68 % (195198)CaDiCaL version: 2.1.3
% 34.66/7.68 % (195198)Termination reason: Instruction limit
% 34.66/7.68 % (195198)Termination phase: Property scanning
% 34.66/7.68 % (195198)Time elapsed: 0.183 s
% 34.66/7.68 % (195198)Peak memory usage: 90 MB
% 34.66/7.68 % (195198)Instructions burned: 248 (million)
% 34.66/7.68 % (195195)Instruction limit reached!
% 34.66/7.68 % (195195)------------------------------
% 34.66/7.68 % (195195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.66/7.68 % (195195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.66/7.68 % (195195)CaDiCaL version: 2.1.3
% 34.66/7.68 % (195195)Termination reason: Instruction limit
% 34.66/7.68 % (195195)Termination phase: Property scanning
% 34.66/7.68 % (195195)Time elapsed: 0.241 s
% 34.66/7.68 % (195195)Peak memory usage: 96 MB
% 34.66/7.68 % (195195)Instructions burned: 286 (million)
% 34.66/7.68 % (195197)Instruction limit reached!
% 34.66/7.68 % (195197)------------------------------
% 34.66/7.68 % (195197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.66/7.68 % (195197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.66/7.68 % (195197)CaDiCaL version: 2.1.3
% 34.66/7.68 % (195197)Termination reason: Instruction limit
% 34.66/7.68 % (195197)Termination phase: Saturation
% 34.66/7.68 % (195197)Time elapsed: 0.288 s
% 34.66/7.68 % (195197)Peak memory usage: 97 MB
% 34.66/7.68 % (195197)Instructions burned: 326 (million)
% 34.66/7.68 % (195203)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=269151601:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 34.66/7.68 % (195204)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4194133155:i=2350_2972 on theBenchmark for (2972ds/2350Mi)
% 34.66/7.68 % (195205)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4210570404:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 34.66/7.68 % (195206)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=35873491:i=127:av=off:fsr=off:sup=off_2971 on theBenchmark for (2971ds/127Mi)
% 34.66/7.68 % (195205)Instruction limit reached!
% 34.66/7.68 % (195205)------------------------------
% 34.66/7.68 % (195205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.66/7.68 % (195205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.66/7.68 % (195205)CaDiCaL version: 2.1.3
% 34.66/7.68 % (195205)Termination reason: Instruction limit
% 34.66/7.68 % (195205)Termination phase: Preprocessing 1
% 34.66/7.68 % (195205)Time elapsed: 0.097 s
% 34.66/7.68 % (195205)Peak memory usage: 91 MB
% 34.66/7.68 % (195205)Instructions burned: 113 (million)
% 34.66/7.68 % (195203)Instruction limit reached!
% 34.66/7.68 % (195203)------------------------------
% 34.66/7.68 % (195203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.66/7.68 % (195203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.66/7.68 % (195203)CaDiCaL version: 2.1.3
% 34.66/7.68 % (195203)Termination reason: Instruction limit
% 34.66/7.68 % (195203)Termination phase: Preprocessing 3
% 34.66/7.68 % (195203)Time elapsed: 0.248 s
% 34.66/7.68 % (195203)Peak memory usage: 95 MB
% 34.66/7.68 % (195203)Instructions burned: 294 (million)
% 34.66/7.68 % (195206)Instruction limit reached!
% 34.66/7.68 % (195206)------------------------------
% 34.66/7.68 % (195206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.66/7.68 % (195206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.66/7.68 % (195206)CaDiCaL version: 2.1.3
% 34.66/7.68 % (195206)Termination reason: Instruction limit
% 34.66/7.68 % (195206)Termination phase: Naming
% 34.66/7.68 % (195206)Time elapsed: 0.117 s
% 34.66/7.68 % (195206)Peak memory usage: 94 MB
% 81.87/14.37 % (195206)Instructions burned: 127 (million)
% 81.87/14.37 % (195211)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4092907844:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2968 on theBenchmark for (2968ds/114Mi)
% 81.87/14.37 % (195212)lrs+10_1_sil=8000:sp=occurrence:random_seed=2386514481:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2968 on theBenchmark for (2968ds/907Mi)
% 81.87/14.37 % (195213)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3054464941:i=437:sd=1:aac=none:ss=included_2967 on theBenchmark for (2967ds/437Mi)
% 81.87/14.37 % (195211)Instruction limit reached!
% 81.87/14.37 % (195211)------------------------------
% 81.87/14.37 % (195211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.87/14.37 % (195211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.87/14.37 % (195211)CaDiCaL version: 2.1.3
% 81.87/14.37 % (195211)Termination reason: Instruction limit
% 81.87/14.37 % (195211)Termination phase: Property scanning
% 81.87/14.37 % (195211)Time elapsed: 0.085 s
% 81.87/14.37 % (195211)Peak memory usage: 90 MB
% 81.87/14.37 % (195211)Instructions burned: 114 (million)
% 81.87/14.37 % (195217)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=129622790:i=5202:ss=axioms:sgt=16_2964 on theBenchmark for (2964ds/5202Mi)
% 81.87/14.37 % (195213)Instruction limit reached!
% 81.87/14.37 % (195213)------------------------------
% 81.87/14.37 % (195213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.87/14.37 % (195213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.87/14.37 % (195213)CaDiCaL version: 2.1.3
% 81.87/14.37 % (195213)Termination reason: Instruction limit
% 81.87/14.37 % (195213)Termination phase: Property scanning
% 81.87/14.37 % (195213)Time elapsed: 0.366 s
% 81.87/14.37 % (195213)Peak memory usage: 100 MB
% 81.87/14.37 % (195213)Instructions burned: 437 (million)
% 81.87/14.37 % (195212)Instruction limit reached!
% 81.87/14.37 % (195212)------------------------------
% 81.87/14.37 % (195212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.87/14.37 % (195212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.87/14.37 % (195212)CaDiCaL version: 2.1.3
% 81.87/14.37 % (195212)Termination reason: Instruction limit
% 81.87/14.37 % (195212)Termination phase: Property scanning
% 81.87/14.37 % (195212)Time elapsed: 0.697 s
% 81.87/14.37 % (195212)Peak memory usage: 99 MB
% 81.87/14.37 % (195212)Instructions burned: 908 (million)
% 81.87/14.37 % (195219)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1999568089:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2961 on theBenchmark for (2961ds/134Mi)
% 81.87/14.37 % (195219)Instruction limit reached!
% 81.87/14.37 % (195219)------------------------------
% 81.87/14.37 % (195219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.87/14.37 % (195219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.87/14.37 % (195219)CaDiCaL version: 2.1.3
% 81.87/14.37 % (195219)Termination reason: Instruction limit
% 81.87/14.37 % (195219)Termination phase: Preprocessing 1
% 81.87/14.37 % (195219)Time elapsed: 0.118 s
% 81.87/14.37 % (195219)Peak memory usage: 91 MB
% 81.87/14.37 % (195219)Instructions burned: 134 (million)
% 81.87/14.37 % (195220)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=735478063:st=8:i=592:sd=3:ep=RST:ss=axioms_2958 on theBenchmark for (2958ds/592Mi)
% 81.87/14.37 % (195222)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3507842799:st=3:i=13193:sd=3:ss=axioms_2956 on theBenchmark for (2956ds/13193Mi)
% 81.87/14.37 % (195220)Instruction limit reached!
% 81.87/14.37 % (195220)------------------------------
% 81.87/14.37 % (195220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.87/14.37 % (195220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.87/14.37 % (195220)CaDiCaL version: 2.1.3
% 81.87/14.37 % (195220)Termination reason: Instruction limit
% 81.87/14.37 % (195220)Termination phase: Preprocessing 3
% 81.87/14.37 % (195220)Time elapsed: 0.274 s
% 81.87/14.37 % (195220)Peak memory usage: 102 MB
% 81.87/14.37 % (195220)Instructions burned: 595 (million)
% 81.87/14.37 % (195204)Instruction limit reached!
% 81.87/14.37 % (195204)------------------------------
% 81.87/14.37 % (195204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.87/14.37 % (195204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.87/14.37 % (195204)CaDiCaL version: 2.1.3
% 81.87/14.37 % (195204)Termination reason: Instruction limit
% 106.89/18.02 % (195204)Termination phase: Twee Goal Transformation
% 106.89/18.02 % (195204)Time elapsed: 1.744 s
% 106.89/18.02 % (195204)Peak memory usage: 105 MB
% 106.89/18.02 % (195204)Instructions burned: 2350 (million)
% 106.89/18.02 % (195225)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2654657630:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2952 on theBenchmark for (2952ds/125Mi)
% 106.89/18.02 % (195225)Instruction limit reached!
% 106.89/18.02 % (195225)------------------------------
% 106.89/18.02 % (195225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.89/18.02 % (195225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.89/18.02 % (195225)CaDiCaL version: 2.1.3
% 106.89/18.02 % (195225)Termination reason: Instruction limit
% 106.89/18.02 % (195225)Termination phase: Property scanning
% 106.89/18.02 % (195225)Time elapsed: 0.049 s
% 106.89/18.02 % (195225)Peak memory usage: 90 MB
% 106.89/18.02 % (195225)Instructions burned: 128 (million)
% 106.89/18.02 % (195226)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1612127410:i=134:gtgl=5:slsql=off:gtg=exists_sym_2952 on theBenchmark for (2952ds/134Mi)
% 106.89/18.02 % (195226)Instruction limit reached!
% 106.89/18.02 % (195226)------------------------------
% 106.89/18.02 % (195226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.89/18.02 % (195226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.89/18.02 % (195226)CaDiCaL version: 2.1.3
% 106.89/18.02 % (195226)Termination reason: Instruction limit
% 106.89/18.02 % (195226)Termination phase: Property scanning
% 106.89/18.02 % (195226)Time elapsed: 0.101 s
% 106.89/18.02 % (195226)Peak memory usage: 90 MB
% 106.89/18.02 % (195226)Instructions burned: 135 (million)
% 106.89/18.02 % (195228)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1833658431:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2950 on theBenchmark for (2950ds/141Mi)
% 106.89/18.02 % (195228)Instruction limit reached!
% 106.89/18.02 % (195228)------------------------------
% 106.89/18.02 % (195228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.89/18.02 % (195228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.89/18.02 % (195228)CaDiCaL version: 2.1.3
% 106.89/18.02 % (195228)Termination reason: Instruction limit
% 106.89/18.02 % (195228)Termination phase: Property scanning
% 106.89/18.02 % (195228)Time elapsed: 0.064 s
% 106.89/18.02 % (195228)Peak memory usage: 92 MB
% 106.89/18.02 % (195228)Instructions burned: 143 (million)
% 106.89/18.02 % (195230)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1255633448:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2948 on theBenchmark for (2948ds/431Mi)
% 106.89/18.02 % (195232)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=424934708:i=6060:aac=none:ins=25_2946 on theBenchmark for (2946ds/6060Mi)
% 106.89/18.02 % (195230)Instruction limit reached!
% 106.89/18.02 % (195230)------------------------------
% 106.89/18.02 % (195230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.89/18.02 % (195230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.89/18.02 % (195230)CaDiCaL version: 2.1.3
% 106.89/18.02 % (195230)Termination reason: Instruction limit
% 106.89/18.02 % (195230)Termination phase: Saturation
% 106.89/18.02 % (195230)Time elapsed: 0.370 s
% 106.89/18.02 % (195230)Peak memory usage: 96 MB
% 106.89/18.02 % (195230)Instructions burned: 431 (million)
% 106.89/18.02 % (195235)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1683360881:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2941 on theBenchmark for (2941ds/150Mi)
% 106.89/18.02 % (195235)Instruction limit reached!
% 106.89/18.02 % (195235)------------------------------
% 106.89/18.02 % (195235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.89/18.02 % (195235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.89/18.02 % (195235)CaDiCaL version: 2.1.3
% 106.89/18.02 % (195235)Termination reason: Instruction limit
% 106.89/18.02 % (195235)Termination phase: Preprocessing 1
% 106.89/18.02 % (195235)Time elapsed: 0.134 s
% 106.89/18.02 % (195235)Peak memory usage: 91 MB
% 106.89/18.02 % (195235)Instructions burned: 150 (million)
% 106.89/18.02 % (195237)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1512308503:i=14155:bd=all_2937 on theBenchmark for (2937ds/14155Mi)
% 96.66/18.65 % (195217)Instruction limit reached!
% 96.66/18.65 % (195217)------------------------------
% 96.66/18.65 % (195217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.66/18.65 % (195217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.66/18.65 % (195217)CaDiCaL version: 2.1.3
% 96.66/18.65 % (195217)Termination reason: Instruction limit
% 96.66/18.65 % (195217)Termination phase: Saturation
% 96.66/18.65 % (195217)Time elapsed: 4.819 s
% 96.66/18.65 % (195217)Peak memory usage: 255 MB
% 96.66/18.65 % (195217)Instructions burned: 5202 (million)
% 96.66/18.65 % (195239)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1743782276:i=667:av=off:fsr=off_2913 on theBenchmark for (2913ds/667Mi)
% 96.66/18.65 % (195239)Instruction limit reached!
% 96.66/18.65 % (195239)------------------------------
% 96.66/18.65 % (195239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.66/18.65 % (195239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.66/18.65 % (195239)CaDiCaL version: 2.1.3
% 96.66/18.65 % (195239)Termination reason: Instruction limit
% 96.66/18.65 % (195239)Termination phase: Property scanning
% 96.66/18.65 % (195239)Time elapsed: 0.181 s
% 96.66/18.65 % (195239)Peak memory usage: 102 MB
% 96.66/18.65 % (195239)Instructions burned: 680 (million)
% 96.66/18.65 % (195241)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=11101429:s2a=on:i=185:s2at=1.8:fdi=4_2909 on theBenchmark for (2909ds/185Mi)
% 96.66/18.65 % (195241)Instruction limit reached!
% 96.66/18.65 % (195241)------------------------------
% 96.66/18.65 % (195241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.66/18.65 % (195241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.66/18.65 % (195241)CaDiCaL version: 2.1.3
% 96.66/18.65 % (195241)Termination reason: Instruction limit
% 96.66/18.65 % (195241)Termination phase: Preprocessing 1
% 96.66/18.65 % (195241)Time elapsed: 0.053 s
% 96.66/18.65 % (195241)Peak memory usage: 91 MB
% 96.66/18.65 % (195241)Instructions burned: 188 (million)
% 96.66/18.65 % (195243)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=716377070:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2907 on theBenchmark for (2907ds/193Mi)
% 96.66/18.65 % (195243)Instruction limit reached!
% 96.66/18.65 % (195243)------------------------------
% 96.66/18.65 % (195243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.66/18.65 % (195243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.66/18.65 % (195243)CaDiCaL version: 2.1.3
% 96.66/18.65 % (195243)Termination reason: Instruction limit
% 96.66/18.65 % (195243)Termination phase: Preprocessing 1
% 96.66/18.65 % (195243)Time elapsed: 0.061 s
% 96.66/18.65 % (195243)Peak memory usage: 91 MB
% 96.66/18.65 % (195243)Instructions burned: 207 (million)
% 96.66/18.65 % (195245)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3410679719:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2905 on theBenchmark for (2905ds/4850Mi)
% 96.66/18.65 % (195232)Instruction limit reached!
% 96.66/18.65 % (195232)------------------------------
% 96.66/18.65 % (195232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.66/18.65 % (195232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.66/18.65 % (195232)CaDiCaL version: 2.1.3
% 96.66/18.65 % (195232)Termination reason: Instruction limit
% 96.66/18.65 % (195232)Termination phase: Saturation
% 96.66/18.65 % (195232)Time elapsed: 5.649 s
% 96.66/18.65 % (195232)Peak memory usage: 433 MB
% 96.66/18.65 % (195232)Instructions burned: 6061 (million)
% 96.66/18.65 % (195247)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4277394955:i=12111:sd=1:ss=included_2886 on theBenchmark for (2886ds/12111Mi)
% 96.66/18.65 % (195245)Instruction limit reached!
% 96.66/18.65 % (195245)------------------------------
% 96.66/18.65 % (195245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.66/18.65 % (195245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.66/18.65 % (195245)CaDiCaL version: 2.1.3
% 96.66/18.65 % (195245)Termination reason: Instruction limit
% 96.66/18.65 % (195245)Termination phase: Saturation
% 96.66/18.65 % (195245)Time elapsed: 3.500 s
% 96.66/18.65 % (195245)Peak memory usage: 131 MB
% 96.66/18.65 % (195245)Instructions burned: 4850 (million)
% 96.66/18.65 % (195249)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=222835429:i=319:kws=precedence:fsr=off_2868 on theBenchmark for (2868ds/319Mi)
% 96.66/18.65 % (195249)Instruction limit reached!
% 96.66/18.65 % (195249)------------------------------
% 96.66/18.65 % (195249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.66/18.65 % (195249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.66/18.65 % (195249)CaDiCaL version: 2.1.3
% 96.66/18.65 % (195249)Termination reason: Instruction limit
% 96.66/18.65 % (195249)Termination phase: Preprocessing 3
% 96.66/18.65 % (195249)Time elapsed: 0.163 s
% 96.66/18.65 % (195249)Peak memory usage: 99 MB
% 96.66/18.65 % (195249)Instructions burned: 321 (million)
% 96.66/18.65 % (195251)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1182305954:i=2064:ep=RST_2865 on theBenchmark for (2865ds/2064Mi)
% 96.66/18.65 % (195251)Instruction limit reached!
% 96.66/18.65 % (195251)------------------------------
% 96.66/18.65 % (195251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.66/18.65 % (195251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.66/18.65 % (195251)CaDiCaL version: 2.1.3
% 96.66/18.65 % (195251)Termination reason: Instruction limit
% 96.66/18.65 % (195251)Termination phase: Property scanning
% 96.66/18.65 % (195251)Time elapsed: 0.773 s
% 96.66/18.65 % (195251)Peak memory usage: 106 MB
% 96.66/18.65 % (195251)Instructions burned: 2067 (million)
% 96.66/18.65 % (195253)dis-1011_128_sil=32000:random_seed=1473347047:i=3706:ep=RST:av=off_2855 on theBenchmark for (2855ds/3706Mi)
% 96.66/18.65 % (195222)Instruction limit reached!
% 96.66/18.65 % (195222)------------------------------
% 96.66/18.65 % (195222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.66/18.65 % (195222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.66/18.65 % (195222)CaDiCaL version: 2.1.3
% 96.66/18.65 % (195222)Termination reason: Instruction limit
% 96.66/18.65 % (195222)Termination phase: Saturation
% 96.66/18.65 % (195222)Time elapsed: 10.432 s
% 96.66/18.65 % (195222)Peak memory usage: 357 MB
% 96.66/18.65 % (195222)Instructions burned: 13194 (million)
% 96.66/18.65 % (195255)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1236617284:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2849 on theBenchmark for (2849ds/757Mi)
% 96.66/18.65 % (195255)Instruction limit reached!
% 96.66/18.65 % (195255)------------------------------
% 96.66/18.65 % (195255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.66/18.65 % (195255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.66/18.65 % (195255)CaDiCaL version: 2.1.3
% 96.66/18.65 % (195255)Termination reason: Instruction limit
% 96.66/18.65 % (195255)Termination phase: Saturation
% 96.66/18.65 % (195255)Time elapsed: 0.322 s
% 96.66/18.65 % (195255)Peak memory usage: 98 MB
% 96.66/18.65 % (195255)Instructions burned: 759 (million)
% 96.66/18.65 % (195257)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3682369885:i=13913:ss=axioms:sgt=8_2844 on theBenchmark for (2844ds/13913Mi)
% 96.66/18.65 % (195253)Instruction limit reached!
% 96.66/18.65 % (195253)------------------------------
% 96.66/18.65 % (195253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.66/18.65 % (195253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.66/18.65 % (195253)CaDiCaL version: 2.1.3
% 96.66/18.65 % (195253)Termination reason: Instruction limit
% 96.66/18.65 % (195253)Termination phase: Saturation
% 96.66/18.65 % (195253)Time elapsed: 1.555 s
% 96.66/18.65 % (195253)Peak memory usage: 116 MB
% 96.66/18.65 % (195253)Instructions burned: 3708 (million)
% 96.66/18.65 % (195259)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1498534941:i=9925:aac=none_2838 on theBenchmark for (2838ds/9925Mi)
% 96.66/18.65 % (195237)Instruction limit reached!
% 96.66/18.65 % (195237)------------------------------
% 96.66/18.65 % (195237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.66/18.65 % (195237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.66/18.65 % (195237)CaDiCaL version: 2.1.3
% 96.66/18.65 % (195237)Termination reason: Instruction limit
% 96.66/18.65 % (195237)Termination phase: Saturation
% 96.66/18.65 % (195237)Time elapsed: 10.151 s
% 96.66/18.65 % (195237)Peak memory usage: 404 MB
% 96.66/18.65 % (195237)Instructions burned: 14156 (million)
% 96.66/18.65 % (195261)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2977706253:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2833 on theBenchmark for (2833ds/2479Mi)
% 96.66/18.65 % (195181)First to succeed.
% 96.66/18.65 % (195181)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-195176"
% 96.66/18.65 % (195181)Refutation found. Thanks to Tanya!
% 96.66/18.65 % SZS status Theorem for theBenchmark
% 96.66/18.65 % SZS output start Proof for theBenchmark
% See solution above
% 112.85/18.89 % (195181)------------------------------
% 112.85/18.89 % (195181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.85/18.89 % (195181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.85/18.89 % (195181)CaDiCaL version: 2.1.3
% 112.85/18.89 % (195181)Termination reason: Refutation
% 112.85/18.89 % (195181)Time elapsed: 14.985 s
% 112.85/18.89 % (195181)Peak memory usage: 382 MB
% 112.85/18.89 % (195181)Instructions burned: 20834 (million)
% 112.85/18.89 % (195181)------------------------------
% 112.85/18.89 % (195181)------------------------------
% 112.85/18.89 % (195176)Success in time 17.45 s
% 112.85/18.89 % Vampire exiting
%------------------------------------------------------------------------------