%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT337+4 : 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 : 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 18.16s 5.70s
% Output : Refutation 18.92s
% 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(f18128,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(f18129,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(f18131,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/sandbox2/benchmark/theBenchmark.p',cc7_lattices) ).
fof(f34646,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/sandbox2/benchmark/theBenchmark.p',dt_k22_filter_2) ).
fof(f34751,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/sandbox2/benchmark/theBenchmark.p',t78_filter_2) ).
fof(f34757,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/sandbox2/benchmark/theBenchmark.p',t84_filter_2) ).
fof(f34759,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/sandbox2/benchmark/theBenchmark.p',t86_filter_2) ).
fof(f34760,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/sandbox2/benchmark/theBenchmark.p',t87_filter_2) ).
fof(f34761,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)],[f34760]) ).
fof(f34875,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,[],[f34646]) ).
fof(f34876,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,[],[f34875]) ).
fof(f35082,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,[],[f34751]) ).
fof(f35083,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,[],[f35082]) ).
fof(f35094,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,[],[f34757]) ).
fof(f35095,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,[],[f35094]) ).
fof(f35098,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,[],[f34759]) ).
fof(f35099,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,[],[f35098]) ).
fof(f35100,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,[],[f34761]) ).
fof(f35101,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,[],[f35100]) ).
fof(f35487,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,[],[f18129]) ).
fof(f35488,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,[],[f35487]) ).
fof(f35489,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,[],[f18128]) ).
fof(f35490,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,[],[f35489]) ).
fof(f35646,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,[],[f18131]) ).
fof(f35647,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,[],[f35646]) ).
fof(f35711,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) )
| ~ sP21(X0) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f35712,plain,
! [X0] :
( sP21(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f35647,f35711]) ).
fof(f35796,plain,
( ( v3_struct_0(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| ~ v10_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| ~ v17_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| ~ l3_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58))) )
& ~ v3_struct_0(sK56)
& v10_lattices(sK56)
& v17_lattices(sK56)
& l3_lattices(sK56)
& r3_lattices(sK56,sK57,sK58)
& m1_subset_1(sK58,u1_struct_0(sK56))
& m1_subset_1(sK57,u1_struct_0(sK56))
& ~ v3_struct_0(sK56)
& v10_lattices(sK56)
& l3_lattices(sK56) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56,sK57,sK58]),skolemize(X0,sK56),skolemize(X1,sK57),skolemize(X2,sK58)],[f35101]) ).
fof(f36053,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) )
| ~ sP21(X0) ),
inference(nnf_transformation,[],[f35711]) ).
fof(f36111,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,[],[f34876]) ).
fof(f36112,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,[],[f34876]) ).
fof(f36414,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,[],[f35083]) ).
fof(f36423,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,[],[f35095]) ).
fof(f36429,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,[],[f35099]) ).
fof(f36430,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,[],[f35099]) ).
fof(f36432,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,[],[f35099]) ).
fof(f36433,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,[],[f35099]) ).
fof(f36434,plain,
l3_lattices(sK56),
inference(cnf_transformation,[],[f35796]) ).
fof(f36435,plain,
v10_lattices(sK56),
inference(cnf_transformation,[],[f35796]) ).
fof(f36436,plain,
~ v3_struct_0(sK56),
inference(cnf_transformation,[],[f35796]) ).
fof(f36437,plain,
m1_subset_1(sK57,u1_struct_0(sK56)),
inference(cnf_transformation,[],[f35796]) ).
fof(f36438,plain,
m1_subset_1(sK58,u1_struct_0(sK56)),
inference(cnf_transformation,[],[f35796]) ).
fof(f36439,plain,
r3_lattices(sK56,sK57,sK58),
inference(cnf_transformation,[],[f35796]) ).
fof(f36441,plain,
v17_lattices(sK56),
inference(cnf_transformation,[],[f35796]) ).
fof(f36444,plain,
( v3_struct_0(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| ~ v10_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| ~ v17_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| ~ l3_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58))) ),
inference(cnf_transformation,[],[f35796]) ).
fof(f36974,plain,
! [X0] :
( v17_lattices(X0)
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35488]) ).
fof(f36976,plain,
! [X0] :
( v16_lattices(X0)
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35490]) ).
fof(f36977,plain,
! [X0] :
( v15_lattices(X0)
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35490]) ).
fof(f36980,plain,
! [X0] :
( v11_lattices(X0)
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35490]) ).
fof(f37310,plain,
! [X0] :
( v12_lattices(X0)
| ~ sP21(X0) ),
inference(cnf_transformation,[],[f36053]) ).
fof(f37319,plain,
! [X0] :
( sP21(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35712]) ).
fof(f37504,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,[],[f36433]) ).
fof(f37505,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,[],[f36432]) ).
fof(f37507,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,[],[f36430]) ).
fof(f37508,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,[],[f36429]) ).
fof(f37544,definition,
( spl196_1
<=> l3_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58))) ),
introduced(definition,[new_symbols(definition,[spl196_1])],[avatar_definition]) ).
fof(f37545,plain,
( ~ l3_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| spl196_1 ),
inference(avatar_component_clause,[],[f37544]) ).
fof(f37547,definition,
( spl196_2
<=> v17_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58))) ),
introduced(definition,[new_symbols(definition,[spl196_2])],[avatar_definition]) ).
fof(f37548,plain,
( ~ v17_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| spl196_2 ),
inference(avatar_component_clause,[],[f37547]) ).
fof(f37550,definition,
( spl196_3
<=> v10_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58))) ),
introduced(definition,[new_symbols(definition,[spl196_3])],[avatar_definition]) ).
fof(f37551,plain,
( ~ v10_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| spl196_3 ),
inference(avatar_component_clause,[],[f37550]) ).
fof(f37553,definition,
( spl196_4
<=> v3_struct_0(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58))) ),
introduced(definition,[new_symbols(definition,[spl196_4])],[avatar_definition]) ).
fof(f37554,plain,
( v3_struct_0(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| ~ spl196_4 ),
inference(avatar_component_clause,[],[f37553]) ).
fof(f37555,plain,
( ~ spl196_1
| ~ spl196_2
| ~ spl196_3
| spl196_4 ),
inference(avatar_split_clause,[],[f36444,f37553,f37550,f37547,f37544]) ).
fof(f37580,plain,
( v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_1 ),
inference(resolution,[],[f37545,f37508]) ).
fof(f37585,plain,
( ~ v10_lattices(sK56)
| ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_1 ),
inference(forward_subsumption_resolution,[],[f37580,f36436]) ).
fof(f37587,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_1 ),
inference(forward_subsumption_resolution,[],[f37585,f36435]) ).
fof(f37589,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_1 ),
inference(forward_subsumption_resolution,[],[f37587,f36434]) ).
fof(f37597,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_1 ),
inference(forward_subsumption_resolution,[],[f37589,f36439]) ).
fof(f37598,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_1 ),
inference(forward_subsumption_resolution,[],[f37597,f36438]) ).
fof(f37599,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| spl196_1 ),
inference(forward_subsumption_resolution,[],[f37598,f36437]) ).
fof(f37601,definition,
( spl196_9
<=> v12_lattices(sK56) ),
introduced(definition,[new_symbols(definition,[spl196_9])],[avatar_definition]) ).
fof(f37602,plain,
( ~ v12_lattices(sK56)
| spl196_9 ),
inference(avatar_component_clause,[],[f37601]) ).
fof(f37604,definition,
( spl196_10
<=> v16_lattices(sK56) ),
introduced(definition,[new_symbols(definition,[spl196_10])],[avatar_definition]) ).
fof(f37605,plain,
( ~ v16_lattices(sK56)
| spl196_10 ),
inference(avatar_component_clause,[],[f37604]) ).
fof(f37607,definition,
( spl196_11
<=> v15_lattices(sK56) ),
introduced(definition,[new_symbols(definition,[spl196_11])],[avatar_definition]) ).
fof(f37608,plain,
( ~ v15_lattices(sK56)
| spl196_11 ),
inference(avatar_component_clause,[],[f37607]) ).
fof(f37609,plain,
( ~ spl196_9
| ~ spl196_10
| ~ spl196_11
| spl196_1 ),
inference(avatar_split_clause,[],[f37599,f37544,f37607,f37604,f37601]) ).
fof(f37610,plain,
( v3_struct_0(sK56)
| ~ v17_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_11 ),
inference(resolution,[],[f37608,f36977]) ).
fof(f37619,plain,
( ~ v17_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_11 ),
inference(forward_subsumption_resolution,[],[f37610,f36436]) ).
fof(f37623,plain,
( ~ l3_lattices(sK56)
| spl196_11 ),
inference(forward_subsumption_resolution,[],[f37619,f36441]) ).
fof(f37634,plain,
( $false
| spl196_11 ),
inference(forward_subsumption_resolution,[],[f37623,f36434]) ).
fof(f37635,plain,
spl196_11,
inference(avatar_contradiction_clause,[],[f37634]) ).
fof(f37636,plain,
( ~ sP21(sK56)
| spl196_9 ),
inference(resolution,[],[f37602,f37310]) ).
fof(f37639,plain,
( v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ v11_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_9 ),
inference(resolution,[],[f37636,f37319]) ).
fof(f37640,plain,
( ~ v10_lattices(sK56)
| ~ v11_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_9 ),
inference(forward_subsumption_resolution,[],[f37639,f36436]) ).
fof(f37641,plain,
( ~ v11_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_9 ),
inference(forward_subsumption_resolution,[],[f37640,f36435]) ).
fof(f37642,plain,
( ~ v11_lattices(sK56)
| spl196_9 ),
inference(forward_subsumption_resolution,[],[f37641,f36434]) ).
fof(f37714,plain,
( v3_struct_0(sK56)
| ~ v17_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_9 ),
inference(resolution,[],[f37642,f36980]) ).
fof(f37717,plain,
( ~ v17_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_9 ),
inference(forward_subsumption_resolution,[],[f37714,f36436]) ).
fof(f37720,plain,
( ~ l3_lattices(sK56)
| spl196_9 ),
inference(forward_subsumption_resolution,[],[f37717,f36441]) ).
fof(f37724,plain,
( $false
| spl196_9 ),
inference(forward_subsumption_resolution,[],[f37720,f36434]) ).
fof(f37725,plain,
spl196_9,
inference(avatar_contradiction_clause,[],[f37724]) ).
fof(f37727,plain,
( v3_struct_0(sK56)
| ~ v17_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_10 ),
inference(resolution,[],[f37605,f36976]) ).
fof(f37731,plain,
( ~ v17_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_10 ),
inference(forward_subsumption_resolution,[],[f37727,f36436]) ).
fof(f37733,plain,
( ~ l3_lattices(sK56)
| spl196_10 ),
inference(forward_subsumption_resolution,[],[f37731,f36441]) ).
fof(f37736,plain,
( $false
| spl196_10 ),
inference(forward_subsumption_resolution,[],[f37733,f36434]) ).
fof(f37737,plain,
spl196_10,
inference(avatar_contradiction_clause,[],[f37736]) ).
fof(f37739,plain,
( v3_struct_0(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| ~ v11_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| ~ v15_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| ~ v16_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| ~ l3_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| spl196_2 ),
inference(resolution,[],[f37548,f36974]) ).
fof(f37744,definition,
( spl196_15
<=> v11_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58))) ),
introduced(definition,[new_symbols(definition,[spl196_15])],[avatar_definition]) ).
fof(f37745,plain,
( ~ v11_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| spl196_15 ),
inference(avatar_component_clause,[],[f37744]) ).
fof(f37747,definition,
( spl196_16
<=> v16_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58))) ),
introduced(definition,[new_symbols(definition,[spl196_16])],[avatar_definition]) ).
fof(f37748,plain,
( ~ v16_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| spl196_16 ),
inference(avatar_component_clause,[],[f37747]) ).
fof(f37750,definition,
( spl196_17
<=> v15_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58))) ),
introduced(definition,[new_symbols(definition,[spl196_17])],[avatar_definition]) ).
fof(f37751,plain,
( ~ v15_lattices(k23_filter_2(sK56,k22_filter_2(sK56,sK57,sK58)))
| spl196_17 ),
inference(avatar_component_clause,[],[f37750]) ).
fof(f37753,plain,
( ~ spl196_1
| ~ spl196_16
| ~ spl196_17
| ~ spl196_15
| spl196_4
| spl196_2 ),
inference(avatar_split_clause,[],[f37739,f37547,f37553,f37744,f37750,f37747,f37544]) ).
fof(f37755,plain,
( ~ v11_lattices(sK56)
| v1_xboole_0(k22_filter_2(sK56,sK57,sK58))
| ~ m2_lattice4(k22_filter_2(sK56,sK57,sK58),sK56)
| v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_15 ),
inference(resolution,[],[f37745,f36414]) ).
fof(f37767,plain,
( ~ v11_lattices(sK56)
| v1_xboole_0(k22_filter_2(sK56,sK57,sK58))
| ~ m2_lattice4(k22_filter_2(sK56,sK57,sK58),sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_15 ),
inference(forward_subsumption_resolution,[],[f37755,f36436]) ).
fof(f37768,plain,
( ~ v11_lattices(sK56)
| v1_xboole_0(k22_filter_2(sK56,sK57,sK58))
| ~ m2_lattice4(k22_filter_2(sK56,sK57,sK58),sK56)
| ~ l3_lattices(sK56)
| spl196_15 ),
inference(forward_subsumption_resolution,[],[f37767,f36435]) ).
fof(f37769,plain,
( ~ v11_lattices(sK56)
| v1_xboole_0(k22_filter_2(sK56,sK57,sK58))
| ~ m2_lattice4(k22_filter_2(sK56,sK57,sK58),sK56)
| spl196_15 ),
inference(forward_subsumption_resolution,[],[f37768,f36434]) ).
fof(f37771,definition,
( spl196_19
<=> m2_lattice4(k22_filter_2(sK56,sK57,sK58),sK56) ),
introduced(definition,[new_symbols(definition,[spl196_19])],[avatar_definition]) ).
fof(f37772,plain,
( ~ m2_lattice4(k22_filter_2(sK56,sK57,sK58),sK56)
| spl196_19 ),
inference(avatar_component_clause,[],[f37771]) ).
fof(f37774,definition,
( spl196_20
<=> v1_xboole_0(k22_filter_2(sK56,sK57,sK58)) ),
introduced(definition,[new_symbols(definition,[spl196_20])],[avatar_definition]) ).
fof(f37775,plain,
( v1_xboole_0(k22_filter_2(sK56,sK57,sK58))
| ~ spl196_20 ),
inference(avatar_component_clause,[],[f37774]) ).
fof(f37777,definition,
( spl196_21
<=> v11_lattices(sK56) ),
introduced(definition,[new_symbols(definition,[spl196_21])],[avatar_definition]) ).
fof(f37778,plain,
( ~ v11_lattices(sK56)
| spl196_21 ),
inference(avatar_component_clause,[],[f37777]) ).
fof(f37779,plain,
( ~ spl196_19
| spl196_20
| ~ spl196_21
| spl196_15 ),
inference(avatar_split_clause,[],[f37769,f37744,f37777,f37774,f37771]) ).
fof(f37783,plain,
( v3_struct_0(sK56)
| ~ v17_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_21 ),
inference(resolution,[],[f37778,f36980]) ).
fof(f37786,plain,
( ~ v17_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_21 ),
inference(forward_subsumption_resolution,[],[f37783,f36436]) ).
fof(f37789,plain,
( ~ l3_lattices(sK56)
| spl196_21 ),
inference(forward_subsumption_resolution,[],[f37786,f36441]) ).
fof(f37793,plain,
( $false
| spl196_21 ),
inference(forward_subsumption_resolution,[],[f37789,f36434]) ).
fof(f37794,plain,
spl196_21,
inference(avatar_contradiction_clause,[],[f37793]) ).
fof(f37796,plain,
( v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_3 ),
inference(resolution,[],[f37551,f37505]) ).
fof(f37830,plain,
( ~ v10_lattices(sK56)
| ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_3 ),
inference(forward_subsumption_resolution,[],[f37796,f36436]) ).
fof(f37831,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_3 ),
inference(forward_subsumption_resolution,[],[f37830,f36435]) ).
fof(f37832,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_3 ),
inference(forward_subsumption_resolution,[],[f37831,f36434]) ).
fof(f37833,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_3 ),
inference(forward_subsumption_resolution,[],[f37832,f36439]) ).
fof(f37834,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_3 ),
inference(forward_subsumption_resolution,[],[f37833,f36438]) ).
fof(f37835,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| spl196_3 ),
inference(forward_subsumption_resolution,[],[f37834,f36437]) ).
fof(f37836,plain,
( ~ spl196_9
| ~ spl196_10
| ~ spl196_11
| spl196_3 ),
inference(avatar_split_clause,[],[f37835,f37550,f37607,f37604,f37601]) ).
fof(f37846,plain,
( v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| spl196_19 ),
inference(resolution,[],[f37772,f36111]) ).
fof(f37851,plain,
( ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| spl196_19 ),
inference(forward_subsumption_resolution,[],[f37846,f36436]) ).
fof(f37853,plain,
( ~ l3_lattices(sK56)
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| spl196_19 ),
inference(forward_subsumption_resolution,[],[f37851,f36435]) ).
fof(f37855,plain,
( ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| spl196_19 ),
inference(forward_subsumption_resolution,[],[f37853,f36434]) ).
fof(f37856,plain,
( ~ m1_subset_1(sK58,u1_struct_0(sK56))
| spl196_19 ),
inference(forward_subsumption_resolution,[],[f37855,f36437]) ).
fof(f37857,plain,
( $false
| spl196_19 ),
inference(forward_subsumption_resolution,[],[f37856,f36438]) ).
fof(f37858,plain,
spl196_19,
inference(avatar_contradiction_clause,[],[f37857]) ).
fof(f38068,plain,
( v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ spl196_20 ),
inference(resolution,[],[f37775,f36112]) ).
fof(f38069,plain,
( ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ spl196_20 ),
inference(forward_subsumption_resolution,[],[f38068,f36436]) ).
fof(f38070,plain,
( ~ l3_lattices(sK56)
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ spl196_20 ),
inference(forward_subsumption_resolution,[],[f38069,f36435]) ).
fof(f38071,plain,
( ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ spl196_20 ),
inference(forward_subsumption_resolution,[],[f38070,f36434]) ).
fof(f38072,plain,
( ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ spl196_20 ),
inference(forward_subsumption_resolution,[],[f38071,f36437]) ).
fof(f38073,plain,
( $false
| ~ spl196_20 ),
inference(forward_subsumption_resolution,[],[f38072,f36438]) ).
fof(f38074,plain,
~ spl196_20,
inference(avatar_contradiction_clause,[],[f38073]) ).
fof(f38075,plain,
( v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_16 ),
inference(resolution,[],[f37748,f37507]) ).
fof(f38081,plain,
( ~ v10_lattices(sK56)
| ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_16 ),
inference(forward_subsumption_resolution,[],[f38075,f36436]) ).
fof(f38082,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_16 ),
inference(forward_subsumption_resolution,[],[f38081,f36435]) ).
fof(f38083,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_16 ),
inference(forward_subsumption_resolution,[],[f38082,f36434]) ).
fof(f38084,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_16 ),
inference(forward_subsumption_resolution,[],[f38083,f36439]) ).
fof(f38085,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| spl196_16 ),
inference(forward_subsumption_resolution,[],[f38084,f36438]) ).
fof(f38086,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| spl196_16 ),
inference(forward_subsumption_resolution,[],[f38085,f36437]) ).
fof(f38087,plain,
( ~ spl196_9
| ~ spl196_10
| ~ spl196_11
| spl196_16 ),
inference(avatar_split_clause,[],[f38086,f37747,f37607,f37604,f37601]) ).
fof(f38089,plain,
( ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_17 ),
inference(resolution,[],[f37751,f36423]) ).
fof(f38106,plain,
( ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_17 ),
inference(forward_subsumption_resolution,[],[f38089,f36439]) ).
fof(f38108,plain,
( ~ m1_subset_1(sK57,u1_struct_0(sK56))
| v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_17 ),
inference(forward_subsumption_resolution,[],[f38106,f36438]) ).
fof(f38110,plain,
( v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_17 ),
inference(forward_subsumption_resolution,[],[f38108,f36437]) ).
fof(f38112,plain,
( ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| spl196_17 ),
inference(forward_subsumption_resolution,[],[f38110,f36436]) ).
fof(f38114,plain,
( ~ l3_lattices(sK56)
| spl196_17 ),
inference(forward_subsumption_resolution,[],[f38112,f36435]) ).
fof(f38116,plain,
( $false
| spl196_17 ),
inference(forward_subsumption_resolution,[],[f38114,f36434]) ).
fof(f38117,plain,
spl196_17,
inference(avatar_contradiction_clause,[],[f38116]) ).
fof(f38120,plain,
( v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ spl196_4 ),
inference(resolution,[],[f37554,f37504]) ).
fof(f38124,plain,
( ~ v10_lattices(sK56)
| ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ spl196_4 ),
inference(forward_subsumption_resolution,[],[f38120,f36436]) ).
fof(f38125,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ l3_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ spl196_4 ),
inference(forward_subsumption_resolution,[],[f38124,f36435]) ).
fof(f38126,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ r3_lattices(sK56,sK57,sK58)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ spl196_4 ),
inference(forward_subsumption_resolution,[],[f38125,f36434]) ).
fof(f38127,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ m1_subset_1(sK58,u1_struct_0(sK56))
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ spl196_4 ),
inference(forward_subsumption_resolution,[],[f38126,f36439]) ).
fof(f38128,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ m1_subset_1(sK57,u1_struct_0(sK56))
| ~ spl196_4 ),
inference(forward_subsumption_resolution,[],[f38127,f36438]) ).
fof(f38129,plain,
( ~ v15_lattices(sK56)
| ~ v16_lattices(sK56)
| ~ v12_lattices(sK56)
| ~ spl196_4 ),
inference(forward_subsumption_resolution,[],[f38128,f36437]) ).
fof(f38130,plain,
( ~ spl196_9
| ~ spl196_10
| ~ spl196_11
| ~ spl196_4 ),
inference(avatar_split_clause,[],[f38129,f37553,f37607,f37604,f37601]) ).
cnf(s1,plain,
( ~ spl196_1
| ~ spl196_2
| ~ spl196_3
| spl196_4 ),
inference(sat_conversion,[],[f37555]) ).
cnf(s4,plain,
( spl196_1
| ~ spl196_9
| ~ spl196_10
| ~ spl196_11 ),
inference(sat_conversion,[],[f37609]) ).
cnf(s8,plain,
spl196_11,
inference(sat_conversion,[],[f37635]) ).
cnf(s14,plain,
spl196_9,
inference(sat_conversion,[],[f37725]) ).
cnf(s16,plain,
spl196_10,
inference(sat_conversion,[],[f37737]) ).
cnf(s18,plain,
( ~ spl196_1
| spl196_2
| spl196_4
| ~ spl196_15
| ~ spl196_16
| ~ spl196_17 ),
inference(sat_conversion,[],[f37753]) ).
cnf(s20,plain,
( spl196_15
| ~ spl196_19
| spl196_20
| ~ spl196_21 ),
inference(sat_conversion,[],[f37779]) ).
cnf(s22,plain,
spl196_21,
inference(sat_conversion,[],[f37794]) ).
cnf(s25,plain,
( spl196_3
| ~ spl196_9
| ~ spl196_10
| ~ spl196_11 ),
inference(sat_conversion,[],[f37836]) ).
cnf(s27,plain,
spl196_19,
inference(sat_conversion,[],[f37858]) ).
cnf(s45,plain,
~ spl196_20,
inference(sat_conversion,[],[f38074]) ).
cnf(s46,plain,
( ~ spl196_9
| ~ spl196_10
| ~ spl196_11
| spl196_16 ),
inference(sat_conversion,[],[f38087]) ).
cnf(s49,plain,
spl196_17,
inference(sat_conversion,[],[f38117]) ).
cnf(s51,plain,
( ~ spl196_4
| ~ spl196_9
| ~ spl196_10
| ~ spl196_11 ),
inference(sat_conversion,[],[f38130]) ).
cnf(s53,plain,
spl196_15,
inference(rat,[],[s20,s22,s45,s27]) ).
cnf(s54,plain,
( ~ spl196_1
| spl196_2
| spl196_4
| ~ spl196_16 ),
inference(rat,[],[s18,s49,s53]) ).
cnf(s56,plain,
spl196_16,
inference(rat,[],[s46,s14,s16,s8]) ).
cnf(s57,plain,
~ spl196_4,
inference(rat,[],[s51,s14,s16,s8]) ).
cnf(s58,plain,
spl196_3,
inference(rat,[],[s25,s14,s16,s8]) ).
cnf(s59,plain,
spl196_1,
inference(rat,[],[s4,s8,s16,s14]) ).
cnf(s60,plain,
spl196_2,
inference(rat,[],[s54,s56,s57,s59]) ).
cnf(s61,plain,
$false,
inference(rat,[],[s1,s57,s58,s60,s59]) ).
fof(f38131,plain,
$false,
inference(avatar_sat_refutation,[],[s61]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT337+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n007.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 14:45:02 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 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
% 18.16/5.70 % (1504080)Detected formulas, will run a generic FOF schedule.
% 18.16/5.70 % (1504133)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1523689212:i=119:av=off:ss=axioms_2974 on theBenchmark for (2974ds/119Mi)
% 18.16/5.70 % (1504130)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=981794072:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2974 on theBenchmark for (2974ds/134677Mi)
% 18.16/5.70 % (1504132)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=557189365:i=109:sd=1:ins=1:gsp=on:ss=axioms_2974 on theBenchmark for (2974ds/109Mi)
% 18.16/5.70 % (1504131)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=1289898774:i=141695:sd=1:nm=32:gsp=on:ss=included_2974 on theBenchmark for (2974ds/141695Mi)
% 18.16/5.70 % (1504129)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=4122975512:i=141193_2974 on theBenchmark for (2974ds/141193Mi)
% 18.16/5.70 % (1504133)Instruction limit reached!
% 18.16/5.70 % (1504133)------------------------------
% 18.16/5.70 % (1504133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504133)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504133)Termination reason: Instruction limit
% 18.16/5.70 % (1504133)Termination phase: SInE selection
% 18.16/5.70 % (1504133)Time elapsed: 0.070 s
% 18.16/5.70 % (1504133)Peak memory usage: 136 MB
% 18.16/5.70 % (1504133)Instructions burned: 120 (million)
% 18.16/5.70 % (1504135)dis-21_1_sil=8000:lcm=predicate:random_seed=3531452047:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2974 on theBenchmark for (2974ds/129Mi)
% 18.16/5.70 % (1504134)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=480274337:s2a=on:i=139:gtg=position_2974 on theBenchmark for (2974ds/139Mi)
% 18.16/5.70 % (1504132)Instruction limit reached!
% 18.16/5.70 % (1504132)------------------------------
% 18.16/5.70 % (1504132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504132)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504132)Termination reason: Instruction limit
% 18.16/5.70 % (1504132)Termination phase: SInE selection
% 18.16/5.70 % (1504132)Time elapsed: 0.115 s
% 18.16/5.70 % (1504132)Peak memory usage: 136 MB
% 18.16/5.70 % (1504132)Instructions burned: 109 (million)
% 18.16/5.70 % (1504134)Instruction limit reached!
% 18.16/5.70 % (1504134)------------------------------
% 18.16/5.70 % (1504134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504134)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504134)Termination reason: Instruction limit
% 18.16/5.70 % (1504134)Termination phase: Property scanning
% 18.16/5.70 % (1504134)Time elapsed: 0.119 s
% 18.16/5.70 % (1504134)Peak memory usage: 136 MB
% 18.16/5.70 % (1504134)Instructions burned: 139 (million)
% 18.16/5.70 % (1504141)lrs+10_1_sil=8000:sp=occurrence:random_seed=781298048:i=285:sd=3:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/285Mi)
% 18.16/5.70 % (1504135)Instruction limit reached!
% 18.16/5.70 % (1504135)------------------------------
% 18.16/5.70 % (1504135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504135)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504135)Termination reason: Instruction limit
% 18.16/5.70 % (1504135)Termination phase: SInE selection
% 18.16/5.70 % (1504135)Time elapsed: 0.138 s
% 18.16/5.70 % (1504135)Peak memory usage: 136 MB
% 18.16/5.70 % (1504135)Instructions burned: 130 (million)
% 18.16/5.70 % (1504144)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1985887167:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/157Mi)
% 18.16/5.70 % (1504147)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=1497993102:s2a=on:i=248:s2at=1.23:gtg=position_2970 on theBenchmark for (2970ds/248Mi)
% 18.16/5.70 % (1504141)Instruction limit reached!
% 18.16/5.70 % (1504141)------------------------------
% 18.16/5.70 % (1504141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504141)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504141)Termination reason: Instruction limit
% 18.16/5.70 % (1504141)Termination phase: Saturation
% 18.16/5.70 % (1504141)Time elapsed: 0.176 s
% 18.16/5.70 % (1504141)Peak memory usage: 141 MB
% 18.16/5.70 % (1504141)Instructions burned: 285 (million)
% 18.16/5.70 % (1504145)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3654793183:i=325:sd=1:ss=axioms:sgt=32_2970 on theBenchmark for (2970ds/325Mi)
% 18.16/5.70 % (1504144)Instruction limit reached!
% 18.16/5.70 % (1504144)------------------------------
% 18.16/5.70 % (1504144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504144)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504144)Termination reason: Instruction limit
% 18.16/5.70 % (1504144)Termination phase: Property scanning
% 18.16/5.70 % (1504144)Time elapsed: 0.132 s
% 18.16/5.70 % (1504144)Peak memory usage: 136 MB
% 18.16/5.70 % (1504144)Instructions burned: 157 (million)
% 18.16/5.70 % (1504147)Instruction limit reached!
% 18.16/5.70 % (1504147)------------------------------
% 18.16/5.70 % (1504147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504147)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504147)Termination reason: Instruction limit
% 18.16/5.70 % (1504147)Termination phase: Property scanning
% 18.16/5.70 % (1504147)Time elapsed: 0.120 s
% 18.16/5.70 % (1504147)Peak memory usage: 136 MB
% 18.16/5.70 % (1504147)Instructions burned: 249 (million)
% 18.16/5.70 % (1504150)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3481129210:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2968 on theBenchmark for (2968ds/294Mi)
% 18.16/5.70 % (1504152)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=623485756:i=2350_2968 on theBenchmark for (2968ds/2350Mi)
% 18.16/5.70 % (1504153)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3187501838:cts=off:i=113:fsr=off:ss=included:sgt=4_2967 on theBenchmark for (2967ds/113Mi)
% 18.16/5.70 % (1504153)Instruction limit reached!
% 18.16/5.70 % (1504153)------------------------------
% 18.16/5.70 % (1504153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504153)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504153)Termination reason: Instruction limit
% 18.16/5.70 % (1504153)Termination phase: SInE selection
% 18.16/5.70 % (1504153)Time elapsed: 0.094 s
% 18.16/5.70 % (1504153)Peak memory usage: 136 MB
% 18.16/5.70 % (1504153)Instructions burned: 114 (million)
% 18.16/5.70 % (1504145)Instruction limit reached!
% 18.16/5.70 % (1504145)------------------------------
% 18.16/5.70 % (1504145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504145)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504145)Termination reason: Instruction limit
% 18.16/5.70 % (1504145)Termination phase: Saturation
% 18.16/5.70 % (1504145)Time elapsed: 0.366 s
% 18.16/5.70 % (1504145)Peak memory usage: 142 MB
% 18.16/5.70 % (1504145)Instructions burned: 326 (million)
% 18.16/5.70 % (1504150)Instruction limit reached!
% 18.16/5.70 % (1504150)------------------------------
% 18.16/5.70 % (1504150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504150)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504150)Termination reason: Instruction limit
% 18.16/5.70 % (1504150)Termination phase: SInE selection
% 18.16/5.70 % (1504150)Time elapsed: 0.275 s
% 18.16/5.70 % (1504150)Peak memory usage: 137 MB
% 18.16/5.70 % (1504150)Instructions burned: 295 (million)
% 18.16/5.70 % (1504160)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4028555049:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2964 on theBenchmark for (2964ds/114Mi)
% 18.16/5.70 % (1504159)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3538100975:i=127:av=off:fsr=off:sup=off_2965 on theBenchmark for (2965ds/127Mi)
% 18.16/5.70 % (1504160)Instruction limit reached!
% 18.16/5.70 % (1504160)------------------------------
% 18.16/5.70 % (1504160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504160)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504160)Termination reason: Instruction limit
% 18.16/5.70 % (1504160)Termination phase: Property scanning
% 18.16/5.70 % (1504160)Time elapsed: 0.061 s
% 18.16/5.70 % (1504160)Peak memory usage: 137 MB
% 18.16/5.70 % (1504160)Instructions burned: 114 (million)
% 18.16/5.70 % (1504159)Instruction limit reached!
% 18.16/5.70 % (1504159)------------------------------
% 18.16/5.70 % (1504159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504159)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504159)Termination reason: Instruction limit
% 18.16/5.70 % (1504159)Termination phase: Preprocessing 1
% 18.16/5.70 % (1504159)Time elapsed: 0.152 s
% 18.16/5.70 % (1504159)Peak memory usage: 137 MB
% 18.16/5.70 % (1504159)Instructions burned: 127 (million)
% 18.16/5.70 % (1504161)lrs+10_1_sil=8000:sp=occurrence:random_seed=2547390902:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2963 on theBenchmark for (2963ds/907Mi)
% 18.16/5.70 % (1504164)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2354183501:i=437:sd=1:aac=none:ss=included_2962 on theBenchmark for (2962ds/437Mi)
% 18.16/5.70 % (1504166)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1973343220:i=5202:ss=axioms:sgt=16_2961 on theBenchmark for (2961ds/5202Mi)
% 18.16/5.70 % (1504164)First to succeed.
% 18.16/5.70 % (1504164)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1504080"
% 18.16/5.70 % (1504152)Instruction limit reached!
% 18.16/5.70 % (1504152)------------------------------
% 18.16/5.70 % (1504152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504152)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504152)Termination reason: Instruction limit
% 18.16/5.70 % (1504152)Termination phase: Property scanning
% 18.16/5.70 % (1504152)Time elapsed: 1.376 s
% 18.16/5.70 % (1504152)Peak memory usage: 233 MB
% 18.16/5.70 % (1504152)Instructions burned: 2352 (million)
% 18.16/5.70 % (1504161)Instruction limit reached!
% 18.16/5.70 % (1504161)------------------------------
% 18.16/5.70 % (1504161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/5.70 % (1504161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/5.70 % (1504161)CaDiCaL version: 2.1.3
% 18.16/5.70 % (1504161)Termination reason: Instruction limit
% 18.16/5.70 % (1504161)Termination phase: Function definition elimination
% 18.16/5.70 % (1504161)Time elapsed: 0.925 s
% 18.16/5.70 % (1504161)Peak memory usage: 156 MB
% 18.16/5.70 % (1504161)Instructions burned: 907 (million)
% 18.16/5.70 % (1504164)Refutation found. Thanks to Tanya!
% 18.16/5.70 % SZS status Theorem for theBenchmark
% 18.16/5.70 % SZS output start Proof for theBenchmark
% See solution above
% 18.92/5.93 % (1504164)------------------------------
% 18.92/5.93 % (1504164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.92/5.93 % (1504164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.92/5.93 % (1504164)CaDiCaL version: 2.1.3
% 18.92/5.93 % (1504164)Termination reason: Refutation
% 18.92/5.93 % (1504164)Time elapsed: 0.402 s
% 18.92/5.93 % (1504164)Peak memory usage: 145 MB
% 18.92/5.93 % (1504164)Instructions burned: 369 (million)
% 18.92/5.93 % (1504164)------------------------------
% 18.92/5.93 % (1504164)------------------------------
% 18.92/5.93 % (1504080)Success in time 4.84 s
% 18.92/5.93 % Vampire exiting
%------------------------------------------------------------------------------