%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : CAT034+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n016.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:01:17 PM UTC 2026
% Result : Theorem 135.81s 43.33s
% Output : CNFRefutation 135.81s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f222ERROR: Could not build tree for root c_257313ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u2_cat_1(X0))
=> m1_subset_1(k4_tarski(k4_tarski(k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))),k3_yoneda_1(X0,X1)),u2_cat_1(k12_nattra_1(X0,k1_yoneda_1(X0)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_yoneda_1) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u2_cat_1(X0))
=> m1_subset_1(k4_tarski(k4_tarski(k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))),k3_yoneda_1(X0,X1)),u2_cat_1(k12_nattra_1(X0,k1_yoneda_1(X0)))) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f8,axiom,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f9,axiom,
! [X0] :
( ( l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1) )
=> ! [X2] :
( m4_nattra_1(X2,X0,X1)
=> ( X2 = k11_nattra_1(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ? [X4] :
( ? [X5] :
( ? [X6] :
( r2_nattra_1(X0,X1,X4,X5)
& X3 = k4_tarski(k4_tarski(X4,X5),X6)
& m2_nattra_1(X6,X0,X1,X4,X5) )
& m2_cat_1(X5,X0,X1) )
& m2_cat_1(X4,X0,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d16_nattra_1) ).
fof(f13,axiom,
! [X0,X1] : k4_tarski(X0,X1) = k2_tarski(k2_tarski(X0,X1),k1_tarski(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_tarski) ).
fof(f17,axiom,
! [X0,X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> m4_nattra_1(k11_nattra_1(X0,X1),X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_nattra_1) ).
fof(f19,axiom,
! [X0,X1] :
( ( l1_cat_1(X1)
& v2_cat_1(X1)
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> ( l1_cat_1(k12_nattra_1(X0,X1))
& v2_cat_1(k12_nattra_1(X0,X1))
& v1_cat_1(k12_nattra_1(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k12_nattra_1) ).
fof(f27,axiom,
! [X0] :
( ( l1_cat_1(X0)
& v2_cat_1(X0) )
=> ( l1_cat_1(k1_yoneda_1(X0))
& v2_cat_1(k1_yoneda_1(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_yoneda_1) ).
fof(f30,axiom,
! [X0,X1] :
( ( m1_subset_1(X1,u2_cat_1(X0))
& l1_cat_1(X0) )
=> m1_subset_1(k2_cat_1(X0,X1),u1_cat_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_cat_1) ).
fof(f34,axiom,
! [X0,X1] :
( ( m1_subset_1(X1,u1_cat_1(X0))
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> m2_cat_1(k2_yoneda_1(X0,X1),X0,k1_yoneda_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_yoneda_1) ).
fof(f36,axiom,
! [X0,X1] :
( ( m1_subset_1(X1,u2_cat_1(X0))
& l1_cat_1(X0) )
=> m1_subset_1(k3_cat_1(X0,X1),u1_cat_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_cat_1) ).
fof(f37,axiom,
! [X0,X1] :
( ( m1_subset_1(X1,u2_cat_1(X0))
& l1_cat_1(X0)
& v2_cat_1(X0) )
=> m2_nattra_1(k3_yoneda_1(X0,X1),X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_yoneda_1) ).
fof(f89,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f92,axiom,
! [X0] :
( ( l1_cat_1(X0)
& v2_cat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u2_cat_1(X0))
=> r2_nattra_1(X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_yoneda_1) ).
fof(f103,plain,
? [X0] :
( l1_cat_1(X0)
& v2_cat_1(X0)
& ? [X1] :
( m1_subset_1(X1,u2_cat_1(X0))
& ~ m1_subset_1(k4_tarski(k4_tarski(k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))),k3_yoneda_1(X0,X1)),u2_cat_1(k12_nattra_1(X0,k1_yoneda_1(X0)))) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f104,plain,
? [X0] :
( l1_cat_1(X0)
& v2_cat_1(X0)
& ? [X1] :
( m1_subset_1(X1,u2_cat_1(X0))
& ~ m1_subset_1(k4_tarski(k4_tarski(k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))),k3_yoneda_1(X0,X1)),u2_cat_1(k12_nattra_1(X0,k1_yoneda_1(X0)))) ) ),
inference(flattening,[],[f103]) ).
fof(f112,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ m4_nattra_1(X2,X0,X1)
| ( X2 = k11_nattra_1(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ? [X4] :
( ? [X5] :
( ? [X6] :
( r2_nattra_1(X0,X1,X4,X5)
& X3 = k4_tarski(k4_tarski(X4,X5),X6)
& m2_nattra_1(X6,X0,X1,X4,X5) )
& m2_cat_1(X5,X0,X1) )
& m2_cat_1(X4,X0,X1) ) ) ) ) ) ),
inference(ennf_transformation,[],[f9]) ).
fof(f113,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ m4_nattra_1(X2,X0,X1)
| ( X2 = k11_nattra_1(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ? [X4] :
( ? [X5] :
( ? [X6] :
( r2_nattra_1(X0,X1,X4,X5)
& X3 = k4_tarski(k4_tarski(X4,X5),X6)
& m2_nattra_1(X6,X0,X1,X4,X5) )
& m2_cat_1(X5,X0,X1) )
& m2_cat_1(X4,X0,X1) ) ) ) ) ) ),
inference(flattening,[],[f112]) ).
fof(f126,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m4_nattra_1(k11_nattra_1(X0,X1),X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f127,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m4_nattra_1(k11_nattra_1(X0,X1),X0,X1) ),
inference(flattening,[],[f126]) ).
fof(f129,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ( l1_cat_1(k12_nattra_1(X0,X1))
& v2_cat_1(k12_nattra_1(X0,X1))
& v1_cat_1(k12_nattra_1(X0,X1)) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f130,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ( l1_cat_1(k12_nattra_1(X0,X1))
& v2_cat_1(k12_nattra_1(X0,X1))
& v1_cat_1(k12_nattra_1(X0,X1)) ) ),
inference(flattening,[],[f129]) ).
fof(f133,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ( l1_cat_1(k1_yoneda_1(X0))
& v2_cat_1(k1_yoneda_1(X0)) ) ),
inference(ennf_transformation,[],[f27]) ).
fof(f134,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ( l1_cat_1(k1_yoneda_1(X0))
& v2_cat_1(k1_yoneda_1(X0)) ) ),
inference(flattening,[],[f133]) ).
fof(f137,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u2_cat_1(X0))
| ~ l1_cat_1(X0)
| m1_subset_1(k2_cat_1(X0,X1),u1_cat_1(X0)) ),
inference(ennf_transformation,[],[f30]) ).
fof(f138,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u2_cat_1(X0))
| ~ l1_cat_1(X0)
| m1_subset_1(k2_cat_1(X0,X1),u1_cat_1(X0)) ),
inference(flattening,[],[f137]) ).
fof(f139,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_cat_1(X0))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k2_yoneda_1(X0,X1),X0,k1_yoneda_1(X0)) ),
inference(ennf_transformation,[],[f34]) ).
fof(f140,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_cat_1(X0))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k2_yoneda_1(X0,X1),X0,k1_yoneda_1(X0)) ),
inference(flattening,[],[f139]) ).
fof(f141,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u2_cat_1(X0))
| ~ l1_cat_1(X0)
| m1_subset_1(k3_cat_1(X0,X1),u1_cat_1(X0)) ),
inference(ennf_transformation,[],[f36]) ).
fof(f142,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u2_cat_1(X0))
| ~ l1_cat_1(X0)
| m1_subset_1(k3_cat_1(X0,X1),u1_cat_1(X0)) ),
inference(flattening,[],[f141]) ).
fof(f143,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u2_cat_1(X0))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_nattra_1(k3_yoneda_1(X0,X1),X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))) ),
inference(ennf_transformation,[],[f37]) ).
fof(f144,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u2_cat_1(X0))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_nattra_1(k3_yoneda_1(X0,X1),X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))) ),
inference(flattening,[],[f143]) ).
fof(f204,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f89]) ).
fof(f208,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u2_cat_1(X0))
| r2_nattra_1(X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))) ) ),
inference(ennf_transformation,[],[f92]) ).
fof(f209,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u2_cat_1(X0))
| r2_nattra_1(X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))) ) ),
inference(flattening,[],[f208]) ).
fof(f224,plain,
( l1_cat_1(sK6)
& v2_cat_1(sK6)
& m1_subset_1(sK7,u2_cat_1(sK6))
& ~ m1_subset_1(k4_tarski(k4_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)),k2_yoneda_1(sK6,k2_cat_1(sK6,sK7))),k3_yoneda_1(sK6,sK7)),u2_cat_1(k12_nattra_1(sK6,k1_yoneda_1(sK6)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X0,sK6),skolemize(X1,sK7)],[f104]) ).
fof(f225,plain,
! [X2,X0,X1] :
( ~ sP1(X2,X0,X1)
| ( ( k11_nattra_1(X0,X1) != X2
| sP0(X1,X0,X2) )
& ( ~ sP0(X1,X0,X2)
| X2 = k11_nattra_1(X0,X1) ) ) ),
inference(nnf_transformation,[],[f217]) ).
fof(f226,plain,
! [X0,X1,X2] :
( ~ sP1(X0,X1,X2)
| ( ( k11_nattra_1(X1,X2) != X0
| sP0(X2,X1,X0) )
& ( ~ sP0(X2,X1,X0)
| k11_nattra_1(X1,X2) = X0 ) ) ),
inference(rectify,[],[f225]) ).
fof(f230,plain,
! [X2,X0,X1] :
( ~ sP5(X2,X0,X1)
| ( ( k12_nattra_1(X0,X1) != X2
| sP4(X1,X0,X2) )
& ( ~ sP4(X1,X0,X2)
| X2 = k12_nattra_1(X0,X1) ) ) ),
inference(nnf_transformation,[],[f222]) ).
fof(f231,plain,
! [X0,X1,X2] :
( ~ sP5(X0,X1,X2)
| ( ( k12_nattra_1(X1,X2) != X0
| sP4(X2,X1,X0) )
& ( ~ sP4(X2,X1,X0)
| k12_nattra_1(X1,X2) = X0 ) ) ),
inference(rectify,[],[f230]) ).
fof(f232,plain,
! [X1,X0,X2] :
( ( ~ sP4(X1,X0,X2)
| ( sP2(X1,X0,X2)
& sP3(X2,X1,X0)
& ! [X4] :
( ~ m1_subset_1(X4,u2_cat_1(X2))
| ! [X5] :
( ~ m1_subset_1(X5,u2_cat_1(X2))
| k3_cat_1(X2,X4) != k2_cat_1(X2,X5)
| r2_hidden(k13_cat_2(X2,X2,X5,X4),k1_relat_1(u5_cat_1(X2))) ) )
& ! [X3] :
( ~ m1_subset_1(X3,u2_cat_1(X2))
| ( k3_cat_1(X2,X3) = k2_mcart_1(k1_mcart_1(X3))
& k2_cat_1(X2,X3) = k1_mcart_1(k1_mcart_1(X3)) ) )
& u2_cat_1(X2) = k11_nattra_1(X0,X1)
& u1_cat_1(X2) = k7_cat_2(X0,X1) ) )
& ( ~ sP2(X1,X0,X2)
| ~ sP3(X2,X1,X0)
| ? [X4] :
( m1_subset_1(X4,u2_cat_1(X2))
& ? [X5] :
( m1_subset_1(X5,u2_cat_1(X2))
& k3_cat_1(X2,X4) = k2_cat_1(X2,X5)
& ~ r2_hidden(k13_cat_2(X2,X2,X5,X4),k1_relat_1(u5_cat_1(X2))) ) )
| ? [X3] :
( m1_subset_1(X3,u2_cat_1(X2))
& ( k3_cat_1(X2,X3) != k2_mcart_1(k1_mcart_1(X3))
| k2_cat_1(X2,X3) != k1_mcart_1(k1_mcart_1(X3)) ) )
| k11_nattra_1(X0,X1) != u2_cat_1(X2)
| u1_cat_1(X2) != k7_cat_2(X0,X1)
| sP4(X1,X0,X2) ) ),
inference(nnf_transformation,[],[f221]) ).
fof(f233,plain,
! [X1,X0,X2] :
( ( ~ sP4(X1,X0,X2)
| ( sP2(X1,X0,X2)
& sP3(X2,X1,X0)
& ! [X4] :
( ~ m1_subset_1(X4,u2_cat_1(X2))
| ! [X5] :
( ~ m1_subset_1(X5,u2_cat_1(X2))
| k3_cat_1(X2,X4) != k2_cat_1(X2,X5)
| r2_hidden(k13_cat_2(X2,X2,X5,X4),k1_relat_1(u5_cat_1(X2))) ) )
& ! [X3] :
( ~ m1_subset_1(X3,u2_cat_1(X2))
| ( k3_cat_1(X2,X3) = k2_mcart_1(k1_mcart_1(X3))
& k2_cat_1(X2,X3) = k1_mcart_1(k1_mcart_1(X3)) ) )
& u2_cat_1(X2) = k11_nattra_1(X0,X1)
& u1_cat_1(X2) = k7_cat_2(X0,X1) ) )
& ( ~ sP2(X1,X0,X2)
| ~ sP3(X2,X1,X0)
| ? [X4] :
( m1_subset_1(X4,u2_cat_1(X2))
& ? [X5] :
( m1_subset_1(X5,u2_cat_1(X2))
& k3_cat_1(X2,X4) = k2_cat_1(X2,X5)
& ~ r2_hidden(k13_cat_2(X2,X2,X5,X4),k1_relat_1(u5_cat_1(X2))) ) )
| ? [X3] :
( m1_subset_1(X3,u2_cat_1(X2))
& ( k3_cat_1(X2,X3) != k2_mcart_1(k1_mcart_1(X3))
| k2_cat_1(X2,X3) != k1_mcart_1(k1_mcart_1(X3)) ) )
| k11_nattra_1(X0,X1) != u2_cat_1(X2)
| u1_cat_1(X2) != k7_cat_2(X0,X1)
| sP4(X1,X0,X2) ) ),
inference(flattening,[],[f232]) ).
fof(f234,plain,
! [X0,X1,X2] :
( ( ~ sP4(X0,X1,X2)
| ( sP2(X0,X1,X2)
& sP3(X2,X0,X1)
& ! [X7] :
( ~ m1_subset_1(X7,u2_cat_1(X2))
| ! [X8] :
( ~ m1_subset_1(X8,u2_cat_1(X2))
| k3_cat_1(X2,X7) != k2_cat_1(X2,X8)
| r2_hidden(k13_cat_2(X2,X2,X8,X7),k1_relat_1(u5_cat_1(X2))) ) )
& ! [X6] :
( ~ m1_subset_1(X6,u2_cat_1(X2))
| ( k3_cat_1(X2,X6) = k2_mcart_1(k1_mcart_1(X6))
& k2_cat_1(X2,X6) = k1_mcart_1(k1_mcart_1(X6)) ) )
& u2_cat_1(X2) = k11_nattra_1(X1,X0)
& u1_cat_1(X2) = k7_cat_2(X1,X0) ) )
& ( ~ sP2(X0,X1,X2)
| ~ sP3(X2,X0,X1)
| ? [X4] :
( m1_subset_1(X4,u2_cat_1(X2))
& ? [X5] :
( m1_subset_1(X5,u2_cat_1(X2))
& k3_cat_1(X2,X4) = k2_cat_1(X2,X5)
& ~ r2_hidden(k13_cat_2(X2,X2,X5,X4),k1_relat_1(u5_cat_1(X2))) ) )
| ? [X3] :
( m1_subset_1(X3,u2_cat_1(X2))
& ( k3_cat_1(X2,X3) != k2_mcart_1(k1_mcart_1(X3))
| k2_cat_1(X2,X3) != k1_mcart_1(k1_mcart_1(X3)) ) )
| u2_cat_1(X2) != k11_nattra_1(X1,X0)
| u1_cat_1(X2) != k7_cat_2(X1,X0)
| sP4(X0,X1,X2) ) ),
inference(rectify,[],[f233]) ).
fof(f235,plain,
! [X0,X1,X2] :
( ( ~ sP4(X0,X1,X2)
| ( sP2(X0,X1,X2)
& sP3(X2,X0,X1)
& ! [X7] :
( ~ m1_subset_1(X7,u2_cat_1(X2))
| ! [X8] :
( ~ m1_subset_1(X8,u2_cat_1(X2))
| k3_cat_1(X2,X7) != k2_cat_1(X2,X8)
| r2_hidden(k13_cat_2(X2,X2,X8,X7),k1_relat_1(u5_cat_1(X2))) ) )
& ! [X6] :
( ~ m1_subset_1(X6,u2_cat_1(X2))
| ( k3_cat_1(X2,X6) = k2_mcart_1(k1_mcart_1(X6))
& k2_cat_1(X2,X6) = k1_mcart_1(k1_mcart_1(X6)) ) )
& u2_cat_1(X2) = k11_nattra_1(X1,X0)
& u1_cat_1(X2) = k7_cat_2(X1,X0) ) )
& ( ~ sP2(X0,X1,X2)
| ~ sP3(X2,X0,X1)
| ( m1_subset_1(sK16(X2),u2_cat_1(X2))
& m1_subset_1(sK17(X2),u2_cat_1(X2))
& k3_cat_1(X2,sK16(X2)) = k2_cat_1(X2,sK17(X2))
& ~ r2_hidden(k13_cat_2(X2,X2,sK17(X2),sK16(X2)),k1_relat_1(u5_cat_1(X2))) )
| ( m1_subset_1(sK15(X2),u2_cat_1(X2))
& ( k3_cat_1(X2,sK15(X2)) != k2_mcart_1(k1_mcart_1(sK15(X2)))
| k2_cat_1(X2,sK15(X2)) != k1_mcart_1(k1_mcart_1(sK15(X2))) ) )
| u2_cat_1(X2) != k11_nattra_1(X1,X0)
| u1_cat_1(X2) != k7_cat_2(X1,X0)
| sP4(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16,sK17]),skolemize(X3,sK15(X2)),skolemize(X4,sK16(X2)),skolemize(X5,sK17(X2))],[f234]) ).
fof(f258,plain,
l1_cat_1(sK6),
inference(cnf_transformation,[],[f224]) ).
fof(f259,plain,
v2_cat_1(sK6),
inference(cnf_transformation,[],[f224]) ).
fof(f260,plain,
m1_subset_1(sK7,u2_cat_1(sK6)),
inference(cnf_transformation,[],[f224]) ).
fof(f261,plain,
~ m1_subset_1(k4_tarski(k4_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)),k2_yoneda_1(sK6,k2_cat_1(sK6,sK7))),k3_yoneda_1(sK6,sK7)),u2_cat_1(k12_nattra_1(sK6,k1_yoneda_1(sK6)))),
inference(cnf_transformation,[],[f224]) ).
fof(f268,plain,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
inference(cnf_transformation,[],[f8]) ).
fof(f269,plain,
! [X2,X0,X1] :
( ~ sP1(X0,X1,X2)
| k11_nattra_1(X1,X2) != X0
| sP0(X2,X1,X0) ),
inference(cnf_transformation,[],[f226]) ).
fof(f283,plain,
! [X2,X0,X1] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m4_nattra_1(X2,X0,X1)
| sP1(X2,X0,X1) ),
inference(cnf_transformation,[],[f218]) ).
fof(f284,plain,
! [X2,X0,X1] :
( ~ sP5(X0,X1,X2)
| k12_nattra_1(X1,X2) != X0
| sP4(X2,X1,X0) ),
inference(cnf_transformation,[],[f231]) ).
fof(f291,plain,
! [X2,X0,X1] :
( ~ sP4(X0,X1,X2)
| u2_cat_1(X2) = k11_nattra_1(X1,X0) ),
inference(cnf_transformation,[],[f235]) ).
fof(f318,plain,
! [X2,X0,X1] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X2)
| ~ v1_cat_1(X2)
| sP5(X2,X0,X1) ),
inference(cnf_transformation,[],[f223]) ).
fof(f321,plain,
! [X0,X1] : k4_tarski(X0,X1) = k2_tarski(k2_tarski(X0,X1),k1_tarski(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f327,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m4_nattra_1(k11_nattra_1(X0,X1),X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
fof(f329,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| l1_cat_1(k12_nattra_1(X0,X1)) ),
inference(cnf_transformation,[],[f130]) ).
fof(f330,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| v2_cat_1(k12_nattra_1(X0,X1)) ),
inference(cnf_transformation,[],[f130]) ).
fof(f331,plain,
! [X0,X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| v1_cat_1(k12_nattra_1(X0,X1)) ),
inference(cnf_transformation,[],[f130]) ).
fof(f333,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| l1_cat_1(k1_yoneda_1(X0)) ),
inference(cnf_transformation,[],[f134]) ).
fof(f334,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| v2_cat_1(k1_yoneda_1(X0)) ),
inference(cnf_transformation,[],[f134]) ).
fof(f338,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u2_cat_1(X0))
| ~ l1_cat_1(X0)
| m1_subset_1(k2_cat_1(X0,X1),u1_cat_1(X0)) ),
inference(cnf_transformation,[],[f138]) ).
fof(f339,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_cat_1(X0))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_cat_1(k2_yoneda_1(X0,X1),X0,k1_yoneda_1(X0)) ),
inference(cnf_transformation,[],[f140]) ).
fof(f340,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u2_cat_1(X0))
| ~ l1_cat_1(X0)
| m1_subset_1(k3_cat_1(X0,X1),u1_cat_1(X0)) ),
inference(cnf_transformation,[],[f142]) ).
fof(f341,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u2_cat_1(X0))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| m2_nattra_1(k3_yoneda_1(X0,X1),X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))) ),
inference(cnf_transformation,[],[f144]) ).
fof(f411,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f204]) ).
fof(f414,plain,
! [X0,X1] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ~ m1_subset_1(X1,u2_cat_1(X0))
| r2_nattra_1(X0,k1_yoneda_1(X0),k2_yoneda_1(X0,k3_cat_1(X0,X1)),k2_yoneda_1(X0,k2_cat_1(X0,X1))) ),
inference(cnf_transformation,[],[f209]) ).
fof(f420,plain,
~ m1_subset_1(k2_tarski(k2_tarski(k2_tarski(k2_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)),k2_yoneda_1(sK6,k2_cat_1(sK6,sK7))),k1_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)))),k3_yoneda_1(sK6,sK7)),k1_tarski(k2_tarski(k2_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)),k2_yoneda_1(sK6,k2_cat_1(sK6,sK7))),k1_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)))))),u2_cat_1(k12_nattra_1(sK6,k1_yoneda_1(sK6)))),
inference(definition_unfolding,[],[f261,f321,f321]) ).
fof(f432,plain,
! [X2,X1] :
( ~ sP1(k11_nattra_1(X1,X2),X1,X2)
| sP0(X2,X1,k11_nattra_1(X1,X2)) ),
inference(equality_resolution,[],[f269]) ).
fof(f434,plain,
! [X2,X1] :
( ~ sP5(k12_nattra_1(X1,X2),X1,X2)
| sP4(X2,X1,k12_nattra_1(X1,X2)) ),
inference(equality_resolution,[],[f284]) ).
tcf(c_49,negated_conjecture,
~ m1_subset_1(k2_tarski(k2_tarski(k2_tarski(k2_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)),k2_yoneda_1(sK6,k2_cat_1(sK6,sK7))),k1_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)))),k3_yoneda_1(sK6,sK7)),k1_tarski(k2_tarski(k2_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)),k2_yoneda_1(sK6,k2_cat_1(sK6,sK7))),k1_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)))))),u2_cat_1(k12_nattra_1(sK6,k1_yoneda_1(sK6)))),
inference(cnf_transformation,[],[f420]) ).
tcf(c_50,negated_conjecture,
m1_subset_1(sK7,u2_cat_1(sK6)),
inference(cnf_transformation,[],[f260]) ).
tcf(c_51,negated_conjecture,
v2_cat_1(sK6),
inference(cnf_transformation,[],[f259]) ).
tcf(c_52,negated_conjecture,
l1_cat_1(sK6),
inference(cnf_transformation,[],[f258]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
inference(cnf_transformation,[],[f268]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( sP0(X1,X0,k11_nattra_1(X0,X1))
| ~ sP1(k11_nattra_1(X0,X1),X0,X1) ),
inference(cnf_transformation,[],[f432]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0,X1,X2)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ m4_nattra_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f283]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( sP4(X1,X0,k12_nattra_1(X0,X1))
| ~ sP5(k12_nattra_1(X0,X1),X0,X1) ),
inference(cnf_transformation,[],[f434]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k11_nattra_1(X1,X0) = u2_cat_1(X2) )
| ~ sP4(X0,X1,X2) ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP5(X2,X0,X1)
| ~ v1_cat_1(X2)
| ~ l1_cat_1(X2)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X2)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0) ),
inference(cnf_transformation,[],[f318]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i] :
( m4_nattra_1(k11_nattra_1(X0,X1),X0,X1)
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0) ),
inference(cnf_transformation,[],[f327]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i] :
( v1_cat_1(k12_nattra_1(X0,X1))
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0) ),
inference(cnf_transformation,[],[f331]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i] :
( v2_cat_1(k12_nattra_1(X0,X1))
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0) ),
inference(cnf_transformation,[],[f330]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i] :
( l1_cat_1(k12_nattra_1(X0,X1))
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0) ),
inference(cnf_transformation,[],[f329]) ).
tcf(c_121,plain,
! [X0: $i] :
( v2_cat_1(k1_yoneda_1(X0))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0) ),
inference(cnf_transformation,[],[f334]) ).
tcf(c_122,plain,
! [X0: $i] :
( l1_cat_1(k1_yoneda_1(X0))
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X0) ),
inference(cnf_transformation,[],[f333]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(k2_cat_1(X1,X0),u1_cat_1(X1))
| ~ l1_cat_1(X1)
| ~ m1_subset_1(X0,u2_cat_1(X1)) ),
inference(cnf_transformation,[],[f338]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i] :
( m2_cat_1(k2_yoneda_1(X1,X0),X1,k1_yoneda_1(X1))
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m1_subset_1(X0,u1_cat_1(X1)) ),
inference(cnf_transformation,[],[f339]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(k3_cat_1(X1,X0),u1_cat_1(X1))
| ~ l1_cat_1(X1)
| ~ m1_subset_1(X0,u2_cat_1(X1)) ),
inference(cnf_transformation,[],[f340]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i] :
( m2_nattra_1(k3_yoneda_1(X1,X0),X1,k1_yoneda_1(X1),k2_yoneda_1(X1,k3_cat_1(X1,X0)),k2_yoneda_1(X1,k2_cat_1(X1,X0)))
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m1_subset_1(X0,u2_cat_1(X1)) ),
inference(cnf_transformation,[],[f341]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f411]) ).
tcf(c_202,plain,
! [X0: $i,X1: $i] :
( r2_nattra_1(X1,k1_yoneda_1(X1),k2_yoneda_1(X1,k3_cat_1(X1,X0)),k2_yoneda_1(X1,k2_cat_1(X1,X0)))
| ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ~ m1_subset_1(X0,u2_cat_1(X1)) ),
inference(cnf_transformation,[],[f414]) ).
tcf(c_393,plain,
! [X0: $i,X1: $i] :
( sP0(X1,X0,k11_nattra_1(X0,X1))
| ~ sP1(k11_nattra_1(X0,X1),X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_59]) ).
tcf(c_403,plain,
! [X0: $i,X1: $i] :
( sP4(X1,X0,k12_nattra_1(X0,X1))
| ~ sP5(k12_nattra_1(X0,X1),X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_74]) ).
tcf(c_3037,plain,
~ m1_subset_1(k2_tarski(k1_tarski(k2_tarski(k1_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7))),k2_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)),k2_yoneda_1(sK6,k2_cat_1(sK6,sK7))))),k2_tarski(k3_yoneda_1(sK6,sK7),k2_tarski(k1_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7))),k2_tarski(k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)),k2_yoneda_1(sK6,k2_cat_1(sK6,sK7)))))),u2_cat_1(k12_nattra_1(sK6,k1_yoneda_1(sK6)))),
inference(demodulation,[status(thm)],[c_49,c_57]) ).
tcf(c_3561,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP0(X1,X0,k11_nattra_1(X0,X1))
| ~ l1_cat_1(X4)
| ~ l1_cat_1(X3)
| ~ v2_cat_1(X4)
| ~ v2_cat_1(X3)
| ~ m4_nattra_1(X2,X3,X4)
| ( X1 != X4 )
| ( X0 != X3 )
| ( k11_nattra_1(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_72,c_393]) ).
tcf(c_3562,plain,
! [X0: $i,X1: $i] :
( sP0(X1,X0,k11_nattra_1(X0,X1))
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ m4_nattra_1(k11_nattra_1(X0,X1),X0,X1) ),
inference(unflattening,[status(thm)],[c_3561]) ).
tcf(c_3564,plain,
! [X0: $i,X1: $i] :
( sP0(X1,X0,k11_nattra_1(X0,X1))
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_3562,c_115,c_3562]) ).
tcf(c_3662,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP4(X1,X0,k12_nattra_1(X0,X1))
| ~ v1_cat_1(X2)
| ~ l1_cat_1(X4)
| ~ l1_cat_1(X3)
| ~ l1_cat_1(X2)
| ~ v2_cat_1(X4)
| ~ v2_cat_1(X3)
| ~ v2_cat_1(X2)
| ( X1 != X4 )
| ( X0 != X3 )
| ( k12_nattra_1(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_403,c_107]) ).
tcf(c_3663,plain,
! [X0: $i,X1: $i] :
( sP4(X1,X0,k12_nattra_1(X0,X1))
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0)
| ~ v1_cat_1(k12_nattra_1(X0,X1))
| ~ l1_cat_1(k12_nattra_1(X0,X1))
| ~ v2_cat_1(k12_nattra_1(X0,X1)) ),
inference(unflattening,[status(thm)],[c_3662]) ).
tcf(c_3665,plain,
! [X0: $i,X1: $i] :
( sP4(X1,X0,k12_nattra_1(X0,X1))
| ~ l1_cat_1(X1)
| ~ l1_cat_1(X0)
| ~ v2_cat_1(X1)
| ~ v2_cat_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_3663,c_119,c_118,c_117,c_3663]) ).
tcf(c_20859,definition,
iPr_def_10 = k3_cat_1(sK6,sK7),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_20860,definition,
iPr_def_11 = k2_yoneda_1(sK6,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_20861,definition,
iPr_def_12 = k1_tarski(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_20862,definition,
iPr_def_13 = k2_cat_1(sK6,sK7),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_20863,definition,
iPr_def_14 = k2_yoneda_1(sK6,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_20864,definition,
iPr_def_15 = k2_tarski(iPr_def_11,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_20865,definition,
iPr_def_16 = k2_tarski(iPr_def_12,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_20866,definition,
iPr_def_17 = k1_tarski(iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_20867,definition,
iPr_def_18 = k3_yoneda_1(sK6,sK7),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_20868,definition,
iPr_def_19 = k2_tarski(iPr_def_18,iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_20869,definition,
iPr_def_20 = k2_tarski(iPr_def_17,iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_20870,definition,
iPr_def_21 = k1_yoneda_1(sK6),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_20871,definition,
iPr_def_22 = k12_nattra_1(sK6,iPr_def_21),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_20872,definition,
iPr_def_23 = u2_cat_1(iPr_def_22),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_20873,definition,
iPr_def_24 = u2_cat_1(sK6),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_20874,plain,
~ m1_subset_1(iPr_def_20,iPr_def_23),
inference(demodulation,[status(thm)],[c_3037,c_20870,c_20871,c_20872,c_20867,c_20868,c_20862,c_20863,c_20864,c_20859,c_20860,c_20861,c_20865,c_20866,c_20869]) ).
tcf(c_20875,negated_conjecture,
l1_cat_1(sK6),
inference(demodulation,[status(thm)],[c_52]) ).
tcf(c_20876,negated_conjecture,
v2_cat_1(sK6),
inference(demodulation,[status(thm)],[c_51]) ).
tcf(c_20877,negated_conjecture,
m1_subset_1(sK7,iPr_def_24),
inference(demodulation,[status(thm)],[c_50,c_20873]) ).
tcf(c_25161,plain,
k2_tarski(iPr_def_16,iPr_def_18) = iPr_def_19,
inference(demodulation,[status(thm)],[c_20868,c_57]) ).
tcf(c_25951,plain,
( m1_subset_1(iPr_def_13,u1_cat_1(sK6))
| ~ l1_cat_1(sK6)
| ~ m1_subset_1(sK7,u2_cat_1(sK6)) ),
inference(superposition,[status(thm)],[c_20862,c_126]) ).
tcf(c_25953,plain,
( m1_subset_1(iPr_def_13,u1_cat_1(sK6))
| ~ l1_cat_1(sK6)
| ~ m1_subset_1(sK7,iPr_def_24) ),
inference(light_normalisation,[status(thm)],[c_25951,c_20873]) ).
tcf(c_25954,plain,
m1_subset_1(iPr_def_13,u1_cat_1(sK6)),
inference(forward_subsumption_resolution,[status(thm)],[c_25953,c_20875,c_20877]) ).
tcf(c_26024,plain,
( m1_subset_1(iPr_def_10,u1_cat_1(sK6))
| ~ l1_cat_1(sK6)
| ~ m1_subset_1(sK7,u2_cat_1(sK6)) ),
inference(superposition,[status(thm)],[c_20859,c_128]) ).
tcf(c_26026,plain,
( m1_subset_1(iPr_def_10,u1_cat_1(sK6))
| ~ l1_cat_1(sK6)
| ~ m1_subset_1(sK7,iPr_def_24) ),
inference(light_normalisation,[status(thm)],[c_26024,c_20873]) ).
tcf(c_26027,plain,
m1_subset_1(iPr_def_10,u1_cat_1(sK6)),
inference(forward_subsumption_resolution,[status(thm)],[c_26026,c_20875,c_20877]) ).
tcf(c_26496,plain,
( m2_cat_1(iPr_def_11,sK6,k1_yoneda_1(sK6))
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(iPr_def_10,u1_cat_1(sK6)) ),
inference(superposition,[status(thm)],[c_20860,c_127]) ).
tcf(c_26497,plain,
( m2_cat_1(iPr_def_14,sK6,k1_yoneda_1(sK6))
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(iPr_def_13,u1_cat_1(sK6)) ),
inference(superposition,[status(thm)],[c_20863,c_127]) ).
tcf(c_26499,plain,
( m2_cat_1(iPr_def_14,sK6,iPr_def_21)
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(iPr_def_13,u1_cat_1(sK6)) ),
inference(light_normalisation,[status(thm)],[c_26497,c_20870]) ).
tcf(c_26500,plain,
m2_cat_1(iPr_def_14,sK6,iPr_def_21),
inference(forward_subsumption_resolution,[status(thm)],[c_26499,c_20875,c_20876,c_25954]) ).
tcf(c_26501,plain,
( m2_cat_1(iPr_def_11,sK6,iPr_def_21)
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(iPr_def_10,u1_cat_1(sK6)) ),
inference(light_normalisation,[status(thm)],[c_26496,c_20870]) ).
tcf(c_26502,plain,
m2_cat_1(iPr_def_11,sK6,iPr_def_21),
inference(forward_subsumption_resolution,[status(thm)],[c_26501,c_20875,c_20876,c_26027]) ).
tcf(c_27496,plain,
( r2_nattra_1(sK6,k1_yoneda_1(sK6),k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)),k2_yoneda_1(sK6,iPr_def_13))
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(sK7,u2_cat_1(sK6)) ),
inference(superposition,[status(thm)],[c_20862,c_202]) ).
tcf(c_27497,plain,
( r2_nattra_1(sK6,iPr_def_21,iPr_def_11,iPr_def_14)
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(sK7,iPr_def_24) ),
inference(light_normalisation,[status(thm)],[c_27496,c_20859,c_20860,c_20863,c_20870,c_20873]) ).
tcf(c_27498,plain,
r2_nattra_1(sK6,iPr_def_21,iPr_def_11,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_27497,c_20875,c_20876,c_20877]) ).
tcf(c_27767,plain,
( m2_nattra_1(k3_yoneda_1(sK6,sK7),sK6,k1_yoneda_1(sK6),k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)),k2_yoneda_1(sK6,iPr_def_13))
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(sK7,u2_cat_1(sK6)) ),
inference(superposition,[status(thm)],[c_20862,c_129]) ).
tcf(c_27768,plain,
( m2_nattra_1(iPr_def_18,sK6,iPr_def_21,iPr_def_11,iPr_def_14)
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(sK7,iPr_def_24) ),
inference(light_normalisation,[status(thm)],[c_27767,c_20859,c_20860,c_20863,c_20867,c_20870,c_20873]) ).
tcf(c_27769,plain,
m2_nattra_1(iPr_def_18,sK6,iPr_def_21,iPr_def_11,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_27768,c_20875,c_20876,c_20877]) ).
tcf(c_246625,plain,
( v2_cat_1(iPr_def_21)
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6) ),
inference(superposition,[status(thm)],[c_20870,c_121]) ).
tcf(c_246627,plain,
v2_cat_1(iPr_def_21),
inference(forward_subsumption_resolution,[status(thm)],[c_246625,c_20875,c_20876]) ).
tcf(c_246638,plain,
( l1_cat_1(iPr_def_21)
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6) ),
inference(superposition,[status(thm)],[c_20870,c_122]) ).
tcf(c_246639,plain,
l1_cat_1(iPr_def_21),
inference(forward_subsumption_resolution,[status(thm)],[c_246638,c_20875,c_20876]) ).
tcf(c_246711,plain,
( m1_subset_1(iPr_def_13,u1_cat_1(sK6))
| ~ l1_cat_1(sK6)
| ~ m1_subset_1(sK7,u2_cat_1(sK6)) ),
inference(superposition,[status(thm)],[c_20862,c_126]) ).
tcf(c_246712,plain,
( m1_subset_1(iPr_def_13,u1_cat_1(sK6))
| ~ l1_cat_1(sK6)
| ~ m1_subset_1(sK7,iPr_def_24) ),
inference(light_normalisation,[status(thm)],[c_246711,c_20873]) ).
tcf(c_246713,plain,
m1_subset_1(iPr_def_13,u1_cat_1(sK6)),
inference(forward_subsumption_resolution,[status(thm)],[c_246712,c_20875,c_20877]) ).
tcf(c_246766,plain,
( m2_nattra_1(k3_yoneda_1(sK6,sK7),sK6,k1_yoneda_1(sK6),k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)),k2_yoneda_1(sK6,iPr_def_13))
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(sK7,u2_cat_1(sK6)) ),
inference(superposition,[status(thm)],[c_20862,c_129]) ).
tcf(c_246767,plain,
( m2_nattra_1(iPr_def_18,sK6,iPr_def_21,iPr_def_11,iPr_def_14)
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(sK7,iPr_def_24) ),
inference(light_normalisation,[status(thm)],[c_246766,c_20859,c_20860,c_20863,c_20867,c_20870,c_20873]) ).
tcf(c_246768,plain,
m2_nattra_1(iPr_def_18,sK6,iPr_def_21,iPr_def_11,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_246767,c_20875,c_20876,c_20877]) ).
tcf(c_246891,plain,
( m2_cat_1(iPr_def_14,sK6,k1_yoneda_1(sK6))
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(iPr_def_13,u1_cat_1(sK6)) ),
inference(superposition,[status(thm)],[c_20863,c_127]) ).
tcf(c_246892,plain,
( m2_cat_1(iPr_def_14,sK6,iPr_def_21)
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(iPr_def_13,u1_cat_1(sK6)) ),
inference(light_normalisation,[status(thm)],[c_246891,c_20870]) ).
tcf(c_246893,plain,
m2_cat_1(iPr_def_14,sK6,iPr_def_21),
inference(forward_subsumption_resolution,[status(thm)],[c_246892,c_20875,c_20876,c_246713]) ).
tcf(c_247124,plain,
k2_tarski(iPr_def_16,iPr_def_18) = iPr_def_19,
inference(demodulation,[status(thm)],[c_20868,c_57]) ).
tcf(c_247795,plain,
( r2_nattra_1(sK6,k1_yoneda_1(sK6),k2_yoneda_1(sK6,k3_cat_1(sK6,sK7)),k2_yoneda_1(sK6,iPr_def_13))
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(sK7,u2_cat_1(sK6)) ),
inference(superposition,[status(thm)],[c_20862,c_202]) ).
tcf(c_247796,plain,
( r2_nattra_1(sK6,iPr_def_21,iPr_def_11,iPr_def_14)
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(sK6)
| ~ m1_subset_1(sK7,iPr_def_24) ),
inference(light_normalisation,[status(thm)],[c_247795,c_20859,c_20860,c_20863,c_20870,c_20873]) ).
tcf(c_247797,plain,
r2_nattra_1(sK6,iPr_def_21,iPr_def_11,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_247796,c_20875,c_20876,c_20877]) ).
tcf(c_248522,plain,
( sP4(iPr_def_21,sK6,iPr_def_22)
| ~ l1_cat_1(iPr_def_21)
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(iPr_def_21)
| ~ v2_cat_1(sK6) ),
inference(superposition,[status(thm)],[c_20871,c_3665]) ).
tcf(c_248530,plain,
sP4(iPr_def_21,sK6,iPr_def_22),
inference(forward_subsumption_resolution,[status(thm)],[c_248522,c_246639,c_20875,c_246627,c_20876]) ).
tcf(c_248596,plain,
k11_nattra_1(sK6,iPr_def_21) = u2_cat_1(iPr_def_22),
inference(superposition,[status(thm)],[c_248530,c_84]) ).
tcf(c_248598,plain,
k11_nattra_1(sK6,iPr_def_21) = iPr_def_23,
inference(light_normalisation,[status(thm)],[c_248596,c_20872]) ).
tcf(c_248809,plain,
( sP0(iPr_def_21,sK6,iPr_def_23)
| ~ l1_cat_1(iPr_def_21)
| ~ l1_cat_1(sK6)
| ~ v2_cat_1(iPr_def_21)
| ~ v2_cat_1(sK6) ),
inference(superposition,[status(thm)],[c_248598,c_3564]) ).
tcf(c_248814,plain,
sP0(iPr_def_21,sK6,iPr_def_23),
inference(forward_subsumption_resolution,[status(thm)],[c_248809,c_246639,c_20875,c_246627,c_20876]) ).
fof(f216,definition,
! [X1,X0,X2] :
( sP0(X1,X0,X2)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ? [X4] :
( ? [X5] :
( ? [X6] :
( r2_nattra_1(X0,X1,X4,X5)
& X3 = k4_tarski(k4_tarski(X4,X5),X6)
& m2_nattra_1(X6,X0,X1,X4,X5) )
& m2_cat_1(X5,X0,X1) )
& m2_cat_1(X4,X0,X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f217,definition,
! [X2,X0,X1] :
( ~ sP1(X2,X0,X1)
| ( X2 = k11_nattra_1(X0,X1)
<=> sP0(X1,X0,X2) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f218,plain,
! [X0] :
( ~ l1_cat_1(X0)
| ~ v2_cat_1(X0)
| ! [X1] :
( ~ l1_cat_1(X1)
| ~ v2_cat_1(X1)
| ! [X2] :
( ~ m4_nattra_1(X2,X0,X1)
| sP1(X2,X0,X1) ) ) ),
inference(definition_folding,[],[f113,f217,f216]) ).
fof(f227,plain,
! [X1,X0,X2] :
( ( ~ sP0(X1,X0,X2)
| ! [X3] :
( ( ~ r2_hidden(X3,X2)
| ? [X4] :
( ? [X5] :
( ? [X6] :
( r2_nattra_1(X0,X1,X4,X5)
& X3 = k4_tarski(k4_tarski(X4,X5),X6)
& m2_nattra_1(X6,X0,X1,X4,X5) )
& m2_cat_1(X5,X0,X1) )
& m2_cat_1(X4,X0,X1) ) )
& ( ! [X4] :
( ! [X5] :
( ! [X6] :
( ~ r2_nattra_1(X0,X1,X4,X5)
| k4_tarski(k4_tarski(X4,X5),X6) != X3
| ~ m2_nattra_1(X6,X0,X1,X4,X5) )
| ~ m2_cat_1(X5,X0,X1) )
| ~ m2_cat_1(X4,X0,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ? [X3] :
( ( r2_hidden(X3,X2)
| ? [X4] :
( ? [X5] :
( ? [X6] :
( r2_nattra_1(X0,X1,X4,X5)
& X3 = k4_tarski(k4_tarski(X4,X5),X6)
& m2_nattra_1(X6,X0,X1,X4,X5) )
& m2_cat_1(X5,X0,X1) )
& m2_cat_1(X4,X0,X1) ) )
& ( ~ r2_hidden(X3,X2)
| ! [X4] :
( ! [X5] :
( ! [X6] :
( ~ r2_nattra_1(X0,X1,X4,X5)
| k4_tarski(k4_tarski(X4,X5),X6) != X3
| ~ m2_nattra_1(X6,X0,X1,X4,X5) )
| ~ m2_cat_1(X5,X0,X1) )
| ~ m2_cat_1(X4,X0,X1) ) ) )
| sP0(X1,X0,X2) ) ),
inference(nnf_transformation,[],[f216]) ).
fof(f228,plain,
! [X0,X1,X2] :
( ( ~ sP0(X0,X1,X2)
| ! [X10] :
( ( ~ r2_hidden(X10,X2)
| ? [X14] :
( ? [X15] :
( ? [X16] :
( r2_nattra_1(X1,X0,X14,X15)
& k4_tarski(k4_tarski(X14,X15),X16) = X10
& m2_nattra_1(X16,X1,X0,X14,X15) )
& m2_cat_1(X15,X1,X0) )
& m2_cat_1(X14,X1,X0) ) )
& ( ! [X11] :
( ! [X12] :
( ! [X13] :
( ~ r2_nattra_1(X1,X0,X11,X12)
| k4_tarski(k4_tarski(X11,X12),X13) != X10
| ~ m2_nattra_1(X13,X1,X0,X11,X12) )
| ~ m2_cat_1(X12,X1,X0) )
| ~ m2_cat_1(X11,X1,X0) )
| r2_hidden(X10,X2) ) ) )
& ( ? [X3] :
( ( r2_hidden(X3,X2)
| ? [X7] :
( ? [X8] :
( ? [X9] :
( r2_nattra_1(X1,X0,X7,X8)
& k4_tarski(k4_tarski(X7,X8),X9) = X3
& m2_nattra_1(X9,X1,X0,X7,X8) )
& m2_cat_1(X8,X1,X0) )
& m2_cat_1(X7,X1,X0) ) )
& ( ~ r2_hidden(X3,X2)
| ! [X4] :
( ! [X5] :
( ! [X6] :
( ~ r2_nattra_1(X1,X0,X4,X5)
| k4_tarski(k4_tarski(X4,X5),X6) != X3
| ~ m2_nattra_1(X6,X1,X0,X4,X5) )
| ~ m2_cat_1(X5,X1,X0) )
| ~ m2_cat_1(X4,X1,X0) ) ) )
| sP0(X0,X1,X2) ) ),
inference(rectify,[],[f227]) ).
fof(f229,plain,
! [X0,X1,X2] :
( ( ~ sP0(X0,X1,X2)
| ! [X10] :
( ( ~ r2_hidden(X10,X2)
| ( r2_nattra_1(X1,X0,sK12(X0,X1,X10),sK13(X0,X1,X10))
& k4_tarski(k4_tarski(sK12(X0,X1,X10),sK13(X0,X1,X10)),sK14(X0,X1,X10)) = X10
& m2_nattra_1(sK14(X0,X1,X10),X1,X0,sK12(X0,X1,X10),sK13(X0,X1,X10))
& m2_cat_1(sK13(X0,X1,X10),X1,X0)
& m2_cat_1(sK12(X0,X1,X10),X1,X0) ) )
& ( ! [X11] :
( ! [X12] :
( ! [X13] :
( ~ r2_nattra_1(X1,X0,X11,X12)
| k4_tarski(k4_tarski(X11,X12),X13) != X10
| ~ m2_nattra_1(X13,X1,X0,X11,X12) )
| ~ m2_cat_1(X12,X1,X0) )
| ~ m2_cat_1(X11,X1,X0) )
| r2_hidden(X10,X2) ) ) )
& ( ( ( r2_hidden(sK8(X0,X1,X2),X2)
| ( r2_nattra_1(X1,X0,sK9(X0,X1,X2),sK10(X0,X1,X2))
& sK8(X0,X1,X2) = k4_tarski(k4_tarski(sK9(X0,X1,X2),sK10(X0,X1,X2)),sK11(X0,X1,X2))
& m2_nattra_1(sK11(X0,X1,X2),X1,X0,sK9(X0,X1,X2),sK10(X0,X1,X2))
& m2_cat_1(sK10(X0,X1,X2),X1,X0)
& m2_cat_1(sK9(X0,X1,X2),X1,X0) ) )
& ( ~ r2_hidden(sK8(X0,X1,X2),X2)
| ! [X4] :
( ! [X5] :
( ! [X6] :
( ~ r2_nattra_1(X1,X0,X4,X5)
| k4_tarski(k4_tarski(X4,X5),X6) != sK8(X0,X1,X2)
| ~ m2_nattra_1(X6,X1,X0,X4,X5) )
| ~ m2_cat_1(X5,X1,X0) )
| ~ m2_cat_1(X4,X1,X0) ) ) )
| sP0(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10,sK11,sK12,sK13,sK14]),skolemize(X3,sK8(X0,X1,X2)),skolemize(X7,sK9(X0,X1,X2)),skolemize(X8,sK10(X0,X1,X2)),skolemize(X9,sK11(X0,X1,X2)),skolemize(X14,sK12(X0,X1,X10)),skolemize(X15,sK13(X0,X1,X10)),skolemize(X16,sK14(X0,X1,X10))],[f228]) ).
fof(f276,plain,
! [X2,X10,X0,X11,X1,X12,X13] :
( ~ sP0(X0,X1,X2)
| ~ r2_nattra_1(X1,X0,X11,X12)
| k4_tarski(k4_tarski(X11,X12),X13) != X10
| ~ m2_nattra_1(X13,X1,X0,X11,X12)
| ~ m2_cat_1(X12,X1,X0)
| ~ m2_cat_1(X11,X1,X0)
| r2_hidden(X10,X2) ),
inference(cnf_transformation,[],[f229]) ).
fof(f423,plain,
! [X2,X10,X0,X11,X1,X12,X13] :
( ~ sP0(X0,X1,X2)
| ~ r2_nattra_1(X1,X0,X11,X12)
| k2_tarski(k2_tarski(k2_tarski(k2_tarski(X11,X12),k1_tarski(X11)),X13),k1_tarski(k2_tarski(k2_tarski(X11,X12),k1_tarski(X11)))) != X10
| ~ m2_nattra_1(X13,X1,X0,X11,X12)
| ~ m2_cat_1(X12,X1,X0)
| ~ m2_cat_1(X11,X1,X0)
| r2_hidden(X10,X2) ),
inference(definition_unfolding,[],[f276,f321,f321]) ).
fof(f433,plain,
! [X2,X0,X11,X1,X12,X13] :
( ~ sP0(X0,X1,X2)
| ~ r2_nattra_1(X1,X0,X11,X12)
| ~ m2_nattra_1(X13,X1,X0,X11,X12)
| ~ m2_cat_1(X12,X1,X0)
| ~ m2_cat_1(X11,X1,X0)
| r2_hidden(k2_tarski(k2_tarski(k2_tarski(k2_tarski(X11,X12),k1_tarski(X11)),X13),k1_tarski(k2_tarski(k2_tarski(X11,X12),k1_tarski(X11)))),X2) ),
inference(equality_resolution,[],[f423]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( r2_hidden(k2_tarski(k2_tarski(k2_tarski(k2_tarski(X3,X4),k1_tarski(X3)),X0),k1_tarski(k2_tarski(k2_tarski(X3,X4),k1_tarski(X3)))),X5)
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,X1,X2)
| ~ sP0(X2,X1,X5)
| ~ r2_nattra_1(X1,X2,X3,X4)
| ~ m2_nattra_1(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f433]) ).
tcf(c_2994,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( r2_hidden(k2_tarski(k1_tarski(k2_tarski(k1_tarski(X3),k2_tarski(X3,X4))),k2_tarski(k2_tarski(k1_tarski(X3),k2_tarski(X3,X4)),X0)),X5)
| ~ m2_cat_1(X4,X1,X2)
| ~ m2_cat_1(X3,X1,X2)
| ~ sP0(X2,X1,X5)
| ~ r2_nattra_1(X1,X2,X3,X4)
| ~ m2_nattra_1(X0,X1,X2,X3,X4) ),
inference(demodulation,[status(thm)],[c_66,c_57]) ).
tcf(c_29015,plain,
! [X0: $i] :
( r2_hidden(k2_tarski(k1_tarski(k2_tarski(k1_tarski(iPr_def_11),k2_tarski(iPr_def_11,iPr_def_14))),k2_tarski(k2_tarski(k1_tarski(iPr_def_11),k2_tarski(iPr_def_11,iPr_def_14)),iPr_def_18)),X0)
| ~ m2_cat_1(iPr_def_14,sK6,iPr_def_21)
| ~ m2_cat_1(iPr_def_11,sK6,iPr_def_21)
| ~ sP0(iPr_def_21,sK6,X0)
| ~ r2_nattra_1(sK6,iPr_def_21,iPr_def_11,iPr_def_14) ),
inference(superposition,[status(thm)],[c_27769,c_2994]) ).
tcf(c_29016,plain,
! [X0: $i] :
( r2_hidden(iPr_def_20,X0)
| ~ m2_cat_1(iPr_def_14,sK6,iPr_def_21)
| ~ m2_cat_1(iPr_def_11,sK6,iPr_def_21)
| ~ sP0(iPr_def_21,sK6,X0)
| ~ r2_nattra_1(sK6,iPr_def_21,iPr_def_11,iPr_def_14) ),
inference(light_normalisation,[status(thm)],[c_29015,c_20861,c_20864,c_20865,c_20866,c_20869,c_25161]) ).
tcf(c_29017,plain,
! [X0: $i] :
( r2_hidden(iPr_def_20,X0)
| ~ sP0(iPr_def_21,sK6,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_29016,c_26500,c_26502,c_27498]) ).
tcf(c_248007,plain,
! [X0: $i] :
( r2_hidden(k2_tarski(k1_tarski(k2_tarski(k1_tarski(iPr_def_11),k2_tarski(iPr_def_11,iPr_def_14))),k2_tarski(k2_tarski(k1_tarski(iPr_def_11),k2_tarski(iPr_def_11,iPr_def_14)),iPr_def_18)),X0)
| ~ m2_cat_1(iPr_def_14,sK6,iPr_def_21)
| ~ m2_cat_1(iPr_def_11,sK6,iPr_def_21)
| ~ sP0(iPr_def_21,sK6,X0)
| ~ r2_nattra_1(sK6,iPr_def_21,iPr_def_11,iPr_def_14) ),
inference(superposition,[status(thm)],[c_246768,c_2994]) ).
tcf(c_248008,plain,
! [X0: $i] :
( r2_hidden(iPr_def_20,X0)
| ~ m2_cat_1(iPr_def_14,sK6,iPr_def_21)
| ~ m2_cat_1(iPr_def_11,sK6,iPr_def_21)
| ~ sP0(iPr_def_21,sK6,X0)
| ~ r2_nattra_1(sK6,iPr_def_21,iPr_def_11,iPr_def_14) ),
inference(light_normalisation,[status(thm)],[c_248007,c_20861,c_20864,c_20865,c_20866,c_20869,c_247124]) ).
tcf(c_248009,plain,
! [X0: $i] :
( r2_hidden(iPr_def_20,X0)
| ~ m2_cat_1(iPr_def_11,sK6,iPr_def_21)
| ~ sP0(iPr_def_21,sK6,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_248008,c_246893,c_247797]) ).
tcf(c_257164,plain,
! [X0: $i] :
( r2_hidden(iPr_def_20,X0)
| ~ sP0(iPr_def_21,sK6,X0) ),
inference(global_subsumption_just,[status(thm)],[c_248009,c_29017]) ).
tcf(c_257171,plain,
r2_hidden(iPr_def_20,iPr_def_23),
inference(superposition,[status(thm)],[c_248814,c_257164]) ).
tcf(c_257312,plain,
m1_subset_1(iPr_def_20,iPr_def_23),
inference(superposition,[status(thm)],[c_257171,c_199]) ).
tcf(c_257313,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_257312,c_20874]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CAT034+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/15.42 % Computer : n016.cluster.edu
% 0.14/15.42 % Model : x86_64 x86_64
% 0.14/15.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/15.42 % Memory : 8046.5625MB
% 0.14/15.42 % OS : Linux 6.8.0-71-generic
% 0.14/15.42 % CPULimit : 300
% 0.14/15.42 % WCLimit : 300
% 0.14/15.42 % DateTime : Fri Sep 25 07:10:30 UTC 2026
% 0.14/15.42 % CPUTime :
% 0.14/15.42 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/15.49 Running first-order theorem proving
% 0.14/15.49 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/15.51
% 0.19/15.51 % ======== iProver multi-core TPTP/SMT =========
% 0.19/15.51
% 0.19/15.51 % Detected problem language: tptp
% 0.19/15.53 % Proving...
% 135.81/43.33 % SZS status Started for theBenchmark.p
% 135.81/43.33 % SZS status Theorem for theBenchmark.p
% 135.81/43.33
% 135.81/43.33 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 135.81/43.33
% 135.81/43.33 % ------ iProver source info
% 135.81/43.33
% 135.81/43.33 % git: date: 2026-07-19 20:42:38 +0200
% 135.81/43.33 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 135.81/43.33 % git: non_committed_changes: false
% 135.81/43.33
% 135.81/43.33 % ------ Parsing...
% 135.81/43.33 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 135.81/43.33
% 135.81/43.33 % ------ Preprocessing... sup_sim: 12 sf_s rm: 7 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 7 0s sf_e pe_s pe_e %
% 135.81/43.33
% 135.81/43.33 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 135.81/43.33
% 135.81/43.33 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 135.81/43.33 % ------ Proving...
% 135.81/43.33 % ------ Problem Properties
% 135.81/43.33
% 135.81/43.33 %
% 135.81/43.33 % clauses 163
% 135.81/43.33 % conjectures 3
% 135.81/43.33 % EPR 27
% 135.81/43.33 % Horn 132
% 135.81/43.33 % unary 32
% 135.81/43.33 % binary 36
% 135.81/43.33 % lits 661
% 135.81/43.33 % lits eq 82
% 135.81/43.33 % fd_pure 0
% 135.81/43.33 % fd_pseudo 0
% 135.81/43.33 % fd_cond 1
% 135.81/43.33 % fd_pseudo_cond 8
% 135.81/43.33 % AC symbols 0
% 135.81/43.33
% 135.81/43.33 % ------ Schedule dynamic 5 is on
% 135.81/43.33
% 135.81/43.33 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 135.81/43.33
% 135.81/43.33
% 135.81/43.33 % ------
% 135.81/43.33 % Current options:
% 135.81/43.33 % ------
% 135.81/43.33
% 135.81/43.33
% 135.81/43.33 %
% 135.81/43.33
% 135.81/43.33 % ------ Proving...
% 135.81/43.33 % Proof_search_loop: time out after: 4193 full_loop iterations
% 135.81/43.33
% 135.81/43.33 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 135.81/43.33
% 135.81/43.33
% 135.81/43.33 % ------
% 135.81/43.33 % Current options:
% 135.81/43.33 % ------
% 135.81/43.33
% 135.81/43.33
% 135.81/43.33 %
% 135.81/43.33
% 135.81/43.33 % ------ Proving...
% 135.81/43.33 % Proof_search_loop: time out after: 9627 full_loop iterations
% 135.81/43.33
% 135.81/43.33 % ------ Option_1: Negative Selections Time Limit: 35.
% 135.81/43.33
% 135.81/43.33
% 135.81/43.33 % ------
% 135.81/43.33 % Current options:
% 135.81/43.33 % ------
% 135.81/43.33
% 135.81/43.33
% 135.81/43.33 %
% 135.81/43.33
% 135.81/43.33 % ------ Proving...
% 135.81/43.33 %
% 135.81/43.33
% 135.81/43.33 % SZS status Theorem for theBenchmark.p
% 135.81/43.33
% 135.81/43.33 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 135.81/43.34
% 135.81/43.34
%------------------------------------------------------------------------------