%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT345+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:48:32 AM UTC 2026
% Result : Theorem 11.64s 4.96s
% Output : Refutation 11.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 38
% Syntax : Number of formulae : 298 ( 42 unt; 19 def)
% Number of atoms : 952 ( 150 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 1122 ( 468 ~; 539 |; 66 &)
% ( 23 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 33 ( 31 usr; 20 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 2 con; 0-3 aty)
% Number of variables : 214 ( 0 sgn 210 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_conlat_1(X0)
& v4_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( ( v6_conlat_1(X1,X0)
& ~ v7_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& l3_conlat_1(X1,X0) )
=> k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1)) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t20_conlat_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_conlat_1(X0)
& v4_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( ( v6_conlat_1(X1,X0)
& ~ v7_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& l3_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/sandbox/benchmark/theBenchmark.p',abstractness_v4_conlat_1) ).
fof(f4,axiom,
! [X0,X1] :
( ( l1_conlat_1(X0)
& l3_conlat_1(X1,X0) )
=> ( v6_conlat_1(X1,X0)
=> X1 = g3_conlat_1(X0,u4_conlat_1(X0,X1),u5_conlat_1(X0,X1)) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f8,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_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/sandbox/benchmark/theBenchmark.p',d7_conlat_2) ).
fof(f9,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( l3_conlat_1(X1,X0)
=> ! [X2] :
( ( v6_conlat_1(X2,k7_conlat_2(X0))
& l3_conlat_1(X2,k7_conlat_2(X0)) )
=> ( X2 = k8_conlat_2(X0,X1)
<=> ( u4_conlat_1(k7_conlat_2(X0),X2) = u5_conlat_1(X0,X1)
& u5_conlat_1(k7_conlat_2(X0),X2) = u4_conlat_1(X0,X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_conlat_2) ).
fof(f10,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> ( v4_conlat_1(g2_conlat_1(X0,X1,X2))
& l2_conlat_1(g2_conlat_1(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_g2_conlat_1) ).
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/sandbox/benchmark/theBenchmark.p',dt_k6_relset_1) ).
fof(f17,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_conlat_1(k7_conlat_2(X0))
& v4_conlat_1(k7_conlat_2(X0))
& l2_conlat_1(k7_conlat_2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_conlat_2) ).
fof(f18,axiom,
! [X0,X1] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0)
& l3_conlat_1(X1,X0) )
=> ( v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
& l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_conlat_2) ).
fof(f19,axiom,
! [X0,X1] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0)
& ~ v7_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& l3_conlat_1(X1,X0) )
=> ( v6_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& ~ v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& l3_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_conlat_2) ).
fof(f21,axiom,
! [X0] :
( l2_conlat_1(X0)
=> l1_conlat_1(X0) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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)
=> ( X0 = X3
& X1 = X4
& X2 = X5 ) ) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',redefinition_k6_relset_1) ).
fof(f60,axiom,
! [X0,X1] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0)
& ~ v7_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& l3_conlat_1(X1,X0) )
=> k9_conlat_2(X0,X1) = k8_conlat_2(X0,X1) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f75,plain,
? [X0] :
( ? [X1] :
( k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1)) != X1
& v6_conlat_1(X1,X0)
& ~ v7_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& l3_conlat_1(X1,X0) )
& ~ v3_conlat_1(X0)
& v4_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f76,plain,
? [X0] :
( ? [X1] :
( k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1)) != X1
& v6_conlat_1(X1,X0)
& ~ v7_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& l3_conlat_1(X1,X0) )
& ~ v3_conlat_1(X0)
& v4_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
! [X0] :
( X0 = g2_conlat_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0))
| ~ v4_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f78,plain,
! [X0] :
( X0 = g2_conlat_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0))
| ~ v4_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
! [X0,X1] :
( X1 = g3_conlat_1(X0,u4_conlat_1(X0,X1),u5_conlat_1(X0,X1))
| ~ v6_conlat_1(X1,X0)
| ~ l1_conlat_1(X0)
| ~ l3_conlat_1(X1,X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f80,plain,
! [X0,X1] :
( X1 = g3_conlat_1(X0,u4_conlat_1(X0,X1),u5_conlat_1(X0,X1))
| ~ v6_conlat_1(X1,X0)
| ~ l1_conlat_1(X0)
| ~ l3_conlat_1(X1,X0) ),
inference(flattening,[],[f79]) ).
fof(f82,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f6]) ).
fof(f83,plain,
! [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)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f84,plain,
! [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)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f83]) ).
fof(f85,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k8_conlat_2(X0,X1)
<=> ( u4_conlat_1(k7_conlat_2(X0),X2) = u5_conlat_1(X0,X1)
& u5_conlat_1(k7_conlat_2(X0),X2) = u4_conlat_1(X0,X1) ) )
| ~ v6_conlat_1(X2,k7_conlat_2(X0))
| ~ l3_conlat_1(X2,k7_conlat_2(X0)) )
| ~ l3_conlat_1(X1,X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f86,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k8_conlat_2(X0,X1)
<=> ( u4_conlat_1(k7_conlat_2(X0),X2) = u5_conlat_1(X0,X1)
& u5_conlat_1(k7_conlat_2(X0),X2) = u4_conlat_1(X0,X1) ) )
| ~ v6_conlat_1(X2,k7_conlat_2(X0))
| ~ l3_conlat_1(X2,k7_conlat_2(X0)) )
| ~ l3_conlat_1(X1,X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f85]) ).
fof(f87,plain,
! [X0,X1,X2] :
( ( v4_conlat_1(g2_conlat_1(X0,X1,X2))
& l2_conlat_1(g2_conlat_1(X0,X1,X2)) )
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f91,plain,
! [X0,X1,X2] :
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f16]) ).
fof(f92,plain,
! [X0] :
( ( ~ v3_conlat_1(k7_conlat_2(X0))
& v4_conlat_1(k7_conlat_2(X0))
& l2_conlat_1(k7_conlat_2(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f93,plain,
! [X0] :
( ( ~ v3_conlat_1(k7_conlat_2(X0))
& v4_conlat_1(k7_conlat_2(X0))
& l2_conlat_1(k7_conlat_2(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f92]) ).
fof(f94,plain,
! [X0,X1] :
( ( v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
& l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ l3_conlat_1(X1,X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f95,plain,
! [X0,X1] :
( ( v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
& l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ l3_conlat_1(X1,X0) ),
inference(flattening,[],[f94]) ).
fof(f96,plain,
! [X0,X1] :
( ( v6_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& ~ v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& l3_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v7_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| ~ l3_conlat_1(X1,X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f97,plain,
! [X0,X1] :
( ( v6_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& ~ v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
& l3_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v7_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| ~ l3_conlat_1(X1,X0) ),
inference(flattening,[],[f96]) ).
fof(f98,plain,
! [X0] :
( l1_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f99,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f100,plain,
! [X0] :
( m2_relset_1(u3_conlat_1(X0),u1_conlat_1(X0),u2_conlat_1(X0))
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f112,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g2_conlat_1(X0,X1,X2) != g2_conlat_1(X3,X4,X5) )
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f42]) ).
fof(f115,plain,
! [X0] :
( k4_relat_1(k4_relat_1(X0)) = X0
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f44]) ).
fof(f131,plain,
! [X0,X1,X2] :
( k6_relset_1(X0,X1,X2) = k4_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f59]) ).
fof(f132,plain,
! [X0,X1] :
( k9_conlat_2(X0,X1) = k8_conlat_2(X0,X1)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v7_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| ~ l3_conlat_1(X1,X0) ),
inference(ennf_transformation,[],[f60]) ).
fof(f133,plain,
! [X0,X1] :
( k9_conlat_2(X0,X1) = k8_conlat_2(X0,X1)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v7_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| ~ l3_conlat_1(X1,X0) ),
inference(flattening,[],[f132]) ).
fof(f144,plain,
l3_conlat_1(sK1,sK0),
inference(cnf_transformation,[],[f76]) ).
fof(f145,plain,
v9_conlat_1(sK1,sK0),
inference(cnf_transformation,[],[f76]) ).
fof(f146,plain,
~ v7_conlat_1(sK1,sK0),
inference(cnf_transformation,[],[f76]) ).
fof(f147,plain,
v6_conlat_1(sK1,sK0),
inference(cnf_transformation,[],[f76]) ).
fof(f148,plain,
sK1 != k9_conlat_2(k7_conlat_2(sK0),k9_conlat_2(sK0,sK1)),
inference(cnf_transformation,[],[f76]) ).
fof(f149,plain,
l2_conlat_1(sK0),
inference(cnf_transformation,[],[f76]) ).
fof(f150,plain,
v4_conlat_1(sK0),
inference(cnf_transformation,[],[f76]) ).
fof(f151,plain,
~ v3_conlat_1(sK0),
inference(cnf_transformation,[],[f76]) ).
fof(f152,plain,
! [X0] :
( ~ v4_conlat_1(X0)
| ~ l2_conlat_1(X0)
| g2_conlat_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0)) = X0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f153,plain,
! [X0,X1] :
( ~ v6_conlat_1(X1,X0)
| ~ l1_conlat_1(X0)
| ~ l3_conlat_1(X1,X0)
| g3_conlat_1(X0,u4_conlat_1(X0,X1),u5_conlat_1(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f80]) ).
fof(f155,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(f156,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(f157,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))
| u4_conlat_1(X0,X1) = u5_conlat_1(k7_conlat_2(X0),X2)
| k8_conlat_2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f86]) ).
fof(f158,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))
| u5_conlat_1(X0,X1) = u4_conlat_1(k7_conlat_2(X0),X2)
| k8_conlat_2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f86]) ).
fof(f161,plain,
! [X2,X0,X1] :
( v4_conlat_1(g2_conlat_1(X0,X1,X2))
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f87]) ).
fof(f165,plain,
! [X2,X0,X1] :
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f91]) ).
fof(f166,plain,
! [X0] :
( l2_conlat_1(k7_conlat_2(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f168,plain,
! [X0] :
( ~ v3_conlat_1(k7_conlat_2(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f169,plain,
! [X0,X1] :
( l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l3_conlat_1(X1,X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f170,plain,
! [X0,X1] :
( v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l3_conlat_1(X1,X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f172,plain,
! [X0,X1] :
( v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l3_conlat_1(X1,X0) ),
inference(cnf_transformation,[],[f97]) ).
fof(f173,plain,
! [X0,X1] :
( ~ v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))
| ~ v9_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l3_conlat_1(X1,X0) ),
inference(cnf_transformation,[],[f97]) ).
fof(f175,plain,
! [X0] :
( l1_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f176,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f177,plain,
! [X0] :
( m2_relset_1(u3_conlat_1(X0),u1_conlat_1(X0),u2_conlat_1(X0))
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f191,plain,
! [X2,X3,X0,X1,X4,X5] :
( g2_conlat_1(X0,X1,X2) != g2_conlat_1(X3,X4,X5)
| ~ m1_relset_1(X2,X0,X1)
| X2 = X5 ),
inference(cnf_transformation,[],[f112]) ).
fof(f192,plain,
! [X2,X3,X0,X1,X4,X5] :
( g2_conlat_1(X0,X1,X2) != g2_conlat_1(X3,X4,X5)
| ~ m1_relset_1(X2,X0,X1)
| X1 = X4 ),
inference(cnf_transformation,[],[f112]) ).
fof(f193,plain,
! [X2,X3,X0,X1,X4,X5] :
( g2_conlat_1(X0,X1,X2) != g2_conlat_1(X3,X4,X5)
| ~ m1_relset_1(X2,X0,X1)
| X0 = X3 ),
inference(cnf_transformation,[],[f112]) ).
fof(f197,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k4_relat_1(k4_relat_1(X0)) = X0 ),
inference(cnf_transformation,[],[f115]) ).
fof(f228,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(f229,plain,
! [X0,X1] :
( ~ v9_conlat_1(X1,X0)
| ~ l3_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(f230,plain,
! [X2,X0,X1] :
( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f61]) ).
fof(f231,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f61]) ).
fof(f241,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,[],[f158]) ).
fof(f242,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,[],[f157]) ).
fof(f243,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l3_conlat_1(X1,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(forward_subsumption_resolution,[],[f242,f169]) ).
fof(f244,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l3_conlat_1(X1,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(forward_subsumption_resolution,[],[f241,f169]) ).
fof(f245,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| u4_conlat_1(X0,X1) = u5_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f243,f170]) ).
fof(f246,plain,
! [X0,X1] :
( ~ l3_conlat_1(X1,X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| u5_conlat_1(X0,X1) = u4_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f244,f170]) ).
fof(f287,plain,
! [X0] :
( m1_relset_1(u3_conlat_1(X0),u1_conlat_1(X0),u2_conlat_1(X0))
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f177,f231]) ).
fof(f307,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f176,f155]) ).
fof(f312,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f307,f230]) ).
fof(f348,plain,
( ~ l2_conlat_1(sK0)
| sK0 = g2_conlat_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) ),
inference(resolution,[],[f152,f150]) ).
fof(f353,plain,
sK0 = g2_conlat_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)),
inference(forward_subsumption_resolution,[],[f348,f149]) ).
fof(f369,definition,
( spl21_3
<=> m1_relset_1(u3_conlat_1(sK0),u1_conlat_1(sK0),u2_conlat_1(sK0)) ),
introduced(definition,[new_symbols(definition,[spl21_3])],[avatar_definition]) ).
fof(f370,plain,
( m1_relset_1(u3_conlat_1(sK0),u1_conlat_1(sK0),u2_conlat_1(sK0))
| ~ spl21_3 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f371,plain,
( ~ m1_relset_1(u3_conlat_1(sK0),u1_conlat_1(sK0),u2_conlat_1(sK0))
| spl21_3 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f383,plain,
( v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| u4_conlat_1(sK0,sK1) = u5_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) ),
inference(resolution,[],[f245,f144]) ).
fof(f398,plain,
( ~ l2_conlat_1(sK0)
| u4_conlat_1(sK0,sK1) = u5_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f383,f151]) ).
fof(f400,plain,
u4_conlat_1(sK0,sK1) = u5_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),
inference(forward_subsumption_resolution,[],[f398,f149]) ).
fof(f404,definition,
( spl21_5
<=> l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl21_5])],[avatar_definition]) ).
fof(f405,plain,
( l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ spl21_5 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f406,plain,
( ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| spl21_5 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f416,plain,
( ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0)
| spl21_5 ),
inference(resolution,[],[f406,f169]) ).
fof(f417,plain,
( v3_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0)
| spl21_5 ),
inference(forward_subsumption_resolution,[],[f416,f149]) ).
fof(f418,plain,
( ~ l3_conlat_1(sK1,sK0)
| spl21_5 ),
inference(forward_subsumption_resolution,[],[f417,f151]) ).
fof(f419,plain,
( $false
| spl21_5 ),
inference(forward_subsumption_resolution,[],[f418,f144]) ).
fof(f420,plain,
spl21_5,
inference(avatar_contradiction_clause,[],[f419]) ).
fof(f427,plain,
( v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| u5_conlat_1(sK0,sK1) = u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) ),
inference(resolution,[],[f246,f144]) ).
fof(f442,plain,
( ~ l2_conlat_1(sK0)
| u5_conlat_1(sK0,sK1) = u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f427,f151]) ).
fof(f444,plain,
u5_conlat_1(sK0,sK1) = u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),
inference(forward_subsumption_resolution,[],[f442,f149]) ).
fof(f446,plain,
( v3_conlat_1(k7_conlat_2(sK0))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| u5_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)))
| ~ spl21_5 ),
inference(resolution,[],[f405,f246]) ).
fof(f447,plain,
( v3_conlat_1(k7_conlat_2(sK0))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)))
| ~ spl21_5 ),
inference(resolution,[],[f405,f245]) ).
fof(f448,plain,
( u5_conlat_1(sK0,sK1) = u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)))
| v3_conlat_1(k7_conlat_2(sK0))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| ~ spl21_5 ),
inference(forward_demodulation,[],[f447,f444]) ).
fof(f449,plain,
( u4_conlat_1(sK0,sK1) = u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)))
| v3_conlat_1(k7_conlat_2(sK0))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| ~ spl21_5 ),
inference(forward_demodulation,[],[f446,f400]) ).
fof(f451,definition,
( spl21_8
<=> l2_conlat_1(k7_conlat_2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl21_8])],[avatar_definition]) ).
fof(f452,plain,
( l2_conlat_1(k7_conlat_2(sK0))
| ~ spl21_8 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f453,plain,
( ~ l2_conlat_1(k7_conlat_2(sK0))
| spl21_8 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f455,definition,
( spl21_9
<=> v3_conlat_1(k7_conlat_2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl21_9])],[avatar_definition]) ).
fof(f456,plain,
( ~ v3_conlat_1(k7_conlat_2(sK0))
| spl21_9 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f457,plain,
( v3_conlat_1(k7_conlat_2(sK0))
| ~ spl21_9 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f459,definition,
( spl21_10
<=> u5_conlat_1(sK0,sK1) = u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) ),
introduced(definition,[new_symbols(definition,[spl21_10])],[avatar_definition]) ).
fof(f461,plain,
( u5_conlat_1(sK0,sK1) = u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)))
| ~ spl21_10 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f462,plain,
( ~ spl21_8
| spl21_9
| spl21_10
| ~ spl21_5 ),
inference(avatar_split_clause,[],[f448,f404,f459,f455,f451]) ).
fof(f464,definition,
( spl21_11
<=> u4_conlat_1(sK0,sK1) = u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) ),
introduced(definition,[new_symbols(definition,[spl21_11])],[avatar_definition]) ).
fof(f466,plain,
( u4_conlat_1(sK0,sK1) = u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)))
| ~ spl21_11 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f467,plain,
( ~ spl21_8
| spl21_9
| spl21_11
| ~ spl21_5 ),
inference(avatar_split_clause,[],[f449,f404,f464,f455,f451]) ).
fof(f478,plain,
( v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| spl21_8 ),
inference(resolution,[],[f453,f166]) ).
fof(f479,plain,
( ~ l2_conlat_1(sK0)
| spl21_8 ),
inference(forward_subsumption_resolution,[],[f478,f151]) ).
fof(f480,plain,
( $false
| spl21_8 ),
inference(forward_subsumption_resolution,[],[f479,f149]) ).
fof(f481,plain,
spl21_8,
inference(avatar_contradiction_clause,[],[f480]) ).
fof(f482,plain,
( v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| ~ spl21_9 ),
inference(resolution,[],[f457,f168]) ).
fof(f483,plain,
( ~ l2_conlat_1(sK0)
| ~ spl21_9 ),
inference(forward_subsumption_resolution,[],[f482,f151]) ).
fof(f484,plain,
( $false
| ~ spl21_9 ),
inference(forward_subsumption_resolution,[],[f483,f149]) ).
fof(f485,plain,
~ spl21_9,
inference(avatar_contradiction_clause,[],[f484]) ).
fof(f488,definition,
( spl21_14
<=> l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl21_14])],[avatar_definition]) ).
fof(f489,plain,
( l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ spl21_14 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f490,plain,
( ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| spl21_14 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f492,definition,
( spl21_15
<=> l1_conlat_1(k7_conlat_2(k7_conlat_2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl21_15])],[avatar_definition]) ).
fof(f493,plain,
( l1_conlat_1(k7_conlat_2(k7_conlat_2(sK0)))
| ~ spl21_15 ),
inference(avatar_component_clause,[],[f492]) ).
fof(f494,plain,
( ~ l1_conlat_1(k7_conlat_2(k7_conlat_2(sK0)))
| spl21_15 ),
inference(avatar_component_clause,[],[f492]) ).
fof(f513,plain,
( ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0))
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| spl21_14 ),
inference(resolution,[],[f490,f169]) ).
fof(f514,plain,
( v3_conlat_1(k7_conlat_2(sK0))
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ spl21_8
| spl21_14 ),
inference(forward_subsumption_resolution,[],[f513,f452]) ).
fof(f515,plain,
( ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ spl21_8
| spl21_9
| spl21_14 ),
inference(forward_subsumption_resolution,[],[f514,f456]) ).
fof(f516,plain,
( $false
| ~ spl21_5
| ~ spl21_8
| spl21_9
| spl21_14 ),
inference(forward_subsumption_resolution,[],[f515,f405]) ).
fof(f517,plain,
( ~ spl21_5
| ~ spl21_8
| spl21_9
| spl21_14 ),
inference(avatar_contradiction_clause,[],[f516]) ).
fof(f518,plain,
( ~ l2_conlat_1(k7_conlat_2(k7_conlat_2(sK0)))
| spl21_15 ),
inference(resolution,[],[f494,f175]) ).
fof(f521,plain,
( v3_conlat_1(k7_conlat_2(sK0))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| spl21_15 ),
inference(resolution,[],[f518,f166]) ).
fof(f522,plain,
( ~ l2_conlat_1(k7_conlat_2(sK0))
| spl21_9
| spl21_15 ),
inference(forward_subsumption_resolution,[],[f521,f456]) ).
fof(f523,plain,
( $false
| ~ spl21_8
| spl21_9
| spl21_15 ),
inference(forward_subsumption_resolution,[],[f522,f452]) ).
fof(f524,plain,
( ~ spl21_8
| spl21_9
| spl21_15 ),
inference(avatar_contradiction_clause,[],[f523]) ).
fof(f623,plain,
( ~ l1_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0)
| sK1 = g3_conlat_1(sK0,u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1)) ),
inference(resolution,[],[f153,f147]) ).
fof(f635,plain,
( ~ l1_conlat_1(sK0)
| sK1 = g3_conlat_1(sK0,u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f623,f144]) ).
fof(f639,definition,
( spl21_34
<=> sK1 = g3_conlat_1(sK0,u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1)) ),
introduced(definition,[new_symbols(definition,[spl21_34])],[avatar_definition]) ).
fof(f641,plain,
( sK1 = g3_conlat_1(sK0,u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1))
| ~ spl21_34 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f643,definition,
( spl21_35
<=> l1_conlat_1(sK0) ),
introduced(definition,[new_symbols(definition,[spl21_35])],[avatar_definition]) ).
fof(f645,plain,
( ~ l1_conlat_1(sK0)
| spl21_35 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f646,plain,
( spl21_34
| ~ spl21_35 ),
inference(avatar_split_clause,[],[f635,f643,f639]) ).
fof(f647,plain,
( ~ l2_conlat_1(sK0)
| spl21_35 ),
inference(resolution,[],[f645,f175]) ).
fof(f648,plain,
( $false
| spl21_35 ),
inference(forward_subsumption_resolution,[],[f647,f149]) ).
fof(f649,plain,
spl21_35,
inference(avatar_contradiction_clause,[],[f648]) ).
fof(f1087,plain,
( v3_conlat_1(k7_conlat_2(sK0))
| k7_conlat_2(k7_conlat_2(sK0)) = g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0)),u1_conlat_1(k7_conlat_2(sK0)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)),u3_conlat_1(k7_conlat_2(sK0))))
| ~ spl21_8 ),
inference(resolution,[],[f156,f452]) ).
fof(f1091,plain,
( v3_conlat_1(sK0)
| k7_conlat_2(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))) ),
inference(resolution,[],[f156,f149]) ).
fof(f1114,plain,
k7_conlat_2(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))),
inference(forward_subsumption_resolution,[],[f1091,f151]) ).
fof(f1117,plain,
( k7_conlat_2(k7_conlat_2(sK0)) = g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0)),u1_conlat_1(k7_conlat_2(sK0)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)),u3_conlat_1(k7_conlat_2(sK0))))
| ~ spl21_8
| spl21_9 ),
inference(forward_subsumption_resolution,[],[f1087,f456]) ).
fof(f1273,plain,
( v4_conlat_1(k7_conlat_2(sK0))
| ~ 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)) ),
inference(superposition,[],[f161,f1114]) ).
fof(f1274,plain,
! [X2,X0,X1] :
( g2_conlat_1(X0,X1,X2) != k7_conlat_2(sK0)
| ~ 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))
| k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = X2 ),
inference(superposition,[],[f191,f1114]) ).
fof(f1276,plain,
! [X2,X0,X1] :
( g2_conlat_1(X0,X1,X2) != k7_conlat_2(sK0)
| ~ 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))
| u1_conlat_1(sK0) = X1 ),
inference(superposition,[],[f192,f1114]) ).
fof(f1278,plain,
! [X2,X0,X1] :
( g2_conlat_1(X0,X1,X2) != k7_conlat_2(sK0)
| ~ 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))
| u2_conlat_1(sK0) = X0 ),
inference(superposition,[],[f193,f1114]) ).
fof(f1294,definition,
( spl21_92
<=> 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)) ),
introduced(definition,[new_symbols(definition,[spl21_92])],[avatar_definition]) ).
fof(f1296,plain,
( ~ 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))
| spl21_92 ),
inference(avatar_component_clause,[],[f1294]) ).
fof(f1347,definition,
( spl21_103
<=> ! [X2,X0,X1] :
( g2_conlat_1(X0,X1,X2) != k7_conlat_2(sK0)
| u2_conlat_1(sK0) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl21_103])],[avatar_definition]) ).
fof(f1348,plain,
( ! [X2,X0,X1] :
( g2_conlat_1(X0,X1,X2) != k7_conlat_2(sK0)
| u2_conlat_1(sK0) = X0 )
| ~ spl21_103 ),
inference(avatar_component_clause,[],[f1347]) ).
fof(f1349,plain,
( ~ spl21_92
| spl21_103 ),
inference(avatar_split_clause,[],[f1278,f1347,f1294]) ).
fof(f1351,definition,
( spl21_104
<=> ! [X2,X0,X1] :
( g2_conlat_1(X0,X1,X2) != k7_conlat_2(sK0)
| u1_conlat_1(sK0) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl21_104])],[avatar_definition]) ).
fof(f1352,plain,
( ! [X2,X0,X1] :
( g2_conlat_1(X0,X1,X2) != k7_conlat_2(sK0)
| u1_conlat_1(sK0) = X1 )
| ~ spl21_104 ),
inference(avatar_component_clause,[],[f1351]) ).
fof(f1353,plain,
( ~ spl21_92
| spl21_104 ),
inference(avatar_split_clause,[],[f1276,f1351,f1294]) ).
fof(f1355,definition,
( spl21_105
<=> ! [X2,X0,X1] :
( g2_conlat_1(X0,X1,X2) != k7_conlat_2(sK0)
| k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = X2 ) ),
introduced(definition,[new_symbols(definition,[spl21_105])],[avatar_definition]) ).
fof(f1356,plain,
( ! [X2,X0,X1] :
( g2_conlat_1(X0,X1,X2) != k7_conlat_2(sK0)
| k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = X2 )
| ~ spl21_105 ),
inference(avatar_component_clause,[],[f1355]) ).
fof(f1357,plain,
( ~ spl21_92
| spl21_105 ),
inference(avatar_split_clause,[],[f1274,f1355,f1294]) ).
fof(f1359,definition,
( spl21_106
<=> v4_conlat_1(k7_conlat_2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl21_106])],[avatar_definition]) ).
fof(f1361,plain,
( v4_conlat_1(k7_conlat_2(sK0))
| ~ spl21_106 ),
inference(avatar_component_clause,[],[f1359]) ).
fof(f1362,plain,
( ~ spl21_92
| spl21_106 ),
inference(avatar_split_clause,[],[f1273,f1359,f1294]) ).
fof(f1425,definition,
( spl21_116
<=> u1_conlat_1(sK0) = u2_conlat_1(k7_conlat_2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl21_116])],[avatar_definition]) ).
fof(f1427,plain,
( u1_conlat_1(sK0) = u2_conlat_1(k7_conlat_2(sK0))
| ~ spl21_116 ),
inference(avatar_component_clause,[],[f1425]) ).
fof(f1429,definition,
( spl21_117
<=> sK0 = k7_conlat_2(k7_conlat_2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl21_117])],[avatar_definition]) ).
fof(f1430,plain,
( sK0 = k7_conlat_2(k7_conlat_2(sK0))
| ~ spl21_117 ),
inference(avatar_component_clause,[],[f1429]) ).
fof(f1431,plain,
( sK0 != k7_conlat_2(k7_conlat_2(sK0))
| spl21_117 ),
inference(avatar_component_clause,[],[f1429]) ).
fof(f1434,definition,
( spl21_118
<=> u2_conlat_1(sK0) = u1_conlat_1(k7_conlat_2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl21_118])],[avatar_definition]) ).
fof(f1436,plain,
( u2_conlat_1(sK0) = u1_conlat_1(k7_conlat_2(sK0))
| ~ spl21_118 ),
inference(avatar_component_clause,[],[f1434]) ).
fof(f2368,plain,
( ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| k9_conlat_2(sK0,sK1) = k8_conlat_2(sK0,sK1) ),
inference(resolution,[],[f229,f145]) ).
fof(f2375,plain,
( v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| k9_conlat_2(sK0,sK1) = k8_conlat_2(sK0,sK1) ),
inference(forward_subsumption_resolution,[],[f2368,f144]) ).
fof(f2379,plain,
( ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| k9_conlat_2(sK0,sK1) = k8_conlat_2(sK0,sK1) ),
inference(forward_subsumption_resolution,[],[f2375,f146]) ).
fof(f2381,plain,
( v3_conlat_1(sK0)
| k9_conlat_2(sK0,sK1) = k8_conlat_2(sK0,sK1) ),
inference(forward_subsumption_resolution,[],[f2379,f149]) ).
fof(f2383,plain,
k9_conlat_2(sK0,sK1) = k8_conlat_2(sK0,sK1),
inference(forward_subsumption_resolution,[],[f2381,f151]) ).
fof(f2453,plain,
sK1 != k9_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),
inference(superposition,[],[f148,f2383]) ).
fof(f2455,plain,
( ~ v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v9_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0) ),
inference(superposition,[],[f173,f2383]) ).
fof(f2456,plain,
( v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v9_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0) ),
inference(superposition,[],[f172,f2383]) ).
fof(f2458,plain,
( v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f2456,f145]) ).
fof(f2459,plain,
( ~ v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f2455,f145]) ).
fof(f2460,plain,
( v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f2458,f146]) ).
fof(f2461,plain,
( ~ v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f2459,f146]) ).
fof(f2462,plain,
( v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| v3_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f2460,f149]) ).
fof(f2463,plain,
( ~ v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| v3_conlat_1(sK0)
| ~ l3_conlat_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f2461,f149]) ).
fof(f2464,plain,
( v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f2462,f151]) ).
fof(f2465,plain,
( ~ v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f2463,f151]) ).
fof(f2466,plain,
v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)),
inference(forward_subsumption_resolution,[],[f2464,f144]) ).
fof(f2467,plain,
~ v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)),
inference(forward_subsumption_resolution,[],[f2465,f144]) ).
fof(f2749,plain,
( ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0))
| k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = k9_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) ),
inference(resolution,[],[f2466,f229]) ).
fof(f2750,plain,
( v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0))
| k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = k9_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ spl21_5 ),
inference(forward_subsumption_resolution,[],[f2749,f405]) ).
fof(f2751,plain,
( ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0))
| k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = k9_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ spl21_5 ),
inference(forward_subsumption_resolution,[],[f2750,f2467]) ).
fof(f2752,plain,
( v3_conlat_1(k7_conlat_2(sK0))
| k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = k9_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ spl21_5
| ~ spl21_8 ),
inference(forward_subsumption_resolution,[],[f2751,f452]) ).
fof(f2753,plain,
( k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = k9_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ spl21_5
| ~ spl21_8
| spl21_9 ),
inference(forward_subsumption_resolution,[],[f2752,f456]) ).
fof(f3036,plain,
( sK1 != k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ spl21_5
| ~ spl21_8
| spl21_9 ),
inference(superposition,[],[f2453,f2753]) ).
fof(f3250,definition,
( spl21_245
<=> v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl21_245])],[avatar_definition]) ).
fof(f3251,plain,
( v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ spl21_245 ),
inference(avatar_component_clause,[],[f3250]) ).
fof(f3252,plain,
( ~ v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| spl21_245 ),
inference(avatar_component_clause,[],[f3250]) ).
fof(f3267,plain,
( ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0))
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| spl21_245 ),
inference(resolution,[],[f3252,f170]) ).
fof(f3268,plain,
( v3_conlat_1(k7_conlat_2(sK0))
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ spl21_8
| spl21_245 ),
inference(forward_subsumption_resolution,[],[f3267,f452]) ).
fof(f3269,plain,
( ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ spl21_8
| spl21_9
| spl21_245 ),
inference(forward_subsumption_resolution,[],[f3268,f456]) ).
fof(f3270,plain,
( $false
| ~ spl21_5
| ~ spl21_8
| spl21_9
| spl21_245 ),
inference(forward_subsumption_resolution,[],[f3269,f405]) ).
fof(f3271,plain,
( ~ spl21_5
| ~ spl21_8
| spl21_9
| spl21_245 ),
inference(avatar_contradiction_clause,[],[f3270]) ).
fof(f3273,plain,
( ~ l1_conlat_1(k7_conlat_2(k7_conlat_2(sK0)))
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = g3_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))),u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))))
| ~ spl21_245 ),
inference(resolution,[],[f3251,f153]) ).
fof(f3274,plain,
( ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = g3_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))),u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))))
| ~ spl21_15
| ~ spl21_245 ),
inference(forward_subsumption_resolution,[],[f3273,f493]) ).
fof(f3275,plain,
( k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = g3_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))),u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))))
| ~ spl21_14
| ~ spl21_15
| ~ spl21_245 ),
inference(forward_subsumption_resolution,[],[f3274,f489]) ).
fof(f3276,plain,
( k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = g3_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))),u5_conlat_1(sK0,sK1))
| ~ spl21_10
| ~ spl21_14
| ~ spl21_15
| ~ spl21_245 ),
inference(forward_demodulation,[],[f3275,f461]) ).
fof(f3277,plain,
( k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = g3_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1))
| ~ spl21_10
| ~ spl21_11
| ~ spl21_14
| ~ spl21_15
| ~ spl21_245 ),
inference(forward_demodulation,[],[f3276,f466]) ).
fof(f3492,plain,
( ~ l2_conlat_1(sK0)
| spl21_3 ),
inference(resolution,[],[f287,f371]) ).
fof(f3496,plain,
( $false
| spl21_3 ),
inference(forward_subsumption_resolution,[],[f3492,f149]) ).
fof(f3497,plain,
spl21_3,
inference(avatar_contradiction_clause,[],[f3496]) ).
fof(f3537,plain,
( k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = k4_relat_1(u3_conlat_1(sK0))
| ~ spl21_3 ),
inference(resolution,[],[f370,f228]) ).
fof(f3538,plain,
( v1_relat_1(u3_conlat_1(sK0))
| ~ spl21_3 ),
inference(resolution,[],[f370,f312]) ).
fof(f3541,plain,
( u3_conlat_1(sK0) = k4_relat_1(k4_relat_1(u3_conlat_1(sK0)))
| ~ spl21_3 ),
inference(resolution,[],[f3538,f197]) ).
fof(f3560,plain,
( ~ m1_relset_1(k4_relat_1(u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0))
| ~ spl21_3
| spl21_92 ),
inference(superposition,[],[f1296,f3537]) ).
fof(f3562,plain,
( m2_relset_1(k4_relat_1(u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0))
| ~ m1_relset_1(u3_conlat_1(sK0),u1_conlat_1(sK0),u2_conlat_1(sK0))
| ~ spl21_3 ),
inference(superposition,[],[f165,f3537]) ).
fof(f3563,plain,
( m2_relset_1(k4_relat_1(u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0))
| ~ spl21_3 ),
inference(forward_subsumption_resolution,[],[f3562,f370]) ).
fof(f3576,plain,
( m1_relset_1(k4_relat_1(u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0))
| ~ spl21_3 ),
inference(resolution,[],[f3563,f231]) ).
fof(f3577,plain,
( $false
| ~ spl21_3
| spl21_92 ),
inference(forward_subsumption_resolution,[],[f3576,f3560]) ).
fof(f3578,plain,
( ~ spl21_3
| spl21_92 ),
inference(avatar_contradiction_clause,[],[f3577]) ).
fof(f3580,plain,
( ! [X2,X0,X1] :
( g2_conlat_1(X0,X1,X2) != k7_conlat_2(sK0)
| k4_relat_1(u3_conlat_1(sK0)) = X2 )
| ~ spl21_3
| ~ spl21_105 ),
inference(forward_demodulation,[],[f1356,f3537]) ).
fof(f3646,plain,
( ~ l2_conlat_1(k7_conlat_2(sK0))
| k7_conlat_2(sK0) = g2_conlat_1(u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)),u3_conlat_1(k7_conlat_2(sK0)))
| ~ spl21_106 ),
inference(resolution,[],[f1361,f152]) ).
fof(f3647,plain,
( k7_conlat_2(sK0) = g2_conlat_1(u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)),u3_conlat_1(k7_conlat_2(sK0)))
| ~ spl21_8
| ~ spl21_106 ),
inference(forward_subsumption_resolution,[],[f3646,f452]) ).
fof(f3692,plain,
( k7_conlat_2(sK0) != k7_conlat_2(sK0)
| u2_conlat_1(sK0) = u1_conlat_1(k7_conlat_2(sK0))
| ~ spl21_8
| ~ spl21_103
| ~ spl21_106 ),
inference(superposition,[],[f1348,f3647]) ).
fof(f3693,plain,
( k7_conlat_2(sK0) != k7_conlat_2(sK0)
| u1_conlat_1(sK0) = u2_conlat_1(k7_conlat_2(sK0))
| ~ spl21_8
| ~ spl21_104
| ~ spl21_106 ),
inference(superposition,[],[f1352,f3647]) ).
fof(f3705,plain,
( k7_conlat_2(sK0) != k7_conlat_2(sK0)
| u3_conlat_1(k7_conlat_2(sK0)) = k4_relat_1(u3_conlat_1(sK0))
| ~ spl21_3
| ~ spl21_8
| ~ spl21_105
| ~ spl21_106 ),
inference(superposition,[],[f3580,f3647]) ).
fof(f3706,plain,
( u3_conlat_1(k7_conlat_2(sK0)) = k4_relat_1(u3_conlat_1(sK0))
| ~ spl21_3
| ~ spl21_8
| ~ spl21_105
| ~ spl21_106 ),
inference(trivial_inequality_removal,[],[f3705]) ).
fof(f3707,plain,
( u1_conlat_1(sK0) = u2_conlat_1(k7_conlat_2(sK0))
| ~ spl21_8
| ~ spl21_104
| ~ spl21_106 ),
inference(trivial_inequality_removal,[],[f3693]) ).
fof(f3708,plain,
( u2_conlat_1(sK0) = u1_conlat_1(k7_conlat_2(sK0))
| ~ spl21_8
| ~ spl21_103
| ~ spl21_106 ),
inference(trivial_inequality_removal,[],[f3692]) ).
fof(f3712,plain,
( spl21_116
| ~ spl21_8
| ~ spl21_104
| ~ spl21_106 ),
inference(avatar_split_clause,[],[f3707,f1359,f1351,f451,f1425]) ).
fof(f3713,plain,
( spl21_118
| ~ spl21_8
| ~ spl21_103
| ~ spl21_106 ),
inference(avatar_split_clause,[],[f3708,f1359,f1347,f451,f1434]) ).
fof(f3753,plain,
( k7_conlat_2(k7_conlat_2(sK0)) = g2_conlat_1(u1_conlat_1(sK0),u1_conlat_1(k7_conlat_2(sK0)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0)),u1_conlat_1(sK0),u3_conlat_1(k7_conlat_2(sK0))))
| ~ spl21_8
| spl21_9
| ~ spl21_116 ),
inference(superposition,[],[f1117,f1427]) ).
fof(f3794,plain,
( k7_conlat_2(k7_conlat_2(sK0)) = g2_conlat_1(u1_conlat_1(sK0),u1_conlat_1(k7_conlat_2(sK0)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0)),u1_conlat_1(sK0),k4_relat_1(u3_conlat_1(sK0))))
| ~ spl21_3
| ~ spl21_8
| spl21_9
| ~ spl21_105
| ~ spl21_106
| ~ spl21_116 ),
inference(forward_demodulation,[],[f3753,f3706]) ).
fof(f3800,plain,
( k7_conlat_2(k7_conlat_2(sK0)) = g2_conlat_1(u1_conlat_1(sK0),u2_conlat_1(sK0),k6_relset_1(u2_conlat_1(sK0),u1_conlat_1(sK0),k4_relat_1(u3_conlat_1(sK0))))
| ~ spl21_3
| ~ spl21_8
| spl21_9
| ~ spl21_105
| ~ spl21_106
| ~ spl21_116
| ~ spl21_118 ),
inference(forward_demodulation,[],[f3794,f1436]) ).
fof(f4130,plain,
( k4_relat_1(k4_relat_1(u3_conlat_1(sK0))) = k6_relset_1(u2_conlat_1(sK0),u1_conlat_1(sK0),k4_relat_1(u3_conlat_1(sK0)))
| ~ spl21_3 ),
inference(resolution,[],[f3576,f228]) ).
fof(f4132,plain,
( u3_conlat_1(sK0) = k6_relset_1(u2_conlat_1(sK0),u1_conlat_1(sK0),k4_relat_1(u3_conlat_1(sK0)))
| ~ spl21_3 ),
inference(forward_demodulation,[],[f4130,f3541]) ).
fof(f4456,plain,
( g2_conlat_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = k7_conlat_2(k7_conlat_2(sK0))
| ~ spl21_3
| ~ spl21_8
| spl21_9
| ~ spl21_105
| ~ spl21_106
| ~ spl21_116
| ~ spl21_118 ),
inference(superposition,[],[f3800,f4132]) ).
fof(f4498,plain,
( sK0 = k7_conlat_2(k7_conlat_2(sK0))
| ~ spl21_3
| ~ spl21_8
| spl21_9
| ~ spl21_105
| ~ spl21_106
| ~ spl21_116
| ~ spl21_118 ),
inference(forward_demodulation,[],[f4456,f353]) ).
fof(f4501,plain,
( $false
| ~ spl21_3
| ~ spl21_8
| spl21_9
| ~ spl21_105
| ~ spl21_106
| ~ spl21_116
| spl21_117
| ~ spl21_118 ),
inference(forward_subsumption_resolution,[],[f4498,f1431]) ).
fof(f4502,plain,
( ~ spl21_3
| ~ spl21_8
| spl21_9
| ~ spl21_105
| ~ spl21_106
| ~ spl21_116
| spl21_117
| ~ spl21_118 ),
inference(avatar_contradiction_clause,[],[f4501]) ).
fof(f4602,plain,
( k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = g3_conlat_1(sK0,u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1))
| ~ spl21_10
| ~ spl21_11
| ~ spl21_14
| ~ spl21_15
| ~ spl21_117
| ~ spl21_245 ),
inference(superposition,[],[f3277,f1430]) ).
fof(f4629,plain,
( sK1 = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ spl21_10
| ~ spl21_11
| ~ spl21_14
| ~ spl21_15
| ~ spl21_34
| ~ spl21_117
| ~ spl21_245 ),
inference(forward_demodulation,[],[f4602,f641]) ).
fof(f4650,plain,
( $false
| ~ spl21_5
| ~ spl21_8
| spl21_9
| ~ spl21_10
| ~ spl21_11
| ~ spl21_14
| ~ spl21_15
| ~ spl21_34
| ~ spl21_117
| ~ spl21_245 ),
inference(forward_subsumption_resolution,[],[f4629,f3036]) ).
fof(f4651,plain,
( ~ spl21_5
| ~ spl21_8
| spl21_9
| ~ spl21_10
| ~ spl21_11
| ~ spl21_14
| ~ spl21_15
| ~ spl21_34
| ~ spl21_117
| ~ spl21_245 ),
inference(avatar_contradiction_clause,[],[f4650]) ).
cnf(s5,plain,
spl21_5,
inference(sat_conversion,[],[f420]) ).
cnf(s7,plain,
( ~ spl21_5
| ~ spl21_8
| spl21_9
| spl21_10 ),
inference(sat_conversion,[],[f462]) ).
cnf(s8,plain,
( ~ spl21_5
| ~ spl21_8
| spl21_9
| spl21_11 ),
inference(sat_conversion,[],[f467]) ).
cnf(s10,plain,
spl21_8,
inference(sat_conversion,[],[f481]) ).
cnf(s11,plain,
~ spl21_9,
inference(sat_conversion,[],[f485]) ).
cnf(s14,plain,
( ~ spl21_5
| ~ spl21_8
| spl21_9
| spl21_14 ),
inference(sat_conversion,[],[f517]) ).
cnf(s15,plain,
( ~ spl21_8
| spl21_9
| spl21_15 ),
inference(sat_conversion,[],[f524]) ).
cnf(s27,plain,
( spl21_34
| ~ spl21_35 ),
inference(sat_conversion,[],[f646]) ).
cnf(s28,plain,
spl21_35,
inference(sat_conversion,[],[f649]) ).
cnf(s85,plain,
( ~ spl21_92
| spl21_103 ),
inference(sat_conversion,[],[f1349]) ).
cnf(s86,plain,
( ~ spl21_92
| spl21_104 ),
inference(sat_conversion,[],[f1353]) ).
cnf(s87,plain,
( ~ spl21_92
| spl21_105 ),
inference(sat_conversion,[],[f1357]) ).
cnf(s88,plain,
( ~ spl21_92
| spl21_106 ),
inference(sat_conversion,[],[f1362]) ).
cnf(s194,plain,
( ~ spl21_5
| ~ spl21_8
| spl21_9
| spl21_245 ),
inference(sat_conversion,[],[f3271]) ).
cnf(s215,plain,
spl21_3,
inference(sat_conversion,[],[f3497]) ).
cnf(s235,plain,
( ~ spl21_3
| spl21_92 ),
inference(sat_conversion,[],[f3578]) ).
cnf(s245,plain,
( ~ spl21_8
| ~ spl21_104
| ~ spl21_106
| spl21_116 ),
inference(sat_conversion,[],[f3712]) ).
cnf(s246,plain,
( ~ spl21_8
| ~ spl21_103
| ~ spl21_106
| spl21_118 ),
inference(sat_conversion,[],[f3713]) ).
cnf(s327,plain,
( ~ spl21_3
| ~ spl21_8
| spl21_9
| ~ spl21_105
| ~ spl21_106
| ~ spl21_116
| spl21_117
| ~ spl21_118 ),
inference(sat_conversion,[],[f4502]) ).
cnf(s330,plain,
( ~ spl21_5
| ~ spl21_8
| spl21_9
| ~ spl21_10
| ~ spl21_11
| ~ spl21_14
| ~ spl21_15
| ~ spl21_34
| ~ spl21_117
| ~ spl21_245 ),
inference(sat_conversion,[],[f4651]) ).
cnf(s333,plain,
spl21_92,
inference(rat,[],[s235,s215]) ).
cnf(s335,plain,
spl21_106,
inference(rat,[],[s88,s333]) ).
cnf(s336,plain,
spl21_105,
inference(rat,[],[s87,s333]) ).
cnf(s337,plain,
spl21_104,
inference(rat,[],[s86,s333]) ).
cnf(s338,plain,
spl21_103,
inference(rat,[],[s85,s333]) ).
cnf(s352,plain,
spl21_34,
inference(rat,[],[s27,s28]) ).
cnf(s354,plain,
spl21_118,
inference(rat,[],[s246,s338,s335,s10]) ).
cnf(s355,plain,
spl21_116,
inference(rat,[],[s245,s337,s335,s10]) ).
cnf(s358,plain,
spl21_15,
inference(rat,[],[s15,s11,s10]) ).
cnf(s360,plain,
spl21_117,
inference(rat,[],[s327,s354,s10,s11,s335,s336,s215,s355]) ).
cnf(s394,plain,
( ~ spl21_5
| spl21_11 ),
inference(rat,[],[s8,s11,s10]) ).
cnf(s395,plain,
( ~ spl21_5
| spl21_10 ),
inference(rat,[],[s7,s11,s10]) ).
cnf(s396,plain,
spl21_245,
inference(rat,[],[s194,s10,s11,s5]) ).
cnf(s398,plain,
spl21_14,
inference(rat,[],[s14,s10,s11,s5]) ).
cnf(s399,plain,
spl21_11,
inference(rat,[],[s394,s5]) ).
cnf(s400,plain,
spl21_10,
inference(rat,[],[s395,s5]) ).
cnf(s404,plain,
$false,
inference(rat,[],[s330,s396,s360,s352,s358,s398,s5,s10,s11,s399,s400]) ).
fof(f4665,plain,
$false,
inference(avatar_sat_refutation,[],[s404]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT345+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n008.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 14:52:25 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.47/4.31 % (1304569)Will run a generic schedule for satisfiability detection.
% 27.47/4.31 % (1304575)% WARNING: option uhcvi not known.
% 27.47/4.31 % (1304575)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=35600411:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 27.47/4.31 % (1304577)dis+10_1_sil=32000:sp=arity:random_seed=3213642258:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 27.47/4.31 % (1304574)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=800981626_2999 on theBenchmark for (2999ds/0Mi)
% 27.47/4.31 % (1304576)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3106295331:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 27.47/4.31 % (1304579)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2537452747:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 27.47/4.31 % (1304578)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1459061233:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 27.47/4.31 % (1304580)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3119427825:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 27.47/4.31 % TRYING [1]
% 27.47/4.31 % TRYING [2]
% 27.47/4.31 % TRYING [3]
% 27.47/4.31 % TRYING [4]
% 27.47/4.31 % (1304577)Instruction limit reached!
% 27.47/4.31 % (1304577)------------------------------
% 27.47/4.31 % (1304577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.47/4.31 % (1304577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.47/4.31 % (1304577)CaDiCaL version: 2.1.3
% 27.47/4.31 % (1304577)Termination reason: Instruction limit
% 27.47/4.31 % (1304577)Termination phase: Saturation
% 27.47/4.31 % (1304577)Time elapsed: 0.068 s
% 27.47/4.31 % (1304577)Peak memory usage: 13 MB
% 27.47/4.31 % (1304577)Instructions burned: 104 (million)
% 27.47/4.31 % TRYING [5]
% 27.47/4.31 % (1304578)Instruction limit reached!
% 27.47/4.31 % (1304578)------------------------------
% 27.47/4.31 % (1304578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.47/4.31 % (1304578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.47/4.31 % (1304578)CaDiCaL version: 2.1.3
% 27.47/4.31 % (1304578)Termination reason: Instruction limit
% 27.47/4.31 % (1304578)Termination phase: Saturation
% 27.47/4.31 % (1304578)Time elapsed: 0.070 s
% 27.47/4.31 % (1304578)Peak memory usage: 13 MB
% 27.47/4.31 % (1304578)Instructions burned: 117 (million)
% 27.47/4.31 % (1304579)Instruction limit reached!
% 27.47/4.31 % (1304579)------------------------------
% 27.47/4.31 % (1304579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.47/4.31 % (1304579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.47/4.31 % (1304579)CaDiCaL version: 2.1.3
% 27.47/4.31 % (1304579)Termination reason: Instruction limit
% 27.47/4.31 % (1304579)Termination phase: Saturation
% 27.47/4.31 % (1304579)Time elapsed: 0.080 s
% 27.47/4.31 % (1304579)Peak memory usage: 13 MB
% 27.47/4.31 % (1304579)Instructions burned: 131 (million)
% 27.47/4.31 % (1304580)Instruction limit reached!
% 27.47/4.31 % (1304580)------------------------------
% 27.47/4.31 % (1304580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.47/4.31 % (1304580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.47/4.31 % (1304580)CaDiCaL version: 2.1.3
% 27.47/4.31 % (1304580)Termination reason: Instruction limit
% 27.47/4.31 % (1304580)Termination phase: Saturation
% 27.47/4.31 % (1304580)Time elapsed: 0.085 s
% 27.47/4.31 % (1304580)Peak memory usage: 12 MB
% 27.47/4.31 % (1304580)Instructions burned: 160 (million)
% 27.47/4.31 % (1304588)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=487684953:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 27.47/4.31 % (1304589)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=422758728:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 27.47/4.31 % TRYING [1]
% 27.47/4.31 % TRYING [2]
% 27.47/4.31 % TRYING [3]
% 27.47/4.31 % (1304590)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=786858258:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 27.47/4.31 % (1304591)ott-21_1_sil=16000:fs=off:random_seed=3729692572:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 27.47/4.31 % TRYING [4]
% 27.47/4.31 % (1304589)Instruction limit reached!
% 27.47/4.31 % (1304589)------------------------------
% 27.47/4.31 % (1304589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.95 % (1304589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.95 % (1304589)CaDiCaL version: 2.1.3
% 11.64/4.95 % (1304589)Termination reason: Instruction limit
% 11.64/4.95 % (1304589)Termination phase: Saturation
% 11.64/4.95 % (1304589)Time elapsed: 0.081 s
% 11.64/4.95 % (1304589)Peak memory usage: 13 MB
% 11.64/4.95 % (1304589)Instructions burned: 132 (million)
% 11.64/4.95 % (1304596)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3114963917:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 11.64/4.95 % (1304591)Instruction limit reached!
% 11.64/4.95 % (1304591)------------------------------
% 11.64/4.95 % (1304591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.95 % (1304591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.95 % (1304591)CaDiCaL version: 2.1.3
% 11.64/4.95 % (1304591)Termination reason: Instruction limit
% 11.64/4.95 % (1304591)Termination phase: Saturation
% 11.64/4.95 % (1304591)Time elapsed: 0.097 s
% 11.64/4.95 % (1304591)Peak memory usage: 13 MB
% 11.64/4.95 % (1304591)Instructions burned: 181 (million)
% 11.64/4.95 % (1304598)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4101167814:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 11.64/4.95 % TRYING [1]
% 11.64/4.95 % TRYING [2]
% 11.64/4.95 % TRYING [3]
% 11.64/4.95 % TRYING [4]
% 11.64/4.95 % TRYING [6]
% 11.64/4.95 % TRYING [5]
% 11.64/4.95 % (1304588)Instruction limit reached!
% 11.64/4.95 % (1304588)------------------------------
% 11.64/4.95 % (1304588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.95 % (1304588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.95 % (1304588)CaDiCaL version: 2.1.3
% 11.64/4.95 % (1304588)Termination reason: Instruction limit
% 11.64/4.95 % (1304588)Termination phase: Finite model building SAT solving
% 11.64/4.95 % (1304588)Time elapsed: 0.292 s
% 11.64/4.95 % (1304588)Peak memory usage: 29 MB
% 11.64/4.95 % (1304588)Instructions burned: 716 (million)
% 11.64/4.95 % (1304600)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2666138027:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 11.64/4.95 % (1304596)Instruction limit reached!
% 11.64/4.95 % (1304596)------------------------------
% 11.64/4.95 % (1304596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.95 % (1304596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.95 % (1304596)CaDiCaL version: 2.1.3
% 11.64/4.95 % (1304596)Termination reason: Instruction limit
% 11.64/4.95 % (1304596)Termination phase: Saturation
% 11.64/4.95 % (1304596)Time elapsed: 0.307 s
% 11.64/4.95 % (1304596)Peak memory usage: 14 MB
% 11.64/4.95 % (1304596)Instructions burned: 478 (million)
% 11.64/4.95 % (1304590)Instruction limit reached!
% 11.64/4.95 % (1304590)------------------------------
% 11.64/4.95 % (1304590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.95 % (1304590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.95 % (1304590)CaDiCaL version: 2.1.3
% 11.64/4.95 % (1304590)Termination reason: Instruction limit
% 11.64/4.95 % (1304590)Termination phase: Saturation
% 11.64/4.95 % (1304590)Time elapsed: 0.405 s
% 11.64/4.95 % (1304590)Peak memory usage: 19 MB
% 11.64/4.95 % (1304590)Instructions burned: 684 (million)
% 11.64/4.95 % (1304602)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1864155506:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 11.64/4.95 % (1304603)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1038828210:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 11.64/4.96 % (1304598)Instruction limit reached!
% 11.64/4.96 % (1304598)------------------------------
% 11.64/4.96 % (1304598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.96 % (1304598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.96 % (1304598)CaDiCaL version: 2.1.3
% 11.64/4.96 % (1304598)Termination reason: Instruction limit
% 11.64/4.96 % (1304598)Termination phase: Finite model building SAT solving
% 11.64/4.96 % (1304598)Time elapsed: 0.325 s
% 11.64/4.96 % (1304598)Peak memory usage: 19 MB
% 11.64/4.96 % (1304598)Instructions burned: 868 (million)
% 11.64/4.96 % (1304606)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=700290280:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 11.64/4.96 % TRYING [14]
% 11.64/4.96 % (1304603)Instruction limit reached!
% 11.64/4.96 % (1304603)------------------------------
% 11.64/4.96 % (1304603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.96 % (1304603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.96 % (1304603)CaDiCaL version: 2.1.3
% 11.64/4.96 % (1304603)Termination reason: Instruction limit
% 11.64/4.96 % (1304603)Termination phase: Saturation
% 11.64/4.96 % (1304603)Time elapsed: 0.316 s
% 11.64/4.96 % (1304603)Peak memory usage: 16 MB
% 11.64/4.96 % (1304603)Instructions burned: 692 (million)
% 11.64/4.96 % (1304602)Instruction limit reached!
% 11.64/4.96 % (1304602)------------------------------
% 11.64/4.96 % (1304602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.96 % (1304602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.96 % (1304602)CaDiCaL version: 2.1.3
% 11.64/4.96 % (1304602)Termination reason: Instruction limit
% 11.64/4.96 % (1304602)Termination phase: Finite model building constraint generation
% 11.64/4.96 % (1304602)Time elapsed: 0.328 s
% 11.64/4.96 % (1304602)Peak memory usage: 78 MB
% 11.64/4.96 % (1304602)Instructions burned: 892 (million)
% 11.64/4.96 % (1304608)fmb+10_1_sil=64000:random_seed=257410791:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 11.64/4.96 % TRYING [1]
% 11.64/4.96 % TRYING [2]
% 11.64/4.96 % (1304609)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=550120104:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 11.64/4.96 % TRYING [3]
% 11.64/4.96 % TRYING [20]
% 11.64/4.96 % TRYING [4]
% 11.64/4.96 % (1304600)Instruction limit reached!
% 11.64/4.96 % (1304600)------------------------------
% 11.64/4.96 % (1304600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.96 % (1304600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.96 % (1304600)CaDiCaL version: 2.1.3
% 11.64/4.96 % (1304600)Termination reason: Instruction limit
% 11.64/4.96 % (1304600)Termination phase: Saturation
% 11.64/4.96 % (1304600)Time elapsed: 0.636 s
% 11.64/4.96 % (1304600)Peak memory usage: 25 MB
% 11.64/4.96 % (1304600)Instructions burned: 1180 (million)
% 11.64/4.96 % (1304612)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2585717972:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 11.64/4.96 % (1304606)Instruction limit reached!
% 11.64/4.96 % (1304606)------------------------------
% 11.64/4.96 % (1304606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.96 % (1304606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.96 % (1304606)CaDiCaL version: 2.1.3
% 11.64/4.96 % (1304606)Termination reason: Instruction limit
% 11.64/4.96 % (1304606)Termination phase: Saturation
% 11.64/4.96 % (1304606)Time elapsed: 0.496 s
% 11.64/4.96 % (1304606)Peak memory usage: 19 MB
% 11.64/4.96 % (1304606)Instructions burned: 879 (million)
% 11.64/4.96 % TRYING [8]
% 11.64/4.96 % (1304614)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=24807094:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 11.64/4.96 % TRYING [5]
% 11.64/4.96 % (1304612)Instruction limit reached!
% 11.64/4.96 % (1304612)------------------------------
% 11.64/4.96 % (1304612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.96 % (1304612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.96 % (1304612)CaDiCaL version: 2.1.3
% 11.64/4.96 % (1304612)Termination reason: Instruction limit
% 11.64/4.96 % (1304612)Termination phase: Finite model building SAT solving
% 11.64/4.96 % (1304612)Time elapsed: 0.362 s
% 11.64/4.96 % (1304612)Peak memory usage: 64 MB
% 11.64/4.96 % (1304612)Instructions burned: 921 (million)
% 11.64/4.96 % (1304616)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2992381631:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 11.64/4.96 % (1304616)Instruction limit reached!
% 11.64/4.96 % (1304616)------------------------------
% 11.64/4.96 % (1304616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.96 % (1304616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.96 % (1304616)CaDiCaL version: 2.1.3
% 11.64/4.96 % (1304616)Termination reason: Instruction limit
% 11.64/4.96 % (1304616)Termination phase: Saturation
% 11.64/4.96 % (1304616)Time elapsed: 0.636 s
% 11.64/4.96 % (1304616)Peak memory usage: 21 MB
% 11.64/4.96 % (1304616)Instructions burned: 1473 (million)
% 11.64/4.96 % (1304618)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2916697855:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 11.64/4.96 % TRYING [77]
% 11.64/4.96 % TRYING [7]
% 11.64/4.96 % (1304614)Instruction limit reached!
% 11.64/4.96 % (1304614)------------------------------
% 11.64/4.96 % (1304614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.96 % (1304614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.96 % (1304614)CaDiCaL version: 2.1.3
% 11.64/4.96 % (1304614)Termination reason: Instruction limit
% 11.64/4.96 % (1304614)Termination phase: Saturation
% 11.64/4.96 % (1304614)Time elapsed: 2.775 s
% 11.64/4.96 % (1304614)Peak memory usage: 32 MB
% 11.64/4.96 % (1304614)Instructions burned: 5132 (million)
% 11.64/4.96 % (1304620)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1444811774:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 11.64/4.96 % TRYING [16]
% 11.64/4.96 % (1304609)Instruction limit reached!
% 11.64/4.96 % (1304609)------------------------------
% 11.64/4.96 % (1304609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.96 % (1304609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.96 % (1304609)CaDiCaL version: 2.1.3
% 11.64/4.96 % (1304609)Termination reason: Instruction limit
% 11.64/4.96 % (1304609)Termination phase: Finite model building constraint generation
% 11.64/4.96 % (1304609)Time elapsed: 3.356 s
% 11.64/4.96 % (1304609)Peak memory usage: 589 MB
% 11.64/4.96 % (1304609)Instructions burned: 9518 (million)
% 11.64/4.96 % (1304622)ott-2_1_sil=16000:newcnf=on:random_seed=471829149:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2956 on theBenchmark for (2956ds/869Mi)
% 11.64/4.96 % (1304622) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1304569-1304622"...
% 11.64/4.96 % (1304618)Instruction limit reached!
% 11.64/4.96 % (1304618)------------------------------
% 11.64/4.96 % (1304618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.96 % (1304618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.96 % (1304618)CaDiCaL version: 2.1.3
% 11.64/4.96 % (1304618)Termination reason: Instruction limit
% 11.64/4.96 % (1304618)Termination phase: Finite model building constraint generation
% 11.64/4.96 % (1304618)Time elapsed: 2.333 s
% 11.64/4.96 % (1304618)Peak memory usage: 516 MB
% 11.64/4.96 % (1304618)Instructions burned: 6326 (million)
% 11.64/4.96 % (1304622)...printing done.
% 11.64/4.96 % (1304622)Refutation found. Thanks to Tanya!
% 11.64/4.96 % SZS status Theorem for theBenchmark
% 11.64/4.96 % SZS output start Proof for theBenchmark
% See solution above
% 11.64/4.96 % (1304622)------------------------------
% 11.64/4.96 % (1304622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/4.96 % (1304622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/4.96 % (1304622)CaDiCaL version: 2.1.3
% 11.64/4.96 % (1304622)Termination reason: Refutation
% 11.64/4.96 % (1304622)Time elapsed: 0.114 s
% 11.64/4.96 % (1304622)Peak memory usage: 14 MB
% 11.64/4.96 % (1304622)Instructions burned: 178 (million)
% 11.64/4.96 % (1304569)Success in time 4.532 s
% 11.64/4.96 % Vampire exiting
%------------------------------------------------------------------------------