%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT374+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:48:42 AM UTC 2026
% Result : Theorem 12.94s 3.33s
% Output : Refutation 12.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 28
% Syntax : Number of formulae : 224 ( 25 unt; 12 def)
% Number of atoms : 861 ( 17 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 1082 ( 445 ~; 487 |; 84 &)
% ( 28 <=>; 36 =>; 0 <=; 2 <~>)
% Maximal formula depth : 25 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 40 ( 38 usr; 13 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 3 con; 0-4 aty)
% Number of variables : 186 ( 0 sgn 181 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
=> ( m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t49_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
=> ( m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f37,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ~ v1_xboole_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_setfam_1) ).
fof(f50,axiom,
! [X0] :
( l2_altcat_1(X0)
=> ! [X1] :
( l2_altcat_1(X1)
=> ( m1_altcat_2(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& r2_altcat_2(k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_altcat_1(X1),u1_altcat_1(X0))
& r2_altcat_2(k3_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1),u1_struct_0(X1)),k3_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0)),u2_altcat_1(X1),u2_altcat_1(X0)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d11_altcat_2) ).
fof(f51,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_altcat_1(X1)
& v6_altcat_1(X1)
& v3_altcat_2(X1,k5_waybel34(X0))
& m1_altcat_2(X1,k5_waybel34(X0)) )
=> ( X1 = k9_waybel34(X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
=> m1_subset_1(X2,u1_struct_0(X1)) )
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( X4 = X2
& X5 = X3 )
=> ( k1_altcat_1(k5_waybel34(X0),X2,X3) = k1_xboole_0
| ! [X6] :
( m1_subset_1(X6,k1_altcat_1(k5_waybel34(X0),X2,X3))
=> ( r2_hidden(X6,k1_altcat_1(X1,X4,X5))
<=> v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X3),k3_yellow21(k5_waybel34(X0),X2),k5_yellow21(k5_waybel34(X0),X2,X3,X6)),k3_yellow21(k5_waybel34(X0),X3),k3_yellow21(k5_waybel34(X0),X2)) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d11_waybel34) ).
fof(f65,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& l2_altcat_1(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_waybel34) ).
fof(f67,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k9_waybel34(X0))
& v2_altcat_1(k9_waybel34(X0))
& v6_altcat_1(k9_waybel34(X0))
& v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_waybel34) ).
fof(f68,axiom,
! [X0] :
( l1_altcat_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_altcat_1) ).
fof(f71,axiom,
! [X0] :
( l2_altcat_1(X0)
=> l1_altcat_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l2_altcat_1) ).
fof(f72,axiom,
! [X0] :
( l2_altcat_1(X0)
=> ! [X1] :
( m1_altcat_2(X1,X0)
=> l2_altcat_1(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_altcat_2) ).
fof(f89,axiom,
! [X0] :
? [X1] : m1_subset_1(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(f96,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f131,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
=> ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_waybel34) ).
fof(f133,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(f134,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f135,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f138,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f140,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_altcat_1(X1)
& v6_altcat_1(X1)
& v3_altcat_2(X1,k5_waybel34(X0))
& m1_altcat_2(X1,k5_waybel34(X0)) )
=> ( X1 = k9_waybel34(X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
=> m1_subset_1(X2,u1_struct_0(X1)) )
& ! [X3] :
( m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k5_waybel34(X0)))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ! [X6] :
( m1_subset_1(X6,u1_struct_0(X1))
=> ( ( X3 = X5
& X4 = X6 )
=> ( k1_xboole_0 = k1_altcat_1(k5_waybel34(X0),X3,X4)
| ! [X7] :
( m1_subset_1(X7,k1_altcat_1(k5_waybel34(X0),X3,X4))
=> ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
<=> v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3)) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f51]) ).
fof(f180,plain,
? [X0] :
( ? [X1] :
( ( m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
<~> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
& ~ v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f181,plain,
? [X0] :
( ? [X1] :
( ( m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
<~> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
& ~ v2_setfam_1(X0) ),
inference(flattening,[],[f180]) ).
fof(f227,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f250,plain,
! [X0] :
( ! [X1] :
( ( m1_altcat_2(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& r2_altcat_2(k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_altcat_1(X1),u1_altcat_1(X0))
& r2_altcat_2(k3_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1),u1_struct_0(X1)),k3_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0)),u2_altcat_1(X1),u2_altcat_1(X0)) ) )
| ~ l2_altcat_1(X1) )
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f251,plain,
! [X0] :
( ! [X1] :
( ( X1 = k9_waybel34(X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0))) )
& ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( k1_xboole_0 = k1_altcat_1(k5_waybel34(X0),X3,X4)
| ! [X7] :
( ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
<=> v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3)) )
| ~ m1_subset_1(X7,k1_altcat_1(k5_waybel34(X0),X3,X4)) )
| X3 != X5
| X4 != X6
| ~ m1_subset_1(X6,u1_struct_0(X1)) )
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(k5_waybel34(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ) ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ m1_altcat_2(X1,k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f140]) ).
fof(f252,plain,
! [X0] :
( ! [X1] :
( ( X1 = k9_waybel34(X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0))) )
& ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( k1_xboole_0 = k1_altcat_1(k5_waybel34(X0),X3,X4)
| ! [X7] :
( ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
<=> v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3)) )
| ~ m1_subset_1(X7,k1_altcat_1(k5_waybel34(X0),X3,X4)) )
| X3 != X5
| X4 != X6
| ~ m1_subset_1(X6,u1_struct_0(X1)) )
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(k5_waybel34(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ) ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ m1_altcat_2(X1,k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(flattening,[],[f251]) ).
fof(f265,plain,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& l2_altcat_1(k5_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f65]) ).
fof(f268,plain,
! [X0] :
( ( ~ v3_struct_0(k9_waybel34(X0))
& v2_altcat_1(k9_waybel34(X0))
& v6_altcat_1(k9_waybel34(X0))
& v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f67]) ).
fof(f269,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_altcat_1(X0) ),
inference(ennf_transformation,[],[f68]) ).
fof(f271,plain,
! [X0] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f71]) ).
fof(f272,plain,
! [X0] :
( ! [X1] :
( l2_altcat_1(X1)
| ~ m1_altcat_2(X1,X0) )
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f72]) ).
fof(f291,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f96]) ).
fof(f292,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f291]) ).
fof(f324,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f131]) ).
fof(f325,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(flattening,[],[f324]) ).
fof(f327,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f133]) ).
fof(f328,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f327]) ).
fof(f329,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f135]) ).
fof(f330,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f329]) ).
fof(f333,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f138]) ).
fof(f335,plain,
( ~ r2_hidden(u1_struct_0(sK1),sK0)
| ~ v3_lattice3(sK1)
| ~ v1_orders_2(sK1)
| ~ m1_subset_1(sK1,u1_struct_0(k9_waybel34(sK0))) ),
inference(cnf_transformation,[],[f181]) ).
fof(f336,plain,
( r2_hidden(u1_struct_0(sK1),sK0)
| m1_subset_1(sK1,u1_struct_0(k9_waybel34(sK0))) ),
inference(cnf_transformation,[],[f181]) ).
fof(f337,plain,
( v3_lattice3(sK1)
| m1_subset_1(sK1,u1_struct_0(k9_waybel34(sK0))) ),
inference(cnf_transformation,[],[f181]) ).
fof(f338,plain,
( v1_orders_2(sK1)
| m1_subset_1(sK1,u1_struct_0(k9_waybel34(sK0))) ),
inference(cnf_transformation,[],[f181]) ).
fof(f339,plain,
l1_orders_2(sK1),
inference(cnf_transformation,[],[f181]) ).
fof(f340,plain,
v2_lattice3(sK1),
inference(cnf_transformation,[],[f181]) ).
fof(f341,plain,
v1_lattice3(sK1),
inference(cnf_transformation,[],[f181]) ).
fof(f342,plain,
v4_orders_2(sK1),
inference(cnf_transformation,[],[f181]) ).
fof(f343,plain,
v3_orders_2(sK1),
inference(cnf_transformation,[],[f181]) ).
fof(f344,plain,
v2_orders_2(sK1),
inference(cnf_transformation,[],[f181]) ).
fof(f345,plain,
~ v2_setfam_1(sK0),
inference(cnf_transformation,[],[f181]) ).
fof(f403,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f227]) ).
fof(f436,plain,
! [X0,X1] :
( ~ l2_altcat_1(X0)
| ~ l2_altcat_1(X1)
| r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_altcat_2(X1,X0) ),
inference(cnf_transformation,[],[f250]) ).
fof(f458,plain,
! [X2,X0,X1] :
( v2_setfam_1(X0)
| ~ m1_altcat_2(X1,k5_waybel34(X0))
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ v6_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X2,u1_struct_0(X1))
| k9_waybel34(X0) != X1 ),
inference(cnf_transformation,[],[f252]) ).
fof(f478,plain,
! [X0] :
( l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f265]) ).
fof(f488,plain,
! [X0] :
( m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f489,plain,
! [X0] :
( v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f490,plain,
! [X0] :
( v6_altcat_1(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f491,plain,
! [X0] :
( v2_altcat_1(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f492,plain,
! [X0] :
( ~ v3_struct_0(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f493,plain,
! [X0] :
( ~ l1_altcat_1(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f269]) ).
fof(f495,plain,
! [X0] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[],[f271]) ).
fof(f496,plain,
! [X0,X1] :
( l2_altcat_1(X1)
| ~ m1_altcat_2(X1,X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[],[f272]) ).
fof(f511,plain,
! [X0] : m1_subset_1(sK15(X0),X0),
inference(cnf_transformation,[],[f89]) ).
fof(f521,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f292]) ).
fof(f654,plain,
! [X0,X1] :
( v2_setfam_1(X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| r2_hidden(u1_struct_0(X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0))) ),
inference(cnf_transformation,[],[f325]) ).
fof(f655,plain,
! [X0,X1] :
( v3_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v2_setfam_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0))) ),
inference(cnf_transformation,[],[f325]) ).
fof(f656,plain,
! [X0,X1] :
( v1_orders_2(X1)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v2_setfam_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0))) ),
inference(cnf_transformation,[],[f325]) ).
fof(f657,plain,
! [X0,X1] :
( v2_setfam_1(X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ r2_hidden(u1_struct_0(X1),X0)
| ~ v3_lattice3(X1)
| ~ v1_orders_2(X1)
| m1_subset_1(X1,u1_struct_0(k5_waybel34(X0))) ),
inference(cnf_transformation,[],[f325]) ).
fof(f659,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f328]) ).
fof(f660,plain,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f134]) ).
fof(f662,plain,
! [X2,X0,X1] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(cnf_transformation,[],[f330]) ).
fof(f665,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f333]) ).
fof(f667,plain,
! [X2,X0] :
( v2_setfam_1(X0)
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ v6_altcat_1(k9_waybel34(X0))
| ~ v2_altcat_1(k9_waybel34(X0))
| v3_struct_0(k9_waybel34(X0))
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X2,u1_struct_0(k9_waybel34(X0))) ),
inference(equality_resolution,[],[f458]) ).
fof(f675,definition,
( spl36_1
<=> m1_subset_1(sK1,u1_struct_0(k9_waybel34(sK0))) ),
introduced(definition,[new_symbols(definition,[spl36_1])],[avatar_definition]) ).
fof(f676,plain,
( ~ m1_subset_1(sK1,u1_struct_0(k9_waybel34(sK0)))
| spl36_1 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f677,plain,
( m1_subset_1(sK1,u1_struct_0(k9_waybel34(sK0)))
| ~ spl36_1 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f679,definition,
( spl36_2
<=> v3_lattice3(sK1) ),
introduced(definition,[new_symbols(definition,[spl36_2])],[avatar_definition]) ).
fof(f680,plain,
( ~ v3_lattice3(sK1)
| spl36_2 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f681,plain,
( v3_lattice3(sK1)
| ~ spl36_2 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f682,plain,
( spl36_1
| spl36_2 ),
inference(avatar_split_clause,[],[f337,f679,f675]) ).
fof(f684,definition,
( spl36_3
<=> v1_orders_2(sK1) ),
introduced(definition,[new_symbols(definition,[spl36_3])],[avatar_definition]) ).
fof(f685,plain,
( ~ v1_orders_2(sK1)
| spl36_3 ),
inference(avatar_component_clause,[],[f684]) ).
fof(f686,plain,
( v1_orders_2(sK1)
| ~ spl36_3 ),
inference(avatar_component_clause,[],[f684]) ).
fof(f687,plain,
( spl36_1
| spl36_3 ),
inference(avatar_split_clause,[],[f338,f684,f675]) ).
fof(f688,plain,
( ~ r2_hidden(u1_struct_0(sK1),sK0)
| ~ v1_orders_2(sK1)
| ~ m1_subset_1(sK1,u1_struct_0(k9_waybel34(sK0)))
| ~ spl36_2 ),
inference(forward_subsumption_resolution,[],[f335,f681]) ).
fof(f689,plain,
( ~ r2_hidden(u1_struct_0(sK1),sK0)
| ~ v1_orders_2(sK1)
| ~ spl36_1
| ~ spl36_2 ),
inference(forward_subsumption_resolution,[],[f688,f677]) ).
fof(f691,definition,
( spl36_4
<=> r2_hidden(u1_struct_0(sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl36_4])],[avatar_definition]) ).
fof(f692,plain,
( r2_hidden(u1_struct_0(sK1),sK0)
| ~ spl36_4 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f693,plain,
( ~ r2_hidden(u1_struct_0(sK1),sK0)
| spl36_4 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f694,plain,
( ~ spl36_3
| ~ spl36_4
| ~ spl36_1
| ~ spl36_2 ),
inference(avatar_split_clause,[],[f689,f679,f675,f691,f684]) ).
fof(f707,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_altcat_1(X0) ),
inference(resolution,[],[f495,f493]) ).
fof(f853,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1) ),
inference(resolution,[],[f659,f403]) ).
fof(f854,plain,
! [X0,X1] :
( v3_struct_0(X1)
| ~ m1_subset_1(X0,u1_struct_0(X1))
| r2_hidden(X0,u1_struct_0(X1))
| ~ l1_struct_0(X1) ),
inference(resolution,[],[f659,f521]) ).
fof(f901,plain,
! [X0] :
( r2_hidden(X0,sK0)
| ~ m1_subset_1(X0,sK0) ),
inference(resolution,[],[f853,f345]) ).
fof(f909,plain,
! [X0] :
( ~ m1_subset_1(X0,sK0)
| ~ v1_xboole_0(sK0) ),
inference(resolution,[],[f901,f665]) ).
fof(f922,definition,
( spl36_16
<=> v1_xboole_0(sK0) ),
introduced(definition,[new_symbols(definition,[spl36_16])],[avatar_definition]) ).
fof(f924,plain,
( ~ v1_xboole_0(sK0)
| spl36_16 ),
inference(avatar_component_clause,[],[f922]) ).
fof(f926,definition,
( spl36_17
<=> ! [X0] : ~ m1_subset_1(X0,sK0) ),
introduced(definition,[new_symbols(definition,[spl36_17])],[avatar_definition]) ).
fof(f927,plain,
( ! [X0] : ~ m1_subset_1(X0,sK0)
| ~ spl36_17 ),
inference(avatar_component_clause,[],[f926]) ).
fof(f928,plain,
( ~ spl36_16
| spl36_17 ),
inference(avatar_split_clause,[],[f909,f926,f922]) ).
fof(f978,plain,
! [X0,X1] :
( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ~ l2_altcat_1(X0)
| ~ m1_altcat_2(X1,X0) ),
inference(forward_subsumption_resolution,[],[f436,f496]) ).
fof(f1036,plain,
( $false
| ~ spl36_17 ),
inference(resolution,[],[f927,f511]) ).
fof(f1039,plain,
~ spl36_17,
inference(avatar_contradiction_clause,[],[f1036]) ).
fof(f1190,plain,
( ! [X0] :
( ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| v2_setfam_1(X0)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0))) )
| spl36_3 ),
inference(resolution,[],[f656,f685]) ).
fof(f1193,plain,
( ! [X0] :
( ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| v2_setfam_1(X0)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0))) )
| spl36_3 ),
inference(forward_subsumption_resolution,[],[f1190,f339]) ).
fof(f1194,plain,
( ! [X0] :
( ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| v2_setfam_1(X0)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0))) )
| spl36_3 ),
inference(forward_subsumption_resolution,[],[f1193,f340]) ).
fof(f1195,plain,
( ! [X0] :
( ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| v2_setfam_1(X0)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0))) )
| spl36_3 ),
inference(forward_subsumption_resolution,[],[f1194,f341]) ).
fof(f1196,plain,
( ! [X0] :
( ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| v2_setfam_1(X0)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0))) )
| spl36_3 ),
inference(forward_subsumption_resolution,[],[f1195,f342]) ).
fof(f1197,plain,
( ! [X0] :
( ~ v2_orders_2(sK1)
| v2_setfam_1(X0)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0))) )
| spl36_3 ),
inference(forward_subsumption_resolution,[],[f1196,f343]) ).
fof(f1198,plain,
( ! [X0] :
( ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0)))
| v2_setfam_1(X0) )
| spl36_3 ),
inference(forward_subsumption_resolution,[],[f1197,f344]) ).
fof(f1199,plain,
( ! [X0,X1] :
( v2_setfam_1(X0)
| ~ r2_hidden(sK1,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k5_waybel34(X0)))) )
| spl36_3 ),
inference(resolution,[],[f1198,f662]) ).
fof(f1243,plain,
! [X0] :
( r2_hidden(u1_struct_0(X0),sK0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(sK0))) ),
inference(resolution,[],[f654,f345]) ).
fof(f1245,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k5_waybel34(sK0))))
| ~ r2_hidden(sK1,X0) )
| spl36_3 ),
inference(resolution,[],[f1199,f345]) ).
fof(f1247,plain,
( ! [X0] :
( ~ r1_tarski(X0,u1_struct_0(k5_waybel34(sK0)))
| ~ r2_hidden(sK1,X0) )
| spl36_3 ),
inference(resolution,[],[f1245,f660]) ).
fof(f1253,plain,
( ! [X0] :
( ~ r2_hidden(sK1,u1_struct_0(X0))
| ~ l2_altcat_1(k5_waybel34(sK0))
| ~ m1_altcat_2(X0,k5_waybel34(sK0)) )
| spl36_3 ),
inference(resolution,[],[f1247,f978]) ).
fof(f1340,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(k5_waybel34(sK0)))
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[],[f657,f345]) ).
fof(f1343,definition,
( spl36_45
<=> l2_altcat_1(k5_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl36_45])],[avatar_definition]) ).
fof(f1344,plain,
( l2_altcat_1(k5_waybel34(sK0))
| ~ spl36_45 ),
inference(avatar_component_clause,[],[f1343]) ).
fof(f1345,plain,
( ~ l2_altcat_1(k5_waybel34(sK0))
| spl36_45 ),
inference(avatar_component_clause,[],[f1343]) ).
fof(f1347,definition,
( spl36_46
<=> ! [X0] :
( ~ r2_hidden(sK1,u1_struct_0(X0))
| ~ m1_altcat_2(X0,k5_waybel34(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl36_46])],[avatar_definition]) ).
fof(f1348,plain,
( ! [X0] :
( ~ r2_hidden(sK1,u1_struct_0(X0))
| ~ m1_altcat_2(X0,k5_waybel34(sK0)) )
| ~ spl36_46 ),
inference(avatar_component_clause,[],[f1347]) ).
fof(f1349,plain,
( ~ spl36_45
| spl36_46
| spl36_3 ),
inference(avatar_split_clause,[],[f1253,f684,f1347,f1343]) ).
fof(f1351,plain,
( v1_xboole_0(sK0)
| spl36_45 ),
inference(resolution,[],[f1345,f478]) ).
fof(f1353,plain,
( $false
| spl36_16
| spl36_45 ),
inference(forward_subsumption_resolution,[],[f1351,f924]) ).
fof(f1354,plain,
( spl36_16
| spl36_45 ),
inference(avatar_contradiction_clause,[],[f1353]) ).
fof(f1384,plain,
! [X2,X0] :
( v2_setfam_1(X0)
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ v6_altcat_1(k9_waybel34(X0))
| ~ v2_altcat_1(k9_waybel34(X0))
| v3_struct_0(k9_waybel34(X0))
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X2,u1_struct_0(k9_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f667,f489]) ).
fof(f1385,plain,
! [X2,X0] :
( v2_setfam_1(X0)
| ~ v6_altcat_1(k9_waybel34(X0))
| ~ v2_altcat_1(k9_waybel34(X0))
| v3_struct_0(k9_waybel34(X0))
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X2,u1_struct_0(k9_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f1384,f488]) ).
fof(f1386,plain,
! [X2,X0] :
( v2_setfam_1(X0)
| ~ v2_altcat_1(k9_waybel34(X0))
| v3_struct_0(k9_waybel34(X0))
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X2,u1_struct_0(k9_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f1385,f490]) ).
fof(f1387,plain,
! [X2,X0] :
( v2_setfam_1(X0)
| v3_struct_0(k9_waybel34(X0))
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X2,u1_struct_0(k9_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f1386,f491]) ).
fof(f1388,plain,
! [X2,X0] :
( v2_setfam_1(X0)
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X2,u1_struct_0(k9_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f1387,f492]) ).
fof(f1398,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(k9_waybel34(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(sK0))) ),
inference(resolution,[],[f1388,f345]) ).
fof(f1735,plain,
( ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK1)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(sK0)))
| spl36_4 ),
inference(resolution,[],[f1243,f693]) ).
fof(f1755,plain,
( ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK1)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(sK0)))
| spl36_4 ),
inference(forward_subsumption_resolution,[],[f1735,f340]) ).
fof(f1759,plain,
( ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK1)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(sK0)))
| spl36_4 ),
inference(forward_subsumption_resolution,[],[f1755,f341]) ).
fof(f1763,plain,
( ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK1)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(sK0)))
| spl36_4 ),
inference(forward_subsumption_resolution,[],[f1759,f342]) ).
fof(f1767,plain,
( ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK1)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(sK0)))
| spl36_4 ),
inference(forward_subsumption_resolution,[],[f1763,f343]) ).
fof(f1771,plain,
( ~ l1_orders_2(sK1)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(sK0)))
| spl36_4 ),
inference(forward_subsumption_resolution,[],[f1767,f344]) ).
fof(f1775,plain,
( ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(sK0)))
| spl36_4 ),
inference(forward_subsumption_resolution,[],[f1771,f339]) ).
fof(f1955,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k5_waybel34(sK0))))
| ~ r2_hidden(sK1,X0) )
| spl36_4 ),
inference(resolution,[],[f1775,f662]) ).
fof(f4026,definition,
( spl36_149
<=> l2_altcat_1(k9_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl36_149])],[avatar_definition]) ).
fof(f4028,plain,
( ~ l2_altcat_1(k9_waybel34(sK0))
| spl36_149 ),
inference(avatar_component_clause,[],[f4026]) ).
fof(f4179,definition,
( spl36_156
<=> v3_struct_0(k9_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl36_156])],[avatar_definition]) ).
fof(f4180,plain,
( ~ v3_struct_0(k9_waybel34(sK0))
| spl36_156 ),
inference(avatar_component_clause,[],[f4179]) ).
fof(f4181,plain,
( v3_struct_0(k9_waybel34(sK0))
| ~ spl36_156 ),
inference(avatar_component_clause,[],[f4179]) ).
fof(f4200,plain,
( v2_setfam_1(sK0)
| ~ spl36_156 ),
inference(resolution,[],[f4181,f492]) ).
fof(f4201,plain,
( $false
| ~ spl36_156 ),
inference(forward_subsumption_resolution,[],[f4200,f345]) ).
fof(f4202,plain,
~ spl36_156,
inference(avatar_contradiction_clause,[],[f4201]) ).
fof(f4207,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k9_waybel34(sK0)))
| r2_hidden(X0,u1_struct_0(k9_waybel34(sK0)))
| ~ l1_struct_0(k9_waybel34(sK0)) )
| spl36_156 ),
inference(resolution,[],[f4180,f854]) ).
fof(f14553,plain,
( ! [X0] :
( ~ r1_tarski(X0,u1_struct_0(k5_waybel34(sK0)))
| ~ r2_hidden(sK1,X0) )
| spl36_4 ),
inference(resolution,[],[f1955,f660]) ).
fof(f14575,plain,
( ! [X0] :
( ~ r2_hidden(sK1,u1_struct_0(X0))
| ~ l2_altcat_1(k5_waybel34(sK0))
| ~ m1_altcat_2(X0,k5_waybel34(sK0)) )
| spl36_4 ),
inference(resolution,[],[f14553,f978]) ).
fof(f17751,definition,
( spl36_405
<=> l1_struct_0(k9_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl36_405])],[avatar_definition]) ).
fof(f17753,plain,
( ~ l1_struct_0(k9_waybel34(sK0))
| spl36_405 ),
inference(avatar_component_clause,[],[f17751]) ).
fof(f17755,definition,
( spl36_406
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k9_waybel34(sK0)))
| r2_hidden(X0,u1_struct_0(k9_waybel34(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl36_406])],[avatar_definition]) ).
fof(f17756,plain,
( ! [X0] :
( r2_hidden(X0,u1_struct_0(k9_waybel34(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k9_waybel34(sK0))) )
| ~ spl36_406 ),
inference(avatar_component_clause,[],[f17755]) ).
fof(f17757,plain,
( ~ spl36_405
| spl36_406
| spl36_156 ),
inference(avatar_split_clause,[],[f4207,f4179,f17755,f17751]) ).
fof(f17758,plain,
( ~ l2_altcat_1(k9_waybel34(sK0))
| spl36_405 ),
inference(resolution,[],[f17753,f707]) ).
fof(f17760,plain,
( ~ spl36_149
| spl36_405 ),
inference(avatar_split_clause,[],[f17758,f17751,f4026]) ).
fof(f17761,plain,
( ! [X0] :
( ~ m1_altcat_2(k9_waybel34(sK0),X0)
| ~ l2_altcat_1(X0) )
| spl36_149 ),
inference(resolution,[],[f4028,f496]) ).
fof(f17762,plain,
( ~ l2_altcat_1(k5_waybel34(sK0))
| v2_setfam_1(sK0)
| spl36_149 ),
inference(resolution,[],[f17761,f488]) ).
fof(f17767,plain,
( v2_setfam_1(sK0)
| ~ spl36_45
| spl36_149 ),
inference(forward_subsumption_resolution,[],[f17762,f1344]) ).
fof(f17768,plain,
( $false
| ~ spl36_45
| spl36_149 ),
inference(forward_subsumption_resolution,[],[f17767,f345]) ).
fof(f17769,plain,
( ~ spl36_45
| spl36_149 ),
inference(avatar_contradiction_clause,[],[f17768]) ).
fof(f17837,plain,
( ~ m1_subset_1(sK1,u1_struct_0(k9_waybel34(sK0)))
| ~ m1_altcat_2(k9_waybel34(sK0),k5_waybel34(sK0))
| ~ spl36_46
| ~ spl36_406 ),
inference(resolution,[],[f17756,f1348]) ).
fof(f17873,plain,
( ~ m1_altcat_2(k9_waybel34(sK0),k5_waybel34(sK0))
| ~ spl36_1
| ~ spl36_46
| ~ spl36_406 ),
inference(forward_subsumption_resolution,[],[f17837,f677]) ).
fof(f17877,plain,
( v2_setfam_1(sK0)
| ~ spl36_1
| ~ spl36_46
| ~ spl36_406 ),
inference(resolution,[],[f17873,f488]) ).
fof(f17882,plain,
( $false
| ~ spl36_1
| ~ spl36_46
| ~ spl36_406 ),
inference(forward_subsumption_resolution,[],[f17877,f345]) ).
fof(f17883,plain,
( ~ spl36_1
| ~ spl36_46
| ~ spl36_406 ),
inference(avatar_contradiction_clause,[],[f17882]) ).
fof(f17886,plain,
( ! [X0] :
( ~ r2_hidden(sK1,u1_struct_0(X0))
| ~ m1_altcat_2(X0,k5_waybel34(sK0)) )
| spl36_4
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f14575,f1344]) ).
fof(f18510,plain,
( spl36_46
| spl36_4
| ~ spl36_45 ),
inference(avatar_split_clause,[],[f17886,f1343,f691,f1347]) ).
fof(f18560,plain,
( ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(sK0)))
| spl36_1 ),
inference(resolution,[],[f676,f1398]) ).
fof(f18579,plain,
( ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ r2_hidden(u1_struct_0(sK1),sK0)
| ~ v3_lattice3(sK1)
| ~ v1_orders_2(sK1)
| ~ l1_orders_2(sK1)
| spl36_1 ),
inference(resolution,[],[f18560,f1340]) ).
fof(f18581,plain,
( ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ r2_hidden(u1_struct_0(sK1),sK0)
| ~ v3_lattice3(sK1)
| ~ v1_orders_2(sK1)
| ~ l1_orders_2(sK1)
| spl36_1 ),
inference(forward_subsumption_resolution,[],[f18579,f340]) ).
fof(f18582,plain,
( ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ r2_hidden(u1_struct_0(sK1),sK0)
| ~ v3_lattice3(sK1)
| ~ v1_orders_2(sK1)
| ~ l1_orders_2(sK1)
| spl36_1 ),
inference(forward_subsumption_resolution,[],[f18581,f341]) ).
fof(f18583,plain,
( ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ r2_hidden(u1_struct_0(sK1),sK0)
| ~ v3_lattice3(sK1)
| ~ v1_orders_2(sK1)
| ~ l1_orders_2(sK1)
| spl36_1 ),
inference(forward_subsumption_resolution,[],[f18582,f342]) ).
fof(f18584,plain,
( ~ v2_orders_2(sK1)
| ~ r2_hidden(u1_struct_0(sK1),sK0)
| ~ v3_lattice3(sK1)
| ~ v1_orders_2(sK1)
| ~ l1_orders_2(sK1)
| spl36_1 ),
inference(forward_subsumption_resolution,[],[f18583,f343]) ).
fof(f18585,plain,
( ~ r2_hidden(u1_struct_0(sK1),sK0)
| ~ v3_lattice3(sK1)
| ~ v1_orders_2(sK1)
| ~ l1_orders_2(sK1)
| spl36_1 ),
inference(forward_subsumption_resolution,[],[f18584,f344]) ).
fof(f18586,plain,
( ~ v3_lattice3(sK1)
| ~ v1_orders_2(sK1)
| ~ l1_orders_2(sK1)
| spl36_1
| ~ spl36_4 ),
inference(forward_subsumption_resolution,[],[f18585,f692]) ).
fof(f18587,plain,
( ~ v1_orders_2(sK1)
| ~ l1_orders_2(sK1)
| spl36_1
| ~ spl36_2
| ~ spl36_4 ),
inference(forward_subsumption_resolution,[],[f18586,f681]) ).
fof(f18588,plain,
( ~ l1_orders_2(sK1)
| spl36_1
| ~ spl36_2
| ~ spl36_3
| ~ spl36_4 ),
inference(forward_subsumption_resolution,[],[f18587,f686]) ).
fof(f18589,plain,
( $false
| spl36_1
| ~ spl36_2
| ~ spl36_3
| ~ spl36_4 ),
inference(forward_subsumption_resolution,[],[f18588,f339]) ).
fof(f18590,plain,
( spl36_1
| ~ spl36_2
| ~ spl36_3
| ~ spl36_4 ),
inference(avatar_contradiction_clause,[],[f18589]) ).
fof(f18591,plain,
( r2_hidden(u1_struct_0(sK1),sK0)
| spl36_1 ),
inference(forward_subsumption_resolution,[],[f336,f676]) ).
fof(f18599,plain,
( $false
| spl36_1
| spl36_4 ),
inference(forward_subsumption_resolution,[],[f18591,f693]) ).
fof(f18600,plain,
( spl36_1
| spl36_4 ),
inference(avatar_contradiction_clause,[],[f18599]) ).
fof(f18604,plain,
( ! [X0] :
( ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| v2_setfam_1(X0)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0))) )
| spl36_2 ),
inference(resolution,[],[f680,f655]) ).
fof(f18605,plain,
( ! [X0] :
( ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| v2_setfam_1(X0)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0))) )
| spl36_2 ),
inference(forward_subsumption_resolution,[],[f18604,f339]) ).
fof(f18606,plain,
( ! [X0] :
( ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| v2_setfam_1(X0)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0))) )
| spl36_2 ),
inference(forward_subsumption_resolution,[],[f18605,f340]) ).
fof(f18607,plain,
( ! [X0] :
( ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| v2_setfam_1(X0)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0))) )
| spl36_2 ),
inference(forward_subsumption_resolution,[],[f18606,f341]) ).
fof(f18608,plain,
( ! [X0] :
( ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| v2_setfam_1(X0)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0))) )
| spl36_2 ),
inference(forward_subsumption_resolution,[],[f18607,f342]) ).
fof(f18609,plain,
( ! [X0] :
( ~ v2_orders_2(sK1)
| v2_setfam_1(X0)
| ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0))) )
| spl36_2 ),
inference(forward_subsumption_resolution,[],[f18608,f343]) ).
fof(f18610,plain,
( ! [X0] :
( ~ m1_subset_1(sK1,u1_struct_0(k5_waybel34(X0)))
| v2_setfam_1(X0) )
| spl36_2 ),
inference(forward_subsumption_resolution,[],[f18609,f344]) ).
fof(f18639,plain,
( ! [X0,X1] :
( v2_setfam_1(X0)
| ~ r2_hidden(sK1,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k5_waybel34(X0)))) )
| spl36_2 ),
inference(resolution,[],[f18610,f662]) ).
fof(f18649,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k5_waybel34(sK0))))
| ~ r2_hidden(sK1,X0) )
| spl36_2 ),
inference(resolution,[],[f18639,f345]) ).
fof(f18663,plain,
( ! [X0] :
( ~ r1_tarski(X0,u1_struct_0(k5_waybel34(sK0)))
| ~ r2_hidden(sK1,X0) )
| spl36_2 ),
inference(resolution,[],[f18649,f660]) ).
fof(f18700,plain,
( ! [X0] :
( ~ r2_hidden(sK1,u1_struct_0(X0))
| ~ l2_altcat_1(k5_waybel34(sK0))
| ~ m1_altcat_2(X0,k5_waybel34(sK0)) )
| spl36_2 ),
inference(resolution,[],[f18663,f978]) ).
fof(f18711,plain,
( ! [X0] :
( ~ r2_hidden(sK1,u1_struct_0(X0))
| ~ m1_altcat_2(X0,k5_waybel34(sK0)) )
| spl36_2
| ~ spl36_45 ),
inference(forward_subsumption_resolution,[],[f18700,f1344]) ).
fof(f18772,plain,
( spl36_46
| spl36_2
| ~ spl36_45 ),
inference(avatar_split_clause,[],[f18711,f1343,f679,f1347]) ).
cnf(s1,plain,
( spl36_1
| spl36_2 ),
inference(sat_conversion,[],[f682]) ).
cnf(s2,plain,
( spl36_1
| spl36_3 ),
inference(sat_conversion,[],[f687]) ).
cnf(s3,plain,
( ~ spl36_1
| ~ spl36_2
| ~ spl36_3
| ~ spl36_4 ),
inference(sat_conversion,[],[f694]) ).
cnf(s8,plain,
( ~ spl36_16
| spl36_17 ),
inference(sat_conversion,[],[f928]) ).
cnf(s14,plain,
~ spl36_17,
inference(sat_conversion,[],[f1039]) ).
cnf(s29,plain,
( spl36_3
| ~ spl36_45
| spl36_46 ),
inference(sat_conversion,[],[f1349]) ).
cnf(s30,plain,
( spl36_16
| spl36_45 ),
inference(sat_conversion,[],[f1354]) ).
cnf(s78,plain,
~ spl36_156,
inference(sat_conversion,[],[f4202]) ).
cnf(s240,plain,
( spl36_156
| ~ spl36_405
| spl36_406 ),
inference(sat_conversion,[],[f17757]) ).
cnf(s241,plain,
( ~ spl36_149
| spl36_405 ),
inference(sat_conversion,[],[f17760]) ).
cnf(s242,plain,
( ~ spl36_45
| spl36_149 ),
inference(sat_conversion,[],[f17769]) ).
cnf(s243,plain,
( ~ spl36_1
| ~ spl36_46
| ~ spl36_406 ),
inference(sat_conversion,[],[f17883]) ).
cnf(s251,plain,
( spl36_4
| ~ spl36_45
| spl36_46 ),
inference(sat_conversion,[],[f18510]) ).
cnf(s254,plain,
( spl36_1
| ~ spl36_2
| ~ spl36_3
| ~ spl36_4 ),
inference(sat_conversion,[],[f18590]) ).
cnf(s255,plain,
( spl36_1
| spl36_4 ),
inference(sat_conversion,[],[f18600]) ).
cnf(s268,plain,
( spl36_2
| ~ spl36_45
| spl36_46 ),
inference(sat_conversion,[],[f18772]) ).
cnf(s318,plain,
~ spl36_16,
inference(rat,[],[s8,s14]) ).
cnf(s319,plain,
spl36_45,
inference(rat,[],[s30,s318]) ).
cnf(s321,plain,
spl36_149,
inference(rat,[],[s242,s319]) ).
cnf(s322,plain,
spl36_405,
inference(rat,[],[s241,s321]) ).
cnf(s323,plain,
spl36_406,
inference(rat,[],[s240,s78,s322]) ).
cnf(s324,plain,
spl36_1,
inference(rat,[],[s254,s1,s2,s255]) ).
cnf(s325,plain,
~ spl36_46,
inference(rat,[],[s243,s323,s324]) ).
cnf(s326,plain,
spl36_2,
inference(rat,[],[s268,s319,s325]) ).
cnf(s327,plain,
spl36_4,
inference(rat,[],[s251,s319,s325]) ).
cnf(s328,plain,
spl36_3,
inference(rat,[],[s29,s319,s325]) ).
cnf(s329,plain,
$false,
inference(rat,[],[s3,s327,s324,s326,s328]) ).
fof(f18773,plain,
$false,
inference(avatar_sat_refutation,[],[s329]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT374+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.15/0.41 % Computer : n003.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sun Sep 27 15:10:26 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.15/0.47 Running first-order model finding
% 0.15/0.47 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.37/3.00 % (672495)Will run a generic schedule for satisfiability detection.
% 15.37/3.00 % (672501)% WARNING: option uhcvi not known.
% 15.37/3.00 % (672501)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3246673372:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.37/3.00 % (672500)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1033130484_2999 on theBenchmark for (2999ds/0Mi)
% 15.37/3.00 % (672503)dis+10_1_sil=32000:sp=arity:random_seed=3237005653:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.37/3.00 % (672506)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3143065090:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.37/3.00 % (672502)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3500065895:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.37/3.00 % (672504)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4294665336:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.37/3.00 % (672505)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1545407536:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.37/3.00 % TRYING [1]
% 15.37/3.00 % TRYING [2]
% 15.37/3.00 % TRYING [3]
% 15.37/3.00 % (672504)Instruction limit reached!
% 15.37/3.00 % (672504)------------------------------
% 15.37/3.00 % (672504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/3.00 % (672504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/3.00 % (672504)CaDiCaL version: 2.1.3
% 15.37/3.00 % (672504)Termination reason: Instruction limit
% 15.37/3.00 % (672504)Termination phase: Saturation
% 15.37/3.00 % (672504)Time elapsed: 0.103 s
% 15.37/3.00 % (672504)Peak memory usage: 13 MB
% 15.37/3.00 % (672504)Instructions burned: 117 (million)
% 15.37/3.00 % (672503)Instruction limit reached!
% 15.37/3.00 % (672503)------------------------------
% 15.37/3.00 % (672503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/3.00 % (672503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/3.00 % (672503)CaDiCaL version: 2.1.3
% 15.37/3.00 % (672503)Termination reason: Instruction limit
% 15.37/3.00 % (672503)Termination phase: Saturation
% 15.37/3.00 % (672503)Time elapsed: 0.107 s
% 15.37/3.00 % (672503)Peak memory usage: 13 MB
% 15.37/3.00 % (672503)Instructions burned: 103 (million)
% 15.37/3.00 % (672505)Instruction limit reached!
% 15.37/3.00 % (672505)------------------------------
% 15.37/3.00 % (672505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/3.00 % (672505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/3.00 % (672505)CaDiCaL version: 2.1.3
% 15.37/3.00 % (672505)Termination reason: Instruction limit
% 15.37/3.00 % (672505)Termination phase: Saturation
% 15.37/3.00 % (672505)Time elapsed: 0.125 s
% 15.37/3.00 % (672505)Peak memory usage: 14 MB
% 15.37/3.00 % (672505)Instructions burned: 131 (million)
% 15.37/3.00 % TRYING [4]
% 15.37/3.00 % (672515)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1485029302:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 15.37/3.00 % (672516)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=126812090:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.37/3.00 % (672506)Instruction limit reached!
% 15.37/3.00 % (672506)------------------------------
% 15.37/3.00 % (672506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/3.00 % (672506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.37/3.00 % (672506)CaDiCaL version: 2.1.3
% 15.37/3.00 % (672506)Termination reason: Instruction limit
% 15.37/3.00 % (672506)Termination phase: Saturation
% 15.37/3.00 % (672506)Time elapsed: 0.146 s
% 15.37/3.00 % (672506)Peak memory usage: 13 MB
% 15.37/3.00 % (672506)Instructions burned: 159 (million)
% 15.37/3.00 % (672517)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=2127786942:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.37/3.00 % (672520)ott-21_1_sil=16000:fs=off:random_seed=2581882162:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.37/3.00 % TRYING [1]
% 15.37/3.00 % TRYING [2]
% 15.37/3.00 % TRYING [3]
% 15.37/3.00 % (672516)Instruction limit reached!
% 15.37/3.00 % (672516)------------------------------
% 15.37/3.00 % (672516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.37/3.00 % (672516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672516)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672516)Termination reason: Instruction limit
% 12.94/3.33 % (672516)Termination phase: Saturation
% 12.94/3.33 % (672516)Time elapsed: 0.139 s
% 12.94/3.33 % (672516)Peak memory usage: 14 MB
% 12.94/3.33 % (672516)Instructions burned: 131 (million)
% 12.94/3.33 % (672523)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1440430980:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 12.94/3.33 % TRYING [4]
% 12.94/3.33 % (672520)Instruction limit reached!
% 12.94/3.33 % (672520)------------------------------
% 12.94/3.33 % (672520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672520)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672520)Termination reason: Instruction limit
% 12.94/3.33 % (672520)Termination phase: Saturation
% 12.94/3.33 % (672520)Time elapsed: 0.182 s
% 12.94/3.33 % (672520)Peak memory usage: 12 MB
% 12.94/3.33 % (672520)Instructions burned: 180 (million)
% 12.94/3.33 % (672525)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2697251947:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 12.94/3.33 % TRYING [1]
% 12.94/3.33 % TRYING [2]
% 12.94/3.33 % TRYING [3]
% 12.94/3.33 % (672515)Instruction limit reached!
% 12.94/3.33 % (672515)------------------------------
% 12.94/3.33 % (672515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672515)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672515)Termination reason: Instruction limit
% 12.94/3.33 % (672515)Termination phase: Finite model building constraint generation
% 12.94/3.33 % (672515)Time elapsed: 0.511 s
% 12.94/3.33 % (672515)Peak memory usage: 37 MB
% 12.94/3.33 % (672515)Instructions burned: 714 (million)
% 12.94/3.33 % (672527)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2471066121:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 12.94/3.33 % (672517)Instruction limit reached!
% 12.94/3.33 % (672517)------------------------------
% 12.94/3.33 % (672517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672517)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672517)Termination reason: Instruction limit
% 12.94/3.33 % (672517)Termination phase: Saturation
% 12.94/3.33 % (672517)Time elapsed: 0.668 s
% 12.94/3.33 % (672517)Peak memory usage: 23 MB
% 12.94/3.33 % (672517)Instructions burned: 684 (million)
% 12.94/3.33 % TRYING [5]
% 12.94/3.33 % (672529)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2974681057:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 12.94/3.33 % (672523)Instruction limit reached!
% 12.94/3.33 % (672523)------------------------------
% 12.94/3.33 % (672523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672523)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672523)Termination reason: Instruction limit
% 12.94/3.33 % (672523)Termination phase: Saturation
% 12.94/3.33 % (672523)Time elapsed: 0.538 s
% 12.94/3.33 % (672523)Peak memory usage: 15 MB
% 12.94/3.33 % (672523)Instructions burned: 477 (million)
% 12.94/3.33 % (672531)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=1664128147:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi)
% 12.94/3.33 % TRYING [4]
% 12.94/3.33 % (672525)Instruction limit reached!
% 12.94/3.33 % (672525)------------------------------
% 12.94/3.33 % (672525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672525)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672525)Termination reason: Instruction limit
% 12.94/3.33 % (672525)Termination phase: Finite model building constraint generation
% 12.94/3.33 % (672525)Time elapsed: 0.626 s
% 12.94/3.33 % (672525)Peak memory usage: 25 MB
% 12.94/3.33 % (672525)Instructions burned: 866 (million)
% 12.94/3.33 % (672533)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3127654648:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 12.94/3.33 % (672531)Instruction limit reached!
% 12.94/3.33 % (672531)------------------------------
% 12.94/3.33 % (672531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672531)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672531)Termination reason: Instruction limit
% 12.94/3.33 % (672531)Termination phase: Saturation
% 12.94/3.33 % (672531)Time elapsed: 0.655 s
% 12.94/3.33 % (672531)Peak memory usage: 24 MB
% 12.94/3.33 % (672531)Instructions burned: 693 (million)
% 12.94/3.33 % (672535)fmb+10_1_sil=64000:random_seed=1319571570:i=22061:nm=2:gsp=on_2983 on theBenchmark for (2983ds/22061Mi)
% 12.94/3.33 % TRYING [1]
% 12.94/3.33 % TRYING [2]
% 12.94/3.33 % (672529)Instruction limit reached!
% 12.94/3.33 % (672529)------------------------------
% 12.94/3.33 % (672529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672529)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672529)Termination reason: Instruction limit
% 12.94/3.33 % (672529)Termination phase: Finite model building constraint generation
% 12.94/3.33 % (672529)Time elapsed: 0.821 s
% 12.94/3.33 % (672529)Peak memory usage: 106 MB
% 12.94/3.33 % (672529)Instructions burned: 890 (million)
% 12.94/3.33 % (672527)Instruction limit reached!
% 12.94/3.33 % (672527)------------------------------
% 12.94/3.33 % (672527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672527)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672527)Termination reason: Instruction limit
% 12.94/3.33 % (672527)Termination phase: Saturation
% 12.94/3.33 % (672527)Time elapsed: 0.990 s
% 12.94/3.33 % (672527)Peak memory usage: 20 MB
% 12.94/3.33 % (672527)Instructions burned: 1180 (million)
% 12.94/3.33 % (672537)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=27513511:i=9515:nm=5_2982 on theBenchmark for (2982ds/9515Mi)
% 12.94/3.33 % (672538)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2608147702:fmbsr=1.7:i=920_2982 on theBenchmark for (2982ds/920Mi)
% 12.94/3.33 % (672537)Cannot represent all propositional literals internally
% 12.94/3.33 % (672537)Refutation not found, incomplete strategy
% 12.94/3.33 % (672537)------------------------------
% 12.94/3.33 % (672537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672537)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672537)Termination reason: Refutation not found, incomplete strategy
% 12.94/3.33 % (672537)Time elapsed: 0.029 s
% 12.94/3.33 % (672537)Peak memory usage: 11 MB
% 12.94/3.33 % (672537)Instructions burned: 45 (million)
% 12.94/3.33 % (672537)------------------------------
% 12.94/3.33 % (672537)------------------------------
% 12.94/3.33 % TRYING [3]
% 12.94/3.33 % TRYING [8]
% 12.94/3.33 % (672541)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2503716530:i=5131_2982 on theBenchmark for (2982ds/5131Mi)
% 12.94/3.33 % (672533)Instruction limit reached!
% 12.94/3.33 % (672533)------------------------------
% 12.94/3.33 % (672533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672533)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672533)Termination reason: Instruction limit
% 12.94/3.33 % (672533)Termination phase: Saturation
% 12.94/3.33 % (672533)Time elapsed: 0.813 s
% 12.94/3.33 % (672533)Peak memory usage: 20 MB
% 12.94/3.33 % (672533)Instructions burned: 879 (million)
% 12.94/3.33 % (672543)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4034160287:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi)
% 12.94/3.33 % TRYING [4]
% 12.94/3.33 % (672538)Instruction limit reached!
% 12.94/3.33 % (672538)------------------------------
% 12.94/3.33 % (672538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672538)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672538)Termination reason: Instruction limit
% 12.94/3.33 % (672538)Termination phase: Finite model building constraint generation
% 12.94/3.33 % (672538)Time elapsed: 0.617 s
% 12.94/3.33 % (672538)Peak memory usage: 61 MB
% 12.94/3.33 % (672538)Instructions burned: 921 (million)
% 12.94/3.33 % (672545)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2186731872:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 12.94/3.33 % (672545)Cannot represent all propositional literals internally
% 12.94/3.33 % (672545)Refutation not found, incomplete strategy
% 12.94/3.33 % (672545)------------------------------
% 12.94/3.33 % (672545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672545)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672545)Termination reason: Refutation not found, incomplete strategy
% 12.94/3.33 % (672545)Time elapsed: 0.056 s
% 12.94/3.33 % (672545)Peak memory usage: 12 MB
% 12.94/3.33 % (672545)Instructions burned: 56 (million)
% 12.94/3.33 % (672545)------------------------------
% 12.94/3.33 % (672545)------------------------------
% 12.94/3.33 % (672547)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2711020730:fmbsr=2.30978:i=2174_2974 on theBenchmark for (2974ds/2174Mi)
% 12.94/3.33 % (672541) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-672495-672541"...
% 12.94/3.33 % (672541)...printing done.
% 12.94/3.33 % (672541)Refutation found. Thanks to Tanya!
% 12.94/3.33 % SZS status Theorem for theBenchmark
% 12.94/3.33 % SZS output start Proof for theBenchmark
% See solution above
% 12.94/3.33 % (672541)------------------------------
% 12.94/3.33 % (672541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.94/3.33 % (672541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/3.33 % (672541)CaDiCaL version: 2.1.3
% 12.94/3.33 % (672541)Termination reason: Refutation
% 12.94/3.33 % (672541)Time elapsed: 0.967 s
% 12.94/3.33 % (672541)Peak memory usage: 20 MB
% 12.94/3.33 % (672541)Instructions burned: 1023 (million)
% 12.94/3.33 % (672495)Success in time 2.843 s
% 12.94/3.33 % Vampire exiting
%------------------------------------------------------------------------------