%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG009-7 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:42 PM UTC 2026
% Result : Unsatisfiable 131.59s 41.45s
% Output : Refutation 131.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 75
% Number of leaves : 11
% Syntax : Number of formulae : 625 ( 625 unt; 0 def)
% Number of atoms : 625 ( 624 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 : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 621 ( 621 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : add(additive_identity,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/RNG005-0.ax',left_additive_identity) ).
fof(f2,axiom,
! [X0] : add(X0,additive_identity) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/RNG005-0.ax',right_additive_identity) ).
fof(f5,axiom,
! [X0] : add(X0,additive_inverse(X0)) = additive_identity,
file('/export/starexec/sandbox2/benchmark/Axioms/RNG005-0.ax',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/sandbox2/benchmark/Axioms/RNG005-0.ax',associativity_for_addition) ).
fof(f8,axiom,
! [X0,X1] : add(X0,X1) = add(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG005-0.ax',commutativity_for_addition) ).
fof(f9,axiom,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG005-0.ax',associativity_for_multiplication) ).
fof(f10,axiom,
! [X2,X0,X1] : multiply(X0,add(X1,X2)) = add(multiply(X0,X1),multiply(X0,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG005-0.ax',distribute1) ).
fof(f11,axiom,
! [X2,X0,X1] : multiply(add(X0,X1),X2) = add(multiply(X0,X2),multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG005-0.ax',distribute2) ).
fof(f12,axiom,
! [X0] : multiply(X0,multiply(X0,X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_cubed_is_x) ).
fof(f13,negated_conjecture,
multiply(a,b) = c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_times_b_is_c) ).
fof(f14,negated_conjecture,
multiply(b,a) != c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_commutativity) ).
fof(f15,plain,
c != multiply(b,a),
inference(reorient_equations,[],[f14]) ).
fof(f18,plain,
additive_identity = additive_inverse(additive_identity),
inference(superposition,[],[f1,f6]) ).
fof(f30,plain,
! [X0,X1] : add(additive_identity,X1) = add(X0,add(additive_inverse(X0),X1)),
inference(superposition,[],[f7,f6]) ).
fof(f32,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X1,add(X0,X2)),
inference(superposition,[],[f7,f8]) ).
fof(f39,plain,
! [X0,X1] : additive_identity = add(X0,add(X1,additive_inverse(add(X0,X1)))),
inference(superposition,[],[f6,f7]) ).
fof(f41,plain,
! [X2,X0,X1] : add(X0,add(X1,X2)) = add(X2,add(X0,X1)),
inference(superposition,[],[f8,f7]) ).
fof(f43,plain,
! [X0,X1] : add(X0,add(additive_inverse(X0),X1)) = X1,
inference(forward_demodulation,[],[f30,f1]) ).
fof(f47,plain,
! [X0,X1] : add(X1,add(X0,additive_inverse(X1))) = X0,
inference(superposition,[],[f43,f8]) ).
fof(f50,plain,
! [X0] : add(X0,additive_identity) = additive_inverse(additive_inverse(X0)),
inference(superposition,[],[f43,f6]) ).
fof(f59,plain,
! [X0] : additive_inverse(additive_inverse(X0)) = X0,
inference(forward_demodulation,[],[f50,f2]) ).
fof(f61,plain,
! [X0] : multiply(a,multiply(b,X0)) = multiply(c,X0),
inference(superposition,[],[f9,f13]) ).
fof(f62,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(multiply(X0,X0),X1)),
inference(superposition,[],[f9,f12]) ).
fof(f66,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(multiply(X0,X1),multiply(X0,X1)))),
inference(superposition,[],[f12,f9]) ).
fof(f67,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X0,X1))))),
inference(forward_demodulation,[],[f66,f9]) ).
fof(f71,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X0,multiply(X0,X1))),
inference(forward_demodulation,[],[f62,f9]) ).
fof(f73,plain,
multiply(a,b) = multiply(c,multiply(b,b)),
inference(superposition,[],[f61,f12]) ).
fof(f76,plain,
c = multiply(c,multiply(b,b)),
inference(forward_demodulation,[],[f73,f13]) ).
fof(f140,plain,
! [X0,X1] : additive_identity = add(X1,add(X0,additive_inverse(add(X0,X1)))),
inference(superposition,[],[f39,f8]) ).
fof(f160,plain,
! [X0,X1] : add(X0,additive_identity) = add(X1,additive_inverse(add(additive_inverse(X0),X1))),
inference(superposition,[],[f43,f39]) ).
fof(f163,plain,
! [X0,X1] : add(X1,additive_inverse(add(additive_inverse(X0),X1))) = X0,
inference(forward_demodulation,[],[f160,f2]) ).
fof(f192,plain,
! [X0,X1] : add(X0,additive_inverse(add(X0,additive_inverse(X1)))) = X1,
inference(superposition,[],[f163,f8]) ).
fof(f234,plain,
! [X0,X1] : multiply(X0,add(multiply(X0,X0),X1)) = add(X0,multiply(X0,X1)),
inference(superposition,[],[f10,f12]) ).
fof(f236,plain,
! [X0] : multiply(a,add(b,X0)) = add(c,multiply(a,X0)),
inference(superposition,[],[f10,f13]) ).
fof(f237,plain,
! [X0,X1] : multiply(a,add(multiply(b,X0),X1)) = add(multiply(c,X0),multiply(a,X1)),
inference(superposition,[],[f10,f61]) ).
fof(f238,plain,
! [X0] : multiply(c,add(multiply(b,b),X0)) = add(c,multiply(c,X0)),
inference(superposition,[],[f10,f76]) ).
fof(f249,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(f251,plain,
! [X2,X0,X1] : multiply(X0,add(X1,X2)) = add(multiply(X0,X2),multiply(X0,X1)),
inference(superposition,[],[f8,f10]) ).
fof(f266,plain,
multiply(a,b) = add(c,multiply(a,additive_identity)),
inference(superposition,[],[f236,f2]) ).
fof(f270,plain,
multiply(a,additive_identity) = add(c,multiply(a,additive_inverse(b))),
inference(superposition,[],[f236,f6]) ).
fof(f271,plain,
! [X0] : multiply(a,X0) = add(c,multiply(a,additive_inverse(add(additive_inverse(X0),b)))),
inference(superposition,[],[f236,f163]) ).
fof(f272,plain,
! [X0,X1] : multiply(a,add(X1,add(b,X0))) = add(multiply(a,X1),add(c,multiply(a,X0))),
inference(superposition,[],[f10,f236]) ).
fof(f274,plain,
! [X0,X1] : multiply(a,multiply(add(b,X0),X1)) = multiply(add(c,multiply(a,X0)),X1),
inference(superposition,[],[f9,f236]) ).
fof(f276,plain,
! [X0,X1] : multiply(a,add(X1,add(b,X0))) = add(c,add(multiply(a,X0),multiply(a,X1))),
inference(forward_demodulation,[],[f272,f41]) ).
fof(f277,plain,
! [X0] : multiply(a,X0) = add(c,multiply(a,additive_inverse(add(b,additive_inverse(X0))))),
inference(forward_demodulation,[],[f271,f8]) ).
fof(f279,plain,
c = add(c,multiply(a,additive_identity)),
inference(forward_demodulation,[],[f266,f13]) ).
fof(f281,plain,
! [X0,X1] : multiply(a,add(X1,add(b,X0))) = add(c,multiply(a,add(X0,X1))),
inference(forward_demodulation,[],[f276,f10]) ).
fof(f283,plain,
additive_identity = add(c,add(multiply(a,additive_identity),additive_inverse(c))),
inference(superposition,[],[f39,f279]) ).
fof(f285,plain,
additive_identity = multiply(a,additive_identity),
inference(forward_demodulation,[],[f283,f47]) ).
fof(f289,plain,
! [X0] : multiply(additive_identity,X0) = multiply(a,multiply(additive_identity,X0)),
inference(superposition,[],[f9,f285]) ).
fof(f299,plain,
! [X0] : add(multiply(a,additive_identity),X0) = add(c,add(multiply(a,additive_inverse(b)),X0)),
inference(superposition,[],[f7,f270]) ).
fof(f300,plain,
! [X0] : add(additive_identity,X0) = add(c,add(multiply(a,additive_inverse(b)),X0)),
inference(forward_demodulation,[],[f299,f285]) ).
fof(f302,plain,
! [X0] : add(c,add(multiply(a,additive_inverse(b)),X0)) = X0,
inference(forward_demodulation,[],[f300,f1]) ).
fof(f325,plain,
multiply(a,additive_inverse(b)) = additive_inverse(c),
inference(superposition,[],[f47,f302]) ).
fof(f356,plain,
! [X0,X1] : multiply(add(X0,X1),multiply(X0,X0)) = add(X0,multiply(X1,multiply(X0,X0))),
inference(superposition,[],[f11,f12]) ).
fof(f357,plain,
! [X2,X3,X0,X1] : multiply(add(multiply(X0,X1),X3),X2) = add(multiply(X0,multiply(X1,X2)),multiply(X3,X2)),
inference(superposition,[],[f11,f9]) ).
fof(f358,plain,
! [X0] : multiply(add(a,X0),additive_identity) = add(additive_identity,multiply(X0,additive_identity)),
inference(superposition,[],[f11,f285]) ).
fof(f363,plain,
! [X0] : multiply(add(a,X0),b) = add(c,multiply(X0,b)),
inference(superposition,[],[f11,f13]) ).
fof(f366,plain,
! [X0,X1] : multiply(add(X1,X0),multiply(X0,X0)) = add(multiply(X1,multiply(X0,X0)),X0),
inference(superposition,[],[f11,f12]) ).
fof(f367,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(f368,plain,
! [X0] : multiply(add(X0,a),additive_identity) = add(multiply(X0,additive_identity),additive_identity),
inference(superposition,[],[f11,f285]) ).
fof(f370,plain,
! [X0] : multiply(add(X0,a),additive_inverse(b)) = add(multiply(X0,additive_inverse(b)),additive_inverse(c)),
inference(superposition,[],[f11,f325]) ).
fof(f372,plain,
! [X0,X1] : multiply(add(X1,a),multiply(additive_identity,X0)) = add(multiply(X1,multiply(additive_identity,X0)),multiply(additive_identity,X0)),
inference(superposition,[],[f11,f289]) ).
fof(f373,plain,
! [X0] : multiply(add(X0,a),b) = add(multiply(X0,b),c),
inference(superposition,[],[f11,f13]) ).
fof(f379,plain,
! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(add(X0,X0),X1),
inference(superposition,[],[f10,f11]) ).
fof(f380,plain,
! [X0] : multiply(X0,additive_inverse(b)) = add(c,multiply(add(a,X0),additive_inverse(b))),
inference(superposition,[],[f302,f11]) ).
fof(f382,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(f384,plain,
! [X2,X0,X1] : multiply(add(X0,X1),X2) = add(multiply(X1,X2),multiply(X0,X2)),
inference(superposition,[],[f8,f11]) ).
fof(f388,plain,
! [X0] : add(c,multiply(X0,b)) = multiply(add(X0,a),b),
inference(forward_demodulation,[],[f373,f8]) ).
fof(f389,plain,
! [X0,X1] : add(multiply(additive_identity,X0),multiply(X1,multiply(additive_identity,X0))) = multiply(add(X1,a),multiply(additive_identity,X0)),
inference(forward_demodulation,[],[f372,f8]) ).
fof(f391,plain,
! [X0] : add(additive_inverse(c),multiply(X0,additive_inverse(b))) = multiply(add(X0,a),additive_inverse(b)),
inference(forward_demodulation,[],[f370,f8]) ).
fof(f393,plain,
! [X0] : add(additive_identity,multiply(X0,additive_identity)) = multiply(add(X0,a),additive_identity),
inference(forward_demodulation,[],[f368,f8]) ).
fof(f394,plain,
! [X0,X1] : add(X0,multiply(X1,multiply(X0,X0))) = multiply(add(X1,X0),multiply(X0,X0)),
inference(forward_demodulation,[],[f366,f8]) ).
fof(f398,plain,
! [X0] : multiply(add(a,X0),additive_identity) = multiply(X0,additive_identity),
inference(forward_demodulation,[],[f358,f1]) ).
fof(f399,plain,
! [X0,X1] : multiply(add(X1,a),multiply(additive_identity,X0)) = multiply(add(additive_identity,multiply(X1,additive_identity)),X0),
inference(forward_demodulation,[],[f389,f367]) ).
fof(f402,plain,
! [X0] : multiply(X0,additive_identity) = multiply(add(X0,a),additive_identity),
inference(forward_demodulation,[],[f393,f1]) ).
fof(f404,plain,
! [X0,X1] : multiply(add(X1,a),multiply(additive_identity,X0)) = multiply(multiply(X1,additive_identity),X0),
inference(forward_demodulation,[],[f399,f1]) ).
fof(f406,plain,
! [X0,X1] : multiply(X1,multiply(additive_identity,X0)) = multiply(add(X1,a),multiply(additive_identity,X0)),
inference(forward_demodulation,[],[f404,f9]) ).
fof(f409,plain,
multiply(a,additive_identity) = multiply(additive_identity,additive_identity),
inference(superposition,[],[f398,f2]) ).
fof(f413,plain,
multiply(additive_identity,additive_identity) = multiply(additive_inverse(a),additive_identity),
inference(superposition,[],[f398,f6]) ).
fof(f427,plain,
additive_identity = multiply(additive_identity,additive_identity),
inference(forward_demodulation,[],[f409,f285]) ).
fof(f436,plain,
! [X0] : multiply(additive_identity,X0) = multiply(additive_identity,multiply(additive_identity,X0)),
inference(superposition,[],[f9,f427]) ).
fof(f486,plain,
! [X0,X1] : multiply(additive_identity,add(multiply(additive_identity,X0),X1)) = add(multiply(additive_identity,X0),multiply(additive_identity,X1)),
inference(superposition,[],[f10,f436]) ).
fof(f489,plain,
! [X0,X1] : multiply(additive_identity,add(multiply(additive_identity,X0),X1)) = multiply(additive_identity,add(X0,X1)),
inference(forward_demodulation,[],[f486,f10]) ).
fof(f609,plain,
multiply(a,b) = add(c,multiply(additive_identity,b)),
inference(superposition,[],[f363,f2]) ).
fof(f613,plain,
multiply(additive_identity,b) = add(c,multiply(additive_inverse(a),b)),
inference(superposition,[],[f363,f6]) ).
fof(f615,plain,
! [X0,X1] : multiply(add(X1,add(a,X0)),b) = add(multiply(X1,b),add(c,multiply(X0,b))),
inference(superposition,[],[f11,f363]) ).
fof(f623,plain,
! [X0,X1] : multiply(add(X1,add(a,X0)),b) = add(c,add(multiply(X0,b),multiply(X1,b))),
inference(forward_demodulation,[],[f615,f41]) ).
fof(f626,plain,
c = add(c,multiply(additive_identity,b)),
inference(forward_demodulation,[],[f609,f13]) ).
fof(f629,plain,
! [X0,X1] : multiply(add(X1,add(a,X0)),b) = add(c,multiply(add(X0,X1),b)),
inference(forward_demodulation,[],[f623,f11]) ).
fof(f631,plain,
additive_identity = add(c,add(multiply(additive_identity,b),additive_inverse(c))),
inference(superposition,[],[f39,f626]) ).
fof(f632,plain,
! [X0] : add(c,X0) = add(c,add(multiply(additive_identity,b),X0)),
inference(superposition,[],[f7,f626]) ).
fof(f633,plain,
additive_identity = multiply(additive_identity,b),
inference(forward_demodulation,[],[f631,f47]) ).
fof(f640,plain,
! [X0] : add(multiply(additive_identity,X0),additive_identity) = multiply(additive_identity,add(X0,b)),
inference(superposition,[],[f10,f633]) ).
fof(f641,plain,
! [X0] : add(additive_identity,multiply(additive_identity,X0)) = multiply(additive_identity,add(b,X0)),
inference(superposition,[],[f10,f633]) ).
fof(f642,plain,
! [X0] : multiply(additive_identity,X0) = multiply(additive_identity,multiply(b,X0)),
inference(superposition,[],[f9,f633]) ).
fof(f643,plain,
! [X0] : multiply(additive_identity,X0) = multiply(additive_identity,add(b,X0)),
inference(forward_demodulation,[],[f641,f1]) ).
fof(f644,plain,
! [X0] : add(additive_identity,multiply(additive_identity,X0)) = multiply(additive_identity,add(X0,b)),
inference(forward_demodulation,[],[f640,f8]) ).
fof(f647,plain,
! [X0] : multiply(additive_identity,X0) = multiply(additive_identity,add(X0,b)),
inference(forward_demodulation,[],[f644,f1]) ).
fof(f655,plain,
! [X0,X1] : add(multiply(additive_identity,X1),multiply(additive_identity,X0)) = multiply(additive_identity,add(X1,multiply(b,X0))),
inference(superposition,[],[f10,f642]) ).
fof(f656,plain,
! [X0,X1] : add(multiply(additive_identity,X0),multiply(additive_identity,X1)) = multiply(additive_identity,add(multiply(b,X0),X1)),
inference(superposition,[],[f10,f642]) ).
fof(f659,plain,
! [X0,X1] : multiply(additive_identity,add(X0,X1)) = multiply(additive_identity,add(multiply(b,X0),X1)),
inference(forward_demodulation,[],[f656,f10]) ).
fof(f660,plain,
! [X0,X1] : multiply(additive_identity,add(X1,X0)) = multiply(additive_identity,add(X1,multiply(b,X0))),
inference(forward_demodulation,[],[f655,f10]) ).
fof(f675,plain,
multiply(additive_identity,additive_identity) = multiply(additive_identity,additive_inverse(b)),
inference(superposition,[],[f643,f6]) ).
fof(f684,plain,
! [X0,X1] : multiply(multiply(additive_identity,X0),X1) = multiply(additive_identity,multiply(add(b,X0),X1)),
inference(superposition,[],[f9,f643]) ).
fof(f685,plain,
! [X0,X1] : multiply(additive_identity,multiply(X0,X1)) = multiply(additive_identity,multiply(add(b,X0),X1)),
inference(forward_demodulation,[],[f684,f9]) ).
fof(f691,plain,
additive_identity = multiply(additive_identity,additive_inverse(b)),
inference(forward_demodulation,[],[f675,f427]) ).
fof(f722,plain,
! [X0,X1] : multiply(multiply(additive_identity,X0),X1) = multiply(additive_identity,multiply(add(X0,b),X1)),
inference(superposition,[],[f9,f647]) ).
fof(f723,plain,
! [X0,X1] : multiply(additive_identity,multiply(X0,X1)) = multiply(additive_identity,multiply(add(X0,b),X1)),
inference(forward_demodulation,[],[f722,f9]) ).
fof(f755,plain,
! [X0] : add(multiply(additive_identity,b),X0) = add(c,add(multiply(additive_inverse(a),b),X0)),
inference(superposition,[],[f7,f613]) ).
fof(f756,plain,
! [X0] : add(additive_identity,X0) = add(c,add(multiply(additive_inverse(a),b),X0)),
inference(forward_demodulation,[],[f755,f633]) ).
fof(f758,plain,
! [X0] : add(c,add(multiply(additive_inverse(a),b),X0)) = X0,
inference(forward_demodulation,[],[f756,f1]) ).
fof(f770,plain,
! [X0] : multiply(additive_inverse(a),X0) = add(c,multiply(additive_inverse(a),add(b,X0))),
inference(superposition,[],[f758,f10]) ).
fof(f782,plain,
additive_inverse(c) = multiply(additive_inverse(a),b),
inference(superposition,[],[f47,f758]) ).
fof(f810,plain,
! [X0] : multiply(additive_inverse(a),add(X0,b)) = add(multiply(additive_inverse(a),X0),additive_inverse(c)),
inference(superposition,[],[f10,f782]) ).
fof(f813,plain,
! [X0] : multiply(additive_inverse(a),add(X0,b)) = add(additive_inverse(c),multiply(additive_inverse(a),X0)),
inference(forward_demodulation,[],[f810,f8]) ).
fof(f972,plain,
additive_inverse(c) = multiply(a,multiply(a,additive_inverse(c))),
inference(superposition,[],[f71,f325]) ).
fof(f973,plain,
! [X0] : multiply(c,X0) = multiply(a,multiply(a,multiply(c,X0))),
inference(superposition,[],[f71,f61]) ).
fof(f975,plain,
c = multiply(a,multiply(a,c)),
inference(superposition,[],[f71,f13]) ).
fof(f1019,plain,
! [X0] : add(c,multiply(a,X0)) = multiply(a,add(multiply(a,c),X0)),
inference(superposition,[],[f10,f975]) ).
fof(f1189,plain,
! [X0,X1] : add(add(c,X0),X1) = add(add(multiply(additive_identity,b),X0),add(c,X1)),
inference(superposition,[],[f32,f632]) ).
fof(f1224,plain,
! [X0,X1] : add(add(c,X0),X1) = add(c,add(X1,add(multiply(additive_identity,b),X0))),
inference(forward_demodulation,[],[f1189,f41]) ).
fof(f1243,plain,
! [X0,X1] : add(add(c,X0),X1) = add(c,add(X1,add(additive_identity,X0))),
inference(forward_demodulation,[],[f1224,f633]) ).
fof(f1258,plain,
! [X0,X1] : add(add(c,X0),X1) = add(c,add(X1,X0)),
inference(forward_demodulation,[],[f1243,f1]) ).
fof(f1269,plain,
! [X0,X1] : add(c,add(X0,X1)) = add(c,add(X1,X0)),
inference(forward_demodulation,[],[f1258,f7]) ).
fof(f1300,plain,
! [X2,X0,X1] : add(c,add(multiply(X0,X2),multiply(X0,X1))) = add(c,multiply(X0,add(X1,X2))),
inference(superposition,[],[f1269,f10]) ).
fof(f1301,plain,
! [X2,X0,X1] : add(c,add(multiply(X1,X2),multiply(X0,X2))) = add(c,multiply(add(X0,X1),X2)),
inference(superposition,[],[f1269,f11]) ).
fof(f1344,plain,
! [X2,X0,X1] : add(c,multiply(add(X0,X1),X2)) = add(c,multiply(add(X1,X0),X2)),
inference(forward_demodulation,[],[f1301,f11]) ).
fof(f1345,plain,
! [X2,X0,X1] : add(c,multiply(X0,add(X1,X2))) = add(c,multiply(X0,add(X2,X1))),
inference(forward_demodulation,[],[f1300,f10]) ).
fof(f2108,plain,
! [X0] : multiply(additive_identity,X0) = multiply(additive_identity,add(X0,X0)),
inference(superposition,[],[f379,f1]) ).
fof(f2230,plain,
multiply(c,multiply(b,b)) = add(c,multiply(c,additive_identity)),
inference(superposition,[],[f238,f2]) ).
fof(f2236,plain,
multiply(c,additive_identity) = add(c,multiply(c,additive_inverse(multiply(b,b)))),
inference(superposition,[],[f238,f6]) ).
fof(f2256,plain,
c = add(c,multiply(c,additive_identity)),
inference(forward_demodulation,[],[f2230,f76]) ).
fof(f2266,plain,
additive_identity = add(c,add(multiply(c,additive_identity),additive_inverse(c))),
inference(superposition,[],[f39,f2256]) ).
fof(f2270,plain,
additive_identity = multiply(c,additive_identity),
inference(forward_demodulation,[],[f2266,f47]) ).
fof(f2278,plain,
! [X0] : add(additive_identity,multiply(X0,additive_identity)) = multiply(add(c,X0),additive_identity),
inference(superposition,[],[f11,f2270]) ).
fof(f2284,plain,
! [X0] : multiply(X0,additive_identity) = multiply(add(c,X0),additive_identity),
inference(forward_demodulation,[],[f2278,f1]) ).
fof(f2351,plain,
multiply(additive_identity,additive_identity) = multiply(additive_inverse(c),additive_identity),
inference(superposition,[],[f2284,f6]) ).
fof(f2377,plain,
additive_identity = multiply(additive_inverse(c),additive_identity),
inference(forward_demodulation,[],[f2351,f427]) ).
fof(f2431,plain,
! [X0] : multiply(additive_identity,X0) = multiply(additive_inverse(c),multiply(additive_identity,X0)),
inference(superposition,[],[f9,f2377]) ).
fof(f3257,plain,
! [X0] : add(X0,multiply(c,additive_identity)) = add(c,add(multiply(c,additive_inverse(multiply(b,b))),X0)),
inference(superposition,[],[f41,f2236]) ).
fof(f3258,plain,
! [X0] : add(X0,additive_identity) = add(c,add(multiply(c,additive_inverse(multiply(b,b))),X0)),
inference(forward_demodulation,[],[f3257,f2270]) ).
fof(f3265,plain,
! [X0] : add(c,add(multiply(c,additive_inverse(multiply(b,b))),X0)) = X0,
inference(forward_demodulation,[],[f3258,f2]) ).
fof(f3351,plain,
additive_inverse(c) = multiply(c,additive_inverse(multiply(b,b))),
inference(superposition,[],[f47,f3265]) ).
fof(f3396,plain,
additive_inverse(c) = multiply(c,multiply(c,additive_inverse(c))),
inference(superposition,[],[f71,f3351]) ).
fof(f3412,plain,
! [X0] : multiply(additive_inverse(c),X0) = multiply(c,multiply(multiply(c,additive_inverse(c)),X0)),
inference(superposition,[],[f9,f3396]) ).
fof(f3413,plain,
! [X0] : multiply(additive_inverse(c),X0) = multiply(c,multiply(c,multiply(additive_inverse(c),X0))),
inference(forward_demodulation,[],[f3412,f9]) ).
fof(f3568,plain,
! [X2,X0,X1] : multiply(X0,add(X1,X2)) = multiply(X0,add(X2,X1)),
inference(superposition,[],[f10,f251]) ).
fof(f3571,plain,
! [X0] : multiply(additive_inverse(a),X0) = add(c,multiply(additive_inverse(a),add(X0,b))),
inference(superposition,[],[f758,f251]) ).
fof(f4003,plain,
! [X0] : multiply(a,additive_inverse(X0)) = add(c,multiply(a,additive_inverse(add(b,X0)))),
inference(superposition,[],[f277,f59]) ).
fof(f4053,plain,
multiply(a,additive_identity) = add(c,multiply(a,additive_inverse(multiply(a,c)))),
inference(superposition,[],[f1019,f6]) ).
fof(f4082,plain,
additive_identity = add(c,multiply(a,additive_inverse(multiply(a,c)))),
inference(forward_demodulation,[],[f4053,f285]) ).
fof(f4100,plain,
! [X0] : add(X0,additive_identity) = add(c,add(multiply(a,additive_inverse(multiply(a,c))),X0)),
inference(superposition,[],[f41,f4082]) ).
fof(f4101,plain,
! [X0] : add(c,add(multiply(a,additive_inverse(multiply(a,c))),X0)) = X0,
inference(forward_demodulation,[],[f4100,f2]) ).
fof(f4279,plain,
! [X2,X0,X1] : multiply(add(X0,X1),X2) = multiply(add(X1,X0),X2),
inference(superposition,[],[f11,f384]) ).
fof(f4282,plain,
! [X0] : multiply(X0,additive_inverse(b)) = add(c,multiply(add(X0,a),additive_inverse(b))),
inference(superposition,[],[f302,f384]) ).
fof(f4599,plain,
additive_inverse(c) = multiply(a,additive_inverse(multiply(a,c))),
inference(superposition,[],[f47,f4101]) ).
fof(f4640,plain,
! [X0] : multiply(additive_inverse(c),X0) = multiply(a,multiply(additive_inverse(multiply(a,c)),X0)),
inference(superposition,[],[f9,f4599]) ).
fof(f4840,plain,
add(c,multiply(additive_identity,additive_inverse(b))) = multiply(additive_inverse(a),additive_inverse(b)),
inference(superposition,[],[f380,f6]) ).
fof(f4854,plain,
add(c,additive_identity) = multiply(additive_inverse(a),additive_inverse(b)),
inference(forward_demodulation,[],[f4840,f691]) ).
fof(f4859,plain,
add(additive_identity,c) = multiply(additive_inverse(a),additive_inverse(b)),
inference(forward_demodulation,[],[f4854,f8]) ).
fof(f4861,plain,
c = multiply(additive_inverse(a),additive_inverse(b)),
inference(forward_demodulation,[],[f4859,f1]) ).
fof(f5035,plain,
! [X0] : multiply(a,multiply(b,X0)) = multiply(c,multiply(X0,multiply(b,multiply(X0,multiply(b,X0))))),
inference(superposition,[],[f61,f67]) ).
fof(f5039,plain,
! [X0] : multiply(c,X0) = multiply(c,multiply(X0,multiply(b,multiply(X0,multiply(b,X0))))),
inference(forward_demodulation,[],[f5035,f61]) ).
fof(f5410,plain,
! [X0] : multiply(c,X0) = multiply(additive_inverse(a),multiply(additive_inverse(b),X0)),
inference(superposition,[],[f9,f4861]) ).
fof(f5416,plain,
c = multiply(additive_inverse(a),multiply(additive_inverse(a),c)),
inference(superposition,[],[f71,f4861]) ).
fof(f5548,plain,
! [X0] : multiply(additive_inverse(a),multiply(additive_inverse(b),X0)) = multiply(c,multiply(additive_inverse(b),multiply(additive_inverse(b),X0))),
inference(superposition,[],[f5410,f71]) ).
fof(f5583,plain,
! [X0] : multiply(c,X0) = multiply(c,multiply(additive_inverse(b),multiply(additive_inverse(b),X0))),
inference(forward_demodulation,[],[f5548,f5410]) ).
fof(f5824,plain,
! [X0,X1] : add(multiply(additive_inverse(a),X0),X1) = add(multiply(additive_inverse(a),add(X0,b)),add(c,X1)),
inference(superposition,[],[f32,f3571]) ).
fof(f5832,plain,
! [X0,X1] : add(multiply(additive_inverse(a),X0),X1) = add(c,add(X1,multiply(additive_inverse(a),add(X0,b)))),
inference(forward_demodulation,[],[f5824,f41]) ).
fof(f5843,plain,
! [X0] : multiply(a,additive_inverse(X0)) = add(c,multiply(a,additive_inverse(add(X0,b)))),
inference(superposition,[],[f4003,f8]) ).
fof(f5925,plain,
! [X0,X1] : add(multiply(X0,additive_inverse(b)),X1) = add(multiply(add(X0,a),additive_inverse(b)),add(c,X1)),
inference(superposition,[],[f32,f4282]) ).
fof(f5933,plain,
! [X0,X1] : add(multiply(X0,additive_inverse(b)),X1) = add(c,add(X1,multiply(add(X0,a),additive_inverse(b)))),
inference(forward_demodulation,[],[f5925,f41]) ).
fof(f6713,plain,
! [X0,X1] : multiply(additive_identity,multiply(add(b,X0),X1)) = multiply(additive_identity,add(X1,multiply(X0,X1))),
inference(superposition,[],[f659,f11]) ).
fof(f6722,plain,
! [X0] : multiply(additive_identity,additive_identity) = multiply(additive_identity,add(X0,additive_inverse(multiply(b,X0)))),
inference(superposition,[],[f659,f6]) ).
fof(f6767,plain,
! [X0] : additive_identity = multiply(additive_identity,add(X0,additive_inverse(multiply(b,X0)))),
inference(forward_demodulation,[],[f6722,f427]) ).
fof(f6770,plain,
! [X0,X1] : multiply(additive_identity,multiply(X0,X1)) = multiply(additive_identity,add(X1,multiply(X0,X1))),
inference(forward_demodulation,[],[f6713,f685]) ).
fof(f7110,plain,
! [X2,X0,X1] : add(multiply(add(X0,a),add(X1,b)),X2) = add(multiply(add(X0,a),X1),add(add(c,multiply(X0,b)),X2)),
inference(superposition,[],[f249,f388]) ).
fof(f7183,plain,
! [X2,X0,X1] : add(multiply(X0,X1),additive_identity) = add(multiply(X0,add(X1,X2)),additive_inverse(multiply(X0,X2))),
inference(superposition,[],[f249,f6]) ).
fof(f7244,plain,
! [X2,X0,X1] : add(multiply(X0,X1),additive_identity) = add(additive_inverse(multiply(X0,X2)),multiply(X0,add(X1,X2))),
inference(forward_demodulation,[],[f7183,f8]) ).
fof(f7310,plain,
! [X2,X0,X1] : add(multiply(add(X0,a),add(X1,b)),X2) = add(add(c,multiply(X0,b)),add(X2,multiply(add(X0,a),X1))),
inference(forward_demodulation,[],[f7110,f41]) ).
fof(f7460,plain,
! [X2,X0,X1] : add(additive_inverse(multiply(X0,X2)),multiply(X0,add(X1,X2))) = add(additive_identity,multiply(X0,X1)),
inference(forward_demodulation,[],[f7244,f8]) ).
fof(f7504,plain,
! [X2,X0,X1] : add(multiply(add(X0,a),add(X1,b)),X2) = add(c,add(multiply(X0,b),add(X2,multiply(add(X0,a),X1)))),
inference(forward_demodulation,[],[f7310,f7]) ).
fof(f7555,plain,
! [X2,X0,X1] : multiply(X0,X1) = add(additive_inverse(multiply(X0,X2)),multiply(X0,add(X1,X2))),
inference(forward_demodulation,[],[f7460,f1]) ).
fof(f8177,plain,
! [X2,X0,X1] : add(multiply(X1,multiply(X0,additive_identity)),multiply(X2,additive_identity)) = multiply(add(multiply(X1,add(X0,a)),X2),additive_identity),
inference(superposition,[],[f357,f402]) ).
fof(f8215,plain,
! [X0,X1] : add(multiply(X0,additive_identity),multiply(X1,additive_identity)) = multiply(add(multiply(X0,a),X1),additive_identity),
inference(superposition,[],[f357,f285]) ).
fof(f8234,plain,
! [X0,X1] : multiply(add(multiply(X0,a),X1),b) = add(multiply(X0,c),multiply(X1,b)),
inference(superposition,[],[f357,f13]) ).
fof(f8248,plain,
! [X0,X1] : add(X0,multiply(X1,X0)) = multiply(add(multiply(X0,X0),X1),X0),
inference(superposition,[],[f357,f12]) ).
fof(f8280,plain,
! [X0] : add(c,multiply(X0,c)) = multiply(add(multiply(a,a),X0),c),
inference(superposition,[],[f357,f975]) ).
fof(f8286,plain,
! [X0] : add(c,multiply(X0,b)) = multiply(add(multiply(c,b),X0),b),
inference(superposition,[],[f357,f76]) ).
fof(f8593,plain,
! [X0,X1] : multiply(add(X0,X1),additive_identity) = multiply(add(multiply(X0,a),X1),additive_identity),
inference(forward_demodulation,[],[f8215,f11]) ).
fof(f8622,plain,
! [X2,X0,X1] : multiply(add(multiply(X1,add(X0,a)),X2),additive_identity) = multiply(add(multiply(X1,X0),X2),additive_identity),
inference(forward_demodulation,[],[f8177,f357]) ).
fof(f9097,plain,
add(c,multiply(additive_identity,c)) = multiply(multiply(a,a),c),
inference(superposition,[],[f8280,f2]) ).
fof(f9103,plain,
multiply(additive_identity,c) = add(c,multiply(additive_inverse(multiply(a,a)),c)),
inference(superposition,[],[f8280,f6]) ).
fof(f9137,plain,
multiply(a,multiply(a,c)) = add(c,multiply(additive_identity,c)),
inference(forward_demodulation,[],[f9097,f9]) ).
fof(f9152,plain,
c = add(c,multiply(additive_identity,c)),
inference(forward_demodulation,[],[f9137,f975]) ).
fof(f9162,plain,
additive_identity = add(c,add(multiply(additive_identity,c),additive_inverse(c))),
inference(superposition,[],[f39,f9152]) ).
fof(f9169,plain,
additive_identity = multiply(additive_identity,c),
inference(forward_demodulation,[],[f9162,f47]) ).
fof(f9587,plain,
! [X2,X0,X1] : add(multiply(X1,multiply(additive_identity,X0)),multiply(X2,multiply(additive_identity,X0))) = multiply(add(X1,multiply(X2,additive_inverse(c))),multiply(additive_identity,X0)),
inference(superposition,[],[f367,f2431]) ).
fof(f9776,plain,
! [X2,X0,X1] : multiply(add(X1,X2),multiply(additive_identity,X0)) = multiply(add(X1,multiply(X2,additive_inverse(c))),multiply(additive_identity,X0)),
inference(forward_demodulation,[],[f9587,f11]) ).
fof(f10965,plain,
! [X2,X0,X1] : add(multiply(add(X1,a),add(b,X0)),X2) = add(multiply(X1,add(b,X0)),add(add(c,multiply(a,X0)),X2)),
inference(superposition,[],[f382,f236]) ).
fof(f11008,plain,
! [X2,X0,X1] : add(multiply(X0,X1),additive_identity) = add(multiply(add(X0,X2),X1),additive_inverse(multiply(X2,X1))),
inference(superposition,[],[f382,f6]) ).
fof(f11070,plain,
! [X2,X0,X1] : add(multiply(X0,X1),additive_identity) = add(additive_inverse(multiply(X2,X1)),multiply(add(X0,X2),X1)),
inference(forward_demodulation,[],[f11008,f8]) ).
fof(f11105,plain,
! [X2,X0,X1] : add(multiply(add(X1,a),add(b,X0)),X2) = add(add(c,multiply(a,X0)),add(X2,multiply(X1,add(b,X0)))),
inference(forward_demodulation,[],[f10965,f41]) ).
fof(f11324,plain,
! [X2,X0,X1] : add(additive_identity,multiply(X0,X1)) = add(additive_inverse(multiply(X2,X1)),multiply(add(X0,X2),X1)),
inference(forward_demodulation,[],[f11070,f8]) ).
fof(f11348,plain,
! [X2,X0,X1] : add(multiply(add(X1,a),add(b,X0)),X2) = add(c,add(multiply(a,X0),add(X2,multiply(X1,add(b,X0))))),
inference(forward_demodulation,[],[f11105,f7]) ).
fof(f11458,plain,
! [X2,X0,X1] : multiply(X0,X1) = add(additive_inverse(multiply(X2,X1)),multiply(add(X0,X2),X1)),
inference(forward_demodulation,[],[f11324,f1]) ).
fof(f12467,plain,
! [X0] : multiply(a,additive_identity) = add(multiply(c,X0),multiply(a,additive_inverse(multiply(b,X0)))),
inference(superposition,[],[f237,f6]) ).
fof(f12524,plain,
! [X0] : additive_identity = add(multiply(c,X0),multiply(a,additive_inverse(multiply(b,X0)))),
inference(forward_demodulation,[],[f12467,f285]) ).
fof(f12614,plain,
! [X0,X1] : add(X1,additive_identity) = add(multiply(c,X0),add(multiply(a,additive_inverse(multiply(b,X0))),X1)),
inference(superposition,[],[f41,f12524]) ).
fof(f12619,plain,
! [X0,X1] : add(multiply(c,X0),add(multiply(a,additive_inverse(multiply(b,X0))),X1)) = X1,
inference(forward_demodulation,[],[f12614,f2]) ).
fof(f12766,plain,
! [X0] : add(X0,multiply(additive_identity,c)) = add(c,add(multiply(additive_inverse(multiply(a,a)),c),X0)),
inference(superposition,[],[f41,f9103]) ).
fof(f12771,plain,
! [X0] : add(X0,additive_identity) = add(c,add(multiply(additive_inverse(multiply(a,a)),c),X0)),
inference(forward_demodulation,[],[f12766,f9169]) ).
fof(f12782,plain,
! [X0] : add(c,add(multiply(additive_inverse(multiply(a,a)),c),X0)) = X0,
inference(forward_demodulation,[],[f12771,f2]) ).
fof(f13340,plain,
additive_inverse(c) = multiply(additive_inverse(multiply(a,a)),c),
inference(superposition,[],[f47,f12782]) ).
fof(f13403,plain,
! [X0] : multiply(additive_inverse(c),X0) = multiply(additive_inverse(multiply(a,a)),multiply(c,X0)),
inference(superposition,[],[f9,f13340]) ).
fof(f13679,plain,
! [X0] : multiply(add(c,additive_inverse(c)),X0) = multiply(a,multiply(add(b,multiply(a,additive_inverse(c))),X0)),
inference(superposition,[],[f274,f972]) ).
fof(f13694,plain,
! [X0] : multiply(additive_identity,X0) = multiply(a,multiply(add(b,additive_inverse(multiply(a,c))),X0)),
inference(superposition,[],[f274,f4082]) ).
fof(f13807,plain,
! [X0] : multiply(additive_identity,X0) = multiply(a,multiply(add(b,multiply(a,additive_inverse(c))),X0)),
inference(forward_demodulation,[],[f13679,f6]) ).
fof(f14599,plain,
! [X0] : multiply(a,additive_identity) = add(c,multiply(a,add(additive_inverse(add(X0,b)),X0))),
inference(superposition,[],[f281,f39]) ).
fof(f14684,plain,
! [X0] : multiply(a,additive_identity) = add(c,multiply(a,add(X0,additive_inverse(add(X0,b))))),
inference(forward_demodulation,[],[f14599,f1345]) ).
fof(f14713,plain,
! [X0] : additive_identity = add(c,multiply(a,add(X0,additive_inverse(add(X0,b))))),
inference(forward_demodulation,[],[f14684,f285]) ).
fof(f14826,plain,
! [X0,X1] : add(X1,additive_identity) = add(c,add(multiply(a,add(X0,additive_inverse(add(X0,b)))),X1)),
inference(superposition,[],[f41,f14713]) ).
fof(f14831,plain,
! [X0,X1] : add(c,add(multiply(a,add(X0,additive_inverse(add(X0,b)))),X1)) = X1,
inference(forward_demodulation,[],[f14826,f2]) ).
fof(f15817,plain,
! [X0] : multiply(X0,b) = add(c,multiply(add(additive_inverse(multiply(c,b)),X0),b)),
inference(superposition,[],[f8286,f43]) ).
fof(f15822,plain,
multiply(additive_identity,b) = add(c,multiply(additive_inverse(multiply(c,b)),b)),
inference(superposition,[],[f8286,f6]) ).
fof(f15873,plain,
additive_identity = add(c,multiply(additive_inverse(multiply(c,b)),b)),
inference(forward_demodulation,[],[f15822,f633]) ).
fof(f15924,plain,
! [X0] : add(X0,additive_identity) = add(c,add(multiply(additive_inverse(multiply(c,b)),b),X0)),
inference(superposition,[],[f41,f15873]) ).
fof(f15929,plain,
! [X0] : add(c,add(multiply(additive_inverse(multiply(c,b)),b),X0)) = X0,
inference(forward_demodulation,[],[f15924,f2]) ).
fof(f16893,plain,
! [X0,X1] : multiply(add(add(X0,X0),X1),additive_identity) = multiply(add(multiply(X0,add(a,a)),X1),additive_identity),
inference(superposition,[],[f8593,f379]) ).
fof(f17001,plain,
! [X0,X1] : multiply(add(multiply(X0,a),X1),additive_identity) = multiply(add(add(X0,X0),X1),additive_identity),
inference(forward_demodulation,[],[f16893,f8622]) ).
fof(f17034,plain,
! [X0,X1] : multiply(add(multiply(X0,a),X1),additive_identity) = multiply(add(X0,add(X0,X1)),additive_identity),
inference(forward_demodulation,[],[f17001,f7]) ).
fof(f17045,plain,
! [X0,X1] : multiply(add(X0,X1),additive_identity) = multiply(add(X0,add(X0,X1)),additive_identity),
inference(forward_demodulation,[],[f17034,f8593]) ).
fof(f18528,plain,
! [X0] : multiply(additive_identity,b) = add(c,multiply(add(additive_inverse(add(X0,a)),X0),b)),
inference(superposition,[],[f629,f39]) ).
fof(f18603,plain,
! [X0] : multiply(additive_identity,b) = add(c,multiply(add(X0,additive_inverse(add(X0,a))),b)),
inference(forward_demodulation,[],[f18528,f1344]) ).
fof(f18634,plain,
! [X0] : additive_identity = add(c,multiply(add(X0,additive_inverse(add(X0,a))),b)),
inference(forward_demodulation,[],[f18603,f633]) ).
fof(f20387,plain,
! [X0] : multiply(additive_identity,multiply(X0,multiply(X0,X0))) = multiply(additive_identity,add(X0,multiply(b,multiply(X0,X0)))),
inference(superposition,[],[f685,f394]) ).
fof(f20477,plain,
! [X0] : multiply(additive_identity,multiply(X0,multiply(X0,X0))) = multiply(additive_identity,add(X0,multiply(X0,X0))),
inference(forward_demodulation,[],[f20387,f660]) ).
fof(f20521,plain,
! [X0] : multiply(additive_identity,multiply(X0,X0)) = multiply(additive_identity,multiply(X0,multiply(X0,X0))),
inference(forward_demodulation,[],[f20477,f6770]) ).
fof(f20540,plain,
! [X0] : multiply(additive_identity,X0) = multiply(additive_identity,multiply(X0,X0)),
inference(forward_demodulation,[],[f20521,f12]) ).
fof(f20574,plain,
! [X0,X1] : add(multiply(additive_identity,X0),multiply(X1,X0)) = multiply(add(multiply(additive_identity,X0),X1),X0),
inference(superposition,[],[f357,f20540]) ).
fof(f20576,plain,
! [X0,X1] : multiply(multiply(additive_identity,X0),X1) = multiply(additive_identity,multiply(multiply(X0,X0),X1)),
inference(superposition,[],[f9,f20540]) ).
fof(f20612,plain,
! [X0,X1] : multiply(multiply(additive_identity,X0),X1) = multiply(additive_identity,multiply(X0,multiply(X0,X1))),
inference(forward_demodulation,[],[f20576,f9]) ).
fof(f20613,plain,
! [X0,X1] : multiply(add(additive_identity,X1),X0) = multiply(add(multiply(additive_identity,X0),X1),X0),
inference(forward_demodulation,[],[f20574,f11]) ).
fof(f20633,plain,
! [X0,X1] : multiply(additive_identity,multiply(X0,X1)) = multiply(additive_identity,multiply(X0,multiply(X0,X1))),
inference(forward_demodulation,[],[f20612,f9]) ).
fof(f20634,plain,
! [X0,X1] : multiply(X1,X0) = multiply(add(multiply(additive_identity,X0),X1),X0),
inference(forward_demodulation,[],[f20613,f1]) ).
fof(f21117,plain,
! [X2,X0,X1] : multiply(add(X2,X0),X1) = multiply(add(X0,add(multiply(additive_identity,X1),X2)),X1),
inference(superposition,[],[f20634,f41]) ).
fof(f21118,plain,
! [X0] : multiply(additive_identity,X0) = multiply(additive_inverse(multiply(additive_identity,X0)),X0),
inference(superposition,[],[f20634,f6]) ).
fof(f21119,plain,
! [X0,X1] : multiply(X0,X1) = multiply(additive_inverse(add(additive_inverse(X0),multiply(additive_identity,X1))),X1),
inference(superposition,[],[f20634,f163]) ).
fof(f21184,plain,
! [X2,X3,X0,X1] : add(multiply(add(X2,add(multiply(additive_identity,X1),X0)),X1),X3) = add(multiply(X2,X1),add(multiply(X0,X1),X3)),
inference(superposition,[],[f382,f20634]) ).
fof(f21209,plain,
! [X2,X3,X0,X1] : add(multiply(add(X2,X0),X1),X3) = add(multiply(add(X2,add(multiply(additive_identity,X1),X0)),X1),X3),
inference(forward_demodulation,[],[f21184,f382]) ).
fof(f21296,plain,
! [X2,X3,X0,X1] : add(multiply(add(X0,X2),X1),X3) = add(multiply(add(X2,X0),X1),X3),
inference(forward_demodulation,[],[f21209,f21117]) ).
fof(f27415,plain,
multiply(additive_identity,multiply(multiply(a,a),c)) = multiply(additive_identity,add(c,multiply(b,c))),
inference(superposition,[],[f723,f8280]) ).
fof(f27531,plain,
multiply(additive_identity,add(c,c)) = multiply(additive_identity,multiply(multiply(a,a),c)),
inference(forward_demodulation,[],[f27415,f660]) ).
fof(f27577,plain,
multiply(additive_identity,add(c,c)) = multiply(additive_identity,multiply(a,multiply(a,c))),
inference(forward_demodulation,[],[f27531,f9]) ).
fof(f27601,plain,
multiply(additive_identity,add(c,c)) = multiply(additive_identity,multiply(a,c)),
inference(forward_demodulation,[],[f27577,f20633]) ).
fof(f27609,plain,
multiply(additive_identity,c) = multiply(additive_identity,multiply(a,c)),
inference(forward_demodulation,[],[f27601,f2108]) ).
fof(f27611,plain,
additive_identity = multiply(additive_identity,multiply(a,c)),
inference(forward_demodulation,[],[f27609,f9169]) ).
fof(f27640,plain,
! [X0] : add(additive_identity,multiply(X0,c)) = multiply(add(multiply(additive_identity,a),X0),c),
inference(superposition,[],[f357,f27611]) ).
fof(f27676,plain,
! [X0] : multiply(X0,c) = multiply(add(multiply(additive_identity,a),X0),c),
inference(forward_demodulation,[],[f27640,f1]) ).
fof(f28780,plain,
multiply(additive_identity,c) = multiply(additive_inverse(multiply(additive_identity,a)),c),
inference(superposition,[],[f27676,f6]) ).
fof(f28781,plain,
! [X0] : multiply(X0,c) = multiply(additive_inverse(add(additive_inverse(X0),multiply(additive_identity,a))),c),
inference(superposition,[],[f27676,f163]) ).
fof(f28834,plain,
additive_identity = multiply(additive_inverse(multiply(additive_identity,a)),c),
inference(forward_demodulation,[],[f28780,f9169]) ).
fof(f30461,plain,
! [X0] : multiply(additive_identity,b) = add(multiply(X0,c),multiply(additive_inverse(multiply(X0,a)),b)),
inference(superposition,[],[f8234,f6]) ).
fof(f30539,plain,
! [X0] : additive_identity = add(multiply(X0,c),multiply(additive_inverse(multiply(X0,a)),b)),
inference(forward_demodulation,[],[f30461,f633]) ).
fof(f30788,plain,
! [X0,X1] : add(additive_identity,X1) = add(multiply(additive_inverse(multiply(X0,a)),b),add(multiply(X0,c),X1)),
inference(superposition,[],[f32,f30539]) ).
fof(f30791,plain,
! [X0,X1] : add(X1,additive_identity) = add(multiply(X0,c),add(multiply(additive_inverse(multiply(X0,a)),b),X1)),
inference(superposition,[],[f41,f30539]) ).
fof(f30796,plain,
! [X0,X1] : add(multiply(X0,c),add(multiply(additive_inverse(multiply(X0,a)),b),X1)) = X1,
inference(forward_demodulation,[],[f30791,f2]) ).
fof(f30799,plain,
! [X0,X1] : add(additive_identity,X1) = add(multiply(X0,c),add(X1,multiply(additive_inverse(multiply(X0,a)),b))),
inference(forward_demodulation,[],[f30788,f41]) ).
fof(f30847,plain,
! [X0,X1] : add(multiply(X0,c),add(X1,multiply(additive_inverse(multiply(X0,a)),b))) = X1,
inference(forward_demodulation,[],[f30799,f1]) ).
fof(f34682,plain,
! [X0,X1] : add(X1,multiply(a,additive_inverse(X0))) = add(c,add(multiply(a,additive_inverse(add(X0,b))),X1)),
inference(superposition,[],[f41,f5843]) ).
fof(f34965,plain,
! [X0,X1] : multiply(X0,additive_identity) = multiply(add(X1,X0),additive_identity),
inference(superposition,[],[f17045,f163]) ).
fof(f35034,plain,
! [X0] : multiply(X0,additive_identity) = multiply(add(X0,additive_inverse(X0)),additive_identity),
inference(superposition,[],[f17045,f47]) ).
fof(f35104,plain,
! [X0] : multiply(additive_identity,additive_identity) = multiply(X0,additive_identity),
inference(forward_demodulation,[],[f35034,f6]) ).
fof(f35144,plain,
! [X0] : additive_identity = multiply(X0,additive_identity),
inference(forward_demodulation,[],[f35104,f427]) ).
fof(f35247,plain,
! [X0,X1] : multiply(additive_identity,X1) = multiply(X0,multiply(additive_identity,X1)),
inference(superposition,[],[f9,f35144]) ).
fof(f36603,plain,
! [X0] : additive_identity = multiply(additive_identity,add(multiply(additive_identity,X0),additive_inverse(multiply(additive_identity,X0)))),
inference(superposition,[],[f6767,f35247]) ).
fof(f36619,plain,
! [X0] : additive_identity = multiply(additive_identity,add(X0,additive_inverse(multiply(additive_identity,X0)))),
inference(forward_demodulation,[],[f36603,f489]) ).
fof(f36871,plain,
! [X0] : additive_identity = multiply(additive_identity,add(add(X0,X0),additive_inverse(multiply(add(additive_identity,additive_identity),X0)))),
inference(superposition,[],[f36619,f379]) ).
fof(f36932,plain,
! [X0,X1] : add(additive_identity,multiply(additive_identity,X0)) = multiply(additive_identity,add(X0,add(X1,additive_inverse(multiply(additive_identity,X1))))),
inference(superposition,[],[f251,f36619]) ).
fof(f36949,plain,
! [X0,X1] : multiply(additive_identity,X0) = multiply(additive_identity,add(X0,add(X1,additive_inverse(multiply(additive_identity,X1))))),
inference(forward_demodulation,[],[f36932,f1]) ).
fof(f37001,plain,
! [X0] : additive_identity = multiply(additive_identity,add(X0,add(X0,additive_inverse(multiply(add(additive_identity,additive_identity),X0))))),
inference(forward_demodulation,[],[f36871,f7]) ).
fof(f37157,plain,
! [X0] : additive_identity = multiply(additive_identity,add(X0,add(X0,additive_inverse(multiply(additive_identity,X0))))),
inference(forward_demodulation,[],[f37001,f2]) ).
fof(f37271,plain,
! [X0] : additive_identity = multiply(additive_identity,X0),
inference(forward_demodulation,[],[f37157,f36949]) ).
fof(f54764,plain,
multiply(additive_inverse(c),multiply(c,c)) = multiply(additive_inverse(multiply(a,a)),c),
inference(superposition,[],[f13403,f12]) ).
fof(f54765,plain,
! [X0] : multiply(additive_inverse(multiply(a,a)),multiply(c,X0)) = multiply(additive_inverse(c),multiply(c,multiply(c,X0))),
inference(superposition,[],[f13403,f71]) ).
fof(f54822,plain,
! [X0] : multiply(additive_inverse(c),X0) = multiply(additive_inverse(c),multiply(c,multiply(c,X0))),
inference(forward_demodulation,[],[f54765,f13403]) ).
fof(f54823,plain,
additive_inverse(c) = multiply(additive_inverse(c),multiply(c,c)),
inference(forward_demodulation,[],[f54764,f13340]) ).
fof(f54877,plain,
! [X0,X1] : multiply(add(X0,multiply(X1,additive_inverse(c))),multiply(c,c)) = add(multiply(X0,multiply(c,c)),multiply(X1,additive_inverse(c))),
inference(superposition,[],[f367,f54823]) ).
fof(f76134,plain,
! [X0] : multiply(a,additive_inverse(multiply(b,X0))) = additive_inverse(multiply(c,X0)),
inference(superposition,[],[f47,f12619]) ).
fof(f77725,plain,
! [X0] : add(c,add(add(a,multiply(a,additive_inverse(add(multiply(a,a),b)))),X0)) = X0,
inference(superposition,[],[f14831,f234]) ).
fof(f77871,plain,
! [X0] : add(c,add(a,add(multiply(a,additive_inverse(add(multiply(a,a),b))),X0))) = X0,
inference(forward_demodulation,[],[f77725,f7]) ).
fof(f77915,plain,
! [X0] : add(a,add(add(multiply(a,additive_inverse(add(multiply(a,a),b))),X0),c)) = X0,
inference(forward_demodulation,[],[f77871,f41]) ).
fof(f77940,plain,
! [X0] : add(a,add(c,add(multiply(a,additive_inverse(add(multiply(a,a),b))),X0))) = X0,
inference(forward_demodulation,[],[f77915,f8]) ).
fof(f77953,plain,
! [X0] : add(a,add(X0,multiply(a,additive_inverse(multiply(a,a))))) = X0,
inference(forward_demodulation,[],[f77940,f34682]) ).
fof(f78171,plain,
additive_inverse(a) = multiply(a,additive_inverse(multiply(a,a))),
inference(superposition,[],[f43,f77953]) ).
fof(f78301,plain,
! [X0] : multiply(additive_inverse(a),X0) = multiply(a,multiply(additive_inverse(multiply(a,a)),X0)),
inference(superposition,[],[f9,f78171]) ).
fof(f78307,plain,
additive_inverse(a) = multiply(a,multiply(a,additive_inverse(a))),
inference(superposition,[],[f71,f78171]) ).
fof(f78351,plain,
! [X0] : multiply(additive_inverse(a),X0) = multiply(a,multiply(multiply(a,additive_inverse(a)),X0)),
inference(superposition,[],[f9,f78307]) ).
fof(f78384,plain,
! [X0] : multiply(additive_inverse(a),X0) = multiply(a,multiply(a,multiply(additive_inverse(a),X0))),
inference(forward_demodulation,[],[f78351,f9]) ).
fof(f79150,plain,
multiply(a,additive_inverse(c)) = multiply(additive_inverse(a),c),
inference(superposition,[],[f78301,f13340]) ).
fof(f79276,plain,
c = multiply(additive_inverse(a),multiply(a,additive_inverse(c))),
inference(superposition,[],[f5416,f79150]) ).
fof(f79324,plain,
! [X0] : multiply(c,X0) = multiply(additive_inverse(a),multiply(multiply(a,additive_inverse(c)),X0)),
inference(superposition,[],[f9,f79276]) ).
fof(f79356,plain,
! [X0] : multiply(c,X0) = multiply(additive_inverse(a),multiply(a,multiply(additive_inverse(c),X0))),
inference(forward_demodulation,[],[f79324,f9]) ).
fof(f79704,plain,
multiply(c,multiply(additive_inverse(c),additive_inverse(c))) = multiply(additive_inverse(a),multiply(a,additive_inverse(c))),
inference(superposition,[],[f79356,f12]) ).
fof(f79705,plain,
! [X0] : multiply(additive_inverse(a),multiply(a,multiply(additive_inverse(c),X0))) = multiply(c,multiply(additive_inverse(c),multiply(additive_inverse(c),X0))),
inference(superposition,[],[f79356,f71]) ).
fof(f79760,plain,
! [X0] : multiply(c,X0) = multiply(c,multiply(additive_inverse(c),multiply(additive_inverse(c),X0))),
inference(forward_demodulation,[],[f79705,f79356]) ).
fof(f79761,plain,
c = multiply(c,multiply(additive_inverse(c),additive_inverse(c))),
inference(forward_demodulation,[],[f79704,f79276]) ).
fof(f79789,plain,
multiply(c,c) = multiply(additive_inverse(c),additive_inverse(c)),
inference(superposition,[],[f3413,f79761]) ).
fof(f79816,plain,
c = multiply(c,multiply(multiply(additive_inverse(c),additive_inverse(c)),multiply(c,multiply(multiply(additive_inverse(c),additive_inverse(c)),c)))),
inference(superposition,[],[f67,f79761]) ).
fof(f79839,plain,
c = multiply(c,multiply(additive_inverse(c),multiply(additive_inverse(c),multiply(c,multiply(multiply(additive_inverse(c),additive_inverse(c)),c))))),
inference(forward_demodulation,[],[f79816,f9]) ).
fof(f79860,plain,
c = multiply(c,multiply(c,multiply(multiply(additive_inverse(c),additive_inverse(c)),c))),
inference(forward_demodulation,[],[f79839,f79760]) ).
fof(f79872,plain,
c = multiply(c,multiply(c,multiply(additive_inverse(c),multiply(additive_inverse(c),c)))),
inference(forward_demodulation,[],[f79860,f9]) ).
fof(f79875,plain,
c = multiply(additive_inverse(c),multiply(additive_inverse(c),c)),
inference(forward_demodulation,[],[f79872,f3413]) ).
fof(f80526,plain,
! [X0,X1] : add(multiply(X0,multiply(c,c)),multiply(X1,additive_inverse(c))) = multiply(add(multiply(X0,additive_inverse(c)),X1),additive_inverse(c)),
inference(superposition,[],[f357,f79789]) ).
fof(f80574,plain,
multiply(c,multiply(additive_inverse(c),c)) = multiply(additive_inverse(a),multiply(a,c)),
inference(superposition,[],[f79356,f79875]) ).
fof(f80962,plain,
! [X0] : multiply(additive_inverse(a),multiply(multiply(a,c),X0)) = multiply(multiply(c,multiply(additive_inverse(c),c)),X0),
inference(superposition,[],[f9,f80574]) ).
fof(f80990,plain,
! [X0] : multiply(additive_inverse(a),multiply(multiply(a,c),X0)) = multiply(c,multiply(multiply(additive_inverse(c),c),X0)),
inference(forward_demodulation,[],[f80962,f9]) ).
fof(f80995,plain,
! [X0] : multiply(additive_inverse(a),multiply(multiply(a,c),X0)) = multiply(c,multiply(additive_inverse(c),multiply(c,X0))),
inference(forward_demodulation,[],[f80990,f9]) ).
fof(f80997,plain,
! [X0] : multiply(c,multiply(additive_inverse(c),multiply(c,X0))) = multiply(additive_inverse(a),multiply(a,multiply(c,X0))),
inference(forward_demodulation,[],[f80995,f9]) ).
fof(f81327,plain,
additive_identity = multiply(additive_inverse(add(additive_inverse(multiply(c,b)),a)),b),
inference(superposition,[],[f18634,f15817]) ).
fof(f81394,plain,
additive_identity = multiply(additive_inverse(add(a,additive_inverse(multiply(c,b)))),b),
inference(forward_demodulation,[],[f81327,f8]) ).
fof(f85043,plain,
! [X0] : multiply(additive_inverse(multiply(X0,a)),b) = additive_inverse(multiply(X0,c)),
inference(superposition,[],[f47,f30796]) ).
fof(f91248,plain,
multiply(add(b,additive_inverse(multiply(a,c))),a) = multiply(add(b,additive_inverse(multiply(a,c))),multiply(additive_identity,multiply(a,multiply(add(b,additive_inverse(multiply(a,c))),a)))),
inference(superposition,[],[f67,f13694]) ).
fof(f91299,plain,
multiply(add(b,additive_inverse(multiply(a,c))),a) = multiply(additive_identity,multiply(a,multiply(add(b,additive_inverse(multiply(a,c))),a))),
inference(forward_demodulation,[],[f91248,f35247]) ).
fof(f91352,plain,
additive_identity = multiply(add(b,additive_inverse(multiply(a,c))),a),
inference(forward_demodulation,[],[f91299,f37271]) ).
fof(f91489,plain,
! [X0] : multiply(additive_identity,X0) = multiply(add(b,additive_inverse(multiply(a,c))),multiply(a,X0)),
inference(superposition,[],[f9,f91352]) ).
fof(f91530,plain,
! [X0] : additive_identity = multiply(add(b,additive_inverse(multiply(a,c))),multiply(a,X0)),
inference(forward_demodulation,[],[f91489,f37271]) ).
fof(f91960,plain,
! [X0] : additive_identity = multiply(add(b,additive_inverse(multiply(a,c))),multiply(additive_inverse(a),X0)),
inference(superposition,[],[f91530,f78384]) ).
fof(f92308,plain,
! [X0] : add(multiply(add(X0,a),add(additive_inverse(b),b)),additive_inverse(c)) = add(c,add(multiply(X0,b),multiply(add(add(X0,a),a),additive_inverse(b)))),
inference(superposition,[],[f7504,f391]) ).
fof(f92437,plain,
! [X0] : add(multiply(add(X0,a),add(additive_inverse(b),b)),additive_inverse(c)) = add(multiply(add(X0,a),additive_inverse(b)),multiply(X0,b)),
inference(forward_demodulation,[],[f92308,f5933]) ).
fof(f92563,plain,
! [X0] : add(multiply(add(X0,a),add(additive_inverse(b),b)),additive_inverse(c)) = add(multiply(X0,b),multiply(add(X0,a),additive_inverse(b))),
inference(forward_demodulation,[],[f92437,f8]) ).
fof(f92671,plain,
! [X0] : add(multiply(X0,b),multiply(add(X0,a),additive_inverse(b))) = add(additive_inverse(c),multiply(add(X0,a),add(additive_inverse(b),b))),
inference(forward_demodulation,[],[f92563,f8]) ).
fof(f92754,plain,
! [X0] : add(multiply(X0,b),multiply(add(X0,a),additive_inverse(b))) = add(additive_inverse(c),multiply(add(X0,a),add(b,additive_inverse(b)))),
inference(forward_demodulation,[],[f92671,f3568]) ).
fof(f92816,plain,
! [X0] : add(multiply(X0,b),multiply(add(X0,a),additive_inverse(b))) = add(additive_inverse(c),multiply(add(X0,a),additive_identity)),
inference(forward_demodulation,[],[f92754,f6]) ).
fof(f92869,plain,
! [X0] : add(additive_inverse(c),multiply(X0,additive_identity)) = add(multiply(X0,b),multiply(add(X0,a),additive_inverse(b))),
inference(forward_demodulation,[],[f92816,f402]) ).
fof(f92916,plain,
! [X0] : add(additive_inverse(c),additive_identity) = add(multiply(X0,b),multiply(add(X0,a),additive_inverse(b))),
inference(forward_demodulation,[],[f92869,f35144]) ).
fof(f92956,plain,
! [X0] : add(additive_identity,additive_inverse(c)) = add(multiply(X0,b),multiply(add(X0,a),additive_inverse(b))),
inference(forward_demodulation,[],[f92916,f8]) ).
fof(f92987,plain,
! [X0] : additive_inverse(c) = add(multiply(X0,b),multiply(add(X0,a),additive_inverse(b))),
inference(forward_demodulation,[],[f92956,f1]) ).
fof(f94818,plain,
additive_inverse(c) = add(additive_identity,multiply(add(additive_inverse(add(a,additive_inverse(multiply(c,b)))),a),additive_inverse(b))),
inference(superposition,[],[f92987,f81394]) ).
fof(f94851,plain,
add(c,additive_inverse(c)) = multiply(add(additive_inverse(multiply(c,b)),a),additive_inverse(b)),
inference(superposition,[],[f15929,f92987]) ).
fof(f94918,plain,
add(c,additive_inverse(c)) = multiply(add(a,additive_inverse(multiply(c,b))),additive_inverse(b)),
inference(forward_demodulation,[],[f94851,f4279]) ).
fof(f94947,plain,
additive_inverse(c) = multiply(add(additive_inverse(add(a,additive_inverse(multiply(c,b)))),a),additive_inverse(b)),
inference(forward_demodulation,[],[f94818,f1]) ).
fof(f94998,plain,
additive_identity = multiply(add(a,additive_inverse(multiply(c,b))),additive_inverse(b)),
inference(forward_demodulation,[],[f94918,f6]) ).
fof(f95022,plain,
additive_inverse(c) = multiply(add(a,additive_inverse(add(a,additive_inverse(multiply(c,b))))),additive_inverse(b)),
inference(forward_demodulation,[],[f94947,f4279]) ).
fof(f95075,plain,
additive_inverse(c) = multiply(multiply(c,b),additive_inverse(b)),
inference(forward_demodulation,[],[f95022,f192]) ).
fof(f95110,plain,
additive_inverse(c) = multiply(c,multiply(b,additive_inverse(b))),
inference(forward_demodulation,[],[f95075,f9]) ).
fof(f95173,plain,
multiply(additive_inverse(c),multiply(c,additive_inverse(c))) = multiply(additive_inverse(c),multiply(b,additive_inverse(b))),
inference(superposition,[],[f54822,f95110]) ).
fof(f95182,plain,
! [X0] : multiply(additive_inverse(c),X0) = multiply(c,multiply(multiply(b,additive_inverse(b)),X0)),
inference(superposition,[],[f9,f95110]) ).
fof(f95214,plain,
! [X0] : multiply(additive_inverse(c),X0) = multiply(c,multiply(b,multiply(additive_inverse(b),X0))),
inference(forward_demodulation,[],[f95182,f9]) ).
fof(f96189,plain,
add(c,additive_identity) = multiply(additive_inverse(multiply(c,b)),additive_inverse(b)),
inference(superposition,[],[f380,f94998]) ).
fof(f96196,plain,
! [X0] : multiply(additive_identity,X0) = multiply(add(a,additive_inverse(multiply(c,b))),multiply(additive_inverse(b),X0)),
inference(superposition,[],[f9,f94998]) ).
fof(f96236,plain,
! [X0] : additive_identity = multiply(add(a,additive_inverse(multiply(c,b))),multiply(additive_inverse(b),X0)),
inference(forward_demodulation,[],[f96196,f37271]) ).
fof(f96243,plain,
add(additive_identity,c) = multiply(additive_inverse(multiply(c,b)),additive_inverse(b)),
inference(forward_demodulation,[],[f96189,f8]) ).
fof(f96263,plain,
c = multiply(additive_inverse(multiply(c,b)),additive_inverse(b)),
inference(forward_demodulation,[],[f96243,f1]) ).
fof(f96280,plain,
! [X0] : multiply(c,X0) = multiply(additive_inverse(multiply(c,b)),multiply(additive_inverse(b),X0)),
inference(superposition,[],[f9,f96263]) ).
fof(f97148,plain,
multiply(additive_inverse(b),additive_identity) = multiply(additive_inverse(b),add(a,additive_inverse(multiply(c,b)))),
inference(superposition,[],[f67,f96236]) ).
fof(f97198,plain,
additive_identity = multiply(additive_inverse(b),add(a,additive_inverse(multiply(c,b)))),
inference(forward_demodulation,[],[f97148,f35144]) ).
fof(f98357,plain,
multiply(c,multiply(additive_inverse(b),additive_identity)) = multiply(c,add(a,additive_inverse(multiply(c,b)))),
inference(superposition,[],[f5583,f97198]) ).
fof(f98404,plain,
multiply(c,additive_identity) = multiply(c,add(a,additive_inverse(multiply(c,b)))),
inference(forward_demodulation,[],[f98357,f35144]) ).
fof(f98420,plain,
additive_identity = multiply(c,add(a,additive_inverse(multiply(c,b)))),
inference(forward_demodulation,[],[f98404,f35144]) ).
fof(f98449,plain,
! [X0] : multiply(additive_identity,X0) = multiply(c,multiply(add(a,additive_inverse(multiply(c,b))),X0)),
inference(superposition,[],[f9,f98420]) ).
fof(f98489,plain,
! [X0] : additive_identity = multiply(c,multiply(add(a,additive_inverse(multiply(c,b))),X0)),
inference(forward_demodulation,[],[f98449,f37271]) ).
fof(f98663,plain,
multiply(add(a,additive_inverse(multiply(c,b))),additive_identity) = multiply(add(a,additive_inverse(multiply(c,b))),c),
inference(superposition,[],[f67,f98489]) ).
fof(f98712,plain,
multiply(additive_inverse(multiply(c,b)),additive_identity) = multiply(add(a,additive_inverse(multiply(c,b))),c),
inference(forward_demodulation,[],[f98663,f34965]) ).
fof(f98757,plain,
additive_identity = multiply(add(a,additive_inverse(multiply(c,b))),c),
inference(forward_demodulation,[],[f98712,f35144]) ).
fof(f98797,plain,
! [X0] : multiply(additive_identity,X0) = multiply(add(a,additive_inverse(multiply(c,b))),multiply(c,X0)),
inference(superposition,[],[f9,f98757]) ).
fof(f98837,plain,
! [X0] : additive_identity = multiply(add(a,additive_inverse(multiply(c,b))),multiply(c,X0)),
inference(forward_demodulation,[],[f98797,f37271]) ).
fof(f98922,plain,
! [X0] : additive_identity = multiply(add(a,additive_inverse(multiply(c,b))),multiply(additive_inverse(c),X0)),
inference(superposition,[],[f98837,f3413]) ).
fof(f99144,plain,
multiply(additive_inverse(a),additive_identity) = multiply(additive_inverse(a),add(b,additive_inverse(multiply(a,c)))),
inference(superposition,[],[f67,f91960]) ).
fof(f99194,plain,
multiply(additive_identity,additive_identity) = multiply(additive_inverse(a),add(b,additive_inverse(multiply(a,c)))),
inference(forward_demodulation,[],[f99144,f413]) ).
fof(f99220,plain,
additive_identity = multiply(additive_inverse(a),add(b,additive_inverse(multiply(a,c)))),
inference(forward_demodulation,[],[f99194,f37271]) ).
fof(f100289,plain,
add(c,additive_identity) = multiply(additive_inverse(a),additive_inverse(multiply(a,c))),
inference(superposition,[],[f770,f99220]) ).
fof(f100345,plain,
add(additive_identity,c) = multiply(additive_inverse(a),additive_inverse(multiply(a,c))),
inference(forward_demodulation,[],[f100289,f8]) ).
fof(f100363,plain,
c = multiply(additive_inverse(a),additive_inverse(multiply(a,c))),
inference(forward_demodulation,[],[f100345,f1]) ).
fof(f100382,plain,
! [X0] : multiply(c,X0) = multiply(additive_inverse(a),multiply(additive_inverse(multiply(a,c)),X0)),
inference(superposition,[],[f9,f100363]) ).
fof(f116447,plain,
multiply(add(b,multiply(a,additive_inverse(c))),a) = multiply(add(b,multiply(a,additive_inverse(c))),multiply(additive_identity,multiply(a,multiply(add(b,multiply(a,additive_inverse(c))),a)))),
inference(superposition,[],[f67,f13807]) ).
fof(f116494,plain,
multiply(add(b,multiply(a,additive_inverse(c))),a) = multiply(add(b,a),multiply(additive_identity,multiply(a,multiply(add(b,multiply(a,additive_inverse(c))),a)))),
inference(forward_demodulation,[],[f116447,f9776]) ).
fof(f116557,plain,
multiply(add(b,multiply(a,additive_inverse(c))),a) = multiply(b,multiply(additive_identity,multiply(a,multiply(add(b,multiply(a,additive_inverse(c))),a)))),
inference(forward_demodulation,[],[f116494,f406]) ).
fof(f116612,plain,
multiply(add(b,multiply(a,additive_inverse(c))),a) = multiply(additive_identity,multiply(a,multiply(add(b,multiply(a,additive_inverse(c))),a))),
inference(forward_demodulation,[],[f116557,f35247]) ).
fof(f116660,plain,
additive_identity = multiply(add(b,multiply(a,additive_inverse(c))),a),
inference(forward_demodulation,[],[f116612,f37271]) ).
fof(f116744,plain,
! [X0] : add(multiply(add(b,multiply(a,additive_inverse(c))),c),add(X0,multiply(additive_inverse(additive_identity),b))) = X0,
inference(superposition,[],[f30847,f116660]) ).
fof(f116745,plain,
multiply(additive_inverse(additive_identity),b) = additive_inverse(multiply(add(b,multiply(a,additive_inverse(c))),c)),
inference(superposition,[],[f85043,f116660]) ).
fof(f116746,plain,
! [X0] : multiply(additive_identity,X0) = multiply(add(b,multiply(a,additive_inverse(c))),multiply(a,X0)),
inference(superposition,[],[f9,f116660]) ).
fof(f116787,plain,
! [X0] : additive_identity = multiply(add(b,multiply(a,additive_inverse(c))),multiply(a,X0)),
inference(forward_demodulation,[],[f116746,f37271]) ).
fof(f116788,plain,
multiply(additive_identity,b) = additive_inverse(multiply(add(b,multiply(a,additive_inverse(c))),c)),
inference(forward_demodulation,[],[f116745,f18]) ).
fof(f116789,plain,
! [X0] : add(multiply(additive_inverse(additive_identity),b),add(multiply(add(b,multiply(a,additive_inverse(c))),c),X0)) = X0,
inference(forward_demodulation,[],[f116744,f41]) ).
fof(f116817,plain,
additive_identity = additive_inverse(multiply(add(b,multiply(a,additive_inverse(c))),c)),
inference(forward_demodulation,[],[f116788,f37271]) ).
fof(f116818,plain,
! [X0] : add(multiply(additive_identity,b),add(multiply(add(b,multiply(a,additive_inverse(c))),c),X0)) = X0,
inference(forward_demodulation,[],[f116789,f18]) ).
fof(f116833,plain,
! [X0] : add(additive_identity,add(multiply(add(b,multiply(a,additive_inverse(c))),c),X0)) = X0,
inference(forward_demodulation,[],[f116818,f37271]) ).
fof(f116842,plain,
! [X0] : add(multiply(add(b,multiply(a,additive_inverse(c))),c),X0) = X0,
inference(forward_demodulation,[],[f116833,f1]) ).
fof(f116861,plain,
! [X0] : multiply(additive_inverse(add(additive_identity,multiply(additive_identity,X0))),X0) = multiply(multiply(add(b,multiply(a,additive_inverse(c))),c),X0),
inference(superposition,[],[f21119,f116817]) ).
fof(f116863,plain,
multiply(additive_inverse(add(additive_identity,multiply(additive_identity,a))),c) = multiply(multiply(add(b,multiply(a,additive_inverse(c))),c),c),
inference(superposition,[],[f28781,f116817]) ).
fof(f116864,plain,
multiply(additive_inverse(add(additive_identity,multiply(additive_identity,a))),c) = multiply(add(b,multiply(a,additive_inverse(c))),multiply(c,c)),
inference(forward_demodulation,[],[f116863,f9]) ).
fof(f116866,plain,
! [X0] : multiply(additive_inverse(add(additive_identity,multiply(additive_identity,X0))),X0) = multiply(add(b,multiply(a,additive_inverse(c))),multiply(c,X0)),
inference(forward_demodulation,[],[f116861,f9]) ).
fof(f116878,plain,
multiply(additive_inverse(add(additive_identity,multiply(additive_identity,a))),c) = add(multiply(b,multiply(c,c)),multiply(a,additive_inverse(c))),
inference(forward_demodulation,[],[f116864,f54877]) ).
fof(f116880,plain,
! [X0] : multiply(additive_inverse(multiply(additive_identity,X0)),X0) = multiply(add(b,multiply(a,additive_inverse(c))),multiply(c,X0)),
inference(forward_demodulation,[],[f116866,f1]) ).
fof(f116889,plain,
multiply(additive_inverse(add(additive_identity,multiply(additive_identity,a))),c) = multiply(add(multiply(b,additive_inverse(c)),a),additive_inverse(c)),
inference(forward_demodulation,[],[f116878,f80526]) ).
fof(f116890,plain,
! [X0] : multiply(additive_identity,X0) = multiply(add(b,multiply(a,additive_inverse(c))),multiply(c,X0)),
inference(forward_demodulation,[],[f116880,f21118]) ).
fof(f116895,plain,
multiply(additive_inverse(add(additive_identity,multiply(additive_identity,a))),c) = multiply(add(a,multiply(b,additive_inverse(c))),additive_inverse(c)),
inference(forward_demodulation,[],[f116889,f4279]) ).
fof(f116896,plain,
! [X0] : additive_identity = multiply(add(b,multiply(a,additive_inverse(c))),multiply(c,X0)),
inference(forward_demodulation,[],[f116890,f37271]) ).
fof(f116901,plain,
multiply(additive_inverse(multiply(additive_identity,a)),c) = multiply(add(a,multiply(b,additive_inverse(c))),additive_inverse(c)),
inference(forward_demodulation,[],[f116895,f1]) ).
fof(f116904,plain,
additive_identity = multiply(add(a,multiply(b,additive_inverse(c))),additive_inverse(c)),
inference(forward_demodulation,[],[f116901,f28834]) ).
fof(f117004,plain,
! [X0] : multiply(additive_identity,X0) = multiply(add(a,multiply(b,additive_inverse(c))),multiply(additive_inverse(c),X0)),
inference(superposition,[],[f9,f116904]) ).
fof(f117044,plain,
! [X0] : additive_identity = multiply(add(a,multiply(b,additive_inverse(c))),multiply(additive_inverse(c),X0)),
inference(forward_demodulation,[],[f117004,f37271]) ).
fof(f117404,plain,
additive_identity = multiply(add(b,multiply(a,additive_inverse(c))),additive_inverse(c)),
inference(superposition,[],[f116787,f972]) ).
fof(f120286,plain,
multiply(c,additive_identity) = multiply(c,add(b,multiply(a,additive_inverse(c)))),
inference(superposition,[],[f67,f116896]) ).
fof(f120332,plain,
additive_identity = multiply(c,add(b,multiply(a,additive_inverse(c)))),
inference(forward_demodulation,[],[f120286,f35144]) ).
fof(f120396,plain,
multiply(additive_inverse(multiply(a,a)),additive_identity) = multiply(additive_inverse(c),add(b,multiply(a,additive_inverse(c)))),
inference(superposition,[],[f13403,f120332]) ).
fof(f120469,plain,
additive_identity = multiply(additive_inverse(c),add(b,multiply(a,additive_inverse(c)))),
inference(forward_demodulation,[],[f120396,f35144]) ).
fof(f121171,plain,
! [X0] : add(multiply(add(additive_inverse(a),a),add(b,X0)),additive_inverse(c)) = add(c,add(multiply(a,X0),multiply(additive_inverse(a),add(add(b,X0),b)))),
inference(superposition,[],[f11348,f813]) ).
fof(f121320,plain,
! [X0] : add(multiply(add(additive_inverse(a),a),add(b,X0)),additive_inverse(c)) = add(multiply(additive_inverse(a),add(b,X0)),multiply(a,X0)),
inference(forward_demodulation,[],[f121171,f5832]) ).
fof(f121496,plain,
! [X0] : add(multiply(a,X0),multiply(additive_inverse(a),add(b,X0))) = add(multiply(add(additive_inverse(a),a),add(b,X0)),additive_inverse(c)),
inference(forward_demodulation,[],[f121320,f8]) ).
fof(f121640,plain,
! [X0] : add(multiply(a,X0),multiply(additive_inverse(a),add(b,X0))) = add(multiply(add(a,additive_inverse(a)),add(b,X0)),additive_inverse(c)),
inference(forward_demodulation,[],[f121496,f21296]) ).
fof(f121759,plain,
! [X0] : add(multiply(a,X0),multiply(additive_inverse(a),add(b,X0))) = add(additive_inverse(c),multiply(add(a,additive_inverse(a)),add(b,X0))),
inference(forward_demodulation,[],[f121640,f8]) ).
fof(f121861,plain,
! [X0] : add(multiply(a,X0),multiply(additive_inverse(a),add(b,X0))) = add(additive_inverse(c),multiply(additive_identity,add(b,X0))),
inference(forward_demodulation,[],[f121759,f6]) ).
fof(f121944,plain,
! [X0] : add(additive_inverse(c),multiply(additive_identity,X0)) = add(multiply(a,X0),multiply(additive_inverse(a),add(b,X0))),
inference(forward_demodulation,[],[f121861,f643]) ).
fof(f122007,plain,
! [X0] : add(additive_inverse(c),additive_identity) = add(multiply(a,X0),multiply(additive_inverse(a),add(b,X0))),
inference(forward_demodulation,[],[f121944,f37271]) ).
fof(f122057,plain,
! [X0] : add(additive_identity,additive_inverse(c)) = add(multiply(a,X0),multiply(additive_inverse(a),add(b,X0))),
inference(forward_demodulation,[],[f122007,f8]) ).
fof(f122104,plain,
! [X0] : additive_inverse(c) = add(multiply(a,X0),multiply(additive_inverse(a),add(b,X0))),
inference(forward_demodulation,[],[f122057,f1]) ).
fof(f122243,plain,
additive_inverse(c) = add(c,multiply(additive_inverse(a),add(b,multiply(a,c)))),
inference(superposition,[],[f122104,f975]) ).
fof(f122369,plain,
additive_inverse(c) = multiply(additive_inverse(a),multiply(a,c)),
inference(forward_demodulation,[],[f122243,f770]) ).
fof(f122668,plain,
additive_inverse(c) = multiply(c,multiply(additive_inverse(c),c)),
inference(superposition,[],[f80574,f122369]) ).
fof(f122722,plain,
multiply(c,additive_inverse(c)) = multiply(additive_inverse(c),c),
inference(superposition,[],[f3413,f122668]) ).
fof(f122738,plain,
multiply(additive_inverse(c),multiply(additive_inverse(c),c)) = multiply(additive_inverse(c),multiply(c,additive_inverse(c))),
inference(superposition,[],[f54822,f122668]) ).
fof(f122751,plain,
! [X0] : multiply(additive_inverse(c),X0) = multiply(c,multiply(multiply(additive_inverse(c),c),X0)),
inference(superposition,[],[f9,f122668]) ).
fof(f122781,plain,
! [X0] : multiply(additive_inverse(c),X0) = multiply(c,multiply(additive_inverse(c),multiply(c,X0))),
inference(forward_demodulation,[],[f122751,f9]) ).
fof(f122788,plain,
multiply(additive_inverse(c),multiply(additive_inverse(c),c)) = multiply(additive_inverse(c),multiply(b,additive_inverse(b))),
inference(forward_demodulation,[],[f122738,f95173]) ).
fof(f122805,plain,
c = multiply(additive_inverse(c),multiply(b,additive_inverse(b))),
inference(forward_demodulation,[],[f122788,f79875]) ).
fof(f122821,plain,
c = multiply(additive_inverse(c),multiply(c,additive_inverse(c))),
inference(superposition,[],[f79875,f122722]) ).
fof(f122989,plain,
! [X0] : multiply(c,X0) = multiply(additive_inverse(c),multiply(multiply(b,additive_inverse(b)),X0)),
inference(superposition,[],[f9,f122805]) ).
fof(f123019,plain,
! [X0] : multiply(c,X0) = multiply(additive_inverse(c),multiply(b,multiply(additive_inverse(b),X0))),
inference(forward_demodulation,[],[f122989,f9]) ).
fof(f126982,plain,
additive_identity = multiply(add(a,multiply(b,additive_inverse(c))),c),
inference(superposition,[],[f117044,f122821]) ).
fof(f127003,plain,
multiply(additive_inverse(c),additive_identity) = multiply(additive_inverse(c),add(a,multiply(b,additive_inverse(c)))),
inference(superposition,[],[f67,f117044]) ).
fof(f127049,plain,
additive_identity = multiply(additive_inverse(c),add(a,multiply(b,additive_inverse(c)))),
inference(forward_demodulation,[],[f127003,f35144]) ).
fof(f127275,plain,
multiply(c,multiply(additive_inverse(c),additive_identity)) = multiply(c,add(a,multiply(b,additive_inverse(c)))),
inference(superposition,[],[f79760,f127049]) ).
fof(f127323,plain,
multiply(c,additive_identity) = multiply(c,add(a,multiply(b,additive_inverse(c)))),
inference(forward_demodulation,[],[f127275,f35144]) ).
fof(f127343,plain,
additive_identity = multiply(c,add(a,multiply(b,additive_inverse(c)))),
inference(forward_demodulation,[],[f127323,f35144]) ).
fof(f132166,plain,
! [X0,X1] : multiply(additive_identity,multiply(X0,X0)) = add(X0,multiply(add(X1,additive_inverse(add(X1,X0))),multiply(X0,X0))),
inference(superposition,[],[f356,f140]) ).
fof(f132257,plain,
! [X0,X1] : multiply(X0,additive_identity) = add(X0,multiply(X0,add(X1,additive_inverse(add(X1,multiply(X0,X0)))))),
inference(superposition,[],[f234,f140]) ).
fof(f132474,plain,
! [X0,X1] : additive_identity = add(X0,multiply(X0,add(X1,additive_inverse(add(X1,multiply(X0,X0)))))),
inference(forward_demodulation,[],[f132257,f35144]) ).
fof(f132563,plain,
! [X0,X1] : multiply(additive_identity,X0) = add(X0,multiply(add(X1,additive_inverse(add(X1,X0))),multiply(X0,X0))),
inference(forward_demodulation,[],[f132166,f20540]) ).
fof(f132907,plain,
! [X0,X1] : additive_identity = add(X0,multiply(add(X1,additive_inverse(add(X1,X0))),multiply(X0,X0))),
inference(forward_demodulation,[],[f132563,f37271]) ).
fof(f136080,plain,
! [X0] : additive_identity = add(X0,multiply(X0,additive_inverse(add(multiply(add(b,multiply(a,additive_inverse(c))),c),multiply(X0,X0))))),
inference(superposition,[],[f132474,f116842]) ).
fof(f136537,plain,
! [X0] : additive_identity = add(X0,multiply(X0,additive_inverse(multiply(X0,X0)))),
inference(forward_demodulation,[],[f136080,f116842]) ).
fof(f137139,plain,
! [X0] : add(X0,additive_identity) = multiply(additive_inverse(X0),additive_inverse(multiply(additive_inverse(X0),additive_inverse(X0)))),
inference(superposition,[],[f43,f136537]) ).
fof(f137448,plain,
! [X0] : multiply(additive_inverse(X0),additive_inverse(multiply(additive_inverse(X0),additive_inverse(X0)))) = X0,
inference(forward_demodulation,[],[f137139,f2]) ).
fof(f137964,plain,
! [X0] : additive_inverse(X0) = multiply(X0,additive_inverse(multiply(X0,X0))),
inference(superposition,[],[f137448,f59]) ).
fof(f138023,plain,
! [X0] : multiply(additive_inverse(X0),multiply(additive_inverse(X0),X0)) = X0,
inference(superposition,[],[f71,f137448]) ).
fof(f138125,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = multiply(X0,multiply(additive_inverse(multiply(X0,X0)),X1)),
inference(superposition,[],[f9,f137964]) ).
fof(f138131,plain,
! [X0] : additive_inverse(X0) = multiply(X0,multiply(X0,additive_inverse(X0))),
inference(superposition,[],[f71,f137964]) ).
fof(f138718,plain,
multiply(additive_inverse(a),multiply(a,c)) = multiply(c,multiply(additive_inverse(multiply(a,c)),multiply(a,c))),
inference(superposition,[],[f100382,f138023]) ).
fof(f138765,plain,
! [X0,X1] : multiply(X0,X1) = multiply(additive_inverse(X0),multiply(multiply(additive_inverse(X0),X0),X1)),
inference(superposition,[],[f9,f138023]) ).
fof(f138798,plain,
! [X0,X1] : multiply(X0,X1) = multiply(additive_inverse(X0),multiply(additive_inverse(X0),multiply(X0,X1))),
inference(forward_demodulation,[],[f138765,f9]) ).
fof(f138820,plain,
multiply(c,multiply(additive_inverse(c),c)) = multiply(c,multiply(additive_inverse(multiply(a,c)),multiply(a,c))),
inference(forward_demodulation,[],[f138718,f80574]) ).
fof(f138836,plain,
additive_inverse(c) = multiply(c,multiply(additive_inverse(multiply(a,c)),multiply(a,c))),
inference(forward_demodulation,[],[f138820,f122668]) ).
fof(f138880,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = multiply(X0,multiply(multiply(X0,additive_inverse(X0)),X1)),
inference(superposition,[],[f9,f138131]) ).
fof(f139233,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = multiply(X0,multiply(X0,multiply(additive_inverse(X0),X1))),
inference(forward_demodulation,[],[f138880,f9]) ).
fof(f150209,plain,
! [X0] : multiply(additive_inverse(X0),multiply(additive_inverse(X0),X0)) = multiply(X0,multiply(additive_inverse(X0),multiply(X0,multiply(additive_inverse(X0),X0)))),
inference(superposition,[],[f138798,f67]) ).
fof(f150317,plain,
! [X0] : multiply(X0,multiply(additive_inverse(X0),multiply(X0,multiply(additive_inverse(X0),X0)))) = X0,
inference(forward_demodulation,[],[f150209,f138023]) ).
fof(f156205,plain,
! [X0] : multiply(X0,X0) = multiply(additive_inverse(X0),multiply(X0,multiply(additive_inverse(X0),X0))),
inference(superposition,[],[f139233,f150317]) ).
fof(f157154,plain,
! [X0] : multiply(additive_inverse(X0),multiply(X0,X0)) = multiply(X0,multiply(additive_inverse(X0),X0)),
inference(superposition,[],[f138798,f156205]) ).
fof(f157162,plain,
multiply(c,multiply(multiply(a,c),multiply(additive_inverse(multiply(a,c)),multiply(a,c)))) = multiply(additive_inverse(a),multiply(multiply(a,c),multiply(a,c))),
inference(superposition,[],[f100382,f156205]) ).
fof(f157163,plain,
multiply(additive_inverse(c),multiply(multiply(a,c),multiply(additive_inverse(multiply(a,c)),multiply(a,c)))) = multiply(a,multiply(multiply(a,c),multiply(a,c))),
inference(superposition,[],[f4640,f156205]) ).
fof(f157287,plain,
multiply(additive_inverse(c),multiply(multiply(a,c),multiply(additive_inverse(multiply(a,c)),multiply(a,c)))) = multiply(a,multiply(a,multiply(c,multiply(a,c)))),
inference(forward_demodulation,[],[f157163,f9]) ).
fof(f157288,plain,
multiply(c,multiply(multiply(a,c),multiply(additive_inverse(multiply(a,c)),multiply(a,c)))) = multiply(additive_inverse(a),multiply(a,multiply(c,multiply(a,c)))),
inference(forward_demodulation,[],[f157162,f9]) ).
fof(f157336,plain,
multiply(c,multiply(a,c)) = multiply(additive_inverse(c),multiply(multiply(a,c),multiply(additive_inverse(multiply(a,c)),multiply(a,c)))),
inference(forward_demodulation,[],[f157287,f973]) ).
fof(f157337,plain,
multiply(c,multiply(multiply(a,c),multiply(additive_inverse(multiply(a,c)),multiply(a,c)))) = multiply(c,multiply(additive_inverse(c),multiply(c,multiply(a,c)))),
inference(forward_demodulation,[],[f157288,f80997]) ).
fof(f157360,plain,
multiply(c,multiply(a,c)) = multiply(additive_inverse(c),multiply(a,multiply(c,multiply(additive_inverse(multiply(a,c)),multiply(a,c))))),
inference(forward_demodulation,[],[f157336,f9]) ).
fof(f157361,plain,
multiply(additive_inverse(c),multiply(a,c)) = multiply(c,multiply(multiply(a,c),multiply(additive_inverse(multiply(a,c)),multiply(a,c)))),
inference(forward_demodulation,[],[f157337,f122781]) ).
fof(f157373,plain,
multiply(c,multiply(a,c)) = multiply(additive_inverse(c),multiply(a,additive_inverse(c))),
inference(forward_demodulation,[],[f157360,f138836]) ).
fof(f157374,plain,
multiply(additive_inverse(c),multiply(a,c)) = multiply(c,multiply(a,multiply(c,multiply(additive_inverse(multiply(a,c)),multiply(a,c))))),
inference(forward_demodulation,[],[f157361,f9]) ).
fof(f157381,plain,
multiply(c,multiply(a,additive_inverse(c))) = multiply(additive_inverse(c),multiply(a,c)),
inference(forward_demodulation,[],[f157374,f138836]) ).
fof(f160172,plain,
! [X0,X1] : multiply(multiply(X0,multiply(additive_inverse(X0),X0)),X1) = multiply(additive_inverse(X0),multiply(multiply(X0,X0),X1)),
inference(superposition,[],[f9,f157154]) ).
fof(f160202,plain,
! [X0,X1] : multiply(multiply(X0,multiply(additive_inverse(X0),X0)),X1) = multiply(additive_inverse(X0),multiply(X0,multiply(X0,X1))),
inference(forward_demodulation,[],[f160172,f9]) ).
fof(f160268,plain,
! [X0,X1] : multiply(X0,multiply(multiply(additive_inverse(X0),X0),X1)) = multiply(additive_inverse(X0),multiply(X0,multiply(X0,X1))),
inference(forward_demodulation,[],[f160202,f9]) ).
fof(f160306,plain,
! [X0,X1] : multiply(X0,multiply(additive_inverse(X0),multiply(X0,X1))) = multiply(additive_inverse(X0),multiply(X0,multiply(X0,X1))),
inference(forward_demodulation,[],[f160268,f9]) ).
fof(f162782,plain,
! [X0,X1] : add(X0,additive_identity) = multiply(add(X1,additive_inverse(add(X1,additive_inverse(X0)))),multiply(additive_inverse(X0),additive_inverse(X0))),
inference(superposition,[],[f43,f132907]) ).
fof(f163021,plain,
! [X0] : add(X0,additive_identity) = multiply(X0,multiply(additive_inverse(X0),additive_inverse(X0))),
inference(forward_demodulation,[],[f162782,f192]) ).
fof(f163377,plain,
! [X0] : multiply(X0,multiply(additive_inverse(X0),additive_inverse(X0))) = X0,
inference(forward_demodulation,[],[f163021,f2]) ).
fof(f164473,plain,
! [X0] : multiply(X0,X0) = multiply(additive_inverse(X0),additive_inverse(X0)),
inference(superposition,[],[f139233,f163377]) ).
fof(f164594,plain,
! [X0] : multiply(X0,additive_inverse(multiply(X0,X0))) = multiply(additive_inverse(X0),multiply(additive_inverse(additive_inverse(multiply(X0,X0))),additive_inverse(additive_inverse(multiply(X0,X0))))),
inference(superposition,[],[f138125,f163377]) ).
fof(f164649,plain,
multiply(additive_inverse(c),b) = multiply(c,additive_inverse(b)),
inference(superposition,[],[f123019,f163377]) ).
fof(f164795,plain,
! [X0] : multiply(X0,additive_inverse(multiply(X0,X0))) = multiply(additive_inverse(X0),multiply(multiply(X0,X0),multiply(X0,X0))),
inference(forward_demodulation,[],[f164594,f59]) ).
fof(f164941,plain,
! [X0] : multiply(X0,additive_inverse(multiply(X0,X0))) = multiply(additive_inverse(X0),multiply(X0,multiply(X0,multiply(X0,X0)))),
inference(forward_demodulation,[],[f164795,f9]) ).
fof(f165029,plain,
! [X0] : multiply(X0,additive_inverse(multiply(X0,X0))) = multiply(X0,multiply(additive_inverse(X0),multiply(X0,multiply(X0,X0)))),
inference(forward_demodulation,[],[f164941,f160306]) ).
fof(f165086,plain,
! [X0] : multiply(X0,additive_inverse(multiply(X0,X0))) = multiply(X0,multiply(X0,multiply(additive_inverse(X0),multiply(X0,X0)))),
inference(forward_demodulation,[],[f165029,f160306]) ).
fof(f165118,plain,
! [X0] : multiply(X0,additive_inverse(multiply(X0,X0))) = multiply(additive_inverse(X0),multiply(X0,X0)),
inference(forward_demodulation,[],[f165086,f139233]) ).
fof(f165133,plain,
! [X0] : multiply(X0,additive_inverse(multiply(X0,X0))) = multiply(X0,multiply(additive_inverse(X0),X0)),
inference(forward_demodulation,[],[f165118,f157154]) ).
fof(f165141,plain,
! [X0] : additive_inverse(X0) = multiply(X0,multiply(additive_inverse(X0),X0)),
inference(forward_demodulation,[],[f165133,f137964]) ).
fof(f166467,plain,
! [X0] : multiply(additive_inverse(X0),X0) = multiply(X0,additive_inverse(X0)),
inference(superposition,[],[f139233,f165141]) ).
fof(f166474,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = multiply(X0,multiply(multiply(additive_inverse(X0),X0),X1)),
inference(superposition,[],[f9,f165141]) ).
fof(f166874,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = multiply(X0,multiply(additive_inverse(X0),multiply(X0,X1))),
inference(forward_demodulation,[],[f166474,f9]) ).
fof(f167129,plain,
multiply(c,additive_inverse(multiply(a,c))) = multiply(additive_inverse(a),multiply(multiply(a,c),multiply(a,c))),
inference(superposition,[],[f100382,f164473]) ).
fof(f167130,plain,
multiply(additive_inverse(c),additive_inverse(multiply(a,c))) = multiply(a,multiply(multiply(a,c),multiply(a,c))),
inference(superposition,[],[f4640,f164473]) ).
fof(f167203,plain,
! [X0,X1] : multiply(multiply(X0,X0),X1) = multiply(additive_inverse(X0),multiply(additive_inverse(X0),X1)),
inference(superposition,[],[f9,f164473]) ).
fof(f167229,plain,
! [X0,X1] : multiply(X0,multiply(X0,X1)) = multiply(additive_inverse(X0),multiply(additive_inverse(X0),X1)),
inference(forward_demodulation,[],[f167203,f9]) ).
fof(f167282,plain,
multiply(additive_inverse(c),additive_inverse(multiply(a,c))) = multiply(a,multiply(a,multiply(c,multiply(a,c)))),
inference(forward_demodulation,[],[f167130,f9]) ).
fof(f167283,plain,
multiply(c,additive_inverse(multiply(a,c))) = multiply(additive_inverse(a),multiply(a,multiply(c,multiply(a,c)))),
inference(forward_demodulation,[],[f167129,f9]) ).
fof(f167330,plain,
multiply(c,multiply(a,c)) = multiply(additive_inverse(c),additive_inverse(multiply(a,c))),
inference(forward_demodulation,[],[f167282,f973]) ).
fof(f167331,plain,
multiply(c,additive_inverse(multiply(a,c))) = multiply(c,multiply(additive_inverse(c),multiply(c,multiply(a,c)))),
inference(forward_demodulation,[],[f167283,f80997]) ).
fof(f167356,plain,
multiply(c,additive_inverse(multiply(a,c))) = multiply(additive_inverse(c),multiply(a,c)),
inference(forward_demodulation,[],[f167331,f166874]) ).
fof(f167369,plain,
multiply(c,additive_inverse(multiply(a,c))) = multiply(c,multiply(a,additive_inverse(c))),
inference(forward_demodulation,[],[f167356,f157381]) ).
fof(f168172,plain,
! [X0] : multiply(additive_inverse(c),multiply(b,X0)) = multiply(multiply(c,additive_inverse(b)),X0),
inference(superposition,[],[f9,f164649]) ).
fof(f168199,plain,
! [X0] : multiply(c,multiply(additive_inverse(b),X0)) = multiply(additive_inverse(c),multiply(b,X0)),
inference(forward_demodulation,[],[f168172,f9]) ).
fof(f168311,plain,
! [X0] : multiply(additive_identity,X0) = add(X0,multiply(additive_inverse(multiply(X0,X0)),X0)),
inference(superposition,[],[f8248,f6]) ).
fof(f168835,plain,
! [X0] : additive_identity = add(X0,multiply(additive_inverse(multiply(X0,X0)),X0)),
inference(forward_demodulation,[],[f168311,f37271]) ).
fof(f169613,plain,
! [X0] : additive_identity = add(additive_inverse(X0),multiply(additive_inverse(multiply(X0,X0)),additive_inverse(X0))),
inference(superposition,[],[f168835,f164473]) ).
fof(f169700,plain,
! [X0] : add(X0,additive_identity) = multiply(additive_inverse(multiply(additive_inverse(X0),additive_inverse(X0))),additive_inverse(X0)),
inference(superposition,[],[f43,f168835]) ).
fof(f169944,plain,
! [X0] : add(X0,additive_identity) = multiply(additive_inverse(multiply(X0,X0)),additive_inverse(X0)),
inference(forward_demodulation,[],[f169700,f164473]) ).
fof(f170123,plain,
! [X0] : multiply(additive_inverse(multiply(X0,X0)),additive_inverse(X0)) = X0,
inference(forward_demodulation,[],[f169944,f2]) ).
fof(f170419,plain,
! [X0] : additive_inverse(X0) = multiply(additive_inverse(multiply(additive_inverse(X0),additive_inverse(X0))),X0),
inference(superposition,[],[f170123,f59]) ).
fof(f170434,plain,
! [X0,X1] : multiply(X0,X1) = multiply(additive_inverse(multiply(X0,X0)),multiply(additive_inverse(X0),X1)),
inference(superposition,[],[f9,f170123]) ).
fof(f170479,plain,
! [X0] : additive_inverse(X0) = multiply(additive_inverse(multiply(X0,X0)),X0),
inference(forward_demodulation,[],[f170419,f164473]) ).
fof(f170540,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = multiply(additive_inverse(multiply(X0,X0)),multiply(X0,X1)),
inference(superposition,[],[f9,f170479]) ).
fof(f185687,plain,
! [X0] : additive_inverse(multiply(X0,X0)) = multiply(multiply(X0,X0),multiply(additive_inverse(X0),X0)),
inference(superposition,[],[f165141,f170540]) ).
fof(f185763,plain,
! [X0] : additive_inverse(multiply(X0,X0)) = multiply(X0,multiply(X0,multiply(additive_inverse(X0),X0))),
inference(forward_demodulation,[],[f185687,f9]) ).
fof(f186310,plain,
! [X0] : additive_inverse(multiply(X0,X0)) = multiply(additive_inverse(X0),X0),
inference(forward_demodulation,[],[f185763,f139233]) ).
fof(f186708,plain,
! [X0] : additive_inverse(multiply(X0,X0)) = multiply(X0,additive_inverse(X0)),
inference(forward_demodulation,[],[f186310,f166467]) ).
fof(f187323,plain,
additive_inverse(multiply(c,b)) = multiply(a,multiply(b,additive_inverse(b))),
inference(superposition,[],[f76134,f186708]) ).
fof(f187411,plain,
multiply(c,additive_inverse(b)) = additive_inverse(multiply(c,b)),
inference(forward_demodulation,[],[f187323,f61]) ).
fof(f189417,plain,
! [X0] : additive_identity = multiply(add(a,multiply(c,additive_inverse(b))),multiply(c,X0)),
inference(superposition,[],[f98837,f187411]) ).
fof(f189419,plain,
! [X0] : additive_identity = multiply(add(a,multiply(c,additive_inverse(b))),multiply(additive_inverse(c),X0)),
inference(superposition,[],[f98922,f187411]) ).
fof(f206295,plain,
! [X0] : multiply(additive_inverse(multiply(c,b)),multiply(c,X0)) = multiply(multiply(c,b),multiply(multiply(c,b),multiply(additive_inverse(b),X0))),
inference(superposition,[],[f167229,f96280]) ).
fof(f206677,plain,
! [X0] : multiply(additive_inverse(multiply(c,b)),multiply(c,X0)) = multiply(c,multiply(b,multiply(multiply(c,b),multiply(additive_inverse(b),X0)))),
inference(forward_demodulation,[],[f206295,f9]) ).
fof(f206857,plain,
! [X0] : multiply(additive_inverse(multiply(c,b)),multiply(c,X0)) = multiply(c,multiply(b,multiply(c,multiply(b,multiply(additive_inverse(b),X0))))),
inference(forward_demodulation,[],[f206677,f9]) ).
fof(f206978,plain,
! [X0] : multiply(additive_inverse(multiply(c,b)),multiply(c,X0)) = multiply(c,multiply(b,multiply(additive_inverse(c),X0))),
inference(forward_demodulation,[],[f206857,f95214]) ).
fof(f207075,plain,
! [X0] : multiply(c,multiply(b,multiply(additive_inverse(c),X0))) = multiply(multiply(c,additive_inverse(b)),multiply(c,X0)),
inference(forward_demodulation,[],[f206978,f187411]) ).
fof(f207152,plain,
! [X0] : multiply(c,multiply(b,multiply(additive_inverse(c),X0))) = multiply(c,multiply(additive_inverse(b),multiply(c,X0))),
inference(forward_demodulation,[],[f207075,f9]) ).
fof(f223159,plain,
! [X0,X1] : multiply(X0,X1) = add(additive_inverse(multiply(X0,additive_inverse(X1))),multiply(X0,additive_identity)),
inference(superposition,[],[f7555,f6]) ).
fof(f223183,plain,
! [X0,X1] : multiply(X0,additive_inverse(X1)) = add(additive_inverse(multiply(X0,multiply(additive_inverse(multiply(X1,X1)),additive_inverse(X1)))),multiply(X0,additive_identity)),
inference(superposition,[],[f7555,f169613]) ).
fof(f223433,plain,
multiply(additive_inverse(c),b) = add(additive_inverse(multiply(additive_inverse(c),multiply(a,additive_inverse(c)))),additive_identity),
inference(superposition,[],[f7555,f120469]) ).
fof(f223462,plain,
multiply(c,a) = add(additive_inverse(multiply(c,multiply(b,additive_inverse(c)))),additive_identity),
inference(superposition,[],[f7555,f127343]) ).
fof(f223464,plain,
multiply(c,b) = add(additive_inverse(multiply(c,multiply(a,additive_inverse(c)))),additive_identity),
inference(superposition,[],[f7555,f120332]) ).
fof(f223607,plain,
multiply(c,b) = add(additive_identity,additive_inverse(multiply(c,multiply(a,additive_inverse(c))))),
inference(forward_demodulation,[],[f223464,f8]) ).
fof(f223609,plain,
multiply(c,a) = add(additive_identity,additive_inverse(multiply(c,multiply(b,additive_inverse(c))))),
inference(forward_demodulation,[],[f223462,f8]) ).
fof(f223638,plain,
multiply(additive_inverse(c),b) = add(additive_identity,additive_inverse(multiply(additive_inverse(c),multiply(a,additive_inverse(c))))),
inference(forward_demodulation,[],[f223433,f8]) ).
fof(f223865,plain,
! [X0,X1] : multiply(X0,additive_inverse(X1)) = add(multiply(X0,additive_identity),additive_inverse(multiply(X0,multiply(additive_inverse(multiply(X1,X1)),additive_inverse(X1))))),
inference(forward_demodulation,[],[f223183,f8]) ).
fof(f223886,plain,
! [X0,X1] : multiply(X0,X1) = add(multiply(X0,additive_identity),additive_inverse(multiply(X0,additive_inverse(X1)))),
inference(forward_demodulation,[],[f223159,f8]) ).
fof(f224511,plain,
multiply(c,b) = additive_inverse(multiply(c,multiply(a,additive_inverse(c)))),
inference(forward_demodulation,[],[f223607,f1]) ).
fof(f224513,plain,
multiply(c,a) = additive_inverse(multiply(c,multiply(b,additive_inverse(c)))),
inference(forward_demodulation,[],[f223609,f1]) ).
fof(f224541,plain,
multiply(additive_inverse(c),b) = additive_inverse(multiply(additive_inverse(c),multiply(a,additive_inverse(c)))),
inference(forward_demodulation,[],[f223638,f1]) ).
fof(f224718,plain,
! [X0,X1] : multiply(X0,additive_inverse(X1)) = add(multiply(X0,additive_identity),additive_inverse(multiply(X0,X1))),
inference(forward_demodulation,[],[f223865,f170123]) ).
fof(f224733,plain,
! [X0,X1] : multiply(X0,X1) = add(additive_identity,additive_inverse(multiply(X0,additive_inverse(X1)))),
inference(forward_demodulation,[],[f223886,f35144]) ).
fof(f225231,plain,
multiply(additive_inverse(c),b) = additive_inverse(multiply(c,multiply(a,c))),
inference(forward_demodulation,[],[f224541,f157373]) ).
fof(f225350,plain,
! [X0,X1] : multiply(X0,additive_inverse(X1)) = add(additive_identity,additive_inverse(multiply(X0,X1))),
inference(forward_demodulation,[],[f224718,f35144]) ).
fof(f225363,plain,
! [X0,X1] : multiply(X0,X1) = additive_inverse(multiply(X0,additive_inverse(X1))),
inference(forward_demodulation,[],[f224733,f1]) ).
fof(f225612,plain,
multiply(c,additive_inverse(b)) = additive_inverse(multiply(c,multiply(a,c))),
inference(forward_demodulation,[],[f225231,f164649]) ).
fof(f225706,plain,
! [X0,X1] : additive_inverse(multiply(X0,X1)) = multiply(X0,additive_inverse(X1)),
inference(forward_demodulation,[],[f225350,f1]) ).
fof(f226147,plain,
multiply(additive_inverse(c),multiply(a,c)) = additive_inverse(multiply(c,multiply(a,c))),
inference(superposition,[],[f225363,f167330]) ).
fof(f226171,plain,
multiply(c,multiply(a,c)) = additive_inverse(multiply(c,multiply(a,additive_inverse(c)))),
inference(superposition,[],[f225363,f167369]) ).
fof(f226410,plain,
multiply(c,b) = multiply(c,multiply(a,c)),
inference(forward_demodulation,[],[f226171,f224511]) ).
fof(f226431,plain,
multiply(c,additive_inverse(b)) = multiply(additive_inverse(c),multiply(a,c)),
inference(forward_demodulation,[],[f226147,f225612]) ).
fof(f231019,plain,
! [X2,X0,X1] : multiply(X2,additive_inverse(X1)) = add(multiply(X0,X1),multiply(add(X2,X0),additive_inverse(X1))),
inference(superposition,[],[f11458,f225363]) ).
fof(f231031,plain,
! [X2,X0,X1] : multiply(X1,X2) = add(additive_inverse(multiply(add(additive_inverse(X1),X0),X2)),multiply(X0,X2)),
inference(superposition,[],[f11458,f43]) ).
fof(f231079,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = add(additive_inverse(multiply(multiply(additive_inverse(multiply(X0,X0)),additive_inverse(X0)),X1)),multiply(additive_identity,X1)),
inference(superposition,[],[f11458,f169613]) ).
fof(f231293,plain,
multiply(b,additive_inverse(c)) = add(additive_inverse(multiply(multiply(a,additive_inverse(c)),additive_inverse(c))),additive_identity),
inference(superposition,[],[f11458,f117404]) ).
fof(f231314,plain,
! [X0] : multiply(a,multiply(c,X0)) = add(additive_inverse(multiply(multiply(c,additive_inverse(b)),multiply(c,X0))),additive_identity),
inference(superposition,[],[f11458,f189417]) ).
fof(f231315,plain,
! [X0] : multiply(a,multiply(additive_inverse(c),X0)) = add(additive_inverse(multiply(multiply(c,additive_inverse(b)),multiply(additive_inverse(c),X0))),additive_identity),
inference(superposition,[],[f11458,f189419]) ).
fof(f231321,plain,
! [X0] : multiply(b,multiply(c,X0)) = add(additive_inverse(multiply(multiply(a,additive_inverse(c)),multiply(c,X0))),additive_identity),
inference(superposition,[],[f11458,f116896]) ).
fof(f231326,plain,
multiply(b,a) = add(additive_inverse(multiply(multiply(a,additive_inverse(c)),a)),additive_identity),
inference(superposition,[],[f11458,f116660]) ).
fof(f231348,plain,
multiply(a,c) = add(additive_inverse(multiply(multiply(b,additive_inverse(c)),c)),additive_identity),
inference(superposition,[],[f11458,f126982]) ).
fof(f231525,plain,
multiply(a,c) = add(additive_identity,additive_inverse(multiply(multiply(b,additive_inverse(c)),c))),
inference(forward_demodulation,[],[f231348,f8]) ).
fof(f231547,plain,
multiply(b,a) = add(additive_identity,additive_inverse(multiply(multiply(a,additive_inverse(c)),a))),
inference(forward_demodulation,[],[f231326,f8]) ).
fof(f231552,plain,
! [X0] : multiply(b,multiply(c,X0)) = add(additive_identity,additive_inverse(multiply(multiply(a,additive_inverse(c)),multiply(c,X0)))),
inference(forward_demodulation,[],[f231321,f8]) ).
fof(f231558,plain,
! [X0] : multiply(a,multiply(additive_inverse(c),X0)) = add(additive_identity,additive_inverse(multiply(multiply(c,additive_inverse(b)),multiply(additive_inverse(c),X0)))),
inference(forward_demodulation,[],[f231315,f8]) ).
fof(f231559,plain,
! [X0] : multiply(a,multiply(c,X0)) = add(additive_identity,additive_inverse(multiply(multiply(c,additive_inverse(b)),multiply(c,X0)))),
inference(forward_demodulation,[],[f231314,f8]) ).
fof(f231580,plain,
multiply(b,additive_inverse(c)) = add(additive_identity,additive_inverse(multiply(multiply(a,additive_inverse(c)),additive_inverse(c)))),
inference(forward_demodulation,[],[f231293,f8]) ).
fof(f231791,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = add(multiply(additive_identity,X1),additive_inverse(multiply(multiply(additive_inverse(multiply(X0,X0)),additive_inverse(X0)),X1))),
inference(forward_demodulation,[],[f231079,f8]) ).
fof(f231837,plain,
! [X2,X0,X1] : multiply(X1,X2) = add(multiply(X0,X2),additive_inverse(multiply(add(additive_inverse(X1),X0),X2))),
inference(forward_demodulation,[],[f231031,f8]) ).
fof(f232497,plain,
multiply(a,c) = additive_inverse(multiply(multiply(b,additive_inverse(c)),c)),
inference(forward_demodulation,[],[f231525,f1]) ).
fof(f232519,plain,
multiply(b,a) = additive_inverse(multiply(multiply(a,additive_inverse(c)),a)),
inference(forward_demodulation,[],[f231547,f1]) ).
fof(f232524,plain,
! [X0] : multiply(b,multiply(c,X0)) = additive_inverse(multiply(multiply(a,additive_inverse(c)),multiply(c,X0))),
inference(forward_demodulation,[],[f231552,f1]) ).
fof(f232530,plain,
! [X0] : multiply(a,multiply(additive_inverse(c),X0)) = additive_inverse(multiply(multiply(c,additive_inverse(b)),multiply(additive_inverse(c),X0))),
inference(forward_demodulation,[],[f231558,f1]) ).
fof(f232531,plain,
! [X0] : multiply(a,multiply(c,X0)) = additive_inverse(multiply(multiply(c,additive_inverse(b)),multiply(c,X0))),
inference(forward_demodulation,[],[f231559,f1]) ).
fof(f232552,plain,
multiply(b,additive_inverse(c)) = additive_inverse(multiply(multiply(a,additive_inverse(c)),additive_inverse(c))),
inference(forward_demodulation,[],[f231580,f1]) ).
fof(f232759,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = add(multiply(additive_identity,X1),multiply(multiply(additive_inverse(multiply(X0,X0)),additive_inverse(X0)),additive_inverse(X1))),
inference(forward_demodulation,[],[f231791,f225706]) ).
fof(f232797,plain,
! [X2,X0,X1] : multiply(X1,X2) = add(multiply(X0,X2),multiply(add(additive_inverse(X1),X0),additive_inverse(X2))),
inference(forward_demodulation,[],[f231837,f225706]) ).
fof(f233339,plain,
multiply(a,c) = multiply(multiply(b,additive_inverse(c)),additive_inverse(c)),
inference(forward_demodulation,[],[f232497,f225706]) ).
fof(f233358,plain,
multiply(b,a) = multiply(multiply(a,additive_inverse(c)),additive_inverse(a)),
inference(forward_demodulation,[],[f232519,f225706]) ).
fof(f233363,plain,
! [X0] : multiply(b,multiply(c,X0)) = multiply(multiply(a,additive_inverse(c)),additive_inverse(multiply(c,X0))),
inference(forward_demodulation,[],[f232524,f225706]) ).
fof(f233369,plain,
! [X0] : multiply(a,multiply(additive_inverse(c),X0)) = multiply(multiply(c,additive_inverse(b)),additive_inverse(multiply(additive_inverse(c),X0))),
inference(forward_demodulation,[],[f232530,f225706]) ).
fof(f233370,plain,
! [X0] : multiply(a,multiply(c,X0)) = multiply(multiply(c,additive_inverse(b)),additive_inverse(multiply(c,X0))),
inference(forward_demodulation,[],[f232531,f225706]) ).
fof(f233390,plain,
multiply(b,additive_inverse(c)) = multiply(multiply(a,additive_inverse(c)),c),
inference(forward_demodulation,[],[f232552,f225363]) ).
fof(f233578,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = add(multiply(additive_identity,X1),multiply(additive_inverse(multiply(X0,X0)),multiply(additive_inverse(X0),additive_inverse(X1)))),
inference(forward_demodulation,[],[f232759,f9]) ).
fof(f233610,plain,
! [X2,X1] : multiply(X1,X2) = multiply(additive_inverse(X1),additive_inverse(X2)),
inference(forward_demodulation,[],[f232797,f231019]) ).
fof(f233937,plain,
multiply(a,c) = multiply(b,multiply(additive_inverse(c),additive_inverse(c))),
inference(forward_demodulation,[],[f233339,f9]) ).
fof(f233952,plain,
multiply(b,a) = multiply(a,multiply(additive_inverse(c),additive_inverse(a))),
inference(forward_demodulation,[],[f233358,f9]) ).
fof(f233956,plain,
! [X0] : multiply(b,multiply(c,X0)) = multiply(a,multiply(additive_inverse(c),additive_inverse(multiply(c,X0)))),
inference(forward_demodulation,[],[f233363,f9]) ).
fof(f233962,plain,
! [X0] : multiply(a,multiply(additive_inverse(c),X0)) = multiply(c,multiply(additive_inverse(b),additive_inverse(multiply(additive_inverse(c),X0)))),
inference(forward_demodulation,[],[f233369,f9]) ).
fof(f233963,plain,
! [X0] : multiply(a,multiply(c,X0)) = multiply(c,multiply(additive_inverse(b),additive_inverse(multiply(c,X0)))),
inference(forward_demodulation,[],[f233370,f9]) ).
fof(f233980,plain,
multiply(b,additive_inverse(c)) = multiply(a,multiply(additive_inverse(c),c)),
inference(forward_demodulation,[],[f233390,f9]) ).
fof(f234138,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = add(multiply(additive_identity,X1),multiply(X0,additive_inverse(X1))),
inference(forward_demodulation,[],[f233578,f170434]) ).
fof(f234291,plain,
multiply(a,c) = multiply(b,multiply(c,c)),
inference(forward_demodulation,[],[f233937,f233610]) ).
fof(f234302,plain,
multiply(b,a) = multiply(a,multiply(c,a)),
inference(forward_demodulation,[],[f233952,f233610]) ).
fof(f234306,plain,
! [X0] : multiply(b,multiply(c,X0)) = multiply(a,multiply(c,multiply(c,X0))),
inference(forward_demodulation,[],[f233956,f233610]) ).
fof(f234312,plain,
! [X0] : multiply(a,multiply(additive_inverse(c),X0)) = multiply(c,multiply(b,multiply(additive_inverse(c),X0))),
inference(forward_demodulation,[],[f233962,f233610]) ).
fof(f234313,plain,
! [X0] : multiply(a,multiply(c,X0)) = multiply(c,multiply(b,multiply(c,X0))),
inference(forward_demodulation,[],[f233963,f233610]) ).
fof(f234328,plain,
multiply(b,additive_inverse(c)) = multiply(a,multiply(c,additive_inverse(c))),
inference(forward_demodulation,[],[f233980,f166467]) ).
fof(f234463,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = add(additive_identity,multiply(X0,additive_inverse(X1))),
inference(forward_demodulation,[],[f234138,f37271]) ).
fof(f234650,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = multiply(X0,additive_inverse(X1)),
inference(forward_demodulation,[],[f234463,f1]) ).
fof(f238300,plain,
multiply(c,multiply(c,c)) = multiply(c,multiply(multiply(c,c),multiply(b,multiply(multiply(c,c),multiply(a,c))))),
inference(superposition,[],[f5039,f234291]) ).
fof(f238317,plain,
multiply(additive_inverse(c),multiply(a,c)) = multiply(c,multiply(additive_inverse(b),multiply(c,c))),
inference(superposition,[],[f168199,f234291]) ).
fof(f238377,plain,
multiply(additive_inverse(c),multiply(a,c)) = multiply(c,multiply(b,multiply(additive_inverse(c),c))),
inference(forward_demodulation,[],[f238317,f207152]) ).
fof(f238394,plain,
multiply(c,multiply(c,c)) = multiply(c,multiply(c,multiply(c,multiply(b,multiply(multiply(c,c),multiply(a,c)))))),
inference(forward_demodulation,[],[f238300,f9]) ).
fof(f238423,plain,
multiply(a,multiply(additive_inverse(c),c)) = multiply(additive_inverse(c),multiply(a,c)),
inference(forward_demodulation,[],[f238377,f234312]) ).
fof(f238439,plain,
multiply(c,multiply(c,c)) = multiply(c,multiply(b,multiply(multiply(c,c),multiply(a,c)))),
inference(forward_demodulation,[],[f238394,f71]) ).
fof(f238455,plain,
multiply(c,additive_inverse(b)) = multiply(a,multiply(additive_inverse(c),c)),
inference(forward_demodulation,[],[f238423,f226431]) ).
fof(f238463,plain,
multiply(c,multiply(c,c)) = multiply(c,multiply(b,multiply(c,multiply(c,multiply(a,c))))),
inference(forward_demodulation,[],[f238439,f9]) ).
fof(f238471,plain,
multiply(c,additive_inverse(b)) = multiply(a,multiply(c,additive_inverse(c))),
inference(forward_demodulation,[],[f238455,f234650]) ).
fof(f238477,plain,
multiply(c,multiply(c,c)) = multiply(a,multiply(c,multiply(c,multiply(a,c)))),
inference(forward_demodulation,[],[f238463,f234313]) ).
fof(f238484,plain,
multiply(b,additive_inverse(c)) = multiply(c,additive_inverse(b)),
inference(forward_demodulation,[],[f238471,f234328]) ).
fof(f238486,plain,
multiply(c,multiply(c,c)) = multiply(b,multiply(c,multiply(a,c))),
inference(forward_demodulation,[],[f238477,f234306]) ).
fof(f238492,plain,
multiply(c,multiply(c,c)) = multiply(b,multiply(c,b)),
inference(forward_demodulation,[],[f238486,f226410]) ).
fof(f238494,plain,
c = multiply(b,multiply(c,b)),
inference(forward_demodulation,[],[f238492,f12]) ).
fof(f238558,plain,
additive_inverse(c) = multiply(b,additive_inverse(multiply(c,b))),
inference(superposition,[],[f225706,f238494]) ).
fof(f238559,plain,
additive_inverse(c) = multiply(b,multiply(c,additive_inverse(b))),
inference(forward_demodulation,[],[f238558,f225706]) ).
fof(f238604,plain,
additive_inverse(c) = multiply(b,multiply(b,additive_inverse(c))),
inference(forward_demodulation,[],[f238559,f238484]) ).
fof(f243831,plain,
multiply(a,additive_inverse(additive_inverse(c))) = additive_inverse(multiply(c,multiply(b,additive_inverse(c)))),
inference(superposition,[],[f76134,f238604]) ).
fof(f243888,plain,
multiply(c,a) = multiply(a,additive_inverse(additive_inverse(c))),
inference(forward_demodulation,[],[f243831,f224513]) ).
fof(f243913,plain,
multiply(a,c) = multiply(c,a),
inference(forward_demodulation,[],[f243888,f59]) ).
fof(f243971,plain,
multiply(b,a) = multiply(a,multiply(a,c)),
inference(superposition,[],[f234302,f243913]) ).
fof(f244097,plain,
c = multiply(b,a),
inference(forward_demodulation,[],[f243971,f975]) ).
fof(f244142,plain,
$false,
inference(forward_subsumption_resolution,[],[f244097,f15]) ).
%------------------------------------------------------------------------------
%----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/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.16/0.41 % Computer : n003.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Sun Sep 27 23:00:11 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.16/0.44 Running first-order model finding
% 0.16/0.44 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
% 15.92/2.71 % (1024242)Will run a generic schedule for satisfiability detection.
% 15.92/2.71 % (1024250)dis+10_1_sil=32000:sp=arity:random_seed=3990276564:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.92/2.71 % (1024248)% WARNING: option uhcvi not known.
% 15.92/2.71 % (1024247)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1388232721_2999 on theBenchmark for (2999ds/0Mi)
% 15.92/2.71 % (1024248)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3598806547:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.92/2.71 % (1024249)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1365447006:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.92/2.71 % (1024251)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2675181985:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.92/2.71 % TRYING [1]
% 15.92/2.71 % TRYING [2]
% 15.92/2.71 % TRYING [3]
% 15.92/2.71 % TRYING [4]
% 15.92/2.71 % (1024253)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=344876409:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.92/2.71 % (1024252)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2776909537:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.92/2.71 % (1024250)Instruction limit reached!
% 15.92/2.71 % (1024250)------------------------------
% 15.92/2.71 % (1024250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.92/2.71 % (1024250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/2.71 % (1024250)CaDiCaL version: 2.1.3
% 15.92/2.71 % (1024250)Termination reason: Instruction limit
% 15.92/2.71 % (1024250)Termination phase: Saturation
% 15.92/2.71 % (1024250)Time elapsed: 0.031 s
% 15.92/2.71 % (1024250)Peak memory usage: 12 MB
% 15.92/2.71 % (1024250)Instructions burned: 106 (million)
% 15.92/2.71 % TRYING [5]
% 15.92/2.71 % (1024261)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3937446147:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.92/2.71 % TRYING [1]
% 15.92/2.71 % TRYING [2]
% 15.92/2.71 % TRYING [3]
% 15.92/2.71 % TRYING [4]
% 15.92/2.71 % TRYING [5]
% 15.92/2.71 % TRYING [6]
% 15.92/2.71 % (1024251)Instruction limit reached!
% 15.92/2.71 % (1024251)------------------------------
% 15.92/2.71 % (1024251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.92/2.71 % (1024251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/2.71 % (1024251)CaDiCaL version: 2.1.3
% 15.92/2.71 % (1024251)Termination reason: Instruction limit
% 15.92/2.71 % (1024251)Termination phase: Saturation
% 15.92/2.71 % (1024251)Time elapsed: 0.080 s
% 15.92/2.71 % (1024251)Peak memory usage: 12 MB
% 15.92/2.71 % (1024251)Instructions burned: 116 (million)
% 15.92/2.71 % (1024252)Instruction limit reached!
% 15.92/2.71 % (1024252)------------------------------
% 15.92/2.71 % (1024252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.92/2.71 % (1024252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/2.71 % (1024252)CaDiCaL version: 2.1.3
% 15.92/2.71 % (1024252)Termination reason: Instruction limit
% 15.92/2.71 % (1024252)Termination phase: Saturation
% 15.92/2.71 % (1024252)Time elapsed: 0.069 s
% 15.92/2.71 % (1024252)Peak memory usage: 12 MB
% 15.92/2.71 % (1024252)Instructions burned: 132 (million)
% 15.92/2.71 % TRYING [6]
% 15.92/2.71 % (1024265)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=800204351:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.92/2.71 % (1024266)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=1771007153:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.92/2.71 % (1024253)Instruction limit reached!
% 15.92/2.71 % (1024253)------------------------------
% 15.92/2.71 % (1024253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.92/2.71 % (1024253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/2.71 % (1024253)CaDiCaL version: 2.1.3
% 15.92/2.71 % (1024253)Termination reason: Instruction limit
% 15.92/2.71 % (1024253)Termination phase: Saturation
% 15.92/2.71 % (1024253)Time elapsed: 0.154 s
% 15.92/2.71 % (1024253)Peak memory usage: 12 MB
% 15.92/2.71 % (1024253)Instructions burned: 160 (million)
% 15.92/2.71 % (1024265)Instruction limit reached!
% 15.92/2.71 % (1024265)------------------------------
% 15.92/2.71 % (1024265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.92/2.71 % (1024265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.54/7.36 % (1024265)CaDiCaL version: 2.1.3
% 48.54/7.36 % (1024265)Termination reason: Instruction limit
% 48.54/7.36 % (1024265)Termination phase: Saturation
% 48.54/7.36 % (1024265)Time elapsed: 0.085 s
% 48.54/7.36 % (1024265)Peak memory usage: 13 MB
% 48.54/7.36 % (1024265)Instructions burned: 132 (million)
% 48.54/7.36 % (1024269)ott-21_1_sil=16000:fs=off:random_seed=1583101154:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 48.54/7.36 % (1024270)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2017017553:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 48.54/7.36 % (1024261)Instruction limit reached!
% 48.54/7.36 % (1024261)------------------------------
% 48.54/7.36 % (1024261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.54/7.36 % (1024261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.54/7.36 % (1024261)CaDiCaL version: 2.1.3
% 48.54/7.36 % (1024261)Termination reason: Instruction limit
% 48.54/7.36 % (1024261)Termination phase: Finite model building SAT solving
% 48.54/7.36 % (1024261)Time elapsed: 0.188 s
% 48.54/7.36 % (1024261)Peak memory usage: 29 MB
% 48.54/7.36 % (1024261)Instructions burned: 715 (million)
% 48.54/7.36 % (1024273)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3986526474:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 48.54/7.36 % TRYING [1]
% 48.54/7.36 % TRYING [2]
% 48.54/7.36 % TRYING [3]
% 48.54/7.36 % TRYING [4]
% 48.54/7.36 % TRYING [5]
% 48.54/7.36 % (1024269)Instruction limit reached!
% 48.54/7.36 % (1024269)------------------------------
% 48.54/7.36 % (1024269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.54/7.36 % (1024269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.54/7.36 % (1024269)CaDiCaL version: 2.1.3
% 48.54/7.36 % (1024269)Termination reason: Instruction limit
% 48.54/7.36 % (1024269)Termination phase: Saturation
% 48.54/7.36 % (1024269)Time elapsed: 0.077 s
% 48.54/7.36 % (1024269)Peak memory usage: 11 MB
% 48.54/7.36 % (1024269)Instructions burned: 181 (million)
% 48.54/7.36 % (1024275)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2327664262:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 48.54/7.36 % TRYING [6]
% 48.54/7.36 % (1024273)Instruction limit reached!
% 48.54/7.36 % (1024273)------------------------------
% 48.54/7.36 % (1024273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.54/7.36 % (1024273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.54/7.36 % (1024273)CaDiCaL version: 2.1.3
% 48.54/7.36 % (1024273)Termination reason: Instruction limit
% 48.54/7.36 % (1024273)Termination phase: Finite model building SAT solving
% 48.54/7.36 % (1024273)Time elapsed: 0.172 s
% 48.54/7.36 % (1024273)Peak memory usage: 23 MB
% 48.54/7.36 % (1024273)Instructions burned: 867 (million)
% 48.54/7.36 % (1024280)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3627151262:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 48.54/7.36 % (1024270)Instruction limit reached!
% 48.54/7.36 % (1024270)------------------------------
% 48.54/7.36 % (1024270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.54/7.36 % (1024270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.54/7.36 % (1024270)CaDiCaL version: 2.1.3
% 48.54/7.36 % (1024270)Termination reason: Instruction limit
% 48.54/7.36 % (1024270)Termination phase: Saturation
% 48.54/7.36 % (1024270)Time elapsed: 0.255 s
% 48.54/7.36 % (1024270)Peak memory usage: 15 MB
% 48.54/7.36 % (1024270)Instructions burned: 479 (million)
% 48.54/7.36 % (1024266)Instruction limit reached!
% 48.54/7.36 % (1024266)------------------------------
% 48.54/7.36 % (1024266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.54/7.36 % (1024266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.54/7.36 % (1024266)CaDiCaL version: 2.1.3
% 48.54/7.36 % (1024266)Termination reason: Instruction limit
% 48.54/7.36 % (1024266)Termination phase: Saturation
% 48.54/7.36 % (1024266)Time elapsed: 0.360 s
% 48.54/7.36 % (1024266)Peak memory usage: 18 MB
% 48.54/7.36 % (1024266)Instructions burned: 685 (million)
% 48.54/7.36 % (1024282)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=1231125497:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 48.54/7.36 % (1024283)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=875536958:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 48.54/7.36 % TRYING [14]
% 48.54/7.36 % TRYING [7]
% 92.52/13.55 % (1024280)Instruction limit reached!
% 92.52/13.55 % (1024280)------------------------------
% 92.52/13.55 % (1024280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.52/13.55 % (1024280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.52/13.55 % (1024280)CaDiCaL version: 2.1.3
% 92.52/13.55 % (1024280)Termination reason: Instruction limit
% 92.52/13.55 % (1024280)Termination phase: Finite model building constraint generation
% 92.52/13.55 % (1024280)Time elapsed: 0.189 s
% 92.52/13.55 % (1024280)Peak memory usage: 80 MB
% 92.52/13.55 % (1024280)Instructions burned: 891 (million)
% 92.52/13.55 % (1024317)fmb+10_1_sil=64000:random_seed=1516966215:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 92.52/13.55 % TRYING [1]
% 92.52/13.55 % TRYING [2]
% 92.52/13.55 % TRYING [3]
% 92.52/13.55 % TRYING [4]
% 92.52/13.55 % TRYING [5]
% 92.52/13.55 % TRYING [6]
% 92.52/13.55 % (1024275)Instruction limit reached!
% 92.52/13.55 % (1024275)------------------------------
% 92.52/13.55 % (1024275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.52/13.55 % (1024275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.52/13.55 % (1024275)CaDiCaL version: 2.1.3
% 92.52/13.55 % (1024275)Termination reason: Instruction limit
% 92.52/13.55 % (1024275)Termination phase: Saturation
% 92.52/13.55 % (1024275)Time elapsed: 0.571 s
% 92.52/13.55 % (1024275)Peak memory usage: 16 MB
% 92.52/13.55 % (1024275)Instructions burned: 1180 (million)
% 92.52/13.55 % (1024282)Instruction limit reached!
% 92.52/13.55 % (1024282)------------------------------
% 92.52/13.55 % (1024282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.52/13.55 % (1024282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.52/13.55 % (1024282)CaDiCaL version: 2.1.3
% 92.52/13.55 % (1024282)Termination reason: Instruction limit
% 92.52/13.55 % (1024282)Termination phase: Saturation
% 92.52/13.55 % (1024282)Time elapsed: 0.387 s
% 92.52/13.55 % (1024282)Peak memory usage: 17 MB
% 92.52/13.55 % (1024282)Instructions burned: 692 (million)
% 92.52/13.55 % (1024406)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=959132647:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 92.52/13.55 % TRYING [20]
% 92.52/13.55 % (1024411)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3483102672:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 92.52/13.55 % TRYING [8]
% 92.52/13.55 % (1024283)Instruction limit reached!
% 92.52/13.55 % (1024283)------------------------------
% 92.52/13.55 % (1024283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.52/13.55 % (1024283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.52/13.55 % (1024283)CaDiCaL version: 2.1.3
% 92.52/13.55 % (1024283)Termination reason: Instruction limit
% 92.52/13.55 % (1024283)Termination phase: Saturation
% 92.52/13.55 % (1024283)Time elapsed: 0.463 s
% 92.52/13.55 % (1024283)Peak memory usage: 18 MB
% 92.52/13.55 % (1024283)Instructions burned: 880 (million)
% 92.52/13.55 % TRYING [7]
% 92.52/13.55 % (1024444)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2539092726:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 92.52/13.55 % (1024411)Instruction limit reached!
% 92.52/13.55 % (1024411)------------------------------
% 92.52/13.55 % (1024411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.52/13.55 % (1024411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.52/13.55 % (1024411)CaDiCaL version: 2.1.3
% 92.52/13.55 % (1024411)Termination reason: Instruction limit
% 92.52/13.55 % (1024411)Termination phase: Finite model building constraint generation
% 92.52/13.55 % (1024411)Time elapsed: 0.348 s
% 92.52/13.55 % (1024411)Peak memory usage: 64 MB
% 92.52/13.55 % (1024411)Instructions burned: 920 (million)
% 92.52/13.55 % (1024446)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=681491491:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 92.52/13.55 % TRYING [8]
% 92.52/13.55 % TRYING [8]
% 92.52/13.55 % (1024446)Instruction limit reached!
% 92.52/13.55 % (1024446)------------------------------
% 92.52/13.55 % (1024446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.52/13.55 % (1024446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.52/13.55 % (1024446)CaDiCaL version: 2.1.3
% 92.52/13.55 % (1024446)Termination reason: Instruction limit
% 92.52/13.55 % (1024446)Termination phase: Saturation
% 92.52/13.55 % (1024446)Time elapsed: 0.931 s
% 92.52/13.55 % (1024446)Peak memory usage: 35 MB
% 92.52/13.55 % (1024446)Instructions burned: 1473 (million)
% 92.52/13.55 % (1024448)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4125024293:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 264.91/37.83 % TRYING [77]
% 264.91/37.83 % (1024444)Instruction limit reached!
% 264.91/37.83 % (1024444)------------------------------
% 264.91/37.83 % (1024444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 264.91/37.83 % (1024444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.91/37.83 % (1024444)CaDiCaL version: 2.1.3
% 264.91/37.83 % (1024444)Termination reason: Instruction limit
% 264.91/37.83 % (1024444)Termination phase: Saturation
% 264.91/37.83 % (1024444)Time elapsed: 2.755 s
% 264.91/37.83 % (1024444)Peak memory usage: 51 MB
% 264.91/37.83 % (1024444)Instructions burned: 5132 (million)
% 264.91/37.83 % (1024450)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1825095225:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 264.91/37.83 % TRYING [16]
% 264.91/37.83 % (1024406)Instruction limit reached!
% 264.91/37.83 % (1024406)------------------------------
% 264.91/37.83 % (1024406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 264.91/37.83 % (1024406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.91/37.83 % (1024406)CaDiCaL version: 2.1.3
% 264.91/37.83 % (1024406)Termination reason: Instruction limit
% 264.91/37.83 % (1024406)Termination phase: Finite model building constraint generation
% 264.91/37.83 % (1024406)Time elapsed: 3.464 s
% 264.91/37.83 % (1024406)Peak memory usage: 665 MB
% 264.91/37.83 % (1024406)Instructions burned: 9516 (million)
% 264.91/37.83 % (1024452)ott-2_1_sil=16000:newcnf=on:random_seed=2831224156:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 264.91/37.83 % (1024450)Instruction limit reached!
% 264.91/37.83 % (1024450)------------------------------
% 264.91/37.83 % (1024450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 264.91/37.83 % (1024450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.91/37.83 % (1024450)CaDiCaL version: 2.1.3
% 264.91/37.83 % (1024450)Termination reason: Instruction limit
% 264.91/37.83 % (1024450)Termination phase: Finite model building constraint generation
% 264.91/37.83 % (1024450)Time elapsed: 0.731 s
% 264.91/37.83 % (1024450)Peak memory usage: 133 MB
% 264.91/37.83 % (1024450)Instructions burned: 2176 (million)
% 264.91/37.83 % (1024454)ott+10_1_sil=32000:tgt=ground:random_seed=3634884836:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 264.91/37.83 % (1024448)Instruction limit reached!
% 264.91/37.83 % (1024448)------------------------------
% 264.91/37.83 % (1024448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 264.91/37.83 % (1024448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.91/37.83 % (1024448)CaDiCaL version: 2.1.3
% 264.91/37.83 % (1024448)Termination reason: Instruction limit
% 264.91/37.83 % (1024448)Termination phase: Finite model building constraint generation
% 264.91/37.83 % (1024448)Time elapsed: 2.317 s
% 264.91/37.83 % (1024448)Peak memory usage: 419 MB
% 264.91/37.83 % (1024448)Instructions burned: 6326 (million)
% 264.91/37.83 % (1024456)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3851270796:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 264.91/37.83 % TRYING [1]
% 264.91/37.83 % TRYING [2]
% 264.91/37.83 % TRYING [3]
% 264.91/37.83 % TRYING [4]
% 264.91/37.83 % TRYING [5]
% 264.91/37.83 % TRYING [6]
% 264.91/37.83 % (1024452)Instruction limit reached!
% 264.91/37.83 % (1024452)------------------------------
% 264.91/37.83 % (1024452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 264.91/37.83 % (1024452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.91/37.83 % (1024452)CaDiCaL version: 2.1.3
% 264.91/37.83 % (1024452)Termination reason: Instruction limit
% 264.91/37.83 % (1024452)Termination phase: Saturation
% 264.91/37.83 % (1024452)Time elapsed: 0.526 s
% 264.91/37.83 % (1024452)Peak memory usage: 20 MB
% 264.91/37.83 % (1024452)Instructions burned: 869 (million)
% 264.91/37.83 % (1024458)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1459299958:i=3512:aac=none_2949 on theBenchmark for (2949ds/3512Mi)
% 264.91/37.83 % TRYING [7]
% 264.91/37.83 % TRYING [8]
% 264.91/37.83 % TRYING [9]
% 264.91/37.83 % (1024458)Instruction limit reached!
% 264.91/37.83 % (1024458)------------------------------
% 264.91/37.83 % (1024458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 264.91/37.83 % (1024458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.91/37.83 % (1024458)CaDiCaL version: 2.1.3
% 264.91/37.83 % (1024458)Termination reason: Instruction limit
% 264.91/37.83 % (1024458)Termination phase: Saturation
% 264.91/37.83 % (1024458)Time elapsed: 1.872 s
% 264.91/37.83 % (1024458)Peak memory usage: 40 MB
% 264.91/37.83 % (1024458)Instructions burned: 3513 (million)
% 131.59/41.45 % (1024317)Instruction limit reached!
% 131.59/41.45 % (1024317)------------------------------
% 131.59/41.45 % (1024317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1024317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1024317)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1024317)Termination reason: Instruction limit
% 131.59/41.45 % (1024317)Termination phase: Finite model building constraint generation
% 131.59/41.45 % (1024317)Time elapsed: 6.252 s
% 131.59/41.45 % (1024317)Peak memory usage: 82 MB
% 131.59/41.45 % (1024317)Instructions burned: 22062 (million)
% 131.59/41.45 % (1024461)ott+11_1_sil=16000:gs=on:random_seed=1440941378:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2930 on theBenchmark for (2930ds/2251Mi)
% 131.59/41.45 % (1024460)dis+21_1_sil=32000:sas=cadical:random_seed=420194491:i=3773:amm=off_2930 on theBenchmark for (2930ds/3773Mi)
% 131.59/41.45 % (1024461)Instruction limit reached!
% 131.59/41.45 % (1024461)------------------------------
% 131.59/41.45 % (1024461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1024461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1024461)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1024461)Termination reason: Instruction limit
% 131.59/41.45 % (1024461)Termination phase: Saturation
% 131.59/41.45 % (1024461)Time elapsed: 0.694 s
% 131.59/41.45 % (1024461)Peak memory usage: 28 MB
% 131.59/41.45 % (1024461)Instructions burned: 2254 (million)
% 131.59/41.45 % (1024464)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1111716419:fmbsr=1.6:i=67534_2923 on theBenchmark for (2923ds/67534Mi)
% 131.59/41.45 % TRYING [7]
% 131.59/41.45 % (1024454)Instruction limit reached!
% 131.59/41.45 % (1024454)------------------------------
% 131.59/41.45 % (1024454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1024454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1024454)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1024454)Termination reason: Instruction limit
% 131.59/41.45 % (1024454)Termination phase: Saturation
% 131.59/41.45 % (1024454)Time elapsed: 3.152 s
% 131.59/41.45 % (1024454)Peak memory usage: 52 MB
% 131.59/41.45 % (1024454)Instructions burned: 5114 (million)
% 131.59/41.45 % (1024466)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1910847153:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2922 on theBenchmark for (2922ds/4591Mi)
% 131.59/41.45 % (1024460)Instruction limit reached!
% 131.59/41.45 % (1024460)------------------------------
% 131.59/41.45 % (1024460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1024460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1024460)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1024460)Termination reason: Instruction limit
% 131.59/41.45 % (1024460)Termination phase: Saturation
% 131.59/41.45 % (1024460)Time elapsed: 2.019 s
% 131.59/41.45 % (1024460)Peak memory usage: 42 MB
% 131.59/41.45 % (1024460)Instructions burned: 3774 (million)
% 131.59/41.45 % (1024468)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1897477754:i=29340_2910 on theBenchmark for (2910ds/29340Mi)
% 131.59/41.45 % TRYING [8]
% 131.59/41.45 % (1024466)Instruction limit reached!
% 131.59/41.45 % (1024466)------------------------------
% 131.59/41.45 % (1024466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1024466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1024466)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1024466)Termination reason: Instruction limit
% 131.59/41.45 % (1024466)Termination phase: Saturation
% 131.59/41.45 % (1024466)Time elapsed: 2.528 s
% 131.59/41.45 % (1024466)Peak memory usage: 72 MB
% 131.59/41.45 % (1024466)Instructions burned: 4592 (million)
% 131.59/41.45 % (1024470)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=687299333:i=5211_2897 on theBenchmark for (2897ds/5211Mi)
% 131.59/41.45 % TRYING [9]
% 131.59/41.45 % (1024470)Instruction limit reached!
% 131.59/41.45 % (1024470)------------------------------
% 131.59/41.45 % (1024470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1024470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1024470)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1024470)Termination reason: Instruction limit
% 131.59/41.45 % (1024470)Termination phase: Saturation
% 131.59/41.45 % (1024470)Time elapsed: 2.804 s
% 131.59/41.45 % (1024470)Peak memory usage: 50 MB
% 131.59/41.45 % (1024470)Instructions burned: 5212 (million)
% 131.59/41.45 % (1024472)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2034817722:i=5497:nm=2_2868 on theBenchmark for (2868ds/5497Mi)
% 131.59/41.45 % TRYING [17]
% 131.59/41.45 % (1024472)Instruction limit reached!
% 131.59/41.45 % (1024472)------------------------------
% 131.59/41.45 % (1024472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1024472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1024472)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1024472)Termination reason: Instruction limit
% 131.59/41.45 % (1024472)Termination phase: Finite model building constraint generation
% 131.59/41.45 % (1024472)Time elapsed: 1.973 s
% 131.59/41.45 % (1024472)Peak memory usage: 388 MB
% 131.59/41.45 % (1024472)Instructions burned: 5500 (million)
% 131.59/41.45 % (1024710)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2163625241:fmbsr=2:i=46332_2848 on theBenchmark for (2848ds/46332Mi)
% 131.59/41.45 % TRYING [15]
% 131.59/41.45 % TRYING [9]
% 131.59/41.45 % TRYING [9]
% 131.59/41.45 % (1024468)Instruction limit reached!
% 131.59/41.45 % (1024468)------------------------------
% 131.59/41.45 % (1024468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1024468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1024468)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1024468)Termination reason: Instruction limit
% 131.59/41.45 % (1024468)Termination phase: Saturation
% 131.59/41.45 % (1024468)Time elapsed: 14.434 s
% 131.59/41.45 % (1024468)Peak memory usage: 73 MB
% 131.59/41.45 % (1024468)Instructions burned: 29341 (million)
% 131.59/41.45 % (1024882)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1691331724:i=14071_2765 on theBenchmark for (2765ds/14071Mi)
% 131.59/41.45 % TRYING [12]
% 131.59/41.45 % (1024249)Instruction limit reached!
% 131.59/41.45 % (1024249)------------------------------
% 131.59/41.45 % (1024249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1024249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1024249)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1024249)Termination reason: Instruction limit
% 131.59/41.45 % (1024249)Termination phase: Saturation
% 131.59/41.45 % (1024249)Time elapsed: 31.512 s
% 131.59/41.45 % (1024249)Peak memory usage: 244 MB
% 131.59/41.45 % (1024249)Instructions burned: 88027 (million)
% 131.59/41.45 % (1025294)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4126203425:i=22565:add=on:rawr=on_2684 on theBenchmark for (2684ds/22565Mi)
% 131.59/41.45 % (1024882)Instruction limit reached!
% 131.59/41.45 % (1024882)------------------------------
% 131.59/41.45 % (1024882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1024882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1024882)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1024882)Termination reason: Instruction limit
% 131.59/41.45 % (1024882)Termination phase: Finite model building SAT solving
% 131.59/41.45 % (1024882)Time elapsed: 9.387 s
% 131.59/41.45 % (1024882)Peak memory usage: 685 MB
% 131.59/41.45 % (1024882)Instructions burned: 14073 (million)
% 131.59/41.45 % (1025297)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1229912509:i=8173:av=off_2670 on theBenchmark for (2670ds/8173Mi)
% 131.59/41.45 % (1024464)Instruction limit reached!
% 131.59/41.45 % (1024464)------------------------------
% 131.59/41.45 % (1024464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1024464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1024464)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1024464)Termination reason: Instruction limit
% 131.59/41.45 % (1024464)Termination phase: Finite model building SAT solving
% 131.59/41.45 % (1024464)Time elapsed: 27.014 s
% 131.59/41.45 % (1024464)Peak memory usage: 126 MB
% 131.59/41.45 % (1024464)Instructions burned: 67535 (million)
% 131.59/41.45 % (1025299)dis+10_16:1_sil=16000:random_seed=3264881895:i=9155:fsr=off_2653 on theBenchmark for (2653ds/9155Mi)
% 131.59/41.45 % (1025299)Instruction limit reached!
% 131.59/41.45 % (1025299)------------------------------
% 131.59/41.45 % (1025299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1025299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1025299)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1025299)Termination reason: Instruction limit
% 131.59/41.45 % (1025299)Termination phase: Saturation
% 131.59/41.45 % (1025299)Time elapsed: 2.704 s
% 131.59/41.45 % (1025299)Peak memory usage: 69 MB
% 131.59/41.45 % (1025299)Instructions burned: 9156 (million)
% 131.59/41.45 % (1025301)ott-3_8_sil=64000:random_seed=865172031:i=20139:bs=on_2626 on theBenchmark for (2626ds/20139Mi)
% 131.59/41.45 % (1025297)Instruction limit reached!
% 131.59/41.45 % (1025297)------------------------------
% 131.59/41.45 % (1025297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.45 % (1025297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.45 % (1025297)CaDiCaL version: 2.1.3
% 131.59/41.45 % (1025297)Termination reason: Instruction limit
% 131.59/41.45 % (1025297)Termination phase: Saturation
% 131.59/41.45 % (1025297)Time elapsed: 4.489 s
% 131.59/41.45 % (1025297)Peak memory usage: 67 MB
% 131.59/41.45 % (1025297)Instructions burned: 8174 (million)
% 131.59/41.45 % (1025303)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3776279602:fmbsr=2:i=32576_2625 on theBenchmark for (2625ds/32576Mi)
% 131.59/41.45 % TRYING [9]
% 131.59/41.45 % (1025301) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1024242-1025301"...
% 131.59/41.45 % (1025301)...printing done.
% 131.59/41.45 % (1025301)Refutation found. Thanks to Tanya!
% 131.59/41.45 % SZS status Unsatisfiable for theBenchmark
% 131.59/41.45 % SZS output start Proof for theBenchmark
% See solution above
% 131.59/41.46 % (1025301)------------------------------
% 131.59/41.46 % (1025301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.59/41.46 % (1025301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.59/41.46 % (1025301)CaDiCaL version: 2.1.3
% 131.59/41.46 % (1025301)Termination reason: Refutation
% 131.59/41.46 % (1025301)Time elapsed: 3.287 s
% 131.59/41.46 % (1025301)Peak memory usage: 82 MB
% 131.59/41.46 % (1025301)Instructions burned: 9145 (million)
% 131.59/41.46 % (1024242)Success in time 41.005 s
% 131.59/41.46 % Vampire exiting
%------------------------------------------------------------------------------