%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT287+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:48:13 AM UTC 2026
% Result : Theorem 52.67s 12.06s
% Output : Refutation 52.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 29
% Syntax : Number of formulae : 194 ( 34 unt; 13 def)
% Number of atoms : 633 ( 47 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 736 ( 297 ~; 338 |; 67 &)
% ( 17 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 36 ( 34 usr; 14 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 2 con; 0-3 aty)
% Number of variables : 139 ( 0 sgn 137 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> m1_subset_1(k1_pre_topc(X0),u1_struct_0(k6_lopclset(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_lopclset) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> m1_subset_1(k1_pre_topc(X0),u1_struct_0(k6_lopclset(X0))) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f9,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(X0)
=> X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v3_lattices) ).
fof(f14,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f55,axiom,
! [X0,X1,X2] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [X3,X4,X5] :
( g3_lattices(X0,X1,X2) = g3_lattices(X3,X4,X5)
=> ( X0 = X3
& X1 = X4
& X2 = X5 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',free_g3_lattices) ).
fof(f59,axiom,
! [X0,X1,X2] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ( v3_lattices(g3_lattices(X0,X1,X2))
& l3_lattices(g3_lattices(X0,X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_g3_lattices) ).
fof(f60,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ( v1_funct_1(k4_lopclset(X0))
& v1_funct_2(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
& m2_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_lopclset) ).
fof(f61,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ( v1_funct_1(k5_lopclset(X0))
& v1_funct_2(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
& m2_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lopclset) ).
fof(f69,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( v1_xboole_0(k1_pre_topc(X0))
& v1_membered(k1_pre_topc(X0))
& v2_membered(k1_pre_topc(X0))
& v3_membered(k1_pre_topc(X0))
& v4_membered(k1_pre_topc(X0))
& v5_membered(k1_pre_topc(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_pre_topc) ).
fof(f74,axiom,
! [X0] :
( v1_xboole_0(X0)
=> X0 = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(f82,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) )
=> ! [X2] :
( m2_subset_1(X2,X0,X1)
<=> m1_subset_1(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_subset_1) ).
fof(f83,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lopclset) ).
fof(f87,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f91,axiom,
! [X0] :
( ~ v1_xboole_0(k1_zfmisc_1(X0))
& v1_finsub_1(k1_zfmisc_1(X0))
& v3_finsub_1(k1_zfmisc_1(X0))
& v4_finsub_1(k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_finsub_1) ).
fof(f92,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ~ v1_xboole_0(k1_lopclset(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lopclset) ).
fof(f95,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> k6_lopclset(X0) = g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_lopclset) ).
fof(f96,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> m2_subset_1(k1_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_lopclset) ).
fof(f117,plain,
? [X0] :
( ~ m1_subset_1(k1_pre_topc(X0),u1_struct_0(k6_lopclset(X0)))
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f118,plain,
? [X0] :
( ~ m1_subset_1(k1_pre_topc(X0),u1_struct_0(k6_lopclset(X0)))
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f117]) ).
fof(f124,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f125,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f124]) ).
fof(f159,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(ennf_transformation,[],[f55]) ).
fof(f160,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f159]) ).
fof(f161,plain,
! [X0,X1,X2] :
( ( v3_lattices(g3_lattices(X0,X1,X2))
& l3_lattices(g3_lattices(X0,X1,X2)) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(ennf_transformation,[],[f59]) ).
fof(f162,plain,
! [X0,X1,X2] :
( ( v3_lattices(g3_lattices(X0,X1,X2))
& l3_lattices(g3_lattices(X0,X1,X2)) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f161]) ).
fof(f163,plain,
! [X0] :
( ( v1_funct_1(k4_lopclset(X0))
& v1_funct_2(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
& m2_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f60]) ).
fof(f164,plain,
! [X0] :
( ( v1_funct_1(k4_lopclset(X0))
& v1_funct_2(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
& m2_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f163]) ).
fof(f165,plain,
! [X0] :
( ( v1_funct_1(k5_lopclset(X0))
& v1_funct_2(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
& m2_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f61]) ).
fof(f166,plain,
! [X0] :
( ( v1_funct_1(k5_lopclset(X0))
& v1_funct_2(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
& m2_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f165]) ).
fof(f175,plain,
! [X0] :
( ( v1_xboole_0(k1_pre_topc(X0))
& v1_membered(k1_pre_topc(X0))
& v2_membered(k1_pre_topc(X0))
& v3_membered(k1_pre_topc(X0))
& v4_membered(k1_pre_topc(X0))
& v5_membered(k1_pre_topc(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f69]) ).
fof(f182,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f74]) ).
fof(f190,plain,
! [X0,X1] :
( ! [X2] :
( m2_subset_1(X2,X0,X1)
<=> m1_subset_1(X2,X1) )
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f82]) ).
fof(f191,plain,
! [X0,X1] :
( ! [X2] :
( m2_subset_1(X2,X0,X1)
<=> m1_subset_1(X2,X1) )
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f190]) ).
fof(f192,plain,
! [X0] :
( m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f193,plain,
! [X0] :
( m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f192]) ).
fof(f197,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f87]) ).
fof(f200,plain,
! [X0] :
( ~ v1_xboole_0(k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f92]) ).
fof(f201,plain,
! [X0] :
( ~ v1_xboole_0(k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f200]) ).
fof(f205,plain,
! [X0] :
( k6_lopclset(X0) = g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f95]) ).
fof(f206,plain,
! [X0] :
( k6_lopclset(X0) = g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f205]) ).
fof(f207,plain,
! [X0] :
( m2_subset_1(k1_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f96]) ).
fof(f208,plain,
! [X0] :
( m2_subset_1(k1_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f207]) ).
fof(f209,plain,
l1_pre_topc(sK0),
inference(cnf_transformation,[],[f118]) ).
fof(f210,plain,
v2_pre_topc(sK0),
inference(cnf_transformation,[],[f118]) ).
fof(f211,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f118]) ).
fof(f212,plain,
~ m1_subset_1(k1_pre_topc(sK0),u1_struct_0(k6_lopclset(sK0))),
inference(cnf_transformation,[],[f118]) ).
fof(f226,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v3_lattices(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = X0 ),
inference(cnf_transformation,[],[f125]) ).
fof(f232,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f14]) ).
fof(f308,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| X0 = X3 ),
inference(cnf_transformation,[],[f160]) ).
fof(f312,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| l3_lattices(g3_lattices(X0,X1,X2)) ),
inference(cnf_transformation,[],[f162]) ).
fof(f313,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| v3_lattices(g3_lattices(X0,X1,X2)) ),
inference(cnf_transformation,[],[f162]) ).
fof(f314,plain,
! [X0] :
( m2_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f164]) ).
fof(f315,plain,
! [X0] :
( v1_funct_2(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f164]) ).
fof(f316,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| v1_funct_1(k4_lopclset(X0)) ),
inference(cnf_transformation,[],[f164]) ).
fof(f317,plain,
! [X0] :
( m2_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f166]) ).
fof(f318,plain,
! [X0] :
( v1_funct_2(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f166]) ).
fof(f319,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| v1_funct_1(k5_lopclset(X0)) ),
inference(cnf_transformation,[],[f166]) ).
fof(f342,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v1_xboole_0(k1_pre_topc(X0)) ),
inference(cnf_transformation,[],[f175]) ).
fof(f349,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| k1_xboole_0 = X0 ),
inference(cnf_transformation,[],[f182]) ).
fof(f363,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0)
| m1_subset_1(X2,X1)
| ~ m2_subset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f191]) ).
fof(f364,plain,
! [X0] :
( m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f193]) ).
fof(f369,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f197]) ).
fof(f374,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f91]) ).
fof(f375,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(k1_lopclset(X0)) ),
inference(cnf_transformation,[],[f201]) ).
fof(f378,plain,
! [X0] :
( ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X0)
| k6_lopclset(X0) = g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)) ),
inference(cnf_transformation,[],[f206]) ).
fof(f379,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| m2_subset_1(k1_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0)) ),
inference(cnf_transformation,[],[f208]) ).
fof(f391,plain,
! [X0] :
( v3_lattices(X0)
| l3_lattices(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = X0 ),
inference(consistent_polarity_flipping,[],[f226]) ).
fof(f429,plain,
! [X2,X3,X0,X1,X4,X5] :
( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| v1_funct_1(X2)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| v1_funct_1(X1)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| X0 = X3 ),
inference(consistent_polarity_flipping,[],[f308]) ).
fof(f433,plain,
! [X2,X0,X1] :
( ~ v3_lattices(g3_lattices(X0,X1,X2))
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| v1_funct_1(X2)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| v1_funct_1(X1)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(consistent_polarity_flipping,[],[f313]) ).
fof(f434,plain,
! [X2,X0,X1] :
( ~ l3_lattices(g3_lattices(X0,X1,X2))
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| v1_funct_1(X2)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| v1_funct_1(X1)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(consistent_polarity_flipping,[],[f312]) ).
fof(f435,plain,
! [X0] :
( ~ v1_funct_1(k4_lopclset(X0))
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(consistent_polarity_flipping,[],[f316]) ).
fof(f436,plain,
! [X0] :
( ~ v1_funct_1(k5_lopclset(X0))
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(consistent_polarity_flipping,[],[f319]) ).
fof(f454,plain,
! [X0] :
( ~ v1_xboole_0(k1_pre_topc(X0))
| ~ l1_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f342]) ).
fof(f458,plain,
! [X0] :
( v1_xboole_0(X0)
| k1_xboole_0 = X0 ),
inference(consistent_polarity_flipping,[],[f349]) ).
fof(f469,plain,
! [X2,X0,X1] :
( m2_subset_1(X2,X0,X1)
| ~ v1_xboole_0(X1)
| ~ v1_xboole_0(X0)
| m1_subset_1(X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(consistent_polarity_flipping,[],[f363]) ).
fof(f474,plain,
! [X0] : v1_xboole_0(k1_zfmisc_1(X0)),
inference(consistent_polarity_flipping,[],[f374]) ).
fof(f476,plain,
! [X0] :
( v1_xboole_0(k1_lopclset(X0))
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(consistent_polarity_flipping,[],[f375]) ).
fof(f477,plain,
! [X0] :
( ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X0)
| ~ m2_subset_1(k1_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0)) ),
inference(consistent_polarity_flipping,[],[f379]) ).
fof(f486,plain,
l1_struct_0(sK0),
inference(resolution,[],[f369,f209]) ).
fof(f501,plain,
! [X0] :
( ~ l1_struct_0(X0)
| k1_pre_topc(X0) = k1_xboole_0 ),
inference(resolution,[],[f458,f454]) ).
fof(f504,plain,
k1_xboole_0 = k1_pre_topc(sK0),
inference(resolution,[],[f501,f486]) ).
fof(f749,plain,
( ~ l1_pre_topc(sK0)
| v3_struct_0(sK0)
| ~ m2_subset_1(k1_pre_topc(sK0),k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0)) ),
inference(resolution,[],[f477,f210]) ).
fof(f750,plain,
( v3_struct_0(sK0)
| ~ m2_subset_1(k1_pre_topc(sK0),k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0)) ),
inference(forward_subsumption_resolution,[],[f749,f209]) ).
fof(f751,plain,
~ m2_subset_1(k1_pre_topc(sK0),k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0)),
inference(forward_subsumption_resolution,[],[f750,f211]) ).
fof(f752,plain,
~ m2_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0)),
inference(forward_demodulation,[],[f751,f504]) ).
fof(f757,plain,
( ~ v1_xboole_0(k1_lopclset(sK0))
| ~ v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0)))
| m1_subset_1(k1_xboole_0,k1_lopclset(sK0))
| ~ m1_subset_1(k1_lopclset(sK0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0)))) ),
inference(resolution,[],[f469,f752]) ).
fof(f759,plain,
( ~ v1_xboole_0(k1_lopclset(sK0))
| m1_subset_1(k1_xboole_0,k1_lopclset(sK0))
| ~ m1_subset_1(k1_lopclset(sK0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0)))) ),
inference(forward_subsumption_resolution,[],[f757,f474]) ).
fof(f761,definition,
( spl25_8
<=> m1_subset_1(k1_lopclset(sK0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0)))) ),
introduced(definition,[new_symbols(definition,[spl25_8])],[avatar_definition]) ).
fof(f763,plain,
( ~ m1_subset_1(k1_lopclset(sK0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0))))
| spl25_8 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f765,definition,
( spl25_9
<=> m1_subset_1(k1_xboole_0,k1_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl25_9])],[avatar_definition]) ).
fof(f767,plain,
( m1_subset_1(k1_xboole_0,k1_lopclset(sK0))
| ~ spl25_9 ),
inference(avatar_component_clause,[],[f765]) ).
fof(f769,definition,
( spl25_10
<=> v1_xboole_0(k1_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl25_10])],[avatar_definition]) ).
fof(f771,plain,
( ~ v1_xboole_0(k1_lopclset(sK0))
| spl25_10 ),
inference(avatar_component_clause,[],[f769]) ).
fof(f772,plain,
( ~ spl25_8
| spl25_9
| ~ spl25_10 ),
inference(avatar_split_clause,[],[f759,f769,f765,f761]) ).
fof(f773,plain,
( v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| spl25_8 ),
inference(resolution,[],[f763,f364]) ).
fof(f775,plain,
( ~ l1_pre_topc(sK0)
| spl25_8 ),
inference(forward_subsumption_resolution,[],[f773,f211]) ).
fof(f776,plain,
( $false
| spl25_8 ),
inference(forward_subsumption_resolution,[],[f775,f209]) ).
fof(f777,plain,
spl25_8,
inference(avatar_contradiction_clause,[],[f776]) ).
fof(f778,plain,
( ~ v2_pre_topc(sK0)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| spl25_10 ),
inference(resolution,[],[f771,f476]) ).
fof(f782,plain,
( v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| spl25_10 ),
inference(forward_subsumption_resolution,[],[f778,f210]) ).
fof(f783,plain,
( ~ l1_pre_topc(sK0)
| spl25_10 ),
inference(forward_subsumption_resolution,[],[f782,f211]) ).
fof(f784,plain,
( $false
| spl25_10 ),
inference(forward_subsumption_resolution,[],[f783,f209]) ).
fof(f785,plain,
spl25_10,
inference(avatar_contradiction_clause,[],[f784]) ).
fof(f793,plain,
! [X0] :
( m1_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0) ),
inference(resolution,[],[f314,f232]) ).
fof(f794,plain,
! [X0] :
( m1_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0) ),
inference(resolution,[],[f317,f232]) ).
fof(f795,plain,
( ~ l1_pre_topc(sK0)
| v3_struct_0(sK0)
| k6_lopclset(sK0) = g3_lattices(k1_lopclset(sK0),k4_lopclset(sK0),k5_lopclset(sK0)) ),
inference(resolution,[],[f378,f210]) ).
fof(f796,plain,
( v3_struct_0(sK0)
| k6_lopclset(sK0) = g3_lattices(k1_lopclset(sK0),k4_lopclset(sK0),k5_lopclset(sK0)) ),
inference(forward_subsumption_resolution,[],[f795,f209]) ).
fof(f797,plain,
k6_lopclset(sK0) = g3_lattices(k1_lopclset(sK0),k4_lopclset(sK0),k5_lopclset(sK0)),
inference(forward_subsumption_resolution,[],[f796,f211]) ).
fof(f888,plain,
! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k6_lopclset(sK0)
| ~ v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| v1_funct_1(k5_lopclset(sK0))
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v1_funct_2(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| v1_funct_1(k4_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| k1_lopclset(sK0) = X0 ),
inference(superposition,[],[f429,f797]) ).
fof(f894,plain,
( ~ v3_lattices(k6_lopclset(sK0))
| ~ v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| v1_funct_1(k5_lopclset(sK0))
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v1_funct_2(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| v1_funct_1(k4_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) ),
inference(superposition,[],[f433,f797]) ).
fof(f895,plain,
( ~ l3_lattices(k6_lopclset(sK0))
| ~ v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| v1_funct_1(k5_lopclset(sK0))
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v1_funct_2(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| v1_funct_1(k4_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) ),
inference(superposition,[],[f434,f797]) ).
fof(f897,definition,
( spl25_21
<=> m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl25_21])],[avatar_definition]) ).
fof(f899,plain,
( ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl25_21 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f901,definition,
( spl25_22
<=> v1_funct_1(k4_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl25_22])],[avatar_definition]) ).
fof(f903,plain,
( v1_funct_1(k4_lopclset(sK0))
| ~ spl25_22 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f905,definition,
( spl25_23
<=> v1_funct_2(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl25_23])],[avatar_definition]) ).
fof(f907,plain,
( ~ v1_funct_2(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl25_23 ),
inference(avatar_component_clause,[],[f905]) ).
fof(f909,definition,
( spl25_24
<=> m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl25_24])],[avatar_definition]) ).
fof(f911,plain,
( ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl25_24 ),
inference(avatar_component_clause,[],[f909]) ).
fof(f913,definition,
( spl25_25
<=> v1_funct_1(k5_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl25_25])],[avatar_definition]) ).
fof(f915,plain,
( v1_funct_1(k5_lopclset(sK0))
| ~ spl25_25 ),
inference(avatar_component_clause,[],[f913]) ).
fof(f917,definition,
( spl25_26
<=> v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl25_26])],[avatar_definition]) ).
fof(f919,plain,
( ~ v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl25_26 ),
inference(avatar_component_clause,[],[f917]) ).
fof(f921,definition,
( spl25_27
<=> l3_lattices(k6_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl25_27])],[avatar_definition]) ).
fof(f923,plain,
( ~ l3_lattices(k6_lopclset(sK0))
| spl25_27 ),
inference(avatar_component_clause,[],[f921]) ).
fof(f924,plain,
( ~ spl25_21
| spl25_22
| ~ spl25_23
| ~ spl25_24
| spl25_25
| ~ spl25_26
| ~ spl25_27 ),
inference(avatar_split_clause,[],[f895,f921,f917,f913,f909,f905,f901,f897]) ).
fof(f926,definition,
( spl25_28
<=> v3_lattices(k6_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl25_28])],[avatar_definition]) ).
fof(f928,plain,
( ~ v3_lattices(k6_lopclset(sK0))
| spl25_28 ),
inference(avatar_component_clause,[],[f926]) ).
fof(f929,plain,
( ~ spl25_21
| spl25_22
| ~ spl25_23
| ~ spl25_24
| spl25_25
| ~ spl25_26
| ~ spl25_28 ),
inference(avatar_split_clause,[],[f894,f926,f917,f913,f909,f905,f901,f897]) ).
fof(f939,definition,
( spl25_31
<=> ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k6_lopclset(sK0)
| k1_lopclset(sK0) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl25_31])],[avatar_definition]) ).
fof(f940,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k6_lopclset(sK0)
| k1_lopclset(sK0) = X0 )
| ~ spl25_31 ),
inference(avatar_component_clause,[],[f939]) ).
fof(f941,plain,
( ~ spl25_21
| spl25_22
| ~ spl25_23
| ~ spl25_24
| spl25_25
| ~ spl25_26
| spl25_31 ),
inference(avatar_split_clause,[],[f888,f939,f917,f913,f909,f905,f901,f897]) ).
fof(f1963,plain,
( v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK0)
| spl25_21 ),
inference(resolution,[],[f899,f794]) ).
fof(f1964,plain,
( ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK0)
| spl25_21 ),
inference(forward_subsumption_resolution,[],[f1963,f211]) ).
fof(f1965,plain,
( ~ v2_pre_topc(sK0)
| spl25_21 ),
inference(forward_subsumption_resolution,[],[f1964,f209]) ).
fof(f1966,plain,
( $false
| spl25_21 ),
inference(forward_subsumption_resolution,[],[f1965,f210]) ).
fof(f1967,plain,
spl25_21,
inference(avatar_contradiction_clause,[],[f1966]) ).
fof(f1979,plain,
( ~ v2_pre_topc(sK0)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| spl25_23 ),
inference(resolution,[],[f907,f315]) ).
fof(f1980,plain,
( v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| spl25_23 ),
inference(forward_subsumption_resolution,[],[f1979,f210]) ).
fof(f1981,plain,
( ~ l1_pre_topc(sK0)
| spl25_23 ),
inference(forward_subsumption_resolution,[],[f1980,f211]) ).
fof(f1982,plain,
( $false
| spl25_23 ),
inference(forward_subsumption_resolution,[],[f1981,f209]) ).
fof(f1983,plain,
spl25_23,
inference(avatar_contradiction_clause,[],[f1982]) ).
fof(f1989,plain,
( v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK0)
| spl25_24 ),
inference(resolution,[],[f911,f793]) ).
fof(f1990,plain,
( ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK0)
| spl25_24 ),
inference(forward_subsumption_resolution,[],[f1989,f211]) ).
fof(f1991,plain,
( ~ v2_pre_topc(sK0)
| spl25_24 ),
inference(forward_subsumption_resolution,[],[f1990,f209]) ).
fof(f1992,plain,
( $false
| spl25_24 ),
inference(forward_subsumption_resolution,[],[f1991,f210]) ).
fof(f1993,plain,
spl25_24,
inference(avatar_contradiction_clause,[],[f1992]) ).
fof(f1994,plain,
( ~ v2_pre_topc(sK0)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| ~ spl25_22 ),
inference(resolution,[],[f903,f435]) ).
fof(f1995,plain,
( v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| ~ spl25_22 ),
inference(forward_subsumption_resolution,[],[f1994,f210]) ).
fof(f1996,plain,
( ~ l1_pre_topc(sK0)
| ~ spl25_22 ),
inference(forward_subsumption_resolution,[],[f1995,f211]) ).
fof(f1997,plain,
( $false
| ~ spl25_22 ),
inference(forward_subsumption_resolution,[],[f1996,f209]) ).
fof(f1998,plain,
~ spl25_22,
inference(avatar_contradiction_clause,[],[f1997]) ).
fof(f2008,plain,
( ~ v2_pre_topc(sK0)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| spl25_26 ),
inference(resolution,[],[f919,f318]) ).
fof(f2009,plain,
( v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| spl25_26 ),
inference(forward_subsumption_resolution,[],[f2008,f210]) ).
fof(f2010,plain,
( ~ l1_pre_topc(sK0)
| spl25_26 ),
inference(forward_subsumption_resolution,[],[f2009,f211]) ).
fof(f2011,plain,
( $false
| spl25_26 ),
inference(forward_subsumption_resolution,[],[f2010,f209]) ).
fof(f2012,plain,
spl25_26,
inference(avatar_contradiction_clause,[],[f2011]) ).
fof(f2013,plain,
( ~ v2_pre_topc(sK0)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| ~ spl25_25 ),
inference(resolution,[],[f915,f436]) ).
fof(f2014,plain,
( v3_struct_0(sK0)
| ~ l1_pre_topc(sK0)
| ~ spl25_25 ),
inference(forward_subsumption_resolution,[],[f2013,f210]) ).
fof(f2015,plain,
( ~ l1_pre_topc(sK0)
| ~ spl25_25 ),
inference(forward_subsumption_resolution,[],[f2014,f211]) ).
fof(f2016,plain,
( $false
| ~ spl25_25 ),
inference(forward_subsumption_resolution,[],[f2015,f209]) ).
fof(f2017,plain,
~ spl25_25,
inference(avatar_contradiction_clause,[],[f2016]) ).
fof(f2018,plain,
( l3_lattices(k6_lopclset(sK0))
| k6_lopclset(sK0) = g3_lattices(u1_struct_0(k6_lopclset(sK0)),u2_lattices(k6_lopclset(sK0)),u1_lattices(k6_lopclset(sK0)))
| spl25_28 ),
inference(resolution,[],[f928,f391]) ).
fof(f2019,plain,
( k6_lopclset(sK0) = g3_lattices(u1_struct_0(k6_lopclset(sK0)),u2_lattices(k6_lopclset(sK0)),u1_lattices(k6_lopclset(sK0)))
| spl25_27
| spl25_28 ),
inference(forward_subsumption_resolution,[],[f2018,f923]) ).
fof(f5676,plain,
( k6_lopclset(sK0) != k6_lopclset(sK0)
| u1_struct_0(k6_lopclset(sK0)) = k1_lopclset(sK0)
| spl25_27
| spl25_28
| ~ spl25_31 ),
inference(superposition,[],[f940,f2019]) ).
fof(f5686,plain,
( u1_struct_0(k6_lopclset(sK0)) = k1_lopclset(sK0)
| spl25_27
| spl25_28
| ~ spl25_31 ),
inference(trivial_inequality_removal,[],[f5676]) ).
fof(f12285,definition,
( spl25_947
<=> u1_struct_0(k6_lopclset(sK0)) = k1_lopclset(sK0) ),
introduced(definition,[new_symbols(definition,[spl25_947])],[avatar_definition]) ).
fof(f12287,plain,
( u1_struct_0(k6_lopclset(sK0)) = k1_lopclset(sK0)
| ~ spl25_947 ),
inference(avatar_component_clause,[],[f12285]) ).
fof(f60682,plain,
( spl25_947
| spl25_27
| spl25_28
| ~ spl25_31 ),
inference(avatar_split_clause,[],[f5686,f939,f926,f921,f12285]) ).
fof(f277340,plain,
( ~ m1_subset_1(k1_pre_topc(sK0),k1_lopclset(sK0))
| ~ spl25_947 ),
inference(superposition,[],[f212,f12287]) ).
fof(f277558,plain,
( ~ m1_subset_1(k1_xboole_0,k1_lopclset(sK0))
| ~ spl25_947 ),
inference(forward_demodulation,[],[f277340,f504]) ).
fof(f277650,plain,
( $false
| ~ spl25_9
| ~ spl25_947 ),
inference(forward_subsumption_resolution,[],[f277558,f767]) ).
fof(f277651,plain,
( ~ spl25_9
| ~ spl25_947 ),
inference(avatar_contradiction_clause,[],[f277650]) ).
cnf(s6,plain,
( ~ spl25_8
| spl25_9
| ~ spl25_10 ),
inference(sat_conversion,[],[f772]) ).
cnf(s7,plain,
spl25_8,
inference(sat_conversion,[],[f777]) ).
cnf(s8,plain,
spl25_10,
inference(sat_conversion,[],[f785]) ).
cnf(s18,plain,
( ~ spl25_21
| spl25_22
| ~ spl25_23
| ~ spl25_24
| spl25_25
| ~ spl25_26
| ~ spl25_27 ),
inference(sat_conversion,[],[f924]) ).
cnf(s19,plain,
( ~ spl25_21
| spl25_22
| ~ spl25_23
| ~ spl25_24
| spl25_25
| ~ spl25_26
| ~ spl25_28 ),
inference(sat_conversion,[],[f929]) ).
cnf(s22,plain,
( ~ spl25_21
| spl25_22
| ~ spl25_23
| ~ spl25_24
| spl25_25
| ~ spl25_26
| spl25_31 ),
inference(sat_conversion,[],[f941]) ).
cnf(s76,plain,
spl25_21,
inference(sat_conversion,[],[f1967]) ).
cnf(s78,plain,
spl25_23,
inference(sat_conversion,[],[f1983]) ).
cnf(s80,plain,
spl25_24,
inference(sat_conversion,[],[f1993]) ).
cnf(s81,plain,
~ spl25_22,
inference(sat_conversion,[],[f1998]) ).
cnf(s83,plain,
spl25_26,
inference(sat_conversion,[],[f2012]) ).
cnf(s84,plain,
~ spl25_25,
inference(sat_conversion,[],[f2017]) ).
cnf(s6012,plain,
( spl25_27
| spl25_28
| ~ spl25_31
| spl25_947 ),
inference(sat_conversion,[],[f60682]) ).
cnf(s34013,plain,
( ~ spl25_9
| ~ spl25_947 ),
inference(sat_conversion,[],[f277651]) ).
cnf(s35018,plain,
spl25_31,
inference(rat,[],[s22,s83,s84,s80,s78,s81,s76]) ).
cnf(s35021,plain,
~ spl25_28,
inference(rat,[],[s19,s83,s84,s80,s78,s81,s76]) ).
cnf(s35022,plain,
~ spl25_27,
inference(rat,[],[s18,s83,s84,s80,s78,s81,s76]) ).
cnf(s35025,plain,
spl25_947,
inference(rat,[],[s6012,s35021,s35018,s35022]) ).
cnf(s35037,plain,
~ spl25_9,
inference(rat,[],[s34013,s35025]) ).
cnf(s35131,plain,
$false,
inference(rat,[],[s6,s8,s35037,s7]) ).
fof(f277966,plain,
$false,
inference(avatar_sat_refutation,[],[s35131]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT287+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.37 % Computer : n004.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 14:15:22 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.51/2.61 % (3562605)Will run a generic schedule for satisfiability detection.
% 15.51/2.61 % (3562614)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2690885910:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.51/2.61 % (3562611)% WARNING: option uhcvi not known.
% 15.51/2.61 % (3562610)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3063939196_2999 on theBenchmark for (2999ds/0Mi)
% 15.51/2.61 % (3562611)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2109634926:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.51/2.61 % (3562612)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3508640182:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.51/2.61 % (3562613)dis+10_1_sil=32000:sp=arity:random_seed=567924880:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.51/2.61 % (3562616)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=90870813:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.51/2.61 % (3562615)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=594546438:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.51/2.61 % TRYING [1]
% 15.51/2.61 % TRYING [2]
% 15.51/2.61 % TRYING [3]
% 15.51/2.61 % TRYING [4]
% 15.51/2.61 % (3562614)Instruction limit reached!
% 15.51/2.61 % (3562614)------------------------------
% 15.51/2.61 % (3562614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.51/2.61 % (3562614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.51/2.61 % (3562614)CaDiCaL version: 2.1.3
% 15.51/2.61 % (3562614)Termination reason: Instruction limit
% 15.51/2.61 % (3562614)Termination phase: Saturation
% 15.51/2.61 % (3562614)Time elapsed: 0.042 s
% 15.51/2.61 % (3562614)Peak memory usage: 13 MB
% 15.51/2.61 % (3562614)Instructions burned: 117 (million)
% 15.51/2.61 % TRYING [5]
% 15.51/2.61 % (3562624)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1987586645:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.51/2.61 % TRYING [1]
% 15.51/2.61 % TRYING [2]
% 15.51/2.61 % TRYING [3]
% 15.51/2.61 % TRYING [4]
% 15.51/2.61 % (3562613)Instruction limit reached!
% 15.51/2.61 % (3562613)------------------------------
% 15.51/2.61 % (3562613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.51/2.61 % (3562613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.51/2.61 % (3562613)CaDiCaL version: 2.1.3
% 15.51/2.61 % (3562613)Termination reason: Instruction limit
% 15.51/2.61 % (3562613)Termination phase: Saturation
% 15.51/2.61 % (3562613)Time elapsed: 0.068 s
% 15.51/2.61 % (3562613)Peak memory usage: 13 MB
% 15.51/2.61 % (3562613)Instructions burned: 104 (million)
% 15.51/2.61 % (3562615)Instruction limit reached!
% 15.51/2.61 % (3562615)------------------------------
% 15.51/2.61 % (3562615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.51/2.61 % (3562615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.51/2.61 % (3562615)CaDiCaL version: 2.1.3
% 15.51/2.61 % (3562615)Termination reason: Instruction limit
% 15.51/2.61 % (3562615)Termination phase: Saturation
% 15.51/2.61 % (3562615)Time elapsed: 0.077 s
% 15.51/2.61 % (3562615)Peak memory usage: 13 MB
% 15.51/2.61 % (3562615)Instructions burned: 131 (million)
% 15.51/2.61 % (3562626)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2628520901:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.51/2.61 % TRYING [6]
% 15.51/2.61 % (3562627)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=91083260:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.51/2.61 % (3562616)Instruction limit reached!
% 15.51/2.61 % (3562616)------------------------------
% 15.51/2.61 % (3562616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.51/2.61 % (3562616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.51/2.61 % (3562616)CaDiCaL version: 2.1.3
% 15.51/2.61 % (3562616)Termination reason: Instruction limit
% 15.51/2.61 % (3562616)Termination phase: Saturation
% 15.51/2.61 % (3562616)Time elapsed: 0.100 s
% 15.51/2.61 % (3562616)Peak memory usage: 14 MB
% 15.51/2.61 % (3562616)Instructions burned: 159 (million)
% 15.51/2.61 % TRYING [5]
% 15.51/2.61 % (3562630)ott-21_1_sil=16000:fs=off:random_seed=2691346447:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.51/2.61 % (3562626)Instruction limit reached!
% 15.51/2.61 % (3562626)------------------------------
% 15.51/2.61 % (3562626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.58/5.02 % (3562626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.58/5.02 % (3562626)CaDiCaL version: 2.1.3
% 30.58/5.02 % (3562626)Termination reason: Instruction limit
% 30.58/5.02 % (3562626)Termination phase: Saturation
% 30.58/5.02 % (3562626)Time elapsed: 0.077 s
% 30.58/5.02 % (3562626)Peak memory usage: 13 MB
% 30.58/5.02 % (3562626)Instructions burned: 131 (million)
% 30.58/5.02 % (3562624)Instruction limit reached!
% 30.58/5.02 % (3562624)------------------------------
% 30.58/5.02 % (3562624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.58/5.02 % (3562624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.58/5.02 % (3562624)CaDiCaL version: 2.1.3
% 30.58/5.02 % (3562624)Termination reason: Instruction limit
% 30.58/5.02 % (3562624)Termination phase: Finite model building constraint generation
% 30.58/5.02 % (3562624)Time elapsed: 0.133 s
% 30.58/5.02 % (3562624)Peak memory usage: 30 MB
% 30.58/5.02 % (3562624)Instructions burned: 716 (million)
% 30.58/5.02 % (3562632)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3841479375:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 30.58/5.02 % (3562633)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2157083949:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 30.58/5.02 % TRYING [1]
% 30.58/5.02 % TRYING [2]
% 30.58/5.02 % TRYING [3]
% 30.58/5.02 % TRYING [4]
% 30.58/5.02 % (3562630)Instruction limit reached!
% 30.58/5.02 % (3562630)------------------------------
% 30.58/5.02 % (3562630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.58/5.02 % (3562630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.58/5.02 % (3562630)CaDiCaL version: 2.1.3
% 30.58/5.02 % (3562630)Termination reason: Instruction limit
% 30.58/5.02 % (3562630)Termination phase: Saturation
% 30.58/5.02 % (3562630)Time elapsed: 0.096 s
% 30.58/5.02 % (3562630)Peak memory usage: 13 MB
% 30.58/5.02 % (3562630)Instructions burned: 182 (million)
% 30.58/5.02 % (3562636)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2918591423:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 30.58/5.02 % TRYING [5]
% 30.58/5.02 % TRYING [7]
% 30.58/5.02 % TRYING [6]
% 30.58/5.02 % (3562633)Instruction limit reached!
% 30.58/5.02 % (3562633)------------------------------
% 30.58/5.02 % (3562633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.58/5.02 % (3562633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.58/5.02 % (3562633)CaDiCaL version: 2.1.3
% 30.58/5.02 % (3562633)Termination reason: Instruction limit
% 30.58/5.02 % (3562633)Termination phase: Finite model building constraint generation
% 30.58/5.02 % (3562633)Time elapsed: 0.172 s
% 30.58/5.02 % (3562633)Peak memory usage: 23 MB
% 30.58/5.02 % (3562633)Instructions burned: 871 (million)
% 30.58/5.02 % (3562638)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2340526688:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 30.58/5.02 % (3562627)Instruction limit reached!
% 30.58/5.02 % (3562627)------------------------------
% 30.58/5.02 % (3562627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.58/5.02 % (3562627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.58/5.02 % (3562627)CaDiCaL version: 2.1.3
% 30.58/5.02 % (3562627)Termination reason: Instruction limit
% 30.58/5.02 % (3562627)Termination phase: Saturation
% 30.58/5.02 % (3562627)Time elapsed: 0.307 s
% 30.58/5.02 % (3562627)Peak memory usage: 15 MB
% 30.58/5.02 % (3562627)Instructions burned: 686 (million)
% 30.58/5.02 % TRYING [14]
% 30.58/5.02 % (3562640)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=533372749:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 30.58/5.02 % (3562632)Instruction limit reached!
% 30.58/5.02 % (3562632)------------------------------
% 30.58/5.02 % (3562632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.58/5.02 % (3562632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.58/5.02 % (3562632)CaDiCaL version: 2.1.3
% 30.58/5.02 % (3562632)Termination reason: Instruction limit
% 30.58/5.02 % (3562632)Termination phase: Saturation
% 30.58/5.02 % (3562632)Time elapsed: 0.322 s
% 30.58/5.02 % (3562632)Peak memory usage: 15 MB
% 30.58/5.02 % (3562632)Instructions burned: 477 (million)
% 30.58/5.02 % (3562642)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3415401384:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 63.05/9.37 % (3562638)Instruction limit reached!
% 63.05/9.37 % (3562638)------------------------------
% 63.05/9.37 % (3562638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.05/9.37 % (3562638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.05/9.37 % (3562638)CaDiCaL version: 2.1.3
% 63.05/9.37 % (3562638)Termination reason: Instruction limit
% 63.05/9.37 % (3562638)Termination phase: Finite model building constraint generation
% 63.05/9.37 % (3562638)Time elapsed: 0.166 s
% 63.05/9.37 % (3562638)Peak memory usage: 63 MB
% 63.05/9.37 % (3562638)Instructions burned: 897 (million)
% 63.05/9.37 % (3562644)fmb+10_1_sil=64000:random_seed=3408795205:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 63.05/9.37 % TRYING [1]
% 63.05/9.37 % TRYING [2]
% 63.05/9.37 % TRYING [3]
% 63.05/9.37 % TRYING [4]
% 63.05/9.37 % TRYING [5]
% 63.05/9.37 % (3562640)Instruction limit reached!
% 63.05/9.37 % (3562640)------------------------------
% 63.05/9.37 % (3562640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.05/9.37 % (3562640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.05/9.37 % (3562640)CaDiCaL version: 2.1.3
% 63.05/9.37 % (3562640)Termination reason: Instruction limit
% 63.05/9.37 % (3562640)Termination phase: Saturation
% 63.05/9.37 % (3562640)Time elapsed: 0.323 s
% 63.05/9.37 % (3562640)Peak memory usage: 16 MB
% 63.05/9.37 % (3562640)Instructions burned: 693 (million)
% 63.05/9.37 % (3562646)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=756462146:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 63.05/9.37 % TRYING [20]
% 63.05/9.37 % TRYING [8]
% 63.05/9.37 % (3562636)Instruction limit reached!
% 63.05/9.37 % (3562636)------------------------------
% 63.05/9.37 % (3562636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.05/9.37 % (3562636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.05/9.37 % (3562636)CaDiCaL version: 2.1.3
% 63.05/9.37 % (3562636)Termination reason: Instruction limit
% 63.05/9.37 % (3562636)Termination phase: Saturation
% 63.05/9.37 % (3562636)Time elapsed: 0.672 s
% 63.05/9.37 % (3562636)Peak memory usage: 24 MB
% 63.05/9.37 % (3562636)Instructions burned: 1180 (million)
% 63.05/9.37 % (3562648)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=320805868:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 63.05/9.37 % TRYING [8]
% 63.05/9.37 % (3562642)Instruction limit reached!
% 63.05/9.37 % (3562642)------------------------------
% 63.05/9.37 % (3562642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.05/9.37 % (3562642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.05/9.37 % (3562642)CaDiCaL version: 2.1.3
% 63.05/9.37 % (3562642)Termination reason: Instruction limit
% 63.05/9.37 % (3562642)Termination phase: Saturation
% 63.05/9.37 % (3562642)Time elapsed: 0.494 s
% 63.05/9.37 % (3562642)Peak memory usage: 21 MB
% 63.05/9.37 % (3562642)Instructions burned: 880 (million)
% 63.05/9.37 % (3562650)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1753485484:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 63.05/9.37 % (3562648)Instruction limit reached!
% 63.05/9.37 % (3562648)------------------------------
% 63.05/9.37 % (3562648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.05/9.37 % (3562648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.05/9.37 % (3562648)CaDiCaL version: 2.1.3
% 63.05/9.37 % (3562648)Termination reason: Instruction limit
% 63.05/9.37 % (3562648)Termination phase: Finite model building SAT solving
% 63.05/9.37 % (3562648)Time elapsed: 0.355 s
% 63.05/9.37 % (3562648)Peak memory usage: 57 MB
% 63.05/9.37 % (3562648)Instructions burned: 923 (million)
% 63.05/9.37 % (3562652)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1055838310:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 63.05/9.37 % TRYING [6]
% 63.05/9.37 % (3562652)Instruction limit reached!
% 63.05/9.37 % (3562652)------------------------------
% 63.05/9.37 % (3562652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.05/9.37 % (3562652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.05/9.37 % (3562652)CaDiCaL version: 2.1.3
% 63.05/9.37 % (3562652)Termination reason: Instruction limit
% 63.05/9.37 % (3562652)Termination phase: Saturation
% 63.05/9.37 % (3562652)Time elapsed: 0.839 s
% 63.05/9.37 % (3562652)Peak memory usage: 30 MB
% 63.05/9.37 % (3562652)Instructions burned: 1473 (million)
% 63.05/9.37 % (3562654)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1469855568:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 52.67/12.06 % TRYING [77]
% 52.67/12.06 % (3562650)Instruction limit reached!
% 52.67/12.06 % (3562650)------------------------------
% 52.67/12.06 % (3562650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562650)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562650)Termination reason: Instruction limit
% 52.67/12.06 % (3562650)Termination phase: Saturation
% 52.67/12.06 % (3562650)Time elapsed: 2.698 s
% 52.67/12.06 % (3562650)Peak memory usage: 31 MB
% 52.67/12.06 % (3562650)Instructions burned: 5132 (million)
% 52.67/12.06 % (3562656)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=521273899:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 52.67/12.06 % TRYING [16]
% 52.67/12.06 % (3562646)Instruction limit reached!
% 52.67/12.06 % (3562646)------------------------------
% 52.67/12.06 % (3562646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562646)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562646)Termination reason: Instruction limit
% 52.67/12.06 % (3562646)Termination phase: Finite model building constraint generation
% 52.67/12.06 % (3562646)Time elapsed: 3.143 s
% 52.67/12.06 % (3562646)Peak memory usage: 520 MB
% 52.67/12.06 % (3562646)Instructions burned: 9518 (million)
% 52.67/12.06 % (3562658)ott-2_1_sil=16000:newcnf=on:random_seed=2014518068:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2959 on theBenchmark for (2959ds/869Mi)
% 52.67/12.06 % (3562654)Instruction limit reached!
% 52.67/12.06 % (3562654)------------------------------
% 52.67/12.06 % (3562654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562654)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562654)Termination reason: Instruction limit
% 52.67/12.06 % (3562654)Termination phase: Finite model building constraint generation
% 52.67/12.06 % (3562654)Time elapsed: 2.162 s
% 52.67/12.06 % (3562654)Peak memory usage: 363 MB
% 52.67/12.06 % (3562654)Instructions burned: 6325 (million)
% 52.67/12.06 % (3562660)ott+10_1_sil=32000:tgt=ground:random_seed=3858857348:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 52.67/12.06 % (3562656)Instruction limit reached!
% 52.67/12.06 % (3562656)------------------------------
% 52.67/12.06 % (3562656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562656)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562656)Termination reason: Instruction limit
% 52.67/12.06 % (3562656)Termination phase: Finite model building constraint generation
% 52.67/12.06 % (3562656)Time elapsed: 0.703 s
% 52.67/12.06 % (3562656)Peak memory usage: 127 MB
% 52.67/12.06 % (3562656)Instructions burned: 2176 (million)
% 52.67/12.06 % (3562658)Instruction limit reached!
% 52.67/12.06 % (3562658)------------------------------
% 52.67/12.06 % (3562658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562658)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562658)Termination reason: Instruction limit
% 52.67/12.06 % (3562658)Termination phase: Saturation
% 52.67/12.06 % (3562658)Time elapsed: 0.494 s
% 52.67/12.06 % (3562658)Peak memory usage: 20 MB
% 52.67/12.06 % (3562658)Instructions burned: 870 (million)
% 52.67/12.06 % (3562662)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=525009985:i=54282_2954 on theBenchmark for (2954ds/54282Mi)
% 52.67/12.06 % TRYING [1]
% 52.67/12.06 % TRYING [2]
% 52.67/12.06 % (3562663)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3439726735:i=3512:aac=none_2954 on theBenchmark for (2954ds/3512Mi)
% 52.67/12.06 % TRYING [3]
% 52.67/12.06 % TRYING [4]
% 52.67/12.06 % TRYING [5]
% 52.67/12.06 % (3562644)Instruction limit reached!
% 52.67/12.06 % (3562644)------------------------------
% 52.67/12.06 % (3562644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562644)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562644)Termination reason: Instruction limit
% 52.67/12.06 % (3562644)Termination phase: Finite model building SAT solving
% 52.67/12.06 % (3562644)Time elapsed: 4.001 s
% 52.67/12.06 % (3562644)Peak memory usage: 98 MB
% 52.67/12.06 % (3562644)Instructions burned: 22064 (million)
% 52.67/12.06 % (3562666)dis+21_1_sil=32000:sas=cadical:random_seed=2766275621:i=3773:amm=off_2954 on theBenchmark for (2954ds/3773Mi)
% 52.67/12.06 % TRYING [6]
% 52.67/12.06 % TRYING [7]
% 52.67/12.06 % TRYING [8]
% 52.67/12.06 % (3562666)Instruction limit reached!
% 52.67/12.06 % (3562666)------------------------------
% 52.67/12.06 % (3562666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562666)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562666)Termination reason: Instruction limit
% 52.67/12.06 % (3562666)Termination phase: Saturation
% 52.67/12.06 % (3562666)Time elapsed: 1.104 s
% 52.67/12.06 % (3562666)Peak memory usage: 34 MB
% 52.67/12.06 % (3562666)Instructions burned: 3776 (million)
% 52.67/12.06 % (3562668)ott+11_1_sil=16000:gs=on:random_seed=2537804079:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2942 on theBenchmark for (2942ds/2251Mi)
% 52.67/12.06 % (3562663)Instruction limit reached!
% 52.67/12.06 % (3562663)------------------------------
% 52.67/12.06 % (3562663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562663)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562663)Termination reason: Instruction limit
% 52.67/12.06 % (3562663)Termination phase: Saturation
% 52.67/12.06 % (3562663)Time elapsed: 1.837 s
% 52.67/12.06 % (3562663)Peak memory usage: 24 MB
% 52.67/12.06 % (3562663)Instructions burned: 3512 (million)
% 52.67/12.06 % (3562670)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4225982361:fmbsr=1.6:i=67534_2936 on theBenchmark for (2936ds/67534Mi)
% 52.67/12.06 % TRYING [7]
% 52.67/12.06 % (3562668)Instruction limit reached!
% 52.67/12.06 % (3562668)------------------------------
% 52.67/12.06 % (3562668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562668)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562668)Termination reason: Instruction limit
% 52.67/12.06 % (3562668)Termination phase: Saturation
% 52.67/12.06 % (3562668)Time elapsed: 0.745 s
% 52.67/12.06 % (3562668)Peak memory usage: 33 MB
% 52.67/12.06 % (3562668)Instructions burned: 2254 (million)
% 52.67/12.06 % (3562672)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2589484643:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2935 on theBenchmark for (2935ds/4591Mi)
% 52.67/12.06 % (3562660)Instruction limit reached!
% 52.67/12.06 % (3562660)------------------------------
% 52.67/12.06 % (3562660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562660)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562660)Termination reason: Instruction limit
% 52.67/12.06 % (3562660)Termination phase: Saturation
% 52.67/12.06 % (3562660)Time elapsed: 2.675 s
% 52.67/12.06 % (3562660)Peak memory usage: 42 MB
% 52.67/12.06 % (3562660)Instructions burned: 5114 (million)
% 52.67/12.06 % (3562674)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=842143101:i=29340_2928 on theBenchmark for (2928ds/29340Mi)
% 52.67/12.06 % TRYING [8]
% 52.67/12.06 % (3562672)Instruction limit reached!
% 52.67/12.06 % (3562672)------------------------------
% 52.67/12.06 % (3562672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562672)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562672)Termination reason: Instruction limit
% 52.67/12.06 % (3562672)Termination phase: Saturation
% 52.67/12.06 % (3562672)Time elapsed: 1.073 s
% 52.67/12.06 % (3562672)Peak memory usage: 38 MB
% 52.67/12.06 % (3562672)Instructions burned: 4595 (million)
% 52.67/12.06 % (3562676)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1161178901:i=5211_2924 on theBenchmark for (2924ds/5211Mi)
% 52.67/12.06 % TRYING [9]
% 52.67/12.06 % (3562676)Instruction limit reached!
% 52.67/12.06 % (3562676)------------------------------
% 52.67/12.06 % (3562676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562676)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562676)Termination reason: Instruction limit
% 52.67/12.06 % (3562676)Termination phase: Saturation
% 52.67/12.06 % (3562676)Time elapsed: 1.369 s
% 52.67/12.06 % (3562676)Peak memory usage: 46 MB
% 52.67/12.06 % (3562676)Instructions burned: 5214 (million)
% 52.67/12.06 % (3562678)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1676783528:i=5497:nm=2_2910 on theBenchmark for (2910ds/5497Mi)
% 52.67/12.06 % TRYING [17]
% 52.67/12.06 % (3562678)Instruction limit reached!
% 52.67/12.06 % (3562678)------------------------------
% 52.67/12.06 % (3562678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562678)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562678)Termination reason: Instruction limit
% 52.67/12.06 % (3562678)Termination phase: Finite model building constraint generation
% 52.67/12.06 % (3562678)Time elapsed: 0.956 s
% 52.67/12.06 % (3562678)Peak memory usage: 265 MB
% 52.67/12.06 % (3562678)Instructions burned: 5500 (million)
% 52.67/12.06 % (3562680)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1119845722:fmbsr=2:i=46332_2900 on theBenchmark for (2900ds/46332Mi)
% 52.67/12.06 % TRYING [15]
% 52.67/12.06 % (3562611) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3562605-3562611"...
% 52.67/12.06 % (3562611)...printing done.
% 52.67/12.06 % (3562611)Refutation found. Thanks to Tanya!
% 52.67/12.06 % SZS status Theorem for theBenchmark
% 52.67/12.06 % SZS output start Proof for theBenchmark
% See solution above
% 52.67/12.06 % (3562611)------------------------------
% 52.67/12.06 % (3562611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.67/12.06 % (3562611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.67/12.06 % (3562611)CaDiCaL version: 2.1.3
% 52.67/12.06 % (3562611)Termination reason: Refutation
% 52.67/12.06 % (3562611)Time elapsed: 11.538 s
% 52.67/12.06 % (3562611)Peak memory usage: 115 MB
% 52.67/12.06 % (3562611)Instructions burned: 20896 (million)
% 52.67/12.06 % (3562605)Success in time 11.65 s
% 52.67/12.06 % Vampire exiting
%------------------------------------------------------------------------------