%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT337+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:04 AM UTC 2026
% Result : Theorem 8.11s 2.13s
% Output : Refutation 8.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 22
% Syntax : Number of formulae : 191 ( 29 unt; 14 def)
% Number of atoms : 951 ( 6 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 1318 ( 558 ~; 571 |; 150 &)
% ( 13 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 36 ( 34 usr; 14 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 98 ( 0 sgn 92 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
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/sandbox/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/sandbox/benchmark/theBenchmark.p',cc6_lattices) ).
fof(f2331,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& v10_lattices(X0)
& v12_lattices(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc7_lattices) ).
fof(f2912,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k22_filter_2) ).
fof(f3017,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( v11_lattices(X0)
=> v11_lattices(k23_filter_2(X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t78_filter_2) ).
fof(f3023,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r3_lattices(X0,X1,X2)
=> ( v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& k6_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) = X2
& k5_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) = X1 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t84_filter_2) ).
fof(f3025,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0)
& v12_lattices(X0)
& r3_lattices(X0,X1,X2) )
=> ( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t86_filter_2) ).
fof(f3026,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0)
& r3_lattices(X0,X1,X2) )
=> ( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v17_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t87_filter_2) ).
fof(f3027,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0)
& r3_lattices(X0,X1,X2) )
=> ( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v17_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f3026]) ).
fof(f3145,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f2912]) ).
fof(f3146,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f3145]) ).
fof(f3352,plain,
! [X0] :
( ! [X1] :
( v11_lattices(k23_filter_2(X0,X1))
| ~ v11_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3017]) ).
fof(f3353,plain,
! [X0] :
( ! [X1] :
( v11_lattices(k23_filter_2(X0,X1))
| ~ v11_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3352]) ).
fof(f3364,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& k6_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) = X2
& k5_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) = X1 )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3023]) ).
fof(f3365,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& k6_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) = X2
& k5_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) = X1 )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3364]) ).
fof(f3368,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v12_lattices(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3025]) ).
fof(f3369,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v12_lattices(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3368]) ).
fof(f3370,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v17_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0)
& r3_lattices(X0,X1,X2)
& m1_subset_1(X2,u1_struct_0(X0)) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f3027]) ).
fof(f3371,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v17_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0)
& r3_lattices(X0,X1,X2)
& m1_subset_1(X2,u1_struct_0(X0)) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f3370]) ).
fof(f3688,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(f3689,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,[],[f3688]) ).
fof(f3690,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(f3691,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,[],[f3690]) ).
fof(f3827,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& v10_lattices(X0)
& v12_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2331]) ).
fof(f3828,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& v10_lattices(X0)
& v12_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3827]) ).
fof(f3876,definition,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& v10_lattices(X0)
& v12_lattices(X0) )
| ~ sP13(X0) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f3877,plain,
! [X0] :
( sP13(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f3828,f3876]) ).
fof(f3961,plain,
( ( v3_struct_0(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| ~ v10_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| ~ v17_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| ~ l3_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50))) )
& ~ v3_struct_0(sK48)
& v10_lattices(sK48)
& v17_lattices(sK48)
& l3_lattices(sK48)
& r3_lattices(sK48,sK49,sK50)
& m1_subset_1(sK50,u1_struct_0(sK48))
& m1_subset_1(sK49,u1_struct_0(sK48))
& ~ v3_struct_0(sK48)
& v10_lattices(sK48)
& l3_lattices(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48,sK49,sK50]),skolemize(X0,sK48),skolemize(X1,sK49),skolemize(X2,sK50)],[f3371]) ).
fof(f4169,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& v10_lattices(X0)
& v12_lattices(X0) )
| ~ sP13(X0) ),
inference(nnf_transformation,[],[f3876]) ).
fof(f4227,plain,
! [X2,X0,X1] :
( m2_lattice4(k22_filter_2(X0,X1,X2),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f3146]) ).
fof(f4228,plain,
! [X2,X0,X1] :
( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f3146]) ).
fof(f4530,plain,
! [X0,X1] :
( v11_lattices(k23_filter_2(X0,X1))
| ~ v11_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3353]) ).
fof(f4539,plain,
! [X2,X0,X1] :
( v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3365]) ).
fof(f4545,plain,
! [X2,X0,X1] :
( l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v12_lattices(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3369]) ).
fof(f4546,plain,
! [X2,X0,X1] :
( v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v12_lattices(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3369]) ).
fof(f4548,plain,
! [X2,X0,X1] :
( v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v12_lattices(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3369]) ).
fof(f4549,plain,
! [X2,X0,X1] :
( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v12_lattices(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3369]) ).
fof(f4550,plain,
l3_lattices(sK48),
inference(cnf_transformation,[],[f3961]) ).
fof(f4551,plain,
v10_lattices(sK48),
inference(cnf_transformation,[],[f3961]) ).
fof(f4552,plain,
~ v3_struct_0(sK48),
inference(cnf_transformation,[],[f3961]) ).
fof(f4553,plain,
m1_subset_1(sK49,u1_struct_0(sK48)),
inference(cnf_transformation,[],[f3961]) ).
fof(f4554,plain,
m1_subset_1(sK50,u1_struct_0(sK48)),
inference(cnf_transformation,[],[f3961]) ).
fof(f4555,plain,
r3_lattices(sK48,sK49,sK50),
inference(cnf_transformation,[],[f3961]) ).
fof(f4557,plain,
v17_lattices(sK48),
inference(cnf_transformation,[],[f3961]) ).
fof(f4560,plain,
( v3_struct_0(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| ~ v10_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| ~ v17_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| ~ l3_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50))) ),
inference(cnf_transformation,[],[f3961]) ).
fof(f5012,plain,
! [X0] :
( v17_lattices(X0)
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3689]) ).
fof(f5014,plain,
! [X0] :
( v16_lattices(X0)
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3691]) ).
fof(f5015,plain,
! [X0] :
( v15_lattices(X0)
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3691]) ).
fof(f5018,plain,
! [X0] :
( v11_lattices(X0)
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3691]) ).
fof(f5222,plain,
! [X0] :
( v12_lattices(X0)
| ~ sP13(X0) ),
inference(cnf_transformation,[],[f4169]) ).
fof(f5231,plain,
! [X0] :
( sP13(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3877]) ).
fof(f5399,plain,
! [X2,X0,X1] :
( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v12_lattices(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(duplicate_literal_removal,[],[f4549]) ).
fof(f5400,plain,
! [X2,X0,X1] :
( v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v12_lattices(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(duplicate_literal_removal,[],[f4548]) ).
fof(f5402,plain,
! [X2,X0,X1] :
( v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v12_lattices(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(duplicate_literal_removal,[],[f4546]) ).
fof(f5403,plain,
! [X2,X0,X1] :
( l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v12_lattices(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(duplicate_literal_removal,[],[f4545]) ).
fof(f5436,definition,
( spl175_1
<=> l3_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50))) ),
introduced(definition,[new_symbols(definition,[spl175_1])],[avatar_definition]) ).
fof(f5437,plain,
( ~ l3_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| spl175_1 ),
inference(avatar_component_clause,[],[f5436]) ).
fof(f5439,definition,
( spl175_2
<=> v17_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50))) ),
introduced(definition,[new_symbols(definition,[spl175_2])],[avatar_definition]) ).
fof(f5440,plain,
( ~ v17_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| spl175_2 ),
inference(avatar_component_clause,[],[f5439]) ).
fof(f5442,definition,
( spl175_3
<=> v10_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50))) ),
introduced(definition,[new_symbols(definition,[spl175_3])],[avatar_definition]) ).
fof(f5443,plain,
( ~ v10_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| spl175_3 ),
inference(avatar_component_clause,[],[f5442]) ).
fof(f5445,definition,
( spl175_4
<=> v3_struct_0(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50))) ),
introduced(definition,[new_symbols(definition,[spl175_4])],[avatar_definition]) ).
fof(f5446,plain,
( v3_struct_0(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| ~ spl175_4 ),
inference(avatar_component_clause,[],[f5445]) ).
fof(f5447,plain,
( ~ spl175_1
| ~ spl175_2
| ~ spl175_3
| spl175_4 ),
inference(avatar_split_clause,[],[f4560,f5445,f5442,f5439,f5436]) ).
fof(f5472,plain,
( v3_struct_0(sK48)
| ~ v10_lattices(sK48)
| ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_1 ),
inference(resolution,[],[f5437,f5403]) ).
fof(f5477,plain,
( ~ v10_lattices(sK48)
| ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_1 ),
inference(forward_subsumption_resolution,[],[f5472,f4552]) ).
fof(f5479,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_1 ),
inference(forward_subsumption_resolution,[],[f5477,f4551]) ).
fof(f5481,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_1 ),
inference(forward_subsumption_resolution,[],[f5479,f4550]) ).
fof(f5489,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_1 ),
inference(forward_subsumption_resolution,[],[f5481,f4555]) ).
fof(f5490,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_1 ),
inference(forward_subsumption_resolution,[],[f5489,f4554]) ).
fof(f5491,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| spl175_1 ),
inference(forward_subsumption_resolution,[],[f5490,f4553]) ).
fof(f5493,definition,
( spl175_9
<=> v12_lattices(sK48) ),
introduced(definition,[new_symbols(definition,[spl175_9])],[avatar_definition]) ).
fof(f5494,plain,
( ~ v12_lattices(sK48)
| spl175_9 ),
inference(avatar_component_clause,[],[f5493]) ).
fof(f5496,definition,
( spl175_10
<=> v16_lattices(sK48) ),
introduced(definition,[new_symbols(definition,[spl175_10])],[avatar_definition]) ).
fof(f5497,plain,
( ~ v16_lattices(sK48)
| spl175_10 ),
inference(avatar_component_clause,[],[f5496]) ).
fof(f5499,definition,
( spl175_11
<=> v15_lattices(sK48) ),
introduced(definition,[new_symbols(definition,[spl175_11])],[avatar_definition]) ).
fof(f5500,plain,
( ~ v15_lattices(sK48)
| spl175_11 ),
inference(avatar_component_clause,[],[f5499]) ).
fof(f5501,plain,
( ~ spl175_9
| ~ spl175_10
| ~ spl175_11
| spl175_1 ),
inference(avatar_split_clause,[],[f5491,f5436,f5499,f5496,f5493]) ).
fof(f5502,plain,
( v3_struct_0(sK48)
| ~ v17_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_11 ),
inference(resolution,[],[f5500,f5015]) ).
fof(f5510,plain,
( ~ v17_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_11 ),
inference(forward_subsumption_resolution,[],[f5502,f4552]) ).
fof(f5514,plain,
( ~ l3_lattices(sK48)
| spl175_11 ),
inference(forward_subsumption_resolution,[],[f5510,f4557]) ).
fof(f5525,plain,
( $false
| spl175_11 ),
inference(forward_subsumption_resolution,[],[f5514,f4550]) ).
fof(f5526,plain,
spl175_11,
inference(avatar_contradiction_clause,[],[f5525]) ).
fof(f5527,plain,
( ~ sP13(sK48)
| spl175_9 ),
inference(resolution,[],[f5494,f5222]) ).
fof(f5529,plain,
( v3_struct_0(sK48)
| ~ v10_lattices(sK48)
| ~ v11_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_9 ),
inference(resolution,[],[f5527,f5231]) ).
fof(f5530,plain,
( ~ v10_lattices(sK48)
| ~ v11_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_9 ),
inference(forward_subsumption_resolution,[],[f5529,f4552]) ).
fof(f5531,plain,
( ~ v11_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_9 ),
inference(forward_subsumption_resolution,[],[f5530,f4551]) ).
fof(f5532,plain,
( ~ v11_lattices(sK48)
| spl175_9 ),
inference(forward_subsumption_resolution,[],[f5531,f4550]) ).
fof(f5546,plain,
( v3_struct_0(sK48)
| ~ v17_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_9 ),
inference(resolution,[],[f5532,f5018]) ).
fof(f5549,plain,
( ~ v17_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_9 ),
inference(forward_subsumption_resolution,[],[f5546,f4552]) ).
fof(f5552,plain,
( ~ l3_lattices(sK48)
| spl175_9 ),
inference(forward_subsumption_resolution,[],[f5549,f4557]) ).
fof(f5556,plain,
( $false
| spl175_9 ),
inference(forward_subsumption_resolution,[],[f5552,f4550]) ).
fof(f5557,plain,
spl175_9,
inference(avatar_contradiction_clause,[],[f5556]) ).
fof(f5559,plain,
( v3_struct_0(sK48)
| ~ v17_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_10 ),
inference(resolution,[],[f5497,f5014]) ).
fof(f5563,plain,
( ~ v17_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_10 ),
inference(forward_subsumption_resolution,[],[f5559,f4552]) ).
fof(f5565,plain,
( ~ l3_lattices(sK48)
| spl175_10 ),
inference(forward_subsumption_resolution,[],[f5563,f4557]) ).
fof(f5568,plain,
( $false
| spl175_10 ),
inference(forward_subsumption_resolution,[],[f5565,f4550]) ).
fof(f5569,plain,
spl175_10,
inference(avatar_contradiction_clause,[],[f5568]) ).
fof(f5571,plain,
( v3_struct_0(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| ~ v11_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| ~ v15_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| ~ v16_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| ~ l3_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| spl175_2 ),
inference(resolution,[],[f5440,f5012]) ).
fof(f5576,definition,
( spl175_14
<=> v11_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50))) ),
introduced(definition,[new_symbols(definition,[spl175_14])],[avatar_definition]) ).
fof(f5577,plain,
( ~ v11_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| spl175_14 ),
inference(avatar_component_clause,[],[f5576]) ).
fof(f5579,definition,
( spl175_15
<=> v16_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50))) ),
introduced(definition,[new_symbols(definition,[spl175_15])],[avatar_definition]) ).
fof(f5580,plain,
( ~ v16_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| spl175_15 ),
inference(avatar_component_clause,[],[f5579]) ).
fof(f5582,definition,
( spl175_16
<=> v15_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50))) ),
introduced(definition,[new_symbols(definition,[spl175_16])],[avatar_definition]) ).
fof(f5583,plain,
( ~ v15_lattices(k23_filter_2(sK48,k22_filter_2(sK48,sK49,sK50)))
| spl175_16 ),
inference(avatar_component_clause,[],[f5582]) ).
fof(f5585,plain,
( ~ spl175_1
| ~ spl175_15
| ~ spl175_16
| ~ spl175_14
| spl175_4
| spl175_2 ),
inference(avatar_split_clause,[],[f5571,f5439,f5445,f5576,f5582,f5579,f5436]) ).
fof(f5586,plain,
( ~ v11_lattices(sK48)
| v1_xboole_0(k22_filter_2(sK48,sK49,sK50))
| ~ m2_lattice4(k22_filter_2(sK48,sK49,sK50),sK48)
| v3_struct_0(sK48)
| ~ v10_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_14 ),
inference(resolution,[],[f5577,f4530]) ).
fof(f5597,plain,
( ~ v11_lattices(sK48)
| v1_xboole_0(k22_filter_2(sK48,sK49,sK50))
| ~ m2_lattice4(k22_filter_2(sK48,sK49,sK50),sK48)
| ~ v10_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_14 ),
inference(forward_subsumption_resolution,[],[f5586,f4552]) ).
fof(f5598,plain,
( ~ v11_lattices(sK48)
| v1_xboole_0(k22_filter_2(sK48,sK49,sK50))
| ~ m2_lattice4(k22_filter_2(sK48,sK49,sK50),sK48)
| ~ l3_lattices(sK48)
| spl175_14 ),
inference(forward_subsumption_resolution,[],[f5597,f4551]) ).
fof(f5599,plain,
( ~ v11_lattices(sK48)
| v1_xboole_0(k22_filter_2(sK48,sK49,sK50))
| ~ m2_lattice4(k22_filter_2(sK48,sK49,sK50),sK48)
| spl175_14 ),
inference(forward_subsumption_resolution,[],[f5598,f4550]) ).
fof(f5601,definition,
( spl175_18
<=> m2_lattice4(k22_filter_2(sK48,sK49,sK50),sK48) ),
introduced(definition,[new_symbols(definition,[spl175_18])],[avatar_definition]) ).
fof(f5602,plain,
( ~ m2_lattice4(k22_filter_2(sK48,sK49,sK50),sK48)
| spl175_18 ),
inference(avatar_component_clause,[],[f5601]) ).
fof(f5604,definition,
( spl175_19
<=> v1_xboole_0(k22_filter_2(sK48,sK49,sK50)) ),
introduced(definition,[new_symbols(definition,[spl175_19])],[avatar_definition]) ).
fof(f5605,plain,
( v1_xboole_0(k22_filter_2(sK48,sK49,sK50))
| ~ spl175_19 ),
inference(avatar_component_clause,[],[f5604]) ).
fof(f5607,definition,
( spl175_20
<=> v11_lattices(sK48) ),
introduced(definition,[new_symbols(definition,[spl175_20])],[avatar_definition]) ).
fof(f5608,plain,
( ~ v11_lattices(sK48)
| spl175_20 ),
inference(avatar_component_clause,[],[f5607]) ).
fof(f5609,plain,
( ~ spl175_18
| spl175_19
| ~ spl175_20
| spl175_14 ),
inference(avatar_split_clause,[],[f5599,f5576,f5607,f5604,f5601]) ).
fof(f5610,plain,
( v3_struct_0(sK48)
| ~ v10_lattices(sK48)
| ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_3 ),
inference(resolution,[],[f5443,f5400]) ).
fof(f5639,plain,
( ~ v10_lattices(sK48)
| ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_3 ),
inference(forward_subsumption_resolution,[],[f5610,f4552]) ).
fof(f5640,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_3 ),
inference(forward_subsumption_resolution,[],[f5639,f4551]) ).
fof(f5641,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_3 ),
inference(forward_subsumption_resolution,[],[f5640,f4550]) ).
fof(f5642,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_3 ),
inference(forward_subsumption_resolution,[],[f5641,f4555]) ).
fof(f5643,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_3 ),
inference(forward_subsumption_resolution,[],[f5642,f4554]) ).
fof(f5644,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| spl175_3 ),
inference(forward_subsumption_resolution,[],[f5643,f4553]) ).
fof(f5645,plain,
( ~ spl175_9
| ~ spl175_10
| ~ spl175_11
| spl175_3 ),
inference(avatar_split_clause,[],[f5644,f5442,f5499,f5496,f5493]) ).
fof(f5648,plain,
( v3_struct_0(sK48)
| ~ v17_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_20 ),
inference(resolution,[],[f5608,f5018]) ).
fof(f5651,plain,
( ~ v17_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_20 ),
inference(forward_subsumption_resolution,[],[f5648,f4552]) ).
fof(f5654,plain,
( ~ l3_lattices(sK48)
| spl175_20 ),
inference(forward_subsumption_resolution,[],[f5651,f4557]) ).
fof(f5658,plain,
( $false
| spl175_20 ),
inference(forward_subsumption_resolution,[],[f5654,f4550]) ).
fof(f5659,plain,
spl175_20,
inference(avatar_contradiction_clause,[],[f5658]) ).
fof(f5676,plain,
( v3_struct_0(sK48)
| ~ v10_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| spl175_18 ),
inference(resolution,[],[f5602,f4227]) ).
fof(f5681,plain,
( ~ v10_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| spl175_18 ),
inference(forward_subsumption_resolution,[],[f5676,f4552]) ).
fof(f5683,plain,
( ~ l3_lattices(sK48)
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| spl175_18 ),
inference(forward_subsumption_resolution,[],[f5681,f4551]) ).
fof(f5685,plain,
( ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| spl175_18 ),
inference(forward_subsumption_resolution,[],[f5683,f4550]) ).
fof(f5686,plain,
( ~ m1_subset_1(sK50,u1_struct_0(sK48))
| spl175_18 ),
inference(forward_subsumption_resolution,[],[f5685,f4553]) ).
fof(f5687,plain,
( $false
| spl175_18 ),
inference(forward_subsumption_resolution,[],[f5686,f4554]) ).
fof(f5688,plain,
spl175_18,
inference(avatar_contradiction_clause,[],[f5687]) ).
fof(f5689,plain,
( v3_struct_0(sK48)
| ~ v10_lattices(sK48)
| ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_15 ),
inference(resolution,[],[f5580,f5402]) ).
fof(f5695,plain,
( ~ v10_lattices(sK48)
| ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_15 ),
inference(forward_subsumption_resolution,[],[f5689,f4552]) ).
fof(f5696,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_15 ),
inference(forward_subsumption_resolution,[],[f5695,f4551]) ).
fof(f5697,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_15 ),
inference(forward_subsumption_resolution,[],[f5696,f4550]) ).
fof(f5698,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_15 ),
inference(forward_subsumption_resolution,[],[f5697,f4555]) ).
fof(f5699,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| spl175_15 ),
inference(forward_subsumption_resolution,[],[f5698,f4554]) ).
fof(f5700,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| spl175_15 ),
inference(forward_subsumption_resolution,[],[f5699,f4553]) ).
fof(f5701,plain,
( ~ spl175_9
| ~ spl175_10
| ~ spl175_11
| spl175_15 ),
inference(avatar_split_clause,[],[f5700,f5579,f5499,f5496,f5493]) ).
fof(f5703,plain,
( ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| v3_struct_0(sK48)
| ~ v10_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_16 ),
inference(resolution,[],[f5583,f4539]) ).
fof(f5719,plain,
( ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| v3_struct_0(sK48)
| ~ v10_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_16 ),
inference(forward_subsumption_resolution,[],[f5703,f4555]) ).
fof(f5721,plain,
( ~ m1_subset_1(sK49,u1_struct_0(sK48))
| v3_struct_0(sK48)
| ~ v10_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_16 ),
inference(forward_subsumption_resolution,[],[f5719,f4554]) ).
fof(f5723,plain,
( v3_struct_0(sK48)
| ~ v10_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_16 ),
inference(forward_subsumption_resolution,[],[f5721,f4553]) ).
fof(f5725,plain,
( ~ v10_lattices(sK48)
| ~ l3_lattices(sK48)
| spl175_16 ),
inference(forward_subsumption_resolution,[],[f5723,f4552]) ).
fof(f5727,plain,
( ~ l3_lattices(sK48)
| spl175_16 ),
inference(forward_subsumption_resolution,[],[f5725,f4551]) ).
fof(f5729,plain,
( $false
| spl175_16 ),
inference(forward_subsumption_resolution,[],[f5727,f4550]) ).
fof(f5730,plain,
spl175_16,
inference(avatar_contradiction_clause,[],[f5729]) ).
fof(f5733,plain,
( v3_struct_0(sK48)
| ~ v10_lattices(sK48)
| ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ spl175_4 ),
inference(resolution,[],[f5446,f5399]) ).
fof(f5737,plain,
( ~ v10_lattices(sK48)
| ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ spl175_4 ),
inference(forward_subsumption_resolution,[],[f5733,f4552]) ).
fof(f5738,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ spl175_4 ),
inference(forward_subsumption_resolution,[],[f5737,f4551]) ).
fof(f5739,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ r3_lattices(sK48,sK49,sK50)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ spl175_4 ),
inference(forward_subsumption_resolution,[],[f5738,f4550]) ).
fof(f5740,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ spl175_4 ),
inference(forward_subsumption_resolution,[],[f5739,f4555]) ).
fof(f5741,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ spl175_4 ),
inference(forward_subsumption_resolution,[],[f5740,f4554]) ).
fof(f5742,plain,
( ~ v15_lattices(sK48)
| ~ v16_lattices(sK48)
| ~ v12_lattices(sK48)
| ~ spl175_4 ),
inference(forward_subsumption_resolution,[],[f5741,f4553]) ).
fof(f5743,plain,
( ~ spl175_9
| ~ spl175_10
| ~ spl175_11
| ~ spl175_4 ),
inference(avatar_split_clause,[],[f5742,f5445,f5499,f5496,f5493]) ).
fof(f5744,plain,
( v3_struct_0(sK48)
| ~ v10_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ spl175_19 ),
inference(resolution,[],[f5605,f4228]) ).
fof(f5745,plain,
( ~ v10_lattices(sK48)
| ~ l3_lattices(sK48)
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ spl175_19 ),
inference(forward_subsumption_resolution,[],[f5744,f4552]) ).
fof(f5746,plain,
( ~ l3_lattices(sK48)
| ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ spl175_19 ),
inference(forward_subsumption_resolution,[],[f5745,f4551]) ).
fof(f5747,plain,
( ~ m1_subset_1(sK49,u1_struct_0(sK48))
| ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ spl175_19 ),
inference(forward_subsumption_resolution,[],[f5746,f4550]) ).
fof(f5748,plain,
( ~ m1_subset_1(sK50,u1_struct_0(sK48))
| ~ spl175_19 ),
inference(forward_subsumption_resolution,[],[f5747,f4553]) ).
fof(f5749,plain,
( $false
| ~ spl175_19 ),
inference(forward_subsumption_resolution,[],[f5748,f4554]) ).
fof(f5750,plain,
~ spl175_19,
inference(avatar_contradiction_clause,[],[f5749]) ).
cnf(s1,plain,
( ~ spl175_1
| ~ spl175_2
| ~ spl175_3
| spl175_4 ),
inference(sat_conversion,[],[f5447]) ).
cnf(s4,plain,
( spl175_1
| ~ spl175_9
| ~ spl175_10
| ~ spl175_11 ),
inference(sat_conversion,[],[f5501]) ).
cnf(s8,plain,
spl175_11,
inference(sat_conversion,[],[f5526]) ).
cnf(s10,plain,
spl175_9,
inference(sat_conversion,[],[f5557]) ).
cnf(s12,plain,
spl175_10,
inference(sat_conversion,[],[f5569]) ).
cnf(s14,plain,
( ~ spl175_1
| spl175_2
| spl175_4
| ~ spl175_14
| ~ spl175_15
| ~ spl175_16 ),
inference(sat_conversion,[],[f5585]) ).
cnf(s16,plain,
( spl175_14
| ~ spl175_18
| spl175_19
| ~ spl175_20 ),
inference(sat_conversion,[],[f5609]) ).
cnf(s19,plain,
( spl175_3
| ~ spl175_9
| ~ spl175_10
| ~ spl175_11 ),
inference(sat_conversion,[],[f5645]) ).
cnf(s21,plain,
spl175_20,
inference(sat_conversion,[],[f5659]) ).
cnf(s22,plain,
spl175_18,
inference(sat_conversion,[],[f5688]) ).
cnf(s23,plain,
( ~ spl175_9
| ~ spl175_10
| ~ spl175_11
| spl175_15 ),
inference(sat_conversion,[],[f5701]) ).
cnf(s26,plain,
spl175_16,
inference(sat_conversion,[],[f5730]) ).
cnf(s28,plain,
( ~ spl175_4
| ~ spl175_9
| ~ spl175_10
| ~ spl175_11 ),
inference(sat_conversion,[],[f5743]) ).
cnf(s29,plain,
~ spl175_19,
inference(sat_conversion,[],[f5750]) ).
cnf(s30,plain,
spl175_14,
inference(rat,[],[s16,s21,s29,s22]) ).
cnf(s31,plain,
( ~ spl175_1
| spl175_2
| spl175_4
| ~ spl175_15 ),
inference(rat,[],[s14,s26,s30]) ).
cnf(s33,plain,
spl175_15,
inference(rat,[],[s23,s10,s12,s8]) ).
cnf(s34,plain,
~ spl175_4,
inference(rat,[],[s28,s10,s12,s8]) ).
cnf(s35,plain,
spl175_3,
inference(rat,[],[s19,s10,s12,s8]) ).
cnf(s36,plain,
spl175_1,
inference(rat,[],[s4,s8,s12,s10]) ).
cnf(s37,plain,
spl175_2,
inference(rat,[],[s31,s33,s34,s36]) ).
cnf(s38,plain,
$false,
inference(rat,[],[s1,s34,s35,s37,s36]) ).
fof(f5751,plain,
$false,
inference(avatar_sat_refutation,[],[s38]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT337+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 % Computer : n007.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 14:44:40 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 Running first-order theorem proving
% 0.11/0.39 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.11/2.13 % (1498327)Detected formulas, will run a generic FOF schedule.
% 8.11/2.13 % (1498335)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4123204100:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 8.11/2.13 % (1498335)Refutation not found, incomplete strategy
% 8.11/2.13 % (1498335)------------------------------
% 8.11/2.13 % (1498335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.13 % (1498335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.13 % (1498335)CaDiCaL version: 2.1.3
% 8.11/2.13 % (1498335)Termination reason: Refutation not found, incomplete strategy
% 8.11/2.13 % (1498335)Time elapsed: 0.008 s
% 8.11/2.13 % (1498335)Peak memory usage: 92 MB
% 8.11/2.13 % (1498335)Instructions burned: 17 (million)
% 8.11/2.13 % (1498333)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=1742953052:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 8.11/2.13 % (1498334)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=4133822058:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 8.11/2.13 % (1498337)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=226845424:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 8.11/2.13 % (1498336)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2595604962:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 8.11/2.13 % (1498332)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=2724692871:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 8.11/2.13 % (1498338)dis-21_1_sil=8000:lcm=predicate:random_seed=3428593903: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)
% 8.11/2.13 % (1498338)Instruction limit reached!
% 8.11/2.13 % (1498338)------------------------------
% 8.11/2.13 % (1498338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.13 % (1498338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.13 % (1498338)CaDiCaL version: 2.1.3
% 8.11/2.13 % (1498338)Termination reason: Instruction limit
% 8.11/2.13 % (1498338)Termination phase: Property scanning
% 8.11/2.13 % (1498338)Time elapsed: 0.078 s
% 8.11/2.13 % (1498338)Peak memory usage: 92 MB
% 8.11/2.13 % (1498338)Instructions burned: 129 (million)
% 8.11/2.13 % (1498336)Instruction limit reached!
% 8.11/2.13 % (1498336)------------------------------
% 8.11/2.13 % (1498336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.13 % (1498336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.13 % (1498336)CaDiCaL version: 2.1.3
% 8.11/2.13 % (1498336)Termination reason: Instruction limit
% 8.11/2.13 % (1498336)Termination phase: Saturation
% 8.11/2.13 % (1498336)Time elapsed: 0.078 s
% 8.11/2.13 % (1498336)Peak memory usage: 92 MB
% 8.11/2.13 % (1498336)Instructions burned: 121 (million)
% 8.11/2.13 % (1498337)Instruction limit reached!
% 8.11/2.13 % (1498337)------------------------------
% 8.11/2.13 % (1498337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.13 % (1498337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.13 % (1498337)CaDiCaL version: 2.1.3
% 8.11/2.13 % (1498337)Termination reason: Instruction limit
% 8.11/2.13 % (1498337)Termination phase: Clausification
% 8.11/2.13 % (1498337)Time elapsed: 0.087 s
% 8.11/2.13 % (1498337)Peak memory usage: 94 MB
% 8.11/2.13 % (1498337)Instructions burned: 140 (million)
% 8.11/2.13 % (1498335)------------------------------
% 8.11/2.13 % (1498335)------------------------------
% 8.11/2.13 % (1498347)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3394587832:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 8.11/2.13 % (1498346)lrs+10_1_sil=8000:sp=occurrence:random_seed=360865462:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 8.11/2.13 % (1498349)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=4028840623:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 8.11/2.13 % (1498348)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1740435479:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 8.11/2.13 % (1498347)Refutation not found, incomplete strategy
% 8.11/2.13 % (1498347)------------------------------
% 8.11/2.13 % (1498347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.13 % (1498347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.13 % (1498347)CaDiCaL version: 2.1.3
% 8.11/2.13 % (1498347)Termination reason: Refutation not found, incomplete strategy
% 8.11/2.13 % (1498347)Time elapsed: 0.044 s
% 8.11/2.13 % (1498347)Peak memory usage: 92 MB
% 8.11/2.13 % (1498347)Instructions burned: 80 (million)
% 8.11/2.13 % (1498349)Instruction limit reached!
% 8.11/2.13 % (1498349)------------------------------
% 8.11/2.13 % (1498349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.13 % (1498349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.13 % (1498349)CaDiCaL version: 2.1.3
% 8.11/2.13 % (1498349)Termination reason: Instruction limit
% 8.11/2.13 % (1498349)Termination phase: Saturation
% 8.11/2.13 % (1498349)Time elapsed: 0.074 s
% 8.11/2.13 % (1498349)Peak memory usage: 97 MB
% 8.11/2.13 % (1498349)Instructions burned: 250 (million)
% 8.11/2.13 % (1498348)Instruction limit reached!
% 8.11/2.13 % (1498348)------------------------------
% 8.11/2.13 % (1498348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.13 % (1498348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.13 % (1498348)CaDiCaL version: 2.1.3
% 8.11/2.13 % (1498348)Termination reason: Instruction limit
% 8.11/2.13 % (1498348)Termination phase: Saturation
% 8.11/2.13 % (1498348)Time elapsed: 0.157 s
% 8.11/2.13 % (1498348)Peak memory usage: 94 MB
% 8.11/2.13 % (1498348)Instructions burned: 326 (million)
% 8.11/2.13 % (1498346)Instruction limit reached!
% 8.11/2.13 % (1498346)------------------------------
% 8.11/2.13 % (1498346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.13 % (1498346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.13 % (1498346)CaDiCaL version: 2.1.3
% 8.11/2.13 % (1498346)Termination reason: Instruction limit
% 8.11/2.13 % (1498346)Termination phase: Saturation
% 8.11/2.13 % (1498346)Time elapsed: 0.174 s
% 8.11/2.13 % (1498346)Peak memory usage: 95 MB
% 8.11/2.13 % (1498346)Instructions burned: 286 (million)
% 8.11/2.13 % (1498354)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3951096403:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 8.11/2.13 % (1498347)------------------------------
% 8.11/2.13 % (1498347)------------------------------
% 8.11/2.13 % (1498354)Instruction limit reached!
% 8.11/2.13 % (1498354)------------------------------
% 8.11/2.13 % (1498354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.13 % (1498354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.13 % (1498354)CaDiCaL version: 2.1.3
% 8.11/2.13 % (1498354)Termination reason: Instruction limit
% 8.11/2.13 % (1498354)Termination phase: Saturation
% 8.11/2.13 % (1498354)Time elapsed: 0.088 s
% 8.11/2.13 % (1498354)Peak memory usage: 94 MB
% 8.11/2.13 % (1498354)Instructions burned: 295 (million)
% 8.11/2.13 % (1498356)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2762838018:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 8.11/2.13 % (1498355)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2022134095:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 8.11/2.13 % (1498356)Instruction limit reached!
% 8.11/2.13 % (1498356)------------------------------
% 8.11/2.13 % (1498356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.13 % (1498356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.13 % (1498356)CaDiCaL version: 2.1.3
% 8.11/2.13 % (1498356)Termination reason: Instruction limit
% 8.11/2.13 % (1498356)Termination phase: Saturation
% 8.11/2.13 % (1498356)Time elapsed: 0.065 s
% 8.11/2.13 % (1498356)Peak memory usage: 93 MB
% 8.11/2.13 % (1498356)Instructions burned: 113 (million)
% 8.11/2.13 % (1498389)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2627358524:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 8.11/2.13 % (1498381)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=782413615:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 8.11/2.13 % (1498389)Instruction limit reached!
% 8.11/2.13 % (1498389)------------------------------
% 8.11/2.13 % (1498389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.13 % (1498389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.13 % (1498389)CaDiCaL version: 2.1.3
% 8.11/2.13 % (1498389)Termination reason: Instruction limit
% 8.11/2.13 % (1498389)Termination phase: Property scanning
% 8.11/2.13 % (1498389)Time elapsed: 0.032 s
% 8.11/2.13 % (1498389)Peak memory usage: 91 MB
% 8.11/2.13 % (1498389)Instructions burned: 115 (million)
% 8.11/2.13 % (1498381)Instruction limit reached!
% 8.11/2.13 % (1498381)------------------------------
% 8.11/2.13 % (1498381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.13 % (1498381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.13 % (1498381)CaDiCaL version: 2.1.3
% 8.11/2.13 % (1498381)Termination reason: Instruction limit
% 8.11/2.13 % (1498381)Termination phase: Property scanning
% 8.11/2.13 % (1498381)Time elapsed: 0.078 s
% 8.11/2.13 % (1498381)Peak memory usage: 94 MB
% 8.11/2.13 % (1498381)Instructions burned: 129 (million)
% 8.11/2.13 % (1498428)lrs+10_1_sil=8000:sp=occurrence:random_seed=2812186286:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 8.11/2.13 % (1498451)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2205713531:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 8.11/2.13 % (1498451)First to succeed.
% 8.11/2.13 % (1498451)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1498327"
% 8.11/2.13 % (1498471)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1985360232:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 8.11/2.13 % (1498451)Refutation found. Thanks to Tanya!
% 8.11/2.13 % SZS status Theorem for theBenchmark
% 8.11/2.13 % SZS output start Proof for theBenchmark
% See solution above
% 8.90/2.26 % (1498451)------------------------------
% 8.90/2.26 % (1498451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.26 % (1498451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.26 % (1498451)CaDiCaL version: 2.1.3
% 8.90/2.26 % (1498451)Termination reason: Refutation
% 8.90/2.26 % (1498451)Time elapsed: 0.037 s
% 8.90/2.26 % (1498451)Peak memory usage: 95 MB
% 8.90/2.26 % (1498451)Instructions burned: 112 (million)
% 8.90/2.26 % (1498451)------------------------------
% 8.90/2.26 % (1498451)------------------------------
% 8.90/2.26 % (1498327)Success in time 1.283 s
% 8.90/2.26 % Vampire exiting
%------------------------------------------------------------------------------