%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP011+5 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.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 11:28:04 AM UTC 2026
% Result : Theorem 13.06s 7.03s
% Output : Refutation 35.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 28
% Syntax : Number of formulae : 258 ( 29 unt; 21 def)
% Number of atoms : 1107 ( 165 equ)
% Maximal formula atoms : 21 ( 4 avg)
% Number of connectives : 1506 ( 657 ~; 718 |; 65 &)
% ( 35 <=>; 30 =>; 0 <=; 1 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 27 ( 24 usr; 23 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-5 aty)
% Number of variables : 282 ( 0 sgn 264 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1,X2] :
( mem(X2,arr(X0,X1))
=> ! [X3] :
( mem(X3,X0)
=> mem(ap(X2,X3),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ap_tp) ).
fof(f874,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Eoption_2ENONE) ).
fof(f886,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Eoption_2ESOME(X0),arr(X0,ty_2Eoption_2Eoption(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Eoption_2ESOME) ).
fof(f902,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,X0)
=> ! [X2] :
( mem(X2,X0)
=> ( ap(c_2Eoption_2ESOME(X0),X1) = ap(c_2Eoption_2ESOME(X0),X2)
<=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Eoption_2ESOME__11) ).
fof(f903,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,X0)
=> c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Eoption_2ENOT__NONE__SOME) ).
fof(f954,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( mem(X2,arr(X0,arr(X1,bool)))
=> ! [X3] :
( mem(X3,ty_2Eoption_2Eoption(X0))
=> ! [X4] :
( mem(X4,ty_2Eoption_2Eoption(X1))
=> ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
<=> ( ( X3 = c_2Eoption_2ENONE(X0)
& X4 = c_2Eoption_2ENONE(X1) )
| ? [X5] :
( mem(X5,X0)
& ? [X6] :
( mem(X6,X1)
& X3 = ap(c_2Eoption_2ESOME(X0),X5)
& X4 = ap(c_2Eoption_2ESOME(X1),X6)
& p(ap(ap(X2,X5),X6)) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_thm_2Eoption_2EOPTREL__def) ).
fof(f9422,conjecture,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,arr(X0,bool)))
=> ! [X2] :
( mem(X2,X0)
=> ! [X3] :
( mem(X3,X0)
=> ( ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X0)))
<=> $true )
& ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),c_2Eoption_2ENONE(X0)))
<=> $false )
& ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),ap(c_2Eoption_2ESOME(X0),X3)))
<=> $false )
& ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),ap(c_2Eoption_2ESOME(X0),X3)))
<=> p(ap(ap(X1,X2),X3)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Equotient__option_2EOPTION__REL__def) ).
fof(f9423,negated_conjecture,
~ ! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,arr(X0,bool)))
=> ! [X2] :
( mem(X2,X0)
=> ! [X3] :
( mem(X3,X0)
=> ( ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X0)))
<=> $true )
& ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),c_2Eoption_2ENONE(X0)))
<=> $false )
& ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),ap(c_2Eoption_2ESOME(X0),X3)))
<=> $false )
& ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),ap(c_2Eoption_2ESOME(X0),X3)))
<=> p(ap(ap(X1,X2),X3)) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f9422]) ).
fof(f9424,plain,
~ ! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,arr(X0,bool)))
=> ! [X2] :
( mem(X2,X0)
=> ! [X3] :
( mem(X3,X0)
=> ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X0)))
& ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),c_2Eoption_2ENONE(X0)))
& ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),ap(c_2Eoption_2ESOME(X0),X3)))
& ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),ap(c_2Eoption_2ESOME(X0),X3)))
<=> p(ap(ap(X1,X2),X3)) ) ) ) ) ) ),
inference(true_and_false_elimination,[],[f9423]) ).
fof(f9425,plain,
~ ! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,arr(X0,bool)))
=> ! [X2] :
( mem(X2,X0)
=> ! [X3] :
( mem(X3,X0)
=> ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X0)))
& ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),c_2Eoption_2ENONE(X0)))
& ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),ap(c_2Eoption_2ESOME(X0),X3)))
& ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),ap(c_2Eoption_2ESOME(X0),X3)))
<=> p(ap(ap(X1,X2),X3)) ) ) ) ) ) ),
inference(flattening,[],[f9424]) ).
fof(f9502,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X0)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),c_2Eoption_2ENONE(X0)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),ap(c_2Eoption_2ESOME(X0),X3)))
| ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),ap(c_2Eoption_2ESOME(X0),X3)))
<~> p(ap(ap(X1,X2),X3)) ) )
& mem(X3,X0) )
& mem(X2,X0) )
& mem(X1,arr(X0,arr(X0,bool))) )
& ne(X0) ),
inference(ennf_transformation,[],[f9425]) ).
fof(f9549,plain,
! [X0,X1,X2] :
( ! [X3] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f9789,plain,
! [X0] :
( ! [X1] :
( c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X1)
| ~ mem(X1,X0) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f903]) ).
fof(f9797,plain,
! [X0] :
( mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0))
| ~ ne(X0) ),
inference(ennf_transformation,[],[f874]) ).
fof(f9803,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
<=> ( ( X3 = c_2Eoption_2ENONE(X0)
& X4 = c_2Eoption_2ENONE(X1) )
| ? [X5] :
( mem(X5,X0)
& ? [X6] :
( mem(X6,X1)
& X3 = ap(c_2Eoption_2ESOME(X0),X5)
& X4 = ap(c_2Eoption_2ESOME(X1),X6)
& p(ap(ap(X2,X5),X6)) ) ) ) )
| ~ mem(X4,ty_2Eoption_2Eoption(X1)) )
| ~ mem(X3,ty_2Eoption_2Eoption(X0)) )
| ~ mem(X2,arr(X0,arr(X1,bool))) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f954]) ).
fof(f9805,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ap(c_2Eoption_2ESOME(X0),X1) = ap(c_2Eoption_2ESOME(X0),X2)
<=> X1 = X2 )
| ~ mem(X2,X0) )
| ~ mem(X1,X0) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f902]) ).
fof(f9806,plain,
! [X0] :
( mem(c_2Eoption_2ESOME(X0),arr(X0,ty_2Eoption_2Eoption(X0)))
| ~ ne(X0) ),
inference(ennf_transformation,[],[f886]) ).
fof(f11924,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X0)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),c_2Eoption_2ENONE(X0)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),ap(c_2Eoption_2ESOME(X0),X3)))
| ( ( ~ p(ap(ap(X1,X2),X3))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),ap(c_2Eoption_2ESOME(X0),X3))) )
& ( p(ap(ap(X1,X2),X3))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),ap(c_2Eoption_2ESOME(X0),X3))) ) ) )
& mem(X3,X0) )
& mem(X2,X0) )
& mem(X1,arr(X0,arr(X0,bool))) )
& ne(X0) ),
inference(nnf_transformation,[],[f9502]) ).
fof(f11925,plain,
( ( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),c_2Eoption_2ENONE(sK77)),c_2Eoption_2ENONE(sK77)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),c_2Eoption_2ENONE(sK77)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),c_2Eoption_2ENONE(sK77)),ap(c_2Eoption_2ESOME(sK77),sK80)))
| ( ( ~ p(ap(ap(sK78,sK79),sK80))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),ap(c_2Eoption_2ESOME(sK77),sK80))) )
& ( p(ap(ap(sK78,sK79),sK80))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),ap(c_2Eoption_2ESOME(sK77),sK80))) ) ) )
& mem(sK80,sK77)
& mem(sK79,sK77)
& mem(sK78,arr(sK77,arr(sK77,bool)))
& ne(sK77) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK77,sK78,sK79,sK80]),skolemize(X0,sK77),skolemize(X1,sK78),skolemize(X2,sK79),skolemize(X3,sK80)],[f11924]) ).
fof(f12316,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ( ( c_2Eoption_2ENONE(X0) != X3
| c_2Eoption_2ENONE(X1) != X4 )
& ! [X5] :
( ~ mem(X5,X0)
| ! [X6] :
( ~ mem(X6,X1)
| ap(c_2Eoption_2ESOME(X0),X5) != X3
| ap(c_2Eoption_2ESOME(X1),X6) != X4
| ~ p(ap(ap(X2,X5),X6)) ) ) ) )
& ( ( X3 = c_2Eoption_2ENONE(X0)
& X4 = c_2Eoption_2ENONE(X1) )
| ? [X5] :
( mem(X5,X0)
& ? [X6] :
( mem(X6,X1)
& X3 = ap(c_2Eoption_2ESOME(X0),X5)
& X4 = ap(c_2Eoption_2ESOME(X1),X6)
& p(ap(ap(X2,X5),X6)) ) )
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ) )
| ~ mem(X4,ty_2Eoption_2Eoption(X1)) )
| ~ mem(X3,ty_2Eoption_2Eoption(X0)) )
| ~ mem(X2,arr(X0,arr(X1,bool))) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(nnf_transformation,[],[f9803]) ).
fof(f12317,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ( ( c_2Eoption_2ENONE(X0) != X3
| c_2Eoption_2ENONE(X1) != X4 )
& ! [X5] :
( ~ mem(X5,X0)
| ! [X6] :
( ~ mem(X6,X1)
| ap(c_2Eoption_2ESOME(X0),X5) != X3
| ap(c_2Eoption_2ESOME(X1),X6) != X4
| ~ p(ap(ap(X2,X5),X6)) ) ) ) )
& ( ( X3 = c_2Eoption_2ENONE(X0)
& X4 = c_2Eoption_2ENONE(X1) )
| ? [X5] :
( mem(X5,X0)
& ? [X6] :
( mem(X6,X1)
& X3 = ap(c_2Eoption_2ESOME(X0),X5)
& X4 = ap(c_2Eoption_2ESOME(X1),X6)
& p(ap(ap(X2,X5),X6)) ) )
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ) )
| ~ mem(X4,ty_2Eoption_2Eoption(X1)) )
| ~ mem(X3,ty_2Eoption_2Eoption(X0)) )
| ~ mem(X2,arr(X0,arr(X1,bool))) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(flattening,[],[f12316]) ).
fof(f12318,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ( ( c_2Eoption_2ENONE(X0) != X3
| c_2Eoption_2ENONE(X1) != X4 )
& ! [X5] :
( ~ mem(X5,X0)
| ! [X6] :
( ~ mem(X6,X1)
| ap(c_2Eoption_2ESOME(X0),X5) != X3
| ap(c_2Eoption_2ESOME(X1),X6) != X4
| ~ p(ap(ap(X2,X5),X6)) ) ) ) )
& ( ( X3 = c_2Eoption_2ENONE(X0)
& X4 = c_2Eoption_2ENONE(X1) )
| ? [X7] :
( mem(X7,X0)
& ? [X8] :
( mem(X8,X1)
& ap(c_2Eoption_2ESOME(X0),X7) = X3
& ap(c_2Eoption_2ESOME(X1),X8) = X4
& p(ap(ap(X2,X7),X8)) ) )
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ) )
| ~ mem(X4,ty_2Eoption_2Eoption(X1)) )
| ~ mem(X3,ty_2Eoption_2Eoption(X0)) )
| ~ mem(X2,arr(X0,arr(X1,bool))) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(rectify,[],[f12317]) ).
fof(f12319,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ( ( c_2Eoption_2ENONE(X0) != X3
| c_2Eoption_2ENONE(X1) != X4 )
& ! [X5] :
( ~ mem(X5,X0)
| ! [X6] :
( ~ mem(X6,X1)
| ap(c_2Eoption_2ESOME(X0),X5) != X3
| ap(c_2Eoption_2ESOME(X1),X6) != X4
| ~ p(ap(ap(X2,X5),X6)) ) ) ) )
& ( ( X3 = c_2Eoption_2ENONE(X0)
& X4 = c_2Eoption_2ENONE(X1) )
| ( mem(sK242(X0,X1,X2,X3,X4),X0)
& mem(sK243(X0,X1,X2,X3,X4),X1)
& ap(c_2Eoption_2ESOME(X0),sK242(X0,X1,X2,X3,X4)) = X3
& ap(c_2Eoption_2ESOME(X1),sK243(X0,X1,X2,X3,X4)) = X4
& p(ap(ap(X2,sK242(X0,X1,X2,X3,X4)),sK243(X0,X1,X2,X3,X4))) )
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ) )
| ~ mem(X4,ty_2Eoption_2Eoption(X1)) )
| ~ mem(X3,ty_2Eoption_2Eoption(X0)) )
| ~ mem(X2,arr(X0,arr(X1,bool))) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK242,sK243]),skolemize(X7,sK242(X0,X1,X2,X3,X4)),skolemize(X8,sK243(X0,X1,X2,X3,X4))],[f12318]) ).
fof(f12320,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( ap(c_2Eoption_2ESOME(X0),X1) = ap(c_2Eoption_2ESOME(X0),X2)
| X1 != X2 )
& ( X1 = X2
| ap(c_2Eoption_2ESOME(X0),X1) != ap(c_2Eoption_2ESOME(X0),X2) ) )
| ~ mem(X2,X0) )
| ~ mem(X1,X0) )
| ~ ne(X0) ),
inference(nnf_transformation,[],[f9805]) ).
fof(f13617,plain,
ne(sK77),
inference(cnf_transformation,[],[f11925]) ).
fof(f13618,plain,
mem(sK78,arr(sK77,arr(sK77,bool))),
inference(cnf_transformation,[],[f11925]) ).
fof(f13619,plain,
mem(sK79,sK77),
inference(cnf_transformation,[],[f11925]) ).
fof(f13620,plain,
mem(sK80,sK77),
inference(cnf_transformation,[],[f11925]) ).
fof(f13621,plain,
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),c_2Eoption_2ENONE(sK77)),c_2Eoption_2ENONE(sK77)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),c_2Eoption_2ENONE(sK77)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),c_2Eoption_2ENONE(sK77)),ap(c_2Eoption_2ESOME(sK77),sK80)))
| p(ap(ap(sK78,sK79),sK80))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),ap(c_2Eoption_2ESOME(sK77),sK80))) ),
inference(cnf_transformation,[],[f11925]) ).
fof(f13622,plain,
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),c_2Eoption_2ENONE(sK77)),c_2Eoption_2ENONE(sK77)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),c_2Eoption_2ENONE(sK77)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),c_2Eoption_2ENONE(sK77)),ap(c_2Eoption_2ESOME(sK77),sK80)))
| ~ p(ap(ap(sK78,sK79),sK80))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),ap(c_2Eoption_2ESOME(sK77),sK80))) ),
inference(cnf_transformation,[],[f11925]) ).
fof(f13724,plain,
! [X2,X3,X0,X1] :
( ~ mem(X2,arr(X0,X1))
| ~ mem(X3,X0)
| mem(ap(X2,X3),X1) ),
inference(cnf_transformation,[],[f9549]) ).
fof(f14758,plain,
! [X0,X1] :
( c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X1)
| ~ mem(X1,X0)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f9789]) ).
fof(f14778,plain,
! [X0] :
( mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f9797]) ).
fof(f14789,plain,
! [X2,X3,X0,X1,X4] :
( ~ ne(X0)
| ap(c_2Eoption_2ESOME(X1),sK243(X0,X1,X2,X3,X4)) = X4
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| c_2Eoption_2ENONE(X1) = X4 ),
inference(cnf_transformation,[],[f12319]) ).
fof(f14790,plain,
! [X2,X3,X0,X1,X4] :
( ~ ne(X0)
| ap(c_2Eoption_2ESOME(X0),sK242(X0,X1,X2,X3,X4)) = X3
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| c_2Eoption_2ENONE(X1) = X4 ),
inference(cnf_transformation,[],[f12319]) ).
fof(f14791,plain,
! [X2,X3,X0,X1,X4] :
( ~ mem(X3,ty_2Eoption_2Eoption(X0))
| mem(sK243(X0,X1,X2,X3,X4),X1)
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| c_2Eoption_2ENONE(X1) = X4
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f12319]) ).
fof(f14792,plain,
! [X2,X3,X0,X1,X4] :
( ~ mem(X3,ty_2Eoption_2Eoption(X0))
| mem(sK242(X0,X1,X2,X3,X4),X0)
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| c_2Eoption_2ENONE(X1) = X4
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f12319]) ).
fof(f14793,plain,
! [X2,X3,X0,X1,X4] :
( p(ap(ap(X2,sK242(X0,X1,X2,X3,X4)),sK243(X0,X1,X2,X3,X4)))
| c_2Eoption_2ENONE(X0) = X3
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f12319]) ).
fof(f14794,plain,
! [X2,X3,X0,X1,X4] :
( ~ ne(X0)
| ap(c_2Eoption_2ESOME(X1),sK243(X0,X1,X2,X3,X4)) = X4
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| c_2Eoption_2ENONE(X0) = X3 ),
inference(cnf_transformation,[],[f12319]) ).
fof(f14795,plain,
! [X2,X3,X0,X1,X4] :
( ~ ne(X0)
| ap(c_2Eoption_2ESOME(X0),sK242(X0,X1,X2,X3,X4)) = X3
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| c_2Eoption_2ENONE(X0) = X3 ),
inference(cnf_transformation,[],[f12319]) ).
fof(f14796,plain,
! [X2,X3,X0,X1,X4] :
( ~ mem(X3,ty_2Eoption_2Eoption(X0))
| mem(sK243(X0,X1,X2,X3,X4),X1)
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| c_2Eoption_2ENONE(X0) = X3
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f12319]) ).
fof(f14798,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ~ mem(X5,X0)
| ~ mem(X6,X1)
| ap(c_2Eoption_2ESOME(X0),X5) != X3
| ap(c_2Eoption_2ESOME(X1),X6) != X4
| ~ p(ap(ap(X2,X5),X6))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f12319]) ).
fof(f14799,plain,
! [X2,X3,X0,X1,X4] :
( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| c_2Eoption_2ENONE(X0) != X3
| c_2Eoption_2ENONE(X1) != X4
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f12319]) ).
fof(f14801,plain,
! [X2,X0,X1] :
( ap(c_2Eoption_2ESOME(X0),X1) != ap(c_2Eoption_2ESOME(X0),X2)
| X1 = X2
| ~ mem(X2,X0)
| ~ mem(X1,X0)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f12320]) ).
fof(f14803,plain,
! [X0] :
( mem(c_2Eoption_2ESOME(X0),arr(X0,ty_2Eoption_2Eoption(X0)))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f9806]) ).
fof(f18881,plain,
! [X2,X0,X1,X4] :
( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),c_2Eoption_2ENONE(X0)),X4))
| c_2Eoption_2ENONE(X1) != X4
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(equality_resolution,[],[f14799]) ).
fof(f18882,plain,
! [X2,X0,X1] :
( ~ mem(c_2Eoption_2ENONE(X1),ty_2Eoption_2Eoption(X1))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X1)))
| ~ mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(equality_resolution,[],[f18881]) ).
fof(f18883,plain,
! [X2,X0,X1,X6,X4,X5] :
( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),ap(c_2Eoption_2ESOME(X0),X5)),X4))
| ~ mem(X5,X0)
| ~ mem(X6,X1)
| ap(c_2Eoption_2ESOME(X1),X6) != X4
| ~ p(ap(ap(X2,X5),X6))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(ap(c_2Eoption_2ESOME(X0),X5),ty_2Eoption_2Eoption(X0))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(equality_resolution,[],[f14798]) ).
fof(f18884,plain,
! [X2,X0,X1,X6,X5] :
( ~ mem(ap(c_2Eoption_2ESOME(X0),X5),ty_2Eoption_2Eoption(X0))
| ~ mem(X5,X0)
| ~ mem(X6,X1)
| ~ p(ap(ap(X2,X5),X6))
| ~ mem(ap(c_2Eoption_2ESOME(X1),X6),ty_2Eoption_2Eoption(X1))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),ap(c_2Eoption_2ESOME(X0),X5)),ap(c_2Eoption_2ESOME(X1),X6)))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(equality_resolution,[],[f18883]) ).
fof(f20068,definition,
( spl880_140
<=> p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),ap(c_2Eoption_2ESOME(sK77),sK80))) ),
introduced(definition,[new_symbols(definition,[spl880_140])],[avatar_definition]) ).
fof(f20069,plain,
( p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),ap(c_2Eoption_2ESOME(sK77),sK80)))
| ~ spl880_140 ),
inference(avatar_component_clause,[],[f20068]) ).
fof(f20071,definition,
( spl880_141
<=> p(ap(ap(sK78,sK79),sK80)) ),
introduced(definition,[new_symbols(definition,[spl880_141])],[avatar_definition]) ).
fof(f20072,plain,
( p(ap(ap(sK78,sK79),sK80))
| ~ spl880_141 ),
inference(avatar_component_clause,[],[f20071]) ).
fof(f20074,definition,
( spl880_142
<=> p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),c_2Eoption_2ENONE(sK77)),ap(c_2Eoption_2ESOME(sK77),sK80))) ),
introduced(definition,[new_symbols(definition,[spl880_142])],[avatar_definition]) ).
fof(f20075,plain,
( p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),c_2Eoption_2ENONE(sK77)),ap(c_2Eoption_2ESOME(sK77),sK80)))
| ~ spl880_142 ),
inference(avatar_component_clause,[],[f20074]) ).
fof(f20077,definition,
( spl880_143
<=> p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),c_2Eoption_2ENONE(sK77))) ),
introduced(definition,[new_symbols(definition,[spl880_143])],[avatar_definition]) ).
fof(f20078,plain,
( p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),c_2Eoption_2ENONE(sK77)))
| ~ spl880_143 ),
inference(avatar_component_clause,[],[f20077]) ).
fof(f20080,definition,
( spl880_144
<=> p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),c_2Eoption_2ENONE(sK77)),c_2Eoption_2ENONE(sK77))) ),
introduced(definition,[new_symbols(definition,[spl880_144])],[avatar_definition]) ).
fof(f20081,plain,
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),c_2Eoption_2ENONE(sK77)),c_2Eoption_2ENONE(sK77)))
| spl880_144 ),
inference(avatar_component_clause,[],[f20080]) ).
fof(f20082,plain,
( spl880_140
| spl880_141
| spl880_142
| spl880_143
| ~ spl880_144 ),
inference(avatar_split_clause,[],[f13621,f20080,f20077,f20074,f20071,f20068]) ).
fof(f20083,plain,
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),ap(c_2Eoption_2ESOME(sK77),sK80)))
| spl880_140 ),
inference(avatar_component_clause,[],[f20068]) ).
fof(f20084,plain,
( ~ p(ap(ap(sK78,sK79),sK80))
| spl880_141 ),
inference(avatar_component_clause,[],[f20071]) ).
fof(f20085,plain,
( ~ spl880_140
| ~ spl880_141
| spl880_142
| spl880_143
| ~ spl880_144 ),
inference(avatar_split_clause,[],[f13622,f20080,f20077,f20074,f20071,f20068]) ).
fof(f20105,plain,
! [X2,X0,X1] :
( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X1)))
| ~ mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0)
| ~ ne(X1) ),
inference(resolution,[],[f18882,f14778]) ).
fof(f20106,plain,
! [X2,X0,X1] :
( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X1)))
| ~ mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(duplicate_literal_removal,[],[f20105]) ).
fof(f20107,plain,
! [X2,X0,X1] :
( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X1)))
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f20106,f14778]) ).
fof(f20109,plain,
( ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| ~ ne(sK77)
| ~ ne(sK77)
| spl880_144 ),
inference(resolution,[],[f20107,f20081]) ).
fof(f20110,plain,
( ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| ~ ne(sK77)
| spl880_144 ),
inference(duplicate_literal_removal,[],[f20109]) ).
fof(f20112,plain,
( ~ ne(sK77)
| spl880_144 ),
inference(forward_subsumption_resolution,[],[f20110,f13618]) ).
fof(f20113,plain,
( $false
| spl880_144 ),
inference(forward_subsumption_resolution,[],[f20112,f13617]) ).
fof(f20114,plain,
spl880_144,
inference(avatar_contradiction_clause,[],[f20113]) ).
fof(f20125,plain,
! [X0,X1] :
( mem(ap(c_2Eoption_2ESOME(X0),X1),ty_2Eoption_2Eoption(X0))
| ~ mem(X1,X0)
| ~ ne(X0) ),
inference(resolution,[],[f14803,f13724]) ).
fof(f20126,plain,
! [X2,X3,X0,X1] :
( ~ mem(X1,arr(sK77,arr(X0,bool)))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,X0),X1),X2),X3))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X2,ty_2Eoption_2Eoption(sK77))
| ap(c_2Eoption_2ESOME(sK77),sK242(sK77,X0,X1,X2,X3)) = X2
| ~ ne(X0)
| c_2Eoption_2ENONE(X0) = X3 ),
inference(resolution,[],[f14790,f13617]) ).
fof(f20127,plain,
! [X2,X3,X0,X1] :
( ~ mem(X1,arr(sK77,arr(X0,bool)))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,X0),X1),X2),X3))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X2,ty_2Eoption_2Eoption(sK77))
| ap(c_2Eoption_2ESOME(sK77),sK242(sK77,X0,X1,X2,X3)) = X2
| ~ ne(X0)
| c_2Eoption_2ENONE(sK77) = X2 ),
inference(resolution,[],[f14795,f13617]) ).
fof(f20128,plain,
! [X2,X3,X0,X1] :
( ~ ne(X0)
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,X0),X1),X2),X3))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X2,ty_2Eoption_2Eoption(sK77))
| ~ mem(X1,arr(sK77,arr(X0,bool)))
| ap(c_2Eoption_2ESOME(X0),sK243(sK77,X0,X1,X2,X3)) = X3
| c_2Eoption_2ENONE(X0) = X3 ),
inference(resolution,[],[f14789,f13617]) ).
fof(f20129,plain,
! [X2,X0,X1] :
( ~ mem(X0,arr(sK77,arr(sK77,bool)))
| ~ mem(X2,ty_2Eoption_2Eoption(sK77))
| ~ mem(X1,ty_2Eoption_2Eoption(sK77))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),X0),X1),X2))
| ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,X0,X1,X2)) = X2
| c_2Eoption_2ENONE(sK77) = X2 ),
inference(resolution,[],[f20128,f13617]) ).
fof(f20130,plain,
! [X2,X3,X0,X1] :
( ~ ne(X0)
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,X0),X1),X2),X3))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X2,ty_2Eoption_2Eoption(sK77))
| ~ mem(X1,arr(sK77,arr(X0,bool)))
| ap(c_2Eoption_2ESOME(X0),sK243(sK77,X0,X1,X2,X3)) = X3
| c_2Eoption_2ENONE(sK77) = X2 ),
inference(resolution,[],[f14794,f13617]) ).
fof(f20131,plain,
! [X2,X0,X1] :
( ~ mem(X0,arr(sK77,arr(sK77,bool)))
| ~ mem(X2,ty_2Eoption_2Eoption(sK77))
| ~ mem(X1,ty_2Eoption_2Eoption(sK77))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),X0),X1),X2))
| ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,X0,X1,X2)) = X2
| c_2Eoption_2ENONE(sK77) = X1 ),
inference(resolution,[],[f20130,f13617]) ).
fof(f20142,plain,
! [X0,X1] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),X0),X1))
| ~ mem(X1,ty_2Eoption_2Eoption(sK77))
| ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,X0,X1)) = X0
| ~ ne(sK77)
| c_2Eoption_2ENONE(sK77) = X0 ),
inference(resolution,[],[f20127,f13618]) ).
fof(f20143,plain,
! [X0,X1] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ~ mem(X1,ty_2Eoption_2Eoption(sK77))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),X0),X1))
| ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,X0,X1)) = X0
| c_2Eoption_2ENONE(sK77) = X0 ),
inference(forward_subsumption_resolution,[],[f20142,f13617]) ).
fof(f20145,plain,
! [X0,X1] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),X1)),X0))
| ap(c_2Eoption_2ESOME(sK77),X1) = ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),X1),X0))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),X1)
| ~ mem(X1,sK77)
| ~ ne(sK77) ),
inference(resolution,[],[f20143,f20125]) ).
fof(f20146,plain,
! [X0,X1] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),X1)),X0))
| ap(c_2Eoption_2ESOME(sK77),X1) = ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),X1),X0))
| ~ mem(X1,sK77)
| ~ ne(sK77) ),
inference(forward_subsumption_resolution,[],[f20145,f14758]) ).
fof(f20147,plain,
! [X0,X1] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),X1)),X0))
| ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ap(c_2Eoption_2ESOME(sK77),X1) = ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),X1),X0))
| ~ mem(X1,sK77) ),
inference(forward_subsumption_resolution,[],[f20146,f13617]) ).
fof(f20148,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| ap(c_2Eoption_2ESOME(sK77),sK79) = ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)))
| ~ mem(sK79,sK77)
| ~ spl880_140 ),
inference(resolution,[],[f20147,f20069]) ).
fof(f20149,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| ap(c_2Eoption_2ESOME(sK77),sK79) = ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)))
| ~ spl880_140 ),
inference(forward_subsumption_resolution,[],[f20148,f13619]) ).
fof(f20151,definition,
( spl880_147
<=> ap(c_2Eoption_2ESOME(sK77),sK79) = ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))) ),
introduced(definition,[new_symbols(definition,[spl880_147])],[avatar_definition]) ).
fof(f20152,plain,
( ap(c_2Eoption_2ESOME(sK77),sK79) = ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)))
| ~ spl880_147 ),
inference(avatar_component_clause,[],[f20151]) ).
fof(f20154,definition,
( spl880_148
<=> mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77)) ),
introduced(definition,[new_symbols(definition,[spl880_148])],[avatar_definition]) ).
fof(f20155,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| spl880_148 ),
inference(avatar_component_clause,[],[f20154]) ).
fof(f20156,plain,
( spl880_147
| ~ spl880_148
| ~ spl880_140 ),
inference(avatar_split_clause,[],[f20149,f20068,f20154,f20151]) ).
fof(f20158,plain,
( ~ mem(sK80,sK77)
| ~ ne(sK77)
| spl880_148 ),
inference(resolution,[],[f20155,f20125]) ).
fof(f20160,plain,
( ~ ne(sK77)
| spl880_148 ),
inference(forward_subsumption_resolution,[],[f20158,f13620]) ).
fof(f20161,plain,
( $false
| spl880_148 ),
inference(forward_subsumption_resolution,[],[f20160,f13617]) ).
fof(f20162,plain,
spl880_148,
inference(avatar_contradiction_clause,[],[f20161]) ).
fof(f20163,plain,
! [X0,X1] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),X0),X1))
| ~ mem(X1,ty_2Eoption_2Eoption(sK77))
| ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,X0,X1)) = X0
| ~ ne(sK77)
| c_2Eoption_2ENONE(sK77) = X1 ),
inference(resolution,[],[f20126,f13618]) ).
fof(f20164,plain,
! [X0,X1] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),X0),X1))
| ~ mem(X1,ty_2Eoption_2Eoption(sK77))
| ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,X0,X1)) = X0
| c_2Eoption_2ENONE(sK77) = X1 ),
inference(forward_subsumption_resolution,[],[f20163,f13617]) ).
fof(f20170,plain,
! [X0,X1] :
( ~ mem(X1,ty_2Eoption_2Eoption(sK77))
| ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),X1),X0))
| ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,X1,X0)) = X0
| c_2Eoption_2ENONE(sK77) = X1 ),
inference(resolution,[],[f20131,f13618]) ).
fof(f20171,plain,
! [X0,X1] :
( ~ mem(X1,ty_2Eoption_2Eoption(sK77))
| ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),X1),X0))
| ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,X1,X0)) = X0
| c_2Eoption_2ENONE(sK77) = X0 ),
inference(resolution,[],[f20129,f13618]) ).
fof(f20173,plain,
! [X0,X1] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),X1)),X0))
| ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),X1),X0)) = X0
| c_2Eoption_2ENONE(sK77) = X0
| ~ mem(X1,sK77)
| ~ ne(sK77) ),
inference(resolution,[],[f20171,f20125]) ).
fof(f20174,plain,
! [X0,X1] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),X1)),X0))
| ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),X1),X0)) = X0
| c_2Eoption_2ENONE(sK77) = X0
| ~ mem(X1,sK77) ),
inference(forward_subsumption_resolution,[],[f20173,f13617]) ).
fof(f20177,plain,
! [X0,X1] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),X1)),X0))
| ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),X1),X0)) = X0
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),X1)
| ~ mem(X1,sK77)
| ~ ne(sK77) ),
inference(resolution,[],[f20170,f20125]) ).
fof(f20178,plain,
! [X0,X1] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),X1)),X0))
| ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),X1),X0)) = X0
| ~ mem(X1,sK77)
| ~ ne(sK77) ),
inference(forward_subsumption_resolution,[],[f20177,f14758]) ).
fof(f20179,plain,
! [X0,X1] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),X1)),X0))
| ~ mem(X0,ty_2Eoption_2Eoption(sK77))
| ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),X1),X0)) = X0
| ~ mem(X1,sK77) ),
inference(forward_subsumption_resolution,[],[f20178,f13617]) ).
fof(f20220,plain,
! [X2,X3,X0,X1] :
( mem(sK242(X0,X1,X2,c_2Eoption_2ENONE(X0),X3),X0)
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),c_2Eoption_2ENONE(X0)),X3))
| ~ mem(X3,ty_2Eoption_2Eoption(X1))
| c_2Eoption_2ENONE(X1) = X3
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0)
| ~ ne(X0) ),
inference(resolution,[],[f14792,f14778]) ).
fof(f20223,plain,
! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),c_2Eoption_2ENONE(X0)),X3))
| mem(sK242(X0,X1,X2,c_2Eoption_2ENONE(X0),X3),X0)
| ~ mem(X3,ty_2Eoption_2Eoption(X1))
| c_2Eoption_2ENONE(X1) = X3
| ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(duplicate_literal_removal,[],[f20220]) ).
fof(f20393,plain,
! [X2,X3,X0,X1,X4] :
( ~ mem(X0,X1)
| ~ mem(X2,X3)
| ~ p(ap(ap(X4,X0),X2))
| ~ mem(ap(c_2Eoption_2ESOME(X3),X2),ty_2Eoption_2Eoption(X3))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X1,X3),X4),ap(c_2Eoption_2ESOME(X1),X0)),ap(c_2Eoption_2ESOME(X3),X2)))
| ~ mem(X4,arr(X1,arr(X3,bool)))
| ~ ne(X3)
| ~ ne(X1)
| ~ mem(X0,X1)
| ~ ne(X1) ),
inference(resolution,[],[f18884,f20125]) ).
fof(f20394,plain,
! [X2,X3,X0,X1,X4] :
( ~ mem(X0,X1)
| ~ mem(X2,X3)
| ~ p(ap(ap(X4,X0),X2))
| ~ mem(ap(c_2Eoption_2ESOME(X3),X2),ty_2Eoption_2Eoption(X3))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X1,X3),X4),ap(c_2Eoption_2ESOME(X1),X0)),ap(c_2Eoption_2ESOME(X3),X2)))
| ~ mem(X4,arr(X1,arr(X3,bool)))
| ~ ne(X3)
| ~ ne(X1) ),
inference(duplicate_literal_removal,[],[f20393]) ).
fof(f20395,plain,
! [X2,X3,X0,X1,X4] :
( ~ mem(X4,arr(X1,arr(X3,bool)))
| ~ mem(X2,X3)
| ~ p(ap(ap(X4,X0),X2))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X1,X3),X4),ap(c_2Eoption_2ESOME(X1),X0)),ap(c_2Eoption_2ESOME(X3),X2)))
| ~ mem(X0,X1)
| ~ ne(X3)
| ~ ne(X1) ),
inference(forward_subsumption_resolution,[],[f20394,f20125]) ).
fof(f20396,plain,
( $false
| spl880_140
| ~ spl880_141 ),
inference(unit_resulting_resolution,[],[f20395,f13617,f13617,f13619,f13620,f20072,f13618,f20083]) ).
fof(f20402,plain,
( spl880_140
| ~ spl880_141 ),
inference(avatar_contradiction_clause,[],[f20396]) ).
fof(f20407,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| ~ mem(c_2Eoption_2ENONE(sK77),ty_2Eoption_2Eoption(sK77))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,c_2Eoption_2ENONE(sK77),ap(c_2Eoption_2ESOME(sK77),sK80)))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK80)
| ~ spl880_142 ),
inference(resolution,[],[f20075,f20164]) ).
fof(f20409,plain,
( mem(sK242(sK77,sK77,sK78,c_2Eoption_2ENONE(sK77),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77)
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK80)
| ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| ~ ne(sK77)
| ~ ne(sK77)
| ~ spl880_142 ),
inference(resolution,[],[f20075,f20223]) ).
fof(f20410,plain,
( mem(sK242(sK77,sK77,sK78,c_2Eoption_2ENONE(sK77),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77)
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK80)
| ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| ~ ne(sK77)
| ~ spl880_142 ),
inference(duplicate_literal_removal,[],[f20409]) ).
fof(f20412,plain,
( mem(sK242(sK77,sK77,sK78,c_2Eoption_2ENONE(sK77),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77)
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK80)
| ~ ne(sK77)
| ~ spl880_142 ),
inference(forward_subsumption_resolution,[],[f20410,f13618]) ).
fof(f20415,definition,
( spl880_149
<=> c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK80) ),
introduced(definition,[new_symbols(definition,[spl880_149])],[avatar_definition]) ).
fof(f20416,plain,
( c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK80)
| ~ spl880_149 ),
inference(avatar_component_clause,[],[f20415]) ).
fof(f20418,definition,
( spl880_150
<=> c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,c_2Eoption_2ENONE(sK77),ap(c_2Eoption_2ESOME(sK77),sK80))) ),
introduced(definition,[new_symbols(definition,[spl880_150])],[avatar_definition]) ).
fof(f20419,plain,
( c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK242(sK77,sK77,sK78,c_2Eoption_2ENONE(sK77),ap(c_2Eoption_2ESOME(sK77),sK80)))
| ~ spl880_150 ),
inference(avatar_component_clause,[],[f20418]) ).
fof(f20421,definition,
( spl880_151
<=> mem(c_2Eoption_2ENONE(sK77),ty_2Eoption_2Eoption(sK77)) ),
introduced(definition,[new_symbols(definition,[spl880_151])],[avatar_definition]) ).
fof(f20422,plain,
( ~ mem(c_2Eoption_2ENONE(sK77),ty_2Eoption_2Eoption(sK77))
| spl880_151 ),
inference(avatar_component_clause,[],[f20421]) ).
fof(f20423,plain,
( spl880_149
| spl880_150
| ~ spl880_151
| ~ spl880_148
| ~ spl880_142 ),
inference(avatar_split_clause,[],[f20407,f20074,f20154,f20421,f20418,f20415]) ).
fof(f20428,plain,
( mem(sK242(sK77,sK77,sK78,c_2Eoption_2ENONE(sK77),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77)
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK80)
| ~ spl880_142 ),
inference(forward_subsumption_resolution,[],[f20412,f13617]) ).
fof(f20431,definition,
( spl880_153
<=> mem(sK242(sK77,sK77,sK78,c_2Eoption_2ENONE(sK77),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77) ),
introduced(definition,[new_symbols(definition,[spl880_153])],[avatar_definition]) ).
fof(f20433,plain,
( spl880_149
| ~ spl880_148
| spl880_153
| ~ spl880_142 ),
inference(avatar_split_clause,[],[f20428,f20074,f20431,f20154,f20415]) ).
fof(f20439,plain,
( ~ mem(c_2Eoption_2ENONE(sK77),ty_2Eoption_2Eoption(sK77))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77)))
| ~ mem(sK79,sK77)
| ~ spl880_143 ),
inference(resolution,[],[f20078,f20179]) ).
fof(f20443,plain,
( ~ mem(c_2Eoption_2ENONE(sK77),ty_2Eoption_2Eoption(sK77))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77)))
| ~ spl880_143 ),
inference(forward_subsumption_resolution,[],[f20439,f13619]) ).
fof(f20449,definition,
( spl880_156
<=> c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77))) ),
introduced(definition,[new_symbols(definition,[spl880_156])],[avatar_definition]) ).
fof(f20450,plain,
( c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77)))
| ~ spl880_156 ),
inference(avatar_component_clause,[],[f20449]) ).
fof(f20451,plain,
( spl880_156
| ~ spl880_151
| ~ spl880_143 ),
inference(avatar_split_clause,[],[f20443,f20077,f20421,f20449]) ).
fof(f20453,plain,
( ~ ne(sK77)
| spl880_151 ),
inference(resolution,[],[f20422,f14778]) ).
fof(f20455,plain,
( $false
| spl880_151 ),
inference(forward_subsumption_resolution,[],[f20453,f13617]) ).
fof(f20456,plain,
spl880_151,
inference(avatar_contradiction_clause,[],[f20455]) ).
fof(f20457,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| ap(c_2Eoption_2ESOME(sK77),sK80) = ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK80)
| ~ mem(sK79,sK77)
| ~ spl880_140 ),
inference(resolution,[],[f20069,f20174]) ).
fof(f20462,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| ap(c_2Eoption_2ESOME(sK77),sK80) = ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK80)
| ~ spl880_140 ),
inference(forward_subsumption_resolution,[],[f20457,f13619]) ).
fof(f20464,definition,
( spl880_157
<=> ap(c_2Eoption_2ESOME(sK77),sK80) = ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))) ),
introduced(definition,[new_symbols(definition,[spl880_157])],[avatar_definition]) ).
fof(f20465,plain,
( ap(c_2Eoption_2ESOME(sK77),sK80) = ap(c_2Eoption_2ESOME(sK77),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)))
| ~ spl880_157 ),
inference(avatar_component_clause,[],[f20464]) ).
fof(f20467,plain,
( spl880_149
| spl880_157
| ~ spl880_148
| ~ spl880_140 ),
inference(avatar_split_clause,[],[f20462,f20068,f20154,f20464,f20415]) ).
fof(f20478,definition,
( spl880_158
<=> mem(sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77) ),
introduced(definition,[new_symbols(definition,[spl880_158])],[avatar_definition]) ).
fof(f20479,plain,
( ~ mem(sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77)
| spl880_158 ),
inference(avatar_component_clause,[],[f20478]) ).
fof(f20493,definition,
( spl880_162
<=> mem(ap(c_2Eoption_2ESOME(sK77),sK79),ty_2Eoption_2Eoption(sK77)) ),
introduced(definition,[new_symbols(definition,[spl880_162])],[avatar_definition]) ).
fof(f20494,plain,
( mem(ap(c_2Eoption_2ESOME(sK77),sK79),ty_2Eoption_2Eoption(sK77))
| ~ spl880_162 ),
inference(avatar_component_clause,[],[f20493]) ).
fof(f20497,definition,
( spl880_163
<=> c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK79) ),
introduced(definition,[new_symbols(definition,[spl880_163])],[avatar_definition]) ).
fof(f20498,plain,
( c_2Eoption_2ENONE(sK77) != ap(c_2Eoption_2ESOME(sK77),sK79)
| spl880_163 ),
inference(avatar_component_clause,[],[f20497]) ).
fof(f20504,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK77),sK79),ty_2Eoption_2Eoption(sK77))
| spl880_162 ),
inference(avatar_component_clause,[],[f20493]) ).
fof(f20518,definition,
( spl880_165
<=> mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77) ),
introduced(definition,[new_symbols(definition,[spl880_165])],[avatar_definition]) ).
fof(f20519,plain,
( ~ mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77)
| spl880_165 ),
inference(avatar_component_clause,[],[f20518]) ).
fof(f20532,plain,
( mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| ~ spl880_148 ),
inference(avatar_component_clause,[],[f20154]) ).
fof(f20534,plain,
( c_2Eoption_2ENONE(sK77) != ap(c_2Eoption_2ESOME(sK77),sK80)
| spl880_149 ),
inference(avatar_component_clause,[],[f20415]) ).
fof(f20584,plain,
( c_2Eoption_2ENONE(sK77) != c_2Eoption_2ENONE(sK77)
| ~ mem(sK80,sK77)
| ~ ne(sK77)
| ~ spl880_149 ),
inference(superposition,[],[f14758,f20416]) ).
fof(f20586,plain,
( ~ mem(sK80,sK77)
| ~ ne(sK77)
| ~ spl880_149 ),
inference(trivial_inequality_removal,[],[f20584]) ).
fof(f20588,plain,
( ~ ne(sK77)
| ~ spl880_149 ),
inference(forward_subsumption_resolution,[],[f20586,f13620]) ).
fof(f20595,plain,
( $false
| ~ spl880_149 ),
inference(forward_subsumption_resolution,[],[f20588,f13617]) ).
fof(f20596,plain,
~ spl880_149,
inference(avatar_contradiction_clause,[],[f20595]) ).
fof(f20705,plain,
( ! [X0] :
( ap(c_2Eoption_2ESOME(sK77),sK79) != ap(c_2Eoption_2ESOME(sK77),X0)
| sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)) = X0
| ~ mem(X0,sK77)
| ~ mem(sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77)
| ~ ne(sK77) )
| ~ spl880_147 ),
inference(superposition,[],[f14801,f20152]) ).
fof(f20706,plain,
( ! [X0] :
( ap(c_2Eoption_2ESOME(sK77),sK80) != ap(c_2Eoption_2ESOME(sK77),X0)
| sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)) = X0
| ~ mem(X0,sK77)
| ~ mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77)
| ~ ne(sK77) )
| ~ spl880_157 ),
inference(superposition,[],[f14801,f20465]) ).
fof(f20914,plain,
( c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK79)
| ~ spl880_163 ),
inference(avatar_component_clause,[],[f20497]) ).
fof(f20920,plain,
( ~ mem(sK79,sK77)
| ~ ne(sK77)
| spl880_162 ),
inference(resolution,[],[f20504,f20125]) ).
fof(f20922,plain,
( ~ ne(sK77)
| spl880_162 ),
inference(forward_subsumption_resolution,[],[f20920,f13619]) ).
fof(f20923,plain,
( $false
| spl880_162 ),
inference(forward_subsumption_resolution,[],[f20922,f13617]) ).
fof(f20924,plain,
spl880_162,
inference(avatar_contradiction_clause,[],[f20923]) ).
fof(f20925,plain,
( $false
| ~ spl880_140
| ~ spl880_148
| spl880_149
| ~ spl880_162
| spl880_165 ),
inference(unit_resulting_resolution,[],[f14791,f13617,f13617,f13618,f20534,f20532,f20519,f20069,f20494]) ).
fof(f20926,plain,
( $false
| ~ spl880_140
| ~ spl880_148
| spl880_149
| spl880_158
| ~ spl880_162 ),
inference(unit_resulting_resolution,[],[f14792,f13617,f13617,f13618,f20534,f20532,f20479,f20069,f20494]) ).
fof(f20936,plain,
( ! [X2,X0,X1] :
( mem(sK243(sK77,X0,X1,ap(c_2Eoption_2ESOME(sK77),sK79),X2),X0)
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,X0),X1),ap(c_2Eoption_2ESOME(sK77),sK79)),X2))
| ~ mem(X2,ty_2Eoption_2Eoption(X0))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK79)
| ~ mem(X1,arr(sK77,arr(X0,bool)))
| ~ ne(X0)
| ~ ne(sK77) )
| ~ spl880_162 ),
inference(resolution,[],[f20494,f14796]) ).
fof(f20939,plain,
( ~ spl880_140
| ~ spl880_148
| spl880_149
| ~ spl880_162
| spl880_165 ),
inference(avatar_contradiction_clause,[],[f20925]) ).
fof(f20940,plain,
( ~ spl880_140
| ~ spl880_148
| spl880_149
| spl880_158
| ~ spl880_162 ),
inference(avatar_contradiction_clause,[],[f20926]) ).
fof(f20943,plain,
( ! [X2,X0,X1] :
( mem(sK243(sK77,X0,X1,ap(c_2Eoption_2ESOME(sK77),sK79),X2),X0)
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,X0),X1),ap(c_2Eoption_2ESOME(sK77),sK79)),X2))
| ~ mem(X2,ty_2Eoption_2Eoption(X0))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK79)
| ~ mem(X1,arr(sK77,arr(X0,bool)))
| ~ ne(X0) )
| ~ spl880_162 ),
inference(forward_subsumption_resolution,[],[f20936,f13617]) ).
fof(f20958,definition,
( spl880_177
<=> ! [X2,X0,X1] :
( mem(sK243(sK77,X0,X1,ap(c_2Eoption_2ESOME(sK77),sK79),X2),X0)
| ~ ne(X0)
| ~ mem(X1,arr(sK77,arr(X0,bool)))
| ~ mem(X2,ty_2Eoption_2Eoption(X0))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,X0),X1),ap(c_2Eoption_2ESOME(sK77),sK79)),X2)) ) ),
introduced(definition,[new_symbols(definition,[spl880_177])],[avatar_definition]) ).
fof(f20959,plain,
( ! [X2,X0,X1] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,X0),X1),ap(c_2Eoption_2ESOME(sK77),sK79)),X2))
| ~ ne(X0)
| ~ mem(X1,arr(sK77,arr(X0,bool)))
| ~ mem(X2,ty_2Eoption_2Eoption(X0))
| mem(sK243(sK77,X0,X1,ap(c_2Eoption_2ESOME(sK77),sK79),X2),X0) )
| ~ spl880_177 ),
inference(avatar_component_clause,[],[f20958]) ).
fof(f20960,plain,
( spl880_163
| spl880_177
| ~ spl880_162 ),
inference(avatar_split_clause,[],[f20943,f20493,f20958,f20497]) ).
fof(f20962,plain,
( ! [X0] :
( ap(c_2Eoption_2ESOME(sK77),sK80) != ap(c_2Eoption_2ESOME(sK77),X0)
| sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)) = X0
| ~ mem(X0,sK77)
| ~ mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77) )
| ~ spl880_157 ),
inference(forward_subsumption_resolution,[],[f20706,f13617]) ).
fof(f20964,plain,
( ! [X0] :
( ap(c_2Eoption_2ESOME(sK77),sK79) != ap(c_2Eoption_2ESOME(sK77),X0)
| sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)) = X0
| ~ mem(X0,sK77)
| ~ mem(sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77) )
| ~ spl880_147 ),
inference(forward_subsumption_resolution,[],[f20705,f13617]) ).
fof(f20966,definition,
( spl880_178
<=> ! [X0] :
( ap(c_2Eoption_2ESOME(sK77),sK80) != ap(c_2Eoption_2ESOME(sK77),X0)
| ~ mem(X0,sK77)
| sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl880_178])],[avatar_definition]) ).
fof(f20967,plain,
( ! [X0] :
( ap(c_2Eoption_2ESOME(sK77),sK80) != ap(c_2Eoption_2ESOME(sK77),X0)
| ~ mem(X0,sK77)
| sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)) = X0 )
| ~ spl880_178 ),
inference(avatar_component_clause,[],[f20966]) ).
fof(f20969,plain,
( ~ spl880_165
| spl880_178
| ~ spl880_157 ),
inference(avatar_split_clause,[],[f20962,f20464,f20966,f20518]) ).
fof(f20971,definition,
( spl880_179
<=> ! [X0] :
( ap(c_2Eoption_2ESOME(sK77),sK79) != ap(c_2Eoption_2ESOME(sK77),X0)
| ~ mem(X0,sK77)
| sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl880_179])],[avatar_definition]) ).
fof(f20972,plain,
( ! [X0] :
( ap(c_2Eoption_2ESOME(sK77),sK79) != ap(c_2Eoption_2ESOME(sK77),X0)
| ~ mem(X0,sK77)
| sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80)) = X0 )
| ~ spl880_179 ),
inference(avatar_component_clause,[],[f20971]) ).
fof(f20974,plain,
( ~ spl880_158
| spl880_179
| ~ spl880_147 ),
inference(avatar_split_clause,[],[f20964,f20151,f20971,f20478]) ).
fof(f20976,plain,
( ~ mem(sK80,sK77)
| sK80 = sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))
| ~ spl880_178 ),
inference(equality_resolution,[],[f20967]) ).
fof(f20977,plain,
( sK80 = sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))
| ~ spl880_178 ),
inference(forward_subsumption_resolution,[],[f20976,f13620]) ).
fof(f21002,plain,
( ~ mem(sK79,sK77)
| sK79 = sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))
| ~ spl880_179 ),
inference(equality_resolution,[],[f20972]) ).
fof(f21003,plain,
( sK79 = sK242(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))
| ~ spl880_179 ),
inference(forward_subsumption_resolution,[],[f21002,f13619]) ).
fof(f21004,plain,
( p(ap(ap(sK78,sK79),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK79)
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),ap(c_2Eoption_2ESOME(sK77),sK80)))
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK79),ty_2Eoption_2Eoption(sK77))
| ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| ~ ne(sK77)
| ~ ne(sK77)
| ~ spl880_179 ),
inference(superposition,[],[f14793,f21003]) ).
fof(f21007,plain,
( p(ap(ap(sK78,sK79),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))))
| c_2Eoption_2ENONE(sK77) = ap(c_2Eoption_2ESOME(sK77),sK79)
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),ap(c_2Eoption_2ESOME(sK77),sK80)))
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK79),ty_2Eoption_2Eoption(sK77))
| ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| ~ ne(sK77)
| ~ spl880_179 ),
inference(duplicate_literal_removal,[],[f21004]) ).
fof(f21009,plain,
( p(ap(ap(sK78,sK79),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK77,sK77),sK78),ap(c_2Eoption_2ESOME(sK77),sK79)),ap(c_2Eoption_2ESOME(sK77),sK80)))
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK79),ty_2Eoption_2Eoption(sK77))
| ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| ~ ne(sK77)
| spl880_163
| ~ spl880_179 ),
inference(forward_subsumption_resolution,[],[f21007,f20498]) ).
fof(f21011,plain,
( p(ap(ap(sK78,sK79),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))))
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK80),ty_2Eoption_2Eoption(sK77))
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK79),ty_2Eoption_2Eoption(sK77))
| ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| ~ ne(sK77)
| ~ spl880_140
| spl880_163
| ~ spl880_179 ),
inference(forward_subsumption_resolution,[],[f21009,f20069]) ).
fof(f21013,plain,
( p(ap(ap(sK78,sK79),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))))
| ~ mem(ap(c_2Eoption_2ESOME(sK77),sK79),ty_2Eoption_2Eoption(sK77))
| ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| ~ ne(sK77)
| ~ spl880_140
| ~ spl880_148
| spl880_163
| ~ spl880_179 ),
inference(forward_subsumption_resolution,[],[f21011,f20532]) ).
fof(f21015,plain,
( p(ap(ap(sK78,sK79),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))))
| ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| ~ ne(sK77)
| ~ spl880_140
| ~ spl880_148
| ~ spl880_162
| spl880_163
| ~ spl880_179 ),
inference(forward_subsumption_resolution,[],[f21013,f20494]) ).
fof(f21017,plain,
( p(ap(ap(sK78,sK79),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))))
| ~ ne(sK77)
| ~ spl880_140
| ~ spl880_148
| ~ spl880_162
| spl880_163
| ~ spl880_179 ),
inference(forward_subsumption_resolution,[],[f21015,f13618]) ).
fof(f21019,plain,
( p(ap(ap(sK78,sK79),sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),ap(c_2Eoption_2ESOME(sK77),sK80))))
| ~ spl880_140
| ~ spl880_148
| ~ spl880_162
| spl880_163
| ~ spl880_179 ),
inference(forward_subsumption_resolution,[],[f21017,f13617]) ).
fof(f21021,plain,
( p(ap(ap(sK78,sK79),sK80))
| ~ spl880_140
| ~ spl880_148
| ~ spl880_162
| spl880_163
| ~ spl880_178
| ~ spl880_179 ),
inference(forward_demodulation,[],[f21019,f20977]) ).
fof(f21024,plain,
( $false
| ~ spl880_140
| spl880_141
| ~ spl880_148
| ~ spl880_162
| spl880_163
| ~ spl880_178
| ~ spl880_179 ),
inference(forward_subsumption_resolution,[],[f21021,f20084]) ).
fof(f21025,plain,
( ~ spl880_140
| spl880_141
| ~ spl880_148
| ~ spl880_162
| spl880_163
| ~ spl880_178
| ~ spl880_179 ),
inference(avatar_contradiction_clause,[],[f21024]) ).
fof(f21071,plain,
( c_2Eoption_2ENONE(sK77) != c_2Eoption_2ENONE(sK77)
| ~ mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77)),sK77)
| ~ ne(sK77)
| ~ spl880_156 ),
inference(superposition,[],[f14758,f20450]) ).
fof(f21073,plain,
( ~ mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77)),sK77)
| ~ ne(sK77)
| ~ spl880_156 ),
inference(trivial_inequality_removal,[],[f21071]) ).
fof(f21074,plain,
( ~ mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77)),sK77)
| ~ spl880_156 ),
inference(forward_subsumption_resolution,[],[f21073,f13617]) ).
fof(f21077,definition,
( spl880_186
<=> mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77)),sK77) ),
introduced(definition,[new_symbols(definition,[spl880_186])],[avatar_definition]) ).
fof(f21078,plain,
( ~ mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77)),sK77)
| spl880_186 ),
inference(avatar_component_clause,[],[f21077]) ).
fof(f21087,plain,
( ~ spl880_186
| ~ spl880_156 ),
inference(avatar_split_clause,[],[f21074,f20449,f21077]) ).
fof(f21101,plain,
( ~ ne(sK77)
| ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| ~ mem(c_2Eoption_2ENONE(sK77),ty_2Eoption_2Eoption(sK77))
| mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77)),sK77)
| ~ spl880_143
| ~ spl880_177 ),
inference(resolution,[],[f20959,f20078]) ).
fof(f21102,plain,
( ~ ne(sK77)
| ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77)),sK77)
| ~ spl880_143
| ~ spl880_177 ),
inference(forward_subsumption_resolution,[],[f21101,f14778]) ).
fof(f21103,plain,
( ~ mem(sK78,arr(sK77,arr(sK77,bool)))
| mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77)),sK77)
| ~ spl880_143
| ~ spl880_177 ),
inference(forward_subsumption_resolution,[],[f21102,f13617]) ).
fof(f21104,plain,
( mem(sK243(sK77,sK77,sK78,ap(c_2Eoption_2ESOME(sK77),sK79),c_2Eoption_2ENONE(sK77)),sK77)
| ~ spl880_143
| ~ spl880_177 ),
inference(forward_subsumption_resolution,[],[f21103,f13618]) ).
fof(f21105,plain,
( $false
| ~ spl880_143
| ~ spl880_177
| spl880_186 ),
inference(forward_subsumption_resolution,[],[f21104,f21078]) ).
fof(f21106,plain,
( ~ spl880_143
| ~ spl880_177
| spl880_186 ),
inference(avatar_contradiction_clause,[],[f21105]) ).
fof(f21121,plain,
( c_2Eoption_2ENONE(sK77) != c_2Eoption_2ENONE(sK77)
| ~ mem(sK242(sK77,sK77,sK78,c_2Eoption_2ENONE(sK77),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77)
| ~ ne(sK77)
| ~ spl880_150 ),
inference(superposition,[],[f14758,f20419]) ).
fof(f21123,plain,
( ~ mem(sK242(sK77,sK77,sK78,c_2Eoption_2ENONE(sK77),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77)
| ~ ne(sK77)
| ~ spl880_150 ),
inference(trivial_inequality_removal,[],[f21121]) ).
fof(f21137,plain,
( ~ mem(sK242(sK77,sK77,sK78,c_2Eoption_2ENONE(sK77),ap(c_2Eoption_2ESOME(sK77),sK80)),sK77)
| ~ spl880_150 ),
inference(forward_subsumption_resolution,[],[f21123,f13617]) ).
fof(f21143,plain,
( ~ spl880_153
| ~ spl880_150 ),
inference(avatar_split_clause,[],[f21137,f20418,f20431]) ).
fof(f21177,plain,
( c_2Eoption_2ENONE(sK77) != c_2Eoption_2ENONE(sK77)
| ~ mem(sK79,sK77)
| ~ ne(sK77)
| ~ spl880_163 ),
inference(superposition,[],[f14758,f20914]) ).
fof(f21179,plain,
( ~ mem(sK79,sK77)
| ~ ne(sK77)
| ~ spl880_163 ),
inference(trivial_inequality_removal,[],[f21177]) ).
fof(f21182,plain,
( ~ ne(sK77)
| ~ spl880_163 ),
inference(forward_subsumption_resolution,[],[f21179,f13619]) ).
fof(f21189,plain,
( $false
| ~ spl880_163 ),
inference(forward_subsumption_resolution,[],[f21182,f13617]) ).
fof(f21190,plain,
~ spl880_163,
inference(avatar_contradiction_clause,[],[f21189]) ).
cnf(s167,plain,
( spl880_140
| spl880_141
| spl880_142
| spl880_143
| ~ spl880_144 ),
inference(sat_conversion,[],[f20082]) ).
cnf(s168,plain,
( ~ spl880_140
| ~ spl880_141
| spl880_142
| spl880_143
| ~ spl880_144 ),
inference(sat_conversion,[],[f20085]) ).
cnf(s174,plain,
spl880_144,
inference(sat_conversion,[],[f20114]) ).
cnf(s177,plain,
( ~ spl880_140
| spl880_147
| ~ spl880_148 ),
inference(sat_conversion,[],[f20156]) ).
cnf(s179,plain,
spl880_148,
inference(sat_conversion,[],[f20162]) ).
cnf(s180,plain,
( spl880_140
| ~ spl880_141 ),
inference(sat_conversion,[],[f20402]) ).
cnf(s181,plain,
( ~ spl880_142
| ~ spl880_148
| spl880_149
| spl880_150
| ~ spl880_151 ),
inference(sat_conversion,[],[f20423]) ).
cnf(s183,plain,
( ~ spl880_142
| ~ spl880_148
| spl880_149
| spl880_153 ),
inference(sat_conversion,[],[f20433]) ).
cnf(s186,plain,
( ~ spl880_143
| ~ spl880_151
| spl880_156 ),
inference(sat_conversion,[],[f20451]) ).
cnf(s188,plain,
spl880_151,
inference(sat_conversion,[],[f20456]) ).
cnf(s190,plain,
( ~ spl880_140
| ~ spl880_148
| spl880_149
| spl880_157 ),
inference(sat_conversion,[],[f20467]) ).
cnf(s212,plain,
~ spl880_149,
inference(sat_conversion,[],[f20596]) ).
cnf(s252,plain,
spl880_162,
inference(sat_conversion,[],[f20924]) ).
cnf(s253,plain,
( ~ spl880_140
| ~ spl880_148
| spl880_149
| ~ spl880_162
| spl880_165 ),
inference(sat_conversion,[],[f20939]) ).
cnf(s254,plain,
( ~ spl880_140
| ~ spl880_148
| spl880_149
| spl880_158
| ~ spl880_162 ),
inference(sat_conversion,[],[f20940]) ).
cnf(s259,plain,
( ~ spl880_162
| spl880_163
| spl880_177 ),
inference(sat_conversion,[],[f20960]) ).
cnf(s261,plain,
( ~ spl880_157
| ~ spl880_165
| spl880_178 ),
inference(sat_conversion,[],[f20969]) ).
cnf(s263,plain,
( ~ spl880_147
| ~ spl880_158
| spl880_179 ),
inference(sat_conversion,[],[f20974]) ).
cnf(s266,plain,
( ~ spl880_140
| spl880_141
| ~ spl880_148
| ~ spl880_162
| spl880_163
| ~ spl880_178
| ~ spl880_179 ),
inference(sat_conversion,[],[f21025]) ).
cnf(s273,plain,
( ~ spl880_156
| ~ spl880_186 ),
inference(sat_conversion,[],[f21087]) ).
cnf(s275,plain,
( ~ spl880_143
| ~ spl880_177
| spl880_186 ),
inference(sat_conversion,[],[f21106]) ).
cnf(s282,plain,
( ~ spl880_150
| ~ spl880_153 ),
inference(sat_conversion,[],[f21143]) ).
cnf(s288,plain,
~ spl880_163,
inference(sat_conversion,[],[f21190]) ).
cnf(s292,plain,
( ~ spl880_140
| spl880_141
| ~ spl880_148
| ~ spl880_162
| ~ spl880_178
| ~ spl880_179 ),
inference(rat,[],[s266,s288]) ).
cnf(s293,plain,
( ~ spl880_162
| spl880_177 ),
inference(rat,[],[s259,s288]) ).
cnf(s297,plain,
spl880_177,
inference(rat,[],[s293,s252]) ).
cnf(s309,plain,
( ~ spl880_140
| ~ spl880_148
| spl880_157 ),
inference(rat,[],[s190,s212]) ).
cnf(s310,plain,
( ~ spl880_143
| spl880_156 ),
inference(rat,[],[s186,s188]) ).
cnf(s313,plain,
( ~ spl880_142
| ~ spl880_148
| spl880_153 ),
inference(rat,[],[s183,s212]) ).
cnf(s315,plain,
( ~ spl880_142
| ~ spl880_148
| spl880_150 ),
inference(rat,[],[s181,s188,s212]) ).
cnf(s321,plain,
( ~ spl880_140
| spl880_147 ),
inference(rat,[],[s177,s179]) ).
cnf(s323,plain,
( ~ spl880_140
| ~ spl880_141
| spl880_142
| spl880_143 ),
inference(rat,[],[s168,s174]) ).
cnf(s324,plain,
( spl880_140
| spl880_141
| spl880_142
| spl880_143 ),
inference(rat,[],[s167,s174]) ).
cnf(s390,plain,
~ spl880_143,
inference(rat,[],[s273,s310,s275,s297]) ).
cnf(s391,plain,
~ spl880_142,
inference(rat,[],[s282,s315,s313,s179]) ).
cnf(s392,plain,
spl880_140,
inference(rat,[],[s324,s180,s391,s390]) ).
cnf(s393,plain,
spl880_158,
inference(rat,[],[s254,s252,s179,s212,s392]) ).
cnf(s394,plain,
spl880_165,
inference(rat,[],[s253,s179,s252,s212,s392]) ).
cnf(s395,plain,
spl880_157,
inference(rat,[],[s309,s179,s392]) ).
cnf(s396,plain,
spl880_147,
inference(rat,[],[s321,s392]) ).
cnf(s397,plain,
~ spl880_141,
inference(rat,[],[s323,s390,s391,s392]) ).
cnf(s398,plain,
spl880_178,
inference(rat,[],[s261,s394,s395]) ).
cnf(s400,plain,
spl880_179,
inference(rat,[],[s263,s393,s396]) ).
cnf(s402,plain,
$false,
inference(rat,[],[s292,s400,s392,s252,s179,s398,s397]) ).
fof(f21196,plain,
$false,
inference(avatar_sat_refutation,[],[s402]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP011+5 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n010.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 11:57:48 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.53/3.85 % (839121)Detected formulas, will run a generic FOF schedule.
% 11.53/3.85 % (839128)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=1086467559:i=141695:sd=1:nm=32:gsp=on:ss=included_2985 on theBenchmark for (2985ds/141695Mi)
% 11.53/3.85 % (839130)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2122255865:i=119:av=off:ss=axioms_2985 on theBenchmark for (2985ds/119Mi)
% 11.53/3.85 % (839127)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=2922018034:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2985 on theBenchmark for (2985ds/134677Mi)
% 11.53/3.85 % (839126)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=1069059030:i=141193_2985 on theBenchmark for (2985ds/141193Mi)
% 11.53/3.85 % (839131)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2143809229:s2a=on:i=139:gtg=position_2985 on theBenchmark for (2985ds/139Mi)
% 11.53/3.85 % (839132)dis-21_1_sil=8000:lcm=predicate:random_seed=2492607722:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2985 on theBenchmark for (2985ds/129Mi)
% 11.53/3.85 % (839129)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3860550346:i=109:sd=1:ins=1:gsp=on:ss=axioms_2985 on theBenchmark for (2985ds/109Mi)
% 11.53/3.85 % (839131)Instruction limit reached!
% 11.53/3.85 % (839131)------------------------------
% 11.53/3.85 % (839131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/3.85 % (839131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/3.85 % (839131)CaDiCaL version: 2.1.3
% 11.53/3.85 % (839131)Termination reason: Instruction limit
% 11.53/3.85 % (839131)Termination phase: Property scanning
% 11.53/3.85 % (839131)Time elapsed: 0.052 s
% 11.53/3.85 % (839131)Peak memory usage: 107 MB
% 11.53/3.85 % (839131)Instructions burned: 140 (million)
% 11.53/3.85 % (839130)Instruction limit reached!
% 11.53/3.85 % (839130)------------------------------
% 11.53/3.85 % (839130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/3.85 % (839130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/3.85 % (839130)CaDiCaL version: 2.1.3
% 11.53/3.85 % (839130)Termination reason: Instruction limit
% 11.53/3.85 % (839130)Termination phase: Preprocessing 1
% 11.53/3.85 % (839130)Time elapsed: 0.082 s
% 11.53/3.85 % (839130)Peak memory usage: 108 MB
% 11.53/3.85 % (839130)Instructions burned: 119 (million)
% 11.53/3.85 % (839132)Instruction limit reached!
% 11.53/3.85 % (839132)------------------------------
% 11.53/3.85 % (839132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/3.85 % (839132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/3.85 % (839132)CaDiCaL version: 2.1.3
% 11.53/3.85 % (839132)Termination reason: Instruction limit
% 11.53/3.85 % (839132)Termination phase: SInE selection
% 11.53/3.85 % (839132)Time elapsed: 0.076 s
% 11.53/3.85 % (839132)Peak memory usage: 107 MB
% 11.53/3.85 % (839132)Instructions burned: 130 (million)
% 11.53/3.85 % (839129)Instruction limit reached!
% 11.53/3.85 % (839129)------------------------------
% 11.53/3.85 % (839129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/3.85 % (839129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/3.85 % (839129)CaDiCaL version: 2.1.3
% 11.53/3.85 % (839129)Termination reason: Instruction limit
% 11.53/3.85 % (839129)Termination phase: Preprocessing 3
% 11.53/3.85 % (839129)Time elapsed: 0.077 s
% 11.53/3.85 % (839129)Peak memory usage: 109 MB
% 11.53/3.85 % (839129)Instructions burned: 109 (million)
% 11.53/3.85 % (839140)lrs+10_1_sil=8000:sp=occurrence:random_seed=4229097347:i=285:sd=3:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/285Mi)
% 11.53/3.85 % (839141)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3919089015:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/157Mi)
% 11.53/3.85 % (839142)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3216902825:i=325:sd=1:ss=axioms:sgt=32_2982 on theBenchmark for (2982ds/325Mi)
% 11.53/3.85 % (839143)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=2226409294:s2a=on:i=248:s2at=1.23:gtg=position_2982 on theBenchmark for (2982ds/248Mi)
% 11.53/3.85 % (839141)Instruction limit reached!
% 11.53/3.85 % (839141)------------------------------
% 17.61/4.62 % (839141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/4.62 % (839141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/4.62 % (839141)CaDiCaL version: 2.1.3
% 17.61/4.62 % (839141)Termination reason: Instruction limit
% 17.61/4.62 % (839141)Termination phase: Property scanning
% 17.61/4.62 % (839141)Time elapsed: 0.062 s
% 17.61/4.62 % (839141)Peak memory usage: 107 MB
% 17.61/4.62 % (839141)Instructions burned: 159 (million)
% 17.61/4.62 % (839143)Instruction limit reached!
% 17.61/4.62 % (839143)------------------------------
% 17.61/4.62 % (839143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/4.62 % (839143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/4.62 % (839143)CaDiCaL version: 2.1.3
% 17.61/4.62 % (839143)Termination reason: Instruction limit
% 17.61/4.62 % (839143)Termination phase: Property scanning
% 17.61/4.62 % (839143)Time elapsed: 0.092 s
% 17.61/4.62 % (839143)Peak memory usage: 107 MB
% 17.61/4.62 % (839143)Instructions burned: 250 (million)
% 17.61/4.62 % (839140)Instruction limit reached!
% 17.61/4.62 % (839140)------------------------------
% 17.61/4.62 % (839140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/4.62 % (839140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/4.62 % (839140)CaDiCaL version: 2.1.3
% 17.61/4.62 % (839140)Termination reason: Instruction limit
% 17.61/4.62 % (839140)Termination phase: Saturation
% 17.61/4.62 % (839140)Time elapsed: 0.168 s
% 17.61/4.62 % (839140)Peak memory usage: 115 MB
% 17.61/4.62 % (839140)Instructions burned: 287 (million)
% 17.61/4.62 % (839148)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=499884573:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2981 on theBenchmark for (2981ds/294Mi)
% 17.61/4.62 % (839142)Instruction limit reached!
% 17.61/4.62 % (839142)------------------------------
% 17.61/4.62 % (839142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/4.62 % (839142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/4.62 % (839142)CaDiCaL version: 2.1.3
% 17.61/4.62 % (839142)Termination reason: Instruction limit
% 17.61/4.62 % (839142)Termination phase: Saturation
% 17.61/4.62 % (839142)Time elapsed: 0.207 s
% 17.61/4.62 % (839142)Peak memory usage: 115 MB
% 17.61/4.62 % (839142)Instructions burned: 326 (million)
% 17.61/4.62 % (839150)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2361033129:cts=off:i=113:fsr=off:ss=included:sgt=4_2980 on theBenchmark for (2980ds/113Mi)
% 17.61/4.62 % (839149)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3840679341:i=2350_2980 on theBenchmark for (2980ds/2350Mi)
% 17.61/4.62 % (839150)Instruction limit reached!
% 17.61/4.62 % (839150)------------------------------
% 17.61/4.62 % (839150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/4.62 % (839150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/4.62 % (839150)CaDiCaL version: 2.1.3
% 17.61/4.62 % (839150)Termination reason: Instruction limit
% 17.61/4.62 % (839150)Termination phase: Preprocessing 1
% 17.61/4.62 % (839150)Time elapsed: 0.047 s
% 17.61/4.62 % (839150)Peak memory usage: 108 MB
% 17.61/4.62 % (839150)Instructions burned: 114 (million)
% 17.61/4.62 % (839148)Instruction limit reached!
% 17.61/4.62 % (839148)------------------------------
% 17.61/4.62 % (839148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/4.62 % (839148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/4.62 % (839148)CaDiCaL version: 2.1.3
% 17.61/4.62 % (839148)Termination reason: Instruction limit
% 17.61/4.62 % (839148)Termination phase: Saturation
% 17.61/4.62 % (839148)Time elapsed: 0.183 s
% 17.61/4.62 % (839148)Peak memory usage: 114 MB
% 17.61/4.62 % (839148)Instructions burned: 295 (million)
% 17.61/4.62 % (839152)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1654159881:i=127:av=off:fsr=off:sup=off_2979 on theBenchmark for (2979ds/127Mi)
% 17.61/4.62 % (839155)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4064033910:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2978 on theBenchmark for (2978ds/114Mi)
% 17.61/4.62 % (839155)Instruction limit reached!
% 17.61/4.62 % (839155)------------------------------
% 17.61/4.62 % (839155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/4.62 % (839155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/7.03 % (839155)CaDiCaL version: 2.1.3
% 13.06/7.03 % (839155)Termination reason: Instruction limit
% 13.06/7.03 % (839155)Termination phase: Property scanning
% 13.06/7.03 % (839155)Time elapsed: 0.025 s
% 13.06/7.03 % (839155)Peak memory usage: 107 MB
% 13.06/7.03 % (839155)Instructions burned: 116 (million)
% 13.06/7.03 % (839152)Instruction limit reached!
% 13.06/7.03 % (839152)------------------------------
% 13.06/7.03 % (839152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/7.03 % (839152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/7.03 % (839152)CaDiCaL version: 2.1.3
% 13.06/7.03 % (839152)Termination reason: Instruction limit
% 13.06/7.03 % (839152)Termination phase: Preprocessing 1
% 13.06/7.03 % (839152)Time elapsed: 0.089 s
% 13.06/7.03 % (839152)Peak memory usage: 107 MB
% 13.06/7.03 % (839152)Instructions burned: 127 (million)
% 13.06/7.03 % (839157)lrs+10_1_sil=8000:sp=occurrence:random_seed=2061512348:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2977 on theBenchmark for (2977ds/907Mi)
% 13.06/7.03 % (839159)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2840103201:i=437:sd=1:aac=none:ss=included_2977 on theBenchmark for (2977ds/437Mi)
% 13.06/7.03 % (839160)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=588037914:i=5202:ss=axioms:sgt=16_2977 on theBenchmark for (2977ds/5202Mi)
% 13.06/7.03 % (839159)Instruction limit reached!
% 13.06/7.03 % (839159)------------------------------
% 13.06/7.03 % (839159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/7.03 % (839159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/7.03 % (839159)CaDiCaL version: 2.1.3
% 13.06/7.03 % (839159)Termination reason: Instruction limit
% 13.06/7.03 % (839159)Termination phase: Saturation
% 13.06/7.03 % (839159)Time elapsed: 0.137 s
% 13.06/7.03 % (839159)Peak memory usage: 115 MB
% 13.06/7.03 % (839159)Instructions burned: 440 (million)
% 13.06/7.03 % (839164)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2277697461:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2975 on theBenchmark for (2975ds/134Mi)
% 13.06/7.03 % (839164)Instruction limit reached!
% 13.06/7.03 % (839164)------------------------------
% 13.06/7.03 % (839164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/7.03 % (839164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/7.03 % (839164)CaDiCaL version: 2.1.3
% 13.06/7.03 % (839164)Termination reason: Instruction limit
% 13.06/7.03 % (839164)Termination phase: Property scanning
% 13.06/7.03 % (839164)Time elapsed: 0.054 s
% 13.06/7.03 % (839164)Peak memory usage: 110 MB
% 13.06/7.03 % (839164)Instructions burned: 134 (million)
% 13.06/7.03 % (839166)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3087900523:st=8:i=592:sd=3:ep=RST:ss=axioms_2973 on theBenchmark for (2973ds/592Mi)
% 13.06/7.03 % (839157)Instruction limit reached!
% 13.06/7.03 % (839157)------------------------------
% 13.06/7.03 % (839157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/7.03 % (839157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/7.03 % (839157)CaDiCaL version: 2.1.3
% 13.06/7.03 % (839157)Termination reason: Instruction limit
% 13.06/7.03 % (839157)Termination phase: Saturation
% 13.06/7.03 % (839157)Time elapsed: 0.477 s
% 13.06/7.03 % (839157)Peak memory usage: 122 MB
% 13.06/7.03 % (839157)Instructions burned: 907 (million)
% 13.06/7.03 % (839166)Instruction limit reached!
% 13.06/7.03 % (839166)------------------------------
% 13.06/7.03 % (839166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/7.03 % (839166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/7.03 % (839166)CaDiCaL version: 2.1.3
% 13.06/7.03 % (839166)Termination reason: Instruction limit
% 13.06/7.03 % (839166)Termination phase: Preprocessing 3
% 13.06/7.03 % (839166)Time elapsed: 0.197 s
% 13.06/7.03 % (839166)Peak memory usage: 121 MB
% 13.06/7.03 % (839166)Instructions burned: 595 (million)
% 13.06/7.03 % (839168)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4094126538:st=3:i=13193:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/13193Mi)
% 13.06/7.03 % (839169)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=636034405:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/125Mi)
% 13.06/7.03 % (839169)Instruction limit reached!
% 13.06/7.03 % (839169)------------------------------
% 13.06/7.03 % (839169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/7.03 % (839169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/7.03 % (839169)CaDiCaL version: 2.1.3
% 13.06/7.03 % (839169)Termination reason: Instruction limit
% 13.06/7.03 % (839169)Termination phase: Property scanning
% 13.06/7.03 % (839169)Time elapsed: 0.026 s
% 13.06/7.03 % (839169)Peak memory usage: 107 MB
% 13.06/7.03 % (839169)Instructions burned: 127 (million)
% 13.06/7.03 % (839172)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2486663353:i=134:gtgl=5:slsql=off:gtg=exists_sym_2969 on theBenchmark for (2969ds/134Mi)
% 13.06/7.03 % (839172)Instruction limit reached!
% 13.06/7.03 % (839172)------------------------------
% 13.06/7.03 % (839172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/7.03 % (839172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/7.03 % (839172)CaDiCaL version: 2.1.3
% 13.06/7.03 % (839172)Termination reason: Instruction limit
% 13.06/7.03 % (839172)Termination phase: Property scanning
% 13.06/7.03 % (839172)Time elapsed: 0.029 s
% 13.06/7.03 % (839172)Peak memory usage: 107 MB
% 13.06/7.03 % (839172)Instructions burned: 137 (million)
% 13.06/7.03 % (839174)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2282281173:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/141Mi)
% 13.06/7.03 % (839174)Instruction limit reached!
% 13.06/7.03 % (839174)------------------------------
% 13.06/7.03 % (839174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/7.03 % (839174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/7.03 % (839174)CaDiCaL version: 2.1.3
% 13.06/7.03 % (839174)Termination reason: Instruction limit
% 13.06/7.03 % (839174)Termination phase: General splitting
% 13.06/7.03 % (839174)Time elapsed: 0.056 s
% 13.06/7.03 % (839174)Peak memory usage: 110 MB
% 13.06/7.03 % (839174)Instructions burned: 144 (million)
% 13.06/7.03 % (839176)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3645416294:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2967 on theBenchmark for (2967ds/431Mi)
% 13.06/7.03 % (839149)Instruction limit reached!
% 13.06/7.03 % (839149)------------------------------
% 13.06/7.03 % (839149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/7.03 % (839149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/7.03 % (839149)CaDiCaL version: 2.1.3
% 13.06/7.03 % (839149)Termination reason: Instruction limit
% 13.06/7.03 % (839149)Termination phase: Property scanning
% 13.06/7.03 % (839149)Time elapsed: 1.320 s
% 13.06/7.03 % (839149)Peak memory usage: 164 MB
% 13.06/7.03 % (839149)Instructions burned: 2350 (million)
% 13.06/7.03 % (839176)Instruction limit reached!
% 13.06/7.03 % (839176)------------------------------
% 13.06/7.03 % (839176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/7.03 % (839176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/7.03 % (839176)CaDiCaL version: 2.1.3
% 13.06/7.03 % (839176)Termination reason: Instruction limit
% 13.06/7.03 % (839176)Termination phase: Saturation
% 13.06/7.03 % (839176)Time elapsed: 0.141 s
% 13.06/7.03 % (839176)Peak memory usage: 116 MB
% 13.06/7.03 % (839176)Instructions burned: 435 (million)
% 13.06/7.03 % (839178)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2450104534:i=6060:aac=none:ins=25_2965 on theBenchmark for (2965ds/6060Mi)
% 13.06/7.03 % (839179)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=12496885:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2964 on theBenchmark for (2964ds/150Mi)
% 13.06/7.03 % (839179)Instruction limit reached!
% 13.06/7.03 % (839179)------------------------------
% 13.06/7.03 % (839179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/7.03 % (839179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/7.03 % (839179)CaDiCaL version: 2.1.3
% 13.06/7.03 % (839179)Termination reason: Instruction limit
% 13.06/7.03 % (839179)Termination phase: Preprocessing 1
% 13.06/7.03 % (839179)Time elapsed: 0.062 s
% 13.06/7.03 % (839179)Peak memory usage: 108 MB
% 13.06/7.03 % (839179)Instructions burned: 152 (million)
% 13.06/7.03 % (839182)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2334615739:i=14155:bd=all_2963 on theBenchmark for (2963ds/14155Mi)
% 13.06/7.03 % (839127)First to succeed.
% 13.06/7.03 % (839127)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-839121"
% 13.06/7.03 % (839127)Refutation found. Thanks to Tanya!
% 13.06/7.03 % SZS status Theorem for theBenchmark
% 13.06/7.03 % SZS output start Proof for theBenchmark
% See solution above
% 35.11/7.26 % (839127)------------------------------
% 35.11/7.26 % (839127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.11/7.26 % (839127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.11/7.26 % (839127)CaDiCaL version: 2.1.3
% 35.11/7.26 % (839127)Termination reason: Refutation
% 35.11/7.26 % (839127)Time elapsed: 4.014 s
% 35.11/7.26 % (839127)Peak memory usage: 232 MB
% 35.11/7.26 % (839127)Instructions burned: 5875 (million)
% 35.11/7.26 % (839127)------------------------------
% 35.11/7.26 % (839127)------------------------------
% 35.11/7.26 % (839121)Success in time 6.192 s
% 35.11/7.26 % Vampire exiting
%------------------------------------------------------------------------------