%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : RNG009-7 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:35:06 PM UTC 2026
% Result : Unsatisfiable 97.05s 22.30s
% Output : Refutation 150.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 87
% Number of leaves : 13
% Syntax : Number of formulae : 317 ( 317 unt; 2 def)
% Number of atoms : 317 ( 316 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 307 ( 307 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : add(additive_identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_additive_identity) ).
fof(f2,axiom,
! [X0] : add(X0,additive_identity) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_additive_identity) ).
fof(f5,axiom,
! [X0] : add(X0,additive_inverse(X0)) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_additive_inverse) ).
fof(f6,plain,
! [X0] : additive_identity = add(X0,additive_inverse(X0)),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X2,X0,X1] : add(X0,add(X1,X2)) = add(add(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_for_addition) ).
fof(f8,axiom,
! [X0,X1] : add(X0,X1) = add(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_for_addition) ).
fof(f9,axiom,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_for_multiplication) ).
fof(f10,axiom,
! [X2,X0,X1] : multiply(X0,add(X1,X2)) = add(multiply(X0,X1),multiply(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distribute1) ).
fof(f11,axiom,
! [X2,X0,X1] : multiply(add(X0,X1),X2) = add(multiply(X0,X2),multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distribute2) ).
fof(f12,axiom,
! [X0] : multiply(X0,multiply(X0,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_cubed_is_x) ).
fof(f13,negated_conjecture,
multiply(a,b) = c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_times_b_is_c) ).
fof(f14,negated_conjecture,
multiply(b,a) != c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_commutativity) ).
fof(f15,plain,
c != multiply(b,a),
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF0 = multiply(a,b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f17,plain,
multiply(a,b) = sF0,
inference(reorient_equations,[],[f16]) ).
fof(f18,plain,
c = sF0,
inference(definition_folding,[],[f13,f17]) ).
fof(f19,definition,
sF1 = multiply(b,a),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f20,plain,
multiply(b,a) = sF1,
inference(reorient_equations,[],[f19]) ).
fof(f21,plain,
c != sF1,
inference(definition_folding,[],[f15,f20]) ).
fof(f23,plain,
multiply(a,b) = c,
inference(forward_demodulation,[],[f17,f18]) ).
fof(f37,plain,
! [X0,X1] : add(additive_identity,X1) = add(X0,add(additive_inverse(X0),X1)),
inference(superposition,[],[f7,f6]) ).
fof(f39,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X1,add(X0,X2)),
inference(superposition,[],[f7,f8]) ).
fof(f46,plain,
! [X0,X1] : additive_identity = add(X0,add(X1,additive_inverse(add(X0,X1)))),
inference(superposition,[],[f6,f7]) ).
fof(f48,plain,
! [X2,X0,X1] : add(X0,add(X1,X2)) = add(X2,add(X0,X1)),
inference(superposition,[],[f8,f7]) ).
fof(f50,plain,
! [X0,X1] : add(X0,add(additive_inverse(X0),X1)) = X1,
inference(forward_demodulation,[],[f37,f1]) ).
fof(f52,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(multiply(X0,X0),X1)),
inference(superposition,[],[f9,f12]) ).
fof(f54,plain,
! [X0] : multiply(a,multiply(b,X0)) = multiply(c,X0),
inference(superposition,[],[f9,f23]) ).
fof(f55,plain,
! [X0] : multiply(b,multiply(a,X0)) = multiply(sF1,X0),
inference(superposition,[],[f9,f20]) ).
fof(f58,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(multiply(X0,X1),multiply(X0,X1)))),
inference(superposition,[],[f12,f9]) ).
fof(f59,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X0,X1))))),
inference(forward_demodulation,[],[f58,f9]) ).
fof(f63,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X0,multiply(X0,X1))),
inference(forward_demodulation,[],[f52,f9]) ).
fof(f65,plain,
multiply(c,a) = multiply(a,sF1),
inference(superposition,[],[f54,f20]) ).
fof(f66,plain,
multiply(a,b) = multiply(c,multiply(b,b)),
inference(superposition,[],[f54,f12]) ).
fof(f69,plain,
c = multiply(c,multiply(b,b)),
inference(forward_demodulation,[],[f66,f23]) ).
fof(f71,plain,
! [X0,X1] : multiply(X0,add(multiply(X0,X0),X1)) = add(X0,multiply(X0,X1)),
inference(superposition,[],[f10,f12]) ).
fof(f73,plain,
! [X0] : multiply(a,add(b,X0)) = add(c,multiply(a,X0)),
inference(superposition,[],[f10,f23]) ).
fof(f75,plain,
! [X0] : multiply(b,add(a,X0)) = add(sF1,multiply(b,X0)),
inference(superposition,[],[f10,f20]) ).
fof(f76,plain,
! [X0,X1] : multiply(X0,add(X1,multiply(X0,X0))) = add(multiply(X0,X1),X0),
inference(superposition,[],[f10,f12]) ).
fof(f80,plain,
! [X0] : multiply(b,add(X0,a)) = add(multiply(b,X0),sF1),
inference(superposition,[],[f10,f20]) ).
fof(f83,plain,
! [X2,X3,X0,X1] : add(multiply(X0,X1),add(multiply(X0,X2),X3)) = add(multiply(X0,add(X1,X2)),X3),
inference(superposition,[],[f7,f10]) ).
fof(f86,plain,
! [X0] : add(sF1,multiply(b,X0)) = multiply(b,add(X0,a)),
inference(forward_demodulation,[],[f80,f8]) ).
fof(f89,plain,
! [X0,X1] : add(X0,multiply(X0,X1)) = multiply(X0,add(X1,multiply(X0,X0))),
inference(forward_demodulation,[],[f76,f8]) ).
fof(f97,plain,
! [X0] : multiply(c,multiply(a,X0)) = multiply(multiply(a,sF1),X0),
inference(superposition,[],[f9,f65]) ).
fof(f98,plain,
! [X0] : multiply(c,multiply(a,X0)) = multiply(a,multiply(sF1,X0)),
inference(forward_demodulation,[],[f97,f9]) ).
fof(f99,plain,
! [X0,X1] : multiply(add(X0,X1),multiply(X0,X0)) = add(X0,multiply(X1,multiply(X0,X0))),
inference(superposition,[],[f11,f12]) ).
fof(f101,plain,
! [X0] : multiply(add(a,X0),b) = add(c,multiply(X0,b)),
inference(superposition,[],[f11,f23]) ).
fof(f103,plain,
! [X0] : multiply(add(b,X0),a) = add(sF1,multiply(X0,a)),
inference(superposition,[],[f11,f20]) ).
fof(f105,plain,
! [X0,X1] : multiply(add(X1,X0),multiply(X0,X0)) = add(multiply(X1,multiply(X0,X0)),X0),
inference(superposition,[],[f11,f12]) ).
fof(f106,plain,
! [X2,X3,X0,X1] : multiply(add(X3,multiply(X0,X1)),X2) = add(multiply(X3,X2),multiply(X0,multiply(X1,X2))),
inference(superposition,[],[f11,f9]) ).
fof(f115,plain,
! [X2,X3,X0,X1] : add(multiply(X0,X2),add(multiply(X1,X2),X3)) = add(multiply(add(X0,X1),X2),X3),
inference(superposition,[],[f7,f11]) ).
fof(f121,plain,
! [X0,X1] : add(X0,multiply(X1,multiply(X0,X0))) = multiply(add(X1,X0),multiply(X0,X0)),
inference(forward_demodulation,[],[f105,f8]) ).
fof(f128,plain,
! [X0] : multiply(c,X0) = multiply(c,multiply(multiply(b,b),X0)),
inference(superposition,[],[f9,f69]) ).
fof(f129,plain,
! [X0] : multiply(c,X0) = multiply(c,multiply(b,multiply(b,X0))),
inference(forward_demodulation,[],[f128,f9]) ).
fof(f132,plain,
multiply(a,b) = add(c,multiply(a,additive_identity)),
inference(superposition,[],[f73,f2]) ).
fof(f133,plain,
multiply(a,additive_identity) = add(c,multiply(a,additive_inverse(b))),
inference(superposition,[],[f73,f6]) ).
fof(f140,plain,
! [X0,X1] : multiply(a,multiply(add(b,X0),X1)) = multiply(add(c,multiply(a,X0)),X1),
inference(superposition,[],[f9,f73]) ).
fof(f145,plain,
c = add(c,multiply(a,additive_identity)),
inference(forward_demodulation,[],[f132,f23]) ).
fof(f171,plain,
! [X0] : add(multiply(a,additive_identity),X0) = add(c,add(multiply(a,additive_inverse(b)),X0)),
inference(superposition,[],[f7,f133]) ).
fof(f172,plain,
multiply(a,b) = add(c,multiply(additive_identity,b)),
inference(superposition,[],[f101,f2]) ).
fof(f173,plain,
multiply(additive_identity,b) = add(c,multiply(additive_inverse(a),b)),
inference(superposition,[],[f101,f6]) ).
fof(f185,plain,
c = add(c,multiply(additive_identity,b)),
inference(forward_demodulation,[],[f172,f23]) ).
fof(f214,plain,
! [X0,X1] : add(X1,add(X0,additive_inverse(X1))) = X0,
inference(superposition,[],[f50,f8]) ).
fof(f217,plain,
! [X0] : add(X0,additive_identity) = additive_inverse(additive_inverse(X0)),
inference(superposition,[],[f50,f6]) ).
fof(f228,plain,
! [X0] : additive_inverse(additive_inverse(X0)) = X0,
inference(forward_demodulation,[],[f217,f2]) ).
fof(f244,plain,
multiply(sF1,b) = multiply(b,c),
inference(superposition,[],[f55,f23]) ).
fof(f245,plain,
! [X0] : multiply(sF1,multiply(b,X0)) = multiply(b,multiply(c,X0)),
inference(superposition,[],[f55,f54]) ).
fof(f281,plain,
additive_identity = add(c,add(multiply(a,additive_identity),additive_inverse(c))),
inference(superposition,[],[f46,f145]) ).
fof(f283,plain,
additive_identity = add(c,add(multiply(additive_identity,b),additive_inverse(c))),
inference(superposition,[],[f46,f185]) ).
fof(f307,plain,
additive_identity = multiply(additive_identity,b),
inference(forward_demodulation,[],[f283,f214]) ).
fof(f309,plain,
additive_identity = multiply(a,additive_identity),
inference(forward_demodulation,[],[f281,f214]) ).
fof(f322,plain,
additive_identity = add(c,multiply(additive_inverse(a),b)),
inference(backward_demodulation,[],[f173,f307]) ).
fof(f324,plain,
! [X0] : add(additive_identity,X0) = add(c,add(multiply(a,additive_inverse(b)),X0)),
inference(backward_demodulation,[],[f171,f309]) ).
fof(f331,plain,
! [X0] : add(c,add(multiply(a,additive_inverse(b)),X0)) = X0,
inference(forward_demodulation,[],[f324,f1]) ).
fof(f337,plain,
! [X0] : multiply(additive_identity,add(b,X0)) = add(additive_identity,multiply(additive_identity,X0)),
inference(superposition,[],[f10,f307]) ).
fof(f338,plain,
! [X0] : multiply(additive_identity,X0) = multiply(additive_identity,multiply(b,X0)),
inference(superposition,[],[f9,f307]) ).
fof(f339,plain,
! [X0] : multiply(additive_identity,X0) = multiply(additive_identity,add(b,X0)),
inference(forward_demodulation,[],[f337,f1]) ).
fof(f351,plain,
c = multiply(a,multiply(a,c)),
inference(superposition,[],[f63,f23]) ).
fof(f352,plain,
! [X0] : multiply(c,X0) = multiply(a,multiply(a,multiply(c,X0))),
inference(superposition,[],[f63,f54]) ).
fof(f355,plain,
sF1 = multiply(b,multiply(b,sF1)),
inference(superposition,[],[f63,f20]) ).
fof(f356,plain,
! [X0] : multiply(sF1,X0) = multiply(b,multiply(b,multiply(sF1,X0))),
inference(superposition,[],[f63,f55]) ).
fof(f394,plain,
multiply(sF1,additive_identity) = multiply(b,additive_identity),
inference(superposition,[],[f55,f309]) ).
fof(f582,plain,
! [X0] : multiply(add(sF1,X0),additive_identity) = add(multiply(b,additive_identity),multiply(X0,additive_identity)),
inference(superposition,[],[f11,f394]) ).
fof(f584,plain,
! [X0] : multiply(sF1,add(additive_identity,X0)) = add(multiply(b,additive_identity),multiply(sF1,X0)),
inference(superposition,[],[f10,f394]) ).
fof(f585,plain,
! [X0] : multiply(sF1,multiply(additive_identity,X0)) = multiply(multiply(b,additive_identity),X0),
inference(superposition,[],[f9,f394]) ).
fof(f586,plain,
! [X0] : multiply(sF1,multiply(additive_identity,X0)) = multiply(b,multiply(additive_identity,X0)),
inference(forward_demodulation,[],[f585,f9]) ).
fof(f587,plain,
! [X0] : multiply(sF1,X0) = add(multiply(b,additive_identity),multiply(sF1,X0)),
inference(forward_demodulation,[],[f584,f1]) ).
fof(f589,plain,
! [X0] : multiply(add(sF1,X0),additive_identity) = multiply(add(b,X0),additive_identity),
inference(forward_demodulation,[],[f582,f11]) ).
fof(f600,plain,
multiply(b,additive_identity) = add(sF1,multiply(b,additive_inverse(a))),
inference(superposition,[],[f75,f6]) ).
fof(f607,plain,
! [X0,X1] : multiply(b,multiply(add(a,X0),X1)) = multiply(add(sF1,multiply(b,X0)),X1),
inference(superposition,[],[f9,f75]) ).
fof(f618,plain,
! [X0] : add(additive_identity,X0) = add(multiply(additive_inverse(a),b),add(c,X0)),
inference(superposition,[],[f39,f322]) ).
fof(f625,plain,
! [X0] : add(additive_identity,X0) = add(c,add(X0,multiply(additive_inverse(a),b))),
inference(forward_demodulation,[],[f618,f48]) ).
fof(f628,plain,
! [X0] : add(c,add(X0,multiply(additive_inverse(a),b))) = X0,
inference(forward_demodulation,[],[f625,f1]) ).
fof(f828,plain,
! [X0] : multiply(X0,multiply(X0,X0)) = add(X0,multiply(X0,additive_identity)),
inference(superposition,[],[f71,f2]) ).
fof(f865,plain,
! [X0] : add(X0,multiply(X0,additive_identity)) = X0,
inference(forward_demodulation,[],[f828,f12]) ).
fof(f888,plain,
multiply(additive_identity,b) = multiply(additive_identity,additive_identity),
inference(superposition,[],[f339,f2]) ).
fof(f905,plain,
additive_identity = multiply(additive_identity,additive_identity),
inference(forward_demodulation,[],[f888,f307]) ).
fof(f987,plain,
! [X0] : multiply(additive_identity,X0) = multiply(additive_identity,multiply(additive_identity,X0)),
inference(superposition,[],[f9,f905]) ).
fof(f1045,plain,
! [X0] : add(c,multiply(X0,b)) = multiply(add(a,X0),multiply(b,multiply(add(a,X0),multiply(b,add(c,multiply(X0,b)))))),
inference(superposition,[],[f59,f101]) ).
fof(f1102,plain,
! [X0] : multiply(b,multiply(a,X0)) = multiply(sF1,multiply(X0,multiply(a,multiply(X0,multiply(a,X0))))),
inference(superposition,[],[f55,f59]) ).
fof(f1106,plain,
! [X0] : multiply(a,multiply(b,X0)) = multiply(c,multiply(X0,multiply(b,multiply(X0,multiply(b,X0))))),
inference(superposition,[],[f54,f59]) ).
fof(f1109,plain,
! [X0] : multiply(c,X0) = multiply(c,multiply(X0,multiply(b,multiply(X0,multiply(b,X0))))),
inference(forward_demodulation,[],[f1106,f54]) ).
fof(f1113,plain,
! [X0] : multiply(sF1,X0) = multiply(sF1,multiply(X0,multiply(a,multiply(X0,multiply(a,X0))))),
inference(forward_demodulation,[],[f1102,f55]) ).
fof(f1373,plain,
! [X0] : multiply(X0,multiply(X0,X0)) = add(X0,multiply(additive_identity,multiply(X0,X0))),
inference(superposition,[],[f99,f2]) ).
fof(f1378,plain,
! [X0] : multiply(additive_identity,multiply(X0,X0)) = add(X0,multiply(additive_inverse(X0),multiply(X0,X0))),
inference(superposition,[],[f99,f6]) ).
fof(f1408,plain,
! [X0] : add(X0,multiply(additive_identity,multiply(X0,X0))) = X0,
inference(forward_demodulation,[],[f1373,f12]) ).
fof(f1585,plain,
! [X0,X1] : add(multiply(b,add(X0,a)),X1) = add(multiply(b,X0),add(sF1,X1)),
inference(superposition,[],[f83,f20]) ).
fof(f1605,plain,
! [X2,X0,X1] : add(multiply(X0,X1),additive_identity) = add(multiply(X0,add(X1,X2)),additive_inverse(multiply(X0,X2))),
inference(superposition,[],[f83,f6]) ).
fof(f1639,plain,
! [X2,X0,X1] : add(multiply(X0,X1),additive_identity) = add(additive_inverse(multiply(X0,X2)),multiply(X0,add(X1,X2))),
inference(forward_demodulation,[],[f1605,f8]) ).
fof(f1651,plain,
! [X0,X1] : add(multiply(b,add(X0,a)),X1) = add(sF1,add(X1,multiply(b,X0))),
inference(forward_demodulation,[],[f1585,f48]) ).
fof(f1721,plain,
! [X2,X0,X1] : add(additive_inverse(multiply(X0,X2)),multiply(X0,add(X1,X2))) = add(additive_identity,multiply(X0,X1)),
inference(forward_demodulation,[],[f1639,f8]) ).
fof(f1729,plain,
! [X0,X1] : add(sF1,add(X1,multiply(b,X0))) = add(add(sF1,multiply(b,X0)),X1),
inference(forward_demodulation,[],[f1651,f86]) ).
fof(f1761,plain,
! [X2,X0,X1] : multiply(X0,X1) = add(additive_inverse(multiply(X0,X2)),multiply(X0,add(X1,X2))),
inference(forward_demodulation,[],[f1721,f1]) ).
fof(f1765,plain,
! [X0,X1] : add(sF1,add(multiply(b,X0),X1)) = add(sF1,add(X1,multiply(b,X0))),
inference(forward_demodulation,[],[f1729,f7]) ).
fof(f2219,plain,
! [X2,X0,X1] : add(multiply(X1,multiply(additive_identity,X0)),multiply(X2,multiply(additive_identity,X0))) = multiply(add(X1,multiply(X2,additive_identity)),multiply(additive_identity,X0)),
inference(superposition,[],[f106,f987]) ).
fof(f2232,plain,
! [X2,X3,X0,X1,X4] : multiply(add(X3,multiply(X4,multiply(X0,X1))),X2) = add(multiply(X3,X2),multiply(X4,multiply(X0,multiply(X1,X2)))),
inference(superposition,[],[f106,f9]) ).
fof(f2320,plain,
! [X2,X0,X1] : multiply(add(X1,X2),multiply(additive_identity,X0)) = multiply(add(X1,multiply(X2,additive_identity)),multiply(additive_identity,X0)),
inference(forward_demodulation,[],[f2219,f11]) ).
fof(f2551,plain,
! [X2,X0,X1] : add(multiply(X0,X1),additive_identity) = add(multiply(add(X0,X2),X1),additive_inverse(multiply(X2,X1))),
inference(superposition,[],[f115,f6]) ).
fof(f2589,plain,
! [X2,X0,X1] : add(multiply(X0,X1),additive_identity) = add(additive_inverse(multiply(X2,X1)),multiply(add(X0,X2),X1)),
inference(forward_demodulation,[],[f2551,f8]) ).
fof(f2673,plain,
! [X2,X0,X1] : add(additive_identity,multiply(X0,X1)) = add(additive_inverse(multiply(X2,X1)),multiply(add(X0,X2),X1)),
inference(forward_demodulation,[],[f2589,f8]) ).
fof(f2726,plain,
! [X2,X0,X1] : multiply(X0,X1) = add(additive_inverse(multiply(X2,X1)),multiply(add(X0,X2),X1)),
inference(forward_demodulation,[],[f2673,f1]) ).
fof(f2907,plain,
multiply(a,multiply(a,c)) = multiply(c,multiply(a,multiply(c,multiply(a,c)))),
inference(superposition,[],[f352,f59]) ).
fof(f2940,plain,
multiply(a,multiply(a,c)) = multiply(a,multiply(sF1,multiply(c,multiply(a,c)))),
inference(forward_demodulation,[],[f2907,f98]) ).
fof(f2946,plain,
multiply(a,multiply(a,c)) = multiply(a,multiply(sF1,multiply(a,multiply(sF1,c)))),
inference(forward_demodulation,[],[f2940,f98]) ).
fof(f2948,plain,
c = multiply(a,multiply(sF1,multiply(a,multiply(sF1,c)))),
inference(forward_demodulation,[],[f2946,f351]) ).
fof(f3002,plain,
multiply(a,additive_inverse(b)) = multiply(additive_inverse(a),b),
inference(superposition,[],[f331,f628]) ).
fof(f3003,plain,
multiply(additive_inverse(a),b) = additive_inverse(c),
inference(superposition,[],[f50,f628]) ).
fof(f3030,plain,
multiply(a,additive_inverse(b)) = additive_inverse(c),
inference(forward_demodulation,[],[f3002,f3003]) ).
fof(f3203,plain,
additive_inverse(c) = multiply(a,multiply(a,additive_inverse(c))),
inference(superposition,[],[f63,f3030]) ).
fof(f4651,plain,
! [X0] : multiply(add(c,additive_inverse(c)),X0) = multiply(a,multiply(add(b,multiply(a,additive_inverse(c))),X0)),
inference(superposition,[],[f140,f3203]) ).
fof(f4759,plain,
! [X0] : multiply(additive_identity,X0) = multiply(a,multiply(add(b,multiply(a,additive_inverse(c))),X0)),
inference(forward_demodulation,[],[f4651,f6]) ).
fof(f5901,plain,
multiply(b,c) = multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,c)))),
inference(superposition,[],[f55,f2948]) ).
fof(f6233,plain,
! [X0,X1] : multiply(multiply(c,X0),X1) = multiply(c,multiply(multiply(X0,multiply(b,multiply(X0,multiply(b,X0)))),X1)),
inference(superposition,[],[f9,f1109]) ).
fof(f6256,plain,
! [X0,X1] : multiply(multiply(c,X0),X1) = multiply(c,multiply(X0,multiply(multiply(b,multiply(X0,multiply(b,X0))),X1))),
inference(forward_demodulation,[],[f6233,f9]) ).
fof(f6289,plain,
! [X0,X1] : multiply(multiply(c,X0),X1) = multiply(c,multiply(X0,multiply(b,multiply(multiply(X0,multiply(b,X0)),X1)))),
inference(forward_demodulation,[],[f6256,f9]) ).
fof(f6309,plain,
! [X0,X1] : multiply(multiply(c,X0),X1) = multiply(c,multiply(X0,multiply(b,multiply(X0,multiply(multiply(b,X0),X1))))),
inference(forward_demodulation,[],[f6289,f9]) ).
fof(f6325,plain,
! [X0,X1] : multiply(multiply(c,X0),X1) = multiply(c,multiply(X0,multiply(b,multiply(X0,multiply(b,multiply(X0,X1)))))),
inference(forward_demodulation,[],[f6309,f9]) ).
fof(f6339,plain,
! [X0,X1] : multiply(c,multiply(X0,X1)) = multiply(c,multiply(X0,multiply(b,multiply(X0,multiply(b,multiply(X0,X1)))))),
inference(forward_demodulation,[],[f6325,f9]) ).
fof(f7853,plain,
! [X0] : multiply(b,multiply(additive_identity,X0)) = multiply(sF1,multiply(sF1,multiply(b,multiply(additive_identity,X0)))),
inference(superposition,[],[f63,f586]) ).
fof(f7868,plain,
! [X0] : multiply(b,multiply(additive_identity,X0)) = multiply(sF1,multiply(b,multiply(c,multiply(additive_identity,X0)))),
inference(forward_demodulation,[],[f7853,f245]) ).
fof(f7886,plain,
! [X0] : multiply(b,multiply(additive_identity,X0)) = multiply(b,multiply(c,multiply(c,multiply(additive_identity,X0)))),
inference(forward_demodulation,[],[f7868,f245]) ).
fof(f8122,plain,
multiply(sF1,multiply(sF1,sF1)) = add(sF1,multiply(sF1,multiply(b,additive_identity))),
inference(superposition,[],[f89,f587]) ).
fof(f8138,plain,
multiply(sF1,multiply(sF1,sF1)) = add(sF1,multiply(b,multiply(c,additive_identity))),
inference(forward_demodulation,[],[f8122,f245]) ).
fof(f8155,plain,
sF1 = add(sF1,multiply(b,multiply(c,additive_identity))),
inference(forward_demodulation,[],[f8138,f12]) ).
fof(f8374,plain,
additive_identity = add(sF1,add(multiply(b,multiply(c,additive_identity)),additive_inverse(sF1))),
inference(superposition,[],[f46,f8155]) ).
fof(f8378,plain,
multiply(sF1,multiply(multiply(b,multiply(c,additive_identity)),multiply(b,multiply(c,additive_identity)))) = add(multiply(b,multiply(c,additive_identity)),multiply(sF1,multiply(multiply(b,multiply(c,additive_identity)),multiply(b,multiply(c,additive_identity))))),
inference(superposition,[],[f121,f8155]) ).
fof(f8379,plain,
multiply(sF1,multiply(multiply(b,multiply(c,additive_identity)),multiply(b,multiply(c,additive_identity)))) = multiply(add(b,multiply(sF1,multiply(multiply(b,multiply(c,additive_identity)),b))),multiply(c,additive_identity)),
inference(forward_demodulation,[],[f8378,f2232]) ).
fof(f8382,plain,
additive_identity = add(sF1,add(additive_inverse(sF1),multiply(b,multiply(c,additive_identity)))),
inference(forward_demodulation,[],[f8374,f1765]) ).
fof(f8385,plain,
multiply(sF1,multiply(multiply(b,multiply(c,additive_identity)),multiply(b,multiply(c,additive_identity)))) = multiply(add(b,multiply(sF1,multiply(b,multiply(multiply(c,additive_identity),b)))),multiply(c,additive_identity)),
inference(forward_demodulation,[],[f8379,f9]) ).
fof(f8387,plain,
additive_identity = multiply(b,multiply(c,additive_identity)),
inference(forward_demodulation,[],[f8382,f50]) ).
fof(f8388,plain,
multiply(sF1,multiply(multiply(b,multiply(c,additive_identity)),multiply(b,multiply(c,additive_identity)))) = multiply(add(b,multiply(b,multiply(c,multiply(multiply(c,additive_identity),b)))),multiply(c,additive_identity)),
inference(forward_demodulation,[],[f8385,f245]) ).
fof(f8394,plain,
multiply(sF1,multiply(multiply(b,multiply(c,additive_identity)),multiply(b,multiply(c,additive_identity)))) = multiply(add(b,multiply(b,multiply(c,multiply(c,multiply(additive_identity,b))))),multiply(c,additive_identity)),
inference(forward_demodulation,[],[f8388,f9]) ).
fof(f8397,plain,
multiply(sF1,multiply(multiply(b,multiply(c,additive_identity)),multiply(b,multiply(c,additive_identity)))) = multiply(add(b,multiply(b,multiply(additive_identity,b))),multiply(c,additive_identity)),
inference(forward_demodulation,[],[f8394,f7886]) ).
fof(f8398,plain,
multiply(sF1,multiply(multiply(b,multiply(c,additive_identity)),multiply(b,multiply(c,additive_identity)))) = multiply(add(b,multiply(b,additive_identity)),multiply(c,additive_identity)),
inference(forward_demodulation,[],[f8397,f307]) ).
fof(f8399,plain,
multiply(b,multiply(c,additive_identity)) = multiply(sF1,multiply(multiply(b,multiply(c,additive_identity)),multiply(b,multiply(c,additive_identity)))),
inference(forward_demodulation,[],[f8398,f865]) ).
fof(f8400,plain,
multiply(b,multiply(c,additive_identity)) = multiply(sF1,multiply(b,multiply(multiply(c,additive_identity),multiply(b,multiply(c,additive_identity))))),
inference(forward_demodulation,[],[f8399,f9]) ).
fof(f8401,plain,
multiply(b,multiply(c,additive_identity)) = multiply(b,multiply(c,multiply(multiply(c,additive_identity),multiply(b,multiply(c,additive_identity))))),
inference(forward_demodulation,[],[f8400,f245]) ).
fof(f8402,plain,
multiply(b,multiply(c,additive_identity)) = multiply(b,multiply(c,multiply(c,multiply(additive_identity,multiply(b,multiply(c,additive_identity)))))),
inference(forward_demodulation,[],[f8401,f9]) ).
fof(f8403,plain,
multiply(b,multiply(c,additive_identity)) = multiply(b,multiply(additive_identity,multiply(b,multiply(c,additive_identity)))),
inference(forward_demodulation,[],[f8402,f7886]) ).
fof(f8404,plain,
multiply(b,multiply(c,additive_identity)) = multiply(b,multiply(additive_identity,multiply(c,additive_identity))),
inference(forward_demodulation,[],[f8403,f338]) ).
fof(f8405,plain,
additive_identity = multiply(b,multiply(additive_identity,multiply(c,additive_identity))),
inference(forward_demodulation,[],[f8404,f8387]) ).
fof(f8588,plain,
multiply(a,additive_identity) = multiply(c,multiply(c,additive_identity)),
inference(superposition,[],[f54,f8387]) ).
fof(f8591,plain,
multiply(c,multiply(c,additive_identity)) = multiply(c,multiply(b,additive_identity)),
inference(superposition,[],[f129,f8387]) ).
fof(f8593,plain,
multiply(additive_identity,additive_identity) = multiply(additive_identity,multiply(c,additive_identity)),
inference(superposition,[],[f338,f8387]) ).
fof(f8601,plain,
! [X0] : multiply(add(b,X0),multiply(c,additive_identity)) = add(additive_identity,multiply(X0,multiply(c,additive_identity))),
inference(superposition,[],[f11,f8387]) ).
fof(f8621,plain,
! [X0] : multiply(X0,multiply(c,additive_identity)) = multiply(add(b,X0),multiply(c,additive_identity)),
inference(forward_demodulation,[],[f8601,f1]) ).
fof(f8629,plain,
additive_identity = multiply(additive_identity,multiply(c,additive_identity)),
inference(forward_demodulation,[],[f8593,f905]) ).
fof(f8634,plain,
additive_identity = multiply(c,multiply(c,additive_identity)),
inference(forward_demodulation,[],[f8588,f309]) ).
fof(f8645,plain,
additive_identity = multiply(b,additive_identity),
inference(backward_demodulation,[],[f8405,f8629]) ).
fof(f8648,plain,
additive_identity = multiply(c,multiply(b,additive_identity)),
inference(backward_demodulation,[],[f8591,f8634]) ).
fof(f8658,plain,
additive_identity = add(sF1,multiply(b,additive_inverse(a))),
inference(backward_demodulation,[],[f600,f8645]) ).
fof(f8669,plain,
additive_identity = multiply(c,additive_identity),
inference(forward_demodulation,[],[f8648,f8645]) ).
fof(f8680,plain,
! [X0] : multiply(X0,additive_identity) = multiply(add(b,X0),additive_identity),
inference(backward_demodulation,[],[f8621,f8669]) ).
fof(f8693,plain,
! [X0] : multiply(X0,additive_identity) = multiply(add(sF1,X0),additive_identity),
inference(backward_demodulation,[],[f589,f8680]) ).
fof(f8705,plain,
! [X0] : add(additive_identity,X0) = add(multiply(b,additive_inverse(a)),add(sF1,X0)),
inference(superposition,[],[f39,f8658]) ).
fof(f8716,plain,
! [X0] : add(additive_identity,X0) = add(sF1,add(X0,multiply(b,additive_inverse(a)))),
inference(forward_demodulation,[],[f8705,f48]) ).
fof(f8723,plain,
! [X0] : add(sF1,add(X0,multiply(b,additive_inverse(a)))) = X0,
inference(forward_demodulation,[],[f8716,f1]) ).
fof(f9500,plain,
! [X0] : multiply(additive_identity,additive_identity) = multiply(add(X0,additive_inverse(add(sF1,X0))),additive_identity),
inference(superposition,[],[f8693,f46]) ).
fof(f9554,plain,
! [X0] : additive_identity = multiply(add(X0,additive_inverse(add(sF1,X0))),additive_identity),
inference(forward_demodulation,[],[f9500,f905]) ).
fof(f14655,plain,
multiply(b,additive_inverse(a)) = additive_inverse(sF1),
inference(superposition,[],[f50,f8723]) ).
fof(f15059,plain,
additive_inverse(sF1) = multiply(b,multiply(b,additive_inverse(sF1))),
inference(superposition,[],[f63,f14655]) ).
fof(f17085,plain,
! [X0,X1] : multiply(additive_identity,X1) = multiply(add(X0,additive_inverse(add(sF1,X0))),multiply(additive_identity,X1)),
inference(superposition,[],[f9,f9554]) ).
fof(f18994,plain,
! [X0] : additive_identity = add(X0,add(multiply(X0,additive_identity),additive_inverse(X0))),
inference(superposition,[],[f46,f865]) ).
fof(f19099,plain,
! [X0] : additive_identity = multiply(X0,additive_identity),
inference(forward_demodulation,[],[f18994,f214]) ).
fof(f19204,plain,
! [X2,X0,X1] : multiply(add(X1,X2),multiply(additive_identity,X0)) = multiply(add(X1,additive_identity),multiply(additive_identity,X0)),
inference(backward_demodulation,[],[f2320,f19099]) ).
fof(f19525,plain,
! [X2,X0,X1] : multiply(X1,multiply(additive_identity,X0)) = multiply(add(X1,X2),multiply(additive_identity,X0)),
inference(forward_demodulation,[],[f19204,f2]) ).
fof(f19604,plain,
! [X0,X1] : multiply(additive_identity,X1) = multiply(X0,multiply(additive_identity,X1)),
inference(backward_demodulation,[],[f17085,f19525]) ).
fof(f20655,plain,
! [X0] : additive_identity = add(X0,add(multiply(additive_identity,multiply(X0,X0)),additive_inverse(X0))),
inference(superposition,[],[f46,f1408]) ).
fof(f20742,plain,
! [X0] : additive_identity = multiply(additive_identity,multiply(X0,X0)),
inference(forward_demodulation,[],[f20655,f214]) ).
fof(f20801,plain,
! [X0] : additive_identity = add(X0,multiply(additive_inverse(X0),multiply(X0,X0))),
inference(backward_demodulation,[],[f1378,f20742]) ).
fof(f21887,plain,
! [X0] : additive_identity = add(multiply(additive_identity,X0),multiply(additive_inverse(multiply(additive_identity,X0)),multiply(additive_identity,X0))),
inference(superposition,[],[f20801,f19604]) ).
fof(f21997,plain,
! [X0] : additive_identity = multiply(add(additive_identity,multiply(additive_inverse(multiply(additive_identity,X0)),additive_identity)),X0),
inference(forward_demodulation,[],[f21887,f106]) ).
fof(f22036,plain,
! [X0] : additive_identity = multiply(multiply(additive_inverse(multiply(additive_identity,X0)),additive_identity),X0),
inference(forward_demodulation,[],[f21997,f1]) ).
fof(f22068,plain,
! [X0] : additive_identity = multiply(additive_inverse(multiply(additive_identity,X0)),multiply(additive_identity,X0)),
inference(forward_demodulation,[],[f22036,f9]) ).
fof(f22097,plain,
! [X0] : additive_identity = multiply(additive_identity,X0),
inference(forward_demodulation,[],[f22068,f19604]) ).
fof(f22139,plain,
! [X0] : additive_identity = multiply(a,multiply(add(b,multiply(a,additive_inverse(c))),X0)),
inference(backward_demodulation,[],[f4759,f22097]) ).
fof(f23045,plain,
multiply(b,multiply(b,sF1)) = multiply(sF1,multiply(b,multiply(sF1,multiply(b,sF1)))),
inference(superposition,[],[f356,f59]) ).
fof(f23085,plain,
multiply(b,multiply(b,sF1)) = multiply(b,multiply(c,multiply(sF1,multiply(b,sF1)))),
inference(forward_demodulation,[],[f23045,f245]) ).
fof(f23092,plain,
multiply(b,multiply(b,sF1)) = multiply(b,multiply(c,multiply(b,multiply(c,sF1)))),
inference(forward_demodulation,[],[f23085,f245]) ).
fof(f23095,plain,
sF1 = multiply(b,multiply(c,multiply(b,multiply(c,sF1)))),
inference(forward_demodulation,[],[f23092,f355]) ).
fof(f24548,plain,
multiply(a,sF1) = multiply(c,multiply(c,multiply(b,multiply(c,sF1)))),
inference(superposition,[],[f54,f23095]) ).
fof(f24553,plain,
multiply(c,multiply(c,multiply(b,multiply(c,sF1)))) = multiply(c,multiply(multiply(c,multiply(b,multiply(c,sF1))),multiply(b,multiply(multiply(c,multiply(b,multiply(c,sF1))),sF1)))),
inference(superposition,[],[f1109,f23095]) ).
fof(f24583,plain,
multiply(c,multiply(c,multiply(b,multiply(c,sF1)))) = multiply(c,multiply(c,multiply(multiply(b,multiply(c,sF1)),multiply(b,multiply(multiply(c,multiply(b,multiply(c,sF1))),sF1))))),
inference(forward_demodulation,[],[f24553,f9]) ).
fof(f24593,plain,
multiply(c,multiply(c,multiply(b,multiply(c,sF1)))) = multiply(c,multiply(c,multiply(b,multiply(multiply(c,sF1),multiply(b,multiply(multiply(c,multiply(b,multiply(c,sF1))),sF1)))))),
inference(forward_demodulation,[],[f24583,f9]) ).
fof(f24599,plain,
multiply(c,multiply(c,multiply(b,multiply(c,sF1)))) = multiply(c,multiply(c,multiply(b,multiply(c,multiply(sF1,multiply(b,multiply(multiply(c,multiply(b,multiply(c,sF1))),sF1))))))),
inference(forward_demodulation,[],[f24593,f9]) ).
fof(f24601,plain,
multiply(c,multiply(c,multiply(b,multiply(c,sF1)))) = multiply(c,multiply(c,multiply(b,multiply(c,multiply(b,multiply(c,multiply(multiply(c,multiply(b,multiply(c,sF1))),sF1))))))),
inference(forward_demodulation,[],[f24599,f245]) ).
fof(f24603,plain,
multiply(c,multiply(c,multiply(b,multiply(c,sF1)))) = multiply(c,multiply(c,multiply(multiply(c,multiply(b,multiply(c,sF1))),sF1))),
inference(forward_demodulation,[],[f24601,f6339]) ).
fof(f24605,plain,
multiply(c,multiply(c,multiply(b,multiply(c,sF1)))) = multiply(c,multiply(c,multiply(c,multiply(multiply(b,multiply(c,sF1)),sF1)))),
inference(forward_demodulation,[],[f24603,f9]) ).
fof(f24607,plain,
multiply(c,multiply(c,multiply(b,multiply(c,sF1)))) = multiply(c,multiply(multiply(b,multiply(c,sF1)),sF1)),
inference(forward_demodulation,[],[f24605,f63]) ).
fof(f24609,plain,
multiply(c,multiply(c,multiply(b,multiply(c,sF1)))) = multiply(c,multiply(b,multiply(multiply(c,sF1),sF1))),
inference(forward_demodulation,[],[f24607,f9]) ).
fof(f24610,plain,
multiply(c,multiply(c,multiply(b,multiply(c,sF1)))) = multiply(c,multiply(b,multiply(c,multiply(sF1,sF1)))),
inference(forward_demodulation,[],[f24609,f9]) ).
fof(f24611,plain,
multiply(a,sF1) = multiply(c,multiply(b,multiply(c,multiply(sF1,sF1)))),
inference(forward_demodulation,[],[f24610,f24548]) ).
fof(f29580,plain,
! [X0,X1] : multiply(X0,X1) = add(additive_inverse(multiply(X0,additive_inverse(X1))),multiply(X0,additive_identity)),
inference(superposition,[],[f1761,f6]) ).
fof(f29771,plain,
! [X0,X1] : multiply(X0,X1) = add(multiply(X0,additive_identity),additive_inverse(multiply(X0,additive_inverse(X1)))),
inference(forward_demodulation,[],[f29580,f8]) ).
fof(f29879,plain,
! [X0,X1] : multiply(X0,X1) = add(additive_identity,additive_inverse(multiply(X0,additive_inverse(X1)))),
inference(forward_demodulation,[],[f29771,f19099]) ).
fof(f29949,plain,
! [X0,X1] : multiply(X0,X1) = additive_inverse(multiply(X0,additive_inverse(X1))),
inference(forward_demodulation,[],[f29879,f1]) ).
fof(f30151,plain,
! [X0,X1] : multiply(X0,X1) = add(additive_inverse(multiply(additive_inverse(X0),X1)),multiply(additive_identity,X1)),
inference(superposition,[],[f2726,f6]) ).
fof(f30159,plain,
! [X2,X3,X0,X1] : multiply(additive_inverse(multiply(X0,X2)),X3) = add(additive_inverse(multiply(multiply(X0,add(X1,X2)),X3)),multiply(multiply(X0,X1),X3)),
inference(superposition,[],[f2726,f1761]) ).
fof(f30262,plain,
! [X2,X3,X0,X1] : multiply(X2,additive_inverse(multiply(X3,X1))) = add(additive_inverse(multiply(X2,multiply(add(X0,X3),X1))),multiply(X2,multiply(X0,X1))),
inference(superposition,[],[f1761,f2726]) ).
fof(f30263,plain,
! [X2,X3,X0,X1] : multiply(X2,additive_inverse(multiply(X3,X1))) = add(multiply(X2,multiply(X0,X1)),additive_inverse(multiply(X2,multiply(add(X0,X3),X1)))),
inference(forward_demodulation,[],[f30262,f8]) ).
fof(f30354,plain,
! [X2,X3,X0,X1] : multiply(additive_inverse(multiply(X0,X2)),X3) = add(multiply(multiply(X0,X1),X3),additive_inverse(multiply(multiply(X0,add(X1,X2)),X3))),
inference(forward_demodulation,[],[f30159,f8]) ).
fof(f30360,plain,
! [X0,X1] : multiply(X0,X1) = add(multiply(additive_identity,X1),additive_inverse(multiply(additive_inverse(X0),X1))),
inference(forward_demodulation,[],[f30151,f8]) ).
fof(f30478,plain,
! [X2,X3,X0,X1] : multiply(additive_inverse(multiply(X0,X2)),X3) = add(multiply(multiply(X0,X1),X3),additive_inverse(multiply(X0,multiply(add(X1,X2),X3)))),
inference(forward_demodulation,[],[f30354,f9]) ).
fof(f30484,plain,
! [X0,X1] : multiply(X0,X1) = add(additive_identity,additive_inverse(multiply(additive_inverse(X0),X1))),
inference(forward_demodulation,[],[f30360,f22097]) ).
fof(f30562,plain,
! [X2,X3,X0,X1] : multiply(additive_inverse(multiply(X0,X2)),X3) = add(multiply(X0,multiply(X1,X3)),additive_inverse(multiply(X0,multiply(add(X1,X2),X3)))),
inference(forward_demodulation,[],[f30478,f9]) ).
fof(f30566,plain,
! [X0,X1] : multiply(X0,X1) = additive_inverse(multiply(additive_inverse(X0),X1)),
inference(forward_demodulation,[],[f30484,f1]) ).
fof(f30608,plain,
! [X2,X3,X0] : multiply(additive_inverse(multiply(X0,X2)),X3) = multiply(X0,additive_inverse(multiply(X2,X3))),
inference(forward_demodulation,[],[f30562,f30263]) ).
fof(f30909,plain,
! [X0,X1] : additive_inverse(multiply(X0,X1)) = multiply(additive_inverse(X0),X1),
inference(superposition,[],[f228,f30566]) ).
fof(f30948,plain,
! [X2,X3,X0] : additive_inverse(multiply(multiply(X0,X2),X3)) = multiply(X0,additive_inverse(multiply(X2,X3))),
inference(backward_demodulation,[],[f30608,f30909]) ).
fof(f31172,plain,
! [X2,X3,X0] : additive_inverse(multiply(X0,multiply(X2,X3))) = multiply(X0,additive_inverse(multiply(X2,X3))),
inference(forward_demodulation,[],[f30948,f9]) ).
fof(f32295,plain,
! [X2,X3,X0,X1] : multiply(add(X2,multiply(X3,additive_inverse(X0))),X1) = add(multiply(X2,X1),multiply(X3,additive_inverse(multiply(X0,X1)))),
inference(superposition,[],[f106,f30909]) ).
fof(f32337,plain,
! [X2,X3,X0,X1] : multiply(add(X3,multiply(additive_inverse(X0),X1)),X2) = add(multiply(X3,X2),additive_inverse(multiply(X0,multiply(X1,X2)))),
inference(superposition,[],[f106,f30909]) ).
fof(f32401,plain,
! [X2,X3,X0,X1] : add(multiply(X3,X2),additive_inverse(multiply(X0,multiply(X1,X2)))) = multiply(add(X3,additive_inverse(multiply(X0,X1))),X2),
inference(forward_demodulation,[],[f32337,f30909]) ).
fof(f32441,plain,
! [X2,X3,X0,X1] : multiply(add(X2,multiply(X3,additive_inverse(X0))),X1) = add(multiply(X2,X1),additive_inverse(multiply(X3,multiply(X0,X1)))),
inference(forward_demodulation,[],[f32295,f31172]) ).
fof(f32562,plain,
! [X2,X3,X0,X1] : multiply(add(X2,multiply(X3,additive_inverse(X0))),X1) = multiply(add(X2,additive_inverse(multiply(X3,X0))),X1),
inference(forward_demodulation,[],[f32441,f32401]) ).
fof(f32658,plain,
! [X0] : additive_identity = multiply(a,multiply(add(b,additive_inverse(multiply(a,c))),X0)),
inference(backward_demodulation,[],[f22139,f32562]) ).
fof(f37500,plain,
multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,c)))) = multiply(sF1,multiply(multiply(sF1,multiply(a,multiply(sF1,c))),multiply(a,multiply(multiply(sF1,multiply(a,multiply(sF1,c))),c)))),
inference(superposition,[],[f1113,f2948]) ).
fof(f37562,plain,
! [X0,X1] : multiply(multiply(sF1,X0),X1) = multiply(sF1,multiply(multiply(X0,multiply(a,multiply(X0,multiply(a,X0)))),X1)),
inference(superposition,[],[f9,f1113]) ).
fof(f37590,plain,
! [X0,X1] : multiply(multiply(sF1,X0),X1) = multiply(sF1,multiply(X0,multiply(multiply(a,multiply(X0,multiply(a,X0))),X1))),
inference(forward_demodulation,[],[f37562,f9]) ).
fof(f37640,plain,
multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,c)))) = multiply(sF1,multiply(sF1,multiply(multiply(a,multiply(sF1,c)),multiply(a,multiply(multiply(sF1,multiply(a,multiply(sF1,c))),c))))),
inference(forward_demodulation,[],[f37500,f9]) ).
fof(f37652,plain,
! [X0,X1] : multiply(multiply(sF1,X0),X1) = multiply(sF1,multiply(X0,multiply(a,multiply(multiply(X0,multiply(a,X0)),X1)))),
inference(forward_demodulation,[],[f37590,f9]) ).
fof(f37687,plain,
multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,c)))) = multiply(sF1,multiply(sF1,multiply(a,multiply(multiply(sF1,c),multiply(a,multiply(multiply(sF1,multiply(a,multiply(sF1,c))),c)))))),
inference(forward_demodulation,[],[f37640,f9]) ).
fof(f37697,plain,
! [X0,X1] : multiply(multiply(sF1,X0),X1) = multiply(sF1,multiply(X0,multiply(a,multiply(X0,multiply(multiply(a,X0),X1))))),
inference(forward_demodulation,[],[f37652,f9]) ).
fof(f37728,plain,
multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,c)))) = multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,multiply(c,multiply(a,multiply(multiply(sF1,multiply(a,multiply(sF1,c))),c))))))),
inference(forward_demodulation,[],[f37687,f9]) ).
fof(f37738,plain,
! [X0,X1] : multiply(multiply(sF1,X0),X1) = multiply(sF1,multiply(X0,multiply(a,multiply(X0,multiply(a,multiply(X0,X1)))))),
inference(forward_demodulation,[],[f37697,f9]) ).
fof(f37751,plain,
multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,c)))) = multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,multiply(a,multiply(sF1,multiply(multiply(sF1,multiply(a,multiply(sF1,c))),c))))))),
inference(forward_demodulation,[],[f37728,f98]) ).
fof(f37761,plain,
! [X0,X1] : multiply(sF1,multiply(X0,X1)) = multiply(sF1,multiply(X0,multiply(a,multiply(X0,multiply(a,multiply(X0,X1)))))),
inference(forward_demodulation,[],[f37738,f9]) ).
fof(f37773,plain,
multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,c)))) = multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,multiply(a,multiply(sF1,multiply(sF1,multiply(multiply(a,multiply(sF1,c)),c)))))))),
inference(forward_demodulation,[],[f37751,f9]) ).
fof(f37790,plain,
multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,c)))) = multiply(sF1,multiply(sF1,multiply(sF1,multiply(multiply(a,multiply(sF1,c)),c)))),
inference(forward_demodulation,[],[f37773,f37761]) ).
fof(f37804,plain,
multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,c)))) = multiply(sF1,multiply(multiply(a,multiply(sF1,c)),c)),
inference(forward_demodulation,[],[f37790,f63]) ).
fof(f37814,plain,
multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,c)))) = multiply(sF1,multiply(a,multiply(multiply(sF1,c),c))),
inference(forward_demodulation,[],[f37804,f9]) ).
fof(f37822,plain,
multiply(sF1,multiply(sF1,multiply(a,multiply(sF1,c)))) = multiply(sF1,multiply(a,multiply(sF1,multiply(c,c)))),
inference(forward_demodulation,[],[f37814,f9]) ).
fof(f37828,plain,
multiply(b,c) = multiply(sF1,multiply(a,multiply(sF1,multiply(c,c)))),
inference(forward_demodulation,[],[f37822,f5901]) ).
fof(f38465,plain,
multiply(add(b,additive_inverse(multiply(a,c))),a) = multiply(add(b,additive_inverse(multiply(a,c))),additive_identity),
inference(superposition,[],[f59,f32658]) ).
fof(f38507,plain,
additive_identity = multiply(add(b,additive_inverse(multiply(a,c))),a),
inference(forward_demodulation,[],[f38465,f19099]) ).
fof(f38567,plain,
additive_identity = add(sF1,multiply(additive_inverse(multiply(a,c)),a)),
inference(forward_demodulation,[],[f38507,f103]) ).
fof(f38612,plain,
additive_identity = add(sF1,additive_inverse(multiply(multiply(a,c),a))),
inference(forward_demodulation,[],[f38567,f30909]) ).
fof(f38642,plain,
additive_identity = add(sF1,additive_inverse(multiply(a,multiply(c,a)))),
inference(forward_demodulation,[],[f38612,f9]) ).
fof(f38662,plain,
additive_identity = add(sF1,additive_inverse(multiply(a,multiply(a,sF1)))),
inference(forward_demodulation,[],[f38642,f65]) ).
fof(f39475,plain,
sF1 = add(multiply(a,multiply(a,sF1)),additive_identity),
inference(superposition,[],[f214,f38662]) ).
fof(f39502,plain,
sF1 = add(additive_identity,multiply(a,multiply(a,sF1))),
inference(forward_demodulation,[],[f39475,f8]) ).
fof(f39515,plain,
sF1 = multiply(a,multiply(a,sF1)),
inference(forward_demodulation,[],[f39502,f1]) ).
fof(f40159,plain,
multiply(b,sF1) = multiply(sF1,multiply(a,sF1)),
inference(superposition,[],[f55,f39515]) ).
fof(f40184,plain,
! [X0] : multiply(sF1,X0) = multiply(a,multiply(multiply(a,sF1),X0)),
inference(superposition,[],[f9,f39515]) ).
fof(f40212,plain,
! [X0] : multiply(sF1,X0) = multiply(a,multiply(a,multiply(sF1,X0))),
inference(forward_demodulation,[],[f40184,f9]) ).
fof(f40942,plain,
! [X0] : multiply(multiply(b,sF1),X0) = multiply(sF1,multiply(multiply(a,sF1),X0)),
inference(superposition,[],[f9,f40159]) ).
fof(f40976,plain,
! [X0] : multiply(multiply(b,sF1),X0) = multiply(sF1,multiply(a,multiply(sF1,X0))),
inference(forward_demodulation,[],[f40942,f9]) ).
fof(f40994,plain,
! [X0] : multiply(b,multiply(sF1,X0)) = multiply(sF1,multiply(a,multiply(sF1,X0))),
inference(forward_demodulation,[],[f40976,f9]) ).
fof(f41020,plain,
multiply(b,c) = multiply(b,multiply(sF1,multiply(c,c))),
inference(backward_demodulation,[],[f37828,f40994]) ).
fof(f41251,plain,
multiply(b,multiply(b,c)) = multiply(sF1,multiply(c,c)),
inference(superposition,[],[f356,f41020]) ).
fof(f42061,plain,
! [X0] : multiply(add(sF1,additive_inverse(sF1)),X0) = multiply(b,multiply(add(a,multiply(b,additive_inverse(sF1))),X0)),
inference(superposition,[],[f607,f15059]) ).
fof(f42386,plain,
! [X0] : multiply(add(sF1,additive_inverse(sF1)),X0) = multiply(b,multiply(add(a,additive_inverse(multiply(b,sF1))),X0)),
inference(forward_demodulation,[],[f42061,f32562]) ).
fof(f42474,plain,
! [X0] : multiply(additive_identity,X0) = multiply(b,multiply(add(a,additive_inverse(multiply(b,sF1))),X0)),
inference(forward_demodulation,[],[f42386,f6]) ).
fof(f42526,plain,
! [X0] : additive_identity = multiply(b,multiply(add(a,additive_inverse(multiply(b,sF1))),X0)),
inference(forward_demodulation,[],[f42474,f22097]) ).
fof(f43515,plain,
multiply(b,sF1) = multiply(a,multiply(a,multiply(b,sF1))),
inference(superposition,[],[f40212,f40159]) ).
fof(f43614,plain,
multiply(b,sF1) = multiply(a,multiply(c,sF1)),
inference(forward_demodulation,[],[f43515,f54]) ).
fof(f44244,plain,
! [X0] : multiply(multiply(b,sF1),X0) = multiply(a,multiply(multiply(c,sF1),X0)),
inference(superposition,[],[f9,f43614]) ).
fof(f44276,plain,
! [X0] : multiply(multiply(b,sF1),X0) = multiply(a,multiply(c,multiply(sF1,X0))),
inference(forward_demodulation,[],[f44244,f9]) ).
fof(f44302,plain,
! [X0] : multiply(b,multiply(sF1,X0)) = multiply(a,multiply(c,multiply(sF1,X0))),
inference(forward_demodulation,[],[f44276,f9]) ).
fof(f47895,plain,
add(c,multiply(additive_inverse(multiply(b,sF1)),b)) = multiply(add(a,additive_inverse(multiply(b,sF1))),additive_identity),
inference(superposition,[],[f1045,f42526]) ).
fof(f47978,plain,
additive_identity = add(c,multiply(additive_inverse(multiply(b,sF1)),b)),
inference(forward_demodulation,[],[f47895,f19099]) ).
fof(f48030,plain,
additive_identity = add(c,additive_inverse(multiply(multiply(b,sF1),b))),
inference(forward_demodulation,[],[f47978,f30909]) ).
fof(f48064,plain,
additive_identity = add(c,additive_inverse(multiply(b,multiply(sF1,b)))),
inference(forward_demodulation,[],[f48030,f9]) ).
fof(f48087,plain,
additive_identity = add(c,additive_inverse(multiply(b,multiply(b,c)))),
inference(forward_demodulation,[],[f48064,f244]) ).
fof(f48400,plain,
c = add(multiply(b,multiply(b,c)),additive_identity),
inference(superposition,[],[f214,f48087]) ).
fof(f48427,plain,
c = add(additive_identity,multiply(b,multiply(b,c))),
inference(forward_demodulation,[],[f48400,f8]) ).
fof(f48440,plain,
c = multiply(b,multiply(b,c)),
inference(forward_demodulation,[],[f48427,f1]) ).
fof(f48450,plain,
c = multiply(sF1,multiply(c,c)),
inference(backward_demodulation,[],[f41251,f48440]) ).
fof(f48868,plain,
! [X0] : multiply(c,X0) = multiply(sF1,multiply(multiply(c,c),X0)),
inference(superposition,[],[f9,f48450]) ).
fof(f48906,plain,
! [X0] : multiply(c,X0) = multiply(sF1,multiply(c,multiply(c,X0))),
inference(forward_demodulation,[],[f48868,f9]) ).
fof(f50996,plain,
multiply(a,c) = multiply(c,multiply(b,c)),
inference(superposition,[],[f54,f48440]) ).
fof(f52187,plain,
! [X0] : multiply(multiply(a,c),X0) = multiply(c,multiply(multiply(b,c),X0)),
inference(superposition,[],[f9,f50996]) ).
fof(f52229,plain,
! [X0] : multiply(multiply(a,c),X0) = multiply(c,multiply(b,multiply(c,X0))),
inference(forward_demodulation,[],[f52187,f9]) ).
fof(f52249,plain,
! [X0] : multiply(a,multiply(c,X0)) = multiply(c,multiply(b,multiply(c,X0))),
inference(forward_demodulation,[],[f52229,f9]) ).
fof(f52265,plain,
multiply(a,sF1) = multiply(a,multiply(c,multiply(sF1,sF1))),
inference(backward_demodulation,[],[f24611,f52249]) ).
fof(f52287,plain,
multiply(a,sF1) = multiply(b,multiply(sF1,sF1)),
inference(forward_demodulation,[],[f52265,f44302]) ).
fof(f52482,plain,
multiply(a,multiply(a,sF1)) = multiply(c,multiply(sF1,sF1)),
inference(superposition,[],[f54,f52287]) ).
fof(f52544,plain,
sF1 = multiply(c,multiply(sF1,sF1)),
inference(forward_demodulation,[],[f52482,f39515]) ).
fof(f53056,plain,
sF1 = multiply(c,multiply(c,sF1)),
inference(superposition,[],[f63,f52544]) ).
fof(f56983,plain,
multiply(sF1,sF1) = multiply(c,sF1),
inference(superposition,[],[f48906,f53056]) ).
fof(f56985,plain,
multiply(c,c) = multiply(sF1,c),
inference(superposition,[],[f48906,f12]) ).
fof(f58270,plain,
! [X0] : multiply(add(sF1,X0),sF1) = add(multiply(c,sF1),multiply(X0,sF1)),
inference(superposition,[],[f11,f56983]) ).
fof(f58303,plain,
! [X0] : multiply(add(c,X0),sF1) = multiply(add(sF1,X0),sF1),
inference(forward_demodulation,[],[f58270,f11]) ).
fof(f75696,plain,
multiply(additive_identity,sF1) = multiply(add(c,additive_inverse(sF1)),sF1),
inference(superposition,[],[f58303,f6]) ).
fof(f75813,plain,
additive_identity = multiply(add(c,additive_inverse(sF1)),sF1),
inference(forward_demodulation,[],[f75696,f22097]) ).
fof(f77727,plain,
! [X0] : multiply(additive_identity,X0) = multiply(add(c,additive_inverse(sF1)),multiply(sF1,X0)),
inference(superposition,[],[f9,f75813]) ).
fof(f77801,plain,
! [X0] : additive_identity = multiply(add(c,additive_inverse(sF1)),multiply(sF1,X0)),
inference(forward_demodulation,[],[f77727,f22097]) ).
fof(f79774,plain,
multiply(sF1,additive_identity) = multiply(sF1,add(c,additive_inverse(sF1))),
inference(superposition,[],[f59,f77801]) ).
fof(f79855,plain,
additive_identity = multiply(sF1,add(c,additive_inverse(sF1))),
inference(forward_demodulation,[],[f79774,f19099]) ).
fof(f81233,plain,
multiply(sF1,c) = add(additive_inverse(multiply(sF1,additive_inverse(sF1))),additive_identity),
inference(superposition,[],[f1761,f79855]) ).
fof(f81315,plain,
multiply(sF1,c) = add(additive_identity,additive_inverse(multiply(sF1,additive_inverse(sF1)))),
inference(forward_demodulation,[],[f81233,f8]) ).
fof(f81352,plain,
multiply(sF1,c) = additive_inverse(multiply(sF1,additive_inverse(sF1))),
inference(forward_demodulation,[],[f81315,f1]) ).
fof(f81373,plain,
multiply(sF1,sF1) = multiply(sF1,c),
inference(forward_demodulation,[],[f81352,f29949]) ).
fof(f81384,plain,
multiply(c,c) = multiply(sF1,sF1),
inference(forward_demodulation,[],[f81373,f56985]) ).
fof(f81389,plain,
multiply(c,c) = multiply(c,sF1),
inference(backward_demodulation,[],[f56983,f81384]) ).
fof(f81412,plain,
sF1 = multiply(c,multiply(c,c)),
inference(backward_demodulation,[],[f53056,f81389]) ).
fof(f81534,plain,
c = sF1,
inference(forward_demodulation,[],[f81412,f12]) ).
fof(f81725,plain,
$false,
inference(forward_subsumption_resolution,[],[f81534,f21]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG009-7 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.21/0.47 % Computer : n017.cluster.edu
% 0.21/0.47 % Model : x86_64 x86_64
% 0.21/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.47 % Memory : 8046.5625MB
% 0.21/0.47 % OS : Linux 6.8.0-71-generic
% 0.21/0.47 % CPULimit : 300
% 0.21/0.47 % WCLimit : 300
% 0.21/0.47 % DateTime : Sun Sep 27 22:53:51 UTC 2026
% 0.21/0.47 % CPUTime :
% 0.21/0.47 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.21/0.53 Running first-order theorem proving
% 0.21/0.53 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 146.93/21.89 % (3051490)Detected a unit-equality problem, will run specialized UEQ schedule.
% 146.93/21.89 % (3051495)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=2095532438:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 146.93/21.89 % (3051497)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3246992707:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 146.93/21.89 % (3051496)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=3029359026:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 146.93/21.89 % (3051499)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2947153815:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 146.93/21.89 % (3051501)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2957119755:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 146.93/21.89 % (3051498)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=832878027:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 146.93/21.89 % (3051500)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3150271503:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 146.93/21.89 % (3051498)Instruction limit reached!
% 146.93/21.89 % (3051498)------------------------------
% 146.93/21.89 % (3051498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.93/21.89 % (3051498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.93/21.89 % (3051498)CaDiCaL version: 2.1.3
% 146.93/21.89 % (3051498)Termination reason: Instruction limit
% 146.93/21.89 % (3051498)Termination phase: Saturation
% 146.93/21.89 % (3051498)Time elapsed: 0.122 s
% 146.93/21.89 % (3051498)Peak memory usage: 88 MB
% 146.93/21.89 % (3051498)Instructions burned: 137 (million)
% 146.93/21.89 % (3051499)Instruction limit reached!
% 146.93/21.89 % (3051499)------------------------------
% 146.93/21.89 % (3051499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.93/21.89 % (3051499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.93/21.89 % (3051499)CaDiCaL version: 2.1.3
% 146.93/21.89 % (3051499)Termination reason: Instruction limit
% 146.93/21.89 % (3051499)Termination phase: Saturation
% 146.93/21.89 % (3051499)Time elapsed: 0.159 s
% 146.93/21.89 % (3051499)Peak memory usage: 89 MB
% 146.93/21.89 % (3051499)Instructions burned: 181 (million)
% 146.93/21.89 % (3051500)Instruction limit reached!
% 146.93/21.89 % (3051500)------------------------------
% 146.93/21.89 % (3051500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.93/21.89 % (3051500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.93/21.89 % (3051500)CaDiCaL version: 2.1.3
% 146.93/21.89 % (3051500)Termination reason: Instruction limit
% 146.93/21.89 % (3051500)Termination phase: Saturation
% 146.93/21.89 % (3051500)Time elapsed: 0.235 s
% 146.93/21.89 % (3051500)Peak memory usage: 90 MB
% 146.93/21.89 % (3051500)Instructions burned: 258 (million)
% 146.93/21.89 % (3051509)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3616618197:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 146.93/21.89 % (3051510)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1247543942:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 146.93/21.89 % (3051511)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1129832440:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 146.93/21.89 % (3051511)Instruction limit reached!
% 146.93/21.89 % (3051511)------------------------------
% 146.93/21.89 % (3051511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.93/21.89 % (3051511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.93/21.89 % (3051511)CaDiCaL version: 2.1.3
% 146.93/21.89 % (3051511)Termination reason: Instruction limit
% 146.93/21.89 % (3051511)Termination phase: Saturation
% 146.93/21.89 % (3051511)Time elapsed: 0.205 s
% 97.05/22.30 % (3051511)Peak memory usage: 92 MB
% 97.05/22.30 % (3051511)Instructions burned: 216 (million)
% 97.05/22.30 % (3051515)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=1575158505:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/317Mi)
% 97.05/22.30 % (3051501)Instruction limit reached!
% 97.05/22.30 % (3051501)------------------------------
% 97.05/22.30 % (3051501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.05/22.30 % (3051501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.05/22.30 % (3051501)CaDiCaL version: 2.1.3
% 97.05/22.30 % (3051501)Termination reason: Instruction limit
% 97.05/22.30 % (3051501)Termination phase: Saturation
% 97.05/22.30 % (3051501)Time elapsed: 1.068 s
% 97.05/22.30 % (3051501)Peak memory usage: 99 MB
% 97.05/22.30 % (3051501)Instructions burned: 1188 (million)
% 97.05/22.30 % (3051515)Instruction limit reached!
% 97.05/22.30 % (3051515)------------------------------
% 97.05/22.30 % (3051515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.05/22.30 % (3051515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.05/22.30 % (3051515)CaDiCaL version: 2.1.3
% 97.05/22.30 % (3051515)Termination reason: Instruction limit
% 97.05/22.30 % (3051515)Termination phase: Saturation
% 97.05/22.30 % (3051515)Time elapsed: 0.330 s
% 97.05/22.30 % (3051515)Peak memory usage: 92 MB
% 97.05/22.30 % (3051515)Instructions burned: 318 (million)
% 97.05/22.30 % (3051517)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=882209522:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/12125Mi)
% 97.05/22.30 % (3051518)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1696799484:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2985 on theBenchmark for (2985ds/2836Mi)
% 97.05/22.30 % (3051509)Instruction limit reached!
% 97.05/22.30 % (3051509)------------------------------
% 97.05/22.30 % (3051509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.05/22.30 % (3051509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.05/22.30 % (3051509)CaDiCaL version: 2.1.3
% 97.05/22.30 % (3051509)Termination reason: Instruction limit
% 97.05/22.30 % (3051509)Termination phase: Saturation
% 97.05/22.30 % (3051509)Time elapsed: 2.187 s
% 97.05/22.30 % (3051509)Peak memory usage: 141 MB
% 97.05/22.30 % (3051509)Instructions burned: 2051 (million)
% 97.05/22.30 % (3051521)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=744476627:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2972 on theBenchmark for (2972ds/14534Mi)
% 97.05/22.30 % (3051518)Instruction limit reached!
% 97.05/22.30 % (3051518)------------------------------
% 97.05/22.30 % (3051518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.05/22.30 % (3051518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.05/22.30 % (3051518)CaDiCaL version: 2.1.3
% 97.05/22.30 % (3051518)Termination reason: Instruction limit
% 97.05/22.30 % (3051518)Termination phase: Saturation
% 97.05/22.30 % (3051518)Time elapsed: 3.076 s
% 97.05/22.30 % (3051518)Peak memory usage: 128 MB
% 97.05/22.30 % (3051518)Instructions burned: 2836 (million)
% 97.05/22.30 % (3051523)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=45802052:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2951 on theBenchmark for (2951ds/11832Mi)
% 97.05/22.30 % (3051510)Instruction limit reached!
% 97.05/22.30 % (3051510)------------------------------
% 97.05/22.30 % (3051510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.05/22.30 % (3051510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.05/22.30 % (3051510)CaDiCaL version: 2.1.3
% 97.05/22.30 % (3051510)Termination reason: Instruction limit
% 97.05/22.30 % (3051510)Termination phase: Saturation
% 97.05/22.30 % (3051510)Time elapsed: 5.136 s
% 97.05/22.30 % (3051510)Peak memory usage: 167 MB
% 97.05/22.30 % (3051510)Instructions burned: 4948 (million)
% 97.05/22.30 % (3051525)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=400647497:i=2279:fgj=on:bd=all_2942 on theBenchmark for (2942ds/2279Mi)
% 97.05/22.30 % (3051525)Instruction limit reached!
% 97.05/22.30 % (3051525)------------------------------
% 97.05/22.30 % (3051525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.05/22.30 % (3051525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.05/22.30 % (3051525)CaDiCaL version: 2.1.3
% 97.05/22.30 % (3051525)Termination reason: Instruction limit
% 97.05/22.30 % (3051525)Termination phase: Saturation
% 97.05/22.30 % (3051525)Time elapsed: 2.265 s
% 97.05/22.30 % (3051525)Peak memory usage: 140 MB
% 97.05/22.30 % (3051525)Instructions burned: 2279 (million)
% 97.05/22.30 % (3051527)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:drc=off:fde=none:sp=reverse_arity:urr=ec_only:gs=on:s2agt=16:random_seed=2143327158:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2917 on theBenchmark for (2917ds/6225Mi)
% 97.05/22.30 % (3051527)Instruction limit reached!
% 97.05/22.30 % (3051527)------------------------------
% 97.05/22.30 % (3051527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.05/22.30 % (3051527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.05/22.30 % (3051527)CaDiCaL version: 2.1.3
% 97.05/22.30 % (3051527)Termination reason: Instruction limit
% 97.05/22.30 % (3051527)Termination phase: Saturation
% 97.05/22.30 % (3051527)Time elapsed: 5.462 s
% 97.05/22.30 % (3051527)Peak memory usage: 147 MB
% 97.05/22.30 % (3051527)Instructions burned: 6226 (million)
% 97.05/22.30 % (3051517)Instruction limit reached!
% 97.05/22.30 % (3051517)------------------------------
% 97.05/22.30 % (3051517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.05/22.30 % (3051517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.05/22.30 % (3051517)CaDiCaL version: 2.1.3
% 97.05/22.30 % (3051517)Termination reason: Instruction limit
% 97.05/22.30 % (3051517)Termination phase: Saturation
% 97.05/22.30 % (3051517)Time elapsed: 12.503 s
% 97.05/22.30 % (3051517)Peak memory usage: 241 MB
% 97.05/22.30 % (3051517)Instructions burned: 12125 (million)
% 97.05/22.30 % (3051529)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=2314304820:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2860 on theBenchmark for (2860ds/21755Mi)
% 97.05/22.30 % (3051530)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=816970640:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2859 on theBenchmark for (2859ds/16427Mi)
% 97.05/22.30 % (3051523)Instruction limit reached!
% 97.05/22.30 % (3051523)------------------------------
% 97.05/22.30 % (3051523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.05/22.30 % (3051523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.05/22.30 % (3051523)CaDiCaL version: 2.1.3
% 97.05/22.30 % (3051523)Termination reason: Instruction limit
% 97.05/22.30 % (3051523)Termination phase: Saturation
% 97.05/22.30 % (3051523)Time elapsed: 12.672 s
% 97.05/22.30 % (3051523)Peak memory usage: 221 MB
% 97.05/22.30 % (3051523)Instructions burned: 11833 (million)
% 97.05/22.30 % (3051535)lrs+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=1579847205:i=9356:fgj=on:bd=preordered:av=off_2822 on theBenchmark for (2822ds/9356Mi)
% 97.05/22.30 % (3051521)Instruction limit reached!
% 97.05/22.30 % (3051521)------------------------------
% 97.05/22.30 % (3051521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.05/22.30 % (3051521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.05/22.30 % (3051521)CaDiCaL version: 2.1.3
% 97.05/22.30 % (3051521)Termination reason: Instruction limit
% 97.05/22.30 % (3051521)Termination phase: Saturation
% 97.05/22.30 % (3051521)Time elapsed: 15.315 s
% 97.05/22.30 % (3051521)Peak memory usage: 252 MB
% 97.05/22.30 % (3051521)Instructions burned: 14534 (million)
% 97.05/22.30 % (3051537)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=285554233:i=2070:kws=inv_precedence:slsql=off:bd=all_2816 on theBenchmark for (2816ds/2070Mi)
% 97.05/22.30 % (3051529)First to succeed.
% 97.05/22.30 % (3051529)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3051490"
% 97.05/22.30 % (3051537)Instruction limit reached!
% 97.05/22.30 % (3051537)------------------------------
% 97.05/22.30 % (3051537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.05/22.30 % (3051537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.05/22.30 % (3051537)CaDiCaL version: 2.1.3
% 97.05/22.30 % (3051537)Termination reason: Instruction limit
% 97.05/22.30 % (3051537)Termination phase: Saturation
% 97.05/22.30 % (3051537)Time elapsed: 2.012 s
% 97.05/22.30 % (3051537)Peak memory usage: 119 MB
% 97.05/22.30 % (3051537)Instructions burned: 2070 (million)
% 97.05/22.30 % (3051539)lrs+1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=8000:tgt=ground:npcc=on:fde=unused:sp=const_min:urr=ec_only:s2agt=32:random_seed=1069094683:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2793 on theBenchmark for (2793ds/6461Mi)
% 97.05/22.30 % (3051529)Refutation found. Thanks to Tanya!
% 97.05/22.30 % SZS status Unsatisfiable for theBenchmark
% 97.05/22.30 % SZS output start Proof for theBenchmark
% See solution above
% 150.60/22.68 % (3051529)------------------------------
% 150.60/22.68 % (3051529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.60/22.68 % (3051529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.60/22.68 % (3051529)CaDiCaL version: 2.1.3
% 150.60/22.68 % (3051529)Termination reason: Refutation
% 150.60/22.68 % (3051529)Time elapsed: 6.299 s
% 150.60/22.68 % (3051529)Peak memory usage: 142 MB
% 150.60/22.68 % (3051529)Instructions burned: 5618 (million)
% 150.60/22.68 % (3051529)------------------------------
% 150.60/22.68 % (3051529)------------------------------
% 150.60/22.68 % (3051490)Success in time 21.021 s
% 150.60/22.68 % Vampire exiting
%------------------------------------------------------------------------------