%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW634_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 : n017.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:00 PM UTC 2026
% Result : Theorem 8.39s 2.17s
% Output : Refutation 9.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 25
% Syntax : Number of formulae : 160 ( 46 unt; 0 typ; 23 def)
% Number of atoms : 893 ( 157 equ)
% Maximal formula atoms : 63 ( 5 avg)
% Number of connectives : 1136 ( 403 ~; 347 |; 304 &)
% ( 45 <=>; 35 =>; 0 <=; 2 <~>)
% Maximal formula depth : 35 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 900 ( 311 atm; 180 fun; 236 num; 173 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 : 26 ( 22 usr; 13 prp; 0-4 aty)
% Number of functors : 117 ( 112 usr; 37 con; 0-5 aty)
% Number of variables : 286 ( 0 sgn 207 !; 79 ?; 286 :)
% 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,
set_int: $tType ).
tff(type_def_10,type,
map_int_int: $tType ).
tff(type_def_11,type,
map_int_lpmap_int_intrp: $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,
set: ty > ty ).
tff(func_def_13,type,
empty: ty > uni ).
tff(func_def_14,type,
add: ( ty * uni * uni ) > uni ).
tff(func_def_15,type,
remove: ( ty * uni * uni ) > uni ).
tff(func_def_16,type,
union: ( ty * uni * uni ) > uni ).
tff(func_def_17,type,
inter: ( ty * uni * uni ) > uni ).
tff(func_def_18,type,
diff: ( ty * uni * uni ) > uni ).
tff(func_def_19,type,
choose: ( ty * uni ) > uni ).
tff(func_def_20,type,
cardinal1: ( ty * uni ) > $int ).
tff(func_def_23,type,
min_elt1: set_int > $int ).
tff(func_def_24,type,
t2tb: set_int > uni ).
tff(func_def_25,type,
tb2t: uni > set_int ).
tff(func_def_26,type,
t2tb1: $int > uni ).
tff(func_def_27,type,
tb2t1: uni > $int ).
tff(func_def_28,type,
max_elt1: set_int > $int ).
tff(func_def_29,type,
below1: $int > set_int ).
tff(func_def_30,type,
succ1: set_int > set_int ).
tff(func_def_32,type,
pred1: set_int > set_int ).
tff(func_def_33,type,
ref: ty > ty ).
tff(func_def_34,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_35,type,
contents: ( ty * uni ) > uni ).
tff(func_def_36,type,
map: ( ty * ty ) > ty ).
tff(func_def_37,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_38,type,
set1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_39,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_40,type,
n1: $int ).
tff(func_def_41,type,
t2tb2: map_int_int > uni ).
tff(func_def_42,type,
tb2t2: uni > map_int_int ).
tff(func_def_43,type,
t2tb3: map_int_lpmap_int_intrp > uni ).
tff(func_def_44,type,
tb2t3: uni > map_int_lpmap_int_intrp ).
tff(func_def_46,type,
sK1: ( ty * uni * uni * $int ) > $int ).
tff(func_def_47,type,
sK2: $int ).
tff(func_def_48,type,
sK3: $int ).
tff(func_def_49,type,
sK4: map_int_int ).
tff(func_def_50,type,
sK5: $int ).
tff(func_def_51,type,
sK6: map_int_lpmap_int_intrp ).
tff(func_def_52,type,
sK7: $int > $int ).
tff(func_def_53,type,
sK8: $int > $int ).
tff(func_def_54,type,
sK9: $int > $int ).
tff(func_def_55,type,
sK10: map_int_lpmap_int_intrp ).
tff(func_def_56,type,
sK11: map_int_int ).
tff(func_def_57,type,
sK12: $int ).
tff(func_def_58,type,
sK13: $int ).
tff(func_def_59,type,
sK14: map_int_int ).
tff(func_def_60,type,
sK15: $int ).
tff(func_def_61,type,
sK16: map_int_int > $int ).
tff(func_def_62,type,
sK17: ( uni * ty ) > uni ).
tff(func_def_63,type,
sK18: ( map_int_int * $int ) > $int ).
tff(func_def_64,type,
sK19: ( map_int_int * $int ) > $int ).
tff(func_def_65,type,
sF20: uni ).
tff(func_def_66,type,
sF21: uni ).
tff(func_def_67,type,
sF22: $int > uni ).
tff(func_def_68,type,
sF23: $int > uni ).
tff(func_def_69,type,
sF24: $int > $int ).
tff(func_def_70,type,
sF25: $int > $int ).
tff(func_def_71,type,
sF26: $int ).
tff(func_def_72,type,
sF27: $int > $int ).
tff(func_def_73,type,
sF28: $int > uni ).
tff(func_def_74,type,
sF29: $int > $int ).
tff(func_def_75,type,
sF30: ( $int * $int ) > $int ).
tff(func_def_76,type,
sF31: set_int ).
tff(func_def_77,type,
sF32: uni ).
tff(func_def_78,type,
sF33: $int ).
tff(func_def_79,type,
sF34: $int ).
tff(func_def_80,type,
sF35: $int > $int ).
tff(func_def_81,type,
sF36: ( $int * $int ) > $int ).
tff(func_def_82,type,
sF37: $int > $int ).
tff(func_def_83,type,
sF38: $int > $int ).
tff(func_def_84,type,
sF39: $int > uni ).
tff(func_def_85,type,
sF40: $int > uni ).
tff(func_def_86,type,
sF41: $int > $int ).
tff(func_def_87,type,
sF42: $int > uni ).
tff(func_def_88,type,
sF43: $int > uni ).
tff(func_def_89,type,
sF44: $int > $int ).
tff(func_def_90,type,
sF45: $int > uni ).
tff(func_def_91,type,
sF46: ty ).
tff(func_def_92,type,
sF47: uni ).
tff(func_def_93,type,
sF48: uni ).
tff(func_def_94,type,
sF49: uni ).
tff(func_def_95,type,
sF50: $int ).
tff(func_def_96,type,
sF51: $int ).
tff(func_def_97,type,
sF52: uni ).
tff(func_def_98,type,
sF53: $int > uni ).
tff(func_def_99,type,
sF54: uni ).
tff(func_def_100,type,
sF55: uni ).
tff(func_def_101,type,
sF56: map_int_int > uni ).
tff(func_def_102,type,
sF57: map_int_int > uni ).
tff(func_def_103,type,
sF58: ( map_int_lpmap_int_intrp * $int ) > uni ).
tff(func_def_104,type,
sF59: ( map_int_int * $int ) > uni ).
tff(func_def_105,type,
sF60: ( map_int_int * $int ) > uni ).
tff(func_def_106,type,
sF61: ( map_int_int * $int ) > $int ).
tff(func_def_107,type,
sF62: ( map_int_int * $int ) > $int ).
tff(func_def_108,type,
sF63: ( map_int_int * $int ) > $int ).
tff(func_def_109,type,
sF64: ( map_int_int * $int ) > uni ).
tff(func_def_110,type,
sF65: ( map_int_int * $int ) > uni ).
tff(func_def_111,type,
sF66: ( map_int_int * $int ) > $int ).
tff(func_def_112,type,
sF67: ( map_int_int * $int ) > $int ).
tff(func_def_113,type,
sF68: ( map_int_int * $int ) > $int ).
tff(func_def_114,type,
sF69: ( map_int_int * $int ) > $int ).
tff(func_def_115,type,
sF70: ( map_int_int * $int ) > $int ).
tff(func_def_116,type,
sF71: ( map_int_int * $int ) > uni ).
tff(func_def_117,type,
sF72: ( map_int_int * $int ) > $int ).
tff(func_def_119,type,
-1: $int > $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_4,type,
infix_eqeq: ( ty * uni * uni ) > $o ).
tff(pred_def_5,type,
subset: ( ty * uni * uni ) > $o ).
tff(pred_def_6,type,
is_empty: ( ty * uni ) > $o ).
tff(pred_def_8,type,
eq_prefix1: ( ty * uni * uni * $int ) > $o ).
tff(pred_def_9,type,
partial_solution1: ( $int * map_int_int ) > $o ).
tff(pred_def_10,type,
lt_sol1: ( map_int_int * map_int_int ) > $o ).
tff(pred_def_11,type,
sorted1: ( map_int_lpmap_int_intrp * $int * $int ) > $o ).
tff(pred_def_12,type,
sP0: ( map_int_int * $int ) > $o ).
tff(f64,axiom,
! [X1: uni,X0: ty,X2: uni,X3: $int] :
( ! [X4: $int] :
( ( $less(X4,X3)
& $lesseq(0,X4) )
=> ( get(X0,int,X1,t2tb1(X4)) = get(X0,int,X2,t2tb1(X4)) ) )
<=> eq_prefix1(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq_prefix_def) ).
tff(f76,conjecture,
! [X2: map_int_lpmap_int_intrp,X3: $int,X1: $int,X4: map_int_int,X0: $int] :
( ( ( X1 = 0 )
& ( X0 = n1 )
& $lesseq(0,X0)
& ( X3 = 0 ) )
=> ( ( $lesseq(0,X3)
& $lesseq(0,X1)
& ! [X5: $int] :
( mem(int,t2tb1(X5),t2tb(below1(X0)))
<=> ( ! [X6: $int] :
( ( $less(X6,X3)
& $lesseq(0,X6) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != X5 ) )
& $less(X5,n1)
& $lesseq(0,X5) ) )
& ( $sum(X3,cardinal1(int,t2tb(below1(X0)))) = n1 )
& ! [X5: $int] :
( $lesseq(0,X5)
=> ( ! [X6: $int] :
( ( $less(X6,X3)
& $lesseq(0,X6) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != $difference($sum(X5,X6),X3) ) )
<=> ~ mem(int,t2tb1(X5),empty(int)) ) )
& ! [X5: $int] :
( $lesseq(0,X5)
=> ( ~ mem(int,t2tb1(X5),empty(int))
<=> ! [X6: $int] :
( ( $lesseq(0,X6)
& $less(X6,X3) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != $difference($sum(X5,X3),X6) ) ) ) )
& partial_solution1(X3,X4) )
=> ! [X8: map_int_lpmap_int_intrp,X9: $int,X7: $int,X10: map_int_int] :
( ( $lesseq(0,$difference(X7,X1))
& sorted1(X8,X1,X7)
& ! [X11: map_int_int] :
( ? [X5: $int] :
( eq_prefix1(int,t2tb2(X11),get(map(int,int),int,t2tb3(X8),t2tb1(X5)),n1)
& $lesseq(X1,X5)
& $less(X5,X7) )
<=> ( partial_solution1(n1,X11)
& eq_prefix1(int,t2tb2(X10),t2tb2(X11),X9) ) )
& eq_prefix1(int,t2tb2(X4),t2tb2(X10),X9)
& eq_prefix1(map(int,int),t2tb3(X2),t2tb3(X8),X1)
& ( X9 = X3 ) )
=> ( sorted1(X8,0,X7)
& ! [X11: map_int_int] :
( ? [X5: $int] :
( $less(X5,$difference(X7,X1))
& eq_prefix1(int,t2tb2(X11),get(map(int,int),int,t2tb3(X8),t2tb1(X5)),n1)
& $lesseq(0,X5) )
<=> partial_solution1(n1,X11) )
& ( $difference(X7,X1) = X7 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_queens3) ).
tff(f77,negated_conjecture,
~ ! [X2: map_int_lpmap_int_intrp,X3: $int,X1: $int,X4: map_int_int,X0: $int] :
( ( ( X1 = 0 )
& ( X0 = n1 )
& $lesseq(0,X0)
& ( X3 = 0 ) )
=> ( ( $lesseq(0,X3)
& $lesseq(0,X1)
& ! [X5: $int] :
( mem(int,t2tb1(X5),t2tb(below1(X0)))
<=> ( ! [X6: $int] :
( ( $less(X6,X3)
& $lesseq(0,X6) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != X5 ) )
& $less(X5,n1)
& $lesseq(0,X5) ) )
& ( $sum(X3,cardinal1(int,t2tb(below1(X0)))) = n1 )
& ! [X5: $int] :
( $lesseq(0,X5)
=> ( ! [X6: $int] :
( ( $less(X6,X3)
& $lesseq(0,X6) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != $difference($sum(X5,X6),X3) ) )
<=> ~ mem(int,t2tb1(X5),empty(int)) ) )
& ! [X5: $int] :
( $lesseq(0,X5)
=> ( ~ mem(int,t2tb1(X5),empty(int))
<=> ! [X6: $int] :
( ( $lesseq(0,X6)
& $less(X6,X3) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != $difference($sum(X5,X3),X6) ) ) ) )
& partial_solution1(X3,X4) )
=> ! [X8: map_int_lpmap_int_intrp,X9: $int,X7: $int,X10: map_int_int] :
( ( $lesseq(0,$difference(X7,X1))
& sorted1(X8,X1,X7)
& ! [X11: map_int_int] :
( ? [X5: $int] :
( eq_prefix1(int,t2tb2(X11),get(map(int,int),int,t2tb3(X8),t2tb1(X5)),n1)
& $lesseq(X1,X5)
& $less(X5,X7) )
<=> ( partial_solution1(n1,X11)
& eq_prefix1(int,t2tb2(X10),t2tb2(X11),X9) ) )
& eq_prefix1(int,t2tb2(X4),t2tb2(X10),X9)
& eq_prefix1(map(int,int),t2tb3(X2),t2tb3(X8),X1)
& ( X9 = X3 ) )
=> ( sorted1(X8,0,X7)
& ! [X11: map_int_int] :
( ? [X5: $int] :
( $less(X5,$difference(X7,X1))
& eq_prefix1(int,t2tb2(X11),get(map(int,int),int,t2tb3(X8),t2tb1(X5)),n1)
& $lesseq(0,X5) )
<=> partial_solution1(n1,X11) )
& ( $difference(X7,X1) = X7 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f76]) ).
tff(f84,plain,
! [X1: uni,X0: ty,X2: uni,X3: $int] :
( ! [X4: $int] :
( ( ~ $less(X4,0)
& $less(X4,X3) )
=> ( get(X0,int,X1,t2tb1(X4)) = get(X0,int,X2,t2tb1(X4)) ) )
<=> eq_prefix1(X0,X1,X2,X3) ),
inference(theory_normalization,[],[f64]) ).
tff(f92,plain,
~ ! [X2: map_int_lpmap_int_intrp,X3: $int,X1: $int,X4: map_int_int,X0: $int] :
( ( ( X1 = 0 )
& ( X0 = n1 )
& ~ $less(X0,0)
& ( X3 = 0 ) )
=> ( ( ~ $less(X3,0)
& ~ $less(X1,0)
& ! [X5: $int] :
( mem(int,t2tb1(X5),t2tb(below1(X0)))
<=> ( ! [X6: $int] :
( ( $less(X6,X3)
& ~ $less(X6,0) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != X5 ) )
& $less(X5,n1)
& ~ $less(X5,0) ) )
& ( $sum(X3,cardinal1(int,t2tb(below1(X0)))) = n1 )
& ! [X5: $int] :
( ~ $less(X5,0)
=> ( ! [X6: $int] :
( ( $less(X6,X3)
& ~ $less(X6,0) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != $sum($sum(X5,X6),$uminus(X3)) ) )
<=> ~ mem(int,t2tb1(X5),empty(int)) ) )
& ! [X5: $int] :
( ~ $less(X5,0)
=> ( ~ mem(int,t2tb1(X5),empty(int))
<=> ! [X6: $int] :
( ( ~ $less(X6,0)
& $less(X6,X3) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != $sum($sum(X5,X3),$uminus(X6)) ) ) ) )
& partial_solution1(X3,X4) )
=> ! [X8: map_int_lpmap_int_intrp,X9: $int,X7: $int,X10: map_int_int] :
( ( ~ $less($sum(X7,$uminus(X1)),0)
& sorted1(X8,X1,X7)
& ! [X11: map_int_int] :
( ? [X5: $int] :
( eq_prefix1(int,t2tb2(X11),get(map(int,int),int,t2tb3(X8),t2tb1(X5)),n1)
& ~ $less(X5,X1)
& $less(X5,X7) )
<=> ( partial_solution1(n1,X11)
& eq_prefix1(int,t2tb2(X10),t2tb2(X11),X9) ) )
& eq_prefix1(int,t2tb2(X4),t2tb2(X10),X9)
& eq_prefix1(map(int,int),t2tb3(X2),t2tb3(X8),X1)
& ( X9 = X3 ) )
=> ( sorted1(X8,0,X7)
& ! [X11: map_int_int] :
( ? [X5: $int] :
( $less(X5,$sum(X7,$uminus(X1)))
& eq_prefix1(int,t2tb2(X11),get(map(int,int),int,t2tb3(X8),t2tb1(X5)),n1)
& ~ $less(X5,0) )
<=> partial_solution1(n1,X11) )
& ( $sum(X7,$uminus(X1)) = X7 ) ) ) ) ),
inference(theory_normalization,[],[f77]) ).
tff(f93,plain,
~ ! [X0: map_int_lpmap_int_intrp,X1: $int,X3: map_int_int,X2: $int,X4: $int] :
( ( ~ $less(X4,0)
& ( 0 = X2 )
& ( n1 = X4 )
& ( 0 = X1 ) )
=> ( ( ~ $less(X1,0)
& ~ $less(X2,0)
& ( n1 = $sum(X1,cardinal1(int,t2tb(below1(X4)))) )
& ! [X5: $int] :
( mem(int,t2tb1(X5),t2tb(below1(X4)))
<=> ( $less(X5,n1)
& ~ $less(X5,0)
& ! [X6: $int] :
( ( ~ $less(X6,0)
& $less(X6,X1) )
=> ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X6))) != X5 ) ) ) )
& partial_solution1(X1,X3)
& ! [X7: $int] :
( ~ $less(X7,0)
=> ( ~ mem(int,t2tb1(X7),empty(int))
<=> ! [X8: $int] :
( ( ~ $less(X8,0)
& $less(X8,X1) )
=> ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X1)) ) ) ) )
& ! [X9: $int] :
( ~ $less(X9,0)
=> ( ! [X10: $int] :
( ( ~ $less(X10,0)
& $less(X10,X1) )
=> ( $sum($sum(X9,X1),$uminus(X10)) != tb2t1(get(int,int,t2tb2(X3),t2tb1(X10))) ) )
<=> ~ mem(int,t2tb1(X9),empty(int)) ) ) )
=> ! [X12: $int,X13: $int,X14: map_int_int,X11: map_int_lpmap_int_intrp] :
( ( ~ $less($sum(X13,$uminus(X2)),0)
& ( X1 = X12 )
& sorted1(X11,X2,X13)
& ! [X15: map_int_int] :
( ( partial_solution1(n1,X15)
& eq_prefix1(int,t2tb2(X14),t2tb2(X15),X12) )
<=> ? [X16: $int] :
( $less(X16,X13)
& ~ $less(X16,X2)
& eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X11),t2tb1(X16)),n1) ) )
& eq_prefix1(int,t2tb2(X3),t2tb2(X14),X12)
& eq_prefix1(map(int,int),t2tb3(X0),t2tb3(X11),X2) )
=> ( sorted1(X11,0,X13)
& ( $sum(X13,$uminus(X2)) = X13 )
& ! [X17: map_int_int] :
( partial_solution1(n1,X17)
<=> ? [X18: $int] :
( ~ $less(X18,0)
& eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X11),t2tb1(X18)),n1)
& $less(X18,$sum(X13,$uminus(X2))) ) ) ) ) ) ),
inference(rectify,[],[f92]) ).
tff(f94,plain,
! [X3: $int,X0: uni,X1: ty,X2: uni] :
( ! [X4: $int] :
( ( ~ $less(X4,0)
& $less(X4,X3) )
=> ( get(X1,int,X0,t2tb1(X4)) = get(X1,int,X2,t2tb1(X4)) ) )
<=> eq_prefix1(X1,X0,X2,X3) ),
inference(rectify,[],[f84]) ).
tff(f119,plain,
! [X3: $int,X0: uni,X1: ty,X2: uni] :
( ! [X4: $int] :
( ( get(X1,int,X0,t2tb1(X4)) = get(X1,int,X2,t2tb1(X4)) )
| $less(X4,0)
| ~ $less(X4,X3) )
<=> eq_prefix1(X1,X0,X2,X3) ),
inference(ennf_transformation,[],[f94]) ).
tff(f120,plain,
! [X1: ty,X0: uni,X2: uni,X3: $int] :
( eq_prefix1(X1,X0,X2,X3)
<=> ! [X4: $int] :
( ( get(X1,int,X0,t2tb1(X4)) = get(X1,int,X2,t2tb1(X4)) )
| ~ $less(X4,X3)
| $less(X4,0) ) ),
inference(flattening,[],[f119]) ).
tff(f121,plain,
? [X0: map_int_lpmap_int_intrp,X1: $int,X3: map_int_int,X2: $int,X4: $int] :
( ? [X12: $int,X13: $int,X14: map_int_int,X11: map_int_lpmap_int_intrp] :
( ( ~ sorted1(X11,0,X13)
| ? [X17: map_int_int] :
( ? [X18: $int] :
( ~ $less(X18,0)
& eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X11),t2tb1(X18)),n1)
& $less(X18,$sum(X13,$uminus(X2))) )
<~> partial_solution1(n1,X17) )
| ( $sum(X13,$uminus(X2)) != X13 ) )
& ~ $less($sum(X13,$uminus(X2)),0)
& ( X1 = X12 )
& sorted1(X11,X2,X13)
& ! [X15: map_int_int] :
( ( partial_solution1(n1,X15)
& eq_prefix1(int,t2tb2(X14),t2tb2(X15),X12) )
<=> ? [X16: $int] :
( $less(X16,X13)
& ~ $less(X16,X2)
& eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X11),t2tb1(X16)),n1) ) )
& eq_prefix1(int,t2tb2(X3),t2tb2(X14),X12)
& eq_prefix1(map(int,int),t2tb3(X0),t2tb3(X11),X2) )
& ~ $less(X1,0)
& ~ $less(X2,0)
& ( n1 = $sum(X1,cardinal1(int,t2tb(below1(X4)))) )
& ! [X5: $int] :
( mem(int,t2tb1(X5),t2tb(below1(X4)))
<=> ( $less(X5,n1)
& ~ $less(X5,0)
& ! [X6: $int] :
( ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X6))) != X5 )
| $less(X6,0)
| ~ $less(X6,X1) ) ) )
& partial_solution1(X1,X3)
& ! [X7: $int] :
( ( ~ mem(int,t2tb1(X7),empty(int))
<=> ! [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X1)) )
| $less(X8,0)
| ~ $less(X8,X1) ) )
| $less(X7,0) )
& ! [X9: $int] :
( ( ! [X10: $int] :
( ( $sum($sum(X9,X1),$uminus(X10)) != tb2t1(get(int,int,t2tb2(X3),t2tb1(X10))) )
| $less(X10,0)
| ~ $less(X10,X1) )
<=> ~ mem(int,t2tb1(X9),empty(int)) )
| $less(X9,0) )
& ~ $less(X4,0)
& ( 0 = X2 )
& ( n1 = X4 )
& ( 0 = X1 ) ),
inference(ennf_transformation,[],[f93]) ).
tff(f122,plain,
? [X2: $int,X1: $int,X3: map_int_int,X4: $int,X0: map_int_lpmap_int_intrp] :
( ! [X7: $int] :
( $less(X7,0)
| ( ~ mem(int,t2tb1(X7),empty(int))
<=> ! [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X1)) )
| ~ $less(X8,X1)
| $less(X8,0) ) ) )
& ( n1 = $sum(X1,cardinal1(int,t2tb(below1(X4)))) )
& ! [X9: $int] :
( $less(X9,0)
| ( ! [X10: $int] :
( ( $sum($sum(X9,X1),$uminus(X10)) != tb2t1(get(int,int,t2tb2(X3),t2tb1(X10))) )
| $less(X10,0)
| ~ $less(X10,X1) )
<=> ~ mem(int,t2tb1(X9),empty(int)) ) )
& partial_solution1(X1,X3)
& ~ $less(X1,0)
& ~ $less(X2,0)
& ! [X5: $int] :
( mem(int,t2tb1(X5),t2tb(below1(X4)))
<=> ( $less(X5,n1)
& ~ $less(X5,0)
& ! [X6: $int] :
( ~ $less(X6,X1)
| ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X6))) != X5 )
| $less(X6,0) ) ) )
& ? [X11: map_int_lpmap_int_intrp,X14: map_int_int,X13: $int,X12: $int] :
( eq_prefix1(map(int,int),t2tb3(X0),t2tb3(X11),X2)
& sorted1(X11,X2,X13)
& eq_prefix1(int,t2tb2(X3),t2tb2(X14),X12)
& ~ $less($sum(X13,$uminus(X2)),0)
& ( ~ sorted1(X11,0,X13)
| ? [X17: map_int_int] :
( ? [X18: $int] :
( ~ $less(X18,0)
& eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X11),t2tb1(X18)),n1)
& $less(X18,$sum(X13,$uminus(X2))) )
<~> partial_solution1(n1,X17) )
| ( $sum(X13,$uminus(X2)) != X13 ) )
& ( X1 = X12 )
& ! [X15: map_int_int] :
( ( partial_solution1(n1,X15)
& eq_prefix1(int,t2tb2(X14),t2tb2(X15),X12) )
<=> ? [X16: $int] :
( $less(X16,X13)
& ~ $less(X16,X2)
& eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X11),t2tb1(X16)),n1) ) ) )
& ( n1 = X4 )
& ~ $less(X4,0)
& ( 0 = X1 )
& ( 0 = X2 ) ),
inference(flattening,[],[f121]) ).
tff(f125,plain,
! [X1: ty,X0: uni,X2: uni,X3: $int] :
( ( eq_prefix1(X1,X0,X2,X3)
| ? [X4: $int] :
( ( get(X1,int,X0,t2tb1(X4)) != get(X1,int,X2,t2tb1(X4)) )
& $less(X4,X3)
& ~ $less(X4,0) ) )
& ( ! [X4: $int] :
( ( get(X1,int,X0,t2tb1(X4)) = get(X1,int,X2,t2tb1(X4)) )
| ~ $less(X4,X3)
| $less(X4,0) )
| ~ eq_prefix1(X1,X0,X2,X3) ) ),
inference(nnf_transformation,[],[f120]) ).
tff(f126,plain,
! [X0: ty,X1: uni,X2: uni,X3: $int] :
( ( eq_prefix1(X0,X1,X2,X3)
| ? [X4: $int] :
( ( get(X0,int,X1,t2tb1(X4)) != get(X0,int,X2,t2tb1(X4)) )
& $less(X4,X3)
& ~ $less(X4,0) ) )
& ( ! [X5: $int] :
( ( get(X0,int,X1,t2tb1(X5)) = get(X0,int,X2,t2tb1(X5)) )
| ~ $less(X5,X3)
| $less(X5,0) )
| ~ eq_prefix1(X0,X1,X2,X3) ) ),
inference(rectify,[],[f125]) ).
tff(f127,plain,
! [X0: ty,X1: uni,X2: uni,X3: $int] :
( ( eq_prefix1(X0,X1,X2,X3)
| ( ( get(X0,int,X1,t2tb1(sK1(X0,X1,X2,X3))) != get(X0,int,X2,t2tb1(sK1(X0,X1,X2,X3))) )
& $less(sK1(X0,X1,X2,X3),X3)
& ~ $less(sK1(X0,X1,X2,X3),0) ) )
& ( ! [X5: $int] :
( ( get(X0,int,X1,t2tb1(X5)) = get(X0,int,X2,t2tb1(X5)) )
| ~ $less(X5,X3)
| $less(X5,0) )
| ~ eq_prefix1(X0,X1,X2,X3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X4,sK1(X0,X1,X2,X3))],[f126]) ).
tff(f128,plain,
? [X2: $int,X1: $int,X3: map_int_int,X4: $int,X0: map_int_lpmap_int_intrp] :
( ! [X7: $int] :
( $less(X7,0)
| ( ( ~ mem(int,t2tb1(X7),empty(int))
| ? [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X8))) = $sum($sum(X7,X8),$uminus(X1)) )
& $less(X8,X1)
& ~ $less(X8,0) ) )
& ( ! [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X1)) )
| ~ $less(X8,X1)
| $less(X8,0) )
| mem(int,t2tb1(X7),empty(int)) ) ) )
& ( n1 = $sum(X1,cardinal1(int,t2tb(below1(X4)))) )
& ! [X9: $int] :
( $less(X9,0)
| ( ( ! [X10: $int] :
( ( $sum($sum(X9,X1),$uminus(X10)) != tb2t1(get(int,int,t2tb2(X3),t2tb1(X10))) )
| $less(X10,0)
| ~ $less(X10,X1) )
| mem(int,t2tb1(X9),empty(int)) )
& ( ~ mem(int,t2tb1(X9),empty(int))
| ? [X10: $int] :
( ( $sum($sum(X9,X1),$uminus(X10)) = tb2t1(get(int,int,t2tb2(X3),t2tb1(X10))) )
& ~ $less(X10,0)
& $less(X10,X1) ) ) ) )
& partial_solution1(X1,X3)
& ~ $less(X1,0)
& ~ $less(X2,0)
& ! [X5: $int] :
( ( mem(int,t2tb1(X5),t2tb(below1(X4)))
| ~ $less(X5,n1)
| $less(X5,0)
| ? [X6: $int] :
( $less(X6,X1)
& ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X6))) = X5 )
& ~ $less(X6,0) ) )
& ( ( $less(X5,n1)
& ~ $less(X5,0)
& ! [X6: $int] :
( ~ $less(X6,X1)
| ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X6))) != X5 )
| $less(X6,0) ) )
| ~ mem(int,t2tb1(X5),t2tb(below1(X4))) ) )
& ? [X11: map_int_lpmap_int_intrp,X14: map_int_int,X13: $int,X12: $int] :
( eq_prefix1(map(int,int),t2tb3(X0),t2tb3(X11),X2)
& sorted1(X11,X2,X13)
& eq_prefix1(int,t2tb2(X3),t2tb2(X14),X12)
& ~ $less($sum(X13,$uminus(X2)),0)
& ( ~ sorted1(X11,0,X13)
| ? [X17: map_int_int] :
( ( ~ partial_solution1(n1,X17)
| ! [X18: $int] :
( $less(X18,0)
| ~ eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X11),t2tb1(X18)),n1)
| ~ $less(X18,$sum(X13,$uminus(X2))) ) )
& ( partial_solution1(n1,X17)
| ? [X18: $int] :
( ~ $less(X18,0)
& eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X11),t2tb1(X18)),n1)
& $less(X18,$sum(X13,$uminus(X2))) ) ) )
| ( $sum(X13,$uminus(X2)) != X13 ) )
& ( X1 = X12 )
& ! [X15: map_int_int] :
( ( ( partial_solution1(n1,X15)
& eq_prefix1(int,t2tb2(X14),t2tb2(X15),X12) )
| ! [X16: $int] :
( ~ $less(X16,X13)
| $less(X16,X2)
| ~ eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X11),t2tb1(X16)),n1) ) )
& ( ? [X16: $int] :
( $less(X16,X13)
& ~ $less(X16,X2)
& eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X11),t2tb1(X16)),n1) )
| ~ partial_solution1(n1,X15)
| ~ eq_prefix1(int,t2tb2(X14),t2tb2(X15),X12) ) ) )
& ( n1 = X4 )
& ~ $less(X4,0)
& ( 0 = X1 )
& ( 0 = X2 ) ),
inference(nnf_transformation,[],[f122]) ).
tff(f129,plain,
? [X2: $int,X1: $int,X3: map_int_int,X4: $int,X0: map_int_lpmap_int_intrp] :
( ! [X7: $int] :
( $less(X7,0)
| ( ( ~ mem(int,t2tb1(X7),empty(int))
| ? [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X8))) = $sum($sum(X7,X8),$uminus(X1)) )
& $less(X8,X1)
& ~ $less(X8,0) ) )
& ( ! [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X1)) )
| ~ $less(X8,X1)
| $less(X8,0) )
| mem(int,t2tb1(X7),empty(int)) ) ) )
& ( n1 = $sum(X1,cardinal1(int,t2tb(below1(X4)))) )
& ! [X9: $int] :
( $less(X9,0)
| ( ( ! [X10: $int] :
( ( $sum($sum(X9,X1),$uminus(X10)) != tb2t1(get(int,int,t2tb2(X3),t2tb1(X10))) )
| $less(X10,0)
| ~ $less(X10,X1) )
| mem(int,t2tb1(X9),empty(int)) )
& ( ~ mem(int,t2tb1(X9),empty(int))
| ? [X10: $int] :
( ( $sum($sum(X9,X1),$uminus(X10)) = tb2t1(get(int,int,t2tb2(X3),t2tb1(X10))) )
& ~ $less(X10,0)
& $less(X10,X1) ) ) ) )
& partial_solution1(X1,X3)
& ~ $less(X1,0)
& ~ $less(X2,0)
& ! [X5: $int] :
( ( mem(int,t2tb1(X5),t2tb(below1(X4)))
| ~ $less(X5,n1)
| $less(X5,0)
| ? [X6: $int] :
( $less(X6,X1)
& ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X6))) = X5 )
& ~ $less(X6,0) ) )
& ( ( $less(X5,n1)
& ~ $less(X5,0)
& ! [X6: $int] :
( ~ $less(X6,X1)
| ( tb2t1(get(int,int,t2tb2(X3),t2tb1(X6))) != X5 )
| $less(X6,0) ) )
| ~ mem(int,t2tb1(X5),t2tb(below1(X4))) ) )
& ? [X11: map_int_lpmap_int_intrp,X14: map_int_int,X13: $int,X12: $int] :
( eq_prefix1(map(int,int),t2tb3(X0),t2tb3(X11),X2)
& sorted1(X11,X2,X13)
& eq_prefix1(int,t2tb2(X3),t2tb2(X14),X12)
& ~ $less($sum(X13,$uminus(X2)),0)
& ( ~ sorted1(X11,0,X13)
| ? [X17: map_int_int] :
( ( ~ partial_solution1(n1,X17)
| ! [X18: $int] :
( $less(X18,0)
| ~ eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X11),t2tb1(X18)),n1)
| ~ $less(X18,$sum(X13,$uminus(X2))) ) )
& ( partial_solution1(n1,X17)
| ? [X18: $int] :
( ~ $less(X18,0)
& eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X11),t2tb1(X18)),n1)
& $less(X18,$sum(X13,$uminus(X2))) ) ) )
| ( $sum(X13,$uminus(X2)) != X13 ) )
& ( X1 = X12 )
& ! [X15: map_int_int] :
( ( ( partial_solution1(n1,X15)
& eq_prefix1(int,t2tb2(X14),t2tb2(X15),X12) )
| ! [X16: $int] :
( ~ $less(X16,X13)
| $less(X16,X2)
| ~ eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X11),t2tb1(X16)),n1) ) )
& ( ? [X16: $int] :
( $less(X16,X13)
& ~ $less(X16,X2)
& eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X11),t2tb1(X16)),n1) )
| ~ partial_solution1(n1,X15)
| ~ eq_prefix1(int,t2tb2(X14),t2tb2(X15),X12) ) ) )
& ( n1 = X4 )
& ~ $less(X4,0)
& ( 0 = X1 )
& ( 0 = X2 ) ),
inference(flattening,[],[f128]) ).
tff(f130,plain,
? [X0: $int,X1: $int,X2: map_int_int,X3: $int,X4: map_int_lpmap_int_intrp] :
( ! [X5: $int] :
( $less(X5,0)
| ( ( ~ mem(int,t2tb1(X5),empty(int))
| ? [X6: $int] :
( ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X6))) = $sum($sum(X5,X6),$uminus(X1)) )
& $less(X6,X1)
& ~ $less(X6,0) ) )
& ( ! [X7: $int] :
( ( $sum($sum(X5,X7),$uminus(X1)) != tb2t1(get(int,int,t2tb2(X2),t2tb1(X7))) )
| ~ $less(X7,X1)
| $less(X7,0) )
| mem(int,t2tb1(X5),empty(int)) ) ) )
& ( n1 = $sum(X1,cardinal1(int,t2tb(below1(X3)))) )
& ! [X8: $int] :
( $less(X8,0)
| ( ( ! [X9: $int] :
( ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X9))) != $sum($sum(X8,X1),$uminus(X9)) )
| $less(X9,0)
| ~ $less(X9,X1) )
| mem(int,t2tb1(X8),empty(int)) )
& ( ~ mem(int,t2tb1(X8),empty(int))
| ? [X10: $int] :
( ( $sum($sum(X8,X1),$uminus(X10)) = tb2t1(get(int,int,t2tb2(X2),t2tb1(X10))) )
& ~ $less(X10,0)
& $less(X10,X1) ) ) ) )
& partial_solution1(X1,X2)
& ~ $less(X1,0)
& ~ $less(X0,0)
& ! [X11: $int] :
( ( mem(int,t2tb1(X11),t2tb(below1(X3)))
| ~ $less(X11,n1)
| $less(X11,0)
| ? [X12: $int] :
( $less(X12,X1)
& ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X12))) = X11 )
& ~ $less(X12,0) ) )
& ( ( $less(X11,n1)
& ~ $less(X11,0)
& ! [X13: $int] :
( ~ $less(X13,X1)
| ( tb2t1(get(int,int,t2tb2(X2),t2tb1(X13))) != X11 )
| $less(X13,0) ) )
| ~ mem(int,t2tb1(X11),t2tb(below1(X3))) ) )
& ? [X14: map_int_lpmap_int_intrp,X15: map_int_int,X16: $int,X17: $int] :
( eq_prefix1(map(int,int),t2tb3(X4),t2tb3(X14),X0)
& sorted1(X14,X0,X16)
& eq_prefix1(int,t2tb2(X2),t2tb2(X15),X17)
& ~ $less($sum(X16,$uminus(X0)),0)
& ( ~ sorted1(X14,0,X16)
| ? [X18: map_int_int] :
( ( ~ partial_solution1(n1,X18)
| ! [X19: $int] :
( $less(X19,0)
| ~ eq_prefix1(int,t2tb2(X18),get(map(int,int),int,t2tb3(X14),t2tb1(X19)),n1)
| ~ $less(X19,$sum(X16,$uminus(X0))) ) )
& ( partial_solution1(n1,X18)
| ? [X20: $int] :
( ~ $less(X20,0)
& eq_prefix1(int,t2tb2(X18),get(map(int,int),int,t2tb3(X14),t2tb1(X20)),n1)
& $less(X20,$sum(X16,$uminus(X0))) ) ) )
| ( $sum(X16,$uminus(X0)) != X16 ) )
& ( X1 = X17 )
& ! [X21: map_int_int] :
( ( ( partial_solution1(n1,X21)
& eq_prefix1(int,t2tb2(X15),t2tb2(X21),X17) )
| ! [X22: $int] :
( ~ $less(X22,X16)
| $less(X22,X0)
| ~ eq_prefix1(int,t2tb2(X21),get(map(int,int),int,t2tb3(X14),t2tb1(X22)),n1) ) )
& ( ? [X23: $int] :
( $less(X23,X16)
& ~ $less(X23,X0)
& eq_prefix1(int,t2tb2(X21),get(map(int,int),int,t2tb3(X14),t2tb1(X23)),n1) )
| ~ partial_solution1(n1,X21)
| ~ eq_prefix1(int,t2tb2(X15),t2tb2(X21),X17) ) ) )
& ( n1 = X3 )
& ~ $less(X3,0)
& ( 0 = X1 )
& ( 0 = X0 ) ),
inference(rectify,[],[f129]) ).
tff(f131,plain,
( ! [X5: $int] :
( $less(X5,0)
| ( ( ~ mem(int,t2tb1(X5),empty(int))
| ( ( tb2t1(get(int,int,t2tb2(sK4),t2tb1(sK7(X5)))) = $sum($sum(X5,sK7(X5)),$uminus(sK3)) )
& $less(sK7(X5),sK3)
& ~ $less(sK7(X5),0) ) )
& ( ! [X7: $int] :
( ( tb2t1(get(int,int,t2tb2(sK4),t2tb1(X7))) != $sum($sum(X5,X7),$uminus(sK3)) )
| ~ $less(X7,sK3)
| $less(X7,0) )
| mem(int,t2tb1(X5),empty(int)) ) ) )
& ( n1 = $sum(sK3,cardinal1(int,t2tb(below1(sK5)))) )
& ! [X8: $int] :
( $less(X8,0)
| ( ( ! [X9: $int] :
( ( tb2t1(get(int,int,t2tb2(sK4),t2tb1(X9))) != $sum($sum(X8,sK3),$uminus(X9)) )
| $less(X9,0)
| ~ $less(X9,sK3) )
| mem(int,t2tb1(X8),empty(int)) )
& ( ~ mem(int,t2tb1(X8),empty(int))
| ( ( tb2t1(get(int,int,t2tb2(sK4),t2tb1(sK8(X8)))) = $sum($sum(X8,sK3),$uminus(sK8(X8))) )
& ~ $less(sK8(X8),0)
& $less(sK8(X8),sK3) ) ) ) )
& partial_solution1(sK3,sK4)
& ~ $less(sK3,0)
& ~ $less(sK2,0)
& ! [X11: $int] :
( ( mem(int,t2tb1(X11),t2tb(below1(sK5)))
| ~ $less(X11,n1)
| $less(X11,0)
| ( $less(sK9(X11),sK3)
& ( tb2t1(get(int,int,t2tb2(sK4),t2tb1(sK9(X11)))) = X11 )
& ~ $less(sK9(X11),0) ) )
& ( ( $less(X11,n1)
& ~ $less(X11,0)
& ! [X13: $int] :
( ~ $less(X13,sK3)
| ( tb2t1(get(int,int,t2tb2(sK4),t2tb1(X13))) != X11 )
| $less(X13,0) ) )
| ~ mem(int,t2tb1(X11),t2tb(below1(sK5))) ) )
& eq_prefix1(map(int,int),t2tb3(sK6),t2tb3(sK10),sK2)
& sorted1(sK10,sK2,sK12)
& eq_prefix1(int,t2tb2(sK4),t2tb2(sK11),sK13)
& ~ $less($sum(sK12,$uminus(sK2)),0)
& ( ~ sorted1(sK10,0,sK12)
| ( ( ~ partial_solution1(n1,sK14)
| ! [X19: $int] :
( $less(X19,0)
| ~ eq_prefix1(int,t2tb2(sK14),get(map(int,int),int,t2tb3(sK10),t2tb1(X19)),n1)
| ~ $less(X19,$sum(sK12,$uminus(sK2))) ) )
& ( partial_solution1(n1,sK14)
| ( ~ $less(sK15,0)
& eq_prefix1(int,t2tb2(sK14),get(map(int,int),int,t2tb3(sK10),t2tb1(sK15)),n1)
& $less(sK15,$sum(sK12,$uminus(sK2))) ) ) )
| ( sK12 != $sum(sK12,$uminus(sK2)) ) )
& ( sK3 = sK13 )
& ! [X21: map_int_int] :
( ( ( partial_solution1(n1,X21)
& eq_prefix1(int,t2tb2(sK11),t2tb2(X21),sK13) )
| ! [X22: $int] :
( ~ $less(X22,sK12)
| $less(X22,sK2)
| ~ eq_prefix1(int,t2tb2(X21),get(map(int,int),int,t2tb3(sK10),t2tb1(X22)),n1) ) )
& ( ( $less(sK16(X21),sK12)
& ~ $less(sK16(X21),sK2)
& eq_prefix1(int,t2tb2(X21),get(map(int,int),int,t2tb3(sK10),t2tb1(sK16(X21))),n1) )
| ~ partial_solution1(n1,X21)
| ~ eq_prefix1(int,t2tb2(sK11),t2tb2(X21),sK13) ) )
& ( n1 = sK5 )
& ~ $less(sK5,0)
& ( 0 = sK3 )
& ( 0 = sK2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK6),skolemize(X6,sK7(X5)),skolemize(X10,sK8(X8)),skolemize(X12,sK9(X11)),skolemize(X14,sK10),skolemize(X15,sK11),skolemize(X16,sK12),skolemize(X17,sK13),skolemize(X18,sK14),skolemize(X20,sK15),skolemize(X23,sK16(X21))],[f130]) ).
tff(f144,plain,
! [X2: uni,X3: $int,X0: ty,X1: uni] :
( ~ $less(sK1(X0,X1,X2,X3),0)
| eq_prefix1(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f127]) ).
tff(f145,plain,
! [X2: uni,X3: $int,X0: ty,X1: uni] :
( $less(sK1(X0,X1,X2,X3),X3)
| eq_prefix1(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f127]) ).
tff(f148,plain,
0 = sK2,
inference(cnf_transformation,[],[f131]) ).
tff(f149,plain,
0 = sK3,
inference(cnf_transformation,[],[f131]) ).
tff(f151,plain,
n1 = sK5,
inference(cnf_transformation,[],[f131]) ).
tff(f152,plain,
! [X21: map_int_int] :
( eq_prefix1(int,t2tb2(X21),get(map(int,int),int,t2tb3(sK10),t2tb1(sK16(X21))),n1)
| ~ partial_solution1(n1,X21)
| ~ eq_prefix1(int,t2tb2(sK11),t2tb2(X21),sK13) ),
inference(cnf_transformation,[],[f131]) ).
tff(f153,plain,
! [X21: map_int_int] :
( ~ $less(sK16(X21),sK2)
| ~ partial_solution1(n1,X21)
| ~ eq_prefix1(int,t2tb2(sK11),t2tb2(X21),sK13) ),
inference(cnf_transformation,[],[f131]) ).
tff(f154,plain,
! [X21: map_int_int] :
( $less(sK16(X21),sK12)
| ~ partial_solution1(n1,X21)
| ~ eq_prefix1(int,t2tb2(sK11),t2tb2(X21),sK13) ),
inference(cnf_transformation,[],[f131]) ).
tff(f156,plain,
! [X21: map_int_int,X22: $int] :
( partial_solution1(n1,X21)
| ~ $less(X22,sK12)
| $less(X22,sK2)
| ~ eq_prefix1(int,t2tb2(X21),get(map(int,int),int,t2tb3(sK10),t2tb1(X22)),n1) ),
inference(cnf_transformation,[],[f131]) ).
tff(f157,plain,
sK3 = sK13,
inference(cnf_transformation,[],[f131]) ).
tff(f158,plain,
( ~ sorted1(sK10,0,sK12)
| partial_solution1(n1,sK14)
| $less(sK15,$sum(sK12,$uminus(sK2)))
| ( sK12 != $sum(sK12,$uminus(sK2)) ) ),
inference(cnf_transformation,[],[f131]) ).
tff(f159,plain,
( ~ sorted1(sK10,0,sK12)
| partial_solution1(n1,sK14)
| eq_prefix1(int,t2tb2(sK14),get(map(int,int),int,t2tb3(sK10),t2tb1(sK15)),n1)
| ( sK12 != $sum(sK12,$uminus(sK2)) ) ),
inference(cnf_transformation,[],[f131]) ).
tff(f160,plain,
( ~ sorted1(sK10,0,sK12)
| partial_solution1(n1,sK14)
| ~ $less(sK15,0)
| ( sK12 != $sum(sK12,$uminus(sK2)) ) ),
inference(cnf_transformation,[],[f131]) ).
tff(f161,plain,
! [X19: $int] :
( ~ sorted1(sK10,0,sK12)
| ~ partial_solution1(n1,sK14)
| $less(X19,0)
| ~ eq_prefix1(int,t2tb2(sK14),get(map(int,int),int,t2tb3(sK10),t2tb1(X19)),n1)
| ~ $less(X19,$sum(sK12,$uminus(sK2)))
| ( sK12 != $sum(sK12,$uminus(sK2)) ) ),
inference(cnf_transformation,[],[f131]) ).
tff(f164,plain,
sorted1(sK10,sK2,sK12),
inference(cnf_transformation,[],[f131]) ).
tff(f227,plain,
sorted1(sK10,0,sK12),
inference(definition_unfolding,[],[f164,f148]) ).
tff(f229,plain,
! [X19: $int] :
( ~ sorted1(sK10,0,sK12)
| ~ partial_solution1(sK5,sK14)
| $less(X19,0)
| ~ eq_prefix1(int,t2tb2(sK14),get(map(int,int),int,t2tb3(sK10),t2tb1(X19)),sK5)
| ~ $less(X19,$sum(sK12,$uminus(0)))
| ( $sum(sK12,$uminus(0)) != sK12 ) ),
inference(definition_unfolding,[],[f161,f151,f151,f148,f148]) ).
tff(f230,plain,
( ~ sorted1(sK10,0,sK12)
| partial_solution1(sK5,sK14)
| ~ $less(sK15,0)
| ( $sum(sK12,$uminus(0)) != sK12 ) ),
inference(definition_unfolding,[],[f160,f151,f148]) ).
tff(f231,plain,
( ~ sorted1(sK10,0,sK12)
| partial_solution1(sK5,sK14)
| eq_prefix1(int,t2tb2(sK14),get(map(int,int),int,t2tb3(sK10),t2tb1(sK15)),sK5)
| ( $sum(sK12,$uminus(0)) != sK12 ) ),
inference(definition_unfolding,[],[f159,f151,f151,f148]) ).
tff(f232,plain,
( ~ sorted1(sK10,0,sK12)
| partial_solution1(sK5,sK14)
| $less(sK15,$sum(sK12,$uminus(0)))
| ( $sum(sK12,$uminus(0)) != sK12 ) ),
inference(definition_unfolding,[],[f158,f151,f148,f148]) ).
tff(f233,plain,
! [X21: map_int_int,X22: $int] :
( partial_solution1(sK5,X21)
| ~ $less(X22,sK12)
| $less(X22,0)
| ~ eq_prefix1(int,t2tb2(X21),get(map(int,int),int,t2tb3(sK10),t2tb1(X22)),sK5) ),
inference(definition_unfolding,[],[f156,f151,f148,f151]) ).
tff(f235,plain,
! [X21: map_int_int] :
( $less(sK16(X21),sK12)
| ~ partial_solution1(sK5,X21)
| ~ eq_prefix1(int,t2tb2(sK11),t2tb2(X21),sK13) ),
inference(definition_unfolding,[],[f154,f151]) ).
tff(f236,plain,
! [X21: map_int_int] :
( ~ $less(sK16(X21),0)
| ~ partial_solution1(sK5,X21)
| ~ eq_prefix1(int,t2tb2(sK11),t2tb2(X21),sK13) ),
inference(definition_unfolding,[],[f153,f148,f151]) ).
tff(f237,plain,
! [X21: map_int_int] :
( eq_prefix1(int,t2tb2(X21),get(map(int,int),int,t2tb3(sK10),t2tb1(sK16(X21))),sK5)
| ~ partial_solution1(sK5,X21)
| ~ eq_prefix1(int,t2tb2(sK11),t2tb2(X21),sK13) ),
inference(definition_unfolding,[],[f152,f151,f151]) ).
tff(f238,plain,
0 = sK13,
inference(definition_unfolding,[],[f149,f157]) ).
tff(f299,definition,
sF46 = map(int,int),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
tff(f300,plain,
map(int,int) = sF46,
inference(reorient_equations,[],[f299]) ).
tff(f303,definition,
sF48 = t2tb3(sK10),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
tff(f304,plain,
t2tb3(sK10) = sF48,
inference(reorient_equations,[],[f303]) ).
tff(f306,definition,
sF49 = t2tb2(sK11),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
tff(f308,definition,
sF50 = $uminus(0),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
tff(f309,plain,
$uminus(0) = sF50,
inference(reorient_equations,[],[f308]) ).
tff(f310,definition,
sF51 = $sum(sK12,sF50),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
tff(f312,definition,
sF52 = t2tb2(sK14),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
tff(f313,definition,
! [X19: $int] : ( sF53(X19) = get(sF46,int,sF48,t2tb1(X19)) ),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
tff(f314,plain,
! [X19: $int] :
( ~ partial_solution1(sK5,sK14)
| ~ $less(X19,sF51)
| ( sF51 != sK12 )
| ~ eq_prefix1(int,sF52,sF53(X19),sK5)
| ~ sorted1(sK10,0,sK12)
| $less(X19,0) ),
inference(definition_folding,[],[f229,f310,f309,f310,f309,f313,f304,f300,f312]) ).
tff(f315,plain,
( partial_solution1(sK5,sK14)
| ( sF51 != sK12 )
| ~ $less(sK15,0)
| ~ sorted1(sK10,0,sK12) ),
inference(definition_folding,[],[f230,f310,f309]) ).
tff(f316,definition,
sF54 = t2tb1(sK15),
introduced(definition,[new_symbols(definition,[sF54])],[function_definition]) ).
tff(f317,plain,
t2tb1(sK15) = sF54,
inference(reorient_equations,[],[f316]) ).
tff(f318,definition,
sF55 = get(sF46,int,sF48,sF54),
introduced(definition,[new_symbols(definition,[sF55])],[function_definition]) ).
tff(f319,plain,
get(sF46,int,sF48,sF54) = sF55,
inference(reorient_equations,[],[f318]) ).
tff(f320,plain,
( partial_solution1(sK5,sK14)
| ~ sorted1(sK10,0,sK12)
| eq_prefix1(int,sF52,sF55,sK5)
| ( sF51 != sK12 ) ),
inference(definition_folding,[],[f231,f310,f309,f319,f317,f304,f300,f312]) ).
tff(f321,plain,
( partial_solution1(sK5,sK14)
| ( sF51 != sK12 )
| $less(sK15,sF51)
| ~ sorted1(sK10,0,sK12) ),
inference(definition_folding,[],[f232,f310,f309,f310,f309]) ).
tff(f322,plain,
! [X21: map_int_int,X22: $int] :
( ~ eq_prefix1(int,t2tb2(X21),sF53(X22),sK5)
| partial_solution1(sK5,X21)
| ~ $less(X22,sK12)
| $less(X22,0) ),
inference(definition_folding,[],[f233,f313,f304,f300]) ).
tff(f324,plain,
! [X21: map_int_int] :
( ~ partial_solution1(sK5,X21)
| ~ eq_prefix1(int,sF49,t2tb2(X21),sK13)
| $less(sK16(X21),sK12) ),
inference(definition_folding,[],[f235,f306]) ).
tff(f325,plain,
! [X21: map_int_int] :
( ~ eq_prefix1(int,sF49,t2tb2(X21),sK13)
| ~ $less(sK16(X21),0)
| ~ partial_solution1(sK5,X21) ),
inference(definition_folding,[],[f236,f306]) ).
tff(f326,definition,
! [X21: map_int_int] : ( sF56(X21) = t2tb1(sK16(X21)) ),
introduced(definition,[new_symbols(definition,[sF56])],[function_definition]) ).
tff(f327,plain,
! [X21: map_int_int] : ( t2tb1(sK16(X21)) = sF56(X21) ),
inference(reorient_equations,[],[f326]) ).
tff(f328,definition,
! [X21: map_int_int] : ( sF57(X21) = get(sF46,int,sF48,sF56(X21)) ),
introduced(definition,[new_symbols(definition,[sF57])],[function_definition]) ).
tff(f329,plain,
! [X21: map_int_int] : ( get(sF46,int,sF48,sF56(X21)) = sF57(X21) ),
inference(reorient_equations,[],[f328]) ).
tff(f330,plain,
! [X21: map_int_int] :
( ~ partial_solution1(sK5,X21)
| ~ eq_prefix1(int,sF49,t2tb2(X21),sK13)
| eq_prefix1(int,t2tb2(X21),sF57(X21),sK5) ),
inference(definition_folding,[],[f237,f306,f329,f327,f304,f300]) ).
tff(f362,definition,
( spl73_1
<=> eq_prefix1(int,sF52,sF55,sK5) ),
introduced(definition,[new_symbols(definition,[spl73_1])],[avatar_definition]) ).
tff(f364,plain,
( eq_prefix1(int,sF52,sF55,sK5)
| ~ spl73_1 ),
inference(avatar_component_clause,[],[f362]) ).
tff(f366,definition,
( spl73_2
<=> sorted1(sK10,0,sK12) ),
introduced(definition,[new_symbols(definition,[spl73_2])],[avatar_definition]) ).
tff(f370,definition,
( spl73_3
<=> partial_solution1(sK5,sK14) ),
introduced(definition,[new_symbols(definition,[spl73_3])],[avatar_definition]) ).
tff(f374,definition,
( spl73_4
<=> ( sF51 = sK12 ) ),
introduced(definition,[new_symbols(definition,[spl73_4])],[avatar_definition]) ).
tff(f375,plain,
( ( sF51 = sK12 )
| ~ spl73_4 ),
inference(avatar_component_clause,[],[f374]) ).
tff(f377,plain,
( spl73_1
| ~ spl73_2
| spl73_3
| ~ spl73_4 ),
inference(avatar_split_clause,[],[f320,f374,f370,f366,f362]) ).
tff(f379,definition,
( spl73_5
<=> ! [X19: $int] :
( ~ $less(X19,sF51)
| $less(X19,0)
| ~ eq_prefix1(int,sF52,sF53(X19),sK5) ) ),
introduced(definition,[new_symbols(definition,[spl73_5])],[avatar_definition]) ).
tff(f380,plain,
( ! [X19: $int] :
( $less(X19,0)
| ~ eq_prefix1(int,sF52,sF53(X19),sK5)
| ~ $less(X19,sF51) )
| ~ spl73_5 ),
inference(avatar_component_clause,[],[f379]) ).
tff(f381,plain,
( ~ spl73_2
| ~ spl73_3
| ~ spl73_4
| spl73_5 ),
inference(avatar_split_clause,[],[f314,f379,f374,f370,f366]) ).
tff(f383,definition,
( spl73_6
<=> $less(sK15,0) ),
introduced(definition,[new_symbols(definition,[spl73_6])],[avatar_definition]) ).
tff(f385,plain,
( ~ $less(sK15,0)
| spl73_6 ),
inference(avatar_component_clause,[],[f383]) ).
tff(f386,plain,
( ~ spl73_4
| ~ spl73_2
| spl73_3
| ~ spl73_6 ),
inference(avatar_split_clause,[],[f315,f383,f370,f366,f374]) ).
tff(f387,plain,
spl73_2,
inference(avatar_split_clause,[],[f227,f366]) ).
tff(f389,definition,
( spl73_7
<=> $less(sK15,sF51) ),
introduced(definition,[new_symbols(definition,[spl73_7])],[avatar_definition]) ).
tff(f391,plain,
( $less(sK15,sF51)
| ~ spl73_7 ),
inference(avatar_component_clause,[],[f389]) ).
tff(f392,plain,
( spl73_7
| ~ spl73_2
| ~ spl73_4
| spl73_3 ),
inference(avatar_split_clause,[],[f321,f370,f374,f366,f389]) ).
tff(f400,plain,
! [X21: map_int_int] :
( ~ eq_prefix1(int,sF49,t2tb2(X21),0)
| $less(sK16(X21),sK12)
| ~ partial_solution1(sK5,X21) ),
inference(forward_demodulation,[],[f324,f238]) ).
tff(f401,plain,
! [X21: map_int_int] :
( ~ eq_prefix1(int,sF49,t2tb2(X21),0)
| ~ $less(sK16(X21),0)
| ~ partial_solution1(sK5,X21) ),
inference(forward_demodulation,[],[f325,f238]) ).
tff(f410,plain,
! [X21: map_int_int] :
( eq_prefix1(int,t2tb2(X21),sF57(X21),sK5)
| ~ partial_solution1(sK5,X21)
| ~ eq_prefix1(int,sF49,t2tb2(X21),0) ),
inference(forward_demodulation,[],[f330,f238]) ).
tff(f485,plain,
0 = sF50,
inference(evaluation,[],[f309]) ).
tff(f487,plain,
( ~ eq_prefix1(int,sF49,sF52,0)
| eq_prefix1(int,sF52,sF57(sK14),sK5)
| ~ partial_solution1(sK5,sK14) ),
inference(superposition,[],[f410,f312]) ).
tff(f488,plain,
! [X0: $int] :
( ~ $less(X0,sK12)
| $less(X0,0)
| ~ eq_prefix1(int,sF52,sF53(X0),sK5)
| partial_solution1(sK5,sK14) ),
inference(superposition,[],[f322,f312]) ).
tff(f489,plain,
( ~ $less(sK16(sK14),0)
| ~ eq_prefix1(int,sF49,sF52,0)
| ~ partial_solution1(sK5,sK14) ),
inference(superposition,[],[f401,f312]) ).
tff(f490,plain,
( ~ partial_solution1(sK5,sK14)
| $less(sK16(sK14),sK12)
| ~ eq_prefix1(int,sF49,sF52,0) ),
inference(superposition,[],[f400,f312]) ).
tff(f492,definition,
( spl73_20
<=> ! [X0: $int] :
( $less(X0,0)
| ~ eq_prefix1(int,sF52,sF53(X0),sK5)
| ~ $less(X0,sK12) ) ),
introduced(definition,[new_symbols(definition,[spl73_20])],[avatar_definition]) ).
tff(f493,plain,
( ! [X0: $int] :
( ~ eq_prefix1(int,sF52,sF53(X0),sK5)
| ~ $less(X0,sK12)
| $less(X0,0) )
| ~ spl73_20 ),
inference(avatar_component_clause,[],[f492]) ).
tff(f495,definition,
( spl73_21
<=> eq_prefix1(int,sF49,sF52,0) ),
introduced(definition,[new_symbols(definition,[spl73_21])],[avatar_definition]) ).
tff(f496,plain,
( ~ eq_prefix1(int,sF49,sF52,0)
| spl73_21 ),
inference(avatar_component_clause,[],[f495]) ).
tff(f500,definition,
( spl73_22
<=> $less(sK16(sK14),0) ),
introduced(definition,[new_symbols(definition,[spl73_22])],[avatar_definition]) ).
tff(f502,plain,
( ~ $less(sK16(sK14),0)
| spl73_22 ),
inference(avatar_component_clause,[],[f500]) ).
tff(f503,plain,
( ~ spl73_21
| ~ spl73_3
| ~ spl73_22 ),
inference(avatar_split_clause,[],[f489,f500,f370,f495]) ).
tff(f505,definition,
( spl73_23
<=> $less(sK16(sK14),sK12) ),
introduced(definition,[new_symbols(definition,[spl73_23])],[avatar_definition]) ).
tff(f507,plain,
( $less(sK16(sK14),sK12)
| ~ spl73_23 ),
inference(avatar_component_clause,[],[f505]) ).
tff(f508,plain,
( ~ spl73_21
| spl73_23
| ~ spl73_3 ),
inference(avatar_split_clause,[],[f490,f370,f505,f495]) ).
tff(f509,plain,
( spl73_20
| spl73_3 ),
inference(avatar_split_clause,[],[f488,f370,f492]) ).
tff(f511,definition,
( spl73_24
<=> eq_prefix1(int,sF52,sF57(sK14),sK5) ),
introduced(definition,[new_symbols(definition,[spl73_24])],[avatar_definition]) ).
tff(f513,plain,
( eq_prefix1(int,sF52,sF57(sK14),sK5)
| ~ spl73_24 ),
inference(avatar_component_clause,[],[f511]) ).
tff(f514,plain,
( spl73_24
| ~ spl73_21
| ~ spl73_3 ),
inference(avatar_split_clause,[],[f487,f370,f495,f511]) ).
tff(f581,plain,
sF51 = $sum(sK12,0),
inference(forward_demodulation,[],[f310,f485]) ).
tff(f582,plain,
sF51 = sK12,
inference(evaluation,[],[f581]) ).
tff(f585,plain,
spl73_4,
inference(avatar_split_clause,[],[f582,f374]) ).
tff(f587,plain,
( $less(sK15,sK12)
| ~ spl73_4
| ~ spl73_7 ),
inference(forward_demodulation,[],[f391,f375]) ).
tff(f775,plain,
sF53(sK15) = get(sF46,int,sF48,sF54),
inference(superposition,[],[f313,f317]) ).
tff(f776,plain,
! [X0: map_int_int] : ( get(sF46,int,sF48,sF56(X0)) = sF53(sK16(X0)) ),
inference(superposition,[],[f313,f327]) ).
tff(f780,plain,
sF53(sK15) = sF55,
inference(forward_demodulation,[],[f775,f319]) ).
tff(f862,plain,
! [X2: uni,X0: ty,X1: uni] :
( eq_prefix1(X0,X1,X2,0)
| eq_prefix1(X0,X1,X2,0) ),
inference(resolution,[],[f145,f144]) ).
tff(f863,plain,
! [X2: uni,X0: ty,X1: uni] : eq_prefix1(X0,X1,X2,0),
inference(duplicate_literal_removal,[],[f862]) ).
tff(f1055,plain,
( ~ eq_prefix1(int,sF52,sF55,sK5)
| ~ $less(sK15,sK12)
| $less(sK15,0)
| ~ spl73_20 ),
inference(superposition,[],[f493,f780]) ).
tff(f1061,plain,
( $less(sK15,0)
| ~ $less(sK15,sK12)
| ~ spl73_1
| ~ spl73_20 ),
inference(forward_subsumption_resolution,[],[f1055,f364]) ).
tff(f1066,plain,
( ~ $less(sK15,sK12)
| ~ spl73_1
| spl73_6
| ~ spl73_20 ),
inference(forward_subsumption_resolution,[],[f1061,f385]) ).
tff(f1070,plain,
( $false
| ~ spl73_1
| ~ spl73_4
| spl73_6
| ~ spl73_7
| ~ spl73_20 ),
inference(forward_subsumption_resolution,[],[f1066,f587]) ).
tff(f1071,plain,
( ~ spl73_1
| ~ spl73_4
| spl73_6
| ~ spl73_7
| ~ spl73_20 ),
inference(avatar_contradiction_clause,[],[f1070]) ).
tff(f1075,plain,
( ! [X19: $int] :
( $less(X19,0)
| ~ eq_prefix1(int,sF52,sF53(X19),sK5)
| ~ $less(X19,sK12) )
| ~ spl73_4
| ~ spl73_5 ),
inference(forward_demodulation,[],[f380,f375]) ).
tff(f1107,plain,
( $false
| spl73_21 ),
inference(resolution,[],[f863,f496]) ).
tff(f1108,plain,
spl73_21,
inference(avatar_contradiction_clause,[],[f1107]) ).
tff(f1576,plain,
! [X0: map_int_int] : ( sF57(X0) = sF53(sK16(X0)) ),
inference(forward_demodulation,[],[f776,f329]) ).
tff(f1578,plain,
( ! [X0: map_int_int] :
( ~ eq_prefix1(int,sF52,sF57(X0),sK5)
| $less(sK16(X0),0)
| ~ $less(sK16(X0),sK12) )
| ~ spl73_20 ),
inference(superposition,[],[f493,f1576]) ).
tff(f1591,plain,
( $less(sK16(sK14),0)
| ~ $less(sK16(sK14),sK12)
| ~ spl73_20
| ~ spl73_24 ),
inference(resolution,[],[f1578,f513]) ).
tff(f1592,plain,
( ~ $less(sK16(sK14),sK12)
| ~ spl73_20
| spl73_22
| ~ spl73_24 ),
inference(forward_subsumption_resolution,[],[f1591,f502]) ).
tff(f1593,plain,
( $false
| ~ spl73_20
| spl73_22
| ~ spl73_23
| ~ spl73_24 ),
inference(forward_subsumption_resolution,[],[f1592,f507]) ).
tff(f1594,plain,
( ~ spl73_20
| spl73_22
| ~ spl73_23
| ~ spl73_24 ),
inference(avatar_contradiction_clause,[],[f1593]) ).
tff(f1595,plain,
( spl73_20
| ~ spl73_4
| ~ spl73_5 ),
inference(avatar_split_clause,[],[f1075,f379,f374,f492]) ).
cnf(s1,plain,
( spl73_1
| ~ spl73_2
| spl73_3
| ~ spl73_4 ),
inference(sat_conversion,[],[f377]) ).
cnf(s2,plain,
( ~ spl73_2
| ~ spl73_3
| ~ spl73_4
| spl73_5 ),
inference(sat_conversion,[],[f381]) ).
cnf(s3,plain,
( ~ spl73_2
| spl73_3
| ~ spl73_4
| ~ spl73_6 ),
inference(sat_conversion,[],[f386]) ).
cnf(s4,plain,
spl73_2,
inference(sat_conversion,[],[f387]) ).
cnf(s5,plain,
( ~ spl73_2
| spl73_3
| ~ spl73_4
| spl73_7 ),
inference(sat_conversion,[],[f392]) ).
cnf(s17,plain,
( ~ spl73_3
| ~ spl73_21
| ~ spl73_22 ),
inference(sat_conversion,[],[f503]) ).
cnf(s18,plain,
( ~ spl73_3
| ~ spl73_21
| spl73_23 ),
inference(sat_conversion,[],[f508]) ).
cnf(s19,plain,
( spl73_3
| spl73_20 ),
inference(sat_conversion,[],[f509]) ).
cnf(s20,plain,
( ~ spl73_3
| ~ spl73_21
| spl73_24 ),
inference(sat_conversion,[],[f514]) ).
cnf(s30,plain,
spl73_4,
inference(sat_conversion,[],[f585]) ).
cnf(s39,plain,
( ~ spl73_1
| ~ spl73_4
| spl73_6
| ~ spl73_7
| ~ spl73_20 ),
inference(sat_conversion,[],[f1071]) ).
cnf(s46,plain,
spl73_21,
inference(sat_conversion,[],[f1108]) ).
cnf(s49,plain,
( ~ spl73_20
| spl73_22
| ~ spl73_23
| ~ spl73_24 ),
inference(sat_conversion,[],[f1594]) ).
cnf(s50,plain,
( ~ spl73_4
| ~ spl73_5
| spl73_20 ),
inference(sat_conversion,[],[f1595]) ).
cnf(s51,plain,
( ~ spl73_3
| spl73_24 ),
inference(rat,[],[s20,s46]) ).
cnf(s52,plain,
( ~ spl73_3
| spl73_23 ),
inference(rat,[],[s18,s46]) ).
cnf(s53,plain,
( ~ spl73_3
| ~ spl73_22 ),
inference(rat,[],[s17,s46]) ).
cnf(s57,plain,
( ~ spl73_2
| spl73_3
| spl73_7 ),
inference(rat,[],[s5,s30]) ).
cnf(s58,plain,
( spl73_3
| ~ spl73_6 ),
inference(rat,[],[s3,s30,s4]) ).
cnf(s59,plain,
( ~ spl73_3
| spl73_5 ),
inference(rat,[],[s2,s30,s4]) ).
cnf(s60,plain,
( spl73_1
| spl73_3 ),
inference(rat,[],[s1,s30,s4]) ).
cnf(s61,plain,
~ spl73_3,
inference(rat,[],[s50,s49,s59,s53,s52,s51,s30]) ).
cnf(s62,plain,
spl73_20,
inference(rat,[],[s19,s61]) ).
cnf(s63,plain,
spl73_7,
inference(rat,[],[s57,s4,s61]) ).
cnf(s64,plain,
~ spl73_6,
inference(rat,[],[s58,s61]) ).
cnf(s65,plain,
spl73_1,
inference(rat,[],[s60,s61]) ).
cnf(s67,plain,
$false,
inference(rat,[],[s39,s62,s63,s30,s65,s64]) ).
tff(f1596,plain,
$false,
inference(avatar_sat_refutation,[],[s67]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW634_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.11/0.27 % Computer : n017.cluster.edu
% 0.11/0.27 % Model : x86_64 x86_64
% 0.11/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.27 % Memory : 8046.5625MB
% 0.11/0.27 % OS : Linux 6.8.0-71-generic
% 0.11/0.27 % CPULimit : 300
% 0.11/0.27 % WCLimit : 300
% 0.11/0.27 % DateTime : Mon Sep 28 14:18:21 UTC 2026
% 0.11/0.27 % CPUTime :
% 0.11/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.31 Running first-order theorem proving
% 0.25/0.31 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.29/1.78 % (3585389)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.29/1.78 % (3585399)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2661977111:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.29/1.78 % (3585401)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=99136752:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.29/1.78 % (3585401)Instruction limit reached!
% 5.29/1.78 % (3585401)------------------------------
% 5.29/1.78 % (3585401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.78 % (3585401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.78 % (3585401)CaDiCaL version: 2.1.3
% 5.29/1.78 % (3585401)Termination reason: Instruction limit
% 5.29/1.78 % (3585401)Termination phase: Function definition elimination
% 5.29/1.78 % (3585401)Time elapsed: 0.006 s
% 5.29/1.78 % (3585401)Peak memory usage: 86 MB
% 5.29/1.78 % (3585401)Instructions burned: 8 (million)
% 5.29/1.78 % (3585400)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3043410778:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.29/1.78 % (3585404)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3599929967:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.29/1.78 % (3585402)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=290496227:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.29/1.78 % (3585403)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=508934957:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.29/1.78 % (3585402)Instruction limit reached!
% 5.29/1.78 % (3585402)------------------------------
% 5.29/1.78 % (3585402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.78 % (3585402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.78 % (3585402)CaDiCaL version: 2.1.3
% 5.29/1.78 % (3585402)Termination reason: Instruction limit
% 5.29/1.78 % (3585402)Termination phase: Preprocessing 3
% 5.29/1.78 % (3585402)Time elapsed: 0.005 s
% 5.29/1.78 % (3585402)Peak memory usage: 86 MB
% 5.29/1.78 % (3585402)Instructions burned: 5 (million)
% 5.29/1.78 % (3585398)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1615932882:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.29/1.78 % (3585404)Instruction limit reached!
% 5.29/1.78 % (3585404)------------------------------
% 5.29/1.78 % (3585404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.78 % (3585404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.78 % (3585404)CaDiCaL version: 2.1.3
% 5.29/1.78 % (3585404)Termination reason: Instruction limit
% 5.29/1.78 % (3585404)Termination phase: Saturation
% 5.29/1.78 % (3585404)Time elapsed: 0.064 s
% 5.29/1.78 % (3585404)Peak memory usage: 116 MB
% 5.29/1.78 % (3585404)Instructions burned: 33 (million)
% 5.29/1.78 % (3585398)Instruction limit reached!
% 5.29/1.78 % (3585398)------------------------------
% 5.29/1.78 % (3585398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.78 % (3585398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.78 % (3585398)CaDiCaL version: 2.1.3
% 5.29/1.78 % (3585398)Termination reason: Instruction limit
% 5.29/1.78 % (3585398)Termination phase: Saturation
% 5.29/1.78 % (3585398)Time elapsed: 0.038 s
% 5.29/1.78 % (3585398)Peak memory usage: 106 MB
% 5.29/1.78 % (3585398)Instructions burned: 12 (million)
% 5.29/1.78 % (3585403)Instruction limit reached!
% 5.29/1.78 % (3585403)------------------------------
% 5.29/1.78 % (3585403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.78 % (3585403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.78 % (3585403)CaDiCaL version: 2.1.3
% 5.29/1.78 % (3585403)Termination reason: Instruction limit
% 5.29/1.78 % (3585403)Termination phase: Saturation
% 5.29/1.78 % (3585403)Time elapsed: 0.080 s
% 5.29/1.78 % (3585403)Peak memory usage: 116 MB
% 5.29/1.78 % (3585403)Instructions burned: 46 (million)
% 5.29/1.78 % (3585399)Instruction limit reached!
% 5.29/1.78 % (3585399)------------------------------
% 5.29/1.78 % (3585399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.78 % (3585399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.48/2.03 % (3585399)CaDiCaL version: 2.1.3
% 6.48/2.03 % (3585399)Termination reason: Instruction limit
% 6.48/2.03 % (3585399)Termination phase: Saturation
% 6.48/2.03 % (3585399)Time elapsed: 0.196 s
% 6.48/2.03 % (3585399)Peak memory usage: 118 MB
% 6.48/2.03 % (3585399)Instructions burned: 308 (million)
% 6.48/2.03 % (3585407)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=506727786:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 6.48/2.03 % (3585407)Instruction limit reached!
% 6.48/2.03 % (3585407)------------------------------
% 6.48/2.03 % (3585407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.48/2.03 % (3585407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.48/2.03 % (3585407)CaDiCaL version: 2.1.3
% 6.48/2.03 % (3585407)Termination reason: Instruction limit
% 6.48/2.03 % (3585407)Termination phase: Saturation
% 6.48/2.03 % (3585407)Time elapsed: 0.016 s
% 6.48/2.03 % (3585407)Peak memory usage: 89 MB
% 6.48/2.03 % (3585407)Instructions burned: 15 (million)
% 6.48/2.03 % (3585400)Instruction limit reached!
% 6.48/2.03 % (3585400)------------------------------
% 6.48/2.03 % (3585400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.48/2.03 % (3585400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.48/2.03 % (3585400)CaDiCaL version: 2.1.3
% 6.48/2.03 % (3585400)Termination reason: Instruction limit
% 6.48/2.03 % (3585400)Termination phase: Saturation
% 6.48/2.03 % (3585400)Time elapsed: 0.245 s
% 6.48/2.03 % (3585400)Peak memory usage: 118 MB
% 6.48/2.03 % (3585400)Instructions burned: 202 (million)
% 6.48/2.03 % (3585412)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=824417923:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 6.48/2.03 % (3585418)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2428625793:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 6.48/2.03 % (3585415)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=47007390:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 6.48/2.03 % (3585412)Instruction limit reached!
% 6.48/2.03 % (3585412)------------------------------
% 6.48/2.03 % (3585412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.48/2.03 % (3585412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.48/2.03 % (3585412)CaDiCaL version: 2.1.3
% 6.48/2.03 % (3585412)Termination reason: Instruction limit
% 6.48/2.03 % (3585412)Termination phase: Saturation
% 6.48/2.03 % (3585412)Time elapsed: 0.035 s
% 6.48/2.03 % (3585412)Peak memory usage: 89 MB
% 6.48/2.03 % (3585412)Instructions burned: 29 (million)
% 6.48/2.03 % (3585414)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3764775262:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi)
% 6.48/2.03 % (3585415)Instruction limit reached!
% 6.48/2.03 % (3585415)------------------------------
% 6.48/2.03 % (3585415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.48/2.03 % (3585415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.48/2.03 % (3585415)CaDiCaL version: 2.1.3
% 6.48/2.03 % (3585415)Termination reason: Instruction limit
% 6.48/2.03 % (3585415)Termination phase: Saturation
% 6.48/2.03 % (3585415)Time elapsed: 0.028 s
% 6.48/2.03 % (3585415)Peak memory usage: 89 MB
% 6.48/2.03 % (3585415)Instructions burned: 24 (million)
% 6.48/2.03 % (3585418)Instruction limit reached!
% 6.48/2.03 % (3585418)------------------------------
% 6.48/2.03 % (3585418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.48/2.03 % (3585418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.48/2.03 % (3585418)CaDiCaL version: 2.1.3
% 6.48/2.03 % (3585418)Termination reason: Instruction limit
% 6.48/2.03 % (3585418)Termination phase: Saturation
% 6.48/2.03 % (3585418)Time elapsed: 0.042 s
% 6.48/2.03 % (3585418)Peak memory usage: 89 MB
% 6.48/2.03 % (3585418)Instructions burned: 86 (million)
% 6.48/2.03 % (3585414)Instruction limit reached!
% 6.48/2.03 % (3585414)------------------------------
% 6.48/2.03 % (3585414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.48/2.03 % (3585414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.48/2.03 % (3585414)CaDiCaL version: 2.1.3
% 6.48/2.03 % (3585414)Termination reason: Instruction limit
% 8.39/2.17 % (3585414)Termination phase: Saturation
% 8.39/2.17 % (3585414)Time elapsed: 0.017 s
% 8.39/2.17 % (3585414)Peak memory usage: 89 MB
% 8.39/2.17 % (3585414)Instructions burned: 17 (million)
% 8.39/2.17 % (3585416)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=3153517009:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 8.39/2.17 % (3585416)Instruction limit reached!
% 8.39/2.17 % (3585416)------------------------------
% 8.39/2.17 % (3585416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585416)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585416)Termination reason: Instruction limit
% 8.39/2.17 % (3585416)Termination phase: Saturation
% 8.39/2.17 % (3585416)Time elapsed: 0.032 s
% 8.39/2.17 % (3585416)Peak memory usage: 90 MB
% 8.39/2.17 % (3585416)Instructions burned: 28 (million)
% 8.39/2.17 % (3585419)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1708710115:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 8.39/2.17 % (3585419)Instruction limit reached!
% 8.39/2.17 % (3585419)------------------------------
% 8.39/2.17 % (3585419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585419)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585419)Termination reason: Instruction limit
% 8.39/2.17 % (3585419)Termination phase: Preprocessing 1
% 8.39/2.17 % (3585419)Time elapsed: 0.003 s
% 8.39/2.17 % (3585419)Peak memory usage: 86 MB
% 8.39/2.17 % (3585419)Instructions burned: 3 (million)
% 8.39/2.17 % (3585421)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=150719619:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 8.39/2.17 % (3585428)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=4228105753:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 8.39/2.17 % (3585426)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3168815622:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 8.39/2.17 % (3585424)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=714776209:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 8.39/2.17 % (3585428)Instruction limit reached!
% 8.39/2.17 % (3585428)------------------------------
% 8.39/2.17 % (3585428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585428)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585428)Termination reason: Instruction limit
% 8.39/2.17 % (3585428)Termination phase: Function definition elimination
% 8.39/2.17 % (3585428)Time elapsed: 0.005 s
% 8.39/2.17 % (3585428)Peak memory usage: 86 MB
% 8.39/2.17 % (3585428)Instructions burned: 9 (million)
% 8.39/2.17 % (3585424)Instruction limit reached!
% 8.39/2.17 % (3585424)------------------------------
% 8.39/2.17 % (3585424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585424)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585424)Termination reason: Instruction limit
% 8.39/2.17 % (3585424)Termination phase: Preprocessing 3
% 8.39/2.17 % (3585424)Time elapsed: 0.005 s
% 8.39/2.17 % (3585424)Peak memory usage: 86 MB
% 8.39/2.17 % (3585424)Instructions burned: 4 (million)
% 8.39/2.17 % (3585427)lrs+10_1_thi=all:si=on:fd=off:random_seed=496805822:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 8.39/2.17 % (3585421)First to succeed.
% 8.39/2.17 % (3585421)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3585389"
% 8.39/2.17 % (3585430)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3019132987:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 8.39/2.17 % (3585430)Instruction limit reached!
% 8.39/2.17 % (3585430)------------------------------
% 8.39/2.17 % (3585430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585430)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585430)Termination reason: Instruction limit
% 8.39/2.17 % (3585430)Termination phase: Preprocessing 1
% 8.39/2.17 % (3585430)Time elapsed: 0.003 s
% 8.39/2.17 % (3585430)Peak memory usage: 85 MB
% 8.39/2.17 % (3585430)Instructions burned: 2 (million)
% 8.39/2.17 % (3585432)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2451581695:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 8.39/2.17 % (3585432)Instruction limit reached!
% 8.39/2.17 % (3585432)------------------------------
% 8.39/2.17 % (3585432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585432)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585432)Termination reason: Instruction limit
% 8.39/2.17 % (3585432)Termination phase: Preprocessing 1
% 8.39/2.17 % (3585432)Time elapsed: 0.003 s
% 8.39/2.17 % (3585432)Peak memory usage: 85 MB
% 8.39/2.17 % (3585432)Instructions burned: 2 (million)
% 8.39/2.17 % (3585426)Instruction limit reached!
% 8.39/2.17 % (3585426)------------------------------
% 8.39/2.17 % (3585426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585426)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585426)Termination reason: Instruction limit
% 8.39/2.17 % (3585426)Termination phase: Saturation
% 8.39/2.17 % (3585426)Time elapsed: 0.133 s
% 8.39/2.17 % (3585426)Peak memory usage: 134 MB
% 8.39/2.17 % (3585426)Instructions burned: 66 (million)
% 8.39/2.17 % (3585427)Instruction limit reached!
% 8.39/2.17 % (3585427)------------------------------
% 8.39/2.17 % (3585427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585427)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585427)Termination reason: Instruction limit
% 8.39/2.17 % (3585427)Termination phase: Saturation
% 8.39/2.17 % (3585427)Time elapsed: 0.093 s
% 8.39/2.17 % (3585427)Peak memory usage: 116 MB
% 8.39/2.17 % (3585427)Instructions burned: 53 (million)
% 8.39/2.17 % (3585437)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2466469601:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 8.39/2.17 % (3585438)dis+10_1_si=on:random_seed=2439154786:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 8.39/2.17 % (3585438)Instruction limit reached!
% 8.39/2.17 % (3585438)------------------------------
% 8.39/2.17 % (3585438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585438)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585438)Termination reason: Instruction limit
% 8.39/2.17 % (3585438)Termination phase: Property scanning
% 8.39/2.17 % (3585438)Time elapsed: 0.006 s
% 8.39/2.17 % (3585438)Peak memory usage: 87 MB
% 8.39/2.17 % (3585438)Instructions burned: 10 (million)
% 8.39/2.17 % (3585443)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=693450474: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)
% 8.39/2.17 % (3585441)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3028934273:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 8.39/2.17 % (3585443)Instruction limit reached!
% 8.39/2.17 % (3585443)------------------------------
% 8.39/2.17 % (3585443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585443)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585443)Termination reason: Instruction limit
% 8.39/2.17 % (3585443)Termination phase: Saturation
% 8.39/2.17 % (3585443)Time elapsed: 0.028 s
% 8.39/2.17 % (3585443)Peak memory usage: 89 MB
% 8.39/2.17 % (3585443)Instructions burned: 35 (million)
% 8.39/2.17 % (3585441)Refutation not found, incomplete strategy
% 8.39/2.17 % (3585441)------------------------------
% 8.39/2.17 % (3585441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585441)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585441)Termination reason: Refutation not found, incomplete strategy
% 8.39/2.17 % (3585441)Time elapsed: 0.019 s
% 8.39/2.17 % (3585441)Peak memory usage: 89 MB
% 8.39/2.17 % (3585441)Instructions burned: 17 (million)
% 8.39/2.17 % (3585437)Instruction limit reached!
% 8.39/2.17 % (3585437)------------------------------
% 8.39/2.17 % (3585437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585437)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585437)Termination reason: Instruction limit
% 8.39/2.17 % (3585437)Termination phase: Saturation
% 8.39/2.17 % (3585437)Time elapsed: 0.173 s
% 8.39/2.17 % (3585437)Peak memory usage: 117 MB
% 8.39/2.17 % (3585437)Instructions burned: 127 (million)
% 8.39/2.17 % (3585444)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1780770089:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 8.39/2.17 % (3585444)Instruction limit reached!
% 8.39/2.17 % (3585444)------------------------------
% 8.39/2.17 % (3585444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585444)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585444)Termination reason: Instruction limit
% 8.39/2.17 % (3585444)Termination phase: Preprocessing 1
% 8.39/2.17 % (3585444)Time elapsed: 0.003 s
% 8.39/2.17 % (3585444)Peak memory usage: 85 MB
% 8.39/2.17 % (3585444)Instructions burned: 3 (million)
% 8.39/2.17 % (3585445)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3508832737:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 8.39/2.17 % (3585445)Instruction limit reached!
% 8.39/2.17 % (3585445)------------------------------
% 8.39/2.17 % (3585445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.39/2.17 % (3585445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.39/2.17 % (3585445)CaDiCaL version: 2.1.3
% 8.39/2.17 % (3585445)Termination reason: Instruction limit
% 8.39/2.17 % (3585445)Termination phase: Property scanning
% 8.39/2.17 % (3585445)Time elapsed: 0.010 s
% 8.39/2.17 % (3585445)Peak memory usage: 87 MB
% 8.39/2.17 % (3585445)Instructions burned: 9 (million)
% 8.39/2.17 % (3585421)Refutation found. Thanks to Tanya!
% 8.39/2.17 % SZS status Theorem for theBenchmark
% 8.39/2.17 % SZS output start Proof for theBenchmark
% See solution above
% 9.78/2.46 % (3585421)------------------------------
% 9.78/2.46 % (3585421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.78/2.46 % (3585421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.78/2.46 % (3585421)CaDiCaL version: 2.1.3
% 9.78/2.46 % (3585421)Termination reason: Refutation
% 9.78/2.46 % (3585421)Time elapsed: 0.097 s
% 9.78/2.46 % (3585421)Peak memory usage: 91 MB
% 9.78/2.46 % (3585421)Instructions burned: 83 (million)
% 9.78/2.46 % (3585421)------------------------------
% 9.78/2.46 % (3585421)------------------------------
% 9.78/2.46 % (3585389)Success in time 1.262 s
% 9.78/2.46 % Vampire exiting
%------------------------------------------------------------------------------