%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:40:34 PM UTC 2026
% Result : Theorem 0.27s 0.35s
% Output : Refutation 0.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 13
% Syntax : Number of formulae : 113 ( 23 unt; 0 typ; 7 def)
% Number of atoms : 787 ( 133 equ)
% Maximal formula atoms : 63 ( 6 avg)
% Number of connectives : 1018 ( 344 ~; 296 |; 303 &)
% ( 39 <=>; 34 =>; 0 <=; 2 <~>)
% Maximal formula depth : 35 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 868 ( 296 atm; 176 fun; 228 num; 168 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 : 21 ( 17 usr; 8 prp; 0-4 aty)
% Number of functors : 68 ( 64 usr; 21 con; 0-5 aty)
% Number of variables : 273 ( 0 sgn 194 !; 79 ?; 273 :)
% 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 ) > uni ).
tff(func_def_47,type,
sK2: ( ty * uni * uni ) > uni ).
tff(func_def_48,type,
sK3: ( ty * uni ) > uni ).
tff(func_def_49,type,
sK4: ( ty * uni * uni * $int ) > $int ).
tff(func_def_50,type,
sK5: ( map_int_int * $int ) > $int ).
tff(func_def_51,type,
sK6: ( map_int_int * $int ) > $int ).
tff(func_def_52,type,
sK7: ( map_int_int * map_int_int ) > $int ).
tff(func_def_53,type,
sK8: ( map_int_lpmap_int_intrp * $int * $int ) > $int ).
tff(func_def_54,type,
sK9: ( map_int_lpmap_int_intrp * $int * $int ) > $int ).
tff(func_def_55,type,
sK10: $int ).
tff(func_def_56,type,
sK11: $int ).
tff(func_def_57,type,
sK12: map_int_lpmap_int_intrp ).
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_lpmap_int_intrp ).
tff(func_def_62,type,
sK17: $int ).
tff(func_def_63,type,
sK18: map_int_int ).
tff(func_def_64,type,
sK19: map_int_int ).
tff(func_def_65,type,
sK20: $int ).
tff(func_def_66,type,
sK21: map_int_int > $int ).
tff(func_def_67,type,
sK22: $int > $int ).
tff(func_def_68,type,
sK23: $int > $int ).
tff(func_def_69,type,
sK24: $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(f44,axiom,
! [X0: $int] : ( tb2t1(t2tb1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL1) ).
tff(f45,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR1) ).
tff(f64,axiom,
! [X0: ty,X1: uni,X2: uni,X3: $int] :
( eq_prefix1(X0,X1,X2,X3)
<=> ! [X4: $int] :
( ( $lesseq(0,X4)
& $less(X4,X3) )
=> ( get(X0,int,X1,t2tb1(X4)) = get(X0,int,X2,t2tb1(X4)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq_prefix_def) ).
tff(f66,axiom,
! [X0: map_int_int] : ( tb2t2(t2tb2(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL2) ).
tff(f67,axiom,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR2) ).
tff(f76,conjecture,
! [X0: $int,X1: $int,X2: map_int_lpmap_int_intrp,X3: $int,X4: map_int_int] :
( ( $lesseq(0,X0)
& ( X0 = n1 )
& ( X1 = 0 )
& ( X3 = 0 ) )
=> ( ( $lesseq(0,X3)
& ( $sum(X3,cardinal1(int,t2tb(below1(X0)))) = n1 )
& $lesseq(0,X1)
& ! [X5: $int] :
( mem(int,t2tb1(X5),t2tb(below1(X0)))
<=> ( $lesseq(0,X5)
& $less(X5,n1)
& ! [X6: $int] :
( ( $lesseq(0,X6)
& $less(X6,X3) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != X5 ) ) ) )
& ! [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,X6),X3) ) ) ) )
& ! [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) )
=> ! [X7: $int,X8: map_int_lpmap_int_intrp,X9: $int,X10: map_int_int] :
( ( $lesseq(0,$difference(X7,X1))
& ( X9 = X3 )
& sorted1(X8,X1,X7)
& ! [X11: map_int_int] :
( ( partial_solution1(n1,X11)
& eq_prefix1(int,t2tb2(X10),t2tb2(X11),X9) )
<=> ? [X5: $int] :
( $lesseq(X1,X5)
& $less(X5,X7)
& eq_prefix1(int,t2tb2(X11),get(map(int,int),int,t2tb3(X8),t2tb1(X5)),n1) ) )
& eq_prefix1(int,t2tb2(X4),t2tb2(X10),X9)
& eq_prefix1(map(int,int),t2tb3(X2),t2tb3(X8),X1) )
=> ( ( $difference(X7,X1) = X7 )
& sorted1(X8,0,X7)
& ! [X11: map_int_int] :
( partial_solution1(n1,X11)
<=> ? [X5: $int] :
( $lesseq(0,X5)
& $less(X5,$difference(X7,X1))
& eq_prefix1(int,t2tb2(X11),get(map(int,int),int,t2tb3(X8),t2tb1(X5)),n1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_queens3) ).
tff(f77,negated_conjecture,
~ ! [X0: $int,X1: $int,X2: map_int_lpmap_int_intrp,X3: $int,X4: map_int_int] :
( ( $lesseq(0,X0)
& ( X0 = n1 )
& ( X1 = 0 )
& ( X3 = 0 ) )
=> ( ( $lesseq(0,X3)
& ( $sum(X3,cardinal1(int,t2tb(below1(X0)))) = n1 )
& $lesseq(0,X1)
& ! [X5: $int] :
( mem(int,t2tb1(X5),t2tb(below1(X0)))
<=> ( $lesseq(0,X5)
& $less(X5,n1)
& ! [X6: $int] :
( ( $lesseq(0,X6)
& $less(X6,X3) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != X5 ) ) ) )
& ! [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,X6),X3) ) ) ) )
& ! [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) )
=> ! [X7: $int,X8: map_int_lpmap_int_intrp,X9: $int,X10: map_int_int] :
( ( $lesseq(0,$difference(X7,X1))
& ( X9 = X3 )
& sorted1(X8,X1,X7)
& ! [X11: map_int_int] :
( ( partial_solution1(n1,X11)
& eq_prefix1(int,t2tb2(X10),t2tb2(X11),X9) )
<=> ? [X5: $int] :
( $lesseq(X1,X5)
& $less(X5,X7)
& eq_prefix1(int,t2tb2(X11),get(map(int,int),int,t2tb3(X8),t2tb1(X5)),n1) ) )
& eq_prefix1(int,t2tb2(X4),t2tb2(X10),X9)
& eq_prefix1(map(int,int),t2tb3(X2),t2tb3(X8),X1) )
=> ( ( $difference(X7,X1) = X7 )
& sorted1(X8,0,X7)
& ! [X11: map_int_int] :
( partial_solution1(n1,X11)
<=> ? [X5: $int] :
( $lesseq(0,X5)
& $less(X5,$difference(X7,X1))
& eq_prefix1(int,t2tb2(X11),get(map(int,int),int,t2tb3(X8),t2tb1(X5)),n1) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f76]) ).
tff(f87,plain,
! [X0: ty,X1: uni,X2: uni,X3: $int] :
( eq_prefix1(X0,X1,X2,X3)
<=> ! [X4: $int] :
( ( ~ $less(X4,0)
& $less(X4,X3) )
=> ( get(X0,int,X1,t2tb1(X4)) = get(X0,int,X2,t2tb1(X4)) ) ) ),
inference(theory_normalization,[],[f64]) ).
tff(f92,plain,
~ ! [X0: $int,X1: $int,X2: map_int_lpmap_int_intrp,X3: $int,X4: map_int_int] :
( ( ~ $less(X0,0)
& ( X0 = n1 )
& ( X1 = 0 )
& ( X3 = 0 ) )
=> ( ( ~ $less(X3,0)
& ( $sum(X3,cardinal1(int,t2tb(below1(X0)))) = n1 )
& ~ $less(X1,0)
& ! [X5: $int] :
( mem(int,t2tb1(X5),t2tb(below1(X0)))
<=> ( ~ $less(X5,0)
& $less(X5,n1)
& ! [X6: $int] :
( ( ~ $less(X6,0)
& $less(X6,X3) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != X5 ) ) ) )
& ! [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,X6),$uminus(X3)) ) ) ) )
& ! [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) )
=> ! [X7: $int,X8: map_int_lpmap_int_intrp,X9: $int,X10: map_int_int] :
( ( ~ $less($sum(X7,$uminus(X1)),0)
& ( X9 = X3 )
& sorted1(X8,X1,X7)
& ! [X11: map_int_int] :
( ( partial_solution1(n1,X11)
& eq_prefix1(int,t2tb2(X10),t2tb2(X11),X9) )
<=> ? [X5: $int] :
( ~ $less(X5,X1)
& $less(X5,X7)
& eq_prefix1(int,t2tb2(X11),get(map(int,int),int,t2tb3(X8),t2tb1(X5)),n1) ) )
& eq_prefix1(int,t2tb2(X4),t2tb2(X10),X9)
& eq_prefix1(map(int,int),t2tb3(X2),t2tb3(X8),X1) )
=> ( ( $sum(X7,$uminus(X1)) = X7 )
& sorted1(X8,0,X7)
& ! [X11: map_int_int] :
( partial_solution1(n1,X11)
<=> ? [X5: $int] :
( ~ $less(X5,0)
& $less(X5,$sum(X7,$uminus(X1)))
& eq_prefix1(int,t2tb2(X11),get(map(int,int),int,t2tb3(X8),t2tb1(X5)),n1) ) ) ) ) ) ),
inference(theory_normalization,[],[f77]) ).
tff(f116,plain,
~ ! [X0: $int,X1: $int,X2: map_int_lpmap_int_intrp,X3: $int,X4: map_int_int] :
( ( ~ $less(X0,0)
& ( X0 = n1 )
& ( X1 = 0 )
& ( X3 = 0 ) )
=> ( ( ~ $less(X3,0)
& ( $sum(X3,cardinal1(int,t2tb(below1(X0)))) = n1 )
& ~ $less(X1,0)
& ! [X5: $int] :
( mem(int,t2tb1(X5),t2tb(below1(X0)))
<=> ( ~ $less(X5,0)
& $less(X5,n1)
& ! [X6: $int] :
( ( ~ $less(X6,0)
& $less(X6,X3) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != X5 ) ) ) )
& ! [X7: $int] :
( ~ $less(X7,0)
=> ( ~ mem(int,t2tb1(X7),empty(int))
<=> ! [X8: $int] :
( ( ~ $less(X8,0)
& $less(X8,X3) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X3)) ) ) ) )
& ! [X9: $int] :
( ~ $less(X9,0)
=> ( ~ mem(int,t2tb1(X9),empty(int))
<=> ! [X10: $int] :
( ( ~ $less(X10,0)
& $less(X10,X3) )
=> ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X10))) != $sum($sum(X9,X3),$uminus(X10)) ) ) ) )
& partial_solution1(X3,X4) )
=> ! [X11: $int,X12: map_int_lpmap_int_intrp,X13: $int,X14: map_int_int] :
( ( ~ $less($sum(X11,$uminus(X1)),0)
& ( X3 = X13 )
& sorted1(X12,X1,X11)
& ! [X15: map_int_int] :
( ( partial_solution1(n1,X15)
& eq_prefix1(int,t2tb2(X14),t2tb2(X15),X13) )
<=> ? [X16: $int] :
( ~ $less(X16,X1)
& $less(X16,X11)
& eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X12),t2tb1(X16)),n1) ) )
& eq_prefix1(int,t2tb2(X4),t2tb2(X14),X13)
& eq_prefix1(map(int,int),t2tb3(X2),t2tb3(X12),X1) )
=> ( ( $sum(X11,$uminus(X1)) = X11 )
& sorted1(X12,0,X11)
& ! [X17: map_int_int] :
( partial_solution1(n1,X17)
<=> ? [X18: $int] :
( ~ $less(X18,0)
& $less(X18,$sum(X11,$uminus(X1)))
& eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X12),t2tb1(X18)),n1) ) ) ) ) ) ),
inference(rectify,[],[f92]) ).
tff(f153,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,0)
| ~ $less(X4,X3) ) ),
inference(ennf_transformation,[],[f87]) ).
tff(f154,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,0)
| ~ $less(X4,X3) ) ),
inference(flattening,[],[f153]) ).
tff(f163,plain,
? [X0: $int,X1: $int,X2: map_int_lpmap_int_intrp,X3: $int,X4: map_int_int] :
( ? [X11: $int,X12: map_int_lpmap_int_intrp,X13: $int,X14: map_int_int] :
( ( ( $sum(X11,$uminus(X1)) != X11 )
| ~ sorted1(X12,0,X11)
| ? [X17: map_int_int] :
( partial_solution1(n1,X17)
<~> ? [X18: $int] :
( ~ $less(X18,0)
& $less(X18,$sum(X11,$uminus(X1)))
& eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X12),t2tb1(X18)),n1) ) ) )
& ~ $less($sum(X11,$uminus(X1)),0)
& ( X3 = X13 )
& sorted1(X12,X1,X11)
& ! [X15: map_int_int] :
( ( partial_solution1(n1,X15)
& eq_prefix1(int,t2tb2(X14),t2tb2(X15),X13) )
<=> ? [X16: $int] :
( ~ $less(X16,X1)
& $less(X16,X11)
& eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X12),t2tb1(X16)),n1) ) )
& eq_prefix1(int,t2tb2(X4),t2tb2(X14),X13)
& eq_prefix1(map(int,int),t2tb3(X2),t2tb3(X12),X1) )
& ~ $less(X3,0)
& ( $sum(X3,cardinal1(int,t2tb(below1(X0)))) = n1 )
& ~ $less(X1,0)
& ! [X5: $int] :
( mem(int,t2tb1(X5),t2tb(below1(X0)))
<=> ( ~ $less(X5,0)
& $less(X5,n1)
& ! [X6: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != X5 )
| $less(X6,0)
| ~ $less(X6,X3) ) ) )
& ! [X7: $int] :
( ( ~ mem(int,t2tb1(X7),empty(int))
<=> ! [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X3)) )
| $less(X8,0)
| ~ $less(X8,X3) ) )
| $less(X7,0) )
& ! [X9: $int] :
( ( ~ mem(int,t2tb1(X9),empty(int))
<=> ! [X10: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X10))) != $sum($sum(X9,X3),$uminus(X10)) )
| $less(X10,0)
| ~ $less(X10,X3) ) )
| $less(X9,0) )
& partial_solution1(X3,X4)
& ~ $less(X0,0)
& ( X0 = n1 )
& ( X1 = 0 )
& ( X3 = 0 ) ),
inference(ennf_transformation,[],[f116]) ).
tff(f164,plain,
? [X0: $int,X1: $int,X2: map_int_lpmap_int_intrp,X3: $int,X4: map_int_int] :
( ? [X11: $int,X12: map_int_lpmap_int_intrp,X13: $int,X14: map_int_int] :
( ( ( $sum(X11,$uminus(X1)) != X11 )
| ~ sorted1(X12,0,X11)
| ? [X17: map_int_int] :
( partial_solution1(n1,X17)
<~> ? [X18: $int] :
( ~ $less(X18,0)
& $less(X18,$sum(X11,$uminus(X1)))
& eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X12),t2tb1(X18)),n1) ) ) )
& ~ $less($sum(X11,$uminus(X1)),0)
& ( X3 = X13 )
& sorted1(X12,X1,X11)
& ! [X15: map_int_int] :
( ( partial_solution1(n1,X15)
& eq_prefix1(int,t2tb2(X14),t2tb2(X15),X13) )
<=> ? [X16: $int] :
( ~ $less(X16,X1)
& $less(X16,X11)
& eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X12),t2tb1(X16)),n1) ) )
& eq_prefix1(int,t2tb2(X4),t2tb2(X14),X13)
& eq_prefix1(map(int,int),t2tb3(X2),t2tb3(X12),X1) )
& ~ $less(X3,0)
& ( $sum(X3,cardinal1(int,t2tb(below1(X0)))) = n1 )
& ~ $less(X1,0)
& ! [X5: $int] :
( mem(int,t2tb1(X5),t2tb(below1(X0)))
<=> ( ~ $less(X5,0)
& $less(X5,n1)
& ! [X6: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != X5 )
| $less(X6,0)
| ~ $less(X6,X3) ) ) )
& ! [X7: $int] :
( ( ~ mem(int,t2tb1(X7),empty(int))
<=> ! [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X3)) )
| $less(X8,0)
| ~ $less(X8,X3) ) )
| $less(X7,0) )
& ! [X9: $int] :
( ( ~ mem(int,t2tb1(X9),empty(int))
<=> ! [X10: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X10))) != $sum($sum(X9,X3),$uminus(X10)) )
| $less(X10,0)
| ~ $less(X10,X3) ) )
| $less(X9,0) )
& partial_solution1(X3,X4)
& ~ $less(X0,0)
& ( X0 = n1 )
& ( X1 = 0 )
& ( X3 = 0 ) ),
inference(flattening,[],[f163]) ).
tff(f189,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,0)
& $less(X4,X3) ) )
& ( ! [X4: $int] :
( ( get(X0,int,X1,t2tb1(X4)) = get(X0,int,X2,t2tb1(X4)) )
| $less(X4,0)
| ~ $less(X4,X3) )
| ~ eq_prefix1(X0,X1,X2,X3) ) ),
inference(nnf_transformation,[],[f154]) ).
tff(f190,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,0)
& $less(X4,X3) ) )
& ( ! [X5: $int] :
( ( get(X0,int,X1,t2tb1(X5)) = get(X0,int,X2,t2tb1(X5)) )
| $less(X5,0)
| ~ $less(X5,X3) )
| ~ eq_prefix1(X0,X1,X2,X3) ) ),
inference(rectify,[],[f189]) ).
tff(f191,plain,
! [X0: ty,X1: uni,X2: uni,X3: $int] :
( ( eq_prefix1(X0,X1,X2,X3)
| ( ( get(X0,int,X1,t2tb1(sK4(X0,X1,X2,X3))) != get(X0,int,X2,t2tb1(sK4(X0,X1,X2,X3))) )
& ~ $less(sK4(X0,X1,X2,X3),0)
& $less(sK4(X0,X1,X2,X3),X3) ) )
& ( ! [X5: $int] :
( ( get(X0,int,X1,t2tb1(X5)) = get(X0,int,X2,t2tb1(X5)) )
| $less(X5,0)
| ~ $less(X5,X3) )
| ~ eq_prefix1(X0,X1,X2,X3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X4,sK4(X0,X1,X2,X3))],[f190]) ).
tff(f202,plain,
? [X0: $int,X1: $int,X2: map_int_lpmap_int_intrp,X3: $int,X4: map_int_int] :
( ? [X11: $int,X12: map_int_lpmap_int_intrp,X13: $int,X14: map_int_int] :
( ( ( $sum(X11,$uminus(X1)) != X11 )
| ~ sorted1(X12,0,X11)
| ? [X17: map_int_int] :
( ( ! [X18: $int] :
( $less(X18,0)
| ~ $less(X18,$sum(X11,$uminus(X1)))
| ~ eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X12),t2tb1(X18)),n1) )
| ~ partial_solution1(n1,X17) )
& ( ? [X18: $int] :
( ~ $less(X18,0)
& $less(X18,$sum(X11,$uminus(X1)))
& eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X12),t2tb1(X18)),n1) )
| partial_solution1(n1,X17) ) ) )
& ~ $less($sum(X11,$uminus(X1)),0)
& ( X3 = X13 )
& sorted1(X12,X1,X11)
& ! [X15: map_int_int] :
( ( ( partial_solution1(n1,X15)
& eq_prefix1(int,t2tb2(X14),t2tb2(X15),X13) )
| ! [X16: $int] :
( $less(X16,X1)
| ~ $less(X16,X11)
| ~ eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X12),t2tb1(X16)),n1) ) )
& ( ? [X16: $int] :
( ~ $less(X16,X1)
& $less(X16,X11)
& eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X12),t2tb1(X16)),n1) )
| ~ partial_solution1(n1,X15)
| ~ eq_prefix1(int,t2tb2(X14),t2tb2(X15),X13) ) )
& eq_prefix1(int,t2tb2(X4),t2tb2(X14),X13)
& eq_prefix1(map(int,int),t2tb3(X2),t2tb3(X12),X1) )
& ~ $less(X3,0)
& ( $sum(X3,cardinal1(int,t2tb(below1(X0)))) = n1 )
& ~ $less(X1,0)
& ! [X5: $int] :
( ( mem(int,t2tb1(X5),t2tb(below1(X0)))
| $less(X5,0)
| ~ $less(X5,n1)
| ? [X6: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) = X5 )
& ~ $less(X6,0)
& $less(X6,X3) ) )
& ( ( ~ $less(X5,0)
& $less(X5,n1)
& ! [X6: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != X5 )
| $less(X6,0)
| ~ $less(X6,X3) ) )
| ~ mem(int,t2tb1(X5),t2tb(below1(X0))) ) )
& ! [X7: $int] :
( ( ( ~ mem(int,t2tb1(X7),empty(int))
| ? [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X8))) = $sum($sum(X7,X8),$uminus(X3)) )
& ~ $less(X8,0)
& $less(X8,X3) ) )
& ( ! [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X3)) )
| $less(X8,0)
| ~ $less(X8,X3) )
| mem(int,t2tb1(X7),empty(int)) ) )
| $less(X7,0) )
& ! [X9: $int] :
( ( ( ~ mem(int,t2tb1(X9),empty(int))
| ? [X10: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X10))) = $sum($sum(X9,X3),$uminus(X10)) )
& ~ $less(X10,0)
& $less(X10,X3) ) )
& ( ! [X10: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X10))) != $sum($sum(X9,X3),$uminus(X10)) )
| $less(X10,0)
| ~ $less(X10,X3) )
| mem(int,t2tb1(X9),empty(int)) ) )
| $less(X9,0) )
& partial_solution1(X3,X4)
& ~ $less(X0,0)
& ( X0 = n1 )
& ( X1 = 0 )
& ( X3 = 0 ) ),
inference(nnf_transformation,[],[f164]) ).
tff(f203,plain,
? [X0: $int,X1: $int,X2: map_int_lpmap_int_intrp,X3: $int,X4: map_int_int] :
( ? [X11: $int,X12: map_int_lpmap_int_intrp,X13: $int,X14: map_int_int] :
( ( ( $sum(X11,$uminus(X1)) != X11 )
| ~ sorted1(X12,0,X11)
| ? [X17: map_int_int] :
( ( ! [X18: $int] :
( $less(X18,0)
| ~ $less(X18,$sum(X11,$uminus(X1)))
| ~ eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X12),t2tb1(X18)),n1) )
| ~ partial_solution1(n1,X17) )
& ( ? [X18: $int] :
( ~ $less(X18,0)
& $less(X18,$sum(X11,$uminus(X1)))
& eq_prefix1(int,t2tb2(X17),get(map(int,int),int,t2tb3(X12),t2tb1(X18)),n1) )
| partial_solution1(n1,X17) ) ) )
& ~ $less($sum(X11,$uminus(X1)),0)
& ( X3 = X13 )
& sorted1(X12,X1,X11)
& ! [X15: map_int_int] :
( ( ( partial_solution1(n1,X15)
& eq_prefix1(int,t2tb2(X14),t2tb2(X15),X13) )
| ! [X16: $int] :
( $less(X16,X1)
| ~ $less(X16,X11)
| ~ eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X12),t2tb1(X16)),n1) ) )
& ( ? [X16: $int] :
( ~ $less(X16,X1)
& $less(X16,X11)
& eq_prefix1(int,t2tb2(X15),get(map(int,int),int,t2tb3(X12),t2tb1(X16)),n1) )
| ~ partial_solution1(n1,X15)
| ~ eq_prefix1(int,t2tb2(X14),t2tb2(X15),X13) ) )
& eq_prefix1(int,t2tb2(X4),t2tb2(X14),X13)
& eq_prefix1(map(int,int),t2tb3(X2),t2tb3(X12),X1) )
& ~ $less(X3,0)
& ( $sum(X3,cardinal1(int,t2tb(below1(X0)))) = n1 )
& ~ $less(X1,0)
& ! [X5: $int] :
( ( mem(int,t2tb1(X5),t2tb(below1(X0)))
| $less(X5,0)
| ~ $less(X5,n1)
| ? [X6: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) = X5 )
& ~ $less(X6,0)
& $less(X6,X3) ) )
& ( ( ~ $less(X5,0)
& $less(X5,n1)
& ! [X6: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X6))) != X5 )
| $less(X6,0)
| ~ $less(X6,X3) ) )
| ~ mem(int,t2tb1(X5),t2tb(below1(X0))) ) )
& ! [X7: $int] :
( ( ( ~ mem(int,t2tb1(X7),empty(int))
| ? [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X8))) = $sum($sum(X7,X8),$uminus(X3)) )
& ~ $less(X8,0)
& $less(X8,X3) ) )
& ( ! [X8: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X8))) != $sum($sum(X7,X8),$uminus(X3)) )
| $less(X8,0)
| ~ $less(X8,X3) )
| mem(int,t2tb1(X7),empty(int)) ) )
| $less(X7,0) )
& ! [X9: $int] :
( ( ( ~ mem(int,t2tb1(X9),empty(int))
| ? [X10: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X10))) = $sum($sum(X9,X3),$uminus(X10)) )
& ~ $less(X10,0)
& $less(X10,X3) ) )
& ( ! [X10: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X10))) != $sum($sum(X9,X3),$uminus(X10)) )
| $less(X10,0)
| ~ $less(X10,X3) )
| mem(int,t2tb1(X9),empty(int)) ) )
| $less(X9,0) )
& partial_solution1(X3,X4)
& ~ $less(X0,0)
& ( X0 = n1 )
& ( X1 = 0 )
& ( X3 = 0 ) ),
inference(flattening,[],[f202]) ).
tff(f204,plain,
? [X0: $int,X1: $int,X2: map_int_lpmap_int_intrp,X3: $int,X4: map_int_int] :
( ? [X5: $int,X6: map_int_lpmap_int_intrp,X7: $int,X8: map_int_int] :
( ( ( $sum(X5,$uminus(X1)) != X5 )
| ~ sorted1(X6,0,X5)
| ? [X9: map_int_int] :
( ( ! [X10: $int] :
( $less(X10,0)
| ~ $less(X10,$sum(X5,$uminus(X1)))
| ~ eq_prefix1(int,t2tb2(X9),get(map(int,int),int,t2tb3(X6),t2tb1(X10)),n1) )
| ~ partial_solution1(n1,X9) )
& ( ? [X11: $int] :
( ~ $less(X11,0)
& $less(X11,$sum(X5,$uminus(X1)))
& eq_prefix1(int,t2tb2(X9),get(map(int,int),int,t2tb3(X6),t2tb1(X11)),n1) )
| partial_solution1(n1,X9) ) ) )
& ~ $less($sum(X5,$uminus(X1)),0)
& ( X3 = X7 )
& sorted1(X6,X1,X5)
& ! [X12: map_int_int] :
( ( ( partial_solution1(n1,X12)
& eq_prefix1(int,t2tb2(X8),t2tb2(X12),X7) )
| ! [X13: $int] :
( $less(X13,X1)
| ~ $less(X13,X5)
| ~ eq_prefix1(int,t2tb2(X12),get(map(int,int),int,t2tb3(X6),t2tb1(X13)),n1) ) )
& ( ? [X14: $int] :
( ~ $less(X14,X1)
& $less(X14,X5)
& eq_prefix1(int,t2tb2(X12),get(map(int,int),int,t2tb3(X6),t2tb1(X14)),n1) )
| ~ partial_solution1(n1,X12)
| ~ eq_prefix1(int,t2tb2(X8),t2tb2(X12),X7) ) )
& eq_prefix1(int,t2tb2(X4),t2tb2(X8),X7)
& eq_prefix1(map(int,int),t2tb3(X2),t2tb3(X6),X1) )
& ~ $less(X3,0)
& ( $sum(X3,cardinal1(int,t2tb(below1(X0)))) = n1 )
& ~ $less(X1,0)
& ! [X15: $int] :
( ( mem(int,t2tb1(X15),t2tb(below1(X0)))
| $less(X15,0)
| ~ $less(X15,n1)
| ? [X16: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X16))) = X15 )
& ~ $less(X16,0)
& $less(X16,X3) ) )
& ( ( ~ $less(X15,0)
& $less(X15,n1)
& ! [X17: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X17))) != X15 )
| $less(X17,0)
| ~ $less(X17,X3) ) )
| ~ mem(int,t2tb1(X15),t2tb(below1(X0))) ) )
& ! [X18: $int] :
( ( ( ~ mem(int,t2tb1(X18),empty(int))
| ? [X19: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X19))) = $sum($sum(X18,X19),$uminus(X3)) )
& ~ $less(X19,0)
& $less(X19,X3) ) )
& ( ! [X20: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X20))) != $sum($sum(X18,X20),$uminus(X3)) )
| $less(X20,0)
| ~ $less(X20,X3) )
| mem(int,t2tb1(X18),empty(int)) ) )
| $less(X18,0) )
& ! [X21: $int] :
( ( ( ~ mem(int,t2tb1(X21),empty(int))
| ? [X22: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X22))) = $sum($sum(X21,X3),$uminus(X22)) )
& ~ $less(X22,0)
& $less(X22,X3) ) )
& ( ! [X23: $int] :
( ( tb2t1(get(int,int,t2tb2(X4),t2tb1(X23))) != $sum($sum(X21,X3),$uminus(X23)) )
| $less(X23,0)
| ~ $less(X23,X3) )
| mem(int,t2tb1(X21),empty(int)) ) )
| $less(X21,0) )
& partial_solution1(X3,X4)
& ~ $less(X0,0)
& ( X0 = n1 )
& ( X1 = 0 )
& ( X3 = 0 ) ),
inference(rectify,[],[f203]) ).
tff(f205,plain,
( ( ( sK15 != $sum(sK15,$uminus(sK11)) )
| ~ sorted1(sK16,0,sK15)
| ( ( ! [X10: $int] :
( $less(X10,0)
| ~ $less(X10,$sum(sK15,$uminus(sK11)))
| ~ eq_prefix1(int,t2tb2(sK19),get(map(int,int),int,t2tb3(sK16),t2tb1(X10)),n1) )
| ~ partial_solution1(n1,sK19) )
& ( ( ~ $less(sK20,0)
& $less(sK20,$sum(sK15,$uminus(sK11)))
& eq_prefix1(int,t2tb2(sK19),get(map(int,int),int,t2tb3(sK16),t2tb1(sK20)),n1) )
| partial_solution1(n1,sK19) ) ) )
& ~ $less($sum(sK15,$uminus(sK11)),0)
& ( sK13 = sK17 )
& sorted1(sK16,sK11,sK15)
& ! [X12: map_int_int] :
( ( ( partial_solution1(n1,X12)
& eq_prefix1(int,t2tb2(sK18),t2tb2(X12),sK17) )
| ! [X13: $int] :
( $less(X13,sK11)
| ~ $less(X13,sK15)
| ~ eq_prefix1(int,t2tb2(X12),get(map(int,int),int,t2tb3(sK16),t2tb1(X13)),n1) ) )
& ( ( ~ $less(sK21(X12),sK11)
& $less(sK21(X12),sK15)
& eq_prefix1(int,t2tb2(X12),get(map(int,int),int,t2tb3(sK16),t2tb1(sK21(X12))),n1) )
| ~ partial_solution1(n1,X12)
| ~ eq_prefix1(int,t2tb2(sK18),t2tb2(X12),sK17) ) )
& eq_prefix1(int,t2tb2(sK14),t2tb2(sK18),sK17)
& eq_prefix1(map(int,int),t2tb3(sK12),t2tb3(sK16),sK11)
& ~ $less(sK13,0)
& ( n1 = $sum(sK13,cardinal1(int,t2tb(below1(sK10)))) )
& ~ $less(sK11,0)
& ! [X15: $int] :
( ( mem(int,t2tb1(X15),t2tb(below1(sK10)))
| $less(X15,0)
| ~ $less(X15,n1)
| ( ( tb2t1(get(int,int,t2tb2(sK14),t2tb1(sK22(X15)))) = X15 )
& ~ $less(sK22(X15),0)
& $less(sK22(X15),sK13) ) )
& ( ( ~ $less(X15,0)
& $less(X15,n1)
& ! [X17: $int] :
( ( tb2t1(get(int,int,t2tb2(sK14),t2tb1(X17))) != X15 )
| $less(X17,0)
| ~ $less(X17,sK13) ) )
| ~ mem(int,t2tb1(X15),t2tb(below1(sK10))) ) )
& ! [X18: $int] :
( ( ( ~ mem(int,t2tb1(X18),empty(int))
| ( ( tb2t1(get(int,int,t2tb2(sK14),t2tb1(sK23(X18)))) = $sum($sum(X18,sK23(X18)),$uminus(sK13)) )
& ~ $less(sK23(X18),0)
& $less(sK23(X18),sK13) ) )
& ( ! [X20: $int] :
( ( tb2t1(get(int,int,t2tb2(sK14),t2tb1(X20))) != $sum($sum(X18,X20),$uminus(sK13)) )
| $less(X20,0)
| ~ $less(X20,sK13) )
| mem(int,t2tb1(X18),empty(int)) ) )
| $less(X18,0) )
& ! [X21: $int] :
( ( ( ~ mem(int,t2tb1(X21),empty(int))
| ( ( tb2t1(get(int,int,t2tb2(sK14),t2tb1(sK24(X21)))) = $sum($sum(X21,sK13),$uminus(sK24(X21))) )
& ~ $less(sK24(X21),0)
& $less(sK24(X21),sK13) ) )
& ( ! [X23: $int] :
( ( tb2t1(get(int,int,t2tb2(sK14),t2tb1(X23))) != $sum($sum(X21,sK13),$uminus(X23)) )
| $less(X23,0)
| ~ $less(X23,sK13) )
| mem(int,t2tb1(X21),empty(int)) ) )
| $less(X21,0) )
& partial_solution1(sK13,sK14)
& ~ $less(sK10,0)
& ( n1 = sK10 )
& ( 0 = sK11 )
& ( 0 = sK13 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24]),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(X11,sK20),skolemize(X14,sK21(X12)),skolemize(X16,sK22(X15)),skolemize(X19,sK23(X18)),skolemize(X22,sK24(X21))],[f204]) ).
tff(f269,plain,
! [X0: $int] : ( tb2t1(t2tb1(X0)) = X0 ),
inference(cnf_transformation,[],[f44]) ).
tff(f270,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f45]) ).
tff(f297,plain,
! [X2: uni,X3: $int,X0: ty,X1: uni] :
( eq_prefix1(X0,X1,X2,X3)
| $less(sK4(X0,X1,X2,X3),X3) ),
inference(cnf_transformation,[],[f191]) ).
tff(f298,plain,
! [X2: uni,X3: $int,X0: ty,X1: uni] :
( ~ $less(sK4(X0,X1,X2,X3),0)
| eq_prefix1(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f191]) ).
tff(f301,plain,
! [X0: map_int_int] : ( tb2t2(t2tb2(X0)) = X0 ),
inference(cnf_transformation,[],[f66]) ).
tff(f302,plain,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
inference(cnf_transformation,[],[f67]) ).
tff(f330,plain,
0 = sK13,
inference(cnf_transformation,[],[f205]) ).
tff(f331,plain,
0 = sK11,
inference(cnf_transformation,[],[f205]) ).
tff(f332,plain,
n1 = sK10,
inference(cnf_transformation,[],[f205]) ).
tff(f354,plain,
! [X12: map_int_int] :
( eq_prefix1(int,t2tb2(X12),get(map(int,int),int,t2tb3(sK16),t2tb1(sK21(X12))),n1)
| ~ partial_solution1(n1,X12)
| ~ eq_prefix1(int,t2tb2(sK18),t2tb2(X12),sK17) ),
inference(cnf_transformation,[],[f205]) ).
tff(f355,plain,
! [X12: map_int_int] :
( $less(sK21(X12),sK15)
| ~ partial_solution1(n1,X12)
| ~ eq_prefix1(int,t2tb2(sK18),t2tb2(X12),sK17) ),
inference(cnf_transformation,[],[f205]) ).
tff(f356,plain,
! [X12: map_int_int] :
( ~ $less(sK21(X12),sK11)
| ~ partial_solution1(n1,X12)
| ~ eq_prefix1(int,t2tb2(sK18),t2tb2(X12),sK17) ),
inference(cnf_transformation,[],[f205]) ).
tff(f358,plain,
! [X12: map_int_int,X13: $int] :
( partial_solution1(n1,X12)
| $less(X13,sK11)
| ~ $less(X13,sK15)
| ~ eq_prefix1(int,t2tb2(X12),get(map(int,int),int,t2tb3(sK16),t2tb1(X13)),n1) ),
inference(cnf_transformation,[],[f205]) ).
tff(f359,plain,
sorted1(sK16,sK11,sK15),
inference(cnf_transformation,[],[f205]) ).
tff(f360,plain,
sK13 = sK17,
inference(cnf_transformation,[],[f205]) ).
tff(f362,plain,
( ( sK15 != $sum(sK15,$uminus(sK11)) )
| ~ sorted1(sK16,0,sK15)
| eq_prefix1(int,t2tb2(sK19),get(map(int,int),int,t2tb3(sK16),t2tb1(sK20)),n1)
| partial_solution1(n1,sK19) ),
inference(cnf_transformation,[],[f205]) ).
tff(f363,plain,
( ( sK15 != $sum(sK15,$uminus(sK11)) )
| ~ sorted1(sK16,0,sK15)
| $less(sK20,$sum(sK15,$uminus(sK11)))
| partial_solution1(n1,sK19) ),
inference(cnf_transformation,[],[f205]) ).
tff(f364,plain,
( ( sK15 != $sum(sK15,$uminus(sK11)) )
| ~ sorted1(sK16,0,sK15)
| ~ $less(sK20,0)
| partial_solution1(n1,sK19) ),
inference(cnf_transformation,[],[f205]) ).
tff(f365,plain,
! [X10: $int] :
( ( sK15 != $sum(sK15,$uminus(sK11)) )
| ~ sorted1(sK16,0,sK15)
| $less(X10,0)
| ~ $less(X10,$sum(sK15,$uminus(sK11)))
| ~ eq_prefix1(int,t2tb2(sK19),get(map(int,int),int,t2tb3(sK16),t2tb1(X10)),n1)
| ~ partial_solution1(n1,sK19) ),
inference(cnf_transformation,[],[f205]) ).
tff(f373,plain,
! [X10: $int] :
( ( sK15 != $sum(sK15,$uminus(0)) )
| ~ sorted1(sK16,0,sK15)
| $less(X10,0)
| ~ $less(X10,$sum(sK15,$uminus(0)))
| ~ eq_prefix1(int,t2tb2(sK19),get(map(int,int),int,t2tb3(sK16),t2tb1(X10)),sK10)
| ~ partial_solution1(sK10,sK19) ),
inference(definition_unfolding,[],[f365,f331,f331,f332,f332]) ).
tff(f374,plain,
( ( sK15 != $sum(sK15,$uminus(0)) )
| ~ sorted1(sK16,0,sK15)
| ~ $less(sK20,0)
| partial_solution1(sK10,sK19) ),
inference(definition_unfolding,[],[f364,f331,f332]) ).
tff(f375,plain,
( ( sK15 != $sum(sK15,$uminus(0)) )
| ~ sorted1(sK16,0,sK15)
| $less(sK20,$sum(sK15,$uminus(0)))
| partial_solution1(sK10,sK19) ),
inference(definition_unfolding,[],[f363,f331,f331,f332]) ).
tff(f376,plain,
( ( sK15 != $sum(sK15,$uminus(0)) )
| ~ sorted1(sK16,0,sK15)
| eq_prefix1(int,t2tb2(sK19),get(map(int,int),int,t2tb3(sK16),t2tb1(sK20)),sK10)
| partial_solution1(sK10,sK19) ),
inference(definition_unfolding,[],[f362,f331,f332,f332]) ).
tff(f378,plain,
sorted1(sK16,0,sK15),
inference(definition_unfolding,[],[f359,f331]) ).
tff(f379,plain,
! [X12: map_int_int,X13: $int] :
( ~ eq_prefix1(int,t2tb2(X12),get(map(int,int),int,t2tb3(sK16),t2tb1(X13)),sK10)
| $less(X13,0)
| ~ $less(X13,sK15)
| partial_solution1(sK10,X12) ),
inference(definition_unfolding,[],[f358,f332,f331,f332]) ).
tff(f381,plain,
! [X12: map_int_int] :
( ~ $less(sK21(X12),0)
| ~ partial_solution1(sK10,X12)
| ~ eq_prefix1(int,t2tb2(sK18),t2tb2(X12),sK17) ),
inference(definition_unfolding,[],[f356,f331,f332]) ).
tff(f382,plain,
! [X12: map_int_int] :
( $less(sK21(X12),sK15)
| ~ partial_solution1(sK10,X12)
| ~ eq_prefix1(int,t2tb2(sK18),t2tb2(X12),sK17) ),
inference(definition_unfolding,[],[f355,f332]) ).
tff(f383,plain,
! [X12: map_int_int] :
( eq_prefix1(int,t2tb2(X12),get(map(int,int),int,t2tb3(sK16),t2tb1(sK21(X12))),sK10)
| ~ partial_solution1(sK10,X12)
| ~ eq_prefix1(int,t2tb2(sK18),t2tb2(X12),sK17) ),
inference(definition_unfolding,[],[f354,f332,f332]) ).
tff(f400,plain,
0 = sK17,
inference(definition_unfolding,[],[f330,f360]) ).
tff(f407,plain,
( ~ sorted1(sK16,0,sK15)
| eq_prefix1(int,t2tb2(sK19),get(map(int,int),int,t2tb3(sK16),t2tb1(sK20)),sK10)
| partial_solution1(sK10,sK19) ),
inference(evaluation,[],[f376]) ).
tff(f408,plain,
( ~ sorted1(sK16,0,sK15)
| $less(sK20,sK15)
| partial_solution1(sK10,sK19) ),
inference(evaluation,[],[f375]) ).
tff(f409,plain,
( ~ sorted1(sK16,0,sK15)
| ~ $less(sK20,0)
| partial_solution1(sK10,sK19) ),
inference(evaluation,[],[f374]) ).
tff(f410,plain,
! [X10: $int] :
( ~ sorted1(sK16,0,sK15)
| $less(X10,0)
| ~ $less(X10,sK15)
| ~ eq_prefix1(int,t2tb2(sK19),get(map(int,int),int,t2tb3(sK16),t2tb1(X10)),sK10)
| ~ partial_solution1(sK10,sK19) ),
inference(evaluation,[],[f373]) ).
tff(f416,definition,
( spl25_1
<=> partial_solution1(sK10,sK19) ),
introduced(definition,[new_symbols(definition,[spl25_1])],[avatar_definition]) ).
tff(f417,plain,
( ~ partial_solution1(sK10,sK19)
| spl25_1 ),
inference(avatar_component_clause,[],[f416]) ).
tff(f420,definition,
( spl25_2
<=> eq_prefix1(int,t2tb2(sK19),get(map(int,int),int,t2tb3(sK16),t2tb1(sK20)),sK10) ),
introduced(definition,[new_symbols(definition,[spl25_2])],[avatar_definition]) ).
tff(f422,plain,
( eq_prefix1(int,t2tb2(sK19),get(map(int,int),int,t2tb3(sK16),t2tb1(sK20)),sK10)
| ~ spl25_2 ),
inference(avatar_component_clause,[],[f420]) ).
tff(f424,definition,
( spl25_3
<=> sorted1(sK16,0,sK15) ),
introduced(definition,[new_symbols(definition,[spl25_3])],[avatar_definition]) ).
tff(f427,plain,
( spl25_1
| spl25_2
| ~ spl25_3 ),
inference(avatar_split_clause,[],[f407,f424,f420,f416]) ).
tff(f429,definition,
( spl25_4
<=> $less(sK20,sK15) ),
introduced(definition,[new_symbols(definition,[spl25_4])],[avatar_definition]) ).
tff(f431,plain,
( $less(sK20,sK15)
| ~ spl25_4 ),
inference(avatar_component_clause,[],[f429]) ).
tff(f432,plain,
( spl25_1
| spl25_4
| ~ spl25_3 ),
inference(avatar_split_clause,[],[f408,f424,f429,f416]) ).
tff(f434,definition,
( spl25_5
<=> $less(sK20,0) ),
introduced(definition,[new_symbols(definition,[spl25_5])],[avatar_definition]) ).
tff(f436,plain,
( ~ $less(sK20,0)
| spl25_5 ),
inference(avatar_component_clause,[],[f434]) ).
tff(f437,plain,
( spl25_1
| ~ spl25_5
| ~ spl25_3 ),
inference(avatar_split_clause,[],[f409,f424,f434,f416]) ).
tff(f439,definition,
( spl25_6
<=> ! [X10: $int] :
( $less(X10,0)
| ~ eq_prefix1(int,t2tb2(sK19),get(map(int,int),int,t2tb3(sK16),t2tb1(X10)),sK10)
| ~ $less(X10,sK15) ) ),
introduced(definition,[new_symbols(definition,[spl25_6])],[avatar_definition]) ).
tff(f440,plain,
( ! [X10: $int] :
( ~ eq_prefix1(int,t2tb2(sK19),get(map(int,int),int,t2tb3(sK16),t2tb1(X10)),sK10)
| $less(X10,0)
| ~ $less(X10,sK15) )
| ~ spl25_6 ),
inference(avatar_component_clause,[],[f439]) ).
tff(f441,plain,
( ~ spl25_1
| spl25_6
| ~ spl25_3 ),
inference(avatar_split_clause,[],[f410,f424,f439,f416]) ).
tff(f444,plain,
spl25_3,
inference(avatar_split_clause,[],[f378,f424]) ).
tff(f450,plain,
! [X12: map_int_int] :
( ~ eq_prefix1(int,t2tb2(sK18),t2tb2(X12),0)
| ~ $less(sK21(X12),0)
| ~ partial_solution1(sK10,X12) ),
inference(forward_demodulation,[],[f381,f400]) ).
tff(f451,plain,
! [X12: map_int_int] :
( ~ eq_prefix1(int,t2tb2(sK18),t2tb2(X12),0)
| $less(sK21(X12),sK15)
| ~ partial_solution1(sK10,X12) ),
inference(forward_demodulation,[],[f382,f400]) ).
tff(f459,plain,
! [X12: map_int_int] :
( eq_prefix1(int,t2tb2(X12),get(map(int,int),int,t2tb3(sK16),t2tb1(sK21(X12))),sK10)
| ~ eq_prefix1(int,t2tb2(sK18),t2tb2(X12),0)
| ~ partial_solution1(sK10,X12) ),
inference(forward_demodulation,[],[f383,f400]) ).
tff(f472,definition,
( spl25_9
<=> eq_prefix1(int,t2tb2(sK18),t2tb2(sK19),0) ),
introduced(definition,[new_symbols(definition,[spl25_9])],[avatar_definition]) ).
tff(f474,plain,
( ~ eq_prefix1(int,t2tb2(sK18),t2tb2(sK19),0)
| spl25_9 ),
inference(avatar_component_clause,[],[f472]) ).
tff(f517,plain,
! [X0: uni,X1: $int] :
( ~ eq_prefix1(int,X0,get(map(int,int),int,t2tb3(sK16),t2tb1(X1)),sK10)
| $less(X1,0)
| ~ $less(X1,sK15)
| partial_solution1(sK10,tb2t2(X0)) ),
inference(superposition,[],[f379,f302]) ).
tff(f518,plain,
! [X0: uni] :
( ~ eq_prefix1(int,t2tb2(sK18),X0,0)
| ~ $less(sK21(tb2t2(X0)),0)
| ~ partial_solution1(sK10,tb2t2(X0)) ),
inference(superposition,[],[f450,f302]) ).
tff(f519,plain,
! [X0: uni] :
( ~ eq_prefix1(int,t2tb2(sK18),X0,0)
| $less(sK21(tb2t2(X0)),sK15)
| ~ partial_solution1(sK10,tb2t2(X0)) ),
inference(superposition,[],[f451,f302]) ).
tff(f520,plain,
! [X0: uni] :
( eq_prefix1(int,X0,get(map(int,int),int,t2tb3(sK16),t2tb1(sK21(tb2t2(X0)))),sK10)
| ~ eq_prefix1(int,t2tb2(sK18),X0,0)
| ~ partial_solution1(sK10,tb2t2(X0)) ),
inference(superposition,[],[f459,f302]) ).
tff(f539,plain,
! [X0: uni,X1: uni] :
( ~ eq_prefix1(int,X1,get(map(int,int),int,t2tb3(sK16),X0),sK10)
| $less(tb2t1(X0),0)
| ~ $less(tb2t1(X0),sK15)
| partial_solution1(sK10,tb2t2(X1)) ),
inference(superposition,[],[f517,f270]) ).
tff(f600,plain,
( ~ eq_prefix1(int,t2tb2(sK18),t2tb2(sK19),0)
| ~ partial_solution1(sK10,tb2t2(t2tb2(sK19)))
| $less(sK21(tb2t2(t2tb2(sK19))),0)
| ~ $less(sK21(tb2t2(t2tb2(sK19))),sK15)
| ~ spl25_6 ),
inference(resolution,[],[f520,f440]) ).
tff(f612,plain,
( ~ eq_prefix1(int,t2tb2(sK18),t2tb2(sK19),0)
| ~ partial_solution1(sK10,tb2t2(t2tb2(sK19)))
| ~ $less(sK21(tb2t2(t2tb2(sK19))),sK15)
| ~ spl25_6 ),
inference(forward_subsumption_resolution,[],[f600,f518]) ).
tff(f615,plain,
( ~ eq_prefix1(int,t2tb2(sK18),t2tb2(sK19),0)
| ~ partial_solution1(sK10,tb2t2(t2tb2(sK19)))
| ~ spl25_6 ),
inference(forward_subsumption_resolution,[],[f612,f519]) ).
tff(f618,plain,
( ~ partial_solution1(sK10,sK19)
| ~ eq_prefix1(int,t2tb2(sK18),t2tb2(sK19),0)
| ~ spl25_6 ),
inference(forward_demodulation,[],[f615,f301]) ).
tff(f1218,plain,
( $less(sK4(int,t2tb2(sK18),t2tb2(sK19),0),0)
| spl25_9 ),
inference(resolution,[],[f297,f474]) ).
tff(f1259,plain,
( eq_prefix1(int,t2tb2(sK18),t2tb2(sK19),0)
| spl25_9 ),
inference(resolution,[],[f298,f1218]) ).
tff(f1263,plain,
( $false
| spl25_9 ),
inference(forward_subsumption_resolution,[],[f1259,f474]) ).
tff(f1264,plain,
spl25_9,
inference(avatar_contradiction_clause,[],[f1263]) ).
tff(f1318,plain,
( ~ spl25_9
| ~ spl25_1
| ~ spl25_6 ),
inference(avatar_split_clause,[],[f618,f439,f416,f472]) ).
tff(f1349,plain,
( $less(tb2t1(t2tb1(sK20)),0)
| ~ $less(tb2t1(t2tb1(sK20)),sK15)
| partial_solution1(sK10,tb2t2(t2tb2(sK19)))
| ~ spl25_2 ),
inference(resolution,[],[f422,f539]) ).
tff(f1350,plain,
( $less(sK20,0)
| ~ $less(tb2t1(t2tb1(sK20)),sK15)
| partial_solution1(sK10,tb2t2(t2tb2(sK19)))
| ~ spl25_2 ),
inference(forward_demodulation,[],[f1349,f269]) ).
tff(f1359,plain,
( ~ $less(tb2t1(t2tb1(sK20)),sK15)
| partial_solution1(sK10,tb2t2(t2tb2(sK19)))
| ~ spl25_2
| spl25_5 ),
inference(forward_subsumption_resolution,[],[f1350,f436]) ).
tff(f1369,plain,
( ~ $less(sK20,sK15)
| partial_solution1(sK10,tb2t2(t2tb2(sK19)))
| ~ spl25_2
| spl25_5 ),
inference(forward_demodulation,[],[f1359,f269]) ).
tff(f1377,plain,
( partial_solution1(sK10,tb2t2(t2tb2(sK19)))
| ~ spl25_2
| ~ spl25_4
| spl25_5 ),
inference(forward_subsumption_resolution,[],[f1369,f431]) ).
tff(f1384,plain,
( partial_solution1(sK10,sK19)
| ~ spl25_2
| ~ spl25_4
| spl25_5 ),
inference(forward_demodulation,[],[f1377,f301]) ).
tff(f1387,plain,
( $false
| spl25_1
| ~ spl25_2
| ~ spl25_4
| spl25_5 ),
inference(forward_subsumption_resolution,[],[f1384,f417]) ).
tff(f1388,plain,
( spl25_1
| ~ spl25_2
| ~ spl25_4
| spl25_5 ),
inference(avatar_contradiction_clause,[],[f1387]) ).
cnf(s1,plain,
( spl25_1
| spl25_2
| ~ spl25_3 ),
inference(sat_conversion,[],[f427]) ).
cnf(s2,plain,
( spl25_1
| ~ spl25_3
| spl25_4 ),
inference(sat_conversion,[],[f432]) ).
cnf(s3,plain,
( spl25_1
| ~ spl25_3
| ~ spl25_5 ),
inference(sat_conversion,[],[f437]) ).
cnf(s4,plain,
( ~ spl25_1
| ~ spl25_3
| spl25_6 ),
inference(sat_conversion,[],[f441]) ).
cnf(s5,plain,
spl25_3,
inference(sat_conversion,[],[f444]) ).
cnf(s32,plain,
spl25_9,
inference(sat_conversion,[],[f1264]) ).
cnf(s40,plain,
( ~ spl25_1
| ~ spl25_6
| ~ spl25_9 ),
inference(sat_conversion,[],[f1318]) ).
cnf(s56,plain,
( spl25_1
| ~ spl25_2
| ~ spl25_4
| spl25_5 ),
inference(sat_conversion,[],[f1388]) ).
cnf(s59,plain,
( ~ spl25_1
| spl25_6 ),
inference(rat,[],[s4,s5]) ).
cnf(s60,plain,
( spl25_1
| ~ spl25_5 ),
inference(rat,[],[s3,s5]) ).
cnf(s61,plain,
( spl25_1
| spl25_4 ),
inference(rat,[],[s2,s5]) ).
cnf(s62,plain,
( spl25_1
| spl25_2 ),
inference(rat,[],[s1,s5]) ).
cnf(s63,plain,
spl25_1,
inference(rat,[],[s56,s62,s61,s60]) ).
cnf(s64,plain,
~ spl25_6,
inference(rat,[],[s40,s32,s63]) ).
cnf(s65,plain,
$false,
inference(rat,[],[s59,s64,s63]) ).
tff(f1389,plain,
$false,
inference(avatar_sat_refutation,[],[s65]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW634_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 % Computer : n004.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Mon Sep 28 14:23:22 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.27 Running first-order model finding
% 0.10/0.27 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.27/0.35 % (382489)Will run a generic schedule for satisfiability detection.
% 0.27/0.35 % (382498)dis+10_1_sil=32000:sp=arity:random_seed=50643645:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.27/0.35 % (382495)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2763647372_2999 on theBenchmark for (2999ds/0Mi)
% 0.27/0.35 % (382497)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2185211680:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.27/0.35 % (382501)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2396834497:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.27/0.35 % (382500)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3154172585:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.27/0.35 % (382496)% WARNING: option uhcvi not known.
% 0.27/0.35 % (382499)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=334194062:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.27/0.35 % (382495)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.27/0.35 % (382495)Terminated due to inappropriate strategy.
% 0.27/0.35 % (382495)------------------------------
% 0.27/0.35 % (382495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.27/0.35 % (382495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.27/0.35 % (382495)CaDiCaL version: 2.1.3
% 0.27/0.35 % (382495)Termination reason: Inappropriate
% 0.27/0.35 % (382495)Time elapsed: 0.010 s
% 0.27/0.35 % (382495)Peak memory usage: 11 MB
% 0.27/0.35 % (382495)Instructions burned: 12 (million)
% 0.27/0.35 % (382496)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=139617452:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.27/0.35 % (382495)------------------------------
% 0.27/0.35 % (382495)------------------------------
% 0.27/0.35 % (382498) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-382489-382498"...
% 0.27/0.35 % (382498)...printing done.
% 0.27/0.35 % (382498)Refutation found. Thanks to Tanya!
% 0.27/0.35 % SZS status Theorem for theBenchmark
% 0.27/0.35 % SZS output start Proof for theBenchmark
% See solution above
% 0.27/0.35 % (382498)------------------------------
% 0.27/0.35 % (382498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.27/0.35 % (382498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.27/0.35 % (382498)CaDiCaL version: 2.1.3
% 0.27/0.35 % (382498)Termination reason: Refutation
% 0.27/0.35 % (382498)Time elapsed: 0.035 s
% 0.27/0.35 % (382498)Peak memory usage: 13 MB
% 0.27/0.35 % (382498)Instructions burned: 70 (million)
% 0.27/0.35 % (382489)Success in time 0.069 s
% 0.27/0.35 % Vampire exiting
%------------------------------------------------------------------------------