%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU443+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 : n002.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:07 PM UTC 2026
% Result : Theorem 26.19s 11.80s
% Output : Refutation 71.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 67
% Syntax : Number of formulae : 379 ( 63 unt; 46 def)
% Number of atoms : 922 ( 137 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 995 ( 452 ~; 453 |; 21 &)
% ( 45 <=>; 23 =>; 0 <=; 1 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 49 ( 47 usr; 43 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 8 con; 0-5 aty)
% Number of variables : 239 ( 0 sgn 227 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f57,axiom,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f70,axiom,
! [X0,X1,X2] :
( ( r1_tarski(X0,X1)
& r1_tarski(X1,X2) )
=> r1_tarski(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f97,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
=> k3_xboole_0(X0,X1) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t28_xboole_1) ).
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f853,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> r1_tarski(k9_relat_1(X1,X0),k2_relat_1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t144_relat_1) ).
fof(f856,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> r1_tarski(k9_relat_1(X1,X0),k9_relat_1(X1,k1_relat_1(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t147_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(f872,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> r1_tarski(k3_xboole_0(k1_relat_1(X1),X0),k9_relat_1(k4_relat_1(X1),k9_relat_1(X1,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t163_relat_1) ).
fof(f907,axiom,
! [X0] :
( v1_relat_1(X0)
=> k4_relat_1(k4_relat_1(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',involutiveness_k4_relat_1) ).
fof(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(f19124,axiom,
! [X0,X1,X2,X3] :
( m2_relset_1(X3,X0,X1)
=> ! [X4] :
( m2_relset_1(X4,X1,X2)
=> ( k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X2,X4,k2_funct_5(X3))
& r1_tarski(k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)),k2_funct_5(X4)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t53_relset_2) ).
fof(f19126,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
=> ! [X3] :
( m2_relset_1(X3,X0,X1)
=> ( r1_tarski(X2,k2_funct_5(X3))
<=> r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t55_relset_2) ).
fof(f19127,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
=> ! [X3] :
( m2_relset_1(X3,X0,X1)
=> ( r1_tarski(X2,k2_funct_5(X3))
<=> r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2)) ) ) ),
inference(negated_conjecture,[status(cth)],[f19126]) ).
fof(f19216,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(f19217,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,[],[f19216]) ).
fof(f19218,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(f19219,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,[],[f19218]) ).
fof(f19280,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(f19282,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ( k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X2,X4,k2_funct_5(X3))
& r1_tarski(k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)),k2_funct_5(X4)) )
| ~ m2_relset_1(X4,X1,X2) )
| ~ m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f19124]) ).
fof(f19284,plain,
? [X0,X1,X2] :
( ? [X3] :
( ( r1_tarski(X2,k2_funct_5(X3))
<~> r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2)) )
& m2_relset_1(X3,X0,X1) )
& m1_subset_1(X2,k1_zfmisc_1(X1)) ),
inference(ennf_transformation,[],[f19127]) ).
fof(f19304,plain,
! [X0,X1] :
( k3_xboole_0(X0,X1) = X0
| ~ r1_tarski(X0,X1) ),
inference(ennf_transformation,[],[f97]) ).
fof(f19315,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(f19316,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(f19377,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(f19392,plain,
! [X0,X1] :
( r1_tarski(k9_relat_1(X1,X0),k9_relat_1(X1,k1_relat_1(X1)))
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f856]) ).
fof(f19395,plain,
! [X0,X1] :
( r1_tarski(k9_relat_1(X1,X0),k2_relat_1(X1))
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f853]) ).
fof(f19594,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f19595,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(flattening,[],[f19594]) ).
fof(f19638,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(f19947,plain,
! [X0] :
( k4_relat_1(k4_relat_1(X0)) = X0
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f907]) ).
fof(f19950,plain,
! [X0,X1] :
( r1_tarski(k3_xboole_0(k1_relat_1(X1),X0),k9_relat_1(k4_relat_1(X1),k9_relat_1(X1,X0)))
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f872]) ).
fof(f19971,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(f19980,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(f19982,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(f20020,plain,
? [X0,X1,X2] :
( ? [X3] :
( ( ~ r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2))
| ~ r1_tarski(X2,k2_funct_5(X3)) )
& ( r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2))
| r1_tarski(X2,k2_funct_5(X3)) )
& m2_relset_1(X3,X0,X1) )
& m1_subset_1(X2,k1_zfmisc_1(X1)) ),
inference(nnf_transformation,[],[f19284]) ).
fof(f20021,plain,
? [X0,X1,X2] :
( ? [X3] :
( ( ~ r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2))
| ~ r1_tarski(X2,k2_funct_5(X3)) )
& ( r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2))
| r1_tarski(X2,k2_funct_5(X3)) )
& m2_relset_1(X3,X0,X1) )
& m1_subset_1(X2,k1_zfmisc_1(X1)) ),
inference(flattening,[],[f20020]) ).
fof(f20022,plain,
( ( ~ r1_tarski(sK18,k10_relset_1(sK17,sK17,k9_relset_2(sK17,sK16,sK17,k6_relset_1(sK16,sK17,sK19),sK19),sK18))
| ~ r1_tarski(sK18,k2_funct_5(sK19)) )
& ( r1_tarski(sK18,k10_relset_1(sK17,sK17,k9_relset_2(sK17,sK16,sK17,k6_relset_1(sK16,sK17,sK19),sK19),sK18))
| r1_tarski(sK18,k2_funct_5(sK19)) )
& m2_relset_1(sK19,sK16,sK17)
& m1_subset_1(sK18,k1_zfmisc_1(sK17)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18,sK19]),skolemize(X0,sK16),skolemize(X1,sK17),skolemize(X2,sK18),skolemize(X3,sK19)],[f20021]) ).
fof(f20033,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(f20312,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[],[f19217]) ).
fof(f20313,plain,
! [X2,X3,X0,X1,X4] :
( ~ 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)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[],[f19219]) ).
fof(f20393,plain,
! [X2,X0,X1] :
( k10_relset_1(X1,X0,X2,X1) = k2_funct_5(X2)
| ~ m2_relset_1(X2,X1,X0) ),
inference(cnf_transformation,[],[f19280]) ).
fof(f20394,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,[],[f19280]) ).
fof(f20397,plain,
! [X2,X3,X0,X1,X4] :
( r1_tarski(k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)),k2_funct_5(X4))
| ~ m2_relset_1(X4,X1,X2)
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f19282]) ).
fof(f20398,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X4,X1,X2)
| k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X2,X4,k2_funct_5(X3))
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f19282]) ).
fof(f20402,plain,
m2_relset_1(sK19,sK16,sK17),
inference(cnf_transformation,[],[f20022]) ).
fof(f20403,plain,
( r1_tarski(sK18,k10_relset_1(sK17,sK17,k9_relset_2(sK17,sK16,sK17,k6_relset_1(sK16,sK17,sK19),sK19),sK18))
| r1_tarski(sK18,k2_funct_5(sK19)) ),
inference(cnf_transformation,[],[f20022]) ).
fof(f20404,plain,
( ~ r1_tarski(sK18,k10_relset_1(sK17,sK17,k9_relset_2(sK17,sK16,sK17,k6_relset_1(sK16,sK17,sK19),sK19),sK18))
| ~ r1_tarski(sK18,k2_funct_5(sK19)) ),
inference(cnf_transformation,[],[f20022]) ).
fof(f20429,plain,
! [X0,X1] :
( k3_xboole_0(X0,X1) = X0
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f19304]) ).
fof(f20441,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f57]) ).
fof(f20459,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20033]) ).
fof(f20465,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,[],[f19315]) ).
fof(f20466,plain,
! [X2,X0,X1] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f19316]) ).
fof(f20520,plain,
! [X2,X0,X1] :
( 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(cnf_transformation,[],[f19377]) ).
fof(f20533,plain,
! [X0,X1] :
( ~ v1_relat_1(X1)
| r1_tarski(k9_relat_1(X1,X0),k9_relat_1(X1,k1_relat_1(X1))) ),
inference(cnf_transformation,[],[f19392]) ).
fof(f20536,plain,
! [X0,X1] :
( ~ v1_relat_1(X1)
| r1_tarski(k9_relat_1(X1,X0),k2_relat_1(X1)) ),
inference(cnf_transformation,[],[f19395]) ).
fof(f20826,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f20878,plain,
! [X2,X0,X1] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(cnf_transformation,[],[f19595]) ).
fof(f20926,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,[],[f19638]) ).
fof(f21408,plain,
! [X0] :
( k4_relat_1(k4_relat_1(X0)) = X0
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f19947]) ).
fof(f21411,plain,
! [X0,X1] :
( r1_tarski(k3_xboole_0(k1_relat_1(X1),X0),k9_relat_1(k4_relat_1(X1),k9_relat_1(X1,X0)))
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f19950]) ).
fof(f21459,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k2_relat_1(X0) = k2_funct_5(X0) ),
inference(cnf_transformation,[],[f19971]) ).
fof(f21460,plain,
! [X0] :
( k1_relat_1(X0) = k1_funct_5(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f19971]) ).
fof(f21501,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f21503,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
inference(cnf_transformation,[],[f19982]) ).
fof(f21549,plain,
! [X0,X1] :
( k4_xboole_0(X0,k4_xboole_0(X0,X1)) = X0
| ~ r1_tarski(X0,X1) ),
inference(definition_unfolding,[],[f20429,f20826]) ).
fof(f21561,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k4_xboole_0(X1,k4_xboole_0(X1,X0)),
inference(definition_unfolding,[],[f20441,f20826,f20826]) ).
fof(f21626,plain,
! [X0,X1] :
( ~ v1_relat_1(X1)
| r1_tarski(k4_xboole_0(k1_relat_1(X1),k4_xboole_0(k1_relat_1(X1),X0)),k9_relat_1(k4_relat_1(X1),k9_relat_1(X1,X0))) ),
inference(definition_unfolding,[],[f21411,f20826]) ).
fof(f21759,definition,
sF216 = k6_relset_1(sK16,sK17,sK19),
introduced(definition,[new_symbols(definition,[sF216])],[function_definition]) ).
fof(f21760,plain,
k6_relset_1(sK16,sK17,sK19) = sF216,
inference(reorient_equations,[],[f21759]) ).
fof(f21761,definition,
sF217 = k9_relset_2(sK17,sK16,sK17,sF216,sK19),
introduced(definition,[new_symbols(definition,[sF217])],[function_definition]) ).
fof(f21762,plain,
k9_relset_2(sK17,sK16,sK17,sF216,sK19) = sF217,
inference(reorient_equations,[],[f21761]) ).
fof(f21763,definition,
sF218 = k10_relset_1(sK17,sK17,sF217,sK18),
introduced(definition,[new_symbols(definition,[sF218])],[function_definition]) ).
fof(f21764,plain,
k10_relset_1(sK17,sK17,sF217,sK18) = sF218,
inference(reorient_equations,[],[f21763]) ).
fof(f21765,definition,
sF219 = k2_funct_5(sK19),
introduced(definition,[new_symbols(definition,[sF219])],[function_definition]) ).
fof(f21766,plain,
k2_funct_5(sK19) = sF219,
inference(reorient_equations,[],[f21765]) ).
fof(f21767,plain,
( ~ r1_tarski(sK18,sF218)
| ~ r1_tarski(sK18,sF219) ),
inference(definition_folding,[],[f20404,f21766,f21764,f21762,f21760]) ).
fof(f21768,plain,
( r1_tarski(sK18,sF218)
| r1_tarski(sK18,sF219) ),
inference(definition_folding,[],[f20403,f21766,f21764,f21762,f21760]) ).
fof(f21938,definition,
( spl221_26
<=> m2_relset_1(sK19,sK16,sK17) ),
introduced(definition,[new_symbols(definition,[spl221_26])],[avatar_definition]) ).
fof(f21940,plain,
( m2_relset_1(sK19,sK16,sK17)
| ~ spl221_26 ),
inference(avatar_component_clause,[],[f21938]) ).
fof(f21941,plain,
spl221_26,
inference(avatar_split_clause,[],[f20402,f21938]) ).
fof(f21943,definition,
( spl221_27
<=> r1_tarski(sK18,sF219) ),
introduced(definition,[new_symbols(definition,[spl221_27])],[avatar_definition]) ).
fof(f21944,plain,
( ~ r1_tarski(sK18,sF219)
| spl221_27 ),
inference(avatar_component_clause,[],[f21943]) ).
fof(f21945,plain,
( r1_tarski(sK18,sF219)
| ~ spl221_27 ),
inference(avatar_component_clause,[],[f21943]) ).
fof(f21947,definition,
( spl221_28
<=> r1_tarski(sK18,sF218) ),
introduced(definition,[new_symbols(definition,[spl221_28])],[avatar_definition]) ).
fof(f21948,plain,
( ~ r1_tarski(sK18,sF218)
| spl221_28 ),
inference(avatar_component_clause,[],[f21947]) ).
fof(f21949,plain,
( r1_tarski(sK18,sF218)
| ~ spl221_28 ),
inference(avatar_component_clause,[],[f21947]) ).
fof(f21950,plain,
( spl221_27
| spl221_28 ),
inference(avatar_split_clause,[],[f21768,f21947,f21943]) ).
fof(f21951,plain,
( ~ spl221_27
| ~ spl221_28 ),
inference(avatar_split_clause,[],[f21767,f21947,f21943]) ).
fof(f21962,definition,
( spl221_30
<=> k6_relset_1(sK16,sK17,sK19) = sF216 ),
introduced(definition,[new_symbols(definition,[spl221_30])],[avatar_definition]) ).
fof(f21964,plain,
( k6_relset_1(sK16,sK17,sK19) = sF216
| ~ spl221_30 ),
inference(avatar_component_clause,[],[f21962]) ).
fof(f21965,plain,
spl221_30,
inference(avatar_split_clause,[],[f21760,f21962]) ).
fof(f21967,definition,
( spl221_31
<=> k9_relset_2(sK17,sK16,sK17,sF216,sK19) = sF217 ),
introduced(definition,[new_symbols(definition,[spl221_31])],[avatar_definition]) ).
fof(f21969,plain,
( k9_relset_2(sK17,sK16,sK17,sF216,sK19) = sF217
| ~ spl221_31 ),
inference(avatar_component_clause,[],[f21967]) ).
fof(f21970,plain,
spl221_31,
inference(avatar_split_clause,[],[f21762,f21967]) ).
fof(f21972,definition,
( spl221_32
<=> k10_relset_1(sK17,sK17,sF217,sK18) = sF218 ),
introduced(definition,[new_symbols(definition,[spl221_32])],[avatar_definition]) ).
fof(f21974,plain,
( k10_relset_1(sK17,sK17,sF217,sK18) = sF218
| ~ spl221_32 ),
inference(avatar_component_clause,[],[f21972]) ).
fof(f21975,plain,
spl221_32,
inference(avatar_split_clause,[],[f21764,f21972]) ).
fof(f21977,definition,
( spl221_33
<=> k2_funct_5(sK19) = sF219 ),
introduced(definition,[new_symbols(definition,[spl221_33])],[avatar_definition]) ).
fof(f21979,plain,
( k2_funct_5(sK19) = sF219
| ~ spl221_33 ),
inference(avatar_component_clause,[],[f21977]) ).
fof(f21980,plain,
spl221_33,
inference(avatar_split_clause,[],[f21766,f21977]) ).
fof(f22013,plain,
( r1_tarski(k2_funct_5(sF217),k2_funct_5(sK19))
| ~ m2_relset_1(sK19,sK16,sK17)
| ~ m2_relset_1(sF216,sK17,sK16)
| ~ spl221_31 ),
inference(superposition,[],[f20397,f21969]) ).
fof(f22014,plain,
( r1_tarski(k2_funct_5(sF217),k2_funct_5(sK19))
| ~ m2_relset_1(sF216,sK17,sK16)
| ~ spl221_26
| ~ spl221_31 ),
inference(forward_subsumption_resolution,[],[f22013,f21940]) ).
fof(f22015,plain,
( r1_tarski(k2_funct_5(sF217),sF219)
| ~ m2_relset_1(sF216,sK17,sK16)
| ~ spl221_26
| ~ spl221_31
| ~ spl221_33 ),
inference(forward_demodulation,[],[f22014,f21979]) ).
fof(f22017,definition,
( spl221_36
<=> m2_relset_1(sF216,sK17,sK16) ),
introduced(definition,[new_symbols(definition,[spl221_36])],[avatar_definition]) ).
fof(f22018,plain,
( m2_relset_1(sF216,sK17,sK16)
| ~ spl221_36 ),
inference(avatar_component_clause,[],[f22017]) ).
fof(f22019,plain,
( ~ m2_relset_1(sF216,sK17,sK16)
| spl221_36 ),
inference(avatar_component_clause,[],[f22017]) ).
fof(f22021,definition,
( spl221_37
<=> r1_tarski(k2_funct_5(sF217),sF219) ),
introduced(definition,[new_symbols(definition,[spl221_37])],[avatar_definition]) ).
fof(f22023,plain,
( r1_tarski(k2_funct_5(sF217),sF219)
| ~ spl221_37 ),
inference(avatar_component_clause,[],[f22021]) ).
fof(f22024,plain,
( ~ spl221_36
| spl221_37
| ~ spl221_26
| ~ spl221_31
| ~ spl221_33 ),
inference(avatar_split_clause,[],[f22015,f21977,f21967,f21938,f22021,f22017]) ).
fof(f22026,plain,
( ! [X0,X1] :
( ~ m2_relset_1(X1,X0,sK16)
| k2_funct_5(k9_relset_2(X0,sK16,sK17,X1,sK19)) = k10_relset_1(sK16,sK17,sK19,k2_funct_5(X1)) )
| ~ spl221_26 ),
inference(resolution,[],[f20398,f21940]) ).
fof(f22028,plain,
( k1_funct_5(sK19) = k10_relset_1(sK17,sK16,k6_relset_1(sK16,sK17,sK19),sK17)
| ~ spl221_26 ),
inference(resolution,[],[f20394,f21940]) ).
fof(f22029,plain,
( k1_funct_5(sK19) = k10_relset_1(sK17,sK16,sF216,sK17)
| ~ spl221_26
| ~ spl221_30 ),
inference(forward_demodulation,[],[f22028,f21964]) ).
fof(f22032,definition,
( spl221_38
<=> k1_funct_5(sK19) = k10_relset_1(sK17,sK16,sF216,sK17) ),
introduced(definition,[new_symbols(definition,[spl221_38])],[avatar_definition]) ).
fof(f22034,plain,
( k1_funct_5(sK19) = k10_relset_1(sK17,sK16,sF216,sK17)
| ~ spl221_38 ),
inference(avatar_component_clause,[],[f22032]) ).
fof(f22035,plain,
( spl221_38
| ~ spl221_26
| ~ spl221_30 ),
inference(avatar_split_clause,[],[f22029,f21962,f21938,f22032]) ).
fof(f22038,plain,
( m1_subset_1(sK19,k1_zfmisc_1(k2_zfmisc_1(sK16,sK17)))
| ~ spl221_26 ),
inference(unit_resulting_resolution,[],[f20465,f21940]) ).
fof(f22039,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X0,X1,X2)
| m2_relset_1(k9_relset_2(X1,X2,X3,X0,X4),X1,X3)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X2,X3))) ),
inference(resolution,[],[f20465,f20312]) ).
fof(f22041,definition,
( spl221_39
<=> m1_subset_1(sK19,k1_zfmisc_1(k2_zfmisc_1(sK16,sK17))) ),
introduced(definition,[new_symbols(definition,[spl221_39])],[avatar_definition]) ).
fof(f22043,plain,
( m1_subset_1(sK19,k1_zfmisc_1(k2_zfmisc_1(sK16,sK17)))
| ~ spl221_39 ),
inference(avatar_component_clause,[],[f22041]) ).
fof(f22044,plain,
( spl221_39
| ~ spl221_26 ),
inference(avatar_split_clause,[],[f22038,f21938,f22041]) ).
fof(f22045,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X0,X2,X3)
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| k5_relat_1(X0,X1) = k9_relset_2(X2,X3,X4,X0,X1) ),
inference(resolution,[],[f20313,f20465]) ).
fof(f22079,plain,
( k1_funct_5(sK19) = k2_funct_5(sF216)
| ~ m2_relset_1(sF216,sK17,sK16)
| ~ spl221_38 ),
inference(superposition,[],[f20393,f22034]) ).
fof(f22082,plain,
( v1_relat_1(sK19)
| ~ spl221_39 ),
inference(unit_resulting_resolution,[],[f20466,f22043]) ).
fof(f22084,definition,
( spl221_44
<=> v1_relat_1(sK19) ),
introduced(definition,[new_symbols(definition,[spl221_44])],[avatar_definition]) ).
fof(f22086,plain,
( v1_relat_1(sK19)
| ~ spl221_44 ),
inference(avatar_component_clause,[],[f22084]) ).
fof(f22087,plain,
( spl221_44
| ~ spl221_39 ),
inference(avatar_split_clause,[],[f22082,f22041,f22084]) ).
fof(f22090,plain,
( k1_funct_5(sK19) = k1_relat_1(sK19)
| ~ spl221_44 ),
inference(unit_resulting_resolution,[],[f21460,f22086]) ).
fof(f22093,definition,
( spl221_45
<=> k1_funct_5(sK19) = k1_relat_1(sK19) ),
introduced(definition,[new_symbols(definition,[spl221_45])],[avatar_definition]) ).
fof(f22095,plain,
( k1_funct_5(sK19) = k1_relat_1(sK19)
| ~ spl221_45 ),
inference(avatar_component_clause,[],[f22093]) ).
fof(f22096,plain,
( spl221_45
| ~ spl221_44 ),
inference(avatar_split_clause,[],[f22090,f22084,f22093]) ).
fof(f22126,plain,
( m1_relset_1(sK19,sK16,sK17)
| ~ spl221_26 ),
inference(resolution,[],[f20459,f21940]) ).
fof(f22128,definition,
( spl221_47
<=> m1_relset_1(sK19,sK16,sK17) ),
introduced(definition,[new_symbols(definition,[spl221_47])],[avatar_definition]) ).
fof(f22130,plain,
( m1_relset_1(sK19,sK16,sK17)
| ~ spl221_47 ),
inference(avatar_component_clause,[],[f22128]) ).
fof(f22131,plain,
( spl221_47
| ~ spl221_26 ),
inference(avatar_split_clause,[],[f22126,f21938,f22128]) ).
fof(f22134,plain,
( m2_relset_1(k6_relset_1(sK16,sK17,sK19),sK17,sK16)
| ~ spl221_47 ),
inference(unit_resulting_resolution,[],[f21503,f22130]) ).
fof(f22138,plain,
( ! [X0] : k10_relset_1(sK16,sK17,sK19,X0) = k9_relat_1(sK19,X0)
| ~ spl221_47 ),
inference(resolution,[],[f22130,f20926]) ).
fof(f22140,plain,
( k6_relset_1(sK16,sK17,sK19) = k4_relat_1(sK19)
| ~ spl221_47 ),
inference(resolution,[],[f22130,f21501]) ).
fof(f22143,plain,
( sF216 = k4_relat_1(sK19)
| ~ spl221_30
| ~ spl221_47 ),
inference(forward_demodulation,[],[f22140,f21964]) ).
fof(f22147,plain,
( m2_relset_1(sF216,sK17,sK16)
| ~ spl221_30
| ~ spl221_47 ),
inference(forward_demodulation,[],[f22134,f21964]) ).
fof(f22152,definition,
( spl221_48
<=> sF216 = k4_relat_1(sK19) ),
introduced(definition,[new_symbols(definition,[spl221_48])],[avatar_definition]) ).
fof(f22154,plain,
( sF216 = k4_relat_1(sK19)
| ~ spl221_48 ),
inference(avatar_component_clause,[],[f22152]) ).
fof(f22155,plain,
( spl221_48
| ~ spl221_30
| ~ spl221_47 ),
inference(avatar_split_clause,[],[f22143,f22128,f21962,f22152]) ).
fof(f22163,plain,
( $false
| ~ spl221_30
| spl221_36
| ~ spl221_47 ),
inference(forward_subsumption_resolution,[],[f22147,f22019]) ).
fof(f22164,plain,
( ~ spl221_30
| spl221_36
| ~ spl221_47 ),
inference(avatar_contradiction_clause,[],[f22163]) ).
fof(f22166,plain,
( k1_funct_5(sK19) = k2_funct_5(sF216)
| ~ spl221_36
| ~ spl221_38 ),
inference(forward_subsumption_resolution,[],[f22079,f22018]) ).
fof(f22168,plain,
( k2_funct_5(sF216) = k1_relat_1(sK19)
| ~ spl221_36
| ~ spl221_38
| ~ spl221_45 ),
inference(forward_demodulation,[],[f22166,f22095]) ).
fof(f22171,definition,
( spl221_50
<=> k2_funct_5(sF216) = k1_relat_1(sK19) ),
introduced(definition,[new_symbols(definition,[spl221_50])],[avatar_definition]) ).
fof(f22173,plain,
( k2_funct_5(sF216) = k1_relat_1(sK19)
| ~ spl221_50 ),
inference(avatar_component_clause,[],[f22171]) ).
fof(f22174,plain,
( spl221_50
| ~ spl221_36
| ~ spl221_38
| ~ spl221_45 ),
inference(avatar_split_clause,[],[f22168,f22093,f22032,f22017,f22171]) ).
fof(f22178,plain,
( k2_funct_5(sK19) = k9_relat_1(sK19,sK16)
| ~ m2_relset_1(sK19,sK16,sK17)
| ~ spl221_47 ),
inference(superposition,[],[f20393,f22138]) ).
fof(f22179,plain,
( k2_funct_5(sK19) = k9_relat_1(sK19,sK16)
| ~ spl221_26
| ~ spl221_47 ),
inference(forward_subsumption_resolution,[],[f22178,f21940]) ).
fof(f22181,definition,
( spl221_51
<=> sF219 = k9_relat_1(sK19,sK16) ),
introduced(definition,[new_symbols(definition,[spl221_51])],[avatar_definition]) ).
fof(f22183,plain,
( sF219 = k9_relat_1(sK19,sK16)
| ~ spl221_51 ),
inference(avatar_component_clause,[],[f22181]) ).
fof(f22186,plain,
( sF219 = k9_relat_1(sK19,sK16)
| ~ spl221_26
| ~ spl221_33
| ~ spl221_47 ),
inference(forward_demodulation,[],[f22179,f21979]) ).
fof(f22188,plain,
( spl221_51
| ~ spl221_26
| ~ spl221_33
| ~ spl221_47 ),
inference(avatar_split_clause,[],[f22186,f22128,f21977,f21938,f22181]) ).
fof(f22202,plain,
( m1_subset_1(sF216,k1_zfmisc_1(k2_zfmisc_1(sK17,sK16)))
| ~ spl221_36 ),
inference(unit_resulting_resolution,[],[f20465,f22018]) ).
fof(f22204,plain,
( m2_relset_1(k9_relset_2(sK17,sK16,sK17,sF216,sK19),sK17,sK17)
| ~ spl221_36
| ~ spl221_39 ),
inference(unit_resulting_resolution,[],[f22039,f22043,f22018]) ).
fof(f22205,plain,
( k9_relset_2(sK17,sK16,sK17,sF216,sK19) = k5_relat_1(sF216,sK19)
| ~ spl221_36
| ~ spl221_39 ),
inference(unit_resulting_resolution,[],[f22045,f22043,f22018]) ).
fof(f22207,plain,
( k2_funct_5(k9_relset_2(sK17,sK16,sK17,sF216,sK19)) = k10_relset_1(sK16,sK17,sK19,k2_funct_5(sF216))
| ~ spl221_26
| ~ spl221_36 ),
inference(resolution,[],[f22018,f22026]) ).
fof(f22208,plain,
( k1_funct_5(sF216) = k10_relset_1(sK16,sK17,k6_relset_1(sK17,sK16,sF216),sK16)
| ~ spl221_36 ),
inference(resolution,[],[f22018,f20394]) ).
fof(f22213,plain,
( m1_relset_1(sF216,sK17,sK16)
| ~ spl221_36 ),
inference(resolution,[],[f22018,f20459]) ).
fof(f22217,definition,
( spl221_52
<=> m1_relset_1(sF216,sK17,sK16) ),
introduced(definition,[new_symbols(definition,[spl221_52])],[avatar_definition]) ).
fof(f22219,plain,
( m1_relset_1(sF216,sK17,sK16)
| ~ spl221_52 ),
inference(avatar_component_clause,[],[f22217]) ).
fof(f22220,plain,
( spl221_52
| ~ spl221_36 ),
inference(avatar_split_clause,[],[f22213,f22017,f22217]) ).
fof(f22223,definition,
( spl221_53
<=> k1_funct_5(sF216) = k10_relset_1(sK16,sK17,k6_relset_1(sK17,sK16,sF216),sK16) ),
introduced(definition,[new_symbols(definition,[spl221_53])],[avatar_definition]) ).
fof(f22225,plain,
( k1_funct_5(sF216) = k10_relset_1(sK16,sK17,k6_relset_1(sK17,sK16,sF216),sK16)
| ~ spl221_53 ),
inference(avatar_component_clause,[],[f22223]) ).
fof(f22226,plain,
( spl221_53
| ~ spl221_36 ),
inference(avatar_split_clause,[],[f22208,f22017,f22223]) ).
fof(f22227,plain,
( k2_funct_5(k9_relset_2(sK17,sK16,sK17,sF216,sK19)) = k9_relat_1(sK19,k2_funct_5(sF216))
| ~ spl221_26
| ~ spl221_36
| ~ spl221_47 ),
inference(forward_demodulation,[],[f22207,f22138]) ).
fof(f22241,definition,
( spl221_54
<=> m1_subset_1(sF216,k1_zfmisc_1(k2_zfmisc_1(sK17,sK16))) ),
introduced(definition,[new_symbols(definition,[spl221_54])],[avatar_definition]) ).
fof(f22243,plain,
( m1_subset_1(sF216,k1_zfmisc_1(k2_zfmisc_1(sK17,sK16)))
| ~ spl221_54 ),
inference(avatar_component_clause,[],[f22241]) ).
fof(f22244,plain,
( spl221_54
| ~ spl221_36 ),
inference(avatar_split_clause,[],[f22202,f22017,f22241]) ).
fof(f22246,plain,
( m2_relset_1(sF217,sK17,sK17)
| ~ spl221_31
| ~ spl221_36
| ~ spl221_39 ),
inference(forward_demodulation,[],[f22204,f21969]) ).
fof(f22247,plain,
( sF217 = k5_relat_1(sF216,sK19)
| ~ spl221_31
| ~ spl221_36
| ~ spl221_39 ),
inference(forward_demodulation,[],[f22205,f21969]) ).
fof(f22248,plain,
( k2_funct_5(k9_relset_2(sK17,sK16,sK17,sF216,sK19)) = k9_relat_1(sK19,k1_relat_1(sK19))
| ~ spl221_26
| ~ spl221_36
| ~ spl221_47
| ~ spl221_50 ),
inference(forward_demodulation,[],[f22227,f22173]) ).
fof(f22286,definition,
( spl221_61
<=> m2_relset_1(sF217,sK17,sK17) ),
introduced(definition,[new_symbols(definition,[spl221_61])],[avatar_definition]) ).
fof(f22288,plain,
( m2_relset_1(sF217,sK17,sK17)
| ~ spl221_61 ),
inference(avatar_component_clause,[],[f22286]) ).
fof(f22289,plain,
( spl221_61
| ~ spl221_31
| ~ spl221_36
| ~ spl221_39 ),
inference(avatar_split_clause,[],[f22246,f22041,f22017,f21967,f22286]) ).
fof(f22291,definition,
( spl221_62
<=> sF217 = k5_relat_1(sF216,sK19) ),
introduced(definition,[new_symbols(definition,[spl221_62])],[avatar_definition]) ).
fof(f22293,plain,
( sF217 = k5_relat_1(sF216,sK19)
| ~ spl221_62 ),
inference(avatar_component_clause,[],[f22291]) ).
fof(f22294,plain,
( spl221_62
| ~ spl221_31
| ~ spl221_36
| ~ spl221_39 ),
inference(avatar_split_clause,[],[f22247,f22041,f22017,f21967,f22291]) ).
fof(f22295,plain,
( k2_funct_5(sF217) = k9_relat_1(sK19,k1_relat_1(sK19))
| ~ spl221_26
| ~ spl221_31
| ~ spl221_36
| ~ spl221_47
| ~ spl221_50 ),
inference(forward_demodulation,[],[f22248,f21969]) ).
fof(f22304,definition,
( spl221_64
<=> k2_funct_5(sF217) = k9_relat_1(sK19,k1_relat_1(sK19)) ),
introduced(definition,[new_symbols(definition,[spl221_64])],[avatar_definition]) ).
fof(f22306,plain,
( k2_funct_5(sF217) = k9_relat_1(sK19,k1_relat_1(sK19))
| ~ spl221_64 ),
inference(avatar_component_clause,[],[f22304]) ).
fof(f22307,plain,
( spl221_64
| ~ spl221_26
| ~ spl221_31
| ~ spl221_36
| ~ spl221_47
| ~ spl221_50 ),
inference(avatar_split_clause,[],[f22295,f22171,f22128,f22017,f21967,f21938,f22304]) ).
fof(f22327,plain,
( m1_subset_1(sF217,k1_zfmisc_1(k2_zfmisc_1(sK17,sK17)))
| ~ spl221_61 ),
inference(unit_resulting_resolution,[],[f20465,f22288]) ).
fof(f22333,plain,
( m1_relset_1(sF217,sK17,sK17)
| ~ spl221_61 ),
inference(resolution,[],[f22288,f20459]) ).
fof(f22337,definition,
( spl221_65
<=> m1_relset_1(sF217,sK17,sK17) ),
introduced(definition,[new_symbols(definition,[spl221_65])],[avatar_definition]) ).
fof(f22339,plain,
( m1_relset_1(sF217,sK17,sK17)
| ~ spl221_65 ),
inference(avatar_component_clause,[],[f22337]) ).
fof(f22340,plain,
( spl221_65
| ~ spl221_61 ),
inference(avatar_split_clause,[],[f22333,f22286,f22337]) ).
fof(f22397,definition,
( spl221_76
<=> m1_subset_1(sF217,k1_zfmisc_1(k2_zfmisc_1(sK17,sK17))) ),
introduced(definition,[new_symbols(definition,[spl221_76])],[avatar_definition]) ).
fof(f22399,plain,
( m1_subset_1(sF217,k1_zfmisc_1(k2_zfmisc_1(sK17,sK17)))
| ~ spl221_76 ),
inference(avatar_component_clause,[],[f22397]) ).
fof(f22400,plain,
( spl221_76
| ~ spl221_61 ),
inference(avatar_split_clause,[],[f22327,f22286,f22397]) ).
fof(f22458,plain,
( m2_relset_1(k6_relset_1(sK17,sK16,sF216),sK16,sK17)
| ~ spl221_52 ),
inference(resolution,[],[f22219,f21503]) ).
fof(f22459,plain,
( k6_relset_1(sK17,sK16,sF216) = k4_relat_1(sF216)
| ~ spl221_52 ),
inference(resolution,[],[f22219,f21501]) ).
fof(f22462,definition,
( spl221_85
<=> k6_relset_1(sK17,sK16,sF216) = k4_relat_1(sF216) ),
introduced(definition,[new_symbols(definition,[spl221_85])],[avatar_definition]) ).
fof(f22464,plain,
( k6_relset_1(sK17,sK16,sF216) = k4_relat_1(sF216)
| ~ spl221_85 ),
inference(avatar_component_clause,[],[f22462]) ).
fof(f22465,plain,
( spl221_85
| ~ spl221_52 ),
inference(avatar_split_clause,[],[f22459,f22217,f22462]) ).
fof(f22467,definition,
( spl221_86
<=> m2_relset_1(k6_relset_1(sK17,sK16,sF216),sK16,sK17) ),
introduced(definition,[new_symbols(definition,[spl221_86])],[avatar_definition]) ).
fof(f22469,plain,
( m2_relset_1(k6_relset_1(sK17,sK16,sF216),sK16,sK17)
| ~ spl221_86 ),
inference(avatar_component_clause,[],[f22467]) ).
fof(f22470,plain,
( spl221_86
| ~ spl221_52 ),
inference(avatar_split_clause,[],[f22458,f22217,f22467]) ).
fof(f22476,plain,
( m2_relset_1(k4_relat_1(sF216),sK16,sK17)
| ~ spl221_85
| ~ spl221_86 ),
inference(forward_demodulation,[],[f22469,f22464]) ).
fof(f22479,definition,
( spl221_88
<=> m2_relset_1(k4_relat_1(sF216),sK16,sK17) ),
introduced(definition,[new_symbols(definition,[spl221_88])],[avatar_definition]) ).
fof(f22481,plain,
( m2_relset_1(k4_relat_1(sF216),sK16,sK17)
| ~ spl221_88 ),
inference(avatar_component_clause,[],[f22479]) ).
fof(f22482,plain,
( spl221_88
| ~ spl221_85
| ~ spl221_86 ),
inference(avatar_split_clause,[],[f22476,f22467,f22462,f22479]) ).
fof(f22551,plain,
( ! [X0] : k10_relset_1(sK17,sK17,sF217,X0) = k9_relat_1(sF217,X0)
| ~ spl221_65 ),
inference(resolution,[],[f22339,f20926]) ).
fof(f22588,plain,
( sF218 = k9_relat_1(sF217,sK18)
| ~ spl221_32
| ~ spl221_65 ),
inference(superposition,[],[f21974,f22551]) ).
fof(f22598,definition,
( spl221_100
<=> sF218 = k9_relat_1(sF217,sK18) ),
introduced(definition,[new_symbols(definition,[spl221_100])],[avatar_definition]) ).
fof(f22600,plain,
( sF218 = k9_relat_1(sF217,sK18)
| ~ spl221_100 ),
inference(avatar_component_clause,[],[f22598]) ).
fof(f22601,plain,
( spl221_100
| ~ spl221_32
| ~ spl221_65 ),
inference(avatar_split_clause,[],[f22588,f22337,f21972,f22598]) ).
fof(f22648,plain,
( v1_relat_1(sF217)
| ~ spl221_76 ),
inference(unit_resulting_resolution,[],[f20466,f22399]) ).
fof(f22677,definition,
( spl221_108
<=> v1_relat_1(sF217) ),
introduced(definition,[new_symbols(definition,[spl221_108])],[avatar_definition]) ).
fof(f22679,plain,
( v1_relat_1(sF217)
| ~ spl221_108 ),
inference(avatar_component_clause,[],[f22677]) ).
fof(f22680,plain,
( spl221_108
| ~ spl221_76 ),
inference(avatar_split_clause,[],[f22648,f22397,f22677]) ).
fof(f22709,plain,
( v1_relat_1(sF216)
| ~ spl221_54 ),
inference(unit_resulting_resolution,[],[f20466,f22243]) ).
fof(f22740,definition,
( spl221_115
<=> v1_relat_1(sF216) ),
introduced(definition,[new_symbols(definition,[spl221_115])],[avatar_definition]) ).
fof(f22742,plain,
( v1_relat_1(sF216)
| ~ spl221_115 ),
inference(avatar_component_clause,[],[f22740]) ).
fof(f22743,plain,
( spl221_115
| ~ spl221_54 ),
inference(avatar_split_clause,[],[f22709,f22241,f22740]) ).
fof(f22754,plain,
( k1_funct_5(sF216) = k1_relat_1(sF216)
| ~ spl221_115 ),
inference(unit_resulting_resolution,[],[f21460,f22742]) ).
fof(f22756,definition,
( spl221_117
<=> k1_funct_5(sF216) = k1_relat_1(sF216) ),
introduced(definition,[new_symbols(definition,[spl221_117])],[avatar_definition]) ).
fof(f22758,plain,
( k1_funct_5(sF216) = k1_relat_1(sF216)
| ~ spl221_117 ),
inference(avatar_component_clause,[],[f22756]) ).
fof(f22759,plain,
( spl221_117
| ~ spl221_115 ),
inference(avatar_split_clause,[],[f22754,f22740,f22756]) ).
fof(f22806,plain,
( k1_funct_5(sF216) = k2_funct_5(k6_relset_1(sK17,sK16,sF216))
| ~ m2_relset_1(k6_relset_1(sK17,sK16,sF216),sK16,sK17)
| ~ spl221_53 ),
inference(superposition,[],[f20393,f22225]) ).
fof(f22807,plain,
( k1_funct_5(sF216) = k2_funct_5(k4_relat_1(sF216))
| ~ m2_relset_1(k6_relset_1(sK17,sK16,sF216),sK16,sK17)
| ~ spl221_53
| ~ spl221_85 ),
inference(forward_demodulation,[],[f22806,f22464]) ).
fof(f22810,plain,
( k1_relat_1(sF216) = k2_funct_5(k4_relat_1(sF216))
| ~ m2_relset_1(k6_relset_1(sK17,sK16,sF216),sK16,sK17)
| ~ spl221_53
| ~ spl221_85
| ~ spl221_117 ),
inference(forward_demodulation,[],[f22807,f22758]) ).
fof(f22817,plain,
( ~ m2_relset_1(k4_relat_1(sF216),sK16,sK17)
| k1_relat_1(sF216) = k2_funct_5(k4_relat_1(sF216))
| ~ spl221_53
| ~ spl221_85
| ~ spl221_117 ),
inference(forward_demodulation,[],[f22810,f22464]) ).
fof(f22819,plain,
( k1_relat_1(sF216) = k2_funct_5(k4_relat_1(sF216))
| ~ spl221_53
| ~ spl221_85
| ~ spl221_88
| ~ spl221_117 ),
inference(forward_subsumption_resolution,[],[f22817,f22481]) ).
fof(f22822,definition,
( spl221_123
<=> k1_relat_1(sF216) = k2_funct_5(k4_relat_1(sF216)) ),
introduced(definition,[new_symbols(definition,[spl221_123])],[avatar_definition]) ).
fof(f22824,plain,
( k1_relat_1(sF216) = k2_funct_5(k4_relat_1(sF216))
| ~ spl221_123 ),
inference(avatar_component_clause,[],[f22822]) ).
fof(f22825,plain,
( spl221_123
| ~ spl221_53
| ~ spl221_85
| ~ spl221_88
| ~ spl221_117 ),
inference(avatar_split_clause,[],[f22819,f22756,f22479,f22462,f22223,f22822]) ).
fof(f22873,plain,
( sK19 = k4_relat_1(sF216)
| ~ v1_relat_1(sK19)
| ~ spl221_48 ),
inference(superposition,[],[f21408,f22154]) ).
fof(f22874,plain,
( sK19 = k4_relat_1(sF216)
| ~ spl221_44
| ~ spl221_48 ),
inference(forward_subsumption_resolution,[],[f22873,f22086]) ).
fof(f22887,definition,
( spl221_131
<=> sK19 = k4_relat_1(sF216) ),
introduced(definition,[new_symbols(definition,[spl221_131])],[avatar_definition]) ).
fof(f22889,plain,
( sK19 = k4_relat_1(sF216)
| ~ spl221_131 ),
inference(avatar_component_clause,[],[f22887]) ).
fof(f22890,plain,
( spl221_131
| ~ spl221_44
| ~ spl221_48 ),
inference(avatar_split_clause,[],[f22874,f22152,f22084,f22887]) ).
fof(f23009,plain,
( ! [X0] : r1_tarski(k9_relat_1(sK19,X0),k9_relat_1(sK19,k1_relat_1(sK19)))
| ~ spl221_44 ),
inference(resolution,[],[f20533,f22086]) ).
fof(f23012,plain,
( ! [X0] : r1_tarski(k9_relat_1(sK19,X0),k2_funct_5(sF217))
| ~ spl221_44
| ~ spl221_64 ),
inference(forward_demodulation,[],[f23009,f22306]) ).
fof(f23021,plain,
( r1_tarski(sF219,k2_funct_5(sF217))
| ~ spl221_44
| ~ spl221_51
| ~ spl221_64 ),
inference(superposition,[],[f23012,f22183]) ).
fof(f23024,definition,
( spl221_144
<=> r1_tarski(sF219,k2_funct_5(sF217)) ),
introduced(definition,[new_symbols(definition,[spl221_144])],[avatar_definition]) ).
fof(f23026,plain,
( r1_tarski(sF219,k2_funct_5(sF217))
| ~ spl221_144 ),
inference(avatar_component_clause,[],[f23024]) ).
fof(f23027,plain,
( spl221_144
| ~ spl221_44
| ~ spl221_51
| ~ spl221_64 ),
inference(avatar_split_clause,[],[f23021,f22304,f22181,f22084,f23024]) ).
fof(f23209,plain,
( ~ r1_tarski(sF218,sF219)
| spl221_27
| ~ spl221_28 ),
inference(unit_resulting_resolution,[],[f20878,f21949,f21944]) ).
fof(f23222,definition,
( spl221_160
<=> r1_tarski(sF218,sF219) ),
introduced(definition,[new_symbols(definition,[spl221_160])],[avatar_definition]) ).
fof(f23224,plain,
( ~ r1_tarski(sF218,sF219)
| spl221_160 ),
inference(avatar_component_clause,[],[f23222]) ).
fof(f23225,plain,
( ~ spl221_160
| spl221_27
| ~ spl221_28 ),
inference(avatar_split_clause,[],[f23209,f21947,f21943,f23222]) ).
fof(f24207,plain,
( k2_funct_5(sF217) = k4_xboole_0(k2_funct_5(sF217),k4_xboole_0(k2_funct_5(sF217),sF219))
| ~ spl221_37 ),
inference(unit_resulting_resolution,[],[f21549,f22023]) ).
fof(f24209,plain,
( sF219 = k4_xboole_0(sF219,k4_xboole_0(sF219,k2_funct_5(sF217)))
| ~ spl221_144 ),
inference(unit_resulting_resolution,[],[f21549,f23026]) ).
fof(f24232,plain,
( k2_funct_5(sF217) = k4_xboole_0(sF219,k4_xboole_0(sF219,k2_funct_5(sF217)))
| ~ spl221_37 ),
inference(forward_demodulation,[],[f24207,f21561]) ).
fof(f24239,definition,
( spl221_210
<=> sF219 = k4_xboole_0(sF219,k4_xboole_0(sF219,k2_funct_5(sF217))) ),
introduced(definition,[new_symbols(definition,[spl221_210])],[avatar_definition]) ).
fof(f24241,plain,
( sF219 = k4_xboole_0(sF219,k4_xboole_0(sF219,k2_funct_5(sF217)))
| ~ spl221_210 ),
inference(avatar_component_clause,[],[f24239]) ).
fof(f24242,plain,
( spl221_210
| ~ spl221_144 ),
inference(avatar_split_clause,[],[f24209,f23024,f24239]) ).
fof(f24259,definition,
( spl221_213
<=> k2_funct_5(sF217) = k4_xboole_0(sF219,k4_xboole_0(sF219,k2_funct_5(sF217))) ),
introduced(definition,[new_symbols(definition,[spl221_213])],[avatar_definition]) ).
fof(f24261,plain,
( k2_funct_5(sF217) = k4_xboole_0(sF219,k4_xboole_0(sF219,k2_funct_5(sF217)))
| ~ spl221_213 ),
inference(avatar_component_clause,[],[f24259]) ).
fof(f24262,plain,
( spl221_213
| ~ spl221_37 ),
inference(avatar_split_clause,[],[f24232,f22021,f24259]) ).
fof(f24289,plain,
( sF219 = k2_funct_5(sF217)
| ~ spl221_210
| ~ spl221_213 ),
inference(forward_demodulation,[],[f24261,f24241]) ).
fof(f24291,definition,
( spl221_217
<=> sF219 = k2_funct_5(sF217) ),
introduced(definition,[new_symbols(definition,[spl221_217])],[avatar_definition]) ).
fof(f24293,plain,
( sF219 = k2_funct_5(sF217)
| ~ spl221_217 ),
inference(avatar_component_clause,[],[f24291]) ).
fof(f24294,plain,
( spl221_217
| ~ spl221_210
| ~ spl221_213 ),
inference(avatar_split_clause,[],[f24289,f24259,f24239,f24291]) ).
fof(f24624,plain,
( k2_funct_5(sF217) = k2_relat_1(sF217)
| ~ spl221_108 ),
inference(resolution,[],[f21459,f22679]) ).
fof(f24625,plain,
( sF219 = k2_relat_1(sF217)
| ~ spl221_108
| ~ spl221_217 ),
inference(forward_demodulation,[],[f24624,f24293]) ).
fof(f24632,definition,
( spl221_233
<=> sF219 = k2_relat_1(sF217) ),
introduced(definition,[new_symbols(definition,[spl221_233])],[avatar_definition]) ).
fof(f24634,plain,
( sF219 = k2_relat_1(sF217)
| ~ spl221_233 ),
inference(avatar_component_clause,[],[f24632]) ).
fof(f24635,plain,
( spl221_233
| ~ spl221_108
| ~ spl221_217 ),
inference(avatar_split_clause,[],[f24625,f24291,f22677,f24632]) ).
fof(f24718,plain,
( k2_funct_5(sK19) = k1_relat_1(sF216)
| ~ spl221_123
| ~ spl221_131 ),
inference(superposition,[],[f22824,f22889]) ).
fof(f24721,plain,
( sF219 = k1_relat_1(sF216)
| ~ spl221_33
| ~ spl221_123
| ~ spl221_131 ),
inference(forward_demodulation,[],[f24718,f21979]) ).
fof(f24724,definition,
( spl221_237
<=> sF219 = k1_relat_1(sF216) ),
introduced(definition,[new_symbols(definition,[spl221_237])],[avatar_definition]) ).
fof(f24726,plain,
( sF219 = k1_relat_1(sF216)
| ~ spl221_237 ),
inference(avatar_component_clause,[],[f24724]) ).
fof(f24727,plain,
( spl221_237
| ~ spl221_33
| ~ spl221_123
| ~ spl221_131 ),
inference(avatar_split_clause,[],[f24721,f22887,f22822,f21977,f24724]) ).
fof(f25608,plain,
( ! [X0] : r1_tarski(k9_relat_1(sF217,X0),k2_relat_1(sF217))
| ~ spl221_108 ),
inference(resolution,[],[f20536,f22679]) ).
fof(f25609,plain,
( ! [X0] : r1_tarski(k9_relat_1(sF217,X0),sF219)
| ~ spl221_108
| ~ spl221_233 ),
inference(forward_demodulation,[],[f25608,f24634]) ).
fof(f25654,plain,
( r1_tarski(sF218,sF219)
| ~ spl221_100
| ~ spl221_108
| ~ spl221_233 ),
inference(superposition,[],[f25609,f22600]) ).
fof(f25657,plain,
( $false
| ~ spl221_100
| ~ spl221_108
| spl221_160
| ~ spl221_233 ),
inference(forward_subsumption_resolution,[],[f25654,f23224]) ).
fof(f25658,plain,
( ~ spl221_100
| ~ spl221_108
| spl221_160
| ~ spl221_233 ),
inference(avatar_contradiction_clause,[],[f25657]) ).
fof(f25802,plain,
( sK18 = k4_xboole_0(sK18,k4_xboole_0(sK18,sF219))
| ~ spl221_27 ),
inference(unit_resulting_resolution,[],[f21549,f21945]) ).
fof(f25840,definition,
( spl221_300
<=> sK18 = k4_xboole_0(sK18,k4_xboole_0(sK18,sF219)) ),
introduced(definition,[new_symbols(definition,[spl221_300])],[avatar_definition]) ).
fof(f25842,plain,
( sK18 = k4_xboole_0(sK18,k4_xboole_0(sK18,sF219))
| ~ spl221_300 ),
inference(avatar_component_clause,[],[f25840]) ).
fof(f25843,plain,
( spl221_300
| ~ spl221_27 ),
inference(avatar_split_clause,[],[f25802,f21943,f25840]) ).
fof(f34482,plain,
( ! [X0] : k9_relat_1(sK19,k9_relat_1(sF216,X0)) = k9_relat_1(k5_relat_1(sF216,sK19),X0)
| ~ spl221_44
| ~ spl221_115 ),
inference(unit_resulting_resolution,[],[f20520,f22742,f22086]) ).
fof(f34491,plain,
( ! [X0] : k9_relat_1(sF217,X0) = k9_relat_1(sK19,k9_relat_1(sF216,X0))
| ~ spl221_44
| ~ spl221_62
| ~ spl221_115 ),
inference(forward_demodulation,[],[f34482,f22293]) ).
fof(f35859,plain,
( ! [X0] : r1_tarski(k4_xboole_0(k1_relat_1(sF216),k4_xboole_0(k1_relat_1(sF216),X0)),k9_relat_1(k4_relat_1(sF216),k9_relat_1(sF216,X0)))
| ~ spl221_115 ),
inference(resolution,[],[f21626,f22742]) ).
fof(f35861,plain,
( ! [X0] : r1_tarski(k4_xboole_0(k1_relat_1(sF216),k4_xboole_0(k1_relat_1(sF216),X0)),k9_relat_1(sK19,k9_relat_1(sF216,X0)))
| ~ spl221_115
| ~ spl221_131 ),
inference(forward_demodulation,[],[f35859,f22889]) ).
fof(f35865,plain,
( ! [X0] : r1_tarski(k4_xboole_0(k1_relat_1(sF216),k4_xboole_0(k1_relat_1(sF216),X0)),k9_relat_1(sF217,X0))
| ~ spl221_44
| ~ spl221_62
| ~ spl221_115
| ~ spl221_131 ),
inference(forward_demodulation,[],[f35861,f34491]) ).
fof(f35867,plain,
( ! [X0] : r1_tarski(k4_xboole_0(sF219,k4_xboole_0(sF219,X0)),k9_relat_1(sF217,X0))
| ~ spl221_44
| ~ spl221_62
| ~ spl221_115
| ~ spl221_131
| ~ spl221_237 ),
inference(forward_demodulation,[],[f35865,f24726]) ).
fof(f36021,plain,
( r1_tarski(k4_xboole_0(sF219,k4_xboole_0(sF219,sK18)),sF218)
| ~ spl221_44
| ~ spl221_62
| ~ spl221_100
| ~ spl221_115
| ~ spl221_131
| ~ spl221_237 ),
inference(superposition,[],[f35867,f22600]) ).
fof(f36024,plain,
( r1_tarski(k4_xboole_0(sK18,k4_xboole_0(sK18,sF219)),sF218)
| ~ spl221_44
| ~ spl221_62
| ~ spl221_100
| ~ spl221_115
| ~ spl221_131
| ~ spl221_237 ),
inference(forward_demodulation,[],[f36021,f21561]) ).
fof(f36049,plain,
( r1_tarski(sK18,sF218)
| ~ spl221_44
| ~ spl221_62
| ~ spl221_100
| ~ spl221_115
| ~ spl221_131
| ~ spl221_237
| ~ spl221_300 ),
inference(forward_demodulation,[],[f36024,f25842]) ).
fof(f36059,plain,
( $false
| spl221_28
| ~ spl221_44
| ~ spl221_62
| ~ spl221_100
| ~ spl221_115
| ~ spl221_131
| ~ spl221_237
| ~ spl221_300 ),
inference(forward_subsumption_resolution,[],[f36049,f21948]) ).
fof(f36060,plain,
( spl221_28
| ~ spl221_44
| ~ spl221_62
| ~ spl221_100
| ~ spl221_115
| ~ spl221_131
| ~ spl221_237
| ~ spl221_300 ),
inference(avatar_contradiction_clause,[],[f36059]) ).
cnf(s29,plain,
spl221_26,
inference(sat_conversion,[],[f21941]) ).
cnf(s30,plain,
( spl221_27
| spl221_28 ),
inference(sat_conversion,[],[f21950]) ).
cnf(s31,plain,
( ~ spl221_27
| ~ spl221_28 ),
inference(sat_conversion,[],[f21951]) ).
cnf(s33,plain,
spl221_30,
inference(sat_conversion,[],[f21965]) ).
cnf(s34,plain,
spl221_31,
inference(sat_conversion,[],[f21970]) ).
cnf(s35,plain,
spl221_32,
inference(sat_conversion,[],[f21975]) ).
cnf(s36,plain,
spl221_33,
inference(sat_conversion,[],[f21980]) ).
cnf(s40,plain,
( ~ spl221_26
| ~ spl221_31
| ~ spl221_33
| ~ spl221_36
| spl221_37 ),
inference(sat_conversion,[],[f22024]) ).
cnf(s41,plain,
( ~ spl221_26
| ~ spl221_30
| spl221_38 ),
inference(sat_conversion,[],[f22035]) ).
cnf(s43,plain,
( ~ spl221_26
| spl221_39 ),
inference(sat_conversion,[],[f22044]) ).
cnf(s48,plain,
( ~ spl221_39
| spl221_44 ),
inference(sat_conversion,[],[f22087]) ).
cnf(s49,plain,
( ~ spl221_44
| spl221_45 ),
inference(sat_conversion,[],[f22096]) ).
cnf(s51,plain,
( ~ spl221_26
| spl221_47 ),
inference(sat_conversion,[],[f22131]) ).
cnf(s53,plain,
( ~ spl221_30
| ~ spl221_47
| spl221_48 ),
inference(sat_conversion,[],[f22155]) ).
cnf(s57,plain,
( ~ spl221_30
| spl221_36
| ~ spl221_47 ),
inference(sat_conversion,[],[f22164]) ).
cnf(s59,plain,
( ~ spl221_36
| ~ spl221_38
| ~ spl221_45
| spl221_50 ),
inference(sat_conversion,[],[f22174]) ).
cnf(s63,plain,
( ~ spl221_26
| ~ spl221_33
| ~ spl221_47
| spl221_51 ),
inference(sat_conversion,[],[f22188]) ).
cnf(s65,plain,
( ~ spl221_36
| spl221_52 ),
inference(sat_conversion,[],[f22220]) ).
cnf(s66,plain,
( ~ spl221_36
| spl221_53 ),
inference(sat_conversion,[],[f22226]) ).
cnf(s69,plain,
( ~ spl221_36
| spl221_54 ),
inference(sat_conversion,[],[f22244]) ).
cnf(s76,plain,
( ~ spl221_31
| ~ spl221_36
| ~ spl221_39
| spl221_61 ),
inference(sat_conversion,[],[f22289]) ).
cnf(s77,plain,
( ~ spl221_31
| ~ spl221_36
| ~ spl221_39
| spl221_62 ),
inference(sat_conversion,[],[f22294]) ).
cnf(s81,plain,
( ~ spl221_26
| ~ spl221_31
| ~ spl221_36
| ~ spl221_47
| ~ spl221_50
| spl221_64 ),
inference(sat_conversion,[],[f22307]) ).
cnf(s84,plain,
( ~ spl221_61
| spl221_65 ),
inference(sat_conversion,[],[f22340]) ).
cnf(s101,plain,
( ~ spl221_61
| spl221_76 ),
inference(sat_conversion,[],[f22400]) ).
cnf(s110,plain,
( ~ spl221_52
| spl221_85 ),
inference(sat_conversion,[],[f22465]) ).
cnf(s111,plain,
( ~ spl221_52
| spl221_86 ),
inference(sat_conversion,[],[f22470]) ).
cnf(s116,plain,
( ~ spl221_85
| ~ spl221_86
| spl221_88 ),
inference(sat_conversion,[],[f22482]) ).
cnf(s135,plain,
( ~ spl221_32
| ~ spl221_65
| spl221_100 ),
inference(sat_conversion,[],[f22601]) ).
cnf(s150,plain,
( ~ spl221_76
| spl221_108 ),
inference(sat_conversion,[],[f22680]) ).
cnf(s163,plain,
( ~ spl221_54
| spl221_115 ),
inference(sat_conversion,[],[f22743]) ).
cnf(s169,plain,
( ~ spl221_115
| spl221_117 ),
inference(sat_conversion,[],[f22759]) ).
cnf(s175,plain,
( ~ spl221_53
| ~ spl221_85
| ~ spl221_88
| ~ spl221_117
| spl221_123 ),
inference(sat_conversion,[],[f22825]) ).
cnf(s185,plain,
( ~ spl221_44
| ~ spl221_48
| spl221_131 ),
inference(sat_conversion,[],[f22890]) ).
cnf(s202,plain,
( ~ spl221_44
| ~ spl221_51
| ~ spl221_64
| spl221_144 ),
inference(sat_conversion,[],[f23027]) ).
cnf(s225,plain,
( spl221_27
| ~ spl221_28
| ~ spl221_160 ),
inference(sat_conversion,[],[f23225]) ).
cnf(s316,plain,
( ~ spl221_144
| spl221_210 ),
inference(sat_conversion,[],[f24242]) ).
cnf(s319,plain,
( ~ spl221_37
| spl221_213 ),
inference(sat_conversion,[],[f24262]) ).
cnf(s329,plain,
( ~ spl221_210
| ~ spl221_213
| spl221_217 ),
inference(sat_conversion,[],[f24294]) ).
cnf(s356,plain,
( ~ spl221_108
| ~ spl221_217
| spl221_233 ),
inference(sat_conversion,[],[f24635]) ).
cnf(s370,plain,
( ~ spl221_33
| ~ spl221_123
| ~ spl221_131
| spl221_237 ),
inference(sat_conversion,[],[f24727]) ).
cnf(s463,plain,
( ~ spl221_100
| ~ spl221_108
| spl221_160
| ~ spl221_233 ),
inference(sat_conversion,[],[f25658]) ).
cnf(s497,plain,
( ~ spl221_27
| spl221_300 ),
inference(sat_conversion,[],[f25843]) ).
cnf(s1329,plain,
( spl221_28
| ~ spl221_44
| ~ spl221_62
| ~ spl221_100
| ~ spl221_115
| ~ spl221_131
| ~ spl221_237
| ~ spl221_300 ),
inference(sat_conversion,[],[f36060]) ).
cnf(s1337,plain,
spl221_47,
inference(rat,[],[s51,s29]) ).
cnf(s1338,plain,
spl221_39,
inference(rat,[],[s43,s29]) ).
cnf(s1339,plain,
spl221_38,
inference(rat,[],[s41,s33,s29]) ).
cnf(s1342,plain,
spl221_48,
inference(rat,[],[s53,s33,s1337]) ).
cnf(s1343,plain,
spl221_51,
inference(rat,[],[s63,s29,s36,s1337]) ).
cnf(s1344,plain,
spl221_36,
inference(rat,[],[s57,s33,s1337]) ).
cnf(s1348,plain,
spl221_44,
inference(rat,[],[s48,s1338]) ).
cnf(s1353,plain,
spl221_62,
inference(rat,[],[s77,s1338,s34,s1344]) ).
cnf(s1354,plain,
spl221_61,
inference(rat,[],[s76,s1338,s34,s1344]) ).
cnf(s1355,plain,
spl221_54,
inference(rat,[],[s69,s1344]) ).
cnf(s1356,plain,
spl221_53,
inference(rat,[],[s66,s1344]) ).
cnf(s1357,plain,
spl221_52,
inference(rat,[],[s65,s1344]) ).
cnf(s1360,plain,
spl221_37,
inference(rat,[],[s40,s29,s34,s36,s1344]) ).
cnf(s1364,plain,
spl221_131,
inference(rat,[],[s185,s1342,s1348]) ).
cnf(s1365,plain,
spl221_45,
inference(rat,[],[s49,s1348]) ).
cnf(s1369,plain,
spl221_76,
inference(rat,[],[s101,s1354]) ).
cnf(s1380,plain,
spl221_65,
inference(rat,[],[s84,s1354]) ).
cnf(s1388,plain,
spl221_115,
inference(rat,[],[s163,s1355]) ).
cnf(s1390,plain,
spl221_86,
inference(rat,[],[s111,s1357]) ).
cnf(s1391,plain,
spl221_85,
inference(rat,[],[s110,s1357]) ).
cnf(s1394,plain,
spl221_213,
inference(rat,[],[s319,s1360]) ).
cnf(s1406,plain,
spl221_50,
inference(rat,[],[s59,s1344,s1339,s1365]) ).
cnf(s1412,plain,
spl221_108,
inference(rat,[],[s150,s1369]) ).
cnf(s1418,plain,
spl221_100,
inference(rat,[],[s135,s35,s1380]) ).
cnf(s1445,plain,
spl221_117,
inference(rat,[],[s169,s1388]) ).
cnf(s1447,plain,
spl221_88,
inference(rat,[],[s116,s1390,s1391]) ).
cnf(s1467,plain,
spl221_64,
inference(rat,[],[s81,s1344,s1337,s29,s34,s1406]) ).
cnf(s1517,plain,
spl221_123,
inference(rat,[],[s175,s1391,s1445,s1356,s1447]) ).
cnf(s1534,plain,
spl221_144,
inference(rat,[],[s202,s1348,s1343,s1467]) ).
cnf(s1578,plain,
spl221_237,
inference(rat,[],[s370,s1364,s36,s1517]) ).
cnf(s1579,plain,
spl221_210,
inference(rat,[],[s316,s1534]) ).
cnf(s1608,plain,
spl221_217,
inference(rat,[],[s329,s1394,s1579]) ).
cnf(s1621,plain,
spl221_233,
inference(rat,[],[s356,s1412,s1608]) ).
cnf(s1644,plain,
spl221_160,
inference(rat,[],[s463,s1418,s1412,s1621]) ).
cnf(s1709,plain,
spl221_27,
inference(rat,[],[s30,s225,s1644]) ).
cnf(s1715,plain,
spl221_300,
inference(rat,[],[s497,s1709]) ).
cnf(s1725,plain,
~ spl221_28,
inference(rat,[],[s31,s1709]) ).
cnf(s1744,plain,
$false,
inference(rat,[],[s1329,s1578,s1418,s1364,s1388,s1348,s1353,s1715,s1725]) ).
fof(f36063,plain,
$false,
inference(avatar_sat_refutation,[],[s1744]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU443+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.10/0.38 % Computer : n002.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 28 05:34:40 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 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
% 16.98/4.14 % (42760)Detected formulas, will run a generic FOF schedule.
% 16.98/4.14 % (42765)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=3229774091:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 16.98/4.14 % (42767)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=2903459343:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 16.98/4.14 % (42766)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=3072155719:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 16.98/4.14 % (42768)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3300621475:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 16.98/4.14 % (42770)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1603446137:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 16.98/4.14 % (42769)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2300373967:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 16.98/4.14 % (42771)dis-21_1_sil=8000:lcm=predicate:random_seed=4284809001:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2988 on theBenchmark for (2988ds/129Mi)
% 16.98/4.14 % (42770)Instruction limit reached!
% 16.98/4.14 % (42770)------------------------------
% 16.98/4.14 % (42770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.98/4.14 % (42770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.98/4.14 % (42770)CaDiCaL version: 2.1.3
% 16.98/4.14 % (42770)Termination reason: Instruction limit
% 16.98/4.14 % (42770)Termination phase: Property scanning
% 16.98/4.14 % (42770)Time elapsed: 0.060 s
% 16.98/4.14 % (42770)Peak memory usage: 112 MB
% 16.98/4.14 % (42770)Instructions burned: 141 (million)
% 16.98/4.14 % (42768)Instruction limit reached!
% 16.98/4.14 % (42768)------------------------------
% 16.98/4.14 % (42768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.98/4.14 % (42768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.98/4.14 % (42768)CaDiCaL version: 2.1.3
% 16.98/4.14 % (42768)Termination reason: Instruction limit
% 16.98/4.14 % (42768)Termination phase: SInE selection
% 16.98/4.14 % (42768)Time elapsed: 0.081 s
% 16.98/4.14 % (42768)Peak memory usage: 112 MB
% 16.98/4.14 % (42768)Instructions burned: 110 (million)
% 16.98/4.14 % (42769)Instruction limit reached!
% 16.98/4.14 % (42769)------------------------------
% 16.98/4.14 % (42769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.98/4.14 % (42769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.98/4.14 % (42769)CaDiCaL version: 2.1.3
% 16.98/4.14 % (42769)Termination reason: Instruction limit
% 16.98/4.14 % (42769)Termination phase: SInE selection
% 16.98/4.14 % (42769)Time elapsed: 0.089 s
% 16.98/4.14 % (42769)Peak memory usage: 112 MB
% 16.98/4.14 % (42769)Instructions burned: 119 (million)
% 16.98/4.14 % (42771)Instruction limit reached!
% 16.98/4.14 % (42771)------------------------------
% 16.98/4.14 % (42771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.98/4.14 % (42771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.98/4.14 % (42771)CaDiCaL version: 2.1.3
% 16.98/4.14 % (42771)Termination reason: Instruction limit
% 16.98/4.14 % (42771)Termination phase: SInE selection
% 16.98/4.14 % (42771)Time elapsed: 0.092 s
% 16.98/4.14 % (42771)Peak memory usage: 113 MB
% 16.98/4.14 % (42771)Instructions burned: 130 (million)
% 16.98/4.14 % (42779)lrs+10_1_sil=8000:sp=occurrence:random_seed=942749063:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 16.98/4.14 % (42781)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2067766031:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 16.98/4.14 % (42780)lrs+10_1_sil=32000:urr=on:br=off:random_seed=425594706:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 16.98/4.14 % (42782)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=944960953:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 16.98/4.14 % (42780)Instruction limit reached!
% 16.98/4.14 % (42780)------------------------------
% 16.98/4.14 % (42780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.28/7.14 % (42780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.28/7.14 % (42780)CaDiCaL version: 2.1.3
% 38.28/7.14 % (42780)Termination reason: Instruction limit
% 38.28/7.14 % (42780)Termination phase: Property scanning
% 38.28/7.14 % (42780)Time elapsed: 0.069 s
% 38.28/7.14 % (42780)Peak memory usage: 112 MB
% 38.28/7.14 % (42780)Instructions burned: 158 (million)
% 38.28/7.14 % (42782)Instruction limit reached!
% 38.28/7.14 % (42782)------------------------------
% 38.28/7.14 % (42782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.28/7.14 % (42782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.28/7.14 % (42782)CaDiCaL version: 2.1.3
% 38.28/7.14 % (42782)Termination reason: Instruction limit
% 38.28/7.14 % (42782)Termination phase: Property scanning
% 38.28/7.14 % (42782)Time elapsed: 0.110 s
% 38.28/7.14 % (42782)Peak memory usage: 112 MB
% 38.28/7.14 % (42782)Instructions burned: 250 (million)
% 38.28/7.14 % (42779)Instruction limit reached!
% 38.28/7.14 % (42779)------------------------------
% 38.28/7.14 % (42779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.28/7.14 % (42779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.28/7.14 % (42779)CaDiCaL version: 2.1.3
% 38.28/7.14 % (42779)Termination reason: Instruction limit
% 38.28/7.14 % (42779)Termination phase: Saturation
% 38.28/7.14 % (42779)Time elapsed: 0.210 s
% 38.28/7.14 % (42779)Peak memory usage: 120 MB
% 38.28/7.14 % (42779)Instructions burned: 287 (million)
% 38.28/7.14 % (42787)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3584851228:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 38.28/7.14 % (42781)Instruction limit reached!
% 38.28/7.14 % (42781)------------------------------
% 38.28/7.14 % (42781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.28/7.14 % (42781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.28/7.14 % (42781)CaDiCaL version: 2.1.3
% 38.28/7.14 % (42781)Termination reason: Instruction limit
% 38.28/7.14 % (42781)Termination phase: Saturation
% 38.28/7.14 % (42781)Time elapsed: 0.249 s
% 38.28/7.14 % (42781)Peak memory usage: 119 MB
% 38.28/7.14 % (42781)Instructions burned: 326 (million)
% 38.28/7.14 % (42788)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=286431903:i=2350_2983 on theBenchmark for (2983ds/2350Mi)
% 38.28/7.14 % (42789)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=80406230:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 38.28/7.14 % (42791)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=338160842:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 38.28/7.14 % (42789)Instruction limit reached!
% 38.28/7.14 % (42789)------------------------------
% 38.28/7.14 % (42789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.28/7.14 % (42789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.28/7.14 % (42789)CaDiCaL version: 2.1.3
% 38.28/7.14 % (42789)Termination reason: Instruction limit
% 38.28/7.14 % (42789)Termination phase: SInE selection
% 38.28/7.14 % (42789)Time elapsed: 0.089 s
% 38.28/7.14 % (42789)Peak memory usage: 112 MB
% 38.28/7.14 % (42789)Instructions burned: 113 (million)
% 38.28/7.14 % (42787)Instruction limit reached!
% 38.28/7.14 % (42787)------------------------------
% 38.28/7.14 % (42787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.28/7.14 % (42787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.28/7.14 % (42787)CaDiCaL version: 2.1.3
% 38.28/7.14 % (42787)Termination reason: Instruction limit
% 38.28/7.14 % (42787)Termination phase: Property scanning
% 38.28/7.14 % (42787)Time elapsed: 0.212 s
% 38.28/7.14 % (42787)Peak memory usage: 118 MB
% 38.28/7.14 % (42787)Instructions burned: 297 (million)
% 38.28/7.14 % (42791)Instruction limit reached!
% 38.28/7.14 % (42791)------------------------------
% 38.28/7.14 % (42791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.28/7.14 % (42791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.28/7.14 % (42791)CaDiCaL version: 2.1.3
% 38.28/7.14 % (42791)Termination reason: Instruction limit
% 38.28/7.14 % (42791)Termination phase: Preprocessing 1
% 38.28/7.14 % (42791)Time elapsed: 0.091 s
% 38.28/7.14 % (42791)Peak memory usage: 113 MB
% 38.28/7.14 % (42791)Instructions burned: 127 (million)
% 38.28/7.14 % (42795)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=170076816:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2980 on theBenchmark for (2980ds/114Mi)
% 26.19/11.80 % (42796)lrs+10_1_sil=8000:sp=occurrence:random_seed=4181832119:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 26.19/11.80 % (42795)Instruction limit reached!
% 26.19/11.80 % (42795)------------------------------
% 26.19/11.80 % (42795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42795)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42795)Termination reason: Instruction limit
% 26.19/11.80 % (42795)Termination phase: Property scanning
% 26.19/11.80 % (42795)Time elapsed: 0.050 s
% 26.19/11.80 % (42795)Peak memory usage: 112 MB
% 26.19/11.80 % (42795)Instructions burned: 116 (million)
% 26.19/11.80 % (42797)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=575344126:i=437:sd=1:aac=none:ss=included_2979 on theBenchmark for (2979ds/437Mi)
% 26.19/11.80 % (42800)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2308269269:i=5202:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/5202Mi)
% 26.19/11.80 % (42797)Instruction limit reached!
% 26.19/11.80 % (42797)------------------------------
% 26.19/11.80 % (42797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42797)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42797)Termination reason: Instruction limit
% 26.19/11.80 % (42797)Termination phase: Saturation
% 26.19/11.80 % (42797)Time elapsed: 0.308 s
% 26.19/11.80 % (42797)Peak memory usage: 121 MB
% 26.19/11.80 % (42797)Instructions burned: 439 (million)
% 26.19/11.80 % (42803)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2205379681:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2975 on theBenchmark for (2975ds/134Mi)
% 26.19/11.80 % (42796)Instruction limit reached!
% 26.19/11.80 % (42796)------------------------------
% 26.19/11.80 % (42796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42796)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42796)Termination reason: Instruction limit
% 26.19/11.80 % (42796)Termination phase: Property scanning
% 26.19/11.80 % (42796)Time elapsed: 0.565 s
% 26.19/11.80 % (42796)Peak memory usage: 136 MB
% 26.19/11.80 % (42796)Instructions burned: 909 (million)
% 26.19/11.80 % (42803)Instruction limit reached!
% 26.19/11.80 % (42803)------------------------------
% 26.19/11.80 % (42803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42803)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42803)Termination reason: Instruction limit
% 26.19/11.80 % (42803)Termination phase: NewCNF
% 26.19/11.80 % (42803)Time elapsed: 0.120 s
% 26.19/11.80 % (42803)Peak memory usage: 115 MB
% 26.19/11.80 % (42803)Instructions burned: 134 (million)
% 26.19/11.80 % (42805)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3972394712:st=8:i=592:sd=3:ep=RST:ss=axioms_2973 on theBenchmark for (2973ds/592Mi)
% 26.19/11.80 % (42806)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2541529163:st=3:i=13193:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/13193Mi)
% 26.19/11.80 % (42788)Instruction limit reached!
% 26.19/11.80 % (42788)------------------------------
% 26.19/11.80 % (42788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42788)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42788)Termination reason: Instruction limit
% 26.19/11.80 % (42788)Termination phase: Property scanning
% 26.19/11.80 % (42788)Time elapsed: 1.288 s
% 26.19/11.80 % (42788)Peak memory usage: 171 MB
% 26.19/11.80 % (42788)Instructions burned: 2351 (million)
% 26.19/11.80 % (42809)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=3570954814:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/125Mi)
% 26.19/11.80 % (42805)Instruction limit reached!
% 26.19/11.80 % (42805)------------------------------
% 26.19/11.80 % (42805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42805)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42805)Termination reason: Instruction limit
% 26.19/11.80 % (42805)Termination phase: Preprocessing 3
% 26.19/11.80 % (42805)Time elapsed: 0.440 s
% 26.19/11.80 % (42805)Peak memory usage: 134 MB
% 26.19/11.80 % (42805)Instructions burned: 593 (million)
% 26.19/11.80 % (42809)Instruction limit reached!
% 26.19/11.80 % (42809)------------------------------
% 26.19/11.80 % (42809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42809)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42809)Termination reason: Instruction limit
% 26.19/11.80 % (42809)Termination phase: Property scanning
% 26.19/11.80 % (42809)Time elapsed: 0.055 s
% 26.19/11.80 % (42809)Peak memory usage: 112 MB
% 26.19/11.80 % (42809)Instructions burned: 126 (million)
% 26.19/11.80 % (42811)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1683124188:i=134:gtgl=5:slsql=off:gtg=exists_sym_2967 on theBenchmark for (2967ds/134Mi)
% 26.19/11.80 % (42812)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3822934914:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/141Mi)
% 26.19/11.80 % (42811)Instruction limit reached!
% 26.19/11.80 % (42811)------------------------------
% 26.19/11.80 % (42811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42811)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42811)Termination reason: Instruction limit
% 26.19/11.80 % (42811)Termination phase: Property scanning
% 26.19/11.80 % (42811)Time elapsed: 0.058 s
% 26.19/11.80 % (42811)Peak memory usage: 112 MB
% 26.19/11.80 % (42811)Instructions burned: 135 (million)
% 26.19/11.80 % (42812)Instruction limit reached!
% 26.19/11.80 % (42812)------------------------------
% 26.19/11.80 % (42812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42812)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42812)Termination reason: Instruction limit
% 26.19/11.80 % (42812)Termination phase: Saturation
% 26.19/11.80 % (42812)Time elapsed: 0.119 s
% 26.19/11.80 % (42812)Peak memory usage: 117 MB
% 26.19/11.80 % (42812)Instructions burned: 142 (million)
% 26.19/11.80 % (42815)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2482311477:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2964 on theBenchmark for (2964ds/431Mi)
% 26.19/11.80 % (42816)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=3285909753:i=6060:aac=none:ins=25_2963 on theBenchmark for (2963ds/6060Mi)
% 26.19/11.80 % (42815)Instruction limit reached!
% 26.19/11.80 % (42815)------------------------------
% 26.19/11.80 % (42815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42815)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42815)Termination reason: Instruction limit
% 26.19/11.80 % (42815)Termination phase: Saturation
% 26.19/11.80 % (42815)Time elapsed: 0.295 s
% 26.19/11.80 % (42815)Peak memory usage: 119 MB
% 26.19/11.80 % (42815)Instructions burned: 433 (million)
% 26.19/11.80 % (42819)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=394819133:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2960 on theBenchmark for (2960ds/150Mi)
% 26.19/11.80 % (42819)Instruction limit reached!
% 26.19/11.80 % (42819)------------------------------
% 26.19/11.80 % (42819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42819)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42819)Termination reason: Instruction limit
% 26.19/11.80 % (42819)Termination phase: Preprocessing 1
% 26.19/11.80 % (42819)Time elapsed: 0.132 s
% 26.19/11.80 % (42819)Peak memory usage: 113 MB
% 26.19/11.80 % (42819)Instructions burned: 150 (million)
% 26.19/11.80 % (42821)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2433325757:i=14155:bd=all_2957 on theBenchmark for (2957ds/14155Mi)
% 26.19/11.80 % (42800)Instruction limit reached!
% 26.19/11.80 % (42800)------------------------------
% 26.19/11.80 % (42800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42800)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42800)Termination reason: Instruction limit
% 26.19/11.80 % (42800)Termination phase: Saturation
% 26.19/11.80 % (42800)Time elapsed: 3.960 s
% 26.19/11.80 % (42800)Peak memory usage: 607 MB
% 26.19/11.80 % (42800)Instructions burned: 5204 (million)
% 26.19/11.80 % (42823)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=205711648:i=667:av=off:fsr=off_2936 on theBenchmark for (2936ds/667Mi)
% 26.19/11.80 % (42823)Instruction limit reached!
% 26.19/11.80 % (42823)------------------------------
% 26.19/11.80 % (42823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42823)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42823)Termination reason: Instruction limit
% 26.19/11.80 % (42823)Termination phase: NewCNF
% 26.19/11.80 % (42823)Time elapsed: 0.515 s
% 26.19/11.80 % (42823)Peak memory usage: 149 MB
% 26.19/11.80 % (42823)Instructions burned: 667 (million)
% 26.19/11.80 % (42825)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=4021644809:s2a=on:i=185:s2at=1.8:fdi=4_2929 on theBenchmark for (2929ds/185Mi)
% 26.19/11.80 % (42825)Instruction limit reached!
% 26.19/11.80 % (42825)------------------------------
% 26.19/11.80 % (42825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42825)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42825)Termination reason: Instruction limit
% 26.19/11.80 % (42825)Termination phase: SInE selection
% 26.19/11.80 % (42825)Time elapsed: 0.150 s
% 26.19/11.80 % (42825)Peak memory usage: 113 MB
% 26.19/11.80 % (42825)Instructions burned: 185 (million)
% 26.19/11.80 % (42827)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=445526317:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2926 on theBenchmark for (2926ds/193Mi)
% 26.19/11.80 % (42827)Instruction limit reached!
% 26.19/11.80 % (42827)------------------------------
% 26.19/11.80 % (42827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42827)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42827)Termination reason: Instruction limit
% 26.19/11.80 % (42827)Termination phase: SInE selection
% 26.19/11.80 % (42827)Time elapsed: 0.158 s
% 26.19/11.80 % (42827)Peak memory usage: 112 MB
% 26.19/11.80 % (42827)Instructions burned: 193 (million)
% 26.19/11.80 % (42829)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=847112120:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2923 on theBenchmark for (2923ds/4850Mi)
% 26.19/11.80 % (42816)Instruction limit reached!
% 26.19/11.80 % (42816)------------------------------
% 26.19/11.80 % (42816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42816)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42816)Termination reason: Instruction limit
% 26.19/11.80 % (42816)Termination phase: Saturation
% 26.19/11.80 % (42816)Time elapsed: 4.591 s
% 26.19/11.80 % (42816)Peak memory usage: 587 MB
% 26.19/11.80 % (42816)Instructions burned: 6063 (million)
% 26.19/11.80 % (42831)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3166327079:i=12111:sd=1:ss=included_2915 on theBenchmark for (2915ds/12111Mi)
% 26.19/11.80 % (42831)First to succeed.
% 26.19/11.80 % (42831)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-42760"
% 26.19/11.80 % (42829)Instruction limit reached!
% 26.19/11.80 % (42829)------------------------------
% 26.19/11.80 % (42829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.19/11.80 % (42829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.19/11.80 % (42829)CaDiCaL version: 2.1.3
% 26.19/11.80 % (42829)Termination reason: Instruction limit
% 26.19/11.80 % (42829)Termination phase: Saturation
% 26.19/11.80 % (42829)Time elapsed: 2.791 s
% 26.19/11.80 % (42829)Peak memory usage: 224 MB
% 26.19/11.80 % (42829)Instructions burned: 4850 (million)
% 26.19/11.80 % (42833)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3496392303:i=319:kws=precedence:fsr=off_2893 on theBenchmark for (2893ds/319Mi)
% 26.19/11.80 % (42831)Refutation found. Thanks to Tanya!
% 26.19/11.80 % SZS status Theorem for theBenchmark
% 26.19/11.80 % SZS output start Proof for theBenchmark
% See solution above
% 71.23/12.01 % (42831)------------------------------
% 71.23/12.01 % (42831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.23/12.01 % (42831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.23/12.01 % (42831)CaDiCaL version: 2.1.3
% 71.23/12.01 % (42831)Termination reason: Refutation
% 71.23/12.01 % (42831)Time elapsed: 2.002 s
% 71.23/12.01 % (42831)Peak memory usage: 182 MB
% 71.23/12.01 % (42831)Instructions burned: 2918 (million)
% 71.23/12.01 % (42831)------------------------------
% 71.23/12.01 % (42831)------------------------------
% 71.23/12.01 % (42760)Success in time 10.948 s
% 71.23/12.01 % Vampire exiting
%------------------------------------------------------------------------------