%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM993_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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 12:26:21 PM UTC 2026
% Result : Theorem 25.04s 8.33s
% Output : Refutation 25.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 32
% Syntax : Number of formulae : 195 ( 126 unt; 0 typ; 0 def)
% Number of atoms : 310 ( 110 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 220 ( 105 ~; 86 |; 11 &)
% ( 9 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-3 aty)
% Number of variables : 246 ( 243 !; 3 ?; 246 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
bool: $tType ).
tff(type_def_6,type,
int: $tType ).
tff(type_def_7,type,
nat: $tType ).
tff(func_def_0,type,
minus_minus:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_1,type,
one_one:
!>[X0: $tType] : X0 ).
tff(func_def_2,type,
plus_plus:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_3,type,
times_times:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_4,type,
zero_zero:
!>[X0: $tType] : X0 ).
tff(func_def_5,type,
bit0: int > int ).
tff(func_def_6,type,
bit1: int > int ).
tff(func_def_7,type,
pls: int ).
tff(func_def_8,type,
number_number_of:
!>[X0: $tType] : ( int > X0 ) ).
tff(func_def_9,type,
semiring_1_of_nat:
!>[X0: $tType] : ( nat > X0 ) ).
tff(func_def_10,type,
fFalse: bool ).
tff(func_def_11,type,
fTrue: bool ).
tff(func_def_12,type,
m1: int ).
tff(func_def_13,type,
n: nat ).
tff(func_def_14,type,
t: int ).
tff(func_def_15,type,
sK0: ( int * int ) > nat ).
tff(pred_def_1,type,
number:
!>[X0: $tType] : $o ).
tff(pred_def_2,type,
ring:
!>[X0: $tType] : $o ).
tff(pred_def_3,type,
semiring:
!>[X0: $tType] : $o ).
tff(pred_def_4,type,
number_ring:
!>[X0: $tType] : $o ).
tff(pred_def_5,type,
ring_char_0:
!>[X0: $tType] : $o ).
tff(pred_def_6,type,
linorder:
!>[X0: $tType] : $o ).
tff(pred_def_7,type,
linordered_idom:
!>[X0: $tType] : $o ).
tff(pred_def_8,type,
linord219039673up_add:
!>[X0: $tType] : $o ).
tff(pred_def_9,type,
ord_less:
!>[X0: $tType] : ( ( X0 * X0 ) > $o ) ).
tff(pred_def_10,type,
ord_less_eq:
!>[X0: $tType] : ( ( X0 * X0 ) > $o ) ).
tff(pred_def_11,type,
pp: bool > $o ).
tff(f4,axiom,
ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_n1pos) ).
tff(f5,axiom,
ord_less(int,minus_minus(int,times_times(int,number_number_of(int,bit0(bit1(pls))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m1)),zero_zero(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4__0962_A_K_A_I1_A_L_Aint_An_J_A_N_A4_A_K_Am1_A_060_A0_096) ).
tff(f14,axiom,
! [X0: int,X1: int] : ( times_times(int,bit1(X1),X0) = plus_plus(int,bit0(times_times(int,X1,X0)),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_mult__Bit1) ).
tff(f15,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ( number_number_of(X0,bit1(pls)) = one_one(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_numeral__1__eq__1) ).
tff(f23,axiom,
! [X0: $tType] :
( linord219039673up_add(X0)
=> ! [X1: X0] :
( ( plus_plus(X0,X1,X1) = zero_zero(X0) )
<=> ( X1 = zero_zero(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_double__eq__0__iff) ).
tff(f30,axiom,
bit0(pls) = pls,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_Bit0__Pls) ).
tff(f37,axiom,
! [X0: int] : ( times_times(int,pls,X0) = pls ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_mult__Pls) ).
tff(f38,axiom,
! [X0: int,X1: int] : ( times_times(int,bit0(X1),X0) = bit0(times_times(int,X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_mult__Bit0) ).
tff(f39,axiom,
! [X0: int,X1: int] : ( plus_plus(int,bit0(X1),bit0(X0)) = bit0(plus_plus(int,X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_add__Bit0__Bit0) ).
tff(f40,axiom,
! [X0: int,X1: int] : ( minus_minus(int,bit0(X1),bit0(X0)) = bit0(minus_minus(int,X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_diff__bin__simps_I7_J) ).
tff(f43,axiom,
! [X0: $tType] :
( ( number(X0)
& semiring(X0) )
=> ! [X1: X0,X2: X0,X3: int] : ( times_times(X0,number_number_of(X0,X3),plus_plus(X0,X2,X1)) = plus_plus(X0,times_times(X0,number_number_of(X0,X3),X2),times_times(X0,number_number_of(X0,X3),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_right__distrib__number__of) ).
tff(f44,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ( number_number_of(X0,pls) = zero_zero(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_number__of__Pls) ).
tff(f46,axiom,
! [X0: $tType] :
( ( number(X0)
& ring(X0) )
=> ! [X1: X0,X2: X0,X3: int] : ( times_times(X0,number_number_of(X0,X3),minus_minus(X0,X2,X1)) = minus_minus(X0,times_times(X0,number_number_of(X0,X3),X2),times_times(X0,number_number_of(X0,X3),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_right__diff__distrib__number__of) ).
tff(f51,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ! [X1: X0,X2: int,X3: int] : ( plus_plus(X0,number_number_of(X0,X3),plus_plus(X0,number_number_of(X0,X2),X1)) = plus_plus(X0,number_number_of(X0,plus_plus(int,X3,X2)),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_add__number__of__left) ).
tff(f62,axiom,
! [X0: int,X1: int] : ( plus_plus(int,bit0(X1),bit1(X0)) = bit1(plus_plus(int,X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_add__Bit0__Bit1) ).
tff(f79,axiom,
! [X0: nat] :
( ord_less(int,zero_zero(int),semiring_1_of_nat(int,X0))
<=> ord_less(nat,zero_zero(nat),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_zero__less__int__conv) ).
tff(f80,axiom,
! [X0: nat,X1: int,X2: int] :
( ord_less(int,X2,X1)
=> ( ord_less(nat,zero_zero(nat),X0)
=> ord_less(int,times_times(int,semiring_1_of_nat(int,X0),X2),times_times(int,semiring_1_of_nat(int,X0),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_zmult__zless__mono2__lemma) ).
tff(f81,axiom,
! [X0: $tType] :
( ( number(X0)
& linorder(X0) )
=> ! [X1: int,X2: int] :
( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
<=> ~ ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_le__number__of__eq__not__less) ).
tff(f85,axiom,
! [X0: nat,X1: nat] : ( plus_plus(int,semiring_1_of_nat(int,X1),semiring_1_of_nat(int,X0)) = semiring_1_of_nat(int,plus_plus(nat,X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_zadd__int) ).
tff(f87,axiom,
! [X0: int,X1: int] :
( ord_less_eq(int,X1,X0)
<=> ? [X2: nat] : ( X0 = plus_plus(int,X1,semiring_1_of_nat(int,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_zle__iff__zadd) ).
tff(f88,axiom,
semiring_1_of_nat(int,one_one(nat)) = one_one(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_int__1) ).
tff(f90,axiom,
semiring_1_of_nat(int,zero_zero(nat)) = zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_int__0) ).
tff(f93,axiom,
! [X0: int] :
( ord_less_eq(int,one_one(int),X0)
<=> ord_less(int,zero_zero(int),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_int__one__le__iff__zero__less) ).
tff(f95,axiom,
! [X0: int,X1: int] :
( ord_less_eq(int,plus_plus(int,X1,one_one(int)),X0)
<=> ord_less(int,X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_add1__zle__eq) ).
tff(f98,axiom,
! [X0: int] : ( number_number_of(int,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_number__of__is__id) ).
tff(f99,axiom,
linord219039673up_add(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Groups_Olinordered__ab__group__add) ).
tff(f101,axiom,
linorder(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Orderings_Olinorder) ).
tff(f103,axiom,
number_ring(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Int_Onumber__ring) ).
tff(f104,axiom,
semiring(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Osemiring) ).
tff(f105,axiom,
ring(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Oring) ).
tff(f106,axiom,
number(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Int_Onumber) ).
tff(f113,conjecture,
ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),minus_minus(int,times_times(int,number_number_of(int,bit0(bit1(pls))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m1))),zero_zero(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(f114,negated_conjecture,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),minus_minus(int,times_times(int,number_number_of(int,bit0(bit1(pls))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m1))),zero_zero(int)),
inference(negated_conjecture,[status(cth)],[f113]) ).
tff(f115,plain,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),minus_minus(int,times_times(int,number_number_of(int,bit0(bit1(pls))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m1))),zero_zero(int)),
inference(flattening,[],[f114]) ).
tff(f127,plain,
! [X0: $tType] :
( ( number_number_of(X0,bit1(pls)) = one_one(X0) )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f15]) ).
tff(f130,plain,
! [X0: $tType] :
( ! [X1: X0] :
( ( plus_plus(X0,X1,X1) = zero_zero(X0) )
<=> ( X1 = zero_zero(X0) ) )
| ~ linord219039673up_add(X0) ),
inference(ennf_transformation,[],[f23]) ).
tff(f133,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0,X3: int] : ( times_times(X0,number_number_of(X0,X3),plus_plus(X0,X2,X1)) = plus_plus(X0,times_times(X0,number_number_of(X0,X3),X2),times_times(X0,number_number_of(X0,X3),X1)) )
| ~ number(X0)
| ~ semiring(X0) ),
inference(ennf_transformation,[],[f43]) ).
tff(f134,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0,X3: int] : ( times_times(X0,number_number_of(X0,X3),plus_plus(X0,X2,X1)) = plus_plus(X0,times_times(X0,number_number_of(X0,X3),X2),times_times(X0,number_number_of(X0,X3),X1)) )
| ~ number(X0)
| ~ semiring(X0) ),
inference(flattening,[],[f133]) ).
tff(f135,plain,
! [X0: $tType] :
( ( number_number_of(X0,pls) = zero_zero(X0) )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f44]) ).
tff(f138,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0,X3: int] : ( times_times(X0,number_number_of(X0,X3),minus_minus(X0,X2,X1)) = minus_minus(X0,times_times(X0,number_number_of(X0,X3),X2),times_times(X0,number_number_of(X0,X3),X1)) )
| ~ number(X0)
| ~ ring(X0) ),
inference(ennf_transformation,[],[f46]) ).
tff(f139,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0,X3: int] : ( times_times(X0,number_number_of(X0,X3),minus_minus(X0,X2,X1)) = minus_minus(X0,times_times(X0,number_number_of(X0,X3),X2),times_times(X0,number_number_of(X0,X3),X1)) )
| ~ number(X0)
| ~ ring(X0) ),
inference(flattening,[],[f138]) ).
tff(f146,plain,
! [X0: $tType] :
( ! [X1: X0,X2: int,X3: int] : ( plus_plus(X0,number_number_of(X0,X3),plus_plus(X0,number_number_of(X0,X2),X1)) = plus_plus(X0,number_number_of(X0,plus_plus(int,X3,X2)),X1) )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f51]) ).
tff(f156,plain,
! [X0: nat,X1: int,X2: int] :
( ord_less(int,times_times(int,semiring_1_of_nat(int,X0),X2),times_times(int,semiring_1_of_nat(int,X0),X1))
| ~ ord_less(nat,zero_zero(nat),X0)
| ~ ord_less(int,X2,X1) ),
inference(ennf_transformation,[],[f80]) ).
tff(f157,plain,
! [X0: nat,X1: int,X2: int] :
( ord_less(int,times_times(int,semiring_1_of_nat(int,X0),X2),times_times(int,semiring_1_of_nat(int,X0),X1))
| ~ ord_less(nat,zero_zero(nat),X0)
| ~ ord_less(int,X2,X1) ),
inference(flattening,[],[f156]) ).
tff(f158,plain,
! [X0: $tType] :
( ! [X1: int,X2: int] :
( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
<=> ~ ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2)) )
| ~ number(X0)
| ~ linorder(X0) ),
inference(ennf_transformation,[],[f81]) ).
tff(f159,plain,
! [X0: $tType] :
( ! [X1: int,X2: int] :
( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
<=> ~ ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2)) )
| ~ number(X0)
| ~ linorder(X0) ),
inference(flattening,[],[f158]) ).
tff(f170,plain,
! [X0: $tType] :
( ! [X1: X0] :
( ( ( plus_plus(X0,X1,X1) = zero_zero(X0) )
| ( zero_zero(X0) != X1 ) )
& ( ( X1 = zero_zero(X0) )
| ( zero_zero(X0) != plus_plus(X0,X1,X1) ) ) )
| ~ linord219039673up_add(X0) ),
inference(nnf_transformation,[],[f130]) ).
tff(f203,plain,
! [X0: nat] :
( ( ord_less(int,zero_zero(int),semiring_1_of_nat(int,X0))
| ~ ord_less(nat,zero_zero(nat),X0) )
& ( ord_less(nat,zero_zero(nat),X0)
| ~ ord_less(int,zero_zero(int),semiring_1_of_nat(int,X0)) ) ),
inference(nnf_transformation,[],[f79]) ).
tff(f204,plain,
! [X0: $tType] :
( ! [X1: int,X2: int] :
( ( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
| ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2)) )
& ( ~ ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2))
| ~ ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1)) ) )
| ~ number(X0)
| ~ linorder(X0) ),
inference(nnf_transformation,[],[f159]) ).
tff(f207,plain,
! [X0: int,X1: int] :
( ( ord_less_eq(int,X1,X0)
| ! [X2: nat] : ( plus_plus(int,X1,semiring_1_of_nat(int,X2)) != X0 ) )
& ( ? [X2: nat] : ( X0 = plus_plus(int,X1,semiring_1_of_nat(int,X2)) )
| ~ ord_less_eq(int,X1,X0) ) ),
inference(nnf_transformation,[],[f87]) ).
tff(f208,plain,
! [X0: int,X1: int] :
( ( ord_less_eq(int,X1,X0)
| ! [X2: nat] : ( plus_plus(int,X1,semiring_1_of_nat(int,X2)) != X0 ) )
& ( ? [X3: nat] : ( plus_plus(int,X1,semiring_1_of_nat(int,X3)) = X0 )
| ~ ord_less_eq(int,X1,X0) ) ),
inference(rectify,[],[f207]) ).
tff(f209,plain,
! [X0: int,X1: int] :
( ( ord_less_eq(int,X1,X0)
| ! [X2: nat] : ( plus_plus(int,X1,semiring_1_of_nat(int,X2)) != X0 ) )
& ( ( plus_plus(int,X1,semiring_1_of_nat(int,sK0(X0,X1))) = X0 )
| ~ ord_less_eq(int,X1,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X0,X1))],[f208]) ).
tff(f213,plain,
! [X0: int] :
( ( ord_less_eq(int,one_one(int),X0)
| ~ ord_less(int,zero_zero(int),X0) )
& ( ord_less(int,zero_zero(int),X0)
| ~ ord_less_eq(int,one_one(int),X0) ) ),
inference(nnf_transformation,[],[f93]) ).
tff(f214,plain,
! [X0: int,X1: int] :
( ( ord_less_eq(int,plus_plus(int,X1,one_one(int)),X0)
| ~ ord_less(int,X1,X0) )
& ( ord_less(int,X1,X0)
| ~ ord_less_eq(int,plus_plus(int,X1,one_one(int)),X0) ) ),
inference(nnf_transformation,[],[f95]) ).
tff(f219,plain,
ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),
inference(cnf_transformation,[],[f4]) ).
tff(f220,plain,
ord_less(int,minus_minus(int,times_times(int,number_number_of(int,bit0(bit1(pls))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m1)),zero_zero(int)),
inference(cnf_transformation,[],[f5]) ).
tff(f233,plain,
! [X0: int,X1: int] : ( times_times(int,bit1(X1),X0) = plus_plus(int,bit0(times_times(int,X1,X0)),X0) ),
inference(cnf_transformation,[],[f14]) ).
tff(f234,plain,
! [X0: $tType] :
( ~ number_ring(X0)
| ( one_one(X0) = number_number_of(X0,bit1(pls)) ) ),
inference(cnf_transformation,[],[f127]) ).
tff(f246,plain,
! [X0: $tType,X1: X0] :
( ( zero_zero(X0) = plus_plus(X0,X1,X1) )
| ( zero_zero(X0) != X1 )
| ~ linord219039673up_add(X0) ),
inference(cnf_transformation,[],[f170]) ).
tff(f255,plain,
pls = bit0(pls),
inference(cnf_transformation,[],[f30]) ).
tff(f266,plain,
! [X0: int] : ( pls = times_times(int,pls,X0) ),
inference(cnf_transformation,[],[f37]) ).
tff(f267,plain,
! [X0: int,X1: int] : ( bit0(times_times(int,X1,X0)) = times_times(int,bit0(X1),X0) ),
inference(cnf_transformation,[],[f38]) ).
tff(f268,plain,
! [X0: int,X1: int] : ( plus_plus(int,bit0(X1),bit0(X0)) = bit0(plus_plus(int,X1,X0)) ),
inference(cnf_transformation,[],[f39]) ).
tff(f269,plain,
! [X0: int,X1: int] : ( minus_minus(int,bit0(X1),bit0(X0)) = bit0(minus_minus(int,X1,X0)) ),
inference(cnf_transformation,[],[f40]) ).
tff(f272,plain,
! [X0: $tType,X2: X0,X3: int,X1: X0] :
( ~ semiring(X0)
| ~ number(X0)
| ( times_times(X0,number_number_of(X0,X3),plus_plus(X0,X2,X1)) = plus_plus(X0,times_times(X0,number_number_of(X0,X3),X2),times_times(X0,number_number_of(X0,X3),X1)) ) ),
inference(cnf_transformation,[],[f134]) ).
tff(f273,plain,
! [X0: $tType] :
( ~ number_ring(X0)
| ( zero_zero(X0) = number_number_of(X0,pls) ) ),
inference(cnf_transformation,[],[f135]) ).
tff(f275,plain,
! [X0: $tType,X2: X0,X3: int,X1: X0] :
( ~ ring(X0)
| ~ number(X0)
| ( times_times(X0,number_number_of(X0,X3),minus_minus(X0,X2,X1)) = minus_minus(X0,times_times(X0,number_number_of(X0,X3),X2),times_times(X0,number_number_of(X0,X3),X1)) ) ),
inference(cnf_transformation,[],[f139]) ).
tff(f282,plain,
! [X0: $tType,X2: int,X3: int,X1: X0] :
( ~ number_ring(X0)
| ( plus_plus(X0,number_number_of(X0,X3),plus_plus(X0,number_number_of(X0,X2),X1)) = plus_plus(X0,number_number_of(X0,plus_plus(int,X3,X2)),X1) ) ),
inference(cnf_transformation,[],[f146]) ).
tff(f301,plain,
! [X0: int,X1: int] : ( bit1(plus_plus(int,X1,X0)) = plus_plus(int,bit0(X1),bit1(X0)) ),
inference(cnf_transformation,[],[f62]) ).
tff(f334,plain,
! [X0: nat] :
( ~ ord_less(int,zero_zero(int),semiring_1_of_nat(int,X0))
| ord_less(nat,zero_zero(nat),X0) ),
inference(cnf_transformation,[],[f203]) ).
tff(f336,plain,
! [X2: int,X0: nat,X1: int] :
( ord_less(int,times_times(int,semiring_1_of_nat(int,X0),X2),times_times(int,semiring_1_of_nat(int,X0),X1))
| ~ ord_less(nat,zero_zero(nat),X0)
| ~ ord_less(int,X2,X1) ),
inference(cnf_transformation,[],[f157]) ).
tff(f337,plain,
! [X0: $tType,X2: int,X1: int] :
( ~ linorder(X0)
| ~ ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
| ~ number(X0)
| ~ ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2)) ),
inference(cnf_transformation,[],[f204]) ).
tff(f338,plain,
! [X0: $tType,X2: int,X1: int] :
( ~ linorder(X0)
| ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2))
| ~ number(X0)
| ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1)) ),
inference(cnf_transformation,[],[f204]) ).
tff(f343,plain,
! [X0: nat,X1: nat] : ( plus_plus(int,semiring_1_of_nat(int,X1),semiring_1_of_nat(int,X0)) = semiring_1_of_nat(int,plus_plus(nat,X1,X0)) ),
inference(cnf_transformation,[],[f85]) ).
tff(f346,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq(int,X1,X0)
| ( plus_plus(int,X1,semiring_1_of_nat(int,sK0(X0,X1))) = X0 ) ),
inference(cnf_transformation,[],[f209]) ).
tff(f347,plain,
! [X2: nat,X0: int,X1: int] :
( ord_less_eq(int,X1,X0)
| ( plus_plus(int,X1,semiring_1_of_nat(int,X2)) != X0 ) ),
inference(cnf_transformation,[],[f209]) ).
tff(f348,plain,
one_one(int) = semiring_1_of_nat(int,one_one(nat)),
inference(cnf_transformation,[],[f88]) ).
tff(f351,plain,
zero_zero(int) = semiring_1_of_nat(int,zero_zero(nat)),
inference(cnf_transformation,[],[f90]) ).
tff(f356,plain,
! [X0: int] :
( ~ ord_less_eq(int,one_one(int),X0)
| ord_less(int,zero_zero(int),X0) ),
inference(cnf_transformation,[],[f213]) ).
tff(f357,plain,
! [X0: int] :
( ord_less_eq(int,one_one(int),X0)
| ~ ord_less(int,zero_zero(int),X0) ),
inference(cnf_transformation,[],[f213]) ).
tff(f359,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq(int,plus_plus(int,X1,one_one(int)),X0)
| ord_less(int,X1,X0) ),
inference(cnf_transformation,[],[f214]) ).
tff(f360,plain,
! [X0: int,X1: int] :
( ord_less_eq(int,plus_plus(int,X1,one_one(int)),X0)
| ~ ord_less(int,X1,X0) ),
inference(cnf_transformation,[],[f214]) ).
tff(f364,plain,
! [X0: int] : ( number_number_of(int,X0) = X0 ),
inference(cnf_transformation,[],[f98]) ).
tff(f365,plain,
linord219039673up_add(int),
inference(cnf_transformation,[],[f99]) ).
tff(f367,plain,
linorder(int),
inference(cnf_transformation,[],[f101]) ).
tff(f369,plain,
number_ring(int),
inference(cnf_transformation,[],[f103]) ).
tff(f370,plain,
semiring(int),
inference(cnf_transformation,[],[f104]) ).
tff(f371,plain,
ring(int),
inference(cnf_transformation,[],[f105]) ).
tff(f372,plain,
number(int),
inference(cnf_transformation,[],[f106]) ).
tff(f379,plain,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),minus_minus(int,times_times(int,number_number_of(int,bit0(bit1(pls))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m1))),zero_zero(int)),
inference(cnf_transformation,[],[f115]) ).
tff(f383,plain,
! [X0: $tType] :
( ~ linord219039673up_add(X0)
| ( zero_zero(X0) = plus_plus(X0,zero_zero(X0),zero_zero(X0)) ) ),
inference(equality_resolution,[],[f246]) ).
tff(f388,plain,
! [X2: nat,X1: int] : ord_less_eq(int,X1,plus_plus(int,X1,semiring_1_of_nat(int,X2))),
inference(equality_resolution,[],[f347]) ).
tff(f396,plain,
ord_less(int,minus_minus(int,times_times(int,number_number_of(int,bit0(bit1(pls))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,bit0(bit0(bit1(pls))),m1)),zero_zero(int)),
inference(forward_demodulation,[],[f220,f364]) ).
tff(f401,plain,
ord_less(int,minus_minus(int,times_times(int,number_number_of(int,bit0(bit1(pls))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(times_times(int,bit0(bit1(pls)),m1))),zero_zero(int)),
inference(forward_demodulation,[],[f396,f267]) ).
tff(f404,plain,
ord_less(int,minus_minus(int,times_times(int,number_number_of(int,bit0(bit1(pls))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(bit0(times_times(int,bit1(pls),m1)))),zero_zero(int)),
inference(forward_demodulation,[],[f401,f267]) ).
tff(f407,plain,
ord_less(int,minus_minus(int,times_times(int,bit0(bit1(pls)),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(bit0(times_times(int,bit1(pls),m1)))),zero_zero(int)),
inference(forward_demodulation,[],[f404,f364]) ).
tff(f410,plain,
ord_less(int,minus_minus(int,bit0(times_times(int,bit1(pls),plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),bit0(bit0(times_times(int,bit1(pls),m1)))),zero_zero(int)),
inference(forward_demodulation,[],[f407,f267]) ).
tff(f413,plain,
ord_less(int,bit0(minus_minus(int,times_times(int,bit1(pls),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(times_times(int,bit1(pls),m1)))),zero_zero(int)),
inference(forward_demodulation,[],[f410,f269]) ).
tff(f417,plain,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),minus_minus(int,times_times(int,number_number_of(int,bit0(bit1(pls))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,bit0(bit0(bit1(pls))),m1))),zero_zero(int)),
inference(superposition,[],[f379,f364]) ).
tff(f418,plain,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),minus_minus(int,times_times(int,number_number_of(int,bit0(bit1(pls))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(times_times(int,bit0(bit1(pls)),m1)))),zero_zero(int)),
inference(forward_demodulation,[],[f417,f267]) ).
tff(f420,plain,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),minus_minus(int,times_times(int,number_number_of(int,bit0(bit1(pls))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(bit0(times_times(int,bit1(pls),m1))))),zero_zero(int)),
inference(forward_demodulation,[],[f418,f267]) ).
tff(f422,plain,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),minus_minus(int,times_times(int,bit0(bit1(pls)),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(bit0(times_times(int,bit1(pls),m1))))),zero_zero(int)),
inference(forward_demodulation,[],[f420,f364]) ).
tff(f424,plain,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),minus_minus(int,bit0(times_times(int,bit1(pls),plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),bit0(bit0(times_times(int,bit1(pls),m1))))),zero_zero(int)),
inference(forward_demodulation,[],[f422,f267]) ).
tff(f426,plain,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),bit0(minus_minus(int,times_times(int,bit1(pls),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(times_times(int,bit1(pls),m1))))),zero_zero(int)),
inference(forward_demodulation,[],[f424,f269]) ).
tff(f434,plain,
zero_zero(int) = number_number_of(int,pls),
inference(resolution,[],[f273,f369]) ).
tff(f435,plain,
pls = zero_zero(int),
inference(forward_demodulation,[],[f434,f364]) ).
tff(f439,plain,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),bit0(minus_minus(int,times_times(int,bit1(pls),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(times_times(int,bit1(pls),m1))))),pls),
inference(superposition,[],[f426,f435]) ).
tff(f447,plain,
one_one(int) = number_number_of(int,bit1(pls)),
inference(resolution,[],[f234,f369]) ).
tff(f448,plain,
one_one(int) = bit1(pls),
inference(forward_demodulation,[],[f447,f364]) ).
tff(f449,plain,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),bit0(minus_minus(int,times_times(int,one_one(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(times_times(int,one_one(int),m1))))),pls),
inference(superposition,[],[f439,f448]) ).
tff(f557,plain,
! [X0: nat] : ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,X0))),
inference(resolution,[],[f356,f388]) ).
tff(f562,plain,
! [X0: nat] : ord_less(int,pls,plus_plus(int,one_one(int),semiring_1_of_nat(int,X0))),
inference(forward_demodulation,[],[f557,f435]) ).
tff(f608,plain,
zero_zero(int) = plus_plus(int,zero_zero(int),zero_zero(int)),
inference(resolution,[],[f383,f365]) ).
tff(f609,plain,
pls = plus_plus(int,pls,pls),
inference(forward_demodulation,[],[f608,f435]) ).
tff(f616,plain,
! [X0: int] : ( bit0(plus_plus(int,pls,X0)) = plus_plus(int,pls,bit0(X0)) ),
inference(superposition,[],[f268,f255]) ).
tff(f663,plain,
! [X0: int] : ( bit1(plus_plus(int,pls,X0)) = plus_plus(int,pls,bit1(X0)) ),
inference(superposition,[],[f301,f255]) ).
tff(f688,plain,
! [X0: nat] :
( ~ ord_less(int,pls,semiring_1_of_nat(int,X0))
| ord_less(nat,zero_zero(nat),X0) ),
inference(superposition,[],[f334,f435]) ).
tff(f715,plain,
! [X0: int,X1: nat] : ord_less(int,X0,plus_plus(int,plus_plus(int,X0,one_one(int)),semiring_1_of_nat(int,X1))),
inference(resolution,[],[f359,f388]) ).
tff(f751,plain,
! [X0: int] : ( times_times(int,bit1(pls),X0) = plus_plus(int,bit0(pls),X0) ),
inference(superposition,[],[f233,f266]) ).
tff(f766,plain,
! [X0: int] : ( plus_plus(int,pls,X0) = times_times(int,bit1(pls),X0) ),
inference(forward_demodulation,[],[f751,f255]) ).
tff(f767,plain,
! [X0: int] : ( plus_plus(int,pls,X0) = times_times(int,one_one(int),X0) ),
inference(forward_demodulation,[],[f766,f448]) ).
tff(f795,plain,
! [X0: int] :
( ( plus_plus(int,one_one(int),semiring_1_of_nat(int,sK0(X0,one_one(int)))) = X0 )
| ~ ord_less(int,zero_zero(int),X0) ),
inference(resolution,[],[f346,f357]) ).
tff(f797,plain,
! [X0: int,X1: int] :
( ~ ord_less(int,X0,X1)
| ( plus_plus(int,plus_plus(int,X0,one_one(int)),semiring_1_of_nat(int,sK0(X1,plus_plus(int,X0,one_one(int))))) = X1 ) ),
inference(resolution,[],[f346,f360]) ).
tff(f815,plain,
! [X0: int] :
( ~ ord_less(int,pls,X0)
| ( plus_plus(int,one_one(int),semiring_1_of_nat(int,sK0(X0,one_one(int)))) = X0 ) ),
inference(forward_demodulation,[],[f795,f435]) ).
tff(f827,plain,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),bit0(minus_minus(int,times_times(int,one_one(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(plus_plus(int,pls,m1))))),pls),
inference(superposition,[],[f449,f767]) ).
tff(f829,plain,
~ ord_less(int,times_times(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),bit0(minus_minus(int,plus_plus(int,pls,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(plus_plus(int,pls,m1))))),pls),
inference(forward_demodulation,[],[f827,f767]) ).
tff(f896,plain,
! [X0: nat] : ( plus_plus(int,one_one(int),semiring_1_of_nat(int,X0)) = semiring_1_of_nat(int,plus_plus(nat,one_one(nat),X0)) ),
inference(superposition,[],[f343,f348]) ).
tff(f897,plain,
! [X0: nat] : ( semiring_1_of_nat(int,plus_plus(nat,zero_zero(nat),X0)) = plus_plus(int,zero_zero(int),semiring_1_of_nat(int,X0)) ),
inference(superposition,[],[f343,f351]) ).
tff(f904,plain,
! [X0: nat] : ( semiring_1_of_nat(int,plus_plus(nat,zero_zero(nat),X0)) = plus_plus(int,pls,semiring_1_of_nat(int,X0)) ),
inference(forward_demodulation,[],[f897,f435]) ).
tff(f1071,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq(int,number_number_of(int,X0),number_number_of(int,X1))
| ~ number(int)
| ~ ord_less(int,number_number_of(int,X1),number_number_of(int,X0)) ),
inference(resolution,[],[f337,f367]) ).
tff(f1075,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq(int,number_number_of(int,X0),number_number_of(int,X1))
| ~ ord_less(int,number_number_of(int,X1),number_number_of(int,X0)) ),
inference(forward_subsumption_resolution,[],[f1071,f372]) ).
tff(f1076,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq(int,number_number_of(int,X0),X1)
| ~ ord_less(int,number_number_of(int,X1),number_number_of(int,X0)) ),
inference(forward_demodulation,[],[f1075,f364]) ).
tff(f1077,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq(int,X0,X1)
| ~ ord_less(int,number_number_of(int,X1),number_number_of(int,X0)) ),
inference(forward_demodulation,[],[f1076,f364]) ).
tff(f1078,plain,
! [X0: int,X1: int] :
( ~ ord_less(int,number_number_of(int,X1),X0)
| ~ ord_less_eq(int,X0,X1) ),
inference(forward_demodulation,[],[f1077,f364]) ).
tff(f1079,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq(int,X0,X1)
| ~ ord_less(int,X1,X0) ),
inference(forward_demodulation,[],[f1078,f364]) ).
tff(f1116,plain,
! [X0: int,X1: int] :
( ord_less(int,number_number_of(int,X0),number_number_of(int,X1))
| ~ number(int)
| ord_less_eq(int,number_number_of(int,X1),number_number_of(int,X0)) ),
inference(resolution,[],[f338,f367]) ).
tff(f1120,plain,
! [X0: int,X1: int] :
( ord_less(int,number_number_of(int,X0),number_number_of(int,X1))
| ord_less_eq(int,number_number_of(int,X1),number_number_of(int,X0)) ),
inference(forward_subsumption_resolution,[],[f1116,f372]) ).
tff(f1121,plain,
! [X0: int,X1: int] :
( ord_less(int,number_number_of(int,X0),X1)
| ord_less_eq(int,number_number_of(int,X1),number_number_of(int,X0)) ),
inference(forward_demodulation,[],[f1120,f364]) ).
tff(f1122,plain,
! [X0: int,X1: int] :
( ord_less(int,X0,X1)
| ord_less_eq(int,number_number_of(int,X1),number_number_of(int,X0)) ),
inference(forward_demodulation,[],[f1121,f364]) ).
tff(f1123,plain,
! [X0: int,X1: int] :
( ord_less_eq(int,number_number_of(int,X1),X0)
| ord_less(int,X0,X1) ),
inference(forward_demodulation,[],[f1122,f364]) ).
tff(f1124,plain,
! [X0: int,X1: int] :
( ord_less_eq(int,X1,X0)
| ord_less(int,X0,X1) ),
inference(forward_demodulation,[],[f1123,f364]) ).
tff(f1152,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,number_number_of(int,X0),plus_plus(int,number_number_of(int,X1),X2)) = plus_plus(int,number_number_of(int,plus_plus(int,X0,X1)),X2) ),
inference(resolution,[],[f282,f369]) ).
tff(f1153,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,number_number_of(int,X0),plus_plus(int,number_number_of(int,X1),X2)) = plus_plus(int,plus_plus(int,X0,X1),X2) ),
inference(forward_demodulation,[],[f1152,f364]) ).
tff(f1154,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,plus_plus(int,X0,X1),X2) = plus_plus(int,number_number_of(int,X0),plus_plus(int,X1,X2)) ),
inference(forward_demodulation,[],[f1153,f364]) ).
tff(f1155,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,plus_plus(int,X0,X1),X2) = plus_plus(int,X0,plus_plus(int,X1,X2)) ),
inference(forward_demodulation,[],[f1154,f364]) ).
tff(f1157,plain,
! [X0: int,X1: int] :
( ord_less(int,X0,X1)
| ( plus_plus(int,X1,semiring_1_of_nat(int,sK0(X0,X1))) = X0 ) ),
inference(resolution,[],[f1124,f346]) ).
tff(f1230,plain,
ord_less(int,bit0(minus_minus(int,times_times(int,bit1(pls),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(times_times(int,bit1(pls),m1)))),pls),
inference(superposition,[],[f413,f435]) ).
tff(f1231,plain,
ord_less(int,bit0(minus_minus(int,times_times(int,one_one(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(times_times(int,one_one(int),m1)))),pls),
inference(forward_demodulation,[],[f1230,f448]) ).
tff(f1234,plain,
ord_less(int,bit0(minus_minus(int,times_times(int,one_one(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(plus_plus(int,pls,m1)))),pls),
inference(forward_demodulation,[],[f1231,f767]) ).
tff(f1237,plain,
ord_less(int,bit0(minus_minus(int,plus_plus(int,pls,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),bit0(plus_plus(int,pls,m1)))),pls),
inference(forward_demodulation,[],[f1234,f767]) ).
tff(f1240,plain,
ord_less(int,bit0(minus_minus(int,plus_plus(int,pls,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n))),bit0(plus_plus(int,pls,m1)))),pls),
inference(forward_demodulation,[],[f1237,f896]) ).
tff(f1292,plain,
! [X2: int,X0: int,X1: int] :
( ~ number(int)
| ( times_times(int,number_number_of(int,X0),plus_plus(int,X1,X2)) = plus_plus(int,times_times(int,number_number_of(int,X0),X1),times_times(int,number_number_of(int,X0),X2)) ) ),
inference(resolution,[],[f272,f370]) ).
tff(f1295,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,number_number_of(int,X0),plus_plus(int,X1,X2)) = plus_plus(int,times_times(int,number_number_of(int,X0),X1),times_times(int,number_number_of(int,X0),X2)) ),
inference(forward_subsumption_resolution,[],[f1292,f372]) ).
tff(f1296,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,X0,plus_plus(int,X1,X2)) = plus_plus(int,times_times(int,X0,X1),times_times(int,X0,X2)) ),
inference(forward_demodulation,[],[f1295,f364]) ).
tff(f1321,plain,
! [X2: int,X0: int,X1: int] :
( ~ number(int)
| ( times_times(int,number_number_of(int,X0),minus_minus(int,X1,X2)) = minus_minus(int,times_times(int,number_number_of(int,X0),X1),times_times(int,number_number_of(int,X0),X2)) ) ),
inference(resolution,[],[f275,f371]) ).
tff(f1322,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,number_number_of(int,X0),minus_minus(int,X1,X2)) = minus_minus(int,times_times(int,number_number_of(int,X0),X1),times_times(int,number_number_of(int,X0),X2)) ),
inference(forward_subsumption_resolution,[],[f1321,f372]) ).
tff(f1323,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,X0,minus_minus(int,X1,X2)) = minus_minus(int,times_times(int,X0,X1),times_times(int,X0,X2)) ),
inference(forward_demodulation,[],[f1322,f364]) ).
tff(f1355,plain,
plus_plus(int,pls,one_one(int)) = bit1(plus_plus(int,pls,pls)),
inference(superposition,[],[f663,f448]) ).
tff(f1356,plain,
bit1(pls) = plus_plus(int,pls,one_one(int)),
inference(forward_demodulation,[],[f1355,f609]) ).
tff(f1357,plain,
one_one(int) = plus_plus(int,pls,one_one(int)),
inference(forward_demodulation,[],[f1356,f448]) ).
tff(f1828,plain,
! [X0: nat,X1: int] : ord_less_eq(int,X1,plus_plus(int,X1,plus_plus(int,pls,semiring_1_of_nat(int,X0)))),
inference(superposition,[],[f388,f904]) ).
tff(f2008,plain,
~ ord_less(int,times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(minus_minus(int,plus_plus(int,pls,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n))),bit0(plus_plus(int,pls,m1))))),pls),
inference(superposition,[],[f829,f896]) ).
tff(f2009,plain,
! [X0: nat] : ord_less(int,pls,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),X0))),
inference(superposition,[],[f562,f896]) ).
tff(f2130,plain,
! [X0: int] : ( plus_plus(int,one_one(int),X0) = plus_plus(int,pls,plus_plus(int,one_one(int),X0)) ),
inference(superposition,[],[f1155,f1357]) ).
tff(f2133,plain,
! [X0: int] : ( plus_plus(int,pls,X0) = plus_plus(int,pls,plus_plus(int,pls,X0)) ),
inference(superposition,[],[f1155,f609]) ).
tff(f2591,plain,
! [X0: nat] : ( plus_plus(int,plus_plus(int,pls,one_one(int)),semiring_1_of_nat(int,X0)) = plus_plus(int,one_one(int),semiring_1_of_nat(int,sK0(plus_plus(int,plus_plus(int,pls,one_one(int)),semiring_1_of_nat(int,X0)),one_one(int)))) ),
inference(resolution,[],[f815,f715]) ).
tff(f2594,plain,
! [X0: nat] : ( plus_plus(int,plus_plus(int,pls,one_one(int)),semiring_1_of_nat(int,X0)) = semiring_1_of_nat(int,plus_plus(nat,one_one(nat),sK0(plus_plus(int,plus_plus(int,pls,one_one(int)),semiring_1_of_nat(int,X0)),one_one(int)))) ),
inference(forward_demodulation,[],[f2591,f896]) ).
tff(f2603,plain,
! [X0: nat] : ( plus_plus(int,pls,plus_plus(int,one_one(int),semiring_1_of_nat(int,X0))) = semiring_1_of_nat(int,plus_plus(nat,one_one(nat),sK0(plus_plus(int,pls,plus_plus(int,one_one(int),semiring_1_of_nat(int,X0))),one_one(int)))) ),
inference(forward_demodulation,[],[f2594,f1155]) ).
tff(f2605,plain,
! [X0: nat] : ( plus_plus(int,one_one(int),semiring_1_of_nat(int,X0)) = semiring_1_of_nat(int,plus_plus(nat,one_one(nat),sK0(plus_plus(int,one_one(int),semiring_1_of_nat(int,X0)),one_one(int)))) ),
inference(forward_demodulation,[],[f2603,f2130]) ).
tff(f2606,plain,
! [X0: nat] : ( semiring_1_of_nat(int,plus_plus(nat,one_one(nat),X0)) = semiring_1_of_nat(int,plus_plus(nat,one_one(nat),sK0(semiring_1_of_nat(int,plus_plus(nat,one_one(nat),X0)),one_one(int)))) ),
inference(forward_demodulation,[],[f2605,f896]) ).
tff(f3969,plain,
! [X0: int,X1: int] : ( times_times(int,one_one(int),minus_minus(int,X1,X0)) = minus_minus(int,times_times(int,one_one(int),X1),plus_plus(int,pls,X0)) ),
inference(superposition,[],[f1323,f767]) ).
tff(f3980,plain,
! [X0: int,X1: int] : ( times_times(int,one_one(int),minus_minus(int,X1,X0)) = minus_minus(int,plus_plus(int,pls,X1),plus_plus(int,pls,X0)) ),
inference(forward_demodulation,[],[f3969,f767]) ).
tff(f3989,plain,
! [X0: int,X1: int] : ( minus_minus(int,plus_plus(int,pls,X1),plus_plus(int,pls,X0)) = plus_plus(int,pls,minus_minus(int,X1,X0)) ),
inference(forward_demodulation,[],[f3980,f767]) ).
tff(f4933,plain,
! [X0: nat] : ord_less(nat,zero_zero(nat),plus_plus(nat,one_one(nat),X0)),
inference(resolution,[],[f688,f2009]) ).
tff(f5085,plain,
plus_plus(int,one_one(int),semiring_1_of_nat(int,n)) = plus_plus(int,plus_plus(int,zero_zero(int),one_one(int)),semiring_1_of_nat(int,sK0(plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),plus_plus(int,zero_zero(int),one_one(int))))),
inference(resolution,[],[f797,f219]) ).
tff(f5167,plain,
plus_plus(int,one_one(int),semiring_1_of_nat(int,n)) = plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,sK0(plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),plus_plus(int,zero_zero(int),one_one(int)))))),
inference(forward_demodulation,[],[f5085,f1155]) ).
tff(f5228,plain,
plus_plus(int,one_one(int),semiring_1_of_nat(int,n)) = plus_plus(int,zero_zero(int),semiring_1_of_nat(int,plus_plus(nat,one_one(nat),sK0(plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),plus_plus(int,zero_zero(int),one_one(int)))))),
inference(forward_demodulation,[],[f5167,f896]) ).
tff(f5280,plain,
plus_plus(int,one_one(int),semiring_1_of_nat(int,n)) = plus_plus(int,pls,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),sK0(plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),plus_plus(int,pls,one_one(int)))))),
inference(forward_demodulation,[],[f5228,f435]) ).
tff(f5314,plain,
plus_plus(int,one_one(int),semiring_1_of_nat(int,n)) = plus_plus(int,pls,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),sK0(plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),one_one(int))))),
inference(forward_demodulation,[],[f5280,f1357]) ).
tff(f5324,plain,
semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)) = plus_plus(int,pls,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),sK0(semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),one_one(int))))),
inference(forward_demodulation,[],[f5314,f896]) ).
tff(f5329,plain,
semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)) = plus_plus(int,pls,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n))),
inference(forward_demodulation,[],[f5324,f2606]) ).
tff(f9170,plain,
times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(minus_minus(int,plus_plus(int,pls,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n))),bit0(plus_plus(int,pls,m1))))) = plus_plus(int,pls,semiring_1_of_nat(int,sK0(times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(minus_minus(int,plus_plus(int,pls,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n))),bit0(plus_plus(int,pls,m1))))),pls))),
inference(resolution,[],[f1157,f2008]) ).
tff(f9264,plain,
times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(plus_plus(int,pls,m1))))) = plus_plus(int,pls,semiring_1_of_nat(int,sK0(times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(plus_plus(int,pls,m1))))),pls))),
inference(forward_demodulation,[],[f9170,f5329]) ).
tff(f9615,plain,
! [X0: int] : ord_less_eq(int,X0,plus_plus(int,X0,times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(plus_plus(int,pls,m1))))))),
inference(superposition,[],[f1828,f9264]) ).
tff(f9857,plain,
! [X0: int] : ord_less_eq(int,times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),X0),times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),plus_plus(int,X0,bit0(minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(plus_plus(int,pls,m1))))))),
inference(superposition,[],[f9615,f1296]) ).
tff(f33694,plain,
! [X0: int] : ( plus_plus(int,pls,minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),X0)) = minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),plus_plus(int,pls,X0)) ),
inference(superposition,[],[f3989,f5329]) ).
tff(f47995,plain,
ord_less(int,bit0(minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(plus_plus(int,pls,m1)))),pls),
inference(superposition,[],[f1240,f5329]) ).
tff(f115875,plain,
ord_less_eq(int,times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),pls),times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(plus_plus(int,pls,minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(plus_plus(int,pls,m1))))))),
inference(superposition,[],[f9857,f616]) ).
tff(f115884,plain,
ord_less_eq(int,times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),pls),times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),plus_plus(int,pls,bit0(plus_plus(int,pls,m1))))))),
inference(forward_demodulation,[],[f115875,f33694]) ).
tff(f115897,plain,
ord_less_eq(int,times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),pls),times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(plus_plus(int,pls,plus_plus(int,pls,m1))))))),
inference(forward_demodulation,[],[f115884,f616]) ).
tff(f115910,plain,
ord_less_eq(int,times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),pls),times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(plus_plus(int,pls,m1)))))),
inference(forward_demodulation,[],[f115897,f2133]) ).
tff(f115942,plain,
~ ord_less(int,times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(plus_plus(int,pls,m1))))),times_times(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),pls)),
inference(resolution,[],[f115910,f1079]) ).
tff(f115971,plain,
( ~ ord_less(nat,zero_zero(nat),plus_plus(nat,one_one(nat),n))
| ~ ord_less(int,bit0(minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(plus_plus(int,pls,m1)))),pls) ),
inference(resolution,[],[f115942,f336]) ).
tff(f115977,plain,
~ ord_less(int,bit0(minus_minus(int,semiring_1_of_nat(int,plus_plus(nat,one_one(nat),n)),bit0(plus_plus(int,pls,m1)))),pls),
inference(forward_subsumption_resolution,[],[f115971,f4933]) ).
tff(f115978,plain,
$false,
inference(forward_subsumption_resolution,[],[f115977,f47995]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM993_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n010.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 21:50:02 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.42 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
% 7.95/1.70 % (1342315)Will run a generic schedule for satisfiability detection.
% 7.95/1.70 % (1342327)% WARNING: option uhcvi not known.
% 7.95/1.70 % (1342327)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3440437685:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.95/1.70 % (1342326)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3528510021_2999 on theBenchmark for (2999ds/0Mi)
% 7.95/1.70 % (1342328)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1661540822:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.95/1.70 % (1342331)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3329943725:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.95/1.70 % (1342329)dis+10_1_sil=32000:sp=arity:random_seed=1228259559:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.95/1.70 % (1342332)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4291436814:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.95/1.70 % (1342330)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3165554763:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.95/1.70 % Exception at run slice level
% 7.95/1.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.95/1.70 % (1342346)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=256029395:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.95/1.70 % Exception at run slice level
% 7.95/1.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.95/1.70 % (1342354)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=668789003:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.95/1.70 % (1342329)Instruction limit reached!
% 7.95/1.70 % (1342329)------------------------------
% 7.95/1.70 % (1342329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.95/1.70 % (1342329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.95/1.70 % (1342329)CaDiCaL version: 2.1.3
% 7.95/1.70 % (1342329)Termination reason: Instruction limit
% 7.95/1.70 % (1342329)Termination phase: Saturation
% 7.95/1.70 % (1342329)Time elapsed: 0.061 s
% 7.95/1.70 % (1342329)Peak memory usage: 12 MB
% 7.95/1.70 % (1342329)Instructions burned: 104 (million)
% 7.95/1.70 % (1342331)Instruction limit reached!
% 7.95/1.70 % (1342331)------------------------------
% 7.95/1.70 % (1342331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.95/1.70 % (1342331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.95/1.70 % (1342331)CaDiCaL version: 2.1.3
% 7.95/1.70 % (1342331)Termination reason: Instruction limit
% 7.95/1.70 % (1342331)Termination phase: Saturation
% 7.95/1.70 % (1342331)Time elapsed: 0.067 s
% 7.95/1.70 % (1342331)Peak memory usage: 13 MB
% 7.95/1.70 % (1342331)Instructions burned: 131 (million)
% 7.95/1.70 % (1342330)Instruction limit reached!
% 7.95/1.70 % (1342330)------------------------------
% 7.95/1.70 % (1342330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.95/1.70 % (1342330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.95/1.70 % (1342330)CaDiCaL version: 2.1.3
% 7.95/1.70 % (1342330)Termination reason: Instruction limit
% 7.95/1.70 % (1342330)Termination phase: Saturation
% 7.95/1.70 % (1342330)Time elapsed: 0.070 s
% 7.95/1.70 % (1342330)Peak memory usage: 13 MB
% 7.95/1.70 % (1342330)Instructions burned: 117 (million)
% 7.95/1.70 % (1342364)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=3859145842:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.95/1.70 % (1342366)ott-21_1_sil=16000:fs=off:random_seed=1839243526:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.95/1.70 % (1342367)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=841932105:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.95/1.70 % (1342332)Instruction limit reached!
% 7.95/1.70 % (1342332)------------------------------
% 7.95/1.70 % (1342332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.95/1.70 % (1342332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.95/1.70 % (1342332)CaDiCaL version: 2.1.3
% 7.95/1.70 % (1342332)Termination reason: Instruction limit
% 7.95/1.70 % (1342332)Termination phase: Saturation
% 22.48/3.80 % (1342332)Time elapsed: 0.100 s
% 22.48/3.80 % (1342332)Peak memory usage: 13 MB
% 22.48/3.80 % (1342332)Instructions burned: 160 (million)
% 22.48/3.80 % (1342377)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2254704685:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 22.48/3.80 % Exception at run slice level
% 22.48/3.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.48/3.80 % (1342354)Instruction limit reached!
% 22.48/3.80 % (1342354)------------------------------
% 22.48/3.80 % (1342354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.48/3.80 % (1342354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.48/3.80 % (1342354)CaDiCaL version: 2.1.3
% 22.48/3.80 % (1342354)Termination reason: Instruction limit
% 22.48/3.80 % (1342354)Termination phase: Saturation
% 22.48/3.80 % (1342354)Time elapsed: 0.082 s
% 22.48/3.80 % (1342354)Peak memory usage: 13 MB
% 22.48/3.80 % (1342354)Instructions burned: 131 (million)
% 22.48/3.80 % (1342388)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1326478957:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 22.48/3.80 % (1342390)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1592940165:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 22.48/3.80 % Exception at run slice level
% 22.48/3.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.48/3.80 % (1342395)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=1727660360: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)
% 22.48/3.80 % (1342366)Instruction limit reached!
% 22.48/3.80 % (1342366)------------------------------
% 22.48/3.80 % (1342366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.48/3.80 % (1342366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.48/3.80 % (1342366)CaDiCaL version: 2.1.3
% 22.48/3.80 % (1342366)Termination reason: Instruction limit
% 22.48/3.80 % (1342366)Termination phase: Saturation
% 22.48/3.80 % (1342366)Time elapsed: 0.086 s
% 22.48/3.80 % (1342366)Peak memory usage: 13 MB
% 22.48/3.80 % (1342366)Instructions burned: 181 (million)
% 22.48/3.80 % (1342405)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2299055079:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 22.48/3.80 % (1342367)Instruction limit reached!
% 22.48/3.80 % (1342367)------------------------------
% 22.48/3.80 % (1342367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.48/3.80 % (1342367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.48/3.80 % (1342367)CaDiCaL version: 2.1.3
% 22.48/3.80 % (1342367)Termination reason: Instruction limit
% 22.48/3.80 % (1342367)Termination phase: Saturation
% 22.48/3.80 % (1342367)Time elapsed: 0.311 s
% 22.48/3.80 % (1342367)Peak memory usage: 14 MB
% 22.48/3.80 % (1342367)Instructions burned: 479 (million)
% 22.48/3.80 % (1342439)fmb+10_1_sil=64000:random_seed=3080416682:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 22.48/3.80 % (1342439)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 22.48/3.80 % Exception at run slice level
% 22.48/3.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.48/3.80 % (1342441)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3992119911:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 22.48/3.80 % Exception at run slice level
% 22.48/3.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.48/3.80 % (1342364)Instruction limit reached!
% 22.48/3.80 % (1342364)------------------------------
% 22.48/3.80 % (1342364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.48/3.80 % (1342364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.48/3.80 % (1342364)CaDiCaL version: 2.1.3
% 22.48/3.80 % (1342364)Termination reason: Instruction limit
% 22.48/3.80 % (1342364)Termination phase: Saturation
% 22.48/3.80 % (1342364)Time elapsed: 0.368 s
% 22.48/3.80 % (1342364)Peak memory usage: 16 MB
% 22.48/3.80 % (1342364)Instructions burned: 685 (million)
% 22.48/3.80 % (1342443)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1936741945:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 22.48/3.80 % Exception at run slice level
% 25.04/8.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 25.04/8.32 % (1342444)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1164839600:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 25.04/8.32 % (1342447)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1034497917:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi)
% 25.04/8.32 % (1342447)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 25.04/8.32 % (1342395)Instruction limit reached!
% 25.04/8.32 % (1342395)------------------------------
% 25.04/8.32 % (1342395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.32 % (1342395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.32 % (1342395)CaDiCaL version: 2.1.3
% 25.04/8.32 % (1342395)Termination reason: Instruction limit
% 25.04/8.32 % (1342395)Termination phase: Saturation
% 25.04/8.32 % (1342395)Time elapsed: 0.409 s
% 25.04/8.32 % (1342395)Peak memory usage: 20 MB
% 25.04/8.32 % (1342395)Instructions burned: 693 (million)
% 25.04/8.32 % (1342449)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2899760935:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 25.04/8.32 % Exception at run slice level
% 25.04/8.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 25.04/8.32 % (1342451)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=202171230:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 25.04/8.32 % Exception at run slice level
% 25.04/8.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 25.04/8.32 % (1342453)ott-2_1_sil=16000:newcnf=on:random_seed=2132379045:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 25.04/8.32 % (1342405)Instruction limit reached!
% 25.04/8.32 % (1342405)------------------------------
% 25.04/8.32 % (1342405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.32 % (1342405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.32 % (1342405)CaDiCaL version: 2.1.3
% 25.04/8.32 % (1342405)Termination reason: Instruction limit
% 25.04/8.32 % (1342405)Termination phase: Saturation
% 25.04/8.32 % (1342405)Time elapsed: 0.488 s
% 25.04/8.32 % (1342405)Peak memory usage: 19 MB
% 25.04/8.32 % (1342405)Instructions burned: 879 (million)
% 25.04/8.32 % (1342455)ott+10_1_sil=32000:tgt=ground:random_seed=2142435096:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 25.04/8.32 % (1342388)Instruction limit reached!
% 25.04/8.32 % (1342388)------------------------------
% 25.04/8.32 % (1342388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.32 % (1342388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.32 % (1342388)CaDiCaL version: 2.1.3
% 25.04/8.32 % (1342388)Termination reason: Instruction limit
% 25.04/8.32 % (1342388)Termination phase: Saturation
% 25.04/8.32 % (1342388)Time elapsed: 0.667 s
% 25.04/8.32 % (1342388)Peak memory usage: 25 MB
% 25.04/8.32 % (1342388)Instructions burned: 1180 (million)
% 25.04/8.32 % (1342457)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3603880804:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 25.04/8.32 % Exception at run slice level
% 25.04/8.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 25.04/8.32 % (1342459)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3318680837:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 25.04/8.32 % (1342453)Instruction limit reached!
% 25.04/8.32 % (1342453)------------------------------
% 25.04/8.32 % (1342453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.32 % (1342453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.32 % (1342453)CaDiCaL version: 2.1.3
% 25.04/8.32 % (1342453)Termination reason: Instruction limit
% 25.04/8.32 % (1342453)Termination phase: Saturation
% 25.04/8.32 % (1342453)Time elapsed: 0.518 s
% 25.04/8.32 % (1342453)Peak memory usage: 20 MB
% 25.04/8.32 % (1342453)Instructions burned: 870 (million)
% 25.04/8.32 % (1342461)dis+21_1_sil=32000:sas=cadical:random_seed=3458984295:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi)
% 25.04/8.32 % (1342447)Instruction limit reached!
% 25.04/8.32 % (1342447)------------------------------
% 25.04/8.32 % (1342447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.33 % (1342447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.33 % (1342447)CaDiCaL version: 2.1.3
% 25.04/8.33 % (1342447)Termination reason: Instruction limit
% 25.04/8.33 % (1342447)Termination phase: Saturation
% 25.04/8.33 % (1342447)Time elapsed: 0.740 s
% 25.04/8.33 % (1342447)Peak memory usage: 26 MB
% 25.04/8.33 % (1342447)Instructions burned: 1474 (million)
% 25.04/8.33 % (1342463)ott+11_1_sil=16000:gs=on:random_seed=3753491255:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 25.04/8.33 % (1342463)Instruction limit reached!
% 25.04/8.33 % (1342463)------------------------------
% 25.04/8.33 % (1342463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.33 % (1342463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.33 % (1342463)CaDiCaL version: 2.1.3
% 25.04/8.33 % (1342463)Termination reason: Instruction limit
% 25.04/8.33 % (1342463)Termination phase: Saturation
% 25.04/8.33 % (1342463)Time elapsed: 1.116 s
% 25.04/8.33 % (1342463)Peak memory usage: 26 MB
% 25.04/8.33 % (1342463)Instructions burned: 2252 (million)
% 25.04/8.33 % (1342465)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3952234305:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi)
% 25.04/8.33 % Exception at run slice level
% 25.04/8.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 25.04/8.33 % (1342467)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3292709506:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2975 on theBenchmark for (2975ds/4591Mi)
% 25.04/8.33 % (1342459)Instruction limit reached!
% 25.04/8.33 % (1342459)------------------------------
% 25.04/8.33 % (1342459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.33 % (1342459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.33 % (1342459)CaDiCaL version: 2.1.3
% 25.04/8.33 % (1342459)Termination reason: Instruction limit
% 25.04/8.33 % (1342459)Termination phase: Saturation
% 25.04/8.33 % (1342459)Time elapsed: 1.817 s
% 25.04/8.33 % (1342459)Peak memory usage: 40 MB
% 25.04/8.33 % (1342459)Instructions burned: 3512 (million)
% 25.04/8.33 % (1342469)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3479477094:i=29340_2972 on theBenchmark for (2972ds/29340Mi)
% 25.04/8.33 % (1342444)Instruction limit reached!
% 25.04/8.33 % (1342444)------------------------------
% 25.04/8.33 % (1342444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.33 % (1342444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.33 % (1342444)CaDiCaL version: 2.1.3
% 25.04/8.33 % (1342444)Termination reason: Instruction limit
% 25.04/8.33 % (1342444)Termination phase: Saturation
% 25.04/8.33 % (1342444)Time elapsed: 2.667 s
% 25.04/8.33 % (1342444)Peak memory usage: 43 MB
% 25.04/8.33 % (1342444)Instructions burned: 5131 (million)
% 25.04/8.33 % (1342471)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2718953784:i=5211_2968 on theBenchmark for (2968ds/5211Mi)
% 25.04/8.33 % (1342461)Instruction limit reached!
% 25.04/8.33 % (1342461)------------------------------
% 25.04/8.33 % (1342461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.33 % (1342461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.33 % (1342461)CaDiCaL version: 2.1.3
% 25.04/8.33 % (1342461)Termination reason: Instruction limit
% 25.04/8.33 % (1342461)Termination phase: Saturation
% 25.04/8.33 % (1342461)Time elapsed: 2.068 s
% 25.04/8.33 % (1342461)Peak memory usage: 38 MB
% 25.04/8.33 % (1342461)Instructions burned: 3773 (million)
% 25.04/8.33 % (1342473)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=597274376:i=5497:nm=2_2966 on theBenchmark for (2966ds/5497Mi)
% 25.04/8.33 % Exception at run slice level
% 25.04/8.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 25.04/8.33 % (1342475)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1118217138:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi)
% 25.04/8.33 % Exception at run slice level
% 25.04/8.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 25.04/8.33 % (1342477)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1949164422:i=14071_2966 on theBenchmark for (2966ds/14071Mi)
% 25.04/8.33 % Exception at run slice level
% 25.04/8.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 25.04/8.33 % (1342479)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3205843703:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi)
% 25.04/8.33 % (1342455)Instruction limit reached!
% 25.04/8.33 % (1342455)------------------------------
% 25.04/8.33 % (1342455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.33 % (1342455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.33 % (1342455)CaDiCaL version: 2.1.3
% 25.04/8.33 % (1342455)Termination reason: Instruction limit
% 25.04/8.33 % (1342455)Termination phase: Saturation
% 25.04/8.33 % (1342455)Time elapsed: 2.919 s
% 25.04/8.33 % (1342455)Peak memory usage: 57 MB
% 25.04/8.33 % (1342455)Instructions burned: 5116 (million)
% 25.04/8.33 % (1342481)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3920181942:i=8173:av=off_2963 on theBenchmark for (2963ds/8173Mi)
% 25.04/8.33 % (1342467)Instruction limit reached!
% 25.04/8.33 % (1342467)------------------------------
% 25.04/8.33 % (1342467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.33 % (1342467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.33 % (1342467)CaDiCaL version: 2.1.3
% 25.04/8.33 % (1342467)Termination reason: Instruction limit
% 25.04/8.33 % (1342467)Termination phase: Saturation
% 25.04/8.33 % (1342467)Time elapsed: 2.293 s
% 25.04/8.33 % (1342467)Peak memory usage: 60 MB
% 25.04/8.33 % (1342467)Instructions burned: 4591 (million)
% 25.04/8.33 % (1342483)dis+10_16:1_sil=16000:random_seed=2776818307:i=9155:fsr=off_2952 on theBenchmark for (2952ds/9155Mi)
% 25.04/8.33 % (1342471)Instruction limit reached!
% 25.04/8.33 % (1342471)------------------------------
% 25.04/8.33 % (1342471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.33 % (1342471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.33 % (1342471)CaDiCaL version: 2.1.3
% 25.04/8.33 % (1342471)Termination reason: Instruction limit
% 25.04/8.33 % (1342471)Termination phase: Saturation
% 25.04/8.33 % (1342471)Time elapsed: 2.671 s
% 25.04/8.33 % (1342471)Peak memory usage: 44 MB
% 25.04/8.33 % (1342471)Instructions burned: 5212 (million)
% 25.04/8.33 % (1342485)ott-3_8_sil=64000:random_seed=2766754108:i=20139:bs=on_2941 on theBenchmark for (2941ds/20139Mi)
% 25.04/8.33 % (1342481) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1342315-1342481"...
% 25.04/8.33 % (1342481)...printing done.
% 25.04/8.33 % (1342481)Refutation found. Thanks to Tanya!
% 25.04/8.33 % SZS status Theorem for theBenchmark
% 25.04/8.33 % SZS output start Proof for theBenchmark
% See solution above
% 25.04/8.33 % (1342481)------------------------------
% 25.04/8.33 % (1342481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.04/8.33 % (1342481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.04/8.33 % (1342481)CaDiCaL version: 2.1.3
% 25.04/8.33 % (1342481)Termination reason: Refutation
% 25.04/8.33 % (1342481)Time elapsed: 4.161 s
% 25.04/8.33 % (1342481)Peak memory usage: 79 MB
% 25.04/8.33 % (1342481)Instructions burned: 7521 (million)
% 25.04/8.33 % (1342315)Success in time 7.9 s
% 25.04/8.33 % Vampire exiting
%------------------------------------------------------------------------------