%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP011+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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:34:56 AM UTC 2026
% Result : Theorem 234.08s 39.51s
% Output : Refutation 234.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 42
% Syntax : Number of formulae : 309 ( 41 unt; 29 def)
% Number of atoms : 1465 ( 238 equ)
% Maximal formula atoms : 57 ( 4 avg)
% Number of connectives : 1908 ( 752 ~; 746 |; 222 &)
% ( 60 <=>; 127 =>; 0 <=; 1 <~>)
% Maximal formula depth : 35 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 35 ( 32 usr; 26 prp; 0-5 aty)
% Number of functors : 21 ( 21 usr; 6 con; 0-5 aty)
% Number of variables : 599 ( 0 sgn 577 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
ne(bool),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',bool_ne) ).
fof(f3,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ne(arr(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',arr_ne) ).
fof(f4,axiom,
! [X0,X1,X2] :
( mem(X2,arr(X0,X1))
=> ! [X3] :
( mem(X3,X0)
=> mem(ap(X2,X3),X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',ap_tp) ).
fof(f9,axiom,
! [X0] :
( ne(X0)
=> ne(ty_2Eoption_2Eoption(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ne_ty_2Eoption_2Eoption) ).
fof(f18,axiom,
mem(c_2Ebool_2ET,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2ET) ).
fof(f19,axiom,
p(c_2Ebool_2ET),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_true_p) ).
fof(f23,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Eoption_2ETHE(X0),arr(ty_2Eoption_2Eoption(X0),X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Eoption_2ETHE) ).
fof(f24,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Eoption_2ESOME(X0),arr(X0,ty_2Eoption_2Eoption(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Eoption_2ESOME) ).
fof(f27,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Eoption_2ENONE) ).
fof(f40,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,bool)
=> ( ? [X2] :
( mem(X2,X0)
& p(X1) )
<=> p(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ebool_2EEXISTS__SIMP) ).
fof(f46,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( mem(X2,X1)
=> ! [X3] :
( mem(X3,arr(X0,X1))
=> ! [X4] :
( mem(X4,ty_2Eoption_2Eoption(X0))
=> ( ! [X5] :
( mem(X5,X0)
=> ! [X6] :
( mem(X6,X0)
=> ( ap(c_2Eoption_2ESOME(X0),X5) = ap(c_2Eoption_2ESOME(X0),X6)
<=> X5 = X6 ) ) )
& ! [X7] :
( mem(X7,X0)
=> ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X7)) = X7 )
& ! [X8] :
( mem(X8,X0)
=> c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X8) )
& ! [X9] :
( mem(X9,X0)
=> ap(c_2Eoption_2ESOME(X0),X9) != c_2Eoption_2ENONE(X0) )
& ! [X10] :
( mem(X10,X0)
=> ( p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X10)))
<=> $true ) )
& ( p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0)))
<=> $false )
& ! [X11] :
( mem(X11,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__NONE(X0),X11))
<=> X11 = c_2Eoption_2ENONE(X0) ) )
& ! [X12] :
( mem(X12,ty_2Eoption_2Eoption(X0))
=> ( ~ p(ap(c_2Eoption_2EIS__SOME(X0),X12))
<=> X12 = c_2Eoption_2ENONE(X0) ) )
& ! [X13] :
( mem(X13,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__SOME(X0),X13))
=> ap(c_2Eoption_2ESOME(X0),ap(c_2Eoption_2ETHE(X0),X13)) = X13 ) )
& ! [X14] :
( mem(X14,ty_2Eoption_2Eoption(X0))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X14),c_2Eoption_2ENONE(X0)),c_2Eoption_2ESOME(X0)) = X14 )
& ! [X15] :
( mem(X15,ty_2Eoption_2Eoption(X0))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X15),X15),c_2Eoption_2ESOME(X0)) = X15 )
& ! [X16] :
( mem(X16,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__NONE(X0),X16))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X16),X2),X3) = X2 ) )
& ! [X17] :
( mem(X17,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__SOME(X0),X17))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X17),X2),X3) = ap(X3,ap(c_2Eoption_2ETHE(X0),X17)) ) )
& ! [X18] :
( mem(X18,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__SOME(X0),X18))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X18),X4),c_2Eoption_2ESOME(X0)) = X18 ) )
& ! [X19] :
( mem(X19,X1)
=> ! [X20] :
( mem(X20,arr(X0,X1))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),c_2Eoption_2ENONE(X0)),X19),X20) = X19 ) )
& ! [X21] :
( mem(X21,X0)
=> ! [X22] :
( mem(X22,X1)
=> ! [X23] :
( mem(X23,arr(X0,X1))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),ap(c_2Eoption_2ESOME(X0),X21)),X22),X23) = ap(X23,X21) ) ) )
& ! [X24] :
( mem(X24,arr(X0,X1))
=> ! [X25] :
( mem(X25,X0)
=> ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X24),ap(c_2Eoption_2ESOME(X0),X25)) = ap(c_2Eoption_2ESOME(X1),ap(X24,X25)) ) )
& ! [X26] :
( mem(X26,arr(X0,X1))
=> ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X26),c_2Eoption_2ENONE(X0)) = c_2Eoption_2ENONE(X1) )
& ap(c_2Eoption_2EOPTION__JOIN(X0),c_2Eoption_2ENONE(ty_2Eoption_2Eoption(X0))) = c_2Eoption_2ENONE(X0)
& ! [X27] :
( mem(X27,ty_2Eoption_2Eoption(X0))
=> ap(c_2Eoption_2EOPTION__JOIN(X0),ap(c_2Eoption_2ESOME(ty_2Eoption_2Eoption(X0)),X27)) = X27 ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eoption_2Eoption__CLAUSES) ).
fof(f47,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/sandbox2/benchmark/theBenchmark.p',ax_thm_2Eoption_2EOPTREL__def) ).
fof(f48,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/sandbox2/benchmark/theBenchmark.p',conj_thm_2Equotient__option_2EOPTION__REL__def) ).
fof(f49,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)],[f48]) ).
fof(f57,plain,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( mem(X2,X1)
=> ! [X3] :
( mem(X3,arr(X0,X1))
=> ! [X4] :
( mem(X4,ty_2Eoption_2Eoption(X0))
=> ( ! [X5] :
( mem(X5,X0)
=> ! [X6] :
( mem(X6,X0)
=> ( ap(c_2Eoption_2ESOME(X0),X5) = ap(c_2Eoption_2ESOME(X0),X6)
<=> X5 = X6 ) ) )
& ! [X7] :
( mem(X7,X0)
=> ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X7)) = X7 )
& ! [X8] :
( mem(X8,X0)
=> c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X8) )
& ! [X9] :
( mem(X9,X0)
=> ap(c_2Eoption_2ESOME(X0),X9) != c_2Eoption_2ENONE(X0) )
& ! [X10] :
( mem(X10,X0)
=> p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X10))) )
& ~ p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0)))
& ! [X11] :
( mem(X11,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__NONE(X0),X11))
<=> X11 = c_2Eoption_2ENONE(X0) ) )
& ! [X12] :
( mem(X12,ty_2Eoption_2Eoption(X0))
=> ( ~ p(ap(c_2Eoption_2EIS__SOME(X0),X12))
<=> X12 = c_2Eoption_2ENONE(X0) ) )
& ! [X13] :
( mem(X13,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__SOME(X0),X13))
=> ap(c_2Eoption_2ESOME(X0),ap(c_2Eoption_2ETHE(X0),X13)) = X13 ) )
& ! [X14] :
( mem(X14,ty_2Eoption_2Eoption(X0))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X14),c_2Eoption_2ENONE(X0)),c_2Eoption_2ESOME(X0)) = X14 )
& ! [X15] :
( mem(X15,ty_2Eoption_2Eoption(X0))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X15),X15),c_2Eoption_2ESOME(X0)) = X15 )
& ! [X16] :
( mem(X16,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__NONE(X0),X16))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X16),X2),X3) = X2 ) )
& ! [X17] :
( mem(X17,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__SOME(X0),X17))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X17),X2),X3) = ap(X3,ap(c_2Eoption_2ETHE(X0),X17)) ) )
& ! [X18] :
( mem(X18,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__SOME(X0),X18))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X18),X4),c_2Eoption_2ESOME(X0)) = X18 ) )
& ! [X19] :
( mem(X19,X1)
=> ! [X20] :
( mem(X20,arr(X0,X1))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),c_2Eoption_2ENONE(X0)),X19),X20) = X19 ) )
& ! [X21] :
( mem(X21,X0)
=> ! [X22] :
( mem(X22,X1)
=> ! [X23] :
( mem(X23,arr(X0,X1))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),ap(c_2Eoption_2ESOME(X0),X21)),X22),X23) = ap(X23,X21) ) ) )
& ! [X24] :
( mem(X24,arr(X0,X1))
=> ! [X25] :
( mem(X25,X0)
=> ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X24),ap(c_2Eoption_2ESOME(X0),X25)) = ap(c_2Eoption_2ESOME(X1),ap(X24,X25)) ) )
& ! [X26] :
( mem(X26,arr(X0,X1))
=> ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X26),c_2Eoption_2ENONE(X0)) = c_2Eoption_2ENONE(X1) )
& ap(c_2Eoption_2EOPTION__JOIN(X0),c_2Eoption_2ENONE(ty_2Eoption_2Eoption(X0))) = c_2Eoption_2ENONE(X0)
& ! [X27] :
( mem(X27,ty_2Eoption_2Eoption(X0))
=> ap(c_2Eoption_2EOPTION__JOIN(X0),ap(c_2Eoption_2ESOME(ty_2Eoption_2Eoption(X0)),X27)) = X27 ) ) ) ) ) ) ),
inference(true_and_false_elimination,[],[f46]) ).
fof(f58,plain,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( mem(X2,X1)
=> ! [X3] :
( mem(X3,arr(X0,X1))
=> ! [X4] :
( mem(X4,ty_2Eoption_2Eoption(X0))
=> ( ! [X5] :
( mem(X5,X0)
=> ! [X6] :
( mem(X6,X0)
=> ( ap(c_2Eoption_2ESOME(X0),X5) = ap(c_2Eoption_2ESOME(X0),X6)
<=> X5 = X6 ) ) )
& ! [X7] :
( mem(X7,X0)
=> ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X7)) = X7 )
& ! [X8] :
( mem(X8,X0)
=> c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X8) )
& ! [X9] :
( mem(X9,X0)
=> ap(c_2Eoption_2ESOME(X0),X9) != c_2Eoption_2ENONE(X0) )
& ! [X10] :
( mem(X10,X0)
=> p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X10))) )
& ~ p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0)))
& ! [X11] :
( mem(X11,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__NONE(X0),X11))
<=> X11 = c_2Eoption_2ENONE(X0) ) )
& ! [X12] :
( mem(X12,ty_2Eoption_2Eoption(X0))
=> ( ~ p(ap(c_2Eoption_2EIS__SOME(X0),X12))
<=> X12 = c_2Eoption_2ENONE(X0) ) )
& ! [X13] :
( mem(X13,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__SOME(X0),X13))
=> ap(c_2Eoption_2ESOME(X0),ap(c_2Eoption_2ETHE(X0),X13)) = X13 ) )
& ! [X14] :
( mem(X14,ty_2Eoption_2Eoption(X0))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X14),c_2Eoption_2ENONE(X0)),c_2Eoption_2ESOME(X0)) = X14 )
& ! [X15] :
( mem(X15,ty_2Eoption_2Eoption(X0))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X15),X15),c_2Eoption_2ESOME(X0)) = X15 )
& ! [X16] :
( mem(X16,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__NONE(X0),X16))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X16),X2),X3) = X2 ) )
& ! [X17] :
( mem(X17,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__SOME(X0),X17))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X17),X2),X3) = ap(X3,ap(c_2Eoption_2ETHE(X0),X17)) ) )
& ! [X18] :
( mem(X18,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__SOME(X0),X18))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X18),X4),c_2Eoption_2ESOME(X0)) = X18 ) )
& ! [X19] :
( mem(X19,X1)
=> ! [X20] :
( mem(X20,arr(X0,X1))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),c_2Eoption_2ENONE(X0)),X19),X20) = X19 ) )
& ! [X21] :
( mem(X21,X0)
=> ! [X22] :
( mem(X22,X1)
=> ! [X23] :
( mem(X23,arr(X0,X1))
=> ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),ap(c_2Eoption_2ESOME(X0),X21)),X22),X23) = ap(X23,X21) ) ) )
& ! [X24] :
( mem(X24,arr(X0,X1))
=> ! [X25] :
( mem(X25,X0)
=> ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X24),ap(c_2Eoption_2ESOME(X0),X25)) = ap(c_2Eoption_2ESOME(X1),ap(X24,X25)) ) )
& ! [X26] :
( mem(X26,arr(X0,X1))
=> ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X26),c_2Eoption_2ENONE(X0)) = c_2Eoption_2ENONE(X1) )
& ap(c_2Eoption_2EOPTION__JOIN(X0),c_2Eoption_2ENONE(ty_2Eoption_2Eoption(X0))) = c_2Eoption_2ENONE(X0)
& ! [X27] :
( mem(X27,ty_2Eoption_2Eoption(X0))
=> ap(c_2Eoption_2EOPTION__JOIN(X0),ap(c_2Eoption_2ESOME(ty_2Eoption_2Eoption(X0)),X27)) = X27 ) ) ) ) ) ) ),
inference(flattening,[],[f57]) ).
fof(f59,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,[],[f49]) ).
fof(f60,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,[],[f59]) ).
fof(f61,plain,
! [X0] :
( ! [X1] :
( ne(arr(X0,X1))
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f62,plain,
! [X0,X1,X2] :
( ! [X3] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f69,plain,
! [X0] :
( ne(ty_2Eoption_2Eoption(X0))
| ~ ne(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f77,plain,
! [X0] :
( mem(c_2Eoption_2ETHE(X0),arr(ty_2Eoption_2Eoption(X0),X0))
| ~ ne(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f78,plain,
! [X0] :
( mem(c_2Eoption_2ESOME(X0),arr(X0,ty_2Eoption_2Eoption(X0)))
| ~ ne(X0) ),
inference(ennf_transformation,[],[f24]) ).
fof(f81,plain,
! [X0] :
( mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0))
| ~ ne(X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f91,plain,
! [X0] :
( ! [X1] :
( ( ? [X2] :
( mem(X2,X0)
& p(X1) )
<=> p(X1) )
| ~ mem(X1,bool) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f40]) ).
fof(f97,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( ! [X5] :
( ! [X6] :
( ( ap(c_2Eoption_2ESOME(X0),X5) = ap(c_2Eoption_2ESOME(X0),X6)
<=> X5 = X6 )
| ~ mem(X6,X0) )
| ~ mem(X5,X0) )
& ! [X7] :
( ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X7)) = X7
| ~ mem(X7,X0) )
& ! [X8] :
( c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X8)
| ~ mem(X8,X0) )
& ! [X9] :
( ap(c_2Eoption_2ESOME(X0),X9) != c_2Eoption_2ENONE(X0)
| ~ mem(X9,X0) )
& ! [X10] :
( p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X10)))
| ~ mem(X10,X0) )
& ~ p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0)))
& ! [X11] :
( ( p(ap(c_2Eoption_2EIS__NONE(X0),X11))
<=> X11 = c_2Eoption_2ENONE(X0) )
| ~ mem(X11,ty_2Eoption_2Eoption(X0)) )
& ! [X12] :
( ( ~ p(ap(c_2Eoption_2EIS__SOME(X0),X12))
<=> X12 = c_2Eoption_2ENONE(X0) )
| ~ mem(X12,ty_2Eoption_2Eoption(X0)) )
& ! [X13] :
( ap(c_2Eoption_2ESOME(X0),ap(c_2Eoption_2ETHE(X0),X13)) = X13
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X13))
| ~ mem(X13,ty_2Eoption_2Eoption(X0)) )
& ! [X14] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X14),c_2Eoption_2ENONE(X0)),c_2Eoption_2ESOME(X0)) = X14
| ~ mem(X14,ty_2Eoption_2Eoption(X0)) )
& ! [X15] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X15),X15),c_2Eoption_2ESOME(X0)) = X15
| ~ mem(X15,ty_2Eoption_2Eoption(X0)) )
& ! [X16] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X16),X2),X3) = X2
| ~ p(ap(c_2Eoption_2EIS__NONE(X0),X16))
| ~ mem(X16,ty_2Eoption_2Eoption(X0)) )
& ! [X17] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X17),X2),X3) = ap(X3,ap(c_2Eoption_2ETHE(X0),X17))
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X17))
| ~ mem(X17,ty_2Eoption_2Eoption(X0)) )
& ! [X18] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X18),X4),c_2Eoption_2ESOME(X0)) = X18
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X18))
| ~ mem(X18,ty_2Eoption_2Eoption(X0)) )
& ! [X19] :
( ! [X20] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),c_2Eoption_2ENONE(X0)),X19),X20) = X19
| ~ mem(X20,arr(X0,X1)) )
| ~ mem(X19,X1) )
& ! [X21] :
( ! [X22] :
( ! [X23] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),ap(c_2Eoption_2ESOME(X0),X21)),X22),X23) = ap(X23,X21)
| ~ mem(X23,arr(X0,X1)) )
| ~ mem(X22,X1) )
| ~ mem(X21,X0) )
& ! [X24] :
( ! [X25] :
( ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X24),ap(c_2Eoption_2ESOME(X0),X25)) = ap(c_2Eoption_2ESOME(X1),ap(X24,X25))
| ~ mem(X25,X0) )
| ~ mem(X24,arr(X0,X1)) )
& ! [X26] :
( ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X26),c_2Eoption_2ENONE(X0)) = c_2Eoption_2ENONE(X1)
| ~ mem(X26,arr(X0,X1)) )
& ap(c_2Eoption_2EOPTION__JOIN(X0),c_2Eoption_2ENONE(ty_2Eoption_2Eoption(X0))) = c_2Eoption_2ENONE(X0)
& ! [X27] :
( ap(c_2Eoption_2EOPTION__JOIN(X0),ap(c_2Eoption_2ESOME(ty_2Eoption_2Eoption(X0)),X27)) = X27
| ~ mem(X27,ty_2Eoption_2Eoption(X0)) ) )
| ~ mem(X4,ty_2Eoption_2Eoption(X0)) )
| ~ mem(X3,arr(X0,X1)) )
| ~ mem(X2,X1) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f58]) ).
fof(f98,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( ! [X5] :
( ! [X6] :
( ( ap(c_2Eoption_2ESOME(X0),X5) = ap(c_2Eoption_2ESOME(X0),X6)
<=> X5 = X6 )
| ~ mem(X6,X0) )
| ~ mem(X5,X0) )
& ! [X7] :
( ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X7)) = X7
| ~ mem(X7,X0) )
& ! [X8] :
( c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X8)
| ~ mem(X8,X0) )
& ! [X9] :
( ap(c_2Eoption_2ESOME(X0),X9) != c_2Eoption_2ENONE(X0)
| ~ mem(X9,X0) )
& ! [X10] :
( p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X10)))
| ~ mem(X10,X0) )
& ~ p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0)))
& ! [X11] :
( ( p(ap(c_2Eoption_2EIS__NONE(X0),X11))
<=> X11 = c_2Eoption_2ENONE(X0) )
| ~ mem(X11,ty_2Eoption_2Eoption(X0)) )
& ! [X12] :
( ( ~ p(ap(c_2Eoption_2EIS__SOME(X0),X12))
<=> X12 = c_2Eoption_2ENONE(X0) )
| ~ mem(X12,ty_2Eoption_2Eoption(X0)) )
& ! [X13] :
( ap(c_2Eoption_2ESOME(X0),ap(c_2Eoption_2ETHE(X0),X13)) = X13
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X13))
| ~ mem(X13,ty_2Eoption_2Eoption(X0)) )
& ! [X14] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X14),c_2Eoption_2ENONE(X0)),c_2Eoption_2ESOME(X0)) = X14
| ~ mem(X14,ty_2Eoption_2Eoption(X0)) )
& ! [X15] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X15),X15),c_2Eoption_2ESOME(X0)) = X15
| ~ mem(X15,ty_2Eoption_2Eoption(X0)) )
& ! [X16] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X16),X2),X3) = X2
| ~ p(ap(c_2Eoption_2EIS__NONE(X0),X16))
| ~ mem(X16,ty_2Eoption_2Eoption(X0)) )
& ! [X17] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X17),X2),X3) = ap(X3,ap(c_2Eoption_2ETHE(X0),X17))
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X17))
| ~ mem(X17,ty_2Eoption_2Eoption(X0)) )
& ! [X18] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X18),X4),c_2Eoption_2ESOME(X0)) = X18
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X18))
| ~ mem(X18,ty_2Eoption_2Eoption(X0)) )
& ! [X19] :
( ! [X20] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),c_2Eoption_2ENONE(X0)),X19),X20) = X19
| ~ mem(X20,arr(X0,X1)) )
| ~ mem(X19,X1) )
& ! [X21] :
( ! [X22] :
( ! [X23] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),ap(c_2Eoption_2ESOME(X0),X21)),X22),X23) = ap(X23,X21)
| ~ mem(X23,arr(X0,X1)) )
| ~ mem(X22,X1) )
| ~ mem(X21,X0) )
& ! [X24] :
( ! [X25] :
( ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X24),ap(c_2Eoption_2ESOME(X0),X25)) = ap(c_2Eoption_2ESOME(X1),ap(X24,X25))
| ~ mem(X25,X0) )
| ~ mem(X24,arr(X0,X1)) )
& ! [X26] :
( ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X26),c_2Eoption_2ENONE(X0)) = c_2Eoption_2ENONE(X1)
| ~ mem(X26,arr(X0,X1)) )
& ap(c_2Eoption_2EOPTION__JOIN(X0),c_2Eoption_2ENONE(ty_2Eoption_2Eoption(X0))) = c_2Eoption_2ENONE(X0)
& ! [X27] :
( ap(c_2Eoption_2EOPTION__JOIN(X0),ap(c_2Eoption_2ESOME(ty_2Eoption_2Eoption(X0)),X27)) = X27
| ~ mem(X27,ty_2Eoption_2Eoption(X0)) ) )
| ~ mem(X4,ty_2Eoption_2Eoption(X0)) )
| ~ mem(X3,arr(X0,X1)) )
| ~ mem(X2,X1) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(flattening,[],[f97]) ).
fof(f99,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,[],[f47]) ).
fof(f100,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,[],[f60]) ).
fof(f101,definition,
! [X0] :
( ! [X12] :
( ( ~ p(ap(c_2Eoption_2EIS__SOME(X0),X12))
<=> X12 = c_2Eoption_2ENONE(X0) )
| ~ mem(X12,ty_2Eoption_2Eoption(X0)) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f102,definition,
! [X0] :
( ! [X11] :
( ( p(ap(c_2Eoption_2EIS__NONE(X0),X11))
<=> X11 = c_2Eoption_2ENONE(X0) )
| ~ mem(X11,ty_2Eoption_2Eoption(X0)) )
| ~ sP1(X0) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f103,definition,
! [X0] :
( ! [X5] :
( ! [X6] :
( ( ap(c_2Eoption_2ESOME(X0),X5) = ap(c_2Eoption_2ESOME(X0),X6)
<=> X5 = X6 )
| ~ mem(X6,X0) )
| ~ mem(X5,X0) )
| ~ sP2(X0) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f104,definition,
! [X0,X2,X3,X1,X4] :
( ( sP2(X0)
& ! [X7] :
( ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X7)) = X7
| ~ mem(X7,X0) )
& ! [X8] :
( c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X8)
| ~ mem(X8,X0) )
& ! [X9] :
( ap(c_2Eoption_2ESOME(X0),X9) != c_2Eoption_2ENONE(X0)
| ~ mem(X9,X0) )
& ! [X10] :
( p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X10)))
| ~ mem(X10,X0) )
& ~ p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0)))
& sP1(X0)
& sP0(X0)
& ! [X13] :
( ap(c_2Eoption_2ESOME(X0),ap(c_2Eoption_2ETHE(X0),X13)) = X13
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X13))
| ~ mem(X13,ty_2Eoption_2Eoption(X0)) )
& ! [X14] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X14),c_2Eoption_2ENONE(X0)),c_2Eoption_2ESOME(X0)) = X14
| ~ mem(X14,ty_2Eoption_2Eoption(X0)) )
& ! [X15] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X15),X15),c_2Eoption_2ESOME(X0)) = X15
| ~ mem(X15,ty_2Eoption_2Eoption(X0)) )
& ! [X16] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X16),X2),X3) = X2
| ~ p(ap(c_2Eoption_2EIS__NONE(X0),X16))
| ~ mem(X16,ty_2Eoption_2Eoption(X0)) )
& ! [X17] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X17),X2),X3) = ap(X3,ap(c_2Eoption_2ETHE(X0),X17))
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X17))
| ~ mem(X17,ty_2Eoption_2Eoption(X0)) )
& ! [X18] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X18),X4),c_2Eoption_2ESOME(X0)) = X18
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X18))
| ~ mem(X18,ty_2Eoption_2Eoption(X0)) )
& ! [X19] :
( ! [X20] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),c_2Eoption_2ENONE(X0)),X19),X20) = X19
| ~ mem(X20,arr(X0,X1)) )
| ~ mem(X19,X1) )
& ! [X21] :
( ! [X22] :
( ! [X23] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),ap(c_2Eoption_2ESOME(X0),X21)),X22),X23) = ap(X23,X21)
| ~ mem(X23,arr(X0,X1)) )
| ~ mem(X22,X1) )
| ~ mem(X21,X0) )
& ! [X24] :
( ! [X25] :
( ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X24),ap(c_2Eoption_2ESOME(X0),X25)) = ap(c_2Eoption_2ESOME(X1),ap(X24,X25))
| ~ mem(X25,X0) )
| ~ mem(X24,arr(X0,X1)) )
& ! [X26] :
( ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X26),c_2Eoption_2ENONE(X0)) = c_2Eoption_2ENONE(X1)
| ~ mem(X26,arr(X0,X1)) )
& ap(c_2Eoption_2EOPTION__JOIN(X0),c_2Eoption_2ENONE(ty_2Eoption_2Eoption(X0))) = c_2Eoption_2ENONE(X0)
& ! [X27] :
( ap(c_2Eoption_2EOPTION__JOIN(X0),ap(c_2Eoption_2ESOME(ty_2Eoption_2Eoption(X0)),X27)) = X27
| ~ mem(X27,ty_2Eoption_2Eoption(X0)) ) )
| ~ sP3(X0,X2,X3,X1,X4) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f105,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( sP3(X0,X2,X3,X1,X4)
| ~ mem(X4,ty_2Eoption_2Eoption(X0)) )
| ~ mem(X3,arr(X0,X1)) )
| ~ mem(X2,X1) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(definition_folding,[],[f98,f104,f103,f102,f101]) ).
fof(f106,definition,
! [X0,X1,X3,X4,X2] :
( sP4(X0,X1,X3,X4,X2)
<=> ? [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)) ) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f107,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) )
| sP4(X0,X1,X3,X4,X2) ) )
| ~ mem(X4,ty_2Eoption_2Eoption(X1)) )
| ~ mem(X3,ty_2Eoption_2Eoption(X0)) )
| ~ mem(X2,arr(X0,arr(X1,bool))) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(definition_folding,[],[f99,f106]) ).
fof(f125,plain,
! [X0] :
( ! [X1] :
( ( ( ? [X2] :
( mem(X2,X0)
& p(X1) )
| ~ p(X1) )
& ( p(X1)
| ! [X2] :
( ~ mem(X2,X0)
| ~ p(X1) ) ) )
| ~ mem(X1,bool) )
| ~ ne(X0) ),
inference(nnf_transformation,[],[f91]) ).
fof(f126,plain,
! [X0] :
( ! [X1] :
( ( ( ? [X2] :
( mem(X2,X0)
& p(X1) )
| ~ p(X1) )
& ( p(X1)
| ! [X3] :
( ~ mem(X3,X0)
| ~ p(X1) ) ) )
| ~ mem(X1,bool) )
| ~ ne(X0) ),
inference(rectify,[],[f125]) ).
fof(f127,plain,
! [X0] :
( ! [X1] :
( ( ( ( mem(sK8(X0,X1),X0)
& p(X1) )
| ~ p(X1) )
& ( p(X1)
| ! [X3] :
( ~ mem(X3,X0)
| ~ p(X1) ) ) )
| ~ mem(X1,bool) )
| ~ ne(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X2,sK8(X0,X1))],[f126]) ).
fof(f135,plain,
! [X0,X2,X3,X1,X4] :
( ( sP2(X0)
& ! [X7] :
( ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X7)) = X7
| ~ mem(X7,X0) )
& ! [X8] :
( c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X8)
| ~ mem(X8,X0) )
& ! [X9] :
( ap(c_2Eoption_2ESOME(X0),X9) != c_2Eoption_2ENONE(X0)
| ~ mem(X9,X0) )
& ! [X10] :
( p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X10)))
| ~ mem(X10,X0) )
& ~ p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0)))
& sP1(X0)
& sP0(X0)
& ! [X13] :
( ap(c_2Eoption_2ESOME(X0),ap(c_2Eoption_2ETHE(X0),X13)) = X13
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X13))
| ~ mem(X13,ty_2Eoption_2Eoption(X0)) )
& ! [X14] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X14),c_2Eoption_2ENONE(X0)),c_2Eoption_2ESOME(X0)) = X14
| ~ mem(X14,ty_2Eoption_2Eoption(X0)) )
& ! [X15] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X15),X15),c_2Eoption_2ESOME(X0)) = X15
| ~ mem(X15,ty_2Eoption_2Eoption(X0)) )
& ! [X16] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X16),X2),X3) = X2
| ~ p(ap(c_2Eoption_2EIS__NONE(X0),X16))
| ~ mem(X16,ty_2Eoption_2Eoption(X0)) )
& ! [X17] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),X17),X2),X3) = ap(X3,ap(c_2Eoption_2ETHE(X0),X17))
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X17))
| ~ mem(X17,ty_2Eoption_2Eoption(X0)) )
& ! [X18] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X18),X4),c_2Eoption_2ESOME(X0)) = X18
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X18))
| ~ mem(X18,ty_2Eoption_2Eoption(X0)) )
& ! [X19] :
( ! [X20] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),c_2Eoption_2ENONE(X0)),X19),X20) = X19
| ~ mem(X20,arr(X0,X1)) )
| ~ mem(X19,X1) )
& ! [X21] :
( ! [X22] :
( ! [X23] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),ap(c_2Eoption_2ESOME(X0),X21)),X22),X23) = ap(X23,X21)
| ~ mem(X23,arr(X0,X1)) )
| ~ mem(X22,X1) )
| ~ mem(X21,X0) )
& ! [X24] :
( ! [X25] :
( ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X24),ap(c_2Eoption_2ESOME(X0),X25)) = ap(c_2Eoption_2ESOME(X1),ap(X24,X25))
| ~ mem(X25,X0) )
| ~ mem(X24,arr(X0,X1)) )
& ! [X26] :
( ap(ap(c_2Eoption_2EOPTION__MAP(X0,X1),X26),c_2Eoption_2ENONE(X0)) = c_2Eoption_2ENONE(X1)
| ~ mem(X26,arr(X0,X1)) )
& ap(c_2Eoption_2EOPTION__JOIN(X0),c_2Eoption_2ENONE(ty_2Eoption_2Eoption(X0))) = c_2Eoption_2ENONE(X0)
& ! [X27] :
( ap(c_2Eoption_2EOPTION__JOIN(X0),ap(c_2Eoption_2ESOME(ty_2Eoption_2Eoption(X0)),X27)) = X27
| ~ mem(X27,ty_2Eoption_2Eoption(X0)) ) )
| ~ sP3(X0,X2,X3,X1,X4) ),
inference(nnf_transformation,[],[f104]) ).
fof(f136,plain,
! [X0,X1,X2,X3,X4] :
( ( sP2(X0)
& ! [X5] :
( ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X5)) = X5
| ~ mem(X5,X0) )
& ! [X6] :
( c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X6)
| ~ mem(X6,X0) )
& ! [X7] :
( c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X7)
| ~ mem(X7,X0) )
& ! [X8] :
( p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X8)))
| ~ mem(X8,X0) )
& ~ p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0)))
& sP1(X0)
& sP0(X0)
& ! [X9] :
( ap(c_2Eoption_2ESOME(X0),ap(c_2Eoption_2ETHE(X0),X9)) = X9
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X9))
| ~ mem(X9,ty_2Eoption_2Eoption(X0)) )
& ! [X10] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X10),c_2Eoption_2ENONE(X0)),c_2Eoption_2ESOME(X0)) = X10
| ~ mem(X10,ty_2Eoption_2Eoption(X0)) )
& ! [X11] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X11),X11),c_2Eoption_2ESOME(X0)) = X11
| ~ mem(X11,ty_2Eoption_2Eoption(X0)) )
& ! [X12] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X3),X12),X1),X2) = X1
| ~ p(ap(c_2Eoption_2EIS__NONE(X0),X12))
| ~ mem(X12,ty_2Eoption_2Eoption(X0)) )
& ! [X13] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X3),X13),X1),X2) = ap(X2,ap(c_2Eoption_2ETHE(X0),X13))
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X13))
| ~ mem(X13,ty_2Eoption_2Eoption(X0)) )
& ! [X14] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,ty_2Eoption_2Eoption(X0)),X14),X4),c_2Eoption_2ESOME(X0)) = X14
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),X14))
| ~ mem(X14,ty_2Eoption_2Eoption(X0)) )
& ! [X15] :
( ! [X16] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X3),c_2Eoption_2ENONE(X0)),X15),X16) = X15
| ~ mem(X16,arr(X0,X3)) )
| ~ mem(X15,X3) )
& ! [X17] :
( ! [X18] :
( ! [X19] :
( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X3),ap(c_2Eoption_2ESOME(X0),X17)),X18),X19) = ap(X19,X17)
| ~ mem(X19,arr(X0,X3)) )
| ~ mem(X18,X3) )
| ~ mem(X17,X0) )
& ! [X20] :
( ! [X21] :
( ap(ap(c_2Eoption_2EOPTION__MAP(X0,X3),X20),ap(c_2Eoption_2ESOME(X0),X21)) = ap(c_2Eoption_2ESOME(X3),ap(X20,X21))
| ~ mem(X21,X0) )
| ~ mem(X20,arr(X0,X3)) )
& ! [X22] :
( ap(ap(c_2Eoption_2EOPTION__MAP(X0,X3),X22),c_2Eoption_2ENONE(X0)) = c_2Eoption_2ENONE(X3)
| ~ mem(X22,arr(X0,X3)) )
& ap(c_2Eoption_2EOPTION__JOIN(X0),c_2Eoption_2ENONE(ty_2Eoption_2Eoption(X0))) = c_2Eoption_2ENONE(X0)
& ! [X23] :
( ap(c_2Eoption_2EOPTION__JOIN(X0),ap(c_2Eoption_2ESOME(ty_2Eoption_2Eoption(X0)),X23)) = X23
| ~ mem(X23,ty_2Eoption_2Eoption(X0)) ) )
| ~ sP3(X0,X1,X2,X3,X4) ),
inference(rectify,[],[f135]) ).
fof(f143,plain,
! [X0,X1,X3,X4,X2] :
( ( sP4(X0,X1,X3,X4,X2)
| ! [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)) ) ) )
& ( ? [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)) ) )
| ~ sP4(X0,X1,X3,X4,X2) ) ),
inference(nnf_transformation,[],[f106]) ).
fof(f144,plain,
! [X0,X1,X2,X3,X4] :
( ( sP4(X0,X1,X2,X3,X4)
| ! [X5] :
( ~ mem(X5,X0)
| ! [X6] :
( ~ mem(X6,X1)
| ap(c_2Eoption_2ESOME(X0),X5) != X2
| ap(c_2Eoption_2ESOME(X1),X6) != X3
| ~ p(ap(ap(X4,X5),X6)) ) ) )
& ( ? [X7] :
( mem(X7,X0)
& ? [X8] :
( mem(X8,X1)
& ap(c_2Eoption_2ESOME(X0),X7) = X2
& ap(c_2Eoption_2ESOME(X1),X8) = X3
& p(ap(ap(X4,X7),X8)) ) )
| ~ sP4(X0,X1,X2,X3,X4) ) ),
inference(rectify,[],[f143]) ).
fof(f145,plain,
! [X0,X1,X2,X3,X4] :
( ( sP4(X0,X1,X2,X3,X4)
| ! [X5] :
( ~ mem(X5,X0)
| ! [X6] :
( ~ mem(X6,X1)
| ap(c_2Eoption_2ESOME(X0),X5) != X2
| ap(c_2Eoption_2ESOME(X1),X6) != X3
| ~ p(ap(ap(X4,X5),X6)) ) ) )
& ( ( mem(sK9(X0,X1,X2,X3,X4),X0)
& mem(sK10(X0,X1,X2,X3,X4),X1)
& ap(c_2Eoption_2ESOME(X0),sK9(X0,X1,X2,X3,X4)) = X2
& ap(c_2Eoption_2ESOME(X1),sK10(X0,X1,X2,X3,X4)) = X3
& p(ap(ap(X4,sK9(X0,X1,X2,X3,X4)),sK10(X0,X1,X2,X3,X4))) )
| ~ sP4(X0,X1,X2,X3,X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10]),skolemize(X7,sK9(X0,X1,X2,X3,X4)),skolemize(X8,sK10(X0,X1,X2,X3,X4))],[f144]) ).
fof(f146,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 )
& ~ sP4(X0,X1,X3,X4,X2) ) )
& ( ( X3 = c_2Eoption_2ENONE(X0)
& X4 = c_2Eoption_2ENONE(X1) )
| sP4(X0,X1,X3,X4,X2)
| ~ 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,[],[f107]) ).
fof(f147,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 )
& ~ sP4(X0,X1,X3,X4,X2) ) )
& ( ( X3 = c_2Eoption_2ENONE(X0)
& X4 = c_2Eoption_2ENONE(X1) )
| sP4(X0,X1,X3,X4,X2)
| ~ 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,[],[f146]) ).
fof(f148,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,[],[f100]) ).
fof(f149,plain,
( ( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),c_2Eoption_2ENONE(sK11)),c_2Eoption_2ENONE(sK11)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),ap(c_2Eoption_2ESOME(sK11),sK13)),c_2Eoption_2ENONE(sK11)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),c_2Eoption_2ENONE(sK11)),ap(c_2Eoption_2ESOME(sK11),sK14)))
| ( ( ~ p(ap(ap(sK12,sK13),sK14))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),ap(c_2Eoption_2ESOME(sK11),sK13)),ap(c_2Eoption_2ESOME(sK11),sK14))) )
& ( p(ap(ap(sK12,sK13),sK14))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),ap(c_2Eoption_2ESOME(sK11),sK13)),ap(c_2Eoption_2ESOME(sK11),sK14))) ) ) )
& mem(sK14,sK11)
& mem(sK13,sK11)
& mem(sK12,arr(sK11,arr(sK11,bool)))
& ne(sK11) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13,sK14]),skolemize(X0,sK11),skolemize(X1,sK12),skolemize(X2,sK13),skolemize(X3,sK14)],[f148]) ).
fof(f150,plain,
ne(bool),
inference(cnf_transformation,[],[f1]) ).
fof(f152,plain,
! [X0,X1] :
( ne(arr(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f61]) ).
fof(f153,plain,
! [X2,X3,X0,X1] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0)
| ~ mem(X2,arr(X0,X1)) ),
inference(cnf_transformation,[],[f62]) ).
fof(f160,plain,
! [X0] :
( ne(ty_2Eoption_2Eoption(X0))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f69]) ).
fof(f171,plain,
mem(c_2Ebool_2ET,bool),
inference(cnf_transformation,[],[f18]) ).
fof(f172,plain,
p(c_2Ebool_2ET),
inference(cnf_transformation,[],[f19]) ).
fof(f177,plain,
! [X0] :
( mem(c_2Eoption_2ETHE(X0),arr(ty_2Eoption_2Eoption(X0),X0))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f178,plain,
! [X0] :
( mem(c_2Eoption_2ESOME(X0),arr(X0,ty_2Eoption_2Eoption(X0)))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f183,plain,
! [X0] :
( mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f210,plain,
! [X0,X1] :
( mem(sK8(X0,X1),X0)
| ~ p(X1)
| ~ mem(X1,bool)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f127]) ).
fof(f250,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0)))
| ~ sP3(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f136]) ).
fof(f251,plain,
! [X2,X3,X0,X1,X8,X4] :
( p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X8)))
| ~ mem(X8,X0)
| ~ sP3(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f136]) ).
fof(f252,plain,
! [X2,X3,X0,X1,X7,X4] :
( c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X7)
| ~ mem(X7,X0)
| ~ sP3(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f136]) ).
fof(f254,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ mem(X5,X0)
| ~ sP3(X0,X1,X2,X3,X4)
| ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X5)) = X5 ),
inference(cnf_transformation,[],[f136]) ).
fof(f262,plain,
! [X2,X3,X0,X1,X4] :
( sP3(X0,X2,X3,X1,X4)
| ~ mem(X4,ty_2Eoption_2Eoption(X0))
| ~ mem(X3,arr(X0,X1))
| ~ mem(X2,X1)
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f263,plain,
! [X2,X3,X0,X1,X4] :
( p(ap(ap(X4,sK9(X0,X1,X2,X3,X4)),sK10(X0,X1,X2,X3,X4)))
| ~ sP4(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f145]) ).
fof(f264,plain,
! [X2,X3,X0,X1,X4] :
( ~ sP4(X0,X1,X2,X3,X4)
| ap(c_2Eoption_2ESOME(X1),sK10(X0,X1,X2,X3,X4)) = X3 ),
inference(cnf_transformation,[],[f145]) ).
fof(f265,plain,
! [X2,X3,X0,X1,X4] :
( ~ sP4(X0,X1,X2,X3,X4)
| ap(c_2Eoption_2ESOME(X0),sK9(X0,X1,X2,X3,X4)) = X2 ),
inference(cnf_transformation,[],[f145]) ).
fof(f266,plain,
! [X2,X3,X0,X1,X4] :
( mem(sK10(X0,X1,X2,X3,X4),X1)
| ~ sP4(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f145]) ).
fof(f267,plain,
! [X2,X3,X0,X1,X4] :
( mem(sK9(X0,X1,X2,X3,X4),X0)
| ~ sP4(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f145]) ).
fof(f268,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( sP4(X0,X1,X2,X3,X4)
| ~ mem(X5,X0)
| ~ mem(X6,X1)
| ap(c_2Eoption_2ESOME(X0),X5) != X2
| ap(c_2Eoption_2ESOME(X1),X6) != X3
| ~ p(ap(ap(X4,X5),X6)) ),
inference(cnf_transformation,[],[f145]) ).
fof(f269,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| sP4(X0,X1,X3,X4,X2)
| 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,[],[f147]) ).
fof(f270,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| sP4(X0,X1,X3,X4,X2)
| c_2Eoption_2ENONE(X0) = X3
| ~ 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,[],[f147]) ).
fof(f271,plain,
! [X2,X3,X0,X1,X4] :
( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| ~ sP4(X0,X1,X3,X4,X2)
| ~ 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,[],[f147]) ).
fof(f272,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,[],[f147]) ).
fof(f273,plain,
ne(sK11),
inference(cnf_transformation,[],[f149]) ).
fof(f274,plain,
mem(sK12,arr(sK11,arr(sK11,bool))),
inference(cnf_transformation,[],[f149]) ).
fof(f275,plain,
mem(sK13,sK11),
inference(cnf_transformation,[],[f149]) ).
fof(f276,plain,
mem(sK14,sK11),
inference(cnf_transformation,[],[f149]) ).
fof(f277,plain,
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),c_2Eoption_2ENONE(sK11)),c_2Eoption_2ENONE(sK11)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),ap(c_2Eoption_2ESOME(sK11),sK13)),c_2Eoption_2ENONE(sK11)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),c_2Eoption_2ENONE(sK11)),ap(c_2Eoption_2ESOME(sK11),sK14)))
| p(ap(ap(sK12,sK13),sK14))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),ap(c_2Eoption_2ESOME(sK11),sK13)),ap(c_2Eoption_2ESOME(sK11),sK14))) ),
inference(cnf_transformation,[],[f149]) ).
fof(f278,plain,
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),c_2Eoption_2ENONE(sK11)),c_2Eoption_2ENONE(sK11)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),ap(c_2Eoption_2ESOME(sK11),sK13)),c_2Eoption_2ENONE(sK11)))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),c_2Eoption_2ENONE(sK11)),ap(c_2Eoption_2ESOME(sK11),sK14)))
| ~ p(ap(ap(sK12,sK13),sK14))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),ap(c_2Eoption_2ESOME(sK11),sK13)),ap(c_2Eoption_2ESOME(sK11),sK14))) ),
inference(cnf_transformation,[],[f149]) ).
fof(f283,plain,
! [X3,X0,X1,X6,X4,X5] :
( sP4(X0,X1,ap(c_2Eoption_2ESOME(X0),X5),X3,X4)
| ~ mem(X5,X0)
| ~ mem(X6,X1)
| ap(c_2Eoption_2ESOME(X1),X6) != X3
| ~ p(ap(ap(X4,X5),X6)) ),
inference(equality_resolution,[],[f268]) ).
fof(f284,plain,
! [X0,X1,X6,X4,X5] :
( sP4(X0,X1,ap(c_2Eoption_2ESOME(X0),X5),ap(c_2Eoption_2ESOME(X1),X6),X4)
| ~ mem(X5,X0)
| ~ mem(X6,X1)
| ~ p(ap(ap(X4,X5),X6)) ),
inference(equality_resolution,[],[f283]) ).
fof(f285,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,[],[f272]) ).
fof(f286,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(X1),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,[],[f285]) ).
fof(f300,definition,
( spl15_1
<=> p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),ap(c_2Eoption_2ESOME(sK11),sK13)),ap(c_2Eoption_2ESOME(sK11),sK14))) ),
introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition]) ).
fof(f301,plain,
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),ap(c_2Eoption_2ESOME(sK11),sK13)),ap(c_2Eoption_2ESOME(sK11),sK14)))
| spl15_1 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f302,plain,
( p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),ap(c_2Eoption_2ESOME(sK11),sK13)),ap(c_2Eoption_2ESOME(sK11),sK14)))
| ~ spl15_1 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f304,definition,
( spl15_2
<=> p(ap(ap(sK12,sK13),sK14)) ),
introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition]) ).
fof(f305,plain,
( ~ p(ap(ap(sK12,sK13),sK14))
| spl15_2 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f306,plain,
( p(ap(ap(sK12,sK13),sK14))
| ~ spl15_2 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f308,definition,
( spl15_3
<=> p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),c_2Eoption_2ENONE(sK11)),ap(c_2Eoption_2ESOME(sK11),sK14))) ),
introduced(definition,[new_symbols(definition,[spl15_3])],[avatar_definition]) ).
fof(f310,plain,
( p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),c_2Eoption_2ENONE(sK11)),ap(c_2Eoption_2ESOME(sK11),sK14)))
| ~ spl15_3 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f312,definition,
( spl15_4
<=> p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),ap(c_2Eoption_2ESOME(sK11),sK13)),c_2Eoption_2ENONE(sK11))) ),
introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition]) ).
fof(f314,plain,
( p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),ap(c_2Eoption_2ESOME(sK11),sK13)),c_2Eoption_2ENONE(sK11)))
| ~ spl15_4 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f316,definition,
( spl15_5
<=> p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),c_2Eoption_2ENONE(sK11)),c_2Eoption_2ENONE(sK11))) ),
introduced(definition,[new_symbols(definition,[spl15_5])],[avatar_definition]) ).
fof(f318,plain,
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK11,sK11),sK12),c_2Eoption_2ENONE(sK11)),c_2Eoption_2ENONE(sK11)))
| spl15_5 ),
inference(avatar_component_clause,[],[f316]) ).
fof(f319,plain,
( spl15_1
| spl15_2
| spl15_3
| spl15_4
| ~ spl15_5 ),
inference(avatar_split_clause,[],[f277,f316,f312,f308,f304,f300]) ).
fof(f320,plain,
( ~ spl15_1
| ~ spl15_2
| spl15_3
| spl15_4
| ~ spl15_5 ),
inference(avatar_split_clause,[],[f278,f316,f312,f308,f304,f300]) ).
fof(f882,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ sP4(X0,X1,X2,X3,X4)
| ~ sP3(X0,X5,X6,X7,X8)
| sK9(X0,X1,X2,X3,X4) = ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),sK9(X0,X1,X2,X3,X4))) ),
inference(resolution,[],[f254,f267]) ).
fof(f884,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ sP4(X0,X1,X2,X3,X4)
| ~ sP3(X1,X5,X6,X7,X8)
| sK10(X0,X1,X2,X3,X4) = ap(c_2Eoption_2ETHE(X1),ap(c_2Eoption_2ESOME(X1),sK10(X0,X1,X2,X3,X4))) ),
inference(resolution,[],[f254,f266]) ).
fof(f2290,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ mem(X0,ty_2Eoption_2Eoption(X1))
| ~ mem(X2,arr(X1,X3))
| ~ mem(X5,X1)
| ~ mem(X4,X3)
| ~ ne(X1)
| ~ ne(X3)
| ap(c_2Eoption_2ETHE(X1),ap(c_2Eoption_2ESOME(X1),X5)) = X5 ),
inference(resolution,[],[f262,f254]) ).
fof(f4829,plain,
( ~ sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11))
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ ne(sK11)
| spl15_1 ),
inference(resolution,[],[f271,f301]) ).
fof(f4832,plain,
( ~ sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11))
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| spl15_1 ),
inference(duplicate_literal_removal,[],[f4829]) ).
fof(f4833,plain,
( ~ sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11))
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| ~ ne(sK11)
| spl15_1 ),
inference(forward_subsumption_resolution,[],[f4832,f274]) ).
fof(f4834,plain,
( ~ sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11))
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| spl15_1 ),
inference(forward_subsumption_resolution,[],[f4833,f273]) ).
fof(f4836,definition,
( spl15_302
<=> mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11)) ),
introduced(definition,[new_symbols(definition,[spl15_302])],[avatar_definition]) ).
fof(f4837,plain,
( mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| ~ spl15_302 ),
inference(avatar_component_clause,[],[f4836]) ).
fof(f4838,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| spl15_302 ),
inference(avatar_component_clause,[],[f4836]) ).
fof(f4840,definition,
( spl15_303
<=> mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11)) ),
introduced(definition,[new_symbols(definition,[spl15_303])],[avatar_definition]) ).
fof(f4841,plain,
( mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11))
| ~ spl15_303 ),
inference(avatar_component_clause,[],[f4840]) ).
fof(f4842,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11))
| spl15_303 ),
inference(avatar_component_clause,[],[f4840]) ).
fof(f4844,definition,
( spl15_304
<=> sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12) ),
introduced(definition,[new_symbols(definition,[spl15_304])],[avatar_definition]) ).
fof(f4845,plain,
( sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ spl15_304 ),
inference(avatar_component_clause,[],[f4844]) ).
fof(f4846,plain,
( ~ sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| spl15_304 ),
inference(avatar_component_clause,[],[f4844]) ).
fof(f4847,plain,
( ~ spl15_302
| ~ spl15_303
| ~ spl15_304
| spl15_1 ),
inference(avatar_split_clause,[],[f4834,f300,f4844,f4840,f4836]) ).
fof(f4848,plain,
( ! [X0] :
( ~ mem(c_2Eoption_2ESOME(sK11),arr(X0,ty_2Eoption_2Eoption(sK11)))
| ~ mem(sK13,X0) )
| spl15_302 ),
inference(resolution,[],[f4838,f153]) ).
fof(f4849,plain,
( ~ mem(sK13,sK11)
| ~ ne(sK11)
| spl15_302 ),
inference(resolution,[],[f4848,f178]) ).
fof(f4850,plain,
( ~ ne(sK11)
| spl15_302 ),
inference(forward_subsumption_resolution,[],[f4849,f275]) ).
fof(f4851,plain,
( $false
| spl15_302 ),
inference(forward_subsumption_resolution,[],[f4850,f273]) ).
fof(f4852,plain,
spl15_302,
inference(avatar_contradiction_clause,[],[f4851]) ).
fof(f4867,definition,
( spl15_306
<=> ! [X2,X0,X1,X3] : ~ sP3(sK11,X0,X1,X2,X3) ),
introduced(definition,[new_symbols(definition,[spl15_306])],[avatar_definition]) ).
fof(f4868,plain,
( ! [X2,X3,X0,X1] : ~ sP3(sK11,X0,X1,X2,X3)
| ~ spl15_306 ),
inference(avatar_component_clause,[],[f4867]) ).
fof(f4880,plain,
( ! [X0] :
( ~ mem(c_2Eoption_2ESOME(sK11),arr(X0,ty_2Eoption_2Eoption(sK11)))
| ~ mem(sK14,X0) )
| spl15_303 ),
inference(resolution,[],[f4842,f153]) ).
fof(f4881,plain,
( ~ mem(sK14,sK11)
| ~ ne(sK11)
| spl15_303 ),
inference(resolution,[],[f4880,f178]) ).
fof(f4882,plain,
( ~ ne(sK11)
| spl15_303 ),
inference(forward_subsumption_resolution,[],[f4881,f276]) ).
fof(f4883,plain,
( $false
| spl15_303 ),
inference(forward_subsumption_resolution,[],[f4882,f273]) ).
fof(f4884,plain,
spl15_303,
inference(avatar_contradiction_clause,[],[f4883]) ).
fof(f4909,plain,
( ! [X2,X3,X0,X1] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK11))
| ~ mem(X1,arr(sK11,X2))
| ~ mem(X3,X2)
| ~ ne(X2)
| ~ ne(sK11) )
| ~ spl15_306 ),
inference(resolution,[],[f4868,f262]) ).
fof(f4910,plain,
( ! [X2,X3,X0,X1] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK11))
| ~ mem(X1,arr(sK11,X2))
| ~ mem(X3,X2)
| ~ ne(X2) )
| ~ spl15_306 ),
inference(forward_subsumption_resolution,[],[f4909,f273]) ).
fof(f4912,definition,
( spl15_312
<=> ! [X2,X1,X3] :
( ~ mem(X1,arr(sK11,X2))
| ~ ne(X2)
| ~ mem(X3,X2) ) ),
introduced(definition,[new_symbols(definition,[spl15_312])],[avatar_definition]) ).
fof(f4913,plain,
( ! [X2,X3,X1] :
( ~ mem(X1,arr(sK11,X2))
| ~ mem(X3,X2)
| ~ ne(X2) )
| ~ spl15_312 ),
inference(avatar_component_clause,[],[f4912]) ).
fof(f4915,definition,
( spl15_313
<=> ! [X0] : ~ mem(X0,ty_2Eoption_2Eoption(sK11)) ),
introduced(definition,[new_symbols(definition,[spl15_313])],[avatar_definition]) ).
fof(f4916,plain,
( ! [X0] : ~ mem(X0,ty_2Eoption_2Eoption(sK11))
| ~ spl15_313 ),
inference(avatar_component_clause,[],[f4915]) ).
fof(f4917,plain,
( spl15_312
| spl15_313
| ~ spl15_306 ),
inference(avatar_split_clause,[],[f4910,f4867,f4915,f4912]) ).
fof(f4918,plain,
( ! [X0] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK11))
| ~ ne(ty_2Eoption_2Eoption(sK11))
| ~ ne(sK11) )
| ~ spl15_312 ),
inference(resolution,[],[f4913,f178]) ).
fof(f4983,definition,
( spl15_314
<=> ! [X1] :
( ~ p(X1)
| ~ mem(X1,bool) ) ),
introduced(definition,[new_symbols(definition,[spl15_314])],[avatar_definition]) ).
fof(f4984,plain,
( ! [X1] :
( ~ mem(X1,bool)
| ~ p(X1) )
| ~ spl15_314 ),
inference(avatar_component_clause,[],[f4983]) ).
fof(f4994,definition,
( spl15_317
<=> ne(arr(sK11,bool)) ),
introduced(definition,[new_symbols(definition,[spl15_317])],[avatar_definition]) ).
fof(f4995,plain,
( ne(arr(sK11,bool))
| ~ spl15_317 ),
inference(avatar_component_clause,[],[f4994]) ).
fof(f4996,plain,
( ~ ne(arr(sK11,bool))
| spl15_317 ),
inference(avatar_component_clause,[],[f4994]) ).
fof(f4998,definition,
( spl15_318
<=> ! [X0] : ~ mem(X0,arr(sK11,bool)) ),
introduced(definition,[new_symbols(definition,[spl15_318])],[avatar_definition]) ).
fof(f4999,plain,
( ! [X0] : ~ mem(X0,arr(sK11,bool))
| ~ spl15_318 ),
inference(avatar_component_clause,[],[f4998]) ).
fof(f5002,plain,
( ! [X0] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK11))
| ~ ne(sK11) )
| ~ spl15_312 ),
inference(forward_subsumption_resolution,[],[f4918,f160]) ).
fof(f5005,plain,
( ! [X0] : ~ mem(X0,ty_2Eoption_2Eoption(sK11))
| ~ spl15_312 ),
inference(forward_subsumption_resolution,[],[f5002,f273]) ).
fof(f5006,plain,
( spl15_313
| ~ spl15_312 ),
inference(avatar_split_clause,[],[f5005,f4912,f4915]) ).
fof(f5021,plain,
( ~ ne(sK11)
| ~ spl15_313 ),
inference(resolution,[],[f4916,f183]) ).
fof(f5045,plain,
( $false
| ~ spl15_313 ),
inference(forward_subsumption_resolution,[],[f5021,f273]) ).
fof(f5046,plain,
~ spl15_313,
inference(avatar_contradiction_clause,[],[f5045]) ).
fof(f5052,plain,
( ~ mem(sK13,sK11)
| ~ mem(sK14,sK11)
| ~ p(ap(ap(sK12,sK13),sK14))
| spl15_304 ),
inference(resolution,[],[f4846,f284]) ).
fof(f5053,plain,
( ~ mem(sK14,sK11)
| ~ p(ap(ap(sK12,sK13),sK14))
| spl15_304 ),
inference(forward_subsumption_resolution,[],[f5052,f275]) ).
fof(f5054,plain,
( ~ p(ap(ap(sK12,sK13),sK14))
| spl15_304 ),
inference(forward_subsumption_resolution,[],[f5053,f276]) ).
fof(f5055,plain,
( $false
| ~ spl15_2
| spl15_304 ),
inference(forward_subsumption_resolution,[],[f5054,f306]) ).
fof(f5056,plain,
( ~ spl15_2
| spl15_304 ),
inference(avatar_contradiction_clause,[],[f5055]) ).
fof(f5143,plain,
( ap(c_2Eoption_2ESOME(sK11),sK13) = ap(c_2Eoption_2ESOME(sK11),sK9(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12))
| ~ spl15_304 ),
inference(resolution,[],[f4845,f265]) ).
fof(f5144,plain,
( ap(c_2Eoption_2ESOME(sK11),sK14) = ap(c_2Eoption_2ESOME(sK11),sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12))
| ~ spl15_304 ),
inference(resolution,[],[f4845,f264]) ).
fof(f5212,plain,
( sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK13)
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11))
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ ne(sK11)
| ~ spl15_1 ),
inference(resolution,[],[f270,f302]) ).
fof(f5215,plain,
( sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK13)
| ~ mem(c_2Eoption_2ENONE(sK11),ty_2Eoption_2Eoption(sK11))
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ ne(sK11)
| ~ spl15_4 ),
inference(resolution,[],[f270,f314]) ).
fof(f5223,plain,
( sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK13)
| ~ mem(c_2Eoption_2ENONE(sK11),ty_2Eoption_2Eoption(sK11))
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ spl15_4 ),
inference(duplicate_literal_removal,[],[f5215]) ).
fof(f5226,plain,
( sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK13)
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11))
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ spl15_1 ),
inference(duplicate_literal_removal,[],[f5212]) ).
fof(f5228,plain,
( sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK13)
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ spl15_4 ),
inference(forward_subsumption_resolution,[],[f5223,f183]) ).
fof(f5229,plain,
( sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK13)
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ spl15_4
| ~ spl15_302 ),
inference(forward_subsumption_resolution,[],[f5228,f4837]) ).
fof(f5230,plain,
( sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK13)
| ~ ne(sK11)
| ~ spl15_4
| ~ spl15_302 ),
inference(forward_subsumption_resolution,[],[f5229,f274]) ).
fof(f5231,plain,
( sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK13)
| ~ spl15_4
| ~ spl15_302 ),
inference(forward_subsumption_resolution,[],[f5230,f273]) ).
fof(f5233,definition,
( spl15_327
<=> c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK13) ),
introduced(definition,[new_symbols(definition,[spl15_327])],[avatar_definition]) ).
fof(f5234,plain,
( c_2Eoption_2ENONE(sK11) != ap(c_2Eoption_2ESOME(sK11),sK13)
| spl15_327 ),
inference(avatar_component_clause,[],[f5233]) ).
fof(f5235,plain,
( c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK13)
| ~ spl15_327 ),
inference(avatar_component_clause,[],[f5233]) ).
fof(f5237,definition,
( spl15_328
<=> sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12) ),
introduced(definition,[new_symbols(definition,[spl15_328])],[avatar_definition]) ).
fof(f5239,plain,
( sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12)
| ~ spl15_328 ),
inference(avatar_component_clause,[],[f5237]) ).
fof(f5240,plain,
( spl15_327
| spl15_328
| ~ spl15_4
| ~ spl15_302 ),
inference(avatar_split_clause,[],[f5231,f4836,f312,f5237,f5233]) ).
fof(f5254,plain,
( ! [X2,X3,X0,X1] :
( c_2Eoption_2ENONE(sK11) != c_2Eoption_2ENONE(sK11)
| ~ mem(sK13,sK11)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_327 ),
inference(superposition,[],[f252,f5235]) ).
fof(f5257,plain,
( ! [X2,X3,X0,X1] :
( ~ mem(sK13,sK11)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_327 ),
inference(trivial_inequality_removal,[],[f5254]) ).
fof(f5262,plain,
( ! [X2,X3,X0,X1] : ~ sP3(sK11,X0,X1,X2,X3)
| ~ spl15_327 ),
inference(forward_subsumption_resolution,[],[f5257,f275]) ).
fof(f5269,plain,
( spl15_306
| ~ spl15_327 ),
inference(avatar_split_clause,[],[f5262,f5233,f4867]) ).
fof(f5281,plain,
( sP4(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK14)
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11))
| ~ mem(c_2Eoption_2ENONE(sK11),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ ne(sK11)
| ~ spl15_3 ),
inference(resolution,[],[f310,f269]) ).
fof(f5282,plain,
( sP4(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK14)
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11))
| ~ mem(c_2Eoption_2ENONE(sK11),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ spl15_3 ),
inference(duplicate_literal_removal,[],[f5281]) ).
fof(f5284,plain,
( sP4(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK14)
| ~ mem(c_2Eoption_2ENONE(sK11),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ spl15_3
| ~ spl15_303 ),
inference(forward_subsumption_resolution,[],[f5282,f4841]) ).
fof(f5285,plain,
( sP4(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK14)
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ spl15_3
| ~ spl15_303 ),
inference(forward_subsumption_resolution,[],[f5284,f183]) ).
fof(f5286,plain,
( sP4(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK14)
| ~ ne(sK11)
| ~ spl15_3
| ~ spl15_303 ),
inference(forward_subsumption_resolution,[],[f5285,f274]) ).
fof(f5287,plain,
( sP4(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK14)
| ~ spl15_3
| ~ spl15_303 ),
inference(forward_subsumption_resolution,[],[f5286,f273]) ).
fof(f5289,definition,
( spl15_332
<=> c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK14) ),
introduced(definition,[new_symbols(definition,[spl15_332])],[avatar_definition]) ).
fof(f5291,plain,
( c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK14)
| ~ spl15_332 ),
inference(avatar_component_clause,[],[f5289]) ).
fof(f5293,definition,
( spl15_333
<=> sP4(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12) ),
introduced(definition,[new_symbols(definition,[spl15_333])],[avatar_definition]) ).
fof(f5295,plain,
( sP4(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ spl15_333 ),
inference(avatar_component_clause,[],[f5293]) ).
fof(f5296,plain,
( spl15_332
| spl15_333
| ~ spl15_3
| ~ spl15_303 ),
inference(avatar_split_clause,[],[f5287,f4840,f308,f5293,f5289]) ).
fof(f5309,plain,
( ! [X2,X3,X0,X1] :
( c_2Eoption_2ENONE(sK11) != c_2Eoption_2ENONE(sK11)
| ~ mem(sK14,sK11)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_332 ),
inference(superposition,[],[f252,f5291]) ).
fof(f5312,plain,
( ! [X2,X3,X0,X1] :
( ~ mem(sK14,sK11)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_332 ),
inference(trivial_inequality_removal,[],[f5309]) ).
fof(f5317,plain,
( ! [X2,X3,X0,X1] : ~ sP3(sK11,X0,X1,X2,X3)
| ~ spl15_332 ),
inference(forward_subsumption_resolution,[],[f5312,f276]) ).
fof(f5326,plain,
( spl15_306
| ~ spl15_332 ),
inference(avatar_split_clause,[],[f5317,f5289,f4867]) ).
fof(f5335,plain,
( c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK9(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12))
| ~ spl15_333 ),
inference(resolution,[],[f5295,f265]) ).
fof(f5374,plain,
( ! [X2,X3,X0,X1] :
( p(ap(c_2Eoption_2EIS__SOME(sK11),c_2Eoption_2ENONE(sK11)))
| ~ mem(sK9(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12),sK11)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_333 ),
inference(superposition,[],[f251,f5335]) ).
fof(f5384,definition,
( spl15_341
<=> mem(sK9(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12),sK11) ),
introduced(definition,[new_symbols(definition,[spl15_341])],[avatar_definition]) ).
fof(f5386,plain,
( ~ mem(sK9(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12),sK11)
| spl15_341 ),
inference(avatar_component_clause,[],[f5384]) ).
fof(f5388,plain,
( ! [X2,X3,X0,X1] :
( ~ mem(sK9(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12),sK11)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_333 ),
inference(forward_subsumption_resolution,[],[f5374,f250]) ).
fof(f5402,plain,
( spl15_306
| ~ spl15_341
| ~ spl15_333 ),
inference(avatar_split_clause,[],[f5388,f5293,f5384,f4867]) ).
fof(f5403,plain,
( ~ sP4(sK11,sK11,c_2Eoption_2ENONE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| spl15_341 ),
inference(resolution,[],[f5386,f267]) ).
fof(f5404,plain,
( $false
| ~ spl15_333
| spl15_341 ),
inference(forward_subsumption_resolution,[],[f5403,f5295]) ).
fof(f5405,plain,
( ~ spl15_333
| spl15_341 ),
inference(avatar_contradiction_clause,[],[f5404]) ).
fof(f17394,plain,
( ~ ne(bool)
| ~ ne(sK11)
| spl15_317 ),
inference(resolution,[],[f4996,f152]) ).
fof(f17395,plain,
( ~ ne(sK11)
| spl15_317 ),
inference(forward_subsumption_resolution,[],[f17394,f150]) ).
fof(f17396,plain,
( $false
| spl15_317 ),
inference(forward_subsumption_resolution,[],[f17395,f273]) ).
fof(f17397,plain,
spl15_317,
inference(avatar_contradiction_clause,[],[f17396]) ).
fof(f18324,plain,
! [X2,X0,X1] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK11))
| ~ mem(X1,sK11)
| ~ mem(X2,arr(sK11,bool))
| ~ ne(sK11)
| ~ ne(arr(sK11,bool))
| ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),X1)) = X1 ),
inference(resolution,[],[f2290,f274]) ).
fof(f18521,plain,
! [X2,X0,X1] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK11))
| ~ mem(X1,sK11)
| ~ mem(X2,arr(sK11,bool))
| ~ ne(arr(sK11,bool))
| ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),X1)) = X1 ),
inference(forward_subsumption_resolution,[],[f18324,f273]) ).
fof(f18582,plain,
( ! [X2,X0,X1] :
( ~ mem(X0,ty_2Eoption_2Eoption(sK11))
| ~ mem(X1,sK11)
| ~ mem(X2,arr(sK11,bool))
| ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),X1)) = X1 )
| ~ spl15_317 ),
inference(forward_subsumption_resolution,[],[f18521,f4995]) ).
fof(f18598,definition,
( spl15_1205
<=> ! [X2] :
( ~ mem(X2,sK11)
| ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),X2)) = X2 ) ),
introduced(definition,[new_symbols(definition,[spl15_1205])],[avatar_definition]) ).
fof(f18599,plain,
( ! [X2] :
( ~ mem(X2,sK11)
| ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),X2)) = X2 )
| ~ spl15_1205 ),
inference(avatar_component_clause,[],[f18598]) ).
fof(f18607,plain,
( spl15_318
| spl15_1205
| spl15_313
| ~ spl15_317 ),
inference(avatar_split_clause,[],[f18582,f4994,f4915,f18598,f4998]) ).
fof(f18626,plain,
( ~ p(c_2Ebool_2ET)
| ~ spl15_314 ),
inference(resolution,[],[f4984,f171]) ).
fof(f18659,plain,
( $false
| ~ spl15_314 ),
inference(forward_subsumption_resolution,[],[f18626,f172]) ).
fof(f18660,plain,
~ spl15_314,
inference(avatar_contradiction_clause,[],[f18659]) ).
fof(f18831,plain,
( sK13 = ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),sK13))
| ~ spl15_1205 ),
inference(resolution,[],[f18599,f275]) ).
fof(f18832,plain,
( sK14 = ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14))
| ~ spl15_1205 ),
inference(resolution,[],[f18599,f276]) ).
fof(f26911,plain,
( ! [X0] :
( ~ p(X0)
| ~ mem(X0,bool)
| ~ ne(arr(sK11,bool)) )
| ~ spl15_318 ),
inference(resolution,[],[f4999,f210]) ).
fof(f26919,plain,
( ! [X0] :
( ~ p(X0)
| ~ mem(X0,bool) )
| ~ spl15_317
| ~ spl15_318 ),
inference(forward_subsumption_resolution,[],[f26911,f4995]) ).
fof(f26921,plain,
( spl15_314
| ~ spl15_317
| ~ spl15_318 ),
inference(avatar_split_clause,[],[f26919,f4998,f4994,f4983]) ).
fof(f28249,plain,
( ! [X2,X3,X0,X1] :
( ~ sP3(sK11,X0,X1,X2,X3)
| sK9(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12) = ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),sK9(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12))) )
| ~ spl15_304 ),
inference(resolution,[],[f882,f4845]) ).
fof(f28251,plain,
( ! [X2,X3,X0,X1] :
( ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),sK13)) = sK9(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_304 ),
inference(forward_demodulation,[],[f28249,f5143]) ).
fof(f28252,plain,
( ! [X2,X3,X0,X1] :
( sK13 = sK9(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_304
| ~ spl15_1205 ),
inference(forward_demodulation,[],[f28251,f18831]) ).
fof(f28254,definition,
( spl15_1851
<=> sK13 = sK9(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12) ),
introduced(definition,[new_symbols(definition,[spl15_1851])],[avatar_definition]) ).
fof(f28256,plain,
( sK13 = sK9(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ spl15_1851 ),
inference(avatar_component_clause,[],[f28254]) ).
fof(f28257,plain,
( spl15_306
| spl15_1851
| ~ spl15_304
| ~ spl15_1205 ),
inference(avatar_split_clause,[],[f28252,f18598,f4844,f28254,f4867]) ).
fof(f28366,plain,
( ! [X2,X3,X0,X1] :
( ~ sP3(sK11,X0,X1,X2,X3)
| sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12) = ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12))) )
| ~ spl15_304 ),
inference(resolution,[],[f884,f4845]) ).
fof(f28368,plain,
( ! [X2,X3,X0,X1] :
( ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),sK14)) = sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_304 ),
inference(forward_demodulation,[],[f28366,f5144]) ).
fof(f28369,plain,
( ! [X2,X3,X0,X1] :
( sK14 = sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_304
| ~ spl15_1205 ),
inference(forward_demodulation,[],[f28368,f18832]) ).
fof(f28371,definition,
( spl15_1866
<=> sK14 = sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12) ),
introduced(definition,[new_symbols(definition,[spl15_1866])],[avatar_definition]) ).
fof(f28373,plain,
( sK14 = sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ spl15_1866 ),
inference(avatar_component_clause,[],[f28371]) ).
fof(f28374,plain,
( spl15_306
| spl15_1866
| ~ spl15_304
| ~ spl15_1205 ),
inference(avatar_split_clause,[],[f28369,f18598,f4844,f28371,f4867]) ).
fof(f28377,plain,
( p(ap(ap(sK12,sK9(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)),sK14))
| ~ sP4(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)
| ~ spl15_1866 ),
inference(superposition,[],[f263,f28373]) ).
fof(f28379,plain,
( p(ap(ap(sK12,sK9(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),ap(c_2Eoption_2ESOME(sK11),sK14),sK12)),sK14))
| ~ spl15_304
| ~ spl15_1866 ),
inference(forward_subsumption_resolution,[],[f28377,f4845]) ).
fof(f28382,plain,
( p(ap(ap(sK12,sK13),sK14))
| ~ spl15_304
| ~ spl15_1851
| ~ spl15_1866 ),
inference(forward_demodulation,[],[f28379,f28256]) ).
fof(f28383,plain,
( $false
| spl15_2
| ~ spl15_304
| ~ spl15_1851
| ~ spl15_1866 ),
inference(forward_subsumption_resolution,[],[f28382,f305]) ).
fof(f28384,plain,
( spl15_2
| ~ spl15_304
| ~ spl15_1851
| ~ spl15_1866 ),
inference(avatar_contradiction_clause,[],[f28383]) ).
fof(f28386,plain,
( c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK13)
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11))
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ spl15_1
| spl15_304 ),
inference(forward_subsumption_resolution,[],[f5226,f4846]) ).
fof(f28388,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK11),sK14),ty_2Eoption_2Eoption(sK11))
| ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ spl15_1
| spl15_304
| spl15_327 ),
inference(forward_subsumption_resolution,[],[f28386,f5234]) ).
fof(f28390,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK11),sK13),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ spl15_1
| ~ spl15_303
| spl15_304
| spl15_327 ),
inference(forward_subsumption_resolution,[],[f28388,f4841]) ).
fof(f28392,plain,
( ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ spl15_1
| ~ spl15_302
| ~ spl15_303
| spl15_304
| spl15_327 ),
inference(forward_subsumption_resolution,[],[f28390,f4837]) ).
fof(f28394,plain,
( ~ ne(sK11)
| ~ spl15_1
| ~ spl15_302
| ~ spl15_303
| spl15_304
| spl15_327 ),
inference(forward_subsumption_resolution,[],[f28392,f274]) ).
fof(f28397,plain,
( $false
| ~ spl15_1
| ~ spl15_302
| ~ spl15_303
| spl15_304
| spl15_327 ),
inference(forward_subsumption_resolution,[],[f28394,f273]) ).
fof(f28398,plain,
( ~ spl15_1
| ~ spl15_302
| ~ spl15_303
| spl15_304
| spl15_327 ),
inference(avatar_contradiction_clause,[],[f28397]) ).
fof(f28401,plain,
( c_2Eoption_2ENONE(sK11) = ap(c_2Eoption_2ESOME(sK11),sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12))
| ~ spl15_328 ),
inference(resolution,[],[f5239,f264]) ).
fof(f28408,plain,
( ! [X2,X3,X0,X1] :
( ~ sP3(sK11,X0,X1,X2,X3)
| sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12) = ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12))) )
| ~ spl15_328 ),
inference(resolution,[],[f5239,f884]) ).
fof(f28410,definition,
( spl15_1867
<=> sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12) = ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12))) ),
introduced(definition,[new_symbols(definition,[spl15_1867])],[avatar_definition]) ).
fof(f28412,plain,
( sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12) = ap(c_2Eoption_2ETHE(sK11),ap(c_2Eoption_2ESOME(sK11),sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12)))
| ~ spl15_1867 ),
inference(avatar_component_clause,[],[f28410]) ).
fof(f28413,plain,
( spl15_1867
| spl15_306
| ~ spl15_328 ),
inference(avatar_split_clause,[],[f28408,f5237,f4867,f28410]) ).
fof(f28419,plain,
( ap(c_2Eoption_2ETHE(sK11),c_2Eoption_2ENONE(sK11)) = sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12)
| ~ spl15_328
| ~ spl15_1867 ),
inference(forward_demodulation,[],[f28412,f28401]) ).
fof(f28466,plain,
( ! [X2,X3,X0,X1] :
( p(ap(c_2Eoption_2EIS__SOME(sK11),c_2Eoption_2ENONE(sK11)))
| ~ mem(sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12),sK11)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_328 ),
inference(superposition,[],[f251,f28401]) ).
fof(f28475,plain,
( ! [X2,X3,X0,X1] :
( ~ mem(sK10(sK11,sK11,ap(c_2Eoption_2ESOME(sK11),sK13),c_2Eoption_2ENONE(sK11),sK12),sK11)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_328 ),
inference(forward_subsumption_resolution,[],[f28466,f250]) ).
fof(f28482,definition,
( spl15_1871
<=> mem(ap(c_2Eoption_2ETHE(sK11),c_2Eoption_2ENONE(sK11)),sK11) ),
introduced(definition,[new_symbols(definition,[spl15_1871])],[avatar_definition]) ).
fof(f28484,plain,
( ~ mem(ap(c_2Eoption_2ETHE(sK11),c_2Eoption_2ENONE(sK11)),sK11)
| spl15_1871 ),
inference(avatar_component_clause,[],[f28482]) ).
fof(f28486,plain,
( ! [X2,X3,X0,X1] :
( ~ mem(ap(c_2Eoption_2ETHE(sK11),c_2Eoption_2ENONE(sK11)),sK11)
| ~ sP3(sK11,X0,X1,X2,X3) )
| ~ spl15_328
| ~ spl15_1867 ),
inference(forward_demodulation,[],[f28475,f28419]) ).
fof(f28491,plain,
( spl15_306
| ~ spl15_1871
| ~ spl15_328
| ~ spl15_1867 ),
inference(avatar_split_clause,[],[f28486,f28410,f5237,f28482,f4867]) ).
fof(f28507,plain,
( ! [X0] :
( ~ mem(c_2Eoption_2ETHE(sK11),arr(X0,sK11))
| ~ mem(c_2Eoption_2ENONE(sK11),X0) )
| spl15_1871 ),
inference(resolution,[],[f28484,f153]) ).
fof(f28508,plain,
( ~ mem(c_2Eoption_2ENONE(sK11),ty_2Eoption_2Eoption(sK11))
| ~ ne(sK11)
| spl15_1871 ),
inference(resolution,[],[f28507,f177]) ).
fof(f28509,plain,
( ~ ne(sK11)
| spl15_1871 ),
inference(forward_subsumption_resolution,[],[f28508,f183]) ).
fof(f28510,plain,
( $false
| spl15_1871 ),
inference(forward_subsumption_resolution,[],[f28509,f273]) ).
fof(f28511,plain,
spl15_1871,
inference(avatar_contradiction_clause,[],[f28510]) ).
fof(f28646,plain,
( ~ mem(c_2Eoption_2ENONE(sK11),ty_2Eoption_2Eoption(sK11))
| ~ mem(c_2Eoption_2ENONE(sK11),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| ~ ne(sK11)
| spl15_5 ),
inference(resolution,[],[f318,f286]) ).
fof(f28667,plain,
( ~ mem(c_2Eoption_2ENONE(sK11),ty_2Eoption_2Eoption(sK11))
| ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| spl15_5 ),
inference(duplicate_literal_removal,[],[f28646]) ).
fof(f28685,plain,
( ~ mem(sK12,arr(sK11,arr(sK11,bool)))
| ~ ne(sK11)
| spl15_5 ),
inference(forward_subsumption_resolution,[],[f28667,f183]) ).
fof(f28703,plain,
( ~ ne(sK11)
| spl15_5 ),
inference(forward_subsumption_resolution,[],[f28685,f274]) ).
fof(f28707,plain,
( $false
| spl15_5 ),
inference(forward_subsumption_resolution,[],[f28703,f273]) ).
fof(f28708,plain,
spl15_5,
inference(avatar_contradiction_clause,[],[f28707]) ).
cnf(s1,plain,
( spl15_1
| spl15_2
| spl15_3
| spl15_4
| ~ spl15_5 ),
inference(sat_conversion,[],[f319]) ).
cnf(s2,plain,
( ~ spl15_1
| ~ spl15_2
| spl15_3
| spl15_4
| ~ spl15_5 ),
inference(sat_conversion,[],[f320]) ).
cnf(s225,plain,
( spl15_1
| ~ spl15_302
| ~ spl15_303
| ~ spl15_304 ),
inference(sat_conversion,[],[f4847]) ).
cnf(s226,plain,
spl15_302,
inference(sat_conversion,[],[f4852]) ).
cnf(s230,plain,
spl15_303,
inference(sat_conversion,[],[f4884]) ).
cnf(s234,plain,
( ~ spl15_306
| spl15_312
| spl15_313 ),
inference(sat_conversion,[],[f4917]) ).
cnf(s240,plain,
( ~ spl15_312
| spl15_313 ),
inference(sat_conversion,[],[f5006]) ).
cnf(s244,plain,
~ spl15_313,
inference(sat_conversion,[],[f5046]) ).
cnf(s246,plain,
( ~ spl15_2
| spl15_304 ),
inference(sat_conversion,[],[f5056]) ).
cnf(s255,plain,
( ~ spl15_4
| ~ spl15_302
| spl15_327
| spl15_328 ),
inference(sat_conversion,[],[f5240]) ).
cnf(s258,plain,
( spl15_306
| ~ spl15_327 ),
inference(sat_conversion,[],[f5269]) ).
cnf(s262,plain,
( ~ spl15_3
| ~ spl15_303
| spl15_332
| spl15_333 ),
inference(sat_conversion,[],[f5296]) ).
cnf(s266,plain,
( spl15_306
| ~ spl15_332 ),
inference(sat_conversion,[],[f5326]) ).
cnf(s280,plain,
( spl15_306
| ~ spl15_333
| ~ spl15_341 ),
inference(sat_conversion,[],[f5402]) ).
cnf(s281,plain,
( ~ spl15_333
| spl15_341 ),
inference(sat_conversion,[],[f5405]) ).
cnf(s1023,plain,
spl15_317,
inference(sat_conversion,[],[f17397]) ).
cnf(s1119,plain,
( spl15_313
| ~ spl15_317
| spl15_318
| spl15_1205 ),
inference(sat_conversion,[],[f18607]) ).
cnf(s1125,plain,
~ spl15_314,
inference(sat_conversion,[],[f18660]) ).
cnf(s1620,plain,
( spl15_314
| ~ spl15_317
| ~ spl15_318 ),
inference(sat_conversion,[],[f26921]) ).
cnf(s1701,plain,
( ~ spl15_304
| spl15_306
| ~ spl15_1205
| spl15_1851 ),
inference(sat_conversion,[],[f28257]) ).
cnf(s1709,plain,
( ~ spl15_304
| spl15_306
| ~ spl15_1205
| spl15_1866 ),
inference(sat_conversion,[],[f28374]) ).
cnf(s1711,plain,
( spl15_2
| ~ spl15_304
| ~ spl15_1851
| ~ spl15_1866 ),
inference(sat_conversion,[],[f28384]) ).
cnf(s1713,plain,
( ~ spl15_1
| ~ spl15_302
| ~ spl15_303
| spl15_304
| spl15_327 ),
inference(sat_conversion,[],[f28398]) ).
cnf(s1714,plain,
( spl15_306
| ~ spl15_328
| spl15_1867 ),
inference(sat_conversion,[],[f28413]) ).
cnf(s1718,plain,
( spl15_306
| ~ spl15_328
| ~ spl15_1867
| ~ spl15_1871 ),
inference(sat_conversion,[],[f28491]) ).
cnf(s1723,plain,
spl15_1871,
inference(sat_conversion,[],[f28511]) ).
cnf(s1733,plain,
spl15_5,
inference(sat_conversion,[],[f28708]) ).
cnf(s1738,plain,
( spl15_306
| ~ spl15_328
| ~ spl15_1867 ),
inference(rat,[],[s1718,s1723]) ).
cnf(s1838,plain,
~ spl15_318,
inference(rat,[],[s1620,s1125,s1023]) ).
cnf(s1980,plain,
spl15_1205,
inference(rat,[],[s1119,s1023,s1838,s244]) ).
cnf(s1991,plain,
~ spl15_312,
inference(rat,[],[s240,s244]) ).
cnf(s1992,plain,
~ spl15_306,
inference(rat,[],[s234,s244,s1991]) ).
cnf(s1995,plain,
~ spl15_332,
inference(rat,[],[s266,s1992]) ).
cnf(s1996,plain,
~ spl15_327,
inference(rat,[],[s258,s1992]) ).
cnf(s2023,plain,
( spl15_1
| ~ spl15_304 ),
inference(rat,[],[s225,s230,s226]) ).
cnf(s2151,plain,
( ~ spl15_1
| ~ spl15_2
| spl15_3
| spl15_4 ),
inference(rat,[],[s2,s1733]) ).
cnf(s2152,plain,
( spl15_1
| spl15_2
| spl15_3
| spl15_4 ),
inference(rat,[],[s1,s1733]) ).
cnf(s2153,plain,
~ spl15_328,
inference(rat,[],[s1714,s1738,s1992]) ).
cnf(s2154,plain,
~ spl15_4,
inference(rat,[],[s255,s226,s1996,s2153]) ).
cnf(s2155,plain,
~ spl15_333,
inference(rat,[],[s280,s281,s1992]) ).
cnf(s2156,plain,
~ spl15_3,
inference(rat,[],[s262,s230,s1995,s2155]) ).
cnf(s2157,plain,
spl15_1,
inference(rat,[],[s246,s2152,s2023,s2156,s2154]) ).
cnf(s2158,plain,
spl15_304,
inference(rat,[],[s1713,s1996,s226,s230,s2157]) ).
cnf(s2159,plain,
~ spl15_2,
inference(rat,[],[s2151,s2154,s2156,s2157]) ).
cnf(s2160,plain,
spl15_1866,
inference(rat,[],[s1709,s1992,s1980,s2158]) ).
cnf(s2161,plain,
spl15_1851,
inference(rat,[],[s1701,s1992,s1980,s2158]) ).
cnf(s2162,plain,
$false,
inference(rat,[],[s1711,s2160,s2161,s2158,s2159]) ).
fof(f28709,plain,
$false,
inference(avatar_sat_refutation,[],[s2162]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP011+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n026.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 12:00:11 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.43 Running first-order model finding
% 0.12/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.27/2.65 % (2718792)Will run a generic schedule for satisfiability detection.
% 15.27/2.65 % (2718812)% WARNING: option uhcvi not known.
% 15.27/2.65 % (2718812)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2224117937:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.27/2.65 % (2718811)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1363433598_2999 on theBenchmark for (2999ds/0Mi)
% 15.27/2.65 % (2718813)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1156088654:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.27/2.65 % (2718815)dis+10_1_sil=32000:sp=arity:random_seed=3891406645:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.27/2.65 % (2718816)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2830010322:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.27/2.65 % (2718817)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1823658786:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.27/2.65 % (2718818)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1284840017:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.27/2.65 % TRYING [1]
% 15.27/2.65 % TRYING [2]
% 15.27/2.65 % TRYING [3]
% 15.27/2.65 % (2718815)Instruction limit reached!
% 15.27/2.65 % (2718815)------------------------------
% 15.27/2.65 % (2718815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.27/2.65 % (2718815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.27/2.65 % (2718815)CaDiCaL version: 2.1.3
% 15.27/2.65 % (2718815)Termination reason: Instruction limit
% 15.27/2.65 % (2718815)Termination phase: Saturation
% 15.27/2.65 % (2718815)Time elapsed: 0.067 s
% 15.27/2.65 % (2718815)Peak memory usage: 13 MB
% 15.27/2.65 % (2718815)Instructions burned: 104 (million)
% 15.27/2.65 % (2718816)Instruction limit reached!
% 15.27/2.65 % (2718816)------------------------------
% 15.27/2.65 % (2718816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.27/2.65 % (2718816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.27/2.65 % (2718816)CaDiCaL version: 2.1.3
% 15.27/2.65 % (2718816)Termination reason: Instruction limit
% 15.27/2.65 % (2718816)Termination phase: Saturation
% 15.27/2.65 % (2718816)Time elapsed: 0.074 s
% 15.27/2.65 % (2718816)Peak memory usage: 13 MB
% 15.27/2.65 % (2718816)Instructions burned: 116 (million)
% 15.27/2.65 % (2718817)Instruction limit reached!
% 15.27/2.65 % (2718817)------------------------------
% 15.27/2.65 % (2718817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.27/2.65 % (2718817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.27/2.65 % (2718817)CaDiCaL version: 2.1.3
% 15.27/2.65 % (2718817)Termination reason: Instruction limit
% 15.27/2.65 % (2718817)Termination phase: Saturation
% 15.27/2.65 % (2718817)Time elapsed: 0.074 s
% 15.27/2.65 % (2718817)Peak memory usage: 15 MB
% 15.27/2.65 % (2718817)Instructions burned: 132 (million)
% 15.27/2.65 % TRYING [4]
% 15.27/2.65 % (2718858)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3820172362:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 15.27/2.65 % (2718862)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3076756242:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.27/2.65 % (2718863)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3848071107:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.27/2.65 % (2718818)Instruction limit reached!
% 15.27/2.65 % (2718818)------------------------------
% 15.27/2.65 % (2718818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.27/2.65 % (2718818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.27/2.65 % (2718818)CaDiCaL version: 2.1.3
% 15.27/2.65 % (2718818)Termination reason: Instruction limit
% 15.27/2.65 % (2718818)Termination phase: Saturation
% 15.27/2.65 % (2718818)Time elapsed: 0.105 s
% 15.27/2.65 % (2718818)Peak memory usage: 15 MB
% 15.27/2.65 % (2718818)Instructions burned: 159 (million)
% 15.27/2.65 % TRYING [1]
% 15.27/2.65 % TRYING [2]
% 15.27/2.65 % TRYING [3]
% 15.27/2.65 % (2718873)ott-21_1_sil=16000:fs=off:random_seed=3543029286:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.27/2.65 % (2718862)Instruction limit reached!
% 15.27/2.65 % (2718862)------------------------------
% 15.27/2.65 % (2718862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.27/2.65 % (2718862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.97/6.51 % (2718862)CaDiCaL version: 2.1.3
% 42.97/6.51 % (2718862)Termination reason: Instruction limit
% 42.97/6.51 % (2718862)Termination phase: Saturation
% 42.97/6.51 % (2718862)Time elapsed: 0.076 s
% 42.97/6.51 % (2718862)Peak memory usage: 14 MB
% 42.97/6.51 % (2718862)Instructions burned: 131 (million)
% 42.97/6.51 % TRYING [4]
% 42.97/6.51 % (2718901)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=976954731:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 42.97/6.51 % (2718873)Instruction limit reached!
% 42.97/6.51 % (2718873)------------------------------
% 42.97/6.51 % (2718873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.97/6.51 % (2718873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.97/6.51 % (2718873)CaDiCaL version: 2.1.3
% 42.97/6.51 % (2718873)Termination reason: Instruction limit
% 42.97/6.51 % (2718873)Termination phase: Saturation
% 42.97/6.51 % (2718873)Time elapsed: 0.097 s
% 42.97/6.51 % (2718873)Peak memory usage: 13 MB
% 42.97/6.51 % (2718873)Instructions burned: 180 (million)
% 42.97/6.51 % (2718925)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=136301382:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 42.97/6.51 % TRYING [1]
% 42.97/6.51 % TRYING [2]
% 42.97/6.51 % TRYING [3]
% 42.97/6.51 % (2718858)Instruction limit reached!
% 42.97/6.51 % (2718858)------------------------------
% 42.97/6.51 % (2718858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.97/6.51 % (2718858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.97/6.51 % (2718858)CaDiCaL version: 2.1.3
% 42.97/6.51 % (2718858)Termination reason: Instruction limit
% 42.97/6.51 % (2718858)Termination phase: Finite model building constraint generation
% 42.97/6.51 % (2718858)Time elapsed: 0.278 s
% 42.97/6.51 % (2718858)Peak memory usage: 41 MB
% 42.97/6.51 % (2718858)Instructions burned: 714 (million)
% 42.97/6.51 % TRYING [5]
% 42.97/6.51 % (2718936)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1428180735:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 42.97/6.51 % TRYING [4]
% 42.97/6.51 % (2718901)Instruction limit reached!
% 42.97/6.51 % (2718901)------------------------------
% 42.97/6.51 % (2718901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.97/6.51 % (2718901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.97/6.51 % (2718901)CaDiCaL version: 2.1.3
% 42.97/6.51 % (2718901)Termination reason: Instruction limit
% 42.97/6.51 % (2718901)Termination phase: Saturation
% 42.97/6.51 % (2718901)Time elapsed: 0.295 s
% 42.97/6.51 % (2718901)Peak memory usage: 14 MB
% 42.97/6.51 % (2718901)Instructions burned: 478 (million)
% 42.97/6.51 % (2718863)Instruction limit reached!
% 42.97/6.51 % (2718863)------------------------------
% 42.97/6.51 % (2718863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.97/6.51 % (2718863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.97/6.51 % (2718863)CaDiCaL version: 2.1.3
% 42.97/6.51 % (2718863)Termination reason: Instruction limit
% 42.97/6.51 % (2718863)Termination phase: Saturation
% 42.97/6.51 % (2718863)Time elapsed: 0.399 s
% 42.97/6.51 % (2718863)Peak memory usage: 19 MB
% 42.97/6.51 % (2718863)Instructions burned: 686 (million)
% 42.97/6.51 % (2718977)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2697164531:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 42.97/6.51 % (2718979)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3922246596:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 42.97/6.51 % (2718925)Instruction limit reached!
% 42.97/6.51 % (2718925)------------------------------
% 42.97/6.51 % (2718925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.97/6.51 % (2718925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.97/6.51 % (2718925)CaDiCaL version: 2.1.3
% 42.97/6.51 % (2718925)Termination reason: Instruction limit
% 42.97/6.51 % (2718925)Termination phase: Finite model building SAT solving
% 42.97/6.51 % (2718925)Time elapsed: 0.361 s
% 42.97/6.51 % (2718925)Peak memory usage: 34 MB
% 42.97/6.51 % (2718925)Instructions burned: 867 (million)
% 42.97/6.51 % (2719026)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=526149093:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 42.97/6.51 % (2718979)Instruction limit reached!
% 42.97/6.51 % (2718979)------------------------------
% 94.64/14.22 % (2718979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.64/14.22 % (2718979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.64/14.22 % (2718979)CaDiCaL version: 2.1.3
% 94.64/14.22 % (2718979)Termination reason: Instruction limit
% 94.64/14.22 % (2718979)Termination phase: Saturation
% 94.64/14.22 % (2718979)Time elapsed: 0.391 s
% 94.64/14.22 % (2718979)Peak memory usage: 24 MB
% 94.64/14.22 % (2718979)Instructions burned: 692 (million)
% 94.64/14.22 % (2718977)Instruction limit reached!
% 94.64/14.22 % (2718977)------------------------------
% 94.64/14.22 % (2718977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.64/14.22 % (2718977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.64/14.22 % (2718977)CaDiCaL version: 2.1.3
% 94.64/14.22 % (2718977)Termination reason: Instruction limit
% 94.64/14.22 % (2718977)Termination phase: Finite model building constraint generation
% 94.64/14.22 % (2718977)Time elapsed: 0.410 s
% 94.64/14.22 % (2718977)Peak memory usage: 107 MB
% 94.64/14.22 % (2718977)Instructions burned: 890 (million)
% 94.64/14.22 % (2719096)fmb+10_1_sil=64000:random_seed=2872801231:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 94.64/14.22 % TRYING [1]
% 94.64/14.22 % TRYING [2]
% 94.64/14.22 % (2719097)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2781036853:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 94.64/14.22 % TRYING [20]
% 94.64/14.22 % TRYING [3]
% 94.64/14.22 % TRYING [4]
% 94.64/14.22 % (2719026)Instruction limit reached!
% 94.64/14.22 % (2719026)------------------------------
% 94.64/14.22 % (2719026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.64/14.22 % (2719026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.64/14.22 % (2719026)CaDiCaL version: 2.1.3
% 94.64/14.22 % (2719026)Termination reason: Instruction limit
% 94.64/14.22 % (2719026)Termination phase: Saturation
% 94.64/14.22 % (2719026)Time elapsed: 0.486 s
% 94.64/14.22 % (2719026)Peak memory usage: 20 MB
% 94.64/14.22 % (2719026)Instructions burned: 881 (million)
% 94.64/14.22 % (2718936)Instruction limit reached!
% 94.64/14.22 % (2718936)------------------------------
% 94.64/14.22 % (2718936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.64/14.22 % (2718936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.64/14.22 % (2718936)CaDiCaL version: 2.1.3
% 94.64/14.22 % (2718936)Termination reason: Instruction limit
% 94.64/14.22 % (2718936)Termination phase: Saturation
% 94.64/14.22 % (2718936)Time elapsed: 0.737 s
% 94.64/14.22 % (2718936)Peak memory usage: 28 MB
% 94.64/14.22 % (2718936)Instructions burned: 1179 (million)
% 94.64/14.22 % (2719100)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1071852136:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 94.64/14.22 % (2719101)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3054116277:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 94.64/14.22 % TRYING [8]
% 94.64/14.22 % TRYING [6]
% 94.64/14.22 % (2719100)Instruction limit reached!
% 94.64/14.22 % (2719100)------------------------------
% 94.64/14.22 % (2719100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.64/14.22 % (2719100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.64/14.22 % (2719100)CaDiCaL version: 2.1.3
% 94.64/14.22 % (2719100)Termination reason: Instruction limit
% 94.64/14.22 % (2719100)Termination phase: Finite model building constraint generation
% 94.64/14.22 % (2719100)Time elapsed: 0.285 s
% 94.64/14.22 % (2719100)Peak memory usage: 51 MB
% 94.64/14.22 % (2719100)Instructions burned: 924 (million)
% 94.64/14.22 % (2719104)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=899625374:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 94.64/14.22 % TRYING [5]
% 94.64/14.22 % (2719104)Instruction limit reached!
% 94.64/14.22 % (2719104)------------------------------
% 94.64/14.22 % (2719104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.64/14.22 % (2719104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.64/14.22 % (2719104)CaDiCaL version: 2.1.3
% 94.64/14.22 % (2719104)Termination reason: Instruction limit
% 94.64/14.22 % (2719104)Termination phase: Saturation
% 94.64/14.22 % (2719104)Time elapsed: 0.686 s
% 94.64/14.22 % (2719104)Peak memory usage: 23 MB
% 94.64/14.22 % (2719104)Instructions burned: 1474 (million)
% 94.64/14.22 % (2719106)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1174536326:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 94.64/14.22 % (2719106)Cannot represent all propositional literals internally
% 259.53/37.07 % (2719106)Refutation not found, incomplete strategy
% 259.53/37.07 % (2719106)------------------------------
% 259.53/37.07 % (2719106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 259.53/37.07 % (2719106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 259.53/37.07 % (2719106)CaDiCaL version: 2.1.3
% 259.53/37.07 % (2719106)Termination reason: Refutation not found, incomplete strategy
% 259.53/37.07 % (2719106)Time elapsed: 0.018 s
% 259.53/37.07 % (2719106)Peak memory usage: 11 MB
% 259.53/37.07 % (2719106)Instructions burned: 36 (million)
% 259.53/37.07 % (2719106)------------------------------
% 259.53/37.07 % (2719106)------------------------------
% 259.53/37.07 % (2719108)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3435143069:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 259.53/37.07 % TRYING [16]
% 259.53/37.07 % (2719108)Instruction limit reached!
% 259.53/37.07 % (2719108)------------------------------
% 259.53/37.07 % (2719108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 259.53/37.07 % (2719108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 259.53/37.07 % (2719108)CaDiCaL version: 2.1.3
% 259.53/37.07 % (2719108)Termination reason: Instruction limit
% 259.53/37.07 % (2719108)Termination phase: Finite model building constraint generation
% 259.53/37.07 % (2719108)Time elapsed: 0.749 s
% 259.53/37.07 % (2719108)Peak memory usage: 129 MB
% 259.53/37.07 % (2719108)Instructions burned: 2174 (million)
% 259.53/37.07 % (2719110)ott-2_1_sil=16000:newcnf=on:random_seed=3013843828:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi)
% 259.53/37.07 % (2719110)Instruction limit reached!
% 259.53/37.07 % (2719110)------------------------------
% 259.53/37.07 % (2719110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 259.53/37.07 % (2719110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 259.53/37.07 % (2719110)CaDiCaL version: 2.1.3
% 259.53/37.07 % (2719110)Termination reason: Instruction limit
% 259.53/37.07 % (2719110)Termination phase: Saturation
% 259.53/37.07 % (2719110)Time elapsed: 0.517 s
% 259.53/37.07 % (2719110)Peak memory usage: 19 MB
% 259.53/37.07 % (2719110)Instructions burned: 869 (million)
% 259.53/37.07 % (2719112)ott+10_1_sil=32000:tgt=ground:random_seed=1776979919:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi)
% 259.53/37.07 % TRYING [6]
% 259.53/37.07 % (2719101)Instruction limit reached!
% 259.53/37.07 % (2719101)------------------------------
% 259.53/37.07 % (2719101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 259.53/37.07 % (2719101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 259.53/37.07 % (2719101)CaDiCaL version: 2.1.3
% 259.53/37.07 % (2719101)Termination reason: Instruction limit
% 259.53/37.07 % (2719101)Termination phase: Saturation
% 259.53/37.07 % (2719101)Time elapsed: 2.709 s
% 259.53/37.07 % (2719101)Peak memory usage: 32 MB
% 259.53/37.07 % (2719101)Instructions burned: 5131 (million)
% 259.53/37.07 % (2719114)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3179649816:i=54282_2960 on theBenchmark for (2960ds/54282Mi)
% 259.53/37.07 % TRYING [1]
% 259.53/37.07 % TRYING [2]
% 259.53/37.07 % TRYING [3]
% 259.53/37.07 % TRYING [4]
% 259.53/37.07 % (2719097)Instruction limit reached!
% 259.53/37.07 % (2719097)------------------------------
% 259.53/37.07 % (2719097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 259.53/37.07 % (2719097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 259.53/37.07 % (2719097)CaDiCaL version: 2.1.3
% 259.53/37.07 % (2719097)Termination reason: Instruction limit
% 259.53/37.07 % (2719097)Termination phase: Finite model building constraint generation
% 259.53/37.07 % (2719097)Time elapsed: 3.045 s
% 259.53/37.07 % (2719097)Peak memory usage: 478 MB
% 259.53/37.07 % (2719097)Instructions burned: 9516 (million)
% 259.53/37.07 % (2719116)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3420052251:i=3512:aac=none_2959 on theBenchmark for (2959ds/3512Mi)
% 259.53/37.07 % TRYING [5]
% 259.53/37.07 % TRYING [7]
% 259.53/37.07 % TRYING [6]
% 259.53/37.07 % (2719116)Instruction limit reached!
% 259.53/37.07 % (2719116)------------------------------
% 259.53/37.07 % (2719116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 259.53/37.07 % (2719116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 259.53/37.07 % (2719116)CaDiCaL version: 2.1.3
% 259.53/37.07 % (2719116)Termination reason: Instruction limit
% 259.53/37.07 % (2719116)Termination phase: Saturation
% 259.53/37.07 % (2719116)Time elapsed: 1.937 s
% 259.53/37.07 % (2719116)Peak memory usage: 37 MB
% 259.53/37.07 % (2719116)Instructions burned: 3512 (million)
% 259.53/37.07 % (2719118)dis+21_1_sil=32000:sas=cadical:random_seed=1742937817:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi)
% 234.08/39.51 % (2719112)Instruction limit reached!
% 234.08/39.51 % (2719112)------------------------------
% 234.08/39.51 % (2719112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719112)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719112)Termination reason: Instruction limit
% 234.08/39.51 % (2719112)Termination phase: Saturation
% 234.08/39.51 % (2719112)Time elapsed: 2.863 s
% 234.08/39.51 % (2719112)Peak memory usage: 48 MB
% 234.08/39.51 % (2719112)Instructions burned: 5115 (million)
% 234.08/39.51 % (2719120)ott+11_1_sil=16000:gs=on:random_seed=100406217:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2935 on theBenchmark for (2935ds/2251Mi)
% 234.08/39.51 % (2719120)Instruction limit reached!
% 234.08/39.51 % (2719120)------------------------------
% 234.08/39.51 % (2719120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719120)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719120)Termination reason: Instruction limit
% 234.08/39.51 % (2719120)Termination phase: Saturation
% 234.08/39.51 % (2719120)Time elapsed: 1.647 s
% 234.08/39.51 % (2719120)Peak memory usage: 39 MB
% 234.08/39.51 % (2719120)Instructions burned: 2252 (million)
% 234.08/39.51 % (2719122)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=248797903:fmbsr=1.6:i=67534_2919 on theBenchmark for (2919ds/67534Mi)
% 234.08/39.51 % (2719118)Instruction limit reached!
% 234.08/39.51 % (2719118)------------------------------
% 234.08/39.51 % (2719118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719118)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719118)Termination reason: Instruction limit
% 234.08/39.51 % (2719118)Termination phase: Saturation
% 234.08/39.51 % (2719118)Time elapsed: 2.122 s
% 234.08/39.51 % (2719118)Peak memory usage: 38 MB
% 234.08/39.51 % (2719118)Instructions burned: 3773 (million)
% 234.08/39.51 % (2719124)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2132408497:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2917 on theBenchmark for (2917ds/4591Mi)
% 234.08/39.51 % TRYING [7]
% 234.08/39.51 % TRYING [7]
% 234.08/39.51 % (2719096)Instruction limit reached!
% 234.08/39.51 % (2719096)------------------------------
% 234.08/39.51 % (2719096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719096)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719096)Termination reason: Instruction limit
% 234.08/39.51 % (2719096)Termination phase: Finite model building SAT solving
% 234.08/39.51 % (2719096)Time elapsed: 8.159 s
% 234.08/39.51 % (2719096)Peak memory usage: 254 MB
% 234.08/39.51 % (2719096)Instructions burned: 22064 (million)
% 234.08/39.51 % (2719126)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=936285135:i=29340_2908 on theBenchmark for (2908ds/29340Mi)
% 234.08/39.51 % (2719124)Instruction limit reached!
% 234.08/39.51 % (2719124)------------------------------
% 234.08/39.51 % (2719124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719124)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719124)Termination reason: Instruction limit
% 234.08/39.51 % (2719124)Termination phase: Saturation
% 234.08/39.51 % (2719124)Time elapsed: 2.621 s
% 234.08/39.51 % (2719124)Peak memory usage: 93 MB
% 234.08/39.51 % (2719124)Instructions burned: 4592 (million)
% 234.08/39.51 % (2719128)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=389759036:i=5211_2891 on theBenchmark for (2891ds/5211Mi)
% 234.08/39.51 % (2719128)Instruction limit reached!
% 234.08/39.51 % (2719128)------------------------------
% 234.08/39.51 % (2719128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719128)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719128)Termination reason: Instruction limit
% 234.08/39.51 % (2719128)Termination phase: Saturation
% 234.08/39.51 % (2719128)Time elapsed: 2.875 s
% 234.08/39.51 % (2719128)Peak memory usage: 61 MB
% 234.08/39.51 % (2719128)Instructions burned: 5211 (million)
% 234.08/39.51 % (2719252)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=683081002:i=5497:nm=2_2862 on theBenchmark for (2862ds/5497Mi)
% 234.08/39.51 % TRYING [17]
% 234.08/39.51 % (2719252)Instruction limit reached!
% 234.08/39.51 % (2719252)------------------------------
% 234.08/39.51 % (2719252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719252)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719252)Termination reason: Instruction limit
% 234.08/39.51 % (2719252)Termination phase: Finite model building constraint generation
% 234.08/39.51 % (2719252)Time elapsed: 2.177 s
% 234.08/39.51 % (2719252)Peak memory usage: 283 MB
% 234.08/39.51 % (2719252)Instructions burned: 5500 (million)
% 234.08/39.51 % (2719390)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4029241854:fmbsr=2:i=46332_2840 on theBenchmark for (2840ds/46332Mi)
% 234.08/39.51 % TRYING [15]
% 234.08/39.51 % TRYING [8]
% 234.08/39.51 % TRYING [8]
% 234.08/39.51 % (2719126)Instruction limit reached!
% 234.08/39.51 % (2719126)------------------------------
% 234.08/39.51 % (2719126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719126)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719126)Termination reason: Instruction limit
% 234.08/39.51 % (2719126)Termination phase: Saturation
% 234.08/39.51 % (2719126)Time elapsed: 14.048 s
% 234.08/39.51 % (2719126)Peak memory usage: 286 MB
% 234.08/39.51 % (2719126)Instructions burned: 29342 (million)
% 234.08/39.51 % (2719546)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1371803110:i=14071_2767 on theBenchmark for (2767ds/14071Mi)
% 234.08/39.51 % TRYING [12]
% 234.08/39.51 % (2719546)Instruction limit reached!
% 234.08/39.51 % (2719546)------------------------------
% 234.08/39.51 % (2719546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719546)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719546)Termination reason: Instruction limit
% 234.08/39.51 % (2719546)Termination phase: Finite model building constraint generation
% 234.08/39.51 % (2719546)Time elapsed: 4.410 s
% 234.08/39.51 % (2719546)Peak memory usage: 637 MB
% 234.08/39.51 % (2719546)Instructions burned: 14073 (million)
% 234.08/39.51 % (2719548)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=560529284:i=22565:add=on:rawr=on_2722 on theBenchmark for (2722ds/22565Mi)
% 234.08/39.51 % (2719390)Instruction limit reached!
% 234.08/39.51 % (2719390)------------------------------
% 234.08/39.51 % (2719390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719390)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719390)Termination reason: Instruction limit
% 234.08/39.51 % (2719390)Termination phase: Finite model building constraint generation
% 234.08/39.51 % (2719390)Time elapsed: 15.325 s
% 234.08/39.51 % (2719390)Peak memory usage: 1679 MB
% 234.08/39.51 % (2719390)Instructions burned: 46333 (million)
% 234.08/39.51 % (2719807)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=467287659:i=8173:av=off_2683 on theBenchmark for (2683ds/8173Mi)
% 234.08/39.51 % (2719114)Instruction limit reached!
% 234.08/39.51 % (2719114)------------------------------
% 234.08/39.51 % (2719114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719114)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719114)Termination reason: Instruction limit
% 234.08/39.51 % (2719114)Termination phase: Finite model building constraint generation
% 234.08/39.51 % (2719114)Time elapsed: 28.331 s
% 234.08/39.51 % (2719114)Peak memory usage: 1310 MB
% 234.08/39.51 % (2719114)Instructions burned: 54283 (million)
% 234.08/39.51 % (2719962)dis+10_16:1_sil=16000:random_seed=3392313806:i=9155:fsr=off_2675 on theBenchmark for (2675ds/9155Mi)
% 234.08/39.51 % (2719807)Instruction limit reached!
% 234.08/39.51 % (2719807)------------------------------
% 234.08/39.51 % (2719807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719807)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719807)Termination reason: Instruction limit
% 234.08/39.51 % (2719807)Termination phase: Saturation
% 234.08/39.51 % (2719807)Time elapsed: 4.936 s
% 234.08/39.51 % (2719807)Peak memory usage: 105 MB
% 234.08/39.51 % (2719807)Instructions burned: 8173 (million)
% 234.08/39.51 % (2719967)ott-3_8_sil=64000:random_seed=2618715264:i=20139:bs=on_2633 on theBenchmark for (2633ds/20139Mi)
% 234.08/39.51 % (2719962)Instruction limit reached!
% 234.08/39.51 % (2719962)------------------------------
% 234.08/39.51 % (2719962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719962)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719962)Termination reason: Instruction limit
% 234.08/39.51 % (2719962)Termination phase: Saturation
% 234.08/39.51 % (2719962)Time elapsed: 4.881 s
% 234.08/39.51 % (2719962)Peak memory usage: 70 MB
% 234.08/39.51 % (2719962)Instructions burned: 9156 (million)
% 234.08/39.51 % (2719969)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3759134663:fmbsr=2:i=32576_2626 on theBenchmark for (2626ds/32576Mi)
% 234.08/39.51 % TRYING [9]
% 234.08/39.51 % (2719548)Instruction limit reached!
% 234.08/39.51 % (2719548)------------------------------
% 234.08/39.51 % (2719548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719548)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719548)Termination reason: Instruction limit
% 234.08/39.51 % (2719548)Termination phase: Saturation
% 234.08/39.51 % (2719548)Time elapsed: 9.620 s
% 234.08/39.51 % (2719548)Peak memory usage: 71 MB
% 234.08/39.51 % (2719548)Instructions burned: 22566 (million)
% 234.08/39.51 % (2719971)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3976514096:i=11404_2625 on theBenchmark for (2625ds/11404Mi)
% 234.08/39.51 % (2718813)Instruction limit reached!
% 234.08/39.51 % (2718813)------------------------------
% 234.08/39.51 % (2718813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2718813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2718813)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2718813)Termination reason: Instruction limit
% 234.08/39.51 % (2718813)Termination phase: Saturation
% 234.08/39.51 % (2718813)Time elapsed: 38.289 s
% 234.08/39.51 % (2718813)Peak memory usage: 232 MB
% 234.08/39.51 % (2718813)Instructions burned: 88024 (million)
% 234.08/39.51 % (2719122)Instruction limit reached!
% 234.08/39.51 % (2719122)------------------------------
% 234.08/39.51 % (2719122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.51 % (2719122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.51 % (2719122)CaDiCaL version: 2.1.3
% 234.08/39.51 % (2719122)Termination reason: Instruction limit
% 234.08/39.51 % (2719122)Termination phase: Finite model building SAT solving
% 234.08/39.51 % (2719122)Time elapsed: 30.214 s
% 234.08/39.51 % (2719122)Peak memory usage: 836 MB
% 234.08/39.51 % (2719122)Instructions burned: 67534 (million)
% 234.08/39.51 % (2719973)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2177931482:i=14134_2616 on theBenchmark for (2616ds/14134Mi)
% 234.08/39.51 % (2719975)dis+33_16_sil=32000:sac=on:random_seed=1600345813:i=15851:nm=0_2615 on theBenchmark for (2615ds/15851Mi)
% 234.08/39.51 % (2719967) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2718792-2719967"...
% 234.08/39.51 % (2719967)...printing done.
% 234.08/39.51 % (2719967)Refutation found. Thanks to Tanya!
% 234.08/39.51 % SZS status Theorem for theBenchmark
% 234.08/39.51 % SZS output start Proof for theBenchmark
% See solution above
% 234.08/39.52 % (2719967)------------------------------
% 234.08/39.52 % (2719967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 234.08/39.52 % (2719967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.08/39.52 % (2719967)CaDiCaL version: 2.1.3
% 234.08/39.52 % (2719967)Termination reason: Refutation
% 234.08/39.52 % (2719967)Time elapsed: 2.073 s
% 234.08/39.52 % (2719967)Peak memory usage: 35 MB
% 234.08/39.52 % (2719967)Instructions burned: 3253 (million)
% 234.08/39.52 % (2718792)Success in time 39.077 s
% 234.08/39.52 % Vampire exiting
%------------------------------------------------------------------------------