%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU442+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 : n007.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:06 PM UTC 2026
% Result : Theorem 42.81s 11.43s
% Output : Refutation 66.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 71
% Syntax : Number of formulae : 372 ( 64 unt; 46 def)
% Number of atoms : 930 ( 156 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1015 ( 457 ~; 458 |; 28 &)
% ( 46 <=>; 25 =>; 0 <=; 1 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 50 ( 48 usr; 44 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 8 con; 0-5 aty)
% Number of variables : 255 ( 0 sgn 243 !; 12 ?)
% 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(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(f855,axiom,
! [X0] :
( v1_relat_1(X0)
=> k9_relat_1(X0,k1_relat_1(X0)) = k2_relat_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t146_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(f19123,axiom,
! [X0,X1,X2,X3] :
( m2_relset_1(X3,X0,X1)
=> ! [X4] :
( m2_relset_1(X4,X1,X2)
=> ( k1_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X0,k6_relset_1(X0,X1,X3),k1_funct_5(X4))
& r1_tarski(k1_funct_5(k9_relset_2(X0,X1,X2,X3,X4)),k1_funct_5(X3)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t52_relset_2) ).
fof(f19124,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(f19125,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m2_relset_1(X3,X0,X1)
=> ( r1_tarski(X2,k1_funct_5(X3))
<=> r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_relset_2) ).
fof(f19126,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m2_relset_1(X3,X0,X1)
=> ( r1_tarski(X2,k1_funct_5(X3))
<=> r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2)) ) ) ),
inference(negated_conjecture,[status(cth)],[f19125]) ).
fof(f19215,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(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(flattening,[],[f19215]) ).
fof(f19217,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(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(flattening,[],[f19217]) ).
fof(f19279,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(f19280,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ( k1_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X0,k6_relset_1(X0,X1,X3),k1_funct_5(X4))
& r1_tarski(k1_funct_5(k9_relset_2(X0,X1,X2,X3,X4)),k1_funct_5(X3)) )
| ~ m2_relset_1(X4,X1,X2) )
| ~ m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f19123]) ).
fof(f19281,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(f19282,plain,
? [X0,X1,X2] :
( ? [X3] :
( ( r1_tarski(X2,k1_funct_5(X3))
<~> r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2)) )
& m2_relset_1(X3,X0,X1) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19126]) ).
fof(f19302,plain,
! [X0,X1] :
( k3_xboole_0(X0,X1) = X0
| ~ r1_tarski(X0,X1) ),
inference(ennf_transformation,[],[f97]) ).
fof(f19313,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(f19314,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(f19375,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(f19391,plain,
! [X0] :
( k9_relat_1(X0,k1_relat_1(X0)) = k2_relat_1(X0)
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f855]) ).
fof(f19393,plain,
! [X0,X1] :
( r1_tarski(k9_relat_1(X1,X0),k2_relat_1(X1))
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f853]) ).
fof(f19592,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f19593,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(flattening,[],[f19592]) ).
fof(f19636,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(f19945,plain,
! [X0] :
( k4_relat_1(k4_relat_1(X0)) = X0
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f907]) ).
fof(f19948,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(f19969,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(f19978,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(f19980,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(f20017,plain,
? [X0,X1,X2] :
( ? [X3] :
( ( ~ r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2))
| ~ r1_tarski(X2,k1_funct_5(X3)) )
& ( r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2))
| r1_tarski(X2,k1_funct_5(X3)) )
& m2_relset_1(X3,X0,X1) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f19282]) ).
fof(f20018,plain,
? [X0,X1,X2] :
( ? [X3] :
( ( ~ r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2))
| ~ r1_tarski(X2,k1_funct_5(X3)) )
& ( r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2))
| r1_tarski(X2,k1_funct_5(X3)) )
& m2_relset_1(X3,X0,X1) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f20017]) ).
fof(f20019,plain,
( ( ~ r1_tarski(sK18,k10_relset_1(sK16,sK16,k9_relset_2(sK16,sK17,sK16,sK19,k6_relset_1(sK16,sK17,sK19)),sK18))
| ~ r1_tarski(sK18,k1_funct_5(sK19)) )
& ( r1_tarski(sK18,k10_relset_1(sK16,sK16,k9_relset_2(sK16,sK17,sK16,sK19,k6_relset_1(sK16,sK17,sK19)),sK18))
| r1_tarski(sK18,k1_funct_5(sK19)) )
& m2_relset_1(sK19,sK16,sK17)
& m1_subset_1(sK18,k1_zfmisc_1(sK16)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18,sK19]),skolemize(X0,sK16),skolemize(X1,sK17),skolemize(X2,sK18),skolemize(X3,sK19)],[f20018]) ).
fof(f20030,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(f20117,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(f20118,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,[],[f20117]) ).
fof(f20309,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,[],[f19216]) ).
fof(f20310,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,[],[f19218]) ).
fof(f20390,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X1,X0)
| k10_relset_1(X1,X0,X2,X1) = k2_funct_5(X2) ),
inference(cnf_transformation,[],[f19279]) ).
fof(f20391,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,[],[f19279]) ).
fof(f20393,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X4,X1,X2)
| k1_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X0,k6_relset_1(X0,X1,X3),k1_funct_5(X4))
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f19280]) ).
fof(f20394,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,[],[f19281]) ).
fof(f20395,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,[],[f19281]) ).
fof(f20397,plain,
m2_relset_1(sK19,sK16,sK17),
inference(cnf_transformation,[],[f20019]) ).
fof(f20398,plain,
( r1_tarski(sK18,k10_relset_1(sK16,sK16,k9_relset_2(sK16,sK17,sK16,sK19,k6_relset_1(sK16,sK17,sK19)),sK18))
| r1_tarski(sK18,k1_funct_5(sK19)) ),
inference(cnf_transformation,[],[f20019]) ).
fof(f20399,plain,
( ~ r1_tarski(sK18,k10_relset_1(sK16,sK16,k9_relset_2(sK16,sK17,sK16,sK19,k6_relset_1(sK16,sK17,sK19)),sK18))
| ~ r1_tarski(sK18,k1_funct_5(sK19)) ),
inference(cnf_transformation,[],[f20019]) ).
fof(f20424,plain,
! [X0,X1] :
( k3_xboole_0(X0,X1) = X0
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f19302]) ).
fof(f20436,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f57]) ).
fof(f20454,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20030]) ).
fof(f20460,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,[],[f19313]) ).
fof(f20461,plain,
! [X2,X0,X1] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f19314]) ).
fof(f20515,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,[],[f19375]) ).
fof(f20529,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k2_relat_1(X0) = k9_relat_1(X0,k1_relat_1(X0)) ),
inference(cnf_transformation,[],[f19391]) ).
fof(f20531,plain,
! [X0,X1] :
( ~ v1_relat_1(X1)
| r1_tarski(k9_relat_1(X1,X0),k2_relat_1(X1)) ),
inference(cnf_transformation,[],[f19393]) ).
fof(f20821,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f20873,plain,
! [X2,X0,X1] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(cnf_transformation,[],[f19593]) ).
fof(f20876,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| X0 = X1
| ~ r1_tarski(X1,X0) ),
inference(cnf_transformation,[],[f20118]) ).
fof(f20921,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,[],[f19636]) ).
fof(f21403,plain,
! [X0] :
( k4_relat_1(k4_relat_1(X0)) = X0
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f19945]) ).
fof(f21406,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,[],[f19948]) ).
fof(f21454,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k2_relat_1(X0) = k2_funct_5(X0) ),
inference(cnf_transformation,[],[f19969]) ).
fof(f21455,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k1_relat_1(X0) = k1_funct_5(X0) ),
inference(cnf_transformation,[],[f19969]) ).
fof(f21496,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
inference(cnf_transformation,[],[f19978]) ).
fof(f21498,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
inference(cnf_transformation,[],[f19980]) ).
fof(f21544,plain,
! [X0,X1] :
( k4_xboole_0(X0,k4_xboole_0(X0,X1)) = X0
| ~ r1_tarski(X0,X1) ),
inference(definition_unfolding,[],[f20424,f20821]) ).
fof(f21556,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k4_xboole_0(X1,k4_xboole_0(X1,X0)),
inference(definition_unfolding,[],[f20436,f20821,f20821]) ).
fof(f21621,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,[],[f21406,f20821]) ).
fof(f21754,definition,
sF216 = k6_relset_1(sK16,sK17,sK19),
introduced(definition,[new_symbols(definition,[sF216])],[function_definition]) ).
fof(f21755,plain,
k6_relset_1(sK16,sK17,sK19) = sF216,
inference(reorient_equations,[],[f21754]) ).
fof(f21756,definition,
sF217 = k9_relset_2(sK16,sK17,sK16,sK19,sF216),
introduced(definition,[new_symbols(definition,[sF217])],[function_definition]) ).
fof(f21757,plain,
k9_relset_2(sK16,sK17,sK16,sK19,sF216) = sF217,
inference(reorient_equations,[],[f21756]) ).
fof(f21758,definition,
sF218 = k10_relset_1(sK16,sK16,sF217,sK18),
introduced(definition,[new_symbols(definition,[sF218])],[function_definition]) ).
fof(f21759,plain,
k10_relset_1(sK16,sK16,sF217,sK18) = sF218,
inference(reorient_equations,[],[f21758]) ).
fof(f21760,definition,
sF219 = k1_funct_5(sK19),
introduced(definition,[new_symbols(definition,[sF219])],[function_definition]) ).
fof(f21761,plain,
k1_funct_5(sK19) = sF219,
inference(reorient_equations,[],[f21760]) ).
fof(f21762,plain,
( ~ r1_tarski(sK18,sF218)
| ~ r1_tarski(sK18,sF219) ),
inference(definition_folding,[],[f20399,f21761,f21759,f21757,f21755]) ).
fof(f21763,plain,
( r1_tarski(sK18,sF218)
| r1_tarski(sK18,sF219) ),
inference(definition_folding,[],[f20398,f21761,f21759,f21757,f21755]) ).
fof(f21933,definition,
( spl221_26
<=> m2_relset_1(sK19,sK16,sK17) ),
introduced(definition,[new_symbols(definition,[spl221_26])],[avatar_definition]) ).
fof(f21935,plain,
( m2_relset_1(sK19,sK16,sK17)
| ~ spl221_26 ),
inference(avatar_component_clause,[],[f21933]) ).
fof(f21936,plain,
spl221_26,
inference(avatar_split_clause,[],[f20397,f21933]) ).
fof(f21938,definition,
( spl221_27
<=> r1_tarski(sK18,sF219) ),
introduced(definition,[new_symbols(definition,[spl221_27])],[avatar_definition]) ).
fof(f21939,plain,
( ~ r1_tarski(sK18,sF219)
| spl221_27 ),
inference(avatar_component_clause,[],[f21938]) ).
fof(f21940,plain,
( r1_tarski(sK18,sF219)
| ~ spl221_27 ),
inference(avatar_component_clause,[],[f21938]) ).
fof(f21942,definition,
( spl221_28
<=> r1_tarski(sK18,sF218) ),
introduced(definition,[new_symbols(definition,[spl221_28])],[avatar_definition]) ).
fof(f21943,plain,
( ~ r1_tarski(sK18,sF218)
| spl221_28 ),
inference(avatar_component_clause,[],[f21942]) ).
fof(f21944,plain,
( r1_tarski(sK18,sF218)
| ~ spl221_28 ),
inference(avatar_component_clause,[],[f21942]) ).
fof(f21945,plain,
( spl221_27
| spl221_28 ),
inference(avatar_split_clause,[],[f21763,f21942,f21938]) ).
fof(f21946,plain,
( ~ spl221_27
| ~ spl221_28 ),
inference(avatar_split_clause,[],[f21762,f21942,f21938]) ).
fof(f21957,definition,
( spl221_30
<=> k6_relset_1(sK16,sK17,sK19) = sF216 ),
introduced(definition,[new_symbols(definition,[spl221_30])],[avatar_definition]) ).
fof(f21959,plain,
( k6_relset_1(sK16,sK17,sK19) = sF216
| ~ spl221_30 ),
inference(avatar_component_clause,[],[f21957]) ).
fof(f21960,plain,
spl221_30,
inference(avatar_split_clause,[],[f21755,f21957]) ).
fof(f21962,definition,
( spl221_31
<=> k9_relset_2(sK16,sK17,sK16,sK19,sF216) = sF217 ),
introduced(definition,[new_symbols(definition,[spl221_31])],[avatar_definition]) ).
fof(f21964,plain,
( k9_relset_2(sK16,sK17,sK16,sK19,sF216) = sF217
| ~ spl221_31 ),
inference(avatar_component_clause,[],[f21962]) ).
fof(f21965,plain,
spl221_31,
inference(avatar_split_clause,[],[f21757,f21962]) ).
fof(f21967,definition,
( spl221_32
<=> k10_relset_1(sK16,sK16,sF217,sK18) = sF218 ),
introduced(definition,[new_symbols(definition,[spl221_32])],[avatar_definition]) ).
fof(f21969,plain,
( k10_relset_1(sK16,sK16,sF217,sK18) = sF218
| ~ spl221_32 ),
inference(avatar_component_clause,[],[f21967]) ).
fof(f21970,plain,
spl221_32,
inference(avatar_split_clause,[],[f21759,f21967]) ).
fof(f21972,definition,
( spl221_33
<=> k1_funct_5(sK19) = sF219 ),
introduced(definition,[new_symbols(definition,[spl221_33])],[avatar_definition]) ).
fof(f21974,plain,
( k1_funct_5(sK19) = sF219
| ~ spl221_33 ),
inference(avatar_component_clause,[],[f21972]) ).
fof(f21975,plain,
spl221_33,
inference(avatar_split_clause,[],[f21761,f21972]) ).
fof(f22006,definition,
( spl221_35
<=> m2_relset_1(sF216,sK17,sK16) ),
introduced(definition,[new_symbols(definition,[spl221_35])],[avatar_definition]) ).
fof(f22007,plain,
( m2_relset_1(sF216,sK17,sK16)
| ~ spl221_35 ),
inference(avatar_component_clause,[],[f22006]) ).
fof(f22008,plain,
( ~ m2_relset_1(sF216,sK17,sK16)
| spl221_35 ),
inference(avatar_component_clause,[],[f22006]) ).
fof(f22015,plain,
( k1_funct_5(sK19) = k10_relset_1(sK17,sK16,k6_relset_1(sK16,sK17,sK19),sK17)
| ~ spl221_26 ),
inference(resolution,[],[f20391,f21935]) ).
fof(f22016,plain,
( k1_funct_5(sK19) = k10_relset_1(sK17,sK16,sF216,sK17)
| ~ spl221_26
| ~ spl221_30 ),
inference(forward_demodulation,[],[f22015,f21959]) ).
fof(f22018,plain,
( sF219 = k10_relset_1(sK17,sK16,sF216,sK17)
| ~ spl221_26
| ~ spl221_30
| ~ spl221_33 ),
inference(forward_demodulation,[],[f22016,f21974]) ).
fof(f22021,definition,
( spl221_37
<=> sF219 = k10_relset_1(sK17,sK16,sF216,sK17) ),
introduced(definition,[new_symbols(definition,[spl221_37])],[avatar_definition]) ).
fof(f22023,plain,
( sF219 = k10_relset_1(sK17,sK16,sF216,sK17)
| ~ spl221_37 ),
inference(avatar_component_clause,[],[f22021]) ).
fof(f22024,plain,
( spl221_37
| ~ spl221_26
| ~ spl221_30
| ~ spl221_33 ),
inference(avatar_split_clause,[],[f22018,f21972,f21957,f21933,f22021]) ).
fof(f22027,plain,
( m1_subset_1(sK19,k1_zfmisc_1(k2_zfmisc_1(sK16,sK17)))
| ~ spl221_26 ),
inference(unit_resulting_resolution,[],[f20460,f21935]) ).
fof(f22028,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,[],[f20460,f20309]) ).
fof(f22030,definition,
( spl221_38
<=> m1_subset_1(sK19,k1_zfmisc_1(k2_zfmisc_1(sK16,sK17))) ),
introduced(definition,[new_symbols(definition,[spl221_38])],[avatar_definition]) ).
fof(f22032,plain,
( m1_subset_1(sK19,k1_zfmisc_1(k2_zfmisc_1(sK16,sK17)))
| ~ spl221_38 ),
inference(avatar_component_clause,[],[f22030]) ).
fof(f22033,plain,
( spl221_38
| ~ spl221_26 ),
inference(avatar_split_clause,[],[f22027,f21933,f22030]) ).
fof(f22034,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,[],[f20310,f20460]) ).
fof(f22051,plain,
( k10_relset_1(sK16,sK17,sK19,sK16) = k2_funct_5(sK19)
| ~ spl221_26 ),
inference(resolution,[],[f20390,f21935]) ).
fof(f22053,definition,
( spl221_41
<=> k10_relset_1(sK16,sK17,sK19,sK16) = k2_funct_5(sK19) ),
introduced(definition,[new_symbols(definition,[spl221_41])],[avatar_definition]) ).
fof(f22056,plain,
( spl221_41
| ~ spl221_26 ),
inference(avatar_split_clause,[],[f22051,f21933,f22053]) ).
fof(f22059,plain,
( v1_relat_1(sK19)
| ~ spl221_38 ),
inference(unit_resulting_resolution,[],[f20461,f22032]) ).
fof(f22061,definition,
( spl221_42
<=> v1_relat_1(sK19) ),
introduced(definition,[new_symbols(definition,[spl221_42])],[avatar_definition]) ).
fof(f22063,plain,
( v1_relat_1(sK19)
| ~ spl221_42 ),
inference(avatar_component_clause,[],[f22061]) ).
fof(f22064,plain,
( spl221_42
| ~ spl221_38 ),
inference(avatar_split_clause,[],[f22059,f22030,f22061]) ).
fof(f22065,plain,
( r1_tarski(k2_funct_5(sF217),k2_funct_5(sF216))
| ~ m2_relset_1(sF216,sK17,sK16)
| ~ m2_relset_1(sK19,sK16,sK17)
| ~ spl221_31 ),
inference(superposition,[],[f20394,f21964]) ).
fof(f22082,plain,
( m1_relset_1(sK19,sK16,sK17)
| ~ spl221_26 ),
inference(resolution,[],[f20454,f21935]) ).
fof(f22084,definition,
( spl221_44
<=> m1_relset_1(sK19,sK16,sK17) ),
introduced(definition,[new_symbols(definition,[spl221_44])],[avatar_definition]) ).
fof(f22086,plain,
( m1_relset_1(sK19,sK16,sK17)
| ~ spl221_44 ),
inference(avatar_component_clause,[],[f22084]) ).
fof(f22087,plain,
( spl221_44
| ~ spl221_26 ),
inference(avatar_split_clause,[],[f22082,f21933,f22084]) ).
fof(f22090,plain,
( m2_relset_1(k6_relset_1(sK16,sK17,sK19),sK17,sK16)
| ~ spl221_44 ),
inference(unit_resulting_resolution,[],[f21498,f22086]) ).
fof(f22097,plain,
( k6_relset_1(sK16,sK17,sK19) = k4_relat_1(sK19)
| ~ spl221_44 ),
inference(resolution,[],[f22086,f21496]) ).
fof(f22098,plain,
( sF216 = k4_relat_1(sK19)
| ~ spl221_30
| ~ spl221_44 ),
inference(forward_demodulation,[],[f22097,f21959]) ).
fof(f22102,plain,
( m2_relset_1(sF216,sK17,sK16)
| ~ spl221_30
| ~ spl221_44 ),
inference(forward_demodulation,[],[f22090,f21959]) ).
fof(f22105,definition,
( spl221_45
<=> sF216 = k4_relat_1(sK19) ),
introduced(definition,[new_symbols(definition,[spl221_45])],[avatar_definition]) ).
fof(f22107,plain,
( sF216 = k4_relat_1(sK19)
| ~ spl221_45 ),
inference(avatar_component_clause,[],[f22105]) ).
fof(f22108,plain,
( spl221_45
| ~ spl221_30
| ~ spl221_44 ),
inference(avatar_split_clause,[],[f22098,f22084,f21957,f22105]) ).
fof(f22116,plain,
( $false
| ~ spl221_30
| spl221_35
| ~ spl221_44 ),
inference(forward_subsumption_resolution,[],[f22102,f22008]) ).
fof(f22117,plain,
( ~ spl221_30
| spl221_35
| ~ spl221_44 ),
inference(avatar_contradiction_clause,[],[f22116]) ).
fof(f22118,plain,
( r1_tarski(k2_funct_5(sF217),k2_funct_5(sF216))
| ~ m2_relset_1(sK19,sK16,sK17)
| ~ spl221_31
| ~ spl221_35 ),
inference(forward_subsumption_resolution,[],[f22065,f22007]) ).
fof(f22119,plain,
( r1_tarski(k2_funct_5(sF217),k2_funct_5(sF216))
| ~ spl221_26
| ~ spl221_31
| ~ spl221_35 ),
inference(forward_subsumption_resolution,[],[f22118,f21935]) ).
fof(f22121,definition,
( spl221_47
<=> r1_tarski(k2_funct_5(sF217),k2_funct_5(sF216)) ),
introduced(definition,[new_symbols(definition,[spl221_47])],[avatar_definition]) ).
fof(f22123,plain,
( r1_tarski(k2_funct_5(sF217),k2_funct_5(sF216))
| ~ spl221_47 ),
inference(avatar_component_clause,[],[f22121]) ).
fof(f22124,plain,
( spl221_47
| ~ spl221_26
| ~ spl221_31
| ~ spl221_35 ),
inference(avatar_split_clause,[],[f22119,f22006,f21962,f21933,f22121]) ).
fof(f22139,plain,
( k1_funct_5(k9_relset_2(sK16,sK17,sK16,sK19,sF216)) = k10_relset_1(sK17,sK16,k6_relset_1(sK16,sK17,sK19),k1_funct_5(sF216))
| ~ spl221_26
| ~ spl221_35 ),
inference(unit_resulting_resolution,[],[f20393,f21935,f22007]) ).
fof(f22143,plain,
( k2_funct_5(k9_relset_2(sK16,sK17,sK16,sK19,sF216)) = k10_relset_1(sK17,sK16,sF216,k2_funct_5(sK19))
| ~ spl221_26
| ~ spl221_35 ),
inference(unit_resulting_resolution,[],[f20395,f21935,f22007]) ).
fof(f22145,plain,
( m1_subset_1(sF216,k1_zfmisc_1(k2_zfmisc_1(sK17,sK16)))
| ~ spl221_35 ),
inference(unit_resulting_resolution,[],[f20460,f22007]) ).
fof(f22151,plain,
( k10_relset_1(sK17,sK16,sF216,sK17) = k2_funct_5(sF216)
| ~ spl221_35 ),
inference(resolution,[],[f22007,f20390]) ).
fof(f22152,plain,
( k1_funct_5(sF216) = k10_relset_1(sK16,sK17,k6_relset_1(sK17,sK16,sF216),sK16)
| ~ spl221_35 ),
inference(resolution,[],[f22007,f20391]) ).
fof(f22155,plain,
( m1_relset_1(sF216,sK17,sK16)
| ~ spl221_35 ),
inference(resolution,[],[f22007,f20454]) ).
fof(f22159,definition,
( spl221_49
<=> m1_relset_1(sF216,sK17,sK16) ),
introduced(definition,[new_symbols(definition,[spl221_49])],[avatar_definition]) ).
fof(f22161,plain,
( m1_relset_1(sF216,sK17,sK16)
| ~ spl221_49 ),
inference(avatar_component_clause,[],[f22159]) ).
fof(f22162,plain,
( spl221_49
| ~ spl221_35 ),
inference(avatar_split_clause,[],[f22155,f22006,f22159]) ).
fof(f22164,definition,
( spl221_50
<=> k1_funct_5(sF216) = k10_relset_1(sK16,sK17,k6_relset_1(sK17,sK16,sF216),sK16) ),
introduced(definition,[new_symbols(definition,[spl221_50])],[avatar_definition]) ).
fof(f22167,plain,
( spl221_50
| ~ spl221_35 ),
inference(avatar_split_clause,[],[f22152,f22006,f22164]) ).
fof(f22168,plain,
( sF219 = k2_funct_5(sF216)
| ~ spl221_35
| ~ spl221_37 ),
inference(forward_demodulation,[],[f22151,f22023]) ).
fof(f22184,plain,
( k1_funct_5(k9_relset_2(sK16,sK17,sK16,sK19,sF216)) = k10_relset_1(sK17,sK16,sF216,k1_funct_5(sF216))
| ~ spl221_26
| ~ spl221_30
| ~ spl221_35 ),
inference(forward_demodulation,[],[f22139,f21959]) ).
fof(f22192,plain,
( k2_funct_5(sF217) = k10_relset_1(sK17,sK16,sF216,k2_funct_5(sK19))
| ~ spl221_26
| ~ spl221_31
| ~ spl221_35 ),
inference(forward_demodulation,[],[f22143,f21964]) ).
fof(f22194,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(f22196,plain,
( m1_subset_1(sF216,k1_zfmisc_1(k2_zfmisc_1(sK17,sK16)))
| ~ spl221_54 ),
inference(avatar_component_clause,[],[f22194]) ).
fof(f22197,plain,
( spl221_54
| ~ spl221_35 ),
inference(avatar_split_clause,[],[f22145,f22006,f22194]) ).
fof(f22210,definition,
( spl221_57
<=> sF219 = k2_funct_5(sF216) ),
introduced(definition,[new_symbols(definition,[spl221_57])],[avatar_definition]) ).
fof(f22212,plain,
( sF219 = k2_funct_5(sF216)
| ~ spl221_57 ),
inference(avatar_component_clause,[],[f22210]) ).
fof(f22213,plain,
( spl221_57
| ~ spl221_35
| ~ spl221_37 ),
inference(avatar_split_clause,[],[f22168,f22021,f22006,f22210]) ).
fof(f22220,plain,
( k1_funct_5(sF217) = k10_relset_1(sK17,sK16,sF216,k1_funct_5(sF216))
| ~ spl221_26
| ~ spl221_30
| ~ spl221_31
| ~ spl221_35 ),
inference(forward_demodulation,[],[f22184,f21964]) ).
fof(f22222,definition,
( spl221_59
<=> k2_funct_5(sF217) = k10_relset_1(sK17,sK16,sF216,k2_funct_5(sK19)) ),
introduced(definition,[new_symbols(definition,[spl221_59])],[avatar_definition]) ).
fof(f22224,plain,
( k2_funct_5(sF217) = k10_relset_1(sK17,sK16,sF216,k2_funct_5(sK19))
| ~ spl221_59 ),
inference(avatar_component_clause,[],[f22222]) ).
fof(f22225,plain,
( spl221_59
| ~ spl221_26
| ~ spl221_31
| ~ spl221_35 ),
inference(avatar_split_clause,[],[f22192,f22006,f21962,f21933,f22222]) ).
fof(f22227,definition,
( spl221_60
<=> k1_funct_5(sF217) = k10_relset_1(sK17,sK16,sF216,k1_funct_5(sF216)) ),
introduced(definition,[new_symbols(definition,[spl221_60])],[avatar_definition]) ).
fof(f22229,plain,
( k1_funct_5(sF217) = k10_relset_1(sK17,sK16,sF216,k1_funct_5(sF216))
| ~ spl221_60 ),
inference(avatar_component_clause,[],[f22227]) ).
fof(f22230,plain,
( spl221_60
| ~ spl221_26
| ~ spl221_30
| ~ spl221_31
| ~ spl221_35 ),
inference(avatar_split_clause,[],[f22220,f22006,f21962,f21957,f21933,f22227]) ).
fof(f22260,plain,
( ! [X0] : k10_relset_1(sK17,sK16,sF216,X0) = k9_relat_1(sF216,X0)
| ~ spl221_49 ),
inference(resolution,[],[f22161,f20921]) ).
fof(f22263,plain,
( k6_relset_1(sK17,sK16,sF216) = k4_relat_1(sF216)
| ~ spl221_49 ),
inference(resolution,[],[f22161,f21496]) ).
fof(f22265,definition,
( spl221_63
<=> k6_relset_1(sK17,sK16,sF216) = k4_relat_1(sF216) ),
introduced(definition,[new_symbols(definition,[spl221_63])],[avatar_definition]) ).
fof(f22268,plain,
( spl221_63
| ~ spl221_49 ),
inference(avatar_split_clause,[],[f22263,f22159,f22265]) ).
fof(f22298,plain,
( k1_funct_5(sF217) = k9_relat_1(sF216,k1_funct_5(sF216))
| ~ spl221_49
| ~ spl221_60 ),
inference(superposition,[],[f22229,f22260]) ).
fof(f22300,definition,
( spl221_68
<=> k1_funct_5(sF217) = k9_relat_1(sF216,k1_funct_5(sF216)) ),
introduced(definition,[new_symbols(definition,[spl221_68])],[avatar_definition]) ).
fof(f22303,plain,
( spl221_68
| ~ spl221_49
| ~ spl221_60 ),
inference(avatar_split_clause,[],[f22298,f22227,f22159,f22300]) ).
fof(f22336,plain,
( k2_funct_5(sF217) = k9_relat_1(sF216,k2_funct_5(sK19))
| ~ spl221_49
| ~ spl221_59 ),
inference(superposition,[],[f22260,f22224]) ).
fof(f22338,definition,
( spl221_74
<=> k2_funct_5(sF217) = k9_relat_1(sF216,k2_funct_5(sK19)) ),
introduced(definition,[new_symbols(definition,[spl221_74])],[avatar_definition]) ).
fof(f22341,plain,
( spl221_74
| ~ spl221_49
| ~ spl221_59 ),
inference(avatar_split_clause,[],[f22336,f22222,f22159,f22338]) ).
fof(f22348,plain,
( v1_relat_1(sF216)
| ~ spl221_54 ),
inference(unit_resulting_resolution,[],[f20461,f22196]) ).
fof(f22349,plain,
( m2_relset_1(k9_relset_2(sK16,sK17,sK16,sK19,sF216),sK16,sK16)
| ~ spl221_26
| ~ spl221_54 ),
inference(unit_resulting_resolution,[],[f22028,f21935,f22196]) ).
fof(f22350,plain,
( k9_relset_2(sK16,sK17,sK16,sK19,sF216) = k5_relat_1(sK19,sF216)
| ~ spl221_26
| ~ spl221_54 ),
inference(unit_resulting_resolution,[],[f22034,f21935,f22196]) ).
fof(f22359,definition,
( spl221_75
<=> v1_relat_1(sF216) ),
introduced(definition,[new_symbols(definition,[spl221_75])],[avatar_definition]) ).
fof(f22361,plain,
( v1_relat_1(sF216)
| ~ spl221_75 ),
inference(avatar_component_clause,[],[f22359]) ).
fof(f22362,plain,
( spl221_75
| ~ spl221_54 ),
inference(avatar_split_clause,[],[f22348,f22194,f22359]) ).
fof(f22363,plain,
( m2_relset_1(sF217,sK16,sK16)
| ~ spl221_26
| ~ spl221_31
| ~ spl221_54 ),
inference(forward_demodulation,[],[f22349,f21964]) ).
fof(f22364,plain,
( sF217 = k5_relat_1(sK19,sF216)
| ~ spl221_26
| ~ spl221_31
| ~ spl221_54 ),
inference(forward_demodulation,[],[f22350,f21964]) ).
fof(f22366,definition,
( spl221_76
<=> sF217 = k5_relat_1(sK19,sF216) ),
introduced(definition,[new_symbols(definition,[spl221_76])],[avatar_definition]) ).
fof(f22368,plain,
( sF217 = k5_relat_1(sK19,sF216)
| ~ spl221_76 ),
inference(avatar_component_clause,[],[f22366]) ).
fof(f22371,definition,
( spl221_77
<=> m2_relset_1(sF217,sK16,sK16) ),
introduced(definition,[new_symbols(definition,[spl221_77])],[avatar_definition]) ).
fof(f22373,plain,
( m2_relset_1(sF217,sK16,sK16)
| ~ spl221_77 ),
inference(avatar_component_clause,[],[f22371]) ).
fof(f22375,plain,
( spl221_77
| ~ spl221_26
| ~ spl221_31
| ~ spl221_54 ),
inference(avatar_split_clause,[],[f22363,f22194,f21962,f21933,f22371]) ).
fof(f22376,plain,
( spl221_76
| ~ spl221_26
| ~ spl221_31
| ~ spl221_54 ),
inference(avatar_split_clause,[],[f22364,f22194,f21962,f21933,f22366]) ).
fof(f22398,plain,
( m1_subset_1(sF217,k1_zfmisc_1(k2_zfmisc_1(sK16,sK16)))
| ~ spl221_77 ),
inference(unit_resulting_resolution,[],[f20460,f22373]) ).
fof(f22407,plain,
( m1_relset_1(sF217,sK16,sK16)
| ~ spl221_77 ),
inference(resolution,[],[f22373,f20454]) ).
fof(f22411,definition,
( spl221_78
<=> m1_relset_1(sF217,sK16,sK16) ),
introduced(definition,[new_symbols(definition,[spl221_78])],[avatar_definition]) ).
fof(f22413,plain,
( m1_relset_1(sF217,sK16,sK16)
| ~ spl221_78 ),
inference(avatar_component_clause,[],[f22411]) ).
fof(f22414,plain,
( spl221_78
| ~ spl221_77 ),
inference(avatar_split_clause,[],[f22407,f22371,f22411]) ).
fof(f22477,definition,
( spl221_90
<=> m1_subset_1(sF217,k1_zfmisc_1(k2_zfmisc_1(sK16,sK16))) ),
introduced(definition,[new_symbols(definition,[spl221_90])],[avatar_definition]) ).
fof(f22479,plain,
( m1_subset_1(sF217,k1_zfmisc_1(k2_zfmisc_1(sK16,sK16)))
| ~ spl221_90 ),
inference(avatar_component_clause,[],[f22477]) ).
fof(f22480,plain,
( spl221_90
| ~ spl221_77 ),
inference(avatar_split_clause,[],[f22398,f22371,f22477]) ).
fof(f22520,plain,
( v1_relat_1(sF217)
| ~ spl221_90 ),
inference(unit_resulting_resolution,[],[f20461,f22479]) ).
fof(f22548,definition,
( spl221_101
<=> v1_relat_1(sF217) ),
introduced(definition,[new_symbols(definition,[spl221_101])],[avatar_definition]) ).
fof(f22550,plain,
( v1_relat_1(sF217)
| ~ spl221_101 ),
inference(avatar_component_clause,[],[f22548]) ).
fof(f22551,plain,
( spl221_101
| ~ spl221_90 ),
inference(avatar_split_clause,[],[f22520,f22477,f22548]) ).
fof(f22562,plain,
( ! [X0] : k10_relset_1(sK16,sK16,sF217,X0) = k9_relat_1(sF217,X0)
| ~ spl221_78 ),
inference(resolution,[],[f22413,f20921]) ).
fof(f22598,plain,
( sF218 = k9_relat_1(sF217,sK18)
| ~ spl221_32
| ~ spl221_78 ),
inference(superposition,[],[f21969,f22562]) ).
fof(f22600,definition,
( spl221_107
<=> sF218 = k9_relat_1(sF217,sK18) ),
introduced(definition,[new_symbols(definition,[spl221_107])],[avatar_definition]) ).
fof(f22602,plain,
( sF218 = k9_relat_1(sF217,sK18)
| ~ spl221_107 ),
inference(avatar_component_clause,[],[f22600]) ).
fof(f22603,plain,
( spl221_107
| ~ spl221_32
| ~ spl221_78 ),
inference(avatar_split_clause,[],[f22598,f22411,f21967,f22600]) ).
fof(f22666,plain,
( r1_tarski(k2_funct_5(sF217),sF219)
| ~ spl221_47
| ~ spl221_57 ),
inference(superposition,[],[f22123,f22212]) ).
fof(f22668,definition,
( spl221_114
<=> r1_tarski(k2_funct_5(sF217),sF219) ),
introduced(definition,[new_symbols(definition,[spl221_114])],[avatar_definition]) ).
fof(f22670,plain,
( r1_tarski(k2_funct_5(sF217),sF219)
| ~ spl221_114 ),
inference(avatar_component_clause,[],[f22668]) ).
fof(f22671,plain,
( spl221_114
| ~ spl221_47
| ~ spl221_57 ),
inference(avatar_split_clause,[],[f22666,f22210,f22121,f22668]) ).
fof(f22722,plain,
( sK19 = k4_relat_1(sF216)
| ~ v1_relat_1(sK19)
| ~ spl221_45 ),
inference(superposition,[],[f21403,f22107]) ).
fof(f22723,plain,
( sK19 = k4_relat_1(sF216)
| ~ spl221_42
| ~ spl221_45 ),
inference(forward_subsumption_resolution,[],[f22722,f22063]) ).
fof(f22736,definition,
( spl221_121
<=> sK19 = k4_relat_1(sF216) ),
introduced(definition,[new_symbols(definition,[spl221_121])],[avatar_definition]) ).
fof(f22739,plain,
( spl221_121
| ~ spl221_42
| ~ spl221_45 ),
inference(avatar_split_clause,[],[f22723,f22105,f22061,f22736]) ).
fof(f22853,plain,
( ~ r1_tarski(sF218,sF219)
| spl221_27
| ~ spl221_28 ),
inference(unit_resulting_resolution,[],[f20873,f21944,f21939]) ).
fof(f22881,definition,
( spl221_138
<=> r1_tarski(sF218,sF219) ),
introduced(definition,[new_symbols(definition,[spl221_138])],[avatar_definition]) ).
fof(f22883,plain,
( ~ r1_tarski(sF218,sF219)
| spl221_138 ),
inference(avatar_component_clause,[],[f22881]) ).
fof(f22884,plain,
( ~ spl221_138
| spl221_27
| ~ spl221_28 ),
inference(avatar_split_clause,[],[f22853,f21942,f21938,f22881]) ).
fof(f23321,plain,
( k2_funct_5(sF216) = k2_relat_1(sF216)
| ~ spl221_75 ),
inference(resolution,[],[f21454,f22361]) ).
fof(f23322,plain,
( k2_funct_5(sF217) = k2_relat_1(sF217)
| ~ spl221_101 ),
inference(resolution,[],[f21454,f22550]) ).
fof(f23324,definition,
( spl221_163
<=> k2_funct_5(sF217) = k2_relat_1(sF217) ),
introduced(definition,[new_symbols(definition,[spl221_163])],[avatar_definition]) ).
fof(f23326,plain,
( k2_funct_5(sF217) = k2_relat_1(sF217)
| ~ spl221_163 ),
inference(avatar_component_clause,[],[f23324]) ).
fof(f23327,plain,
( spl221_163
| ~ spl221_101 ),
inference(avatar_split_clause,[],[f23322,f22548,f23324]) ).
fof(f23328,plain,
( sF219 = k2_relat_1(sF216)
| ~ spl221_57
| ~ spl221_75 ),
inference(forward_demodulation,[],[f23321,f22212]) ).
fof(f23336,definition,
( spl221_165
<=> sF219 = k2_relat_1(sF216) ),
introduced(definition,[new_symbols(definition,[spl221_165])],[avatar_definition]) ).
fof(f23338,plain,
( sF219 = k2_relat_1(sF216)
| ~ spl221_165 ),
inference(avatar_component_clause,[],[f23336]) ).
fof(f23339,plain,
( spl221_165
| ~ spl221_57
| ~ spl221_75 ),
inference(avatar_split_clause,[],[f23328,f22359,f22210,f23336]) ).
fof(f24067,plain,
( k1_funct_5(sK19) = k1_relat_1(sK19)
| ~ spl221_42 ),
inference(resolution,[],[f21455,f22063]) ).
fof(f24068,plain,
( k1_funct_5(sF216) = k1_relat_1(sF216)
| ~ spl221_75 ),
inference(resolution,[],[f21455,f22361]) ).
fof(f24076,definition,
( spl221_220
<=> k1_funct_5(sF216) = k1_relat_1(sF216) ),
introduced(definition,[new_symbols(definition,[spl221_220])],[avatar_definition]) ).
fof(f24079,plain,
( spl221_220
| ~ spl221_75 ),
inference(avatar_split_clause,[],[f24068,f22359,f24076]) ).
fof(f24080,plain,
( sF219 = k1_relat_1(sK19)
| ~ spl221_33
| ~ spl221_42 ),
inference(forward_demodulation,[],[f24067,f21974]) ).
fof(f24083,definition,
( spl221_221
<=> sF219 = k1_relat_1(sK19) ),
introduced(definition,[new_symbols(definition,[spl221_221])],[avatar_definition]) ).
fof(f24085,plain,
( sF219 = k1_relat_1(sK19)
| ~ spl221_221 ),
inference(avatar_component_clause,[],[f24083]) ).
fof(f24086,plain,
( spl221_221
| ~ spl221_33
| ~ spl221_42 ),
inference(avatar_split_clause,[],[f24080,f22061,f21972,f24083]) ).
fof(f24677,plain,
( sF219 = k2_funct_5(sF217)
| ~ r1_tarski(sF219,k2_funct_5(sF217))
| ~ spl221_114 ),
inference(resolution,[],[f20876,f22670]) ).
fof(f24700,plain,
( sF219 = k2_relat_1(sF217)
| ~ r1_tarski(sF219,k2_funct_5(sF217))
| ~ spl221_114
| ~ spl221_163 ),
inference(forward_demodulation,[],[f24677,f23326]) ).
fof(f24703,plain,
( ~ r1_tarski(sF219,k2_relat_1(sF217))
| sF219 = k2_relat_1(sF217)
| ~ spl221_114
| ~ spl221_163 ),
inference(forward_demodulation,[],[f24700,f23326]) ).
fof(f24707,definition,
( spl221_279
<=> sF219 = k2_relat_1(sF217) ),
introduced(definition,[new_symbols(definition,[spl221_279])],[avatar_definition]) ).
fof(f24709,plain,
( sF219 = k2_relat_1(sF217)
| ~ spl221_279 ),
inference(avatar_component_clause,[],[f24707]) ).
fof(f24711,definition,
( spl221_280
<=> r1_tarski(sF219,k2_relat_1(sF217)) ),
introduced(definition,[new_symbols(definition,[spl221_280])],[avatar_definition]) ).
fof(f24714,plain,
( spl221_279
| ~ spl221_280
| ~ spl221_114
| ~ spl221_163 ),
inference(avatar_split_clause,[],[f24703,f23324,f22668,f24711,f24707]) ).
fof(f25188,plain,
( k9_relat_1(sF216,k1_relat_1(sF216)) = k2_relat_1(sF216)
| ~ spl221_75 ),
inference(resolution,[],[f20529,f22361]) ).
fof(f25195,plain,
( sF219 = k9_relat_1(sF216,k1_relat_1(sF216))
| ~ spl221_75
| ~ spl221_165 ),
inference(forward_demodulation,[],[f25188,f23338]) ).
fof(f25200,definition,
( spl221_324
<=> sF219 = k9_relat_1(sF216,k1_relat_1(sF216)) ),
introduced(definition,[new_symbols(definition,[spl221_324])],[avatar_definition]) ).
fof(f25203,plain,
( spl221_324
| ~ spl221_75
| ~ spl221_165 ),
inference(avatar_split_clause,[],[f25195,f23336,f22359,f25200]) ).
fof(f25209,plain,
( sF219 != k2_funct_5(sF216)
| k1_funct_5(sF216) != k1_relat_1(sF216)
| sF219 != k9_relat_1(sF216,k1_relat_1(sF216))
| k6_relset_1(sK17,sK16,sF216) != k4_relat_1(sF216)
| sK19 != k4_relat_1(sF216)
| k1_funct_5(sF216) != k10_relset_1(sK16,sK17,k6_relset_1(sK17,sK16,sF216),sK16)
| k10_relset_1(sK16,sK17,sK19,sK16) != k2_funct_5(sK19)
| k2_funct_5(sF217) != k2_relat_1(sF217)
| k2_funct_5(sF217) != k9_relat_1(sF216,k2_funct_5(sK19))
| k1_funct_5(sF217) != k9_relat_1(sF216,k1_funct_5(sF216))
| r1_tarski(sF219,k1_funct_5(sF217))
| ~ r1_tarski(k2_funct_5(sF217),k2_funct_5(sF216)) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f25210,plain,
( k6_relset_1(sK17,sK16,sF216) != k4_relat_1(sF216)
| sK19 != k4_relat_1(sF216)
| k1_funct_5(sF216) != k10_relset_1(sK16,sK17,k6_relset_1(sK17,sK16,sF216),sK16)
| k10_relset_1(sK16,sK17,sK19,sK16) != k2_funct_5(sK19)
| k2_funct_5(sF217) != k2_relat_1(sF217)
| k2_funct_5(sF217) != k9_relat_1(sF216,k2_funct_5(sK19))
| k1_funct_5(sF217) != k9_relat_1(sF216,k1_funct_5(sF216))
| r1_tarski(sF219,k2_relat_1(sF217))
| ~ r1_tarski(sF219,k1_funct_5(sF217)) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f25590,plain,
( ! [X0] : r1_tarski(k9_relat_1(sF217,X0),k2_relat_1(sF217))
| ~ spl221_101 ),
inference(resolution,[],[f20531,f22550]) ).
fof(f25591,plain,
( ! [X0] : r1_tarski(k9_relat_1(sF217,X0),sF219)
| ~ spl221_101
| ~ spl221_279 ),
inference(forward_demodulation,[],[f25590,f24709]) ).
fof(f25633,plain,
( r1_tarski(sF218,sF219)
| ~ spl221_101
| ~ spl221_107
| ~ spl221_279 ),
inference(superposition,[],[f25591,f22602]) ).
fof(f25638,plain,
( $false
| ~ spl221_101
| ~ spl221_107
| spl221_138
| ~ spl221_279 ),
inference(forward_subsumption_resolution,[],[f25633,f22883]) ).
fof(f25639,plain,
( ~ spl221_101
| ~ spl221_107
| spl221_138
| ~ spl221_279 ),
inference(avatar_contradiction_clause,[],[f25638]) ).
fof(f25780,plain,
( sK18 = k4_xboole_0(sK18,k4_xboole_0(sK18,sF219))
| ~ spl221_27 ),
inference(unit_resulting_resolution,[],[f21544,f21940]) ).
fof(f25813,definition,
( spl221_356
<=> sK18 = k4_xboole_0(sK18,k4_xboole_0(sK18,sF219)) ),
introduced(definition,[new_symbols(definition,[spl221_356])],[avatar_definition]) ).
fof(f25815,plain,
( sK18 = k4_xboole_0(sK18,k4_xboole_0(sK18,sF219))
| ~ spl221_356 ),
inference(avatar_component_clause,[],[f25813]) ).
fof(f25816,plain,
( spl221_356
| ~ spl221_27 ),
inference(avatar_split_clause,[],[f25780,f21938,f25813]) ).
fof(f34348,plain,
( ! [X0] : k9_relat_1(sF216,k9_relat_1(sK19,X0)) = k9_relat_1(k5_relat_1(sK19,sF216),X0)
| ~ spl221_42
| ~ spl221_75 ),
inference(unit_resulting_resolution,[],[f20515,f22063,f22361]) ).
fof(f34353,plain,
( ! [X0] : k9_relat_1(sF217,X0) = k9_relat_1(sF216,k9_relat_1(sK19,X0))
| ~ spl221_42
| ~ spl221_75
| ~ spl221_76 ),
inference(forward_demodulation,[],[f34348,f22368]) ).
fof(f36454,plain,
( ! [X0] : r1_tarski(k4_xboole_0(k1_relat_1(sK19),k4_xboole_0(k1_relat_1(sK19),X0)),k9_relat_1(k4_relat_1(sK19),k9_relat_1(sK19,X0)))
| ~ spl221_42 ),
inference(resolution,[],[f21621,f22063]) ).
fof(f36459,plain,
( ! [X0] : r1_tarski(k4_xboole_0(k1_relat_1(sK19),k4_xboole_0(k1_relat_1(sK19),X0)),k9_relat_1(sF216,k9_relat_1(sK19,X0)))
| ~ spl221_42
| ~ spl221_45 ),
inference(forward_demodulation,[],[f36454,f22107]) ).
fof(f36465,plain,
( ! [X0] : r1_tarski(k4_xboole_0(k1_relat_1(sK19),k4_xboole_0(k1_relat_1(sK19),X0)),k9_relat_1(sF217,X0))
| ~ spl221_42
| ~ spl221_45
| ~ spl221_75
| ~ spl221_76 ),
inference(forward_demodulation,[],[f36459,f34353]) ).
fof(f36469,plain,
( ! [X0] : r1_tarski(k4_xboole_0(sF219,k4_xboole_0(sF219,X0)),k9_relat_1(sF217,X0))
| ~ spl221_42
| ~ spl221_45
| ~ spl221_75
| ~ spl221_76
| ~ spl221_221 ),
inference(forward_demodulation,[],[f36465,f24085]) ).
fof(f36536,plain,
( r1_tarski(k4_xboole_0(sF219,k4_xboole_0(sF219,sK18)),sF218)
| ~ spl221_42
| ~ spl221_45
| ~ spl221_75
| ~ spl221_76
| ~ spl221_107
| ~ spl221_221 ),
inference(superposition,[],[f36469,f22602]) ).
fof(f36538,plain,
( r1_tarski(k4_xboole_0(sK18,k4_xboole_0(sK18,sF219)),sF218)
| ~ spl221_42
| ~ spl221_45
| ~ spl221_75
| ~ spl221_76
| ~ spl221_107
| ~ spl221_221 ),
inference(forward_demodulation,[],[f36536,f21556]) ).
fof(f36572,plain,
( r1_tarski(sK18,sF218)
| ~ spl221_42
| ~ spl221_45
| ~ spl221_75
| ~ spl221_76
| ~ spl221_107
| ~ spl221_221
| ~ spl221_356 ),
inference(forward_demodulation,[],[f36538,f25815]) ).
fof(f36586,plain,
( $false
| spl221_28
| ~ spl221_42
| ~ spl221_45
| ~ spl221_75
| ~ spl221_76
| ~ spl221_107
| ~ spl221_221
| ~ spl221_356 ),
inference(forward_subsumption_resolution,[],[f36572,f21943]) ).
fof(f36587,plain,
( spl221_28
| ~ spl221_42
| ~ spl221_45
| ~ spl221_75
| ~ spl221_76
| ~ spl221_107
| ~ spl221_221
| ~ spl221_356 ),
inference(avatar_contradiction_clause,[],[f36586]) ).
cnf(s29,plain,
spl221_26,
inference(sat_conversion,[],[f21936]) ).
cnf(s30,plain,
( spl221_27
| spl221_28 ),
inference(sat_conversion,[],[f21945]) ).
cnf(s31,plain,
( ~ spl221_27
| ~ spl221_28 ),
inference(sat_conversion,[],[f21946]) ).
cnf(s33,plain,
spl221_30,
inference(sat_conversion,[],[f21960]) ).
cnf(s34,plain,
spl221_31,
inference(sat_conversion,[],[f21965]) ).
cnf(s35,plain,
spl221_32,
inference(sat_conversion,[],[f21970]) ).
cnf(s36,plain,
spl221_33,
inference(sat_conversion,[],[f21975]) ).
cnf(s40,plain,
( ~ spl221_26
| ~ spl221_30
| ~ spl221_33
| spl221_37 ),
inference(sat_conversion,[],[f22024]) ).
cnf(s42,plain,
( ~ spl221_26
| spl221_38 ),
inference(sat_conversion,[],[f22033]) ).
cnf(s46,plain,
( ~ spl221_26
| spl221_41 ),
inference(sat_conversion,[],[f22056]) ).
cnf(s48,plain,
( ~ spl221_38
| spl221_42 ),
inference(sat_conversion,[],[f22064]) ).
cnf(s50,plain,
( ~ spl221_26
| spl221_44 ),
inference(sat_conversion,[],[f22087]) ).
cnf(s52,plain,
( ~ spl221_30
| ~ spl221_44
| spl221_45 ),
inference(sat_conversion,[],[f22108]) ).
cnf(s56,plain,
( ~ spl221_30
| spl221_35
| ~ spl221_44 ),
inference(sat_conversion,[],[f22117]) ).
cnf(s58,plain,
( ~ spl221_26
| ~ spl221_31
| ~ spl221_35
| spl221_47 ),
inference(sat_conversion,[],[f22124]) ).
cnf(s61,plain,
( ~ spl221_35
| spl221_49 ),
inference(sat_conversion,[],[f22162]) ).
cnf(s62,plain,
( ~ spl221_35
| spl221_50 ),
inference(sat_conversion,[],[f22167]) ).
cnf(s69,plain,
( ~ spl221_35
| spl221_54 ),
inference(sat_conversion,[],[f22197]) ).
cnf(s72,plain,
( ~ spl221_35
| ~ spl221_37
| spl221_57 ),
inference(sat_conversion,[],[f22213]) ).
cnf(s78,plain,
( ~ spl221_26
| ~ spl221_31
| ~ spl221_35
| spl221_59 ),
inference(sat_conversion,[],[f22225]) ).
cnf(s79,plain,
( ~ spl221_26
| ~ spl221_30
| ~ spl221_31
| ~ spl221_35
| spl221_60 ),
inference(sat_conversion,[],[f22230]) ).
cnf(s82,plain,
( ~ spl221_49
| spl221_63 ),
inference(sat_conversion,[],[f22268]) ).
cnf(s90,plain,
( ~ spl221_49
| ~ spl221_60
| spl221_68 ),
inference(sat_conversion,[],[f22303]) ).
cnf(s98,plain,
( ~ spl221_49
| ~ spl221_59
| spl221_74 ),
inference(sat_conversion,[],[f22341]) ).
cnf(s100,plain,
( ~ spl221_54
| spl221_75 ),
inference(sat_conversion,[],[f22362]) ).
cnf(s105,plain,
( ~ spl221_26
| ~ spl221_31
| ~ spl221_54
| spl221_77 ),
inference(sat_conversion,[],[f22375]) ).
cnf(s106,plain,
( ~ spl221_26
| ~ spl221_31
| ~ spl221_54
| spl221_76 ),
inference(sat_conversion,[],[f22376]) ).
cnf(s107,plain,
( ~ spl221_77
| spl221_78 ),
inference(sat_conversion,[],[f22414]) ).
cnf(s127,plain,
( ~ spl221_77
| spl221_90 ),
inference(sat_conversion,[],[f22480]) ).
cnf(s143,plain,
( ~ spl221_90
| spl221_101 ),
inference(sat_conversion,[],[f22551]) ).
cnf(s156,plain,
( ~ spl221_32
| ~ spl221_78
| spl221_107 ),
inference(sat_conversion,[],[f22603]) ).
cnf(s165,plain,
( ~ spl221_47
| ~ spl221_57
| spl221_114 ),
inference(sat_conversion,[],[f22671]) ).
cnf(s173,plain,
( ~ spl221_42
| ~ spl221_45
| spl221_121 ),
inference(sat_conversion,[],[f22739]) ).
cnf(s195,plain,
( spl221_27
| ~ spl221_28
| ~ spl221_138 ),
inference(sat_conversion,[],[f22884]) ).
cnf(s236,plain,
( ~ spl221_101
| spl221_163 ),
inference(sat_conversion,[],[f23327]) ).
cnf(s240,plain,
( ~ spl221_57
| ~ spl221_75
| spl221_165 ),
inference(sat_conversion,[],[f23339]) ).
cnf(s326,plain,
( ~ spl221_75
| spl221_220 ),
inference(sat_conversion,[],[f24079]) ).
cnf(s329,plain,
( ~ spl221_33
| ~ spl221_42
| spl221_221 ),
inference(sat_conversion,[],[f24086]) ).
cnf(s400,plain,
( ~ spl221_114
| ~ spl221_163
| spl221_279
| ~ spl221_280 ),
inference(sat_conversion,[],[f24714]) ).
cnf(s454,plain,
( ~ spl221_75
| ~ spl221_165
| spl221_324 ),
inference(sat_conversion,[],[f25203]) ).
cnf(s458,plain,
( ~ spl221_41
| ~ spl221_47
| ~ spl221_50
| ~ spl221_57
| ~ spl221_63
| ~ spl221_68
| ~ spl221_74
| ~ spl221_121
| spl221_149
| ~ spl221_163
| ~ spl221_220
| ~ spl221_324 ),
inference(sat_conversion,[],[f25209]) ).
cnf(s459,plain,
( ~ spl221_41
| ~ spl221_50
| ~ spl221_63
| ~ spl221_68
| ~ spl221_74
| ~ spl221_121
| ~ spl221_149
| ~ spl221_163
| spl221_280 ),
inference(sat_conversion,[],[f25210]) ).
cnf(s502,plain,
( ~ spl221_101
| ~ spl221_107
| spl221_138
| ~ spl221_279 ),
inference(sat_conversion,[],[f25639]) ).
cnf(s555,plain,
( ~ spl221_27
| spl221_356 ),
inference(sat_conversion,[],[f25816]) ).
cnf(s1493,plain,
( spl221_28
| ~ spl221_42
| ~ spl221_45
| ~ spl221_75
| ~ spl221_76
| ~ spl221_107
| ~ spl221_221
| ~ spl221_356 ),
inference(sat_conversion,[],[f36587]) ).
cnf(s1502,plain,
spl221_44,
inference(rat,[],[s50,s29]) ).
cnf(s1503,plain,
spl221_41,
inference(rat,[],[s46,s29]) ).
cnf(s1504,plain,
spl221_38,
inference(rat,[],[s42,s29]) ).
cnf(s1505,plain,
spl221_37,
inference(rat,[],[s40,s33,s36,s29]) ).
cnf(s1507,plain,
spl221_45,
inference(rat,[],[s52,s33,s1502]) ).
cnf(s1508,plain,
spl221_35,
inference(rat,[],[s56,s33,s1502]) ).
cnf(s1512,plain,
spl221_42,
inference(rat,[],[s48,s1504]) ).
cnf(s1515,plain,
spl221_57,
inference(rat,[],[s72,s1505,s1508]) ).
cnf(s1518,plain,
spl221_54,
inference(rat,[],[s69,s1508]) ).
cnf(s1521,plain,
spl221_50,
inference(rat,[],[s62,s1508]) ).
cnf(s1522,plain,
spl221_49,
inference(rat,[],[s61,s1508]) ).
cnf(s1524,plain,
spl221_59,
inference(rat,[],[s78,s29,s34,s1508]) ).
cnf(s1525,plain,
spl221_47,
inference(rat,[],[s58,s29,s34,s1508]) ).
cnf(s1527,plain,
spl221_60,
inference(rat,[],[s79,s29,s33,s34,s1508]) ).
cnf(s1528,plain,
spl221_221,
inference(rat,[],[s329,s36,s1512]) ).
cnf(s1530,plain,
spl221_121,
inference(rat,[],[s173,s1507,s1512]) ).
cnf(s1548,plain,
spl221_75,
inference(rat,[],[s100,s1518]) ).
cnf(s1549,plain,
spl221_76,
inference(rat,[],[s106,s29,s34,s1518]) ).
cnf(s1550,plain,
spl221_77,
inference(rat,[],[s105,s29,s34,s1518]) ).
cnf(s1554,plain,
spl221_63,
inference(rat,[],[s82,s1522]) ).
cnf(s1556,plain,
spl221_74,
inference(rat,[],[s98,s1522,s1524]) ).
cnf(s1559,plain,
spl221_114,
inference(rat,[],[s165,s1515,s1525]) ).
cnf(s1563,plain,
spl221_68,
inference(rat,[],[s90,s1522,s1527]) ).
cnf(s1567,plain,
spl221_220,
inference(rat,[],[s326,s1548]) ).
cnf(s1568,plain,
spl221_165,
inference(rat,[],[s240,s1515,s1548]) ).
cnf(s1574,plain,
spl221_90,
inference(rat,[],[s127,s1550]) ).
cnf(s1585,plain,
spl221_78,
inference(rat,[],[s107,s1550]) ).
cnf(s1608,plain,
spl221_324,
inference(rat,[],[s454,s1548,s1568]) ).
cnf(s1631,plain,
spl221_101,
inference(rat,[],[s143,s1574]) ).
cnf(s1634,plain,
spl221_107,
inference(rat,[],[s156,s35,s1585]) ).
cnf(s1684,plain,
spl221_163,
inference(rat,[],[s236,s1631]) ).
cnf(s1720,plain,
spl221_149,
inference(rat,[],[s458,s1608,s1567,s1563,s1554,s1530,s1556,s1525,s1521,s1515,s1503,s1684]) ).
cnf(s1767,plain,
spl221_280,
inference(rat,[],[s459,s1684,s1563,s1554,s1530,s1556,s1521,s1503,s1720]) ).
cnf(s1820,plain,
spl221_279,
inference(rat,[],[s400,s1684,s1559,s1767]) ).
cnf(s1845,plain,
spl221_138,
inference(rat,[],[s502,s1634,s1631,s1820]) ).
cnf(s1953,plain,
spl221_27,
inference(rat,[],[s30,s195,s1845]) ).
cnf(s1961,plain,
spl221_356,
inference(rat,[],[s555,s1953]) ).
cnf(s1969,plain,
~ spl221_28,
inference(rat,[],[s31,s1953]) ).
cnf(s1993,plain,
$false,
inference(rat,[],[s1493,s1634,s1528,s1548,s1549,s1512,s1507,s1961,s1969]) ).
fof(f36591,plain,
$false,
inference(avatar_sat_refutation,[],[s1993]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU442+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.41 % Computer : n007.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 28 05:29:28 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.47 Running first-order theorem proving
% 0.16/0.47 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 24.18/5.62 % (2085074)Detected formulas, will run a generic FOF schedule.
% 24.18/5.62 % (2085095)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=1707523953:i=141695:sd=1:nm=32:gsp=on:ss=included_2986 on theBenchmark for (2986ds/141695Mi)
% 24.18/5.62 % (2085096)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3287599187:i=109:sd=1:ins=1:gsp=on:ss=axioms_2986 on theBenchmark for (2986ds/109Mi)
% 24.18/5.62 % (2085097)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1873654937:i=119:av=off:ss=axioms_2986 on theBenchmark for (2986ds/119Mi)
% 24.18/5.62 % (2085094)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=3686592886:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2986 on theBenchmark for (2986ds/134677Mi)
% 24.18/5.62 % (2085098)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3379703617:s2a=on:i=139:gtg=position_2986 on theBenchmark for (2986ds/139Mi)
% 24.18/5.62 % (2085093)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=825967672:i=141193_2986 on theBenchmark for (2986ds/141193Mi)
% 24.18/5.62 % (2085099)dis-21_1_sil=8000:lcm=predicate:random_seed=1772233671:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2986 on theBenchmark for (2986ds/129Mi)
% 24.18/5.62 % (2085098)Instruction limit reached!
% 24.18/5.62 % (2085098)------------------------------
% 24.18/5.62 % (2085098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.18/5.62 % (2085098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.18/5.62 % (2085098)CaDiCaL version: 2.1.3
% 24.18/5.62 % (2085098)Termination reason: Instruction limit
% 24.18/5.62 % (2085098)Termination phase: Property scanning
% 24.18/5.62 % (2085098)Time elapsed: 0.114 s
% 24.18/5.62 % (2085098)Peak memory usage: 112 MB
% 24.18/5.62 % (2085098)Instructions burned: 140 (million)
% 24.18/5.62 % (2085096)Instruction limit reached!
% 24.18/5.62 % (2085096)------------------------------
% 24.18/5.62 % (2085096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.18/5.62 % (2085096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.18/5.62 % (2085096)CaDiCaL version: 2.1.3
% 24.18/5.62 % (2085096)Termination reason: Instruction limit
% 24.18/5.62 % (2085096)Termination phase: SInE selection
% 24.18/5.62 % (2085096)Time elapsed: 0.121 s
% 24.18/5.62 % (2085096)Peak memory usage: 112 MB
% 24.18/5.62 % (2085096)Instructions burned: 109 (million)
% 24.18/5.62 % (2085099)Instruction limit reached!
% 24.18/5.62 % (2085099)------------------------------
% 24.18/5.62 % (2085099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.18/5.62 % (2085099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.18/5.62 % (2085099)CaDiCaL version: 2.1.3
% 24.18/5.62 % (2085099)Termination reason: Instruction limit
% 24.18/5.62 % (2085099)Termination phase: SInE selection
% 24.18/5.62 % (2085099)Time elapsed: 0.132 s
% 24.18/5.62 % (2085099)Peak memory usage: 112 MB
% 24.18/5.62 % (2085099)Instructions burned: 130 (million)
% 24.18/5.62 % (2085097)Instruction limit reached!
% 24.18/5.62 % (2085097)------------------------------
% 24.18/5.62 % (2085097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.18/5.62 % (2085097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.18/5.62 % (2085097)CaDiCaL version: 2.1.3
% 24.18/5.62 % (2085097)Termination reason: Instruction limit
% 24.18/5.62 % (2085097)Termination phase: SInE selection
% 24.18/5.62 % (2085097)Time elapsed: 0.134 s
% 24.18/5.62 % (2085097)Peak memory usage: 112 MB
% 24.18/5.62 % (2085097)Instructions burned: 119 (million)
% 24.18/5.62 % (2085110)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=1908277530:s2a=on:i=248:s2at=1.23:gtg=position_2982 on theBenchmark for (2982ds/248Mi)
% 24.18/5.62 % (2085107)lrs+10_1_sil=8000:sp=occurrence:random_seed=557890083:i=285:sd=3:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/285Mi)
% 24.18/5.62 % (2085108)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2955306481:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/157Mi)
% 24.18/5.62 % (2085109)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1355385423:i=325:sd=1:ss=axioms:sgt=32_2982 on theBenchmark for (2982ds/325Mi)
% 24.18/5.62 % (2085108)Instruction limit reached!
% 31.08/6.63 % (2085108)------------------------------
% 31.08/6.63 % (2085108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/6.63 % (2085108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/6.63 % (2085108)CaDiCaL version: 2.1.3
% 31.08/6.63 % (2085108)Termination reason: Instruction limit
% 31.08/6.63 % (2085108)Termination phase: Property scanning
% 31.08/6.63 % (2085108)Time elapsed: 0.071 s
% 31.08/6.63 % (2085108)Peak memory usage: 113 MB
% 31.08/6.63 % (2085108)Instructions burned: 157 (million)
% 31.08/6.63 % (2085110)Instruction limit reached!
% 31.08/6.63 % (2085110)------------------------------
% 31.08/6.63 % (2085110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/6.63 % (2085110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/6.63 % (2085110)CaDiCaL version: 2.1.3
% 31.08/6.63 % (2085110)Termination reason: Instruction limit
% 31.08/6.63 % (2085110)Termination phase: Property scanning
% 31.08/6.63 % (2085110)Time elapsed: 0.110 s
% 31.08/6.63 % (2085110)Peak memory usage: 112 MB
% 31.08/6.63 % (2085110)Instructions burned: 249 (million)
% 31.08/6.63 % (2085115)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3740504153:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2979 on theBenchmark for (2979ds/294Mi)
% 31.08/6.63 % (2085107)Instruction limit reached!
% 31.08/6.63 % (2085107)------------------------------
% 31.08/6.63 % (2085107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/6.63 % (2085107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/6.63 % (2085107)CaDiCaL version: 2.1.3
% 31.08/6.63 % (2085107)Termination reason: Instruction limit
% 31.08/6.63 % (2085107)Termination phase: Saturation
% 31.08/6.63 % (2085107)Time elapsed: 0.318 s
% 31.08/6.63 % (2085107)Peak memory usage: 120 MB
% 31.08/6.63 % (2085107)Instructions burned: 285 (million)
% 31.08/6.63 % (2085116)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=376114751:i=2350_2979 on theBenchmark for (2979ds/2350Mi)
% 31.08/6.63 % (2085109)Instruction limit reached!
% 31.08/6.63 % (2085109)------------------------------
% 31.08/6.63 % (2085109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/6.63 % (2085109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/6.63 % (2085109)CaDiCaL version: 2.1.3
% 31.08/6.63 % (2085109)Termination reason: Instruction limit
% 31.08/6.63 % (2085109)Termination phase: Saturation
% 31.08/6.63 % (2085109)Time elapsed: 0.401 s
% 31.08/6.63 % (2085109)Peak memory usage: 119 MB
% 31.08/6.63 % (2085109)Instructions burned: 326 (million)
% 31.08/6.63 % (2085115)Instruction limit reached!
% 31.08/6.63 % (2085115)------------------------------
% 31.08/6.63 % (2085115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/6.63 % (2085115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/6.63 % (2085115)CaDiCaL version: 2.1.3
% 31.08/6.63 % (2085115)Termination reason: Instruction limit
% 31.08/6.63 % (2085115)Termination phase: Property scanning
% 31.08/6.63 % (2085115)Time elapsed: 0.192 s
% 31.08/6.63 % (2085115)Peak memory usage: 118 MB
% 31.08/6.63 % (2085115)Instructions burned: 295 (million)
% 31.08/6.63 % (2085119)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3026210186:cts=off:i=113:fsr=off:ss=included:sgt=4_2977 on theBenchmark for (2977ds/113Mi)
% 31.08/6.63 % (2085119)Instruction limit reached!
% 31.08/6.63 % (2085119)------------------------------
% 31.08/6.63 % (2085119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/6.63 % (2085119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/6.63 % (2085119)CaDiCaL version: 2.1.3
% 31.08/6.63 % (2085119)Termination reason: Instruction limit
% 31.08/6.63 % (2085119)Termination phase: SInE selection
% 31.08/6.63 % (2085119)Time elapsed: 0.084 s
% 31.08/6.63 % (2085119)Peak memory usage: 112 MB
% 31.08/6.63 % (2085119)Instructions burned: 113 (million)
% 31.08/6.63 % (2085120)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4171859785:i=127:av=off:fsr=off:sup=off_2975 on theBenchmark for (2975ds/127Mi)
% 31.08/6.63 % (2085121)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1099131490:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2975 on theBenchmark for (2975ds/114Mi)
% 31.08/6.63 % (2085123)lrs+10_1_sil=8000:sp=occurrence:random_seed=74060312:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2974 on theBenchmark for (2974ds/907Mi)
% 61.72/10.80 % (2085121)Instruction limit reached!
% 61.72/10.80 % (2085121)------------------------------
% 61.72/10.80 % (2085121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.72/10.80 % (2085121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.72/10.80 % (2085121)CaDiCaL version: 2.1.3
% 61.72/10.80 % (2085121)Termination reason: Instruction limit
% 61.72/10.80 % (2085121)Termination phase: Property scanning
% 61.72/10.80 % (2085121)Time elapsed: 0.095 s
% 61.72/10.80 % (2085121)Peak memory usage: 112 MB
% 61.72/10.80 % (2085121)Instructions burned: 114 (million)
% 61.72/10.80 % (2085120)Instruction limit reached!
% 61.72/10.80 % (2085120)------------------------------
% 61.72/10.80 % (2085120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.72/10.80 % (2085120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.72/10.80 % (2085120)CaDiCaL version: 2.1.3
% 61.72/10.80 % (2085120)Termination reason: Instruction limit
% 61.72/10.80 % (2085120)Termination phase: Preprocessing 1
% 61.72/10.80 % (2085120)Time elapsed: 0.146 s
% 61.72/10.80 % (2085120)Peak memory usage: 113 MB
% 61.72/10.80 % (2085120)Instructions burned: 127 (million)
% 61.72/10.80 % (2085129)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1885812241:i=5202:ss=axioms:sgt=16_2971 on theBenchmark for (2971ds/5202Mi)
% 61.72/10.80 % (2085128)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=958534537:i=437:sd=1:aac=none:ss=included_2971 on theBenchmark for (2971ds/437Mi)
% 61.72/10.80 % (2085128)Instruction limit reached!
% 61.72/10.80 % (2085128)------------------------------
% 61.72/10.80 % (2085128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.72/10.80 % (2085128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.72/10.80 % (2085128)CaDiCaL version: 2.1.3
% 61.72/10.80 % (2085128)Termination reason: Instruction limit
% 61.72/10.80 % (2085128)Termination phase: Saturation
% 61.72/10.80 % (2085128)Time elapsed: 0.490 s
% 61.72/10.80 % (2085128)Peak memory usage: 121 MB
% 61.72/10.80 % (2085128)Instructions burned: 437 (million)
% 61.72/10.80 % (2085123)Instruction limit reached!
% 61.72/10.80 % (2085123)------------------------------
% 61.72/10.80 % (2085123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.72/10.80 % (2085123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.72/10.80 % (2085123)CaDiCaL version: 2.1.3
% 61.72/10.80 % (2085123)Termination reason: Instruction limit
% 61.72/10.80 % (2085123)Termination phase: Property scanning
% 61.72/10.80 % (2085123)Time elapsed: 0.879 s
% 61.72/10.80 % (2085123)Peak memory usage: 135 MB
% 61.72/10.80 % (2085123)Instructions burned: 908 (million)
% 61.72/10.80 % (2085133)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=48304902:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2963 on theBenchmark for (2963ds/134Mi)
% 61.72/10.80 % (2085135)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2455670118:st=8:i=592:sd=3:ep=RST:ss=axioms_2963 on theBenchmark for (2963ds/592Mi)
% 61.72/10.80 % (2085133)Instruction limit reached!
% 61.72/10.80 % (2085133)------------------------------
% 61.72/10.80 % (2085133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.72/10.80 % (2085133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.72/10.80 % (2085133)CaDiCaL version: 2.1.3
% 61.72/10.80 % (2085133)Termination reason: Instruction limit
% 61.72/10.80 % (2085133)Termination phase: NewCNF
% 61.72/10.80 % (2085133)Time elapsed: 0.161 s
% 61.72/10.80 % (2085133)Peak memory usage: 115 MB
% 61.72/10.80 % (2085133)Instructions burned: 134 (million)
% 61.72/10.80 % (2085140)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2678515229:st=3:i=13193:sd=3:ss=axioms_2959 on theBenchmark for (2959ds/13193Mi)
% 61.72/10.80 % (2085116)Instruction limit reached!
% 61.72/10.80 % (2085116)------------------------------
% 61.72/10.80 % (2085116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.72/10.80 % (2085116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.72/10.80 % (2085116)CaDiCaL version: 2.1.3
% 61.72/10.80 % (2085116)Termination reason: Instruction limit
% 61.72/10.80 % (2085116)Termination phase: Property scanning
% 61.72/10.80 % (2085116)Time elapsed: 2.224 s
% 61.72/10.80 % (2085116)Peak memory usage: 171 MB
% 61.72/10.80 % (2085116)Instructions burned: 2353 (million)
% 61.72/10.80 % (2085135)Instruction limit reached!
% 61.72/10.80 % (2085135)------------------------------
% 61.72/10.80 % (2085135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085135)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085135)Termination reason: Instruction limit
% 42.81/11.43 % (2085135)Termination phase: Preprocessing 3
% 42.81/11.43 % (2085135)Time elapsed: 0.622 s
% 42.81/11.43 % (2085135)Peak memory usage: 134 MB
% 42.81/11.43 % (2085135)Instructions burned: 593 (million)
% 42.81/11.43 % (2085144)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=1801501421:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2954 on theBenchmark for (2954ds/125Mi)
% 42.81/11.43 % (2085144)Instruction limit reached!
% 42.81/11.43 % (2085144)------------------------------
% 42.81/11.43 % (2085144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085144)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085144)Termination reason: Instruction limit
% 42.81/11.43 % (2085144)Termination phase: Property scanning
% 42.81/11.43 % (2085144)Time elapsed: 0.055 s
% 42.81/11.43 % (2085144)Peak memory usage: 112 MB
% 42.81/11.43 % (2085144)Instructions burned: 126 (million)
% 42.81/11.43 % (2085145)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3056114316:i=134:gtgl=5:slsql=off:gtg=exists_sym_2953 on theBenchmark for (2953ds/134Mi)
% 42.81/11.43 % (2085145)Instruction limit reached!
% 42.81/11.43 % (2085145)------------------------------
% 42.81/11.43 % (2085145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085145)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085145)Termination reason: Instruction limit
% 42.81/11.43 % (2085145)Termination phase: Property scanning
% 42.81/11.43 % (2085145)Time elapsed: 0.059 s
% 42.81/11.43 % (2085145)Peak memory usage: 112 MB
% 42.81/11.43 % (2085145)Instructions burned: 136 (million)
% 42.81/11.43 % (2085147)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3314019693:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2952 on theBenchmark for (2952ds/141Mi)
% 42.81/11.43 % (2085147)Instruction limit reached!
% 42.81/11.43 % (2085147)------------------------------
% 42.81/11.43 % (2085147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085147)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085147)Termination reason: Instruction limit
% 42.81/11.43 % (2085147)Termination phase: Saturation
% 42.81/11.43 % (2085147)Time elapsed: 0.119 s
% 42.81/11.43 % (2085147)Peak memory usage: 117 MB
% 42.81/11.43 % (2085147)Instructions burned: 143 (million)
% 42.81/11.43 % (2085150)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3269804093:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2951 on theBenchmark for (2951ds/431Mi)
% 42.81/11.43 % (2085181)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=307082282:i=6060:aac=none:ins=25_2949 on theBenchmark for (2949ds/6060Mi)
% 42.81/11.43 % (2085150)Instruction limit reached!
% 42.81/11.43 % (2085150)------------------------------
% 42.81/11.43 % (2085150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085150)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085150)Termination reason: Instruction limit
% 42.81/11.43 % (2085150)Termination phase: Saturation
% 42.81/11.43 % (2085150)Time elapsed: 0.302 s
% 42.81/11.43 % (2085150)Peak memory usage: 119 MB
% 42.81/11.43 % (2085150)Instructions burned: 431 (million)
% 42.81/11.43 % (2085260)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=1510144310:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2946 on theBenchmark for (2946ds/150Mi)
% 42.81/11.43 % (2085260)Instruction limit reached!
% 42.81/11.43 % (2085260)------------------------------
% 42.81/11.43 % (2085260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085260)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085260)Termination reason: Instruction limit
% 42.81/11.43 % (2085260)Termination phase: Preprocessing 1
% 42.81/11.43 % (2085260)Time elapsed: 0.134 s
% 42.81/11.43 % (2085260)Peak memory usage: 113 MB
% 42.81/11.43 % (2085260)Instructions burned: 151 (million)
% 42.81/11.43 % (2085309)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1941460358:i=14155:bd=all_2943 on theBenchmark for (2943ds/14155Mi)
% 42.81/11.43 % (2085129)Instruction limit reached!
% 42.81/11.43 % (2085129)------------------------------
% 42.81/11.43 % (2085129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085129)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085129)Termination reason: Instruction limit
% 42.81/11.43 % (2085129)Termination phase: Saturation
% 42.81/11.43 % (2085129)Time elapsed: 3.020 s
% 42.81/11.43 % (2085129)Peak memory usage: 606 MB
% 42.81/11.43 % (2085129)Instructions burned: 5205 (million)
% 42.81/11.43 % (2085311)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1154376060:i=667:av=off:fsr=off_2938 on theBenchmark for (2938ds/667Mi)
% 42.81/11.43 % (2085311)Instruction limit reached!
% 42.81/11.43 % (2085311)------------------------------
% 42.81/11.43 % (2085311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085311)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085311)Termination reason: Instruction limit
% 42.81/11.43 % (2085311)Termination phase: NewCNF
% 42.81/11.43 % (2085311)Time elapsed: 0.302 s
% 42.81/11.43 % (2085311)Peak memory usage: 149 MB
% 42.81/11.43 % (2085311)Instructions burned: 670 (million)
% 42.81/11.43 % (2085313)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=4029720015:s2a=on:i=185:s2at=1.8:fdi=4_2934 on theBenchmark for (2934ds/185Mi)
% 42.81/11.43 % (2085313)Instruction limit reached!
% 42.81/11.43 % (2085313)------------------------------
% 42.81/11.43 % (2085313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085313)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085313)Termination reason: Instruction limit
% 42.81/11.43 % (2085313)Termination phase: SInE selection
% 42.81/11.43 % (2085313)Time elapsed: 0.091 s
% 42.81/11.43 % (2085313)Peak memory usage: 113 MB
% 42.81/11.43 % (2085313)Instructions burned: 185 (million)
% 42.81/11.43 % (2085315)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3421853661:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2931 on theBenchmark for (2931ds/193Mi)
% 42.81/11.43 % (2085315)Instruction limit reached!
% 42.81/11.43 % (2085315)------------------------------
% 42.81/11.43 % (2085315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085315)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085315)Termination reason: Instruction limit
% 42.81/11.43 % (2085315)Termination phase: SInE selection
% 42.81/11.43 % (2085315)Time elapsed: 0.097 s
% 42.81/11.43 % (2085315)Peak memory usage: 112 MB
% 42.81/11.43 % (2085315)Instructions burned: 194 (million)
% 42.81/11.43 % (2085317)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1748164332:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2929 on theBenchmark for (2929ds/4850Mi)
% 42.81/11.43 % (2085317)Instruction limit reached!
% 42.81/11.43 % (2085317)------------------------------
% 42.81/11.43 % (2085317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085317)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085317)Termination reason: Instruction limit
% 42.81/11.43 % (2085317)Termination phase: Saturation
% 42.81/11.43 % (2085317)Time elapsed: 1.618 s
% 42.81/11.43 % (2085317)Peak memory usage: 224 MB
% 42.81/11.43 % (2085317)Instructions burned: 4851 (million)
% 42.81/11.43 % (2085319)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2009935121:i=12111:sd=1:ss=included_2911 on theBenchmark for (2911ds/12111Mi)
% 42.81/11.43 % (2085181)Instruction limit reached!
% 42.81/11.43 % (2085181)------------------------------
% 42.81/11.43 % (2085181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085181)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085181)Termination reason: Instruction limit
% 42.81/11.43 % (2085181)Termination phase: Saturation
% 42.81/11.43 % (2085181)Time elapsed: 4.621 s
% 42.81/11.43 % (2085181)Peak memory usage: 598 MB
% 42.81/11.43 % (2085181)Instructions burned: 6064 (million)
% 42.81/11.43 % (2085321)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=737841059:i=319:kws=precedence:fsr=off_2901 on theBenchmark for (2901ds/319Mi)
% 42.81/11.43 % (2085319)First to succeed.
% 42.81/11.43 % (2085319)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2085074"
% 42.81/11.43 % (2085321)Instruction limit reached!
% 42.81/11.43 % (2085321)------------------------------
% 42.81/11.43 % (2085321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/11.43 % (2085321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/11.43 % (2085321)CaDiCaL version: 2.1.3
% 42.81/11.43 % (2085321)Termination reason: Instruction limit
% 42.81/11.43 % (2085321)Termination phase: Naming
% 42.81/11.43 % (2085321)Time elapsed: 0.255 s
% 42.81/11.43 % (2085321)Peak memory usage: 135 MB
% 42.81/11.43 % (2085321)Instructions burned: 319 (million)
% 42.81/11.43 % (2085319)Refutation found. Thanks to Tanya!
% 42.81/11.43 % SZS status Theorem for theBenchmark
% 42.81/11.43 % SZS output start Proof for theBenchmark
% See solution above
% 66.13/11.66 % (2085319)------------------------------
% 66.13/11.66 % (2085319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.13/11.66 % (2085319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.13/11.66 % (2085319)CaDiCaL version: 2.1.3
% 66.13/11.66 % (2085319)Termination reason: Refutation
% 66.13/11.66 % (2085319)Time elapsed: 1.196 s
% 66.13/11.66 % (2085319)Peak memory usage: 181 MB
% 66.13/11.66 % (2085319)Instructions burned: 3018 (million)
% 66.13/11.66 % (2085319)------------------------------
% 66.13/11.66 % (2085319)------------------------------
% 66.13/11.66 % (2085074)Success in time 10.413 s
% 66.13/11.66 % Vampire exiting
%------------------------------------------------------------------------------