%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT346+1 : 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 : n004.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:47:09 AM UTC 2026
% Result : Theorem 1.94s 2.04s
% Output : Refutation 6.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 27
% Syntax : Number of formulae : 182 ( 27 unt; 16 def)
% Number of atoms : 680 ( 0 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 785 ( 287 ~; 310 |; 157 &)
% ( 17 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 37 ( 36 usr; 15 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-2 aty)
% Number of variables : 81 ( 0 sgn 74 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> r1_filter_1(k11_conlat_1(k7_conlat_2(X0)),k1_lattice2(k11_conlat_1(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t22_conlat_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> r1_filter_1(k11_conlat_1(k7_conlat_2(X0)),k1_lattice2(k11_conlat_1(X0))) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f14,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ( r1_filter_1(X0,X1)
<=> ? [X2] :
( m1_lattice4(X2,X0,X1)
& v3_lattice4(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_lattice4) ).
fof(f18,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> m1_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k10_conlat_2) ).
fof(f19,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_conlat_1) ).
fof(f20,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(f26,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_conlat_1(k7_conlat_2(X0))
& v4_conlat_1(k7_conlat_2(X0))
& l2_conlat_1(k7_conlat_2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_conlat_2) ).
fof(f54,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_conlat_2) ).
fof(f55,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(f60,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v4_lattice3(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v4_lattice3(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_conlat_2) ).
fof(f94,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ( r1_filter_1(X0,X1)
=> r1_filter_1(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_r1_filter_1) ).
fof(f96,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> v3_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_conlat_2) ).
fof(f110,plain,
? [X0] :
( ~ r1_filter_1(k11_conlat_1(k7_conlat_2(X0)),k1_lattice2(k11_conlat_1(X0)))
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f111,plain,
? [X0] :
( ~ r1_filter_1(k11_conlat_1(k7_conlat_2(X0)),k1_lattice2(k11_conlat_1(X0)))
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(flattening,[],[f110]) ).
fof(f132,plain,
! [X0] :
( ! [X1] :
( ( r1_filter_1(X0,X1)
<=> ? [X2] :
( m1_lattice4(X2,X0,X1)
& v3_lattice4(X2,X0,X1) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f133,plain,
! [X0] :
( ! [X1] :
( ( r1_filter_1(X0,X1)
<=> ? [X2] :
( m1_lattice4(X2,X0,X1)
& v3_lattice4(X2,X0,X1) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f132]) ).
fof(f139,plain,
! [X0] :
( m1_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f140,plain,
! [X0] :
( m1_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f139]) ).
fof(f141,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f142,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f141]) ).
fof(f143,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f146,plain,
! [X0] :
( ( ~ v3_conlat_1(k7_conlat_2(X0))
& v4_conlat_1(k7_conlat_2(X0))
& l2_conlat_1(k7_conlat_2(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f147,plain,
! [X0] :
( ( ~ v3_conlat_1(k7_conlat_2(X0))
& v4_conlat_1(k7_conlat_2(X0))
& l2_conlat_1(k7_conlat_2(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f146]) ).
fof(f162,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f54]) ).
fof(f163,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f162]) ).
fof(f164,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f55]) ).
fof(f165,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f164]) ).
fof(f170,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v4_lattice3(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f60]) ).
fof(f171,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v4_lattice3(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f170]) ).
fof(f205,plain,
! [X0,X1] :
( r1_filter_1(X1,X0)
| ~ r1_filter_1(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(ennf_transformation,[],[f94]) ).
fof(f206,plain,
! [X0,X1] :
( r1_filter_1(X1,X0)
| ~ r1_filter_1(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(flattening,[],[f205]) ).
fof(f208,plain,
! [X0] :
( v3_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f96]) ).
fof(f209,plain,
! [X0] :
( v3_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f208]) ).
fof(f219,definition,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f220,plain,
! [X0] :
( sP0(X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(definition_folding,[],[f163,f219]) ).
fof(f221,definition,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v4_lattice3(k1_lattice2(X0)) )
| ~ sP1(X0) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f222,plain,
! [X0] :
( sP1(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f171,f221]) ).
fof(f229,plain,
( ~ r1_filter_1(k11_conlat_1(k7_conlat_2(sK5)),k1_lattice2(k11_conlat_1(sK5)))
& ~ v3_conlat_1(sK5)
& l2_conlat_1(sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X0,sK5)],[f111]) ).
fof(f230,plain,
! [X0] :
( ! [X1] :
( ( ( r1_filter_1(X0,X1)
| ! [X2] :
( ~ m1_lattice4(X2,X0,X1)
| ~ v3_lattice4(X2,X0,X1) ) )
& ( ? [X2] :
( m1_lattice4(X2,X0,X1)
& v3_lattice4(X2,X0,X1) )
| ~ r1_filter_1(X0,X1) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f133]) ).
fof(f231,plain,
! [X0] :
( ! [X1] :
( ( ( r1_filter_1(X0,X1)
| ! [X2] :
( ~ m1_lattice4(X2,X0,X1)
| ~ v3_lattice4(X2,X0,X1) ) )
& ( ? [X3] :
( m1_lattice4(X3,X0,X1)
& v3_lattice4(X3,X0,X1) )
| ~ r1_filter_1(X0,X1) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f230]) ).
fof(f232,plain,
! [X0] :
( ! [X1] :
( ( ( r1_filter_1(X0,X1)
| ! [X2] :
( ~ m1_lattice4(X2,X0,X1)
| ~ v3_lattice4(X2,X0,X1) ) )
& ( ( m1_lattice4(sK6(X0,X1),X0,X1)
& v3_lattice4(sK6(X0,X1),X0,X1) )
| ~ r1_filter_1(X0,X1) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X3,sK6(X0,X1))],[f231]) ).
fof(f243,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) )
| ~ sP0(X0) ),
inference(nnf_transformation,[],[f219]) ).
fof(f244,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v4_lattice3(k1_lattice2(X0)) )
| ~ sP1(X0) ),
inference(nnf_transformation,[],[f221]) ).
fof(f265,plain,
l2_conlat_1(sK5),
inference(cnf_transformation,[],[f229]) ).
fof(f266,plain,
~ v3_conlat_1(sK5),
inference(cnf_transformation,[],[f229]) ).
fof(f267,plain,
~ r1_filter_1(k11_conlat_1(k7_conlat_2(sK5)),k1_lattice2(k11_conlat_1(sK5))),
inference(cnf_transformation,[],[f229]) ).
fof(f297,plain,
! [X2,X0,X1] :
( r1_filter_1(X0,X1)
| ~ m1_lattice4(X2,X0,X1)
| ~ v3_lattice4(X2,X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f232]) ).
fof(f303,plain,
! [X0] :
( m1_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f140]) ).
fof(f304,plain,
! [X0] :
( l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f306,plain,
! [X0] :
( ~ v3_struct_0(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f307,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f311,plain,
! [X0] :
( l2_conlat_1(k7_conlat_2(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f313,plain,
! [X0] :
( ~ v3_conlat_1(k7_conlat_2(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f341,plain,
! [X0] :
( v4_lattice3(k11_conlat_1(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f243]) ).
fof(f345,plain,
! [X0] :
( v10_lattices(k11_conlat_1(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f243]) ).
fof(f354,plain,
! [X0] :
( sP0(X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f220]) ).
fof(f356,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f165]) ).
fof(f362,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f244]) ).
fof(f371,plain,
! [X0] :
( sP1(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f222]) ).
fof(f489,plain,
! [X0,X1] :
( r1_filter_1(X1,X0)
| ~ r1_filter_1(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f206]) ).
fof(f491,plain,
! [X0] :
( v3_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f209]) ).
fof(f508,plain,
( ~ r1_filter_1(k1_lattice2(k11_conlat_1(sK5)),k11_conlat_1(k7_conlat_2(sK5)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK5)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK5)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK5)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK5)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK5)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK5))) ),
inference(resolution,[],[f489,f267]) ).
fof(f510,definition,
( spl33_3
<=> l3_lattices(k11_conlat_1(k7_conlat_2(sK5))) ),
introduced(definition,[new_symbols(definition,[spl33_3])],[avatar_definition]) ).
fof(f511,plain,
( l3_lattices(k11_conlat_1(k7_conlat_2(sK5)))
| ~ spl33_3 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f512,plain,
( ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK5)))
| spl33_3 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f514,definition,
( spl33_4
<=> v10_lattices(k11_conlat_1(k7_conlat_2(sK5))) ),
introduced(definition,[new_symbols(definition,[spl33_4])],[avatar_definition]) ).
fof(f516,plain,
( ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK5)))
| spl33_4 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f518,definition,
( spl33_5
<=> v3_struct_0(k11_conlat_1(k7_conlat_2(sK5))) ),
introduced(definition,[new_symbols(definition,[spl33_5])],[avatar_definition]) ).
fof(f520,plain,
( v3_struct_0(k11_conlat_1(k7_conlat_2(sK5)))
| ~ spl33_5 ),
inference(avatar_component_clause,[],[f518]) ).
fof(f522,definition,
( spl33_6
<=> l3_lattices(k1_lattice2(k11_conlat_1(sK5))) ),
introduced(definition,[new_symbols(definition,[spl33_6])],[avatar_definition]) ).
fof(f524,plain,
( ~ l3_lattices(k1_lattice2(k11_conlat_1(sK5)))
| spl33_6 ),
inference(avatar_component_clause,[],[f522]) ).
fof(f526,definition,
( spl33_7
<=> v10_lattices(k1_lattice2(k11_conlat_1(sK5))) ),
introduced(definition,[new_symbols(definition,[spl33_7])],[avatar_definition]) ).
fof(f528,plain,
( ~ v10_lattices(k1_lattice2(k11_conlat_1(sK5)))
| spl33_7 ),
inference(avatar_component_clause,[],[f526]) ).
fof(f530,definition,
( spl33_8
<=> v3_struct_0(k1_lattice2(k11_conlat_1(sK5))) ),
introduced(definition,[new_symbols(definition,[spl33_8])],[avatar_definition]) ).
fof(f532,plain,
( v3_struct_0(k1_lattice2(k11_conlat_1(sK5)))
| ~ spl33_8 ),
inference(avatar_component_clause,[],[f530]) ).
fof(f534,definition,
( spl33_9
<=> r1_filter_1(k1_lattice2(k11_conlat_1(sK5)),k11_conlat_1(k7_conlat_2(sK5))) ),
introduced(definition,[new_symbols(definition,[spl33_9])],[avatar_definition]) ).
fof(f536,plain,
( ~ r1_filter_1(k1_lattice2(k11_conlat_1(sK5)),k11_conlat_1(k7_conlat_2(sK5)))
| spl33_9 ),
inference(avatar_component_clause,[],[f534]) ).
fof(f537,plain,
( ~ spl33_3
| ~ spl33_4
| spl33_5
| ~ spl33_6
| ~ spl33_7
| spl33_8
| ~ spl33_9 ),
inference(avatar_split_clause,[],[f508,f534,f530,f526,f522,f518,f514,f510]) ).
fof(f538,plain,
( v3_conlat_1(k7_conlat_2(sK5))
| ~ l2_conlat_1(k7_conlat_2(sK5))
| spl33_3 ),
inference(resolution,[],[f512,f304]) ).
fof(f540,definition,
( spl33_10
<=> l2_conlat_1(k7_conlat_2(sK5)) ),
introduced(definition,[new_symbols(definition,[spl33_10])],[avatar_definition]) ).
fof(f541,plain,
( l2_conlat_1(k7_conlat_2(sK5))
| ~ spl33_10 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f542,plain,
( ~ l2_conlat_1(k7_conlat_2(sK5))
| spl33_10 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f544,definition,
( spl33_11
<=> v3_conlat_1(k7_conlat_2(sK5)) ),
introduced(definition,[new_symbols(definition,[spl33_11])],[avatar_definition]) ).
fof(f545,plain,
( ~ v3_conlat_1(k7_conlat_2(sK5))
| spl33_11 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f546,plain,
( v3_conlat_1(k7_conlat_2(sK5))
| ~ spl33_11 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f547,plain,
( ~ spl33_10
| spl33_11
| spl33_3 ),
inference(avatar_split_clause,[],[f538,f510,f544,f540]) ).
fof(f550,plain,
( v3_conlat_1(sK5)
| ~ l2_conlat_1(sK5)
| spl33_10 ),
inference(resolution,[],[f542,f311]) ).
fof(f551,plain,
( ~ l2_conlat_1(sK5)
| spl33_10 ),
inference(forward_subsumption_resolution,[],[f550,f266]) ).
fof(f552,plain,
( $false
| spl33_10 ),
inference(forward_subsumption_resolution,[],[f551,f265]) ).
fof(f553,plain,
spl33_10,
inference(avatar_contradiction_clause,[],[f552]) ).
fof(f560,plain,
( ! [X0] :
( ~ m1_lattice4(X0,k1_lattice2(k11_conlat_1(sK5)),k11_conlat_1(k7_conlat_2(sK5)))
| ~ v3_lattice4(X0,k1_lattice2(k11_conlat_1(sK5)),k11_conlat_1(k7_conlat_2(sK5)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK5)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK5)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK5)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK5)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK5)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK5))) )
| spl33_9 ),
inference(resolution,[],[f536,f297]) ).
fof(f568,plain,
( ~ sP0(k7_conlat_2(sK5))
| spl33_4 ),
inference(resolution,[],[f345,f516]) ).
fof(f570,plain,
( v3_conlat_1(k7_conlat_2(sK5))
| ~ l2_conlat_1(k7_conlat_2(sK5))
| spl33_4 ),
inference(resolution,[],[f568,f354]) ).
fof(f571,plain,
( v3_conlat_1(k7_conlat_2(sK5))
| spl33_4
| ~ spl33_10 ),
inference(forward_subsumption_resolution,[],[f570,f541]) ).
fof(f572,plain,
( spl33_11
| spl33_4
| ~ spl33_10 ),
inference(avatar_split_clause,[],[f571,f540,f514,f544]) ).
fof(f573,plain,
( v3_conlat_1(sK5)
| ~ l2_conlat_1(sK5)
| ~ spl33_11 ),
inference(resolution,[],[f546,f313]) ).
fof(f574,plain,
( ~ l2_conlat_1(sK5)
| ~ spl33_11 ),
inference(forward_subsumption_resolution,[],[f573,f266]) ).
fof(f575,plain,
( $false
| ~ spl33_11 ),
inference(forward_subsumption_resolution,[],[f574,f265]) ).
fof(f576,plain,
~ spl33_11,
inference(avatar_contradiction_clause,[],[f575]) ).
fof(f577,plain,
( ! [X0] :
( ~ m1_lattice4(X0,k1_lattice2(k11_conlat_1(sK5)),k11_conlat_1(k7_conlat_2(sK5)))
| ~ v3_lattice4(X0,k1_lattice2(k11_conlat_1(sK5)),k11_conlat_1(k7_conlat_2(sK5)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK5)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK5)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK5)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK5)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK5))) )
| ~ spl33_3
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f560,f511]) ).
fof(f579,definition,
( spl33_13
<=> ! [X0] :
( ~ m1_lattice4(X0,k1_lattice2(k11_conlat_1(sK5)),k11_conlat_1(k7_conlat_2(sK5)))
| ~ v3_lattice4(X0,k1_lattice2(k11_conlat_1(sK5)),k11_conlat_1(k7_conlat_2(sK5))) ) ),
introduced(definition,[new_symbols(definition,[spl33_13])],[avatar_definition]) ).
fof(f580,plain,
( ! [X0] :
( ~ v3_lattice4(X0,k1_lattice2(k11_conlat_1(sK5)),k11_conlat_1(k7_conlat_2(sK5)))
| ~ m1_lattice4(X0,k1_lattice2(k11_conlat_1(sK5)),k11_conlat_1(k7_conlat_2(sK5))) )
| ~ spl33_13 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f581,plain,
( ~ spl33_6
| ~ spl33_7
| spl33_8
| ~ spl33_4
| spl33_5
| spl33_13
| ~ spl33_3
| spl33_9 ),
inference(avatar_split_clause,[],[f577,f534,f510,f579,f518,f514,f530,f526,f522]) ).
fof(f582,plain,
( ~ l3_lattices(k11_conlat_1(sK5))
| spl33_6 ),
inference(resolution,[],[f524,f307]) ).
fof(f583,plain,
( v3_conlat_1(sK5)
| ~ l2_conlat_1(sK5)
| spl33_6 ),
inference(resolution,[],[f582,f304]) ).
fof(f584,plain,
( ~ l2_conlat_1(sK5)
| spl33_6 ),
inference(forward_subsumption_resolution,[],[f583,f266]) ).
fof(f585,plain,
( $false
| spl33_6 ),
inference(forward_subsumption_resolution,[],[f584,f265]) ).
fof(f586,plain,
spl33_6,
inference(avatar_contradiction_clause,[],[f585]) ).
fof(f593,plain,
( ~ sP1(k11_conlat_1(sK5))
| spl33_7 ),
inference(resolution,[],[f362,f528]) ).
fof(f596,definition,
( spl33_14
<=> l3_lattices(k11_conlat_1(sK5)) ),
introduced(definition,[new_symbols(definition,[spl33_14])],[avatar_definition]) ).
fof(f597,plain,
( l3_lattices(k11_conlat_1(sK5))
| ~ spl33_14 ),
inference(avatar_component_clause,[],[f596]) ).
fof(f598,plain,
( ~ l3_lattices(k11_conlat_1(sK5))
| spl33_14 ),
inference(avatar_component_clause,[],[f596]) ).
fof(f600,definition,
( spl33_15
<=> v4_lattice3(k11_conlat_1(sK5)) ),
introduced(definition,[new_symbols(definition,[spl33_15])],[avatar_definition]) ).
fof(f601,plain,
( v4_lattice3(k11_conlat_1(sK5))
| ~ spl33_15 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f602,plain,
( ~ v4_lattice3(k11_conlat_1(sK5))
| spl33_15 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f604,definition,
( spl33_16
<=> v10_lattices(k11_conlat_1(sK5)) ),
introduced(definition,[new_symbols(definition,[spl33_16])],[avatar_definition]) ).
fof(f605,plain,
( v10_lattices(k11_conlat_1(sK5))
| ~ spl33_16 ),
inference(avatar_component_clause,[],[f604]) ).
fof(f606,plain,
( ~ v10_lattices(k11_conlat_1(sK5))
| spl33_16 ),
inference(avatar_component_clause,[],[f604]) ).
fof(f608,definition,
( spl33_17
<=> v3_struct_0(k11_conlat_1(sK5)) ),
introduced(definition,[new_symbols(definition,[spl33_17])],[avatar_definition]) ).
fof(f610,plain,
( v3_struct_0(k11_conlat_1(sK5))
| ~ spl33_17 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f612,plain,
( v3_conlat_1(sK5)
| ~ l2_conlat_1(sK5)
| spl33_14 ),
inference(resolution,[],[f598,f304]) ).
fof(f613,plain,
( ~ l2_conlat_1(sK5)
| spl33_14 ),
inference(forward_subsumption_resolution,[],[f612,f266]) ).
fof(f614,plain,
( $false
| spl33_14 ),
inference(forward_subsumption_resolution,[],[f613,f265]) ).
fof(f615,plain,
spl33_14,
inference(avatar_contradiction_clause,[],[f614]) ).
fof(f616,plain,
( ~ sP0(sK5)
| spl33_15 ),
inference(resolution,[],[f602,f341]) ).
fof(f617,plain,
( v3_conlat_1(sK5)
| ~ l2_conlat_1(sK5)
| spl33_15 ),
inference(resolution,[],[f616,f354]) ).
fof(f618,plain,
( ~ l2_conlat_1(sK5)
| spl33_15 ),
inference(forward_subsumption_resolution,[],[f617,f266]) ).
fof(f619,plain,
( $false
| spl33_15 ),
inference(forward_subsumption_resolution,[],[f618,f265]) ).
fof(f620,plain,
spl33_15,
inference(avatar_contradiction_clause,[],[f619]) ).
fof(f622,plain,
( ~ sP0(sK5)
| spl33_16 ),
inference(resolution,[],[f606,f345]) ).
fof(f623,plain,
( v3_conlat_1(sK5)
| ~ l2_conlat_1(sK5)
| spl33_16 ),
inference(resolution,[],[f622,f354]) ).
fof(f624,plain,
( ~ l2_conlat_1(sK5)
| spl33_16 ),
inference(forward_subsumption_resolution,[],[f623,f266]) ).
fof(f625,plain,
( $false
| spl33_16 ),
inference(forward_subsumption_resolution,[],[f624,f265]) ).
fof(f626,plain,
spl33_16,
inference(avatar_contradiction_clause,[],[f625]) ).
fof(f627,plain,
( v3_struct_0(k11_conlat_1(sK5))
| ~ l3_lattices(k11_conlat_1(sK5))
| ~ spl33_8 ),
inference(resolution,[],[f532,f356]) ).
fof(f628,plain,
( v3_struct_0(k11_conlat_1(sK5))
| ~ spl33_8
| ~ spl33_14 ),
inference(forward_subsumption_resolution,[],[f627,f597]) ).
fof(f629,plain,
( spl33_17
| ~ spl33_8
| ~ spl33_14 ),
inference(avatar_split_clause,[],[f628,f596,f530,f608]) ).
fof(f631,plain,
( ~ m1_lattice4(k10_conlat_2(sK5),k1_lattice2(k11_conlat_1(sK5)),k11_conlat_1(k7_conlat_2(sK5)))
| v3_conlat_1(sK5)
| ~ l2_conlat_1(sK5)
| ~ spl33_13 ),
inference(resolution,[],[f580,f491]) ).
fof(f633,plain,
( v3_conlat_1(sK5)
| ~ l2_conlat_1(sK5)
| ~ spl33_13 ),
inference(forward_subsumption_resolution,[],[f631,f303]) ).
fof(f634,plain,
( ~ l2_conlat_1(sK5)
| ~ spl33_13 ),
inference(forward_subsumption_resolution,[],[f633,f266]) ).
fof(f635,plain,
( $false
| ~ spl33_13 ),
inference(forward_subsumption_resolution,[],[f634,f265]) ).
fof(f636,plain,
~ spl33_13,
inference(avatar_contradiction_clause,[],[f635]) ).
fof(f638,plain,
( v3_conlat_1(k7_conlat_2(sK5))
| ~ l2_conlat_1(k7_conlat_2(sK5))
| ~ spl33_5 ),
inference(resolution,[],[f520,f306]) ).
fof(f639,plain,
( ~ l2_conlat_1(k7_conlat_2(sK5))
| ~ spl33_5
| spl33_11 ),
inference(forward_subsumption_resolution,[],[f638,f545]) ).
fof(f640,plain,
( $false
| ~ spl33_5
| ~ spl33_10
| spl33_11 ),
inference(forward_subsumption_resolution,[],[f639,f541]) ).
fof(f641,plain,
( ~ spl33_5
| ~ spl33_10
| spl33_11 ),
inference(avatar_contradiction_clause,[],[f640]) ).
fof(f642,plain,
( v3_struct_0(k11_conlat_1(sK5))
| ~ v10_lattices(k11_conlat_1(sK5))
| ~ v4_lattice3(k11_conlat_1(sK5))
| ~ l3_lattices(k11_conlat_1(sK5))
| spl33_7 ),
inference(resolution,[],[f593,f371]) ).
fof(f643,plain,
( v3_struct_0(k11_conlat_1(sK5))
| ~ v4_lattice3(k11_conlat_1(sK5))
| ~ l3_lattices(k11_conlat_1(sK5))
| spl33_7
| ~ spl33_16 ),
inference(forward_subsumption_resolution,[],[f642,f605]) ).
fof(f644,plain,
( v3_struct_0(k11_conlat_1(sK5))
| ~ l3_lattices(k11_conlat_1(sK5))
| spl33_7
| ~ spl33_15
| ~ spl33_16 ),
inference(forward_subsumption_resolution,[],[f643,f601]) ).
fof(f645,plain,
( v3_struct_0(k11_conlat_1(sK5))
| spl33_7
| ~ spl33_14
| ~ spl33_15
| ~ spl33_16 ),
inference(forward_subsumption_resolution,[],[f644,f597]) ).
fof(f646,plain,
( spl33_17
| spl33_7
| ~ spl33_14
| ~ spl33_15
| ~ spl33_16 ),
inference(avatar_split_clause,[],[f645,f604,f600,f596,f526,f608]) ).
fof(f648,plain,
( v3_conlat_1(sK5)
| ~ l2_conlat_1(sK5)
| ~ spl33_17 ),
inference(resolution,[],[f610,f306]) ).
fof(f649,plain,
( ~ l2_conlat_1(sK5)
| ~ spl33_17 ),
inference(forward_subsumption_resolution,[],[f648,f266]) ).
fof(f650,plain,
( $false
| ~ spl33_17 ),
inference(forward_subsumption_resolution,[],[f649,f265]) ).
fof(f651,plain,
~ spl33_17,
inference(avatar_contradiction_clause,[],[f650]) ).
cnf(s2,plain,
( ~ spl33_3
| ~ spl33_4
| spl33_5
| ~ spl33_6
| ~ spl33_7
| spl33_8
| ~ spl33_9 ),
inference(sat_conversion,[],[f537]) ).
cnf(s3,plain,
( spl33_3
| ~ spl33_10
| spl33_11 ),
inference(sat_conversion,[],[f547]) ).
cnf(s4,plain,
spl33_10,
inference(sat_conversion,[],[f553]) ).
cnf(s6,plain,
( spl33_4
| ~ spl33_10
| spl33_11 ),
inference(sat_conversion,[],[f572]) ).
cnf(s7,plain,
~ spl33_11,
inference(sat_conversion,[],[f576]) ).
cnf(s8,plain,
( ~ spl33_3
| ~ spl33_4
| spl33_5
| ~ spl33_6
| ~ spl33_7
| spl33_8
| spl33_9
| spl33_13 ),
inference(sat_conversion,[],[f581]) ).
cnf(s9,plain,
spl33_6,
inference(sat_conversion,[],[f586]) ).
cnf(s11,plain,
spl33_14,
inference(sat_conversion,[],[f615]) ).
cnf(s12,plain,
spl33_15,
inference(sat_conversion,[],[f620]) ).
cnf(s13,plain,
spl33_16,
inference(sat_conversion,[],[f626]) ).
cnf(s14,plain,
( ~ spl33_8
| ~ spl33_14
| spl33_17 ),
inference(sat_conversion,[],[f629]) ).
cnf(s15,plain,
~ spl33_13,
inference(sat_conversion,[],[f636]) ).
cnf(s16,plain,
( ~ spl33_5
| ~ spl33_10
| spl33_11 ),
inference(sat_conversion,[],[f641]) ).
cnf(s17,plain,
( spl33_7
| ~ spl33_14
| ~ spl33_15
| ~ spl33_16
| spl33_17 ),
inference(sat_conversion,[],[f646]) ).
cnf(s18,plain,
~ spl33_17,
inference(sat_conversion,[],[f651]) ).
cnf(s19,plain,
( spl33_7
| ~ spl33_14
| ~ spl33_15
| ~ spl33_16 ),
inference(rat,[],[s17,s18]) ).
cnf(s20,plain,
( ~ spl33_8
| ~ spl33_14 ),
inference(rat,[],[s14,s18]) ).
cnf(s21,plain,
spl33_7,
inference(rat,[],[s19,s13,s12,s11]) ).
cnf(s22,plain,
~ spl33_8,
inference(rat,[],[s20,s11]) ).
cnf(s23,plain,
( ~ spl33_3
| ~ spl33_4
| spl33_5
| spl33_9 ),
inference(rat,[],[s8,s15,s22,s21,s9]) ).
cnf(s24,plain,
( spl33_4
| ~ spl33_10 ),
inference(rat,[],[s6,s7]) ).
cnf(s26,plain,
~ spl33_5,
inference(rat,[],[s16,s7,s4]) ).
cnf(s27,plain,
spl33_4,
inference(rat,[],[s24,s4]) ).
cnf(s28,plain,
spl33_3,
inference(rat,[],[s3,s7,s4]) ).
cnf(s29,plain,
spl33_9,
inference(rat,[],[s23,s27,s26,s28]) ).
cnf(s31,plain,
$false,
inference(rat,[],[s2,s29,s22,s21,s9,s26,s27,s28]) ).
fof(f652,plain,
$false,
inference(avatar_sat_refutation,[],[s31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT346+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.43 % Computer : n004.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sun Sep 27 14:52:07 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.50 Running first-order theorem proving
% 0.23/0.50 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
% 1.94/2.04 % (3614536)Detected formulas, will run a generic FOF schedule.
% 1.94/2.04 % (3614545)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=277577976:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 1.94/2.04 % (3614545)Refutation not found, incomplete strategy
% 1.94/2.04 % (3614545)------------------------------
% 1.94/2.04 % (3614545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.94/2.04 % (3614545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/2.04 % (3614545)CaDiCaL version: 2.1.3
% 1.94/2.04 % (3614545)Termination reason: Refutation not found, incomplete strategy
% 1.94/2.04 % (3614545)Time elapsed: 0.002 s
% 1.94/2.04 % (3614545)Peak memory usage: 88 MB
% 1.94/2.04 % (3614545)Instructions burned: 2 (million)
% 1.94/2.04 % (3614541)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=1071005147:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 1.94/2.04 % (3614542)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=3385729302:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 1.94/2.04 % (3614543)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=282716050:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 1.94/2.04 % (3614544)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=770850624:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 1.94/2.04 % (3614546)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3786529892:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 1.94/2.04 % (3614547)dis-21_1_sil=8000:lcm=predicate:random_seed=790324286:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 1.94/2.04 % (3614544)Refutation not found, incomplete strategy
% 1.94/2.04 % (3614544)------------------------------
% 1.94/2.04 % (3614544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.94/2.04 % (3614544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/2.04 % (3614544)CaDiCaL version: 2.1.3
% 1.94/2.04 % (3614544)Termination reason: Refutation not found, incomplete strategy
% 1.94/2.04 % (3614544)Time elapsed: 0.003 s
% 1.94/2.04 % (3614544)Peak memory usage: 88 MB
% 1.94/2.04 % (3614544)Instructions burned: 1 (million)
% 1.94/2.04 % (3614546)First to succeed.
% 1.94/2.04 % (3614546)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3614536"
% 1.94/2.04 % (3614547)Instruction limit reached!
% 1.94/2.04 % (3614547)------------------------------
% 1.94/2.04 % (3614547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.94/2.04 % (3614547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/2.04 % (3614547)CaDiCaL version: 2.1.3
% 1.94/2.04 % (3614547)Termination reason: Instruction limit
% 1.94/2.04 % (3614547)Termination phase: Saturation
% 1.94/2.04 % (3614547)Time elapsed: 0.114 s
% 1.94/2.04 % (3614547)Peak memory usage: 91 MB
% 1.94/2.04 % (3614547)Instructions burned: 129 (million)
% 1.94/2.04 % (3614545)------------------------------
% 1.94/2.04 % (3614545)------------------------------
% 1.94/2.04 % (3614544)------------------------------
% 1.94/2.04 % (3614544)------------------------------
% 1.94/2.04 % (3614556)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1840053231:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 1.94/2.04 % (3614556)Also succeeded, but the first one will report.
% 1.94/2.04 % (3614555)lrs+10_1_sil=8000:sp=occurrence:random_seed=1252274980:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 1.94/2.04 % (3614546)Refutation found. Thanks to Tanya!
% 1.94/2.04 % SZS status Theorem for theBenchmark
% 1.94/2.04 % SZS output start Proof for theBenchmark
% See solution above
% 6.47/2.39 % (3614546)------------------------------
% 6.47/2.39 % (3614546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.47/2.39 % (3614546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/2.39 % (3614546)CaDiCaL version: 2.1.3
% 6.47/2.39 % (3614546)Termination reason: Refutation
% 6.47/2.39 % (3614546)Time elapsed: 0.023 s
% 6.47/2.39 % (3614546)Peak memory usage: 90 MB
% 6.47/2.39 % (3614546)Instructions burned: 18 (million)
% 6.47/2.39 % (3614546)------------------------------
% 6.47/2.39 % (3614546)------------------------------
% 6.47/2.39 % (3614536)Success in time 0.767 s
% 6.47/2.39 % Vampire exiting
%------------------------------------------------------------------------------