%------------------------------------------------------------------------------
% 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/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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 15.53s 2.64s
% Output : Refutation 15.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 39
% Syntax : Number of formulae : 299 ( 53 unt; 0 typ; 29 def)
% Number of atoms : 2493 ( 173 equ)
% Maximal formula atoms : 55 ( 8 avg)
% Number of connectives : 1397 ( 435 ~; 785 |; 77 &)
% ( 55 <=>; 41 =>; 0 <=; 4 <~>)
% Maximal formula depth : 33 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of FOOLs : 1232 (1232 fml; 0 var)
% Number of types : 4 ( 2 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 42 ( 39 usr; 38 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 5 con; 0-5 aty)
% Number of variables : 413 ( 0 sgn 404 !; 9 ?; 413 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
del: $tType ).
tff(type_def_6,type,
tp__o: $tType ).
tff(func_def_0,type,
bool: del ).
tff(func_def_1,type,
ind: del ).
tff(func_def_2,type,
arr: ( del * del ) > del ).
tff(func_def_4,type,
k: ( del * $i ) > $i ).
tff(func_def_5,type,
i: del > $i ).
tff(func_def_6,type,
ty_2Eoption_2Eoption: del > del ).
tff(func_def_7,type,
c_2Eoption_2EOPTION__JOIN: del > $i ).
tff(func_def_8,type,
c_2Eoption_2EOPTION__MAP: ( del * del ) > $i ).
tff(func_def_9,type,
c_2Eoption_2Eoption__CASE: ( del * del ) > $i ).
tff(func_def_10,type,
inj__o: tp__o > $i ).
tff(func_def_11,type,
surj__o: $i > tp__o ).
tff(func_def_13,type,
fo__c_2Emin_2E_3D_3D_3E: ( tp__o * tp__o ) > tp__o ).
tff(func_def_14,type,
c_2Eoption_2EIS__NONE: del > $i ).
tff(func_def_16,type,
fo__c_2Ebool_2EF: tp__o ).
tff(func_def_18,type,
fo__c_2Ebool_2ET: tp__o ).
tff(func_def_19,type,
c_2Eoption_2EIS__SOME: del > $i ).
tff(func_def_21,type,
fo__c_2Ebool_2E_7E: tp__o > tp__o ).
tff(func_def_22,type,
c_2Eoption_2ETHE: del > $i ).
tff(func_def_23,type,
c_2Eoption_2ESOME: del > $i ).
tff(func_def_24,type,
c_2Ebool_2E_3F: del > $i ).
tff(func_def_25,type,
c_2Eoption_2ENONE: del > $i ).
tff(func_def_27,type,
fo__c_2Ebool_2E_2F_5C: ( tp__o * tp__o ) > tp__o ).
tff(func_def_29,type,
fo__c_2Ebool_2E_5C_2F: ( tp__o * tp__o ) > tp__o ).
tff(func_def_30,type,
c_2Eoption_2EOPTREL: ( del * del ) > $i ).
tff(func_def_31,type,
c_2Emin_2E_3D: del > $i ).
tff(func_def_32,type,
c_2Ebool_2E_21: del > $i ).
tff(func_def_33,type,
sK0: ( del * $i * $i ) > $i ).
tff(func_def_34,type,
sK1: ( del * $i ) > $i ).
tff(func_def_35,type,
sK2: ( del * $i ) > $i ).
tff(func_def_36,type,
sK3: ( del * tp__o ) > $i ).
tff(func_def_37,type,
sK4: ( del * del * $i * $i * $i ) > $i ).
tff(func_def_38,type,
sK5: ( del * del * $i * $i * $i ) > $i ).
tff(func_def_39,type,
sK6: del ).
tff(pred_def_1,type,
mem: ( $i * del ) > $o ).
tff(f1,axiom,
! [X0: del,X1: del,X2: $i] :
( mem(X2,arr(X0,X1))
=> ! [X3: $i] :
( mem(X3,X0)
=> mem(ap(X2,X3),X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001_2.ax',ap_tp) ).
tff(f20,axiom,
inj__o(fo__c_2Ebool_2ET) = c_2Ebool_2ET,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',stp_eq_fo_c_2Ebool_2ET) ).
tff(f21,axiom,
p(c_2Ebool_2ET),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_true_p) ).
tff(f27,axiom,
! [X0: del] : mem(c_2Eoption_2ESOME(X0),arr(X0,ty_2Eoption_2Eoption(X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Eoption_2ESOME) ).
tff(f30,axiom,
! [X0: del] : mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Eoption_2ENONE) ).
tff(f38,axiom,
! [X0: del] : mem(c_2Emin_2E_3D(X0),arr(X0,arr(X0,bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Emin_2E_3D) ).
tff(f45,axiom,
! [X0: del,X1: tp__o] :
( ? [X2: $i] :
( mem(X2,X0)
& p(inj__o(X1)) )
<=> p(inj__o(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ebool_2EEXISTS__SIMP) ).
tff(f51,axiom,
! [X0: del,X1: del,X2: $i] :
( mem(X2,X1)
=> ! [X3: $i] :
( mem(X3,arr(X0,X1))
=> ! [X4: $i] :
( mem(X4,ty_2Eoption_2Eoption(X0))
=> ( ! [X5: $i] :
( mem(X5,X0)
=> ! [X6: $i] :
( mem(X6,X0)
=> ( ( ap(c_2Eoption_2ESOME(X0),X5) = ap(c_2Eoption_2ESOME(X0),X6) )
<=> ( X5 = X6 ) ) ) )
& ! [X7: $i] :
( mem(X7,X0)
=> ( ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X7)) = X7 ) )
& ! [X8: $i] :
( mem(X8,X0)
=> ( c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X8) ) )
& ! [X9: $i] :
( mem(X9,X0)
=> ( ap(c_2Eoption_2ESOME(X0),X9) != c_2Eoption_2ENONE(X0) ) )
& ! [X10: $i] :
( 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: $i] :
( mem(X11,ty_2Eoption_2Eoption(X0))
=> ( p(ap(c_2Eoption_2EIS__NONE(X0),X11))
<=> ( X11 = c_2Eoption_2ENONE(X0) ) ) )
& ! [X12: $i] :
( mem(X12,ty_2Eoption_2Eoption(X0))
=> ( ~ p(ap(c_2Eoption_2EIS__SOME(X0),X12))
<=> ( X12 = c_2Eoption_2ENONE(X0) ) ) )
& ! [X13: $i] :
( 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: $i] :
( 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: $i] :
( 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: $i] :
( 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: $i] :
( 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: $i] :
( 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: $i] :
( mem(X19,X1)
=> ! [X20: $i] :
( mem(X20,arr(X0,X1))
=> ( ap(ap(ap(c_2Eoption_2Eoption__CASE(X0,X1),c_2Eoption_2ENONE(X0)),X19),X20) = X19 ) ) )
& ! [X21: $i] :
( mem(X21,X0)
=> ! [X22: $i] :
( mem(X22,X1)
=> ! [X23: $i] :
( 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: $i] :
( mem(X24,arr(X0,X1))
=> ! [X25: $i] :
( 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: $i] :
( 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: $i] :
( 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/sandbox/benchmark/theBenchmark.p',conj_thm_2Eoption_2Eoption__CLAUSES) ).
tff(f52,axiom,
! [X0: del,X1: del,X2: $i] :
( mem(X2,arr(X0,arr(X1,bool)))
=> ! [X3: $i] :
( mem(X3,ty_2Eoption_2Eoption(X0))
=> ! [X4: $i] :
( 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: $i] :
( mem(X5,X0)
& ? [X6: $i] :
( mem(X6,X1)
& ( X3 = ap(c_2Eoption_2ESOME(X0),X5) )
& ( X4 = ap(c_2Eoption_2ESOME(X1),X6) )
& p(ap(ap(X2,X5),X6)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_thm_2Eoption_2EOPTREL__def) ).
tff(f53,conjecture,
! [X0: del,X1: $i] :
( mem(X1,arr(X0,arr(X0,bool)))
=> ! [X2: $i] :
( mem(X2,X0)
=> ! [X3: $i] :
( mem(X3,X0)
=> ( ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X0)))
<=> $true )
& ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),c_2Eoption_2ENONE(X0)))
<=> $false )
& ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),c_2Eoption_2ENONE(X0)),ap(c_2Eoption_2ESOME(X0),X3)))
<=> $false )
& ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X0),X1),ap(c_2Eoption_2ESOME(X0),X2)),ap(c_2Eoption_2ESOME(X0),X3)))
<=> p(ap(ap(X1,X2),X3)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Equotient__option_2EOPTION__REL__def) ).
tff(f54,negated_conjecture,
~ ! [X0: del,X1: $i] :
( mem(X1,arr(X0,arr(X0,bool)))
=> ! [X2: $i] :
( mem(X2,X0)
=> ! [X3: $i] :
( 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)],[f53]) ).
tff(f55,plain,
! [X0: del,X1: del,X2: $i] :
( ! [X3: $i] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f1]) ).
tff(f75,plain,
! [X0: del,X1: del,X2: $i] :
( ! [X3: $i] :
( ! [X4: $i] :
( ( ! [X5: $i] :
( ! [X6: $i] :
( ( ( ap(c_2Eoption_2ESOME(X0),X5) = ap(c_2Eoption_2ESOME(X0),X6) )
<=> ( X5 = X6 ) )
| ~ mem(X6,X0) )
| ~ mem(X5,X0) )
& ! [X7: $i] :
( ( ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X7)) = X7 )
| ~ mem(X7,X0) )
& ! [X8: $i] :
( ( c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X8) )
| ~ mem(X8,X0) )
& ! [X9: $i] :
( ( ap(c_2Eoption_2ESOME(X0),X9) != c_2Eoption_2ENONE(X0) )
| ~ mem(X9,X0) )
& ! [X10: $i] :
( ( p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X10)))
<=> $true )
| ~ mem(X10,X0) )
& ( p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0)))
<=> $false )
& ! [X11: $i] :
( ( p(ap(c_2Eoption_2EIS__NONE(X0),X11))
<=> ( X11 = c_2Eoption_2ENONE(X0) ) )
| ~ mem(X11,ty_2Eoption_2Eoption(X0)) )
& ! [X12: $i] :
( ( ~ p(ap(c_2Eoption_2EIS__SOME(X0),X12))
<=> ( X12 = c_2Eoption_2ENONE(X0) ) )
| ~ mem(X12,ty_2Eoption_2Eoption(X0)) )
& ! [X13: $i] :
( ( 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: $i] :
( ( 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: $i] :
( ( 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: $i] :
( ( 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: $i] :
( ( 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: $i] :
( ( 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: $i] :
( ! [X20: $i] :
( ( 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: $i] :
( ! [X22: $i] :
( ! [X23: $i] :
( ( 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: $i] :
( ! [X25: $i] :
( ( 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: $i] :
( ( 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: $i] :
( ( 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) ),
inference(ennf_transformation,[],[f51]) ).
tff(f76,plain,
! [X0: del,X1: del,X2: $i] :
( ! [X3: $i] :
( ! [X4: $i] :
( ( ! [X5: $i] :
( ! [X6: $i] :
( ( ( ap(c_2Eoption_2ESOME(X0),X5) = ap(c_2Eoption_2ESOME(X0),X6) )
<=> ( X5 = X6 ) )
| ~ mem(X6,X0) )
| ~ mem(X5,X0) )
& ! [X7: $i] :
( ( ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X7)) = X7 )
| ~ mem(X7,X0) )
& ! [X8: $i] :
( ( c_2Eoption_2ENONE(X0) != ap(c_2Eoption_2ESOME(X0),X8) )
| ~ mem(X8,X0) )
& ! [X9: $i] :
( ( ap(c_2Eoption_2ESOME(X0),X9) != c_2Eoption_2ENONE(X0) )
| ~ mem(X9,X0) )
& ! [X10: $i] :
( ( p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X10)))
<=> $true )
| ~ mem(X10,X0) )
& ( p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0)))
<=> $false )
& ! [X11: $i] :
( ( p(ap(c_2Eoption_2EIS__NONE(X0),X11))
<=> ( X11 = c_2Eoption_2ENONE(X0) ) )
| ~ mem(X11,ty_2Eoption_2Eoption(X0)) )
& ! [X12: $i] :
( ( ~ p(ap(c_2Eoption_2EIS__SOME(X0),X12))
<=> ( X12 = c_2Eoption_2ENONE(X0) ) )
| ~ mem(X12,ty_2Eoption_2Eoption(X0)) )
& ! [X13: $i] :
( ( 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: $i] :
( ( 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: $i] :
( ( 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: $i] :
( ( 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: $i] :
( ( 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: $i] :
( ( 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: $i] :
( ! [X20: $i] :
( ( 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: $i] :
( ! [X22: $i] :
( ! [X23: $i] :
( ( 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: $i] :
( ! [X25: $i] :
( ( 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: $i] :
( ( 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: $i] :
( ( 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) ),
inference(flattening,[],[f75]) ).
tff(f77,plain,
! [X0: del,X1: del,X2: $i] :
( ! [X3: $i] :
( ! [X4: $i] :
( ( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
<=> ( ( ( X3 = c_2Eoption_2ENONE(X0) )
& ( X4 = c_2Eoption_2ENONE(X1) ) )
| ? [X5: $i] :
( mem(X5,X0)
& ? [X6: $i] :
( 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))) ),
inference(ennf_transformation,[],[f52]) ).
tff(f78,plain,
? [X0: del,X1: $i] :
( ? [X2: $i] :
( ? [X3: $i] :
( ( ( 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)) ) )
& mem(X3,X0) )
& mem(X2,X0) )
& mem(X1,arr(X0,arr(X0,bool))) ),
inference(ennf_transformation,[],[f54]) ).
tff(f79,plain,
! [X2: $i,X3: $i,X0: del,X1: del] :
( ~ mem(X2,arr(X0,X1))
| ~ mem(X3,X0)
| mem(ap(X2,X3),X1) ),
inference(cnf_transformation,[],[f55]) ).
tff(f102,plain,
c_2Ebool_2ET = inj__o(fo__c_2Ebool_2ET),
inference(cnf_transformation,[],[f20]) ).
tff(f103,plain,
p(c_2Ebool_2ET),
inference(cnf_transformation,[],[f21]) ).
tff(f110,plain,
! [X0: del] : mem(c_2Eoption_2ESOME(X0),arr(X0,ty_2Eoption_2Eoption(X0))),
inference(cnf_transformation,[],[f27]) ).
tff(f115,plain,
! [X0: del] : mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0)),
inference(cnf_transformation,[],[f30]) ).
tff(f127,plain,
! [X0: del] : mem(c_2Emin_2E_3D(X0),arr(X0,arr(X0,bool))),
inference(cnf_transformation,[],[f38]) ).
tff(f134,plain,
! [X0: del,X1: tp__o] :
( ~ p(inj__o(X1))
| mem(sK3(X0,X1),X0) ),
inference(cnf_transformation,[],[f45]) ).
tff(f139,plain,
! [X2: $i,X3: $i,X10: $i,X0: del,X1: del,X4: $i] :
( ~ mem(X2,X1)
| ~ mem(X3,arr(X0,X1))
| ~ mem(X4,ty_2Eoption_2Eoption(X0))
| ~ mem(X10,X0)
| p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X10))) ),
inference(cnf_transformation,[],[f76]) ).
tff(f146,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X7: $i,X4: $i] :
( ~ mem(X2,X1)
| ~ mem(X3,arr(X0,X1))
| ~ mem(X4,ty_2Eoption_2Eoption(X0))
| ~ mem(X7,X0)
| ( ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X7)) = X7 ) ),
inference(cnf_transformation,[],[f76]) ).
tff(f149,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ mem(X2,X1)
| ~ mem(X3,arr(X0,X1))
| ~ mem(X4,ty_2Eoption_2Eoption(X0))
| ~ p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0))) ),
inference(cnf_transformation,[],[f76]) ).
tff(f161,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ( ap(c_2Eoption_2ESOME(X0),sK4(X0,X1,X2,X3,X4)) = X3 )
| ( c_2Eoption_2ENONE(X1) = X4 )
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ),
inference(cnf_transformation,[],[f77]) ).
tff(f162,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| mem(sK5(X0,X1,X2,X3,X4),X1)
| ( c_2Eoption_2ENONE(X1) = X4 )
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ),
inference(cnf_transformation,[],[f77]) ).
tff(f163,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| p(ap(ap(X2,sK4(X0,X1,X2,X3,X4)),sK5(X0,X1,X2,X3,X4)))
| ( c_2Eoption_2ENONE(X0) = X3 )
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ),
inference(cnf_transformation,[],[f77]) ).
tff(f164,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ( ap(c_2Eoption_2ESOME(X1),sK5(X0,X1,X2,X3,X4)) = X4 )
| ( c_2Eoption_2ENONE(X0) = X3 )
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ),
inference(cnf_transformation,[],[f77]) ).
tff(f165,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ( ap(c_2Eoption_2ESOME(X0),sK4(X0,X1,X2,X3,X4)) = X3 )
| ( c_2Eoption_2ENONE(X0) = X3 )
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ),
inference(cnf_transformation,[],[f77]) ).
tff(f166,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| mem(sK5(X0,X1,X2,X3,X4),X1)
| ( c_2Eoption_2ENONE(X0) = X3 )
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ),
inference(cnf_transformation,[],[f77]) ).
tff(f167,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X6: $i,X4: $i,X5: $i] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ~ p(ap(ap(X2,X5),X6))
| ( ap(c_2Eoption_2ESOME(X1),X6) != X4 )
| ( ap(c_2Eoption_2ESOME(X0),X5) != X3 )
| ~ mem(X6,X1)
| ~ mem(X5,X0)
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ),
inference(cnf_transformation,[],[f77]) ).
tff(f168,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| mem(sK4(X0,X1,X2,X3,X4),X0)
| ( c_2Eoption_2ENONE(X0) = X3 )
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ),
inference(cnf_transformation,[],[f77]) ).
tff(f169,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| mem(sK4(X0,X1,X2,X3,X4),X0)
| ( c_2Eoption_2ENONE(X1) = X4 )
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ),
inference(cnf_transformation,[],[f77]) ).
tff(f170,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(X4,ty_2Eoption_2Eoption(X1))
| ( c_2Eoption_2ENONE(X1) != X4 )
| ( c_2Eoption_2ENONE(X0) != X3 )
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4)) ),
inference(cnf_transformation,[],[f77]) ).
tff(f171,plain,
sP12,
inference(cnf_transformation,[],[f78]) ).
tff(f172,plain,
~ sP11,
inference(cnf_transformation,[],[f78]) ).
tff(f173,plain,
~ sP10,
inference(cnf_transformation,[],[f78]) ).
tff(f177,plain,
( ~ p(ap(ap(sK7,sK8),sK9))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),ap(c_2Eoption_2ESOME(sK6),sK9)))
| sP10
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),c_2Eoption_2ENONE(sK6)),ap(c_2Eoption_2ESOME(sK6),sK9)))
| sP11
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),c_2Eoption_2ENONE(sK6)))
| ~ sP12
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),c_2Eoption_2ENONE(sK6)),c_2Eoption_2ENONE(sK6))) ),
inference(cnf_transformation,[],[f78]) ).
tff(f185,plain,
( p(ap(ap(sK7,sK8),sK9))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),ap(c_2Eoption_2ESOME(sK6),sK9)))
| sP10
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),c_2Eoption_2ENONE(sK6)),ap(c_2Eoption_2ESOME(sK6),sK9)))
| sP11
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),c_2Eoption_2ENONE(sK6)))
| ~ sP12
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),c_2Eoption_2ENONE(sK6)),c_2Eoption_2ENONE(sK6))) ),
inference(cnf_transformation,[],[f78]) ).
tff(f190,plain,
mem(sK9,sK6),
inference(cnf_transformation,[],[f78]) ).
tff(f191,plain,
mem(sK8,sK6),
inference(cnf_transformation,[],[f78]) ).
tff(f192,plain,
mem(sK7,arr(sK6,arr(sK6,bool))),
inference(cnf_transformation,[],[f78]) ).
tff(f197,plain,
! [X2: $i,X3: $i,X0: del,X1: del] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(c_2Eoption_2ENONE(X1),ty_2Eoption_2Eoption(X1))
| ( c_2Eoption_2ENONE(X0) != X3 )
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),c_2Eoption_2ENONE(X1))) ),
inference(equality_resolution,[],[f170]) ).
tff(f198,plain,
! [X2: $i,X0: del,X1: del] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0))
| ~ mem(c_2Eoption_2ENONE(X1),ty_2Eoption_2Eoption(X1))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X1))) ),
inference(equality_resolution,[],[f197]) ).
tff(f199,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X6: $i,X5: $i] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(X3,ty_2Eoption_2Eoption(X0))
| ~ mem(ap(c_2Eoption_2ESOME(X1),X6),ty_2Eoption_2Eoption(X1))
| ~ p(ap(ap(X2,X5),X6))
| ( ap(c_2Eoption_2ESOME(X0),X5) != X3 )
| ~ mem(X6,X1)
| ~ mem(X5,X0)
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),ap(c_2Eoption_2ESOME(X1),X6))) ),
inference(equality_resolution,[],[f167]) ).
tff(f200,plain,
! [X2: $i,X0: del,X1: del,X6: $i,X5: $i] :
( ~ mem(X2,arr(X0,arr(X1,bool)))
| ~ mem(ap(c_2Eoption_2ESOME(X0),X5),ty_2Eoption_2Eoption(X0))
| ~ mem(ap(c_2Eoption_2ESOME(X1),X6),ty_2Eoption_2Eoption(X1))
| ~ p(ap(ap(X2,X5),X6))
| ~ mem(X6,X1)
| ~ mem(X5,X0)
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),ap(c_2Eoption_2ESOME(X0),X5)),ap(c_2Eoption_2ESOME(X1),X6))) ),
inference(equality_resolution,[],[f199]) ).
tff(f201,plain,
! [X2: $i,X3: $i,X0: del,X1: del] :
( ~ mem(ap(X2,X3),X1)
| mem(X3,X0)
| mem(X2,arr(X0,X1)) ),
inference(consistent_polarity_flipping,[],[f79]) ).
tff(f225,plain,
! [X0: del] : ~ mem(c_2Eoption_2ESOME(X0),arr(X0,ty_2Eoption_2Eoption(X0))),
inference(consistent_polarity_flipping,[],[f110]) ).
tff(f230,plain,
! [X0: del] : ~ mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0)),
inference(consistent_polarity_flipping,[],[f115]) ).
tff(f240,plain,
! [X0: del] : ~ mem(c_2Emin_2E_3D(X0),arr(X0,arr(X0,bool))),
inference(consistent_polarity_flipping,[],[f127]) ).
tff(f247,plain,
! [X0: del,X1: tp__o] :
( ~ mem(sK3(X0,X1),X0)
| ~ p(inj__o(X1)) ),
inference(consistent_polarity_flipping,[],[f134]) ).
tff(f258,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ p(ap(c_2Eoption_2EIS__SOME(X0),c_2Eoption_2ENONE(X0)))
| mem(X3,arr(X0,X1))
| mem(X4,ty_2Eoption_2Eoption(X0))
| mem(X2,X1) ),
inference(consistent_polarity_flipping,[],[f149]) ).
tff(f261,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X7: $i,X4: $i] :
( mem(X2,X1)
| mem(X3,arr(X0,X1))
| mem(X4,ty_2Eoption_2Eoption(X0))
| mem(X7,X0)
| ( ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X7)) = X7 ) ),
inference(consistent_polarity_flipping,[],[f146]) ).
tff(f268,plain,
! [X2: $i,X3: $i,X10: $i,X0: del,X1: del,X4: $i] :
( mem(X2,X1)
| mem(X3,arr(X0,X1))
| mem(X4,ty_2Eoption_2Eoption(X0))
| p(ap(c_2Eoption_2EIS__SOME(X0),ap(c_2Eoption_2ESOME(X0),X10)))
| mem(X10,X0) ),
inference(consistent_polarity_flipping,[],[f139]) ).
tff(f272,plain,
! [X2: $i,X0: del,X1: del] :
( mem(X2,arr(X0,arr(X1,bool)))
| mem(c_2Eoption_2ENONE(X0),ty_2Eoption_2Eoption(X0))
| mem(c_2Eoption_2ENONE(X1),ty_2Eoption_2Eoption(X1))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X1))) ),
inference(consistent_polarity_flipping,[],[f198]) ).
tff(f273,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| mem(X3,ty_2Eoption_2Eoption(X0))
| mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(sK4(X0,X1,X2,X3,X4),X0)
| ( c_2Eoption_2ENONE(X1) = X4 )
| mem(X2,arr(X0,arr(X1,bool))) ),
inference(consistent_polarity_flipping,[],[f169]) ).
tff(f274,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| mem(X3,ty_2Eoption_2Eoption(X0))
| mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(sK4(X0,X1,X2,X3,X4),X0)
| ( c_2Eoption_2ENONE(X0) = X3 )
| mem(X2,arr(X0,arr(X1,bool))) ),
inference(consistent_polarity_flipping,[],[f168]) ).
tff(f275,plain,
! [X2: $i,X0: del,X1: del,X6: $i,X5: $i] :
( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),ap(c_2Eoption_2ESOME(X0),X5)),ap(c_2Eoption_2ESOME(X1),X6)))
| mem(ap(c_2Eoption_2ESOME(X0),X5),ty_2Eoption_2Eoption(X0))
| mem(ap(c_2Eoption_2ESOME(X1),X6),ty_2Eoption_2Eoption(X1))
| ~ p(ap(ap(X2,X5),X6))
| mem(X6,X1)
| mem(X5,X0)
| mem(X2,arr(X0,arr(X1,bool))) ),
inference(consistent_polarity_flipping,[],[f200]) ).
tff(f276,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| mem(X3,ty_2Eoption_2Eoption(X0))
| mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(sK5(X0,X1,X2,X3,X4),X1)
| ( c_2Eoption_2ENONE(X0) = X3 )
| mem(X2,arr(X0,arr(X1,bool))) ),
inference(consistent_polarity_flipping,[],[f166]) ).
tff(f277,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| mem(X3,ty_2Eoption_2Eoption(X0))
| mem(X4,ty_2Eoption_2Eoption(X1))
| ( ap(c_2Eoption_2ESOME(X0),sK4(X0,X1,X2,X3,X4)) = X3 )
| ( c_2Eoption_2ENONE(X0) = X3 )
| mem(X2,arr(X0,arr(X1,bool))) ),
inference(consistent_polarity_flipping,[],[f165]) ).
tff(f278,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| mem(X3,ty_2Eoption_2Eoption(X0))
| mem(X4,ty_2Eoption_2Eoption(X1))
| ( ap(c_2Eoption_2ESOME(X1),sK5(X0,X1,X2,X3,X4)) = X4 )
| ( c_2Eoption_2ENONE(X0) = X3 )
| mem(X2,arr(X0,arr(X1,bool))) ),
inference(consistent_polarity_flipping,[],[f164]) ).
tff(f279,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| mem(X3,ty_2Eoption_2Eoption(X0))
| mem(X4,ty_2Eoption_2Eoption(X1))
| p(ap(ap(X2,sK4(X0,X1,X2,X3,X4)),sK5(X0,X1,X2,X3,X4)))
| ( c_2Eoption_2ENONE(X0) = X3 )
| mem(X2,arr(X0,arr(X1,bool))) ),
inference(consistent_polarity_flipping,[],[f163]) ).
tff(f280,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| mem(X3,ty_2Eoption_2Eoption(X0))
| mem(X4,ty_2Eoption_2Eoption(X1))
| ~ mem(sK5(X0,X1,X2,X3,X4),X1)
| ( c_2Eoption_2ENONE(X1) = X4 )
| mem(X2,arr(X0,arr(X1,bool))) ),
inference(consistent_polarity_flipping,[],[f162]) ).
tff(f281,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X4: $i] :
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),X3),X4))
| mem(X3,ty_2Eoption_2Eoption(X0))
| mem(X4,ty_2Eoption_2Eoption(X1))
| ( ap(c_2Eoption_2ESOME(X0),sK4(X0,X1,X2,X3,X4)) = X3 )
| ( c_2Eoption_2ENONE(X1) = X4 )
| mem(X2,arr(X0,arr(X1,bool))) ),
inference(consistent_polarity_flipping,[],[f161]) ).
tff(f284,plain,
~ mem(sK7,arr(sK6,arr(sK6,bool))),
inference(consistent_polarity_flipping,[],[f192]) ).
tff(f285,plain,
~ mem(sK8,sK6),
inference(consistent_polarity_flipping,[],[f191]) ).
tff(f286,plain,
~ mem(sK9,sK6),
inference(consistent_polarity_flipping,[],[f190]) ).
tff(f291,plain,
( p(ap(ap(sK7,sK8),sK9))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),ap(c_2Eoption_2ESOME(sK6),sK9)))
| sP10
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),c_2Eoption_2ENONE(sK6)),ap(c_2Eoption_2ESOME(sK6),sK9)))
| ~ sP11
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),c_2Eoption_2ENONE(sK6)))
| ~ sP12
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),c_2Eoption_2ENONE(sK6)),c_2Eoption_2ENONE(sK6))) ),
inference(consistent_polarity_flipping,[],[f185]) ).
tff(f299,plain,
( ~ p(ap(ap(sK7,sK8),sK9))
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),ap(c_2Eoption_2ESOME(sK6),sK9)))
| sP10
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),c_2Eoption_2ENONE(sK6)),ap(c_2Eoption_2ESOME(sK6),sK9)))
| ~ sP11
| p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),c_2Eoption_2ENONE(sK6)))
| ~ sP12
| ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),c_2Eoption_2ENONE(sK6)),c_2Eoption_2ENONE(sK6))) ),
inference(consistent_polarity_flipping,[],[f177]) ).
tff(f303,plain,
sP11,
inference(consistent_polarity_flipping,[],[f172]) ).
tff(f307,definition,
( spl13_1
<=> p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),c_2Eoption_2ENONE(sK6)),c_2Eoption_2ENONE(sK6))) ),
introduced(definition,[new_symbols(definition,[spl13_1])],[avatar_definition]) ).
tff(f308,plain,
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),c_2Eoption_2ENONE(sK6)),c_2Eoption_2ENONE(sK6)))
| spl13_1 ),
inference(avatar_component_clause,[],[f307]) ).
tff(f311,definition,
( spl13_2
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl13_2])],[avatar_definition]) ).
tff(f315,definition,
( spl13_3
<=> p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),c_2Eoption_2ENONE(sK6))) ),
introduced(definition,[new_symbols(definition,[spl13_3])],[avatar_definition]) ).
tff(f316,plain,
( p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),c_2Eoption_2ENONE(sK6)))
| ~ spl13_3 ),
inference(avatar_component_clause,[],[f315]) ).
tff(f319,definition,
( spl13_4
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl13_4])],[avatar_definition]) ).
tff(f323,definition,
( spl13_5
<=> p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),c_2Eoption_2ENONE(sK6)),ap(c_2Eoption_2ESOME(sK6),sK9))) ),
introduced(definition,[new_symbols(definition,[spl13_5])],[avatar_definition]) ).
tff(f325,plain,
( p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),c_2Eoption_2ENONE(sK6)),ap(c_2Eoption_2ESOME(sK6),sK9)))
| ~ spl13_5 ),
inference(avatar_component_clause,[],[f323]) ).
tff(f327,definition,
( spl13_6
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl13_6])],[avatar_definition]) ).
tff(f331,definition,
( spl13_7
<=> p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),ap(c_2Eoption_2ESOME(sK6),sK9))) ),
introduced(definition,[new_symbols(definition,[spl13_7])],[avatar_definition]) ).
tff(f332,plain,
( p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),ap(c_2Eoption_2ESOME(sK6),sK9)))
| ~ spl13_7 ),
inference(avatar_component_clause,[],[f331]) ).
tff(f333,plain,
( ~ p(ap(ap(ap(c_2Eoption_2EOPTREL(sK6,sK6),sK7),ap(c_2Eoption_2ESOME(sK6),sK8)),ap(c_2Eoption_2ESOME(sK6),sK9)))
| spl13_7 ),
inference(avatar_component_clause,[],[f331]) ).
tff(f335,definition,
( spl13_8
<=> p(ap(ap(sK7,sK8),sK9)) ),
introduced(definition,[new_symbols(definition,[spl13_8])],[avatar_definition]) ).
tff(f337,plain,
( ~ p(ap(ap(sK7,sK8),sK9))
| spl13_8 ),
inference(avatar_component_clause,[],[f335]) ).
tff(f341,plain,
( ~ spl13_1
| ~ spl13_2
| spl13_3
| ~ spl13_4
| spl13_5
| spl13_6
| ~ spl13_7
| ~ spl13_8 ),
inference(avatar_split_clause,[],[f299,f335,f331,f327,f323,f319,f315,f311,f307]) ).
tff(f349,plain,
( ~ spl13_1
| ~ spl13_2
| spl13_3
| ~ spl13_4
| spl13_5
| spl13_6
| spl13_7
| spl13_8 ),
inference(avatar_split_clause,[],[f291,f335,f331,f327,f323,f319,f315,f311,f307]) ).
tff(f354,plain,
spl13_2,
inference(avatar_split_clause,[],[f171,f311]) ).
tff(f355,plain,
~ spl13_6,
inference(avatar_split_clause,[],[f173,f327]) ).
tff(f356,plain,
spl13_4,
inference(avatar_split_clause,[],[f303,f319]) ).
tff(f620,definition,
( spl13_15
<=> ! [X1: tp__o] : ~ p(inj__o(X1)) ),
introduced(definition,[new_symbols(definition,[spl13_15])],[avatar_definition]) ).
tff(f621,plain,
( ! [X1: tp__o] : ~ p(inj__o(X1))
| ~ spl13_15 ),
inference(avatar_component_clause,[],[f620]) ).
tff(f631,definition,
( spl13_18
<=> ! [X1: del,X3: $i] : mem(X3,X1) ),
introduced(definition,[new_symbols(definition,[spl13_18])],[avatar_definition]) ).
tff(f632,plain,
( ! [X3: $i,X1: del] : mem(X3,X1)
| ~ spl13_18 ),
inference(avatar_component_clause,[],[f631]) ).
tff(f639,definition,
( spl13_20
<=> ! [X1: $i] : mem(X1,ty_2Eoption_2Eoption(sK6)) ),
introduced(definition,[new_symbols(definition,[spl13_20])],[avatar_definition]) ).
tff(f640,plain,
( ! [X1: $i] : mem(X1,ty_2Eoption_2Eoption(sK6))
| ~ spl13_20 ),
inference(avatar_component_clause,[],[f639]) ).
tff(f642,definition,
( spl13_21
<=> ! [X0: $i] : mem(X0,arr(sK6,bool)) ),
introduced(definition,[new_symbols(definition,[spl13_21])],[avatar_definition]) ).
tff(f643,plain,
( ! [X0: $i] : mem(X0,arr(sK6,bool))
| ~ spl13_21 ),
inference(avatar_component_clause,[],[f642]) ).
tff(f856,definition,
( spl13_39
<=> ! [X3: del,X4: $i,X0: del,X5: $i,X2: $i] :
( mem(X2,X3)
| ( ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X5)) = X5 )
| mem(X5,X0)
| mem(X4,arr(X0,X3)) ) ),
introduced(definition,[new_symbols(definition,[spl13_39])],[avatar_definition]) ).
tff(f857,plain,
( ! [X2: $i,X3: del,X0: del,X4: $i,X5: $i] :
( mem(X2,X3)
| mem(X5,X0)
| mem(X4,arr(X0,X3))
| ( ap(c_2Eoption_2ETHE(X0),ap(c_2Eoption_2ESOME(X0),X5)) = X5 ) )
| ~ spl13_39 ),
inference(avatar_component_clause,[],[f856]) ).
tff(f865,definition,
( spl13_41
<=> ! [X2: $i] :
( mem(X2,sK6)
| ( ap(c_2Eoption_2ETHE(sK6),ap(c_2Eoption_2ESOME(sK6),X2)) = X2 ) ) ),
introduced(definition,[new_symbols(definition,[spl13_41])],[avatar_definition]) ).
tff(f866,plain,
( ! [X2: $i] :
( mem(X2,sK6)
| ( ap(c_2Eoption_2ETHE(sK6),ap(c_2Eoption_2ESOME(sK6),X2)) = X2 ) )
| ~ spl13_41 ),
inference(avatar_component_clause,[],[f865]) ).
tff(f890,plain,
( ! [X0: tp__o] : ~ p(inj__o(X0))
| ~ spl13_20 ),
inference(resolution,[],[f640,f247]) ).
tff(f895,plain,
( spl13_15
| ~ spl13_20 ),
inference(avatar_split_clause,[],[f890,f639,f620]) ).
tff(f978,plain,
( ! [X2: $i,X0: $i,X1: del] :
( mem(X0,X1)
| mem(X2,arr(X1,arr(sK6,bool))) )
| ~ spl13_21 ),
inference(resolution,[],[f643,f201]) ).
tff(f1091,plain,
( ! [X0: $i] : mem(X0,sK6)
| ~ spl13_21 ),
inference(resolution,[],[f978,f240]) ).
tff(f1318,plain,
! [X2: $i,X0: del,X1: del] :
( mem(X2,arr(X0,arr(X1,bool)))
| mem(c_2Eoption_2ENONE(X1),ty_2Eoption_2Eoption(X1))
| p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X1))) ),
inference(forward_subsumption_resolution,[],[f272,f230]) ).
tff(f1319,plain,
! [X2: $i,X0: del,X1: del] :
( p(ap(ap(ap(c_2Eoption_2EOPTREL(X0,X1),X2),c_2Eoption_2ENONE(X0)),c_2Eoption_2ENONE(X1)))
| mem(X2,arr(X0,arr(X1,bool))) ),
inference(forward_subsumption_resolution,[],[f1318,f230]) ).
tff(f1320,plain,
( mem(sK7,arr(sK6,arr(sK6,bool)))
| spl13_1 ),
inference(resolution,[],[f1319,f308]) ).
tff(f1323,plain,
( $false
| spl13_1 ),
inference(forward_subsumption_resolution,[],[f1320,f284]) ).
tff(f1324,plain,
spl13_1,
inference(avatar_contradiction_clause,[],[f1323]) ).
tff(f1356,plain,
( $false
| ~ spl13_21 ),
inference(backward_subsumption_resolution,[],[f286,f1091]) ).
tff(f1362,plain,
~ spl13_21,
inference(avatar_contradiction_clause,[],[f1356]) ).
tff(f1713,plain,
! [X2: $i,X0: $i,X1: $i] :
( mem(X0,arr(sK6,bool))
| mem(X1,ty_2Eoption_2Eoption(sK6))
| mem(X2,sK6)
| ( ap(c_2Eoption_2ETHE(sK6),ap(c_2Eoption_2ESOME(sK6),X2)) = X2 ) ),
inference(resolution,[],[f284,f261]) ).
tff(f1723,plain,
( spl13_41
| spl13_20
| spl13_21 ),
inference(avatar_split_clause,[],[f1713,f642,f639,f865]) ).
tff(f1907,definition,
( spl13_146
<=> ( ap(c_2Eoption_2ESOME(sK6),sK9) = c_2Eoption_2ENONE(sK6) ) ),
introduced(definition,[new_symbols(definition,[spl13_146])],[avatar_definition]) ).
tff(f1908,plain,
( ( ap(c_2Eoption_2ESOME(sK6),sK9) != c_2Eoption_2ENONE(sK6) )
| spl13_146 ),
inference(avatar_component_clause,[],[f1907]) ).
tff(f1909,plain,
( ( ap(c_2Eoption_2ESOME(sK6),sK9) = c_2Eoption_2ENONE(sK6) )
| ~ spl13_146 ),
inference(avatar_component_clause,[],[f1907]) ).
tff(f1911,definition,
( spl13_147
<=> mem(sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6) ),
introduced(definition,[new_symbols(definition,[spl13_147])],[avatar_definition]) ).
tff(f1913,plain,
( ~ mem(sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| spl13_147 ),
inference(avatar_component_clause,[],[f1911]) ).
tff(f1915,definition,
( spl13_148
<=> mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6)) ),
introduced(definition,[new_symbols(definition,[spl13_148])],[avatar_definition]) ).
tff(f1916,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| spl13_148 ),
inference(avatar_component_clause,[],[f1915]) ).
tff(f1917,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ~ spl13_148 ),
inference(avatar_component_clause,[],[f1915]) ).
tff(f1919,definition,
( spl13_149
<=> mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6)) ),
introduced(definition,[new_symbols(definition,[spl13_149])],[avatar_definition]) ).
tff(f1920,plain,
( ~ mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| spl13_149 ),
inference(avatar_component_clause,[],[f1919]) ).
tff(f1921,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| ~ spl13_149 ),
inference(avatar_component_clause,[],[f1919]) ).
tff(f1930,definition,
( spl13_150
<=> ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) ) ),
introduced(definition,[new_symbols(definition,[spl13_150])],[avatar_definition]) ).
tff(f1931,plain,
( ( ap(c_2Eoption_2ESOME(sK6),sK8) != c_2Eoption_2ENONE(sK6) )
| spl13_150 ),
inference(avatar_component_clause,[],[f1930]) ).
tff(f1932,plain,
( ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| ~ spl13_150 ),
inference(avatar_component_clause,[],[f1930]) ).
tff(f1941,definition,
( spl13_151
<=> mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6) ),
introduced(definition,[new_symbols(definition,[spl13_151])],[avatar_definition]) ).
tff(f1943,plain,
( ~ mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| spl13_151 ),
inference(avatar_component_clause,[],[f1941]) ).
tff(f2153,definition,
( spl13_173
<=> ( ap(c_2Eoption_2ESOME(sK6),sK8) = ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) ) ),
introduced(definition,[new_symbols(definition,[spl13_173])],[avatar_definition]) ).
tff(f2155,plain,
( ( ap(c_2Eoption_2ESOME(sK6),sK8) = ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ~ spl13_173 ),
inference(avatar_component_clause,[],[f2153]) ).
tff(f2161,plain,
( mem(c_2Eoption_2ENONE(sK6),ty_2Eoption_2Eoption(sK6))
| mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ~ mem(sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK9) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_5 ),
inference(resolution,[],[f325,f273]) ).
tff(f2172,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ~ mem(sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK9) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_5 ),
inference(forward_subsumption_resolution,[],[f2161,f230]) ).
tff(f2174,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ~ mem(sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK9) = c_2Eoption_2ENONE(sK6) )
| ~ spl13_5 ),
inference(forward_subsumption_resolution,[],[f2172,f284]) ).
tff(f2177,definition,
( spl13_176
<=> mem(sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6) ),
introduced(definition,[new_symbols(definition,[spl13_176])],[avatar_definition]) ).
tff(f2179,plain,
( ~ mem(sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| spl13_176 ),
inference(avatar_component_clause,[],[f2177]) ).
tff(f2206,plain,
( ( sK8 = ap(c_2Eoption_2ETHE(sK6),ap(c_2Eoption_2ESOME(sK6),sK8)) )
| ~ spl13_41 ),
inference(resolution,[],[f866,f285]) ).
tff(f2207,plain,
( ( sK9 = ap(c_2Eoption_2ETHE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9)) )
| ~ spl13_41 ),
inference(resolution,[],[f866,f286]) ).
tff(f2244,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ~ p(ap(ap(sK7,sK8),sK9))
| mem(sK9,sK6)
| mem(sK8,sK6)
| mem(sK7,arr(sK6,arr(sK6,bool)))
| spl13_7 ),
inference(resolution,[],[f275,f333]) ).
tff(f2272,plain,
( ! [X0: del] :
( mem(c_2Eoption_2ESOME(sK6),arr(X0,ty_2Eoption_2Eoption(sK6)))
| mem(sK9,X0) )
| ~ spl13_148 ),
inference(resolution,[],[f1917,f201]) ).
tff(f2284,definition,
( spl13_178
<=> ! [X2: del,X1: $i,X4: $i] :
( mem(X1,arr(sK6,X2))
| mem(X4,X2) ) ),
introduced(definition,[new_symbols(definition,[spl13_178])],[avatar_definition]) ).
tff(f2285,plain,
( ! [X2: del,X1: $i,X4: $i] :
( mem(X1,arr(sK6,X2))
| mem(X4,X2) )
| ~ spl13_178 ),
inference(avatar_component_clause,[],[f2284]) ).
tff(f2304,plain,
( ! [X2: $i,X0: del,X1: tp__o] :
( mem(X2,X0)
| ~ p(inj__o(X1)) )
| ~ spl13_178 ),
inference(resolution,[],[f2285,f247]) ).
tff(f2332,plain,
( spl13_15
| spl13_18
| ~ spl13_178 ),
inference(avatar_split_clause,[],[f2304,f2284,f631,f620]) ).
tff(f2468,plain,
( mem(sK9,sK6)
| ~ spl13_148 ),
inference(resolution,[],[f2272,f225]) ).
tff(f2469,plain,
( $false
| ~ spl13_148 ),
inference(forward_subsumption_resolution,[],[f2468,f286]) ).
tff(f2470,plain,
~ spl13_148,
inference(avatar_contradiction_clause,[],[f2469]) ).
tff(f2556,plain,
( ! [X0: del] :
( mem(c_2Eoption_2ESOME(sK6),arr(X0,ty_2Eoption_2Eoption(sK6)))
| mem(sK8,X0) )
| ~ spl13_149 ),
inference(resolution,[],[f1921,f201]) ).
tff(f2557,plain,
( mem(sK8,sK6)
| ~ spl13_149 ),
inference(resolution,[],[f2556,f225]) ).
tff(f2558,plain,
( $false
| ~ spl13_149 ),
inference(forward_subsumption_resolution,[],[f2557,f285]) ).
tff(f2559,plain,
~ spl13_149,
inference(avatar_contradiction_clause,[],[f2558]) ).
tff(f2561,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| ~ p(ap(ap(sK7,sK8),sK9))
| mem(sK9,sK6)
| mem(sK8,sK6)
| mem(sK7,arr(sK6,arr(sK6,bool)))
| spl13_7
| spl13_148 ),
inference(forward_subsumption_resolution,[],[f2244,f1916]) ).
tff(f2562,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| ~ p(ap(ap(sK7,sK8),sK9))
| mem(sK8,sK6)
| mem(sK7,arr(sK6,arr(sK6,bool)))
| spl13_7
| spl13_148 ),
inference(forward_subsumption_resolution,[],[f2561,f286]) ).
tff(f2563,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| ~ p(ap(ap(sK7,sK8),sK9))
| mem(sK7,arr(sK6,arr(sK6,bool)))
| spl13_7
| spl13_148 ),
inference(forward_subsumption_resolution,[],[f2562,f285]) ).
tff(f2564,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| ~ p(ap(ap(sK7,sK8),sK9))
| spl13_7
| spl13_148 ),
inference(forward_subsumption_resolution,[],[f2563,f284]) ).
tff(f2565,plain,
( ~ spl13_8
| spl13_149
| spl13_7
| spl13_148 ),
inference(avatar_split_clause,[],[f2564,f1915,f331,f1919,f335]) ).
tff(f2568,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| mem(c_2Eoption_2ENONE(sK6),ty_2Eoption_2Eoption(sK6))
| ~ mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),c_2Eoption_2ENONE(sK6)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_3 ),
inference(resolution,[],[f316,f276]) ).
tff(f2570,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| mem(c_2Eoption_2ENONE(sK6),ty_2Eoption_2Eoption(sK6))
| ( c_2Eoption_2ENONE(sK6) = ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),c_2Eoption_2ENONE(sK6))) )
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_3 ),
inference(resolution,[],[f316,f278]) ).
tff(f2580,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| ( c_2Eoption_2ENONE(sK6) = ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),c_2Eoption_2ENONE(sK6))) )
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_3 ),
inference(forward_subsumption_resolution,[],[f2570,f230]) ).
tff(f2582,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| ~ mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),c_2Eoption_2ENONE(sK6)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_3 ),
inference(forward_subsumption_resolution,[],[f2568,f230]) ).
tff(f2585,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| ( c_2Eoption_2ENONE(sK6) = ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),c_2Eoption_2ENONE(sK6))) )
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| ~ spl13_3 ),
inference(forward_subsumption_resolution,[],[f2580,f284]) ).
tff(f2587,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| ~ mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),c_2Eoption_2ENONE(sK6)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| ~ spl13_3 ),
inference(forward_subsumption_resolution,[],[f2582,f284]) ).
tff(f2595,definition,
( spl13_205
<=> ( c_2Eoption_2ENONE(sK6) = ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),c_2Eoption_2ENONE(sK6))) ) ),
introduced(definition,[new_symbols(definition,[spl13_205])],[avatar_definition]) ).
tff(f2597,plain,
( ( c_2Eoption_2ENONE(sK6) = ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),c_2Eoption_2ENONE(sK6))) )
| ~ spl13_205 ),
inference(avatar_component_clause,[],[f2595]) ).
tff(f2598,plain,
( spl13_150
| spl13_205
| spl13_149
| ~ spl13_3 ),
inference(avatar_split_clause,[],[f2585,f315,f1919,f2595,f1930]) ).
tff(f2605,definition,
( spl13_207
<=> mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),c_2Eoption_2ENONE(sK6)),sK6) ),
introduced(definition,[new_symbols(definition,[spl13_207])],[avatar_definition]) ).
tff(f2607,plain,
( ~ mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),c_2Eoption_2ENONE(sK6)),sK6)
| spl13_207 ),
inference(avatar_component_clause,[],[f2605]) ).
tff(f2608,plain,
( spl13_150
| ~ spl13_207
| spl13_149
| ~ spl13_3 ),
inference(avatar_split_clause,[],[f2587,f315,f1919,f2605,f1930]) ).
tff(f2787,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: del] :
( p(ap(c_2Eoption_2EIS__SOME(sK6),c_2Eoption_2ENONE(sK6)))
| mem(X0,X1)
| mem(X2,arr(sK6,X1))
| mem(X3,ty_2Eoption_2Eoption(sK6))
| mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),c_2Eoption_2ENONE(sK6)),sK6) )
| ~ spl13_205 ),
inference(superposition,[],[f268,f2597]) ).
tff(f2793,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: del] :
( mem(X0,X1)
| mem(X2,arr(sK6,X1))
| mem(X3,ty_2Eoption_2Eoption(sK6))
| mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),c_2Eoption_2ENONE(sK6)),sK6) )
| ~ spl13_205 ),
inference(forward_subsumption_resolution,[],[f2787,f258]) ).
tff(f2797,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: del] :
( mem(X0,X1)
| mem(X2,arr(sK6,X1))
| mem(X3,ty_2Eoption_2Eoption(sK6)) )
| ~ spl13_205
| spl13_207 ),
inference(forward_subsumption_resolution,[],[f2793,f2607]) ).
tff(f2800,plain,
( spl13_20
| spl13_178
| ~ spl13_205
| spl13_207 ),
inference(avatar_split_clause,[],[f2797,f2605,f2595,f2284,f639]) ).
tff(f2814,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: del] :
( p(ap(c_2Eoption_2EIS__SOME(sK6),c_2Eoption_2ENONE(sK6)))
| mem(X0,X1)
| mem(X2,arr(sK6,X1))
| mem(X3,ty_2Eoption_2Eoption(sK6))
| mem(sK8,sK6) )
| ~ spl13_150 ),
inference(superposition,[],[f268,f1932]) ).
tff(f2820,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: del] :
( mem(X0,X1)
| mem(X2,arr(sK6,X1))
| mem(X3,ty_2Eoption_2Eoption(sK6))
| mem(sK8,sK6) )
| ~ spl13_150 ),
inference(forward_subsumption_resolution,[],[f2814,f258]) ).
tff(f2826,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: del] :
( mem(X0,X1)
| mem(X2,arr(sK6,X1))
| mem(X3,ty_2Eoption_2Eoption(sK6)) )
| ~ spl13_150 ),
inference(forward_subsumption_resolution,[],[f2820,f285]) ).
tff(f2829,plain,
( spl13_20
| spl13_178
| ~ spl13_150 ),
inference(avatar_split_clause,[],[f2826,f1930,f2284,f639]) ).
tff(f2838,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7 ),
inference(resolution,[],[f332,f277]) ).
tff(f2839,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ( ap(c_2Eoption_2ESOME(sK6),sK9) = ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7 ),
inference(resolution,[],[f332,f278]) ).
tff(f2840,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| p(ap(ap(sK7,sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))))
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7 ),
inference(resolution,[],[f332,f279]) ).
tff(f2851,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| p(ap(ap(sK7,sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))))
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_149 ),
inference(forward_subsumption_resolution,[],[f2840,f1920]) ).
tff(f2852,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ( ap(c_2Eoption_2ESOME(sK6),sK9) = ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_149 ),
inference(forward_subsumption_resolution,[],[f2839,f1920]) ).
tff(f2853,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_149 ),
inference(forward_subsumption_resolution,[],[f2838,f1920]) ).
tff(f2857,plain,
( p(ap(ap(sK7,sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))))
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_148
| spl13_149 ),
inference(forward_subsumption_resolution,[],[f2851,f1916]) ).
tff(f2858,plain,
( ( ap(c_2Eoption_2ESOME(sK6),sK9) = ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_148
| spl13_149 ),
inference(forward_subsumption_resolution,[],[f2852,f1916]) ).
tff(f2859,plain,
( ( ap(c_2Eoption_2ESOME(sK6),sK8) = ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_148
| spl13_149 ),
inference(forward_subsumption_resolution,[],[f2853,f1916]) ).
tff(f2863,plain,
( p(ap(ap(sK7,sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))))
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_148
| spl13_149
| spl13_150 ),
inference(forward_subsumption_resolution,[],[f2857,f1931]) ).
tff(f2864,plain,
( ( ap(c_2Eoption_2ESOME(sK6),sK9) = ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_148
| spl13_149
| spl13_150 ),
inference(forward_subsumption_resolution,[],[f2858,f1931]) ).
tff(f2865,plain,
( ( ap(c_2Eoption_2ESOME(sK6),sK8) = ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_148
| spl13_149
| spl13_150 ),
inference(forward_subsumption_resolution,[],[f2859,f1931]) ).
tff(f2867,definition,
( spl13_229
<=> p(ap(ap(sK7,sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)))) ),
introduced(definition,[new_symbols(definition,[spl13_229])],[avatar_definition]) ).
tff(f2869,plain,
( p(ap(ap(sK7,sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))))
| ~ spl13_229 ),
inference(avatar_component_clause,[],[f2867]) ).
tff(f2872,definition,
( spl13_230
<=> ( ap(c_2Eoption_2ESOME(sK6),sK9) = ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) ) ),
introduced(definition,[new_symbols(definition,[spl13_230])],[avatar_definition]) ).
tff(f2874,plain,
( ( ap(c_2Eoption_2ESOME(sK6),sK9) = ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ~ spl13_230 ),
inference(avatar_component_clause,[],[f2872]) ).
tff(f2877,plain,
( p(ap(ap(sK7,sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))))
| ~ spl13_7
| spl13_148
| spl13_149
| spl13_150 ),
inference(forward_subsumption_resolution,[],[f2863,f284]) ).
tff(f2878,plain,
( ( ap(c_2Eoption_2ESOME(sK6),sK9) = ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ~ spl13_7
| spl13_148
| spl13_149
| spl13_150 ),
inference(forward_subsumption_resolution,[],[f2864,f284]) ).
tff(f2879,plain,
( ( ap(c_2Eoption_2ESOME(sK6),sK8) = ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ~ spl13_7
| spl13_148
| spl13_149
| spl13_150 ),
inference(forward_subsumption_resolution,[],[f2865,f284]) ).
tff(f2880,plain,
( spl13_229
| ~ spl13_7
| spl13_148
| spl13_149
| spl13_150 ),
inference(avatar_split_clause,[],[f2877,f1930,f1919,f1915,f331,f2867]) ).
tff(f2881,plain,
( spl13_230
| ~ spl13_7
| spl13_148
| spl13_149
| spl13_150 ),
inference(avatar_split_clause,[],[f2878,f1930,f1919,f1915,f331,f2872]) ).
tff(f2882,plain,
( spl13_173
| ~ spl13_7
| spl13_148
| spl13_149
| spl13_150 ),
inference(avatar_split_clause,[],[f2879,f1930,f1919,f1915,f331,f2153]) ).
tff(f3120,plain,
( ~ p(c_2Ebool_2ET)
| ~ spl13_15 ),
inference(superposition,[],[f621,f102]) ).
tff(f3122,plain,
( $false
| ~ spl13_15 ),
inference(forward_subsumption_resolution,[],[f3120,f103]) ).
tff(f3123,plain,
~ spl13_15,
inference(avatar_contradiction_clause,[],[f3122]) ).
tff(f3164,plain,
( $false
| ~ spl13_18 ),
inference(backward_subsumption_resolution,[],[f286,f632]) ).
tff(f3193,plain,
~ spl13_18,
inference(avatar_contradiction_clause,[],[f3164]) ).
tff(f3905,plain,
! [X2: $i,X3: del,X0: tp__o,X1: del,X4: $i,X5: $i] :
( ~ p(inj__o(X0))
| mem(X2,X3)
| mem(X4,arr(X1,X3))
| mem(X5,X1)
| ( ap(c_2Eoption_2ETHE(X1),ap(c_2Eoption_2ESOME(X1),X5)) = X5 ) ),
inference(resolution,[],[f247,f261]) ).
tff(f3924,plain,
( spl13_39
| spl13_15 ),
inference(avatar_split_clause,[],[f3905,f620,f856]) ).
tff(f4417,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ~ mem(sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7 ),
inference(resolution,[],[f274,f332]) ).
tff(f4423,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ~ mem(sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_149 ),
inference(forward_subsumption_resolution,[],[f4417,f1920]) ).
tff(f4424,plain,
( ~ mem(sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK8) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_148
| spl13_149 ),
inference(forward_subsumption_resolution,[],[f4423,f1916]) ).
tff(f4425,plain,
( ~ mem(sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_148
| spl13_149
| spl13_150 ),
inference(forward_subsumption_resolution,[],[f4424,f1931]) ).
tff(f4426,plain,
( ~ mem(sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ~ spl13_7
| spl13_148
| spl13_149
| spl13_150 ),
inference(forward_subsumption_resolution,[],[f4425,f284]) ).
tff(f4427,plain,
( ~ spl13_147
| ~ spl13_7
| spl13_148
| spl13_149
| spl13_150 ),
inference(avatar_split_clause,[],[f4426,f1930,f1919,f1915,f331,f1911]) ).
tff(f4441,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK8),ty_2Eoption_2Eoption(sK6))
| mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ~ mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK9) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7 ),
inference(resolution,[],[f280,f332]) ).
tff(f4447,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ~ mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK9) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_149 ),
inference(forward_subsumption_resolution,[],[f4441,f1920]) ).
tff(f4448,plain,
( ~ mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK9) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_148
| spl13_149 ),
inference(forward_subsumption_resolution,[],[f4447,f1916]) ).
tff(f4449,plain,
( ~ mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_7
| spl13_146
| spl13_148
| spl13_149 ),
inference(forward_subsumption_resolution,[],[f4448,f1908]) ).
tff(f4450,plain,
( ~ mem(sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ~ spl13_7
| spl13_146
| spl13_148
| spl13_149 ),
inference(forward_subsumption_resolution,[],[f4449,f284]) ).
tff(f4451,plain,
( ~ spl13_151
| ~ spl13_7
| spl13_146
| spl13_148
| spl13_149 ),
inference(avatar_split_clause,[],[f4450,f1919,f1915,f1907,f331,f1941]) ).
tff(f4493,definition,
( spl13_261
<=> ( sK8 = sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)) ) ),
introduced(definition,[new_symbols(definition,[spl13_261])],[avatar_definition]) ).
tff(f4495,plain,
( ( sK8 = sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)) )
| ~ spl13_261 ),
inference(avatar_component_clause,[],[f4493]) ).
tff(f4539,definition,
( spl13_264
<=> ( sK9 = sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)) ) ),
introduced(definition,[new_symbols(definition,[spl13_264])],[avatar_definition]) ).
tff(f4541,plain,
( ( sK9 = sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)) )
| ~ spl13_264 ),
inference(avatar_component_clause,[],[f4539]) ).
tff(f7593,plain,
( ! [X2: $i,X0: $i,X1: del] :
( mem(X0,X1)
| mem(X2,arr(sK6,X1))
| ( sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)) = ap(c_2Eoption_2ETHE(sK6),ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)))) ) )
| ~ spl13_39
| spl13_147 ),
inference(resolution,[],[f857,f1913]) ).
tff(f7595,plain,
( ! [X2: $i,X0: $i,X1: del] :
( mem(X0,X1)
| mem(X2,arr(sK6,X1))
| ( sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)) = ap(c_2Eoption_2ETHE(sK6),ap(c_2Eoption_2ESOME(sK6),sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)))) ) )
| ~ spl13_39
| spl13_151 ),
inference(resolution,[],[f857,f1943]) ).
tff(f7632,plain,
( ! [X2: $i,X0: $i,X1: del] :
( ( sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)) = ap(c_2Eoption_2ETHE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9)) )
| mem(X0,X1)
| mem(X2,arr(sK6,X1)) )
| ~ spl13_39
| spl13_151
| ~ spl13_230 ),
inference(forward_demodulation,[],[f7595,f2874]) ).
tff(f7634,plain,
( ! [X2: $i,X0: $i,X1: del] :
( ( sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)) = ap(c_2Eoption_2ETHE(sK6),ap(c_2Eoption_2ESOME(sK6),sK8)) )
| mem(X0,X1)
| mem(X2,arr(sK6,X1)) )
| ~ spl13_39
| spl13_147
| ~ spl13_173 ),
inference(forward_demodulation,[],[f7593,f2155]) ).
tff(f7642,plain,
( ! [X2: $i,X0: $i,X1: del] :
( ( sK9 = sK5(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)) )
| mem(X0,X1)
| mem(X2,arr(sK6,X1)) )
| ~ spl13_39
| ~ spl13_41
| spl13_151
| ~ spl13_230 ),
inference(forward_demodulation,[],[f7632,f2207]) ).
tff(f7643,plain,
( ! [X2: $i,X0: $i,X1: del] :
( ( sK8 = sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9)) )
| mem(X0,X1)
| mem(X2,arr(sK6,X1)) )
| ~ spl13_39
| ~ spl13_41
| spl13_147
| ~ spl13_173 ),
inference(forward_demodulation,[],[f7634,f2206]) ).
tff(f7645,plain,
( spl13_178
| spl13_264
| ~ spl13_39
| ~ spl13_41
| spl13_151
| ~ spl13_230 ),
inference(avatar_split_clause,[],[f7642,f2872,f1941,f865,f856,f4539,f2284]) ).
tff(f7646,plain,
( spl13_178
| spl13_261
| ~ spl13_39
| ~ spl13_41
| spl13_147
| ~ spl13_173 ),
inference(avatar_split_clause,[],[f7643,f2153,f1911,f865,f856,f4493,f2284]) ).
tff(f46344,plain,
( p(ap(ap(sK7,sK4(sK6,sK6,sK7,ap(c_2Eoption_2ESOME(sK6),sK8),ap(c_2Eoption_2ESOME(sK6),sK9))),sK9))
| ~ spl13_229
| ~ spl13_264 ),
inference(superposition,[],[f2869,f4541]) ).
tff(f46347,plain,
( p(ap(ap(sK7,sK8),sK9))
| ~ spl13_229
| ~ spl13_261
| ~ spl13_264 ),
inference(forward_demodulation,[],[f46344,f4495]) ).
tff(f46348,plain,
( $false
| spl13_8
| ~ spl13_229
| ~ spl13_261
| ~ spl13_264 ),
inference(forward_subsumption_resolution,[],[f46347,f337]) ).
tff(f46349,plain,
( spl13_8
| ~ spl13_229
| ~ spl13_261
| ~ spl13_264 ),
inference(avatar_contradiction_clause,[],[f46348]) ).
tff(f46350,plain,
( ~ mem(sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ( ap(c_2Eoption_2ESOME(sK6),sK9) = c_2Eoption_2ENONE(sK6) )
| ~ spl13_5
| spl13_148 ),
inference(forward_subsumption_resolution,[],[f2174,f1916]) ).
tff(f46354,plain,
( ~ mem(sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6)
| ~ spl13_5
| spl13_146
| spl13_148 ),
inference(forward_subsumption_resolution,[],[f46350,f1908]) ).
tff(f46357,plain,
( ~ spl13_176
| ~ spl13_5
| spl13_146
| spl13_148 ),
inference(avatar_split_clause,[],[f46354,f1915,f1907,f323,f2177]) ).
tff(f46375,plain,
( mem(c_2Eoption_2ENONE(sK6),ty_2Eoption_2Eoption(sK6))
| mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ( c_2Eoption_2ENONE(sK6) = ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ( ap(c_2Eoption_2ESOME(sK6),sK9) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_5 ),
inference(resolution,[],[f325,f281]) ).
tff(f46463,plain,
( mem(ap(c_2Eoption_2ESOME(sK6),sK9),ty_2Eoption_2Eoption(sK6))
| ( c_2Eoption_2ENONE(sK6) = ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ( ap(c_2Eoption_2ESOME(sK6),sK9) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_5 ),
inference(forward_subsumption_resolution,[],[f46375,f230]) ).
tff(f46468,plain,
( ( c_2Eoption_2ENONE(sK6) = ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ( ap(c_2Eoption_2ESOME(sK6),sK9) = c_2Eoption_2ENONE(sK6) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_5
| spl13_148 ),
inference(forward_subsumption_resolution,[],[f46463,f1916]) ).
tff(f46473,plain,
( ( c_2Eoption_2ENONE(sK6) = ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| mem(sK7,arr(sK6,arr(sK6,bool)))
| ~ spl13_5
| spl13_146
| spl13_148 ),
inference(forward_subsumption_resolution,[],[f46468,f1908]) ).
tff(f46478,plain,
( ( c_2Eoption_2ENONE(sK6) = ap(c_2Eoption_2ESOME(sK6),sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9))) )
| ~ spl13_5
| spl13_146
| spl13_148 ),
inference(forward_subsumption_resolution,[],[f46473,f284]) ).
tff(f47458,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: del] :
( p(ap(c_2Eoption_2EIS__SOME(sK6),c_2Eoption_2ENONE(sK6)))
| mem(X0,X1)
| mem(X2,arr(sK6,X1))
| mem(X3,ty_2Eoption_2Eoption(sK6))
| mem(sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6) )
| ~ spl13_5
| spl13_146
| spl13_148 ),
inference(superposition,[],[f268,f46478]) ).
tff(f47495,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: del] :
( mem(X0,X1)
| mem(X2,arr(sK6,X1))
| mem(X3,ty_2Eoption_2Eoption(sK6))
| mem(sK4(sK6,sK6,sK7,c_2Eoption_2ENONE(sK6),ap(c_2Eoption_2ESOME(sK6),sK9)),sK6) )
| ~ spl13_5
| spl13_146
| spl13_148 ),
inference(forward_subsumption_resolution,[],[f47458,f258]) ).
tff(f47518,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: del] :
( mem(X0,X1)
| mem(X2,arr(sK6,X1))
| mem(X3,ty_2Eoption_2Eoption(sK6)) )
| ~ spl13_5
| spl13_146
| spl13_148
| spl13_176 ),
inference(forward_subsumption_resolution,[],[f47495,f2179]) ).
tff(f47533,plain,
( spl13_20
| spl13_178
| ~ spl13_5
| spl13_146
| spl13_148
| spl13_176 ),
inference(avatar_split_clause,[],[f47518,f2177,f1915,f1907,f323,f2284,f639]) ).
tff(f48193,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: del] :
( p(ap(c_2Eoption_2EIS__SOME(sK6),c_2Eoption_2ENONE(sK6)))
| mem(X0,X1)
| mem(X2,arr(sK6,X1))
| mem(X3,ty_2Eoption_2Eoption(sK6))
| mem(sK9,sK6) )
| ~ spl13_146 ),
inference(superposition,[],[f268,f1909]) ).
tff(f48226,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: del] :
( mem(X0,X1)
| mem(X2,arr(sK6,X1))
| mem(X3,ty_2Eoption_2Eoption(sK6))
| mem(sK9,sK6) )
| ~ spl13_146 ),
inference(forward_subsumption_resolution,[],[f48193,f258]) ).
tff(f48241,plain,
( ! [X2: $i,X3: $i,X0: $i,X1: del] :
( mem(X0,X1)
| mem(X2,arr(sK6,X1))
| mem(X3,ty_2Eoption_2Eoption(sK6)) )
| ~ spl13_146 ),
inference(forward_subsumption_resolution,[],[f48226,f286]) ).
tff(f48246,plain,
( spl13_20
| spl13_178
| ~ spl13_146 ),
inference(avatar_split_clause,[],[f48241,f1907,f2284,f639]) ).
cnf(s4,plain,
( ~ spl13_1
| ~ spl13_2
| spl13_3
| ~ spl13_4
| spl13_5
| spl13_6
| ~ spl13_7
| ~ spl13_8 ),
inference(sat_conversion,[],[f341]) ).
cnf(s12,plain,
( ~ spl13_1
| ~ spl13_2
| spl13_3
| ~ spl13_4
| spl13_5
| spl13_6
| spl13_7
| spl13_8 ),
inference(sat_conversion,[],[f349]) ).
cnf(s17,plain,
spl13_2,
inference(sat_conversion,[],[f354]) ).
cnf(s18,plain,
~ spl13_6,
inference(sat_conversion,[],[f355]) ).
cnf(s19,plain,
spl13_4,
inference(sat_conversion,[],[f356]) ).
cnf(s61,plain,
( spl13_15
| ~ spl13_20 ),
inference(sat_conversion,[],[f895]) ).
cnf(s122,plain,
spl13_1,
inference(sat_conversion,[],[f1324]) ).
cnf(s127,plain,
~ spl13_21,
inference(sat_conversion,[],[f1362]) ).
cnf(s183,plain,
( spl13_20
| spl13_21
| spl13_41 ),
inference(sat_conversion,[],[f1723]) ).
cnf(s257,plain,
( spl13_15
| spl13_18
| ~ spl13_178 ),
inference(sat_conversion,[],[f2332]) ).
cnf(s283,plain,
~ spl13_148,
inference(sat_conversion,[],[f2470]) ).
cnf(s297,plain,
~ spl13_149,
inference(sat_conversion,[],[f2559]) ).
cnf(s299,plain,
( spl13_7
| ~ spl13_8
| spl13_148
| spl13_149 ),
inference(sat_conversion,[],[f2565]) ).
cnf(s302,plain,
( ~ spl13_3
| spl13_149
| spl13_150
| spl13_205 ),
inference(sat_conversion,[],[f2598]) ).
cnf(s304,plain,
( ~ spl13_3
| spl13_149
| spl13_150
| ~ spl13_207 ),
inference(sat_conversion,[],[f2608]) ).
cnf(s331,plain,
( spl13_20
| spl13_178
| ~ spl13_205
| spl13_207 ),
inference(sat_conversion,[],[f2800]) ).
cnf(s335,plain,
( spl13_20
| ~ spl13_150
| spl13_178 ),
inference(sat_conversion,[],[f2829]) ).
cnf(s343,plain,
( ~ spl13_7
| spl13_148
| spl13_149
| spl13_150
| spl13_229 ),
inference(sat_conversion,[],[f2880]) ).
cnf(s344,plain,
( ~ spl13_7
| spl13_148
| spl13_149
| spl13_150
| spl13_230 ),
inference(sat_conversion,[],[f2881]) ).
cnf(s345,plain,
( ~ spl13_7
| spl13_148
| spl13_149
| spl13_150
| spl13_173 ),
inference(sat_conversion,[],[f2882]) ).
cnf(s370,plain,
~ spl13_15,
inference(sat_conversion,[],[f3123]) ).
cnf(s399,plain,
~ spl13_18,
inference(sat_conversion,[],[f3193]) ).
cnf(s564,plain,
( spl13_15
| spl13_39 ),
inference(sat_conversion,[],[f3924]) ).
cnf(s607,plain,
( ~ spl13_7
| ~ spl13_147
| spl13_148
| spl13_149
| spl13_150 ),
inference(sat_conversion,[],[f4427]) ).
cnf(s609,plain,
( ~ spl13_7
| spl13_146
| spl13_148
| spl13_149
| ~ spl13_151 ),
inference(sat_conversion,[],[f4451]) ).
cnf(s824,plain,
( ~ spl13_39
| ~ spl13_41
| spl13_151
| spl13_178
| ~ spl13_230
| spl13_264 ),
inference(sat_conversion,[],[f7645]) ).
cnf(s825,plain,
( ~ spl13_39
| ~ spl13_41
| spl13_147
| ~ spl13_173
| spl13_178
| spl13_261 ),
inference(sat_conversion,[],[f7646]) ).
cnf(s3784,plain,
( spl13_8
| ~ spl13_229
| ~ spl13_261
| ~ spl13_264 ),
inference(sat_conversion,[],[f46349]) ).
cnf(s3786,plain,
( ~ spl13_5
| spl13_146
| spl13_148
| ~ spl13_176 ),
inference(sat_conversion,[],[f46357]) ).
cnf(s3972,plain,
( ~ spl13_5
| spl13_20
| spl13_146
| spl13_148
| spl13_176
| spl13_178 ),
inference(sat_conversion,[],[f47533]) ).
cnf(s4167,plain,
( spl13_20
| ~ spl13_146
| spl13_178 ),
inference(sat_conversion,[],[f48246]) ).
cnf(s5018,plain,
spl13_39,
inference(rat,[],[s564,s370]) ).
cnf(s5118,plain,
~ spl13_178,
inference(rat,[],[s257,s399,s370]) ).
cnf(s5181,plain,
~ spl13_20,
inference(rat,[],[s61,s370]) ).
cnf(s5182,plain,
~ spl13_146,
inference(rat,[],[s4167,s5118,s5181]) ).
cnf(s5255,plain,
~ spl13_150,
inference(rat,[],[s335,s5118,s5181]) ).
cnf(s5261,plain,
spl13_41,
inference(rat,[],[s183,s127,s5181]) ).
cnf(s5310,plain,
( spl13_3
| spl13_5
| spl13_7
| spl13_8 ),
inference(rat,[],[s12,s18,s19,s17,s122]) ).
cnf(s5311,plain,
( spl13_3
| spl13_5
| ~ spl13_7
| ~ spl13_8 ),
inference(rat,[],[s4,s18,s19,s17,s122]) ).
cnf(s5312,plain,
( spl13_7
| spl13_5
| spl13_3 ),
inference(rat,[],[s5310,s299,s283,s297]) ).
cnf(s5313,plain,
( spl13_5
| spl13_3 ),
inference(rat,[],[s3784,s824,s825,s5311,s343,s344,s345,s607,s609,s5312,s5182,s5255,s283,s297,s5261,s5118,s5018]) ).
cnf(s5314,plain,
~ spl13_5,
inference(rat,[],[s3786,s3972,s283,s5182,s5181,s5118]) ).
cnf(s5315,plain,
spl13_3,
inference(rat,[],[s5313,s5314]) ).
cnf(s5317,plain,
~ spl13_207,
inference(rat,[],[s304,s5255,s297,s5315]) ).
cnf(s5319,plain,
spl13_205,
inference(rat,[],[s302,s5255,s297,s5315]) ).
cnf(s5395,plain,
$false,
inference(rat,[],[s331,s5181,s5118,s5317,s5319]) ).
tff(f48247,plain,
$false,
inference(avatar_sat_refutation,[],[s5395]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP011_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 11:57:31 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.53/2.64 % (677424)Will run a generic schedule for satisfiability detection.
% 15.53/2.64 % (677429)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3618020149_2999 on theBenchmark for (2999ds/0Mi)
% 15.53/2.64 % (677431)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2553072101:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.53/2.64 % (677432)dis+10_1_sil=32000:sp=arity:random_seed=2891996853:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.53/2.64 % (677433)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=915954858:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.53/2.64 % (677434)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=351520100:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.53/2.64 % (677435)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3496724746:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.53/2.64 % (677430)% WARNING: option uhcvi not known.
% 15.53/2.64 % TRYING [1,1,1]
% 15.53/2.64 % TRYING [1,2,1]
% 15.53/2.64 % (677430)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=398299986:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.53/2.64 % TRYING [1,3,1]
% 15.53/2.64 % TRYING [1,2,2]
% 15.53/2.64 % TRYING [2,2,2]
% 15.53/2.64 % TRYING [1,3,2]
% 15.53/2.64 % TRYING [2,3,2]
% 15.53/2.64 % TRYING [1,4,1]
% 15.53/2.64 % TRYING [1,4,2]
% 15.53/2.64 % (677432)Instruction limit reached!
% 15.53/2.64 % (677432)------------------------------
% 15.53/2.64 % (677432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677432)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677432)Termination reason: Instruction limit
% 15.53/2.64 % (677432)Termination phase: Saturation
% 15.53/2.64 % (677432)Time elapsed: 0.063 s
% 15.53/2.64 % (677432)Peak memory usage: 13 MB
% 15.53/2.64 % (677432)Instructions burned: 103 (million)
% 15.53/2.64 % (677433)Instruction limit reached!
% 15.53/2.64 % (677433)------------------------------
% 15.53/2.64 % (677433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677433)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677433)Termination reason: Instruction limit
% 15.53/2.64 % (677433)Termination phase: Saturation
% 15.53/2.64 % (677433)Time elapsed: 0.068 s
% 15.53/2.64 % (677433)Peak memory usage: 13 MB
% 15.53/2.64 % (677433)Instructions burned: 118 (million)
% 15.53/2.64 % TRYING [3,3,2]
% 15.53/2.64 % (677434)Instruction limit reached!
% 15.53/2.64 % (677434)------------------------------
% 15.53/2.64 % (677434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677434)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677434)Termination reason: Instruction limit
% 15.53/2.64 % (677434)Termination phase: Saturation
% 15.53/2.64 % (677434)Time elapsed: 0.080 s
% 15.53/2.64 % (677434)Peak memory usage: 13 MB
% 15.53/2.64 % (677434)Instructions burned: 131 (million)
% 15.53/2.64 % (677443)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1508544751:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.53/2.64 % (677444)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=837160154:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.53/2.64 % TRYING [2,4,2]
% 15.53/2.64 % (677445)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=1015579509:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.53/2.64 % TRYING [1]
% 15.53/2.64 % TRYING [2]
% 15.53/2.64 % (677435)Instruction limit reached!
% 15.53/2.64 % (677435)------------------------------
% 15.53/2.64 % (677435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677435)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677435)Termination reason: Instruction limit
% 15.53/2.64 % (677435)Termination phase: Saturation
% 15.53/2.64 % (677435)Time elapsed: 0.108 s
% 15.53/2.64 % (677435)Peak memory usage: 14 MB
% 15.53/2.64 % (677435)Instructions burned: 160 (million)
% 15.53/2.64 % TRYING [3]
% 15.53/2.64 % (677449)ott-21_1_sil=16000:fs=off:random_seed=2746845218:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.53/2.64 % TRYING [1,5,1]
% 15.53/2.64 % TRYING [1,5,2]
% 15.53/2.64 % (677444)Instruction limit reached!
% 15.53/2.64 % (677444)------------------------------
% 15.53/2.64 % (677444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677444)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677444)Termination reason: Instruction limit
% 15.53/2.64 % (677444)Termination phase: Saturation
% 15.53/2.64 % (677444)Time elapsed: 0.078 s
% 15.53/2.64 % (677444)Peak memory usage: 13 MB
% 15.53/2.64 % (677444)Instructions burned: 131 (million)
% 15.53/2.64 % TRYING [4]
% 15.53/2.64 % (677451)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=257095409:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 15.53/2.64 % TRYING [3,4,2]
% 15.53/2.64 % (677449)Instruction limit reached!
% 15.53/2.64 % (677449)------------------------------
% 15.53/2.64 % (677449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677449)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677449)Termination reason: Instruction limit
% 15.53/2.64 % (677449)Termination phase: Saturation
% 15.53/2.64 % (677449)Time elapsed: 0.094 s
% 15.53/2.64 % (677449)Peak memory usage: 13 MB
% 15.53/2.64 % (677449)Instructions burned: 181 (million)
% 15.53/2.64 % (677453)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1874741709:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 15.53/2.64 % TRYING [1,1,1]
% 15.53/2.64 % TRYING [1,2,1]
% 15.53/2.64 % TRYING [1,3,1]
% 15.53/2.64 % TRYING [2,5,2]
% 15.53/2.64 % TRYING [1,2,2]
% 15.53/2.64 % TRYING [2,2,2]
% 15.53/2.64 % (677443)Instruction limit reached!
% 15.53/2.64 % (677443)------------------------------
% 15.53/2.64 % (677443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677443)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677443)Termination reason: Instruction limit
% 15.53/2.64 % (677443)Termination phase: Finite model building SAT solving
% 15.53/2.64 % (677443)Time elapsed: 0.292 s
% 15.53/2.64 % (677443)Peak memory usage: 43 MB
% 15.53/2.64 % (677443)Instructions burned: 715 (million)
% 15.53/2.64 % TRYING [1,6,1]
% 15.53/2.64 % TRYING [1,3,2]
% 15.53/2.64 % (677455)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1762500153:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 15.53/2.64 % TRYING [2,3,2]
% 15.53/2.64 % TRYING [1,6,2]
% 15.53/2.64 % (677445)Instruction limit reached!
% 15.53/2.64 % (677445)------------------------------
% 15.53/2.64 % (677445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677445)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677445)Termination reason: Instruction limit
% 15.53/2.64 % (677445)Termination phase: Saturation
% 15.53/2.64 % (677445)Time elapsed: 0.342 s
% 15.53/2.64 % (677445)Peak memory usage: 16 MB
% 15.53/2.64 % (677445)Instructions burned: 684 (million)
% 15.53/2.64 % (677457)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2038975817:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 15.53/2.64 % (677451)Instruction limit reached!
% 15.53/2.64 % (677451)------------------------------
% 15.53/2.64 % (677451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677451)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677451)Termination reason: Instruction limit
% 15.53/2.64 % (677451)Termination phase: Saturation
% 15.53/2.64 % (677451)Time elapsed: 0.305 s
% 15.53/2.64 % (677451)Peak memory usage: 14 MB
% 15.53/2.64 % (677451)Instructions burned: 477 (million)
% 15.53/2.64 % TRYING [4,4,2]
% 15.53/2.64 % TRYING [1,4,1]
% 15.53/2.64 % (677459)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=369804588: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)
% 15.53/2.64 % (677453)Instruction limit reached!
% 15.53/2.64 % (677453)------------------------------
% 15.53/2.64 % (677453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677453)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677453)Termination reason: Instruction limit
% 15.53/2.64 % (677453)Termination phase: Finite model building SAT solving
% 15.53/2.64 % (677453)Time elapsed: 0.338 s
% 15.53/2.64 % (677453)Peak memory usage: 17 MB
% 15.53/2.64 % (677453)Instructions burned: 865 (million)
% 15.53/2.64 % (677461)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1289243249:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 15.53/2.64 % TRYING [3,5,2]
% 15.53/2.64 % TRYING [3,4,3]
% 15.53/2.64 % (677457)Instruction limit reached!
% 15.53/2.64 % (677457)------------------------------
% 15.53/2.64 % (677457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677457)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677457)Termination reason: Instruction limit
% 15.53/2.64 % (677457)Termination phase: Finite model building constraint generation
% 15.53/2.64 % (677457)Time elapsed: 0.410 s
% 15.53/2.64 % (677457)Peak memory usage: 105 MB
% 15.53/2.64 % (677457)Instructions burned: 889 (million)
% 15.53/2.64 % (677463)fmb+10_1_sil=64000:random_seed=582871030:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 15.53/2.64 % TRYING [3,5,3]
% 15.53/2.64 % TRYING [1,1,1]
% 15.53/2.64 % TRYING [1,2,1]
% 15.53/2.64 % (677459)Instruction limit reached!
% 15.53/2.64 % (677459)------------------------------
% 15.53/2.64 % (677459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677459)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677459)Termination reason: Instruction limit
% 15.53/2.64 % (677459)Termination phase: Saturation
% 15.53/2.64 % (677459)Time elapsed: 0.428 s
% 15.53/2.64 % (677459)Peak memory usage: 20 MB
% 15.53/2.64 % (677459)Instructions burned: 692 (million)
% 15.53/2.64 % TRYING [1,3,1]
% 15.53/2.64 % (677465)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2095475901:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 15.53/2.64 % TRYING [20,20,20]
% 15.53/2.64 % TRYING [1,2,2]
% 15.53/2.64 % TRYING [2,2,2]
% 15.53/2.64 % TRYING [1,3,2]
% 15.53/2.64 % TRYING [3,4,4]
% 15.53/2.64 % TRYING [2,3,2]
% 15.53/2.64 % (677461)Instruction limit reached!
% 15.53/2.64 % (677461)------------------------------
% 15.53/2.64 % (677461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677461)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677461)Termination reason: Instruction limit
% 15.53/2.64 % (677461)Termination phase: Saturation
% 15.53/2.64 % (677461)Time elapsed: 0.483 s
% 15.53/2.64 % (677461)Peak memory usage: 19 MB
% 15.53/2.64 % (677461)Instructions burned: 881 (million)
% 15.53/2.64 % (677467)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2792670831:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 15.53/2.64 % TRYING [3,5,4]
% 15.53/2.64 % TRYING [8,8,8]
% 15.53/2.64 % (677455)Instruction limit reached!
% 15.53/2.64 % (677455)------------------------------
% 15.53/2.64 % (677455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677455)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677455)Termination reason: Instruction limit
% 15.53/2.64 % (677455)Termination phase: Saturation
% 15.53/2.64 % (677455)Time elapsed: 0.733 s
% 15.53/2.64 % (677455)Peak memory usage: 26 MB
% 15.53/2.64 % (677455)Instructions burned: 1180 (million)
% 15.53/2.64 % TRYING [1,4,1]
% 15.53/2.64 % (677469)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3529714477:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 15.53/2.64 % TRYING [1,4,2]
% 15.53/2.64 % TRYING [3,4,5]
% 15.53/2.64 % TRYING [3,5,5]
% 15.53/2.64 % TRYING [3,3,2]
% 15.53/2.64 % (677467)Instruction limit reached!
% 15.53/2.64 % (677467)------------------------------
% 15.53/2.64 % (677467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677467)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677467)Termination reason: Instruction limit
% 15.53/2.64 % (677467)Termination phase: Finite model building constraint generation
% 15.53/2.64 % (677467)Time elapsed: 0.294 s
% 15.53/2.64 % (677467)Peak memory usage: 56 MB
% 15.53/2.64 % (677467)Instructions burned: 921 (million)
% 15.53/2.64 % (677471)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1592147375:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 15.53/2.64 % TRYING [3,4,6]
% 15.53/2.64 % TRYING [2,4,2]
% 15.53/2.64 % TRYING [3,5,6]
% 15.53/2.64 % TRYING [1,5,1]
% 15.53/2.64 % TRYING [3,4,7]
% 15.53/2.64 % TRYING [3,5,7]
% 15.53/2.64 % TRYING [3,4,8]
% 15.53/2.64 % TRYING [1,5,2]
% 15.53/2.64 % TRYING [1,7,1]
% 15.53/2.64 % TRYING [2,6,2]
% 15.53/2.64 % (677430) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-677424-677430"...
% 15.53/2.64 % (677430)...printing done.
% 15.53/2.64 % (677430)Refutation found. Thanks to Tanya!
% 15.53/2.64 % SZS status Theorem for theBenchmark
% 15.53/2.64 % SZS output start Proof for theBenchmark
% See solution above
% 15.53/2.64 % (677430)------------------------------
% 15.53/2.64 % (677430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.53/2.64 % (677430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/2.64 % (677430)CaDiCaL version: 2.1.3
% 15.53/2.64 % (677430)Termination reason: Refutation
% 15.53/2.64 % (677430)Time elapsed: 2.156 s
% 15.53/2.64 % (677430)Peak memory usage: 36 MB
% 15.53/2.64 % (677430)Instructions burned: 4015 (million)
% 15.53/2.64 % (677424)Success in time 2.232 s
% 15.53/2.64 % Vampire exiting
%------------------------------------------------------------------------------