%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT363+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n011.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 : Fri Sep 25 01:59:39 PM UTC 2026
% Result : Theorem 1.35s 1.73s
% Output : CNFRefutation 1.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 12
% Syntax : Number of formulae : 158 ( 35 unt; 0 def)
% Number of atoms : 871 ( 26 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 1267 ( 554 ~; 554 |; 120 &)
% ( 9 <=>; 28 =>; 0 <=; 2 <~>)
% Maximal formula depth : 16 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-4 aty)
% Number of variables : 267 ( 0 sgn 251 !; 16 ?; 70 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_pre_topc(X1)
& v2_pre_topc(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> ( v2_waybel34(X2,X0,X1)
<=> v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t26_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_pre_topc(X1)
& v2_pre_topc(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> ( v2_waybel34(X2,X0,X1)
<=> v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f32,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> ( v1_t_0topsp(X2,X0,X1)
<=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v3_pre_topc(X3,X0)
=> v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_t_0topsp) ).
fof(f33,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> k7_waybel18(X0,X1,X2) = k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_waybel18) ).
fof(f34,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( ( l1_pre_topc(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> k8_waybel18(X0,X1,X2) = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d7_waybel18) ).
fof(f35,axiom,
! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0) )
=> ! [X1] :
( ( l1_pre_topc(X1)
& v2_pre_topc(X1) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> ( v2_waybel34(X2,X0,X1)
<=> ! [X3] :
( ( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X3,X0) )
=> ( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))))
& v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_waybel34) ).
fof(f43,axiom,
! [X0,X1,X2,X3] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_struct_0(X1)
& l1_struct_0(X0) )
=> m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_pre_topc) ).
fof(f44,axiom,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_pre_topc(X1)
& l1_struct_0(X0) )
=> m1_pre_topc(k7_waybel18(X0,X1,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_waybel18) ).
fof(f45,axiom,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_pre_topc(X1)
& ~ v3_struct_0(X1)
& l1_struct_0(X0) )
=> ( m2_relset_1(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2)))
& v1_funct_2(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2)))
& v1_funct_1(k8_waybel18(X0,X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_waybel18) ).
fof(f48,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f50,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m1_pre_topc(X1,X0)
=> l1_pre_topc(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_pre_topc) ).
fof(f92,axiom,
! [X0,X1,X2,X3] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_struct_0(X1)
& l1_struct_0(X0) )
=> k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_pre_topc) ).
fof(f94,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(f117,plain,
? [X0] :
( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( l1_pre_topc(X1)
& v2_pre_topc(X1)
& ~ v3_struct_0(X1)
& ? [X2] :
( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& ( v2_waybel34(X2,X0,X1)
<~> v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2)) ) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f118,plain,
? [X0] :
( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( l1_pre_topc(X1)
& v2_pre_topc(X1)
& ~ v3_struct_0(X1)
& ? [X2] :
( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& ( v2_waybel34(X2,X0,X1)
<~> v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2)) ) ) ) ),
inference(flattening,[],[f117]) ).
fof(f123,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_pre_topc(X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X0)
| ( m2_relset_1(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2)))
& v1_funct_2(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2)))
& v1_funct_1(k8_waybel18(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f45]) ).
fof(f124,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_pre_topc(X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X0)
| ( m2_relset_1(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2)))
& v1_funct_2(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2)))
& v1_funct_1(k8_waybel18(X0,X1,X2)) ) ),
inference(flattening,[],[f123]) ).
fof(f125,plain,
! [X0] :
( ~ l1_struct_0(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k8_waybel18(X0,X1,X2) = X2 ) ) ),
inference(ennf_transformation,[],[f34]) ).
fof(f126,plain,
! [X0] :
( ~ l1_struct_0(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k8_waybel18(X0,X1,X2) = X2 ) ) ),
inference(flattening,[],[f125]) ).
fof(f127,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_pre_topc(X1)
| ~ l1_struct_0(X0)
| m1_pre_topc(k7_waybel18(X0,X1,X2),X1) ),
inference(ennf_transformation,[],[f44]) ).
fof(f128,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_pre_topc(X1)
| ~ l1_struct_0(X0)
| m1_pre_topc(k7_waybel18(X0,X1,X2),X1) ),
inference(flattening,[],[f127]) ).
fof(f129,plain,
! [X0] :
( ~ l1_struct_0(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k7_waybel18(X0,X1,X2) = k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)) ) ) ),
inference(ennf_transformation,[],[f33]) ).
fof(f130,plain,
! [X0] :
( ~ l1_struct_0(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k7_waybel18(X0,X1,X2) = k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)) ) ) ),
inference(flattening,[],[f129]) ).
fof(f132,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( v2_waybel34(X2,X0,X1)
<=> ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X3,X0)
| ( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))))
& v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))) ) ) ) ) ) ),
inference(ennf_transformation,[],[f35]) ).
fof(f133,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( v2_waybel34(X2,X0,X1)
<=> ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X3,X0)
| ( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))))
& v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))) ) ) ) ) ) ),
inference(flattening,[],[f132]) ).
fof(f134,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( v1_t_0topsp(X2,X0,X1)
<=> ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X3,X0)
| v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),X1) ) ) ) ) ),
inference(ennf_transformation,[],[f32]) ).
fof(f135,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( v1_t_0topsp(X2,X0,X1)
<=> ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X3,X0)
| v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),X1) ) ) ) ) ),
inference(flattening,[],[f134]) ).
fof(f136,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| l1_struct_0(X0) ),
inference(ennf_transformation,[],[f48]) ).
fof(f144,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ~ m1_pre_topc(X1,X0)
| l1_pre_topc(X1) ) ),
inference(ennf_transformation,[],[f50]) ).
fof(f155,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(ennf_transformation,[],[f92]) ).
fof(f156,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(flattening,[],[f155]) ).
fof(f157,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(ennf_transformation,[],[f43]) ).
fof(f158,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(flattening,[],[f157]) ).
fof(f179,plain,
? [X0] :
( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( l1_pre_topc(X1)
& v2_pre_topc(X1)
& ~ v3_struct_0(X1)
& ? [X2] :
( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& ( v2_waybel34(X2,X0,X1)
| v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2)) )
& ( ~ v2_waybel34(X2,X0,X1)
| ~ v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2)) ) ) ) ),
inference(nnf_transformation,[],[f118]) ).
fof(f180,plain,
? [X0] :
( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( l1_pre_topc(X1)
& v2_pre_topc(X1)
& ~ v3_struct_0(X1)
& ? [X2] :
( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& ( v2_waybel34(X2,X0,X1)
| v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2)) )
& ( ~ v2_waybel34(X2,X0,X1)
| ~ v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2)) ) ) ) ),
inference(flattening,[],[f179]) ).
fof(f181,plain,
( l1_pre_topc(sK0)
& v2_pre_topc(sK0)
& ~ v3_struct_0(sK0)
& l1_pre_topc(sK1)
& v2_pre_topc(sK1)
& ~ v3_struct_0(sK1)
& m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
& v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
& v1_funct_1(sK2)
& ( v2_waybel34(sK2,sK0,sK1)
| v1_t_0topsp(k8_waybel18(sK0,sK1,sK2),sK0,k7_waybel18(sK0,sK1,sK2)) )
& ( ~ v2_waybel34(sK2,sK0,sK1)
| ~ v1_t_0topsp(k8_waybel18(sK0,sK1,sK2),sK0,k7_waybel18(sK0,sK1,sK2)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f180]) ).
fof(f186,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,[],[f94]) ).
fof(f188,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( ( ~ v2_waybel34(X2,X0,X1)
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X3,X0)
| ( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))))
& v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))) ) ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X3,X0)
& ( ~ m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))))
| ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))) ) )
| v2_waybel34(X2,X0,X1) ) ) ) ) ),
inference(nnf_transformation,[],[f133]) ).
fof(f189,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( ( ~ v2_waybel34(X2,X0,X1)
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X4,X0)
| ( m1_subset_1(k4_pre_topc(X0,X1,X2,X4),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))))
& v3_pre_topc(k4_pre_topc(X0,X1,X2,X4),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))) ) ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X3,X0)
& ( ~ m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))))
| ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))) ) )
| v2_waybel34(X2,X0,X1) ) ) ) ) ),
inference(rectify,[],[f188]) ).
fof(f190,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( ( ~ v2_waybel34(X2,X0,X1)
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X4,X0)
| ( m1_subset_1(k4_pre_topc(X0,X1,X2,X4),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))))
& v3_pre_topc(k4_pre_topc(X0,X1,X2,X4),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))) ) ) )
& ( ( m1_subset_1(sK8(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(sK8(X0,X1,X2),X0)
& ( ~ m1_subset_1(k4_pre_topc(X0,X1,X2,sK8(X0,X1,X2)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))))
| ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,sK8(X0,X1,X2)),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))) ) )
| v2_waybel34(X2,X0,X1) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X3,sK8(X0,X1,X2))],[f189]) ).
fof(f191,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( ( ~ v1_t_0topsp(X2,X0,X1)
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X3,X0)
| v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),X1) ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X3,X0)
& ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),X1) )
| v1_t_0topsp(X2,X0,X1) ) ) ) ) ),
inference(nnf_transformation,[],[f135]) ).
fof(f192,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( ( ~ v1_t_0topsp(X2,X0,X1)
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X4,X0)
| v3_pre_topc(k4_pre_topc(X0,X1,X2,X4),X1) ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(X3,X0)
& ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),X1) )
| v1_t_0topsp(X2,X0,X1) ) ) ) ) ),
inference(rectify,[],[f191]) ).
fof(f193,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( ( ~ v1_t_0topsp(X2,X0,X1)
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X4,X0)
| v3_pre_topc(k4_pre_topc(X0,X1,X2,X4),X1) ) )
& ( ( m1_subset_1(sK9(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
& v3_pre_topc(sK9(X0,X1,X2),X0)
& ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,sK9(X0,X1,X2)),X1) )
| v1_t_0topsp(X2,X0,X1) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X3,sK9(X0,X1,X2))],[f192]) ).
fof(f212,plain,
l1_pre_topc(sK0),
inference(cnf_transformation,[],[f181]) ).
fof(f213,plain,
v2_pre_topc(sK0),
inference(cnf_transformation,[],[f181]) ).
fof(f215,plain,
l1_pre_topc(sK1),
inference(cnf_transformation,[],[f181]) ).
fof(f216,plain,
v2_pre_topc(sK1),
inference(cnf_transformation,[],[f181]) ).
fof(f217,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f181]) ).
fof(f218,plain,
m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f181]) ).
fof(f219,plain,
v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f181]) ).
fof(f220,plain,
v1_funct_1(sK2),
inference(cnf_transformation,[],[f181]) ).
fof(f221,plain,
( v2_waybel34(sK2,sK0,sK1)
| v1_t_0topsp(k8_waybel18(sK0,sK1,sK2),sK0,k7_waybel18(sK0,sK1,sK2)) ),
inference(cnf_transformation,[],[f181]) ).
fof(f222,plain,
( ~ v2_waybel34(sK2,sK0,sK1)
| ~ v1_t_0topsp(k8_waybel18(sK0,sK1,sK2),sK0,k7_waybel18(sK0,sK1,sK2)) ),
inference(cnf_transformation,[],[f181]) ).
fof(f231,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_pre_topc(X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X0)
| m2_relset_1(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2))) ),
inference(cnf_transformation,[],[f124]) ).
fof(f232,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_pre_topc(X1)
| v3_struct_0(X1)
| ~ l1_struct_0(X0)
| v1_funct_2(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2))) ),
inference(cnf_transformation,[],[f124]) ).
fof(f234,plain,
! [X2,X0,X1] :
( ~ l1_struct_0(X0)
| ~ l1_pre_topc(X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k8_waybel18(X0,X1,X2) = X2 ),
inference(cnf_transformation,[],[f126]) ).
fof(f235,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_pre_topc(X1)
| ~ l1_struct_0(X0)
| m1_pre_topc(k7_waybel18(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f128]) ).
fof(f236,plain,
! [X2,X0,X1] :
( ~ l1_struct_0(X0)
| ~ l1_pre_topc(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k7_waybel18(X0,X1,X2) = k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f130]) ).
fof(f239,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f186]) ).
fof(f243,plain,
! [X2,X0,X1,X4] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v2_waybel34(X2,X0,X1)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X4,X0)
| v3_pre_topc(k4_pre_topc(X0,X1,X2,X4),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))) ),
inference(cnf_transformation,[],[f190]) ).
fof(f244,plain,
! [X2,X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| m1_subset_1(sK8(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| v2_waybel34(X2,X0,X1) ),
inference(cnf_transformation,[],[f190]) ).
fof(f245,plain,
! [X2,X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| v3_pre_topc(sK8(X0,X1,X2),X0)
| v2_waybel34(X2,X0,X1) ),
inference(cnf_transformation,[],[f190]) ).
fof(f246,plain,
! [X2,X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m1_subset_1(k4_pre_topc(X0,X1,X2,sK8(X0,X1,X2)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))))
| ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,sK8(X0,X1,X2)),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))
| v2_waybel34(X2,X0,X1) ),
inference(cnf_transformation,[],[f190]) ).
fof(f247,plain,
! [X2,X0,X1,X4] :
( ~ l1_pre_topc(X0)
| ~ l1_pre_topc(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v1_t_0topsp(X2,X0,X1)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X4,X0)
| v3_pre_topc(k4_pre_topc(X0,X1,X2,X4),X1) ),
inference(cnf_transformation,[],[f193]) ).
fof(f248,plain,
! [X2,X0,X1] :
( ~ l1_pre_topc(X0)
| ~ l1_pre_topc(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| m1_subset_1(sK9(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| v1_t_0topsp(X2,X0,X1) ),
inference(cnf_transformation,[],[f193]) ).
fof(f249,plain,
! [X2,X0,X1] :
( ~ l1_pre_topc(X0)
| ~ l1_pre_topc(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| v3_pre_topc(sK9(X0,X1,X2),X0)
| v1_t_0topsp(X2,X0,X1) ),
inference(cnf_transformation,[],[f193]) ).
fof(f250,plain,
! [X2,X0,X1] :
( ~ l1_pre_topc(X0)
| ~ l1_pre_topc(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,sK9(X0,X1,X2)),X1)
| v1_t_0topsp(X2,X0,X1) ),
inference(cnf_transformation,[],[f193]) ).
fof(f253,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f263,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f144]) ).
fof(f269,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f156]) ).
fof(f270,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f158]) ).
tcf(c_49,negated_conjecture,
( ~ v2_waybel34(sK2,sK0,sK1)
| ~ v1_t_0topsp(k8_waybel18(sK0,sK1,sK2),sK0,k7_waybel18(sK0,sK1,sK2)) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_50,negated_conjecture,
( v2_waybel34(sK2,sK0,sK1)
| v1_t_0topsp(k8_waybel18(sK0,sK1,sK2),sK0,k7_waybel18(sK0,sK1,sK2)) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_51,negated_conjecture,
v1_funct_1(sK2),
inference(cnf_transformation,[],[f220]) ).
tcf(c_52,negated_conjecture,
v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f219]) ).
tcf(c_53,negated_conjecture,
m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f218]) ).
tcf(c_54,negated_conjecture,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f217]) ).
tcf(c_55,negated_conjecture,
v2_pre_topc(sK1),
inference(cnf_transformation,[],[f216]) ).
tcf(c_56,negated_conjecture,
l1_pre_topc(sK1),
inference(cnf_transformation,[],[f215]) ).
tcf(c_58,negated_conjecture,
v2_pre_topc(sK0),
inference(cnf_transformation,[],[f213]) ).
tcf(c_59,negated_conjecture,
l1_pre_topc(sK0),
inference(cnf_transformation,[],[f212]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v1_funct_2(k8_waybel18(X1,X2,X0),u1_struct_0(X1),u1_struct_0(k7_waybel18(X1,X2,X0)))
| ~ l1_struct_0(X1)
| ~ l1_pre_topc(X2)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f232]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| m2_relset_1(k8_waybel18(X1,X2,X0),u1_struct_0(X1),u1_struct_0(k7_waybel18(X1,X2,X0)))
| ~ l1_struct_0(X1)
| ~ l1_pre_topc(X2)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| ( k8_waybel18(X1,X2,X0) = X0 )
| ~ l1_struct_0(X1)
| ~ l1_pre_topc(X2)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f234]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_pre_topc(k7_waybel18(X1,X2,X0),X2)
| ~ l1_struct_0(X1)
| ~ l1_pre_topc(X2)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f235]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k3_pre_topc(X2,k1_yellow_2(X1,X2,X0)) = k7_waybel18(X1,X2,X0) )
| ~ l1_struct_0(X1)
| ~ l1_pre_topc(X2)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f236]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f239]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i,X2: $i] :
( v2_waybel34(X2,X0,X1)
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X1)
| ~ v2_pre_topc(X0)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,sK8(X0,X1,X2)),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))
| ~ m1_subset_1(k4_pre_topc(X0,X1,X2,sK8(X0,X1,X2)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))))) ),
inference(cnf_transformation,[],[f246]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i,X2: $i] :
( v2_waybel34(X0,X1,X2)
| v3_pre_topc(sK8(X1,X2,X0),X1)
| ~ l1_pre_topc(X2)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X2)
| ~ v2_pre_topc(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f245]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i,X2: $i] :
( v2_waybel34(X0,X1,X2)
| m1_subset_1(sK8(X1,X2,X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_pre_topc(X2)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X2)
| ~ v2_pre_topc(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f244]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_pre_topc(k4_pre_topc(X1,X2,X0,X3),k3_pre_topc(X2,k1_yellow_2(X1,X2,X0)))
| ~ l1_pre_topc(X2)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X2)
| ~ v2_pre_topc(X1)
| ~ v1_funct_1(X0)
| ~ v3_pre_topc(X3,X1)
| ~ v2_waybel34(X0,X1,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f243]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_t_0topsp(X2,X0,X1)
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,sK9(X0,X1,X2)),X1) ),
inference(cnf_transformation,[],[f250]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_t_0topsp(X0,X1,X2)
| v3_pre_topc(sK9(X1,X2,X0),X1)
| ~ l1_pre_topc(X2)
| ~ l1_pre_topc(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_t_0topsp(X0,X1,X2)
| m1_subset_1(sK9(X1,X2,X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_pre_topc(X2)
| ~ l1_pre_topc(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f248]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_pre_topc(k4_pre_topc(X1,X2,X0,X3),X2)
| ~ l1_pre_topc(X2)
| ~ l1_pre_topc(X1)
| ~ v1_funct_1(X0)
| ~ v3_pre_topc(X3,X1)
| ~ v1_t_0topsp(X0,X1,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f247]) ).
tcf(c_90,plain,
! [X0: $i] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f253]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i] :
( l1_pre_topc(X0)
| ~ l1_pre_topc(X1)
| ~ m1_pre_topc(X0,X1) ),
inference(cnf_transformation,[],[f263]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k4_pre_topc(X1,X2,X0,X3) = k9_relat_1(X0,X3) )
| ~ l1_struct_0(X2)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f269]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_subset_1(k4_pre_topc(X1,X2,X0,X3),k1_zfmisc_1(u1_struct_0(X2)))
| ~ l1_struct_0(X2)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f270]) ).
tcf(c_194,plain,
( ~ v1_t_0topsp(k8_waybel18(sK0,sK1,sK2),sK0,k7_waybel18(sK0,sK1,sK2))
| ~ v2_waybel34(sK2,sK0,sK1) ),
inference(prop_impl_just,[status(thm)],[c_49]) ).
tcf(c_195,plain,
( ~ v2_waybel34(sK2,sK0,sK1)
| ~ v1_t_0topsp(k8_waybel18(sK0,sK1,sK2),sK0,k7_waybel18(sK0,sK1,sK2)) ),
inference(renaming,[status(thm)],[c_194]) ).
tcf(c_2583,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(sK8(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X1)
| ~ v2_pre_topc(X0)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_t_0topsp(k8_waybel18(sK0,sK1,sK2),sK0,k7_waybel18(sK0,sK1,sK2))
| ( X2 != sK2 )
| ( X1 != sK1 )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_195,c_81]) ).
tcf(c_2584,plain,
( m1_subset_1(sK8(sK0,sK1,sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_pre_topc(sK1)
| ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK1)
| ~ v2_pre_topc(sK0)
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_t_0topsp(k8_waybel18(sK0,sK1,sK2),sK0,k7_waybel18(sK0,sK1,sK2)) ),
inference(unflattening,[status(thm)],[c_2583]) ).
tcf(c_2585,plain,
( m1_subset_1(sK8(sK0,sK1,sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_t_0topsp(k8_waybel18(sK0,sK1,sK2),sK0,k7_waybel18(sK0,sK1,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_2584,c_59,c_58,c_56,c_55,c_51,c_53,c_52,c_2584]) ).
tcf(c_10403,plain,
l1_struct_0(sK1),
inference(superposition,[status(thm)],[c_56,c_90]) ).
tcf(c_10404,plain,
l1_struct_0(sK0),
inference(superposition,[status(thm)],[c_59,c_90]) ).
tcf(c_10471,plain,
m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(superposition,[status(thm)],[c_53,c_77]) ).
tcf(c_10486,plain,
! [X0: $i] :
( ( k4_pre_topc(sK0,sK1,sK2,X0) = k9_relat_1(sK2,X0) )
| ~ l1_struct_0(sK1)
| ~ l1_struct_0(sK0)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_10471,c_106]) ).
tcf(c_10488,plain,
! [X0: $i] : k4_pre_topc(sK0,sK1,sK2,X0) = k9_relat_1(sK2,X0),
inference(forward_subsumption_resolution,[status(thm)],[c_10486,c_10403,c_10404,c_51,c_52]) ).
tcf(c_11362,plain,
( m1_pre_topc(k7_waybel18(sK0,sK1,sK2),sK1)
| ~ l1_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v1_funct_1(sK2)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_52,c_72]) ).
tcf(c_11363,plain,
m1_pre_topc(k7_waybel18(sK0,sK1,sK2),sK1),
inference(forward_subsumption_resolution,[status(thm)],[c_11362,c_10404,c_56,c_51,c_10471]) ).
tcf(c_11400,plain,
( v3_struct_0(sK1)
| ( k8_waybel18(sK0,sK1,sK2) = sK2 )
| ~ l1_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_53,c_71]) ).
tcf(c_11403,plain,
k8_waybel18(sK0,sK1,sK2) = sK2,
inference(forward_subsumption_resolution,[status(thm)],[c_11400,c_54,c_10404,c_56,c_51,c_52]) ).
tcf(c_11416,plain,
( v2_waybel34(sK2,sK0,sK1)
| v1_t_0topsp(sK2,sK0,k7_waybel18(sK0,sK1,sK2)) ),
inference(demodulation,[status(thm)],[c_50,c_11403]) ).
tcf(c_11417,plain,
( ~ v2_waybel34(sK2,sK0,sK1)
| ~ v1_t_0topsp(sK2,sK0,k7_waybel18(sK0,sK1,sK2)) ),
inference(demodulation,[status(thm)],[c_49,c_11403]) ).
tcf(c_11425,plain,
( l1_pre_topc(k7_waybel18(sK0,sK1,sK2))
| ~ l1_pre_topc(sK1) ),
inference(superposition,[status(thm)],[c_11363,c_100]) ).
tcf(c_11426,plain,
l1_pre_topc(k7_waybel18(sK0,sK1,sK2)),
inference(forward_subsumption_resolution,[status(thm)],[c_11425,c_56]) ).
tcf(c_11428,plain,
l1_struct_0(k7_waybel18(sK0,sK1,sK2)),
inference(superposition,[status(thm)],[c_11426,c_90]) ).
tcf(c_11524,plain,
( ( k3_pre_topc(sK1,k1_yellow_2(sK0,sK1,sK2)) = k7_waybel18(sK0,sK1,sK2) )
| ~ l1_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_53,c_73]) ).
tcf(c_11527,plain,
k3_pre_topc(sK1,k1_yellow_2(sK0,sK1,sK2)) = k7_waybel18(sK0,sK1,sK2),
inference(forward_subsumption_resolution,[status(thm)],[c_11524,c_10404,c_56,c_51,c_52]) ).
tcf(c_11618,plain,
( v3_struct_0(sK1)
| v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2)))
| ~ l1_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v1_funct_1(sK2)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_11403,c_69]) ).
tcf(c_11622,plain,
v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2))),
inference(forward_subsumption_resolution,[status(thm)],[c_11618,c_54,c_10404,c_56,c_51,c_10471,c_52]) ).
tcf(c_11671,plain,
( v1_t_0topsp(sK2,sK0,k7_waybel18(sK0,sK1,sK2))
| v3_pre_topc(sK9(sK0,k7_waybel18(sK0,sK1,sK2),sK2),sK0)
| ~ l1_pre_topc(sK0)
| ~ v1_funct_1(sK2)
| ~ l1_pre_topc(k7_waybel18(sK0,sK1,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2))) ),
inference(superposition,[status(thm)],[c_11622,c_85]) ).
tcf(c_11681,plain,
( v1_t_0topsp(sK2,sK0,k7_waybel18(sK0,sK1,sK2))
| v3_pre_topc(sK9(sK0,k7_waybel18(sK0,sK1,sK2),sK2),sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11671,c_59,c_51,c_11426]) ).
tcf(c_11792,plain,
( v3_struct_0(sK1)
| m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2)))
| ~ l1_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v1_funct_1(sK2)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_11403,c_70]) ).
tcf(c_11796,plain,
m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2))),
inference(forward_subsumption_resolution,[status(thm)],[c_11792,c_54,c_10404,c_56,c_51,c_10471,c_52]) ).
tcf(c_11872,plain,
( v2_waybel34(sK2,sK0,sK1)
| v3_pre_topc(sK8(sK0,sK1,sK2),sK0)
| ~ l1_pre_topc(sK1)
| ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK1)
| ~ v2_pre_topc(sK0)
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_52,c_80]) ).
tcf(c_11875,plain,
( v2_waybel34(sK2,sK0,sK1)
| v3_pre_topc(sK8(sK0,sK1,sK2),sK0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11872,c_56,c_59,c_55,c_58,c_51,c_53]) ).
tcf(c_11987,plain,
m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2))),
inference(superposition,[status(thm)],[c_11796,c_77]) ).
tcf(c_12050,plain,
! [X0: $i] :
( ( k4_pre_topc(sK0,k7_waybel18(sK0,sK1,sK2),sK2,X0) = k9_relat_1(sK2,X0) )
| ~ l1_struct_0(sK0)
| ~ v1_funct_1(sK2)
| ~ l1_struct_0(k7_waybel18(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2))) ),
inference(superposition,[status(thm)],[c_11987,c_106]) ).
tcf(c_12059,plain,
! [X0: $i] : k4_pre_topc(sK0,k7_waybel18(sK0,sK1,sK2),sK2,X0) = k9_relat_1(sK2,X0),
inference(forward_subsumption_resolution,[status(thm)],[c_12050,c_10404,c_51,c_11428,c_11622]) ).
tcf(c_12062,plain,
! [X0: $i] :
( m1_subset_1(k9_relat_1(sK2,X0),k1_zfmisc_1(u1_struct_0(k7_waybel18(sK0,sK1,sK2))))
| ~ l1_struct_0(sK0)
| ~ v1_funct_1(sK2)
| ~ l1_struct_0(k7_waybel18(sK0,sK1,sK2))
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2)))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2))) ),
inference(superposition,[status(thm)],[c_12059,c_107]) ).
tcf(c_12063,plain,
( v1_t_0topsp(sK2,sK0,k7_waybel18(sK0,sK1,sK2))
| ~ l1_pre_topc(sK0)
| ~ v1_funct_1(sK2)
| ~ l1_pre_topc(k7_waybel18(sK0,sK1,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2)))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2)))
| ~ v3_pre_topc(k9_relat_1(sK2,sK9(sK0,k7_waybel18(sK0,sK1,sK2),sK2)),k7_waybel18(sK0,sK1,sK2)) ),
inference(superposition,[status(thm)],[c_12059,c_84]) ).
tcf(c_12064,plain,
! [X0: $i] : m1_subset_1(k9_relat_1(sK2,X0),k1_zfmisc_1(u1_struct_0(k7_waybel18(sK0,sK1,sK2)))),
inference(forward_subsumption_resolution,[status(thm)],[c_12062,c_10404,c_51,c_11428,c_11987,c_11622]) ).
tcf(c_12065,plain,
( v1_t_0topsp(sK2,sK0,k7_waybel18(sK0,sK1,sK2))
| ~ v3_pre_topc(k9_relat_1(sK2,sK9(sK0,k7_waybel18(sK0,sK1,sK2),sK2)),k7_waybel18(sK0,sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12063,c_59,c_51,c_11426,c_11796,c_11622]) ).
tcf(c_12098,plain,
! [X0: $i] :
( v3_pre_topc(k9_relat_1(sK2,X0),k7_waybel18(sK0,sK1,sK2))
| ~ l1_pre_topc(sK0)
| ~ v1_funct_1(sK2)
| ~ v3_pre_topc(X0,sK0)
| ~ l1_pre_topc(k7_waybel18(sK0,sK1,sK2))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_t_0topsp(sK2,sK0,k7_waybel18(sK0,sK1,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2)))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2))) ),
inference(superposition,[status(thm)],[c_12059,c_87]) ).
tcf(c_12105,plain,
! [X0: $i] :
( v3_pre_topc(k9_relat_1(sK2,X0),k7_waybel18(sK0,sK1,sK2))
| ~ v3_pre_topc(X0,sK0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_t_0topsp(sK2,sK0,k7_waybel18(sK0,sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12098,c_59,c_51,c_11426,c_11796,c_11622]) ).
tcf(c_12136,plain,
! [X0: $i] :
( v3_pre_topc(k4_pre_topc(sK0,sK1,sK2,X0),k7_waybel18(sK0,sK1,sK2))
| ~ l1_pre_topc(sK1)
| ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK1)
| ~ v2_pre_topc(sK0)
| ~ v1_funct_1(sK2)
| ~ v3_pre_topc(X0,sK0)
| ~ v2_waybel34(sK2,sK0,sK1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_11527,c_82]) ).
tcf(c_12138,plain,
! [X0: $i] :
( v3_pre_topc(k9_relat_1(sK2,X0),k7_waybel18(sK0,sK1,sK2))
| ~ l1_pre_topc(sK1)
| ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK1)
| ~ v2_pre_topc(sK0)
| ~ v1_funct_1(sK2)
| ~ v3_pre_topc(X0,sK0)
| ~ v2_waybel34(sK2,sK0,sK1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(light_normalisation,[status(thm)],[c_12136,c_10488]) ).
tcf(c_12139,plain,
! [X0: $i] :
( v3_pre_topc(k9_relat_1(sK2,X0),k7_waybel18(sK0,sK1,sK2))
| ~ v3_pre_topc(X0,sK0)
| ~ v2_waybel34(sK2,sK0,sK1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12138,c_56,c_59,c_55,c_58,c_51,c_53,c_52]) ).
tcf(c_12282,plain,
( v2_waybel34(sK2,sK0,sK1)
| ~ l1_pre_topc(sK1)
| ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK1)
| ~ v2_pre_topc(sK0)
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v3_pre_topc(k4_pre_topc(sK0,sK1,sK2,sK8(sK0,sK1,sK2)),k3_pre_topc(sK1,k1_yellow_2(sK0,sK1,sK2)))
| ~ m1_subset_1(k9_relat_1(sK2,sK8(sK0,sK1,sK2)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK1,k1_yellow_2(sK0,sK1,sK2))))) ),
inference(superposition,[status(thm)],[c_10488,c_79]) ).
tcf(c_12284,plain,
( v2_waybel34(sK2,sK0,sK1)
| ~ l1_pre_topc(sK1)
| ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK1)
| ~ v2_pre_topc(sK0)
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v3_pre_topc(k4_pre_topc(sK0,sK1,sK2,sK8(sK0,sK1,sK2)),k3_pre_topc(sK1,k1_yellow_2(sK0,sK1,sK2)))
| ~ m1_subset_1(k4_pre_topc(sK0,sK1,sK2,sK8(sK0,sK1,sK2)),k1_zfmisc_1(u1_struct_0(k7_waybel18(sK0,sK1,sK2)))) ),
inference(superposition,[status(thm)],[c_11527,c_79]) ).
tcf(c_12286,plain,
( v2_waybel34(sK2,sK0,sK1)
| ~ l1_pre_topc(sK1)
| ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK1)
| ~ v2_pre_topc(sK0)
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v3_pre_topc(k4_pre_topc(sK0,sK1,sK2,sK8(sK0,sK1,sK2)),k7_waybel18(sK0,sK1,sK2))
| ~ m1_subset_1(k4_pre_topc(sK0,sK1,sK2,sK8(sK0,sK1,sK2)),k1_zfmisc_1(u1_struct_0(k7_waybel18(sK0,sK1,sK2)))) ),
inference(light_normalisation,[status(thm)],[c_12284,c_11527]) ).
tcf(c_12287,plain,
( v2_waybel34(sK2,sK0,sK1)
| ~ v3_pre_topc(k4_pre_topc(sK0,sK1,sK2,sK8(sK0,sK1,sK2)),k7_waybel18(sK0,sK1,sK2))
| ~ m1_subset_1(k4_pre_topc(sK0,sK1,sK2,sK8(sK0,sK1,sK2)),k1_zfmisc_1(u1_struct_0(k7_waybel18(sK0,sK1,sK2)))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12286,c_56,c_59,c_55,c_58,c_51,c_53,c_52]) ).
tcf(c_12291,plain,
( v2_waybel34(sK2,sK0,sK1)
| ~ l1_pre_topc(sK1)
| ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK1)
| ~ v2_pre_topc(sK0)
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v3_pre_topc(k4_pre_topc(sK0,sK1,sK2,sK8(sK0,sK1,sK2)),k7_waybel18(sK0,sK1,sK2))
| ~ m1_subset_1(k9_relat_1(sK2,sK8(sK0,sK1,sK2)),k1_zfmisc_1(u1_struct_0(k7_waybel18(sK0,sK1,sK2)))) ),
inference(light_normalisation,[status(thm)],[c_12282,c_11527]) ).
tcf(c_12292,plain,
( v2_waybel34(sK2,sK0,sK1)
| ~ v3_pre_topc(k4_pre_topc(sK0,sK1,sK2,sK8(sK0,sK1,sK2)),k7_waybel18(sK0,sK1,sK2))
| ~ m1_subset_1(k9_relat_1(sK2,sK8(sK0,sK1,sK2)),k1_zfmisc_1(u1_struct_0(k7_waybel18(sK0,sK1,sK2)))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12291,c_56,c_59,c_55,c_58,c_51,c_53,c_52]) ).
tcf(c_12879,plain,
! [X0: $i] :
( v3_pre_topc(k9_relat_1(sK2,X0),k7_waybel18(sK0,sK1,sK2))
| ~ v3_pre_topc(X0,sK0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(global_subsumption_just,[status(thm)],[c_12139,c_11416,c_12105,c_12139]) ).
tcf(c_12888,plain,
( v1_t_0topsp(sK2,sK0,k7_waybel18(sK0,sK1,sK2))
| ~ v3_pre_topc(sK9(sK0,k7_waybel18(sK0,sK1,sK2),sK2),sK0)
| ~ m1_subset_1(sK9(sK0,k7_waybel18(sK0,sK1,sK2),sK2),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(superposition,[status(thm)],[c_12879,c_12065]) ).
tcf(c_12998,plain,
( v2_waybel34(sK2,sK0,sK1)
| ~ v3_pre_topc(k9_relat_1(sK2,sK8(sK0,sK1,sK2)),k7_waybel18(sK0,sK1,sK2))
| ~ m1_subset_1(k9_relat_1(sK2,sK8(sK0,sK1,sK2)),k1_zfmisc_1(u1_struct_0(k7_waybel18(sK0,sK1,sK2)))) ),
inference(demodulation,[status(thm)],[c_12292,c_10488]) ).
tcf(c_12999,plain,
( v2_waybel34(sK2,sK0,sK1)
| ~ v3_pre_topc(k9_relat_1(sK2,sK8(sK0,sK1,sK2)),k7_waybel18(sK0,sK1,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12998,c_12064]) ).
tcf(c_13006,plain,
( v2_waybel34(sK2,sK0,sK1)
| ~ v3_pre_topc(sK8(sK0,sK1,sK2),sK0)
| ~ m1_subset_1(sK8(sK0,sK1,sK2),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(superposition,[status(thm)],[c_12879,c_12999]) ).
tcf(c_13018,plain,
v2_waybel34(sK2,sK0,sK1),
inference(global_subsumption_just,[status(thm)],[c_12287,c_50,c_2585,c_11875,c_13006]) ).
tcf(c_13020,plain,
~ v1_t_0topsp(sK2,sK0,k7_waybel18(sK0,sK1,sK2)),
inference(backward_subsumption_resolution,[status(thm)],[c_11417,c_13018]) ).
tcf(c_13021,plain,
~ v3_pre_topc(k9_relat_1(sK2,sK9(sK0,k7_waybel18(sK0,sK1,sK2),sK2)),k7_waybel18(sK0,sK1,sK2)),
inference(backward_subsumption_resolution,[status(thm)],[c_12065,c_13020]) ).
tcf(c_13293,plain,
( ~ v3_pre_topc(sK9(sK0,k7_waybel18(sK0,sK1,sK2),sK2),sK0)
| ~ m1_subset_1(sK9(sK0,k7_waybel18(sK0,sK1,sK2),sK2),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(superposition,[status(thm)],[c_12879,c_13021]) ).
tcf(c_13577,plain,
~ m1_subset_1(sK9(sK0,k7_waybel18(sK0,sK1,sK2),sK2),k1_zfmisc_1(u1_struct_0(sK0))),
inference(global_subsumption_just,[status(thm)],[c_13293,c_11417,c_11681,c_11796,c_12888,c_13018]) ).
tcf(c_13579,plain,
( v1_t_0topsp(sK2,sK0,k7_waybel18(sK0,sK1,sK2))
| ~ l1_pre_topc(sK0)
| ~ v1_funct_1(sK2)
| ~ l1_pre_topc(k7_waybel18(sK0,sK1,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2)))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(k7_waybel18(sK0,sK1,sK2))) ),
inference(superposition,[status(thm)],[c_86,c_13577]) ).
tcf(c_13580,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_13579,c_13020,c_59,c_51,c_11426,c_11796,c_11622]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT363+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 21:22:27 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 1.35/1.73 % SZS status Started for theBenchmark.p
% 1.35/1.73 % SZS status Theorem for theBenchmark.p
% 1.35/1.73
% 1.35/1.73 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.35/1.73
% 1.35/1.73 % ------ iProver source info
% 1.35/1.73
% 1.35/1.73 % git: date: 2026-07-19 20:42:38 +0200
% 1.35/1.73 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.35/1.73 % git: non_committed_changes: false
% 1.35/1.73
% 1.35/1.73 % ------ Parsing...
% 1.35/1.73 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.35/1.73
% 1.35/1.73 % ------ Preprocessing... sup_sim: 0 sf_s rm: 11 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 3 0s sf_e pe_s pe_e %
% 1.35/1.73
% 1.35/1.73 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 1.35/1.73
% 1.35/1.73 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 1.35/1.73 % ------ Proving...
% 1.35/1.73 % ------ Problem Properties
% 1.35/1.73
% 1.35/1.73 %
% 1.35/1.73 % clauses 79
% 1.35/1.73 % conjectures 11
% 1.35/1.73 % EPR 26
% 1.35/1.73 % Horn 61
% 1.35/1.73 % unary 24
% 1.35/1.73 % binary 12
% 1.35/1.73 % lits 277
% 1.35/1.73 % lits eq 4
% 1.35/1.73 % fd_pure 0
% 1.35/1.73 % fd_pseudo 0
% 1.35/1.73 % fd_cond 0
% 1.35/1.73 % fd_pseudo_cond 1
% 1.35/1.73 % AC symbols 0
% 1.35/1.73
% 1.35/1.73 % ------ Schedule dynamic 5 is on
% 1.35/1.73
% 1.35/1.73 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 1.35/1.73
% 1.35/1.73
% 1.35/1.73 % ------
% 1.35/1.73 % Current options:
% 1.35/1.73 % ------
% 1.35/1.73
% 1.35/1.73
% 1.35/1.73 %
% 1.35/1.73
% 1.35/1.73 % ------ Proving...
% 1.35/1.73 %
% 1.35/1.73
% 1.35/1.73 % SZS status Theorem for theBenchmark.p
% 1.35/1.73
% 1.35/1.73 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.35/1.74
% 1.35/1.74
%------------------------------------------------------------------------------