%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU442+4 : 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 : n018.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 74.74s 25.37s
% Output : Refutation 131.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 128
% Syntax : Number of formulae : 738 ( 118 unt; 96 def)
% Number of atoms : 1887 ( 311 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 2139 ( 990 ~; 991 |; 29 &)
% ( 96 <=>; 32 =>; 0 <=; 1 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 99 ( 97 usr; 93 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 8 con; 0-5 aty)
% Number of variables : 318 ( 1 sgn 306 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
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(f54,axiom,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_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(f77,axiom,
! [X0,X1,X2] :
( ( r1_tarski(X0,X1)
& r1_tarski(X2,X1) )
=> r1_tarski(k2_xboole_0(X0,X2),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_xboole_1) ).
fof(f81,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
=> k2_xboole_0(X0,X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_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(f865,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r1_tarski(X0,X1)
=> r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t156_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(f869,axiom,
! [X0] :
( v1_relat_1(X0)
=> ! [X1] :
( v1_relat_1(X1)
=> k2_relat_1(k5_relat_1(X0,X1)) = k9_relat_1(X1,k2_relat_1(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t160_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(f1422,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(f1481,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(f1483,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(f1498,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(f1499,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> k6_relset_1(X0,X1,k6_relset_1(X0,X1,X2)) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',involutiveness_k6_relset_1) ).
fof(f1500,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(f1508,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(f6128,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(f71077,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(f71078,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(f71133,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(f71134,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(f71135,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(f71136,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(f71137,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)],[f71136]) ).
fof(f71153,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f18]) ).
fof(f71224,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,[],[f71077]) ).
fof(f71225,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,[],[f71224]) ).
fof(f71226,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,[],[f71078]) ).
fof(f71227,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,[],[f71226]) ).
fof(f71288,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,[],[f71133]) ).
fof(f71289,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,[],[f71134]) ).
fof(f71290,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,[],[f71135]) ).
fof(f71291,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,[],[f71137]) ).
fof(f71368,plain,
! [X0,X1] :
( k3_xboole_0(X0,X1) = X0
| ~ r1_tarski(X0,X1) ),
inference(ennf_transformation,[],[f97]) ).
fof(f71392,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,[],[f1481]) ).
fof(f71393,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1422]) ).
fof(f71478,plain,
! [X0] :
( ! [X1] :
( k2_relat_1(k5_relat_1(X0,X1)) = k9_relat_1(X1,k2_relat_1(X0))
| ~ v1_relat_1(X1) )
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f869]) ).
fof(f71479,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(f71484,plain,
! [X0,X1,X2] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f865]) ).
fof(f71485,plain,
! [X0,X1,X2] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(flattening,[],[f71484]) ).
fof(f71495,plain,
! [X0] :
( k9_relat_1(X0,k1_relat_1(X0)) = k2_relat_1(X0)
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f855]) ).
fof(f71497,plain,
! [X0,X1] :
( r1_tarski(k9_relat_1(X1,X0),k2_relat_1(X1))
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f853]) ).
fof(f71702,plain,
! [X0,X1] :
( k2_xboole_0(X0,X1) = X1
| ~ r1_tarski(X0,X1) ),
inference(ennf_transformation,[],[f81]) ).
fof(f71706,plain,
! [X0,X1,X2] :
( r1_tarski(k2_xboole_0(X0,X2),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X2,X1) ),
inference(ennf_transformation,[],[f77]) ).
fof(f71707,plain,
! [X0,X1,X2] :
( r1_tarski(k2_xboole_0(X0,X2),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X2,X1) ),
inference(flattening,[],[f71706]) ).
fof(f71795,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f71796,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(flattening,[],[f71795]) ).
fof(f71847,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,[],[f1508]) ).
fof(f72269,plain,
! [X0] :
( k4_relat_1(k4_relat_1(X0)) = X0
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f907]) ).
fof(f72272,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(f72294,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,[],[f6128]) ).
fof(f72303,plain,
! [X0,X1,X2] :
( k6_relset_1(X0,X1,X2) = k4_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1500]) ).
fof(f72304,plain,
! [X0,X1,X2] :
( k6_relset_1(X0,X1,k6_relset_1(X0,X1,X2)) = X2
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1499]) ).
fof(f72305,plain,
! [X0,X1,X2] :
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1498]) ).
fof(f72359,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,[],[f71291]) ).
fof(f72360,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,[],[f72359]) ).
fof(f72361,plain,
( ( ~ r1_tarski(sK29,k10_relset_1(sK27,sK27,k9_relset_2(sK27,sK28,sK27,sK30,k6_relset_1(sK27,sK28,sK30)),sK29))
| ~ r1_tarski(sK29,k1_funct_5(sK30)) )
& ( r1_tarski(sK29,k10_relset_1(sK27,sK27,k9_relset_2(sK27,sK28,sK27,sK30,k6_relset_1(sK27,sK28,sK30)),sK29))
| r1_tarski(sK29,k1_funct_5(sK30)) )
& m2_relset_1(sK30,sK27,sK28)
& m1_subset_1(sK29,k1_zfmisc_1(sK27)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27,sK28,sK29,sK30]),skolemize(X0,sK27),skolemize(X1,sK28),skolemize(X2,sK29),skolemize(X3,sK30)],[f72360]) ).
fof(f72387,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,[],[f1483]) ).
fof(f72527,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(f72528,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,[],[f72527]) ).
fof(f72782,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,[],[f71225]) ).
fof(f72783,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,[],[f71227]) ).
fof(f72863,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X1,X0)
| k10_relset_1(X1,X0,X2,X1) = k2_funct_5(X2) ),
inference(cnf_transformation,[],[f71288]) ).
fof(f72864,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,[],[f71288]) ).
fof(f72865,plain,
! [X2,X3,X0,X1,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(cnf_transformation,[],[f71289]) ).
fof(f72866,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,[],[f71289]) ).
fof(f72867,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,[],[f71290]) ).
fof(f72868,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,[],[f71290]) ).
fof(f72870,plain,
m2_relset_1(sK30,sK27,sK28),
inference(cnf_transformation,[],[f72361]) ).
fof(f72871,plain,
( r1_tarski(sK29,k10_relset_1(sK27,sK27,k9_relset_2(sK27,sK28,sK27,sK30,k6_relset_1(sK27,sK28,sK30)),sK29))
| r1_tarski(sK29,k1_funct_5(sK30)) ),
inference(cnf_transformation,[],[f72361]) ).
fof(f72872,plain,
( ~ r1_tarski(sK29,k10_relset_1(sK27,sK27,k9_relset_2(sK27,sK28,sK27,sK30,k6_relset_1(sK27,sK28,sK30)),sK29))
| ~ r1_tarski(sK29,k1_funct_5(sK30)) ),
inference(cnf_transformation,[],[f72361]) ).
fof(f72966,plain,
! [X0,X1] :
( k3_xboole_0(X0,X1) = X0
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f71368]) ).
fof(f72983,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f57]) ).
fof(f73020,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f72387]) ).
fof(f73035,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f71392]) ).
fof(f73036,plain,
! [X2,X0,X1] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f71393]) ).
fof(f73121,plain,
! [X0,X1] :
( ~ v1_relat_1(X1)
| k2_relat_1(k5_relat_1(X0,X1)) = k9_relat_1(X1,k2_relat_1(X0))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f71478]) ).
fof(f73122,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,[],[f71479]) ).
fof(f73125,plain,
! [X2,X0,X1] :
( ~ v1_relat_1(X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ),
inference(cnf_transformation,[],[f71485]) ).
fof(f73136,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k2_relat_1(X0) = k9_relat_1(X0,k1_relat_1(X0)) ),
inference(cnf_transformation,[],[f71495]) ).
fof(f73138,plain,
! [X0,X1] :
( ~ v1_relat_1(X1)
| r1_tarski(k9_relat_1(X1,X0),k2_relat_1(X1)) ),
inference(cnf_transformation,[],[f71497]) ).
fof(f73449,plain,
! [X0,X1] :
( k2_xboole_0(X0,X1) = X1
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f71702]) ).
fof(f73453,plain,
! [X2,X0,X1] :
( r1_tarski(k2_xboole_0(X0,X2),X1)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X2,X1) ),
inference(cnf_transformation,[],[f71707]) ).
fof(f73460,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X1,X0),
inference(cnf_transformation,[],[f54]) ).
fof(f73580,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f73635,plain,
! [X2,X0,X1] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(cnf_transformation,[],[f71796]) ).
fof(f73638,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| X0 = X1
| ~ r1_tarski(X1,X0) ),
inference(cnf_transformation,[],[f72528]) ).
fof(f73639,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f71153]) ).
fof(f73715,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,[],[f71847]) ).
fof(f74350,plain,
! [X0] :
( k4_relat_1(k4_relat_1(X0)) = X0
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f72269]) ).
fof(f74353,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,[],[f72272]) ).
fof(f74403,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k2_relat_1(X0) = k2_funct_5(X0) ),
inference(cnf_transformation,[],[f72294]) ).
fof(f74404,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k1_relat_1(X0) = k1_funct_5(X0) ),
inference(cnf_transformation,[],[f72294]) ).
fof(f74445,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
inference(cnf_transformation,[],[f72303]) ).
fof(f74446,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k6_relset_1(X0,X1,k6_relset_1(X0,X1,X2)) = X2 ),
inference(cnf_transformation,[],[f72304]) ).
fof(f74447,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
inference(cnf_transformation,[],[f72305]) ).
fof(f74564,plain,
! [X0,X1] :
( k4_xboole_0(X0,k4_xboole_0(X0,X1)) = X0
| ~ r1_tarski(X0,X1) ),
inference(definition_unfolding,[],[f72966,f73580]) ).
fof(f74581,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k4_xboole_0(X1,k4_xboole_0(X1,X0)),
inference(definition_unfolding,[],[f72983,f73580,f73580]) ).
fof(f75034,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,[],[f74353,f73580]) ).
fof(f75245,definition,
sF304 = k6_relset_1(sK27,sK28,sK30),
introduced(definition,[new_symbols(definition,[sF304])],[function_definition]) ).
fof(f75246,plain,
k6_relset_1(sK27,sK28,sK30) = sF304,
inference(reorient_equations,[],[f75245]) ).
fof(f75247,definition,
sF305 = k9_relset_2(sK27,sK28,sK27,sK30,sF304),
introduced(definition,[new_symbols(definition,[sF305])],[function_definition]) ).
fof(f75248,plain,
k9_relset_2(sK27,sK28,sK27,sK30,sF304) = sF305,
inference(reorient_equations,[],[f75247]) ).
fof(f75249,definition,
sF306 = k10_relset_1(sK27,sK27,sF305,sK29),
introduced(definition,[new_symbols(definition,[sF306])],[function_definition]) ).
fof(f75250,plain,
k10_relset_1(sK27,sK27,sF305,sK29) = sF306,
inference(reorient_equations,[],[f75249]) ).
fof(f75251,definition,
sF307 = k1_funct_5(sK30),
introduced(definition,[new_symbols(definition,[sF307])],[function_definition]) ).
fof(f75252,plain,
k1_funct_5(sK30) = sF307,
inference(reorient_equations,[],[f75251]) ).
fof(f75253,plain,
( ~ r1_tarski(sK29,sF306)
| ~ r1_tarski(sK29,sF307) ),
inference(definition_folding,[],[f72872,f75252,f75250,f75248,f75246]) ).
fof(f75254,plain,
( r1_tarski(sK29,sF306)
| r1_tarski(sK29,sF307) ),
inference(definition_folding,[],[f72871,f75252,f75250,f75248,f75246]) ).
fof(f75597,definition,
( spl309_47
<=> m2_relset_1(sK30,sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl309_47])],[avatar_definition]) ).
fof(f75599,plain,
( m2_relset_1(sK30,sK27,sK28)
| ~ spl309_47 ),
inference(avatar_component_clause,[],[f75597]) ).
fof(f75600,plain,
spl309_47,
inference(avatar_split_clause,[],[f72870,f75597]) ).
fof(f75602,definition,
( spl309_48
<=> r1_tarski(sK29,sF307) ),
introduced(definition,[new_symbols(definition,[spl309_48])],[avatar_definition]) ).
fof(f75603,plain,
( ~ r1_tarski(sK29,sF307)
| spl309_48 ),
inference(avatar_component_clause,[],[f75602]) ).
fof(f75604,plain,
( r1_tarski(sK29,sF307)
| ~ spl309_48 ),
inference(avatar_component_clause,[],[f75602]) ).
fof(f75606,definition,
( spl309_49
<=> r1_tarski(sK29,sF306) ),
introduced(definition,[new_symbols(definition,[spl309_49])],[avatar_definition]) ).
fof(f75607,plain,
( ~ r1_tarski(sK29,sF306)
| spl309_49 ),
inference(avatar_component_clause,[],[f75606]) ).
fof(f75608,plain,
( r1_tarski(sK29,sF306)
| ~ spl309_49 ),
inference(avatar_component_clause,[],[f75606]) ).
fof(f75609,plain,
( spl309_48
| spl309_49 ),
inference(avatar_split_clause,[],[f75254,f75606,f75602]) ).
fof(f75610,plain,
( ~ spl309_48
| ~ spl309_49 ),
inference(avatar_split_clause,[],[f75253,f75606,f75602]) ).
fof(f75625,definition,
( spl309_51
<=> k6_relset_1(sK27,sK28,sK30) = sF304 ),
introduced(definition,[new_symbols(definition,[spl309_51])],[avatar_definition]) ).
fof(f75627,plain,
( k6_relset_1(sK27,sK28,sK30) = sF304
| ~ spl309_51 ),
inference(avatar_component_clause,[],[f75625]) ).
fof(f75628,plain,
spl309_51,
inference(avatar_split_clause,[],[f75246,f75625]) ).
fof(f75630,definition,
( spl309_52
<=> k9_relset_2(sK27,sK28,sK27,sK30,sF304) = sF305 ),
introduced(definition,[new_symbols(definition,[spl309_52])],[avatar_definition]) ).
fof(f75632,plain,
( k9_relset_2(sK27,sK28,sK27,sK30,sF304) = sF305
| ~ spl309_52 ),
inference(avatar_component_clause,[],[f75630]) ).
fof(f75633,plain,
spl309_52,
inference(avatar_split_clause,[],[f75248,f75630]) ).
fof(f75635,definition,
( spl309_53
<=> k10_relset_1(sK27,sK27,sF305,sK29) = sF306 ),
introduced(definition,[new_symbols(definition,[spl309_53])],[avatar_definition]) ).
fof(f75637,plain,
( k10_relset_1(sK27,sK27,sF305,sK29) = sF306
| ~ spl309_53 ),
inference(avatar_component_clause,[],[f75635]) ).
fof(f75638,plain,
spl309_53,
inference(avatar_split_clause,[],[f75250,f75635]) ).
fof(f75640,definition,
( spl309_54
<=> k1_funct_5(sK30) = sF307 ),
introduced(definition,[new_symbols(definition,[spl309_54])],[avatar_definition]) ).
fof(f75642,plain,
( k1_funct_5(sK30) = sF307
| ~ spl309_54 ),
inference(avatar_component_clause,[],[f75640]) ).
fof(f75643,plain,
spl309_54,
inference(avatar_split_clause,[],[f75252,f75640]) ).
fof(f75743,plain,
( r1_tarski(k1_funct_5(sF305),k1_funct_5(sK30))
| ~ m2_relset_1(sF304,sK28,sK27)
| ~ m2_relset_1(sK30,sK27,sK28)
| ~ spl309_52 ),
inference(superposition,[],[f72865,f75632]) ).
fof(f75744,plain,
( r1_tarski(k1_funct_5(sF305),k1_funct_5(sK30))
| ~ m2_relset_1(sF304,sK28,sK27)
| ~ spl309_47
| ~ spl309_52 ),
inference(forward_subsumption_resolution,[],[f75743,f75599]) ).
fof(f75745,plain,
( r1_tarski(k1_funct_5(sF305),sF307)
| ~ m2_relset_1(sF304,sK28,sK27)
| ~ spl309_47
| ~ spl309_52
| ~ spl309_54 ),
inference(forward_demodulation,[],[f75744,f75642]) ).
fof(f75747,definition,
( spl309_60
<=> m2_relset_1(sF304,sK28,sK27) ),
introduced(definition,[new_symbols(definition,[spl309_60])],[avatar_definition]) ).
fof(f75748,plain,
( m2_relset_1(sF304,sK28,sK27)
| ~ spl309_60 ),
inference(avatar_component_clause,[],[f75747]) ).
fof(f75749,plain,
( ~ m2_relset_1(sF304,sK28,sK27)
| spl309_60 ),
inference(avatar_component_clause,[],[f75747]) ).
fof(f75751,definition,
( spl309_61
<=> r1_tarski(k1_funct_5(sF305),sF307) ),
introduced(definition,[new_symbols(definition,[spl309_61])],[avatar_definition]) ).
fof(f75753,plain,
( r1_tarski(k1_funct_5(sF305),sF307)
| ~ spl309_61 ),
inference(avatar_component_clause,[],[f75751]) ).
fof(f75754,plain,
( ~ spl309_60
| spl309_61
| ~ spl309_47
| ~ spl309_52
| ~ spl309_54 ),
inference(avatar_split_clause,[],[f75745,f75640,f75630,f75597,f75751,f75747]) ).
fof(f75755,plain,
( ! [X0,X1] :
( k1_funct_5(k9_relset_2(X0,sK27,sK28,X1,sK30)) = k10_relset_1(sK27,X0,k6_relset_1(X0,sK27,X1),k1_funct_5(sK30))
| ~ m2_relset_1(X1,X0,sK27) )
| ~ spl309_47 ),
inference(resolution,[],[f72866,f75599]) ).
fof(f75756,plain,
( ! [X0,X1] :
( ~ m2_relset_1(X1,X0,sK27)
| k1_funct_5(k9_relset_2(X0,sK27,sK28,X1,sK30)) = k10_relset_1(sK27,X0,k6_relset_1(X0,sK27,X1),sF307) )
| ~ spl309_47
| ~ spl309_54 ),
inference(forward_demodulation,[],[f75755,f75642]) ).
fof(f75758,plain,
( k1_funct_5(sK30) = k10_relset_1(sK28,sK27,k6_relset_1(sK27,sK28,sK30),sK28)
| ~ spl309_47 ),
inference(resolution,[],[f72864,f75599]) ).
fof(f75759,plain,
( k1_funct_5(sK30) = k10_relset_1(sK28,sK27,sF304,sK28)
| ~ spl309_47
| ~ spl309_51 ),
inference(forward_demodulation,[],[f75758,f75627]) ).
fof(f75761,plain,
( sF307 = k10_relset_1(sK28,sK27,sF304,sK28)
| ~ spl309_47
| ~ spl309_51
| ~ spl309_54 ),
inference(forward_demodulation,[],[f75759,f75642]) ).
fof(f75764,definition,
( spl309_62
<=> sF307 = k10_relset_1(sK28,sK27,sF304,sK28) ),
introduced(definition,[new_symbols(definition,[spl309_62])],[avatar_definition]) ).
fof(f75766,plain,
( sF307 = k10_relset_1(sK28,sK27,sF304,sK28)
| ~ spl309_62 ),
inference(avatar_component_clause,[],[f75764]) ).
fof(f75767,plain,
( spl309_62
| ~ spl309_47
| ~ spl309_51
| ~ spl309_54 ),
inference(avatar_split_clause,[],[f75761,f75640,f75625,f75597,f75764]) ).
fof(f75769,plain,
( m1_subset_1(sK30,k1_zfmisc_1(k2_zfmisc_1(sK27,sK28)))
| ~ spl309_47 ),
inference(resolution,[],[f73035,f75599]) ).
fof(f75771,definition,
( spl309_63
<=> m1_subset_1(sK30,k1_zfmisc_1(k2_zfmisc_1(sK27,sK28))) ),
introduced(definition,[new_symbols(definition,[spl309_63])],[avatar_definition]) ).
fof(f75773,plain,
( m1_subset_1(sK30,k1_zfmisc_1(k2_zfmisc_1(sK27,sK28)))
| ~ spl309_63 ),
inference(avatar_component_clause,[],[f75771]) ).
fof(f75774,plain,
( spl309_63
| ~ spl309_47 ),
inference(avatar_split_clause,[],[f75769,f75597,f75771]) ).
fof(f75796,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK28,X1)))
| k5_relat_1(sK30,X0) = k9_relset_2(sK27,sK28,X1,sK30,X0) )
| ~ spl309_63 ),
inference(resolution,[],[f75773,f72783]) ).
fof(f75806,plain,
( ! [X0,X1] :
( ~ m2_relset_1(X1,X0,sK27)
| k2_funct_5(k9_relset_2(X0,sK27,sK28,X1,sK30)) = k10_relset_1(sK27,sK28,sK30,k2_funct_5(X1)) )
| ~ spl309_47 ),
inference(resolution,[],[f72868,f75599]) ).
fof(f75807,plain,
( v1_relat_1(sK30)
| ~ spl309_63 ),
inference(unit_resulting_resolution,[],[f73036,f75773]) ).
fof(f75809,definition,
( spl309_68
<=> v1_relat_1(sK30) ),
introduced(definition,[new_symbols(definition,[spl309_68])],[avatar_definition]) ).
fof(f75811,plain,
( v1_relat_1(sK30)
| ~ spl309_68 ),
inference(avatar_component_clause,[],[f75809]) ).
fof(f75812,plain,
( spl309_68
| ~ spl309_63 ),
inference(avatar_split_clause,[],[f75807,f75771,f75809]) ).
fof(f75930,plain,
( m1_relset_1(sK30,sK27,sK28)
| ~ spl309_47 ),
inference(resolution,[],[f73020,f75599]) ).
fof(f75932,definition,
( spl309_74
<=> m1_relset_1(sK30,sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl309_74])],[avatar_definition]) ).
fof(f75934,plain,
( m1_relset_1(sK30,sK27,sK28)
| ~ spl309_74 ),
inference(avatar_component_clause,[],[f75932]) ).
fof(f75935,plain,
( spl309_74
| ~ spl309_47 ),
inference(avatar_split_clause,[],[f75930,f75597,f75932]) ).
fof(f75937,plain,
( m2_relset_1(k6_relset_1(sK27,sK28,sK30),sK28,sK27)
| ~ spl309_74 ),
inference(unit_resulting_resolution,[],[f74447,f75934]) ).
fof(f75943,plain,
( ! [X0] : k10_relset_1(sK27,sK28,sK30,X0) = k9_relat_1(sK30,X0)
| ~ spl309_74 ),
inference(resolution,[],[f75934,f73715]) ).
fof(f75944,plain,
( k6_relset_1(sK27,sK28,sK30) = k4_relat_1(sK30)
| ~ spl309_74 ),
inference(resolution,[],[f75934,f74445]) ).
fof(f75946,plain,
( sF304 = k4_relat_1(sK30)
| ~ spl309_51
| ~ spl309_74 ),
inference(forward_demodulation,[],[f75944,f75627]) ).
fof(f75950,plain,
( m2_relset_1(sF304,sK28,sK27)
| ~ spl309_51
| ~ spl309_74 ),
inference(forward_demodulation,[],[f75937,f75627]) ).
fof(f75953,definition,
( spl309_75
<=> sF304 = k4_relat_1(sK30) ),
introduced(definition,[new_symbols(definition,[spl309_75])],[avatar_definition]) ).
fof(f75955,plain,
( sF304 = k4_relat_1(sK30)
| ~ spl309_75 ),
inference(avatar_component_clause,[],[f75953]) ).
fof(f75956,plain,
( spl309_75
| ~ spl309_51
| ~ spl309_74 ),
inference(avatar_split_clause,[],[f75946,f75932,f75625,f75953]) ).
fof(f75964,plain,
( $false
| ~ spl309_51
| spl309_60
| ~ spl309_74 ),
inference(forward_subsumption_resolution,[],[f75950,f75749]) ).
fof(f75965,plain,
( ~ spl309_51
| spl309_60
| ~ spl309_74 ),
inference(avatar_contradiction_clause,[],[f75964]) ).
fof(f75984,plain,
( r1_tarski(k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)),k1_funct_5(sF304))
| ~ spl309_47
| ~ spl309_60 ),
inference(unit_resulting_resolution,[],[f72865,f75599,f75748]) ).
fof(f75987,plain,
( k1_funct_5(k9_relset_2(sK27,sK28,sK27,sK30,sF304)) = k10_relset_1(sK28,sK27,k6_relset_1(sK27,sK28,sK30),k1_funct_5(sF304))
| ~ spl309_47
| ~ spl309_60 ),
inference(unit_resulting_resolution,[],[f72866,f75599,f75748]) ).
fof(f75991,plain,
( k2_funct_5(k9_relset_2(sK27,sK28,sK27,sK30,sF304)) = k10_relset_1(sK28,sK27,sF304,k2_funct_5(sK30))
| ~ spl309_47
| ~ spl309_60 ),
inference(unit_resulting_resolution,[],[f72868,f75599,f75748]) ).
fof(f75995,plain,
( k2_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)) = k10_relset_1(sK27,sK28,sK30,k2_funct_5(sF304))
| ~ spl309_47
| ~ spl309_60 ),
inference(resolution,[],[f75748,f75806]) ).
fof(f75996,plain,
( k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)) = k10_relset_1(sK27,sK28,k6_relset_1(sK28,sK27,sF304),sF307)
| ~ spl309_47
| ~ spl309_54
| ~ spl309_60 ),
inference(resolution,[],[f75748,f75756]) ).
fof(f75997,plain,
( m1_relset_1(sF304,sK28,sK27)
| ~ spl309_60 ),
inference(resolution,[],[f75748,f73020]) ).
fof(f75999,plain,
( k10_relset_1(sK28,sK27,sF304,sK28) = k2_funct_5(sF304)
| ~ spl309_60 ),
inference(resolution,[],[f75748,f72863]) ).
fof(f76000,plain,
( m1_subset_1(sF304,k1_zfmisc_1(k2_zfmisc_1(sK28,sK27)))
| ~ spl309_60 ),
inference(resolution,[],[f75748,f73035]) ).
fof(f76001,plain,
( k1_funct_5(sF304) = k10_relset_1(sK27,sK28,k6_relset_1(sK28,sK27,sF304),sK27)
| ~ spl309_60 ),
inference(resolution,[],[f75748,f72864]) ).
fof(f76004,definition,
( spl309_79
<=> k1_funct_5(sF304) = k10_relset_1(sK27,sK28,k6_relset_1(sK28,sK27,sF304),sK27) ),
introduced(definition,[new_symbols(definition,[spl309_79])],[avatar_definition]) ).
fof(f76006,plain,
( k1_funct_5(sF304) = k10_relset_1(sK27,sK28,k6_relset_1(sK28,sK27,sF304),sK27)
| ~ spl309_79 ),
inference(avatar_component_clause,[],[f76004]) ).
fof(f76007,plain,
( spl309_79
| ~ spl309_60 ),
inference(avatar_split_clause,[],[f76001,f75747,f76004]) ).
fof(f76009,definition,
( spl309_80
<=> m1_subset_1(sF304,k1_zfmisc_1(k2_zfmisc_1(sK28,sK27))) ),
introduced(definition,[new_symbols(definition,[spl309_80])],[avatar_definition]) ).
fof(f76011,plain,
( m1_subset_1(sF304,k1_zfmisc_1(k2_zfmisc_1(sK28,sK27)))
| ~ spl309_80 ),
inference(avatar_component_clause,[],[f76009]) ).
fof(f76012,plain,
( spl309_80
| ~ spl309_60 ),
inference(avatar_split_clause,[],[f76000,f75747,f76009]) ).
fof(f76013,plain,
( sF307 = k2_funct_5(sF304)
| ~ spl309_60
| ~ spl309_62 ),
inference(forward_demodulation,[],[f75999,f75766]) ).
fof(f76015,definition,
( spl309_81
<=> m1_relset_1(sF304,sK28,sK27) ),
introduced(definition,[new_symbols(definition,[spl309_81])],[avatar_definition]) ).
fof(f76017,plain,
( m1_relset_1(sF304,sK28,sK27)
| ~ spl309_81 ),
inference(avatar_component_clause,[],[f76015]) ).
fof(f76018,plain,
( spl309_81
| ~ spl309_60 ),
inference(avatar_split_clause,[],[f75997,f75747,f76015]) ).
fof(f76020,definition,
( spl309_82
<=> k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)) = k10_relset_1(sK27,sK28,k6_relset_1(sK28,sK27,sF304),sF307) ),
introduced(definition,[new_symbols(definition,[spl309_82])],[avatar_definition]) ).
fof(f76022,plain,
( k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)) = k10_relset_1(sK27,sK28,k6_relset_1(sK28,sK27,sF304),sF307)
| ~ spl309_82 ),
inference(avatar_component_clause,[],[f76020]) ).
fof(f76023,plain,
( spl309_82
| ~ spl309_47
| ~ spl309_54
| ~ spl309_60 ),
inference(avatar_split_clause,[],[f75996,f75747,f75640,f75597,f76020]) ).
fof(f76024,plain,
( k2_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)) = k9_relat_1(sK30,k2_funct_5(sF304))
| ~ spl309_47
| ~ spl309_60
| ~ spl309_74 ),
inference(forward_demodulation,[],[f75995,f75943]) ).
fof(f76028,definition,
( spl309_83
<=> r1_tarski(k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)),k1_funct_5(sF304)) ),
introduced(definition,[new_symbols(definition,[spl309_83])],[avatar_definition]) ).
fof(f76030,plain,
( r1_tarski(k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)),k1_funct_5(sF304))
| ~ spl309_83 ),
inference(avatar_component_clause,[],[f76028]) ).
fof(f76031,plain,
( spl309_83
| ~ spl309_47
| ~ spl309_60 ),
inference(avatar_split_clause,[],[f75984,f75747,f75597,f76028]) ).
fof(f76034,plain,
( k1_funct_5(k9_relset_2(sK27,sK28,sK27,sK30,sF304)) = k10_relset_1(sK28,sK27,sF304,k1_funct_5(sF304))
| ~ spl309_47
| ~ spl309_51
| ~ spl309_60 ),
inference(forward_demodulation,[],[f75987,f75627]) ).
fof(f76042,plain,
( k2_funct_5(sF305) = k10_relset_1(sK28,sK27,sF304,k2_funct_5(sK30))
| ~ spl309_47
| ~ spl309_52
| ~ spl309_60 ),
inference(forward_demodulation,[],[f75991,f75632]) ).
fof(f76045,definition,
( spl309_85
<=> sF307 = k2_funct_5(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_85])],[avatar_definition]) ).
fof(f76047,plain,
( sF307 = k2_funct_5(sF304)
| ~ spl309_85 ),
inference(avatar_component_clause,[],[f76045]) ).
fof(f76048,plain,
( spl309_85
| ~ spl309_60
| ~ spl309_62 ),
inference(avatar_split_clause,[],[f76013,f75764,f75747,f76045]) ).
fof(f76050,definition,
( spl309_86
<=> k2_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)) = k9_relat_1(sK30,k2_funct_5(sF304)) ),
introduced(definition,[new_symbols(definition,[spl309_86])],[avatar_definition]) ).
fof(f76053,plain,
( spl309_86
| ~ spl309_47
| ~ spl309_60
| ~ spl309_74 ),
inference(avatar_split_clause,[],[f76024,f75932,f75747,f75597,f76050]) ).
fof(f76055,plain,
( k1_funct_5(sF305) = k10_relset_1(sK28,sK27,sF304,k1_funct_5(sF304))
| ~ spl309_47
| ~ spl309_51
| ~ spl309_52
| ~ spl309_60 ),
inference(forward_demodulation,[],[f76034,f75632]) ).
fof(f76057,definition,
( spl309_87
<=> k2_funct_5(sF305) = k10_relset_1(sK28,sK27,sF304,k2_funct_5(sK30)) ),
introduced(definition,[new_symbols(definition,[spl309_87])],[avatar_definition]) ).
fof(f76059,plain,
( k2_funct_5(sF305) = k10_relset_1(sK28,sK27,sF304,k2_funct_5(sK30))
| ~ spl309_87 ),
inference(avatar_component_clause,[],[f76057]) ).
fof(f76060,plain,
( spl309_87
| ~ spl309_47
| ~ spl309_52
| ~ spl309_60 ),
inference(avatar_split_clause,[],[f76042,f75747,f75630,f75597,f76057]) ).
fof(f76062,definition,
( spl309_88
<=> k1_funct_5(sF305) = k10_relset_1(sK28,sK27,sF304,k1_funct_5(sF304)) ),
introduced(definition,[new_symbols(definition,[spl309_88])],[avatar_definition]) ).
fof(f76064,plain,
( k1_funct_5(sF305) = k10_relset_1(sK28,sK27,sF304,k1_funct_5(sF304))
| ~ spl309_88 ),
inference(avatar_component_clause,[],[f76062]) ).
fof(f76065,plain,
( spl309_88
| ~ spl309_47
| ~ spl309_51
| ~ spl309_52
| ~ spl309_60 ),
inference(avatar_split_clause,[],[f76055,f75747,f75630,f75625,f75597,f76062]) ).
fof(f76130,plain,
( ~ r1_tarski(sF306,sF307)
| spl309_48
| ~ spl309_49 ),
inference(unit_resulting_resolution,[],[f73635,f75608,f75603]) ).
fof(f76147,definition,
( spl309_95
<=> r1_tarski(sF306,sF307) ),
introduced(definition,[new_symbols(definition,[spl309_95])],[avatar_definition]) ).
fof(f76149,plain,
( ~ r1_tarski(sF306,sF307)
| spl309_95 ),
inference(avatar_component_clause,[],[f76147]) ).
fof(f76150,plain,
( ~ spl309_95
| spl309_48
| ~ spl309_49 ),
inference(avatar_split_clause,[],[f76130,f75606,f75602,f76147]) ).
fof(f76163,plain,
( m2_relset_1(k6_relset_1(sK28,sK27,sF304),sK27,sK28)
| ~ spl309_81 ),
inference(resolution,[],[f76017,f74447]) ).
fof(f76164,plain,
( ! [X0] : k10_relset_1(sK28,sK27,sF304,X0) = k9_relat_1(sF304,X0)
| ~ spl309_81 ),
inference(resolution,[],[f76017,f73715]) ).
fof(f76165,plain,
( k6_relset_1(sK28,sK27,sF304) = k4_relat_1(sF304)
| ~ spl309_81 ),
inference(resolution,[],[f76017,f74445]) ).
fof(f76169,definition,
( spl309_97
<=> k6_relset_1(sK28,sK27,sF304) = k4_relat_1(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_97])],[avatar_definition]) ).
fof(f76171,plain,
( k6_relset_1(sK28,sK27,sF304) = k4_relat_1(sF304)
| ~ spl309_97 ),
inference(avatar_component_clause,[],[f76169]) ).
fof(f76172,plain,
( spl309_97
| ~ spl309_81 ),
inference(avatar_split_clause,[],[f76165,f76015,f76169]) ).
fof(f76174,definition,
( spl309_98
<=> m2_relset_1(k6_relset_1(sK28,sK27,sF304),sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl309_98])],[avatar_definition]) ).
fof(f76176,plain,
( m2_relset_1(k6_relset_1(sK28,sK27,sF304),sK27,sK28)
| ~ spl309_98 ),
inference(avatar_component_clause,[],[f76174]) ).
fof(f76177,plain,
( spl309_98
| ~ spl309_81 ),
inference(avatar_split_clause,[],[f76163,f76015,f76174]) ).
fof(f76186,plain,
( m2_relset_1(k4_relat_1(sF304),sK27,sK28)
| ~ spl309_97
| ~ spl309_98 ),
inference(forward_demodulation,[],[f76176,f76171]) ).
fof(f76189,definition,
( spl309_100
<=> m2_relset_1(k4_relat_1(sF304),sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl309_100])],[avatar_definition]) ).
fof(f76191,plain,
( m2_relset_1(k4_relat_1(sF304),sK27,sK28)
| ~ spl309_100 ),
inference(avatar_component_clause,[],[f76189]) ).
fof(f76192,plain,
( spl309_100
| ~ spl309_97
| ~ spl309_98 ),
inference(avatar_split_clause,[],[f76186,f76174,f76169,f76189]) ).
fof(f76201,plain,
( k1_funct_5(sF305) = k9_relat_1(sF304,k1_funct_5(sF304))
| ~ spl309_81
| ~ spl309_88 ),
inference(superposition,[],[f76064,f76164]) ).
fof(f76203,definition,
( spl309_102
<=> k1_funct_5(sF305) = k9_relat_1(sF304,k1_funct_5(sF304)) ),
introduced(definition,[new_symbols(definition,[spl309_102])],[avatar_definition]) ).
fof(f76205,plain,
( k1_funct_5(sF305) = k9_relat_1(sF304,k1_funct_5(sF304))
| ~ spl309_102 ),
inference(avatar_component_clause,[],[f76203]) ).
fof(f76206,plain,
( spl309_102
| ~ spl309_81
| ~ spl309_88 ),
inference(avatar_split_clause,[],[f76201,f76062,f76015,f76203]) ).
fof(f76235,plain,
( v1_relat_1(sF304)
| ~ spl309_80 ),
inference(unit_resulting_resolution,[],[f73036,f76011]) ).
fof(f76236,plain,
( m2_relset_1(k9_relset_2(sK27,sK28,sK27,sK30,sF304),sK27,sK27)
| ~ spl309_63
| ~ spl309_80 ),
inference(unit_resulting_resolution,[],[f72782,f75773,f76011]) ).
fof(f76239,plain,
( k9_relset_2(sK28,sK27,sK28,sF304,sK30) = k5_relat_1(sF304,sK30)
| ~ spl309_63
| ~ spl309_80 ),
inference(unit_resulting_resolution,[],[f72783,f75773,f76011]) ).
fof(f76241,plain,
( k9_relset_2(sK27,sK28,sK27,sK30,sF304) = k5_relat_1(sK30,sF304)
| ~ spl309_63
| ~ spl309_80 ),
inference(resolution,[],[f76011,f75796]) ).
fof(f76244,plain,
( sF305 = k5_relat_1(sK30,sF304)
| ~ spl309_52
| ~ spl309_63
| ~ spl309_80 ),
inference(forward_demodulation,[],[f76241,f75632]) ).
fof(f76247,definition,
( spl309_106
<=> v1_relat_1(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_106])],[avatar_definition]) ).
fof(f76249,plain,
( v1_relat_1(sF304)
| ~ spl309_106 ),
inference(avatar_component_clause,[],[f76247]) ).
fof(f76250,plain,
( spl309_106
| ~ spl309_80 ),
inference(avatar_split_clause,[],[f76235,f76009,f76247]) ).
fof(f76251,plain,
( m2_relset_1(sF305,sK27,sK27)
| ~ spl309_52
| ~ spl309_63
| ~ spl309_80 ),
inference(forward_demodulation,[],[f76236,f75632]) ).
fof(f76259,definition,
( spl309_108
<=> k9_relset_2(sK28,sK27,sK28,sF304,sK30) = k5_relat_1(sF304,sK30) ),
introduced(definition,[new_symbols(definition,[spl309_108])],[avatar_definition]) ).
fof(f76261,plain,
( k9_relset_2(sK28,sK27,sK28,sF304,sK30) = k5_relat_1(sF304,sK30)
| ~ spl309_108 ),
inference(avatar_component_clause,[],[f76259]) ).
fof(f76262,plain,
( spl309_108
| ~ spl309_63
| ~ spl309_80 ),
inference(avatar_split_clause,[],[f76239,f76009,f75771,f76259]) ).
fof(f76269,definition,
( spl309_110
<=> sF305 = k5_relat_1(sK30,sF304) ),
introduced(definition,[new_symbols(definition,[spl309_110])],[avatar_definition]) ).
fof(f76271,plain,
( sF305 = k5_relat_1(sK30,sF304)
| ~ spl309_110 ),
inference(avatar_component_clause,[],[f76269]) ).
fof(f76272,plain,
( spl309_110
| ~ spl309_52
| ~ spl309_63
| ~ spl309_80 ),
inference(avatar_split_clause,[],[f76244,f76009,f75771,f75630,f76269]) ).
fof(f76274,definition,
( spl309_111
<=> m2_relset_1(sF305,sK27,sK27) ),
introduced(definition,[new_symbols(definition,[spl309_111])],[avatar_definition]) ).
fof(f76276,plain,
( m2_relset_1(sF305,sK27,sK27)
| ~ spl309_111 ),
inference(avatar_component_clause,[],[f76274]) ).
fof(f76277,plain,
( spl309_111
| ~ spl309_52
| ~ spl309_63
| ~ spl309_80 ),
inference(avatar_split_clause,[],[f76251,f76009,f75771,f75630,f76274]) ).
fof(f76282,plain,
( r1_tarski(k1_funct_5(k9_relset_2(sK27,sK27,sK28,sF305,sK30)),k1_funct_5(sF305))
| ~ spl309_47
| ~ spl309_111 ),
inference(unit_resulting_resolution,[],[f72865,f75599,f76276]) ).
fof(f76300,plain,
( k2_funct_5(k9_relset_2(sK27,sK27,sK28,sF305,sK30)) = k10_relset_1(sK27,sK28,sK30,k2_funct_5(sF305))
| ~ spl309_47
| ~ spl309_111 ),
inference(resolution,[],[f76276,f75806]) ).
fof(f76301,plain,
( k1_funct_5(k9_relset_2(sK27,sK27,sK28,sF305,sK30)) = k10_relset_1(sK27,sK27,k6_relset_1(sK27,sK27,sF305),sF307)
| ~ spl309_47
| ~ spl309_54
| ~ spl309_111 ),
inference(resolution,[],[f76276,f75756]) ).
fof(f76302,plain,
( m1_relset_1(sF305,sK27,sK27)
| ~ spl309_111 ),
inference(resolution,[],[f76276,f73020]) ).
fof(f76304,plain,
( k2_funct_5(sF305) = k10_relset_1(sK27,sK27,sF305,sK27)
| ~ spl309_111 ),
inference(resolution,[],[f76276,f72863]) ).
fof(f76305,plain,
( m1_subset_1(sF305,k1_zfmisc_1(k2_zfmisc_1(sK27,sK27)))
| ~ spl309_111 ),
inference(resolution,[],[f76276,f73035]) ).
fof(f76306,plain,
( k1_funct_5(sF305) = k10_relset_1(sK27,sK27,k6_relset_1(sK27,sK27,sF305),sK27)
| ~ spl309_111 ),
inference(resolution,[],[f76276,f72864]) ).
fof(f76309,definition,
( spl309_112
<=> k1_funct_5(sF305) = k10_relset_1(sK27,sK27,k6_relset_1(sK27,sK27,sF305),sK27) ),
introduced(definition,[new_symbols(definition,[spl309_112])],[avatar_definition]) ).
fof(f76311,plain,
( k1_funct_5(sF305) = k10_relset_1(sK27,sK27,k6_relset_1(sK27,sK27,sF305),sK27)
| ~ spl309_112 ),
inference(avatar_component_clause,[],[f76309]) ).
fof(f76312,plain,
( spl309_112
| ~ spl309_111 ),
inference(avatar_split_clause,[],[f76306,f76274,f76309]) ).
fof(f76314,definition,
( spl309_113
<=> m1_subset_1(sF305,k1_zfmisc_1(k2_zfmisc_1(sK27,sK27))) ),
introduced(definition,[new_symbols(definition,[spl309_113])],[avatar_definition]) ).
fof(f76316,plain,
( m1_subset_1(sF305,k1_zfmisc_1(k2_zfmisc_1(sK27,sK27)))
| ~ spl309_113 ),
inference(avatar_component_clause,[],[f76314]) ).
fof(f76317,plain,
( spl309_113
| ~ spl309_111 ),
inference(avatar_split_clause,[],[f76305,f76274,f76314]) ).
fof(f76319,definition,
( spl309_114
<=> k2_funct_5(sF305) = k10_relset_1(sK27,sK27,sF305,sK27) ),
introduced(definition,[new_symbols(definition,[spl309_114])],[avatar_definition]) ).
fof(f76321,plain,
( k2_funct_5(sF305) = k10_relset_1(sK27,sK27,sF305,sK27)
| ~ spl309_114 ),
inference(avatar_component_clause,[],[f76319]) ).
fof(f76322,plain,
( spl309_114
| ~ spl309_111 ),
inference(avatar_split_clause,[],[f76304,f76274,f76319]) ).
fof(f76324,definition,
( spl309_115
<=> m1_relset_1(sF305,sK27,sK27) ),
introduced(definition,[new_symbols(definition,[spl309_115])],[avatar_definition]) ).
fof(f76326,plain,
( m1_relset_1(sF305,sK27,sK27)
| ~ spl309_115 ),
inference(avatar_component_clause,[],[f76324]) ).
fof(f76327,plain,
( spl309_115
| ~ spl309_111 ),
inference(avatar_split_clause,[],[f76302,f76274,f76324]) ).
fof(f76329,definition,
( spl309_116
<=> k1_funct_5(k9_relset_2(sK27,sK27,sK28,sF305,sK30)) = k10_relset_1(sK27,sK27,k6_relset_1(sK27,sK27,sF305),sF307) ),
introduced(definition,[new_symbols(definition,[spl309_116])],[avatar_definition]) ).
fof(f76331,plain,
( k1_funct_5(k9_relset_2(sK27,sK27,sK28,sF305,sK30)) = k10_relset_1(sK27,sK27,k6_relset_1(sK27,sK27,sF305),sF307)
| ~ spl309_116 ),
inference(avatar_component_clause,[],[f76329]) ).
fof(f76332,plain,
( spl309_116
| ~ spl309_47
| ~ spl309_54
| ~ spl309_111 ),
inference(avatar_split_clause,[],[f76301,f76274,f75640,f75597,f76329]) ).
fof(f76333,plain,
( k2_funct_5(k9_relset_2(sK27,sK27,sK28,sF305,sK30)) = k9_relat_1(sK30,k2_funct_5(sF305))
| ~ spl309_47
| ~ spl309_74
| ~ spl309_111 ),
inference(forward_demodulation,[],[f76300,f75943]) ).
fof(f76336,definition,
( spl309_117
<=> r1_tarski(k1_funct_5(k9_relset_2(sK27,sK27,sK28,sF305,sK30)),k1_funct_5(sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_117])],[avatar_definition]) ).
fof(f76338,plain,
( r1_tarski(k1_funct_5(k9_relset_2(sK27,sK27,sK28,sF305,sK30)),k1_funct_5(sF305))
| ~ spl309_117 ),
inference(avatar_component_clause,[],[f76336]) ).
fof(f76339,plain,
( spl309_117
| ~ spl309_47
| ~ spl309_111 ),
inference(avatar_split_clause,[],[f76282,f76274,f75597,f76336]) ).
fof(f76380,definition,
( spl309_125
<=> k2_funct_5(k9_relset_2(sK27,sK27,sK28,sF305,sK30)) = k9_relat_1(sK30,k2_funct_5(sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_125])],[avatar_definition]) ).
fof(f76382,plain,
( k2_funct_5(k9_relset_2(sK27,sK27,sK28,sF305,sK30)) = k9_relat_1(sK30,k2_funct_5(sF305))
| ~ spl309_125 ),
inference(avatar_component_clause,[],[f76380]) ).
fof(f76383,plain,
( spl309_125
| ~ spl309_47
| ~ spl309_74
| ~ spl309_111 ),
inference(avatar_split_clause,[],[f76333,f76274,f75932,f75597,f76380]) ).
fof(f76407,plain,
( sF305 = k6_relset_1(sK27,sK27,k6_relset_1(sK27,sK27,sF305))
| ~ spl309_115 ),
inference(resolution,[],[f76326,f74446]) ).
fof(f76408,plain,
( m2_relset_1(k6_relset_1(sK27,sK27,sF305),sK27,sK27)
| ~ spl309_115 ),
inference(resolution,[],[f76326,f74447]) ).
fof(f76409,plain,
( ! [X0] : k10_relset_1(sK27,sK27,sF305,X0) = k9_relat_1(sF305,X0)
| ~ spl309_115 ),
inference(resolution,[],[f76326,f73715]) ).
fof(f76410,plain,
( k6_relset_1(sK27,sK27,sF305) = k4_relat_1(sF305)
| ~ spl309_115 ),
inference(resolution,[],[f76326,f74445]) ).
fof(f76414,definition,
( spl309_128
<=> k6_relset_1(sK27,sK27,sF305) = k4_relat_1(sF305) ),
introduced(definition,[new_symbols(definition,[spl309_128])],[avatar_definition]) ).
fof(f76416,plain,
( k6_relset_1(sK27,sK27,sF305) = k4_relat_1(sF305)
| ~ spl309_128 ),
inference(avatar_component_clause,[],[f76414]) ).
fof(f76417,plain,
( spl309_128
| ~ spl309_115 ),
inference(avatar_split_clause,[],[f76410,f76324,f76414]) ).
fof(f76419,definition,
( spl309_129
<=> m2_relset_1(k6_relset_1(sK27,sK27,sF305),sK27,sK27) ),
introduced(definition,[new_symbols(definition,[spl309_129])],[avatar_definition]) ).
fof(f76421,plain,
( m2_relset_1(k6_relset_1(sK27,sK27,sF305),sK27,sK27)
| ~ spl309_129 ),
inference(avatar_component_clause,[],[f76419]) ).
fof(f76422,plain,
( spl309_129
| ~ spl309_115 ),
inference(avatar_split_clause,[],[f76408,f76324,f76419]) ).
fof(f76424,definition,
( spl309_130
<=> sF305 = k6_relset_1(sK27,sK27,k6_relset_1(sK27,sK27,sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_130])],[avatar_definition]) ).
fof(f76426,plain,
( sF305 = k6_relset_1(sK27,sK27,k6_relset_1(sK27,sK27,sF305))
| ~ spl309_130 ),
inference(avatar_component_clause,[],[f76424]) ).
fof(f76427,plain,
( spl309_130
| ~ spl309_115 ),
inference(avatar_split_clause,[],[f76407,f76324,f76424]) ).
fof(f76431,plain,
( m2_relset_1(k4_relat_1(sF305),sK27,sK27)
| ~ spl309_128
| ~ spl309_129 ),
inference(forward_demodulation,[],[f76421,f76416]) ).
fof(f76432,plain,
( sF305 = k6_relset_1(sK27,sK27,k4_relat_1(sF305))
| ~ spl309_128
| ~ spl309_130 ),
inference(forward_demodulation,[],[f76426,f76416]) ).
fof(f76434,definition,
( spl309_131
<=> m2_relset_1(k4_relat_1(sF305),sK27,sK27) ),
introduced(definition,[new_symbols(definition,[spl309_131])],[avatar_definition]) ).
fof(f76436,plain,
( m2_relset_1(k4_relat_1(sF305),sK27,sK27)
| ~ spl309_131 ),
inference(avatar_component_clause,[],[f76434]) ).
fof(f76437,plain,
( spl309_131
| ~ spl309_128
| ~ spl309_129 ),
inference(avatar_split_clause,[],[f76431,f76419,f76414,f76434]) ).
fof(f76439,definition,
( spl309_132
<=> sF305 = k6_relset_1(sK27,sK27,k4_relat_1(sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_132])],[avatar_definition]) ).
fof(f76441,plain,
( sF305 = k6_relset_1(sK27,sK27,k4_relat_1(sF305))
| ~ spl309_132 ),
inference(avatar_component_clause,[],[f76439]) ).
fof(f76442,plain,
( spl309_132
| ~ spl309_128
| ~ spl309_130 ),
inference(avatar_split_clause,[],[f76432,f76424,f76414,f76439]) ).
fof(f76444,plain,
( sF306 = k9_relat_1(sF305,sK29)
| ~ spl309_53
| ~ spl309_115 ),
inference(superposition,[],[f75637,f76409]) ).
fof(f76446,definition,
( spl309_133
<=> sF306 = k9_relat_1(sF305,sK29) ),
introduced(definition,[new_symbols(definition,[spl309_133])],[avatar_definition]) ).
fof(f76448,plain,
( sF306 = k9_relat_1(sF305,sK29)
| ~ spl309_133 ),
inference(avatar_component_clause,[],[f76446]) ).
fof(f76449,plain,
( spl309_133
| ~ spl309_53
| ~ spl309_115 ),
inference(avatar_split_clause,[],[f76444,f76324,f75635,f76446]) ).
fof(f76545,definition,
( spl309_141
<=> r1_tarski(sF307,k1_funct_5(sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_141])],[avatar_definition]) ).
fof(f76546,plain,
( r1_tarski(sF307,k1_funct_5(sF305))
| ~ spl309_141 ),
inference(avatar_component_clause,[],[f76545]) ).
fof(f76547,plain,
( ~ r1_tarski(sF307,k1_funct_5(sF305))
| spl309_141 ),
inference(avatar_component_clause,[],[f76545]) ).
fof(f76550,plain,
( v1_relat_1(sF305)
| ~ spl309_113 ),
inference(unit_resulting_resolution,[],[f73036,f76316]) ).
fof(f76553,plain,
( m2_relset_1(k9_relset_2(sK27,sK27,sK28,sF305,sK30),sK27,sK28)
| ~ spl309_63
| ~ spl309_113 ),
inference(unit_resulting_resolution,[],[f72782,f75773,f76316]) ).
fof(f76557,plain,
( k9_relset_2(sK27,sK27,sK28,sF305,sK30) = k5_relat_1(sF305,sK30)
| ~ spl309_63
| ~ spl309_113 ),
inference(unit_resulting_resolution,[],[f72783,f75773,f76316]) ).
fof(f76569,definition,
( spl309_143
<=> v1_relat_1(sF305) ),
introduced(definition,[new_symbols(definition,[spl309_143])],[avatar_definition]) ).
fof(f76571,plain,
( v1_relat_1(sF305)
| ~ spl309_143 ),
inference(avatar_component_clause,[],[f76569]) ).
fof(f76572,plain,
( spl309_143
| ~ spl309_113 ),
inference(avatar_split_clause,[],[f76550,f76314,f76569]) ).
fof(f76584,definition,
( spl309_146
<=> m2_relset_1(k9_relset_2(sK27,sK27,sK28,sF305,sK30),sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl309_146])],[avatar_definition]) ).
fof(f76586,plain,
( m2_relset_1(k9_relset_2(sK27,sK27,sK28,sF305,sK30),sK27,sK28)
| ~ spl309_146 ),
inference(avatar_component_clause,[],[f76584]) ).
fof(f76587,plain,
( spl309_146
| ~ spl309_63
| ~ spl309_113 ),
inference(avatar_split_clause,[],[f76553,f76314,f75771,f76584]) ).
fof(f76594,definition,
( spl309_148
<=> k9_relset_2(sK27,sK27,sK28,sF305,sK30) = k5_relat_1(sF305,sK30) ),
introduced(definition,[new_symbols(definition,[spl309_148])],[avatar_definition]) ).
fof(f76596,plain,
( k9_relset_2(sK27,sK27,sK28,sF305,sK30) = k5_relat_1(sF305,sK30)
| ~ spl309_148 ),
inference(avatar_component_clause,[],[f76594]) ).
fof(f76597,plain,
( spl309_148
| ~ spl309_63
| ~ spl309_113 ),
inference(avatar_split_clause,[],[f76557,f76314,f75771,f76594]) ).
fof(f76684,plain,
( k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)) = k10_relset_1(sK27,sK28,k4_relat_1(sF304),sF307)
| ~ spl309_82
| ~ spl309_97 ),
inference(superposition,[],[f76022,f76171]) ).
fof(f76686,plain,
( k10_relset_1(sK27,sK28,k4_relat_1(sF304),sF307) = k1_funct_5(k5_relat_1(sF304,sK30))
| ~ spl309_82
| ~ spl309_97
| ~ spl309_108 ),
inference(forward_demodulation,[],[f76684,f76261]) ).
fof(f76688,definition,
( spl309_154
<=> k10_relset_1(sK27,sK28,k4_relat_1(sF304),sF307) = k1_funct_5(k5_relat_1(sF304,sK30)) ),
introduced(definition,[new_symbols(definition,[spl309_154])],[avatar_definition]) ).
fof(f76690,plain,
( k10_relset_1(sK27,sK28,k4_relat_1(sF304),sF307) = k1_funct_5(k5_relat_1(sF304,sK30))
| ~ spl309_154 ),
inference(avatar_component_clause,[],[f76688]) ).
fof(f76691,plain,
( spl309_154
| ~ spl309_82
| ~ spl309_97
| ~ spl309_108 ),
inference(avatar_split_clause,[],[f76686,f76259,f76169,f76020,f76688]) ).
fof(f76706,plain,
( k1_funct_5(sF304) = k10_relset_1(sK27,sK28,k4_relat_1(sF304),sK27)
| ~ spl309_79
| ~ spl309_97 ),
inference(superposition,[],[f76006,f76171]) ).
fof(f76708,definition,
( spl309_155
<=> k1_funct_5(sF304) = k10_relset_1(sK27,sK28,k4_relat_1(sF304),sK27) ),
introduced(definition,[new_symbols(definition,[spl309_155])],[avatar_definition]) ).
fof(f76710,plain,
( k1_funct_5(sF304) = k10_relset_1(sK27,sK28,k4_relat_1(sF304),sK27)
| ~ spl309_155 ),
inference(avatar_component_clause,[],[f76708]) ).
fof(f76711,plain,
( spl309_155
| ~ spl309_79
| ~ spl309_97 ),
inference(avatar_split_clause,[],[f76706,f76169,f76004,f76708]) ).
fof(f76727,plain,
( k2_funct_5(sF305) = k9_relat_1(sF304,k2_funct_5(sK30))
| ~ spl309_81
| ~ spl309_87 ),
inference(superposition,[],[f76164,f76059]) ).
fof(f76729,definition,
( spl309_158
<=> k2_funct_5(sF305) = k9_relat_1(sF304,k2_funct_5(sK30)) ),
introduced(definition,[new_symbols(definition,[spl309_158])],[avatar_definition]) ).
fof(f76731,plain,
( k2_funct_5(sF305) = k9_relat_1(sF304,k2_funct_5(sK30))
| ~ spl309_158 ),
inference(avatar_component_clause,[],[f76729]) ).
fof(f76732,plain,
( spl309_158
| ~ spl309_81
| ~ spl309_87 ),
inference(avatar_split_clause,[],[f76727,f76057,f76015,f76729]) ).
fof(f76733,plain,
( k1_funct_5(k9_relset_2(sK27,sK27,sK28,sF305,sK30)) = k10_relset_1(sK27,sK27,k4_relat_1(sF305),sF307)
| ~ spl309_116
| ~ spl309_128 ),
inference(superposition,[],[f76331,f76416]) ).
fof(f76736,plain,
( k10_relset_1(sK27,sK27,k4_relat_1(sF305),sF307) = k1_funct_5(k5_relat_1(sF305,sK30))
| ~ spl309_116
| ~ spl309_128
| ~ spl309_148 ),
inference(forward_demodulation,[],[f76733,f76596]) ).
fof(f76739,definition,
( spl309_159
<=> k10_relset_1(sK27,sK27,k4_relat_1(sF305),sF307) = k1_funct_5(k5_relat_1(sF305,sK30)) ),
introduced(definition,[new_symbols(definition,[spl309_159])],[avatar_definition]) ).
fof(f76741,plain,
( k10_relset_1(sK27,sK27,k4_relat_1(sF305),sF307) = k1_funct_5(k5_relat_1(sF305,sK30))
| ~ spl309_159 ),
inference(avatar_component_clause,[],[f76739]) ).
fof(f76742,plain,
( spl309_159
| ~ spl309_116
| ~ spl309_128
| ~ spl309_148 ),
inference(avatar_split_clause,[],[f76736,f76594,f76414,f76329,f76739]) ).
fof(f76754,plain,
( k1_funct_5(sF305) = k10_relset_1(sK27,sK27,k4_relat_1(sF305),sK27)
| ~ spl309_112
| ~ spl309_128 ),
inference(superposition,[],[f76311,f76416]) ).
fof(f76756,definition,
( spl309_162
<=> k1_funct_5(sF305) = k10_relset_1(sK27,sK27,k4_relat_1(sF305),sK27) ),
introduced(definition,[new_symbols(definition,[spl309_162])],[avatar_definition]) ).
fof(f76758,plain,
( k1_funct_5(sF305) = k10_relset_1(sK27,sK27,k4_relat_1(sF305),sK27)
| ~ spl309_162 ),
inference(avatar_component_clause,[],[f76756]) ).
fof(f76759,plain,
( spl309_162
| ~ spl309_112
| ~ spl309_128 ),
inference(avatar_split_clause,[],[f76754,f76414,f76309,f76756]) ).
fof(f77076,plain,
( r1_tarski(k9_relat_1(sK30,k2_funct_5(sF305)),k2_funct_5(sK30))
| ~ m2_relset_1(sK30,sK27,sK28)
| ~ m2_relset_1(sF305,sK27,sK27)
| ~ spl309_125 ),
inference(superposition,[],[f72867,f76382]) ).
fof(f77079,plain,
( r1_tarski(k9_relat_1(sK30,k2_funct_5(sF305)),k2_funct_5(sK30))
| ~ m2_relset_1(sF305,sK27,sK27)
| ~ spl309_47
| ~ spl309_125 ),
inference(forward_subsumption_resolution,[],[f77076,f75599]) ).
fof(f77081,plain,
( r1_tarski(k9_relat_1(sK30,k2_funct_5(sF305)),k2_funct_5(sK30))
| ~ spl309_47
| ~ spl309_111
| ~ spl309_125 ),
inference(forward_subsumption_resolution,[],[f77079,f76276]) ).
fof(f77083,definition,
( spl309_185
<=> r1_tarski(k9_relat_1(sK30,k2_funct_5(sF305)),k2_funct_5(sK30)) ),
introduced(definition,[new_symbols(definition,[spl309_185])],[avatar_definition]) ).
fof(f77085,plain,
( r1_tarski(k9_relat_1(sK30,k2_funct_5(sF305)),k2_funct_5(sK30))
| ~ spl309_185 ),
inference(avatar_component_clause,[],[f77083]) ).
fof(f77086,plain,
( spl309_185
| ~ spl309_47
| ~ spl309_111
| ~ spl309_125 ),
inference(avatar_split_clause,[],[f77081,f76380,f76274,f75597,f77083]) ).
fof(f77347,plain,
( r1_tarski(k9_relat_1(sF304,k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30))),k9_relat_1(sF304,k1_funct_5(sF304)))
| ~ spl309_83
| ~ spl309_106 ),
inference(unit_resulting_resolution,[],[f73125,f76249,f76030]) ).
fof(f77359,plain,
( r1_tarski(k9_relat_1(sF304,k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30))),k1_funct_5(sF305))
| ~ spl309_83
| ~ spl309_102
| ~ spl309_106 ),
inference(forward_demodulation,[],[f77347,f76205]) ).
fof(f77377,plain,
( r1_tarski(k9_relat_1(sF304,k1_funct_5(k5_relat_1(sF304,sK30))),k1_funct_5(sF305))
| ~ spl309_83
| ~ spl309_102
| ~ spl309_106
| ~ spl309_108 ),
inference(forward_demodulation,[],[f77359,f76261]) ).
fof(f77383,definition,
( spl309_204
<=> r1_tarski(k9_relat_1(sF304,k1_funct_5(k5_relat_1(sF304,sK30))),k1_funct_5(sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_204])],[avatar_definition]) ).
fof(f77386,plain,
( spl309_204
| ~ spl309_83
| ~ spl309_102
| ~ spl309_106
| ~ spl309_108 ),
inference(avatar_split_clause,[],[f77377,f76259,f76247,f76203,f76028,f77383]) ).
fof(f77868,plain,
( ~ r1_tarski(sF307,k1_funct_5(k9_relset_2(sK27,sK27,sK28,sF305,sK30)))
| ~ spl309_117
| spl309_141 ),
inference(unit_resulting_resolution,[],[f73635,f76547,f76338]) ).
fof(f77888,plain,
( ~ r1_tarski(sF307,k1_funct_5(k5_relat_1(sF305,sK30)))
| ~ spl309_117
| spl309_141
| ~ spl309_148 ),
inference(forward_demodulation,[],[f77868,f76596]) ).
fof(f77928,definition,
( spl309_255
<=> r1_tarski(sF307,k1_funct_5(k5_relat_1(sF305,sK30))) ),
introduced(definition,[new_symbols(definition,[spl309_255])],[avatar_definition]) ).
fof(f77931,plain,
( ~ spl309_255
| ~ spl309_117
| spl309_141
| ~ spl309_148 ),
inference(avatar_split_clause,[],[f77888,f76594,f76545,f76336,f77928]) ).
fof(f77989,plain,
( sK29 = k4_xboole_0(sK29,k4_xboole_0(sK29,sF307))
| ~ spl309_48 ),
inference(unit_resulting_resolution,[],[f74564,f75604]) ).
fof(f78017,definition,
( spl309_262
<=> sK29 = k4_xboole_0(sK29,k4_xboole_0(sK29,sF307)) ),
introduced(definition,[new_symbols(definition,[spl309_262])],[avatar_definition]) ).
fof(f78019,plain,
( sK29 = k4_xboole_0(sK29,k4_xboole_0(sK29,sF307))
| ~ spl309_262 ),
inference(avatar_component_clause,[],[f78017]) ).
fof(f78020,plain,
( spl309_262
| ~ spl309_48 ),
inference(avatar_split_clause,[],[f77989,f75602,f78017]) ).
fof(f78144,plain,
( k2_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,k4_relat_1(sF304))) = k10_relset_1(sK27,sK28,k4_relat_1(sF304),k2_funct_5(sF304))
| ~ spl309_60
| ~ spl309_100 ),
inference(unit_resulting_resolution,[],[f72868,f75748,f76191]) ).
fof(f78151,plain,
( k10_relset_1(sK27,sK28,k4_relat_1(sF304),sK27) = k2_funct_5(k4_relat_1(sF304))
| ~ spl309_100 ),
inference(resolution,[],[f76191,f72863]) ).
fof(f78165,plain,
( k1_funct_5(sF304) = k2_funct_5(k4_relat_1(sF304))
| ~ spl309_100
| ~ spl309_155 ),
inference(forward_demodulation,[],[f78151,f76710]) ).
fof(f78206,plain,
( k10_relset_1(sK27,sK28,k4_relat_1(sF304),sF307) = k2_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,k4_relat_1(sF304)))
| ~ spl309_60
| ~ spl309_85
| ~ spl309_100 ),
inference(forward_demodulation,[],[f78144,f76047]) ).
fof(f78213,definition,
( spl309_282
<=> k1_funct_5(sF304) = k2_funct_5(k4_relat_1(sF304)) ),
introduced(definition,[new_symbols(definition,[spl309_282])],[avatar_definition]) ).
fof(f78215,plain,
( k1_funct_5(sF304) = k2_funct_5(k4_relat_1(sF304))
| ~ spl309_282 ),
inference(avatar_component_clause,[],[f78213]) ).
fof(f78216,plain,
( spl309_282
| ~ spl309_100
| ~ spl309_155 ),
inference(avatar_split_clause,[],[f78165,f76708,f76189,f78213]) ).
fof(f78237,plain,
( k1_funct_5(k5_relat_1(sF304,sK30)) = k2_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,k4_relat_1(sF304)))
| ~ spl309_60
| ~ spl309_85
| ~ spl309_100
| ~ spl309_154 ),
inference(forward_demodulation,[],[f78206,f76690]) ).
fof(f78239,definition,
( spl309_287
<=> k1_funct_5(k5_relat_1(sF304,sK30)) = k2_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,k4_relat_1(sF304))) ),
introduced(definition,[new_symbols(definition,[spl309_287])],[avatar_definition]) ).
fof(f78242,plain,
( spl309_287
| ~ spl309_60
| ~ spl309_85
| ~ spl309_100
| ~ spl309_154 ),
inference(avatar_split_clause,[],[f78237,f76688,f76189,f76045,f75747,f78239]) ).
fof(f78262,plain,
( sK30 = k4_relat_1(sF304)
| ~ v1_relat_1(sK30)
| ~ spl309_75 ),
inference(superposition,[],[f74350,f75955]) ).
fof(f78263,plain,
( sK30 = k4_relat_1(sF304)
| ~ spl309_68
| ~ spl309_75 ),
inference(forward_subsumption_resolution,[],[f78262,f75811]) ).
fof(f78276,definition,
( spl309_291
<=> sK30 = k4_relat_1(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_291])],[avatar_definition]) ).
fof(f78278,plain,
( sK30 = k4_relat_1(sF304)
| ~ spl309_291 ),
inference(avatar_component_clause,[],[f78276]) ).
fof(f78279,plain,
( spl309_291
| ~ spl309_68
| ~ spl309_75 ),
inference(avatar_split_clause,[],[f78263,f75953,f75809,f78276]) ).
fof(f78280,plain,
( k2_funct_5(sK30) = k1_funct_5(sF304)
| ~ spl309_282
| ~ spl309_291 ),
inference(superposition,[],[f78215,f78278]) ).
fof(f78284,definition,
( spl309_292
<=> k2_funct_5(sK30) = k1_funct_5(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_292])],[avatar_definition]) ).
fof(f78286,plain,
( k2_funct_5(sK30) = k1_funct_5(sF304)
| ~ spl309_292 ),
inference(avatar_component_clause,[],[f78284]) ).
fof(f78287,plain,
( spl309_292
| ~ spl309_282
| ~ spl309_291 ),
inference(avatar_split_clause,[],[f78280,f78276,f78213,f78284]) ).
fof(f78289,plain,
( k2_funct_5(sF305) = k10_relset_1(sK28,sK27,sF304,k1_funct_5(sF304))
| ~ spl309_87
| ~ spl309_292 ),
inference(superposition,[],[f76059,f78286]) ).
fof(f78291,plain,
( k1_funct_5(sF305) = k2_funct_5(sF305)
| ~ spl309_87
| ~ spl309_88
| ~ spl309_292 ),
inference(forward_demodulation,[],[f78289,f76064]) ).
fof(f78294,definition,
( spl309_293
<=> k1_funct_5(sF305) = k2_funct_5(sF305) ),
introduced(definition,[new_symbols(definition,[spl309_293])],[avatar_definition]) ).
fof(f78296,plain,
( k1_funct_5(sF305) = k2_funct_5(sF305)
| ~ spl309_293 ),
inference(avatar_component_clause,[],[f78294]) ).
fof(f78297,plain,
( spl309_293
| ~ spl309_87
| ~ spl309_88
| ~ spl309_292 ),
inference(avatar_split_clause,[],[f78291,f78284,f76062,f76057,f78294]) ).
fof(f78311,plain,
( k1_funct_5(k5_relat_1(sF304,sK30)) = k10_relset_1(sK27,sK28,sK30,sF307)
| ~ spl309_154
| ~ spl309_291 ),
inference(superposition,[],[f76690,f78278]) ).
fof(f78312,plain,
( k9_relat_1(sK30,sF307) = k1_funct_5(k5_relat_1(sF304,sK30))
| ~ spl309_74
| ~ spl309_154
| ~ spl309_291 ),
inference(forward_demodulation,[],[f78311,f75943]) ).
fof(f78314,definition,
( spl309_294
<=> k9_relat_1(sK30,sF307) = k1_funct_5(k5_relat_1(sF304,sK30)) ),
introduced(definition,[new_symbols(definition,[spl309_294])],[avatar_definition]) ).
fof(f78316,plain,
( k9_relat_1(sK30,sF307) = k1_funct_5(k5_relat_1(sF304,sK30))
| ~ spl309_294 ),
inference(avatar_component_clause,[],[f78314]) ).
fof(f78317,plain,
( spl309_294
| ~ spl309_74
| ~ spl309_154
| ~ spl309_291 ),
inference(avatar_split_clause,[],[f78312,f78276,f76688,f75932,f78314]) ).
fof(f78479,plain,
( k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)) = k1_funct_5(sF304)
| ~ r1_tarski(k1_funct_5(sF304),k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)))
| ~ spl309_83 ),
inference(resolution,[],[f73638,f76030]) ).
fof(f78481,plain,
( sF307 = k1_funct_5(sF305)
| ~ r1_tarski(sF307,k1_funct_5(sF305))
| ~ spl309_61 ),
inference(resolution,[],[f73638,f75753]) ).
fof(f78517,plain,
( k1_funct_5(sF304) = k1_funct_5(k5_relat_1(sF304,sK30))
| ~ r1_tarski(k1_funct_5(sF304),k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)))
| ~ spl309_83
| ~ spl309_108 ),
inference(forward_demodulation,[],[f78479,f76261]) ).
fof(f78539,plain,
( k1_funct_5(sF304) = k9_relat_1(sK30,sF307)
| ~ r1_tarski(k1_funct_5(sF304),k1_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)))
| ~ spl309_83
| ~ spl309_108
| ~ spl309_294 ),
inference(forward_demodulation,[],[f78517,f78316]) ).
fof(f78550,plain,
( ~ r1_tarski(k1_funct_5(sF304),k1_funct_5(k5_relat_1(sF304,sK30)))
| k1_funct_5(sF304) = k9_relat_1(sK30,sF307)
| ~ spl309_83
| ~ spl309_108
| ~ spl309_294 ),
inference(forward_demodulation,[],[f78539,f76261]) ).
fof(f78552,plain,
( ~ r1_tarski(k1_funct_5(sF304),k9_relat_1(sK30,sF307))
| k1_funct_5(sF304) = k9_relat_1(sK30,sF307)
| ~ spl309_83
| ~ spl309_108
| ~ spl309_294 ),
inference(forward_demodulation,[],[f78550,f78316]) ).
fof(f78554,definition,
( spl309_315
<=> k1_funct_5(sF304) = k9_relat_1(sK30,sF307) ),
introduced(definition,[new_symbols(definition,[spl309_315])],[avatar_definition]) ).
fof(f78558,definition,
( spl309_316
<=> r1_tarski(k1_funct_5(sF304),k9_relat_1(sK30,sF307)) ),
introduced(definition,[new_symbols(definition,[spl309_316])],[avatar_definition]) ).
fof(f78561,plain,
( spl309_315
| ~ spl309_316
| ~ spl309_83
| ~ spl309_108
| ~ spl309_294 ),
inference(avatar_split_clause,[],[f78552,f78314,f76259,f76028,f78558,f78554]) ).
fof(f79051,plain,
( k10_relset_1(sK27,sK27,k4_relat_1(sF305),sK27) = k2_funct_5(k4_relat_1(sF305))
| ~ spl309_131 ),
inference(resolution,[],[f76436,f72863]) ).
fof(f79052,plain,
( k1_funct_5(k4_relat_1(sF305)) = k10_relset_1(sK27,sK27,k6_relset_1(sK27,sK27,k4_relat_1(sF305)),sK27)
| ~ spl309_131 ),
inference(resolution,[],[f76436,f72864]) ).
fof(f79055,plain,
( m1_relset_1(k4_relat_1(sF305),sK27,sK27)
| ~ spl309_131 ),
inference(resolution,[],[f76436,f73020]) ).
fof(f79056,plain,
( m1_subset_1(k4_relat_1(sF305),k1_zfmisc_1(k2_zfmisc_1(sK27,sK27)))
| ~ spl309_131 ),
inference(resolution,[],[f76436,f73035]) ).
fof(f79060,definition,
( spl309_349
<=> m1_subset_1(k4_relat_1(sF305),k1_zfmisc_1(k2_zfmisc_1(sK27,sK27))) ),
introduced(definition,[new_symbols(definition,[spl309_349])],[avatar_definition]) ).
fof(f79062,plain,
( m1_subset_1(k4_relat_1(sF305),k1_zfmisc_1(k2_zfmisc_1(sK27,sK27)))
| ~ spl309_349 ),
inference(avatar_component_clause,[],[f79060]) ).
fof(f79063,plain,
( spl309_349
| ~ spl309_131 ),
inference(avatar_split_clause,[],[f79056,f76434,f79060]) ).
fof(f79065,definition,
( spl309_350
<=> m1_relset_1(k4_relat_1(sF305),sK27,sK27) ),
introduced(definition,[new_symbols(definition,[spl309_350])],[avatar_definition]) ).
fof(f79067,plain,
( m1_relset_1(k4_relat_1(sF305),sK27,sK27)
| ~ spl309_350 ),
inference(avatar_component_clause,[],[f79065]) ).
fof(f79068,plain,
( spl309_350
| ~ spl309_131 ),
inference(avatar_split_clause,[],[f79055,f76434,f79065]) ).
fof(f79069,plain,
( k10_relset_1(sK27,sK27,sF305,sK27) = k1_funct_5(k4_relat_1(sF305))
| ~ spl309_131
| ~ spl309_132 ),
inference(forward_demodulation,[],[f79052,f76441]) ).
fof(f79070,plain,
( k1_funct_5(sF305) = k2_funct_5(k4_relat_1(sF305))
| ~ spl309_131
| ~ spl309_162 ),
inference(forward_demodulation,[],[f79051,f76758]) ).
fof(f79143,plain,
( k2_funct_5(sF305) = k1_funct_5(k4_relat_1(sF305))
| ~ spl309_114
| ~ spl309_131
| ~ spl309_132 ),
inference(forward_demodulation,[],[f79069,f76321]) ).
fof(f79145,definition,
( spl309_360
<=> k1_funct_5(sF305) = k2_funct_5(k4_relat_1(sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_360])],[avatar_definition]) ).
fof(f79147,plain,
( k1_funct_5(sF305) = k2_funct_5(k4_relat_1(sF305))
| ~ spl309_360 ),
inference(avatar_component_clause,[],[f79145]) ).
fof(f79148,plain,
( spl309_360
| ~ spl309_131
| ~ spl309_162 ),
inference(avatar_split_clause,[],[f79070,f76756,f76434,f79145]) ).
fof(f79196,plain,
( k1_funct_5(sF305) = k1_funct_5(k4_relat_1(sF305))
| ~ spl309_114
| ~ spl309_131
| ~ spl309_132
| ~ spl309_293 ),
inference(forward_demodulation,[],[f79143,f78296]) ).
fof(f79226,definition,
( spl309_371
<=> k1_funct_5(sF305) = k1_funct_5(k4_relat_1(sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_371])],[avatar_definition]) ).
fof(f79228,plain,
( k1_funct_5(sF305) = k1_funct_5(k4_relat_1(sF305))
| ~ spl309_371 ),
inference(avatar_component_clause,[],[f79226]) ).
fof(f79229,plain,
( spl309_371
| ~ spl309_114
| ~ spl309_131
| ~ spl309_132
| ~ spl309_293 ),
inference(avatar_split_clause,[],[f79196,f78294,f76439,f76434,f76319,f79226]) ).
fof(f79441,plain,
( k2_funct_5(sK30) = k2_xboole_0(k9_relat_1(sK30,k2_funct_5(sF305)),k2_funct_5(sK30))
| ~ spl309_185 ),
inference(unit_resulting_resolution,[],[f73449,f77085]) ).
fof(f79445,plain,
( r1_tarski(k2_xboole_0(k2_funct_5(sK30),k9_relat_1(sK30,k2_funct_5(sF305))),k2_funct_5(sK30))
| ~ spl309_185 ),
inference(unit_resulting_resolution,[],[f73453,f73639,f77085]) ).
fof(f79465,plain,
( k2_funct_5(sK30) = k2_xboole_0(k2_funct_5(sK30),k9_relat_1(sK30,k2_funct_5(sF305)))
| ~ spl309_185 ),
inference(forward_demodulation,[],[f79441,f73460]) ).
fof(f79469,plain,
( r1_tarski(k2_xboole_0(k1_funct_5(sF304),k9_relat_1(sK30,k2_funct_5(sF305))),k1_funct_5(sF304))
| ~ spl309_185
| ~ spl309_292 ),
inference(forward_demodulation,[],[f79445,f78286]) ).
fof(f79482,plain,
( k2_funct_5(sK30) = k2_xboole_0(k2_funct_5(sK30),k9_relat_1(sK30,k1_funct_5(sF305)))
| ~ spl309_185
| ~ spl309_293 ),
inference(forward_demodulation,[],[f79465,f78296]) ).
fof(f79486,plain,
( r1_tarski(k2_xboole_0(k1_funct_5(sF304),k9_relat_1(sK30,k1_funct_5(sF305))),k1_funct_5(sF304))
| ~ spl309_185
| ~ spl309_292
| ~ spl309_293 ),
inference(forward_demodulation,[],[f79469,f78296]) ).
fof(f79511,plain,
( k1_funct_5(sF304) = k2_xboole_0(k1_funct_5(sF304),k9_relat_1(sK30,k1_funct_5(sF305)))
| ~ spl309_185
| ~ spl309_292
| ~ spl309_293 ),
inference(forward_demodulation,[],[f79482,f78286]) ).
fof(f79515,definition,
( spl309_385
<=> r1_tarski(k2_xboole_0(k1_funct_5(sF304),k9_relat_1(sK30,k1_funct_5(sF305))),k1_funct_5(sF304)) ),
introduced(definition,[new_symbols(definition,[spl309_385])],[avatar_definition]) ).
fof(f79518,plain,
( spl309_385
| ~ spl309_185
| ~ spl309_292
| ~ spl309_293 ),
inference(avatar_split_clause,[],[f79486,f78294,f78284,f77083,f79515]) ).
fof(f79528,definition,
( spl309_387
<=> k1_funct_5(sF304) = k2_xboole_0(k1_funct_5(sF304),k9_relat_1(sK30,k1_funct_5(sF305))) ),
introduced(definition,[new_symbols(definition,[spl309_387])],[avatar_definition]) ).
fof(f79531,plain,
( spl309_387
| ~ spl309_185
| ~ spl309_292
| ~ spl309_293 ),
inference(avatar_split_clause,[],[f79511,f78294,f78284,f77083,f79528]) ).
fof(f79715,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| k1_relat_1(X0) = k1_funct_5(X0) ),
inference(resolution,[],[f74404,f73036]) ).
fof(f79716,plain,
( k1_funct_5(sK30) = k1_relat_1(sK30)
| ~ spl309_68 ),
inference(resolution,[],[f74404,f75811]) ).
fof(f79717,plain,
( k1_funct_5(sF304) = k1_relat_1(sF304)
| ~ spl309_106 ),
inference(resolution,[],[f74404,f76249]) ).
fof(f79718,plain,
( k1_funct_5(sF305) = k1_relat_1(sF305)
| ~ spl309_143 ),
inference(resolution,[],[f74404,f76571]) ).
fof(f79720,definition,
( spl309_402
<=> k1_funct_5(sF305) = k1_relat_1(sF305) ),
introduced(definition,[new_symbols(definition,[spl309_402])],[avatar_definition]) ).
fof(f79722,plain,
( k1_funct_5(sF305) = k1_relat_1(sF305)
| ~ spl309_402 ),
inference(avatar_component_clause,[],[f79720]) ).
fof(f79723,plain,
( spl309_402
| ~ spl309_143 ),
inference(avatar_split_clause,[],[f79718,f76569,f79720]) ).
fof(f79725,definition,
( spl309_403
<=> k1_funct_5(sF304) = k1_relat_1(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_403])],[avatar_definition]) ).
fof(f79727,plain,
( k1_funct_5(sF304) = k1_relat_1(sF304)
| ~ spl309_403 ),
inference(avatar_component_clause,[],[f79725]) ).
fof(f79728,plain,
( spl309_403
| ~ spl309_106 ),
inference(avatar_split_clause,[],[f79717,f76247,f79725]) ).
fof(f79729,plain,
( sF307 = k1_relat_1(sK30)
| ~ spl309_54
| ~ spl309_68 ),
inference(forward_demodulation,[],[f79716,f75642]) ).
fof(f79732,definition,
( spl309_404
<=> sF307 = k1_relat_1(sK30) ),
introduced(definition,[new_symbols(definition,[spl309_404])],[avatar_definition]) ).
fof(f79734,plain,
( sF307 = k1_relat_1(sK30)
| ~ spl309_404 ),
inference(avatar_component_clause,[],[f79732]) ).
fof(f79735,plain,
( spl309_404
| ~ spl309_54
| ~ spl309_68 ),
inference(avatar_split_clause,[],[f79729,f75809,f75640,f79732]) ).
fof(f79780,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| k2_relat_1(X0) = k2_funct_5(X0) ),
inference(resolution,[],[f74403,f73036]) ).
fof(f79781,plain,
( k2_funct_5(sK30) = k2_relat_1(sK30)
| ~ spl309_68 ),
inference(resolution,[],[f74403,f75811]) ).
fof(f79782,plain,
( k2_funct_5(sF304) = k2_relat_1(sF304)
| ~ spl309_106 ),
inference(resolution,[],[f74403,f76249]) ).
fof(f79789,plain,
( sF307 = k2_relat_1(sF304)
| ~ spl309_85
| ~ spl309_106 ),
inference(forward_demodulation,[],[f79782,f76047]) ).
fof(f79791,definition,
( spl309_407
<=> k2_funct_5(sK30) = k2_relat_1(sK30) ),
introduced(definition,[new_symbols(definition,[spl309_407])],[avatar_definition]) ).
fof(f79793,plain,
( k2_funct_5(sK30) = k2_relat_1(sK30)
| ~ spl309_407 ),
inference(avatar_component_clause,[],[f79791]) ).
fof(f79794,plain,
( spl309_407
| ~ spl309_68 ),
inference(avatar_split_clause,[],[f79781,f75809,f79791]) ).
fof(f79797,definition,
( spl309_408
<=> sF307 = k2_relat_1(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_408])],[avatar_definition]) ).
fof(f79799,plain,
( sF307 = k2_relat_1(sF304)
| ~ spl309_408 ),
inference(avatar_component_clause,[],[f79797]) ).
fof(f79800,plain,
( spl309_408
| ~ spl309_85
| ~ spl309_106 ),
inference(avatar_split_clause,[],[f79789,f76247,f76045,f79797]) ).
fof(f81187,plain,
( ! [X0] : r1_tarski(k9_relat_1(sF305,X0),k2_relat_1(sF305))
| ~ spl309_143 ),
inference(resolution,[],[f73138,f76571]) ).
fof(f81744,plain,
( k1_funct_5(sF304) = k2_relat_1(sK30)
| ~ spl309_292
| ~ spl309_407 ),
inference(superposition,[],[f78286,f79793]) ).
fof(f81745,plain,
( k2_funct_5(sF305) = k9_relat_1(sF304,k2_relat_1(sK30))
| ~ spl309_158
| ~ spl309_407 ),
inference(superposition,[],[f76731,f79793]) ).
fof(f81749,plain,
( k1_funct_5(sF305) = k9_relat_1(sF304,k2_relat_1(sK30))
| ~ spl309_158
| ~ spl309_293
| ~ spl309_407 ),
inference(forward_demodulation,[],[f81745,f78296]) ).
fof(f81750,plain,
( k1_relat_1(sF304) = k2_relat_1(sK30)
| ~ spl309_292
| ~ spl309_403
| ~ spl309_407 ),
inference(forward_demodulation,[],[f81744,f79727]) ).
fof(f81758,plain,
( k1_relat_1(sF305) = k9_relat_1(sF304,k2_relat_1(sK30))
| ~ spl309_158
| ~ spl309_293
| ~ spl309_402
| ~ spl309_407 ),
inference(forward_demodulation,[],[f81749,f79722]) ).
fof(f81760,definition,
( spl309_445
<=> k1_relat_1(sF304) = k2_relat_1(sK30) ),
introduced(definition,[new_symbols(definition,[spl309_445])],[avatar_definition]) ).
fof(f81762,plain,
( k1_relat_1(sF304) = k2_relat_1(sK30)
| ~ spl309_445 ),
inference(avatar_component_clause,[],[f81760]) ).
fof(f81763,plain,
( spl309_445
| ~ spl309_292
| ~ spl309_403
| ~ spl309_407 ),
inference(avatar_split_clause,[],[f81750,f79791,f79725,f78284,f81760]) ).
fof(f81766,definition,
( spl309_446
<=> k1_relat_1(sF305) = k9_relat_1(sF304,k2_relat_1(sK30)) ),
introduced(definition,[new_symbols(definition,[spl309_446])],[avatar_definition]) ).
fof(f81768,plain,
( k1_relat_1(sF305) = k9_relat_1(sF304,k2_relat_1(sK30))
| ~ spl309_446 ),
inference(avatar_component_clause,[],[f81766]) ).
fof(f81769,plain,
( spl309_446
| ~ spl309_158
| ~ spl309_293
| ~ spl309_402
| ~ spl309_407 ),
inference(avatar_split_clause,[],[f81758,f79791,f79720,f78294,f76729,f81766]) ).
fof(f81771,plain,
( k1_relat_1(sF305) = k9_relat_1(sF304,k1_relat_1(sF304))
| ~ spl309_445
| ~ spl309_446 ),
inference(forward_demodulation,[],[f81768,f81762]) ).
fof(f81773,definition,
( spl309_447
<=> k1_relat_1(sF305) = k9_relat_1(sF304,k1_relat_1(sF304)) ),
introduced(definition,[new_symbols(definition,[spl309_447])],[avatar_definition]) ).
fof(f81775,plain,
( k1_relat_1(sF305) = k9_relat_1(sF304,k1_relat_1(sF304))
| ~ spl309_447 ),
inference(avatar_component_clause,[],[f81773]) ).
fof(f81776,plain,
( spl309_447
| ~ spl309_445
| ~ spl309_446 ),
inference(avatar_split_clause,[],[f81771,f81766,f81760,f81773]) ).
fof(f83208,plain,
( v1_relat_1(k4_relat_1(sF305))
| ~ spl309_349 ),
inference(unit_resulting_resolution,[],[f73036,f79062]) ).
fof(f83249,plain,
( k2_funct_5(k4_relat_1(sF305)) = k2_relat_1(k4_relat_1(sF305))
| ~ spl309_349 ),
inference(resolution,[],[f79062,f79780]) ).
fof(f83250,plain,
( k1_funct_5(k4_relat_1(sF305)) = k1_relat_1(k4_relat_1(sF305))
| ~ spl309_349 ),
inference(resolution,[],[f79062,f79715]) ).
fof(f83253,plain,
( k1_funct_5(sF305) = k1_relat_1(k4_relat_1(sF305))
| ~ spl309_349
| ~ spl309_371 ),
inference(forward_demodulation,[],[f83250,f79228]) ).
fof(f83254,plain,
( k1_funct_5(sF305) = k2_relat_1(k4_relat_1(sF305))
| ~ spl309_349
| ~ spl309_360 ),
inference(forward_demodulation,[],[f83249,f79147]) ).
fof(f83309,definition,
( spl309_553
<=> v1_relat_1(k4_relat_1(sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_553])],[avatar_definition]) ).
fof(f83311,plain,
( v1_relat_1(k4_relat_1(sF305))
| ~ spl309_553 ),
inference(avatar_component_clause,[],[f83309]) ).
fof(f83312,plain,
( spl309_553
| ~ spl309_349 ),
inference(avatar_split_clause,[],[f83208,f79060,f83309]) ).
fof(f83368,plain,
( k1_relat_1(sF305) = k1_relat_1(k4_relat_1(sF305))
| ~ spl309_349
| ~ spl309_371
| ~ spl309_402 ),
inference(forward_demodulation,[],[f83253,f79722]) ).
fof(f83369,plain,
( k1_relat_1(sF305) = k2_relat_1(k4_relat_1(sF305))
| ~ spl309_349
| ~ spl309_360
| ~ spl309_402 ),
inference(forward_demodulation,[],[f83254,f79722]) ).
fof(f83410,definition,
( spl309_566
<=> k1_relat_1(sF305) = k1_relat_1(k4_relat_1(sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_566])],[avatar_definition]) ).
fof(f83412,plain,
( k1_relat_1(sF305) = k1_relat_1(k4_relat_1(sF305))
| ~ spl309_566 ),
inference(avatar_component_clause,[],[f83410]) ).
fof(f83413,plain,
( spl309_566
| ~ spl309_349
| ~ spl309_371
| ~ spl309_402 ),
inference(avatar_split_clause,[],[f83368,f79720,f79226,f79060,f83410]) ).
fof(f83415,definition,
( spl309_567
<=> k1_relat_1(sF305) = k2_relat_1(k4_relat_1(sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_567])],[avatar_definition]) ).
fof(f83417,plain,
( k1_relat_1(sF305) = k2_relat_1(k4_relat_1(sF305))
| ~ spl309_567 ),
inference(avatar_component_clause,[],[f83415]) ).
fof(f83418,plain,
( spl309_567
| ~ spl309_349
| ~ spl309_360
| ~ spl309_402 ),
inference(avatar_split_clause,[],[f83369,f79720,f79145,f79060,f83415]) ).
fof(f83716,plain,
( k2_relat_1(k4_relat_1(sF305)) = k9_relat_1(k4_relat_1(sF305),k1_relat_1(k4_relat_1(sF305)))
| ~ spl309_553 ),
inference(resolution,[],[f73136,f83311]) ).
fof(f83717,plain,
( k9_relat_1(sK30,k1_relat_1(sK30)) = k2_relat_1(sK30)
| ~ spl309_68 ),
inference(resolution,[],[f73136,f75811]) ).
fof(f83718,plain,
( k9_relat_1(sF304,k1_relat_1(sF304)) = k2_relat_1(sF304)
| ~ spl309_106 ),
inference(resolution,[],[f73136,f76249]) ).
fof(f83725,plain,
( sF307 = k9_relat_1(sF304,k1_relat_1(sF304))
| ~ spl309_106
| ~ spl309_408 ),
inference(forward_demodulation,[],[f83718,f79799]) ).
fof(f83726,plain,
( k9_relat_1(sK30,k1_relat_1(sK30)) = k1_relat_1(sF304)
| ~ spl309_68
| ~ spl309_445 ),
inference(forward_demodulation,[],[f83717,f81762]) ).
fof(f83727,plain,
( k2_relat_1(k4_relat_1(sF305)) = k9_relat_1(k4_relat_1(sF305),k1_relat_1(sF305))
| ~ spl309_553
| ~ spl309_566 ),
inference(forward_demodulation,[],[f83716,f83412]) ).
fof(f83732,definition,
( spl309_582
<=> sF307 = k9_relat_1(sF304,k1_relat_1(sF304)) ),
introduced(definition,[new_symbols(definition,[spl309_582])],[avatar_definition]) ).
fof(f83735,plain,
( spl309_582
| ~ spl309_106
| ~ spl309_408 ),
inference(avatar_split_clause,[],[f83725,f79797,f76247,f83732]) ).
fof(f83736,plain,
( k9_relat_1(sK30,sF307) = k1_relat_1(sF304)
| ~ spl309_68
| ~ spl309_404
| ~ spl309_445 ),
inference(forward_demodulation,[],[f83726,f79734]) ).
fof(f83737,plain,
( k1_relat_1(sF305) = k9_relat_1(k4_relat_1(sF305),k1_relat_1(sF305))
| ~ spl309_553
| ~ spl309_566
| ~ spl309_567 ),
inference(forward_demodulation,[],[f83727,f83417]) ).
fof(f83741,definition,
( spl309_583
<=> k9_relat_1(sK30,sF307) = k1_relat_1(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_583])],[avatar_definition]) ).
fof(f83744,plain,
( spl309_583
| ~ spl309_68
| ~ spl309_404
| ~ spl309_445 ),
inference(avatar_split_clause,[],[f83736,f81760,f79732,f75809,f83741]) ).
fof(f83746,definition,
( spl309_584
<=> k1_relat_1(sF305) = k9_relat_1(k4_relat_1(sF305),k1_relat_1(sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_584])],[avatar_definition]) ).
fof(f83749,plain,
( spl309_584
| ~ spl309_553
| ~ spl309_566
| ~ spl309_567 ),
inference(avatar_split_clause,[],[f83737,f83415,f83410,f83309,f83746]) ).
fof(f83763,plain,
( k1_funct_5(sF304) != k2_xboole_0(k1_funct_5(sF304),k9_relat_1(sK30,k1_funct_5(sF305)))
| k1_funct_5(sF304) != k1_relat_1(sF304)
| k9_relat_1(sK30,sF307) != k1_relat_1(sF304)
| r1_tarski(k1_funct_5(sF304),k9_relat_1(sK30,sF307))
| ~ r1_tarski(k2_xboole_0(k1_funct_5(sF304),k9_relat_1(sK30,k1_funct_5(sF305))),k1_funct_5(sF304)) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f83769,plain,
( r1_tarski(sF307,k1_relat_1(sF305))
| ~ spl309_141
| ~ spl309_402 ),
inference(forward_demodulation,[],[f76546,f79722]) ).
fof(f83780,plain,
( sF307 = k1_relat_1(sF305)
| ~ r1_tarski(sF307,k1_funct_5(sF305))
| ~ spl309_61
| ~ spl309_402 ),
inference(forward_demodulation,[],[f78481,f79722]) ).
fof(f83810,definition,
( spl309_589
<=> r1_tarski(sF307,k1_relat_1(sF305)) ),
introduced(definition,[new_symbols(definition,[spl309_589])],[avatar_definition]) ).
fof(f83813,plain,
( spl309_589
| ~ spl309_141
| ~ spl309_402 ),
inference(avatar_split_clause,[],[f83769,f79720,f76545,f83810]) ).
fof(f83838,plain,
( ~ r1_tarski(sF307,k1_relat_1(sF305))
| sF307 = k1_relat_1(sF305)
| ~ spl309_61
| ~ spl309_402 ),
inference(forward_demodulation,[],[f83780,f79722]) ).
fof(f83845,definition,
( spl309_594
<=> sF307 = k1_relat_1(sF305) ),
introduced(definition,[new_symbols(definition,[spl309_594])],[avatar_definition]) ).
fof(f83847,plain,
( sF307 = k1_relat_1(sF305)
| ~ spl309_594 ),
inference(avatar_component_clause,[],[f83845]) ).
fof(f83862,plain,
( spl309_594
| ~ spl309_589
| ~ spl309_61
| ~ spl309_402 ),
inference(avatar_split_clause,[],[f83838,f79720,f75751,f83810,f83845]) ).
fof(f87113,plain,
( m1_subset_1(k9_relset_2(sK27,sK27,sK28,sF305,sK30),k1_zfmisc_1(k2_zfmisc_1(sK27,sK28)))
| ~ spl309_146 ),
inference(resolution,[],[f76586,f73035]) ).
fof(f87122,plain,
( m1_subset_1(k5_relat_1(sF305,sK30),k1_zfmisc_1(k2_zfmisc_1(sK27,sK28)))
| ~ spl309_146
| ~ spl309_148 ),
inference(forward_demodulation,[],[f87113,f76596]) ).
fof(f87166,definition,
( spl309_719
<=> m1_subset_1(k5_relat_1(sF305,sK30),k1_zfmisc_1(k2_zfmisc_1(sK27,sK28))) ),
introduced(definition,[new_symbols(definition,[spl309_719])],[avatar_definition]) ).
fof(f87168,plain,
( m1_subset_1(k5_relat_1(sF305,sK30),k1_zfmisc_1(k2_zfmisc_1(sK27,sK28)))
| ~ spl309_719 ),
inference(avatar_component_clause,[],[f87166]) ).
fof(f87169,plain,
( spl309_719
| ~ spl309_146
| ~ spl309_148 ),
inference(avatar_split_clause,[],[f87122,f76594,f76584,f87166]) ).
fof(f87460,plain,
( k1_funct_5(k5_relat_1(sF305,sK30)) = k1_relat_1(k5_relat_1(sF305,sK30))
| ~ spl309_719 ),
inference(resolution,[],[f87168,f79715]) ).
fof(f87464,definition,
( spl309_746
<=> k1_funct_5(k5_relat_1(sF305,sK30)) = k1_relat_1(k5_relat_1(sF305,sK30)) ),
introduced(definition,[new_symbols(definition,[spl309_746])],[avatar_definition]) ).
fof(f87466,plain,
( k1_funct_5(k5_relat_1(sF305,sK30)) = k1_relat_1(k5_relat_1(sF305,sK30))
| ~ spl309_746 ),
inference(avatar_component_clause,[],[f87464]) ).
fof(f87467,plain,
( spl309_746
| ~ spl309_719 ),
inference(avatar_split_clause,[],[f87460,f87166,f87464]) ).
fof(f89072,plain,
( ! [X0] : k9_relat_1(sF304,k9_relat_1(sK30,X0)) = k9_relat_1(k5_relat_1(sK30,sF304),X0)
| ~ spl309_68
| ~ spl309_106 ),
inference(unit_resulting_resolution,[],[f73122,f75811,f76249]) ).
fof(f89085,plain,
( ! [X0] : k9_relat_1(sF305,X0) = k9_relat_1(sF304,k9_relat_1(sK30,X0))
| ~ spl309_68
| ~ spl309_106
| ~ spl309_110 ),
inference(forward_demodulation,[],[f89072,f76271]) ).
fof(f91310,plain,
( k9_relat_1(sF304,k2_relat_1(sK30)) = k2_relat_1(k5_relat_1(sK30,sF304))
| ~ spl309_68
| ~ spl309_106 ),
inference(unit_resulting_resolution,[],[f73121,f75811,f76249]) ).
fof(f91375,plain,
( k2_relat_1(sF305) = k9_relat_1(sF304,k2_relat_1(sK30))
| ~ spl309_68
| ~ spl309_106
| ~ spl309_110 ),
inference(forward_demodulation,[],[f91310,f76271]) ).
fof(f91445,plain,
( k9_relat_1(sF304,k1_relat_1(sF304)) = k2_relat_1(sF305)
| ~ spl309_68
| ~ spl309_106
| ~ spl309_110
| ~ spl309_445 ),
inference(forward_demodulation,[],[f91375,f81762]) ).
fof(f91493,plain,
( k1_relat_1(sF305) = k2_relat_1(sF305)
| ~ spl309_68
| ~ spl309_106
| ~ spl309_110
| ~ spl309_445
| ~ spl309_447 ),
inference(forward_demodulation,[],[f91445,f81775]) ).
fof(f91542,plain,
( sF307 = k2_relat_1(sF305)
| ~ spl309_68
| ~ spl309_106
| ~ spl309_110
| ~ spl309_445
| ~ spl309_447
| ~ spl309_594 ),
inference(forward_demodulation,[],[f91493,f83847]) ).
fof(f91551,definition,
( spl309_962
<=> sF307 = k2_relat_1(sF305) ),
introduced(definition,[new_symbols(definition,[spl309_962])],[avatar_definition]) ).
fof(f91553,plain,
( sF307 = k2_relat_1(sF305)
| ~ spl309_962 ),
inference(avatar_component_clause,[],[f91551]) ).
fof(f91554,plain,
( spl309_962
| ~ spl309_68
| ~ spl309_106
| ~ spl309_110
| ~ spl309_445
| ~ spl309_447
| ~ spl309_594 ),
inference(avatar_split_clause,[],[f91542,f83845,f81773,f81760,f76269,f76247,f75809,f91551]) ).
fof(f92951,plain,
( ! [X0] : k9_relat_1(k4_relat_1(sF305),X0) = k10_relset_1(sK27,sK27,k4_relat_1(sF305),X0)
| ~ spl309_350 ),
inference(resolution,[],[f79067,f73715]) ).
fof(f92969,plain,
( k1_funct_5(k5_relat_1(sF305,sK30)) = k9_relat_1(k4_relat_1(sF305),sF307)
| ~ spl309_159
| ~ spl309_350 ),
inference(superposition,[],[f76741,f92951]) ).
fof(f92970,plain,
( k9_relat_1(k4_relat_1(sF305),sF307) = k1_relat_1(k5_relat_1(sF305,sK30))
| ~ spl309_159
| ~ spl309_350
| ~ spl309_746 ),
inference(forward_demodulation,[],[f92969,f87466]) ).
fof(f92977,definition,
( spl309_1034
<=> k9_relat_1(k4_relat_1(sF305),sF307) = k1_relat_1(k5_relat_1(sF305,sK30)) ),
introduced(definition,[new_symbols(definition,[spl309_1034])],[avatar_definition]) ).
fof(f92980,plain,
( spl309_1034
| ~ spl309_159
| ~ spl309_350
| ~ spl309_746 ),
inference(avatar_split_clause,[],[f92970,f87464,f79065,f76739,f92977]) ).
fof(f92997,plain,
( sK30 != k4_relat_1(sF304)
| k9_relset_2(sK28,sK27,sK28,sF304,sK30) != k5_relat_1(sF304,sK30)
| sF307 != k2_funct_5(sF304)
| k1_funct_5(sF304) != k1_relat_1(sF304)
| k1_funct_5(sF304) != k9_relat_1(sK30,sF307)
| k2_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,sK30)) != k9_relat_1(sK30,k2_funct_5(sF304))
| k1_funct_5(k5_relat_1(sF304,sK30)) != k2_funct_5(k9_relset_2(sK28,sK27,sK28,sF304,k4_relat_1(sF304)))
| sF307 != k9_relat_1(sF304,k1_relat_1(sF304))
| k1_funct_5(sF305) != k9_relat_1(sF304,k1_funct_5(sF304))
| k1_funct_5(k5_relat_1(sF305,sK30)) != k1_relat_1(k5_relat_1(sF305,sK30))
| k9_relat_1(k4_relat_1(sF305),sF307) != k1_relat_1(k5_relat_1(sF305,sK30))
| k1_relat_1(sF305) != k9_relat_1(k4_relat_1(sF305),k1_relat_1(sF305))
| k1_funct_5(sF305) != k1_relat_1(sF305)
| r1_tarski(sF307,k1_funct_5(k5_relat_1(sF305,sK30)))
| ~ r1_tarski(k9_relat_1(sF304,k1_funct_5(k5_relat_1(sF304,sK30))),k1_funct_5(sF305)) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f148671,plain,
( r1_tarski(sF306,k2_relat_1(sF305))
| ~ spl309_133
| ~ spl309_143 ),
inference(superposition,[],[f81187,f76448]) ).
fof(f148675,plain,
( r1_tarski(sF306,sF307)
| ~ spl309_133
| ~ spl309_143
| ~ spl309_962 ),
inference(forward_demodulation,[],[f148671,f91553]) ).
fof(f166371,plain,
( ! [X0] : r1_tarski(k4_xboole_0(k1_relat_1(sK30),k4_xboole_0(k1_relat_1(sK30),X0)),k9_relat_1(k4_relat_1(sK30),k9_relat_1(sK30,X0)))
| ~ spl309_68 ),
inference(resolution,[],[f75034,f75811]) ).
fof(f166376,plain,
( ! [X0] : r1_tarski(k4_xboole_0(k1_relat_1(sK30),k4_xboole_0(k1_relat_1(sK30),X0)),k9_relat_1(sF304,k9_relat_1(sK30,X0)))
| ~ spl309_68
| ~ spl309_75 ),
inference(forward_demodulation,[],[f166371,f75955]) ).
fof(f166386,plain,
( ! [X0] : r1_tarski(k4_xboole_0(k1_relat_1(sK30),k4_xboole_0(k1_relat_1(sK30),X0)),k9_relat_1(sF305,X0))
| ~ spl309_68
| ~ spl309_75
| ~ spl309_106
| ~ spl309_110 ),
inference(forward_demodulation,[],[f166376,f89085]) ).
fof(f166394,plain,
( ! [X0] : r1_tarski(k4_xboole_0(sF307,k4_xboole_0(sF307,X0)),k9_relat_1(sF305,X0))
| ~ spl309_68
| ~ spl309_75
| ~ spl309_106
| ~ spl309_110
| ~ spl309_404 ),
inference(forward_demodulation,[],[f166386,f79734]) ).
fof(f166820,plain,
( r1_tarski(k4_xboole_0(sF307,k4_xboole_0(sF307,sK29)),sF306)
| ~ spl309_68
| ~ spl309_75
| ~ spl309_106
| ~ spl309_110
| ~ spl309_133
| ~ spl309_404 ),
inference(superposition,[],[f166394,f76448]) ).
fof(f166822,plain,
( r1_tarski(k4_xboole_0(sK29,k4_xboole_0(sK29,sF307)),sF306)
| ~ spl309_68
| ~ spl309_75
| ~ spl309_106
| ~ spl309_110
| ~ spl309_133
| ~ spl309_404 ),
inference(forward_demodulation,[],[f166820,f74581]) ).
fof(f167114,plain,
( r1_tarski(sK29,sF306)
| ~ spl309_68
| ~ spl309_75
| ~ spl309_106
| ~ spl309_110
| ~ spl309_133
| ~ spl309_262
| ~ spl309_404 ),
inference(forward_demodulation,[],[f166822,f78019]) ).
fof(f167293,plain,
( $false
| spl309_49
| ~ spl309_68
| ~ spl309_75
| ~ spl309_106
| ~ spl309_110
| ~ spl309_133
| ~ spl309_262
| ~ spl309_404 ),
inference(forward_subsumption_resolution,[],[f167114,f75607]) ).
fof(f167294,plain,
( spl309_49
| ~ spl309_68
| ~ spl309_75
| ~ spl309_106
| ~ spl309_110
| ~ spl309_133
| ~ spl309_262
| ~ spl309_404 ),
inference(avatar_contradiction_clause,[],[f167293]) ).
fof(f167704,plain,
( $false
| spl309_95
| ~ spl309_133
| ~ spl309_143
| ~ spl309_962 ),
inference(forward_subsumption_resolution,[],[f148675,f76149]) ).
fof(f167705,plain,
( spl309_95
| ~ spl309_133
| ~ spl309_143
| ~ spl309_962 ),
inference(avatar_contradiction_clause,[],[f167704]) ).
cnf(s50,plain,
spl309_47,
inference(sat_conversion,[],[f75600]) ).
cnf(s51,plain,
( spl309_48
| spl309_49 ),
inference(sat_conversion,[],[f75609]) ).
cnf(s52,plain,
( ~ spl309_48
| ~ spl309_49 ),
inference(sat_conversion,[],[f75610]) ).
cnf(s54,plain,
spl309_51,
inference(sat_conversion,[],[f75628]) ).
cnf(s55,plain,
spl309_52,
inference(sat_conversion,[],[f75633]) ).
cnf(s56,plain,
spl309_53,
inference(sat_conversion,[],[f75638]) ).
cnf(s57,plain,
spl309_54,
inference(sat_conversion,[],[f75643]) ).
cnf(s64,plain,
( ~ spl309_47
| ~ spl309_52
| ~ spl309_54
| ~ spl309_60
| spl309_61 ),
inference(sat_conversion,[],[f75754]) ).
cnf(s65,plain,
( ~ spl309_47
| ~ spl309_51
| ~ spl309_54
| spl309_62 ),
inference(sat_conversion,[],[f75767]) ).
cnf(s67,plain,
( ~ spl309_47
| spl309_63 ),
inference(sat_conversion,[],[f75774]) ).
cnf(s74,plain,
( ~ spl309_63
| spl309_68 ),
inference(sat_conversion,[],[f75812]) ).
cnf(s83,plain,
( ~ spl309_47
| spl309_74 ),
inference(sat_conversion,[],[f75935]) ).
cnf(s85,plain,
( ~ spl309_51
| ~ spl309_74
| spl309_75 ),
inference(sat_conversion,[],[f75956]) ).
cnf(s89,plain,
( ~ spl309_51
| spl309_60
| ~ spl309_74 ),
inference(sat_conversion,[],[f75965]) ).
cnf(s94,plain,
( ~ spl309_60
| spl309_79 ),
inference(sat_conversion,[],[f76007]) ).
cnf(s95,plain,
( ~ spl309_60
| spl309_80 ),
inference(sat_conversion,[],[f76012]) ).
cnf(s96,plain,
( ~ spl309_60
| spl309_81 ),
inference(sat_conversion,[],[f76018]) ).
cnf(s97,plain,
( ~ spl309_47
| ~ spl309_54
| ~ spl309_60
| spl309_82 ),
inference(sat_conversion,[],[f76023]) ).
cnf(s100,plain,
( ~ spl309_47
| ~ spl309_60
| spl309_83 ),
inference(sat_conversion,[],[f76031]) ).
cnf(s104,plain,
( ~ spl309_60
| ~ spl309_62
| spl309_85 ),
inference(sat_conversion,[],[f76048]) ).
cnf(s105,plain,
( ~ spl309_47
| ~ spl309_60
| ~ spl309_74
| spl309_86 ),
inference(sat_conversion,[],[f76053]) ).
cnf(s110,plain,
( ~ spl309_47
| ~ spl309_52
| ~ spl309_60
| spl309_87 ),
inference(sat_conversion,[],[f76060]) ).
cnf(s111,plain,
( ~ spl309_47
| ~ spl309_51
| ~ spl309_52
| ~ spl309_60
| spl309_88 ),
inference(sat_conversion,[],[f76065]) ).
cnf(s121,plain,
( spl309_48
| ~ spl309_49
| ~ spl309_95 ),
inference(sat_conversion,[],[f76150]) ).
cnf(s123,plain,
( ~ spl309_81
| spl309_97 ),
inference(sat_conversion,[],[f76172]) ).
cnf(s124,plain,
( ~ spl309_81
| spl309_98 ),
inference(sat_conversion,[],[f76177]) ).
cnf(s129,plain,
( ~ spl309_97
| ~ spl309_98
| spl309_100 ),
inference(sat_conversion,[],[f76192]) ).
cnf(s131,plain,
( ~ spl309_81
| ~ spl309_88
| spl309_102 ),
inference(sat_conversion,[],[f76206]) ).
cnf(s137,plain,
( ~ spl309_80
| spl309_106 ),
inference(sat_conversion,[],[f76250]) ).
cnf(s139,plain,
( ~ spl309_63
| ~ spl309_80
| spl309_108 ),
inference(sat_conversion,[],[f76262]) ).
cnf(s141,plain,
( ~ spl309_52
| ~ spl309_63
| ~ spl309_80
| spl309_110 ),
inference(sat_conversion,[],[f76272]) ).
cnf(s143,plain,
( ~ spl309_52
| ~ spl309_63
| ~ spl309_80
| spl309_111 ),
inference(sat_conversion,[],[f76277]) ).
cnf(s145,plain,
( ~ spl309_111
| spl309_112 ),
inference(sat_conversion,[],[f76312]) ).
cnf(s146,plain,
( ~ spl309_111
| spl309_113 ),
inference(sat_conversion,[],[f76317]) ).
cnf(s147,plain,
( ~ spl309_111
| spl309_114 ),
inference(sat_conversion,[],[f76322]) ).
cnf(s148,plain,
( ~ spl309_111
| spl309_115 ),
inference(sat_conversion,[],[f76327]) ).
cnf(s149,plain,
( ~ spl309_47
| ~ spl309_54
| ~ spl309_111
| spl309_116 ),
inference(sat_conversion,[],[f76332]) ).
cnf(s153,plain,
( ~ spl309_47
| ~ spl309_111
| spl309_117 ),
inference(sat_conversion,[],[f76339]) ).
cnf(s167,plain,
( ~ spl309_47
| ~ spl309_74
| ~ spl309_111
| spl309_125 ),
inference(sat_conversion,[],[f76383]) ).
cnf(s173,plain,
( ~ spl309_115
| spl309_128 ),
inference(sat_conversion,[],[f76417]) ).
cnf(s174,plain,
( ~ spl309_115
| spl309_129 ),
inference(sat_conversion,[],[f76422]) ).
cnf(s175,plain,
( ~ spl309_115
| spl309_130 ),
inference(sat_conversion,[],[f76427]) ).
cnf(s179,plain,
( ~ spl309_128
| ~ spl309_129
| spl309_131 ),
inference(sat_conversion,[],[f76437]) ).
cnf(s180,plain,
( ~ spl309_128
| ~ spl309_130
| spl309_132 ),
inference(sat_conversion,[],[f76442]) ).
cnf(s181,plain,
( ~ spl309_53
| ~ spl309_115
| spl309_133 ),
inference(sat_conversion,[],[f76449]) ).
cnf(s195,plain,
( ~ spl309_113
| spl309_143 ),
inference(sat_conversion,[],[f76572]) ).
cnf(s198,plain,
( ~ spl309_63
| ~ spl309_113
| spl309_146 ),
inference(sat_conversion,[],[f76587]) ).
cnf(s202,plain,
( ~ spl309_63
| ~ spl309_113
| spl309_148 ),
inference(sat_conversion,[],[f76597]) ).
cnf(s210,plain,
( ~ spl309_82
| ~ spl309_97
| ~ spl309_108
| spl309_154 ),
inference(sat_conversion,[],[f76691]) ).
cnf(s211,plain,
( ~ spl309_79
| ~ spl309_97
| spl309_155 ),
inference(sat_conversion,[],[f76711]) ).
cnf(s215,plain,
( ~ spl309_81
| ~ spl309_87
| spl309_158 ),
inference(sat_conversion,[],[f76732]) ).
cnf(s217,plain,
( ~ spl309_116
| ~ spl309_128
| ~ spl309_148
| spl309_159 ),
inference(sat_conversion,[],[f76742]) ).
cnf(s220,plain,
( ~ spl309_112
| ~ spl309_128
| spl309_162 ),
inference(sat_conversion,[],[f76759]) ).
cnf(s252,plain,
( ~ spl309_47
| ~ spl309_111
| ~ spl309_125
| spl309_185 ),
inference(sat_conversion,[],[f77086]) ).
cnf(s278,plain,
( ~ spl309_83
| ~ spl309_102
| ~ spl309_106
| ~ spl309_108
| spl309_204 ),
inference(sat_conversion,[],[f77386]) ).
cnf(s344,plain,
( ~ spl309_117
| spl309_141
| ~ spl309_148
| ~ spl309_255 ),
inference(sat_conversion,[],[f77931]) ).
cnf(s354,plain,
( ~ spl309_48
| spl309_262 ),
inference(sat_conversion,[],[f78020]) ).
cnf(s380,plain,
( ~ spl309_100
| ~ spl309_155
| spl309_282 ),
inference(sat_conversion,[],[f78216]) ).
cnf(s386,plain,
( ~ spl309_60
| ~ spl309_85
| ~ spl309_100
| ~ spl309_154
| spl309_287 ),
inference(sat_conversion,[],[f78242]) ).
cnf(s390,plain,
( ~ spl309_68
| ~ spl309_75
| spl309_291 ),
inference(sat_conversion,[],[f78279]) ).
cnf(s392,plain,
( ~ spl309_282
| ~ spl309_291
| spl309_292 ),
inference(sat_conversion,[],[f78287]) ).
cnf(s393,plain,
( ~ spl309_87
| ~ spl309_88
| ~ spl309_292
| spl309_293 ),
inference(sat_conversion,[],[f78297]) ).
cnf(s395,plain,
( ~ spl309_74
| ~ spl309_154
| ~ spl309_291
| spl309_294 ),
inference(sat_conversion,[],[f78317]) ).
cnf(s412,plain,
( ~ spl309_83
| ~ spl309_108
| ~ spl309_294
| spl309_315
| ~ spl309_316 ),
inference(sat_conversion,[],[f78561]) ).
cnf(s478,plain,
( ~ spl309_131
| spl309_349 ),
inference(sat_conversion,[],[f79063]) ).
cnf(s479,plain,
( ~ spl309_131
| spl309_350 ),
inference(sat_conversion,[],[f79068]) ).
cnf(s494,plain,
( ~ spl309_131
| ~ spl309_162
| spl309_360 ),
inference(sat_conversion,[],[f79148]) ).
cnf(s514,plain,
( ~ spl309_114
| ~ spl309_131
| ~ spl309_132
| ~ spl309_293
| spl309_371 ),
inference(sat_conversion,[],[f79229]) ).
cnf(s535,plain,
( ~ spl309_185
| ~ spl309_292
| ~ spl309_293
| spl309_385 ),
inference(sat_conversion,[],[f79518]) ).
cnf(s537,plain,
( ~ spl309_185
| ~ spl309_292
| ~ spl309_293
| spl309_387 ),
inference(sat_conversion,[],[f79531]) ).
cnf(s552,plain,
( ~ spl309_143
| spl309_402 ),
inference(sat_conversion,[],[f79723]) ).
cnf(s553,plain,
( ~ spl309_106
| spl309_403 ),
inference(sat_conversion,[],[f79728]) ).
cnf(s556,plain,
( ~ spl309_54
| ~ spl309_68
| spl309_404 ),
inference(sat_conversion,[],[f79735]) ).
cnf(s560,plain,
( ~ spl309_68
| spl309_407 ),
inference(sat_conversion,[],[f79794]) ).
cnf(s563,plain,
( ~ spl309_85
| ~ spl309_106
| spl309_408 ),
inference(sat_conversion,[],[f79800]) ).
cnf(s616,plain,
( ~ spl309_292
| ~ spl309_403
| ~ spl309_407
| spl309_445 ),
inference(sat_conversion,[],[f81763]) ).
cnf(s618,plain,
( ~ spl309_158
| ~ spl309_293
| ~ spl309_402
| ~ spl309_407
| spl309_446 ),
inference(sat_conversion,[],[f81769]) ).
cnf(s620,plain,
( ~ spl309_445
| ~ spl309_446
| spl309_447 ),
inference(sat_conversion,[],[f81776]) ).
cnf(s792,plain,
( ~ spl309_349
| spl309_553 ),
inference(sat_conversion,[],[f83312]) ).
cnf(s807,plain,
( ~ spl309_349
| ~ spl309_371
| ~ spl309_402
| spl309_566 ),
inference(sat_conversion,[],[f83413]) ).
cnf(s808,plain,
( ~ spl309_349
| ~ spl309_360
| ~ spl309_402
| spl309_567 ),
inference(sat_conversion,[],[f83418]) ).
cnf(s839,plain,
( ~ spl309_106
| ~ spl309_408
| spl309_582 ),
inference(sat_conversion,[],[f83735]) ).
cnf(s841,plain,
( ~ spl309_68
| ~ spl309_404
| ~ spl309_445
| spl309_583 ),
inference(sat_conversion,[],[f83744]) ).
cnf(s842,plain,
( ~ spl309_553
| ~ spl309_566
| ~ spl309_567
| spl309_584 ),
inference(sat_conversion,[],[f83749]) ).
cnf(s858,plain,
( spl309_316
| ~ spl309_385
| ~ spl309_387
| ~ spl309_403
| ~ spl309_583 ),
inference(sat_conversion,[],[f83763]) ).
cnf(s864,plain,
( ~ spl309_141
| ~ spl309_402
| spl309_589 ),
inference(sat_conversion,[],[f83813]) ).
cnf(s873,plain,
( ~ spl309_61
| ~ spl309_402
| ~ spl309_589
| spl309_594 ),
inference(sat_conversion,[],[f83862]) ).
cnf(s1091,plain,
( ~ spl309_146
| ~ spl309_148
| spl309_719 ),
inference(sat_conversion,[],[f87169]) ).
cnf(s1131,plain,
( ~ spl309_719
| spl309_746 ),
inference(sat_conversion,[],[f87467]) ).
cnf(s1444,plain,
( ~ spl309_68
| ~ spl309_106
| ~ spl309_110
| ~ spl309_445
| ~ spl309_447
| ~ spl309_594
| spl309_962 ),
inference(sat_conversion,[],[f91554]) ).
cnf(s1534,plain,
( ~ spl309_159
| ~ spl309_350
| ~ spl309_746
| spl309_1034 ),
inference(sat_conversion,[],[f92980]) ).
cnf(s1540,plain,
( ~ spl309_85
| ~ spl309_86
| ~ spl309_102
| ~ spl309_108
| ~ spl309_204
| spl309_255
| ~ spl309_287
| ~ spl309_291
| ~ spl309_315
| ~ spl309_402
| ~ spl309_403
| ~ spl309_582
| ~ spl309_584
| ~ spl309_746
| ~ spl309_1034 ),
inference(sat_conversion,[],[f92997]) ).
cnf(s3575,plain,
( spl309_49
| ~ spl309_68
| ~ spl309_75
| ~ spl309_106
| ~ spl309_110
| ~ spl309_133
| ~ spl309_262
| ~ spl309_404 ),
inference(sat_conversion,[],[f167294]) ).
cnf(s3625,plain,
( spl309_95
| ~ spl309_133
| ~ spl309_143
| ~ spl309_962 ),
inference(sat_conversion,[],[f167705]) ).
cnf(s3656,plain,
spl309_74,
inference(rat,[],[s83,s50]) ).
cnf(s3658,plain,
spl309_63,
inference(rat,[],[s67,s50]) ).
cnf(s3659,plain,
spl309_62,
inference(rat,[],[s65,s54,s57,s50]) ).
cnf(s3661,plain,
spl309_75,
inference(rat,[],[s85,s54,s3656]) ).
cnf(s3662,plain,
spl309_60,
inference(rat,[],[s89,s54,s3656]) ).
cnf(s3674,plain,
spl309_68,
inference(rat,[],[s74,s3658]) ).
cnf(s3678,plain,
spl309_86,
inference(rat,[],[s105,s3656,s50,s3662]) ).
cnf(s3679,plain,
spl309_85,
inference(rat,[],[s104,s3659,s3662]) ).
cnf(s3681,plain,
spl309_83,
inference(rat,[],[s100,s50,s3662]) ).
cnf(s3682,plain,
spl309_81,
inference(rat,[],[s96,s3662]) ).
cnf(s3683,plain,
spl309_80,
inference(rat,[],[s95,s3662]) ).
cnf(s3684,plain,
spl309_79,
inference(rat,[],[s94,s3662]) ).
cnf(s3685,plain,
spl309_82,
inference(rat,[],[s97,s50,s57,s3662]) ).
cnf(s3686,plain,
spl309_87,
inference(rat,[],[s110,s50,s55,s3662]) ).
cnf(s3688,plain,
spl309_61,
inference(rat,[],[s64,s50,s55,s57,s3662]) ).
cnf(s3689,plain,
spl309_88,
inference(rat,[],[s111,s50,s54,s55,s3662]) ).
cnf(s3691,plain,
spl309_407,
inference(rat,[],[s560,s3674]) ).
cnf(s3692,plain,
spl309_404,
inference(rat,[],[s556,s57,s3674]) ).
cnf(s3693,plain,
spl309_291,
inference(rat,[],[s390,s3661,s3674]) ).
cnf(s3698,plain,
spl309_98,
inference(rat,[],[s124,s3682]) ).
cnf(s3699,plain,
spl309_97,
inference(rat,[],[s123,s3682]) ).
cnf(s3712,plain,
spl309_108,
inference(rat,[],[s139,s3658,s3683]) ).
cnf(s3714,plain,
spl309_106,
inference(rat,[],[s137,s3683]) ).
cnf(s3716,plain,
spl309_111,
inference(rat,[],[s143,s3658,s55,s3683]) ).
cnf(s3717,plain,
spl309_110,
inference(rat,[],[s141,s3658,s55,s3683]) ).
cnf(s3719,plain,
spl309_158,
inference(rat,[],[s215,s3682,s3686]) ).
cnf(s3732,plain,
spl309_102,
inference(rat,[],[s131,s3682,s3689]) ).
cnf(s3735,plain,
spl309_155,
inference(rat,[],[s211,s3684,s3699]) ).
cnf(s3736,plain,
spl309_154,
inference(rat,[],[s210,s3685,s3712,s3699]) ).
cnf(s3738,plain,
spl309_100,
inference(rat,[],[s129,s3698,s3699]) ).
cnf(s3759,plain,
spl309_408,
inference(rat,[],[s563,s3679,s3714]) ).
cnf(s3760,plain,
spl309_403,
inference(rat,[],[s553,s3714]) ).
cnf(s3778,plain,
spl309_117,
inference(rat,[],[s153,s50,s3716]) ).
cnf(s3779,plain,
spl309_115,
inference(rat,[],[s148,s3716]) ).
cnf(s3780,plain,
spl309_114,
inference(rat,[],[s147,s3716]) ).
cnf(s3781,plain,
spl309_113,
inference(rat,[],[s146,s3716]) ).
cnf(s3782,plain,
spl309_112,
inference(rat,[],[s145,s3716]) ).
cnf(s3783,plain,
spl309_116,
inference(rat,[],[s149,s50,s57,s3716]) ).
cnf(s3784,plain,
spl309_125,
inference(rat,[],[s167,s3656,s50,s3716]) ).
cnf(s3791,plain,
spl309_204,
inference(rat,[],[s278,s3714,s3712,s3681,s3732]) ).
cnf(s3795,plain,
spl309_294,
inference(rat,[],[s395,s3693,s3656,s3736]) ).
cnf(s3797,plain,
spl309_282,
inference(rat,[],[s380,s3735,s3738]) ).
cnf(s3808,plain,
spl309_287,
inference(rat,[],[s386,s3736,s3679,s3662,s3738]) ).
cnf(s3836,plain,
spl309_582,
inference(rat,[],[s839,s3714,s3759]) ).
cnf(s3841,plain,
spl309_133,
inference(rat,[],[s181,s56,s3779]) ).
cnf(s3842,plain,
spl309_130,
inference(rat,[],[s175,s3779]) ).
cnf(s3843,plain,
spl309_129,
inference(rat,[],[s174,s3779]) ).
cnf(s3844,plain,
spl309_128,
inference(rat,[],[s173,s3779]) ).
cnf(s3854,plain,
spl309_148,
inference(rat,[],[s202,s3658,s3781]) ).
cnf(s3856,plain,
spl309_146,
inference(rat,[],[s198,s3658,s3781]) ).
cnf(s3859,plain,
spl309_143,
inference(rat,[],[s195,s3781]) ).
cnf(s3861,plain,
spl309_185,
inference(rat,[],[s252,s3716,s50,s3784]) ).
cnf(s3873,plain,
spl309_292,
inference(rat,[],[s392,s3693,s3797]) ).
cnf(s3903,plain,
spl309_162,
inference(rat,[],[s220,s3782,s3844]) ).
cnf(s3904,plain,
spl309_159,
inference(rat,[],[s217,s3783,s3854,s3844]) ).
cnf(s3905,plain,
spl309_132,
inference(rat,[],[s180,s3842,s3844]) ).
cnf(s3906,plain,
spl309_131,
inference(rat,[],[s179,s3843,s3844]) ).
cnf(s3927,plain,
spl309_719,
inference(rat,[],[s1091,s3854,s3856]) ).
cnf(s3966,plain,
spl309_402,
inference(rat,[],[s552,s3859]) ).
cnf(s4009,plain,
spl309_445,
inference(rat,[],[s616,s3760,s3691,s3873]) ).
cnf(s4013,plain,
spl309_293,
inference(rat,[],[s393,s3689,s3686,s3873]) ).
cnf(s4049,plain,
spl309_371,
inference(rat,[],[s514,s3905,s4013,s3780,s3906]) ).
cnf(s4053,plain,
spl309_360,
inference(rat,[],[s494,s3903,s3906]) ).
cnf(s4062,plain,
spl309_350,
inference(rat,[],[s479,s3906]) ).
cnf(s4063,plain,
spl309_349,
inference(rat,[],[s478,s3906]) ).
cnf(s4113,plain,
spl309_746,
inference(rat,[],[s1131,s3927]) ).
cnf(s4164,plain,
spl309_583,
inference(rat,[],[s841,s3692,s3674,s4009]) ).
cnf(s4167,plain,
spl309_446,
inference(rat,[],[s618,s3966,s3691,s3719,s4013]) ).
cnf(s4193,plain,
spl309_387,
inference(rat,[],[s537,s3873,s3861,s4013]) ).
cnf(s4195,plain,
spl309_385,
inference(rat,[],[s535,s3873,s3861,s4013]) ).
cnf(s4223,plain,
spl309_567,
inference(rat,[],[s808,s4053,s3966,s4063]) ).
cnf(s4224,plain,
spl309_566,
inference(rat,[],[s807,s4049,s3966,s4063]) ).
cnf(s4230,plain,
spl309_553,
inference(rat,[],[s792,s4063]) ).
cnf(s4276,plain,
spl309_1034,
inference(rat,[],[s1534,s4062,s3904,s4113]) ).
cnf(s4306,plain,
spl309_447,
inference(rat,[],[s620,s4009,s4167]) ).
cnf(s4311,plain,
spl309_316,
inference(rat,[],[s858,s4164,s3760,s4193,s4195]) ).
cnf(s4320,plain,
spl309_584,
inference(rat,[],[s842,s4224,s4223,s4230]) ).
cnf(s4347,plain,
spl309_315,
inference(rat,[],[s412,s3795,s3712,s3681,s4311]) ).
cnf(s4352,plain,
spl309_255,
inference(rat,[],[s1540,s4276,s4113,s4320,s3836,s3760,s3966,s3791,s3693,s3808,s3732,s3712,s3679,s3678,s4347]) ).
cnf(s4355,plain,
spl309_141,
inference(rat,[],[s344,s3854,s3778,s4352]) ).
cnf(s4357,plain,
spl309_589,
inference(rat,[],[s864,s3966,s4355]) ).
cnf(s4361,plain,
spl309_594,
inference(rat,[],[s873,s3966,s3688,s4357]) ).
cnf(s4409,plain,
spl309_962,
inference(rat,[],[s1444,s4306,s4009,s3717,s3714,s3674,s4361]) ).
cnf(s4451,plain,
spl309_95,
inference(rat,[],[s3625,s3841,s3859,s4409]) ).
cnf(s4671,plain,
spl309_48,
inference(rat,[],[s51,s121,s4451]) ).
cnf(s4712,plain,
spl309_262,
inference(rat,[],[s354,s4671]) ).
cnf(s4721,plain,
~ spl309_49,
inference(rat,[],[s52,s4671]) ).
cnf(s4891,plain,
$false,
inference(rat,[],[s3575,s3692,s3841,s3714,s3717,s3674,s3661,s4712,s4721]) ).
fof(f167868,plain,
$false,
inference(avatar_sat_refutation,[],[s4891]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU442+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 % Computer : n018.cluster.edu
% 0.13/0.42 % Model : x86_64 x86_64
% 0.13/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.42 % Memory : 8046.5625MB
% 0.13/0.42 % OS : Linux 6.8.0-71-generic
% 0.13/0.42 % CPULimit : 300
% 0.13/0.42 % WCLimit : 300
% 0.13/0.42 % DateTime : Mon Sep 28 05:33:50 UTC 2026
% 0.13/0.42 % CPUTime :
% 0.13/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.22/0.47 Running first-order theorem proving
% 0.22/0.48 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
% 33.85/11.66 % (3065376)Detected formulas, will run a generic FOF schedule.
% 33.85/11.66 % (3065388)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=19589263:i=141193_2931 on theBenchmark for (2931ds/141193Mi)
% 33.85/11.66 % (3065391)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2164334625:i=109:sd=1:ins=1:gsp=on:ss=axioms_2931 on theBenchmark for (2931ds/109Mi)
% 33.85/11.66 % (3065390)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=2502164296:i=141695:sd=1:nm=32:gsp=on:ss=included_2931 on theBenchmark for (2931ds/141695Mi)
% 33.85/11.66 % (3065389)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=1343646510:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2931 on theBenchmark for (2931ds/134677Mi)
% 33.85/11.66 % (3065394)dis-21_1_sil=8000:lcm=predicate:random_seed=3116141921:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2931 on theBenchmark for (2931ds/129Mi)
% 33.85/11.66 % (3065392)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1178467535:i=119:av=off:ss=axioms_2931 on theBenchmark for (2931ds/119Mi)
% 33.85/11.66 % (3065393)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3780512517:s2a=on:i=139:gtg=position_2931 on theBenchmark for (2931ds/139Mi)
% 33.85/11.66 % (3065391)Instruction limit reached!
% 33.85/11.66 % (3065391)------------------------------
% 33.85/11.66 % (3065391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.85/11.66 % (3065391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.85/11.66 % (3065391)CaDiCaL version: 2.1.3
% 33.85/11.66 % (3065391)Termination reason: Instruction limit
% 33.85/11.66 % (3065391)Termination phase: SInE selection
% 33.85/11.66 % (3065391)Time elapsed: 0.118 s
% 33.85/11.66 % (3065391)Peak memory usage: 201 MB
% 33.85/11.66 % (3065391)Instructions burned: 109 (million)
% 33.85/11.66 % (3065394)Instruction limit reached!
% 33.85/11.66 % (3065394)------------------------------
% 33.85/11.66 % (3065394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.85/11.66 % (3065394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.85/11.66 % (3065394)CaDiCaL version: 2.1.3
% 33.85/11.66 % (3065394)Termination reason: Instruction limit
% 33.85/11.66 % (3065394)Termination phase: SInE selection
% 33.85/11.66 % (3065394)Time elapsed: 0.141 s
% 33.85/11.66 % (3065394)Peak memory usage: 201 MB
% 33.85/11.66 % (3065394)Instructions burned: 131 (million)
% 33.85/11.66 % (3065393)Instruction limit reached!
% 33.85/11.66 % (3065393)------------------------------
% 33.85/11.66 % (3065393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.85/11.66 % (3065393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.85/11.66 % (3065393)CaDiCaL version: 2.1.3
% 33.85/11.66 % (3065393)Termination reason: Instruction limit
% 33.85/11.66 % (3065393)Termination phase: Property scanning
% 33.85/11.66 % (3065393)Time elapsed: 0.128 s
% 33.85/11.66 % (3065393)Peak memory usage: 201 MB
% 33.85/11.66 % (3065393)Instructions burned: 140 (million)
% 33.85/11.66 % (3065392)Instruction limit reached!
% 33.85/11.66 % (3065392)------------------------------
% 33.85/11.66 % (3065392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.85/11.66 % (3065392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.85/11.66 % (3065392)CaDiCaL version: 2.1.3
% 33.85/11.66 % (3065392)Termination reason: Instruction limit
% 33.85/11.66 % (3065392)Termination phase: SInE selection
% 33.85/11.66 % (3065392)Time elapsed: 0.136 s
% 33.85/11.66 % (3065392)Peak memory usage: 201 MB
% 33.85/11.66 % (3065392)Instructions burned: 120 (million)
% 33.85/11.66 % (3065402)lrs+10_1_sil=8000:sp=occurrence:random_seed=3823757540:i=285:sd=3:ss=axioms:sgt=8_2927 on theBenchmark for (2927ds/285Mi)
% 33.85/11.66 % (3065405)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=576646921:s2a=on:i=248:s2at=1.23:gtg=position_2926 on theBenchmark for (2926ds/248Mi)
% 33.85/11.66 % (3065403)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2841773692:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2927 on theBenchmark for (2927ds/157Mi)
% 33.85/11.66 % (3065404)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4181263606:i=325:sd=1:ss=axioms:sgt=32_2926 on theBenchmark for (2926ds/325Mi)
% 33.85/11.66 % (3065403)Instruction limit reached!
% 46.09/13.34 % (3065403)------------------------------
% 46.09/13.34 % (3065403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.09/13.34 % (3065403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.09/13.34 % (3065403)CaDiCaL version: 2.1.3
% 46.09/13.34 % (3065403)Termination reason: Instruction limit
% 46.09/13.34 % (3065403)Termination phase: Property scanning
% 46.09/13.34 % (3065403)Time elapsed: 0.141 s
% 46.09/13.34 % (3065403)Peak memory usage: 201 MB
% 46.09/13.34 % (3065403)Instructions burned: 157 (million)
% 46.09/13.34 % (3065405)Instruction limit reached!
% 46.09/13.34 % (3065405)------------------------------
% 46.09/13.34 % (3065405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.09/13.34 % (3065405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.09/13.34 % (3065405)CaDiCaL version: 2.1.3
% 46.09/13.34 % (3065405)Termination reason: Instruction limit
% 46.09/13.34 % (3065405)Termination phase: Property scanning
% 46.09/13.34 % (3065405)Time elapsed: 0.201 s
% 46.09/13.34 % (3065405)Peak memory usage: 201 MB
% 46.09/13.34 % (3065405)Instructions burned: 249 (million)
% 46.09/13.34 % (3065402)Instruction limit reached!
% 46.09/13.34 % (3065402)------------------------------
% 46.09/13.34 % (3065402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.09/13.34 % (3065402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.09/13.34 % (3065402)CaDiCaL version: 2.1.3
% 46.09/13.34 % (3065402)Termination reason: Instruction limit
% 46.09/13.34 % (3065402)Termination phase: SInE selection
% 46.09/13.34 % (3065402)Time elapsed: 0.307 s
% 46.09/13.34 % (3065402)Peak memory usage: 201 MB
% 46.09/13.34 % (3065402)Instructions burned: 286 (million)
% 46.09/13.34 % (3065410)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=63004020:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2923 on theBenchmark for (2923ds/294Mi)
% 46.09/13.34 % (3065404)Instruction limit reached!
% 46.09/13.34 % (3065404)------------------------------
% 46.09/13.34 % (3065404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.09/13.34 % (3065404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.09/13.34 % (3065404)CaDiCaL version: 2.1.3
% 46.09/13.34 % (3065404)Termination reason: Instruction limit
% 46.09/13.34 % (3065404)Termination phase: SInE selection
% 46.09/13.34 % (3065404)Time elapsed: 0.352 s
% 46.09/13.34 % (3065404)Peak memory usage: 201 MB
% 46.09/13.34 % (3065404)Instructions burned: 326 (million)
% 46.09/13.34 % (3065411)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4068514801:i=2350_2922 on theBenchmark for (2922ds/2350Mi)
% 46.09/13.34 % (3065412)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3198059754:cts=off:i=113:fsr=off:ss=included:sgt=4_2921 on theBenchmark for (2921ds/113Mi)
% 46.09/13.34 % (3065412)Instruction limit reached!
% 46.09/13.34 % (3065412)------------------------------
% 46.09/13.34 % (3065412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.09/13.34 % (3065412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.09/13.34 % (3065412)CaDiCaL version: 2.1.3
% 46.09/13.34 % (3065412)Termination reason: Instruction limit
% 46.09/13.34 % (3065412)Termination phase: SInE selection
% 46.09/13.34 % (3065412)Time elapsed: 0.126 s
% 46.09/13.34 % (3065412)Peak memory usage: 201 MB
% 46.09/13.34 % (3065412)Instructions burned: 113 (million)
% 46.09/13.34 % (3065410)Instruction limit reached!
% 46.09/13.34 % (3065410)------------------------------
% 46.09/13.34 % (3065410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.09/13.34 % (3065410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.09/13.34 % (3065410)CaDiCaL version: 2.1.3
% 46.09/13.34 % (3065410)Termination reason: Instruction limit
% 46.09/13.34 % (3065410)Termination phase: SInE selection
% 46.09/13.34 % (3065410)Time elapsed: 0.317 s
% 46.09/13.34 % (3065410)Peak memory usage: 201 MB
% 46.09/13.34 % (3065410)Instructions burned: 294 (million)
% 46.09/13.34 % (3065414)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2200775193:i=127:av=off:fsr=off:sup=off_2920 on theBenchmark for (2920ds/127Mi)
% 46.09/13.34 % (3065414)Instruction limit reached!
% 46.09/13.34 % (3065414)------------------------------
% 46.09/13.34 % (3065414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.09/13.34 % (3065414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.09/13.34 % (3065414)CaDiCaL version: 2.1.3
% 108.20/22.10 % (3065414)Termination reason: Instruction limit
% 108.20/22.10 % (3065414)Termination phase: Preprocessing 1
% 108.20/22.10 % (3065414)Time elapsed: 0.153 s
% 108.20/22.10 % (3065414)Peak memory usage: 202 MB
% 108.20/22.10 % (3065414)Instructions burned: 127 (million)
% 108.20/22.10 % (3065418)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2396109341:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2917 on theBenchmark for (2917ds/114Mi)
% 108.20/22.10 % (3065419)lrs+10_1_sil=8000:sp=occurrence:random_seed=1366751065:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2917 on theBenchmark for (2917ds/907Mi)
% 108.20/22.10 % (3065418)Instruction limit reached!
% 108.20/22.10 % (3065418)------------------------------
% 108.20/22.10 % (3065418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.20/22.10 % (3065418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.20/22.10 % (3065418)CaDiCaL version: 2.1.3
% 108.20/22.10 % (3065418)Termination reason: Instruction limit
% 108.20/22.10 % (3065418)Termination phase: Property scanning
% 108.20/22.10 % (3065418)Time elapsed: 0.108 s
% 108.20/22.10 % (3065418)Peak memory usage: 201 MB
% 108.20/22.10 % (3065418)Instructions burned: 115 (million)
% 108.20/22.10 % (3065420)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=982658647:i=437:sd=1:aac=none:ss=included_2915 on theBenchmark for (2915ds/437Mi)
% 108.20/22.10 % (3065423)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=749218008:i=5202:ss=axioms:sgt=16_2913 on theBenchmark for (2913ds/5202Mi)
% 108.20/22.10 % (3065420)Instruction limit reached!
% 108.20/22.10 % (3065420)------------------------------
% 108.20/22.10 % (3065420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.20/22.10 % (3065420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.20/22.10 % (3065420)CaDiCaL version: 2.1.3
% 108.20/22.10 % (3065420)Termination reason: Instruction limit
% 108.20/22.10 % (3065420)Termination phase: SInE selection
% 108.20/22.10 % (3065420)Time elapsed: 0.460 s
% 108.20/22.10 % (3065420)Peak memory usage: 201 MB
% 108.20/22.10 % (3065420)Instructions burned: 437 (million)
% 108.20/22.10 % (3065428)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3856383306:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2908 on theBenchmark for (2908ds/134Mi)
% 108.20/22.10 % (3065419)Instruction limit reached!
% 108.20/22.10 % (3065419)------------------------------
% 108.20/22.10 % (3065419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.20/22.10 % (3065419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.20/22.10 % (3065419)CaDiCaL version: 2.1.3
% 108.20/22.10 % (3065419)Termination reason: Instruction limit
% 108.20/22.10 % (3065419)Termination phase: Preprocessing 1
% 108.20/22.10 % (3065419)Time elapsed: 0.993 s
% 108.20/22.10 % (3065419)Peak memory usage: 204 MB
% 108.20/22.10 % (3065419)Instructions burned: 907 (million)
% 108.20/22.10 % (3065428)Instruction limit reached!
% 108.20/22.10 % (3065428)------------------------------
% 108.20/22.10 % (3065428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.20/22.10 % (3065428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.20/22.10 % (3065428)CaDiCaL version: 2.1.3
% 108.20/22.10 % (3065428)Termination reason: Instruction limit
% 108.20/22.10 % (3065428)Termination phase: SInE selection
% 108.20/22.10 % (3065428)Time elapsed: 0.147 s
% 108.20/22.10 % (3065428)Peak memory usage: 201 MB
% 108.20/22.10 % (3065428)Instructions burned: 134 (million)
% 108.20/22.10 % (3065430)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2841970862:st=8:i=592:sd=3:ep=RST:ss=axioms_2905 on theBenchmark for (2905ds/592Mi)
% 108.20/22.10 % (3065431)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1117829608:st=3:i=13193:sd=3:ss=axioms_2903 on theBenchmark for (2903ds/13193Mi)
% 108.20/22.10 % (3065430)Instruction limit reached!
% 108.20/22.10 % (3065430)------------------------------
% 108.20/22.10 % (3065430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.20/22.10 % (3065430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.20/22.10 % (3065430)CaDiCaL version: 2.1.3
% 108.20/22.10 % (3065430)Termination reason: Instruction limit
% 108.20/22.10 % (3065430)Termination phase: SInE selection
% 108.20/22.10 % (3065430)Time elapsed: 0.586 s
% 108.20/22.10 % (3065430)Peak memory usage: 203 MB
% 108.20/22.10 % (3065430)Instructions burned: 592 (million)
% 108.20/22.10 % (3065434)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=1373520014:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2896 on theBenchmark for (2896ds/125Mi)
% 74.74/25.37 % (3065411)Instruction limit reached!
% 74.74/25.37 % (3065411)------------------------------
% 74.74/25.37 % (3065411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065411)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065411)Termination reason: Instruction limit
% 74.74/25.37 % (3065411)Termination phase: Preprocessing 3
% 74.74/25.37 % (3065411)Time elapsed: 2.725 s
% 74.74/25.37 % (3065411)Peak memory usage: 305 MB
% 74.74/25.37 % (3065411)Instructions burned: 2350 (million)
% 74.74/25.37 % (3065434)Instruction limit reached!
% 74.74/25.37 % (3065434)------------------------------
% 74.74/25.37 % (3065434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065434)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065434)Termination reason: Instruction limit
% 74.74/25.37 % (3065434)Termination phase: Property scanning
% 74.74/25.37 % (3065434)Time elapsed: 0.115 s
% 74.74/25.37 % (3065434)Peak memory usage: 201 MB
% 74.74/25.37 % (3065434)Instructions burned: 126 (million)
% 74.74/25.37 % (3065436)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2159709385:i=134:gtgl=5:slsql=off:gtg=exists_sym_2891 on theBenchmark for (2891ds/134Mi)
% 74.74/25.37 % (3065437)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=475609676:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2891 on theBenchmark for (2891ds/141Mi)
% 74.74/25.37 % (3065436)Instruction limit reached!
% 74.74/25.37 % (3065436)------------------------------
% 74.74/25.37 % (3065436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065436)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065436)Termination reason: Instruction limit
% 74.74/25.37 % (3065436)Termination phase: Property scanning
% 74.74/25.37 % (3065436)Time elapsed: 0.123 s
% 74.74/25.37 % (3065436)Peak memory usage: 201 MB
% 74.74/25.37 % (3065436)Instructions burned: 134 (million)
% 74.74/25.37 % (3065437)Instruction limit reached!
% 74.74/25.37 % (3065437)------------------------------
% 74.74/25.37 % (3065437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065437)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065437)Termination reason: Instruction limit
% 74.74/25.37 % (3065437)Termination phase: SInE selection
% 74.74/25.37 % (3065437)Time elapsed: 0.156 s
% 74.74/25.37 % (3065437)Peak memory usage: 201 MB
% 74.74/25.37 % (3065437)Instructions burned: 141 (million)
% 74.74/25.37 % (3065440)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3111451488:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2888 on theBenchmark for (2888ds/431Mi)
% 74.74/25.37 % (3065441)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=2877849134:i=6060:aac=none:ins=25_2887 on theBenchmark for (2887ds/6060Mi)
% 74.74/25.37 % (3065440)Instruction limit reached!
% 74.74/25.37 % (3065440)------------------------------
% 74.74/25.37 % (3065440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065440)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065440)Termination reason: Instruction limit
% 74.74/25.37 % (3065440)Termination phase: SInE selection
% 74.74/25.37 % (3065440)Time elapsed: 0.460 s
% 74.74/25.37 % (3065440)Peak memory usage: 202 MB
% 74.74/25.37 % (3065440)Instructions burned: 431 (million)
% 74.74/25.37 % (3065444)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=3100595660:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2880 on theBenchmark for (2880ds/150Mi)
% 74.74/25.37 % (3065444)Instruction limit reached!
% 74.74/25.37 % (3065444)------------------------------
% 74.74/25.37 % (3065444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065444)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065444)Termination reason: Instruction limit
% 74.74/25.37 % (3065444)Termination phase: SInE selection
% 74.74/25.37 % (3065444)Time elapsed: 0.168 s
% 74.74/25.37 % (3065444)Peak memory usage: 201 MB
% 74.74/25.37 % (3065444)Instructions burned: 150 (million)
% 74.74/25.37 % (3065446)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=714824254:i=14155:bd=all_2876 on theBenchmark for (2876ds/14155Mi)
% 74.74/25.37 % (3065423)Instruction limit reached!
% 74.74/25.37 % (3065423)------------------------------
% 74.74/25.37 % (3065423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065423)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065423)Termination reason: Instruction limit
% 74.74/25.37 % (3065423)Termination phase: Property scanning
% 74.74/25.37 % (3065423)Time elapsed: 5.417 s
% 74.74/25.37 % (3065423)Peak memory usage: 333 MB
% 74.74/25.37 % (3065423)Instructions burned: 5202 (million)
% 74.74/25.37 % (3065450)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3716371015:i=667:av=off:fsr=off_2856 on theBenchmark for (2856ds/667Mi)
% 74.74/25.37 % (3065450)Instruction limit reached!
% 74.74/25.37 % (3065450)------------------------------
% 74.74/25.37 % (3065450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065450)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065450)Termination reason: Instruction limit
% 74.74/25.37 % (3065450)Termination phase: Preprocessing 2
% 74.74/25.37 % (3065450)Time elapsed: 0.885 s
% 74.74/25.37 % (3065450)Peak memory usage: 218 MB
% 74.74/25.37 % (3065450)Instructions burned: 667 (million)
% 74.74/25.37 % (3065454)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=1987929908:s2a=on:i=185:s2at=1.8:fdi=4_2844 on theBenchmark for (2844ds/185Mi)
% 74.74/25.37 % (3065454)Instruction limit reached!
% 74.74/25.37 % (3065454)------------------------------
% 74.74/25.37 % (3065454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065454)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065454)Termination reason: Instruction limit
% 74.74/25.37 % (3065454)Termination phase: SInE selection
% 74.74/25.37 % (3065454)Time elapsed: 0.188 s
% 74.74/25.37 % (3065454)Peak memory usage: 201 MB
% 74.74/25.37 % (3065454)Instructions burned: 185 (million)
% 74.74/25.37 % (3065456)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3417336103:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2840 on theBenchmark for (2840ds/193Mi)
% 74.74/25.37 % (3065456)Instruction limit reached!
% 74.74/25.37 % (3065456)------------------------------
% 74.74/25.37 % (3065456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065456)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065456)Termination reason: Instruction limit
% 74.74/25.37 % (3065456)Termination phase: SInE selection
% 74.74/25.37 % (3065456)Time elapsed: 0.230 s
% 74.74/25.37 % (3065456)Peak memory usage: 201 MB
% 74.74/25.37 % (3065456)Instructions burned: 193 (million)
% 74.74/25.37 % (3065458)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=946873977:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2834 on theBenchmark for (2834ds/4850Mi)
% 74.74/25.37 % (3065441)Instruction limit reached!
% 74.74/25.37 % (3065441)------------------------------
% 74.74/25.37 % (3065441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065441)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065441)Termination reason: Instruction limit
% 74.74/25.37 % (3065441)Termination phase: NewCNF
% 74.74/25.37 % (3065441)Time elapsed: 6.726 s
% 74.74/25.37 % (3065441)Peak memory usage: 381 MB
% 74.74/25.37 % (3065441)Instructions burned: 6060 (million)
% 74.74/25.37 % (3065462)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3863827510:i=12111:sd=1:ss=included_2816 on theBenchmark for (2816ds/12111Mi)
% 74.74/25.37 % (3065458)Instruction limit reached!
% 74.74/25.37 % (3065458)------------------------------
% 74.74/25.37 % (3065458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065458)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065458)Termination reason: Instruction limit
% 74.74/25.37 % (3065458)Termination phase: Property scanning
% 74.74/25.37 % (3065458)Time elapsed: 4.299 s
% 74.74/25.37 % (3065458)Peak memory usage: 362 MB
% 74.74/25.37 % (3065458)Instructions burned: 4850 (million)
% 74.74/25.37 % (3065617)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2851433076:i=319:kws=precedence:fsr=off_2788 on theBenchmark for (2788ds/319Mi)
% 74.74/25.37 % (3065617)Instruction limit reached!
% 74.74/25.37 % (3065617)------------------------------
% 74.74/25.37 % (3065617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065617)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065617)Termination reason: Instruction limit
% 74.74/25.37 % (3065617)Termination phase: Preprocessing 1
% 74.74/25.37 % (3065617)Time elapsed: 0.245 s
% 74.74/25.37 % (3065617)Peak memory usage: 203 MB
% 74.74/25.37 % (3065617)Instructions burned: 319 (million)
% 74.74/25.37 % (3065431)Instruction limit reached!
% 74.74/25.37 % (3065431)------------------------------
% 74.74/25.37 % (3065431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065431)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065431)Termination reason: Instruction limit
% 74.74/25.37 % (3065431)Termination phase: Saturation
% 74.74/25.37 % (3065431)Time elapsed: 11.814 s
% 74.74/25.37 % (3065431)Peak memory usage: 623 MB
% 74.74/25.37 % (3065431)Instructions burned: 13193 (million)
% 74.74/25.37 % (3065619)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3906188414:i=2064:ep=RST_2783 on theBenchmark for (2783ds/2064Mi)
% 74.74/25.37 % (3065621)dis-1011_128_sil=32000:random_seed=2115760407:i=3706:ep=RST:av=off_2782 on theBenchmark for (2782ds/3706Mi)
% 74.74/25.37 % (3065446)Instruction limit reached!
% 74.74/25.37 % (3065446)------------------------------
% 74.74/25.37 % (3065446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065446)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065446)Termination reason: Instruction limit
% 74.74/25.37 % (3065446)Termination phase: Property scanning
% 74.74/25.37 % (3065446)Time elapsed: 9.929 s
% 74.74/25.37 % (3065446)Peak memory usage: 447 MB
% 74.74/25.37 % (3065446)Instructions burned: 14157 (million)
% 74.74/25.37 % (3065623)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3827430575:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2773 on theBenchmark for (2773ds/757Mi)
% 74.74/25.37 % (3065619)Instruction limit reached!
% 74.74/25.37 % (3065619)------------------------------
% 74.74/25.37 % (3065619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065619)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065619)Termination reason: Instruction limit
% 74.74/25.37 % (3065619)Termination phase: Preprocessing 3
% 74.74/25.37 % (3065619)Time elapsed: 1.584 s
% 74.74/25.37 % (3065619)Peak memory usage: 317 MB
% 74.74/25.37 % (3065619)Instructions burned: 2065 (million)
% 74.74/25.37 % (3065623)Instruction limit reached!
% 74.74/25.37 % (3065623)------------------------------
% 74.74/25.37 % (3065623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/25.37 % (3065623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/25.37 % (3065623)CaDiCaL version: 2.1.3
% 74.74/25.37 % (3065623)Termination reason: Instruction limit
% 74.74/25.37 % (3065623)Termination phase: Saturation
% 74.74/25.37 % (3065623)Time elapsed: 0.586 s
% 74.74/25.37 % (3065623)Peak memory usage: 211 MB
% 74.74/25.37 % (3065623)Instructions burned: 758 (million)
% 74.74/25.37 % (3065625)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3765422912:i=13913:ss=axioms:sgt=8_2765 on theBenchmark for (2765ds/13913Mi)
% 74.74/25.37 % (3065626)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1889399143:i=9925:aac=none_2765 on theBenchmark for (2765ds/9925Mi)
% 74.74/25.37 % (3065462)First to succeed.
% 74.74/25.37 % (3065462)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3065376"
% 74.74/25.37 % (3065462)Refutation found. Thanks to Tanya!
% 74.74/25.37 % SZS status Theorem for theBenchmark
% 74.74/25.37 % SZS output start Proof for theBenchmark
% See solution above
% 131.64/25.64 % (3065462)------------------------------
% 131.64/25.64 % (3065462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.64/25.64 % (3065462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.64/25.64 % (3065462)CaDiCaL version: 2.1.3
% 131.64/25.64 % (3065462)Termination reason: Refutation
% 131.64/25.64 % (3065462)Time elapsed: 5.365 s
% 131.64/25.64 % (3065462)Peak memory usage: 324 MB
% 131.64/25.64 % (3065462)Instructions burned: 7613 (million)
% 131.64/25.64 % (3065462)------------------------------
% 131.64/25.64 % (3065462)------------------------------
% 131.64/25.64 % (3065376)Success in time 24.405 s
% 131.64/25.64 % Vampire exiting
%------------------------------------------------------------------------------