%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP038+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:34:01 PM UTC 2026
% Result : Theorem 112.16s 16.86s
% Output : Refutation 114.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 24
% Syntax : Number of formulae : 208 ( 34 unt; 11 def)
% Number of atoms : 863 ( 17 equ)
% Maximal formula atoms : 11 ( 4 avg)
% Number of connectives : 1214 ( 559 ~; 564 |; 58 &)
% ( 14 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 11 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-4 aty)
% Number of variables : 146 ( 0 sgn 138 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f433,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_subset_1) ).
fof(f446,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f631,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> k9_relat_1(X2,k2_xboole_0(X0,X1)) = k2_xboole_0(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t153_relat_1) ).
fof(f1026,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(f1085,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(f1087,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(f2245,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f2251,axiom,
! [X0,X1,X2,X3] :
( ( l1_struct_0(X0)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_pre_topc) ).
fof(f2252,axiom,
! [X0,X1,X2,X3] :
( ( l1_struct_0(X0)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_pre_topc) ).
fof(f3565,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> l1_pre_topc(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_tsp_1) ).
fof(f3567,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
fof(f3575,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m1_pre_topc(X1,X0) )
=> ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_tsp_2) ).
fof(f3636,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_subset_1(u1_struct_0(X0),X2,X3)) = k4_subset_1(u1_struct_0(X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X3)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t31_tsp_2) ).
fof(f3637,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_subset_1(u1_struct_0(X0),X2,X3)) = k4_subset_1(u1_struct_0(X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X3)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f3636]) ).
fof(f4108,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f433]) ).
fof(f4109,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f4108]) ).
fof(f4318,plain,
! [X0,X1,X2] :
( k9_relat_1(X2,k2_xboole_0(X0,X1)) = k2_xboole_0(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f631]) ).
fof(f4731,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1026]) ).
fof(f4789,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,[],[f1085]) ).
fof(f6199,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f2245]) ).
fof(f6206,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f2251]) ).
fof(f6207,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f6206]) ).
fof(f6208,plain,
! [X0,X1,X2,X3] :
( k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f2252]) ).
fof(f6209,plain,
! [X0,X1,X2,X3] :
( k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f6208]) ).
fof(f8443,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3565]) ).
fof(f8445,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3567]) ).
fof(f8460,plain,
! [X0,X1] :
( ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(ennf_transformation,[],[f3575]) ).
fof(f8461,plain,
! [X0,X1] :
( ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(flattening,[],[f8460]) ).
fof(f8582,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_subset_1(u1_struct_0(X0),X2,X3)) != k4_subset_1(u1_struct_0(X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X3))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3637]) ).
fof(f8583,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_subset_1(u1_struct_0(X0),X2,X3)) != k4_subset_1(u1_struct_0(X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X3))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f8582]) ).
fof(f9123,plain,
! [X0,X1] :
( ( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) )
& ( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ) ),
inference(nnf_transformation,[],[f446]) ).
fof(f9418,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,[],[f1087]) ).
fof(f11106,plain,
! [X0] :
( ! [X1] :
( ( m2_tsp_1(X1,X0)
| ~ m1_pre_topc(X1,X0) )
& ( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0) ) )
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f8445]) ).
fof(f11167,plain,
( k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),k4_subset_1(u1_struct_0(sK1387),sK1389,sK1390)) != k4_subset_1(u1_struct_0(sK1388),k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1389),k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390))
& m1_subset_1(sK1390,k1_zfmisc_1(u1_struct_0(sK1387)))
& m1_subset_1(sK1389,k1_zfmisc_1(u1_struct_0(sK1387)))
& ~ v3_struct_0(sK1388)
& v2_tsp_2(sK1388,sK1387)
& m2_tsp_1(sK1388,sK1387)
& ~ v3_struct_0(sK1387)
& v2_pre_topc(sK1387)
& l1_pre_topc(sK1387) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1387,sK1388,sK1389,sK1390]),skolemize(X0,sK1387),skolemize(X1,sK1388),skolemize(X2,sK1389),skolemize(X3,sK1390)],[f8583]) ).
fof(f11782,plain,
! [X2,X0,X1] :
( k2_xboole_0(X1,X2) = k4_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f4109]) ).
fof(f11795,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f9123]) ).
fof(f11796,plain,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f9123]) ).
fof(f12035,plain,
! [X2,X0,X1] :
( k9_relat_1(X2,k2_xboole_0(X0,X1)) = k2_xboole_0(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f4318]) ).
fof(f12673,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f4731]) ).
fof(f12753,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,[],[f4789]) ).
fof(f12755,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f9418]) ).
fof(f15298,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f6199]) ).
fof(f15305,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f6207]) ).
fof(f15306,plain,
! [X2,X3,X0,X1] :
( k9_relat_1(X2,X3) = k4_pre_topc(X0,X1,X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f6209]) ).
fof(f19070,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f8443]) ).
fof(f19072,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f11106]) ).
fof(f19092,plain,
! [X0,X1] :
( m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f8461]) ).
fof(f19094,plain,
! [X0,X1] :
( v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f8461]) ).
fof(f19095,plain,
! [X0,X1] :
( v1_funct_1(k4_tsp_2(X0,X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f8461]) ).
fof(f19261,plain,
l1_pre_topc(sK1387),
inference(cnf_transformation,[],[f11167]) ).
fof(f19262,plain,
v2_pre_topc(sK1387),
inference(cnf_transformation,[],[f11167]) ).
fof(f19263,plain,
~ v3_struct_0(sK1387),
inference(cnf_transformation,[],[f11167]) ).
fof(f19264,plain,
m2_tsp_1(sK1388,sK1387),
inference(cnf_transformation,[],[f11167]) ).
fof(f19265,plain,
v2_tsp_2(sK1388,sK1387),
inference(cnf_transformation,[],[f11167]) ).
fof(f19266,plain,
~ v3_struct_0(sK1388),
inference(cnf_transformation,[],[f11167]) ).
fof(f19267,plain,
m1_subset_1(sK1389,k1_zfmisc_1(u1_struct_0(sK1387))),
inference(cnf_transformation,[],[f11167]) ).
fof(f19268,plain,
m1_subset_1(sK1390,k1_zfmisc_1(u1_struct_0(sK1387))),
inference(cnf_transformation,[],[f11167]) ).
fof(f19269,plain,
k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),k4_subset_1(u1_struct_0(sK1387),sK1389,sK1390)) != k4_subset_1(u1_struct_0(sK1388),k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1389),k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390)),
inference(cnf_transformation,[],[f11167]) ).
fof(f19286,definition,
~ sP1399(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),k4_subset_1(u1_struct_0(sK1387),sK1389,sK1390))),
introduced(definition,[new_symbols(definition,[sP1399])],[inequality_splitting_name_introduction]) ).
fof(f19287,plain,
sP1399(k4_subset_1(u1_struct_0(sK1388),k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1389),k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390))),
inference(inequality_splitting,[],[f19269,f19286]) ).
fof(f22694,plain,
( ~ sP1399(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),k2_xboole_0(sK1389,sK1390)))
| ~ m1_subset_1(sK1389,k1_zfmisc_1(u1_struct_0(sK1387)))
| ~ m1_subset_1(sK1390,k1_zfmisc_1(u1_struct_0(sK1387))) ),
inference(superposition,[],[f19286,f11782]) ).
fof(f22699,definition,
( spl1400_389
<=> m1_subset_1(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390),k1_zfmisc_1(u1_struct_0(sK1388))) ),
introduced(definition,[new_symbols(definition,[spl1400_389])],[avatar_definition]) ).
fof(f22700,plain,
( m1_subset_1(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390),k1_zfmisc_1(u1_struct_0(sK1388)))
| ~ spl1400_389 ),
inference(avatar_component_clause,[],[f22699]) ).
fof(f22701,plain,
( ~ m1_subset_1(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390),k1_zfmisc_1(u1_struct_0(sK1388)))
| spl1400_389 ),
inference(avatar_component_clause,[],[f22699]) ).
fof(f22703,definition,
( spl1400_390
<=> m1_subset_1(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1389),k1_zfmisc_1(u1_struct_0(sK1388))) ),
introduced(definition,[new_symbols(definition,[spl1400_390])],[avatar_definition]) ).
fof(f22704,plain,
( m1_subset_1(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1389),k1_zfmisc_1(u1_struct_0(sK1388)))
| ~ spl1400_390 ),
inference(avatar_component_clause,[],[f22703]) ).
fof(f22705,plain,
( ~ m1_subset_1(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1389),k1_zfmisc_1(u1_struct_0(sK1388)))
| spl1400_390 ),
inference(avatar_component_clause,[],[f22703]) ).
fof(f22711,plain,
( ~ sP1399(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),k2_xboole_0(sK1389,sK1390)))
| ~ m1_subset_1(sK1390,k1_zfmisc_1(u1_struct_0(sK1387))) ),
inference(forward_subsumption_resolution,[],[f22694,f19267]) ).
fof(f22712,plain,
~ sP1399(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),k2_xboole_0(sK1389,sK1390))),
inference(forward_subsumption_resolution,[],[f22711,f19268]) ).
fof(f22713,plain,
( ~ l1_struct_0(sK1387)
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| spl1400_389 ),
inference(resolution,[],[f22701,f15305]) ).
fof(f22715,definition,
( spl1400_392
<=> m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388)) ),
introduced(definition,[new_symbols(definition,[spl1400_392])],[avatar_definition]) ).
fof(f22716,plain,
( m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_392 ),
inference(avatar_component_clause,[],[f22715]) ).
fof(f22717,plain,
( ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| spl1400_392 ),
inference(avatar_component_clause,[],[f22715]) ).
fof(f22719,definition,
( spl1400_393
<=> v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388)) ),
introduced(definition,[new_symbols(definition,[spl1400_393])],[avatar_definition]) ).
fof(f22720,plain,
( v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_393 ),
inference(avatar_component_clause,[],[f22719]) ).
fof(f22721,plain,
( ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| spl1400_393 ),
inference(avatar_component_clause,[],[f22719]) ).
fof(f22723,definition,
( spl1400_394
<=> v1_funct_1(k4_tsp_2(sK1387,sK1388)) ),
introduced(definition,[new_symbols(definition,[spl1400_394])],[avatar_definition]) ).
fof(f22724,plain,
( v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ spl1400_394 ),
inference(avatar_component_clause,[],[f22723]) ).
fof(f22725,plain,
( ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| spl1400_394 ),
inference(avatar_component_clause,[],[f22723]) ).
fof(f22727,definition,
( spl1400_395
<=> l1_struct_0(sK1388) ),
introduced(definition,[new_symbols(definition,[spl1400_395])],[avatar_definition]) ).
fof(f22728,plain,
( l1_struct_0(sK1388)
| ~ spl1400_395 ),
inference(avatar_component_clause,[],[f22727]) ).
fof(f22731,definition,
( spl1400_396
<=> l1_struct_0(sK1387) ),
introduced(definition,[new_symbols(definition,[spl1400_396])],[avatar_definition]) ).
fof(f22732,plain,
( l1_struct_0(sK1387)
| ~ spl1400_396 ),
inference(avatar_component_clause,[],[f22731]) ).
fof(f22734,plain,
( ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| spl1400_389 ),
inference(avatar_split_clause,[],[f22713,f22699,f22731,f22727,f22723,f22719,f22715]) ).
fof(f22749,plain,
( l1_pre_topc(sK1388)
| ~ l1_pre_topc(sK1387) ),
inference(resolution,[],[f19070,f19264]) ).
fof(f22750,plain,
l1_pre_topc(sK1388),
inference(forward_subsumption_resolution,[],[f22749,f19261]) ).
fof(f22758,plain,
( ~ sP1399(k9_relat_1(k4_tsp_2(sK1387,sK1388),k2_xboole_0(sK1389,sK1390)))
| ~ l1_struct_0(sK1387)
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388)) ),
inference(superposition,[],[f22712,f15306]) ).
fof(f22760,plain,
( sP1399(k4_subset_1(u1_struct_0(sK1388),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ l1_struct_0(sK1387)
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388)) ),
inference(superposition,[],[f19287,f15306]) ).
fof(f22763,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k9_relat_1(X0,X1),k1_zfmisc_1(u1_struct_0(X3)))
| ~ l1_struct_0(X2)
| ~ l1_struct_0(X3)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X2),u1_struct_0(X3))
| ~ m1_relset_1(X0,u1_struct_0(X2),u1_struct_0(X3))
| ~ l1_struct_0(X2)
| ~ l1_struct_0(X3)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X2),u1_struct_0(X3))
| ~ m1_relset_1(X0,u1_struct_0(X2),u1_struct_0(X3)) ),
inference(superposition,[],[f15305,f15306]) ).
fof(f22767,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k9_relat_1(X0,X1),k1_zfmisc_1(u1_struct_0(X3)))
| ~ l1_struct_0(X2)
| ~ l1_struct_0(X3)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X2),u1_struct_0(X3))
| ~ m1_relset_1(X0,u1_struct_0(X2),u1_struct_0(X3)) ),
inference(duplicate_literal_removal,[],[f22763]) ).
fof(f22770,plain,
( m1_pre_topc(sK1388,sK1387)
| ~ l1_pre_topc(sK1387) ),
inference(resolution,[],[f19072,f19264]) ).
fof(f22771,plain,
m1_pre_topc(sK1388,sK1387),
inference(forward_subsumption_resolution,[],[f22770,f19261]) ).
fof(f22772,plain,
l1_struct_0(sK1387),
inference(resolution,[],[f15298,f19261]) ).
fof(f22773,plain,
l1_struct_0(sK1388),
inference(resolution,[],[f15298,f22750]) ).
fof(f22774,plain,
spl1400_395,
inference(avatar_split_clause,[],[f22773,f22727]) ).
fof(f22775,plain,
spl1400_396,
inference(avatar_split_clause,[],[f22772,f22731]) ).
fof(f22960,plain,
! [X0,X1] :
( m1_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(resolution,[],[f12755,f19092]) ).
fof(f23140,plain,
( v3_struct_0(sK1387)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_392 ),
inference(resolution,[],[f22960,f22717]) ).
fof(f23141,plain,
( ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_392 ),
inference(forward_subsumption_resolution,[],[f23140,f19263]) ).
fof(f23142,plain,
( ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_392 ),
inference(forward_subsumption_resolution,[],[f23141,f19262]) ).
fof(f23143,plain,
( v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_392 ),
inference(forward_subsumption_resolution,[],[f23142,f19261]) ).
fof(f23144,plain,
( ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_392 ),
inference(forward_subsumption_resolution,[],[f23143,f19266]) ).
fof(f23145,plain,
( ~ m1_pre_topc(sK1388,sK1387)
| spl1400_392 ),
inference(forward_subsumption_resolution,[],[f23144,f19265]) ).
fof(f23146,plain,
( $false
| spl1400_392 ),
inference(forward_subsumption_resolution,[],[f23145,f22771]) ).
fof(f23147,plain,
spl1400_392,
inference(avatar_contradiction_clause,[],[f23146]) ).
fof(f23148,plain,
( v3_struct_0(sK1387)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_393 ),
inference(resolution,[],[f22721,f19094]) ).
fof(f23149,plain,
( ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_393 ),
inference(forward_subsumption_resolution,[],[f23148,f19263]) ).
fof(f23150,plain,
( ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_393 ),
inference(forward_subsumption_resolution,[],[f23149,f19262]) ).
fof(f23151,plain,
( v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_393 ),
inference(forward_subsumption_resolution,[],[f23150,f19261]) ).
fof(f23152,plain,
( ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_393 ),
inference(forward_subsumption_resolution,[],[f23151,f19266]) ).
fof(f23153,plain,
( ~ m1_pre_topc(sK1388,sK1387)
| spl1400_393 ),
inference(forward_subsumption_resolution,[],[f23152,f19265]) ).
fof(f23154,plain,
( $false
| spl1400_393 ),
inference(forward_subsumption_resolution,[],[f23153,f22771]) ).
fof(f23155,plain,
spl1400_393,
inference(avatar_contradiction_clause,[],[f23154]) ).
fof(f23157,plain,
( v3_struct_0(sK1387)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_394 ),
inference(resolution,[],[f22725,f19095]) ).
fof(f23158,plain,
( ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_394 ),
inference(forward_subsumption_resolution,[],[f23157,f19263]) ).
fof(f23159,plain,
( ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_394 ),
inference(forward_subsumption_resolution,[],[f23158,f19262]) ).
fof(f23160,plain,
( v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_394 ),
inference(forward_subsumption_resolution,[],[f23159,f19261]) ).
fof(f23161,plain,
( ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_394 ),
inference(forward_subsumption_resolution,[],[f23160,f19266]) ).
fof(f23162,plain,
( ~ m1_pre_topc(sK1388,sK1387)
| spl1400_394 ),
inference(forward_subsumption_resolution,[],[f23161,f19265]) ).
fof(f23163,plain,
( $false
| spl1400_394 ),
inference(forward_subsumption_resolution,[],[f23162,f22771]) ).
fof(f23164,plain,
spl1400_394,
inference(avatar_contradiction_clause,[],[f23163]) ).
fof(f23166,plain,
( sP1399(k4_subset_1(u1_struct_0(sK1388),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f22760,f22732]) ).
fof(f23168,plain,
( ~ sP1399(k9_relat_1(k4_tsp_2(sK1387,sK1388),k2_xboole_0(sK1389,sK1390)))
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f22758,f22732]) ).
fof(f23171,plain,
( sP1399(k4_subset_1(u1_struct_0(sK1388),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23166,f22728]) ).
fof(f23173,plain,
( ~ sP1399(k9_relat_1(k4_tsp_2(sK1387,sK1388),k2_xboole_0(sK1389,sK1390)))
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23168,f22728]) ).
fof(f23176,plain,
( sP1399(k4_subset_1(u1_struct_0(sK1388),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23171,f22724]) ).
fof(f23178,plain,
( ~ sP1399(k9_relat_1(k4_tsp_2(sK1387,sK1388),k2_xboole_0(sK1389,sK1390)))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23173,f22724]) ).
fof(f23181,plain,
( sP1399(k4_subset_1(u1_struct_0(sK1388),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23176,f22720]) ).
fof(f23183,plain,
( ~ sP1399(k9_relat_1(k4_tsp_2(sK1387,sK1388),k2_xboole_0(sK1389,sK1390)))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23178,f22720]) ).
fof(f23186,plain,
( sP1399(k4_subset_1(u1_struct_0(sK1388),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23181,f22716]) ).
fof(f23188,plain,
( ~ sP1399(k9_relat_1(k4_tsp_2(sK1387,sK1388),k2_xboole_0(sK1389,sK1390)))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23183,f22716]) ).
fof(f23193,definition,
( spl1400_401
<=> m2_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388)) ),
introduced(definition,[new_symbols(definition,[spl1400_401])],[avatar_definition]) ).
fof(f23194,plain,
( m2_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_401 ),
inference(avatar_component_clause,[],[f23193]) ).
fof(f23195,plain,
( ~ m2_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| spl1400_401 ),
inference(avatar_component_clause,[],[f23193]) ).
fof(f23211,plain,
( ~ m1_subset_1(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k1_zfmisc_1(u1_struct_0(sK1388)))
| ~ l1_struct_0(sK1387)
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| spl1400_390 ),
inference(superposition,[],[f22705,f15306]) ).
fof(f23212,plain,
( ~ l1_struct_0(sK1387)
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| spl1400_390 ),
inference(forward_subsumption_resolution,[],[f23211,f22767]) ).
fof(f23214,plain,
( ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| spl1400_390
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23212,f22732]) ).
fof(f23216,plain,
( ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| spl1400_390
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23214,f22728]) ).
fof(f23218,plain,
( ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| spl1400_390
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23216,f22724]) ).
fof(f23220,plain,
( ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| spl1400_390
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23218,f22720]) ).
fof(f23223,plain,
( $false
| spl1400_390
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23220,f22716]) ).
fof(f23224,plain,
( spl1400_390
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(avatar_contradiction_clause,[],[f23223]) ).
fof(f23233,plain,
( r1_tarski(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1390),u1_struct_0(sK1388))
| ~ spl1400_389 ),
inference(resolution,[],[f22700,f11795]) ).
fof(f23236,plain,
( r1_tarski(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1389),u1_struct_0(sK1388))
| ~ spl1400_390 ),
inference(resolution,[],[f22704,f11795]) ).
fof(f23239,plain,
( v3_struct_0(sK1387)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_401 ),
inference(resolution,[],[f23195,f19092]) ).
fof(f23240,plain,
( ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_401 ),
inference(forward_subsumption_resolution,[],[f23239,f19263]) ).
fof(f23241,plain,
( ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_401 ),
inference(forward_subsumption_resolution,[],[f23240,f19262]) ).
fof(f23242,plain,
( v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_401 ),
inference(forward_subsumption_resolution,[],[f23241,f19261]) ).
fof(f23243,plain,
( ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1400_401 ),
inference(forward_subsumption_resolution,[],[f23242,f19266]) ).
fof(f23244,plain,
( ~ m1_pre_topc(sK1388,sK1387)
| spl1400_401 ),
inference(forward_subsumption_resolution,[],[f23243,f19265]) ).
fof(f23245,plain,
( $false
| spl1400_401 ),
inference(forward_subsumption_resolution,[],[f23244,f22771]) ).
fof(f23246,plain,
spl1400_401,
inference(avatar_contradiction_clause,[],[f23245]) ).
fof(f23247,plain,
( sP1399(k4_subset_1(u1_struct_0(sK1388),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ l1_struct_0(sK1387)
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(superposition,[],[f23186,f15306]) ).
fof(f23252,plain,
( sP1399(k4_subset_1(u1_struct_0(sK1388),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23247,f22732]) ).
fof(f23254,definition,
( spl1400_405
<=> m1_subset_1(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k1_zfmisc_1(u1_struct_0(sK1388))) ),
introduced(definition,[new_symbols(definition,[spl1400_405])],[avatar_definition]) ).
fof(f23255,plain,
( m1_subset_1(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k1_zfmisc_1(u1_struct_0(sK1388)))
| ~ spl1400_405 ),
inference(avatar_component_clause,[],[f23254]) ).
fof(f23256,plain,
( ~ m1_subset_1(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k1_zfmisc_1(u1_struct_0(sK1388)))
| spl1400_405 ),
inference(avatar_component_clause,[],[f23254]) ).
fof(f23263,plain,
( sP1399(k4_subset_1(u1_struct_0(sK1388),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23252,f22728]) ).
fof(f23265,plain,
( sP1399(k4_subset_1(u1_struct_0(sK1388),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23263,f22724]) ).
fof(f23266,plain,
( sP1399(k4_subset_1(u1_struct_0(sK1388),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23265,f22720]) ).
fof(f23267,plain,
( sP1399(k4_subset_1(u1_struct_0(sK1388),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(forward_subsumption_resolution,[],[f23266,f22716]) ).
fof(f23268,plain,
( ~ r1_tarski(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),u1_struct_0(sK1388))
| spl1400_405 ),
inference(resolution,[],[f23256,f11796]) ).
fof(f23280,definition,
( spl1400_407
<=> m1_subset_1(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390),k1_zfmisc_1(u1_struct_0(sK1388))) ),
introduced(definition,[new_symbols(definition,[spl1400_407])],[avatar_definition]) ).
fof(f23281,plain,
( m1_subset_1(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390),k1_zfmisc_1(u1_struct_0(sK1388)))
| ~ spl1400_407 ),
inference(avatar_component_clause,[],[f23280]) ).
fof(f23282,plain,
( ~ m1_subset_1(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390),k1_zfmisc_1(u1_struct_0(sK1388)))
| spl1400_407 ),
inference(avatar_component_clause,[],[f23280]) ).
fof(f23295,plain,
( ~ r1_tarski(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390),u1_struct_0(sK1388))
| spl1400_407 ),
inference(resolution,[],[f23282,f11796]) ).
fof(f23306,plain,
( sP1399(k2_xboole_0(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ m1_subset_1(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k1_zfmisc_1(u1_struct_0(sK1388)))
| ~ m1_subset_1(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390),k1_zfmisc_1(u1_struct_0(sK1388)))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(superposition,[],[f23267,f11782]) ).
fof(f23349,plain,
( r1_tarski(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),u1_struct_0(sK1388))
| ~ l1_struct_0(sK1387)
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_390 ),
inference(superposition,[],[f23236,f15306]) ).
fof(f23350,plain,
( ~ l1_struct_0(sK1387)
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_390
| spl1400_405 ),
inference(forward_subsumption_resolution,[],[f23349,f23268]) ).
fof(f23360,plain,
( ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_390
| ~ spl1400_396
| spl1400_405 ),
inference(forward_subsumption_resolution,[],[f23350,f22732]) ).
fof(f23361,plain,
( ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_390
| ~ spl1400_395
| ~ spl1400_396
| spl1400_405 ),
inference(forward_subsumption_resolution,[],[f23360,f22728]) ).
fof(f23362,plain,
( ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_390
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| spl1400_405 ),
inference(forward_subsumption_resolution,[],[f23361,f22724]) ).
fof(f23363,plain,
( ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_390
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| spl1400_405 ),
inference(forward_subsumption_resolution,[],[f23362,f22720]) ).
fof(f23364,plain,
( $false
| ~ spl1400_390
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| spl1400_405 ),
inference(forward_subsumption_resolution,[],[f23363,f22716]) ).
fof(f23365,plain,
( ~ spl1400_390
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| spl1400_405 ),
inference(avatar_contradiction_clause,[],[f23364]) ).
fof(f23384,plain,
( r1_tarski(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390),u1_struct_0(sK1388))
| ~ l1_struct_0(sK1387)
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_389 ),
inference(superposition,[],[f23233,f15306]) ).
fof(f23385,plain,
( ~ l1_struct_0(sK1387)
| ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_389
| spl1400_407 ),
inference(forward_subsumption_resolution,[],[f23384,f23295]) ).
fof(f23395,plain,
( ~ l1_struct_0(sK1388)
| ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_389
| ~ spl1400_396
| spl1400_407 ),
inference(forward_subsumption_resolution,[],[f23385,f22732]) ).
fof(f23396,plain,
( ~ v1_funct_1(k4_tsp_2(sK1387,sK1388))
| ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_389
| ~ spl1400_395
| ~ spl1400_396
| spl1400_407 ),
inference(forward_subsumption_resolution,[],[f23395,f22728]) ).
fof(f23397,plain,
( ~ v1_funct_2(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_389
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| spl1400_407 ),
inference(forward_subsumption_resolution,[],[f23396,f22724]) ).
fof(f23398,plain,
( ~ m1_relset_1(k4_tsp_2(sK1387,sK1388),u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ spl1400_389
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| spl1400_407 ),
inference(forward_subsumption_resolution,[],[f23397,f22720]) ).
fof(f23399,plain,
( $false
| ~ spl1400_389
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| spl1400_407 ),
inference(forward_subsumption_resolution,[],[f23398,f22716]) ).
fof(f23400,plain,
( ~ spl1400_389
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| spl1400_407 ),
inference(avatar_contradiction_clause,[],[f23399]) ).
fof(f23402,plain,
( sP1399(k2_xboole_0(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ m1_subset_1(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390),k1_zfmisc_1(u1_struct_0(sK1388)))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| ~ spl1400_405 ),
inference(forward_subsumption_resolution,[],[f23306,f23255]) ).
fof(f23405,plain,
( sP1399(k2_xboole_0(k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1389),k9_relat_1(k4_tsp_2(sK1387,sK1388),sK1390)))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| ~ spl1400_405
| ~ spl1400_407 ),
inference(forward_subsumption_resolution,[],[f23402,f23281]) ).
fof(f23446,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f12753,f12673]) ).
fof(f23756,plain,
( v1_relat_1(k4_tsp_2(sK1387,sK1388))
| ~ spl1400_401 ),
inference(resolution,[],[f23446,f23194]) ).
fof(f23771,plain,
( sP1399(k9_relat_1(k4_tsp_2(sK1387,sK1388),k2_xboole_0(sK1389,sK1390)))
| ~ v1_relat_1(k4_tsp_2(sK1387,sK1388))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| ~ spl1400_405
| ~ spl1400_407 ),
inference(superposition,[],[f23405,f12035]) ).
fof(f23775,plain,
( ~ v1_relat_1(k4_tsp_2(sK1387,sK1388))
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| ~ spl1400_405
| ~ spl1400_407 ),
inference(forward_subsumption_resolution,[],[f23771,f23188]) ).
fof(f23776,plain,
( $false
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| ~ spl1400_401
| ~ spl1400_405
| ~ spl1400_407 ),
inference(forward_subsumption_resolution,[],[f23775,f23756]) ).
fof(f23777,plain,
( ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| ~ spl1400_401
| ~ spl1400_405
| ~ spl1400_407 ),
inference(avatar_contradiction_clause,[],[f23776]) ).
cnf(s338,plain,
( spl1400_389
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(sat_conversion,[],[f22734]) ).
cnf(s339,plain,
spl1400_395,
inference(sat_conversion,[],[f22774]) ).
cnf(s340,plain,
spl1400_396,
inference(sat_conversion,[],[f22775]) ).
cnf(s344,plain,
spl1400_392,
inference(sat_conversion,[],[f23147]) ).
cnf(s345,plain,
spl1400_393,
inference(sat_conversion,[],[f23155]) ).
cnf(s346,plain,
spl1400_394,
inference(sat_conversion,[],[f23164]) ).
cnf(s349,plain,
( spl1400_390
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396 ),
inference(sat_conversion,[],[f23224]) ).
cnf(s350,plain,
spl1400_401,
inference(sat_conversion,[],[f23246]) ).
cnf(s361,plain,
( ~ spl1400_390
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| spl1400_405 ),
inference(sat_conversion,[],[f23365]) ).
cnf(s364,plain,
( ~ spl1400_389
| ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| spl1400_407 ),
inference(sat_conversion,[],[f23400]) ).
cnf(s378,plain,
( ~ spl1400_392
| ~ spl1400_393
| ~ spl1400_394
| ~ spl1400_395
| ~ spl1400_396
| ~ spl1400_401
| ~ spl1400_405
| ~ spl1400_407 ),
inference(sat_conversion,[],[f23777]) ).
cnf(s380,plain,
spl1400_390,
inference(rat,[],[s349,s340,s344,s346,s345,s339]) ).
cnf(s381,plain,
spl1400_405,
inference(rat,[],[s361,s339,s340,s344,s346,s345,s380]) ).
cnf(s382,plain,
~ spl1400_407,
inference(rat,[],[s378,s339,s340,s350,s344,s345,s346,s381]) ).
cnf(s383,plain,
~ spl1400_389,
inference(rat,[],[s364,s339,s340,s344,s346,s345,s382]) ).
cnf(s384,plain,
$false,
inference(rat,[],[s338,s340,s339,s346,s345,s344,s383]) ).
fof(f23778,plain,
$false,
inference(avatar_sat_refutation,[],[s384]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : TOP038+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n006.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 19:00:11 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.11/2.56 % (59700)Detected formulas, will run a generic FOF schedule.
% 12.11/2.56 % (59708)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4051548923:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 12.11/2.56 % (59708)Instruction limit reached!
% 12.11/2.56 % (59708)------------------------------
% 12.11/2.56 % (59708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.11/2.56 % (59708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.56 % (59708)CaDiCaL version: 2.1.3
% 12.11/2.56 % (59708)Termination reason: Instruction limit
% 12.11/2.56 % (59708)Termination phase: Saturation
% 12.11/2.56 % (59708)Time elapsed: 0.037 s
% 12.11/2.56 % (59708)Peak memory usage: 94 MB
% 12.11/2.56 % (59708)Instructions burned: 110 (million)
% 12.11/2.56 % (59705)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1169737748:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 12.11/2.56 % (59709)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2684872335:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 12.11/2.56 % (59710)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1902452808:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 12.11/2.56 % (59711)dis-21_1_sil=8000:lcm=predicate:random_seed=3569916545:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 12.11/2.56 % (59706)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2096813952:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 12.11/2.56 % (59707)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=845319731:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 12.11/2.56 % (59709)Instruction limit reached!
% 12.11/2.56 % (59709)------------------------------
% 12.11/2.56 % (59709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.11/2.56 % (59709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.56 % (59709)CaDiCaL version: 2.1.3
% 12.11/2.56 % (59709)Termination reason: Instruction limit
% 12.11/2.56 % (59709)Termination phase: Property scanning
% 12.11/2.56 % (59709)Time elapsed: 0.072 s
% 12.11/2.56 % (59709)Peak memory usage: 94 MB
% 12.11/2.56 % (59709)Instructions burned: 119 (million)
% 12.11/2.56 % (59711)Instruction limit reached!
% 12.11/2.56 % (59711)------------------------------
% 12.11/2.56 % (59711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.11/2.56 % (59711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.56 % (59711)CaDiCaL version: 2.1.3
% 12.11/2.56 % (59711)Termination reason: Instruction limit
% 12.11/2.56 % (59711)Termination phase: Preprocessing 3
% 12.11/2.56 % (59711)Time elapsed: 0.092 s
% 12.11/2.56 % (59711)Peak memory usage: 95 MB
% 12.11/2.56 % (59711)Instructions burned: 130 (million)
% 12.11/2.56 % (59710)Instruction limit reached!
% 12.11/2.56 % (59710)------------------------------
% 12.11/2.56 % (59710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.11/2.56 % (59710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.56 % (59710)CaDiCaL version: 2.1.3
% 12.11/2.56 % (59710)Termination reason: Instruction limit
% 12.11/2.56 % (59710)Termination phase: Preprocessing 3
% 12.11/2.56 % (59710)Time elapsed: 0.094 s
% 12.11/2.56 % (59710)Peak memory usage: 94 MB
% 12.11/2.56 % (59710)Instructions burned: 139 (million)
% 12.11/2.56 % (59719)lrs+10_1_sil=8000:sp=occurrence:random_seed=35146701:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 12.11/2.56 % (59720)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3440690563:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 12.11/2.56 % (59719)Instruction limit reached!
% 12.11/2.56 % (59719)------------------------------
% 12.11/2.56 % (59719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.11/2.56 % (59719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.11/2.56 % (59719)CaDiCaL version: 2.1.3
% 12.11/2.56 % (59719)Termination reason: Instruction limit
% 12.11/2.56 % (59719)Termination phase: Saturation
% 12.11/2.56 % (59719)Time elapsed: 0.101 s
% 12.11/2.56 % (59719)Peak memory usage: 98 MB
% 28.69/4.80 % (59719)Instructions burned: 288 (million)
% 28.69/4.80 % (59721)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4003829290:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 28.69/4.80 % (59722)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2135148537:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 28.69/4.80 % (59720)Instruction limit reached!
% 28.69/4.80 % (59720)------------------------------
% 28.69/4.80 % (59720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.69/4.80 % (59720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.69/4.80 % (59720)CaDiCaL version: 2.1.3
% 28.69/4.80 % (59720)Termination reason: Instruction limit
% 28.69/4.80 % (59720)Termination phase: Saturation
% 28.69/4.80 % (59720)Time elapsed: 0.088 s
% 28.69/4.80 % (59720)Peak memory usage: 94 MB
% 28.69/4.80 % (59720)Instructions burned: 157 (million)
% 28.69/4.80 % (59725)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4157488205:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 28.69/4.80 % (59722)Instruction limit reached!
% 28.69/4.80 % (59722)------------------------------
% 28.69/4.80 % (59722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.69/4.80 % (59722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.69/4.80 % (59722)CaDiCaL version: 2.1.3
% 28.69/4.80 % (59722)Termination reason: Instruction limit
% 28.69/4.80 % (59722)Termination phase: Property scanning
% 28.69/4.80 % (59722)Time elapsed: 0.146 s
% 28.69/4.80 % (59722)Peak memory usage: 98 MB
% 28.69/4.80 % (59722)Instructions burned: 250 (million)
% 28.69/4.80 % (59725)Instruction limit reached!
% 28.69/4.80 % (59725)------------------------------
% 28.69/4.80 % (59725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.69/4.80 % (59725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.69/4.80 % (59725)CaDiCaL version: 2.1.3
% 28.69/4.80 % (59725)Termination reason: Instruction limit
% 28.69/4.80 % (59725)Termination phase: Saturation
% 28.69/4.80 % (59725)Time elapsed: 0.089 s
% 28.69/4.80 % (59725)Peak memory usage: 98 MB
% 28.69/4.80 % (59725)Instructions burned: 294 (million)
% 28.69/4.80 % (59721)Instruction limit reached!
% 28.69/4.80 % (59721)------------------------------
% 28.69/4.80 % (59721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.69/4.80 % (59721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.69/4.80 % (59721)CaDiCaL version: 2.1.3
% 28.69/4.80 % (59721)Termination reason: Instruction limit
% 28.69/4.80 % (59721)Termination phase: Saturation
% 28.69/4.80 % (59721)Time elapsed: 0.221 s
% 28.69/4.80 % (59721)Peak memory usage: 96 MB
% 28.69/4.80 % (59721)Instructions burned: 326 (million)
% 28.69/4.80 % (59728)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=222047411:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 28.69/4.80 % (59730)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1635214107:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 28.69/4.80 % (59731)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=733292271:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 28.69/4.80 % (59731)Instruction limit reached!
% 28.69/4.80 % (59731)------------------------------
% 28.69/4.80 % (59731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.69/4.80 % (59731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.69/4.80 % (59731)CaDiCaL version: 2.1.3
% 28.69/4.80 % (59731)Termination reason: Instruction limit
% 28.69/4.80 % (59731)Termination phase: Preprocessing 3
% 28.69/4.80 % (59731)Time elapsed: 0.049 s
% 28.69/4.80 % (59731)Peak memory usage: 96 MB
% 28.69/4.80 % (59731)Instructions burned: 128 (million)
% 28.69/4.80 % (59732)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3628928736:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 28.69/4.80 % (59730)Instruction limit reached!
% 28.69/4.80 % (59730)------------------------------
% 28.69/4.80 % (59730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.69/4.80 % (59730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.69/4.80 % (59730)CaDiCaL version: 2.1.3
% 28.69/4.80 % (59730)Termination reason: Instruction limit
% 28.69/4.80 % (59730)Termination phase: Property scanning
% 28.69/4.80 % (59730)Time elapsed: 0.073 s
% 53.34/8.31 % (59730)Peak memory usage: 94 MB
% 53.34/8.31 % (59730)Instructions burned: 115 (million)
% 53.34/8.31 % (59732)Instruction limit reached!
% 53.34/8.31 % (59732)------------------------------
% 53.34/8.31 % (59732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.34/8.31 % (59732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.34/8.31 % (59732)CaDiCaL version: 2.1.3
% 53.34/8.31 % (59732)Termination reason: Instruction limit
% 53.34/8.31 % (59732)Termination phase: Preprocessing 3
% 53.34/8.31 % (59732)Time elapsed: 0.059 s
% 53.34/8.31 % (59732)Peak memory usage: 91 MB
% 53.34/8.31 % (59732)Instructions burned: 115 (million)
% 53.34/8.31 % (59736)lrs+10_1_sil=8000:sp=occurrence:random_seed=2248989525:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 53.34/8.31 % (59738)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2468037392:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 53.34/8.31 % (59739)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2243386032:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 53.34/8.31 % (59738)Instruction limit reached!
% 53.34/8.31 % (59738)------------------------------
% 53.34/8.31 % (59738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.34/8.31 % (59738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.34/8.31 % (59738)CaDiCaL version: 2.1.3
% 53.34/8.31 % (59738)Termination reason: Instruction limit
% 53.34/8.31 % (59738)Termination phase: Saturation
% 53.34/8.31 % (59738)Time elapsed: 0.251 s
% 53.34/8.31 % (59738)Peak memory usage: 97 MB
% 53.34/8.31 % (59738)Instructions burned: 437 (million)
% 53.34/8.31 % (59736)Instruction limit reached!
% 53.34/8.31 % (59736)------------------------------
% 53.34/8.31 % (59736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.34/8.31 % (59736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.34/8.31 % (59736)CaDiCaL version: 2.1.3
% 53.34/8.31 % (59736)Termination reason: Instruction limit
% 53.34/8.31 % (59736)Termination phase: Saturation
% 53.34/8.31 % (59736)Time elapsed: 0.319 s
% 53.34/8.31 % (59736)Peak memory usage: 107 MB
% 53.34/8.31 % (59736)Instructions burned: 909 (million)
% 53.34/8.31 % (59744)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3304565069:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 53.34/8.31 % (59743)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2877675039:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 53.34/8.31 % (59743)Instruction limit reached!
% 53.34/8.31 % (59743)------------------------------
% 53.34/8.31 % (59743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.34/8.31 % (59743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.34/8.31 % (59743)CaDiCaL version: 2.1.3
% 53.34/8.31 % (59743)Termination reason: Instruction limit
% 53.34/8.31 % (59743)Termination phase: Saturation
% 53.34/8.31 % (59743)Time elapsed: 0.081 s
% 53.34/8.31 % (59743)Peak memory usage: 96 MB
% 53.34/8.31 % (59743)Instructions burned: 134 (million)
% 53.34/8.31 % (59744)Instruction limit reached!
% 53.34/8.31 % (59744)------------------------------
% 53.34/8.31 % (59744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.34/8.31 % (59744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.34/8.31 % (59744)CaDiCaL version: 2.1.3
% 53.34/8.31 % (59744)Termination reason: Instruction limit
% 53.34/8.31 % (59744)Termination phase: Saturation
% 53.34/8.31 % (59744)Time elapsed: 0.181 s
% 53.34/8.31 % (59744)Peak memory usage: 106 MB
% 53.34/8.31 % (59744)Instructions burned: 597 (million)
% 53.34/8.31 % (59747)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2094461647:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 53.34/8.31 % (59748)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=337508951:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 53.34/8.31 % (59748)Instruction limit reached!
% 53.34/8.31 % (59748)------------------------------
% 53.34/8.31 % (59748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.34/8.31 % (59748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.34/8.31 % (59748)CaDiCaL version: 2.1.3
% 84.74/12.74 % (59748)Termination reason: Instruction limit
% 84.74/12.74 % (59748)Termination phase: Clausification
% 84.74/12.74 % (59748)Time elapsed: 0.043 s
% 84.74/12.74 % (59748)Peak memory usage: 93 MB
% 84.74/12.74 % (59748)Instructions burned: 125 (million)
% 84.74/12.74 % (59751)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2972995938:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 84.74/12.74 % (59751)Instruction limit reached!
% 84.74/12.74 % (59751)------------------------------
% 84.74/12.74 % (59751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.74/12.74 % (59751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.74/12.74 % (59751)CaDiCaL version: 2.1.3
% 84.74/12.74 % (59751)Termination reason: Instruction limit
% 84.74/12.74 % (59751)Termination phase: Unused predicate definition removal
% 84.74/12.74 % (59751)Time elapsed: 0.042 s
% 84.74/12.74 % (59751)Peak memory usage: 90 MB
% 84.74/12.74 % (59751)Instructions burned: 134 (million)
% 84.74/12.74 % (59753)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1298363269:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 84.74/12.74 % (59753)Instruction limit reached!
% 84.74/12.74 % (59753)------------------------------
% 84.74/12.74 % (59753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.74/12.74 % (59753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.74/12.74 % (59753)CaDiCaL version: 2.1.3
% 84.74/12.74 % (59753)Termination reason: Instruction limit
% 84.74/12.74 % (59753)Termination phase: Saturation
% 84.74/12.74 % (59753)Time elapsed: 0.044 s
% 84.74/12.74 % (59753)Peak memory usage: 95 MB
% 84.74/12.74 % (59753)Instructions burned: 144 (million)
% 84.74/12.74 % (59728)Instruction limit reached!
% 84.74/12.74 % (59728)------------------------------
% 84.74/12.74 % (59728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.74/12.74 % (59728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.74/12.74 % (59728)CaDiCaL version: 2.1.3
% 84.74/12.74 % (59728)Termination reason: Instruction limit
% 84.74/12.74 % (59728)Termination phase: Saturation
% 84.74/12.74 % (59728)Time elapsed: 1.527 s
% 84.74/12.74 % (59728)Peak memory usage: 234 MB
% 84.74/12.74 % (59728)Instructions burned: 2352 (million)
% 84.74/12.74 % (59755)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=40199165:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 84.74/12.74 % (59756)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=4048233596:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 84.74/12.74 % (59755)Instruction limit reached!
% 84.74/12.74 % (59755)------------------------------
% 84.74/12.74 % (59755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.74/12.74 % (59755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.74/12.74 % (59755)CaDiCaL version: 2.1.3
% 84.74/12.74 % (59755)Termination reason: Instruction limit
% 84.74/12.74 % (59755)Termination phase: Saturation
% 84.74/12.74 % (59755)Time elapsed: 0.140 s
% 84.74/12.74 % (59755)Peak memory usage: 98 MB
% 84.74/12.74 % (59755)Instructions burned: 431 (million)
% 84.74/12.74 % (59759)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2373366208:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 84.74/12.74 % (59759)Instruction limit reached!
% 84.74/12.74 % (59759)------------------------------
% 84.74/12.74 % (59759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.74/12.74 % (59759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.74/12.74 % (59759)CaDiCaL version: 2.1.3
% 84.74/12.74 % (59759)Termination reason: Instruction limit
% 84.74/12.74 % (59759)Termination phase: Preprocessing 3
% 84.74/12.74 % (59759)Time elapsed: 0.057 s
% 84.74/12.74 % (59759)Peak memory usage: 96 MB
% 84.74/12.74 % (59759)Instructions burned: 150 (million)
% 84.74/12.74 % (59761)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4114986675:i=14155:bd=all_2972 on theBenchmark for (2972ds/14155Mi)
% 84.74/12.74 % (59739)Instruction limit reached!
% 84.74/12.74 % (59739)------------------------------
% 84.74/12.74 % (59739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.74/12.74 % (59739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.26/15.55 % (59739)CaDiCaL version: 2.1.3
% 104.26/15.55 % (59739)Termination reason: Instruction limit
% 104.26/15.55 % (59739)Termination phase: Saturation
% 104.26/15.55 % (59739)Time elapsed: 2.958 s
% 104.26/15.55 % (59739)Peak memory usage: 190 MB
% 104.26/15.55 % (59739)Instructions burned: 5204 (million)
% 104.26/15.55 % (59763)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1408437112:i=667:av=off:fsr=off_2958 on theBenchmark for (2958ds/667Mi)
% 104.26/15.55 % (59763)Instruction limit reached!
% 104.26/15.55 % (59763)------------------------------
% 104.26/15.55 % (59763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.26/15.55 % (59763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.26/15.55 % (59763)CaDiCaL version: 2.1.3
% 104.26/15.55 % (59763)Termination reason: Instruction limit
% 104.26/15.55 % (59763)Termination phase: Saturation
% 104.26/15.55 % (59763)Time elapsed: 0.342 s
% 104.26/15.55 % (59763)Peak memory usage: 106 MB
% 104.26/15.55 % (59763)Instructions burned: 667 (million)
% 104.26/15.55 % (59765)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3209418665:s2a=on:i=185:s2at=1.8:fdi=4_2953 on theBenchmark for (2953ds/185Mi)
% 104.26/15.55 % (59765)Instruction limit reached!
% 104.26/15.55 % (59765)------------------------------
% 104.26/15.55 % (59765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.26/15.55 % (59765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.26/15.55 % (59765)CaDiCaL version: 2.1.3
% 104.26/15.55 % (59765)Termination reason: Instruction limit
% 104.26/15.55 % (59765)Termination phase: NewCNF
% 104.26/15.55 % (59765)Time elapsed: 0.123 s
% 104.26/15.55 % (59765)Peak memory usage: 98 MB
% 104.26/15.55 % (59765)Instructions burned: 186 (million)
% 104.26/15.55 % (59767)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1489872094:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2950 on theBenchmark for (2950ds/193Mi)
% 104.26/15.55 % (59767)Instruction limit reached!
% 104.26/15.55 % (59767)------------------------------
% 104.26/15.55 % (59767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.26/15.55 % (59767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.26/15.55 % (59767)CaDiCaL version: 2.1.3
% 104.26/15.55 % (59767)Termination reason: Instruction limit
% 104.26/15.55 % (59767)Termination phase: Saturation
% 104.26/15.55 % (59767)Time elapsed: 0.109 s
% 104.26/15.55 % (59767)Peak memory usage: 97 MB
% 104.26/15.55 % (59767)Instructions burned: 193 (million)
% 104.26/15.55 % (59769)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3273830937:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2947 on theBenchmark for (2947ds/4850Mi)
% 104.26/15.55 % (59756)Instruction limit reached!
% 104.26/15.55 % (59756)------------------------------
% 104.26/15.55 % (59756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.26/15.55 % (59756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.26/15.55 % (59756)CaDiCaL version: 2.1.3
% 104.26/15.55 % (59756)Termination reason: Instruction limit
% 104.26/15.55 % (59756)Termination phase: Saturation
% 104.26/15.55 % (59756)Time elapsed: 3.556 s
% 104.26/15.55 % (59756)Peak memory usage: 242 MB
% 104.26/15.55 % (59756)Instructions burned: 6061 (million)
% 104.26/15.55 % (59771)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4044494139:i=12111:sd=1:ss=included_2938 on theBenchmark for (2938ds/12111Mi)
% 104.26/15.55 % (59761)Instruction limit reached!
% 104.26/15.55 % (59761)------------------------------
% 104.26/15.55 % (59761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.26/15.55 % (59761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.26/15.55 % (59761)CaDiCaL version: 2.1.3
% 104.26/15.55 % (59761)Termination reason: Instruction limit
% 104.26/15.55 % (59761)Termination phase: Saturation
% 104.26/15.55 % (59761)Time elapsed: 4.546 s
% 104.26/15.55 % (59761)Peak memory usage: 252 MB
% 104.26/15.55 % (59761)Instructions burned: 14157 (million)
% 104.26/15.55 % (59773)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1224906317:i=319:kws=precedence:fsr=off_2925 on theBenchmark for (2925ds/319Mi)
% 104.26/15.55 % (59773)Instruction limit reached!
% 104.26/15.55 % (59773)------------------------------
% 104.26/15.55 % (59773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59773)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59773)Termination reason: Instruction limit
% 112.16/16.86 % (59773)Termination phase: Property scanning
% 112.16/16.86 % (59773)Time elapsed: 0.088 s
% 112.16/16.86 % (59773)Peak memory usage: 99 MB
% 112.16/16.86 % (59773)Instructions burned: 325 (million)
% 112.16/16.86 % (59775)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2970568812:i=2064:ep=RST_2923 on theBenchmark for (2923ds/2064Mi)
% 112.16/16.86 % (59769)Instruction limit reached!
% 112.16/16.86 % (59769)------------------------------
% 112.16/16.86 % (59769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59769)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59769)Termination reason: Instruction limit
% 112.16/16.86 % (59769)Termination phase: Saturation
% 112.16/16.86 % (59769)Time elapsed: 2.615 s
% 112.16/16.86 % (59769)Peak memory usage: 125 MB
% 112.16/16.86 % (59769)Instructions burned: 4853 (million)
% 112.16/16.86 % (59777)dis-1011_128_sil=32000:random_seed=946007749:i=3706:ep=RST:av=off_2919 on theBenchmark for (2919ds/3706Mi)
% 112.16/16.86 % (59775)Instruction limit reached!
% 112.16/16.86 % (59775)------------------------------
% 112.16/16.86 % (59775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59775)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59775)Termination reason: Instruction limit
% 112.16/16.86 % (59775)Termination phase: Saturation
% 112.16/16.86 % (59775)Time elapsed: 0.568 s
% 112.16/16.86 % (59775)Peak memory usage: 124 MB
% 112.16/16.86 % (59775)Instructions burned: 2078 (million)
% 112.16/16.86 % (59779)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2956274769:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2916 on theBenchmark for (2916ds/757Mi)
% 112.16/16.86 % (59779)Instruction limit reached!
% 112.16/16.86 % (59779)------------------------------
% 112.16/16.86 % (59779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59779)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59779)Termination reason: Instruction limit
% 112.16/16.86 % (59779)Termination phase: Saturation
% 112.16/16.86 % (59779)Time elapsed: 0.285 s
% 112.16/16.86 % (59779)Peak memory usage: 100 MB
% 112.16/16.86 % (59779)Instructions burned: 757 (million)
% 112.16/16.86 % (59781)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2083620052:i=13913:ss=axioms:sgt=8_2912 on theBenchmark for (2912ds/13913Mi)
% 112.16/16.86 % (59747)Instruction limit reached!
% 112.16/16.86 % (59747)------------------------------
% 112.16/16.86 % (59747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59747)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59747)Termination reason: Instruction limit
% 112.16/16.86 % (59747)Termination phase: Saturation
% 112.16/16.86 % (59747)Time elapsed: 7.785 s
% 112.16/16.86 % (59747)Peak memory usage: 258 MB
% 112.16/16.86 % (59747)Instructions burned: 13193 (million)
% 112.16/16.86 % (59783)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=594672143:i=9925:aac=none_2904 on theBenchmark for (2904ds/9925Mi)
% 112.16/16.86 % (59777)Instruction limit reached!
% 112.16/16.86 % (59777)------------------------------
% 112.16/16.86 % (59777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59777)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59777)Termination reason: Instruction limit
% 112.16/16.86 % (59777)Termination phase: Saturation
% 112.16/16.86 % (59777)Time elapsed: 2.259 s
% 112.16/16.86 % (59777)Peak memory usage: 130 MB
% 112.16/16.86 % (59777)Instructions burned: 3706 (million)
% 112.16/16.86 % (59785)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2198776405:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2895 on theBenchmark for (2895ds/2479Mi)
% 112.16/16.86 % (59785)Instruction limit reached!
% 112.16/16.86 % (59785)------------------------------
% 112.16/16.86 % (59785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59785)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59785)Termination reason: Instruction limit
% 112.16/16.86 % (59785)Termination phase: Saturation
% 112.16/16.86 % (59785)Time elapsed: 1.450 s
% 112.16/16.86 % (59785)Peak memory usage: 114 MB
% 112.16/16.86 % (59785)Instructions burned: 2479 (million)
% 112.16/16.86 % (59787)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3669663160:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2879 on theBenchmark for (2879ds/440Mi)
% 112.16/16.86 % (59787)Instruction limit reached!
% 112.16/16.86 % (59787)------------------------------
% 112.16/16.86 % (59787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59787)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59787)Termination reason: Instruction limit
% 112.16/16.86 % (59787)Termination phase: Property scanning
% 112.16/16.86 % (59787)Time elapsed: 0.220 s
% 112.16/16.86 % (59787)Peak memory usage: 102 MB
% 112.16/16.86 % (59787)Instructions burned: 441 (million)
% 112.16/16.86 % (59789)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=625621664:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2875 on theBenchmark for (2875ds/11145Mi)
% 112.16/16.86 % (59781)Instruction limit reached!
% 112.16/16.86 % (59781)------------------------------
% 112.16/16.86 % (59781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59781)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59781)Termination reason: Instruction limit
% 112.16/16.86 % (59781)Termination phase: Saturation
% 112.16/16.86 % (59781)Time elapsed: 4.356 s
% 112.16/16.86 % (59781)Peak memory usage: 252 MB
% 112.16/16.86 % (59781)Instructions burned: 13916 (million)
% 112.16/16.86 % (59791)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=4182655755:cts=off:i=3034:av=off:er=known:fsd=on_2867 on theBenchmark for (2867ds/3034Mi)
% 112.16/16.86 % (59771)Instruction limit reached!
% 112.16/16.86 % (59771)------------------------------
% 112.16/16.86 % (59771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59771)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59771)Termination reason: Instruction limit
% 112.16/16.86 % (59771)Termination phase: Saturation
% 112.16/16.86 % (59771)Time elapsed: 7.430 s
% 112.16/16.86 % (59771)Peak memory usage: 266 MB
% 112.16/16.86 % (59771)Instructions burned: 12111 (million)
% 112.16/16.86 % (59793)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1863631379:st=2:s2a=on:i=524:s2at=2:ss=axioms_2862 on theBenchmark for (2862ds/524Mi)
% 112.16/16.86 % (59793)Instruction limit reached!
% 112.16/16.86 % (59793)------------------------------
% 112.16/16.86 % (59793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59793)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59793)Termination reason: Instruction limit
% 112.16/16.86 % (59793)Termination phase: Saturation
% 112.16/16.86 % (59793)Time elapsed: 0.297 s
% 112.16/16.86 % (59793)Peak memory usage: 102 MB
% 112.16/16.86 % (59793)Instructions burned: 525 (million)
% 112.16/16.86 % (59795)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3166288671:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2857 on theBenchmark for (2857ds/1016Mi)
% 112.16/16.86 % (59791)Instruction limit reached!
% 112.16/16.86 % (59791)------------------------------
% 112.16/16.86 % (59791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59791)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59791)Termination reason: Instruction limit
% 112.16/16.86 % (59791)Termination phase: Saturation
% 112.16/16.86 % (59791)Time elapsed: 1.056 s
% 112.16/16.86 % (59791)Peak memory usage: 227 MB
% 112.16/16.86 % (59791)Instructions burned: 3034 (million)
% 112.16/16.86 % (59797)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1198312331:i=14123:bd=preordered:ins=4_2855 on theBenchmark for (2855ds/14123Mi)
% 112.16/16.86 % (59795)Instruction limit reached!
% 112.16/16.86 % (59795)------------------------------
% 112.16/16.86 % (59795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59795)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59795)Termination reason: Instruction limit
% 112.16/16.86 % (59795)Termination phase: Saturation
% 112.16/16.86 % (59795)Time elapsed: 0.513 s
% 112.16/16.86 % (59795)Peak memory usage: 110 MB
% 112.16/16.86 % (59795)Instructions burned: 1017 (million)
% 112.16/16.86 % (59799)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=430279063:i=5781:kws=precedence:bd=all:rawr=on_2851 on theBenchmark for (2851ds/5781Mi)
% 112.16/16.86 % (59783)Instruction limit reached!
% 112.16/16.86 % (59783)------------------------------
% 112.16/16.86 % (59783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.86 % (59783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.86 % (59783)CaDiCaL version: 2.1.3
% 112.16/16.86 % (59783)Termination reason: Instruction limit
% 112.16/16.86 % (59783)Termination phase: Saturation
% 112.16/16.86 % (59783)Time elapsed: 5.522 s
% 112.16/16.86 % (59783)Peak memory usage: 240 MB
% 112.16/16.86 % (59783)Instructions burned: 9926 (million)
% 112.16/16.86 % (59801)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=4160423355:i=2448:gtgl=5:bd=preordered:gtg=all_2847 on theBenchmark for (2847ds/2448Mi)
% 112.16/16.86 % (59797)First to succeed.
% 112.16/16.86 % (59797)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-59700"
% 112.16/16.86 % (59789)Also succeeded, but the first one will report.
% 112.16/16.86 % (59797)Refutation found. Thanks to Tanya!
% 112.16/16.86 % SZS status Theorem for theBenchmark
% 112.16/16.86 % SZS output start Proof for theBenchmark
% See solution above
% 114.33/17.06 % (59797)------------------------------
% 114.33/17.06 % (59797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.33/17.06 % (59797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.33/17.06 % (59797)CaDiCaL version: 2.1.3
% 114.33/17.06 % (59797)Termination reason: Refutation
% 114.33/17.06 % (59797)Time elapsed: 1.394 s
% 114.33/17.06 % (59797)Peak memory usage: 233 MB
% 114.33/17.06 % (59797)Instructions burned: 4341 (million)
% 114.33/17.06 % (59797)------------------------------
% 114.33/17.06 % (59797)------------------------------
% 114.33/17.06 % (59700)Success in time 16.189 s
% 114.33/17.06 % Vampire exiting
%------------------------------------------------------------------------------