%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW527_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 : n001.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:40:23 PM UTC 2026
% Result : Theorem 95.13s 13.74s
% Output : Refutation 95.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 13
% Syntax : Number of formulae : 95 ( 18 unt; 0 typ; 3 def)
% Number of atoms : 360 ( 137 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 477 ( 212 ~; 215 |; 17 &)
% ( 6 <=>; 27 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 7 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 16 ( 14 usr; 5 prp; 0-5 aty)
% Number of functors : 45 ( 45 usr; 8 con; 0-5 aty)
% Number of variables : 234 ( 0 sgn 220 !; 14 ?; 234 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
a: $tType ).
tff(type_def_6,type,
bool: $tType ).
tff(type_def_7,type,
huffma1450048681e_tree: $tType > $tType ).
tff(type_def_8,type,
nat: $tType ).
tff(type_def_9,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,
combk:
!>[X0: $tType,X1: $tType] : ( X0 > fun(X1,X0) ) ).
tff(func_def_3,type,
combs:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( fun(X0,fun(X1,X2)) * fun(X0,X1) ) > fun(X0,X2) ) ).
tff(func_def_4,type,
huffma675207370phabet:
!>[X0: $tType] : ( huffma1450048681e_tree(X0) > fun(X0,bool) ) ).
tff(func_def_5,type,
huffma1146269203erNode:
!>[X0: $tType] : ( ( nat * huffma1450048681e_tree(X0) * huffma1450048681e_tree(X0) ) > huffma1450048681e_tree(X0) ) ).
tff(func_def_6,type,
huffma2021818691e_Leaf:
!>[X0: $tType] : ( ( nat * X0 ) > huffma1450048681e_tree(X0) ) ).
tff(func_def_7,type,
huffma107959123e_case:
!>[X0: $tType,X1: $tType] : ( ( fun(nat,fun(X0,X1)) * fun(nat,fun(huffma1450048681e_tree(X0),fun(huffma1450048681e_tree(X0),X1))) * huffma1450048681e_tree(X0) ) > X1 ) ).
tff(func_def_8,type,
huffma1280178957ee_rec:
!>[X0: $tType,X1: $tType] : ( ( fun(nat,fun(X0,X1)) * fun(nat,fun(huffma1450048681e_tree(X0),fun(huffma1450048681e_tree(X0),fun(X1,fun(X1,X1))))) * huffma1450048681e_tree(X0) ) > X1 ) ).
tff(func_def_9,type,
inf_inf:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_10,type,
sup_sup:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_11,type,
bot_bot:
!>[X0: $tType] : X0 ).
tff(func_def_12,type,
collect:
!>[X0: $tType] : ( fun(X0,bool) > fun(X0,bool) ) ).
tff(func_def_13,type,
insert:
!>[X0: $tType] : ( ( X0 * fun(X0,bool) ) > fun(X0,bool) ) ).
tff(func_def_14,type,
the_elem:
!>[X0: $tType] : ( fun(X0,bool) > X0 ) ).
tff(func_def_15,type,
aa1:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,X1) * X0 ) > X1 ) ).
tff(func_def_16,type,
fFalse: bool ).
tff(func_def_17,type,
fNot: fun(bool,bool) ).
tff(func_def_18,type,
fTrue: bool ).
tff(func_def_19,type,
fconj: fun(bool,fun(bool,bool)) ).
tff(func_def_20,type,
fdisj: fun(bool,fun(bool,bool)) ).
tff(func_def_21,type,
fequal:
!>[X0: $tType] : fun(X0,fun(X0,bool)) ).
tff(func_def_22,type,
fimplies: fun(bool,fun(bool,bool)) ).
tff(func_def_23,type,
member:
!>[X0: $tType] : fun(X0,fun(fun(X0,bool),bool)) ).
tff(func_def_24,type,
aa: a ).
tff(func_def_25,type,
ta: huffma1450048681e_tree(a) ).
tff(func_def_26,type,
sK2:
!>[X0: $tType] : ( fun(X0,bool) > X0 ) ).
tff(func_def_27,type,
sK3:
!>[X0: $tType] : ( fun(X0,bool) > X0 ) ).
tff(func_def_28,type,
sK4:
!>[X0: $tType] : ( fun(X0,bool) > X0 ) ).
tff(func_def_29,type,
sK5:
!>[X0: $tType] : ( fun(X0,bool) > X0 ) ).
tff(func_def_30,type,
sK6:
!>[X0: $tType] : ( ( fun(X0,bool) * fun(X0,bool) ) > X0 ) ).
tff(func_def_31,type,
sK7:
!>[X0: $tType] : ( ( fun(X0,bool) * fun(X0,bool) ) > X0 ) ).
tff(func_def_32,type,
sK8:
!>[X0: $tType] : ( huffma1450048681e_tree(X0) > X0 ) ).
tff(func_def_33,type,
sK9:
!>[X0: $tType] : ( huffma1450048681e_tree(X0) > nat ) ).
tff(func_def_34,type,
sK10:
!>[X0: $tType] : ( huffma1450048681e_tree(X0) > huffma1450048681e_tree(X0) ) ).
tff(func_def_35,type,
sK11:
!>[X0: $tType] : ( huffma1450048681e_tree(X0) > huffma1450048681e_tree(X0) ) ).
tff(func_def_36,type,
sK12:
!>[X0: $tType] : ( huffma1450048681e_tree(X0) > nat ) ).
tff(func_def_37,type,
sK13:
!>[X0: $tType] : ( huffma1450048681e_tree(X0) > X0 ) ).
tff(func_def_38,type,
sK14:
!>[X0: $tType] : ( fun(X0,bool) > X0 ) ).
tff(func_def_39,type,
sK15:
!>[X0: $tType] : ( ( fun(X0,bool) * fun(X0,bool) * X0 * X0 ) > fun(X0,bool) ) ).
tff(func_def_40,type,
sK16:
!>[X0: $tType,X1: $tType] : ( ( fun(X1,X0) * fun(X1,X0) ) > X1 ) ).
tff(func_def_41,type,
sK17:
!>[X0: $tType] : ( ( fun(X0,bool) * X0 ) > fun(X0,bool) ) ).
tff(func_def_42,type,
sK18:
!>[X0: $tType] : ( ( fun(X0,bool) * X0 ) > fun(X0,bool) ) ).
tff(pred_def_1,type,
bounded_lattice:
!>[X0: $tType] : $o ).
tff(pred_def_2,type,
bot:
!>[X0: $tType] : $o ).
tff(pred_def_3,type,
lattice:
!>[X0: $tType] : $o ).
tff(pred_def_4,type,
semilattice_inf:
!>[X0: $tType] : $o ).
tff(pred_def_5,type,
semilattice_sup:
!>[X0: $tType] : $o ).
tff(pred_def_6,type,
bounded_lattice_bot:
!>[X0: $tType] : $o ).
tff(pred_def_7,type,
huffma1518433673istent:
!>[X0: $tType] : ( huffma1450048681e_tree(X0) > $o ) ).
tff(pred_def_8,type,
pp: bool > $o ).
tff(pred_def_10,type,
sP0:
!>[X0: $tType] : ( ( fun(X0,bool) * fun(X0,bool) * X0 * X0 ) > $o ) ).
tff(pred_def_11,type,
sP1:
!>[X0: $tType] : ( ( X0 * X0 * fun(X0,bool) * fun(X0,bool) ) > $o ) ).
tff(f4,axiom,
! [X0: $tType,X1: huffma1450048681e_tree(X0),X2: huffma1450048681e_tree(X0),X3: nat] :
( huffma1518433673istent(X0,huffma1146269203erNode(X0,X3,X2,X1))
<=> ( huffma1518433673istent(X0,X2)
& huffma1518433673istent(X0,X1)
& ( inf_inf(fun(X0,bool),huffma675207370phabet(X0,X2),huffma675207370phabet(X0,X1)) = bot_bot(fun(X0,bool)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_consistent_Osimps_I2_J) ).
tff(f47,axiom,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool)] :
( ( inf_inf(fun(X0,bool),X2,X1) = bot_bot(fun(X0,bool)) )
<=> ! [X3: X0] :
( pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X3),X2))
=> ! [X4: X0] :
( pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X4),X1))
=> ( X3 != X4 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_disjoint__iff__not__equal) ).
tff(f57,axiom,
! [X0: $tType,X1: huffma1450048681e_tree(X0)] :
( ! [X2: nat,X3: X0] : ( X1 != huffma2021818691e_Leaf(X0,X2,X3) )
=> ~ ! [X2: nat,X4: huffma1450048681e_tree(X0),X5: huffma1450048681e_tree(X0)] : ( X1 != huffma1146269203erNode(X0,X2,X4,X5) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_tree_Oexhaust) ).
tff(f122,axiom,
! [X0: $tType,X1: $tType,X2: $tType,X3: X0,X4: X2,X5: fun(X0,fun(X2,X1))] : ( aa1(X0,X1,combc(X0,X2,X1,X5,X4),X3) = aa1(X2,X1,aa1(X0,fun(X2,X1),X5,X3),X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBC_1_1_U) ).
tff(f138,axiom,
huffma1518433673istent(a,ta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(f139,axiom,
! [X0: nat,X1: a,X2: a] :
( ( ta = huffma2021818691e_Leaf(a,X0,X1) )
=> ( ( aa = X2 )
=> pa ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
tff(f140,axiom,
! [X0: nat,X1: huffma1450048681e_tree(a),X2: huffma1450048681e_tree(a),X3: a] :
( huffma1518433673istent(a,X1)
=> ( huffma1518433673istent(a,X2)
=> ( ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) = bot_bot(fun(a,bool)) )
=> ( pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X1)))
=> ( ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X2)))
=> ( ( ta = huffma1146269203erNode(a,X0,X1,X2) )
=> ( ( aa = X3 )
=> pa ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_2) ).
tff(f141,axiom,
! [X0: nat,X1: huffma1450048681e_tree(a),X2: huffma1450048681e_tree(a),X3: a] :
( huffma1518433673istent(a,X1)
=> ( huffma1518433673istent(a,X2)
=> ( ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) = bot_bot(fun(a,bool)) )
=> ( ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X1)))
=> ( pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X2)))
=> ( ( ta = huffma1146269203erNode(a,X0,X1,X2) )
=> ( ( aa = X3 )
=> pa ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_3) ).
tff(f142,axiom,
! [X0: nat,X1: huffma1450048681e_tree(a),X2: huffma1450048681e_tree(a),X3: a] :
( huffma1518433673istent(a,X1)
=> ( huffma1518433673istent(a,X2)
=> ( ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) = bot_bot(fun(a,bool)) )
=> ( ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X1)))
=> ( ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X2)))
=> ( ( ta = huffma1146269203erNode(a,X0,X1,X2) )
=> ( ( aa = X3 )
=> pa ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_4) ).
tff(f143,conjecture,
pa,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_5) ).
tff(f144,negated_conjecture,
~ pa,
inference(negated_conjecture,[status(cth)],[f143]) ).
tff(f146,plain,
! [X0: $tType,X1: huffma1450048681e_tree(X0)] :
( ! [X2: nat,X3: X0] : ( X1 != huffma2021818691e_Leaf(X0,X2,X3) )
=> ~ ! [X4: nat,X5: huffma1450048681e_tree(X0),X6: huffma1450048681e_tree(X0)] : ( huffma1146269203erNode(X0,X4,X5,X6) != X1 ) ),
inference(rectify,[],[f57]) ).
tff(f147,plain,
~ pa,
inference(flattening,[],[f144]) ).
tff(f175,plain,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool)] :
( ( inf_inf(fun(X0,bool),X2,X1) = bot_bot(fun(X0,bool)) )
<=> ! [X3: X0] :
( ! [X4: X0] :
( ( X3 != X4 )
| ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X4),X1)) )
| ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X3),X2)) ) ),
inference(ennf_transformation,[],[f47]) ).
tff(f180,plain,
! [X0: $tType,X1: huffma1450048681e_tree(X0)] :
( ? [X4: nat,X5: huffma1450048681e_tree(X0),X6: huffma1450048681e_tree(X0)] : ( huffma1146269203erNode(X0,X4,X5,X6) = X1 )
| ? [X2: nat,X3: X0] : ( huffma2021818691e_Leaf(X0,X2,X3) = X1 ) ),
inference(ennf_transformation,[],[f146]) ).
tff(f215,plain,
! [X0: nat,X1: a,X2: a] :
( pa
| ( aa != X2 )
| ( ta != huffma2021818691e_Leaf(a,X0,X1) ) ),
inference(ennf_transformation,[],[f139]) ).
tff(f216,plain,
! [X0: nat,X1: a,X2: a] :
( pa
| ( aa != X2 )
| ( ta != huffma2021818691e_Leaf(a,X0,X1) ) ),
inference(flattening,[],[f215]) ).
tff(f217,plain,
! [X0: nat,X1: huffma1450048681e_tree(a),X2: huffma1450048681e_tree(a),X3: a] :
( pa
| ( aa != X3 )
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X2)))
| ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(ennf_transformation,[],[f140]) ).
tff(f218,plain,
! [X0: nat,X1: huffma1450048681e_tree(a),X2: huffma1450048681e_tree(a),X3: a] :
( pa
| ( aa != X3 )
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X2)))
| ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(flattening,[],[f217]) ).
tff(f219,plain,
! [X0: nat,X1: huffma1450048681e_tree(a),X2: huffma1450048681e_tree(a),X3: a] :
( pa
| ( aa != X3 )
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X2)))
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(ennf_transformation,[],[f141]) ).
tff(f220,plain,
! [X0: nat,X1: huffma1450048681e_tree(a),X2: huffma1450048681e_tree(a),X3: a] :
( pa
| ( aa != X3 )
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X2)))
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(flattening,[],[f219]) ).
tff(f221,plain,
! [X0: nat,X1: huffma1450048681e_tree(a),X2: huffma1450048681e_tree(a),X3: a] :
( pa
| ( aa != X3 )
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X2)))
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(ennf_transformation,[],[f142]) ).
tff(f222,plain,
! [X0: nat,X1: huffma1450048681e_tree(a),X2: huffma1450048681e_tree(a),X3: a] :
( pa
| ( aa != X3 )
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X2)))
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(flattening,[],[f221]) ).
tff(f230,plain,
! [X0: $tType,X1: huffma1450048681e_tree(X0),X2: huffma1450048681e_tree(X0),X3: nat] :
( ( huffma1518433673istent(X0,huffma1146269203erNode(X0,X3,X2,X1))
| ~ huffma1518433673istent(X0,X2)
| ~ huffma1518433673istent(X0,X1)
| ( inf_inf(fun(X0,bool),huffma675207370phabet(X0,X2),huffma675207370phabet(X0,X1)) != bot_bot(fun(X0,bool)) ) )
& ( ( huffma1518433673istent(X0,X2)
& huffma1518433673istent(X0,X1)
& ( inf_inf(fun(X0,bool),huffma675207370phabet(X0,X2),huffma675207370phabet(X0,X1)) = bot_bot(fun(X0,bool)) ) )
| ~ huffma1518433673istent(X0,huffma1146269203erNode(X0,X3,X2,X1)) ) ),
inference(nnf_transformation,[],[f4]) ).
tff(f231,plain,
! [X0: $tType,X1: huffma1450048681e_tree(X0),X2: huffma1450048681e_tree(X0),X3: nat] :
( ( huffma1518433673istent(X0,huffma1146269203erNode(X0,X3,X2,X1))
| ~ huffma1518433673istent(X0,X2)
| ~ huffma1518433673istent(X0,X1)
| ( inf_inf(fun(X0,bool),huffma675207370phabet(X0,X2),huffma675207370phabet(X0,X1)) != bot_bot(fun(X0,bool)) ) )
& ( ( huffma1518433673istent(X0,X2)
& huffma1518433673istent(X0,X1)
& ( inf_inf(fun(X0,bool),huffma675207370phabet(X0,X2),huffma675207370phabet(X0,X1)) = bot_bot(fun(X0,bool)) ) )
| ~ huffma1518433673istent(X0,huffma1146269203erNode(X0,X3,X2,X1)) ) ),
inference(flattening,[],[f230]) ).
tff(f247,plain,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool)] :
( ( ( inf_inf(fun(X0,bool),X2,X1) = bot_bot(fun(X0,bool)) )
| ? [X3: X0] :
( ? [X4: X0] :
( ( X3 = X4 )
& pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X4),X1)) )
& pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X3),X2)) ) )
& ( ! [X3: X0] :
( ! [X4: X0] :
( ( X3 != X4 )
| ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X4),X1)) )
| ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X3),X2)) )
| ( bot_bot(fun(X0,bool)) != inf_inf(fun(X0,bool),X2,X1) ) ) ),
inference(nnf_transformation,[],[f175]) ).
tff(f248,plain,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool)] :
( ( ( inf_inf(fun(X0,bool),X2,X1) = bot_bot(fun(X0,bool)) )
| ? [X3: X0] :
( ? [X4: X0] :
( ( X3 = X4 )
& pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X4),X1)) )
& pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X3),X2)) ) )
& ( ! [X5: X0] :
( ! [X6: X0] :
( ( X5 != X6 )
| ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X6),X1)) )
| ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X5),X2)) )
| ( bot_bot(fun(X0,bool)) != inf_inf(fun(X0,bool),X2,X1) ) ) ),
inference(rectify,[],[f247]) ).
tff(f249,plain,
! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool)] :
( ( ( inf_inf(fun(X0,bool),X2,X1) = bot_bot(fun(X0,bool)) )
| ( ( sK6(X0,X1,X2) = sK7(X0,X1,X2) )
& pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),sK7(X0,X1,X2)),X1))
& pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),sK6(X0,X1,X2)),X2)) ) )
& ( ! [X5: X0] :
( ! [X6: X0] :
( ( X5 != X6 )
| ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X6),X1)) )
| ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X5),X2)) )
| ( bot_bot(fun(X0,bool)) != inf_inf(fun(X0,bool),X2,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X3,sK6(X0,X1,X2)),skolemize(X4,sK7(X0,X1,X2))],[f248]) ).
tff(f251,plain,
! [X0: $tType,X1: huffma1450048681e_tree(X0)] :
( ? [X2: nat,X3: huffma1450048681e_tree(X0),X4: huffma1450048681e_tree(X0)] : ( huffma1146269203erNode(X0,X2,X3,X4) = X1 )
| ? [X5: nat,X6: X0] : ( huffma2021818691e_Leaf(X0,X5,X6) = X1 ) ),
inference(rectify,[],[f180]) ).
tff(f252,plain,
! [X0: $tType,X1: huffma1450048681e_tree(X0)] :
( ( huffma1146269203erNode(X0,sK9(X0,X1),sK10(X0,X1),sK11(X0,X1)) = X1 )
| ( huffma2021818691e_Leaf(X0,sK12(X0,X1),sK13(X0,X1)) = X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11,sK12,sK13]),skolemize(X2,sK9(X0,X1)),skolemize(X3,sK10(X0,X1)),skolemize(X4,sK11(X0,X1)),skolemize(X5,sK12(X0,X1)),skolemize(X6,sK13(X0,X1))],[f251]) ).
tff(f280,plain,
! [X0: $tType,X2: huffma1450048681e_tree(X0),X3: nat,X1: huffma1450048681e_tree(X0)] :
( ~ huffma1518433673istent(X0,huffma1146269203erNode(X0,X3,X2,X1))
| ( inf_inf(fun(X0,bool),huffma675207370phabet(X0,X2),huffma675207370phabet(X0,X1)) = bot_bot(fun(X0,bool)) ) ),
inference(cnf_transformation,[],[f231]) ).
tff(f281,plain,
! [X0: $tType,X2: huffma1450048681e_tree(X0),X3: nat,X1: huffma1450048681e_tree(X0)] :
( ~ huffma1518433673istent(X0,huffma1146269203erNode(X0,X3,X2,X1))
| huffma1518433673istent(X0,X1) ),
inference(cnf_transformation,[],[f231]) ).
tff(f282,plain,
! [X0: $tType,X2: huffma1450048681e_tree(X0),X3: nat,X1: huffma1450048681e_tree(X0)] :
( ~ huffma1518433673istent(X0,huffma1146269203erNode(X0,X3,X2,X1))
| huffma1518433673istent(X0,X2) ),
inference(cnf_transformation,[],[f231]) ).
tff(f335,plain,
! [X0: $tType,X2: fun(X0,bool),X1: fun(X0,bool),X6: X0,X5: X0] :
( ( X5 != X6 )
| ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X6),X1))
| ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X5),X2))
| ( bot_bot(fun(X0,bool)) != inf_inf(fun(X0,bool),X2,X1) ) ),
inference(cnf_transformation,[],[f249]) ).
tff(f348,plain,
! [X0: $tType,X1: huffma1450048681e_tree(X0)] :
( ( huffma1146269203erNode(X0,sK9(X0,X1),sK10(X0,X1),sK11(X0,X1)) = X1 )
| ( huffma2021818691e_Leaf(X0,sK12(X0,X1),sK13(X0,X1)) = X1 ) ),
inference(cnf_transformation,[],[f252]) ).
tff(f443,plain,
! [X1: $tType,X0: $tType,X2: $tType,X3: X0,X4: X2,X5: fun(X0,fun(X2,X1))] : ( aa1(X0,X1,combc(X0,X2,X1,X5,X4),X3) = aa1(X2,X1,aa1(X0,fun(X2,X1),X5,X3),X4) ),
inference(cnf_transformation,[],[f122]) ).
tff(f459,plain,
huffma1518433673istent(a,ta),
inference(cnf_transformation,[],[f138]) ).
tff(f460,plain,
! [X2: a,X0: nat,X1: a] :
( pa
| ( aa != X2 )
| ( ta != huffma2021818691e_Leaf(a,X0,X1) ) ),
inference(cnf_transformation,[],[f216]) ).
tff(f461,plain,
! [X2: huffma1450048681e_tree(a),X3: a,X0: nat,X1: huffma1450048681e_tree(a)] :
( pa
| ( aa != X3 )
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X2)))
| ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(cnf_transformation,[],[f218]) ).
tff(f462,plain,
! [X2: huffma1450048681e_tree(a),X3: a,X0: nat,X1: huffma1450048681e_tree(a)] :
( pa
| ( aa != X3 )
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X2)))
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(cnf_transformation,[],[f220]) ).
tff(f463,plain,
! [X2: huffma1450048681e_tree(a),X3: a,X0: nat,X1: huffma1450048681e_tree(a)] :
( pa
| ( aa != X3 )
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X2)))
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),X3),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(cnf_transformation,[],[f222]) ).
tff(f464,plain,
~ pa,
inference(cnf_transformation,[],[f147]) ).
tff(f521,plain,
! [X0: $tType,X2: fun(X0,bool),X1: fun(X0,bool),X6: X0] :
( ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X6),X1))
| ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X6),X2))
| ( bot_bot(fun(X0,bool)) != inf_inf(fun(X0,bool),X2,X1) ) ),
inference(equality_resolution,[],[f335]) ).
tff(f540,plain,
! [X0: nat,X1: a] :
( pa
| ( ta != huffma2021818691e_Leaf(a,X0,X1) ) ),
inference(equality_resolution,[],[f460]) ).
tff(f541,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( pa
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X2)))
| ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(equality_resolution,[],[f461]) ).
tff(f542,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( pa
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X2)))
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(equality_resolution,[],[f462]) ).
tff(f543,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( pa
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X2)))
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(equality_resolution,[],[f463]) ).
tff(f545,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X2)))
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(forward_subsumption_resolution,[],[f543,f464]) ).
tff(f546,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X2)))
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(forward_subsumption_resolution,[],[f542,f464]) ).
tff(f547,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X2)))
| ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(forward_subsumption_resolution,[],[f541,f464]) ).
tff(f548,plain,
! [X0: nat,X1: a] : ( ta != huffma2021818691e_Leaf(a,X0,X1) ),
inference(forward_subsumption_resolution,[],[f540,f464]) ).
tff(f603,plain,
! [X0: $tType,X2: fun(X0,bool),X1: fun(X0,bool),X6: X0] :
( ~ pp(aa1(X0,bool,combc(X0,fun(X0,bool),bool,member(X0),X1),X6))
| ~ pp(aa1(fun(X0,bool),bool,aa1(X0,fun(fun(X0,bool),bool),member(X0),X6),X2))
| ( bot_bot(fun(X0,bool)) != inf_inf(fun(X0,bool),X2,X1) ) ),
inference(forward_demodulation,[],[f521,f443]) ).
tff(f629,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( pp(aa1(a,bool,combc(a,fun(a,bool),bool,member(a),huffma675207370phabet(a,X2)),aa))
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(forward_demodulation,[],[f545,f443]) ).
tff(f630,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( ~ pp(aa1(a,bool,combc(a,fun(a,bool),bool,member(a),huffma675207370phabet(a,X2)),aa))
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(forward_demodulation,[],[f546,f443]) ).
tff(f631,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( pp(aa1(a,bool,combc(a,fun(a,bool),bool,member(a),huffma675207370phabet(a,X2)),aa))
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| ~ pp(aa1(fun(a,bool),bool,aa1(a,fun(fun(a,bool),bool),member(a),aa),huffma675207370phabet(a,X1)))
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(forward_demodulation,[],[f547,f443]) ).
tff(f669,plain,
! [X0: $tType,X2: fun(X0,bool),X1: fun(X0,bool),X6: X0] :
( ( bot_bot(fun(X0,bool)) != inf_inf(fun(X0,bool),X2,X1) )
| ~ pp(aa1(X0,bool,combc(X0,fun(X0,bool),bool,member(X0),X1),X6))
| ~ pp(aa1(X0,bool,combc(X0,fun(X0,bool),bool,member(X0),X2),X6)) ),
inference(forward_demodulation,[],[f603,f443]) ).
tff(f678,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| pp(aa1(a,bool,combc(a,fun(a,bool),bool,member(a),huffma675207370phabet(a,X2)),aa))
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| pp(aa1(a,bool,combc(a,fun(a,bool),bool,member(a),huffma675207370phabet(a,X1)),aa))
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(forward_demodulation,[],[f629,f443]) ).
tff(f679,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( pp(aa1(a,bool,combc(a,fun(a,bool),bool,member(a),huffma675207370phabet(a,X1)),aa))
| ~ pp(aa1(a,bool,combc(a,fun(a,bool),bool,member(a),huffma675207370phabet(a,X2)),aa))
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(forward_demodulation,[],[f630,f443]) ).
tff(f680,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( ~ pp(aa1(a,bool,combc(a,fun(a,bool),bool,member(a),huffma675207370phabet(a,X1)),aa))
| pp(aa1(a,bool,combc(a,fun(a,bool),bool,member(a),huffma675207370phabet(a,X2)),aa))
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(forward_demodulation,[],[f631,f443]) ).
tff(f698,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| ~ pp(aa1(a,bool,combc(a,fun(a,bool),bool,member(a),huffma675207370phabet(a,X2)),aa))
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(forward_subsumption_resolution,[],[f679,f669]) ).
tff(f699,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( ~ pp(aa1(a,bool,combc(a,fun(a,bool),bool,member(a),huffma675207370phabet(a,X1)),aa))
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(forward_subsumption_resolution,[],[f680,f669]) ).
tff(f707,plain,
! [X2: huffma1450048681e_tree(a),X0: nat,X1: huffma1450048681e_tree(a)] :
( ( inf_inf(fun(a,bool),huffma675207370phabet(a,X1),huffma675207370phabet(a,X2)) != bot_bot(fun(a,bool)) )
| ( ta != huffma1146269203erNode(a,X0,X1,X2) )
| ~ huffma1518433673istent(a,X2)
| ~ huffma1518433673istent(a,X1) ),
inference(global_subsumption,[],[f699,f698,f678]) ).
tff(f1231,plain,
! [X1: $tType,X0: huffma1450048681e_tree(X1)] :
( ~ huffma1518433673istent(X1,X0)
| ( bot_bot(fun(X1,bool)) = inf_inf(fun(X1,bool),huffma675207370phabet(X1,sK10(X1,X0)),huffma675207370phabet(X1,sK11(X1,X0))) )
| ( huffma2021818691e_Leaf(X1,sK12(X1,X0),sK13(X1,X0)) = X0 ) ),
inference(superposition,[],[f280,f348]) ).
tff(f1232,plain,
! [X1: $tType,X0: huffma1450048681e_tree(X1)] :
( huffma1518433673istent(X1,sK11(X1,X0))
| ~ huffma1518433673istent(X1,X0)
| ( huffma2021818691e_Leaf(X1,sK12(X1,X0),sK13(X1,X0)) = X0 ) ),
inference(superposition,[],[f281,f348]) ).
tff(f1233,plain,
! [X1: $tType,X0: huffma1450048681e_tree(X1)] :
( huffma1518433673istent(X1,sK10(X1,X0))
| ~ huffma1518433673istent(X1,X0)
| ( huffma2021818691e_Leaf(X1,sK12(X1,X0),sK13(X1,X0)) = X0 ) ),
inference(superposition,[],[f282,f348]) ).
tff(f19012,plain,
( ( bot_bot(fun(a,bool)) = inf_inf(fun(a,bool),huffma675207370phabet(a,sK10(a,ta)),huffma675207370phabet(a,sK11(a,ta))) )
| ( ta = huffma2021818691e_Leaf(a,sK12(a,ta),sK13(a,ta)) ) ),
inference(resolution,[],[f1231,f459]) ).
tff(f19018,plain,
bot_bot(fun(a,bool)) = inf_inf(fun(a,bool),huffma675207370phabet(a,sK10(a,ta)),huffma675207370phabet(a,sK11(a,ta))),
inference(forward_subsumption_resolution,[],[f19012,f548]) ).
tff(f19025,plain,
! [X0: nat] :
( ( bot_bot(fun(a,bool)) != bot_bot(fun(a,bool)) )
| ( ta != huffma1146269203erNode(a,X0,sK10(a,ta),sK11(a,ta)) )
| ~ huffma1518433673istent(a,sK11(a,ta))
| ~ huffma1518433673istent(a,sK10(a,ta)) ),
inference(superposition,[],[f707,f19018]) ).
tff(f19063,plain,
! [X0: nat] :
( ( ta != huffma1146269203erNode(a,X0,sK10(a,ta),sK11(a,ta)) )
| ~ huffma1518433673istent(a,sK11(a,ta))
| ~ huffma1518433673istent(a,sK10(a,ta)) ),
inference(trivial_inequality_removal,[],[f19025]) ).
tff(f19094,definition,
( spl19_20
<=> huffma1518433673istent(a,sK11(a,ta)) ),
introduced(definition,[new_symbols(definition,[spl19_20])],[avatar_definition]) ).
tff(f19096,plain,
( ~ huffma1518433673istent(a,sK11(a,ta))
| spl19_20 ),
inference(avatar_component_clause,[],[f19094]) ).
tff(f19098,definition,
( spl19_21
<=> huffma1518433673istent(a,sK10(a,ta)) ),
introduced(definition,[new_symbols(definition,[spl19_21])],[avatar_definition]) ).
tff(f19100,plain,
( ~ huffma1518433673istent(a,sK10(a,ta))
| spl19_21 ),
inference(avatar_component_clause,[],[f19098]) ).
tff(f19107,definition,
( spl19_23
<=> ! [X0: nat] : ( ta != huffma1146269203erNode(a,X0,sK10(a,ta),sK11(a,ta)) ) ),
introduced(definition,[new_symbols(definition,[spl19_23])],[avatar_definition]) ).
tff(f19108,plain,
( ! [X0: nat] : ( ta != huffma1146269203erNode(a,X0,sK10(a,ta),sK11(a,ta)) )
| ~ spl19_23 ),
inference(avatar_component_clause,[],[f19107]) ).
tff(f19111,plain,
! [X0: nat] :
( ( ta != huffma1146269203erNode(a,X0,sK10(a,ta),sK11(a,ta)) )
| ~ huffma1518433673istent(a,sK11(a,ta))
| ~ huffma1518433673istent(a,sK10(a,ta)) ),
inference(global_subsumption,[],[f19063]) ).
tff(f19130,plain,
( ~ spl19_21
| ~ spl19_20
| spl19_23 ),
inference(avatar_split_clause,[],[f19111,f19107,f19094,f19098]) ).
tff(f20383,plain,
( ~ huffma1518433673istent(a,ta)
| ( ta = huffma2021818691e_Leaf(a,sK12(a,ta),sK13(a,ta)) )
| spl19_20 ),
inference(resolution,[],[f19096,f1232]) ).
tff(f20384,plain,
( ( ta = huffma2021818691e_Leaf(a,sK12(a,ta),sK13(a,ta)) )
| spl19_20 ),
inference(forward_subsumption_resolution,[],[f20383,f459]) ).
tff(f20385,plain,
( $false
| spl19_20 ),
inference(forward_subsumption_resolution,[],[f20384,f548]) ).
tff(f20386,plain,
spl19_20,
inference(avatar_contradiction_clause,[],[f20385]) ).
tff(f23848,plain,
( ~ huffma1518433673istent(a,ta)
| ( ta = huffma2021818691e_Leaf(a,sK12(a,ta),sK13(a,ta)) )
| spl19_21 ),
inference(resolution,[],[f19100,f1233]) ).
tff(f23849,plain,
( ( ta = huffma2021818691e_Leaf(a,sK12(a,ta),sK13(a,ta)) )
| spl19_21 ),
inference(forward_subsumption_resolution,[],[f23848,f459]) ).
tff(f23850,plain,
( $false
| spl19_21 ),
inference(forward_subsumption_resolution,[],[f23849,f548]) ).
tff(f23851,plain,
spl19_21,
inference(avatar_contradiction_clause,[],[f23850]) ).
tff(f29327,plain,
( ( ta != ta )
| ( ta = huffma2021818691e_Leaf(a,sK12(a,ta),sK13(a,ta)) )
| ~ spl19_23 ),
inference(superposition,[],[f19108,f348]) ).
tff(f29328,plain,
( ( ta = huffma2021818691e_Leaf(a,sK12(a,ta),sK13(a,ta)) )
| ~ spl19_23 ),
inference(trivial_inequality_removal,[],[f29327]) ).
tff(f29329,plain,
( $false
| ~ spl19_23 ),
inference(forward_subsumption_resolution,[],[f29328,f548]) ).
tff(f29330,plain,
~ spl19_23,
inference(avatar_contradiction_clause,[],[f29329]) ).
cnf(s7330,plain,
( ~ spl19_20
| ~ spl19_21
| spl19_23 ),
inference(sat_conversion,[],[f19130]) ).
cnf(s7998,plain,
spl19_20,
inference(sat_conversion,[],[f20386]) ).
cnf(s9940,plain,
spl19_21,
inference(sat_conversion,[],[f23851]) ).
cnf(s12811,plain,
~ spl19_23,
inference(sat_conversion,[],[f29330]) ).
cnf(s12812,plain,
$false,
inference(rat,[],[s7330,s12811,s9940,s7998]) ).
tff(f29331,plain,
$false,
inference(avatar_sat_refutation,[],[s12812]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW527_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.27 % Computer : n001.cluster.edu
% 0.12/0.27 % Model : x86_64 x86_64
% 0.12/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.27 % Memory : 8046.5625MB
% 0.12/0.27 % OS : Linux 6.8.0-71-generic
% 0.12/0.27 % CPULimit : 300
% 0.12/0.27 % WCLimit : 300
% 0.12/0.27 % DateTime : Mon Sep 28 14:23:03 UTC 2026
% 0.26/0.27 % CPUTime :
% 0.26/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.26/0.32 Running first-order model finding
% 0.26/0.32 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
% 13.38/2.28 % (372722)Will run a generic schedule for satisfiability detection.
% 13.38/2.28 % (372730)dis+10_1_sil=32000:sp=arity:random_seed=912083094:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.38/2.28 % (372728)% WARNING: option uhcvi not known.
% 13.38/2.28 % (372727)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=349320998_2999 on theBenchmark for (2999ds/0Mi)
% 13.38/2.28 % (372728)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1928706864:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.38/2.28 % (372729)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3727368547:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.38/2.28 % (372731)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2588409333:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.38/2.28 % (372733)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2823087554:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.38/2.28 % (372732)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2643763753:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.38/2.28 % Exception at run slice level
% 13.38/2.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.38/2.28 % (372730)Instruction limit reached!
% 13.38/2.28 % (372730)------------------------------
% 13.38/2.28 % (372730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.28 % (372730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.28 % (372730)CaDiCaL version: 2.1.3
% 13.38/2.28 % (372730)Termination reason: Instruction limit
% 13.38/2.28 % (372730)Termination phase: Saturation
% 13.38/2.28 % (372730)Time elapsed: 0.052 s
% 13.38/2.28 % (372730)Peak memory usage: 12 MB
% 13.38/2.28 % (372730)Instructions burned: 105 (million)
% 13.38/2.28 % (372741)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3754959923:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.38/2.28 % Exception at run slice level
% 13.38/2.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.38/2.28 % (372743)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=490206331:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 13.38/2.28 % (372744)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=2671265702:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 13.38/2.28 % (372731)Instruction limit reached!
% 13.38/2.28 % (372731)------------------------------
% 13.38/2.28 % (372731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.28 % (372731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.28 % (372731)CaDiCaL version: 2.1.3
% 13.38/2.28 % (372731)Termination reason: Instruction limit
% 13.38/2.28 % (372731)Termination phase: Saturation
% 13.38/2.28 % (372731)Time elapsed: 0.112 s
% 13.38/2.28 % (372731)Peak memory usage: 12 MB
% 13.38/2.28 % (372731)Instructions burned: 116 (million)
% 13.38/2.28 % (372743)Instruction limit reached!
% 13.38/2.28 % (372743)------------------------------
% 13.38/2.28 % (372743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.28 % (372743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.28 % (372743)CaDiCaL version: 2.1.3
% 13.38/2.28 % (372743)Termination reason: Instruction limit
% 13.38/2.28 % (372743)Termination phase: Saturation
% 13.38/2.28 % (372743)Time elapsed: 0.066 s
% 13.38/2.28 % (372743)Peak memory usage: 13 MB
% 13.38/2.28 % (372743)Instructions burned: 131 (million)
% 13.38/2.28 % (372732)Instruction limit reached!
% 13.38/2.28 % (372732)------------------------------
% 13.38/2.28 % (372732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.28 % (372732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.28 % (372732)CaDiCaL version: 2.1.3
% 13.38/2.28 % (372732)Termination reason: Instruction limit
% 13.38/2.28 % (372732)Termination phase: Saturation
% 13.38/2.28 % (372732)Time elapsed: 0.128 s
% 13.38/2.28 % (372732)Peak memory usage: 13 MB
% 13.38/2.28 % (372732)Instructions burned: 132 (million)
% 13.38/2.28 % (372747)ott-21_1_sil=16000:fs=off:random_seed=800076699:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.38/2.28 % (372749)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3583642890:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 36.13/5.43 % (372733)Instruction limit reached!
% 36.13/5.43 % (372733)------------------------------
% 36.13/5.43 % (372733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.13/5.43 % (372733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.13/5.43 % (372733)CaDiCaL version: 2.1.3
% 36.13/5.43 % (372733)Termination reason: Instruction limit
% 36.13/5.43 % (372733)Termination phase: Saturation
% 36.13/5.43 % (372733)Time elapsed: 0.151 s
% 36.13/5.43 % (372733)Peak memory usage: 13 MB
% 36.13/5.43 % (372733)Instructions burned: 160 (million)
% 36.13/5.43 % (372748)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2567753856:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 36.13/5.43 % Exception at run slice level
% 36.13/5.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 36.13/5.43 % (372754)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2980684703:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 36.13/5.43 % Exception at run slice level
% 36.13/5.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 36.13/5.43 % (372752)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4233418903:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 36.13/5.43 % (372756)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=2099365236: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)
% 36.13/5.43 % (372747)Instruction limit reached!
% 36.13/5.43 % (372747)------------------------------
% 36.13/5.43 % (372747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.13/5.43 % (372747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.13/5.43 % (372747)CaDiCaL version: 2.1.3
% 36.13/5.43 % (372747)Termination reason: Instruction limit
% 36.13/5.43 % (372747)Termination phase: Saturation
% 36.13/5.43 % (372747)Time elapsed: 0.133 s
% 36.13/5.43 % (372747)Peak memory usage: 12 MB
% 36.13/5.43 % (372747)Instructions burned: 181 (million)
% 36.13/5.43 % (372759)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2145115161:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 36.13/5.43 % (372756)Instruction limit reached!
% 36.13/5.43 % (372756)------------------------------
% 36.13/5.43 % (372756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.13/5.43 % (372756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.13/5.43 % (372756)CaDiCaL version: 2.1.3
% 36.13/5.43 % (372756)Termination reason: Instruction limit
% 36.13/5.43 % (372756)Termination phase: Saturation
% 36.13/5.43 % (372756)Time elapsed: 0.308 s
% 36.13/5.43 % (372756)Peak memory usage: 15 MB
% 36.13/5.43 % (372756)Instructions burned: 694 (million)
% 36.13/5.43 % (372761)fmb+10_1_sil=64000:random_seed=2881532901:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 36.13/5.43 % (372761)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 36.13/5.43 % Exception at run slice level
% 36.13/5.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 36.13/5.43 % (372763)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=9038297:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 36.13/5.43 % Exception at run slice level
% 36.13/5.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 36.13/5.43 % (372765)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1625682010:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 36.13/5.43 % Exception at run slice level
% 36.13/5.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 36.13/5.43 % (372748)Instruction limit reached!
% 36.13/5.43 % (372748)------------------------------
% 36.13/5.43 % (372748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.13/5.43 % (372748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.13/5.43 % (372748)CaDiCaL version: 2.1.3
% 36.13/5.43 % (372748)Termination reason: Instruction limit
% 36.13/5.43 % (372748)Termination phase: Saturation
% 36.13/5.43 % (372748)Time elapsed: 0.449 s
% 36.13/5.43 % (372748)Peak memory usage: 13 MB
% 36.13/5.43 % (372748)Instructions burned: 477 (million)
% 95.13/13.74 % (372767)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4164111490:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 95.13/13.74 % (372768)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1912800726:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi)
% 95.13/13.74 % (372768)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 95.13/13.74 % (372744)Instruction limit reached!
% 95.13/13.74 % (372744)------------------------------
% 95.13/13.74 % (372744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372744)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372744)Termination reason: Instruction limit
% 95.13/13.74 % (372744)Termination phase: Saturation
% 95.13/13.74 % (372744)Time elapsed: 0.586 s
% 95.13/13.74 % (372744)Peak memory usage: 15 MB
% 95.13/13.74 % (372744)Instructions burned: 685 (million)
% 95.13/13.74 % (372771)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4037705925:i=6324_2992 on theBenchmark for (2992ds/6324Mi)
% 95.13/13.74 % Exception at run slice level
% 95.13/13.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 95.13/13.74 % (372773)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2284110179:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi)
% 95.13/13.74 % Exception at run slice level
% 95.13/13.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 95.13/13.74 % (372775)ott-2_1_sil=16000:newcnf=on:random_seed=2522928594:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi)
% 95.13/13.74 % (372759)Instruction limit reached!
% 95.13/13.74 % (372759)------------------------------
% 95.13/13.74 % (372759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372759)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372759)Termination reason: Instruction limit
% 95.13/13.74 % (372759)Termination phase: Saturation
% 95.13/13.74 % (372759)Time elapsed: 0.776 s
% 95.13/13.74 % (372759)Peak memory usage: 18 MB
% 95.13/13.74 % (372759)Instructions burned: 879 (million)
% 95.13/13.74 % (372777)ott+10_1_sil=32000:tgt=ground:random_seed=4043908412:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 95.13/13.74 % (372752)Instruction limit reached!
% 95.13/13.74 % (372752)------------------------------
% 95.13/13.74 % (372752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372752)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372752)Termination reason: Instruction limit
% 95.13/13.74 % (372752)Termination phase: Saturation
% 95.13/13.74 % (372752)Time elapsed: 1.102 s
% 95.13/13.74 % (372752)Peak memory usage: 19 MB
% 95.13/13.74 % (372752)Instructions burned: 1180 (million)
% 95.13/13.74 % (372779)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1599257381:i=54282_2986 on theBenchmark for (2986ds/54282Mi)
% 95.13/13.74 % Exception at run slice level
% 95.13/13.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 95.13/13.74 % (372781)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3185386461:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi)
% 95.13/13.74 % (372775)Instruction limit reached!
% 95.13/13.74 % (372775)------------------------------
% 95.13/13.74 % (372775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372775)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372775)Termination reason: Instruction limit
% 95.13/13.74 % (372775)Termination phase: Saturation
% 95.13/13.74 % (372775)Time elapsed: 0.700 s
% 95.13/13.74 % (372775)Peak memory usage: 14 MB
% 95.13/13.74 % (372775)Instructions burned: 869 (million)
% 95.13/13.74 % (372783)dis+21_1_sil=32000:sas=cadical:random_seed=3794325074:i=3773:amm=off_2984 on theBenchmark for (2984ds/3773Mi)
% 95.13/13.74 % (372768)Instruction limit reached!
% 95.13/13.74 % (372768)------------------------------
% 95.13/13.74 % (372768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372768)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372768)Termination reason: Instruction limit
% 95.13/13.74 % (372768)Termination phase: Saturation
% 95.13/13.74 % (372768)Time elapsed: 1.273 s
% 95.13/13.74 % (372768)Peak memory usage: 17 MB
% 95.13/13.74 % (372768)Instructions burned: 1473 (million)
% 95.13/13.74 % (372786)ott+11_1_sil=16000:gs=on:random_seed=523990371:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2980 on theBenchmark for (2980ds/2251Mi)
% 95.13/13.74 % (372767)Instruction limit reached!
% 95.13/13.74 % (372767)------------------------------
% 95.13/13.74 % (372767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372767)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372767)Termination reason: Instruction limit
% 95.13/13.74 % (372767)Termination phase: Saturation
% 95.13/13.74 % (372767)Time elapsed: 2.396 s
% 95.13/13.74 % (372767)Peak memory usage: 37 MB
% 95.13/13.74 % (372767)Instructions burned: 5132 (million)
% 95.13/13.74 % (372803)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=771461171:fmbsr=1.6:i=67534_2969 on theBenchmark for (2969ds/67534Mi)
% 95.13/13.74 % Exception at run slice level
% 95.13/13.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 95.13/13.74 % (372805)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3415886470:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2968 on theBenchmark for (2968ds/4591Mi)
% 95.13/13.74 % (372786)Instruction limit reached!
% 95.13/13.74 % (372786)------------------------------
% 95.13/13.74 % (372786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372786)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372786)Termination reason: Instruction limit
% 95.13/13.74 % (372786)Termination phase: Saturation
% 95.13/13.74 % (372786)Time elapsed: 1.951 s
% 95.13/13.74 % (372786)Peak memory usage: 19 MB
% 95.13/13.74 % (372786)Instructions burned: 2251 (million)
% 95.13/13.74 % (372809)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2559324199:i=29340_2960 on theBenchmark for (2960ds/29340Mi)
% 95.13/13.74 % (372781)Instruction limit reached!
% 95.13/13.74 % (372781)------------------------------
% 95.13/13.74 % (372781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372781)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372781)Termination reason: Instruction limit
% 95.13/13.74 % (372781)Termination phase: Saturation
% 95.13/13.74 % (372781)Time elapsed: 3.095 s
% 95.13/13.74 % (372781)Peak memory usage: 31 MB
% 95.13/13.74 % (372781)Instructions burned: 3513 (million)
% 95.13/13.74 % (372811)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4026167423:i=5211_2954 on theBenchmark for (2954ds/5211Mi)
% 95.13/13.74 % (372783)Instruction limit reached!
% 95.13/13.74 % (372783)------------------------------
% 95.13/13.74 % (372783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372783)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372783)Termination reason: Instruction limit
% 95.13/13.74 % (372783)Termination phase: Saturation
% 95.13/13.74 % (372783)Time elapsed: 3.410 s
% 95.13/13.74 % (372783)Peak memory usage: 32 MB
% 95.13/13.74 % (372783)Instructions burned: 3773 (million)
% 95.13/13.74 % (372813)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1917808927:i=5497:nm=2_2950 on theBenchmark for (2950ds/5497Mi)
% 95.13/13.74 % Exception at run slice level
% 95.13/13.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 95.13/13.74 % (372815)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1961707657:fmbsr=2:i=46332_2950 on theBenchmark for (2950ds/46332Mi)
% 95.13/13.74 % Exception at run slice level
% 95.13/13.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 95.13/13.74 % (372817)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3477920928:i=14071_2949 on theBenchmark for (2949ds/14071Mi)
% 95.13/13.74 % Exception at run slice level
% 95.13/13.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 95.13/13.74 % (372819)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1319381077:i=22565:add=on:rawr=on_2949 on theBenchmark for (2949ds/22565Mi)
% 95.13/13.74 % (372805)Instruction limit reached!
% 95.13/13.74 % (372805)------------------------------
% 95.13/13.74 % (372805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372805)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372805)Termination reason: Instruction limit
% 95.13/13.74 % (372805)Termination phase: Saturation
% 95.13/13.74 % (372805)Time elapsed: 1.960 s
% 95.13/13.74 % (372805)Peak memory usage: 37 MB
% 95.13/13.74 % (372805)Instructions burned: 4593 (million)
% 95.13/13.74 % (372821)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2492568492:i=8173:av=off_2948 on theBenchmark for (2948ds/8173Mi)
% 95.13/13.74 % (372777)Instruction limit reached!
% 95.13/13.74 % (372777)------------------------------
% 95.13/13.74 % (372777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372777)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372777)Termination reason: Instruction limit
% 95.13/13.74 % (372777)Termination phase: Saturation
% 95.13/13.74 % (372777)Time elapsed: 4.412 s
% 95.13/13.74 % (372777)Peak memory usage: 23 MB
% 95.13/13.74 % (372777)Instructions burned: 5114 (million)
% 95.13/13.74 % (372823)dis+10_16:1_sil=16000:random_seed=2943046240:i=9155:fsr=off_2944 on theBenchmark for (2944ds/9155Mi)
% 95.13/13.74 % (372821)Instruction limit reached!
% 95.13/13.74 % (372821)------------------------------
% 95.13/13.74 % (372821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372821)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372821)Termination reason: Instruction limit
% 95.13/13.74 % (372821)Termination phase: Saturation
% 95.13/13.74 % (372821)Time elapsed: 3.816 s
% 95.13/13.74 % (372821)Peak memory usage: 51 MB
% 95.13/13.74 % (372821)Instructions burned: 8174 (million)
% 95.13/13.74 % (372829)ott-3_8_sil=64000:random_seed=2478992477:i=20139:bs=on_2910 on theBenchmark for (2910ds/20139Mi)
% 95.13/13.74 % (372811)Instruction limit reached!
% 95.13/13.74 % (372811)------------------------------
% 95.13/13.74 % (372811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.74 % (372811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.74 % (372811)CaDiCaL version: 2.1.3
% 95.13/13.74 % (372811)Termination reason: Instruction limit
% 95.13/13.74 % (372811)Termination phase: Saturation
% 95.13/13.74 % (372811)Time elapsed: 4.655 s
% 95.13/13.74 % (372811)Peak memory usage: 45 MB
% 95.13/13.74 % (372811)Instructions burned: 5211 (million)
% 95.13/13.74 % (372831)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1335451900:fmbsr=2:i=32576_2908 on theBenchmark for (2908ds/32576Mi)
% 95.13/13.74 % Exception at run slice level
% 95.13/13.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 95.13/13.74 % (372833)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=740526808:i=11404_2907 on theBenchmark for (2907ds/11404Mi)
% 95.13/13.74 % (372833) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-372722-372833"...
% 95.13/13.74 % (372833)...printing done.
% 95.13/13.74 % (372833)Refutation found. Thanks to Tanya!
% 95.13/13.74 % SZS status Theorem for theBenchmark
% 95.13/13.74 % SZS output start Proof for theBenchmark
% See solution above
% 95.13/13.75 % (372833)------------------------------
% 95.13/13.75 % (372833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.13/13.75 % (372833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.13/13.75 % (372833)CaDiCaL version: 2.1.3
% 95.13/13.75 % (372833)Termination reason: Refutation
% 95.13/13.75 % (372833)Time elapsed: 4.119 s
% 95.13/13.75 % (372833)Peak memory usage: 50 MB
% 95.13/13.75 % (372833)Instructions burned: 4120 (million)
% 95.13/13.75 % (372722)Success in time 13.415 s
% 95.13/13.75 % Vampire exiting
%------------------------------------------------------------------------------