%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU419+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:48:52 PM UTC 2026
% Result : Theorem 10.07s 3.31s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 28
% Syntax : Number of formulae : 158 ( 125 unt; 7 def)
% Number of atoms : 202 ( 138 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 80 ( 36 ~; 30 |; 4 &)
% ( 1 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 2 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 11 con; 0-2 aty)
% Number of variables : 204 ( 1 sgn 201 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f54,axiom,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X1,X0),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f58,axiom,
! [X0,X1] : k3_xboole_0(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_k3_xboole_0) ).
fof(f63,axiom,
! [X0] : k3_xboole_0(X0,k1_xboole_0) = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_boole) ).
fof(f64,axiom,
! [X0] : k4_xboole_0(X0,k1_xboole_0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_boole) ).
fof(f108,axiom,
! [X0,X1] : k2_xboole_0(X0,k4_xboole_0(X1,X0)) = k2_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t39_xboole_1) ).
fof(f109,axiom,
! [X0,X1] : k4_xboole_0(k2_xboole_0(X0,X1),X1) = k4_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t40_xboole_1) ).
fof(f110,axiom,
! [X0,X1,X2] : k4_xboole_0(k4_xboole_0(X0,X1),X2) = k4_xboole_0(X0,k2_xboole_0(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t41_xboole_1) ).
fof(f115,axiom,
! [X0,X1] : k4_xboole_0(X0,k2_xboole_0(X0,X1)) = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t46_xboole_1) ).
fof(f116,axiom,
! [X0,X1] : k4_xboole_0(X0,k3_xboole_0(X0,X1)) = k4_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t47_xboole_1) ).
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f118,axiom,
! [X0,X1,X2] : k3_xboole_0(X0,k4_xboole_0(X1,X2)) = k4_xboole_0(k3_xboole_0(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t49_xboole_1) ).
fof(f121,axiom,
! [X0,X1,X2] : k4_xboole_0(X0,k4_xboole_0(X1,X2)) = k2_xboole_0(k4_xboole_0(X0,X1),k3_xboole_0(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t52_xboole_1) ).
fof(f122,axiom,
! [X0,X1,X2] : k4_xboole_0(X0,k2_xboole_0(X1,X2)) = k3_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t53_xboole_1) ).
fof(f180,axiom,
! [X0,X1,X2] : k4_xboole_0(k3_xboole_0(X0,X1),k3_xboole_0(X2,X1)) = k3_xboole_0(k4_xboole_0(X0,X2),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t111_xboole_1) ).
fof(f572,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> v1_relat_1(k4_xboole_0(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_relat_1) ).
fof(f722,axiom,
! [X0] : k9_relat_1(k1_xboole_0,X0) = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t150_relat_1) ).
fof(f2485,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_card_1) ).
fof(f4479,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> ! [X2] :
( v1_relat_1(X2)
=> k9_relat_1(k2_xboole_0(X1,X2),k1_tarski(X0)) = k2_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_relset_2) ).
fof(f4480,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> ! [X2] :
( v1_relat_1(X2)
=> k9_relat_1(k3_xboole_0(X1,X2),k1_tarski(X0)) = k3_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_relset_2) ).
fof(f4481,conjecture,
! [X0,X1] :
( v1_relat_1(X1)
=> ! [X2] :
( v1_relat_1(X2)
=> k9_relat_1(k4_xboole_0(X1,X2),k1_tarski(X0)) = k4_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_relset_2) ).
fof(f4482,negated_conjecture,
~ ! [X0,X1] :
( v1_relat_1(X1)
=> ! [X2] :
( v1_relat_1(X2)
=> k9_relat_1(k4_xboole_0(X1,X2),k1_tarski(X0)) = k4_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0))) ) ),
inference(negated_conjecture,[status(cth)],[f4481]) ).
fof(f4494,plain,
! [X0] : k3_xboole_0(X0,X0) = X0,
inference(rectify,[],[f58]) ).
fof(f5100,plain,
! [X0,X1] :
( v1_relat_1(k4_xboole_0(X1,X0))
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f572]) ).
fof(f9707,plain,
! [X0,X1] :
( ! [X2] :
( k9_relat_1(k2_xboole_0(X1,X2),k1_tarski(X0)) = k2_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0)))
| ~ v1_relat_1(X2) )
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f4479]) ).
fof(f9708,plain,
! [X0,X1] :
( ! [X2] :
( k9_relat_1(k3_xboole_0(X1,X2),k1_tarski(X0)) = k3_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0)))
| ~ v1_relat_1(X2) )
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f4480]) ).
fof(f9709,plain,
? [X0,X1] :
( ? [X2] :
( k9_relat_1(k4_xboole_0(X1,X2),k1_tarski(X0)) != k4_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0)))
& v1_relat_1(X2) )
& v1_relat_1(X1) ),
inference(ennf_transformation,[],[f4482]) ).
fof(f12135,plain,
( k9_relat_1(k4_xboole_0(sK1507,sK1508),k1_tarski(sK1506)) != k4_xboole_0(k9_relat_1(sK1507,k1_tarski(sK1506)),k9_relat_1(sK1508,k1_tarski(sK1506)))
& v1_relat_1(sK1508)
& v1_relat_1(sK1507) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1506,sK1507,sK1508]),skolemize(X0,sK1506),skolemize(X1,sK1507),skolemize(X2,sK1508)],[f9709]) ).
fof(f12252,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X1,X0),
inference(cnf_transformation,[],[f54]) ).
fof(f12254,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f57]) ).
fof(f12255,plain,
! [X0] : k3_xboole_0(X0,X0) = X0,
inference(cnf_transformation,[],[f4494]) ).
fof(f12258,plain,
! [X0] : k1_xboole_0 = k3_xboole_0(X0,k1_xboole_0),
inference(cnf_transformation,[],[f63]) ).
fof(f12259,plain,
! [X0] : k4_xboole_0(X0,k1_xboole_0) = X0,
inference(cnf_transformation,[],[f64]) ).
fof(f12308,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X0,k4_xboole_0(X1,X0)),
inference(cnf_transformation,[],[f108]) ).
fof(f12309,plain,
! [X0,X1] : k4_xboole_0(X0,X1) = k4_xboole_0(k2_xboole_0(X0,X1),X1),
inference(cnf_transformation,[],[f109]) ).
fof(f12310,plain,
! [X2,X0,X1] : k4_xboole_0(k4_xboole_0(X0,X1),X2) = k4_xboole_0(X0,k2_xboole_0(X1,X2)),
inference(cnf_transformation,[],[f110]) ).
fof(f12315,plain,
! [X0,X1] : k1_xboole_0 = k4_xboole_0(X0,k2_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f115]) ).
fof(f12316,plain,
! [X0,X1] : k4_xboole_0(X0,X1) = k4_xboole_0(X0,k3_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f116]) ).
fof(f12317,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f12318,plain,
! [X2,X0,X1] : k3_xboole_0(X0,k4_xboole_0(X1,X2)) = k4_xboole_0(k3_xboole_0(X0,X1),X2),
inference(cnf_transformation,[],[f118]) ).
fof(f12321,plain,
! [X2,X0,X1] : k4_xboole_0(X0,k4_xboole_0(X1,X2)) = k2_xboole_0(k4_xboole_0(X0,X1),k3_xboole_0(X0,X2)),
inference(cnf_transformation,[],[f121]) ).
fof(f12322,plain,
! [X2,X0,X1] : k4_xboole_0(X0,k2_xboole_0(X1,X2)) = k3_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,X2)),
inference(cnf_transformation,[],[f122]) ).
fof(f12390,plain,
! [X2,X0,X1] : k4_xboole_0(k3_xboole_0(X0,X1),k3_xboole_0(X2,X1)) = k3_xboole_0(k4_xboole_0(X0,X2),X1),
inference(cnf_transformation,[],[f180]) ).
fof(f12939,plain,
! [X0,X1] :
( v1_relat_1(k4_xboole_0(X1,X0))
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f5100]) ).
fof(f13127,plain,
! [X0] : k1_xboole_0 = k9_relat_1(k1_xboole_0,X0),
inference(cnf_transformation,[],[f722]) ).
fof(f16535,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f2485]) ).
fof(f20289,plain,
! [X2,X0,X1] :
( ~ v1_relat_1(X2)
| k9_relat_1(k2_xboole_0(X1,X2),k1_tarski(X0)) = k2_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0)))
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f9707]) ).
fof(f20290,plain,
! [X2,X0,X1] :
( k9_relat_1(k3_xboole_0(X1,X2),k1_tarski(X0)) = k3_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0)))
| ~ v1_relat_1(X2)
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f9708]) ).
fof(f20291,plain,
v1_relat_1(sK1507),
inference(cnf_transformation,[],[f12135]) ).
fof(f20292,plain,
v1_relat_1(sK1508),
inference(cnf_transformation,[],[f12135]) ).
fof(f20293,plain,
k9_relat_1(k4_xboole_0(sK1507,sK1508),k1_tarski(sK1506)) != k4_xboole_0(k9_relat_1(sK1507,k1_tarski(sK1506)),k9_relat_1(sK1508,k1_tarski(sK1506))),
inference(cnf_transformation,[],[f12135]) ).
fof(f20331,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k4_xboole_0(X1,k4_xboole_0(X1,X0)),
inference(definition_unfolding,[],[f12254,f12317,f12317]) ).
fof(f20332,plain,
! [X0] : k4_xboole_0(X0,k4_xboole_0(X0,X0)) = X0,
inference(definition_unfolding,[],[f12255,f12317]) ).
fof(f20334,plain,
! [X0] : np__0 = k4_xboole_0(X0,k4_xboole_0(X0,np__0)),
inference(definition_unfolding,[],[f12258,f16535,f12317,f16535]) ).
fof(f20335,plain,
! [X0] : k4_xboole_0(X0,np__0) = X0,
inference(definition_unfolding,[],[f12259,f16535]) ).
fof(f20363,plain,
! [X0,X1] : k4_xboole_0(X0,k2_xboole_0(X0,X1)) = np__0,
inference(definition_unfolding,[],[f12315,f16535]) ).
fof(f20364,plain,
! [X0,X1] : k4_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,k4_xboole_0(X0,X1))),
inference(definition_unfolding,[],[f12316,f12317]) ).
fof(f20365,plain,
! [X2,X0,X1] : k4_xboole_0(k4_xboole_0(X0,k4_xboole_0(X0,X1)),X2) = k4_xboole_0(X0,k4_xboole_0(X0,k4_xboole_0(X1,X2))),
inference(definition_unfolding,[],[f12318,f12317,f12317]) ).
fof(f20368,plain,
! [X2,X0,X1] : k4_xboole_0(X0,k4_xboole_0(X1,X2)) = k2_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X2))),
inference(definition_unfolding,[],[f12321,f12317]) ).
fof(f20369,plain,
! [X2,X0,X1] : k4_xboole_0(X0,k2_xboole_0(X1,X2)) = k4_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,X2))),
inference(definition_unfolding,[],[f12322,f12317]) ).
fof(f20395,plain,
! [X2,X0,X1] : k4_xboole_0(k4_xboole_0(X0,k4_xboole_0(X0,X1)),k4_xboole_0(X2,k4_xboole_0(X2,X1))) = k4_xboole_0(k4_xboole_0(X0,X2),k4_xboole_0(k4_xboole_0(X0,X2),X1)),
inference(definition_unfolding,[],[f12390,f12317,f12317,f12317]) ).
fof(f20645,plain,
! [X0] : np__0 = k9_relat_1(np__0,X0),
inference(definition_unfolding,[],[f13127,f16535,f16535]) ).
fof(f22245,plain,
! [X2,X0,X1] :
( ~ v1_relat_1(X2)
| k9_relat_1(k4_xboole_0(X1,k4_xboole_0(X1,X2)),k1_tarski(X0)) = k4_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k4_xboole_0(k9_relat_1(X1,k1_tarski(X0)),k9_relat_1(X2,k1_tarski(X0))))
| ~ v1_relat_1(X1) ),
inference(definition_unfolding,[],[f20290,f12317,f12317]) ).
fof(f23160,definition,
sF1509 = k4_xboole_0(sK1507,sK1508),
introduced(definition,[new_symbols(definition,[sF1509])],[function_definition]) ).
fof(f23161,plain,
k4_xboole_0(sK1507,sK1508) = sF1509,
inference(reorient_equations,[],[f23160]) ).
fof(f23162,definition,
sF1510 = k1_tarski(sK1506),
introduced(definition,[new_symbols(definition,[sF1510])],[function_definition]) ).
fof(f23163,plain,
k1_tarski(sK1506) = sF1510,
inference(reorient_equations,[],[f23162]) ).
fof(f23164,definition,
sF1511 = k9_relat_1(sF1509,sF1510),
introduced(definition,[new_symbols(definition,[sF1511])],[function_definition]) ).
fof(f23165,plain,
k9_relat_1(sF1509,sF1510) = sF1511,
inference(reorient_equations,[],[f23164]) ).
fof(f23166,definition,
sF1512 = k9_relat_1(sK1507,sF1510),
introduced(definition,[new_symbols(definition,[sF1512])],[function_definition]) ).
fof(f23167,plain,
k9_relat_1(sK1507,sF1510) = sF1512,
inference(reorient_equations,[],[f23166]) ).
fof(f23168,definition,
sF1513 = k9_relat_1(sK1508,sF1510),
introduced(definition,[new_symbols(definition,[sF1513])],[function_definition]) ).
fof(f23169,plain,
k9_relat_1(sK1508,sF1510) = sF1513,
inference(reorient_equations,[],[f23168]) ).
fof(f23170,definition,
sF1514 = k4_xboole_0(sF1512,sF1513),
introduced(definition,[new_symbols(definition,[sF1514])],[function_definition]) ).
fof(f23171,plain,
k4_xboole_0(sF1512,sF1513) = sF1514,
inference(reorient_equations,[],[f23170]) ).
fof(f23172,plain,
sF1511 != sF1514,
inference(definition_folding,[],[f20293,f23171,f23169,f23163,f23167,f23163,f23165,f23163,f23161]) ).
fof(f26142,plain,
! [X0] : np__0 = k4_xboole_0(X0,X0),
inference(forward_demodulation,[],[f20334,f20335]) ).
fof(f26909,plain,
! [X2,X0,X1] : k4_xboole_0(k4_xboole_0(X2,X1),k4_xboole_0(k4_xboole_0(X2,X1),X0)) = k4_xboole_0(k4_xboole_0(X2,k4_xboole_0(X2,X0)),k4_xboole_0(X0,k4_xboole_0(X0,X1))),
inference(superposition,[],[f20395,f20331]) ).
fof(f26916,plain,
! [X2,X0,X1] : k4_xboole_0(k4_xboole_0(X2,X1),k4_xboole_0(k4_xboole_0(X2,X1),X0)) = k4_xboole_0(X2,k4_xboole_0(X2,k4_xboole_0(X0,k4_xboole_0(X0,k4_xboole_0(X0,X1))))),
inference(forward_demodulation,[],[f26909,f20365]) ).
fof(f26934,plain,
! [X2,X0,X1] : k4_xboole_0(k4_xboole_0(X2,X1),k4_xboole_0(k4_xboole_0(X2,X1),X0)) = k4_xboole_0(X2,k4_xboole_0(X2,k4_xboole_0(X0,X1))),
inference(forward_demodulation,[],[f26916,f20364]) ).
fof(f26952,plain,
! [X2,X0,X1] : k4_xboole_0(X2,k4_xboole_0(X2,k4_xboole_0(X0,X1))) = k4_xboole_0(X2,k2_xboole_0(X1,k4_xboole_0(k4_xboole_0(X2,X1),X0))),
inference(forward_demodulation,[],[f26934,f12310]) ).
fof(f26968,plain,
! [X2,X0,X1] : k4_xboole_0(X2,k4_xboole_0(X2,k4_xboole_0(X0,X1))) = k4_xboole_0(X2,k2_xboole_0(X1,k4_xboole_0(X2,k2_xboole_0(X1,X0)))),
inference(forward_demodulation,[],[f26952,f12310]) ).
fof(f27034,plain,
! [X0,X1] : k4_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(k4_xboole_0(X0,X1),X0)) = k4_xboole_0(X0,k4_xboole_0(X1,k4_xboole_0(X1,X0))),
inference(superposition,[],[f20395,f20332]) ).
fof(f27036,plain,
! [X0,X1] : k4_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,X0))) = k4_xboole_0(k4_xboole_0(X0,X0),k4_xboole_0(X1,k4_xboole_0(X1,k4_xboole_0(X0,X0)))),
inference(superposition,[],[f20395,f20332]) ).
fof(f27037,plain,
! [X0,X1] : k4_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,X0))) = k4_xboole_0(X0,k2_xboole_0(X0,k4_xboole_0(X1,k4_xboole_0(X1,k4_xboole_0(X0,X0))))),
inference(forward_demodulation,[],[f27036,f12310]) ).
fof(f27039,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X1,k4_xboole_0(X1,X0))) = k4_xboole_0(X0,k2_xboole_0(X1,k4_xboole_0(k4_xboole_0(X0,X1),X0))),
inference(forward_demodulation,[],[f27034,f12310]) ).
fof(f27042,plain,
! [X0,X1] : np__0 = k4_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,X0))),
inference(forward_demodulation,[],[f27037,f20363]) ).
fof(f27044,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X1,k4_xboole_0(X1,X0))) = k4_xboole_0(X0,k2_xboole_0(X1,k4_xboole_0(X0,k2_xboole_0(X1,X0)))),
inference(forward_demodulation,[],[f27039,f12310]) ).
fof(f27047,plain,
! [X0,X1] : np__0 = k4_xboole_0(X0,k2_xboole_0(X1,X0)),
inference(forward_demodulation,[],[f27042,f20369]) ).
fof(f27049,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,k4_xboole_0(X0,X1))) = k4_xboole_0(X0,k4_xboole_0(X1,k4_xboole_0(X1,X0))),
inference(forward_demodulation,[],[f27044,f26968]) ).
fof(f27053,plain,
! [X0,X1] : k4_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X1,k4_xboole_0(X1,X0))),
inference(forward_demodulation,[],[f27049,f20364]) ).
fof(f27083,definition,
( spl1515_548
<=> v1_relat_1(sF1509) ),
introduced(definition,[new_symbols(definition,[spl1515_548])],[avatar_definition]) ).
fof(f27084,plain,
( v1_relat_1(sF1509)
| ~ spl1515_548 ),
inference(avatar_component_clause,[],[f27083]) ).
fof(f27085,plain,
( ~ v1_relat_1(sF1509)
| spl1515_548 ),
inference(avatar_component_clause,[],[f27083]) ).
fof(f27122,plain,
( v1_relat_1(sF1509)
| ~ v1_relat_1(sK1507) ),
inference(superposition,[],[f12939,f23161]) ).
fof(f27133,plain,
( ~ v1_relat_1(sK1507)
| spl1515_548 ),
inference(forward_subsumption_resolution,[],[f27122,f27085]) ).
fof(f27135,plain,
( $false
| spl1515_548 ),
inference(forward_subsumption_resolution,[],[f27133,f20291]) ).
fof(f27136,plain,
spl1515_548,
inference(avatar_contradiction_clause,[],[f27135]) ).
fof(f27157,plain,
! [X0] : k4_xboole_0(sK1507,k4_xboole_0(sK1508,X0)) = k2_xboole_0(sF1509,k4_xboole_0(sK1507,k4_xboole_0(sK1507,X0))),
inference(superposition,[],[f20368,f23161]) ).
fof(f27167,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X1,X0)) = k2_xboole_0(k4_xboole_0(X0,X1),X0),
inference(superposition,[],[f20368,f20332]) ).
fof(f27220,plain,
! [X0] : k2_xboole_0(k4_xboole_0(X0,X0),X0) = X0,
inference(superposition,[],[f20332,f27167]) ).
fof(f27231,plain,
! [X0] : k2_xboole_0(np__0,X0) = X0,
inference(forward_demodulation,[],[f27220,f26142]) ).
fof(f27404,plain,
! [X0] : k4_xboole_0(sK1507,k2_xboole_0(sK1508,X0)) = k4_xboole_0(sF1509,X0),
inference(superposition,[],[f12310,f23161]) ).
fof(f27517,plain,
! [X0] :
( v1_relat_1(k4_xboole_0(sF1509,X0))
| ~ v1_relat_1(sK1507) ),
inference(superposition,[],[f12939,f27404]) ).
fof(f27526,plain,
! [X0] : v1_relat_1(k4_xboole_0(sF1509,X0)),
inference(forward_subsumption_resolution,[],[f27517,f20291]) ).
fof(f27569,plain,
! [X0,X1] :
( ~ v1_relat_1(X0)
| k9_relat_1(k4_xboole_0(X0,k4_xboole_0(X0,sK1508)),k1_tarski(X1)) = k4_xboole_0(k9_relat_1(X0,k1_tarski(X1)),k4_xboole_0(k9_relat_1(X0,k1_tarski(X1)),k9_relat_1(sK1508,k1_tarski(X1)))) ),
inference(resolution,[],[f22245,f20292]) ).
fof(f27600,plain,
k4_xboole_0(sK1507,k4_xboole_0(sK1508,sK1508)) = k2_xboole_0(sF1509,k4_xboole_0(sK1507,sF1509)),
inference(superposition,[],[f27157,f23161]) ).
fof(f27617,plain,
k4_xboole_0(sK1507,k4_xboole_0(sK1508,sK1508)) = k2_xboole_0(sF1509,sK1507),
inference(forward_demodulation,[],[f27600,f12308]) ).
fof(f27624,plain,
k2_xboole_0(sF1509,sK1507) = k4_xboole_0(sK1507,np__0),
inference(forward_demodulation,[],[f27617,f26142]) ).
fof(f27628,plain,
sK1507 = k2_xboole_0(sF1509,sK1507),
inference(forward_demodulation,[],[f27624,f20335]) ).
fof(f28048,plain,
k4_xboole_0(sF1509,sK1507) = k4_xboole_0(sK1507,sK1507),
inference(superposition,[],[f12309,f27628]) ).
fof(f28063,plain,
! [X0,X1] : k4_xboole_0(X1,k4_xboole_0(X0,X1)) = k2_xboole_0(k4_xboole_0(X1,k2_xboole_0(X0,X1)),X1),
inference(superposition,[],[f27167,f12309]) ).
fof(f28068,plain,
! [X0,X1] : k2_xboole_0(np__0,X1) = k4_xboole_0(X1,k4_xboole_0(X0,X1)),
inference(forward_demodulation,[],[f28063,f27047]) ).
fof(f28076,plain,
np__0 = k4_xboole_0(sF1509,sK1507),
inference(forward_demodulation,[],[f28048,f26142]) ).
fof(f28081,plain,
! [X0,X1] : k2_xboole_0(np__0,X1) = k2_xboole_0(k4_xboole_0(X1,X0),X1),
inference(forward_demodulation,[],[f28068,f27167]) ).
fof(f28085,plain,
! [X0,X1] : k2_xboole_0(k4_xboole_0(X1,X0),X1) = X1,
inference(forward_demodulation,[],[f28081,f27231]) ).
fof(f28099,plain,
! [X0] : k4_xboole_0(sF1509,k4_xboole_0(sK1507,X0)) = k2_xboole_0(np__0,k4_xboole_0(sF1509,k4_xboole_0(sF1509,X0))),
inference(superposition,[],[f20368,f28076]) ).
fof(f28110,plain,
! [X0] : k4_xboole_0(sF1509,k4_xboole_0(sF1509,X0)) = k4_xboole_0(sF1509,k4_xboole_0(sK1507,X0)),
inference(forward_demodulation,[],[f28099,f27231]) ).
fof(f28200,plain,
! [X0,X1] :
( ~ v1_relat_1(X0)
| k9_relat_1(k2_xboole_0(X0,sK1508),k1_tarski(X1)) = k2_xboole_0(k9_relat_1(X0,k1_tarski(X1)),k9_relat_1(sK1508,k1_tarski(X1))) ),
inference(resolution,[],[f20289,f20292]) ).
fof(f29119,plain,
! [X0] : k9_relat_1(k2_xboole_0(sK1507,sK1508),k1_tarski(X0)) = k2_xboole_0(k9_relat_1(sK1507,k1_tarski(X0)),k9_relat_1(sK1508,k1_tarski(X0))),
inference(resolution,[],[f28200,f20291]) ).
fof(f29121,plain,
( ! [X0] : k9_relat_1(k2_xboole_0(sF1509,sK1508),k1_tarski(X0)) = k2_xboole_0(k9_relat_1(sF1509,k1_tarski(X0)),k9_relat_1(sK1508,k1_tarski(X0)))
| ~ spl1515_548 ),
inference(resolution,[],[f28200,f27084]) ).
fof(f29124,plain,
k9_relat_1(k2_xboole_0(sK1507,sK1508),sF1510) = k2_xboole_0(k9_relat_1(sK1507,sF1510),k9_relat_1(sK1508,sF1510)),
inference(superposition,[],[f29119,f23163]) ).
fof(f29128,plain,
k9_relat_1(k2_xboole_0(sK1507,sK1508),sF1510) = k2_xboole_0(k9_relat_1(sK1507,sF1510),sF1513),
inference(forward_demodulation,[],[f29124,f23169]) ).
fof(f29129,plain,
k2_xboole_0(sF1512,sF1513) = k9_relat_1(k2_xboole_0(sK1507,sK1508),sF1510),
inference(forward_demodulation,[],[f29128,f23167]) ).
fof(f30322,plain,
! [X0] : np__0 = k4_xboole_0(sF1509,k4_xboole_0(sK1507,k4_xboole_0(sK1508,X0))),
inference(superposition,[],[f20363,f27157]) ).
fof(f30380,plain,
! [X0] : np__0 = k4_xboole_0(sF1509,k4_xboole_0(sF1509,k4_xboole_0(sK1508,X0))),
inference(forward_demodulation,[],[f30322,f28110]) ).
fof(f30843,plain,
k2_xboole_0(sK1508,sK1507) = k2_xboole_0(sK1508,sF1509),
inference(superposition,[],[f12308,f23161]) ).
fof(f30924,plain,
k2_xboole_0(sK1507,sK1508) = k2_xboole_0(sK1508,sF1509),
inference(superposition,[],[f12252,f30843]) ).
fof(f31437,plain,
! [X0,X1] : k9_relat_1(k4_xboole_0(k4_xboole_0(sF1509,X0),k4_xboole_0(k4_xboole_0(sF1509,X0),sK1508)),k1_tarski(X1)) = k4_xboole_0(k9_relat_1(k4_xboole_0(sF1509,X0),k1_tarski(X1)),k4_xboole_0(k9_relat_1(k4_xboole_0(sF1509,X0),k1_tarski(X1)),k9_relat_1(sK1508,k1_tarski(X1)))),
inference(resolution,[],[f27569,f27526]) ).
fof(f31444,plain,
! [X0,X1] : k4_xboole_0(k9_relat_1(k4_xboole_0(sF1509,X0),k1_tarski(X1)),k4_xboole_0(k9_relat_1(k4_xboole_0(sF1509,X0),k1_tarski(X1)),k9_relat_1(sK1508,k1_tarski(X1)))) = k9_relat_1(k4_xboole_0(sF1509,k2_xboole_0(X0,k4_xboole_0(k4_xboole_0(sF1509,X0),sK1508))),k1_tarski(X1)),
inference(forward_demodulation,[],[f31437,f12310]) ).
fof(f31448,plain,
! [X0,X1] : k4_xboole_0(k9_relat_1(k4_xboole_0(sF1509,X0),k1_tarski(X1)),k4_xboole_0(k9_relat_1(k4_xboole_0(sF1509,X0),k1_tarski(X1)),k9_relat_1(sK1508,k1_tarski(X1)))) = k9_relat_1(k4_xboole_0(sF1509,k2_xboole_0(X0,k4_xboole_0(sF1509,k2_xboole_0(X0,sK1508)))),k1_tarski(X1)),
inference(forward_demodulation,[],[f31444,f12310]) ).
fof(f31452,plain,
! [X0,X1] : k4_xboole_0(k9_relat_1(k4_xboole_0(sF1509,X0),k1_tarski(X1)),k4_xboole_0(k9_relat_1(k4_xboole_0(sF1509,X0),k1_tarski(X1)),k9_relat_1(sK1508,k1_tarski(X1)))) = k9_relat_1(k4_xboole_0(sF1509,k4_xboole_0(sF1509,k4_xboole_0(sK1508,X0))),k1_tarski(X1)),
inference(forward_demodulation,[],[f31448,f26968]) ).
fof(f31455,plain,
! [X0,X1] : k4_xboole_0(k9_relat_1(k4_xboole_0(sF1509,X0),k1_tarski(X1)),k4_xboole_0(k9_relat_1(k4_xboole_0(sF1509,X0),k1_tarski(X1)),k9_relat_1(sK1508,k1_tarski(X1)))) = k9_relat_1(np__0,k1_tarski(X1)),
inference(forward_demodulation,[],[f31452,f30380]) ).
fof(f31456,plain,
! [X0,X1] : np__0 = k4_xboole_0(k9_relat_1(k4_xboole_0(sF1509,X0),k1_tarski(X1)),k4_xboole_0(k9_relat_1(k4_xboole_0(sF1509,X0),k1_tarski(X1)),k9_relat_1(sK1508,k1_tarski(X1)))),
inference(forward_demodulation,[],[f31455,f20645]) ).
fof(f31480,plain,
! [X0,X1] : k4_xboole_0(k9_relat_1(sK1508,k1_tarski(X0)),k9_relat_1(k4_xboole_0(sF1509,X1),k1_tarski(X0))) = k4_xboole_0(k9_relat_1(sK1508,k1_tarski(X0)),np__0),
inference(superposition,[],[f27053,f31456]) ).
fof(f31518,plain,
! [X0,X1] : k9_relat_1(sK1508,k1_tarski(X0)) = k4_xboole_0(k9_relat_1(sK1508,k1_tarski(X0)),k9_relat_1(k4_xboole_0(sF1509,X1),k1_tarski(X0))),
inference(forward_demodulation,[],[f31480,f20335]) ).
fof(f31573,plain,
! [X0] : k9_relat_1(sK1508,sF1510) = k4_xboole_0(k9_relat_1(sK1508,sF1510),k9_relat_1(k4_xboole_0(sF1509,X0),sF1510)),
inference(superposition,[],[f31518,f23163]) ).
fof(f31604,plain,
! [X0] : sF1513 = k4_xboole_0(sF1513,k9_relat_1(k4_xboole_0(sF1509,X0),sF1510)),
inference(forward_demodulation,[],[f31573,f23169]) ).
fof(f31625,plain,
sF1513 = k4_xboole_0(sF1513,k9_relat_1(sF1509,sF1510)),
inference(superposition,[],[f31604,f20332]) ).
fof(f31667,plain,
sF1513 = k4_xboole_0(sF1513,sF1511),
inference(forward_demodulation,[],[f31625,f23165]) ).
fof(f31699,plain,
k4_xboole_0(sF1511,sF1513) = k2_xboole_0(k4_xboole_0(sF1511,sF1513),sF1511),
inference(superposition,[],[f27167,f31667]) ).
fof(f31702,plain,
sF1511 = k4_xboole_0(sF1511,sF1513),
inference(forward_demodulation,[],[f31699,f28085]) ).
fof(f33633,plain,
k2_xboole_0(sK1507,sK1508) = k2_xboole_0(sF1509,sK1508),
inference(superposition,[],[f12252,f30924]) ).
fof(f33650,plain,
k2_xboole_0(sF1512,sF1513) = k9_relat_1(k2_xboole_0(sF1509,sK1508),sF1510),
inference(superposition,[],[f29129,f33633]) ).
fof(f39031,plain,
( k9_relat_1(k2_xboole_0(sF1509,sK1508),sF1510) = k2_xboole_0(k9_relat_1(sF1509,sF1510),k9_relat_1(sK1508,sF1510))
| ~ spl1515_548 ),
inference(superposition,[],[f29121,f23163]) ).
fof(f39042,plain,
( k9_relat_1(k2_xboole_0(sF1509,sK1508),sF1510) = k2_xboole_0(k9_relat_1(sF1509,sF1510),sF1513)
| ~ spl1515_548 ),
inference(forward_demodulation,[],[f39031,f23169]) ).
fof(f39044,plain,
( k2_xboole_0(sF1511,sF1513) = k9_relat_1(k2_xboole_0(sF1509,sK1508),sF1510)
| ~ spl1515_548 ),
inference(forward_demodulation,[],[f39042,f23165]) ).
fof(f39045,plain,
( k2_xboole_0(sF1512,sF1513) = k2_xboole_0(sF1511,sF1513)
| ~ spl1515_548 ),
inference(forward_demodulation,[],[f39044,f33650]) ).
fof(f39050,plain,
( k4_xboole_0(sF1511,sF1513) = k4_xboole_0(k2_xboole_0(sF1512,sF1513),sF1513)
| ~ spl1515_548 ),
inference(superposition,[],[f12309,f39045]) ).
fof(f39064,plain,
( k4_xboole_0(sF1512,sF1513) = k4_xboole_0(sF1511,sF1513)
| ~ spl1515_548 ),
inference(forward_demodulation,[],[f39050,f12309]) ).
fof(f39066,plain,
( sF1511 = k4_xboole_0(sF1512,sF1513)
| ~ spl1515_548 ),
inference(forward_demodulation,[],[f39064,f31702]) ).
fof(f39068,plain,
( sF1511 = sF1514
| ~ spl1515_548 ),
inference(forward_demodulation,[],[f39066,f23171]) ).
fof(f39070,plain,
( $false
| ~ spl1515_548 ),
inference(forward_subsumption_resolution,[],[f39068,f23172]) ).
fof(f39071,plain,
~ spl1515_548,
inference(avatar_contradiction_clause,[],[f39070]) ).
cnf(s479,plain,
spl1515_548,
inference(sat_conversion,[],[f27136]) ).
cnf(s615,plain,
~ spl1515_548,
inference(sat_conversion,[],[f39071]) ).
cnf(s616,plain,
$false,
inference(rat,[],[s479,s615]) ).
fof(f39072,plain,
$false,
inference(avatar_sat_refutation,[],[s616]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU419+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n016.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Mon Sep 28 05:22:04 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.35/3.13 % (3281694)Detected formulas, will run a generic FOF schedule.
% 15.35/3.13 % (3281699)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=2379537455:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 15.35/3.13 % (3281705)dis-21_1_sil=8000:lcm=predicate:random_seed=442297464: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)
% 15.35/3.13 % (3281704)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=970981138:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 15.35/3.13 % (3281703)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=563557596:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 15.35/3.13 % (3281700)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=2924835210:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 15.35/3.13 % (3281702)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1052505941:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 15.35/3.13 % (3281701)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=26016470:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 15.35/3.13 % (3281702)Refutation not found, incomplete strategy
% 15.35/3.13 % (3281702)------------------------------
% 15.35/3.13 % (3281702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.35/3.13 % (3281702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/3.13 % (3281702)CaDiCaL version: 2.1.3
% 15.35/3.13 % (3281702)Termination reason: Refutation not found, incomplete strategy
% 15.35/3.13 % (3281702)Time elapsed: 0.033 s
% 15.35/3.13 % (3281702)Peak memory usage: 94 MB
% 15.35/3.13 % (3281702)Instructions burned: 47 (million)
% 15.35/3.13 % (3281703)Instruction limit reached!
% 15.35/3.13 % (3281703)------------------------------
% 15.35/3.13 % (3281703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.35/3.13 % (3281703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/3.13 % (3281703)CaDiCaL version: 2.1.3
% 15.35/3.13 % (3281703)Termination reason: Instruction limit
% 15.35/3.13 % (3281703)Termination phase: Saturation
% 15.35/3.13 % (3281703)Time elapsed: 0.079 s
% 15.35/3.13 % (3281703)Peak memory usage: 94 MB
% 15.35/3.13 % (3281703)Instructions burned: 120 (million)
% 15.35/3.13 % (3281704)Instruction limit reached!
% 15.35/3.13 % (3281704)------------------------------
% 15.35/3.13 % (3281704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.35/3.13 % (3281704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/3.13 % (3281704)CaDiCaL version: 2.1.3
% 15.35/3.13 % (3281704)Termination reason: Instruction limit
% 15.35/3.13 % (3281704)Termination phase: Preprocessing 3
% 15.35/3.13 % (3281704)Time elapsed: 0.087 s
% 15.35/3.13 % (3281704)Peak memory usage: 94 MB
% 15.35/3.13 % (3281704)Instructions burned: 140 (million)
% 15.35/3.13 % (3281705)Instruction limit reached!
% 15.35/3.13 % (3281705)------------------------------
% 15.35/3.13 % (3281705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.35/3.13 % (3281705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.35/3.13 % (3281705)CaDiCaL version: 2.1.3
% 15.35/3.13 % (3281705)Termination reason: Instruction limit
% 15.35/3.13 % (3281705)Termination phase: Clausification
% 15.35/3.13 % (3281705)Time elapsed: 0.099 s
% 15.35/3.13 % (3281705)Peak memory usage: 95 MB
% 15.35/3.13 % (3281705)Instructions burned: 129 (million)
% 15.35/3.13 % (3281714)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3593803189:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 15.35/3.13 % (3281713)lrs+10_1_sil=8000:sp=occurrence:random_seed=3740681750:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 15.35/3.13 % (3281715)lrs+1011_1_sil=32000:sp=occurrence:random_seed=202036905:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 15.35/3.13 % (3281702)------------------------------
% 15.35/3.13 % (3281702)------------------------------
% 15.35/3.13 % (3281714)Instruction limit reached!
% 15.35/3.13 % (3281714)------------------------------
% 15.35/3.13 % (3281714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281714)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281714)Termination reason: Instruction limit
% 10.07/3.31 % (3281714)Termination phase: Saturation
% 10.07/3.31 % (3281714)Time elapsed: 0.089 s
% 10.07/3.31 % (3281714)Peak memory usage: 95 MB
% 10.07/3.31 % (3281714)Instructions burned: 157 (million)
% 10.07/3.31 % (3281713)Instruction limit reached!
% 10.07/3.31 % (3281713)------------------------------
% 10.07/3.31 % (3281713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281713)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281713)Termination reason: Instruction limit
% 10.07/3.31 % (3281713)Termination phase: Saturation
% 10.07/3.31 % (3281713)Time elapsed: 0.193 s
% 10.07/3.31 % (3281713)Peak memory usage: 97 MB
% 10.07/3.31 % (3281713)Instructions burned: 285 (million)
% 10.07/3.31 % (3281719)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=3920970063:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 10.07/3.31 % (3281720)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1132766962:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 10.07/3.31 % (3281715)Instruction limit reached!
% 10.07/3.31 % (3281715)------------------------------
% 10.07/3.31 % (3281715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281715)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281715)Termination reason: Instruction limit
% 10.07/3.31 % (3281715)Termination phase: Saturation
% 10.07/3.31 % (3281715)Time elapsed: 0.223 s
% 10.07/3.31 % (3281715)Peak memory usage: 96 MB
% 10.07/3.31 % (3281715)Instructions burned: 326 (million)
% 10.07/3.31 % (3281721)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2271961326:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 10.07/3.31 % (3281719)Instruction limit reached!
% 10.07/3.31 % (3281719)------------------------------
% 10.07/3.31 % (3281719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281719)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281719)Termination reason: Instruction limit
% 10.07/3.31 % (3281719)Termination phase: Property scanning
% 10.07/3.31 % (3281719)Time elapsed: 0.152 s
% 10.07/3.31 % (3281719)Peak memory usage: 98 MB
% 10.07/3.31 % (3281719)Instructions burned: 250 (million)
% 10.07/3.31 % (3281724)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4101691179:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 10.07/3.31 % (3281720)Instruction limit reached!
% 10.07/3.31 % (3281720)------------------------------
% 10.07/3.31 % (3281720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281720)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281720)Termination reason: Instruction limit
% 10.07/3.31 % (3281720)Termination phase: Saturation
% 10.07/3.31 % (3281720)Time elapsed: 0.184 s
% 10.07/3.31 % (3281720)Peak memory usage: 97 MB
% 10.07/3.31 % (3281720)Instructions burned: 294 (million)
% 10.07/3.31 % (3281724)Instruction limit reached!
% 10.07/3.31 % (3281724)------------------------------
% 10.07/3.31 % (3281724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281724)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281724)Termination reason: Instruction limit
% 10.07/3.31 % (3281724)Termination phase: Saturation
% 10.07/3.31 % (3281724)Time elapsed: 0.072 s
% 10.07/3.31 % (3281724)Peak memory usage: 95 MB
% 10.07/3.31 % (3281724)Instructions burned: 114 (million)
% 10.07/3.31 % (3281726)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1743683078:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 10.07/3.31 % (3281728)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3380377810:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 10.07/3.31 % (3281729)lrs+10_1_sil=8000:sp=occurrence:random_seed=1768457399:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 10.07/3.31 % (3281726)Instruction limit reached!
% 10.07/3.31 % (3281726)------------------------------
% 10.07/3.31 % (3281726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281726)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281726)Termination reason: Instruction limit
% 10.07/3.31 % (3281726)Termination phase: Preprocessing 3
% 10.07/3.31 % (3281726)Time elapsed: 0.090 s
% 10.07/3.31 % (3281726)Peak memory usage: 97 MB
% 10.07/3.31 % (3281726)Instructions burned: 128 (million)
% 10.07/3.31 % (3281728)Instruction limit reached!
% 10.07/3.31 % (3281728)------------------------------
% 10.07/3.31 % (3281728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281728)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281728)Termination reason: Instruction limit
% 10.07/3.31 % (3281728)Termination phase: SInE selection
% 10.07/3.31 % (3281728)Time elapsed: 0.054 s
% 10.07/3.31 % (3281728)Peak memory usage: 89 MB
% 10.07/3.31 % (3281728)Instructions burned: 114 (million)
% 10.07/3.31 % (3281733)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=448184905:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 10.07/3.31 % (3281734)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2641051600:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 10.07/3.31 % (3281733)Instruction limit reached!
% 10.07/3.31 % (3281733)------------------------------
% 10.07/3.31 % (3281733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281733)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281733)Termination reason: Instruction limit
% 10.07/3.31 % (3281733)Termination phase: Saturation
% 10.07/3.31 % (3281733)Time elapsed: 0.282 s
% 10.07/3.31 % (3281733)Peak memory usage: 97 MB
% 10.07/3.31 % (3281733)Instructions burned: 438 (million)
% 10.07/3.31 % (3281737)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1669627728:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 10.07/3.31 % (3281729)Instruction limit reached!
% 10.07/3.31 % (3281729)------------------------------
% 10.07/3.31 % (3281729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281729)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281729)Termination reason: Instruction limit
% 10.07/3.31 % (3281729)Termination phase: Saturation
% 10.07/3.31 % (3281729)Time elapsed: 0.596 s
% 10.07/3.31 % (3281729)Peak memory usage: 104 MB
% 10.07/3.31 % (3281729)Instructions burned: 908 (million)
% 10.07/3.31 % (3281737)Instruction limit reached!
% 10.07/3.31 % (3281737)------------------------------
% 10.07/3.31 % (3281737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281737)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281737)Termination reason: Instruction limit
% 10.07/3.31 % (3281737)Termination phase: Saturation
% 10.07/3.31 % (3281737)Time elapsed: 0.084 s
% 10.07/3.31 % (3281737)Peak memory usage: 96 MB
% 10.07/3.31 % (3281737)Instructions burned: 136 (million)
% 10.07/3.31 % (3281739)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1037574572:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi)
% 10.07/3.31 % (3281740)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1692740366:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 10.07/3.31 % (3281739)Instruction limit reached!
% 10.07/3.31 % (3281739)------------------------------
% 10.07/3.31 % (3281739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281739)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281739)Termination reason: Instruction limit
% 10.07/3.31 % (3281739)Termination phase: Saturation
% 10.07/3.31 % (3281739)Time elapsed: 0.323 s
% 10.07/3.31 % (3281739)Peak memory usage: 106 MB
% 10.07/3.31 % (3281739)Instructions burned: 593 (million)
% 10.07/3.31 % (3281699)First to succeed.
% 10.07/3.31 % (3281699)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3281694"
% 10.07/3.31 % (3281743)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=759288319:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/125Mi)
% 10.07/3.31 % (3281701)Also succeeded, but the first one will report.
% 10.07/3.31 % (3281721)Instruction limit reached!
% 10.07/3.31 % (3281721)------------------------------
% 10.07/3.31 % (3281721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281721)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281721)Termination reason: Instruction limit
% 10.07/3.31 % (3281721)Termination phase: Saturation
% 10.07/3.31 % (3281721)Time elapsed: 1.504 s
% 10.07/3.31 % (3281721)Peak memory usage: 241 MB
% 10.07/3.31 % (3281721)Instructions burned: 2351 (million)
% 10.07/3.31 % (3281743)Instruction limit reached!
% 10.07/3.31 % (3281743)------------------------------
% 10.07/3.31 % (3281743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.07/3.31 % (3281743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.07/3.31 % (3281743)CaDiCaL version: 2.1.3
% 10.07/3.31 % (3281743)Termination reason: Instruction limit
% 10.07/3.31 % (3281743)Termination phase: Property scanning
% 10.07/3.31 % (3281743)Time elapsed: 0.073 s
% 10.07/3.31 % (3281743)Peak memory usage: 92 MB
% 10.07/3.31 % (3281743)Instructions burned: 126 (million)
% 10.07/3.31 % (3281699)Refutation found. Thanks to Tanya!
% 10.07/3.31 % SZS status Theorem for theBenchmark
% 10.07/3.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/3.50 % (3281699)------------------------------
% 0.17/3.50 % (3281699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/3.50 % (3281699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/3.50 % (3281699)CaDiCaL version: 2.1.3
% 0.17/3.50 % (3281699)Termination reason: Refutation
% 0.17/3.50 % (3281699)Time elapsed: 2.003 s
% 0.17/3.50 % (3281699)Peak memory usage: 235 MB
% 0.17/3.50 % (3281699)Instructions burned: 5953 (million)
% 0.17/3.50 % (3281699)------------------------------
% 0.17/3.50 % (3281699)------------------------------
% 0.17/3.50 % (3281694)Success in time 2.445 s
% 0.17/3.50 % Vampire exiting
%------------------------------------------------------------------------------