%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : BOO023-1 : TPTP v9.3.1. Released v2.2.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:35:55 AM UTC 2026
% Result : Unsatisfiable 28.16s 5.19s
% Output : Refutation 31.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 9
% Syntax : Number of formulae : 309 ( 309 unt; 1 def)
% Number of atoms : 309 ( 304 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 661 ( 661 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : multiply(add(X0,X1),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiply_add) ).
fof(f2,axiom,
! [X2,X0,X1] : multiply(X0,add(X1,X2)) = add(multiply(X1,X0),multiply(X2,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiply_add_property) ).
fof(f3,axiom,
! [X0] : add(X0,inverse(X0)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_inverse) ).
fof(f4,axiom,
! [X2,X0,X1] : pixley(X0,X1,X2) = add(multiply(X0,inverse(X1)),add(multiply(X0,X2),multiply(inverse(X1),X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pixley_defn) ).
fof(f5,axiom,
! [X0,X1] : pixley(X0,X0,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pixley1) ).
fof(f6,axiom,
! [X0,X1] : pixley(X0,X1,X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pixley2) ).
fof(f7,axiom,
! [X0,X1] : pixley(X0,X1,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pixley3) ).
fof(f8,negated_conjecture,
add(a,multiply(b,c)) != multiply(add(a,b),add(a,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_add_multiply_property) ).
fof(f9,plain,
! [X0,X1] : add(multiply(X0,inverse(X1)),add(multiply(X0,X0),multiply(inverse(X1),X0))) = X0,
inference(definition_unfolding,[],[f7,f4]) ).
fof(f10,plain,
! [X0,X1] : add(multiply(X0,inverse(X1)),add(multiply(X0,X1),multiply(inverse(X1),X1))) = X0,
inference(definition_unfolding,[],[f6,f4]) ).
fof(f11,plain,
! [X0,X1] : add(multiply(X0,inverse(X0)),add(multiply(X0,X1),multiply(inverse(X0),X1))) = X1,
inference(definition_unfolding,[],[f5,f4]) ).
fof(f12,definition,
~ sP0(multiply(add(a,b),add(a,c))),
introduced(definition,[new_symbols(definition,[sP0])],[inequality_splitting_name_introduction]) ).
fof(f13,plain,
sP0(add(a,multiply(b,c))),
inference(inequality_splitting,[],[f8,f12]) ).
fof(f14,plain,
! [X0,X1] : add(multiply(X0,inverse(X0)),multiply(X1,add(X0,inverse(X0)))) = X1,
inference(forward_demodulation,[],[f11,f2]) ).
fof(f15,plain,
! [X0,X1] : add(multiply(X0,inverse(X1)),multiply(X1,add(X0,inverse(X1)))) = X0,
inference(forward_demodulation,[],[f10,f2]) ).
fof(f16,plain,
! [X0,X1] : add(multiply(X0,inverse(X1)),multiply(X0,add(X0,inverse(X1)))) = X0,
inference(forward_demodulation,[],[f9,f2]) ).
fof(f17,plain,
! [X0,X1] : add(multiply(X0,inverse(X0)),multiply(X1,n1)) = X1,
inference(forward_demodulation,[],[f14,f3]) ).
fof(f18,plain,
! [X2,X0,X1] : multiply(X0,add(add(X1,X0),X2)) = add(X0,multiply(X2,X0)),
inference(superposition,[],[f2,f1]) ).
fof(f19,plain,
! [X2,X0,X1] : multiply(X0,add(X1,add(X2,X0))) = add(multiply(X1,X0),X0),
inference(superposition,[],[f2,f1]) ).
fof(f20,plain,
! [X2,X0,X1] : multiply(X2,X0) = multiply(multiply(X0,add(X1,X2)),multiply(X2,X0)),
inference(superposition,[],[f1,f2]) ).
fof(f24,plain,
! [X0,X1] : add(X1,n1) = add(multiply(X0,inverse(X0)),n1),
inference(superposition,[],[f17,f1]) ).
fof(f31,plain,
! [X0,X1] : add(X1,X0) = add(multiply(add(X1,X0),inverse(X0)),add(X0,multiply(inverse(X0),X0))),
inference(superposition,[],[f15,f18]) ).
fof(f33,plain,
! [X0,X1] : multiply(X1,add(X0,inverse(X1))) = multiply(X0,multiply(X1,add(X0,inverse(X1)))),
inference(superposition,[],[f1,f15]) ).
fof(f35,plain,
! [X0,X1] : add(multiply(X1,multiply(X0,n1)),multiply(X0,n1)) = multiply(multiply(X0,n1),add(X1,X0)),
inference(superposition,[],[f19,f17]) ).
fof(f41,plain,
! [X2,X3,X0,X1] : multiply(add(X0,add(X2,X1)),add(X1,X3)) = add(add(multiply(X0,X1),X1),multiply(X3,add(X0,add(X2,X1)))),
inference(superposition,[],[f2,f19]) ).
fof(f46,plain,
! [X0,X1] : add(multiply(X1,inverse(X0)),inverse(X0)) = multiply(inverse(X0),add(X1,n1)),
inference(superposition,[],[f19,f3]) ).
fof(f47,plain,
! [X0,X1] : add(inverse(X0),multiply(X1,inverse(X0))) = multiply(inverse(X0),add(n1,X1)),
inference(superposition,[],[f18,f3]) ).
fof(f48,plain,
! [X0] : inverse(X0) = multiply(n1,inverse(X0)),
inference(superposition,[],[f1,f3]) ).
fof(f55,plain,
! [X2,X0,X1] : multiply(X1,add(X2,add(X0,X1))) = multiply(add(X0,X1),multiply(X1,add(X2,add(X0,X1)))),
inference(superposition,[],[f20,f1]) ).
fof(f59,plain,
! [X2,X3,X0,X1] : add(X0,multiply(X1,X0)) = multiply(multiply(add(add(X2,X0),X1),add(X3,X0)),add(X0,multiply(X1,X0))),
inference(superposition,[],[f20,f18]) ).
fof(f67,plain,
! [X2,X0,X1] : add(multiply(X2,X1),X1) = multiply(add(X0,X1),add(multiply(X2,X1),X1)),
inference(forward_demodulation,[],[f55,f19]) ).
fof(f72,plain,
! [X0] : add(inverse(n1),multiply(X0,n1)) = X0,
inference(superposition,[],[f17,f48]) ).
fof(f73,plain,
! [X0] : n1 = add(inverse(X0),multiply(X0,add(n1,inverse(X0)))),
inference(superposition,[],[f15,f48]) ).
fof(f74,plain,
! [X0] : n1 = add(inverse(X0),multiply(n1,add(n1,inverse(X0)))),
inference(superposition,[],[f16,f48]) ).
fof(f86,plain,
! [X2,X0] : add(X0,X0) = multiply(add(X2,X0),add(X0,X0)),
inference(superposition,[],[f67,f1]) ).
fof(f103,plain,
! [X0] : add(inverse(X0),inverse(X0)) = multiply(n1,add(inverse(X0),inverse(X0))),
inference(superposition,[],[f86,f3]) ).
fof(f108,plain,
! [X2,X0,X1] : multiply(add(X0,X0),add(X1,add(X2,X0))) = add(multiply(X1,add(X0,X0)),add(X0,X0)),
inference(superposition,[],[f2,f86]) ).
fof(f109,plain,
! [X2,X0,X1] : multiply(add(X0,X0),add(add(X1,X0),X2)) = add(add(X0,X0),multiply(X2,add(X0,X0))),
inference(superposition,[],[f2,f86]) ).
fof(f115,plain,
! [X0,X1] : add(X0,multiply(inverse(X0),X0)) = multiply(add(X1,X0),add(X0,multiply(inverse(X0),X0))),
inference(superposition,[],[f33,f18]) ).
fof(f137,plain,
! [X0,X1] : add(X1,n1) = add(X0,n1),
inference(superposition,[],[f24,f24]) ).
fof(f186,plain,
! [X0] : add(inverse(X0),inverse(X0)) = multiply(inverse(X0),add(n1,n1)),
inference(superposition,[],[f47,f48]) ).
fof(f223,plain,
! [X0] : add(X0,multiply(X0,X0)) = multiply(add(X0,X0),add(X0,multiply(X0,X0))),
inference(superposition,[],[f59,f86]) ).
fof(f439,plain,
! [X0,X1] : multiply(add(inverse(X0),inverse(X0)),add(X1,n1)) = add(multiply(X1,add(inverse(X0),inverse(X0))),add(inverse(X0),inverse(X0))),
inference(superposition,[],[f2,f103]) ).
fof(f440,plain,
! [X0,X1] : multiply(add(inverse(X0),inverse(X0)),add(n1,X1)) = add(add(inverse(X0),inverse(X0)),multiply(X1,add(inverse(X0),inverse(X0)))),
inference(superposition,[],[f2,f103]) ).
fof(f463,plain,
! [X2,X0,X1] : multiply(add(X1,multiply(inverse(X1),X1)),X2) = multiply(multiply(X2,add(X0,X1)),multiply(add(X1,multiply(inverse(X1),X1)),X2)),
inference(superposition,[],[f20,f31]) ).
fof(f704,plain,
! [X0,X1] : multiply(inverse(X1),add(X0,n1)) = add(inverse(X1),inverse(X1)),
inference(superposition,[],[f186,f137]) ).
fof(f962,plain,
! [X2,X3,X0,X1] : multiply(add(X2,multiply(multiply(X0,n1),add(X1,X0))),add(multiply(X0,n1),X3)) = add(add(multiply(X2,multiply(X0,n1)),multiply(X0,n1)),multiply(X3,add(X2,multiply(multiply(X0,n1),add(X1,X0))))),
inference(superposition,[],[f41,f35]) ).
fof(f974,plain,
! [X2,X3,X0,X1] : multiply(add(X2,multiply(inverse(X0),add(X1,n1))),add(inverse(X0),X3)) = add(add(multiply(X2,inverse(X0)),inverse(X0)),multiply(X3,add(X2,multiply(inverse(X0),add(X1,n1))))),
inference(superposition,[],[f41,f704]) ).
fof(f978,plain,
! [X2,X0,X1] : add(add(multiply(X0,X1),X1),add(multiply(X0,X1),X1)) = multiply(add(X0,add(X2,X1)),add(X1,X1)),
inference(superposition,[],[f41,f19]) ).
fof(f1006,plain,
! [X2,X3,X0,X1] : multiply(add(X2,multiply(inverse(X0),add(X1,n1))),add(inverse(X0),X3)) = add(multiply(inverse(X0),add(X2,n1)),multiply(X3,add(X2,multiply(inverse(X0),add(X1,n1))))),
inference(forward_demodulation,[],[f974,f46]) ).
fof(f1013,plain,
! [X2,X3,X0,X1] : multiply(add(X2,multiply(multiply(X0,n1),add(X1,X0))),add(multiply(X0,n1),X3)) = add(multiply(multiply(X0,n1),add(X2,X0)),multiply(X3,add(X2,multiply(multiply(X0,n1),add(X1,X0))))),
inference(forward_demodulation,[],[f962,f35]) ).
fof(f1038,plain,
! [X2,X0,X1] : add(add(X0,X0),add(X0,X0)) = multiply(add(add(X1,X0),add(X2,X0)),add(X0,X0)),
inference(superposition,[],[f978,f1]) ).
fof(f1105,plain,
! [X2,X0,X1] : add(X1,multiply(add(X2,X1),X1)) = multiply(add(add(multiply(add(X0,X1),X1),X1),add(multiply(add(X0,X1),X1),X1)),add(X1,multiply(add(X2,X1),X1))),
inference(superposition,[],[f59,f978]) ).
fof(f1117,plain,
! [X0,X1] : add(X1,X1) = multiply(add(add(multiply(add(X0,X1),X1),X1),add(multiply(add(X0,X1),X1),X1)),add(X1,X1)),
inference(forward_demodulation,[],[f1105,f1]) ).
fof(f1146,plain,
! [X1] : add(X1,X1) = add(add(X1,X1),add(X1,X1)),
inference(forward_demodulation,[],[f1117,f1038]) ).
fof(f1194,plain,
! [X0,X1] : multiply(X0,add(X1,X1)) = add(multiply(X0,add(X1,X1)),multiply(X0,add(X1,X1))),
inference(superposition,[],[f1146,f2]) ).
fof(f1199,plain,
! [X0,X1] : multiply(add(X0,X0),add(X0,X1)) = add(add(multiply(add(X0,X0),X0),X0),multiply(X1,add(X0,X0))),
inference(superposition,[],[f41,f1146]) ).
fof(f1200,plain,
! [X0] : multiply(X0,add(X0,X0)) = add(multiply(add(X0,X0),X0),X0),
inference(superposition,[],[f19,f1146]) ).
fof(f1206,plain,
! [X2,X0,X1] : add(add(multiply(X1,add(X0,X0)),add(X0,X0)),add(multiply(X1,add(X0,X0)),add(X0,X0))) = multiply(add(X1,add(X2,add(X0,X0))),add(X0,X0)),
inference(superposition,[],[f978,f1146]) ).
fof(f1227,plain,
! [X0] : add(X0,X0) = multiply(X0,add(X0,X0)),
inference(forward_demodulation,[],[f1200,f1]) ).
fof(f1228,plain,
! [X0,X1] : add(add(X0,X0),multiply(X1,add(X0,X0))) = multiply(add(X0,X0),add(X0,X1)),
inference(forward_demodulation,[],[f1199,f1]) ).
fof(f1233,plain,
! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(add(X1,X1),add(X0,X0)),
inference(forward_demodulation,[],[f1194,f2]) ).
fof(f1245,plain,
! [X2,X0,X1] : multiply(add(X0,X0),add(add(X1,X0),X2)) = multiply(add(X0,X0),add(X0,X2)),
inference(backward_demodulation,[],[f109,f1228]) ).
fof(f1247,plain,
! [X0,X1] : multiply(add(inverse(X0),inverse(X0)),add(n1,X1)) = multiply(add(inverse(X0),inverse(X0)),add(inverse(X0),X1)),
inference(backward_demodulation,[],[f440,f1228]) ).
fof(f1265,plain,
! [X0] : add(X0,n1) = multiply(n1,add(X0,n1)),
inference(superposition,[],[f1227,f137]) ).
fof(f1274,plain,
! [X0] : multiply(X0,X0) = multiply(add(X0,X0),multiply(X0,X0)),
inference(superposition,[],[f20,f1227]) ).
fof(f1275,plain,
! [X0,X1] : add(add(multiply(add(X0,X1),X1),X1),add(add(X0,X1),add(X0,X1))) = multiply(add(add(X0,X1),add(X0,X1)),add(X1,add(X0,X1))),
inference(superposition,[],[f41,f1227]) ).
fof(f1278,plain,
! [X0,X1] : add(multiply(X1,add(X0,X0)),add(X0,X0)) = multiply(add(X0,X0),add(X1,X0)),
inference(superposition,[],[f2,f1227]) ).
fof(f1292,plain,
! [X2,X0,X1] : multiply(add(X1,add(X2,add(X0,X0))),add(X0,X0)) = add(multiply(add(X0,X0),add(X1,X0)),multiply(add(X0,X0),add(X1,X0))),
inference(backward_demodulation,[],[f1206,f1278]) ).
fof(f1295,plain,
! [X2,X0,X1] : multiply(add(X0,X0),add(X1,add(X2,X0))) = multiply(add(X0,X0),add(X1,X0)),
inference(backward_demodulation,[],[f108,f1278]) ).
fof(f1296,plain,
! [X0,X1] : multiply(add(inverse(X0),inverse(X0)),add(X1,n1)) = multiply(add(inverse(X0),inverse(X0)),add(X1,inverse(X0))),
inference(backward_demodulation,[],[f439,f1278]) ).
fof(f1299,plain,
! [X0,X1] : add(add(X1,X1),add(add(X0,X1),add(X0,X1))) = multiply(add(add(X0,X1),add(X0,X1)),add(X1,add(X0,X1))),
inference(forward_demodulation,[],[f1275,f1]) ).
fof(f1309,plain,
! [X2,X0,X1] : multiply(add(X1,add(X2,add(X0,X0))),add(X0,X0)) = multiply(add(X1,X0),add(add(X0,X0),add(X0,X0))),
inference(forward_demodulation,[],[f1292,f2]) ).
fof(f1311,plain,
! [X2,X0,X1] : multiply(add(X1,X0),add(X0,X0)) = multiply(add(X1,add(X2,add(X0,X0))),add(X0,X0)),
inference(forward_demodulation,[],[f1309,f1146]) ).
fof(f1313,plain,
! [X2,X0,X1] : add(X0,X0) = multiply(add(X1,add(X2,add(X0,X0))),add(X0,X0)),
inference(forward_demodulation,[],[f1311,f86]) ).
fof(f1326,plain,
! [X0,X1] : multiply(multiply(X0,X0),add(add(X0,X0),X1)) = add(multiply(X0,X0),multiply(X1,multiply(X0,X0))),
inference(superposition,[],[f2,f1274]) ).
fof(f1356,plain,
! [X0,X1] : multiply(n1,add(X1,X1)) = multiply(add(X1,X1),add(X0,n1)),
inference(superposition,[],[f1233,f137]) ).
fof(f1358,plain,
! [X0,X1] : multiply(add(X0,X0),add(X1,X1)) = multiply(add(X1,X1),add(X0,X0)),
inference(superposition,[],[f1233,f1146]) ).
fof(f1359,plain,
! [X2,X0,X1] : multiply(multiply(X1,X0),add(X2,X2)) = multiply(add(X2,X2),multiply(X0,add(X1,X1))),
inference(superposition,[],[f1233,f2]) ).
fof(f1360,plain,
! [X2,X0,X1] : multiply(inverse(X0),add(X2,X2)) = multiply(add(X2,X2),multiply(inverse(X0),add(X1,n1))),
inference(superposition,[],[f1233,f704]) ).
fof(f1374,plain,
! [X2,X0,X1] : multiply(add(add(X0,X1),add(X0,X1)),add(X1,add(X2,X2))) = add(add(multiply(add(X0,X1),X1),X1),multiply(add(X0,X1),add(X2,X2))),
inference(superposition,[],[f41,f1233]) ).
fof(f1380,plain,
! [X2,X0,X1] : multiply(add(X0,X0),add(add(X1,X1),X2)) = add(multiply(X0,add(X1,X1)),multiply(X2,add(X0,X0))),
inference(superposition,[],[f2,f1233]) ).
fof(f1381,plain,
! [X2,X0,X1] : multiply(add(X0,X0),add(X2,add(X1,X1))) = add(multiply(X2,add(X0,X0)),multiply(X0,add(X1,X1))),
inference(superposition,[],[f2,f1233]) ).
fof(f1387,plain,
! [X2,X0,X1] : multiply(add(add(X1,X1),add(X2,add(X0,X0))),add(add(X0,X0),add(X0,X0))) = add(add(multiply(X0,add(X1,X1)),add(X0,X0)),add(multiply(X0,add(X1,X1)),add(X0,X0))),
inference(superposition,[],[f978,f1233]) ).
fof(f1388,plain,
! [X2,X0,X1] : add(add(multiply(X0,add(X1,X1)),add(X0,X0)),add(multiply(X0,add(X1,X1)),add(X0,X0))) = multiply(add(add(X1,X1),add(X2,add(X0,X0))),add(X0,X0)),
inference(forward_demodulation,[],[f1387,f1146]) ).
fof(f1392,plain,
! [X2,X0,X1] : multiply(add(add(X0,X1),add(X0,X1)),add(X1,add(X2,X2))) = add(add(X1,X1),multiply(add(X0,X1),add(X2,X2))),
inference(forward_demodulation,[],[f1374,f1]) ).
fof(f1402,plain,
! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(add(X0,X0),add(X1,X1)),
inference(forward_demodulation,[],[f1358,f1233]) ).
fof(f1406,plain,
! [X0,X1] : multiply(n1,add(inverse(X0),inverse(X0))) = multiply(add(inverse(X0),inverse(X0)),add(X1,inverse(X0))),
inference(backward_demodulation,[],[f1296,f1356]) ).
fof(f1413,plain,
! [X0,X1] : add(X0,X0) = add(add(multiply(X0,add(X1,X1)),add(X0,X0)),add(multiply(X0,add(X1,X1)),add(X0,X0))),
inference(forward_demodulation,[],[f1388,f1313]) ).
fof(f1421,plain,
! [X0,X1] : add(inverse(X0),inverse(X0)) = multiply(add(inverse(X0),inverse(X0)),add(X1,inverse(X0))),
inference(forward_demodulation,[],[f1406,f103]) ).
fof(f1440,plain,
! [X0,X1] : multiply(X1,add(X0,n1)) = multiply(add(X1,X1),add(X0,n1)),
inference(superposition,[],[f1402,f137]) ).
fof(f1445,plain,
! [X0,X1] : multiply(X1,multiply(inverse(X0),add(n1,n1))) = multiply(add(X1,X1),multiply(inverse(X0),add(n1,n1))),
inference(superposition,[],[f1402,f186]) ).
fof(f1453,plain,
! [X0,X1] : multiply(X1,add(X0,X0)) = multiply(X0,add(X1,X1)),
inference(superposition,[],[f1233,f1402]) ).
fof(f1463,plain,
! [X0] : multiply(X0,add(X0,X0)) = multiply(add(add(X0,X0),add(X0,X0)),multiply(X0,add(X0,X0))),
inference(superposition,[],[f1274,f1402]) ).
fof(f1466,plain,
! [X2,X0,X1] : multiply(add(X1,X1),add(add(X0,X0),X2)) = add(multiply(X0,add(X1,X1)),multiply(X2,add(X1,X1))),
inference(superposition,[],[f2,f1402]) ).
fof(f1467,plain,
! [X2,X0,X1] : multiply(add(X1,X1),add(X2,add(X0,X0))) = add(multiply(X2,add(X1,X1)),multiply(X0,add(X1,X1))),
inference(superposition,[],[f2,f1402]) ).
fof(f1477,plain,
! [X2,X0,X1] : multiply(add(X1,X1),add(X2,add(X0,X0))) = multiply(add(X1,X1),add(X2,X0)),
inference(forward_demodulation,[],[f1467,f2]) ).
fof(f1478,plain,
! [X2,X0,X1] : multiply(add(X1,X1),add(add(X0,X0),X2)) = multiply(add(X1,X1),add(X0,X2)),
inference(forward_demodulation,[],[f1466,f2]) ).
fof(f1480,plain,
! [X0] : multiply(X0,add(X0,X0)) = multiply(multiply(X0,X0),add(add(X0,X0),add(X0,X0))),
inference(forward_demodulation,[],[f1463,f1359]) ).
fof(f1492,plain,
! [X0,X1] : multiply(inverse(X0),add(X1,X1)) = multiply(X1,multiply(inverse(X0),add(n1,n1))),
inference(forward_demodulation,[],[f1445,f1360]) ).
fof(f1497,plain,
! [X2,X0,X1] : add(multiply(X2,add(X0,X0)),multiply(X0,add(X1,X1))) = multiply(add(X0,X0),add(X2,X1)),
inference(backward_demodulation,[],[f1381,f1477]) ).
fof(f1499,plain,
! [X2,X0,X1] : add(add(X1,X1),multiply(add(X0,X1),add(X2,X2))) = multiply(add(add(X0,X1),add(X0,X1)),add(X1,X2)),
inference(backward_demodulation,[],[f1392,f1477]) ).
fof(f1500,plain,
! [X2,X0,X1] : add(multiply(X0,add(X1,X1)),multiply(X2,add(X0,X0))) = multiply(add(X0,X0),add(X1,X2)),
inference(backward_demodulation,[],[f1380,f1478]) ).
fof(f1501,plain,
! [X0] : multiply(multiply(X0,X0),add(X0,X0)) = multiply(X0,add(X0,X0)),
inference(forward_demodulation,[],[f1480,f1146]) ).
fof(f1511,plain,
! [X0] : add(X0,X0) = multiply(multiply(X0,X0),add(X0,X0)),
inference(forward_demodulation,[],[f1501,f1227]) ).
fof(f1545,plain,
! [X0,X1] : add(add(X0,X0),multiply(X1,add(X0,X0))) = multiply(add(X0,X0),add(multiply(X0,X0),X1)),
inference(superposition,[],[f2,f1511]) ).
fof(f1546,plain,
! [X0,X1] : add(multiply(X1,add(X0,X0)),add(X0,X0)) = multiply(add(X0,X0),add(X1,multiply(X0,X0))),
inference(superposition,[],[f2,f1511]) ).
fof(f1556,plain,
! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = multiply(add(X0,X0),add(X1,multiply(X0,X0))),
inference(forward_demodulation,[],[f1546,f1278]) ).
fof(f1557,plain,
! [X0,X1] : multiply(add(X0,X0),add(X0,X1)) = multiply(add(X0,X0),add(multiply(X0,X0),X1)),
inference(forward_demodulation,[],[f1545,f1228]) ).
fof(f1564,plain,
! [X0] : add(X0,multiply(X0,X0)) = multiply(add(X0,X0),add(X0,X0)),
inference(backward_demodulation,[],[f223,f1556]) ).
fof(f1569,plain,
! [X0] : add(X0,X0) = add(X0,multiply(X0,X0)),
inference(forward_demodulation,[],[f1564,f86]) ).
fof(f1609,plain,
! [X0] : add(multiply(X0,X0),multiply(inverse(multiply(X0,X0)),multiply(X0,X0))) = multiply(add(X0,X0),add(multiply(X0,X0),multiply(inverse(multiply(X0,X0)),multiply(X0,X0)))),
inference(superposition,[],[f115,f1569]) ).
fof(f1616,plain,
! [X0] : add(multiply(X0,X0),multiply(inverse(multiply(X0,X0)),multiply(X0,X0))) = multiply(add(X0,X0),add(X0,multiply(inverse(multiply(X0,X0)),multiply(X0,X0)))),
inference(forward_demodulation,[],[f1609,f1557]) ).
fof(f1629,plain,
! [X0] : multiply(add(X0,X0),add(X0,multiply(inverse(multiply(X0,X0)),multiply(X0,X0)))) = multiply(multiply(X0,X0),add(add(X0,X0),inverse(multiply(X0,X0)))),
inference(forward_demodulation,[],[f1616,f1326]) ).
fof(f1774,plain,
! [X0,X1] : multiply(X1,add(X0,n1)) = multiply(n1,add(X1,X1)),
inference(superposition,[],[f1453,f137]) ).
fof(f1777,plain,
! [X2,X0,X1] : multiply(X2,multiply(X0,add(X1,X1))) = multiply(multiply(X1,X0),add(X2,X2)),
inference(superposition,[],[f1453,f2]) ).
fof(f1872,plain,
! [X0] : multiply(add(inverse(X0),inverse(X0)),inverse(X0)) = multiply(add(inverse(X0),inverse(X0)),add(inverse(X0),multiply(inverse(X0),add(inverse(X0),inverse(X0))))),
inference(superposition,[],[f1557,f16]) ).
fof(f1928,plain,
! [X0] : multiply(add(inverse(X0),inverse(X0)),inverse(X0)) = multiply(add(inverse(X0),inverse(X0)),add(n1,multiply(inverse(X0),add(inverse(X0),inverse(X0))))),
inference(forward_demodulation,[],[f1872,f1247]) ).
fof(f1938,plain,
! [X0] : multiply(add(inverse(X0),inverse(X0)),inverse(X0)) = multiply(add(inverse(X0),inverse(X0)),add(n1,add(inverse(X0),inverse(X0)))),
inference(forward_demodulation,[],[f1928,f1227]) ).
fof(f1948,plain,
! [X0] : multiply(add(inverse(X0),inverse(X0)),inverse(X0)) = multiply(add(inverse(X0),inverse(X0)),add(n1,inverse(X0))),
inference(forward_demodulation,[],[f1938,f1295]) ).
fof(f1958,plain,
! [X0] : add(inverse(X0),inverse(X0)) = multiply(add(inverse(X0),inverse(X0)),inverse(X0)),
inference(forward_demodulation,[],[f1948,f1421]) ).
fof(f1963,plain,
! [X0] : inverse(X0) = add(inverse(X0),inverse(X0)),
inference(forward_demodulation,[],[f1958,f1]) ).
fof(f1972,plain,
! [X0,X1] : inverse(X1) = multiply(inverse(X1),add(X0,n1)),
inference(backward_demodulation,[],[f704,f1963]) ).
fof(f1993,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(X0),add(X1,inverse(X0))),
inference(backward_demodulation,[],[f1421,f1963]) ).
fof(f2037,plain,
! [X2,X3,X0] : multiply(add(X2,inverse(X0)),add(inverse(X0),X3)) = add(multiply(inverse(X0),add(X2,n1)),multiply(X3,add(X2,inverse(X0)))),
inference(backward_demodulation,[],[f1006,f1972]) ).
fof(f2055,plain,
! [X0,X1] : multiply(X1,inverse(X0)) = multiply(inverse(X0),add(X1,X1)),
inference(backward_demodulation,[],[f1492,f1972]) ).
fof(f2082,plain,
! [X2,X3,X0] : multiply(add(X2,inverse(X0)),add(inverse(X0),X3)) = add(inverse(X0),multiply(X3,add(X2,inverse(X0)))),
inference(forward_demodulation,[],[f2037,f1972]) ).
fof(f2102,plain,
! [X0] : n1 = multiply(add(n1,inverse(X0)),add(inverse(X0),n1)),
inference(backward_demodulation,[],[f74,f2082]) ).
fof(f2103,plain,
! [X0] : n1 = multiply(add(n1,inverse(X0)),add(inverse(X0),X0)),
inference(backward_demodulation,[],[f73,f2082]) ).
fof(f2283,plain,
! [X2,X0,X1] : multiply(multiply(X1,X0),inverse(X2)) = multiply(inverse(X2),multiply(X0,add(X1,X1))),
inference(superposition,[],[f2055,f2]) ).
fof(f2525,plain,
! [X0] : inverse(X0) = multiply(inverse(X0),n1),
inference(superposition,[],[f1993,f3]) ).
fof(f2576,plain,
! [X0] : inverse(X0) = add(inverse(n1),inverse(X0)),
inference(superposition,[],[f72,f2525]) ).
fof(f2583,plain,
! [X0,X1] : multiply(n1,add(inverse(X0),X1)) = add(inverse(X0),multiply(X1,n1)),
inference(superposition,[],[f2,f2525]) ).
fof(f2595,plain,
! [X0] : multiply(n1,add(inverse(n1),X0)) = X0,
inference(backward_demodulation,[],[f72,f2583]) ).
fof(f2611,plain,
! [X0] : inverse(n1) = add(multiply(inverse(n1),inverse(X0)),multiply(X0,inverse(X0))),
inference(superposition,[],[f15,f2576]) ).
fof(f2662,plain,
! [X0] : inverse(n1) = multiply(inverse(X0),add(inverse(n1),X0)),
inference(forward_demodulation,[],[f2611,f2]) ).
fof(f2677,plain,
! [X0] : n1 = multiply(n1,add(X0,n1)),
inference(superposition,[],[f2595,f137]) ).
fof(f2703,plain,
! [X0] : n1 = add(X0,n1),
inference(backward_demodulation,[],[f1265,f2677]) ).
fof(f2716,plain,
! [X1] : multiply(X1,n1) = multiply(add(X1,X1),n1),
inference(backward_demodulation,[],[f1440,f2703]) ).
fof(f2717,plain,
! [X1] : multiply(X1,n1) = multiply(n1,add(X1,X1)),
inference(backward_demodulation,[],[f1774,f2703]) ).
fof(f2736,plain,
! [X0] : n1 = multiply(add(n1,inverse(X0)),n1),
inference(backward_demodulation,[],[f2102,f2703]) ).
fof(f2892,plain,
! [X0,X1] : add(multiply(X1,inverse(X1)),multiply(X0,n1)) = add(X0,X0),
inference(superposition,[],[f17,f2716]) ).
fof(f2917,plain,
! [X0] : add(X0,X0) = X0,
inference(forward_demodulation,[],[f2892,f17]) ).
fof(f2947,plain,
! [X2,X0,X1] : add(add(multiply(X0,X1),X1),add(multiply(X0,X1),X1)) = multiply(add(X0,add(X2,X1)),X1),
inference(backward_demodulation,[],[f978,f2917]) ).
fof(f2984,plain,
! [X0] : multiply(X0,X0) = X0,
inference(backward_demodulation,[],[f1227,f2917]) ).
fof(f2985,plain,
! [X0,X1] : add(X0,multiply(X1,X0)) = multiply(X0,add(X0,X1)),
inference(backward_demodulation,[],[f1228,f2917]) ).
fof(f2989,plain,
! [X2,X0,X1] : multiply(X0,add(add(X1,X0),X2)) = multiply(X0,add(X0,X2)),
inference(backward_demodulation,[],[f1245,f2917]) ).
fof(f2997,plain,
! [X0,X1] : add(multiply(X1,X0),X0) = multiply(X0,add(X1,X0)),
inference(backward_demodulation,[],[f1278,f2917]) ).
fof(f3004,plain,
! [X0,X1] : multiply(add(add(X0,X1),add(X0,X1)),add(X1,add(X0,X1))) = add(X1,add(add(X0,X1),add(X0,X1))),
inference(backward_demodulation,[],[f1299,f2917]) ).
fof(f3005,plain,
! [X2,X0,X1] : multiply(add(X1,add(X2,X0)),X0) = X0,
inference(backward_demodulation,[],[f1313,f2917]) ).
fof(f3022,plain,
! [X0,X1] : add(X0,X0) = add(add(multiply(X0,X1),add(X0,X0)),add(multiply(X0,X1),add(X0,X0))),
inference(backward_demodulation,[],[f1413,f2917]) ).
fof(f3025,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,add(X0,X0)),
inference(backward_demodulation,[],[f1453,f2917]) ).
fof(f3032,plain,
! [X2,X0,X1] : multiply(add(X0,X0),add(X2,X1)) = add(multiply(X2,add(X0,X0)),multiply(X0,X1)),
inference(backward_demodulation,[],[f1497,f2917]) ).
fof(f3034,plain,
! [X2,X0,X1] : multiply(add(add(X0,X1),add(X0,X1)),add(X1,X2)) = add(X1,multiply(add(X0,X1),add(X2,X2))),
inference(backward_demodulation,[],[f1499,f2917]) ).
fof(f3035,plain,
! [X2,X0,X1] : multiply(add(X0,X0),add(X1,X2)) = add(multiply(X0,X1),multiply(X2,add(X0,X0))),
inference(backward_demodulation,[],[f1500,f2917]) ).
fof(f3048,plain,
! [X0] : multiply(X0,add(X0,multiply(inverse(multiply(X0,X0)),multiply(X0,X0)))) = multiply(multiply(X0,X0),add(X0,inverse(multiply(X0,X0)))),
inference(backward_demodulation,[],[f1629,f2917]) ).
fof(f3069,plain,
! [X2,X0,X1] : multiply(X2,multiply(X0,X1)) = multiply(multiply(X1,X0),add(X2,X2)),
inference(backward_demodulation,[],[f1777,f2917]) ).
fof(f3087,plain,
! [X0,X1] : multiply(inverse(X0),X1) = multiply(X1,inverse(X0)),
inference(backward_demodulation,[],[f2055,f2917]) ).
fof(f3094,plain,
! [X2,X0,X1] : multiply(multiply(X1,X0),inverse(X2)) = multiply(inverse(X2),multiply(X0,X1)),
inference(backward_demodulation,[],[f2283,f2917]) ).
fof(f3110,plain,
! [X1] : multiply(X1,n1) = multiply(n1,X1),
inference(backward_demodulation,[],[f2717,f2917]) ).
fof(f3164,plain,
! [X2,X0,X1] : multiply(X2,multiply(X0,X1)) = multiply(multiply(X1,X0),X2),
inference(forward_demodulation,[],[f3069,f2917]) ).
fof(f3168,plain,
! [X0] : multiply(multiply(X0,X0),add(X0,inverse(multiply(X0,X0)))) = multiply(X0,add(X0,multiply(multiply(X0,X0),inverse(multiply(X0,X0))))),
inference(forward_demodulation,[],[f3048,f3094]) ).
fof(f3170,plain,
! [X2,X0,X1] : multiply(X0,add(X1,X2)) = add(multiply(X0,X1),multiply(X2,X0)),
inference(forward_demodulation,[],[f3035,f2917]) ).
fof(f3171,plain,
! [X2,X0,X1] : multiply(add(add(X0,X1),add(X0,X1)),add(X1,X2)) = add(X1,multiply(add(X0,X1),X2)),
inference(forward_demodulation,[],[f3034,f2917]) ).
fof(f3173,plain,
! [X2,X0,X1] : multiply(X0,add(X2,X1)) = add(multiply(X2,X0),multiply(X0,X1)),
inference(forward_demodulation,[],[f3032,f2917]) ).
fof(f3178,plain,
! [X0,X1] : multiply(X1,X0) = multiply(X0,X1),
inference(forward_demodulation,[],[f3025,f2917]) ).
fof(f3180,plain,
! [X0,X1] : add(X0,X0) = add(multiply(X0,X1),add(X0,X0)),
inference(forward_demodulation,[],[f3022,f2917]) ).
fof(f3191,plain,
! [X0,X1] : add(X1,add(X0,X1)) = multiply(add(X0,X1),add(X1,add(X0,X1))),
inference(forward_demodulation,[],[f3004,f2917]) ).
fof(f3221,plain,
! [X0,X1] : multiply(multiply(X0,n1),add(X1,X0)) = multiply(multiply(X0,n1),add(X1,multiply(X0,n1))),
inference(backward_demodulation,[],[f35,f2997]) ).
fof(f3255,plain,
! [X2,X0,X1] : multiply(multiply(X1,add(X1,inverse(X1))),X2) = multiply(multiply(X2,add(X0,X1)),multiply(multiply(X1,add(X1,inverse(X1))),X2)),
inference(backward_demodulation,[],[f463,f2985]) ).
fof(f3332,plain,
! [X0,X1] : add(add(multiply(X0,X1),X1),add(multiply(X0,X1),X1)) = X1,
inference(forward_demodulation,[],[f2947,f3005]) ).
fof(f3352,plain,
! [X0] : multiply(X0,add(X0,inverse(X0))) = multiply(X0,add(X0,multiply(X0,inverse(X0)))),
inference(forward_demodulation,[],[f3168,f2984]) ).
fof(f3355,plain,
! [X2,X0,X1] : add(X1,multiply(add(X0,X1),X2)) = multiply(add(X0,X1),add(X1,X2)),
inference(forward_demodulation,[],[f3171,f2917]) ).
fof(f3358,plain,
! [X0,X1] : add(multiply(X0,X1),X0) = X0,
inference(forward_demodulation,[],[f3180,f2917]) ).
fof(f3401,plain,
! [X2,X0,X1] : multiply(multiply(X1,n1),X2) = multiply(multiply(X2,add(X0,X1)),multiply(multiply(X1,n1),X2)),
inference(forward_demodulation,[],[f3255,f3]) ).
fof(f3440,plain,
! [X0,X1] : add(multiply(X0,X1),X1) = X1,
inference(forward_demodulation,[],[f3332,f2917]) ).
fof(f3458,plain,
! [X0] : multiply(X0,n1) = multiply(X0,add(X0,multiply(X0,inverse(X0)))),
inference(forward_demodulation,[],[f3352,f3]) ).
fof(f3491,plain,
! [X2,X0,X1] : multiply(multiply(X1,n1),X2) = multiply(multiply(X2,multiply(X1,n1)),multiply(X2,add(X0,X1))),
inference(forward_demodulation,[],[f3401,f3164]) ).
fof(f3520,plain,
! [X0,X1] : multiply(X0,add(X1,X0)) = X0,
inference(backward_demodulation,[],[f2997,f3440]) ).
fof(f3601,plain,
! [X0,X1] : add(X0,X1) = add(X1,add(X0,X1)),
inference(backward_demodulation,[],[f3191,f3520]) ).
fof(f3609,plain,
! [X0,X1] : multiply(X0,n1) = multiply(multiply(X0,n1),add(X1,X0)),
inference(backward_demodulation,[],[f3221,f3520]) ).
fof(f3665,plain,
! [X2,X3,X0] : multiply(add(X2,multiply(X0,n1)),add(multiply(X0,n1),X3)) = add(multiply(multiply(X0,n1),add(X2,X0)),multiply(X3,add(X2,multiply(X0,n1)))),
inference(backward_demodulation,[],[f1013,f3609]) ).
fof(f3708,plain,
! [X2,X3,X0] : multiply(add(X2,multiply(X0,n1)),add(multiply(X0,n1),X3)) = add(multiply(X0,n1),multiply(X3,add(X2,multiply(X0,n1)))),
inference(forward_demodulation,[],[f3665,f3609]) ).
fof(f3782,plain,
! [X0] : multiply(X0,n1) = X0,
inference(superposition,[],[f17,f3358]) ).
fof(f3824,plain,
! [X1] : multiply(n1,X1) = X1,
inference(backward_demodulation,[],[f3110,f3782]) ).
fof(f3835,plain,
! [X0] : multiply(X0,add(X0,multiply(X0,inverse(X0)))) = X0,
inference(backward_demodulation,[],[f3458,f3782]) ).
fof(f3840,plain,
! [X2,X0,X1] : multiply(X1,X2) = multiply(multiply(X2,X1),multiply(X2,add(X0,X1))),
inference(backward_demodulation,[],[f3491,f3782]) ).
fof(f3851,plain,
! [X2,X3,X0] : multiply(add(X2,X0),add(X0,X3)) = add(X0,multiply(X3,add(X2,X0))),
inference(backward_demodulation,[],[f3708,f3782]) ).
fof(f3867,plain,
! [X0] : n1 = add(n1,inverse(X0)),
inference(backward_demodulation,[],[f2736,f3782]) ).
fof(f3884,plain,
! [X0] : n1 = multiply(n1,add(inverse(X0),X0)),
inference(backward_demodulation,[],[f2103,f3867]) ).
fof(f3905,plain,
! [X0] : add(inverse(n1),X0) = X0,
inference(backward_demodulation,[],[f2595,f3824]) ).
fof(f3939,plain,
! [X0] : n1 = add(inverse(X0),X0),
inference(forward_demodulation,[],[f3884,f3824]) ).
fof(f3949,plain,
! [X0] : multiply(inverse(X0),X0) = inverse(n1),
inference(backward_demodulation,[],[f2662,f3905]) ).
fof(f3978,plain,
! [X0] : multiply(X0,inverse(X0)) = inverse(n1),
inference(forward_demodulation,[],[f3949,f3178]) ).
fof(f3997,plain,
! [X0] : multiply(X0,add(X0,inverse(n1))) = X0,
inference(backward_demodulation,[],[f3835,f3978]) ).
fof(f4015,plain,
! [X0] : add(X0,inverse(n1)) = multiply(X0,add(X0,inverse(n1))),
inference(superposition,[],[f33,f3824]) ).
fof(f4024,plain,
! [X0] : add(X0,inverse(n1)) = X0,
inference(forward_demodulation,[],[f4015,f3997]) ).
fof(f4056,plain,
! [X2,X0,X1] : multiply(add(X1,X0),add(X2,X0)) = add(multiply(X2,add(X1,X0)),X0),
inference(superposition,[],[f2,f3520]) ).
fof(f4164,plain,
! [X0,X1] : add(multiply(inverse(X0),X1),multiply(X1,add(X1,inverse(X0)))) = X1,
inference(superposition,[],[f16,f3178]) ).
fof(f4166,plain,
! [X0,X1] : multiply(X1,add(inverse(X0),add(X1,inverse(X0)))) = X1,
inference(forward_demodulation,[],[f4164,f3173]) ).
fof(f4170,plain,
! [X0,X1] : multiply(X1,add(X1,inverse(X0))) = X1,
inference(forward_demodulation,[],[f4166,f3601]) ).
fof(f4193,plain,
! [X0,X1] : multiply(inverse(X0),add(X0,X1)) = add(inverse(n1),multiply(X1,inverse(X0))),
inference(superposition,[],[f2,f3978]) ).
fof(f4194,plain,
! [X0,X1] : multiply(inverse(X0),add(X1,X0)) = add(multiply(X1,inverse(X0)),inverse(n1)),
inference(superposition,[],[f2,f3978]) ).
fof(f4199,plain,
! [X0,X1] : multiply(X1,inverse(X0)) = multiply(inverse(X0),add(X1,X0)),
inference(forward_demodulation,[],[f4194,f4024]) ).
fof(f4200,plain,
! [X0,X1] : multiply(X1,inverse(X0)) = multiply(inverse(X0),add(X0,X1)),
inference(forward_demodulation,[],[f4193,f3905]) ).
fof(f4226,plain,
! [X0,X1] : multiply(X0,X1) = multiply(multiply(X1,n1),multiply(X0,X1)),
inference(superposition,[],[f20,f3939]) ).
fof(f4230,plain,
! [X0] : inverse(inverse(X0)) = add(multiply(inverse(inverse(X0)),inverse(X0)),multiply(X0,n1)),
inference(superposition,[],[f15,f3939]) ).
fof(f4231,plain,
! [X0] : inverse(inverse(X0)) = add(multiply(inverse(inverse(X0)),inverse(X0)),X0),
inference(forward_demodulation,[],[f4230,f3782]) ).
fof(f4233,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,multiply(X0,X1)),
inference(forward_demodulation,[],[f4226,f3782]) ).
fof(f4234,plain,
! [X0] : inverse(inverse(X0)) = add(multiply(inverse(X0),inverse(inverse(X0))),X0),
inference(forward_demodulation,[],[f4231,f3087]) ).
fof(f4238,plain,
! [X0] : inverse(inverse(X0)) = add(inverse(n1),X0),
inference(forward_demodulation,[],[f4234,f3978]) ).
fof(f4240,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[],[f4238,f3905]) ).
fof(f4322,plain,
! [X0,X1] : multiply(X0,add(X0,X1)) = add(X0,multiply(X0,X1)),
inference(superposition,[],[f3355,f3905]) ).
fof(f4543,plain,
! [X0,X1] : multiply(X1,add(X1,X0)) = X1,
inference(superposition,[],[f4170,f4240]) ).
fof(f4555,plain,
! [X2,X0,X1] : multiply(add(X0,inverse(X1)),add(X0,X2)) = add(X0,multiply(X2,add(X0,inverse(X1)))),
inference(superposition,[],[f2,f4170]) ).
fof(f4571,plain,
! [X0,X1] : add(X0,multiply(X1,X0)) = X0,
inference(backward_demodulation,[],[f2985,f4543]) ).
fof(f4573,plain,
! [X2,X0,X1] : multiply(X0,add(add(X1,X0),X2)) = X0,
inference(backward_demodulation,[],[f2989,f4543]) ).
fof(f4587,plain,
! [X0,X1] : add(X0,multiply(X0,X1)) = X0,
inference(backward_demodulation,[],[f4322,f4543]) ).
fof(f4670,plain,
! [X0,X1] : add(X1,multiply(X0,add(X1,inverse(X0)))) = X1,
inference(superposition,[],[f4587,f33]) ).
fof(f4700,plain,
! [X0,X1] : multiply(add(X1,inverse(X0)),add(X1,X0)) = X1,
inference(forward_demodulation,[],[f4670,f4555]) ).
fof(f4701,plain,
! [X0,X1] : multiply(add(X1,X0),add(X1,inverse(X0))) = X1,
inference(forward_demodulation,[],[f4700,f3178]) ).
fof(f4721,plain,
! [X2,X0,X1] : multiply(add(X0,X1),add(X2,X0)) = add(multiply(X2,add(X0,X1)),X0),
inference(superposition,[],[f2,f4543]) ).
fof(f4726,plain,
! [X0,X1] : add(X0,X1) = add(add(X0,X1),X0),
inference(superposition,[],[f4571,f4543]) ).
fof(f4774,plain,
! [X2,X0,X1] : multiply(X0,X1) = multiply(multiply(X0,X1),add(X0,X2)),
inference(superposition,[],[f4573,f4587]) ).
fof(f4888,plain,
! [X0,X1] : multiply(X1,X0) = multiply(X0,add(X1,inverse(X0))),
inference(superposition,[],[f4199,f4240]) ).
fof(f4899,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(multiply(X1,X0),inverse(X0)),
inference(superposition,[],[f4199,f3440]) ).
fof(f4923,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X0),multiply(X0,X1)),
inference(forward_demodulation,[],[f4899,f3094]) ).
fof(f4946,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(inverse(X0),multiply(X0,X1)),
inference(forward_demodulation,[],[f4923,f3178]) ).
fof(f4957,plain,
! [X0,X1] : inverse(n1) = multiply(inverse(X0),multiply(X0,X1)),
inference(forward_demodulation,[],[f4946,f3978]) ).
fof(f4994,plain,
! [X2,X0,X1] : multiply(add(X0,X1),add(X0,X2)) = add(X0,multiply(add(X0,X1),X2)),
inference(superposition,[],[f3355,f4726]) ).
fof(f5093,plain,
! [X0,X1] : multiply(X1,X0) = multiply(X0,add(inverse(X0),X1)),
inference(superposition,[],[f4200,f4240]) ).
fof(f5171,plain,
! [X0,X1] : multiply(inverse(X0),add(X1,X0)) = add(multiply(inverse(X0),X1),inverse(n1)),
inference(superposition,[],[f3170,f3978]) ).
fof(f5226,plain,
! [X0,X1] : multiply(inverse(X0),X1) = multiply(inverse(X0),add(X1,X0)),
inference(forward_demodulation,[],[f5171,f4024]) ).
fof(f6141,plain,
! [X2,X0,X1] : add(multiply(X2,add(X0,X1)),X0) = multiply(add(X0,X1),add(X2,add(X0,inverse(X1)))),
inference(superposition,[],[f3173,f4701]) ).
fof(f6152,plain,
! [X0,X1] : add(X1,X0) = multiply(add(X0,X1),add(X1,add(X0,inverse(X1)))),
inference(superposition,[],[f3355,f4701]) ).
fof(f6156,plain,
! [X2,X0,X1] : multiply(add(X0,X1),add(X2,X0)) = multiply(add(X0,X1),add(X2,add(X0,inverse(X1)))),
inference(forward_demodulation,[],[f6141,f4721]) ).
fof(f6187,plain,
! [X0,X1] : add(X1,X0) = multiply(add(X0,X1),add(X1,X0)),
inference(backward_demodulation,[],[f6152,f6156]) ).
fof(f6250,plain,
! [X2,X0,X1] : multiply(X2,add(X0,X1)) = multiply(multiply(add(X0,X1),add(X1,X0)),X2),
inference(superposition,[],[f3164,f6187]) ).
fof(f6272,plain,
! [X2,X0,X1] : multiply(X2,add(X0,X1)) = multiply(add(X1,X0),X2),
inference(forward_demodulation,[],[f6250,f6187]) ).
fof(f6585,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(multiply(X1,inverse(X0)),X0),
inference(superposition,[],[f5093,f4571]) ).
fof(f6648,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(X0,multiply(inverse(X0),X1)),
inference(forward_demodulation,[],[f6585,f3164]) ).
fof(f6659,plain,
! [X0,X1] : inverse(n1) = multiply(X0,multiply(inverse(X0),X1)),
inference(forward_demodulation,[],[f6648,f3978]) ).
fof(f6910,plain,
! [X2,X0,X1] : multiply(add(X0,X1),X2) = multiply(add(X1,X0),X2),
inference(superposition,[],[f3178,f6272]) ).
fof(f6934,plain,
! [X2,X3,X0,X1] : multiply(X3,multiply(X0,add(X1,X2))) = multiply(multiply(X0,add(X2,X1)),X3),
inference(superposition,[],[f3164,f6272]) ).
fof(f6940,plain,
! [X2,X0,X1] : multiply(X0,add(X1,X2)) = multiply(X0,add(X2,X1)),
inference(superposition,[],[f3178,f6272]) ).
fof(f6958,plain,
! [X0,X1] : add(X1,X0) = multiply(n1,add(X0,X1)),
inference(superposition,[],[f3782,f6272]) ).
fof(f6959,plain,
! [X0,X1] : add(X0,X1) = add(X1,X0),
inference(forward_demodulation,[],[f6958,f3824]) ).
fof(f7815,plain,
! [X2,X0,X1] : multiply(add(X1,X0),add(X0,X2)) = add(X0,multiply(add(X0,X1),X2)),
inference(superposition,[],[f3355,f6910]) ).
fof(f8493,plain,
! [X0,X1] : add(multiply(X0,X1),inverse(X1)) = multiply(add(X0,inverse(X1)),add(X1,inverse(X1))),
inference(superposition,[],[f4056,f4888]) ).
fof(f8513,plain,
! [X0,X1] : add(multiply(inverse(X0),X1),X0) = multiply(add(X1,X0),add(inverse(X0),X0)),
inference(superposition,[],[f4056,f5226]) ).
fof(f8614,plain,
! [X0,X1] : add(multiply(inverse(X0),X1),X0) = multiply(add(X1,X0),add(X0,inverse(X0))),
inference(forward_demodulation,[],[f8513,f6940]) ).
fof(f8631,plain,
! [X0,X1] : multiply(add(X0,inverse(X1)),n1) = add(multiply(X0,X1),inverse(X1)),
inference(forward_demodulation,[],[f8493,f3]) ).
fof(f8667,plain,
! [X0,X1] : multiply(add(X1,X0),n1) = add(multiply(inverse(X0),X1),X0),
inference(forward_demodulation,[],[f8614,f3]) ).
fof(f8675,plain,
! [X0,X1] : multiply(add(X0,inverse(X1)),n1) = add(inverse(X1),multiply(X0,X1)),
inference(forward_demodulation,[],[f8631,f6959]) ).
fof(f8685,plain,
! [X0,X1] : multiply(add(X1,X0),n1) = add(X0,multiply(inverse(X0),X1)),
inference(forward_demodulation,[],[f8667,f6959]) ).
fof(f8688,plain,
! [X0,X1] : add(inverse(X1),multiply(X0,X1)) = multiply(n1,add(inverse(X1),X0)),
inference(forward_demodulation,[],[f8675,f6272]) ).
fof(f8692,plain,
! [X0,X1] : multiply(n1,add(X0,X1)) = add(X0,multiply(inverse(X0),X1)),
inference(forward_demodulation,[],[f8685,f6272]) ).
fof(f8693,plain,
! [X0,X1] : add(inverse(X1),X0) = add(inverse(X1),multiply(X0,X1)),
inference(forward_demodulation,[],[f8688,f3824]) ).
fof(f8695,plain,
! [X0,X1] : add(X0,X1) = add(X0,multiply(inverse(X0),X1)),
inference(forward_demodulation,[],[f8692,f3824]) ).
fof(f8696,plain,
! [X0,X1] : add(inverse(X0),X1) = add(inverse(X0),multiply(X0,X1)),
inference(superposition,[],[f8695,f4240]) ).
fof(f8979,plain,
! [X0,X1] : add(inverse(add(X0,inverse(X1))),X1) = add(inverse(add(X0,inverse(X1))),multiply(X0,X1)),
inference(superposition,[],[f8693,f4888]) ).
fof(f8986,plain,
! [X0,X1] : add(inverse(X0),X0) = add(inverse(X0),add(X1,X0)),
inference(superposition,[],[f8693,f1]) ).
fof(f9094,plain,
! [X0,X1] : add(X0,inverse(X0)) = add(inverse(X0),add(X1,X0)),
inference(forward_demodulation,[],[f8986,f6959]) ).
fof(f9099,plain,
! [X0,X1] : add(inverse(add(X0,inverse(X1))),X1) = add(multiply(X0,X1),inverse(add(X0,inverse(X1)))),
inference(forward_demodulation,[],[f8979,f6959]) ).
fof(f9129,plain,
! [X0,X1] : n1 = add(inverse(X0),add(X1,X0)),
inference(forward_demodulation,[],[f9094,f3]) ).
fof(f9134,plain,
! [X0,X1] : add(multiply(X0,X1),inverse(add(X0,inverse(X1)))) = add(X1,inverse(add(X0,inverse(X1)))),
inference(forward_demodulation,[],[f9099,f6959]) ).
fof(f9228,plain,
! [X0,X1] : inverse(X0) = multiply(n1,add(inverse(X0),inverse(add(X1,X0)))),
inference(superposition,[],[f4701,f9129]) ).
fof(f9253,plain,
! [X0,X1] : inverse(X0) = add(inverse(X0),inverse(add(X1,X0))),
inference(forward_demodulation,[],[f9228,f3824]) ).
fof(f11344,plain,
! [X0,X1] : add(X0,inverse(add(X1,inverse(X0)))) = X0,
inference(superposition,[],[f9253,f4240]) ).
fof(f11461,plain,
! [X0,X1] : add(multiply(X0,X1),inverse(add(X0,inverse(X1)))) = X1,
inference(backward_demodulation,[],[f9134,f11344]) ).
fof(f11490,plain,
! [X0,X1] : add(X0,inverse(X1)) = add(multiply(X0,X1),inverse(add(X1,inverse(add(X0,inverse(X1)))))),
inference(superposition,[],[f11461,f4888]) ).
fof(f11673,plain,
! [X0,X1] : add(X0,inverse(X1)) = add(multiply(X0,X1),inverse(X1)),
inference(forward_demodulation,[],[f11490,f11344]) ).
fof(f11732,plain,
! [X0,X1] : add(X0,inverse(X1)) = add(inverse(X1),multiply(X0,X1)),
inference(forward_demodulation,[],[f11673,f6959]) ).
fof(f15657,plain,
! [X2,X0,X1] : add(inverse(X0),multiply(X0,multiply(X1,X2))) = add(multiply(X2,X1),inverse(X0)),
inference(superposition,[],[f11732,f3164]) ).
fof(f15784,plain,
! [X2,X0,X1] : add(inverse(X0),multiply(X1,X2)) = add(multiply(X2,X1),inverse(X0)),
inference(forward_demodulation,[],[f15657,f8696]) ).
fof(f16527,plain,
! [X2,X0,X1] : add(X2,multiply(X0,X1)) = multiply(add(X0,X2),add(X2,multiply(X0,X1))),
inference(superposition,[],[f3851,f4774]) ).
fof(f18398,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),add(inverse(X0),X2)) = add(inverse(n1),multiply(multiply(X0,X1),X2)),
inference(superposition,[],[f3173,f4957]) ).
fof(f18443,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(multiply(X0,X1),add(inverse(X0),X2)),
inference(forward_demodulation,[],[f18398,f3905]) ).
fof(f24326,plain,
! [X2,X0,X1] : multiply(multiply(inverse(X0),X1),add(X0,X2)) = add(inverse(n1),multiply(X2,multiply(inverse(X0),X1))),
inference(superposition,[],[f2,f6659]) ).
fof(f24327,plain,
! [X2,X0,X1] : multiply(multiply(inverse(X0),X1),add(X2,X0)) = add(multiply(X2,multiply(inverse(X0),X1)),inverse(n1)),
inference(superposition,[],[f2,f6659]) ).
fof(f24338,plain,
! [X2,X0,X1] : multiply(multiply(inverse(X0),X1),add(X2,X0)) = add(multiply(multiply(inverse(X0),X1),X2),inverse(n1)),
inference(superposition,[],[f3170,f6659]) ).
fof(f24415,plain,
! [X2,X0,X1] : add(inverse(n1),multiply(X2,multiply(inverse(X0),X1))) = multiply(multiply(inverse(X0),X1),add(X2,X0)),
inference(forward_demodulation,[],[f24338,f15784]) ).
fof(f24422,plain,
! [X2,X0,X1] : multiply(multiply(inverse(X0),X1),add(X2,X0)) = add(inverse(n1),multiply(multiply(inverse(X0),X1),X2)),
inference(forward_demodulation,[],[f24327,f15784]) ).
fof(f24423,plain,
! [X2,X0,X1] : multiply(X2,multiply(inverse(X0),X1)) = multiply(multiply(inverse(X0),X1),add(X0,X2)),
inference(forward_demodulation,[],[f24326,f3905]) ).
fof(f24447,plain,
! [X2,X0,X1] : multiply(X2,multiply(inverse(X0),X1)) = multiply(multiply(inverse(X0),X1),add(X2,X0)),
inference(forward_demodulation,[],[f24415,f3905]) ).
fof(f24454,plain,
! [X2,X0,X1] : multiply(multiply(inverse(X0),X1),X2) = multiply(multiply(inverse(X0),X1),add(X2,X0)),
inference(forward_demodulation,[],[f24422,f3905]) ).
fof(f24581,plain,
! [X2,X0,X1] : multiply(add(X2,X0),add(X0,multiply(inverse(X0),X1))) = add(X0,multiply(multiply(inverse(X0),X1),X2)),
inference(superposition,[],[f3851,f24454]) ).
fof(f24681,plain,
! [X2,X0,X1] : multiply(add(X2,X0),add(X0,X1)) = add(X0,multiply(multiply(inverse(X0),X1),X2)),
inference(forward_demodulation,[],[f24581,f8695]) ).
fof(f25466,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),multiply(inverse(inverse(X1)),X2)) = multiply(multiply(inverse(inverse(X1)),X2),add(X0,inverse(X1))),
inference(superposition,[],[f24423,f11732]) ).
fof(f25468,plain,
! [X2,X0,X1] : multiply(multiply(inverse(inverse(X0)),X2),add(inverse(X0),X1)) = multiply(multiply(X0,X1),multiply(inverse(inverse(X0)),X2)),
inference(superposition,[],[f24423,f8696]) ).
fof(f25600,plain,
! [X2,X0,X1] : multiply(multiply(X0,X2),add(inverse(X0),X1)) = multiply(multiply(X0,X1),multiply(X0,X2)),
inference(forward_demodulation,[],[f25468,f4240]) ).
fof(f25602,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),multiply(inverse(inverse(X1)),X2)) = multiply(X0,multiply(inverse(inverse(X1)),X2)),
inference(forward_demodulation,[],[f25466,f24447]) ).
fof(f25659,plain,
! [X2,X0,X1] : multiply(multiply(X0,X2),X1) = multiply(multiply(X0,X1),multiply(X0,X2)),
inference(forward_demodulation,[],[f25600,f18443]) ).
fof(f25661,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X0,X1),multiply(X1,X2)),
inference(forward_demodulation,[],[f25602,f4240]) ).
fof(f25689,plain,
! [X2,X0,X1] : multiply(X1,X2) = multiply(multiply(X2,add(X0,X1)),X1),
inference(backward_demodulation,[],[f3840,f25659]) ).
fof(f25797,plain,
! [X2,X0,X1] : multiply(X1,X2) = multiply(X1,multiply(X2,add(X1,X0))),
inference(forward_demodulation,[],[f25689,f6934]) ).
fof(f25970,plain,
! [X2,X0,X1] : multiply(X0,X2) = multiply(X0,multiply(add(X0,X1),X2)),
inference(superposition,[],[f25797,f3178]) ).
fof(f26357,plain,
! [X2,X0,X1] : multiply(multiply(X1,X0),X2) = multiply(multiply(X1,X0),multiply(X0,X2)),
inference(superposition,[],[f25970,f3440]) ).
fof(f26563,plain,
! [X2,X0,X1] : multiply(multiply(X1,X0),X2) = multiply(X1,multiply(X0,X2)),
inference(forward_demodulation,[],[f26357,f25661]) ).
fof(f26981,plain,
! [X2,X0,X1] : multiply(add(X2,X0),add(X0,X1)) = add(X0,multiply(inverse(X0),multiply(X1,X2))),
inference(backward_demodulation,[],[f24681,f26563]) ).
fof(f27054,plain,
! [X2,X0,X1] : add(X0,multiply(X1,X2)) = multiply(add(X2,X0),add(X0,X1)),
inference(forward_demodulation,[],[f26981,f8695]) ).
fof(f27308,plain,
! [X2,X0,X1] : add(X0,multiply(X2,X1)) = add(X0,multiply(add(X0,X1),X2)),
inference(backward_demodulation,[],[f7815,f27054]) ).
fof(f27322,plain,
! [X2,X0,X1] : add(X2,multiply(X0,X1)) = add(X2,multiply(multiply(X0,X1),X0)),
inference(backward_demodulation,[],[f16527,f27054]) ).
fof(f27475,plain,
! [X2,X0,X1] : add(X2,multiply(X0,X1)) = add(X2,multiply(X0,multiply(X1,X0))),
inference(forward_demodulation,[],[f27322,f3164]) ).
fof(f27485,plain,
! [X2,X0,X1] : add(X0,multiply(X2,X1)) = multiply(add(X0,X1),add(X0,X2)),
inference(backward_demodulation,[],[f4994,f27308]) ).
fof(f27582,plain,
! [X2,X0,X1] : add(X2,multiply(X1,X0)) = add(X2,multiply(X0,X1)),
inference(forward_demodulation,[],[f27475,f4233]) ).
fof(f27614,plain,
~ sP0(add(a,multiply(c,b))),
inference(backward_demodulation,[],[f12,f27485]) ).
fof(f27696,plain,
~ sP0(add(a,multiply(b,c))),
inference(forward_demodulation,[],[f27614,f27582]) ).
fof(f27773,plain,
$false,
inference(forward_subsumption_resolution,[],[f27696,f13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : BOO023-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.27 % Computer : n008.cluster.edu
% 0.10/0.27 % Model : x86_64 x86_64
% 0.10/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.27 % Memory : 8046.5625MB
% 0.10/0.27 % OS : Linux 6.8.0-71-generic
% 0.10/0.27 % CPULimit : 300
% 0.10/0.27 % WCLimit : 300
% 0.10/0.27 % DateTime : Mon Sep 28 21:05:09 UTC 2026
% 0.10/0.27 % CPUTime :
% 0.10/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.27/0.33 Running first-order theorem proving
% 0.27/0.33 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
% 28.16/5.19 % (2650141)Detected a unit-equality problem, will run specialized UEQ schedule.
% 28.16/5.19 % (2650151)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1133528038:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 28.16/5.19 % (2650147)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=127386834:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 28.16/5.19 % (2650148)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1852554196:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 28.16/5.19 % (2650149)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3854786848:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 28.16/5.19 % (2650150)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1933289641:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 28.16/5.19 % (2650146)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=383658021:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 28.16/5.19 % (2650152)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1288911211:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 28.16/5.19 % (2650151)Instruction limit reached!
% 28.16/5.19 % (2650151)------------------------------
% 28.16/5.19 % (2650151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.16/5.19 % (2650151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.16/5.19 % (2650151)CaDiCaL version: 2.1.3
% 28.16/5.19 % (2650151)Termination reason: Instruction limit
% 28.16/5.19 % (2650151)Termination phase: Saturation
% 28.16/5.19 % (2650151)Time elapsed: 0.143 s
% 28.16/5.19 % (2650151)Peak memory usage: 91 MB
% 28.16/5.19 % (2650151)Instructions burned: 257 (million)
% 28.16/5.19 % (2650149)Instruction limit reached!
% 28.16/5.19 % (2650149)------------------------------
% 28.16/5.19 % (2650149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.16/5.19 % (2650149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.16/5.19 % (2650149)CaDiCaL version: 2.1.3
% 28.16/5.19 % (2650149)Termination reason: Instruction limit
% 28.16/5.19 % (2650149)Termination phase: Saturation
% 28.16/5.19 % (2650149)Time elapsed: 0.143 s
% 28.16/5.19 % (2650149)Peak memory usage: 89 MB
% 28.16/5.19 % (2650149)Instructions burned: 137 (million)
% 28.16/5.19 % (2650150)Instruction limit reached!
% 28.16/5.19 % (2650150)------------------------------
% 28.16/5.19 % (2650150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.16/5.19 % (2650150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.16/5.19 % (2650150)CaDiCaL version: 2.1.3
% 28.16/5.19 % (2650150)Termination reason: Instruction limit
% 28.16/5.19 % (2650150)Termination phase: Saturation
% 28.16/5.19 % (2650150)Time elapsed: 0.178 s
% 28.16/5.19 % (2650150)Peak memory usage: 89 MB
% 28.16/5.19 % (2650150)Instructions burned: 181 (million)
% 28.16/5.19 % (2650160)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3362339444:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 28.16/5.19 % (2650162)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=865799133:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 28.16/5.19 % (2650161)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1197827699:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 28.16/5.19 % (2650162)Instruction limit reached!
% 28.16/5.19 % (2650162)------------------------------
% 28.16/5.19 % (2650162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.16/5.19 % (2650162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.16/5.19 % (2650162)CaDiCaL version: 2.1.3
% 28.16/5.19 % (2650162)Termination reason: Instruction limit
% 28.16/5.19 % (2650162)Termination phase: Saturation
% 28.16/5.19 % (2650162)Time elapsed: 0.118 s
% 28.16/5.19 % (2650162)Peak memory usage: 91 MB
% 28.16/5.19 % (2650162)Instructions burned: 215 (million)
% 28.16/5.19 % (2650166)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=94654536:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2992 on theBenchmark for (2992ds/317Mi)
% 28.16/5.19 % (2650166)Instruction limit reached!
% 28.16/5.19 % (2650166)------------------------------
% 28.16/5.19 % (2650166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.16/5.19 % (2650166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.16/5.19 % (2650166)CaDiCaL version: 2.1.3
% 28.16/5.19 % (2650166)Termination reason: Instruction limit
% 28.16/5.19 % (2650166)Termination phase: Saturation
% 28.16/5.19 % (2650166)Time elapsed: 0.320 s
% 28.16/5.19 % (2650166)Peak memory usage: 93 MB
% 28.16/5.19 % (2650166)Instructions burned: 317 (million)
% 28.16/5.19 % (2650152)Instruction limit reached!
% 28.16/5.19 % (2650152)------------------------------
% 28.16/5.19 % (2650152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.16/5.19 % (2650152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.16/5.19 % (2650152)CaDiCaL version: 2.1.3
% 28.16/5.19 % (2650152)Termination reason: Instruction limit
% 28.16/5.19 % (2650152)Termination phase: Saturation
% 28.16/5.19 % (2650152)Time elapsed: 1.133 s
% 28.16/5.19 % (2650152)Peak memory usage: 99 MB
% 28.16/5.19 % (2650152)Instructions burned: 1188 (million)
% 28.16/5.19 % (2650168)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=3636187882:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/12125Mi)
% 28.16/5.19 % (2650169)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=491853490:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2985 on theBenchmark for (2985ds/2836Mi)
% 28.16/5.19 % (2650160)Instruction limit reached!
% 28.16/5.19 % (2650160)------------------------------
% 28.16/5.19 % (2650160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.16/5.19 % (2650160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.16/5.19 % (2650160)CaDiCaL version: 2.1.3
% 28.16/5.19 % (2650160)Termination reason: Instruction limit
% 28.16/5.19 % (2650160)Termination phase: Saturation
% 28.16/5.19 % (2650160)Time elapsed: 1.195 s
% 28.16/5.19 % (2650160)Peak memory usage: 138 MB
% 28.16/5.19 % (2650160)Instructions burned: 2051 (million)
% 28.16/5.19 % (2650172)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1485012502:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2982 on theBenchmark for (2982ds/14534Mi)
% 28.16/5.19 % (2650172)First to succeed.
% 28.16/5.19 % (2650172)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2650141"
% 28.16/5.19 % (2650172)Refutation found. Thanks to Tanya!
% 28.16/5.19 % SZS status Unsatisfiable for theBenchmark
% 28.16/5.19 % SZS output start Proof for theBenchmark
% See solution above
% 31.19/5.42 % (2650172)------------------------------
% 31.19/5.42 % (2650172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.19/5.42 % (2650172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.19/5.42 % (2650172)CaDiCaL version: 2.1.3
% 31.19/5.42 % (2650172)Termination reason: Refutation
% 31.19/5.42 % (2650172)Time elapsed: 2.008 s
% 31.19/5.42 % (2650172)Peak memory usage: 149 MB
% 31.19/5.42 % (2650172)Instructions burned: 3415 (million)
% 31.19/5.42 % (2650172)------------------------------
% 31.19/5.42 % (2650172)------------------------------
% 31.19/5.42 % (2650141)Success in time 4.269 s
% 31.19/5.42 % Vampire exiting
%------------------------------------------------------------------------------