%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT333+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 : n014.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:03 AM UTC 2026
% Result : Theorem 39.86s 9.22s
% Output : Refutation 46.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 36
% Syntax : Number of formulae : 335 ( 37 unt; 15 def)
% Number of atoms : 1469 ( 101 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 1869 ( 735 ~; 893 |; 183 &)
% ( 25 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 14 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-3 aty)
% Number of variables : 189 ( 0 sgn 185 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21572,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( v14_lattices(X0)
=> v14_lattices(k8_filter_0(X0,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t66_filter_0) ).
fof(f21611,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_filter_0(X1,X0) )
=> ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1))
& l3_lattices(k8_filter_0(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_filter_0) ).
fof(f22747,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f22752,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f22779,axiom,
! [X0] :
( l3_lattices(X0)
=> k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_lattice2) ).
fof(f22780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22781,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_lattices(X0)
& l3_lattices(X0) )
=> k1_lattice2(k1_lattice2(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t19_lattice2) ).
fof(f22827,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t63_lattice2) ).
fof(f22828,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_lattice2) ).
fof(f22852,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f25570,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_nat_lat(X1,X0)
=> ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_nat_lat) ).
fof(f31938,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/sandbox2/benchmark/theBenchmark.p',t11_lattice4) ).
fof(f34606,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f34607,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f34647,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> m2_nat_lat(k23_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k23_filter_2) ).
fof(f34657,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_filter_2) ).
fof(f34675,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_filter_2) ).
fof(f34742,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( ~ v3_struct_0(k23_filter_2(X0,X1))
& v3_lattices(k23_filter_2(X0,X1))
& v4_lattices(k23_filter_2(X0,X1))
& v5_lattices(k23_filter_2(X0,X1))
& v6_lattices(k23_filter_2(X0,X1))
& v7_lattices(k23_filter_2(X0,X1))
& v8_lattices(k23_filter_2(X0,X1))
& v9_lattices(k23_filter_2(X0,X1))
& v10_lattices(k23_filter_2(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_filter_2) ).
fof(f34743,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
=> k8_filter_0(X0,X1) = k23_filter_2(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t70_filter_2) ).
fof(f34746,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( u1_struct_0(k23_filter_2(X0,X1)) = X1
& u2_lattices(k23_filter_2(X0,X1)) = k1_realset1(u2_lattices(X0),X1)
& u1_lattices(k23_filter_2(X0,X1)) = k1_realset1(u1_lattices(X0),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t73_filter_2) ).
fof(f34749,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( v13_lattices(X0)
=> v13_lattices(k23_filter_2(X0,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t76_filter_2) ).
fof(f34750,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( v13_lattices(X0)
=> v13_lattices(k23_filter_2(X0,X1)) ) ) ),
inference(negated_conjecture,[status(cth)],[f34749]) ).
fof(f35027,plain,
? [X0] :
( ? [X1] :
( ~ v13_lattices(k23_filter_2(X0,X1))
& v13_lattices(X0)
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34750]) ).
fof(f35028,plain,
? [X0] :
( ? [X1] :
( ~ v13_lattices(k23_filter_2(X0,X1))
& v13_lattices(X0)
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f35027]) ).
fof(f35059,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22828]) ).
fof(f35060,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35059]) ).
fof(f35061,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22827]) ).
fof(f35062,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35061]) ).
fof(f35095,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34607]) ).
fof(f35096,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35095]) ).
fof(f35101,plain,
! [X0] :
( ! [X1] :
( ( u1_struct_0(k23_filter_2(X0,X1)) = X1
& u2_lattices(k23_filter_2(X0,X1)) = k1_realset1(u2_lattices(X0),X1)
& u1_lattices(k23_filter_2(X0,X1)) = k1_realset1(u1_lattices(X0),X1) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34746]) ).
fof(f35102,plain,
! [X0] :
( ! [X1] :
( ( u1_struct_0(k23_filter_2(X0,X1)) = X1
& u2_lattices(k23_filter_2(X0,X1)) = k1_realset1(u2_lattices(X0),X1)
& u1_lattices(k23_filter_2(X0,X1)) = k1_realset1(u1_lattices(X0),X1) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35101]) ).
fof(f35103,plain,
! [X0] :
( ! [X1] :
( k8_filter_0(X0,X1) = k23_filter_2(X0,X1)
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34743]) ).
fof(f35104,plain,
! [X0] :
( ! [X1] :
( k8_filter_0(X0,X1) = k23_filter_2(X0,X1)
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35103]) ).
fof(f35105,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k23_filter_2(X0,X1))
& v3_lattices(k23_filter_2(X0,X1))
& v4_lattices(k23_filter_2(X0,X1))
& v5_lattices(k23_filter_2(X0,X1))
& v6_lattices(k23_filter_2(X0,X1))
& v7_lattices(k23_filter_2(X0,X1))
& v8_lattices(k23_filter_2(X0,X1))
& v9_lattices(k23_filter_2(X0,X1))
& v10_lattices(k23_filter_2(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(ennf_transformation,[],[f34742]) ).
fof(f35106,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k23_filter_2(X0,X1))
& v3_lattices(k23_filter_2(X0,X1))
& v4_lattices(k23_filter_2(X0,X1))
& v5_lattices(k23_filter_2(X0,X1))
& v6_lattices(k23_filter_2(X0,X1))
& v7_lattices(k23_filter_2(X0,X1))
& v8_lattices(k23_filter_2(X0,X1))
& v9_lattices(k23_filter_2(X0,X1))
& v10_lattices(k23_filter_2(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(flattening,[],[f35105]) ).
fof(f35109,plain,
! [X0,X1] :
( m2_nat_lat(k23_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(ennf_transformation,[],[f34647]) ).
fof(f35110,plain,
! [X0,X1] :
( m2_nat_lat(k23_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(flattening,[],[f35109]) ).
fof(f35213,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34657]) ).
fof(f35214,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35213]) ).
fof(f35217,plain,
! [X0] :
( k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22779]) ).
fof(f35252,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22780]) ).
fof(f35253,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35252]) ).
fof(f35647,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f35652,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = X0
| v3_struct_0(X0)
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22781]) ).
fof(f35653,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = X0
| v3_struct_0(X0)
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35652]) ).
fof(f35654,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22752]) ).
fof(f35655,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35654]) ).
fof(f35656,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22747]) ).
fof(f35657,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35656]) ).
fof(f35936,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,[],[f31938]) ).
fof(f35937,plain,
! [X0] :
( ! [X1] :
( m2_lattice4(X1,X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35936]) ).
fof(f35968,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34675]) ).
fof(f35969,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35968]) ).
fof(f35972,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34606]) ).
fof(f35973,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35972]) ).
fof(f35978,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1))
& l3_lattices(k8_filter_0(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(ennf_transformation,[],[f21611]) ).
fof(f35979,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1))
& l3_lattices(k8_filter_0(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(flattening,[],[f35978]) ).
fof(f35992,plain,
! [X0] :
( ! [X1] :
( v14_lattices(k8_filter_0(X0,X1))
| ~ v14_lattices(X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21572]) ).
fof(f35993,plain,
! [X0] :
( ! [X1] :
( v14_lattices(k8_filter_0(X0,X1))
| ~ v14_lattices(X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35992]) ).
fof(f36071,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
| ~ m2_nat_lat(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f25570]) ).
fof(f36072,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
| ~ m2_nat_lat(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f36071]) ).
fof(f41150,definition,
! [X1,X0] :
( ( ~ v3_struct_0(k23_filter_2(X0,X1))
& v3_lattices(k23_filter_2(X0,X1))
& v4_lattices(k23_filter_2(X0,X1))
& v5_lattices(k23_filter_2(X0,X1))
& v6_lattices(k23_filter_2(X0,X1))
& v7_lattices(k23_filter_2(X0,X1))
& v8_lattices(k23_filter_2(X0,X1))
& v9_lattices(k23_filter_2(X0,X1))
& v10_lattices(k23_filter_2(X0,X1)) )
| ~ sP3(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f41151,plain,
! [X0,X1] :
( sP3(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(definition_folding,[],[f35106,f41150]) ).
fof(f41166,definition,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP12(X0) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f41167,plain,
! [X0] :
( sP12(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f35655,f41166]) ).
fof(f41437,plain,
( ~ v13_lattices(k23_filter_2(sK198,sK199))
& v13_lattices(sK198)
& m2_filter_2(sK199,sK198)
& ~ v3_struct_0(sK198)
& v10_lattices(sK198)
& l3_lattices(sK198) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK198,sK199]),skolemize(X0,sK198),skolemize(X1,sK199)],[f35028]) ).
fof(f41441,plain,
! [X0] :
( ( ( v14_lattices(X0)
| ~ v13_lattices(k1_lattice2(X0)) )
& ( v13_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35060]) ).
fof(f41442,plain,
! [X0] :
( ( ( v13_lattices(X0)
| ~ v14_lattices(k1_lattice2(X0)) )
& ( v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35062]) ).
fof(f41465,plain,
! [X1,X0] :
( ( ~ v3_struct_0(k23_filter_2(X0,X1))
& v3_lattices(k23_filter_2(X0,X1))
& v4_lattices(k23_filter_2(X0,X1))
& v5_lattices(k23_filter_2(X0,X1))
& v6_lattices(k23_filter_2(X0,X1))
& v7_lattices(k23_filter_2(X0,X1))
& v8_lattices(k23_filter_2(X0,X1))
& v9_lattices(k23_filter_2(X0,X1))
& v10_lattices(k23_filter_2(X0,X1)) )
| ~ sP3(X1,X0) ),
inference(nnf_transformation,[],[f41150]) ).
fof(f41466,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k23_filter_2(X1,X0))
& v3_lattices(k23_filter_2(X1,X0))
& v4_lattices(k23_filter_2(X1,X0))
& v5_lattices(k23_filter_2(X1,X0))
& v6_lattices(k23_filter_2(X1,X0))
& v7_lattices(k23_filter_2(X1,X0))
& v8_lattices(k23_filter_2(X1,X0))
& v9_lattices(k23_filter_2(X1,X0))
& v10_lattices(k23_filter_2(X1,X0)) )
| ~ sP3(X0,X1) ),
inference(rectify,[],[f41465]) ).
fof(f41601,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP12(X0) ),
inference(nnf_transformation,[],[f41166]) ).
fof(f41763,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
| ~ m1_filter_2(X1,k1_lattice2(X0)) )
& ( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35969]) ).
fof(f41764,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_2(X1,X0)
| ~ m1_filter_0(X1,X0) )
& ( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35973]) ).
fof(f43465,plain,
l3_lattices(sK198),
inference(cnf_transformation,[],[f41437]) ).
fof(f43466,plain,
v10_lattices(sK198),
inference(cnf_transformation,[],[f41437]) ).
fof(f43467,plain,
~ v3_struct_0(sK198),
inference(cnf_transformation,[],[f41437]) ).
fof(f43468,plain,
m2_filter_2(sK199,sK198),
inference(cnf_transformation,[],[f41437]) ).
fof(f43469,plain,
v13_lattices(sK198),
inference(cnf_transformation,[],[f41437]) ).
fof(f43470,plain,
~ v13_lattices(k23_filter_2(sK198,sK199)),
inference(cnf_transformation,[],[f41437]) ).
fof(f43493,plain,
! [X0] :
( v13_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f41441]) ).
fof(f43495,plain,
! [X0] :
( v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f41442]) ).
fof(f43576,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35096]) ).
fof(f43577,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35096]) ).
fof(f43582,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| k1_realset1(u1_lattices(X0),X1) = u1_lattices(k23_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35102]) ).
fof(f43583,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| k1_realset1(u2_lattices(X0),X1) = u2_lattices(k23_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35102]) ).
fof(f43584,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| u1_struct_0(k23_filter_2(X0,X1)) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35102]) ).
fof(f43585,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| k8_filter_0(X0,X1) = k23_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35104]) ).
fof(f43586,plain,
! [X0,X1] :
( v10_lattices(k23_filter_2(X1,X0))
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f41466]) ).
fof(f43593,plain,
! [X0,X1] :
( v3_lattices(k23_filter_2(X1,X0))
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f41466]) ).
fof(f43594,plain,
! [X0,X1] :
( ~ v3_struct_0(k23_filter_2(X1,X0))
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f41466]) ).
fof(f43595,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| sP3(X1,X0) ),
inference(cnf_transformation,[],[f41151]) ).
fof(f43609,plain,
! [X0,X1] :
( m2_nat_lat(k23_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(cnf_transformation,[],[f35110]) ).
fof(f43715,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = k1_lattice2(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35214]) ).
fof(f43717,plain,
! [X0] :
( ~ l3_lattices(X0)
| k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
inference(cnf_transformation,[],[f35217]) ).
fof(f43750,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f35253]) ).
fof(f43751,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u2_lattices(X0) = u1_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f35253]) ).
fof(f44242,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35647]) ).
fof(f44248,plain,
! [X0] :
( ~ v3_lattices(X0)
| v3_struct_0(X0)
| k1_lattice2(k1_lattice2(X0)) = X0
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35653]) ).
fof(f44249,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP12(X0) ),
inference(cnf_transformation,[],[f41601]) ).
fof(f44258,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP12(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f41167]) ).
fof(f44260,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35657]) ).
fof(f44954,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,[],[f35937]) ).
fof(f45008,plain,
! [X0,X1] :
( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f41763]) ).
fof(f45011,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f41764]) ).
fof(f45015,plain,
! [X0,X1] :
( l3_lattices(k8_filter_0(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(cnf_transformation,[],[f35979]) ).
fof(f45027,plain,
! [X0,X1] :
( v14_lattices(k8_filter_0(X0,X1))
| ~ v14_lattices(X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35993]) ).
fof(f45136,plain,
! [X0,X1] :
( ~ m2_nat_lat(X1,X0)
| l3_lattices(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36072]) ).
fof(f55189,plain,
( m2_lattice4(sK199,sK198)
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(resolution,[],[f43576,f43468]) ).
fof(f55190,plain,
( m2_lattice4(sK199,sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55189,f43467]) ).
fof(f55191,plain,
( m2_lattice4(sK199,sK198)
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55190,f43466]) ).
fof(f55192,plain,
m2_lattice4(sK199,sK198),
inference(forward_subsumption_resolution,[],[f55191,f43465]) ).
fof(f55193,plain,
( ~ v1_xboole_0(sK199)
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(resolution,[],[f43577,f43468]) ).
fof(f55199,plain,
( ~ v1_xboole_0(sK199)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55193,f43467]) ).
fof(f55200,plain,
( ~ v1_xboole_0(sK199)
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55199,f43466]) ).
fof(f55201,plain,
~ v1_xboole_0(sK199),
inference(forward_subsumption_resolution,[],[f55200,f43465]) ).
fof(f55206,plain,
! [X0,X1] :
( k8_filter_0(k1_lattice2(X0),X1) = k23_filter_2(k1_lattice2(X0),X1)
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f43585,f45008]) ).
fof(f55207,plain,
! [X0,X1] :
( k8_filter_0(k1_lattice2(X0),X1) = k23_filter_2(k1_lattice2(X0),X1)
| ~ v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f55206,f44260]) ).
fof(f55208,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ v10_lattices(k1_lattice2(X0))
| k8_filter_0(k1_lattice2(X0),X1) = k23_filter_2(k1_lattice2(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f55207,f44242]) ).
fof(f55209,plain,
( v1_xboole_0(sK199)
| sK199 = u1_struct_0(k23_filter_2(sK198,sK199))
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(resolution,[],[f43584,f55192]) ).
fof(f55210,plain,
( sK199 = u1_struct_0(k23_filter_2(sK198,sK199))
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55209,f55201]) ).
fof(f55211,plain,
( sK199 = u1_struct_0(k23_filter_2(sK198,sK199))
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55210,f43467]) ).
fof(f55212,plain,
( sK199 = u1_struct_0(k23_filter_2(sK198,sK199))
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55211,f43466]) ).
fof(f55213,plain,
sK199 = u1_struct_0(k23_filter_2(sK198,sK199)),
inference(forward_subsumption_resolution,[],[f55212,f43465]) ).
fof(f55218,definition,
( spl1443_69
<=> l3_lattices(k23_filter_2(sK198,sK199)) ),
introduced(definition,[new_symbols(definition,[spl1443_69])],[avatar_definition]) ).
fof(f55219,plain,
( l3_lattices(k23_filter_2(sK198,sK199))
| ~ spl1443_69 ),
inference(avatar_component_clause,[],[f55218]) ).
fof(f55220,plain,
( ~ l3_lattices(k23_filter_2(sK198,sK199))
| spl1443_69 ),
inference(avatar_component_clause,[],[f55218]) ).
fof(f55222,definition,
( spl1443_70
<=> v10_lattices(k23_filter_2(sK198,sK199)) ),
introduced(definition,[new_symbols(definition,[spl1443_70])],[avatar_definition]) ).
fof(f55223,plain,
( v10_lattices(k23_filter_2(sK198,sK199))
| ~ spl1443_70 ),
inference(avatar_component_clause,[],[f55222]) ).
fof(f55224,plain,
( ~ v10_lattices(k23_filter_2(sK198,sK199))
| spl1443_70 ),
inference(avatar_component_clause,[],[f55222]) ).
fof(f55226,definition,
( spl1443_71
<=> v3_struct_0(k23_filter_2(sK198,sK199)) ),
introduced(definition,[new_symbols(definition,[spl1443_71])],[avatar_definition]) ).
fof(f55227,plain,
( ~ v3_struct_0(k23_filter_2(sK198,sK199))
| spl1443_71 ),
inference(avatar_component_clause,[],[f55226]) ).
fof(f55228,plain,
( v3_struct_0(k23_filter_2(sK198,sK199))
| ~ spl1443_71 ),
inference(avatar_component_clause,[],[f55226]) ).
fof(f55243,plain,
( v3_struct_0(sK198)
| sP12(sK198)
| ~ l3_lattices(sK198) ),
inference(resolution,[],[f44258,f43466]) ).
fof(f55246,plain,
( sP12(sK198)
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55243,f43467]) ).
fof(f55247,plain,
sP12(sK198),
inference(forward_subsumption_resolution,[],[f55246,f43465]) ).
fof(f55255,definition,
( spl1443_75
<=> l3_lattices(k1_lattice2(sK198)) ),
introduced(definition,[new_symbols(definition,[spl1443_75])],[avatar_definition]) ).
fof(f55256,plain,
( l3_lattices(k1_lattice2(sK198))
| ~ spl1443_75 ),
inference(avatar_component_clause,[],[f55255]) ).
fof(f55257,plain,
( ~ l3_lattices(k1_lattice2(sK198))
| spl1443_75 ),
inference(avatar_component_clause,[],[f55255]) ).
fof(f55259,definition,
( spl1443_76
<=> v10_lattices(k1_lattice2(sK198)) ),
introduced(definition,[new_symbols(definition,[spl1443_76])],[avatar_definition]) ).
fof(f55260,plain,
( v10_lattices(k1_lattice2(sK198))
| ~ spl1443_76 ),
inference(avatar_component_clause,[],[f55259]) ).
fof(f55261,plain,
( ~ v10_lattices(k1_lattice2(sK198))
| spl1443_76 ),
inference(avatar_component_clause,[],[f55259]) ).
fof(f55263,definition,
( spl1443_77
<=> v3_struct_0(k1_lattice2(sK198)) ),
introduced(definition,[new_symbols(definition,[spl1443_77])],[avatar_definition]) ).
fof(f55264,plain,
( ~ v3_struct_0(k1_lattice2(sK198))
| spl1443_77 ),
inference(avatar_component_clause,[],[f55263]) ).
fof(f55265,plain,
( v3_struct_0(k1_lattice2(sK198))
| ~ spl1443_77 ),
inference(avatar_component_clause,[],[f55263]) ).
fof(f55283,plain,
( ~ l3_lattices(sK198)
| spl1443_75 ),
inference(resolution,[],[f55257,f44242]) ).
fof(f55284,plain,
( $false
| spl1443_75 ),
inference(forward_subsumption_resolution,[],[f55283,f43465]) ).
fof(f55285,plain,
spl1443_75,
inference(avatar_contradiction_clause,[],[f55284]) ).
fof(f55293,plain,
( v3_struct_0(sK198)
| ~ l3_lattices(sK198)
| ~ spl1443_77 ),
inference(resolution,[],[f55265,f44260]) ).
fof(f55294,plain,
( ~ l3_lattices(sK198)
| ~ spl1443_77 ),
inference(forward_subsumption_resolution,[],[f55293,f43467]) ).
fof(f55295,plain,
( $false
| ~ spl1443_77 ),
inference(forward_subsumption_resolution,[],[f55294,f43465]) ).
fof(f55296,plain,
~ spl1443_77,
inference(avatar_contradiction_clause,[],[f55295]) ).
fof(f55319,plain,
( v1_xboole_0(sK199)
| k1_realset1(u2_lattices(sK198),sK199) = u2_lattices(k23_filter_2(sK198,sK199))
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(resolution,[],[f43583,f55192]) ).
fof(f55320,plain,
( k1_realset1(u2_lattices(sK198),sK199) = u2_lattices(k23_filter_2(sK198,sK199))
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55319,f55201]) ).
fof(f55321,plain,
( k1_realset1(u2_lattices(sK198),sK199) = u2_lattices(k23_filter_2(sK198,sK199))
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55320,f43467]) ).
fof(f55322,plain,
( k1_realset1(u2_lattices(sK198),sK199) = u2_lattices(k23_filter_2(sK198,sK199))
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55321,f43466]) ).
fof(f55323,plain,
k1_realset1(u2_lattices(sK198),sK199) = u2_lattices(k23_filter_2(sK198,sK199)),
inference(forward_subsumption_resolution,[],[f55322,f43465]) ).
fof(f55332,plain,
! [X0,X1] :
( m1_filter_0(X0,k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f45011,f45008]) ).
fof(f55333,plain,
! [X0,X1] :
( m1_filter_0(X0,k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f55332,f44260]) ).
fof(f55334,plain,
! [X0,X1] :
( m1_filter_0(X0,k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f55333,f44242]) ).
fof(f55336,plain,
! [X0,X1] :
( ~ v10_lattices(k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| m2_lattice4(X1,k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) ),
inference(resolution,[],[f55334,f44954]) ).
fof(f55337,plain,
! [X0,X1] :
( ~ v10_lattices(k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| m2_lattice4(X1,k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) ),
inference(duplicate_literal_removal,[],[f55336]) ).
fof(f55339,plain,
! [X0,X1] :
( ~ v10_lattices(k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| m2_lattice4(X1,k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) ),
inference(forward_subsumption_resolution,[],[f55337,f44260]) ).
fof(f55340,plain,
! [X0,X1] :
( m2_lattice4(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(k1_lattice2(X0)) ),
inference(forward_subsumption_resolution,[],[f55339,f44242]) ).
fof(f55341,plain,
( ~ sP12(sK198)
| spl1443_76 ),
inference(resolution,[],[f44249,f55261]) ).
fof(f55346,plain,
( $false
| spl1443_76 ),
inference(forward_subsumption_resolution,[],[f55341,f55247]) ).
fof(f55347,plain,
spl1443_76,
inference(avatar_contradiction_clause,[],[f55346]) ).
fof(f55386,plain,
( ~ v10_lattices(k1_lattice2(sK198))
| k8_filter_0(k1_lattice2(sK198),sK199) = k23_filter_2(k1_lattice2(sK198),sK199)
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(resolution,[],[f55208,f43468]) ).
fof(f55391,plain,
( k8_filter_0(k1_lattice2(sK198),sK199) = k23_filter_2(k1_lattice2(sK198),sK199)
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ spl1443_76 ),
inference(forward_subsumption_resolution,[],[f55386,f55260]) ).
fof(f55393,plain,
( k8_filter_0(k1_lattice2(sK198),sK199) = k23_filter_2(k1_lattice2(sK198),sK199)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ spl1443_76 ),
inference(forward_subsumption_resolution,[],[f55391,f43467]) ).
fof(f55395,plain,
( k8_filter_0(k1_lattice2(sK198),sK199) = k23_filter_2(k1_lattice2(sK198),sK199)
| ~ l3_lattices(sK198)
| ~ spl1443_76 ),
inference(forward_subsumption_resolution,[],[f55393,f43466]) ).
fof(f55405,plain,
( k8_filter_0(k1_lattice2(sK198),sK199) = k23_filter_2(k1_lattice2(sK198),sK199)
| ~ spl1443_76 ),
inference(forward_subsumption_resolution,[],[f55395,f43465]) ).
fof(f55408,plain,
( v10_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ sP3(sK199,k1_lattice2(sK198))
| ~ spl1443_76 ),
inference(superposition,[],[f43586,f55405]) ).
fof(f55410,definition,
( spl1443_85
<=> sP3(sK199,k1_lattice2(sK198)) ),
introduced(definition,[new_symbols(definition,[spl1443_85])],[avatar_definition]) ).
fof(f55411,plain,
( sP3(sK199,k1_lattice2(sK198))
| ~ spl1443_85 ),
inference(avatar_component_clause,[],[f55410]) ).
fof(f55412,plain,
( ~ sP3(sK199,k1_lattice2(sK198))
| spl1443_85 ),
inference(avatar_component_clause,[],[f55410]) ).
fof(f55414,definition,
( spl1443_86
<=> v10_lattices(k8_filter_0(k1_lattice2(sK198),sK199)) ),
introduced(definition,[new_symbols(definition,[spl1443_86])],[avatar_definition]) ).
fof(f55416,plain,
( v10_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_86 ),
inference(avatar_component_clause,[],[f55414]) ).
fof(f55417,plain,
( ~ spl1443_85
| spl1443_86
| ~ spl1443_76 ),
inference(avatar_split_clause,[],[f55408,f55259,f55414,f55410]) ).
fof(f55430,definition,
( spl1443_88
<=> m2_lattice4(sK199,k1_lattice2(sK198)) ),
introduced(definition,[new_symbols(definition,[spl1443_88])],[avatar_definition]) ).
fof(f55431,plain,
( m2_lattice4(sK199,k1_lattice2(sK198))
| ~ spl1443_88 ),
inference(avatar_component_clause,[],[f55430]) ).
fof(f55432,plain,
( ~ m2_lattice4(sK199,k1_lattice2(sK198))
| spl1443_88 ),
inference(avatar_component_clause,[],[f55430]) ).
fof(f55437,plain,
( ~ v3_struct_0(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ sP3(sK199,k1_lattice2(sK198))
| ~ spl1443_76 ),
inference(superposition,[],[f43594,f55405]) ).
fof(f55493,plain,
( v1_xboole_0(sK199)
| k1_realset1(u1_lattices(sK198),sK199) = u1_lattices(k23_filter_2(sK198,sK199))
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(resolution,[],[f43582,f55192]) ).
fof(f55494,plain,
( k1_realset1(u1_lattices(sK198),sK199) = u1_lattices(k23_filter_2(sK198,sK199))
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55493,f55201]) ).
fof(f55495,plain,
( k1_realset1(u1_lattices(sK198),sK199) = u1_lattices(k23_filter_2(sK198,sK199))
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55494,f43467]) ).
fof(f55496,plain,
( k1_realset1(u1_lattices(sK198),sK199) = u1_lattices(k23_filter_2(sK198,sK199))
| ~ l3_lattices(sK198) ),
inference(forward_subsumption_resolution,[],[f55495,f43466]) ).
fof(f55497,plain,
k1_realset1(u1_lattices(sK198),sK199) = u1_lattices(k23_filter_2(sK198,sK199)),
inference(forward_subsumption_resolution,[],[f55496,f43465]) ).
fof(f55609,plain,
( v3_struct_0(sK198)
| u1_lattices(sK198) = u2_lattices(k1_lattice2(sK198)) ),
inference(resolution,[],[f43750,f43465]) ).
fof(f55613,plain,
u1_lattices(sK198) = u2_lattices(k1_lattice2(sK198)),
inference(forward_subsumption_resolution,[],[f55609,f43467]) ).
fof(f55620,definition,
( spl1443_92
<=> v14_lattices(k1_lattice2(sK198)) ),
introduced(definition,[new_symbols(definition,[spl1443_92])],[avatar_definition]) ).
fof(f55621,plain,
( v14_lattices(k1_lattice2(sK198))
| ~ spl1443_92 ),
inference(avatar_component_clause,[],[f55620]) ).
fof(f55622,plain,
( ~ v14_lattices(k1_lattice2(sK198))
| spl1443_92 ),
inference(avatar_component_clause,[],[f55620]) ).
fof(f55627,plain,
( ~ v13_lattices(sK198)
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| spl1443_92 ),
inference(resolution,[],[f55622,f43495]) ).
fof(f55628,plain,
( v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| spl1443_92 ),
inference(forward_subsumption_resolution,[],[f55627,f43469]) ).
fof(f55629,plain,
( ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| spl1443_92 ),
inference(forward_subsumption_resolution,[],[f55628,f43467]) ).
fof(f55630,plain,
( ~ l3_lattices(sK198)
| spl1443_92 ),
inference(forward_subsumption_resolution,[],[f55629,f43466]) ).
fof(f55631,plain,
( $false
| spl1443_92 ),
inference(forward_subsumption_resolution,[],[f55630,f43465]) ).
fof(f55632,plain,
spl1443_92,
inference(avatar_contradiction_clause,[],[f55631]) ).
fof(f55801,plain,
! [X0,X1] :
( v3_struct_0(k23_filter_2(X0,X1))
| k23_filter_2(X0,X1) = k1_lattice2(k1_lattice2(k23_filter_2(X0,X1)))
| ~ l3_lattices(k23_filter_2(X0,X1))
| ~ sP3(X1,X0) ),
inference(resolution,[],[f44248,f43593]) ).
fof(f55804,plain,
! [X0,X1] :
( ~ l3_lattices(k23_filter_2(X0,X1))
| k23_filter_2(X0,X1) = k1_lattice2(k1_lattice2(k23_filter_2(X0,X1)))
| ~ sP3(X1,X0) ),
inference(forward_subsumption_resolution,[],[f55801,f43594]) ).
fof(f55842,plain,
( ~ m2_filter_2(sK199,sK198)
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ v10_lattices(k1_lattice2(sK198))
| spl1443_88 ),
inference(resolution,[],[f55340,f55432]) ).
fof(f55846,plain,
( v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ v10_lattices(k1_lattice2(sK198))
| spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55842,f43468]) ).
fof(f55850,plain,
( ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ v10_lattices(k1_lattice2(sK198))
| spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55846,f43467]) ).
fof(f55854,plain,
( ~ l3_lattices(sK198)
| ~ v10_lattices(k1_lattice2(sK198))
| spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55850,f43466]) ).
fof(f55858,plain,
( ~ v10_lattices(k1_lattice2(sK198))
| spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55854,f43465]) ).
fof(f55859,plain,
( $false
| ~ spl1443_76
| spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55858,f55260]) ).
fof(f55860,plain,
( ~ spl1443_76
| spl1443_88 ),
inference(avatar_contradiction_clause,[],[f55859]) ).
fof(f55868,plain,
( v1_xboole_0(sK199)
| k1_realset1(u1_lattices(k1_lattice2(sK198)),sK199) = u1_lattices(k23_filter_2(k1_lattice2(sK198),sK199))
| v3_struct_0(k1_lattice2(sK198))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ spl1443_88 ),
inference(resolution,[],[f55431,f43582]) ).
fof(f55869,plain,
( v1_xboole_0(sK199)
| k1_realset1(u2_lattices(k1_lattice2(sK198)),sK199) = u2_lattices(k23_filter_2(k1_lattice2(sK198),sK199))
| v3_struct_0(k1_lattice2(sK198))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ spl1443_88 ),
inference(resolution,[],[f55431,f43583]) ).
fof(f55870,plain,
( v1_xboole_0(sK199)
| sK199 = u1_struct_0(k23_filter_2(k1_lattice2(sK198),sK199))
| v3_struct_0(k1_lattice2(sK198))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ spl1443_88 ),
inference(resolution,[],[f55431,f43584]) ).
fof(f55871,plain,
( sK199 = u1_struct_0(k23_filter_2(k1_lattice2(sK198),sK199))
| v3_struct_0(k1_lattice2(sK198))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55870,f55201]) ).
fof(f55872,plain,
( k1_realset1(u2_lattices(k1_lattice2(sK198)),sK199) = u2_lattices(k23_filter_2(k1_lattice2(sK198),sK199))
| v3_struct_0(k1_lattice2(sK198))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55869,f55201]) ).
fof(f55873,plain,
( k1_realset1(u1_lattices(k1_lattice2(sK198)),sK199) = u1_lattices(k23_filter_2(k1_lattice2(sK198),sK199))
| v3_struct_0(k1_lattice2(sK198))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55868,f55201]) ).
fof(f55874,plain,
( sK199 = u1_struct_0(k23_filter_2(k1_lattice2(sK198),sK199))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55871,f55264]) ).
fof(f55875,plain,
( k1_realset1(u2_lattices(k1_lattice2(sK198)),sK199) = u2_lattices(k23_filter_2(k1_lattice2(sK198),sK199))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55872,f55264]) ).
fof(f55876,plain,
( k1_realset1(u1_lattices(k1_lattice2(sK198)),sK199) = u1_lattices(k23_filter_2(k1_lattice2(sK198),sK199))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55873,f55264]) ).
fof(f55877,plain,
( sK199 = u1_struct_0(k23_filter_2(k1_lattice2(sK198),sK199))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55874,f55260]) ).
fof(f55878,plain,
( k1_realset1(u2_lattices(k1_lattice2(sK198)),sK199) = u2_lattices(k23_filter_2(k1_lattice2(sK198),sK199))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55875,f55260]) ).
fof(f55879,plain,
( k1_realset1(u1_lattices(k1_lattice2(sK198)),sK199) = u1_lattices(k23_filter_2(k1_lattice2(sK198),sK199))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55876,f55260]) ).
fof(f55880,plain,
( sK199 = u1_struct_0(k23_filter_2(k1_lattice2(sK198),sK199))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55877,f55256]) ).
fof(f55881,plain,
( k1_realset1(u2_lattices(k1_lattice2(sK198)),sK199) = u2_lattices(k23_filter_2(k1_lattice2(sK198),sK199))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55878,f55256]) ).
fof(f55882,plain,
( k1_realset1(u1_lattices(k1_lattice2(sK198)),sK199) = u1_lattices(k23_filter_2(k1_lattice2(sK198),sK199))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f55879,f55256]) ).
fof(f55883,plain,
( sK199 = u1_struct_0(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_demodulation,[],[f55880,f55405]) ).
fof(f55884,plain,
( k1_realset1(u2_lattices(k1_lattice2(sK198)),sK199) = u2_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_demodulation,[],[f55881,f55405]) ).
fof(f55885,plain,
( k1_realset1(u1_lattices(k1_lattice2(sK198)),sK199) = u1_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_demodulation,[],[f55882,f55405]) ).
fof(f55886,plain,
( k1_realset1(u1_lattices(sK198),sK199) = u2_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_demodulation,[],[f55884,f55613]) ).
fof(f55887,plain,
( u1_lattices(k23_filter_2(sK198,sK199)) = u2_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_demodulation,[],[f55886,f55497]) ).
fof(f55905,definition,
( spl1443_98
<=> l3_lattices(k8_filter_0(k1_lattice2(sK198),sK199)) ),
introduced(definition,[new_symbols(definition,[spl1443_98])],[avatar_definition]) ).
fof(f55906,plain,
( l3_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_98 ),
inference(avatar_component_clause,[],[f55905]) ).
fof(f55907,plain,
( ~ l3_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| spl1443_98 ),
inference(avatar_component_clause,[],[f55905]) ).
fof(f55909,definition,
( spl1443_99
<=> v3_struct_0(k8_filter_0(k1_lattice2(sK198),sK199)) ),
introduced(definition,[new_symbols(definition,[spl1443_99])],[avatar_definition]) ).
fof(f55910,plain,
( ~ v3_struct_0(k8_filter_0(k1_lattice2(sK198),sK199))
| spl1443_99 ),
inference(avatar_component_clause,[],[f55909]) ).
fof(f55911,plain,
( v3_struct_0(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_99 ),
inference(avatar_component_clause,[],[f55909]) ).
fof(f55977,plain,
( v3_struct_0(k1_lattice2(sK198))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ m1_filter_0(sK199,k1_lattice2(sK198))
| spl1443_98 ),
inference(resolution,[],[f55907,f45015]) ).
fof(f55978,plain,
( ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ m1_filter_0(sK199,k1_lattice2(sK198))
| spl1443_77
| spl1443_98 ),
inference(forward_subsumption_resolution,[],[f55977,f55264]) ).
fof(f55979,plain,
( ~ l3_lattices(k1_lattice2(sK198))
| ~ m1_filter_0(sK199,k1_lattice2(sK198))
| ~ spl1443_76
| spl1443_77
| spl1443_98 ),
inference(forward_subsumption_resolution,[],[f55978,f55260]) ).
fof(f55980,plain,
( ~ m1_filter_0(sK199,k1_lattice2(sK198))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| spl1443_98 ),
inference(forward_subsumption_resolution,[],[f55979,f55256]) ).
fof(f55981,plain,
( ~ v10_lattices(k1_lattice2(sK198))
| ~ m2_filter_2(sK199,sK198)
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| spl1443_98 ),
inference(resolution,[],[f55980,f55334]) ).
fof(f55982,plain,
( ~ m2_filter_2(sK199,sK198)
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| spl1443_98 ),
inference(forward_subsumption_resolution,[],[f55981,f55260]) ).
fof(f55983,plain,
( v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| spl1443_98 ),
inference(forward_subsumption_resolution,[],[f55982,f43468]) ).
fof(f55984,plain,
( ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| spl1443_98 ),
inference(forward_subsumption_resolution,[],[f55983,f43467]) ).
fof(f55985,plain,
( ~ l3_lattices(sK198)
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| spl1443_98 ),
inference(forward_subsumption_resolution,[],[f55984,f43466]) ).
fof(f55986,plain,
( $false
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| spl1443_98 ),
inference(forward_subsumption_resolution,[],[f55985,f43465]) ).
fof(f55987,plain,
( ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| spl1443_98 ),
inference(avatar_contradiction_clause,[],[f55986]) ).
fof(f56058,plain,
( v3_struct_0(sK198)
| u2_lattices(sK198) = u1_lattices(k1_lattice2(sK198)) ),
inference(resolution,[],[f43751,f43465]) ).
fof(f56064,plain,
u2_lattices(sK198) = u1_lattices(k1_lattice2(sK198)),
inference(forward_subsumption_resolution,[],[f56058,f43467]) ).
fof(f56066,plain,
( k1_realset1(u2_lattices(sK198),sK199) = u1_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(superposition,[],[f55885,f56064]) ).
fof(f56067,plain,
( u2_lattices(k23_filter_2(sK198,sK199)) = u1_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_demodulation,[],[f56066,f55323]) ).
fof(f56242,plain,
( v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| v1_xboole_0(sK199)
| sP3(sK199,sK198) ),
inference(resolution,[],[f43595,f55192]) ).
fof(f56243,plain,
( v3_struct_0(k1_lattice2(sK198))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| v1_xboole_0(sK199)
| sP3(sK199,k1_lattice2(sK198))
| ~ spl1443_88 ),
inference(resolution,[],[f43595,f55431]) ).
fof(f56250,plain,
( ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| v1_xboole_0(sK199)
| sP3(sK199,k1_lattice2(sK198))
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f56243,f55264]) ).
fof(f56251,plain,
( ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| v1_xboole_0(sK199)
| sP3(sK199,sK198) ),
inference(forward_subsumption_resolution,[],[f56242,f43467]) ).
fof(f56253,plain,
( ~ l3_lattices(k1_lattice2(sK198))
| v1_xboole_0(sK199)
| sP3(sK199,k1_lattice2(sK198))
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f56250,f55260]) ).
fof(f56254,plain,
( ~ l3_lattices(sK198)
| v1_xboole_0(sK199)
| sP3(sK199,sK198) ),
inference(forward_subsumption_resolution,[],[f56251,f43466]) ).
fof(f56256,plain,
( v1_xboole_0(sK199)
| sP3(sK199,k1_lattice2(sK198))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f56253,f55256]) ).
fof(f56257,plain,
( v1_xboole_0(sK199)
| sP3(sK199,sK198) ),
inference(forward_subsumption_resolution,[],[f56254,f43465]) ).
fof(f56258,plain,
( sP3(sK199,k1_lattice2(sK198))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f56256,f55201]) ).
fof(f56259,plain,
sP3(sK199,sK198),
inference(forward_subsumption_resolution,[],[f56257,f55201]) ).
fof(f56260,plain,
( $false
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| spl1443_85
| ~ spl1443_88 ),
inference(forward_subsumption_resolution,[],[f56258,f55412]) ).
fof(f56261,plain,
( ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| spl1443_85
| ~ spl1443_88 ),
inference(avatar_contradiction_clause,[],[f56260]) ).
fof(f56262,plain,
( ~ sP3(sK199,k1_lattice2(sK198))
| ~ spl1443_76
| ~ spl1443_99 ),
inference(forward_subsumption_resolution,[],[f55437,f55911]) ).
fof(f56271,plain,
( $false
| ~ spl1443_76
| ~ spl1443_85
| ~ spl1443_99 ),
inference(forward_subsumption_resolution,[],[f56262,f55411]) ).
fof(f56272,plain,
( ~ spl1443_76
| ~ spl1443_85
| ~ spl1443_99 ),
inference(avatar_contradiction_clause,[],[f56271]) ).
fof(f56640,plain,
! [X0,X1] :
( l3_lattices(k23_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(resolution,[],[f45136,f43609]) ).
fof(f56643,plain,
! [X0,X1] :
( l3_lattices(k23_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(duplicate_literal_removal,[],[f56640]) ).
fof(f56644,plain,
( v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| v1_xboole_0(sK199)
| ~ m2_lattice4(sK199,sK198)
| spl1443_69 ),
inference(resolution,[],[f56643,f55220]) ).
fof(f56659,plain,
( ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| v1_xboole_0(sK199)
| ~ m2_lattice4(sK199,sK198)
| spl1443_69 ),
inference(forward_subsumption_resolution,[],[f56644,f43467]) ).
fof(f56660,plain,
( ~ l3_lattices(sK198)
| v1_xboole_0(sK199)
| ~ m2_lattice4(sK199,sK198)
| spl1443_69 ),
inference(forward_subsumption_resolution,[],[f56659,f43466]) ).
fof(f56661,plain,
( v1_xboole_0(sK199)
| ~ m2_lattice4(sK199,sK198)
| spl1443_69 ),
inference(forward_subsumption_resolution,[],[f56660,f43465]) ).
fof(f56662,plain,
( ~ m2_lattice4(sK199,sK198)
| spl1443_69 ),
inference(forward_subsumption_resolution,[],[f56661,f55201]) ).
fof(f56663,plain,
( $false
| spl1443_69 ),
inference(forward_subsumption_resolution,[],[f56662,f55192]) ).
fof(f56664,plain,
spl1443_69,
inference(avatar_contradiction_clause,[],[f56663]) ).
fof(f56696,plain,
( ~ sP3(sK199,sK198)
| ~ spl1443_71 ),
inference(resolution,[],[f55228,f43594]) ).
fof(f56697,plain,
( $false
| ~ spl1443_71 ),
inference(forward_subsumption_resolution,[],[f56696,f56259]) ).
fof(f56698,plain,
~ spl1443_71,
inference(avatar_contradiction_clause,[],[f56697]) ).
fof(f56699,plain,
( ~ sP3(sK199,sK198)
| spl1443_70 ),
inference(resolution,[],[f55224,f43586]) ).
fof(f56700,plain,
( $false
| spl1443_70 ),
inference(forward_subsumption_resolution,[],[f56699,f56259]) ).
fof(f56701,plain,
spl1443_70,
inference(avatar_contradiction_clause,[],[f56700]) ).
fof(f56745,plain,
( k23_filter_2(sK198,sK199) = k1_lattice2(k1_lattice2(k23_filter_2(sK198,sK199)))
| ~ sP3(sK199,sK198)
| ~ spl1443_69 ),
inference(resolution,[],[f55219,f55804]) ).
fof(f56758,plain,
( k23_filter_2(sK198,sK199) = k1_lattice2(k1_lattice2(k23_filter_2(sK198,sK199)))
| ~ spl1443_69 ),
inference(forward_subsumption_resolution,[],[f56745,f56259]) ).
fof(f56760,plain,
( v3_struct_0(k23_filter_2(sK198,sK199))
| k1_lattice2(k1_lattice2(k23_filter_2(sK198,sK199))) = g3_lattices(u1_struct_0(k23_filter_2(sK198,sK199)),u2_lattices(k23_filter_2(sK198,sK199)),u1_lattices(k23_filter_2(sK198,sK199)))
| ~ l3_lattices(k23_filter_2(sK198,sK199))
| ~ spl1443_70 ),
inference(resolution,[],[f55223,f43715]) ).
fof(f56778,plain,
( k1_lattice2(k1_lattice2(k23_filter_2(sK198,sK199))) = g3_lattices(u1_struct_0(k23_filter_2(sK198,sK199)),u2_lattices(k23_filter_2(sK198,sK199)),u1_lattices(k23_filter_2(sK198,sK199)))
| ~ l3_lattices(k23_filter_2(sK198,sK199))
| ~ spl1443_70
| spl1443_71 ),
inference(forward_subsumption_resolution,[],[f56760,f55227]) ).
fof(f56787,plain,
( k1_lattice2(k1_lattice2(k23_filter_2(sK198,sK199))) = g3_lattices(u1_struct_0(k23_filter_2(sK198,sK199)),u2_lattices(k23_filter_2(sK198,sK199)),u1_lattices(k23_filter_2(sK198,sK199)))
| ~ spl1443_69
| ~ spl1443_70
| spl1443_71 ),
inference(forward_subsumption_resolution,[],[f56778,f55219]) ).
fof(f56791,plain,
( k1_lattice2(k1_lattice2(k23_filter_2(sK198,sK199))) = g3_lattices(sK199,u2_lattices(k23_filter_2(sK198,sK199)),u1_lattices(k23_filter_2(sK198,sK199)))
| ~ spl1443_69
| ~ spl1443_70
| spl1443_71 ),
inference(forward_demodulation,[],[f56787,f55213]) ).
fof(f56792,plain,
( k23_filter_2(sK198,sK199) = g3_lattices(sK199,u2_lattices(k23_filter_2(sK198,sK199)),u1_lattices(k23_filter_2(sK198,sK199)))
| ~ spl1443_69
| ~ spl1443_70
| spl1443_71 ),
inference(forward_demodulation,[],[f56791,f56758]) ).
fof(f58138,definition,
( spl1443_182
<=> v14_lattices(k8_filter_0(k1_lattice2(sK198),sK199)) ),
introduced(definition,[new_symbols(definition,[spl1443_182])],[avatar_definition]) ).
fof(f58139,plain,
( v14_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_182 ),
inference(avatar_component_clause,[],[f58138]) ).
fof(f58140,plain,
( ~ v14_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| spl1443_182 ),
inference(avatar_component_clause,[],[f58138]) ).
fof(f58149,plain,
( ~ v14_lattices(k1_lattice2(sK198))
| ~ m1_filter_0(sK199,k1_lattice2(sK198))
| v3_struct_0(k1_lattice2(sK198))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| spl1443_182 ),
inference(resolution,[],[f58140,f45027]) ).
fof(f58150,plain,
( ~ m1_filter_0(sK199,k1_lattice2(sK198))
| v3_struct_0(k1_lattice2(sK198))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ spl1443_92
| spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58149,f55621]) ).
fof(f58151,plain,
( ~ m1_filter_0(sK199,k1_lattice2(sK198))
| ~ v10_lattices(k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| spl1443_77
| ~ spl1443_92
| spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58150,f55264]) ).
fof(f58152,plain,
( ~ m1_filter_0(sK199,k1_lattice2(sK198))
| ~ l3_lattices(k1_lattice2(sK198))
| ~ spl1443_76
| spl1443_77
| ~ spl1443_92
| spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58151,f55260]) ).
fof(f58153,plain,
( ~ m1_filter_0(sK199,k1_lattice2(sK198))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_92
| spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58152,f55256]) ).
fof(f58154,plain,
( ~ v10_lattices(k1_lattice2(sK198))
| ~ m2_filter_2(sK199,sK198)
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_92
| spl1443_182 ),
inference(resolution,[],[f58153,f55334]) ).
fof(f58155,plain,
( ~ m2_filter_2(sK199,sK198)
| v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_92
| spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58154,f55260]) ).
fof(f58156,plain,
( v3_struct_0(sK198)
| ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_92
| spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58155,f43468]) ).
fof(f58157,plain,
( ~ v10_lattices(sK198)
| ~ l3_lattices(sK198)
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_92
| spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58156,f43467]) ).
fof(f58158,plain,
( ~ l3_lattices(sK198)
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_92
| spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58157,f43466]) ).
fof(f58159,plain,
( $false
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_92
| spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58158,f43465]) ).
fof(f58160,plain,
( ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_92
| spl1443_182 ),
inference(avatar_contradiction_clause,[],[f58159]) ).
fof(f58279,plain,
( k1_lattice2(k8_filter_0(k1_lattice2(sK198),sK199)) = g3_lattices(u1_struct_0(k8_filter_0(k1_lattice2(sK198),sK199)),u1_lattices(k8_filter_0(k1_lattice2(sK198),sK199)),u2_lattices(k8_filter_0(k1_lattice2(sK198),sK199)))
| ~ spl1443_98 ),
inference(resolution,[],[f55906,f43717]) ).
fof(f58288,plain,
( k1_lattice2(k8_filter_0(k1_lattice2(sK198),sK199)) = g3_lattices(u1_struct_0(k8_filter_0(k1_lattice2(sK198),sK199)),u1_lattices(k8_filter_0(k1_lattice2(sK198),sK199)),u1_lattices(k23_filter_2(sK198,sK199)))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88
| ~ spl1443_98 ),
inference(forward_demodulation,[],[f58279,f55887]) ).
fof(f58292,plain,
( k1_lattice2(k8_filter_0(k1_lattice2(sK198),sK199)) = g3_lattices(u1_struct_0(k8_filter_0(k1_lattice2(sK198),sK199)),u2_lattices(k23_filter_2(sK198,sK199)),u1_lattices(k23_filter_2(sK198,sK199)))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88
| ~ spl1443_98 ),
inference(forward_demodulation,[],[f58288,f56067]) ).
fof(f58293,plain,
( k1_lattice2(k8_filter_0(k1_lattice2(sK198),sK199)) = g3_lattices(sK199,u2_lattices(k23_filter_2(sK198,sK199)),u1_lattices(k23_filter_2(sK198,sK199)))
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88
| ~ spl1443_98 ),
inference(forward_demodulation,[],[f58292,f55883]) ).
fof(f58294,plain,
( k23_filter_2(sK198,sK199) = k1_lattice2(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_69
| ~ spl1443_70
| spl1443_71
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88
| ~ spl1443_98 ),
inference(forward_demodulation,[],[f58293,f56792]) ).
fof(f58295,plain,
( v13_lattices(k23_filter_2(sK198,sK199))
| ~ v14_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| v3_struct_0(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ v10_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ l3_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_69
| ~ spl1443_70
| spl1443_71
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88
| ~ spl1443_98 ),
inference(superposition,[],[f43493,f58294]) ).
fof(f58324,plain,
( ~ v14_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| v3_struct_0(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ v10_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ l3_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_69
| ~ spl1443_70
| spl1443_71
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88
| ~ spl1443_98 ),
inference(forward_subsumption_resolution,[],[f58295,f43470]) ).
fof(f58331,plain,
( v3_struct_0(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ v10_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ l3_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_69
| ~ spl1443_70
| spl1443_71
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88
| ~ spl1443_98
| ~ spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58324,f58139]) ).
fof(f58338,plain,
( ~ v10_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ l3_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_69
| ~ spl1443_70
| spl1443_71
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_88
| ~ spl1443_98
| spl1443_99
| ~ spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58331,f55910]) ).
fof(f58344,plain,
( ~ l3_lattices(k8_filter_0(k1_lattice2(sK198),sK199))
| ~ spl1443_69
| ~ spl1443_70
| spl1443_71
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_86
| ~ spl1443_88
| ~ spl1443_98
| spl1443_99
| ~ spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58338,f55416]) ).
fof(f58345,plain,
( $false
| ~ spl1443_69
| ~ spl1443_70
| spl1443_71
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_86
| ~ spl1443_88
| ~ spl1443_98
| spl1443_99
| ~ spl1443_182 ),
inference(forward_subsumption_resolution,[],[f58344,f55906]) ).
fof(f58346,plain,
( ~ spl1443_69
| ~ spl1443_70
| spl1443_71
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_86
| ~ spl1443_88
| ~ spl1443_98
| spl1443_99
| ~ spl1443_182 ),
inference(avatar_contradiction_clause,[],[f58345]) ).
cnf(s56,plain,
spl1443_75,
inference(sat_conversion,[],[f55285]) ).
cnf(s58,plain,
~ spl1443_77,
inference(sat_conversion,[],[f55296]) ).
cnf(s59,plain,
spl1443_76,
inference(sat_conversion,[],[f55347]) ).
cnf(s61,plain,
( ~ spl1443_76
| ~ spl1443_85
| spl1443_86 ),
inference(sat_conversion,[],[f55417]) ).
cnf(s66,plain,
spl1443_92,
inference(sat_conversion,[],[f55632]) ).
cnf(s69,plain,
( ~ spl1443_76
| spl1443_88 ),
inference(sat_conversion,[],[f55860]) ).
cnf(s83,plain,
( ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| spl1443_98 ),
inference(sat_conversion,[],[f55987]) ).
cnf(s88,plain,
( ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| spl1443_85
| ~ spl1443_88 ),
inference(sat_conversion,[],[f56261]) ).
cnf(s89,plain,
( ~ spl1443_76
| ~ spl1443_85
| ~ spl1443_99 ),
inference(sat_conversion,[],[f56272]) ).
cnf(s92,plain,
spl1443_69,
inference(sat_conversion,[],[f56664]) ).
cnf(s96,plain,
~ spl1443_71,
inference(sat_conversion,[],[f56698]) ).
cnf(s97,plain,
spl1443_70,
inference(sat_conversion,[],[f56701]) ).
cnf(s150,plain,
( ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_92
| spl1443_182 ),
inference(sat_conversion,[],[f58160]) ).
cnf(s160,plain,
( ~ spl1443_69
| ~ spl1443_70
| spl1443_71
| ~ spl1443_75
| ~ spl1443_76
| spl1443_77
| ~ spl1443_86
| ~ spl1443_88
| ~ spl1443_98
| spl1443_99
| ~ spl1443_182 ),
inference(sat_conversion,[],[f58346]) ).
cnf(s185,plain,
spl1443_88,
inference(rat,[],[s69,s59]) ).
cnf(s190,plain,
spl1443_182,
inference(rat,[],[s150,s58,s66,s59,s56]) ).
cnf(s194,plain,
spl1443_85,
inference(rat,[],[s88,s185,s58,s59,s56]) ).
cnf(s195,plain,
spl1443_98,
inference(rat,[],[s83,s58,s59,s56]) ).
cnf(s199,plain,
~ spl1443_99,
inference(rat,[],[s89,s59,s194]) ).
cnf(s201,plain,
spl1443_86,
inference(rat,[],[s61,s59,s194]) ).
cnf(s202,plain,
$false,
inference(rat,[],[s160,s190,s199,s56,s185,s58,s59,s92,s96,s97,s195,s201]) ).
fof(f58347,plain,
$false,
inference(avatar_sat_refutation,[],[s202]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT333+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.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 14:43:39 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 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.70/5.33 % (881615)Detected formulas, will run a generic FOF schedule.
% 18.70/5.33 % (881621)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=96283103:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 18.70/5.33 % (881625)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3895430226:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 18.70/5.33 % (881623)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2121236235:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 18.70/5.33 % (881626)dis-21_1_sil=8000:lcm=predicate:random_seed=4075001185:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2978 on theBenchmark for (2978ds/129Mi)
% 18.70/5.33 % (881620)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=2360081783:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 18.70/5.33 % (881622)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=3769429212:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 18.70/5.33 % (881624)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2468773371:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 18.70/5.33 % (881625)Instruction limit reached!
% 18.70/5.33 % (881625)------------------------------
% 18.70/5.33 % (881625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/5.33 % (881625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/5.33 % (881625)CaDiCaL version: 2.1.3
% 18.70/5.33 % (881625)Termination reason: Instruction limit
% 18.70/5.33 % (881625)Termination phase: Property scanning
% 18.70/5.33 % (881625)Time elapsed: 0.060 s
% 18.70/5.33 % (881625)Peak memory usage: 136 MB
% 18.70/5.33 % (881625)Instructions burned: 139 (million)
% 18.70/5.33 % (881623)Instruction limit reached!
% 18.70/5.33 % (881623)------------------------------
% 18.70/5.33 % (881623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/5.33 % (881623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/5.33 % (881623)CaDiCaL version: 2.1.3
% 18.70/5.33 % (881623)Termination reason: Instruction limit
% 18.70/5.33 % (881623)Termination phase: SInE selection
% 18.70/5.33 % (881623)Time elapsed: 0.080 s
% 18.70/5.33 % (881623)Peak memory usage: 136 MB
% 18.70/5.33 % (881623)Instructions burned: 109 (million)
% 18.70/5.33 % (881624)Instruction limit reached!
% 18.70/5.33 % (881624)------------------------------
% 18.70/5.33 % (881624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/5.33 % (881624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/5.33 % (881624)CaDiCaL version: 2.1.3
% 18.70/5.33 % (881624)Termination reason: Instruction limit
% 18.70/5.33 % (881624)Termination phase: SInE selection
% 18.70/5.33 % (881624)Time elapsed: 0.083 s
% 18.70/5.33 % (881624)Peak memory usage: 136 MB
% 18.70/5.33 % (881624)Instructions burned: 120 (million)
% 18.70/5.33 % (881626)Instruction limit reached!
% 18.70/5.33 % (881626)------------------------------
% 18.70/5.33 % (881626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/5.33 % (881626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/5.33 % (881626)CaDiCaL version: 2.1.3
% 18.70/5.33 % (881626)Termination reason: Instruction limit
% 18.70/5.33 % (881626)Termination phase: SInE selection
% 18.70/5.33 % (881626)Time elapsed: 0.089 s
% 18.70/5.33 % (881626)Peak memory usage: 136 MB
% 18.70/5.33 % (881626)Instructions burned: 129 (million)
% 18.70/5.33 % (881634)lrs+10_1_sil=8000:sp=occurrence:random_seed=1724587412:i=285:sd=3:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/285Mi)
% 18.70/5.33 % (881635)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3604410785:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 18.70/5.33 % (881637)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=1413152055:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 18.70/5.33 % (881636)lrs+1011_1_sil=32000:sp=occurrence:random_seed=825122494:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 18.70/5.33 % (881635)Instruction limit reached!
% 18.70/5.33 % (881635)------------------------------
% 25.07/6.22 % (881635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.07/6.22 % (881635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.07/6.22 % (881635)CaDiCaL version: 2.1.3
% 25.07/6.22 % (881635)Termination reason: Instruction limit
% 25.07/6.22 % (881635)Termination phase: Property scanning
% 25.07/6.22 % (881635)Time elapsed: 0.069 s
% 25.07/6.22 % (881635)Peak memory usage: 136 MB
% 25.07/6.22 % (881635)Instructions burned: 158 (million)
% 25.07/6.22 % (881637)Instruction limit reached!
% 25.07/6.22 % (881637)------------------------------
% 25.07/6.22 % (881637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.07/6.22 % (881637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.07/6.22 % (881637)CaDiCaL version: 2.1.3
% 25.07/6.22 % (881637)Termination reason: Instruction limit
% 25.07/6.22 % (881637)Termination phase: Property scanning
% 25.07/6.22 % (881637)Time elapsed: 0.106 s
% 25.07/6.22 % (881637)Peak memory usage: 136 MB
% 25.07/6.22 % (881637)Instructions burned: 248 (million)
% 25.07/6.22 % (881642)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3257701022:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 25.07/6.22 % (881636)Refutation not found, incomplete strategy
% 25.07/6.22 % (881636)------------------------------
% 25.07/6.22 % (881636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.07/6.22 % (881636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.07/6.22 % (881636)CaDiCaL version: 2.1.3
% 25.07/6.22 % (881636)Termination reason: Refutation not found, incomplete strategy
% 25.07/6.22 % (881636)Time elapsed: 0.199 s
% 25.07/6.22 % (881636)Peak memory usage: 142 MB
% 25.07/6.22 % (881636)Instructions burned: 241 (million)
% 25.07/6.22 % (881634)Instruction limit reached!
% 25.07/6.22 % (881634)------------------------------
% 25.07/6.22 % (881634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.07/6.22 % (881634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.07/6.22 % (881634)CaDiCaL version: 2.1.3
% 25.07/6.22 % (881634)Termination reason: Instruction limit
% 25.07/6.22 % (881634)Termination phase: Saturation
% 25.07/6.22 % (881634)Time elapsed: 0.230 s
% 25.07/6.22 % (881634)Peak memory usage: 141 MB
% 25.07/6.22 % (881634)Instructions burned: 287 (million)
% 25.07/6.22 % (881643)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2210651109:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 25.07/6.22 % (881645)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1484247933:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 25.07/6.22 % (881642)Instruction limit reached!
% 25.07/6.22 % (881642)------------------------------
% 25.07/6.22 % (881642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.07/6.22 % (881642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.07/6.22 % (881642)CaDiCaL version: 2.1.3
% 25.07/6.22 % (881642)Termination reason: Instruction limit
% 25.07/6.22 % (881642)Termination phase: SInE selection
% 25.07/6.22 % (881642)Time elapsed: 0.182 s
% 25.07/6.22 % (881642)Peak memory usage: 137 MB
% 25.07/6.22 % (881642)Instructions burned: 294 (million)
% 25.07/6.22 % (881645)Instruction limit reached!
% 25.07/6.22 % (881645)------------------------------
% 25.07/6.22 % (881645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.07/6.22 % (881645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.07/6.22 % (881645)CaDiCaL version: 2.1.3
% 25.07/6.22 % (881645)Termination reason: Instruction limit
% 25.07/6.22 % (881645)Termination phase: SInE selection
% 25.07/6.22 % (881645)Time elapsed: 0.090 s
% 25.07/6.22 % (881645)Peak memory usage: 136 MB
% 25.07/6.22 % (881645)Instructions burned: 114 (million)
% 25.07/6.22 % (881636)------------------------------
% 25.07/6.22 % (881636)------------------------------
% 25.07/6.22 % (881648)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2459126616:i=127:av=off:fsr=off:sup=off_2970 on theBenchmark for (2970ds/127Mi)
% 25.07/6.22 % (881649)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2757480986:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2969 on theBenchmark for (2969ds/114Mi)
% 25.07/6.22 % (881648)Instruction limit reached!
% 25.07/6.22 % (881648)------------------------------
% 25.07/6.22 % (881648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.07/6.22 % (881648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.21 % (881648)CaDiCaL version: 2.1.3
% 39.86/9.21 % (881648)Termination reason: Instruction limit
% 39.86/9.21 % (881648)Termination phase: Preprocessing 1
% 39.86/9.21 % (881648)Time elapsed: 0.099 s
% 39.86/9.21 % (881648)Peak memory usage: 137 MB
% 39.86/9.21 % (881648)Instructions burned: 127 (million)
% 39.86/9.21 % (881650)lrs+10_1_sil=8000:sp=occurrence:random_seed=3135049827:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2969 on theBenchmark for (2969ds/907Mi)
% 39.86/9.21 % (881649)Instruction limit reached!
% 39.86/9.21 % (881649)------------------------------
% 39.86/9.21 % (881649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.21 % (881649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.21 % (881649)CaDiCaL version: 2.1.3
% 39.86/9.21 % (881649)Termination reason: Instruction limit
% 39.86/9.21 % (881649)Termination phase: Property scanning
% 39.86/9.21 % (881649)Time elapsed: 0.054 s
% 39.86/9.21 % (881649)Peak memory usage: 136 MB
% 39.86/9.21 % (881649)Instructions burned: 116 (million)
% 39.86/9.21 % (881654)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3208880456:i=437:sd=1:aac=none:ss=included_2968 on theBenchmark for (2968ds/437Mi)
% 39.86/9.21 % (881655)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4263596351:i=5202:ss=axioms:sgt=16_2967 on theBenchmark for (2967ds/5202Mi)
% 39.86/9.21 % (881654)Refutation not found, incomplete strategy
% 39.86/9.21 % (881654)------------------------------
% 39.86/9.21 % (881654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.21 % (881654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.21 % (881654)CaDiCaL version: 2.1.3
% 39.86/9.21 % (881654)Termination reason: Refutation not found, incomplete strategy
% 39.86/9.21 % (881654)Time elapsed: 0.269 s
% 39.86/9.21 % (881654)Peak memory usage: 144 MB
% 39.86/9.21 % (881654)Instructions burned: 360 (million)
% 39.86/9.21 % (881650)Instruction limit reached!
% 39.86/9.21 % (881650)------------------------------
% 39.86/9.21 % (881650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.21 % (881650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.21 % (881650)CaDiCaL version: 2.1.3
% 39.86/9.21 % (881650)Termination reason: Instruction limit
% 39.86/9.21 % (881650)Termination phase: Property scanning
% 39.86/9.21 % (881650)Time elapsed: 0.638 s
% 39.86/9.21 % (881650)Peak memory usage: 161 MB
% 39.86/9.21 % (881650)Instructions burned: 907 (million)
% 39.86/9.21 % (881654)------------------------------
% 39.86/9.21 % (881654)------------------------------
% 39.86/9.21 % (881658)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2538889356:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2961 on theBenchmark for (2961ds/134Mi)
% 39.86/9.21 % (881659)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2161223463:st=8:i=592:sd=3:ep=RST:ss=axioms_2961 on theBenchmark for (2961ds/592Mi)
% 39.86/9.21 % (881658)Instruction limit reached!
% 39.86/9.21 % (881658)------------------------------
% 39.86/9.21 % (881658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.21 % (881658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.21 % (881658)CaDiCaL version: 2.1.3
% 39.86/9.21 % (881658)Termination reason: Instruction limit
% 39.86/9.21 % (881658)Termination phase: SInE selection
% 39.86/9.21 % (881658)Time elapsed: 0.100 s
% 39.86/9.21 % (881658)Peak memory usage: 136 MB
% 39.86/9.21 % (881658)Instructions burned: 134 (million)
% 39.86/9.21 % (881662)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=287039083:st=3:i=13193:sd=3:ss=axioms_2959 on theBenchmark for (2959ds/13193Mi)
% 39.86/9.21 % (881643)Instruction limit reached!
% 39.86/9.21 % (881643)------------------------------
% 39.86/9.21 % (881643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.21 % (881643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.21 % (881643)CaDiCaL version: 2.1.3
% 39.86/9.21 % (881643)Termination reason: Instruction limit
% 39.86/9.21 % (881643)Termination phase: Property scanning
% 39.86/9.21 % (881643)Time elapsed: 1.618 s
% 39.86/9.21 % (881643)Peak memory usage: 233 MB
% 39.86/9.21 % (881643)Instructions burned: 2353 (million)
% 39.86/9.21 % (881659)Instruction limit reached!
% 39.86/9.21 % (881659)------------------------------
% 39.86/9.21 % (881659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.22 % (881659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.22 % (881659)CaDiCaL version: 2.1.3
% 39.86/9.22 % (881659)Termination reason: Instruction limit
% 39.86/9.22 % (881659)Termination phase: Naming
% 39.86/9.22 % (881659)Time elapsed: 0.466 s
% 39.86/9.22 % (881659)Peak memory usage: 154 MB
% 39.86/9.22 % (881659)Instructions burned: 592 (million)
% 39.86/9.22 % (881664)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=130981103:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/125Mi)
% 39.86/9.22 % (881665)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1282952600:i=134:gtgl=5:slsql=off:gtg=exists_sym_2955 on theBenchmark for (2955ds/134Mi)
% 39.86/9.22 % (881664)Instruction limit reached!
% 39.86/9.22 % (881664)------------------------------
% 39.86/9.22 % (881664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.22 % (881664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.22 % (881664)CaDiCaL version: 2.1.3
% 39.86/9.22 % (881664)Termination reason: Instruction limit
% 39.86/9.22 % (881664)Termination phase: Property scanning
% 39.86/9.22 % (881664)Time elapsed: 0.057 s
% 39.86/9.22 % (881664)Peak memory usage: 136 MB
% 39.86/9.22 % (881664)Instructions burned: 126 (million)
% 39.86/9.22 % (881665)Instruction limit reached!
% 39.86/9.22 % (881665)------------------------------
% 39.86/9.22 % (881665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.22 % (881665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.22 % (881665)CaDiCaL version: 2.1.3
% 39.86/9.22 % (881665)Termination reason: Instruction limit
% 39.86/9.22 % (881665)Termination phase: Property scanning
% 39.86/9.22 % (881665)Time elapsed: 0.059 s
% 39.86/9.22 % (881665)Peak memory usage: 136 MB
% 39.86/9.22 % (881665)Instructions burned: 135 (million)
% 39.86/9.22 % (881668)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=396295655:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2953 on theBenchmark for (2953ds/141Mi)
% 39.86/9.22 % (881669)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4021410550:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2953 on theBenchmark for (2953ds/431Mi)
% 39.86/9.22 % (881668)Instruction limit reached!
% 39.86/9.22 % (881668)------------------------------
% 39.86/9.22 % (881668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.22 % (881668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.22 % (881668)CaDiCaL version: 2.1.3
% 39.86/9.22 % (881668)Termination reason: Instruction limit
% 39.86/9.22 % (881668)Termination phase: SInE selection
% 39.86/9.22 % (881668)Time elapsed: 0.103 s
% 39.86/9.22 % (881668)Peak memory usage: 136 MB
% 39.86/9.22 % (881668)Instructions burned: 141 (million)
% 39.86/9.22 % (881672)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3715090994:i=6060:aac=none:ins=25_2951 on theBenchmark for (2951ds/6060Mi)
% 39.86/9.22 % (881669)Instruction limit reached!
% 39.86/9.22 % (881669)------------------------------
% 39.86/9.22 % (881669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.22 % (881669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.22 % (881669)CaDiCaL version: 2.1.3
% 39.86/9.22 % (881669)Termination reason: Instruction limit
% 39.86/9.22 % (881669)Termination phase: Saturation
% 39.86/9.22 % (881669)Time elapsed: 0.294 s
% 39.86/9.22 % (881669)Peak memory usage: 144 MB
% 39.86/9.22 % (881669)Instructions burned: 432 (million)
% 39.86/9.22 % (881674)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=145580648:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2948 on theBenchmark for (2948ds/150Mi)
% 39.86/9.22 % (881674)Instruction limit reached!
% 39.86/9.22 % (881674)------------------------------
% 39.86/9.22 % (881674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.22 % (881674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.22 % (881674)CaDiCaL version: 2.1.3
% 39.86/9.22 % (881674)Termination reason: Instruction limit
% 39.86/9.22 % (881674)Termination phase: SInE selection
% 39.86/9.22 % (881674)Time elapsed: 0.117 s
% 39.86/9.22 % (881674)Peak memory usage: 136 MB
% 39.86/9.22 % (881674)Instructions burned: 151 (million)
% 39.86/9.22 % (881676)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=424855934:i=14155:bd=all_2946 on theBenchmark for (2946ds/14155Mi)
% 39.86/9.22 % (881655)Instruction limit reached!
% 39.86/9.22 % (881655)------------------------------
% 39.86/9.22 % (881655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.22 % (881655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.22 % (881655)CaDiCaL version: 2.1.3
% 39.86/9.22 % (881655)Termination reason: Instruction limit
% 39.86/9.22 % (881655)Termination phase: Saturation
% 39.86/9.22 % (881655)Time elapsed: 3.897 s
% 39.86/9.22 % (881655)Peak memory usage: 644 MB
% 39.86/9.22 % (881655)Instructions burned: 5202 (million)
% 39.86/9.22 % (881678)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1983657230:i=667:av=off:fsr=off_2926 on theBenchmark for (2926ds/667Mi)
% 39.86/9.22 % (881662)First to succeed.
% 39.86/9.22 % (881662)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-881615"
% 39.86/9.22 % (881678)Instruction limit reached!
% 39.86/9.22 % (881678)------------------------------
% 39.86/9.22 % (881678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.86/9.22 % (881678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.86/9.22 % (881678)CaDiCaL version: 2.1.3
% 39.86/9.22 % (881678)Termination reason: Instruction limit
% 39.86/9.22 % (881678)Termination phase: NewCNF
% 39.86/9.22 % (881678)Time elapsed: 0.550 s
% 39.86/9.22 % (881678)Peak memory usage: 186 MB
% 39.86/9.22 % (881678)Instructions burned: 668 (million)
% 39.86/9.22 % (881680)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1153241705:s2a=on:i=185:s2at=1.8:fdi=4_2919 on theBenchmark for (2919ds/185Mi)
% 39.86/9.22 % (881662)Refutation found. Thanks to Tanya!
% 39.86/9.22 % SZS status Theorem for theBenchmark
% 39.86/9.22 % SZS output start Proof for theBenchmark
% See solution above
% 46.30/9.45 % (881662)------------------------------
% 46.30/9.45 % (881662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.30/9.45 % (881662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.30/9.45 % (881662)CaDiCaL version: 2.1.3
% 46.30/9.45 % (881662)Termination reason: Refutation
% 46.30/9.45 % (881662)Time elapsed: 3.785 s
% 46.30/9.45 % (881662)Peak memory usage: 310 MB
% 46.30/9.45 % (881662)Instructions burned: 6212 (million)
% 46.30/9.45 % (881662)------------------------------
% 46.30/9.45 % (881662)------------------------------
% 46.30/9.45 % (881615)Success in time 8.372 s
% 46.30/9.45 % Vampire exiting
%------------------------------------------------------------------------------