%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : BOO073-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:36:01 AM UTC 2026
% Result : Unsatisfiable 21.55s 7.81s
% Output : Refutation 50.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 74
% Number of leaves : 2
% Syntax : Number of formulae : 148 ( 148 unt; 0 def)
% Number of atoms : 148 ( 147 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 345 ( 345 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : inverse(add(inverse(add(inverse(add(X0,X1)),X2)),inverse(add(X0,inverse(add(inverse(X2),inverse(add(X2,X3)))))))) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dn1) ).
fof(f2,negated_conjecture,
add(add(a,b),c) != add(a,add(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',huntinton_2) ).
fof(f3,plain,
! [X2,X0,X1,X4,X5] : inverse(add(inverse(add(X0,X4)),inverse(add(inverse(add(inverse(add(X1,X2)),X0)),inverse(add(inverse(X4),inverse(add(X4,X5)))))))) = X4,
inference(superposition,[],[f1,f1]) ).
fof(f18,plain,
! [X0] : inverse(X0) = inverse(add(inverse(add(X0,inverse(X0))),X0)),
inference(superposition,[],[f3,f1]) ).
fof(f27,plain,
! [X0,X1] : inverse(add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1)))))))) = X0,
inference(superposition,[],[f1,f18]) ).
fof(f45,plain,
! [X0] : inverse(add(inverse(X0),inverse(add(X0,X0)))) = X0,
inference(superposition,[],[f27,f27]) ).
fof(f47,plain,
! [X2,X0,X1] : inverse(add(inverse(add(inverse(add(X1,X2)),X0)),inverse(add(X1,X0)))) = X0,
inference(superposition,[],[f1,f27]) ).
fof(f59,plain,
! [X0,X1,X5] : inverse(add(inverse(add(X0,X5)),inverse(add(inverse(add(X1,X0)),X5)))) = X5,
inference(superposition,[],[f47,f3]) ).
fof(f62,plain,
! [X2,X0] : inverse(add(inverse(add(X0,X2)),inverse(add(inverse(X0),X2)))) = X2,
inference(superposition,[],[f47,f27]) ).
fof(f73,plain,
! [X0,X1] : inverse(add(inverse(add(inverse(add(X0,X1)),X0)),inverse(add(X0,X1)))) = X0,
inference(superposition,[],[f3,f47]) ).
fof(f106,plain,
! [X0,X1] : inverse(add(inverse(X1),X0)) = inverse(add(X0,inverse(add(X1,inverse(add(inverse(X1),X0)))))),
inference(superposition,[],[f47,f62]) ).
fof(f125,plain,
! [X0] : inverse(add(inverse(X0),inverse(add(X0,inverse(X0))))) = X0,
inference(superposition,[],[f73,f18]) ).
fof(f133,plain,
! [X0] : inverse(add(inverse(add(inverse(X0),X0)),inverse(X0))) = X0,
inference(superposition,[],[f3,f73]) ).
fof(f195,plain,
! [X0] : inverse(X0) = inverse(add(X0,inverse(add(inverse(X0),inverse(X0))))),
inference(superposition,[],[f47,f133]) ).
fof(f230,plain,
! [X0] : inverse(add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(X0))))))) = X0,
inference(superposition,[],[f27,f195]) ).
fof(f231,plain,
! [X0,X1] : inverse(add(inverse(add(inverse(X0),X1)),inverse(add(X0,X1)))) = X1,
inference(superposition,[],[f47,f195]) ).
fof(f246,plain,
! [X0] : inverse(add(inverse(X0),inverse(X0))) = X0,
inference(forward_demodulation,[],[f230,f106]) ).
fof(f249,plain,
! [X2,X0,X1] : inverse(add(X0,X0)) = add(inverse(add(inverse(add(X1,X2)),X0)),inverse(add(X1,X0))),
inference(superposition,[],[f246,f47]) ).
fof(f250,plain,
! [X0,X1] : inverse(add(X0,X0)) = add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0))),
inference(superposition,[],[f246,f62]) ).
fof(f251,plain,
! [X0,X1] : inverse(add(X0,X0)) = add(inverse(add(inverse(add(X0,X1)),X0)),inverse(add(X0,X1))),
inference(superposition,[],[f246,f73]) ).
fof(f257,plain,
! [X0] : inverse(add(inverse(X0),inverse(X0))) = add(X0,inverse(add(inverse(X0),inverse(X0)))),
inference(superposition,[],[f246,f195]) ).
fof(f259,plain,
! [X0] : inverse(X0) = inverse(add(X0,X0)),
inference(superposition,[],[f195,f246]) ).
fof(f284,plain,
! [X0] : add(X0,X0) = X0,
inference(forward_demodulation,[],[f257,f246]) ).
fof(f290,plain,
! [X0,X1] : inverse(X0) = add(inverse(add(inverse(add(X0,X1)),X0)),inverse(add(X0,X1))),
inference(forward_demodulation,[],[f251,f259]) ).
fof(f291,plain,
! [X0,X1] : inverse(X0) = add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0))),
inference(forward_demodulation,[],[f250,f259]) ).
fof(f292,plain,
! [X2,X0,X1] : inverse(X0) = add(inverse(add(inverse(add(X1,X2)),X0)),inverse(add(X1,X0))),
inference(forward_demodulation,[],[f249,f259]) ).
fof(f308,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(superposition,[],[f246,f284]) ).
fof(f623,plain,
! [X0,X1] : add(X0,inverse(add(inverse(inverse(add(X1,X0))),inverse(add(inverse(X1),X0))))) = inverse(inverse(add(inverse(X1),X0))),
inference(superposition,[],[f291,f62]) ).
fof(f630,plain,
! [X0] : inverse(inverse(X0)) = add(X0,inverse(add(inverse(inverse(X0)),inverse(X0)))),
inference(superposition,[],[f291,f246]) ).
fof(f729,plain,
! [X0] : add(X0,inverse(add(X0,inverse(X0)))) = X0,
inference(forward_demodulation,[],[f630,f308]) ).
fof(f736,plain,
! [X0,X1] : add(inverse(X1),X0) = add(X0,inverse(add(inverse(inverse(add(X1,X0))),inverse(add(inverse(X1),X0))))),
inference(forward_demodulation,[],[f623,f308]) ).
fof(f757,plain,
! [X0,X1] : add(inverse(X1),X0) = add(X0,inverse(add(add(X1,X0),inverse(add(inverse(X1),X0))))),
inference(forward_demodulation,[],[f736,f308]) ).
fof(f792,plain,
! [X0] : inverse(inverse(add(X0,inverse(X0)))) = add(inverse(X0),inverse(add(inverse(X0),inverse(add(X0,inverse(X0)))))),
inference(superposition,[],[f291,f729]) ).
fof(f803,plain,
! [X0] : inverse(inverse(add(X0,inverse(X0)))) = add(inverse(X0),X0),
inference(forward_demodulation,[],[f792,f125]) ).
fof(f821,plain,
! [X0] : add(X0,inverse(X0)) = add(inverse(X0),X0),
inference(forward_demodulation,[],[f803,f308]) ).
fof(f1142,plain,
! [X0,X1] : inverse(X1) = add(inverse(add(X0,X1)),inverse(add(inverse(add(inverse(X0),X0)),X1))),
inference(superposition,[],[f292,f133]) ).
fof(f1160,plain,
! [X2,X0,X1] : inverse(inverse(add(X1,X0))) = add(X0,inverse(add(inverse(add(X1,X2)),inverse(add(X1,X0))))),
inference(superposition,[],[f292,f47]) ).
fof(f1161,plain,
! [X0,X1] : add(X0,inverse(add(X1,inverse(add(inverse(X1),X0))))) = inverse(inverse(add(inverse(X1),X0))),
inference(superposition,[],[f292,f62]) ).
fof(f1162,plain,
! [X0,X1] : inverse(inverse(add(X0,X1))) = add(X0,inverse(add(inverse(add(X0,X1)),inverse(add(X0,X1))))),
inference(superposition,[],[f292,f73]) ).
fof(f1163,plain,
! [X0,X1] : inverse(inverse(add(X1,X0))) = add(X0,inverse(add(inverse(X1),inverse(add(X1,X0))))),
inference(superposition,[],[f292,f231]) ).
fof(f1264,plain,
! [X0,X1] : add(X1,X0) = add(X0,inverse(add(inverse(X1),inverse(add(X1,X0))))),
inference(forward_demodulation,[],[f1163,f308]) ).
fof(f1265,plain,
! [X0,X1] : inverse(inverse(add(X0,X1))) = add(X0,add(X0,X1)),
inference(forward_demodulation,[],[f1162,f246]) ).
fof(f1266,plain,
! [X0,X1] : add(inverse(X1),X0) = add(X0,inverse(add(X1,inverse(add(inverse(X1),X0))))),
inference(forward_demodulation,[],[f1161,f308]) ).
fof(f1267,plain,
! [X2,X0,X1] : add(X1,X0) = add(X0,inverse(add(inverse(add(X1,X2)),inverse(add(X1,X0))))),
inference(forward_demodulation,[],[f1160,f308]) ).
fof(f1276,plain,
! [X0,X1] : inverse(X1) = add(inverse(add(X0,X1)),inverse(add(inverse(add(X0,inverse(X0))),X1))),
inference(forward_demodulation,[],[f1142,f821]) ).
fof(f1297,plain,
! [X0,X1] : add(X0,X1) = add(X0,add(X0,X1)),
inference(forward_demodulation,[],[f1265,f308]) ).
fof(f1315,plain,
! [X0,X1] : inverse(X0) = add(inverse(add(X1,X0)),inverse(X0)),
inference(superposition,[],[f1297,f291]) ).
fof(f1366,plain,
! [X0,X1] : add(X0,X1) = add(add(X0,X1),inverse(add(inverse(X0),inverse(add(X0,X1))))),
inference(superposition,[],[f1264,f1297]) ).
fof(f1384,plain,
! [X2,X0,X1] : inverse(add(inverse(add(inverse(add(X1,X2)),X0)),inverse(add(X0,X1)))) = X0,
inference(superposition,[],[f1,f1264]) ).
fof(f1400,plain,
! [X0,X1] : add(X0,X1) = add(X1,add(X0,X1)),
inference(superposition,[],[f1297,f1264]) ).
fof(f1707,plain,
! [X0,X1] : inverse(inverse(X0)) = add(inverse(inverse(X0)),inverse(add(X1,inverse(X0)))),
inference(superposition,[],[f292,f1315]) ).
fof(f1708,plain,
! [X0,X1] : inverse(X0) = inverse(add(inverse(inverse(X0)),inverse(add(X1,inverse(X0))))),
inference(superposition,[],[f47,f1315]) ).
fof(f1748,plain,
! [X0,X1] : inverse(X0) = inverse(add(X0,inverse(add(X1,inverse(X0))))),
inference(forward_demodulation,[],[f1708,f308]) ).
fof(f1749,plain,
! [X0,X1] : add(X0,inverse(add(X1,inverse(X0)))) = X0,
inference(forward_demodulation,[],[f1707,f308]) ).
fof(f1816,plain,
! [X0,X1] : inverse(X0) = add(inverse(X0),inverse(add(X1,X0))),
inference(superposition,[],[f1749,f308]) ).
fof(f1832,plain,
! [X0,X1] : add(X0,X1) = add(add(X0,X1),X0),
inference(superposition,[],[f1749,f73]) ).
fof(f1843,plain,
! [X2,X0,X1] : inverse(add(inverse(add(inverse(add(add(X0,X1),X2)),X0)),inverse(add(X0,X1)))) = X0,
inference(superposition,[],[f1,f1749]) ).
fof(f1958,plain,
! [X0,X1] : inverse(X0) = add(inverse(add(X0,X1)),inverse(X0)),
inference(superposition,[],[f1315,f1832]) ).
fof(f1960,plain,
! [X0,X1] : add(X0,inverse(add(inverse(X0),X1))) = X0,
inference(superposition,[],[f1749,f1832]) ).
fof(f2025,plain,
! [X0,X1] : inverse(X0) = add(inverse(X0),inverse(add(X0,X1))),
inference(superposition,[],[f1960,f308]) ).
fof(f2081,plain,
! [X0,X1] : add(inverse(add(inverse(X0),X1)),X0) = X0,
inference(superposition,[],[f1400,f1960]) ).
fof(f2164,plain,
! [X0,X1] : inverse(add(inverse(add(inverse(X0),X1)),inverse(add(X1,inverse(add(X0,inverse(X0))))))) = X1,
inference(superposition,[],[f1384,f18]) ).
fof(f2187,plain,
! [X0,X1] : inverse(add(inverse(X1),X0)) = inverse(add(X0,inverse(add(inverse(add(inverse(X1),X0)),X1)))),
inference(superposition,[],[f1384,f62]) ).
fof(f2189,plain,
! [X0,X1] : inverse(add(X1,X0)) = inverse(add(X0,inverse(add(inverse(add(X1,X0)),inverse(X1))))),
inference(superposition,[],[f1384,f231]) ).
fof(f2190,plain,
! [X2,X0,X1] : inverse(add(X1,X0)) = inverse(add(X0,inverse(add(inverse(add(X1,X0)),inverse(add(X1,X2)))))),
inference(superposition,[],[f1384,f47]) ).
fof(f2337,plain,
! [X0,X1] : inverse(add(X1,X0)) = inverse(add(X0,inverse(inverse(X1)))),
inference(forward_demodulation,[],[f2189,f1958]) ).
fof(f2338,plain,
! [X0,X1] : inverse(add(X0,inverse(X1))) = inverse(add(inverse(X1),X0)),
inference(forward_demodulation,[],[f2187,f2081]) ).
fof(f2368,plain,
! [X0,X1] : inverse(add(X0,X1)) = inverse(add(X1,X0)),
inference(forward_demodulation,[],[f2337,f308]) ).
fof(f2510,plain,
! [X2,X0,X1] : inverse(add(inverse(add(X0,inverse(add(X1,X2)))),inverse(add(X1,X0)))) = X0,
inference(superposition,[],[f47,f2368]) ).
fof(f2517,plain,
! [X2,X0,X1] : add(X0,X1) = add(X1,inverse(add(inverse(add(X0,X1)),inverse(add(X0,X2))))),
inference(superposition,[],[f1267,f2368]) ).
fof(f2525,plain,
! [X0,X1] : add(X1,X0) = inverse(add(inverse(add(X0,X1)),inverse(add(add(X1,X0),add(X1,X0))))),
inference(superposition,[],[f45,f2368]) ).
fof(f2535,plain,
! [X0,X1] : add(X1,X0) = inverse(inverse(add(X0,X1))),
inference(superposition,[],[f308,f2368]) ).
fof(f2542,plain,
! [X2,X0,X1] : add(X1,X0) = add(add(X1,X0),inverse(add(inverse(add(X0,X1)),X2))),
inference(superposition,[],[f1960,f2368]) ).
fof(f2544,plain,
! [X0,X1] : add(X0,X1) = add(X1,X0),
inference(forward_demodulation,[],[f2535,f308]) ).
fof(f2552,plain,
! [X0,X1] : add(X1,X0) = inverse(add(inverse(add(X0,X1)),inverse(add(X1,X0)))),
inference(forward_demodulation,[],[f2525,f259]) ).
fof(f2561,plain,
! [X2,X0,X1] : inverse(add(inverse(add(X1,X0)),inverse(add(X0,inverse(add(X1,X2)))))) = X0,
inference(forward_demodulation,[],[f2510,f2338]) ).
fof(f3207,plain,
! [X2,X0,X1] : add(inverse(add(X0,X1)),X2) = add(X2,inverse(add(add(X1,X0),inverse(add(inverse(add(X0,X1)),X2))))),
inference(superposition,[],[f1266,f2368]) ).
fof(f3348,plain,
! [X2,X0,X1] : add(inverse(add(X0,X1)),X2) = add(X2,inverse(add(X1,X0))),
inference(forward_demodulation,[],[f3207,f2542]) ).
fof(f3595,plain,
! [X2,X0,X1] : inverse(add(X0,inverse(add(X1,X2)))) = inverse(add(X0,inverse(add(X2,X1)))),
inference(superposition,[],[f2368,f3348]) ).
fof(f3597,plain,
! [X2,X0,X1] : add(X0,inverse(add(X1,X2))) = add(X0,inverse(add(X2,X1))),
inference(superposition,[],[f2544,f3348]) ).
fof(f4020,plain,
! [X2,X0,X1] : add(X2,add(X0,X1)) = add(inverse(add(inverse(add(X0,X1)),inverse(add(X1,X0)))),X2),
inference(superposition,[],[f3348,f2552]) ).
fof(f4068,plain,
! [X2,X0,X1] : add(X2,add(X0,X1)) = add(add(X1,X0),X2),
inference(forward_demodulation,[],[f4020,f2552]) ).
fof(f4439,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X1,X0),X2),
inference(superposition,[],[f2544,f4068]) ).
fof(f4444,plain,
! [X2,X0,X1] : add(add(X1,X0),X2) = add(add(X0,X1),add(add(X1,X0),X2)),
inference(superposition,[],[f1832,f4068]) ).
fof(f9021,plain,
! [X0,X1] : inverse(inverse(add(X0,X1))) = add(X0,inverse(add(inverse(add(X0,X1)),X0))),
inference(superposition,[],[f290,f73]) ).
fof(f9271,plain,
! [X0,X1] : inverse(inverse(add(X0,X1))) = add(X0,inverse(add(X0,inverse(add(X0,X1))))),
inference(forward_demodulation,[],[f9021,f3597]) ).
fof(f9366,plain,
! [X0,X1] : add(X0,X1) = add(X0,inverse(add(X0,inverse(add(X0,X1))))),
inference(forward_demodulation,[],[f9271,f308]) ).
fof(f9537,plain,
! [X0,X1] : add(X1,X0) = add(X1,inverse(add(X1,inverse(add(X0,X1))))),
inference(superposition,[],[f9366,f2368]) ).
fof(f34222,plain,
! [X2,X0,X1] : inverse(add(inverse(add(X1,X0)),X2)) = inverse(add(X2,inverse(add(inverse(add(inverse(add(X1,X0)),X2)),add(X0,X1))))),
inference(superposition,[],[f2190,f2552]) ).
fof(f34584,plain,
! [X2,X0,X1] : inverse(add(inverse(add(X1,X0)),X2)) = inverse(add(X2,inverse(add(add(X0,X1),inverse(add(inverse(add(X1,X0)),X2)))))),
inference(forward_demodulation,[],[f34222,f3595]) ).
fof(f34736,plain,
! [X2,X0,X1] : inverse(add(inverse(add(X1,X0)),X2)) = inverse(add(X2,inverse(add(X0,X1)))),
inference(forward_demodulation,[],[f34584,f2542]) ).
fof(f70547,plain,
! [X0,X1] : inverse(add(inverse(add(add(X0,inverse(X0)),X1)),X0)) = inverse(add(inverse(add(inverse(X0),inverse(add(inverse(add(add(X0,inverse(X0)),X1)),X0)))),X0)),
inference(superposition,[],[f2164,f1843]) ).
fof(f70940,plain,
! [X0,X1] : inverse(add(inverse(add(add(X0,inverse(X0)),X1)),X0)) = inverse(add(X0,inverse(add(inverse(add(inverse(add(add(X0,inverse(X0)),X1)),X0)),inverse(X0))))),
inference(forward_demodulation,[],[f70547,f34736]) ).
fof(f71186,plain,
! [X0,X1] : inverse(X0) = inverse(add(inverse(add(add(X0,inverse(X0)),X1)),X0)),
inference(forward_demodulation,[],[f70940,f1748]) ).
fof(f71305,plain,
! [X0,X1] : inverse(X0) = inverse(add(X0,inverse(add(X1,add(X0,inverse(X0)))))),
inference(forward_demodulation,[],[f71186,f34736]) ).
fof(f71608,plain,
! [X0,X1] : inverse(inverse(add(X1,add(X0,inverse(X0))))) = add(inverse(X0),inverse(add(inverse(add(X0,inverse(X0))),inverse(add(X1,add(X0,inverse(X0))))))),
inference(superposition,[],[f1276,f71305]) ).
fof(f71891,plain,
! [X0,X1] : add(inverse(X0),inverse(inverse(add(X0,inverse(X0))))) = inverse(inverse(add(X1,add(X0,inverse(X0))))),
inference(forward_demodulation,[],[f71608,f1816]) ).
fof(f72058,plain,
! [X0,X1] : add(inverse(X0),inverse(inverse(add(X0,inverse(X0))))) = add(X1,add(X0,inverse(X0))),
inference(forward_demodulation,[],[f71891,f308]) ).
fof(f72187,plain,
! [X0,X1] : add(inverse(X0),add(X0,inverse(X0))) = add(X1,add(X0,inverse(X0))),
inference(forward_demodulation,[],[f72058,f308]) ).
fof(f72273,plain,
! [X0,X1] : add(X0,inverse(X0)) = add(X1,add(X0,inverse(X0))),
inference(forward_demodulation,[],[f72187,f1400]) ).
fof(f72572,plain,
! [X0,X1] : add(X0,inverse(X0)) = add(X1,inverse(add(X1,inverse(add(X0,inverse(X0)))))),
inference(superposition,[],[f9366,f72273]) ).
fof(f72626,plain,
! [X0,X1] : add(X1,inverse(add(X0,inverse(X0)))) = X1,
inference(superposition,[],[f1960,f72273]) ).
fof(f72627,plain,
! [X0,X1] : add(inverse(add(X0,inverse(X0))),X1) = X1,
inference(superposition,[],[f2081,f72273]) ).
fof(f72673,plain,
! [X0,X1] : add(X0,inverse(X0)) = add(X1,inverse(X1)),
inference(forward_demodulation,[],[f72572,f72626]) ).
fof(f73519,plain,
! [X2,X0,X1] : add(X0,inverse(X0)) = add(inverse(X1),inverse(add(inverse(add(X0,inverse(X0))),inverse(add(X1,X2))))),
inference(superposition,[],[f2517,f72673]) ).
fof(f73648,plain,
! [X2,X0,X1] : add(X0,inverse(X0)) = add(inverse(X1),inverse(inverse(add(X1,X2)))),
inference(forward_demodulation,[],[f73519,f72627]) ).
fof(f74045,plain,
! [X2,X0,X1] : add(X0,inverse(X0)) = add(inverse(X1),add(X1,X2)),
inference(forward_demodulation,[],[f73648,f308]) ).
fof(f88808,plain,
! [X2,X3,X0,X1] : add(X1,X2) = inverse(add(inverse(add(X0,inverse(X0))),inverse(add(add(X1,X2),inverse(add(inverse(X1),X3)))))),
inference(superposition,[],[f2561,f74045]) ).
fof(f88861,plain,
! [X2,X3,X1] : add(X1,X2) = inverse(inverse(add(add(X1,X2),inverse(add(inverse(X1),X3))))),
inference(forward_demodulation,[],[f88808,f72627]) ).
fof(f89272,plain,
! [X2,X3,X1] : add(X1,X2) = add(add(X1,X2),inverse(add(inverse(X1),X3))),
inference(forward_demodulation,[],[f88861,f308]) ).
fof(f90028,plain,
! [X0,X1] : add(inverse(X0),X1) = add(X1,inverse(add(X0,X1))),
inference(superposition,[],[f757,f89272]) ).
fof(f90692,plain,
! [X2,X0,X1] : add(inverse(add(inverse(add(X2,X1)),X0)),X0) = add(inverse(inverse(add(X1,X0))),inverse(add(inverse(add(X2,X1)),X0))),
inference(superposition,[],[f90028,f59]) ).
fof(f91148,plain,
! [X2,X0,X1] : add(inverse(add(inverse(add(X2,X1)),X0)),X0) = add(add(X1,X0),inverse(add(inverse(add(X2,X1)),X0))),
inference(forward_demodulation,[],[f90692,f308]) ).
fof(f91341,plain,
! [X2,X0,X1] : add(X0,inverse(add(inverse(add(X2,X1)),X0))) = add(add(X1,X0),inverse(add(inverse(add(X2,X1)),X0))),
inference(forward_demodulation,[],[f91148,f2544]) ).
fof(f91472,plain,
! [X2,X0,X1] : add(inverse(inverse(add(X2,X1))),X0) = add(add(X1,X0),inverse(add(inverse(add(X2,X1)),X0))),
inference(forward_demodulation,[],[f91341,f90028]) ).
fof(f91566,plain,
! [X2,X0,X1] : add(add(X2,X1),X0) = add(add(X1,X0),inverse(add(inverse(add(X2,X1)),X0))),
inference(forward_demodulation,[],[f91472,f308]) ).
fof(f220910,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X2,X1),add(add(X0,X1),X2)),
inference(superposition,[],[f4444,f91566]) ).
fof(f221016,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X1,X2),add(add(X0,X1),X2)),
inference(superposition,[],[f1297,f91566]) ).
fof(f223374,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),X2),add(add(X0,X1),X2)),
inference(superposition,[],[f221016,f1366]) ).
fof(f223985,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X2,add(X0,X1)),add(inverse(add(inverse(X0),inverse(add(X0,X1)))),X2)),
inference(forward_demodulation,[],[f223374,f4068]) ).
fof(f224268,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X2,add(X0,X1)),add(inverse(inverse(X0)),X2)),
inference(forward_demodulation,[],[f223985,f2025]) ).
fof(f224378,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X2,add(X0,X1)),add(X0,X2)),
inference(forward_demodulation,[],[f224268,f308]) ).
fof(f224405,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X2,X0),add(X2,add(X0,X1))),
inference(forward_demodulation,[],[f224378,f4068]) ).
fof(f226516,plain,
! [X2,X0,X1] : add(add(add(X0,X1),X2),add(X1,X2)) = add(add(add(X1,X2),add(X0,X1)),add(add(X0,X1),X2)),
inference(superposition,[],[f224405,f221016]) ).
fof(f227035,plain,
! [X2,X0,X1] : add(add(add(X0,X1),X2),add(X1,X2)) = add(add(X2,add(X0,X1)),add(add(X1,X2),add(X0,X1))),
inference(forward_demodulation,[],[f226516,f4068]) ).
fof(f227389,plain,
! [X2,X0,X1] : add(add(X1,X2),add(X0,X1)) = add(add(add(X0,X1),X2),add(X1,X2)),
inference(forward_demodulation,[],[f227035,f221016]) ).
fof(f227536,plain,
! [X2,X0,X1] : add(add(X1,X2),add(X0,X1)) = add(add(X2,X1),add(add(X0,X1),X2)),
inference(forward_demodulation,[],[f227389,f4068]) ).
fof(f227598,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X1,X2),add(X0,X1)),
inference(forward_demodulation,[],[f227536,f220910]) ).
fof(f228004,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),X2),add(X0,X1)),
inference(superposition,[],[f227598,f1366]) ).
fof(f228085,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X2,X1),add(X0,X1)),
inference(superposition,[],[f4439,f227598]) ).
fof(f228245,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X0,X1),add(X1,X2)),
inference(superposition,[],[f2544,f227598]) ).
fof(f228519,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X1,X0),add(inverse(add(inverse(X0),inverse(add(X0,X1)))),X2)),
inference(forward_demodulation,[],[f228004,f4068]) ).
fof(f228812,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X1,X0),add(inverse(inverse(X0)),X2)),
inference(forward_demodulation,[],[f228519,f2025]) ).
fof(f228918,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X1,X0),add(X0,X2)),
inference(forward_demodulation,[],[f228812,f308]) ).
fof(f229288,plain,
! [X2,X0,X1] : add(add(X1,X2),inverse(add(X0,X1))) = add(add(X2,X1),add(inverse(X0),X1)),
inference(superposition,[],[f228918,f90028]) ).
fof(f229304,plain,
! [X2,X0,X1] : add(add(X2,X0),add(X0,X1)) = add(add(X0,X2),inverse(add(X0,inverse(add(X1,X0))))),
inference(superposition,[],[f228918,f9537]) ).
fof(f229937,plain,
! [X2,X0,X1] : add(add(X2,X0),add(X0,X1)) = add(add(X0,X2),inverse(add(inverse(X1),X0))),
inference(forward_demodulation,[],[f229304,f90028]) ).
fof(f229953,plain,
! [X2,X0,X1] : add(add(inverse(X0),X1),X2) = add(add(X1,X2),inverse(add(X0,X1))),
inference(forward_demodulation,[],[f229288,f228085]) ).
fof(f230299,plain,
! [X2,X0,X1] : add(add(X2,X0),X1) = add(add(X0,X2),inverse(add(inverse(X1),X0))),
inference(forward_demodulation,[],[f229937,f228245]) ).
fof(f230528,plain,
! [X2,X0,X1] : add(add(X2,X0),X1) = add(add(inverse(inverse(X1)),X0),X2),
inference(forward_demodulation,[],[f230299,f229953]) ).
fof(f230617,plain,
! [X2,X0,X1] : add(add(X1,X0),X2) = add(add(X2,X0),X1),
inference(forward_demodulation,[],[f230528,f308]) ).
fof(f231077,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(add(X2,inverse(add(inverse(X0),inverse(add(X0,X1))))),X1),
inference(superposition,[],[f230617,f1264]) ).
fof(f232291,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X1,add(X2,inverse(add(inverse(X0),inverse(add(X0,X1)))))),
inference(forward_demodulation,[],[f231077,f2544]) ).
fof(f232956,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X1,add(X2,inverse(inverse(X0)))),
inference(forward_demodulation,[],[f232291,f2025]) ).
fof(f233378,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X1,add(X2,X0)),
inference(forward_demodulation,[],[f232956,f308]) ).
fof(f234566,plain,
add(a,add(b,c)) != add(b,add(c,a)),
inference(superposition,[],[f2,f233378]) ).
fof(f234672,plain,
! [X2,X0,X1] : add(X0,add(X1,X2)) = add(X1,add(X2,X0)),
inference(superposition,[],[f2544,f233378]) ).
fof(f235317,plain,
$false,
inference(forward_subsumption_resolution,[],[f234566,f234672]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO073-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 % Computer : n008.cluster.edu
% 0.08/0.23 % Model : x86_64 x86_64
% 0.08/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.23 % Memory : 8046.5625MB
% 0.08/0.23 % OS : Linux 6.8.0-71-generic
% 0.08/0.23 % CPULimit : 300
% 0.08/0.23 % WCLimit : 300
% 0.08/0.23 % DateTime : Mon Sep 28 21:08:54 UTC 2026
% 0.08/0.23 % CPUTime :
% 0.08/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.29 Running first-order theorem proving
% 0.08/0.29 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
% 21.55/7.80 % (2654012)Detected a unit-equality problem, will run specialized UEQ schedule.
% 21.55/7.80 % (2654018)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3464403849:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_3000 on theBenchmark for (3000ds/130792Mi)
% 21.55/7.80 % (2654023)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3491019139:i=1187:sd=4:av=off:ss=axioms:sgt=32_3000 on theBenchmark for (3000ds/1187Mi)
% 21.55/7.80 % (2654021)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2359598355:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_3000 on theBenchmark for (3000ds/181Mi)
% 21.55/7.80 % (2654020)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=852864993:i=136:bd=preordered:ins=2:av=off_3000 on theBenchmark for (3000ds/136Mi)
% 21.55/7.80 % (2654022)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1969351237:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_3000 on theBenchmark for (3000ds/257Mi)
% 21.55/7.80 % (2654017)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=96645369:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_3000 on theBenchmark for (3000ds/138329Mi)
% 21.55/7.80 % (2654019)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=231063772:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_3000 on theBenchmark for (3000ds/130716Mi)
% 21.55/7.80 % (2654020)Instruction limit reached!
% 21.55/7.80 % (2654020)------------------------------
% 21.55/7.80 % (2654020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.55/7.80 % (2654020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.55/7.80 % (2654020)CaDiCaL version: 2.1.3
% 21.55/7.80 % (2654020)Termination reason: Instruction limit
% 21.55/7.80 % (2654020)Termination phase: Saturation
% 21.55/7.80 % (2654020)Time elapsed: 0.129 s
% 21.55/7.80 % (2654020)Peak memory usage: 89 MB
% 21.55/7.80 % (2654020)Instructions burned: 137 (million)
% 21.55/7.80 % (2654021)Instruction limit reached!
% 21.55/7.80 % (2654021)------------------------------
% 21.55/7.80 % (2654021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.55/7.80 % (2654021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.55/7.80 % (2654021)CaDiCaL version: 2.1.3
% 21.55/7.80 % (2654021)Termination reason: Instruction limit
% 21.55/7.80 % (2654021)Termination phase: Saturation
% 21.55/7.80 % (2654021)Time elapsed: 0.153 s
% 21.55/7.80 % (2654021)Peak memory usage: 89 MB
% 21.55/7.80 % (2654021)Instructions burned: 181 (million)
% 21.55/7.80 % (2654022)Instruction limit reached!
% 21.55/7.80 % (2654022)------------------------------
% 21.55/7.80 % (2654022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.55/7.80 % (2654022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.55/7.80 % (2654022)CaDiCaL version: 2.1.3
% 21.55/7.80 % (2654022)Termination reason: Instruction limit
% 21.55/7.80 % (2654022)Termination phase: Saturation
% 21.55/7.80 % (2654022)Time elapsed: 0.244 s
% 21.55/7.80 % (2654022)Peak memory usage: 90 MB
% 21.55/7.80 % (2654022)Instructions burned: 257 (million)
% 21.55/7.80 % (2654031)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=386120163:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 21.55/7.80 % (2654032)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=735638229:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 21.55/7.80 % (2654033)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2033081904:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 21.55/7.80 % (2654033)Instruction limit reached!
% 21.55/7.80 % (2654033)------------------------------
% 21.55/7.80 % (2654033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.55/7.80 % (2654033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.55/7.80 % (2654033)CaDiCaL version: 2.1.3
% 21.55/7.80 % (2654033)Termination reason: Instruction limit
% 21.55/7.80 % (2654033)Termination phase: Saturation
% 21.55/7.80 % (2654033)Time elapsed: 0.150 s
% 21.55/7.80 % (2654033)Peak memory usage: 105 MB
% 21.55/7.80 % (2654033)Instructions burned: 215 (million)
% 21.55/7.80 % (2654023)Instruction limit reached!
% 21.55/7.80 % (2654023)------------------------------
% 21.55/7.80 % (2654023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.55/7.80 % (2654023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.55/7.80 % (2654023)CaDiCaL version: 2.1.3
% 21.55/7.80 % (2654023)Termination reason: Instruction limit
% 21.55/7.80 % (2654023)Termination phase: Saturation
% 21.55/7.80 % (2654023)Time elapsed: 0.873 s
% 21.55/7.80 % (2654023)Peak memory usage: 98 MB
% 21.55/7.80 % (2654023)Instructions burned: 1189 (million)
% 21.55/7.80 % (2654038)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=598023626:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/317Mi)
% 21.55/7.80 % (2654039)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=3761074674:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/12125Mi)
% 21.55/7.80 % (2654038)Instruction limit reached!
% 21.55/7.80 % (2654038)------------------------------
% 21.55/7.80 % (2654038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.55/7.80 % (2654038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.55/7.80 % (2654038)CaDiCaL version: 2.1.3
% 21.55/7.80 % (2654038)Termination reason: Instruction limit
% 21.55/7.80 % (2654038)Termination phase: Saturation
% 21.55/7.80 % (2654038)Time elapsed: 0.317 s
% 21.55/7.80 % (2654038)Peak memory usage: 93 MB
% 21.55/7.80 % (2654038)Instructions burned: 318 (million)
% 21.55/7.80 % (2654043)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3795952927:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2985 on theBenchmark for (2985ds/2836Mi)
% 21.55/7.80 % (2654031)Instruction limit reached!
% 21.55/7.80 % (2654031)------------------------------
% 21.55/7.80 % (2654031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.55/7.80 % (2654031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.55/7.80 % (2654031)CaDiCaL version: 2.1.3
% 21.55/7.80 % (2654031)Termination reason: Instruction limit
% 21.55/7.80 % (2654031)Termination phase: Saturation
% 21.55/7.80 % (2654031)Time elapsed: 2.146 s
% 21.55/7.80 % (2654031)Peak memory usage: 139 MB
% 21.55/7.80 % (2654031)Instructions burned: 2051 (million)
% 21.55/7.80 % (2654045)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=76008641:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2972 on theBenchmark for (2972ds/14534Mi)
% 21.55/7.80 % (2654043)Instruction limit reached!
% 21.55/7.80 % (2654043)------------------------------
% 21.55/7.80 % (2654043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.55/7.80 % (2654043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.55/7.80 % (2654043)CaDiCaL version: 2.1.3
% 21.55/7.80 % (2654043)Termination reason: Instruction limit
% 21.55/7.80 % (2654043)Termination phase: Saturation
% 21.55/7.80 % (2654043)Time elapsed: 2.862 s
% 21.55/7.80 % (2654043)Peak memory usage: 131 MB
% 21.55/7.80 % (2654043)Instructions burned: 2838 (million)
% 21.55/7.80 % (2654050)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2722564133:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2954 on theBenchmark for (2954ds/11832Mi)
% 21.55/7.81 % (2654032)Instruction limit reached!
% 21.55/7.81 % (2654032)------------------------------
% 21.55/7.81 % (2654032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.55/7.81 % (2654032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.55/7.81 % (2654032)CaDiCaL version: 2.1.3
% 21.55/7.81 % (2654032)Termination reason: Instruction limit
% 21.55/7.81 % (2654032)Termination phase: Saturation
% 21.55/7.81 % (2654032)Time elapsed: 4.595 s
% 21.55/7.81 % (2654032)Peak memory usage: 161 MB
% 21.55/7.81 % (2654032)Instructions burned: 4948 (million)
% 21.55/7.81 % (2654054)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=4125893041:i=2279:fgj=on:bd=all_2947 on theBenchmark for (2947ds/2279Mi)
% 21.55/7.81 % (2654018)First to succeed.
% 21.55/7.81 % (2654018)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2654012"
% 21.55/7.81 % (2654018)Refutation found. Thanks to Tanya!
% 21.55/7.81 % SZS status Unsatisfiable for theBenchmark
% 21.55/7.81 % SZS output start Proof for theBenchmark
% See solution above
% 50.26/8.08 % (2654018)------------------------------
% 50.26/8.08 % (2654018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.26/8.08 % (2654018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.26/8.08 % (2654018)CaDiCaL version: 2.1.3
% 50.26/8.08 % (2654018)Termination reason: Refutation
% 50.26/8.08 % (2654018)Time elapsed: 6.528 s
% 50.26/8.08 % (2654018)Peak memory usage: 204 MB
% 50.26/8.08 % (2654018)Instructions burned: 12054 (million)
% 50.26/8.08 % (2654018)------------------------------
% 50.26/8.08 % (2654018)------------------------------
% 50.26/8.08 % (2654012)Success in time 6.987 s
% 50.26/8.08 % Vampire exiting
%------------------------------------------------------------------------------