%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP051-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 10:12:15 AM UTC 2026
% Result : Unsatisfiable 8.34s 2.09s
% Output : Refutation 9.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 2
% Syntax : Number of formulae : 89 ( 87 unt; 0 def)
% Number of atoms : 93 ( 92 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 11 ( 7 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 301 ( 301 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(inverse(X2),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f3,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != multiply(multiply(inverse(b2),b2),a2)
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(reorient_equations,[],[f2]) ).
fof(f4,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(X0,X3)))),multiply(X2,inverse(X3))) = multiply(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),
inference(superposition,[],[f1,f1]) ).
fof(f5,plain,
! [X2,X0,X1] : inverse(X2) = multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,X2)))),multiply(X1,inverse(X2))),inverse(X2))),inverse(multiply(inverse(X2),X2))),
inference(superposition,[],[f1,f1]) ).
fof(f37,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),X2))),X2)))),multiply(X0,inverse(X2))) = X1,
inference(superposition,[],[f1,f4]) ).
fof(f57,plain,
! [X2,X3,X0,X1] : inverse(multiply(X2,inverse(multiply(multiply(X0,inverse(multiply(inverse(X3),X3))),X3)))) = multiply(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(multiply(X2,inverse(X3))))),inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X3))))),
inference(superposition,[],[f1,f37]) ).
fof(f73,plain,
! [X2,X0,X1] : inverse(multiply(X0,inverse(multiply(multiply(multiply(X1,multiply(X0,inverse(X2))),inverse(multiply(inverse(X2),X2))),X2)))) = X1,
inference(superposition,[],[f1,f57]) ).
fof(f74,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(multiply(X0,inverse(X2))))) = multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X0,inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),X2))),X2)))),multiply(X0,inverse(X2)))))),multiply(X3,inverse(multiply(X0,inverse(X2))))),
inference(superposition,[],[f37,f57]) ).
fof(f86,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(multiply(X0,inverse(X2))))) = multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(multiply(X0,inverse(X2))))),
inference(forward_demodulation,[],[f74,f37]) ).
fof(f136,plain,
! [X2,X0,X1,X5] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X0)) = multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,X0)),
inference(superposition,[],[f86,f73]) ).
fof(f201,plain,
! [X0,X1,X4,X5] : multiply(inverse(multiply(X1,X0)),multiply(X1,X4)) = multiply(inverse(multiply(X5,X0)),multiply(X5,X4)),
inference(superposition,[],[f136,f73]) ).
fof(f202,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,X3)) = multiply(inverse(X0),multiply(multiply(inverse(multiply(X4,inverse(multiply(X0,X2)))),multiply(X4,inverse(X2))),X3)),
inference(superposition,[],[f136,f1]) ).
fof(f206,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(multiply(multiply(X0,multiply(X2,inverse(X3))),inverse(multiply(inverse(X3),X3))),X3)))),multiply(X1,X4)) = multiply(X0,multiply(X2,X4)),
inference(superposition,[],[f136,f73]) ).
fof(f362,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(X2,inverse(multiply(X3,multiply(X4,X1))))),multiply(X2,inverse(multiply(X4,X1)))),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))) = X3,
inference(superposition,[],[f1,f201]) ).
fof(f619,plain,
! [X2,X3,X0,X4] : multiply(X0,inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,X3)))) = multiply(X0,inverse(multiply(inverse(multiply(X4,X3)),multiply(X4,X3)))),
inference(superposition,[],[f362,f37]) ).
fof(f1130,plain,
! [X2,X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,inverse(multiply(inverse(X2),X2)))),
inference(superposition,[],[f202,f1]) ).
fof(f1262,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(superposition,[],[f1130,f1130]) ).
fof(f1546,plain,
! [X3,X0,X1,X4] : multiply(X1,inverse(multiply(inverse(X0),X0))) = multiply(X1,inverse(multiply(inverse(multiply(X4,X3)),multiply(X4,X3)))),
inference(superposition,[],[f619,f1262]) ).
fof(f1562,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))),inverse(multiply(inverse(X0),X0))) = X2,
inference(superposition,[],[f1,f1262]) ).
fof(f1572,plain,
! [X2,X0,X1] : inverse(X2) = multiply(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X0)))),multiply(X1,inverse(X2))),inverse(multiply(inverse(X0),X0))),
inference(superposition,[],[f1,f1262]) ).
fof(f1581,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X2),X3)),
inference(superposition,[],[f201,f1262]) ).
fof(f2435,plain,
! [X2,X3,X0,X1,X4] : inverse(X3) = multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,X2)))),multiply(X1,inverse(X2))),inverse(X3))),inverse(multiply(inverse(X4),X4))),
inference(superposition,[],[f1562,f1562]) ).
fof(f2529,plain,
! [X2,X3,X0,X1] : inverse(X3) = multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,X2)))),multiply(X1,inverse(X2))),inverse(X3))),inverse(multiply(inverse(X3),X3))),
inference(superposition,[],[f1,f1562]) ).
fof(f2855,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,X3))) = multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(inverse(multiply(X2,X3)),multiply(X2,X3)))))),multiply(X0,inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,X3))))),inverse(multiply(inverse(X4),X4)))),inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,X3))),multiply(inverse(multiply(X2,X3)),multiply(X2,X3))))),
inference(superposition,[],[f5,f1546]) ).
fof(f2886,plain,
! [X2,X3,X4] : inverse(multiply(inverse(X4),X4)) = inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,X3))),
inference(forward_demodulation,[],[f2855,f2435]) ).
fof(f2984,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X0)) = inverse(multiply(inverse(X1),X1)),
inference(superposition,[],[f2886,f2886]) ).
fof(f3828,plain,
! [X3,X0,X4] : multiply(multiply(inverse(multiply(X3,inverse(multiply(inverse(X4),X4)))),multiply(X3,X0)),inverse(multiply(inverse(X4),X4))) = X0,
inference(superposition,[],[f1572,f73]) ).
fof(f4067,plain,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))),multiply(inverse(X0),X0)),inverse(multiply(inverse(X2),X2))) = X1,
inference(superposition,[],[f3828,f1262]) ).
fof(f4148,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(X0,X3)))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))),multiply(X2,X0)),
inference(superposition,[],[f37,f3828]) ).
fof(f8728,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X1)))),multiply(X0,multiply(X2,inverse(multiply(inverse(X1),X1))))) = X2,
inference(superposition,[],[f37,f4148]) ).
fof(f8843,plain,
! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X1)),X1)))),multiply(X0,inverse(X1))),
inference(superposition,[],[f1262,f4148]) ).
fof(f9434,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X3),X3)),X3)))),multiply(X2,inverse(X3))) = multiply(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X1)),X1)))),multiply(X0,inverse(X1))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),
inference(superposition,[],[f4,f8843]) ).
fof(f9540,plain,
! [X2,X3,X0,X1] : inverse(multiply(X2,inverse(X3))) = inverse(multiply(X2,inverse(multiply(multiply(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X1)),X1)))),multiply(X0,inverse(X1))),inverse(multiply(inverse(X3),X3))),X3)))),
inference(superposition,[],[f73,f8843]) ).
fof(f9620,plain,
! [X2,X3,X0,X1] : multiply(X1,inverse(X2)) = multiply(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),X2)),X2)))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(X0),X0)),inverse(multiply(inverse(X3),X3))),
inference(superposition,[],[f3828,f8843]) ).
fof(f9623,plain,
! [X2,X1] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),X2)),X2))),
inference(forward_demodulation,[],[f9620,f4067]) ).
fof(f9633,plain,
! [X2,X3,X1] : inverse(multiply(X2,inverse(X3))) = inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X1),X1)),X3)))),
inference(forward_demodulation,[],[f9540,f1562]) ).
fof(f9635,plain,
! [X2,X3,X1] : inverse(multiply(inverse(X1),X1)) = multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X3),X3)),X3)))),multiply(X2,inverse(X3))),
inference(forward_demodulation,[],[f9434,f1562]) ).
fof(f9653,plain,
! [X2,X3,X1] : inverse(multiply(inverse(X1),X1)) = multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X3))),
inference(forward_demodulation,[],[f9635,f9633]) ).
fof(f9712,plain,
! [X2,X3,X0,X1] : multiply(X3,inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))) = multiply(X3,inverse(multiply(inverse(X1),X2))),
inference(superposition,[],[f9623,f1581]) ).
fof(f9813,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(X3),X3)),X3)) = multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(X3))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X3)),X3)),multiply(inverse(multiply(inverse(X3),X3)),X3)))),
inference(superposition,[],[f2529,f9623]) ).
fof(f9889,plain,
! [X3] : inverse(X3) = inverse(multiply(inverse(multiply(inverse(X3),X3)),X3)),
inference(forward_demodulation,[],[f9813,f2435]) ).
fof(f10097,plain,
! [X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(X0),multiply(inverse(multiply(inverse(X0),X0)),X0)),
inference(superposition,[],[f1262,f9889]) ).
fof(f10567,plain,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))),multiply(inverse(X0),X0)),inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(inverse(X1),X1)),X1),
inference(superposition,[],[f3828,f10097]) ).
fof(f10571,plain,
! [X1] : multiply(inverse(multiply(inverse(X1),X1)),X1) = X1,
inference(forward_demodulation,[],[f10567,f4067]) ).
fof(f10712,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(X0),X0)),X1) = X1,
inference(superposition,[],[f10571,f2984]) ).
fof(f10743,plain,
! [X2,X0,X1] : multiply(inverse(X0),X1) = multiply(inverse(multiply(X2,X0)),multiply(X2,X1)),
inference(superposition,[],[f1581,f10571]) ).
fof(f11059,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(X2,multiply(X0,inverse(multiply(inverse(X3),X3))))) = multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))),X1)),X0),
inference(superposition,[],[f10743,f8728]) ).
fof(f12687,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X2,inverse(multiply(X3,X4)))),multiply(X2,inverse(X4))) = multiply(multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1)))))),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1)))),multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1)))))),
inference(superposition,[],[f4,f9653]) ).
fof(f12691,plain,
! [X2,X3,X0,X1,X6,X4,X5] : multiply(inverse(X5),multiply(multiply(inverse(multiply(X6,inverse(multiply(X5,X3)))),multiply(X6,inverse(X3))),X4)) = multiply(inverse(multiply(X2,multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1))))),multiply(X2,X4)),
inference(superposition,[],[f202,f9653]) ).
fof(f12715,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X2,inverse(multiply(X3,X4)))),multiply(X2,inverse(X4))) = multiply(inverse(multiply(X5,multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1))))),multiply(X5,X3)),
inference(superposition,[],[f4148,f9653]) ).
fof(f12751,plain,
! [X2,X3,X0,X1,X4] : inverse(X3) = multiply(multiply(inverse(multiply(X2,multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1))))),multiply(X2,inverse(X3))),inverse(multiply(inverse(X4),X4))),
inference(superposition,[],[f1562,f9653]) ).
fof(f12953,plain,
! [X3,X0] : multiply(inverse(inverse(multiply(inverse(X0),X0))),X3) = X3,
inference(superposition,[],[f10712,f9653]) ).
fof(f12961,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X0),X0))) = X1,
inference(superposition,[],[f8728,f9653]) ).
fof(f13036,plain,
! [X2,X0,X1] : multiply(inverse(inverse(multiply(inverse(X2),X2))),multiply(X1,multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(inverse(X2),X2))))) = X1,
inference(forward_demodulation,[],[f12961,f11059]) ).
fof(f13179,plain,
! [X3,X0,X1,X4] : inverse(X3) = multiply(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1)))),inverse(X3)),inverse(multiply(inverse(X4),X4))),
inference(forward_demodulation,[],[f12751,f10743]) ).
fof(f13208,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,inverse(multiply(X3,X4)))),multiply(X2,inverse(X4))) = multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1)))),X3),
inference(forward_demodulation,[],[f12715,f10743]) ).
fof(f13221,plain,
! [X3,X0,X1,X6,X4,X5] : multiply(inverse(X5),multiply(multiply(inverse(multiply(X6,inverse(multiply(X5,X3)))),multiply(X6,inverse(X3))),X4)) = multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1)))),X4),
inference(forward_demodulation,[],[f12691,f10743]) ).
fof(f13225,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X2,inverse(multiply(X3,X4)))),multiply(X2,inverse(X4))) = multiply(multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1)))))),inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1))))),
inference(forward_demodulation,[],[f12687,f9712]) ).
fof(f13297,plain,
! [X2,X0,X1] : multiply(X1,multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(inverse(X2),X2)))) = X1,
inference(forward_demodulation,[],[f13036,f12953]) ).
fof(f13384,plain,
! [X3,X4] : inverse(X3) = multiply(inverse(X3),inverse(multiply(inverse(X4),X4))),
inference(forward_demodulation,[],[f13179,f10712]) ).
fof(f13401,plain,
! [X2,X3,X4] : multiply(inverse(multiply(X2,inverse(multiply(X3,X4)))),multiply(X2,inverse(X4))) = X3,
inference(forward_demodulation,[],[f13208,f10712]) ).
fof(f13411,plain,
! [X3,X6,X4,X5] : multiply(inverse(X5),multiply(multiply(inverse(multiply(X6,inverse(multiply(X5,X3)))),multiply(X6,inverse(X3))),X4)) = X4,
inference(forward_demodulation,[],[f13221,f10712]) ).
fof(f13414,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X2,inverse(multiply(X3,X4)))),multiply(X2,inverse(X4))) = multiply(multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1)))))),inverse(multiply(inverse(inverse(X1)),inverse(X1)))),
inference(forward_demodulation,[],[f13225,f9712]) ).
fof(f13443,plain,
! [X2,X1] : multiply(X1,inverse(multiply(inverse(X2),X2))) = X1,
inference(forward_demodulation,[],[f13297,f10712]) ).
fof(f13502,plain,
! [X3,X4] : multiply(inverse(inverse(multiply(X3,X4))),inverse(X4)) = X3,
inference(forward_demodulation,[],[f13401,f10743]) ).
fof(f13506,plain,
! [X3,X4,X5] : multiply(inverse(X5),multiply(multiply(inverse(inverse(multiply(X5,X3))),inverse(X3)),X4)) = X4,
inference(forward_demodulation,[],[f13411,f10743]) ).
fof(f13508,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,inverse(multiply(X3,X4)))),multiply(X2,inverse(X4))) = multiply(multiply(inverse(inverse(X3)),inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1))))),inverse(multiply(inverse(inverse(X1)),inverse(X1)))),
inference(forward_demodulation,[],[f13414,f10743]) ).
fof(f13538,plain,
! [X4,X5] : multiply(inverse(X5),multiply(X5,X4)) = X4,
inference(forward_demodulation,[],[f13506,f13502]) ).
fof(f13539,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,inverse(multiply(X3,X4)))),multiply(X2,inverse(X4))) = multiply(inverse(inverse(X3)),inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1))))),
inference(forward_demodulation,[],[f13508,f13443]) ).
fof(f13558,plain,
! [X2,X3,X4] : inverse(inverse(X3)) = multiply(inverse(multiply(X2,inverse(multiply(X3,X4)))),multiply(X2,inverse(X4))),
inference(forward_demodulation,[],[f13539,f13384]) ).
fof(f13570,plain,
! [X3,X4] : inverse(inverse(X3)) = multiply(inverse(inverse(multiply(X3,X4))),inverse(X4)),
inference(forward_demodulation,[],[f13558,f10743]) ).
fof(f13580,plain,
! [X3] : inverse(inverse(X3)) = X3,
inference(forward_demodulation,[],[f13570,f13502]) ).
fof(f13597,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(X2,X0)))),multiply(X1,inverse(X0))) = multiply(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,multiply(inverse(X0),X0))),inverse(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X0),X0))))),
inference(superposition,[],[f4,f13580]) ).
fof(f13625,plain,
! [X0,X1] : multiply(inverse(X1),X1) = multiply(X0,inverse(X0)),
inference(superposition,[],[f1262,f13580]) ).
fof(f13736,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(X2,X0)))),multiply(X1,inverse(X0))) = multiply(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))),
inference(forward_demodulation,[],[f13597,f13443]) ).
fof(f13777,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(X2,X0)))),multiply(X1,inverse(X0))) = multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,multiply(inverse(X0),X0))),
inference(forward_demodulation,[],[f13736,f13443]) ).
fof(f13803,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(X2,X0)))),multiply(X1,inverse(X0))) = multiply(inverse(inverse(X2)),multiply(inverse(X0),X0)),
inference(forward_demodulation,[],[f13777,f10743]) ).
fof(f13812,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(X2,X0)))),multiply(X1,inverse(X0))) = multiply(X2,multiply(inverse(X0),X0)),
inference(forward_demodulation,[],[f13803,f13580]) ).
fof(f13818,plain,
! [X2,X0] : multiply(X2,multiply(inverse(X0),X0)) = multiply(inverse(inverse(multiply(X2,X0))),inverse(X0)),
inference(forward_demodulation,[],[f13812,f10743]) ).
fof(f13821,plain,
! [X2,X0] : multiply(X2,multiply(inverse(X0),X0)) = X2,
inference(forward_demodulation,[],[f13818,f13502]) ).
fof(f13915,plain,
! [X0,X1] : multiply(multiply(inverse(X1),X1),X0) = X0,
inference(superposition,[],[f10712,f13538]) ).
fof(f14522,plain,
! [X2,X3,X0,X1,X4] : multiply(X2,multiply(X3,X4)) = multiply(inverse(multiply(X1,inverse(multiply(multiply(multiply(X2,multiply(inverse(X0),X0)),inverse(multiply(inverse(X3),X3))),X3)))),multiply(X1,X4)),
inference(superposition,[],[f206,f13625]) ).
fof(f14701,plain,
! [X2,X3,X0,X4] : multiply(X2,multiply(X3,X4)) = multiply(inverse(inverse(multiply(multiply(multiply(X2,multiply(inverse(X0),X0)),inverse(multiply(inverse(X3),X3))),X3))),X4),
inference(forward_demodulation,[],[f14522,f10743]) ).
fof(f14984,plain,
! [X2,X3,X0,X4] : multiply(X2,multiply(X3,X4)) = multiply(multiply(multiply(multiply(X2,multiply(inverse(X0),X0)),inverse(multiply(inverse(X3),X3))),X3),X4),
inference(forward_demodulation,[],[f14701,f13580]) ).
fof(f15148,plain,
! [X2,X3,X0,X4] : multiply(X2,multiply(X3,X4)) = multiply(multiply(multiply(X2,multiply(inverse(X0),X0)),X3),X4),
inference(forward_demodulation,[],[f14984,f13443]) ).
fof(f15236,plain,
! [X2,X3,X4] : multiply(X2,multiply(X3,X4)) = multiply(multiply(X2,X3),X4),
inference(forward_demodulation,[],[f15148,f13821]) ).
fof(f15292,plain,
a2 != multiply(multiply(inverse(b2),b2),a2),
inference(unit_resulting_resolution,[],[f3,f1262,f15236]) ).
fof(f15771,plain,
$false,
inference(forward_subsumption_resolution,[],[f15292,f13915]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP051-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n017.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 09:12:20 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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
% 8.34/2.08 % (2274800)Input is clausal, will run a generic CNF schedule.
% 8.34/2.08 % (2274806)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1708665696:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.34/2.08 % (2274811)dis-21_1_sil=8000:lcm=predicate:random_seed=75475735:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 8.34/2.08 % (2274810)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3763351261:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.34/2.08 % (2274808)lrs+10_1_sil=8000:sp=occurrence:random_seed=750508374:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.34/2.08 % (2274807)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1611550157:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.34/2.08 % (2274805)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=4197443010:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.34/2.08 % (2274809)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3016384588:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.34/2.08 % (2274811)Refutation not found, incomplete strategy
% 8.34/2.08 % (2274811)------------------------------
% 8.34/2.08 % (2274811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.08 % (2274811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.08 % (2274811)CaDiCaL version: 2.1.3
% 8.34/2.08 % (2274811)Termination reason: Refutation not found, incomplete strategy
% 8.34/2.08 % (2274811)Time elapsed: 0.001 s
% 8.34/2.08 % (2274811)Peak memory usage: 88 MB
% 8.34/2.08 % (2274808)Instruction limit reached!
% 8.34/2.08 % (2274808)------------------------------
% 8.34/2.08 % (2274808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.08 % (2274808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.08 % (2274808)CaDiCaL version: 2.1.3
% 8.34/2.08 % (2274808)Termination reason: Instruction limit
% 8.34/2.08 % (2274808)Termination phase: Saturation
% 8.34/2.08 % (2274808)Time elapsed: 0.064 s
% 8.34/2.08 % (2274808)Peak memory usage: 89 MB
% 8.34/2.08 % (2274808)Instructions burned: 107 (million)
% 8.34/2.08 % (2274809)Instruction limit reached!
% 8.34/2.08 % (2274809)------------------------------
% 8.34/2.08 % (2274809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.08 % (2274809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.08 % (2274809)CaDiCaL version: 2.1.3
% 8.34/2.08 % (2274809)Termination reason: Instruction limit
% 8.34/2.08 % (2274809)Termination phase: Saturation
% 8.34/2.08 % (2274809)Time elapsed: 0.071 s
% 8.34/2.08 % (2274809)Peak memory usage: 89 MB
% 8.34/2.08 % (2274809)Instructions burned: 115 (million)
% 8.34/2.08 % (2274810)Instruction limit reached!
% 8.34/2.08 % (2274810)------------------------------
% 8.34/2.08 % (2274810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.08 % (2274810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.09 % (2274810)CaDiCaL version: 2.1.3
% 8.34/2.09 % (2274810)Termination reason: Instruction limit
% 8.34/2.09 % (2274810)Termination phase: Saturation
% 8.34/2.09 % (2274810)Time elapsed: 0.097 s
% 8.34/2.09 % (2274810)Peak memory usage: 89 MB
% 8.34/2.09 % (2274810)Instructions burned: 181 (million)
% 8.34/2.09 % (2274819)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3899535830:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 8.34/2.09 % (2274819)Refutation not found, incomplete strategy
% 8.34/2.09 % (2274819)------------------------------
% 8.34/2.09 % (2274819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.09 % (2274819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.09 % (2274819)CaDiCaL version: 2.1.3
% 8.34/2.09 % (2274819)Termination reason: Refutation not found, incomplete strategy
% 8.34/2.09 % (2274819)Time elapsed: 0.001 s
% 8.34/2.09 % (2274819)Peak memory usage: 88 MB
% 8.34/2.09 % (2274820)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2774412700:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 8.34/2.09 % (2274820)Refutation not found, incomplete strategy
% 8.34/2.09 % (2274820)------------------------------
% 8.34/2.09 % (2274820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.09 % (2274820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.09 % (2274820)CaDiCaL version: 2.1.3
% 8.34/2.09 % (2274820)Termination reason: Refutation not found, incomplete strategy
% 8.34/2.09 % (2274820)Time elapsed: 0.001 s
% 8.34/2.09 % (2274820)Peak memory usage: 88 MB
% 8.34/2.09 % (2274821)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=970860396:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 8.34/2.09 % (2274821)Refutation not found, incomplete strategy
% 8.34/2.09 % (2274821)------------------------------
% 8.34/2.09 % (2274821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.09 % (2274821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.09 % (2274821)CaDiCaL version: 2.1.3
% 8.34/2.09 % (2274821)Termination reason: Refutation not found, incomplete strategy
% 8.34/2.09 % (2274821)Time elapsed: 0.001 s
% 8.34/2.09 % (2274821)Peak memory usage: 88 MB
% 8.34/2.09 % (2274811)------------------------------
% 8.34/2.09 % (2274811)------------------------------
% 8.34/2.09 % (2274825)lrs+10_64_to=lpo:sil=8000:random_seed=2498306868:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 8.34/2.09 % (2274819)------------------------------
% 8.34/2.09 % (2274819)------------------------------
% 8.34/2.09 % (2274825)Instruction limit reached!
% 8.34/2.09 % (2274825)------------------------------
% 8.34/2.09 % (2274825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.09 % (2274825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.09 % (2274825)CaDiCaL version: 2.1.3
% 8.34/2.09 % (2274825)Termination reason: Instruction limit
% 8.34/2.09 % (2274825)Termination phase: Saturation
% 8.34/2.09 % (2274825)Time elapsed: 0.073 s
% 8.34/2.09 % (2274825)Peak memory usage: 89 MB
% 8.34/2.09 % (2274825)Instructions burned: 127 (million)
% 8.34/2.09 % (2274820)------------------------------
% 8.34/2.09 % (2274820)------------------------------
% 8.34/2.09 % (2274821)------------------------------
% 8.34/2.09 % (2274821)------------------------------
% 8.34/2.09 % (2274828)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1748309532:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 8.34/2.09 % (2274827)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=582342022:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 8.34/2.09 % (2274829)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1702159351:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 8.34/2.09 % (2274830)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3381857708:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 8.34/2.09 % (2274828)Instruction limit reached!
% 8.34/2.09 % (2274828)------------------------------
% 8.34/2.09 % (2274828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.09 % (2274828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.09 % (2274828)CaDiCaL version: 2.1.3
% 8.34/2.09 % (2274828)Termination reason: Instruction limit
% 8.34/2.09 % (2274828)Termination phase: Saturation
% 8.34/2.09 % (2274828)Time elapsed: 0.091 s
% 8.34/2.09 % (2274828)Peak memory usage: 90 MB
% 8.34/2.09 % (2274828)Instructions burned: 159 (million)
% 8.34/2.09 % (2274830)Instruction limit reached!
% 8.34/2.09 % (2274830)------------------------------
% 8.34/2.09 % (2274830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.09 % (2274830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.09 % (2274830)CaDiCaL version: 2.1.3
% 8.34/2.09 % (2274830)Termination reason: Instruction limit
% 8.34/2.09 % (2274830)Termination phase: Saturation
% 8.34/2.09 % (2274830)Time elapsed: 0.063 s
% 8.34/2.09 % (2274830)Peak memory usage: 90 MB
% 8.34/2.09 % (2274830)Instructions burned: 108 (million)
% 8.34/2.09 % (2274827)Instruction limit reached!
% 8.34/2.09 % (2274827)------------------------------
% 8.34/2.09 % (2274827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.09 % (2274827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.09 % (2274827)CaDiCaL version: 2.1.3
% 8.34/2.09 % (2274827)Termination reason: Instruction limit
% 8.34/2.09 % (2274827)Termination phase: Saturation
% 8.34/2.09 % (2274827)Time elapsed: 0.111 s
% 8.34/2.09 % (2274827)Peak memory usage: 90 MB
% 8.34/2.09 % (2274827)Instructions burned: 195 (million)
% 8.34/2.09 % (2274835)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3720726129:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 8.34/2.09 % (2274835)Refutation not found, incomplete strategy
% 8.34/2.09 % (2274835)------------------------------
% 8.34/2.09 % (2274835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.09 % (2274835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.09 % (2274835)CaDiCaL version: 2.1.3
% 8.34/2.09 % (2274835)Termination reason: Refutation not found, incomplete strategy
% 8.34/2.09 % (2274835)Time elapsed: 0.001 s
% 8.34/2.09 % (2274835)Peak memory usage: 88 MB
% 8.34/2.09 % (2274836)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=519559404:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 8.34/2.09 % (2274837)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=402280365:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 8.34/2.09 % (2274806)First to succeed.
% 8.34/2.09 % (2274806)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2274800"
% 8.34/2.09 % (2274836)Instruction limit reached!
% 8.34/2.09 % (2274836)------------------------------
% 8.34/2.09 % (2274836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.34/2.09 % (2274836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.34/2.09 % (2274836)CaDiCaL version: 2.1.3
% 8.34/2.09 % (2274836)Termination reason: Instruction limit
% 8.34/2.09 % (2274836)Termination phase: Saturation
% 8.34/2.09 % (2274836)Time elapsed: 0.136 s
% 8.34/2.09 % (2274836)Peak memory usage: 91 MB
% 8.34/2.09 % (2274836)Instructions burned: 243 (million)
% 8.34/2.09 % (2274835)------------------------------
% 8.34/2.09 % (2274835)------------------------------
% 8.34/2.09 % (2274841)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2237652904:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 8.34/2.09 % (2274806)Refutation found. Thanks to Tanya!
% 8.34/2.09 % SZS status Unsatisfiable for theBenchmark
% 8.34/2.09 % SZS output start Proof for theBenchmark
% See solution above
% 9.24/2.28 % (2274806)------------------------------
% 9.24/2.28 % (2274806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.24/2.28 % (2274806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.24/2.28 % (2274806)CaDiCaL version: 2.1.3
% 9.24/2.28 % (2274806)Termination reason: Refutation
% 9.24/2.28 % (2274806)Time elapsed: 0.950 s
% 9.24/2.28 % (2274806)Peak memory usage: 147 MB
% 9.24/2.28 % (2274806)Instructions burned: 2891 (million)
% 9.24/2.28 % (2274806)------------------------------
% 9.24/2.28 % (2274806)------------------------------
% 9.24/2.28 % (2274800)Success in time 1.226 s
% 9.24/2.28 % Vampire exiting
%------------------------------------------------------------------------------