%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW629_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 : n014.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 6.53s 1.24s
% Output : Refutation 6.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 13
% Syntax : Number of formulae : 66 ( 34 unt; 0 typ; 9 def)
% Number of atoms : 261 ( 92 equ)
% Maximal formula atoms : 25 ( 3 avg)
% Number of connectives : 246 ( 51 ~; 47 |; 114 &)
% ( 5 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 35 ( 7 atm; 7 fun; 21 num; 0 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 ( 6 usr; 2 prp; 0-3 aty)
% Number of functors : 70 ( 67 usr; 38 con; 0-5 aty)
% Number of variables : 109 ( 0 sgn 69 !; 40 ?; 109 :)
% 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,
elt1: $tType ).
tff(type_def_10,type,
list_elt: $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,
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_list1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_16,type,
cons_proj_11: ( ty * uni ) > uni ).
tff(func_def_17,type,
cons_proj_21: ( ty * uni ) > uni ).
tff(func_def_18,type,
length2: ( ty * uni ) > $int ).
tff(func_def_21,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_22,type,
num_occ1: ( ty * uni * uni ) > $int ).
tff(func_def_23,type,
reverse: ( ty * uni ) > uni ).
tff(func_def_24,type,
t: ty > ty ).
tff(func_def_25,type,
mk_t: ( ty * uni ) > uni ).
tff(func_def_26,type,
elts: ( ty * uni ) > uni ).
tff(func_def_27,type,
length3: ( ty * uni ) > $int ).
tff(func_def_28,type,
elt: ty ).
tff(func_def_29,type,
t2tb: list_elt > uni ).
tff(func_def_30,type,
tb2t: uni > list_elt ).
tff(func_def_31,type,
t2tb1: elt1 > uni ).
tff(func_def_32,type,
tb2t1: uni > elt1 ).
tff(func_def_34,type,
sK0: ( ty * uni * uni ) > uni ).
tff(func_def_35,type,
sK1: ( ty * uni * uni ) > uni ).
tff(func_def_36,type,
sK2: ( ty * uni * uni ) > uni ).
tff(func_def_37,type,
sK3: list_elt > elt1 ).
tff(func_def_38,type,
sK4: list_elt > elt1 ).
tff(func_def_39,type,
sK5: list_elt > elt1 ).
tff(func_def_40,type,
sK6: list_elt > list_elt ).
tff(func_def_41,type,
sK7: ( elt1 * list_elt ) > elt1 ).
tff(func_def_42,type,
sK8: ( list_elt * list_elt ) > elt1 ).
tff(func_def_43,type,
sK9: ( list_elt * list_elt ) > elt1 ).
tff(func_def_44,type,
sK10: list_elt ).
tff(func_def_45,type,
sK11: list_elt ).
tff(func_def_46,type,
sK12: list_elt ).
tff(func_def_47,type,
sK13: list_elt ).
tff(func_def_48,type,
sK14: list_elt ).
tff(func_def_49,type,
sK15: list_elt ).
tff(func_def_50,type,
sK16: bool1 ).
tff(func_def_51,type,
sK17: list_elt ).
tff(func_def_52,type,
sK18: list_elt ).
tff(func_def_53,type,
sK19: list_elt ).
tff(func_def_54,type,
sF20: ( ty * uni * uni ) > uni ).
tff(func_def_55,type,
sF21: uni ).
tff(func_def_56,type,
sF22: uni ).
tff(func_def_57,type,
sF23: uni ).
tff(func_def_58,type,
sF24: uni ).
tff(func_def_59,type,
sF25: uni ).
tff(func_def_60,type,
sF26: uni ).
tff(func_def_61,type,
sF27: list_elt ).
tff(func_def_62,type,
sF28: uni ).
tff(func_def_63,type,
sF29: uni ).
tff(func_def_64,type,
sF30: uni ).
tff(func_def_65,type,
sF31: uni ).
tff(func_def_66,type,
sF32: uni ).
tff(func_def_67,type,
sF33: $int ).
tff(func_def_68,type,
sF34: $int ).
tff(func_def_69,type,
sF35: $int ).
tff(func_def_70,type,
sF36: $int ).
tff(func_def_71,type,
sF37: $int ).
tff(pred_def_1,type,
sort1: ( 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,
le1: ( elt1 * elt1 ) > $o ).
tff(pred_def_7,type,
sorted1: list_elt > $o ).
tff(f44,axiom,
! [X0: ty,X1: uni,X2: uni] :
( permut(X0,X1,X2)
=> permut(X0,X2,X1) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',permut_append) ).
tff(f74,conjecture,
! [X0: list_elt] :
( $less(1,length2(elt,t2tb(X0)))
=> ! [X1: list_elt] :
( ( X1 = tb2t(nil(elt)) )
=> ! [X2: list_elt] :
( ( X2 = tb2t(nil(elt)) )
=> ! [X3: list_elt,X4: list_elt,X5: list_elt] :
( ( permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X5)),t2tb(X0))
& ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X3)) )
| ( ( length2(elt,t2tb(X5)) = 0 )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X3)),1) ) ) ) )
=> ! [X6: bool1] :
( ( ( X6 = true1 )
<=> ( X5 = tb2t(nil(elt)) ) )
=> ( ( X6 = true1 )
=> ( ( X5 = tb2t(nil(elt)) )
=> ( permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X0))
=> ! [X7: list_elt] :
( ( sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4)) )
=> ! [X8: list_elt] :
( ( sorted1(X8)
& permut(elt,t2tb(X8),t2tb(X3)) )
=> ( ( ( X5 = tb2t(nil(elt)) )
& sorted1(X7)
& sorted1(X8) )
=> ! [X9: list_elt] :
( ( sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8))) )
=> ( sorted1(X9)
& permut(elt,t2tb(X9),t2tb(X0)) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_mergesort) ).
tff(f75,negated_conjecture,
~ ! [X0: list_elt] :
( $less(1,length2(elt,t2tb(X0)))
=> ! [X1: list_elt] :
( ( X1 = tb2t(nil(elt)) )
=> ! [X2: list_elt] :
( ( X2 = tb2t(nil(elt)) )
=> ! [X3: list_elt,X4: list_elt,X5: list_elt] :
( ( permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X5)),t2tb(X0))
& ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X3)) )
| ( ( length2(elt,t2tb(X5)) = 0 )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X3)),1) ) ) ) )
=> ! [X6: bool1] :
( ( ( X6 = true1 )
<=> ( X5 = tb2t(nil(elt)) ) )
=> ( ( X6 = true1 )
=> ( ( X5 = tb2t(nil(elt)) )
=> ( permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X0))
=> ! [X7: list_elt] :
( ( sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4)) )
=> ! [X8: list_elt] :
( ( sorted1(X8)
& permut(elt,t2tb(X8),t2tb(X3)) )
=> ( ( ( X5 = tb2t(nil(elt)) )
& sorted1(X7)
& sorted1(X8) )
=> ! [X9: list_elt] :
( ( sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8))) )
=> ( sorted1(X9)
& permut(elt,t2tb(X9),t2tb(X0)) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f74]) ).
tff(f109,plain,
! [X0: ty,X1: uni,X2: uni] :
( permut(X0,X2,X1)
| ~ permut(X0,X1,X2) ),
inference(ennf_transformation,[],[f44]) ).
tff(f110,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(f111,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni] :
( permut(X0,X1,X3)
| ~ permut(X0,X2,X3)
| ~ permut(X0,X1,X2) ),
inference(flattening,[],[f110]) ).
tff(f113,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(f114,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,[],[f113]) ).
tff(f128,plain,
? [X0: list_elt] :
( ? [X1: list_elt] :
( ? [X2: list_elt] :
( ? [X3: list_elt,X4: list_elt,X5: list_elt] :
( ? [X6: bool1] :
( ? [X7: list_elt] :
( ? [X8: list_elt] :
( ? [X9: list_elt] :
( ( ~ sorted1(X9)
| ~ permut(elt,t2tb(X9),t2tb(X0)) )
& sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8))) )
& ( X5 = tb2t(nil(elt)) )
& sorted1(X7)
& sorted1(X8)
& sorted1(X8)
& permut(elt,t2tb(X8),t2tb(X3)) )
& sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4)) )
& permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X0))
& ( X5 = tb2t(nil(elt)) )
& ( X6 = true1 )
& ( ( X6 = true1 )
<=> ( X5 = tb2t(nil(elt)) ) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X5)),t2tb(X0))
& ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X3)) )
| ( ( length2(elt,t2tb(X5)) = 0 )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X3)),1) ) ) ) )
& ( X2 = tb2t(nil(elt)) ) )
& ( X1 = tb2t(nil(elt)) ) )
& $less(1,length2(elt,t2tb(X0))) ),
inference(ennf_transformation,[],[f75]) ).
tff(f129,plain,
? [X0: list_elt] :
( ? [X1: list_elt] :
( ? [X2: list_elt] :
( ? [X3: list_elt,X4: list_elt,X5: list_elt] :
( ? [X6: bool1] :
( ? [X7: list_elt] :
( ? [X8: list_elt] :
( ? [X9: list_elt] :
( ( ~ sorted1(X9)
| ~ permut(elt,t2tb(X9),t2tb(X0)) )
& sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8))) )
& ( X5 = tb2t(nil(elt)) )
& sorted1(X7)
& sorted1(X8)
& sorted1(X8)
& permut(elt,t2tb(X8),t2tb(X3)) )
& sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4)) )
& permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X0))
& ( X5 = tb2t(nil(elt)) )
& ( X6 = true1 )
& ( ( X6 = true1 )
<=> ( X5 = tb2t(nil(elt)) ) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X5)),t2tb(X0))
& ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X3)) )
| ( ( length2(elt,t2tb(X5)) = 0 )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X3)),1) ) ) ) )
& ( X2 = tb2t(nil(elt)) ) )
& ( X1 = tb2t(nil(elt)) ) )
& $less(1,length2(elt,t2tb(X0))) ),
inference(flattening,[],[f128]) ).
tff(f148,plain,
? [X0: list_elt] :
( ? [X1: list_elt] :
( ? [X2: list_elt] :
( ? [X3: list_elt,X4: list_elt,X5: list_elt] :
( ? [X6: bool1] :
( ? [X7: list_elt] :
( ? [X8: list_elt] :
( ? [X9: list_elt] :
( ( ~ sorted1(X9)
| ~ permut(elt,t2tb(X9),t2tb(X0)) )
& sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8))) )
& ( X5 = tb2t(nil(elt)) )
& sorted1(X7)
& sorted1(X8)
& sorted1(X8)
& permut(elt,t2tb(X8),t2tb(X3)) )
& sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4)) )
& permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X0))
& ( X5 = tb2t(nil(elt)) )
& ( X6 = true1 )
& ( ( X6 = true1 )
| ( tb2t(nil(elt)) != X5 ) )
& ( ( X5 = tb2t(nil(elt)) )
| ( true1 != X6 ) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X5)),t2tb(X0))
& ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X3)) )
| ( ( length2(elt,t2tb(X5)) = 0 )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X3)),1) ) ) ) )
& ( X2 = tb2t(nil(elt)) ) )
& ( X1 = tb2t(nil(elt)) ) )
& $less(1,length2(elt,t2tb(X0))) ),
inference(nnf_transformation,[],[f129]) ).
tff(f149,plain,
? [X0: list_elt] :
( ? [X1: list_elt] :
( ? [X2: list_elt] :
( ? [X3: list_elt,X4: list_elt,X5: list_elt] :
( ? [X6: bool1] :
( ? [X7: list_elt] :
( ? [X8: list_elt] :
( ? [X9: list_elt] :
( ( ~ sorted1(X9)
| ~ permut(elt,t2tb(X9),t2tb(X0)) )
& sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8))) )
& ( X5 = tb2t(nil(elt)) )
& sorted1(X7)
& sorted1(X8)
& sorted1(X8)
& permut(elt,t2tb(X8),t2tb(X3)) )
& sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4)) )
& permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X0))
& ( X5 = tb2t(nil(elt)) )
& ( X6 = true1 )
& ( ( X6 = true1 )
| ( tb2t(nil(elt)) != X5 ) )
& ( ( X5 = tb2t(nil(elt)) )
| ( true1 != X6 ) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X5)),t2tb(X0))
& ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X3)) )
| ( ( length2(elt,t2tb(X5)) = 0 )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X3)),1) ) ) ) )
& ( X2 = tb2t(nil(elt)) ) )
& ( X1 = tb2t(nil(elt)) ) )
& $less(1,length2(elt,t2tb(X0))) ),
inference(flattening,[],[f148]) ).
tff(f150,plain,
( ( ~ sorted1(sK19)
| ~ permut(elt,t2tb(sK19),t2tb(sK10)) )
& sorted1(sK19)
& permut(elt,t2tb(sK19),infix_plpl(elt,t2tb(sK17),t2tb(sK18)))
& ( tb2t(nil(elt)) = sK15 )
& sorted1(sK17)
& sorted1(sK18)
& sorted1(sK18)
& permut(elt,t2tb(sK18),t2tb(sK13))
& sorted1(sK17)
& permut(elt,t2tb(sK17),t2tb(sK14))
& permut(elt,infix_plpl(elt,t2tb(sK14),t2tb(sK13)),t2tb(sK10))
& ( tb2t(nil(elt)) = sK15 )
& ( true1 = sK16 )
& ( ( true1 = sK16 )
| ( tb2t(nil(elt)) != sK15 ) )
& ( ( tb2t(nil(elt)) = sK15 )
| ( true1 != sK16 ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(sK14),t2tb(sK13)),t2tb(sK15)),t2tb(sK10))
& ( ( length2(elt,t2tb(sK14)) = length2(elt,t2tb(sK13)) )
| ( ( 0 = length2(elt,t2tb(sK15)) )
& ( length2(elt,t2tb(sK14)) = $sum(length2(elt,t2tb(sK13)),1) ) ) )
& ( tb2t(nil(elt)) = sK12 )
& ( tb2t(nil(elt)) = sK11 )
& $less(1,length2(elt,t2tb(sK10))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19]),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)],[f149]) ).
tff(f211,plain,
! [X2: uni,X0: ty,X1: uni] :
( ~ permut(X0,X1,X2)
| permut(X0,X2,X1) ),
inference(cnf_transformation,[],[f109]) ).
tff(f212,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] :
( ~ permut(X0,X2,X3)
| permut(X0,X1,X3)
| ~ permut(X0,X1,X2) ),
inference(cnf_transformation,[],[f111]) ).
tff(f217,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,[],[f114]) ).
tff(f261,plain,
permut(elt,infix_plpl(elt,t2tb(sK14),t2tb(sK13)),t2tb(sK10)),
inference(cnf_transformation,[],[f150]) ).
tff(f262,plain,
permut(elt,t2tb(sK17),t2tb(sK14)),
inference(cnf_transformation,[],[f150]) ).
tff(f264,plain,
permut(elt,t2tb(sK18),t2tb(sK13)),
inference(cnf_transformation,[],[f150]) ).
tff(f269,plain,
permut(elt,t2tb(sK19),infix_plpl(elt,t2tb(sK17),t2tb(sK18))),
inference(cnf_transformation,[],[f150]) ).
tff(f270,plain,
sorted1(sK19),
inference(cnf_transformation,[],[f150]) ).
tff(f271,plain,
( ~ sorted1(sK19)
| ~ permut(elt,t2tb(sK19),t2tb(sK10)) ),
inference(cnf_transformation,[],[f150]) ).
tff(f284,definition,
sF21 = t2tb(sK19),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f285,plain,
t2tb(sK19) = sF21,
inference(reorient_equations,[],[f284]) ).
tff(f286,definition,
sF22 = t2tb(sK10),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f287,plain,
t2tb(sK10) = sF22,
inference(reorient_equations,[],[f286]) ).
tff(f288,plain,
( ~ sorted1(sK19)
| ~ permut(elt,sF21,sF22) ),
inference(definition_folding,[],[f271,f287,f285]) ).
tff(f289,definition,
sF23 = t2tb(sK17),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f290,plain,
t2tb(sK17) = sF23,
inference(reorient_equations,[],[f289]) ).
tff(f291,definition,
sF24 = t2tb(sK18),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f292,plain,
t2tb(sK18) = sF24,
inference(reorient_equations,[],[f291]) ).
tff(f293,definition,
sF25 = infix_plpl(elt,sF23,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f294,plain,
infix_plpl(elt,sF23,sF24) = sF25,
inference(reorient_equations,[],[f293]) ).
tff(f295,plain,
permut(elt,sF21,sF25),
inference(definition_folding,[],[f269,f294,f292,f290,f285]) ).
tff(f301,definition,
sF28 = t2tb(sK13),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f302,plain,
t2tb(sK13) = sF28,
inference(reorient_equations,[],[f301]) ).
tff(f303,plain,
permut(elt,sF24,sF28),
inference(definition_folding,[],[f264,f302,f292]) ).
tff(f304,definition,
sF29 = t2tb(sK14),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f305,plain,
t2tb(sK14) = sF29,
inference(reorient_equations,[],[f304]) ).
tff(f306,plain,
permut(elt,sF23,sF29),
inference(definition_folding,[],[f262,f305,f290]) ).
tff(f307,definition,
sF30 = infix_plpl(elt,sF29,sF28),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
tff(f308,plain,
infix_plpl(elt,sF29,sF28) = sF30,
inference(reorient_equations,[],[f307]) ).
tff(f309,plain,
permut(elt,sF30,sF22),
inference(definition_folding,[],[f261,f287,f308,f302,f305]) ).
tff(f355,plain,
~ permut(elt,sF21,sF22),
inference(forward_subsumption_resolution,[],[f288,f270]) ).
tff(f2155,plain,
permut(elt,sF25,sF21),
inference(resolution,[],[f211,f295]) ).
tff(f2736,plain,
! [X0: uni] :
( ~ permut(elt,X0,sF25)
| permut(elt,X0,sF21) ),
inference(resolution,[],[f212,f2155]) ).
tff(f2739,plain,
! [X0: uni] :
( ~ permut(elt,X0,sF30)
| permut(elt,X0,sF22) ),
inference(resolution,[],[f212,f309]) ).
tff(f3294,plain,
! [X0: uni,X1: uni] :
( permut(elt,sF25,infix_plpl(elt,X0,X1))
| ~ permut(elt,sF24,X1)
| ~ permut(elt,sF23,X0) ),
inference(superposition,[],[f217,f294]) ).
tff(f16237,plain,
( permut(elt,sF25,sF30)
| ~ permut(elt,sF24,sF28)
| ~ permut(elt,sF23,sF29) ),
inference(superposition,[],[f3294,f308]) ).
tff(f16260,plain,
( permut(elt,sF25,sF30)
| ~ permut(elt,sF23,sF29) ),
inference(forward_subsumption_resolution,[],[f16237,f303]) ).
tff(f16291,definition,
( spl38_196
<=> permut(elt,sF25,sF30) ),
introduced(definition,[new_symbols(definition,[spl38_196])],[avatar_definition]) ).
tff(f16293,plain,
( permut(elt,sF25,sF30)
| ~ spl38_196 ),
inference(avatar_component_clause,[],[f16291]) ).
tff(f16296,plain,
permut(elt,sF25,sF30),
inference(forward_subsumption_resolution,[],[f16260,f306]) ).
tff(f16301,plain,
spl38_196,
inference(avatar_split_clause,[],[f16296,f16291]) ).
tff(f16313,plain,
( permut(elt,sF25,sF22)
| ~ spl38_196 ),
inference(resolution,[],[f16293,f2739]) ).
tff(f16418,plain,
( permut(elt,sF22,sF25)
| ~ spl38_196 ),
inference(resolution,[],[f16313,f211]) ).
tff(f16625,plain,
( permut(elt,sF22,sF21)
| ~ spl38_196 ),
inference(resolution,[],[f16418,f2736]) ).
tff(f16755,plain,
( permut(elt,sF21,sF22)
| ~ spl38_196 ),
inference(resolution,[],[f16625,f211]) ).
tff(f16764,plain,
( $false
| ~ spl38_196 ),
inference(forward_subsumption_resolution,[],[f16755,f355]) ).
tff(f16765,plain,
~ spl38_196,
inference(avatar_contradiction_clause,[],[f16764]) ).
cnf(s183,plain,
spl38_196,
inference(sat_conversion,[],[f16301]) ).
cnf(s202,plain,
~ spl38_196,
inference(sat_conversion,[],[f16765]) ).
cnf(s203,plain,
$false,
inference(rat,[],[s183,s202]) ).
tff(f16779,plain,
$false,
inference(avatar_sat_refutation,[],[s203]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW629_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.11/0.23 % Computer : n014.cluster.edu
% 0.11/0.23 % Model : x86_64 x86_64
% 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.23 % Memory : 8046.5625MB
% 0.11/0.23 % OS : Linux 6.8.0-71-generic
% 0.11/0.23 % CPULimit : 300
% 0.11/0.23 % WCLimit : 300
% 0.11/0.23 % DateTime : Mon Sep 28 14:23:01 UTC 2026
% 0.11/0.23 % CPUTime :
% 0.11/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.27 Running first-order model finding
% 0.11/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
% 6.53/1.22 % (1806955)Will run a generic schedule for satisfiability detection.
% 6.53/1.22 % (1806962)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2111801332:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.53/1.22 % (1806966)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2733682945:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.53/1.22 % (1806961)% WARNING: option uhcvi not known.
% 6.53/1.22 % (1806963)dis+10_1_sil=32000:sp=arity:random_seed=1063145621:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.53/1.22 % (1806960)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3519541476_2999 on theBenchmark for (2999ds/0Mi)
% 6.53/1.22 % (1806961)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3447129578:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.53/1.22 % (1806964)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1340972273:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.53/1.22 % (1806965)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2928502350:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.53/1.22 % (1806960)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.53/1.22 % (1806960)Terminated due to inappropriate strategy.
% 6.53/1.22 % (1806960)------------------------------
% 6.53/1.22 % (1806960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.22 % (1806960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.22 % (1806960)CaDiCaL version: 2.1.3
% 6.53/1.22 % (1806960)Termination reason: Inappropriate
% 6.53/1.22 % (1806960)Time elapsed: 0.007 s
% 6.53/1.22 % (1806960)Peak memory usage: 11 MB
% 6.53/1.22 % (1806960)Instructions burned: 7 (million)
% 6.53/1.22 % (1806960)------------------------------
% 6.53/1.22 % (1806960)------------------------------
% 6.53/1.22 % (1806976)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=269195732:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.53/1.22 % (1806976)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.53/1.22 % (1806976)Terminated due to inappropriate strategy.
% 6.53/1.22 % (1806976)------------------------------
% 6.53/1.22 % (1806976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.22 % (1806976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.22 % (1806976)CaDiCaL version: 2.1.3
% 6.53/1.22 % (1806976)Termination reason: Inappropriate
% 6.53/1.22 % (1806976)Time elapsed: 0.006 s
% 6.53/1.22 % (1806976)Peak memory usage: 10 MB
% 6.53/1.22 % (1806976)Instructions burned: 6 (million)
% 6.53/1.22 % (1806976)------------------------------
% 6.53/1.22 % (1806976)------------------------------
% 6.53/1.22 % (1806966)Instruction limit reached!
% 6.53/1.22 % (1806966)------------------------------
% 6.53/1.22 % (1806966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.22 % (1806966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.22 % (1806966)CaDiCaL version: 2.1.3
% 6.53/1.22 % (1806966)Termination reason: Instruction limit
% 6.53/1.22 % (1806966)Termination phase: Saturation
% 6.53/1.22 % (1806966)Time elapsed: 0.082 s
% 6.53/1.22 % (1806966)Peak memory usage: 12 MB
% 6.53/1.22 % (1806966)Instructions burned: 159 (million)
% 6.53/1.22 % (1806963)Instruction limit reached!
% 6.53/1.22 % (1806963)------------------------------
% 6.53/1.22 % (1806963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.22 % (1806963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.22 % (1806963)CaDiCaL version: 2.1.3
% 6.53/1.22 % (1806963)Termination reason: Instruction limit
% 6.53/1.22 % (1806963)Termination phase: Saturation
% 6.53/1.22 % (1806963)Time elapsed: 0.080 s
% 6.53/1.22 % (1806963)Peak memory usage: 12 MB
% 6.53/1.22 % (1806963)Instructions burned: 104 (million)
% 6.53/1.22 % (1806982)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=790239783:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.53/1.22 % (1806965)Instruction limit reached!
% 6.53/1.22 % (1806965)------------------------------
% 6.53/1.22 % (1806965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.22 % (1806965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.22 % (1806965)CaDiCaL version: 2.1.3
% 6.53/1.22 % (1806965)Termination reason: Instruction limit
% 6.53/1.24 % (1806965)Termination phase: Saturation
% 6.53/1.24 % (1806965)Time elapsed: 0.088 s
% 6.53/1.24 % (1806965)Peak memory usage: 12 MB
% 6.53/1.24 % (1806965)Instructions burned: 131 (million)
% 6.53/1.24 % (1806964)Instruction limit reached!
% 6.53/1.24 % (1806964)------------------------------
% 6.53/1.24 % (1806964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.24 % (1806964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.24 % (1806964)CaDiCaL version: 2.1.3
% 6.53/1.24 % (1806964)Termination reason: Instruction limit
% 6.53/1.24 % (1806964)Termination phase: Saturation
% 6.53/1.24 % (1806964)Time elapsed: 0.089 s
% 6.53/1.24 % (1806964)Peak memory usage: 12 MB
% 6.53/1.24 % (1806964)Instructions burned: 116 (million)
% 6.53/1.24 % (1806983)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=2072808907:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.53/1.24 % (1806984)ott-21_1_sil=16000:fs=off:random_seed=2510888301:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.53/1.24 % (1806986)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2712121828:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.53/1.24 % (1806987)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1046924008:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 6.53/1.24 % (1806987)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.53/1.24 % (1806987)Terminated due to inappropriate strategy.
% 6.53/1.24 % (1806987)------------------------------
% 6.53/1.24 % (1806987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.24 % (1806987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.24 % (1806987)CaDiCaL version: 2.1.3
% 6.53/1.24 % (1806987)Termination reason: Inappropriate
% 6.53/1.24 % (1806987)Time elapsed: 0.005 s
% 6.53/1.24 % (1806987)Peak memory usage: 10 MB
% 6.53/1.24 % (1806987)Instructions burned: 6 (million)
% 6.53/1.24 % (1806987)------------------------------
% 6.53/1.24 % (1806987)------------------------------
% 6.53/1.24 % (1806993)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3007995870:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 6.53/1.24 % (1806982)Instruction limit reached!
% 6.53/1.24 % (1806982)------------------------------
% 6.53/1.24 % (1806982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.24 % (1806982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.24 % (1806982)CaDiCaL version: 2.1.3
% 6.53/1.24 % (1806982)Termination reason: Instruction limit
% 6.53/1.24 % (1806982)Termination phase: Saturation
% 6.53/1.24 % (1806982)Time elapsed: 0.113 s
% 6.53/1.24 % (1806982)Peak memory usage: 12 MB
% 6.53/1.24 % (1806982)Instructions burned: 131 (million)
% 6.53/1.24 % (1807001)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=156387986:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 6.53/1.24 % (1807001)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.53/1.24 % (1807001)Terminated due to inappropriate strategy.
% 6.53/1.24 % (1807001)------------------------------
% 6.53/1.24 % (1807001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.24 % (1807001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.24 % (1807001)CaDiCaL version: 2.1.3
% 6.53/1.24 % (1807001)Termination reason: Inappropriate
% 6.53/1.24 % (1807001)Time elapsed: 0.006 s
% 6.53/1.24 % (1807001)Peak memory usage: 11 MB
% 6.53/1.24 % (1807001)Instructions burned: 6 (million)
% 6.53/1.24 % (1807001)------------------------------
% 6.53/1.24 % (1807001)------------------------------
% 6.53/1.24 % (1806984)Instruction limit reached!
% 6.53/1.24 % (1806984)------------------------------
% 6.53/1.24 % (1806984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.24 % (1806984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.24 % (1806984)CaDiCaL version: 2.1.3
% 6.53/1.24 % (1806984)Termination reason: Instruction limit
% 6.53/1.24 % (1806984)Termination phase: Saturation
% 6.53/1.24 % (1806984)Time elapsed: 0.146 s
% 6.53/1.24 % (1806984)Peak memory usage: 13 MB
% 6.53/1.24 % (1806984)Instructions burned: 181 (million)
% 6.53/1.24 % (1807003)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=1821640216: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)
% 6.53/1.24 % (1807005)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2475218370:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 6.53/1.24 % (1806986)Instruction limit reached!
% 6.53/1.24 % (1806986)------------------------------
% 6.53/1.24 % (1806986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.24 % (1806986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.24 % (1806986)CaDiCaL version: 2.1.3
% 6.53/1.24 % (1806986)Termination reason: Instruction limit
% 6.53/1.24 % (1806986)Termination phase: Saturation
% 6.53/1.24 % (1806986)Time elapsed: 0.250 s
% 6.53/1.24 % (1806986)Peak memory usage: 12 MB
% 6.53/1.24 % (1806986)Instructions burned: 478 (million)
% 6.53/1.24 % (1807015)fmb+10_1_sil=64000:random_seed=3026480131:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 6.53/1.24 % (1807015)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.53/1.24 % (1807015)Terminated due to inappropriate strategy.
% 6.53/1.24 % (1807015)------------------------------
% 6.53/1.24 % (1807015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.24 % (1807015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.24 % (1807015)CaDiCaL version: 2.1.3
% 6.53/1.24 % (1807015)Termination reason: Inappropriate
% 6.53/1.24 % (1807015)Time elapsed: 0.007 s
% 6.53/1.24 % (1807015)Peak memory usage: 11 MB
% 6.53/1.24 % (1807015)Instructions burned: 7 (million)
% 6.53/1.24 % (1807015)------------------------------
% 6.53/1.24 % (1807015)------------------------------
% 6.53/1.24 % (1807020)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1775389203:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 6.53/1.24 % (1807020)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.53/1.24 % (1807020)Terminated due to inappropriate strategy.
% 6.53/1.24 % (1807020)------------------------------
% 6.53/1.24 % (1807020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.24 % (1807020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.24 % (1807020)CaDiCaL version: 2.1.3
% 6.53/1.24 % (1807020)Termination reason: Inappropriate
% 6.53/1.24 % (1807020)Time elapsed: 0.006 s
% 6.53/1.24 % (1807020)Peak memory usage: 10 MB
% 6.53/1.24 % (1807020)Instructions burned: 6 (million)
% 6.53/1.24 % (1807020)------------------------------
% 6.53/1.24 % (1807020)------------------------------
% 6.53/1.24 % (1807023)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=466120948:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 6.53/1.24 % (1807023)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.53/1.24 % (1807023)Terminated due to inappropriate strategy.
% 6.53/1.24 % (1807023)------------------------------
% 6.53/1.24 % (1807023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.24 % (1807023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.24 % (1807023)CaDiCaL version: 2.1.3
% 6.53/1.24 % (1807023)Termination reason: Inappropriate
% 6.53/1.24 % (1807023)Time elapsed: 0.005 s
% 6.53/1.24 % (1807023)Peak memory usage: 10 MB
% 6.53/1.24 % (1807023)Instructions burned: 6 (million)
% 6.53/1.24 % (1807023)------------------------------
% 6.53/1.24 % (1807023)------------------------------
% 6.53/1.24 % (1807025)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1856718383:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 6.53/1.24 % (1806983)Instruction limit reached!
% 6.53/1.24 % (1806983)------------------------------
% 6.53/1.24 % (1806983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.24 % (1806983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.24 % (1806983)CaDiCaL version: 2.1.3
% 6.53/1.24 % (1806983)Termination reason: Instruction limit
% 6.53/1.24 % (1806983)Termination phase: Saturation
% 6.53/1.24 % (1806983)Time elapsed: 0.533 s
% 6.53/1.24 % (1806983)Peak memory usage: 15 MB
% 6.53/1.24 % (1806983)Instructions burned: 685 (million)
% 6.53/1.24 % (1807036)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1881161666:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi)
% 6.53/1.24 % (1807003)Instruction limit reached!
% 6.53/1.24 % (1807003)------------------------------
% 6.53/1.24 % (1807003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.24 % (1807003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.24 % (1807003)CaDiCaL version: 2.1.3
% 6.53/1.24 % (1807003)Termination reason: Instruction limit
% 6.53/1.24 % (1807003)Termination phase: Saturation
% 6.53/1.24 % (1807003)Time elapsed: 0.623 s
% 6.53/1.24 % (1807003)Peak memory usage: 18 MB
% 6.53/1.24 % (1807003)Instructions burned: 692 (million)
% 6.53/1.24 % (1806993) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1806955-1806993"...
% 6.53/1.24 % (1806993)...printing done.
% 6.53/1.24 % (1806993)Refutation found. Thanks to Tanya!
% 6.53/1.24 % SZS status Theorem for theBenchmark
% 6.53/1.24 % SZS output start Proof for theBenchmark
% See solution above
% 6.53/1.24 % (1806993)------------------------------
% 6.53/1.24 % (1806993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.24 % (1806993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.24 % (1806993)CaDiCaL version: 2.1.3
% 6.53/1.24 % (1806993)Termination reason: Refutation
% 6.53/1.24 % (1806993)Time elapsed: 0.754 s
% 6.53/1.24 % (1806993)Peak memory usage: 20 MB
% 6.53/1.24 % (1806993)Instructions burned: 1050 (million)
% 6.53/1.24 % (1806955)Success in time 0.959 s
% 6.53/1.24 % Vampire exiting
%------------------------------------------------------------------------------