%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG232+2 : 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 : n009.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 09:19:31 AM UTC 2026
% Result : Theorem 13.63s 2.89s
% Output : Refutation 15.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 24
% Syntax : Number of formulae : 174 ( 50 unt; 14 def)
% Number of atoms : 454 ( 42 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 523 ( 243 ~; 239 |; 14 &)
% ( 7 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 8 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 11 con; 0-4 aty)
% Number of variables : 161 ( 0 sgn 157 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f105,axiom,
! [X0,X1] : r1_tarski(k4_xboole_0(X0,X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t36_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(f2979,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_pboole(X2,X0)
=> ! [X3] :
( m1_pboole(X3,X0)
=> ( ( r2_pboole(X0,X1,X2)
& r2_pboole(X0,X1,X3) )
=> r2_pboole(X0,X1,k3_pboole(X0,X2,X3)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_pboole) ).
fof(f3137,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m4_pboole(X2,X0,X1)
=> m1_pboole(X2,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m4_pboole) ).
fof(f4712,axiom,
! [X0,X1,X2] :
( ( m1_pboole(X1,X0)
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
=> m4_pboole(k2_closure3(X0,X1,X2),X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_closure3) ).
fof(f4717,axiom,
! [X0,X1,X2,X3] :
( ( m1_pboole(X1,X0)
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
=> m1_subset_1(k4_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_closure3) ).
fof(f4718,axiom,
! [X0,X1,X2,X3] :
( ( m1_pboole(X1,X0)
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
=> k4_closure3(X0,X1,X2,X3) = k4_closure3(X0,X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k4_closure3) ).
fof(f4720,axiom,
! [X0,X1,X2,X3] :
( ( m1_pboole(X1,X0)
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
=> k4_closure3(X0,X1,X2,X3) = k3_xboole_0(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_closure3) ).
fof(f4739,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ( r1_tarski(X2,X3)
=> r2_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_closure3) ).
fof(f4740,conjecture,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
=> r2_pboole(X0,k2_closure3(X0,X1,k4_closure3(X0,X1,X2,X3)),k3_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_closure3) ).
fof(f4741,negated_conjecture,
~ ! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
=> r2_pboole(X0,k2_closure3(X0,X1,k4_closure3(X0,X1,X2,X3)),k3_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3))) ) ) ),
inference(negated_conjecture,[status(cth)],[f4740]) ).
fof(f8065,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( r2_pboole(X0,X1,k3_pboole(X0,X2,X3))
| ~ r2_pboole(X0,X1,X2)
| ~ r2_pboole(X0,X1,X3)
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f2979]) ).
fof(f8066,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( r2_pboole(X0,X1,k3_pboole(X0,X2,X3))
| ~ r2_pboole(X0,X1,X2)
| ~ r2_pboole(X0,X1,X3)
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(flattening,[],[f8065]) ).
fof(f8278,plain,
! [X0,X1] :
( ! [X2] :
( m1_pboole(X2,X0)
| ~ m4_pboole(X2,X0,X1) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f3137]) ).
fof(f10512,plain,
! [X0,X1,X2] :
( m4_pboole(k2_closure3(X0,X1,X2),X0,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(ennf_transformation,[],[f4712]) ).
fof(f10513,plain,
! [X0,X1,X2] :
( m4_pboole(k2_closure3(X0,X1,X2),X0,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(flattening,[],[f10512]) ).
fof(f10522,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(ennf_transformation,[],[f4717]) ).
fof(f10523,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(flattening,[],[f10522]) ).
fof(f10524,plain,
! [X0,X1,X2,X3] :
( k4_closure3(X0,X1,X2,X3) = k4_closure3(X0,X1,X3,X2)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(ennf_transformation,[],[f4718]) ).
fof(f10525,plain,
! [X0,X1,X2,X3] :
( k4_closure3(X0,X1,X2,X3) = k4_closure3(X0,X1,X3,X2)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(flattening,[],[f10524]) ).
fof(f10528,plain,
! [X0,X1,X2,X3] :
( k4_closure3(X0,X1,X2,X3) = k3_xboole_0(X2,X3)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(ennf_transformation,[],[f4720]) ).
fof(f10529,plain,
! [X0,X1,X2,X3] :
( k4_closure3(X0,X1,X2,X3) = k3_xboole_0(X2,X3)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(flattening,[],[f10528]) ).
fof(f10559,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( r2_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3))
| ~ r1_tarski(X2,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f4739]) ).
fof(f10560,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( r2_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3))
| ~ r1_tarski(X2,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
| ~ m1_pboole(X1,X0) ),
inference(flattening,[],[f10559]) ).
fof(f10561,plain,
? [X0,X1] :
( ? [X2] :
( ? [X3] :
( ~ r2_pboole(X0,k2_closure3(X0,X1,k4_closure3(X0,X1,X2,X3)),k3_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3)))
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
& m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f4741]) ).
fof(f13306,plain,
( ~ r2_pboole(sK1612,k2_closure3(sK1612,sK1613,k4_closure3(sK1612,sK1613,sK1614,sK1615)),k3_pboole(sK1612,k2_closure3(sK1612,sK1613,sK1614),k2_closure3(sK1612,sK1613,sK1615)))
& m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
& m1_subset_1(sK1614,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
& m1_pboole(sK1613,sK1612) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1612,sK1613,sK1614,sK1615]),skolemize(X0,sK1612),skolemize(X1,sK1613),skolemize(X2,sK1614),skolemize(X3,sK1615)],[f10561]) ).
fof(f13475,plain,
! [X0,X1] : r1_tarski(k4_xboole_0(X0,X1),X0),
inference(cnf_transformation,[],[f105]) ).
fof(f13488,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f18815,plain,
! [X2,X3,X0,X1] :
( r2_pboole(X0,X1,k3_pboole(X0,X2,X3))
| ~ r2_pboole(X0,X1,X2)
| ~ r2_pboole(X0,X1,X3)
| ~ m1_pboole(X3,X0)
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f8066]) ).
fof(f19056,plain,
! [X2,X0,X1] :
( ~ m4_pboole(X2,X0,X1)
| m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f8278]) ).
fof(f22392,plain,
! [X2,X0,X1] :
( m4_pboole(k2_closure3(X0,X1,X2),X0,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(cnf_transformation,[],[f10513]) ).
fof(f22397,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k4_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(cnf_transformation,[],[f10523]) ).
fof(f22398,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| k4_closure3(X0,X1,X2,X3) = k4_closure3(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f10525]) ).
fof(f22400,plain,
! [X2,X3,X0,X1] :
( k3_xboole_0(X2,X3) = k4_closure3(X0,X1,X2,X3)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(cnf_transformation,[],[f10529]) ).
fof(f22437,plain,
! [X2,X3,X0,X1] :
( r2_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3))
| ~ r1_tarski(X2,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f10560]) ).
fof(f22438,plain,
m1_pboole(sK1613,sK1612),
inference(cnf_transformation,[],[f13306]) ).
fof(f22439,plain,
m1_subset_1(sK1614,k1_zfmisc_1(k1_closure2(sK1612,sK1613))),
inference(cnf_transformation,[],[f13306]) ).
fof(f22440,plain,
m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613))),
inference(cnf_transformation,[],[f13306]) ).
fof(f22441,plain,
~ r2_pboole(sK1612,k2_closure3(sK1612,sK1613,k4_closure3(sK1612,sK1613,sK1614,sK1615)),k3_pboole(sK1612,k2_closure3(sK1612,sK1613,sK1614),k2_closure3(sK1612,sK1613,sK1615))),
inference(cnf_transformation,[],[f13306]) ).
fof(f24524,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| k4_closure3(X0,X1,X2,X3) = k4_xboole_0(X2,k4_xboole_0(X2,X3)) ),
inference(definition_unfolding,[],[f22400,f13488]) ).
fof(f25471,definition,
sF1616 = k4_closure3(sK1612,sK1613,sK1614,sK1615),
introduced(definition,[new_symbols(definition,[sF1616])],[function_definition]) ).
fof(f25472,plain,
k4_closure3(sK1612,sK1613,sK1614,sK1615) = sF1616,
inference(reorient_equations,[],[f25471]) ).
fof(f25473,definition,
sF1617 = k2_closure3(sK1612,sK1613,sF1616),
introduced(definition,[new_symbols(definition,[sF1617])],[function_definition]) ).
fof(f25474,plain,
k2_closure3(sK1612,sK1613,sF1616) = sF1617,
inference(reorient_equations,[],[f25473]) ).
fof(f25475,definition,
sF1618 = k2_closure3(sK1612,sK1613,sK1614),
introduced(definition,[new_symbols(definition,[sF1618])],[function_definition]) ).
fof(f25476,plain,
k2_closure3(sK1612,sK1613,sK1614) = sF1618,
inference(reorient_equations,[],[f25475]) ).
fof(f25477,definition,
sF1619 = k2_closure3(sK1612,sK1613,sK1615),
introduced(definition,[new_symbols(definition,[sF1619])],[function_definition]) ).
fof(f25478,plain,
k2_closure3(sK1612,sK1613,sK1615) = sF1619,
inference(reorient_equations,[],[f25477]) ).
fof(f25479,definition,
sF1620 = k3_pboole(sK1612,sF1618,sF1619),
introduced(definition,[new_symbols(definition,[sF1620])],[function_definition]) ).
fof(f25480,plain,
k3_pboole(sK1612,sF1618,sF1619) = sF1620,
inference(reorient_equations,[],[f25479]) ).
fof(f25481,plain,
~ r2_pboole(sK1612,sF1617,sF1620),
inference(definition_folding,[],[f22441,f25480,f25478,f25476,f25474,f25472]) ).
fof(f25482,definition,
sF1621 = k1_closure2(sK1612,sK1613),
introduced(definition,[new_symbols(definition,[sF1621])],[function_definition]) ).
fof(f25483,plain,
k1_closure2(sK1612,sK1613) = sF1621,
inference(reorient_equations,[],[f25482]) ).
fof(f25484,definition,
sF1622 = k1_zfmisc_1(sF1621),
introduced(definition,[new_symbols(definition,[sF1622])],[function_definition]) ).
fof(f25485,plain,
k1_zfmisc_1(sF1621) = sF1622,
inference(reorient_equations,[],[f25484]) ).
fof(f25486,plain,
m1_subset_1(sK1615,sF1622),
inference(definition_folding,[],[f22440,f25485,f25483]) ).
fof(f25487,plain,
m1_subset_1(sK1614,sF1622),
inference(definition_folding,[],[f22439,f25485,f25483]) ).
fof(f29539,plain,
! [X0] :
( r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1618)
| ~ r1_tarski(X0,sK1614)
| ~ m1_subset_1(sK1614,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_pboole(sK1613,sK1612) ),
inference(superposition,[],[f22437,f25476]) ).
fof(f29540,plain,
! [X0] :
( r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1619)
| ~ r1_tarski(X0,sK1615)
| ~ m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_pboole(sK1613,sK1612) ),
inference(superposition,[],[f22437,f25478]) ).
fof(f29541,plain,
! [X0] :
( r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1619)
| ~ r1_tarski(X0,sK1615)
| ~ m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_subsumption_resolution,[],[f29540,f22438]) ).
fof(f29542,plain,
! [X0] :
( r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1618)
| ~ r1_tarski(X0,sK1614)
| ~ m1_subset_1(sK1614,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_subsumption_resolution,[],[f29539,f22438]) ).
fof(f29547,plain,
! [X0] :
( ~ m1_subset_1(sK1615,k1_zfmisc_1(sF1621))
| r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1619)
| ~ r1_tarski(X0,sK1615)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_demodulation,[],[f29541,f25483]) ).
fof(f29548,plain,
! [X0] :
( ~ m1_subset_1(sK1614,k1_zfmisc_1(sF1621))
| r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1618)
| ~ r1_tarski(X0,sK1614)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_demodulation,[],[f29542,f25483]) ).
fof(f29553,plain,
! [X0] :
( ~ m1_subset_1(sK1615,sF1622)
| r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1619)
| ~ r1_tarski(X0,sK1615)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_demodulation,[],[f29547,f25485]) ).
fof(f29554,plain,
! [X0] :
( ~ m1_subset_1(sK1614,sF1622)
| r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1618)
| ~ r1_tarski(X0,sK1614)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_demodulation,[],[f29548,f25485]) ).
fof(f29559,plain,
! [X0] :
( r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1619)
| ~ r1_tarski(X0,sK1615)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_subsumption_resolution,[],[f29553,f25486]) ).
fof(f29560,plain,
! [X0] :
( r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1618)
| ~ r1_tarski(X0,sK1614)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_subsumption_resolution,[],[f29554,f25487]) ).
fof(f29565,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1621))
| r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1619)
| ~ r1_tarski(X0,sK1615) ),
inference(forward_demodulation,[],[f29559,f25483]) ).
fof(f29566,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1621))
| r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1618)
| ~ r1_tarski(X0,sK1614) ),
inference(forward_demodulation,[],[f29560,f25483]) ).
fof(f29571,plain,
! [X0] :
( r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1619)
| ~ m1_subset_1(X0,sF1622)
| ~ r1_tarski(X0,sK1615) ),
inference(forward_demodulation,[],[f29565,f25485]) ).
fof(f29572,plain,
! [X0] :
( r2_pboole(sK1612,k2_closure3(sK1612,sK1613,X0),sF1618)
| ~ m1_subset_1(X0,sF1622)
| ~ r1_tarski(X0,sK1614) ),
inference(forward_demodulation,[],[f29566,f25485]) ).
fof(f29574,definition,
( spl1623_622
<=> m1_subset_1(sF1616,sF1622) ),
introduced(definition,[new_symbols(definition,[spl1623_622])],[avatar_definition]) ).
fof(f29575,plain,
( m1_subset_1(sF1616,sF1622)
| ~ spl1623_622 ),
inference(avatar_component_clause,[],[f29574]) ).
fof(f29576,plain,
( ~ m1_subset_1(sF1616,sF1622)
| spl1623_622 ),
inference(avatar_component_clause,[],[f29574]) ).
fof(f29587,plain,
( r2_pboole(sK1612,sF1617,sF1619)
| ~ m1_subset_1(sF1616,sF1622)
| ~ r1_tarski(sF1616,sK1615) ),
inference(superposition,[],[f29571,f25474]) ).
fof(f29602,plain,
( r2_pboole(sK1612,sF1617,sF1618)
| ~ m1_subset_1(sF1616,sF1622)
| ~ r1_tarski(sF1616,sK1614) ),
inference(superposition,[],[f29572,f25474]) ).
fof(f29619,definition,
( spl1623_629
<=> m1_pboole(sF1618,sK1612) ),
introduced(definition,[new_symbols(definition,[spl1623_629])],[avatar_definition]) ).
fof(f29620,plain,
( m1_pboole(sF1618,sK1612)
| ~ spl1623_629 ),
inference(avatar_component_clause,[],[f29619]) ).
fof(f29621,plain,
( ~ m1_pboole(sF1618,sK1612)
| spl1623_629 ),
inference(avatar_component_clause,[],[f29619]) ).
fof(f29623,definition,
( spl1623_630
<=> m1_pboole(sF1619,sK1612) ),
introduced(definition,[new_symbols(definition,[spl1623_630])],[avatar_definition]) ).
fof(f29624,plain,
( m1_pboole(sF1619,sK1612)
| ~ spl1623_630 ),
inference(avatar_component_clause,[],[f29623]) ).
fof(f29638,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1621))
| ~ m1_pboole(sK1613,sK1612)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1621))
| k4_xboole_0(X1,k4_xboole_0(X1,X0)) = k4_closure3(sK1612,sK1613,X1,X0) ),
inference(superposition,[],[f24524,f25483]) ).
fof(f29639,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1621))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1621))
| k4_xboole_0(X1,k4_xboole_0(X1,X0)) = k4_closure3(sK1612,sK1613,X1,X0) ),
inference(forward_subsumption_resolution,[],[f29638,f22438]) ).
fof(f29640,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF1622)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1621))
| k4_xboole_0(X1,k4_xboole_0(X1,X0)) = k4_closure3(sK1612,sK1613,X1,X0) ),
inference(forward_demodulation,[],[f29639,f25485]) ).
fof(f29641,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF1622)
| ~ m1_subset_1(X0,sF1622)
| k4_xboole_0(X1,k4_xboole_0(X1,X0)) = k4_closure3(sK1612,sK1613,X1,X0) ),
inference(forward_demodulation,[],[f29640,f25485]) ).
fof(f29642,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1622)
| k4_xboole_0(sK1614,k4_xboole_0(sK1614,X0)) = k4_closure3(sK1612,sK1613,sK1614,X0) ),
inference(resolution,[],[f29641,f25487]) ).
fof(f29643,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1622)
| k4_xboole_0(sK1615,k4_xboole_0(sK1615,X0)) = k4_closure3(sK1612,sK1613,sK1615,X0) ),
inference(resolution,[],[f29641,f25486]) ).
fof(f29644,plain,
k4_xboole_0(sK1615,k4_xboole_0(sK1615,sK1614)) = k4_closure3(sK1612,sK1613,sK1615,sK1614),
inference(resolution,[],[f29643,f25487]) ).
fof(f29648,plain,
k4_closure3(sK1612,sK1613,sK1614,sK1615) = k4_xboole_0(sK1614,k4_xboole_0(sK1614,sK1615)),
inference(resolution,[],[f29642,f25486]) ).
fof(f29649,plain,
sF1616 = k4_xboole_0(sK1614,k4_xboole_0(sK1614,sK1615)),
inference(forward_demodulation,[],[f29648,f25472]) ).
fof(f29651,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1621))
| ~ m1_pboole(sK1613,sK1612)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1621))
| k4_closure3(sK1612,sK1613,X1,X0) = k4_closure3(sK1612,sK1613,X0,X1) ),
inference(superposition,[],[f22398,f25483]) ).
fof(f29652,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1621))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1621))
| k4_closure3(sK1612,sK1613,X1,X0) = k4_closure3(sK1612,sK1613,X0,X1) ),
inference(forward_subsumption_resolution,[],[f29651,f22438]) ).
fof(f29653,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF1622)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF1621))
| k4_closure3(sK1612,sK1613,X1,X0) = k4_closure3(sK1612,sK1613,X0,X1) ),
inference(forward_demodulation,[],[f29652,f25485]) ).
fof(f29654,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF1622)
| ~ m1_subset_1(X0,sF1622)
| k4_closure3(sK1612,sK1613,X1,X0) = k4_closure3(sK1612,sK1613,X0,X1) ),
inference(forward_demodulation,[],[f29653,f25485]) ).
fof(f29655,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1622)
| k4_closure3(sK1612,sK1613,sK1614,X0) = k4_closure3(sK1612,sK1613,X0,sK1614) ),
inference(resolution,[],[f29654,f25487]) ).
fof(f29658,plain,
k4_closure3(sK1612,sK1613,sK1614,sK1615) = k4_closure3(sK1612,sK1613,sK1615,sK1614),
inference(resolution,[],[f29655,f25486]) ).
fof(f29659,plain,
k4_closure3(sK1612,sK1613,sK1614,sK1615) = k4_xboole_0(sK1615,k4_xboole_0(sK1615,sK1614)),
inference(forward_demodulation,[],[f29658,f29644]) ).
fof(f29660,plain,
sF1616 = k4_xboole_0(sK1615,k4_xboole_0(sK1615,sK1614)),
inference(forward_demodulation,[],[f29659,f25472]) ).
fof(f29666,plain,
( m4_pboole(sF1617,sK1612,sK1613)
| ~ m1_pboole(sK1613,sK1612)
| ~ m1_subset_1(sF1616,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(superposition,[],[f22392,f25474]) ).
fof(f29667,plain,
( m4_pboole(sF1618,sK1612,sK1613)
| ~ m1_pboole(sK1613,sK1612)
| ~ m1_subset_1(sK1614,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(superposition,[],[f22392,f25476]) ).
fof(f29668,plain,
( m4_pboole(sF1619,sK1612,sK1613)
| ~ m1_pboole(sK1613,sK1612)
| ~ m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(superposition,[],[f22392,f25478]) ).
fof(f29670,plain,
( m4_pboole(sF1619,sK1612,sK1613)
| ~ m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_subsumption_resolution,[],[f29668,f22438]) ).
fof(f29671,plain,
( m4_pboole(sF1618,sK1612,sK1613)
| ~ m1_subset_1(sK1614,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_subsumption_resolution,[],[f29667,f22438]) ).
fof(f29672,plain,
( m4_pboole(sF1617,sK1612,sK1613)
| ~ m1_subset_1(sF1616,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_subsumption_resolution,[],[f29666,f22438]) ).
fof(f29673,plain,
( ~ m1_subset_1(sK1615,k1_zfmisc_1(sF1621))
| m4_pboole(sF1619,sK1612,sK1613) ),
inference(forward_demodulation,[],[f29670,f25483]) ).
fof(f29674,plain,
( ~ m1_subset_1(sK1614,k1_zfmisc_1(sF1621))
| m4_pboole(sF1618,sK1612,sK1613) ),
inference(forward_demodulation,[],[f29671,f25483]) ).
fof(f29675,plain,
( ~ m1_subset_1(sF1616,k1_zfmisc_1(sF1621))
| m4_pboole(sF1617,sK1612,sK1613) ),
inference(forward_demodulation,[],[f29672,f25483]) ).
fof(f29676,plain,
( ~ m1_subset_1(sK1615,sF1622)
| m4_pboole(sF1619,sK1612,sK1613) ),
inference(forward_demodulation,[],[f29673,f25485]) ).
fof(f29677,plain,
( ~ m1_subset_1(sK1614,sF1622)
| m4_pboole(sF1618,sK1612,sK1613) ),
inference(forward_demodulation,[],[f29674,f25485]) ).
fof(f29678,plain,
( ~ m1_subset_1(sF1616,sF1622)
| m4_pboole(sF1617,sK1612,sK1613) ),
inference(forward_demodulation,[],[f29675,f25485]) ).
fof(f29679,plain,
m4_pboole(sF1619,sK1612,sK1613),
inference(forward_subsumption_resolution,[],[f29676,f25486]) ).
fof(f29680,plain,
m4_pboole(sF1618,sK1612,sK1613),
inference(forward_subsumption_resolution,[],[f29677,f25487]) ).
fof(f29736,plain,
( m1_subset_1(sF1616,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_pboole(sK1613,sK1612)
| ~ m1_subset_1(sK1614,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(superposition,[],[f22397,f25472]) ).
fof(f29743,plain,
( m1_subset_1(sF1616,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_subset_1(sK1614,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_subsumption_resolution,[],[f29736,f22438]) ).
fof(f29745,plain,
( m1_subset_1(sF1616,k1_zfmisc_1(sF1621))
| ~ m1_subset_1(sK1614,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_demodulation,[],[f29743,f25483]) ).
fof(f29747,plain,
( m1_subset_1(sF1616,sF1622)
| ~ m1_subset_1(sK1614,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613))) ),
inference(forward_demodulation,[],[f29745,f25485]) ).
fof(f29749,plain,
( ~ m1_subset_1(sK1614,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| ~ m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| spl1623_622 ),
inference(forward_subsumption_resolution,[],[f29747,f29576]) ).
fof(f29750,plain,
( ~ m1_subset_1(sK1614,k1_zfmisc_1(sF1621))
| ~ m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| spl1623_622 ),
inference(forward_demodulation,[],[f29749,f25483]) ).
fof(f29751,plain,
( ~ m1_subset_1(sK1614,sF1622)
| ~ m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| spl1623_622 ),
inference(forward_demodulation,[],[f29750,f25485]) ).
fof(f29752,plain,
( ~ m1_subset_1(sK1615,k1_zfmisc_1(k1_closure2(sK1612,sK1613)))
| spl1623_622 ),
inference(forward_subsumption_resolution,[],[f29751,f25487]) ).
fof(f29753,plain,
( ~ m1_subset_1(sK1615,k1_zfmisc_1(sF1621))
| spl1623_622 ),
inference(forward_demodulation,[],[f29752,f25483]) ).
fof(f29754,plain,
( ~ m1_subset_1(sK1615,sF1622)
| spl1623_622 ),
inference(forward_demodulation,[],[f29753,f25485]) ).
fof(f29755,plain,
( $false
| spl1623_622 ),
inference(forward_subsumption_resolution,[],[f29754,f25486]) ).
fof(f29756,plain,
spl1623_622,
inference(avatar_contradiction_clause,[],[f29755]) ).
fof(f29757,plain,
( r2_pboole(sK1612,sF1617,sF1619)
| ~ r1_tarski(sF1616,sK1615)
| ~ spl1623_622 ),
inference(forward_subsumption_resolution,[],[f29587,f29575]) ).
fof(f29758,plain,
( r2_pboole(sK1612,sF1617,sF1618)
| ~ r1_tarski(sF1616,sK1614)
| ~ spl1623_622 ),
inference(forward_subsumption_resolution,[],[f29602,f29575]) ).
fof(f29761,plain,
( m4_pboole(sF1617,sK1612,sK1613)
| ~ spl1623_622 ),
inference(forward_subsumption_resolution,[],[f29678,f29575]) ).
fof(f29764,definition,
( spl1623_634
<=> r1_tarski(sF1616,sK1615) ),
introduced(definition,[new_symbols(definition,[spl1623_634])],[avatar_definition]) ).
fof(f29766,plain,
( ~ r1_tarski(sF1616,sK1615)
| spl1623_634 ),
inference(avatar_component_clause,[],[f29764]) ).
fof(f29768,definition,
( spl1623_635
<=> r2_pboole(sK1612,sF1617,sF1619) ),
introduced(definition,[new_symbols(definition,[spl1623_635])],[avatar_definition]) ).
fof(f29770,plain,
( r2_pboole(sK1612,sF1617,sF1619)
| ~ spl1623_635 ),
inference(avatar_component_clause,[],[f29768]) ).
fof(f29771,plain,
( ~ spl1623_634
| spl1623_635
| ~ spl1623_622 ),
inference(avatar_split_clause,[],[f29757,f29574,f29768,f29764]) ).
fof(f29773,definition,
( spl1623_636
<=> r1_tarski(sF1616,sK1614) ),
introduced(definition,[new_symbols(definition,[spl1623_636])],[avatar_definition]) ).
fof(f29775,plain,
( ~ r1_tarski(sF1616,sK1614)
| spl1623_636 ),
inference(avatar_component_clause,[],[f29773]) ).
fof(f29777,definition,
( spl1623_637
<=> r2_pboole(sK1612,sF1617,sF1618) ),
introduced(definition,[new_symbols(definition,[spl1623_637])],[avatar_definition]) ).
fof(f29779,plain,
( r2_pboole(sK1612,sF1617,sF1618)
| ~ spl1623_637 ),
inference(avatar_component_clause,[],[f29777]) ).
fof(f29780,plain,
( ~ spl1623_636
| spl1623_637
| ~ spl1623_622 ),
inference(avatar_split_clause,[],[f29758,f29574,f29777,f29773]) ).
fof(f29988,plain,
( m1_pboole(sF1617,sK1612)
| ~ m1_pboole(sK1613,sK1612)
| ~ spl1623_622 ),
inference(resolution,[],[f19056,f29761]) ).
fof(f29989,plain,
( m1_pboole(sF1618,sK1612)
| ~ m1_pboole(sK1613,sK1612) ),
inference(resolution,[],[f19056,f29680]) ).
fof(f29990,plain,
( m1_pboole(sF1619,sK1612)
| ~ m1_pboole(sK1613,sK1612) ),
inference(resolution,[],[f19056,f29679]) ).
fof(f29992,plain,
m1_pboole(sF1619,sK1612),
inference(forward_subsumption_resolution,[],[f29990,f22438]) ).
fof(f29993,plain,
( ~ m1_pboole(sK1613,sK1612)
| spl1623_629 ),
inference(forward_subsumption_resolution,[],[f29989,f29621]) ).
fof(f29994,plain,
( m1_pboole(sF1617,sK1612)
| ~ spl1623_622 ),
inference(forward_subsumption_resolution,[],[f29988,f22438]) ).
fof(f29995,plain,
spl1623_630,
inference(avatar_split_clause,[],[f29992,f29623]) ).
fof(f29996,plain,
( $false
| spl1623_629 ),
inference(forward_subsumption_resolution,[],[f29993,f22438]) ).
fof(f29997,plain,
spl1623_629,
inference(avatar_contradiction_clause,[],[f29996]) ).
fof(f30194,plain,
r1_tarski(sF1616,sK1614),
inference(superposition,[],[f13475,f29649]) ).
fof(f30195,plain,
r1_tarski(sF1616,sK1615),
inference(superposition,[],[f13475,f29660]) ).
fof(f30200,plain,
( $false
| spl1623_634 ),
inference(forward_subsumption_resolution,[],[f30195,f29766]) ).
fof(f30201,plain,
spl1623_634,
inference(avatar_contradiction_clause,[],[f30200]) ).
fof(f30202,plain,
( $false
| spl1623_636 ),
inference(forward_subsumption_resolution,[],[f30194,f29775]) ).
fof(f30203,plain,
spl1623_636,
inference(avatar_contradiction_clause,[],[f30202]) ).
fof(f30277,plain,
! [X0] :
( r2_pboole(sK1612,X0,sF1620)
| ~ r2_pboole(sK1612,X0,sF1618)
| ~ r2_pboole(sK1612,X0,sF1619)
| ~ m1_pboole(sF1619,sK1612)
| ~ m1_pboole(sF1618,sK1612)
| ~ m1_pboole(X0,sK1612) ),
inference(superposition,[],[f18815,f25480]) ).
fof(f30284,plain,
( ! [X0] :
( r2_pboole(sK1612,X0,sF1620)
| ~ r2_pboole(sK1612,X0,sF1618)
| ~ r2_pboole(sK1612,X0,sF1619)
| ~ m1_pboole(sF1618,sK1612)
| ~ m1_pboole(X0,sK1612) )
| ~ spl1623_630 ),
inference(forward_subsumption_resolution,[],[f30277,f29624]) ).
fof(f30287,plain,
( ! [X0] :
( ~ r2_pboole(sK1612,X0,sF1619)
| ~ r2_pboole(sK1612,X0,sF1618)
| r2_pboole(sK1612,X0,sF1620)
| ~ m1_pboole(X0,sK1612) )
| ~ spl1623_629
| ~ spl1623_630 ),
inference(forward_subsumption_resolution,[],[f30284,f29620]) ).
fof(f30745,plain,
( ~ r2_pboole(sK1612,sF1617,sF1618)
| r2_pboole(sK1612,sF1617,sF1620)
| ~ m1_pboole(sF1617,sK1612)
| ~ spl1623_629
| ~ spl1623_630
| ~ spl1623_635 ),
inference(resolution,[],[f30287,f29770]) ).
fof(f30750,plain,
( r2_pboole(sK1612,sF1617,sF1620)
| ~ m1_pboole(sF1617,sK1612)
| ~ spl1623_629
| ~ spl1623_630
| ~ spl1623_635
| ~ spl1623_637 ),
inference(forward_subsumption_resolution,[],[f30745,f29779]) ).
fof(f30763,plain,
( ~ m1_pboole(sF1617,sK1612)
| ~ spl1623_629
| ~ spl1623_630
| ~ spl1623_635
| ~ spl1623_637 ),
inference(forward_subsumption_resolution,[],[f30750,f25481]) ).
fof(f30770,plain,
( $false
| ~ spl1623_622
| ~ spl1623_629
| ~ spl1623_630
| ~ spl1623_635
| ~ spl1623_637 ),
inference(forward_subsumption_resolution,[],[f30763,f29994]) ).
fof(f30771,plain,
( ~ spl1623_622
| ~ spl1623_629
| ~ spl1623_630
| ~ spl1623_635
| ~ spl1623_637 ),
inference(avatar_contradiction_clause,[],[f30770]) ).
cnf(s549,plain,
spl1623_622,
inference(sat_conversion,[],[f29756]) ).
cnf(s550,plain,
( ~ spl1623_622
| ~ spl1623_634
| spl1623_635 ),
inference(sat_conversion,[],[f29771]) ).
cnf(s551,plain,
( ~ spl1623_622
| ~ spl1623_636
| spl1623_637 ),
inference(sat_conversion,[],[f29780]) ).
cnf(s554,plain,
spl1623_630,
inference(sat_conversion,[],[f29995]) ).
cnf(s555,plain,
spl1623_629,
inference(sat_conversion,[],[f29997]) ).
cnf(s560,plain,
spl1623_634,
inference(sat_conversion,[],[f30201]) ).
cnf(s561,plain,
spl1623_636,
inference(sat_conversion,[],[f30203]) ).
cnf(s572,plain,
( ~ spl1623_622
| ~ spl1623_629
| ~ spl1623_630
| ~ spl1623_635
| ~ spl1623_637 ),
inference(sat_conversion,[],[f30771]) ).
cnf(s576,plain,
( ~ spl1623_622
| spl1623_637 ),
inference(rat,[],[s551,s561]) ).
cnf(s577,plain,
( ~ spl1623_622
| spl1623_635 ),
inference(rat,[],[s550,s560]) ).
cnf(s579,plain,
spl1623_637,
inference(rat,[],[s576,s549]) ).
cnf(s580,plain,
spl1623_635,
inference(rat,[],[s577,s549]) ).
cnf(s581,plain,
$false,
inference(rat,[],[s572,s549,s554,s555,s579,s580]) ).
fof(f30772,plain,
$false,
inference(avatar_sat_refutation,[],[s581]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG232+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.18 % Computer : n009.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.18 % WCLimit : 300
% 0.06/0.18 % DateTime : Mon Sep 28 19:55:31 UTC 2026
% 0.06/0.19 % CPUTime :
% 0.06/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.22 Running first-order theorem proving
% 0.06/0.22 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
% 13.63/2.89 % (3387190)Detected formulas, will run a generic FOF schedule.
% 13.63/2.89 % (3387195)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=4227996227:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 13.63/2.89 % (3387200)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=208135327:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 13.63/2.89 % (3387198)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3592519827:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 13.63/2.89 % (3387196)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=3407766035:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 13.63/2.89 % (3387199)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2856608047:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 13.63/2.89 % (3387197)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=1316862441:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 13.63/2.89 % (3387201)dis-21_1_sil=8000:lcm=predicate:random_seed=541327379:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 13.63/2.89 % (3387198)Refutation not found, incomplete strategy
% 13.63/2.89 % (3387198)------------------------------
% 13.63/2.89 % (3387198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387198)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387198)Termination reason: Refutation not found, incomplete strategy
% 13.63/2.89 % (3387198)Time elapsed: 0.025 s
% 13.63/2.89 % (3387198)Peak memory usage: 94 MB
% 13.63/2.89 % (3387198)Instructions burned: 31 (million)
% 13.63/2.89 % (3387199)Instruction limit reached!
% 13.63/2.89 % (3387199)------------------------------
% 13.63/2.89 % (3387199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387199)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387199)Termination reason: Instruction limit
% 13.63/2.89 % (3387199)Termination phase: Saturation
% 13.63/2.89 % (3387199)Time elapsed: 0.075 s
% 13.63/2.89 % (3387199)Peak memory usage: 95 MB
% 13.63/2.89 % (3387199)Instructions burned: 119 (million)
% 13.63/2.89 % (3387200)Instruction limit reached!
% 13.63/2.89 % (3387200)------------------------------
% 13.63/2.89 % (3387200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387200)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387200)Termination reason: Instruction limit
% 13.63/2.89 % (3387200)Termination phase: Naming
% 13.63/2.89 % (3387200)Time elapsed: 0.102 s
% 13.63/2.89 % (3387200)Peak memory usage: 94 MB
% 13.63/2.89 % (3387200)Instructions burned: 141 (million)
% 13.63/2.89 % (3387201)Instruction limit reached!
% 13.63/2.89 % (3387201)------------------------------
% 13.63/2.89 % (3387201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387201)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387201)Termination reason: Instruction limit
% 13.63/2.89 % (3387201)Termination phase: Preprocessing 3
% 13.63/2.89 % (3387201)Time elapsed: 0.094 s
% 13.63/2.89 % (3387201)Peak memory usage: 95 MB
% 13.63/2.89 % (3387201)Instructions burned: 129 (million)
% 13.63/2.89 % (3387209)lrs+10_1_sil=8000:sp=occurrence:random_seed=1909202173:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 13.63/2.89 % (3387210)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1886062863:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 13.63/2.89 % (3387211)lrs+1011_1_sil=32000:sp=occurrence:random_seed=667860984:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 13.63/2.89 % (3387198)------------------------------
% 13.63/2.89 % (3387198)------------------------------
% 13.63/2.89 % (3387210)Instruction limit reached!
% 13.63/2.89 % (3387210)------------------------------
% 13.63/2.89 % (3387210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387210)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387210)Termination reason: Instruction limit
% 13.63/2.89 % (3387210)Termination phase: Saturation
% 13.63/2.89 % (3387210)Time elapsed: 0.086 s
% 13.63/2.89 % (3387210)Peak memory usage: 94 MB
% 13.63/2.89 % (3387210)Instructions burned: 159 (million)
% 13.63/2.89 % (3387209)Instruction limit reached!
% 13.63/2.89 % (3387209)------------------------------
% 13.63/2.89 % (3387209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387209)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387209)Termination reason: Instruction limit
% 13.63/2.89 % (3387209)Termination phase: Saturation
% 13.63/2.89 % (3387209)Time elapsed: 0.197 s
% 13.63/2.89 % (3387209)Peak memory usage: 98 MB
% 13.63/2.89 % (3387209)Instructions burned: 285 (million)
% 13.63/2.89 % (3387215)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=3255547468:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 13.63/2.89 % (3387216)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1945516675:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 13.63/2.89 % (3387211)Instruction limit reached!
% 13.63/2.89 % (3387211)------------------------------
% 13.63/2.89 % (3387211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387211)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387211)Termination reason: Instruction limit
% 13.63/2.89 % (3387211)Termination phase: Saturation
% 13.63/2.89 % (3387211)Time elapsed: 0.227 s
% 13.63/2.89 % (3387211)Peak memory usage: 97 MB
% 13.63/2.89 % (3387211)Instructions burned: 325 (million)
% 13.63/2.89 % (3387218)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=799188640:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 13.63/2.89 % (3387215)Instruction limit reached!
% 13.63/2.89 % (3387215)------------------------------
% 13.63/2.89 % (3387215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387215)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387215)Termination reason: Instruction limit
% 13.63/2.89 % (3387215)Termination phase: Property scanning
% 13.63/2.89 % (3387215)Time elapsed: 0.155 s
% 13.63/2.89 % (3387215)Peak memory usage: 100 MB
% 13.63/2.89 % (3387215)Instructions burned: 249 (million)
% 13.63/2.89 % (3387220)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4100193606:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 13.63/2.89 % (3387216)Instruction limit reached!
% 13.63/2.89 % (3387216)------------------------------
% 13.63/2.89 % (3387216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387216)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387216)Termination reason: Instruction limit
% 13.63/2.89 % (3387216)Termination phase: Saturation
% 13.63/2.89 % (3387216)Time elapsed: 0.178 s
% 13.63/2.89 % (3387216)Peak memory usage: 98 MB
% 13.63/2.89 % (3387216)Instructions burned: 297 (million)
% 13.63/2.89 % (3387220)Instruction limit reached!
% 13.63/2.89 % (3387220)------------------------------
% 13.63/2.89 % (3387220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387220)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387220)Termination reason: Instruction limit
% 13.63/2.89 % (3387220)Termination phase: Property scanning
% 13.63/2.89 % (3387220)Time elapsed: 0.074 s
% 13.63/2.89 % (3387220)Peak memory usage: 94 MB
% 13.63/2.89 % (3387220)Instructions burned: 115 (million)
% 13.63/2.89 % (3387222)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3616373555:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 13.63/2.89 % (3387224)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=719892639:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 13.63/2.89 % (3387222)Instruction limit reached!
% 13.63/2.89 % (3387222)------------------------------
% 13.63/2.89 % (3387222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387222)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387222)Termination reason: Instruction limit
% 13.63/2.89 % (3387222)Termination phase: Preprocessing 3
% 13.63/2.89 % (3387222)Time elapsed: 0.088 s
% 13.63/2.89 % (3387222)Peak memory usage: 97 MB
% 13.63/2.89 % (3387222)Instructions burned: 127 (million)
% 13.63/2.89 % (3387224)Instruction limit reached!
% 13.63/2.89 % (3387224)------------------------------
% 13.63/2.89 % (3387224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387224)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387224)Termination reason: Instruction limit
% 13.63/2.89 % (3387224)Termination phase: SInE selection
% 13.63/2.89 % (3387224)Time elapsed: 0.052 s
% 13.63/2.89 % (3387224)Peak memory usage: 90 MB
% 13.63/2.89 % (3387224)Instructions burned: 115 (million)
% 13.63/2.89 % (3387225)lrs+10_1_sil=8000:sp=occurrence:random_seed=2227225066:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 13.63/2.89 % (3387228)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=852472186:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 13.63/2.89 % (3387230)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2834472126:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 13.63/2.89 % (3387228)Instruction limit reached!
% 13.63/2.89 % (3387228)------------------------------
% 13.63/2.89 % (3387228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387228)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387228)Termination reason: Instruction limit
% 13.63/2.89 % (3387228)Termination phase: Saturation
% 13.63/2.89 % (3387228)Time elapsed: 0.266 s
% 13.63/2.89 % (3387228)Peak memory usage: 98 MB
% 13.63/2.89 % (3387228)Instructions burned: 438 (million)
% 13.63/2.89 % (3387233)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=370325006:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 13.63/2.89 % (3387225)Instruction limit reached!
% 13.63/2.89 % (3387225)------------------------------
% 13.63/2.89 % (3387225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387225)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387225)Termination reason: Instruction limit
% 13.63/2.89 % (3387225)Termination phase: Saturation
% 13.63/2.89 % (3387225)Time elapsed: 0.583 s
% 13.63/2.89 % (3387225)Peak memory usage: 109 MB
% 13.63/2.89 % (3387225)Instructions burned: 907 (million)
% 13.63/2.89 % (3387233)Instruction limit reached!
% 13.63/2.89 % (3387233)------------------------------
% 13.63/2.89 % (3387233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.89 % (3387233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.89 % (3387233)CaDiCaL version: 2.1.3
% 13.63/2.89 % (3387233)Termination reason: Instruction limit
% 13.63/2.89 % (3387233)Termination phase: Saturation
% 13.63/2.89 % (3387233)Time elapsed: 0.084 s
% 13.63/2.89 % (3387233)Peak memory usage: 96 MB
% 13.63/2.89 % (3387233)Instructions burned: 134 (million)
% 13.63/2.89 % (3387235)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3997717422:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 13.63/2.89 % (3387236)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2987478653:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 13.63/2.89 % (3387195)First to succeed.
% 13.63/2.89 % (3387195)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3387190"
% 13.63/2.89 % (3387195)Refutation found. Thanks to Tanya!
% 13.63/2.89 % SZS status Theorem for theBenchmark
% 13.63/2.89 % SZS output start Proof for theBenchmark
% See solution above
% 15.21/3.09 % (3387195)------------------------------
% 15.21/3.09 % (3387195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.21/3.09 % (3387195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.21/3.09 % (3387195)CaDiCaL version: 2.1.3
% 15.21/3.09 % (3387195)Termination reason: Refutation
% 15.21/3.09 % (3387195)Time elapsed: 1.741 s
% 15.21/3.09 % (3387195)Peak memory usage: 243 MB
% 15.21/3.09 % (3387195)Instructions burned: 5177 (million)
% 15.21/3.09 % (3387195)------------------------------
% 15.21/3.09 % (3387195)------------------------------
% 15.21/3.09 % (3387190)Success in time 2.234 s
% 15.21/3.09 % Vampire exiting
%------------------------------------------------------------------------------