%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW937+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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 01:38:03 PM UTC 2026
% Result : Theorem 6.05s 1.81s
% Output : Refutation 8.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 33
% Syntax : Number of formulae : 197 ( 34 unt; 24 def)
% Number of atoms : 660 ( 59 equ)
% Maximal formula atoms : 30 ( 3 avg)
% Number of connectives : 802 ( 339 ~; 321 |; 93 &)
% ( 42 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 27 ( 25 usr; 25 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 8 con; 0-4 aty)
% Number of variables : 172 ( 0 sgn 155 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
~ p__01(s__02(cbool__00,cF__00)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','HL_FALSITY') ).
fof(f5,axiom,
p__01(s__02(cbool__00,cT__00)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.bool.TRUTH') ).
fof(f7,axiom,
! [X0] :
( ( ( p__01(s__02(cbool__00,cT__00))
=> p__01(s__02(cbool__00,X0)) )
<=> p__01(s__02(cbool__00,X0)) )
& ( ( p__01(s__02(cbool__00,X0))
=> p__01(s__02(cbool__00,cT__00)) )
<=> p__01(s__02(cbool__00,cT__00)) )
& ( ( p__01(s__02(cbool__00,cF__00))
=> p__01(s__02(cbool__00,X0)) )
<=> p__01(s__02(cbool__00,cT__00)) )
& ( ( p__01(s__02(cbool__00,X0))
=> p__01(s__02(cbool__00,X0)) )
<=> p__01(s__02(cbool__00,cT__00)) )
& ( ( p__01(s__02(cbool__00,X0))
=> p__01(s__02(cbool__00,cF__00)) )
<=> ~ p__01(s__02(cbool__00,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.bool.IMP_CLAUSES') ).
fof(f11,axiom,
! [X0] :
( ( s__02(cbool__00,cT__00) = s__02(cbool__00,X0)
<=> p__01(s__02(cbool__00,X0)) )
& ( s__02(cbool__00,X0) = s__02(cbool__00,cT__00)
<=> p__01(s__02(cbool__00,X0)) )
& ( s__02(cbool__00,cF__00) = s__02(cbool__00,X0)
<=> ~ p__01(s__02(cbool__00,X0)) )
& ( s__02(cbool__00,X0) = s__02(cbool__00,cF__00)
<=> ~ p__01(s__02(cbool__00,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.bool.EQ_CLAUSES') ).
fof(f25,axiom,
! [X0,X1,X2,X3] :
( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3))))
<=> ( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X3))))
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.pred_set.DISJOINT_UNION') ).
fof(f26,axiom,
! [X0,X1,X2,X3] :
( p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))))))
<=> ( s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))) = s__02(cfun__02(X0,cbool__00),X1)
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.set_sep.SPLIT_def') ).
fof(f27,axiom,
! [X0,X1,X2,X3] :
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3))))
<=> ? [X4,X5] :
( p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X4),s__02(cfun__02(X0,cbool__00),X5))))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(X0,cbool__00),X4))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2),s__02(cfun__02(X0,cbool__00),X5)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.set_sep.STAR_def') ).
fof(f28,axiom,
! [X0,X1,X2,X3,X4] :
( p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(cfun__02(X0,cbool__00),X4))))))))
<=> ( s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))),s__02(cfun__02(X0,cbool__00),X4))) = s__02(cfun__02(X0,cbool__00),X1)
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))))
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(cfun__02(X0,cbool__00),X4))))
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X4)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm.cfHeapsBase.SPLIT3_def') ).
fof(f29,conjecture,
! [X0,X1,X2,X3,X4] :
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X3))),s__02(cfun__02(X0,cbool__00),X4))))
=> ? [X5,X6,X7] :
( p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(X0,cbool__00),X4),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X5),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X6),s__02(cfun__02(X0,cbool__00),X7))))))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(X0,cbool__00),X5))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2),s__02(cfun__02(X0,cbool__00),X6))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X3),s__02(cfun__02(X0,cbool__00),X7)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture) ).
fof(f30,negated_conjecture,
~ ! [X0,X1,X2,X3,X4] :
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X3))),s__02(cfun__02(X0,cbool__00),X4))))
=> ? [X5,X6,X7] :
( p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(X0,cbool__00),X4),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X5),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X6),s__02(cfun__02(X0,cbool__00),X7))))))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(X0,cbool__00),X5))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2),s__02(cfun__02(X0,cbool__00),X6))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X3),s__02(cfun__02(X0,cbool__00),X7)))) ) ),
inference(negated_conjecture,[status(cth)],[f29]) ).
fof(f34,plain,
! [X0] :
( ( ( p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,cT__00)) )
<=> p__01(s__02(cbool__00,X0)) )
& ( ( p__01(s__02(cbool__00,cT__00))
| ~ p__01(s__02(cbool__00,X0)) )
<=> p__01(s__02(cbool__00,cT__00)) )
& ( ( p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,cF__00)) )
<=> p__01(s__02(cbool__00,cT__00)) )
& ( ( p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,X0)) )
<=> p__01(s__02(cbool__00,cT__00)) )
& ( ( p__01(s__02(cbool__00,cF__00))
| ~ p__01(s__02(cbool__00,X0)) )
<=> ~ p__01(s__02(cbool__00,X0)) ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f51,plain,
? [X0,X1,X2,X3,X4] :
( ! [X5,X6,X7] :
( ~ p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(X0,cbool__00),X4),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X5),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X6),s__02(cfun__02(X0,cbool__00),X7))))))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(X0,cbool__00),X5))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2),s__02(cfun__02(X0,cbool__00),X6))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X3),s__02(cfun__02(X0,cbool__00),X7)))) )
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X3))),s__02(cfun__02(X0,cbool__00),X4)))) ),
inference(ennf_transformation,[],[f30]) ).
fof(f60,plain,
! [X0] :
( ( p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,cT__00))
| ~ p__01(s__02(cbool__00,X0)) )
& ( p__01(s__02(cbool__00,X0))
| ( ~ p__01(s__02(cbool__00,X0))
& p__01(s__02(cbool__00,cT__00)) ) )
& ( p__01(s__02(cbool__00,cT__00))
| ~ p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,cT__00)) )
& ( p__01(s__02(cbool__00,cT__00))
| ( ~ p__01(s__02(cbool__00,cT__00))
& p__01(s__02(cbool__00,X0)) ) )
& ( p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,cF__00))
| ~ p__01(s__02(cbool__00,cT__00)) )
& ( p__01(s__02(cbool__00,cT__00))
| ( ~ p__01(s__02(cbool__00,X0))
& p__01(s__02(cbool__00,cF__00)) ) )
& ( p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,cT__00)) )
& ( p__01(s__02(cbool__00,cT__00))
| ( ~ p__01(s__02(cbool__00,X0))
& p__01(s__02(cbool__00,X0)) ) )
& ( p__01(s__02(cbool__00,cF__00))
| ~ p__01(s__02(cbool__00,X0))
| p__01(s__02(cbool__00,X0)) )
& ( ~ p__01(s__02(cbool__00,X0))
| ( ~ p__01(s__02(cbool__00,cF__00))
& p__01(s__02(cbool__00,X0)) ) ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f61,plain,
! [X0] :
( ( p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,cT__00))
| ~ p__01(s__02(cbool__00,X0)) )
& ( p__01(s__02(cbool__00,X0))
| ( ~ p__01(s__02(cbool__00,X0))
& p__01(s__02(cbool__00,cT__00)) ) )
& ( p__01(s__02(cbool__00,cT__00))
| ~ p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,cT__00)) )
& ( p__01(s__02(cbool__00,cT__00))
| ( ~ p__01(s__02(cbool__00,cT__00))
& p__01(s__02(cbool__00,X0)) ) )
& ( p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,cF__00))
| ~ p__01(s__02(cbool__00,cT__00)) )
& ( p__01(s__02(cbool__00,cT__00))
| ( ~ p__01(s__02(cbool__00,X0))
& p__01(s__02(cbool__00,cF__00)) ) )
& ( p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,X0))
| ~ p__01(s__02(cbool__00,cT__00)) )
& ( p__01(s__02(cbool__00,cT__00))
| ( ~ p__01(s__02(cbool__00,X0))
& p__01(s__02(cbool__00,X0)) ) )
& ( p__01(s__02(cbool__00,cF__00))
| ~ p__01(s__02(cbool__00,X0))
| p__01(s__02(cbool__00,X0)) )
& ( ~ p__01(s__02(cbool__00,X0))
| ( ~ p__01(s__02(cbool__00,cF__00))
& p__01(s__02(cbool__00,X0)) ) ) ),
inference(flattening,[],[f60]) ).
fof(f65,plain,
! [X0] :
( ( s__02(cbool__00,cT__00) = s__02(cbool__00,X0)
| ~ p__01(s__02(cbool__00,X0)) )
& ( p__01(s__02(cbool__00,X0))
| s__02(cbool__00,cT__00) != s__02(cbool__00,X0) )
& ( s__02(cbool__00,X0) = s__02(cbool__00,cT__00)
| ~ p__01(s__02(cbool__00,X0)) )
& ( p__01(s__02(cbool__00,X0))
| s__02(cbool__00,cT__00) != s__02(cbool__00,X0) )
& ( s__02(cbool__00,cF__00) = s__02(cbool__00,X0)
| p__01(s__02(cbool__00,X0)) )
& ( ~ p__01(s__02(cbool__00,X0))
| s__02(cbool__00,cF__00) != s__02(cbool__00,X0) )
& ( s__02(cbool__00,X0) = s__02(cbool__00,cF__00)
| p__01(s__02(cbool__00,X0)) )
& ( ~ p__01(s__02(cbool__00,X0))
| s__02(cbool__00,cF__00) != s__02(cbool__00,X0) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f66,plain,
! [X0] :
( ( s__02(cbool__00,cT__00) = s__02(cbool__00,X0)
| ~ p__01(s__02(cbool__00,X0)) )
& ( p__01(s__02(cbool__00,X0))
| s__02(cbool__00,cT__00) != s__02(cbool__00,X0) )
& ( s__02(cbool__00,X0) = s__02(cbool__00,cT__00)
| ~ p__01(s__02(cbool__00,X0)) )
& ( p__01(s__02(cbool__00,X0))
| s__02(cbool__00,cT__00) != s__02(cbool__00,X0) )
& ( s__02(cbool__00,cF__00) = s__02(cbool__00,X0)
| p__01(s__02(cbool__00,X0)) )
& ( ~ p__01(s__02(cbool__00,X0))
| s__02(cbool__00,cF__00) != s__02(cbool__00,X0) )
& ( s__02(cbool__00,X0) = s__02(cbool__00,cF__00)
| p__01(s__02(cbool__00,X0)) )
& ( ~ p__01(s__02(cbool__00,X0))
| s__02(cbool__00,cF__00) != s__02(cbool__00,X0) ) ),
inference(flattening,[],[f65]) ).
fof(f94,plain,
! [X0,X1,X2,X3] :
( ( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X3))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))) )
& ( ( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X3))))
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))) )
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3)))) ) ),
inference(nnf_transformation,[],[f25]) ).
fof(f95,plain,
! [X0,X1,X2,X3] :
( ( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X3))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))) )
& ( ( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X3))))
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))) )
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3)))) ) ),
inference(flattening,[],[f94]) ).
fof(f96,plain,
! [X0,X1,X2,X3] :
( ( p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))))))
| s__02(cfun__02(X0,cbool__00),X1) != s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))) )
& ( ( s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))) = s__02(cfun__02(X0,cbool__00),X1)
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))) )
| ~ p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))))) ) ),
inference(nnf_transformation,[],[f26]) ).
fof(f97,plain,
! [X0,X1,X2,X3] :
( ( p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))))))
| s__02(cfun__02(X0,cbool__00),X1) != s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))) )
& ( ( s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))) = s__02(cfun__02(X0,cbool__00),X1)
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))) )
| ~ p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))))) ) ),
inference(flattening,[],[f96]) ).
fof(f98,plain,
! [X0,X1,X2,X3] :
( ( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3))))
| ! [X4,X5] :
( ~ p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X4),s__02(cfun__02(X0,cbool__00),X5))))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(X0,cbool__00),X4))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2),s__02(cfun__02(X0,cbool__00),X5)))) ) )
& ( ? [X4,X5] :
( p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X4),s__02(cfun__02(X0,cbool__00),X5))))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(X0,cbool__00),X4))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2),s__02(cfun__02(X0,cbool__00),X5)))) )
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3)))) ) ),
inference(nnf_transformation,[],[f27]) ).
fof(f99,plain,
! [X0,X1,X2,X3] :
( ( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3))))
| ! [X4,X5] :
( ~ p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X4),s__02(cfun__02(X0,cbool__00),X5))))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(X0,cbool__00),X4))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2),s__02(cfun__02(X0,cbool__00),X5)))) ) )
& ( ? [X6,X7] :
( p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X6),s__02(cfun__02(X0,cbool__00),X7))))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(X0,cbool__00),X6))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2),s__02(cfun__02(X0,cbool__00),X7)))) )
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3)))) ) ),
inference(rectify,[],[f98]) ).
fof(f100,plain,
! [X0,X1,X2,X3] :
( ( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3))))
| ! [X4,X5] :
( ~ p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X4),s__02(cfun__02(X0,cbool__00),X5))))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(X0,cbool__00),X4))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2),s__02(cfun__02(X0,cbool__00),X5)))) ) )
& ( ( p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),sK5(X0,X1,X2,X3)),s__02(cfun__02(X0,cbool__00),sK6(X0,X1,X2,X3)))))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(X0,cbool__00),sK5(X0,X1,X2,X3)))))
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2),s__02(cfun__02(X0,cbool__00),sK6(X0,X1,X2,X3))))) )
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6]),skolemize(X6,sK5(X0,X1,X2,X3)),skolemize(X7,sK6(X0,X1,X2,X3))],[f99]) ).
fof(f101,plain,
! [X0,X1,X2,X3,X4] :
( ( p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(cfun__02(X0,cbool__00),X4))))))))
| s__02(cfun__02(X0,cbool__00),X1) != s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))),s__02(cfun__02(X0,cbool__00),X4)))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(cfun__02(X0,cbool__00),X4))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X4)))) )
& ( ( s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))),s__02(cfun__02(X0,cbool__00),X4))) = s__02(cfun__02(X0,cbool__00),X1)
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))))
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(cfun__02(X0,cbool__00),X4))))
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X4)))) )
| ~ p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(cfun__02(X0,cbool__00),X4)))))))) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f102,plain,
! [X0,X1,X2,X3,X4] :
( ( p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(cfun__02(X0,cbool__00),X4))))))))
| s__02(cfun__02(X0,cbool__00),X1) != s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))),s__02(cfun__02(X0,cbool__00),X4)))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(cfun__02(X0,cbool__00),X4))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X4)))) )
& ( ( s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))),s__02(cfun__02(X0,cbool__00),X4))) = s__02(cfun__02(X0,cbool__00),X1)
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))))
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(cfun__02(X0,cbool__00),X4))))
& p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X4)))) )
| ~ p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(cfun__02(X0,cbool__00),X4)))))))) ) ),
inference(flattening,[],[f101]) ).
fof(f103,plain,
( ! [X5,X6,X7] :
( ~ p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X5),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X6),s__02(cfun__02(sK7,cbool__00),X7))))))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),X5))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),X6))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),X7)))) )
& p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9))),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10))),s__02(cfun__02(sK7,cbool__00),sK11)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9,sK10,sK11]),skolemize(X0,sK7),skolemize(X1,sK8),skolemize(X2,sK9),skolemize(X3,sK10),skolemize(X4,sK11)],[f51]) ).
fof(f105,plain,
~ p__01(s__02(cbool__00,cF__00)),
inference(cnf_transformation,[],[f2]) ).
fof(f108,plain,
p__01(s__02(cbool__00,cT__00)),
inference(cnf_transformation,[],[f5]) ).
fof(f120,plain,
! [X0] :
( p__01(s__02(cbool__00,cT__00))
| ~ p__01(s__02(cbool__00,X0)) ),
inference(cnf_transformation,[],[f61]) ).
fof(f140,plain,
! [X0] :
( s__02(cbool__00,cF__00) = s__02(cbool__00,X0)
| p__01(s__02(cbool__00,X0)) ),
inference(cnf_transformation,[],[f66]) ).
fof(f144,plain,
! [X0] :
( s__02(cbool__00,cT__00) = s__02(cbool__00,X0)
| ~ p__01(s__02(cbool__00,X0)) ),
inference(cnf_transformation,[],[f66]) ).
fof(f276,plain,
! [X2,X3,X0,X1] :
( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3)))) ),
inference(cnf_transformation,[],[f95]) ).
fof(f277,plain,
! [X2,X3,X0,X1] :
( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X3))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(cfun__02(X0,cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3)))) ),
inference(cnf_transformation,[],[f95]) ).
fof(f279,plain,
! [X2,X3,X0,X1] :
( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))))
| ~ p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))))) ),
inference(cnf_transformation,[],[f97]) ).
fof(f280,plain,
! [X2,X3,X0,X1] :
( s__02(cfun__02(X0,cbool__00),X1) = s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))
| ~ p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3)))))) ),
inference(cnf_transformation,[],[f97]) ).
fof(f282,plain,
! [X2,X3,X0,X1] :
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2),s__02(cfun__02(X0,cbool__00),sK6(X0,X1,X2,X3)))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3)))) ),
inference(cnf_transformation,[],[f100]) ).
fof(f283,plain,
! [X2,X3,X0,X1] :
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(X0,cbool__00),sK5(X0,X1,X2,X3)))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3)))) ),
inference(cnf_transformation,[],[f100]) ).
fof(f284,plain,
! [X2,X3,X0,X1] :
( p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),sK5(X0,X1,X2,X3)),s__02(cfun__02(X0,cbool__00),sK6(X0,X1,X2,X3)))))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X1),s__02(cfun__02(cfun__02(X0,cbool__00),cbool__00),X2))),s__02(cfun__02(X0,cbool__00),X3)))) ),
inference(cnf_transformation,[],[f100]) ).
fof(f290,plain,
! [X2,X3,X0,X1,X4] :
( p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(X0,cbool__00),X1),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(c_27type_2epair_2eprod_27__02(cfun__02(X0,cbool__00),cfun__02(X0,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(cfun__02(X0,cbool__00),X4))))))))
| s__02(cfun__02(X0,cbool__00),X1) != s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))),s__02(cfun__02(X0,cbool__00),X4)))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X3))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X3),s__02(cfun__02(X0,cbool__00),X4))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(X0,cbool__00),X2),s__02(cfun__02(X0,cbool__00),X4)))) ),
inference(cnf_transformation,[],[f102]) ).
fof(f291,plain,
p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9))),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10))),s__02(cfun__02(sK7,cbool__00),sK11)))),
inference(cnf_transformation,[],[f103]) ).
fof(f292,plain,
! [X6,X7,X5] :
( ~ p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X5),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X6),s__02(cfun__02(sK7,cbool__00),X7))))))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),X5))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),X6))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),X7)))) ),
inference(cnf_transformation,[],[f103]) ).
fof(f433,definition,
( spl66_1
<=> p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9))),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10))),s__02(cfun__02(sK7,cbool__00),sK11)))) ),
introduced(definition,[new_symbols(definition,[spl66_1])],[avatar_definition]) ).
fof(f435,plain,
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9))),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10))),s__02(cfun__02(sK7,cbool__00),sK11))))
| ~ spl66_1 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f436,plain,
spl66_1,
inference(avatar_split_clause,[],[f291,f433]) ).
fof(f438,definition,
( spl66_2
<=> ! [X6,X5,X7] :
( ~ p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X5),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X6),s__02(cfun__02(sK7,cbool__00),X7))))))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),X5))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),X6))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),X7)))) ) ),
introduced(definition,[new_symbols(definition,[spl66_2])],[avatar_definition]) ).
fof(f439,plain,
( ! [X6,X7,X5] :
( ~ p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X5),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X6),s__02(cfun__02(sK7,cbool__00),X7))))))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),X5))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),X6))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),X7)))) )
| ~ spl66_2 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f440,plain,
spl66_2,
inference(avatar_split_clause,[],[f292,f438]) ).
fof(f449,plain,
( ! [X2,X0,X1] :
( ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),X0))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),X1))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),X2))))
| s__02(cbool__00,cF__00) = s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X0),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X1),s__02(cfun__02(sK7,cbool__00),X2))))))) )
| ~ spl66_2 ),
inference(resolution,[],[f439,f140]) ).
fof(f692,plain,
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_1 ),
inference(resolution,[],[f435,f282]) ).
fof(f693,plain,
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9))),s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_1 ),
inference(resolution,[],[f435,f283]) ).
fof(f694,plain,
( p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))))
| ~ spl66_1 ),
inference(resolution,[],[f435,f284]) ).
fof(f834,definition,
( spl66_7
<=> p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9))),s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))) ),
introduced(definition,[new_symbols(definition,[spl66_7])],[avatar_definition]) ).
fof(f836,plain,
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9))),s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_7 ),
inference(avatar_component_clause,[],[f834]) ).
fof(f837,plain,
( spl66_7
| ~ spl66_1 ),
inference(avatar_split_clause,[],[f693,f433,f834]) ).
fof(f838,plain,
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ spl66_7 ),
inference(resolution,[],[f836,f282]) ).
fof(f839,plain,
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ spl66_7 ),
inference(resolution,[],[f836,f283]) ).
fof(f840,plain,
( p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))))
| ~ spl66_7 ),
inference(resolution,[],[f836,f284]) ).
fof(f972,definition,
( spl66_9
<=> p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))) ),
introduced(definition,[new_symbols(definition,[spl66_9])],[avatar_definition]) ).
fof(f974,plain,
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ spl66_9 ),
inference(avatar_component_clause,[],[f972]) ).
fof(f975,plain,
( spl66_9
| ~ spl66_7 ),
inference(avatar_split_clause,[],[f839,f834,f972]) ).
fof(f986,plain,
( s__02(cbool__00,cT__00) = s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_9 ),
inference(resolution,[],[f974,f144]) ).
fof(f1100,definition,
( spl66_10
<=> p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))) ),
introduced(definition,[new_symbols(definition,[spl66_10])],[avatar_definition]) ).
fof(f1102,plain,
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ spl66_10 ),
inference(avatar_component_clause,[],[f1100]) ).
fof(f1103,plain,
( spl66_10
| ~ spl66_7 ),
inference(avatar_split_clause,[],[f838,f834,f1100]) ).
fof(f1114,plain,
( s__02(cbool__00,cT__00) = s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_10 ),
inference(resolution,[],[f1102,f144]) ).
fof(f1228,definition,
( spl66_11
<=> p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))) ),
introduced(definition,[new_symbols(definition,[spl66_11])],[avatar_definition]) ).
fof(f1230,plain,
( p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_11 ),
inference(avatar_component_clause,[],[f1228]) ).
fof(f1231,plain,
( spl66_11
| ~ spl66_1 ),
inference(avatar_split_clause,[],[f692,f433,f1228]) ).
fof(f1242,plain,
( s__02(cbool__00,cT__00) = s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))
| ~ spl66_11 ),
inference(resolution,[],[f1230,f144]) ).
fof(f1397,definition,
( spl66_20
<=> p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))) ),
introduced(definition,[new_symbols(definition,[spl66_20])],[avatar_definition]) ).
fof(f1399,plain,
( p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))))
| ~ spl66_20 ),
inference(avatar_component_clause,[],[f1397]) ).
fof(f1400,plain,
( spl66_20
| ~ spl66_1 ),
inference(avatar_split_clause,[],[f694,f433,f1397]) ).
fof(f1401,plain,
( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_20 ),
inference(resolution,[],[f1399,f279]) ).
fof(f1402,plain,
( s__02(cfun__02(sK7,cbool__00),sK11) = s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))
| ~ spl66_20 ),
inference(resolution,[],[f1399,f280]) ).
fof(f1530,definition,
( spl66_21
<=> p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))) ),
introduced(definition,[new_symbols(definition,[spl66_21])],[avatar_definition]) ).
fof(f1532,plain,
( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_21 ),
inference(avatar_component_clause,[],[f1530]) ).
fof(f1533,plain,
( spl66_21
| ~ spl66_20 ),
inference(avatar_split_clause,[],[f1401,f1397,f1530]) ).
fof(f1548,plain,
( s__02(cbool__00,cT__00) = s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))
| ~ spl66_21 ),
inference(resolution,[],[f1532,f144]) ).
fof(f1666,definition,
( spl66_22
<=> s__02(cfun__02(sK7,cbool__00),sK11) = s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))) ),
introduced(definition,[new_symbols(definition,[spl66_22])],[avatar_definition]) ).
fof(f1668,plain,
( s__02(cfun__02(sK7,cbool__00),sK11) = s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))
| ~ spl66_22 ),
inference(avatar_component_clause,[],[f1666]) ).
fof(f1669,plain,
( spl66_22
| ~ spl66_20 ),
inference(avatar_split_clause,[],[f1402,f1397,f1666]) ).
fof(f1800,definition,
( spl66_25
<=> p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))))) ),
introduced(definition,[new_symbols(definition,[spl66_25])],[avatar_definition]) ).
fof(f1802,plain,
( p__01(s__02(cbool__00,c_27const_2eset__sep_2eSPLIT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))))
| ~ spl66_25 ),
inference(avatar_component_clause,[],[f1800]) ).
fof(f1803,plain,
( spl66_25
| ~ spl66_7 ),
inference(avatar_split_clause,[],[f840,f834,f1800]) ).
fof(f1804,plain,
( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ spl66_25 ),
inference(resolution,[],[f1802,f279]) ).
fof(f1805,plain,
( s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)) = s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_25 ),
inference(resolution,[],[f1802,f280]) ).
fof(f1936,definition,
( spl66_26
<=> s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)) = s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))) ),
introduced(definition,[new_symbols(definition,[spl66_26])],[avatar_definition]) ).
fof(f1938,plain,
( s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)) = s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_26 ),
inference(avatar_component_clause,[],[f1936]) ).
fof(f1939,plain,
( spl66_26
| ~ spl66_25 ),
inference(avatar_split_clause,[],[f1805,f1800,f1936]) ).
fof(f1957,plain,
( ! [X0] :
( ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X0))))
| p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0)))) )
| ~ spl66_26 ),
inference(superposition,[],[f276,f1938]) ).
fof(f1958,plain,
( ! [X0] :
( ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X0))))
| p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0)))) )
| ~ spl66_26 ),
inference(superposition,[],[f277,f1938]) ).
fof(f1963,plain,
( ! [X0,X1] :
( s__02(cfun__02(sK7,cbool__00),X0) != s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X1)))
| p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),X0),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X1))))))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X1))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X1)))) )
| ~ spl66_26 ),
inference(superposition,[],[f290,f1938]) ).
fof(f2057,plain,
( ! [X0,X1] :
( s__02(cfun__02(sK7,cbool__00),X0) != s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X1)))
| p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),X0),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X1))))))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X1))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X1)))) )
| ~ spl66_25
| ~ spl66_26 ),
inference(forward_subsumption_resolution,[],[f1963,f1804]) ).
fof(f5007,definition,
( spl66_68
<=> s__02(cbool__00,cT__00) = s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))) ),
introduced(definition,[new_symbols(definition,[spl66_68])],[avatar_definition]) ).
fof(f5009,plain,
( s__02(cbool__00,cT__00) = s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_68 ),
inference(avatar_component_clause,[],[f5007]) ).
fof(f5010,plain,
( spl66_68
| ~ spl66_9 ),
inference(avatar_split_clause,[],[f986,f972,f5007]) ).
fof(f5012,definition,
( spl66_69
<=> s__02(cbool__00,cT__00) = s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))) ),
introduced(definition,[new_symbols(definition,[spl66_69])],[avatar_definition]) ).
fof(f5014,plain,
( s__02(cbool__00,cT__00) = s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))
| ~ spl66_69 ),
inference(avatar_component_clause,[],[f5012]) ).
fof(f5015,plain,
( spl66_69
| ~ spl66_11 ),
inference(avatar_split_clause,[],[f1242,f1228,f5012]) ).
fof(f5075,definition,
( spl66_70
<=> s__02(cbool__00,cT__00) = s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))) ),
introduced(definition,[new_symbols(definition,[spl66_70])],[avatar_definition]) ).
fof(f5077,plain,
( s__02(cbool__00,cT__00) = s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_70 ),
inference(avatar_component_clause,[],[f5075]) ).
fof(f5078,plain,
( spl66_70
| ~ spl66_10 ),
inference(avatar_split_clause,[],[f1114,f1100,f5075]) ).
fof(f5211,definition,
( spl66_72
<=> p__01(s__02(cbool__00,cT__00)) ),
introduced(definition,[new_symbols(definition,[spl66_72])],[avatar_definition]) ).
fof(f5213,plain,
( p__01(s__02(cbool__00,cT__00))
| ~ spl66_72 ),
inference(avatar_component_clause,[],[f5211]) ).
fof(f5214,plain,
spl66_72,
inference(avatar_split_clause,[],[f108,f5211]) ).
fof(f6094,definition,
( spl66_85
<=> ! [X0,X1] :
( s__02(cfun__02(sK7,cbool__00),X0) != s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X1)))
| p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),X0),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X1))))))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X1))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X1)))) ) ),
introduced(definition,[new_symbols(definition,[spl66_85])],[avatar_definition]) ).
fof(f6095,plain,
( ! [X0,X1] :
( s__02(cfun__02(sK7,cbool__00),X0) != s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X1)))
| p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),X0),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X1))))))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X1))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X1)))) )
| ~ spl66_85 ),
inference(avatar_component_clause,[],[f6094]) ).
fof(f6096,plain,
( spl66_85
| ~ spl66_25
| ~ spl66_26 ),
inference(avatar_split_clause,[],[f2057,f1936,f1800,f6094]) ).
fof(f6126,plain,
( ! [X0] :
( p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X0))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0))))))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0)))) )
| ~ spl66_85 ),
inference(equality_resolution,[],[f6095]) ).
fof(f6128,definition,
( spl66_86
<=> ! [X0] :
( p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X0))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0))))))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0)))) ) ),
introduced(definition,[new_symbols(definition,[spl66_86])],[avatar_definition]) ).
fof(f6129,plain,
( ! [X0] :
( p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),c_27const_2epred__set_2eUNION_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X0))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0))))))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0)))) )
| ~ spl66_86 ),
inference(avatar_component_clause,[],[f6128]) ).
fof(f6130,plain,
( spl66_86
| ~ spl66_85 ),
inference(avatar_split_clause,[],[f6126,f6094,f6128]) ).
fof(f6168,plain,
( p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ spl66_22
| ~ spl66_86 ),
inference(superposition,[],[f6129,f1668]) ).
fof(f6403,definition,
( spl66_96
<=> ! [X2,X0,X1] :
( ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),X0))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),X1))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),X2))))
| s__02(cbool__00,cF__00) = s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X0),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X1),s__02(cfun__02(sK7,cbool__00),X2))))))) ) ),
introduced(definition,[new_symbols(definition,[spl66_96])],[avatar_definition]) ).
fof(f6404,plain,
( ! [X2,X0,X1] :
( s__02(cbool__00,cF__00) = s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X0),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),X1),s__02(cfun__02(sK7,cbool__00),X2)))))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),X1))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),X2))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),X0)))) )
| ~ spl66_96 ),
inference(avatar_component_clause,[],[f6403]) ).
fof(f6405,plain,
( spl66_96
| ~ spl66_2 ),
inference(avatar_split_clause,[],[f449,f438,f6403]) ).
fof(f6944,definition,
( spl66_112
<=> s__02(cbool__00,cT__00) = s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))) ),
introduced(definition,[new_symbols(definition,[spl66_112])],[avatar_definition]) ).
fof(f6946,plain,
( s__02(cbool__00,cT__00) = s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))
| ~ spl66_112 ),
inference(avatar_component_clause,[],[f6944]) ).
fof(f6947,plain,
( spl66_112
| ~ spl66_21 ),
inference(avatar_split_clause,[],[f1548,f1530,f6944]) ).
fof(f7360,definition,
( spl66_116
<=> p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))) ),
introduced(definition,[new_symbols(definition,[spl66_116])],[avatar_definition]) ).
fof(f7362,plain,
( ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| spl66_116 ),
inference(avatar_component_clause,[],[f7360]) ).
fof(f7364,definition,
( spl66_117
<=> p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))) ),
introduced(definition,[new_symbols(definition,[spl66_117])],[avatar_definition]) ).
fof(f7366,plain,
( ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| spl66_117 ),
inference(avatar_component_clause,[],[f7364]) ).
fof(f7368,definition,
( spl66_118
<=> p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))))) ),
introduced(definition,[new_symbols(definition,[spl66_118])],[avatar_definition]) ).
fof(f7370,plain,
( p__01(s__02(cbool__00,c_27const_2ecfHeapsBase_2eSPLIT3_27__02(s__02(cfun__02(sK7,cbool__00),sK11),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00))),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(c_27type_2epair_2eprod_27__02(cfun__02(sK7,cbool__00),cfun__02(sK7,cbool__00)),c_27const_2epair_2e_2c_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))))))
| ~ spl66_118 ),
inference(avatar_component_clause,[],[f7368]) ).
fof(f7371,plain,
( ~ spl66_116
| ~ spl66_117
| spl66_118
| ~ spl66_22
| ~ spl66_86 ),
inference(avatar_split_clause,[],[f6168,f6128,f1666,f7368,f7364,f7360]) ).
fof(f8096,definition,
( spl66_135
<=> ! [X0] :
( ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X0))))
| p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0)))) ) ),
introduced(definition,[new_symbols(definition,[spl66_135])],[avatar_definition]) ).
fof(f8097,plain,
( ! [X0] :
( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X0)))) )
| ~ spl66_135 ),
inference(avatar_component_clause,[],[f8096]) ).
fof(f8098,plain,
( spl66_135
| ~ spl66_26 ),
inference(avatar_split_clause,[],[f1958,f1936,f8096]) ).
fof(f8099,plain,
( ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| spl66_116
| ~ spl66_135 ),
inference(resolution,[],[f8097,f7362]) ).
fof(f8162,plain,
( ~ p__01(s__02(cbool__00,cT__00))
| ~ spl66_112
| spl66_116
| ~ spl66_135 ),
inference(forward_demodulation,[],[f8099,f6946]) ).
fof(f8163,plain,
( $false
| ~ spl66_72
| ~ spl66_112
| spl66_116
| ~ spl66_135 ),
inference(forward_subsumption_resolution,[],[f8162,f5213]) ).
fof(f8164,plain,
( ~ spl66_72
| ~ spl66_112
| spl66_116
| ~ spl66_135 ),
inference(avatar_contradiction_clause,[],[f8163]) ).
fof(f8271,definition,
( spl66_138
<=> ! [X0] :
( ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X0))))
| p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0)))) ) ),
introduced(definition,[new_symbols(definition,[spl66_138])],[avatar_definition]) ).
fof(f8272,plain,
( ! [X0] :
( p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))),s__02(cfun__02(sK7,cbool__00),X0))))
| ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),X0)))) )
| ~ spl66_138 ),
inference(avatar_component_clause,[],[f8271]) ).
fof(f8273,plain,
( spl66_138
| ~ spl66_26 ),
inference(avatar_split_clause,[],[f1957,f1936,f8271]) ).
fof(f8274,plain,
( ~ p__01(s__02(cbool__00,c_27const_2epred__set_2eDISJOINT_27__02(s__02(cfun__02(sK7,cbool__00),sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| spl66_117
| ~ spl66_138 ),
inference(resolution,[],[f8272,f7366]) ).
fof(f8337,plain,
( ~ p__01(s__02(cbool__00,cT__00))
| ~ spl66_112
| spl66_117
| ~ spl66_138 ),
inference(forward_demodulation,[],[f8274,f6946]) ).
fof(f8338,plain,
( $false
| ~ spl66_72
| ~ spl66_112
| spl66_117
| ~ spl66_138 ),
inference(forward_subsumption_resolution,[],[f8337,f5213]) ).
fof(f8339,plain,
( ~ spl66_72
| ~ spl66_112
| spl66_117
| ~ spl66_138 ),
inference(avatar_contradiction_clause,[],[f8338]) ).
fof(f8394,plain,
( p__01(s__02(cbool__00,cF__00))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ spl66_96
| ~ spl66_118 ),
inference(superposition,[],[f7370,f6404]) ).
fof(f8408,plain,
( ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9),s__02(cfun__02(sK7,cbool__00),sK6(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ spl66_96
| ~ spl66_118 ),
inference(forward_subsumption_resolution,[],[f8394,f105]) ).
fof(f8411,plain,
( ~ p__01(s__02(cbool__00,cT__00))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ spl66_70
| ~ spl66_96
| ~ spl66_118 ),
inference(forward_demodulation,[],[f8408,f5077]) ).
fof(f8413,plain,
( ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK10),s__02(cfun__02(sK7,cbool__00),sK6(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11)))))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ spl66_70
| ~ spl66_96
| ~ spl66_118 ),
inference(forward_subsumption_resolution,[],[f8411,f120]) ).
fof(f8415,plain,
( ~ p__01(s__02(cbool__00,cT__00))
| ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ spl66_69
| ~ spl66_70
| ~ spl66_96
| ~ spl66_118 ),
inference(forward_demodulation,[],[f8413,f5014]) ).
fof(f8417,plain,
( ~ p__01(s__02(cbool__00,chapp__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(sK7,cbool__00),sK5(sK7,sK8,sK9,sK5(sK7,c_27const_2eset__sep_2eSTAR_27__02(s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK8),s__02(cfun__02(cfun__02(sK7,cbool__00),cbool__00),sK9)),sK10,sK11))))))
| ~ spl66_69
| ~ spl66_70
| ~ spl66_96
| ~ spl66_118 ),
inference(forward_subsumption_resolution,[],[f8415,f120]) ).
fof(f8419,plain,
( ~ p__01(s__02(cbool__00,cT__00))
| ~ spl66_68
| ~ spl66_69
| ~ spl66_70
| ~ spl66_96
| ~ spl66_118 ),
inference(forward_demodulation,[],[f8417,f5009]) ).
fof(f8422,plain,
( $false
| ~ spl66_68
| ~ spl66_69
| ~ spl66_70
| ~ spl66_72
| ~ spl66_96
| ~ spl66_118 ),
inference(forward_subsumption_resolution,[],[f8419,f5213]) ).
fof(f8423,plain,
( ~ spl66_68
| ~ spl66_69
| ~ spl66_70
| ~ spl66_72
| ~ spl66_96
| ~ spl66_118 ),
inference(avatar_contradiction_clause,[],[f8422]) ).
cnf(s1,plain,
spl66_1,
inference(sat_conversion,[],[f436]) ).
cnf(s2,plain,
spl66_2,
inference(sat_conversion,[],[f440]) ).
cnf(s6,plain,
( ~ spl66_1
| spl66_7 ),
inference(sat_conversion,[],[f837]) ).
cnf(s8,plain,
( ~ spl66_7
| spl66_9 ),
inference(sat_conversion,[],[f975]) ).
cnf(s9,plain,
( ~ spl66_7
| spl66_10 ),
inference(sat_conversion,[],[f1103]) ).
cnf(s10,plain,
( ~ spl66_1
| spl66_11 ),
inference(sat_conversion,[],[f1231]) ).
cnf(s19,plain,
( ~ spl66_1
| spl66_20 ),
inference(sat_conversion,[],[f1400]) ).
cnf(s20,plain,
( ~ spl66_20
| spl66_21 ),
inference(sat_conversion,[],[f1533]) ).
cnf(s21,plain,
( ~ spl66_20
| spl66_22 ),
inference(sat_conversion,[],[f1669]) ).
cnf(s24,plain,
( ~ spl66_7
| spl66_25 ),
inference(sat_conversion,[],[f1803]) ).
cnf(s25,plain,
( ~ spl66_25
| spl66_26 ),
inference(sat_conversion,[],[f1939]) ).
cnf(s281,plain,
( ~ spl66_9
| spl66_68 ),
inference(sat_conversion,[],[f5010]) ).
cnf(s282,plain,
( ~ spl66_11
| spl66_69 ),
inference(sat_conversion,[],[f5015]) ).
cnf(s283,plain,
( ~ spl66_10
| spl66_70 ),
inference(sat_conversion,[],[f5078]) ).
cnf(s285,plain,
spl66_72,
inference(sat_conversion,[],[f5214]) ).
cnf(s298,plain,
( ~ spl66_25
| ~ spl66_26
| spl66_85 ),
inference(sat_conversion,[],[f6096]) ).
cnf(s299,plain,
( ~ spl66_85
| spl66_86 ),
inference(sat_conversion,[],[f6130]) ).
cnf(s308,plain,
( ~ spl66_2
| spl66_96 ),
inference(sat_conversion,[],[f6405]) ).
cnf(s324,plain,
( ~ spl66_21
| spl66_112 ),
inference(sat_conversion,[],[f6947]) ).
cnf(s328,plain,
( ~ spl66_22
| ~ spl66_86
| ~ spl66_116
| ~ spl66_117
| spl66_118 ),
inference(sat_conversion,[],[f7371]) ).
cnf(s345,plain,
( ~ spl66_26
| spl66_135 ),
inference(sat_conversion,[],[f8098]) ).
cnf(s346,plain,
( ~ spl66_72
| ~ spl66_112
| spl66_116
| ~ spl66_135 ),
inference(sat_conversion,[],[f8164]) ).
cnf(s349,plain,
( ~ spl66_26
| spl66_138 ),
inference(sat_conversion,[],[f8273]) ).
cnf(s350,plain,
( ~ spl66_72
| ~ spl66_112
| spl66_117
| ~ spl66_138 ),
inference(sat_conversion,[],[f8339]) ).
cnf(s352,plain,
( ~ spl66_68
| ~ spl66_69
| ~ spl66_70
| ~ spl66_72
| ~ spl66_96
| ~ spl66_118 ),
inference(sat_conversion,[],[f8423]) ).
cnf(s359,plain,
spl66_96,
inference(rat,[],[s308,s2]) ).
cnf(s400,plain,
spl66_20,
inference(rat,[],[s19,s1]) ).
cnf(s406,plain,
spl66_11,
inference(rat,[],[s10,s1]) ).
cnf(s407,plain,
spl66_7,
inference(rat,[],[s6,s1]) ).
cnf(s412,plain,
spl66_22,
inference(rat,[],[s21,s400]) ).
cnf(s413,plain,
spl66_21,
inference(rat,[],[s20,s400]) ).
cnf(s417,plain,
spl66_69,
inference(rat,[],[s282,s406]) ).
cnf(s421,plain,
spl66_25,
inference(rat,[],[s24,s407]) ).
cnf(s422,plain,
spl66_10,
inference(rat,[],[s9,s407]) ).
cnf(s423,plain,
spl66_9,
inference(rat,[],[s8,s407]) ).
cnf(s431,plain,
spl66_112,
inference(rat,[],[s324,s413]) ).
cnf(s434,plain,
spl66_26,
inference(rat,[],[s25,s421]) ).
cnf(s435,plain,
spl66_70,
inference(rat,[],[s283,s422]) ).
cnf(s436,plain,
spl66_68,
inference(rat,[],[s281,s423]) ).
cnf(s449,plain,
spl66_138,
inference(rat,[],[s349,s434]) ).
cnf(s450,plain,
spl66_135,
inference(rat,[],[s345,s434]) ).
cnf(s454,plain,
spl66_85,
inference(rat,[],[s298,s421,s434]) ).
cnf(s455,plain,
~ spl66_118,
inference(rat,[],[s352,s435,s359,s285,s417,s436]) ).
cnf(s459,plain,
spl66_117,
inference(rat,[],[s350,s431,s285,s449]) ).
cnf(s460,plain,
spl66_116,
inference(rat,[],[s346,s431,s285,s450]) ).
cnf(s461,plain,
spl66_86,
inference(rat,[],[s299,s454]) ).
cnf(s463,plain,
$false,
inference(rat,[],[s328,s455,s459,s412,s460,s461]) ).
fof(f8424,plain,
$false,
inference(avatar_sat_refutation,[],[s463]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW937+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.20 % Computer : n015.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Mon Sep 28 14:49:25 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 Running first-order theorem proving
% 0.10/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.05/1.81 % (2688116)Detected formulas, will run a generic FOF schedule.
% 6.05/1.81 % (2688123)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=1674751431:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 6.05/1.81 % (2688121)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=1878780596:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 6.05/1.81 % (2688125)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=185355057:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 6.05/1.81 % (2688124)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1579282428:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 6.05/1.81 % (2688127)dis-21_1_sil=8000:lcm=predicate:random_seed=2718809146:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 6.05/1.81 % (2688122)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=2255358273:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 6.05/1.81 % (2688126)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=316330802:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 6.05/1.81 % (2688124)Refutation not found, incomplete strategy
% 6.05/1.81 % (2688124)------------------------------
% 6.05/1.81 % (2688124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.81 % (2688124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.81 % (2688124)CaDiCaL version: 2.1.3
% 6.05/1.81 % (2688124)Termination reason: Refutation not found, incomplete strategy
% 6.05/1.81 % (2688124)Time elapsed: 0.011 s
% 6.05/1.81 % (2688124)Peak memory usage: 88 MB
% 6.05/1.81 % (2688124)Instructions burned: 19 (million)
% 6.05/1.81 % (2688125)Instruction limit reached!
% 6.05/1.81 % (2688125)------------------------------
% 6.05/1.81 % (2688125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.81 % (2688125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.81 % (2688125)CaDiCaL version: 2.1.3
% 6.05/1.81 % (2688125)Termination reason: Instruction limit
% 6.05/1.81 % (2688125)Termination phase: Saturation
% 6.05/1.81 % (2688125)Time elapsed: 0.064 s
% 6.05/1.81 % (2688125)Peak memory usage: 88 MB
% 6.05/1.81 % (2688125)Instructions burned: 119 (million)
% 6.05/1.81 % (2688127)Instruction limit reached!
% 6.05/1.81 % (2688127)------------------------------
% 6.05/1.81 % (2688127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.81 % (2688127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.81 % (2688127)CaDiCaL version: 2.1.3
% 6.05/1.81 % (2688127)Termination reason: Instruction limit
% 6.05/1.81 % (2688127)Termination phase: Saturation
% 6.05/1.81 % (2688127)Time elapsed: 0.065 s
% 6.05/1.81 % (2688127)Peak memory usage: 88 MB
% 6.05/1.81 % (2688127)Instructions burned: 129 (million)
% 6.05/1.81 % (2688126)Instruction limit reached!
% 6.05/1.81 % (2688126)------------------------------
% 6.05/1.81 % (2688126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.81 % (2688126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.81 % (2688126)CaDiCaL version: 2.1.3
% 6.05/1.81 % (2688126)Termination reason: Instruction limit
% 6.05/1.81 % (2688126)Termination phase: Saturation
% 6.05/1.81 % (2688126)Time elapsed: 0.079 s
% 6.05/1.81 % (2688126)Peak memory usage: 89 MB
% 6.05/1.81 % (2688126)Instructions burned: 140 (million)
% 6.05/1.81 % (2688136)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3827408086:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 6.05/1.81 % (2688135)lrs+10_1_sil=8000:sp=occurrence:random_seed=910061754:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 6.05/1.81 % (2688137)lrs+1011_1_sil=32000:sp=occurrence:random_seed=68680099:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 6.05/1.81 % (2688124)------------------------------
% 6.05/1.81 % (2688124)------------------------------
% 6.05/1.81 % (2688136)Instruction limit reached!
% 6.05/1.81 % (2688136)------------------------------
% 6.05/1.81 % (2688136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.81 % (2688136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.81 % (2688136)CaDiCaL version: 2.1.3
% 6.05/1.81 % (2688136)Termination reason: Instruction limit
% 6.05/1.81 % (2688136)Termination phase: Saturation
% 6.05/1.81 % (2688136)Time elapsed: 0.073 s
% 6.05/1.81 % (2688136)Peak memory usage: 89 MB
% 6.05/1.81 % (2688136)Instructions burned: 158 (million)
% 6.05/1.81 % (2688135)Instruction limit reached!
% 6.05/1.81 % (2688135)------------------------------
% 6.05/1.81 % (2688135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.81 % (2688135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.81 % (2688135)CaDiCaL version: 2.1.3
% 6.05/1.81 % (2688135)Termination reason: Instruction limit
% 6.05/1.81 % (2688135)Termination phase: Saturation
% 6.05/1.81 % (2688135)Time elapsed: 0.151 s
% 6.05/1.81 % (2688135)Peak memory usage: 89 MB
% 6.05/1.81 % (2688135)Instructions burned: 285 (million)
% 6.05/1.81 % (2688141)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=1681573656:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 6.05/1.81 % (2688137)Instruction limit reached!
% 6.05/1.81 % (2688137)------------------------------
% 6.05/1.81 % (2688137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.81 % (2688137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.81 % (2688137)CaDiCaL version: 2.1.3
% 6.05/1.81 % (2688137)Termination reason: Instruction limit
% 6.05/1.81 % (2688137)Termination phase: Saturation
% 6.05/1.81 % (2688137)Time elapsed: 0.174 s
% 6.05/1.81 % (2688137)Peak memory usage: 90 MB
% 6.05/1.81 % (2688137)Instructions burned: 326 (million)
% 6.05/1.81 % (2688142)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=458865029:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 6.05/1.81 % (2688143)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2979784625:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 6.05/1.81 % (2688141)Instruction limit reached!
% 6.05/1.81 % (2688141)------------------------------
% 6.05/1.81 % (2688141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.81 % (2688141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.81 % (2688141)CaDiCaL version: 2.1.3
% 6.05/1.81 % (2688141)Termination reason: Instruction limit
% 6.05/1.81 % (2688141)Termination phase: Saturation
% 6.05/1.81 % (2688141)Time elapsed: 0.128 s
% 6.05/1.81 % (2688141)Peak memory usage: 90 MB
% 6.05/1.81 % (2688141)Instructions burned: 249 (million)
% 6.05/1.81 % (2688145)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4088576939:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 6.05/1.81 % (2688142)Instruction limit reached!
% 6.05/1.81 % (2688142)------------------------------
% 6.05/1.81 % (2688142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.81 % (2688142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.81 % (2688142)CaDiCaL version: 2.1.3
% 6.05/1.81 % (2688142)Termination reason: Instruction limit
% 6.05/1.81 % (2688142)Termination phase: Saturation
% 6.05/1.81 % (2688142)Time elapsed: 0.156 s
% 6.05/1.81 % (2688142)Peak memory usage: 89 MB
% 6.05/1.81 % (2688142)Instructions burned: 294 (million)
% 6.05/1.81 % (2688145)Instruction limit reached!
% 6.05/1.81 % (2688145)------------------------------
% 6.05/1.81 % (2688145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.81 % (2688145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.81 % (2688145)CaDiCaL version: 2.1.3
% 6.05/1.81 % (2688145)Termination reason: Instruction limit
% 6.05/1.81 % (2688145)Termination phase: Saturation
% 6.05/1.81 % (2688145)Time elapsed: 0.056 s
% 6.05/1.81 % (2688145)Peak memory usage: 89 MB
% 6.05/1.81 % (2688145)Instructions burned: 114 (million)
% 6.05/1.81 % (2688148)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2306778268:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 6.05/1.81 % (2688148)Instruction limit reached!
% 6.05/1.81 % (2688148)------------------------------
% 6.05/1.81 % (2688148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.81 % (2688148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.81 % (2688148)CaDiCaL version: 2.1.3
% 6.05/1.81 % (2688148)Termination reason: Instruction limit
% 6.05/1.81 % (2688148)Termination phase: Saturation
% 6.05/1.81 % (2688148)Time elapsed: 0.055 s
% 6.05/1.81 % (2688148)Peak memory usage: 88 MB
% 6.05/1.81 % (2688148)Instructions burned: 128 (million)
% 6.05/1.81 % (2688150)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3033325786:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 6.05/1.81 % (2688151)lrs+10_1_sil=8000:sp=occurrence:random_seed=3233590279:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 6.05/1.81 % (2688123)First to succeed.
% 6.05/1.81 % (2688123)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2688116"
% 6.05/1.81 % (2688150)Instruction limit reached!
% 6.05/1.81 % (2688150)------------------------------
% 6.05/1.81 % (2688150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.81 % (2688150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.81 % (2688150)CaDiCaL version: 2.1.3
% 6.05/1.81 % (2688150)Termination reason: Instruction limit
% 6.05/1.81 % (2688150)Termination phase: Saturation
% 6.05/1.81 % (2688150)Time elapsed: 0.059 s
% 6.05/1.81 % (2688150)Peak memory usage: 88 MB
% 6.05/1.81 % (2688150)Instructions burned: 114 (million)
% 6.05/1.81 % (2688153)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2063925554:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 6.05/1.81 % (2688123)Refutation found. Thanks to Tanya!
% 6.05/1.81 % SZS status Theorem for theBenchmark
% 6.05/1.81 % SZS output start Proof for theBenchmark
% See solution above
% 8.51/2.01 % (2688123)------------------------------
% 8.51/2.01 % (2688123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.01 % (2688123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.01 % (2688123)CaDiCaL version: 2.1.3
% 8.51/2.01 % (2688123)Termination reason: Refutation
% 8.51/2.01 % (2688123)Time elapsed: 0.832 s
% 8.51/2.01 % (2688123)Peak memory usage: 141 MB
% 8.51/2.01 % (2688123)Instructions burned: 2343 (million)
% 8.51/2.01 % (2688123)------------------------------
% 8.51/2.01 % (2688123)------------------------------
% 8.51/2.01 % (2688116)Success in time 1.128 s
% 8.51/2.01 % Vampire exiting
%------------------------------------------------------------------------------