%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU447+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:49:09 PM UTC 2026
% Result : Theorem 67.08s 11.30s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 70
% Syntax : Number of formulae : 357 ( 83 unt; 53 def)
% Number of atoms : 914 ( 138 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1039 ( 482 ~; 480 |; 10 &)
% ( 45 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 50 ( 48 usr; 45 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 15 con; 0-5 aty)
% Number of variables : 189 ( 0 sgn 183 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f493,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> k3_subset_1(X0,X1) = k4_xboole_0(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_subset_1) ).
fof(f565,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> m1_subset_1(k3_subset_1(X0,X1),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_subset_1) ).
fof(f566,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> k3_subset_1(X0,k3_subset_1(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',involutiveness_k3_subset_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/sandbox2/benchmark/theBenchmark.p',t159_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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1418,axiom,
! [X0,X1,X2,X3] :
( m1_relset_1(X2,X0,X1)
=> m1_subset_1(k10_relset_1(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k10_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/sandbox2/benchmark/theBenchmark.p',redefinition_k10_relset_1) ).
fof(f19064,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
=> m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_relset_2) ).
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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',redefinition_k9_relset_2) ).
fof(f19120,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> k3_subset_1(X1,k8_relset_2(X0,X1,X2,X3)) = k9_relat_1(k3_subset_1(k2_zfmisc_1(X0,X1),X3),X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t49_relset_2) ).
fof(f19121,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m2_relset_1(X3,X0,X1)
=> k3_subset_1(X1,k10_relset_1(X0,X1,X3,X2)) = k8_relset_2(X0,X1,X2,k3_subset_1(k2_zfmisc_1(X0,X1),X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t50_relset_2) ).
fof(f19130,conjecture,
! [X0,X1,X2,X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m2_relset_1(X4,X0,X1)
=> ! [X5] :
( m2_relset_1(X5,X1,X2)
=> k8_relset_2(X1,X2,k10_relset_1(X0,X1,X4,X3),X5) = k8_relset_2(X0,X2,X3,k3_subset_1(k2_zfmisc_1(X0,X2),k9_relset_2(X0,X1,X2,X4,k3_subset_1(k2_zfmisc_1(X1,X2),X5)))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t59_relset_2) ).
fof(f19131,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m2_relset_1(X4,X0,X1)
=> ! [X5] :
( m2_relset_1(X5,X1,X2)
=> k8_relset_2(X1,X2,k10_relset_1(X0,X1,X4,X3),X5) = k8_relset_2(X0,X2,X3,k3_subset_1(k2_zfmisc_1(X0,X2),k9_relset_2(X0,X1,X2,X4,k3_subset_1(k2_zfmisc_1(X1,X2),X5)))) ) ) ),
inference(negated_conjecture,[status(cth)],[f19130]) ).
fof(f19215,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f19064]) ).
fof(f19216,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(flattening,[],[f19215]) ).
fof(f19219,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(f19220,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,[],[f19219]) ).
fof(f19221,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(f19222,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,[],[f19221]) ).
fof(f19281,plain,
! [X0,X1,X2] :
( ! [X3] :
( k3_subset_1(X1,k8_relset_2(X0,X1,X2,X3)) = k9_relat_1(k3_subset_1(k2_zfmisc_1(X0,X1),X3),X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19120]) ).
fof(f19282,plain,
! [X0,X1,X2] :
( ! [X3] :
( k3_subset_1(X1,k10_relset_1(X0,X1,X3,X2)) = k8_relset_2(X0,X1,X2,k3_subset_1(k2_zfmisc_1(X0,X1),X3))
| ~ m2_relset_1(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19121]) ).
fof(f19291,plain,
? [X0,X1,X2,X3] :
( ? [X4] :
( ? [X5] :
( k8_relset_2(X1,X2,k10_relset_1(X0,X1,X4,X3),X5) != k8_relset_2(X0,X2,X3,k3_subset_1(k2_zfmisc_1(X0,X2),k9_relset_2(X0,X1,X2,X4,k3_subset_1(k2_zfmisc_1(X1,X2),X5))))
& m2_relset_1(X5,X1,X2) )
& m2_relset_1(X4,X0,X1) )
& m1_subset_1(X3,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19131]) ).
fof(f19322,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(f19323,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(f19384,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(f19645,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(f19646,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k10_relset_1(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1418]) ).
fof(f19841,plain,
! [X0,X1] :
( k3_subset_1(X0,k3_subset_1(X0,X1)) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f566]) ).
fof(f19842,plain,
! [X0,X1] :
( m1_subset_1(k3_subset_1(X0,X1),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f565]) ).
fof(f19868,plain,
! [X0,X1] :
( k3_subset_1(X0,X1) = k4_xboole_0(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f493]) ).
fof(f20021,plain,
( k8_relset_2(sK15,sK16,k10_relset_1(sK14,sK15,sK18,sK17),sK19) != k8_relset_2(sK14,sK16,sK17,k3_subset_1(k2_zfmisc_1(sK14,sK16),k9_relset_2(sK14,sK15,sK16,sK18,k3_subset_1(k2_zfmisc_1(sK15,sK16),sK19))))
& m2_relset_1(sK19,sK15,sK16)
& m2_relset_1(sK18,sK14,sK15)
& m1_subset_1(sK17,k1_zfmisc_1(sK14)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15,sK16,sK17,sK18,sK19]),skolemize(X0,sK14),skolemize(X1,sK15),skolemize(X2,sK16),skolemize(X3,sK17),skolemize(X4,sK18),skolemize(X5,sK19)],[f19291]) ).
fof(f20032,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(f20303,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f19216]) ).
fof(f20305,plain,
! [X2,X3,X0,X1,X4] :
( m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[],[f19220]) ).
fof(f20306,plain,
! [X2,X3,X0,X1,X4] :
( k5_relat_1(X3,X4) = k9_relset_2(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))) ),
inference(cnf_transformation,[],[f19222]) ).
fof(f20384,plain,
! [X2,X3,X0,X1] :
( k3_subset_1(X1,k8_relset_2(X0,X1,X2,X3)) = k9_relat_1(k3_subset_1(k2_zfmisc_1(X0,X1),X3),X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19281]) ).
fof(f20385,plain,
! [X2,X3,X0,X1] :
( ~ m2_relset_1(X3,X0,X1)
| k3_subset_1(X1,k10_relset_1(X0,X1,X3,X2)) = k8_relset_2(X0,X1,X2,k3_subset_1(k2_zfmisc_1(X0,X1),X3))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19282]) ).
fof(f20400,plain,
m1_subset_1(sK17,k1_zfmisc_1(sK14)),
inference(cnf_transformation,[],[f20021]) ).
fof(f20401,plain,
m2_relset_1(sK18,sK14,sK15),
inference(cnf_transformation,[],[f20021]) ).
fof(f20402,plain,
m2_relset_1(sK19,sK15,sK16),
inference(cnf_transformation,[],[f20021]) ).
fof(f20403,plain,
k8_relset_2(sK15,sK16,k10_relset_1(sK14,sK15,sK18,sK17),sK19) != k8_relset_2(sK14,sK16,sK17,k3_subset_1(k2_zfmisc_1(sK14,sK16),k9_relset_2(sK14,sK15,sK16,sK18,k3_subset_1(k2_zfmisc_1(sK15,sK16),sK19)))),
inference(cnf_transformation,[],[f20021]) ).
fof(f20458,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20032]) ).
fof(f20464,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,[],[f19322]) ).
fof(f20465,plain,
! [X2,X0,X1] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f19323]) ).
fof(f20519,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,[],[f19384]) ).
fof(f20925,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,[],[f19645]) ).
fof(f20926,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m1_subset_1(k10_relset_1(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f19646]) ).
fof(f21266,plain,
! [X0,X1] :
( k3_subset_1(X0,k3_subset_1(X0,X1)) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19841]) ).
fof(f21267,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| m1_subset_1(k3_subset_1(X0,X1),k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19842]) ).
fof(f21292,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k4_xboole_0(X0,X1) = k3_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f19868]) ).
fof(f21729,definition,
sF213 = k10_relset_1(sK14,sK15,sK18,sK17),
introduced(definition,[new_symbols(definition,[sF213])],[function_definition]) ).
fof(f21730,plain,
k10_relset_1(sK14,sK15,sK18,sK17) = sF213,
inference(reorient_equations,[],[f21729]) ).
fof(f21731,definition,
sF214 = k8_relset_2(sK15,sK16,sF213,sK19),
introduced(definition,[new_symbols(definition,[sF214])],[function_definition]) ).
fof(f21732,plain,
k8_relset_2(sK15,sK16,sF213,sK19) = sF214,
inference(reorient_equations,[],[f21731]) ).
fof(f21733,definition,
sF215 = k2_zfmisc_1(sK14,sK16),
introduced(definition,[new_symbols(definition,[sF215])],[function_definition]) ).
fof(f21734,plain,
k2_zfmisc_1(sK14,sK16) = sF215,
inference(reorient_equations,[],[f21733]) ).
fof(f21735,definition,
sF216 = k2_zfmisc_1(sK15,sK16),
introduced(definition,[new_symbols(definition,[sF216])],[function_definition]) ).
fof(f21736,plain,
k2_zfmisc_1(sK15,sK16) = sF216,
inference(reorient_equations,[],[f21735]) ).
fof(f21737,definition,
sF217 = k3_subset_1(sF216,sK19),
introduced(definition,[new_symbols(definition,[sF217])],[function_definition]) ).
fof(f21738,plain,
k3_subset_1(sF216,sK19) = sF217,
inference(reorient_equations,[],[f21737]) ).
fof(f21739,definition,
sF218 = k9_relset_2(sK14,sK15,sK16,sK18,sF217),
introduced(definition,[new_symbols(definition,[sF218])],[function_definition]) ).
fof(f21740,plain,
k9_relset_2(sK14,sK15,sK16,sK18,sF217) = sF218,
inference(reorient_equations,[],[f21739]) ).
fof(f21741,definition,
sF219 = k3_subset_1(sF215,sF218),
introduced(definition,[new_symbols(definition,[sF219])],[function_definition]) ).
fof(f21742,plain,
k3_subset_1(sF215,sF218) = sF219,
inference(reorient_equations,[],[f21741]) ).
fof(f21743,definition,
sF220 = k8_relset_2(sK14,sK16,sK17,sF219),
introduced(definition,[new_symbols(definition,[sF220])],[function_definition]) ).
fof(f21744,plain,
k8_relset_2(sK14,sK16,sK17,sF219) = sF220,
inference(reorient_equations,[],[f21743]) ).
fof(f21745,plain,
sF214 != sF220,
inference(definition_folding,[],[f20403,f21744,f21742,f21740,f21738,f21736,f21734,f21732,f21730]) ).
fof(f21746,definition,
sF221 = k1_zfmisc_1(sK14),
introduced(definition,[new_symbols(definition,[sF221])],[function_definition]) ).
fof(f21747,plain,
k1_zfmisc_1(sK14) = sF221,
inference(reorient_equations,[],[f21746]) ).
fof(f21748,plain,
m1_subset_1(sK17,sF221),
inference(definition_folding,[],[f20400,f21747]) ).
fof(f21910,definition,
( spl222_25
<=> m1_subset_1(sK17,sF221) ),
introduced(definition,[new_symbols(definition,[spl222_25])],[avatar_definition]) ).
fof(f21912,plain,
( m1_subset_1(sK17,sF221)
| ~ spl222_25 ),
inference(avatar_component_clause,[],[f21910]) ).
fof(f21913,plain,
spl222_25,
inference(avatar_split_clause,[],[f21748,f21910]) ).
fof(f21915,definition,
( spl222_26
<=> m2_relset_1(sK18,sK14,sK15) ),
introduced(definition,[new_symbols(definition,[spl222_26])],[avatar_definition]) ).
fof(f21917,plain,
( m2_relset_1(sK18,sK14,sK15)
| ~ spl222_26 ),
inference(avatar_component_clause,[],[f21915]) ).
fof(f21918,plain,
spl222_26,
inference(avatar_split_clause,[],[f20401,f21915]) ).
fof(f21920,definition,
( spl222_27
<=> m2_relset_1(sK19,sK15,sK16) ),
introduced(definition,[new_symbols(definition,[spl222_27])],[avatar_definition]) ).
fof(f21922,plain,
( m2_relset_1(sK19,sK15,sK16)
| ~ spl222_27 ),
inference(avatar_component_clause,[],[f21920]) ).
fof(f21923,plain,
spl222_27,
inference(avatar_split_clause,[],[f20402,f21920]) ).
fof(f21925,definition,
( spl222_28
<=> sF214 = sF220 ),
introduced(definition,[new_symbols(definition,[spl222_28])],[avatar_definition]) ).
fof(f21928,plain,
~ spl222_28,
inference(avatar_split_clause,[],[f21745,f21925]) ).
fof(f21939,definition,
( spl222_30
<=> k10_relset_1(sK14,sK15,sK18,sK17) = sF213 ),
introduced(definition,[new_symbols(definition,[spl222_30])],[avatar_definition]) ).
fof(f21941,plain,
( k10_relset_1(sK14,sK15,sK18,sK17) = sF213
| ~ spl222_30 ),
inference(avatar_component_clause,[],[f21939]) ).
fof(f21942,plain,
spl222_30,
inference(avatar_split_clause,[],[f21730,f21939]) ).
fof(f21944,definition,
( spl222_31
<=> k8_relset_2(sK15,sK16,sF213,sK19) = sF214 ),
introduced(definition,[new_symbols(definition,[spl222_31])],[avatar_definition]) ).
fof(f21946,plain,
( k8_relset_2(sK15,sK16,sF213,sK19) = sF214
| ~ spl222_31 ),
inference(avatar_component_clause,[],[f21944]) ).
fof(f21947,plain,
spl222_31,
inference(avatar_split_clause,[],[f21732,f21944]) ).
fof(f21949,definition,
( spl222_32
<=> k2_zfmisc_1(sK14,sK16) = sF215 ),
introduced(definition,[new_symbols(definition,[spl222_32])],[avatar_definition]) ).
fof(f21951,plain,
( k2_zfmisc_1(sK14,sK16) = sF215
| ~ spl222_32 ),
inference(avatar_component_clause,[],[f21949]) ).
fof(f21952,plain,
spl222_32,
inference(avatar_split_clause,[],[f21734,f21949]) ).
fof(f21954,definition,
( spl222_33
<=> k2_zfmisc_1(sK15,sK16) = sF216 ),
introduced(definition,[new_symbols(definition,[spl222_33])],[avatar_definition]) ).
fof(f21956,plain,
( k2_zfmisc_1(sK15,sK16) = sF216
| ~ spl222_33 ),
inference(avatar_component_clause,[],[f21954]) ).
fof(f21957,plain,
spl222_33,
inference(avatar_split_clause,[],[f21736,f21954]) ).
fof(f21959,definition,
( spl222_34
<=> k3_subset_1(sF216,sK19) = sF217 ),
introduced(definition,[new_symbols(definition,[spl222_34])],[avatar_definition]) ).
fof(f21961,plain,
( k3_subset_1(sF216,sK19) = sF217
| ~ spl222_34 ),
inference(avatar_component_clause,[],[f21959]) ).
fof(f21962,plain,
spl222_34,
inference(avatar_split_clause,[],[f21738,f21959]) ).
fof(f21964,definition,
( spl222_35
<=> k9_relset_2(sK14,sK15,sK16,sK18,sF217) = sF218 ),
introduced(definition,[new_symbols(definition,[spl222_35])],[avatar_definition]) ).
fof(f21966,plain,
( k9_relset_2(sK14,sK15,sK16,sK18,sF217) = sF218
| ~ spl222_35 ),
inference(avatar_component_clause,[],[f21964]) ).
fof(f21967,plain,
spl222_35,
inference(avatar_split_clause,[],[f21740,f21964]) ).
fof(f21969,definition,
( spl222_36
<=> k3_subset_1(sF215,sF218) = sF219 ),
introduced(definition,[new_symbols(definition,[spl222_36])],[avatar_definition]) ).
fof(f21971,plain,
( k3_subset_1(sF215,sF218) = sF219
| ~ spl222_36 ),
inference(avatar_component_clause,[],[f21969]) ).
fof(f21972,plain,
spl222_36,
inference(avatar_split_clause,[],[f21742,f21969]) ).
fof(f21974,definition,
( spl222_37
<=> k8_relset_2(sK14,sK16,sK17,sF219) = sF220 ),
introduced(definition,[new_symbols(definition,[spl222_37])],[avatar_definition]) ).
fof(f21976,plain,
( k8_relset_2(sK14,sK16,sK17,sF219) = sF220
| ~ spl222_37 ),
inference(avatar_component_clause,[],[f21974]) ).
fof(f21977,plain,
spl222_37,
inference(avatar_split_clause,[],[f21744,f21974]) ).
fof(f21979,definition,
( spl222_38
<=> k1_zfmisc_1(sK14) = sF221 ),
introduced(definition,[new_symbols(definition,[spl222_38])],[avatar_definition]) ).
fof(f21981,plain,
( k1_zfmisc_1(sK14) = sF221
| ~ spl222_38 ),
inference(avatar_component_clause,[],[f21979]) ).
fof(f21982,plain,
spl222_38,
inference(avatar_split_clause,[],[f21747,f21979]) ).
fof(f22003,plain,
( m1_subset_1(sK19,k1_zfmisc_1(k2_zfmisc_1(sK15,sK16)))
| ~ spl222_27 ),
inference(unit_resulting_resolution,[],[f20464,f21922]) ).
fof(f22004,plain,
( m1_subset_1(sK18,k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| ~ spl222_26 ),
inference(unit_resulting_resolution,[],[f20464,f21917]) ).
fof(f22007,plain,
( m1_subset_1(sK19,k1_zfmisc_1(sF216))
| ~ spl222_27
| ~ spl222_33 ),
inference(forward_demodulation,[],[f22003,f21956]) ).
fof(f22009,definition,
( spl222_39
<=> m1_subset_1(sK18,k1_zfmisc_1(k2_zfmisc_1(sK14,sK15))) ),
introduced(definition,[new_symbols(definition,[spl222_39])],[avatar_definition]) ).
fof(f22011,plain,
( m1_subset_1(sK18,k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| ~ spl222_39 ),
inference(avatar_component_clause,[],[f22009]) ).
fof(f22012,plain,
( spl222_39
| ~ spl222_26 ),
inference(avatar_split_clause,[],[f22004,f21915,f22009]) ).
fof(f22014,definition,
( spl222_40
<=> m1_subset_1(sK19,k1_zfmisc_1(sF216)) ),
introduced(definition,[new_symbols(definition,[spl222_40])],[avatar_definition]) ).
fof(f22016,plain,
( m1_subset_1(sK19,k1_zfmisc_1(sF216))
| ~ spl222_40 ),
inference(avatar_component_clause,[],[f22014]) ).
fof(f22017,plain,
( spl222_40
| ~ spl222_27
| ~ spl222_33 ),
inference(avatar_split_clause,[],[f22007,f21954,f21920,f22014]) ).
fof(f22018,plain,
( m1_subset_1(sF214,k1_zfmisc_1(sK16))
| ~ m1_subset_1(sF213,k1_zfmisc_1(sK15))
| ~ m1_subset_1(sK19,k1_zfmisc_1(k2_zfmisc_1(sK15,sK16)))
| ~ spl222_31 ),
inference(superposition,[],[f20303,f21946]) ).
fof(f22021,plain,
( ~ m1_subset_1(sK19,k1_zfmisc_1(sF216))
| m1_subset_1(sF214,k1_zfmisc_1(sK16))
| ~ m1_subset_1(sF213,k1_zfmisc_1(sK15))
| ~ spl222_31
| ~ spl222_33 ),
inference(forward_demodulation,[],[f22018,f21956]) ).
fof(f22023,plain,
( m1_subset_1(sF214,k1_zfmisc_1(sK16))
| ~ m1_subset_1(sF213,k1_zfmisc_1(sK15))
| ~ spl222_31
| ~ spl222_33
| ~ spl222_40 ),
inference(forward_subsumption_resolution,[],[f22021,f22016]) ).
fof(f22026,definition,
( spl222_41
<=> m1_subset_1(sF213,k1_zfmisc_1(sK15)) ),
introduced(definition,[new_symbols(definition,[spl222_41])],[avatar_definition]) ).
fof(f22027,plain,
( m1_subset_1(sF213,k1_zfmisc_1(sK15))
| ~ spl222_41 ),
inference(avatar_component_clause,[],[f22026]) ).
fof(f22030,definition,
( spl222_42
<=> m1_subset_1(sF214,k1_zfmisc_1(sK16)) ),
introduced(definition,[new_symbols(definition,[spl222_42])],[avatar_definition]) ).
fof(f22032,plain,
( m1_subset_1(sF214,k1_zfmisc_1(sK16))
| ~ spl222_42 ),
inference(avatar_component_clause,[],[f22030]) ).
fof(f22033,plain,
( ~ spl222_41
| spl222_42
| ~ spl222_31
| ~ spl222_33
| ~ spl222_40 ),
inference(avatar_split_clause,[],[f22023,f22014,f21954,f21944,f22030,f22026]) ).
fof(f22039,definition,
( spl222_44
<=> m1_subset_1(sF219,k1_zfmisc_1(sF215)) ),
introduced(definition,[new_symbols(definition,[spl222_44])],[avatar_definition]) ).
fof(f22040,plain,
( m1_subset_1(sF219,k1_zfmisc_1(sF215))
| ~ spl222_44 ),
inference(avatar_component_clause,[],[f22039]) ).
fof(f22041,plain,
( ~ m1_subset_1(sF219,k1_zfmisc_1(sF215))
| spl222_44 ),
inference(avatar_component_clause,[],[f22039]) ).
fof(f22045,plain,
( sF218 = k5_relat_1(sK18,sF217)
| ~ m1_subset_1(sK18,k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| ~ m1_subset_1(sF217,k1_zfmisc_1(k2_zfmisc_1(sK15,sK16)))
| ~ spl222_35 ),
inference(superposition,[],[f21966,f20306]) ).
fof(f22046,plain,
( m2_relset_1(sF218,sK14,sK16)
| ~ m1_subset_1(sK18,k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| ~ m1_subset_1(sF217,k1_zfmisc_1(k2_zfmisc_1(sK15,sK16)))
| ~ spl222_35 ),
inference(superposition,[],[f20305,f21966]) ).
fof(f22049,plain,
( m2_relset_1(sF218,sK14,sK16)
| ~ m1_subset_1(sF217,k1_zfmisc_1(k2_zfmisc_1(sK15,sK16)))
| ~ spl222_35
| ~ spl222_39 ),
inference(forward_subsumption_resolution,[],[f22046,f22011]) ).
fof(f22050,plain,
( sF218 = k5_relat_1(sK18,sF217)
| ~ m1_subset_1(sF217,k1_zfmisc_1(k2_zfmisc_1(sK15,sK16)))
| ~ spl222_35
| ~ spl222_39 ),
inference(forward_subsumption_resolution,[],[f22045,f22011]) ).
fof(f22052,plain,
( ~ m1_subset_1(sF217,k1_zfmisc_1(sF216))
| m2_relset_1(sF218,sK14,sK16)
| ~ spl222_33
| ~ spl222_35
| ~ spl222_39 ),
inference(forward_demodulation,[],[f22049,f21956]) ).
fof(f22053,plain,
( ~ m1_subset_1(sF217,k1_zfmisc_1(sF216))
| sF218 = k5_relat_1(sK18,sF217)
| ~ spl222_33
| ~ spl222_35
| ~ spl222_39 ),
inference(forward_demodulation,[],[f22050,f21956]) ).
fof(f22055,definition,
( spl222_45
<=> sF218 = k5_relat_1(sK18,sF217) ),
introduced(definition,[new_symbols(definition,[spl222_45])],[avatar_definition]) ).
fof(f22057,plain,
( sF218 = k5_relat_1(sK18,sF217)
| ~ spl222_45 ),
inference(avatar_component_clause,[],[f22055]) ).
fof(f22059,definition,
( spl222_46
<=> m1_subset_1(sF217,k1_zfmisc_1(sF216)) ),
introduced(definition,[new_symbols(definition,[spl222_46])],[avatar_definition]) ).
fof(f22060,plain,
( m1_subset_1(sF217,k1_zfmisc_1(sF216))
| ~ spl222_46 ),
inference(avatar_component_clause,[],[f22059]) ).
fof(f22061,plain,
( ~ m1_subset_1(sF217,k1_zfmisc_1(sF216))
| spl222_46 ),
inference(avatar_component_clause,[],[f22059]) ).
fof(f22064,definition,
( spl222_47
<=> m2_relset_1(sF218,sK14,sK16) ),
introduced(definition,[new_symbols(definition,[spl222_47])],[avatar_definition]) ).
fof(f22066,plain,
( m2_relset_1(sF218,sK14,sK16)
| ~ spl222_47 ),
inference(avatar_component_clause,[],[f22064]) ).
fof(f22067,plain,
( spl222_47
| ~ spl222_46
| ~ spl222_33
| ~ spl222_35
| ~ spl222_39 ),
inference(avatar_split_clause,[],[f22052,f22009,f21964,f21954,f22059,f22064]) ).
fof(f22068,plain,
( spl222_45
| ~ spl222_46
| ~ spl222_33
| ~ spl222_35
| ~ spl222_39 ),
inference(avatar_split_clause,[],[f22053,f22009,f21964,f21954,f22059,f22055]) ).
fof(f22072,plain,
( sF218 = k3_subset_1(sF215,sF219)
| ~ m1_subset_1(sF218,k1_zfmisc_1(sF215))
| ~ spl222_36 ),
inference(superposition,[],[f21266,f21971]) ).
fof(f22074,definition,
( spl222_48
<=> m1_subset_1(sF218,k1_zfmisc_1(sF215)) ),
introduced(definition,[new_symbols(definition,[spl222_48])],[avatar_definition]) ).
fof(f22075,plain,
( m1_subset_1(sF218,k1_zfmisc_1(sF215))
| ~ spl222_48 ),
inference(avatar_component_clause,[],[f22074]) ).
fof(f22076,plain,
( ~ m1_subset_1(sF218,k1_zfmisc_1(sF215))
| spl222_48 ),
inference(avatar_component_clause,[],[f22074]) ).
fof(f22078,definition,
( spl222_49
<=> sF218 = k3_subset_1(sF215,sF219) ),
introduced(definition,[new_symbols(definition,[spl222_49])],[avatar_definition]) ).
fof(f22080,plain,
( sF218 = k3_subset_1(sF215,sF219)
| ~ spl222_49 ),
inference(avatar_component_clause,[],[f22078]) ).
fof(f22081,plain,
( ~ spl222_48
| spl222_49
| ~ spl222_36 ),
inference(avatar_split_clause,[],[f22072,f21969,f22078,f22074]) ).
fof(f22090,plain,
( ! [X0] :
( k3_subset_1(sK15,k10_relset_1(sK14,sK15,sK18,X0)) = k8_relset_2(sK14,sK15,X0,k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK14)) )
| ~ spl222_26 ),
inference(resolution,[],[f20385,f21917]) ).
fof(f22092,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF221)
| k3_subset_1(sK15,k10_relset_1(sK14,sK15,sK18,X0)) = k8_relset_2(sK14,sK15,X0,k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18)) )
| ~ spl222_26
| ~ spl222_38 ),
inference(forward_demodulation,[],[f22090,f21981]) ).
fof(f22097,plain,
( k3_subset_1(sK15,k10_relset_1(sK14,sK15,sK18,sK17)) = k8_relset_2(sK14,sK15,sK17,k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18))
| ~ spl222_25
| ~ spl222_26
| ~ spl222_38 ),
inference(resolution,[],[f22092,f21912]) ).
fof(f22098,plain,
( k8_relset_2(sK14,sK15,sK17,k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18)) = k3_subset_1(sK15,sF213)
| ~ spl222_25
| ~ spl222_26
| ~ spl222_30
| ~ spl222_38 ),
inference(forward_demodulation,[],[f22097,f21941]) ).
fof(f22101,definition,
( spl222_51
<=> k8_relset_2(sK14,sK15,sK17,k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18)) = k3_subset_1(sK15,sF213) ),
introduced(definition,[new_symbols(definition,[spl222_51])],[avatar_definition]) ).
fof(f22103,plain,
( k8_relset_2(sK14,sK15,sK17,k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18)) = k3_subset_1(sK15,sF213)
| ~ spl222_51 ),
inference(avatar_component_clause,[],[f22101]) ).
fof(f22104,plain,
( spl222_51
| ~ spl222_25
| ~ spl222_26
| ~ spl222_30
| ~ spl222_38 ),
inference(avatar_split_clause,[],[f22098,f21979,f21939,f21915,f21910,f22101]) ).
fof(f22105,plain,
( m1_subset_1(k3_subset_1(sK15,sF213),k1_zfmisc_1(sK15))
| ~ m1_subset_1(sK17,k1_zfmisc_1(sK14))
| ~ m1_subset_1(k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| ~ spl222_51 ),
inference(superposition,[],[f20303,f22103]) ).
fof(f22106,plain,
( ~ m1_subset_1(sK17,sF221)
| m1_subset_1(k3_subset_1(sK15,sF213),k1_zfmisc_1(sK15))
| ~ m1_subset_1(k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| ~ spl222_38
| ~ spl222_51 ),
inference(forward_demodulation,[],[f22105,f21981]) ).
fof(f22107,plain,
( m1_subset_1(k3_subset_1(sK15,sF213),k1_zfmisc_1(sK15))
| ~ m1_subset_1(k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| ~ spl222_25
| ~ spl222_38
| ~ spl222_51 ),
inference(forward_subsumption_resolution,[],[f22106,f21912]) ).
fof(f22109,definition,
( spl222_52
<=> m1_subset_1(k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15))) ),
introduced(definition,[new_symbols(definition,[spl222_52])],[avatar_definition]) ).
fof(f22111,plain,
( ~ m1_subset_1(k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| spl222_52 ),
inference(avatar_component_clause,[],[f22109]) ).
fof(f22113,definition,
( spl222_53
<=> m1_subset_1(k3_subset_1(sK15,sF213),k1_zfmisc_1(sK15)) ),
introduced(definition,[new_symbols(definition,[spl222_53])],[avatar_definition]) ).
fof(f22115,plain,
( m1_subset_1(k3_subset_1(sK15,sF213),k1_zfmisc_1(sK15))
| ~ spl222_53 ),
inference(avatar_component_clause,[],[f22113]) ).
fof(f22116,plain,
( ~ spl222_52
| spl222_53
| ~ spl222_25
| ~ spl222_38
| ~ spl222_51 ),
inference(avatar_split_clause,[],[f22107,f22101,f21979,f21910,f22113,f22109]) ).
fof(f22144,plain,
( sK18 = k3_subset_1(k2_zfmisc_1(sK14,sK15),k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18))
| ~ spl222_39 ),
inference(unit_resulting_resolution,[],[f21266,f22011]) ).
fof(f22146,definition,
( spl222_58
<=> sK18 = k3_subset_1(k2_zfmisc_1(sK14,sK15),k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18)) ),
introduced(definition,[new_symbols(definition,[spl222_58])],[avatar_definition]) ).
fof(f22148,plain,
( sK18 = k3_subset_1(k2_zfmisc_1(sK14,sK15),k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18))
| ~ spl222_58 ),
inference(avatar_component_clause,[],[f22146]) ).
fof(f22149,plain,
( spl222_58
| ~ spl222_39 ),
inference(avatar_split_clause,[],[f22144,f22009,f22146]) ).
fof(f22150,plain,
( v1_relat_1(sK18)
| ~ spl222_39 ),
inference(unit_resulting_resolution,[],[f20465,f22011]) ).
fof(f22152,definition,
( spl222_59
<=> v1_relat_1(sK18) ),
introduced(definition,[new_symbols(definition,[spl222_59])],[avatar_definition]) ).
fof(f22154,plain,
( v1_relat_1(sK18)
| ~ spl222_59 ),
inference(avatar_component_clause,[],[f22152]) ).
fof(f22155,plain,
( spl222_59
| ~ spl222_39 ),
inference(avatar_split_clause,[],[f22150,f22009,f22152]) ).
fof(f22156,plain,
( k9_relat_1(k3_subset_1(k2_zfmisc_1(sK15,sK16),sK19),sF213) = k3_subset_1(sK16,sF214)
| ~ m1_subset_1(sK19,k1_zfmisc_1(k2_zfmisc_1(sK15,sK16)))
| ~ m1_subset_1(sF213,k1_zfmisc_1(sK15))
| ~ spl222_31 ),
inference(superposition,[],[f20384,f21946]) ).
fof(f22157,plain,
( k9_relat_1(k3_subset_1(k2_zfmisc_1(sK14,sK16),sF219),sK17) = k3_subset_1(sK16,sF220)
| ~ m1_subset_1(sF219,k1_zfmisc_1(k2_zfmisc_1(sK14,sK16)))
| ~ m1_subset_1(sK17,k1_zfmisc_1(sK14))
| ~ spl222_37 ),
inference(superposition,[],[f20384,f21976]) ).
fof(f22158,plain,
( k9_relat_1(k3_subset_1(k2_zfmisc_1(sK14,sK15),k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18)),sK17) = k3_subset_1(sK15,k3_subset_1(sK15,sF213))
| ~ m1_subset_1(k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| ~ m1_subset_1(sK17,k1_zfmisc_1(sK14))
| ~ spl222_51 ),
inference(superposition,[],[f20384,f22103]) ).
fof(f22161,plain,
( k3_subset_1(sK16,sF220) = k9_relat_1(k3_subset_1(sF215,sF219),sK17)
| ~ m1_subset_1(sF219,k1_zfmisc_1(k2_zfmisc_1(sK14,sK16)))
| ~ m1_subset_1(sK17,k1_zfmisc_1(sK14))
| ~ spl222_32
| ~ spl222_37 ),
inference(forward_demodulation,[],[f22157,f21951]) ).
fof(f22162,plain,
( ~ m1_subset_1(sF219,k1_zfmisc_1(sF215))
| k3_subset_1(sK16,sF220) = k9_relat_1(k3_subset_1(sF215,sF219),sK17)
| ~ m1_subset_1(sK17,k1_zfmisc_1(sK14))
| ~ spl222_32
| ~ spl222_37 ),
inference(forward_demodulation,[],[f22161,f21951]) ).
fof(f22199,plain,
( k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18) = k4_xboole_0(k2_zfmisc_1(sK14,sK15),sK18)
| ~ spl222_39 ),
inference(resolution,[],[f21292,f22011]) ).
fof(f22204,definition,
( spl222_65
<=> k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18) = k4_xboole_0(k2_zfmisc_1(sK14,sK15),sK18) ),
introduced(definition,[new_symbols(definition,[spl222_65])],[avatar_definition]) ).
fof(f22206,plain,
( k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18) = k4_xboole_0(k2_zfmisc_1(sK14,sK15),sK18)
| ~ spl222_65 ),
inference(avatar_component_clause,[],[f22204]) ).
fof(f22207,plain,
( spl222_65
| ~ spl222_39 ),
inference(avatar_split_clause,[],[f22199,f22009,f22204]) ).
fof(f22214,plain,
( m1_subset_1(k3_subset_1(sF216,sK19),k1_zfmisc_1(sF216))
| ~ spl222_40 ),
inference(unit_resulting_resolution,[],[f21267,f22016]) ).
fof(f22215,plain,
( m1_subset_1(k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| ~ spl222_39 ),
inference(unit_resulting_resolution,[],[f21267,f22011]) ).
fof(f22219,plain,
( m1_subset_1(k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| ~ spl222_39 ),
inference(resolution,[],[f21267,f22011]) ).
fof(f22225,plain,
( m1_subset_1(sF217,k1_zfmisc_1(sF216))
| ~ spl222_34
| ~ spl222_40 ),
inference(forward_demodulation,[],[f22214,f21961]) ).
fof(f22226,plain,
( $false
| ~ spl222_39
| spl222_52 ),
inference(forward_subsumption_resolution,[],[f22215,f22111]) ).
fof(f22227,plain,
( ~ spl222_39
| spl222_52 ),
inference(avatar_contradiction_clause,[],[f22226]) ).
fof(f22230,plain,
( $false
| ~ spl222_34
| ~ spl222_40
| spl222_46 ),
inference(forward_subsumption_resolution,[],[f22225,f22061]) ).
fof(f22231,plain,
( ~ spl222_34
| ~ spl222_40
| spl222_46 ),
inference(avatar_contradiction_clause,[],[f22230]) ).
fof(f22233,plain,
( k3_subset_1(sK15,k3_subset_1(sK15,sF213)) = k9_relat_1(sK18,sK17)
| ~ m1_subset_1(k3_subset_1(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| ~ m1_subset_1(sK17,k1_zfmisc_1(sK14))
| ~ spl222_51
| ~ spl222_58 ),
inference(forward_demodulation,[],[f22158,f22148]) ).
fof(f22234,plain,
( m1_subset_1(k4_xboole_0(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| ~ spl222_39
| ~ spl222_65 ),
inference(forward_demodulation,[],[f22219,f22206]) ).
fof(f22237,definition,
( spl222_67
<=> m1_subset_1(k4_xboole_0(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15))) ),
introduced(definition,[new_symbols(definition,[spl222_67])],[avatar_definition]) ).
fof(f22241,plain,
( ~ m1_subset_1(k4_xboole_0(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| k3_subset_1(sK15,k3_subset_1(sK15,sF213)) = k9_relat_1(sK18,sK17)
| ~ m1_subset_1(sK17,k1_zfmisc_1(sK14))
| ~ spl222_51
| ~ spl222_58
| ~ spl222_65 ),
inference(forward_demodulation,[],[f22233,f22206]) ).
fof(f22242,plain,
( spl222_67
| ~ spl222_39
| ~ spl222_65 ),
inference(avatar_split_clause,[],[f22234,f22204,f22009,f22237]) ).
fof(f22243,plain,
( ~ m1_subset_1(sK17,sF221)
| ~ m1_subset_1(k4_xboole_0(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| k3_subset_1(sK15,k3_subset_1(sK15,sF213)) = k9_relat_1(sK18,sK17)
| ~ spl222_38
| ~ spl222_51
| ~ spl222_58
| ~ spl222_65 ),
inference(forward_demodulation,[],[f22241,f21981]) ).
fof(f22244,plain,
( ~ m1_subset_1(k4_xboole_0(k2_zfmisc_1(sK14,sK15),sK18),k1_zfmisc_1(k2_zfmisc_1(sK14,sK15)))
| k3_subset_1(sK15,k3_subset_1(sK15,sF213)) = k9_relat_1(sK18,sK17)
| ~ spl222_25
| ~ spl222_38
| ~ spl222_51
| ~ spl222_58
| ~ spl222_65 ),
inference(forward_subsumption_resolution,[],[f22243,f21912]) ).
fof(f22246,definition,
( spl222_68
<=> k3_subset_1(sK15,k3_subset_1(sK15,sF213)) = k9_relat_1(sK18,sK17) ),
introduced(definition,[new_symbols(definition,[spl222_68])],[avatar_definition]) ).
fof(f22248,plain,
( k3_subset_1(sK15,k3_subset_1(sK15,sF213)) = k9_relat_1(sK18,sK17)
| ~ spl222_68 ),
inference(avatar_component_clause,[],[f22246]) ).
fof(f22249,plain,
( spl222_68
| ~ spl222_67
| ~ spl222_25
| ~ spl222_38
| ~ spl222_51
| ~ spl222_58
| ~ spl222_65 ),
inference(avatar_split_clause,[],[f22244,f22204,f22146,f22101,f21979,f21910,f22237,f22246]) ).
fof(f22267,plain,
( m1_subset_1(sF218,k1_zfmisc_1(k2_zfmisc_1(sK14,sK16)))
| ~ spl222_47 ),
inference(unit_resulting_resolution,[],[f20464,f22066]) ).
fof(f22269,plain,
( ! [X0] :
( k3_subset_1(sK16,k10_relset_1(sK14,sK16,sF218,X0)) = k8_relset_2(sK14,sK16,X0,k3_subset_1(k2_zfmisc_1(sK14,sK16),sF218))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK14)) )
| ~ spl222_47 ),
inference(resolution,[],[f22066,f20385]) ).
fof(f22270,plain,
( ! [X0] :
( k3_subset_1(sK16,k10_relset_1(sK14,sK16,sF218,X0)) = k8_relset_2(sK14,sK16,X0,k3_subset_1(sF215,sF218))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK14)) )
| ~ spl222_32
| ~ spl222_47 ),
inference(forward_demodulation,[],[f22269,f21951]) ).
fof(f22280,plain,
( m1_subset_1(sF218,k1_zfmisc_1(sF215))
| ~ spl222_32
| ~ spl222_47 ),
inference(forward_demodulation,[],[f22267,f21951]) ).
fof(f22281,plain,
( ! [X0] :
( k3_subset_1(sK16,k10_relset_1(sK14,sK16,sF218,X0)) = k8_relset_2(sK14,sK16,X0,sF219)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK14)) )
| ~ spl222_32
| ~ spl222_36
| ~ spl222_47 ),
inference(forward_demodulation,[],[f22270,f21971]) ).
fof(f22282,plain,
( $false
| ~ spl222_32
| ~ spl222_47
| spl222_48 ),
inference(forward_subsumption_resolution,[],[f22280,f22076]) ).
fof(f22283,plain,
( ~ spl222_32
| ~ spl222_47
| spl222_48 ),
inference(avatar_contradiction_clause,[],[f22282]) ).
fof(f22284,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF221)
| k3_subset_1(sK16,k10_relset_1(sK14,sK16,sF218,X0)) = k8_relset_2(sK14,sK16,X0,sF219) )
| ~ spl222_32
| ~ spl222_36
| ~ spl222_38
| ~ spl222_47 ),
inference(forward_demodulation,[],[f22281,f21981]) ).
fof(f22286,plain,
( k8_relset_2(sK14,sK16,sK17,sF219) = k3_subset_1(sK16,k10_relset_1(sK14,sK16,sF218,sK17))
| ~ spl222_25
| ~ spl222_32
| ~ spl222_36
| ~ spl222_38
| ~ spl222_47 ),
inference(resolution,[],[f22284,f21912]) ).
fof(f22287,plain,
( sF220 = k3_subset_1(sK16,k10_relset_1(sK14,sK16,sF218,sK17))
| ~ spl222_25
| ~ spl222_32
| ~ spl222_36
| ~ spl222_37
| ~ spl222_38
| ~ spl222_47 ),
inference(forward_demodulation,[],[f22286,f21976]) ).
fof(f22290,definition,
( spl222_71
<=> sF220 = k3_subset_1(sK16,k10_relset_1(sK14,sK16,sF218,sK17)) ),
introduced(definition,[new_symbols(definition,[spl222_71])],[avatar_definition]) ).
fof(f22292,plain,
( sF220 = k3_subset_1(sK16,k10_relset_1(sK14,sK16,sF218,sK17))
| ~ spl222_71 ),
inference(avatar_component_clause,[],[f22290]) ).
fof(f22293,plain,
( spl222_71
| ~ spl222_25
| ~ spl222_32
| ~ spl222_36
| ~ spl222_37
| ~ spl222_38
| ~ spl222_47 ),
inference(avatar_split_clause,[],[f22287,f22064,f21979,f21974,f21969,f21949,f21910,f22290]) ).
fof(f22294,plain,
( k3_subset_1(sK16,sF220) = k10_relset_1(sK14,sK16,sF218,sK17)
| ~ m1_subset_1(k10_relset_1(sK14,sK16,sF218,sK17),k1_zfmisc_1(sK16))
| ~ spl222_71 ),
inference(superposition,[],[f21266,f22292]) ).
fof(f22296,definition,
( spl222_72
<=> m1_subset_1(k10_relset_1(sK14,sK16,sF218,sK17),k1_zfmisc_1(sK16)) ),
introduced(definition,[new_symbols(definition,[spl222_72])],[avatar_definition]) ).
fof(f22298,plain,
( ~ m1_subset_1(k10_relset_1(sK14,sK16,sF218,sK17),k1_zfmisc_1(sK16))
| spl222_72 ),
inference(avatar_component_clause,[],[f22296]) ).
fof(f22300,definition,
( spl222_73
<=> k3_subset_1(sK16,sF220) = k10_relset_1(sK14,sK16,sF218,sK17) ),
introduced(definition,[new_symbols(definition,[spl222_73])],[avatar_definition]) ).
fof(f22303,plain,
( ~ spl222_72
| spl222_73
| ~ spl222_71 ),
inference(avatar_split_clause,[],[f22294,f22290,f22300,f22296]) ).
fof(f22304,plain,
( ~ m1_relset_1(sF218,sK14,sK16)
| spl222_72 ),
inference(unit_resulting_resolution,[],[f20926,f22298]) ).
fof(f22306,definition,
( spl222_74
<=> m1_relset_1(sF218,sK14,sK16) ),
introduced(definition,[new_symbols(definition,[spl222_74])],[avatar_definition]) ).
fof(f22308,plain,
( ~ m1_relset_1(sF218,sK14,sK16)
| spl222_74 ),
inference(avatar_component_clause,[],[f22306]) ).
fof(f22309,plain,
( ~ spl222_74
| spl222_72 ),
inference(avatar_split_clause,[],[f22304,f22296,f22306]) ).
fof(f22348,plain,
( m1_subset_1(k3_subset_1(sK15,k3_subset_1(sK15,sF213)),k1_zfmisc_1(sK15))
| ~ spl222_53 ),
inference(resolution,[],[f22115,f21267]) ).
fof(f22351,plain,
( m1_subset_1(k9_relat_1(sK18,sK17),k1_zfmisc_1(sK15))
| ~ spl222_53
| ~ spl222_68 ),
inference(forward_demodulation,[],[f22348,f22248]) ).
fof(f22367,definition,
( spl222_81
<=> m1_subset_1(k9_relat_1(sK18,sK17),k1_zfmisc_1(sK15)) ),
introduced(definition,[new_symbols(definition,[spl222_81])],[avatar_definition]) ).
fof(f22370,plain,
( spl222_81
| ~ spl222_53
| ~ spl222_68 ),
inference(avatar_split_clause,[],[f22351,f22246,f22113,f22367]) ).
fof(f22411,plain,
( m1_subset_1(k3_subset_1(sF215,sF218),k1_zfmisc_1(sF215))
| ~ spl222_48 ),
inference(unit_resulting_resolution,[],[f21267,f22075]) ).
fof(f22418,plain,
( m1_subset_1(sF219,k1_zfmisc_1(sF215))
| ~ spl222_36
| ~ spl222_48 ),
inference(forward_demodulation,[],[f22411,f21971]) ).
fof(f22427,plain,
( $false
| ~ spl222_36
| spl222_44
| ~ spl222_48 ),
inference(forward_subsumption_resolution,[],[f22418,f22041]) ).
fof(f22428,plain,
( ~ spl222_36
| spl222_44
| ~ spl222_48 ),
inference(avatar_contradiction_clause,[],[f22427]) ).
fof(f22429,plain,
( k3_subset_1(sK16,sF220) = k9_relat_1(k3_subset_1(sF215,sF219),sK17)
| ~ m1_subset_1(sK17,k1_zfmisc_1(sK14))
| ~ spl222_32
| ~ spl222_37
| ~ spl222_44 ),
inference(forward_subsumption_resolution,[],[f22162,f22040]) ).
fof(f22430,plain,
( k3_subset_1(sK16,sF220) = k9_relat_1(sF218,sK17)
| ~ m1_subset_1(sK17,k1_zfmisc_1(sK14))
| ~ spl222_32
| ~ spl222_37
| ~ spl222_44
| ~ spl222_49 ),
inference(forward_demodulation,[],[f22429,f22080]) ).
fof(f22431,plain,
( ~ m1_subset_1(sK17,sF221)
| k3_subset_1(sK16,sF220) = k9_relat_1(sF218,sK17)
| ~ spl222_32
| ~ spl222_37
| ~ spl222_38
| ~ spl222_44
| ~ spl222_49 ),
inference(forward_demodulation,[],[f22430,f21981]) ).
fof(f22432,plain,
( k3_subset_1(sK16,sF220) = k9_relat_1(sF218,sK17)
| ~ spl222_25
| ~ spl222_32
| ~ spl222_37
| ~ spl222_38
| ~ spl222_44
| ~ spl222_49 ),
inference(forward_subsumption_resolution,[],[f22431,f21912]) ).
fof(f22434,definition,
( spl222_89
<=> k3_subset_1(sK16,sF220) = k9_relat_1(sF218,sK17) ),
introduced(definition,[new_symbols(definition,[spl222_89])],[avatar_definition]) ).
fof(f22437,plain,
( spl222_89
| ~ spl222_25
| ~ spl222_32
| ~ spl222_37
| ~ spl222_38
| ~ spl222_44
| ~ spl222_49 ),
inference(avatar_split_clause,[],[f22432,f22078,f22039,f21979,f21974,f21949,f21910,f22434]) ).
fof(f22482,plain,
( m1_relset_1(sK18,sK14,sK15)
| ~ spl222_26 ),
inference(unit_resulting_resolution,[],[f20458,f21917]) ).
fof(f22483,plain,
( m1_relset_1(sF218,sK14,sK16)
| ~ spl222_47 ),
inference(unit_resulting_resolution,[],[f20458,f22066]) ).
fof(f22492,definition,
( spl222_95
<=> m1_relset_1(sK18,sK14,sK15) ),
introduced(definition,[new_symbols(definition,[spl222_95])],[avatar_definition]) ).
fof(f22494,plain,
( m1_relset_1(sK18,sK14,sK15)
| ~ spl222_95 ),
inference(avatar_component_clause,[],[f22492]) ).
fof(f22495,plain,
( spl222_95
| ~ spl222_26 ),
inference(avatar_split_clause,[],[f22482,f21915,f22492]) ).
fof(f22496,plain,
( $false
| ~ spl222_47
| spl222_74 ),
inference(forward_subsumption_resolution,[],[f22483,f22308]) ).
fof(f22497,plain,
( ~ spl222_47
| spl222_74 ),
inference(avatar_contradiction_clause,[],[f22496]) ).
fof(f22506,plain,
( ! [X0] : k10_relset_1(sK14,sK15,sK18,X0) = k9_relat_1(sK18,X0)
| ~ spl222_95 ),
inference(resolution,[],[f22494,f20925]) ).
fof(f22511,plain,
( sF213 = k9_relat_1(sK18,sK17)
| ~ spl222_30
| ~ spl222_95 ),
inference(superposition,[],[f21941,f22506]) ).
fof(f22521,definition,
( spl222_98
<=> sF213 = k9_relat_1(sK18,sK17) ),
introduced(definition,[new_symbols(definition,[spl222_98])],[avatar_definition]) ).
fof(f22523,plain,
( sF213 = k9_relat_1(sK18,sK17)
| ~ spl222_98 ),
inference(avatar_component_clause,[],[f22521]) ).
fof(f22524,plain,
( spl222_98
| ~ spl222_30
| ~ spl222_95 ),
inference(avatar_split_clause,[],[f22511,f22492,f21939,f22521]) ).
fof(f22527,plain,
( sF213 != k9_relat_1(sK18,sK17)
| m1_subset_1(sF213,k1_zfmisc_1(sK15))
| ~ m1_subset_1(k9_relat_1(sK18,sK17),k1_zfmisc_1(sK15)) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f22528,plain,
( k9_relat_1(k3_subset_1(k2_zfmisc_1(sK15,sK16),sK19),sF213) = k3_subset_1(sK16,sF214)
| ~ m1_subset_1(sK19,k1_zfmisc_1(k2_zfmisc_1(sK15,sK16)))
| ~ spl222_31
| ~ spl222_41 ),
inference(forward_subsumption_resolution,[],[f22156,f22027]) ).
fof(f22529,plain,
( k3_subset_1(sK16,sF214) = k9_relat_1(k3_subset_1(sF216,sK19),sF213)
| ~ m1_subset_1(sK19,k1_zfmisc_1(k2_zfmisc_1(sK15,sK16)))
| ~ spl222_31
| ~ spl222_33
| ~ spl222_41 ),
inference(forward_demodulation,[],[f22528,f21956]) ).
fof(f22530,plain,
( k3_subset_1(sK16,sF214) = k9_relat_1(sF217,sF213)
| ~ m1_subset_1(sK19,k1_zfmisc_1(k2_zfmisc_1(sK15,sK16)))
| ~ spl222_31
| ~ spl222_33
| ~ spl222_34
| ~ spl222_41 ),
inference(forward_demodulation,[],[f22529,f21961]) ).
fof(f22531,plain,
( ~ m1_subset_1(sK19,k1_zfmisc_1(sF216))
| k3_subset_1(sK16,sF214) = k9_relat_1(sF217,sF213)
| ~ spl222_31
| ~ spl222_33
| ~ spl222_34
| ~ spl222_41 ),
inference(forward_demodulation,[],[f22530,f21956]) ).
fof(f22532,plain,
( k3_subset_1(sK16,sF214) = k9_relat_1(sF217,sF213)
| ~ spl222_31
| ~ spl222_33
| ~ spl222_34
| ~ spl222_40
| ~ spl222_41 ),
inference(forward_subsumption_resolution,[],[f22531,f22016]) ).
fof(f22534,definition,
( spl222_99
<=> k3_subset_1(sK16,sF214) = k9_relat_1(sF217,sF213) ),
introduced(definition,[new_symbols(definition,[spl222_99])],[avatar_definition]) ).
fof(f22536,plain,
( k3_subset_1(sK16,sF214) = k9_relat_1(sF217,sF213)
| ~ spl222_99 ),
inference(avatar_component_clause,[],[f22534]) ).
fof(f22537,plain,
( spl222_99
| ~ spl222_31
| ~ spl222_33
| ~ spl222_34
| ~ spl222_40
| ~ spl222_41 ),
inference(avatar_split_clause,[],[f22532,f22026,f22014,f21959,f21954,f21944,f22534]) ).
fof(f22538,plain,
( sF214 = k3_subset_1(sK16,k3_subset_1(sK16,sF214))
| ~ spl222_42 ),
inference(unit_resulting_resolution,[],[f21266,f22032]) ).
fof(f22549,plain,
( sF214 = k3_subset_1(sK16,k9_relat_1(sF217,sF213))
| ~ spl222_42
| ~ spl222_99 ),
inference(forward_demodulation,[],[f22538,f22536]) ).
fof(f22557,definition,
( spl222_102
<=> sF214 = k3_subset_1(sK16,k9_relat_1(sF217,sF213)) ),
introduced(definition,[new_symbols(definition,[spl222_102])],[avatar_definition]) ).
fof(f22560,plain,
( spl222_102
| ~ spl222_42
| ~ spl222_99 ),
inference(avatar_split_clause,[],[f22549,f22534,f22030,f22557]) ).
fof(f28962,plain,
( ! [X0] :
( k9_relat_1(sF218,X0) = k9_relat_1(sF217,k9_relat_1(sK18,X0))
| ~ v1_relat_1(sF217)
| ~ v1_relat_1(sK18) )
| ~ spl222_45 ),
inference(superposition,[],[f20519,f22057]) ).
fof(f28964,plain,
( ! [X0] :
( k9_relat_1(sF218,X0) = k9_relat_1(sF217,k9_relat_1(sK18,X0))
| ~ v1_relat_1(sF217) )
| ~ spl222_45
| ~ spl222_59 ),
inference(forward_subsumption_resolution,[],[f28962,f22154]) ).
fof(f28966,definition,
( spl222_614
<=> v1_relat_1(sF217) ),
introduced(definition,[new_symbols(definition,[spl222_614])],[avatar_definition]) ).
fof(f28968,plain,
( ~ v1_relat_1(sF217)
| spl222_614 ),
inference(avatar_component_clause,[],[f28966]) ).
fof(f28970,definition,
( spl222_615
<=> ! [X0] : k9_relat_1(sF218,X0) = k9_relat_1(sF217,k9_relat_1(sK18,X0)) ),
introduced(definition,[new_symbols(definition,[spl222_615])],[avatar_definition]) ).
fof(f28971,plain,
( ! [X0] : k9_relat_1(sF218,X0) = k9_relat_1(sF217,k9_relat_1(sK18,X0))
| ~ spl222_615 ),
inference(avatar_component_clause,[],[f28970]) ).
fof(f28972,plain,
( ~ spl222_614
| spl222_615
| ~ spl222_45
| ~ spl222_59 ),
inference(avatar_split_clause,[],[f28964,f22152,f22055,f28970,f28966]) ).
fof(f28974,plain,
( ! [X0,X1] : ~ m1_subset_1(sF217,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| spl222_614 ),
inference(resolution,[],[f28968,f20465]) ).
fof(f28978,plain,
( ~ m1_subset_1(sF217,k1_zfmisc_1(sF216))
| ~ spl222_33
| spl222_614 ),
inference(superposition,[],[f28974,f21956]) ).
fof(f28985,plain,
( $false
| ~ spl222_33
| ~ spl222_46
| spl222_614 ),
inference(forward_subsumption_resolution,[],[f28978,f22060]) ).
fof(f28986,plain,
( ~ spl222_33
| ~ spl222_46
| spl222_614 ),
inference(avatar_contradiction_clause,[],[f28985]) ).
fof(f29252,plain,
( k9_relat_1(sF218,sK17) = k9_relat_1(sF217,sF213)
| ~ spl222_98
| ~ spl222_615 ),
inference(superposition,[],[f28971,f22523]) ).
fof(f29293,definition,
( spl222_642
<=> k9_relat_1(sF218,sK17) = k9_relat_1(sF217,sF213) ),
introduced(definition,[new_symbols(definition,[spl222_642])],[avatar_definition]) ).
fof(f29296,plain,
( spl222_642
| ~ spl222_98
| ~ spl222_615 ),
inference(avatar_split_clause,[],[f29252,f28970,f22521,f29293]) ).
fof(f29299,plain,
( k3_subset_1(sK16,sF220) != k10_relset_1(sK14,sK16,sF218,sK17)
| k3_subset_1(sK16,sF220) != k9_relat_1(sF218,sK17)
| k9_relat_1(sF218,sK17) != k9_relat_1(sF217,sF213)
| sF220 != k3_subset_1(sK16,k10_relset_1(sK14,sK16,sF218,sK17))
| sF214 != k3_subset_1(sK16,k9_relat_1(sF217,sF213))
| sF214 = sF220 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
cnf(s28,plain,
spl222_25,
inference(sat_conversion,[],[f21913]) ).
cnf(s29,plain,
spl222_26,
inference(sat_conversion,[],[f21918]) ).
cnf(s30,plain,
spl222_27,
inference(sat_conversion,[],[f21923]) ).
cnf(s31,plain,
~ spl222_28,
inference(sat_conversion,[],[f21928]) ).
cnf(s33,plain,
spl222_30,
inference(sat_conversion,[],[f21942]) ).
cnf(s34,plain,
spl222_31,
inference(sat_conversion,[],[f21947]) ).
cnf(s35,plain,
spl222_32,
inference(sat_conversion,[],[f21952]) ).
cnf(s36,plain,
spl222_33,
inference(sat_conversion,[],[f21957]) ).
cnf(s37,plain,
spl222_34,
inference(sat_conversion,[],[f21962]) ).
cnf(s38,plain,
spl222_35,
inference(sat_conversion,[],[f21967]) ).
cnf(s39,plain,
spl222_36,
inference(sat_conversion,[],[f21972]) ).
cnf(s40,plain,
spl222_37,
inference(sat_conversion,[],[f21977]) ).
cnf(s41,plain,
spl222_38,
inference(sat_conversion,[],[f21982]) ).
cnf(s43,plain,
( ~ spl222_26
| spl222_39 ),
inference(sat_conversion,[],[f22012]) ).
cnf(s44,plain,
( ~ spl222_27
| ~ spl222_33
| spl222_40 ),
inference(sat_conversion,[],[f22017]) ).
cnf(s45,plain,
( ~ spl222_31
| ~ spl222_33
| ~ spl222_40
| ~ spl222_41
| spl222_42 ),
inference(sat_conversion,[],[f22033]) ).
cnf(s48,plain,
( ~ spl222_33
| ~ spl222_35
| ~ spl222_39
| ~ spl222_46
| spl222_47 ),
inference(sat_conversion,[],[f22067]) ).
cnf(s49,plain,
( ~ spl222_33
| ~ spl222_35
| ~ spl222_39
| spl222_45
| ~ spl222_46 ),
inference(sat_conversion,[],[f22068]) ).
cnf(s50,plain,
( ~ spl222_36
| ~ spl222_48
| spl222_49 ),
inference(sat_conversion,[],[f22081]) ).
cnf(s53,plain,
( ~ spl222_25
| ~ spl222_26
| ~ spl222_30
| ~ spl222_38
| spl222_51 ),
inference(sat_conversion,[],[f22104]) ).
cnf(s55,plain,
( ~ spl222_25
| ~ spl222_38
| ~ spl222_51
| ~ spl222_52
| spl222_53 ),
inference(sat_conversion,[],[f22116]) ).
cnf(s61,plain,
( ~ spl222_39
| spl222_58 ),
inference(sat_conversion,[],[f22149]) ).
cnf(s62,plain,
( ~ spl222_39
| spl222_59 ),
inference(sat_conversion,[],[f22155]) ).
cnf(s66,plain,
( ~ spl222_39
| spl222_65 ),
inference(sat_conversion,[],[f22207]) ).
cnf(s71,plain,
( ~ spl222_39
| spl222_52 ),
inference(sat_conversion,[],[f22227]) ).
cnf(s73,plain,
( ~ spl222_34
| ~ spl222_40
| spl222_46 ),
inference(sat_conversion,[],[f22231]) ).
cnf(s75,plain,
( ~ spl222_39
| ~ spl222_65
| spl222_67 ),
inference(sat_conversion,[],[f22242]) ).
cnf(s77,plain,
( ~ spl222_25
| ~ spl222_38
| ~ spl222_51
| ~ spl222_58
| ~ spl222_65
| ~ spl222_67
| spl222_68 ),
inference(sat_conversion,[],[f22249]) ).
cnf(s83,plain,
( ~ spl222_32
| ~ spl222_47
| spl222_48 ),
inference(sat_conversion,[],[f22283]) ).
cnf(s84,plain,
( ~ spl222_25
| ~ spl222_32
| ~ spl222_36
| ~ spl222_37
| ~ spl222_38
| ~ spl222_47
| spl222_71 ),
inference(sat_conversion,[],[f22293]) ).
cnf(s86,plain,
( ~ spl222_71
| ~ spl222_72
| spl222_73 ),
inference(sat_conversion,[],[f22303]) ).
cnf(s87,plain,
( spl222_72
| ~ spl222_74 ),
inference(sat_conversion,[],[f22309]) ).
cnf(s96,plain,
( ~ spl222_53
| ~ spl222_68
| spl222_81 ),
inference(sat_conversion,[],[f22370]) ).
cnf(s107,plain,
( ~ spl222_36
| spl222_44
| ~ spl222_48 ),
inference(sat_conversion,[],[f22428]) ).
cnf(s109,plain,
( ~ spl222_25
| ~ spl222_32
| ~ spl222_37
| ~ spl222_38
| ~ spl222_44
| ~ spl222_49
| spl222_89 ),
inference(sat_conversion,[],[f22437]) ).
cnf(s118,plain,
( ~ spl222_26
| spl222_95 ),
inference(sat_conversion,[],[f22495]) ).
cnf(s119,plain,
( ~ spl222_47
| spl222_74 ),
inference(sat_conversion,[],[f22497]) ).
cnf(s122,plain,
( ~ spl222_30
| ~ spl222_95
| spl222_98 ),
inference(sat_conversion,[],[f22524]) ).
cnf(s127,plain,
( spl222_41
| ~ spl222_81
| ~ spl222_98 ),
inference(sat_conversion,[],[f22527]) ).
cnf(s128,plain,
( ~ spl222_31
| ~ spl222_33
| ~ spl222_34
| ~ spl222_40
| ~ spl222_41
| spl222_99 ),
inference(sat_conversion,[],[f22537]) ).
cnf(s132,plain,
( ~ spl222_42
| ~ spl222_99
| spl222_102 ),
inference(sat_conversion,[],[f22560]) ).
cnf(s767,plain,
( ~ spl222_45
| ~ spl222_59
| ~ spl222_614
| spl222_615 ),
inference(sat_conversion,[],[f28972]) ).
cnf(s769,plain,
( ~ spl222_33
| ~ spl222_46
| spl222_614 ),
inference(sat_conversion,[],[f28986]) ).
cnf(s825,plain,
( ~ spl222_98
| ~ spl222_615
| spl222_642 ),
inference(sat_conversion,[],[f29296]) ).
cnf(s826,plain,
( spl222_28
| ~ spl222_71
| ~ spl222_73
| ~ spl222_89
| ~ spl222_102
| ~ spl222_642 ),
inference(sat_conversion,[],[f29299]) ).
cnf(s843,plain,
spl222_40,
inference(rat,[],[s44,s36,s30]) ).
cnf(s857,plain,
spl222_46,
inference(rat,[],[s73,s37,s843]) ).
cnf(s875,plain,
spl222_614,
inference(rat,[],[s769,s36,s857]) ).
cnf(s906,plain,
spl222_95,
inference(rat,[],[s118,s29]) ).
cnf(s910,plain,
spl222_39,
inference(rat,[],[s43,s29]) ).
cnf(s913,plain,
spl222_98,
inference(rat,[],[s122,s33,s906]) ).
cnf(s917,plain,
spl222_52,
inference(rat,[],[s71,s910]) ).
cnf(s918,plain,
spl222_65,
inference(rat,[],[s66,s910]) ).
cnf(s919,plain,
spl222_59,
inference(rat,[],[s62,s910]) ).
cnf(s920,plain,
spl222_58,
inference(rat,[],[s61,s910]) ).
cnf(s921,plain,
spl222_45,
inference(rat,[],[s49,s857,s36,s38,s910]) ).
cnf(s922,plain,
spl222_47,
inference(rat,[],[s48,s857,s36,s38,s910]) ).
cnf(s927,plain,
spl222_67,
inference(rat,[],[s75,s910,s918]) ).
cnf(s936,plain,
spl222_615,
inference(rat,[],[s767,s919,s875,s921]) ).
cnf(s941,plain,
spl222_74,
inference(rat,[],[s119,s922]) ).
cnf(s942,plain,
spl222_48,
inference(rat,[],[s83,s35,s922]) ).
cnf(s961,plain,
spl222_642,
inference(rat,[],[s825,s913,s936]) ).
cnf(s975,plain,
spl222_72,
inference(rat,[],[s87,s941]) ).
cnf(s981,plain,
spl222_49,
inference(rat,[],[s50,s39,s942]) ).
cnf(s982,plain,
spl222_44,
inference(rat,[],[s107,s39,s942]) ).
cnf(s1019,plain,
spl222_89,
inference(rat,[],[s109,s982,s981,s35,s41,s40,s28]) ).
cnf(s1021,plain,
spl222_71,
inference(rat,[],[s84,s922,s35,s41,s40,s39,s28]) ).
cnf(s1022,plain,
spl222_51,
inference(rat,[],[s53,s29,s41,s33,s28]) ).
cnf(s1043,plain,
spl222_73,
inference(rat,[],[s86,s975,s1021]) ).
cnf(s1044,plain,
spl222_68,
inference(rat,[],[s77,s28,s927,s918,s920,s41,s1022]) ).
cnf(s1045,plain,
spl222_53,
inference(rat,[],[s55,s28,s917,s41,s1022]) ).
cnf(s1070,plain,
~ spl222_102,
inference(rat,[],[s826,s961,s1021,s1019,s31,s1043]) ).
cnf(s1072,plain,
spl222_81,
inference(rat,[],[s96,s1044,s1045]) ).
cnf(s1094,plain,
spl222_41,
inference(rat,[],[s127,s913,s1072]) ).
cnf(s1103,plain,
spl222_99,
inference(rat,[],[s128,s843,s34,s36,s37,s1094]) ).
cnf(s1104,plain,
spl222_42,
inference(rat,[],[s45,s843,s34,s36,s1094]) ).
cnf(s1139,plain,
$false,
inference(rat,[],[s132,s1070,s1103,s1104]) ).
fof(f29300,plain,
$false,
inference(avatar_sat_refutation,[],[s1139]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU447+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n010.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 05:36:31 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 Running first-order theorem proving
% 0.15/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.31/3.96 % (1614054)Detected formulas, will run a generic FOF schedule.
% 14.31/3.96 % (1614061)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=3387598801:i=141695:sd=1:nm=32:gsp=on:ss=included_2989 on theBenchmark for (2989ds/141695Mi)
% 14.31/3.96 % (1614059)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=1275738174:i=141193_2989 on theBenchmark for (2989ds/141193Mi)
% 14.31/3.96 % (1614060)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=3805941551:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2989 on theBenchmark for (2989ds/134677Mi)
% 14.31/3.96 % (1614065)dis-21_1_sil=8000:lcm=predicate:random_seed=853316753:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2989 on theBenchmark for (2989ds/129Mi)
% 14.31/3.96 % (1614063)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3887547276:i=119:av=off:ss=axioms_2989 on theBenchmark for (2989ds/119Mi)
% 14.31/3.96 % (1614064)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=407296164:s2a=on:i=139:gtg=position_2989 on theBenchmark for (2989ds/139Mi)
% 14.31/3.96 % (1614062)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1278740000:i=109:sd=1:ins=1:gsp=on:ss=axioms_2989 on theBenchmark for (2989ds/109Mi)
% 14.31/3.96 % (1614064)Instruction limit reached!
% 14.31/3.96 % (1614064)------------------------------
% 14.31/3.96 % (1614064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.31/3.96 % (1614064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.31/3.96 % (1614064)CaDiCaL version: 2.1.3
% 14.31/3.96 % (1614064)Termination reason: Instruction limit
% 14.31/3.96 % (1614064)Termination phase: Property scanning
% 14.31/3.96 % (1614064)Time elapsed: 0.062 s
% 14.31/3.96 % (1614064)Peak memory usage: 112 MB
% 14.31/3.96 % (1614064)Instructions burned: 141 (million)
% 14.31/3.96 % (1614062)Instruction limit reached!
% 14.31/3.96 % (1614062)------------------------------
% 14.31/3.96 % (1614062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.31/3.96 % (1614062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.31/3.96 % (1614062)CaDiCaL version: 2.1.3
% 14.31/3.96 % (1614062)Termination reason: Instruction limit
% 14.31/3.96 % (1614062)Termination phase: SInE selection
% 14.31/3.96 % (1614062)Time elapsed: 0.080 s
% 14.31/3.96 % (1614062)Peak memory usage: 112 MB
% 14.31/3.96 % (1614062)Instructions burned: 110 (million)
% 14.31/3.96 % (1614065)Instruction limit reached!
% 14.31/3.96 % (1614065)------------------------------
% 14.31/3.96 % (1614065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.31/3.96 % (1614065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.31/3.96 % (1614065)CaDiCaL version: 2.1.3
% 14.31/3.96 % (1614065)Termination reason: Instruction limit
% 14.31/3.96 % (1614065)Termination phase: SInE selection
% 14.31/3.96 % (1614065)Time elapsed: 0.086 s
% 14.31/3.96 % (1614065)Peak memory usage: 113 MB
% 14.31/3.96 % (1614065)Instructions burned: 131 (million)
% 14.31/3.96 % (1614063)Instruction limit reached!
% 14.31/3.96 % (1614063)------------------------------
% 14.31/3.96 % (1614063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.31/3.96 % (1614063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.31/3.96 % (1614063)CaDiCaL version: 2.1.3
% 14.31/3.96 % (1614063)Termination reason: Instruction limit
% 14.31/3.96 % (1614063)Termination phase: Preprocessing 1
% 14.31/3.96 % (1614063)Time elapsed: 0.095 s
% 14.31/3.96 % (1614063)Peak memory usage: 113 MB
% 14.31/3.96 % (1614063)Instructions burned: 119 (million)
% 14.31/3.96 % (1614075)lrs+1011_1_sil=32000:sp=occurrence:random_seed=301976716:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 14.31/3.96 % (1614073)lrs+10_1_sil=8000:sp=occurrence:random_seed=405895220:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 14.31/3.96 % (1614074)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3982643986:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 14.31/3.96 % (1614076)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=490308788:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 14.31/3.96 % (1614074)Instruction limit reached!
% 23.34/5.05 % (1614074)------------------------------
% 23.34/5.05 % (1614074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/5.05 % (1614074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/5.05 % (1614074)CaDiCaL version: 2.1.3
% 23.34/5.05 % (1614074)Termination reason: Instruction limit
% 23.34/5.05 % (1614074)Termination phase: Property scanning
% 23.34/5.05 % (1614074)Time elapsed: 0.068 s
% 23.34/5.05 % (1614074)Peak memory usage: 112 MB
% 23.34/5.05 % (1614074)Instructions burned: 157 (million)
% 23.34/5.05 % (1614076)Instruction limit reached!
% 23.34/5.05 % (1614076)------------------------------
% 23.34/5.05 % (1614076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/5.05 % (1614076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/5.05 % (1614076)CaDiCaL version: 2.1.3
% 23.34/5.05 % (1614076)Termination reason: Instruction limit
% 23.34/5.05 % (1614076)Termination phase: Property scanning
% 23.34/5.05 % (1614076)Time elapsed: 0.106 s
% 23.34/5.05 % (1614076)Peak memory usage: 112 MB
% 23.34/5.05 % (1614076)Instructions burned: 250 (million)
% 23.34/5.05 % (1614073)Instruction limit reached!
% 23.34/5.05 % (1614073)------------------------------
% 23.34/5.05 % (1614073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/5.05 % (1614073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/5.05 % (1614073)CaDiCaL version: 2.1.3
% 23.34/5.05 % (1614073)Termination reason: Instruction limit
% 23.34/5.05 % (1614073)Termination phase: Saturation
% 23.34/5.05 % (1614073)Time elapsed: 0.197 s
% 23.34/5.05 % (1614073)Peak memory usage: 119 MB
% 23.34/5.05 % (1614073)Instructions burned: 286 (million)
% 23.34/5.05 % (1614081)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3831740046:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 23.34/5.05 % (1614082)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3635397868:i=2350_2984 on theBenchmark for (2984ds/2350Mi)
% 23.34/5.05 % (1614075)Instruction limit reached!
% 23.34/5.05 % (1614075)------------------------------
% 23.34/5.05 % (1614075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/5.05 % (1614075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/5.05 % (1614075)CaDiCaL version: 2.1.3
% 23.34/5.05 % (1614075)Termination reason: Instruction limit
% 23.34/5.05 % (1614075)Termination phase: Saturation
% 23.34/5.05 % (1614075)Time elapsed: 0.251 s
% 23.34/5.05 % (1614075)Peak memory usage: 119 MB
% 23.34/5.05 % (1614075)Instructions burned: 326 (million)
% 23.34/5.05 % (1614083)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2589926699:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 23.34/5.05 % (1614086)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1603992934:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 23.34/5.05 % (1614083)Instruction limit reached!
% 23.34/5.05 % (1614083)------------------------------
% 23.34/5.05 % (1614083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/5.05 % (1614083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/5.05 % (1614083)CaDiCaL version: 2.1.3
% 23.34/5.05 % (1614083)Termination reason: Instruction limit
% 23.34/5.05 % (1614083)Termination phase: SInE selection
% 23.34/5.05 % (1614083)Time elapsed: 0.088 s
% 23.34/5.05 % (1614083)Peak memory usage: 112 MB
% 23.34/5.05 % (1614083)Instructions burned: 114 (million)
% 23.34/5.05 % (1614081)Instruction limit reached!
% 23.34/5.05 % (1614081)------------------------------
% 23.34/5.05 % (1614081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/5.05 % (1614081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/5.05 % (1614081)CaDiCaL version: 2.1.3
% 23.34/5.05 % (1614081)Termination reason: Instruction limit
% 23.34/5.05 % (1614081)Termination phase: Function definition elimination
% 23.34/5.05 % (1614081)Time elapsed: 0.216 s
% 23.34/5.05 % (1614081)Peak memory usage: 118 MB
% 23.34/5.05 % (1614081)Instructions burned: 295 (million)
% 23.34/5.05 % (1614086)Instruction limit reached!
% 23.34/5.05 % (1614086)------------------------------
% 23.34/5.05 % (1614086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/5.05 % (1614086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/5.05 % (1614086)CaDiCaL version: 2.1.3
% 64.94/10.94 % (1614086)Termination reason: Instruction limit
% 64.94/10.94 % (1614086)Termination phase: Preprocessing 1
% 64.94/10.94 % (1614086)Time elapsed: 0.092 s
% 64.94/10.94 % (1614086)Peak memory usage: 113 MB
% 64.94/10.94 % (1614086)Instructions burned: 128 (million)
% 64.94/10.94 % (1614089)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2171120853:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2981 on theBenchmark for (2981ds/114Mi)
% 64.94/10.94 % (1614090)lrs+10_1_sil=8000:sp=occurrence:random_seed=4136903955:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2981 on theBenchmark for (2981ds/907Mi)
% 64.94/10.94 % (1614089)Instruction limit reached!
% 64.94/10.94 % (1614089)------------------------------
% 64.94/10.94 % (1614089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.94/10.94 % (1614089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.94/10.94 % (1614089)CaDiCaL version: 2.1.3
% 64.94/10.94 % (1614089)Termination reason: Instruction limit
% 64.94/10.94 % (1614089)Termination phase: Property scanning
% 64.94/10.94 % (1614089)Time elapsed: 0.050 s
% 64.94/10.94 % (1614089)Peak memory usage: 112 MB
% 64.94/10.94 % (1614089)Instructions burned: 116 (million)
% 64.94/10.94 % (1614091)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=59638396:i=437:sd=1:aac=none:ss=included_2980 on theBenchmark for (2980ds/437Mi)
% 64.94/10.94 % (1614094)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3907763440:i=5202:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/5202Mi)
% 64.94/10.94 % (1614091)Instruction limit reached!
% 64.94/10.94 % (1614091)------------------------------
% 64.94/10.94 % (1614091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.94/10.94 % (1614091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.94/10.94 % (1614091)CaDiCaL version: 2.1.3
% 64.94/10.94 % (1614091)Termination reason: Instruction limit
% 64.94/10.94 % (1614091)Termination phase: Saturation
% 64.94/10.94 % (1614091)Time elapsed: 0.296 s
% 64.94/10.94 % (1614091)Peak memory usage: 121 MB
% 64.94/10.94 % (1614091)Instructions burned: 437 (million)
% 64.94/10.94 % (1614097)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=899268232:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2976 on theBenchmark for (2976ds/134Mi)
% 64.94/10.94 % (1614090)Instruction limit reached!
% 64.94/10.94 % (1614090)------------------------------
% 64.94/10.94 % (1614090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.94/10.94 % (1614090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.94/10.94 % (1614090)CaDiCaL version: 2.1.3
% 64.94/10.94 % (1614090)Termination reason: Instruction limit
% 64.94/10.94 % (1614090)Termination phase: Saturation
% 64.94/10.94 % (1614090)Time elapsed: 0.521 s
% 64.94/10.94 % (1614090)Peak memory usage: 131 MB
% 64.94/10.94 % (1614090)Instructions burned: 909 (million)
% 64.94/10.94 % (1614097)Instruction limit reached!
% 64.94/10.94 % (1614097)------------------------------
% 64.94/10.94 % (1614097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.94/10.94 % (1614097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.94/10.94 % (1614097)CaDiCaL version: 2.1.3
% 64.94/10.94 % (1614097)Termination reason: Instruction limit
% 64.94/10.94 % (1614097)Termination phase: NewCNF
% 64.94/10.94 % (1614097)Time elapsed: 0.119 s
% 64.94/10.94 % (1614097)Peak memory usage: 115 MB
% 64.94/10.94 % (1614097)Instructions burned: 135 (million)
% 64.94/10.94 % (1614099)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=885303061:st=8:i=592:sd=3:ep=RST:ss=axioms_2974 on theBenchmark for (2974ds/592Mi)
% 64.94/10.94 % (1614100)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2507410702:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 64.94/10.94 % (1614082)Instruction limit reached!
% 64.94/10.94 % (1614082)------------------------------
% 64.94/10.94 % (1614082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.94/10.94 % (1614082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.94/10.94 % (1614082)CaDiCaL version: 2.1.3
% 64.94/10.94 % (1614082)Termination reason: Instruction limit
% 64.94/10.94 % (1614082)Termination phase: Property scanning
% 64.94/10.94 % (1614082)Time elapsed: 1.245 s
% 64.94/10.94 % (1614082)Peak memory usage: 171 MB
% 64.94/10.94 % (1614082)Instructions burned: 2351 (million)
% 64.94/10.94 % (1614103)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=49580460:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/125Mi)
% 67.08/11.30 % (1614099)Instruction limit reached!
% 67.08/11.30 % (1614099)------------------------------
% 67.08/11.30 % (1614099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.08/11.30 % (1614099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.08/11.30 % (1614099)CaDiCaL version: 2.1.3
% 67.08/11.30 % (1614099)Termination reason: Instruction limit
% 67.08/11.30 % (1614099)Termination phase: Preprocessing 3
% 67.08/11.30 % (1614099)Time elapsed: 0.450 s
% 67.08/11.30 % (1614099)Peak memory usage: 134 MB
% 67.08/11.30 % (1614099)Instructions burned: 592 (million)
% 67.08/11.30 % (1614103)Instruction limit reached!
% 67.08/11.30 % (1614103)------------------------------
% 67.08/11.30 % (1614103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.08/11.30 % (1614103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.08/11.30 % (1614103)CaDiCaL version: 2.1.3
% 67.08/11.30 % (1614103)Termination reason: Instruction limit
% 67.08/11.30 % (1614103)Termination phase: Property scanning
% 67.08/11.30 % (1614103)Time elapsed: 0.056 s
% 67.08/11.30 % (1614103)Peak memory usage: 112 MB
% 67.08/11.30 % (1614103)Instructions burned: 127 (million)
% 67.08/11.30 % (1614105)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=607349050:i=134:gtgl=5:slsql=off:gtg=exists_sym_2968 on theBenchmark for (2968ds/134Mi)
% 67.08/11.30 % (1614106)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1985554616:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/141Mi)
% 67.08/11.30 % (1614105)Instruction limit reached!
% 67.08/11.30 % (1614105)------------------------------
% 67.08/11.30 % (1614105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.08/11.30 % (1614105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.08/11.30 % (1614105)CaDiCaL version: 2.1.3
% 67.08/11.30 % (1614105)Termination reason: Instruction limit
% 67.08/11.30 % (1614105)Termination phase: Property scanning
% 67.08/11.30 % (1614105)Time elapsed: 0.058 s
% 67.08/11.30 % (1614105)Peak memory usage: 112 MB
% 67.08/11.30 % (1614105)Instructions burned: 135 (million)
% 67.08/11.30 % (1614106)Instruction limit reached!
% 67.08/11.30 % (1614106)------------------------------
% 67.08/11.30 % (1614106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.08/11.30 % (1614106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.08/11.30 % (1614106)CaDiCaL version: 2.1.3
% 67.08/11.30 % (1614106)Termination reason: Instruction limit
% 67.08/11.30 % (1614106)Termination phase: Saturation
% 67.08/11.30 % (1614106)Time elapsed: 0.117 s
% 67.08/11.30 % (1614106)Peak memory usage: 117 MB
% 67.08/11.30 % (1614106)Instructions burned: 141 (million)
% 67.08/11.30 % (1614109)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3451147558:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2966 on theBenchmark for (2966ds/431Mi)
% 67.08/11.30 % (1614110)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=1807429120:i=6060:aac=none:ins=25_2965 on theBenchmark for (2965ds/6060Mi)
% 67.08/11.30 % (1614109)Refutation not found, incomplete strategy
% 67.08/11.30 % (1614109)------------------------------
% 67.08/11.30 % (1614109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.08/11.30 % (1614109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.08/11.30 % (1614109)CaDiCaL version: 2.1.3
% 67.08/11.30 % (1614109)Termination reason: Refutation not found, incomplete strategy
% 67.08/11.30 % (1614109)Time elapsed: 0.246 s
% 67.08/11.30 % (1614109)Peak memory usage: 121 MB
% 67.08/11.30 % (1614109)Instructions burned: 347 (million)
% 67.08/11.30 % (1614109)------------------------------
% 67.08/11.30 % (1614109)------------------------------
% 67.08/11.30 % (1614113)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=414922006:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2960 on theBenchmark for (2960ds/150Mi)
% 67.08/11.30 % (1614113)Instruction limit reached!
% 67.08/11.30 % (1614113)------------------------------
% 67.08/11.30 % (1614113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.08/11.30 % (1614113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.08/11.30 % (1614113)CaDiCaL version: 2.1.3
% 67.08/11.30 % (1614113)Termination reason: Instruction limit
% 67.08/11.30 % (1614113)Termination phase: Preprocessing 1
% 67.08/11.30 % (1614113)Time elapsed: 0.123 s
% 67.08/11.30 % (1614113)Peak memory usage: 113 MB
% 67.08/11.30 % (1614113)Instructions burned: 150 (million)
% 67.08/11.30 % (1614115)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3260454200:i=14155:bd=all_2958 on theBenchmark for (2958ds/14155Mi)
% 67.08/11.30 % (1614094)Instruction limit reached!
% 67.08/11.30 % (1614094)------------------------------
% 67.08/11.30 % (1614094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.08/11.30 % (1614094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.08/11.30 % (1614094)CaDiCaL version: 2.1.3
% 67.08/11.30 % (1614094)Termination reason: Instruction limit
% 67.08/11.30 % (1614094)Termination phase: Saturation
% 67.08/11.30 % (1614094)Time elapsed: 3.988 s
% 67.08/11.30 % (1614094)Peak memory usage: 600 MB
% 67.08/11.30 % (1614094)Instructions burned: 5202 (million)
% 67.08/11.30 % (1614117)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4028359557:i=667:av=off:fsr=off_2937 on theBenchmark for (2937ds/667Mi)
% 67.08/11.30 % (1614117)Instruction limit reached!
% 67.08/11.30 % (1614117)------------------------------
% 67.08/11.30 % (1614117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.08/11.30 % (1614117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.08/11.30 % (1614117)CaDiCaL version: 2.1.3
% 67.08/11.30 % (1614117)Termination reason: Instruction limit
% 67.08/11.30 % (1614117)Termination phase: NewCNF
% 67.08/11.30 % (1614117)Time elapsed: 0.514 s
% 67.08/11.30 % (1614117)Peak memory usage: 149 MB
% 67.08/11.30 % (1614117)Instructions burned: 668 (million)
% 67.08/11.30 % (1614119)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=483079853:s2a=on:i=185:s2at=1.8:fdi=4_2931 on theBenchmark for (2931ds/185Mi)
% 67.08/11.30 % (1614119)Instruction limit reached!
% 67.08/11.30 % (1614119)------------------------------
% 67.08/11.30 % (1614119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.08/11.30 % (1614119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.08/11.30 % (1614119)CaDiCaL version: 2.1.3
% 67.08/11.30 % (1614119)Termination reason: Instruction limit
% 67.08/11.30 % (1614119)Termination phase: SInE selection
% 67.08/11.30 % (1614119)Time elapsed: 0.150 s
% 67.08/11.30 % (1614119)Peak memory usage: 113 MB
% 67.08/11.30 % (1614119)Instructions burned: 185 (million)
% 67.08/11.30 % (1614121)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2361612313:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2928 on theBenchmark for (2928ds/193Mi)
% 67.08/11.30 % (1614121)Instruction limit reached!
% 67.08/11.30 % (1614121)------------------------------
% 67.08/11.30 % (1614121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.08/11.30 % (1614121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.08/11.30 % (1614121)CaDiCaL version: 2.1.3
% 67.08/11.30 % (1614121)Termination reason: Instruction limit
% 67.08/11.30 % (1614121)Termination phase: SInE selection
% 67.08/11.30 % (1614121)Time elapsed: 0.158 s
% 67.08/11.30 % (1614121)Peak memory usage: 112 MB
% 67.08/11.30 % (1614121)Instructions burned: 193 (million)
% 67.08/11.30 % (1614123)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4262511273:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2925 on theBenchmark for (2925ds/4850Mi)
% 67.08/11.30 % (1614110)Instruction limit reached!
% 67.08/11.30 % (1614110)------------------------------
% 67.08/11.30 % (1614110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.08/11.30 % (1614110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.08/11.30 % (1614110)CaDiCaL version: 2.1.3
% 67.08/11.30 % (1614110)Termination reason: Instruction limit
% 67.08/11.30 % (1614110)Termination phase: Saturation
% 67.08/11.30 % (1614110)Time elapsed: 4.512 s
% 67.08/11.30 % (1614110)Peak memory usage: 569 MB
% 67.08/11.30 % (1614110)Instructions burned: 6061 (million)
% 67.08/11.30 % (1614125)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3825833554:i=12111:sd=1:ss=included_2919 on theBenchmark for (2919ds/12111Mi)
% 67.08/11.30 % (1614125)First to succeed.
% 67.08/11.30 % (1614125)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1614054"
% 67.08/11.30 % (1614125)Refutation found. Thanks to Tanya!
% 67.08/11.30 % SZS status Theorem for theBenchmark
% 67.08/11.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/11.50 % (1614125)------------------------------
% 0.16/11.50 % (1614125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/11.50 % (1614125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/11.50 % (1614125)CaDiCaL version: 2.1.3
% 0.16/11.50 % (1614125)Termination reason: Refutation
% 0.16/11.50 % (1614125)Time elapsed: 1.837 s
% 0.16/11.50 % (1614125)Peak memory usage: 182 MB
% 0.16/11.50 % (1614125)Instructions burned: 2729 (million)
% 0.16/11.50 % (1614125)------------------------------
% 0.16/11.50 % (1614125)------------------------------
% 0.16/11.50 % (1614054)Success in time 10.438 s
% 0.16/11.50 % Vampire exiting
%------------------------------------------------------------------------------