%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : TOP041+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 02:34:27 PM UTC 2026
% Result : Theorem 30.37s 6.71s
% Output : Refutation 30.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 23
% Syntax : Number of formulae : 204 ( 47 unt; 6 def)
% Number of atoms : 974 ( 118 equ)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 1302 ( 532 ~; 580 |; 141 &)
% ( 15 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 1 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 7 con; 0-4 aty)
% Number of variables : 272 ( 250 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v3_pre_topc(X2,X0)
=> v3_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t34_tsp_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v3_pre_topc(X2,X0)
=> v3_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f50,axiom,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f52,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> ( X3 = u1_struct_0(X1)
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
=> k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d12_tsp_2) ).
fof(f53,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( l1_pre_topc(X1)
=> ( m1_tsp_1(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ( v3_pre_topc(X2,X1)
<=> ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X3,X0)
& X2 = k3_xboole_0(X3,u1_struct_0(X1)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_tsp_1) ).
fof(f54,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m1_pre_topc(X1,X0) )
=> ( v1_funct_1(k1_tsp_2(X0,X1))
& v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_tsp_2) ).
fof(f60,axiom,
! [X0,X1,X2,X3] :
( ( l1_struct_0(X0)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_pre_topc) ).
fof(f61,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m1_pre_topc(X1,X0) )
=> ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_tsp_2) ).
fof(f64,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f69,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m1_tsp_1(X1,X0)
=> l1_pre_topc(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_tsp_1) ).
fof(f71,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> l1_pre_topc(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_tsp_1) ).
fof(f110,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m1_pre_topc(X1,X0) )
=> k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_tsp_2) ).
fof(f111,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k5_subset_1) ).
fof(f112,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m1_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m1_tsp_1) ).
fof(f113,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f114,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
fof(f117,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m1_pre_topc(X1,X0)
=> m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_tsep_1) ).
fof(f122,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v3_pre_topc(X1,X0)
=> k3_tex_4(X0,X1) = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t58_tex_4) ).
fof(f157,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ v3_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1)
& v3_pre_topc(X2,X0)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f158,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ v3_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1)
& v3_pre_topc(X2,X0)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f157]) ).
fof(f222,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( ! [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f52]) ).
fof(f223,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( ! [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f222]) ).
fof(f224,plain,
! [X0] :
( ! [X1] :
( ( m1_tsp_1(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& ! [X2] :
( ( v3_pre_topc(X2,X1)
<=> ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X3,X0)
& X2 = k3_xboole_0(X3,u1_struct_0(X1)) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ) ) )
| ~ l1_pre_topc(X1) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f53]) ).
fof(f225,plain,
! [X0,X1] :
( ( v1_funct_1(k1_tsp_2(X0,X1))
& v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(ennf_transformation,[],[f54]) ).
fof(f226,plain,
! [X0,X1] :
( ( v1_funct_1(k1_tsp_2(X0,X1))
& v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(flattening,[],[f225]) ).
fof(f229,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f60]) ).
fof(f230,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f229]) ).
fof(f231,plain,
! [X0,X1] :
( ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(ennf_transformation,[],[f61]) ).
fof(f232,plain,
! [X0,X1] :
( ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(flattening,[],[f231]) ).
fof(f235,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f64]) ).
fof(f237,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m1_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f69]) ).
fof(f239,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f71]) ).
fof(f277,plain,
! [X0,X1] :
( k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(ennf_transformation,[],[f110]) ).
fof(f278,plain,
! [X0,X1] :
( k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(flattening,[],[f277]) ).
fof(f279,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f111]) ).
fof(f280,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f279]) ).
fof(f281,plain,
! [X0] :
( ! [X1] :
( m1_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f112]) ).
fof(f282,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f114]) ).
fof(f284,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f117]) ).
fof(f289,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v3_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f122]) ).
fof(f290,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v3_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f289]) ).
fof(f297,definition,
! [X0,X1] :
( sP1(X0,X1)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& ! [X2] :
( ( v3_pre_topc(X2,X1)
<=> ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X3,X0)
& X2 = k3_xboole_0(X3,u1_struct_0(X1)) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f298,definition,
! [X1,X0] :
( ( m1_tsp_1(X1,X0)
<=> sP1(X0,X1) )
| ~ sP2(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f299,plain,
! [X0] :
( ! [X1] :
( sP2(X1,X0)
| ~ l1_pre_topc(X1) )
| ~ l1_pre_topc(X0) ),
inference(definition_folding,[],[f224,f298,f297]) ).
fof(f302,plain,
( ~ v3_pre_topc(k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),sK6),sK5)
& v3_pre_topc(sK6,sK4)
& m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK4)))
& ~ v3_struct_0(sK5)
& v2_tsp_2(sK5,sK4)
& m2_tsp_1(sK5,sK4)
& ~ v3_struct_0(sK4)
& v2_pre_topc(sK4)
& l1_pre_topc(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6)],[f158]) ).
fof(f305,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ? [X3] :
( ? [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) != k4_pre_topc(X0,X1,X2,X4)
& m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
& u1_struct_0(X1) = X3
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X3] :
( ! [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| k4_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f223]) ).
fof(f306,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ? [X3] :
( ? [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) != k4_pre_topc(X0,X1,X2,X4)
& m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
& u1_struct_0(X1) = X3
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X5] :
( ! [X6] :
( k5_subset_1(u1_struct_0(X0),X5,k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,X2,X6)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0))) )
| k4_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f305]) ).
fof(f307,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ( k5_subset_1(u1_struct_0(X0),sK7(X0,X1,X2),k3_tex_4(X0,sK8(X0,X1,X2))) != k4_pre_topc(X0,X1,X2,sK8(X0,X1,X2))
& m1_subset_1(sK8(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
& u1_struct_0(X1) = sK7(X0,X1,X2)
& m1_subset_1(sK7(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X5] :
( ! [X6] :
( k5_subset_1(u1_struct_0(X0),X5,k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,X2,X6)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0))) )
| k4_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X3,sK7(X0,X1,X2)),skolemize(X4,sK8(X0,X1,X2))],[f306]) ).
fof(f308,plain,
! [X1,X0] :
( ( ( m1_tsp_1(X1,X0)
| ~ sP1(X0,X1) )
& ( sP1(X0,X1)
| ~ m1_tsp_1(X1,X0) ) )
| ~ sP2(X1,X0) ),
inference(nnf_transformation,[],[f298]) ).
fof(f309,plain,
! [X0,X1] :
( ( ( m1_tsp_1(X0,X1)
| ~ sP1(X1,X0) )
& ( sP1(X1,X0)
| ~ m1_tsp_1(X0,X1) ) )
| ~ sP2(X0,X1) ),
inference(rectify,[],[f308]) ).
fof(f310,plain,
! [X0,X1] :
( ( sP1(X0,X1)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ? [X2] :
( ( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X3,X0)
| k3_xboole_0(X3,u1_struct_0(X1)) != X2 )
| ~ v3_pre_topc(X2,X1) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X3,X0)
& X2 = k3_xboole_0(X3,u1_struct_0(X1)) )
| v3_pre_topc(X2,X1) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ) )
& ( ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& ! [X2] :
( ( ( v3_pre_topc(X2,X1)
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X3,X0)
| k3_xboole_0(X3,u1_struct_0(X1)) != X2 ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X3,X0)
& X2 = k3_xboole_0(X3,u1_struct_0(X1)) )
| ~ v3_pre_topc(X2,X1) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ) )
| ~ sP1(X0,X1) ) ),
inference(nnf_transformation,[],[f297]) ).
fof(f311,plain,
! [X0,X1] :
( ( sP1(X0,X1)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ? [X2] :
( ( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X3,X0)
| k3_xboole_0(X3,u1_struct_0(X1)) != X2 )
| ~ v3_pre_topc(X2,X1) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X3,X0)
& X2 = k3_xboole_0(X3,u1_struct_0(X1)) )
| v3_pre_topc(X2,X1) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ) )
& ( ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& ! [X2] :
( ( ( v3_pre_topc(X2,X1)
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X3,X0)
| k3_xboole_0(X3,u1_struct_0(X1)) != X2 ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X3,X0)
& X2 = k3_xboole_0(X3,u1_struct_0(X1)) )
| ~ v3_pre_topc(X2,X1) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ) )
| ~ sP1(X0,X1) ) ),
inference(flattening,[],[f310]) ).
fof(f312,plain,
! [X0,X1] :
( ( sP1(X0,X1)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ? [X2] :
( ( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X3,X0)
| k3_xboole_0(X3,u1_struct_0(X1)) != X2 )
| ~ v3_pre_topc(X2,X1) )
& ( ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X4,X0)
& k3_xboole_0(X4,u1_struct_0(X1)) = X2 )
| v3_pre_topc(X2,X1) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ) )
& ( ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& ! [X5] :
( ( ( v3_pre_topc(X5,X1)
| ! [X6] :
( ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X6,X0)
| k3_xboole_0(X6,u1_struct_0(X1)) != X5 ) )
& ( ? [X7] :
( m1_subset_1(X7,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X7,X0)
& k3_xboole_0(X7,u1_struct_0(X1)) = X5 )
| ~ v3_pre_topc(X5,X1) ) )
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) ) )
| ~ sP1(X0,X1) ) ),
inference(rectify,[],[f311]) ).
fof(f313,plain,
! [X0,X1] :
( ( sP1(X0,X1)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ( ( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X3,X0)
| k3_xboole_0(X3,u1_struct_0(X1)) != sK9(X0,X1) )
| ~ v3_pre_topc(sK9(X0,X1),X1) )
& ( ( m1_subset_1(sK10(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(sK10(X0,X1),X0)
& sK9(X0,X1) = k3_xboole_0(sK10(X0,X1),u1_struct_0(X1)) )
| v3_pre_topc(sK9(X0,X1),X1) )
& m1_subset_1(sK9(X0,X1),k1_zfmisc_1(u1_struct_0(X1))) ) )
& ( ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& ! [X5] :
( ( ( v3_pre_topc(X5,X1)
| ! [X6] :
( ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X6,X0)
| k3_xboole_0(X6,u1_struct_0(X1)) != X5 ) )
& ( ( m1_subset_1(sK11(X0,X1,X5),k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(sK11(X0,X1,X5),X0)
& k3_xboole_0(sK11(X0,X1,X5),u1_struct_0(X1)) = X5 )
| ~ v3_pre_topc(X5,X1) ) )
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) ) )
| ~ sP1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11]),skolemize(X2,sK9(X0,X1)),skolemize(X4,sK10(X0,X1)),skolemize(X7,sK11(X0,X1,X5))],[f312]) ).
fof(f335,plain,
! [X0] :
( ! [X1] :
( ( m1_tsp_1(X1,X0)
| ~ m1_pre_topc(X1,X0) )
& ( m1_pre_topc(X1,X0)
| ~ m1_tsp_1(X1,X0) ) )
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f281]) ).
fof(f336,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f113]) ).
fof(f337,plain,
! [X0] :
( ! [X1] :
( ( m2_tsp_1(X1,X0)
| ~ m1_pre_topc(X1,X0) )
& ( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0) ) )
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f282]) ).
fof(f339,plain,
l1_pre_topc(sK4),
inference(cnf_transformation,[],[f302]) ).
fof(f340,plain,
v2_pre_topc(sK4),
inference(cnf_transformation,[],[f302]) ).
fof(f341,plain,
~ v3_struct_0(sK4),
inference(cnf_transformation,[],[f302]) ).
fof(f342,plain,
m2_tsp_1(sK5,sK4),
inference(cnf_transformation,[],[f302]) ).
fof(f343,plain,
v2_tsp_2(sK5,sK4),
inference(cnf_transformation,[],[f302]) ).
fof(f344,plain,
~ v3_struct_0(sK5),
inference(cnf_transformation,[],[f302]) ).
fof(f345,plain,
m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK4))),
inference(cnf_transformation,[],[f302]) ).
fof(f346,plain,
v3_pre_topc(sK6,sK4),
inference(cnf_transformation,[],[f302]) ).
fof(f347,plain,
~ v3_pre_topc(k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),sK6),sK5),
inference(cnf_transformation,[],[f302]) ).
fof(f448,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f50]) ).
fof(f450,plain,
! [X2,X0,X1,X6,X5] :
( k5_subset_1(u1_struct_0(X0),X5,k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,X2,X6)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0)))
| k4_tsp_2(X0,X1) != X2
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f307]) ).
fof(f455,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| ~ m1_tsp_1(X0,X1)
| sP1(X1,X0) ),
inference(cnf_transformation,[],[f309]) ).
fof(f460,plain,
! [X0,X1,X6,X5] :
( v3_pre_topc(X5,X1)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X6,X0)
| k3_xboole_0(X6,u1_struct_0(X1)) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1)))
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f313]) ).
fof(f467,plain,
! [X0,X1] :
( sP2(X1,X0)
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f299]) ).
fof(f468,plain,
! [X0,X1] :
( m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f226]) ).
fof(f470,plain,
! [X0,X1] :
( v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f226]) ).
fof(f473,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f230]) ).
fof(f475,plain,
! [X0,X1] :
( v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f232]) ).
fof(f477,plain,
! [X0,X1] :
( v1_funct_1(k4_tsp_2(X0,X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f232]) ).
fof(f479,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f235]) ).
fof(f481,plain,
! [X0,X1] :
( ~ m1_tsp_1(X1,X0)
| l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f483,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f239]) ).
fof(f582,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1) ),
inference(cnf_transformation,[],[f278]) ).
fof(f583,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
inference(cnf_transformation,[],[f280]) ).
fof(f585,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| m1_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f335]) ).
fof(f586,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f336]) ).
fof(f588,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f337]) ).
fof(f592,plain,
! [X0,X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_pre_topc(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f284]) ).
fof(f598,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X1,X0)
| k3_tex_4(X0,X1) = X1
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f290]) ).
fof(f603,plain,
! [X2,X0,X1,X6] :
( k4_pre_topc(X0,X1,X2,X6) = k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k3_tex_4(X0,X6))
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| k4_tsp_2(X0,X1) != X2
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f450]) ).
fof(f604,plain,
! [X0,X1,X6] :
( ~ m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(k4_tsp_2(X0,X1))
| ~ v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
| k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X6)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f603]) ).
fof(f605,plain,
! [X0,X1,X6] :
( ~ m1_subset_1(k3_xboole_0(X6,u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X6,X0)
| v3_pre_topc(k3_xboole_0(X6,u1_struct_0(X1)),X1)
| ~ sP1(X0,X1) ),
inference(equality_resolution,[],[f460]) ).
fof(f606,definition,
sF32 = k4_tsp_2(sK4,sK5),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f607,plain,
k4_tsp_2(sK4,sK5) = sF32,
inference(reorient_equations,[],[f606]) ).
fof(f608,definition,
sF33 = k4_pre_topc(sK4,sK5,sF32,sK6),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f609,plain,
k4_pre_topc(sK4,sK5,sF32,sK6) = sF33,
inference(reorient_equations,[],[f608]) ).
fof(f610,plain,
~ v3_pre_topc(sF33,sK5),
inference(definition_folding,[],[f347,f609,f607]) ).
fof(f611,definition,
sF34 = u1_struct_0(sK4),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f612,plain,
u1_struct_0(sK4) = sF34,
inference(reorient_equations,[],[f611]) ).
fof(f613,definition,
sF35 = k1_zfmisc_1(sF34),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f614,plain,
k1_zfmisc_1(sF34) = sF35,
inference(reorient_equations,[],[f613]) ).
fof(f615,plain,
m1_subset_1(sK6,sF35),
inference(definition_folding,[],[f345,f614,f612]) ).
fof(f639,plain,
l1_struct_0(sK4),
inference(resolution,[],[f479,f339]) ).
fof(f919,plain,
( l1_pre_topc(sK5)
| ~ l1_pre_topc(sK4) ),
inference(resolution,[],[f483,f342]) ).
fof(f922,plain,
l1_pre_topc(sK5),
inference(forward_subsumption_resolution,[],[f919,f339]) ).
fof(f925,plain,
l1_struct_0(sK5),
inference(resolution,[],[f922,f479]) ).
fof(f1149,plain,
( m1_pre_topc(sK5,sK4)
| ~ l1_pre_topc(sK4) ),
inference(resolution,[],[f588,f342]) ).
fof(f1152,plain,
m1_pre_topc(sK5,sK4),
inference(forward_subsumption_resolution,[],[f1149,f339]) ).
fof(f1153,plain,
( m1_tsp_1(sK5,sK4)
| ~ l1_pre_topc(sK4) ),
inference(resolution,[],[f1152,f585]) ).
fof(f1155,plain,
m1_tsp_1(sK5,sK4),
inference(forward_subsumption_resolution,[],[f1153,f339]) ).
fof(f1195,plain,
! [X0,X1] :
( ~ m1_tsp_1(X0,X1)
| sP1(X1,X0)
| ~ l1_pre_topc(X0)
| ~ l1_pre_topc(X1) ),
inference(resolution,[],[f455,f467]) ).
fof(f1196,plain,
! [X0,X1] :
( ~ m1_tsp_1(X0,X1)
| sP1(X1,X0)
| ~ l1_pre_topc(X1) ),
inference(forward_subsumption_resolution,[],[f1195,f481]) ).
fof(f1391,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(sF34))
| ~ m1_pre_topc(X0,sK4)
| ~ l1_pre_topc(sK4) ),
inference(superposition,[],[f592,f612]) ).
fof(f1392,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(sF34))
| ~ m1_pre_topc(X0,sK4) ),
inference(forward_subsumption_resolution,[],[f1391,f339]) ).
fof(f1394,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),sF35)
| ~ m1_pre_topc(X0,sK4) ),
inference(forward_demodulation,[],[f1392,f614]) ).
fof(f1758,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF35)
| ~ m1_subset_1(X0,sF35)
| k3_xboole_0(X1,X0) = k5_subset_1(sF34,X1,X0) ),
inference(superposition,[],[f583,f614]) ).
fof(f1899,plain,
( v1_funct_1(sF32)
| v3_struct_0(sK4)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(superposition,[],[f477,f607]) ).
fof(f1900,plain,
( v1_funct_1(sF32)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f1899,f341]) ).
fof(f1901,plain,
( v1_funct_1(sF32)
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f1900,f340]) ).
fof(f1902,plain,
( v1_funct_1(sF32)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f1901,f339]) ).
fof(f1903,plain,
( v1_funct_1(sF32)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f1902,f344]) ).
fof(f1904,plain,
( v1_funct_1(sF32)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f1903,f343]) ).
fof(f1905,plain,
v1_funct_1(sF32),
inference(forward_subsumption_resolution,[],[f1904,f1152]) ).
fof(f1957,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF34))
| ~ v3_pre_topc(X0,sK4)
| k3_tex_4(sK4,X0) = X0
| v3_struct_0(sK4)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4) ),
inference(superposition,[],[f598,f612]) ).
fof(f1967,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF34))
| ~ v3_pre_topc(X0,sK4)
| k3_tex_4(sK4,X0) = X0
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4) ),
inference(forward_subsumption_resolution,[],[f1957,f341]) ).
fof(f1977,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF34))
| ~ v3_pre_topc(X0,sK4)
| k3_tex_4(sK4,X0) = X0
| ~ l1_pre_topc(sK4) ),
inference(forward_subsumption_resolution,[],[f1967,f340]) ).
fof(f1979,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF34))
| ~ v3_pre_topc(X0,sK4)
| k3_tex_4(sK4,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f1977,f339]) ).
fof(f1981,plain,
! [X0] :
( ~ v3_pre_topc(X0,sK4)
| ~ m1_subset_1(X0,sF35)
| k3_tex_4(sK4,X0) = X0 ),
inference(forward_demodulation,[],[f1979,f614]) ).
fof(f2049,plain,
( v5_pre_topc(sF32,sK4,sK5)
| v3_struct_0(sK4)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(superposition,[],[f475,f607]) ).
fof(f2050,plain,
( v5_pre_topc(sF32,sK4,sK5)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2049,f341]) ).
fof(f2051,plain,
( v5_pre_topc(sF32,sK4,sK5)
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2050,f340]) ).
fof(f2052,plain,
( v5_pre_topc(sF32,sK4,sK5)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2051,f339]) ).
fof(f2053,plain,
( v5_pre_topc(sF32,sK4,sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2052,f344]) ).
fof(f2054,plain,
( v5_pre_topc(sF32,sK4,sK5)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2053,f343]) ).
fof(f2055,plain,
v5_pre_topc(sF32,sK4,sK5),
inference(forward_subsumption_resolution,[],[f2054,f1152]) ).
fof(f2057,plain,
( v3_struct_0(sK4)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| k4_tsp_2(sK4,sK5) = k1_tsp_2(sK4,sK5) ),
inference(resolution,[],[f582,f1152]) ).
fof(f2059,plain,
( ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| k4_tsp_2(sK4,sK5) = k1_tsp_2(sK4,sK5) ),
inference(forward_subsumption_resolution,[],[f2057,f341]) ).
fof(f2060,plain,
( ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| k4_tsp_2(sK4,sK5) = k1_tsp_2(sK4,sK5) ),
inference(forward_subsumption_resolution,[],[f2059,f340]) ).
fof(f2061,plain,
( v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| k4_tsp_2(sK4,sK5) = k1_tsp_2(sK4,sK5) ),
inference(forward_subsumption_resolution,[],[f2060,f339]) ).
fof(f2062,plain,
( ~ v2_tsp_2(sK5,sK4)
| k4_tsp_2(sK4,sK5) = k1_tsp_2(sK4,sK5) ),
inference(forward_subsumption_resolution,[],[f2061,f344]) ).
fof(f2063,plain,
k4_tsp_2(sK4,sK5) = k1_tsp_2(sK4,sK5),
inference(forward_subsumption_resolution,[],[f2062,f343]) ).
fof(f2064,plain,
sF32 = k1_tsp_2(sK4,sK5),
inference(forward_demodulation,[],[f2063,f607]) ).
fof(f2068,plain,
( m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| v3_struct_0(sK4)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(superposition,[],[f468,f2064]) ).
fof(f2073,plain,
( m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2068,f341]) ).
fof(f2075,plain,
( m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2073,f340]) ).
fof(f2077,plain,
( m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2075,f339]) ).
fof(f2078,plain,
( m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2077,f344]) ).
fof(f2079,plain,
( m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2078,f343]) ).
fof(f2080,plain,
m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5)),
inference(forward_subsumption_resolution,[],[f2079,f1152]) ).
fof(f2081,plain,
m2_relset_1(sF32,sF34,u1_struct_0(sK5)),
inference(forward_demodulation,[],[f2080,f612]) ).
fof(f2082,plain,
m1_relset_1(sF32,sF34,u1_struct_0(sK5)),
inference(resolution,[],[f2081,f586]) ).
fof(f2083,plain,
( v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| v3_struct_0(sK4)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(superposition,[],[f470,f2064]) ).
fof(f2088,plain,
( v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2083,f341]) ).
fof(f2090,plain,
( v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ l1_pre_topc(sK4)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2088,f340]) ).
fof(f2092,plain,
( v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2090,f339]) ).
fof(f2093,plain,
( v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ v2_tsp_2(sK5,sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2092,f344]) ).
fof(f2094,plain,
( v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_pre_topc(sK5,sK4) ),
inference(forward_subsumption_resolution,[],[f2093,f343]) ).
fof(f2095,plain,
v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5)),
inference(forward_subsumption_resolution,[],[f2094,f1152]) ).
fof(f2096,plain,
v1_funct_2(sF32,sF34,u1_struct_0(sK5)),
inference(forward_demodulation,[],[f2095,f612]) ).
fof(f2174,plain,
( m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK5)))
| ~ l1_struct_0(sK4)
| ~ l1_struct_0(sK5)
| ~ v1_funct_1(sF32)
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5)) ),
inference(superposition,[],[f473,f609]) ).
fof(f2177,plain,
( m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK5)))
| ~ l1_struct_0(sK5)
| ~ v1_funct_1(sF32)
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5)) ),
inference(forward_subsumption_resolution,[],[f2174,f639]) ).
fof(f2189,plain,
( m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK5)))
| ~ v1_funct_1(sF32)
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5)) ),
inference(forward_subsumption_resolution,[],[f2177,f925]) ).
fof(f2190,plain,
( m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK5)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5)) ),
inference(forward_subsumption_resolution,[],[f2189,f1905]) ).
fof(f2191,plain,
( ~ v1_funct_2(sF32,sF34,u1_struct_0(sK5))
| m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK5)))
| ~ m1_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5)) ),
inference(forward_demodulation,[],[f2190,f612]) ).
fof(f2192,plain,
( m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK5)))
| ~ m1_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5)) ),
inference(forward_subsumption_resolution,[],[f2191,f2096]) ).
fof(f2193,plain,
( ~ m1_relset_1(sF32,sF34,u1_struct_0(sK5))
| m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK5))) ),
inference(forward_demodulation,[],[f2192,f612]) ).
fof(f2194,plain,
m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK5))),
inference(forward_subsumption_resolution,[],[f2193,f2082]) ).
fof(f2359,plain,
! [X0] :
( ~ m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_1(sF32)
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ v5_pre_topc(sF32,sK4,sK5)
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m2_tsp_1(sK5,sK4)
| v3_struct_0(sK4)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4) ),
inference(superposition,[],[f604,f607]) ).
fof(f2365,plain,
! [X0] :
( ~ m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ v5_pre_topc(sF32,sK4,sK5)
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m2_tsp_1(sK5,sK4)
| v3_struct_0(sK4)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4) ),
inference(forward_subsumption_resolution,[],[f2359,f1905]) ).
fof(f2368,plain,
! [X0] :
( ~ m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0)
| v3_struct_0(sK5)
| ~ v2_tsp_2(sK5,sK4)
| ~ m2_tsp_1(sK5,sK4)
| v3_struct_0(sK4)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4) ),
inference(forward_subsumption_resolution,[],[f2365,f2055]) ).
fof(f2371,plain,
! [X0] :
( ~ m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0)
| ~ v2_tsp_2(sK5,sK4)
| ~ m2_tsp_1(sK5,sK4)
| v3_struct_0(sK4)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4) ),
inference(forward_subsumption_resolution,[],[f2368,f344]) ).
fof(f2374,plain,
! [X0] :
( ~ m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0)
| ~ m2_tsp_1(sK5,sK4)
| v3_struct_0(sK4)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4) ),
inference(forward_subsumption_resolution,[],[f2371,f343]) ).
fof(f2377,plain,
! [X0] :
( ~ m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0)
| v3_struct_0(sK4)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4) ),
inference(forward_subsumption_resolution,[],[f2374,f342]) ).
fof(f2379,plain,
! [X0] :
( ~ m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0)
| ~ v2_pre_topc(sK4)
| ~ l1_pre_topc(sK4) ),
inference(forward_subsumption_resolution,[],[f2377,f341]) ).
fof(f2380,plain,
! [X0] :
( ~ m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0)
| ~ l1_pre_topc(sK4) ),
inference(forward_subsumption_resolution,[],[f2379,f340]) ).
fof(f2381,plain,
! [X0] :
( ~ m2_relset_1(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0) ),
inference(forward_subsumption_resolution,[],[f2380,f339]) ).
fof(f2382,plain,
! [X0] :
( ~ m2_relset_1(sF32,sF34,u1_struct_0(sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0) ),
inference(forward_demodulation,[],[f2381,f612]) ).
fof(f2383,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0) ),
inference(forward_subsumption_resolution,[],[f2382,f2081]) ).
fof(f2384,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF34))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0) ),
inference(forward_demodulation,[],[f2383,f612]) ).
fof(f2385,plain,
! [X0] :
( ~ m1_subset_1(X0,sF35)
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0) ),
inference(forward_demodulation,[],[f2384,f614]) ).
fof(f2386,plain,
! [X0] :
( ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(sF34))
| ~ m1_subset_1(X0,sF35)
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0) ),
inference(forward_demodulation,[],[f2385,f612]) ).
fof(f2387,plain,
! [X0] :
( ~ m1_subset_1(u1_struct_0(sK5),sF35)
| ~ m1_subset_1(X0,sF35)
| ~ v1_funct_2(sF32,u1_struct_0(sK4),u1_struct_0(sK5))
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0) ),
inference(forward_demodulation,[],[f2386,f614]) ).
fof(f2388,plain,
! [X0] :
( ~ v1_funct_2(sF32,sF34,u1_struct_0(sK5))
| ~ m1_subset_1(u1_struct_0(sK5),sF35)
| ~ m1_subset_1(X0,sF35)
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0) ),
inference(forward_demodulation,[],[f2387,f612]) ).
fof(f2389,plain,
! [X0] :
( ~ m1_subset_1(u1_struct_0(sK5),sF35)
| ~ m1_subset_1(X0,sF35)
| k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,sF32,X0) ),
inference(forward_subsumption_resolution,[],[f2388,f2096]) ).
fof(f2390,plain,
! [X0] :
( ~ m1_subset_1(u1_struct_0(sK5),sF35)
| k4_pre_topc(sK4,sK5,sF32,X0) = k5_subset_1(sF34,u1_struct_0(sK5),k3_tex_4(sK4,X0))
| ~ m1_subset_1(X0,sF35) ),
inference(forward_demodulation,[],[f2389,f612]) ).
fof(f2431,plain,
( ~ m1_subset_1(sK6,sF35)
| sK6 = k3_tex_4(sK4,sK6) ),
inference(resolution,[],[f1981,f346]) ).
fof(f2441,plain,
sK6 = k3_tex_4(sK4,sK6),
inference(forward_subsumption_resolution,[],[f2431,f615]) ).
fof(f2510,plain,
! [X0] :
( k4_pre_topc(sK4,sK5,sF32,X0) = k5_subset_1(sF34,u1_struct_0(sK5),k3_tex_4(sK4,X0))
| ~ m1_subset_1(X0,sF35)
| ~ m1_pre_topc(sK5,sK4) ),
inference(resolution,[],[f2390,f1394]) ).
fof(f2511,plain,
! [X0] :
( ~ m1_subset_1(X0,sF35)
| k4_pre_topc(sK4,sK5,sF32,X0) = k5_subset_1(sF34,u1_struct_0(sK5),k3_tex_4(sK4,X0)) ),
inference(forward_subsumption_resolution,[],[f2510,f1152]) ).
fof(f3387,plain,
( sP1(sK4,sK5)
| ~ l1_pre_topc(sK4) ),
inference(resolution,[],[f1196,f1155]) ).
fof(f3391,plain,
sP1(sK4,sK5),
inference(forward_subsumption_resolution,[],[f3387,f339]) ).
fof(f5297,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,sK4)
| k3_xboole_0(u1_struct_0(X1),X0) = k5_subset_1(sF34,u1_struct_0(X1),X0)
| ~ m1_subset_1(X0,sF35) ),
inference(resolution,[],[f1758,f1394]) ).
fof(f16473,plain,
k4_pre_topc(sK4,sK5,sF32,sK6) = k5_subset_1(sF34,u1_struct_0(sK5),k3_tex_4(sK4,sK6)),
inference(resolution,[],[f2511,f615]) ).
fof(f16502,plain,
k4_pre_topc(sK4,sK5,sF32,sK6) = k5_subset_1(sF34,u1_struct_0(sK5),sK6),
inference(forward_demodulation,[],[f16473,f2441]) ).
fof(f16514,plain,
sF33 = k5_subset_1(sF34,u1_struct_0(sK5),sK6),
inference(forward_demodulation,[],[f16502,f609]) ).
fof(f16622,plain,
! [X0] :
( ~ m1_subset_1(X0,sF35)
| k3_xboole_0(u1_struct_0(sK5),X0) = k5_subset_1(sF34,u1_struct_0(sK5),X0) ),
inference(resolution,[],[f5297,f1152]) ).
fof(f97154,plain,
k5_subset_1(sF34,u1_struct_0(sK5),sK6) = k3_xboole_0(u1_struct_0(sK5),sK6),
inference(resolution,[],[f16622,f615]) ).
fof(f97180,plain,
k5_subset_1(sF34,u1_struct_0(sK5),sK6) = k3_xboole_0(sK6,u1_struct_0(sK5)),
inference(forward_demodulation,[],[f97154,f448]) ).
fof(f97183,plain,
sF33 = k3_xboole_0(sK6,u1_struct_0(sK5)),
inference(forward_demodulation,[],[f97180,f16514]) ).
fof(f97202,plain,
! [X0] :
( ~ m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK5)))
| ~ m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(sK6,X0)
| v3_pre_topc(sF33,sK5)
| ~ sP1(X0,sK5) ),
inference(superposition,[],[f605,f97183]) ).
fof(f97233,plain,
! [X0] :
( ~ m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(sK6,X0)
| v3_pre_topc(sF33,sK5)
| ~ sP1(X0,sK5) ),
inference(forward_subsumption_resolution,[],[f97202,f2194]) ).
fof(f97235,plain,
! [X0] :
( ~ m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(sK6,X0)
| ~ sP1(X0,sK5) ),
inference(forward_subsumption_resolution,[],[f97233,f610]) ).
fof(f101836,plain,
( ~ m1_subset_1(sK6,k1_zfmisc_1(sF34))
| ~ v3_pre_topc(sK6,sK4)
| ~ sP1(sK4,sK5) ),
inference(superposition,[],[f97235,f612]) ).
fof(f101837,plain,
( ~ m1_subset_1(sK6,k1_zfmisc_1(sF34))
| ~ sP1(sK4,sK5) ),
inference(forward_subsumption_resolution,[],[f101836,f346]) ).
fof(f101838,plain,
~ m1_subset_1(sK6,k1_zfmisc_1(sF34)),
inference(forward_subsumption_resolution,[],[f101837,f3391]) ).
fof(f101839,plain,
~ m1_subset_1(sK6,sF35),
inference(forward_demodulation,[],[f101838,f614]) ).
fof(f101840,plain,
$false,
inference(forward_subsumption_resolution,[],[f101839,f615]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP041+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n003.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 19:03:42 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 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
% 14.79/2.38 % (1881473)Will run a generic schedule for satisfiability detection.
% 14.79/2.38 % (1881483)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2040612985_2999 on theBenchmark for (2999ds/0Mi)
% 14.79/2.38 % (1881484)% WARNING: option uhcvi not known.
% 14.79/2.38 % (1881484)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2657324543:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.79/2.38 % TRYING [1]
% 14.79/2.38 % (1881487)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3288180174:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.79/2.38 % (1881488)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3919458157:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.79/2.38 % TRYING [2]
% 14.79/2.38 % (1881489)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3196332773:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.79/2.38 % TRYING [3]
% 14.79/2.38 % (1881485)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=866082046:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.79/2.38 % (1881486)dis+10_1_sil=32000:sp=arity:random_seed=3628031203:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.79/2.38 % TRYING [4]
% 14.79/2.38 % TRYING [5]
% 14.79/2.38 % (1881487)Instruction limit reached!
% 14.79/2.38 % (1881487)------------------------------
% 14.79/2.38 % (1881487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.79/2.38 % (1881487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.38 % (1881487)CaDiCaL version: 2.1.3
% 14.79/2.38 % (1881487)Termination reason: Instruction limit
% 14.79/2.38 % (1881487)Termination phase: Saturation
% 14.79/2.38 % (1881487)Time elapsed: 0.073 s
% 14.79/2.38 % (1881487)Peak memory usage: 13 MB
% 14.79/2.38 % (1881487)Instructions burned: 117 (million)
% 14.79/2.38 % (1881486)Instruction limit reached!
% 14.79/2.38 % (1881486)------------------------------
% 14.79/2.38 % (1881486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.79/2.38 % (1881486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.38 % (1881486)CaDiCaL version: 2.1.3
% 14.79/2.38 % (1881486)Termination reason: Instruction limit
% 14.79/2.38 % (1881486)Termination phase: Saturation
% 14.79/2.38 % (1881486)Time elapsed: 0.064 s
% 14.79/2.38 % (1881486)Peak memory usage: 13 MB
% 14.79/2.38 % (1881486)Instructions burned: 103 (million)
% 14.79/2.38 % (1881488)Instruction limit reached!
% 14.79/2.38 % (1881488)------------------------------
% 14.79/2.38 % (1881488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.79/2.38 % (1881488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.38 % (1881488)CaDiCaL version: 2.1.3
% 14.79/2.38 % (1881488)Termination reason: Instruction limit
% 14.79/2.38 % (1881488)Termination phase: Saturation
% 14.79/2.38 % (1881488)Time elapsed: 0.080 s
% 14.79/2.38 % (1881488)Peak memory usage: 13 MB
% 14.79/2.38 % (1881488)Instructions burned: 132 (million)
% 14.79/2.38 % (1881520)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=557616695:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.79/2.38 % (1881521)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2109178666:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.79/2.38 % (1881489)Instruction limit reached!
% 14.79/2.38 % (1881489)------------------------------
% 14.79/2.38 % (1881489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.79/2.38 % (1881489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/2.38 % (1881489)CaDiCaL version: 2.1.3
% 14.79/2.38 % (1881489)Termination reason: Instruction limit
% 14.79/2.38 % (1881489)Termination phase: Saturation
% 14.79/2.38 % (1881489)Time elapsed: 0.098 s
% 14.79/2.38 % (1881489)Peak memory usage: 15 MB
% 14.79/2.38 % (1881489)Instructions burned: 160 (million)
% 14.79/2.38 % (1881522)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=1143081619:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.79/2.38 % TRYING [1]
% 14.79/2.38 % TRYING [2]
% 14.79/2.38 % TRYING [3]
% 14.79/2.38 % (1881526)ott-21_1_sil=16000:fs=off:random_seed=239319217:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.79/2.38 % TRYING [4]
% 14.79/2.38 % TRYING [6]
% 14.79/2.38 % (1881521)Instruction limit reached!
% 14.79/2.38 % (1881521)------------------------------
% 14.79/2.38 % (1881521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.87/6.48 % (1881521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.87/6.48 % (1881521)CaDiCaL version: 2.1.3
% 43.87/6.48 % (1881521)Termination reason: Instruction limit
% 43.87/6.48 % (1881521)Termination phase: Saturation
% 43.87/6.48 % (1881521)Time elapsed: 0.083 s
% 43.87/6.48 % (1881521)Peak memory usage: 13 MB
% 43.87/6.48 % (1881521)Instructions burned: 132 (million)
% 43.87/6.48 % TRYING [5]
% 43.87/6.48 % (1881533)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1732019400:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 43.87/6.48 % (1881526)Instruction limit reached!
% 43.87/6.48 % (1881526)------------------------------
% 43.87/6.48 % (1881526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.87/6.48 % (1881526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.87/6.48 % (1881526)CaDiCaL version: 2.1.3
% 43.87/6.48 % (1881526)Termination reason: Instruction limit
% 43.87/6.48 % (1881526)Termination phase: Saturation
% 43.87/6.48 % (1881526)Time elapsed: 0.095 s
% 43.87/6.48 % (1881526)Peak memory usage: 13 MB
% 43.87/6.48 % (1881526)Instructions burned: 181 (million)
% 43.87/6.48 % (1881546)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1795968300:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 43.87/6.48 % TRYING [1]
% 43.87/6.48 % TRYING [2]
% 43.87/6.48 % TRYING [3]
% 43.87/6.48 % TRYING [4]
% 43.87/6.48 % TRYING [6]
% 43.87/6.48 % (1881520)Instruction limit reached!
% 43.87/6.48 % (1881520)------------------------------
% 43.87/6.48 % (1881520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.87/6.48 % (1881520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.87/6.48 % (1881520)CaDiCaL version: 2.1.3
% 43.87/6.48 % (1881520)Termination reason: Instruction limit
% 43.87/6.48 % (1881520)Termination phase: Finite model building constraint generation
% 43.87/6.48 % (1881520)Time elapsed: 0.271 s
% 43.87/6.48 % (1881520)Peak memory usage: 34 MB
% 43.87/6.48 % (1881520)Instructions burned: 716 (million)
% 43.87/6.48 % (1881579)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2857233710:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 43.87/6.48 % TRYING [7]
% 43.87/6.48 % (1881522)Instruction limit reached!
% 43.87/6.48 % (1881522)------------------------------
% 43.87/6.48 % (1881522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.87/6.48 % (1881522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.87/6.48 % (1881522)CaDiCaL version: 2.1.3
% 43.87/6.48 % (1881522)Termination reason: Instruction limit
% 43.87/6.48 % (1881522)Termination phase: Saturation
% 43.87/6.48 % (1881522)Time elapsed: 0.400 s
% 43.87/6.48 % (1881522)Peak memory usage: 20 MB
% 43.87/6.48 % (1881522)Instructions burned: 684 (million)
% 43.87/6.48 % (1881581)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3484466507:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 43.87/6.48 % (1881533)Instruction limit reached!
% 43.87/6.48 % (1881533)------------------------------
% 43.87/6.48 % (1881533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.87/6.48 % (1881533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.87/6.48 % (1881533)CaDiCaL version: 2.1.3
% 43.87/6.48 % (1881533)Termination reason: Instruction limit
% 43.87/6.48 % (1881533)Termination phase: Saturation
% 43.87/6.48 % (1881533)Time elapsed: 0.323 s
% 43.87/6.48 % (1881533)Peak memory usage: 15 MB
% 43.87/6.48 % (1881533)Instructions burned: 478 (million)
% 43.87/6.48 % TRYING [5]
% 43.87/6.48 % (1881583)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=4020186240:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 43.87/6.48 % (1881546)Instruction limit reached!
% 43.87/6.48 % (1881546)------------------------------
% 43.87/6.48 % (1881546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.87/6.48 % (1881546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.87/6.48 % (1881546)CaDiCaL version: 2.1.3
% 43.87/6.48 % (1881546)Termination reason: Instruction limit
% 43.87/6.48 % (1881546)Termination phase: Finite model building constraint generation
% 43.87/6.48 % (1881546)Time elapsed: 0.325 s
% 43.87/6.48 % (1881546)Peak memory usage: 23 MB
% 43.87/6.48 % (1881546)Instructions burned: 867 (million)
% 43.87/6.48 % (1881585)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1393608136:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 43.87/6.48 % (1881581)Instruction limit reached!
% 30.37/6.71 % (1881581)------------------------------
% 30.37/6.71 % (1881581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881581)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881581)Termination reason: Instruction limit
% 30.37/6.71 % (1881581)Termination phase: Finite model building constraint generation
% 30.37/6.71 % (1881581)Time elapsed: 0.415 s
% 30.37/6.71 % (1881581)Peak memory usage: 107 MB
% 30.37/6.71 % (1881581)Instructions burned: 891 (million)
% 30.37/6.71 % (1881587)fmb+10_1_sil=64000:random_seed=2370918154:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 30.37/6.71 % TRYING [1]
% 30.37/6.71 % (1881583)Instruction limit reached!
% 30.37/6.71 % (1881583)------------------------------
% 30.37/6.71 % (1881583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881583)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881583)Termination reason: Instruction limit
% 30.37/6.71 % (1881583)Termination phase: Saturation
% 30.37/6.71 % (1881583)Time elapsed: 0.442 s
% 30.37/6.71 % (1881583)Peak memory usage: 19 MB
% 30.37/6.71 % (1881583)Instructions burned: 692 (million)
% 30.37/6.71 % TRYING [2]
% 30.37/6.71 % TRYING [3]
% 30.37/6.71 % (1881589)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1222455486:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 30.37/6.71 % TRYING [20]
% 30.37/6.71 % TRYING [4]
% 30.37/6.71 % (1881579)Instruction limit reached!
% 30.37/6.71 % (1881579)------------------------------
% 30.37/6.71 % (1881579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881579)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881579)Termination reason: Instruction limit
% 30.37/6.71 % (1881579)Termination phase: Saturation
% 30.37/6.71 % (1881579)Time elapsed: 0.694 s
% 30.37/6.71 % (1881579)Peak memory usage: 26 MB
% 30.37/6.71 % (1881579)Instructions burned: 1182 (million)
% 30.37/6.71 % (1881585)Instruction limit reached!
% 30.37/6.71 % (1881585)------------------------------
% 30.37/6.71 % (1881585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881585)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881585)Termination reason: Instruction limit
% 30.37/6.71 % (1881585)Termination phase: Saturation
% 30.37/6.71 % (1881585)Time elapsed: 0.509 s
% 30.37/6.71 % (1881585)Peak memory usage: 19 MB
% 30.37/6.71 % (1881585)Instructions burned: 880 (million)
% 30.37/6.71 % (1881591)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3845441505:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 30.37/6.71 % (1881592)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3963883773:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 30.37/6.71 % TRYING [8]
% 30.37/6.71 % TRYING [5]
% 30.37/6.71 % (1881591)Instruction limit reached!
% 30.37/6.71 % (1881591)------------------------------
% 30.37/6.71 % (1881591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881591)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881591)Termination reason: Instruction limit
% 30.37/6.71 % (1881591)Termination phase: Finite model building constraint generation
% 30.37/6.71 % (1881591)Time elapsed: 0.302 s
% 30.37/6.71 % (1881591)Peak memory usage: 56 MB
% 30.37/6.71 % (1881591)Instructions burned: 921 (million)
% 30.37/6.71 % (1881595)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2182236843:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 30.37/6.71 % TRYING [8]
% 30.37/6.71 % TRYING [6]
% 30.37/6.71 % (1881595)Instruction limit reached!
% 30.37/6.71 % (1881595)------------------------------
% 30.37/6.71 % (1881595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881595)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881595)Termination reason: Instruction limit
% 30.37/6.71 % (1881595)Termination phase: Saturation
% 30.37/6.71 % (1881595)Time elapsed: 0.663 s
% 30.37/6.71 % (1881595)Peak memory usage: 18 MB
% 30.37/6.71 % (1881595)Instructions burned: 1475 (million)
% 30.37/6.71 % (1881597)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1537985314:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 30.37/6.71 % (1881597)Cannot represent all propositional literals internally
% 30.37/6.71 % (1881597)Refutation not found, incomplete strategy
% 30.37/6.71 % (1881597)------------------------------
% 30.37/6.71 % (1881597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881597)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881597)Termination reason: Refutation not found, incomplete strategy
% 30.37/6.71 % (1881597)Time elapsed: 0.015 s
% 30.37/6.71 % (1881597)Peak memory usage: 11 MB
% 30.37/6.71 % (1881597)Instructions burned: 30 (million)
% 30.37/6.71 % (1881597)------------------------------
% 30.37/6.71 % (1881597)------------------------------
% 30.37/6.71 % (1881599)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=855002952:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 30.37/6.71 % TRYING [16]
% 30.37/6.71 % TRYING [7]
% 30.37/6.71 % (1881599)Instruction limit reached!
% 30.37/6.71 % (1881599)------------------------------
% 30.37/6.71 % (1881599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881599)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881599)Termination reason: Instruction limit
% 30.37/6.71 % (1881599)Termination phase: Finite model building constraint generation
% 30.37/6.71 % (1881599)Time elapsed: 0.756 s
% 30.37/6.71 % (1881599)Peak memory usage: 129 MB
% 30.37/6.71 % (1881599)Instructions burned: 2176 (million)
% 30.37/6.71 % (1881601)ott-2_1_sil=16000:newcnf=on:random_seed=2889444158:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi)
% 30.37/6.71 % (1881601)Instruction limit reached!
% 30.37/6.71 % (1881601)------------------------------
% 30.37/6.71 % (1881601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881601)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881601)Termination reason: Instruction limit
% 30.37/6.71 % (1881601)Termination phase: Saturation
% 30.37/6.71 % (1881601)Time elapsed: 0.486 s
% 30.37/6.71 % (1881601)Peak memory usage: 23 MB
% 30.37/6.71 % (1881601)Instructions burned: 872 (million)
% 30.37/6.71 % (1881603)ott+10_1_sil=32000:tgt=ground:random_seed=1314505335:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 30.37/6.71 % (1881589)Instruction limit reached!
% 30.37/6.71 % (1881589)------------------------------
% 30.37/6.71 % (1881589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881589)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881589)Termination reason: Instruction limit
% 30.37/6.71 % (1881589)Termination phase: Finite model building constraint generation
% 30.37/6.71 % (1881589)Time elapsed: 3.122 s
% 30.37/6.71 % (1881589)Peak memory usage: 527 MB
% 30.37/6.71 % (1881589)Instructions burned: 9517 (million)
% 30.37/6.71 % (1881592)Instruction limit reached!
% 30.37/6.71 % (1881592)------------------------------
% 30.37/6.71 % (1881592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881592)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881592)Termination reason: Instruction limit
% 30.37/6.71 % (1881592)Termination phase: Saturation
% 30.37/6.71 % (1881592)Time elapsed: 3.026 s
% 30.37/6.71 % (1881592)Peak memory usage: 37 MB
% 30.37/6.71 % (1881592)Instructions burned: 5131 (million)
% 30.37/6.71 % (1881605)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=391727432:i=54282_2958 on theBenchmark for (2958ds/54282Mi)
% 30.37/6.71 % TRYING [1]
% 30.37/6.71 % TRYING [2]
% 30.37/6.71 % TRYING [3]
% 30.37/6.71 % TRYING [4]
% 30.37/6.71 % (1881607)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3585441159:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 30.37/6.71 % TRYING [5]
% 30.37/6.71 % TRYING [6]
% 30.37/6.71 % TRYING [7]
% 30.37/6.71 % TRYING [8]
% 30.37/6.71 % (1881607)Instruction limit reached!
% 30.37/6.71 % (1881607)------------------------------
% 30.37/6.71 % (1881607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881607)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881607)Termination reason: Instruction limit
% 30.37/6.71 % (1881607)Termination phase: Saturation
% 30.37/6.71 % (1881607)Time elapsed: 2.009 s
% 30.37/6.71 % (1881607)Peak memory usage: 34 MB
% 30.37/6.71 % (1881607)Instructions burned: 3514 (million)
% 30.37/6.71 % (1881609)dis+21_1_sil=32000:sas=cadical:random_seed=3471272143:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi)
% 30.37/6.71 % (1881603) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1881473-1881603"...
% 30.37/6.71 % (1881603)...printing done.
% 30.37/6.71 % (1881603)Refutation found. Thanks to Tanya!
% 30.37/6.71 % SZS status Theorem for theBenchmark
% 30.37/6.71 % SZS output start Proof for theBenchmark
% See solution above
% 30.37/6.71 % (1881603)------------------------------
% 30.37/6.71 % (1881603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.37/6.71 % (1881603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.37/6.71 % (1881603)CaDiCaL version: 2.1.3
% 30.37/6.71 % (1881603)Termination reason: Refutation
% 30.37/6.71 % (1881603)Time elapsed: 2.940 s
% 30.37/6.71 % (1881603)Peak memory usage: 48 MB
% 30.37/6.71 % (1881603)Instructions burned: 4976 (million)
% 30.37/6.71 % (1881473)Success in time 6.486 s
% 30.37/6.71 % Vampire exiting
%------------------------------------------------------------------------------