%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU450+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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:49:11 PM UTC 2026
% Result : Theorem 11.79s 5.17s
% Output : Refutation 24.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 23
% Syntax : Number of formulae : 147 ( 27 unt; 14 def)
% Number of atoms : 415 ( 51 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 492 ( 224 ~; 218 |; 17 &)
% ( 16 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 15 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-4 aty)
% Number of variables : 158 ( 0 sgn 153 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
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(f19064,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
=> m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_relset_2) ).
fof(f19103,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( r1_tarski(X2,X3)
=> r1_tarski(k8_relset_2(X0,X1,X3,X4),k8_relset_2(X0,X1,X2,X4)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t32_relset_2) ).
fof(f19134,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X1))
=> ! [X4] :
( m2_relset_1(X4,X0,X1)
=> ( r1_tarski(X2,k8_relset_2(X1,X0,k8_relset_2(X0,X1,X2,X4),k6_relset_1(X0,X1,X4)))
& r1_tarski(X3,k8_relset_2(X0,X1,k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)),X4)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_relset_2) ).
fof(f19135,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X1))
=> ! [X4] :
( m2_relset_1(X4,X0,X1)
=> ( k8_relset_2(X0,X1,X2,X4) = k8_relset_2(X0,X1,k8_relset_2(X1,X0,k8_relset_2(X0,X1,X2,X4),k6_relset_1(X0,X1,X4)),X4)
& k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)) = k8_relset_2(X1,X0,k8_relset_2(X0,X1,k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)),X4),k6_relset_1(X0,X1,X4)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t64_relset_2) ).
fof(f19136,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X1))
=> ! [X4] :
( m2_relset_1(X4,X0,X1)
=> ( k8_relset_2(X0,X1,X2,X4) = k8_relset_2(X0,X1,k8_relset_2(X1,X0,k8_relset_2(X0,X1,X2,X4),k6_relset_1(X0,X1,X4)),X4)
& k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)) = k8_relset_2(X1,X0,k8_relset_2(X0,X1,k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)),X4),k6_relset_1(X0,X1,X4)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f19135]) ).
fof(f19195,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f19064]) ).
fof(f19196,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(flattening,[],[f19195]) ).
fof(f19238,plain,
! [X0,X1,X2] :
( ! [X3] :
( ! [X4] :
( r1_tarski(k8_relset_2(X0,X1,X3,X4),k8_relset_2(X0,X1,X2,X4))
| ~ r1_tarski(X2,X3)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19103]) ).
fof(f19239,plain,
! [X0,X1,X2] :
( ! [X3] :
( ! [X4] :
( r1_tarski(k8_relset_2(X0,X1,X3,X4),k8_relset_2(X0,X1,X2,X4))
| ~ r1_tarski(X2,X3)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f19238]) ).
fof(f19275,plain,
! [X0,X1,X2] :
( ! [X3] :
( ! [X4] :
( ( r1_tarski(X2,k8_relset_2(X1,X0,k8_relset_2(X0,X1,X2,X4),k6_relset_1(X0,X1,X4)))
& r1_tarski(X3,k8_relset_2(X0,X1,k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)),X4)) )
| ~ m2_relset_1(X4,X0,X1) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X1)) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19134]) ).
fof(f19276,plain,
? [X0,X1,X2] :
( ? [X3] :
( ? [X4] :
( ( k8_relset_2(X0,X1,X2,X4) != k8_relset_2(X0,X1,k8_relset_2(X1,X0,k8_relset_2(X0,X1,X2,X4),k6_relset_1(X0,X1,X4)),X4)
| k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)) != k8_relset_2(X1,X0,k8_relset_2(X0,X1,k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)),X4),k6_relset_1(X0,X1,X4)) )
& m2_relset_1(X4,X0,X1) )
& m1_subset_1(X3,k1_zfmisc_1(X1)) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19136]) ).
fof(f19311,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(f20034,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(f20036,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(f22429,plain,
( ( k8_relset_2(sK22,sK23,sK24,sK26) != k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,sK24,sK26),k6_relset_1(sK22,sK23,sK26)),sK26)
| k8_relset_2(sK23,sK22,sK25,k6_relset_1(sK22,sK23,sK26)) != k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,sK25,k6_relset_1(sK22,sK23,sK26)),sK26),k6_relset_1(sK22,sK23,sK26)) )
& m2_relset_1(sK26,sK22,sK23)
& m1_subset_1(sK25,k1_zfmisc_1(sK23))
& m1_subset_1(sK24,k1_zfmisc_1(sK22)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23,sK24,sK25,sK26]),skolemize(X0,sK22),skolemize(X1,sK23),skolemize(X2,sK24),skolemize(X3,sK25),skolemize(X4,sK26)],[f19276]) ).
fof(f22440,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(f22525,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f22526,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f22525]) ).
fof(f23554,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f19196]) ).
fof(f23608,plain,
! [X2,X3,X0,X1,X4] :
( r1_tarski(k8_relset_2(X0,X1,X3,X4),k8_relset_2(X0,X1,X2,X4))
| ~ r1_tarski(X2,X3)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19239]) ).
fof(f23657,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X4,X0,X1)
| r1_tarski(X3,k8_relset_2(X0,X1,k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)),X4))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19275]) ).
fof(f23658,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X4,X0,X1)
| r1_tarski(X2,k8_relset_2(X1,X0,k8_relset_2(X0,X1,X2,X4),k6_relset_1(X0,X1,X4)))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19275]) ).
fof(f23659,plain,
m1_subset_1(sK24,k1_zfmisc_1(sK22)),
inference(cnf_transformation,[],[f22429]) ).
fof(f23660,plain,
m1_subset_1(sK25,k1_zfmisc_1(sK23)),
inference(cnf_transformation,[],[f22429]) ).
fof(f23661,plain,
m2_relset_1(sK26,sK22,sK23),
inference(cnf_transformation,[],[f22429]) ).
fof(f23662,plain,
( k8_relset_2(sK22,sK23,sK24,sK26) != k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,sK24,sK26),k6_relset_1(sK22,sK23,sK26)),sK26)
| k8_relset_2(sK23,sK22,sK25,k6_relset_1(sK22,sK23,sK26)) != k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,sK25,k6_relset_1(sK22,sK23,sK26)),sK26),k6_relset_1(sK22,sK23,sK26)) ),
inference(cnf_transformation,[],[f22429]) ).
fof(f23719,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f22440]) ).
fof(f23725,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,[],[f19311]) ).
fof(f24147,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f22526]) ).
fof(f24868,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
inference(cnf_transformation,[],[f20034]) ).
fof(f24870,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
inference(cnf_transformation,[],[f20036]) ).
fof(f30723,definition,
( spl729_19
<=> k8_relset_2(sK23,sK22,sK25,k6_relset_1(sK22,sK23,sK26)) = k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,sK25,k6_relset_1(sK22,sK23,sK26)),sK26),k6_relset_1(sK22,sK23,sK26)) ),
introduced(definition,[new_symbols(definition,[spl729_19])],[avatar_definition]) ).
fof(f30724,plain,
( k8_relset_2(sK23,sK22,sK25,k6_relset_1(sK22,sK23,sK26)) != k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,sK25,k6_relset_1(sK22,sK23,sK26)),sK26),k6_relset_1(sK22,sK23,sK26))
| spl729_19 ),
inference(avatar_component_clause,[],[f30723]) ).
fof(f30726,definition,
( spl729_20
<=> k8_relset_2(sK22,sK23,sK24,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,sK24,sK26),k6_relset_1(sK22,sK23,sK26)),sK26) ),
introduced(definition,[new_symbols(definition,[spl729_20])],[avatar_definition]) ).
fof(f30727,plain,
( k8_relset_2(sK22,sK23,sK24,sK26) != k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,sK24,sK26),k6_relset_1(sK22,sK23,sK26)),sK26)
| spl729_20 ),
inference(avatar_component_clause,[],[f30726]) ).
fof(f30728,plain,
( ~ spl729_19
| ~ spl729_20 ),
inference(avatar_split_clause,[],[f23662,f30726,f30723]) ).
fof(f30919,plain,
! [X0,X1] :
( r1_tarski(X0,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k6_relset_1(sK22,sK23,sK26)))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK23))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22)) ),
inference(resolution,[],[f23658,f23661]) ).
fof(f30921,definition,
( spl729_21
<=> ! [X1] : ~ m1_subset_1(X1,k1_zfmisc_1(sK23)) ),
introduced(definition,[new_symbols(definition,[spl729_21])],[avatar_definition]) ).
fof(f30922,plain,
( ! [X1] : ~ m1_subset_1(X1,k1_zfmisc_1(sK23))
| ~ spl729_21 ),
inference(avatar_component_clause,[],[f30921]) ).
fof(f30924,definition,
( spl729_22
<=> ! [X0] :
( r1_tarski(X0,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k6_relset_1(sK22,sK23,sK26)))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22)) ) ),
introduced(definition,[new_symbols(definition,[spl729_22])],[avatar_definition]) ).
fof(f30925,plain,
( ! [X0] :
( r1_tarski(X0,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k6_relset_1(sK22,sK23,sK26)))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22)) )
| ~ spl729_22 ),
inference(avatar_component_clause,[],[f30924]) ).
fof(f30926,plain,
( spl729_21
| spl729_22 ),
inference(avatar_split_clause,[],[f30919,f30924,f30921]) ).
fof(f30927,plain,
! [X0,X1] :
( r1_tarski(X0,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k6_relset_1(sK22,sK23,sK26)),sK26))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK23))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK22)) ),
inference(resolution,[],[f23657,f23661]) ).
fof(f30928,plain,
( $false
| ~ spl729_21 ),
inference(unit_resulting_resolution,[],[f30922,f23660]) ).
fof(f30932,plain,
~ spl729_21,
inference(avatar_contradiction_clause,[],[f30928]) ).
fof(f30934,definition,
( spl729_23
<=> ! [X1] : ~ m1_subset_1(X1,k1_zfmisc_1(sK22)) ),
introduced(definition,[new_symbols(definition,[spl729_23])],[avatar_definition]) ).
fof(f30935,plain,
( ! [X1] : ~ m1_subset_1(X1,k1_zfmisc_1(sK22))
| ~ spl729_23 ),
inference(avatar_component_clause,[],[f30934]) ).
fof(f30937,definition,
( spl729_24
<=> ! [X0] :
( r1_tarski(X0,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k6_relset_1(sK22,sK23,sK26)),sK26))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK23)) ) ),
introduced(definition,[new_symbols(definition,[spl729_24])],[avatar_definition]) ).
fof(f30938,plain,
( ! [X0] :
( r1_tarski(X0,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k6_relset_1(sK22,sK23,sK26)),sK26))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK23)) )
| ~ spl729_24 ),
inference(avatar_component_clause,[],[f30937]) ).
fof(f30939,plain,
( spl729_23
| spl729_24 ),
inference(avatar_split_clause,[],[f30927,f30937,f30934]) ).
fof(f30940,plain,
m1_relset_1(sK26,sK22,sK23),
inference(resolution,[],[f23719,f23661]) ).
fof(f30942,plain,
m2_relset_1(k6_relset_1(sK22,sK23,sK26),sK23,sK22),
inference(resolution,[],[f30940,f24870]) ).
fof(f30943,plain,
k6_relset_1(sK22,sK23,sK26) = k4_relat_1(sK26),
inference(resolution,[],[f30940,f24868]) ).
fof(f30944,plain,
m2_relset_1(k4_relat_1(sK26),sK23,sK22),
inference(forward_demodulation,[],[f30942,f30943]) ).
fof(f30946,plain,
( ! [X0] :
( r1_tarski(X0,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22)) )
| ~ spl729_22 ),
inference(superposition,[],[f30925,f30943]) ).
fof(f30947,plain,
( k8_relset_2(sK22,sK23,sK24,sK26) != k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,sK24,sK26),k4_relat_1(sK26)),sK26)
| spl729_20 ),
inference(superposition,[],[f30727,f30943]) ).
fof(f30958,plain,
( $false
| ~ spl729_23 ),
inference(unit_resulting_resolution,[],[f30935,f23659]) ).
fof(f30962,plain,
~ spl729_23,
inference(avatar_contradiction_clause,[],[f30958]) ).
fof(f30963,plain,
( ! [X0] :
( r1_tarski(X0,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK23)) )
| ~ spl729_24 ),
inference(forward_demodulation,[],[f30938,f30943]) ).
fof(f31011,definition,
( spl729_29
<=> m1_subset_1(k4_relat_1(sK26),k1_zfmisc_1(k2_zfmisc_1(sK23,sK22))) ),
introduced(definition,[new_symbols(definition,[spl729_29])],[avatar_definition]) ).
fof(f31012,plain,
( ~ m1_subset_1(k4_relat_1(sK26),k1_zfmisc_1(k2_zfmisc_1(sK23,sK22)))
| spl729_29 ),
inference(avatar_component_clause,[],[f31011]) ).
fof(f31018,plain,
( ~ m2_relset_1(k4_relat_1(sK26),sK23,sK22)
| spl729_29 ),
inference(resolution,[],[f31012,f23725]) ).
fof(f31020,plain,
( $false
| spl729_29 ),
inference(forward_subsumption_resolution,[],[f31018,f30944]) ).
fof(f31021,plain,
spl729_29,
inference(avatar_contradiction_clause,[],[f31020]) ).
fof(f31070,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sK22))
| k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)) = X0
| ~ r1_tarski(k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),X0) )
| ~ spl729_22 ),
inference(resolution,[],[f24147,f30946]) ).
fof(f31073,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sK23))
| k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26) = X0
| ~ r1_tarski(k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),X0) )
| ~ spl729_24 ),
inference(resolution,[],[f24147,f30963]) ).
fof(f31106,plain,
( ! [X2,X0,X1] :
( ~ r1_tarski(k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(X0,sK23,X1,X2),k4_relat_1(sK26)),sK26),k8_relset_2(X0,sK23,X1,X2))
| k8_relset_2(X0,sK23,X1,X2) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(X0,sK23,X1,X2),k4_relat_1(sK26)),sK26)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,sK23))) )
| ~ spl729_24 ),
inference(resolution,[],[f31073,f23554]) ).
fof(f31117,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,sK22)))
| ~ r1_tarski(k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(X0,sK22,X1,X2),sK26),k4_relat_1(sK26)),k8_relset_2(X0,sK22,X1,X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k8_relset_2(X0,sK22,X1,X2) = k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(X0,sK22,X1,X2),sK26),k4_relat_1(sK26)) )
| ~ spl729_22 ),
inference(resolution,[],[f31070,f23554]) ).
fof(f31133,plain,
( ! [X0] :
( k8_relset_2(sK22,sK23,X0,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ r1_tarski(X0,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)))
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),k1_zfmisc_1(sK22))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22)) )
| ~ spl729_24 ),
inference(resolution,[],[f31106,f23608]) ).
fof(f31134,plain,
( ! [X0] :
( k8_relset_2(sK22,sK23,X0,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ r1_tarski(X0,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)))
| ~ m1_subset_1(k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),k1_zfmisc_1(sK22)) )
| ~ spl729_24 ),
inference(duplicate_literal_removal,[],[f31133]) ).
fof(f31135,plain,
( ! [X0] :
( k8_relset_2(sK22,sK23,X0,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),k1_zfmisc_1(sK22)) )
| ~ spl729_22
| ~ spl729_24 ),
inference(forward_subsumption_resolution,[],[f31134,f30946]) ).
fof(f31137,definition,
( spl729_39
<=> m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23))) ),
introduced(definition,[new_symbols(definition,[spl729_39])],[avatar_definition]) ).
fof(f31138,plain,
( ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| spl729_39 ),
inference(avatar_component_clause,[],[f31137]) ).
fof(f31140,definition,
( spl729_40
<=> ! [X0] :
( k8_relset_2(sK22,sK23,X0,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),sK26)
| ~ m1_subset_1(k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),k1_zfmisc_1(sK22))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22)) ) ),
introduced(definition,[new_symbols(definition,[spl729_40])],[avatar_definition]) ).
fof(f31141,plain,
( ! [X0] :
( ~ m1_subset_1(k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),k1_zfmisc_1(sK22))
| k8_relset_2(sK22,sK23,X0,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22)) )
| ~ spl729_40 ),
inference(avatar_component_clause,[],[f31140]) ).
fof(f31142,plain,
( ~ spl729_39
| spl729_40
| ~ spl729_22
| ~ spl729_24 ),
inference(avatar_split_clause,[],[f31135,f30937,f30924,f31140,f31137]) ).
fof(f31144,plain,
( ~ m2_relset_1(sK26,sK22,sK23)
| spl729_39 ),
inference(resolution,[],[f31138,f23725]) ).
fof(f31146,plain,
( $false
| spl729_39 ),
inference(forward_subsumption_resolution,[],[f31144,f23661]) ).
fof(f31147,plain,
spl729_39,
inference(avatar_contradiction_clause,[],[f31146]) ).
fof(f31148,plain,
( ! [X0] :
( k8_relset_2(sK22,sK23,X0,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22))
| ~ m1_subset_1(k8_relset_2(sK22,sK23,X0,sK26),k1_zfmisc_1(sK23))
| ~ m1_subset_1(k4_relat_1(sK26),k1_zfmisc_1(k2_zfmisc_1(sK23,sK22))) )
| ~ spl729_40 ),
inference(resolution,[],[f31141,f23554]) ).
fof(f31150,definition,
( spl729_41
<=> ! [X0] :
( k8_relset_2(sK22,sK23,X0,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),sK26)
| ~ m1_subset_1(k8_relset_2(sK22,sK23,X0,sK26),k1_zfmisc_1(sK23))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22)) ) ),
introduced(definition,[new_symbols(definition,[spl729_41])],[avatar_definition]) ).
fof(f31151,plain,
( ! [X0] :
( ~ m1_subset_1(k8_relset_2(sK22,sK23,X0,sK26),k1_zfmisc_1(sK23))
| k8_relset_2(sK22,sK23,X0,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22)) )
| ~ spl729_41 ),
inference(avatar_component_clause,[],[f31150]) ).
fof(f31152,plain,
( ~ spl729_29
| spl729_41
| ~ spl729_40 ),
inference(avatar_split_clause,[],[f31148,f31140,f31150,f31011]) ).
fof(f31153,plain,
( ! [X0] :
( k8_relset_2(sK22,sK23,X0,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23))) )
| ~ spl729_41 ),
inference(resolution,[],[f31151,f23554]) ).
fof(f31154,plain,
( ! [X0] :
( k8_relset_2(sK22,sK23,X0,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23))) )
| ~ spl729_41 ),
inference(duplicate_literal_removal,[],[f31153]) ).
fof(f31156,definition,
( spl729_42
<=> ! [X0] :
( k8_relset_2(sK22,sK23,X0,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK22)) ) ),
introduced(definition,[new_symbols(definition,[spl729_42])],[avatar_definition]) ).
fof(f31157,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sK22))
| k8_relset_2(sK22,sK23,X0,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,X0,sK26),k4_relat_1(sK26)),sK26) )
| ~ spl729_42 ),
inference(avatar_component_clause,[],[f31156]) ).
fof(f31158,plain,
( ~ spl729_39
| spl729_42
| ~ spl729_41 ),
inference(avatar_split_clause,[],[f31154,f31150,f31156,f31137]) ).
fof(f31161,plain,
( k8_relset_2(sK22,sK23,sK24,sK26) = k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,sK24,sK26),k4_relat_1(sK26)),sK26)
| ~ spl729_42 ),
inference(resolution,[],[f31157,f23659]) ).
fof(f31163,plain,
( $false
| spl729_20
| ~ spl729_42 ),
inference(forward_subsumption_resolution,[],[f31161,f30947]) ).
fof(f31164,plain,
( spl729_20
| ~ spl729_42 ),
inference(avatar_contradiction_clause,[],[f31163]) ).
fof(f31165,plain,
( k8_relset_2(sK23,sK22,sK25,k4_relat_1(sK26)) != k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,sK25,k4_relat_1(sK26)),sK26),k4_relat_1(sK26))
| spl729_19 ),
inference(forward_demodulation,[],[f30724,f30943]) ).
fof(f31238,definition,
( spl729_50
<=> m1_subset_1(k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,sK25,k4_relat_1(sK26)),sK26),k1_zfmisc_1(sK23)) ),
introduced(definition,[new_symbols(definition,[spl729_50])],[avatar_definition]) ).
fof(f31239,plain,
( m1_subset_1(k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,sK25,k4_relat_1(sK26)),sK26),k1_zfmisc_1(sK23))
| ~ spl729_50 ),
inference(avatar_component_clause,[],[f31238]) ).
fof(f31251,plain,
( ~ m1_subset_1(k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,sK25,k4_relat_1(sK26)),sK26),k1_zfmisc_1(sK23))
| spl729_50 ),
inference(avatar_component_clause,[],[f31238]) ).
fof(f31253,plain,
( ~ m1_subset_1(k8_relset_2(sK23,sK22,sK25,k4_relat_1(sK26)),k1_zfmisc_1(sK22))
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| spl729_50 ),
inference(resolution,[],[f31251,f23554]) ).
fof(f31255,definition,
( spl729_53
<=> m1_subset_1(k8_relset_2(sK23,sK22,sK25,k4_relat_1(sK26)),k1_zfmisc_1(sK22)) ),
introduced(definition,[new_symbols(definition,[spl729_53])],[avatar_definition]) ).
fof(f31256,plain,
( ~ m1_subset_1(k8_relset_2(sK23,sK22,sK25,k4_relat_1(sK26)),k1_zfmisc_1(sK22))
| spl729_53 ),
inference(avatar_component_clause,[],[f31255]) ).
fof(f31257,plain,
( ~ spl729_39
| ~ spl729_53
| spl729_50 ),
inference(avatar_split_clause,[],[f31253,f31238,f31255,f31137]) ).
fof(f31258,plain,
( ~ m1_subset_1(sK25,k1_zfmisc_1(sK23))
| ~ m1_subset_1(k4_relat_1(sK26),k1_zfmisc_1(k2_zfmisc_1(sK23,sK22)))
| spl729_53 ),
inference(resolution,[],[f31256,f23554]) ).
fof(f31259,plain,
( ~ m1_subset_1(k4_relat_1(sK26),k1_zfmisc_1(k2_zfmisc_1(sK23,sK22)))
| spl729_53 ),
inference(forward_subsumption_resolution,[],[f31258,f23660]) ).
fof(f31260,plain,
( ~ spl729_29
| spl729_53 ),
inference(avatar_split_clause,[],[f31259,f31255,f31011]) ).
fof(f32199,plain,
( ! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,sK22)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k8_relset_2(X0,sK22,X1,X2) = k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(X0,sK22,X1,X2),sK26),k4_relat_1(sK26))
| ~ r1_tarski(k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(X0,sK22,X1,X2),sK26),k4_relat_1(sK26)),k8_relset_2(X0,sK22,X1,X2)) )
| ~ spl729_22 ),
inference(resolution,[],[f31117,f23725]) ).
fof(f34895,plain,
( ! [X0] :
( ~ r1_tarski(k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),k4_relat_1(sK26)),k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)))
| k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)) = k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),k4_relat_1(sK26))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK23)) )
| ~ spl729_22 ),
inference(resolution,[],[f32199,f30944]) ).
fof(f34896,plain,
( ! [X0] :
( k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)) = k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),k4_relat_1(sK26))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK23))
| ~ r1_tarski(X0,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26))
| ~ m1_subset_1(k4_relat_1(sK26),k1_zfmisc_1(k2_zfmisc_1(sK23,sK22)))
| ~ m1_subset_1(k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),k1_zfmisc_1(sK23))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK23)) )
| ~ spl729_22 ),
inference(resolution,[],[f34895,f23608]) ).
fof(f34899,plain,
( ! [X0] :
( k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)) = k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),k4_relat_1(sK26))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK23))
| ~ r1_tarski(X0,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26))
| ~ m1_subset_1(k4_relat_1(sK26),k1_zfmisc_1(k2_zfmisc_1(sK23,sK22)))
| ~ m1_subset_1(k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),k1_zfmisc_1(sK23)) )
| ~ spl729_22 ),
inference(duplicate_literal_removal,[],[f34896]) ).
fof(f34900,plain,
( ! [X0] :
( k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)) = k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),k4_relat_1(sK26))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK23))
| ~ m1_subset_1(k4_relat_1(sK26),k1_zfmisc_1(k2_zfmisc_1(sK23,sK22)))
| ~ m1_subset_1(k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),k1_zfmisc_1(sK23)) )
| ~ spl729_22
| ~ spl729_24 ),
inference(forward_subsumption_resolution,[],[f34899,f30963]) ).
fof(f34902,definition,
( spl729_292
<=> ! [X0] :
( k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)) = k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),k4_relat_1(sK26))
| ~ m1_subset_1(k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),k1_zfmisc_1(sK23))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK23)) ) ),
introduced(definition,[new_symbols(definition,[spl729_292])],[avatar_definition]) ).
fof(f34903,plain,
( ! [X0] :
( ~ m1_subset_1(k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),k1_zfmisc_1(sK23))
| k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)) = k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,X0,k4_relat_1(sK26)),sK26),k4_relat_1(sK26))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK23)) )
| ~ spl729_292 ),
inference(avatar_component_clause,[],[f34902]) ).
fof(f34904,plain,
( ~ spl729_29
| spl729_292
| ~ spl729_22
| ~ spl729_24 ),
inference(avatar_split_clause,[],[f34900,f30937,f30924,f34902,f31011]) ).
fof(f34906,plain,
( k8_relset_2(sK23,sK22,sK25,k4_relat_1(sK26)) = k8_relset_2(sK23,sK22,k8_relset_2(sK22,sK23,k8_relset_2(sK23,sK22,sK25,k4_relat_1(sK26)),sK26),k4_relat_1(sK26))
| ~ m1_subset_1(sK25,k1_zfmisc_1(sK23))
| ~ spl729_50
| ~ spl729_292 ),
inference(resolution,[],[f34903,f31239]) ).
fof(f34915,plain,
( ~ m1_subset_1(sK25,k1_zfmisc_1(sK23))
| spl729_19
| ~ spl729_50
| ~ spl729_292 ),
inference(forward_subsumption_resolution,[],[f34906,f31165]) ).
fof(f34916,plain,
( $false
| spl729_19
| ~ spl729_50
| ~ spl729_292 ),
inference(forward_subsumption_resolution,[],[f34915,f23660]) ).
fof(f34917,plain,
( spl729_19
| ~ spl729_50
| ~ spl729_292 ),
inference(avatar_contradiction_clause,[],[f34916]) ).
cnf(s10,plain,
( ~ spl729_19
| ~ spl729_20 ),
inference(sat_conversion,[],[f30728]) ).
cnf(s16,plain,
( spl729_21
| spl729_22 ),
inference(sat_conversion,[],[f30926]) ).
cnf(s18,plain,
~ spl729_21,
inference(sat_conversion,[],[f30932]) ).
cnf(s19,plain,
( spl729_23
| spl729_24 ),
inference(sat_conversion,[],[f30939]) ).
cnf(s21,plain,
~ spl729_23,
inference(sat_conversion,[],[f30962]) ).
cnf(s28,plain,
spl729_29,
inference(sat_conversion,[],[f31021]) ).
cnf(s33,plain,
( ~ spl729_22
| ~ spl729_24
| ~ spl729_39
| spl729_40 ),
inference(sat_conversion,[],[f31142]) ).
cnf(s35,plain,
spl729_39,
inference(sat_conversion,[],[f31147]) ).
cnf(s36,plain,
( ~ spl729_29
| ~ spl729_40
| spl729_41 ),
inference(sat_conversion,[],[f31152]) ).
cnf(s37,plain,
( ~ spl729_39
| ~ spl729_41
| spl729_42 ),
inference(sat_conversion,[],[f31158]) ).
cnf(s39,plain,
( spl729_20
| ~ spl729_42 ),
inference(sat_conversion,[],[f31164]) ).
cnf(s50,plain,
( ~ spl729_39
| spl729_50
| ~ spl729_53 ),
inference(sat_conversion,[],[f31257]) ).
cnf(s51,plain,
( ~ spl729_29
| spl729_53 ),
inference(sat_conversion,[],[f31260]) ).
cnf(s272,plain,
( ~ spl729_22
| ~ spl729_24
| ~ spl729_29
| spl729_292 ),
inference(sat_conversion,[],[f34904]) ).
cnf(s275,plain,
( spl729_19
| ~ spl729_50
| ~ spl729_292 ),
inference(sat_conversion,[],[f34917]) ).
cnf(s305,plain,
( ~ spl729_22
| ~ spl729_24
| spl729_40 ),
inference(rat,[],[s33,s35]) ).
cnf(s324,plain,
spl729_53,
inference(rat,[],[s51,s28]) ).
cnf(s328,plain,
spl729_50,
inference(rat,[],[s50,s35,s324]) ).
cnf(s344,plain,
spl729_24,
inference(rat,[],[s19,s21]) ).
cnf(s347,plain,
spl729_22,
inference(rat,[],[s16,s18]) ).
cnf(s348,plain,
spl729_292,
inference(rat,[],[s272,s344,s28,s347]) ).
cnf(s349,plain,
spl729_40,
inference(rat,[],[s305,s344,s347]) ).
cnf(s351,plain,
spl729_19,
inference(rat,[],[s275,s328,s348]) ).
cnf(s352,plain,
spl729_41,
inference(rat,[],[s36,s28,s349]) ).
cnf(s353,plain,
spl729_42,
inference(rat,[],[s37,s35,s352]) ).
cnf(s398,plain,
spl729_20,
inference(rat,[],[s39,s353]) ).
cnf(s399,plain,
$false,
inference(rat,[],[s10,s398,s351]) ).
fof(f34918,plain,
$false,
inference(avatar_sat_refutation,[],[s399]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU450+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n008.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 28 05:37:43 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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.38/3.56 % (1948797)Detected formulas, will run a generic FOF schedule.
% 12.38/3.56 % (1948808)dis-21_1_sil=8000:lcm=predicate:random_seed=3413794498:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2989 on theBenchmark for (2989ds/129Mi)
% 12.38/3.56 % (1948806)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3316959603:i=119:av=off:ss=axioms_2989 on theBenchmark for (2989ds/119Mi)
% 12.38/3.56 % (1948805)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1160283940:i=109:sd=1:ins=1:gsp=on:ss=axioms_2989 on theBenchmark for (2989ds/109Mi)
% 12.38/3.56 % (1948804)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=2199007430:i=141695:sd=1:nm=32:gsp=on:ss=included_2989 on theBenchmark for (2989ds/141695Mi)
% 12.38/3.56 % (1948803)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=3218581771:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2989 on theBenchmark for (2989ds/134677Mi)
% 12.38/3.56 % (1948802)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=3471220659:i=141193_2989 on theBenchmark for (2989ds/141193Mi)
% 12.38/3.56 % (1948808)Instruction limit reached!
% 12.38/3.56 % (1948808)------------------------------
% 12.38/3.56 % (1948808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/3.56 % (1948808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/3.56 % (1948808)CaDiCaL version: 2.1.3
% 12.38/3.56 % (1948808)Termination reason: Instruction limit
% 12.38/3.56 % (1948808)Termination phase: SInE selection
% 12.38/3.56 % (1948808)Time elapsed: 0.052 s
% 12.38/3.56 % (1948808)Peak memory usage: 113 MB
% 12.38/3.56 % (1948808)Instructions burned: 131 (million)
% 12.38/3.56 % (1948807)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1119797788:s2a=on:i=139:gtg=position_2989 on theBenchmark for (2989ds/139Mi)
% 12.38/3.56 % (1948805)Instruction limit reached!
% 12.38/3.56 % (1948805)------------------------------
% 12.38/3.56 % (1948805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/3.56 % (1948805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/3.56 % (1948805)CaDiCaL version: 2.1.3
% 12.38/3.56 % (1948805)Termination reason: Instruction limit
% 12.38/3.56 % (1948805)Termination phase: SInE selection
% 12.38/3.56 % (1948805)Time elapsed: 0.085 s
% 12.38/3.56 % (1948805)Peak memory usage: 112 MB
% 12.38/3.56 % (1948805)Instructions burned: 109 (million)
% 12.38/3.56 % (1948807)Instruction limit reached!
% 12.38/3.56 % (1948807)------------------------------
% 12.38/3.56 % (1948807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/3.56 % (1948807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/3.56 % (1948807)CaDiCaL version: 2.1.3
% 12.38/3.56 % (1948807)Termination reason: Instruction limit
% 12.38/3.56 % (1948807)Termination phase: Property scanning
% 12.38/3.56 % (1948807)Time elapsed: 0.062 s
% 12.38/3.56 % (1948807)Peak memory usage: 112 MB
% 12.38/3.56 % (1948807)Instructions burned: 141 (million)
% 12.38/3.56 % (1948806)Instruction limit reached!
% 12.38/3.56 % (1948806)------------------------------
% 12.38/3.56 % (1948806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/3.56 % (1948806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/3.56 % (1948806)CaDiCaL version: 2.1.3
% 12.38/3.56 % (1948806)Termination reason: Instruction limit
% 12.38/3.56 % (1948806)Termination phase: Preprocessing 1
% 12.38/3.56 % (1948806)Time elapsed: 0.101 s
% 12.38/3.56 % (1948806)Peak memory usage: 113 MB
% 12.38/3.56 % (1948806)Instructions burned: 119 (million)
% 12.38/3.56 % (1948815)lrs+10_1_sil=8000:sp=occurrence:random_seed=4138326864:i=285:sd=3:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/285Mi)
% 12.38/3.56 % (1948818)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2672085673:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 12.38/3.56 % (1948817)lrs+10_1_sil=32000:urr=on:br=off:random_seed=792707022:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 12.38/3.56 % (1948819)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=171355053:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 12.38/3.56 % (1948815)Instruction limit reached!
% 18.98/4.55 % (1948815)------------------------------
% 18.98/4.55 % (1948815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/4.55 % (1948815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/4.55 % (1948815)CaDiCaL version: 2.1.3
% 18.98/4.55 % (1948815)Termination reason: Instruction limit
% 18.98/4.55 % (1948815)Termination phase: Saturation
% 18.98/4.55 % (1948815)Time elapsed: 0.123 s
% 18.98/4.55 % (1948815)Peak memory usage: 119 MB
% 18.98/4.55 % (1948815)Instructions burned: 287 (million)
% 18.98/4.55 % (1948817)Instruction limit reached!
% 18.98/4.55 % (1948817)------------------------------
% 18.98/4.55 % (1948817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/4.55 % (1948817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/4.55 % (1948817)CaDiCaL version: 2.1.3
% 18.98/4.55 % (1948817)Termination reason: Instruction limit
% 18.98/4.55 % (1948817)Termination phase: Property scanning
% 18.98/4.55 % (1948817)Time elapsed: 0.070 s
% 18.98/4.55 % (1948817)Peak memory usage: 112 MB
% 18.98/4.55 % (1948817)Instructions burned: 159 (million)
% 18.98/4.55 % (1948819)Instruction limit reached!
% 18.98/4.55 % (1948819)------------------------------
% 18.98/4.55 % (1948819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/4.55 % (1948819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/4.55 % (1948819)CaDiCaL version: 2.1.3
% 18.98/4.55 % (1948819)Termination reason: Instruction limit
% 18.98/4.55 % (1948819)Termination phase: Property scanning
% 18.98/4.55 % (1948819)Time elapsed: 0.106 s
% 18.98/4.55 % (1948819)Peak memory usage: 112 MB
% 18.98/4.55 % (1948819)Instructions burned: 249 (million)
% 18.98/4.55 % (1948824)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1778112573:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2985 on theBenchmark for (2985ds/294Mi)
% 18.98/4.55 % (1948825)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1552604212:i=2350_2984 on theBenchmark for (2984ds/2350Mi)
% 18.98/4.55 % (1948824)Instruction limit reached!
% 18.98/4.55 % (1948824)------------------------------
% 18.98/4.55 % (1948824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/4.55 % (1948824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/4.55 % (1948824)CaDiCaL version: 2.1.3
% 18.98/4.55 % (1948824)Termination reason: Instruction limit
% 18.98/4.55 % (1948824)Termination phase: Saturation
% 18.98/4.55 % (1948824)Time elapsed: 0.118 s
% 18.98/4.55 % (1948824)Peak memory usage: 119 MB
% 18.98/4.55 % (1948824)Instructions burned: 294 (million)
% 18.98/4.55 % (1948827)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2608514974:cts=off:i=113:fsr=off:ss=included:sgt=4_2984 on theBenchmark for (2984ds/113Mi)
% 18.98/4.55 % (1948818)Instruction limit reached!
% 18.98/4.55 % (1948818)------------------------------
% 18.98/4.55 % (1948818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/4.55 % (1948818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/4.55 % (1948818)CaDiCaL version: 2.1.3
% 18.98/4.55 % (1948818)Termination reason: Instruction limit
% 18.98/4.55 % (1948818)Termination phase: Saturation
% 18.98/4.55 % (1948818)Time elapsed: 0.252 s
% 18.98/4.55 % (1948818)Peak memory usage: 119 MB
% 18.98/4.55 % (1948818)Instructions burned: 325 (million)
% 18.98/4.55 % (1948830)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=438687647:i=127:av=off:fsr=off:sup=off_2983 on theBenchmark for (2983ds/127Mi)
% 18.98/4.55 % (1948827)Instruction limit reached!
% 18.98/4.55 % (1948827)------------------------------
% 18.98/4.55 % (1948827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/4.55 % (1948827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/4.55 % (1948827)CaDiCaL version: 2.1.3
% 18.98/4.55 % (1948827)Termination reason: Instruction limit
% 18.98/4.55 % (1948827)Termination phase: SInE selection
% 18.98/4.55 % (1948827)Time elapsed: 0.090 s
% 18.98/4.55 % (1948827)Peak memory usage: 112 MB
% 18.98/4.55 % (1948827)Instructions burned: 113 (million)
% 18.98/4.55 % (1948831)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1708255515:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2982 on theBenchmark for (2982ds/114Mi)
% 18.98/4.55 % (1948830)Instruction limit reached!
% 18.98/4.55 % (1948830)------------------------------
% 18.98/4.55 % (1948830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/5.17 % (1948830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/5.17 % (1948830)CaDiCaL version: 2.1.3
% 11.79/5.17 % (1948830)Termination reason: Instruction limit
% 11.79/5.17 % (1948830)Termination phase: Preprocessing 1
% 11.79/5.17 % (1948830)Time elapsed: 0.052 s
% 11.79/5.17 % (1948830)Peak memory usage: 113 MB
% 11.79/5.17 % (1948830)Instructions burned: 128 (million)
% 11.79/5.17 % (1948831)Instruction limit reached!
% 11.79/5.17 % (1948831)------------------------------
% 11.79/5.17 % (1948831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/5.17 % (1948831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/5.17 % (1948831)CaDiCaL version: 2.1.3
% 11.79/5.17 % (1948831)Termination reason: Instruction limit
% 11.79/5.17 % (1948831)Termination phase: Property scanning
% 11.79/5.17 % (1948831)Time elapsed: 0.050 s
% 11.79/5.17 % (1948831)Peak memory usage: 112 MB
% 11.79/5.17 % (1948831)Instructions burned: 114 (million)
% 11.79/5.17 % (1948833)lrs+10_1_sil=8000:sp=occurrence:random_seed=2530741862:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi)
% 11.79/5.17 % (1948835)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2752032439:i=437:sd=1:aac=none:ss=included_2981 on theBenchmark for (2981ds/437Mi)
% 11.79/5.17 % (1948836)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3913275972:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 11.79/5.17 % (1948835)Instruction limit reached!
% 11.79/5.17 % (1948835)------------------------------
% 11.79/5.17 % (1948835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/5.17 % (1948835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/5.17 % (1948835)CaDiCaL version: 2.1.3
% 11.79/5.17 % (1948835)Termination reason: Instruction limit
% 11.79/5.17 % (1948835)Termination phase: Saturation
% 11.79/5.17 % (1948835)Time elapsed: 0.169 s
% 11.79/5.17 % (1948835)Peak memory usage: 121 MB
% 11.79/5.17 % (1948835)Instructions burned: 439 (million)
% 11.79/5.17 % (1948840)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1342201895:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi)
% 11.79/5.17 % (1948840)Instruction limit reached!
% 11.79/5.17 % (1948840)------------------------------
% 11.79/5.17 % (1948840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/5.17 % (1948840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/5.17 % (1948840)CaDiCaL version: 2.1.3
% 11.79/5.17 % (1948840)Termination reason: Instruction limit
% 11.79/5.17 % (1948840)Termination phase: NewCNF
% 11.79/5.17 % (1948840)Time elapsed: 0.068 s
% 11.79/5.17 % (1948840)Peak memory usage: 115 MB
% 11.79/5.17 % (1948840)Instructions burned: 136 (million)
% 11.79/5.17 % (1948842)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=951639623:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 11.79/5.17 % (1948833)Instruction limit reached!
% 11.79/5.17 % (1948833)------------------------------
% 11.79/5.17 % (1948833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/5.17 % (1948833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/5.17 % (1948833)CaDiCaL version: 2.1.3
% 11.79/5.17 % (1948833)Termination reason: Instruction limit
% 11.79/5.17 % (1948833)Termination phase: Saturation
% 11.79/5.17 % (1948833)Time elapsed: 0.528 s
% 11.79/5.17 % (1948833)Peak memory usage: 130 MB
% 11.79/5.17 % (1948833)Instructions burned: 907 (million)
% 11.79/5.17 % (1948844)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3898504887:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 11.79/5.17 % (1948842)Instruction limit reached!
% 11.79/5.17 % (1948842)------------------------------
% 11.79/5.17 % (1948842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/5.17 % (1948842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/5.17 % (1948842)CaDiCaL version: 2.1.3
% 11.79/5.17 % (1948842)Termination reason: Instruction limit
% 11.79/5.17 % (1948842)Termination phase: Preprocessing 3
% 11.79/5.17 % (1948842)Time elapsed: 0.274 s
% 11.79/5.17 % (1948842)Peak memory usage: 133 MB
% 11.79/5.17 % (1948842)Instructions burned: 592 (million)
% 11.79/5.17 % (1948846)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=898298498:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/125Mi)
% 11.79/5.17 % (1948846)Instruction limit reached!
% 11.79/5.17 % (1948846)------------------------------
% 11.79/5.17 % (1948846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/5.17 % (1948846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/5.17 % (1948846)CaDiCaL version: 2.1.3
% 11.79/5.17 % (1948846)Termination reason: Instruction limit
% 11.79/5.17 % (1948846)Termination phase: Property scanning
% 11.79/5.17 % (1948846)Time elapsed: 0.029 s
% 11.79/5.17 % (1948846)Peak memory usage: 112 MB
% 11.79/5.17 % (1948846)Instructions burned: 125 (million)
% 11.79/5.17 % (1948848)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3130193764:i=134:gtgl=5:slsql=off:gtg=exists_sym_2972 on theBenchmark for (2972ds/134Mi)
% 11.79/5.17 % (1948848)Instruction limit reached!
% 11.79/5.17 % (1948848)------------------------------
% 11.79/5.17 % (1948848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/5.17 % (1948848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/5.17 % (1948848)CaDiCaL version: 2.1.3
% 11.79/5.17 % (1948848)Termination reason: Instruction limit
% 11.79/5.17 % (1948848)Termination phase: Property scanning
% 11.79/5.17 % (1948848)Time elapsed: 0.033 s
% 11.79/5.17 % (1948848)Peak memory usage: 112 MB
% 11.79/5.17 % (1948848)Instructions burned: 134 (million)
% 11.79/5.17 % (1948825)Instruction limit reached!
% 11.79/5.17 % (1948825)------------------------------
% 11.79/5.17 % (1948825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/5.17 % (1948825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/5.17 % (1948825)CaDiCaL version: 2.1.3
% 11.79/5.17 % (1948825)Termination reason: Instruction limit
% 11.79/5.17 % (1948825)Termination phase: Property scanning
% 11.79/5.17 % (1948825)Time elapsed: 1.254 s
% 11.79/5.17 % (1948825)Peak memory usage: 172 MB
% 11.79/5.17 % (1948825)Instructions burned: 2352 (million)
% 11.79/5.17 % (1948850)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1065083778:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/141Mi)
% 11.79/5.17 % (1948850)Refutation not found, incomplete strategy
% 11.79/5.17 % (1948850)------------------------------
% 11.79/5.17 % (1948850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/5.17 % (1948850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/5.17 % (1948850)CaDiCaL version: 2.1.3
% 11.79/5.17 % (1948850)Termination reason: Refutation not found, incomplete strategy
% 11.79/5.17 % (1948850)Time elapsed: 0.064 s
% 11.79/5.17 % (1948850)Peak memory usage: 117 MB
% 11.79/5.17 % (1948850)Instructions burned: 125 (million)
% 11.79/5.17 % (1948851)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2543033571:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2970 on theBenchmark for (2970ds/431Mi)
% 11.79/5.17 % (1948850)------------------------------
% 11.79/5.17 % (1948850)------------------------------
% 11.79/5.17 % (1948851)Refutation not found, incomplete strategy
% 11.79/5.17 % (1948851)------------------------------
% 11.79/5.17 % (1948851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/5.17 % (1948851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/5.17 % (1948851)CaDiCaL version: 2.1.3
% 11.79/5.17 % (1948851)Termination reason: Refutation not found, incomplete strategy
% 11.79/5.17 % (1948851)Time elapsed: 0.108 s
% 11.79/5.17 % (1948851)Peak memory usage: 118 MB
% 11.79/5.17 % (1948851)Instructions burned: 122 (million)
% 11.79/5.17 % (1948854)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=3903473286:i=6060:aac=none:ins=25_2968 on theBenchmark for (2968ds/6060Mi)
% 11.79/5.17 % (1948851)------------------------------
% 11.79/5.17 % (1948851)------------------------------
% 11.79/5.17 % (1948856)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=3073224178:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2965 on theBenchmark for (2965ds/150Mi)
% 11.79/5.17 % (1948856)Instruction limit reached!
% 11.79/5.17 % (1948856)------------------------------
% 11.79/5.17 % (1948856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/5.17 % (1948856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/5.17 % (1948856)CaDiCaL version: 2.1.3
% 11.79/5.17 % (1948856)Termination reason: Instruction limit
% 11.79/5.17 % (1948856)Termination phase: Preprocessing 1
% 11.79/5.17 % (1948856)Time elapsed: 0.129 s
% 11.79/5.17 % (1948856)Peak memory usage: 113 MB
% 11.79/5.17 % (1948856)Instructions burned: 151 (million)
% 11.79/5.17 % (1948858)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=380406826:i=14155:bd=all_2962 on theBenchmark for (2962ds/14155Mi)
% 11.79/5.17 % (1948803)First to succeed.
% 11.79/5.17 % (1948803)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1948797"
% 11.79/5.17 % (1948803)Refutation found. Thanks to Tanya!
% 11.79/5.17 % SZS status Theorem for theBenchmark
% 11.79/5.17 % SZS output start Proof for theBenchmark
% See solution above
% 24.43/5.37 % (1948803)------------------------------
% 24.43/5.37 % (1948803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.43/5.37 % (1948803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.43/5.37 % (1948803)CaDiCaL version: 2.1.3
% 24.43/5.37 % (1948803)Termination reason: Refutation
% 24.43/5.37 % (1948803)Time elapsed: 2.774 s
% 24.43/5.37 % (1948803)Peak memory usage: 219 MB
% 24.43/5.37 % (1948803)Instructions burned: 4305 (million)
% 24.43/5.37 % (1948803)------------------------------
% 24.43/5.37 % (1948803)------------------------------
% 24.43/5.37 % (1948797)Success in time 4.322 s
% 24.43/5.37 % Vampire exiting
%------------------------------------------------------------------------------