%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP041+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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:03 PM UTC 2026
% Result : Theorem 26.48s 5.47s
% Output : Refutation 31.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 24
% Syntax : Number of formulae : 279 ( 53 unt; 5 def)
% Number of atoms : 1397 ( 177 equ)
% Maximal formula atoms : 20 ( 5 avg)
% Number of connectives : 1941 ( 823 ~; 929 |; 136 &)
% ( 17 <=>; 36 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 6 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 3 con; 0-4 aty)
% Number of variables : 365 ( 0 sgn 346 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21,axiom,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f574,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(f602,axiom,
! [X0,X1] : k1_setfam_1(k2_tarski(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_setfam_1) ).
fof(f1394,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(f6788,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f6850,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f6857,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)) )
=> k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_pre_topc) ).
fof(f13329,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(f13459,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(f13461,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(f13469,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(f13470,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(f13489,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l19_tsp_2) ).
fof(f13505,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [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)
<=> ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v3_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_tsp_2) ).
fof(f13512,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))
& v3_borsuk_1(X2,X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t22_tsp_2) ).
fof(f13519,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 = k1_tsp_2(X0,X1)
<=> v3_borsuk_1(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_tsp_2) ).
fof(f13527,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(f13533,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(f13534,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)],[f13533]) ).
fof(f13616,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,[],[f13469]) ).
fof(f13617,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,[],[f13616]) ).
fof(f13618,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,[],[f13470]) ).
fof(f13619,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,[],[f13618]) ).
fof(f13656,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13489]) ).
fof(f13657,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13656]) ).
fof(f13688,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v3_pre_topc(X2,X0)
<=> ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v3_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ 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,[],[f13505]) ).
fof(f13689,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v3_pre_topc(X2,X0)
<=> ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v3_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13688]) ).
fof(f13702,plain,
! [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_borsuk_1(X2,X0,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,[],[f13512]) ).
fof(f13703,plain,
! [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_borsuk_1(X2,X0,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,[],[f13702]) ).
fof(f13716,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k1_tsp_2(X0,X1)
<=> v3_borsuk_1(X2,X0,X1) )
| ~ 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,[],[f13519]) ).
fof(f13717,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k1_tsp_2(X0,X1)
<=> v3_borsuk_1(X2,X0,X1) )
| ~ 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,[],[f13716]) ).
fof(f13732,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,[],[f13527]) ).
fof(f13733,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,[],[f13732]) ).
fof(f13744,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,[],[f13534]) ).
fof(f13745,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,[],[f13744]) ).
fof(f13866,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,[],[f574]) ).
fof(f13867,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,[],[f13866]) ).
fof(f14001,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,[],[f13329]) ).
fof(f14002,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,[],[f14001]) ).
fof(f14253,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13461]) ).
fof(f14255,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13459]) ).
fof(f14477,plain,
! [X0,X1,X2,X3] :
( k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(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)) ),
inference(ennf_transformation,[],[f6857]) ).
fof(f14478,plain,
! [X0,X1,X2,X3] :
( k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(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)) ),
inference(flattening,[],[f14477]) ).
fof(f14891,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f6850]) ).
fof(f15093,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6788]) ).
fof(f20694,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v3_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v3_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v3_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) )
| ~ v3_pre_topc(X2,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ 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,[],[f13689]) ).
fof(f20695,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v3_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v3_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v3_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) )
| ~ v3_pre_topc(X2,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f20694]) ).
fof(f20696,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v3_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v3_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X1)))
& v3_pre_topc(X4,X1)
& k3_xboole_0(X2,u1_struct_0(X1)) = X4 ) )
| ~ v3_pre_topc(X2,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f20695]) ).
fof(f20697,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v3_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v3_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& m1_subset_1(sK63(X1,X2),k1_zfmisc_1(u1_struct_0(X1)))
& v3_pre_topc(sK63(X1,X2),X1)
& k3_xboole_0(X2,u1_struct_0(X1)) = sK63(X1,X2) )
| ~ v3_pre_topc(X2,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ 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,[sK63]),skolemize(X4,sK63(X1,X2))],[f20696]) ).
fof(f20708,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(sK69(X0,X1))
& v1_funct_2(sK69(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(sK69(X0,X1),X0,X1)
& m2_relset_1(sK69(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v3_borsuk_1(sK69(X0,X1),X0,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,[sK69]),skolemize(X2,sK69(X0,X1))],[f13703]) ).
fof(f20709,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k1_tsp_2(X0,X1)
| ~ v3_borsuk_1(X2,X0,X1) )
& ( v3_borsuk_1(X2,X0,X1)
| k1_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,[],[f13717]) ).
fof(f20716,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,[],[f13733]) ).
fof(f20717,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,[],[f20716]) ).
fof(f20718,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ( k5_subset_1(u1_struct_0(X0),sK73(X0,X1,X2),k3_tex_4(X0,sK74(X0,X1,X2))) != k4_pre_topc(X0,X1,X2,sK74(X0,X1,X2))
& m1_subset_1(sK74(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
& u1_struct_0(X1) = sK73(X0,X1,X2)
& m1_subset_1(sK73(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,[sK73,sK74]),skolemize(X3,sK73(X0,X1,X2)),skolemize(X4,sK74(X0,X1,X2))],[f20717]) ).
fof(f20719,plain,
( ~ v3_pre_topc(k4_pre_topc(sK75,sK76,k4_tsp_2(sK75,sK76),sK77),sK76)
& v3_pre_topc(sK77,sK75)
& m1_subset_1(sK77,k1_zfmisc_1(u1_struct_0(sK75)))
& ~ v3_struct_0(sK76)
& v2_tsp_2(sK76,sK75)
& m2_tsp_1(sK76,sK75)
& ~ v3_struct_0(sK75)
& v2_pre_topc(sK75)
& l1_pre_topc(sK75) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK75,sK76,sK77]),skolemize(X0,sK75),skolemize(X1,sK76),skolemize(X2,sK77)],[f13745]) ).
fof(f20894,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,[],[f14253]) ).
fof(f21037,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,[],[f1394]) ).
fof(f22974,plain,
! [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(cnf_transformation,[],[f13617]) ).
fof(f22975,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f13617]) ).
fof(f22976,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)
| v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f13617]) ).
fof(f22978,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)
| k1_tsp_2(X0,X1) = k4_tsp_2(X0,X1) ),
inference(cnf_transformation,[],[f13619]) ).
fof(f23030,plain,
! [X0,X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f13657]) ).
fof(f23077,plain,
! [X2,X0,X1] :
( k3_xboole_0(X2,u1_struct_0(X1)) = sK63(X1,X2)
| ~ v3_pre_topc(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ 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,[],[f20697]) ).
fof(f23078,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v3_pre_topc(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| v3_pre_topc(sK63(X1,X2),X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f20697]) ).
fof(f23110,plain,
! [X0,X1] :
( v3_borsuk_1(sK69(X0,X1),X0,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,[],[f20708]) ).
fof(f23111,plain,
! [X0,X1] :
( m2_relset_1(sK69(X0,X1),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,[],[f20708]) ).
fof(f23112,plain,
! [X0,X1] :
( v5_pre_topc(sK69(X0,X1),X0,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,[],[f20708]) ).
fof(f23113,plain,
! [X0,X1] :
( v1_funct_2(sK69(X0,X1),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,[],[f20708]) ).
fof(f23114,plain,
! [X0,X1] :
( v1_funct_1(sK69(X0,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,[],[f20708]) ).
fof(f23122,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v3_borsuk_1(X2,X0,X1)
| ~ 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)
| k1_tsp_2(X0,X1) = X2
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f20709]) ).
fof(f23136,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,[],[f20718]) ).
fof(f23148,plain,
l1_pre_topc(sK75),
inference(cnf_transformation,[],[f20719]) ).
fof(f23149,plain,
v2_pre_topc(sK75),
inference(cnf_transformation,[],[f20719]) ).
fof(f23150,plain,
~ v3_struct_0(sK75),
inference(cnf_transformation,[],[f20719]) ).
fof(f23151,plain,
m2_tsp_1(sK76,sK75),
inference(cnf_transformation,[],[f20719]) ).
fof(f23152,plain,
v2_tsp_2(sK76,sK75),
inference(cnf_transformation,[],[f20719]) ).
fof(f23153,plain,
~ v3_struct_0(sK76),
inference(cnf_transformation,[],[f20719]) ).
fof(f23154,plain,
m1_subset_1(sK77,k1_zfmisc_1(u1_struct_0(sK75))),
inference(cnf_transformation,[],[f20719]) ).
fof(f23155,plain,
v3_pre_topc(sK77,sK75),
inference(cnf_transformation,[],[f20719]) ).
fof(f23156,plain,
~ v3_pre_topc(k4_pre_topc(sK75,sK76,k4_tsp_2(sK75,sK76),sK77),sK76),
inference(cnf_transformation,[],[f20719]) ).
fof(f23383,plain,
! [X2,X0,X1] :
( k3_xboole_0(X1,X2) = k5_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f13867]) ).
fof(f23513,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v3_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| k3_tex_4(X0,X1) = X1
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f14002]) ).
fof(f23850,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f20894]) ).
fof(f23853,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f14255]) ).
fof(f24350,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),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))
| k9_relat_1(X2,X3) = k4_pre_topc(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f14478]) ).
fof(f24464,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f21037]) ).
fof(f24959,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f14891]) ).
fof(f25055,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f25255,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f15093]) ).
fof(f26347,plain,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
inference(cnf_transformation,[],[f21]) ).
fof(f26718,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k1_setfam_1(k2_tarski(X0,X1)),
inference(cnf_transformation,[],[f602]) ).
fof(f32994,plain,
! [X2,X0,X1] :
( sK63(X1,X2) = k4_xboole_0(X2,k4_xboole_0(X2,u1_struct_0(X1)))
| ~ v3_pre_topc(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(definition_unfolding,[],[f23077,f25055]) ).
fof(f33004,plain,
! [X2,X0,X1] :
( k5_subset_1(X0,X1,X2) = k4_xboole_0(X1,k4_xboole_0(X1,X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(definition_unfolding,[],[f23383,f25055]) ).
fof(f33695,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k1_setfam_1(k2_tarski(X0,X1)),
inference(definition_unfolding,[],[f26718,f25055]) ).
fof(f35112,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,[],[f23136]) ).
fof(f35113,plain,
! [X0,X1,X6] :
( ~ v1_funct_2(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))
| 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)
| ~ 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(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,[],[f35112]) ).
fof(f36714,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) = k1_setfam_1(k2_tarski(X1,X2)) ),
inference(forward_demodulation,[],[f33004,f33695]) ).
fof(f36734,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v3_pre_topc(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| sK63(X1,X2) = k1_setfam_1(k2_tarski(X2,u1_struct_0(X1)))
| ~ l1_pre_topc(X0) ),
inference(forward_demodulation,[],[f32994,f33695]) ).
fof(f37118,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK75)
| l1_pre_topc(X0) ),
inference(resolution,[],[f23853,f23148]) ).
fof(f37119,plain,
! [X0,X1] :
( ~ v3_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| v3_struct_0(sK75)
| v3_pre_topc(sK63(X1,X0),X1)
| ~ l1_pre_topc(sK75) ),
inference(resolution,[],[f23078,f23149]) ).
fof(f37120,plain,
l1_pre_topc(sK76),
inference(resolution,[],[f37118,f23151]) ).
fof(f37124,plain,
( m1_pre_topc(sK76,sK75)
| ~ l1_pre_topc(sK75) ),
inference(resolution,[],[f23850,f23151]) ).
fof(f37125,plain,
m1_pre_topc(sK76,sK75),
inference(forward_subsumption_resolution,[],[f37124,f23148]) ).
fof(f37126,plain,
( v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| k4_tsp_2(sK75,sK76) = k1_tsp_2(sK75,sK76) ),
inference(resolution,[],[f37125,f22978]) ).
fof(f37127,plain,
( v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| v1_funct_2(k4_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)) ),
inference(resolution,[],[f37125,f22976]) ).
fof(f37128,plain,
( ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| v1_funct_2(k4_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)) ),
inference(forward_subsumption_resolution,[],[f37127,f23150]) ).
fof(f37129,plain,
( ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| k4_tsp_2(sK75,sK76) = k1_tsp_2(sK75,sK76) ),
inference(forward_subsumption_resolution,[],[f37126,f23150]) ).
fof(f37130,plain,
( ~ l1_pre_topc(sK75)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| v1_funct_2(k4_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)) ),
inference(forward_subsumption_resolution,[],[f37128,f23149]) ).
fof(f37131,plain,
( ~ l1_pre_topc(sK75)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| k4_tsp_2(sK75,sK76) = k1_tsp_2(sK75,sK76) ),
inference(forward_subsumption_resolution,[],[f37129,f23149]) ).
fof(f37132,plain,
( v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| v1_funct_2(k4_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)) ),
inference(forward_subsumption_resolution,[],[f37130,f23148]) ).
fof(f37133,plain,
( v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| k4_tsp_2(sK75,sK76) = k1_tsp_2(sK75,sK76) ),
inference(forward_subsumption_resolution,[],[f37131,f23148]) ).
fof(f37134,plain,
( ~ v2_tsp_2(sK76,sK75)
| v1_funct_2(k4_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)) ),
inference(forward_subsumption_resolution,[],[f37132,f23153]) ).
fof(f37135,plain,
( ~ v2_tsp_2(sK76,sK75)
| k4_tsp_2(sK75,sK76) = k1_tsp_2(sK75,sK76) ),
inference(forward_subsumption_resolution,[],[f37133,f23153]) ).
fof(f37136,plain,
v1_funct_2(k4_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)),
inference(forward_subsumption_resolution,[],[f37134,f23152]) ).
fof(f37137,plain,
k4_tsp_2(sK75,sK76) = k1_tsp_2(sK75,sK76),
inference(forward_subsumption_resolution,[],[f37135,f23152]) ).
fof(f37138,plain,
~ v3_pre_topc(k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),sK77),sK76),
inference(superposition,[],[f23156,f37137]) ).
fof(f37143,plain,
v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)),
inference(superposition,[],[f37136,f37137]) ).
fof(f37144,plain,
! [X0] :
( ~ v3_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| v3_struct_0(sK75)
| k3_tex_4(sK75,X0) = X0
| ~ l1_pre_topc(sK75) ),
inference(resolution,[],[f23513,f23149]) ).
fof(f37145,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f25255,f24959]) ).
fof(f37146,plain,
u1_struct_0(sK75) = k2_pre_topc(sK75),
inference(resolution,[],[f37145,f23148]) ).
fof(f37147,plain,
u1_struct_0(sK76) = k2_pre_topc(sK76),
inference(resolution,[],[f37145,f37120]) ).
fof(f37148,plain,
v1_funct_2(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)),
inference(superposition,[],[f37143,f37146]) ).
fof(f37150,plain,
m1_subset_1(sK77,k1_zfmisc_1(k2_pre_topc(sK75))),
inference(superposition,[],[f23154,f37146]) ).
fof(f37151,plain,
! [X0] :
( m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(superposition,[],[f22974,f37146]) ).
fof(f37153,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m2_tsp_1(X0,sK75)
| v3_struct_0(sK75)
| ~ l1_pre_topc(sK75) ),
inference(superposition,[],[f23030,f37146]) ).
fof(f37155,plain,
! [X0] :
( m2_relset_1(sK69(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m2_tsp_1(X0,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(superposition,[],[f23111,f37146]) ).
fof(f37157,plain,
! [X0] :
( v1_funct_2(sK69(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m2_tsp_1(X0,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(superposition,[],[f23113,f37146]) ).
fof(f37162,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v1_funct_1(k4_tsp_2(sK75,X0))
| k4_pre_topc(sK75,X0,k4_tsp_2(sK75,X0),X1) = k5_subset_1(k2_pre_topc(sK75),u1_struct_0(X0),k3_tex_4(sK75,X1))
| ~ v5_pre_topc(k4_tsp_2(sK75,X0),sK75,X0)
| ~ m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m2_tsp_1(X0,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(superposition,[],[f35113,f37146]) ).
fof(f37175,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v1_funct_1(k4_tsp_2(sK75,X0))
| k4_pre_topc(sK75,X0,k4_tsp_2(sK75,X0),X1) = k5_subset_1(k2_pre_topc(sK75),u1_struct_0(X0),k3_tex_4(sK75,X1))
| ~ v5_pre_topc(k4_tsp_2(sK75,X0),sK75,X0)
| ~ m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m2_tsp_1(X0,sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37162,f23150]) ).
fof(f37192,plain,
! [X0] :
( v1_funct_2(sK69(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m2_tsp_1(X0,sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37157,f23150]) ).
fof(f37194,plain,
! [X0] :
( m2_relset_1(sK69(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m2_tsp_1(X0,sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37155,f23150]) ).
fof(f37196,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m2_tsp_1(X0,sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37153,f23150]) ).
fof(f37198,plain,
! [X0] :
( m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37151,f23150]) ).
fof(f37200,plain,
v1_funct_2(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76)),
inference(forward_demodulation,[],[f37148,f37147]) ).
fof(f37201,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v1_funct_1(k4_tsp_2(sK75,X0))
| k4_pre_topc(sK75,X0,k4_tsp_2(sK75,X0),X1) = k5_subset_1(k2_pre_topc(sK75),u1_struct_0(X0),k3_tex_4(sK75,X1))
| ~ v5_pre_topc(k4_tsp_2(sK75,X0),sK75,X0)
| ~ m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m2_tsp_1(X0,sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37175,f23149]) ).
fof(f37202,plain,
! [X0] :
( v1_funct_2(sK69(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m2_tsp_1(X0,sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37192,f23149]) ).
fof(f37203,plain,
! [X0] :
( m2_relset_1(sK69(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m2_tsp_1(X0,sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37194,f23149]) ).
fof(f37204,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK75)
| m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK75))) ),
inference(forward_subsumption_resolution,[],[f37196,f23148]) ).
fof(f37205,plain,
! [X0] :
( m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37198,f23149]) ).
fof(f37207,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v1_funct_1(k4_tsp_2(sK75,X0))
| k4_pre_topc(sK75,X0,k4_tsp_2(sK75,X0),X1) = k5_subset_1(k2_pre_topc(sK75),u1_struct_0(X0),k3_tex_4(sK75,X1))
| ~ v5_pre_topc(k4_tsp_2(sK75,X0),sK75,X0)
| ~ m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m2_tsp_1(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37201,f23148]) ).
fof(f37208,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK75)
| v3_struct_0(X0)
| v1_funct_2(sK69(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ m2_tsp_1(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37202,f23148]) ).
fof(f37209,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK75)
| v3_struct_0(X0)
| m2_relset_1(sK69(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ m2_tsp_1(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37203,f23148]) ).
fof(f37210,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK75)
| v3_struct_0(X0)
| m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37205,f23148]) ).
fof(f37211,plain,
! [X0,X1] :
( ~ v2_tsp_2(X0,sK75)
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v1_funct_1(k4_tsp_2(sK75,X0))
| k4_pre_topc(sK75,X0,k4_tsp_2(sK75,X0),X1) = k5_subset_1(k2_pre_topc(sK75),u1_struct_0(X0),k3_tex_4(sK75,X1))
| ~ v5_pre_topc(k4_tsp_2(sK75,X0),sK75,X0)
| ~ m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_funct_2(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ m2_tsp_1(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37207,f37204]) ).
fof(f37281,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v1_funct_1(k4_tsp_2(sK75,sK76))
| k4_pre_topc(sK75,sK76,k4_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0))
| ~ v5_pre_topc(k4_tsp_2(sK75,sK76),sK75,sK76)
| ~ m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| v3_struct_0(sK76)
| ~ v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m2_tsp_1(sK76,sK75) ),
inference(resolution,[],[f37211,f23152]) ).
fof(f37282,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v1_funct_1(k4_tsp_2(sK75,sK76))
| k4_pre_topc(sK75,sK76,k4_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0))
| ~ v5_pre_topc(k4_tsp_2(sK75,sK76),sK75,sK76)
| ~ m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m2_tsp_1(sK76,sK75) ),
inference(forward_subsumption_resolution,[],[f37281,f23153]) ).
fof(f37283,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v1_funct_1(k4_tsp_2(sK75,sK76))
| k4_pre_topc(sK75,sK76,k4_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0))
| ~ v5_pre_topc(k4_tsp_2(sK75,sK76),sK75,sK76)
| ~ m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)) ),
inference(forward_subsumption_resolution,[],[f37282,f23151]) ).
fof(f37284,plain,
! [X0] :
( ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| k4_pre_topc(sK75,sK76,k4_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0))
| ~ v5_pre_topc(k4_tsp_2(sK75,sK76),sK75,sK76)
| ~ m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)) ),
inference(forward_demodulation,[],[f37283,f37137]) ).
fof(f37285,plain,
! [X0] :
( k4_pre_topc(sK75,sK76,k4_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v5_pre_topc(k4_tsp_2(sK75,sK76),sK75,sK76)
| ~ m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)) ),
inference(forward_demodulation,[],[f37284,f37147]) ).
fof(f37286,plain,
! [X0] :
( k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v5_pre_topc(k4_tsp_2(sK75,sK76),sK75,sK76)
| ~ m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)) ),
inference(forward_demodulation,[],[f37285,f37137]) ).
fof(f37287,plain,
! [X0] :
( ~ v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76)
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)) ),
inference(forward_demodulation,[],[f37286,f37137]) ).
fof(f37288,plain,
! [X0] :
( ~ m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76)
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)) ),
inference(forward_demodulation,[],[f37287,f37147]) ).
fof(f37289,plain,
! [X0] :
( ~ m2_relset_1(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76)
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)) ),
inference(forward_demodulation,[],[f37288,f37137]) ).
fof(f37290,plain,
! [X0] :
( ~ v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76)
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75))) ),
inference(forward_demodulation,[],[f37289,f37147]) ).
fof(f37291,plain,
! [X0] :
( ~ v1_funct_2(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76)
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75))) ),
inference(forward_demodulation,[],[f37290,f37137]) ).
fof(f37292,plain,
! [X0] :
( ~ m2_relset_1(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76)
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75))) ),
inference(forward_subsumption_resolution,[],[f37291,f37200]) ).
fof(f37294,definition,
( spl1369_59
<=> v1_funct_1(k1_tsp_2(sK75,sK76)) ),
introduced(definition,[new_symbols(definition,[spl1369_59])],[avatar_definition]) ).
fof(f37295,plain,
( ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| spl1369_59 ),
inference(avatar_component_clause,[],[f37294]) ).
fof(f37297,definition,
( spl1369_60
<=> ! [X0] :
( k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75))) ) ),
introduced(definition,[new_symbols(definition,[spl1369_60])],[avatar_definition]) ).
fof(f37298,plain,
( ! [X0] :
( k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75))) )
| ~ spl1369_60 ),
inference(avatar_component_clause,[],[f37297]) ).
fof(f37300,definition,
( spl1369_61
<=> v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76) ),
introduced(definition,[new_symbols(definition,[spl1369_61])],[avatar_definition]) ).
fof(f37301,plain,
( ~ v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76)
| spl1369_61 ),
inference(avatar_component_clause,[],[f37300]) ).
fof(f37303,definition,
( spl1369_62
<=> m2_relset_1(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76)) ),
introduced(definition,[new_symbols(definition,[spl1369_62])],[avatar_definition]) ).
fof(f37304,plain,
( ~ m2_relset_1(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| spl1369_62 ),
inference(avatar_component_clause,[],[f37303]) ).
fof(f37305,plain,
( ~ spl1369_59
| spl1369_60
| ~ spl1369_61
| ~ spl1369_62 ),
inference(avatar_split_clause,[],[f37292,f37303,f37300,f37297,f37294]) ).
fof(f37306,plain,
! [X0,X1] :
( ~ v3_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| v3_struct_0(sK75)
| sK63(X1,X0) = k1_setfam_1(k2_tarski(X0,u1_struct_0(X1)))
| ~ l1_pre_topc(sK75) ),
inference(resolution,[],[f36734,f23149]) ).
fof(f37307,plain,
! [X0] :
( v3_struct_0(sK75)
| v5_pre_topc(k4_tsp_2(sK75,X0),sK75,X0)
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(resolution,[],[f22975,f23149]) ).
fof(f37308,plain,
! [X0] :
( v5_pre_topc(k4_tsp_2(sK75,X0),sK75,X0)
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37307,f23150]) ).
fof(f37309,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK75)
| v3_struct_0(X0)
| v5_pre_topc(k4_tsp_2(sK75,X0),sK75,X0)
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37308,f23148]) ).
fof(f37310,plain,
( v3_struct_0(sK76)
| v1_funct_2(sK69(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m2_tsp_1(sK76,sK75) ),
inference(resolution,[],[f37208,f23152]) ).
fof(f37311,plain,
( v1_funct_2(sK69(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m2_tsp_1(sK76,sK75) ),
inference(forward_subsumption_resolution,[],[f37310,f23153]) ).
fof(f37312,plain,
v1_funct_2(sK69(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)),
inference(forward_subsumption_resolution,[],[f37311,f23151]) ).
fof(f37313,plain,
v1_funct_2(sK69(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76)),
inference(forward_demodulation,[],[f37312,f37147]) ).
fof(f37314,plain,
( v3_struct_0(sK76)
| m2_relset_1(sK69(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m2_tsp_1(sK76,sK75) ),
inference(resolution,[],[f37209,f23152]) ).
fof(f37315,plain,
( m2_relset_1(sK69(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m2_tsp_1(sK76,sK75) ),
inference(forward_subsumption_resolution,[],[f37314,f23153]) ).
fof(f37316,plain,
m2_relset_1(sK69(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)),
inference(forward_subsumption_resolution,[],[f37315,f23151]) ).
fof(f37317,plain,
m2_relset_1(sK69(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76)),
inference(forward_demodulation,[],[f37316,f37147]) ).
fof(f37318,plain,
( v3_struct_0(sK76)
| v5_pre_topc(k4_tsp_2(sK75,sK76),sK75,sK76)
| ~ m1_pre_topc(sK76,sK75) ),
inference(resolution,[],[f37309,f23152]) ).
fof(f37319,plain,
( v5_pre_topc(k4_tsp_2(sK75,sK76),sK75,sK76)
| ~ m1_pre_topc(sK76,sK75) ),
inference(forward_subsumption_resolution,[],[f37318,f23153]) ).
fof(f37320,plain,
v5_pre_topc(k4_tsp_2(sK75,sK76),sK75,sK76),
inference(forward_subsumption_resolution,[],[f37319,f37125]) ).
fof(f37321,plain,
v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76),
inference(forward_demodulation,[],[f37320,f37137]) ).
fof(f37339,plain,
! [X2,X3,X0,X1] :
( ~ l1_struct_0(X2)
| ~ l1_struct_0(X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| k9_relat_1(X0,X3) = k4_pre_topc(X1,X2,X0,X3) ),
inference(resolution,[],[f24464,f24350]) ).
fof(f37340,plain,
! [X2,X3,X0,X1] :
( ~ l1_struct_0(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X2))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X2))
| k9_relat_1(X1,X3) = k4_pre_topc(X0,X2,X1,X3)
| ~ l1_pre_topc(X2) ),
inference(resolution,[],[f37339,f24959]) ).
fof(f37341,plain,
! [X2,X3,X0,X1] :
( ~ l1_pre_topc(X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| k9_relat_1(X0,X3) = k4_pre_topc(X1,X2,X0,X3)
| ~ l1_pre_topc(X2)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(resolution,[],[f37340,f24959]) ).
fof(f37342,plain,
! [X2,X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK75),u1_struct_0(X1))
| k9_relat_1(X0,X2) = k4_pre_topc(sK75,X1,X0,X2)
| ~ l1_pre_topc(X1)
| ~ m2_relset_1(X0,u1_struct_0(sK75),u1_struct_0(X1)) ),
inference(resolution,[],[f37341,f23148]) ).
fof(f37345,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK75),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| k9_relat_1(X0,X2) = k4_pre_topc(sK75,X1,X0,X2)
| ~ l1_pre_topc(X1)
| ~ m2_relset_1(X0,u1_struct_0(sK75),u1_struct_0(X1)) ),
inference(forward_demodulation,[],[f37342,f37146]) ).
fof(f37347,plain,
! [X2,X0,X1] :
( ~ l1_pre_topc(X1)
| ~ v1_funct_2(X0,k2_pre_topc(sK75),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| k9_relat_1(X0,X2) = k4_pre_topc(sK75,X1,X0,X2)
| ~ m2_relset_1(X0,k2_pre_topc(sK75),u1_struct_0(X1)) ),
inference(forward_demodulation,[],[f37345,f37146]) ).
fof(f37349,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ v1_funct_1(X0)
| k9_relat_1(X0,X1) = k4_pre_topc(sK75,sK76,X0,X1)
| ~ m2_relset_1(X0,k2_pre_topc(sK75),u1_struct_0(sK76)) ),
inference(resolution,[],[f37347,f37120]) ).
fof(f37350,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ v1_funct_1(X0)
| k9_relat_1(X0,X1) = k4_pre_topc(sK75,sK76,X0,X1)
| ~ m2_relset_1(X0,k2_pre_topc(sK75),u1_struct_0(sK76)) ),
inference(forward_demodulation,[],[f37349,f37147]) ).
fof(f37352,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ m2_relset_1(X0,k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ v1_funct_1(X0)
| k9_relat_1(X0,X1) = k4_pre_topc(sK75,sK76,X0,X1) ),
inference(forward_demodulation,[],[f37350,f37147]) ).
fof(f37354,plain,
( v3_struct_0(sK76)
| m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m1_pre_topc(sK76,sK75) ),
inference(resolution,[],[f37210,f23152]) ).
fof(f37355,plain,
( m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m1_pre_topc(sK76,sK75) ),
inference(forward_subsumption_resolution,[],[f37354,f23153]) ).
fof(f37356,plain,
m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)),
inference(forward_subsumption_resolution,[],[f37355,f37125]) ).
fof(f37357,plain,
m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76)),
inference(forward_demodulation,[],[f37356,f37147]) ).
fof(f37358,plain,
m2_relset_1(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76)),
inference(forward_demodulation,[],[f37357,f37137]) ).
fof(f37391,plain,
m1_subset_1(u1_struct_0(sK76),k1_zfmisc_1(k2_pre_topc(sK75))),
inference(resolution,[],[f37204,f23151]) ).
fof(f37392,plain,
m1_subset_1(k2_pre_topc(sK76),k1_zfmisc_1(k2_pre_topc(sK75))),
inference(forward_demodulation,[],[f37391,f37147]) ).
fof(f37393,plain,
! [X0,X1] :
( ~ v3_borsuk_1(X0,sK75,X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK75),u1_struct_0(X1))
| ~ v5_pre_topc(X0,sK75,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK75),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| v3_struct_0(sK75)
| k1_tsp_2(sK75,X1) = X0
| ~ l1_pre_topc(sK75) ),
inference(resolution,[],[f23122,f23149]) ).
fof(f37394,plain,
! [X0] :
( ~ m2_relset_1(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k9_relat_1(k1_tsp_2(sK75,sK76),X0) ),
inference(resolution,[],[f37200,f37352]) ).
fof(f37405,plain,
! [X0,X1] :
( ~ v3_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| v3_pre_topc(sK63(X1,X0),X1)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37119,f23150]) ).
fof(f37406,plain,
! [X0] :
( ~ v3_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k3_tex_4(sK75,X0) = X0
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37144,f23150]) ).
fof(f37407,plain,
! [X0,X1] :
( ~ v3_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| sK63(X1,X0) = k1_setfam_1(k2_tarski(X0,u1_struct_0(X1)))
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37306,f23150]) ).
fof(f37411,plain,
! [X0,X1] :
( ~ v3_borsuk_1(X0,sK75,X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK75),u1_struct_0(X1))
| ~ v5_pre_topc(X0,sK75,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK75),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| k1_tsp_2(sK75,X1) = X0
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37393,f23150]) ).
fof(f37412,plain,
! [X0,X1] :
( ~ v3_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| v3_pre_topc(sK63(X1,X0),X1) ),
inference(forward_subsumption_resolution,[],[f37405,f23148]) ).
fof(f37413,plain,
! [X0] :
( ~ v3_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k3_tex_4(sK75,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f37406,f23148]) ).
fof(f37414,plain,
! [X0,X1] :
( ~ v3_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| sK63(X1,X0) = k1_setfam_1(k2_tarski(X0,u1_struct_0(X1))) ),
inference(forward_subsumption_resolution,[],[f37407,f23148]) ).
fof(f37418,plain,
! [X0,X1] :
( ~ v3_borsuk_1(X0,sK75,X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK75),u1_struct_0(X1))
| ~ v5_pre_topc(X0,sK75,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK75),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| k1_tsp_2(sK75,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f37411,f23148]) ).
fof(f37419,plain,
! [X0,X1] :
( v3_pre_topc(sK63(X1,X0),X1)
| ~ v3_pre_topc(X0,sK75)
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75))) ),
inference(forward_demodulation,[],[f37412,f37146]) ).
fof(f37420,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v3_pre_topc(X0,sK75)
| k3_tex_4(sK75,X0) = X0 ),
inference(forward_demodulation,[],[f37413,f37146]) ).
fof(f37421,plain,
! [X0,X1] :
( ~ v2_tsp_2(X1,sK75)
| ~ v3_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m2_tsp_1(X1,sK75)
| sK63(X1,X0) = k1_setfam_1(k2_tarski(X0,u1_struct_0(X1))) ),
inference(forward_demodulation,[],[f37414,f37146]) ).
fof(f37425,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK75),u1_struct_0(X1))
| ~ v3_borsuk_1(X0,sK75,X1)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK75,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK75),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| k1_tsp_2(sK75,X1) = X0 ),
inference(forward_demodulation,[],[f37418,f37146]) ).
fof(f37426,plain,
! [X0,X1] :
( ~ v2_tsp_2(X1,sK75)
| ~ v1_funct_2(X0,k2_pre_topc(sK75),u1_struct_0(X1))
| ~ v3_borsuk_1(X0,sK75,X1)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK75,X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X0,k2_pre_topc(sK75),u1_struct_0(X1))
| ~ m2_tsp_1(X1,sK75)
| k1_tsp_2(sK75,X1) = X0 ),
inference(forward_demodulation,[],[f37425,f37146]) ).
fof(f37427,plain,
( ~ v3_pre_topc(sK77,sK75)
| sK77 = k3_tex_4(sK75,sK77) ),
inference(resolution,[],[f37420,f37150]) ).
fof(f37436,plain,
sK77 = k3_tex_4(sK75,sK77),
inference(forward_subsumption_resolution,[],[f37427,f23155]) ).
fof(f37444,plain,
! [X0] :
( ~ v3_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m2_tsp_1(sK76,sK75)
| sK63(sK76,X0) = k1_setfam_1(k2_tarski(X0,u1_struct_0(sK76))) ),
inference(resolution,[],[f37421,f23152]) ).
fof(f37445,plain,
! [X0] :
( ~ v3_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| sK63(sK76,X0) = k1_setfam_1(k2_tarski(X0,u1_struct_0(sK76))) ),
inference(forward_subsumption_resolution,[],[f37444,f23151]) ).
fof(f37446,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v3_pre_topc(X0,sK75)
| sK63(sK76,X0) = k1_setfam_1(k2_tarski(X0,k2_pre_topc(sK76))) ),
inference(forward_demodulation,[],[f37445,f37147]) ).
fof(f37447,plain,
( ~ v3_pre_topc(sK77,sK75)
| sK63(sK76,sK77) = k1_setfam_1(k2_tarski(sK77,k2_pre_topc(sK76))) ),
inference(resolution,[],[f37446,f37150]) ).
fof(f37449,plain,
sK63(sK76,sK77) = k1_setfam_1(k2_tarski(sK77,k2_pre_topc(sK76))),
inference(forward_subsumption_resolution,[],[f37447,f23155]) ).
fof(f37454,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ v3_borsuk_1(X0,sK75,sK76)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK75,sK76)
| v3_struct_0(sK76)
| ~ m2_relset_1(X0,k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m2_tsp_1(sK76,sK75)
| k1_tsp_2(sK75,sK76) = X0 ),
inference(resolution,[],[f37426,f23152]) ).
fof(f37455,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ v3_borsuk_1(X0,sK75,sK76)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK75,sK76)
| ~ m2_relset_1(X0,k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m2_tsp_1(sK76,sK75)
| k1_tsp_2(sK75,sK76) = X0 ),
inference(forward_subsumption_resolution,[],[f37454,f23153]) ).
fof(f37456,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ v3_borsuk_1(X0,sK75,sK76)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK75,sK76)
| ~ m2_relset_1(X0,k2_pre_topc(sK75),u1_struct_0(sK76))
| k1_tsp_2(sK75,sK76) = X0 ),
inference(forward_subsumption_resolution,[],[f37455,f23151]) ).
fof(f37457,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ v3_borsuk_1(X0,sK75,sK76)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK75,sK76)
| ~ m2_relset_1(X0,k2_pre_topc(sK75),u1_struct_0(sK76))
| k1_tsp_2(sK75,sK76) = X0 ),
inference(forward_demodulation,[],[f37456,f37147]) ).
fof(f37458,plain,
! [X0] :
( ~ v3_borsuk_1(X0,sK75,sK76)
| ~ v1_funct_2(X0,k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ m2_relset_1(X0,k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK75,sK76)
| k1_tsp_2(sK75,sK76) = X0 ),
inference(forward_demodulation,[],[f37457,f37147]) ).
fof(f37467,plain,
( ~ v1_funct_2(sK69(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ m2_relset_1(sK69(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ v1_funct_1(sK69(sK75,sK76))
| ~ v5_pre_topc(sK69(sK75,sK76),sK75,sK76)
| k1_tsp_2(sK75,sK76) = sK69(sK75,sK76)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(resolution,[],[f37458,f23110]) ).
fof(f37468,plain,
( ~ v1_funct_2(sK69(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ m2_relset_1(sK69(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ v5_pre_topc(sK69(sK75,sK76),sK75,sK76)
| k1_tsp_2(sK75,sK76) = sK69(sK75,sK76)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37467,f23114]) ).
fof(f37469,plain,
( ~ v1_funct_2(sK69(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| ~ m2_relset_1(sK69(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| k1_tsp_2(sK75,sK76) = sK69(sK75,sK76)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37468,f23112]) ).
fof(f37470,plain,
( ~ m2_relset_1(sK69(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| k1_tsp_2(sK75,sK76) = sK69(sK75,sK76)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37469,f37313]) ).
fof(f37471,plain,
( k1_tsp_2(sK75,sK76) = sK69(sK75,sK76)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37470,f37317]) ).
fof(f37472,plain,
( k1_tsp_2(sK75,sK76) = sK69(sK75,sK76)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37471,f23153]) ).
fof(f37473,plain,
( k1_tsp_2(sK75,sK76) = sK69(sK75,sK76)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37472,f23152]) ).
fof(f37474,plain,
( k1_tsp_2(sK75,sK76) = sK69(sK75,sK76)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37473,f23151]) ).
fof(f37475,plain,
( k1_tsp_2(sK75,sK76) = sK69(sK75,sK76)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37474,f23150]) ).
fof(f37476,plain,
( k1_tsp_2(sK75,sK76) = sK69(sK75,sK76)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37475,f23149]) ).
fof(f37477,plain,
k1_tsp_2(sK75,sK76) = sK69(sK75,sK76),
inference(forward_subsumption_resolution,[],[f37476,f23148]) ).
fof(f37483,plain,
( v1_funct_1(k1_tsp_2(sK75,sK76))
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(superposition,[],[f23114,f37477]) ).
fof(f37485,plain,
( v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| spl1369_59 ),
inference(forward_subsumption_resolution,[],[f37483,f37295]) ).
fof(f37488,plain,
( ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| spl1369_59 ),
inference(forward_subsumption_resolution,[],[f37485,f23153]) ).
fof(f37491,plain,
( ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| spl1369_59 ),
inference(forward_subsumption_resolution,[],[f37488,f23152]) ).
fof(f37494,plain,
( v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| spl1369_59 ),
inference(forward_subsumption_resolution,[],[f37491,f23151]) ).
fof(f37497,plain,
( ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| spl1369_59 ),
inference(forward_subsumption_resolution,[],[f37494,f23150]) ).
fof(f37500,plain,
( ~ l1_pre_topc(sK75)
| spl1369_59 ),
inference(forward_subsumption_resolution,[],[f37497,f23149]) ).
fof(f37503,plain,
( $false
| spl1369_59 ),
inference(forward_subsumption_resolution,[],[f37500,f23148]) ).
fof(f37504,plain,
spl1369_59,
inference(avatar_contradiction_clause,[],[f37503]) ).
fof(f37507,plain,
( $false
| spl1369_61 ),
inference(forward_subsumption_resolution,[],[f37301,f37321]) ).
fof(f37508,plain,
spl1369_61,
inference(avatar_contradiction_clause,[],[f37507]) ).
fof(f37509,plain,
! [X0] :
( ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k9_relat_1(k1_tsp_2(sK75,sK76),X0) ),
inference(forward_subsumption_resolution,[],[f37394,f37358]) ).
fof(f37512,definition,
( spl1369_67
<=> ! [X0] : k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k9_relat_1(k1_tsp_2(sK75,sK76),X0) ),
introduced(definition,[new_symbols(definition,[spl1369_67])],[avatar_definition]) ).
fof(f37513,plain,
( ! [X0] : k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k9_relat_1(k1_tsp_2(sK75,sK76),X0)
| ~ spl1369_67 ),
inference(avatar_component_clause,[],[f37512]) ).
fof(f37514,plain,
( spl1369_67
| ~ spl1369_59 ),
inference(avatar_split_clause,[],[f37509,f37294,f37512]) ).
fof(f37520,plain,
( $false
| spl1369_62 ),
inference(forward_subsumption_resolution,[],[f37304,f37358]) ).
fof(f37521,plain,
spl1369_62,
inference(avatar_contradiction_clause,[],[f37520]) ).
fof(f37522,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0)) = k9_relat_1(k1_tsp_2(sK75,sK76),X0) )
| ~ spl1369_60
| ~ spl1369_67 ),
inference(forward_demodulation,[],[f37298,f37513]) ).
fof(f37524,plain,
( ~ v3_pre_topc(k9_relat_1(k1_tsp_2(sK75,sK76),sK77),sK76)
| ~ spl1369_67 ),
inference(superposition,[],[f37138,f37513]) ).
fof(f37543,plain,
( k9_relat_1(k1_tsp_2(sK75,sK76),sK77) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,sK77))
| ~ spl1369_60
| ~ spl1369_67 ),
inference(resolution,[],[f37522,f37150]) ).
fof(f37545,plain,
( k9_relat_1(k1_tsp_2(sK75,sK76),sK77) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),sK77)
| ~ spl1369_60
| ~ spl1369_67 ),
inference(forward_demodulation,[],[f37543,f37436]) ).
fof(f37921,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| k5_subset_1(k2_pre_topc(sK75),X0,sK77) = k1_setfam_1(k2_tarski(X0,sK77)) ),
inference(resolution,[],[f36714,f37150]) ).
fof(f37927,plain,
k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),sK77) = k1_setfam_1(k2_tarski(k2_pre_topc(sK76),sK77)),
inference(resolution,[],[f37921,f37392]) ).
fof(f37930,plain,
k1_setfam_1(k2_tarski(sK77,k2_pre_topc(sK76))) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),sK77),
inference(forward_demodulation,[],[f37927,f26347]) ).
fof(f37932,plain,
( k1_setfam_1(k2_tarski(sK77,k2_pre_topc(sK76))) = k9_relat_1(k1_tsp_2(sK75,sK76),sK77)
| ~ spl1369_60
| ~ spl1369_67 ),
inference(forward_demodulation,[],[f37930,f37545]) ).
fof(f37933,plain,
( sK63(sK76,sK77) = k9_relat_1(k1_tsp_2(sK75,sK76),sK77)
| ~ spl1369_60
| ~ spl1369_67 ),
inference(forward_demodulation,[],[f37932,f37449]) ).
fof(f37935,plain,
( ~ v3_pre_topc(sK63(sK76,sK77),sK76)
| ~ spl1369_60
| ~ spl1369_67 ),
inference(superposition,[],[f37524,f37933]) ).
fof(f37942,plain,
( ~ v3_pre_topc(sK77,sK75)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| ~ m1_subset_1(sK77,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ spl1369_60
| ~ spl1369_67 ),
inference(resolution,[],[f37935,f37419]) ).
fof(f37945,plain,
( ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| ~ m1_subset_1(sK77,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ spl1369_60
| ~ spl1369_67 ),
inference(forward_subsumption_resolution,[],[f37942,f23155]) ).
fof(f37946,plain,
( ~ m2_tsp_1(sK76,sK75)
| ~ m1_subset_1(sK77,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ spl1369_60
| ~ spl1369_67 ),
inference(forward_subsumption_resolution,[],[f37945,f23152]) ).
fof(f37947,plain,
( ~ m1_subset_1(sK77,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ spl1369_60
| ~ spl1369_67 ),
inference(forward_subsumption_resolution,[],[f37946,f23151]) ).
fof(f37948,plain,
( $false
| ~ spl1369_60
| ~ spl1369_67 ),
inference(forward_subsumption_resolution,[],[f37947,f37150]) ).
fof(f37949,plain,
( ~ spl1369_60
| ~ spl1369_67 ),
inference(avatar_contradiction_clause,[],[f37948]) ).
cnf(s39,plain,
( ~ spl1369_59
| spl1369_60
| ~ spl1369_61
| ~ spl1369_62 ),
inference(sat_conversion,[],[f37305]) ).
cnf(s52,plain,
spl1369_59,
inference(sat_conversion,[],[f37504]) ).
cnf(s53,plain,
spl1369_61,
inference(sat_conversion,[],[f37508]) ).
cnf(s54,plain,
( ~ spl1369_59
| spl1369_67 ),
inference(sat_conversion,[],[f37514]) ).
cnf(s55,plain,
spl1369_62,
inference(sat_conversion,[],[f37521]) ).
cnf(s68,plain,
( ~ spl1369_60
| ~ spl1369_67 ),
inference(sat_conversion,[],[f37949]) ).
cnf(s72,plain,
spl1369_67,
inference(rat,[],[s54,s52]) ).
cnf(s73,plain,
~ spl1369_60,
inference(rat,[],[s68,s72]) ).
cnf(s76,plain,
$false,
inference(rat,[],[s39,s55,s53,s73,s52]) ).
fof(f37950,plain,
$false,
inference(avatar_sat_refutation,[],[s76]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : TOP041+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.19 % Computer : n003.cluster.edu
% 0.12/0.19 % Model : x86_64 x86_64
% 0.12/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.19 % Memory : 8046.5625MB
% 0.12/0.19 % OS : Linux 6.8.0-71-generic
% 0.12/0.19 % CPULimit : 300
% 0.12/0.19 % WCLimit : 300
% 0.12/0.19 % DateTime : Mon Sep 28 19:03:59 UTC 2026
% 0.12/0.19 % CPUTime :
% 0.12/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.23 Running first-order theorem proving
% 0.12/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.91/2.98 % (1883271)Detected formulas, will run a generic FOF schedule.
% 11.91/2.98 % (1883279)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=748508020:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 11.91/2.98 % (1883281)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3671623113:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 11.91/2.98 % (1883280)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3267101213:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 11.91/2.98 % (1883276)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1488210793:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 11.91/2.98 % (1883278)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=158845978:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 11.91/2.98 % (1883282)dis-21_1_sil=8000:lcm=predicate:random_seed=4078524463:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 11.91/2.98 % (1883277)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3022887018:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 11.91/2.98 % (1883279)Instruction limit reached!
% 11.91/2.98 % (1883279)------------------------------
% 11.91/2.98 % (1883279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.91/2.98 % (1883279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.91/2.98 % (1883279)CaDiCaL version: 2.1.3
% 11.91/2.98 % (1883279)Termination reason: Instruction limit
% 11.91/2.98 % (1883279)Time elapsed: 0.051 s
% 11.91/2.98 % (1883279)Peak memory usage: 107 MB
% 11.91/2.98 % (1883279)Instructions burned: 111 (million)
% 11.91/2.98 % (1883281)Instruction limit reached!
% 11.91/2.98 % (1883281)------------------------------
% 11.91/2.98 % (1883281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.91/2.98 % (1883281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.91/2.98 % (1883281)CaDiCaL version: 2.1.3
% 11.91/2.98 % (1883281)Termination reason: Instruction limit
% 11.91/2.98 % (1883281)Termination phase: Property scanning
% 11.91/2.98 % (1883281)Time elapsed: 0.058 s
% 11.91/2.98 % (1883281)Peak memory usage: 102 MB
% 11.91/2.98 % (1883281)Instructions burned: 141 (million)
% 11.91/2.98 % (1883282)Instruction limit reached!
% 11.91/2.98 % (1883282)------------------------------
% 11.91/2.98 % (1883282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.91/2.98 % (1883282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.91/2.98 % (1883282)CaDiCaL version: 2.1.3
% 11.91/2.98 % (1883282)Termination reason: Instruction limit
% 11.91/2.98 % (1883282)Termination phase: Preprocessing 1
% 11.91/2.98 % (1883282)Time elapsed: 0.094 s
% 11.91/2.98 % (1883282)Peak memory usage: 103 MB
% 11.91/2.98 % (1883282)Instructions burned: 129 (million)
% 11.91/2.98 % (1883280)Instruction limit reached!
% 11.91/2.98 % (1883280)------------------------------
% 11.91/2.98 % (1883280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.91/2.98 % (1883280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.91/2.98 % (1883280)CaDiCaL version: 2.1.3
% 11.91/2.98 % (1883280)Termination reason: Instruction limit
% 11.91/2.98 % (1883280)Termination phase: Preprocessing 3
% 11.91/2.98 % (1883280)Time elapsed: 0.103 s
% 11.91/2.98 % (1883280)Peak memory usage: 105 MB
% 11.91/2.98 % (1883280)Instructions burned: 120 (million)
% 11.91/2.98 % (1883290)lrs+10_1_sil=8000:sp=occurrence:random_seed=1943390160:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 11.91/2.98 % (1883291)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1003382050:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 11.91/2.98 % (1883292)lrs+1011_1_sil=32000:sp=occurrence:random_seed=307425347:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 11.91/2.98 % (1883290)Instruction limit reached!
% 11.91/2.98 % (1883290)------------------------------
% 11.91/2.98 % (1883290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.91/2.98 % (1883290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/4.03 % (1883290)CaDiCaL version: 2.1.3
% 19.41/4.03 % (1883290)Termination reason: Instruction limit
% 19.41/4.03 % (1883290)Termination phase: Saturation
% 19.41/4.03 % (1883290)Time elapsed: 0.110 s
% 19.41/4.03 % (1883290)Peak memory usage: 110 MB
% 19.41/4.03 % (1883290)Instructions burned: 286 (million)
% 19.41/4.03 % (1883293)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2757650725:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 19.41/4.03 % (1883291)Instruction limit reached!
% 19.41/4.03 % (1883291)------------------------------
% 19.41/4.03 % (1883291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/4.03 % (1883291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/4.03 % (1883291)CaDiCaL version: 2.1.3
% 19.41/4.03 % (1883291)Termination reason: Instruction limit
% 19.41/4.03 % (1883291)Termination phase: Property scanning
% 19.41/4.03 % (1883291)Time elapsed: 0.068 s
% 19.41/4.03 % (1883291)Peak memory usage: 102 MB
% 19.41/4.03 % (1883291)Instructions burned: 158 (million)
% 19.41/4.03 % (1883297)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3931890278:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 19.41/4.03 % (1883293)Instruction limit reached!
% 19.41/4.03 % (1883293)------------------------------
% 19.41/4.03 % (1883293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/4.03 % (1883293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/4.03 % (1883293)CaDiCaL version: 2.1.3
% 19.41/4.03 % (1883293)Termination reason: Instruction limit
% 19.41/4.03 % (1883293)Termination phase: SInE selection
% 19.41/4.03 % (1883293)Time elapsed: 0.129 s
% 19.41/4.03 % (1883293)Peak memory usage: 103 MB
% 19.41/4.03 % (1883293)Instructions burned: 249 (million)
% 19.41/4.03 % (1883299)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2706509200:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 19.41/4.03 % (1883297)Instruction limit reached!
% 19.41/4.03 % (1883297)------------------------------
% 19.41/4.03 % (1883297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/4.03 % (1883297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/4.03 % (1883297)CaDiCaL version: 2.1.3
% 19.41/4.03 % (1883297)Termination reason: Instruction limit
% 19.41/4.03 % (1883297)Termination phase: Saturation
% 19.41/4.03 % (1883297)Time elapsed: 0.104 s
% 19.41/4.03 % (1883297)Peak memory usage: 110 MB
% 19.41/4.03 % (1883297)Instructions burned: 295 (million)
% 19.41/4.03 % (1883292)Instruction limit reached!
% 19.41/4.03 % (1883292)------------------------------
% 19.41/4.03 % (1883292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/4.03 % (1883292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/4.03 % (1883292)CaDiCaL version: 2.1.3
% 19.41/4.03 % (1883292)Termination reason: Instruction limit
% 19.41/4.03 % (1883292)Termination phase: Saturation
% 19.41/4.03 % (1883292)Time elapsed: 0.232 s
% 19.41/4.03 % (1883292)Peak memory usage: 109 MB
% 19.41/4.03 % (1883292)Instructions burned: 326 (million)
% 19.41/4.03 % (1883301)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1996863128:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 19.41/4.03 % (1883303)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3726761032:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 19.41/4.03 % (1883304)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3884297222:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 19.41/4.03 % (1883301)Instruction limit reached!
% 19.41/4.03 % (1883301)------------------------------
% 19.41/4.03 % (1883301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/4.03 % (1883301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/4.03 % (1883301)CaDiCaL version: 2.1.3
% 19.41/4.03 % (1883301)Termination reason: Instruction limit
% 19.41/4.03 % (1883301)Termination phase: Preprocessing 2
% 19.41/4.03 % (1883301)Time elapsed: 0.097 s
% 19.41/4.03 % (1883301)Peak memory usage: 105 MB
% 19.41/4.03 % (1883301)Instructions burned: 114 (million)
% 19.41/4.03 % (1883303)Instruction limit reached!
% 19.41/4.03 % (1883303)------------------------------
% 19.41/4.03 % (1883303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/4.03 % (1883303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/5.47 % (1883303)CaDiCaL version: 2.1.3
% 26.48/5.47 % (1883303)Termination reason: Instruction limit
% 26.48/5.47 % (1883303)Termination phase: Preprocessing 2
% 26.48/5.47 % (1883303)Time elapsed: 0.058 s
% 26.48/5.47 % (1883303)Peak memory usage: 106 MB
% 26.48/5.47 % (1883303)Instructions burned: 127 (million)
% 26.48/5.47 % (1883304)Instruction limit reached!
% 26.48/5.47 % (1883304)------------------------------
% 26.48/5.47 % (1883304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.48/5.47 % (1883304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/5.47 % (1883304)CaDiCaL version: 2.1.3
% 26.48/5.47 % (1883304)Termination reason: Instruction limit
% 26.48/5.47 % (1883304)Termination phase: Property scanning
% 26.48/5.47 % (1883304)Time elapsed: 0.051 s
% 26.48/5.47 % (1883304)Peak memory usage: 102 MB
% 26.48/5.47 % (1883304)Instructions burned: 114 (million)
% 26.48/5.47 % (1883309)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1191371343:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 26.48/5.47 % (1883308)lrs+10_1_sil=8000:sp=occurrence:random_seed=3912849406:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 26.48/5.47 % (1883310)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1635682340:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 26.48/5.47 % (1883309)Instruction limit reached!
% 26.48/5.47 % (1883309)------------------------------
% 26.48/5.47 % (1883309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.48/5.47 % (1883309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/5.47 % (1883309)CaDiCaL version: 2.1.3
% 26.48/5.47 % (1883309)Termination reason: Instruction limit
% 26.48/5.47 % (1883309)Termination phase: Saturation
% 26.48/5.47 % (1883309)Time elapsed: 0.147 s
% 26.48/5.47 % (1883309)Peak memory usage: 111 MB
% 26.48/5.47 % (1883309)Instructions burned: 440 (million)
% 26.48/5.47 % (1883314)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=419774680:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 26.48/5.47 % (1883314)Instruction limit reached!
% 26.48/5.47 % (1883314)------------------------------
% 26.48/5.47 % (1883314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.48/5.47 % (1883314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/5.47 % (1883314)CaDiCaL version: 2.1.3
% 26.48/5.47 % (1883314)Termination reason: Instruction limit
% 26.48/5.47 % (1883314)Termination phase: Property scanning
% 26.48/5.47 % (1883314)Time elapsed: 0.061 s
% 26.48/5.47 % (1883314)Peak memory usage: 107 MB
% 26.48/5.47 % (1883314)Instructions burned: 139 (million)
% 26.48/5.47 % (1883316)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3988625378:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 26.48/5.47 % (1883308)Instruction limit reached!
% 26.48/5.47 % (1883308)------------------------------
% 26.48/5.47 % (1883308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.48/5.47 % (1883308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/5.47 % (1883308)CaDiCaL version: 2.1.3
% 26.48/5.47 % (1883308)Termination reason: Instruction limit
% 26.48/5.47 % (1883308)Termination phase: Saturation
% 26.48/5.47 % (1883308)Time elapsed: 0.517 s
% 26.48/5.47 % (1883308)Peak memory usage: 121 MB
% 26.48/5.47 % (1883308)Instructions burned: 908 (million)
% 26.48/5.47 % (1883316)Instruction limit reached!
% 26.48/5.47 % (1883316)------------------------------
% 26.48/5.47 % (1883316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.48/5.47 % (1883316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/5.47 % (1883316)CaDiCaL version: 2.1.3
% 26.48/5.47 % (1883316)Termination reason: Instruction limit
% 26.48/5.47 % (1883316)Termination phase: Property scanning
% 26.48/5.47 % (1883316)Time elapsed: 0.223 s
% 26.48/5.47 % (1883316)Peak memory usage: 121 MB
% 26.48/5.47 % (1883316)Instructions burned: 597 (million)
% 26.48/5.47 % (1883318)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2209918501:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 26.48/5.47 % (1883319)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1868414241:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/125Mi)
% 26.48/5.47 % (1883319)Instruction limit reached!
% 26.48/5.47 % (1883319)------------------------------
% 26.48/5.47 % (1883319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.48/5.47 % (1883319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/5.47 % (1883319)CaDiCaL version: 2.1.3
% 26.48/5.47 % (1883319)Termination reason: Instruction limit
% 26.48/5.47 % (1883319)Termination phase: Property scanning
% 26.48/5.47 % (1883319)Time elapsed: 0.029 s
% 26.48/5.47 % (1883319)Peak memory usage: 102 MB
% 26.48/5.47 % (1883319)Instructions burned: 126 (million)
% 26.48/5.47 % (1883322)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=750490076:i=134:gtgl=5:slsql=off:gtg=exists_sym_2975 on theBenchmark for (2975ds/134Mi)
% 26.48/5.47 % (1883322)Instruction limit reached!
% 26.48/5.47 % (1883322)------------------------------
% 26.48/5.47 % (1883322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.48/5.47 % (1883322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/5.47 % (1883322)CaDiCaL version: 2.1.3
% 26.48/5.47 % (1883322)Termination reason: Instruction limit
% 26.48/5.47 % (1883322)Termination phase: Property scanning
% 26.48/5.47 % (1883322)Time elapsed: 0.033 s
% 26.48/5.47 % (1883322)Peak memory usage: 102 MB
% 26.48/5.47 % (1883322)Instructions burned: 137 (million)
% 26.48/5.47 % (1883299)Instruction limit reached!
% 26.48/5.47 % (1883299)------------------------------
% 26.48/5.47 % (1883299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.48/5.47 % (1883299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/5.47 % (1883299)CaDiCaL version: 2.1.3
% 26.48/5.47 % (1883299)Termination reason: Instruction limit
% 26.48/5.47 % (1883299)Termination phase: Saturation
% 26.48/5.47 % (1883299)Time elapsed: 1.441 s
% 26.48/5.47 % (1883299)Peak memory usage: 239 MB
% 26.48/5.47 % (1883299)Instructions burned: 2350 (million)
% 26.48/5.47 % (1883325)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=702889338:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/141Mi)
% 26.48/5.47 % (1883325)Instruction limit reached!
% 26.48/5.47 % (1883325)------------------------------
% 26.48/5.47 % (1883325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.48/5.47 % (1883325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/5.47 % (1883325)CaDiCaL version: 2.1.3
% 26.48/5.47 % (1883325)Termination reason: Instruction limit
% 26.48/5.47 % (1883325)Termination phase: Saturation
% 26.48/5.47 % (1883325)Time elapsed: 0.060 s
% 26.48/5.47 % (1883325)Peak memory usage: 107 MB
% 26.48/5.47 % (1883325)Instructions burned: 142 (million)
% 26.48/5.47 % (1883326)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2810325884:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2972 on theBenchmark for (2972ds/431Mi)
% 26.48/5.47 % (1883328)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3089885405:i=6060:aac=none:ins=25_2971 on theBenchmark for (2971ds/6060Mi)
% 26.48/5.47 % (1883326)Instruction limit reached!
% 26.48/5.47 % (1883326)------------------------------
% 26.48/5.47 % (1883326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.48/5.47 % (1883326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/5.47 % (1883326)CaDiCaL version: 2.1.3
% 26.48/5.47 % (1883326)Termination reason: Instruction limit
% 26.48/5.47 % (1883326)Termination phase: Saturation
% 26.48/5.47 % (1883326)Time elapsed: 0.290 s
% 26.48/5.47 % (1883326)Peak memory usage: 111 MB
% 26.48/5.47 % (1883326)Instructions burned: 432 (million)
% 26.48/5.47 % (1883331)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1047493961:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2967 on theBenchmark for (2967ds/150Mi)
% 26.48/5.47 % (1883331)Instruction limit reached!
% 26.48/5.47 % (1883331)------------------------------
% 26.48/5.47 % (1883331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.48/5.47 % (1883331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.48/5.47 % (1883331)CaDiCaL version: 2.1.3
% 26.48/5.47 % (1883331)Termination reason: Instruction limit
% 26.48/5.47 % (1883331)Termination phase: Preprocessing 1
% 26.48/5.47 % (1883331)Time elapsed: 0.114 s
% 26.48/5.47 % (1883331)Peak memory usage: 103 MB
% 26.48/5.47 % (1883331)Instructions burned: 151 (million)
% 26.48/5.47 % (1883333)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1951340635:i=14155:bd=all_2964 on theBenchmark for (2964ds/14155Mi)
% 26.48/5.47 % (1883277)First to succeed.
% 26.48/5.47 % (1883277)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1883271"
% 26.48/5.47 % (1883277)Refutation found. Thanks to Tanya!
% 26.48/5.47 % SZS status Theorem for theBenchmark
% 26.48/5.47 % SZS output start Proof for theBenchmark
% See solution above
% 31.20/5.67 % (1883277)------------------------------
% 31.20/5.67 % (1883277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.20/5.67 % (1883277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.20/5.67 % (1883277)CaDiCaL version: 2.1.3
% 31.20/5.67 % (1883277)Termination reason: Refutation
% 31.20/5.67 % (1883277)Time elapsed: 3.749 s
% 31.20/5.67 % (1883277)Peak memory usage: 284 MB
% 31.20/5.67 % (1883277)Instructions burned: 6188 (million)
% 31.20/5.67 % (1883277)------------------------------
% 31.20/5.67 % (1883277)------------------------------
% 31.20/5.67 % (1883271)Success in time 4.936 s
% 31.20/5.67 % Vampire exiting
%------------------------------------------------------------------------------