%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW646_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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:02 PM UTC 2026
% Result : Theorem 38.42s 6.62s
% Output : Refutation 40.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 79
% Syntax : Number of formulae : 342 ( 130 unt; 0 typ; 63 def)
% Number of atoms : 1185 ( 261 equ)
% Maximal formula atoms : 39 ( 3 avg)
% Number of connectives : 1381 ( 538 ~; 430 |; 292 &)
% ( 46 <=>; 75 =>; 0 <=; 0 <~>)
% Maximal formula depth : 54 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 615 ( 221 atm; 0 fun; 253 num; 141 var)
% Number of types : 9 ( 7 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 56 ( 52 usr; 34 prp; 0-5 aty)
% Number of functors : 102 ( 98 usr; 63 con; 0-6 aty)
% Number of variables : 442 ( 0 sgn 382 !; 60 ?; 442 :)
% 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,
map_int_int: $tType ).
tff(type_def_10,type,
sudoku_chunks1: $tType ).
tff(type_def_11,type,
array_int: $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_12,type,
map: ( ty * ty ) > ty ).
tff(func_def_13,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_14,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_15,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_17,type,
t2tb: map_int_int > uni ).
tff(func_def_18,type,
tb2t: uni > map_int_int ).
tff(func_def_19,type,
t2tb1: $int > uni ).
tff(func_def_20,type,
tb2t1: uni > $int ).
tff(func_def_22,type,
array: ty > ty ).
tff(func_def_23,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(func_def_24,type,
length1: ( ty * uni ) > $int ).
tff(func_def_25,type,
elts: ( ty * uni ) > uni ).
tff(func_def_26,type,
get2: ( ty * uni * $int ) > uni ).
tff(func_def_27,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_28,type,
make1: ( ty * $int * uni ) > uni ).
tff(func_def_29,type,
sudoku_chunks: ty ).
tff(func_def_30,type,
mk_sudoku_chunks1: ( array_int * array_int * array_int * array_int * array_int * array_int ) > sudoku_chunks1 ).
tff(func_def_31,type,
column_start1: sudoku_chunks1 > array_int ).
tff(func_def_32,type,
column_offsets1: sudoku_chunks1 > array_int ).
tff(func_def_33,type,
row_start1: sudoku_chunks1 > array_int ).
tff(func_def_34,type,
row_offsets1: sudoku_chunks1 > array_int ).
tff(func_def_35,type,
square_start1: sudoku_chunks1 > array_int ).
tff(func_def_36,type,
square_offsets1: sudoku_chunks1 > array_int ).
tff(func_def_37,type,
t2tb2: array_int > uni ).
tff(func_def_38,type,
tb2t2: uni > array_int ).
tff(func_def_41,type,
sK1: ( array_int * array_int ) > $int ).
tff(func_def_42,type,
sK2: ( array_int * array_int ) > $int ).
tff(func_def_43,type,
sK3: ( $int * map_int_int * sudoku_chunks1 ) > $int ).
tff(func_def_44,type,
sK4: ( array_int * array_int ) > $int ).
tff(func_def_45,type,
sK5: ( array_int * array_int ) > $int ).
tff(func_def_46,type,
sK6: ( array_int * array_int ) > $int ).
tff(func_def_47,type,
sK7: ( map_int_int * map_int_int ) > $int ).
tff(func_def_48,type,
sK8: ( map_int_int * sudoku_chunks1 ) > $int ).
tff(func_def_49,type,
sK9: ( $int * map_int_int * map_int_int * $int ) > $int ).
tff(func_def_50,type,
sK10: map_int_int ).
tff(func_def_51,type,
sK11: $int ).
tff(func_def_52,type,
sK12: $int ).
tff(func_def_53,type,
sK13: $int ).
tff(func_def_54,type,
sK14: $int ).
tff(func_def_55,type,
sK15: map_int_int ).
tff(func_def_56,type,
sK16: map_int_int ).
tff(func_def_57,type,
sK17: $int ).
tff(func_def_58,type,
sK18: $int ).
tff(func_def_59,type,
sK19: $int ).
tff(func_def_60,type,
sK20: map_int_int ).
tff(func_def_61,type,
sK21: $int ).
tff(func_def_62,type,
sK22: map_int_int ).
tff(func_def_63,type,
sK23: map_int_int ).
tff(func_def_64,type,
sK24: map_int_int ).
tff(func_def_65,type,
sK25: map_int_int ).
tff(func_def_66,type,
sK26: $int ).
tff(func_def_67,type,
sK27: map_int_int ).
tff(func_def_68,type,
sK28: ( map_int_int * array_int * array_int * $int ) > $int ).
tff(func_def_69,type,
sK29: ( map_int_int * array_int * array_int * $int ) > $int ).
tff(func_def_70,type,
sK30: ( map_int_int * $int ) > $int ).
tff(func_def_71,type,
sK31: map_int_int > $int ).
tff(func_def_72,type,
sF32: uni ).
tff(func_def_73,type,
sF33: uni ).
tff(func_def_74,type,
sF34: array_int ).
tff(func_def_75,type,
sF35: uni ).
tff(func_def_76,type,
sF36: uni ).
tff(func_def_77,type,
sF37: array_int ).
tff(func_def_78,type,
sF38: uni ).
tff(func_def_79,type,
sF39: uni ).
tff(func_def_80,type,
sF40: array_int ).
tff(func_def_81,type,
sF41: uni ).
tff(func_def_82,type,
sF42: uni ).
tff(func_def_83,type,
sF43: array_int ).
tff(func_def_84,type,
sF44: uni ).
tff(func_def_85,type,
sF45: uni ).
tff(func_def_86,type,
sF46: array_int ).
tff(func_def_87,type,
sF47: uni ).
tff(func_def_88,type,
sF48: uni ).
tff(func_def_89,type,
sF49: array_int ).
tff(func_def_90,type,
sF50: sudoku_chunks1 ).
tff(func_def_91,type,
sF51: uni ).
tff(func_def_92,type,
sF52: uni ).
tff(func_def_93,type,
sF53: uni ).
tff(func_def_94,type,
sF54: $int ).
tff(func_def_95,type,
sF55: uni ).
tff(func_def_96,type,
sF56: uni ).
tff(func_def_97,type,
sF57: map_int_int ).
tff(func_def_98,type,
sF58: uni ).
tff(func_def_99,type,
sF59: uni ).
tff(func_def_100,type,
sF60: map_int_int ).
tff(func_def_101,type,
sF61: uni ).
tff(func_def_102,type,
sF62: uni ).
tff(func_def_103,type,
sF63: map_int_int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
is_index1: $int > $o ).
tff(pred_def_5,type,
valid_values1: map_int_int > $o ).
tff(pred_def_6,type,
grid_eq_sub1: ( map_int_int * map_int_int * $int * $int ) > $o ).
tff(pred_def_7,type,
chunk_valid_indexes1: ( array_int * array_int ) > $o ).
tff(pred_def_8,type,
disjoint_chunks1: ( array_int * array_int ) > $o ).
tff(pred_def_9,type,
well_formed_sudoku1: sudoku_chunks1 > $o ).
tff(pred_def_10,type,
valid_chunk1: ( map_int_int * $int * array_int * array_int ) > $o ).
tff(pred_def_11,type,
valid_column1: ( sudoku_chunks1 * map_int_int * $int ) > $o ).
tff(pred_def_12,type,
valid_row1: ( sudoku_chunks1 * map_int_int * $int ) > $o ).
tff(pred_def_13,type,
valid_square1: ( sudoku_chunks1 * map_int_int * $int ) > $o ).
tff(pred_def_14,type,
valid1: ( sudoku_chunks1 * map_int_int ) > $o ).
tff(pred_def_15,type,
full1: map_int_int > $o ).
tff(pred_def_16,type,
included1: ( map_int_int * map_int_int ) > $o ).
tff(pred_def_17,type,
is_solution_for1: ( sudoku_chunks1 * map_int_int * map_int_int ) > $o ).
tff(pred_def_18,type,
valid_chunk_up_to1: ( map_int_int * $int * array_int * array_int * $int ) > $o ).
tff(pred_def_19,type,
valid_up_to1: ( sudoku_chunks1 * map_int_int * $int ) > $o ).
tff(pred_def_20,type,
full_up_to1: ( map_int_int * $int ) > $o ).
tff(pred_def_21,type,
sP0: ( array_int * array_int ) > $o ).
tff(f11,axiom,
! [X4: uni,X0: ty,X2: uni,X3: uni,X5: uni,X1: ty] :
( sort1(X1,X5)
=> ( ( X3 = X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = X5 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',select_eq) ).
tff(f12,axiom,
! [X1: ty,X2: uni,X4: uni,X3: uni,X0: ty] :
( sort1(X0,X3)
=> ( sort1(X0,X4)
=> ! [X5: uni] :
( ( X3 != X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = get(X1,X0,X2,X4) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',select_neq) ).
tff(f15,axiom,
! [X0: $int] :
( ( $less(X0,81)
& $lesseq(0,X0) )
<=> is_index1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',is_index_def) ).
tff(f18,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR) ).
tff(f19,axiom,
! [X0: $int] : sort1(int,t2tb1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort1) ).
tff(f20,axiom,
! [X0: $int] : ( tb2t1(t2tb1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL1) ).
tff(f21,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR1) ).
tff(f23,axiom,
! [X3: $int,X0: map_int_int,X1: map_int_int,X2: $int] :
( ! [X4: $int] :
( ( $less(X4,X3)
& $lesseq(X2,X4) )
=> ( tb2t1(get(int,int,t2tb(X0),t2tb1(X4))) = tb2t1(get(int,int,t2tb(X1),t2tb1(X4))) ) )
<=> grid_eq_sub1(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',grid_eq_sub_def) ).
tff(f36,axiom,
! [X1: array_int,X3: array_int,X5: array_int,X2: array_int,X4: array_int,X0: array_int] : ( column_start1(mk_sudoku_chunks1(X0,X1,X2,X3,X4,X5)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',column_start_def1) ).
tff(f37,axiom,
! [X3: array_int,X5: array_int,X4: array_int,X2: array_int,X0: array_int,X1: array_int] : ( column_offsets1(mk_sudoku_chunks1(X0,X1,X2,X3,X4,X5)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',column_offsets_def1) ).
tff(f50,axiom,
! [X0: sudoku_chunks1,X1: map_int_int,X2: $int] :
( valid_chunk1(X1,X2,column_start1(X0),column_offsets1(X0))
<=> valid_column1(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',valid_column_def) ).
tff(f53,axiom,
! [X1: map_int_int,X0: sudoku_chunks1] :
( valid1(X0,X1)
<=> ! [X2: $int] :
( is_index1(X2)
=> ( valid_square1(X0,X1,X2)
& valid_column1(X0,X1,X2)
& valid_row1(X0,X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',valid_def) ).
tff(f55,axiom,
! [X1: map_int_int,X0: map_int_int] :
( ! [X2: $int] :
( ( $lesseq(tb2t1(get(int,int,t2tb(X0),t2tb1(X2))),9)
& is_index1(X2)
& $lesseq(1,tb2t1(get(int,int,t2tb(X0),t2tb1(X2)))) )
=> ( tb2t1(get(int,int,t2tb(X1),t2tb1(X2))) = tb2t1(get(int,int,t2tb(X0),t2tb1(X2))) ) )
<=> included1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',included_def) ).
tff(f56,axiom,
! [X1: map_int_int,X0: map_int_int] :
( included1(X0,X1)
=> ! [X3: array_int,X4: array_int,X2: $int] :
( ( is_index1(X2)
& valid_chunk1(X1,X2,X3,X4)
& chunk_valid_indexes1(X3,X4) )
=> valid_chunk1(X0,X2,X3,X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subset_valid_chunk) ).
tff(f68,conjecture,
! [X2: $int,X6: $int,X4: $int,X5: map_int_int,X10: $int,X9: map_int_int,X8: $int,X1: map_int_int,X14: $int,X0: $int,X13: map_int_int,X7: map_int_int,X12: $int,X11: map_int_int,X3: map_int_int] :
( ( $lesseq(0,X0)
& $lesseq(0,X8)
& ( X12 = 81 )
& well_formed_sudoku1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X4,t2tb(X5))),tb2t2(mk_array1(int,X6,t2tb(X7))),tb2t2(mk_array1(int,X8,t2tb(X9))),tb2t2(mk_array1(int,X10,t2tb(X11)))))
& $lesseq(0,X4)
& $lesseq(0,X12)
& valid_values1(X13)
& full_up_to1(X13,X14)
& $lesseq(0,X10)
& $lesseq(0,X14)
& valid_up_to1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X4,t2tb(X5))),tb2t2(mk_array1(int,X6,t2tb(X7))),tb2t2(mk_array1(int,X8,t2tb(X9))),tb2t2(mk_array1(int,X10,t2tb(X11)))),X13,X14)
& $lesseq(X14,81)
& $lesseq(0,X6)
& $lesseq(0,X2) )
=> ( ( X14 != 81 )
=> ( ( $less(X14,X12)
& $lesseq(0,X14) )
=> ( ( tb2t1(get(int,int,t2tb(X13),t2tb1(X14))) = 0 )
=> ( $lesseq(1,9)
=> ! [X16: $int,X15: map_int_int] :
( ( $lesseq(1,X16)
& $lesseq(X16,9) )
=> ( ( ! [X17: $int] :
( ( $less(X17,X16)
& $lesseq(1,X17) )
=> ! [X18: map_int_int] :
( ( included1(tb2t(set(int,int,t2tb(X13),t2tb1(X14),t2tb1(X17))),X18)
& full1(X18) )
=> ~ valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X4,t2tb(X5))),tb2t2(mk_array1(int,X6,t2tb(X7))),tb2t2(mk_array1(int,X8,t2tb(X9))),tb2t2(mk_array1(int,X10,t2tb(X11)))),X18) ) )
& grid_eq_sub1(X13,tb2t(set(int,int,t2tb(X15),t2tb1(X14),t2tb1(0))),0,81)
& full_up_to1(X15,X14) )
=> ( ( $lesseq(0,X14)
& $lesseq(0,X12)
& $less(X14,X12) )
=> ! [X19: map_int_int] :
( ( ( X19 = tb2t(set(int,int,t2tb(X15),t2tb1(X14),t2tb1(X16))) )
& $lesseq(0,X12) )
=> ( ( chunk_valid_indexes1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))))
& valid_values1(X19)
& ( X12 = 81 )
& is_index1(X14) )
=> ( ~ valid_chunk1(X19,X14,tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))))
=> ~ valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X4,t2tb(X5))),tb2t2(mk_array1(int,X6,t2tb(X7))),tb2t2(mk_array1(int,X8,t2tb(X9))),tb2t2(mk_array1(int,X10,t2tb(X11)))),tb2t(set(int,int,t2tb(X13),t2tb1(X14),t2tb1(X16)))) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_solve_aux) ).
tff(f69,negated_conjecture,
~ ! [X2: $int,X6: $int,X4: $int,X5: map_int_int,X10: $int,X9: map_int_int,X8: $int,X1: map_int_int,X14: $int,X0: $int,X13: map_int_int,X7: map_int_int,X12: $int,X11: map_int_int,X3: map_int_int] :
( ( $lesseq(0,X0)
& $lesseq(0,X8)
& ( X12 = 81 )
& well_formed_sudoku1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X4,t2tb(X5))),tb2t2(mk_array1(int,X6,t2tb(X7))),tb2t2(mk_array1(int,X8,t2tb(X9))),tb2t2(mk_array1(int,X10,t2tb(X11)))))
& $lesseq(0,X4)
& $lesseq(0,X12)
& valid_values1(X13)
& full_up_to1(X13,X14)
& $lesseq(0,X10)
& $lesseq(0,X14)
& valid_up_to1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X4,t2tb(X5))),tb2t2(mk_array1(int,X6,t2tb(X7))),tb2t2(mk_array1(int,X8,t2tb(X9))),tb2t2(mk_array1(int,X10,t2tb(X11)))),X13,X14)
& $lesseq(X14,81)
& $lesseq(0,X6)
& $lesseq(0,X2) )
=> ( ( X14 != 81 )
=> ( ( $less(X14,X12)
& $lesseq(0,X14) )
=> ( ( tb2t1(get(int,int,t2tb(X13),t2tb1(X14))) = 0 )
=> ( $lesseq(1,9)
=> ! [X16: $int,X15: map_int_int] :
( ( $lesseq(1,X16)
& $lesseq(X16,9) )
=> ( ( ! [X17: $int] :
( ( $less(X17,X16)
& $lesseq(1,X17) )
=> ! [X18: map_int_int] :
( ( included1(tb2t(set(int,int,t2tb(X13),t2tb1(X14),t2tb1(X17))),X18)
& full1(X18) )
=> ~ valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X4,t2tb(X5))),tb2t2(mk_array1(int,X6,t2tb(X7))),tb2t2(mk_array1(int,X8,t2tb(X9))),tb2t2(mk_array1(int,X10,t2tb(X11)))),X18) ) )
& grid_eq_sub1(X13,tb2t(set(int,int,t2tb(X15),t2tb1(X14),t2tb1(0))),0,81)
& full_up_to1(X15,X14) )
=> ( ( $lesseq(0,X14)
& $lesseq(0,X12)
& $less(X14,X12) )
=> ! [X19: map_int_int] :
( ( ( X19 = tb2t(set(int,int,t2tb(X15),t2tb1(X14),t2tb1(X16))) )
& $lesseq(0,X12) )
=> ( ( chunk_valid_indexes1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))))
& valid_values1(X19)
& ( X12 = 81 )
& is_index1(X14) )
=> ( ~ valid_chunk1(X19,X14,tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))))
=> ~ valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X4,t2tb(X5))),tb2t2(mk_array1(int,X6,t2tb(X7))),tb2t2(mk_array1(int,X8,t2tb(X9))),tb2t2(mk_array1(int,X10,t2tb(X11)))),tb2t(set(int,int,t2tb(X13),t2tb1(X14),t2tb1(X16)))) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f68]) ).
tff(f76,plain,
! [X3: $int,X0: map_int_int,X1: map_int_int,X2: $int] :
( ! [X4: $int] :
( ( $less(X4,X3)
& ~ $less(X4,X2) )
=> ( tb2t1(get(int,int,t2tb(X0),t2tb1(X4))) = tb2t1(get(int,int,t2tb(X1),t2tb1(X4))) ) )
<=> grid_eq_sub1(X0,X1,X2,X3) ),
inference(theory_normalization,[],[f23]) ).
tff(f78,plain,
~ ! [X2: $int,X6: $int,X4: $int,X5: map_int_int,X10: $int,X9: map_int_int,X8: $int,X1: map_int_int,X14: $int,X0: $int,X13: map_int_int,X7: map_int_int,X12: $int,X11: map_int_int,X3: map_int_int] :
( ( ~ $less(X0,0)
& ~ $less(X8,0)
& ( X12 = 81 )
& well_formed_sudoku1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X4,t2tb(X5))),tb2t2(mk_array1(int,X6,t2tb(X7))),tb2t2(mk_array1(int,X8,t2tb(X9))),tb2t2(mk_array1(int,X10,t2tb(X11)))))
& ~ $less(X4,0)
& ~ $less(X12,0)
& valid_values1(X13)
& full_up_to1(X13,X14)
& ~ $less(X10,0)
& ~ $less(X14,0)
& valid_up_to1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X4,t2tb(X5))),tb2t2(mk_array1(int,X6,t2tb(X7))),tb2t2(mk_array1(int,X8,t2tb(X9))),tb2t2(mk_array1(int,X10,t2tb(X11)))),X13,X14)
& ~ $less(81,X14)
& ~ $less(X6,0)
& ~ $less(X2,0) )
=> ( ( X14 != 81 )
=> ( ( $less(X14,X12)
& ~ $less(X14,0) )
=> ( ( tb2t1(get(int,int,t2tb(X13),t2tb1(X14))) = 0 )
=> ( ~ $less(9,1)
=> ! [X16: $int,X15: map_int_int] :
( ( ~ $less(X16,1)
& ~ $less(9,X16) )
=> ( ( ! [X17: $int] :
( ( $less(X17,X16)
& ~ $less(X17,1) )
=> ! [X18: map_int_int] :
( ( included1(tb2t(set(int,int,t2tb(X13),t2tb1(X14),t2tb1(X17))),X18)
& full1(X18) )
=> ~ valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X4,t2tb(X5))),tb2t2(mk_array1(int,X6,t2tb(X7))),tb2t2(mk_array1(int,X8,t2tb(X9))),tb2t2(mk_array1(int,X10,t2tb(X11)))),X18) ) )
& grid_eq_sub1(X13,tb2t(set(int,int,t2tb(X15),t2tb1(X14),t2tb1(0))),0,81)
& full_up_to1(X15,X14) )
=> ( ( ~ $less(X14,0)
& ~ $less(X12,0)
& $less(X14,X12) )
=> ! [X19: map_int_int] :
( ( ( X19 = tb2t(set(int,int,t2tb(X15),t2tb1(X14),t2tb1(X16))) )
& ~ $less(X12,0) )
=> ( ( chunk_valid_indexes1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))))
& valid_values1(X19)
& ( X12 = 81 )
& is_index1(X14) )
=> ( ~ valid_chunk1(X19,X14,tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))))
=> ~ valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X0,t2tb(X1))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X4,t2tb(X5))),tb2t2(mk_array1(int,X6,t2tb(X7))),tb2t2(mk_array1(int,X8,t2tb(X9))),tb2t2(mk_array1(int,X10,t2tb(X11)))),tb2t(set(int,int,t2tb(X13),t2tb1(X14),t2tb1(X16)))) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f69]) ).
tff(f84,plain,
! [X0: $int] :
( ( $less(X0,81)
& ~ $less(X0,0) )
<=> is_index1(X0) ),
inference(theory_normalization,[],[f15]) ).
tff(f88,plain,
! [X1: map_int_int,X0: map_int_int] :
( ! [X2: $int] :
( ( ~ $less(9,tb2t1(get(int,int,t2tb(X0),t2tb1(X2))))
& is_index1(X2)
& ~ $less(tb2t1(get(int,int,t2tb(X0),t2tb1(X2))),1) )
=> ( tb2t1(get(int,int,t2tb(X1),t2tb1(X2))) = tb2t1(get(int,int,t2tb(X0),t2tb1(X2))) ) )
<=> included1(X0,X1) ),
inference(theory_normalization,[],[f55]) ).
tff(f90,plain,
! [X2: array_int,X1: array_int,X4: array_int,X3: array_int,X0: array_int,X5: array_int] : ( column_offsets1(mk_sudoku_chunks1(X4,X5,X3,X0,X2,X1)) = X5 ),
inference(rectify,[],[f37]) ).
tff(f97,plain,
! [X5: ty,X4: uni,X0: uni,X2: uni,X1: ty,X3: uni] :
( sort1(X5,X4)
=> ( ( X0 = X3 )
=> ( get(X5,X1,set(X5,X1,X2,X3,X4),X0) = X4 ) ) ),
inference(rectify,[],[f11]) ).
tff(f98,plain,
! [X3: array_int,X0: array_int,X4: array_int,X2: array_int,X1: array_int,X5: array_int] : ( column_start1(mk_sudoku_chunks1(X5,X0,X3,X1,X4,X2)) = X5 ),
inference(rectify,[],[f36]) ).
tff(f102,plain,
! [X1: map_int_int,X0: map_int_int] :
( included1(X1,X0)
=> ! [X3: array_int,X2: array_int,X4: $int] :
( ( chunk_valid_indexes1(X2,X3)
& is_index1(X4)
& valid_chunk1(X0,X4,X2,X3) )
=> valid_chunk1(X1,X4,X2,X3) ) ),
inference(rectify,[],[f56]) ).
tff(f106,plain,
! [X2: map_int_int,X3: $int,X0: $int,X1: map_int_int] :
( ! [X4: $int] :
( ( ~ $less(X4,X3)
& $less(X4,X0) )
=> ( tb2t1(get(int,int,t2tb(X1),t2tb1(X4))) = tb2t1(get(int,int,t2tb(X2),t2tb1(X4))) ) )
<=> grid_eq_sub1(X1,X2,X3,X0) ),
inference(rectify,[],[f76]) ).
tff(f108,plain,
~ ! [X2: $int,X12: $int,X9: $int,X10: map_int_int,X6: $int,X5: map_int_int,X4: $int,X0: $int,X13: map_int_int,X1: $int,X8: $int,X3: map_int_int,X7: map_int_int,X11: map_int_int,X14: map_int_int] :
( ( ~ $less(81,X8)
& ~ $less(X6,0)
& valid_up_to1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X1,t2tb(X11))),tb2t2(mk_array1(int,X6,t2tb(X5))),tb2t2(mk_array1(int,X4,t2tb(X13)))),X10,X8)
& ~ $less(X0,0)
& valid_values1(X10)
& well_formed_sudoku1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X1,t2tb(X11))),tb2t2(mk_array1(int,X6,t2tb(X5))),tb2t2(mk_array1(int,X4,t2tb(X13)))))
& ~ $less(X9,0)
& ~ $less(X2,0)
& ~ $less(X4,0)
& ( X12 = 81 )
& ~ $less(X8,0)
& ~ $less(X12,0)
& ~ $less(X1,0)
& full_up_to1(X10,X8) )
=> ( ( 81 != X8 )
=> ( ( ~ $less(X8,0)
& $less(X8,X12) )
=> ( ( 0 = tb2t1(get(int,int,t2tb(X10),t2tb1(X8))) )
=> ( ~ $less(9,1)
=> ! [X15: $int,X16: map_int_int] :
( ( ~ $less(X15,1)
& ~ $less(9,X15) )
=> ( ( grid_eq_sub1(X10,tb2t(set(int,int,t2tb(X16),t2tb1(X8),t2tb1(0))),0,81)
& full_up_to1(X16,X8)
& ! [X17: $int] :
( ( ~ $less(X17,1)
& $less(X17,X15) )
=> ! [X18: map_int_int] :
( ( full1(X18)
& included1(tb2t(set(int,int,t2tb(X10),t2tb1(X8),t2tb1(X17))),X18) )
=> ~ valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X1,t2tb(X11))),tb2t2(mk_array1(int,X6,t2tb(X5))),tb2t2(mk_array1(int,X4,t2tb(X13)))),X18) ) ) )
=> ( ( ~ $less(X12,0)
& ~ $less(X8,0)
& $less(X8,X12) )
=> ! [X19: map_int_int] :
( ( ~ $less(X12,0)
& ( tb2t(set(int,int,t2tb(X16),t2tb1(X8),t2tb1(X15))) = X19 ) )
=> ( ( ( X12 = 81 )
& is_index1(X8)
& chunk_valid_indexes1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))))
& valid_values1(X19) )
=> ( ~ valid_chunk1(X19,X8,tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))))
=> ~ valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X1,t2tb(X11))),tb2t2(mk_array1(int,X6,t2tb(X5))),tb2t2(mk_array1(int,X4,t2tb(X13)))),tb2t(set(int,int,t2tb(X10),t2tb1(X8),t2tb1(X15)))) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f78]) ).
tff(f118,plain,
! [X2: uni,X4: ty,X0: ty,X1: uni,X3: uni] :
( sort1(X4,X3)
=> ( sort1(X4,X2)
=> ! [X5: uni] :
( ( X2 != X3 )
=> ( get(X0,X4,set(X0,X4,X1,X3,X5),X2) = get(X0,X4,X1,X2) ) ) ) ),
inference(rectify,[],[f12]) ).
tff(f128,plain,
! [X0: map_int_int,X1: map_int_int] :
( included1(X1,X0)
<=> ! [X2: $int] :
( ( is_index1(X2)
& ~ $less(tb2t1(get(int,int,t2tb(X1),t2tb1(X2))),1)
& ~ $less(9,tb2t1(get(int,int,t2tb(X1),t2tb1(X2)))) )
=> ( tb2t1(get(int,int,t2tb(X1),t2tb1(X2))) = tb2t1(get(int,int,t2tb(X0),t2tb1(X2))) ) ) ),
inference(rectify,[],[f88]) ).
tff(f131,plain,
! [X0: map_int_int,X1: map_int_int] :
( ! [X2: $int] :
( ( is_index1(X2)
& ~ $less(tb2t1(get(int,int,t2tb(X1),t2tb1(X2))),1)
& ~ $less(9,tb2t1(get(int,int,t2tb(X1),t2tb1(X2)))) )
=> ( tb2t1(get(int,int,t2tb(X1),t2tb1(X2))) = tb2t1(get(int,int,t2tb(X0),t2tb1(X2))) ) )
=> included1(X1,X0) ),
inference(unused_predicate_definition_removal,[],[f128]) ).
tff(f139,plain,
! [X2: map_int_int,X3: $int,X0: $int,X1: map_int_int] :
( ! [X4: $int] :
( ( tb2t1(get(int,int,t2tb(X1),t2tb1(X4))) = tb2t1(get(int,int,t2tb(X2),t2tb1(X4))) )
| $less(X4,X3)
| ~ $less(X4,X0) )
<=> grid_eq_sub1(X1,X2,X3,X0) ),
inference(ennf_transformation,[],[f106]) ).
tff(f140,plain,
! [X3: $int,X2: map_int_int,X1: map_int_int,X0: $int] :
( grid_eq_sub1(X1,X2,X3,X0)
<=> ! [X4: $int] :
( ~ $less(X4,X0)
| $less(X4,X3)
| ( tb2t1(get(int,int,t2tb(X1),t2tb1(X4))) = tb2t1(get(int,int,t2tb(X2),t2tb1(X4))) ) ) ),
inference(flattening,[],[f139]) ).
tff(f149,plain,
? [X2: $int,X12: $int,X9: $int,X10: map_int_int,X6: $int,X5: map_int_int,X4: $int,X0: $int,X13: map_int_int,X1: $int,X8: $int,X3: map_int_int,X7: map_int_int,X11: map_int_int,X14: map_int_int] :
( ? [X15: $int,X16: map_int_int] :
( ? [X19: map_int_int] :
( valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X1,t2tb(X11))),tb2t2(mk_array1(int,X6,t2tb(X5))),tb2t2(mk_array1(int,X4,t2tb(X13)))),tb2t(set(int,int,t2tb(X10),t2tb1(X8),t2tb1(X15))))
& ~ valid_chunk1(X19,X8,tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))))
& ( X12 = 81 )
& is_index1(X8)
& chunk_valid_indexes1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))))
& valid_values1(X19)
& ~ $less(X12,0)
& ( tb2t(set(int,int,t2tb(X16),t2tb1(X8),t2tb1(X15))) = X19 ) )
& ~ $less(X12,0)
& ~ $less(X8,0)
& $less(X8,X12)
& grid_eq_sub1(X10,tb2t(set(int,int,t2tb(X16),t2tb1(X8),t2tb1(0))),0,81)
& full_up_to1(X16,X8)
& ! [X17: $int] :
( ! [X18: map_int_int] :
( ~ valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X1,t2tb(X11))),tb2t2(mk_array1(int,X6,t2tb(X5))),tb2t2(mk_array1(int,X4,t2tb(X13)))),X18)
| ~ full1(X18)
| ~ included1(tb2t(set(int,int,t2tb(X10),t2tb1(X8),t2tb1(X17))),X18) )
| $less(X17,1)
| ~ $less(X17,X15) )
& ~ $less(X15,1)
& ~ $less(9,X15) )
& ~ $less(9,1)
& ( 0 = tb2t1(get(int,int,t2tb(X10),t2tb1(X8))) )
& ~ $less(X8,0)
& $less(X8,X12)
& ( 81 != X8 )
& ~ $less(81,X8)
& ~ $less(X6,0)
& valid_up_to1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X1,t2tb(X11))),tb2t2(mk_array1(int,X6,t2tb(X5))),tb2t2(mk_array1(int,X4,t2tb(X13)))),X10,X8)
& ~ $less(X0,0)
& valid_values1(X10)
& well_formed_sudoku1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X1,t2tb(X11))),tb2t2(mk_array1(int,X6,t2tb(X5))),tb2t2(mk_array1(int,X4,t2tb(X13)))))
& ~ $less(X9,0)
& ~ $less(X2,0)
& ~ $less(X4,0)
& ( X12 = 81 )
& ~ $less(X8,0)
& ~ $less(X12,0)
& ~ $less(X1,0)
& full_up_to1(X10,X8) ),
inference(ennf_transformation,[],[f108]) ).
tff(f150,plain,
? [X14: map_int_int,X9: $int,X2: $int,X4: $int,X6: $int,X7: map_int_int,X5: map_int_int,X8: $int,X1: $int,X12: $int,X3: map_int_int,X0: $int,X13: map_int_int,X10: map_int_int,X11: map_int_int] :
( valid_up_to1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X1,t2tb(X11))),tb2t2(mk_array1(int,X6,t2tb(X5))),tb2t2(mk_array1(int,X4,t2tb(X13)))),X10,X8)
& ~ $less(81,X8)
& ~ $less(X0,0)
& valid_values1(X10)
& ( 0 = tb2t1(get(int,int,t2tb(X10),t2tb1(X8))) )
& ~ $less(X6,0)
& ( X12 = 81 )
& ~ $less(X2,0)
& ~ $less(X4,0)
& well_formed_sudoku1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X1,t2tb(X11))),tb2t2(mk_array1(int,X6,t2tb(X5))),tb2t2(mk_array1(int,X4,t2tb(X13)))))
& ~ $less(X8,0)
& ~ $less(X9,0)
& $less(X8,X12)
& ( 81 != X8 )
& ~ $less(9,1)
& full_up_to1(X10,X8)
& ~ $less(X1,0)
& ? [X16: map_int_int,X15: $int] :
( ? [X19: map_int_int] :
( valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X1,t2tb(X11))),tb2t2(mk_array1(int,X6,t2tb(X5))),tb2t2(mk_array1(int,X4,t2tb(X13)))),tb2t(set(int,int,t2tb(X10),t2tb1(X8),t2tb1(X15))))
& chunk_valid_indexes1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))))
& valid_values1(X19)
& is_index1(X8)
& ( tb2t(set(int,int,t2tb(X16),t2tb1(X8),t2tb1(X15))) = X19 )
& ~ $less(X12,0)
& ( X12 = 81 )
& ~ valid_chunk1(X19,X8,tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14)))) )
& ~ $less(X15,1)
& ~ $less(X12,0)
& grid_eq_sub1(X10,tb2t(set(int,int,t2tb(X16),t2tb1(X8),t2tb1(0))),0,81)
& $less(X8,X12)
& ! [X17: $int] :
( ~ $less(X17,X15)
| $less(X17,1)
| ! [X18: map_int_int] :
( ~ valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X9,t2tb(X7))),tb2t2(mk_array1(int,X0,t2tb(X14))),tb2t2(mk_array1(int,X2,t2tb(X3))),tb2t2(mk_array1(int,X1,t2tb(X11))),tb2t2(mk_array1(int,X6,t2tb(X5))),tb2t2(mk_array1(int,X4,t2tb(X13)))),X18)
| ~ full1(X18)
| ~ included1(tb2t(set(int,int,t2tb(X10),t2tb1(X8),t2tb1(X17))),X18) ) )
& ~ $less(X8,0)
& ~ $less(9,X15)
& full_up_to1(X16,X8) )
& ~ $less(X12,0)
& ~ $less(X8,0) ),
inference(flattening,[],[f149]) ).
tff(f151,plain,
! [X1: map_int_int,X0: sudoku_chunks1] :
( valid1(X0,X1)
<=> ! [X2: $int] :
( ~ is_index1(X2)
| ( valid_square1(X0,X1,X2)
& valid_column1(X0,X1,X2)
& valid_row1(X0,X1,X2) ) ) ),
inference(ennf_transformation,[],[f53]) ).
tff(f154,plain,
! [X2: uni,X4: ty,X0: ty,X1: uni,X3: uni] :
( ! [X5: uni] :
( ( X2 = X3 )
| ( get(X0,X4,set(X0,X4,X1,X3,X5),X2) = get(X0,X4,X1,X2) ) )
| ~ sort1(X4,X2)
| ~ sort1(X4,X3) ),
inference(ennf_transformation,[],[f118]) ).
tff(f155,plain,
! [X4: ty,X0: ty,X3: uni,X1: uni,X2: uni] :
( ~ sort1(X4,X3)
| ! [X5: uni] :
( ( X2 = X3 )
| ( get(X0,X4,set(X0,X4,X1,X3,X5),X2) = get(X0,X4,X1,X2) ) )
| ~ sort1(X4,X2) ),
inference(flattening,[],[f154]) ).
tff(f160,plain,
! [X1: map_int_int,X0: map_int_int] :
( ! [X3: array_int,X2: array_int,X4: $int] :
( valid_chunk1(X1,X4,X2,X3)
| ~ chunk_valid_indexes1(X2,X3)
| ~ is_index1(X4)
| ~ valid_chunk1(X0,X4,X2,X3) )
| ~ included1(X1,X0) ),
inference(ennf_transformation,[],[f102]) ).
tff(f161,plain,
! [X1: map_int_int,X0: map_int_int] :
( ~ included1(X1,X0)
| ! [X3: array_int,X2: array_int,X4: $int] :
( ~ valid_chunk1(X0,X4,X2,X3)
| ~ is_index1(X4)
| ~ chunk_valid_indexes1(X2,X3)
| valid_chunk1(X1,X4,X2,X3) ) ),
inference(flattening,[],[f160]) ).
tff(f162,plain,
! [X5: ty,X4: uni,X0: uni,X2: uni,X1: ty,X3: uni] :
( ( get(X5,X1,set(X5,X1,X2,X3,X4),X0) = X4 )
| ( X0 != X3 )
| ~ sort1(X5,X4) ),
inference(ennf_transformation,[],[f97]) ).
tff(f163,plain,
! [X2: uni,X4: uni,X3: uni,X0: uni,X5: ty,X1: ty] :
( ( get(X5,X1,set(X5,X1,X2,X3,X4),X0) = X4 )
| ( X0 != X3 )
| ~ sort1(X5,X4) ),
inference(flattening,[],[f162]) ).
tff(f172,plain,
! [X0: map_int_int,X1: map_int_int] :
( included1(X1,X0)
| ? [X2: $int] :
( ( tb2t1(get(int,int,t2tb(X0),t2tb1(X2))) != tb2t1(get(int,int,t2tb(X1),t2tb1(X2))) )
& is_index1(X2)
& ~ $less(tb2t1(get(int,int,t2tb(X1),t2tb1(X2))),1)
& ~ $less(9,tb2t1(get(int,int,t2tb(X1),t2tb1(X2)))) ) ),
inference(ennf_transformation,[],[f131]) ).
tff(f173,plain,
! [X0: map_int_int,X1: map_int_int] :
( ? [X2: $int] :
( is_index1(X2)
& ( tb2t1(get(int,int,t2tb(X0),t2tb1(X2))) != tb2t1(get(int,int,t2tb(X1),t2tb1(X2))) )
& ~ $less(tb2t1(get(int,int,t2tb(X1),t2tb1(X2))),1)
& ~ $less(9,tb2t1(get(int,int,t2tb(X1),t2tb1(X2)))) )
| included1(X1,X0) ),
inference(flattening,[],[f172]) ).
tff(f201,plain,
! [X0: map_int_int,X1: map_int_int] :
( ( is_index1(sK7(X0,X1))
& ( tb2t1(get(int,int,t2tb(X0),t2tb1(sK7(X0,X1)))) != tb2t1(get(int,int,t2tb(X1),t2tb1(sK7(X0,X1)))) )
& ~ $less(tb2t1(get(int,int,t2tb(X1),t2tb1(sK7(X0,X1)))),1)
& ~ $less(9,tb2t1(get(int,int,t2tb(X1),t2tb1(sK7(X0,X1))))) )
| included1(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f173]) ).
tff(f202,plain,
! [X1: map_int_int,X0: sudoku_chunks1] :
( ( valid1(X0,X1)
| ? [X2: $int] :
( is_index1(X2)
& ( ~ valid_square1(X0,X1,X2)
| ~ valid_column1(X0,X1,X2)
| ~ valid_row1(X0,X1,X2) ) ) )
& ( ! [X2: $int] :
( ~ is_index1(X2)
| ( valid_square1(X0,X1,X2)
& valid_column1(X0,X1,X2)
& valid_row1(X0,X1,X2) ) )
| ~ valid1(X0,X1) ) ),
inference(nnf_transformation,[],[f151]) ).
tff(f203,plain,
! [X0: map_int_int,X1: sudoku_chunks1] :
( ( valid1(X1,X0)
| ? [X2: $int] :
( is_index1(X2)
& ( ~ valid_square1(X1,X0,X2)
| ~ valid_column1(X1,X0,X2)
| ~ valid_row1(X1,X0,X2) ) ) )
& ( ! [X3: $int] :
( ~ is_index1(X3)
| ( valid_square1(X1,X0,X3)
& valid_column1(X1,X0,X3)
& valid_row1(X1,X0,X3) ) )
| ~ valid1(X1,X0) ) ),
inference(rectify,[],[f202]) ).
tff(f204,plain,
! [X0: map_int_int,X1: sudoku_chunks1] :
( ( valid1(X1,X0)
| ( is_index1(sK8(X0,X1))
& ( ~ valid_square1(X1,X0,sK8(X0,X1))
| ~ valid_column1(X1,X0,sK8(X0,X1))
| ~ valid_row1(X1,X0,sK8(X0,X1)) ) ) )
& ( ! [X3: $int] :
( ~ is_index1(X3)
| ( valid_square1(X1,X0,X3)
& valid_column1(X1,X0,X3)
& valid_row1(X1,X0,X3) ) )
| ~ valid1(X1,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X2,sK8(X0,X1))],[f203]) ).
tff(f205,plain,
! [X3: $int,X2: map_int_int,X1: map_int_int,X0: $int] :
( ( grid_eq_sub1(X1,X2,X3,X0)
| ? [X4: $int] :
( $less(X4,X0)
& ~ $less(X4,X3)
& ( tb2t1(get(int,int,t2tb(X1),t2tb1(X4))) != tb2t1(get(int,int,t2tb(X2),t2tb1(X4))) ) ) )
& ( ! [X4: $int] :
( ~ $less(X4,X0)
| $less(X4,X3)
| ( tb2t1(get(int,int,t2tb(X1),t2tb1(X4))) = tb2t1(get(int,int,t2tb(X2),t2tb1(X4))) ) )
| ~ grid_eq_sub1(X1,X2,X3,X0) ) ),
inference(nnf_transformation,[],[f140]) ).
tff(f206,plain,
! [X0: $int,X1: map_int_int,X2: map_int_int,X3: $int] :
( ( grid_eq_sub1(X2,X1,X0,X3)
| ? [X4: $int] :
( $less(X4,X3)
& ~ $less(X4,X0)
& ( tb2t1(get(int,int,t2tb(X1),t2tb1(X4))) != tb2t1(get(int,int,t2tb(X2),t2tb1(X4))) ) ) )
& ( ! [X5: $int] :
( ~ $less(X5,X3)
| $less(X5,X0)
| ( tb2t1(get(int,int,t2tb(X1),t2tb1(X5))) = tb2t1(get(int,int,t2tb(X2),t2tb1(X5))) ) )
| ~ grid_eq_sub1(X2,X1,X0,X3) ) ),
inference(rectify,[],[f205]) ).
tff(f207,plain,
! [X0: $int,X1: map_int_int,X2: map_int_int,X3: $int] :
( ( grid_eq_sub1(X2,X1,X0,X3)
| ( $less(sK9(X0,X1,X2,X3),X3)
& ~ $less(sK9(X0,X1,X2,X3),X0)
& ( tb2t1(get(int,int,t2tb(X1),t2tb1(sK9(X0,X1,X2,X3)))) != tb2t1(get(int,int,t2tb(X2),t2tb1(sK9(X0,X1,X2,X3)))) ) ) )
& ( ! [X5: $int] :
( ~ $less(X5,X3)
| $less(X5,X0)
| ( tb2t1(get(int,int,t2tb(X1),t2tb1(X5))) = tb2t1(get(int,int,t2tb(X2),t2tb1(X5))) ) )
| ~ grid_eq_sub1(X2,X1,X0,X3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X4,sK9(X0,X1,X2,X3))],[f206]) ).
tff(f212,plain,
! [X0: ty,X1: ty,X2: uni,X3: uni,X4: uni] :
( ~ sort1(X0,X2)
| ! [X5: uni] :
( ( X2 = X4 )
| ( get(X1,X0,X3,X4) = get(X1,X0,set(X1,X0,X3,X2,X5),X4) ) )
| ~ sort1(X0,X4) ),
inference(rectify,[],[f155]) ).
tff(f213,plain,
! [X0: array_int,X1: array_int,X2: array_int,X3: array_int,X4: array_int,X5: array_int] : ( column_offsets1(mk_sudoku_chunks1(X2,X5,X3,X4,X0,X1)) = X5 ),
inference(rectify,[],[f90]) ).
tff(f215,plain,
? [X0: map_int_int,X1: $int,X2: $int,X3: $int,X4: $int,X5: map_int_int,X6: map_int_int,X7: $int,X8: $int,X9: $int,X10: map_int_int,X11: $int,X12: map_int_int,X13: map_int_int,X14: map_int_int] :
( valid_up_to1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X1,t2tb(X5))),tb2t2(mk_array1(int,X11,t2tb(X0))),tb2t2(mk_array1(int,X2,t2tb(X10))),tb2t2(mk_array1(int,X8,t2tb(X14))),tb2t2(mk_array1(int,X4,t2tb(X6))),tb2t2(mk_array1(int,X3,t2tb(X12)))),X13,X7)
& ~ $less(81,X7)
& ~ $less(X11,0)
& valid_values1(X13)
& ( 0 = tb2t1(get(int,int,t2tb(X13),t2tb1(X7))) )
& ~ $less(X4,0)
& ( 81 = X9 )
& ~ $less(X2,0)
& ~ $less(X3,0)
& well_formed_sudoku1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X1,t2tb(X5))),tb2t2(mk_array1(int,X11,t2tb(X0))),tb2t2(mk_array1(int,X2,t2tb(X10))),tb2t2(mk_array1(int,X8,t2tb(X14))),tb2t2(mk_array1(int,X4,t2tb(X6))),tb2t2(mk_array1(int,X3,t2tb(X12)))))
& ~ $less(X7,0)
& ~ $less(X1,0)
& $less(X7,X9)
& ( 81 != X7 )
& ~ $less(9,1)
& full_up_to1(X13,X7)
& ~ $less(X8,0)
& ? [X15: map_int_int,X16: $int] :
( ? [X17: map_int_int] :
( valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X1,t2tb(X5))),tb2t2(mk_array1(int,X11,t2tb(X0))),tb2t2(mk_array1(int,X2,t2tb(X10))),tb2t2(mk_array1(int,X8,t2tb(X14))),tb2t2(mk_array1(int,X4,t2tb(X6))),tb2t2(mk_array1(int,X3,t2tb(X12)))),tb2t(set(int,int,t2tb(X13),t2tb1(X7),t2tb1(X16))))
& chunk_valid_indexes1(tb2t2(mk_array1(int,X1,t2tb(X5))),tb2t2(mk_array1(int,X11,t2tb(X0))))
& valid_values1(X17)
& is_index1(X7)
& ( tb2t(set(int,int,t2tb(X15),t2tb1(X7),t2tb1(X16))) = X17 )
& ~ $less(X9,0)
& ( 81 = X9 )
& ~ valid_chunk1(X17,X7,tb2t2(mk_array1(int,X1,t2tb(X5))),tb2t2(mk_array1(int,X11,t2tb(X0)))) )
& ~ $less(X16,1)
& ~ $less(X9,0)
& grid_eq_sub1(X13,tb2t(set(int,int,t2tb(X15),t2tb1(X7),t2tb1(0))),0,81)
& $less(X7,X9)
& ! [X18: $int] :
( ~ $less(X18,X16)
| $less(X18,1)
| ! [X19: map_int_int] :
( ~ valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,X1,t2tb(X5))),tb2t2(mk_array1(int,X11,t2tb(X0))),tb2t2(mk_array1(int,X2,t2tb(X10))),tb2t2(mk_array1(int,X8,t2tb(X14))),tb2t2(mk_array1(int,X4,t2tb(X6))),tb2t2(mk_array1(int,X3,t2tb(X12)))),X19)
| ~ full1(X19)
| ~ included1(tb2t(set(int,int,t2tb(X13),t2tb1(X7),t2tb1(X18))),X19) ) )
& ~ $less(X7,0)
& ~ $less(9,X16)
& full_up_to1(X15,X7) )
& ~ $less(X9,0)
& ~ $less(X7,0) ),
inference(rectify,[],[f150]) ).
tff(f216,plain,
( valid_up_to1(mk_sudoku_chunks1(tb2t2(mk_array1(int,sK11,t2tb(sK15))),tb2t2(mk_array1(int,sK21,t2tb(sK10))),tb2t2(mk_array1(int,sK12,t2tb(sK20))),tb2t2(mk_array1(int,sK18,t2tb(sK24))),tb2t2(mk_array1(int,sK14,t2tb(sK16))),tb2t2(mk_array1(int,sK13,t2tb(sK22)))),sK23,sK17)
& ~ $less(81,sK17)
& ~ $less(sK21,0)
& valid_values1(sK23)
& ( 0 = tb2t1(get(int,int,t2tb(sK23),t2tb1(sK17))) )
& ~ $less(sK14,0)
& ( 81 = sK19 )
& ~ $less(sK12,0)
& ~ $less(sK13,0)
& well_formed_sudoku1(mk_sudoku_chunks1(tb2t2(mk_array1(int,sK11,t2tb(sK15))),tb2t2(mk_array1(int,sK21,t2tb(sK10))),tb2t2(mk_array1(int,sK12,t2tb(sK20))),tb2t2(mk_array1(int,sK18,t2tb(sK24))),tb2t2(mk_array1(int,sK14,t2tb(sK16))),tb2t2(mk_array1(int,sK13,t2tb(sK22)))))
& ~ $less(sK17,0)
& ~ $less(sK11,0)
& $less(sK17,sK19)
& ( 81 != sK17 )
& ~ $less(9,1)
& full_up_to1(sK23,sK17)
& ~ $less(sK18,0)
& valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,sK11,t2tb(sK15))),tb2t2(mk_array1(int,sK21,t2tb(sK10))),tb2t2(mk_array1(int,sK12,t2tb(sK20))),tb2t2(mk_array1(int,sK18,t2tb(sK24))),tb2t2(mk_array1(int,sK14,t2tb(sK16))),tb2t2(mk_array1(int,sK13,t2tb(sK22)))),tb2t(set(int,int,t2tb(sK23),t2tb1(sK17),t2tb1(sK26))))
& chunk_valid_indexes1(tb2t2(mk_array1(int,sK11,t2tb(sK15))),tb2t2(mk_array1(int,sK21,t2tb(sK10))))
& valid_values1(sK27)
& is_index1(sK17)
& ( tb2t(set(int,int,t2tb(sK25),t2tb1(sK17),t2tb1(sK26))) = sK27 )
& ~ $less(sK19,0)
& ( 81 = sK19 )
& ~ valid_chunk1(sK27,sK17,tb2t2(mk_array1(int,sK11,t2tb(sK15))),tb2t2(mk_array1(int,sK21,t2tb(sK10))))
& ~ $less(sK26,1)
& ~ $less(sK19,0)
& grid_eq_sub1(sK23,tb2t(set(int,int,t2tb(sK25),t2tb1(sK17),t2tb1(0))),0,81)
& $less(sK17,sK19)
& ! [X18: $int] :
( ~ $less(X18,sK26)
| $less(X18,1)
| ! [X19: map_int_int] :
( ~ valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,sK11,t2tb(sK15))),tb2t2(mk_array1(int,sK21,t2tb(sK10))),tb2t2(mk_array1(int,sK12,t2tb(sK20))),tb2t2(mk_array1(int,sK18,t2tb(sK24))),tb2t2(mk_array1(int,sK14,t2tb(sK16))),tb2t2(mk_array1(int,sK13,t2tb(sK22)))),X19)
| ~ full1(X19)
| ~ included1(tb2t(set(int,int,t2tb(sK23),t2tb1(sK17),t2tb1(X18))),X19) ) )
& ~ $less(sK17,0)
& ~ $less(9,sK26)
& full_up_to1(sK25,sK17)
& ~ $less(sK19,0)
& ~ $less(sK17,0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27]),skolemize(X0,sK10),skolemize(X1,sK11),skolemize(X2,sK12),skolemize(X3,sK13),skolemize(X4,sK14),skolemize(X5,sK15),skolemize(X6,sK16),skolemize(X7,sK17),skolemize(X8,sK18),skolemize(X9,sK19),skolemize(X10,sK20),skolemize(X11,sK21),skolemize(X12,sK22),skolemize(X13,sK23),skolemize(X14,sK24),skolemize(X15,sK25),skolemize(X16,sK26),skolemize(X17,sK27)],[f215]) ).
tff(f222,plain,
! [X0: map_int_int,X1: map_int_int] :
( ~ included1(X0,X1)
| ! [X2: array_int,X3: array_int,X4: $int] :
( ~ valid_chunk1(X1,X4,X3,X2)
| ~ is_index1(X4)
| ~ chunk_valid_indexes1(X3,X2)
| valid_chunk1(X0,X4,X3,X2) ) ),
inference(rectify,[],[f161]) ).
tff(f228,plain,
! [X0: $int] :
( ( ( $less(X0,81)
& ~ $less(X0,0) )
| ~ is_index1(X0) )
& ( is_index1(X0)
| ~ $less(X0,81)
| $less(X0,0) ) ),
inference(nnf_transformation,[],[f84]) ).
tff(f229,plain,
! [X0: $int] :
( ( ( $less(X0,81)
& ~ $less(X0,0) )
| ~ is_index1(X0) )
& ( is_index1(X0)
| ~ $less(X0,81)
| $less(X0,0) ) ),
inference(flattening,[],[f228]) ).
tff(f233,plain,
! [X0: sudoku_chunks1,X1: map_int_int,X2: $int] :
( ( valid_chunk1(X1,X2,column_start1(X0),column_offsets1(X0))
| ~ valid_column1(X0,X1,X2) )
& ( valid_column1(X0,X1,X2)
| ~ valid_chunk1(X1,X2,column_start1(X0),column_offsets1(X0)) ) ),
inference(nnf_transformation,[],[f50]) ).
tff(f247,plain,
! [X0: array_int,X1: array_int,X2: array_int,X3: array_int,X4: array_int,X5: array_int] : ( column_start1(mk_sudoku_chunks1(X5,X1,X0,X4,X2,X3)) = X5 ),
inference(rectify,[],[f98]) ).
tff(f252,plain,
! [X0: uni,X1: uni,X2: uni,X3: uni,X4: ty,X5: ty] :
( ( get(X4,X5,set(X4,X5,X0,X2,X1),X3) = X1 )
| ( X2 != X3 )
| ~ sort1(X4,X1) ),
inference(rectify,[],[f163]) ).
tff(f289,plain,
! [X0: map_int_int,X1: map_int_int] :
( included1(X1,X0)
| ( tb2t1(get(int,int,t2tb(X0),t2tb1(sK7(X0,X1)))) != tb2t1(get(int,int,t2tb(X1),t2tb1(sK7(X0,X1)))) ) ),
inference(cnf_transformation,[],[f201]) ).
tff(f290,plain,
! [X0: map_int_int,X1: map_int_int] :
( is_index1(sK7(X0,X1))
| included1(X1,X0) ),
inference(cnf_transformation,[],[f201]) ).
tff(f293,plain,
! [X3: $int,X0: map_int_int,X1: sudoku_chunks1] :
( valid_column1(X1,X0,X3)
| ~ is_index1(X3)
| ~ valid1(X1,X0) ),
inference(cnf_transformation,[],[f204]) ).
tff(f297,plain,
! [X2: map_int_int,X3: $int,X0: $int,X1: map_int_int,X5: $int] :
( ~ grid_eq_sub1(X2,X1,X0,X3)
| ~ $less(X5,X3)
| ( tb2t1(get(int,int,t2tb(X1),t2tb1(X5))) = tb2t1(get(int,int,t2tb(X2),t2tb1(X5))) )
| $less(X5,X0) ),
inference(cnf_transformation,[],[f207]) ).
tff(f307,plain,
! [X2: uni,X3: uni,X0: ty,X1: ty,X4: uni,X5: uni] :
( ( get(X1,X0,X3,X4) = get(X1,X0,set(X1,X0,X3,X2,X5),X4) )
| ~ sort1(X0,X2)
| ~ sort1(X0,X4)
| ( X2 = X4 ) ),
inference(cnf_transformation,[],[f212]) ).
tff(f308,plain,
! [X2: array_int,X3: array_int,X0: array_int,X1: array_int,X4: array_int,X5: array_int] : ( column_offsets1(mk_sudoku_chunks1(X2,X5,X3,X4,X0,X1)) = X5 ),
inference(cnf_transformation,[],[f213]) ).
tff(f309,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f21]) ).
tff(f319,plain,
grid_eq_sub1(sK23,tb2t(set(int,int,t2tb(sK25),t2tb1(sK17),t2tb1(0))),0,81),
inference(cnf_transformation,[],[f216]) ).
tff(f322,plain,
~ valid_chunk1(sK27,sK17,tb2t2(mk_array1(int,sK11,t2tb(sK15))),tb2t2(mk_array1(int,sK21,t2tb(sK10)))),
inference(cnf_transformation,[],[f216]) ).
tff(f325,plain,
tb2t(set(int,int,t2tb(sK25),t2tb1(sK17),t2tb1(sK26))) = sK27,
inference(cnf_transformation,[],[f216]) ).
tff(f326,plain,
is_index1(sK17),
inference(cnf_transformation,[],[f216]) ).
tff(f328,plain,
chunk_valid_indexes1(tb2t2(mk_array1(int,sK11,t2tb(sK15))),tb2t2(mk_array1(int,sK21,t2tb(sK10)))),
inference(cnf_transformation,[],[f216]) ).
tff(f329,plain,
valid1(mk_sudoku_chunks1(tb2t2(mk_array1(int,sK11,t2tb(sK15))),tb2t2(mk_array1(int,sK21,t2tb(sK10))),tb2t2(mk_array1(int,sK12,t2tb(sK20))),tb2t2(mk_array1(int,sK18,t2tb(sK24))),tb2t2(mk_array1(int,sK14,t2tb(sK16))),tb2t2(mk_array1(int,sK13,t2tb(sK22)))),tb2t(set(int,int,t2tb(sK23),t2tb1(sK17),t2tb1(sK26)))),
inference(cnf_transformation,[],[f216]) ).
tff(f352,plain,
! [X2: array_int,X3: array_int,X0: map_int_int,X1: map_int_int,X4: $int] :
( valid_chunk1(X0,X4,X3,X2)
| ~ valid_chunk1(X1,X4,X3,X2)
| ~ chunk_valid_indexes1(X3,X2)
| ~ included1(X0,X1)
| ~ is_index1(X4) ),
inference(cnf_transformation,[],[f222]) ).
tff(f360,plain,
! [X0: $int] :
( ~ $less(X0,0)
| ~ is_index1(X0) ),
inference(cnf_transformation,[],[f229]) ).
tff(f361,plain,
! [X0: $int] :
( $less(X0,81)
| ~ is_index1(X0) ),
inference(cnf_transformation,[],[f229]) ).
tff(f368,plain,
! [X2: $int,X0: sudoku_chunks1,X1: map_int_int] :
( ~ valid_column1(X0,X1,X2)
| valid_chunk1(X1,X2,column_start1(X0),column_offsets1(X0)) ),
inference(cnf_transformation,[],[f233]) ).
tff(f374,plain,
! [X0: $int] : ( tb2t1(t2tb1(X0)) = X0 ),
inference(cnf_transformation,[],[f20]) ).
tff(f401,plain,
! [X2: array_int,X3: array_int,X0: array_int,X1: array_int,X4: array_int,X5: array_int] : ( column_start1(mk_sudoku_chunks1(X5,X1,X0,X4,X2,X3)) = X5 ),
inference(cnf_transformation,[],[f247]) ).
tff(f404,plain,
! [X0: $int] : sort1(int,t2tb1(X0)),
inference(cnf_transformation,[],[f19]) ).
tff(f405,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f18]) ).
tff(f409,plain,
! [X2: uni,X3: uni,X0: uni,X1: uni,X4: ty,X5: ty] :
( ( get(X4,X5,set(X4,X5,X0,X2,X1),X3) = X1 )
| ( X2 != X3 )
| ~ sort1(X4,X1) ),
inference(cnf_transformation,[],[f252]) ).
tff(f434,plain,
! [X3: uni,X0: uni,X1: uni,X4: ty,X5: ty] :
( ( get(X4,X5,set(X4,X5,X0,X3,X1),X3) = X1 )
| ~ sort1(X4,X1) ),
inference(equality_resolution,[],[f409]) ).
tff(f435,definition,
sF32 = t2tb(sK15),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
tff(f436,definition,
sF33 = mk_array1(int,sK11,sF32),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
tff(f437,plain,
mk_array1(int,sK11,sF32) = sF33,
inference(reorient_equations,[],[f436]) ).
tff(f438,definition,
sF34 = tb2t2(sF33),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
tff(f439,plain,
tb2t2(sF33) = sF34,
inference(reorient_equations,[],[f438]) ).
tff(f440,definition,
sF35 = t2tb(sK10),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
tff(f441,plain,
t2tb(sK10) = sF35,
inference(reorient_equations,[],[f440]) ).
tff(f442,definition,
sF36 = mk_array1(int,sK21,sF35),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
tff(f443,definition,
sF37 = tb2t2(sF36),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
tff(f444,definition,
sF38 = t2tb(sK20),
introduced(definition,[new_symbols(definition,[sF38])],[function_definition]) ).
tff(f445,definition,
sF39 = mk_array1(int,sK12,sF38),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
tff(f446,plain,
mk_array1(int,sK12,sF38) = sF39,
inference(reorient_equations,[],[f445]) ).
tff(f447,definition,
sF40 = tb2t2(sF39),
introduced(definition,[new_symbols(definition,[sF40])],[function_definition]) ).
tff(f448,plain,
tb2t2(sF39) = sF40,
inference(reorient_equations,[],[f447]) ).
tff(f449,definition,
sF41 = t2tb(sK24),
introduced(definition,[new_symbols(definition,[sF41])],[function_definition]) ).
tff(f450,plain,
t2tb(sK24) = sF41,
inference(reorient_equations,[],[f449]) ).
tff(f451,definition,
sF42 = mk_array1(int,sK18,sF41),
introduced(definition,[new_symbols(definition,[sF42])],[function_definition]) ).
tff(f452,plain,
mk_array1(int,sK18,sF41) = sF42,
inference(reorient_equations,[],[f451]) ).
tff(f453,definition,
sF43 = tb2t2(sF42),
introduced(definition,[new_symbols(definition,[sF43])],[function_definition]) ).
tff(f454,plain,
tb2t2(sF42) = sF43,
inference(reorient_equations,[],[f453]) ).
tff(f455,definition,
sF44 = t2tb(sK16),
introduced(definition,[new_symbols(definition,[sF44])],[function_definition]) ).
tff(f456,plain,
t2tb(sK16) = sF44,
inference(reorient_equations,[],[f455]) ).
tff(f457,definition,
sF45 = mk_array1(int,sK14,sF44),
introduced(definition,[new_symbols(definition,[sF45])],[function_definition]) ).
tff(f458,definition,
sF46 = tb2t2(sF45),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
tff(f459,definition,
sF47 = t2tb(sK22),
introduced(definition,[new_symbols(definition,[sF47])],[function_definition]) ).
tff(f460,plain,
t2tb(sK22) = sF47,
inference(reorient_equations,[],[f459]) ).
tff(f461,definition,
sF48 = mk_array1(int,sK13,sF47),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
tff(f462,plain,
mk_array1(int,sK13,sF47) = sF48,
inference(reorient_equations,[],[f461]) ).
tff(f463,definition,
sF49 = tb2t2(sF48),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
tff(f464,plain,
tb2t2(sF48) = sF49,
inference(reorient_equations,[],[f463]) ).
tff(f465,definition,
sF50 = mk_sudoku_chunks1(sF34,sF37,sF40,sF43,sF46,sF49),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
tff(f466,plain,
mk_sudoku_chunks1(sF34,sF37,sF40,sF43,sF46,sF49) = sF50,
inference(reorient_equations,[],[f465]) ).
tff(f468,definition,
sF51 = t2tb(sK23),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
tff(f469,plain,
t2tb(sK23) = sF51,
inference(reorient_equations,[],[f468]) ).
tff(f470,definition,
sF52 = t2tb1(sK17),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
tff(f471,plain,
t2tb1(sK17) = sF52,
inference(reorient_equations,[],[f470]) ).
tff(f477,definition,
sF55 = t2tb1(sK26),
introduced(definition,[new_symbols(definition,[sF55])],[function_definition]) ).
tff(f478,plain,
t2tb1(sK26) = sF55,
inference(reorient_equations,[],[f477]) ).
tff(f479,definition,
sF56 = set(int,int,sF51,sF52,sF55),
introduced(definition,[new_symbols(definition,[sF56])],[function_definition]) ).
tff(f480,plain,
set(int,int,sF51,sF52,sF55) = sF56,
inference(reorient_equations,[],[f479]) ).
tff(f481,definition,
sF57 = tb2t(sF56),
introduced(definition,[new_symbols(definition,[sF57])],[function_definition]) ).
tff(f482,plain,
valid1(sF50,sF57),
inference(definition_folding,[],[f329,f481,f480,f478,f471,f469,f466,f464,f462,f460,f458,f457,f456,f454,f452,f450,f448,f446,f444,f443,f442,f441,f439,f437,f435]) ).
tff(f483,plain,
chunk_valid_indexes1(sF34,sF37),
inference(definition_folding,[],[f328,f443,f442,f441,f439,f437,f435]) ).
tff(f484,definition,
sF58 = t2tb(sK25),
introduced(definition,[new_symbols(definition,[sF58])],[function_definition]) ).
tff(f485,definition,
sF59 = set(int,int,sF58,sF52,sF55),
introduced(definition,[new_symbols(definition,[sF59])],[function_definition]) ).
tff(f486,plain,
set(int,int,sF58,sF52,sF55) = sF59,
inference(reorient_equations,[],[f485]) ).
tff(f487,definition,
sF60 = tb2t(sF59),
introduced(definition,[new_symbols(definition,[sF60])],[function_definition]) ).
tff(f488,plain,
sF60 = sK27,
inference(definition_folding,[],[f325,f487,f486,f478,f471,f484]) ).
tff(f489,plain,
~ valid_chunk1(sK27,sK17,sF34,sF37),
inference(definition_folding,[],[f322,f443,f442,f441,f439,f437,f435]) ).
tff(f490,definition,
sF61 = t2tb1(0),
introduced(definition,[new_symbols(definition,[sF61])],[function_definition]) ).
tff(f491,plain,
t2tb1(0) = sF61,
inference(reorient_equations,[],[f490]) ).
tff(f492,definition,
sF62 = set(int,int,sF58,sF52,sF61),
introduced(definition,[new_symbols(definition,[sF62])],[function_definition]) ).
tff(f493,plain,
set(int,int,sF58,sF52,sF61) = sF62,
inference(reorient_equations,[],[f492]) ).
tff(f494,definition,
sF63 = tb2t(sF62),
introduced(definition,[new_symbols(definition,[sF63])],[function_definition]) ).
tff(f495,plain,
grid_eq_sub1(sK23,sF63,0,81),
inference(definition_folding,[],[f319,f494,f493,f491,f471,f484]) ).
tff(f523,definition,
( spl64_6
<=> ( set(int,int,sF58,sF52,sF55) = sF59 ) ),
introduced(definition,[new_symbols(definition,[spl64_6])],[avatar_definition]) ).
tff(f525,plain,
( ( set(int,int,sF58,sF52,sF55) = sF59 )
| ~ spl64_6 ),
inference(avatar_component_clause,[],[f523]) ).
tff(f526,plain,
spl64_6,
inference(avatar_split_clause,[],[f486,f523]) ).
tff(f538,definition,
( spl64_9
<=> ( t2tb(sK23) = sF51 ) ),
introduced(definition,[new_symbols(definition,[spl64_9])],[avatar_definition]) ).
tff(f540,plain,
( ( t2tb(sK23) = sF51 )
| ~ spl64_9 ),
inference(avatar_component_clause,[],[f538]) ).
tff(f541,plain,
spl64_9,
inference(avatar_split_clause,[],[f469,f538]) ).
tff(f553,definition,
( spl64_12
<=> ( set(int,int,sF51,sF52,sF55) = sF56 ) ),
introduced(definition,[new_symbols(definition,[spl64_12])],[avatar_definition]) ).
tff(f555,plain,
( ( set(int,int,sF51,sF52,sF55) = sF56 )
| ~ spl64_12 ),
inference(avatar_component_clause,[],[f553]) ).
tff(f556,plain,
spl64_12,
inference(avatar_split_clause,[],[f480,f553]) ).
tff(f558,definition,
( spl64_13
<=> valid1(sF50,sF57) ),
introduced(definition,[new_symbols(definition,[spl64_13])],[avatar_definition]) ).
tff(f560,plain,
( valid1(sF50,sF57)
| ~ spl64_13 ),
inference(avatar_component_clause,[],[f558]) ).
tff(f561,plain,
spl64_13,
inference(avatar_split_clause,[],[f482,f558]) ).
tff(f598,definition,
( spl64_21
<=> ( sF60 = sK27 ) ),
introduced(definition,[new_symbols(definition,[spl64_21])],[avatar_definition]) ).
tff(f600,plain,
( ( sF60 = sK27 )
| ~ spl64_21 ),
inference(avatar_component_clause,[],[f598]) ).
tff(f601,plain,
spl64_21,
inference(avatar_split_clause,[],[f488,f598]) ).
tff(f603,definition,
( spl64_22
<=> ( mk_sudoku_chunks1(sF34,sF37,sF40,sF43,sF46,sF49) = sF50 ) ),
introduced(definition,[new_symbols(definition,[spl64_22])],[avatar_definition]) ).
tff(f605,plain,
( ( mk_sudoku_chunks1(sF34,sF37,sF40,sF43,sF46,sF49) = sF50 )
| ~ spl64_22 ),
inference(avatar_component_clause,[],[f603]) ).
tff(f606,plain,
spl64_22,
inference(avatar_split_clause,[],[f466,f603]) ).
tff(f633,definition,
( spl64_28
<=> valid_chunk1(sK27,sK17,sF34,sF37) ),
introduced(definition,[new_symbols(definition,[spl64_28])],[avatar_definition]) ).
tff(f635,plain,
( ~ valid_chunk1(sK27,sK17,sF34,sF37)
| spl64_28 ),
inference(avatar_component_clause,[],[f633]) ).
tff(f636,plain,
~ spl64_28,
inference(avatar_split_clause,[],[f489,f633]) ).
tff(f658,definition,
( spl64_33
<=> ( sF63 = tb2t(sF62) ) ),
introduced(definition,[new_symbols(definition,[spl64_33])],[avatar_definition]) ).
tff(f660,plain,
( ( sF63 = tb2t(sF62) )
| ~ spl64_33 ),
inference(avatar_component_clause,[],[f658]) ).
tff(f661,plain,
spl64_33,
inference(avatar_split_clause,[],[f494,f658]) ).
tff(f663,definition,
( spl64_34
<=> ( t2tb1(sK17) = sF52 ) ),
introduced(definition,[new_symbols(definition,[spl64_34])],[avatar_definition]) ).
tff(f665,plain,
( ( t2tb1(sK17) = sF52 )
| ~ spl64_34 ),
inference(avatar_component_clause,[],[f663]) ).
tff(f666,plain,
spl64_34,
inference(avatar_split_clause,[],[f471,f663]) ).
tff(f693,definition,
( spl64_40
<=> chunk_valid_indexes1(sF34,sF37) ),
introduced(definition,[new_symbols(definition,[spl64_40])],[avatar_definition]) ).
tff(f695,plain,
( chunk_valid_indexes1(sF34,sF37)
| ~ spl64_40 ),
inference(avatar_component_clause,[],[f693]) ).
tff(f696,plain,
spl64_40,
inference(avatar_split_clause,[],[f483,f693]) ).
tff(f698,definition,
( spl64_41
<=> ( sF60 = tb2t(sF59) ) ),
introduced(definition,[new_symbols(definition,[spl64_41])],[avatar_definition]) ).
tff(f700,plain,
( ( sF60 = tb2t(sF59) )
| ~ spl64_41 ),
inference(avatar_component_clause,[],[f698]) ).
tff(f701,plain,
spl64_41,
inference(avatar_split_clause,[],[f487,f698]) ).
tff(f708,definition,
( spl64_43
<=> ( t2tb1(sK26) = sF55 ) ),
introduced(definition,[new_symbols(definition,[spl64_43])],[avatar_definition]) ).
tff(f710,plain,
( ( t2tb1(sK26) = sF55 )
| ~ spl64_43 ),
inference(avatar_component_clause,[],[f708]) ).
tff(f711,plain,
spl64_43,
inference(avatar_split_clause,[],[f478,f708]) ).
tff(f713,definition,
( spl64_44
<=> grid_eq_sub1(sK23,sF63,0,81) ),
introduced(definition,[new_symbols(definition,[spl64_44])],[avatar_definition]) ).
tff(f715,plain,
( grid_eq_sub1(sK23,sF63,0,81)
| ~ spl64_44 ),
inference(avatar_component_clause,[],[f713]) ).
tff(f716,plain,
spl64_44,
inference(avatar_split_clause,[],[f495,f713]) ).
tff(f718,definition,
( spl64_45
<=> ( set(int,int,sF58,sF52,sF61) = sF62 ) ),
introduced(definition,[new_symbols(definition,[spl64_45])],[avatar_definition]) ).
tff(f720,plain,
( ( set(int,int,sF58,sF52,sF61) = sF62 )
| ~ spl64_45 ),
inference(avatar_component_clause,[],[f718]) ).
tff(f721,plain,
spl64_45,
inference(avatar_split_clause,[],[f493,f718]) ).
tff(f763,definition,
( spl64_54
<=> ( sF57 = tb2t(sF56) ) ),
introduced(definition,[new_symbols(definition,[spl64_54])],[avatar_definition]) ).
tff(f765,plain,
( ( sF57 = tb2t(sF56) )
| ~ spl64_54 ),
inference(avatar_component_clause,[],[f763]) ).
tff(f766,plain,
spl64_54,
inference(avatar_split_clause,[],[f481,f763]) ).
tff(f778,definition,
( spl64_57
<=> is_index1(sK17) ),
introduced(definition,[new_symbols(definition,[spl64_57])],[avatar_definition]) ).
tff(f780,plain,
( is_index1(sK17)
| ~ spl64_57 ),
inference(avatar_component_clause,[],[f778]) ).
tff(f781,plain,
spl64_57,
inference(avatar_split_clause,[],[f326,f778]) ).
tff(f783,definition,
( spl64_58
<=> ( t2tb1(0) = sF61 ) ),
introduced(definition,[new_symbols(definition,[spl64_58])],[avatar_definition]) ).
tff(f785,plain,
( ( t2tb1(0) = sF61 )
| ~ spl64_58 ),
inference(avatar_component_clause,[],[f783]) ).
tff(f786,plain,
spl64_58,
inference(avatar_split_clause,[],[f491,f783]) ).
tff(f787,plain,
( ( set(int,int,sF58,sF52,t2tb1(0)) = sF62 )
| ~ spl64_45
| ~ spl64_58 ),
inference(forward_demodulation,[],[f720,f785]) ).
tff(f789,definition,
( spl64_59
<=> ( set(int,int,sF58,sF52,t2tb1(0)) = sF62 ) ),
introduced(definition,[new_symbols(definition,[spl64_59])],[avatar_definition]) ).
tff(f791,plain,
( ( set(int,int,sF58,sF52,t2tb1(0)) = sF62 )
| ~ spl64_59 ),
inference(avatar_component_clause,[],[f789]) ).
tff(f792,plain,
( spl64_59
| ~ spl64_45
| ~ spl64_58 ),
inference(avatar_split_clause,[],[f787,f783,f718,f789]) ).
tff(f796,plain,
( sort1(int,sF52)
| ~ spl64_34 ),
inference(superposition,[],[f404,f665]) ).
tff(f798,definition,
( spl64_60
<=> sort1(int,sF52) ),
introduced(definition,[new_symbols(definition,[spl64_60])],[avatar_definition]) ).
tff(f800,plain,
( sort1(int,sF52)
| ~ spl64_60 ),
inference(avatar_component_clause,[],[f798]) ).
tff(f801,plain,
( spl64_60
| ~ spl64_34 ),
inference(avatar_split_clause,[],[f796,f663,f798]) ).
tff(f802,plain,
( sort1(int,sF55)
| ~ spl64_43 ),
inference(superposition,[],[f404,f710]) ).
tff(f804,definition,
( spl64_61
<=> sort1(int,sF55) ),
introduced(definition,[new_symbols(definition,[spl64_61])],[avatar_definition]) ).
tff(f806,plain,
( sort1(int,sF55)
| ~ spl64_61 ),
inference(avatar_component_clause,[],[f804]) ).
tff(f807,plain,
( spl64_61
| ~ spl64_43 ),
inference(avatar_split_clause,[],[f802,f708,f804]) ).
tff(f882,plain,
! [X0: uni] : sort1(int,X0),
inference(superposition,[],[f404,f309]) ).
tff(f966,plain,
( ( t2tb(sF57) = sF56 )
| ~ spl64_54 ),
inference(superposition,[],[f405,f765]) ).
tff(f968,plain,
( ( t2tb(sF60) = sF59 )
| ~ spl64_41 ),
inference(superposition,[],[f405,f700]) ).
tff(f969,plain,
( ( sF62 = t2tb(sF63) )
| ~ spl64_33 ),
inference(superposition,[],[f405,f660]) ).
tff(f971,definition,
( spl64_85
<=> ( sF62 = t2tb(sF63) ) ),
introduced(definition,[new_symbols(definition,[spl64_85])],[avatar_definition]) ).
tff(f973,plain,
( ( sF62 = t2tb(sF63) )
| ~ spl64_85 ),
inference(avatar_component_clause,[],[f971]) ).
tff(f974,plain,
( spl64_85
| ~ spl64_33 ),
inference(avatar_split_clause,[],[f969,f658,f971]) ).
tff(f975,plain,
( ( t2tb(sK27) = sF59 )
| ~ spl64_21
| ~ spl64_41 ),
inference(forward_demodulation,[],[f968,f600]) ).
tff(f977,definition,
( spl64_86
<=> ( t2tb(sF57) = sF56 ) ),
introduced(definition,[new_symbols(definition,[spl64_86])],[avatar_definition]) ).
tff(f979,plain,
( ( t2tb(sF57) = sF56 )
| ~ spl64_86 ),
inference(avatar_component_clause,[],[f977]) ).
tff(f980,plain,
( spl64_86
| ~ spl64_54 ),
inference(avatar_split_clause,[],[f966,f763,f977]) ).
tff(f982,definition,
( spl64_87
<=> ( t2tb(sK27) = sF59 ) ),
introduced(definition,[new_symbols(definition,[spl64_87])],[avatar_definition]) ).
tff(f984,plain,
( ( t2tb(sK27) = sF59 )
| ~ spl64_87 ),
inference(avatar_component_clause,[],[f982]) ).
tff(f985,plain,
( spl64_87
| ~ spl64_21
| ~ spl64_41 ),
inference(avatar_split_clause,[],[f975,f698,f598,f982]) ).
tff(f1288,plain,
( ( sF37 = column_offsets1(sF50) )
| ~ spl64_22 ),
inference(superposition,[],[f308,f605]) ).
tff(f1294,definition,
( spl64_124
<=> ( sF37 = column_offsets1(sF50) ) ),
introduced(definition,[new_symbols(definition,[spl64_124])],[avatar_definition]) ).
tff(f1296,plain,
( ( sF37 = column_offsets1(sF50) )
| ~ spl64_124 ),
inference(avatar_component_clause,[],[f1294]) ).
tff(f1297,plain,
( spl64_124
| ~ spl64_22 ),
inference(avatar_split_clause,[],[f1288,f603,f1294]) ).
tff(f1578,plain,
( ( column_start1(sF50) = sF34 )
| ~ spl64_22 ),
inference(superposition,[],[f401,f605]) ).
tff(f1584,definition,
( spl64_151
<=> ( column_start1(sF50) = sF34 ) ),
introduced(definition,[new_symbols(definition,[spl64_151])],[avatar_definition]) ).
tff(f1586,plain,
( ( column_start1(sF50) = sF34 )
| ~ spl64_151 ),
inference(avatar_component_clause,[],[f1584]) ).
tff(f1587,plain,
( spl64_151
| ~ spl64_22 ),
inference(avatar_split_clause,[],[f1578,f603,f1584]) ).
tff(f1622,plain,
! [X2: sudoku_chunks1,X0: map_int_int,X1: $int] :
( ~ valid1(X2,X0)
| valid_chunk1(X0,X1,column_start1(X2),column_offsets1(X2))
| ~ is_index1(X1) ),
inference(resolution,[],[f368,f293]) ).
tff(f1634,plain,
( ! [X0: $int] :
( ~ is_index1(X0)
| valid_chunk1(sF57,X0,column_start1(sF50),column_offsets1(sF50)) )
| ~ spl64_13 ),
inference(resolution,[],[f1622,f560]) ).
tff(f1635,plain,
( ! [X0: $int] :
( ~ is_index1(X0)
| valid_chunk1(sF57,X0,column_start1(sF50),sF37) )
| ~ spl64_13
| ~ spl64_124 ),
inference(forward_demodulation,[],[f1634,f1296]) ).
tff(f1636,plain,
( ! [X0: $int] :
( valid_chunk1(sF57,X0,sF34,sF37)
| ~ is_index1(X0) )
| ~ spl64_13
| ~ spl64_124
| ~ spl64_151 ),
inference(forward_demodulation,[],[f1635,f1586]) ).
tff(f1983,plain,
( ( get(int,int,sF59,sF52) = sF55 )
| ~ sort1(int,sF55)
| ~ spl64_6 ),
inference(superposition,[],[f434,f525]) ).
tff(f1984,plain,
( ~ sort1(int,sF55)
| ( get(int,int,sF56,sF52) = sF55 )
| ~ spl64_12 ),
inference(superposition,[],[f434,f555]) ).
tff(f1987,plain,
( ( get(int,int,sF56,sF52) = sF55 )
| ~ spl64_12
| ~ spl64_61 ),
inference(forward_subsumption_resolution,[],[f1984,f806]) ).
tff(f1989,plain,
( ( get(int,int,sF59,sF52) = sF55 )
| ~ spl64_6
| ~ spl64_61 ),
inference(forward_subsumption_resolution,[],[f1983,f806]) ).
tff(f1991,definition,
( spl64_165
<=> ( get(int,int,sF56,sF52) = sF55 ) ),
introduced(definition,[new_symbols(definition,[spl64_165])],[avatar_definition]) ).
tff(f1994,plain,
( spl64_165
| ~ spl64_12
| ~ spl64_61 ),
inference(avatar_split_clause,[],[f1987,f804,f553,f1991]) ).
tff(f2001,definition,
( spl64_167
<=> ( get(int,int,sF59,sF52) = sF55 ) ),
introduced(definition,[new_symbols(definition,[spl64_167])],[avatar_definition]) ).
tff(f2004,plain,
( spl64_167
| ~ spl64_6
| ~ spl64_61 ),
inference(avatar_split_clause,[],[f1989,f804,f523,f2001]) ).
tff(f2117,plain,
( ! [X0: map_int_int] :
( ~ is_index1(sK17)
| ~ valid_chunk1(X0,sK17,sF34,sF37)
| ~ chunk_valid_indexes1(sF34,sF37)
| ~ included1(sK27,X0) )
| spl64_28 ),
inference(resolution,[],[f352,f635]) ).
tff(f2118,plain,
( ! [X0: map_int_int] :
( ~ chunk_valid_indexes1(sF34,sF37)
| ~ included1(sK27,X0)
| ~ valid_chunk1(X0,sK17,sF34,sF37) )
| spl64_28
| ~ spl64_57 ),
inference(forward_subsumption_resolution,[],[f2117,f780]) ).
tff(f2119,plain,
( ! [X0: map_int_int] :
( ~ included1(sK27,X0)
| ~ valid_chunk1(X0,sK17,sF34,sF37) )
| spl64_28
| ~ spl64_40
| ~ spl64_57 ),
inference(forward_subsumption_resolution,[],[f2118,f695]) ).
tff(f2486,plain,
( ! [X0: map_int_int] :
( ~ valid_chunk1(X0,sK17,sF34,sF37)
| ( tb2t1(get(int,int,t2tb(X0),t2tb1(sK7(X0,sK27)))) != tb2t1(get(int,int,t2tb(sK27),t2tb1(sK7(X0,sK27)))) ) )
| spl64_28
| ~ spl64_40
| ~ spl64_57 ),
inference(resolution,[],[f289,f2119]) ).
tff(f2487,plain,
( ! [X0: map_int_int] :
( ~ valid_chunk1(X0,sK17,sF34,sF37)
| ( tb2t1(get(int,int,t2tb(X0),t2tb1(sK7(X0,sK27)))) != tb2t1(get(int,int,sF59,t2tb1(sK7(X0,sK27)))) ) )
| spl64_28
| ~ spl64_40
| ~ spl64_57
| ~ spl64_87 ),
inference(forward_demodulation,[],[f2486,f984]) ).
tff(f2488,plain,
( ~ is_index1(sK17)
| ( tb2t1(get(int,int,sF59,t2tb1(sK7(sF57,sK27)))) != tb2t1(get(int,int,t2tb(sF57),t2tb1(sK7(sF57,sK27)))) )
| ~ spl64_13
| spl64_28
| ~ spl64_40
| ~ spl64_57
| ~ spl64_87
| ~ spl64_124
| ~ spl64_151 ),
inference(resolution,[],[f2487,f1636]) ).
tff(f2492,plain,
( ( tb2t1(get(int,int,sF59,t2tb1(sK7(sF57,sK27)))) != tb2t1(get(int,int,t2tb(sF57),t2tb1(sK7(sF57,sK27)))) )
| ~ spl64_13
| spl64_28
| ~ spl64_40
| ~ spl64_57
| ~ spl64_87
| ~ spl64_124
| ~ spl64_151 ),
inference(forward_subsumption_resolution,[],[f2488,f780]) ).
tff(f2495,plain,
( ( tb2t1(get(int,int,sF59,t2tb1(sK7(sF57,sK27)))) != tb2t1(get(int,int,sF56,t2tb1(sK7(sF57,sK27)))) )
| ~ spl64_13
| spl64_28
| ~ spl64_40
| ~ spl64_57
| ~ spl64_86
| ~ spl64_87
| ~ spl64_124
| ~ spl64_151 ),
inference(forward_demodulation,[],[f2492,f979]) ).
tff(f2498,definition,
( spl64_168
<=> ( tb2t1(get(int,int,sF59,t2tb1(sK7(sF57,sK27)))) = tb2t1(get(int,int,sF56,t2tb1(sK7(sF57,sK27)))) ) ),
introduced(definition,[new_symbols(definition,[spl64_168])],[avatar_definition]) ).
tff(f2500,plain,
( ( tb2t1(get(int,int,sF59,t2tb1(sK7(sF57,sK27)))) != tb2t1(get(int,int,sF56,t2tb1(sK7(sF57,sK27)))) )
| spl64_168 ),
inference(avatar_component_clause,[],[f2498]) ).
tff(f2501,plain,
( ~ spl64_168
| ~ spl64_13
| spl64_28
| ~ spl64_40
| ~ spl64_57
| ~ spl64_86
| ~ spl64_87
| ~ spl64_124
| ~ spl64_151 ),
inference(avatar_split_clause,[],[f2495,f1584,f1294,f982,f977,f778,f693,f633,f558,f2498]) ).
tff(f2738,plain,
( ! [X0: uni] :
( ( get(int,int,sF58,X0) = get(int,int,sF59,X0) )
| ( sF52 = X0 )
| ~ sort1(int,X0)
| ~ sort1(int,sF52) )
| ~ spl64_6 ),
inference(superposition,[],[f307,f525]) ).
tff(f2739,plain,
( ! [X0: uni] :
( ~ sort1(int,X0)
| ~ sort1(int,sF52)
| ( sF52 = X0 )
| ( get(int,int,sF56,X0) = get(int,int,sF51,X0) ) )
| ~ spl64_12 ),
inference(superposition,[],[f307,f555]) ).
tff(f2740,plain,
( ! [X0: uni] :
( ( sF52 = X0 )
| ( get(int,int,sF62,X0) = get(int,int,sF58,X0) )
| ~ sort1(int,sF52)
| ~ sort1(int,X0) )
| ~ spl64_59 ),
inference(superposition,[],[f307,f791]) ).
tff(f2744,plain,
( ! [X0: uni] :
( ~ sort1(int,X0)
| ( get(int,int,sF62,X0) = get(int,int,sF58,X0) )
| ( sF52 = X0 ) )
| ~ spl64_59
| ~ spl64_60 ),
inference(forward_subsumption_resolution,[],[f2740,f800]) ).
tff(f2746,plain,
( ! [X0: uni] :
( ~ sort1(int,X0)
| ( get(int,int,sF56,X0) = get(int,int,sF51,X0) )
| ( sF52 = X0 ) )
| ~ spl64_12
| ~ spl64_60 ),
inference(forward_subsumption_resolution,[],[f2739,f800]) ).
tff(f2747,plain,
( ! [X0: uni] :
( ( get(int,int,sF58,X0) = get(int,int,sF59,X0) )
| ~ sort1(int,X0)
| ( sF52 = X0 ) )
| ~ spl64_6
| ~ spl64_60 ),
inference(forward_subsumption_resolution,[],[f2738,f800]) ).
tff(f2749,plain,
( ! [X0: uni] :
( ( get(int,int,sF62,X0) = get(int,int,sF58,X0) )
| ( sF52 = X0 ) )
| ~ spl64_59
| ~ spl64_60 ),
inference(forward_subsumption_resolution,[],[f2744,f882]) ).
tff(f2751,plain,
( ! [X0: uni] :
( ( get(int,int,sF56,X0) = get(int,int,sF51,X0) )
| ( sF52 = X0 ) )
| ~ spl64_12
| ~ spl64_60 ),
inference(forward_subsumption_resolution,[],[f2746,f882]) ).
tff(f2752,plain,
( ! [X0: uni] :
( ( get(int,int,sF58,X0) = get(int,int,sF59,X0) )
| ( sF52 = X0 ) )
| ~ spl64_6
| ~ spl64_60 ),
inference(forward_subsumption_resolution,[],[f2747,f882]) ).
tff(f2974,plain,
( ! [X0: $int] :
( $less(X0,0)
| ( tb2t1(get(int,int,t2tb(sF63),t2tb1(X0))) = tb2t1(get(int,int,t2tb(sK23),t2tb1(X0))) )
| ~ $less(X0,81) )
| ~ spl64_44 ),
inference(resolution,[],[f297,f715]) ).
tff(f2978,plain,
( ! [X0: $int] :
( $less(X0,0)
| ( tb2t1(get(int,int,sF51,t2tb1(X0))) = tb2t1(get(int,int,t2tb(sF63),t2tb1(X0))) )
| ~ $less(X0,81) )
| ~ spl64_9
| ~ spl64_44 ),
inference(forward_demodulation,[],[f2974,f540]) ).
tff(f2979,plain,
( ! [X0: $int] :
( ( tb2t1(get(int,int,sF62,t2tb1(X0))) = tb2t1(get(int,int,sF51,t2tb1(X0))) )
| ~ $less(X0,81)
| $less(X0,0) )
| ~ spl64_9
| ~ spl64_44
| ~ spl64_85 ),
inference(forward_demodulation,[],[f2978,f973]) ).
tff(f2982,plain,
( ! [X0: uni] :
( ~ $less(tb2t1(X0),81)
| $less(tb2t1(X0),0)
| ( tb2t1(get(int,int,sF62,X0)) = tb2t1(get(int,int,sF51,X0)) ) )
| ~ spl64_9
| ~ spl64_44
| ~ spl64_85 ),
inference(superposition,[],[f2979,f309]) ).
tff(f3180,plain,
( ! [X0: uni] :
( ( tb2t1(get(int,int,sF62,X0)) = tb2t1(get(int,int,sF51,X0)) )
| ~ is_index1(tb2t1(X0))
| $less(tb2t1(X0),0) )
| ~ spl64_9
| ~ spl64_44
| ~ spl64_85 ),
inference(resolution,[],[f2982,f361]) ).
tff(f3188,plain,
( ! [X0: uni] :
( ~ is_index1(tb2t1(X0))
| ( tb2t1(get(int,int,sF62,X0)) = tb2t1(get(int,int,sF51,X0)) ) )
| ~ spl64_9
| ~ spl64_44
| ~ spl64_85 ),
inference(forward_subsumption_resolution,[],[f3180,f360]) ).
tff(f3200,plain,
( ! [X0: $int] :
( ~ is_index1(X0)
| ( tb2t1(get(int,int,sF62,t2tb1(X0))) = tb2t1(get(int,int,sF51,t2tb1(X0))) ) )
| ~ spl64_9
| ~ spl64_44
| ~ spl64_85 ),
inference(superposition,[],[f3188,f374]) ).
tff(f3215,plain,
( ! [X0: map_int_int,X1: map_int_int] :
( included1(X1,X0)
| ( tb2t1(get(int,int,sF51,t2tb1(sK7(X0,X1)))) = tb2t1(get(int,int,sF62,t2tb1(sK7(X0,X1)))) ) )
| ~ spl64_9
| ~ spl64_44
| ~ spl64_85 ),
inference(resolution,[],[f3200,f290]) ).
tff(f3236,plain,
( ! [X0: map_int_int] :
( ~ valid_chunk1(X0,sK17,sF34,sF37)
| ( tb2t1(get(int,int,sF62,t2tb1(sK7(X0,sK27)))) = tb2t1(get(int,int,sF51,t2tb1(sK7(X0,sK27)))) ) )
| ~ spl64_9
| spl64_28
| ~ spl64_40
| ~ spl64_44
| ~ spl64_57
| ~ spl64_85 ),
inference(resolution,[],[f3215,f2119]) ).
tff(f3246,plain,
( ( tb2t1(get(int,int,sF62,t2tb1(sK7(sF57,sK27)))) = tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27)))) )
| ~ is_index1(sK17)
| ~ spl64_9
| ~ spl64_13
| spl64_28
| ~ spl64_40
| ~ spl64_44
| ~ spl64_57
| ~ spl64_85
| ~ spl64_124
| ~ spl64_151 ),
inference(resolution,[],[f3236,f1636]) ).
tff(f3251,plain,
( ( tb2t1(get(int,int,sF62,t2tb1(sK7(sF57,sK27)))) = tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27)))) )
| ~ spl64_9
| ~ spl64_13
| spl64_28
| ~ spl64_40
| ~ spl64_44
| ~ spl64_57
| ~ spl64_85
| ~ spl64_124
| ~ spl64_151 ),
inference(forward_subsumption_resolution,[],[f3246,f780]) ).
tff(f3259,definition,
( spl64_218
<=> ( tb2t1(get(int,int,sF62,t2tb1(sK7(sF57,sK27)))) = tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27)))) ) ),
introduced(definition,[new_symbols(definition,[spl64_218])],[avatar_definition]) ).
tff(f3261,plain,
( ( tb2t1(get(int,int,sF62,t2tb1(sK7(sF57,sK27)))) = tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27)))) )
| ~ spl64_218 ),
inference(avatar_component_clause,[],[f3259]) ).
tff(f3262,plain,
( spl64_218
| ~ spl64_9
| ~ spl64_13
| spl64_28
| ~ spl64_40
| ~ spl64_44
| ~ spl64_57
| ~ spl64_85
| ~ spl64_124
| ~ spl64_151 ),
inference(avatar_split_clause,[],[f3251,f1584,f1294,f971,f778,f713,f693,f633,f558,f538,f3259]) ).
tff(f3268,plain,
( ( t2tb1(tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27))))) = get(int,int,sF62,t2tb1(sK7(sF57,sK27))) )
| ~ spl64_218 ),
inference(superposition,[],[f309,f3261]) ).
tff(f3293,plain,
( ( get(int,int,sF51,t2tb1(sK7(sF57,sK27))) = get(int,int,sF62,t2tb1(sK7(sF57,sK27))) )
| ~ spl64_218 ),
inference(forward_demodulation,[],[f3268,f309]) ).
tff(f3295,definition,
( spl64_224
<=> ( get(int,int,sF51,t2tb1(sK7(sF57,sK27))) = get(int,int,sF62,t2tb1(sK7(sF57,sK27))) ) ),
introduced(definition,[new_symbols(definition,[spl64_224])],[avatar_definition]) ).
tff(f3297,plain,
( ( get(int,int,sF51,t2tb1(sK7(sF57,sK27))) = get(int,int,sF62,t2tb1(sK7(sF57,sK27))) )
| ~ spl64_224 ),
inference(avatar_component_clause,[],[f3295]) ).
tff(f3298,plain,
( spl64_224
| ~ spl64_218 ),
inference(avatar_split_clause,[],[f3293,f3259,f3295]) ).
tff(f4877,plain,
( ( get(int,int,sF58,t2tb1(sK7(sF57,sK27))) = get(int,int,sF51,t2tb1(sK7(sF57,sK27))) )
| ( t2tb1(sK7(sF57,sK27)) = sF52 )
| ~ spl64_59
| ~ spl64_60
| ~ spl64_224 ),
inference(superposition,[],[f3297,f2749]) ).
tff(f4902,definition,
( spl64_307
<=> ( t2tb1(sK7(sF57,sK27)) = sF52 ) ),
introduced(definition,[new_symbols(definition,[spl64_307])],[avatar_definition]) ).
tff(f4903,plain,
( ( t2tb1(sK7(sF57,sK27)) != sF52 )
| spl64_307 ),
inference(avatar_component_clause,[],[f4902]) ).
tff(f4906,definition,
( spl64_308
<=> ( get(int,int,sF58,t2tb1(sK7(sF57,sK27))) = get(int,int,sF51,t2tb1(sK7(sF57,sK27))) ) ),
introduced(definition,[new_symbols(definition,[spl64_308])],[avatar_definition]) ).
tff(f4908,plain,
( ( get(int,int,sF58,t2tb1(sK7(sF57,sK27))) = get(int,int,sF51,t2tb1(sK7(sF57,sK27))) )
| ~ spl64_308 ),
inference(avatar_component_clause,[],[f4906]) ).
tff(f4986,plain,
( spl64_307
| spl64_308
| ~ spl64_59
| ~ spl64_60
| ~ spl64_224 ),
inference(avatar_split_clause,[],[f4877,f3295,f798,f789,f4906,f4902]) ).
tff(f5045,plain,
( ( get(int,int,sF56,sF52) != sF55 )
| ( t2tb1(sK7(sF57,sK27)) != sF52 )
| ( get(int,int,sF59,sF52) != sF55 )
| ( tb2t1(get(int,int,sF59,t2tb1(sK7(sF57,sK27)))) = tb2t1(get(int,int,sF56,t2tb1(sK7(sF57,sK27)))) ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
tff(f5162,plain,
( ( tb2t1(get(int,int,sF59,t2tb1(sK7(sF57,sK27)))) != tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27)))) )
| ( t2tb1(sK7(sF57,sK27)) = sF52 )
| ~ spl64_12
| ~ spl64_60
| spl64_168 ),
inference(superposition,[],[f2500,f2751]) ).
tff(f5171,plain,
( ( tb2t1(get(int,int,sF59,t2tb1(sK7(sF57,sK27)))) != tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27)))) )
| ~ spl64_12
| ~ spl64_60
| spl64_168
| spl64_307 ),
inference(forward_subsumption_resolution,[],[f5162,f4903]) ).
tff(f5176,definition,
( spl64_341
<=> ( tb2t1(get(int,int,sF59,t2tb1(sK7(sF57,sK27)))) = tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27)))) ) ),
introduced(definition,[new_symbols(definition,[spl64_341])],[avatar_definition]) ).
tff(f5178,plain,
( ( tb2t1(get(int,int,sF59,t2tb1(sK7(sF57,sK27)))) != tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27)))) )
| spl64_341 ),
inference(avatar_component_clause,[],[f5176]) ).
tff(f5179,plain,
( ~ spl64_341
| ~ spl64_12
| ~ spl64_60
| spl64_168
| spl64_307 ),
inference(avatar_split_clause,[],[f5171,f4902,f2498,f798,f553,f5176]) ).
tff(f9664,plain,
( ( tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27)))) != tb2t1(get(int,int,sF58,t2tb1(sK7(sF57,sK27)))) )
| ( t2tb1(sK7(sF57,sK27)) = sF52 )
| ~ spl64_6
| ~ spl64_60
| spl64_341 ),
inference(superposition,[],[f5178,f2752]) ).
tff(f9665,plain,
( ( tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27)))) != tb2t1(get(int,int,sF58,t2tb1(sK7(sF57,sK27)))) )
| ~ spl64_6
| ~ spl64_60
| spl64_307
| spl64_341 ),
inference(forward_subsumption_resolution,[],[f9664,f4903]) ).
tff(f9666,plain,
( ( tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27)))) != tb2t1(get(int,int,sF51,t2tb1(sK7(sF57,sK27)))) )
| ~ spl64_6
| ~ spl64_60
| spl64_307
| ~ spl64_308
| spl64_341 ),
inference(forward_demodulation,[],[f9665,f4908]) ).
tff(f9667,plain,
( $false
| ~ spl64_6
| ~ spl64_60
| spl64_307
| ~ spl64_308
| spl64_341 ),
inference(trivial_inequality_removal,[],[f9666]) ).
tff(f9668,plain,
( ~ spl64_6
| ~ spl64_60
| spl64_307
| ~ spl64_308
| spl64_341 ),
inference(avatar_contradiction_clause,[],[f9667]) ).
cnf(s6,plain,
spl64_6,
inference(sat_conversion,[],[f526]) ).
cnf(s9,plain,
spl64_9,
inference(sat_conversion,[],[f541]) ).
cnf(s12,plain,
spl64_12,
inference(sat_conversion,[],[f556]) ).
cnf(s13,plain,
spl64_13,
inference(sat_conversion,[],[f561]) ).
cnf(s22,plain,
spl64_21,
inference(sat_conversion,[],[f601]) ).
cnf(s23,plain,
spl64_22,
inference(sat_conversion,[],[f606]) ).
cnf(s29,plain,
~ spl64_28,
inference(sat_conversion,[],[f636]) ).
cnf(s35,plain,
spl64_33,
inference(sat_conversion,[],[f661]) ).
cnf(s36,plain,
spl64_34,
inference(sat_conversion,[],[f666]) ).
cnf(s42,plain,
spl64_40,
inference(sat_conversion,[],[f696]) ).
cnf(s43,plain,
spl64_41,
inference(sat_conversion,[],[f701]) ).
cnf(s45,plain,
spl64_43,
inference(sat_conversion,[],[f711]) ).
cnf(s46,plain,
spl64_44,
inference(sat_conversion,[],[f716]) ).
cnf(s47,plain,
spl64_45,
inference(sat_conversion,[],[f721]) ).
cnf(s56,plain,
spl64_54,
inference(sat_conversion,[],[f766]) ).
cnf(s60,plain,
spl64_57,
inference(sat_conversion,[],[f781]) ).
cnf(s61,plain,
spl64_58,
inference(sat_conversion,[],[f786]) ).
cnf(s62,plain,
( ~ spl64_45
| ~ spl64_58
| spl64_59 ),
inference(sat_conversion,[],[f792]) ).
cnf(s63,plain,
( ~ spl64_34
| spl64_60 ),
inference(sat_conversion,[],[f801]) ).
cnf(s64,plain,
( ~ spl64_43
| spl64_61 ),
inference(sat_conversion,[],[f807]) ).
cnf(s88,plain,
( ~ spl64_33
| spl64_85 ),
inference(sat_conversion,[],[f974]) ).
cnf(s89,plain,
( ~ spl64_54
| spl64_86 ),
inference(sat_conversion,[],[f980]) ).
cnf(s90,plain,
( ~ spl64_21
| ~ spl64_41
| spl64_87 ),
inference(sat_conversion,[],[f985]) ).
cnf(s131,plain,
( ~ spl64_22
| spl64_124 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s170,plain,
( ~ spl64_22
| spl64_151 ),
inference(sat_conversion,[],[f1587]) ).
cnf(s189,plain,
( ~ spl64_12
| ~ spl64_61
| spl64_165 ),
inference(sat_conversion,[],[f1994]) ).
cnf(s191,plain,
( ~ spl64_6
| ~ spl64_61
| spl64_167 ),
inference(sat_conversion,[],[f2004]) ).
cnf(s194,plain,
( ~ spl64_13
| spl64_28
| ~ spl64_40
| ~ spl64_57
| ~ spl64_86
| ~ spl64_87
| ~ spl64_124
| ~ spl64_151
| ~ spl64_168 ),
inference(sat_conversion,[],[f2501]) ).
cnf(s231,plain,
( ~ spl64_9
| ~ spl64_13
| spl64_28
| ~ spl64_40
| ~ spl64_44
| ~ spl64_57
| ~ spl64_85
| ~ spl64_124
| ~ spl64_151
| spl64_218 ),
inference(sat_conversion,[],[f3262]) ).
cnf(s236,plain,
( ~ spl64_218
| spl64_224 ),
inference(sat_conversion,[],[f3298]) ).
cnf(s315,plain,
( ~ spl64_59
| ~ spl64_60
| ~ spl64_224
| spl64_307
| spl64_308 ),
inference(sat_conversion,[],[f4986]) ).
cnf(s329,plain,
( ~ spl64_165
| ~ spl64_167
| spl64_168
| ~ spl64_307 ),
inference(sat_conversion,[],[f5045]) ).
cnf(s337,plain,
( ~ spl64_12
| ~ spl64_60
| spl64_168
| spl64_307
| ~ spl64_341 ),
inference(sat_conversion,[],[f5179]) ).
cnf(s729,plain,
( ~ spl64_6
| ~ spl64_60
| spl64_307
| ~ spl64_308
| spl64_341 ),
inference(sat_conversion,[],[f9668]) ).
cnf(s730,plain,
spl64_86,
inference(rat,[],[s89,s56]) ).
cnf(s740,plain,
spl64_59,
inference(rat,[],[s62,s61,s47]) ).
cnf(s743,plain,
spl64_61,
inference(rat,[],[s64,s45]) ).
cnf(s753,plain,
spl64_60,
inference(rat,[],[s63,s36]) ).
cnf(s754,plain,
spl64_85,
inference(rat,[],[s88,s35]) ).
cnf(s768,plain,
spl64_151,
inference(rat,[],[s170,s23]) ).
cnf(s771,plain,
spl64_124,
inference(rat,[],[s131,s23]) ).
cnf(s804,plain,
spl64_87,
inference(rat,[],[s90,s43,s22]) ).
cnf(s830,plain,
~ spl64_168,
inference(rat,[],[s194,s804,s768,s771,s29,s730,s60,s42,s13]) ).
cnf(s831,plain,
spl64_165,
inference(rat,[],[s189,s743,s12]) ).
cnf(s833,plain,
spl64_218,
inference(rat,[],[s231,s13,s768,s771,s754,s60,s46,s42,s29,s9]) ).
cnf(s838,plain,
spl64_224,
inference(rat,[],[s236,s833]) ).
cnf(s839,plain,
spl64_167,
inference(rat,[],[s191,s743,s6]) ).
cnf(s840,plain,
~ spl64_307,
inference(rat,[],[s329,s831,s830,s839]) ).
cnf(s843,plain,
spl64_308,
inference(rat,[],[s315,s838,s753,s740,s840]) ).
cnf(s844,plain,
~ spl64_341,
inference(rat,[],[s337,s12,s830,s753,s840]) ).
cnf(s845,plain,
$false,
inference(rat,[],[s729,s840,s6,s753,s844,s843]) ).
tff(f9669,plain,
$false,
inference(avatar_sat_refutation,[],[s845]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW646_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.28 % Computer : n020.cluster.edu
% 0.24/0.28 % Model : x86_64 x86_64
% 0.24/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.24/0.28 % Memory : 8046.5625MB
% 0.24/0.28 % OS : Linux 6.8.0-71-generic
% 0.24/0.28 % CPULimit : 300
% 0.24/0.28 % WCLimit : 300
% 0.24/0.28 % DateTime : Mon Sep 28 14:24:19 UTC 2026
% 0.24/0.28 % CPUTime :
% 0.24/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.32 Running first-order theorem proving
% 0.24/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.72/1.87 % (198759)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.72/1.87 % (198770)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2663237040:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.72/1.87 % (198774)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1216631830:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.72/1.87 % (198772)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1044202624:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.72/1.87 % (198771)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2123969097:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.72/1.87 % (198773)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2048114879:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.72/1.87 % (198768)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1718065911:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.72/1.87 % (198769)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1425827750:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.72/1.87 % (198772)Instruction limit reached!
% 5.72/1.87 % (198772)------------------------------
% 5.72/1.87 % (198772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.72/1.87 % (198772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/1.87 % (198772)CaDiCaL version: 2.1.3
% 5.72/1.87 % (198772)Termination reason: Instruction limit
% 5.72/1.87 % (198772)Termination phase: Naming
% 5.72/1.87 % (198772)Time elapsed: 0.005 s
% 5.72/1.87 % (198772)Peak memory usage: 85 MB
% 5.72/1.87 % (198772)Instructions burned: 4 (million)
% 5.72/1.87 % (198771)Instruction limit reached!
% 5.72/1.87 % (198771)------------------------------
% 5.72/1.87 % (198771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.72/1.87 % (198771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/1.87 % (198771)CaDiCaL version: 2.1.3
% 5.72/1.87 % (198771)Termination reason: Instruction limit
% 5.72/1.87 % (198771)Termination phase: Preprocessing 3
% 5.72/1.87 % (198771)Time elapsed: 0.008 s
% 5.72/1.87 % (198771)Peak memory usage: 86 MB
% 5.72/1.87 % (198771)Instructions burned: 7 (million)
% 5.72/1.87 % (198768)Instruction limit reached!
% 5.72/1.87 % (198768)------------------------------
% 5.72/1.87 % (198768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.72/1.87 % (198768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/1.87 % (198768)CaDiCaL version: 2.1.3
% 5.72/1.87 % (198768)Termination reason: Instruction limit
% 5.72/1.87 % (198768)Termination phase: Function definition elimination
% 5.72/1.87 % (198768)Time elapsed: 0.012 s
% 5.72/1.87 % (198768)Peak memory usage: 86 MB
% 5.72/1.87 % (198768)Instructions burned: 12 (million)
% 5.72/1.87 % (198770)Instruction limit reached!
% 5.72/1.87 % (198770)------------------------------
% 5.72/1.87 % (198770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.72/1.87 % (198770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/1.87 % (198770)CaDiCaL version: 2.1.3
% 5.72/1.87 % (198770)Termination reason: Instruction limit
% 5.72/1.87 % (198770)Termination phase: Saturation
% 5.72/1.87 % (198770)Time elapsed: 0.125 s
% 5.72/1.87 % (198770)Peak memory usage: 117 MB
% 5.72/1.87 % (198770)Instructions burned: 201 (million)
% 5.72/1.87 % (198774)Instruction limit reached!
% 5.72/1.87 % (198774)------------------------------
% 5.72/1.87 % (198774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.72/1.87 % (198774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/1.87 % (198774)CaDiCaL version: 2.1.3
% 5.72/1.87 % (198774)Termination reason: Instruction limit
% 5.72/1.87 % (198774)Termination phase: Saturation
% 5.72/1.87 % (198774)Time elapsed: 0.062 s
% 5.72/1.87 % (198774)Peak memory usage: 116 MB
% 5.72/1.87 % (198774)Instructions burned: 33 (million)
% 5.72/1.87 % (198773)Instruction limit reached!
% 5.72/1.87 % (198773)------------------------------
% 5.72/1.87 % (198773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.72/1.87 % (198773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/1.87 % (198773)CaDiCaL version: 2.1.3
% 8.22/2.09 % (198773)Termination reason: Instruction limit
% 8.22/2.09 % (198773)Termination phase: Saturation
% 8.22/2.09 % (198773)Time elapsed: 0.077 s
% 8.22/2.09 % (198773)Peak memory usage: 116 MB
% 8.22/2.09 % (198773)Instructions burned: 47 (million)
% 8.22/2.09 % (198785)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3206034998:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 8.22/2.09 % (198783)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=766072702:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 8.22/2.09 % (198785)Instruction limit reached!
% 8.22/2.09 % (198785)------------------------------
% 8.22/2.09 % (198785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.22/2.09 % (198785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.22/2.09 % (198785)CaDiCaL version: 2.1.3
% 8.22/2.09 % (198785)Termination reason: Instruction limit
% 8.22/2.09 % (198785)Termination phase: Saturation
% 8.22/2.09 % (198785)Time elapsed: 0.017 s
% 8.22/2.09 % (198785)Peak memory usage: 89 MB
% 8.22/2.09 % (198785)Instructions burned: 25 (million)
% 8.22/2.09 % (198782)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3227619821:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 8.22/2.09 % (198784)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2338522826:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 8.22/2.09 % (198782)Instruction limit reached!
% 8.22/2.09 % (198782)------------------------------
% 8.22/2.09 % (198782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.22/2.09 % (198782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.22/2.09 % (198782)CaDiCaL version: 2.1.3
% 8.22/2.09 % (198782)Termination reason: Instruction limit
% 8.22/2.09 % (198782)Termination phase: Saturation
% 8.22/2.09 % (198782)Time elapsed: 0.014 s
% 8.22/2.09 % (198782)Peak memory usage: 88 MB
% 8.22/2.09 % (198782)Instructions burned: 14 (million)
% 8.22/2.09 % (198784)Instruction limit reached!
% 8.22/2.09 % (198784)------------------------------
% 8.22/2.09 % (198784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.22/2.09 % (198784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.22/2.09 % (198784)CaDiCaL version: 2.1.3
% 8.22/2.09 % (198784)Termination reason: Instruction limit
% 8.22/2.09 % (198784)Termination phase: Saturation
% 8.22/2.09 % (198784)Time elapsed: 0.016 s
% 8.22/2.09 % (198784)Peak memory usage: 89 MB
% 8.22/2.09 % (198784)Instructions burned: 16 (million)
% 8.22/2.09 % (198783)Instruction limit reached!
% 8.22/2.09 % (198783)------------------------------
% 8.22/2.09 % (198783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.22/2.09 % (198783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.22/2.09 % (198783)CaDiCaL version: 2.1.3
% 8.22/2.09 % (198783)Termination reason: Instruction limit
% 8.22/2.09 % (198783)Termination phase: Saturation
% 8.22/2.09 % (198783)Time elapsed: 0.034 s
% 8.22/2.09 % (198783)Peak memory usage: 89 MB
% 8.22/2.09 % (198783)Instructions burned: 29 (million)
% 8.22/2.09 % (198786)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=727426303:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 8.22/2.09 % (198787)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1454863892:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 8.22/2.09 % (198769)Instruction limit reached!
% 8.22/2.09 % (198769)------------------------------
% 8.22/2.09 % (198769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.22/2.09 % (198769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.22/2.09 % (198769)CaDiCaL version: 2.1.3
% 8.22/2.09 % (198769)Termination reason: Instruction limit
% 8.22/2.09 % (198769)Termination phase: Saturation
% 8.22/2.09 % (198769)Time elapsed: 0.356 s
% 8.22/2.09 % (198769)Peak memory usage: 118 MB
% 8.22/2.09 % (198769)Instructions burned: 307 (million)
% 8.22/2.09 % (198786)Instruction limit reached!
% 8.22/2.09 % (198786)------------------------------
% 8.22/2.09 % (198786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.22/2.09 % (198786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/2.41 % (198786)CaDiCaL version: 2.1.3
% 9.90/2.41 % (198786)Termination reason: Instruction limit
% 9.90/2.41 % (198786)Termination phase: Saturation
% 9.90/2.41 % (198786)Time elapsed: 0.028 s
% 9.90/2.41 % (198786)Peak memory usage: 90 MB
% 9.90/2.41 % (198786)Instructions burned: 27 (million)
% 9.90/2.41 % (198787)Instruction limit reached!
% 9.90/2.41 % (198787)------------------------------
% 9.90/2.41 % (198787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/2.41 % (198787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/2.41 % (198787)CaDiCaL version: 2.1.3
% 9.90/2.41 % (198787)Termination reason: Instruction limit
% 9.90/2.41 % (198787)Termination phase: Saturation
% 9.90/2.41 % (198787)Time elapsed: 0.075 s
% 9.90/2.41 % (198787)Peak memory usage: 89 MB
% 9.90/2.41 % (198787)Instructions burned: 86 (million)
% 9.90/2.41 % (198792)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3010582129:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi)
% 9.90/2.41 % (198792)Instruction limit reached!
% 9.90/2.41 % (198792)------------------------------
% 9.90/2.41 % (198792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/2.41 % (198792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/2.41 % (198792)CaDiCaL version: 2.1.3
% 9.90/2.41 % (198792)Termination reason: Instruction limit
% 9.90/2.41 % (198792)Termination phase: Preprocessing 1
% 9.90/2.41 % (198792)Time elapsed: 0.002 s
% 9.90/2.41 % (198792)Peak memory usage: 86 MB
% 9.90/2.41 % (198792)Instructions burned: 4 (million)
% 9.90/2.41 % (198795)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=17746041:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 9.90/2.41 % (198794)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2901786443:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 9.90/2.41 % (198793)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=411504742:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 9.90/2.41 % (198794)Instruction limit reached!
% 9.90/2.41 % (198794)------------------------------
% 9.90/2.41 % (198794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/2.41 % (198794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/2.41 % (198794)CaDiCaL version: 2.1.3
% 9.90/2.41 % (198794)Termination reason: Instruction limit
% 9.90/2.41 % (198794)Termination phase: Unused predicate definition removal
% 9.90/2.41 % (198794)Time elapsed: 0.004 s
% 9.90/2.41 % (198794)Peak memory usage: 85 MB
% 9.90/2.41 % (198794)Instructions burned: 4 (million)
% 9.90/2.41 % (198795)Instruction limit reached!
% 9.90/2.41 % (198795)------------------------------
% 9.90/2.41 % (198795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/2.41 % (198795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/2.41 % (198795)CaDiCaL version: 2.1.3
% 9.90/2.41 % (198795)Termination reason: Instruction limit
% 9.90/2.41 % (198795)Termination phase: Saturation
% 9.90/2.41 % (198795)Time elapsed: 0.101 s
% 9.90/2.41 % (198795)Peak memory usage: 134 MB
% 9.90/2.41 % (198795)Instructions burned: 66 (million)
% 9.90/2.41 % (198799)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=2060146308:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 9.90/2.41 % (198799)Instruction limit reached!
% 9.90/2.41 % (198799)------------------------------
% 9.90/2.41 % (198799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/2.41 % (198798)lrs+10_1_thi=all:si=on:fd=off:random_seed=4084181350:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi)
% 9.90/2.41 % (198799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/2.41 % (198799)CaDiCaL version: 2.1.3
% 9.90/2.41 % (198799)Termination reason: Instruction limit
% 9.90/2.41 % (198799)Termination phase: Property scanning
% 9.90/2.41 % (198799)Time elapsed: 0.007 s
% 9.90/2.41 % (198799)Peak memory usage: 87 MB
% 9.90/2.41 % (198799)Instructions burned: 10 (million)
% 9.90/2.41 % (198801)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2562799811:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi)
% 9.90/2.41 % (198801)Instruction limit reached!
% 11.47/2.78 % (198801)------------------------------
% 11.47/2.78 % (198801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.78 % (198801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.78 % (198801)CaDiCaL version: 2.1.3
% 11.47/2.78 % (198801)Termination reason: Instruction limit
% 11.47/2.78 % (198801)Termination phase: Preprocessing 2
% 11.47/2.78 % (198801)Time elapsed: 0.002 s
% 11.47/2.78 % (198801)Peak memory usage: 86 MB
% 11.47/2.78 % (198801)Instructions burned: 3 (million)
% 11.47/2.78 % (198802)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2565646460:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 11.47/2.78 % (198802)Instruction limit reached!
% 11.47/2.78 % (198802)------------------------------
% 11.47/2.78 % (198802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.78 % (198802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.78 % (198802)CaDiCaL version: 2.1.3
% 11.47/2.78 % (198802)Termination reason: Instruction limit
% 11.47/2.78 % (198802)Termination phase: Property scanning
% 11.47/2.78 % (198802)Time elapsed: 0.003 s
% 11.47/2.78 % (198802)Peak memory usage: 85 MB
% 11.47/2.78 % (198802)Instructions burned: 3 (million)
% 11.47/2.78 % (198798)Instruction limit reached!
% 11.47/2.78 % (198798)------------------------------
% 11.47/2.78 % (198798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.78 % (198798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.78 % (198798)CaDiCaL version: 2.1.3
% 11.47/2.78 % (198798)Termination reason: Instruction limit
% 11.47/2.78 % (198798)Termination phase: Saturation
% 11.47/2.78 % (198798)Time elapsed: 0.092 s
% 11.47/2.78 % (198798)Peak memory usage: 118 MB
% 11.47/2.78 % (198798)Instructions burned: 53 (million)
% 11.47/2.78 % (198793)Instruction limit reached!
% 11.47/2.78 % (198793)------------------------------
% 11.47/2.78 % (198793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.78 % (198793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.78 % (198793)CaDiCaL version: 2.1.3
% 11.47/2.78 % (198793)Termination reason: Instruction limit
% 11.47/2.78 % (198793)Termination phase: Saturation
% 11.47/2.78 % (198793)Time elapsed: 0.191 s
% 11.47/2.78 % (198793)Peak memory usage: 92 MB
% 11.47/2.78 % (198793)Instructions burned: 181 (million)
% 11.47/2.78 % (198806)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3360886439:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi)
% 11.47/2.78 % (198808)dis+10_1_si=on:random_seed=1522524891:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 11.47/2.78 % (198808)Instruction limit reached!
% 11.47/2.78 % (198808)------------------------------
% 11.47/2.78 % (198808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.78 % (198808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.78 % (198808)CaDiCaL version: 2.1.3
% 11.47/2.78 % (198808)Termination reason: Instruction limit
% 11.47/2.78 % (198808)Termination phase: Property scanning
% 11.47/2.78 % (198808)Time elapsed: 0.010 s
% 11.47/2.78 % (198808)Peak memory usage: 87 MB
% 11.47/2.78 % (198808)Instructions burned: 10 (million)
% 11.47/2.78 % (198814)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1594938507:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 11.47/2.78 % (198816)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=894076040: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_2990 on theBenchmark for (2990ds/35Mi)
% 11.47/2.78 % (198814)Refutation not found, incomplete strategy
% 11.47/2.78 % (198814)------------------------------
% 11.47/2.78 % (198814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.78 % (198814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.78 % (198814)CaDiCaL version: 2.1.3
% 11.47/2.78 % (198814)Termination reason: Refutation not found, incomplete strategy
% 11.47/2.78 % (198814)Time elapsed: 0.023 s
% 11.47/2.78 % (198814)Peak memory usage: 89 MB
% 11.47/2.78 % (198814)Instructions burned: 21 (million)
% 11.47/2.78 % (198816)Instruction limit reached!
% 11.47/2.78 % (198816)------------------------------
% 11.47/2.78 % (198816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.78 % (198816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.28 % (198816)CaDiCaL version: 2.1.3
% 16.16/3.28 % (198816)Termination reason: Instruction limit
% 16.16/3.28 % (198816)Termination phase: Saturation
% 16.16/3.28 % (198816)Time elapsed: 0.022 s
% 16.16/3.28 % (198816)Peak memory usage: 89 MB
% 16.16/3.28 % (198816)Instructions burned: 36 (million)
% 16.16/3.28 % (198806)Instruction limit reached!
% 16.16/3.28 % (198806)------------------------------
% 16.16/3.28 % (198806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.28 % (198806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.28 % (198806)CaDiCaL version: 2.1.3
% 16.16/3.28 % (198806)Termination reason: Instruction limit
% 16.16/3.28 % (198806)Termination phase: Saturation
% 16.16/3.28 % (198806)Time elapsed: 0.159 s
% 16.16/3.28 % (198806)Peak memory usage: 117 MB
% 16.16/3.28 % (198806)Instructions burned: 127 (million)
% 16.16/3.28 % (198818)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2186183562:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 16.16/3.28 % (198820)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1354669890:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi)
% 16.16/3.28 % (198818)Instruction limit reached!
% 16.16/3.28 % (198818)------------------------------
% 16.16/3.28 % (198818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.28 % (198818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.28 % (198818)CaDiCaL version: 2.1.3
% 16.16/3.28 % (198818)Termination reason: Instruction limit
% 16.16/3.28 % (198818)Termination phase: Property scanning
% 16.16/3.28 % (198818)Time elapsed: 0.002 s
% 16.16/3.28 % (198818)Peak memory usage: 85 MB
% 16.16/3.28 % (198818)Instructions burned: 2 (million)
% 16.16/3.28 % (198819)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2392949699:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 16.16/3.28 % (198819)Instruction limit reached!
% 16.16/3.28 % (198819)------------------------------
% 16.16/3.28 % (198819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.28 % (198819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.28 % (198819)CaDiCaL version: 2.1.3
% 16.16/3.28 % (198819)Termination reason: Instruction limit
% 16.16/3.28 % (198819)Termination phase: Property scanning
% 16.16/3.28 % (198819)Time elapsed: 0.009 s
% 16.16/3.28 % (198819)Peak memory usage: 86 MB
% 16.16/3.28 % (198819)Instructions burned: 9 (million)
% 16.16/3.28 % (198826)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2545073039:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi)
% 16.16/3.28 % (198824)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=874070819:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 16.16/3.28 % (198824)Instruction limit reached!
% 16.16/3.28 % (198824)------------------------------
% 16.16/3.28 % (198824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.28 % (198824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.28 % (198824)CaDiCaL version: 2.1.3
% 16.16/3.28 % (198824)Termination reason: Instruction limit
% 16.16/3.28 % (198824)Termination phase: Property scanning
% 16.16/3.28 % (198824)Time elapsed: 0.012 s
% 16.16/3.28 % (198824)Peak memory usage: 87 MB
% 16.16/3.28 % (198824)Instructions burned: 13 (million)
% 16.16/3.28 % (198827)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3046818003:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi)
% 16.16/3.28 % (198832)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=3455734419:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi)
% 16.16/3.28 % (198827)Instruction limit reached!
% 16.16/3.28 % (198827)------------------------------
% 16.16/3.28 % (198827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.28 % (198827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.28 % (198827)CaDiCaL version: 2.1.3
% 16.16/3.28 % (198827)Termination reason: Instruction limit
% 16.16/3.28 % (198827)Termination phase: Property scanning
% 16.16/3.28 % (198827)Time elapsed: 0.010 s
% 16.16/3.28 % (198827)Peak memory usage: 86 MB
% 18.11/3.64 % (198827)Instructions burned: 10 (million)
% 18.11/3.64 % (198830)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=207541375:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi)
% 18.11/3.64 % (198832)Instruction limit reached!
% 18.11/3.64 % (198832)------------------------------
% 18.11/3.64 % (198832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.11/3.64 % (198832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.11/3.64 % (198832)CaDiCaL version: 2.1.3
% 18.11/3.64 % (198832)Termination reason: Instruction limit
% 18.11/3.64 % (198832)Termination phase: Saturation
% 18.11/3.64 % (198832)Time elapsed: 0.046 s
% 18.11/3.64 % (198832)Peak memory usage: 90 MB
% 18.11/3.64 % (198832)Instructions burned: 75 (million)
% 18.11/3.64 % (198814)------------------------------
% 18.11/3.64 % (198814)------------------------------
% 18.11/3.64 % (198826)Instruction limit reached!
% 18.11/3.64 % (198826)------------------------------
% 18.11/3.64 % (198826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.11/3.64 % (198826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.11/3.64 % (198826)CaDiCaL version: 2.1.3
% 18.11/3.64 % (198826)Termination reason: Instruction limit
% 18.11/3.64 % (198826)Termination phase: Saturation
% 18.11/3.64 % (198826)Time elapsed: 0.262 s
% 18.11/3.64 % (198826)Peak memory usage: 117 MB
% 18.11/3.64 % (198826)Instructions burned: 227 (million)
% 18.11/3.64 % (198830)Instruction limit reached!
% 18.11/3.64 % (198830)------------------------------
% 18.11/3.64 % (198830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.11/3.64 % (198830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.11/3.64 % (198830)CaDiCaL version: 2.1.3
% 18.11/3.64 % (198830)Termination reason: Instruction limit
% 18.11/3.64 % (198830)Termination phase: Saturation
% 18.11/3.64 % (198830)Time elapsed: 0.127 s
% 18.11/3.64 % (198830)Peak memory usage: 133 MB
% 18.11/3.64 % (198830)Instructions burned: 72 (million)
% 18.11/3.64 % (198820)Instruction limit reached!
% 18.11/3.64 % (198820)------------------------------
% 18.11/3.64 % (198820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.11/3.64 % (198820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.11/3.64 % (198820)CaDiCaL version: 2.1.3
% 18.11/3.64 % (198820)Termination reason: Instruction limit
% 18.11/3.64 % (198820)Termination phase: Saturation
% 18.11/3.64 % (198820)Time elapsed: 0.373 s
% 18.11/3.64 % (198820)Peak memory usage: 92 MB
% 18.11/3.64 % (198820)Instructions burned: 370 (million)
% 18.11/3.64 % (198835)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=671079362:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2986 on theBenchmark for (2986ds/294Mi)
% 18.11/3.64 % (198838)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3274972071:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/130Mi)
% 18.11/3.64 % (198840)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1227652228:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 18.11/3.64 % (198838)Instruction limit reached!
% 18.11/3.64 % (198838)------------------------------
% 18.11/3.64 % (198838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.11/3.64 % (198838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.11/3.64 % (198838)CaDiCaL version: 2.1.3
% 18.11/3.64 % (198838)Termination reason: Instruction limit
% 18.11/3.64 % (198838)Termination phase: Saturation
% 18.11/3.64 % (198838)Time elapsed: 0.110 s
% 18.11/3.64 % (198838)Peak memory usage: 117 MB
% 18.11/3.64 % (198838)Instructions burned: 131 (million)
% 18.11/3.64 % (198841)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=825850822:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi)
% 18.11/3.64 % (198840)Instruction limit reached!
% 18.11/3.64 % (198840)------------------------------
% 18.11/3.64 % (198840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.11/3.64 % (198840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.11/3.64 % (198840)CaDiCaL version: 2.1.3
% 18.11/3.64 % (198840)Termination reason: Instruction limit
% 18.11/3.64 % (198840)Termination phase: Saturation
% 18.11/3.64 % (198840)Time elapsed: 0.109 s
% 18.11/3.64 % (198840)Peak memory usage: 134 MB
% 18.11/3.64 % (198840)Instructions burned: 131 (million)
% 22.23/4.12 % (198842)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1287362818:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 22.23/4.12 % (198845)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2846016570:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi)
% 22.23/4.12 % (198843)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2800626173:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/598Mi)
% 22.23/4.12 % (198841)Instruction limit reached!
% 22.23/4.12 % (198841)------------------------------
% 22.23/4.12 % (198841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.23/4.12 % (198841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.23/4.12 % (198841)CaDiCaL version: 2.1.3
% 22.23/4.12 % (198841)Termination reason: Instruction limit
% 22.23/4.12 % (198841)Termination phase: Saturation
% 22.23/4.12 % (198841)Time elapsed: 0.097 s
% 22.23/4.12 % (198841)Peak memory usage: 133 MB
% 22.23/4.12 % (198841)Instructions burned: 40 (million)
% 22.23/4.12 % (198835)Instruction limit reached!
% 22.23/4.12 % (198835)------------------------------
% 22.23/4.12 % (198835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.23/4.12 % (198835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.23/4.12 % (198835)CaDiCaL version: 2.1.3
% 22.23/4.12 % (198835)Termination reason: Instruction limit
% 22.23/4.12 % (198835)Termination phase: Saturation
% 22.23/4.12 % (198835)Time elapsed: 0.317 s
% 22.23/4.12 % (198835)Peak memory usage: 92 MB
% 22.23/4.12 % (198835)Instructions burned: 294 (million)
% 22.23/4.12 % (198848)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=955229339:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi)
% 22.23/4.12 % (198850)dis+10_1_si=on:random_seed=1302591397:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi)
% 22.23/4.12 % (198845)Instruction limit reached!
% 22.23/4.12 % (198845)------------------------------
% 22.23/4.12 % (198845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.23/4.12 % (198845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.23/4.12 % (198845)CaDiCaL version: 2.1.3
% 22.23/4.12 % (198845)Termination reason: Instruction limit
% 22.23/4.12 % (198845)Termination phase: Saturation
% 22.23/4.12 % (198845)Time elapsed: 0.166 s
% 22.23/4.12 % (198845)Peak memory usage: 117 MB
% 22.23/4.12 % (198845)Instructions burned: 131 (million)
% 22.23/4.12 % (198842)Instruction limit reached!
% 22.23/4.12 % (198842)------------------------------
% 22.23/4.12 % (198842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.23/4.12 % (198842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.23/4.12 % (198842)CaDiCaL version: 2.1.3
% 22.23/4.12 % (198842)Termination reason: Instruction limit
% 22.23/4.12 % (198842)Termination phase: Saturation
% 22.23/4.12 % (198842)Time elapsed: 0.284 s
% 22.23/4.12 % (198842)Peak memory usage: 92 MB
% 22.23/4.12 % (198842)Instructions burned: 308 (million)
% 22.23/4.12 % (198854)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3327735730:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi)
% 22.23/4.12 % (198855)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3121290796:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi)
% 22.23/4.12 % (198848)Instruction limit reached!
% 22.23/4.12 % (198848)------------------------------
% 22.23/4.12 % (198848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.23/4.12 % (198848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.23/4.12 % (198848)CaDiCaL version: 2.1.3
% 22.23/4.12 % (198848)Termination reason: Instruction limit
% 22.23/4.12 % (198848)Termination phase: Saturation
% 22.23/4.12 % (198848)Time elapsed: 0.279 s
% 22.23/4.12 % (198848)Peak memory usage: 117 MB
% 22.23/4.12 % (198848)Instructions burned: 259 (million)
% 22.23/4.12 % (198855)Instruction limit reached!
% 22.23/4.12 % (198855)------------------------------
% 22.23/4.12 % (198855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.23/4.12 % (198855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.23/4.12 % (198855)CaDiCaL version: 2.1.3
% 22.23/4.12 % (198855)Termination reason: Instruction limit
% 24.22/4.64 % (198855)Termination phase: Saturation
% 24.22/4.64 % (198855)Time elapsed: 0.154 s
% 24.22/4.64 % (198855)Peak memory usage: 90 MB
% 24.22/4.64 % (198855)Instructions burned: 142 (million)
% 24.22/4.64 % (198858)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1298110837:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi)
% 24.22/4.64 % (198859)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3624895180:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi)
% 24.22/4.64 % (198858)Instruction limit reached!
% 24.22/4.64 % (198858)------------------------------
% 24.22/4.64 % (198858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.22/4.64 % (198858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.22/4.64 % (198858)CaDiCaL version: 2.1.3
% 24.22/4.64 % (198858)Termination reason: Instruction limit
% 24.22/4.64 % (198858)Termination phase: Saturation
% 24.22/4.64 % (198858)Time elapsed: 0.099 s
% 24.22/4.64 % (198858)Peak memory usage: 116 MB
% 24.22/4.64 % (198858)Instructions burned: 66 (million)
% 24.22/4.64 % (198862)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=1238080250:s2a=on:i=128:s2at=5:ins=3:rtra=on_2977 on theBenchmark for (2977ds/128Mi)
% 24.22/4.64 % (198843)Instruction limit reached!
% 24.22/4.64 % (198843)------------------------------
% 24.22/4.64 % (198843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.22/4.64 % (198843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.22/4.64 % (198843)CaDiCaL version: 2.1.3
% 24.22/4.64 % (198843)Termination reason: Instruction limit
% 24.22/4.64 % (198843)Termination phase: Saturation
% 24.22/4.64 % (198843)Time elapsed: 0.629 s
% 24.22/4.64 % (198843)Peak memory usage: 139 MB
% 24.22/4.64 % (198843)Instructions burned: 598 (million)
% 24.22/4.64 % (198859)Instruction limit reached!
% 24.22/4.64 % (198859)------------------------------
% 24.22/4.64 % (198859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.22/4.64 % (198859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.22/4.64 % (198859)CaDiCaL version: 2.1.3
% 24.22/4.64 % (198859)Termination reason: Instruction limit
% 24.22/4.64 % (198859)Termination phase: Saturation
% 24.22/4.64 % (198859)Time elapsed: 0.121 s
% 24.22/4.64 % (198859)Peak memory usage: 90 MB
% 24.22/4.64 % (198859)Instructions burned: 121 (million)
% 24.22/4.64 % (198850)Instruction limit reached!
% 24.22/4.64 % (198850)------------------------------
% 24.22/4.64 % (198850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.22/4.64 % (198850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.22/4.64 % (198850)CaDiCaL version: 2.1.3
% 24.22/4.64 % (198850)Termination reason: Instruction limit
% 24.22/4.64 % (198850)Termination phase: Saturation
% 24.22/4.64 % (198850)Time elapsed: 0.529 s
% 24.22/4.64 % (198850)Peak memory usage: 94 MB
% 24.22/4.64 % (198850)Instructions burned: 1000 (million)
% 24.22/4.64 % (198854)Instruction limit reached!
% 24.22/4.64 % (198854)------------------------------
% 24.22/4.64 % (198854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.22/4.64 % (198854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.22/4.64 % (198854)CaDiCaL version: 2.1.3
% 24.22/4.64 % (198854)Termination reason: Instruction limit
% 24.22/4.64 % (198854)Termination phase: Saturation
% 24.22/4.64 % (198854)Time elapsed: 0.406 s
% 24.22/4.64 % (198854)Peak memory usage: 98 MB
% 24.22/4.64 % (198854)Instructions burned: 383 (million)
% 24.22/4.64 % (198863)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=2582902116:i=39:ins=3:rtra=on_2976 on theBenchmark for (2976ds/39Mi)
% 24.22/4.64 % (198863)Instruction limit reached!
% 24.22/4.64 % (198863)------------------------------
% 24.22/4.64 % (198863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.22/4.64 % (198863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.22/4.64 % (198863)CaDiCaL version: 2.1.3
% 24.22/4.64 % (198863)Termination reason: Instruction limit
% 24.22/4.64 % (198863)Termination phase: Saturation
% 24.22/4.64 % (198863)Time elapsed: 0.071 s
% 24.22/4.64 % (198863)Peak memory usage: 116 MB
% 24.22/4.64 % (198863)Instructions burned: 39 (million)
% 24.22/4.64 % (198862)Instruction limit reached!
% 24.22/4.64 % (198862)------------------------------
% 24.22/4.64 % (198862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.41/5.07 % (198862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.41/5.07 % (198862)CaDiCaL version: 2.1.3
% 29.41/5.07 % (198862)Termination reason: Instruction limit
% 29.41/5.07 % (198862)Termination phase: Saturation
% 29.41/5.07 % (198862)Time elapsed: 0.173 s
% 29.41/5.07 % (198862)Peak memory usage: 117 MB
% 29.41/5.07 % (198862)Instructions burned: 128 (million)
% 29.41/5.07 % (198866)dis+1010_1_to=kbo:si=on:random_seed=2109607930:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/175Mi)
% 29.41/5.07 % (198870)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=4208182547:thitd=on:i=215:nm=0:rtra=on:ev=force_2974 on theBenchmark for (2974ds/215Mi)
% 29.41/5.07 % (198869)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3375284727:s2a=on:i=483:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/483Mi)
% 29.41/5.07 % (198868)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2084630138:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2974 on theBenchmark for (2974ds/329Mi)
% 29.41/5.07 % (198871)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1087899399:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi)
% 29.41/5.07 % (198870)Instruction limit reached!
% 29.41/5.07 % (198870)------------------------------
% 29.41/5.07 % (198870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.41/5.07 % (198870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.41/5.07 % (198870)CaDiCaL version: 2.1.3
% 29.41/5.07 % (198870)Termination reason: Instruction limit
% 29.41/5.07 % (198870)Termination phase: Saturation
% 29.41/5.07 % (198870)Time elapsed: 0.143 s
% 29.41/5.07 % (198870)Peak memory usage: 136 MB
% 29.41/5.07 % (198870)Instructions burned: 215 (million)
% 29.41/5.07 % (198873)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3851312631:st=2:i=295:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/295Mi)
% 29.41/5.07 % (198866)Instruction limit reached!
% 29.41/5.07 % (198866)------------------------------
% 29.41/5.07 % (198866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.41/5.07 % (198866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.41/5.07 % (198866)CaDiCaL version: 2.1.3
% 29.41/5.07 % (198866)Termination reason: Instruction limit
% 29.41/5.07 % (198866)Termination phase: Saturation
% 29.41/5.07 % (198866)Time elapsed: 0.211 s
% 29.41/5.07 % (198866)Peak memory usage: 92 MB
% 29.41/5.07 % (198866)Instructions burned: 175 (million)
% 29.41/5.07 % (198874)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3401885009:i=328:kws=inv_frequency:nm=20:rtra=on_2973 on theBenchmark for (2973ds/328Mi)
% 29.41/5.07 % (198873)Instruction limit reached!
% 29.41/5.07 % (198873)------------------------------
% 29.41/5.07 % (198873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.41/5.07 % (198873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.41/5.07 % (198873)CaDiCaL version: 2.1.3
% 29.41/5.07 % (198873)Termination reason: Instruction limit
% 29.41/5.07 % (198873)Termination phase: Saturation
% 29.41/5.07 % (198873)Time elapsed: 0.190 s
% 29.41/5.07 % (198873)Peak memory usage: 90 MB
% 29.41/5.07 % (198873)Instructions burned: 296 (million)
% 29.41/5.07 % (198868)Instruction limit reached!
% 29.41/5.07 % (198868)------------------------------
% 29.41/5.07 % (198868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.41/5.07 % (198868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.41/5.07 % (198868)CaDiCaL version: 2.1.3
% 29.41/5.07 % (198868)Termination reason: Instruction limit
% 29.41/5.07 % (198868)Termination phase: Saturation
% 29.41/5.07 % (198868)Time elapsed: 0.335 s
% 29.41/5.07 % (198868)Peak memory usage: 119 MB
% 29.41/5.07 % (198868)Instructions burned: 329 (million)
% 29.41/5.07 % (198881)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2878863214:i=281:gtgl=2:rtra=on:gtg=all_2971 on theBenchmark for (2971ds/281Mi)
% 29.41/5.07 % (198871)Instruction limit reached!
% 29.41/5.07 % (198871)------------------------------
% 29.41/5.07 % (198871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.41/5.07 % (198871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.41/5.07 % (198871)CaDiCaL version: 2.1.3
% 31.65/5.42 % (198871)Termination reason: Instruction limit
% 31.65/5.42 % (198871)Termination phase: Saturation
% 31.65/5.42 % (198871)Time elapsed: 0.360 s
% 31.65/5.42 % (198871)Peak memory usage: 118 MB
% 31.65/5.42 % (198871)Instructions burned: 349 (million)
% 31.65/5.42 % (198869)Instruction limit reached!
% 31.65/5.42 % (198869)------------------------------
% 31.65/5.42 % (198869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.65/5.42 % (198869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.65/5.42 % (198869)CaDiCaL version: 2.1.3
% 31.65/5.42 % (198869)Termination reason: Instruction limit
% 31.65/5.42 % (198869)Termination phase: Saturation
% 31.65/5.42 % (198869)Time elapsed: 0.451 s
% 31.65/5.42 % (198869)Peak memory usage: 135 MB
% 31.65/5.42 % (198869)Instructions burned: 483 (million)
% 31.65/5.42 % (198882)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3770850772:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/484Mi)
% 31.65/5.42 % (198881)Instruction limit reached!
% 31.65/5.42 % (198881)------------------------------
% 31.65/5.42 % (198881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.65/5.42 % (198881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.65/5.42 % (198881)CaDiCaL version: 2.1.3
% 31.65/5.42 % (198881)Termination reason: Instruction limit
% 31.65/5.42 % (198881)Termination phase: Saturation
% 31.65/5.42 % (198881)Time elapsed: 0.178 s
% 31.65/5.42 % (198881)Peak memory usage: 118 MB
% 31.65/5.42 % (198881)Instructions burned: 282 (million)
% 31.65/5.42 % (198874)Instruction limit reached!
% 31.65/5.42 % (198874)------------------------------
% 31.65/5.42 % (198874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.65/5.42 % (198874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.65/5.42 % (198874)CaDiCaL version: 2.1.3
% 31.65/5.42 % (198874)Termination reason: Instruction limit
% 31.65/5.42 % (198874)Termination phase: Saturation
% 31.65/5.42 % (198874)Time elapsed: 0.314 s
% 31.65/5.42 % (198874)Peak memory usage: 118 MB
% 31.65/5.42 % (198874)Instructions burned: 329 (million)
% 31.65/5.42 % (198884)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1482767138:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2969 on theBenchmark for (2969ds/321Mi)
% 31.65/5.42 % (198885)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3545983165:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi)
% 31.65/5.42 % (198887)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3393453857:i=471:thf=on:kws=precedence:rtra=on_2968 on theBenchmark for (2968ds/471Mi)
% 31.65/5.42 % (198889)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=1805708446:avsq=on:i=276:avsqr=1,2:rtra=on_2967 on theBenchmark for (2967ds/276Mi)
% 31.65/5.42 % (198895)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2862846589:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/387Mi)
% 31.65/5.42 % (198894)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1166674328:i=375:kws=inv_arity_squared:rtra=on_2967 on theBenchmark for (2967ds/375Mi)
% 31.65/5.42 % (198884)Instruction limit reached!
% 31.65/5.42 % (198884)------------------------------
% 31.65/5.42 % (198884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.65/5.42 % (198884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.65/5.42 % (198884)CaDiCaL version: 2.1.3
% 31.65/5.42 % (198884)Termination reason: Instruction limit
% 31.65/5.42 % (198884)Termination phase: Saturation
% 31.65/5.42 % (198884)Time elapsed: 0.305 s
% 31.65/5.42 % (198884)Peak memory usage: 116 MB
% 31.65/5.42 % (198884)Instructions burned: 321 (million)
% 31.65/5.42 % (198882)Instruction limit reached!
% 31.65/5.42 % (198882)------------------------------
% 31.65/5.42 % (198882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.65/5.42 % (198882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.65/5.42 % (198882)CaDiCaL version: 2.1.3
% 31.65/5.42 % (198882)Termination reason: Instruction limit
% 31.65/5.42 % (198882)Termination phase: Saturation
% 31.65/5.42 % (198882)Time elapsed: 0.461 s
% 31.65/5.42 % (198882)Peak memory usage: 94 MB
% 31.65/5.42 % (198882)Instructions burned: 484 (million)
% 37.97/6.32 % (198895)Instruction limit reached!
% 37.97/6.32 % (198895)------------------------------
% 37.97/6.32 % (198895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.97/6.32 % (198895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.97/6.32 % (198895)CaDiCaL version: 2.1.3
% 37.97/6.32 % (198895)Termination reason: Instruction limit
% 37.97/6.32 % (198895)Termination phase: Saturation
% 37.97/6.32 % (198895)Time elapsed: 0.229 s
% 37.97/6.32 % (198895)Peak memory usage: 119 MB
% 37.97/6.32 % (198895)Instructions burned: 387 (million)
% 37.97/6.32 % (198885)Instruction limit reached!
% 37.97/6.32 % (198885)------------------------------
% 37.97/6.32 % (198885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.97/6.32 % (198885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.97/6.32 % (198885)CaDiCaL version: 2.1.3
% 37.97/6.32 % (198885)Termination reason: Instruction limit
% 37.97/6.32 % (198885)Termination phase: Saturation
% 37.97/6.32 % (198885)Time elapsed: 0.414 s
% 37.97/6.32 % (198885)Peak memory usage: 118 MB
% 37.97/6.32 % (198885)Instructions burned: 417 (million)
% 37.97/6.32 % (198887)Instruction limit reached!
% 37.97/6.32 % (198887)------------------------------
% 37.97/6.32 % (198887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.97/6.32 % (198887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.97/6.32 % (198887)CaDiCaL version: 2.1.3
% 37.97/6.32 % (198887)Termination reason: Instruction limit
% 37.97/6.32 % (198887)Termination phase: Saturation
% 37.97/6.32 % (198887)Time elapsed: 0.395 s
% 37.97/6.32 % (198887)Peak memory usage: 119 MB
% 37.97/6.32 % (198887)Instructions burned: 471 (million)
% 37.97/6.32 % (198889)Instruction limit reached!
% 37.97/6.32 % (198889)------------------------------
% 37.97/6.32 % (198889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.97/6.32 % (198889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.97/6.32 % (198889)CaDiCaL version: 2.1.3
% 37.97/6.32 % (198889)Termination reason: Instruction limit
% 37.97/6.32 % (198889)Termination phase: Saturation
% 37.97/6.32 % (198889)Time elapsed: 0.339 s
% 37.97/6.32 % (198889)Peak memory usage: 135 MB
% 37.97/6.32 % (198889)Instructions burned: 276 (million)
% 37.97/6.32 % (198903)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=245973454:i=334:rtra=on_2963 on theBenchmark for (2963ds/334Mi)
% 37.97/6.32 % (198902)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=969574360:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2963 on theBenchmark for (2963ds/513Mi)
% 37.97/6.32 % (198894)Instruction limit reached!
% 37.97/6.32 % (198894)------------------------------
% 37.97/6.32 % (198894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.97/6.32 % (198894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.97/6.32 % (198894)CaDiCaL version: 2.1.3
% 37.97/6.32 % (198894)Termination reason: Instruction limit
% 37.97/6.32 % (198894)Termination phase: Saturation
% 37.97/6.32 % (198894)Time elapsed: 0.402 s
% 37.97/6.32 % (198894)Peak memory usage: 118 MB
% 37.97/6.32 % (198894)Instructions burned: 376 (million)
% 37.97/6.32 % (198904)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=933995045:i=359:rtra=on:gtg=exists_top:ss=axioms_2962 on theBenchmark for (2962ds/359Mi)
% 37.97/6.32 % (198905)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=290179445:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2962 on theBenchmark for (2962ds/341Mi)
% 37.97/6.32 % (198906)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1004648086:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2961 on theBenchmark for (2961ds/261Mi)
% 37.97/6.32 % (198907)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=1631658569:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2961 on theBenchmark for (2961ds/235Mi)
% 37.97/6.32 % (198903)Instruction limit reached!
% 37.97/6.32 % (198903)------------------------------
% 37.97/6.32 % (198903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.97/6.32 % (198903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.97/6.32 % (198903)CaDiCaL version: 2.1.3
% 37.97/6.32 % (198903)Termination reason: Instruction limit
% 38.42/6.62 % (198903)Termination phase: Saturation
% 38.42/6.62 % (198903)Time elapsed: 0.224 s
% 38.42/6.62 % (198903)Peak memory usage: 135 MB
% 38.42/6.62 % (198903)Instructions burned: 335 (million)
% 38.42/6.62 % (198910)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1479068650:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2960 on theBenchmark for (2960ds/273Mi)
% 38.42/6.62 % (198904)Instruction limit reached!
% 38.42/6.62 % (198904)------------------------------
% 38.42/6.62 % (198904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198904)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198904)Termination reason: Instruction limit
% 38.42/6.62 % (198904)Termination phase: Saturation
% 38.42/6.62 % (198904)Time elapsed: 0.337 s
% 38.42/6.62 % (198904)Peak memory usage: 92 MB
% 38.42/6.62 % (198904)Instructions burned: 359 (million)
% 38.42/6.62 % (198915)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2830965286:i=146:doe=on:rtra=on_2958 on theBenchmark for (2958ds/146Mi)
% 38.42/6.62 % (198906)Instruction limit reached!
% 38.42/6.62 % (198906)------------------------------
% 38.42/6.62 % (198906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198906)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198906)Termination reason: Instruction limit
% 38.42/6.62 % (198906)Termination phase: Saturation
% 38.42/6.62 % (198906)Time elapsed: 0.269 s
% 38.42/6.62 % (198906)Peak memory usage: 117 MB
% 38.42/6.62 % (198906)Instructions burned: 261 (million)
% 38.42/6.62 % (198907)Instruction limit reached!
% 38.42/6.62 % (198907)------------------------------
% 38.42/6.62 % (198907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198907)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198907)Termination reason: Instruction limit
% 38.42/6.62 % (198907)Termination phase: Saturation
% 38.42/6.62 % (198907)Time elapsed: 0.260 s
% 38.42/6.62 % (198907)Peak memory usage: 117 MB
% 38.42/6.62 % (198907)Instructions burned: 235 (million)
% 38.42/6.62 % (198902)Instruction limit reached!
% 38.42/6.62 % (198902)------------------------------
% 38.42/6.62 % (198902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198902)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198902)Termination reason: Instruction limit
% 38.42/6.62 % (198902)Termination phase: Saturation
% 38.42/6.62 % (198902)Time elapsed: 0.519 s
% 38.42/6.62 % (198902)Peak memory usage: 93 MB
% 38.42/6.62 % (198902)Instructions burned: 513 (million)
% 38.42/6.62 % (198905)Instruction limit reached!
% 38.42/6.62 % (198905)------------------------------
% 38.42/6.62 % (198905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198905)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198905)Termination reason: Instruction limit
% 38.42/6.62 % (198905)Termination phase: Saturation
% 38.42/6.62 % (198905)Time elapsed: 0.397 s
% 38.42/6.62 % (198905)Peak memory usage: 121 MB
% 38.42/6.62 % (198905)Instructions burned: 341 (million)
% 38.42/6.62 % (198915)Instruction limit reached!
% 38.42/6.62 % (198915)------------------------------
% 38.42/6.62 % (198915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198915)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198915)Termination reason: Instruction limit
% 38.42/6.62 % (198915)Termination phase: Saturation
% 38.42/6.62 % (198915)Time elapsed: 0.085 s
% 38.42/6.62 % (198915)Peak memory usage: 91 MB
% 38.42/6.62 % (198915)Instructions burned: 147 (million)
% 38.42/6.62 % (198910)Instruction limit reached!
% 38.42/6.62 % (198910)------------------------------
% 38.42/6.62 % (198910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198910)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198910)Termination reason: Instruction limit
% 38.42/6.62 % (198910)Termination phase: Saturation
% 38.42/6.62 % (198910)Time elapsed: 0.317 s
% 38.42/6.62 % (198910)Peak memory usage: 92 MB
% 38.42/6.62 % (198910)Instructions burned: 273 (million)
% 38.42/6.62 % (198917)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=983062096:i=4428:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/4428Mi)
% 38.42/6.62 % (198923)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3098447515:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2955 on theBenchmark for (2955ds/1054Mi)
% 38.42/6.62 % (198924)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3275729644:i=107:rtra=on_2955 on theBenchmark for (2955ds/107Mi)
% 38.42/6.62 % (198921)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=524354351:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/655Mi)
% 38.42/6.62 % (198920)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1839326785:i=1052:rtra=on_2956 on theBenchmark for (2956ds/1052Mi)
% 38.42/6.62 % (198919)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=244338460:avsq=on:i=276:avsqr=1,2:rtra=on_2956 on theBenchmark for (2956ds/276Mi)
% 38.42/6.62 % (198924)Instruction limit reached!
% 38.42/6.62 % (198924)------------------------------
% 38.42/6.62 % (198924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198924)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198924)Termination reason: Instruction limit
% 38.42/6.62 % (198924)Termination phase: Saturation
% 38.42/6.62 % (198924)Time elapsed: 0.126 s
% 38.42/6.62 % (198924)Peak memory usage: 117 MB
% 38.42/6.62 % (198924)Instructions burned: 107 (million)
% 38.42/6.62 % (198926)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3101888212:s2a=on:i=450:doe=on:nm=32:rtra=on_2955 on theBenchmark for (2955ds/450Mi)
% 38.42/6.62 % (198919)Instruction limit reached!
% 38.42/6.62 % (198919)------------------------------
% 38.42/6.62 % (198919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198919)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198919)Termination reason: Instruction limit
% 38.42/6.62 % (198919)Termination phase: Saturation
% 38.42/6.62 % (198919)Time elapsed: 0.349 s
% 38.42/6.62 % (198919)Peak memory usage: 135 MB
% 38.42/6.62 % (198919)Instructions burned: 276 (million)
% 38.42/6.62 % (198933)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 38.42/6.62 % (198933)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=320649694:i=1090:aac=none:nm=0:rtra=on:rawr=on_2952 on theBenchmark for (2952ds/1090Mi)
% 38.42/6.62 % (198923)Instruction limit reached!
% 38.42/6.62 % (198923)------------------------------
% 38.42/6.62 % (198923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198923)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198923)Termination reason: Instruction limit
% 38.42/6.62 % (198923)Termination phase: Saturation
% 38.42/6.62 % (198923)Time elapsed: 0.561 s
% 38.42/6.62 % (198923)Peak memory usage: 99 MB
% 38.42/6.62 % (198923)Instructions burned: 1055 (million)
% 38.42/6.62 % (198921)First to succeed.
% 38.42/6.62 % (198935)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=535623977:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2950 on theBenchmark for (2950ds/130Mi)
% 38.42/6.62 % (198926)Instruction limit reached!
% 38.42/6.62 % (198926)------------------------------
% 38.42/6.62 % (198926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198926)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198926)Termination reason: Instruction limit
% 38.42/6.62 % (198926)Termination phase: Saturation
% 38.42/6.62 % (198926)Time elapsed: 0.506 s
% 38.42/6.62 % (198926)Peak memory usage: 135 MB
% 38.42/6.62 % (198926)Instructions burned: 450 (million)
% 38.42/6.62 % (198921)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-198759"
% 38.42/6.62 % (198937)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=417680168:i=312:kws=inv_frequency:nm=20:rtra=on_2948 on theBenchmark for (2948ds/312Mi)
% 38.42/6.62 % (198935)Instruction limit reached!
% 38.42/6.62 % (198935)------------------------------
% 38.42/6.62 % (198935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198935)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198935)Termination reason: Instruction limit
% 38.42/6.62 % (198935)Termination phase: Saturation
% 38.42/6.62 % (198935)Time elapsed: 0.155 s
% 38.42/6.62 % (198935)Peak memory usage: 117 MB
% 38.42/6.62 % (198935)Instructions burned: 130 (million)
% 38.42/6.62 % (198937)Instruction limit reached!
% 38.42/6.62 % (198937)------------------------------
% 38.42/6.62 % (198937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198937)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198937)Termination reason: Instruction limit
% 38.42/6.62 % (198937)Termination phase: Saturation
% 38.42/6.62 % (198937)Time elapsed: 0.194 s
% 38.42/6.62 % (198937)Peak memory usage: 118 MB
% 38.42/6.62 % (198937)Instructions burned: 314 (million)
% 38.42/6.62 % (198939)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1339656782:i=491:doe=on:rtra=on:gtg=position_2947 on theBenchmark for (2947ds/491Mi)
% 38.42/6.62 % (198920)Instruction limit reached!
% 38.42/6.62 % (198920)------------------------------
% 38.42/6.62 % (198920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.42/6.62 % (198920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.42/6.62 % (198920)CaDiCaL version: 2.1.3
% 38.42/6.62 % (198920)Termination reason: Instruction limit
% 38.42/6.62 % (198920)Termination phase: Saturation
% 38.42/6.62 % (198920)Time elapsed: 0.994 s
% 38.42/6.62 % (198920)Peak memory usage: 95 MB
% 38.42/6.62 % (198920)Instructions burned: 1052 (million)
% 38.42/6.62 % (198941)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2948491120:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi)
% 38.42/6.62 % (198921)Refutation found. Thanks to Tanya!
% 38.42/6.62 % SZS status Theorem for theBenchmark
% 38.42/6.62 % SZS output start Proof for theBenchmark
% See solution above
% 40.70/6.92 % (198921)------------------------------
% 40.70/6.92 % (198921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.70/6.92 % (198921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.70/6.92 % (198921)CaDiCaL version: 2.1.3
% 40.70/6.92 % (198921)Termination reason: Refutation
% 40.70/6.92 % (198921)Time elapsed: 0.653 s
% 40.70/6.92 % (198921)Peak memory usage: 97 MB
% 40.70/6.92 % (198921)Instructions burned: 672 (million)
% 40.70/6.92 % (198921)------------------------------
% 40.70/6.92 % (198921)------------------------------
% 40.70/6.92 % (198759)Success in time 5.656 s
% 40.70/6.92 % Vampire exiting
%------------------------------------------------------------------------------