%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : TOP036+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:26 PM UTC 2026
% Result : Theorem 10.00s 4.52s
% Output : Refutation 10.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 31
% Syntax : Number of formulae : 247 ( 66 unt; 6 def)
% Number of atoms : 843 ( 141 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 1025 ( 429 ~; 459 |; 99 &)
% ( 5 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 1 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 10 con; 0-4 aty)
% Number of variables : 278 ( 272 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X0,X2)) = k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k4_tex_4(X0,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t28_tsp_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X0,X2)) = k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k4_tex_4(X0,X2)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f21,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f62,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(k3_tsp_2(X0,X1))
& v1_funct_2(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k3_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_tsp_2) ).
fof(f64,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> ( ~ v1_xboole_0(k4_tex_4(X0,X1))
& m1_subset_1(k4_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_tex_4) ).
fof(f66,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_funct_2) ).
fof(f68,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f73,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f74,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> l1_pre_topc(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_tsp_1) ).
fof(f85,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f91,axiom,
( v1_xboole_0(k1_xboole_0)
& v1_membered(k1_xboole_0)
& v2_membered(k1_xboole_0)
& v3_membered(k1_xboole_0)
& v4_membered(k1_xboole_0)
& v5_membered(k1_xboole_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_membered) ).
fof(f109,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k1_struct_0(X0,X1) = k1_tarski(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_struct_0) ).
fof(f111,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/sandbox2/benchmark/theBenchmark.p',redefinition_k4_pre_topc) ).
fof(f113,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)) )
=> k5_pre_topc(X0,X1,X2,X3) = k10_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_pre_topc) ).
fof(f114,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k8_funct_2) ).
fof(f115,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f116,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
fof(f118,axiom,
! [X0,X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
=> ( r2_hidden(X0,k1_relat_1(X1))
=> k9_relat_1(X1,k1_tarski(X0)) = k1_tarski(k1_funct_1(X1,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t117_funct_1) ).
fof(f119,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f120,axiom,
! [X0,X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
=> r1_tarski(k9_relat_1(X1,k10_relat_1(X1,X0)),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t145_funct_1) ).
fof(f121,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> ~ ( X0 != k1_xboole_0
& r1_tarski(X0,k1_relat_1(X1))
& k9_relat_1(X1,X0) = k1_xboole_0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t152_relat_1) ).
fof(f123,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] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k5_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),k3_tsp_2(X0,X1),X2))) = k4_tex_4(X0,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t27_tsp_2) ).
fof(f124,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f125,axiom,
! [X0,X1] :
( r1_tarski(X0,k1_tarski(X1))
<=> ( X0 = k1_xboole_0
| X0 = k1_tarski(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t39_zfmisc_1) ).
fof(f126,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f128,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_struct_0(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( k1_relat_1(X2) = k2_pre_topc(X0)
& r1_tarski(k2_relat_1(X2),k2_pre_topc(X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_tops_2) ).
fof(f135,plain,
! [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(k3_tsp_2(X0,X1))
& v1_funct_2(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ) ),
inference(pure_predicate_removal,[],[f62]) ).
fof(f149,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X0,X2)) != k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k4_tex_4(X0,X2))
& m1_subset_1(X2,u1_struct_0(X0)) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f150,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X0,X2)) != k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k4_tex_4(X0,X2))
& m1_subset_1(X2,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,[],[f149]) ).
fof(f175,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f21]) ).
fof(f225,plain,
! [X0,X1] :
( ( v1_funct_1(k3_tsp_2(X0,X1))
& v1_funct_2(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k3_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,[],[f135]) ).
fof(f226,plain,
! [X0,X1] :
( ( v1_funct_1(k3_tsp_2(X0,X1))
& v1_funct_2(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(flattening,[],[f225]) ).
fof(f229,plain,
! [X0,X1] :
( ( ~ v1_xboole_0(k4_tex_4(X0,X1))
& m1_subset_1(k4_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f64]) ).
fof(f230,plain,
! [X0,X1] :
( ( ~ v1_xboole_0(k4_tex_4(X0,X1))
& m1_subset_1(k4_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f229]) ).
fof(f233,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f66]) ).
fof(f234,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f233]) ).
fof(f235,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f68]) ).
fof(f237,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f73]) ).
fof(f238,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f74]) ).
fof(f243,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f85]) ).
fof(f244,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f243]) ).
fof(f272,plain,
! [X0,X1] :
( k1_struct_0(X0,X1) = k1_tarski(X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f109]) ).
fof(f273,plain,
! [X0,X1] :
( k1_struct_0(X0,X1) = k1_tarski(X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f272]) ).
fof(f276,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,[],[f111]) ).
fof(f277,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,[],[f276]) ).
fof(f280,plain,
! [X0,X1,X2,X3] :
( k5_pre_topc(X0,X1,X2,X3) = k10_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,[],[f113]) ).
fof(f281,plain,
! [X0,X1,X2,X3] :
( k5_pre_topc(X0,X1,X2,X3) = k10_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,[],[f280]) ).
fof(f282,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f114]) ).
fof(f283,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f282]) ).
fof(f284,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f116]) ).
fof(f285,plain,
! [X0,X1] :
( k9_relat_1(X1,k1_tarski(X0)) = k1_tarski(k1_funct_1(X1,X0))
| ~ r2_hidden(X0,k1_relat_1(X1))
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(ennf_transformation,[],[f118]) ).
fof(f286,plain,
! [X0,X1] :
( k9_relat_1(X1,k1_tarski(X0)) = k1_tarski(k1_funct_1(X1,X0))
| ~ r2_hidden(X0,k1_relat_1(X1))
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(flattening,[],[f285]) ).
fof(f287,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f119]) ).
fof(f288,plain,
! [X0,X1] :
( r1_tarski(k9_relat_1(X1,k10_relat_1(X1,X0)),X0)
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(ennf_transformation,[],[f120]) ).
fof(f289,plain,
! [X0,X1] :
( r1_tarski(k9_relat_1(X1,k10_relat_1(X1,X0)),X0)
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(flattening,[],[f288]) ).
fof(f290,plain,
! [X0,X1] :
( k1_xboole_0 = X0
| ~ r1_tarski(X0,k1_relat_1(X1))
| k1_xboole_0 != k9_relat_1(X1,X0)
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f121]) ).
fof(f291,plain,
! [X0,X1] :
( k1_xboole_0 = X0
| ~ r1_tarski(X0,k1_relat_1(X1))
| k1_xboole_0 != k9_relat_1(X1,X0)
| ~ v1_relat_1(X1) ),
inference(flattening,[],[f290]) ).
fof(f293,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k5_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),k3_tsp_2(X0,X1),X2))) = k4_tex_4(X0,X2)
| ~ m1_subset_1(X2,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,[],[f123]) ).
fof(f294,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k5_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),k3_tsp_2(X0,X1),X2))) = k4_tex_4(X0,X2)
| ~ m1_subset_1(X2,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,[],[f293]) ).
fof(f295,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f124]) ).
fof(f296,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f295]) ).
fof(f299,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k1_relat_1(X2) = k2_pre_topc(X0)
& r1_tarski(k2_relat_1(X2),k2_pre_topc(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f128]) ).
fof(f300,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k1_relat_1(X2) = k2_pre_topc(X0)
& r1_tarski(k2_relat_1(X2),k2_pre_topc(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f299]) ).
fof(f309,plain,
( k4_pre_topc(sK2,sK3,k3_tsp_2(sK2,sK3),k1_struct_0(sK2,sK4)) != k4_pre_topc(sK2,sK3,k3_tsp_2(sK2,sK3),k4_tex_4(sK2,sK4))
& m1_subset_1(sK4,u1_struct_0(sK2))
& ~ v3_struct_0(sK3)
& v2_tsp_2(sK3,sK2)
& m2_tsp_1(sK3,sK2)
& ~ v3_struct_0(sK2)
& v2_pre_topc(sK2)
& l1_pre_topc(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4)],[f150]) ).
fof(f332,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,[],[f115]) ).
fof(f333,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,[],[f284]) ).
fof(f334,plain,
! [X0,X1] :
( ( r1_tarski(X0,k1_tarski(X1))
| ( k1_xboole_0 != X0
& k1_tarski(X1) != X0 ) )
& ( X0 = k1_xboole_0
| X0 = k1_tarski(X1)
| ~ r1_tarski(X0,k1_tarski(X1)) ) ),
inference(nnf_transformation,[],[f125]) ).
fof(f335,plain,
! [X0,X1] :
( ( r1_tarski(X0,k1_tarski(X1))
| ( k1_xboole_0 != X0
& k1_tarski(X1) != X0 ) )
& ( X0 = k1_xboole_0
| X0 = k1_tarski(X1)
| ~ r1_tarski(X0,k1_tarski(X1)) ) ),
inference(flattening,[],[f334]) ).
fof(f336,plain,
! [X0,X1] :
( ( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) )
& ( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ) ),
inference(nnf_transformation,[],[f126]) ).
fof(f337,plain,
l1_pre_topc(sK2),
inference(cnf_transformation,[],[f309]) ).
fof(f338,plain,
v2_pre_topc(sK2),
inference(cnf_transformation,[],[f309]) ).
fof(f339,plain,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f309]) ).
fof(f340,plain,
m2_tsp_1(sK3,sK2),
inference(cnf_transformation,[],[f309]) ).
fof(f341,plain,
v2_tsp_2(sK3,sK2),
inference(cnf_transformation,[],[f309]) ).
fof(f342,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f309]) ).
fof(f343,plain,
m1_subset_1(sK4,u1_struct_0(sK2)),
inference(cnf_transformation,[],[f309]) ).
fof(f344,plain,
k4_pre_topc(sK2,sK3,k3_tsp_2(sK2,sK3),k1_struct_0(sK2,sK4)) != k4_pre_topc(sK2,sK3,k3_tsp_2(sK2,sK3),k4_tex_4(sK2,sK4)),
inference(cnf_transformation,[],[f309]) ).
fof(f392,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f175]) ).
fof(f467,plain,
! [X0,X1] :
( m2_relset_1(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f226]) ).
fof(f468,plain,
! [X0,X1] :
( v1_funct_2(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f226]) ).
fof(f469,plain,
! [X0,X1] :
( v1_funct_1(k3_tsp_2(X0,X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f226]) ).
fof(f471,plain,
! [X0,X1] :
( m1_subset_1(k4_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f230]) ).
fof(f472,plain,
! [X0,X1] :
( ~ v1_xboole_0(k4_tex_4(X0,X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f230]) ).
fof(f474,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f234]) ).
fof(f475,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f235]) ).
fof(f477,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f237]) ).
fof(f478,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f238]) ).
fof(f495,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f244]) ).
fof(f506,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f91]) ).
fof(f563,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| k1_struct_0(X0,X1) = k1_tarski(X1) ),
inference(cnf_transformation,[],[f273]) ).
fof(f565,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))
| k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f277]) ).
fof(f567,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))
| k5_pre_topc(X0,X1,X2,X3) = k10_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f281]) ).
fof(f568,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f283]) ).
fof(f569,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f332]) ).
fof(f571,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f333]) ).
fof(f574,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k1_relat_1(X1))
| k9_relat_1(X1,k1_tarski(X0)) = k1_tarski(k1_funct_1(X1,X0))
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(cnf_transformation,[],[f286]) ).
fof(f575,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f287]) ).
fof(f576,plain,
! [X0,X1] :
( r1_tarski(k9_relat_1(X1,k10_relat_1(X1,X0)),X0)
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(cnf_transformation,[],[f289]) ).
fof(f577,plain,
! [X0,X1] :
( k1_xboole_0 != k9_relat_1(X1,X0)
| ~ r1_tarski(X0,k1_relat_1(X1))
| k1_xboole_0 = X0
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f291]) ).
fof(f579,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| k4_tex_4(X0,X2) = k5_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),k3_tsp_2(X0,X1),X2)))
| 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,[],[f294]) ).
fof(f580,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f296]) ).
fof(f581,plain,
! [X0,X1] :
( ~ r1_tarski(X0,k1_tarski(X1))
| k1_tarski(X1) = X0
| k1_xboole_0 = X0 ),
inference(cnf_transformation,[],[f335]) ).
fof(f584,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f336]) ).
fof(f588,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| k2_pre_topc(X0) = k1_relat_1(X2)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f300]) ).
fof(f595,definition,
sF24 = k3_tsp_2(sK2,sK3),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f596,plain,
k3_tsp_2(sK2,sK3) = sF24,
inference(reorient_equations,[],[f595]) ).
fof(f597,definition,
sF25 = k1_struct_0(sK2,sK4),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f598,plain,
k1_struct_0(sK2,sK4) = sF25,
inference(reorient_equations,[],[f597]) ).
fof(f599,definition,
sF26 = k4_pre_topc(sK2,sK3,sF24,sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f600,plain,
k4_pre_topc(sK2,sK3,sF24,sF25) = sF26,
inference(reorient_equations,[],[f599]) ).
fof(f601,definition,
sF27 = k4_tex_4(sK2,sK4),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f602,plain,
k4_tex_4(sK2,sK4) = sF27,
inference(reorient_equations,[],[f601]) ).
fof(f603,definition,
sF28 = k4_pre_topc(sK2,sK3,sF24,sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f604,plain,
k4_pre_topc(sK2,sK3,sF24,sF27) = sF28,
inference(reorient_equations,[],[f603]) ).
fof(f605,plain,
sF26 != sF28,
inference(definition_folding,[],[f344,f604,f602,f596,f600,f598,f596]) ).
fof(f606,definition,
sF29 = u1_struct_0(sK2),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f607,plain,
u1_struct_0(sK2) = sF29,
inference(reorient_equations,[],[f606]) ).
fof(f608,plain,
m1_subset_1(sK4,sF29),
inference(definition_folding,[],[f343,f607]) ).
fof(f632,plain,
l1_struct_0(sK2),
inference(resolution,[],[f475,f337]) ).
fof(f753,plain,
( l1_pre_topc(sK3)
| ~ l1_pre_topc(sK2) ),
inference(resolution,[],[f478,f340]) ).
fof(f756,plain,
l1_pre_topc(sK3),
inference(forward_subsumption_resolution,[],[f753,f337]) ).
fof(f758,plain,
l1_struct_0(sK3),
inference(resolution,[],[f756,f475]) ).
fof(f759,plain,
( ~ v1_xboole_0(sF29)
| v3_struct_0(sK2)
| ~ l1_struct_0(sK2) ),
inference(superposition,[],[f495,f607]) ).
fof(f760,plain,
( ~ v1_xboole_0(sF29)
| ~ l1_struct_0(sK2) ),
inference(forward_subsumption_resolution,[],[f759,f339]) ).
fof(f761,plain,
~ v1_xboole_0(sF29),
inference(forward_subsumption_resolution,[],[f760,f632]) ).
fof(f777,plain,
u1_struct_0(sK2) = k2_pre_topc(sK2),
inference(resolution,[],[f575,f632]) ).
fof(f782,plain,
sF29 = k2_pre_topc(sK2),
inference(forward_demodulation,[],[f777,f607]) ).
fof(f1123,plain,
( m1_pre_topc(sK3,sK2)
| ~ l1_pre_topc(sK2) ),
inference(resolution,[],[f571,f340]) ).
fof(f1126,plain,
m1_pre_topc(sK3,sK2),
inference(forward_subsumption_resolution,[],[f1123,f337]) ).
fof(f1134,plain,
( r2_hidden(sK4,sF29)
| v1_xboole_0(sF29) ),
inference(resolution,[],[f580,f608]) ).
fof(f1150,plain,
r2_hidden(sK4,sF29),
inference(forward_subsumption_resolution,[],[f1134,f761]) ).
fof(f1179,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f477,f392]) ).
fof(f1836,plain,
( ~ v1_xboole_0(sF27)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ m1_subset_1(sK4,u1_struct_0(sK2)) ),
inference(superposition,[],[f472,f602]) ).
fof(f1837,plain,
( ~ v1_xboole_0(sF27)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ m1_subset_1(sK4,u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1836,f339]) ).
fof(f1838,plain,
( ~ v1_xboole_0(sF27)
| ~ l1_pre_topc(sK2)
| ~ m1_subset_1(sK4,u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1837,f338]) ).
fof(f1839,plain,
( ~ v1_xboole_0(sF27)
| ~ m1_subset_1(sK4,u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1838,f337]) ).
fof(f1840,plain,
( ~ m1_subset_1(sK4,sF29)
| ~ v1_xboole_0(sF27) ),
inference(forward_demodulation,[],[f1839,f607]) ).
fof(f1841,plain,
~ v1_xboole_0(sF27),
inference(forward_subsumption_resolution,[],[f1840,f608]) ).
fof(f1843,plain,
! [X0] :
( ~ m1_subset_1(X0,sF29)
| v3_struct_0(sK2)
| ~ l1_struct_0(sK2)
| k1_tarski(X0) = k1_struct_0(sK2,X0) ),
inference(superposition,[],[f563,f607]) ).
fof(f1844,plain,
! [X0] :
( ~ m1_subset_1(X0,sF29)
| ~ l1_struct_0(sK2)
| k1_tarski(X0) = k1_struct_0(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f1843,f339]) ).
fof(f1845,plain,
! [X0] :
( ~ m1_subset_1(X0,sF29)
| k1_tarski(X0) = k1_struct_0(sK2,X0) ),
inference(forward_subsumption_resolution,[],[f1844,f632]) ).
fof(f2008,plain,
( m1_subset_1(sF27,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ m1_subset_1(sK4,u1_struct_0(sK2)) ),
inference(superposition,[],[f471,f602]) ).
fof(f2016,plain,
( m1_subset_1(sF27,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ m1_subset_1(sK4,u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f2008,f339]) ).
fof(f2019,plain,
( m1_subset_1(sF27,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l1_pre_topc(sK2)
| ~ m1_subset_1(sK4,u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f2016,f338]) ).
fof(f2021,plain,
( m1_subset_1(sF27,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(sK4,u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f2019,f337]) ).
fof(f2022,plain,
( m1_subset_1(sF27,k1_zfmisc_1(sF29))
| ~ m1_subset_1(sK4,u1_struct_0(sK2)) ),
inference(forward_demodulation,[],[f2021,f607]) ).
fof(f2023,plain,
( ~ m1_subset_1(sK4,sF29)
| m1_subset_1(sF27,k1_zfmisc_1(sF29)) ),
inference(forward_demodulation,[],[f2022,f607]) ).
fof(f2024,plain,
m1_subset_1(sF27,k1_zfmisc_1(sF29)),
inference(forward_subsumption_resolution,[],[f2023,f608]) ).
fof(f2040,plain,
r1_tarski(sF27,sF29),
inference(resolution,[],[f2024,f584]) ).
fof(f2166,plain,
( v1_funct_1(sF24)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(superposition,[],[f469,f596]) ).
fof(f2167,plain,
( v1_funct_1(sF24)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2166,f339]) ).
fof(f2168,plain,
( v1_funct_1(sF24)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2167,f338]) ).
fof(f2169,plain,
( v1_funct_1(sF24)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2168,f337]) ).
fof(f2170,plain,
( v1_funct_1(sF24)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2169,f342]) ).
fof(f2171,plain,
( v1_funct_1(sF24)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2170,f341]) ).
fof(f2172,plain,
v1_funct_1(sF24),
inference(forward_subsumption_resolution,[],[f2171,f1126]) ).
fof(f2196,plain,
( m2_relset_1(sF24,u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(superposition,[],[f467,f596]) ).
fof(f2201,plain,
( m2_relset_1(sF24,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2196,f339]) ).
fof(f2203,plain,
( m2_relset_1(sF24,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2201,f338]) ).
fof(f2205,plain,
( m2_relset_1(sF24,u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2203,f337]) ).
fof(f2206,plain,
( m2_relset_1(sF24,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2205,f342]) ).
fof(f2207,plain,
( m2_relset_1(sF24,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2206,f341]) ).
fof(f2208,plain,
m2_relset_1(sF24,u1_struct_0(sK2),u1_struct_0(sK3)),
inference(forward_subsumption_resolution,[],[f2207,f1126]) ).
fof(f2209,plain,
m2_relset_1(sF24,sF29,u1_struct_0(sK3)),
inference(forward_demodulation,[],[f2208,f607]) ).
fof(f2210,plain,
( v1_funct_2(sF24,u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(superposition,[],[f468,f596]) ).
fof(f2215,plain,
( v1_funct_2(sF24,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2210,f339]) ).
fof(f2217,plain,
( v1_funct_2(sF24,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2215,f338]) ).
fof(f2219,plain,
( v1_funct_2(sF24,u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2217,f337]) ).
fof(f2220,plain,
( v1_funct_2(sF24,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2219,f342]) ).
fof(f2221,plain,
( v1_funct_2(sF24,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_pre_topc(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f2220,f341]) ).
fof(f2222,plain,
v1_funct_2(sF24,u1_struct_0(sK2),u1_struct_0(sK3)),
inference(forward_subsumption_resolution,[],[f2221,f1126]) ).
fof(f2223,plain,
v1_funct_2(sF24,sF29,u1_struct_0(sK3)),
inference(forward_demodulation,[],[f2222,f607]) ).
fof(f2289,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,sF29,u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF29,u1_struct_0(X1))
| k2_pre_topc(sK2) = k1_relat_1(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(sK2) ),
inference(superposition,[],[f588,f607]) ).
fof(f2294,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,sF29,u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF29,u1_struct_0(X1))
| k2_pre_topc(sK2) = k1_relat_1(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1) ),
inference(forward_subsumption_resolution,[],[f2289,f632]) ).
fof(f2298,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,sF29,u1_struct_0(X1))
| sF29 = k1_relat_1(X0)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF29,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_struct_0(X1) ),
inference(forward_demodulation,[],[f2294,f782]) ).
fof(f2423,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X0,sF29,u1_struct_0(X1))
| ~ l1_struct_0(sK2)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF29,u1_struct_0(X1))
| k4_pre_topc(sK2,X1,X0,X2) = k9_relat_1(X0,X2) ),
inference(superposition,[],[f565,f607]) ).
fof(f2426,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X0,sF29,u1_struct_0(X1))
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF29,u1_struct_0(X1))
| k4_pre_topc(sK2,X1,X0,X2) = k9_relat_1(X0,X2) ),
inference(forward_subsumption_resolution,[],[f2423,f632]) ).
fof(f2428,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X0,sF29,u1_struct_0(X1))
| ~ l1_struct_0(sK2)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF29,u1_struct_0(X1))
| k5_pre_topc(sK2,X1,X0,X2) = k10_relat_1(X0,X2) ),
inference(superposition,[],[f567,f607]) ).
fof(f2431,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X0,sF29,u1_struct_0(X1))
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF29,u1_struct_0(X1))
| k5_pre_topc(sK2,X1,X0,X2) = k10_relat_1(X0,X2) ),
inference(forward_subsumption_resolution,[],[f2428,f632]) ).
fof(f2434,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF29)
| k4_tex_4(sK2,X0) = k5_pre_topc(sK2,X1,k3_tsp_2(sK2,X1),k1_struct_0(X1,k8_funct_2(sF29,u1_struct_0(X1),k3_tsp_2(sK2,X1),X0)))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,sK2)
| ~ m2_tsp_1(X1,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) ),
inference(superposition,[],[f579,f607]) ).
fof(f2435,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF29)
| k4_tex_4(sK2,X0) = k5_pre_topc(sK2,X1,k3_tsp_2(sK2,X1),k1_struct_0(X1,k8_funct_2(sF29,u1_struct_0(X1),k3_tsp_2(sK2,X1),X0)))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,sK2)
| ~ m2_tsp_1(X1,sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) ),
inference(forward_subsumption_resolution,[],[f2434,f339]) ).
fof(f2436,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF29)
| k4_tex_4(sK2,X0) = k5_pre_topc(sK2,X1,k3_tsp_2(sK2,X1),k1_struct_0(X1,k8_funct_2(sF29,u1_struct_0(X1),k3_tsp_2(sK2,X1),X0)))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,sK2)
| ~ m2_tsp_1(X1,sK2)
| ~ l1_pre_topc(sK2) ),
inference(forward_subsumption_resolution,[],[f2435,f338]) ).
fof(f2437,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF29)
| k4_tex_4(sK2,X0) = k5_pre_topc(sK2,X1,k3_tsp_2(sK2,X1),k1_struct_0(X1,k8_funct_2(sF29,u1_struct_0(X1),k3_tsp_2(sK2,X1),X0)))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,sK2)
| ~ m2_tsp_1(X1,sK2) ),
inference(forward_subsumption_resolution,[],[f2436,f337]) ).
fof(f2438,plain,
m1_relset_1(sF24,sF29,u1_struct_0(sK3)),
inference(resolution,[],[f2209,f569]) ).
fof(f2559,plain,
k1_struct_0(sK2,sK4) = k1_tarski(sK4),
inference(resolution,[],[f1845,f608]) ).
fof(f2561,plain,
sF25 = k1_tarski(sK4),
inference(forward_demodulation,[],[f2559,f598]) ).
fof(f2798,plain,
( sF29 = k1_relat_1(sF24)
| ~ v1_funct_1(sF24)
| ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ l1_struct_0(sK3) ),
inference(resolution,[],[f2298,f2209]) ).
fof(f2802,plain,
( sF29 = k1_relat_1(sF24)
| ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ l1_struct_0(sK3) ),
inference(forward_subsumption_resolution,[],[f2798,f2172]) ).
fof(f2805,plain,
( sF29 = k1_relat_1(sF24)
| v3_struct_0(sK3)
| ~ l1_struct_0(sK3) ),
inference(forward_subsumption_resolution,[],[f2802,f2223]) ).
fof(f2806,plain,
( sF29 = k1_relat_1(sF24)
| ~ l1_struct_0(sK3) ),
inference(forward_subsumption_resolution,[],[f2805,f342]) ).
fof(f2807,plain,
sF29 = k1_relat_1(sF24),
inference(forward_subsumption_resolution,[],[f2806,f758]) ).
fof(f2808,plain,
! [X0] :
( ~ r2_hidden(X0,sF29)
| k9_relat_1(sF24,k1_tarski(X0)) = k1_tarski(k1_funct_1(sF24,X0))
| ~ v1_relat_1(sF24)
| ~ v1_funct_1(sF24) ),
inference(superposition,[],[f574,f2807]) ).
fof(f2809,plain,
! [X0] :
( ~ r2_hidden(X0,sF29)
| k9_relat_1(sF24,k1_tarski(X0)) = k1_tarski(k1_funct_1(sF24,X0))
| ~ v1_relat_1(sF24) ),
inference(forward_subsumption_resolution,[],[f2808,f2172]) ).
fof(f2922,plain,
! [X0] :
( k4_tex_4(sK2,sK4) = k5_pre_topc(sK2,X0,k3_tsp_2(sK2,X0),k1_struct_0(X0,k8_funct_2(sF29,u1_struct_0(X0),k3_tsp_2(sK2,X0),sK4)))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK2)
| ~ m2_tsp_1(X0,sK2) ),
inference(resolution,[],[f2437,f608]) ).
fof(f2924,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK2)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK2)
| sF27 = k5_pre_topc(sK2,X0,k3_tsp_2(sK2,X0),k1_struct_0(X0,k8_funct_2(sF29,u1_struct_0(X0),k3_tsp_2(sK2,X0),sK4))) ),
inference(forward_demodulation,[],[f2922,f602]) ).
fof(f3066,plain,
v1_relat_1(sF24),
inference(resolution,[],[f1179,f2209]) ).
fof(f4112,plain,
! [X0] :
( ~ l1_struct_0(sK3)
| ~ v1_funct_1(sF24)
| ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| k5_pre_topc(sK2,sK3,sF24,X0) = k10_relat_1(sF24,X0) ),
inference(resolution,[],[f2438,f2431]) ).
fof(f4113,plain,
! [X0] :
( ~ l1_struct_0(sK3)
| ~ v1_funct_1(sF24)
| ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| k4_pre_topc(sK2,sK3,sF24,X0) = k9_relat_1(sF24,X0) ),
inference(resolution,[],[f2438,f2426]) ).
fof(f4114,plain,
! [X0] :
( v1_xboole_0(sF29)
| ~ v1_funct_1(sF24)
| ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| k1_funct_1(sF24,X0) = k8_funct_2(sF29,u1_struct_0(sK3),sF24,X0)
| ~ m1_subset_1(X0,sF29) ),
inference(resolution,[],[f2438,f568]) ).
fof(f4116,plain,
! [X0] :
( ~ v1_funct_1(sF24)
| ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| k1_funct_1(sF24,X0) = k8_funct_2(sF29,u1_struct_0(sK3),sF24,X0)
| ~ m1_subset_1(X0,sF29) ),
inference(forward_subsumption_resolution,[],[f4114,f761]) ).
fof(f4117,plain,
! [X0] :
( ~ v1_funct_1(sF24)
| ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| k4_pre_topc(sK2,sK3,sF24,X0) = k9_relat_1(sF24,X0) ),
inference(forward_subsumption_resolution,[],[f4113,f758]) ).
fof(f4118,plain,
! [X0] :
( ~ v1_funct_1(sF24)
| ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| k5_pre_topc(sK2,sK3,sF24,X0) = k10_relat_1(sF24,X0) ),
inference(forward_subsumption_resolution,[],[f4112,f758]) ).
fof(f4119,plain,
! [X0] :
( ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| k1_funct_1(sF24,X0) = k8_funct_2(sF29,u1_struct_0(sK3),sF24,X0)
| ~ m1_subset_1(X0,sF29) ),
inference(forward_subsumption_resolution,[],[f4116,f2172]) ).
fof(f4120,plain,
! [X0] :
( ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| k4_pre_topc(sK2,sK3,sF24,X0) = k9_relat_1(sF24,X0) ),
inference(forward_subsumption_resolution,[],[f4117,f2172]) ).
fof(f4121,plain,
! [X0] :
( ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| k5_pre_topc(sK2,sK3,sF24,X0) = k10_relat_1(sF24,X0) ),
inference(forward_subsumption_resolution,[],[f4118,f2172]) ).
fof(f4122,plain,
! [X0] :
( ~ m1_subset_1(X0,sF29)
| k1_funct_1(sF24,X0) = k8_funct_2(sF29,u1_struct_0(sK3),sF24,X0) ),
inference(forward_subsumption_resolution,[],[f4119,f2223]) ).
fof(f4123,plain,
! [X0] : k4_pre_topc(sK2,sK3,sF24,X0) = k9_relat_1(sF24,X0),
inference(forward_subsumption_resolution,[],[f4120,f2223]) ).
fof(f4124,plain,
! [X0] : k5_pre_topc(sK2,sK3,sF24,X0) = k10_relat_1(sF24,X0),
inference(forward_subsumption_resolution,[],[f4121,f2223]) ).
fof(f8613,plain,
sF26 = k9_relat_1(sF24,sF25),
inference(superposition,[],[f600,f4123]) ).
fof(f8614,plain,
sF28 = k9_relat_1(sF24,sF27),
inference(superposition,[],[f604,f4123]) ).
fof(f8725,plain,
( k1_xboole_0 != sF28
| ~ r1_tarski(sF27,k1_relat_1(sF24))
| k1_xboole_0 = sF27
| ~ v1_relat_1(sF24) ),
inference(superposition,[],[f577,f8614]) ).
fof(f8726,plain,
( k1_xboole_0 != sF28
| ~ r1_tarski(sF27,k1_relat_1(sF24))
| k1_xboole_0 = sF27 ),
inference(forward_subsumption_resolution,[],[f8725,f3066]) ).
fof(f8727,plain,
( ~ r1_tarski(sF27,sF29)
| k1_xboole_0 != sF28
| k1_xboole_0 = sF27 ),
inference(forward_demodulation,[],[f8726,f2807]) ).
fof(f8728,plain,
( k1_xboole_0 != sF28
| k1_xboole_0 = sF27 ),
inference(forward_subsumption_resolution,[],[f8727,f2040]) ).
fof(f11008,plain,
( v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| sF27 = k5_pre_topc(sK2,sK3,k3_tsp_2(sK2,sK3),k1_struct_0(sK3,k8_funct_2(sF29,u1_struct_0(sK3),k3_tsp_2(sK2,sK3),sK4))) ),
inference(resolution,[],[f2924,f340]) ).
fof(f11013,plain,
( ~ v2_tsp_2(sK3,sK2)
| sF27 = k5_pre_topc(sK2,sK3,k3_tsp_2(sK2,sK3),k1_struct_0(sK3,k8_funct_2(sF29,u1_struct_0(sK3),k3_tsp_2(sK2,sK3),sK4))) ),
inference(forward_subsumption_resolution,[],[f11008,f342]) ).
fof(f11014,plain,
sF27 = k5_pre_topc(sK2,sK3,k3_tsp_2(sK2,sK3),k1_struct_0(sK3,k8_funct_2(sF29,u1_struct_0(sK3),k3_tsp_2(sK2,sK3),sK4))),
inference(forward_subsumption_resolution,[],[f11013,f341]) ).
fof(f11015,plain,
sF27 = k5_pre_topc(sK2,sK3,sF24,k1_struct_0(sK3,k8_funct_2(sF29,u1_struct_0(sK3),sF24,sK4))),
inference(forward_demodulation,[],[f11014,f596]) ).
fof(f11016,plain,
sF27 = k10_relat_1(sF24,k1_struct_0(sK3,k8_funct_2(sF29,u1_struct_0(sK3),sF24,sK4))),
inference(forward_demodulation,[],[f11015,f4124]) ).
fof(f23886,plain,
k8_funct_2(sF29,u1_struct_0(sK3),sF24,sK4) = k1_funct_1(sF24,sK4),
inference(resolution,[],[f4122,f608]) ).
fof(f23913,plain,
sF27 = k10_relat_1(sF24,k1_struct_0(sK3,k1_funct_1(sF24,sK4))),
inference(superposition,[],[f11016,f23886]) ).
fof(f23959,plain,
( m1_subset_1(k1_funct_1(sF24,sK4),u1_struct_0(sK3))
| v1_xboole_0(sF29)
| ~ v1_funct_1(sF24)
| ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| ~ m1_relset_1(sF24,sF29,u1_struct_0(sK3))
| ~ m1_subset_1(sK4,sF29) ),
inference(superposition,[],[f474,f23886]) ).
fof(f23994,plain,
( m1_subset_1(k1_funct_1(sF24,sK4),u1_struct_0(sK3))
| ~ v1_funct_1(sF24)
| ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| ~ m1_relset_1(sF24,sF29,u1_struct_0(sK3))
| ~ m1_subset_1(sK4,sF29) ),
inference(forward_subsumption_resolution,[],[f23959,f761]) ).
fof(f24057,plain,
( m1_subset_1(k1_funct_1(sF24,sK4),u1_struct_0(sK3))
| ~ v1_funct_2(sF24,sF29,u1_struct_0(sK3))
| ~ m1_relset_1(sF24,sF29,u1_struct_0(sK3))
| ~ m1_subset_1(sK4,sF29) ),
inference(forward_subsumption_resolution,[],[f23994,f2172]) ).
fof(f24120,plain,
( m1_subset_1(k1_funct_1(sF24,sK4),u1_struct_0(sK3))
| ~ m1_relset_1(sF24,sF29,u1_struct_0(sK3))
| ~ m1_subset_1(sK4,sF29) ),
inference(forward_subsumption_resolution,[],[f24057,f2223]) ).
fof(f24183,plain,
( m1_subset_1(k1_funct_1(sF24,sK4),u1_struct_0(sK3))
| ~ m1_subset_1(sK4,sF29) ),
inference(forward_subsumption_resolution,[],[f24120,f2438]) ).
fof(f24246,plain,
m1_subset_1(k1_funct_1(sF24,sK4),u1_struct_0(sK3)),
inference(forward_subsumption_resolution,[],[f24183,f608]) ).
fof(f24413,plain,
( v3_struct_0(sK3)
| ~ l1_struct_0(sK3)
| k1_struct_0(sK3,k1_funct_1(sF24,sK4)) = k1_tarski(k1_funct_1(sF24,sK4)) ),
inference(resolution,[],[f24246,f563]) ).
fof(f24496,plain,
( ~ l1_struct_0(sK3)
| k1_struct_0(sK3,k1_funct_1(sF24,sK4)) = k1_tarski(k1_funct_1(sF24,sK4)) ),
inference(forward_subsumption_resolution,[],[f24413,f342]) ).
fof(f24507,plain,
k1_struct_0(sK3,k1_funct_1(sF24,sK4)) = k1_tarski(k1_funct_1(sF24,sK4)),
inference(forward_subsumption_resolution,[],[f24496,f758]) ).
fof(f24649,plain,
( k1_tarski(k1_funct_1(sF24,sK4)) = k9_relat_1(sF24,k1_tarski(sK4))
| ~ v1_relat_1(sF24) ),
inference(resolution,[],[f2809,f1150]) ).
fof(f24689,plain,
k1_tarski(k1_funct_1(sF24,sK4)) = k9_relat_1(sF24,k1_tarski(sK4)),
inference(forward_subsumption_resolution,[],[f24649,f3066]) ).
fof(f24690,plain,
k9_relat_1(sF24,sF25) = k1_tarski(k1_funct_1(sF24,sK4)),
inference(forward_demodulation,[],[f24689,f2561]) ).
fof(f24691,plain,
sF26 = k1_tarski(k1_funct_1(sF24,sK4)),
inference(forward_demodulation,[],[f24690,f8613]) ).
fof(f24708,plain,
! [X0] :
( ~ r1_tarski(X0,sF26)
| sF26 = X0
| k1_xboole_0 = X0 ),
inference(superposition,[],[f581,f24691]) ).
fof(f26237,plain,
( r1_tarski(k9_relat_1(sF24,sF27),k1_struct_0(sK3,k1_funct_1(sF24,sK4)))
| ~ v1_relat_1(sF24)
| ~ v1_funct_1(sF24) ),
inference(superposition,[],[f576,f23913]) ).
fof(f26302,plain,
( r1_tarski(k9_relat_1(sF24,sF27),k1_struct_0(sK3,k1_funct_1(sF24,sK4)))
| ~ v1_funct_1(sF24) ),
inference(forward_subsumption_resolution,[],[f26237,f3066]) ).
fof(f26335,plain,
r1_tarski(k9_relat_1(sF24,sF27),k1_struct_0(sK3,k1_funct_1(sF24,sK4))),
inference(forward_subsumption_resolution,[],[f26302,f2172]) ).
fof(f26368,plain,
r1_tarski(k9_relat_1(sF24,sF27),k1_tarski(k1_funct_1(sF24,sK4))),
inference(forward_demodulation,[],[f26335,f24507]) ).
fof(f26401,plain,
r1_tarski(k9_relat_1(sF24,sF27),sF26),
inference(forward_demodulation,[],[f26368,f24691]) ).
fof(f26402,plain,
r1_tarski(sF28,sF26),
inference(forward_demodulation,[],[f26401,f8614]) ).
fof(f26941,plain,
( sF26 = sF28
| k1_xboole_0 = sF28 ),
inference(resolution,[],[f24708,f26402]) ).
fof(f26942,plain,
k1_xboole_0 = sF28,
inference(forward_subsumption_resolution,[],[f26941,f605]) ).
fof(f26966,plain,
( k1_xboole_0 != k1_xboole_0
| k1_xboole_0 = sF27 ),
inference(superposition,[],[f8728,f26942]) ).
fof(f27051,plain,
k1_xboole_0 = sF27,
inference(trivial_inequality_removal,[],[f26966]) ).
fof(f27069,plain,
~ v1_xboole_0(k1_xboole_0),
inference(superposition,[],[f1841,f27051]) ).
fof(f27156,plain,
$false,
inference(forward_subsumption_resolution,[],[f27069,f506]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP036+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 % Computer : n001.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 19:04:49 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.24 Running first-order model finding
% 0.08/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.47/2.32 % (629840)Will run a generic schedule for satisfiability detection.
% 14.47/2.32 % (629848)dis+10_1_sil=32000:sp=arity:random_seed=756572266:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.47/2.32 % (629846)% WARNING: option uhcvi not known.
% 14.47/2.32 % (629845)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3283907512_2999 on theBenchmark for (2999ds/0Mi)
% 14.47/2.32 % (629846)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=637548632:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.47/2.32 % (629847)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4071542613:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.47/2.32 % (629849)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4234908809:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.47/2.32 % (629850)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3347051051:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.47/2.32 % (629851)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2208420988:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.47/2.32 % TRYING [1]
% 14.47/2.32 % TRYING [2]
% 14.47/2.32 % TRYING [3]
% 14.47/2.32 % (629848)Instruction limit reached!
% 14.47/2.32 % (629848)------------------------------
% 14.47/2.32 % (629848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.47/2.32 % (629848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.47/2.32 % (629848)CaDiCaL version: 2.1.3
% 14.47/2.32 % (629848)Termination reason: Instruction limit
% 14.47/2.32 % (629848)Termination phase: Saturation
% 14.47/2.32 % (629848)Time elapsed: 0.036 s
% 14.47/2.32 % (629848)Peak memory usage: 13 MB
% 14.47/2.32 % (629848)Instructions burned: 105 (million)
% 14.47/2.32 % TRYING [4]
% 14.47/2.32 % (629859)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=807117363:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.47/2.32 % TRYING [1]
% 14.47/2.32 % TRYING [2]
% 14.47/2.32 % TRYING [3]
% 14.47/2.32 % TRYING [4]
% 14.47/2.32 % (629849)Instruction limit reached!
% 14.47/2.32 % (629849)------------------------------
% 14.47/2.32 % (629849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.47/2.32 % (629849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.47/2.32 % (629849)CaDiCaL version: 2.1.3
% 14.47/2.32 % (629849)Termination reason: Instruction limit
% 14.47/2.32 % (629849)Termination phase: Saturation
% 14.47/2.32 % (629849)Time elapsed: 0.073 s
% 14.47/2.32 % (629849)Peak memory usage: 13 MB
% 14.47/2.32 % (629849)Instructions burned: 116 (million)
% 14.47/2.32 % (629850)Instruction limit reached!
% 14.47/2.32 % (629850)------------------------------
% 14.47/2.32 % (629850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.47/2.32 % (629850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.47/2.32 % (629850)CaDiCaL version: 2.1.3
% 14.47/2.32 % (629850)Termination reason: Instruction limit
% 14.47/2.32 % (629850)Termination phase: Saturation
% 14.47/2.32 % (629850)Time elapsed: 0.080 s
% 14.47/2.32 % (629850)Peak memory usage: 14 MB
% 14.47/2.32 % (629850)Instructions burned: 131 (million)
% 14.47/2.32 % (629861)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4035119516:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.47/2.32 % TRYING [5]
% 14.47/2.32 % TRYING [5]
% 14.47/2.32 % (629851)Instruction limit reached!
% 14.47/2.32 % (629851)------------------------------
% 14.47/2.32 % (629851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.47/2.32 % (629851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.47/2.32 % (629851)CaDiCaL version: 2.1.3
% 14.47/2.32 % (629851)Termination reason: Instruction limit
% 14.47/2.32 % (629851)Termination phase: Saturation
% 14.47/2.32 % (629851)Time elapsed: 0.098 s
% 14.47/2.32 % (629851)Peak memory usage: 14 MB
% 14.47/2.32 % (629851)Instructions burned: 160 (million)
% 14.47/2.32 % (629862)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2922182552:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.47/2.32 % (629864)ott-21_1_sil=16000:fs=off:random_seed=706161343:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.47/2.32 % (629859)Instruction limit reached!
% 14.47/2.32 % (629859)------------------------------
% 14.47/2.32 % (629859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.47/2.32 % (629859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629859)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629859)Termination reason: Instruction limit
% 10.00/4.52 % (629859)Termination phase: Finite model building constraint generation
% 10.00/4.52 % (629859)Time elapsed: 0.141 s
% 10.00/4.52 % (629859)Peak memory usage: 36 MB
% 10.00/4.52 % (629859)Instructions burned: 719 (million)
% 10.00/4.52 % (629867)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1288114658:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 10.00/4.52 % (629861)Instruction limit reached!
% 10.00/4.52 % (629861)------------------------------
% 10.00/4.52 % (629861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629861)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629861)Termination reason: Instruction limit
% 10.00/4.52 % (629861)Termination phase: Saturation
% 10.00/4.52 % (629861)Time elapsed: 0.105 s
% 10.00/4.52 % (629861)Peak memory usage: 14 MB
% 10.00/4.52 % (629861)Instructions burned: 131 (million)
% 10.00/4.52 % (629864)Instruction limit reached!
% 10.00/4.52 % (629864)------------------------------
% 10.00/4.52 % (629864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629864)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629864)Termination reason: Instruction limit
% 10.00/4.52 % (629864)Termination phase: Saturation
% 10.00/4.52 % (629864)Time elapsed: 0.092 s
% 10.00/4.52 % (629864)Peak memory usage: 13 MB
% 10.00/4.52 % (629864)Instructions burned: 181 (million)
% 10.00/4.52 % (629869)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=680295999:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 10.00/4.52 % TRYING [1]
% 10.00/4.52 % TRYING [2]
% 10.00/4.52 % (629870)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1198157335:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 10.00/4.52 % TRYING [3]
% 10.00/4.52 % TRYING [6]
% 10.00/4.52 % TRYING [4]
% 10.00/4.52 % (629867)Instruction limit reached!
% 10.00/4.52 % (629867)------------------------------
% 10.00/4.52 % (629867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629867)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629867)Termination reason: Instruction limit
% 10.00/4.52 % (629867)Termination phase: Saturation
% 10.00/4.52 % (629867)Time elapsed: 0.172 s
% 10.00/4.52 % (629867)Peak memory usage: 16 MB
% 10.00/4.52 % (629867)Instructions burned: 478 (million)
% 10.00/4.52 % (629873)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4291355678:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 10.00/4.52 % TRYING [5]
% 10.00/4.52 % (629862)Instruction limit reached!
% 10.00/4.52 % (629862)------------------------------
% 10.00/4.52 % (629862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629862)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629862)Termination reason: Instruction limit
% 10.00/4.52 % (629862)Termination phase: Saturation
% 10.00/4.52 % (629862)Time elapsed: 0.413 s
% 10.00/4.52 % (629862)Peak memory usage: 19 MB
% 10.00/4.52 % (629862)Instructions burned: 684 (million)
% 10.00/4.52 % (629875)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3455701057:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 10.00/4.52 % (629869)Instruction limit reached!
% 10.00/4.52 % (629869)------------------------------
% 10.00/4.52 % (629869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629869)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629869)Termination reason: Instruction limit
% 10.00/4.52 % (629869)Termination phase: Finite model building constraint generation
% 10.00/4.52 % (629869)Time elapsed: 0.323 s
% 10.00/4.52 % (629869)Peak memory usage: 22 MB
% 10.00/4.52 % (629869)Instructions burned: 867 (million)
% 10.00/4.52 % (629877)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1373367192:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 10.00/4.52 % (629873)Instruction limit reached!
% 10.00/4.52 % (629873)------------------------------
% 10.00/4.52 % (629873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629873)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629873)Termination reason: Instruction limit
% 10.00/4.52 % (629873)Termination phase: Finite model building constraint generation
% 10.00/4.52 % (629873)Time elapsed: 0.234 s
% 10.00/4.52 % (629873)Peak memory usage: 108 MB
% 10.00/4.52 % (629873)Instructions burned: 894 (million)
% 10.00/4.52 % (629879)fmb+10_1_sil=64000:random_seed=4250221298:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 10.00/4.52 % TRYING [1]
% 10.00/4.52 % TRYING [2]
% 10.00/4.52 % TRYING [3]
% 10.00/4.52 % TRYING [4]
% 10.00/4.52 % TRYING [5]
% 10.00/4.52 % TRYING [7]
% 10.00/4.52 % (629870)Instruction limit reached!
% 10.00/4.52 % (629870)------------------------------
% 10.00/4.52 % (629870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629870)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629870)Termination reason: Instruction limit
% 10.00/4.52 % (629870)Termination phase: Saturation
% 10.00/4.52 % (629870)Time elapsed: 0.667 s
% 10.00/4.52 % (629870)Peak memory usage: 27 MB
% 10.00/4.52 % (629870)Instructions burned: 1180 (million)
% 10.00/4.52 % (629881)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1789863210:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 10.00/4.52 % (629875)Instruction limit reached!
% 10.00/4.52 % (629875)------------------------------
% 10.00/4.52 % (629875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629875)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629875)Termination reason: Instruction limit
% 10.00/4.52 % (629875)Termination phase: Saturation
% 10.00/4.52 % (629875)Time elapsed: 0.386 s
% 10.00/4.52 % (629875)Peak memory usage: 23 MB
% 10.00/4.52 % (629875)Instructions burned: 693 (million)
% 10.00/4.52 % TRYING [20]
% 10.00/4.52 % (629883)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4246115456:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 10.00/4.52 % TRYING [8]
% 10.00/4.52 % (629877)Instruction limit reached!
% 10.00/4.52 % (629877)------------------------------
% 10.00/4.52 % (629877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629877)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629877)Termination reason: Instruction limit
% 10.00/4.52 % (629877)Termination phase: Saturation
% 10.00/4.52 % (629877)Time elapsed: 0.503 s
% 10.00/4.52 % (629877)Peak memory usage: 20 MB
% 10.00/4.52 % (629877)Instructions burned: 880 (million)
% 10.00/4.52 % (629885)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4141000871:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 10.00/4.52 % TRYING [6]
% 10.00/4.52 % (629883)Instruction limit reached!
% 10.00/4.52 % (629883)------------------------------
% 10.00/4.52 % (629883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629883)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629883)Termination reason: Instruction limit
% 10.00/4.52 % (629883)Termination phase: Finite model building constraint generation
% 10.00/4.52 % (629883)Time elapsed: 0.293 s
% 10.00/4.52 % (629883)Peak memory usage: 54 MB
% 10.00/4.52 % (629883)Instructions burned: 920 (million)
% 10.00/4.52 % (629887)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1852256999:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 10.00/4.52 % (629887)Instruction limit reached!
% 10.00/4.52 % (629887)------------------------------
% 10.00/4.52 % (629887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629887)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629887)Termination reason: Instruction limit
% 10.00/4.52 % (629887)Termination phase: Saturation
% 10.00/4.52 % (629887)Time elapsed: 0.726 s
% 10.00/4.52 % (629887)Peak memory usage: 22 MB
% 10.00/4.52 % (629887)Instructions burned: 1472 (million)
% 10.00/4.52 % (629889)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2932218058:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 10.00/4.52 % (629889)Cannot represent all propositional literals internally
% 10.00/4.52 % (629889)Refutation not found, incomplete strategy
% 10.00/4.52 % (629889)------------------------------
% 10.00/4.52 % (629889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629889)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629889)Termination reason: Refutation not found, incomplete strategy
% 10.00/4.52 % (629889)Time elapsed: 0.012 s
% 10.00/4.52 % (629889)Peak memory usage: 11 MB
% 10.00/4.52 % (629889)Instructions burned: 23 (million)
% 10.00/4.52 % (629889)------------------------------
% 10.00/4.52 % (629889)------------------------------
% 10.00/4.52 % (629891)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4236048921:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 10.00/4.52 % TRYING [7]
% 10.00/4.52 % TRYING [16]
% 10.00/4.52 % (629891)Instruction limit reached!
% 10.00/4.52 % (629891)------------------------------
% 10.00/4.52 % (629891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629891)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629891)Termination reason: Instruction limit
% 10.00/4.52 % (629891)Termination phase: Finite model building constraint generation
% 10.00/4.52 % (629891)Time elapsed: 0.764 s
% 10.00/4.52 % (629891)Peak memory usage: 132 MB
% 10.00/4.52 % (629891)Instructions burned: 2177 (million)
% 10.00/4.52 % (629893)ott-2_1_sil=16000:newcnf=on:random_seed=830452608:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 10.00/4.52 % TRYING [8]
% 10.00/4.52 % (629893)Instruction limit reached!
% 10.00/4.52 % (629893)------------------------------
% 10.00/4.52 % (629893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629893)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629893)Termination reason: Instruction limit
% 10.00/4.52 % (629893)Termination phase: Saturation
% 10.00/4.52 % (629893)Time elapsed: 0.529 s
% 10.00/4.52 % (629893)Peak memory usage: 21 MB
% 10.00/4.52 % (629893)Instructions burned: 871 (million)
% 10.00/4.52 % (629895)ott+10_1_sil=32000:tgt=ground:random_seed=2006957968:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 10.00/4.52 % (629885)Instruction limit reached!
% 10.00/4.52 % (629885)------------------------------
% 10.00/4.52 % (629885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629885)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629885)Termination reason: Instruction limit
% 10.00/4.52 % (629885)Termination phase: Saturation
% 10.00/4.52 % (629885)Time elapsed: 2.821 s
% 10.00/4.52 % (629885)Peak memory usage: 34 MB
% 10.00/4.52 % (629885)Instructions burned: 5131 (million)
% 10.00/4.52 % (629897)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=336256166:i=54282_2960 on theBenchmark for (2960ds/54282Mi)
% 10.00/4.52 % TRYING [1]
% 10.00/4.52 % TRYING [2]
% 10.00/4.52 % TRYING [3]
% 10.00/4.52 % TRYING [4]
% 10.00/4.52 % TRYING [5]
% 10.00/4.52 % (629895) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-629840-629895"...
% 10.00/4.52 % (629895)...printing done.
% 10.00/4.52 % (629895)Refutation found. Thanks to Tanya!
% 10.00/4.52 % SZS status Theorem for theBenchmark
% 10.00/4.52 % SZS output start Proof for theBenchmark
% See solution above
% 10.00/4.52 % (629895)------------------------------
% 10.00/4.52 % (629895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.00/4.52 % (629895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/4.52 % (629895)CaDiCaL version: 2.1.3
% 10.00/4.52 % (629895)Termination reason: Refutation
% 10.00/4.52 % (629895)Time elapsed: 0.738 s
% 10.00/4.52 % (629895)Peak memory usage: 24 MB
% 10.00/4.52 % (629895)Instructions burned: 1381 (million)
% 10.00/4.52 % (629840)Success in time 4.272 s
% 10.00/4.52 % Vampire exiting
%------------------------------------------------------------------------------