%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT297+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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:38 AM UTC 2026
% Result : Theorem 2.81s 1.47s
% Output : Refutation 4.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 10
% Syntax : Number of formulae : 114 ( 14 unt; 2 def)
% Number of atoms : 687 ( 13 equ)
% Maximal formula atoms : 23 ( 6 avg)
% Number of connectives : 914 ( 341 ~; 429 |; 105 &)
% ( 17 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 3 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-3 aty)
% Number of variables : 150 ( 0 sgn 130 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,axiom,
! [X0] :
( X0 = k1_xboole_0
<=> ! [X1] : ~ r2_hidden(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f33,axiom,
! [X0] :
( v1_xboole_0(X0)
<=> X0 = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_xboole_0) ).
fof(f68,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f584,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f2447,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( m1_filter_0(X1,X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_filter_0) ).
fof(f2808,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( m2_lattice4(X1,X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
=> ( r2_hidden(k4_lattices(X0,X2,X3),X1)
& r2_hidden(k3_lattices(X0,X2,X3),X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_lattice4) ).
fof(f2810,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> m2_lattice4(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_lattice4) ).
fof(f2929,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) ) ) )
=> m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_filter_2) ).
fof(f2930,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) ) ) )
=> m2_lattice4(X1,X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f2929]) ).
fof(f2934,plain,
? [X0] :
( ? [X1] :
( ~ m2_lattice4(X1,X0)
& ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2930]) ).
fof(f2935,plain,
? [X0] :
( ? [X1] :
( ~ m2_lattice4(X1,X0)
& ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f2934]) ).
fof(f2945,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f584]) ).
fof(f2946,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f2945]) ).
fof(f2963,plain,
! [X0] :
( ! [X1] :
( m2_lattice4(X1,X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2810]) ).
fof(f2964,plain,
! [X0] :
( ! [X1] :
( m2_lattice4(X1,X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f2963]) ).
fof(f2967,plain,
! [X0] :
( ! [X1] :
( ( m2_lattice4(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( r2_hidden(k4_lattices(X0,X2,X3),X1)
& r2_hidden(k3_lattices(X0,X2,X3),X1) )
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2808]) ).
fof(f2968,plain,
! [X0] :
( ! [X1] :
( ( m2_lattice4(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( r2_hidden(k4_lattices(X0,X2,X3),X1)
& r2_hidden(k3_lattices(X0,X2,X3),X1) )
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f2967]) ).
fof(f2971,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_0(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2447]) ).
fof(f2972,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_0(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f2971]) ).
fof(f2979,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f68]) ).
fof(f3058,plain,
? [X0] :
( ? [X1] :
( ~ m2_lattice4(X1,X0)
& ! [X2] :
( ! [X3] :
( ( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(nnf_transformation,[],[f2935]) ).
fof(f3059,plain,
? [X0] :
( ? [X1] :
( ~ m2_lattice4(X1,X0)
& ! [X2] :
( ! [X3] :
( ( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f3058]) ).
fof(f3060,plain,
( ~ m2_lattice4(sK2,sK1)
& ! [X2] :
( ! [X3] :
( ( ( ( r2_hidden(X2,sK2)
& r2_hidden(X3,sK2) )
| ~ r2_hidden(k4_lattices(sK1,X2,X3),sK2) )
& ( r2_hidden(k4_lattices(sK1,X2,X3),sK2)
| ~ r2_hidden(X2,sK2)
| ~ r2_hidden(X3,sK2) ) )
| ~ m1_subset_1(X3,u1_struct_0(sK1)) )
| ~ m1_subset_1(X2,u1_struct_0(sK1)) )
& m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
& ~ v3_struct_0(sK1)
& v10_lattices(sK1)
& l3_lattices(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X0,sK1),skolemize(X1,sK2)],[f3059]) ).
fof(f3080,plain,
! [X0] :
( ! [X1] :
( ( ( m2_lattice4(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(k3_lattices(X0,X2,X3),X1) )
& r2_hidden(X2,X1)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( ( r2_hidden(k4_lattices(X0,X2,X3),X1)
& r2_hidden(k3_lattices(X0,X2,X3),X1) )
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m2_lattice4(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f2968]) ).
fof(f3081,plain,
! [X0] :
( ! [X1] :
( ( ( m2_lattice4(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(k3_lattices(X0,X2,X3),X1) )
& r2_hidden(X2,X1)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( r2_hidden(k4_lattices(X0,X4,X5),X1)
& r2_hidden(k3_lattices(X0,X4,X5),X1) )
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m2_lattice4(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f3080]) ).
fof(f3082,plain,
! [X0] :
( ! [X1] :
( ( ( m2_lattice4(X1,X0)
| ( ( ~ r2_hidden(k4_lattices(X0,sK16(X0,X1),sK17(X0,X1)),X1)
| ~ r2_hidden(k3_lattices(X0,sK16(X0,X1),sK17(X0,X1)),X1) )
& r2_hidden(sK16(X0,X1),X1)
& r2_hidden(sK17(X0,X1),X1)
& m1_subset_1(sK17(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK16(X0,X1),u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( r2_hidden(k4_lattices(X0,X4,X5),X1)
& r2_hidden(k3_lattices(X0,X4,X5),X1) )
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m2_lattice4(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17]),skolemize(X2,sK16(X0,X1)),skolemize(X3,sK17(X0,X1))],[f3081]) ).
fof(f3084,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( ( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f2972]) ).
fof(f3085,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( ( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3084]) ).
fof(f3086,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( ( ( r2_hidden(X4,X1)
& r2_hidden(X5,X1) )
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1) )
& ( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1) ) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f3085]) ).
fof(f3087,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ( ( ~ r2_hidden(k4_lattices(X0,sK19(X0,X1),sK20(X0,X1)),X1)
| ~ r2_hidden(sK19(X0,X1),X1)
| ~ r2_hidden(sK20(X0,X1),X1) )
& ( r2_hidden(k4_lattices(X0,sK19(X0,X1),sK20(X0,X1)),X1)
| ( r2_hidden(sK19(X0,X1),X1)
& r2_hidden(sK20(X0,X1),X1) ) )
& m1_subset_1(sK20(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK19(X0,X1),u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( ( ( r2_hidden(X4,X1)
& r2_hidden(X5,X1) )
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1) )
& ( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1) ) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20]),skolemize(X2,sK19(X0,X1)),skolemize(X3,sK20(X0,X1))],[f3086]) ).
fof(f3099,plain,
! [X0] :
( ( v1_xboole_0(X0)
| k1_xboole_0 != X0 )
& ( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ) ),
inference(nnf_transformation,[],[f33]) ).
fof(f3100,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X1] : ~ r2_hidden(X1,X0)
| k1_xboole_0 != X0 ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f3101,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(rectify,[],[f3100]) ).
fof(f3102,plain,
! [X0] :
( ( X0 = k1_xboole_0
| r2_hidden(sK27(X0),X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(X1,sK27(X0))],[f3101]) ).
fof(f3119,plain,
l3_lattices(sK1),
inference(cnf_transformation,[],[f3060]) ).
fof(f3120,plain,
v10_lattices(sK1),
inference(cnf_transformation,[],[f3060]) ).
fof(f3121,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f3060]) ).
fof(f3122,plain,
m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))),
inference(cnf_transformation,[],[f3060]) ).
fof(f3123,plain,
! [X2,X3] :
( r2_hidden(k4_lattices(sK1,X2,X3),sK2)
| ~ r2_hidden(X2,sK2)
| ~ r2_hidden(X3,sK2)
| ~ m1_subset_1(X3,u1_struct_0(sK1))
| ~ m1_subset_1(X2,u1_struct_0(sK1)) ),
inference(cnf_transformation,[],[f3060]) ).
fof(f3124,plain,
! [X2,X3] :
( ~ r2_hidden(k4_lattices(sK1,X2,X3),sK2)
| r2_hidden(X3,sK2)
| ~ m1_subset_1(X3,u1_struct_0(sK1))
| ~ m1_subset_1(X2,u1_struct_0(sK1)) ),
inference(cnf_transformation,[],[f3060]) ).
fof(f3125,plain,
! [X2,X3] :
( ~ r2_hidden(k4_lattices(sK1,X2,X3),sK2)
| r2_hidden(X2,sK2)
| ~ m1_subset_1(X3,u1_struct_0(sK1))
| ~ m1_subset_1(X2,u1_struct_0(sK1)) ),
inference(cnf_transformation,[],[f3060]) ).
fof(f3126,plain,
~ m2_lattice4(sK2,sK1),
inference(cnf_transformation,[],[f3060]) ).
fof(f3139,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f2946]) ).
fof(f3168,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f2964]) ).
fof(f3174,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| r2_hidden(sK17(X0,X1),X1)
| m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3082]) ).
fof(f3182,plain,
! [X0,X1] :
( m1_subset_1(sK19(X0,X1),u1_struct_0(X0))
| m1_filter_0(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3087]) ).
fof(f3183,plain,
! [X0,X1] :
( m1_subset_1(sK20(X0,X1),u1_struct_0(X0))
| m1_filter_0(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3087]) ).
fof(f3184,plain,
! [X0,X1] :
( r2_hidden(k4_lattices(X0,sK19(X0,X1),sK20(X0,X1)),X1)
| m1_filter_0(X1,X0)
| r2_hidden(sK20(X0,X1),X1)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3087]) ).
fof(f3185,plain,
! [X0,X1] :
( r2_hidden(k4_lattices(X0,sK19(X0,X1),sK20(X0,X1)),X1)
| m1_filter_0(X1,X0)
| r2_hidden(sK19(X0,X1),X1)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3087]) ).
fof(f3186,plain,
! [X0,X1] :
( m1_filter_0(X1,X0)
| ~ r2_hidden(k4_lattices(X0,sK19(X0,X1),sK20(X0,X1)),X1)
| ~ r2_hidden(sK19(X0,X1),X1)
| ~ r2_hidden(sK20(X0,X1),X1)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3087]) ).
fof(f3202,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f2979]) ).
fof(f3241,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| k1_xboole_0 = X0 ),
inference(cnf_transformation,[],[f3099]) ).
fof(f3243,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ),
inference(cnf_transformation,[],[f3102]) ).
fof(f3308,plain,
! [X2] : ~ r2_hidden(X2,k1_xboole_0),
inference(equality_resolution,[],[f3243]) ).
fof(f3321,plain,
! [X0,X1] :
( ~ r2_hidden(k4_lattices(X0,sK19(X0,X1),sK20(X0,X1)),X1)
| m1_filter_0(X1,X0)
| ~ r2_hidden(sK19(X0,X1),X1)
| ~ r2_hidden(sK20(X0,X1),X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f3186,f3202]) ).
fof(f3707,definition,
( spl42_20
<=> v1_xboole_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl42_20])],[avatar_definition]) ).
fof(f3708,plain,
( ~ v1_xboole_0(sK2)
| spl42_20 ),
inference(avatar_component_clause,[],[f3707]) ).
fof(f3709,plain,
( v1_xboole_0(sK2)
| ~ spl42_20 ),
inference(avatar_component_clause,[],[f3707]) ).
fof(f3715,plain,
( k1_xboole_0 = sK2
| ~ spl42_20 ),
inference(resolution,[],[f3709,f3241]) ).
fof(f4165,plain,
( r2_hidden(sK17(sK1,sK2),sK2)
| m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(resolution,[],[f3174,f3122]) ).
fof(f4180,plain,
( r2_hidden(sK17(sK1,sK2),sK2)
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f4165,f3126]) ).
fof(f4184,plain,
( r2_hidden(sK17(sK1,sK2),sK2)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f4180,f3121]) ).
fof(f4187,plain,
( r2_hidden(sK17(sK1,sK2),sK2)
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f4184,f3120]) ).
fof(f4189,plain,
r2_hidden(sK17(sK1,sK2),sK2),
inference(forward_subsumption_resolution,[],[f4187,f3119]) ).
fof(f4191,plain,
( r2_hidden(sK17(sK1,k1_xboole_0),k1_xboole_0)
| ~ spl42_20 ),
inference(forward_demodulation,[],[f4189,f3715]) ).
fof(f4193,plain,
( $false
| ~ spl42_20 ),
inference(forward_subsumption_resolution,[],[f4191,f3308]) ).
fof(f4194,plain,
~ spl42_20,
inference(avatar_contradiction_clause,[],[f4193]) ).
fof(f4286,definition,
( spl42_29
<=> m1_filter_0(sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl42_29])],[avatar_definition]) ).
fof(f4287,plain,
( m1_filter_0(sK2,sK1)
| ~ spl42_29 ),
inference(avatar_component_clause,[],[f4286]) ).
fof(f4288,plain,
( ~ m1_filter_0(sK2,sK1)
| spl42_29 ),
inference(avatar_component_clause,[],[f4286]) ).
fof(f4692,plain,
( m1_filter_0(sK2,sK1)
| r2_hidden(sK20(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| r2_hidden(sK20(sK1,sK2),sK2)
| ~ m1_subset_1(sK20(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK19(sK1,sK2),u1_struct_0(sK1)) ),
inference(resolution,[],[f3184,f3124]) ).
fof(f4715,plain,
( m1_filter_0(sK2,sK1)
| r2_hidden(sK20(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK20(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK19(sK1,sK2),u1_struct_0(sK1)) ),
inference(duplicate_literal_removal,[],[f4692]) ).
fof(f4723,plain,
( m1_filter_0(sK2,sK1)
| r2_hidden(sK20(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK19(sK1,sK2),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f4715,f3183]) ).
fof(f4731,plain,
( m1_filter_0(sK2,sK1)
| r2_hidden(sK20(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f4723,f3182]) ).
fof(f4768,plain,
( m1_filter_0(sK2,sK1)
| r2_hidden(sK19(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| r2_hidden(sK19(sK1,sK2),sK2)
| ~ m1_subset_1(sK20(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK19(sK1,sK2),u1_struct_0(sK1)) ),
inference(resolution,[],[f3185,f3125]) ).
fof(f4792,plain,
( m1_filter_0(sK2,sK1)
| r2_hidden(sK19(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK20(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK19(sK1,sK2),u1_struct_0(sK1)) ),
inference(duplicate_literal_removal,[],[f4768]) ).
fof(f4800,plain,
( m1_filter_0(sK2,sK1)
| r2_hidden(sK19(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK19(sK1,sK2),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f4792,f3183]) ).
fof(f4807,plain,
( m1_filter_0(sK2,sK1)
| r2_hidden(sK19(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f4800,f3182]) ).
fof(f4911,plain,
( m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl42_29 ),
inference(resolution,[],[f4287,f3168]) ).
fof(f4913,plain,
( v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl42_29 ),
inference(forward_subsumption_resolution,[],[f4911,f3126]) ).
fof(f4914,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl42_29 ),
inference(forward_subsumption_resolution,[],[f4913,f3121]) ).
fof(f4915,plain,
( ~ l3_lattices(sK1)
| ~ spl42_29 ),
inference(forward_subsumption_resolution,[],[f4914,f3120]) ).
fof(f4916,plain,
( $false
| ~ spl42_29 ),
inference(forward_subsumption_resolution,[],[f4915,f3119]) ).
fof(f4917,plain,
~ spl42_29,
inference(avatar_contradiction_clause,[],[f4916]) ).
fof(f4919,plain,
( r2_hidden(sK20(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f4731,f4288]) ).
fof(f4922,plain,
( r2_hidden(sK19(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f4807,f4288]) ).
fof(f4923,plain,
( r2_hidden(sK20(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f4919,f3708]) ).
fof(f4926,plain,
( r2_hidden(sK19(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f4922,f3708]) ).
fof(f4927,plain,
( r2_hidden(sK20(sK1,sK2),sK2)
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f4923,f3122]) ).
fof(f4930,plain,
( r2_hidden(sK19(sK1,sK2),sK2)
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f4926,f3122]) ).
fof(f4931,plain,
( r2_hidden(sK20(sK1,sK2),sK2)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f4927,f3121]) ).
fof(f4934,plain,
( r2_hidden(sK19(sK1,sK2),sK2)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f4930,f3121]) ).
fof(f4935,plain,
( r2_hidden(sK20(sK1,sK2),sK2)
| ~ l3_lattices(sK1)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f4931,f3120]) ).
fof(f4938,plain,
( r2_hidden(sK19(sK1,sK2),sK2)
| ~ l3_lattices(sK1)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f4934,f3120]) ).
fof(f4939,plain,
( r2_hidden(sK20(sK1,sK2),sK2)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f4935,f3119]) ).
fof(f4942,plain,
( r2_hidden(sK19(sK1,sK2),sK2)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f4938,f3119]) ).
fof(f5237,plain,
( m1_filter_0(sK2,sK1)
| ~ r2_hidden(sK19(sK1,sK2),sK2)
| ~ r2_hidden(sK20(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ r2_hidden(sK19(sK1,sK2),sK2)
| ~ r2_hidden(sK20(sK1,sK2),sK2)
| ~ m1_subset_1(sK20(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK19(sK1,sK2),u1_struct_0(sK1)) ),
inference(resolution,[],[f3321,f3123]) ).
fof(f5249,plain,
( m1_filter_0(sK2,sK1)
| ~ r2_hidden(sK19(sK1,sK2),sK2)
| ~ r2_hidden(sK20(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK20(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK19(sK1,sK2),u1_struct_0(sK1)) ),
inference(duplicate_literal_removal,[],[f5237]) ).
fof(f5252,plain,
( m1_filter_0(sK2,sK1)
| ~ r2_hidden(sK19(sK1,sK2),sK2)
| ~ r2_hidden(sK20(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK20(sK1,sK2),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f5249,f3139]) ).
fof(f5255,plain,
( m1_filter_0(sK2,sK1)
| ~ r2_hidden(sK19(sK1,sK2),sK2)
| ~ r2_hidden(sK20(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f5252,f3139]) ).
fof(f5258,plain,
( ~ r2_hidden(sK19(sK1,sK2),sK2)
| ~ r2_hidden(sK20(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f5255,f4288]) ).
fof(f5260,plain,
( ~ r2_hidden(sK20(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f5258,f4942]) ).
fof(f5262,plain,
( ~ r2_hidden(sK20(sK1,sK2),sK2)
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f5260,f3122]) ).
fof(f5264,plain,
( ~ r2_hidden(sK20(sK1,sK2),sK2)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f5262,f3121]) ).
fof(f5266,plain,
( ~ r2_hidden(sK20(sK1,sK2),sK2)
| ~ l3_lattices(sK1)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f5264,f3120]) ).
fof(f5267,plain,
( ~ r2_hidden(sK20(sK1,sK2),sK2)
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f5266,f3119]) ).
fof(f5337,plain,
( $false
| spl42_20
| spl42_29 ),
inference(forward_subsumption_resolution,[],[f5267,f4939]) ).
fof(f5338,plain,
( spl42_20
| spl42_29 ),
inference(avatar_contradiction_clause,[],[f5337]) ).
cnf(s15,plain,
~ spl42_20,
inference(sat_conversion,[],[f4194]) ).
cnf(s31,plain,
~ spl42_29,
inference(sat_conversion,[],[f4917]) ).
cnf(s45,plain,
( spl42_20
| spl42_29 ),
inference(sat_conversion,[],[f5338]) ).
cnf(s46,plain,
spl42_20,
inference(rat,[],[s45,s31]) ).
cnf(s48,plain,
$false,
inference(rat,[],[s15,s46]) ).
fof(f5339,plain,
$false,
inference(avatar_sat_refutation,[],[s48]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT297+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.09/0.37 % Computer : n004.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 14:20:37 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 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
% 2.81/1.47 % (3564350)Detected formulas, will run a generic FOF schedule.
% 2.81/1.47 % (3564361)dis-21_1_sil=8000:lcm=predicate:random_seed=222589120: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)
% 2.81/1.47 % (3564355)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=1190790159:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 2.81/1.47 % (3564359)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=918267709:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 2.81/1.47 % (3564358)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=17501721:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 2.81/1.47 % (3564356)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=135095613:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 2.81/1.47 % (3564357)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=2791993774:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 2.81/1.47 % (3564360)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3443740282:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 2.81/1.47 % (3564361)Instruction limit reached!
% 2.81/1.47 % (3564361)------------------------------
% 2.81/1.47 % (3564361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.81/1.47 % (3564361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.81/1.47 % (3564361)CaDiCaL version: 2.1.3
% 2.81/1.47 % (3564361)Termination reason: Instruction limit
% 2.81/1.47 % (3564361)Termination phase: Function definition elimination
% 2.81/1.47 % (3564361)Time elapsed: 0.044 s
% 2.81/1.47 % (3564361)Peak memory usage: 93 MB
% 2.81/1.47 % (3564361)Instructions burned: 131 (million)
% 2.81/1.47 % (3564358)Instruction limit reached!
% 2.81/1.47 % (3564358)------------------------------
% 2.81/1.47 % (3564358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.81/1.47 % (3564358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.81/1.47 % (3564358)CaDiCaL version: 2.1.3
% 2.81/1.47 % (3564358)Termination reason: Instruction limit
% 2.81/1.47 % (3564358)Termination phase: Saturation
% 2.81/1.47 % (3564358)Time elapsed: 0.069 s
% 2.81/1.47 % (3564358)Peak memory usage: 92 MB
% 2.81/1.47 % (3564358)Instructions burned: 111 (million)
% 2.81/1.47 % (3564359)Instruction limit reached!
% 2.81/1.47 % (3564359)------------------------------
% 2.81/1.47 % (3564359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.81/1.47 % (3564359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.81/1.47 % (3564359)CaDiCaL version: 2.1.3
% 2.81/1.47 % (3564359)Termination reason: Instruction limit
% 2.81/1.47 % (3564359)Termination phase: Saturation
% 2.81/1.47 % (3564359)Time elapsed: 0.077 s
% 2.81/1.47 % (3564359)Peak memory usage: 91 MB
% 2.81/1.47 % (3564359)Instructions burned: 120 (million)
% 2.81/1.47 % (3564360)Instruction limit reached!
% 2.81/1.47 % (3564360)------------------------------
% 2.81/1.47 % (3564360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.81/1.47 % (3564360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.81/1.47 % (3564360)CaDiCaL version: 2.1.3
% 2.81/1.47 % (3564360)Termination reason: Instruction limit
% 2.81/1.47 % (3564360)Termination phase: Property scanning
% 2.81/1.47 % (3564360)Time elapsed: 0.088 s
% 2.81/1.47 % (3564360)Peak memory usage: 94 MB
% 2.81/1.47 % (3564360)Instructions burned: 140 (million)
% 2.81/1.47 % (3564369)lrs+10_1_sil=8000:sp=occurrence:random_seed=123918700:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 2.81/1.47 % (3564369)First to succeed.
% 2.81/1.47 % (3564369)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3564350"
% 2.81/1.47 % (3564370)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2704029106:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 2.81/1.47 % (3564371)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1588055080:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 2.81/1.47 % (3564372)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=1676092537:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 2.81/1.47 % (3564370)Instruction limit reached!
% 2.81/1.47 % (3564370)------------------------------
% 2.81/1.47 % (3564370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.81/1.47 % (3564370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.81/1.47 % (3564370)CaDiCaL version: 2.1.3
% 2.81/1.47 % (3564370)Termination reason: Instruction limit
% 2.81/1.47 % (3564370)Termination phase: Saturation
% 2.81/1.47 % (3564370)Time elapsed: 0.088 s
% 2.81/1.47 % (3564370)Peak memory usage: 92 MB
% 2.81/1.47 % (3564370)Instructions burned: 157 (million)
% 2.81/1.47 % (3564369)Refutation found. Thanks to Tanya!
% 2.81/1.47 % SZS status Theorem for theBenchmark
% 2.81/1.47 % SZS output start Proof for theBenchmark
% See solution above
% 4.30/1.67 % (3564369)------------------------------
% 4.30/1.67 % (3564369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.30/1.67 % (3564369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.30/1.67 % (3564369)CaDiCaL version: 2.1.3
% 4.30/1.67 % (3564369)Termination reason: Refutation
% 4.30/1.67 % (3564369)Time elapsed: 0.047 s
% 4.30/1.67 % (3564369)Peak memory usage: 94 MB
% 4.30/1.67 % (3564369)Instructions burned: 131 (million)
% 4.30/1.67 % (3564369)------------------------------
% 4.30/1.67 % (3564369)------------------------------
% 4.30/1.67 % (3564350)Success in time 0.615 s
% 4.30/1.67 % Vampire exiting
%------------------------------------------------------------------------------