%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW626_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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:33 PM UTC 2026
% Result : Theorem 7.82s 1.65s
% Output : Refutation 7.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 23
% Syntax : Number of formulae : 85 ( 59 unt; 0 typ; 17 def)
% Number of atoms : 338 ( 87 equ)
% Maximal formula atoms : 29 ( 3 avg)
% Number of connectives : 373 ( 120 ~; 39 |; 141 &)
% ( 0 <=>; 73 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number arithmetic : 293 ( 64 atm; 64 fun; 158 num; 7 var)
% Number of types : 8 ( 6 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 80 ( 74 usr; 43 con; 0-5 aty)
% Number of variables : 133 ( 115 !; 18 ?; 133 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
elt: $tType ).
tff(type_def_10,type,
list_elt: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
list: ty > ty ).
tff(func_def_13,type,
nil: ty > uni ).
tff(func_def_14,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_15,type,
match_list: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_16,type,
cons_proj_1: ( ty * uni ) > uni ).
tff(func_def_17,type,
cons_proj_2: ( ty * uni ) > uni ).
tff(func_def_18,type,
length: ( ty * uni ) > $int ).
tff(func_def_21,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_22,type,
num_occ: ( ty * uni * uni ) > $int ).
tff(func_def_23,type,
reverse: ( ty * uni ) > uni ).
tff(func_def_24,type,
elt1: ty ).
tff(func_def_25,type,
t2tb: list_elt > uni ).
tff(func_def_26,type,
tb2t: uni > list_elt ).
tff(func_def_27,type,
t2tb1: elt > uni ).
tff(func_def_28,type,
tb2t1: uni > elt ).
tff(func_def_29,type,
rev_append: ( ty * uni * uni ) > uni ).
tff(func_def_30,type,
prefix: ( ty * $int * uni ) > uni ).
tff(func_def_32,type,
abs: $int > $int ).
tff(func_def_34,type,
div: ( $int * $int ) > $int ).
tff(func_def_35,type,
mod: ( $int * $int ) > $int ).
tff(func_def_38,type,
sK0: ( ty * uni * uni ) > uni ).
tff(func_def_39,type,
sK1: ( ty * uni * uni ) > uni ).
tff(func_def_40,type,
sK2: ( ty * uni * uni ) > uni ).
tff(func_def_41,type,
sK3: list_elt > elt ).
tff(func_def_42,type,
sK4: list_elt > elt ).
tff(func_def_43,type,
sK5: list_elt > elt ).
tff(func_def_44,type,
sK6: list_elt > list_elt ).
tff(func_def_45,type,
sK7: ( elt * list_elt ) > elt ).
tff(func_def_46,type,
sK8: ( list_elt * list_elt ) > elt ).
tff(func_def_47,type,
sK9: ( list_elt * list_elt ) > elt ).
tff(func_def_48,type,
sK10: ( list_elt * elt ) > elt ).
tff(func_def_49,type,
sK11: ( list_elt * list_elt ) > elt ).
tff(func_def_50,type,
sK12: ( list_elt * list_elt ) > elt ).
tff(func_def_51,type,
sK13: $int ).
tff(func_def_52,type,
sK14: list_elt ).
tff(func_def_53,type,
sK15: list_elt ).
tff(func_def_54,type,
sK16: list_elt ).
tff(func_def_55,type,
sK17: list_elt ).
tff(func_def_56,type,
sK18: list_elt ).
tff(func_def_57,type,
sF19: uni ).
tff(func_def_58,type,
sF20: uni ).
tff(func_def_59,type,
sF21: uni ).
tff(func_def_60,type,
sF22: uni ).
tff(func_def_61,type,
sF23: list_elt ).
tff(func_def_62,type,
sF24: uni ).
tff(func_def_63,type,
sF25: uni ).
tff(func_def_64,type,
sF26: uni ).
tff(func_def_65,type,
sF27: uni ).
tff(func_def_66,type,
sF28: uni ).
tff(func_def_67,type,
sF29: uni ).
tff(func_def_68,type,
sF30: list_elt ).
tff(func_def_69,type,
sF31: $int ).
tff(func_def_70,type,
sF32: $int ).
tff(func_def_71,type,
sF33: $int ).
tff(func_def_72,type,
sF34: uni ).
tff(func_def_73,type,
sF35: uni ).
tff(func_def_74,type,
sF36: $int ).
tff(func_def_75,type,
sF37: uni ).
tff(func_def_76,type,
sF38: $int ).
tff(func_def_77,type,
sF39: list_elt ).
tff(func_def_78,type,
sF40: uni ).
tff(func_def_79,type,
sF41: list_elt ).
tff(func_def_80,type,
sF42: uni ).
tff(func_def_81,type,
sF43: list_elt ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_5,type,
permut: ( ty * uni * uni ) > $o ).
tff(pred_def_6,type,
le: ( elt * elt ) > $o ).
tff(pred_def_7,type,
sorted: list_elt > $o ).
tff(f24,axiom,
! [X0: ty,X1: uni] :
( ( infix_plpl(X0,nil(X0),X1) = X1 )
& ! [X2: uni,X3: uni] : ( infix_plpl(X0,cons(X0,X2,X3),X1) = cons(X0,X2,infix_plpl(X0,X3,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',infix_plpl_def) ).
tff(f44,axiom,
! [X0: ty,X1: uni,X2: uni] :
( permut(X0,X1,X2)
=> permut(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',permut_sym) ).
tff(f45,axiom,
! [X0: ty,X1: uni,X2: uni,X3: uni] :
( permut(X0,X1,X2)
=> ( permut(X0,X2,X3)
=> permut(X0,X1,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',permut_trans) ).
tff(f50,axiom,
! [X0: ty,X1: uni,X2: uni,X3: uni,X4: uni] :
( permut(X0,X1,X3)
=> ( permut(X0,X2,X4)
=> permut(X0,infix_plpl(X0,X1,X2),infix_plpl(X0,X3,X4)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',permut_append) ).
tff(f59,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f101,conjecture,
! [X0: $int,X1: list_elt] :
( ( $lesseq(2,X0)
& $lesseq(X0,length(elt1,t2tb(X1))) )
=> ( ( X0 != 2 )
=> ( ( X0 != 3 )
=> ( ( 2 != 0 )
=> ( ( $lesseq(0,div(X0,2))
& $lesseq(div(X0,2),length(elt1,t2tb(X1))) )
=> ! [X2: list_elt] :
( ( X1 = tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),t2tb(X2))) )
=> ( ( tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),prefix(elt1,$difference(X0,div(X0,2)),t2tb(X2)))) = tb2t(prefix(elt1,X0,t2tb(X1))) )
=> ( ( $lesseq(2,div(X0,2))
& $lesseq(div(X0,2),length(elt1,t2tb(X1))) )
=> ! [X3: list_elt] :
( ( sorted(X3)
& permut(elt1,t2tb(X3),prefix(elt1,div(X0,2),t2tb(X1))) )
=> ( ( $lesseq(2,$difference(X0,div(X0,2)))
& $lesseq($difference(X0,div(X0,2)),length(elt1,t2tb(X2))) )
=> ! [X4: list_elt] :
( ( sorted(X4)
& permut(elt1,t2tb(X4),prefix(elt1,$difference(X0,div(X0,2)),t2tb(X2))) )
=> ( ( sorted(tb2t(reverse(elt1,nil(elt1))))
& sorted(X3)
& sorted(X4)
& ! [X5: elt,X6: elt] :
( mem(elt1,t2tb1(X5),nil(elt1))
=> ( mem(elt1,t2tb1(X6),t2tb(X3))
=> le(X5,X6) ) )
& ! [X5: elt,X6: elt] :
( mem(elt1,t2tb1(X5),nil(elt1))
=> ( mem(elt1,t2tb1(X6),t2tb(X4))
=> le(X5,X6) ) ) )
=> ! [X7: list_elt] :
( ( sorted(tb2t(reverse(elt1,t2tb(X7))))
& permut(elt1,t2tb(X7),infix_plpl(elt1,infix_plpl(elt1,nil(elt1),t2tb(X3)),t2tb(X4))) )
=> permut(elt1,t2tb(X7),prefix(elt1,X0,t2tb(X1))) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_rev_sort) ).
tff(f102,negated_conjecture,
~ ! [X0: $int,X1: list_elt] :
( ( $lesseq(2,X0)
& $lesseq(X0,length(elt1,t2tb(X1))) )
=> ( ( X0 != 2 )
=> ( ( X0 != 3 )
=> ( ( 2 != 0 )
=> ( ( $lesseq(0,div(X0,2))
& $lesseq(div(X0,2),length(elt1,t2tb(X1))) )
=> ! [X2: list_elt] :
( ( X1 = tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),t2tb(X2))) )
=> ( ( tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),prefix(elt1,$difference(X0,div(X0,2)),t2tb(X2)))) = tb2t(prefix(elt1,X0,t2tb(X1))) )
=> ( ( $lesseq(2,div(X0,2))
& $lesseq(div(X0,2),length(elt1,t2tb(X1))) )
=> ! [X3: list_elt] :
( ( sorted(X3)
& permut(elt1,t2tb(X3),prefix(elt1,div(X0,2),t2tb(X1))) )
=> ( ( $lesseq(2,$difference(X0,div(X0,2)))
& $lesseq($difference(X0,div(X0,2)),length(elt1,t2tb(X2))) )
=> ! [X4: list_elt] :
( ( sorted(X4)
& permut(elt1,t2tb(X4),prefix(elt1,$difference(X0,div(X0,2)),t2tb(X2))) )
=> ( ( sorted(tb2t(reverse(elt1,nil(elt1))))
& sorted(X3)
& sorted(X4)
& ! [X5: elt,X6: elt] :
( mem(elt1,t2tb1(X5),nil(elt1))
=> ( mem(elt1,t2tb1(X6),t2tb(X3))
=> le(X5,X6) ) )
& ! [X5: elt,X6: elt] :
( mem(elt1,t2tb1(X5),nil(elt1))
=> ( mem(elt1,t2tb1(X6),t2tb(X4))
=> le(X5,X6) ) ) )
=> ! [X7: list_elt] :
( ( sorted(tb2t(reverse(elt1,t2tb(X7))))
& permut(elt1,t2tb(X7),infix_plpl(elt1,infix_plpl(elt1,nil(elt1),t2tb(X3)),t2tb(X4))) )
=> permut(elt1,t2tb(X7),prefix(elt1,X0,t2tb(X1))) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f101]) ).
tff(f121,plain,
~ ! [X0: $int,X1: list_elt] :
( ( ~ $less(X0,2)
& ~ $less(length(elt1,t2tb(X1)),X0) )
=> ( ( X0 != 2 )
=> ( ( X0 != 3 )
=> ( ( 2 != 0 )
=> ( ( ~ $less(div(X0,2),0)
& ~ $less(length(elt1,t2tb(X1)),div(X0,2)) )
=> ! [X2: list_elt] :
( ( X1 = tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),t2tb(X2))) )
=> ( ( tb2t(prefix(elt1,X0,t2tb(X1))) = tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),prefix(elt1,$sum(X0,$uminus(div(X0,2))),t2tb(X2)))) )
=> ( ( ~ $less(div(X0,2),2)
& ~ $less(length(elt1,t2tb(X1)),div(X0,2)) )
=> ! [X3: list_elt] :
( ( sorted(X3)
& permut(elt1,t2tb(X3),prefix(elt1,div(X0,2),t2tb(X1))) )
=> ( ( ~ $less($sum(X0,$uminus(div(X0,2))),2)
& ~ $less(length(elt1,t2tb(X2)),$sum(X0,$uminus(div(X0,2)))) )
=> ! [X4: list_elt] :
( ( sorted(X4)
& permut(elt1,t2tb(X4),prefix(elt1,$sum(X0,$uminus(div(X0,2))),t2tb(X2))) )
=> ( ( sorted(tb2t(reverse(elt1,nil(elt1))))
& sorted(X3)
& sorted(X4)
& ! [X5: elt,X6: elt] :
( mem(elt1,t2tb1(X5),nil(elt1))
=> ( mem(elt1,t2tb1(X6),t2tb(X3))
=> le(X5,X6) ) )
& ! [X5: elt,X6: elt] :
( mem(elt1,t2tb1(X5),nil(elt1))
=> ( mem(elt1,t2tb1(X6),t2tb(X4))
=> le(X5,X6) ) ) )
=> ! [X7: list_elt] :
( ( sorted(tb2t(reverse(elt1,t2tb(X7))))
& permut(elt1,t2tb(X7),infix_plpl(elt1,infix_plpl(elt1,nil(elt1),t2tb(X3)),t2tb(X4))) )
=> permut(elt1,t2tb(X7),prefix(elt1,X0,t2tb(X1))) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f102]) ).
tff(f142,plain,
~ ! [X0: $int,X1: list_elt] :
( ( ~ $less(X0,2)
& ~ $less(length(elt1,t2tb(X1)),X0) )
=> ( ( X0 != 2 )
=> ( ( X0 != 3 )
=> ( ( 2 != 0 )
=> ( ( ~ $less(div(X0,2),0)
& ~ $less(length(elt1,t2tb(X1)),div(X0,2)) )
=> ! [X2: list_elt] :
( ( X1 = tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),t2tb(X2))) )
=> ( ( tb2t(prefix(elt1,X0,t2tb(X1))) = tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),prefix(elt1,$sum(X0,$uminus(div(X0,2))),t2tb(X2)))) )
=> ( ( ~ $less(div(X0,2),2)
& ~ $less(length(elt1,t2tb(X1)),div(X0,2)) )
=> ! [X3: list_elt] :
( ( sorted(X3)
& permut(elt1,t2tb(X3),prefix(elt1,div(X0,2),t2tb(X1))) )
=> ( ( ~ $less($sum(X0,$uminus(div(X0,2))),2)
& ~ $less(length(elt1,t2tb(X2)),$sum(X0,$uminus(div(X0,2)))) )
=> ! [X4: list_elt] :
( ( sorted(X4)
& permut(elt1,t2tb(X4),prefix(elt1,$sum(X0,$uminus(div(X0,2))),t2tb(X2))) )
=> ( ( sorted(tb2t(reverse(elt1,nil(elt1))))
& sorted(X3)
& sorted(X4)
& ! [X5: elt,X6: elt] :
( mem(elt1,t2tb1(X5),nil(elt1))
=> ( mem(elt1,t2tb1(X6),t2tb(X3))
=> le(X5,X6) ) )
& ! [X7: elt,X8: elt] :
( mem(elt1,t2tb1(X7),nil(elt1))
=> ( mem(elt1,t2tb1(X8),t2tb(X4))
=> le(X7,X8) ) ) )
=> ! [X9: list_elt] :
( ( sorted(tb2t(reverse(elt1,t2tb(X9))))
& permut(elt1,t2tb(X9),infix_plpl(elt1,infix_plpl(elt1,nil(elt1),t2tb(X3)),t2tb(X4))) )
=> permut(elt1,t2tb(X9),prefix(elt1,X0,t2tb(X1))) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f121]) ).
tff(f154,plain,
! [X0: ty,X1: uni,X2: uni] :
( permut(X0,X2,X1)
| ~ permut(X0,X1,X2) ),
inference(ennf_transformation,[],[f44]) ).
tff(f155,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni] :
( permut(X0,X1,X3)
| ~ permut(X0,X2,X3)
| ~ permut(X0,X1,X2) ),
inference(ennf_transformation,[],[f45]) ).
tff(f156,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni] :
( permut(X0,X1,X3)
| ~ permut(X0,X2,X3)
| ~ permut(X0,X1,X2) ),
inference(flattening,[],[f155]) ).
tff(f158,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni,X4: uni] :
( permut(X0,infix_plpl(X0,X1,X2),infix_plpl(X0,X3,X4))
| ~ permut(X0,X2,X4)
| ~ permut(X0,X1,X3) ),
inference(ennf_transformation,[],[f50]) ).
tff(f159,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni,X4: uni] :
( permut(X0,infix_plpl(X0,X1,X2),infix_plpl(X0,X3,X4))
| ~ permut(X0,X2,X4)
| ~ permut(X0,X1,X3) ),
inference(flattening,[],[f158]) ).
tff(f206,plain,
? [X0: $int,X1: list_elt] :
( ? [X2: list_elt] :
( ? [X3: list_elt] :
( ? [X4: list_elt] :
( ? [X9: list_elt] :
( ~ permut(elt1,t2tb(X9),prefix(elt1,X0,t2tb(X1)))
& sorted(tb2t(reverse(elt1,t2tb(X9))))
& permut(elt1,t2tb(X9),infix_plpl(elt1,infix_plpl(elt1,nil(elt1),t2tb(X3)),t2tb(X4))) )
& sorted(tb2t(reverse(elt1,nil(elt1))))
& sorted(X3)
& sorted(X4)
& ! [X5: elt,X6: elt] :
( le(X5,X6)
| ~ mem(elt1,t2tb1(X6),t2tb(X3))
| ~ mem(elt1,t2tb1(X5),nil(elt1)) )
& ! [X7: elt,X8: elt] :
( le(X7,X8)
| ~ mem(elt1,t2tb1(X8),t2tb(X4))
| ~ mem(elt1,t2tb1(X7),nil(elt1)) )
& sorted(X4)
& permut(elt1,t2tb(X4),prefix(elt1,$sum(X0,$uminus(div(X0,2))),t2tb(X2))) )
& ~ $less($sum(X0,$uminus(div(X0,2))),2)
& ~ $less(length(elt1,t2tb(X2)),$sum(X0,$uminus(div(X0,2))))
& sorted(X3)
& permut(elt1,t2tb(X3),prefix(elt1,div(X0,2),t2tb(X1))) )
& ~ $less(div(X0,2),2)
& ~ $less(length(elt1,t2tb(X1)),div(X0,2))
& ( tb2t(prefix(elt1,X0,t2tb(X1))) = tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),prefix(elt1,$sum(X0,$uminus(div(X0,2))),t2tb(X2)))) )
& ( X1 = tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),t2tb(X2))) ) )
& ~ $less(div(X0,2),0)
& ~ $less(length(elt1,t2tb(X1)),div(X0,2))
& ( 2 != 0 )
& ( X0 != 3 )
& ( X0 != 2 )
& ~ $less(X0,2)
& ~ $less(length(elt1,t2tb(X1)),X0) ),
inference(ennf_transformation,[],[f142]) ).
tff(f207,plain,
? [X0: $int,X1: list_elt] :
( ? [X2: list_elt] :
( ? [X3: list_elt] :
( ? [X4: list_elt] :
( ? [X9: list_elt] :
( ~ permut(elt1,t2tb(X9),prefix(elt1,X0,t2tb(X1)))
& sorted(tb2t(reverse(elt1,t2tb(X9))))
& permut(elt1,t2tb(X9),infix_plpl(elt1,infix_plpl(elt1,nil(elt1),t2tb(X3)),t2tb(X4))) )
& sorted(tb2t(reverse(elt1,nil(elt1))))
& sorted(X3)
& sorted(X4)
& ! [X5: elt,X6: elt] :
( le(X5,X6)
| ~ mem(elt1,t2tb1(X6),t2tb(X3))
| ~ mem(elt1,t2tb1(X5),nil(elt1)) )
& ! [X7: elt,X8: elt] :
( le(X7,X8)
| ~ mem(elt1,t2tb1(X8),t2tb(X4))
| ~ mem(elt1,t2tb1(X7),nil(elt1)) )
& sorted(X4)
& permut(elt1,t2tb(X4),prefix(elt1,$sum(X0,$uminus(div(X0,2))),t2tb(X2))) )
& ~ $less($sum(X0,$uminus(div(X0,2))),2)
& ~ $less(length(elt1,t2tb(X2)),$sum(X0,$uminus(div(X0,2))))
& sorted(X3)
& permut(elt1,t2tb(X3),prefix(elt1,div(X0,2),t2tb(X1))) )
& ~ $less(div(X0,2),2)
& ~ $less(length(elt1,t2tb(X1)),div(X0,2))
& ( tb2t(prefix(elt1,X0,t2tb(X1))) = tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),prefix(elt1,$sum(X0,$uminus(div(X0,2))),t2tb(X2)))) )
& ( X1 = tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),t2tb(X2))) ) )
& ~ $less(div(X0,2),0)
& ~ $less(length(elt1,t2tb(X1)),div(X0,2))
& ( 2 != 0 )
& ( X0 != 3 )
& ( X0 != 2 )
& ~ $less(X0,2)
& ~ $less(length(elt1,t2tb(X1)),X0) ),
inference(flattening,[],[f206]) ).
tff(f230,plain,
? [X0: $int,X1: list_elt] :
( ? [X2: list_elt] :
( ? [X3: list_elt] :
( ? [X4: list_elt] :
( ? [X5: list_elt] :
( ~ permut(elt1,t2tb(X5),prefix(elt1,X0,t2tb(X1)))
& sorted(tb2t(reverse(elt1,t2tb(X5))))
& permut(elt1,t2tb(X5),infix_plpl(elt1,infix_plpl(elt1,nil(elt1),t2tb(X3)),t2tb(X4))) )
& sorted(tb2t(reverse(elt1,nil(elt1))))
& sorted(X3)
& sorted(X4)
& ! [X6: elt,X7: elt] :
( le(X6,X7)
| ~ mem(elt1,t2tb1(X7),t2tb(X3))
| ~ mem(elt1,t2tb1(X6),nil(elt1)) )
& ! [X8: elt,X9: elt] :
( le(X8,X9)
| ~ mem(elt1,t2tb1(X9),t2tb(X4))
| ~ mem(elt1,t2tb1(X8),nil(elt1)) )
& sorted(X4)
& permut(elt1,t2tb(X4),prefix(elt1,$sum(X0,$uminus(div(X0,2))),t2tb(X2))) )
& ~ $less($sum(X0,$uminus(div(X0,2))),2)
& ~ $less(length(elt1,t2tb(X2)),$sum(X0,$uminus(div(X0,2))))
& sorted(X3)
& permut(elt1,t2tb(X3),prefix(elt1,div(X0,2),t2tb(X1))) )
& ~ $less(div(X0,2),2)
& ~ $less(length(elt1,t2tb(X1)),div(X0,2))
& ( tb2t(prefix(elt1,X0,t2tb(X1))) = tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),prefix(elt1,$sum(X0,$uminus(div(X0,2))),t2tb(X2)))) )
& ( X1 = tb2t(infix_plpl(elt1,prefix(elt1,div(X0,2),t2tb(X1)),t2tb(X2))) ) )
& ~ $less(div(X0,2),0)
& ~ $less(length(elt1,t2tb(X1)),div(X0,2))
& ( 2 != 0 )
& ( X0 != 3 )
& ( X0 != 2 )
& ~ $less(X0,2)
& ~ $less(length(elt1,t2tb(X1)),X0) ),
inference(rectify,[],[f207]) ).
tff(f231,plain,
( ~ permut(elt1,t2tb(sK18),prefix(elt1,sK13,t2tb(sK14)))
& sorted(tb2t(reverse(elt1,t2tb(sK18))))
& permut(elt1,t2tb(sK18),infix_plpl(elt1,infix_plpl(elt1,nil(elt1),t2tb(sK16)),t2tb(sK17)))
& sorted(tb2t(reverse(elt1,nil(elt1))))
& sorted(sK16)
& sorted(sK17)
& ! [X6: elt,X7: elt] :
( le(X6,X7)
| ~ mem(elt1,t2tb1(X7),t2tb(sK16))
| ~ mem(elt1,t2tb1(X6),nil(elt1)) )
& ! [X8: elt,X9: elt] :
( le(X8,X9)
| ~ mem(elt1,t2tb1(X9),t2tb(sK17))
| ~ mem(elt1,t2tb1(X8),nil(elt1)) )
& sorted(sK17)
& permut(elt1,t2tb(sK17),prefix(elt1,$sum(sK13,$uminus(div(sK13,2))),t2tb(sK15)))
& ~ $less($sum(sK13,$uminus(div(sK13,2))),2)
& ~ $less(length(elt1,t2tb(sK15)),$sum(sK13,$uminus(div(sK13,2))))
& sorted(sK16)
& permut(elt1,t2tb(sK16),prefix(elt1,div(sK13,2),t2tb(sK14)))
& ~ $less(div(sK13,2),2)
& ~ $less(length(elt1,t2tb(sK14)),div(sK13,2))
& ( tb2t(prefix(elt1,sK13,t2tb(sK14))) = tb2t(infix_plpl(elt1,prefix(elt1,div(sK13,2),t2tb(sK14)),prefix(elt1,$sum(sK13,$uminus(div(sK13,2))),t2tb(sK15)))) )
& ( sK14 = tb2t(infix_plpl(elt1,prefix(elt1,div(sK13,2),t2tb(sK14)),t2tb(sK15))) )
& ~ $less(div(sK13,2),0)
& ~ $less(length(elt1,t2tb(sK14)),div(sK13,2))
& ( 2 != 0 )
& ( 3 != sK13 )
& ( 2 != sK13 )
& ~ $less(sK13,2)
& ~ $less(length(elt1,t2tb(sK14)),sK13) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16,sK17,sK18]),skolemize(X0,sK13),skolemize(X1,sK14),skolemize(X2,sK15),skolemize(X3,sK16),skolemize(X4,sK17),skolemize(X5,sK18)],[f230]) ).
tff(f258,plain,
! [X0: ty,X1: uni] : ( infix_plpl(X0,nil(X0),X1) = X1 ),
inference(cnf_transformation,[],[f24]) ).
tff(f292,plain,
! [X2: uni,X0: ty,X1: uni] :
( ~ permut(X0,X1,X2)
| permut(X0,X2,X1) ),
inference(cnf_transformation,[],[f154]) ).
tff(f293,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] :
( ~ permut(X0,X2,X3)
| permut(X0,X1,X3)
| ~ permut(X0,X1,X2) ),
inference(cnf_transformation,[],[f156]) ).
tff(f298,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni,X4: uni] :
( permut(X0,infix_plpl(X0,X1,X2),infix_plpl(X0,X3,X4))
| ~ permut(X0,X2,X4)
| ~ permut(X0,X1,X3) ),
inference(cnf_transformation,[],[f159]) ).
tff(f307,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f59]) ).
tff(f376,plain,
tb2t(prefix(elt1,sK13,t2tb(sK14))) = tb2t(infix_plpl(elt1,prefix(elt1,div(sK13,2),t2tb(sK14)),prefix(elt1,$sum(sK13,$uminus(div(sK13,2))),t2tb(sK15)))),
inference(cnf_transformation,[],[f231]) ).
tff(f379,plain,
permut(elt1,t2tb(sK16),prefix(elt1,div(sK13,2),t2tb(sK14))),
inference(cnf_transformation,[],[f231]) ).
tff(f383,plain,
permut(elt1,t2tb(sK17),prefix(elt1,$sum(sK13,$uminus(div(sK13,2))),t2tb(sK15))),
inference(cnf_transformation,[],[f231]) ).
tff(f390,plain,
permut(elt1,t2tb(sK18),infix_plpl(elt1,infix_plpl(elt1,nil(elt1),t2tb(sK16)),t2tb(sK17))),
inference(cnf_transformation,[],[f231]) ).
tff(f392,plain,
~ permut(elt1,t2tb(sK18),prefix(elt1,sK13,t2tb(sK14))),
inference(cnf_transformation,[],[f231]) ).
tff(f406,definition,
sF19 = t2tb(sK18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f407,plain,
t2tb(sK18) = sF19,
inference(reorient_equations,[],[f406]) ).
tff(f408,definition,
sF20 = t2tb(sK14),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f409,plain,
t2tb(sK14) = sF20,
inference(reorient_equations,[],[f408]) ).
tff(f410,definition,
sF21 = prefix(elt1,sK13,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f411,plain,
prefix(elt1,sK13,sF20) = sF21,
inference(reorient_equations,[],[f410]) ).
tff(f412,plain,
~ permut(elt1,sF19,sF21),
inference(definition_folding,[],[f392,f411,f409,f407]) ).
tff(f418,definition,
sF24 = nil(elt1),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f419,plain,
nil(elt1) = sF24,
inference(reorient_equations,[],[f418]) ).
tff(f420,definition,
sF25 = t2tb(sK16),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f421,plain,
t2tb(sK16) = sF25,
inference(reorient_equations,[],[f420]) ).
tff(f422,definition,
sF26 = infix_plpl(elt1,sF24,sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f423,plain,
infix_plpl(elt1,sF24,sF25) = sF26,
inference(reorient_equations,[],[f422]) ).
tff(f424,definition,
sF27 = t2tb(sK17),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f425,plain,
t2tb(sK17) = sF27,
inference(reorient_equations,[],[f424]) ).
tff(f426,definition,
sF28 = infix_plpl(elt1,sF26,sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f427,plain,
infix_plpl(elt1,sF26,sF27) = sF28,
inference(reorient_equations,[],[f426]) ).
tff(f428,plain,
permut(elt1,sF19,sF28),
inference(definition_folding,[],[f390,f427,f425,f423,f421,f419,f407]) ).
tff(f436,definition,
sF31 = div(sK13,2),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
tff(f437,plain,
div(sK13,2) = sF31,
inference(reorient_equations,[],[f436]) ).
tff(f438,definition,
sF32 = $uminus(sF31),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
tff(f439,plain,
$uminus(sF31) = sF32,
inference(reorient_equations,[],[f438]) ).
tff(f440,definition,
sF33 = $sum(sK13,sF32),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
tff(f441,plain,
$sum(sK13,sF32) = sF33,
inference(reorient_equations,[],[f440]) ).
tff(f442,definition,
sF34 = t2tb(sK15),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
tff(f443,plain,
t2tb(sK15) = sF34,
inference(reorient_equations,[],[f442]) ).
tff(f444,definition,
sF35 = prefix(elt1,sF33,sF34),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
tff(f445,plain,
prefix(elt1,sF33,sF34) = sF35,
inference(reorient_equations,[],[f444]) ).
tff(f446,plain,
permut(elt1,sF27,sF35),
inference(definition_folding,[],[f383,f445,f443,f441,f439,f437,f425]) ).
tff(f451,definition,
sF37 = prefix(elt1,sF31,sF20),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
tff(f452,plain,
prefix(elt1,sF31,sF20) = sF37,
inference(reorient_equations,[],[f451]) ).
tff(f453,plain,
permut(elt1,sF25,sF37),
inference(definition_folding,[],[f379,f452,f409,f437,f421]) ).
tff(f458,definition,
sF39 = tb2t(sF21),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
tff(f459,plain,
tb2t(sF21) = sF39,
inference(reorient_equations,[],[f458]) ).
tff(f460,definition,
sF40 = infix_plpl(elt1,sF37,sF35),
introduced(definition,[new_symbols(definition,[sF40])],[function_definition]) ).
tff(f461,plain,
infix_plpl(elt1,sF37,sF35) = sF40,
inference(reorient_equations,[],[f460]) ).
tff(f462,definition,
sF41 = tb2t(sF40),
introduced(definition,[new_symbols(definition,[sF41])],[function_definition]) ).
tff(f463,plain,
tb2t(sF40) = sF41,
inference(reorient_equations,[],[f462]) ).
tff(f464,plain,
sF39 = sF41,
inference(definition_folding,[],[f376,f463,f461,f445,f443,f441,f439,f437,f452,f409,f437,f459,f411,f409]) ).
tff(f477,plain,
sF39 = tb2t(sF40),
inference(forward_demodulation,[],[f463,f464]) ).
tff(f496,plain,
sF21 = t2tb(sF39),
inference(superposition,[],[f307,f459]) ).
tff(f499,plain,
sF40 = t2tb(sF39),
inference(superposition,[],[f307,f477]) ).
tff(f522,plain,
sF21 = sF40,
inference(superposition,[],[f499,f496]) ).
tff(f552,plain,
! [X0: uni] : ( infix_plpl(elt1,sF24,X0) = X0 ),
inference(superposition,[],[f258,f419]) ).
tff(f558,plain,
sF25 = sF26,
inference(superposition,[],[f423,f552]) ).
tff(f616,plain,
permut(elt1,sF28,sF19),
inference(resolution,[],[f292,f428]) ).
tff(f1297,plain,
! [X0: uni] :
( ~ permut(elt1,X0,sF28)
| permut(elt1,X0,sF19) ),
inference(resolution,[],[f293,f616]) ).
tff(f2044,plain,
! [X0: uni,X1: uni] :
( permut(elt1,infix_plpl(elt1,X0,X1),sF40)
| ~ permut(elt1,X1,sF35)
| ~ permut(elt1,X0,sF37) ),
inference(superposition,[],[f298,f461]) ).
tff(f2053,plain,
! [X0: uni,X1: uni] :
( permut(elt1,infix_plpl(elt1,X0,X1),sF21)
| ~ permut(elt1,X1,sF35)
| ~ permut(elt1,X0,sF37) ),
inference(forward_demodulation,[],[f2044,f522]) ).
tff(f3289,plain,
( permut(elt1,sF28,sF21)
| ~ permut(elt1,sF27,sF35)
| ~ permut(elt1,sF26,sF37) ),
inference(superposition,[],[f2053,f427]) ).
tff(f3314,plain,
( permut(elt1,sF28,sF21)
| ~ permut(elt1,sF26,sF37) ),
inference(forward_subsumption_resolution,[],[f3289,f446]) ).
tff(f3320,plain,
( ~ permut(elt1,sF25,sF37)
| permut(elt1,sF28,sF21) ),
inference(forward_demodulation,[],[f3314,f558]) ).
tff(f3322,plain,
permut(elt1,sF28,sF21),
inference(forward_subsumption_resolution,[],[f3320,f453]) ).
tff(f3327,plain,
permut(elt1,sF21,sF28),
inference(resolution,[],[f3322,f292]) ).
tff(f3372,plain,
permut(elt1,sF21,sF19),
inference(resolution,[],[f3327,f1297]) ).
tff(f3426,plain,
permut(elt1,sF19,sF21),
inference(resolution,[],[f3372,f292]) ).
tff(f3427,plain,
$false,
inference(forward_subsumption_resolution,[],[f3426,f412]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW626_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 % Computer : n005.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Mon Sep 28 14:22:46 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.28 Running first-order model finding
% 0.09/0.28 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.97/1.18 % (815184)Will run a generic schedule for satisfiability detection.
% 5.97/1.18 % (815195)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2661316597:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.97/1.18 % (815189)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3974204115_2999 on theBenchmark for (2999ds/0Mi)
% 5.97/1.18 % (815190)% WARNING: option uhcvi not known.
% 5.97/1.18 % (815189)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.97/1.18 % (815189)Terminated due to inappropriate strategy.
% 5.97/1.18 % (815189)------------------------------
% 5.97/1.18 % (815189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.18 % (815189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.18 % (815189)CaDiCaL version: 2.1.3
% 5.97/1.18 % (815189)Termination reason: Inappropriate
% 5.97/1.18 % (815189)Time elapsed: 0.006 s
% 5.97/1.18 % (815189)Peak memory usage: 11 MB
% 5.97/1.18 % (815189)Instructions burned: 10 (million)
% 5.97/1.18 % (815189)------------------------------
% 5.97/1.18 % (815189)------------------------------
% 5.97/1.18 % (815190)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2624778010:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.97/1.18 % (815194)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4057429377:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.97/1.18 % (815193)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3089428463:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.97/1.18 % (815192)dis+10_1_sil=32000:sp=arity:random_seed=2204269303:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.97/1.18 % (815191)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=165961617:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.97/1.18 % (815198)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4209312761:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.97/1.18 % (815198)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.97/1.18 % (815198)Terminated due to inappropriate strategy.
% 5.97/1.18 % (815198)------------------------------
% 5.97/1.18 % (815198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.18 % (815198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.18 % (815198)CaDiCaL version: 2.1.3
% 5.97/1.18 % (815198)Termination reason: Inappropriate
% 5.97/1.18 % (815198)Time elapsed: 0.011 s
% 5.97/1.18 % (815198)Peak memory usage: 10 MB
% 5.97/1.18 % (815198)Instructions burned: 9 (million)
% 5.97/1.18 % (815198)------------------------------
% 5.97/1.18 % (815198)------------------------------
% 5.97/1.18 % (815205)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1069682131:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.97/1.18 % (815195)Instruction limit reached!
% 5.97/1.18 % (815195)------------------------------
% 5.97/1.18 % (815195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.18 % (815195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.18 % (815195)CaDiCaL version: 2.1.3
% 5.97/1.18 % (815195)Termination reason: Instruction limit
% 5.97/1.18 % (815195)Termination phase: Saturation
% 5.97/1.18 % (815195)Time elapsed: 0.095 s
% 5.97/1.18 % (815195)Peak memory usage: 14 MB
% 5.97/1.18 % (815195)Instructions burned: 160 (million)
% 5.97/1.18 % (815192)Instruction limit reached!
% 5.97/1.18 % (815192)------------------------------
% 5.97/1.18 % (815192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.18 % (815192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.18 % (815192)CaDiCaL version: 2.1.3
% 5.97/1.18 % (815192)Termination reason: Instruction limit
% 5.97/1.18 % (815192)Termination phase: Saturation
% 5.97/1.18 % (815192)Time elapsed: 0.106 s
% 5.97/1.18 % (815192)Peak memory usage: 13 MB
% 5.97/1.18 % (815192)Instructions burned: 103 (million)
% 5.97/1.18 % (815207)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3974303226:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.97/1.18 % (815193)Instruction limit reached!
% 5.97/1.18 % (815193)------------------------------
% 5.97/1.18 % (815193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815193)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815193)Termination reason: Instruction limit
% 7.82/1.65 % (815193)Termination phase: Saturation
% 7.82/1.65 % (815193)Time elapsed: 0.120 s
% 7.82/1.65 % (815193)Peak memory usage: 13 MB
% 7.82/1.65 % (815193)Instructions burned: 116 (million)
% 7.82/1.65 % (815208)ott-21_1_sil=16000:fs=off:random_seed=3751373615:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.82/1.65 % (815194)Instruction limit reached!
% 7.82/1.65 % (815194)------------------------------
% 7.82/1.65 % (815194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815194)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815194)Termination reason: Instruction limit
% 7.82/1.65 % (815194)Termination phase: Saturation
% 7.82/1.65 % (815194)Time elapsed: 0.141 s
% 7.82/1.65 % (815194)Peak memory usage: 13 MB
% 7.82/1.65 % (815194)Instructions burned: 131 (million)
% 7.82/1.65 % (815210)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3854970562:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.82/1.65 % (815212)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1939493499:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.82/1.65 % (815212)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.82/1.65 % (815212)Terminated due to inappropriate strategy.
% 7.82/1.65 % (815212)------------------------------
% 7.82/1.65 % (815212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815212)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815212)Termination reason: Inappropriate
% 7.82/1.65 % (815212)Time elapsed: 0.009 s
% 7.82/1.65 % (815212)Peak memory usage: 10 MB
% 7.82/1.65 % (815212)Instructions burned: 9 (million)
% 7.82/1.65 % (815212)------------------------------
% 7.82/1.65 % (815212)------------------------------
% 7.82/1.65 % (815205)Instruction limit reached!
% 7.82/1.65 % (815205)------------------------------
% 7.82/1.65 % (815205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815205)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815205)Termination reason: Instruction limit
% 7.82/1.65 % (815205)Termination phase: Saturation
% 7.82/1.65 % (815205)Time elapsed: 0.122 s
% 7.82/1.65 % (815205)Peak memory usage: 13 MB
% 7.82/1.65 % (815205)Instructions burned: 131 (million)
% 7.82/1.65 % (815215)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2685700477:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 7.82/1.65 % (815208)Instruction limit reached!
% 7.82/1.65 % (815208)------------------------------
% 7.82/1.65 % (815208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815208)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815208)Termination reason: Instruction limit
% 7.82/1.65 % (815208)Termination phase: Saturation
% 7.82/1.65 % (815208)Time elapsed: 0.093 s
% 7.82/1.65 % (815208)Peak memory usage: 13 MB
% 7.82/1.65 % (815208)Instructions burned: 181 (million)
% 7.82/1.65 % (815216)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2103095819:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 7.82/1.65 % (815216)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.82/1.65 % (815216)Terminated due to inappropriate strategy.
% 7.82/1.65 % (815216)------------------------------
% 7.82/1.65 % (815216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815216)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815216)Termination reason: Inappropriate
% 7.82/1.65 % (815216)Time elapsed: 0.009 s
% 7.82/1.65 % (815216)Peak memory usage: 10 MB
% 7.82/1.65 % (815216)Instructions burned: 9 (million)
% 7.82/1.65 % (815216)------------------------------
% 7.82/1.65 % (815216)------------------------------
% 7.82/1.65 % (815218)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3010237580:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 7.82/1.65 % (815220)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=750141579:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 7.82/1.65 % (815218)Instruction limit reached!
% 7.82/1.65 % (815218)------------------------------
% 7.82/1.65 % (815218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815218)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815218)Termination reason: Instruction limit
% 7.82/1.65 % (815218)Termination phase: Saturation
% 7.82/1.65 % (815218)Time elapsed: 0.399 s
% 7.82/1.65 % (815218)Peak memory usage: 21 MB
% 7.82/1.65 % (815218)Instructions burned: 693 (million)
% 7.82/1.65 % (815223)fmb+10_1_sil=64000:random_seed=524960275:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 7.82/1.65 % (815210)Instruction limit reached!
% 7.82/1.65 % (815210)------------------------------
% 7.82/1.65 % (815210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815210)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815210)Termination reason: Instruction limit
% 7.82/1.65 % (815210)Termination phase: Saturation
% 7.82/1.65 % (815210)Time elapsed: 0.514 s
% 7.82/1.65 % (815210)Peak memory usage: 15 MB
% 7.82/1.65 % (815210)Instructions burned: 477 (million)
% 7.82/1.65 % (815223)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.82/1.65 % (815223)Terminated due to inappropriate strategy.
% 7.82/1.65 % (815223)------------------------------
% 7.82/1.65 % (815223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815223)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815223)Termination reason: Inappropriate
% 7.82/1.65 % (815223)Time elapsed: 0.006 s
% 7.82/1.65 % (815223)Peak memory usage: 11 MB
% 7.82/1.65 % (815223)Instructions burned: 10 (million)
% 7.82/1.65 % (815223)------------------------------
% 7.82/1.65 % (815223)------------------------------
% 7.82/1.65 % (815226)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1583001967:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi)
% 7.82/1.65 % (815226)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.82/1.65 % (815226)Terminated due to inappropriate strategy.
% 7.82/1.65 % (815226)------------------------------
% 7.82/1.65 % (815226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815226)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815226)Termination reason: Inappropriate
% 7.82/1.65 % (815226)Time elapsed: 0.005 s
% 7.82/1.65 % (815226)Peak memory usage: 10 MB
% 7.82/1.65 % (815226)Instructions burned: 9 (million)
% 7.82/1.65 % (815226)------------------------------
% 7.82/1.65 % (815226)------------------------------
% 7.82/1.65 % (815225)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=533469166:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 7.82/1.65 % (815225)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.82/1.65 % (815225)Terminated due to inappropriate strategy.
% 7.82/1.65 % (815225)------------------------------
% 7.82/1.65 % (815225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815225)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815225)Termination reason: Inappropriate
% 7.82/1.65 % (815225)Time elapsed: 0.010 s
% 7.82/1.65 % (815225)Peak memory usage: 10 MB
% 7.82/1.65 % (815225)Instructions burned: 9 (million)
% 7.82/1.65 % (815225)------------------------------
% 7.82/1.65 % (815225)------------------------------
% 7.82/1.65 % (815228)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2756233193:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 7.82/1.65 % (815230)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3914092191:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 7.82/1.65 % (815207)Instruction limit reached!
% 7.82/1.65 % (815207)------------------------------
% 7.82/1.65 % (815207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815207)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815207)Termination reason: Instruction limit
% 7.82/1.65 % (815207)Termination phase: Saturation
% 7.82/1.65 % (815207)Time elapsed: 0.727 s
% 7.82/1.65 % (815207)Peak memory usage: 18 MB
% 7.82/1.65 % (815207)Instructions burned: 685 (million)
% 7.82/1.65 % (815233)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3716169551:i=6324_2991 on theBenchmark for (2991ds/6324Mi)
% 7.82/1.65 % (815233)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.82/1.65 % (815233)Terminated due to inappropriate strategy.
% 7.82/1.65 % (815233)------------------------------
% 7.82/1.65 % (815233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815233)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815233)Termination reason: Inappropriate
% 7.82/1.65 % (815233)Time elapsed: 0.011 s
% 7.82/1.65 % (815233)Peak memory usage: 11 MB
% 7.82/1.65 % (815233)Instructions burned: 10 (million)
% 7.82/1.65 % (815233)------------------------------
% 7.82/1.65 % (815233)------------------------------
% 7.82/1.65 % (815235)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2577229206:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi)
% 7.82/1.65 % (815235)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.82/1.65 % (815235)Terminated due to inappropriate strategy.
% 7.82/1.65 % (815235)------------------------------
% 7.82/1.65 % (815235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815235)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815235)Termination reason: Inappropriate
% 7.82/1.65 % (815235)Time elapsed: 0.009 s
% 7.82/1.65 % (815235)Peak memory usage: 10 MB
% 7.82/1.65 % (815235)Instructions burned: 9 (million)
% 7.82/1.65 % (815235)------------------------------
% 7.82/1.65 % (815235)------------------------------
% 7.82/1.65 % (815237)ott-2_1_sil=16000:newcnf=on:random_seed=580805385:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi)
% 7.82/1.65 % (815220)Instruction limit reached!
% 7.82/1.65 % (815220)------------------------------
% 7.82/1.65 % (815220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815220)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815220)Termination reason: Instruction limit
% 7.82/1.65 % (815220)Termination phase: Saturation
% 7.82/1.65 % (815220)Time elapsed: 0.831 s
% 7.82/1.65 % (815220)Peak memory usage: 18 MB
% 7.82/1.65 % (815220)Instructions burned: 879 (million)
% 7.82/1.65 % (815239)ott+10_1_sil=32000:tgt=ground:random_seed=3009754157:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 7.82/1.65 % (815239) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-815184-815239"...
% 7.82/1.65 % (815239)...printing done.
% 7.82/1.65 % (815239)Refutation found. Thanks to Tanya!
% 7.82/1.65 % SZS status Theorem for theBenchmark
% 7.82/1.65 % SZS output start Proof for theBenchmark
% See solution above
% 7.82/1.65 % (815239)------------------------------
% 7.82/1.65 % (815239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.82/1.65 % (815239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.65 % (815239)CaDiCaL version: 2.1.3
% 7.82/1.65 % (815239)Termination reason: Refutation
% 7.82/1.65 % (815239)Time elapsed: 0.166 s
% 7.82/1.65 % (815239)Peak memory usage: 14 MB
% 7.82/1.65 % (815239)Instructions burned: 167 (million)
% 7.82/1.65 % (815184)Success in time 1.354 s
% 7.82/1.65 % Vampire exiting
%------------------------------------------------------------------------------