%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT343+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:48:31 AM UTC 2026
% Result : Theorem 0.19s 0.54s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 46
% Syntax : Number of formulae : 359 ( 46 unt; 25 def)
% Number of atoms : 1221 ( 63 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 1416 ( 554 ~; 698 |; 105 &)
% ( 29 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 44 ( 42 usr; 26 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 3 con; 0-4 aty)
% Number of variables : 234 ( 0 sgn 226 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_conlat_1(X0))
=> ! [X2] :
( m1_subset_1(X2,u2_conlat_1(X0))
=> ( ~ v7_conlat_1(k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1),X0)
& v9_conlat_1(k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1),X0)
& l3_conlat_1(k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1),X0)
& ~ v7_conlat_1(k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X2),X0)
& v9_conlat_1(k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X2),X0)
& l3_conlat_1(k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X2),X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_conlat_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_conlat_1(X0))
=> ! [X2] :
( m1_subset_1(X2,u2_conlat_1(X0))
=> ( ~ v7_conlat_1(k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1),X0)
& v9_conlat_1(k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1),X0)
& l3_conlat_1(k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1),X0)
& ~ v7_conlat_1(k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X2),X0)
& v9_conlat_1(k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X2),X0)
& l3_conlat_1(k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X2),X0) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(X0)
=> X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v3_lattices) ).
fof(f14,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( ~ v1_xboole_0(X1)
=> ( m1_conlat_1(X1,X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
=> ( ~ v7_conlat_1(X2,X0)
& v9_conlat_1(X2,X0)
& l3_conlat_1(X2,X0) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d18_conlat_1) ).
fof(f15,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> k11_conlat_1(X0) = g3_lattices(k8_conlat_1(X0),k10_conlat_1(X0),k9_conlat_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d23_conlat_1) ).
fof(f17,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( v1_funct_1(k10_conlat_1(X0))
& v1_funct_2(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
& m2_relset_1(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k10_conlat_1) ).
fof(f18,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_conlat_1) ).
fof(f23,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( v1_funct_1(k4_conlat_2(X0))
& v1_funct_2(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
& m2_relset_1(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_conlat_2) ).
fof(f24,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( v1_funct_1(k5_conlat_2(X0))
& v1_funct_2(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
& m2_relset_1(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_conlat_2) ).
fof(f25,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ~ v1_xboole_0(k7_conlat_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_conlat_1) ).
fof(f26,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> m1_conlat_1(k8_conlat_1(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_conlat_1) ).
fof(f27,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_funct_2) ).
fof(f28,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( v1_funct_1(k9_conlat_1(X0))
& v1_funct_2(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
& m2_relset_1(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k9_conlat_1) ).
fof(f32,axiom,
! [X0] :
( l2_conlat_1(X0)
=> l1_conlat_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_conlat_1) ).
fof(f36,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( m1_conlat_1(X1,X0)
=> ~ v1_xboole_0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_conlat_1) ).
fof(f56,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l1_conlat_1(X0) )
=> ~ v1_xboole_0(u2_conlat_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_conlat_1) ).
fof(f61,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l1_conlat_1(X0) )
=> ~ v1_xboole_0(u1_conlat_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_conlat_1) ).
fof(f71,axiom,
! [X0,X1,X2] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [X3,X4,X5] :
( g3_lattices(X0,X1,X2) = g3_lattices(X3,X4,X5)
=> ( X0 = X3
& X1 = X4
& X2 = X5 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',free_g3_lattices) ).
fof(f87,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> k8_conlat_1(X0) = k7_conlat_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k8_conlat_1) ).
fof(f88,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k8_funct_2) ).
fof(f89,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f92,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f115,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( v7_conlat_1(k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1),X0)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1),X0)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1),X0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X2),X0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X2),X0)
| ~ l3_conlat_1(k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X2),X0) )
& m1_subset_1(X2,u2_conlat_1(X0)) )
& m1_subset_1(X1,u1_conlat_1(X0)) )
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f116,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( v7_conlat_1(k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1),X0)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1),X0)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1),X0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X2),X0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X2),X0)
| ~ l3_conlat_1(k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X2),X0) )
& m1_subset_1(X2,u2_conlat_1(X0)) )
& m1_subset_1(X1,u1_conlat_1(X0)) )
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(flattening,[],[f115]) ).
fof(f117,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f118,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f117]) ).
fof(f134,plain,
! [X0] :
( ! [X1] :
( ( m1_conlat_1(X1,X0)
<=> ! [X2] :
( ( ~ v7_conlat_1(X2,X0)
& v9_conlat_1(X2,X0)
& l3_conlat_1(X2,X0) )
| ~ r2_hidden(X2,X1) ) )
| v1_xboole_0(X1) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f135,plain,
! [X0] :
( ! [X1] :
( ( m1_conlat_1(X1,X0)
<=> ! [X2] :
( ( ~ v7_conlat_1(X2,X0)
& v9_conlat_1(X2,X0)
& l3_conlat_1(X2,X0) )
| ~ r2_hidden(X2,X1) ) )
| v1_xboole_0(X1) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f134]) ).
fof(f136,plain,
! [X0] :
( k11_conlat_1(X0) = g3_lattices(k8_conlat_1(X0),k10_conlat_1(X0),k9_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f137,plain,
! [X0] :
( k11_conlat_1(X0) = g3_lattices(k8_conlat_1(X0),k10_conlat_1(X0),k9_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f136]) ).
fof(f140,plain,
! [X0] :
( ( v1_funct_1(k10_conlat_1(X0))
& v1_funct_2(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
& m2_relset_1(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f141,plain,
! [X0] :
( ( v1_funct_1(k10_conlat_1(X0))
& v1_funct_2(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
& m2_relset_1(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f140]) ).
fof(f142,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f143,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f142]) ).
fof(f144,plain,
! [X0] :
( ( v1_funct_1(k4_conlat_2(X0))
& v1_funct_2(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
& m2_relset_1(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f145,plain,
! [X0] :
( ( v1_funct_1(k4_conlat_2(X0))
& v1_funct_2(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
& m2_relset_1(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f144]) ).
fof(f146,plain,
! [X0] :
( ( v1_funct_1(k5_conlat_2(X0))
& v1_funct_2(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
& m2_relset_1(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f24]) ).
fof(f147,plain,
! [X0] :
( ( v1_funct_1(k5_conlat_2(X0))
& v1_funct_2(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
& m2_relset_1(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f146]) ).
fof(f148,plain,
! [X0] :
( ~ v1_xboole_0(k7_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f149,plain,
! [X0] :
( ~ v1_xboole_0(k7_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f148]) ).
fof(f150,plain,
! [X0] :
( m1_conlat_1(k8_conlat_1(X0),X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f151,plain,
! [X0] :
( m1_conlat_1(k8_conlat_1(X0),X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f150]) ).
fof(f152,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f153,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f152]) ).
fof(f154,plain,
! [X0] :
( ( v1_funct_1(k9_conlat_1(X0))
& v1_funct_2(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
& m2_relset_1(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f155,plain,
! [X0] :
( ( v1_funct_1(k9_conlat_1(X0))
& v1_funct_2(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
& m2_relset_1(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f154]) ).
fof(f157,plain,
! [X0] :
( l1_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f32]) ).
fof(f160,plain,
! [X0] :
( ! [X1] :
( ~ v1_xboole_0(X1)
| ~ m1_conlat_1(X1,X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f161,plain,
! [X0] :
( ! [X1] :
( ~ v1_xboole_0(X1)
| ~ m1_conlat_1(X1,X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f160]) ).
fof(f168,plain,
! [X0] :
( ~ v1_xboole_0(u2_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l1_conlat_1(X0) ),
inference(ennf_transformation,[],[f56]) ).
fof(f169,plain,
! [X0] :
( ~ v1_xboole_0(u2_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l1_conlat_1(X0) ),
inference(flattening,[],[f168]) ).
fof(f174,plain,
! [X0] :
( ~ v1_xboole_0(u1_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l1_conlat_1(X0) ),
inference(ennf_transformation,[],[f61]) ).
fof(f175,plain,
! [X0] :
( ~ v1_xboole_0(u1_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l1_conlat_1(X0) ),
inference(flattening,[],[f174]) ).
fof(f194,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(ennf_transformation,[],[f71]) ).
fof(f195,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f194]) ).
fof(f205,plain,
! [X0] :
( k8_conlat_1(X0) = k7_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f87]) ).
fof(f206,plain,
! [X0] :
( k8_conlat_1(X0) = k7_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f205]) ).
fof(f207,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f88]) ).
fof(f208,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f207]) ).
fof(f210,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f92]) ).
fof(f211,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f210]) ).
fof(f225,plain,
( ( v7_conlat_1(k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4),sK3)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4),sK3)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4),sK3)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5),sK3)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5),sK3)
| ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5),sK3) )
& m1_subset_1(sK5,u2_conlat_1(sK3))
& m1_subset_1(sK4,u1_conlat_1(sK3))
& ~ v3_conlat_1(sK3)
& l2_conlat_1(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5)],[f116]) ).
fof(f226,plain,
! [X0] :
( ! [X1] :
( ( ( m1_conlat_1(X1,X0)
| ? [X2] :
( ( v7_conlat_1(X2,X0)
| ~ v9_conlat_1(X2,X0)
| ~ l3_conlat_1(X2,X0) )
& r2_hidden(X2,X1) ) )
& ( ! [X2] :
( ( ~ v7_conlat_1(X2,X0)
& v9_conlat_1(X2,X0)
& l3_conlat_1(X2,X0) )
| ~ r2_hidden(X2,X1) )
| ~ m1_conlat_1(X1,X0) ) )
| v1_xboole_0(X1) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(nnf_transformation,[],[f135]) ).
fof(f227,plain,
! [X0] :
( ! [X1] :
( ( ( m1_conlat_1(X1,X0)
| ? [X2] :
( ( v7_conlat_1(X2,X0)
| ~ v9_conlat_1(X2,X0)
| ~ l3_conlat_1(X2,X0) )
& r2_hidden(X2,X1) ) )
& ( ! [X3] :
( ( ~ v7_conlat_1(X3,X0)
& v9_conlat_1(X3,X0)
& l3_conlat_1(X3,X0) )
| ~ r2_hidden(X3,X1) )
| ~ m1_conlat_1(X1,X0) ) )
| v1_xboole_0(X1) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(rectify,[],[f226]) ).
fof(f228,plain,
! [X0] :
( ! [X1] :
( ( ( m1_conlat_1(X1,X0)
| ( ( v7_conlat_1(sK6(X0,X1),X0)
| ~ v9_conlat_1(sK6(X0,X1),X0)
| ~ l3_conlat_1(sK6(X0,X1),X0) )
& r2_hidden(sK6(X0,X1),X1) ) )
& ( ! [X3] :
( ( ~ v7_conlat_1(X3,X0)
& v9_conlat_1(X3,X0)
& l3_conlat_1(X3,X0) )
| ~ r2_hidden(X3,X1) )
| ~ m1_conlat_1(X1,X0) ) )
| v1_xboole_0(X1) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X2,sK6(X0,X1))],[f227]) ).
fof(f258,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f89]) ).
fof(f259,plain,
l2_conlat_1(sK3),
inference(cnf_transformation,[],[f225]) ).
fof(f260,plain,
~ v3_conlat_1(sK3),
inference(cnf_transformation,[],[f225]) ).
fof(f261,plain,
m1_subset_1(sK4,u1_conlat_1(sK3)),
inference(cnf_transformation,[],[f225]) ).
fof(f262,plain,
m1_subset_1(sK5,u2_conlat_1(sK3)),
inference(cnf_transformation,[],[f225]) ).
fof(f263,plain,
( v7_conlat_1(k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4),sK3)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4),sK3)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4),sK3)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5),sK3)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5),sK3)
| ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5),sK3) ),
inference(cnf_transformation,[],[f225]) ).
fof(f264,plain,
! [X0] :
( ~ v3_lattices(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = X0
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f118]) ).
fof(f289,plain,
! [X3,X0,X1] :
( l3_conlat_1(X3,X0)
| ~ r2_hidden(X3,X1)
| ~ m1_conlat_1(X1,X0)
| v1_xboole_0(X1)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f228]) ).
fof(f290,plain,
! [X3,X0,X1] :
( v9_conlat_1(X3,X0)
| ~ r2_hidden(X3,X1)
| ~ m1_conlat_1(X1,X0)
| v1_xboole_0(X1)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f228]) ).
fof(f291,plain,
! [X3,X0,X1] :
( ~ v7_conlat_1(X3,X0)
| ~ r2_hidden(X3,X1)
| ~ m1_conlat_1(X1,X0)
| v1_xboole_0(X1)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f228]) ).
fof(f294,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k11_conlat_1(X0) = g3_lattices(k8_conlat_1(X0),k10_conlat_1(X0),k9_conlat_1(X0)) ),
inference(cnf_transformation,[],[f137]) ).
fof(f297,plain,
! [X0] :
( m2_relset_1(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f141]) ).
fof(f298,plain,
! [X0] :
( v1_funct_2(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f141]) ).
fof(f299,plain,
! [X0] :
( v1_funct_1(k10_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f141]) ).
fof(f300,plain,
! [X0] :
( l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f301,plain,
! [X0] :
( v3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f303,plain,
! [X0] :
( m2_relset_1(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f304,plain,
! [X0] :
( v1_funct_2(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f305,plain,
! [X0] :
( v1_funct_1(k4_conlat_2(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f306,plain,
! [X0] :
( m2_relset_1(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f307,plain,
! [X0] :
( v1_funct_2(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f308,plain,
! [X0] :
( v1_funct_1(k5_conlat_2(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f309,plain,
! [X0] :
( ~ v1_xboole_0(k7_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f310,plain,
! [X0] :
( m1_conlat_1(k8_conlat_1(X0),X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f311,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f153]) ).
fof(f312,plain,
! [X0] :
( m2_relset_1(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f313,plain,
! [X0] :
( v1_funct_2(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f314,plain,
! [X0] :
( v1_funct_1(k9_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f316,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| l1_conlat_1(X0) ),
inference(cnf_transformation,[],[f157]) ).
fof(f320,plain,
! [X0,X1] :
( ~ m1_conlat_1(X1,X0)
| ~ v1_xboole_0(X1)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f339,plain,
! [X0] :
( ~ v1_xboole_0(u2_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l1_conlat_1(X0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f356,plain,
! [X0] :
( ~ v1_xboole_0(u1_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l1_conlat_1(X0) ),
inference(cnf_transformation,[],[f175]) ).
fof(f395,plain,
! [X2,X3,X0,X1,X4,X5] :
( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| X0 = X3
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f195]) ).
fof(f446,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k8_conlat_1(X0) = k7_conlat_1(X0) ),
inference(cnf_transformation,[],[f206]) ).
fof(f447,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X2,X0,X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f208]) ).
fof(f448,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f258]) ).
fof(f452,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f211]) ).
fof(f460,definition,
( spl33_1
<=> l3_conlat_1(k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5),sK3) ),
introduced(definition,[new_symbols(definition,[spl33_1])],[avatar_definition]) ).
fof(f462,plain,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5),sK3)
| spl33_1 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f464,definition,
( spl33_2
<=> v9_conlat_1(k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5),sK3) ),
introduced(definition,[new_symbols(definition,[spl33_2])],[avatar_definition]) ).
fof(f466,plain,
( ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5),sK3)
| spl33_2 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f468,definition,
( spl33_3
<=> v7_conlat_1(k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5),sK3) ),
introduced(definition,[new_symbols(definition,[spl33_3])],[avatar_definition]) ).
fof(f470,plain,
( v7_conlat_1(k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5),sK3)
| ~ spl33_3 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f472,definition,
( spl33_4
<=> l3_conlat_1(k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4),sK3) ),
introduced(definition,[new_symbols(definition,[spl33_4])],[avatar_definition]) ).
fof(f474,plain,
( ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4),sK3)
| spl33_4 ),
inference(avatar_component_clause,[],[f472]) ).
fof(f476,definition,
( spl33_5
<=> v9_conlat_1(k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4),sK3) ),
introduced(definition,[new_symbols(definition,[spl33_5])],[avatar_definition]) ).
fof(f478,plain,
( ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4),sK3)
| spl33_5 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f480,definition,
( spl33_6
<=> v7_conlat_1(k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4),sK3) ),
introduced(definition,[new_symbols(definition,[spl33_6])],[avatar_definition]) ).
fof(f482,plain,
( v7_conlat_1(k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4),sK3)
| ~ spl33_6 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f483,plain,
( ~ spl33_1
| ~ spl33_2
| spl33_3
| ~ spl33_4
| ~ spl33_5
| spl33_6 ),
inference(avatar_split_clause,[],[f263,f480,f476,f472,f468,f464,f460]) ).
fof(f485,plain,
l1_conlat_1(sK3),
inference(resolution,[],[f316,f259]) ).
fof(f600,definition,
( spl33_11
<=> v1_xboole_0(u2_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl33_11])],[avatar_definition]) ).
fof(f601,plain,
( ~ v1_xboole_0(u2_conlat_1(sK3))
| spl33_11 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f602,plain,
( v1_xboole_0(u2_conlat_1(sK3))
| ~ spl33_11 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f609,definition,
( spl33_13
<=> v1_xboole_0(u1_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl33_13])],[avatar_definition]) ).
fof(f610,plain,
( ~ v1_xboole_0(u1_conlat_1(sK3))
| spl33_13 ),
inference(avatar_component_clause,[],[f609]) ).
fof(f611,plain,
( v1_xboole_0(u1_conlat_1(sK3))
| ~ spl33_13 ),
inference(avatar_component_clause,[],[f609]) ).
fof(f620,plain,
( v3_conlat_1(sK3)
| ~ l1_conlat_1(sK3)
| ~ spl33_11 ),
inference(resolution,[],[f602,f339]) ).
fof(f623,plain,
( ~ l1_conlat_1(sK3)
| ~ spl33_11 ),
inference(forward_subsumption_resolution,[],[f620,f260]) ).
fof(f624,plain,
( $false
| ~ spl33_11 ),
inference(forward_subsumption_resolution,[],[f623,f485]) ).
fof(f625,plain,
~ spl33_11,
inference(avatar_contradiction_clause,[],[f624]) ).
fof(f630,plain,
( v3_conlat_1(sK3)
| ~ l1_conlat_1(sK3)
| ~ spl33_13 ),
inference(resolution,[],[f611,f356]) ).
fof(f633,plain,
( ~ l1_conlat_1(sK3)
| ~ spl33_13 ),
inference(forward_subsumption_resolution,[],[f630,f260]) ).
fof(f634,plain,
( $false
| ~ spl33_13 ),
inference(forward_subsumption_resolution,[],[f633,f485]) ).
fof(f635,plain,
~ spl33_13,
inference(avatar_contradiction_clause,[],[f634]) ).
fof(f642,plain,
( v3_conlat_1(sK3)
| k8_conlat_1(sK3) = k7_conlat_1(sK3) ),
inference(resolution,[],[f446,f259]) ).
fof(f644,plain,
k8_conlat_1(sK3) = k7_conlat_1(sK3),
inference(forward_subsumption_resolution,[],[f642,f260]) ).
fof(f661,plain,
( ~ v1_xboole_0(k8_conlat_1(sK3))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3) ),
inference(superposition,[],[f309,f644]) ).
fof(f662,plain,
( ~ v1_xboole_0(k8_conlat_1(sK3))
| ~ l2_conlat_1(sK3) ),
inference(forward_subsumption_resolution,[],[f661,f260]) ).
fof(f663,plain,
~ v1_xboole_0(k8_conlat_1(sK3)),
inference(forward_subsumption_resolution,[],[f662,f259]) ).
fof(f695,plain,
! [X0] :
( m1_relset_1(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(resolution,[],[f303,f448]) ).
fof(f698,plain,
! [X0] :
( m1_relset_1(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(resolution,[],[f306,f448]) ).
fof(f712,plain,
! [X0] :
( k11_conlat_1(X0) = g3_lattices(u1_struct_0(k11_conlat_1(X0)),u2_lattices(k11_conlat_1(X0)),u1_lattices(k11_conlat_1(X0)))
| ~ l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f264,f301]) ).
fof(f724,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k11_conlat_1(X0) = g3_lattices(u1_struct_0(k11_conlat_1(X0)),u2_lattices(k11_conlat_1(X0)),u1_lattices(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f712,f300]) ).
fof(f733,plain,
( v3_conlat_1(sK3)
| k11_conlat_1(sK3) = g3_lattices(k8_conlat_1(sK3),k10_conlat_1(sK3),k9_conlat_1(sK3)) ),
inference(resolution,[],[f294,f259]) ).
fof(f735,plain,
k11_conlat_1(sK3) = g3_lattices(k8_conlat_1(sK3),k10_conlat_1(sK3),k9_conlat_1(sK3)),
inference(forward_subsumption_resolution,[],[f733,f260]) ).
fof(f736,plain,
! [X0] :
( m1_relset_1(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(resolution,[],[f297,f448]) ).
fof(f738,plain,
! [X0] :
( m1_relset_1(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(resolution,[],[f312,f448]) ).
fof(f750,plain,
! [X3,X0,X1] :
( ~ m1_conlat_1(X1,X0)
| ~ r2_hidden(X3,X1)
| l3_conlat_1(X3,X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f289,f320]) ).
fof(f751,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k8_conlat_1(X1))
| l3_conlat_1(X0,X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(resolution,[],[f750,f310]) ).
fof(f754,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k8_conlat_1(X1))
| l3_conlat_1(X0,X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(duplicate_literal_removal,[],[f751]) ).
fof(f755,plain,
! [X3,X0,X1] :
( ~ m1_conlat_1(X1,X0)
| ~ r2_hidden(X3,X1)
| v9_conlat_1(X3,X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f290,f320]) ).
fof(f757,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k8_conlat_1(X1))
| v9_conlat_1(X0,X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(resolution,[],[f755,f310]) ).
fof(f760,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k8_conlat_1(X1))
| v9_conlat_1(X0,X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(duplicate_literal_removal,[],[f757]) ).
fof(f764,plain,
! [X3,X0,X1] :
( ~ m1_conlat_1(X1,X0)
| ~ r2_hidden(X3,X1)
| ~ v7_conlat_1(X3,X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f291,f320]) ).
fof(f766,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k8_conlat_1(X1))
| ~ v7_conlat_1(X0,X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(resolution,[],[f764,f310]) ).
fof(f769,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k8_conlat_1(X1))
| ~ v7_conlat_1(X0,X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(duplicate_literal_removal,[],[f766]) ).
fof(f852,plain,
! [X2,X3,X0,X1] :
( r2_hidden(k8_funct_2(X0,X2,X1,X3),X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,X2)
| ~ m1_relset_1(X1,X0,X2)
| ~ m1_subset_1(X3,X0)
| v1_xboole_0(X0)
| v1_xboole_0(X2) ),
inference(resolution,[],[f311,f452]) ).
fof(f879,plain,
! [X0,X1] :
( v1_xboole_0(u1_conlat_1(X0))
| ~ v1_funct_1(k4_conlat_2(X0))
| k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1) = k1_funct_1(k4_conlat_2(X0),X1)
| ~ m1_relset_1(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m1_subset_1(X1,u1_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f447,f304]) ).
fof(f880,plain,
! [X0,X1] :
( v1_xboole_0(u2_conlat_1(X0))
| ~ v1_funct_1(k5_conlat_2(X0))
| k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X1) = k1_funct_1(k5_conlat_2(X0),X1)
| ~ m1_relset_1(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m1_subset_1(X1,u2_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f447,f307]) ).
fof(f891,plain,
! [X0,X1] :
( v1_xboole_0(u2_conlat_1(X0))
| k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X1) = k1_funct_1(k5_conlat_2(X0),X1)
| ~ m1_relset_1(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m1_subset_1(X1,u2_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f880,f308]) ).
fof(f892,plain,
! [X0,X1] :
( v1_xboole_0(u1_conlat_1(X0))
| k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1) = k1_funct_1(k4_conlat_2(X0),X1)
| ~ m1_relset_1(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m1_subset_1(X1,u1_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f879,f305]) ).
fof(f940,definition,
( spl33_19
<=> m1_relset_1(k9_conlat_1(sK3),k2_zfmisc_1(k8_conlat_1(sK3),k8_conlat_1(sK3)),k8_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl33_19])],[avatar_definition]) ).
fof(f942,plain,
( ~ m1_relset_1(k9_conlat_1(sK3),k2_zfmisc_1(k8_conlat_1(sK3),k8_conlat_1(sK3)),k8_conlat_1(sK3))
| spl33_19 ),
inference(avatar_component_clause,[],[f940]) ).
fof(f944,definition,
( spl33_20
<=> v1_funct_2(k9_conlat_1(sK3),k2_zfmisc_1(k8_conlat_1(sK3),k8_conlat_1(sK3)),k8_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl33_20])],[avatar_definition]) ).
fof(f946,plain,
( ~ v1_funct_2(k9_conlat_1(sK3),k2_zfmisc_1(k8_conlat_1(sK3),k8_conlat_1(sK3)),k8_conlat_1(sK3))
| spl33_20 ),
inference(avatar_component_clause,[],[f944]) ).
fof(f948,definition,
( spl33_21
<=> v1_funct_1(k9_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl33_21])],[avatar_definition]) ).
fof(f950,plain,
( ~ v1_funct_1(k9_conlat_1(sK3))
| spl33_21 ),
inference(avatar_component_clause,[],[f948]) ).
fof(f952,definition,
( spl33_22
<=> m1_relset_1(k10_conlat_1(sK3),k2_zfmisc_1(k8_conlat_1(sK3),k8_conlat_1(sK3)),k8_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl33_22])],[avatar_definition]) ).
fof(f954,plain,
( ~ m1_relset_1(k10_conlat_1(sK3),k2_zfmisc_1(k8_conlat_1(sK3),k8_conlat_1(sK3)),k8_conlat_1(sK3))
| spl33_22 ),
inference(avatar_component_clause,[],[f952]) ).
fof(f956,definition,
( spl33_23
<=> v1_funct_2(k10_conlat_1(sK3),k2_zfmisc_1(k8_conlat_1(sK3),k8_conlat_1(sK3)),k8_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl33_23])],[avatar_definition]) ).
fof(f958,plain,
( ~ v1_funct_2(k10_conlat_1(sK3),k2_zfmisc_1(k8_conlat_1(sK3),k8_conlat_1(sK3)),k8_conlat_1(sK3))
| spl33_23 ),
inference(avatar_component_clause,[],[f956]) ).
fof(f960,definition,
( spl33_24
<=> v1_funct_1(k10_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl33_24])],[avatar_definition]) ).
fof(f962,plain,
( ~ v1_funct_1(k10_conlat_1(sK3))
| spl33_24 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f970,plain,
! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k11_conlat_1(sK3)
| k8_conlat_1(sK3) = X0
| ~ v1_funct_1(k10_conlat_1(sK3))
| ~ v1_funct_2(k10_conlat_1(sK3),k2_zfmisc_1(k8_conlat_1(sK3),k8_conlat_1(sK3)),k8_conlat_1(sK3))
| ~ m1_relset_1(k10_conlat_1(sK3),k2_zfmisc_1(k8_conlat_1(sK3),k8_conlat_1(sK3)),k8_conlat_1(sK3))
| ~ v1_funct_1(k9_conlat_1(sK3))
| ~ v1_funct_2(k9_conlat_1(sK3),k2_zfmisc_1(k8_conlat_1(sK3),k8_conlat_1(sK3)),k8_conlat_1(sK3))
| ~ m1_relset_1(k9_conlat_1(sK3),k2_zfmisc_1(k8_conlat_1(sK3),k8_conlat_1(sK3)),k8_conlat_1(sK3)) ),
inference(superposition,[],[f395,f735]) ).
fof(f1396,plain,
( ~ l2_conlat_1(sK3)
| v3_conlat_1(sK3)
| spl33_19 ),
inference(resolution,[],[f738,f942]) ).
fof(f1398,plain,
( v3_conlat_1(sK3)
| spl33_19 ),
inference(forward_subsumption_resolution,[],[f1396,f259]) ).
fof(f1399,plain,
( $false
| spl33_19 ),
inference(forward_subsumption_resolution,[],[f1398,f260]) ).
fof(f1400,plain,
spl33_19,
inference(avatar_contradiction_clause,[],[f1399]) ).
fof(f1406,definition,
( spl33_79
<=> ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k11_conlat_1(sK3)
| k8_conlat_1(sK3) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl33_79])],[avatar_definition]) ).
fof(f1407,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k11_conlat_1(sK3)
| k8_conlat_1(sK3) = X0 )
| ~ spl33_79 ),
inference(avatar_component_clause,[],[f1406]) ).
fof(f1408,plain,
( ~ spl33_19
| ~ spl33_20
| ~ spl33_21
| ~ spl33_22
| ~ spl33_23
| ~ spl33_24
| spl33_79 ),
inference(avatar_split_clause,[],[f970,f1406,f960,f956,f952,f948,f944,f940]) ).
fof(f1410,plain,
( v3_conlat_1(sK3)
| k11_conlat_1(sK3) = g3_lattices(u1_struct_0(k11_conlat_1(sK3)),u2_lattices(k11_conlat_1(sK3)),u1_lattices(k11_conlat_1(sK3))) ),
inference(resolution,[],[f724,f259]) ).
fof(f1412,plain,
k11_conlat_1(sK3) = g3_lattices(u1_struct_0(k11_conlat_1(sK3)),u2_lattices(k11_conlat_1(sK3)),u1_lattices(k11_conlat_1(sK3))),
inference(forward_subsumption_resolution,[],[f1410,f260]) ).
fof(f1413,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl33_20 ),
inference(resolution,[],[f946,f313]) ).
fof(f1414,plain,
( ~ l2_conlat_1(sK3)
| spl33_20 ),
inference(forward_subsumption_resolution,[],[f1413,f260]) ).
fof(f1415,plain,
( $false
| spl33_20 ),
inference(forward_subsumption_resolution,[],[f1414,f259]) ).
fof(f1416,plain,
spl33_20,
inference(avatar_contradiction_clause,[],[f1415]) ).
fof(f1418,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl33_21 ),
inference(resolution,[],[f950,f314]) ).
fof(f1419,plain,
( ~ l2_conlat_1(sK3)
| spl33_21 ),
inference(forward_subsumption_resolution,[],[f1418,f260]) ).
fof(f1420,plain,
( $false
| spl33_21 ),
inference(forward_subsumption_resolution,[],[f1419,f259]) ).
fof(f1421,plain,
spl33_21,
inference(avatar_contradiction_clause,[],[f1420]) ).
fof(f1490,plain,
( ~ l2_conlat_1(sK3)
| v3_conlat_1(sK3)
| spl33_22 ),
inference(resolution,[],[f954,f736]) ).
fof(f1491,plain,
( v3_conlat_1(sK3)
| spl33_22 ),
inference(forward_subsumption_resolution,[],[f1490,f259]) ).
fof(f1492,plain,
( $false
| spl33_22 ),
inference(forward_subsumption_resolution,[],[f1491,f260]) ).
fof(f1493,plain,
spl33_22,
inference(avatar_contradiction_clause,[],[f1492]) ).
fof(f1504,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl33_23 ),
inference(resolution,[],[f958,f298]) ).
fof(f1505,plain,
( ~ l2_conlat_1(sK3)
| spl33_23 ),
inference(forward_subsumption_resolution,[],[f1504,f260]) ).
fof(f1506,plain,
( $false
| spl33_23 ),
inference(forward_subsumption_resolution,[],[f1505,f259]) ).
fof(f1507,plain,
spl33_23,
inference(avatar_contradiction_clause,[],[f1506]) ).
fof(f1516,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl33_24 ),
inference(resolution,[],[f962,f299]) ).
fof(f1517,plain,
( ~ l2_conlat_1(sK3)
| spl33_24 ),
inference(forward_subsumption_resolution,[],[f1516,f260]) ).
fof(f1518,plain,
( $false
| spl33_24 ),
inference(forward_subsumption_resolution,[],[f1517,f259]) ).
fof(f1519,plain,
spl33_24,
inference(avatar_contradiction_clause,[],[f1518]) ).
fof(f1828,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u2_conlat_1(X0))
| k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X1) = k1_funct_1(k5_conlat_2(X0),X1)
| v1_xboole_0(u2_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f891,f698]) ).
fof(f1830,plain,
( k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5) = k1_funct_1(k5_conlat_2(sK3),sK5)
| v1_xboole_0(u2_conlat_1(sK3))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3) ),
inference(resolution,[],[f1828,f262]) ).
fof(f1838,plain,
( k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5) = k1_funct_1(k5_conlat_2(sK3),sK5)
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl33_11 ),
inference(forward_subsumption_resolution,[],[f1830,f601]) ).
fof(f1839,plain,
( k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5) = k1_funct_1(k5_conlat_2(sK3),sK5)
| ~ l2_conlat_1(sK3)
| spl33_11 ),
inference(forward_subsumption_resolution,[],[f1838,f260]) ).
fof(f1840,plain,
( k8_funct_2(u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k5_conlat_2(sK3),sK5) = k1_funct_1(k5_conlat_2(sK3),sK5)
| spl33_11 ),
inference(forward_subsumption_resolution,[],[f1839,f259]) ).
fof(f1853,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_conlat_1(X0))
| k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X1) = k1_funct_1(k4_conlat_2(X0),X1)
| v1_xboole_0(u1_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f892,f695]) ).
fof(f1855,plain,
( k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4) = k1_funct_1(k4_conlat_2(sK3),sK4)
| v1_xboole_0(u1_conlat_1(sK3))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3) ),
inference(resolution,[],[f1853,f261]) ).
fof(f1863,plain,
( k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4) = k1_funct_1(k4_conlat_2(sK3),sK4)
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl33_13 ),
inference(forward_subsumption_resolution,[],[f1855,f610]) ).
fof(f1864,plain,
( k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4) = k1_funct_1(k4_conlat_2(sK3),sK4)
| ~ l2_conlat_1(sK3)
| spl33_13 ),
inference(forward_subsumption_resolution,[],[f1863,f260]) ).
fof(f1865,plain,
( k8_funct_2(u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)),k4_conlat_2(sK3),sK4) = k1_funct_1(k4_conlat_2(sK3),sK4)
| spl33_13 ),
inference(forward_subsumption_resolution,[],[f1864,f259]) ).
fof(f2266,plain,
( k11_conlat_1(sK3) != k11_conlat_1(sK3)
| u1_struct_0(k11_conlat_1(sK3)) = k8_conlat_1(sK3)
| ~ spl33_79 ),
inference(superposition,[],[f1407,f1412]) ).
fof(f2267,plain,
( u1_struct_0(k11_conlat_1(sK3)) = k8_conlat_1(sK3)
| ~ spl33_79 ),
inference(trivial_inequality_removal,[],[f2266]) ).
fof(f2298,definition,
( spl33_103
<=> u1_struct_0(k11_conlat_1(sK3)) = k8_conlat_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl33_103])],[avatar_definition]) ).
fof(f2300,plain,
( u1_struct_0(k11_conlat_1(sK3)) = k8_conlat_1(sK3)
| ~ spl33_103 ),
inference(avatar_component_clause,[],[f2298]) ).
fof(f2324,plain,
( spl33_103
| ~ spl33_79 ),
inference(avatar_split_clause,[],[f2267,f1406,f2298]) ).
fof(f2325,plain,
( ~ l3_conlat_1(k1_funct_1(k5_conlat_2(sK3),sK5),sK3)
| spl33_1
| spl33_11 ),
inference(superposition,[],[f462,f1840]) ).
fof(f2326,plain,
( r2_hidden(k1_funct_1(k5_conlat_2(sK3),sK5),u1_struct_0(k11_conlat_1(sK3)))
| ~ v1_funct_1(k5_conlat_2(sK3))
| ~ v1_funct_2(k5_conlat_2(sK3),u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| ~ m1_relset_1(k5_conlat_2(sK3),u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| ~ m1_subset_1(sK5,u2_conlat_1(sK3))
| v1_xboole_0(u2_conlat_1(sK3))
| v1_xboole_0(u1_struct_0(k11_conlat_1(sK3)))
| spl33_11 ),
inference(superposition,[],[f852,f1840]) ).
fof(f2329,plain,
( r2_hidden(k1_funct_1(k5_conlat_2(sK3),sK5),u1_struct_0(k11_conlat_1(sK3)))
| ~ v1_funct_1(k5_conlat_2(sK3))
| ~ v1_funct_2(k5_conlat_2(sK3),u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| ~ m1_relset_1(k5_conlat_2(sK3),u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v1_xboole_0(u2_conlat_1(sK3))
| v1_xboole_0(u1_struct_0(k11_conlat_1(sK3)))
| spl33_11 ),
inference(forward_subsumption_resolution,[],[f2326,f262]) ).
fof(f2331,plain,
( r2_hidden(k1_funct_1(k5_conlat_2(sK3),sK5),u1_struct_0(k11_conlat_1(sK3)))
| ~ v1_funct_1(k5_conlat_2(sK3))
| ~ v1_funct_2(k5_conlat_2(sK3),u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| ~ m1_relset_1(k5_conlat_2(sK3),u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v1_xboole_0(u1_struct_0(k11_conlat_1(sK3)))
| spl33_11 ),
inference(forward_subsumption_resolution,[],[f2329,f601]) ).
fof(f2333,definition,
( spl33_109
<=> m1_relset_1(k5_conlat_2(sK3),u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3))) ),
introduced(definition,[new_symbols(definition,[spl33_109])],[avatar_definition]) ).
fof(f2335,plain,
( ~ m1_relset_1(k5_conlat_2(sK3),u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| spl33_109 ),
inference(avatar_component_clause,[],[f2333]) ).
fof(f2337,definition,
( spl33_110
<=> v1_funct_2(k5_conlat_2(sK3),u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3))) ),
introduced(definition,[new_symbols(definition,[spl33_110])],[avatar_definition]) ).
fof(f2339,plain,
( ~ v1_funct_2(k5_conlat_2(sK3),u2_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| spl33_110 ),
inference(avatar_component_clause,[],[f2337]) ).
fof(f2341,definition,
( spl33_111
<=> v1_funct_1(k5_conlat_2(sK3)) ),
introduced(definition,[new_symbols(definition,[spl33_111])],[avatar_definition]) ).
fof(f2343,plain,
( ~ v1_funct_1(k5_conlat_2(sK3))
| spl33_111 ),
inference(avatar_component_clause,[],[f2341]) ).
fof(f2350,definition,
( spl33_113
<=> v1_xboole_0(u1_struct_0(k11_conlat_1(sK3))) ),
introduced(definition,[new_symbols(definition,[spl33_113])],[avatar_definition]) ).
fof(f2352,plain,
( v1_xboole_0(u1_struct_0(k11_conlat_1(sK3)))
| ~ spl33_113 ),
inference(avatar_component_clause,[],[f2350]) ).
fof(f2354,definition,
( spl33_114
<=> r2_hidden(k1_funct_1(k5_conlat_2(sK3),sK5),u1_struct_0(k11_conlat_1(sK3))) ),
introduced(definition,[new_symbols(definition,[spl33_114])],[avatar_definition]) ).
fof(f2356,plain,
( r2_hidden(k1_funct_1(k5_conlat_2(sK3),sK5),u1_struct_0(k11_conlat_1(sK3)))
| ~ spl33_114 ),
inference(avatar_component_clause,[],[f2354]) ).
fof(f2357,plain,
( spl33_113
| ~ spl33_109
| ~ spl33_110
| ~ spl33_111
| spl33_114
| spl33_11 ),
inference(avatar_split_clause,[],[f2331,f600,f2354,f2341,f2337,f2333,f2350]) ).
fof(f2359,plain,
( r2_hidden(k1_funct_1(k4_conlat_2(sK3),sK4),u1_struct_0(k11_conlat_1(sK3)))
| ~ v1_funct_1(k4_conlat_2(sK3))
| ~ v1_funct_2(k4_conlat_2(sK3),u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| ~ m1_relset_1(k4_conlat_2(sK3),u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| ~ m1_subset_1(sK4,u1_conlat_1(sK3))
| v1_xboole_0(u1_conlat_1(sK3))
| v1_xboole_0(u1_struct_0(k11_conlat_1(sK3)))
| spl33_13 ),
inference(superposition,[],[f852,f1865]) ).
fof(f2362,plain,
( r2_hidden(k1_funct_1(k4_conlat_2(sK3),sK4),u1_struct_0(k11_conlat_1(sK3)))
| ~ v1_funct_1(k4_conlat_2(sK3))
| ~ v1_funct_2(k4_conlat_2(sK3),u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| ~ m1_relset_1(k4_conlat_2(sK3),u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v1_xboole_0(u1_conlat_1(sK3))
| v1_xboole_0(u1_struct_0(k11_conlat_1(sK3)))
| spl33_13 ),
inference(forward_subsumption_resolution,[],[f2359,f261]) ).
fof(f2364,plain,
( r2_hidden(k1_funct_1(k4_conlat_2(sK3),sK4),u1_struct_0(k11_conlat_1(sK3)))
| ~ v1_funct_1(k4_conlat_2(sK3))
| ~ v1_funct_2(k4_conlat_2(sK3),u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| ~ m1_relset_1(k4_conlat_2(sK3),u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v1_xboole_0(u1_struct_0(k11_conlat_1(sK3)))
| spl33_13 ),
inference(forward_subsumption_resolution,[],[f2362,f610]) ).
fof(f2366,definition,
( spl33_115
<=> m1_relset_1(k4_conlat_2(sK3),u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3))) ),
introduced(definition,[new_symbols(definition,[spl33_115])],[avatar_definition]) ).
fof(f2368,plain,
( ~ m1_relset_1(k4_conlat_2(sK3),u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| spl33_115 ),
inference(avatar_component_clause,[],[f2366]) ).
fof(f2370,definition,
( spl33_116
<=> v1_funct_2(k4_conlat_2(sK3),u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3))) ),
introduced(definition,[new_symbols(definition,[spl33_116])],[avatar_definition]) ).
fof(f2372,plain,
( ~ v1_funct_2(k4_conlat_2(sK3),u1_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| spl33_116 ),
inference(avatar_component_clause,[],[f2370]) ).
fof(f2374,definition,
( spl33_117
<=> v1_funct_1(k4_conlat_2(sK3)) ),
introduced(definition,[new_symbols(definition,[spl33_117])],[avatar_definition]) ).
fof(f2376,plain,
( ~ v1_funct_1(k4_conlat_2(sK3))
| spl33_117 ),
inference(avatar_component_clause,[],[f2374]) ).
fof(f2383,definition,
( spl33_119
<=> r2_hidden(k1_funct_1(k4_conlat_2(sK3),sK4),u1_struct_0(k11_conlat_1(sK3))) ),
introduced(definition,[new_symbols(definition,[spl33_119])],[avatar_definition]) ).
fof(f2385,plain,
( r2_hidden(k1_funct_1(k4_conlat_2(sK3),sK4),u1_struct_0(k11_conlat_1(sK3)))
| ~ spl33_119 ),
inference(avatar_component_clause,[],[f2383]) ).
fof(f2386,plain,
( spl33_113
| ~ spl33_115
| ~ spl33_116
| ~ spl33_117
| spl33_119
| spl33_13 ),
inference(avatar_split_clause,[],[f2364,f609,f2383,f2374,f2370,f2366,f2350]) ).
fof(f2417,plain,
( v1_funct_2(k4_conlat_2(sK3),u1_conlat_1(sK3),k8_conlat_1(sK3))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ spl33_103 ),
inference(superposition,[],[f304,f2300]) ).
fof(f2419,plain,
( v1_funct_2(k5_conlat_2(sK3),u2_conlat_1(sK3),k8_conlat_1(sK3))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ spl33_103 ),
inference(superposition,[],[f307,f2300]) ).
fof(f2420,plain,
( m1_relset_1(k4_conlat_2(sK3),u1_conlat_1(sK3),k8_conlat_1(sK3))
| ~ l2_conlat_1(sK3)
| v3_conlat_1(sK3)
| ~ spl33_103 ),
inference(superposition,[],[f695,f2300]) ).
fof(f2421,plain,
( m1_relset_1(k5_conlat_2(sK3),u2_conlat_1(sK3),k8_conlat_1(sK3))
| ~ l2_conlat_1(sK3)
| v3_conlat_1(sK3)
| ~ spl33_103 ),
inference(superposition,[],[f698,f2300]) ).
fof(f2479,plain,
( m1_relset_1(k5_conlat_2(sK3),u2_conlat_1(sK3),k8_conlat_1(sK3))
| v3_conlat_1(sK3)
| ~ spl33_103 ),
inference(forward_subsumption_resolution,[],[f2421,f259]) ).
fof(f2480,plain,
( m1_relset_1(k4_conlat_2(sK3),u1_conlat_1(sK3),k8_conlat_1(sK3))
| v3_conlat_1(sK3)
| ~ spl33_103 ),
inference(forward_subsumption_resolution,[],[f2420,f259]) ).
fof(f2481,plain,
( v1_funct_2(k5_conlat_2(sK3),u2_conlat_1(sK3),k8_conlat_1(sK3))
| ~ l2_conlat_1(sK3)
| ~ spl33_103 ),
inference(forward_subsumption_resolution,[],[f2419,f260]) ).
fof(f2483,plain,
( v1_funct_2(k4_conlat_2(sK3),u1_conlat_1(sK3),k8_conlat_1(sK3))
| ~ l2_conlat_1(sK3)
| ~ spl33_103 ),
inference(forward_subsumption_resolution,[],[f2417,f260]) ).
fof(f2503,plain,
( m1_relset_1(k5_conlat_2(sK3),u2_conlat_1(sK3),k8_conlat_1(sK3))
| ~ spl33_103 ),
inference(forward_subsumption_resolution,[],[f2479,f260]) ).
fof(f2504,plain,
( m1_relset_1(k4_conlat_2(sK3),u1_conlat_1(sK3),k8_conlat_1(sK3))
| ~ spl33_103 ),
inference(forward_subsumption_resolution,[],[f2480,f260]) ).
fof(f2505,plain,
( v1_funct_2(k5_conlat_2(sK3),u2_conlat_1(sK3),k8_conlat_1(sK3))
| ~ spl33_103 ),
inference(forward_subsumption_resolution,[],[f2481,f259]) ).
fof(f2507,plain,
( v1_funct_2(k4_conlat_2(sK3),u1_conlat_1(sK3),k8_conlat_1(sK3))
| ~ spl33_103 ),
inference(forward_subsumption_resolution,[],[f2483,f259]) ).
fof(f2796,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl33_111 ),
inference(resolution,[],[f2343,f308]) ).
fof(f2797,plain,
( ~ l2_conlat_1(sK3)
| spl33_111 ),
inference(forward_subsumption_resolution,[],[f2796,f260]) ).
fof(f2798,plain,
( $false
| spl33_111 ),
inference(forward_subsumption_resolution,[],[f2797,f259]) ).
fof(f2799,plain,
spl33_111,
inference(avatar_contradiction_clause,[],[f2798]) ).
fof(f2860,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl33_117 ),
inference(resolution,[],[f2376,f305]) ).
fof(f2861,plain,
( ~ l2_conlat_1(sK3)
| spl33_117 ),
inference(forward_subsumption_resolution,[],[f2860,f260]) ).
fof(f2862,plain,
( $false
| spl33_117 ),
inference(forward_subsumption_resolution,[],[f2861,f259]) ).
fof(f2863,plain,
spl33_117,
inference(avatar_contradiction_clause,[],[f2862]) ).
fof(f3029,plain,
( ~ m1_relset_1(k5_conlat_2(sK3),u2_conlat_1(sK3),k8_conlat_1(sK3))
| ~ spl33_103
| spl33_109 ),
inference(forward_demodulation,[],[f2335,f2300]) ).
fof(f3030,plain,
( $false
| ~ spl33_103
| spl33_109 ),
inference(forward_subsumption_resolution,[],[f3029,f2503]) ).
fof(f3031,plain,
( ~ spl33_103
| spl33_109 ),
inference(avatar_contradiction_clause,[],[f3030]) ).
fof(f3033,plain,
( ~ v1_funct_2(k5_conlat_2(sK3),u2_conlat_1(sK3),k8_conlat_1(sK3))
| ~ spl33_103
| spl33_110 ),
inference(forward_demodulation,[],[f2339,f2300]) ).
fof(f3034,plain,
( $false
| ~ spl33_103
| spl33_110 ),
inference(forward_subsumption_resolution,[],[f3033,f2505]) ).
fof(f3035,plain,
( ~ spl33_103
| spl33_110 ),
inference(avatar_contradiction_clause,[],[f3034]) ).
fof(f3038,plain,
( v1_xboole_0(k8_conlat_1(sK3))
| ~ spl33_103
| ~ spl33_113 ),
inference(forward_demodulation,[],[f2352,f2300]) ).
fof(f3039,plain,
( $false
| ~ spl33_103
| ~ spl33_113 ),
inference(forward_subsumption_resolution,[],[f3038,f663]) ).
fof(f3040,plain,
( ~ spl33_103
| ~ spl33_113 ),
inference(avatar_contradiction_clause,[],[f3039]) ).
fof(f3042,plain,
( r2_hidden(k1_funct_1(k5_conlat_2(sK3),sK5),k8_conlat_1(sK3))
| ~ spl33_103
| ~ spl33_114 ),
inference(forward_demodulation,[],[f2356,f2300]) ).
fof(f3048,plain,
( ~ v7_conlat_1(k1_funct_1(k5_conlat_2(sK3),sK5),sK3)
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ spl33_103
| ~ spl33_114 ),
inference(resolution,[],[f3042,f769]) ).
fof(f3049,plain,
( v9_conlat_1(k1_funct_1(k5_conlat_2(sK3),sK5),sK3)
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ spl33_103
| ~ spl33_114 ),
inference(resolution,[],[f3042,f760]) ).
fof(f3050,plain,
( l3_conlat_1(k1_funct_1(k5_conlat_2(sK3),sK5),sK3)
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ spl33_103
| ~ spl33_114 ),
inference(resolution,[],[f3042,f754]) ).
fof(f3054,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl33_1
| spl33_11
| ~ spl33_103
| ~ spl33_114 ),
inference(forward_subsumption_resolution,[],[f3050,f2325]) ).
fof(f3055,plain,
( v9_conlat_1(k1_funct_1(k5_conlat_2(sK3),sK5),sK3)
| ~ l2_conlat_1(sK3)
| ~ spl33_103
| ~ spl33_114 ),
inference(forward_subsumption_resolution,[],[f3049,f260]) ).
fof(f3056,plain,
( ~ v7_conlat_1(k1_funct_1(k5_conlat_2(sK3),sK5),sK3)
| ~ l2_conlat_1(sK3)
| ~ spl33_103
| ~ spl33_114 ),
inference(forward_subsumption_resolution,[],[f3048,f260]) ).
fof(f3057,plain,
( ~ l2_conlat_1(sK3)
| spl33_1
| spl33_11
| ~ spl33_103
| ~ spl33_114 ),
inference(forward_subsumption_resolution,[],[f3054,f260]) ).
fof(f3058,plain,
( v9_conlat_1(k1_funct_1(k5_conlat_2(sK3),sK5),sK3)
| ~ spl33_103
| ~ spl33_114 ),
inference(forward_subsumption_resolution,[],[f3055,f259]) ).
fof(f3059,plain,
( ~ v7_conlat_1(k1_funct_1(k5_conlat_2(sK3),sK5),sK3)
| ~ spl33_103
| ~ spl33_114 ),
inference(forward_subsumption_resolution,[],[f3056,f259]) ).
fof(f3060,plain,
( $false
| spl33_1
| spl33_11
| ~ spl33_103
| ~ spl33_114 ),
inference(forward_subsumption_resolution,[],[f3057,f259]) ).
fof(f3061,plain,
( spl33_1
| spl33_11
| ~ spl33_103
| ~ spl33_114 ),
inference(avatar_contradiction_clause,[],[f3060]) ).
fof(f3063,plain,
( ~ v9_conlat_1(k1_funct_1(k5_conlat_2(sK3),sK5),sK3)
| spl33_2
| spl33_11 ),
inference(forward_demodulation,[],[f466,f1840]) ).
fof(f3066,plain,
( $false
| spl33_2
| spl33_11
| ~ spl33_103
| ~ spl33_114 ),
inference(forward_subsumption_resolution,[],[f3058,f3063]) ).
fof(f3067,plain,
( spl33_2
| spl33_11
| ~ spl33_103
| ~ spl33_114 ),
inference(avatar_contradiction_clause,[],[f3066]) ).
fof(f3069,plain,
( ~ l3_conlat_1(k1_funct_1(k4_conlat_2(sK3),sK4),sK3)
| spl33_4
| spl33_13 ),
inference(forward_demodulation,[],[f474,f1865]) ).
fof(f3085,plain,
( ~ m1_relset_1(k4_conlat_2(sK3),u1_conlat_1(sK3),k8_conlat_1(sK3))
| ~ spl33_103
| spl33_115 ),
inference(forward_demodulation,[],[f2368,f2300]) ).
fof(f3086,plain,
( $false
| ~ spl33_103
| spl33_115 ),
inference(forward_subsumption_resolution,[],[f3085,f2504]) ).
fof(f3087,plain,
( ~ spl33_103
| spl33_115 ),
inference(avatar_contradiction_clause,[],[f3086]) ).
fof(f3089,plain,
( ~ v1_funct_2(k4_conlat_2(sK3),u1_conlat_1(sK3),k8_conlat_1(sK3))
| ~ spl33_103
| spl33_116 ),
inference(forward_demodulation,[],[f2372,f2300]) ).
fof(f3090,plain,
( $false
| ~ spl33_103
| spl33_116 ),
inference(forward_subsumption_resolution,[],[f3089,f2507]) ).
fof(f3091,plain,
( ~ spl33_103
| spl33_116 ),
inference(avatar_contradiction_clause,[],[f3090]) ).
fof(f3094,plain,
( r2_hidden(k1_funct_1(k4_conlat_2(sK3),sK4),k8_conlat_1(sK3))
| ~ spl33_103
| ~ spl33_119 ),
inference(forward_demodulation,[],[f2385,f2300]) ).
fof(f3111,plain,
( ~ v7_conlat_1(k1_funct_1(k4_conlat_2(sK3),sK4),sK3)
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ spl33_103
| ~ spl33_119 ),
inference(resolution,[],[f3094,f769]) ).
fof(f3112,plain,
( v9_conlat_1(k1_funct_1(k4_conlat_2(sK3),sK4),sK3)
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ spl33_103
| ~ spl33_119 ),
inference(resolution,[],[f3094,f760]) ).
fof(f3113,plain,
( l3_conlat_1(k1_funct_1(k4_conlat_2(sK3),sK4),sK3)
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ spl33_103
| ~ spl33_119 ),
inference(resolution,[],[f3094,f754]) ).
fof(f3117,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl33_4
| spl33_13
| ~ spl33_103
| ~ spl33_119 ),
inference(forward_subsumption_resolution,[],[f3113,f3069]) ).
fof(f3118,plain,
( v9_conlat_1(k1_funct_1(k4_conlat_2(sK3),sK4),sK3)
| ~ l2_conlat_1(sK3)
| ~ spl33_103
| ~ spl33_119 ),
inference(forward_subsumption_resolution,[],[f3112,f260]) ).
fof(f3119,plain,
( ~ v7_conlat_1(k1_funct_1(k4_conlat_2(sK3),sK4),sK3)
| ~ l2_conlat_1(sK3)
| ~ spl33_103
| ~ spl33_119 ),
inference(forward_subsumption_resolution,[],[f3111,f260]) ).
fof(f3120,plain,
( ~ l2_conlat_1(sK3)
| spl33_4
| spl33_13
| ~ spl33_103
| ~ spl33_119 ),
inference(forward_subsumption_resolution,[],[f3117,f260]) ).
fof(f3121,plain,
( v9_conlat_1(k1_funct_1(k4_conlat_2(sK3),sK4),sK3)
| ~ spl33_103
| ~ spl33_119 ),
inference(forward_subsumption_resolution,[],[f3118,f259]) ).
fof(f3122,plain,
( ~ v7_conlat_1(k1_funct_1(k4_conlat_2(sK3),sK4),sK3)
| ~ spl33_103
| ~ spl33_119 ),
inference(forward_subsumption_resolution,[],[f3119,f259]) ).
fof(f3123,plain,
( $false
| spl33_4
| spl33_13
| ~ spl33_103
| ~ spl33_119 ),
inference(forward_subsumption_resolution,[],[f3120,f259]) ).
fof(f3124,plain,
( spl33_4
| spl33_13
| ~ spl33_103
| ~ spl33_119 ),
inference(avatar_contradiction_clause,[],[f3123]) ).
fof(f3126,plain,
( ~ v9_conlat_1(k1_funct_1(k4_conlat_2(sK3),sK4),sK3)
| spl33_5
| spl33_13 ),
inference(forward_demodulation,[],[f478,f1865]) ).
fof(f3136,plain,
( $false
| spl33_5
| spl33_13
| ~ spl33_103
| ~ spl33_119 ),
inference(forward_subsumption_resolution,[],[f3121,f3126]) ).
fof(f3137,plain,
( spl33_5
| spl33_13
| ~ spl33_103
| ~ spl33_119 ),
inference(avatar_contradiction_clause,[],[f3136]) ).
fof(f3139,plain,
( v7_conlat_1(k1_funct_1(k4_conlat_2(sK3),sK4),sK3)
| ~ spl33_6
| spl33_13 ),
inference(forward_demodulation,[],[f482,f1865]) ).
fof(f3140,plain,
( $false
| ~ spl33_6
| spl33_13
| ~ spl33_103
| ~ spl33_119 ),
inference(forward_subsumption_resolution,[],[f3122,f3139]) ).
fof(f3141,plain,
( ~ spl33_6
| spl33_13
| ~ spl33_103
| ~ spl33_119 ),
inference(avatar_contradiction_clause,[],[f3140]) ).
fof(f3142,plain,
( v7_conlat_1(k1_funct_1(k5_conlat_2(sK3),sK5),sK3)
| ~ spl33_3
| spl33_11 ),
inference(forward_demodulation,[],[f470,f1840]) ).
fof(f3144,plain,
( $false
| ~ spl33_3
| spl33_11
| ~ spl33_103
| ~ spl33_114 ),
inference(forward_subsumption_resolution,[],[f3142,f3059]) ).
fof(f3145,plain,
( ~ spl33_3
| spl33_11
| ~ spl33_103
| ~ spl33_114 ),
inference(avatar_contradiction_clause,[],[f3144]) ).
cnf(s1,plain,
( ~ spl33_1
| ~ spl33_2
| spl33_3
| ~ spl33_4
| ~ spl33_5
| spl33_6 ),
inference(sat_conversion,[],[f483]) ).
cnf(s7,plain,
~ spl33_11,
inference(sat_conversion,[],[f625]) ).
cnf(s8,plain,
~ spl33_13,
inference(sat_conversion,[],[f635]) ).
cnf(s48,plain,
spl33_19,
inference(sat_conversion,[],[f1400]) ).
cnf(s50,plain,
( ~ spl33_19
| ~ spl33_20
| ~ spl33_21
| ~ spl33_22
| ~ spl33_23
| ~ spl33_24
| spl33_79 ),
inference(sat_conversion,[],[f1408]) ).
cnf(s51,plain,
spl33_20,
inference(sat_conversion,[],[f1416]) ).
cnf(s52,plain,
spl33_21,
inference(sat_conversion,[],[f1421]) ).
cnf(s55,plain,
spl33_22,
inference(sat_conversion,[],[f1493]) ).
cnf(s56,plain,
spl33_23,
inference(sat_conversion,[],[f1507]) ).
cnf(s57,plain,
spl33_24,
inference(sat_conversion,[],[f1519]) ).
cnf(s91,plain,
( ~ spl33_79
| spl33_103 ),
inference(sat_conversion,[],[f2324]) ).
cnf(s93,plain,
( spl33_11
| ~ spl33_109
| ~ spl33_110
| ~ spl33_111
| spl33_113
| spl33_114 ),
inference(sat_conversion,[],[f2357]) ).
cnf(s96,plain,
( spl33_13
| spl33_113
| ~ spl33_115
| ~ spl33_116
| ~ spl33_117
| spl33_119 ),
inference(sat_conversion,[],[f2386]) ).
cnf(s125,plain,
spl33_111,
inference(sat_conversion,[],[f2799]) ).
cnf(s129,plain,
spl33_117,
inference(sat_conversion,[],[f2863]) ).
cnf(s133,plain,
( ~ spl33_103
| spl33_109 ),
inference(sat_conversion,[],[f3031]) ).
cnf(s134,plain,
( ~ spl33_103
| spl33_110 ),
inference(sat_conversion,[],[f3035]) ).
cnf(s135,plain,
( ~ spl33_103
| ~ spl33_113 ),
inference(sat_conversion,[],[f3040]) ).
cnf(s136,plain,
( spl33_1
| spl33_11
| ~ spl33_103
| ~ spl33_114 ),
inference(sat_conversion,[],[f3061]) ).
cnf(s137,plain,
( spl33_2
| spl33_11
| ~ spl33_103
| ~ spl33_114 ),
inference(sat_conversion,[],[f3067]) ).
cnf(s138,plain,
( ~ spl33_103
| spl33_115 ),
inference(sat_conversion,[],[f3087]) ).
cnf(s139,plain,
( ~ spl33_103
| spl33_116 ),
inference(sat_conversion,[],[f3091]) ).
cnf(s141,plain,
( spl33_4
| spl33_13
| ~ spl33_103
| ~ spl33_119 ),
inference(sat_conversion,[],[f3124]) ).
cnf(s143,plain,
( spl33_5
| spl33_13
| ~ spl33_103
| ~ spl33_119 ),
inference(sat_conversion,[],[f3137]) ).
cnf(s144,plain,
( ~ spl33_6
| spl33_13
| ~ spl33_103
| ~ spl33_119 ),
inference(sat_conversion,[],[f3141]) ).
cnf(s145,plain,
( ~ spl33_3
| spl33_11
| ~ spl33_103
| ~ spl33_114 ),
inference(sat_conversion,[],[f3145]) ).
cnf(s154,plain,
( spl33_13
| spl33_113
| ~ spl33_115
| ~ spl33_116
| spl33_119 ),
inference(rat,[],[s96,s129]) ).
cnf(s156,plain,
( spl33_11
| ~ spl33_109
| ~ spl33_110
| spl33_113
| spl33_114 ),
inference(rat,[],[s93,s125]) ).
cnf(s174,plain,
( ~ spl33_19
| spl33_79 ),
inference(rat,[],[s50,s57,s56,s55,s52,s51]) ).
cnf(s178,plain,
spl33_79,
inference(rat,[],[s174,s48]) ).
cnf(s180,plain,
spl33_103,
inference(rat,[],[s91,s178]) ).
cnf(s182,plain,
spl33_116,
inference(rat,[],[s139,s180]) ).
cnf(s183,plain,
spl33_115,
inference(rat,[],[s138,s180]) ).
cnf(s184,plain,
~ spl33_113,
inference(rat,[],[s135,s180]) ).
cnf(s185,plain,
spl33_110,
inference(rat,[],[s134,s180]) ).
cnf(s186,plain,
spl33_109,
inference(rat,[],[s133,s180]) ).
cnf(s227,plain,
spl33_119,
inference(rat,[],[s154,s184,s182,s183,s8]) ).
cnf(s229,plain,
~ spl33_6,
inference(rat,[],[s144,s8,s180,s227]) ).
cnf(s230,plain,
spl33_5,
inference(rat,[],[s143,s8,s180,s227]) ).
cnf(s231,plain,
spl33_4,
inference(rat,[],[s141,s8,s180,s227]) ).
cnf(s233,plain,
spl33_114,
inference(rat,[],[s156,s186,s184,s185,s7]) ).
cnf(s235,plain,
~ spl33_3,
inference(rat,[],[s145,s7,s180,s233]) ).
cnf(s236,plain,
spl33_2,
inference(rat,[],[s137,s7,s180,s233]) ).
cnf(s237,plain,
spl33_1,
inference(rat,[],[s136,s7,s180,s233]) ).
cnf(s240,plain,
$false,
inference(rat,[],[s1,s229,s230,s231,s235,s236,s237]) ).
fof(f3146,plain,
$false,
inference(avatar_sat_refutation,[],[s240]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT343+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n003.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 14:52:11 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.54 % (622339)Will run a generic schedule for satisfiability detection.
% 0.19/0.54 % (622349)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3048090031:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.54 % (622345)% WARNING: option uhcvi not known.
% 0.19/0.54 % (622344)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=902630891_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.54 % (622345)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1105083247:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.54 % (622346)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3808835945:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.54 % (622347)dis+10_1_sil=32000:sp=arity:random_seed=2557632522:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.54 % (622348)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=441482998:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.54 % (622350)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2728670681:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.54 % TRYING [1]
% 0.19/0.54 % TRYING [2]
% 0.19/0.54 % TRYING [3]
% 0.19/0.54 % TRYING [4]
% 0.19/0.54 % (622349)Instruction limit reached!
% 0.19/0.54 % (622349)------------------------------
% 0.19/0.54 % (622349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.54 % (622349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.54 % (622349)CaDiCaL version: 2.1.3
% 0.19/0.54 % (622349)Termination reason: Instruction limit
% 0.19/0.54 % (622349)Termination phase: Saturation
% 0.19/0.54 % (622349)Time elapsed: 0.040 s
% 0.19/0.54 % (622349)Peak memory usage: 14 MB
% 0.19/0.54 % (622349)Instructions burned: 132 (million)
% 0.19/0.54 % (622358)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=672561392:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.19/0.54 % TRYING [1]
% 0.19/0.54 % (622347) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-622339-622347"...
% 0.19/0.54 % TRYING [2]
% 0.19/0.54 % TRYING [5]
% 0.19/0.54 % TRYING [3]
% 0.19/0.54 % (622347)...printing done.
% 0.19/0.54 % (622347)Refutation found. Thanks to Tanya!
% 0.19/0.54 % SZS status Theorem for theBenchmark
% 0.19/0.54 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.55 % (622347)------------------------------
% 0.19/0.55 % (622347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.55 % (622347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.55 % (622347)CaDiCaL version: 2.1.3
% 0.19/0.55 % (622347)Termination reason: Refutation
% 0.19/0.55 % (622347)Time elapsed: 0.067 s
% 0.19/0.55 % (622347)Peak memory usage: 14 MB
% 0.19/0.55 % (622347)Instructions burned: 103 (million)
% 0.19/0.55 % (622339)Success in time 0.119 s
% 0.19/0.55 % Vampire exiting
%------------------------------------------------------------------------------