%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV739_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:26:19 PM UTC 2026
% Result : Theorem 101.11s 14.58s
% Output : Refutation 101.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 26
% Syntax : Number of formulae : 118 ( 43 unt; 0 typ; 7 def)
% Number of atoms : 407 ( 75 equ)
% Maximal formula atoms : 30 ( 3 avg)
% Number of connectives : 463 ( 174 ~; 171 |; 100 &)
% ( 9 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 6 ( 5 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 16 ( 14 usr; 8 prp; 0-3 aty)
% Number of functors : 48 ( 48 usr; 18 con; 0-5 aty)
% Number of variables : 238 ( 0 sgn 226 !; 12 ?; 238 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
event: $tType ).
tff(type_def_6,type,
bool: $tType ).
tff(type_def_7,type,
list: $tType > $tType ).
tff(type_def_8,type,
agent: $tType ).
tff(type_def_9,type,
msg: $tType ).
tff(type_def_10,type,
nat: $tType ).
tff(type_def_11,type,
fun: ( $tType * $tType ) > $tType ).
tff(func_def_0,type,
combb:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( fun(X0,X1) * fun(X2,X0) ) > fun(X2,X1) ) ).
tff(func_def_1,type,
combc:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( fun(X0,fun(X1,X2)) * X1 ) > fun(X0,X2) ) ).
tff(func_def_2,type,
combi:
!>[X0: $tType] : fun(X0,X0) ).
tff(func_def_3,type,
combk:
!>[X0: $tType,X1: $tType] : ( X0 > fun(X1,X0) ) ).
tff(func_def_4,type,
combs:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( fun(X0,fun(X1,X2)) * fun(X0,X1) ) > fun(X0,X2) ) ).
tff(func_def_5,type,
says: ( agent * agent * msg ) > event ).
tff(func_def_6,type,
knows: ( agent * list(event) ) > fun(msg,bool) ).
tff(func_def_7,type,
used: list(event) > fun(msg,bool) ).
tff(func_def_8,type,
uminus_uminus:
!>[X0: $tType] : ( X0 > X0 ) ).
tff(func_def_9,type,
sup_sup:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_10,type,
set:
!>[X0: $tType] : ( list(X0) > fun(X0,bool) ) ).
tff(func_def_11,type,
server: agent ).
tff(func_def_12,type,
spy: agent ).
tff(func_def_13,type,
analz: fun(msg,bool) > fun(msg,bool) ).
tff(func_def_14,type,
agent1: agent > msg ).
tff(func_def_15,type,
key: fun(nat,msg) ).
tff(func_def_16,type,
mPair: ( msg * msg ) > msg ).
tff(func_def_17,type,
nonce: nat > msg ).
tff(func_def_18,type,
symKeys: fun(nat,bool) ).
tff(func_def_19,type,
nS_Sha254967238shared: fun(list(event),bool) ).
tff(func_def_20,type,
top_top:
!>[X0: $tType] : X0 ).
tff(func_def_21,type,
shrK: fun(agent,nat) ).
tff(func_def_22,type,
collect:
!>[X0: $tType] : ( fun(X0,bool) > fun(X0,bool) ) ).
tff(func_def_23,type,
image:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,X1) * fun(X0,bool) ) > fun(X1,bool) ) ).
tff(func_def_24,type,
aa:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,X1) * X0 ) > X1 ) ).
tff(func_def_25,type,
fFalse: bool ).
tff(func_def_26,type,
fNot: fun(bool,bool) ).
tff(func_def_27,type,
fTrue: bool ).
tff(func_def_28,type,
fdisj: fun(bool,fun(bool,bool)) ).
tff(func_def_29,type,
member:
!>[X0: $tType] : fun(X0,fun(fun(X0,bool),bool)) ).
tff(func_def_30,type,
a: agent ).
tff(func_def_31,type,
a1: agent ).
tff(func_def_32,type,
b: agent ).
tff(func_def_33,type,
k: nat ).
tff(func_def_34,type,
kab: nat ).
tff(func_def_35,type,
kk: fun(nat,bool) ).
tff(func_def_36,type,
na: nat ).
tff(func_def_37,type,
evs2: list(event) ).
tff(func_def_38,type,
sK2:
!>[X0: $tType,X1: $tType] : ( ( fun(X1,bool) * fun(X1,X0) * X0 ) > X1 ) ).
tff(func_def_39,type,
sK3:
!>[X0: $tType] : ( ( fun(X0,bool) * fun(X0,bool) ) > X0 ) ).
tff(func_def_40,type,
sK4:
!>[X0: $tType] : ( ( fun(X0,bool) * fun(X0,bool) ) > X0 ) ).
tff(func_def_41,type,
sK5:
!>[X0: $tType] : ( ( fun(X0,bool) * fun(X0,bool) * fun(X0,bool) ) > X0 ) ).
tff(func_def_42,type,
sK6:
!>[X0: $tType] : ( ( fun(X0,bool) * fun(X0,bool) * fun(X0,bool) ) > X0 ) ).
tff(func_def_43,type,
sK7:
!>[X0: $tType] : ( ( fun(X0,bool) * fun(X0,bool) ) > X0 ) ).
tff(func_def_44,type,
sK8:
!>[X0: $tType] : ( ( fun(X0,bool) * fun(X0,bool) ) > X0 ) ).
tff(func_def_45,type,
sK9:
!>[X0: $tType,X1: $tType] : ( ( fun(X1,X0) * fun(X1,X0) ) > X1 ) ).
tff(pred_def_1,type,
bounded_lattice:
!>[X0: $tType] : $o ).
tff(pred_def_2,type,
lattice:
!>[X0: $tType] : $o ).
tff(pred_def_3,type,
boolean_algebra:
!>[X0: $tType] : $o ).
tff(pred_def_4,type,
semilattice_sup:
!>[X0: $tType] : $o ).
tff(pred_def_5,type,
bounded_lattice_top:
!>[X0: $tType] : $o ).
tff(pred_def_6,type,
ord_less_eq:
!>[X0: $tType] : ( ( X0 * X0 ) > $o ) ).
tff(pred_def_7,type,
pp: bool > $o ).
tff(f18,axiom,
! [X0: $tType,X1: X0] : pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X1),top_top(fun(X0,bool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_UNIV__I) ).
tff(f68,axiom,
! [X0: $tType,X1: $tType,X2: fun(X1,bool),X3: fun(X1,X0),X4: X0] :
( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),image(X1,X0,X3,X2)))
<=> ? [X5: X1] :
( pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),X5),X2))
& ( X4 = aa(X1,X0,X3,X5) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_image__iff) ).
tff(f73,axiom,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool),X3: fun(X0,bool)] :
( ! [X4: X0] :
( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),sup_sup(fun(X0,bool),X3,X2)))
=> pp(aa(X0,bool,X1,X4)) )
<=> ( ! [X4: X0] :
( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),X3))
=> pp(aa(X0,bool,X1,X4)) )
& ! [X4: X0] :
( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),X2))
=> pp(aa(X0,bool,X1,X4)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_ball__Un) ).
tff(f78,axiom,
! [X0: $tType,X1: fun(X0,bool)] : ( collect(X0,X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_Collect__def) ).
tff(f82,axiom,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool)] : ( sup_sup(fun(X0,bool),X2,X1) = sup_sup(fun(X0,bool),X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_Un__commute) ).
tff(f88,axiom,
! [X0: $tType,X1: fun(X0,bool)] : ( uminus_uminus(fun(X0,bool),uminus_uminus(fun(X0,bool),X1)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_double__complement) ).
tff(f89,axiom,
! [X0: $tType,X1: fun(X0,bool)] : ( uminus_uminus(fun(X0,bool),X1) = collect(X0,combb(bool,bool,X0,fNot,combc(X0,fun(X0,bool),bool,member(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_Compl__eq) ).
tff(f94,axiom,
! [X0: $tType,X1: fun(X0,bool)] : ( collect(X0,combb(bool,bool,X0,fNot,X1)) = uminus_uminus(fun(X0,bool),collect(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_Collect__neg__eq) ).
tff(f99,axiom,
! [X0: $tType] :
( semilattice_sup(X0)
=> ! [X1: X0,X2: X0] :
( ord_less_eq(X0,X2,X1)
=> ( sup_sup(X0,X1,X2) = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_sup__absorb1) ).
tff(f104,axiom,
! [X0: $tType,X1: $tType] :
( lattice(X1)
=> semilattice_sup(fun(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_fun___Lattices_Osemilattice__sup) ).
tff(f112,axiom,
lattice(bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_HOL_Obool___Lattices_Olattice) ).
tff(f113,axiom,
~ pp(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_pp_1_1_U) ).
tff(f115,axiom,
! [X0: bool] :
( ~ pp(aa(bool,bool,fNot,X0))
| ~ pp(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fNot_1_1_U) ).
tff(f117,axiom,
! [X0: $tType,X1: $tType,X2: $tType,X3: X2,X4: fun(X2,X1),X5: fun(X1,X0)] : ( aa(X2,X0,combb(X1,X0,X2,X5,X4),X3) = aa(X1,X0,X5,aa(X2,X1,X4,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBB_1_1_U) ).
tff(f118,axiom,
! [X0: $tType,X1: $tType,X2: $tType,X3: X0,X4: X2,X5: fun(X0,fun(X2,X1))] : ( aa(X0,X1,combc(X0,X2,X1,X5,X4),X3) = aa(X2,X1,aa(X0,fun(X2,X1),X5,X3),X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBC_1_1_U) ).
tff(f122,axiom,
pp(fTrue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fTrue_1_1_U) ).
tff(f123,axiom,
! [X0: bool] :
( ( X0 = fTrue )
| ( X0 = fFalse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fTrue_1_1_T) ).
tff(f132,axiom,
ord_less_eq(fun(nat,bool),kk,uminus_uminus(fun(nat,bool),image(agent,nat,shrK,top_top(fun(agent,bool))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_5) ).
tff(f133,conjecture,
( ( ( ( aa(agent,nat,shrK,b) != kab )
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2)))) )
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,a))),analz(knows(spy,evs2))))
| ( ( ( ( aa(agent,nat,shrK,b) != kab )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,b)),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2)))) )
| ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
| ( ( k != kab )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
& ( ( aa(agent,nat,shrK,b) = kab )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,b)),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2))))
| ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
| ( ( k != kab )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) ) ) )
& ( ( aa(agent,nat,shrK,b) = kab )
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2))))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,a))),analz(knows(spy,evs2))))
| ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
| ( ( k != kab )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_6) ).
tff(f134,negated_conjecture,
~ ( ( ( ( aa(agent,nat,shrK,b) != kab )
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2)))) )
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,a))),analz(knows(spy,evs2))))
| ( ( ( ( aa(agent,nat,shrK,b) != kab )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,b)),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2)))) )
| ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
| ( ( k != kab )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
& ( ( aa(agent,nat,shrK,b) = kab )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,b)),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2))))
| ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
| ( ( k != kab )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) ) ) )
& ( ( aa(agent,nat,shrK,b) = kab )
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2))))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,a))),analz(knows(spy,evs2))))
| ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
| ( ( k != kab )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) ) ),
inference(negated_conjecture,[status(cth)],[f133]) ).
tff(f136,plain,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool),X3: fun(X0,bool)] :
( ! [X4: X0] :
( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),sup_sup(fun(X0,bool),X3,X2)))
=> pp(aa(X0,bool,X1,X4)) )
<=> ( ! [X5: X0] :
( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X5),X3))
=> pp(aa(X0,bool,X1,X5)) )
& ! [X6: X0] :
( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X6),X2))
=> pp(aa(X0,bool,X1,X6)) ) ) ),
inference(rectify,[],[f73]) ).
tff(f195,plain,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool),X3: fun(X0,bool)] :
( ! [X4: X0] :
( pp(aa(X0,bool,X1,X4))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),sup_sup(fun(X0,bool),X3,X2))) )
<=> ( ! [X5: X0] :
( pp(aa(X0,bool,X1,X5))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X5),X3)) )
& ! [X6: X0] :
( pp(aa(X0,bool,X1,X6))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X6),X2)) ) ) ),
inference(ennf_transformation,[],[f136]) ).
tff(f208,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0] :
( ( sup_sup(X0,X1,X2) = X1 )
| ~ ord_less_eq(X0,X2,X1) )
| ~ semilattice_sup(X0) ),
inference(ennf_transformation,[],[f99]) ).
tff(f212,plain,
! [X0: $tType,X1: $tType] :
( semilattice_sup(fun(X0,X1))
| ~ lattice(X1) ),
inference(ennf_transformation,[],[f104]) ).
tff(f216,plain,
( ( ( ( kab = aa(agent,nat,shrK,b) )
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2)))) )
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,a))),analz(knows(spy,evs2))))
& ( ( ( ( kab = aa(agent,nat,shrK,b) )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,b)),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2)))) )
& pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
& ( ( kab = k )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
| ( ( kab != aa(agent,nat,shrK,b) )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,b)),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2))))
& pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
& ( ( kab = k )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) ) ) )
| ( ( kab != aa(agent,nat,shrK,b) )
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2))))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,a))),analz(knows(spy,evs2))))
& pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
& ( ( kab = k )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) ) ),
inference(ennf_transformation,[],[f134]) ).
tff(f217,definition,
( ( ( kab != aa(agent,nat,shrK,b) )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,b)),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2))))
& pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
& ( ( kab = k )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f218,definition,
( ( ( kab != aa(agent,nat,shrK,b) )
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2))))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,a))),analz(knows(spy,evs2))))
& pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
& ( ( kab = k )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
tff(f219,plain,
( ( ( ( kab = aa(agent,nat,shrK,b) )
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2)))) )
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,a))),analz(knows(spy,evs2))))
& ( ( ( ( kab = aa(agent,nat,shrK,b) )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,b)),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2)))) )
& pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
& ( ( kab = k )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
| sP0 ) )
| sP1 ),
inference(definition_folding,[],[f216,f218,f217]) ).
tff(f242,plain,
! [X0: $tType,X1: $tType,X2: fun(X1,bool),X3: fun(X1,X0),X4: X0] :
( ( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),image(X1,X0,X3,X2)))
| ! [X5: X1] :
( ~ pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),X5),X2))
| ( aa(X1,X0,X3,X5) != X4 ) ) )
& ( ? [X5: X1] :
( pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),X5),X2))
& ( X4 = aa(X1,X0,X3,X5) ) )
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),image(X1,X0,X3,X2))) ) ),
inference(nnf_transformation,[],[f68]) ).
tff(f243,plain,
! [X0: $tType,X1: $tType,X2: fun(X1,bool),X3: fun(X1,X0),X4: X0] :
( ( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),image(X1,X0,X3,X2)))
| ! [X5: X1] :
( ~ pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),X5),X2))
| ( aa(X1,X0,X3,X5) != X4 ) ) )
& ( ? [X6: X1] :
( pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),X6),X2))
& ( aa(X1,X0,X3,X6) = X4 ) )
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),image(X1,X0,X3,X2))) ) ),
inference(rectify,[],[f242]) ).
tff(f244,plain,
! [X0: $tType,X1: $tType,X2: fun(X1,bool),X3: fun(X1,X0),X4: X0] :
( ( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),image(X1,X0,X3,X2)))
| ! [X5: X1] :
( ~ pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),X5),X2))
| ( aa(X1,X0,X3,X5) != X4 ) ) )
& ( ( pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),sK2(X0,X1,X2,X3,X4)),X2))
& ( aa(X1,X0,X3,sK2(X0,X1,X2,X3,X4)) = X4 ) )
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),image(X1,X0,X3,X2))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X6,sK2(X0,X1,X2,X3,X4))],[f243]) ).
tff(f245,plain,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool),X3: fun(X0,bool)] :
( ( ! [X4: X0] :
( pp(aa(X0,bool,X1,X4))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),sup_sup(fun(X0,bool),X3,X2))) )
| ? [X5: X0] :
( ~ pp(aa(X0,bool,X1,X5))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X5),X3)) )
| ? [X6: X0] :
( ~ pp(aa(X0,bool,X1,X6))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X6),X2)) ) )
& ( ( ! [X5: X0] :
( pp(aa(X0,bool,X1,X5))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X5),X3)) )
& ! [X6: X0] :
( pp(aa(X0,bool,X1,X6))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X6),X2)) ) )
| ? [X4: X0] :
( ~ pp(aa(X0,bool,X1,X4))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),sup_sup(fun(X0,bool),X3,X2))) ) ) ),
inference(nnf_transformation,[],[f195]) ).
tff(f246,plain,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool),X3: fun(X0,bool)] :
( ( ! [X4: X0] :
( pp(aa(X0,bool,X1,X4))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),sup_sup(fun(X0,bool),X3,X2))) )
| ? [X5: X0] :
( ~ pp(aa(X0,bool,X1,X5))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X5),X3)) )
| ? [X6: X0] :
( ~ pp(aa(X0,bool,X1,X6))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X6),X2)) ) )
& ( ( ! [X5: X0] :
( pp(aa(X0,bool,X1,X5))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X5),X3)) )
& ! [X6: X0] :
( pp(aa(X0,bool,X1,X6))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X6),X2)) ) )
| ? [X4: X0] :
( ~ pp(aa(X0,bool,X1,X4))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),sup_sup(fun(X0,bool),X3,X2))) ) ) ),
inference(flattening,[],[f245]) ).
tff(f247,plain,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool),X3: fun(X0,bool)] :
( ( ! [X4: X0] :
( pp(aa(X0,bool,X1,X4))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),sup_sup(fun(X0,bool),X3,X2))) )
| ? [X5: X0] :
( ~ pp(aa(X0,bool,X1,X5))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X5),X3)) )
| ? [X6: X0] :
( ~ pp(aa(X0,bool,X1,X6))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X6),X2)) ) )
& ( ( ! [X7: X0] :
( pp(aa(X0,bool,X1,X7))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X7),X3)) )
& ! [X8: X0] :
( pp(aa(X0,bool,X1,X8))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X8),X2)) ) )
| ? [X9: X0] :
( ~ pp(aa(X0,bool,X1,X9))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X9),sup_sup(fun(X0,bool),X3,X2))) ) ) ),
inference(rectify,[],[f246]) ).
tff(f248,plain,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool),X3: fun(X0,bool)] :
( ( ! [X4: X0] :
( pp(aa(X0,bool,X1,X4))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),sup_sup(fun(X0,bool),X3,X2))) )
| ( ~ pp(aa(X0,bool,X1,sK3(X0,X1,X3)))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),sK3(X0,X1,X3)),X3)) )
| ( ~ pp(aa(X0,bool,X1,sK4(X0,X1,X2)))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),sK4(X0,X1,X2)),X2)) ) )
& ( ( ! [X7: X0] :
( pp(aa(X0,bool,X1,X7))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X7),X3)) )
& ! [X8: X0] :
( pp(aa(X0,bool,X1,X8))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X8),X2)) ) )
| ( ~ pp(aa(X0,bool,X1,sK5(X0,X1,X2,X3)))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),sK5(X0,X1,X2,X3)),sup_sup(fun(X0,bool),X3,X2))) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5]),skolemize(X5,sK3(X0,X1,X3)),skolemize(X6,sK4(X0,X1,X2)),skolemize(X9,sK5(X0,X1,X2,X3))],[f247]) ).
tff(f258,plain,
( ( ( kab != aa(agent,nat,shrK,b) )
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2))))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,a))),analz(knows(spy,evs2))))
& pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
& ( ( kab = k )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
| ~ sP1 ),
inference(nnf_transformation,[],[f218]) ).
tff(f259,plain,
( ( ( kab != aa(agent,nat,shrK,b) )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,b)),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,aa(agent,nat,shrK,b))),analz(knows(spy,evs2))))
& pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
& ( ( kab = k )
| pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
| pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
& ~ pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),k),kk))
& ~ pp(aa(fun(msg,bool),bool,aa(msg,fun(fun(msg,bool),bool),member(msg),aa(nat,msg,key,k)),analz(knows(spy,evs2)))) )
| ~ sP0 ),
inference(nnf_transformation,[],[f217]) ).
tff(f281,plain,
! [X0: $tType,X1: X0] : pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X1),top_top(fun(X0,bool)))),
inference(cnf_transformation,[],[f18]) ).
tff(f356,plain,
! [X1: $tType,X0: $tType,X2: fun(X1,bool),X3: fun(X1,X0),X4: X0,X5: X1] :
( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X4),image(X1,X0,X3,X2)))
| ~ pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),X5),X2))
| ( aa(X1,X0,X3,X5) != X4 ) ),
inference(cnf_transformation,[],[f244]) ).
tff(f363,plain,
! [X0: $tType,X2: fun(X0,bool),X3: fun(X0,bool),X1: fun(X0,bool),X7: X0] :
( pp(aa(X0,bool,X1,X7))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X7),X3))
| pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),sK5(X0,X1,X2,X3)),sup_sup(fun(X0,bool),X3,X2))) ),
inference(cnf_transformation,[],[f248]) ).
tff(f364,plain,
! [X0: $tType,X2: fun(X0,bool),X3: fun(X0,bool),X1: fun(X0,bool),X7: X0] :
( pp(aa(X0,bool,X1,X7))
| ~ pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X7),X3))
| ~ pp(aa(X0,bool,X1,sK5(X0,X1,X2,X3))) ),
inference(cnf_transformation,[],[f248]) ).
tff(f381,plain,
! [X0: $tType,X1: fun(X0,bool)] : ( collect(X0,X1) = X1 ),
inference(cnf_transformation,[],[f78]) ).
tff(f385,plain,
! [X0: $tType,X2: fun(X0,bool),X1: fun(X0,bool)] : ( sup_sup(fun(X0,bool),X1,X2) = sup_sup(fun(X0,bool),X2,X1) ),
inference(cnf_transformation,[],[f82]) ).
tff(f391,plain,
! [X0: $tType,X1: fun(X0,bool)] : ( uminus_uminus(fun(X0,bool),uminus_uminus(fun(X0,bool),X1)) = X1 ),
inference(cnf_transformation,[],[f88]) ).
tff(f392,plain,
! [X0: $tType,X1: fun(X0,bool)] : ( uminus_uminus(fun(X0,bool),X1) = collect(X0,combb(bool,bool,X0,fNot,combc(X0,fun(X0,bool),bool,member(X0),X1))) ),
inference(cnf_transformation,[],[f89]) ).
tff(f398,plain,
! [X0: $tType,X1: fun(X0,bool)] : ( collect(X0,combb(bool,bool,X0,fNot,X1)) = uminus_uminus(fun(X0,bool),collect(X0,X1)) ),
inference(cnf_transformation,[],[f94]) ).
tff(f404,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ~ ord_less_eq(X0,X2,X1)
| ( sup_sup(X0,X1,X2) = X1 )
| ~ semilattice_sup(X0) ),
inference(cnf_transformation,[],[f208]) ).
tff(f409,plain,
! [X1: $tType,X0: $tType] :
( semilattice_sup(fun(X0,X1))
| ~ lattice(X1) ),
inference(cnf_transformation,[],[f212]) ).
tff(f417,plain,
lattice(bool),
inference(cnf_transformation,[],[f112]) ).
tff(f418,plain,
~ pp(fFalse),
inference(cnf_transformation,[],[f113]) ).
tff(f420,plain,
! [X0: bool] :
( ~ pp(aa(bool,bool,fNot,X0))
| ~ pp(X0) ),
inference(cnf_transformation,[],[f115]) ).
tff(f422,plain,
! [X1: $tType,X0: $tType,X2: $tType,X3: X2,X4: fun(X2,X1),X5: fun(X1,X0)] : ( aa(X2,X0,combb(X1,X0,X2,X5,X4),X3) = aa(X1,X0,X5,aa(X2,X1,X4,X3)) ),
inference(cnf_transformation,[],[f117]) ).
tff(f423,plain,
! [X1: $tType,X0: $tType,X2: $tType,X3: X0,X4: X2,X5: fun(X0,fun(X2,X1))] : ( aa(X0,X1,combc(X0,X2,X1,X5,X4),X3) = aa(X2,X1,aa(X0,fun(X2,X1),X5,X3),X4) ),
inference(cnf_transformation,[],[f118]) ).
tff(f427,plain,
pp(fTrue),
inference(cnf_transformation,[],[f122]) ).
tff(f428,plain,
! [X0: bool] :
( ( fTrue = X0 )
| ( fFalse = X0 ) ),
inference(cnf_transformation,[],[f123]) ).
tff(f439,plain,
ord_less_eq(fun(nat,bool),kk,uminus_uminus(fun(nat,bool),image(agent,nat,shrK,top_top(fun(agent,bool))))),
inference(cnf_transformation,[],[f132]) ).
tff(f443,plain,
( pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
| ~ sP1 ),
inference(cnf_transformation,[],[f258]) ).
tff(f450,plain,
( pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
| ~ sP0 ),
inference(cnf_transformation,[],[f259]) ).
tff(f457,plain,
( pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f219]) ).
tff(f480,plain,
! [X1: $tType,X0: $tType,X2: fun(X1,bool),X3: fun(X1,X0),X5: X1] :
( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),aa(X1,X0,X3,X5)),image(X1,X0,X3,X2)))
| ~ pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),X5),X2)) ),
inference(equality_resolution,[],[f356]) ).
tff(f484,definition,
( spl10_1
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl10_1])],[avatar_definition]) ).
tff(f488,definition,
( spl10_2
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl10_2])],[avatar_definition]) ).
tff(f503,definition,
( spl10_5
<=> pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk)) ),
introduced(definition,[new_symbols(definition,[spl10_5])],[avatar_definition]) ).
tff(f505,plain,
( pp(aa(fun(nat,bool),bool,aa(nat,fun(fun(nat,bool),bool),member(nat),aa(agent,nat,shrK,a)),kk))
| ~ spl10_5 ),
inference(avatar_component_clause,[],[f503]) ).
tff(f506,plain,
( spl10_1
| spl10_2
| spl10_5 ),
inference(avatar_split_clause,[],[f457,f503,f488,f484]) ).
tff(f529,plain,
( ~ spl10_2
| spl10_5 ),
inference(avatar_split_clause,[],[f450,f503,f488]) ).
tff(f536,plain,
( ~ spl10_1
| spl10_5 ),
inference(avatar_split_clause,[],[f443,f503,f484]) ).
tff(f540,plain,
! [X0: $tType,X1: fun(X0,bool)] : ( uminus_uminus(fun(X0,bool),X1) = uminus_uminus(fun(X0,bool),collect(X0,combc(X0,fun(X0,bool),bool,member(X0),X1))) ),
inference(forward_demodulation,[],[f392,f398]) ).
tff(f557,plain,
! [X0: $tType,X2: fun(X0,bool),X3: fun(X0,bool),X1: fun(X0,bool),X7: X0] :
( ~ pp(aa(X0,bool,combc(X0,fun(X0,bool),bool,member(X0),X3),X7))
| pp(aa(X0,bool,X1,X7))
| pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),sK5(X0,X1,X2,X3)),sup_sup(fun(X0,bool),X3,X2))) ),
inference(forward_demodulation,[],[f363,f423]) ).
tff(f558,plain,
! [X0: $tType,X2: fun(X0,bool),X3: fun(X0,bool),X1: fun(X0,bool),X7: X0] :
( ~ pp(aa(X0,bool,combc(X0,fun(X0,bool),bool,member(X0),X3),X7))
| pp(aa(X0,bool,X1,X7))
| ~ pp(aa(X0,bool,X1,sK5(X0,X1,X2,X3))) ),
inference(forward_demodulation,[],[f364,f423]) ).
tff(f568,plain,
! [X1: $tType,X0: $tType,X2: fun(X1,bool),X3: fun(X1,X0),X5: X1] :
( pp(aa(X0,bool,combc(X0,fun(X0,bool),bool,member(X0),image(X1,X0,X3,X2)),aa(X1,X0,X3,X5)))
| ~ pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),X5),X2)) ),
inference(forward_demodulation,[],[f480,f423]) ).
tff(f587,plain,
! [X0: $tType,X1: X0] : pp(aa(X0,bool,combc(X0,fun(X0,bool),bool,member(X0),top_top(fun(X0,bool))),X1)),
inference(forward_demodulation,[],[f281,f423]) ).
tff(f608,plain,
! [X0: $tType,X1: fun(X0,bool)] : ( uminus_uminus(fun(X0,bool),X1) = uminus_uminus(fun(X0,bool),combc(X0,fun(X0,bool),bool,member(X0),X1)) ),
inference(forward_demodulation,[],[f540,f381]) ).
tff(f619,plain,
! [X0: $tType,X2: fun(X0,bool),X3: fun(X0,bool),X1: fun(X0,bool),X7: X0] :
( ~ pp(aa(X0,bool,combc(X0,fun(X0,bool),bool,member(X0),X3),X7))
| pp(aa(X0,bool,combc(X0,fun(X0,bool),bool,member(X0),sup_sup(fun(X0,bool),X3,X2)),sK5(X0,X1,X2,X3)))
| pp(aa(X0,bool,X1,X7)) ),
inference(forward_demodulation,[],[f557,f423]) ).
tff(f626,plain,
! [X1: $tType,X0: $tType,X2: fun(X1,bool),X3: fun(X1,X0),X5: X1] :
( ~ pp(aa(X1,bool,combc(X1,fun(X1,bool),bool,member(X1),X2),X5))
| pp(aa(X0,bool,combc(X0,fun(X0,bool),bool,member(X0),image(X1,X0,X3,X2)),aa(X1,X0,X3,X5))) ),
inference(forward_demodulation,[],[f568,f423]) ).
tff(f663,plain,
( pp(aa(nat,bool,combc(nat,fun(nat,bool),bool,member(nat),kk),aa(agent,nat,shrK,a)))
| ~ spl10_5 ),
inference(forward_demodulation,[],[f505,f423]) ).
tff(f694,plain,
! [X0: bool] :
( ~ pp(fTrue)
| ~ pp(X0)
| ( fFalse = aa(bool,bool,fNot,X0) ) ),
inference(superposition,[],[f420,f428]) ).
tff(f695,plain,
! [X0: bool] :
( ~ pp(X0)
| ( fFalse = aa(bool,bool,fNot,X0) ) ),
inference(forward_subsumption_resolution,[],[f694,f427]) ).
tff(f833,plain,
( ( uminus_uminus(fun(nat,bool),image(agent,nat,shrK,top_top(fun(agent,bool)))) = sup_sup(fun(nat,bool),uminus_uminus(fun(nat,bool),image(agent,nat,shrK,top_top(fun(agent,bool)))),kk) )
| ~ semilattice_sup(fun(nat,bool)) ),
inference(resolution,[],[f439,f404]) ).
tff(f834,plain,
( ( uminus_uminus(fun(nat,bool),image(agent,nat,shrK,top_top(fun(agent,bool)))) = sup_sup(fun(nat,bool),kk,uminus_uminus(fun(nat,bool),image(agent,nat,shrK,top_top(fun(agent,bool))))) )
| ~ semilattice_sup(fun(nat,bool)) ),
inference(forward_demodulation,[],[f833,f385]) ).
tff(f836,definition,
( spl10_15
<=> semilattice_sup(fun(nat,bool)) ),
introduced(definition,[new_symbols(definition,[spl10_15])],[avatar_definition]) ).
tff(f838,plain,
( ~ semilattice_sup(fun(nat,bool))
| spl10_15 ),
inference(avatar_component_clause,[],[f836]) ).
tff(f840,definition,
( spl10_16
<=> ( uminus_uminus(fun(nat,bool),image(agent,nat,shrK,top_top(fun(agent,bool)))) = sup_sup(fun(nat,bool),kk,uminus_uminus(fun(nat,bool),image(agent,nat,shrK,top_top(fun(agent,bool))))) ) ),
introduced(definition,[new_symbols(definition,[spl10_16])],[avatar_definition]) ).
tff(f842,plain,
( ( uminus_uminus(fun(nat,bool),image(agent,nat,shrK,top_top(fun(agent,bool)))) = sup_sup(fun(nat,bool),kk,uminus_uminus(fun(nat,bool),image(agent,nat,shrK,top_top(fun(agent,bool))))) )
| ~ spl10_16 ),
inference(avatar_component_clause,[],[f840]) ).
tff(f844,plain,
( ~ spl10_15
| spl10_16 ),
inference(avatar_split_clause,[],[f834,f840,f836]) ).
tff(f919,plain,
! [X0: $tType,X1: fun(X0,bool)] : ( combb(bool,bool,X0,fNot,X1) = uminus_uminus(fun(X0,bool),collect(X0,X1)) ),
inference(superposition,[],[f381,f398]) ).
tff(f920,plain,
! [X0: $tType,X1: fun(X0,bool)] : ( uminus_uminus(fun(X0,bool),X1) = combb(bool,bool,X0,fNot,X1) ),
inference(forward_demodulation,[],[f919,f381]) ).
tff(f961,plain,
( ~ lattice(bool)
| spl10_15 ),
inference(resolution,[],[f838,f409]) ).
tff(f962,plain,
( $false
| spl10_15 ),
inference(forward_subsumption_resolution,[],[f961,f417]) ).
tff(f963,plain,
spl10_15,
inference(avatar_contradiction_clause,[],[f962]) ).
tff(f1045,plain,
! [X0: $tType,X1: fun(X0,bool)] : ( combc(X0,fun(X0,bool),bool,member(X0),X1) = uminus_uminus(fun(X0,bool),uminus_uminus(fun(X0,bool),X1)) ),
inference(superposition,[],[f391,f608]) ).
tff(f1052,plain,
! [X0: $tType,X1: fun(X0,bool)] : ( combc(X0,fun(X0,bool),bool,member(X0),X1) = X1 ),
inference(forward_demodulation,[],[f1045,f391]) ).
tff(f1329,plain,
( ! [X0: fun(nat,bool),X1: fun(nat,bool)] :
( ~ pp(aa(nat,bool,X0,sK5(nat,X0,X1,kk)))
| pp(aa(nat,bool,X0,aa(agent,nat,shrK,a))) )
| ~ spl10_5 ),
inference(resolution,[],[f558,f663]) ).
tff(f1611,plain,
! [X1: $tType,X0: $tType,X2: fun(X1,X0),X3: X1] : pp(aa(X0,bool,combc(X0,fun(X0,bool),bool,member(X0),image(X1,X0,X2,top_top(fun(X1,bool)))),aa(X1,X0,X2,X3))),
inference(resolution,[],[f626,f587]) ).
tff(f1641,plain,
! [X1: $tType,X0: $tType,X2: fun(X1,X0),X3: X1] : pp(aa(X0,bool,image(X1,X0,X2,top_top(fun(X1,bool))),aa(X1,X0,X2,X3))),
inference(forward_demodulation,[],[f1611,f1052]) ).
tff(f1890,plain,
( ! [X0: fun(nat,bool),X1: fun(nat,bool)] :
( pp(aa(nat,bool,combc(nat,fun(nat,bool),bool,member(nat),sup_sup(fun(nat,bool),kk,X0)),sK5(nat,X1,X0,kk)))
| pp(aa(nat,bool,X1,aa(agent,nat,shrK,a))) )
| ~ spl10_5 ),
inference(resolution,[],[f619,f663]) ).
tff(f1908,plain,
( ! [X0: fun(nat,bool),X1: fun(nat,bool)] :
( pp(aa(nat,bool,sup_sup(fun(nat,bool),kk,X0),sK5(nat,X1,X0,kk)))
| pp(aa(nat,bool,X1,aa(agent,nat,shrK,a))) )
| ~ spl10_5 ),
inference(forward_demodulation,[],[f1890,f1052]) ).
tff(f2605,plain,
( ! [X0: fun(nat,bool)] :
( pp(aa(nat,bool,sup_sup(fun(nat,bool),kk,X0),aa(agent,nat,shrK,a)))
| pp(aa(nat,bool,sup_sup(fun(nat,bool),kk,X0),aa(agent,nat,shrK,a))) )
| ~ spl10_5 ),
inference(resolution,[],[f1908,f1329]) ).
tff(f2613,plain,
( ! [X0: fun(nat,bool)] : pp(aa(nat,bool,sup_sup(fun(nat,bool),kk,X0),aa(agent,nat,shrK,a)))
| ~ spl10_5 ),
inference(duplicate_literal_removal,[],[f2605]) ).
tff(f4883,plain,
! [X0: $tType,X2: X0,X1: fun(X0,bool)] : ( aa(bool,bool,fNot,aa(X0,bool,X1,X2)) = aa(X0,bool,uminus_uminus(fun(X0,bool),X1),X2) ),
inference(superposition,[],[f422,f920]) ).
tff(f6523,plain,
! [X1: $tType,X0: $tType,X2: fun(X1,X0),X3: X1] : ( fFalse = aa(bool,bool,fNot,aa(X0,bool,image(X1,X0,X2,top_top(fun(X1,bool))),aa(X1,X0,X2,X3))) ),
inference(resolution,[],[f1641,f695]) ).
tff(f73052,plain,
( pp(aa(nat,bool,uminus_uminus(fun(nat,bool),image(agent,nat,shrK,top_top(fun(agent,bool)))),aa(agent,nat,shrK,a)))
| ~ spl10_5
| ~ spl10_16 ),
inference(superposition,[],[f2613,f842]) ).
tff(f73077,plain,
( pp(aa(bool,bool,fNot,aa(nat,bool,image(agent,nat,shrK,top_top(fun(agent,bool))),aa(agent,nat,shrK,a))))
| ~ spl10_5
| ~ spl10_16 ),
inference(forward_demodulation,[],[f73052,f4883]) ).
tff(f73085,plain,
( pp(fFalse)
| ~ spl10_5
| ~ spl10_16 ),
inference(forward_demodulation,[],[f73077,f6523]) ).
tff(f73089,plain,
( $false
| ~ spl10_5
| ~ spl10_16 ),
inference(forward_subsumption_resolution,[],[f73085,f418]) ).
tff(f73090,plain,
( ~ spl10_5
| ~ spl10_16 ),
inference(avatar_contradiction_clause,[],[f73089]) ).
cnf(s7,plain,
( spl10_1
| spl10_2
| spl10_5 ),
inference(sat_conversion,[],[f506]) ).
cnf(s20,plain,
( ~ spl10_2
| spl10_5 ),
inference(sat_conversion,[],[f529]) ).
cnf(s33,plain,
( ~ spl10_1
| spl10_5 ),
inference(sat_conversion,[],[f536]) ).
cnf(s253,plain,
( ~ spl10_15
| spl10_16 ),
inference(sat_conversion,[],[f844]) ).
cnf(s297,plain,
spl10_15,
inference(sat_conversion,[],[f963]) ).
cnf(s29511,plain,
( ~ spl10_5
| ~ spl10_16 ),
inference(sat_conversion,[],[f73090]) ).
cnf(s29542,plain,
spl10_16,
inference(rat,[],[s253,s297]) ).
cnf(s29543,plain,
~ spl10_5,
inference(rat,[],[s29511,s29542]) ).
cnf(s29561,plain,
~ spl10_1,
inference(rat,[],[s33,s29543]) ).
cnf(s29562,plain,
~ spl10_2,
inference(rat,[],[s20,s29543]) ).
cnf(s29586,plain,
$false,
inference(rat,[],[s7,s29543,s29562,s29561]) ).
tff(f73091,plain,
$false,
inference(avatar_sat_refutation,[],[s29586]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV739_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n013.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 12:23:52 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 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
% 7.38/1.39 % (1141100)Will run a generic schedule for satisfiability detection.
% 7.38/1.39 % (1141106)% WARNING: option uhcvi not known.
% 7.38/1.39 % (1141106)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4124874675:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.38/1.39 % (1141105)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3749719057_2999 on theBenchmark for (2999ds/0Mi)
% 7.38/1.39 % (1141107)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3518829917:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.38/1.39 % (1141108)dis+10_1_sil=32000:sp=arity:random_seed=794273437:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.38/1.39 % (1141109)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1967205860:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.38/1.39 % (1141110)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2473033762:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.38/1.39 % (1141111)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3363531984:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.38/1.39 % Exception at run slice level
% 7.38/1.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.38/1.39 % (1141119)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4234023820:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.38/1.39 % Exception at run slice level
% 7.38/1.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.38/1.39 % (1141121)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2968319766:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.38/1.39 % (1141108)Instruction limit reached!
% 7.38/1.39 % (1141108)------------------------------
% 7.38/1.39 % (1141108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.38/1.39 % (1141108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.38/1.39 % (1141108)CaDiCaL version: 2.1.3
% 7.38/1.39 % (1141108)Termination reason: Instruction limit
% 7.38/1.39 % (1141108)Termination phase: Saturation
% 7.38/1.39 % (1141108)Time elapsed: 0.057 s
% 7.38/1.39 % (1141108)Peak memory usage: 12 MB
% 7.38/1.39 % (1141108)Instructions burned: 103 (million)
% 7.38/1.39 % (1141109)Instruction limit reached!
% 7.38/1.39 % (1141109)------------------------------
% 7.38/1.39 % (1141109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.38/1.39 % (1141109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.38/1.39 % (1141109)CaDiCaL version: 2.1.3
% 7.38/1.39 % (1141109)Termination reason: Instruction limit
% 7.38/1.39 % (1141109)Termination phase: Saturation
% 7.38/1.39 % (1141109)Time elapsed: 0.060 s
% 7.38/1.39 % (1141109)Peak memory usage: 12 MB
% 7.38/1.39 % (1141109)Instructions burned: 116 (million)
% 7.38/1.39 % (1141110)Instruction limit reached!
% 7.38/1.39 % (1141110)------------------------------
% 7.38/1.39 % (1141110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.38/1.39 % (1141110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.38/1.39 % (1141110)CaDiCaL version: 2.1.3
% 7.38/1.39 % (1141110)Termination reason: Instruction limit
% 7.38/1.39 % (1141110)Termination phase: Saturation
% 7.38/1.39 % (1141110)Time elapsed: 0.072 s
% 7.38/1.39 % (1141110)Peak memory usage: 12 MB
% 7.38/1.39 % (1141110)Instructions burned: 133 (million)
% 7.38/1.39 % (1141123)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=689679326:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 7.38/1.39 % (1141124)ott-21_1_sil=16000:fs=off:random_seed=2472220679:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 7.38/1.39 % (1141111)Instruction limit reached!
% 7.38/1.39 % (1141111)------------------------------
% 7.38/1.39 % (1141111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.38/1.39 % (1141111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.38/1.39 % (1141111)CaDiCaL version: 2.1.3
% 7.38/1.39 % (1141111)Termination reason: Instruction limit
% 7.38/1.39 % (1141111)Termination phase: Saturation
% 7.38/1.39 % (1141111)Time elapsed: 0.088 s
% 7.38/1.39 % (1141111)Peak memory usage: 13 MB
% 7.38/1.39 % (1141111)Instructions burned: 159 (million)
% 7.38/1.39 % (1141125)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=801981311:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 22.00/3.49 % (1141128)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2870285182:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 22.00/3.49 % Exception at run slice level
% 22.00/3.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.00/3.49 % (1141131)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2151228049:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 22.00/3.49 % (1141121)Instruction limit reached!
% 22.00/3.49 % (1141121)------------------------------
% 22.00/3.49 % (1141121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.00/3.49 % (1141121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.00/3.49 % (1141121)CaDiCaL version: 2.1.3
% 22.00/3.49 % (1141121)Termination reason: Instruction limit
% 22.00/3.49 % (1141121)Termination phase: Saturation
% 22.00/3.49 % (1141121)Time elapsed: 0.116 s
% 22.00/3.49 % (1141121)Peak memory usage: 13 MB
% 22.00/3.49 % (1141121)Instructions burned: 132 (million)
% 22.00/3.49 % (1141124)Instruction limit reached!
% 22.00/3.49 % (1141124)------------------------------
% 22.00/3.49 % (1141124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.00/3.49 % (1141124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.00/3.49 % (1141124)CaDiCaL version: 2.1.3
% 22.00/3.49 % (1141124)Termination reason: Instruction limit
% 22.00/3.49 % (1141124)Termination phase: Saturation
% 22.00/3.49 % (1141124)Time elapsed: 0.094 s
% 22.00/3.49 % (1141124)Peak memory usage: 13 MB
% 22.00/3.49 % (1141124)Instructions burned: 180 (million)
% 22.00/3.49 % (1141133)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3634161197:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 22.00/3.49 % Exception at run slice level
% 22.00/3.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.00/3.49 % (1141134)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=4138741105:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 22.00/3.49 % (1141136)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=887145201:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 22.00/3.49 % (1141125)Instruction limit reached!
% 22.00/3.49 % (1141125)------------------------------
% 22.00/3.49 % (1141125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.00/3.49 % (1141125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.00/3.49 % (1141125)CaDiCaL version: 2.1.3
% 22.00/3.49 % (1141125)Termination reason: Instruction limit
% 22.00/3.49 % (1141125)Termination phase: Saturation
% 22.00/3.49 % (1141125)Time elapsed: 0.258 s
% 22.00/3.49 % (1141125)Peak memory usage: 13 MB
% 22.00/3.49 % (1141125)Instructions burned: 477 (million)
% 22.00/3.49 % (1141139)fmb+10_1_sil=64000:random_seed=1836134723:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 22.00/3.49 % (1141139)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 22.00/3.49 % Exception at run slice level
% 22.00/3.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.00/3.49 % (1141141)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3880126704:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 22.00/3.49 % Exception at run slice level
% 22.00/3.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.00/3.49 % (1141123)Instruction limit reached!
% 22.00/3.49 % (1141123)------------------------------
% 22.00/3.49 % (1141123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.00/3.49 % (1141123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.00/3.49 % (1141123)CaDiCaL version: 2.1.3
% 22.00/3.49 % (1141123)Termination reason: Instruction limit
% 22.00/3.49 % (1141123)Termination phase: Saturation
% 22.00/3.49 % (1141123)Time elapsed: 0.341 s
% 22.00/3.49 % (1141123)Peak memory usage: 15 MB
% 22.00/3.49 % (1141123)Instructions burned: 684 (million)
% 22.00/3.49 % (1141143)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2918723593:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 22.00/3.49 % Exception at run slice level
% 99.79/14.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 99.79/14.36 % (1141145)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3672183599:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 99.79/14.36 % (1141146)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3362238178:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 99.79/14.36 % (1141146)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 99.79/14.36 % (1141134)Instruction limit reached!
% 99.79/14.36 % (1141134)------------------------------
% 99.79/14.36 % (1141134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.79/14.36 % (1141134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.79/14.36 % (1141134)CaDiCaL version: 2.1.3
% 99.79/14.36 % (1141134)Termination reason: Instruction limit
% 99.79/14.36 % (1141134)Termination phase: Saturation
% 99.79/14.36 % (1141134)Time elapsed: 0.365 s
% 99.79/14.36 % (1141134)Peak memory usage: 15 MB
% 99.79/14.36 % (1141134)Instructions burned: 693 (million)
% 99.79/14.36 % (1141149)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=6348034:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 99.79/14.36 % Exception at run slice level
% 99.79/14.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 99.79/14.36 % (1141151)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1150110071:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 99.79/14.36 % Exception at run slice level
% 99.79/14.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 99.79/14.36 % (1141153)ott-2_1_sil=16000:newcnf=on:random_seed=475184872:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 99.79/14.36 % (1141136)Instruction limit reached!
% 99.79/14.36 % (1141136)------------------------------
% 99.79/14.36 % (1141136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.79/14.36 % (1141136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.79/14.36 % (1141136)CaDiCaL version: 2.1.3
% 99.79/14.36 % (1141136)Termination reason: Instruction limit
% 99.79/14.36 % (1141136)Termination phase: Saturation
% 99.79/14.36 % (1141136)Time elapsed: 0.499 s
% 99.79/14.36 % (1141136)Peak memory usage: 18 MB
% 99.79/14.36 % (1141136)Instructions burned: 880 (million)
% 99.79/14.36 % (1141155)ott+10_1_sil=32000:tgt=ground:random_seed=338906119:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 99.79/14.36 % (1141131)Instruction limit reached!
% 99.79/14.36 % (1141131)------------------------------
% 99.79/14.36 % (1141131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.79/14.36 % (1141131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.79/14.36 % (1141131)CaDiCaL version: 2.1.3
% 99.79/14.36 % (1141131)Termination reason: Instruction limit
% 99.79/14.36 % (1141131)Termination phase: Saturation
% 99.79/14.36 % (1141131)Time elapsed: 0.678 s
% 99.79/14.36 % (1141131)Peak memory usage: 18 MB
% 99.79/14.36 % (1141131)Instructions burned: 1180 (million)
% 99.79/14.36 % (1141157)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1341045372:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 99.79/14.36 % Exception at run slice level
% 99.79/14.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 99.79/14.36 % (1141159)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3483282603:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 99.79/14.36 % (1141153)Instruction limit reached!
% 99.79/14.36 % (1141153)------------------------------
% 99.79/14.36 % (1141153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.79/14.36 % (1141153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.79/14.36 % (1141153)CaDiCaL version: 2.1.3
% 99.79/14.36 % (1141153)Termination reason: Instruction limit
% 99.79/14.36 % (1141153)Termination phase: Saturation
% 99.79/14.36 % (1141153)Time elapsed: 0.398 s
% 99.79/14.36 % (1141153)Peak memory usage: 13 MB
% 99.79/14.36 % (1141153)Instructions burned: 871 (million)
% 99.79/14.36 % (1141161)dis+21_1_sil=32000:sas=cadical:random_seed=3727652083:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi)
% 99.79/14.36 % (1141146)Instruction limit reached!
% 99.79/14.36 % (1141146)------------------------------
% 99.79/14.36 % (1141146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.11/14.58 % (1141146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.11/14.58 % (1141146)CaDiCaL version: 2.1.3
% 101.11/14.58 % (1141146)Termination reason: Instruction limit
% 101.11/14.58 % (1141146)Termination phase: Saturation
% 101.11/14.58 % (1141146)Time elapsed: 0.680 s
% 101.11/14.58 % (1141146)Peak memory usage: 17 MB
% 101.11/14.58 % (1141146)Instructions burned: 1473 (million)
% 101.11/14.58 % (1141163)ott+11_1_sil=16000:gs=on:random_seed=1513472452:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 101.11/14.58 % (1141163)Instruction limit reached!
% 101.11/14.58 % (1141163)------------------------------
% 101.11/14.58 % (1141163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.11/14.58 % (1141163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.11/14.58 % (1141163)CaDiCaL version: 2.1.3
% 101.11/14.58 % (1141163)Termination reason: Instruction limit
% 101.11/14.58 % (1141163)Termination phase: Saturation
% 101.11/14.58 % (1141163)Time elapsed: 1.107 s
% 101.11/14.58 % (1141163)Peak memory usage: 18 MB
% 101.11/14.58 % (1141163)Instructions burned: 2252 (million)
% 101.11/14.58 % (1141165)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4010133701:fmbsr=1.6:i=67534_2977 on theBenchmark for (2977ds/67534Mi)
% 101.11/14.58 % Exception at run slice level
% 101.11/14.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.11/14.58 % (1141167)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1517112923:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2976 on theBenchmark for (2976ds/4591Mi)
% 101.11/14.58 % (1141159)Instruction limit reached!
% 101.11/14.58 % (1141159)------------------------------
% 101.11/14.58 % (1141159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.11/14.58 % (1141159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.11/14.58 % (1141159)CaDiCaL version: 2.1.3
% 101.11/14.58 % (1141159)Termination reason: Instruction limit
% 101.11/14.58 % (1141159)Termination phase: Saturation
% 101.11/14.58 % (1141159)Time elapsed: 1.880 s
% 101.11/14.58 % (1141159)Peak memory usage: 30 MB
% 101.11/14.58 % (1141159)Instructions burned: 3512 (million)
% 101.11/14.58 % (1141169)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3705092123:i=29340_2972 on theBenchmark for (2972ds/29340Mi)
% 101.11/14.58 % (1141145)Instruction limit reached!
% 101.11/14.58 % (1141145)------------------------------
% 101.11/14.58 % (1141145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.11/14.58 % (1141145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.11/14.58 % (1141145)CaDiCaL version: 2.1.3
% 101.11/14.58 % (1141145)Termination reason: Instruction limit
% 101.11/14.58 % (1141145)Termination phase: Saturation
% 101.11/14.58 % (1141145)Time elapsed: 2.615 s
% 101.11/14.58 % (1141145)Peak memory usage: 32 MB
% 101.11/14.58 % (1141145)Instructions burned: 5133 (million)
% 101.11/14.58 % (1141171)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=615290721:i=5211_2969 on theBenchmark for (2969ds/5211Mi)
% 101.11/14.58 % (1141161)Instruction limit reached!
% 101.11/14.58 % (1141161)------------------------------
% 101.11/14.58 % (1141161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.11/14.58 % (1141161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.11/14.58 % (1141161)CaDiCaL version: 2.1.3
% 101.11/14.58 % (1141161)Termination reason: Instruction limit
% 101.11/14.58 % (1141161)Termination phase: Saturation
% 101.11/14.58 % (1141161)Time elapsed: 2.092 s
% 101.11/14.58 % (1141161)Peak memory usage: 35 MB
% 101.11/14.58 % (1141161)Instructions burned: 3774 (million)
% 101.11/14.58 % (1141173)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3856490345:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi)
% 101.11/14.58 % Exception at run slice level
% 101.11/14.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.11/14.58 % (1141175)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=352628354:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi)
% 101.11/14.58 % Exception at run slice level
% 101.11/14.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.11/14.58 % (1141177)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3581408739:i=14071_2967 on theBenchmark for (2967ds/14071Mi)
% 101.11/14.58 % Exception at run slice level
% 101.11/14.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.11/14.58 % (1141179)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2063465010:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi)
% 101.11/14.58 % (1141155)Instruction limit reached!
% 101.11/14.58 % (1141155)------------------------------
% 101.11/14.58 % (1141155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.11/14.58 % (1141155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.11/14.58 % (1141155)CaDiCaL version: 2.1.3
% 101.11/14.58 % (1141155)Termination reason: Instruction limit
% 101.11/14.58 % (1141155)Termination phase: Saturation
% 101.11/14.58 % (1141155)Time elapsed: 2.766 s
% 101.11/14.58 % (1141155)Peak memory usage: 23 MB
% 101.11/14.58 % (1141155)Instructions burned: 5114 (million)
% 101.11/14.58 % (1141181)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3902465300:i=8173:av=off_2964 on theBenchmark for (2964ds/8173Mi)
% 101.11/14.58 % (1141167)Instruction limit reached!
% 101.11/14.58 % (1141167)------------------------------
% 101.11/14.58 % (1141167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.11/14.58 % (1141167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.11/14.58 % (1141167)CaDiCaL version: 2.1.3
% 101.11/14.58 % (1141167)Termination reason: Instruction limit
% 101.11/14.58 % (1141167)Termination phase: Saturation
% 101.11/14.58 % (1141167)Time elapsed: 2.028 s
% 101.11/14.58 % (1141167)Peak memory usage: 22 MB
% 101.11/14.58 % (1141167)Instructions burned: 4592 (million)
% 101.11/14.58 % (1141183)dis+10_16:1_sil=16000:random_seed=3198167051:i=9155:fsr=off_2956 on theBenchmark for (2956ds/9155Mi)
% 101.11/14.58 % (1141171)Instruction limit reached!
% 101.11/14.58 % (1141171)------------------------------
% 101.11/14.58 % (1141171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.11/14.58 % (1141171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.11/14.58 % (1141171)CaDiCaL version: 2.1.3
% 101.11/14.58 % (1141171)Termination reason: Instruction limit
% 101.11/14.58 % (1141171)Termination phase: Saturation
% 101.11/14.58 % (1141171)Time elapsed: 2.658 s
% 101.11/14.58 % (1141171)Peak memory usage: 39 MB
% 101.11/14.58 % (1141171)Instructions burned: 5211 (million)
% 101.11/14.58 % (1141185)ott-3_8_sil=64000:random_seed=2879890424:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi)
% 101.11/14.58 % (1141181)Instruction limit reached!
% 101.11/14.58 % (1141181)------------------------------
% 101.11/14.58 % (1141181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.11/14.58 % (1141181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.11/14.58 % (1141181)CaDiCaL version: 2.1.3
% 101.11/14.58 % (1141181)Termination reason: Instruction limit
% 101.11/14.58 % (1141181)Termination phase: Saturation
% 101.11/14.58 % (1141181)Time elapsed: 4.355 s
% 101.11/14.58 % (1141181)Peak memory usage: 25 MB
% 101.11/14.58 % (1141181)Instructions burned: 8173 (million)
% 101.11/14.58 % (1141187)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3928361395:fmbsr=2:i=32576_2920 on theBenchmark for (2920ds/32576Mi)
% 101.11/14.58 % Exception at run slice level
% 101.11/14.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.11/14.58 % (1141189)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2917967923:i=11404_2920 on theBenchmark for (2920ds/11404Mi)
% 101.11/14.58 % (1141183)Instruction limit reached!
% 101.11/14.58 % (1141183)------------------------------
% 101.11/14.58 % (1141183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.11/14.58 % (1141183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.11/14.58 % (1141183)CaDiCaL version: 2.1.3
% 101.11/14.58 % (1141183)Termination reason: Instruction limit
% 101.11/14.58 % (1141183)Termination phase: Saturation
% 101.11/14.58 % (1141183)Time elapsed: 4.752 s
% 101.11/14.58 % (1141183)Peak memory usage: 60 MB
% 101.11/14.58 % (1141183)Instructions burned: 9156 (million)
% 101.11/14.58 % (1141191)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1601910521:i=14134_2908 on theBenchmark for (2908ds/14134Mi)
% 101.11/14.58 % (1141179)Instruction limit reached!
% 101.11/14.58 % (1141179)------------------------------
% 101.11/14.58 % (1141179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.11/14.58 % (1141179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.11/14.58 % (1141179)CaDiCaL version: 2.1.3
% 101.11/14.58 % (1141179)Termination reason: Instruction limit
% 101.11/14.58 % (1141179)Termination phase: Saturation
% 101.11/14.58 % (1141179)Time elapsed: 10.853 s
% 101.11/14.58 % (1141179)Peak memory usage: 39 MB
% 101.11/14.58 % (1141179)Instructions burned: 22566 (million)
% 101.11/14.58 % (1141405)dis+33_16_sil=32000:sac=on:random_seed=1138271993:i=15851:nm=0_2858 on theBenchmark for (2858ds/15851Mi)
% 101.11/14.58 % (1141189) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1141100-1141189"...
% 101.11/14.58 % (1141189)...printing done.
% 101.11/14.58 % (1141189)Refutation found. Thanks to Tanya!
% 101.11/14.58 % SZS status Theorem for theBenchmark
% 101.11/14.58 % SZS output start Proof for theBenchmark
% See solution above
% 101.11/14.58 % (1141189)------------------------------
% 101.11/14.58 % (1141189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.11/14.58 % (1141189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.11/14.58 % (1141189)CaDiCaL version: 2.1.3
% 101.11/14.58 % (1141189)Termination reason: Refutation
% 101.11/14.58 % (1141189)Time elapsed: 6.345 s
% 101.11/14.58 % (1141189)Peak memory usage: 86 MB
% 101.11/14.58 % (1141189)Instructions burned: 9989 (million)
% 101.11/14.58 % (1141100)Success in time 14.351 s
% 101.11/14.58 % Vampire exiting
%------------------------------------------------------------------------------