%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : BOO022-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:36:12 AM UTC 2026
% Result : Unsatisfiable 63.44s 9.40s
% Output : Refutation 0.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 11
% Syntax : Number of formulae : 199 ( 199 unt; 4 def)
% Number of atoms : 199 ( 198 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 221 ( 221 !; 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,
! [X0,X1] : add(multiply(X0,X1),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add_multiply) ).
fof(f5,axiom,
! [X2,X0,X1] : add(X0,multiply(X1,X2)) = multiply(add(X1,X0),add(X2,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add_multiply_property) ).
fof(f6,axiom,
! [X0] : multiply(X0,inverse(X0)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_inverse) ).
fof(f7,negated_conjecture,
multiply(multiply(a,b),c) != multiply(a,multiply(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_associativity_of_multiply) ).
fof(f8,definition,
sF0 = multiply(a,b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f9,plain,
multiply(a,b) = sF0,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF1 = multiply(sF0,c),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f11,plain,
multiply(sF0,c) = sF1,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF2 = multiply(b,c),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f13,plain,
multiply(b,c) = sF2,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF3 = multiply(a,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f15,plain,
multiply(a,sF2) = sF3,
inference(reorient_equations,[],[f14]) ).
fof(f16,plain,
sF1 != sF3,
inference(definition_folding,[],[f7,f15,f13,f11,f9]) ).
fof(f17,plain,
! [X0] : inverse(X0) = multiply(n1,inverse(X0)),
inference(superposition,[],[f1,f3]) ).
fof(f18,plain,
! [X0] : inverse(X0) = add(n0,inverse(X0)),
inference(superposition,[],[f4,f6]) ).
fof(f19,plain,
! [X0] : add(X0,X0) = X0,
inference(superposition,[],[f4,f1]) ).
fof(f20,plain,
b = add(sF0,b),
inference(superposition,[],[f4,f9]) ).
fof(f24,plain,
! [X0] : multiply(X0,X0) = X0,
inference(superposition,[],[f1,f4]) ).
fof(f26,plain,
! [X2,X0,X1] : multiply(X0,add(add(X1,X0),X2)) = add(X0,multiply(X2,X0)),
inference(superposition,[],[f2,f1]) ).
fof(f27,plain,
! [X0] : multiply(b,add(a,X0)) = add(sF0,multiply(X0,b)),
inference(superposition,[],[f2,f9]) ).
fof(f28,plain,
! [X0] : multiply(sF2,add(a,X0)) = add(sF3,multiply(X0,sF2)),
inference(superposition,[],[f2,f15]) ).
fof(f29,plain,
! [X0] : multiply(c,add(b,X0)) = add(sF2,multiply(X0,c)),
inference(superposition,[],[f2,f13]) ).
fof(f30,plain,
! [X0] : multiply(c,add(sF0,X0)) = add(sF1,multiply(X0,c)),
inference(superposition,[],[f2,f11]) ).
fof(f31,plain,
! [X0,X1] : multiply(inverse(X0),add(X1,X0)) = add(multiply(X1,inverse(X0)),n0),
inference(superposition,[],[f2,f6]) ).
fof(f32,plain,
! [X2,X0,X1] : add(multiply(X1,X0),X0) = multiply(X0,add(X1,add(X2,X0))),
inference(superposition,[],[f2,f1]) ).
fof(f33,plain,
! [X0] : multiply(b,add(X0,a)) = add(multiply(X0,b),sF0),
inference(superposition,[],[f2,f9]) ).
fof(f34,plain,
! [X0] : multiply(sF2,add(X0,a)) = add(multiply(X0,sF2),sF3),
inference(superposition,[],[f2,f15]) ).
fof(f35,plain,
! [X0] : multiply(c,add(X0,b)) = add(multiply(X0,c),sF2),
inference(superposition,[],[f2,f13]) ).
fof(f36,plain,
! [X0] : multiply(c,add(X0,sF0)) = add(multiply(X0,c),sF1),
inference(superposition,[],[f2,f11]) ).
fof(f37,plain,
! [X2,X0,X1] : multiply(X2,X0) = multiply(multiply(X0,add(X1,X2)),multiply(X2,X0)),
inference(superposition,[],[f1,f2]) ).
fof(f38,plain,
! [X2,X0,X1] : multiply(X0,add(X1,add(X2,X0))) = X0,
inference(forward_demodulation,[],[f32,f4]) ).
fof(f41,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,add(X0,X0)),
inference(superposition,[],[f2,f19]) ).
fof(f42,plain,
! [X0,X1] : multiply(X1,X0) = multiply(X0,X1),
inference(forward_demodulation,[],[f41,f19]) ).
fof(f45,plain,
! [X0,X1] : add(X0,multiply(X0,X1)) = multiply(X0,add(X1,X0)),
inference(superposition,[],[f5,f19]) ).
fof(f46,plain,
! [X2,X0,X1] : add(X0,multiply(multiply(X1,X0),X2)) = multiply(X0,add(X2,X0)),
inference(superposition,[],[f5,f4]) ).
fof(f47,plain,
! [X2,X3,X0,X1] : add(multiply(X2,X0),multiply(multiply(X1,X0),X3)) = multiply(multiply(X0,add(X1,X2)),add(X3,multiply(X2,X0))),
inference(superposition,[],[f5,f2]) ).
fof(f48,plain,
! [X0,X1] : add(inverse(X0),multiply(X1,X0)) = multiply(add(X1,inverse(X0)),n1),
inference(superposition,[],[f5,f3]) ).
fof(f49,plain,
! [X0,X1] : multiply(add(X1,X0),X0) = add(X0,multiply(X1,X0)),
inference(superposition,[],[f5,f19]) ).
fof(f53,plain,
! [X2,X3,X0,X1] : multiply(add(X2,X0),add(add(X1,X0),X3)) = add(add(X0,multiply(X1,X2)),multiply(X3,add(X2,X0))),
inference(superposition,[],[f2,f5]) ).
fof(f54,plain,
! [X2,X0,X1] : add(X2,X0) = add(add(X0,multiply(X1,X2)),add(X2,X0)),
inference(superposition,[],[f4,f5]) ).
fof(f56,plain,
! [X0,X1] : multiply(X0,add(X1,X0)) = add(X0,multiply(X1,X0)),
inference(forward_demodulation,[],[f49,f42]) ).
fof(f57,plain,
! [X0,X1] : multiply(n1,add(X1,inverse(X0))) = add(inverse(X0),multiply(X1,X0)),
inference(forward_demodulation,[],[f48,f42]) ).
fof(f75,plain,
! [X0,X1] : add(multiply(X1,X0),X0) = multiply(X0,add(X1,X0)),
inference(superposition,[],[f2,f24]) ).
fof(f78,plain,
! [X0,X1] : add(X0,X1) = add(X1,multiply(X0,X0)),
inference(superposition,[],[f5,f24]) ).
fof(f79,plain,
! [X0,X1] : add(X0,X1) = add(X1,X0),
inference(forward_demodulation,[],[f78,f24]) ).
fof(f80,plain,
! [X0,X1] : multiply(X0,add(X1,X0)) = X0,
inference(forward_demodulation,[],[f75,f4]) ).
fof(f155,plain,
! [X0,X1] : add(multiply(X0,sF2),multiply(X1,sF3)) = multiply(add(X1,multiply(X0,sF2)),multiply(sF2,add(a,X0))),
inference(superposition,[],[f5,f28]) ).
fof(f159,plain,
! [X0,X1] : add(multiply(X0,sF2),multiply(X1,sF3)) = multiply(multiply(sF2,add(a,X0)),add(X1,multiply(X0,sF2))),
inference(forward_demodulation,[],[f155,f42]) ).
fof(f163,plain,
! [X0,X1] : add(multiply(X0,sF2),multiply(X1,sF3)) = add(multiply(X0,sF2),multiply(multiply(a,sF2),X1)),
inference(forward_demodulation,[],[f159,f47]) ).
fof(f165,plain,
! [X0,X1] : add(multiply(X0,sF2),multiply(X1,sF3)) = add(multiply(X0,sF2),multiply(sF3,X1)),
inference(forward_demodulation,[],[f163,f15]) ).
fof(f183,plain,
! [X0,X1] : add(multiply(X0,X1),X0) = X0,
inference(superposition,[],[f4,f42]) ).
fof(f188,plain,
sF1 = multiply(c,sF0),
inference(superposition,[],[f11,f42]) ).
fof(f189,plain,
! [X0,X1] : add(X0,multiply(X0,X1)) = X0,
inference(forward_demodulation,[],[f183,f79]) ).
fof(f196,plain,
multiply(c,add(b,sF0)) = add(sF2,sF1),
inference(superposition,[],[f29,f11]) ).
fof(f203,plain,
multiply(c,add(b,sF0)) = add(sF1,sF2),
inference(forward_demodulation,[],[f196,f79]) ).
fof(f213,plain,
sF0 = add(sF1,sF0),
inference(superposition,[],[f4,f188]) ).
fof(f214,plain,
sF0 = add(sF0,sF1),
inference(forward_demodulation,[],[f213,f79]) ).
fof(f220,plain,
add(sF1,sF2) = multiply(c,add(sF0,b)),
inference(superposition,[],[f30,f13]) ).
fof(f229,plain,
multiply(c,b) = add(sF1,sF2),
inference(forward_demodulation,[],[f220,f20]) ).
fof(f235,plain,
multiply(b,c) = add(sF1,sF2),
inference(forward_demodulation,[],[f229,f42]) ).
fof(f237,plain,
sF2 = add(sF1,sF2),
inference(forward_demodulation,[],[f235,f13]) ).
fof(f246,plain,
add(b,sF0) = multiply(b,add(b,a)),
inference(superposition,[],[f33,f24]) ).
fof(f260,plain,
multiply(b,add(a,b)) = add(b,sF0),
inference(forward_demodulation,[],[f246,f79]) ).
fof(f263,plain,
b = add(b,sF0),
inference(forward_demodulation,[],[f260,f80]) ).
fof(f273,plain,
multiply(sF2,add(sF2,a)) = add(sF2,sF3),
inference(superposition,[],[f34,f24]) ).
fof(f287,plain,
multiply(sF2,add(a,sF2)) = add(sF2,sF3),
inference(forward_demodulation,[],[f273,f79]) ).
fof(f290,plain,
sF2 = add(sF2,sF3),
inference(forward_demodulation,[],[f287,f80]) ).
fof(f293,plain,
! [X0] : sF3 = multiply(sF3,add(X0,sF2)),
inference(superposition,[],[f38,f290]) ).
fof(f300,plain,
multiply(c,add(c,b)) = add(c,sF2),
inference(superposition,[],[f35,f24]) ).
fof(f316,plain,
multiply(c,add(b,c)) = add(c,sF2),
inference(forward_demodulation,[],[f300,f79]) ).
fof(f320,plain,
c = add(c,sF2),
inference(forward_demodulation,[],[f316,f80]) ).
fof(f334,plain,
! [X0] : add(c,sF1) = multiply(c,add(add(X0,c),sF0)),
inference(superposition,[],[f36,f1]) ).
fof(f344,plain,
add(c,sF1) = add(c,multiply(sF0,c)),
inference(forward_demodulation,[],[f334,f26]) ).
fof(f348,plain,
multiply(c,add(sF0,c)) = add(c,sF1),
inference(forward_demodulation,[],[f344,f56]) ).
fof(f349,plain,
c = add(c,sF1),
inference(forward_demodulation,[],[f348,f80]) ).
fof(f423,plain,
! [X0] : add(sF1,multiply(X0,sF1)) = multiply(sF1,add(c,X0)),
inference(superposition,[],[f26,f349]) ).
fof(f433,plain,
! [X0,X1] : add(multiply(X0,sF2),multiply(X1,multiply(X0,sF2))) = multiply(multiply(X0,sF2),add(multiply(sF2,add(a,X0)),X1)),
inference(superposition,[],[f26,f28]) ).
fof(f434,plain,
! [X0,X1] : multiply(X0,n1) = add(X0,multiply(inverse(add(X1,X0)),X0)),
inference(superposition,[],[f26,f3]) ).
fof(f451,plain,
! [X0,X1] : multiply(X0,n1) = multiply(X0,add(inverse(add(X1,X0)),X0)),
inference(forward_demodulation,[],[f434,f56]) ).
fof(f452,plain,
! [X0,X1] : multiply(multiply(X0,sF2),add(multiply(sF2,add(a,X0)),X1)) = multiply(multiply(X0,sF2),add(X1,multiply(X0,sF2))),
inference(forward_demodulation,[],[f433,f56]) ).
fof(f457,plain,
! [X0] : multiply(sF1,add(c,X0)) = multiply(sF1,add(X0,sF1)),
inference(forward_demodulation,[],[f423,f56]) ).
fof(f474,plain,
! [X0] : multiply(X0,n1) = X0,
inference(forward_demodulation,[],[f451,f80]) ).
fof(f475,plain,
! [X0,X1] : multiply(X0,sF2) = multiply(multiply(X0,sF2),add(multiply(sF2,add(a,X0)),X1)),
inference(forward_demodulation,[],[f452,f80]) ).
fof(f480,plain,
! [X0] : sF1 = multiply(sF1,add(c,X0)),
inference(forward_demodulation,[],[f457,f80]) ).
fof(f502,plain,
! [X0] : multiply(n1,X0) = X0,
inference(superposition,[],[f42,f474]) ).
fof(f506,plain,
! [X0] : n1 = add(X0,n1),
inference(superposition,[],[f1,f474]) ).
fof(f509,plain,
! [X0] : add(multiply(X0,inverse(inverse(X0))),n0) = multiply(inverse(inverse(X0)),n1),
inference(superposition,[],[f31,f3]) ).
fof(f565,plain,
! [X0] : add(multiply(X0,inverse(inverse(X0))),n0) = multiply(n1,inverse(inverse(X0))),
inference(forward_demodulation,[],[f509,f42]) ).
fof(f579,plain,
! [X0] : inverse(inverse(X0)) = add(multiply(X0,inverse(inverse(X0))),n0),
inference(forward_demodulation,[],[f565,f17]) ).
fof(f589,plain,
! [X0] : inverse(inverse(X0)) = add(n0,multiply(X0,inverse(inverse(X0)))),
inference(forward_demodulation,[],[f579,f79]) ).
fof(f844,plain,
! [X0,X1] : multiply(n1,add(X1,n1)) = add(n1,multiply(X0,X1)),
inference(superposition,[],[f46,f474]) ).
fof(f861,plain,
! [X2,X0,X1] : multiply(add(X2,X0),add(multiply(X0,X1),add(X2,X0))) = add(add(X2,X0),multiply(X0,X1)),
inference(superposition,[],[f46,f37]) ).
fof(f867,plain,
! [X0,X1] : add(X0,n0) = multiply(X0,add(inverse(multiply(X1,X0)),X0)),
inference(superposition,[],[f46,f6]) ).
fof(f912,plain,
! [X0] : add(X0,n0) = X0,
inference(forward_demodulation,[],[f867,f80]) ).
fof(f916,plain,
! [X2,X0,X1] : add(X2,X0) = add(add(X2,X0),multiply(X0,X1)),
inference(forward_demodulation,[],[f861,f80]) ).
fof(f921,plain,
! [X0,X1] : n1 = add(n1,multiply(X0,X1)),
inference(forward_demodulation,[],[f844,f80]) ).
fof(f946,plain,
! [X0,X1] : add(n0,multiply(X1,X0)) = multiply(add(X1,n0),X0),
inference(superposition,[],[f5,f912]) ).
fof(f952,plain,
! [X0] : n0 = multiply(X0,n0),
inference(superposition,[],[f4,f912]) ).
fof(f957,plain,
! [X0,X1] : multiply(X1,X0) = add(n0,multiply(X1,X0)),
inference(forward_demodulation,[],[f946,f912]) ).
fof(f976,plain,
! [X0] : add(b,X0) = add(add(X0,sF0),add(b,X0)),
inference(superposition,[],[f54,f9]) ).
fof(f983,plain,
! [X0] : add(c,X0) = add(add(X0,sF1),add(c,X0)),
inference(superposition,[],[f54,f11]) ).
fof(f1140,plain,
! [X0,X1] : add(add(X0,n1),X1) = add(n1,multiply(X1,n1)),
inference(superposition,[],[f26,f502]) ).
fof(f1162,plain,
! [X0,X1] : n1 = add(add(X0,n1),X1),
inference(forward_demodulation,[],[f1140,f921]) ).
fof(f1180,plain,
! [X1] : n1 = add(n1,X1),
inference(forward_demodulation,[],[f1162,f506]) ).
fof(f1307,plain,
! [X0] : multiply(n1,add(X0,inverse(inverse(X0)))) = add(inverse(inverse(X0)),n0),
inference(superposition,[],[f57,f6]) ).
fof(f1368,plain,
! [X0] : multiply(n1,add(X0,inverse(inverse(X0)))) = add(n0,inverse(inverse(X0))),
inference(forward_demodulation,[],[f1307,f79]) ).
fof(f1399,plain,
! [X0] : inverse(inverse(X0)) = multiply(n1,add(X0,inverse(inverse(X0)))),
inference(forward_demodulation,[],[f1368,f18]) ).
fof(f1412,plain,
! [X0] : inverse(inverse(X0)) = add(X0,inverse(inverse(X0))),
inference(forward_demodulation,[],[f1399,f502]) ).
fof(f1427,plain,
! [X0] : n0 = multiply(n0,X0),
inference(superposition,[],[f42,f952]) ).
fof(f1442,plain,
! [X2,X0,X1] : add(multiply(X0,X1),multiply(multiply(X0,X1),X2)) = multiply(multiply(X1,X0),add(X2,multiply(X0,X1))),
inference(superposition,[],[f47,f19]) ).
fof(f1447,plain,
! [X2,X0,X1] : add(multiply(n0,X1),multiply(multiply(X0,X1),X2)) = multiply(multiply(X1,X0),add(X2,multiply(n0,X1))),
inference(superposition,[],[f47,f912]) ).
fof(f1476,plain,
! [X2,X0,X1] : add(multiply(X1,add(X0,X1)),multiply(multiply(X0,add(X0,X1)),X2)) = multiply(add(X0,X1),add(X2,multiply(X1,add(X0,X1)))),
inference(superposition,[],[f47,f24]) ).
fof(f1479,plain,
! [X2,X3,X0,X1] : add(multiply(X0,add(X1,X0)),multiply(multiply(X2,add(X1,X0)),X3)) = multiply(add(X0,multiply(X1,X2)),add(X3,multiply(X0,add(X1,X0)))),
inference(superposition,[],[f47,f5]) ).
fof(f1583,plain,
! [X2,X3,X0,X1] : add(X0,multiply(multiply(X2,add(X1,X0)),X3)) = multiply(add(X0,multiply(X1,X2)),add(X3,X0)),
inference(forward_demodulation,[],[f1479,f80]) ).
fof(f1584,plain,
! [X2,X0,X1] : multiply(add(X0,X1),add(X2,X1)) = add(X1,multiply(multiply(X0,add(X0,X1)),X2)),
inference(forward_demodulation,[],[f1476,f80]) ).
fof(f1593,plain,
! [X2,X0,X1] : add(n0,multiply(multiply(X0,X1),X2)) = multiply(multiply(X1,X0),add(X2,n0)),
inference(forward_demodulation,[],[f1447,f1427]) ).
fof(f1598,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),add(X2,multiply(X0,X1))) = multiply(multiply(X1,X0),add(X2,multiply(X0,X1))),
inference(forward_demodulation,[],[f1442,f45]) ).
fof(f1619,plain,
! [X2,X0,X1] : multiply(add(X0,X1),add(X2,X1)) = multiply(add(X1,multiply(X0,X0)),add(X2,X1)),
inference(forward_demodulation,[],[f1584,f1583]) ).
fof(f1626,plain,
! [X2,X0,X1] : multiply(multiply(X1,X0),X2) = add(n0,multiply(multiply(X0,X1),X2)),
inference(forward_demodulation,[],[f1593,f912]) ).
fof(f1628,plain,
! [X2,X0,X1] : multiply(X0,X1) = multiply(multiply(X1,X0),add(X2,multiply(X0,X1))),
inference(forward_demodulation,[],[f1598,f80]) ).
fof(f1636,plain,
! [X2,X0,X1] : multiply(add(X0,X1),add(X2,X1)) = multiply(add(X1,X0),add(X2,X1)),
inference(forward_demodulation,[],[f1619,f24]) ).
fof(f1642,plain,
! [X2,X0,X1] : multiply(multiply(X1,X0),X2) = multiply(multiply(X0,X1),X2),
inference(forward_demodulation,[],[f1626,f957]) ).
fof(f1645,plain,
! [X2,X0,X1] : add(X1,multiply(X0,X2)) = multiply(add(X1,X0),add(X2,X1)),
inference(forward_demodulation,[],[f1636,f5]) ).
fof(f1660,plain,
! [X0] : sF1 = multiply(sF1,add(X0,sF0)),
inference(superposition,[],[f38,f214]) ).
fof(f2217,plain,
! [X0] : add(n0,X0) = X0,
inference(superposition,[],[f4,f1427]) ).
fof(f2379,plain,
! [X2,X0,X1] : multiply(n1,add(add(X1,X0),X2)) = add(add(X0,multiply(X1,n1)),multiply(X2,n1)),
inference(superposition,[],[f53,f1180]) ).
fof(f2461,plain,
! [X2,X0,X1] : multiply(n1,add(add(X1,X0),X2)) = add(add(X0,multiply(X1,n1)),X2),
inference(forward_demodulation,[],[f2379,f474]) ).
fof(f2521,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = multiply(n1,add(add(X1,X0),X2)),
inference(forward_demodulation,[],[f2461,f474]) ).
fof(f2556,plain,
! [X2,X0,X1] : add(add(X1,X0),X2) = add(add(X0,X1),X2),
inference(forward_demodulation,[],[f2521,f502]) ).
fof(f2681,plain,
! [X0,X1] : multiply(add(X0,X1),X0) = X0,
inference(superposition,[],[f1,f79]) ).
fof(f2726,plain,
! [X0,X1] : multiply(X0,add(X0,X1)) = X0,
inference(forward_demodulation,[],[f2681,f42]) ).
fof(f3618,plain,
multiply(sF0,c) = multiply(add(sF1,sF2),multiply(sF0,c)),
inference(superposition,[],[f37,f203]) ).
fof(f3621,plain,
add(b,sF0) = add(add(sF1,sF2),add(b,sF0)),
inference(superposition,[],[f4,f203]) ).
fof(f3642,plain,
add(b,sF0) = add(add(b,sF0),add(sF1,sF2)),
inference(forward_demodulation,[],[f3621,f79]) ).
fof(f3645,plain,
multiply(sF0,c) = multiply(multiply(sF0,c),add(sF1,sF2)),
inference(forward_demodulation,[],[f3618,f42]) ).
fof(f3661,plain,
add(b,sF0) = add(add(b,sF0),sF2),
inference(forward_demodulation,[],[f3642,f237]) ).
fof(f3664,plain,
multiply(sF0,c) = multiply(multiply(c,sF0),add(sF1,sF2)),
inference(forward_demodulation,[],[f3645,f1642]) ).
fof(f3677,plain,
add(b,sF0) = add(sF2,add(b,sF0)),
inference(forward_demodulation,[],[f3661,f79]) ).
fof(f3679,plain,
multiply(sF0,c) = multiply(multiply(c,sF0),sF2),
inference(forward_demodulation,[],[f3664,f237]) ).
fof(f3687,plain,
b = add(sF2,b),
inference(forward_demodulation,[],[f3677,f263]) ).
fof(f3688,plain,
multiply(sF0,c) = multiply(sF2,multiply(c,sF0)),
inference(forward_demodulation,[],[f3679,f42]) ).
fof(f3693,plain,
b = add(b,sF2),
inference(forward_demodulation,[],[f3687,f79]) ).
fof(f3694,plain,
multiply(sF0,c) = multiply(sF2,sF1),
inference(forward_demodulation,[],[f3688,f188]) ).
fof(f3699,plain,
multiply(sF0,c) = multiply(sF1,sF2),
inference(forward_demodulation,[],[f3694,f42]) ).
fof(f3700,plain,
multiply(c,sF0) = multiply(sF1,sF2),
inference(forward_demodulation,[],[f3699,f42]) ).
fof(f3701,plain,
sF1 = multiply(sF1,sF2),
inference(forward_demodulation,[],[f3700,f188]) ).
fof(f4131,plain,
a = add(a,sF0),
inference(superposition,[],[f189,f9]) ).
fof(f4132,plain,
a = add(a,sF3),
inference(superposition,[],[f189,f15]) ).
fof(f5181,plain,
sF3 = multiply(sF3,b),
inference(superposition,[],[f293,f3693]) ).
fof(f5182,plain,
sF3 = multiply(sF3,c),
inference(superposition,[],[f293,f320]) ).
fof(f5220,plain,
sF3 = multiply(c,sF3),
inference(forward_demodulation,[],[f5182,f42]) ).
fof(f5221,plain,
sF3 = multiply(b,sF3),
inference(forward_demodulation,[],[f5181,f42]) ).
fof(f5278,plain,
c = add(c,sF3),
inference(superposition,[],[f189,f5220]) ).
fof(f5340,plain,
b = add(b,sF3),
inference(superposition,[],[f189,f5221]) ).
fof(f8871,plain,
sF1 = multiply(sF1,inverse(inverse(c))),
inference(superposition,[],[f480,f1412]) ).
fof(f10292,plain,
! [X0] : multiply(X0,inverse(inverse(X0))) = X0,
inference(superposition,[],[f2726,f1412]) ).
fof(f10670,plain,
! [X0] : inverse(inverse(X0)) = multiply(X0,inverse(inverse(X0))),
inference(superposition,[],[f2217,f589]) ).
fof(f10716,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[],[f10670,f10292]) ).
fof(f13309,plain,
b = add(add(sF3,sF0),b),
inference(superposition,[],[f976,f5340]) ).
fof(f13378,plain,
b = add(add(sF0,sF3),b),
inference(forward_demodulation,[],[f13309,f2556]) ).
fof(f13411,plain,
b = add(b,add(sF0,sF3)),
inference(forward_demodulation,[],[f13378,f79]) ).
fof(f14125,plain,
c = add(add(sF3,sF1),c),
inference(superposition,[],[f983,f5278]) ).
fof(f14194,plain,
c = add(add(sF1,sF3),c),
inference(forward_demodulation,[],[f14125,f2556]) ).
fof(f14226,plain,
c = add(c,add(sF1,sF3)),
inference(forward_demodulation,[],[f14194,f79]) ).
fof(f19734,plain,
! [X0] : multiply(inverse(inverse(c)),add(sF1,X0)) = add(sF1,multiply(X0,inverse(inverse(c)))),
inference(superposition,[],[f2,f8871]) ).
fof(f19789,plain,
! [X0] : add(sF1,multiply(X0,c)) = multiply(c,add(sF1,X0)),
inference(forward_demodulation,[],[f19734,f10716]) ).
fof(f19808,plain,
! [X0] : multiply(c,add(sF0,X0)) = multiply(c,add(sF1,X0)),
inference(forward_demodulation,[],[f19789,f30]) ).
fof(f22928,plain,
sF1 = multiply(sF1,a),
inference(superposition,[],[f1660,f4131]) ).
fof(f23003,plain,
sF1 = multiply(a,sF1),
inference(forward_demodulation,[],[f22928,f42]) ).
fof(f23339,plain,
a = add(a,sF1),
inference(superposition,[],[f189,f23003]) ).
fof(f26297,plain,
! [X0] : add(sF0,multiply(X0,b)) = multiply(add(sF0,X0),b),
inference(superposition,[],[f1645,f263]) ).
fof(f26487,plain,
! [X0] : add(sF0,multiply(X0,b)) = multiply(b,add(sF0,X0)),
inference(forward_demodulation,[],[f26297,f42]) ).
fof(f26678,plain,
! [X0] : multiply(b,add(a,X0)) = multiply(b,add(sF0,X0)),
inference(forward_demodulation,[],[f26487,f27]) ).
fof(f34505,plain,
add(sF0,sF3) = multiply(b,add(sF0,sF3)),
inference(superposition,[],[f1,f13411]) ).
fof(f34578,plain,
add(sF0,sF3) = multiply(b,add(a,sF3)),
inference(forward_demodulation,[],[f34505,f26678]) ).
fof(f34600,plain,
multiply(b,a) = add(sF0,sF3),
inference(forward_demodulation,[],[f34578,f4132]) ).
fof(f34609,plain,
multiply(a,b) = add(sF0,sF3),
inference(forward_demodulation,[],[f34600,f42]) ).
fof(f34615,plain,
sF0 = add(sF0,sF3),
inference(forward_demodulation,[],[f34609,f9]) ).
fof(f36703,plain,
add(sF1,sF3) = multiply(c,add(sF1,sF3)),
inference(superposition,[],[f1,f14226]) ).
fof(f36778,plain,
add(sF1,sF3) = multiply(c,add(sF0,sF3)),
inference(forward_demodulation,[],[f36703,f19808]) ).
fof(f36802,plain,
multiply(c,sF0) = add(sF1,sF3),
inference(forward_demodulation,[],[f36778,f34615]) ).
fof(f36813,plain,
sF1 = add(sF1,sF3),
inference(forward_demodulation,[],[f36802,f188]) ).
fof(f37264,plain,
! [X0] : sF1 = add(sF1,multiply(sF3,X0)),
inference(superposition,[],[f916,f36813]) ).
fof(f40454,plain,
! [X0] : add(sF1,multiply(sF3,X0)) = add(sF1,multiply(X0,sF3)),
inference(superposition,[],[f165,f3701]) ).
fof(f40652,plain,
! [X0] : sF1 = add(sF1,multiply(X0,sF3)),
inference(forward_demodulation,[],[f40454,f37264]) ).
fof(f40720,plain,
! [X0] : multiply(X0,sF3) = multiply(multiply(sF3,X0),sF1),
inference(superposition,[],[f1628,f40652]) ).
fof(f40800,plain,
! [X0] : multiply(X0,sF3) = multiply(sF1,multiply(sF3,X0)),
inference(forward_demodulation,[],[f40720,f42]) ).
fof(f42163,plain,
! [X0] : multiply(sF1,sF2) = multiply(multiply(sF1,sF2),add(multiply(sF2,a),X0)),
inference(superposition,[],[f475,f23339]) ).
fof(f42325,plain,
! [X0] : multiply(sF1,sF2) = multiply(multiply(sF1,sF2),add(multiply(a,sF2),X0)),
inference(forward_demodulation,[],[f42163,f42]) ).
fof(f42364,plain,
! [X0] : multiply(sF1,sF2) = multiply(multiply(sF1,sF2),add(sF3,X0)),
inference(forward_demodulation,[],[f42325,f15]) ).
fof(f42391,plain,
! [X0] : sF1 = multiply(sF1,add(sF3,X0)),
inference(forward_demodulation,[],[f42364,f3701]) ).
fof(f48920,plain,
! [X0] : sF1 = multiply(sF1,multiply(sF3,add(X0,sF3))),
inference(superposition,[],[f42391,f45]) ).
fof(f49031,plain,
! [X0] : sF1 = multiply(add(X0,sF3),sF3),
inference(forward_demodulation,[],[f48920,f40800]) ).
fof(f49048,plain,
! [X0] : sF1 = multiply(sF3,add(X0,sF3)),
inference(forward_demodulation,[],[f49031,f42]) ).
fof(f49058,plain,
sF1 = sF3,
inference(forward_demodulation,[],[f49048,f80]) ).
fof(f49065,plain,
$false,
inference(forward_subsumption_resolution,[],[f49058,f16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BOO022-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.30 % Computer : n005.cluster.edu
% 0.12/0.30 % Model : x86_64 x86_64
% 0.12/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.30 % Memory : 8046.5625MB
% 0.12/0.30 % OS : Linux 6.8.0-71-generic
% 0.12/0.30 % CPULimit : 300
% 0.12/0.30 % WCLimit : 300
% 0.12/0.30 % DateTime : Mon Sep 28 21:04:16 UTC 2026
% 0.12/0.31 % CPUTime :
% 0.12/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.30/0.36 Running first-order model finding
% 0.30/0.36 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.33/4.56 % (1173838)Will run a generic schedule for satisfiability detection.
% 29.33/4.56 % (1173846)dis+10_1_sil=32000:sp=arity:random_seed=4202517389:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 29.33/4.56 % (1173844)% WARNING: option uhcvi not known.
% 29.33/4.56 % (1173845)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1811961387:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 29.33/4.56 % (1173844)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2668711790:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 29.33/4.56 % (1173843)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4238058859_2999 on theBenchmark for (2999ds/0Mi)
% 29.33/4.56 % (1173847)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=888248470:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 29.33/4.56 % TRYING [1]
% 29.33/4.56 % TRYING [2]
% 29.33/4.56 % TRYING [3]
% 29.33/4.56 % TRYING [4]
% 29.33/4.56 % (1173849)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1948345289:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 29.33/4.56 % (1173848)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2813660043:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 29.33/4.56 % (1173846)Instruction limit reached!
% 29.33/4.56 % (1173846)------------------------------
% 29.33/4.56 % (1173846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.33/4.56 % (1173846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.33/4.56 % (1173846)CaDiCaL version: 2.1.3
% 29.33/4.56 % (1173846)Termination reason: Instruction limit
% 29.33/4.56 % (1173846)Termination phase: Saturation
% 29.33/4.56 % (1173846)Time elapsed: 0.049 s
% 29.33/4.56 % (1173846)Peak memory usage: 12 MB
% 29.33/4.56 % (1173846)Instructions burned: 103 (million)
% 29.33/4.56 % TRYING [5]
% 29.33/4.56 % (1173857)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1465306884:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 29.33/4.56 % TRYING [1]
% 29.33/4.56 % TRYING [2]
% 29.33/4.56 % TRYING [3]
% 29.33/4.56 % TRYING [4]
% 29.33/4.56 % TRYING [5]
% 29.33/4.56 % TRYING [6]
% 29.33/4.56 % (1173847)Instruction limit reached!
% 29.33/4.56 % (1173847)------------------------------
% 29.33/4.56 % (1173847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.33/4.56 % (1173847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.33/4.56 % (1173847)CaDiCaL version: 2.1.3
% 29.33/4.56 % (1173847)Termination reason: Instruction limit
% 29.33/4.56 % (1173847)Termination phase: Saturation
% 29.33/4.56 % (1173847)Time elapsed: 0.117 s
% 29.33/4.56 % (1173847)Peak memory usage: 12 MB
% 29.33/4.56 % (1173847)Instructions burned: 116 (million)
% 29.33/4.56 % TRYING [6]
% 29.33/4.56 % (1173848)Instruction limit reached!
% 29.33/4.56 % (1173848)------------------------------
% 29.33/4.56 % (1173848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.33/4.56 % (1173848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.33/4.56 % (1173848)CaDiCaL version: 2.1.3
% 29.33/4.56 % (1173848)Termination reason: Instruction limit
% 29.33/4.56 % (1173848)Termination phase: Saturation
% 29.33/4.56 % (1173848)Time elapsed: 0.136 s
% 29.33/4.56 % (1173848)Peak memory usage: 13 MB
% 29.33/4.56 % (1173848)Instructions burned: 132 (million)
% 29.33/4.56 % (1173859)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=792912209:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 29.33/4.56 % (1173860)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3160376115:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 29.33/4.56 % (1173849)Instruction limit reached!
% 29.33/4.56 % (1173849)------------------------------
% 29.33/4.56 % (1173849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.33/4.56 % (1173849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.33/4.56 % (1173849)CaDiCaL version: 2.1.3
% 29.33/4.56 % (1173849)Termination reason: Instruction limit
% 29.33/4.56 % (1173849)Termination phase: Saturation
% 29.33/4.56 % (1173849)Time elapsed: 0.215 s
% 29.33/4.56 % (1173849)Peak memory usage: 12 MB
% 29.33/4.56 % (1173849)Instructions burned: 160 (million)
% 29.33/4.56 % (1173863)ott-21_1_sil=16000:fs=off:random_seed=1954238842:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 29.33/4.56 % TRYING [7]
% 29.33/4.56 % (1173859)Instruction limit reached!
% 29.33/4.56 % (1173859)------------------------------
% 29.33/4.56 % (1173859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173859)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173859)Termination reason: Instruction limit
% 63.44/9.40 % (1173859)Termination phase: Saturation
% 63.44/9.40 % (1173859)Time elapsed: 0.142 s
% 63.44/9.40 % (1173859)Peak memory usage: 12 MB
% 63.44/9.40 % (1173859)Instructions burned: 131 (million)
% 63.44/9.40 % TRYING [7]
% 63.44/9.40 % (1173865)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1544944823:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 63.44/9.40 % (1173857)Instruction limit reached!
% 63.44/9.40 % (1173857)------------------------------
% 63.44/9.40 % (1173857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173857)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173857)Termination reason: Instruction limit
% 63.44/9.40 % (1173857)Termination phase: Finite model building constraint generation
% 63.44/9.40 % (1173857)Time elapsed: 0.309 s
% 63.44/9.40 % (1173857)Peak memory usage: 24 MB
% 63.44/9.40 % (1173857)Instructions burned: 714 (million)
% 63.44/9.40 % (1173867)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=889614814:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 63.44/9.40 % TRYING [1]
% 63.44/9.40 % TRYING [2]
% 63.44/9.40 % TRYING [3]
% 63.44/9.40 % TRYING [4]
% 63.44/9.40 % (1173863)Instruction limit reached!
% 63.44/9.40 % (1173863)------------------------------
% 63.44/9.40 % (1173863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173863)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173863)Termination reason: Instruction limit
% 63.44/9.40 % (1173863)Termination phase: Saturation
% 63.44/9.40 % (1173863)Time elapsed: 0.154 s
% 63.44/9.40 % (1173863)Peak memory usage: 12 MB
% 63.44/9.40 % (1173863)Instructions burned: 181 (million)
% 63.44/9.40 % TRYING [5]
% 63.44/9.40 % (1173869)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4114587677:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 63.44/9.40 % TRYING [6]
% 63.44/9.40 % (1173867)Instruction limit reached!
% 63.44/9.40 % (1173867)------------------------------
% 63.44/9.40 % (1173867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173867)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173867)Termination reason: Instruction limit
% 63.44/9.40 % (1173867)Termination phase: Finite model building SAT solving
% 63.44/9.40 % (1173867)Time elapsed: 0.276 s
% 63.44/9.40 % (1173867)Peak memory usage: 18 MB
% 63.44/9.40 % (1173867)Instructions burned: 868 (million)
% 63.44/9.40 % (1173871)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4230052482:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 63.44/9.40 % (1173860)Instruction limit reached!
% 63.44/9.40 % (1173860)------------------------------
% 63.44/9.40 % (1173860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173860)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173860)Termination reason: Instruction limit
% 63.44/9.40 % (1173860)Termination phase: Saturation
% 63.44/9.40 % (1173860)Time elapsed: 0.600 s
% 63.44/9.40 % (1173860)Peak memory usage: 18 MB
% 63.44/9.40 % (1173860)Instructions burned: 685 (million)
% 63.44/9.40 % TRYING [14]
% 63.44/9.40 % (1173865)Instruction limit reached!
% 63.44/9.40 % (1173865)------------------------------
% 63.44/9.40 % (1173865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173865)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173865)Termination reason: Instruction limit
% 63.44/9.40 % (1173865)Termination phase: Saturation
% 63.44/9.40 % (1173865)Time elapsed: 0.447 s
% 63.44/9.40 % (1173865)Peak memory usage: 15 MB
% 63.44/9.40 % (1173865)Instructions burned: 477 (million)
% 63.44/9.40 % TRYING [8]
% 63.44/9.40 % (1173873)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=950599869:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 63.44/9.40 % (1173874)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=760472580:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 63.44/9.40 % (1173871)Instruction limit reached!
% 63.44/9.40 % (1173871)------------------------------
% 63.44/9.40 % (1173871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173871)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173871)Termination reason: Instruction limit
% 63.44/9.40 % (1173871)Termination phase: Finite model building constraint generation
% 63.44/9.40 % (1173871)Time elapsed: 0.330 s
% 63.44/9.40 % (1173871)Peak memory usage: 77 MB
% 63.44/9.40 % (1173871)Instructions burned: 892 (million)
% 63.44/9.40 % (1173877)fmb+10_1_sil=64000:random_seed=2304271607:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 63.44/9.40 % TRYING [1]
% 63.44/9.40 % TRYING [2]
% 63.44/9.40 % TRYING [3]
% 63.44/9.40 % TRYING [4]
% 63.44/9.40 % TRYING [5]
% 63.44/9.40 % TRYING [6]
% 63.44/9.40 % (1173873)Instruction limit reached!
% 63.44/9.40 % (1173873)------------------------------
% 63.44/9.40 % (1173873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173873)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173873)Termination reason: Instruction limit
% 63.44/9.40 % (1173873)Termination phase: Saturation
% 63.44/9.40 % (1173873)Time elapsed: 0.644 s
% 63.44/9.40 % (1173873)Peak memory usage: 18 MB
% 63.44/9.40 % (1173873)Instructions burned: 692 (million)
% 63.44/9.40 % TRYING [7]
% 63.44/9.40 % (1173879)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2696669306:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 63.44/9.40 % TRYING [20]
% 63.44/9.40 % (1173874)Instruction limit reached!
% 63.44/9.40 % (1173874)------------------------------
% 63.44/9.40 % (1173874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173874)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173874)Termination reason: Instruction limit
% 63.44/9.40 % (1173874)Termination phase: Saturation
% 63.44/9.40 % (1173874)Time elapsed: 0.810 s
% 63.44/9.40 % (1173874)Peak memory usage: 18 MB
% 63.44/9.40 % (1173874)Instructions burned: 879 (million)
% 63.44/9.40 % (1173881)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1875302904:fmbsr=1.7:i=920_2982 on theBenchmark for (2982ds/920Mi)
% 63.44/9.40 % TRYING [8]
% 63.44/9.40 % (1173869)Instruction limit reached!
% 63.44/9.40 % (1173869)------------------------------
% 63.44/9.40 % (1173869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173869)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173869)Termination reason: Instruction limit
% 63.44/9.40 % (1173869)Termination phase: Saturation
% 63.44/9.40 % (1173869)Time elapsed: 1.262 s
% 63.44/9.40 % (1173869)Peak memory usage: 22 MB
% 63.44/9.40 % (1173869)Instructions burned: 1180 (million)
% 63.44/9.40 % (1173883)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4270832191:i=5131_2981 on theBenchmark for (2981ds/5131Mi)
% 63.44/9.40 % TRYING [8]
% 63.44/9.40 % (1173881)Instruction limit reached!
% 63.44/9.40 % (1173881)------------------------------
% 63.44/9.40 % (1173881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173881)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173881)Termination reason: Instruction limit
% 63.44/9.40 % (1173881)Termination phase: Finite model building SAT solving
% 63.44/9.40 % (1173881)Time elapsed: 0.824 s
% 63.44/9.40 % (1173881)Peak memory usage: 54 MB
% 63.44/9.40 % (1173881)Instructions burned: 920 (million)
% 63.44/9.40 % (1173885)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3122840010:i=1472:ins=7:fdi=8:gsp=on_2974 on theBenchmark for (2974ds/1472Mi)
% 63.44/9.40 % TRYING [9]
% 63.44/9.40 % (1173885)Instruction limit reached!
% 63.44/9.40 % (1173885)------------------------------
% 63.44/9.40 % (1173885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173885)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173885)Termination reason: Instruction limit
% 63.44/9.40 % (1173885)Termination phase: Saturation
% 63.44/9.40 % (1173885)Time elapsed: 1.476 s
% 63.44/9.40 % (1173885)Peak memory usage: 28 MB
% 63.44/9.40 % (1173885)Instructions burned: 1473 (million)
% 63.44/9.40 % (1173888)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1283129781:i=6324_2958 on theBenchmark for (2958ds/6324Mi)
% 63.44/9.40 % TRYING [77]
% 63.44/9.40 % TRYING [9]
% 63.44/9.40 % (1173883)Instruction limit reached!
% 63.44/9.40 % (1173883)------------------------------
% 63.44/9.40 % (1173883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173883)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173883)Termination reason: Instruction limit
% 63.44/9.40 % (1173883)Termination phase: Saturation
% 63.44/9.40 % (1173883)Time elapsed: 4.899 s
% 63.44/9.40 % (1173883)Peak memory usage: 65 MB
% 63.44/9.40 % (1173883)Instructions burned: 5132 (million)
% 63.44/9.40 % (1173893)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1416266886:fmbsr=2.30978:i=2174_2932 on theBenchmark for (2932ds/2174Mi)
% 63.44/9.40 % TRYING [16]
% 63.44/9.40 % (1173893)Instruction limit reached!
% 63.44/9.40 % (1173893)------------------------------
% 63.44/9.40 % (1173893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173893)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173893)Termination reason: Instruction limit
% 63.44/9.40 % (1173893)Termination phase: Finite model building constraint generation
% 63.44/9.40 % (1173893)Time elapsed: 1.059 s
% 63.44/9.40 % (1173893)Peak memory usage: 132 MB
% 63.44/9.40 % (1173893)Instructions burned: 2175 (million)
% 63.44/9.40 % (1173879)Instruction limit reached!
% 63.44/9.40 % (1173879)------------------------------
% 63.44/9.40 % (1173879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173879)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173879)Termination reason: Instruction limit
% 63.44/9.40 % (1173879)Termination phase: Finite model building constraint generation
% 63.44/9.40 % (1173879)Time elapsed: 6.307 s
% 63.44/9.40 % (1173879)Peak memory usage: 666 MB
% 63.44/9.40 % (1173879)Instructions burned: 9515 (million)
% 63.44/9.40 % (1173984)ott-2_1_sil=16000:newcnf=on:random_seed=291775553:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2921 on theBenchmark for (2921ds/869Mi)
% 63.44/9.40 % (1174011)ott+10_1_sil=32000:tgt=ground:random_seed=1630320003:i=5114:av=off_2920 on theBenchmark for (2920ds/5114Mi)
% 63.44/9.40 % (1173888)Instruction limit reached!
% 63.44/9.40 % (1173888)------------------------------
% 63.44/9.40 % (1173888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173888)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173888)Termination reason: Instruction limit
% 63.44/9.40 % (1173888)Termination phase: Finite model building constraint generation
% 63.44/9.40 % (1173888)Time elapsed: 3.953 s
% 63.44/9.40 % (1173888)Peak memory usage: 430 MB
% 63.44/9.40 % (1173888)Instructions burned: 6325 (million)
% 63.44/9.40 % (1174052)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2975998105:i=54282_2918 on theBenchmark for (2918ds/54282Mi)
% 63.44/9.40 % TRYING [1]
% 63.44/9.40 % TRYING [2]
% 63.44/9.40 % TRYING [3]
% 63.44/9.40 % TRYING [4]
% 63.44/9.40 % TRYING [5]
% 63.44/9.40 % TRYING [6]
% 63.44/9.40 % TRYING [7]
% 63.44/9.40 % (1173984)Instruction limit reached!
% 63.44/9.40 % (1173984)------------------------------
% 63.44/9.40 % (1173984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.44/9.40 % (1173984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.44/9.40 % (1173984)CaDiCaL version: 2.1.3
% 63.44/9.40 % (1173984)Termination reason: Instruction limit
% 63.44/9.40 % (1173984)Termination phase: Saturation
% 63.44/9.40 % (1173984)Time elapsed: 0.518 s
% 63.44/9.40 % (1173984)Peak memory usage: 19 MB
% 63.44/9.40 % (1173984)Instructions burned: 871 (million)
% 63.44/9.40 % (1174054)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2177488080:i=3512:aac=none_2915 on theBenchmark for (2915ds/3512Mi)
% 63.44/9.40 % TRYING [8]
% 63.44/9.40 % (1174011) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1173838-1174011"...
% 63.44/9.40 % (1174011)...printing done.
% 63.44/9.40 % (1174011)Refutation found. Thanks to Tanya!
% 63.44/9.40 % SZS status Unsatisfiable for theBenchmark
% 63.44/9.40 % SZS output start Proof for theBenchmark
% See solution above
% 0.34/9.40 % (1174011)------------------------------
% 0.34/9.40 % (1174011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.34/9.40 % (1174011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.34/9.40 % (1174011)CaDiCaL version: 2.1.3
% 0.34/9.40 % (1174011)Termination reason: Refutation
% 0.34/9.40 % (1174011)Time elapsed: 0.984 s
% 0.34/9.40 % (1174011)Peak memory usage: 31 MB
% 0.34/9.40 % (1174011)Instructions burned: 1624 (million)
% 0.34/9.40 % (1173838)Success in time 9.026 s
% 0.34/9.40 % Vampire exiting
%------------------------------------------------------------------------------