%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP470-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 10:14:05 AM UTC 2026
% Result : Unsatisfiable 9.74s 2.42s
% Output : Refutation 11.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 7
% Syntax : Number of formulae : 200 ( 200 unt; 4 def)
% Number of atoms : 200 ( 199 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 231 ( 231 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X2,X3,X0,X1] : divide(inverse(divide(X0,divide(X1,divide(X2,X3)))),divide(divide(X3,X2),X0)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
! [X0,X1] : multiply(X0,X1) = divide(X0,inverse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiply) ).
fof(f3,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_2) ).
fof(f4,plain,
a2 != multiply(multiply(inverse(b2),b2),a2),
inference(reorient_equations,[],[f3]) ).
fof(f5,plain,
a2 != divide(divide(inverse(b2),inverse(b2)),inverse(a2)),
inference(definition_unfolding,[],[f4,f2,f2]) ).
fof(f6,definition,
sF0 = inverse(b2),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f7,plain,
inverse(b2) = sF0,
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF1 = divide(sF0,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f9,plain,
divide(sF0,sF0) = sF1,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF2 = inverse(a2),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f11,plain,
inverse(a2) = sF2,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF3 = divide(sF1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f13,plain,
divide(sF1,sF2) = sF3,
inference(reorient_equations,[],[f12]) ).
fof(f14,plain,
a2 != sF3,
inference(definition_folding,[],[f5,f13,f11,f9,f7,f7]) ).
fof(f15,plain,
! [X2,X3,X0,X1,X4,X5] : divide(inverse(divide(X1,divide(X2,X0))),divide(divide(divide(divide(X5,X4),X3),inverse(divide(X3,divide(X0,divide(X4,X5))))),X1)) = X2,
inference(superposition,[],[f1,f1]) ).
fof(f16,plain,
! [X2,X3,X0,X1,X4] : inverse(divide(X2,divide(X0,divide(X3,X4)))) = divide(inverse(divide(X1,X0)),divide(divide(X2,divide(X4,X3)),X1)),
inference(superposition,[],[f1,f1]) ).
fof(f17,plain,
! [X2,X3,X0,X1,X4] : divide(X4,X3) = divide(inverse(X0),divide(divide(X2,X1),inverse(divide(divide(X1,X2),divide(X0,divide(X3,X4)))))),
inference(superposition,[],[f1,f1]) ).
fof(f20,plain,
! [X0,X1] : divide(inverse(divide(X0,divide(X1,sF1))),divide(sF1,X0)) = X1,
inference(superposition,[],[f1,f9]) ).
fof(f22,plain,
! [X0,X1] : divide(inverse(divide(X0,divide(X1,sF3))),divide(divide(sF2,sF1),X0)) = X1,
inference(superposition,[],[f1,f13]) ).
fof(f25,plain,
! [X0] : divide(inverse(divide(sF2,divide(X0,sF1))),sF3) = X0,
inference(superposition,[],[f20,f13]) ).
fof(f26,plain,
! [X2,X0,X1] : inverse(divide(X2,divide(X0,sF1))) = divide(inverse(divide(X1,X0)),divide(divide(X2,sF1),X1)),
inference(superposition,[],[f1,f20]) ).
fof(f27,plain,
! [X2,X0,X1] : sF1 = divide(inverse(X0),divide(divide(X2,X1),inverse(divide(divide(X1,X2),divide(X0,sF1))))),
inference(superposition,[],[f1,f20]) ).
fof(f30,plain,
! [X1] : inverse(divide(sF2,divide(divide(X1,sF3),sF1))) = X1,
inference(backward_demodulation,[],[f22,f26]) ).
fof(f57,plain,
! [X2,X0,X1] : divide(inverse(divide(X1,divide(X2,X0))),divide(divide(sF3,inverse(divide(sF2,divide(X0,sF1)))),X1)) = X2,
inference(superposition,[],[f1,f25]) ).
fof(f64,plain,
! [X2,X3,X0,X1] : sF0 = divide(inverse(divide(X0,sF1)),divide(divide(divide(divide(X1,X2),X3),inverse(divide(X3,divide(sF0,divide(X2,X1))))),X0)),
inference(superposition,[],[f15,f9]) ).
fof(f65,plain,
! [X2,X3,X0,X1] : sF1 = divide(inverse(divide(X0,sF3)),divide(divide(divide(divide(X1,X2),X3),inverse(divide(X3,divide(sF2,divide(X2,X1))))),X0)),
inference(superposition,[],[f15,f13]) ).
fof(f95,plain,
! [X2,X3,X0,X1,X6,X4,X5] : divide(divide(divide(X4,X5),X6),inverse(divide(X6,divide(X3,divide(X5,X4))))) = divide(inverse(X0),divide(divide(X2,X1),inverse(divide(divide(X1,X2),divide(X0,X3))))),
inference(superposition,[],[f1,f15]) ).
fof(f127,plain,
! [X2,X3,X0,X1] : divide(sF3,inverse(divide(sF2,divide(X0,sF1)))) = divide(inverse(X1),divide(divide(X2,X3),inverse(divide(divide(X3,X2),divide(X1,X0))))),
inference(superposition,[],[f17,f25]) ).
fof(f151,plain,
! [X3,X6,X4,X5] : divide(sF3,inverse(divide(sF2,divide(X3,sF1)))) = divide(divide(divide(X4,X5),X6),inverse(divide(X6,divide(X3,divide(X5,X4))))),
inference(backward_demodulation,[],[f95,f127]) ).
fof(f152,plain,
! [X3,X4] : divide(X4,X3) = divide(sF3,inverse(divide(sF2,divide(divide(X3,X4),sF1)))),
inference(backward_demodulation,[],[f17,f127]) ).
fof(f153,plain,
sF1 = divide(sF3,inverse(divide(sF2,divide(sF1,sF1)))),
inference(backward_demodulation,[],[f27,f127]) ).
fof(f190,plain,
! [X0] : sF0 = divide(inverse(divide(X0,sF1)),divide(divide(sF3,inverse(divide(sF2,divide(sF0,sF1)))),X0)),
inference(backward_demodulation,[],[f64,f151]) ).
fof(f192,plain,
! [X0] : sF1 = divide(inverse(divide(X0,sF3)),divide(divide(sF3,inverse(divide(sF2,divide(sF2,sF1)))),X0)),
inference(backward_demodulation,[],[f65,f151]) ).
fof(f317,plain,
! [X0,X1] : inverse(divide(X0,divide(divide(X1,divide(sF1,X0)),sF1))) = X1,
inference(superposition,[],[f1,f26]) ).
fof(f334,plain,
! [X0,X1] : inverse(inverse(divide(X0,divide(X1,divide(inverse(divide(sF1,X1)),sF1))))) = X0,
inference(superposition,[],[f317,f16]) ).
fof(f448,plain,
! [X2,X3,X0,X1] : inverse(divide(divide(inverse(divide(sF1,divide(X0,divide(X3,X2)))),sF1),X1)) = inverse(inverse(inverse(divide(X0,divide(X1,divide(X2,X3)))))),
inference(superposition,[],[f334,f16]) ).
fof(f449,plain,
! [X0,X1] : inverse(divide(divide(inverse(divide(sF1,divide(X0,sF1))),sF1),X1)) = inverse(inverse(inverse(divide(X0,divide(X1,sF1))))),
inference(superposition,[],[f334,f26]) ).
fof(f461,plain,
divide(sF3,inverse(divide(sF2,divide(sF2,sF1)))) = divide(inverse(sF1),divide(sF1,inverse(divide(sF1,sF3)))),
inference(superposition,[],[f20,f192]) ).
fof(f527,plain,
! [X0,X1] : divide(sF3,inverse(divide(sF2,divide(divide(sF3,inverse(divide(sF2,divide(sF0,sF1)))),sF1)))) = divide(divide(divide(X0,X1),inverse(divide(divide(X1,X0),sF1))),inverse(sF0)),
inference(superposition,[],[f151,f190]) ).
fof(f555,plain,
! [X0,X1] : divide(inverse(divide(sF2,divide(sF0,sF1))),sF3) = divide(divide(divide(X0,X1),inverse(divide(divide(X1,X0),sF1))),inverse(sF0)),
inference(forward_demodulation,[],[f527,f152]) ).
fof(f588,plain,
! [X0,X1] : sF0 = divide(divide(divide(X0,X1),inverse(divide(divide(X1,X0),sF1))),inverse(sF0)),
inference(forward_demodulation,[],[f555,f25]) ).
fof(f703,plain,
sF0 = divide(divide(sF1,inverse(divide(sF1,sF1))),inverse(sF0)),
inference(superposition,[],[f588,f9]) ).
fof(f850,plain,
! [X0] : divide(inverse(divide(inverse(sF0),divide(X0,divide(inverse(divide(sF1,sF1)),sF1)))),sF0) = X0,
inference(superposition,[],[f1,f703]) ).
fof(f922,plain,
! [X2,X0,X1] : divide(divide(X1,X2),inverse(divide(divide(X2,X1),sF1))) = divide(inverse(divide(X0,sF0)),divide(divide(sF3,inverse(divide(sF2,divide(inverse(sF0),sF1)))),X0)),
inference(superposition,[],[f57,f588]) ).
fof(f924,plain,
! [X0] : divide(sF1,inverse(divide(sF1,sF1))) = divide(inverse(divide(X0,sF0)),divide(divide(sF3,inverse(divide(sF2,divide(inverse(sF0),sF1)))),X0)),
inference(superposition,[],[f57,f703]) ).
fof(f962,plain,
! [X2,X3,X0,X1] : divide(sF3,inverse(divide(sF2,divide(divide(sF3,inverse(divide(sF2,divide(X1,sF1)))),sF1)))) = divide(divide(divide(X2,X3),inverse(divide(divide(X3,X2),divide(X0,X1)))),inverse(X0)),
inference(superposition,[],[f151,f57]) ).
fof(f1002,plain,
! [X2,X3,X0,X1] : divide(divide(divide(X2,X3),inverse(divide(divide(X3,X2),divide(X0,X1)))),inverse(X0)) = divide(inverse(divide(sF2,divide(X1,sF1))),sF3),
inference(forward_demodulation,[],[f962,f152]) ).
fof(f1028,plain,
! [X2,X1] : divide(sF1,inverse(divide(sF1,sF1))) = divide(divide(X1,X2),inverse(divide(divide(X2,X1),sF1))),
inference(forward_demodulation,[],[f922,f924]) ).
fof(f1029,plain,
! [X2,X3,X0,X1] : divide(divide(divide(X2,X3),inverse(divide(divide(X3,X2),divide(X0,X1)))),inverse(X0)) = X1,
inference(forward_demodulation,[],[f1002,f25]) ).
fof(f1082,plain,
! [X0,X1] : divide(divide(sF1,inverse(divide(sF1,divide(X0,X1)))),inverse(X0)) = X1,
inference(superposition,[],[f1029,f9]) ).
fof(f1104,plain,
! [X0,X1] : inverse(divide(sF2,divide(sF1,sF1))) = divide(divide(divide(X0,X1),inverse(divide(divide(X1,X0),sF1))),inverse(sF3)),
inference(superposition,[],[f1029,f153]) ).
fof(f1142,plain,
inverse(divide(sF2,divide(sF1,sF1))) = divide(divide(sF1,inverse(divide(sF1,sF1))),inverse(sF3)),
inference(forward_demodulation,[],[f1104,f1028]) ).
fof(f1208,plain,
! [X0] : divide(divide(sF1,inverse(divide(sF1,divide(a2,X0)))),sF2) = X0,
inference(superposition,[],[f1082,f11]) ).
fof(f1219,plain,
! [X2,X0,X1] : divide(sF1,inverse(divide(sF1,divide(X2,X0)))) = divide(inverse(divide(X1,X0)),divide(divide(sF3,inverse(divide(sF2,divide(inverse(X2),sF1)))),X1)),
inference(superposition,[],[f57,f1082]) ).
fof(f1287,plain,
! [X0,X1] : divide(sF1,inverse(divide(sF1,divide(a2,X0)))) = divide(inverse(divide(X1,X0)),divide(divide(sF3,inverse(divide(sF2,divide(sF2,sF1)))),X1)),
inference(superposition,[],[f57,f1208]) ).
fof(f1300,plain,
sF1 = divide(sF1,inverse(divide(sF1,divide(a2,sF3)))),
inference(backward_demodulation,[],[f192,f1287]) ).
fof(f1311,plain,
! [X0] : inverse(divide(inverse(divide(sF1,divide(a2,sF3))),divide(divide(X0,sF1),sF1))) = X0,
inference(superposition,[],[f317,f1300]) ).
fof(f1320,plain,
! [X0] : sF1 = divide(inverse(divide(X0,sF1)),divide(divide(sF3,inverse(divide(sF2,divide(inverse(divide(sF1,divide(a2,sF3))),sF1)))),X0)),
inference(superposition,[],[f57,f1300]) ).
fof(f1323,plain,
divide(sF3,inverse(divide(sF2,divide(sF1,sF1)))) = divide(inverse(divide(sF1,divide(a2,sF3))),sF1),
inference(superposition,[],[f152,f1300]) ).
fof(f1326,plain,
inverse(divide(sF1,divide(a2,sF3))) = divide(divide(sF1,inverse(divide(sF1,sF1))),inverse(sF1)),
inference(superposition,[],[f1082,f1300]) ).
fof(f1328,plain,
sF1 = divide(inverse(divide(sF1,divide(a2,sF3))),sF1),
inference(forward_demodulation,[],[f1323,f153]) ).
fof(f1329,plain,
sF1 = divide(sF1,inverse(divide(sF1,divide(divide(sF1,divide(a2,sF3)),sF1)))),
inference(forward_demodulation,[],[f1320,f1219]) ).
fof(f1332,plain,
! [X0] : inverse(inverse(divide(X0,divide(divide(a2,sF3),sF1)))) = X0,
inference(forward_demodulation,[],[f1311,f26]) ).
fof(f1344,plain,
! [X0] : inverse(inverse(X0)) = inverse(divide(sF1,divide(X0,divide(sF3,a2)))),
inference(superposition,[],[f1332,f1]) ).
fof(f1351,plain,
inverse(divide(sF1,divide(a2,sF3))) = divide(inverse(divide(sF2,sF1)),sF3),
inference(superposition,[],[f25,f1328]) ).
fof(f1352,plain,
! [X0] : inverse(divide(sF1,divide(a2,sF3))) = divide(inverse(divide(X0,sF1)),divide(sF1,X0)),
inference(superposition,[],[f20,f1328]) ).
fof(f1378,plain,
sF1 = divide(sF1,divide(inverse(divide(sF2,sF1)),sF3)),
inference(backward_demodulation,[],[f1300,f1351]) ).
fof(f1381,plain,
divide(divide(sF1,inverse(divide(sF1,sF1))),inverse(sF1)) = divide(inverse(divide(sF2,sF1)),sF3),
inference(backward_demodulation,[],[f1326,f1351]) ).
fof(f1382,plain,
sF1 = divide(divide(inverse(divide(sF2,sF1)),sF3),sF1),
inference(backward_demodulation,[],[f1328,f1351]) ).
fof(f1383,plain,
! [X0] : divide(inverse(divide(sF2,sF1)),sF3) = divide(inverse(divide(X0,sF1)),divide(sF1,X0)),
inference(backward_demodulation,[],[f1352,f1351]) ).
fof(f1429,plain,
! [X0] : divide(sF3,inverse(divide(sF2,divide(X0,sF1)))) = divide(divide(divide(a2,sF3),sF1),inverse(inverse(X0))),
inference(superposition,[],[f151,f1344]) ).
fof(f1430,plain,
! [X0] : divide(inverse(inverse(X0)),divide(divide(a2,sF3),sF1)) = X0,
inference(superposition,[],[f1,f1344]) ).
fof(f1439,plain,
! [X0] : divide(sF2,divide(divide(X0,sF3),sF1)) = divide(inverse(X0),divide(divide(a2,sF3),sF1)),
inference(superposition,[],[f1430,f30]) ).
fof(f1443,plain,
! [X0] : divide(sF1,divide(X0,divide(sF3,a2))) = divide(inverse(inverse(inverse(X0))),divide(divide(a2,sF3),sF1)),
inference(superposition,[],[f1430,f1344]) ).
fof(f1448,plain,
a2 = divide(inverse(sF2),divide(divide(a2,sF3),sF1)),
inference(superposition,[],[f1430,f11]) ).
fof(f1452,plain,
! [X0] : divide(a2,sF3) = divide(inverse(X0),divide(sF1,inverse(inverse(X0)))),
inference(superposition,[],[f20,f1430]) ).
fof(f1471,plain,
! [X0] : divide(divide(a2,sF3),sF1) = divide(divide(sF1,inverse(divide(sF1,X0))),inverse(inverse(inverse(X0)))),
inference(superposition,[],[f1082,f1430]) ).
fof(f1495,plain,
! [X0] : inverse(X0) = divide(sF1,divide(X0,divide(sF3,a2))),
inference(forward_demodulation,[],[f1443,f1430]) ).
fof(f1506,plain,
! [X0] : divide(sF2,divide(divide(inverse(X0),sF3),sF1)) = X0,
inference(backward_demodulation,[],[f1430,f1439]) ).
fof(f1508,plain,
a2 = divide(sF2,divide(divide(sF2,sF3),sF1)),
inference(backward_demodulation,[],[f1448,f1439]) ).
fof(f1674,plain,
! [X0] : divide(a2,sF3) = divide(X0,divide(sF1,inverse(X0))),
inference(superposition,[],[f1452,f30]) ).
fof(f1713,plain,
! [X0,X1] : divide(sF3,inverse(divide(sF2,divide(X0,sF1)))) = divide(divide(divide(inverse(X0),sF1),X1),inverse(divide(X1,divide(a2,sF3)))),
inference(superposition,[],[f151,f1674]) ).
fof(f1724,plain,
! [X0] : divide(sF3,inverse(divide(sF2,divide(divide(a2,sF3),sF1)))) = divide(divide(sF1,inverse(X0)),X0),
inference(superposition,[],[f152,f1674]) ).
fof(f1738,plain,
! [X0] : divide(sF3,a2) = divide(divide(sF1,inverse(X0)),X0),
inference(forward_demodulation,[],[f1724,f152]) ).
fof(f1773,plain,
! [X2,X0,X1] : divide(sF3,inverse(divide(sF2,divide(divide(sF1,inverse(divide(X0,X1))),sF1)))) = divide(divide(divide(X1,X0),X2),inverse(divide(X2,divide(sF3,a2)))),
inference(superposition,[],[f151,f1738]) ).
fof(f1781,plain,
divide(sF1,divide(sF3,a2)) = inverse(divide(sF1,inverse(divide(sF3,a2)))),
inference(superposition,[],[f1495,f1738]) ).
fof(f1789,plain,
! [X2,X0,X1] : divide(inverse(divide(X0,X1)),sF1) = divide(divide(divide(X1,X0),X2),inverse(divide(X2,divide(sF3,a2)))),
inference(forward_demodulation,[],[f1773,f152]) ).
fof(f1899,plain,
! [X0,X1] : divide(inverse(divide(X0,divide(X1,sF1))),divide(divide(divide(inverse(divide(sF2,sF1)),sF3),sF1),X0)) = X1,
inference(superposition,[],[f1,f1378]) ).
fof(f1916,plain,
! [X1] : inverse(divide(divide(inverse(divide(sF2,sF1)),sF3),divide(divide(X1,sF1),sF1))) = X1,
inference(forward_demodulation,[],[f1899,f26]) ).
fof(f1927,plain,
! [X0] : divide(sF2,divide(divide(X0,sF3),sF1)) = divide(divide(inverse(divide(sF2,sF1)),sF3),divide(divide(X0,sF1),sF1)),
inference(superposition,[],[f1506,f1916]) ).
fof(f1939,plain,
divide(inverse(divide(sF2,sF1)),sF3) = divide(inverse(divide(divide(inverse(divide(sF2,sF1)),sF3),sF1)),sF1),
inference(superposition,[],[f1383,f1378]) ).
fof(f1957,plain,
! [X0] : divide(sF3,inverse(divide(sF2,divide(divide(inverse(divide(sF2,sF1)),sF3),sF1)))) = divide(divide(sF1,X0),inverse(divide(X0,sF1))),
inference(superposition,[],[f152,f1383]) ).
fof(f1958,plain,
! [X0] : divide(sF1,X0) = divide(divide(sF1,inverse(divide(sF1,divide(inverse(divide(sF2,sF1)),sF3)))),inverse(inverse(divide(X0,sF1)))),
inference(superposition,[],[f1082,f1383]) ).
fof(f1959,plain,
! [X0] : divide(sF1,X0) = divide(divide(sF1,inverse(sF1)),inverse(inverse(divide(X0,sF1)))),
inference(forward_demodulation,[],[f1958,f1378]) ).
fof(f1960,plain,
! [X0] : divide(sF3,inverse(divide(sF2,sF1))) = divide(divide(sF1,X0),inverse(divide(X0,sF1))),
inference(forward_demodulation,[],[f1957,f152]) ).
fof(f1970,plain,
divide(inverse(sF1),sF1) = divide(inverse(divide(sF2,sF1)),sF3),
inference(forward_demodulation,[],[f1939,f1382]) ).
fof(f1980,plain,
divide(inverse(sF1),sF1) = inverse(divide(sF1,divide(a2,sF3))),
inference(backward_demodulation,[],[f1351,f1970]) ).
fof(f1981,plain,
sF1 = divide(sF1,divide(inverse(sF1),sF1)),
inference(backward_demodulation,[],[f1378,f1970]) ).
fof(f1984,plain,
divide(inverse(sF1),sF1) = divide(divide(sF1,inverse(divide(sF1,sF1))),inverse(sF1)),
inference(backward_demodulation,[],[f1381,f1970]) ).
fof(f1985,plain,
sF1 = divide(divide(inverse(sF1),sF1),sF1),
inference(backward_demodulation,[],[f1382,f1970]) ).
fof(f1994,plain,
! [X0] : divide(sF2,divide(divide(X0,sF3),sF1)) = divide(divide(inverse(sF1),sF1),divide(divide(X0,sF1),sF1)),
inference(backward_demodulation,[],[f1927,f1970]) ).
fof(f2013,plain,
! [X0] : sF1 = divide(inverse(divide(X0,sF1)),divide(divide(sF1,inverse(sF1)),X0)),
inference(superposition,[],[f1,f1981]) ).
fof(f2035,plain,
divide(sF1,inverse(sF1)) = divide(sF3,inverse(divide(sF2,sF1))),
inference(superposition,[],[f152,f1985]) ).
fof(f2036,plain,
! [X0] : divide(inverse(divide(sF1,X0)),sF1) = inverse(divide(inverse(sF1),divide(X0,sF1))),
inference(superposition,[],[f26,f1985]) ).
fof(f2067,plain,
! [X0] : divide(sF1,inverse(sF1)) = divide(divide(sF1,X0),inverse(divide(X0,sF1))),
inference(backward_demodulation,[],[f1960,f2035]) ).
fof(f2075,plain,
! [X0] : inverse(divide(sF1,divide(X0,sF1))) = divide(inverse(divide(inverse(divide(sF1,sF1)),X0)),divide(sF1,inverse(sF1))),
inference(superposition,[],[f26,f2067]) ).
fof(f2210,plain,
! [X0] : divide(inverse(inverse(divide(X0,sF1))),divide(sF1,inverse(sF1))) = divide(sF3,inverse(divide(sF2,divide(divide(sF1,X0),sF1)))),
inference(superposition,[],[f152,f1959]) ).
fof(f2212,plain,
! [X0] : divide(X0,sF1) = divide(inverse(inverse(divide(X0,sF1))),divide(sF1,inverse(sF1))),
inference(forward_demodulation,[],[f2210,f152]) ).
fof(f2229,plain,
! [X0,X1] : inverse(inverse(divide(X0,sF1))) = divide(inverse(divide(X1,divide(X0,sF1))),divide(divide(inverse(sF1),sF1),X1)),
inference(superposition,[],[f1,f2212]) ).
fof(f2239,plain,
! [X0] : divide(sF1,inverse(sF1)) = divide(divide(sF1,inverse(divide(sF1,divide(X0,sF1)))),inverse(inverse(inverse(divide(X0,sF1))))),
inference(superposition,[],[f1082,f2212]) ).
fof(f2240,plain,
divide(divide(a2,sF3),sF1) = divide(sF1,inverse(sF1)),
inference(forward_demodulation,[],[f2239,f1471]) ).
fof(f2250,plain,
! [X0] : inverse(inverse(divide(X0,sF1))) = inverse(divide(inverse(sF1),divide(divide(X0,sF1),sF1))),
inference(forward_demodulation,[],[f2229,f26]) ).
fof(f2254,plain,
! [X0] : divide(sF3,inverse(divide(sF2,divide(X0,sF1)))) = divide(divide(sF1,inverse(sF1)),inverse(inverse(X0))),
inference(backward_demodulation,[],[f1429,f2240]) ).
fof(f2255,plain,
! [X0] : divide(sF2,divide(divide(X0,sF3),sF1)) = divide(inverse(X0),divide(sF1,inverse(sF1))),
inference(backward_demodulation,[],[f1439,f2240]) ).
fof(f2263,plain,
! [X0] : divide(inverse(divide(sF1,divide(X0,sF1))),sF1) = inverse(inverse(divide(X0,sF1))),
inference(forward_demodulation,[],[f2250,f2036]) ).
fof(f2269,plain,
! [X0] : inverse(divide(sF1,divide(X0,sF1))) = divide(sF2,divide(divide(divide(inverse(divide(sF1,sF1)),X0),sF3),sF1)),
inference(backward_demodulation,[],[f2075,f2255]) ).
fof(f2279,plain,
! [X0,X1] : inverse(inverse(inverse(divide(X0,divide(X1,sF1))))) = inverse(divide(inverse(inverse(divide(X0,sF1))),X1)),
inference(backward_demodulation,[],[f449,f2263]) ).
fof(f2282,plain,
divide(inverse(divide(sF1,sF1)),sF1) = inverse(inverse(sF1)),
inference(superposition,[],[f2263,f1985]) ).
fof(f2308,plain,
! [X0] : divide(inverse(divide(inverse(sF0),divide(X0,inverse(inverse(sF1))))),sF0) = X0,
inference(backward_demodulation,[],[f850,f2282]) ).
fof(f2320,plain,
! [X0,X1] : inverse(divide(divide(a2,sF3),divide(X0,sF1))) = divide(inverse(divide(X1,X0)),divide(divide(sF1,inverse(sF1)),X1)),
inference(superposition,[],[f26,f2240]) ).
fof(f2330,plain,
! [X0] : inverse(divide(X0,divide(sF1,sF1))) = divide(inverse(divide(sF1,inverse(sF1))),divide(divide(X0,sF1),divide(a2,sF3))),
inference(superposition,[],[f26,f2240]) ).
fof(f2334,plain,
divide(sF1,divide(a2,sF3)) = divide(sF3,inverse(divide(sF2,divide(divide(sF1,inverse(sF1)),sF1)))),
inference(superposition,[],[f152,f2240]) ).
fof(f2337,plain,
divide(inverse(sF1),sF1) = divide(sF1,divide(a2,sF3)),
inference(forward_demodulation,[],[f2334,f152]) ).
fof(f2345,plain,
sF1 = inverse(divide(divide(a2,sF3),divide(sF1,sF1))),
inference(backward_demodulation,[],[f2013,f2320]) ).
fof(f2352,plain,
sF1 = divide(sF1,inverse(divide(sF1,divide(divide(inverse(sF1),sF1),sF1)))),
inference(backward_demodulation,[],[f1329,f2337]) ).
fof(f2355,plain,
divide(inverse(sF1),sF1) = inverse(divide(inverse(sF1),sF1)),
inference(backward_demodulation,[],[f1980,f2337]) ).
fof(f2373,plain,
sF1 = divide(sF1,inverse(divide(sF1,sF1))),
inference(forward_demodulation,[],[f2352,f1985]) ).
fof(f2381,plain,
inverse(divide(sF2,divide(sF1,sF1))) = divide(sF1,inverse(sF3)),
inference(backward_demodulation,[],[f1142,f2373]) ).
fof(f2384,plain,
divide(inverse(sF1),sF1) = divide(sF1,inverse(sF1)),
inference(backward_demodulation,[],[f1984,f2373]) ).
fof(f2390,plain,
sF1 = divide(sF1,divide(sF1,inverse(sF1))),
inference(backward_demodulation,[],[f1981,f2384]) ).
fof(f2393,plain,
sF1 = divide(divide(sF1,inverse(sF1)),sF1),
inference(backward_demodulation,[],[f1985,f2384]) ).
fof(f2401,plain,
! [X0] : divide(sF2,divide(divide(X0,sF3),sF1)) = divide(divide(sF1,inverse(sF1)),divide(divide(X0,sF1),sF1)),
inference(backward_demodulation,[],[f1994,f2384]) ).
fof(f2409,plain,
divide(sF1,divide(a2,sF3)) = divide(sF1,inverse(sF1)),
inference(backward_demodulation,[],[f2337,f2384]) ).
fof(f2412,plain,
divide(sF1,inverse(sF1)) = inverse(divide(sF1,inverse(sF1))),
inference(backward_demodulation,[],[f2355,f2384]) ).
fof(f2449,plain,
! [X0] : inverse(divide(X0,divide(sF1,sF1))) = divide(divide(sF1,inverse(sF1)),divide(divide(X0,sF1),divide(a2,sF3))),
inference(backward_demodulation,[],[f2330,f2412]) ).
fof(f2455,plain,
sF1 = divide(sF3,a2),
inference(forward_demodulation,[],[f2393,f1738]) ).
fof(f2457,plain,
sF1 = divide(a2,sF3),
inference(forward_demodulation,[],[f2390,f1674]) ).
fof(f2473,plain,
! [X0] : inverse(X0) = divide(sF1,divide(X0,sF1)),
inference(backward_demodulation,[],[f1495,f2455]) ).
fof(f2504,plain,
divide(sF1,sF1) = inverse(divide(sF1,inverse(sF1))),
inference(backward_demodulation,[],[f1781,f2455]) ).
fof(f2509,plain,
! [X2,X0,X1] : divide(inverse(divide(X0,X1)),sF1) = divide(divide(divide(X1,X0),X2),inverse(divide(X2,sF1))),
inference(backward_demodulation,[],[f1789,f2455]) ).
fof(f2530,plain,
! [X0] : sF1 = divide(X0,divide(sF1,inverse(X0))),
inference(backward_demodulation,[],[f1674,f2457]) ).
fof(f2533,plain,
! [X0,X1] : divide(sF3,inverse(divide(sF2,divide(X0,sF1)))) = divide(divide(divide(inverse(X0),sF1),X1),inverse(divide(X1,sF1))),
inference(backward_demodulation,[],[f1713,f2457]) ).
fof(f2549,plain,
sF1 = inverse(divide(sF1,divide(sF1,sF1))),
inference(backward_demodulation,[],[f2345,f2457]) ).
fof(f2551,plain,
divide(sF1,sF1) = divide(sF1,inverse(sF1)),
inference(backward_demodulation,[],[f2409,f2457]) ).
fof(f2553,plain,
! [X0] : inverse(divide(X0,divide(sF1,sF1))) = divide(divide(sF1,inverse(sF1)),divide(divide(X0,sF1),sF1)),
inference(backward_demodulation,[],[f2449,f2457]) ).
fof(f2619,plain,
! [X0] : inverse(inverse(divide(X0,sF1))) = divide(inverse(inverse(X0)),sF1),
inference(backward_demodulation,[],[f2263,f2473]) ).
fof(f2620,plain,
! [X0] : inverse(inverse(X0)) = divide(sF2,divide(divide(divide(inverse(divide(sF1,sF1)),X0),sF3),sF1)),
inference(backward_demodulation,[],[f2269,f2473]) ).
fof(f2630,plain,
! [X0] : divide(sF2,divide(divide(X0,sF3),sF1)) = inverse(divide(X0,divide(sF1,sF1))),
inference(backward_demodulation,[],[f2401,f2553]) ).
fof(f2643,plain,
! [X0] : divide(sF3,inverse(divide(sF2,divide(X0,sF1)))) = divide(divide(sF1,sF1),inverse(inverse(X0))),
inference(backward_demodulation,[],[f2254,f2551]) ).
fof(f2644,plain,
! [X0] : divide(sF2,divide(divide(X0,sF3),sF1)) = divide(inverse(X0),divide(sF1,sF1)),
inference(backward_demodulation,[],[f2255,f2551]) ).
fof(f2669,plain,
divide(sF1,sF1) = inverse(divide(sF1,sF1)),
inference(backward_demodulation,[],[f2504,f2551]) ).
fof(f2675,plain,
sF1 = inverse(inverse(sF1)),
inference(forward_demodulation,[],[f2549,f2473]) ).
fof(f2684,plain,
! [X0] : divide(sF3,inverse(divide(sF2,divide(X0,sF1)))) = divide(inverse(divide(sF1,inverse(X0))),sF1),
inference(forward_demodulation,[],[f2533,f2509]) ).
fof(f2714,plain,
! [X0,X1] : inverse(inverse(inverse(divide(X0,divide(X1,sF1))))) = inverse(divide(divide(inverse(inverse(X0)),sF1),X1)),
inference(backward_demodulation,[],[f2279,f2619]) ).
fof(f2736,plain,
! [X0] : inverse(inverse(X0)) = inverse(divide(divide(inverse(divide(sF1,sF1)),X0),divide(sF1,sF1))),
inference(backward_demodulation,[],[f2620,f2630]) ).
fof(f2737,plain,
! [X0] : inverse(divide(inverse(X0),divide(sF1,sF1))) = X0,
inference(backward_demodulation,[],[f1506,f2630]) ).
fof(f2740,plain,
a2 = inverse(divide(sF2,divide(sF1,sF1))),
inference(backward_demodulation,[],[f1508,f2630]) ).
fof(f2743,plain,
sF1 = divide(sF1,divide(sF1,sF1)),
inference(backward_demodulation,[],[f2373,f2669]) ).
fof(f2751,plain,
! [X0] : inverse(divide(X0,divide(sF1,sF1))) = divide(inverse(X0),divide(sF1,sF1)),
inference(backward_demodulation,[],[f2630,f2644]) ).
fof(f2811,plain,
! [X3,X4] : divide(X4,X3) = divide(divide(sF1,sF1),inverse(inverse(divide(X3,X4)))),
inference(backward_demodulation,[],[f152,f2643]) ).
fof(f2819,plain,
divide(inverse(sF1),divide(sF1,inverse(divide(sF1,sF3)))) = divide(divide(sF1,sF1),inverse(inverse(sF2))),
inference(backward_demodulation,[],[f461,f2643]) ).
fof(f2833,plain,
! [X0] : divide(inverse(divide(inverse(sF0),divide(X0,sF1))),sF0) = X0,
inference(backward_demodulation,[],[f2308,f2675]) ).
fof(f2843,plain,
! [X0] : divide(divide(sF1,sF1),inverse(inverse(X0))) = divide(inverse(divide(sF1,inverse(X0))),sF1),
inference(forward_demodulation,[],[f2684,f2643]) ).
fof(f2875,plain,
a2 = divide(sF1,inverse(sF3)),
inference(backward_demodulation,[],[f2381,f2740]) ).
fof(f2876,plain,
! [X0] : inverse(inverse(X0)) = inverse(divide(divide(divide(sF1,sF1),X0),divide(sF1,sF1))),
inference(forward_demodulation,[],[f2736,f2669]) ).
fof(f2882,plain,
sF1 = inverse(sF1),
inference(forward_demodulation,[],[f2743,f2473]) ).
fof(f2900,plain,
! [X0] : divide(inverse(inverse(X0)),divide(sF1,sF1)) = X0,
inference(backward_demodulation,[],[f2737,f2751]) ).
fof(f2935,plain,
! [X0] : inverse(inverse(X0)) = divide(inverse(divide(divide(sF1,sF1),X0)),divide(sF1,sF1)),
inference(forward_demodulation,[],[f2876,f2751]) ).
fof(f2951,plain,
! [X0] : inverse(divide(sF1,divide(X0,sF1))) = divide(inverse(divide(sF1,X0)),sF1),
inference(backward_demodulation,[],[f2036,f2882]) ).
fof(f2968,plain,
divide(divide(sF1,sF1),inverse(inverse(sF2))) = divide(sF1,divide(sF1,inverse(divide(sF1,sF3)))),
inference(backward_demodulation,[],[f2819,f2882]) ).
fof(f3002,plain,
! [X0] : inverse(inverse(X0)) = divide(inverse(divide(sF1,X0)),sF1),
inference(forward_demodulation,[],[f2951,f2473]) ).
fof(f3024,plain,
! [X2,X3,X0,X1] : inverse(inverse(inverse(divide(X0,divide(X1,divide(X2,X3)))))) = inverse(divide(inverse(inverse(divide(X0,divide(X3,X2)))),X1)),
inference(backward_demodulation,[],[f448,f3002]) ).
fof(f3027,plain,
! [X0] : inverse(inverse(inverse(X0))) = divide(divide(sF1,sF1),inverse(inverse(X0))),
inference(backward_demodulation,[],[f2843,f3002]) ).
fof(f3099,plain,
! [X3,X4] : divide(X4,X3) = inverse(inverse(inverse(divide(X3,X4)))),
inference(backward_demodulation,[],[f2811,f3027]) ).
fof(f3108,plain,
divide(sF1,divide(sF1,inverse(divide(sF1,sF3)))) = inverse(inverse(inverse(sF2))),
inference(backward_demodulation,[],[f2968,f3027]) ).
fof(f3118,plain,
! [X0,X1] : divide(divide(X1,sF1),X0) = inverse(divide(divide(inverse(inverse(X0)),sF1),X1)),
inference(backward_demodulation,[],[f2714,f3099]) ).
fof(f3119,plain,
! [X2,X3,X0,X1] : inverse(divide(inverse(inverse(divide(X0,divide(X3,X2)))),X1)) = divide(divide(X1,divide(X2,X3)),X0),
inference(backward_demodulation,[],[f3024,f3099]) ).
fof(f3273,plain,
! [X0] : divide(sF1,X0) = inverse(divide(inverse(inverse(X0)),sF1)),
inference(superposition,[],[f3099,f2619]) ).
fof(f3295,plain,
! [X0] : divide(sF1,divide(X0,sF1)) = inverse(divide(divide(inverse(inverse(X0)),sF1),sF1)),
inference(superposition,[],[f3273,f2619]) ).
fof(f3302,plain,
! [X0] : divide(sF1,divide(X0,sF1)) = divide(divide(sF1,sF1),X0),
inference(forward_demodulation,[],[f3295,f3118]) ).
fof(f3322,plain,
! [X0] : inverse(X0) = divide(divide(sF1,sF1),X0),
inference(forward_demodulation,[],[f3302,f2473]) ).
fof(f3334,plain,
! [X0] : inverse(inverse(X0)) = divide(inverse(inverse(X0)),divide(sF1,sF1)),
inference(backward_demodulation,[],[f2935,f3322]) ).
fof(f3369,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[],[f3334,f2900]) ).
fof(f3469,plain,
! [X0,X1] : divide(divide(X1,sF1),X0) = inverse(divide(divide(X0,sF1),X1)),
inference(backward_demodulation,[],[f3118,f3369]) ).
fof(f3491,plain,
! [X3,X4] : divide(X4,X3) = inverse(divide(X3,X4)),
inference(backward_demodulation,[],[f3099,f3369]) ).
fof(f3504,plain,
! [X2,X3,X0,X1] : divide(divide(X1,divide(X2,X3)),X0) = inverse(divide(divide(X0,divide(X3,X2)),X1)),
inference(backward_demodulation,[],[f3119,f3369]) ).
fof(f3516,plain,
inverse(sF2) = divide(sF1,divide(sF1,inverse(divide(sF1,sF3)))),
inference(backward_demodulation,[],[f3108,f3369]) ).
fof(f3634,plain,
! [X2,X3,X0,X1] : divide(X1,divide(X0,divide(X3,X2))) = divide(divide(X1,divide(X2,X3)),X0),
inference(backward_demodulation,[],[f3504,f3491]) ).
fof(f3696,plain,
! [X0] : divide(divide(divide(X0,sF1),inverse(sF0)),sF0) = X0,
inference(backward_demodulation,[],[f2833,f3491]) ).
fof(f3714,plain,
inverse(sF2) = divide(sF1,divide(sF1,divide(sF3,sF1))),
inference(backward_demodulation,[],[f3516,f3491]) ).
fof(f3730,plain,
! [X0,X1] : divide(X1,divide(X0,sF1)) = divide(divide(X1,sF1),X0),
inference(forward_demodulation,[],[f3469,f3491]) ).
fof(f3853,plain,
inverse(sF2) = divide(sF1,inverse(sF3)),
inference(forward_demodulation,[],[f3714,f2473]) ).
fof(f3976,plain,
! [X0] : divide(divide(X0,divide(inverse(sF0),sF1)),sF0) = X0,
inference(backward_demodulation,[],[f3696,f3730]) ).
fof(f4089,plain,
a2 = inverse(sF2),
inference(forward_demodulation,[],[f3853,f2875]) ).
fof(f4191,plain,
! [X0] : divide(X0,divide(sF0,divide(sF1,inverse(sF0)))) = X0,
inference(forward_demodulation,[],[f3976,f3634]) ).
fof(f4373,plain,
! [X0] : divide(X0,sF1) = X0,
inference(forward_demodulation,[],[f4191,f2530]) ).
fof(f4523,plain,
! [X0] : inverse(X0) = divide(sF1,X0),
inference(backward_demodulation,[],[f2473,f4373]) ).
fof(f4680,plain,
sF3 = inverse(sF2),
inference(backward_demodulation,[],[f13,f4523]) ).
fof(f4769,plain,
a2 = sF3,
inference(forward_demodulation,[],[f4680,f4089]) ).
fof(f4858,plain,
$false,
inference(forward_subsumption_resolution,[],[f4769,f14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP470-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n008.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 10:06:11 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 Running first-order theorem proving
% 0.15/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
% 9.74/2.42 % (996650)Detected a unit-equality problem, will run specialized UEQ schedule.
% 9.74/2.42 % (996771)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=216173267:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_3000 on theBenchmark for (3000ds/181Mi)
% 9.74/2.42 % (996767)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=1564824682:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_3000 on theBenchmark for (3000ds/130792Mi)
% 9.74/2.42 % (996765)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=2437677051:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_3000 on theBenchmark for (3000ds/138329Mi)
% 9.74/2.42 % (996770)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3980985325:i=136:bd=preordered:ins=2:av=off_3000 on theBenchmark for (3000ds/136Mi)
% 9.74/2.42 % (996769)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1143784978:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_3000 on theBenchmark for (3000ds/130716Mi)
% 9.74/2.42 % (996772)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1687097022:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_3000 on theBenchmark for (3000ds/257Mi)
% 9.74/2.42 % (996773)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1648241074:i=1187:sd=4:av=off:ss=axioms:sgt=32_3000 on theBenchmark for (3000ds/1187Mi)
% 9.74/2.42 % (996771)Instruction limit reached!
% 9.74/2.42 % (996771)------------------------------
% 9.74/2.42 % (996771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.74/2.42 % (996771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.42 % (996771)CaDiCaL version: 2.1.3
% 9.74/2.42 % (996771)Termination reason: Instruction limit
% 9.74/2.42 % (996771)Termination phase: Saturation
% 9.74/2.42 % (996771)Time elapsed: 0.054 s
% 9.74/2.42 % (996771)Peak memory usage: 90 MB
% 9.74/2.42 % (996771)Instructions burned: 185 (million)
% 9.74/2.42 % (996770)Instruction limit reached!
% 9.74/2.42 % (996770)------------------------------
% 9.74/2.42 % (996770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.74/2.42 % (996770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.42 % (996770)CaDiCaL version: 2.1.3
% 9.74/2.42 % (996770)Termination reason: Instruction limit
% 9.74/2.42 % (996770)Termination phase: Saturation
% 9.74/2.42 % (996770)Time elapsed: 0.082 s
% 9.74/2.42 % (996770)Peak memory usage: 89 MB
% 9.74/2.42 % (996770)Instructions burned: 137 (million)
% 9.74/2.42 % (996795)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3182731604:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 9.74/2.42 % (996772)Instruction limit reached!
% 9.74/2.42 % (996772)------------------------------
% 9.74/2.42 % (996772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.74/2.42 % (996772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.42 % (996772)CaDiCaL version: 2.1.3
% 9.74/2.42 % (996772)Termination reason: Instruction limit
% 9.74/2.42 % (996772)Termination phase: Saturation
% 9.74/2.42 % (996772)Time elapsed: 0.159 s
% 9.74/2.42 % (996772)Peak memory usage: 91 MB
% 9.74/2.42 % (996772)Instructions burned: 257 (million)
% 9.74/2.42 % (996803)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4013175345:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 9.74/2.42 % (996805)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1571553323:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 9.74/2.42 % (996805)Instruction limit reached!
% 9.74/2.42 % (996805)------------------------------
% 9.74/2.42 % (996805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.74/2.42 % (996805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.42 % (996805)CaDiCaL version: 2.1.3
% 9.74/2.42 % (996805)Termination reason: Instruction limit
% 9.74/2.42 % (996805)Termination phase: Saturation
% 9.74/2.42 % (996805)Time elapsed: 0.128 s
% 9.74/2.42 % (996805)Peak memory usage: 90 MB
% 9.74/2.42 % (996805)Instructions burned: 216 (million)
% 9.74/2.42 % (996817)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=3537641013:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 9.74/2.42 % (996773)Instruction limit reached!
% 9.74/2.42 % (996773)------------------------------
% 9.74/2.42 % (996773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.74/2.42 % (996773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.42 % (996773)CaDiCaL version: 2.1.3
% 9.74/2.42 % (996773)Termination reason: Instruction limit
% 9.74/2.42 % (996773)Termination phase: Saturation
% 9.74/2.42 % (996773)Time elapsed: 0.635 s
% 9.74/2.42 % (996773)Peak memory usage: 100 MB
% 9.74/2.42 % (996773)Instructions burned: 1187 (million)
% 9.74/2.42 % (996817)Instruction limit reached!
% 9.74/2.42 % (996817)------------------------------
% 9.74/2.42 % (996817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.74/2.42 % (996817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.42 % (996817)CaDiCaL version: 2.1.3
% 9.74/2.42 % (996817)Termination reason: Instruction limit
% 9.74/2.42 % (996817)Termination phase: Saturation
% 9.74/2.42 % (996817)Time elapsed: 0.180 s
% 9.74/2.42 % (996817)Peak memory usage: 92 MB
% 9.74/2.42 % (996817)Instructions burned: 317 (million)
% 9.74/2.42 % (996850)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=1148220968:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 9.74/2.42 % (996795)Instruction limit reached!
% 9.74/2.42 % (996795)------------------------------
% 9.74/2.42 % (996795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.74/2.42 % (996795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/2.42 % (996795)CaDiCaL version: 2.1.3
% 9.74/2.42 % (996795)Termination reason: Instruction limit
% 9.74/2.42 % (996795)Termination phase: Saturation
% 9.74/2.42 % (996795)Time elapsed: 0.689 s
% 9.74/2.42 % (996795)Peak memory usage: 141 MB
% 9.74/2.42 % (996795)Instructions burned: 2054 (million)
% 9.74/2.42 % (996851)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3575317016:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 9.74/2.42 % (996853)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3128546677:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2990 on theBenchmark for (2990ds/14534Mi)
% 9.74/2.42 % (996769)First to succeed.
% 9.74/2.42 % (996769)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-996650"
% 9.74/2.42 % (996851)Also succeeded, but the first one will report.
% 9.74/2.42 % (996769)Refutation found. Thanks to Tanya!
% 9.74/2.42 % SZS status Unsatisfiable for theBenchmark
% 9.74/2.42 % SZS output start Proof for theBenchmark
% See solution above
% 11.54/2.51 % (996769)------------------------------
% 11.54/2.51 % (996769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.51 % (996769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.51 % (996769)CaDiCaL version: 2.1.3
% 11.54/2.51 % (996769)Termination reason: Refutation
% 11.54/2.51 % (996769)Time elapsed: 1.166 s
% 11.54/2.51 % (996769)Peak memory usage: 136 MB
% 11.54/2.51 % (996769)Instructions burned: 1858 (million)
% 11.54/2.51 % (996769)------------------------------
% 11.54/2.51 % (996769)------------------------------
% 11.54/2.51 % (996650)Success in time 1.549 s
% 11.54/2.51 % Vampire exiting
%------------------------------------------------------------------------------