%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT169+7 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:37:05 PM UTC 2026
% Result : Theorem 71.32s 19.23s
% Output : Refutation 129.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 27
% Syntax : Number of formulae : 164 ( 46 unt; 4 def)
% Number of atoms : 357 ( 114 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 321 ( 128 ~; 159 |; 20 &)
% ( 10 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 5 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 10 con; 0-4 aty)
% Number of variables : 271 ( 0 sgn 260 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f85,axiom,
! [X0,X1,X2,X3] : hAPP(X0,X1,X2,ti(X0,X3)) = hAPP(X0,X1,X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_hAPP_arg2) ).
fof(f86,axiom,
! [X0,X1,X2,X3] : ti(X0,hAPP(X1,X0,X2,X3)) = hAPP(X1,X0,X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_hAPP_res) ).
fof(f89,axiom,
ti(arrow_2142409994le_alt,a) = a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_v_a_res) ).
fof(f90,axiom,
ti(arrow_2142409994le_alt,b) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_v_b_res) ).
fof(f91,axiom,
? [X0,X1,X2] : hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X1),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X2),nil(arrow_2142409994le_alt)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_alt3) ).
fof(f92,axiom,
! [X0] : hBOOL(hAPP(list(X0),bool,distinct(X0),nil(X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_distinct_Osimps_I1_J) ).
fof(f101,axiom,
! [X0,X1] : hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),insert(X0),X1),nil(X0)) = hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),nil(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_10_insert__Nil) ).
fof(f105,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP(list(X0),bool,distinct(X0),X2))
=> hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),insert(X0),X1),X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_14_distinct__insert) ).
fof(f143,axiom,
! [X0,X1,X2] :
( X1 = X2
=> X1 = hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),nil(X0)),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_52_eq__Nil__appendI) ).
fof(f167,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2))
<=> hBOOL(hAPP(X0,bool,X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_76_mem__def) ).
fof(f198,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X2),X3))
=> hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X2),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X3))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_107_insert) ).
fof(f200,axiom,
! [X0,X1,X2] : hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X1),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_109_elem) ).
fof(f220,axiom,
! [X0,X1,X2] :
( hAPP(X0,list(X0),hAPP(nat,fun(X0,list(X0)),replicate(X0),X1),X2) = nil(X0)
<=> X1 = zero_zero(nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_129_replicate__empty) ).
fof(f238,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X3))))
=> ( ti(X0,X1) = ti(X0,X2)
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X3))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_147_set__ConsD) ).
fof(f249,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X1),X2))
<=> hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_158_ListMem__iff) ).
fof(f257,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))
<=> ( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
& hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_166_distinct_Osimps_I2_J) ).
fof(f258,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(X0,list(X0),hAPP(nat,fun(X0,list(X0)),replicate(X0),X2),X3))))
<=> ( ti(X0,X1) = ti(X0,X3)
& X2 != zero_zero(nat) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_167_in__set__replicate) ).
fof(f273,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
<=> ? [X3,X4] :
( X2 = hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),X3),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X4))
& ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X3))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_182_in__set__conv__decomp__first) ).
fof(f1134,axiom,
hBOOL(fTrue),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fTrue_1_1_U) ).
fof(f1142,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(f1143,axiom,
! [X0] :
( ti(bool,X0) = fTrue
| ti(bool,X0) = fFalse ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fFalse_1_1_T) ).
fof(f1146,axiom,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1147,conjecture,
? [X0] : hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
fof(f1148,negated_conjecture,
~ ? [X0] : hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))))),
inference(negated_conjecture,[status(cth)],[f1147]) ).
fof(f1209,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),insert(X0),X1),X2)))
| ~ hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) ),
inference(ennf_transformation,[],[f105]) ).
fof(f1221,plain,
! [X0,X1,X2] :
( X1 = hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),nil(X0)),X2)
| X1 != X2 ),
inference(ennf_transformation,[],[f143]) ).
fof(f1246,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X2),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X3)))
| ~ hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X2),X3)) ),
inference(ennf_transformation,[],[f198]) ).
fof(f1274,plain,
! [X0,X1,X2,X3] :
( ti(X0,X1) = ti(X0,X2)
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X3)))
| ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X3)))) ),
inference(ennf_transformation,[],[f238]) ).
fof(f1275,plain,
! [X0,X1,X2,X3] :
( ti(X0,X1) = ti(X0,X2)
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X3)))
| ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X3)))) ),
inference(flattening,[],[f1274]) ).
fof(f1986,plain,
! [X0] : ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))))),
inference(ennf_transformation,[],[f1148]) ).
fof(f1990,plain,
hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK1),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK2),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK3),nil(arrow_2142409994le_alt)))))),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3)],[f91]) ).
fof(f2034,plain,
! [X0,X1,X2] :
( ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2))
| ~ hBOOL(hAPP(X0,bool,X2,X1)) )
& ( hBOOL(hAPP(X0,bool,X2,X1))
| ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f167]) ).
fof(f2057,plain,
! [X0,X1,X2] :
( ( hAPP(X0,list(X0),hAPP(nat,fun(X0,list(X0)),replicate(X0),X1),X2) = nil(X0)
| zero_zero(nat) != X1 )
& ( X1 = zero_zero(nat)
| nil(X0) != hAPP(X0,list(X0),hAPP(nat,fun(X0,list(X0)),replicate(X0),X1),X2) ) ),
inference(nnf_transformation,[],[f220]) ).
fof(f2074,plain,
! [X0,X1,X2] :
( ( hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X1),X2))
| ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2))) )
& ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
| ~ hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f249]) ).
fof(f2076,plain,
! [X0,X1,X2] :
( ( hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
| ~ hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) )
& ( ( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
& hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) )
| ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2))) ) ),
inference(nnf_transformation,[],[f257]) ).
fof(f2077,plain,
! [X0,X1,X2] :
( ( hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
| ~ hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) )
& ( ( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
& hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) )
| ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2))) ) ),
inference(flattening,[],[f2076]) ).
fof(f2078,plain,
! [X0,X1,X2,X3] :
( ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(X0,list(X0),hAPP(nat,fun(X0,list(X0)),replicate(X0),X2),X3))))
| ti(X0,X3) != ti(X0,X1)
| zero_zero(nat) = X2 )
& ( ( ti(X0,X1) = ti(X0,X3)
& X2 != zero_zero(nat) )
| ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(X0,list(X0),hAPP(nat,fun(X0,list(X0)),replicate(X0),X2),X3)))) ) ),
inference(nnf_transformation,[],[f258]) ).
fof(f2079,plain,
! [X0,X1,X2,X3] :
( ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(X0,list(X0),hAPP(nat,fun(X0,list(X0)),replicate(X0),X2),X3))))
| ti(X0,X3) != ti(X0,X1)
| zero_zero(nat) = X2 )
& ( ( ti(X0,X1) = ti(X0,X3)
& X2 != zero_zero(nat) )
| ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(X0,list(X0),hAPP(nat,fun(X0,list(X0)),replicate(X0),X2),X3)))) ) ),
inference(flattening,[],[f2078]) ).
fof(f2099,plain,
! [X0,X1,X2] :
( ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
| ! [X3,X4] :
( hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),X3),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X4)) != X2
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X3))) ) )
& ( ? [X3,X4] :
( X2 = hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),X3),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X4))
& ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X3))) )
| ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2))) ) ),
inference(nnf_transformation,[],[f273]) ).
fof(f2100,plain,
! [X0,X1,X2] :
( ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
| ! [X3,X4] :
( hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),X3),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X4)) != X2
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X3))) ) )
& ( ? [X5,X6] :
( hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),X5),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X6)) = X2
& ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X5))) )
| ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2))) ) ),
inference(rectify,[],[f2099]) ).
fof(f2101,plain,
! [X0,X1,X2] :
( ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
| ! [X3,X4] :
( hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),X3),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X4)) != X2
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X3))) ) )
& ( ( hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),sK52(X0,X1,X2)),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),sK53(X0,X1,X2))) = X2
& ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),sK52(X0,X1,X2)))) )
| ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52,sK53]),skolemize(X5,sK52(X0,X1,X2)),skolemize(X6,sK53(X0,X1,X2))],[f2100]) ).
fof(f2535,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,X2,X3) = hAPP(X0,X1,X2,ti(X0,X3)),
inference(cnf_transformation,[],[f85]) ).
fof(f2536,plain,
! [X2,X3,X0,X1] : hAPP(X1,X0,X2,X3) = ti(X0,hAPP(X1,X0,X2,X3)),
inference(cnf_transformation,[],[f86]) ).
fof(f2540,plain,
a = ti(arrow_2142409994le_alt,a),
inference(cnf_transformation,[],[f89]) ).
fof(f2541,plain,
b = ti(arrow_2142409994le_alt,b),
inference(cnf_transformation,[],[f90]) ).
fof(f2542,plain,
hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK1),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK2),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK3),nil(arrow_2142409994le_alt)))))),
inference(cnf_transformation,[],[f1990]) ).
fof(f2543,plain,
! [X0] : hBOOL(hAPP(list(X0),bool,distinct(X0),nil(X0))),
inference(cnf_transformation,[],[f92]) ).
fof(f2555,plain,
! [X0,X1] : hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),insert(X0),X1),nil(X0)) = hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),nil(X0)),
inference(cnf_transformation,[],[f101]) ).
fof(f2561,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),insert(X0),X1),X2)))
| ~ hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) ),
inference(cnf_transformation,[],[f1209]) ).
fof(f2618,plain,
! [X2,X0,X1] :
( hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),nil(X0)),X2) = X1
| X1 != X2 ),
inference(cnf_transformation,[],[f1221]) ).
fof(f2666,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2))
| hBOOL(hAPP(X0,bool,X2,X1)) ),
inference(cnf_transformation,[],[f2034]) ).
fof(f2667,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2))
| ~ hBOOL(hAPP(X0,bool,X2,X1)) ),
inference(cnf_transformation,[],[f2034]) ).
fof(f2707,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X2),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X3)))
| ~ hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X2),X3)) ),
inference(cnf_transformation,[],[f1246]) ).
fof(f2711,plain,
! [X2,X0,X1] : hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X1),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2))),
inference(cnf_transformation,[],[f200]) ).
fof(f2747,plain,
! [X2,X0,X1] :
( nil(X0) = hAPP(X0,list(X0),hAPP(nat,fun(X0,list(X0)),replicate(X0),X1),X2)
| zero_zero(nat) != X1 ),
inference(cnf_transformation,[],[f2057]) ).
fof(f2783,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X3))))
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X3)))
| ti(X0,X1) = ti(X0,X2) ),
inference(cnf_transformation,[],[f1275]) ).
fof(f2803,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
| ~ hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X1),X2)) ),
inference(cnf_transformation,[],[f2074]) ).
fof(f2804,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
| hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X1),X2)) ),
inference(cnf_transformation,[],[f2074]) ).
fof(f2813,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))
| hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) ),
inference(cnf_transformation,[],[f2077]) ).
fof(f2814,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
| ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2))) ),
inference(cnf_transformation,[],[f2077]) ).
fof(f2815,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
| hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))
| ~ hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) ),
inference(cnf_transformation,[],[f2077]) ).
fof(f2816,plain,
! [X2,X3,X0,X1] :
( zero_zero(nat) != X2
| ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(X0,list(X0),hAPP(nat,fun(X0,list(X0)),replicate(X0),X2),X3)))) ),
inference(cnf_transformation,[],[f2079]) ).
fof(f2849,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
| hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),X3),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X4)) != X2
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X3))) ),
inference(cnf_transformation,[],[f2101]) ).
fof(f4063,plain,
hBOOL(fTrue),
inference(cnf_transformation,[],[f1134]) ).
fof(f4071,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[],[f1142]) ).
fof(f4072,plain,
! [X0] :
( fTrue = ti(bool,X0)
| fFalse = ti(bool,X0) ),
inference(cnf_transformation,[],[f1143]) ).
fof(f4075,plain,
a != b,
inference(cnf_transformation,[],[f1146]) ).
fof(f4076,plain,
! [X0] : ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))))),
inference(cnf_transformation,[],[f1986]) ).
fof(f4127,plain,
! [X2,X0] : hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),nil(X0)),X2) = X2,
inference(equality_resolution,[],[f2618]) ).
fof(f4160,plain,
! [X2,X0] : nil(X0) = hAPP(X0,list(X0),hAPP(nat,fun(X0,list(X0)),replicate(X0),zero_zero(nat)),X2),
inference(equality_resolution,[],[f2747]) ).
fof(f4165,plain,
! [X3,X0,X1] : ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(X0,list(X0),hAPP(nat,fun(X0,list(X0)),replicate(X0),zero_zero(nat)),X3)))),
inference(equality_resolution,[],[f2816]) ).
fof(f4170,plain,
! [X3,X0,X1,X4] :
( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(list(X0),fun(list(X0),list(X0)),append(X0),X3),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X4)))))
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X3))) ),
inference(equality_resolution,[],[f2849]) ).
fof(f4347,plain,
! [X0,X1] : ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),nil(X0)))),
inference(backward_demodulation,[],[f4165,f4160]) ).
fof(f4441,plain,
hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK2),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK3),nil(arrow_2142409994le_alt))))),
inference(resolution,[],[f2813,f2542]) ).
fof(f4656,plain,
! [X0,X1] :
( hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),nil(X0))))
| ~ hBOOL(hAPP(list(X0),bool,distinct(X0),nil(X0))) ),
inference(superposition,[],[f2561,f2555]) ).
fof(f4658,plain,
! [X0,X1] : hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),nil(X0)))),
inference(forward_subsumption_resolution,[],[f4656,f2543]) ).
fof(f5153,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2))))
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),nil(X0)))) ),
inference(superposition,[],[f4170,f4127]) ).
fof(f5154,plain,
! [X2,X0,X1] : hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))),
inference(forward_subsumption_resolution,[],[f5153,f4347]) ).
fof(f5204,plain,
! [X2,X0,X1] :
( fTrue = hAPP(X0,bool,X1,X2)
| fFalse = hAPP(X0,bool,X1,X2) ),
inference(superposition,[],[f4072,f2536]) ).
fof(f5560,plain,
! [X0] :
( ~ hBOOL(fTrue)
| fFalse = hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt))))) ),
inference(superposition,[],[f4076,f5204]) ).
fof(f5564,plain,
! [X0] : fFalse = hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt))))),
inference(forward_subsumption_resolution,[],[f5560,f4063]) ).
fof(f6291,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X1),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X3)))
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X3)))
| ti(X0,X1) = ti(X0,X2) ),
inference(resolution,[],[f2803,f2783]) ).
fof(f6378,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(X0,bool,hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)),X3))
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X3),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
| ti(X0,X3) = ti(X0,X1) ),
inference(resolution,[],[f2667,f2783]) ).
fof(f12148,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))
| ~ hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X1),X2)) ),
inference(resolution,[],[f2814,f2803]) ).
fof(f12401,definition,
( spl274_67
<=> ti(arrow_2142409994le_alt,sK2) = ti(arrow_2142409994le_alt,sK1) ),
introduced(definition,[new_symbols(definition,[spl274_67])],[avatar_definition]) ).
fof(f12402,plain,
( ti(arrow_2142409994le_alt,sK2) != ti(arrow_2142409994le_alt,sK1)
| spl274_67 ),
inference(avatar_component_clause,[],[f12401]) ).
fof(f12403,plain,
( ti(arrow_2142409994le_alt,sK2) = ti(arrow_2142409994le_alt,sK1)
| ~ spl274_67 ),
inference(avatar_component_clause,[],[f12401]) ).
fof(f12411,plain,
( ! [X0,X1] : hAPP(arrow_2142409994le_alt,X0,X1,sK2) = hAPP(arrow_2142409994le_alt,X0,X1,ti(arrow_2142409994le_alt,sK1))
| ~ spl274_67 ),
inference(superposition,[],[f2535,f12403]) ).
fof(f12412,plain,
( ! [X0,X1] : hAPP(arrow_2142409994le_alt,X0,X1,sK2) = hAPP(arrow_2142409994le_alt,X0,X1,sK1)
| ~ spl274_67 ),
inference(forward_demodulation,[],[f12411,f2535]) ).
fof(f12413,plain,
( hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK1),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK1),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK3),nil(arrow_2142409994le_alt))))))
| ~ spl274_67 ),
inference(backward_demodulation,[],[f2542,f12412]) ).
fof(f12771,plain,
! [X2,X0,X1] : ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))),
inference(resolution,[],[f5154,f2814]) ).
fof(f16885,plain,
( $false
| ~ spl274_67 ),
inference(forward_subsumption_resolution,[],[f12413,f12771]) ).
fof(f16886,plain,
~ spl274_67,
inference(avatar_contradiction_clause,[],[f16885]) ).
fof(f21892,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X1)))
| hBOOL(hAPP(X0,bool,hAPP(list(X0),fun(X0,bool),set(X0),X1),X2))
| ~ hBOOL(hAPP(list(X0),bool,distinct(X0),X1)) ),
inference(resolution,[],[f2666,f2815]) ).
fof(f21996,plain,
! [X0] :
( hBOOL(fFalse)
| hBOOL(hAPP(arrow_2142409994le_alt,bool,hAPP(list(arrow_2142409994le_alt),fun(arrow_2142409994le_alt,bool),set(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))),a))
| ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt))))) ),
inference(superposition,[],[f21892,f5564]) ).
fof(f22001,plain,
! [X0] :
( hBOOL(hAPP(arrow_2142409994le_alt,bool,hAPP(list(arrow_2142409994le_alt),fun(arrow_2142409994le_alt,bool),set(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))),a))
| ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt))))) ),
inference(forward_subsumption_resolution,[],[f21996,f4071]) ).
fof(f22005,plain,
! [X0] :
( ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))))
| hBOOL(hAPP(fun(arrow_2142409994le_alt,bool),bool,hAPP(arrow_2142409994le_alt,fun(fun(arrow_2142409994le_alt,bool),bool),member(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),fun(arrow_2142409994le_alt,bool),set(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))))
| ti(arrow_2142409994le_alt,a) = ti(arrow_2142409994le_alt,b) ),
inference(resolution,[],[f22001,f6378]) ).
fof(f22013,plain,
! [X0] :
( ti(arrow_2142409994le_alt,a) = b
| ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))))
| hBOOL(hAPP(fun(arrow_2142409994le_alt,bool),bool,hAPP(arrow_2142409994le_alt,fun(fun(arrow_2142409994le_alt,bool),bool),member(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),fun(arrow_2142409994le_alt,bool),set(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt))))) ),
inference(forward_demodulation,[],[f22005,f2541]) ).
fof(f22015,plain,
! [X0] :
( a = b
| ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))))
| hBOOL(hAPP(fun(arrow_2142409994le_alt,bool),bool,hAPP(arrow_2142409994le_alt,fun(fun(arrow_2142409994le_alt,bool),bool),member(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),fun(arrow_2142409994le_alt,bool),set(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt))))) ),
inference(forward_demodulation,[],[f22013,f2540]) ).
fof(f22017,plain,
! [X0] :
( hBOOL(hAPP(fun(arrow_2142409994le_alt,bool),bool,hAPP(arrow_2142409994le_alt,fun(fun(arrow_2142409994le_alt,bool),bool),member(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),fun(arrow_2142409994le_alt,bool),set(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))))
| ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt))))) ),
inference(forward_subsumption_resolution,[],[f22015,f4075]) ).
fof(f22025,plain,
! [X0] :
( ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))))
| hBOOL(hAPP(fun(arrow_2142409994le_alt,bool),bool,hAPP(arrow_2142409994le_alt,fun(fun(arrow_2142409994le_alt,bool),bool),member(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),fun(arrow_2142409994le_alt,bool),set(arrow_2142409994le_alt),nil(arrow_2142409994le_alt))))
| ti(arrow_2142409994le_alt,a) = ti(arrow_2142409994le_alt,X0) ),
inference(resolution,[],[f22017,f2783]) ).
fof(f22033,plain,
! [X0] :
( ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))))
| ti(arrow_2142409994le_alt,a) = ti(arrow_2142409994le_alt,X0) ),
inference(forward_subsumption_resolution,[],[f22025,f4347]) ).
fof(f22034,plain,
! [X0] :
( ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt)))))
| a = ti(arrow_2142409994le_alt,X0) ),
inference(forward_demodulation,[],[f22033,f2540]) ).
fof(f22439,plain,
~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),bool),listMem(arrow_2142409994le_alt),sK1),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK2),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK3),nil(arrow_2142409994le_alt))))),
inference(resolution,[],[f12148,f2542]) ).
fof(f22469,plain,
~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),bool),listMem(arrow_2142409994le_alt),sK1),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK3),nil(arrow_2142409994le_alt)))),
inference(resolution,[],[f22439,f2707]) ).
fof(f25552,plain,
! [X2,X0,X1] :
( ~ hBOOL(fTrue)
| fFalse = hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2))) ),
inference(superposition,[],[f12771,f5204]) ).
fof(f25553,plain,
! [X2,X0,X1] : fFalse = hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2))),
inference(forward_subsumption_resolution,[],[f25552,f4063]) ).
fof(f28444,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))
| hBOOL(hAPP(list(X0),bool,hAPP(X0,fun(list(X0),bool),listMem(X0),X1),X2))
| ~ hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) ),
inference(resolution,[],[f2804,f2815]) ).
fof(f28603,plain,
! [X0] :
( hBOOL(hAPP(list(arrow_2142409994le_alt),bool,hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),bool),listMem(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt))))
| ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt))))
| a = ti(arrow_2142409994le_alt,X0) ),
inference(resolution,[],[f28444,f22034]) ).
fof(f28637,plain,
! [X0] :
( hBOOL(hAPP(list(arrow_2142409994le_alt),bool,hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),bool),listMem(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt))))
| a = ti(arrow_2142409994le_alt,X0) ),
inference(forward_subsumption_resolution,[],[f28603,f4658]) ).
fof(f29131,plain,
! [X0] :
( a = ti(arrow_2142409994le_alt,X0)
| hBOOL(hAPP(fun(arrow_2142409994le_alt,bool),bool,hAPP(arrow_2142409994le_alt,fun(fun(arrow_2142409994le_alt,bool),bool),member(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),fun(arrow_2142409994le_alt,bool),set(arrow_2142409994le_alt),nil(arrow_2142409994le_alt))))
| ti(arrow_2142409994le_alt,b) = ti(arrow_2142409994le_alt,X0) ),
inference(resolution,[],[f28637,f6291]) ).
fof(f29151,plain,
! [X0] :
( a = ti(arrow_2142409994le_alt,X0)
| ti(arrow_2142409994le_alt,b) = ti(arrow_2142409994le_alt,X0) ),
inference(forward_subsumption_resolution,[],[f29131,f4347]) ).
fof(f29152,plain,
! [X0] :
( b = ti(arrow_2142409994le_alt,X0)
| a = ti(arrow_2142409994le_alt,X0) ),
inference(forward_demodulation,[],[f29151,f2541]) ).
fof(f29156,plain,
( b != ti(arrow_2142409994le_alt,sK1)
| a = ti(arrow_2142409994le_alt,sK2)
| spl274_67 ),
inference(superposition,[],[f12402,f29152]) ).
fof(f29157,plain,
! [X2,X0,X1] :
( hAPP(arrow_2142409994le_alt,X0,X1,b) = hAPP(arrow_2142409994le_alt,X0,X1,X2)
| a = ti(arrow_2142409994le_alt,X2) ),
inference(superposition,[],[f2535,f29152]) ).
fof(f29171,definition,
( spl274_95
<=> a = ti(arrow_2142409994le_alt,sK2) ),
introduced(definition,[new_symbols(definition,[spl274_95])],[avatar_definition]) ).
fof(f29172,plain,
( a != ti(arrow_2142409994le_alt,sK2)
| spl274_95 ),
inference(avatar_component_clause,[],[f29171]) ).
fof(f29173,plain,
( a = ti(arrow_2142409994le_alt,sK2)
| ~ spl274_95 ),
inference(avatar_component_clause,[],[f29171]) ).
fof(f29175,definition,
( spl274_96
<=> b = ti(arrow_2142409994le_alt,sK1) ),
introduced(definition,[new_symbols(definition,[spl274_96])],[avatar_definition]) ).
fof(f29176,plain,
( b = ti(arrow_2142409994le_alt,sK1)
| ~ spl274_96 ),
inference(avatar_component_clause,[],[f29175]) ).
fof(f29177,plain,
( b != ti(arrow_2142409994le_alt,sK1)
| spl274_96 ),
inference(avatar_component_clause,[],[f29175]) ).
fof(f29178,plain,
( spl274_95
| ~ spl274_96
| spl274_67 ),
inference(avatar_split_clause,[],[f29156,f12401,f29175,f29171]) ).
fof(f29347,plain,
( b != b
| a = ti(arrow_2142409994le_alt,sK1)
| spl274_96 ),
inference(superposition,[],[f29177,f29152]) ).
fof(f29348,plain,
( a = ti(arrow_2142409994le_alt,sK1)
| spl274_96 ),
inference(trivial_inequality_removal,[],[f29347]) ).
fof(f29351,plain,
( a != ti(arrow_2142409994le_alt,sK2)
| spl274_67
| spl274_96 ),
inference(backward_demodulation,[],[f12402,f29348]) ).
fof(f29352,plain,
( ~ spl274_95
| spl274_67
| spl274_96 ),
inference(avatar_split_clause,[],[f29351,f29175,f12401,f29171]) ).
fof(f29354,plain,
( ! [X0,X1] : hAPP(arrow_2142409994le_alt,X0,X1,a) = hAPP(arrow_2142409994le_alt,X0,X1,sK1)
| spl274_96 ),
inference(superposition,[],[f2535,f29348]) ).
fof(f29364,plain,
( hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK2),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK3),nil(arrow_2142409994le_alt))))))
| spl274_96 ),
inference(backward_demodulation,[],[f2542,f29354]) ).
fof(f29816,plain,
! [X2,X3,X0,X1] :
( hAPP(arrow_2142409994le_alt,X0,X1,X2) = hAPP(arrow_2142409994le_alt,X0,X1,X3)
| a = ti(arrow_2142409994le_alt,X3)
| a = ti(arrow_2142409994le_alt,X2) ),
inference(superposition,[],[f29157,f29157]) ).
fof(f30106,plain,
( hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK3),nil(arrow_2142409994le_alt))))))
| a = ti(arrow_2142409994le_alt,sK2)
| spl274_96 ),
inference(superposition,[],[f29364,f29157]) ).
fof(f30118,plain,
! [X0,X1] :
( hBOOL(hAPP(list(arrow_2142409994le_alt),bool,hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),bool),listMem(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),X1)))
| a = ti(arrow_2142409994le_alt,X0) ),
inference(superposition,[],[f2711,f29157]) ).
fof(f30449,definition,
( spl274_110
<=> a = ti(arrow_2142409994le_alt,sK3) ),
introduced(definition,[new_symbols(definition,[spl274_110])],[avatar_definition]) ).
fof(f30450,plain,
( a != ti(arrow_2142409994le_alt,sK3)
| spl274_110 ),
inference(avatar_component_clause,[],[f30449]) ).
fof(f30451,plain,
( a = ti(arrow_2142409994le_alt,sK3)
| ~ spl274_110 ),
inference(avatar_component_clause,[],[f30449]) ).
fof(f30463,plain,
( hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK3),nil(arrow_2142409994le_alt))))))
| spl274_95
| spl274_96 ),
inference(forward_subsumption_resolution,[],[f30106,f29172]) ).
fof(f30561,plain,
( hBOOL(fFalse)
| spl274_95
| spl274_96 ),
inference(forward_demodulation,[],[f30463,f5564]) ).
fof(f30584,plain,
( $false
| spl274_95
| spl274_96 ),
inference(forward_subsumption_resolution,[],[f30561,f4071]) ).
fof(f30585,plain,
( spl274_95
| spl274_96 ),
inference(avatar_contradiction_clause,[],[f30584]) ).
fof(f30590,plain,
( ! [X0,X1] : hAPP(arrow_2142409994le_alt,X0,X1,b) = hAPP(arrow_2142409994le_alt,X0,X1,sK1)
| ~ spl274_96 ),
inference(superposition,[],[f2535,f29176]) ).
fof(f30630,plain,
( ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),bool),listMem(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK3),nil(arrow_2142409994le_alt))))
| ~ spl274_96 ),
inference(backward_demodulation,[],[f22469,f30590]) ).
fof(f30635,plain,
( ! [X0,X1] : hAPP(arrow_2142409994le_alt,X0,X1,a) = hAPP(arrow_2142409994le_alt,X0,X1,sK2)
| ~ spl274_95 ),
inference(superposition,[],[f2535,f29173]) ).
fof(f30643,plain,
( hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),sK3),nil(arrow_2142409994le_alt)))))
| ~ spl274_95 ),
inference(backward_demodulation,[],[f4441,f30635]) ).
fof(f30689,plain,
( ! [X0,X1] : hAPP(arrow_2142409994le_alt,X0,X1,a) = hAPP(arrow_2142409994le_alt,X0,X1,sK3)
| ~ spl274_110 ),
inference(superposition,[],[f2535,f30451]) ).
fof(f30703,plain,
( hBOOL(hAPP(list(arrow_2142409994le_alt),bool,distinct(arrow_2142409994le_alt),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),a),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),a),nil(arrow_2142409994le_alt)))))
| ~ spl274_95
| ~ spl274_110 ),
inference(backward_demodulation,[],[f30643,f30689]) ).
fof(f30749,plain,
( hBOOL(fFalse)
| ~ spl274_95
| ~ spl274_110 ),
inference(forward_demodulation,[],[f30703,f25553]) ).
fof(f30755,plain,
( $false
| ~ spl274_95
| ~ spl274_110 ),
inference(forward_subsumption_resolution,[],[f30749,f4071]) ).
fof(f30756,plain,
( ~ spl274_95
| ~ spl274_110 ),
inference(avatar_contradiction_clause,[],[f30755]) ).
fof(f33842,plain,
( ! [X0] :
( ~ hBOOL(hAPP(list(arrow_2142409994le_alt),bool,hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),bool),listMem(arrow_2142409994le_alt),b),hAPP(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(list(arrow_2142409994le_alt),list(arrow_2142409994le_alt)),cons(arrow_2142409994le_alt),X0),nil(arrow_2142409994le_alt))))
| a = ti(arrow_2142409994le_alt,X0)
| a = ti(arrow_2142409994le_alt,sK3) )
| ~ spl274_96 ),
inference(superposition,[],[f30630,f29816]) ).
fof(f33849,plain,
( ! [X0] :
( a = ti(arrow_2142409994le_alt,X0)
| a = ti(arrow_2142409994le_alt,sK3) )
| ~ spl274_96 ),
inference(forward_subsumption_resolution,[],[f33842,f30118]) ).
fof(f33858,plain,
( ! [X0] : a = ti(arrow_2142409994le_alt,X0)
| ~ spl274_96
| spl274_110 ),
inference(forward_subsumption_resolution,[],[f33849,f30450]) ).
fof(f33921,plain,
( a = b
| ~ spl274_96
| spl274_110 ),
inference(backward_demodulation,[],[f29176,f33858]) ).
fof(f33983,plain,
( $false
| ~ spl274_96
| spl274_110 ),
inference(forward_subsumption_resolution,[],[f33921,f4075]) ).
fof(f33984,plain,
( ~ spl274_96
| spl274_110 ),
inference(avatar_contradiction_clause,[],[f33983]) ).
cnf(s366,plain,
~ spl274_67,
inference(sat_conversion,[],[f16886]) ).
cnf(s386,plain,
( spl274_67
| spl274_95
| ~ spl274_96 ),
inference(sat_conversion,[],[f29178]) ).
cnf(s393,plain,
( spl274_67
| ~ spl274_95
| spl274_96 ),
inference(sat_conversion,[],[f29352]) ).
cnf(s404,plain,
( spl274_95
| spl274_96 ),
inference(sat_conversion,[],[f30585]) ).
cnf(s405,plain,
( ~ spl274_95
| ~ spl274_110 ),
inference(sat_conversion,[],[f30756]) ).
cnf(s415,plain,
( ~ spl274_96
| spl274_110 ),
inference(sat_conversion,[],[f33984]) ).
cnf(s429,plain,
spl274_95,
inference(rat,[],[s386,s404,s366]) ).
cnf(s430,plain,
~ spl274_110,
inference(rat,[],[s405,s429]) ).
cnf(s431,plain,
spl274_96,
inference(rat,[],[s393,s366,s429]) ).
cnf(s432,plain,
$false,
inference(rat,[],[s415,s430,s431]) ).
fof(f34043,plain,
$false,
inference(avatar_sat_refutation,[],[s432]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT169+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n001.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Mon Sep 28 00:00:47 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.87/2.51 % (4094807)Detected formulas, will run a generic FOF schedule.
% 10.87/2.51 % (4094814)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2584217385:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 10.87/2.51 % (4094816)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=903360911:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 10.87/2.51 % (4094815)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1629756160:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 10.87/2.51 % (4094817)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1246938082:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 10.87/2.51 % (4094813)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1817773903:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 10.87/2.51 % (4094812)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1248429181:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 10.87/2.51 % (4094818)dis-21_1_sil=8000:lcm=predicate:random_seed=1539823096:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 10.87/2.51 % (4094815)Refutation not found, incomplete strategy
% 10.87/2.51 % (4094815)------------------------------
% 10.87/2.51 % (4094815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.87/2.51 % (4094815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.87/2.51 % (4094815)CaDiCaL version: 2.1.3
% 10.87/2.51 % (4094815)Termination reason: Refutation not found, incomplete strategy
% 10.87/2.51 % (4094815)Time elapsed: 0.014 s
% 10.87/2.51 % (4094815)Peak memory usage: 90 MB
% 10.87/2.51 % (4094815)Instructions burned: 23 (million)
% 10.87/2.51 % (4094816)Instruction limit reached!
% 10.87/2.51 % (4094816)------------------------------
% 10.87/2.51 % (4094816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.87/2.51 % (4094816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.87/2.51 % (4094816)CaDiCaL version: 2.1.3
% 10.87/2.51 % (4094816)Termination reason: Instruction limit
% 10.87/2.51 % (4094816)Termination phase: Saturation
% 10.87/2.51 % (4094816)Time elapsed: 0.053 s
% 10.87/2.51 % (4094816)Peak memory usage: 89 MB
% 10.87/2.51 % (4094816)Instructions burned: 119 (million)
% 10.87/2.51 % (4094818)Instruction limit reached!
% 10.87/2.51 % (4094818)------------------------------
% 10.87/2.51 % (4094818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.87/2.51 % (4094818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.87/2.51 % (4094818)CaDiCaL version: 2.1.3
% 10.87/2.51 % (4094818)Termination reason: Instruction limit
% 10.87/2.51 % (4094818)Termination phase: Function definition elimination
% 10.87/2.51 % (4094818)Time elapsed: 0.056 s
% 10.87/2.51 % (4094818)Peak memory usage: 88 MB
% 10.87/2.51 % (4094818)Instructions burned: 130 (million)
% 10.87/2.51 % (4094817)Instruction limit reached!
% 10.87/2.51 % (4094817)------------------------------
% 10.87/2.51 % (4094817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.87/2.51 % (4094817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.87/2.51 % (4094817)CaDiCaL version: 2.1.3
% 10.87/2.51 % (4094817)Termination reason: Instruction limit
% 10.87/2.51 % (4094817)Termination phase: Property scanning
% 10.87/2.51 % (4094817)Time elapsed: 0.060 s
% 10.87/2.51 % (4094817)Peak memory usage: 88 MB
% 10.87/2.51 % (4094817)Instructions burned: 140 (million)
% 10.87/2.51 % (4094829)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3458012191:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 10.87/2.51 % (4094827)lrs+10_1_sil=8000:sp=occurrence:random_seed=1266103076:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 10.87/2.51 % (4094828)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1474652523:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 10.87/2.51 % (4094815)------------------------------
% 10.87/2.51 % (4094815)------------------------------
% 10.87/2.51 % (4094828)Instruction limit reached!
% 10.87/2.51 % (4094828)------------------------------
% 10.87/2.51 % (4094828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.57 % (4094828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.57 % (4094828)CaDiCaL version: 2.1.3
% 17.73/3.57 % (4094828)Termination reason: Instruction limit
% 17.73/3.57 % (4094828)Termination phase: Saturation
% 17.73/3.57 % (4094828)Time elapsed: 0.078 s
% 17.73/3.57 % (4094828)Peak memory usage: 90 MB
% 17.73/3.57 % (4094828)Instructions burned: 158 (million)
% 17.73/3.57 % (4094827)Instruction limit reached!
% 17.73/3.57 % (4094827)------------------------------
% 17.73/3.57 % (4094827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.57 % (4094827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.57 % (4094827)CaDiCaL version: 2.1.3
% 17.73/3.57 % (4094827)Termination reason: Instruction limit
% 17.73/3.57 % (4094827)Termination phase: Saturation
% 17.73/3.57 % (4094827)Time elapsed: 0.157 s
% 17.73/3.57 % (4094827)Peak memory usage: 91 MB
% 17.73/3.57 % (4094827)Instructions burned: 285 (million)
% 17.73/3.57 % (4094829)Instruction limit reached!
% 17.73/3.57 % (4094829)------------------------------
% 17.73/3.57 % (4094829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.57 % (4094829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.57 % (4094829)CaDiCaL version: 2.1.3
% 17.73/3.57 % (4094829)Termination reason: Instruction limit
% 17.73/3.57 % (4094829)Termination phase: Saturation
% 17.73/3.57 % (4094829)Time elapsed: 0.188 s
% 17.73/3.57 % (4094829)Peak memory usage: 91 MB
% 17.73/3.57 % (4094829)Instructions burned: 326 (million)
% 17.73/3.57 % (4094833)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=761295395:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 17.73/3.57 % (4094834)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=859781990:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 17.73/3.57 % (4094835)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2066546655:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 17.73/3.57 % (4094833)Instruction limit reached!
% 17.73/3.57 % (4094833)------------------------------
% 17.73/3.57 % (4094833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.57 % (4094833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.57 % (4094833)CaDiCaL version: 2.1.3
% 17.73/3.57 % (4094833)Termination reason: Instruction limit
% 17.73/3.57 % (4094833)Termination phase: Saturation
% 17.73/3.57 % (4094833)Time elapsed: 0.116 s
% 17.73/3.57 % (4094833)Peak memory usage: 91 MB
% 17.73/3.57 % (4094833)Instructions burned: 249 (million)
% 17.73/3.57 % (4094836)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2546151491:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 17.73/3.57 % (4094834)Instruction limit reached!
% 17.73/3.57 % (4094834)------------------------------
% 17.73/3.57 % (4094834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.57 % (4094834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.57 % (4094834)CaDiCaL version: 2.1.3
% 17.73/3.57 % (4094834)Termination reason: Instruction limit
% 17.73/3.57 % (4094834)Termination phase: Saturation
% 17.73/3.57 % (4094834)Time elapsed: 0.137 s
% 17.73/3.57 % (4094834)Peak memory usage: 92 MB
% 17.73/3.57 % (4094834)Instructions burned: 294 (million)
% 17.73/3.57 % (4094836)Instruction limit reached!
% 17.73/3.57 % (4094836)------------------------------
% 17.73/3.57 % (4094836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.57 % (4094836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.57 % (4094836)CaDiCaL version: 2.1.3
% 17.73/3.57 % (4094836)Termination reason: Instruction limit
% 17.73/3.57 % (4094836)Termination phase: Property scanning
% 17.73/3.57 % (4094836)Time elapsed: 0.049 s
% 17.73/3.57 % (4094836)Peak memory usage: 88 MB
% 17.73/3.57 % (4094836)Instructions burned: 113 (million)
% 17.73/3.57 % (4094841)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=405936100:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 17.73/3.57 % (4094842)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1371192229:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 17.73/3.57 % (4094842)Instruction limit reached!
% 17.73/3.57 % (4094842)------------------------------
% 40.94/6.93 % (4094842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.94/6.93 % (4094842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.94/6.93 % (4094842)CaDiCaL version: 2.1.3
% 40.94/6.93 % (4094842)Termination reason: Instruction limit
% 40.94/6.93 % (4094842)Termination phase: Property scanning
% 40.94/6.93 % (4094842)Time elapsed: 0.024 s
% 40.94/6.93 % (4094842)Peak memory usage: 87 MB
% 40.94/6.93 % (4094842)Instructions burned: 116 (million)
% 40.94/6.93 % (4094841)Instruction limit reached!
% 40.94/6.93 % (4094841)------------------------------
% 40.94/6.93 % (4094841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.94/6.93 % (4094841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.94/6.93 % (4094841)CaDiCaL version: 2.1.3
% 40.94/6.93 % (4094841)Termination reason: Instruction limit
% 40.94/6.93 % (4094841)Termination phase: Property scanning
% 40.94/6.93 % (4094841)Time elapsed: 0.056 s
% 40.94/6.93 % (4094841)Peak memory usage: 88 MB
% 40.94/6.93 % (4094841)Instructions burned: 130 (million)
% 40.94/6.93 % (4094843)lrs+10_1_sil=8000:sp=occurrence:random_seed=249729009:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 40.94/6.93 % (4094846)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2187063029:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 40.94/6.93 % (4094847)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=645652069:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 40.94/6.93 % (4094846)Instruction limit reached!
% 40.94/6.93 % (4094846)------------------------------
% 40.94/6.93 % (4094846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.94/6.93 % (4094846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.94/6.93 % (4094846)CaDiCaL version: 2.1.3
% 40.94/6.93 % (4094846)Termination reason: Instruction limit
% 40.94/6.93 % (4094846)Termination phase: Saturation
% 40.94/6.93 % (4094846)Time elapsed: 0.117 s
% 40.94/6.93 % (4094846)Peak memory usage: 94 MB
% 40.94/6.93 % (4094846)Instructions burned: 439 (million)
% 40.94/6.93 % (4094851)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1637800606:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 40.94/6.93 % (4094851)Instruction limit reached!
% 40.94/6.93 % (4094851)------------------------------
% 40.94/6.93 % (4094851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.94/6.93 % (4094851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.94/6.93 % (4094851)CaDiCaL version: 2.1.3
% 40.94/6.93 % (4094851)Termination reason: Instruction limit
% 40.94/6.93 % (4094851)Termination phase: Property scanning
% 40.94/6.93 % (4094851)Time elapsed: 0.031 s
% 40.94/6.93 % (4094851)Peak memory usage: 89 MB
% 40.94/6.93 % (4094851)Instructions burned: 134 (million)
% 40.94/6.93 % (4094853)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3627871672:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 40.94/6.93 % (4094853)Instruction limit reached!
% 40.94/6.93 % (4094853)------------------------------
% 40.94/6.93 % (4094853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.94/6.93 % (4094853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.94/6.93 % (4094853)CaDiCaL version: 2.1.3
% 40.94/6.93 % (4094853)Termination reason: Instruction limit
% 40.94/6.93 % (4094853)Termination phase: Saturation
% 40.94/6.93 % (4094853)Time elapsed: 0.149 s
% 40.94/6.93 % (4094853)Peak memory usage: 96 MB
% 40.94/6.93 % (4094853)Instructions burned: 595 (million)
% 40.94/6.93 % (4094843)Instruction limit reached!
% 40.94/6.93 % (4094843)------------------------------
% 40.94/6.93 % (4094843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.94/6.93 % (4094843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.94/6.93 % (4094843)CaDiCaL version: 2.1.3
% 40.94/6.93 % (4094843)Termination reason: Instruction limit
% 40.94/6.93 % (4094843)Termination phase: Saturation
% 40.94/6.93 % (4094843)Time elapsed: 0.526 s
% 40.94/6.93 % (4094843)Peak memory usage: 95 MB
% 40.94/6.93 % (4094843)Instructions burned: 907 (million)
% 40.94/6.93 % (4094855)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3886751722:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 40.94/6.93 % (4094856)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=345964102:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 67.60/10.57 % (4094856)Instruction limit reached!
% 67.60/10.57 % (4094856)------------------------------
% 67.60/10.57 % (4094856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.60/10.57 % (4094856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.60/10.57 % (4094856)CaDiCaL version: 2.1.3
% 67.60/10.57 % (4094856)Termination reason: Instruction limit
% 67.60/10.57 % (4094856)Termination phase: General splitting
% 67.60/10.57 % (4094856)Time elapsed: 0.055 s
% 67.60/10.57 % (4094856)Peak memory usage: 87 MB
% 67.60/10.57 % (4094856)Instructions burned: 127 (million)
% 67.60/10.57 % (4094859)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1421380182:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 67.60/10.57 % (4094859)Instruction limit reached!
% 67.60/10.57 % (4094859)------------------------------
% 67.60/10.57 % (4094859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.60/10.57 % (4094859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.60/10.57 % (4094859)CaDiCaL version: 2.1.3
% 67.60/10.57 % (4094859)Termination reason: Instruction limit
% 67.60/10.57 % (4094859)Termination phase: Preprocessing 3
% 67.60/10.57 % (4094859)Time elapsed: 0.055 s
% 67.60/10.57 % (4094859)Peak memory usage: 87 MB
% 67.60/10.57 % (4094859)Instructions burned: 135 (million)
% 67.60/10.57 % (4094861)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=464865162:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi)
% 67.60/10.57 % (4094861)Refutation not found, incomplete strategy
% 67.60/10.57 % (4094861)------------------------------
% 67.60/10.57 % (4094861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.60/10.57 % (4094861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.60/10.57 % (4094861)CaDiCaL version: 2.1.3
% 67.60/10.57 % (4094861)Termination reason: Refutation not found, incomplete strategy
% 67.60/10.57 % (4094861)Time elapsed: 0.011 s
% 67.60/10.57 % (4094861)Peak memory usage: 89 MB
% 67.60/10.57 % (4094861)Instructions burned: 17 (million)
% 67.60/10.57 % (4094835)Instruction limit reached!
% 67.60/10.57 % (4094835)------------------------------
% 67.60/10.57 % (4094835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.60/10.57 % (4094835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.60/10.57 % (4094835)CaDiCaL version: 2.1.3
% 67.60/10.57 % (4094835)Termination reason: Instruction limit
% 67.60/10.57 % (4094835)Termination phase: Saturation
% 67.60/10.57 % (4094835)Time elapsed: 1.396 s
% 67.60/10.57 % (4094835)Peak memory usage: 159 MB
% 67.60/10.57 % (4094835)Instructions burned: 2350 (million)
% 67.60/10.57 % (4094861)------------------------------
% 67.60/10.57 % (4094861)------------------------------
% 67.60/10.57 % (4094863)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1020141524:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi)
% 67.60/10.57 % (4094864)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3675231960:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi)
% 67.60/10.57 % (4094863)Instruction limit reached!
% 67.60/10.57 % (4094863)------------------------------
% 67.60/10.57 % (4094863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.60/10.57 % (4094863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.60/10.57 % (4094863)CaDiCaL version: 2.1.3
% 67.60/10.57 % (4094863)Termination reason: Instruction limit
% 67.60/10.57 % (4094863)Termination phase: Saturation
% 67.60/10.57 % (4094863)Time elapsed: 0.223 s
% 67.60/10.57 % (4094863)Peak memory usage: 91 MB
% 67.60/10.57 % (4094863)Instructions burned: 431 (million)
% 67.60/10.57 % (4094867)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1449639405:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 67.60/10.57 % (4094867)Instruction limit reached!
% 67.60/10.57 % (4094867)------------------------------
% 67.60/10.57 % (4094867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.60/10.57 % (4094867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.75/14.66 % (4094867)CaDiCaL version: 2.1.3
% 96.75/14.66 % (4094867)Termination reason: Instruction limit
% 96.75/14.66 % (4094867)Termination phase: Property scanning
% 96.75/14.66 % (4094867)Time elapsed: 0.065 s
% 96.75/14.66 % (4094867)Peak memory usage: 88 MB
% 96.75/14.66 % (4094867)Instructions burned: 152 (million)
% 96.75/14.66 % (4094869)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2232215616:i=14155:bd=all_2972 on theBenchmark for (2972ds/14155Mi)
% 96.75/14.66 % (4094847)Instruction limit reached!
% 96.75/14.66 % (4094847)------------------------------
% 96.75/14.66 % (4094847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.75/14.66 % (4094847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.75/14.66 % (4094847)CaDiCaL version: 2.1.3
% 96.75/14.66 % (4094847)Termination reason: Instruction limit
% 96.75/14.66 % (4094847)Termination phase: Saturation
% 96.75/14.66 % (4094847)Time elapsed: 3.046 s
% 96.75/14.66 % (4094847)Peak memory usage: 161 MB
% 96.75/14.66 % (4094847)Instructions burned: 5204 (million)
% 96.75/14.66 % (4094871)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=567673849:i=667:av=off:fsr=off_2958 on theBenchmark for (2958ds/667Mi)
% 96.75/14.66 % (4094871)Instruction limit reached!
% 96.75/14.66 % (4094871)------------------------------
% 96.75/14.66 % (4094871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.75/14.66 % (4094871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.75/14.66 % (4094871)CaDiCaL version: 2.1.3
% 96.75/14.66 % (4094871)Termination reason: Instruction limit
% 96.75/14.66 % (4094871)Termination phase: Saturation
% 96.75/14.66 % (4094871)Time elapsed: 0.314 s
% 96.75/14.66 % (4094871)Peak memory usage: 97 MB
% 96.75/14.66 % (4094871)Instructions burned: 668 (million)
% 96.75/14.66 % (4094873)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3323513269:s2a=on:i=185:s2at=1.8:fdi=4_2953 on theBenchmark for (2953ds/185Mi)
% 96.75/14.66 % (4094873)Instruction limit reached!
% 96.75/14.66 % (4094873)------------------------------
% 96.75/14.66 % (4094873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.75/14.66 % (4094873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.75/14.66 % (4094873)CaDiCaL version: 2.1.3
% 96.75/14.66 % (4094873)Termination reason: Instruction limit
% 96.75/14.66 % (4094873)Termination phase: Property scanning
% 96.75/14.66 % (4094873)Time elapsed: 0.076 s
% 96.75/14.66 % (4094873)Peak memory usage: 88 MB
% 96.75/14.66 % (4094873)Instructions burned: 185 (million)
% 96.75/14.66 % (4094875)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=695800093:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2951 on theBenchmark for (2951ds/193Mi)
% 96.75/14.66 % (4094875)Instruction limit reached!
% 96.75/14.66 % (4094875)------------------------------
% 96.75/14.66 % (4094875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.75/14.66 % (4094875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.75/14.66 % (4094875)CaDiCaL version: 2.1.3
% 96.75/14.66 % (4094875)Termination reason: Instruction limit
% 96.75/14.66 % (4094875)Termination phase: Saturation
% 96.75/14.66 % (4094875)Time elapsed: 0.093 s
% 96.75/14.66 % (4094875)Peak memory usage: 91 MB
% 96.75/14.66 % (4094875)Instructions burned: 194 (million)
% 96.75/14.66 % (4094877)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1704717149:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2947 on theBenchmark for (2947ds/4850Mi)
% 96.75/14.66 % (4094855)Instruction limit reached!
% 96.75/14.66 % (4094855)------------------------------
% 96.75/14.66 % (4094855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.75/14.66 % (4094855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.75/14.66 % (4094855)CaDiCaL version: 2.1.3
% 96.75/14.66 % (4094855)Termination reason: Instruction limit
% 96.75/14.66 % (4094855)Termination phase: Saturation
% 96.75/14.66 % (4094855)Time elapsed: 4.030 s
% 96.75/14.66 % (4094855)Peak memory usage: 225 MB
% 96.75/14.66 % (4094855)Instructions burned: 13196 (million)
% 96.75/14.66 % (4094879)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1281537301:i=12111:sd=1:ss=included_2943 on theBenchmark for (2943ds/12111Mi)
% 96.75/14.66 % (4094864)Instruction limit reached!
% 96.75/14.66 % (4094864)------------------------------
% 125.17/18.62 % (4094864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.17/18.62 % (4094864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.17/18.62 % (4094864)CaDiCaL version: 2.1.3
% 125.17/18.62 % (4094864)Termination reason: Instruction limit
% 125.17/18.62 % (4094864)Termination phase: Saturation
% 125.17/18.62 % (4094864)Time elapsed: 3.685 s
% 125.17/18.62 % (4094864)Peak memory usage: 183 MB
% 125.17/18.62 % (4094864)Instructions burned: 6060 (million)
% 125.17/18.62 % (4094881)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=985586206:i=319:kws=precedence:fsr=off_2939 on theBenchmark for (2939ds/319Mi)
% 125.17/18.62 % (4094881)Instruction limit reached!
% 125.17/18.62 % (4094881)------------------------------
% 125.17/18.62 % (4094881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.17/18.62 % (4094881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.17/18.62 % (4094881)CaDiCaL version: 2.1.3
% 125.17/18.62 % (4094881)Termination reason: Instruction limit
% 125.17/18.62 % (4094881)Termination phase: Saturation
% 125.17/18.62 % (4094881)Time elapsed: 0.142 s
% 125.17/18.62 % (4094881)Peak memory usage: 93 MB
% 125.17/18.62 % (4094881)Instructions burned: 319 (million)
% 125.17/18.62 % (4094883)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1193171105:i=2064:ep=RST_2936 on theBenchmark for (2936ds/2064Mi)
% 125.17/18.62 % (4094883)Instruction limit reached!
% 125.17/18.62 % (4094883)------------------------------
% 125.17/18.62 % (4094883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.17/18.62 % (4094883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.17/18.62 % (4094883)CaDiCaL version: 2.1.3
% 125.17/18.62 % (4094883)Termination reason: Instruction limit
% 125.17/18.62 % (4094883)Termination phase: Saturation
% 125.17/18.62 % (4094883)Time elapsed: 1.117 s
% 125.17/18.62 % (4094883)Peak memory usage: 104 MB
% 125.17/18.62 % (4094883)Instructions burned: 2064 (million)
% 125.17/18.62 % (4094885)dis-1011_128_sil=32000:random_seed=1073574828:i=3706:ep=RST:av=off_2923 on theBenchmark for (2923ds/3706Mi)
% 125.17/18.62 % (4094877)Instruction limit reached!
% 125.17/18.62 % (4094877)------------------------------
% 125.17/18.62 % (4094877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.17/18.62 % (4094877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.17/18.62 % (4094877)CaDiCaL version: 2.1.3
% 125.17/18.62 % (4094877)Termination reason: Instruction limit
% 125.17/18.62 % (4094877)Termination phase: Saturation
% 125.17/18.62 % (4094877)Time elapsed: 2.760 s
% 125.17/18.62 % (4094877)Peak memory usage: 119 MB
% 125.17/18.62 % (4094877)Instructions burned: 4850 (million)
% 125.17/18.62 % (4094887)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=491272227:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2918 on theBenchmark for (2918ds/757Mi)
% 125.17/18.62 % (4094887)Instruction limit reached!
% 125.17/18.62 % (4094887)------------------------------
% 125.17/18.62 % (4094887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.17/18.62 % (4094887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.17/18.62 % (4094887)CaDiCaL version: 2.1.3
% 125.17/18.62 % (4094887)Termination reason: Instruction limit
% 125.17/18.62 % (4094887)Termination phase: Saturation
% 125.17/18.62 % (4094887)Time elapsed: 0.380 s
% 125.17/18.62 % (4094887)Peak memory usage: 92 MB
% 125.17/18.62 % (4094887)Instructions burned: 758 (million)
% 125.17/18.62 % (4094889)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1516022985:i=13913:ss=axioms:sgt=8_2913 on theBenchmark for (2913ds/13913Mi)
% 125.17/18.62 % (4094885)Instruction limit reached!
% 125.17/18.62 % (4094885)------------------------------
% 125.17/18.62 % (4094885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.17/18.62 % (4094885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.17/18.62 % (4094885)CaDiCaL version: 2.1.3
% 125.17/18.62 % (4094885)Termination reason: Instruction limit
% 125.17/18.62 % (4094885)Termination phase: Saturation
% 125.17/18.62 % (4094885)Time elapsed: 1.785 s
% 125.17/18.62 % (4094885)Peak memory usage: 100 MB
% 125.17/18.62 % (4094885)Instructions burned: 3707 (million)
% 125.17/18.62 % (4094891)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3641229667:i=9925:aac=none_2904 on theBenchmark for (2904ds/9925Mi)
% 125.17/18.62 % (4094879)Instruction limit reached!
% 125.17/18.62 % (4094879)------------------------------
% 71.32/19.22 % (4094879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.22 % (4094879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.22 % (4094879)CaDiCaL version: 2.1.3
% 71.32/19.22 % (4094879)Termination reason: Instruction limit
% 71.32/19.22 % (4094879)Termination phase: Saturation
% 71.32/19.22 % (4094879)Time elapsed: 3.949 s
% 71.32/19.22 % (4094879)Peak memory usage: 217 MB
% 71.32/19.22 % (4094879)Instructions burned: 12114 (million)
% 71.32/19.22 % (4094893)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3555440668:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2902 on theBenchmark for (2902ds/2479Mi)
% 71.32/19.22 % (4094893)Instruction limit reached!
% 71.32/19.22 % (4094893)------------------------------
% 71.32/19.22 % (4094893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.22 % (4094893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.22 % (4094893)CaDiCaL version: 2.1.3
% 71.32/19.22 % (4094893)Termination reason: Instruction limit
% 71.32/19.22 % (4094893)Termination phase: Saturation
% 71.32/19.22 % (4094893)Time elapsed: 0.646 s
% 71.32/19.22 % (4094893)Peak memory usage: 98 MB
% 71.32/19.22 % (4094893)Instructions burned: 2480 (million)
% 71.32/19.22 % (4094895)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2846324897:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2895 on theBenchmark for (2895ds/440Mi)
% 71.32/19.22 % (4094895)Instruction limit reached!
% 71.32/19.22 % (4094895)------------------------------
% 71.32/19.22 % (4094895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.22 % (4094895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.22 % (4094895)CaDiCaL version: 2.1.3
% 71.32/19.22 % (4094895)Termination reason: Instruction limit
% 71.32/19.22 % (4094895)Termination phase: Saturation
% 71.32/19.22 % (4094895)Time elapsed: 0.096 s
% 71.32/19.22 % (4094895)Peak memory usage: 91 MB
% 71.32/19.22 % (4094895)Instructions burned: 441 (million)
% 71.32/19.22 % (4094897)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=647001916:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2893 on theBenchmark for (2893ds/11145Mi)
% 71.32/19.22 % (4094869)Instruction limit reached!
% 71.32/19.22 % (4094869)------------------------------
% 71.32/19.22 % (4094869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.22 % (4094869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.22 % (4094869)CaDiCaL version: 2.1.3
% 71.32/19.22 % (4094869)Termination reason: Instruction limit
% 71.32/19.22 % (4094869)Termination phase: Saturation
% 71.32/19.22 % (4094869)Time elapsed: 8.690 s
% 71.32/19.22 % (4094869)Peak memory usage: 238 MB
% 71.32/19.22 % (4094869)Instructions burned: 14155 (million)
% 71.32/19.22 % (4094899)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=456961437:cts=off:i=3034:av=off:er=known:fsd=on_2884 on theBenchmark for (2884ds/3034Mi)
% 71.32/19.22 % (4094899)Instruction limit reached!
% 71.32/19.22 % (4094899)------------------------------
% 71.32/19.22 % (4094899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.22 % (4094899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.22 % (4094899)CaDiCaL version: 2.1.3
% 71.32/19.22 % (4094899)Termination reason: Instruction limit
% 71.32/19.22 % (4094899)Termination phase: Saturation
% 71.32/19.22 % (4094899)Time elapsed: 1.565 s
% 71.32/19.22 % (4094899)Peak memory usage: 160 MB
% 71.32/19.22 % (4094899)Instructions burned: 3037 (million)
% 71.32/19.22 % (4094901)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3892467311:st=2:s2a=on:i=524:s2at=2:ss=axioms_2867 on theBenchmark for (2867ds/524Mi)
% 71.32/19.22 % (4094901)Instruction limit reached!
% 71.32/19.22 % (4094901)------------------------------
% 71.32/19.22 % (4094901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.22 % (4094901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.22 % (4094901)CaDiCaL version: 2.1.3
% 71.32/19.22 % (4094901)Termination reason: Instruction limit
% 71.32/19.22 % (4094901)Termination phase: Saturation
% 71.32/19.22 % (4094901)Time elapsed: 0.266 s
% 71.32/19.22 % (4094901)Peak memory usage: 93 MB
% 71.32/19.22 % (4094901)Instructions burned: 524 (million)
% 71.32/19.22 % (4094903)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1981068589:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2863 on theBenchmark for (2863ds/1016Mi)
% 71.32/19.22 % (4094897)Instruction limit reached!
% 71.32/19.22 % (4094897)------------------------------
% 71.32/19.22 % (4094897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.22 % (4094897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.22 % (4094897)CaDiCaL version: 2.1.3
% 71.32/19.22 % (4094897)Termination reason: Instruction limit
% 71.32/19.22 % (4094897)Termination phase: Saturation
% 71.32/19.22 % (4094897)Time elapsed: 3.614 s
% 71.32/19.22 % (4094897)Peak memory usage: 206 MB
% 71.32/19.22 % (4094897)Instructions burned: 11147 (million)
% 71.32/19.22 % (4094903)Instruction limit reached!
% 71.32/19.22 % (4094903)------------------------------
% 71.32/19.22 % (4094903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.22 % (4094903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.22 % (4094903)CaDiCaL version: 2.1.3
% 71.32/19.22 % (4094903)Termination reason: Instruction limit
% 71.32/19.22 % (4094903)Termination phase: Saturation
% 71.32/19.22 % (4094903)Time elapsed: 0.561 s
% 71.32/19.22 % (4094903)Peak memory usage: 95 MB
% 71.32/19.22 % (4094903)Instructions burned: 1018 (million)
% 71.32/19.22 % (4094905)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1882428507:i=14123:bd=preordered:ins=4_2856 on theBenchmark for (2856ds/14123Mi)
% 71.32/19.22 % (4094906)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3686459867:i=5781:kws=precedence:bd=all:rawr=on_2856 on theBenchmark for (2856ds/5781Mi)
% 71.32/19.22 % (4094891)Instruction limit reached!
% 71.32/19.22 % (4094891)------------------------------
% 71.32/19.22 % (4094891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.22 % (4094891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.22 % (4094891)CaDiCaL version: 2.1.3
% 71.32/19.22 % (4094891)Termination reason: Instruction limit
% 71.32/19.22 % (4094891)Termination phase: Saturation
% 71.32/19.22 % (4094891)Time elapsed: 5.267 s
% 71.32/19.22 % (4094891)Peak memory usage: 200 MB
% 71.32/19.22 % (4094891)Instructions burned: 9926 (million)
% 71.32/19.22 % (4094909)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=802433402:i=2448:gtgl=5:bd=preordered:gtg=all_2850 on theBenchmark for (2850ds/2448Mi)
% 71.32/19.22 % (4094909)Instruction limit reached!
% 71.32/19.22 % (4094909)------------------------------
% 71.32/19.22 % (4094909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.22 % (4094909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.22 % (4094909)CaDiCaL version: 2.1.3
% 71.32/19.22 % (4094909)Termination reason: Instruction limit
% 71.32/19.22 % (4094909)Termination phase: Saturation
% 71.32/19.22 % (4094909)Time elapsed: 1.357 s
% 71.32/19.22 % (4094909)Peak memory usage: 150 MB
% 71.32/19.22 % (4094909)Instructions burned: 2448 (million)
% 71.32/19.22 % (4094889)Instruction limit reached!
% 71.32/19.22 % (4094889)------------------------------
% 71.32/19.22 % (4094889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.22 % (4094889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.22 % (4094889)CaDiCaL version: 2.1.3
% 71.32/19.22 % (4094889)Termination reason: Instruction limit
% 71.32/19.22 % (4094889)Termination phase: Saturation
% 71.32/19.22 % (4094889)Time elapsed: 7.771 s
% 71.32/19.22 % (4094889)Peak memory usage: 222 MB
% 71.32/19.22 % (4094889)Instructions burned: 13913 (million)
% 71.32/19.22 % (4094911)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2438837271:i=3223:kws=precedence:fgj=on:av=off_2835 on theBenchmark for (2835ds/3223Mi)
% 71.32/19.22 % (4094912)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1116269290:st=5.6:i=2033:sd=3:ss=axioms_2834 on theBenchmark for (2834ds/2033Mi)
% 71.32/19.22 % (4094906)Instruction limit reached!
% 71.32/19.22 % (4094906)------------------------------
% 71.32/19.22 % (4094906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.22 % (4094906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.22 % (4094906)CaDiCaL version: 2.1.3
% 71.32/19.22 % (4094906)Termination reason: Instruction limit
% 71.32/19.22 % (4094906)Termination phase: Saturation
% 71.32/19.23 % (4094906)Time elapsed: 3.259 s
% 71.32/19.23 % (4094906)Peak memory usage: 107 MB
% 71.32/19.23 % (4094906)Instructions burned: 5782 (million)
% 71.32/19.23 % (4094912)Instruction limit reached!
% 71.32/19.23 % (4094912)------------------------------
% 71.32/19.23 % (4094912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.32/19.23 % (4094912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.32/19.23 % (4094912)CaDiCaL version: 2.1.3
% 71.32/19.23 % (4094912)Termination reason: Instruction limit
% 71.32/19.23 % (4094912)Termination phase: Saturation
% 71.32/19.23 % (4094912)Time elapsed: 1.234 s
% 71.32/19.23 % (4094912)Peak memory usage: 163 MB
% 71.32/19.23 % (4094912)Instructions burned: 2034 (million)
% 71.32/19.23 % (4094915)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=4179434029:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2822 on theBenchmark for (2822ds/2055Mi)
% 71.32/19.23 % (4094917)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=1643204119:i=21611:sd=3:ss=axioms_2821 on theBenchmark for (2821ds/21611Mi)
% 71.32/19.23 % (4094905)First to succeed.
% 71.32/19.23 % (4094905)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4094807"
% 71.32/19.23 % (4094905)Refutation found. Thanks to Tanya!
% 71.32/19.23 % SZS status Theorem for theBenchmark
% 71.32/19.23 % SZS output start Proof for theBenchmark
% See solution above
% 129.65/19.42 % (4094905)------------------------------
% 129.65/19.42 % (4094905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.65/19.42 % (4094905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.65/19.42 % (4094905)CaDiCaL version: 2.1.3
% 129.65/19.42 % (4094905)Termination reason: Refutation
% 129.65/19.42 % (4094905)Time elapsed: 3.715 s
% 129.65/19.42 % (4094905)Peak memory usage: 198 MB
% 129.65/19.42 % (4094905)Instructions burned: 11303 (million)
% 129.65/19.42 % (4094905)------------------------------
% 129.65/19.42 % (4094905)------------------------------
% 129.65/19.42 % (4094807)Success in time 18.35 s
% 129.65/19.42 % Vampire exiting
%------------------------------------------------------------------------------