%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT345+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 : n020.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:25 PM UTC 2026
% Result : Theorem 10.70s 2.73s
% Output : CNFRefutation 10.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 21
% Syntax : Number of formulae : 234 ( 66 unt; 3 def)
% Number of atoms : 930 ( 167 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 797 ( 318 ~; 374 |; 76 &)
% ( 4 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 17 ( 15 usr; 4 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 2 con; 0-3 aty)
% Number of variables : 300 ( 0 sgn 296 !; 4 ?; 128 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l2_conlat_1(X0)
& v4_conlat_1(X0)
& ~ v3_conlat_1(X0) )
=> ! [X1] :
( ( l3_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& ~ v7_conlat_1(X1,X0)
& v6_conlat_1(X1,X0) )
=> k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1)) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_conlat_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l2_conlat_1(X0)
& v4_conlat_1(X0)
& ~ v3_conlat_1(X0) )
=> ! [X1] :
( ( l3_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& ~ v7_conlat_1(X1,X0)
& v6_conlat_1(X1,X0) )
=> k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1)) = X1 ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
! [X0] :
( l2_conlat_1(X0)
=> ( v4_conlat_1(X0)
=> X0 = g2_conlat_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v4_conlat_1) ).
fof(f4,axiom,
! [X0,X1] :
( ( l3_conlat_1(X1,X0)
& l1_conlat_1(X0) )
=> ( v6_conlat_1(X1,X0)
=> X1 = g3_conlat_1(X0,u4_conlat_1(X0,X1),u5_conlat_1(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v6_conlat_1) ).
fof(f6,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f8,axiom,
! [X0] :
( ( l2_conlat_1(X0)
& ~ v3_conlat_1(X0) )
=> k7_conlat_2(X0) = g2_conlat_1(u2_conlat_1(X0),u1_conlat_1(X0),k6_relset_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d7_conlat_2) ).
fof(f9,axiom,
! [X0] :
( ( l2_conlat_1(X0)
& ~ v3_conlat_1(X0) )
=> ! [X1] :
( l3_conlat_1(X1,X0)
=> ! [X2] :
( ( l3_conlat_1(X2,k7_conlat_2(X0))
& v6_conlat_1(X2,k7_conlat_2(X0)) )
=> ( X2 = k8_conlat_2(X0,X1)
<=> ( u5_conlat_1(k7_conlat_2(X0),X2) = u4_conlat_1(X0,X1)
& u4_conlat_1(k7_conlat_2(X0),X2) = u5_conlat_1(X0,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_conlat_2) ).
fof(f16,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_relset_1) ).
fof(f17,axiom,
! [X0] :
( ( l2_conlat_1(X0)
& ~ v3_conlat_1(X0) )
=> ( l2_conlat_1(k7_conlat_2(X0))
& v4_conlat_1(k7_conlat_2(X0))
& ~ v3_conlat_1(k7_conlat_2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_conlat_2) ).
fof(f18,axiom,
! [X0,X1] :
( ( l3_conlat_1(X1,X0)
& l2_conlat_1(X0)
& ~ v3_conlat_1(X0) )
=> ( l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
& v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_conlat_2) ).
fof(f19,axiom,
! [X0,X1] :
( ( l3_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& ~ v7_conlat_1(X1,X0)
& l2_conlat_1(X0)
& ~ v3_conlat_1(X0) )
=> ( l3_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& ~ v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& v6_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k9_conlat_2) ).
fof(f21,axiom,
! [X0] :
( l2_conlat_1(X0)
=> l1_conlat_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_conlat_1) ).
fof(f25,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f28,axiom,
! [X0] :
( l2_conlat_1(X0)
=> m2_relset_1(u3_conlat_1(X0),u1_conlat_1(X0),u2_conlat_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u3_conlat_1) ).
fof(f42,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> ! [X3,X4,X5] :
( g2_conlat_1(X0,X1,X2) = g2_conlat_1(X3,X4,X5)
=> ( X2 = X5
& X1 = X4
& X0 = X3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',free_g2_conlat_1) ).
fof(f44,axiom,
! [X0] :
( v1_relat_1(X0)
=> k4_relat_1(k4_relat_1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',involutiveness_k4_relat_1) ).
fof(f59,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_relset_1) ).
fof(f60,axiom,
! [X0,X1] :
( ( l3_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& ~ v7_conlat_1(X1,X0)
& l2_conlat_1(X0)
& ~ v3_conlat_1(X0) )
=> k9_conlat_2(X0,X1) = k8_conlat_2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k9_conlat_2) ).
fof(f61,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(f75,plain,
? [X0] :
( l2_conlat_1(X0)
& v4_conlat_1(X0)
& ~ v3_conlat_1(X0)
& ? [X1] :
( l3_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& ~ v7_conlat_1(X1,X0)
& v6_conlat_1(X1,X0)
& k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1)) != X1 ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f76,plain,
? [X0] :
( l2_conlat_1(X0)
& v4_conlat_1(X0)
& ~ v3_conlat_1(X0)
& ? [X1] :
( l3_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& ~ v7_conlat_1(X1,X0)
& v6_conlat_1(X1,X0)
& k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1)) != X1 ) ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| ~ v4_conlat_1(X0)
| X0 = g2_conlat_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0)) ),
inference(ennf_transformation,[],[f3]) ).
fof(f78,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| ~ v4_conlat_1(X0)
| X0 = g2_conlat_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0)) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ l1_conlat_1(X0)
| ~ v6_conlat_1(X1,X0)
| X1 = g3_conlat_1(X0,u4_conlat_1(X0,X1),u5_conlat_1(X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f80,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ l1_conlat_1(X0)
| ~ v6_conlat_1(X1,X0)
| X1 = g3_conlat_1(X0,u4_conlat_1(X0,X1),u5_conlat_1(X0,X1)) ),
inference(flattening,[],[f79]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(ennf_transformation,[],[f6]) ).
fof(f83,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k7_conlat_2(X0) = g2_conlat_1(u2_conlat_1(X0),u1_conlat_1(X0),k6_relset_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0))) ),
inference(ennf_transformation,[],[f8]) ).
fof(f84,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k7_conlat_2(X0) = g2_conlat_1(u2_conlat_1(X0),u1_conlat_1(X0),k6_relset_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0))) ),
inference(flattening,[],[f83]) ).
fof(f85,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ! [X1] :
( ~ l3_conlat_1(X1,X0)
| ! [X2] :
( ~ l3_conlat_1(X2,k7_conlat_2(X0))
| ~ v6_conlat_1(X2,k7_conlat_2(X0))
| ( X2 = k8_conlat_2(X0,X1)
<=> ( u5_conlat_1(k7_conlat_2(X0),X2) = u4_conlat_1(X0,X1)
& u4_conlat_1(k7_conlat_2(X0),X2) = u5_conlat_1(X0,X1) ) ) ) ) ),
inference(ennf_transformation,[],[f9]) ).
fof(f86,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ! [X1] :
( ~ l3_conlat_1(X1,X0)
| ! [X2] :
( ~ l3_conlat_1(X2,k7_conlat_2(X0))
| ~ v6_conlat_1(X2,k7_conlat_2(X0))
| ( X2 = k8_conlat_2(X0,X1)
<=> ( u5_conlat_1(k7_conlat_2(X0),X2) = u4_conlat_1(X0,X1)
& u4_conlat_1(k7_conlat_2(X0),X2) = u5_conlat_1(X0,X1) ) ) ) ) ),
inference(flattening,[],[f85]) ).
fof(f91,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f92,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ( l2_conlat_1(k7_conlat_2(X0))
& v4_conlat_1(k7_conlat_2(X0))
& ~ v3_conlat_1(k7_conlat_2(X0)) ) ),
inference(ennf_transformation,[],[f17]) ).
fof(f93,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ( l2_conlat_1(k7_conlat_2(X0))
& v4_conlat_1(k7_conlat_2(X0))
& ~ v3_conlat_1(k7_conlat_2(X0)) ) ),
inference(flattening,[],[f92]) ).
fof(f94,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ( l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
& v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)) ) ),
inference(ennf_transformation,[],[f18]) ).
fof(f95,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ( l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
& v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)) ) ),
inference(flattening,[],[f94]) ).
fof(f96,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ( l3_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& ~ v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& v6_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f97,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ( l3_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& ~ v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& v6_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)) ) ),
inference(flattening,[],[f96]) ).
fof(f98,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| l1_conlat_1(X0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ~ m2_relset_1(X2,X0,X1)
| m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f25]) ).
fof(f100,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| m2_relset_1(u3_conlat_1(X0),u1_conlat_1(X0),u2_conlat_1(X0)) ),
inference(ennf_transformation,[],[f28]) ).
fof(f112,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,X0,X1)
| ! [X3,X4,X5] :
( g2_conlat_1(X0,X1,X2) != g2_conlat_1(X3,X4,X5)
| ( X2 = X5
& X1 = X4
& X0 = X3 ) ) ),
inference(ennf_transformation,[],[f42]) ).
fof(f115,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k4_relat_1(k4_relat_1(X0)) = X0 ),
inference(ennf_transformation,[],[f44]) ).
fof(f131,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,X0,X1)
| k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
inference(ennf_transformation,[],[f59]) ).
fof(f132,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k9_conlat_2(X0,X1) = k8_conlat_2(X0,X1) ),
inference(ennf_transformation,[],[f60]) ).
fof(f133,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k9_conlat_2(X0,X1) = k8_conlat_2(X0,X1) ),
inference(flattening,[],[f132]) ).
fof(f144,plain,
( l2_conlat_1(sK0)
& v4_conlat_1(sK0)
& ~ v3_conlat_1(sK0)
& l3_conlat_1(sK1,sK0)
& v9_conlat_1(sK1,sK0)
& ~ v7_conlat_1(sK1,sK0)
& v6_conlat_1(sK1,sK0)
& sK1 != k9_conlat_2(k7_conlat_2(sK0),k9_conlat_2(sK0,sK1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f76]) ).
fof(f145,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ! [X1] :
( ~ l3_conlat_1(X1,X0)
| ! [X2] :
( ~ l3_conlat_1(X2,k7_conlat_2(X0))
| ~ v6_conlat_1(X2,k7_conlat_2(X0))
| ( ( k8_conlat_2(X0,X1) != X2
| ( u5_conlat_1(k7_conlat_2(X0),X2) = u4_conlat_1(X0,X1)
& u4_conlat_1(k7_conlat_2(X0),X2) = u5_conlat_1(X0,X1) ) )
& ( u4_conlat_1(X0,X1) != u5_conlat_1(k7_conlat_2(X0),X2)
| u5_conlat_1(X0,X1) != u4_conlat_1(k7_conlat_2(X0),X2)
| X2 = k8_conlat_2(X0,X1) ) ) ) ) ),
inference(nnf_transformation,[],[f86]) ).
fof(f146,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ! [X1] :
( ~ l3_conlat_1(X1,X0)
| ! [X2] :
( ~ l3_conlat_1(X2,k7_conlat_2(X0))
| ~ v6_conlat_1(X2,k7_conlat_2(X0))
| ( ( k8_conlat_2(X0,X1) != X2
| ( u5_conlat_1(k7_conlat_2(X0),X2) = u4_conlat_1(X0,X1)
& u4_conlat_1(k7_conlat_2(X0),X2) = u5_conlat_1(X0,X1) ) )
& ( u4_conlat_1(X0,X1) != u5_conlat_1(k7_conlat_2(X0),X2)
| u5_conlat_1(X0,X1) != u4_conlat_1(k7_conlat_2(X0),X2)
| X2 = k8_conlat_2(X0,X1) ) ) ) ) ),
inference(flattening,[],[f145]) ).
fof(f166,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,[],[f61]) ).
fof(f167,plain,
l2_conlat_1(sK0),
inference(cnf_transformation,[],[f144]) ).
fof(f168,plain,
v4_conlat_1(sK0),
inference(cnf_transformation,[],[f144]) ).
fof(f169,plain,
~ v3_conlat_1(sK0),
inference(cnf_transformation,[],[f144]) ).
fof(f170,plain,
l3_conlat_1(sK1,sK0),
inference(cnf_transformation,[],[f144]) ).
fof(f171,plain,
v9_conlat_1(sK1,sK0),
inference(cnf_transformation,[],[f144]) ).
fof(f172,plain,
~ v7_conlat_1(sK1,sK0),
inference(cnf_transformation,[],[f144]) ).
fof(f173,plain,
v6_conlat_1(sK1,sK0),
inference(cnf_transformation,[],[f144]) ).
fof(f174,plain,
sK1 != k9_conlat_2(k7_conlat_2(sK0),k9_conlat_2(sK0,sK1)),
inference(cnf_transformation,[],[f144]) ).
fof(f175,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| ~ v4_conlat_1(X0)
| g2_conlat_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0)) = X0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f176,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ l1_conlat_1(X0)
| ~ v6_conlat_1(X1,X0)
| g3_conlat_1(X0,u4_conlat_1(X0,X1),u5_conlat_1(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f80]) ).
fof(f178,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f82]) ).
fof(f179,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k7_conlat_2(X0) = g2_conlat_1(u2_conlat_1(X0),u1_conlat_1(X0),k6_relset_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0))) ),
inference(cnf_transformation,[],[f84]) ).
fof(f180,plain,
! [X2,X0,X1] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l3_conlat_1(X1,X0)
| ~ l3_conlat_1(X2,k7_conlat_2(X0))
| ~ v6_conlat_1(X2,k7_conlat_2(X0))
| k8_conlat_2(X0,X1) != X2
| u4_conlat_1(X0,X1) = u5_conlat_1(k7_conlat_2(X0),X2) ),
inference(cnf_transformation,[],[f146]) ).
fof(f181,plain,
! [X2,X0,X1] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l3_conlat_1(X1,X0)
| ~ l3_conlat_1(X2,k7_conlat_2(X0))
| ~ v6_conlat_1(X2,k7_conlat_2(X0))
| k8_conlat_2(X0,X1) != X2
| u5_conlat_1(X0,X1) = u4_conlat_1(k7_conlat_2(X0),X2) ),
inference(cnf_transformation,[],[f146]) ).
fof(f188,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
inference(cnf_transformation,[],[f91]) ).
fof(f189,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| l2_conlat_1(k7_conlat_2(X0)) ),
inference(cnf_transformation,[],[f93]) ).
fof(f190,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| v4_conlat_1(k7_conlat_2(X0)) ),
inference(cnf_transformation,[],[f93]) ).
fof(f191,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ v3_conlat_1(k7_conlat_2(X0)) ),
inference(cnf_transformation,[],[f93]) ).
fof(f192,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)) ),
inference(cnf_transformation,[],[f95]) ).
fof(f193,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)) ),
inference(cnf_transformation,[],[f95]) ).
fof(f194,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| l3_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)) ),
inference(cnf_transformation,[],[f97]) ).
fof(f195,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)) ),
inference(cnf_transformation,[],[f97]) ).
fof(f196,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)) ),
inference(cnf_transformation,[],[f97]) ).
fof(f198,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| l1_conlat_1(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f199,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f99]) ).
fof(f200,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| m2_relset_1(u3_conlat_1(X0),u1_conlat_1(X0),u2_conlat_1(X0)) ),
inference(cnf_transformation,[],[f100]) ).
fof(f214,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m1_relset_1(X2,X0,X1)
| g2_conlat_1(X0,X1,X2) != g2_conlat_1(X3,X4,X5)
| X2 = X5 ),
inference(cnf_transformation,[],[f112]) ).
fof(f215,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m1_relset_1(X2,X0,X1)
| g2_conlat_1(X0,X1,X2) != g2_conlat_1(X3,X4,X5)
| X1 = X4 ),
inference(cnf_transformation,[],[f112]) ).
fof(f216,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m1_relset_1(X2,X0,X1)
| g2_conlat_1(X0,X1,X2) != g2_conlat_1(X3,X4,X5)
| X0 = X3 ),
inference(cnf_transformation,[],[f112]) ).
fof(f220,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k4_relat_1(k4_relat_1(X0)) = X0 ),
inference(cnf_transformation,[],[f115]) ).
fof(f251,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
inference(cnf_transformation,[],[f131]) ).
fof(f252,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k9_conlat_2(X0,X1) = k8_conlat_2(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f253,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f166]) ).
fof(f254,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f166]) ).
fof(f264,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l3_conlat_1(X1,X0)
| ~ l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| u5_conlat_1(X0,X1) = u4_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) ),
inference(equality_resolution,[],[f181]) ).
fof(f265,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l3_conlat_1(X1,X0)
| ~ l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| u4_conlat_1(X0,X1) = u5_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) ),
inference(equality_resolution,[],[f180]) ).
tcf(c_49,negated_conjecture,
k9_conlat_2(k7_conlat_2(sK0),k9_conlat_2(sK0,sK1)) != sK1,
inference(cnf_transformation,[],[f174]) ).
tcf(c_50,negated_conjecture,
v6_conlat_1(sK1,sK0),
inference(cnf_transformation,[],[f173]) ).
tcf(c_51,negated_conjecture,
~ v7_conlat_1(sK1,sK0),
inference(cnf_transformation,[],[f172]) ).
tcf(c_52,negated_conjecture,
v9_conlat_1(sK1,sK0),
inference(cnf_transformation,[],[f171]) ).
tcf(c_53,negated_conjecture,
l3_conlat_1(sK1,sK0),
inference(cnf_transformation,[],[f170]) ).
tcf(c_54,negated_conjecture,
~ v3_conlat_1(sK0),
inference(cnf_transformation,[],[f169]) ).
tcf(c_55,negated_conjecture,
v4_conlat_1(sK0),
inference(cnf_transformation,[],[f168]) ).
tcf(c_56,negated_conjecture,
l2_conlat_1(sK0),
inference(cnf_transformation,[],[f167]) ).
tcf(c_57,plain,
! [X0: $i] :
( ( g2_conlat_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0)) = X0 )
| ~ l2_conlat_1(X0)
| ~ v4_conlat_1(X0) ),
inference(cnf_transformation,[],[f175]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( ( g3_conlat_1(X1,u4_conlat_1(X1,X0),u5_conlat_1(X1,X0)) = X0 )
| ~ l1_conlat_1(X1)
| ~ l3_conlat_1(X0,X1)
| ~ v6_conlat_1(X0,X1) ),
inference(cnf_transformation,[],[f176]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[],[f178]) ).
tcf(c_61,plain,
! [X0: $i] :
( v3_conlat_1(X0)
| ( g2_conlat_1(u2_conlat_1(X0),u1_conlat_1(X0),k6_relset_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0))) = k7_conlat_2(X0) )
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] :
( v3_conlat_1(X0)
| ( u4_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) = u5_conlat_1(X0,X1) )
| ~ l2_conlat_1(X0)
| ~ l3_conlat_1(X1,X0)
| ~ l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)) ),
inference(cnf_transformation,[],[f264]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] :
( v3_conlat_1(X0)
| ( u5_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) = u4_conlat_1(X0,X1) )
| ~ l2_conlat_1(X0)
| ~ l3_conlat_1(X1,X0)
| ~ l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)) ),
inference(cnf_transformation,[],[f265]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] :
( m2_relset_1(k6_relset_1(X1,X2,X0),X2,X1)
| ~ m1_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_71,plain,
! [X0: $i] :
( v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ v3_conlat_1(k7_conlat_2(X0)) ),
inference(cnf_transformation,[],[f191]) ).
tcf(c_72,plain,
! [X0: $i] :
( v3_conlat_1(X0)
| v4_conlat_1(k7_conlat_2(X0))
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f190]) ).
tcf(c_73,plain,
! [X0: $i] :
( v3_conlat_1(X0)
| l2_conlat_1(k7_conlat_2(X0))
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f189]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( v3_conlat_1(X1)
| v6_conlat_1(k8_conlat_2(X1,X0),k7_conlat_2(X1))
| ~ l2_conlat_1(X1)
| ~ l3_conlat_1(X0,X1) ),
inference(cnf_transformation,[],[f193]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] :
( v3_conlat_1(X1)
| l3_conlat_1(k8_conlat_2(X1,X0),k7_conlat_2(X1))
| ~ l2_conlat_1(X1)
| ~ l3_conlat_1(X0,X1) ),
inference(cnf_transformation,[],[f192]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i] :
( v3_conlat_1(X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| ~ l3_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| ~ v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)) ),
inference(cnf_transformation,[],[f196]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i] :
( v3_conlat_1(X1)
| v7_conlat_1(X0,X1)
| v9_conlat_1(k9_conlat_2(X1,X0),k7_conlat_2(X1))
| ~ l2_conlat_1(X1)
| ~ l3_conlat_1(X0,X1)
| ~ v9_conlat_1(X0,X1) ),
inference(cnf_transformation,[],[f195]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] :
( v3_conlat_1(X1)
| v7_conlat_1(X0,X1)
| l3_conlat_1(k9_conlat_2(X1,X0),k7_conlat_2(X1))
| ~ l2_conlat_1(X1)
| ~ l3_conlat_1(X0,X1)
| ~ v9_conlat_1(X0,X1) ),
inference(cnf_transformation,[],[f194]) ).
tcf(c_80,plain,
! [X0: $i] :
( l1_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f199]) ).
tcf(c_82,plain,
! [X0: $i] :
( m2_relset_1(u3_conlat_1(X0),u1_conlat_1(X0),u2_conlat_1(X0))
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X0 = X3 )
| ~ m1_relset_1(X2,X0,X1)
| ( g2_conlat_1(X0,X1,X2) != g2_conlat_1(X3,X4,X5) ) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X1 = X4 )
| ~ m1_relset_1(X2,X0,X1)
| ( g2_conlat_1(X0,X1,X2) != g2_conlat_1(X3,X4,X5) ) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X2 = X5 )
| ~ m1_relset_1(X2,X0,X1)
| ( g2_conlat_1(X0,X1,X2) != g2_conlat_1(X3,X4,X5) ) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_102,plain,
! [X0: $i] :
( ( k4_relat_1(k4_relat_1(X0)) = X0 )
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k6_relset_1(X1,X2,X0) = k4_relat_1(X0) )
| ~ m1_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f251]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i] :
( v3_conlat_1(X1)
| v7_conlat_1(X0,X1)
| ( k9_conlat_2(X1,X0) = k8_conlat_2(X1,X0) )
| ~ l2_conlat_1(X1)
| ~ l3_conlat_1(X0,X1)
| ~ v9_conlat_1(X0,X1) ),
inference(cnf_transformation,[],[f252]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i,X2: $i] :
( m2_relset_1(X0,X1,X2)
| ~ m1_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f254]) ).
tcf(c_136,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f253]) ).
tcf(c_191,plain,
( m2_relset_1(u3_conlat_1(sK0),u1_conlat_1(sK0),u2_conlat_1(sK0))
| ~ l2_conlat_1(sK0) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_259,plain,
! [X0: $i,X1: $i,X2: $i] :
( m2_relset_1(k6_relset_1(X1,X2,X0),X2,X1)
| ~ m2_relset_1(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_136,c_70]) ).
tcf(c_263,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k6_relset_1(X1,X2,X0) = k4_relat_1(X0) )
| ~ m2_relset_1(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_136,c_133]) ).
tcf(c_794,plain,
! [X0: $i,X1: $i] :
( v3_conlat_1(X0)
| ( u5_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) = u4_conlat_1(X0,X1) )
| ~ l2_conlat_1(X0)
| ~ l3_conlat_1(X1,X0)
| ~ l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_64,c_74]) ).
tcf(c_795,plain,
! [X0: $i,X1: $i] :
( v3_conlat_1(X0)
| ( u4_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) = u5_conlat_1(X0,X1) )
| ~ l2_conlat_1(X0)
| ~ l3_conlat_1(X1,X0)
| ~ l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_63,c_74]) ).
tcf(c_806,plain,
! [X0: $i,X1: $i] :
( v3_conlat_1(X1)
| ( u4_conlat_1(k7_conlat_2(X1),k8_conlat_2(X1,X0)) = u5_conlat_1(X1,X0) )
| ~ l2_conlat_1(X1)
| ~ l3_conlat_1(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_795,c_75]) ).
tcf(c_807,plain,
! [X0: $i,X1: $i] :
( v3_conlat_1(X1)
| ( u5_conlat_1(k7_conlat_2(X1),k8_conlat_2(X1,X0)) = u4_conlat_1(X1,X0) )
| ~ l2_conlat_1(X1)
| ~ l3_conlat_1(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_794,c_75]) ).
tcf(c_2685,plain,
! [X0: $i,X1: $i,X2: $i] :
( m2_relset_1(k6_relset_1(X1,X2,X0),X2,X1)
| ~ m2_relset_1(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_259]) ).
tcf(c_2689,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k6_relset_1(X1,X2,X0) = k4_relat_1(X0) )
| ~ m2_relset_1(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_263]) ).
tcf(c_4971,definition,
iPr_def_10 = k7_conlat_2(sK0),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_4972,definition,
iPr_def_11 = k9_conlat_2(sK0,sK1),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_4973,definition,
iPr_def_12 = k9_conlat_2(iPr_def_10,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_4974,negated_conjecture,
l2_conlat_1(sK0),
inference(demodulation,[status(thm)],[c_56]) ).
tcf(c_4975,negated_conjecture,
v4_conlat_1(sK0),
inference(demodulation,[status(thm)],[c_55]) ).
tcf(c_4976,negated_conjecture,
~ v3_conlat_1(sK0),
inference(demodulation,[status(thm)],[c_54]) ).
tcf(c_4977,negated_conjecture,
l3_conlat_1(sK1,sK0),
inference(demodulation,[status(thm)],[c_53]) ).
tcf(c_4978,negated_conjecture,
v9_conlat_1(sK1,sK0),
inference(demodulation,[status(thm)],[c_52]) ).
tcf(c_4979,negated_conjecture,
~ v7_conlat_1(sK1,sK0),
inference(demodulation,[status(thm)],[c_51]) ).
tcf(c_4980,negated_conjecture,
v6_conlat_1(sK1,sK0),
inference(demodulation,[status(thm)],[c_50]) ).
tcf(c_4981,negated_conjecture,
iPr_def_12 != sK1,
inference(demodulation,[status(thm)],[c_49,c_4972,c_4971,c_4973]) ).
tcf(c_6863,plain,
l1_conlat_1(sK0),
inference(superposition,[status(thm)],[c_4974,c_80]) ).
tcf(c_6921,plain,
( v4_conlat_1(iPr_def_10)
| v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0) ),
inference(superposition,[status(thm)],[c_4971,c_72]) ).
tcf(c_6922,plain,
v4_conlat_1(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_6921,c_4976,c_4974]) ).
tcf(c_6929,plain,
( l2_conlat_1(iPr_def_10)
| v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0) ),
inference(superposition,[status(thm)],[c_4971,c_73]) ).
tcf(c_6931,plain,
l2_conlat_1(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_6929,c_4976,c_4974]) ).
tcf(c_6963,plain,
( v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| ~ v3_conlat_1(iPr_def_10) ),
inference(superposition,[status(thm)],[c_4971,c_71]) ).
tcf(c_6964,plain,
~ v3_conlat_1(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_6963,c_4976,c_4974]) ).
tcf(c_6979,plain,
( v3_conlat_1(sK0)
| ( u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u5_conlat_1(sK0,sK1) )
| ~ l2_conlat_1(sK0) ),
inference(superposition,[status(thm)],[c_4977,c_806]) ).
tcf(c_6982,plain,
( v3_conlat_1(sK0)
| ( u4_conlat_1(iPr_def_10,k8_conlat_2(sK0,sK1)) = u5_conlat_1(sK0,sK1) )
| ~ l2_conlat_1(sK0) ),
inference(light_normalisation,[status(thm)],[c_6979,c_4971]) ).
tcf(c_6983,plain,
u4_conlat_1(iPr_def_10,k8_conlat_2(sK0,sK1)) = u5_conlat_1(sK0,sK1),
inference(forward_subsumption_resolution,[status(thm)],[c_6982,c_4976,c_4974]) ).
tcf(c_7246,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_relat_1(X0)
| ~ m2_relset_1(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_81,c_60]) ).
tcf(c_7259,plain,
! [X0: $i] :
( v1_relat_1(u3_conlat_1(X0))
| ~ l2_conlat_1(X0) ),
inference(superposition,[status(thm)],[c_82,c_7246]) ).
tcf(c_7275,plain,
! [X0: $i] :
( ( k4_relat_1(k4_relat_1(u3_conlat_1(X0))) = u3_conlat_1(X0) )
| ~ l2_conlat_1(X0) ),
inference(superposition,[status(thm)],[c_7259,c_102]) ).
tcf(c_7313,plain,
( v3_conlat_1(sK0)
| ( u5_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u4_conlat_1(sK0,sK1) )
| ~ l2_conlat_1(sK0) ),
inference(superposition,[status(thm)],[c_4977,c_807]) ).
tcf(c_7320,plain,
( v3_conlat_1(sK0)
| ( u5_conlat_1(iPr_def_10,k8_conlat_2(sK0,sK1)) = u4_conlat_1(sK0,sK1) )
| ~ l2_conlat_1(sK0) ),
inference(light_normalisation,[status(thm)],[c_7313,c_4971]) ).
tcf(c_7321,plain,
u5_conlat_1(iPr_def_10,k8_conlat_2(sK0,sK1)) = u4_conlat_1(sK0,sK1),
inference(forward_subsumption_resolution,[status(thm)],[c_7320,c_4976,c_4974]) ).
tcf(c_7421,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(k6_relset_1(X1,X2,X0),X2,X1)
| ~ m2_relset_1(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_2685,c_136]) ).
tcf(c_7433,plain,
! [X0: $i] :
( ( k6_relset_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0)) = k4_relat_1(u3_conlat_1(X0)) )
| ~ l2_conlat_1(X0) ),
inference(superposition,[status(thm)],[c_82,c_2689]) ).
tcf(c_7772,plain,
( ( g2_conlat_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = sK0 )
| ~ l2_conlat_1(sK0) ),
inference(superposition,[status(thm)],[c_4975,c_57]) ).
tcf(c_7777,plain,
( ( g2_conlat_1(u1_conlat_1(iPr_def_10),u2_conlat_1(iPr_def_10),u3_conlat_1(iPr_def_10)) = iPr_def_10 )
| ~ l2_conlat_1(iPr_def_10) ),
inference(superposition,[status(thm)],[c_6922,c_57]) ).
tcf(c_7778,plain,
g2_conlat_1(u1_conlat_1(iPr_def_10),u2_conlat_1(iPr_def_10),u3_conlat_1(iPr_def_10)) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_7777,c_6931]) ).
tcf(c_7781,plain,
g2_conlat_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = sK0,
inference(forward_subsumption_resolution,[status(thm)],[c_7772,c_4974]) ).
tcf(c_8034,plain,
( v3_conlat_1(sK0)
| ( g2_conlat_1(u2_conlat_1(sK0),u1_conlat_1(sK0),k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0))) = k7_conlat_2(sK0) ) ),
inference(superposition,[status(thm)],[c_4974,c_61]) ).
tcf(c_8040,plain,
( v3_conlat_1(iPr_def_10)
| ( g2_conlat_1(u2_conlat_1(iPr_def_10),u1_conlat_1(iPr_def_10),k6_relset_1(u1_conlat_1(iPr_def_10),u2_conlat_1(iPr_def_10),u3_conlat_1(iPr_def_10))) = k7_conlat_2(iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_6931,c_61]) ).
tcf(c_8041,plain,
g2_conlat_1(u2_conlat_1(iPr_def_10),u1_conlat_1(iPr_def_10),k6_relset_1(u1_conlat_1(iPr_def_10),u2_conlat_1(iPr_def_10),u3_conlat_1(iPr_def_10))) = k7_conlat_2(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_8040,c_6964]) ).
tcf(c_8047,plain,
( v3_conlat_1(sK0)
| ( g2_conlat_1(u2_conlat_1(sK0),u1_conlat_1(sK0),k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0))) = iPr_def_10 ) ),
inference(light_normalisation,[status(thm)],[c_8034,c_4971]) ).
tcf(c_8048,plain,
g2_conlat_1(u2_conlat_1(sK0),u1_conlat_1(sK0),k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0))) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_8047,c_4976]) ).
tcf(c_8237,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = X2 )
| ~ m1_relset_1(k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0))
| ( g2_conlat_1(X0,X1,X2) != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_8048,c_98]) ).
tcf(c_8240,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( u1_conlat_1(sK0) = X1 )
| ~ m1_relset_1(k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0))
| ( g2_conlat_1(X0,X1,X2) != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_8048,c_97]) ).
tcf(c_8241,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( u2_conlat_1(sK0) = X0 )
| ~ m1_relset_1(k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0))
| ( g2_conlat_1(X0,X1,X2) != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_8048,c_96]) ).
tcf(c_8245,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = X2 )
| ~ m1_relset_1(X2,X0,X1)
| ( g2_conlat_1(X0,X1,X2) != iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_8048,c_98]) ).
tcf(c_8414,plain,
( ( g3_conlat_1(sK0,u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1)) = sK1 )
| ~ l1_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0) ),
inference(superposition,[status(thm)],[c_4980,c_58]) ).
tcf(c_8422,plain,
g3_conlat_1(sK0,u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1)) = sK1,
inference(forward_subsumption_resolution,[status(thm)],[c_8414,c_6863,c_4977]) ).
tcf(c_8515,plain,
( v3_conlat_1(sK0)
| v7_conlat_1(sK1,sK0)
| v9_conlat_1(iPr_def_11,k7_conlat_2(sK0))
| ~ l2_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0)
| ~ v9_conlat_1(sK1,sK0) ),
inference(superposition,[status(thm)],[c_4972,c_78]) ).
tcf(c_8523,plain,
( v3_conlat_1(sK0)
| v9_conlat_1(iPr_def_11,iPr_def_10)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0)
| ~ v9_conlat_1(sK1,sK0) ),
inference(light_normalisation,[status(thm)],[c_8515,c_4971]) ).
tcf(c_8524,plain,
v9_conlat_1(iPr_def_11,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_8523,c_4976,c_4979,c_4974,c_4977,c_4978]) ).
tcf(c_8552,plain,
( v3_conlat_1(sK0)
| v7_conlat_1(sK1,sK0)
| l3_conlat_1(iPr_def_11,k7_conlat_2(sK0))
| ~ l2_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0)
| ~ v9_conlat_1(sK1,sK0) ),
inference(superposition,[status(thm)],[c_4972,c_79]) ).
tcf(c_8553,plain,
( v3_conlat_1(iPr_def_10)
| v7_conlat_1(iPr_def_11,iPr_def_10)
| l3_conlat_1(iPr_def_12,k7_conlat_2(iPr_def_10))
| ~ l2_conlat_1(iPr_def_10)
| ~ l3_conlat_1(iPr_def_11,iPr_def_10)
| ~ v9_conlat_1(iPr_def_11,iPr_def_10) ),
inference(superposition,[status(thm)],[c_4973,c_79]) ).
tcf(c_8554,plain,
! [X0: $i] :
( v3_conlat_1(sK0)
| v7_conlat_1(X0,sK0)
| l3_conlat_1(k9_conlat_2(sK0,X0),iPr_def_10)
| ~ l2_conlat_1(sK0)
| ~ l3_conlat_1(X0,sK0)
| ~ v9_conlat_1(X0,sK0) ),
inference(superposition,[status(thm)],[c_4971,c_79]) ).
tcf(c_8557,plain,
( v7_conlat_1(iPr_def_11,iPr_def_10)
| l3_conlat_1(iPr_def_12,k7_conlat_2(iPr_def_10))
| ~ l3_conlat_1(iPr_def_11,iPr_def_10)
| ~ v9_conlat_1(iPr_def_11,iPr_def_10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8553,c_6964,c_6931]) ).
tcf(c_8562,plain,
( v3_conlat_1(sK0)
| l3_conlat_1(iPr_def_11,iPr_def_10)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0)
| ~ v9_conlat_1(sK1,sK0) ),
inference(light_normalisation,[status(thm)],[c_8552,c_4971]) ).
tcf(c_8563,plain,
l3_conlat_1(iPr_def_11,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_8562,c_4976,c_4979,c_4974,c_4977,c_4978]) ).
tcf(c_8564,plain,
( v7_conlat_1(iPr_def_11,iPr_def_10)
| l3_conlat_1(iPr_def_12,k7_conlat_2(iPr_def_10))
| ~ v9_conlat_1(iPr_def_11,iPr_def_10) ),
inference(backward_subsumption_resolution,[status(thm)],[c_8557,c_8563]) ).
tcf(c_8568,plain,
! [X0: $i] :
( v7_conlat_1(X0,sK0)
| l3_conlat_1(k9_conlat_2(sK0,X0),iPr_def_10)
| ~ l3_conlat_1(X0,sK0)
| ~ v9_conlat_1(X0,sK0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8554,c_4976,c_4974]) ).
tcf(c_8601,plain,
( v3_conlat_1(iPr_def_10)
| ( u5_conlat_1(k7_conlat_2(iPr_def_10),k8_conlat_2(iPr_def_10,iPr_def_11)) = u4_conlat_1(iPr_def_10,iPr_def_11) )
| ~ l2_conlat_1(iPr_def_10) ),
inference(superposition,[status(thm)],[c_8563,c_807]) ).
tcf(c_8604,plain,
u5_conlat_1(k7_conlat_2(iPr_def_10),k8_conlat_2(iPr_def_10,iPr_def_11)) = u4_conlat_1(iPr_def_10,iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_8601,c_6964,c_6931]) ).
tcf(c_8670,plain,
! [X0: $i] :
( v3_conlat_1(iPr_def_10)
| v7_conlat_1(X0,sK0)
| ( u4_conlat_1(k7_conlat_2(iPr_def_10),k8_conlat_2(iPr_def_10,k9_conlat_2(sK0,X0))) = u5_conlat_1(iPr_def_10,k9_conlat_2(sK0,X0)) )
| ~ l2_conlat_1(iPr_def_10)
| ~ l3_conlat_1(X0,sK0)
| ~ v9_conlat_1(X0,sK0) ),
inference(superposition,[status(thm)],[c_8568,c_806]) ).
tcf(c_8671,plain,
! [X0: $i] :
( v7_conlat_1(X0,sK0)
| ( u4_conlat_1(k7_conlat_2(iPr_def_10),k8_conlat_2(iPr_def_10,k9_conlat_2(sK0,X0))) = u5_conlat_1(iPr_def_10,k9_conlat_2(sK0,X0)) )
| ~ l3_conlat_1(X0,sK0)
| ~ v9_conlat_1(X0,sK0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8670,c_6964,c_6931]) ).
tcf(c_8689,plain,
( v7_conlat_1(iPr_def_11,iPr_def_10)
| l3_conlat_1(iPr_def_12,k7_conlat_2(iPr_def_10)) ),
inference(global_subsumption_just,[status(thm)],[c_8564,c_8524,c_8564]) ).
tcf(c_8806,plain,
( v3_conlat_1(sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0)
| ~ v9_conlat_1(sK1,sK0)
| ~ v7_conlat_1(iPr_def_11,k7_conlat_2(sK0)) ),
inference(superposition,[status(thm)],[c_4972,c_77]) ).
tcf(c_8812,plain,
( v3_conlat_1(sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0)
| ~ v9_conlat_1(sK1,sK0)
| ~ v7_conlat_1(iPr_def_11,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_8806,c_4971]) ).
tcf(c_8813,plain,
~ v7_conlat_1(iPr_def_11,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_8812,c_4976,c_4979,c_4974,c_4977,c_4978]) ).
tcf(c_8820,plain,
l3_conlat_1(iPr_def_12,k7_conlat_2(iPr_def_10)),
inference(backward_subsumption_resolution,[status(thm)],[c_8689,c_8813]) ).
tcf(c_8835,plain,
( v3_conlat_1(sK0)
| v7_conlat_1(sK1,sK0)
| ( k9_conlat_2(sK0,sK1) = k8_conlat_2(sK0,sK1) )
| ~ l2_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0) ),
inference(superposition,[status(thm)],[c_4978,c_134]) ).
tcf(c_8839,plain,
( v3_conlat_1(iPr_def_10)
| v7_conlat_1(iPr_def_11,iPr_def_10)
| ( k9_conlat_2(iPr_def_10,iPr_def_11) = k8_conlat_2(iPr_def_10,iPr_def_11) )
| ~ l2_conlat_1(iPr_def_10)
| ~ l3_conlat_1(iPr_def_11,iPr_def_10) ),
inference(superposition,[status(thm)],[c_8524,c_134]) ).
tcf(c_8841,plain,
( v3_conlat_1(iPr_def_10)
| v7_conlat_1(iPr_def_11,iPr_def_10)
| ( k8_conlat_2(iPr_def_10,iPr_def_11) = iPr_def_12 )
| ~ l2_conlat_1(iPr_def_10)
| ~ l3_conlat_1(iPr_def_11,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_8839,c_4973]) ).
tcf(c_8842,plain,
( v7_conlat_1(iPr_def_11,iPr_def_10)
| ( k8_conlat_2(iPr_def_10,iPr_def_11) = iPr_def_12 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8841,c_6964,c_6931,c_8563]) ).
tcf(c_8845,plain,
( v3_conlat_1(sK0)
| v7_conlat_1(sK1,sK0)
| ( k8_conlat_2(sK0,sK1) = iPr_def_11 )
| ~ l2_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0) ),
inference(light_normalisation,[status(thm)],[c_8835,c_4972]) ).
tcf(c_8846,plain,
k8_conlat_2(sK0,sK1) = iPr_def_11,
inference(forward_subsumption_resolution,[status(thm)],[c_8845,c_4976,c_4979,c_4974,c_4977]) ).
tcf(c_8876,plain,
u4_conlat_1(sK0,sK1) = u5_conlat_1(iPr_def_10,iPr_def_11),
inference(demodulation,[status(thm)],[c_7321,c_8846]) ).
tcf(c_8877,plain,
u4_conlat_1(iPr_def_10,iPr_def_11) = u5_conlat_1(sK0,sK1),
inference(demodulation,[status(thm)],[c_6983,c_8846]) ).
tcf(c_8878,plain,
g3_conlat_1(sK0,u4_conlat_1(sK0,sK1),u4_conlat_1(iPr_def_10,iPr_def_11)) = sK1,
inference(demodulation,[status(thm)],[c_8422,c_8877]) ).
tcf(c_8973,plain,
k8_conlat_2(iPr_def_10,iPr_def_11) = iPr_def_12,
inference(global_subsumption_just,[status(thm)],[c_8842,c_8813,c_8842]) ).
tcf(c_8975,plain,
u5_conlat_1(k7_conlat_2(iPr_def_10),iPr_def_12) = u4_conlat_1(iPr_def_10,iPr_def_11),
inference(demodulation,[status(thm)],[c_8604,c_8973]) ).
tcf(c_8977,plain,
( v3_conlat_1(iPr_def_10)
| v6_conlat_1(iPr_def_12,k7_conlat_2(iPr_def_10))
| ~ l2_conlat_1(iPr_def_10)
| ~ l3_conlat_1(iPr_def_11,iPr_def_10) ),
inference(superposition,[status(thm)],[c_8973,c_74]) ).
tcf(c_8978,plain,
v6_conlat_1(iPr_def_12,k7_conlat_2(iPr_def_10)),
inference(forward_subsumption_resolution,[status(thm)],[c_8977,c_6964,c_6931,c_8563]) ).
tcf(c_8979,plain,
( ( g3_conlat_1(k7_conlat_2(iPr_def_10),u4_conlat_1(k7_conlat_2(iPr_def_10),iPr_def_12),u5_conlat_1(k7_conlat_2(iPr_def_10),iPr_def_12)) = iPr_def_12 )
| ~ l1_conlat_1(k7_conlat_2(iPr_def_10))
| ~ l3_conlat_1(iPr_def_12,k7_conlat_2(iPr_def_10)) ),
inference(superposition,[status(thm)],[c_8978,c_58]) ).
tcf(c_8980,plain,
( ( g3_conlat_1(k7_conlat_2(iPr_def_10),u4_conlat_1(k7_conlat_2(iPr_def_10),iPr_def_12),u4_conlat_1(iPr_def_10,iPr_def_11)) = iPr_def_12 )
| ~ l1_conlat_1(k7_conlat_2(iPr_def_10))
| ~ l3_conlat_1(iPr_def_12,k7_conlat_2(iPr_def_10)) ),
inference(light_normalisation,[status(thm)],[c_8979,c_8975]) ).
tcf(c_8981,plain,
( ( g3_conlat_1(k7_conlat_2(iPr_def_10),u4_conlat_1(k7_conlat_2(iPr_def_10),iPr_def_12),u4_conlat_1(iPr_def_10,iPr_def_11)) = iPr_def_12 )
| ~ l1_conlat_1(k7_conlat_2(iPr_def_10)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8980,c_8820]) ).
tcf(c_9666,plain,
k4_relat_1(k4_relat_1(u3_conlat_1(sK0))) = u3_conlat_1(sK0),
inference(superposition,[status(thm)],[c_4974,c_7275]) ).
tcf(c_10222,plain,
( v7_conlat_1(sK1,sK0)
| ( u4_conlat_1(k7_conlat_2(iPr_def_10),k8_conlat_2(iPr_def_10,k9_conlat_2(sK0,sK1))) = u5_conlat_1(iPr_def_10,k9_conlat_2(sK0,sK1)) )
| ~ l3_conlat_1(sK1,sK0) ),
inference(superposition,[status(thm)],[c_4978,c_8671]) ).
tcf(c_10225,plain,
( v7_conlat_1(sK1,sK0)
| ( u4_conlat_1(k7_conlat_2(iPr_def_10),iPr_def_12) = u4_conlat_1(sK0,sK1) )
| ~ l3_conlat_1(sK1,sK0) ),
inference(light_normalisation,[status(thm)],[c_10222,c_4972,c_8876,c_8973]) ).
tcf(c_10226,plain,
u4_conlat_1(k7_conlat_2(iPr_def_10),iPr_def_12) = u4_conlat_1(sK0,sK1),
inference(forward_subsumption_resolution,[status(thm)],[c_10225,c_4979,c_4977]) ).
tcf(c_22125,plain,
k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = k4_relat_1(u3_conlat_1(sK0)),
inference(superposition,[status(thm)],[c_4974,c_7433]) ).
tcf(c_22131,plain,
k6_relset_1(u1_conlat_1(iPr_def_10),u2_conlat_1(iPr_def_10),u3_conlat_1(iPr_def_10)) = k4_relat_1(u3_conlat_1(iPr_def_10)),
inference(superposition,[status(thm)],[c_6931,c_7433]) ).
tcf(c_22137,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k4_relat_1(u3_conlat_1(sK0)) = X2 )
| ~ m1_relset_1(k4_relat_1(u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0))
| ( g2_conlat_1(X0,X1,X2) != iPr_def_10 ) ),
inference(demodulation,[status(thm)],[c_8237,c_22125]) ).
tcf(c_22138,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( u2_conlat_1(sK0) = X0 )
| ~ m1_relset_1(k4_relat_1(u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0))
| ( g2_conlat_1(X0,X1,X2) != iPr_def_10 ) ),
inference(demodulation,[status(thm)],[c_8241,c_22125]) ).
tcf(c_22139,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( u1_conlat_1(sK0) = X1 )
| ~ m1_relset_1(k4_relat_1(u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0))
| ( g2_conlat_1(X0,X1,X2) != iPr_def_10 ) ),
inference(demodulation,[status(thm)],[c_8240,c_22125]) ).
tcf(c_22140,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k4_relat_1(u3_conlat_1(sK0)) = X2 )
| ~ m1_relset_1(X2,X0,X1)
| ( g2_conlat_1(X0,X1,X2) != iPr_def_10 ) ),
inference(demodulation,[status(thm)],[c_8245,c_22125]) ).
tcf(c_22162,plain,
g2_conlat_1(u2_conlat_1(iPr_def_10),u1_conlat_1(iPr_def_10),k4_relat_1(u3_conlat_1(iPr_def_10))) = k7_conlat_2(iPr_def_10),
inference(demodulation,[status(thm)],[c_8041,c_22131]) ).
tcf(c_22192,plain,
( m1_relset_1(k4_relat_1(u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0))
| ~ m2_relset_1(u3_conlat_1(sK0),u1_conlat_1(sK0),u2_conlat_1(sK0)) ),
inference(superposition,[status(thm)],[c_22125,c_7421]) ).
tcf(c_22292,plain,
m1_relset_1(k4_relat_1(u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0)),
inference(global_subsumption_just,[status(thm)],[c_22192,c_56,c_191,c_22192]) ).
tcf(c_22294,plain,
m2_relset_1(k4_relat_1(u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0)),
inference(superposition,[status(thm)],[c_22292,c_135]) ).
tcf(c_22318,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k4_relat_1(u3_conlat_1(sK0)) = X2 )
| ( g2_conlat_1(X0,X1,X2) != iPr_def_10 ) ),
inference(global_subsumption_just,[status(thm)],[c_22140,c_56,c_191,c_22137,c_22192]) ).
tcf(c_22328,plain,
k4_relat_1(u3_conlat_1(sK0)) = u3_conlat_1(iPr_def_10),
inference(superposition,[status(thm)],[c_7778,c_22318]) ).
tcf(c_22340,plain,
k4_relat_1(u3_conlat_1(iPr_def_10)) = u3_conlat_1(sK0),
inference(demodulation,[status(thm)],[c_9666,c_22328]) ).
tcf(c_22354,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( u2_conlat_1(sK0) = X0 )
| ( g2_conlat_1(X0,X1,X2) != iPr_def_10 ) ),
inference(global_subsumption_just,[status(thm)],[c_22138,c_56,c_191,c_22138,c_22192]) ).
tcf(c_22364,plain,
u1_conlat_1(iPr_def_10) = u2_conlat_1(sK0),
inference(superposition,[status(thm)],[c_7778,c_22354]) ).
tcf(c_22411,plain,
g2_conlat_1(u1_conlat_1(sK0),u1_conlat_1(iPr_def_10),u3_conlat_1(sK0)) = sK0,
inference(demodulation,[status(thm)],[c_7781,c_22364]) ).
tcf(c_22501,plain,
m2_relset_1(u3_conlat_1(iPr_def_10),u1_conlat_1(iPr_def_10),u1_conlat_1(sK0)),
inference(light_normalisation,[status(thm)],[c_22294,c_22328,c_22364]) ).
tcf(c_22505,plain,
k6_relset_1(u1_conlat_1(iPr_def_10),u1_conlat_1(sK0),u3_conlat_1(iPr_def_10)) = k4_relat_1(u3_conlat_1(iPr_def_10)),
inference(superposition,[status(thm)],[c_22501,c_2689]) ).
tcf(c_22508,plain,
k6_relset_1(u1_conlat_1(iPr_def_10),u1_conlat_1(sK0),u3_conlat_1(iPr_def_10)) = u3_conlat_1(sK0),
inference(light_normalisation,[status(thm)],[c_22505,c_22340]) ).
tcf(c_22778,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( u1_conlat_1(sK0) = X1 )
| ( g2_conlat_1(X0,X1,X2) != iPr_def_10 ) ),
inference(global_subsumption_just,[status(thm)],[c_22139,c_56,c_191,c_22139,c_22192]) ).
tcf(c_22787,plain,
u1_conlat_1(sK0) = u2_conlat_1(iPr_def_10),
inference(superposition,[status(thm)],[c_7778,c_22778]) ).
tcf(c_23750,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_22787,c_22508,c_22505,c_22411,c_22162,c_10226,c_8981,c_8878,c_6863,c_4981]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT345+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.37 % Computer : n020.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 21:15:33 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.41 Running first-order theorem proving
% 0.10/0.41 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...
% 10.70/2.73 % SZS status Started for theBenchmark.p
% 10.70/2.73 % SZS status Theorem for theBenchmark.p
% 10.70/2.73
% 10.70/2.73 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.70/2.73
% 10.70/2.73 % ------ iProver source info
% 10.70/2.73
% 10.70/2.73 % git: date: 2026-07-19 20:42:38 +0200
% 10.70/2.73 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.70/2.73 % git: non_committed_changes: false
% 10.70/2.73
% 10.70/2.73 % ------ Parsing...
% 10.70/2.73 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 10.70/2.73
% 10.70/2.73 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 10.70/2.73
% 10.70/2.73 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 10.70/2.73
% 10.70/2.73 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 10.70/2.73 % ------ Proving...
% 10.70/2.73 % ------ Problem Properties
% 10.70/2.73
% 10.70/2.73 %
% 10.70/2.73 % clauses 99
% 10.70/2.73 % conjectures 8
% 10.70/2.73 % EPR 27
% 10.70/2.73 % Horn 72
% 10.70/2.73 % unary 28
% 10.70/2.73 % binary 22
% 10.70/2.73 % lits 252
% 10.70/2.73 % lits eq 30
% 10.70/2.73 % fd_pure 0
% 10.70/2.73 % fd_pseudo 0
% 10.70/2.73 % fd_cond 1
% 10.70/2.73 % fd_pseudo_cond 8
% 10.70/2.73 % AC symbols 0
% 10.70/2.73
% 10.70/2.73 % ------ Schedule dynamic 5 is on
% 10.70/2.73
% 10.70/2.73 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 10.70/2.73
% 10.70/2.73
% 10.70/2.73 % ------
% 10.70/2.73 % Current options:
% 10.70/2.73 % ------
% 10.70/2.73
% 10.70/2.73
% 10.70/2.73 %
% 10.70/2.73
% 10.70/2.73 % ------ Proving...
% 10.70/2.73 %
% 10.70/2.73
% 10.70/2.73 % SZS status Theorem for theBenchmark.p
% 10.70/2.73
% 10.70/2.73 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.70/2.73
% 10.70/2.73
%------------------------------------------------------------------------------