%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT319+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:53 AM UTC 2026
% Result : Theorem 5.40s 1.74s
% Output : Refutation 6.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 26
% Syntax : Number of formulae : 264 ( 21 unt; 17 def)
% Number of atoms : 1175 ( 0 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 1507 ( 596 ~; 670 |; 198 &)
% ( 28 <=>; 13 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 28 ( 27 usr; 16 prp; 0-1 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 62 ( 0 sgn 58 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2324,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v13_lattices(X0)
& v14_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v15_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc3_lattices) ).
fof(f2328,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc5_lattices) ).
fof(f2329,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v17_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc6_lattices) ).
fof(f2351,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( v17_lattices(X0)
<=> ( v15_lattices(X0)
& v16_lattices(X0)
& v11_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d20_lattices) ).
fof(f2564,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f2646,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_lattice2) ).
fof(f2669,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f2986,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t53_filter_2) ).
fof(f2987,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t54_filter_2) ).
fof(f2988,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f2987]) ).
fof(f3032,plain,
? [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<~> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2988]) ).
fof(f3033,plain,
? [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<~> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f3032]) ).
fof(f3064,plain,
! [X0] :
( ( v17_lattices(X0)
<=> ( v15_lattices(X0)
& v16_lattices(X0)
& v11_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2351]) ).
fof(f3065,plain,
! [X0] :
( ( v17_lattices(X0)
<=> ( v15_lattices(X0)
& v16_lattices(X0)
& v11_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3064]) ).
fof(f3066,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2329]) ).
fof(f3067,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3066]) ).
fof(f3068,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2328]) ).
fof(f3069,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3068]) ).
fof(f3070,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2986]) ).
fof(f3071,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3070]) ).
fof(f3076,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2669]) ).
fof(f3081,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2646]) ).
fof(f3082,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3081]) ).
fof(f3102,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2564]) ).
fof(f3103,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3102]) ).
fof(f3392,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v15_lattices(X0) )
| v3_struct_0(X0)
| ~ v13_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2324]) ).
fof(f3393,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v15_lattices(X0) )
| v3_struct_0(X0)
| ~ v13_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3392]) ).
fof(f3596,definition,
! [X0] :
( sP0(X0)
<=> ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f3597,definition,
! [X0] :
( ( sP0(X0)
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| ~ sP1(X0) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f3598,plain,
! [X0] :
( sP1(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f3071,f3597,f3596]) ).
fof(f3614,plain,
? [X0] :
( ( v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(nnf_transformation,[],[f3033]) ).
fof(f3615,plain,
? [X0] :
( ( v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f3614]) ).
fof(f3616,plain,
( ( v3_struct_0(k1_lattice2(sK10))
| ~ v10_lattices(k1_lattice2(sK10))
| ~ v17_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| v3_struct_0(sK10)
| ~ v10_lattices(sK10)
| ~ v17_lattices(sK10)
| ~ l3_lattices(sK10) )
& ( ( ~ v3_struct_0(k1_lattice2(sK10))
& v10_lattices(k1_lattice2(sK10))
& v17_lattices(k1_lattice2(sK10))
& l3_lattices(k1_lattice2(sK10)) )
| ( ~ v3_struct_0(sK10)
& v10_lattices(sK10)
& v17_lattices(sK10)
& l3_lattices(sK10) ) )
& ~ v3_struct_0(sK10)
& v10_lattices(sK10)
& l3_lattices(sK10) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X0,sK10)],[f3615]) ).
fof(f3620,plain,
! [X0] :
( ( ( v17_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ v11_lattices(X0) )
& ( ( v15_lattices(X0)
& v16_lattices(X0)
& v11_lattices(X0) )
| ~ v17_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f3065]) ).
fof(f3621,plain,
! [X0] :
( ( ( v17_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ v11_lattices(X0) )
& ( ( v15_lattices(X0)
& v16_lattices(X0)
& v11_lattices(X0) )
| ~ v17_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3620]) ).
fof(f3623,plain,
! [X0] :
( ( ( sP0(X0)
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ sP0(X0) ) )
| ~ sP1(X0) ),
inference(nnf_transformation,[],[f3597]) ).
fof(f3624,plain,
! [X0] :
( ( ( sP0(X0)
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ sP0(X0) ) )
| ~ sP1(X0) ),
inference(flattening,[],[f3623]) ).
fof(f3625,plain,
! [X0] :
( ( sP0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) )
& ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
| ~ sP0(X0) ) ),
inference(nnf_transformation,[],[f3596]) ).
fof(f3626,plain,
! [X0] :
( ( sP0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) )
& ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
| ~ sP0(X0) ) ),
inference(flattening,[],[f3625]) ).
fof(f3627,plain,
! [X0] :
( ( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v11_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f3082]) ).
fof(f3628,plain,
! [X0] :
( ( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v11_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3627]) ).
fof(f3807,plain,
l3_lattices(sK10),
inference(cnf_transformation,[],[f3616]) ).
fof(f3808,plain,
v10_lattices(sK10),
inference(cnf_transformation,[],[f3616]) ).
fof(f3809,plain,
~ v3_struct_0(sK10),
inference(cnf_transformation,[],[f3616]) ).
fof(f3815,plain,
( v17_lattices(k1_lattice2(sK10))
| v17_lattices(sK10) ),
inference(cnf_transformation,[],[f3616]) ).
fof(f3819,plain,
( v10_lattices(k1_lattice2(sK10))
| v17_lattices(sK10) ),
inference(cnf_transformation,[],[f3616]) ).
fof(f3826,plain,
( v3_struct_0(k1_lattice2(sK10))
| ~ v10_lattices(k1_lattice2(sK10))
| ~ v17_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| v3_struct_0(sK10)
| ~ v10_lattices(sK10)
| ~ v17_lattices(sK10)
| ~ l3_lattices(sK10) ),
inference(cnf_transformation,[],[f3616]) ).
fof(f3849,plain,
! [X0] :
( ~ v17_lattices(X0)
| v11_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3621]) ).
fof(f3850,plain,
! [X0] :
( ~ v17_lattices(X0)
| v16_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3621]) ).
fof(f3851,plain,
! [X0] :
( ~ v17_lattices(X0)
| v15_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3621]) ).
fof(f3869,plain,
! [X0] :
( v17_lattices(X0)
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3067]) ).
fof(f3873,plain,
! [X0] :
( ~ v17_lattices(X0)
| v3_struct_0(X0)
| v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3069]) ).
fof(f3874,plain,
! [X0] :
( ~ v17_lattices(X0)
| v3_struct_0(X0)
| v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3069]) ).
fof(f3875,plain,
! [X0] :
( ~ v17_lattices(X0)
| v3_struct_0(X0)
| v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3069]) ).
fof(f3878,plain,
! [X0] :
( v16_lattices(k1_lattice2(X0))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f3624]) ).
fof(f3879,plain,
! [X0] :
( v15_lattices(k1_lattice2(X0))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f3624]) ).
fof(f3882,plain,
! [X0] :
( ~ v16_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| sP0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f3624]) ).
fof(f3884,plain,
! [X0] :
( ~ sP0(X0)
| v16_lattices(X0) ),
inference(cnf_transformation,[],[f3626]) ).
fof(f3885,plain,
! [X0] :
( ~ sP0(X0)
| v15_lattices(X0) ),
inference(cnf_transformation,[],[f3626]) ).
fof(f3888,plain,
! [X0] :
( sP0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3626]) ).
fof(f3889,plain,
! [X0] :
( sP1(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3598]) ).
fof(f3892,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3076]) ).
fof(f3897,plain,
! [X0] :
( v11_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3628]) ).
fof(f3898,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3628]) ).
fof(f3901,plain,
! [X0] :
( ~ v11_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v11_lattices(X0)
| ~ l3_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3628]) ).
fof(f3930,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3103]) ).
fof(f4335,plain,
! [X0] :
( v15_lattices(X0)
| v3_struct_0(X0)
| ~ v13_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3393]) ).
fof(f4734,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f3898]) ).
fof(f4735,plain,
! [X0] :
( v11_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f3897]) ).
fof(f4769,definition,
( spl144_1
<=> v17_lattices(sK10) ),
introduced(definition,[new_symbols(definition,[spl144_1])],[avatar_definition]) ).
fof(f4770,plain,
( ~ v17_lattices(sK10)
| spl144_1 ),
inference(avatar_component_clause,[],[f4769]) ).
fof(f4771,plain,
( v17_lattices(sK10)
| ~ spl144_1 ),
inference(avatar_component_clause,[],[f4769]) ).
fof(f4773,definition,
( spl144_2
<=> l3_lattices(k1_lattice2(sK10)) ),
introduced(definition,[new_symbols(definition,[spl144_2])],[avatar_definition]) ).
fof(f4774,plain,
( ~ l3_lattices(k1_lattice2(sK10))
| spl144_2 ),
inference(avatar_component_clause,[],[f4773]) ).
fof(f4775,plain,
( l3_lattices(k1_lattice2(sK10))
| ~ spl144_2 ),
inference(avatar_component_clause,[],[f4773]) ).
fof(f4778,definition,
( spl144_3
<=> v17_lattices(k1_lattice2(sK10)) ),
introduced(definition,[new_symbols(definition,[spl144_3])],[avatar_definition]) ).
fof(f4779,plain,
( ~ v17_lattices(k1_lattice2(sK10))
| spl144_3 ),
inference(avatar_component_clause,[],[f4778]) ).
fof(f4780,plain,
( v17_lattices(k1_lattice2(sK10))
| ~ spl144_3 ),
inference(avatar_component_clause,[],[f4778]) ).
fof(f4781,plain,
( spl144_1
| spl144_3 ),
inference(avatar_split_clause,[],[f3815,f4778,f4769]) ).
fof(f4783,definition,
( spl144_4
<=> v10_lattices(k1_lattice2(sK10)) ),
introduced(definition,[new_symbols(definition,[spl144_4])],[avatar_definition]) ).
fof(f4784,plain,
( ~ v10_lattices(k1_lattice2(sK10))
| spl144_4 ),
inference(avatar_component_clause,[],[f4783]) ).
fof(f4785,plain,
( v10_lattices(k1_lattice2(sK10))
| ~ spl144_4 ),
inference(avatar_component_clause,[],[f4783]) ).
fof(f4786,plain,
( spl144_1
| spl144_4 ),
inference(avatar_split_clause,[],[f3819,f4783,f4769]) ).
fof(f4788,definition,
( spl144_5
<=> v3_struct_0(k1_lattice2(sK10)) ),
introduced(definition,[new_symbols(definition,[spl144_5])],[avatar_definition]) ).
fof(f4789,plain,
( v3_struct_0(k1_lattice2(sK10))
| ~ spl144_5 ),
inference(avatar_component_clause,[],[f4788]) ).
fof(f4790,plain,
( ~ v3_struct_0(k1_lattice2(sK10))
| spl144_5 ),
inference(avatar_component_clause,[],[f4788]) ).
fof(f4792,plain,
( v3_struct_0(k1_lattice2(sK10))
| ~ v10_lattices(k1_lattice2(sK10))
| ~ v17_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| ~ v10_lattices(sK10)
| ~ v17_lattices(sK10)
| ~ l3_lattices(sK10) ),
inference(forward_subsumption_resolution,[],[f3826,f3809]) ).
fof(f4793,plain,
( v3_struct_0(k1_lattice2(sK10))
| ~ v10_lattices(k1_lattice2(sK10))
| ~ v17_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| ~ v17_lattices(sK10)
| ~ l3_lattices(sK10) ),
inference(forward_subsumption_resolution,[],[f4792,f3808]) ).
fof(f4794,plain,
( v3_struct_0(k1_lattice2(sK10))
| ~ v10_lattices(k1_lattice2(sK10))
| ~ v17_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| ~ v17_lattices(sK10) ),
inference(forward_subsumption_resolution,[],[f4793,f3807]) ).
fof(f4795,plain,
( ~ spl144_1
| ~ spl144_2
| ~ spl144_3
| ~ spl144_4
| spl144_5 ),
inference(avatar_split_clause,[],[f4794,f4788,f4783,f4778,f4773,f4769]) ).
fof(f4799,plain,
( v3_struct_0(sK10)
| ~ v11_lattices(sK10)
| ~ v15_lattices(sK10)
| ~ v16_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_1 ),
inference(resolution,[],[f4770,f3869]) ).
fof(f4802,plain,
( ~ v11_lattices(sK10)
| ~ v15_lattices(sK10)
| ~ v16_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_1 ),
inference(forward_subsumption_resolution,[],[f4799,f3809]) ).
fof(f4804,plain,
( ~ v11_lattices(sK10)
| ~ v15_lattices(sK10)
| ~ v16_lattices(sK10)
| spl144_1 ),
inference(forward_subsumption_resolution,[],[f4802,f3807]) ).
fof(f4806,definition,
( spl144_6
<=> v11_lattices(sK10) ),
introduced(definition,[new_symbols(definition,[spl144_6])],[avatar_definition]) ).
fof(f4807,plain,
( v11_lattices(sK10)
| ~ spl144_6 ),
inference(avatar_component_clause,[],[f4806]) ).
fof(f4808,plain,
( ~ v11_lattices(sK10)
| spl144_6 ),
inference(avatar_component_clause,[],[f4806]) ).
fof(f4810,definition,
( spl144_7
<=> v16_lattices(sK10) ),
introduced(definition,[new_symbols(definition,[spl144_7])],[avatar_definition]) ).
fof(f4811,plain,
( v16_lattices(sK10)
| ~ spl144_7 ),
inference(avatar_component_clause,[],[f4810]) ).
fof(f4812,plain,
( ~ v16_lattices(sK10)
| spl144_7 ),
inference(avatar_component_clause,[],[f4810]) ).
fof(f4814,definition,
( spl144_8
<=> v15_lattices(sK10) ),
introduced(definition,[new_symbols(definition,[spl144_8])],[avatar_definition]) ).
fof(f4815,plain,
( v15_lattices(sK10)
| ~ spl144_8 ),
inference(avatar_component_clause,[],[f4814]) ).
fof(f4816,plain,
( ~ v15_lattices(sK10)
| spl144_8 ),
inference(avatar_component_clause,[],[f4814]) ).
fof(f4818,plain,
( ~ spl144_7
| ~ spl144_8
| ~ spl144_6
| spl144_1 ),
inference(avatar_split_clause,[],[f4804,f4769,f4806,f4814,f4810]) ).
fof(f4824,plain,
( v3_struct_0(k1_lattice2(sK10))
| v14_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| ~ spl144_3 ),
inference(resolution,[],[f4780,f3873]) ).
fof(f4825,plain,
( v3_struct_0(k1_lattice2(sK10))
| v13_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| ~ spl144_3 ),
inference(resolution,[],[f4780,f3874]) ).
fof(f4826,plain,
( v3_struct_0(k1_lattice2(sK10))
| v11_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| ~ spl144_3 ),
inference(resolution,[],[f4780,f3875]) ).
fof(f4827,plain,
( v11_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| ~ spl144_3
| spl144_5 ),
inference(forward_subsumption_resolution,[],[f4826,f4790]) ).
fof(f4828,plain,
( v13_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| ~ spl144_3
| spl144_5 ),
inference(forward_subsumption_resolution,[],[f4825,f4790]) ).
fof(f4829,plain,
( v14_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| ~ spl144_3
| spl144_5 ),
inference(forward_subsumption_resolution,[],[f4824,f4790]) ).
fof(f4835,plain,
( v11_lattices(k1_lattice2(sK10))
| ~ spl144_2
| ~ spl144_3
| spl144_5 ),
inference(forward_subsumption_resolution,[],[f4827,f4775]) ).
fof(f4836,plain,
( v13_lattices(k1_lattice2(sK10))
| ~ spl144_2
| ~ spl144_3
| spl144_5 ),
inference(forward_subsumption_resolution,[],[f4828,f4775]) ).
fof(f4837,plain,
( v14_lattices(k1_lattice2(sK10))
| ~ spl144_2
| ~ spl144_3
| spl144_5 ),
inference(forward_subsumption_resolution,[],[f4829,f4775]) ).
fof(f4860,plain,
( v3_struct_0(k1_lattice2(sK10))
| ~ v10_lattices(k1_lattice2(sK10))
| v11_lattices(sK10)
| ~ l3_lattices(k1_lattice2(sK10))
| v3_struct_0(sK10)
| ~ v10_lattices(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_2
| ~ spl144_3
| spl144_5 ),
inference(resolution,[],[f4835,f3901]) ).
fof(f4861,plain,
( ~ v10_lattices(k1_lattice2(sK10))
| v11_lattices(sK10)
| ~ l3_lattices(k1_lattice2(sK10))
| v3_struct_0(sK10)
| ~ v10_lattices(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_2
| ~ spl144_3
| spl144_5 ),
inference(forward_subsumption_resolution,[],[f4860,f4790]) ).
fof(f4862,plain,
( v11_lattices(sK10)
| ~ l3_lattices(k1_lattice2(sK10))
| v3_struct_0(sK10)
| ~ v10_lattices(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_2
| ~ spl144_3
| ~ spl144_4
| spl144_5 ),
inference(forward_subsumption_resolution,[],[f4861,f4785]) ).
fof(f4863,plain,
( ~ l3_lattices(k1_lattice2(sK10))
| v3_struct_0(sK10)
| ~ v10_lattices(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_2
| ~ spl144_3
| ~ spl144_4
| spl144_5
| spl144_6 ),
inference(forward_subsumption_resolution,[],[f4862,f4808]) ).
fof(f4864,plain,
( v3_struct_0(sK10)
| ~ v10_lattices(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_2
| ~ spl144_3
| ~ spl144_4
| spl144_5
| spl144_6 ),
inference(forward_subsumption_resolution,[],[f4863,f4775]) ).
fof(f4865,plain,
( ~ v10_lattices(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_2
| ~ spl144_3
| ~ spl144_4
| spl144_5
| spl144_6 ),
inference(forward_subsumption_resolution,[],[f4864,f3809]) ).
fof(f4866,plain,
( ~ l3_lattices(sK10)
| ~ spl144_2
| ~ spl144_3
| ~ spl144_4
| spl144_5
| spl144_6 ),
inference(forward_subsumption_resolution,[],[f4865,f3808]) ).
fof(f4867,plain,
( $false
| ~ spl144_2
| ~ spl144_3
| ~ spl144_4
| spl144_5
| spl144_6 ),
inference(forward_subsumption_resolution,[],[f4866,f3807]) ).
fof(f4868,plain,
( ~ spl144_2
| ~ spl144_3
| ~ spl144_4
| spl144_5
| spl144_6 ),
inference(avatar_contradiction_clause,[],[f4867]) ).
fof(f4869,plain,
( v11_lattices(sK10)
| v3_struct_0(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_1 ),
inference(resolution,[],[f4771,f3849]) ).
fof(f4870,plain,
( v16_lattices(sK10)
| v3_struct_0(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_1 ),
inference(resolution,[],[f4771,f3850]) ).
fof(f4871,plain,
( v15_lattices(sK10)
| v3_struct_0(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_1 ),
inference(resolution,[],[f4771,f3851]) ).
fof(f4882,plain,
( v3_struct_0(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_1
| spl144_8 ),
inference(forward_subsumption_resolution,[],[f4871,f4816]) ).
fof(f4883,plain,
( v3_struct_0(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_1
| spl144_7 ),
inference(forward_subsumption_resolution,[],[f4870,f4812]) ).
fof(f4884,plain,
( v3_struct_0(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_1
| spl144_6 ),
inference(forward_subsumption_resolution,[],[f4869,f4808]) ).
fof(f4890,plain,
( ~ l3_lattices(sK10)
| ~ spl144_1
| spl144_8 ),
inference(forward_subsumption_resolution,[],[f4882,f3809]) ).
fof(f4891,plain,
( ~ l3_lattices(sK10)
| ~ spl144_1
| spl144_7 ),
inference(forward_subsumption_resolution,[],[f4883,f3809]) ).
fof(f4892,plain,
( ~ l3_lattices(sK10)
| ~ spl144_1
| spl144_6 ),
inference(forward_subsumption_resolution,[],[f4884,f3809]) ).
fof(f4903,plain,
( $false
| ~ spl144_1
| spl144_8 ),
inference(forward_subsumption_resolution,[],[f4890,f3807]) ).
fof(f4904,plain,
( ~ spl144_1
| spl144_8 ),
inference(avatar_contradiction_clause,[],[f4903]) ).
fof(f4905,plain,
( $false
| ~ spl144_1
| spl144_7 ),
inference(forward_subsumption_resolution,[],[f4891,f3807]) ).
fof(f4906,plain,
( ~ spl144_1
| spl144_7 ),
inference(avatar_contradiction_clause,[],[f4905]) ).
fof(f4907,plain,
( $false
| ~ spl144_1
| spl144_6 ),
inference(forward_subsumption_resolution,[],[f4892,f3807]) ).
fof(f4908,plain,
( ~ spl144_1
| spl144_6 ),
inference(avatar_contradiction_clause,[],[f4907]) ).
fof(f4910,plain,
( ~ l3_lattices(sK10)
| spl144_2 ),
inference(resolution,[],[f4774,f3892]) ).
fof(f4913,definition,
( spl144_11
<=> sP1(sK10) ),
introduced(definition,[new_symbols(definition,[spl144_11])],[avatar_definition]) ).
fof(f4914,plain,
( sP1(sK10)
| ~ spl144_11 ),
inference(avatar_component_clause,[],[f4913]) ).
fof(f4915,plain,
( ~ sP1(sK10)
| spl144_11 ),
inference(avatar_component_clause,[],[f4913]) ).
fof(f4917,definition,
( spl144_12
<=> sP0(sK10) ),
introduced(definition,[new_symbols(definition,[spl144_12])],[avatar_definition]) ).
fof(f4918,plain,
( sP0(sK10)
| ~ spl144_12 ),
inference(avatar_component_clause,[],[f4917]) ).
fof(f4919,plain,
( ~ sP0(sK10)
| spl144_12 ),
inference(avatar_component_clause,[],[f4917]) ).
fof(f4921,plain,
( $false
| spl144_2 ),
inference(forward_subsumption_resolution,[],[f4910,f3807]) ).
fof(f4922,plain,
spl144_2,
inference(avatar_contradiction_clause,[],[f4921]) ).
fof(f4928,plain,
( v3_struct_0(k1_lattice2(sK10))
| ~ v11_lattices(k1_lattice2(sK10))
| ~ v15_lattices(k1_lattice2(sK10))
| ~ v16_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| spl144_3 ),
inference(resolution,[],[f4779,f3869]) ).
fof(f4931,plain,
( ~ v11_lattices(k1_lattice2(sK10))
| ~ v15_lattices(k1_lattice2(sK10))
| ~ v16_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| spl144_3
| spl144_5 ),
inference(forward_subsumption_resolution,[],[f4928,f4790]) ).
fof(f4933,plain,
( ~ v11_lattices(k1_lattice2(sK10))
| ~ v15_lattices(k1_lattice2(sK10))
| ~ v16_lattices(k1_lattice2(sK10))
| ~ spl144_2
| spl144_3
| spl144_5 ),
inference(forward_subsumption_resolution,[],[f4931,f4775]) ).
fof(f4935,definition,
( spl144_13
<=> v11_lattices(k1_lattice2(sK10)) ),
introduced(definition,[new_symbols(definition,[spl144_13])],[avatar_definition]) ).
fof(f4937,plain,
( ~ v11_lattices(k1_lattice2(sK10))
| spl144_13 ),
inference(avatar_component_clause,[],[f4935]) ).
fof(f4939,definition,
( spl144_14
<=> v16_lattices(k1_lattice2(sK10)) ),
introduced(definition,[new_symbols(definition,[spl144_14])],[avatar_definition]) ).
fof(f4940,plain,
( v16_lattices(k1_lattice2(sK10))
| ~ spl144_14 ),
inference(avatar_component_clause,[],[f4939]) ).
fof(f4941,plain,
( ~ v16_lattices(k1_lattice2(sK10))
| spl144_14 ),
inference(avatar_component_clause,[],[f4939]) ).
fof(f4943,definition,
( spl144_15
<=> v15_lattices(k1_lattice2(sK10)) ),
introduced(definition,[new_symbols(definition,[spl144_15])],[avatar_definition]) ).
fof(f4944,plain,
( v15_lattices(k1_lattice2(sK10))
| ~ spl144_15 ),
inference(avatar_component_clause,[],[f4943]) ).
fof(f4945,plain,
( ~ v15_lattices(k1_lattice2(sK10))
| spl144_15 ),
inference(avatar_component_clause,[],[f4943]) ).
fof(f4947,plain,
( ~ spl144_14
| ~ spl144_15
| ~ spl144_13
| ~ spl144_2
| spl144_3
| spl144_5 ),
inference(avatar_split_clause,[],[f4933,f4788,f4778,f4773,f4935,f4943,f4939]) ).
fof(f4952,plain,
( v3_struct_0(sK10)
| ~ v10_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_11 ),
inference(resolution,[],[f4915,f3889]) ).
fof(f4953,plain,
( ~ v10_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_11 ),
inference(forward_subsumption_resolution,[],[f4952,f3809]) ).
fof(f4954,plain,
( ~ l3_lattices(sK10)
| spl144_11 ),
inference(forward_subsumption_resolution,[],[f4953,f3808]) ).
fof(f4955,plain,
( $false
| spl144_11 ),
inference(forward_subsumption_resolution,[],[f4954,f3807]) ).
fof(f4956,plain,
spl144_11,
inference(avatar_contradiction_clause,[],[f4955]) ).
fof(f4957,plain,
( v3_struct_0(sK10)
| ~ v10_lattices(sK10)
| ~ v15_lattices(sK10)
| ~ v16_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_12 ),
inference(resolution,[],[f4919,f3888]) ).
fof(f4958,plain,
( ~ v10_lattices(sK10)
| ~ v15_lattices(sK10)
| ~ v16_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_12 ),
inference(forward_subsumption_resolution,[],[f4957,f3809]) ).
fof(f4959,plain,
( ~ v15_lattices(sK10)
| ~ v16_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_12 ),
inference(forward_subsumption_resolution,[],[f4958,f3808]) ).
fof(f4960,plain,
( ~ v16_lattices(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_8
| spl144_12 ),
inference(forward_subsumption_resolution,[],[f4959,f4815]) ).
fof(f4961,plain,
( ~ l3_lattices(sK10)
| ~ spl144_7
| ~ spl144_8
| spl144_12 ),
inference(forward_subsumption_resolution,[],[f4960,f4811]) ).
fof(f4962,plain,
( $false
| ~ spl144_7
| ~ spl144_8
| spl144_12 ),
inference(forward_subsumption_resolution,[],[f4961,f3807]) ).
fof(f4963,plain,
( ~ spl144_7
| ~ spl144_8
| spl144_12 ),
inference(avatar_contradiction_clause,[],[f4962]) ).
fof(f4965,plain,
( v16_lattices(sK10)
| ~ spl144_12 ),
inference(resolution,[],[f4918,f3884]) ).
fof(f4966,plain,
( v15_lattices(sK10)
| ~ spl144_12 ),
inference(resolution,[],[f4918,f3885]) ).
fof(f4969,plain,
( v3_struct_0(sK10)
| ~ v10_lattices(sK10)
| ~ v11_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_13 ),
inference(resolution,[],[f4937,f4735]) ).
fof(f4970,plain,
( ~ v10_lattices(sK10)
| ~ v11_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_13 ),
inference(forward_subsumption_resolution,[],[f4969,f3809]) ).
fof(f4971,plain,
( ~ v11_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_13 ),
inference(forward_subsumption_resolution,[],[f4970,f3808]) ).
fof(f4972,plain,
( ~ l3_lattices(sK10)
| ~ spl144_6
| spl144_13 ),
inference(forward_subsumption_resolution,[],[f4971,f4807]) ).
fof(f4973,plain,
( $false
| ~ spl144_6
| spl144_13 ),
inference(forward_subsumption_resolution,[],[f4972,f3807]) ).
fof(f4974,plain,
( ~ spl144_6
| spl144_13 ),
inference(avatar_contradiction_clause,[],[f4973]) ).
fof(f4976,plain,
( ~ sP0(sK10)
| ~ sP1(sK10)
| spl144_14 ),
inference(resolution,[],[f4941,f3878]) ).
fof(f4977,plain,
( ~ sP1(sK10)
| ~ spl144_12
| spl144_14 ),
inference(forward_subsumption_resolution,[],[f4976,f4918]) ).
fof(f4978,plain,
( $false
| ~ spl144_11
| ~ spl144_12
| spl144_14 ),
inference(forward_subsumption_resolution,[],[f4977,f4914]) ).
fof(f4979,plain,
( ~ spl144_11
| ~ spl144_12
| spl144_14 ),
inference(avatar_contradiction_clause,[],[f4978]) ).
fof(f4980,plain,
( v3_struct_0(k1_lattice2(sK10))
| ~ v10_lattices(k1_lattice2(sK10))
| ~ v15_lattices(k1_lattice2(sK10))
| sP0(sK10)
| ~ l3_lattices(k1_lattice2(sK10))
| ~ sP1(sK10)
| ~ spl144_14 ),
inference(resolution,[],[f4940,f3882]) ).
fof(f4981,plain,
( ~ sP0(sK10)
| ~ sP1(sK10)
| spl144_15 ),
inference(resolution,[],[f4945,f3879]) ).
fof(f4982,plain,
( v3_struct_0(k1_lattice2(sK10))
| ~ v13_lattices(k1_lattice2(sK10))
| ~ v14_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| spl144_15 ),
inference(resolution,[],[f4945,f4335]) ).
fof(f4985,plain,
( ~ v13_lattices(k1_lattice2(sK10))
| ~ v14_lattices(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| spl144_5
| spl144_15 ),
inference(forward_subsumption_resolution,[],[f4982,f4790]) ).
fof(f4986,plain,
( ~ sP1(sK10)
| ~ spl144_12
| spl144_15 ),
inference(forward_subsumption_resolution,[],[f4981,f4918]) ).
fof(f4988,plain,
( ~ v13_lattices(k1_lattice2(sK10))
| ~ v14_lattices(k1_lattice2(sK10))
| ~ spl144_2
| spl144_5
| spl144_15 ),
inference(forward_subsumption_resolution,[],[f4985,f4775]) ).
fof(f4989,plain,
( $false
| ~ spl144_11
| ~ spl144_12
| spl144_15 ),
inference(forward_subsumption_resolution,[],[f4986,f4914]) ).
fof(f4990,plain,
( ~ spl144_11
| ~ spl144_12
| spl144_15 ),
inference(avatar_contradiction_clause,[],[f4989]) ).
fof(f4992,definition,
( spl144_16
<=> v14_lattices(k1_lattice2(sK10)) ),
introduced(definition,[new_symbols(definition,[spl144_16])],[avatar_definition]) ).
fof(f4994,plain,
( ~ v14_lattices(k1_lattice2(sK10))
| spl144_16 ),
inference(avatar_component_clause,[],[f4992]) ).
fof(f4996,definition,
( spl144_17
<=> v13_lattices(k1_lattice2(sK10)) ),
introduced(definition,[new_symbols(definition,[spl144_17])],[avatar_definition]) ).
fof(f4998,plain,
( ~ v13_lattices(k1_lattice2(sK10))
| spl144_17 ),
inference(avatar_component_clause,[],[f4996]) ).
fof(f5000,plain,
( ~ spl144_16
| ~ spl144_17
| ~ spl144_2
| spl144_5
| spl144_15 ),
inference(avatar_split_clause,[],[f4988,f4943,f4788,f4773,f4996,f4992]) ).
fof(f5001,plain,
( v3_struct_0(sK10)
| ~ l3_lattices(sK10)
| ~ spl144_5 ),
inference(resolution,[],[f4789,f3930]) ).
fof(f5007,plain,
( ~ l3_lattices(sK10)
| ~ spl144_5 ),
inference(forward_subsumption_resolution,[],[f5001,f3809]) ).
fof(f5011,plain,
( $false
| ~ spl144_5 ),
inference(forward_subsumption_resolution,[],[f5007,f3807]) ).
fof(f5012,plain,
~ spl144_5,
inference(avatar_contradiction_clause,[],[f5011]) ).
fof(f5016,plain,
( $false
| ~ spl144_2
| ~ spl144_3
| spl144_5
| spl144_16 ),
inference(forward_subsumption_resolution,[],[f4837,f4994]) ).
fof(f5017,plain,
( ~ spl144_2
| ~ spl144_3
| spl144_5
| spl144_16 ),
inference(avatar_contradiction_clause,[],[f5016]) ).
fof(f5018,plain,
( $false
| ~ spl144_2
| ~ spl144_3
| spl144_5
| spl144_17 ),
inference(forward_subsumption_resolution,[],[f4836,f4998]) ).
fof(f5019,plain,
( ~ spl144_2
| ~ spl144_3
| spl144_5
| spl144_17 ),
inference(avatar_contradiction_clause,[],[f5018]) ).
fof(f5021,plain,
( v16_lattices(k1_lattice2(sK10))
| v3_struct_0(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| ~ spl144_3 ),
inference(resolution,[],[f4780,f3850]) ).
fof(f5029,plain,
( v3_struct_0(sK10)
| ~ v10_lattices(sK10)
| ~ v11_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_4 ),
inference(resolution,[],[f4784,f4734]) ).
fof(f5032,plain,
( ~ v10_lattices(sK10)
| ~ v11_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_4 ),
inference(forward_subsumption_resolution,[],[f5029,f3809]) ).
fof(f5035,plain,
( ~ v11_lattices(sK10)
| ~ l3_lattices(sK10)
| spl144_4 ),
inference(forward_subsumption_resolution,[],[f5032,f3808]) ).
fof(f5036,plain,
( ~ l3_lattices(sK10)
| spl144_4
| ~ spl144_6 ),
inference(forward_subsumption_resolution,[],[f5035,f4807]) ).
fof(f5037,plain,
( $false
| spl144_4
| ~ spl144_6 ),
inference(forward_subsumption_resolution,[],[f5036,f3807]) ).
fof(f5038,plain,
( spl144_4
| ~ spl144_6 ),
inference(avatar_contradiction_clause,[],[f5037]) ).
fof(f5039,plain,
( $false
| spl144_7
| ~ spl144_12 ),
inference(forward_subsumption_resolution,[],[f4965,f4812]) ).
fof(f5040,plain,
( spl144_7
| ~ spl144_12 ),
inference(avatar_contradiction_clause,[],[f5039]) ).
fof(f5041,plain,
( ~ v10_lattices(k1_lattice2(sK10))
| ~ v15_lattices(k1_lattice2(sK10))
| sP0(sK10)
| ~ l3_lattices(k1_lattice2(sK10))
| ~ sP1(sK10)
| spl144_5
| ~ spl144_14 ),
inference(forward_subsumption_resolution,[],[f4980,f4790]) ).
fof(f5042,plain,
( ~ v15_lattices(k1_lattice2(sK10))
| sP0(sK10)
| ~ l3_lattices(k1_lattice2(sK10))
| ~ sP1(sK10)
| ~ spl144_4
| spl144_5
| ~ spl144_14 ),
inference(forward_subsumption_resolution,[],[f5041,f4785]) ).
fof(f5043,plain,
( sP0(sK10)
| ~ l3_lattices(k1_lattice2(sK10))
| ~ sP1(sK10)
| ~ spl144_4
| spl144_5
| ~ spl144_14
| ~ spl144_15 ),
inference(forward_subsumption_resolution,[],[f5042,f4944]) ).
fof(f5044,plain,
( ~ l3_lattices(k1_lattice2(sK10))
| ~ sP1(sK10)
| ~ spl144_4
| spl144_5
| spl144_12
| ~ spl144_14
| ~ spl144_15 ),
inference(forward_subsumption_resolution,[],[f5043,f4919]) ).
fof(f5045,plain,
( ~ sP1(sK10)
| ~ spl144_2
| ~ spl144_4
| spl144_5
| spl144_12
| ~ spl144_14
| ~ spl144_15 ),
inference(forward_subsumption_resolution,[],[f5044,f4775]) ).
fof(f5046,plain,
( $false
| ~ spl144_2
| ~ spl144_4
| spl144_5
| ~ spl144_11
| spl144_12
| ~ spl144_14
| ~ spl144_15 ),
inference(forward_subsumption_resolution,[],[f5045,f4914]) ).
fof(f5047,plain,
( ~ spl144_2
| ~ spl144_4
| spl144_5
| ~ spl144_11
| spl144_12
| ~ spl144_14
| ~ spl144_15 ),
inference(avatar_contradiction_clause,[],[f5046]) ).
fof(f5048,plain,
( $false
| spl144_8
| ~ spl144_12 ),
inference(forward_subsumption_resolution,[],[f4966,f4816]) ).
fof(f5049,plain,
( spl144_8
| ~ spl144_12 ),
inference(avatar_contradiction_clause,[],[f5048]) ).
fof(f5053,plain,
( v3_struct_0(k1_lattice2(sK10))
| ~ l3_lattices(k1_lattice2(sK10))
| ~ spl144_3
| spl144_14 ),
inference(forward_subsumption_resolution,[],[f5021,f4941]) ).
fof(f5055,plain,
( ~ l3_lattices(k1_lattice2(sK10))
| ~ spl144_3
| spl144_5
| spl144_14 ),
inference(forward_subsumption_resolution,[],[f5053,f4790]) ).
fof(f5058,plain,
( $false
| ~ spl144_2
| ~ spl144_3
| spl144_5
| spl144_14 ),
inference(forward_subsumption_resolution,[],[f5055,f4775]) ).
fof(f5059,plain,
( ~ spl144_2
| ~ spl144_3
| spl144_5
| spl144_14 ),
inference(avatar_contradiction_clause,[],[f5058]) ).
cnf(s2,plain,
( spl144_1
| spl144_3 ),
inference(sat_conversion,[],[f4781]) ).
cnf(s3,plain,
( spl144_1
| spl144_4 ),
inference(sat_conversion,[],[f4786]) ).
cnf(s5,plain,
( ~ spl144_1
| ~ spl144_2
| ~ spl144_3
| ~ spl144_4
| spl144_5 ),
inference(sat_conversion,[],[f4795]) ).
cnf(s7,plain,
( spl144_1
| ~ spl144_6
| ~ spl144_7
| ~ spl144_8 ),
inference(sat_conversion,[],[f4818]) ).
cnf(s10,plain,
( ~ spl144_2
| ~ spl144_3
| ~ spl144_4
| spl144_5
| spl144_6 ),
inference(sat_conversion,[],[f4868]) ).
cnf(s16,plain,
( ~ spl144_1
| spl144_8 ),
inference(sat_conversion,[],[f4904]) ).
cnf(s17,plain,
( ~ spl144_1
| spl144_7 ),
inference(sat_conversion,[],[f4906]) ).
cnf(s18,plain,
( ~ spl144_1
| spl144_6 ),
inference(sat_conversion,[],[f4908]) ).
cnf(s20,plain,
spl144_2,
inference(sat_conversion,[],[f4922]) ).
cnf(s23,plain,
( ~ spl144_2
| spl144_3
| spl144_5
| ~ spl144_13
| ~ spl144_14
| ~ spl144_15 ),
inference(sat_conversion,[],[f4947]) ).
cnf(s24,plain,
spl144_11,
inference(sat_conversion,[],[f4956]) ).
cnf(s25,plain,
( ~ spl144_7
| ~ spl144_8
| spl144_12 ),
inference(sat_conversion,[],[f4963]) ).
cnf(s26,plain,
( ~ spl144_6
| spl144_13 ),
inference(sat_conversion,[],[f4974]) ).
cnf(s27,plain,
( ~ spl144_11
| ~ spl144_12
| spl144_14 ),
inference(sat_conversion,[],[f4979]) ).
cnf(s28,plain,
( ~ spl144_11
| ~ spl144_12
| spl144_15 ),
inference(sat_conversion,[],[f4990]) ).
cnf(s30,plain,
( ~ spl144_2
| spl144_5
| spl144_15
| ~ spl144_16
| ~ spl144_17 ),
inference(sat_conversion,[],[f5000]) ).
cnf(s32,plain,
~ spl144_5,
inference(sat_conversion,[],[f5012]) ).
cnf(s34,plain,
( ~ spl144_2
| ~ spl144_3
| spl144_5
| spl144_16 ),
inference(sat_conversion,[],[f5017]) ).
cnf(s35,plain,
( ~ spl144_2
| ~ spl144_3
| spl144_5
| spl144_17 ),
inference(sat_conversion,[],[f5019]) ).
cnf(s37,plain,
( spl144_4
| ~ spl144_6 ),
inference(sat_conversion,[],[f5038]) ).
cnf(s38,plain,
( spl144_7
| ~ spl144_12 ),
inference(sat_conversion,[],[f5040]) ).
cnf(s39,plain,
( ~ spl144_2
| ~ spl144_4
| spl144_5
| ~ spl144_11
| spl144_12
| ~ spl144_14
| ~ spl144_15 ),
inference(sat_conversion,[],[f5047]) ).
cnf(s40,plain,
( spl144_8
| ~ spl144_12 ),
inference(sat_conversion,[],[f5049]) ).
cnf(s43,plain,
( ~ spl144_2
| ~ spl144_3
| spl144_5
| spl144_14 ),
inference(sat_conversion,[],[f5059]) ).
cnf(s44,plain,
( ~ spl144_2
| spl144_15
| ~ spl144_16
| ~ spl144_17 ),
inference(rat,[],[s30,s32]) ).
cnf(s46,plain,
( ~ spl144_2
| spl144_3
| ~ spl144_13
| ~ spl144_14
| ~ spl144_15 ),
inference(rat,[],[s23,s32]) ).
cnf(s48,plain,
( ~ spl144_3
| ~ spl144_4
| spl144_6 ),
inference(rat,[],[s10,s32,s20]) ).
cnf(s49,plain,
( ~ spl144_1
| ~ spl144_3
| ~ spl144_4 ),
inference(rat,[],[s5,s32,s20]) ).
cnf(s50,plain,
spl144_1,
inference(rat,[],[s7,s38,s40,s39,s44,s48,s34,s35,s43,s2,s3,s32,s24,s20]) ).
cnf(s51,plain,
spl144_6,
inference(rat,[],[s18,s50]) ).
cnf(s52,plain,
spl144_7,
inference(rat,[],[s17,s50]) ).
cnf(s53,plain,
spl144_8,
inference(rat,[],[s16,s50]) ).
cnf(s56,plain,
spl144_4,
inference(rat,[],[s37,s51]) ).
cnf(s57,plain,
spl144_13,
inference(rat,[],[s26,s51]) ).
cnf(s58,plain,
spl144_12,
inference(rat,[],[s25,s53,s52]) ).
cnf(s59,plain,
~ spl144_3,
inference(rat,[],[s49,s50,s56]) ).
cnf(s60,plain,
spl144_15,
inference(rat,[],[s28,s24,s58]) ).
cnf(s61,plain,
spl144_14,
inference(rat,[],[s27,s24,s58]) ).
cnf(s62,plain,
$false,
inference(rat,[],[s46,s57,s59,s20,s60,s61]) ).
fof(f5060,plain,
$false,
inference(avatar_sat_refutation,[],[s62]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT319+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.36 % Computer : n026.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 27 14:38:27 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.39 Running first-order theorem proving
% 0.08/0.39 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
% 5.40/1.74 % (2902582)Detected formulas, will run a generic FOF schedule.
% 5.40/1.74 % (2902591)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=983084857:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 5.40/1.74 % (2902591)Refutation not found, incomplete strategy
% 5.40/1.74 % (2902591)------------------------------
% 5.40/1.74 % (2902591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.40/1.74 % (2902591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.40/1.74 % (2902591)CaDiCaL version: 2.1.3
% 5.40/1.74 % (2902591)Termination reason: Refutation not found, incomplete strategy
% 5.40/1.74 % (2902591)Time elapsed: 0.007 s
% 5.40/1.74 % (2902591)Peak memory usage: 91 MB
% 5.40/1.74 % (2902591)Instructions burned: 12 (million)
% 5.40/1.74 % (2902587)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=2824288936:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 5.40/1.74 % (2902588)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=2811826985:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 5.40/1.74 % (2902590)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3981814927:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 5.40/1.74 % (2902589)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=1403163671:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 5.40/1.74 % (2902592)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1140353745:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 5.40/1.74 % (2902590)Refutation not found, incomplete strategy
% 5.40/1.74 % (2902590)------------------------------
% 5.40/1.74 % (2902590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.40/1.74 % (2902590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.40/1.74 % (2902590)CaDiCaL version: 2.1.3
% 5.40/1.74 % (2902590)Termination reason: Refutation not found, incomplete strategy
% 5.40/1.74 % (2902590)Time elapsed: 0.011 s
% 5.40/1.74 % (2902590)Peak memory usage: 91 MB
% 5.40/1.74 % (2902590)Instructions burned: 12 (million)
% 5.40/1.74 % (2902593)dis-21_1_sil=8000:lcm=predicate:random_seed=1333539427: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)
% 5.40/1.74 % (2902592)Instruction limit reached!
% 5.40/1.74 % (2902592)------------------------------
% 5.40/1.74 % (2902592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.40/1.74 % (2902592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.40/1.74 % (2902592)CaDiCaL version: 2.1.3
% 5.40/1.74 % (2902592)Termination reason: Instruction limit
% 5.40/1.74 % (2902592)Termination phase: Clausification
% 5.40/1.74 % (2902592)Time elapsed: 0.089 s
% 5.40/1.74 % (2902592)Peak memory usage: 94 MB
% 5.40/1.74 % (2902592)Instructions burned: 139 (million)
% 5.40/1.74 % (2902593)Instruction limit reached!
% 5.40/1.74 % (2902593)------------------------------
% 5.40/1.74 % (2902593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.40/1.74 % (2902593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.40/1.74 % (2902593)CaDiCaL version: 2.1.3
% 5.40/1.74 % (2902593)Termination reason: Instruction limit
% 5.40/1.74 % (2902593)Termination phase: Property scanning
% 5.40/1.74 % (2902593)Time elapsed: 0.081 s
% 5.40/1.74 % (2902593)Peak memory usage: 93 MB
% 5.40/1.74 % (2902593)Instructions burned: 130 (million)
% 5.40/1.74 % (2902591)------------------------------
% 5.40/1.74 % (2902591)------------------------------
% 5.40/1.74 % (2902603)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1323422754:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 5.40/1.74 % (2902603)Refutation not found, incomplete strategy
% 5.40/1.74 % (2902603)------------------------------
% 5.40/1.74 % (2902603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.40/1.74 % (2902603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.40/1.74 % (2902603)CaDiCaL version: 2.1.3
% 5.40/1.74 % (2902603)Termination reason: Refutation not found, incomplete strategy
% 5.40/1.74 % (2902603)Time elapsed: 0.006 s
% 5.40/1.74 % (2902603)Peak memory usage: 91 MB
% 5.40/1.74 % (2902603)Instructions burned: 12 (million)
% 5.40/1.74 % (2902601)lrs+10_1_sil=8000:sp=occurrence:random_seed=208245235:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 5.40/1.74 % (2902601)Refutation not found, incomplete strategy
% 5.40/1.74 % (2902601)------------------------------
% 5.40/1.74 % (2902601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.40/1.74 % (2902601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.40/1.74 % (2902601)CaDiCaL version: 2.1.3
% 5.40/1.74 % (2902601)Termination reason: Refutation not found, incomplete strategy
% 5.40/1.74 % (2902601)Time elapsed: 0.012 s
% 5.40/1.74 % (2902601)Peak memory usage: 91 MB
% 5.40/1.74 % (2902601)Instructions burned: 12 (million)
% 5.40/1.74 % (2902602)lrs+10_1_sil=32000:urr=on:br=off:random_seed=315912416:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 5.40/1.74 % (2902590)------------------------------
% 5.40/1.74 % (2902590)------------------------------
% 5.40/1.74 % (2902602)Refutation not found, incomplete strategy
% 5.40/1.74 % (2902602)------------------------------
% 5.40/1.74 % (2902602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.40/1.74 % (2902602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.40/1.74 % (2902602)CaDiCaL version: 2.1.3
% 5.40/1.74 % (2902602)Termination reason: Refutation not found, incomplete strategy
% 5.40/1.74 % (2902602)Time elapsed: 0.024 s
% 5.40/1.74 % (2902602)Peak memory usage: 92 MB
% 5.40/1.74 % (2902602)Instructions burned: 40 (million)
% 5.40/1.74 % (2902603)------------------------------
% 5.40/1.74 % (2902603)------------------------------
% 5.40/1.74 % (2902607)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=2340031378:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 5.40/1.74 % (2902608)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2477846361:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 5.40/1.74 % (2902601)------------------------------
% 5.40/1.74 % (2902601)------------------------------
% 5.40/1.74 % (2902608)First to succeed.
% 5.40/1.74 % (2902608)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2902582"
% 5.40/1.74 % (2902602)------------------------------
% 5.40/1.74 % (2902602)------------------------------
% 5.40/1.74 % (2902607)Instruction limit reached!
% 5.40/1.74 % (2902607)------------------------------
% 5.40/1.74 % (2902607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.40/1.74 % (2902607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.40/1.74 % (2902607)CaDiCaL version: 2.1.3
% 5.40/1.74 % (2902607)Termination reason: Instruction limit
% 5.40/1.74 % (2902607)Termination phase: Saturation
% 5.40/1.74 % (2902607)Time elapsed: 0.144 s
% 5.40/1.74 % (2902607)Peak memory usage: 98 MB
% 5.40/1.74 % (2902607)Instructions burned: 248 (million)
% 5.40/1.74 % (2902611)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3193228999:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 5.40/1.74 % (2902608)Refutation found. Thanks to Tanya!
% 5.40/1.74 % SZS status Theorem for theBenchmark
% 5.40/1.74 % SZS output start Proof for theBenchmark
% See solution above
% 6.32/1.94 % (2902608)------------------------------
% 6.32/1.94 % (2902608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.32/1.94 % (2902608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.32/1.94 % (2902608)CaDiCaL version: 2.1.3
% 6.32/1.94 % (2902608)Termination reason: Refutation
% 6.32/1.94 % (2902608)Time elapsed: 0.026 s
% 6.32/1.94 % (2902608)Peak memory usage: 94 MB
% 6.32/1.94 % (2902608)Instructions burned: 76 (million)
% 6.32/1.94 % (2902608)------------------------------
% 6.32/1.94 % (2902608)------------------------------
% 6.32/1.94 % (2902582)Success in time 0.903 s
% 6.32/1.94 % Vampire exiting
%------------------------------------------------------------------------------