%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT343+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 : n018.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:08 AM UTC 2026
% Result : Theorem 32.29s 12.04s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 24
% Syntax : Number of formulae : 234 ( 31 unt; 11 def)
% Number of atoms : 925 ( 139 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 1163 ( 472 ~; 511 |; 134 &)
% ( 17 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 25 ( 23 usr; 12 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 3 con; 0-4 aty)
% Number of variables : 235 ( 0 sgn 205 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f2300,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,X0) )
=> m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_domain_1) ).
fof(f2301,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,X0) )
=> k6_domain_1(X0,X1) = k1_tarski(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_domain_1) ).
fof(f46198,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(f46199,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(f46242,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_conlat_1(X0)))
=> ( ~ v7_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X0)
& v9_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X0)
& l3_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X0)
& ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_conlat_1(X0)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u2_conlat_1(X0)))
=> ( ( ~ v7_conlat_1(g3_conlat_1(X0,X2,X3),X0)
& v9_conlat_1(g3_conlat_1(X0,X2,X3),X0)
& l3_conlat_1(g3_conlat_1(X0,X2,X3),X0)
& r1_tarski(X1,X2) )
=> r1_tarski(k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X2) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_conlat_1) ).
fof(f46244,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u2_conlat_1(X0)))
=> ( ~ v7_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1))),X0)
& v9_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1))),X0)
& l3_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1))),X0)
& ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_conlat_1(X0)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u2_conlat_1(X0)))
=> ( ( ~ v7_conlat_1(g3_conlat_1(X0,X2,X3),X0)
& v9_conlat_1(g3_conlat_1(X0,X2,X3),X0)
& l3_conlat_1(g3_conlat_1(X0,X2,X3),X0)
& r1_tarski(X1,X3) )
=> r1_tarski(k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1)),X3) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t22_conlat_1) ).
fof(f46291,axiom,
! [X0] :
( l2_conlat_1(X0)
=> l1_conlat_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_conlat_1) ).
fof(f49785,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(f49786,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(f49807,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
& m2_relset_1(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
=> ( X1 = k4_conlat_2(X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_conlat_1(X0))
=> ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
& k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X2) = g3_conlat_1(X0,X3,X4)
& X3 = k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X2)))
& X4 = k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_conlat_2) ).
fof(f49808,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
& m2_relset_1(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
=> ( X1 = k5_conlat_2(X0)
<=> ! [X2] :
( m1_subset_1(X2,u2_conlat_1(X0))
=> ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
& k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X2) = g3_conlat_1(X0,X3,X4)
& X3 = k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X2))
& X4 = k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X2))) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_conlat_2) ).
fof(f49809,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(f49810,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)],[f49809]) ).
fof(f49935,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,[],[f49785]) ).
fof(f49936,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,[],[f49935]) ).
fof(f49937,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,[],[f49786]) ).
fof(f49938,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,[],[f49937]) ).
fof(f49979,plain,
! [X0] :
( ! [X1] :
( ( X1 = k4_conlat_2(X0)
<=> ! [X2] :
( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
& k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X2) = g3_conlat_1(X0,X3,X4)
& X3 = k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X2)))
& X4 = k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X2)) ) )
| ~ m1_subset_1(X2,u1_conlat_1(X0)) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f49807]) ).
fof(f49980,plain,
! [X0] :
( ! [X1] :
( ( X1 = k4_conlat_2(X0)
<=> ! [X2] :
( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
& k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X2) = g3_conlat_1(X0,X3,X4)
& X3 = k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X2)))
& X4 = k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X2)) ) )
| ~ m1_subset_1(X2,u1_conlat_1(X0)) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f49979]) ).
fof(f49981,plain,
! [X0] :
( ! [X1] :
( ( X1 = k5_conlat_2(X0)
<=> ! [X2] :
( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
& k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X2) = g3_conlat_1(X0,X3,X4)
& X3 = k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X2))
& X4 = k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X2))) ) )
| ~ m1_subset_1(X2,u2_conlat_1(X0)) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f49808]) ).
fof(f49982,plain,
! [X0] :
( ! [X1] :
( ( X1 = k5_conlat_2(X0)
<=> ! [X2] :
( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
& k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X2) = g3_conlat_1(X0,X3,X4)
& X3 = k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X2))
& X4 = k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X2))) ) )
| ~ m1_subset_1(X2,u2_conlat_1(X0)) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f49981]) ).
fof(f49983,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,[],[f49810]) ).
fof(f49984,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,[],[f49983]) ).
fof(f50306,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f2301]) ).
fof(f50307,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f50306]) ).
fof(f50308,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f2300]) ).
fof(f50309,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f50308]) ).
fof(f50316,plain,
! [X0] :
( ! [X1] :
( ( ~ v7_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1))),X0)
& v9_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1))),X0)
& l3_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1))),X0)
& ! [X2] :
( ! [X3] :
( r1_tarski(k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1)),X3)
| v7_conlat_1(g3_conlat_1(X0,X2,X3),X0)
| ~ v9_conlat_1(g3_conlat_1(X0,X2,X3),X0)
| ~ l3_conlat_1(g3_conlat_1(X0,X2,X3),X0)
| ~ r1_tarski(X1,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u2_conlat_1(X0))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_conlat_1(X0))) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u2_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f46244]) ).
fof(f50317,plain,
! [X0] :
( ! [X1] :
( ( ~ v7_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1))),X0)
& v9_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1))),X0)
& l3_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1))),X0)
& ! [X2] :
( ! [X3] :
( r1_tarski(k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1)),X3)
| v7_conlat_1(g3_conlat_1(X0,X2,X3),X0)
| ~ v9_conlat_1(g3_conlat_1(X0,X2,X3),X0)
| ~ l3_conlat_1(g3_conlat_1(X0,X2,X3),X0)
| ~ r1_tarski(X1,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u2_conlat_1(X0))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_conlat_1(X0))) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u2_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f50316]) ).
fof(f50320,plain,
! [X0] :
( ! [X1] :
( ( ~ v7_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X0)
& v9_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X0)
& l3_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X0)
& ! [X2] :
( ! [X3] :
( r1_tarski(k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X2)
| v7_conlat_1(g3_conlat_1(X0,X2,X3),X0)
| ~ v9_conlat_1(g3_conlat_1(X0,X2,X3),X0)
| ~ l3_conlat_1(g3_conlat_1(X0,X2,X3),X0)
| ~ r1_tarski(X1,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u2_conlat_1(X0))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_conlat_1(X0))) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f46242]) ).
fof(f50321,plain,
! [X0] :
( ! [X1] :
( ( ~ v7_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X0)
& v9_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X0)
& l3_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X0)
& ! [X2] :
( ! [X3] :
( r1_tarski(k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X2)
| v7_conlat_1(g3_conlat_1(X0,X2,X3),X0)
| ~ v9_conlat_1(g3_conlat_1(X0,X2,X3),X0)
| ~ l3_conlat_1(g3_conlat_1(X0,X2,X3),X0)
| ~ r1_tarski(X1,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u2_conlat_1(X0))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_conlat_1(X0))) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f50320]) ).
fof(f52290,plain,
! [X0] :
( l1_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f46291]) ).
fof(f52299,plain,
! [X0] :
( ~ v1_xboole_0(u1_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l1_conlat_1(X0) ),
inference(ennf_transformation,[],[f46199]) ).
fof(f52300,plain,
! [X0] :
( ~ v1_xboole_0(u1_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l1_conlat_1(X0) ),
inference(flattening,[],[f52299]) ).
fof(f52301,plain,
! [X0] :
( ~ v1_xboole_0(u2_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l1_conlat_1(X0) ),
inference(ennf_transformation,[],[f46198]) ).
fof(f52302,plain,
! [X0] :
( ~ v1_xboole_0(u2_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l1_conlat_1(X0) ),
inference(flattening,[],[f52301]) ).
fof(f59347,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k4_conlat_2(X0)
| ? [X2] :
( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
| k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X2) != g3_conlat_1(X0,X3,X4)
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X2))) != X3
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X2)) != X4 ) )
& m1_subset_1(X2,u1_conlat_1(X0)) ) )
& ( ! [X2] :
( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
& k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X2) = g3_conlat_1(X0,X3,X4)
& X3 = k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X2)))
& X4 = k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X2)) ) )
| ~ m1_subset_1(X2,u1_conlat_1(X0)) )
| k4_conlat_2(X0) != X1 ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(nnf_transformation,[],[f49980]) ).
fof(f59348,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k4_conlat_2(X0)
| ? [X2] :
( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
| k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X2) != g3_conlat_1(X0,X3,X4)
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X2))) != X3
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X2)) != X4 ) )
& m1_subset_1(X2,u1_conlat_1(X0)) ) )
& ( ! [X5] :
( ? [X6] :
( m1_subset_1(X6,k1_zfmisc_1(u1_conlat_1(X0)))
& ? [X7] :
( m1_subset_1(X7,k1_zfmisc_1(u2_conlat_1(X0)))
& k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X5) = g3_conlat_1(X0,X6,X7)
& k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X5))) = X6
& k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X5)) = X7 ) )
| ~ m1_subset_1(X5,u1_conlat_1(X0)) )
| k4_conlat_2(X0) != X1 ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(rectify,[],[f59347]) ).
fof(f59349,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k4_conlat_2(X0)
| ( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
| g3_conlat_1(X0,X3,X4) != k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,sK56(X0,X1))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),sK56(X0,X1)))) != X3
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),sK56(X0,X1))) != X4 ) )
& m1_subset_1(sK56(X0,X1),u1_conlat_1(X0)) ) )
& ( ! [X5] :
( ( m1_subset_1(sK57(X0,X1,X5),k1_zfmisc_1(u1_conlat_1(X0)))
& m1_subset_1(sK58(X0,X1,X5),k1_zfmisc_1(u2_conlat_1(X0)))
& k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X5) = g3_conlat_1(X0,sK57(X0,X1,X5),sK58(X0,X1,X5))
& k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X5))) = sK57(X0,X1,X5)
& k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X5)) = sK58(X0,X1,X5) )
| ~ m1_subset_1(X5,u1_conlat_1(X0)) )
| k4_conlat_2(X0) != X1 ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56,sK57,sK58]),skolemize(X2,sK56(X0,X1)),skolemize(X6,sK57(X0,X1,X5)),skolemize(X7,sK58(X0,X1,X5))],[f59348]) ).
fof(f59350,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k5_conlat_2(X0)
| ? [X2] :
( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
| g3_conlat_1(X0,X3,X4) != k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X2)
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X2)) != X3
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X2))) != X4 ) )
& m1_subset_1(X2,u2_conlat_1(X0)) ) )
& ( ! [X2] :
( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
& k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X2) = g3_conlat_1(X0,X3,X4)
& X3 = k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X2))
& X4 = k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X2))) ) )
| ~ m1_subset_1(X2,u2_conlat_1(X0)) )
| k5_conlat_2(X0) != X1 ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(nnf_transformation,[],[f49982]) ).
fof(f59351,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k5_conlat_2(X0)
| ? [X2] :
( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
| g3_conlat_1(X0,X3,X4) != k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X2)
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X2)) != X3
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X2))) != X4 ) )
& m1_subset_1(X2,u2_conlat_1(X0)) ) )
& ( ! [X5] :
( ? [X6] :
( m1_subset_1(X6,k1_zfmisc_1(u1_conlat_1(X0)))
& ? [X7] :
( m1_subset_1(X7,k1_zfmisc_1(u2_conlat_1(X0)))
& g3_conlat_1(X0,X6,X7) = k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X5)
& k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X5)) = X6
& k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X5))) = X7 ) )
| ~ m1_subset_1(X5,u2_conlat_1(X0)) )
| k5_conlat_2(X0) != X1 ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(rectify,[],[f59350]) ).
fof(f59352,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k5_conlat_2(X0)
| ( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_conlat_1(X0)))
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u2_conlat_1(X0)))
| g3_conlat_1(X0,X3,X4) != k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,sK59(X0,X1))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),sK59(X0,X1))) != X3
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),sK59(X0,X1)))) != X4 ) )
& m1_subset_1(sK59(X0,X1),u2_conlat_1(X0)) ) )
& ( ! [X5] :
( ( m1_subset_1(sK60(X0,X1,X5),k1_zfmisc_1(u1_conlat_1(X0)))
& m1_subset_1(sK61(X0,X1,X5),k1_zfmisc_1(u2_conlat_1(X0)))
& k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X5) = g3_conlat_1(X0,sK60(X0,X1,X5),sK61(X0,X1,X5))
& k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X5)) = sK60(X0,X1,X5)
& k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X5))) = sK61(X0,X1,X5) )
| ~ m1_subset_1(X5,u2_conlat_1(X0)) )
| k5_conlat_2(X0) != X1 ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK59,sK60,sK61]),skolemize(X2,sK59(X0,X1)),skolemize(X6,sK60(X0,X1,X5)),skolemize(X7,sK61(X0,X1,X5))],[f59351]) ).
fof(f59353,plain,
( ( v7_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62)
| ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62) )
& m1_subset_1(sK64,u2_conlat_1(sK62))
& m1_subset_1(sK63,u1_conlat_1(sK62))
& ~ v3_conlat_1(sK62)
& l2_conlat_1(sK62) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62,sK63,sK64]),skolemize(X0,sK62),skolemize(X1,sK63),skolemize(X2,sK64)],[f49984]) ).
fof(f61987,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,[],[f49936]) ).
fof(f61988,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,[],[f49936]) ).
fof(f61989,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| v1_funct_1(k4_conlat_2(X0)) ),
inference(cnf_transformation,[],[f49936]) ).
fof(f61990,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,[],[f49938]) ).
fof(f61991,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,[],[f49938]) ).
fof(f61992,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| v1_funct_1(k5_conlat_2(X0)) ),
inference(cnf_transformation,[],[f49938]) ).
fof(f62043,plain,
! [X0,X1,X5] :
( k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X5)) = sK58(X0,X1,X5)
| ~ m1_subset_1(X5,u1_conlat_1(X0))
| k4_conlat_2(X0) != X1
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f59349]) ).
fof(f62044,plain,
! [X0,X1,X5] :
( k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X5))) = sK57(X0,X1,X5)
| ~ m1_subset_1(X5,u1_conlat_1(X0))
| k4_conlat_2(X0) != X1
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f59349]) ).
fof(f62045,plain,
! [X0,X1,X5] :
( k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X5) = g3_conlat_1(X0,sK57(X0,X1,X5),sK58(X0,X1,X5))
| ~ m1_subset_1(X5,u1_conlat_1(X0))
| k4_conlat_2(X0) != X1
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f59349]) ).
fof(f62050,plain,
! [X0,X1,X5] :
( k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X5))) = sK61(X0,X1,X5)
| ~ m1_subset_1(X5,u2_conlat_1(X0))
| k5_conlat_2(X0) != X1
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f59352]) ).
fof(f62051,plain,
! [X0,X1,X5] :
( k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X5)) = sK60(X0,X1,X5)
| ~ m1_subset_1(X5,u2_conlat_1(X0))
| k5_conlat_2(X0) != X1
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f59352]) ).
fof(f62052,plain,
! [X0,X1,X5] :
( k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),X1,X5) = g3_conlat_1(X0,sK60(X0,X1,X5),sK61(X0,X1,X5))
| ~ m1_subset_1(X5,u2_conlat_1(X0))
| k5_conlat_2(X0) != X1
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ m2_relset_1(X1,u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f59352]) ).
fof(f62057,plain,
l2_conlat_1(sK62),
inference(cnf_transformation,[],[f59353]) ).
fof(f62058,plain,
~ v3_conlat_1(sK62),
inference(cnf_transformation,[],[f59353]) ).
fof(f62059,plain,
m1_subset_1(sK63,u1_conlat_1(sK62)),
inference(cnf_transformation,[],[f59353]) ).
fof(f62060,plain,
m1_subset_1(sK64,u2_conlat_1(sK62)),
inference(cnf_transformation,[],[f59353]) ).
fof(f62061,plain,
( v7_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62)
| ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62) ),
inference(cnf_transformation,[],[f59353]) ).
fof(f62684,plain,
! [X0,X1] :
( k1_tarski(X1) = k6_domain_1(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(cnf_transformation,[],[f50307]) ).
fof(f62685,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| v1_xboole_0(X0)
| m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f50309]) ).
fof(f62697,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u2_conlat_1(X0)))
| v3_conlat_1(X0)
| l3_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1))),X0) ),
inference(cnf_transformation,[],[f50317]) ).
fof(f62698,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u2_conlat_1(X0)))
| v3_conlat_1(X0)
| v9_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1))),X0) ),
inference(cnf_transformation,[],[f50317]) ).
fof(f62699,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u2_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ v7_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),X1))),X0) ),
inference(cnf_transformation,[],[f50317]) ).
fof(f62706,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_conlat_1(X0)))
| v3_conlat_1(X0)
| l3_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X0) ),
inference(cnf_transformation,[],[f50321]) ).
fof(f62707,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_conlat_1(X0)))
| v3_conlat_1(X0)
| v9_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X0) ),
inference(cnf_transformation,[],[f50321]) ).
fof(f62708,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ v7_conlat_1(g3_conlat_1(X0,k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),X1)),X0) ),
inference(cnf_transformation,[],[f50321]) ).
fof(f63605,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f65856,plain,
! [X0] :
( l1_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f52290]) ).
fof(f65870,plain,
! [X0] :
( ~ v1_xboole_0(u1_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l1_conlat_1(X0) ),
inference(cnf_transformation,[],[f52300]) ).
fof(f65871,plain,
! [X0] :
( ~ v1_xboole_0(u2_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l1_conlat_1(X0) ),
inference(cnf_transformation,[],[f52302]) ).
fof(f75221,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| v1_xboole_0(X0)
| k6_domain_1(X0,X1) = k2_tarski(X1,X1) ),
inference(definition_unfolding,[],[f62684,f63605]) ).
fof(f77291,plain,
! [X0,X5] :
( ~ v1_funct_1(k4_conlat_2(X0))
| ~ m1_subset_1(X5,u1_conlat_1(X0))
| k8_funct_2(u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k4_conlat_2(X0),X5) = g3_conlat_1(X0,sK57(X0,k4_conlat_2(X0),X5),sK58(X0,k4_conlat_2(X0),X5))
| ~ 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(equality_resolution,[],[f62045]) ).
fof(f77292,plain,
! [X0,X5] :
( ~ v1_funct_1(k4_conlat_2(X0))
| ~ m1_subset_1(X5,u1_conlat_1(X0))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X5))) = sK57(X0,k4_conlat_2(X0),X5)
| ~ 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(equality_resolution,[],[f62044]) ).
fof(f77293,plain,
! [X0,X5] :
( ~ v1_funct_1(k4_conlat_2(X0))
| ~ m1_subset_1(X5,u1_conlat_1(X0))
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k6_domain_1(u1_conlat_1(X0),X5)) = sK58(X0,k4_conlat_2(X0),X5)
| ~ 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(equality_resolution,[],[f62043]) ).
fof(f77298,plain,
! [X0,X5] :
( ~ v1_funct_1(k5_conlat_2(X0))
| ~ m1_subset_1(X5,u2_conlat_1(X0))
| k8_funct_2(u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)),k5_conlat_2(X0),X5) = g3_conlat_1(X0,sK60(X0,k5_conlat_2(X0),X5),sK61(X0,k5_conlat_2(X0),X5))
| ~ 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(equality_resolution,[],[f62052]) ).
fof(f77299,plain,
! [X0,X5] :
( ~ v1_funct_1(k5_conlat_2(X0))
| ~ m1_subset_1(X5,u2_conlat_1(X0))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X5)) = sK60(X0,k5_conlat_2(X0),X5)
| ~ 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(equality_resolution,[],[f62051]) ).
fof(f77300,plain,
! [X0,X5] :
( ~ v1_funct_1(k5_conlat_2(X0))
| ~ m1_subset_1(X5,u2_conlat_1(X0))
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(X0)),k1_zfmisc_1(u2_conlat_1(X0)),k1_conlat_1(X0),k8_funct_2(k1_zfmisc_1(u2_conlat_1(X0)),k1_zfmisc_1(u1_conlat_1(X0)),k2_conlat_1(X0),k6_domain_1(u2_conlat_1(X0),X5))) = sK61(X0,k5_conlat_2(X0),X5)
| ~ 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(equality_resolution,[],[f62050]) ).
fof(f79173,definition,
( spl1780_63
<=> l3_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62) ),
introduced(definition,[new_symbols(definition,[spl1780_63])],[avatar_definition]) ).
fof(f79174,plain,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62)
| spl1780_63 ),
inference(avatar_component_clause,[],[f79173]) ).
fof(f79176,definition,
( spl1780_64
<=> v9_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62) ),
introduced(definition,[new_symbols(definition,[spl1780_64])],[avatar_definition]) ).
fof(f79177,plain,
( ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62)
| spl1780_64 ),
inference(avatar_component_clause,[],[f79176]) ).
fof(f79179,definition,
( spl1780_65
<=> v7_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62) ),
introduced(definition,[new_symbols(definition,[spl1780_65])],[avatar_definition]) ).
fof(f79180,plain,
( v7_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62)
| ~ spl1780_65 ),
inference(avatar_component_clause,[],[f79179]) ).
fof(f79182,definition,
( spl1780_66
<=> l3_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62) ),
introduced(definition,[new_symbols(definition,[spl1780_66])],[avatar_definition]) ).
fof(f79183,plain,
( ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62)
| spl1780_66 ),
inference(avatar_component_clause,[],[f79182]) ).
fof(f79185,definition,
( spl1780_67
<=> v9_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62) ),
introduced(definition,[new_symbols(definition,[spl1780_67])],[avatar_definition]) ).
fof(f79186,plain,
( ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62)
| spl1780_67 ),
inference(avatar_component_clause,[],[f79185]) ).
fof(f79188,definition,
( spl1780_68
<=> v7_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62) ),
introduced(definition,[new_symbols(definition,[spl1780_68])],[avatar_definition]) ).
fof(f79189,plain,
( v7_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62)
| ~ spl1780_68 ),
inference(avatar_component_clause,[],[f79188]) ).
fof(f79190,plain,
( ~ spl1780_63
| ~ spl1780_64
| spl1780_65
| ~ spl1780_66
| ~ spl1780_67
| spl1780_68 ),
inference(avatar_split_clause,[],[f62061,f79188,f79185,f79182,f79179,f79176,f79173]) ).
fof(f79474,plain,
( v3_conlat_1(sK62)
| v1_funct_1(k4_conlat_2(sK62)) ),
inference(resolution,[],[f61989,f62057]) ).
fof(f79475,plain,
v1_funct_1(k4_conlat_2(sK62)),
inference(forward_subsumption_resolution,[],[f79474,f62058]) ).
fof(f79476,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k6_domain_1(u1_conlat_1(sK62),X0))) = sK57(sK62,k4_conlat_2(sK62),X0)
| ~ v1_funct_2(k4_conlat_2(sK62),u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| ~ m2_relset_1(k4_conlat_2(sK62),u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(resolution,[],[f79475,f77292]) ).
fof(f79477,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),X0) = g3_conlat_1(sK62,sK57(sK62,k4_conlat_2(sK62),X0),sK58(sK62,k4_conlat_2(sK62),X0))
| ~ v1_funct_2(k4_conlat_2(sK62),u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| ~ m2_relset_1(k4_conlat_2(sK62),u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(resolution,[],[f79475,f77291]) ).
fof(f79478,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k6_domain_1(u1_conlat_1(sK62),X0)) = sK58(sK62,k4_conlat_2(sK62),X0)
| ~ v1_funct_2(k4_conlat_2(sK62),u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| ~ m2_relset_1(k4_conlat_2(sK62),u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(resolution,[],[f79475,f77293]) ).
fof(f79479,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k6_domain_1(u1_conlat_1(sK62),X0)) = sK58(sK62,k4_conlat_2(sK62),X0)
| ~ m2_relset_1(k4_conlat_2(sK62),u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79478,f61988]) ).
fof(f79480,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),X0) = g3_conlat_1(sK62,sK57(sK62,k4_conlat_2(sK62),X0),sK58(sK62,k4_conlat_2(sK62),X0))
| ~ m2_relset_1(k4_conlat_2(sK62),u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79477,f61988]) ).
fof(f79481,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k6_domain_1(u1_conlat_1(sK62),X0))) = sK57(sK62,k4_conlat_2(sK62),X0)
| ~ m2_relset_1(k4_conlat_2(sK62),u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79476,f61988]) ).
fof(f79482,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k6_domain_1(u1_conlat_1(sK62),X0)) = sK58(sK62,k4_conlat_2(sK62),X0)
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79479,f61987]) ).
fof(f79483,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),X0) = g3_conlat_1(sK62,sK57(sK62,k4_conlat_2(sK62),X0),sK58(sK62,k4_conlat_2(sK62),X0))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79480,f61987]) ).
fof(f79484,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k6_domain_1(u1_conlat_1(sK62),X0))) = sK57(sK62,k4_conlat_2(sK62),X0)
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79481,f61987]) ).
fof(f79485,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k6_domain_1(u1_conlat_1(sK62),X0)) = sK58(sK62,k4_conlat_2(sK62),X0)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79482,f62058]) ).
fof(f79486,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),X0) = g3_conlat_1(sK62,sK57(sK62,k4_conlat_2(sK62),X0),sK58(sK62,k4_conlat_2(sK62),X0))
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79483,f62058]) ).
fof(f79487,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k6_domain_1(u1_conlat_1(sK62),X0))) = sK57(sK62,k4_conlat_2(sK62),X0)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79484,f62058]) ).
fof(f79488,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k6_domain_1(u1_conlat_1(sK62),X0)) = sK58(sK62,k4_conlat_2(sK62),X0) ),
inference(forward_subsumption_resolution,[],[f79485,f62057]) ).
fof(f79489,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),X0) = g3_conlat_1(sK62,sK57(sK62,k4_conlat_2(sK62),X0),sK58(sK62,k4_conlat_2(sK62),X0)) ),
inference(forward_subsumption_resolution,[],[f79486,f62057]) ).
fof(f79490,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k6_domain_1(u1_conlat_1(sK62),X0))) = sK57(sK62,k4_conlat_2(sK62),X0) ),
inference(forward_subsumption_resolution,[],[f79487,f62057]) ).
fof(f79491,plain,
k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k6_domain_1(u1_conlat_1(sK62),sK63)) = sK58(sK62,k4_conlat_2(sK62),sK63),
inference(resolution,[],[f79488,f62059]) ).
fof(f79492,plain,
k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k6_domain_1(u1_conlat_1(sK62),sK63))) = sK57(sK62,k4_conlat_2(sK62),sK63),
inference(resolution,[],[f79490,f62059]) ).
fof(f79493,plain,
sK57(sK62,k4_conlat_2(sK62),sK63) = k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),sK58(sK62,k4_conlat_2(sK62),sK63)),
inference(forward_demodulation,[],[f79492,f79491]) ).
fof(f79494,plain,
( v3_conlat_1(sK62)
| v1_funct_1(k5_conlat_2(sK62)) ),
inference(resolution,[],[f61992,f62057]) ).
fof(f79495,plain,
v1_funct_1(k5_conlat_2(sK62)),
inference(forward_subsumption_resolution,[],[f79494,f62058]) ).
fof(f79496,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k6_domain_1(u2_conlat_1(sK62),X0))) = sK61(sK62,k5_conlat_2(sK62),X0)
| ~ v1_funct_2(k5_conlat_2(sK62),u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| ~ m2_relset_1(k5_conlat_2(sK62),u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(resolution,[],[f79495,f77300]) ).
fof(f79497,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),X0) = g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),X0),sK61(sK62,k5_conlat_2(sK62),X0))
| ~ v1_funct_2(k5_conlat_2(sK62),u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| ~ m2_relset_1(k5_conlat_2(sK62),u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(resolution,[],[f79495,f77298]) ).
fof(f79498,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k6_domain_1(u2_conlat_1(sK62),X0)) = sK60(sK62,k5_conlat_2(sK62),X0)
| ~ v1_funct_2(k5_conlat_2(sK62),u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| ~ m2_relset_1(k5_conlat_2(sK62),u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(resolution,[],[f79495,f77299]) ).
fof(f79499,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k6_domain_1(u2_conlat_1(sK62),X0)) = sK60(sK62,k5_conlat_2(sK62),X0)
| ~ m2_relset_1(k5_conlat_2(sK62),u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79498,f61991]) ).
fof(f79500,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),X0) = g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),X0),sK61(sK62,k5_conlat_2(sK62),X0))
| ~ m2_relset_1(k5_conlat_2(sK62),u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79497,f61991]) ).
fof(f79501,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k6_domain_1(u2_conlat_1(sK62),X0))) = sK61(sK62,k5_conlat_2(sK62),X0)
| ~ m2_relset_1(k5_conlat_2(sK62),u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79496,f61991]) ).
fof(f79502,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k6_domain_1(u2_conlat_1(sK62),X0)) = sK60(sK62,k5_conlat_2(sK62),X0)
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79499,f61990]) ).
fof(f79503,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),X0) = g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),X0),sK61(sK62,k5_conlat_2(sK62),X0))
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79500,f61990]) ).
fof(f79504,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k6_domain_1(u2_conlat_1(sK62),X0))) = sK61(sK62,k5_conlat_2(sK62),X0)
| v3_conlat_1(sK62)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79501,f61990]) ).
fof(f79505,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k6_domain_1(u2_conlat_1(sK62),X0)) = sK60(sK62,k5_conlat_2(sK62),X0)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79502,f62058]) ).
fof(f79506,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),X0) = g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),X0),sK61(sK62,k5_conlat_2(sK62),X0))
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79503,f62058]) ).
fof(f79507,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k6_domain_1(u2_conlat_1(sK62),X0))) = sK61(sK62,k5_conlat_2(sK62),X0)
| ~ l2_conlat_1(sK62) ),
inference(forward_subsumption_resolution,[],[f79504,f62058]) ).
fof(f79508,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k6_domain_1(u2_conlat_1(sK62),X0)) = sK60(sK62,k5_conlat_2(sK62),X0) ),
inference(forward_subsumption_resolution,[],[f79505,f62057]) ).
fof(f79509,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),X0) = g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),X0),sK61(sK62,k5_conlat_2(sK62),X0)) ),
inference(forward_subsumption_resolution,[],[f79506,f62057]) ).
fof(f79510,plain,
! [X0] :
( ~ m1_subset_1(X0,u2_conlat_1(sK62))
| k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k6_domain_1(u2_conlat_1(sK62),X0))) = sK61(sK62,k5_conlat_2(sK62),X0) ),
inference(forward_subsumption_resolution,[],[f79507,f62057]) ).
fof(f79511,plain,
k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k6_domain_1(u2_conlat_1(sK62),sK64)) = sK60(sK62,k5_conlat_2(sK62),sK64),
inference(resolution,[],[f79508,f62060]) ).
fof(f79512,plain,
k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k6_domain_1(u2_conlat_1(sK62),sK64))) = sK61(sK62,k5_conlat_2(sK62),sK64),
inference(resolution,[],[f79510,f62060]) ).
fof(f79513,plain,
sK61(sK62,k5_conlat_2(sK62),sK64) = k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),sK60(sK62,k5_conlat_2(sK62),sK64)),
inference(forward_demodulation,[],[f79512,f79511]) ).
fof(f79514,plain,
k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64) = g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),sK64),sK61(sK62,k5_conlat_2(sK62),sK64)),
inference(resolution,[],[f79509,f62060]) ).
fof(f79515,plain,
k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63) = g3_conlat_1(sK62,sK57(sK62,k4_conlat_2(sK62),sK63),sK58(sK62,k4_conlat_2(sK62),sK63)),
inference(resolution,[],[f79489,f62059]) ).
fof(f79632,plain,
( v1_xboole_0(u1_conlat_1(sK62))
| m1_subset_1(k6_domain_1(u1_conlat_1(sK62),sK63),k1_zfmisc_1(u1_conlat_1(sK62))) ),
inference(resolution,[],[f62685,f62059]) ).
fof(f79633,plain,
( v1_xboole_0(u2_conlat_1(sK62))
| m1_subset_1(k6_domain_1(u2_conlat_1(sK62),sK64),k1_zfmisc_1(u2_conlat_1(sK62))) ),
inference(resolution,[],[f62685,f62060]) ).
fof(f79635,definition,
( spl1780_93
<=> m1_subset_1(k6_domain_1(u2_conlat_1(sK62),sK64),k1_zfmisc_1(u2_conlat_1(sK62))) ),
introduced(definition,[new_symbols(definition,[spl1780_93])],[avatar_definition]) ).
fof(f79636,plain,
( m1_subset_1(k6_domain_1(u2_conlat_1(sK62),sK64),k1_zfmisc_1(u2_conlat_1(sK62)))
| ~ spl1780_93 ),
inference(avatar_component_clause,[],[f79635]) ).
fof(f79638,definition,
( spl1780_94
<=> v1_xboole_0(u2_conlat_1(sK62)) ),
introduced(definition,[new_symbols(definition,[spl1780_94])],[avatar_definition]) ).
fof(f79639,plain,
( v1_xboole_0(u2_conlat_1(sK62))
| ~ spl1780_94 ),
inference(avatar_component_clause,[],[f79638]) ).
fof(f79640,plain,
( spl1780_93
| spl1780_94 ),
inference(avatar_split_clause,[],[f79633,f79638,f79635]) ).
fof(f79642,definition,
( spl1780_95
<=> m1_subset_1(k6_domain_1(u1_conlat_1(sK62),sK63),k1_zfmisc_1(u1_conlat_1(sK62))) ),
introduced(definition,[new_symbols(definition,[spl1780_95])],[avatar_definition]) ).
fof(f79643,plain,
( m1_subset_1(k6_domain_1(u1_conlat_1(sK62),sK63),k1_zfmisc_1(u1_conlat_1(sK62)))
| ~ spl1780_95 ),
inference(avatar_component_clause,[],[f79642]) ).
fof(f79645,definition,
( spl1780_96
<=> v1_xboole_0(u1_conlat_1(sK62)) ),
introduced(definition,[new_symbols(definition,[spl1780_96])],[avatar_definition]) ).
fof(f79646,plain,
( v1_xboole_0(u1_conlat_1(sK62))
| ~ spl1780_96 ),
inference(avatar_component_clause,[],[f79645]) ).
fof(f79647,plain,
( spl1780_95
| spl1780_96 ),
inference(avatar_split_clause,[],[f79632,f79645,f79642]) ).
fof(f79679,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ v7_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),X0)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),X0)),sK62) ),
inference(resolution,[],[f62708,f62057]) ).
fof(f79681,plain,
! [X0] :
( ~ v7_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),X0)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),X0)),sK62)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_conlat_1(sK62))) ),
inference(forward_subsumption_resolution,[],[f79679,f62058]) ).
fof(f79683,plain,
( ~ v7_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),sK58(sK62,k4_conlat_2(sK62),sK63)),sK58(sK62,k4_conlat_2(sK62),sK63)),sK62)
| ~ m1_subset_1(k6_domain_1(u1_conlat_1(sK62),sK63),k1_zfmisc_1(u1_conlat_1(sK62))) ),
inference(superposition,[],[f79681,f79491]) ).
fof(f79684,plain,
( ~ v7_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),sK58(sK62,k4_conlat_2(sK62),sK63)),sK58(sK62,k4_conlat_2(sK62),sK63)),sK62)
| ~ spl1780_95 ),
inference(forward_subsumption_resolution,[],[f79683,f79643]) ).
fof(f79692,plain,
( ~ v7_conlat_1(g3_conlat_1(sK62,sK57(sK62,k4_conlat_2(sK62),sK63),sK58(sK62,k4_conlat_2(sK62),sK63)),sK62)
| ~ spl1780_95 ),
inference(forward_demodulation,[],[f79684,f79493]) ).
fof(f79693,plain,
( ~ v7_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62)
| ~ spl1780_95 ),
inference(forward_demodulation,[],[f79692,f79515]) ).
fof(f79708,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u2_conlat_1(sK62)))
| v3_conlat_1(sK62)
| ~ v7_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),X0))),sK62) ),
inference(resolution,[],[f62699,f62057]) ).
fof(f79710,plain,
! [X0] :
( ~ v7_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),X0))),sK62)
| ~ m1_subset_1(X0,k1_zfmisc_1(u2_conlat_1(sK62))) ),
inference(forward_subsumption_resolution,[],[f79708,f62058]) ).
fof(f79712,plain,
( ~ v7_conlat_1(g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),sK64),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),sK60(sK62,k5_conlat_2(sK62),sK64))),sK62)
| ~ m1_subset_1(k6_domain_1(u2_conlat_1(sK62),sK64),k1_zfmisc_1(u2_conlat_1(sK62))) ),
inference(superposition,[],[f79710,f79511]) ).
fof(f79713,plain,
( ~ v7_conlat_1(g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),sK64),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),sK60(sK62,k5_conlat_2(sK62),sK64))),sK62)
| ~ spl1780_93 ),
inference(forward_subsumption_resolution,[],[f79712,f79636]) ).
fof(f79721,plain,
( ~ v7_conlat_1(g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),sK64),sK61(sK62,k5_conlat_2(sK62),sK64)),sK62)
| ~ spl1780_93 ),
inference(forward_demodulation,[],[f79713,f79513]) ).
fof(f79722,plain,
( ~ v7_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62)
| ~ spl1780_93 ),
inference(forward_demodulation,[],[f79721,f79514]) ).
fof(f79751,plain,
( v1_xboole_0(u1_conlat_1(sK62))
| k6_domain_1(u1_conlat_1(sK62),sK63) = k2_tarski(sK63,sK63) ),
inference(resolution,[],[f75221,f62059]) ).
fof(f79758,definition,
( spl1780_104
<=> k6_domain_1(u1_conlat_1(sK62),sK63) = k2_tarski(sK63,sK63) ),
introduced(definition,[new_symbols(definition,[spl1780_104])],[avatar_definition]) ).
fof(f79759,plain,
( k6_domain_1(u1_conlat_1(sK62),sK63) = k2_tarski(sK63,sK63)
| ~ spl1780_104 ),
inference(avatar_component_clause,[],[f79758]) ).
fof(f79760,plain,
( spl1780_104
| spl1780_96 ),
inference(avatar_split_clause,[],[f79751,f79645,f79758]) ).
fof(f79783,plain,
( v3_conlat_1(sK62)
| ~ l1_conlat_1(sK62)
| ~ spl1780_94 ),
inference(resolution,[],[f79639,f65871]) ).
fof(f79784,plain,
( ~ l1_conlat_1(sK62)
| ~ spl1780_94 ),
inference(forward_subsumption_resolution,[],[f79783,f62058]) ).
fof(f79785,plain,
( v3_conlat_1(sK62)
| ~ l1_conlat_1(sK62)
| ~ spl1780_96 ),
inference(resolution,[],[f79646,f65870]) ).
fof(f79787,plain,
( ~ l2_conlat_1(sK62)
| ~ spl1780_94 ),
inference(resolution,[],[f79784,f65856]) ).
fof(f79789,plain,
( $false
| ~ spl1780_94 ),
inference(forward_subsumption_resolution,[],[f79787,f62057]) ).
fof(f79790,plain,
~ spl1780_94,
inference(avatar_contradiction_clause,[],[f79789]) ).
fof(f79791,plain,
( ~ l1_conlat_1(sK62)
| ~ spl1780_96 ),
inference(forward_subsumption_resolution,[],[f79785,f62058]) ).
fof(f79795,plain,
( ~ l2_conlat_1(sK62)
| ~ spl1780_96 ),
inference(resolution,[],[f79791,f65856]) ).
fof(f79797,plain,
( $false
| ~ spl1780_96 ),
inference(forward_subsumption_resolution,[],[f79795,f62057]) ).
fof(f79798,plain,
~ spl1780_96,
inference(avatar_contradiction_clause,[],[f79797]) ).
fof(f79799,plain,
( m1_subset_1(k2_tarski(sK63,sK63),k1_zfmisc_1(u1_conlat_1(sK62)))
| ~ spl1780_95
| ~ spl1780_104 ),
inference(superposition,[],[f79643,f79759]) ).
fof(f79800,plain,
( sK58(sK62,k4_conlat_2(sK62),sK63) = k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k2_tarski(sK63,sK63))
| ~ spl1780_104 ),
inference(superposition,[],[f79491,f79759]) ).
fof(f79908,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_conlat_1(sK62)))
| v3_conlat_1(sK62)
| l3_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),X0)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),X0)),sK62) ),
inference(resolution,[],[f62706,f62057]) ).
fof(f79910,plain,
! [X0] :
( l3_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),X0)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),X0)),sK62)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_conlat_1(sK62))) ),
inference(forward_subsumption_resolution,[],[f79908,f62058]) ).
fof(f79915,plain,
( l3_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),sK58(sK62,k4_conlat_2(sK62),sK63)),sK58(sK62,k4_conlat_2(sK62),sK63)),sK62)
| ~ m1_subset_1(k2_tarski(sK63,sK63),k1_zfmisc_1(u1_conlat_1(sK62)))
| ~ spl1780_104 ),
inference(superposition,[],[f79910,f79800]) ).
fof(f79916,plain,
( l3_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),sK58(sK62,k4_conlat_2(sK62),sK63)),sK58(sK62,k4_conlat_2(sK62),sK63)),sK62)
| ~ spl1780_95
| ~ spl1780_104 ),
inference(forward_subsumption_resolution,[],[f79915,f79799]) ).
fof(f79924,plain,
( l3_conlat_1(g3_conlat_1(sK62,sK57(sK62,k4_conlat_2(sK62),sK63),sK58(sK62,k4_conlat_2(sK62),sK63)),sK62)
| ~ spl1780_95
| ~ spl1780_104 ),
inference(forward_demodulation,[],[f79916,f79493]) ).
fof(f79926,plain,
( l3_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62)
| ~ spl1780_95
| ~ spl1780_104 ),
inference(forward_demodulation,[],[f79924,f79515]) ).
fof(f79960,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_conlat_1(sK62)))
| v3_conlat_1(sK62)
| v9_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),X0)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),X0)),sK62) ),
inference(resolution,[],[f62707,f62057]) ).
fof(f79962,plain,
! [X0] :
( v9_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),X0)),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),X0)),sK62)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_conlat_1(sK62))) ),
inference(forward_subsumption_resolution,[],[f79960,f62058]) ).
fof(f79965,plain,
( v9_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),sK58(sK62,k4_conlat_2(sK62),sK63)),sK58(sK62,k4_conlat_2(sK62),sK63)),sK62)
| ~ m1_subset_1(k2_tarski(sK63,sK63),k1_zfmisc_1(u1_conlat_1(sK62)))
| ~ spl1780_104 ),
inference(superposition,[],[f79962,f79800]) ).
fof(f79966,plain,
( v9_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),sK58(sK62,k4_conlat_2(sK62),sK63)),sK58(sK62,k4_conlat_2(sK62),sK63)),sK62)
| ~ spl1780_95
| ~ spl1780_104 ),
inference(forward_subsumption_resolution,[],[f79965,f79799]) ).
fof(f79972,plain,
( v9_conlat_1(g3_conlat_1(sK62,sK57(sK62,k4_conlat_2(sK62),sK63),sK58(sK62,k4_conlat_2(sK62),sK63)),sK62)
| ~ spl1780_95
| ~ spl1780_104 ),
inference(forward_demodulation,[],[f79966,f79493]) ).
fof(f79974,plain,
( v9_conlat_1(k8_funct_2(u1_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k4_conlat_2(sK62),sK63),sK62)
| ~ spl1780_95
| ~ spl1780_104 ),
inference(forward_demodulation,[],[f79972,f79515]) ).
fof(f79976,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u2_conlat_1(sK62)))
| v3_conlat_1(sK62)
| l3_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),X0))),sK62) ),
inference(resolution,[],[f62697,f62057]) ).
fof(f79978,plain,
! [X0] :
( l3_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),X0))),sK62)
| ~ m1_subset_1(X0,k1_zfmisc_1(u2_conlat_1(sK62))) ),
inference(forward_subsumption_resolution,[],[f79976,f62058]) ).
fof(f79982,plain,
( l3_conlat_1(g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),sK64),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),sK60(sK62,k5_conlat_2(sK62),sK64))),sK62)
| ~ m1_subset_1(k6_domain_1(u2_conlat_1(sK62),sK64),k1_zfmisc_1(u2_conlat_1(sK62))) ),
inference(superposition,[],[f79978,f79511]) ).
fof(f79985,plain,
( l3_conlat_1(g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),sK64),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),sK60(sK62,k5_conlat_2(sK62),sK64))),sK62)
| ~ spl1780_93 ),
inference(forward_subsumption_resolution,[],[f79982,f79636]) ).
fof(f79993,plain,
( l3_conlat_1(g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),sK64),sK61(sK62,k5_conlat_2(sK62),sK64)),sK62)
| ~ spl1780_93 ),
inference(forward_demodulation,[],[f79985,f79513]) ).
fof(f79995,plain,
( l3_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62)
| ~ spl1780_93 ),
inference(forward_demodulation,[],[f79993,f79514]) ).
fof(f79998,plain,
( $false
| spl1780_63
| ~ spl1780_93 ),
inference(forward_subsumption_resolution,[],[f79995,f79174]) ).
fof(f79999,plain,
( spl1780_63
| ~ spl1780_93 ),
inference(avatar_contradiction_clause,[],[f79998]) ).
fof(f80098,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u2_conlat_1(sK62)))
| v3_conlat_1(sK62)
| v9_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),X0))),sK62) ),
inference(resolution,[],[f62698,f62057]) ).
fof(f80104,plain,
! [X0] :
( v9_conlat_1(g3_conlat_1(sK62,k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),X0),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),k8_funct_2(k1_zfmisc_1(u2_conlat_1(sK62)),k1_zfmisc_1(u1_conlat_1(sK62)),k2_conlat_1(sK62),X0))),sK62)
| ~ m1_subset_1(X0,k1_zfmisc_1(u2_conlat_1(sK62))) ),
inference(forward_subsumption_resolution,[],[f80098,f62058]) ).
fof(f80106,plain,
( v9_conlat_1(g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),sK64),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),sK60(sK62,k5_conlat_2(sK62),sK64))),sK62)
| ~ m1_subset_1(k6_domain_1(u2_conlat_1(sK62),sK64),k1_zfmisc_1(u2_conlat_1(sK62))) ),
inference(superposition,[],[f80104,f79511]) ).
fof(f80109,plain,
( v9_conlat_1(g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),sK64),k8_funct_2(k1_zfmisc_1(u1_conlat_1(sK62)),k1_zfmisc_1(u2_conlat_1(sK62)),k1_conlat_1(sK62),sK60(sK62,k5_conlat_2(sK62),sK64))),sK62)
| ~ spl1780_93 ),
inference(forward_subsumption_resolution,[],[f80106,f79636]) ).
fof(f80115,plain,
( v9_conlat_1(g3_conlat_1(sK62,sK60(sK62,k5_conlat_2(sK62),sK64),sK61(sK62,k5_conlat_2(sK62),sK64)),sK62)
| ~ spl1780_93 ),
inference(forward_demodulation,[],[f80109,f79513]) ).
fof(f80117,plain,
( v9_conlat_1(k8_funct_2(u2_conlat_1(sK62),u1_struct_0(k11_conlat_1(sK62)),k5_conlat_2(sK62),sK64),sK62)
| ~ spl1780_93 ),
inference(forward_demodulation,[],[f80115,f79514]) ).
fof(f80120,plain,
( $false
| spl1780_64
| ~ spl1780_93 ),
inference(forward_subsumption_resolution,[],[f80117,f79177]) ).
fof(f80121,plain,
( spl1780_64
| ~ spl1780_93 ),
inference(avatar_contradiction_clause,[],[f80120]) ).
fof(f80122,plain,
( $false
| spl1780_66
| ~ spl1780_95
| ~ spl1780_104 ),
inference(forward_subsumption_resolution,[],[f79183,f79926]) ).
fof(f80123,plain,
( spl1780_66
| ~ spl1780_95
| ~ spl1780_104 ),
inference(avatar_contradiction_clause,[],[f80122]) ).
fof(f80124,plain,
( $false
| spl1780_67
| ~ spl1780_95
| ~ spl1780_104 ),
inference(forward_subsumption_resolution,[],[f79186,f79974]) ).
fof(f80125,plain,
( spl1780_67
| ~ spl1780_95
| ~ spl1780_104 ),
inference(avatar_contradiction_clause,[],[f80124]) ).
fof(f80126,plain,
( $false
| ~ spl1780_65
| ~ spl1780_93 ),
inference(forward_subsumption_resolution,[],[f79180,f79722]) ).
fof(f80127,plain,
( ~ spl1780_65
| ~ spl1780_93 ),
inference(avatar_contradiction_clause,[],[f80126]) ).
fof(f80128,plain,
( $false
| ~ spl1780_68
| ~ spl1780_95 ),
inference(forward_subsumption_resolution,[],[f79189,f79693]) ).
fof(f80129,plain,
( ~ spl1780_68
| ~ spl1780_95 ),
inference(avatar_contradiction_clause,[],[f80128]) ).
cnf(s50,plain,
( ~ spl1780_63
| ~ spl1780_64
| spl1780_65
| ~ spl1780_66
| ~ spl1780_67
| spl1780_68 ),
inference(sat_conversion,[],[f79190]) ).
cnf(s72,plain,
( spl1780_93
| spl1780_94 ),
inference(sat_conversion,[],[f79640]) ).
cnf(s73,plain,
( spl1780_95
| spl1780_96 ),
inference(sat_conversion,[],[f79647]) ).
cnf(s80,plain,
( spl1780_96
| spl1780_104 ),
inference(sat_conversion,[],[f79760]) ).
cnf(s82,plain,
~ spl1780_94,
inference(sat_conversion,[],[f79790]) ).
cnf(s84,plain,
~ spl1780_96,
inference(sat_conversion,[],[f79798]) ).
cnf(s96,plain,
( spl1780_63
| ~ spl1780_93 ),
inference(sat_conversion,[],[f79999]) ).
cnf(s116,plain,
( spl1780_64
| ~ spl1780_93 ),
inference(sat_conversion,[],[f80121]) ).
cnf(s117,plain,
( spl1780_66
| ~ spl1780_95
| ~ spl1780_104 ),
inference(sat_conversion,[],[f80123]) ).
cnf(s118,plain,
( spl1780_67
| ~ spl1780_95
| ~ spl1780_104 ),
inference(sat_conversion,[],[f80125]) ).
cnf(s119,plain,
( ~ spl1780_65
| ~ spl1780_93 ),
inference(sat_conversion,[],[f80127]) ).
cnf(s120,plain,
( ~ spl1780_68
| ~ spl1780_95 ),
inference(sat_conversion,[],[f80129]) ).
cnf(s134,plain,
spl1780_104,
inference(rat,[],[s80,s84]) ).
cnf(s142,plain,
spl1780_95,
inference(rat,[],[s73,s84]) ).
cnf(s143,plain,
~ spl1780_68,
inference(rat,[],[s120,s142]) ).
cnf(s144,plain,
spl1780_67,
inference(rat,[],[s118,s134,s142]) ).
cnf(s145,plain,
spl1780_66,
inference(rat,[],[s117,s134,s142]) ).
cnf(s146,plain,
spl1780_93,
inference(rat,[],[s72,s82]) ).
cnf(s147,plain,
~ spl1780_65,
inference(rat,[],[s119,s146]) ).
cnf(s148,plain,
spl1780_64,
inference(rat,[],[s116,s146]) ).
cnf(s149,plain,
spl1780_63,
inference(rat,[],[s96,s146]) ).
cnf(s161,plain,
$false,
inference(rat,[],[s50,s143,s144,s145,s147,s148,s149]) ).
fof(f80130,plain,
$false,
inference(avatar_sat_refutation,[],[s161]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT343+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n018.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 14:52:20 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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
% 27.31/8.57 % (2442662)Detected formulas, will run a generic FOF schedule.
% 27.31/8.57 % (2443204)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=2128249362:i=141193_2956 on theBenchmark for (2956ds/141193Mi)
% 27.31/8.57 % (2443205)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=682161913:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2956 on theBenchmark for (2956ds/134677Mi)
% 27.31/8.57 % (2443206)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=4066534906:i=141695:sd=1:nm=32:gsp=on:ss=included_2956 on theBenchmark for (2956ds/141695Mi)
% 27.31/8.57 % (2443207)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1892802178:i=109:sd=1:ins=1:gsp=on:ss=axioms_2956 on theBenchmark for (2956ds/109Mi)
% 27.31/8.57 % (2443208)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2155680835:i=119:av=off:ss=axioms_2956 on theBenchmark for (2956ds/119Mi)
% 27.31/8.57 % (2443209)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1499948411:s2a=on:i=139:gtg=position_2956 on theBenchmark for (2956ds/139Mi)
% 27.31/8.57 % (2443210)dis-21_1_sil=8000:lcm=predicate:random_seed=233727165:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2956 on theBenchmark for (2956ds/129Mi)
% 27.31/8.57 % (2443207)Instruction limit reached!
% 27.31/8.57 % (2443207)------------------------------
% 27.31/8.57 % (2443207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.31/8.57 % (2443207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.31/8.57 % (2443207)CaDiCaL version: 2.1.3
% 27.31/8.57 % (2443207)Termination reason: Instruction limit
% 27.31/8.57 % (2443207)Termination phase: SInE selection
% 27.31/8.57 % (2443207)Time elapsed: 0.123 s
% 27.31/8.57 % (2443207)Peak memory usage: 163 MB
% 27.31/8.57 % (2443207)Instructions burned: 110 (million)
% 27.31/8.57 % (2443208)Instruction limit reached!
% 27.31/8.57 % (2443208)------------------------------
% 27.31/8.57 % (2443208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.31/8.57 % (2443208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.31/8.57 % (2443208)CaDiCaL version: 2.1.3
% 27.31/8.57 % (2443208)Termination reason: Instruction limit
% 27.31/8.57 % (2443208)Termination phase: SInE selection
% 27.31/8.57 % (2443208)Time elapsed: 0.134 s
% 27.31/8.57 % (2443208)Peak memory usage: 163 MB
% 27.31/8.57 % (2443208)Instructions burned: 119 (million)
% 27.31/8.57 % (2443209)Instruction limit reached!
% 27.31/8.57 % (2443209)------------------------------
% 27.31/8.57 % (2443209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.31/8.57 % (2443209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.31/8.57 % (2443209)CaDiCaL version: 2.1.3
% 27.31/8.57 % (2443209)Termination reason: Instruction limit
% 27.31/8.57 % (2443209)Termination phase: Property scanning
% 27.31/8.57 % (2443209)Time elapsed: 0.127 s
% 27.31/8.57 % (2443209)Peak memory usage: 164 MB
% 27.31/8.57 % (2443209)Instructions burned: 139 (million)
% 27.31/8.57 % (2443210)Instruction limit reached!
% 27.31/8.57 % (2443210)------------------------------
% 27.31/8.57 % (2443210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.31/8.57 % (2443210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.31/8.57 % (2443210)CaDiCaL version: 2.1.3
% 27.31/8.57 % (2443210)Termination reason: Instruction limit
% 27.31/8.57 % (2443210)Termination phase: SInE selection
% 27.31/8.57 % (2443210)Time elapsed: 0.145 s
% 27.31/8.57 % (2443210)Peak memory usage: 163 MB
% 27.31/8.57 % (2443210)Instructions burned: 129 (million)
% 27.31/8.57 % (2443221)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=4171165863:s2a=on:i=248:s2at=1.23:gtg=position_2951 on theBenchmark for (2951ds/248Mi)
% 27.31/8.57 % (2443219)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2162877530:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2951 on theBenchmark for (2951ds/157Mi)
% 27.31/8.57 % (2443220)lrs+1011_1_sil=32000:sp=occurrence:random_seed=382727982:i=325:sd=1:ss=axioms:sgt=32_2951 on theBenchmark for (2951ds/325Mi)
% 27.31/8.57 % (2443218)lrs+10_1_sil=8000:sp=occurrence:random_seed=1604795759:i=285:sd=3:ss=axioms:sgt=8_2952 on theBenchmark for (2952ds/285Mi)
% 27.31/8.57 % (2443219)Instruction limit reached!
% 35.42/9.69 % (2443219)------------------------------
% 35.42/9.69 % (2443219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/9.69 % (2443219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/9.69 % (2443219)CaDiCaL version: 2.1.3
% 35.42/9.69 % (2443219)Termination reason: Instruction limit
% 35.42/9.69 % (2443219)Termination phase: Property scanning
% 35.42/9.69 % (2443219)Time elapsed: 0.138 s
% 35.42/9.69 % (2443219)Peak memory usage: 163 MB
% 35.42/9.69 % (2443219)Instructions burned: 157 (million)
% 35.42/9.69 % (2443221)Instruction limit reached!
% 35.42/9.69 % (2443221)------------------------------
% 35.42/9.69 % (2443221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/9.69 % (2443221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/9.69 % (2443221)CaDiCaL version: 2.1.3
% 35.42/9.69 % (2443221)Termination reason: Instruction limit
% 35.42/9.69 % (2443221)Termination phase: Property scanning
% 35.42/9.69 % (2443221)Time elapsed: 0.197 s
% 35.42/9.69 % (2443221)Peak memory usage: 164 MB
% 35.42/9.69 % (2443221)Instructions burned: 248 (million)
% 35.42/9.69 % (2443218)Instruction limit reached!
% 35.42/9.69 % (2443218)------------------------------
% 35.42/9.69 % (2443218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/9.69 % (2443218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/9.69 % (2443218)CaDiCaL version: 2.1.3
% 35.42/9.69 % (2443218)Termination reason: Instruction limit
% 35.42/9.69 % (2443218)Termination phase: SInE selection
% 35.42/9.69 % (2443218)Time elapsed: 0.292 s
% 35.42/9.69 % (2443218)Peak memory usage: 164 MB
% 35.42/9.69 % (2443218)Instructions burned: 285 (million)
% 35.42/9.69 % (2443220)Instruction limit reached!
% 35.42/9.69 % (2443220)------------------------------
% 35.42/9.69 % (2443220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/9.69 % (2443220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/9.69 % (2443220)CaDiCaL version: 2.1.3
% 35.42/9.69 % (2443220)Termination reason: Instruction limit
% 35.42/9.69 % (2443220)Termination phase: SInE selection
% 35.42/9.69 % (2443220)Time elapsed: 0.334 s
% 35.42/9.69 % (2443220)Peak memory usage: 164 MB
% 35.42/9.69 % (2443220)Instructions burned: 325 (million)
% 35.42/9.69 % (2443226)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1921763440:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2948 on theBenchmark for (2948ds/294Mi)
% 35.42/9.69 % (2443227)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3479449922:i=2350_2947 on theBenchmark for (2947ds/2350Mi)
% 35.42/9.69 % (2443228)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1477835152:cts=off:i=113:fsr=off:ss=included:sgt=4_2946 on theBenchmark for (2946ds/113Mi)
% 35.42/9.69 % (2443226)Instruction limit reached!
% 35.42/9.69 % (2443226)------------------------------
% 35.42/9.69 % (2443226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/9.69 % (2443226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/9.69 % (2443226)CaDiCaL version: 2.1.3
% 35.42/9.69 % (2443226)Termination reason: Instruction limit
% 35.42/9.69 % (2443226)Termination phase: SInE selection
% 35.42/9.69 % (2443226)Time elapsed: 0.261 s
% 35.42/9.69 % (2443226)Peak memory usage: 164 MB
% 35.42/9.69 % (2443226)Instructions burned: 294 (million)
% 35.42/9.69 % (2443229)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1963970559:i=127:av=off:fsr=off:sup=off_2946 on theBenchmark for (2946ds/127Mi)
% 35.42/9.69 % (2443228)Instruction limit reached!
% 35.42/9.69 % (2443228)------------------------------
% 35.42/9.69 % (2443228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/9.69 % (2443228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/9.69 % (2443228)CaDiCaL version: 2.1.3
% 35.42/9.69 % (2443228)Termination reason: Instruction limit
% 35.42/9.69 % (2443228)Termination phase: SInE selection
% 35.42/9.69 % (2443228)Time elapsed: 0.128 s
% 35.42/9.69 % (2443228)Peak memory usage: 163 MB
% 35.42/9.69 % (2443228)Instructions burned: 113 (million)
% 35.42/9.69 % (2443229)Instruction limit reached!
% 35.42/9.69 % (2443229)------------------------------
% 35.42/9.69 % (2443229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/9.69 % (2443229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/9.69 % (2443229)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443229)Termination reason: Instruction limit
% 32.29/12.04 % (2443229)Termination phase: Preprocessing 1
% 32.29/12.04 % (2443229)Time elapsed: 0.161 s
% 32.29/12.04 % (2443229)Peak memory usage: 165 MB
% 32.29/12.04 % (2443229)Instructions burned: 128 (million)
% 32.29/12.04 % (2443234)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4090614763:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2943 on theBenchmark for (2943ds/114Mi)
% 32.29/12.04 % (2443234)Instruction limit reached!
% 32.29/12.04 % (2443234)------------------------------
% 32.29/12.04 % (2443234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443234)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443234)Termination reason: Instruction limit
% 32.29/12.04 % (2443234)Termination phase: Property scanning
% 32.29/12.04 % (2443234)Time elapsed: 0.105 s
% 32.29/12.04 % (2443234)Peak memory usage: 164 MB
% 32.29/12.04 % (2443234)Instructions burned: 115 (million)
% 32.29/12.04 % (2443235)lrs+10_1_sil=8000:sp=occurrence:random_seed=3911652950:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2942 on theBenchmark for (2942ds/907Mi)
% 32.29/12.04 % (2443236)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3967649296:i=437:sd=1:aac=none:ss=included_2941 on theBenchmark for (2941ds/437Mi)
% 32.29/12.04 % (2443238)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1451472530:i=5202:ss=axioms:sgt=16_2939 on theBenchmark for (2939ds/5202Mi)
% 32.29/12.04 % (2443236)Refutation not found, incomplete strategy
% 32.29/12.04 % (2443236)------------------------------
% 32.29/12.04 % (2443236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443236)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443236)Termination reason: Refutation not found, incomplete strategy
% 32.29/12.04 % (2443236)Time elapsed: 0.479 s
% 32.29/12.04 % (2443236)Peak memory usage: 170 MB
% 32.29/12.04 % (2443236)Instructions burned: 417 (million)
% 32.29/12.04 % (2443235)Instruction limit reached!
% 32.29/12.04 % (2443235)------------------------------
% 32.29/12.04 % (2443235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443235)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443235)Termination reason: Instruction limit
% 32.29/12.04 % (2443235)Termination phase: Property scanning
% 32.29/12.04 % (2443235)Time elapsed: 0.768 s
% 32.29/12.04 % (2443235)Peak memory usage: 178 MB
% 32.29/12.04 % (2443235)Instructions burned: 908 (million)
% 32.29/12.04 % (2443236)------------------------------
% 32.29/12.04 % (2443236)------------------------------
% 32.29/12.04 % (2443242)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3924898986:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2931 on theBenchmark for (2931ds/134Mi)
% 32.29/12.04 % (2443243)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1907781830:st=8:i=592:sd=3:ep=RST:ss=axioms_2930 on theBenchmark for (2930ds/592Mi)
% 32.29/12.04 % (2443242)Instruction limit reached!
% 32.29/12.04 % (2443242)------------------------------
% 32.29/12.04 % (2443242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443242)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443242)Termination reason: Instruction limit
% 32.29/12.04 % (2443242)Termination phase: SInE selection
% 32.29/12.04 % (2443242)Time elapsed: 0.107 s
% 32.29/12.04 % (2443242)Peak memory usage: 163 MB
% 32.29/12.04 % (2443242)Instructions burned: 135 (million)
% 32.29/12.04 % (2443246)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3769047557:st=3:i=13193:sd=3:ss=axioms_2928 on theBenchmark for (2928ds/13193Mi)
% 32.29/12.04 % (2443243)Instruction limit reached!
% 32.29/12.04 % (2443243)------------------------------
% 32.29/12.04 % (2443243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443243)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443243)Termination reason: Instruction limit
% 32.29/12.04 % (2443243)Termination phase: Preprocessing 1
% 32.29/12.04 % (2443243)Time elapsed: 0.440 s
% 32.29/12.04 % (2443243)Peak memory usage: 167 MB
% 32.29/12.04 % (2443243)Instructions burned: 593 (million)
% 32.29/12.04 % (2443227)Instruction limit reached!
% 32.29/12.04 % (2443227)------------------------------
% 32.29/12.04 % (2443227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443227)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443227)Termination reason: Instruction limit
% 32.29/12.04 % (2443227)Termination phase: Preprocessing 3
% 32.29/12.04 % (2443227)Time elapsed: 2.191 s
% 32.29/12.04 % (2443227)Peak memory usage: 264 MB
% 32.29/12.04 % (2443227)Instructions burned: 2350 (million)
% 32.29/12.04 % (2443248)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=1496275919:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2924 on theBenchmark for (2924ds/125Mi)
% 32.29/12.04 % (2443248)Instruction limit reached!
% 32.29/12.04 % (2443248)------------------------------
% 32.29/12.04 % (2443248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443248)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443248)Termination reason: Instruction limit
% 32.29/12.04 % (2443248)Termination phase: Property scanning
% 32.29/12.04 % (2443248)Time elapsed: 0.061 s
% 32.29/12.04 % (2443248)Peak memory usage: 164 MB
% 32.29/12.04 % (2443248)Instructions burned: 127 (million)
% 32.29/12.04 % (2443249)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=750580858:i=134:gtgl=5:slsql=off:gtg=exists_sym_2922 on theBenchmark for (2922ds/134Mi)
% 32.29/12.04 % (2443249)Instruction limit reached!
% 32.29/12.04 % (2443249)------------------------------
% 32.29/12.04 % (2443249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443249)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443249)Termination reason: Instruction limit
% 32.29/12.04 % (2443249)Termination phase: Property scanning
% 32.29/12.04 % (2443249)Time elapsed: 0.065 s
% 32.29/12.04 % (2443249)Peak memory usage: 164 MB
% 32.29/12.04 % (2443249)Instructions burned: 135 (million)
% 32.29/12.04 % (2443251)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2004989247:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2921 on theBenchmark for (2921ds/141Mi)
% 32.29/12.04 % (2443251)Instruction limit reached!
% 32.29/12.04 % (2443251)------------------------------
% 32.29/12.04 % (2443251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443251)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443251)Termination reason: Instruction limit
% 32.29/12.04 % (2443251)Termination phase: SInE selection
% 32.29/12.04 % (2443251)Time elapsed: 0.111 s
% 32.29/12.04 % (2443251)Peak memory usage: 163 MB
% 32.29/12.04 % (2443251)Instructions burned: 142 (million)
% 32.29/12.04 % (2443254)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2996061315:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2920 on theBenchmark for (2920ds/431Mi)
% 32.29/12.04 % (2443255)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=21783326:i=6060:aac=none:ins=25_2918 on theBenchmark for (2918ds/6060Mi)
% 32.29/12.04 % (2443254)Instruction limit reached!
% 32.29/12.04 % (2443254)------------------------------
% 32.29/12.04 % (2443254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443254)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443254)Termination reason: Instruction limit
% 32.29/12.04 % (2443254)Termination phase: Saturation
% 32.29/12.04 % (2443254)Time elapsed: 0.362 s
% 32.29/12.04 % (2443254)Peak memory usage: 170 MB
% 32.29/12.04 % (2443254)Instructions burned: 431 (million)
% 32.29/12.04 % (2443258)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=1386769578:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2914 on theBenchmark for (2914ds/150Mi)
% 32.29/12.04 % (2443258)Instruction limit reached!
% 32.29/12.04 % (2443258)------------------------------
% 32.29/12.04 % (2443258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443258)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443258)Termination reason: Instruction limit
% 32.29/12.04 % (2443258)Termination phase: SInE selection
% 32.29/12.04 % (2443258)Time elapsed: 0.122 s
% 32.29/12.04 % (2443258)Peak memory usage: 163 MB
% 32.29/12.04 % (2443258)Instructions burned: 150 (million)
% 32.29/12.04 % (2443260)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2545209542:i=14155:bd=all_2911 on theBenchmark for (2911ds/14155Mi)
% 32.29/12.04 % (2443238)Instruction limit reached!
% 32.29/12.04 % (2443238)------------------------------
% 32.29/12.04 % (2443238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443238)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443238)Termination reason: Instruction limit
% 32.29/12.04 % (2443238)Termination phase: Saturation
% 32.29/12.04 % (2443238)Time elapsed: 3.375 s
% 32.29/12.04 % (2443238)Peak memory usage: 286 MB
% 32.29/12.04 % (2443238)Instructions burned: 5204 (million)
% 32.29/12.04 % (2443262)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1691225021:i=667:av=off:fsr=off_2902 on theBenchmark for (2902ds/667Mi)
% 32.29/12.04 % (2443262)Instruction limit reached!
% 32.29/12.04 % (2443262)------------------------------
% 32.29/12.04 % (2443262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443262)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443262)Termination reason: Instruction limit
% 32.29/12.04 % (2443262)Termination phase: Preprocessing 2
% 32.29/12.04 % (2443262)Time elapsed: 0.593 s
% 32.29/12.04 % (2443262)Peak memory usage: 219 MB
% 32.29/12.04 % (2443262)Instructions burned: 667 (million)
% 32.29/12.04 % (2443264)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=3300562386:s2a=on:i=185:s2at=1.8:fdi=4_2894 on theBenchmark for (2894ds/185Mi)
% 32.29/12.04 % (2443205)First to succeed.
% 32.29/12.04 % (2443205)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2442662"
% 32.29/12.04 % (2443264)Instruction limit reached!
% 32.29/12.04 % (2443264)------------------------------
% 32.29/12.04 % (2443264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.29/12.04 % (2443264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.29/12.04 % (2443264)CaDiCaL version: 2.1.3
% 32.29/12.04 % (2443264)Termination reason: Instruction limit
% 32.29/12.04 % (2443264)Termination phase: SInE selection
% 32.29/12.04 % (2443264)Time elapsed: 0.140 s
% 32.29/12.04 % (2443264)Peak memory usage: 163 MB
% 32.29/12.04 % (2443264)Instructions burned: 186 (million)
% 32.29/12.04 % (2443266)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1756362876:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2891 on theBenchmark for (2891ds/193Mi)
% 32.29/12.04 % (2443205)Refutation found. Thanks to Tanya!
% 32.29/12.04 % SZS status Theorem for theBenchmark
% 32.29/12.04 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/12.30 % (2443205)------------------------------
% 0.16/12.30 % (2443205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/12.30 % (2443205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/12.30 % (2443205)CaDiCaL version: 2.1.3
% 0.16/12.30 % (2443205)Termination reason: Refutation
% 0.16/12.30 % (2443205)Time elapsed: 6.151 s
% 0.16/12.30 % (2443205)Peak memory usage: 379 MB
% 0.16/12.30 % (2443205)Instructions burned: 8655 (million)
% 0.16/12.30 % (2443205)------------------------------
% 0.16/12.30 % (2443205)------------------------------
% 0.16/12.30 % (2442662)Success in time 11.189 s
% 0.16/12.30 % Vampire exiting
%------------------------------------------------------------------------------