%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU440+3 : 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 : n010.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 12:49:05 PM UTC 2026
% Result : Theorem 78.40s 22.26s
% Output : Refutation 142.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 27
% Syntax : Number of formulae : 210 ( 35 unt; 11 def)
% Number of atoms : 513 ( 89 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 556 ( 253 ~; 257 |; 13 &)
% ( 12 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 18 ( 16 usr; 12 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 5 con; 0-5 aty)
% Number of variables : 200 ( 0 sgn 195 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f758,axiom,
! [X0] :
( v1_relat_1(X0)
=> ! [X1] :
( v1_relat_1(X1)
=> k4_relat_1(k5_relat_1(X0,X1)) = k5_relat_1(k4_relat_1(X1),k4_relat_1(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_relat_1) ).
fof(f868,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> ! [X2] :
( v1_relat_1(X2)
=> k9_relat_1(k5_relat_1(X1,X2),X0) = k9_relat_1(X2,k9_relat_1(X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t159_relat_1) ).
fof(f879,axiom,
! [X0] :
( v1_relat_1(X0)
=> k10_relat_1(X0,k2_relat_1(X0)) = k1_relat_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t169_relat_1) ).
fof(f880,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> r1_tarski(k10_relat_1(X1,X0),k10_relat_1(X1,k2_relat_1(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t170_relat_1) ).
fof(f892,axiom,
! [X0] :
( v1_relat_1(X0)
=> ! [X1] :
( v1_relat_1(X1)
=> k1_relat_1(k5_relat_1(X0,X1)) = k10_relat_1(X0,k1_relat_1(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t182_relat_1) ).
fof(f1333,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(f1392,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(f1394,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(f1409,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(f1411,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(f1419,axiom,
! [X0,X1,X2,X3] :
( m1_relset_1(X2,X0,X1)
=> k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k10_relset_1) ).
fof(f4077,axiom,
! [X0] :
( v1_relat_1(X0)
=> ( k1_funct_5(X0) = k1_relat_1(X0)
& k2_funct_5(X0) = k2_relat_1(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_funct_5) ).
fof(f19066,axiom,
! [X0,X1,X2,X3,X4] :
( ( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
& m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) )
=> m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_relset_2) ).
fof(f19067,axiom,
! [X0,X1,X2,X3,X4] :
( ( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
& m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) )
=> k9_relset_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k9_relset_2) ).
fof(f19122,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X1,X0)
=> ( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
& k2_funct_5(X2) = k10_relset_1(X1,X0,X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t51_relset_2) ).
fof(f19123,conjecture,
! [X0,X1,X2,X3] :
( m2_relset_1(X3,X0,X1)
=> ! [X4] :
( m2_relset_1(X4,X1,X2)
=> ( k1_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X0,k6_relset_1(X0,X1,X3),k1_funct_5(X4))
& r1_tarski(k1_funct_5(k9_relset_2(X0,X1,X2,X3,X4)),k1_funct_5(X3)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t52_relset_2) ).
fof(f19124,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( m2_relset_1(X3,X0,X1)
=> ! [X4] :
( m2_relset_1(X4,X1,X2)
=> ( k1_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X0,k6_relset_1(X0,X1,X3),k1_funct_5(X4))
& r1_tarski(k1_funct_5(k9_relset_2(X0,X1,X2,X3,X4)),k1_funct_5(X3)) ) ) ),
inference(negated_conjecture,[status(cth)],[f19123]) ).
fof(f19197,plain,
? [X0,X1,X2,X3] :
( ? [X4] :
( ( k1_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) != k10_relset_1(X1,X0,k6_relset_1(X0,X1,X3),k1_funct_5(X4))
| ~ r1_tarski(k1_funct_5(k9_relset_2(X0,X1,X2,X3,X4)),k1_funct_5(X3)) )
& m2_relset_1(X4,X1,X2) )
& m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f19124]) ).
fof(f19225,plain,
! [X0,X1,X2] :
( ( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
& k2_funct_5(X2) = k10_relset_1(X1,X0,X2,X1) )
| ~ m2_relset_1(X2,X1,X0) ),
inference(ennf_transformation,[],[f19122]) ).
fof(f19229,plain,
! [X0,X1,X2] :
( k6_relset_1(X0,X1,X2) = k4_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1411]) ).
fof(f19231,plain,
! [X0,X1,X2] :
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1409]) ).
fof(f19238,plain,
! [X0,X1,X2,X3] :
( k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1419]) ).
fof(f19245,plain,
! [X0,X1,X2,X3,X4] :
( k9_relset_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(ennf_transformation,[],[f19067]) ).
fof(f19246,plain,
! [X0,X1,X2,X3,X4] :
( k9_relset_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(flattening,[],[f19245]) ).
fof(f19247,plain,
! [X0,X1,X2,X3,X4] :
( m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(ennf_transformation,[],[f19066]) ).
fof(f19248,plain,
! [X0,X1,X2,X3,X4] :
( m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(flattening,[],[f19247]) ).
fof(f19276,plain,
! [X0] :
( ( k1_funct_5(X0) = k1_relat_1(X0)
& k2_funct_5(X0) = k2_relat_1(X0) )
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f4077]) ).
fof(f19453,plain,
! [X0] :
( ! [X1] :
( k4_relat_1(k5_relat_1(X0,X1)) = k5_relat_1(k4_relat_1(X1),k4_relat_1(X0))
| ~ v1_relat_1(X1) )
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f758]) ).
fof(f19518,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,[],[f1392]) ).
fof(f19519,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1333]) ).
fof(f19809,plain,
! [X0,X1] :
( ! [X2] :
( k9_relat_1(k5_relat_1(X1,X2),X0) = k9_relat_1(X2,k9_relat_1(X1,X0))
| ~ v1_relat_1(X2) )
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f868]) ).
fof(f20798,plain,
! [X0] :
( ! [X1] :
( k1_relat_1(k5_relat_1(X0,X1)) = k10_relat_1(X0,k1_relat_1(X1))
| ~ v1_relat_1(X1) )
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f892]) ).
fof(f20813,plain,
! [X0,X1] :
( r1_tarski(k10_relat_1(X1,X0),k10_relat_1(X1,k2_relat_1(X1)))
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f880]) ).
fof(f20814,plain,
! [X0] :
( k10_relat_1(X0,k2_relat_1(X0)) = k1_relat_1(X0)
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f879]) ).
fof(f24059,plain,
( ( k1_funct_5(k9_relset_2(sK143,sK144,sK145,sK146,sK147)) != k10_relset_1(sK144,sK143,k6_relset_1(sK143,sK144,sK146),k1_funct_5(sK147))
| ~ r1_tarski(k1_funct_5(k9_relset_2(sK143,sK144,sK145,sK146,sK147)),k1_funct_5(sK146)) )
& m2_relset_1(sK147,sK144,sK145)
& m2_relset_1(sK146,sK143,sK144) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK143,sK144,sK145,sK146,sK147]),skolemize(X0,sK143),skolemize(X1,sK144),skolemize(X2,sK145),skolemize(X3,sK146),skolemize(X4,sK147)],[f19197]) ).
fof(f24157,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,[],[f1394]) ).
fof(f25781,plain,
m2_relset_1(sK146,sK143,sK144),
inference(cnf_transformation,[],[f24059]) ).
fof(f25782,plain,
m2_relset_1(sK147,sK144,sK145),
inference(cnf_transformation,[],[f24059]) ).
fof(f25783,plain,
( k1_funct_5(k9_relset_2(sK143,sK144,sK145,sK146,sK147)) != k10_relset_1(sK144,sK143,k6_relset_1(sK143,sK144,sK146),k1_funct_5(sK147))
| ~ r1_tarski(k1_funct_5(k9_relset_2(sK143,sK144,sK145,sK146,sK147)),k1_funct_5(sK146)) ),
inference(cnf_transformation,[],[f24059]) ).
fof(f25819,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X1,X0)
| k10_relset_1(X1,X0,X2,X1) = k2_funct_5(X2) ),
inference(cnf_transformation,[],[f19225]) ).
fof(f25820,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X1,X0)
| k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0) ),
inference(cnf_transformation,[],[f19225]) ).
fof(f25826,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
inference(cnf_transformation,[],[f19229]) ).
fof(f25828,plain,
! [X2,X0,X1] :
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f19231]) ).
fof(f25844,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f19238]) ).
fof(f25857,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| k5_relat_1(X3,X4) = k9_relset_2(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f19246]) ).
fof(f25858,plain,
! [X2,X3,X0,X1,X4] :
( m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[],[f19248]) ).
fof(f25917,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k1_relat_1(X0) = k1_funct_5(X0) ),
inference(cnf_transformation,[],[f19276]) ).
fof(f26213,plain,
! [X0,X1] :
( ~ v1_relat_1(X1)
| k4_relat_1(k5_relat_1(X0,X1)) = k5_relat_1(k4_relat_1(X1),k4_relat_1(X0))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f19453]) ).
fof(f26237,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f24157]) ).
fof(f26320,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,[],[f19518]) ).
fof(f26321,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f19519]) ).
fof(f26703,plain,
! [X2,X0,X1] :
( ~ v1_relat_1(X2)
| k9_relat_1(k5_relat_1(X1,X2),X0) = k9_relat_1(X2,k9_relat_1(X1,X0))
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f19809]) ).
fof(f28321,plain,
! [X0,X1] :
( ~ v1_relat_1(X1)
| k1_relat_1(k5_relat_1(X0,X1)) = k10_relat_1(X0,k1_relat_1(X1))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f20798]) ).
fof(f28334,plain,
! [X0,X1] :
( r1_tarski(k10_relat_1(X1,X0),k10_relat_1(X1,k2_relat_1(X1)))
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f20813]) ).
fof(f28335,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k1_relat_1(X0) = k10_relat_1(X0,k2_relat_1(X0)) ),
inference(cnf_transformation,[],[f20814]) ).
fof(f35764,definition,
( spl1100_13
<=> r1_tarski(k1_funct_5(k9_relset_2(sK143,sK144,sK145,sK146,sK147)),k1_funct_5(sK146)) ),
introduced(definition,[new_symbols(definition,[spl1100_13])],[avatar_definition]) ).
fof(f35766,plain,
( ~ r1_tarski(k1_funct_5(k9_relset_2(sK143,sK144,sK145,sK146,sK147)),k1_funct_5(sK146))
| spl1100_13 ),
inference(avatar_component_clause,[],[f35764]) ).
fof(f35768,definition,
( spl1100_14
<=> k1_funct_5(k9_relset_2(sK143,sK144,sK145,sK146,sK147)) = k10_relset_1(sK144,sK143,k6_relset_1(sK143,sK144,sK146),k1_funct_5(sK147)) ),
introduced(definition,[new_symbols(definition,[spl1100_14])],[avatar_definition]) ).
fof(f35770,plain,
( k1_funct_5(k9_relset_2(sK143,sK144,sK145,sK146,sK147)) != k10_relset_1(sK144,sK143,k6_relset_1(sK143,sK144,sK146),k1_funct_5(sK147))
| spl1100_14 ),
inference(avatar_component_clause,[],[f35768]) ).
fof(f35771,plain,
( ~ spl1100_13
| ~ spl1100_14 ),
inference(avatar_split_clause,[],[f25783,f35768,f35764]) ).
fof(f36165,plain,
k1_funct_5(sK147) = k10_relset_1(sK145,sK144,k6_relset_1(sK144,sK145,sK147),sK145),
inference(resolution,[],[f25820,f25782]) ).
fof(f36176,plain,
m1_relset_1(sK146,sK143,sK144),
inference(resolution,[],[f26237,f25781]) ).
fof(f36177,plain,
! [X2,X0,X1] :
( m1_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(resolution,[],[f26237,f25828]) ).
fof(f36178,plain,
m1_relset_1(sK147,sK144,sK145),
inference(resolution,[],[f26237,f25782]) ).
fof(f36182,plain,
k6_relset_1(sK143,sK144,sK146) = k4_relat_1(sK146),
inference(resolution,[],[f36176,f25826]) ).
fof(f36186,plain,
( k1_funct_5(k9_relset_2(sK143,sK144,sK145,sK146,sK147)) != k10_relset_1(sK144,sK143,k4_relat_1(sK146),k1_funct_5(sK147))
| spl1100_14 ),
inference(superposition,[],[f35770,f36182]) ).
fof(f36187,plain,
( m2_relset_1(k4_relat_1(sK146),sK144,sK143)
| ~ m1_relset_1(sK146,sK143,sK144) ),
inference(superposition,[],[f25828,f36182]) ).
fof(f36188,plain,
m2_relset_1(k4_relat_1(sK146),sK144,sK143),
inference(forward_subsumption_resolution,[],[f36187,f36176]) ).
fof(f36189,plain,
m1_relset_1(k4_relat_1(sK146),sK144,sK143),
inference(resolution,[],[f36188,f26237]) ).
fof(f36237,plain,
k6_relset_1(sK144,sK145,sK147) = k4_relat_1(sK147),
inference(resolution,[],[f36178,f25826]) ).
fof(f36240,plain,
k1_funct_5(sK147) = k10_relset_1(sK145,sK144,k4_relat_1(sK147),sK145),
inference(superposition,[],[f36165,f36237]) ).
fof(f36241,plain,
( m2_relset_1(k4_relat_1(sK147),sK145,sK144)
| ~ m1_relset_1(sK147,sK144,sK145) ),
inference(superposition,[],[f25828,f36237]) ).
fof(f36242,plain,
m2_relset_1(k4_relat_1(sK147),sK145,sK144),
inference(forward_subsumption_resolution,[],[f36241,f36178]) ).
fof(f36243,plain,
m1_relset_1(k4_relat_1(sK147),sK145,sK144),
inference(resolution,[],[f36242,f26237]) ).
fof(f36255,plain,
! [X2,X3,X0,X1,X4] :
( m1_relset_1(k9_relset_2(X1,X2,X4,X0,X3),X1,X4)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X2,X4)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(resolution,[],[f25858,f26237]) ).
fof(f36259,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X1,X0)
| k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0) = k2_funct_5(k6_relset_1(X1,X0,X2)) ),
inference(resolution,[],[f25819,f25828]) ).
fof(f36298,plain,
! [X0] : k10_relset_1(sK144,sK143,k4_relat_1(sK146),X0) = k9_relat_1(k4_relat_1(sK146),X0),
inference(resolution,[],[f25844,f36189]) ).
fof(f36299,plain,
! [X0] : k10_relset_1(sK145,sK144,k4_relat_1(sK147),X0) = k9_relat_1(k4_relat_1(sK147),X0),
inference(resolution,[],[f25844,f36243]) ).
fof(f36316,plain,
k1_funct_5(sK147) = k9_relat_1(k4_relat_1(sK147),sK145),
inference(superposition,[],[f36240,f36299]) ).
fof(f36323,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X4,X1)))
| ~ m2_relset_1(X0,X1,X2)
| k5_relat_1(X3,X0) = k9_relset_2(X4,X1,X2,X3,X0) ),
inference(resolution,[],[f26320,f25857]) ).
fof(f36326,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X3,X4,X1)
| k5_relat_1(X3,X0) = k9_relset_2(X4,X1,X2,X3,X0)
| ~ m2_relset_1(X0,X1,X2) ),
inference(resolution,[],[f36323,f26320]) ).
fof(f36344,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,sK144,X1)
| k5_relat_1(sK146,X0) = k9_relset_2(sK143,sK144,X1,sK146,X0) ),
inference(resolution,[],[f36326,f25781]) ).
fof(f36352,plain,
k9_relset_2(sK143,sK144,sK145,sK146,sK147) = k5_relat_1(sK146,sK147),
inference(resolution,[],[f36344,f25782]) ).
fof(f36353,plain,
( k10_relset_1(sK144,sK143,k4_relat_1(sK146),k1_funct_5(sK147)) != k1_funct_5(k5_relat_1(sK146,sK147))
| spl1100_14 ),
inference(superposition,[],[f36186,f36352]) ).
fof(f36354,plain,
( m2_relset_1(k5_relat_1(sK146,sK147),sK143,sK145)
| ~ m1_subset_1(sK146,k1_zfmisc_1(k2_zfmisc_1(sK143,sK144)))
| ~ m1_subset_1(sK147,k1_zfmisc_1(k2_zfmisc_1(sK144,sK145))) ),
inference(superposition,[],[f25858,f36352]) ).
fof(f36356,definition,
( spl1100_32
<=> m1_subset_1(sK147,k1_zfmisc_1(k2_zfmisc_1(sK144,sK145))) ),
introduced(definition,[new_symbols(definition,[spl1100_32])],[avatar_definition]) ).
fof(f36357,plain,
( m1_subset_1(sK147,k1_zfmisc_1(k2_zfmisc_1(sK144,sK145)))
| ~ spl1100_32 ),
inference(avatar_component_clause,[],[f36356]) ).
fof(f36358,plain,
( ~ m1_subset_1(sK147,k1_zfmisc_1(k2_zfmisc_1(sK144,sK145)))
| spl1100_32 ),
inference(avatar_component_clause,[],[f36356]) ).
fof(f36360,definition,
( spl1100_33
<=> m1_subset_1(sK146,k1_zfmisc_1(k2_zfmisc_1(sK143,sK144))) ),
introduced(definition,[new_symbols(definition,[spl1100_33])],[avatar_definition]) ).
fof(f36361,plain,
( m1_subset_1(sK146,k1_zfmisc_1(k2_zfmisc_1(sK143,sK144)))
| ~ spl1100_33 ),
inference(avatar_component_clause,[],[f36360]) ).
fof(f36362,plain,
( ~ m1_subset_1(sK146,k1_zfmisc_1(k2_zfmisc_1(sK143,sK144)))
| spl1100_33 ),
inference(avatar_component_clause,[],[f36360]) ).
fof(f36364,definition,
( spl1100_34
<=> m2_relset_1(k5_relat_1(sK146,sK147),sK143,sK145) ),
introduced(definition,[new_symbols(definition,[spl1100_34])],[avatar_definition]) ).
fof(f36366,plain,
( m2_relset_1(k5_relat_1(sK146,sK147),sK143,sK145)
| ~ spl1100_34 ),
inference(avatar_component_clause,[],[f36364]) ).
fof(f36367,plain,
( ~ spl1100_32
| ~ spl1100_33
| spl1100_34 ),
inference(avatar_split_clause,[],[f36354,f36364,f36360,f36356]) ).
fof(f36368,plain,
( k1_funct_5(k5_relat_1(sK146,sK147)) != k9_relat_1(k4_relat_1(sK146),k1_funct_5(sK147))
| spl1100_14 ),
inference(forward_demodulation,[],[f36353,f36298]) ).
fof(f36369,plain,
( ~ m2_relset_1(sK147,sK144,sK145)
| spl1100_32 ),
inference(resolution,[],[f36358,f26320]) ).
fof(f36370,plain,
( $false
| spl1100_32 ),
inference(forward_subsumption_resolution,[],[f36369,f25782]) ).
fof(f36371,plain,
spl1100_32,
inference(avatar_contradiction_clause,[],[f36370]) ).
fof(f36376,plain,
( ~ m2_relset_1(sK146,sK143,sK144)
| spl1100_33 ),
inference(resolution,[],[f36362,f26320]) ).
fof(f36377,plain,
( $false
| spl1100_33 ),
inference(forward_subsumption_resolution,[],[f36376,f25781]) ).
fof(f36378,plain,
spl1100_33,
inference(avatar_contradiction_clause,[],[f36377]) ).
fof(f36386,plain,
( m1_relset_1(k5_relat_1(sK146,sK147),sK143,sK145)
| ~ spl1100_34 ),
inference(resolution,[],[f36366,f26237]) ).
fof(f36387,plain,
( k1_funct_5(k5_relat_1(sK146,sK147)) = k10_relset_1(sK145,sK143,k6_relset_1(sK143,sK145,k5_relat_1(sK146,sK147)),sK145)
| ~ spl1100_34 ),
inference(resolution,[],[f36366,f25820]) ).
fof(f36388,plain,
( k10_relset_1(sK145,sK143,k6_relset_1(sK143,sK145,k5_relat_1(sK146,sK147)),sK145) = k2_funct_5(k6_relset_1(sK143,sK145,k5_relat_1(sK146,sK147)))
| ~ spl1100_34 ),
inference(resolution,[],[f36386,f36259]) ).
fof(f36393,plain,
( k6_relset_1(sK143,sK145,k5_relat_1(sK146,sK147)) = k4_relat_1(k5_relat_1(sK146,sK147))
| ~ spl1100_34 ),
inference(resolution,[],[f36386,f25826]) ).
fof(f36396,plain,
( k10_relset_1(sK145,sK143,k4_relat_1(k5_relat_1(sK146,sK147)),sK145) = k2_funct_5(k4_relat_1(k5_relat_1(sK146,sK147)))
| ~ spl1100_34 ),
inference(forward_demodulation,[],[f36388,f36393]) ).
fof(f36455,plain,
( k1_funct_5(k5_relat_1(sK146,sK147)) = k10_relset_1(sK145,sK143,k4_relat_1(k5_relat_1(sK146,sK147)),sK145)
| ~ spl1100_34 ),
inference(superposition,[],[f36387,f36393]) ).
fof(f36459,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X0,X1,X2)
| k10_relset_1(X2,X1,k6_relset_1(X1,X2,X0),X3) = k9_relat_1(k6_relset_1(X1,X2,X0),X3) ),
inference(resolution,[],[f36177,f25844]) ).
fof(f36488,definition,
( spl1100_41
<=> m1_subset_1(k4_relat_1(sK146),k1_zfmisc_1(k2_zfmisc_1(sK144,sK143))) ),
introduced(definition,[new_symbols(definition,[spl1100_41])],[avatar_definition]) ).
fof(f36489,plain,
( m1_subset_1(k4_relat_1(sK146),k1_zfmisc_1(k2_zfmisc_1(sK144,sK143)))
| ~ spl1100_41 ),
inference(avatar_component_clause,[],[f36488]) ).
fof(f36490,plain,
( ~ m1_subset_1(k4_relat_1(sK146),k1_zfmisc_1(k2_zfmisc_1(sK144,sK143)))
| spl1100_41 ),
inference(avatar_component_clause,[],[f36488]) ).
fof(f36496,plain,
( ~ m2_relset_1(k4_relat_1(sK146),sK144,sK143)
| spl1100_41 ),
inference(resolution,[],[f36490,f26320]) ).
fof(f36497,plain,
( $false
| spl1100_41 ),
inference(forward_subsumption_resolution,[],[f36496,f36188]) ).
fof(f36498,plain,
spl1100_41,
inference(avatar_contradiction_clause,[],[f36497]) ).
fof(f36523,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,sK144)))
| k9_relset_2(X1,sK144,sK143,X0,k4_relat_1(sK146)) = k5_relat_1(X0,k4_relat_1(sK146)) )
| ~ spl1100_41 ),
inference(resolution,[],[f36489,f25857]) ).
fof(f36551,definition,
( spl1100_45
<=> v1_relat_1(k4_relat_1(sK147)) ),
introduced(definition,[new_symbols(definition,[spl1100_45])],[avatar_definition]) ).
fof(f36552,plain,
( v1_relat_1(k4_relat_1(sK147))
| ~ spl1100_45 ),
inference(avatar_component_clause,[],[f36551]) ).
fof(f36553,plain,
( ~ v1_relat_1(k4_relat_1(sK147))
| spl1100_45 ),
inference(avatar_component_clause,[],[f36551]) ).
fof(f36559,definition,
( spl1100_47
<=> v1_relat_1(k4_relat_1(sK146)) ),
introduced(definition,[new_symbols(definition,[spl1100_47])],[avatar_definition]) ).
fof(f36560,plain,
( v1_relat_1(k4_relat_1(sK146))
| ~ spl1100_47 ),
inference(avatar_component_clause,[],[f36559]) ).
fof(f36561,plain,
( ~ v1_relat_1(k4_relat_1(sK146))
| spl1100_47 ),
inference(avatar_component_clause,[],[f36559]) ).
fof(f36567,definition,
( spl1100_49
<=> v1_relat_1(sK147) ),
introduced(definition,[new_symbols(definition,[spl1100_49])],[avatar_definition]) ).
fof(f36568,plain,
( v1_relat_1(sK147)
| ~ spl1100_49 ),
inference(avatar_component_clause,[],[f36567]) ).
fof(f36569,plain,
( ~ v1_relat_1(sK147)
| spl1100_49 ),
inference(avatar_component_clause,[],[f36567]) ).
fof(f36575,definition,
( spl1100_51
<=> v1_relat_1(sK146) ),
introduced(definition,[new_symbols(definition,[spl1100_51])],[avatar_definition]) ).
fof(f36576,plain,
( v1_relat_1(sK146)
| ~ spl1100_51 ),
inference(avatar_component_clause,[],[f36575]) ).
fof(f36577,plain,
( ~ v1_relat_1(sK146)
| spl1100_51 ),
inference(avatar_component_clause,[],[f36575]) ).
fof(f36655,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f26321,f26320]) ).
fof(f36656,plain,
( v1_relat_1(k4_relat_1(sK146))
| ~ spl1100_41 ),
inference(resolution,[],[f26321,f36489]) ).
fof(f36658,plain,
( v1_relat_1(sK146)
| ~ spl1100_33 ),
inference(resolution,[],[f26321,f36361]) ).
fof(f36659,plain,
( v1_relat_1(sK147)
| ~ spl1100_32 ),
inference(resolution,[],[f26321,f36357]) ).
fof(f36660,plain,
( $false
| ~ spl1100_32
| spl1100_49 ),
inference(forward_subsumption_resolution,[],[f36659,f36569]) ).
fof(f36661,plain,
( ~ spl1100_32
| spl1100_49 ),
inference(avatar_contradiction_clause,[],[f36660]) ).
fof(f36662,plain,
( $false
| ~ spl1100_33
| spl1100_51 ),
inference(forward_subsumption_resolution,[],[f36658,f36577]) ).
fof(f36663,plain,
( ~ spl1100_33
| spl1100_51 ),
inference(avatar_contradiction_clause,[],[f36662]) ).
fof(f36664,plain,
( $false
| ~ spl1100_41
| spl1100_47 ),
inference(forward_subsumption_resolution,[],[f36656,f36561]) ).
fof(f36665,plain,
( ~ spl1100_41
| spl1100_47 ),
inference(avatar_contradiction_clause,[],[f36664]) ).
fof(f36666,plain,
( v1_relat_1(k5_relat_1(sK146,sK147))
| ~ spl1100_34 ),
inference(resolution,[],[f36655,f36366]) ).
fof(f36670,plain,
v1_relat_1(k4_relat_1(sK147)),
inference(resolution,[],[f36655,f36242]) ).
fof(f36675,plain,
( $false
| spl1100_45 ),
inference(forward_subsumption_resolution,[],[f36670,f36553]) ).
fof(f36676,plain,
spl1100_45,
inference(avatar_contradiction_clause,[],[f36675]) ).
fof(f36693,definition,
( spl1100_61
<=> m1_subset_1(k4_relat_1(sK147),k1_zfmisc_1(k2_zfmisc_1(sK145,sK144))) ),
introduced(definition,[new_symbols(definition,[spl1100_61])],[avatar_definition]) ).
fof(f36694,plain,
( m1_subset_1(k4_relat_1(sK147),k1_zfmisc_1(k2_zfmisc_1(sK145,sK144)))
| ~ spl1100_61 ),
inference(avatar_component_clause,[],[f36693]) ).
fof(f36695,plain,
( ~ m1_subset_1(k4_relat_1(sK147),k1_zfmisc_1(k2_zfmisc_1(sK145,sK144)))
| spl1100_61 ),
inference(avatar_component_clause,[],[f36693]) ).
fof(f36701,plain,
( ~ m2_relset_1(k4_relat_1(sK147),sK145,sK144)
| spl1100_61 ),
inference(resolution,[],[f36695,f26320]) ).
fof(f36702,plain,
( $false
| spl1100_61 ),
inference(forward_subsumption_resolution,[],[f36701,f36242]) ).
fof(f36703,plain,
spl1100_61,
inference(avatar_contradiction_clause,[],[f36702]) ).
fof(f36704,plain,
( k9_relset_2(sK145,sK144,sK143,k4_relat_1(sK147),k4_relat_1(sK146)) = k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146))
| ~ spl1100_41
| ~ spl1100_61 ),
inference(resolution,[],[f36694,f36523]) ).
fof(f36739,plain,
( m2_relset_1(k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)),sK145,sK143)
| ~ m1_subset_1(k4_relat_1(sK147),k1_zfmisc_1(k2_zfmisc_1(sK145,sK144)))
| ~ m1_subset_1(k4_relat_1(sK146),k1_zfmisc_1(k2_zfmisc_1(sK144,sK143)))
| ~ spl1100_41
| ~ spl1100_61 ),
inference(superposition,[],[f25858,f36704]) ).
fof(f36740,plain,
( m2_relset_1(k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)),sK145,sK143)
| ~ m1_subset_1(k4_relat_1(sK146),k1_zfmisc_1(k2_zfmisc_1(sK144,sK143)))
| ~ spl1100_41
| ~ spl1100_61 ),
inference(forward_subsumption_resolution,[],[f36739,f36694]) ).
fof(f36741,plain,
( m2_relset_1(k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)),sK145,sK143)
| ~ spl1100_41
| ~ spl1100_61 ),
inference(forward_subsumption_resolution,[],[f36740,f36489]) ).
fof(f36799,plain,
( k1_funct_5(sK147) = k1_relat_1(sK147)
| ~ spl1100_49 ),
inference(resolution,[],[f25917,f36568]) ).
fof(f36800,plain,
( k1_funct_5(sK146) = k1_relat_1(sK146)
| ~ spl1100_51 ),
inference(resolution,[],[f25917,f36576]) ).
fof(f36805,plain,
( k1_funct_5(k5_relat_1(sK146,sK147)) != k9_relat_1(k4_relat_1(sK146),k1_relat_1(sK147))
| spl1100_14
| ~ spl1100_49 ),
inference(superposition,[],[f36368,f36799]) ).
fof(f37048,plain,
( ! [X0] : k10_relset_1(sK145,sK143,k6_relset_1(sK143,sK145,k5_relat_1(sK146,sK147)),X0) = k9_relat_1(k6_relset_1(sK143,sK145,k5_relat_1(sK146,sK147)),X0)
| ~ spl1100_34 ),
inference(resolution,[],[f36459,f36386]) ).
fof(f37064,plain,
( ! [X0] : k10_relset_1(sK145,sK143,k4_relat_1(k5_relat_1(sK146,sK147)),X0) = k9_relat_1(k4_relat_1(k5_relat_1(sK146,sK147)),X0)
| ~ spl1100_34 ),
inference(forward_demodulation,[],[f37048,f36393]) ).
fof(f37095,plain,
( k1_funct_5(k5_relat_1(sK146,sK147)) = k1_relat_1(k5_relat_1(sK146,sK147))
| ~ spl1100_34 ),
inference(resolution,[],[f36666,f25917]) ).
fof(f37536,plain,
( k1_funct_5(k5_relat_1(sK146,sK147)) = k9_relat_1(k4_relat_1(k5_relat_1(sK146,sK147)),sK145)
| ~ spl1100_34 ),
inference(superposition,[],[f36455,f37064]) ).
fof(f37541,plain,
( k1_relat_1(k5_relat_1(sK146,sK147)) = k9_relat_1(k4_relat_1(k5_relat_1(sK146,sK147)),sK145)
| ~ spl1100_34 ),
inference(forward_demodulation,[],[f37536,f37095]) ).
fof(f37655,plain,
( ! [X0,X1] :
( ~ v1_relat_1(X0)
| k9_relat_1(k5_relat_1(X0,k4_relat_1(sK146)),X1) = k9_relat_1(k4_relat_1(sK146),k9_relat_1(X0,X1)) )
| ~ spl1100_47 ),
inference(resolution,[],[f26703,f36560]) ).
fof(f37747,plain,
( k2_funct_5(k4_relat_1(k5_relat_1(sK146,sK147))) = k9_relat_1(k4_relat_1(k5_relat_1(sK146,sK147)),sK145)
| ~ spl1100_34 ),
inference(superposition,[],[f37064,f36396]) ).
fof(f37752,plain,
( k2_funct_5(k4_relat_1(k5_relat_1(sK146,sK147))) = k1_relat_1(k5_relat_1(sK146,sK147))
| ~ spl1100_34 ),
inference(forward_demodulation,[],[f37747,f37541]) ).
fof(f37758,plain,
( ! [X0] : k9_relat_1(k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)),X0) = k9_relat_1(k4_relat_1(sK146),k9_relat_1(k4_relat_1(sK147),X0))
| ~ spl1100_45
| ~ spl1100_47 ),
inference(resolution,[],[f37655,f36552]) ).
fof(f37844,plain,
( m1_relset_1(k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)),sK145,sK143)
| ~ m1_subset_1(k4_relat_1(sK146),k1_zfmisc_1(k2_zfmisc_1(sK144,sK143)))
| ~ m1_subset_1(k4_relat_1(sK147),k1_zfmisc_1(k2_zfmisc_1(sK145,sK144)))
| ~ spl1100_41
| ~ spl1100_61 ),
inference(superposition,[],[f36255,f36704]) ).
fof(f37846,plain,
( m1_relset_1(k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)),sK145,sK143)
| ~ m1_subset_1(k4_relat_1(sK147),k1_zfmisc_1(k2_zfmisc_1(sK145,sK144)))
| ~ spl1100_41
| ~ spl1100_61 ),
inference(forward_subsumption_resolution,[],[f37844,f36489]) ).
fof(f37848,plain,
( m1_relset_1(k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)),sK145,sK143)
| ~ spl1100_41
| ~ spl1100_61 ),
inference(forward_subsumption_resolution,[],[f37846,f36694]) ).
fof(f38412,plain,
( k1_relat_1(sK146) = k10_relat_1(sK146,k2_relat_1(sK146))
| ~ spl1100_51 ),
inference(resolution,[],[f28335,f36576]) ).
fof(f39373,plain,
( k10_relset_1(sK145,sK143,k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)),sK145) = k2_funct_5(k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)))
| ~ spl1100_41
| ~ spl1100_61 ),
inference(resolution,[],[f36741,f25819]) ).
fof(f39823,plain,
( ! [X0] :
( ~ v1_relat_1(X0)
| k10_relat_1(X0,k1_relat_1(sK147)) = k1_relat_1(k5_relat_1(X0,sK147)) )
| ~ spl1100_49 ),
inference(resolution,[],[f28321,f36568]) ).
fof(f39871,plain,
( k1_relat_1(k5_relat_1(sK146,sK147)) = k10_relat_1(sK146,k1_relat_1(sK147))
| ~ spl1100_49
| ~ spl1100_51 ),
inference(resolution,[],[f39823,f36576]) ).
fof(f40322,plain,
( r1_tarski(k1_relat_1(k5_relat_1(sK146,sK147)),k10_relat_1(sK146,k2_relat_1(sK146)))
| ~ v1_relat_1(sK146)
| ~ spl1100_49
| ~ spl1100_51 ),
inference(superposition,[],[f28334,f39871]) ).
fof(f40354,plain,
( r1_tarski(k1_relat_1(k5_relat_1(sK146,sK147)),k10_relat_1(sK146,k2_relat_1(sK146)))
| ~ spl1100_49
| ~ spl1100_51 ),
inference(forward_subsumption_resolution,[],[f40322,f36576]) ).
fof(f40372,plain,
( r1_tarski(k1_relat_1(k5_relat_1(sK146,sK147)),k1_relat_1(sK146))
| ~ spl1100_49
| ~ spl1100_51 ),
inference(forward_demodulation,[],[f40354,f38412]) ).
fof(f44785,plain,
( ! [X0] : k9_relat_1(k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)),X0) = k10_relset_1(sK145,sK143,k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)),X0)
| ~ spl1100_41
| ~ spl1100_61 ),
inference(resolution,[],[f37848,f25844]) ).
fof(f44805,plain,
( ! [X0] : k9_relat_1(k4_relat_1(sK146),k9_relat_1(k4_relat_1(sK147),X0)) = k10_relset_1(sK145,sK143,k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)),X0)
| ~ spl1100_41
| ~ spl1100_45
| ~ spl1100_47
| ~ spl1100_61 ),
inference(forward_demodulation,[],[f44785,f37758]) ).
fof(f44813,plain,
( k2_funct_5(k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146))) = k9_relat_1(k4_relat_1(sK146),k9_relat_1(k4_relat_1(sK147),sK145))
| ~ spl1100_41
| ~ spl1100_45
| ~ spl1100_47
| ~ spl1100_61 ),
inference(superposition,[],[f39373,f44805]) ).
fof(f44816,plain,
( k9_relat_1(k4_relat_1(sK146),k1_funct_5(sK147)) = k2_funct_5(k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)))
| ~ spl1100_41
| ~ spl1100_45
| ~ spl1100_47
| ~ spl1100_61 ),
inference(forward_demodulation,[],[f44813,f36316]) ).
fof(f44818,plain,
( k9_relat_1(k4_relat_1(sK146),k1_relat_1(sK147)) = k2_funct_5(k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146)))
| ~ spl1100_41
| ~ spl1100_45
| ~ spl1100_47
| ~ spl1100_49
| ~ spl1100_61 ),
inference(forward_demodulation,[],[f44816,f36799]) ).
fof(f44829,plain,
( ! [X0] :
( ~ v1_relat_1(X0)
| k4_relat_1(k5_relat_1(X0,sK147)) = k5_relat_1(k4_relat_1(sK147),k4_relat_1(X0)) )
| ~ spl1100_49 ),
inference(resolution,[],[f26213,f36568]) ).
fof(f44883,plain,
( k4_relat_1(k5_relat_1(sK146,sK147)) = k5_relat_1(k4_relat_1(sK147),k4_relat_1(sK146))
| ~ spl1100_49
| ~ spl1100_51 ),
inference(resolution,[],[f44829,f36576]) ).
fof(f44899,plain,
( k2_funct_5(k4_relat_1(k5_relat_1(sK146,sK147))) = k9_relat_1(k4_relat_1(sK146),k1_relat_1(sK147))
| ~ spl1100_41
| ~ spl1100_45
| ~ spl1100_47
| ~ spl1100_49
| ~ spl1100_51
| ~ spl1100_61 ),
inference(superposition,[],[f44818,f44883]) ).
fof(f44900,plain,
( k9_relat_1(k4_relat_1(sK146),k1_relat_1(sK147)) = k1_relat_1(k5_relat_1(sK146,sK147))
| ~ spl1100_34
| ~ spl1100_41
| ~ spl1100_45
| ~ spl1100_47
| ~ spl1100_49
| ~ spl1100_51
| ~ spl1100_61 ),
inference(forward_demodulation,[],[f44899,f37752]) ).
fof(f44931,plain,
( k1_funct_5(k5_relat_1(sK146,sK147)) != k1_relat_1(k5_relat_1(sK146,sK147))
| spl1100_14
| ~ spl1100_34
| ~ spl1100_41
| ~ spl1100_45
| ~ spl1100_47
| ~ spl1100_49
| ~ spl1100_51
| ~ spl1100_61 ),
inference(superposition,[],[f36805,f44900]) ).
fof(f44954,plain,
( $false
| spl1100_14
| ~ spl1100_34
| ~ spl1100_41
| ~ spl1100_45
| ~ spl1100_47
| ~ spl1100_49
| ~ spl1100_51
| ~ spl1100_61 ),
inference(forward_subsumption_resolution,[],[f44931,f37095]) ).
fof(f44955,plain,
( spl1100_14
| ~ spl1100_34
| ~ spl1100_41
| ~ spl1100_45
| ~ spl1100_47
| ~ spl1100_49
| ~ spl1100_51
| ~ spl1100_61 ),
inference(avatar_contradiction_clause,[],[f44954]) ).
fof(f44962,plain,
( ~ r1_tarski(k1_funct_5(k9_relset_2(sK143,sK144,sK145,sK146,sK147)),k1_relat_1(sK146))
| spl1100_13
| ~ spl1100_51 ),
inference(forward_demodulation,[],[f35766,f36800]) ).
fof(f44964,plain,
( ~ r1_tarski(k1_funct_5(k5_relat_1(sK146,sK147)),k1_relat_1(sK146))
| spl1100_13
| ~ spl1100_51 ),
inference(forward_demodulation,[],[f44962,f36352]) ).
fof(f44966,plain,
( ~ r1_tarski(k1_relat_1(k5_relat_1(sK146,sK147)),k1_relat_1(sK146))
| spl1100_13
| ~ spl1100_34
| ~ spl1100_51 ),
inference(forward_demodulation,[],[f44964,f37095]) ).
fof(f44968,plain,
( $false
| spl1100_13
| ~ spl1100_34
| ~ spl1100_49
| ~ spl1100_51 ),
inference(forward_subsumption_resolution,[],[f44966,f40372]) ).
fof(f44969,plain,
( spl1100_13
| ~ spl1100_34
| ~ spl1100_49
| ~ spl1100_51 ),
inference(avatar_contradiction_clause,[],[f44968]) ).
cnf(s15,plain,
( ~ spl1100_13
| ~ spl1100_14 ),
inference(sat_conversion,[],[f35771]) ).
cnf(s30,plain,
( ~ spl1100_32
| ~ spl1100_33
| spl1100_34 ),
inference(sat_conversion,[],[f36367]) ).
cnf(s31,plain,
spl1100_32,
inference(sat_conversion,[],[f36371]) ).
cnf(s32,plain,
spl1100_33,
inference(sat_conversion,[],[f36378]) ).
cnf(s40,plain,
spl1100_41,
inference(sat_conversion,[],[f36498]) ).
cnf(s53,plain,
( ~ spl1100_32
| spl1100_49 ),
inference(sat_conversion,[],[f36661]) ).
cnf(s54,plain,
( ~ spl1100_33
| spl1100_51 ),
inference(sat_conversion,[],[f36663]) ).
cnf(s55,plain,
( ~ spl1100_41
| spl1100_47 ),
inference(sat_conversion,[],[f36665]) ).
cnf(s56,plain,
spl1100_45,
inference(sat_conversion,[],[f36676]) ).
cnf(s58,plain,
spl1100_61,
inference(sat_conversion,[],[f36703]) ).
cnf(s316,plain,
( spl1100_14
| ~ spl1100_34
| ~ spl1100_41
| ~ spl1100_45
| ~ spl1100_47
| ~ spl1100_49
| ~ spl1100_51
| ~ spl1100_61 ),
inference(sat_conversion,[],[f44955]) ).
cnf(s317,plain,
( spl1100_13
| ~ spl1100_34
| ~ spl1100_49
| ~ spl1100_51 ),
inference(sat_conversion,[],[f44969]) ).
cnf(s323,plain,
spl1100_47,
inference(rat,[],[s55,s40]) ).
cnf(s334,plain,
spl1100_51,
inference(rat,[],[s54,s32]) ).
cnf(s351,plain,
spl1100_49,
inference(rat,[],[s53,s31]) ).
cnf(s363,plain,
spl1100_34,
inference(rat,[],[s30,s32,s31]) ).
cnf(s364,plain,
spl1100_13,
inference(rat,[],[s317,s334,s351,s363]) ).
cnf(s365,plain,
spl1100_14,
inference(rat,[],[s316,s58,s334,s351,s323,s56,s40,s363]) ).
cnf(s377,plain,
$false,
inference(rat,[],[s15,s365,s364]) ).
fof(f44972,plain,
$false,
inference(avatar_sat_refutation,[],[s377]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU440+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.41 % Computer : n010.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Mon Sep 28 05:29:34 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.47 Running first-order theorem proving
% 0.15/0.47 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
% 26.29/5.86 % (1608553)Detected formulas, will run a generic FOF schedule.
% 26.29/5.86 % (1608563)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3635207106:s2a=on:i=139:gtg=position_2986 on theBenchmark for (2986ds/139Mi)
% 26.29/5.86 % (1608558)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=1873362366:i=141193_2986 on theBenchmark for (2986ds/141193Mi)
% 26.29/5.86 % (1608562)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2583508095:i=119:av=off:ss=axioms_2986 on theBenchmark for (2986ds/119Mi)
% 26.29/5.86 % (1608561)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=739213479:i=109:sd=1:ins=1:gsp=on:ss=axioms_2986 on theBenchmark for (2986ds/109Mi)
% 26.29/5.86 % (1608560)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=193617297:i=141695:sd=1:nm=32:gsp=on:ss=included_2986 on theBenchmark for (2986ds/141695Mi)
% 26.29/5.86 % (1608559)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=4166235944:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2986 on theBenchmark for (2986ds/134677Mi)
% 26.29/5.86 % (1608563)Instruction limit reached!
% 26.29/5.86 % (1608563)------------------------------
% 26.29/5.86 % (1608563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.29/5.86 % (1608563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.29/5.86 % (1608563)CaDiCaL version: 2.1.3
% 26.29/5.86 % (1608563)Termination reason: Instruction limit
% 26.29/5.86 % (1608563)Termination phase: Property scanning
% 26.29/5.86 % (1608563)Time elapsed: 0.063 s
% 26.29/5.86 % (1608563)Peak memory usage: 112 MB
% 26.29/5.86 % (1608563)Instructions burned: 140 (million)
% 26.29/5.86 % (1608564)dis-21_1_sil=8000:lcm=predicate:random_seed=73995149:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2986 on theBenchmark for (2986ds/129Mi)
% 26.29/5.86 % (1608561)Instruction limit reached!
% 26.29/5.86 % (1608561)------------------------------
% 26.29/5.86 % (1608561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.29/5.86 % (1608561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.29/5.86 % (1608561)CaDiCaL version: 2.1.3
% 26.29/5.86 % (1608561)Termination reason: Instruction limit
% 26.29/5.86 % (1608561)Termination phase: SInE selection
% 26.29/5.86 % (1608561)Time elapsed: 0.118 s
% 26.29/5.86 % (1608561)Peak memory usage: 112 MB
% 26.29/5.86 % (1608561)Instructions burned: 109 (million)
% 26.29/5.86 % (1608562)Instruction limit reached!
% 26.29/5.86 % (1608562)------------------------------
% 26.29/5.86 % (1608562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.29/5.86 % (1608562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.29/5.86 % (1608562)CaDiCaL version: 2.1.3
% 26.29/5.86 % (1608562)Termination reason: Instruction limit
% 26.29/5.86 % (1608562)Termination phase: SInE selection
% 26.29/5.86 % (1608562)Time elapsed: 0.133 s
% 26.29/5.86 % (1608562)Peak memory usage: 112 MB
% 26.29/5.86 % (1608562)Instructions burned: 120 (million)
% 26.29/5.86 % (1608564)Instruction limit reached!
% 26.29/5.86 % (1608564)------------------------------
% 26.29/5.86 % (1608564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.29/5.86 % (1608564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.29/5.86 % (1608564)CaDiCaL version: 2.1.3
% 26.29/5.86 % (1608564)Termination reason: Instruction limit
% 26.29/5.86 % (1608564)Termination phase: SInE selection
% 26.29/5.86 % (1608564)Time elapsed: 0.134 s
% 26.29/5.86 % (1608564)Peak memory usage: 112 MB
% 26.29/5.86 % (1608564)Instructions burned: 129 (million)
% 26.29/5.86 % (1608571)lrs+10_1_sil=8000:sp=occurrence:random_seed=2504389395:i=285:sd=3:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/285Mi)
% 26.29/5.86 % (1608573)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2479630286:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/157Mi)
% 26.29/5.86 % (1608575)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=1855521197:s2a=on:i=248:s2at=1.23:gtg=position_2982 on theBenchmark for (2982ds/248Mi)
% 26.29/5.86 % (1608574)lrs+1011_1_sil=32000:sp=occurrence:random_seed=53595820:i=325:sd=1:ss=axioms:sgt=32_2982 on theBenchmark for (2982ds/325Mi)
% 26.29/5.86 % (1608573)Instruction limit reached!
% 37.19/7.47 % (1608573)------------------------------
% 37.19/7.47 % (1608573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.19/7.47 % (1608573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.19/7.47 % (1608573)CaDiCaL version: 2.1.3
% 37.19/7.47 % (1608573)Termination reason: Instruction limit
% 37.19/7.47 % (1608573)Termination phase: Property scanning
% 37.19/7.47 % (1608573)Time elapsed: 0.070 s
% 37.19/7.47 % (1608573)Peak memory usage: 112 MB
% 37.19/7.47 % (1608573)Instructions burned: 158 (million)
% 37.19/7.47 % (1608571)Instruction limit reached!
% 37.19/7.47 % (1608571)------------------------------
% 37.19/7.47 % (1608571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.19/7.47 % (1608571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.19/7.47 % (1608571)CaDiCaL version: 2.1.3
% 37.19/7.47 % (1608571)Termination reason: Instruction limit
% 37.19/7.47 % (1608571)Termination phase: Saturation
% 37.19/7.47 % (1608571)Time elapsed: 0.319 s
% 37.19/7.47 % (1608571)Peak memory usage: 119 MB
% 37.19/7.47 % (1608571)Instructions burned: 285 (million)
% 37.19/7.47 % (1608575)Instruction limit reached!
% 37.19/7.47 % (1608575)------------------------------
% 37.19/7.47 % (1608575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.19/7.47 % (1608575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.19/7.47 % (1608575)CaDiCaL version: 2.1.3
% 37.19/7.47 % (1608575)Termination reason: Instruction limit
% 37.19/7.47 % (1608575)Termination phase: Property scanning
% 37.19/7.47 % (1608575)Time elapsed: 0.218 s
% 37.19/7.47 % (1608575)Peak memory usage: 113 MB
% 37.19/7.47 % (1608575)Instructions burned: 248 (million)
% 37.19/7.47 % (1608580)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2306315298:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2980 on theBenchmark for (2980ds/294Mi)
% 37.19/7.47 % (1608574)Instruction limit reached!
% 37.19/7.47 % (1608574)------------------------------
% 37.19/7.47 % (1608574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.19/7.47 % (1608574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.19/7.47 % (1608574)CaDiCaL version: 2.1.3
% 37.19/7.47 % (1608574)Termination reason: Instruction limit
% 37.19/7.47 % (1608574)Termination phase: Saturation
% 37.19/7.47 % (1608574)Time elapsed: 0.371 s
% 37.19/7.47 % (1608574)Peak memory usage: 118 MB
% 37.19/7.47 % (1608574)Instructions burned: 326 (million)
% 37.19/7.47 % (1608580)Instruction limit reached!
% 37.19/7.47 % (1608580)------------------------------
% 37.19/7.47 % (1608580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.19/7.47 % (1608580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.19/7.47 % (1608580)CaDiCaL version: 2.1.3
% 37.19/7.47 % (1608580)Termination reason: Instruction limit
% 37.19/7.47 % (1608580)Termination phase: Property scanning
% 37.19/7.47 % (1608580)Time elapsed: 0.183 s
% 37.19/7.47 % (1608580)Peak memory usage: 118 MB
% 37.19/7.47 % (1608580)Instructions burned: 296 (million)
% 37.19/7.47 % (1608581)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=704633148:i=2350_2978 on theBenchmark for (2978ds/2350Mi)
% 37.19/7.47 % (1608582)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4024220674:cts=off:i=113:fsr=off:ss=included:sgt=4_2978 on theBenchmark for (2978ds/113Mi)
% 37.19/7.47 % (1608584)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3147659001:i=127:av=off:fsr=off:sup=off_2976 on theBenchmark for (2976ds/127Mi)
% 37.19/7.47 % (1608582)Instruction limit reached!
% 37.19/7.47 % (1608582)------------------------------
% 37.19/7.47 % (1608582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.19/7.47 % (1608582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.19/7.47 % (1608582)CaDiCaL version: 2.1.3
% 37.19/7.47 % (1608582)Termination reason: Instruction limit
% 37.19/7.47 % (1608582)Termination phase: SInE selection
% 37.19/7.47 % (1608582)Time elapsed: 0.127 s
% 37.19/7.47 % (1608582)Peak memory usage: 112 MB
% 37.19/7.47 % (1608582)Instructions burned: 113 (million)
% 37.19/7.47 % (1608585)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4197289468:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2975 on theBenchmark for (2975ds/114Mi)
% 37.19/7.47 % (1608585)Instruction limit reached!
% 37.19/7.47 % (1608585)------------------------------
% 37.19/7.47 % (1608585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.33/14.50 % (1608585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.33/14.50 % (1608585)CaDiCaL version: 2.1.3
% 87.33/14.50 % (1608585)Termination reason: Instruction limit
% 87.33/14.50 % (1608585)Termination phase: Property scanning
% 87.33/14.50 % (1608585)Time elapsed: 0.053 s
% 87.33/14.50 % (1608585)Peak memory usage: 112 MB
% 87.33/14.50 % (1608585)Instructions burned: 116 (million)
% 87.33/14.50 % (1608584)Instruction limit reached!
% 87.33/14.50 % (1608584)------------------------------
% 87.33/14.50 % (1608584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.33/14.50 % (1608584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.33/14.50 % (1608584)CaDiCaL version: 2.1.3
% 87.33/14.50 % (1608584)Termination reason: Instruction limit
% 87.33/14.50 % (1608584)Termination phase: Preprocessing 1
% 87.33/14.50 % (1608584)Time elapsed: 0.138 s
% 87.33/14.50 % (1608584)Peak memory usage: 113 MB
% 87.33/14.50 % (1608584)Instructions burned: 127 (million)
% 87.33/14.50 % (1608589)lrs+10_1_sil=8000:sp=occurrence:random_seed=3879836685:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2973 on theBenchmark for (2973ds/907Mi)
% 87.33/14.50 % (1608591)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=438878466:i=437:sd=1:aac=none:ss=included_2973 on theBenchmark for (2973ds/437Mi)
% 87.33/14.50 % (1608592)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3619477986:i=5202:ss=axioms:sgt=16_2973 on theBenchmark for (2973ds/5202Mi)
% 87.33/14.50 % (1608591)Instruction limit reached!
% 87.33/14.50 % (1608591)------------------------------
% 87.33/14.50 % (1608591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.33/14.50 % (1608591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.33/14.50 % (1608591)CaDiCaL version: 2.1.3
% 87.33/14.50 % (1608591)Termination reason: Instruction limit
% 87.33/14.50 % (1608591)Termination phase: Saturation
% 87.33/14.50 % (1608591)Time elapsed: 0.493 s
% 87.33/14.50 % (1608591)Peak memory usage: 121 MB
% 87.33/14.50 % (1608591)Instructions burned: 437 (million)
% 87.33/14.50 % (1608596)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3554520654:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2965 on theBenchmark for (2965ds/134Mi)
% 87.33/14.50 % (1608589)Instruction limit reached!
% 87.33/14.50 % (1608589)------------------------------
% 87.33/14.50 % (1608589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.33/14.50 % (1608589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.33/14.50 % (1608589)CaDiCaL version: 2.1.3
% 87.33/14.50 % (1608589)Termination reason: Instruction limit
% 87.33/14.50 % (1608589)Termination phase: Property scanning
% 87.33/14.50 % (1608589)Time elapsed: 0.931 s
% 87.33/14.50 % (1608589)Peak memory usage: 136 MB
% 87.33/14.50 % (1608589)Instructions burned: 908 (million)
% 87.33/14.50 % (1608596)Instruction limit reached!
% 87.33/14.50 % (1608596)------------------------------
% 87.33/14.50 % (1608596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.33/14.50 % (1608596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.33/14.50 % (1608596)CaDiCaL version: 2.1.3
% 87.33/14.50 % (1608596)Termination reason: Instruction limit
% 87.33/14.50 % (1608596)Termination phase: NewCNF
% 87.33/14.50 % (1608596)Time elapsed: 0.183 s
% 87.33/14.50 % (1608596)Peak memory usage: 114 MB
% 87.33/14.50 % (1608596)Instructions burned: 134 (million)
% 87.33/14.50 % (1608598)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1457343140:st=8:i=592:sd=3:ep=RST:ss=axioms_2961 on theBenchmark for (2961ds/592Mi)
% 87.33/14.50 % (1608599)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=236537873:st=3:i=13193:sd=3:ss=axioms_2960 on theBenchmark for (2960ds/13193Mi)
% 87.33/14.50 % (1608581)Instruction limit reached!
% 87.33/14.50 % (1608581)------------------------------
% 87.33/14.50 % (1608581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.33/14.50 % (1608581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.33/14.50 % (1608581)CaDiCaL version: 2.1.3
% 87.33/14.50 % (1608581)Termination reason: Instruction limit
% 87.33/14.50 % (1608581)Termination phase: Property scanning
% 87.33/14.50 % (1608581)Time elapsed: 2.235 s
% 87.33/14.50 % (1608581)Peak memory usage: 171 MB
% 87.33/14.50 % (1608581)Instructions burned: 2350 (million)
% 87.33/14.50 % (1608598)Instruction limit reached!
% 87.33/14.50 % (1608598)------------------------------
% 87.33/14.50 % (1608598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.31/18.98 % (1608598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.31/18.98 % (1608598)CaDiCaL version: 2.1.3
% 118.31/18.98 % (1608598)Termination reason: Instruction limit
% 118.31/18.98 % (1608598)Termination phase: Preprocessing 3
% 118.31/18.98 % (1608598)Time elapsed: 0.705 s
% 118.31/18.98 % (1608598)Peak memory usage: 134 MB
% 118.31/18.98 % (1608598)Instructions burned: 592 (million)
% 118.31/18.98 % (1608602)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=1065587113:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2953 on theBenchmark for (2953ds/125Mi)
% 118.31/18.98 % (1608602)Instruction limit reached!
% 118.31/18.98 % (1608602)------------------------------
% 118.31/18.98 % (1608602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.31/18.98 % (1608602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.31/18.98 % (1608602)CaDiCaL version: 2.1.3
% 118.31/18.98 % (1608602)Termination reason: Instruction limit
% 118.31/18.98 % (1608602)Termination phase: Property scanning
% 118.31/18.98 % (1608602)Time elapsed: 0.104 s
% 118.31/18.98 % (1608602)Peak memory usage: 112 MB
% 118.31/18.98 % (1608602)Instructions burned: 125 (million)
% 118.31/18.98 % (1608603)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1732172237:i=134:gtgl=5:slsql=off:gtg=exists_sym_2951 on theBenchmark for (2951ds/134Mi)
% 118.31/18.98 % (1608603)Instruction limit reached!
% 118.31/18.98 % (1608603)------------------------------
% 118.31/18.98 % (1608603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.31/18.98 % (1608603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.31/18.98 % (1608603)CaDiCaL version: 2.1.3
% 118.31/18.98 % (1608603)Termination reason: Instruction limit
% 118.31/18.98 % (1608603)Termination phase: Property scanning
% 118.31/18.98 % (1608603)Time elapsed: 0.112 s
% 118.31/18.98 % (1608603)Peak memory usage: 112 MB
% 118.31/18.98 % (1608603)Instructions burned: 134 (million)
% 118.31/18.98 % (1608605)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2463158453:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2949 on theBenchmark for (2949ds/141Mi)
% 118.31/18.98 % (1608605)Instruction limit reached!
% 118.31/18.98 % (1608605)------------------------------
% 118.31/18.98 % (1608605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.31/18.98 % (1608605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.31/18.98 % (1608605)CaDiCaL version: 2.1.3
% 118.31/18.98 % (1608605)Termination reason: Instruction limit
% 118.31/18.98 % (1608605)Termination phase: Saturation
% 118.31/18.98 % (1608605)Time elapsed: 0.177 s
% 118.31/18.98 % (1608605)Peak memory usage: 117 MB
% 118.31/18.98 % (1608605)Instructions burned: 141 (million)
% 118.31/18.98 % (1608607)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=86283272:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2947 on theBenchmark for (2947ds/431Mi)
% 118.31/18.98 % (1608609)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=3638559577:i=6060:aac=none:ins=25_2944 on theBenchmark for (2944ds/6060Mi)
% 118.31/18.98 % (1608607)Instruction limit reached!
% 118.31/18.98 % (1608607)------------------------------
% 118.31/18.98 % (1608607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.31/18.98 % (1608607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.31/18.98 % (1608607)CaDiCaL version: 2.1.3
% 118.31/18.98 % (1608607)Termination reason: Instruction limit
% 118.31/18.98 % (1608607)Termination phase: Saturation
% 118.31/18.98 % (1608607)Time elapsed: 0.446 s
% 118.31/18.98 % (1608607)Peak memory usage: 119 MB
% 118.31/18.98 % (1608607)Instructions burned: 431 (million)
% 118.31/18.98 % (1608614)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=692477908:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2940 on theBenchmark for (2940ds/150Mi)
% 118.31/18.98 % (1608614)Instruction limit reached!
% 118.31/18.98 % (1608614)------------------------------
% 118.31/18.98 % (1608614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.31/18.98 % (1608614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.31/18.98 % (1608614)CaDiCaL version: 2.1.3
% 118.31/18.98 % (1608614)Termination reason: Instruction limit
% 78.40/22.26 % (1608614)Termination phase: Preprocessing 1
% 78.40/22.26 % (1608614)Time elapsed: 0.192 s
% 78.40/22.26 % (1608614)Peak memory usage: 113 MB
% 78.40/22.26 % (1608614)Instructions burned: 150 (million)
% 78.40/22.26 % (1608592)Instruction limit reached!
% 78.40/22.26 % (1608592)------------------------------
% 78.40/22.26 % (1608592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608592)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608592)Termination reason: Instruction limit
% 78.40/22.26 % (1608592)Termination phase: Saturation
% 78.40/22.26 % (1608592)Time elapsed: 3.526 s
% 78.40/22.26 % (1608592)Peak memory usage: 582 MB
% 78.40/22.26 % (1608592)Instructions burned: 5205 (million)
% 78.40/22.26 % (1608616)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=327738947:i=14155:bd=all_2935 on theBenchmark for (2935ds/14155Mi)
% 78.40/22.26 % (1608617)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=474840677:i=667:av=off:fsr=off_2934 on theBenchmark for (2934ds/667Mi)
% 78.40/22.26 % (1608617)Instruction limit reached!
% 78.40/22.26 % (1608617)------------------------------
% 78.40/22.26 % (1608617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608617)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608617)Termination reason: Instruction limit
% 78.40/22.26 % (1608617)Termination phase: NewCNF
% 78.40/22.26 % (1608617)Time elapsed: 0.791 s
% 78.40/22.26 % (1608617)Peak memory usage: 149 MB
% 78.40/22.26 % (1608617)Instructions burned: 667 (million)
% 78.40/22.26 % (1608621)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=213548751:s2a=on:i=185:s2at=1.8:fdi=4_2924 on theBenchmark for (2924ds/185Mi)
% 78.40/22.26 % (1608621)Instruction limit reached!
% 78.40/22.26 % (1608621)------------------------------
% 78.40/22.26 % (1608621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608621)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608621)Termination reason: Instruction limit
% 78.40/22.26 % (1608621)Termination phase: SInE selection
% 78.40/22.26 % (1608621)Time elapsed: 0.166 s
% 78.40/22.26 % (1608621)Peak memory usage: 113 MB
% 78.40/22.26 % (1608621)Instructions burned: 185 (million)
% 78.40/22.26 % (1608624)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3595771774:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2920 on theBenchmark for (2920ds/193Mi)
% 78.40/22.26 % (1608624)Instruction limit reached!
% 78.40/22.26 % (1608624)------------------------------
% 78.40/22.26 % (1608624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608624)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608624)Termination reason: Instruction limit
% 78.40/22.26 % (1608624)Termination phase: SInE selection
% 78.40/22.26 % (1608624)Time elapsed: 0.246 s
% 78.40/22.26 % (1608624)Peak memory usage: 112 MB
% 78.40/22.26 % (1608624)Instructions burned: 194 (million)
% 78.40/22.26 % (1608626)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=276091431:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2915 on theBenchmark for (2915ds/4850Mi)
% 78.40/22.26 % (1608609)Instruction limit reached!
% 78.40/22.26 % (1608609)------------------------------
% 78.40/22.26 % (1608609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608609)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608609)Termination reason: Instruction limit
% 78.40/22.26 % (1608609)Termination phase: Saturation
% 78.40/22.26 % (1608609)Time elapsed: 6.985 s
% 78.40/22.26 % (1608609)Peak memory usage: 614 MB
% 78.40/22.26 % (1608609)Instructions burned: 6060 (million)
% 78.40/22.26 % (1608628)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3747874771:i=12111:sd=1:ss=included_2871 on theBenchmark for (2871ds/12111Mi)
% 78.40/22.26 % (1608626)Instruction limit reached!
% 78.40/22.26 % (1608626)------------------------------
% 78.40/22.26 % (1608626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608626)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608626)Termination reason: Instruction limit
% 78.40/22.26 % (1608626)Termination phase: Saturation
% 78.40/22.26 % (1608626)Time elapsed: 4.728 s
% 78.40/22.26 % (1608626)Peak memory usage: 222 MB
% 78.40/22.26 % (1608626)Instructions burned: 4851 (million)
% 78.40/22.26 % (1608630)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1718434774:i=319:kws=precedence:fsr=off_2864 on theBenchmark for (2864ds/319Mi)
% 78.40/22.26 % (1608630)Instruction limit reached!
% 78.40/22.26 % (1608630)------------------------------
% 78.40/22.26 % (1608630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608630)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608630)Termination reason: Instruction limit
% 78.40/22.26 % (1608630)Termination phase: Naming
% 78.40/22.26 % (1608630)Time elapsed: 0.399 s
% 78.40/22.26 % (1608630)Peak memory usage: 135 MB
% 78.40/22.26 % (1608630)Instructions burned: 319 (million)
% 78.40/22.26 % (1608632)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1348240763:i=2064:ep=RST_2857 on theBenchmark for (2857ds/2064Mi)
% 78.40/22.26 % (1608616)Instruction limit reached!
% 78.40/22.26 % (1608616)------------------------------
% 78.40/22.26 % (1608616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608616)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608616)Termination reason: Instruction limit
% 78.40/22.26 % (1608616)Termination phase: Saturation
% 78.40/22.26 % (1608616)Time elapsed: 8.539 s
% 78.40/22.26 % (1608616)Peak memory usage: 503 MB
% 78.40/22.26 % (1608616)Instructions burned: 14157 (million)
% 78.40/22.26 % (1608634)dis-1011_128_sil=32000:random_seed=1716051560:i=3706:ep=RST:av=off_2847 on theBenchmark for (2847ds/3706Mi)
% 78.40/22.26 % (1608632)Instruction limit reached!
% 78.40/22.26 % (1608632)------------------------------
% 78.40/22.26 % (1608632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608632)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608632)Termination reason: Instruction limit
% 78.40/22.26 % (1608632)Termination phase: Property scanning
% 78.40/22.26 % (1608632)Time elapsed: 1.847 s
% 78.40/22.26 % (1608632)Peak memory usage: 171 MB
% 78.40/22.26 % (1608632)Instructions burned: 2065 (million)
% 78.40/22.26 % (1608638)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1571911139:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2836 on theBenchmark for (2836ds/757Mi)
% 78.40/22.26 % (1608634)Instruction limit reached!
% 78.40/22.26 % (1608634)------------------------------
% 78.40/22.26 % (1608634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608634)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608634)Termination reason: Instruction limit
% 78.40/22.26 % (1608634)Termination phase: Saturation
% 78.40/22.26 % (1608634)Time elapsed: 1.742 s
% 78.40/22.26 % (1608634)Peak memory usage: 186 MB
% 78.40/22.26 % (1608634)Instructions burned: 3708 (million)
% 78.40/22.26 % (1608638)Instruction limit reached!
% 78.40/22.26 % (1608638)------------------------------
% 78.40/22.26 % (1608638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608638)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608638)Termination reason: Instruction limit
% 78.40/22.26 % (1608638)Termination phase: Saturation
% 78.40/22.26 % (1608638)Time elapsed: 0.824 s
% 78.40/22.26 % (1608638)Peak memory usage: 126 MB
% 78.40/22.26 % (1608638)Instructions burned: 758 (million)
% 78.40/22.26 % (1608640)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3615855746:i=13913:ss=axioms:sgt=8_2827 on theBenchmark for (2827ds/13913Mi)
% 78.40/22.26 % (1608641)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3831237575:i=9925:aac=none_2826 on theBenchmark for (2826ds/9925Mi)
% 78.40/22.26 % (1608599)Instruction limit reached!
% 78.40/22.26 % (1608599)------------------------------
% 78.40/22.26 % (1608599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608599)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608599)Termination reason: Instruction limit
% 78.40/22.26 % (1608599)Termination phase: Saturation
% 78.40/22.26 % (1608599)Time elapsed: 13.751 s
% 78.40/22.26 % (1608599)Peak memory usage: 336 MB
% 78.40/22.26 % (1608599)Instructions burned: 13193 (million)
% 78.40/22.26 % (1608644)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2107217191:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2819 on theBenchmark for (2819ds/2479Mi)
% 78.40/22.26 % (1608640)First to succeed.
% 78.40/22.26 % (1608640)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1608553"
% 78.40/22.26 % (1608644)Instruction limit reached!
% 78.40/22.26 % (1608644)------------------------------
% 78.40/22.26 % (1608644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.40/22.26 % (1608644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.40/22.26 % (1608644)CaDiCaL version: 2.1.3
% 78.40/22.26 % (1608644)Termination reason: Instruction limit
% 78.40/22.26 % (1608644)Termination phase: Saturation
% 78.40/22.26 % (1608644)Time elapsed: 2.602 s
% 78.40/22.26 % (1608644)Peak memory usage: 136 MB
% 78.40/22.26 % (1608644)Instructions burned: 2479 (million)
% 78.40/22.26 % (1608640)Refutation found. Thanks to Tanya!
% 78.40/22.26 % SZS status Theorem for theBenchmark
% 78.40/22.26 % SZS output start Proof for theBenchmark
% See solution above
% 142.88/22.56 % (1608640)------------------------------
% 142.88/22.56 % (1608640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.88/22.56 % (1608640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.88/22.56 % (1608640)CaDiCaL version: 2.1.3
% 142.88/22.56 % (1608640)Termination reason: Refutation
% 142.88/22.56 % (1608640)Time elapsed: 3.278 s
% 142.88/22.56 % (1608640)Peak memory usage: 256 MB
% 142.88/22.56 % (1608640)Instructions burned: 5872 (million)
% 142.88/22.56 % (1608640)------------------------------
% 142.88/22.56 % (1608640)------------------------------
% 142.88/22.56 % (1608553)Success in time 21.231 s
% 142.88/22.56 % Vampire exiting
%------------------------------------------------------------------------------