%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW654_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:31:03 PM UTC 2026
% Result : Theorem 12.98s 2.63s
% Output : Refutation 14.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 46
% Syntax : Number of formulae : 363 ( 29 unt; 0 typ; 32 def)
% Number of atoms : 1312 ( 200 equ)
% Maximal formula atoms : 27 ( 3 avg)
% Number of connectives : 1594 ( 645 ~; 698 |; 132 &)
% ( 34 <=>; 85 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number arithmetic : 308 ( 55 atm; 0 fun; 0 num; 253 var)
% Number of types : 8 ( 6 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 43 ( 40 usr; 33 prp; 0-3 aty)
% Number of functors : 54 ( 54 usr; 42 con; 0-5 aty)
% Number of variables : 543 ( 0 sgn 456 !; 87 ?; 543 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool1: $tType ).
tff(type_def_8,type,
tuple02: $tType ).
tff(type_def_9,type,
color1: $tType ).
tff(type_def_10,type,
tree1: $tType ).
tff(func_def_0,type,
witness1: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool: ty ).
tff(func_def_4,type,
true1: bool1 ).
tff(func_def_5,type,
false1: bool1 ).
tff(func_def_6,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(func_def_7,type,
tuple0: ty ).
tff(func_def_8,type,
tuple03: tuple02 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_10,type,
color: ty ).
tff(func_def_11,type,
red1: color1 ).
tff(func_def_12,type,
black1: color1 ).
tff(func_def_13,type,
match_color1: ( ty * color1 * uni * uni ) > uni ).
tff(func_def_14,type,
tree: ty ).
tff(func_def_15,type,
leaf1: tree1 ).
tff(func_def_16,type,
node1: ( color1 * tree1 * $int * $int * tree1 ) > tree1 ).
tff(func_def_17,type,
match_tree1: ( ty * tree1 * uni * uni ) > uni ).
tff(func_def_18,type,
node_proj_11: tree1 > color1 ).
tff(func_def_19,type,
node_proj_21: tree1 > tree1 ).
tff(func_def_20,type,
node_proj_31: tree1 > $int ).
tff(func_def_21,type,
node_proj_41: tree1 > $int ).
tff(func_def_22,type,
node_proj_51: tree1 > tree1 ).
tff(func_def_29,type,
sK0: tree1 > $int ).
tff(func_def_30,type,
sK1: tree1 > $int ).
tff(func_def_31,type,
sK2: $int ).
tff(func_def_32,type,
sK3: tree1 ).
tff(func_def_33,type,
sK4: $int ).
tff(func_def_34,type,
sK5: tree1 ).
tff(func_def_35,type,
sK6: tree1 ).
tff(func_def_36,type,
sK7: color1 ).
tff(func_def_37,type,
sK8: $int ).
tff(func_def_38,type,
sK9: tree1 ).
tff(func_def_39,type,
sK10: $int ).
tff(func_def_40,type,
sK11: $int ).
tff(func_def_41,type,
sK12: tree1 ).
tff(func_def_42,type,
sK13: color1 ).
tff(func_def_43,type,
sK14: $int ).
tff(func_def_44,type,
sK15: tree1 ).
tff(func_def_45,type,
sK16: $int ).
tff(func_def_46,type,
sK17: color1 ).
tff(func_def_47,type,
sK18: $int ).
tff(func_def_48,type,
sK19: tree1 ).
tff(func_def_49,type,
sK20: tree1 ).
tff(func_def_50,type,
sK21: color1 ).
tff(func_def_51,type,
sK22: tree1 ).
tff(func_def_52,type,
sK23: $int ).
tff(func_def_53,type,
sK24: $int ).
tff(func_def_54,type,
sK25: tree1 ).
tff(func_def_55,type,
sK26: color1 ).
tff(func_def_56,type,
sK27: tree1 ).
tff(func_def_57,type,
sK28: $int ).
tff(func_def_58,type,
sK29: $int ).
tff(func_def_59,type,
sK30: tree1 ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_2,type,
memt1: ( tree1 * $int * $int ) > $o ).
tff(pred_def_4,type,
lt_tree1: ( $int * tree1 ) > $o ).
tff(pred_def_6,type,
gt_tree1: ( $int * tree1 ) > $o ).
tff(pred_def_7,type,
bst1: tree1 > $o ).
tff(pred_def_8,type,
is_not_red1: tree1 > $o ).
tff(pred_def_9,type,
rbtree1: ( $int * tree1 ) > $o ).
tff(pred_def_10,type,
almost_rbtree1: ( $int * tree1 ) > $o ).
tff(f11,axiom,
red1 != black1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',red_Black) ).
tff(f16,axiom,
! [X4: tree1,X1: tree1,X3: $int,X0: color1,X2: $int] : ( leaf1 != node1(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leaf_Node) ).
tff(f30,axiom,
! [X1: $int,X5: color1,X2: $int,X3: tree1,X4: tree1,X0: $int] :
( lt_tree1(X0,X3)
=> ( lt_tree1(X0,X4)
=> ( $less(X1,X0)
=> lt_tree1(X0,node1(X5,X3,X1,X2,X4)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lt_tree_node) ).
tff(f31,axiom,
! [X2: $int,X4: tree1,X1: $int,X3: tree1,X0: $int,X5: color1] :
( gt_tree1(X0,X3)
=> ( gt_tree1(X0,X4)
=> ( $less(X0,X1)
=> gt_tree1(X0,node1(X5,X3,X1,X2,X4)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_tree_node) ).
tff(f32,axiom,
! [X3: tree1,X0: $int,X4: tree1,X5: color1,X2: $int,X1: $int] :
( lt_tree1(X0,node1(X5,X3,X1,X2,X4))
=> $less(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lt_node_lt) ).
tff(f33,axiom,
! [X5: color1,X4: tree1,X1: $int,X3: tree1,X2: $int,X0: $int] :
( gt_tree1(X0,node1(X5,X3,X1,X2,X4))
=> $less(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_node_gt) ).
tff(f34,axiom,
! [X1: $int,X2: $int,X0: $int,X5: color1,X4: tree1,X3: tree1] :
( lt_tree1(X0,node1(X5,X3,X1,X2,X4))
=> lt_tree1(X0,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lt_left) ).
tff(f35,axiom,
! [X2: $int,X1: $int,X0: $int,X4: tree1,X3: tree1,X5: color1] :
( lt_tree1(X0,node1(X5,X3,X1,X2,X4))
=> lt_tree1(X0,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lt_right) ).
tff(f36,axiom,
! [X4: tree1,X5: color1,X0: $int,X3: tree1,X1: $int,X2: $int] :
( gt_tree1(X0,node1(X5,X3,X1,X2,X4))
=> gt_tree1(X0,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_left) ).
tff(f39,axiom,
! [X0: $int,X1: $int] :
( $less(X0,X1)
=> ! [X2: tree1] :
( lt_tree1(X0,X2)
=> lt_tree1(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lt_tree_trans) ).
tff(f41,axiom,
! [X0: $int,X1: $int] :
( $less(X1,X0)
=> ! [X2: tree1] :
( gt_tree1(X0,X2)
=> gt_tree1(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_tree_trans) ).
tff(f42,axiom,
( ! [X3: $int,X4: tree1,X1: tree1,X0: color1,X2: $int] :
( ( bst1(X1)
& gt_tree1(X2,X4)
& bst1(X4)
& lt_tree1(X2,X1) )
<=> bst1(node1(X0,X1,X2,X3,X4)) )
& bst1(leaf1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bst_def) ).
tff(f46,axiom,
! [X0: color1,X3: $int,X2: $int,X4: tree1,X1: color1,X5: tree1] :
( bst1(node1(X0,X4,X2,X3,X5))
=> bst1(node1(X1,X4,X2,X3,X5)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bst_color) ).
tff(f59,conjecture,
! [X0: tree1,X2: $int,X3: tree1,X1: $int] :
( ( bst1(X3)
& bst1(X0)
& gt_tree1(X1,X3)
& lt_tree1(X1,X0) )
=> ! [X7: $int,X4: color1,X8: tree1,X6: $int,X5: tree1] :
( ( X0 = node1(X4,X5,X6,X7,X8) )
=> ( ( ( X8 = leaf1 )
=> ! [X9: color1,X12: $int,X11: $int,X10: tree1,X13: tree1] :
( ( X5 = node1(X9,X10,X11,X12,X13) )
=> ( ( X9 = red1 )
=> ( ( X4 = red1 )
=> bst1(node1(red1,node1(black1,X10,X11,X12,X13),X6,X7,node1(black1,X8,X1,X2,X3))) ) ) ) )
& ! [X12: $int,X10: tree1,X13: tree1,X9: color1,X11: $int] :
( ( X8 = node1(X9,X10,X11,X12,X13) )
=> ( ( ( X9 = black1 )
=> ! [X16: $int,X17: $int,X14: color1,X15: tree1,X18: tree1] :
( ( X5 = node1(X14,X15,X16,X17,X18) )
=> ( ( X14 = red1 )
=> ( ( X4 = red1 )
=> bst1(node1(red1,node1(black1,X15,X16,X17,X18),X6,X7,node1(black1,X8,X1,X2,X3))) ) ) ) )
& ( ( X9 = red1 )
=> ( ! [X17: $int,X14: color1,X18: tree1,X15: tree1,X16: $int] :
( ( X5 = node1(X14,X15,X16,X17,X18) )
=> ( ( ( X14 = black1 )
=> ( ( X4 = red1 )
=> bst1(node1(red1,node1(black1,X5,X6,X7,X10),X11,X12,node1(black1,X13,X1,X2,X3))) ) )
& ( ( X14 = red1 )
=> ( ( X4 = red1 )
=> bst1(node1(red1,node1(black1,X15,X16,X17,X18),X6,X7,node1(black1,X8,X1,X2,X3))) ) ) ) )
& ( ( X5 = leaf1 )
=> ( ( X4 = red1 )
=> bst1(node1(red1,node1(black1,X5,X6,X7,X10),X11,X12,node1(black1,X13,X1,X2,X3))) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_lbalance) ).
tff(f60,negated_conjecture,
~ ! [X0: tree1,X2: $int,X3: tree1,X1: $int] :
( ( bst1(X3)
& bst1(X0)
& gt_tree1(X1,X3)
& lt_tree1(X1,X0) )
=> ! [X7: $int,X4: color1,X8: tree1,X6: $int,X5: tree1] :
( ( X0 = node1(X4,X5,X6,X7,X8) )
=> ( ( ( X8 = leaf1 )
=> ! [X9: color1,X12: $int,X11: $int,X10: tree1,X13: tree1] :
( ( X5 = node1(X9,X10,X11,X12,X13) )
=> ( ( X9 = red1 )
=> ( ( X4 = red1 )
=> bst1(node1(red1,node1(black1,X10,X11,X12,X13),X6,X7,node1(black1,X8,X1,X2,X3))) ) ) ) )
& ! [X12: $int,X10: tree1,X13: tree1,X9: color1,X11: $int] :
( ( X8 = node1(X9,X10,X11,X12,X13) )
=> ( ( ( X9 = black1 )
=> ! [X16: $int,X17: $int,X14: color1,X15: tree1,X18: tree1] :
( ( X5 = node1(X14,X15,X16,X17,X18) )
=> ( ( X14 = red1 )
=> ( ( X4 = red1 )
=> bst1(node1(red1,node1(black1,X15,X16,X17,X18),X6,X7,node1(black1,X8,X1,X2,X3))) ) ) ) )
& ( ( X9 = red1 )
=> ( ! [X17: $int,X14: color1,X18: tree1,X15: tree1,X16: $int] :
( ( X5 = node1(X14,X15,X16,X17,X18) )
=> ( ( ( X14 = black1 )
=> ( ( X4 = red1 )
=> bst1(node1(red1,node1(black1,X5,X6,X7,X10),X11,X12,node1(black1,X13,X1,X2,X3))) ) )
& ( ( X14 = red1 )
=> ( ( X4 = red1 )
=> bst1(node1(red1,node1(black1,X15,X16,X17,X18),X6,X7,node1(black1,X8,X1,X2,X3))) ) ) ) )
& ( ( X5 = leaf1 )
=> ( ( X4 = red1 )
=> bst1(node1(red1,node1(black1,X5,X6,X7,X10),X11,X12,node1(black1,X13,X1,X2,X3))) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f59]) ).
tff(f82,plain,
~ ! [X1: $int,X3: $int,X2: tree1,X0: tree1] :
( ( bst1(X0)
& lt_tree1(X3,X0)
& bst1(X2)
& gt_tree1(X3,X2) )
=> ! [X7: $int,X4: $int,X8: tree1,X5: color1,X6: tree1] :
( ( node1(X5,X8,X7,X4,X6) = X0 )
=> ( ( ( leaf1 = X6 )
=> ! [X11: $int,X13: tree1,X10: $int,X9: color1,X12: tree1] :
( ( node1(X9,X12,X11,X10,X13) = X8 )
=> ( ( X9 = red1 )
=> ( ( red1 = X5 )
=> bst1(node1(red1,node1(black1,X12,X11,X10,X13),X7,X4,node1(black1,X6,X3,X1,X2))) ) ) ) )
& ! [X17: color1,X14: $int,X18: $int,X16: tree1,X15: tree1] :
( ( node1(X17,X15,X18,X14,X16) = X6 )
=> ( ( ( red1 = X17 )
=> ( ( ( leaf1 = X8 )
=> ( ( red1 = X5 )
=> bst1(node1(red1,node1(black1,X8,X7,X4,X15),X18,X14,node1(black1,X16,X3,X1,X2))) ) )
& ! [X27: tree1,X26: tree1,X24: $int,X25: color1,X28: $int] :
( ( node1(X25,X27,X28,X24,X26) = X8 )
=> ( ( ( black1 = X25 )
=> ( ( red1 = X5 )
=> bst1(node1(red1,node1(black1,X8,X7,X4,X15),X18,X14,node1(black1,X16,X3,X1,X2))) ) )
& ( ( red1 = X25 )
=> ( ( red1 = X5 )
=> bst1(node1(red1,node1(black1,X27,X28,X24,X26),X7,X4,node1(black1,X6,X3,X1,X2))) ) ) ) ) ) )
& ( ( black1 = X17 )
=> ! [X22: tree1,X23: tree1,X21: color1,X20: $int,X19: $int] :
( ( node1(X21,X22,X19,X20,X23) = X8 )
=> ( ( red1 = X21 )
=> ( ( red1 = X5 )
=> bst1(node1(red1,node1(black1,X22,X19,X20,X23),X7,X4,node1(black1,X6,X3,X1,X2))) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f60]) ).
tff(f83,plain,
! [X1: $int,X4: $int,X3: color1,X2: tree1,X5: $int,X0: tree1] :
( lt_tree1(X1,node1(X3,X0,X5,X4,X2))
=> $less(X5,X1) ),
inference(rectify,[],[f32]) ).
tff(f84,plain,
! [X3: tree1,X1: $int,X5: color1,X2: $int,X4: tree1,X0: $int] :
( lt_tree1(X2,node1(X5,X4,X1,X0,X3))
=> lt_tree1(X2,X3) ),
inference(rectify,[],[f35]) ).
tff(f85,plain,
! [X0: $int,X2: $int,X1: $int,X4: tree1,X3: color1,X5: tree1] :
( lt_tree1(X2,node1(X3,X5,X0,X1,X4))
=> lt_tree1(X2,X5) ),
inference(rectify,[],[f34]) ).
tff(f86,plain,
! [X3: tree1,X2: $int,X0: $int,X4: tree1,X1: color1,X5: $int] :
( lt_tree1(X5,X3)
=> ( lt_tree1(X5,X4)
=> ( $less(X0,X5)
=> lt_tree1(X5,node1(X1,X3,X0,X2,X4)) ) ) ),
inference(rectify,[],[f30]) ).
tff(f88,plain,
! [X4: $int,X0: tree1,X5: $int,X3: tree1,X2: $int,X1: color1] :
( gt_tree1(X2,node1(X1,X3,X4,X5,X0))
=> gt_tree1(X2,X3) ),
inference(rectify,[],[f36]) ).
tff(f89,plain,
! [X1: tree1,X3: tree1,X2: $int,X5: $int,X0: color1,X4: $int] :
( gt_tree1(X5,node1(X0,X3,X2,X4,X1))
=> $less(X5,X2) ),
inference(rectify,[],[f33]) ).
tff(f90,plain,
! [X0: $int,X3: tree1,X2: $int,X5: color1,X4: $int,X1: tree1] :
( gt_tree1(X4,X3)
=> ( gt_tree1(X4,X1)
=> ( $less(X4,X2)
=> gt_tree1(X4,node1(X5,X3,X2,X0,X1)) ) ) ),
inference(rectify,[],[f31]) ).
tff(f93,plain,
! [X1: $int,X5: tree1,X3: tree1,X0: color1,X2: $int,X4: color1] :
( bst1(node1(X0,X3,X2,X1,X5))
=> bst1(node1(X4,X3,X2,X1,X5)) ),
inference(rectify,[],[f46]) ).
tff(f96,plain,
( ! [X1: tree1,X0: $int,X4: $int,X3: color1,X2: tree1] :
( bst1(node1(X3,X2,X4,X0,X1))
<=> ( bst1(X2)
& gt_tree1(X4,X1)
& bst1(X1)
& lt_tree1(X4,X2) ) )
& bst1(leaf1) ),
inference(rectify,[],[f42]) ).
tff(f97,plain,
! [X1: tree1,X4: $int,X3: color1,X0: tree1,X2: $int] : ( leaf1 != node1(X3,X1,X4,X2,X0) ),
inference(rectify,[],[f16]) ).
tff(f101,plain,
! [X3: color1,X0: tree1,X2: tree1,X5: $int,X4: $int,X1: $int] :
( ~ lt_tree1(X1,node1(X3,X0,X5,X4,X2))
| $less(X5,X1) ),
inference(ennf_transformation,[],[f83]) ).
tff(f102,plain,
! [X0: $int,X1: $int] :
( ~ $less(X0,X1)
| ! [X2: tree1] :
( lt_tree1(X1,X2)
| ~ lt_tree1(X0,X2) ) ),
inference(ennf_transformation,[],[f39]) ).
tff(f105,plain,
! [X5: tree1,X2: $int,X3: tree1,X0: color1,X1: $int,X4: color1] :
( ~ bst1(node1(X0,X3,X2,X1,X5))
| bst1(node1(X4,X3,X2,X1,X5)) ),
inference(ennf_transformation,[],[f93]) ).
tff(f109,plain,
! [X3: tree1,X2: $int,X5: color1,X0: $int,X4: tree1,X1: $int] :
( ~ lt_tree1(X2,node1(X5,X4,X1,X0,X3))
| lt_tree1(X2,X3) ),
inference(ennf_transformation,[],[f84]) ).
tff(f110,plain,
? [X1: $int,X3: $int,X2: tree1,X0: tree1] :
( ? [X7: $int,X4: $int,X8: tree1,X5: color1,X6: tree1] :
( ( ( ? [X11: $int,X13: tree1,X10: $int,X9: color1,X12: tree1] :
( ~ bst1(node1(red1,node1(black1,X12,X11,X10,X13),X7,X4,node1(black1,X6,X3,X1,X2)))
& ( red1 = X5 )
& ( X9 = red1 )
& ( node1(X9,X12,X11,X10,X13) = X8 ) )
& ( leaf1 = X6 ) )
| ? [X17: color1,X14: $int,X18: $int,X16: tree1,X15: tree1] :
( ( ( ( ( ~ bst1(node1(red1,node1(black1,X8,X7,X4,X15),X18,X14,node1(black1,X16,X3,X1,X2)))
& ( red1 = X5 )
& ( leaf1 = X8 ) )
| ? [X27: tree1,X26: tree1,X24: $int,X25: color1,X28: $int] :
( ( ( ~ bst1(node1(red1,node1(black1,X8,X7,X4,X15),X18,X14,node1(black1,X16,X3,X1,X2)))
& ( red1 = X5 )
& ( black1 = X25 ) )
| ( ~ bst1(node1(red1,node1(black1,X27,X28,X24,X26),X7,X4,node1(black1,X6,X3,X1,X2)))
& ( red1 = X5 )
& ( red1 = X25 ) ) )
& ( node1(X25,X27,X28,X24,X26) = X8 ) ) )
& ( red1 = X17 ) )
| ( ? [X22: tree1,X23: tree1,X21: color1,X20: $int,X19: $int] :
( ~ bst1(node1(red1,node1(black1,X22,X19,X20,X23),X7,X4,node1(black1,X6,X3,X1,X2)))
& ( red1 = X5 )
& ( red1 = X21 )
& ( node1(X21,X22,X19,X20,X23) = X8 ) )
& ( black1 = X17 ) ) )
& ( node1(X17,X15,X18,X14,X16) = X6 ) ) )
& ( node1(X5,X8,X7,X4,X6) = X0 ) )
& bst1(X0)
& lt_tree1(X3,X0)
& bst1(X2)
& gt_tree1(X3,X2) ),
inference(ennf_transformation,[],[f82]) ).
tff(f111,plain,
? [X3: $int,X0: tree1,X1: $int,X2: tree1] :
( bst1(X2)
& gt_tree1(X3,X2)
& ? [X8: tree1,X5: color1,X4: $int,X6: tree1,X7: $int] :
( ( node1(X5,X8,X7,X4,X6) = X0 )
& ( ( ? [X11: $int,X12: tree1,X9: color1,X10: $int,X13: tree1] :
( ( node1(X9,X12,X11,X10,X13) = X8 )
& ( red1 = X5 )
& ( X9 = red1 )
& ~ bst1(node1(red1,node1(black1,X12,X11,X10,X13),X7,X4,node1(black1,X6,X3,X1,X2))) )
& ( leaf1 = X6 ) )
| ? [X14: $int,X17: color1,X18: $int,X15: tree1,X16: tree1] :
( ( ( ( black1 = X17 )
& ? [X21: color1,X22: tree1,X19: $int,X20: $int,X23: tree1] :
( ( red1 = X5 )
& ( red1 = X21 )
& ~ bst1(node1(red1,node1(black1,X22,X19,X20,X23),X7,X4,node1(black1,X6,X3,X1,X2)))
& ( node1(X21,X22,X19,X20,X23) = X8 ) ) )
| ( ( ? [X25: color1,X26: tree1,X28: $int,X24: $int,X27: tree1] :
( ( node1(X25,X27,X28,X24,X26) = X8 )
& ( ( ~ bst1(node1(red1,node1(black1,X27,X28,X24,X26),X7,X4,node1(black1,X6,X3,X1,X2)))
& ( red1 = X25 )
& ( red1 = X5 ) )
| ( ( red1 = X5 )
& ( black1 = X25 )
& ~ bst1(node1(red1,node1(black1,X8,X7,X4,X15),X18,X14,node1(black1,X16,X3,X1,X2))) ) ) )
| ( ~ bst1(node1(red1,node1(black1,X8,X7,X4,X15),X18,X14,node1(black1,X16,X3,X1,X2)))
& ( red1 = X5 )
& ( leaf1 = X8 ) ) )
& ( red1 = X17 ) ) )
& ( node1(X17,X15,X18,X14,X16) = X6 ) ) ) )
& bst1(X0)
& lt_tree1(X3,X0) ),
inference(flattening,[],[f110]) ).
tff(f112,plain,
! [X0: $int,X3: tree1,X2: $int,X5: color1,X4: $int,X1: tree1] :
( gt_tree1(X4,node1(X5,X3,X2,X0,X1))
| ~ $less(X4,X2)
| ~ gt_tree1(X4,X1)
| ~ gt_tree1(X4,X3) ),
inference(ennf_transformation,[],[f90]) ).
tff(f113,plain,
! [X3: tree1,X5: color1,X2: $int,X1: tree1,X0: $int,X4: $int] :
( ~ gt_tree1(X4,X3)
| ~ gt_tree1(X4,X1)
| ~ $less(X4,X2)
| gt_tree1(X4,node1(X5,X3,X2,X0,X1)) ),
inference(flattening,[],[f112]) ).
tff(f114,plain,
! [X0: $int,X3: color1,X1: $int,X4: tree1,X5: tree1,X2: $int] :
( lt_tree1(X2,X5)
| ~ lt_tree1(X2,node1(X3,X5,X0,X1,X4)) ),
inference(ennf_transformation,[],[f85]) ).
tff(f115,plain,
! [X3: tree1,X2: $int,X0: $int,X4: tree1,X1: color1,X5: $int] :
( lt_tree1(X5,node1(X1,X3,X0,X2,X4))
| ~ $less(X0,X5)
| ~ lt_tree1(X5,X4)
| ~ lt_tree1(X5,X3) ),
inference(ennf_transformation,[],[f86]) ).
tff(f116,plain,
! [X4: tree1,X1: color1,X5: $int,X3: tree1,X0: $int,X2: $int] :
( ~ lt_tree1(X5,X3)
| ~ $less(X0,X5)
| lt_tree1(X5,node1(X1,X3,X0,X2,X4))
| ~ lt_tree1(X5,X4) ),
inference(flattening,[],[f115]) ).
tff(f118,plain,
! [X2: $int,X5: $int,X0: color1,X4: $int,X1: tree1,X3: tree1] :
( $less(X5,X2)
| ~ gt_tree1(X5,node1(X0,X3,X2,X4,X1)) ),
inference(ennf_transformation,[],[f89]) ).
tff(f122,plain,
! [X1: $int,X0: $int] :
( ! [X2: tree1] :
( gt_tree1(X1,X2)
| ~ gt_tree1(X0,X2) )
| ~ $less(X1,X0) ),
inference(ennf_transformation,[],[f41]) ).
tff(f123,plain,
! [X4: $int,X0: tree1,X1: color1,X2: $int,X3: tree1,X5: $int] :
( ~ gt_tree1(X2,node1(X1,X3,X4,X5,X0))
| gt_tree1(X2,X3) ),
inference(ennf_transformation,[],[f88]) ).
tff(f126,plain,
! [X0: $int,X1: $int] :
( ! [X2: tree1] :
( gt_tree1(X0,X2)
| ~ gt_tree1(X1,X2) )
| ~ $less(X0,X1) ),
inference(rectify,[],[f122]) ).
tff(f127,plain,
( ! [X1: tree1,X0: $int,X4: $int,X3: color1,X2: tree1] :
( ( bst1(node1(X3,X2,X4,X0,X1))
| ~ bst1(X2)
| ~ gt_tree1(X4,X1)
| ~ bst1(X1)
| ~ lt_tree1(X4,X2) )
& ( ( bst1(X2)
& gt_tree1(X4,X1)
& bst1(X1)
& lt_tree1(X4,X2) )
| ~ bst1(node1(X3,X2,X4,X0,X1)) ) )
& bst1(leaf1) ),
inference(nnf_transformation,[],[f96]) ).
tff(f128,plain,
( ! [X1: tree1,X0: $int,X4: $int,X3: color1,X2: tree1] :
( ( bst1(node1(X3,X2,X4,X0,X1))
| ~ bst1(X2)
| ~ gt_tree1(X4,X1)
| ~ bst1(X1)
| ~ lt_tree1(X4,X2) )
& ( ( bst1(X2)
& gt_tree1(X4,X1)
& bst1(X1)
& lt_tree1(X4,X2) )
| ~ bst1(node1(X3,X2,X4,X0,X1)) ) )
& bst1(leaf1) ),
inference(flattening,[],[f127]) ).
tff(f129,plain,
( ! [X0: tree1,X1: $int,X2: $int,X3: color1,X4: tree1] :
( ( bst1(node1(X3,X4,X2,X1,X0))
| ~ bst1(X4)
| ~ gt_tree1(X2,X0)
| ~ bst1(X0)
| ~ lt_tree1(X2,X4) )
& ( ( bst1(X4)
& gt_tree1(X2,X0)
& bst1(X0)
& lt_tree1(X2,X4) )
| ~ bst1(node1(X3,X4,X2,X1,X0)) ) )
& bst1(leaf1) ),
inference(rectify,[],[f128]) ).
tff(f130,plain,
! [X0: $int,X1: tree1,X2: color1,X3: $int,X4: tree1,X5: $int] :
( ~ gt_tree1(X3,node1(X2,X4,X0,X5,X1))
| gt_tree1(X3,X4) ),
inference(rectify,[],[f123]) ).
tff(f135,plain,
! [X0: $int,X1: color1,X2: $int,X3: tree1,X4: tree1,X5: $int] :
( lt_tree1(X5,X4)
| ~ lt_tree1(X5,node1(X1,X4,X0,X2,X3)) ),
inference(rectify,[],[f114]) ).
tff(f137,plain,
! [X0: tree1,X1: color1,X2: $int,X3: tree1,X4: $int,X5: $int] :
( ~ lt_tree1(X2,X3)
| ~ $less(X4,X2)
| lt_tree1(X2,node1(X1,X3,X4,X5,X0))
| ~ lt_tree1(X2,X0) ),
inference(rectify,[],[f116]) ).
tff(f138,plain,
! [X0: tree1,X1: $int,X2: tree1,X3: color1,X4: $int,X5: color1] :
( ~ bst1(node1(X3,X2,X1,X4,X0))
| bst1(node1(X5,X2,X1,X4,X0)) ),
inference(rectify,[],[f105]) ).
tff(f141,plain,
! [X0: tree1,X1: $int,X2: color1,X3: $int,X4: tree1,X5: $int] :
( ~ lt_tree1(X1,node1(X2,X4,X5,X3,X0))
| lt_tree1(X1,X0) ),
inference(rectify,[],[f109]) ).
tff(f142,plain,
? [X0: $int,X1: tree1,X2: $int,X3: tree1] :
( bst1(X3)
& gt_tree1(X0,X3)
& ? [X4: tree1,X5: color1,X6: $int,X7: tree1,X8: $int] :
( ( node1(X5,X4,X8,X6,X7) = X1 )
& ( ( ? [X9: $int,X10: tree1,X11: color1,X12: $int,X13: tree1] :
( ( node1(X11,X10,X9,X12,X13) = X4 )
& ( red1 = X5 )
& ( red1 = X11 )
& ~ bst1(node1(red1,node1(black1,X10,X9,X12,X13),X8,X6,node1(black1,X7,X0,X2,X3))) )
& ( leaf1 = X7 ) )
| ? [X14: $int,X15: color1,X16: $int,X17: tree1,X18: tree1] :
( ( ( ( black1 = X15 )
& ? [X19: color1,X20: tree1,X21: $int,X22: $int,X23: tree1] :
( ( red1 = X5 )
& ( red1 = X19 )
& ~ bst1(node1(red1,node1(black1,X20,X21,X22,X23),X8,X6,node1(black1,X7,X0,X2,X3)))
& ( node1(X19,X20,X21,X22,X23) = X4 ) ) )
| ( ( ? [X24: color1,X25: tree1,X26: $int,X27: $int,X28: tree1] :
( ( node1(X24,X28,X26,X27,X25) = X4 )
& ( ( ~ bst1(node1(red1,node1(black1,X28,X26,X27,X25),X8,X6,node1(black1,X7,X0,X2,X3)))
& ( red1 = X24 )
& ( red1 = X5 ) )
| ( ( red1 = X5 )
& ( black1 = X24 )
& ~ bst1(node1(red1,node1(black1,X4,X8,X6,X17),X16,X14,node1(black1,X18,X0,X2,X3))) ) ) )
| ( ~ bst1(node1(red1,node1(black1,X4,X8,X6,X17),X16,X14,node1(black1,X18,X0,X2,X3)))
& ( red1 = X5 )
& ( leaf1 = X4 ) ) )
& ( red1 = X15 ) ) )
& ( node1(X15,X17,X16,X14,X18) = X7 ) ) ) )
& bst1(X1)
& lt_tree1(X0,X1) ),
inference(rectify,[],[f111]) ).
tff(f143,plain,
( bst1(sK5)
& gt_tree1(sK2,sK5)
& ( sK3 = node1(sK7,sK6,sK10,sK8,sK9) )
& ( ( ( node1(sK13,sK12,sK11,sK14,sK15) = sK6 )
& ( red1 = sK7 )
& ( red1 = sK13 )
& ~ bst1(node1(red1,node1(black1,sK12,sK11,sK14,sK15),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5)))
& ( leaf1 = sK9 ) )
| ( ( ( ( black1 = sK17 )
& ( red1 = sK7 )
& ( red1 = sK21 )
& ~ bst1(node1(red1,node1(black1,sK22,sK23,sK24,sK25),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5)))
& ( sK6 = node1(sK21,sK22,sK23,sK24,sK25) ) )
| ( ( ( ( sK6 = node1(sK26,sK30,sK28,sK29,sK27) )
& ( ( ~ bst1(node1(red1,node1(black1,sK30,sK28,sK29,sK27),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5)))
& ( red1 = sK26 )
& ( red1 = sK7 ) )
| ( ( red1 = sK7 )
& ( black1 = sK26 )
& ~ bst1(node1(red1,node1(black1,sK6,sK10,sK8,sK19),sK18,sK16,node1(black1,sK20,sK2,sK4,sK5))) ) ) )
| ( ~ bst1(node1(red1,node1(black1,sK6,sK10,sK8,sK19),sK18,sK16,node1(black1,sK20,sK2,sK4,sK5)))
& ( red1 = sK7 )
& ( leaf1 = sK6 ) ) )
& ( red1 = sK17 ) ) )
& ( sK9 = node1(sK17,sK19,sK18,sK16,sK20) ) ) )
& bst1(sK3)
& lt_tree1(sK2,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK6),skolemize(X5,sK7),skolemize(X6,sK8),skolemize(X7,sK9),skolemize(X8,sK10),skolemize(X9,sK11),skolemize(X10,sK12),skolemize(X11,sK13),skolemize(X12,sK14),skolemize(X13,sK15),skolemize(X14,sK16),skolemize(X15,sK17),skolemize(X16,sK18),skolemize(X17,sK19),skolemize(X18,sK20),skolemize(X19,sK21),skolemize(X20,sK22),skolemize(X21,sK23),skolemize(X22,sK24),skolemize(X23,sK25),skolemize(X24,sK26),skolemize(X25,sK27),skolemize(X26,sK28),skolemize(X27,sK29),skolemize(X28,sK30)],[f142]) ).
tff(f144,plain,
! [X0: tree1,X1: $int,X2: color1,X3: tree1,X4: $int] : ( leaf1 != node1(X2,X0,X1,X4,X3) ),
inference(rectify,[],[f97]) ).
tff(f145,plain,
! [X0: color1,X1: tree1,X2: tree1,X3: $int,X4: $int,X5: $int] :
( ~ lt_tree1(X5,node1(X0,X1,X3,X4,X2))
| $less(X3,X5) ),
inference(rectify,[],[f101]) ).
tff(f147,plain,
! [X0: tree1,X1: color1,X2: $int,X3: tree1,X4: $int,X5: $int] :
( ~ gt_tree1(X5,X0)
| ~ gt_tree1(X5,X3)
| ~ $less(X5,X2)
| gt_tree1(X5,node1(X1,X0,X2,X4,X3)) ),
inference(rectify,[],[f113]) ).
tff(f148,plain,
! [X0: $int,X1: $int,X2: color1,X3: $int,X4: tree1,X5: tree1] :
( $less(X1,X0)
| ~ gt_tree1(X1,node1(X2,X5,X0,X3,X4)) ),
inference(rectify,[],[f118]) ).
tff(f153,plain,
! [X2: tree1,X0: $int,X1: $int] :
( ~ gt_tree1(X1,X2)
| gt_tree1(X0,X2)
| ~ $less(X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
tff(f155,plain,
! [X2: tree1,X0: $int,X1: $int] :
( ~ $less(X0,X1)
| ~ lt_tree1(X0,X2)
| lt_tree1(X1,X2) ),
inference(cnf_transformation,[],[f102]) ).
tff(f157,plain,
! [X2: $int,X3: color1,X0: tree1,X1: $int,X4: tree1] :
( ~ bst1(node1(X3,X4,X2,X1,X0))
| lt_tree1(X2,X4) ),
inference(cnf_transformation,[],[f129]) ).
tff(f158,plain,
! [X2: $int,X3: color1,X0: tree1,X1: $int,X4: tree1] :
( ~ bst1(node1(X3,X4,X2,X1,X0))
| bst1(X0) ),
inference(cnf_transformation,[],[f129]) ).
tff(f159,plain,
! [X2: $int,X3: color1,X0: tree1,X1: $int,X4: tree1] :
( ~ bst1(node1(X3,X4,X2,X1,X0))
| gt_tree1(X2,X0) ),
inference(cnf_transformation,[],[f129]) ).
tff(f160,plain,
! [X2: $int,X3: color1,X0: tree1,X1: $int,X4: tree1] :
( ~ bst1(node1(X3,X4,X2,X1,X0))
| bst1(X4) ),
inference(cnf_transformation,[],[f129]) ).
tff(f161,plain,
! [X2: $int,X3: color1,X0: tree1,X1: $int,X4: tree1] :
( bst1(node1(X3,X4,X2,X1,X0))
| ~ gt_tree1(X2,X0)
| ~ lt_tree1(X2,X4)
| ~ bst1(X4)
| ~ bst1(X0) ),
inference(cnf_transformation,[],[f129]) ).
tff(f162,plain,
! [X2: color1,X3: $int,X0: $int,X1: tree1,X4: tree1,X5: $int] :
( ~ gt_tree1(X3,node1(X2,X4,X0,X5,X1))
| gt_tree1(X3,X4) ),
inference(cnf_transformation,[],[f130]) ).
tff(f166,plain,
! [X2: $int,X3: tree1,X0: $int,X1: color1,X4: tree1,X5: $int] :
( ~ lt_tree1(X5,node1(X1,X4,X0,X2,X3))
| lt_tree1(X5,X4) ),
inference(cnf_transformation,[],[f135]) ).
tff(f168,plain,
! [X2: $int,X3: tree1,X0: tree1,X1: color1,X4: $int,X5: $int] :
( lt_tree1(X2,node1(X1,X3,X4,X5,X0))
| ~ $less(X4,X2)
| ~ lt_tree1(X2,X3)
| ~ lt_tree1(X2,X0) ),
inference(cnf_transformation,[],[f137]) ).
tff(f170,plain,
! [X2: tree1,X3: color1,X0: tree1,X1: $int,X4: $int,X5: color1] :
( ~ bst1(node1(X3,X2,X1,X4,X0))
| bst1(node1(X5,X2,X1,X4,X0)) ),
inference(cnf_transformation,[],[f138]) ).
tff(f172,plain,
! [X2: color1,X3: $int,X0: tree1,X1: $int,X4: tree1,X5: $int] :
( ~ lt_tree1(X1,node1(X2,X4,X5,X3,X0))
| lt_tree1(X1,X0) ),
inference(cnf_transformation,[],[f141]) ).
tff(f174,plain,
lt_tree1(sK2,sK3),
inference(cnf_transformation,[],[f143]) ).
tff(f175,plain,
bst1(sK3),
inference(cnf_transformation,[],[f143]) ).
tff(f177,plain,
( ( leaf1 = sK9 )
| ( red1 = sK17 )
| ( sK6 = node1(sK21,sK22,sK23,sK24,sK25) ) ),
inference(cnf_transformation,[],[f143]) ).
tff(f208,plain,
( ( leaf1 = sK9 )
| ~ bst1(node1(red1,node1(black1,sK22,sK23,sK24,sK25),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5)))
| ( red1 = sK17 ) ),
inference(cnf_transformation,[],[f143]) ).
tff(f239,plain,
( ( red1 = sK17 )
| ( red1 = sK21 )
| ( leaf1 = sK9 ) ),
inference(cnf_transformation,[],[f143]) ).
tff(f313,plain,
( ~ bst1(node1(red1,node1(black1,sK6,sK10,sK8,sK19),sK18,sK16,node1(black1,sK20,sK2,sK4,sK5)))
| ( red1 = sK26 )
| ~ bst1(node1(red1,node1(black1,sK6,sK10,sK8,sK19),sK18,sK16,node1(black1,sK20,sK2,sK4,sK5)))
| ( leaf1 = sK9 )
| ( black1 = sK17 ) ),
inference(cnf_transformation,[],[f143]) ).
tff(f322,plain,
( ~ bst1(node1(red1,node1(black1,sK6,sK10,sK8,sK19),sK18,sK16,node1(black1,sK20,sK2,sK4,sK5)))
| ~ bst1(node1(red1,node1(black1,sK30,sK28,sK29,sK27),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5)))
| ( black1 = sK17 )
| ~ bst1(node1(red1,node1(black1,sK6,sK10,sK8,sK19),sK18,sK16,node1(black1,sK20,sK2,sK4,sK5)))
| ( leaf1 = sK9 ) ),
inference(cnf_transformation,[],[f143]) ).
tff(f331,plain,
( ~ bst1(node1(red1,node1(black1,sK6,sK10,sK8,sK19),sK18,sK16,node1(black1,sK20,sK2,sK4,sK5)))
| ( sK6 = node1(sK26,sK30,sK28,sK29,sK27) )
| ( black1 = sK17 )
| ( leaf1 = sK9 ) ),
inference(cnf_transformation,[],[f143]) ).
tff(f332,plain,
( ( sK9 = node1(sK17,sK19,sK18,sK16,sK20) )
| ~ bst1(node1(red1,node1(black1,sK12,sK11,sK14,sK15),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5))) ),
inference(cnf_transformation,[],[f143]) ).
tff(f488,plain,
( ( red1 = sK13 )
| ( sK9 = node1(sK17,sK19,sK18,sK16,sK20) ) ),
inference(cnf_transformation,[],[f143]) ).
tff(f551,plain,
( ( red1 = sK17 )
| ( red1 = sK21 )
| ( red1 = sK13 ) ),
inference(cnf_transformation,[],[f143]) ).
tff(f746,plain,
( ( red1 = sK7 )
| ( red1 = sK7 )
| ( red1 = sK7 )
| ( red1 = sK7 )
| ( red1 = sK7 ) ),
inference(cnf_transformation,[],[f143]) ).
tff(f800,plain,
( ( sK9 = node1(sK17,sK19,sK18,sK16,sK20) )
| ( node1(sK13,sK12,sK11,sK14,sK15) = sK6 ) ),
inference(cnf_transformation,[],[f143]) ).
tff(f863,plain,
( ( red1 = sK21 )
| ( node1(sK13,sK12,sK11,sK14,sK15) = sK6 )
| ( red1 = sK17 ) ),
inference(cnf_transformation,[],[f143]) ).
tff(f956,plain,
sK3 = node1(sK7,sK6,sK10,sK8,sK9),
inference(cnf_transformation,[],[f143]) ).
tff(f957,plain,
gt_tree1(sK2,sK5),
inference(cnf_transformation,[],[f143]) ).
tff(f958,plain,
bst1(sK5),
inference(cnf_transformation,[],[f143]) ).
tff(f959,plain,
! [X2: color1,X3: tree1,X0: tree1,X1: $int,X4: $int] : ( leaf1 != node1(X2,X0,X1,X4,X3) ),
inference(cnf_transformation,[],[f144]) ).
tff(f961,plain,
! [X2: tree1,X3: $int,X0: color1,X1: tree1,X4: $int,X5: $int] :
( ~ lt_tree1(X5,node1(X0,X1,X3,X4,X2))
| $less(X3,X5) ),
inference(cnf_transformation,[],[f145]) ).
tff(f963,plain,
! [X2: $int,X3: tree1,X0: tree1,X1: color1,X4: $int,X5: $int] :
( gt_tree1(X5,node1(X1,X0,X2,X4,X3))
| ~ gt_tree1(X5,X0)
| ~ $less(X5,X2)
| ~ gt_tree1(X5,X3) ),
inference(cnf_transformation,[],[f147]) ).
tff(f964,plain,
red1 != black1,
inference(cnf_transformation,[],[f11]) ).
tff(f965,plain,
! [X2: color1,X3: $int,X0: $int,X1: $int,X4: tree1,X5: tree1] :
( ~ gt_tree1(X1,node1(X2,X5,X0,X3,X4))
| $less(X1,X0) ),
inference(cnf_transformation,[],[f148]) ).
tff(f1007,plain,
red1 = sK7,
inference(duplicate_literal_removal,[],[f746]) ).
tff(f1222,plain,
( ( black1 = sK17 )
| ~ bst1(node1(red1,node1(black1,sK6,sK10,sK8,sK19),sK18,sK16,node1(black1,sK20,sK2,sK4,sK5)))
| ( leaf1 = sK9 )
| ~ bst1(node1(red1,node1(black1,sK30,sK28,sK29,sK27),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5))) ),
inference(duplicate_literal_removal,[],[f322]) ).
tff(f1310,plain,
( ( red1 = sK26 )
| ( leaf1 = sK9 )
| ~ bst1(node1(red1,node1(black1,sK6,sK10,sK8,sK19),sK18,sK16,node1(black1,sK20,sK2,sK4,sK5)))
| ( black1 = sK17 ) ),
inference(duplicate_literal_removal,[],[f313]) ).
tff(f1336,definition,
( spl31_1
<=> ( red1 = sK26 ) ),
introduced(definition,[new_symbols(definition,[spl31_1])],[avatar_definition]) ).
tff(f1338,plain,
( ( red1 = sK26 )
| ~ spl31_1 ),
inference(avatar_component_clause,[],[f1336]) ).
tff(f1340,definition,
( spl31_2
<=> bst1(node1(red1,node1(black1,sK6,sK10,sK8,sK19),sK18,sK16,node1(black1,sK20,sK2,sK4,sK5))) ),
introduced(definition,[new_symbols(definition,[spl31_2])],[avatar_definition]) ).
tff(f1342,plain,
( ~ bst1(node1(red1,node1(black1,sK6,sK10,sK8,sK19),sK18,sK16,node1(black1,sK20,sK2,sK4,sK5)))
| spl31_2 ),
inference(avatar_component_clause,[],[f1340]) ).
tff(f1344,definition,
( spl31_3
<=> bst1(node1(red1,node1(black1,sK12,sK11,sK14,sK15),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5))) ),
introduced(definition,[new_symbols(definition,[spl31_3])],[avatar_definition]) ).
tff(f1346,plain,
( ~ bst1(node1(red1,node1(black1,sK12,sK11,sK14,sK15),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5)))
| spl31_3 ),
inference(avatar_component_clause,[],[f1344]) ).
tff(f1348,definition,
( spl31_4
<=> ( red1 = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl31_4])],[avatar_definition]) ).
tff(f1350,plain,
( ( red1 = sK7 )
| ~ spl31_4 ),
inference(avatar_component_clause,[],[f1348]) ).
tff(f1357,definition,
( spl31_6
<=> bst1(node1(red1,node1(black1,sK22,sK23,sK24,sK25),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5))) ),
introduced(definition,[new_symbols(definition,[spl31_6])],[avatar_definition]) ).
tff(f1359,plain,
( ~ bst1(node1(red1,node1(black1,sK22,sK23,sK24,sK25),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5)))
| spl31_6 ),
inference(avatar_component_clause,[],[f1357]) ).
tff(f1363,definition,
( spl31_7
<=> bst1(node1(red1,node1(black1,sK30,sK28,sK29,sK27),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5))) ),
introduced(definition,[new_symbols(definition,[spl31_7])],[avatar_definition]) ).
tff(f1365,plain,
( ~ bst1(node1(red1,node1(black1,sK30,sK28,sK29,sK27),sK10,sK8,node1(black1,sK9,sK2,sK4,sK5)))
| spl31_7 ),
inference(avatar_component_clause,[],[f1363]) ).
tff(f1367,definition,
( spl31_8
<=> ( red1 = sK21 ) ),
introduced(definition,[new_symbols(definition,[spl31_8])],[avatar_definition]) ).
tff(f1369,plain,
( ( red1 = sK21 )
| ~ spl31_8 ),
inference(avatar_component_clause,[],[f1367]) ).
tff(f1372,definition,
( spl31_9
<=> ( red1 = sK13 ) ),
introduced(definition,[new_symbols(definition,[spl31_9])],[avatar_definition]) ).
tff(f1374,plain,
( ( red1 = sK13 )
| ~ spl31_9 ),
inference(avatar_component_clause,[],[f1372]) ).
tff(f1376,definition,
( spl31_10
<=> ( black1 = sK17 ) ),
introduced(definition,[new_symbols(definition,[spl31_10])],[avatar_definition]) ).
tff(f1378,plain,
( ( black1 = sK17 )
| ~ spl31_10 ),
inference(avatar_component_clause,[],[f1376]) ).
tff(f1381,definition,
( spl31_11
<=> ( leaf1 = sK9 ) ),
introduced(definition,[new_symbols(definition,[spl31_11])],[avatar_definition]) ).
tff(f1383,plain,
( ( leaf1 = sK9 )
| ~ spl31_11 ),
inference(avatar_component_clause,[],[f1381]) ).
tff(f1385,definition,
( spl31_12
<=> ( sK6 = node1(sK21,sK22,sK23,sK24,sK25) ) ),
introduced(definition,[new_symbols(definition,[spl31_12])],[avatar_definition]) ).
tff(f1387,plain,
( ( sK6 = node1(sK21,sK22,sK23,sK24,sK25) )
| ~ spl31_12 ),
inference(avatar_component_clause,[],[f1385]) ).
tff(f1394,definition,
( spl31_14
<=> ( node1(sK13,sK12,sK11,sK14,sK15) = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl31_14])],[avatar_definition]) ).
tff(f1396,plain,
( ( node1(sK13,sK12,sK11,sK14,sK15) = sK6 )
| ~ spl31_14 ),
inference(avatar_component_clause,[],[f1394]) ).
tff(f1402,definition,
( spl31_15
<=> ( sK6 = node1(sK26,sK30,sK28,sK29,sK27) ) ),
introduced(definition,[new_symbols(definition,[spl31_15])],[avatar_definition]) ).
tff(f1404,plain,
( ( sK6 = node1(sK26,sK30,sK28,sK29,sK27) )
| ~ spl31_15 ),
inference(avatar_component_clause,[],[f1402]) ).
tff(f1409,definition,
( spl31_16
<=> ( red1 = sK17 ) ),
introduced(definition,[new_symbols(definition,[spl31_16])],[avatar_definition]) ).
tff(f1411,plain,
( ( red1 = sK17 )
| ~ spl31_16 ),
inference(avatar_component_clause,[],[f1409]) ).
tff(f1480,plain,
spl31_4,
inference(avatar_split_clause,[],[f1007,f1348]) ).
tff(f1520,definition,
( spl31_17
<=> ( sK9 = node1(sK17,sK19,sK18,sK16,sK20) ) ),
introduced(definition,[new_symbols(definition,[spl31_17])],[avatar_definition]) ).
tff(f1522,plain,
( ( sK9 = node1(sK17,sK19,sK18,sK16,sK20) )
| ~ spl31_17 ),
inference(avatar_component_clause,[],[f1520]) ).
tff(f1523,plain,
( spl31_14
| spl31_17 ),
inference(avatar_split_clause,[],[f800,f1520,f1394]) ).
tff(f1543,plain,
( spl31_16
| spl31_11
| spl31_12 ),
inference(avatar_split_clause,[],[f177,f1385,f1381,f1409]) ).
tff(f1644,plain,
( spl31_15
| ~ spl31_2
| spl31_10
| spl31_11 ),
inference(avatar_split_clause,[],[f331,f1381,f1376,f1340,f1402]) ).
tff(f1659,plain,
( spl31_16
| spl31_14
| spl31_8 ),
inference(avatar_split_clause,[],[f863,f1367,f1394,f1409]) ).
tff(f1687,plain,
( spl31_8
| spl31_9
| spl31_16 ),
inference(avatar_split_clause,[],[f551,f1409,f1372,f1367]) ).
tff(f1755,plain,
( spl31_17
| spl31_9 ),
inference(avatar_split_clause,[],[f488,f1372,f1520]) ).
tff(f1850,plain,
( ~ spl31_6
| spl31_11
| spl31_16 ),
inference(avatar_split_clause,[],[f208,f1409,f1381,f1357]) ).
tff(f1939,plain,
( ~ spl31_7
| spl31_10
| spl31_11
| ~ spl31_2 ),
inference(avatar_split_clause,[],[f1222,f1340,f1381,f1376,f1363]) ).
tff(f2003,plain,
( ~ spl31_3
| spl31_17 ),
inference(avatar_split_clause,[],[f332,f1520,f1344]) ).
tff(f2025,plain,
( spl31_16
| spl31_11
| spl31_8 ),
inference(avatar_split_clause,[],[f239,f1367,f1381,f1409]) ).
tff(f2133,plain,
( spl31_10
| spl31_1
| ~ spl31_2
| spl31_11 ),
inference(avatar_split_clause,[],[f1310,f1381,f1340,f1336,f1376]) ).
tff(f2186,plain,
( ( sK3 = node1(red1,sK6,sK10,sK8,sK9) )
| ~ spl31_4 ),
inference(forward_demodulation,[],[f956,f1350]) ).
tff(f2187,plain,
( ( node1(red1,sK12,sK11,sK14,sK15) = sK6 )
| ~ spl31_9
| ~ spl31_14 ),
inference(forward_demodulation,[],[f1396,f1374]) ).
tff(f2223,plain,
( ! [X2: color1,X3: tree1,X0: tree1,X1: $int,X4: $int] : ( node1(X2,X0,X1,X4,X3) != sK9 )
| ~ spl31_11 ),
inference(forward_demodulation,[],[f959,f1383]) ).
tff(f2231,plain,
! [X0: $int] :
( ~ $less(X0,sK2)
| gt_tree1(X0,sK5) ),
inference(resolution,[],[f153,f957]) ).
tff(f2236,plain,
( bst1(sK9)
| ~ bst1(sK3)
| ~ spl31_4 ),
inference(superposition,[],[f158,f2186]) ).
tff(f2237,plain,
( ~ bst1(sK6)
| bst1(sK15)
| ~ spl31_9
| ~ spl31_14 ),
inference(superposition,[],[f158,f2187]) ).
tff(f2239,definition,
( spl31_18
<=> bst1(sK15) ),
introduced(definition,[new_symbols(definition,[spl31_18])],[avatar_definition]) ).
tff(f2243,definition,
( spl31_19
<=> bst1(sK6) ),
introduced(definition,[new_symbols(definition,[spl31_19])],[avatar_definition]) ).
tff(f2244,plain,
( bst1(sK6)
| ~ spl31_19 ),
inference(avatar_component_clause,[],[f2243]) ).
tff(f2247,plain,
( ~ bst1(sK3)
| bst1(sK6)
| ~ spl31_4 ),
inference(superposition,[],[f160,f2186]) ).
tff(f2248,plain,
( ~ bst1(sK6)
| bst1(sK12)
| ~ spl31_9
| ~ spl31_14 ),
inference(superposition,[],[f160,f2187]) ).
tff(f2249,plain,
( bst1(sK6)
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f2247,f175]) ).
tff(f2252,plain,
( $false
| ~ spl31_11
| ~ spl31_17 ),
inference(forward_subsumption_resolution,[],[f1522,f2223]) ).
tff(f2253,plain,
( ~ spl31_11
| ~ spl31_17 ),
inference(avatar_contradiction_clause,[],[f2252]) ).
tff(f2255,plain,
( spl31_19
| ~ spl31_4 ),
inference(avatar_split_clause,[],[f2249,f1348,f2243]) ).
tff(f2256,plain,
( bst1(sK9)
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f2236,f175]) ).
tff(f2264,plain,
( ( sK9 = node1(red1,sK19,sK18,sK16,sK20) )
| ~ spl31_16
| ~ spl31_17 ),
inference(forward_demodulation,[],[f1522,f1411]) ).
tff(f2265,plain,
( bst1(sK19)
| ~ bst1(sK9)
| ~ spl31_16
| ~ spl31_17 ),
inference(superposition,[],[f160,f2264]) ).
tff(f2266,plain,
( bst1(sK20)
| ~ bst1(sK9)
| ~ spl31_16
| ~ spl31_17 ),
inference(superposition,[],[f158,f2264]) ).
tff(f2267,plain,
( bst1(sK19)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17 ),
inference(forward_subsumption_resolution,[],[f2265,f2256]) ).
tff(f2268,plain,
( bst1(sK20)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17 ),
inference(forward_subsumption_resolution,[],[f2266,f2256]) ).
tff(f2282,plain,
( ~ bst1(sK3)
| lt_tree1(sK10,sK6)
| ~ spl31_4 ),
inference(superposition,[],[f157,f2186]) ).
tff(f2283,plain,
( ~ bst1(sK9)
| lt_tree1(sK18,sK19)
| ~ spl31_16
| ~ spl31_17 ),
inference(superposition,[],[f157,f2264]) ).
tff(f2284,plain,
( lt_tree1(sK18,sK19)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17 ),
inference(forward_subsumption_resolution,[],[f2283,f2256]) ).
tff(f2285,plain,
( ~ bst1(sK3)
| gt_tree1(sK10,sK9)
| ~ spl31_4 ),
inference(superposition,[],[f159,f2186]) ).
tff(f2286,plain,
( ~ bst1(sK9)
| gt_tree1(sK18,sK20)
| ~ spl31_16
| ~ spl31_17 ),
inference(superposition,[],[f159,f2264]) ).
tff(f2287,plain,
( gt_tree1(sK10,sK9)
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f2285,f175]) ).
tff(f2288,plain,
( gt_tree1(sK18,sK20)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17 ),
inference(forward_subsumption_resolution,[],[f2286,f2256]) ).
tff(f2325,plain,
( ! [X0: $int] :
( ~ gt_tree1(X0,sK9)
| gt_tree1(X0,sK19) )
| ~ spl31_16
| ~ spl31_17 ),
inference(superposition,[],[f162,f2264]) ).
tff(f2326,plain,
( gt_tree1(sK10,sK19)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17 ),
inference(resolution,[],[f2325,f2287]) ).
tff(f2332,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK3)
| lt_tree1(X0,sK9) )
| ~ spl31_4 ),
inference(superposition,[],[f172,f2186]) ).
tff(f2333,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK9)
| lt_tree1(X0,sK20) )
| ~ spl31_16
| ~ spl31_17 ),
inference(superposition,[],[f172,f2264]) ).
tff(f2335,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK3)
| $less(sK10,X0) )
| ~ spl31_4 ),
inference(superposition,[],[f961,f2186]) ).
tff(f2336,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK9)
| $less(sK18,X0) )
| ~ spl31_16
| ~ spl31_17 ),
inference(superposition,[],[f961,f2264]) ).
tff(f2339,plain,
( ! [X0: $int] :
( ~ gt_tree1(X0,sK9)
| $less(X0,sK18) )
| ~ spl31_16
| ~ spl31_17 ),
inference(superposition,[],[f965,f2264]) ).
tff(f2389,plain,
( lt_tree1(sK2,sK9)
| ~ spl31_4 ),
inference(resolution,[],[f2332,f174]) ).
tff(f2406,plain,
( ~ gt_tree1(sK18,node1(black1,sK20,sK2,sK4,sK5))
| ~ lt_tree1(sK18,node1(black1,sK6,sK10,sK8,sK19))
| ~ bst1(node1(black1,sK6,sK10,sK8,sK19))
| ~ bst1(node1(black1,sK20,sK2,sK4,sK5))
| spl31_2 ),
inference(resolution,[],[f161,f1342]) ).
tff(f2407,plain,
( ~ gt_tree1(sK10,node1(black1,sK9,sK2,sK4,sK5))
| ~ lt_tree1(sK10,node1(black1,sK12,sK11,sK14,sK15))
| ~ bst1(node1(black1,sK9,sK2,sK4,sK5))
| ~ bst1(node1(black1,sK12,sK11,sK14,sK15))
| spl31_3 ),
inference(resolution,[],[f161,f1346]) ).
tff(f2416,definition,
( spl31_25
<=> gt_tree1(sK10,node1(black1,sK9,sK2,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl31_25])],[avatar_definition]) ).
tff(f2417,plain,
( gt_tree1(sK10,node1(black1,sK9,sK2,sK4,sK5))
| ~ spl31_25 ),
inference(avatar_component_clause,[],[f2416]) ).
tff(f2418,plain,
( ~ gt_tree1(sK10,node1(black1,sK9,sK2,sK4,sK5))
| spl31_25 ),
inference(avatar_component_clause,[],[f2416]) ).
tff(f2420,definition,
( spl31_26
<=> bst1(node1(black1,sK12,sK11,sK14,sK15)) ),
introduced(definition,[new_symbols(definition,[spl31_26])],[avatar_definition]) ).
tff(f2422,plain,
( ~ bst1(node1(black1,sK12,sK11,sK14,sK15))
| spl31_26 ),
inference(avatar_component_clause,[],[f2420]) ).
tff(f2424,definition,
( spl31_27
<=> lt_tree1(sK10,node1(black1,sK12,sK11,sK14,sK15)) ),
introduced(definition,[new_symbols(definition,[spl31_27])],[avatar_definition]) ).
tff(f2426,plain,
( ~ lt_tree1(sK10,node1(black1,sK12,sK11,sK14,sK15))
| spl31_27 ),
inference(avatar_component_clause,[],[f2424]) ).
tff(f2428,definition,
( spl31_28
<=> bst1(node1(black1,sK9,sK2,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl31_28])],[avatar_definition]) ).
tff(f2430,plain,
( ~ bst1(node1(black1,sK9,sK2,sK4,sK5))
| spl31_28 ),
inference(avatar_component_clause,[],[f2428]) ).
tff(f2431,plain,
( ~ spl31_25
| ~ spl31_26
| ~ spl31_27
| ~ spl31_28
| spl31_3 ),
inference(avatar_split_clause,[],[f2407,f1344,f2428,f2424,f2420,f2416]) ).
tff(f2433,definition,
( spl31_29
<=> bst1(node1(black1,sK20,sK2,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl31_29])],[avatar_definition]) ).
tff(f2435,plain,
( ~ bst1(node1(black1,sK20,sK2,sK4,sK5))
| spl31_29 ),
inference(avatar_component_clause,[],[f2433]) ).
tff(f2437,definition,
( spl31_30
<=> gt_tree1(sK18,node1(black1,sK20,sK2,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl31_30])],[avatar_definition]) ).
tff(f2439,plain,
( ~ gt_tree1(sK18,node1(black1,sK20,sK2,sK4,sK5))
| spl31_30 ),
inference(avatar_component_clause,[],[f2437]) ).
tff(f2441,definition,
( spl31_31
<=> bst1(node1(black1,sK6,sK10,sK8,sK19)) ),
introduced(definition,[new_symbols(definition,[spl31_31])],[avatar_definition]) ).
tff(f2443,plain,
( ~ bst1(node1(black1,sK6,sK10,sK8,sK19))
| spl31_31 ),
inference(avatar_component_clause,[],[f2441]) ).
tff(f2445,definition,
( spl31_32
<=> lt_tree1(sK18,node1(black1,sK6,sK10,sK8,sK19)) ),
introduced(definition,[new_symbols(definition,[spl31_32])],[avatar_definition]) ).
tff(f2447,plain,
( ~ lt_tree1(sK18,node1(black1,sK6,sK10,sK8,sK19))
| spl31_32 ),
inference(avatar_component_clause,[],[f2445]) ).
tff(f2448,plain,
( ~ spl31_29
| ~ spl31_30
| ~ spl31_31
| ~ spl31_32
| spl31_2 ),
inference(avatar_split_clause,[],[f2406,f1340,f2445,f2441,f2437,f2433]) ).
tff(f2449,plain,
( lt_tree1(sK2,sK20)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17 ),
inference(resolution,[],[f2333,f2389]) ).
tff(f2464,plain,
( $less(sK10,sK2)
| ~ spl31_4 ),
inference(resolution,[],[f2335,f174]) ).
tff(f2475,plain,
( $less(sK18,sK2)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17 ),
inference(resolution,[],[f2336,f2389]) ).
tff(f2480,plain,
( $less(sK10,sK18)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17 ),
inference(resolution,[],[f2339,f2287]) ).
tff(f2481,plain,
( ! [X0: tree1] :
( ~ lt_tree1(sK10,X0)
| lt_tree1(sK18,X0) )
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17 ),
inference(resolution,[],[f2480,f155]) ).
tff(f2503,plain,
( ~ $less(sK10,sK2)
| ~ gt_tree1(sK10,sK5)
| ~ gt_tree1(sK10,sK9)
| spl31_25 ),
inference(resolution,[],[f2418,f963]) ).
tff(f2505,plain,
( ~ $less(sK10,sK2)
| ~ gt_tree1(sK10,sK9)
| spl31_25 ),
inference(forward_subsumption_resolution,[],[f2503,f2231]) ).
tff(f2506,plain,
( ~ gt_tree1(sK10,sK9)
| ~ spl31_4
| spl31_25 ),
inference(forward_subsumption_resolution,[],[f2505,f2464]) ).
tff(f2507,plain,
( $false
| ~ spl31_4
| spl31_25 ),
inference(forward_subsumption_resolution,[],[f2506,f2287]) ).
tff(f2508,plain,
( ~ spl31_4
| spl31_25 ),
inference(avatar_contradiction_clause,[],[f2507]) ).
tff(f2509,plain,
( ~ bst1(sK12)
| ~ bst1(sK15)
| ~ lt_tree1(sK11,sK12)
| ~ gt_tree1(sK11,sK15)
| spl31_26 ),
inference(resolution,[],[f2422,f161]) ).
tff(f2512,definition,
( spl31_33
<=> lt_tree1(sK11,sK12) ),
introduced(definition,[new_symbols(definition,[spl31_33])],[avatar_definition]) ).
tff(f2516,definition,
( spl31_34
<=> gt_tree1(sK11,sK15) ),
introduced(definition,[new_symbols(definition,[spl31_34])],[avatar_definition]) ).
tff(f2520,definition,
( spl31_35
<=> bst1(sK12) ),
introduced(definition,[new_symbols(definition,[spl31_35])],[avatar_definition]) ).
tff(f2523,plain,
( ~ spl31_33
| ~ spl31_34
| ~ spl31_35
| ~ spl31_18
| spl31_26 ),
inference(avatar_split_clause,[],[f2509,f2420,f2239,f2520,f2516,f2512]) ).
tff(f2532,plain,
( ~ $less(sK10,sK18)
| ~ lt_tree1(sK18,sK19)
| ~ lt_tree1(sK18,sK6)
| spl31_32 ),
inference(resolution,[],[f2447,f168]) ).
tff(f2534,plain,
( ~ lt_tree1(sK18,sK19)
| ~ lt_tree1(sK18,sK6)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_32 ),
inference(forward_subsumption_resolution,[],[f2532,f2480]) ).
tff(f2535,plain,
( ~ lt_tree1(sK18,sK6)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_32 ),
inference(forward_subsumption_resolution,[],[f2534,f2284]) ).
tff(f2539,plain,
( ~ gt_tree1(sK2,sK5)
| ~ bst1(sK20)
| ~ bst1(sK5)
| ~ lt_tree1(sK2,sK20)
| spl31_29 ),
inference(resolution,[],[f2435,f161]) ).
tff(f2541,plain,
( ~ bst1(sK20)
| ~ lt_tree1(sK2,sK20)
| ~ bst1(sK5)
| spl31_29 ),
inference(forward_subsumption_resolution,[],[f2539,f957]) ).
tff(f2542,plain,
( ~ bst1(sK5)
| ~ lt_tree1(sK2,sK20)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_29 ),
inference(forward_subsumption_resolution,[],[f2541,f2268]) ).
tff(f2543,plain,
( ~ lt_tree1(sK2,sK20)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_29 ),
inference(forward_subsumption_resolution,[],[f2542,f958]) ).
tff(f2544,plain,
( $false
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_29 ),
inference(forward_subsumption_resolution,[],[f2543,f2449]) ).
tff(f2545,plain,
( ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_29 ),
inference(avatar_contradiction_clause,[],[f2544]) ).
tff(f2574,plain,
( ~ gt_tree1(sK18,sK20)
| ~ gt_tree1(sK18,sK5)
| ~ $less(sK18,sK2)
| spl31_30 ),
inference(resolution,[],[f2439,f963]) ).
tff(f2576,plain,
( ~ $less(sK18,sK2)
| ~ gt_tree1(sK18,sK20)
| spl31_30 ),
inference(forward_subsumption_resolution,[],[f2574,f2231]) ).
tff(f2577,plain,
( ~ gt_tree1(sK18,sK20)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_30 ),
inference(forward_subsumption_resolution,[],[f2576,f2475]) ).
tff(f2578,plain,
( $false
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_30 ),
inference(forward_subsumption_resolution,[],[f2577,f2288]) ).
tff(f2579,plain,
( ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_30 ),
inference(avatar_contradiction_clause,[],[f2578]) ).
tff(f2580,plain,
( lt_tree1(sK10,sK6)
| ~ spl31_4 ),
inference(forward_subsumption_resolution,[],[f2282,f175]) ).
tff(f2582,plain,
( lt_tree1(sK18,sK6)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17 ),
inference(resolution,[],[f2580,f2481]) ).
tff(f2584,plain,
( ( node1(red1,sK30,sK28,sK29,sK27) = sK6 )
| ~ spl31_1
| ~ spl31_15 ),
inference(forward_demodulation,[],[f1404,f1338]) ).
tff(f2595,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK6)
| lt_tree1(X0,sK30) )
| ~ spl31_1
| ~ spl31_15 ),
inference(superposition,[],[f166,f2584]) ).
tff(f2597,plain,
( ! [X0: color1] :
( bst1(node1(X0,sK30,sK28,sK29,sK27))
| ~ bst1(sK6) )
| ~ spl31_1
| ~ spl31_15 ),
inference(superposition,[],[f170,f2584]) ).
tff(f2599,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK6)
| lt_tree1(X0,sK27) )
| ~ spl31_1
| ~ spl31_15 ),
inference(superposition,[],[f172,f2584]) ).
tff(f2600,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK6)
| $less(sK28,X0) )
| ~ spl31_1
| ~ spl31_15 ),
inference(superposition,[],[f961,f2584]) ).
tff(f2606,plain,
( ! [X0: color1] : bst1(node1(X0,sK30,sK28,sK29,sK27))
| ~ spl31_1
| ~ spl31_15
| ~ spl31_19 ),
inference(forward_subsumption_resolution,[],[f2597,f2244]) ).
tff(f2621,plain,
( ~ bst1(node1(black1,sK30,sK28,sK29,sK27))
| ~ gt_tree1(sK10,node1(black1,sK9,sK2,sK4,sK5))
| ~ bst1(node1(black1,sK9,sK2,sK4,sK5))
| ~ lt_tree1(sK10,node1(black1,sK30,sK28,sK29,sK27))
| spl31_7 ),
inference(resolution,[],[f1365,f161]) ).
tff(f2623,plain,
( ~ bst1(node1(black1,sK9,sK2,sK4,sK5))
| ~ lt_tree1(sK10,node1(black1,sK30,sK28,sK29,sK27))
| ~ bst1(node1(black1,sK30,sK28,sK29,sK27))
| spl31_7
| ~ spl31_25 ),
inference(forward_subsumption_resolution,[],[f2621,f2417]) ).
tff(f2625,definition,
( spl31_39
<=> lt_tree1(sK10,node1(black1,sK30,sK28,sK29,sK27)) ),
introduced(definition,[new_symbols(definition,[spl31_39])],[avatar_definition]) ).
tff(f2627,plain,
( ~ lt_tree1(sK10,node1(black1,sK30,sK28,sK29,sK27))
| spl31_39 ),
inference(avatar_component_clause,[],[f2625]) ).
tff(f2629,definition,
( spl31_40
<=> bst1(node1(black1,sK30,sK28,sK29,sK27)) ),
introduced(definition,[new_symbols(definition,[spl31_40])],[avatar_definition]) ).
tff(f2631,plain,
( ~ bst1(node1(black1,sK30,sK28,sK29,sK27))
| spl31_40 ),
inference(avatar_component_clause,[],[f2629]) ).
tff(f2632,plain,
( ~ spl31_39
| ~ spl31_28
| ~ spl31_40
| spl31_7
| ~ spl31_25 ),
inference(avatar_split_clause,[],[f2623,f2416,f1363,f2629,f2428,f2625]) ).
tff(f2639,plain,
( ( red1 = black1 )
| ~ spl31_10
| ~ spl31_16 ),
inference(forward_demodulation,[],[f1378,f1411]) ).
tff(f2641,plain,
( $false
| ~ spl31_10
| ~ spl31_16 ),
inference(forward_subsumption_resolution,[],[f2639,f964]) ).
tff(f2642,plain,
( ~ spl31_10
| ~ spl31_16 ),
inference(avatar_contradiction_clause,[],[f2641]) ).
tff(f2647,plain,
( ( sK6 = node1(red1,sK22,sK23,sK24,sK25) )
| ~ spl31_8
| ~ spl31_12 ),
inference(forward_demodulation,[],[f1387,f1369]) ).
tff(f2660,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK6)
| lt_tree1(X0,sK22) )
| ~ spl31_8
| ~ spl31_12 ),
inference(superposition,[],[f166,f2647]) ).
tff(f2662,plain,
( ! [X0: color1] :
( bst1(node1(X0,sK22,sK23,sK24,sK25))
| ~ bst1(sK6) )
| ~ spl31_8
| ~ spl31_12 ),
inference(superposition,[],[f170,f2647]) ).
tff(f2664,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK6)
| lt_tree1(X0,sK25) )
| ~ spl31_8
| ~ spl31_12 ),
inference(superposition,[],[f172,f2647]) ).
tff(f2666,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK6)
| $less(sK23,X0) )
| ~ spl31_8
| ~ spl31_12 ),
inference(superposition,[],[f961,f2647]) ).
tff(f2683,plain,
( ! [X0: color1] : bst1(node1(X0,sK22,sK23,sK24,sK25))
| ~ spl31_8
| ~ spl31_12
| ~ spl31_19 ),
inference(forward_subsumption_resolution,[],[f2662,f2244]) ).
tff(f2712,plain,
( ~ bst1(node1(black1,sK22,sK23,sK24,sK25))
| ~ lt_tree1(sK10,node1(black1,sK22,sK23,sK24,sK25))
| ~ gt_tree1(sK10,node1(black1,sK9,sK2,sK4,sK5))
| ~ bst1(node1(black1,sK9,sK2,sK4,sK5))
| spl31_6 ),
inference(resolution,[],[f1359,f161]) ).
tff(f2714,plain,
( ~ lt_tree1(sK10,node1(black1,sK22,sK23,sK24,sK25))
| ~ bst1(node1(black1,sK9,sK2,sK4,sK5))
| ~ bst1(node1(black1,sK22,sK23,sK24,sK25))
| spl31_6
| ~ spl31_25 ),
inference(forward_subsumption_resolution,[],[f2712,f2417]) ).
tff(f2716,definition,
( spl31_43
<=> bst1(node1(black1,sK22,sK23,sK24,sK25)) ),
introduced(definition,[new_symbols(definition,[spl31_43])],[avatar_definition]) ).
tff(f2718,plain,
( ~ bst1(node1(black1,sK22,sK23,sK24,sK25))
| spl31_43 ),
inference(avatar_component_clause,[],[f2716]) ).
tff(f2720,definition,
( spl31_44
<=> lt_tree1(sK10,node1(black1,sK22,sK23,sK24,sK25)) ),
introduced(definition,[new_symbols(definition,[spl31_44])],[avatar_definition]) ).
tff(f2722,plain,
( ~ lt_tree1(sK10,node1(black1,sK22,sK23,sK24,sK25))
| spl31_44 ),
inference(avatar_component_clause,[],[f2720]) ).
tff(f2723,plain,
( ~ spl31_43
| ~ spl31_44
| ~ spl31_28
| spl31_6
| ~ spl31_25 ),
inference(avatar_split_clause,[],[f2714,f2416,f1357,f2428,f2720,f2716]) ).
tff(f2728,plain,
( lt_tree1(sK10,sK22)
| ~ spl31_4
| ~ spl31_8
| ~ spl31_12 ),
inference(resolution,[],[f2660,f2580]) ).
tff(f2733,plain,
( lt_tree1(sK10,sK25)
| ~ spl31_4
| ~ spl31_8
| ~ spl31_12 ),
inference(resolution,[],[f2664,f2580]) ).
tff(f2738,plain,
( $less(sK23,sK10)
| ~ spl31_4
| ~ spl31_8
| ~ spl31_12 ),
inference(resolution,[],[f2666,f2580]) ).
tff(f2778,plain,
( ~ gt_tree1(sK2,sK5)
| ~ bst1(sK5)
| ~ lt_tree1(sK2,sK9)
| ~ bst1(sK9)
| spl31_28 ),
inference(resolution,[],[f2430,f161]) ).
tff(f2780,plain,
( ~ bst1(sK5)
| ~ bst1(sK9)
| ~ lt_tree1(sK2,sK9)
| spl31_28 ),
inference(forward_subsumption_resolution,[],[f2778,f957]) ).
tff(f2781,plain,
( ~ lt_tree1(sK2,sK9)
| ~ bst1(sK9)
| spl31_28 ),
inference(forward_subsumption_resolution,[],[f2780,f958]) ).
tff(f2782,plain,
( ~ bst1(sK9)
| ~ spl31_4
| spl31_28 ),
inference(forward_subsumption_resolution,[],[f2781,f2389]) ).
tff(f2783,plain,
( $false
| ~ spl31_4
| spl31_28 ),
inference(forward_subsumption_resolution,[],[f2782,f2256]) ).
tff(f2784,plain,
( ~ spl31_4
| spl31_28 ),
inference(avatar_contradiction_clause,[],[f2783]) ).
tff(f2792,plain,
( ~ bst1(sK6)
| ~ gt_tree1(sK10,sK19)
| ~ lt_tree1(sK10,sK6)
| ~ bst1(sK19)
| spl31_31 ),
inference(resolution,[],[f2443,f161]) ).
tff(f2794,plain,
( ~ bst1(sK19)
| ~ lt_tree1(sK10,sK6)
| ~ gt_tree1(sK10,sK19)
| ~ spl31_19
| spl31_31 ),
inference(forward_subsumption_resolution,[],[f2792,f2244]) ).
tff(f2795,plain,
( ~ lt_tree1(sK10,sK6)
| ~ gt_tree1(sK10,sK19)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| ~ spl31_19
| spl31_31 ),
inference(forward_subsumption_resolution,[],[f2794,f2267]) ).
tff(f2796,plain,
( ~ gt_tree1(sK10,sK19)
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| ~ spl31_19
| spl31_31 ),
inference(forward_subsumption_resolution,[],[f2795,f2580]) ).
tff(f2797,plain,
( $false
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| ~ spl31_19
| spl31_31 ),
inference(forward_subsumption_resolution,[],[f2796,f2326]) ).
tff(f2798,plain,
( ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| ~ spl31_19
| spl31_31 ),
inference(avatar_contradiction_clause,[],[f2797]) ).
tff(f2799,plain,
( $false
| ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_32 ),
inference(forward_subsumption_resolution,[],[f2535,f2582]) ).
tff(f2800,plain,
( ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_32 ),
inference(avatar_contradiction_clause,[],[f2799]) ).
tff(f2938,plain,
( lt_tree1(sK10,sK30)
| ~ spl31_1
| ~ spl31_4
| ~ spl31_15 ),
inference(resolution,[],[f2595,f2580]) ).
tff(f2941,plain,
( lt_tree1(sK10,sK27)
| ~ spl31_1
| ~ spl31_4
| ~ spl31_15 ),
inference(resolution,[],[f2599,f2580]) ).
tff(f2944,plain,
( $less(sK28,sK10)
| ~ spl31_1
| ~ spl31_4
| ~ spl31_15 ),
inference(resolution,[],[f2600,f2580]) ).
tff(f2967,plain,
( $false
| ~ spl31_1
| ~ spl31_15
| ~ spl31_19
| spl31_40 ),
inference(forward_subsumption_resolution,[],[f2631,f2606]) ).
tff(f2968,plain,
( ~ spl31_1
| ~ spl31_15
| ~ spl31_19
| spl31_40 ),
inference(avatar_contradiction_clause,[],[f2967]) ).
tff(f2969,plain,
( ~ $less(sK28,sK10)
| ~ lt_tree1(sK10,sK30)
| ~ lt_tree1(sK10,sK27)
| spl31_39 ),
inference(resolution,[],[f2627,f168]) ).
tff(f2971,plain,
( ~ lt_tree1(sK10,sK27)
| ~ $less(sK28,sK10)
| ~ spl31_1
| ~ spl31_4
| ~ spl31_15
| spl31_39 ),
inference(forward_subsumption_resolution,[],[f2969,f2938]) ).
tff(f2972,plain,
( ~ $less(sK28,sK10)
| ~ spl31_1
| ~ spl31_4
| ~ spl31_15
| spl31_39 ),
inference(forward_subsumption_resolution,[],[f2971,f2941]) ).
tff(f2973,plain,
( $false
| ~ spl31_1
| ~ spl31_4
| ~ spl31_15
| spl31_39 ),
inference(forward_subsumption_resolution,[],[f2972,f2944]) ).
tff(f2974,plain,
( ~ spl31_1
| ~ spl31_4
| ~ spl31_15
| spl31_39 ),
inference(avatar_contradiction_clause,[],[f2973]) ).
tff(f2996,plain,
( ~ lt_tree1(sK10,sK25)
| ~ lt_tree1(sK10,sK22)
| ~ $less(sK23,sK10)
| spl31_44 ),
inference(resolution,[],[f2722,f168]) ).
tff(f2998,plain,
( ~ lt_tree1(sK10,sK22)
| ~ $less(sK23,sK10)
| ~ spl31_4
| ~ spl31_8
| ~ spl31_12
| spl31_44 ),
inference(forward_subsumption_resolution,[],[f2996,f2733]) ).
tff(f2999,plain,
( ~ $less(sK23,sK10)
| ~ spl31_4
| ~ spl31_8
| ~ spl31_12
| spl31_44 ),
inference(forward_subsumption_resolution,[],[f2998,f2728]) ).
tff(f3000,plain,
( $false
| ~ spl31_4
| ~ spl31_8
| ~ spl31_12
| spl31_44 ),
inference(forward_subsumption_resolution,[],[f2999,f2738]) ).
tff(f3001,plain,
( ~ spl31_4
| ~ spl31_8
| ~ spl31_12
| spl31_44 ),
inference(avatar_contradiction_clause,[],[f3000]) ).
tff(f3002,plain,
( $false
| ~ spl31_8
| ~ spl31_12
| ~ spl31_19
| spl31_43 ),
inference(forward_subsumption_resolution,[],[f2718,f2683]) ).
tff(f3003,plain,
( ~ spl31_8
| ~ spl31_12
| ~ spl31_19
| spl31_43 ),
inference(avatar_contradiction_clause,[],[f3002]) ).
tff(f3004,plain,
( bst1(sK12)
| ~ spl31_9
| ~ spl31_14
| ~ spl31_19 ),
inference(forward_subsumption_resolution,[],[f2248,f2244]) ).
tff(f3005,plain,
( bst1(sK15)
| ~ spl31_9
| ~ spl31_14
| ~ spl31_19 ),
inference(forward_subsumption_resolution,[],[f2237,f2244]) ).
tff(f3010,plain,
( spl31_35
| ~ spl31_9
| ~ spl31_14
| ~ spl31_19 ),
inference(avatar_split_clause,[],[f3004,f2243,f1394,f1372,f2520]) ).
tff(f3011,plain,
( spl31_18
| ~ spl31_9
| ~ spl31_14
| ~ spl31_19 ),
inference(avatar_split_clause,[],[f3005,f2243,f1394,f1372,f2239]) ).
tff(f3027,plain,
( ~ bst1(sK6)
| lt_tree1(sK11,sK12)
| ~ spl31_9
| ~ spl31_14 ),
inference(superposition,[],[f157,f2187]) ).
tff(f3029,plain,
( gt_tree1(sK11,sK15)
| ~ bst1(sK6)
| ~ spl31_9
| ~ spl31_14 ),
inference(superposition,[],[f159,f2187]) ).
tff(f3035,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK6)
| lt_tree1(X0,sK12) )
| ~ spl31_9
| ~ spl31_14 ),
inference(superposition,[],[f166,f2187]) ).
tff(f3039,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK6)
| lt_tree1(X0,sK15) )
| ~ spl31_9
| ~ spl31_14 ),
inference(superposition,[],[f172,f2187]) ).
tff(f3041,plain,
( ! [X0: $int] :
( ~ lt_tree1(X0,sK6)
| $less(sK11,X0) )
| ~ spl31_9
| ~ spl31_14 ),
inference(superposition,[],[f961,f2187]) ).
tff(f3044,plain,
( gt_tree1(sK11,sK15)
| ~ spl31_9
| ~ spl31_14
| ~ spl31_19 ),
inference(forward_subsumption_resolution,[],[f3029,f2244]) ).
tff(f3045,plain,
( lt_tree1(sK11,sK12)
| ~ spl31_9
| ~ spl31_14
| ~ spl31_19 ),
inference(forward_subsumption_resolution,[],[f3027,f2244]) ).
tff(f3058,plain,
( spl31_34
| ~ spl31_9
| ~ spl31_14
| ~ spl31_19 ),
inference(avatar_split_clause,[],[f3044,f2243,f1394,f1372,f2516]) ).
tff(f3059,plain,
( spl31_33
| ~ spl31_9
| ~ spl31_14
| ~ spl31_19 ),
inference(avatar_split_clause,[],[f3045,f2243,f1394,f1372,f2512]) ).
tff(f3086,plain,
( lt_tree1(sK10,sK12)
| ~ spl31_4
| ~ spl31_9
| ~ spl31_14 ),
inference(resolution,[],[f3035,f2580]) ).
tff(f3088,plain,
( lt_tree1(sK10,sK15)
| ~ spl31_4
| ~ spl31_9
| ~ spl31_14 ),
inference(resolution,[],[f3039,f2580]) ).
tff(f3091,plain,
( $less(sK11,sK10)
| ~ spl31_4
| ~ spl31_9
| ~ spl31_14 ),
inference(resolution,[],[f3041,f2580]) ).
tff(f3110,plain,
( ~ lt_tree1(sK10,sK12)
| ~ $less(sK11,sK10)
| ~ lt_tree1(sK10,sK15)
| spl31_27 ),
inference(resolution,[],[f2426,f168]) ).
tff(f3112,plain,
( ~ $less(sK11,sK10)
| ~ lt_tree1(sK10,sK15)
| ~ spl31_4
| ~ spl31_9
| ~ spl31_14
| spl31_27 ),
inference(forward_subsumption_resolution,[],[f3110,f3086]) ).
tff(f3113,plain,
( ~ lt_tree1(sK10,sK15)
| ~ spl31_4
| ~ spl31_9
| ~ spl31_14
| spl31_27 ),
inference(forward_subsumption_resolution,[],[f3112,f3091]) ).
tff(f3114,plain,
( $false
| ~ spl31_4
| ~ spl31_9
| ~ spl31_14
| spl31_27 ),
inference(forward_subsumption_resolution,[],[f3113,f3088]) ).
tff(f3115,plain,
( ~ spl31_4
| ~ spl31_9
| ~ spl31_14
| spl31_27 ),
inference(avatar_contradiction_clause,[],[f3114]) ).
cnf(s82,plain,
spl31_4,
inference(sat_conversion,[],[f1480]) ).
cnf(s121,plain,
( spl31_14
| spl31_17 ),
inference(sat_conversion,[],[f1523]) ).
cnf(s141,plain,
( spl31_11
| spl31_12
| spl31_16 ),
inference(sat_conversion,[],[f1543]) ).
cnf(s242,plain,
( ~ spl31_2
| spl31_10
| spl31_11
| spl31_15 ),
inference(sat_conversion,[],[f1644]) ).
cnf(s257,plain,
( spl31_8
| spl31_14
| spl31_16 ),
inference(sat_conversion,[],[f1659]) ).
cnf(s285,plain,
( spl31_8
| spl31_9
| spl31_16 ),
inference(sat_conversion,[],[f1687]) ).
cnf(s353,plain,
( spl31_9
| spl31_17 ),
inference(sat_conversion,[],[f1755]) ).
cnf(s448,plain,
( ~ spl31_6
| spl31_11
| spl31_16 ),
inference(sat_conversion,[],[f1850]) ).
cnf(s537,plain,
( ~ spl31_2
| ~ spl31_7
| spl31_10
| spl31_11 ),
inference(sat_conversion,[],[f1939]) ).
cnf(s601,plain,
( ~ spl31_3
| spl31_17 ),
inference(sat_conversion,[],[f2003]) ).
cnf(s623,plain,
( spl31_8
| spl31_11
| spl31_16 ),
inference(sat_conversion,[],[f2025]) ).
cnf(s731,plain,
( spl31_1
| ~ spl31_2
| spl31_10
| spl31_11 ),
inference(sat_conversion,[],[f2133]) ).
cnf(s783,plain,
( ~ spl31_11
| ~ spl31_17 ),
inference(sat_conversion,[],[f2253]) ).
cnf(s784,plain,
( ~ spl31_4
| spl31_19 ),
inference(sat_conversion,[],[f2255]) ).
cnf(s788,plain,
( spl31_3
| ~ spl31_25
| ~ spl31_26
| ~ spl31_27
| ~ spl31_28 ),
inference(sat_conversion,[],[f2431]) ).
cnf(s789,plain,
( spl31_2
| ~ spl31_29
| ~ spl31_30
| ~ spl31_31
| ~ spl31_32 ),
inference(sat_conversion,[],[f2448]) ).
cnf(s791,plain,
( ~ spl31_4
| spl31_25 ),
inference(sat_conversion,[],[f2508]) ).
cnf(s792,plain,
( ~ spl31_18
| spl31_26
| ~ spl31_33
| ~ spl31_34
| ~ spl31_35 ),
inference(sat_conversion,[],[f2523]) ).
cnf(s794,plain,
( ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_29 ),
inference(sat_conversion,[],[f2545]) ).
cnf(s796,plain,
( ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_30 ),
inference(sat_conversion,[],[f2579]) ).
cnf(s799,plain,
( spl31_7
| ~ spl31_25
| ~ spl31_28
| ~ spl31_39
| ~ spl31_40 ),
inference(sat_conversion,[],[f2632]) ).
cnf(s801,plain,
( ~ spl31_10
| ~ spl31_16 ),
inference(sat_conversion,[],[f2642]) ).
cnf(s806,plain,
( spl31_6
| ~ spl31_25
| ~ spl31_28
| ~ spl31_43
| ~ spl31_44 ),
inference(sat_conversion,[],[f2723]) ).
cnf(s807,plain,
( ~ spl31_4
| spl31_28 ),
inference(sat_conversion,[],[f2784]) ).
cnf(s808,plain,
( ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| ~ spl31_19
| spl31_31 ),
inference(sat_conversion,[],[f2798]) ).
cnf(s809,plain,
( ~ spl31_4
| ~ spl31_16
| ~ spl31_17
| spl31_32 ),
inference(sat_conversion,[],[f2800]) ).
cnf(s815,plain,
( ~ spl31_1
| ~ spl31_15
| ~ spl31_19
| spl31_40 ),
inference(sat_conversion,[],[f2968]) ).
cnf(s816,plain,
( ~ spl31_1
| ~ spl31_4
| ~ spl31_15
| spl31_39 ),
inference(sat_conversion,[],[f2974]) ).
cnf(s818,plain,
( ~ spl31_4
| ~ spl31_8
| ~ spl31_12
| spl31_44 ),
inference(sat_conversion,[],[f3001]) ).
cnf(s819,plain,
( ~ spl31_8
| ~ spl31_12
| ~ spl31_19
| spl31_43 ),
inference(sat_conversion,[],[f3003]) ).
cnf(s822,plain,
( ~ spl31_9
| ~ spl31_14
| ~ spl31_19
| spl31_35 ),
inference(sat_conversion,[],[f3010]) ).
cnf(s823,plain,
( ~ spl31_9
| ~ spl31_14
| spl31_18
| ~ spl31_19 ),
inference(sat_conversion,[],[f3011]) ).
cnf(s827,plain,
( ~ spl31_9
| ~ spl31_14
| ~ spl31_19
| spl31_34 ),
inference(sat_conversion,[],[f3058]) ).
cnf(s828,plain,
( ~ spl31_9
| ~ spl31_14
| ~ spl31_19
| spl31_33 ),
inference(sat_conversion,[],[f3059]) ).
cnf(s831,plain,
( ~ spl31_4
| ~ spl31_9
| ~ spl31_14
| spl31_27 ),
inference(sat_conversion,[],[f3115]) ).
cnf(s832,plain,
spl31_28,
inference(rat,[],[s807,s82]) ).
cnf(s833,plain,
spl31_25,
inference(rat,[],[s791,s82]) ).
cnf(s834,plain,
spl31_19,
inference(rat,[],[s784,s82]) ).
cnf(s835,plain,
( spl31_9
| spl31_8
| spl31_2 ),
inference(rat,[],[s789,s794,s796,s808,s809,s285,s353,s82,s834]) ).
cnf(s836,plain,
( ~ spl31_17
| ~ spl31_16
| spl31_2 ),
inference(rat,[],[s789,s794,s796,s808,s809,s82,s834]) ).
cnf(s837,plain,
( ~ spl31_14
| ~ spl31_9
| spl31_3 ),
inference(rat,[],[s788,s792,s823,s831,s822,s827,s828,s833,s832,s834,s82]) ).
cnf(s838,plain,
( spl31_8
| spl31_3
| spl31_2 ),
inference(rat,[],[s836,s121,s257,s837,s835]) ).
cnf(s839,plain,
( spl31_17
| spl31_3 ),
inference(rat,[],[s837,s121,s353]) ).
cnf(s840,plain,
( spl31_3
| spl31_2 ),
inference(rat,[],[s448,s806,s818,s819,s141,s836,s783,s839,s838,s834,s82,s833,s832]) ).
cnf(s841,plain,
( spl31_16
| spl31_11 ),
inference(rat,[],[s806,s818,s819,s141,s448,s623,s834,s82,s833,s832]) ).
cnf(s842,plain,
spl31_2,
inference(rat,[],[s841,s836,s783,s601,s840]) ).
cnf(s845,plain,
spl31_17,
inference(rat,[],[s839,s601]) ).
cnf(s846,plain,
~ spl31_11,
inference(rat,[],[s783,s845]) ).
cnf(s847,plain,
spl31_16,
inference(rat,[],[s841,s846]) ).
cnf(s848,plain,
~ spl31_10,
inference(rat,[],[s801,s847]) ).
cnf(s852,plain,
spl31_1,
inference(rat,[],[s731,s842,s846,s848]) ).
cnf(s853,plain,
~ spl31_7,
inference(rat,[],[s537,s842,s846,s848]) ).
cnf(s854,plain,
spl31_15,
inference(rat,[],[s242,s846,s842,s848]) ).
cnf(s855,plain,
spl31_40,
inference(rat,[],[s815,s852,s834,s854]) ).
cnf(s856,plain,
spl31_39,
inference(rat,[],[s816,s852,s82,s854]) ).
cnf(s857,plain,
$false,
inference(rat,[],[s799,s853,s833,s832,s856,s855]) ).
tff(f3116,plain,
$false,
inference(avatar_sat_refutation,[],[s857]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW654_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n018.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 14:26:10 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.51/1.23 % (3423487)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.51/1.23 % (3423583)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3614446357:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.51/1.23 % (3423583)Instruction limit reached!
% 3.51/1.23 % (3423583)------------------------------
% 3.51/1.23 % (3423583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.23 % (3423583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.23 % (3423583)CaDiCaL version: 2.1.3
% 3.51/1.23 % (3423583)Termination reason: Instruction limit
% 3.51/1.23 % (3423583)Termination phase: Saturation
% 3.51/1.23 % (3423583)Time elapsed: 0.027 s
% 3.51/1.23 % (3423583)Peak memory usage: 116 MB
% 3.51/1.23 % (3423583)Instructions burned: 34 (million)
% 3.51/1.23 % (3423578)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4231637954:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.51/1.23 % (3423582)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1022467364:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.51/1.23 % (3423579)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1583165563:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.51/1.23 % (3423577)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2320611410:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.51/1.23 % (3423580)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=462705036:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.51/1.23 % (3423581)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=789201879:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.51/1.23 % (3423581)Instruction limit reached!
% 3.51/1.23 % (3423581)------------------------------
% 3.51/1.23 % (3423581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.23 % (3423581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.23 % (3423581)CaDiCaL version: 2.1.3
% 3.51/1.23 % (3423581)Termination reason: Instruction limit
% 3.51/1.23 % (3423581)Termination phase: Property scanning
% 3.51/1.23 % (3423581)Time elapsed: 0.003 s
% 3.51/1.23 % (3423581)Peak memory usage: 86 MB
% 3.51/1.23 % (3423581)Instructions burned: 4 (million)
% 3.51/1.23 % (3423580)Instruction limit reached!
% 3.51/1.23 % (3423580)------------------------------
% 3.51/1.23 % (3423580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.23 % (3423580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.23 % (3423580)CaDiCaL version: 2.1.3
% 3.51/1.23 % (3423580)Termination reason: Instruction limit
% 3.51/1.23 % (3423580)Termination phase: Saturation
% 3.51/1.23 % (3423580)Time elapsed: 0.005 s
% 3.51/1.23 % (3423580)Peak memory usage: 87 MB
% 3.51/1.23 % (3423580)Instructions burned: 8 (million)
% 3.51/1.23 % (3423577)Instruction limit reached!
% 3.51/1.23 % (3423577)------------------------------
% 3.51/1.23 % (3423577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.23 % (3423577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.23 % (3423577)CaDiCaL version: 2.1.3
% 3.51/1.23 % (3423577)Termination reason: Instruction limit
% 3.51/1.23 % (3423577)Termination phase: Saturation
% 3.51/1.23 % (3423577)Time elapsed: 0.030 s
% 3.51/1.23 % (3423577)Peak memory usage: 113 MB
% 3.51/1.23 % (3423577)Instructions burned: 12 (million)
% 3.51/1.23 % (3423582)Instruction limit reached!
% 3.51/1.23 % (3423582)------------------------------
% 3.51/1.23 % (3423582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.23 % (3423582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.23 % (3423582)CaDiCaL version: 2.1.3
% 3.51/1.23 % (3423582)Termination reason: Instruction limit
% 3.51/1.23 % (3423582)Termination phase: Saturation
% 3.51/1.23 % (3423582)Time elapsed: 0.054 s
% 3.51/1.23 % (3423582)Peak memory usage: 115 MB
% 3.51/1.23 % (3423582)Instructions burned: 47 (million)
% 3.51/1.23 % (3423585)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=120936623:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.51/1.23 % (3423585)Instruction limit reached!
% 3.51/1.23 % (3423585)------------------------------
% 4.54/1.39 % (3423585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.54/1.39 % (3423585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.54/1.39 % (3423585)CaDiCaL version: 2.1.3
% 4.54/1.39 % (3423585)Termination reason: Instruction limit
% 4.54/1.39 % (3423585)Termination phase: Saturation
% 4.54/1.39 % (3423585)Time elapsed: 0.006 s
% 4.54/1.39 % (3423585)Peak memory usage: 88 MB
% 4.54/1.39 % (3423585)Instructions burned: 17 (million)
% 4.54/1.39 % (3423579)Instruction limit reached!
% 4.54/1.39 % (3423579)------------------------------
% 4.54/1.39 % (3423579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.54/1.39 % (3423579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.54/1.39 % (3423579)CaDiCaL version: 2.1.3
% 4.54/1.39 % (3423579)Termination reason: Instruction limit
% 4.54/1.39 % (3423579)Termination phase: Saturation
% 4.54/1.39 % (3423579)Time elapsed: 0.123 s
% 4.54/1.39 % (3423579)Peak memory usage: 116 MB
% 4.54/1.39 % (3423579)Instructions burned: 201 (million)
% 4.54/1.39 % (3423593)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1174605249:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.54/1.39 % (3423592)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=4194301872:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.54/1.39 % (3423593)Instruction limit reached!
% 4.54/1.39 % (3423593)------------------------------
% 4.54/1.39 % (3423593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.54/1.39 % (3423593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.54/1.39 % (3423593)CaDiCaL version: 2.1.3
% 4.54/1.39 % (3423593)Termination reason: Instruction limit
% 4.54/1.39 % (3423593)Termination phase: Saturation
% 4.54/1.39 % (3423593)Time elapsed: 0.010 s
% 4.54/1.39 % (3423593)Peak memory usage: 88 MB
% 4.54/1.39 % (3423593)Instructions burned: 18 (million)
% 4.54/1.39 % (3423592)Instruction limit reached!
% 4.54/1.39 % (3423592)------------------------------
% 4.54/1.39 % (3423592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.54/1.39 % (3423592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.54/1.39 % (3423592)CaDiCaL version: 2.1.3
% 4.54/1.39 % (3423592)Termination reason: Instruction limit
% 4.54/1.39 % (3423592)Termination phase: Property scanning
% 4.54/1.39 % (3423592)Time elapsed: 0.013 s
% 4.54/1.39 % (3423592)Peak memory usage: 86 MB
% 4.54/1.39 % (3423592)Instructions burned: 31 (million)
% 4.54/1.39 % (3423594)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=41332009:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.54/1.39 % (3423578)Instruction limit reached!
% 4.54/1.39 % (3423578)------------------------------
% 4.54/1.39 % (3423578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.54/1.39 % (3423578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.54/1.39 % (3423578)CaDiCaL version: 2.1.3
% 4.54/1.39 % (3423578)Termination reason: Instruction limit
% 4.54/1.39 % (3423578)Termination phase: Saturation
% 4.54/1.39 % (3423578)Time elapsed: 0.188 s
% 4.54/1.39 % (3423578)Peak memory usage: 118 MB
% 4.54/1.39 % (3423578)Instructions burned: 310 (million)
% 4.54/1.39 % (3423594)Instruction limit reached!
% 4.54/1.39 % (3423594)------------------------------
% 4.54/1.39 % (3423594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.54/1.39 % (3423594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.54/1.39 % (3423594)CaDiCaL version: 2.1.3
% 4.54/1.39 % (3423594)Termination reason: Instruction limit
% 4.54/1.39 % (3423594)Termination phase: Saturation
% 4.54/1.39 % (3423594)Time elapsed: 0.020 s
% 4.54/1.39 % (3423594)Peak memory usage: 89 MB
% 4.54/1.39 % (3423594)Instructions burned: 25 (million)
% 4.54/1.39 % (3423595)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=3760931333:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.54/1.39 % (3423597)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4249224524:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.54/1.39 % (3423595)Instruction limit reached!
% 4.54/1.39 % (3423595)------------------------------
% 4.54/1.39 % (3423595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.43/1.58 % (3423595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.58 % (3423595)CaDiCaL version: 2.1.3
% 5.43/1.58 % (3423595)Termination reason: Instruction limit
% 5.43/1.58 % (3423595)Termination phase: Saturation
% 5.43/1.58 % (3423595)Time elapsed: 0.019 s
% 5.43/1.58 % (3423595)Peak memory usage: 90 MB
% 5.43/1.58 % (3423595)Instructions burned: 28 (million)
% 5.43/1.58 % (3423597)Instruction limit reached!
% 5.43/1.58 % (3423597)------------------------------
% 5.43/1.58 % (3423597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.43/1.58 % (3423597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.58 % (3423597)CaDiCaL version: 2.1.3
% 5.43/1.58 % (3423597)Termination reason: Instruction limit
% 5.43/1.58 % (3423597)Termination phase: Saturation
% 5.43/1.58 % (3423597)Time elapsed: 0.024 s
% 5.43/1.58 % (3423597)Peak memory usage: 89 MB
% 5.43/1.58 % (3423597)Instructions burned: 89 (million)
% 5.43/1.58 % (3423598)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1799702062:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.43/1.58 % (3423598)Instruction limit reached!
% 5.43/1.58 % (3423598)------------------------------
% 5.43/1.58 % (3423598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.43/1.58 % (3423598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.58 % (3423598)CaDiCaL version: 2.1.3
% 5.43/1.58 % (3423598)Termination reason: Instruction limit
% 5.43/1.58 % (3423598)Termination phase: Naming
% 5.43/1.58 % (3423598)Time elapsed: 0.002 s
% 5.43/1.58 % (3423598)Peak memory usage: 86 MB
% 5.43/1.58 % (3423598)Instructions burned: 2 (million)
% 5.43/1.58 % (3423603)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3628323881:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.43/1.58 % (3423602)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=105541734:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.43/1.58 % (3423603)Instruction limit reached!
% 5.43/1.58 % (3423603)------------------------------
% 5.43/1.58 % (3423603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.43/1.58 % (3423603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.58 % (3423603)CaDiCaL version: 2.1.3
% 5.43/1.58 % (3423603)Termination reason: Instruction limit
% 5.43/1.58 % (3423603)Termination phase: Property scanning
% 5.43/1.58 % (3423603)Time elapsed: 0.003 s
% 5.43/1.58 % (3423603)Peak memory usage: 86 MB
% 5.43/1.58 % (3423603)Instructions burned: 4 (million)
% 5.43/1.58 % (3423605)lrs+10_1_thi=all:si=on:fd=off:random_seed=760880152:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.43/1.58 % (3423604)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1228041074:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.43/1.58 % (3423609)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4030070715:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.43/1.58 % (3423609)Instruction limit reached!
% 5.43/1.58 % (3423609)------------------------------
% 5.43/1.58 % (3423609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.43/1.58 % (3423609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.58 % (3423609)CaDiCaL version: 2.1.3
% 5.43/1.58 % (3423609)Termination reason: Instruction limit
% 5.43/1.58 % (3423609)Termination phase: Naming
% 5.43/1.58 % (3423609)Time elapsed: 0.001 s
% 5.43/1.58 % (3423609)Peak memory usage: 86 MB
% 5.43/1.58 % (3423609)Instructions burned: 2 (million)
% 5.43/1.58 % (3423608)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=1129363918:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 5.43/1.58 % (3423608)Instruction limit reached!
% 5.43/1.58 % (3423608)------------------------------
% 5.43/1.58 % (3423608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.43/1.58 % (3423608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.58 % (3423608)CaDiCaL version: 2.1.3
% 5.43/1.58 % (3423608)Termination reason: Instruction limit
% 5.43/1.58 % (3423608)Termination phase: Property scanning
% 7.52/1.80 % (3423608)Time elapsed: 0.005 s
% 7.52/1.80 % (3423608)Peak memory usage: 87 MB
% 7.52/1.80 % (3423608)Instructions burned: 9 (million)
% 7.52/1.80 % (3423605)Instruction limit reached!
% 7.52/1.80 % (3423605)------------------------------
% 7.52/1.80 % (3423605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.52/1.80 % (3423605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.80 % (3423605)CaDiCaL version: 2.1.3
% 7.52/1.80 % (3423605)Termination reason: Instruction limit
% 7.52/1.80 % (3423605)Termination phase: Saturation
% 7.52/1.80 % (3423605)Time elapsed: 0.063 s
% 7.52/1.80 % (3423605)Peak memory usage: 117 MB
% 7.52/1.80 % (3423605)Instructions burned: 54 (million)
% 7.52/1.80 % (3423604)Instruction limit reached!
% 7.52/1.80 % (3423604)------------------------------
% 7.52/1.80 % (3423604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.52/1.80 % (3423604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.80 % (3423604)CaDiCaL version: 2.1.3
% 7.52/1.80 % (3423604)Termination reason: Instruction limit
% 7.52/1.80 % (3423604)Termination phase: Saturation
% 7.52/1.80 % (3423604)Time elapsed: 0.089 s
% 7.52/1.80 % (3423604)Peak memory usage: 134 MB
% 7.52/1.80 % (3423604)Instructions burned: 67 (million)
% 7.52/1.80 % (3423611)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1412595985:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 7.52/1.80 % (3423611)Instruction limit reached!
% 7.52/1.80 % (3423611)------------------------------
% 7.52/1.80 % (3423611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.52/1.80 % (3423611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.80 % (3423611)CaDiCaL version: 2.1.3
% 7.52/1.80 % (3423611)Termination reason: Instruction limit
% 7.52/1.80 % (3423611)Termination phase: Naming
% 7.52/1.80 % (3423611)Time elapsed: 0.002 s
% 7.52/1.80 % (3423611)Peak memory usage: 86 MB
% 7.52/1.80 % (3423611)Instructions burned: 2 (million)
% 7.52/1.80 % (3423602)Instruction limit reached!
% 7.52/1.80 % (3423602)------------------------------
% 7.52/1.80 % (3423602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.52/1.80 % (3423602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.80 % (3423602)CaDiCaL version: 2.1.3
% 7.52/1.80 % (3423602)Termination reason: Instruction limit
% 7.52/1.80 % (3423602)Termination phase: Saturation
% 7.52/1.80 % (3423602)Time elapsed: 0.127 s
% 7.52/1.80 % (3423602)Peak memory usage: 91 MB
% 7.52/1.80 % (3423602)Instructions burned: 181 (million)
% 7.52/1.80 % (3423614)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=364194824:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 7.52/1.80 % (3423618)dis+10_1_si=on:random_seed=4291235051:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 7.52/1.80 % (3423618)Instruction limit reached!
% 7.52/1.80 % (3423618)------------------------------
% 7.52/1.80 % (3423618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.52/1.80 % (3423618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.80 % (3423618)CaDiCaL version: 2.1.3
% 7.52/1.80 % (3423618)Termination reason: Instruction limit
% 7.52/1.80 % (3423618)Termination phase: Saturation
% 7.52/1.80 % (3423618)Time elapsed: 0.006 s
% 7.52/1.80 % (3423618)Peak memory usage: 88 MB
% 7.52/1.80 % (3423618)Instructions burned: 10 (million)
% 7.52/1.80 % (3423621)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3966452169:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi)
% 7.52/1.80 % (3423620)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3515544174:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 7.52/1.80 % (3423620)Refutation not found, incomplete strategy
% 7.52/1.80 % (3423620)------------------------------
% 7.52/1.80 % (3423620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.52/1.80 % (3423620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.80 % (3423620)CaDiCaL version: 2.1.3
% 7.52/1.80 % (3423620)Termination reason: Refutation not found, incomplete strategy
% 7.52/1.80 % (3423620)Time elapsed: 0.015 s
% 7.52/1.80 % (3423620)Peak memory usage: 89 MB
% 7.52/1.80 % (3423620)Instructions burned: 24 (million)
% 7.52/1.80 % (3423621)Instruction limit reached!
% 10.07/2.05 % (3423621)------------------------------
% 10.07/2.05 % (3423621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/2.05 % (3423621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/2.05 % (3423621)CaDiCaL version: 2.1.3
% 10.07/2.05 % (3423621)Termination reason: Instruction limit
% 10.07/2.05 % (3423621)Termination phase: Saturation
% 10.07/2.05 % (3423621)Time elapsed: 0.024 s
% 10.07/2.05 % (3423621)Peak memory usage: 89 MB
% 10.07/2.05 % (3423621)Instructions burned: 36 (million)
% 10.07/2.05 % (3423624)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3207781607:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 10.07/2.05 % (3423622)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=97359944:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 10.07/2.05 % (3423625)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3277025447:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 10.07/2.05 % (3423614)Instruction limit reached!
% 10.07/2.05 % (3423614)------------------------------
% 10.07/2.05 % (3423614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/2.05 % (3423614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/2.05 % (3423614)CaDiCaL version: 2.1.3
% 10.07/2.05 % (3423614)Termination reason: Instruction limit
% 10.07/2.05 % (3423614)Termination phase: Saturation
% 10.07/2.05 % (3423614)Time elapsed: 0.107 s
% 10.07/2.05 % (3423614)Peak memory usage: 117 MB
% 10.07/2.05 % (3423614)Instructions burned: 128 (million)
% 10.07/2.05 % (3423622)Instruction limit reached!
% 10.07/2.05 % (3423622)------------------------------
% 10.07/2.05 % (3423622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/2.05 % (3423622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/2.05 % (3423622)CaDiCaL version: 2.1.3
% 10.07/2.05 % (3423622)Termination reason: Instruction limit
% 10.07/2.05 % (3423622)Termination phase: Preprocessing 3
% 10.07/2.05 % (3423622)Time elapsed: 0.002 s
% 10.07/2.05 % (3423622)Peak memory usage: 86 MB
% 10.07/2.05 % (3423622)Instructions burned: 2 (million)
% 10.07/2.05 % (3423624)Instruction limit reached!
% 10.07/2.05 % (3423624)------------------------------
% 10.07/2.05 % (3423624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/2.05 % (3423624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/2.05 % (3423624)CaDiCaL version: 2.1.3
% 10.07/2.05 % (3423624)Termination reason: Instruction limit
% 10.07/2.05 % (3423624)Termination phase: Saturation
% 10.07/2.05 % (3423624)Time elapsed: 0.005 s
% 10.07/2.05 % (3423624)Peak memory usage: 88 MB
% 10.07/2.05 % (3423624)Instructions burned: 8 (million)
% 10.07/2.05 % (3423628)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=143961413:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 10.07/2.05 % (3423628)Instruction limit reached!
% 10.07/2.05 % (3423628)------------------------------
% 10.07/2.05 % (3423628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/2.05 % (3423628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/2.05 % (3423628)CaDiCaL version: 2.1.3
% 10.07/2.05 % (3423628)Termination reason: Instruction limit
% 10.07/2.05 % (3423628)Termination phase: Saturation
% 10.07/2.05 % (3423628)Time elapsed: 0.024 s
% 10.07/2.05 % (3423628)Peak memory usage: 112 MB
% 10.07/2.05 % (3423628)Instructions burned: 15 (million)
% 10.07/2.05 % (3423631)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3080352283:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 10.07/2.05 % (3423636)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2509529756:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 10.07/2.05 % (3423635)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3931453155:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.07/2.05 % (3423637)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=717564621:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 10.07/2.05 % (3423635)Instruction limit reached!
% 10.07/2.05 % (3423635)------------------------------
% 11.12/2.25 % (3423635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.12/2.25 % (3423635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.12/2.25 % (3423635)CaDiCaL version: 2.1.3
% 11.12/2.25 % (3423635)Termination reason: Instruction limit
% 11.12/2.25 % (3423635)Termination phase: Saturation
% 11.12/2.25 % (3423635)Time elapsed: 0.008 s
% 11.12/2.25 % (3423635)Peak memory usage: 88 MB
% 11.12/2.25 % (3423635)Instructions burned: 11 (million)
% 11.12/2.25 % (3423637)Instruction limit reached!
% 11.12/2.25 % (3423637)------------------------------
% 11.12/2.25 % (3423637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.12/2.25 % (3423637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.12/2.25 % (3423637)CaDiCaL version: 2.1.3
% 11.12/2.25 % (3423637)Termination reason: Instruction limit
% 11.12/2.25 % (3423637)Termination phase: Saturation
% 11.12/2.25 % (3423637)Time elapsed: 0.055 s
% 11.12/2.25 % (3423637)Peak memory usage: 90 MB
% 11.12/2.25 % (3423637)Instructions burned: 75 (million)
% 11.12/2.25 % (3423639)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=461312515:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 11.12/2.25 % (3423620)------------------------------
% 11.12/2.25 % (3423620)------------------------------
% 11.12/2.25 % (3423625)Instruction limit reached!
% 11.12/2.25 % (3423625)------------------------------
% 11.12/2.25 % (3423625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.12/2.25 % (3423625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.12/2.25 % (3423625)CaDiCaL version: 2.1.3
% 11.12/2.25 % (3423625)Termination reason: Instruction limit
% 11.12/2.25 % (3423625)Termination phase: Saturation
% 11.12/2.25 % (3423625)Time elapsed: 0.235 s
% 11.12/2.25 % (3423625)Peak memory usage: 93 MB
% 11.12/2.25 % (3423625)Instructions burned: 371 (million)
% 11.12/2.25 % (3423636)Instruction limit reached!
% 11.12/2.25 % (3423636)------------------------------
% 11.12/2.25 % (3423636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.12/2.25 % (3423636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.12/2.25 % (3423636)CaDiCaL version: 2.1.3
% 11.12/2.25 % (3423636)Termination reason: Instruction limit
% 11.12/2.25 % (3423636)Termination phase: Saturation
% 11.12/2.25 % (3423636)Time elapsed: 0.091 s
% 11.12/2.25 % (3423636)Peak memory usage: 133 MB
% 11.12/2.25 % (3423636)Instructions burned: 72 (million)
% 11.12/2.25 % (3423631)Instruction limit reached!
% 11.12/2.25 % (3423631)------------------------------
% 11.12/2.25 % (3423631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.12/2.25 % (3423631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.12/2.25 % (3423631)CaDiCaL version: 2.1.3
% 11.12/2.25 % (3423631)Termination reason: Instruction limit
% 11.12/2.25 % (3423631)Termination phase: Saturation
% 11.12/2.25 % (3423631)Time elapsed: 0.163 s
% 11.12/2.25 % (3423631)Peak memory usage: 116 MB
% 11.12/2.25 % (3423631)Instructions burned: 226 (million)
% 11.12/2.25 % (3423644)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2449172271:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi)
% 11.12/2.25 % (3423639)Instruction limit reached!
% 11.12/2.25 % (3423639)------------------------------
% 11.12/2.25 % (3423639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.12/2.25 % (3423639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.12/2.25 % (3423639)CaDiCaL version: 2.1.3
% 11.12/2.25 % (3423639)Termination reason: Instruction limit
% 11.12/2.25 % (3423639)Termination phase: Saturation
% 11.12/2.25 % (3423639)Time elapsed: 0.097 s
% 11.12/2.25 % (3423639)Peak memory usage: 91 MB
% 11.12/2.25 % (3423639)Instructions burned: 296 (million)
% 11.12/2.25 % (3423646)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3527988339:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 11.12/2.25 % (3423647)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2630602890:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 11.12/2.25 % (3423648)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=4101869321:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 11.12/2.25 % (3423644)Instruction limit reached!
% 11.12/2.25 % (3423644)------------------------------
% 11.99/2.59 % (3423644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.99/2.59 % (3423644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.59 % (3423644)CaDiCaL version: 2.1.3
% 11.99/2.59 % (3423644)Termination reason: Instruction limit
% 11.99/2.59 % (3423644)Termination phase: Saturation
% 11.99/2.59 % (3423644)Time elapsed: 0.082 s
% 11.99/2.59 % (3423644)Peak memory usage: 113 MB
% 11.99/2.59 % (3423644)Instructions burned: 132 (million)
% 11.99/2.59 % (3423649)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1043138660:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi)
% 11.99/2.59 % (3423647)Instruction limit reached!
% 11.99/2.59 % (3423647)------------------------------
% 11.99/2.59 % (3423647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.99/2.59 % (3423647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.59 % (3423647)CaDiCaL version: 2.1.3
% 11.99/2.59 % (3423647)Termination reason: Instruction limit
% 11.99/2.59 % (3423647)Termination phase: Saturation
% 11.99/2.59 % (3423647)Time elapsed: 0.068 s
% 11.99/2.59 % (3423647)Peak memory usage: 134 MB
% 11.99/2.59 % (3423647)Instructions burned: 40 (million)
% 11.99/2.59 % (3423652)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=2186363522:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 11.99/2.59 % (3423650)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2777521892:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 11.99/2.59 % (3423646)Instruction limit reached!
% 11.99/2.59 % (3423646)------------------------------
% 11.99/2.59 % (3423646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.99/2.59 % (3423646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.59 % (3423646)CaDiCaL version: 2.1.3
% 11.99/2.59 % (3423646)Termination reason: Instruction limit
% 11.99/2.59 % (3423646)Termination phase: Saturation
% 11.99/2.59 % (3423646)Time elapsed: 0.129 s
% 11.99/2.59 % (3423646)Peak memory usage: 133 MB
% 11.99/2.59 % (3423646)Instructions burned: 131 (million)
% 11.99/2.59 % (3423652)Instruction limit reached!
% 11.99/2.59 % (3423652)------------------------------
% 11.99/2.59 % (3423652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.99/2.59 % (3423652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.59 % (3423652)CaDiCaL version: 2.1.3
% 11.99/2.59 % (3423652)Termination reason: Instruction limit
% 11.99/2.59 % (3423652)Termination phase: Saturation
% 11.99/2.59 % (3423652)Time elapsed: 0.098 s
% 11.99/2.59 % (3423652)Peak memory usage: 117 MB
% 11.99/2.59 % (3423652)Instructions burned: 261 (million)
% 11.99/2.59 % (3423650)Instruction limit reached!
% 11.99/2.59 % (3423650)------------------------------
% 11.99/2.59 % (3423650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.99/2.59 % (3423650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.59 % (3423650)CaDiCaL version: 2.1.3
% 11.99/2.59 % (3423650)Termination reason: Instruction limit
% 11.99/2.59 % (3423650)Termination phase: Saturation
% 11.99/2.59 % (3423650)Time elapsed: 0.107 s
% 11.99/2.59 % (3423650)Peak memory usage: 118 MB
% 11.99/2.59 % (3423650)Instructions burned: 131 (million)
% 11.99/2.59 % (3423648)Instruction limit reached!
% 11.99/2.59 % (3423648)------------------------------
% 11.99/2.59 % (3423648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.99/2.59 % (3423648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.59 % (3423648)CaDiCaL version: 2.1.3
% 11.99/2.59 % (3423648)Termination reason: Instruction limit
% 11.99/2.59 % (3423648)Termination phase: Saturation
% 11.99/2.59 % (3423648)Time elapsed: 0.168 s
% 11.99/2.59 % (3423648)Peak memory usage: 92 MB
% 11.99/2.59 % (3423648)Instructions burned: 308 (million)
% 11.99/2.59 % (3423657)dis+10_1_si=on:random_seed=818169887:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi)
% 11.99/2.59 % (3423660)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2394710201:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 11.99/2.59 % (3423662)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=4060874247:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 12.98/2.63 % (3423661)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=753289903:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi)
% 12.98/2.63 % (3423662)Instruction limit reached!
% 12.98/2.63 % (3423662)------------------------------
% 12.98/2.63 % (3423662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.98/2.63 % (3423662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.98/2.63 % (3423662)CaDiCaL version: 2.1.3
% 12.98/2.63 % (3423662)Termination reason: Instruction limit
% 12.98/2.63 % (3423662)Termination phase: Saturation
% 12.98/2.63 % (3423662)Time elapsed: 0.036 s
% 12.98/2.63 % (3423662)Peak memory usage: 116 MB
% 12.98/2.63 % (3423662)Instructions burned: 67 (million)
% 12.98/2.63 % (3423664)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=2538750214:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi)
% 12.98/2.63 % (3423663)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3896868634:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi)
% 12.98/2.63 % (3423661)Instruction limit reached!
% 12.98/2.63 % (3423661)------------------------------
% 12.98/2.63 % (3423661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.98/2.63 % (3423661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.98/2.63 % (3423661)CaDiCaL version: 2.1.3
% 12.98/2.63 % (3423661)Termination reason: Instruction limit
% 12.98/2.63 % (3423661)Termination phase: Saturation
% 12.98/2.63 % (3423661)Time elapsed: 0.098 s
% 12.98/2.63 % (3423661)Peak memory usage: 90 MB
% 12.98/2.63 % (3423661)Instructions burned: 142 (million)
% 12.98/2.63 % (3423663)Instruction limit reached!
% 12.98/2.63 % (3423663)------------------------------
% 12.98/2.63 % (3423663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.98/2.63 % (3423663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.98/2.63 % (3423663)CaDiCaL version: 2.1.3
% 12.98/2.63 % (3423663)Termination reason: Instruction limit
% 12.98/2.63 % (3423663)Termination phase: Saturation
% 12.98/2.63 % (3423663)Time elapsed: 0.081 s
% 12.98/2.63 % (3423663)Peak memory usage: 89 MB
% 12.98/2.63 % (3423663)Instructions burned: 122 (million)
% 12.98/2.63 % (3423669)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=1678831044:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi)
% 12.98/2.63 % (3423664)Instruction limit reached!
% 12.98/2.63 % (3423664)------------------------------
% 12.98/2.63 % (3423664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.98/2.63 % (3423664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.98/2.63 % (3423664)CaDiCaL version: 2.1.3
% 12.98/2.63 % (3423664)Termination reason: Instruction limit
% 12.98/2.63 % (3423664)Termination phase: Saturation
% 12.98/2.63 % (3423664)Time elapsed: 0.102 s
% 12.98/2.63 % (3423664)Peak memory usage: 117 MB
% 12.98/2.63 % (3423664)Instructions burned: 128 (million)
% 12.98/2.63 % (3423660)Instruction limit reached!
% 12.98/2.63 % (3423660)------------------------------
% 12.98/2.63 % (3423660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.98/2.63 % (3423660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.98/2.63 % (3423660)CaDiCaL version: 2.1.3
% 12.98/2.63 % (3423660)Termination reason: Instruction limit
% 12.98/2.63 % (3423660)Termination phase: Saturation
% 12.98/2.63 % (3423660)Time elapsed: 0.235 s
% 12.98/2.63 % (3423660)Peak memory usage: 94 MB
% 12.98/2.63 % (3423660)Instructions burned: 384 (million)
% 12.98/2.63 % (3423669)Instruction limit reached!
% 12.98/2.63 % (3423669)------------------------------
% 12.98/2.63 % (3423669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.98/2.63 % (3423669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.98/2.63 % (3423669)CaDiCaL version: 2.1.3
% 12.98/2.63 % (3423669)Termination reason: Instruction limit
% 12.98/2.63 % (3423669)Termination phase: Saturation
% 12.98/2.63 % (3423669)Time elapsed: 0.027 s
% 12.98/2.63 % (3423669)Peak memory usage: 115 MB
% 12.98/2.63 % (3423669)Instructions burned: 41 (million)
% 12.98/2.63 % (3423649)Instruction limit reached!
% 12.98/2.63 % (3423649)------------------------------
% 12.98/2.63 % (3423649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.98/2.63 % (3423649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.98/2.63 % (3423649)CaDiCaL version: 2.1.3
% 12.98/2.63 % (3423649)Termination reason: Instruction limit
% 12.98/2.63 % (3423649)Termination phase: Saturation
% 12.98/2.63 % (3423649)Time elapsed: 0.441 s
% 12.98/2.63 % (3423649)Peak memory usage: 137 MB
% 12.98/2.63 % (3423649)Instructions burned: 598 (million)
% 12.98/2.63 % (3423672)dis+1010_1_to=kbo:si=on:random_seed=1303658649:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi)
% 12.98/2.63 % (3423677)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1765291571:i=349:rtra=on_2984 on theBenchmark for (2984ds/349Mi)
% 12.98/2.63 % (3423674)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1282036568:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi)
% 12.98/2.63 % (3423672)First to succeed.
% 12.98/2.63 % (3423675)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3081383832:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi)
% 12.98/2.63 % (3423672)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3423487"
% 12.98/2.63 % (3423676)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2553372829:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi)
% 12.98/2.63 % (3423678)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=199403211:st=2:i=295:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/295Mi)
% 12.98/2.63 % (3423677)Instruction limit reached!
% 12.98/2.63 % (3423677)------------------------------
% 12.98/2.63 % (3423677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.98/2.63 % (3423677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.98/2.63 % (3423677)CaDiCaL version: 2.1.3
% 12.98/2.63 % (3423677)Termination reason: Instruction limit
% 12.98/2.63 % (3423677)Termination phase: Saturation
% 12.98/2.63 % (3423677)Time elapsed: 0.130 s
% 12.98/2.63 % (3423677)Peak memory usage: 118 MB
% 12.98/2.63 % (3423677)Instructions burned: 350 (million)
% 12.98/2.63 % (3423674)Instruction limit reached!
% 12.98/2.63 % (3423674)------------------------------
% 12.98/2.63 % (3423674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.98/2.63 % (3423674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.98/2.63 % (3423674)CaDiCaL version: 2.1.3
% 12.98/2.63 % (3423674)Termination reason: Instruction limit
% 12.98/2.63 % (3423674)Termination phase: Saturation
% 12.98/2.63 % (3423674)Time elapsed: 0.176 s
% 12.98/2.63 % (3423674)Peak memory usage: 116 MB
% 12.98/2.63 % (3423674)Instructions burned: 331 (million)
% 12.98/2.63 % (3423657)Instruction limit reached!
% 12.98/2.63 % (3423657)------------------------------
% 12.98/2.63 % (3423657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.98/2.63 % (3423657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.98/2.63 % (3423657)CaDiCaL version: 2.1.3
% 12.98/2.63 % (3423657)Termination reason: Instruction limit
% 12.98/2.63 % (3423657)Termination phase: Saturation
% 12.98/2.63 % (3423657)Time elapsed: 0.541 s
% 12.98/2.63 % (3423657)Peak memory usage: 93 MB
% 12.98/2.63 % (3423657)Instructions burned: 1001 (million)
% 12.98/2.63 % (3423676)Instruction limit reached!
% 12.98/2.63 % (3423676)------------------------------
% 12.98/2.63 % (3423676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.98/2.63 % (3423676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.98/2.63 % (3423676)CaDiCaL version: 2.1.3
% 12.98/2.63 % (3423676)Termination reason: Instruction limit
% 12.98/2.63 % (3423676)Termination phase: Saturation
% 12.98/2.63 % (3423676)Time elapsed: 0.143 s
% 12.98/2.63 % (3423676)Peak memory usage: 135 MB
% 12.98/2.63 % (3423676)Instructions burned: 215 (million)
% 12.98/2.63 % (3423685)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=296423813:i=328:kws=inv_frequency:nm=20:rtra=on_2981 on theBenchmark for (2981ds/328Mi)
% 12.98/2.63 % (3423678)Instruction limit reached!
% 12.98/2.63 % (3423678)------------------------------
% 12.98/2.63 % (3423678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.98/2.63 % (3423678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.98/2.63 % (3423678)CaDiCaL version: 2.1.3
% 12.98/2.63 % (3423678)Termination reason: Instruction limit
% 12.98/2.63 % (3423678)Termination phase: Saturation
% 12.98/2.63 % (3423678)Time elapsed: 0.170 s
% 12.98/2.63 % (3423678)Peak memory usage: 90 MB
% 12.98/2.63 % (3423678)Instructions burned: 295 (million)
% 12.98/2.63 % (3423672)Refutation found. Thanks to Tanya!
% 12.98/2.63 % SZS status Theorem for theBenchmark
% 12.98/2.63 % SZS output start Proof for theBenchmark
% See solution above
% 14.50/2.82 % (3423672)------------------------------
% 14.50/2.82 % (3423672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.50/2.82 % (3423672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.50/2.82 % (3423672)CaDiCaL version: 2.1.3
% 14.50/2.82 % (3423672)Termination reason: Refutation
% 14.50/2.82 % (3423672)Time elapsed: 0.073 s
% 14.50/2.82 % (3423672)Peak memory usage: 92 MB
% 14.50/2.82 % (3423672)Instructions burned: 135 (million)
% 14.50/2.82 % (3423672)------------------------------
% 14.50/2.82 % (3423672)------------------------------
% 14.50/2.82 % (3423487)Success in time 1.964 s
% 14.50/2.82 % Vampire exiting
%------------------------------------------------------------------------------