%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP352_1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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 11:39:25 AM UTC 2026
% Result : Theorem 69.84s 13.83s
% Output : Refutation 69.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 29
% Syntax : Number of formulae : 138 ( 50 unt; 0 typ; 4 def)
% Number of atoms : 318 ( 111 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 292 ( 112 ~; 122 |; 31 &)
% ( 14 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number arithmetic : 517 ( 150 atm; 0 fun; 250 num; 117 var)
% Number of types : 13 ( 10 usr; 2 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 18 ( 14 usr; 5 prp; 0-3 aty)
% Number of functors : 60 ( 56 usr; 14 con; 0-2 aty)
% Number of variables : 129 ( 0 sgn 129 !; 0 ?; 129 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'Int_int_fun$': $tType ).
tff(type_def_6,type,
'Num_bool_fun$': $tType ).
tff(type_def_7,type,
'Nat_nat_fun$': $tType ).
tff(type_def_8,type,
'Nat$': $tType ).
tff(type_def_9,type,
'Num$': $tType ).
tff(type_def_10,type,
'Real_real_fun$': $tType ).
tff(type_def_11,type,
'Nat_real_fun$': $tType ).
tff(type_def_12,type,
'A$': $tType ).
tff(type_def_13,type,
'Nat_bool_fun$': $tType ).
tff(type_def_14,type,
'Nat_int_fun$': $tType ).
tff(func_def_0,type,
'times$b': 'Nat$' > 'Nat_nat_fun$' ).
tff(func_def_1,type,
'norm$': $real > $real ).
tff(func_def_2,type,
'bit0$': 'Num$' > 'Num$' ).
tff(func_def_3,type,
'zero$': 'Nat$' ).
tff(func_def_4,type,
'one$a': 'A$' ).
tff(func_def_5,type,
'c$a': $real ).
tff(func_def_6,type,
'f$': 'Nat$' > 'A$' ).
tff(func_def_7,type,
'zero$a': 'A$' ).
tff(func_def_8,type,
'power$a': 'Nat$' > 'Nat_nat_fun$' ).
tff(func_def_9,type,
'fun_app$e': ( 'Nat_int_fun$' * 'Nat$' ) > $int ).
tff(func_def_10,type,
'n$': 'Nat$' ).
tff(func_def_11,type,
'u$': $real ).
tff(func_def_12,type,
'fun_app$': ( 'Real_real_fun$' * $real ) > $real ).
tff(func_def_13,type,
'of_nat$': 'Nat$' > $int ).
tff(func_def_14,type,
'power$': $real > 'Nat_real_fun$' ).
tff(func_def_15,type,
'c$': $real ).
tff(func_def_16,type,
'inverse$a': 'A$' > 'A$' ).
tff(func_def_17,type,
'power$c': ( 'A$' * 'Nat$' ) > 'A$' ).
tff(func_def_18,type,
'divide$': $real > 'Real_real_fun$' ).
tff(func_def_19,type,
'numeral$a': 'Num$' > $int ).
tff(func_def_20,type,
'numeral$c': 'Num$' > 'Nat$' ).
tff(func_def_21,type,
'divide$a': $int > 'Int_int_fun$' ).
tff(func_def_22,type,
'times$a': ( 'Num$' * 'Num$' ) > 'Num$' ).
tff(func_def_23,type,
'fun_app$d': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_24,type,
'times$d': ( 'A$' * 'A$' ) > 'A$' ).
tff(func_def_25,type,
'one$b': 'Nat$' ).
tff(func_def_26,type,
'numeral$': 'Num$' > $real ).
tff(func_def_27,type,
'times$c': ( $int * $int ) > $int ).
tff(func_def_28,type,
'one$': 'Num$' ).
tff(func_def_29,type,
'times$': ( $real * $real ) > $real ).
tff(func_def_30,type,
'less_eq$a': 'Nat$' > 'Nat_bool_fun$' ).
tff(func_def_31,type,
'less_eq$': 'Num$' > 'Num_bool_fun$' ).
tff(func_def_32,type,
'nat$': $int > 'Nat$' ).
tff(func_def_33,type,
'numeral$b': 'Num$' > 'A$' ).
tff(func_def_34,type,
'less$': 'Num$' > 'Num_bool_fun$' ).
tff(func_def_35,type,
'fun_app$a': ( 'Nat_real_fun$' * 'Nat$' ) > $real ).
tff(func_def_36,type,
'less$a': 'Nat$' > 'Nat_bool_fun$' ).
tff(func_def_37,type,
'l$': $real ).
tff(func_def_38,type,
'fun_app$f': ( 'Int_int_fun$' * $int ) > $int ).
tff(func_def_39,type,
'norm$a': 'A$' > $real ).
tff(func_def_40,type,
'power$b': $int > 'Nat_int_fun$' ).
tff(func_def_41,type,
'inverse$': $real > $real ).
tff(func_def_42,type,
'divide$b': 'Nat$' > 'Nat_nat_fun$' ).
tff(func_def_57,type,
sK8: $real > $real ).
tff(func_def_58,type,
sK9: $real > $real ).
tff(func_def_59,type,
sK10: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_60,type,
sK11: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_61,type,
sK12: ( $real * $real ) > $real ).
tff(func_def_62,type,
sK13: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_63,type,
sK14: ( 'Nat$' * $real ) > $real ).
tff(func_def_64,type,
sK15: ( 'Nat$' * $real ) > $real ).
tff(func_def_65,type,
sK16: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_66,type,
sK17: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_67,type,
sK18: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_68,type,
sK19: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_69,type,
sK20: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(pred_def_1,type,
'fun_app$c': ( 'Nat_bool_fun$' * 'Nat$' ) > $o ).
tff(pred_def_2,type,
'fun_app$b': ( 'Num_bool_fun$' * 'Num$' ) > $o ).
tff(pred_def_7,type,
sP0: ( $real * 'Num$' * $real ) > $o ).
tff(pred_def_8,type,
sP1: ( $real * $real * 'Num$' ) > $o ).
tff(pred_def_9,type,
sP2: ( $real * $real * $real ) > $o ).
tff(pred_def_10,type,
sP3: ( $real * $real * $real ) > $o ).
tff(pred_def_11,type,
sP4: ( $real * $real * $real ) > $o ).
tff(pred_def_12,type,
sP5: ( $real * $real * $real ) > $o ).
tff(pred_def_13,type,
sP6: ( $real * $real * 'Num$' ) > $o ).
tff(pred_def_14,type,
sP7: ( $real * 'Num$' * $real ) > $o ).
tff(f1,conjecture,
$less('times$'('fun_app$'('divide$'(1/1),2/1),'norm$'('fun_app$a'('power$'('inverse$'('c$')),'n$'))),'norm$'('fun_app$a'('power$'('inverse$'('c$')),'n$'))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture0) ).
tff(f2,negated_conjecture,
~ $less('times$'('fun_app$'('divide$'(1/1),2/1),'norm$'('fun_app$a'('power$'('inverse$'('c$')),'n$'))),'norm$'('fun_app$a'('power$'('inverse$'('c$')),'n$'))),
inference(negated_conjecture,[status(cth)],[f1]) ).
tff(f3,axiom,
$less(0/1,'c$'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom1) ).
tff(f18,axiom,
'norm$'(1/1) = 1/1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom16) ).
tff(f40,axiom,
$less(0,'of_nat$'('n$')),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom38) ).
tff(f53,axiom,
! [X0: 'Nat$'] : ( 'fun_app$a'('power$'(1/1),X0) = 1/1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom51) ).
tff(f62,axiom,
'norm$'(0/1) = 0/1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom60) ).
tff(f79,axiom,
! [X0: 'Nat$'] :
( $less(0,'of_nat$'(X0))
=> ( 'fun_app$a'('power$'(0/1),X0) = 0/1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom77) ).
tff(f120,axiom,
! [X0: $real,X1: 'Nat$'] :
( $less(0/1,X0)
=> $less(0/1,'fun_app$a'('power$'(X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom118) ).
tff(f145,axiom,
! [X0: $real,X1: $real,X2: 'Nat$'] : ( 'fun_app$a'('power$'('fun_app$'('divide$'(X0),X1)),X2) = 'fun_app$'('divide$'('fun_app$a'('power$'(X0),X2)),'fun_app$a'('power$'(X1),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom143) ).
tff(f174,axiom,
! [X0: $real,X1: 'Nat$'] : ( 'fun_app$a'('power$'('fun_app$'('divide$'(1/1),X0)),X1) = 'fun_app$'('divide$'(1/1),'fun_app$a'('power$'(X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom172) ).
tff(f176,axiom,
! [X0: $real,X1: $real] : ( 'norm$'('times$'(X0,X1)) = 'times$'('norm$'(X0),'norm$'(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom174) ).
tff(f181,axiom,
! [X0: $real] : ( 'norm$'('inverse$'(X0)) = 'inverse$'('norm$'(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom179) ).
tff(f286,axiom,
! [X0: $real,X1: $real,X2: $real] :
( ( X0 != 0/1 )
=> ( ( X1 = 'fun_app$'('divide$'(X2),X0) )
<=> ( 'times$'(X1,X0) = X2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom284) ).
tff(f309,axiom,
! [X0: $real,X1: $real] : ( 'fun_app$'('divide$'(X0),X1) = 'times$'('inverse$'(X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom307) ).
tff(f310,axiom,
! [X0: $real] : ( 'inverse$'(X0) = 'fun_app$'('divide$'(1/1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom308) ).
tff(f366,axiom,
! [X0: $real] :
( $lesseq('norm$'(X0),0/1)
<=> ( X0 = 0/1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom364) ).
tff(f420,axiom,
! [X0: $real] : $lesseq(0/1,'norm$'(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom418) ).
tff(f463,axiom,
! [X0: $real,X1: $real,X2: $real] :
( ( $lesseq(X0,X1)
& $lesseq(0/1,X2)
& $less(0/1,'times$'(X1,X0)) )
=> $lesseq('fun_app$'('divide$'(X2),X1),'fun_app$'('divide$'(X2),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom461) ).
tff(f468,axiom,
! [X0: $real,X1: $real] :
( $less('inverse$'(X0),'inverse$'(X1))
<=> ( ( $less(0/1,'times$'(X0,X1))
=> $less(X1,X0) )
& ( $lesseq('times$'(X0,X1),0/1)
=> $less(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom466) ).
tff(f471,axiom,
! [X0: $real] :
( $less('inverse$'(X0),1/1)
<=> ( $lesseq(X0,0/1)
| $less(1/1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom469) ).
tff(f524,axiom,
! [X0: $real] :
( ( X0 != 0/1 )
=> ( 'fun_app$'('divide$'(X0),X0) = 1/1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom522) ).
tff(f549,axiom,
! [X0: $real] : ( 'fun_app$'('divide$'(X0),0/1) = 0/1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom547) ).
tff(f551,axiom,
! [X0: $real] : ( 'fun_app$'('divide$'(X0),1/1) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom549) ).
tff(f559,axiom,
! [X0: $real,X1: $real] :
( ( 'times$'(X0,X1) = X0 )
<=> ( ( X0 = 0/1 )
| ( X1 = 1/1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom557) ).
tff(f612,axiom,
! [X0: $real,X1: $real] :
( ( ( X0 != X1 )
& ( $less(X0,X1)
=> $false )
& ( $less(X1,X0)
=> $false ) )
=> $false ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom610) ).
tff(f657,plain,
! [X0: $real] :
( ~ $less(0/1,'norm$'(X0))
<=> ( X0 = 0/1 ) ),
inference(theory_normalization,[],[f366]) ).
tff(f706,plain,
! [X0: $real] : ~ $less('norm$'(X0),0/1),
inference(theory_normalization,[],[f420]) ).
tff(f737,plain,
! [X0: $real,X1: $real,X2: $real] :
( ( ~ $less(X1,X0)
& ~ $less(X2,0/1)
& $less(0/1,'times$'(X1,X0)) )
=> ~ $less('fun_app$'('divide$'(X2),X0),'fun_app$'('divide$'(X2),X1)) ),
inference(theory_normalization,[],[f463]) ).
tff(f742,plain,
! [X0: $real,X1: $real] :
( $less('inverse$'(X0),'inverse$'(X1))
<=> ( ( $less(0/1,'times$'(X0,X1))
=> $less(X1,X0) )
& ( ~ $less(0/1,'times$'(X0,X1))
=> $less(X0,X1) ) ) ),
inference(theory_normalization,[],[f468]) ).
tff(f745,plain,
! [X0: $real] :
( $less('inverse$'(X0),1/1)
<=> ( ~ $less(0/1,X0)
| $less(1/1,X0) ) ),
inference(theory_normalization,[],[f471]) ).
tff(f861,plain,
~ $less('times$'('fun_app$'('divide$'(1/1),2/1),'norm$'('fun_app$a'('power$'('inverse$'('c$')),'n$'))),'norm$'('fun_app$a'('power$'('inverse$'('c$')),'n$'))),
inference(flattening,[],[f2]) ).
tff(f887,plain,
! [X0: $real,X1: $real] :
~ ( ( X0 != X1 )
& ~ $less(X0,X1)
& ~ $less(X1,X0) ),
inference(true_and_false_elimination,[],[f612]) ).
tff(f888,plain,
! [X0: $real,X1: $real] :
~ ( ( X0 != X1 )
& ~ $less(X0,X1)
& ~ $less(X1,X0) ),
inference(flattening,[],[f887]) ).
tff(f905,plain,
! [X0: 'Nat$'] :
( ( 'fun_app$a'('power$'(0/1),X0) = 0/1 )
| ~ $less(0,'of_nat$'(X0)) ),
inference(ennf_transformation,[],[f79]) ).
tff(f915,plain,
! [X0: $real,X1: 'Nat$'] :
( $less(0/1,'fun_app$a'('power$'(X0),X1))
| ~ $less(0/1,X0) ),
inference(ennf_transformation,[],[f120]) ).
tff(f1032,plain,
! [X0: $real,X1: $real,X2: $real] :
( ( ( X1 = 'fun_app$'('divide$'(X2),X0) )
<=> ( 'times$'(X1,X0) = X2 ) )
| ( 0/1 = X0 ) ),
inference(ennf_transformation,[],[f286]) ).
tff(f1207,plain,
! [X0: $real,X1: $real,X2: $real] :
( ~ $less('fun_app$'('divide$'(X2),X0),'fun_app$'('divide$'(X2),X1))
| $less(X1,X0)
| $less(X2,0/1)
| ~ $less(0/1,'times$'(X1,X0)) ),
inference(ennf_transformation,[],[f737]) ).
tff(f1208,plain,
! [X0: $real,X1: $real,X2: $real] :
( ~ $less('fun_app$'('divide$'(X2),X0),'fun_app$'('divide$'(X2),X1))
| $less(X1,X0)
| $less(X2,0/1)
| ~ $less(0/1,'times$'(X1,X0)) ),
inference(flattening,[],[f1207]) ).
tff(f1211,plain,
! [X0: $real,X1: $real] :
( $less('inverse$'(X0),'inverse$'(X1))
<=> ( ( $less(X1,X0)
| ~ $less(0/1,'times$'(X0,X1)) )
& ( $less(X0,X1)
| $less(0/1,'times$'(X0,X1)) ) ) ),
inference(ennf_transformation,[],[f742]) ).
tff(f1280,plain,
! [X0: $real] :
( ( 'fun_app$'('divide$'(X0),X0) = 1/1 )
| ( 0/1 = X0 ) ),
inference(ennf_transformation,[],[f524]) ).
tff(f1334,plain,
! [X0: $real,X1: $real] :
( ( X0 = X1 )
| $less(X0,X1)
| $less(X1,X0) ),
inference(ennf_transformation,[],[f888]) ).
tff(f1481,plain,
! [X0: $real,X1: $real,X2: $real] :
( ( ( ( X1 = 'fun_app$'('divide$'(X2),X0) )
| ( 'times$'(X1,X0) != X2 ) )
& ( ( 'times$'(X1,X0) = X2 )
| ( 'fun_app$'('divide$'(X2),X0) != X1 ) ) )
| ( 0/1 = X0 ) ),
inference(nnf_transformation,[],[f1032]) ).
tff(f1545,plain,
! [X0: $real] :
( ( ~ $less(0/1,'norm$'(X0))
| ( 0/1 != X0 ) )
& ( ( X0 = 0/1 )
| $less(0/1,'norm$'(X0)) ) ),
inference(nnf_transformation,[],[f657]) ).
tff(f1593,plain,
! [X0: $real,X1: $real] :
( ( $less('inverse$'(X0),'inverse$'(X1))
| ( ~ $less(X1,X0)
& $less(0/1,'times$'(X0,X1)) )
| ( ~ $less(X0,X1)
& ~ $less(0/1,'times$'(X0,X1)) ) )
& ( ( ( $less(X1,X0)
| ~ $less(0/1,'times$'(X0,X1)) )
& ( $less(X0,X1)
| $less(0/1,'times$'(X0,X1)) ) )
| ~ $less('inverse$'(X0),'inverse$'(X1)) ) ),
inference(nnf_transformation,[],[f1211]) ).
tff(f1594,plain,
! [X0: $real,X1: $real] :
( ( $less('inverse$'(X0),'inverse$'(X1))
| ( ~ $less(X1,X0)
& $less(0/1,'times$'(X0,X1)) )
| ( ~ $less(X0,X1)
& ~ $less(0/1,'times$'(X0,X1)) ) )
& ( ( ( $less(X1,X0)
| ~ $less(0/1,'times$'(X0,X1)) )
& ( $less(X0,X1)
| $less(0/1,'times$'(X0,X1)) ) )
| ~ $less('inverse$'(X0),'inverse$'(X1)) ) ),
inference(flattening,[],[f1593]) ).
tff(f1599,plain,
! [X0: $real] :
( ( $less('inverse$'(X0),1/1)
| ( $less(0/1,X0)
& ~ $less(1/1,X0) ) )
& ( ~ $less(0/1,X0)
| $less(1/1,X0)
| ~ $less('inverse$'(X0),1/1) ) ),
inference(nnf_transformation,[],[f745]) ).
tff(f1600,plain,
! [X0: $real] :
( ( $less('inverse$'(X0),1/1)
| ( $less(0/1,X0)
& ~ $less(1/1,X0) ) )
& ( ~ $less(0/1,X0)
| $less(1/1,X0)
| ~ $less('inverse$'(X0),1/1) ) ),
inference(flattening,[],[f1599]) ).
tff(f1645,plain,
! [X0: $real,X1: $real] :
( ( ( 'times$'(X0,X1) = X0 )
| ( ( 0/1 != X0 )
& ( 1/1 != X1 ) ) )
& ( ( X0 = 0/1 )
| ( X1 = 1/1 )
| ( 'times$'(X0,X1) != X0 ) ) ),
inference(nnf_transformation,[],[f559]) ).
tff(f1646,plain,
! [X0: $real,X1: $real] :
( ( ( 'times$'(X0,X1) = X0 )
| ( ( 0/1 != X0 )
& ( 1/1 != X1 ) ) )
& ( ( X0 = 0/1 )
| ( X1 = 1/1 )
| ( 'times$'(X0,X1) != X0 ) ) ),
inference(flattening,[],[f1645]) ).
tff(f1692,plain,
~ $less('times$'('fun_app$'('divide$'(1/1),2/1),'norm$'('fun_app$a'('power$'('inverse$'('c$')),'n$'))),'norm$'('fun_app$a'('power$'('inverse$'('c$')),'n$'))),
inference(cnf_transformation,[],[f861]) ).
tff(f1693,plain,
$less(0/1,'c$'),
inference(cnf_transformation,[],[f3]) ).
tff(f1712,plain,
1/1 = 'norm$'(1/1),
inference(cnf_transformation,[],[f18]) ).
tff(f1743,plain,
$less(0,'of_nat$'('n$')),
inference(cnf_transformation,[],[f40]) ).
tff(f1762,plain,
! [X0: 'Nat$'] : ( 1/1 = 'fun_app$a'('power$'(1/1),X0) ),
inference(cnf_transformation,[],[f53]) ).
tff(f1776,plain,
0/1 = 'norm$'(0/1),
inference(cnf_transformation,[],[f62]) ).
tff(f1815,plain,
! [X0: 'Nat$'] :
( ~ $less(0,'of_nat$'(X0))
| ( 0/1 = 'fun_app$a'('power$'(0/1),X0) ) ),
inference(cnf_transformation,[],[f905]) ).
tff(f1859,plain,
! [X0: $real,X1: 'Nat$'] :
( $less(0/1,'fun_app$a'('power$'(X0),X1))
| ~ $less(0/1,X0) ),
inference(cnf_transformation,[],[f915]) ).
tff(f1894,plain,
! [X2: 'Nat$',X0: $real,X1: $real] : ( 'fun_app$a'('power$'('fun_app$'('divide$'(X0),X1)),X2) = 'fun_app$'('divide$'('fun_app$a'('power$'(X0),X2)),'fun_app$a'('power$'(X1),X2)) ),
inference(cnf_transformation,[],[f145]) ).
tff(f1944,plain,
! [X0: $real,X1: 'Nat$'] : ( 'fun_app$a'('power$'('fun_app$'('divide$'(1/1),X0)),X1) = 'fun_app$'('divide$'(1/1),'fun_app$a'('power$'(X0),X1)) ),
inference(cnf_transformation,[],[f174]) ).
tff(f1946,plain,
! [X0: $real,X1: $real] : ( 'norm$'('times$'(X0,X1)) = 'times$'('norm$'(X0),'norm$'(X1)) ),
inference(cnf_transformation,[],[f176]) ).
tff(f1951,plain,
! [X0: $real] : ( 'norm$'('inverse$'(X0)) = 'inverse$'('norm$'(X0)) ),
inference(cnf_transformation,[],[f181]) ).
tff(f2108,plain,
! [X2: $real,X0: $real,X1: $real] :
( ( 'times$'(X1,X0) = X2 )
| ( 'fun_app$'('divide$'(X2),X0) != X1 )
| ( 0/1 = X0 ) ),
inference(cnf_transformation,[],[f1481]) ).
tff(f2149,plain,
! [X0: $real,X1: $real] : ( 'fun_app$'('divide$'(X0),X1) = 'times$'('inverse$'(X1),X0) ),
inference(cnf_transformation,[],[f309]) ).
tff(f2150,plain,
! [X0: $real] : ( 'inverse$'(X0) = 'fun_app$'('divide$'(1/1),X0) ),
inference(cnf_transformation,[],[f310]) ).
tff(f2281,plain,
! [X0: $real] :
( $less(0/1,'norm$'(X0))
| ( 0/1 = X0 ) ),
inference(cnf_transformation,[],[f1545]) ).
tff(f2362,plain,
! [X0: $real] : ~ $less('norm$'(X0),0/1),
inference(cnf_transformation,[],[f706]) ).
tff(f2422,plain,
! [X2: $real,X0: $real,X1: $real] :
( ~ $less('fun_app$'('divide$'(X2),X0),'fun_app$'('divide$'(X2),X1))
| $less(X1,X0)
| $less(X2,0/1)
| ~ $less(0/1,'times$'(X1,X0)) ),
inference(cnf_transformation,[],[f1208]) ).
tff(f2458,plain,
! [X0: $real,X1: $real] :
( $less(X0,X1)
| $less(0/1,'times$'(X0,X1))
| ~ $less('inverse$'(X0),'inverse$'(X1)) ),
inference(cnf_transformation,[],[f1594]) ).
tff(f2475,plain,
! [X0: $real] :
( $less('inverse$'(X0),1/1)
| $less(0/1,X0) ),
inference(cnf_transformation,[],[f1600]) ).
tff(f2561,plain,
! [X0: $real] :
( ( 1/1 = 'fun_app$'('divide$'(X0),X0) )
| ( 0/1 = X0 ) ),
inference(cnf_transformation,[],[f1280]) ).
tff(f2604,plain,
! [X0: $real] : ( 0/1 = 'fun_app$'('divide$'(X0),0/1) ),
inference(cnf_transformation,[],[f549]) ).
tff(f2606,plain,
! [X0: $real] : ( 'fun_app$'('divide$'(X0),1/1) = X0 ),
inference(cnf_transformation,[],[f551]) ).
tff(f2620,plain,
! [X0: $real,X1: $real] :
( ( 'times$'(X0,X1) = X0 )
| ( 1/1 != X1 ) ),
inference(cnf_transformation,[],[f1646]) ).
tff(f2721,plain,
! [X0: $real,X1: $real] :
( $less(X1,X0)
| $less(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f1334]) ).
tff(f2764,plain,
~ $less('times$'('fun_app$'('divide$'(1/1),2/1),'norm$'('fun_app$a'('power$'('fun_app$'('divide$'(1/1),'c$')),'n$'))),'norm$'('fun_app$a'('power$'('fun_app$'('divide$'(1/1),'c$')),'n$'))),
inference(definition_unfolding,[],[f1692,f2150,f2150]) ).
tff(f2841,plain,
! [X0: $real] : ( 'norm$'('fun_app$'('divide$'(1/1),X0)) = 'fun_app$'('divide$'(1/1),'norm$'(X0)) ),
inference(definition_unfolding,[],[f1951,f2150,f2150]) ).
tff(f2883,plain,
! [X0: $real,X1: $real] : ( 'fun_app$'('divide$'(X0),X1) = 'times$'('fun_app$'('divide$'(1/1),X1),X0) ),
inference(definition_unfolding,[],[f2149,f2150]) ).
tff(f2923,plain,
! [X0: $real,X1: $real] :
( ~ $less('fun_app$'('divide$'(1/1),X0),'fun_app$'('divide$'(1/1),X1))
| $less(0/1,'times$'(X0,X1))
| $less(X0,X1) ),
inference(definition_unfolding,[],[f2458,f2150,f2150]) ).
tff(f2933,plain,
! [X0: $real] :
( $less('fun_app$'('divide$'(1/1),X0),1/1)
| $less(0/1,X0) ),
inference(definition_unfolding,[],[f2475,f2150]) ).
tff(f3045,plain,
! [X2: $real,X0: $real] :
( ( 'times$'('fun_app$'('divide$'(X2),X0),X0) = X2 )
| ( 0/1 = X0 ) ),
inference(equality_resolution,[],[f2108]) ).
tff(f3086,plain,
! [X0: $real] : ( 'times$'(X0,1/1) = X0 ),
inference(equality_resolution,[],[f2620]) ).
tff(f3161,plain,
~ $less('times$'('fun_app$'('divide$'(1/1),2/1),'norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$')))),'norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$')))),
inference(forward_demodulation,[],[f2764,f1944]) ).
tff(f3166,plain,
~ $less('fun_app$'('divide$'('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$')))),2/1),'norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$')))),
inference(forward_demodulation,[],[f3161,f2883]) ).
tff(f3458,plain,
( $less('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))),'fun_app$'('divide$'('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$')))),2/1))
| ( 'norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))) = 'fun_app$'('divide$'('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$')))),2/1) ) ),
inference(resolution,[],[f2721,f3166]) ).
tff(f3478,definition,
( spl21_3
<=> ( 'norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))) = 'fun_app$'('divide$'('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$')))),2/1) ) ),
introduced(definition,[new_symbols(definition,[spl21_3])],[avatar_definition]) ).
tff(f3480,plain,
( ( 'norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))) = 'fun_app$'('divide$'('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$')))),2/1) )
| ~ spl21_3 ),
inference(avatar_component_clause,[],[f3478]) ).
tff(f3482,definition,
( spl21_4
<=> $less('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))),'fun_app$'('divide$'('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$')))),2/1)) ),
introduced(definition,[new_symbols(definition,[spl21_4])],[avatar_definition]) ).
tff(f3484,plain,
( $less('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))),'fun_app$'('divide$'('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$')))),2/1))
| ~ spl21_4 ),
inference(avatar_component_clause,[],[f3482]) ).
tff(f3486,plain,
( spl21_3
| spl21_4 ),
inference(avatar_split_clause,[],[f3458,f3482,f3478]) ).
tff(f3667,plain,
0/1 = 'fun_app$a'('power$'(0/1),'n$'),
inference(resolution,[],[f1815,f1743]) ).
tff(f4398,plain,
! [X0: $real,X1: $real] : ( 'fun_app$'('divide$'(X1),'norm$'(X0)) = 'times$'('norm$'('fun_app$'('divide$'(1/1),X0)),X1) ),
inference(superposition,[],[f2883,f2841]) ).
tff(f4488,plain,
( ( 'norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))) = 'times$'('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))),2/1) )
| ( 2/1 = 0/1 )
| ~ spl21_3 ),
inference(superposition,[],[f3045,f3480]) ).
tff(f4510,plain,
( ( 'norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))) = 'times$'('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))),2/1) )
| ~ spl21_3 ),
inference(evaluation,[],[f4488]) ).
tff(f4520,plain,
( ( 'norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))) = 'fun_app$'('divide$'(2/1),'norm$'('fun_app$a'('power$'('c$'),'n$'))) )
| ~ spl21_3 ),
inference(forward_demodulation,[],[f4510,f4398]) ).
tff(f4543,plain,
( ( 2/1 = 'times$'('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))),'norm$'('fun_app$a'('power$'('c$'),'n$'))) )
| ( 0/1 = 'norm$'('fun_app$a'('power$'('c$'),'n$')) )
| ~ spl21_3 ),
inference(superposition,[],[f3045,f4520]) ).
tff(f4547,plain,
( ( 2/1 = 'norm$'('times$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$')),'fun_app$a'('power$'('c$'),'n$'))) )
| ( 0/1 = 'norm$'('fun_app$a'('power$'('c$'),'n$')) )
| ~ spl21_3 ),
inference(forward_demodulation,[],[f4543,f1946]) ).
tff(f4548,plain,
( ( 2/1 = 'norm$'('fun_app$'('divide$'('fun_app$a'('power$'('c$'),'n$')),'fun_app$a'('power$'('c$'),'n$'))) )
| ( 0/1 = 'norm$'('fun_app$a'('power$'('c$'),'n$')) )
| ~ spl21_3 ),
inference(forward_demodulation,[],[f4547,f2883]) ).
tff(f4549,plain,
( ( 2/1 = 'norm$'('fun_app$a'('power$'('fun_app$'('divide$'('c$'),'c$')),'n$')) )
| ( 0/1 = 'norm$'('fun_app$a'('power$'('c$'),'n$')) )
| ~ spl21_3 ),
inference(forward_demodulation,[],[f4548,f1894]) ).
tff(f4551,definition,
( spl21_17
<=> ( 0/1 = 'norm$'('fun_app$a'('power$'('c$'),'n$')) ) ),
introduced(definition,[new_symbols(definition,[spl21_17])],[avatar_definition]) ).
tff(f4553,plain,
( ( 0/1 = 'norm$'('fun_app$a'('power$'('c$'),'n$')) )
| ~ spl21_17 ),
inference(avatar_component_clause,[],[f4551]) ).
tff(f4555,definition,
( spl21_18
<=> ( 2/1 = 'norm$'('fun_app$a'('power$'('fun_app$'('divide$'('c$'),'c$')),'n$')) ) ),
introduced(definition,[new_symbols(definition,[spl21_18])],[avatar_definition]) ).
tff(f4557,plain,
( ( 2/1 = 'norm$'('fun_app$a'('power$'('fun_app$'('divide$'('c$'),'c$')),'n$')) )
| ~ spl21_18 ),
inference(avatar_component_clause,[],[f4555]) ).
tff(f5349,plain,
( spl21_17
| spl21_18
| ~ spl21_3 ),
inference(avatar_split_clause,[],[f4549,f3478,f4555,f4551]) ).
tff(f5419,plain,
( $less(0/1,0/1)
| ( 0/1 = 'fun_app$a'('power$'('c$'),'n$') )
| ~ spl21_17 ),
inference(superposition,[],[f2281,f4553]) ).
tff(f5425,plain,
( ( 0/1 = 'fun_app$a'('power$'('c$'),'n$') )
| ~ spl21_17 ),
inference(evaluation,[],[f5419]) ).
tff(f5602,plain,
( $less(0/1,0/1)
| ~ $less(0/1,'c$')
| ~ spl21_17 ),
inference(superposition,[],[f1859,f5425]) ).
tff(f5609,plain,
( ~ $less(0/1,'c$')
| ~ spl21_17 ),
inference(evaluation,[],[f5602]) ).
tff(f5615,plain,
( $false
| ~ spl21_17 ),
inference(forward_subsumption_resolution,[],[f5609,f1693]) ).
tff(f5616,plain,
~ spl21_17,
inference(avatar_contradiction_clause,[],[f5615]) ).
tff(f6013,plain,
( ( 2/1 = 'norm$'('fun_app$a'('power$'(1/1),'n$')) )
| ( 'c$' = 0/1 )
| ~ spl21_18 ),
inference(superposition,[],[f4557,f2561]) ).
tff(f6028,plain,
( ( 2/1 = 'norm$'(1/1) )
| ( 'c$' = 0/1 )
| ~ spl21_18 ),
inference(forward_demodulation,[],[f6013,f1762]) ).
tff(f6030,plain,
( ( 1/1 = 2/1 )
| ( 'c$' = 0/1 )
| ~ spl21_18 ),
inference(forward_demodulation,[],[f6028,f1712]) ).
tff(f6031,plain,
( ( 'c$' = 0/1 )
| ~ spl21_18 ),
inference(evaluation,[],[f6030]) ).
tff(f6360,plain,
( ( 2/1 = 'norm$'('fun_app$a'('power$'('fun_app$'('divide$'(0/1),0/1)),'n$')) )
| ~ spl21_18 ),
inference(superposition,[],[f4557,f6031]) ).
tff(f6365,plain,
( ( 2/1 = 'norm$'('fun_app$a'('power$'(0/1),'n$')) )
| ~ spl21_18 ),
inference(forward_demodulation,[],[f6360,f2604]) ).
tff(f6370,plain,
( ( 2/1 = 'norm$'(0/1) )
| ~ spl21_18 ),
inference(forward_demodulation,[],[f6365,f3667]) ).
tff(f6376,plain,
( ( 2/1 = 0/1 )
| ~ spl21_18 ),
inference(forward_demodulation,[],[f6370,f1776]) ).
tff(f6377,plain,
( $false
| ~ spl21_18 ),
inference(evaluation,[],[f6376]) ).
tff(f6378,plain,
~ spl21_18,
inference(avatar_contradiction_clause,[],[f6377]) ).
tff(f14135,plain,
! [X0: $real] :
( ~ $less('fun_app$'('divide$'(1/1),X0),1/1)
| $less(0/1,'times$'(X0,1/1))
| $less(X0,1/1) ),
inference(superposition,[],[f2923,f2606]) ).
tff(f14144,plain,
! [X0: $real] :
( $less(0/1,X0)
| ~ $less('fun_app$'('divide$'(1/1),X0),1/1)
| $less(X0,1/1) ),
inference(forward_demodulation,[],[f14135,f3086]) ).
tff(f15380,plain,
! [X0: $real] :
( $less(0/1,X0)
| $less(X0,1/1) ),
inference(forward_subsumption_resolution,[],[f14144,f2933]) ).
tff(f18412,plain,
! [X0: $real,X1: $real] :
( ~ $less(X0,'fun_app$'('divide$'(X0),X1))
| $less(X1,1/1)
| $less(X0,0/1)
| ~ $less(0/1,'times$'(X1,1/1)) ),
inference(superposition,[],[f2422,f2606]) ).
tff(f18489,plain,
! [X0: $real,X1: $real] :
( ~ $less(0/1,X1)
| ~ $less(X0,'fun_app$'('divide$'(X0),X1))
| $less(X1,1/1)
| $less(X0,0/1) ),
inference(forward_demodulation,[],[f18412,f3086]) ).
tff(f18502,plain,
! [X0: $real,X1: $real] :
( ~ $less(X0,'fun_app$'('divide$'(X0),X1))
| $less(X1,1/1)
| $less(X0,0/1) ),
inference(forward_subsumption_resolution,[],[f18489,f15380]) ).
tff(f41271,plain,
( $less(2/1,1/1)
| $less('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))),0/1)
| ~ spl21_4 ),
inference(resolution,[],[f18502,f3484]) ).
tff(f41333,plain,
( $less('norm$'('fun_app$'('divide$'(1/1),'fun_app$a'('power$'('c$'),'n$'))),0/1)
| ~ spl21_4 ),
inference(evaluation,[],[f41271]) ).
tff(f41345,plain,
( $false
| ~ spl21_4 ),
inference(forward_subsumption_resolution,[],[f41333,f2362]) ).
tff(f41346,plain,
~ spl21_4,
inference(avatar_contradiction_clause,[],[f41345]) ).
cnf(s732,plain,
( spl21_3
| spl21_4 ),
inference(sat_conversion,[],[f3486]) ).
cnf(s1213,plain,
( ~ spl21_3
| spl21_17
| spl21_18 ),
inference(sat_conversion,[],[f5349]) ).
cnf(s1244,plain,
~ spl21_17,
inference(sat_conversion,[],[f5616]) ).
cnf(s1454,plain,
~ spl21_18,
inference(sat_conversion,[],[f6378]) ).
cnf(s11910,plain,
~ spl21_4,
inference(sat_conversion,[],[f41346]) ).
cnf(s11946,plain,
~ spl21_3,
inference(rat,[],[s1213,s1454,s1244]) ).
cnf(s11949,plain,
$false,
inference(rat,[],[s732,s11910,s11946]) ).
tff(f41358,plain,
$false,
inference(avatar_sat_refutation,[],[s11949]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP352_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.15/0.42 % Computer : n007.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sun Sep 27 12:53:24 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.21/0.48 Running first-order model finding
% 0.21/0.48 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.69/1.39 % (1392234)Will run a generic schedule for satisfiability detection.
% 5.69/1.39 % (1392239)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2597311429_2999 on theBenchmark for (2999ds/0Mi)
% 5.69/1.39 % (1392240)% WARNING: option uhcvi not known.
% 5.69/1.39 % (1392244)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3000796652:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.69/1.39 % (1392240)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3524764898:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.69/1.39 % (1392241)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3591617354:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.69/1.39 % (1392242)dis+10_1_sil=32000:sp=arity:random_seed=1821131553:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.69/1.39 % (1392243)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1151941616:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.69/1.39 % (1392245)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2214809272:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.69/1.39 % (1392239)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.69/1.39 % (1392239)Terminated due to inappropriate strategy.
% 5.69/1.39 % (1392239)------------------------------
% 5.69/1.39 % (1392239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.39 % (1392239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.39 % (1392239)CaDiCaL version: 2.1.3
% 5.69/1.39 % (1392239)Termination reason: Inappropriate
% 5.69/1.39 % (1392239)Time elapsed: 0.029 s
% 5.69/1.39 % (1392239)Peak memory usage: 12 MB
% 5.69/1.39 % (1392239)Instructions burned: 59 (million)
% 5.69/1.39 % (1392239)------------------------------
% 5.69/1.39 % (1392239)------------------------------
% 5.69/1.39 % (1392253)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4188658021:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.69/1.39 % (1392253)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.69/1.39 % (1392253)Terminated due to inappropriate strategy.
% 5.69/1.39 % (1392253)------------------------------
% 5.69/1.39 % (1392253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.39 % (1392253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.39 % (1392253)CaDiCaL version: 2.1.3
% 5.69/1.39 % (1392253)Termination reason: Inappropriate
% 5.69/1.39 % (1392253)Time elapsed: 0.028 s
% 5.69/1.39 % (1392253)Peak memory usage: 12 MB
% 5.69/1.39 % (1392253)Instructions burned: 58 (million)
% 5.69/1.39 % (1392253)------------------------------
% 5.69/1.39 % (1392253)------------------------------
% 5.69/1.39 % (1392255)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=627133826:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.69/1.39 % (1392242)Instruction limit reached!
% 5.69/1.39 % (1392242)------------------------------
% 5.69/1.39 % (1392242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.39 % (1392242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.39 % (1392242)CaDiCaL version: 2.1.3
% 5.69/1.39 % (1392242)Termination reason: Instruction limit
% 5.69/1.39 % (1392242)Termination phase: Saturation
% 5.69/1.39 % (1392242)Time elapsed: 0.101 s
% 5.69/1.39 % (1392242)Peak memory usage: 13 MB
% 5.69/1.39 % (1392242)Instructions burned: 103 (million)
% 5.69/1.39 % (1392243)Instruction limit reached!
% 5.69/1.39 % (1392243)------------------------------
% 5.69/1.39 % (1392243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.39 % (1392243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.39 % (1392243)CaDiCaL version: 2.1.3
% 5.69/1.39 % (1392243)Termination reason: Instruction limit
% 5.69/1.39 % (1392243)Termination phase: Saturation
% 5.69/1.39 % (1392243)Time elapsed: 0.109 s
% 5.69/1.39 % (1392243)Peak memory usage: 13 MB
% 5.69/1.39 % (1392243)Instructions burned: 116 (million)
% 5.69/1.39 % (1392244)Instruction limit reached!
% 5.69/1.39 % (1392244)------------------------------
% 5.69/1.39 % (1392244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.39 % (1392244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.39 % (1392244)CaDiCaL version: 2.1.3
% 5.69/1.39 % (1392244)Termination reason: Instruction limit
% 8.38/2.03 % (1392244)Termination phase: Saturation
% 8.38/2.03 % (1392244)Time elapsed: 0.116 s
% 8.38/2.03 % (1392244)Peak memory usage: 14 MB
% 8.38/2.03 % (1392244)Instructions burned: 131 (million)
% 8.38/2.03 % (1392257)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=3709884005:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.38/2.03 % (1392258)ott-21_1_sil=16000:fs=off:random_seed=3910634758:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.38/2.03 % (1392259)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4078770722:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.38/2.03 % (1392245)Instruction limit reached!
% 8.38/2.03 % (1392245)------------------------------
% 8.38/2.03 % (1392245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/2.03 % (1392245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/2.03 % (1392245)CaDiCaL version: 2.1.3
% 8.38/2.03 % (1392245)Termination reason: Instruction limit
% 8.38/2.03 % (1392245)Termination phase: Saturation
% 8.38/2.03 % (1392245)Time elapsed: 0.161 s
% 8.38/2.03 % (1392245)Peak memory usage: 14 MB
% 8.38/2.03 % (1392245)Instructions burned: 159 (million)
% 8.38/2.03 % (1392255)Instruction limit reached!
% 8.38/2.03 % (1392255)------------------------------
% 8.38/2.03 % (1392255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/2.03 % (1392255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/2.03 % (1392255)CaDiCaL version: 2.1.3
% 8.38/2.03 % (1392255)Termination reason: Instruction limit
% 8.38/2.03 % (1392255)Termination phase: Saturation
% 8.38/2.03 % (1392255)Time elapsed: 0.071 s
% 8.38/2.03 % (1392255)Peak memory usage: 14 MB
% 8.38/2.03 % (1392255)Instructions burned: 135 (million)
% 8.38/2.03 % (1392263)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1233440425:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.38/2.03 % (1392264)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2215060307:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 8.38/2.03 % (1392263)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.38/2.03 % (1392263)Terminated due to inappropriate strategy.
% 8.38/2.03 % (1392263)------------------------------
% 8.38/2.03 % (1392263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/2.03 % (1392263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/2.03 % (1392263)CaDiCaL version: 2.1.3
% 8.38/2.03 % (1392263)Termination reason: Inappropriate
% 8.38/2.03 % (1392263)Time elapsed: 0.029 s
% 8.38/2.03 % (1392263)Peak memory usage: 12 MB
% 8.38/2.03 % (1392263)Instructions burned: 55 (million)
% 8.38/2.03 % (1392263)------------------------------
% 8.38/2.03 % (1392263)------------------------------
% 8.38/2.03 % (1392267)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1754085803:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 8.38/2.03 % (1392267)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.38/2.03 % (1392267)Terminated due to inappropriate strategy.
% 8.38/2.03 % (1392267)------------------------------
% 8.38/2.03 % (1392267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/2.03 % (1392267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/2.03 % (1392267)CaDiCaL version: 2.1.3
% 8.38/2.03 % (1392267)Termination reason: Inappropriate
% 8.38/2.03 % (1392267)Time elapsed: 0.029 s
% 8.38/2.03 % (1392267)Peak memory usage: 12 MB
% 8.38/2.03 % (1392267)Instructions burned: 57 (million)
% 8.38/2.03 % (1392267)------------------------------
% 8.38/2.03 % (1392267)------------------------------
% 8.38/2.03 % (1392269)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=1389040215:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 8.38/2.03 % (1392258)Instruction limit reached!
% 8.38/2.03 % (1392258)------------------------------
% 8.38/2.03 % (1392258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.38/2.03 % (1392258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.38/2.03 % (1392258)CaDiCaL version: 2.1.3
% 8.38/2.03 % (1392258)Termination reason: Instruction limit
% 8.38/2.03 % (1392258)Termination phase: Saturation
% 35.73/5.62 % (1392258)Time elapsed: 0.164 s
% 35.73/5.62 % (1392258)Peak memory usage: 13 MB
% 35.73/5.62 % (1392258)Instructions burned: 180 (million)
% 35.73/5.62 % (1392271)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2807266535:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 35.73/5.62 % (1392259)Instruction limit reached!
% 35.73/5.62 % (1392259)------------------------------
% 35.73/5.62 % (1392259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.73/5.62 % (1392259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.73/5.62 % (1392259)CaDiCaL version: 2.1.3
% 35.73/5.62 % (1392259)Termination reason: Instruction limit
% 35.73/5.62 % (1392259)Termination phase: Saturation
% 35.73/5.62 % (1392259)Time elapsed: 0.532 s
% 35.73/5.62 % (1392259)Peak memory usage: 16 MB
% 35.73/5.62 % (1392259)Instructions burned: 477 (million)
% 35.73/5.62 % (1392273)fmb+10_1_sil=64000:random_seed=4009799946:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 35.73/5.62 % (1392269)Instruction limit reached!
% 35.73/5.62 % (1392269)------------------------------
% 35.73/5.62 % (1392269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.73/5.62 % (1392269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.73/5.62 % (1392269)CaDiCaL version: 2.1.3
% 35.73/5.62 % (1392269)Termination reason: Instruction limit
% 35.73/5.62 % (1392269)Termination phase: Saturation
% 35.73/5.62 % (1392269)Time elapsed: 0.412 s
% 35.73/5.62 % (1392269)Peak memory usage: 21 MB
% 35.73/5.62 % (1392269)Instructions burned: 692 (million)
% 35.73/5.62 % (1392275)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2763240096:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 35.73/5.62 % (1392273)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 35.73/5.62 % (1392273)Terminated due to inappropriate strategy.
% 35.73/5.62 % (1392273)------------------------------
% 35.73/5.62 % (1392273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.73/5.62 % (1392273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.73/5.62 % (1392273)CaDiCaL version: 2.1.3
% 35.73/5.62 % (1392273)Termination reason: Inappropriate
% 35.73/5.62 % (1392273)Time elapsed: 0.033 s
% 35.73/5.62 % (1392273)Peak memory usage: 12 MB
% 35.73/5.62 % (1392273)Instructions burned: 62 (million)
% 35.73/5.62 % (1392273)------------------------------
% 35.73/5.62 % (1392273)------------------------------
% 35.73/5.62 % (1392275)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 35.73/5.62 % (1392275)Terminated due to inappropriate strategy.
% 35.73/5.62 % (1392275)------------------------------
% 35.73/5.62 % (1392275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.73/5.62 % (1392275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.73/5.62 % (1392275)CaDiCaL version: 2.1.3
% 35.73/5.62 % (1392275)Termination reason: Inappropriate
% 35.73/5.62 % (1392275)Time elapsed: 0.027 s
% 35.73/5.62 % (1392275)Peak memory usage: 12 MB
% 35.73/5.62 % (1392275)Instructions burned: 57 (million)
% 35.73/5.62 % (1392275)------------------------------
% 35.73/5.62 % (1392275)------------------------------
% 35.73/5.62 % (1392257)Instruction limit reached!
% 35.73/5.62 % (1392257)------------------------------
% 35.73/5.62 % (1392257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.73/5.62 % (1392257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.73/5.62 % (1392257)CaDiCaL version: 2.1.3
% 35.73/5.62 % (1392257)Termination reason: Instruction limit
% 35.73/5.62 % (1392257)Termination phase: Saturation
% 35.73/5.62 % (1392257)Time elapsed: 0.642 s
% 35.73/5.62 % (1392257)Peak memory usage: 19 MB
% 35.73/5.62 % (1392257)Instructions burned: 684 (million)
% 35.73/5.62 % (1392277)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1592672423:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 35.73/5.62 % (1392278)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1242794781:i=5131_2991 on theBenchmark for (2991ds/5131Mi)
% 35.73/5.62 % (1392279)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2147932270:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 35.73/5.62 % (1392277)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 35.73/5.62 % (1392277)Terminated due to inappropriate strategy.
% 35.73/5.62 % (1392277)------------------------------
% 40.51/6.24 % (1392277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.51/6.24 % (1392277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.51/6.24 % (1392277)CaDiCaL version: 2.1.3
% 40.51/6.24 % (1392277)Termination reason: Inappropriate
% 40.51/6.24 % (1392277)Time elapsed: 0.051 s
% 40.51/6.24 % (1392277)Peak memory usage: 12 MB
% 40.51/6.24 % (1392277)Instructions burned: 56 (million)
% 40.51/6.24 % (1392277)------------------------------
% 40.51/6.24 % (1392277)------------------------------
% 40.51/6.24 % (1392283)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2098471833:i=6324_2990 on theBenchmark for (2990ds/6324Mi)
% 40.51/6.24 % (1392283)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 40.51/6.24 % (1392283)Terminated due to inappropriate strategy.
% 40.51/6.24 % (1392283)------------------------------
% 40.51/6.24 % (1392283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.51/6.24 % (1392283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.51/6.24 % (1392283)CaDiCaL version: 2.1.3
% 40.51/6.24 % (1392283)Termination reason: Inappropriate
% 40.51/6.24 % (1392283)Time elapsed: 0.061 s
% 40.51/6.24 % (1392283)Peak memory usage: 12 MB
% 40.51/6.24 % (1392283)Instructions burned: 59 (million)
% 40.51/6.24 % (1392283)------------------------------
% 40.51/6.24 % (1392283)------------------------------
% 40.51/6.24 % (1392285)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=403293241:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi)
% 40.51/6.24 % (1392285)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 40.51/6.24 % (1392285)Terminated due to inappropriate strategy.
% 40.51/6.24 % (1392285)------------------------------
% 40.51/6.24 % (1392285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.51/6.24 % (1392285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.51/6.24 % (1392285)CaDiCaL version: 2.1.3
% 40.51/6.24 % (1392285)Termination reason: Inappropriate
% 40.51/6.24 % (1392285)Time elapsed: 0.053 s
% 40.51/6.24 % (1392285)Peak memory usage: 12 MB
% 40.51/6.24 % (1392285)Instructions burned: 56 (million)
% 40.51/6.24 % (1392285)------------------------------
% 40.51/6.24 % (1392285)------------------------------
% 40.51/6.24 % (1392287)ott-2_1_sil=16000:newcnf=on:random_seed=3438268146:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi)
% 40.51/6.24 % (1392271)Instruction limit reached!
% 40.51/6.24 % (1392271)------------------------------
% 40.51/6.24 % (1392271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.51/6.24 % (1392271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.51/6.24 % (1392271)CaDiCaL version: 2.1.3
% 40.51/6.24 % (1392271)Termination reason: Instruction limit
% 40.51/6.24 % (1392271)Termination phase: Saturation
% 40.51/6.24 % (1392271)Time elapsed: 0.823 s
% 40.51/6.24 % (1392271)Peak memory usage: 19 MB
% 40.51/6.24 % (1392271)Instructions burned: 879 (million)
% 40.51/6.24 % (1392289)ott+10_1_sil=32000:tgt=ground:random_seed=2227942139:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi)
% 40.51/6.24 % (1392264)Instruction limit reached!
% 40.51/6.24 % (1392264)------------------------------
% 40.51/6.24 % (1392264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.51/6.24 % (1392264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.51/6.24 % (1392264)CaDiCaL version: 2.1.3
% 40.51/6.24 % (1392264)Termination reason: Instruction limit
% 40.51/6.24 % (1392264)Termination phase: Saturation
% 40.51/6.24 % (1392264)Time elapsed: 1.189 s
% 40.51/6.24 % (1392264)Peak memory usage: 20 MB
% 40.51/6.24 % (1392264)Instructions burned: 1179 (million)
% 40.51/6.24 % (1392291)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3718168062:i=54282_2985 on theBenchmark for (2985ds/54282Mi)
% 40.51/6.24 % (1392291)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 40.51/6.24 % (1392291)Terminated due to inappropriate strategy.
% 40.51/6.24 % (1392291)------------------------------
% 40.51/6.24 % (1392291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.51/6.24 % (1392291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.51/6.24 % (1392291)CaDiCaL version: 2.1.3
% 40.51/6.24 % (1392291)Termination reason: Inappropriate
% 40.51/6.24 % (1392291)Time elapsed: 0.047 s
% 40.51/6.24 % (1392291)Peak memory usage: 12 MB
% 40.51/6.24 % (1392291)Instructions burned: 59 (million)
% 69.84/13.82 % (1392291)------------------------------
% 69.84/13.82 % (1392291)------------------------------
% 69.84/13.82 % (1392293)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=468222011:i=3512:aac=none_2984 on theBenchmark for (2984ds/3512Mi)
% 69.84/13.82 % (1392287)Instruction limit reached!
% 69.84/13.82 % (1392287)------------------------------
% 69.84/13.82 % (1392287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.82 % (1392287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.82 % (1392287)CaDiCaL version: 2.1.3
% 69.84/13.82 % (1392287)Termination reason: Instruction limit
% 69.84/13.82 % (1392287)Termination phase: Saturation
% 69.84/13.82 % (1392287)Time elapsed: 0.696 s
% 69.84/13.82 % (1392287)Peak memory usage: 16 MB
% 69.84/13.82 % (1392287)Instructions burned: 871 (million)
% 69.84/13.82 % (1392295)dis+21_1_sil=32000:sas=cadical:random_seed=4186799588:i=3773:amm=off_2981 on theBenchmark for (2981ds/3773Mi)
% 69.84/13.82 % (1392279)Instruction limit reached!
% 69.84/13.82 % (1392279)------------------------------
% 69.84/13.82 % (1392279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392279)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392279)Termination reason: Instruction limit
% 69.84/13.83 % (1392279)Termination phase: Saturation
% 69.84/13.83 % (1392279)Time elapsed: 1.337 s
% 69.84/13.83 % (1392279)Peak memory usage: 27 MB
% 69.84/13.83 % (1392279)Instructions burned: 1472 (million)
% 69.84/13.83 % (1392297)ott+11_1_sil=16000:gs=on:random_seed=484778673:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2977 on theBenchmark for (2977ds/2251Mi)
% 69.84/13.83 % (1392278)Instruction limit reached!
% 69.84/13.83 % (1392278)------------------------------
% 69.84/13.83 % (1392278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392278)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392278)Termination reason: Instruction limit
% 69.84/13.83 % (1392278)Termination phase: Saturation
% 69.84/13.83 % (1392278)Time elapsed: 2.457 s
% 69.84/13.83 % (1392278)Peak memory usage: 36 MB
% 69.84/13.83 % (1392278)Instructions burned: 5132 (million)
% 69.84/13.83 % (1392303)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2508520816:fmbsr=1.6:i=67534_2966 on theBenchmark for (2966ds/67534Mi)
% 69.84/13.83 % (1392303)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 69.84/13.83 % (1392303)Terminated due to inappropriate strategy.
% 69.84/13.83 % (1392303)------------------------------
% 69.84/13.83 % (1392303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392303)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392303)Termination reason: Inappropriate
% 69.84/13.83 % (1392303)Time elapsed: 0.035 s
% 69.84/13.83 % (1392303)Peak memory usage: 12 MB
% 69.84/13.83 % (1392303)Instructions burned: 56 (million)
% 69.84/13.83 % (1392303)------------------------------
% 69.84/13.83 % (1392303)------------------------------
% 69.84/13.83 % (1392305)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1199212609:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2966 on theBenchmark for (2966ds/4591Mi)
% 69.84/13.83 % (1392297)Instruction limit reached!
% 69.84/13.83 % (1392297)------------------------------
% 69.84/13.83 % (1392297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392297)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392297)Termination reason: Instruction limit
% 69.84/13.83 % (1392297)Termination phase: Saturation
% 69.84/13.83 % (1392297)Time elapsed: 2.362 s
% 69.84/13.83 % (1392297)Peak memory usage: 27 MB
% 69.84/13.83 % (1392297)Instructions burned: 2251 (million)
% 69.84/13.83 % (1392308)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2075322275:i=29340_2953 on theBenchmark for (2953ds/29340Mi)
% 69.84/13.83 % (1392293)Instruction limit reached!
% 69.84/13.83 % (1392293)------------------------------
% 69.84/13.83 % (1392293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392293)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392293)Termination reason: Instruction limit
% 69.84/13.83 % (1392293)Termination phase: Saturation
% 69.84/13.83 % (1392293)Time elapsed: 3.546 s
% 69.84/13.83 % (1392293)Peak memory usage: 34 MB
% 69.84/13.83 % (1392293)Instructions burned: 3514 (million)
% 69.84/13.83 % (1392310)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3812749141:i=5211_2948 on theBenchmark for (2948ds/5211Mi)
% 69.84/13.83 % (1392295)Instruction limit reached!
% 69.84/13.83 % (1392295)------------------------------
% 69.84/13.83 % (1392295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392295)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392295)Termination reason: Instruction limit
% 69.84/13.83 % (1392295)Termination phase: Saturation
% 69.84/13.83 % (1392295)Time elapsed: 3.672 s
% 69.84/13.83 % (1392295)Peak memory usage: 35 MB
% 69.84/13.83 % (1392295)Instructions burned: 3774 (million)
% 69.84/13.83 % (1392312)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1329263415:i=5497:nm=2_2944 on theBenchmark for (2944ds/5497Mi)
% 69.84/13.83 % (1392305)Instruction limit reached!
% 69.84/13.83 % (1392305)------------------------------
% 69.84/13.83 % (1392305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392305)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392305)Termination reason: Instruction limit
% 69.84/13.83 % (1392305)Termination phase: Saturation
% 69.84/13.83 % (1392305)Time elapsed: 2.230 s
% 69.84/13.83 % (1392305)Peak memory usage: 40 MB
% 69.84/13.83 % (1392305)Instructions burned: 4592 (million)
% 69.84/13.83 % (1392312)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 69.84/13.83 % (1392312)Terminated due to inappropriate strategy.
% 69.84/13.83 % (1392312)------------------------------
% 69.84/13.83 % (1392312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392312)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392312)Termination reason: Inappropriate
% 69.84/13.83 % (1392312)Time elapsed: 0.041 s
% 69.84/13.83 % (1392312)Peak memory usage: 12 MB
% 69.84/13.83 % (1392312)Instructions burned: 63 (million)
% 69.84/13.83 % (1392312)------------------------------
% 69.84/13.83 % (1392312)------------------------------
% 69.84/13.83 % (1392314)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1417237944:fmbsr=2:i=46332_2943 on theBenchmark for (2943ds/46332Mi)
% 69.84/13.83 % (1392315)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4098460949:i=14071_2943 on theBenchmark for (2943ds/14071Mi)
% 69.84/13.83 % (1392315)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 69.84/13.83 % (1392315)Terminated due to inappropriate strategy.
% 69.84/13.83 % (1392315)------------------------------
% 69.84/13.83 % (1392315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392315)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392315)Termination reason: Inappropriate
% 69.84/13.83 % (1392315)Time elapsed: 0.026 s
% 69.84/13.83 % (1392315)Peak memory usage: 12 MB
% 69.84/13.83 % (1392315)Instructions burned: 56 (million)
% 69.84/13.83 % (1392315)------------------------------
% 69.84/13.83 % (1392315)------------------------------
% 69.84/13.83 % (1392314)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 69.84/13.83 % (1392314)Terminated due to inappropriate strategy.
% 69.84/13.83 % (1392314)------------------------------
% 69.84/13.83 % (1392314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392314)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392314)Termination reason: Inappropriate
% 69.84/13.83 % (1392314)Time elapsed: 0.031 s
% 69.84/13.83 % (1392314)Peak memory usage: 12 MB
% 69.84/13.83 % (1392314)Instructions burned: 56 (million)
% 69.84/13.83 % (1392314)------------------------------
% 69.84/13.83 % (1392314)------------------------------
% 69.84/13.83 % (1392318)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3878993491:i=22565:add=on:rawr=on_2942 on theBenchmark for (2942ds/22565Mi)
% 69.84/13.83 % (1392319)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3540543678:i=8173:av=off_2942 on theBenchmark for (2942ds/8173Mi)
% 69.84/13.83 % (1392289)Instruction limit reached!
% 69.84/13.83 % (1392289)------------------------------
% 69.84/13.83 % (1392289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392289)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392289)Termination reason: Instruction limit
% 69.84/13.83 % (1392289)Termination phase: Saturation
% 69.84/13.83 % (1392289)Time elapsed: 5.442 s
% 69.84/13.83 % (1392289)Peak memory usage: 33 MB
% 69.84/13.83 % (1392289)Instructions burned: 5114 (million)
% 69.84/13.83 % (1392324)dis+10_16:1_sil=16000:random_seed=408464418:i=9155:fsr=off_2932 on theBenchmark for (2932ds/9155Mi)
% 69.84/13.83 % (1392310)Instruction limit reached!
% 69.84/13.83 % (1392310)------------------------------
% 69.84/13.83 % (1392310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392310)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392310)Termination reason: Instruction limit
% 69.84/13.83 % (1392310)Termination phase: Saturation
% 69.84/13.83 % (1392310)Time elapsed: 4.574 s
% 69.84/13.83 % (1392310)Peak memory usage: 45 MB
% 69.84/13.83 % (1392310)Instructions burned: 5212 (million)
% 69.84/13.83 % (1392328)ott-3_8_sil=64000:random_seed=558849467:i=20139:bs=on_2902 on theBenchmark for (2902ds/20139Mi)
% 69.84/13.83 % (1392324)Instruction limit reached!
% 69.84/13.83 % (1392324)------------------------------
% 69.84/13.83 % (1392324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392324)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392324)Termination reason: Instruction limit
% 69.84/13.83 % (1392324)Termination phase: Saturation
% 69.84/13.83 % (1392324)Time elapsed: 4.774 s
% 69.84/13.83 % (1392324)Peak memory usage: 48 MB
% 69.84/13.83 % (1392324)Instructions burned: 9157 (million)
% 69.84/13.83 % (1392334)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2438530697:fmbsr=2:i=32576_2884 on theBenchmark for (2884ds/32576Mi)
% 69.84/13.83 % (1392334)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 69.84/13.83 % (1392334)Terminated due to inappropriate strategy.
% 69.84/13.83 % (1392334)------------------------------
% 69.84/13.83 % (1392334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392334)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392334)Termination reason: Inappropriate
% 69.84/13.83 % (1392334)Time elapsed: 0.029 s
% 69.84/13.83 % (1392334)Peak memory usage: 12 MB
% 69.84/13.83 % (1392334)Instructions burned: 59 (million)
% 69.84/13.83 % (1392334)------------------------------
% 69.84/13.83 % (1392334)------------------------------
% 69.84/13.83 % (1392336)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4200583282:i=11404_2884 on theBenchmark for (2884ds/11404Mi)
% 69.84/13.83 % (1392336) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1392234-1392336"...
% 69.84/13.83 % (1392336)...printing done.
% 69.84/13.83 % (1392336)Refutation found. Thanks to Tanya!
% 69.84/13.83 % SZS status Theorem for theBenchmark
% 69.84/13.83 % SZS output start Proof for theBenchmark
% See solution above
% 69.84/13.83 % (1392336)------------------------------
% 69.84/13.83 % (1392336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.84/13.83 % (1392336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.84/13.83 % (1392336)CaDiCaL version: 2.1.3
% 69.84/13.83 % (1392336)Termination reason: Refutation
% 69.84/13.83 % (1392336)Time elapsed: 1.677 s
% 69.84/13.83 % (1392336)Peak memory usage: 41 MB
% 69.84/13.83 % (1392336)Instructions burned: 3232 (million)
% 69.84/13.83 % (1392234)Success in time 13.336 s
% 69.84/13.83 % Vampire exiting
%------------------------------------------------------------------------------