%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP701-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:15:58 AM UTC 2026
% Result : Unsatisfiable 47.05s 7.57s
% Output : Refutation 47.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 117
% Number of leaves : 11
% Syntax : Number of formulae : 393 ( 393 unt; 0 def)
% Number of atoms : 393 ( 392 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 760 ( 760 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c01) ).
fof(f2,axiom,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c04) ).
fof(f5,axiom,
! [X0] : mult(X0,unit) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c05) ).
fof(f6,axiom,
! [X0] : mult(unit,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c06) ).
fof(f7,axiom,
! [X2,X0,X1] : mult(mult(mult(X0,X1),X0),mult(X0,X2)) = mult(X0,mult(mult(mult(X1,X0),X0),X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c07) ).
fof(f8,axiom,
! [X2,X0,X1] : mult(mult(X0,X1),mult(X1,mult(X2,X1))) = mult(mult(X0,mult(X1,mult(X1,X2))),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c08) ).
fof(f9,axiom,
! [X0] : mult(X0,i(X0)) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c09) ).
fof(f10,plain,
! [X0] : unit = mult(X0,i(X0)),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X0] : mult(i(X0),X0) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c10) ).
fof(f12,plain,
! [X0] : unit = mult(i(X0),X0),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
mult(a,i(mult(b,a))) != i(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f29,plain,
! [X0,X1] : mult(mult(X0,mult(X0,X1)),X0) = mult(mult(unit,X0),mult(X0,mult(X1,X0))),
inference(superposition,[],[f8,f6]) ).
fof(f30,plain,
! [X0,X1] : mult(mult(X0,mult(X0,X1)),X0) = mult(X0,mult(X0,mult(X1,X0))),
inference(forward_demodulation,[],[f29,f6]) ).
fof(f47,plain,
! [X0,X1] : mult(X0,mult(mult(mult(X1,X0),X0),i(X0))) = mult(mult(mult(X0,X1),X0),unit),
inference(superposition,[],[f7,f10]) ).
fof(f53,plain,
! [X0,X1] : mult(mult(X0,X1),X0) = mult(X0,mult(mult(mult(X1,X0),X0),i(X0))),
inference(forward_demodulation,[],[f47,f5]) ).
fof(f58,plain,
! [X2,X0,X1] : mult(X1,mult(mult(mult(ld(X1,X0),X1),X1),X2)) = mult(mult(X0,X1),mult(X1,X2)),
inference(superposition,[],[f7,f1]) ).
fof(f59,plain,
! [X2,X0,X1] : mult(mult(X1,X2),mult(X2,mult(ld(X2,X0),X2))) = mult(mult(X1,mult(X2,X0)),X2),
inference(superposition,[],[f8,f1]) ).
fof(f88,plain,
! [X0,X1] : mult(i(X0),mult(mult(mult(X1,i(X0)),i(X0)),X0)) = mult(mult(mult(i(X0),X1),i(X0)),unit),
inference(superposition,[],[f7,f12]) ).
fof(f95,plain,
! [X0,X1] : mult(mult(i(X0),X1),i(X0)) = mult(i(X0),mult(mult(mult(X1,i(X0)),i(X0)),X0)),
inference(forward_demodulation,[],[f88,f5]) ).
fof(f103,plain,
! [X0] : mult(mult(i(X0),unit),i(X0)) = mult(i(X0),mult(mult(i(X0),i(X0)),X0)),
inference(superposition,[],[f95,f6]) ).
fof(f110,plain,
! [X0] : mult(i(X0),i(X0)) = mult(i(X0),mult(mult(i(X0),i(X0)),X0)),
inference(forward_demodulation,[],[f103,f5]) ).
fof(f116,plain,
! [X0] : i(X0) = ld(X0,unit),
inference(superposition,[],[f2,f10]) ).
fof(f125,plain,
! [X0] : unit = ld(X0,X0),
inference(superposition,[],[f2,f5]) ).
fof(f127,plain,
! [X0,X1] : mult(mult(mult(X0,X1),X0),X0) = mult(X0,mult(mult(mult(X1,X0),X0),unit)),
inference(superposition,[],[f7,f5]) ).
fof(f128,plain,
! [X0,X1] : mult(X0,mult(mult(mult(unit,X0),X0),X1)) = mult(mult(X0,X0),mult(X0,X1)),
inference(superposition,[],[f7,f5]) ).
fof(f140,plain,
! [X0,X1] : mult(mult(X0,X0),mult(X0,X1)) = mult(X0,mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f128,f6]) ).
fof(f141,plain,
! [X0,X1] : mult(mult(mult(X0,X1),X0),X0) = mult(X0,mult(mult(X1,X0),X0)),
inference(forward_demodulation,[],[f127,f5]) ).
fof(f168,plain,
! [X0] : mult(mult(X0,X0),X0) = mult(X0,mult(mult(X0,X0),unit)),
inference(superposition,[],[f140,f5]) ).
fof(f187,plain,
! [X0] : mult(mult(X0,X0),X0) = mult(X0,mult(X0,X0)),
inference(forward_demodulation,[],[f168,f5]) ).
fof(f309,plain,
! [X0] : ld(mult(X0,X0),mult(X0,mult(X0,X0))) = X0,
inference(superposition,[],[f2,f187]) ).
fof(f385,plain,
! [X0,X1] : mult(mult(X0,mult(i(X0),X1)),i(X0)) = mult(unit,mult(i(X0),mult(ld(i(X0),X1),i(X0)))),
inference(superposition,[],[f59,f10]) ).
fof(f394,plain,
! [X0,X1] : mult(mult(i(X0),mult(X0,X1)),X0) = mult(unit,mult(X0,mult(ld(X0,X1),X0))),
inference(superposition,[],[f59,f12]) ).
fof(f404,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X2),X1)) = ld(mult(X0,X1),mult(mult(X0,mult(X1,X2)),X1)),
inference(superposition,[],[f2,f59]) ).
fof(f417,plain,
! [X0,X1] : mult(X0,mult(ld(X0,X1),X0)) = mult(mult(i(X0),mult(X0,X1)),X0),
inference(forward_demodulation,[],[f394,f6]) ).
fof(f421,plain,
! [X0,X1] : mult(i(X0),mult(ld(i(X0),X1),i(X0))) = mult(mult(X0,mult(i(X0),X1)),i(X0)),
inference(forward_demodulation,[],[f385,f6]) ).
fof(f442,plain,
! [X0,X1] : mult(mult(X1,rd(X0,X1)),X1) = mult(X1,mult(mult(X0,X1),i(X1))),
inference(superposition,[],[f53,f3]) ).
fof(f573,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f576,plain,
! [X0] : rd(unit,i(X0)) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f586,plain,
! [X0] : i(X0) = rd(unit,X0),
inference(superposition,[],[f4,f12]) ).
fof(f589,plain,
! [X0] : i(i(X0)) = X0,
inference(forward_demodulation,[],[f576,f586]) ).
fof(f600,plain,
! [X0] : mult(mult(i(X0),i(X0)),X0) = ld(i(X0),mult(i(X0),i(X0))),
inference(superposition,[],[f2,f110]) ).
fof(f617,plain,
! [X0] : i(X0) = mult(mult(i(X0),i(X0)),X0),
inference(forward_demodulation,[],[f600,f2]) ).
fof(f627,plain,
! [X0] : mult(mult(X0,X0),i(X0)) = X0,
inference(superposition,[],[f617,f589]) ).
fof(f630,plain,
! [X0] : mult(i(X0),i(X0)) = rd(i(X0),X0),
inference(superposition,[],[f4,f617]) ).
fof(f671,plain,
! [X0] : mult(X0,X0) = rd(X0,i(X0)),
inference(superposition,[],[f630,f589]) ).
fof(f805,plain,
! [X0,X1] : mult(mult(X1,rd(rd(X0,X1),X1)),X1) = mult(X1,mult(X0,i(X1))),
inference(superposition,[],[f442,f3]) ).
fof(f807,plain,
! [X0] : mult(mult(X0,rd(i(X0),X0)),X0) = mult(X0,mult(unit,i(X0))),
inference(superposition,[],[f442,f12]) ).
fof(f840,plain,
! [X0] : mult(X0,i(X0)) = mult(mult(X0,rd(i(X0),X0)),X0),
inference(forward_demodulation,[],[f807,f6]) ).
fof(f855,plain,
! [X0] : unit = mult(mult(X0,rd(i(X0),X0)),X0),
inference(forward_demodulation,[],[f840,f10]) ).
fof(f883,plain,
! [X0] : rd(unit,X0) = mult(X0,rd(i(X0),X0)),
inference(superposition,[],[f4,f855]) ).
fof(f910,plain,
! [X0] : i(X0) = mult(X0,rd(i(X0),X0)),
inference(forward_demodulation,[],[f883,f586]) ).
fof(f940,plain,
! [X0] : mult(i(X0),rd(X0,i(X0))) = X0,
inference(superposition,[],[f910,f589]) ).
fof(f943,plain,
! [X0] : rd(i(X0),X0) = ld(X0,i(X0)),
inference(superposition,[],[f2,f910]) ).
fof(f962,plain,
! [X0] : mult(i(X0),mult(X0,X0)) = X0,
inference(forward_demodulation,[],[f940,f671]) ).
fof(f986,plain,
! [X0] : mult(X0,X0) = ld(i(X0),X0),
inference(superposition,[],[f2,f962]) ).
fof(f987,plain,
! [X0] : i(X0) = rd(X0,mult(X0,X0)),
inference(superposition,[],[f4,f962]) ).
fof(f1022,plain,
! [X0] : mult(i(X0),i(X0)) = ld(X0,i(X0)),
inference(superposition,[],[f986,f589]) ).
fof(f1043,plain,
! [X0] : i(X0) = mult(ld(X0,i(X0)),X0),
inference(superposition,[],[f617,f1022]) ).
fof(f1168,plain,
! [X2,X0,X1] : mult(mult(mult(ld(X1,X0),X1),X1),X2) = ld(X1,mult(mult(X0,X1),mult(X1,X2))),
inference(superposition,[],[f2,f58]) ).
fof(f1426,plain,
! [X0,X1] : mult(X0,mult(mult(rd(rd(X1,X0),X0),X0),X0)) = mult(mult(X0,mult(X1,i(X0))),X0),
inference(superposition,[],[f141,f805]) ).
fof(f1448,plain,
! [X0,X1] : mult(mult(X0,mult(X1,i(X0))),X0) = mult(X0,mult(rd(X1,X0),X0)),
inference(forward_demodulation,[],[f1426,f3]) ).
fof(f1459,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,mult(X1,i(X0))),X0),
inference(forward_demodulation,[],[f1448,f3]) ).
fof(f1479,plain,
! [X0,X1] : mult(i(X0),X1) = mult(mult(i(X0),mult(X1,X0)),i(X0)),
inference(superposition,[],[f1459,f589]) ).
fof(f1493,plain,
! [X0,X1] : mult(mult(X1,X0),X1) = mult(X1,rd(X0,i(X1))),
inference(superposition,[],[f1459,f3]) ).
fof(f1511,plain,
! [X0,X1] : mult(X0,mult(X1,i(X0))) = rd(mult(X0,X1),X0),
inference(superposition,[],[f4,f1459]) ).
fof(f1582,plain,
! [X0,X1] : mult(mult(i(X0),X1),i(X0)) = mult(i(X0),rd(X1,X0)),
inference(superposition,[],[f1493,f589]) ).
fof(f1589,plain,
! [X0,X1] : ld(X0,mult(mult(X0,X1),X0)) = rd(X1,i(X0)),
inference(superposition,[],[f2,f1493]) ).
fof(f1661,plain,
! [X0,X1] : mult(mult(X0,mult(i(X0),X1)),X0) = mult(X0,mult(i(X0),mult(X1,X0))),
inference(superposition,[],[f1459,f1479]) ).
fof(f1664,plain,
! [X0,X1] : mult(i(X0),mult(X1,X0)) = rd(mult(i(X0),X1),i(X0)),
inference(superposition,[],[f4,f1479]) ).
fof(f1742,plain,
! [X0,X1] : mult(X0,i(X1)) = mult(i(X1),rd(ld(i(X1),X0),X1)),
inference(superposition,[],[f1582,f1]) ).
fof(f1864,plain,
! [X0,X1] : rd(ld(i(X1),X0),X1) = ld(i(X1),mult(X0,i(X1))),
inference(superposition,[],[f2,f1742]) ).
fof(f1900,plain,
! [X0,X1] : rd(ld(X1,X0),i(X1)) = ld(X1,mult(X0,X1)),
inference(superposition,[],[f1589,f1]) ).
fof(f1912,plain,
! [X0] : ld(mult(X0,X0),mult(X0,mult(X0,X0))) = rd(i(X0),i(mult(X0,X0))),
inference(superposition,[],[f1589,f627]) ).
fof(f1938,plain,
! [X0,X1] : rd(mult(X0,mult(X0,X1)),i(X0)) = ld(X0,mult(mult(X0,X0),mult(X0,mult(X1,X0)))),
inference(superposition,[],[f1589,f8]) ).
fof(f1940,plain,
! [X0,X1] : rd(mult(X0,X1),i(X0)) = ld(X0,mult(X0,mult(X0,mult(X1,X0)))),
inference(superposition,[],[f1589,f30]) ).
fof(f1963,plain,
! [X0,X1] : mult(X0,mult(X1,X0)) = rd(mult(X0,X1),i(X0)),
inference(forward_demodulation,[],[f1940,f2]) ).
fof(f1965,plain,
! [X0,X1] : rd(mult(X0,mult(X0,X1)),i(X0)) = mult(mult(mult(ld(X0,X0),X0),X0),mult(X1,X0)),
inference(forward_demodulation,[],[f1938,f1168]) ).
fof(f1981,plain,
! [X0] : rd(i(X0),i(mult(X0,X0))) = X0,
inference(forward_demodulation,[],[f1912,f309]) ).
fof(f1995,plain,
! [X0,X1] : rd(mult(X0,mult(X0,X1)),i(X0)) = mult(mult(mult(unit,X0),X0),mult(X1,X0)),
inference(forward_demodulation,[],[f1965,f125]) ).
fof(f2016,plain,
! [X0,X1] : mult(mult(X0,X0),mult(X1,X0)) = rd(mult(X0,mult(X0,X1)),i(X0)),
inference(forward_demodulation,[],[f1995,f6]) ).
fof(f2028,plain,
! [X0,X1] : mult(X0,mult(mult(X0,X1),X0)) = mult(mult(X0,X0),mult(X1,X0)),
inference(forward_demodulation,[],[f2016,f1963]) ).
fof(f2066,plain,
! [X0,X1] : mult(mult(X1,X1),X0) = mult(X1,mult(mult(X1,rd(X0,X1)),X1)),
inference(superposition,[],[f2028,f3]) ).
fof(f2262,plain,
! [X0] : i(X0) = mult(X0,i(mult(X0,X0))),
inference(superposition,[],[f3,f1981]) ).
fof(f2283,plain,
! [X0] : i(mult(X0,X0)) = ld(X0,i(X0)),
inference(superposition,[],[f2,f2262]) ).
fof(f2349,plain,
! [X0] : i(X0) = mult(i(mult(X0,X0)),X0),
inference(superposition,[],[f1043,f2283]) ).
fof(f2385,plain,
! [X0] : mult(i(mult(X0,X0)),rd(X0,mult(X0,X0))) = mult(i(X0),i(mult(X0,X0))),
inference(superposition,[],[f1582,f2349]) ).
fof(f2421,plain,
! [X0] : mult(i(mult(X0,X0)),i(X0)) = mult(i(X0),i(mult(X0,X0))),
inference(forward_demodulation,[],[f2385,f987]) ).
fof(f2791,plain,
! [X0] : i(mult(X0,X0)) = rd(mult(i(X0),i(mult(X0,X0))),i(X0)),
inference(superposition,[],[f4,f2421]) ).
fof(f2818,plain,
! [X0] : i(mult(X0,X0)) = mult(i(X0),mult(i(mult(X0,X0)),X0)),
inference(forward_demodulation,[],[f2791,f1664]) ).
fof(f2841,plain,
! [X0] : mult(i(X0),i(X0)) = i(mult(X0,X0)),
inference(forward_demodulation,[],[f2818,f2349]) ).
fof(f3115,plain,
! [X0,X1] : mult(X1,mult(ld(X1,X0),X1)) = rd(X0,i(X1)),
inference(superposition,[],[f1963,f1]) ).
fof(f3158,plain,
! [X0,X1] : mult(i(X0),mult(X1,i(X0))) = rd(mult(i(X0),X1),X0),
inference(superposition,[],[f1963,f589]) ).
fof(f3163,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,mult(X1,X0)),i(X0)),
inference(superposition,[],[f3,f1963]) ).
fof(f3423,plain,
! [X0,X1] : mult(X1,rd(X0,X1)) = mult(mult(X1,X0),i(X1)),
inference(superposition,[],[f3163,f3]) ).
fof(f3566,plain,
! [X0,X1] : mult(X0,i(X1)) = mult(X1,rd(ld(X1,X0),X1)),
inference(superposition,[],[f3423,f1]) ).
fof(f3612,plain,
! [X0,X1] : mult(i(X0),rd(X1,i(X0))) = mult(mult(i(X0),X1),X0),
inference(superposition,[],[f3423,f589]) ).
fof(f3647,plain,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = mult(mult(i(X0),mult(X0,rd(X1,X0))),i(i(X0))),
inference(superposition,[],[f3163,f3423]) ).
fof(f3648,plain,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = mult(i(X0),rd(mult(X0,rd(X1,X0)),i(X0))),
inference(forward_demodulation,[],[f3647,f3423]) ).
fof(f3700,plain,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = mult(mult(i(X0),mult(X0,rd(X1,X0))),X0),
inference(forward_demodulation,[],[f3648,f3612]) ).
fof(f3734,plain,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = mult(X0,mult(ld(X0,rd(X1,X0)),X0)),
inference(forward_demodulation,[],[f3700,f417]) ).
fof(f3760,plain,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = rd(rd(X1,X0),i(X0)),
inference(forward_demodulation,[],[f3734,f3115]) ).
fof(f3793,plain,
! [X0,X1] : rd(ld(X1,X0),X1) = ld(X1,mult(X0,i(X1))),
inference(superposition,[],[f2,f3566]) ).
fof(f3797,plain,
! [X2,X0,X1] : mult(mult(X2,X1),mult(X1,mult(rd(ld(X1,X0),X1),X1))) = mult(mult(X2,mult(X1,mult(X0,i(X1)))),X1),
inference(superposition,[],[f8,f3566]) ).
fof(f3828,plain,
! [X2,X0,X1] : mult(mult(X2,X1),mult(X1,mult(rd(ld(X1,X0),X1),X1))) = mult(mult(X2,rd(mult(X1,X0),X1)),X1),
inference(forward_demodulation,[],[f3797,f1511]) ).
fof(f3844,plain,
! [X2,X0,X1] : mult(mult(X2,rd(mult(X1,X0),X1)),X1) = mult(mult(X2,X1),mult(X1,ld(X1,X0))),
inference(forward_demodulation,[],[f3828,f3]) ).
fof(f3852,plain,
! [X2,X0,X1] : mult(mult(X2,rd(mult(X1,X0),X1)),X1) = mult(mult(X2,X1),X0),
inference(forward_demodulation,[],[f3844,f1]) ).
fof(f3865,plain,
! [X0,X1] : mult(i(i(X0)),mult(i(X0),ld(X0,X1))) = rd(ld(X0,mult(X1,X0)),i(i(X0))),
inference(superposition,[],[f3760,f1900]) ).
fof(f3866,plain,
! [X0,X1] : rd(X0,i(X1)) = mult(i(X1),mult(X1,mult(X0,X1))),
inference(superposition,[],[f3760,f4]) ).
fof(f3867,plain,
! [X0,X1] : mult(i(i(X0)),mult(i(X0),mult(X0,X1))) = rd(mult(X0,mult(X1,X0)),i(i(X0))),
inference(superposition,[],[f3760,f1963]) ).
fof(f3874,plain,
! [X0,X1] : mult(X0,mult(i(X0),X1)) = rd(rd(X1,i(X0)),X0),
inference(superposition,[],[f3760,f589]) ).
fof(f3875,plain,
! [X0,X1] : mult(mult(X0,rd(X1,X0)),X0) = mult(X0,mult(i(X0),mult(X0,X1))),
inference(superposition,[],[f1493,f3760]) ).
fof(f3876,plain,
! [X0,X1] : mult(i(X0),mult(rd(X1,X0),i(i(X0)))) = mult(mult(i(X0),rd(mult(i(X0),mult(X0,X1)),i(X0))),i(X0)),
inference(superposition,[],[f805,f3760]) ).
fof(f3877,plain,
! [X0,X1] : rd(X1,X0) = mult(mult(i(X0),mult(X0,X1)),i(X0)),
inference(superposition,[],[f3,f3760]) ).
fof(f3878,plain,
! [X0,X1] : rd(X1,X0) = mult(i(X0),rd(mult(X0,X1),X0)),
inference(forward_demodulation,[],[f3877,f1582]) ).
fof(f3879,plain,
! [X0,X1] : mult(mult(i(X0),i(X0)),mult(X0,X1)) = mult(i(X0),mult(rd(X1,X0),i(i(X0)))),
inference(forward_demodulation,[],[f3876,f3852]) ).
fof(f3886,plain,
! [X0,X1] : mult(X0,mult(i(X0),mult(X0,X1))) = rd(mult(X0,mult(X1,X0)),X0),
inference(forward_demodulation,[],[f3867,f589]) ).
fof(f3887,plain,
! [X0,X1] : mult(X0,mult(i(X0),ld(X0,X1))) = rd(ld(X0,mult(X1,X0)),X0),
inference(forward_demodulation,[],[f3865,f589]) ).
fof(f3892,plain,
! [X0,X1] : mult(mult(i(X0),i(X0)),mult(X0,X1)) = rd(mult(i(X0),rd(X1,X0)),i(X0)),
inference(forward_demodulation,[],[f3879,f1511]) ).
fof(f3899,plain,
! [X0,X1] : mult(mult(X0,rd(X1,X0)),X0) = rd(mult(X0,mult(X1,X0)),X0),
inference(forward_demodulation,[],[f3886,f3875]) ).
fof(f3904,plain,
! [X0,X1] : mult(mult(i(X0),i(X0)),mult(X0,X1)) = mult(i(X0),mult(rd(X1,X0),X0)),
inference(forward_demodulation,[],[f3892,f1664]) ).
fof(f3910,plain,
! [X0,X1] : mult(i(X0),X1) = mult(mult(i(X0),i(X0)),mult(X0,X1)),
inference(forward_demodulation,[],[f3904,f3]) ).
fof(f3914,plain,
! [X0,X1] : mult(i(X0),X1) = mult(rd(i(X0),X0),mult(X0,X1)),
inference(forward_demodulation,[],[f3910,f630]) ).
fof(f3917,plain,
! [X0,X1] : mult(i(X0),X1) = mult(ld(X0,i(X0)),mult(X0,X1)),
inference(forward_demodulation,[],[f3914,f943]) ).
fof(f3918,plain,
! [X0,X1] : mult(i(X0),X1) = mult(i(mult(X0,X0)),mult(X0,X1)),
inference(forward_demodulation,[],[f3917,f2283]) ).
fof(f3923,plain,
! [X0,X1] : mult(i(i(X0)),X1) = mult(i(i(mult(X0,X0))),mult(i(X0),X1)),
inference(superposition,[],[f3918,f2841]) ).
fof(f3926,plain,
! [X0,X1] : mult(i(X1),ld(X1,X0)) = mult(i(mult(X1,X1)),X0),
inference(superposition,[],[f3918,f1]) ).
fof(f3980,plain,
! [X0,X1] : mult(mult(i(X0),mult(X0,X1)),X0) = mult(mult(i(mult(X0,X0)),X0),mult(X0,mult(X1,X0))),
inference(superposition,[],[f8,f3918]) ).
fof(f4016,plain,
! [X0,X1] : mult(mult(i(X0),mult(X0,X1)),X0) = mult(i(X0),mult(X0,mult(X1,X0))),
inference(forward_demodulation,[],[f3980,f2349]) ).
fof(f4053,plain,
! [X0,X1] : mult(i(i(X0)),X1) = mult(mult(X0,X0),mult(i(X0),X1)),
inference(forward_demodulation,[],[f3923,f589]) ).
fof(f4068,plain,
! [X0,X1] : mult(mult(i(X0),mult(X0,X1)),X0) = rd(X1,i(X0)),
inference(forward_demodulation,[],[f4016,f3866]) ).
fof(f4100,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,X0),mult(i(X0),X1)),
inference(forward_demodulation,[],[f4053,f589]) ).
fof(f4194,plain,
! [X0,X1] : mult(mult(i(X1),X0),X1) = rd(ld(X1,X0),i(X1)),
inference(superposition,[],[f4068,f1]) ).
fof(f4202,plain,
! [X0,X1] : mult(mult(i(X1),mult(X0,i(X1))),X1) = rd(rd(ld(X1,X0),X1),i(X1)),
inference(superposition,[],[f4068,f3566]) ).
fof(f4252,plain,
! [X0,X1] : rd(rd(X0,i(X1)),X1) = mult(i(X1),mult(X1,X0)),
inference(superposition,[],[f4,f4068]) ).
fof(f4294,plain,
! [X0,X1] : mult(X1,mult(i(X1),X0)) = mult(i(X1),mult(X1,X0)),
inference(forward_demodulation,[],[f4252,f3874]) ).
fof(f4328,plain,
! [X0,X1] : mult(i(X1),mult(X1,ld(X1,X0))) = mult(mult(i(X1),mult(X0,i(X1))),X1),
inference(forward_demodulation,[],[f4202,f3760]) ).
fof(f4336,plain,
! [X0,X1] : mult(mult(i(X1),X0),X1) = ld(X1,mult(X0,X1)),
inference(forward_demodulation,[],[f4194,f1900]) ).
fof(f4369,plain,
! [X0,X1] : mult(i(X1),mult(X1,ld(X1,X0))) = mult(rd(mult(i(X1),X0),X1),X1),
inference(forward_demodulation,[],[f4328,f3158]) ).
fof(f4396,plain,
! [X0,X1] : mult(i(X1),X0) = mult(i(X1),mult(X1,ld(X1,X0))),
inference(forward_demodulation,[],[f4369,f3]) ).
fof(f4413,plain,
! [X0,X1] : mult(i(X1),X0) = mult(X1,mult(i(X1),ld(X1,X0))),
inference(forward_demodulation,[],[f4396,f4294]) ).
fof(f4437,plain,
! [X0,X1] : mult(i(X0),mult(mult(X0,X1),X0)) = mult(X0,mult(i(X0),rd(X1,i(X0)))),
inference(superposition,[],[f4294,f1493]) ).
fof(f4443,plain,
! [X0,X1] : mult(i(mult(X0,X0)),mult(X0,mult(mult(X0,X0),X1))) = mult(mult(X0,X0),mult(i(mult(X0,X0)),mult(X0,X1))),
inference(superposition,[],[f4294,f140]) ).
fof(f4507,plain,
! [X0,X1] : mult(i(X0),rd(mult(X0,X1),i(X0))) = mult(mult(X0,mult(i(X0),X1)),i(i(X0))),
inference(superposition,[],[f3423,f4294]) ).
fof(f4512,plain,
! [X0,X1] : mult(mult(X0,mult(i(X0),X1)),X0) = mult(i(X0),rd(mult(X0,X1),i(X0))),
inference(forward_demodulation,[],[f4507,f589]) ).
fof(f4562,plain,
! [X0,X1] : mult(mult(X0,X0),mult(i(X0),X1)) = mult(i(mult(X0,X0)),mult(X0,mult(mult(X0,X0),X1))),
inference(forward_demodulation,[],[f4443,f3918]) ).
fof(f4568,plain,
! [X0,X1] : mult(i(X0),mult(mult(X0,X1),X0)) = mult(X0,mult(mult(i(X0),X1),X0)),
inference(forward_demodulation,[],[f4437,f3612]) ).
fof(f4575,plain,
! [X0,X1] : mult(mult(i(X0),mult(X0,X1)),X0) = mult(mult(X0,mult(i(X0),X1)),X0),
inference(forward_demodulation,[],[f4512,f3612]) ).
fof(f4609,plain,
! [X0,X1] : mult(mult(X0,X0),mult(i(X0),X1)) = mult(i(X0),mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f4562,f3918]) ).
fof(f4614,plain,
! [X0,X1] : mult(i(X0),mult(mult(X0,X1),X0)) = mult(X0,ld(X0,mult(X1,X0))),
inference(forward_demodulation,[],[f4568,f4336]) ).
fof(f4618,plain,
! [X0,X1] : mult(mult(i(X0),mult(X0,X1)),X0) = mult(X0,mult(i(X0),mult(X1,X0))),
inference(forward_demodulation,[],[f4575,f1661]) ).
fof(f4644,plain,
! [X0,X1] : mult(X0,X1) = mult(i(X0),mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f4609,f4100]) ).
fof(f4648,plain,
! [X0,X1] : mult(X1,X0) = mult(i(X0),mult(mult(X0,X1),X0)),
inference(forward_demodulation,[],[f4614,f1]) ).
fof(f4651,plain,
! [X0,X1] : mult(X0,mult(ld(X0,X1),X0)) = mult(X0,mult(i(X0),mult(X1,X0))),
inference(forward_demodulation,[],[f4618,f417]) ).
fof(f4673,plain,
! [X0,X1] : rd(X1,i(X0)) = mult(X0,mult(i(X0),mult(X1,X0))),
inference(forward_demodulation,[],[f4651,f3115]) ).
fof(f4706,plain,
! [X0,X1] : mult(mult(X0,X1),i(X0)) = ld(i(X0),mult(X1,i(X0))),
inference(superposition,[],[f4336,f589]) ).
fof(f4713,plain,
! [X0,X1] : mult(mult(X0,i(X1)),X1) = ld(X1,mult(rd(ld(i(X1),X0),X1),X1)),
inference(superposition,[],[f4336,f1742]) ).
fof(f4753,plain,
! [X0,X1] : mult(i(X0),X1) = rd(ld(X0,mult(X1,X0)),X0),
inference(superposition,[],[f4,f4336]) ).
fof(f4768,plain,
! [X0,X1] : mult(X0,mult(i(X0),X1)) = mult(mult(X0,ld(X0,mult(X1,X0))),i(X0)),
inference(superposition,[],[f3163,f4336]) ).
fof(f4786,plain,
! [X0,X1] : mult(X0,mult(i(X0),X1)) = mult(X0,rd(ld(X0,mult(X1,X0)),X0)),
inference(forward_demodulation,[],[f4768,f3423]) ).
fof(f4827,plain,
! [X0,X1] : mult(mult(X0,i(X1)),X1) = ld(X1,ld(i(X1),X0)),
inference(forward_demodulation,[],[f4713,f3]) ).
fof(f4834,plain,
! [X0,X1] : mult(X0,rd(X1,X0)) = ld(i(X0),mult(X1,i(X0))),
inference(forward_demodulation,[],[f4706,f3423]) ).
fof(f4840,plain,
! [X0,X1] : mult(X0,mult(i(X0),X1)) = mult(mult(X1,X0),i(X0)),
inference(forward_demodulation,[],[f4786,f3566]) ).
fof(f4955,plain,
! [X0,X1] : mult(X0,i(X1)) = mult(X1,mult(i(X1),rd(X0,X1))),
inference(superposition,[],[f4840,f3]) ).
fof(f4971,plain,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = mult(mult(X1,i(X0)),X0),
inference(superposition,[],[f4840,f589]) ).
fof(f5038,plain,
! [X0,X1] : mult(X0,mult(i(X0),X1)) = mult(mult(X1,i(X0)),X0),
inference(forward_demodulation,[],[f4971,f4294]) ).
fof(f5226,plain,
! [X0,X1] : mult(ld(X0,X1),i(i(X0))) = mult(i(X0),mult(i(i(X0)),ld(X0,mult(X1,X0)))),
inference(superposition,[],[f4955,f1900]) ).
fof(f5293,plain,
! [X0,X1] : mult(ld(X0,X1),X0) = mult(i(X0),mult(X0,ld(X0,mult(X1,X0)))),
inference(forward_demodulation,[],[f5226,f589]) ).
fof(f5318,plain,
! [X0,X1] : mult(ld(X0,X1),X0) = mult(X0,mult(i(X0),ld(X0,mult(X1,X0)))),
inference(forward_demodulation,[],[f5293,f4294]) ).
fof(f5340,plain,
! [X0,X1] : mult(ld(X0,X1),X0) = rd(ld(X0,mult(mult(X1,X0),X0)),X0),
inference(forward_demodulation,[],[f5318,f3887]) ).
fof(f5349,plain,
! [X0,X1] : mult(ld(X0,X1),X0) = mult(i(X0),mult(X1,X0)),
inference(forward_demodulation,[],[f5340,f4753]) ).
fof(f5499,plain,
! [X0,X1] : mult(i(X0),mult(X0,mult(X1,i(X0)))) = mult(ld(X0,mult(X0,rd(rd(X1,X0),X0))),X0),
inference(superposition,[],[f5349,f805]) ).
fof(f5509,plain,
! [X0,X1] : mult(i(X1),X0) = mult(ld(X1,rd(X0,X1)),X1),
inference(superposition,[],[f5349,f3]) ).
fof(f5537,plain,
! [X0,X1] : mult(mult(i(X0),X1),i(X0)) = mult(ld(X0,mult(mult(X1,i(X0)),i(X0))),X0),
inference(superposition,[],[f95,f5349]) ).
fof(f5594,plain,
! [X0,X1] : mult(mult(i(X0),X1),i(X0)) = mult(rd(ld(X0,mult(X1,i(X0))),X0),X0),
inference(forward_demodulation,[],[f5537,f3793]) ).
fof(f5625,plain,
! [X0,X1] : mult(rd(rd(X1,X0),X0),X0) = mult(i(X0),mult(X0,mult(X1,i(X0)))),
inference(forward_demodulation,[],[f5499,f2]) ).
fof(f5664,plain,
! [X0,X1] : mult(mult(i(X0),X1),i(X0)) = ld(X0,mult(X1,i(X0))),
inference(forward_demodulation,[],[f5594,f3]) ).
fof(f5690,plain,
! [X0,X1] : mult(rd(rd(X1,X0),X0),X0) = mult(X0,mult(i(X0),mult(X1,i(X0)))),
inference(forward_demodulation,[],[f5625,f4294]) ).
fof(f5719,plain,
! [X0,X1] : mult(mult(i(X0),X1),i(X0)) = rd(ld(X0,X1),X0),
inference(forward_demodulation,[],[f5664,f3793]) ).
fof(f5737,plain,
! [X0,X1] : mult(rd(rd(X1,X0),X0),X0) = mult(X0,rd(mult(i(X0),X1),X0)),
inference(forward_demodulation,[],[f5690,f3158]) ).
fof(f5767,plain,
! [X0,X1] : rd(X1,X0) = mult(X0,rd(mult(i(X0),X1),X0)),
inference(forward_demodulation,[],[f5737,f3]) ).
fof(f5829,plain,
! [X2,X0,X1] : mult(X1,mult(mult(mult(rd(mult(i(X1),X0),X1),X1),X1),X2)) = mult(mult(rd(X0,X1),X1),mult(X1,X2)),
inference(superposition,[],[f7,f5767]) ).
fof(f5841,plain,
! [X0,X1] : rd(rd(X0,X1),i(X1)) = mult(X1,mult(rd(mult(i(X1),X0),X1),X1)),
inference(superposition,[],[f1963,f5767]) ).
fof(f5864,plain,
! [X0,X1] : mult(X1,mult(i(X1),X0)) = rd(rd(X0,X1),i(X1)),
inference(forward_demodulation,[],[f5841,f3]) ).
fof(f5874,plain,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = mult(X1,mult(mult(mult(rd(mult(i(X1),X0),X1),X1),X1),X2)),
inference(forward_demodulation,[],[f5829,f3]) ).
fof(f5918,plain,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = mult(X1,mult(mult(mult(i(X1),X0),X1),X2)),
inference(forward_demodulation,[],[f5874,f3]) ).
fof(f5950,plain,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = mult(X1,mult(ld(X1,mult(X0,X1)),X2)),
inference(forward_demodulation,[],[f5918,f4336]) ).
fof(f6089,plain,
! [X0,X1] : mult(X0,mult(i(X0),mult(i(i(X0)),X1))) = mult(ld(i(X0),mult(X1,i(X0))),X0),
inference(superposition,[],[f5038,f4336]) ).
fof(f6188,plain,
! [X0,X1] : mult(X0,mult(i(X0),mult(i(i(X0)),X1))) = mult(rd(ld(i(X0),X1),X0),X0),
inference(forward_demodulation,[],[f6089,f1864]) ).
fof(f6242,plain,
! [X0,X1] : ld(i(X0),X1) = mult(X0,mult(i(X0),mult(i(i(X0)),X1))),
inference(forward_demodulation,[],[f6188,f3]) ).
fof(f6281,plain,
! [X0,X1] : ld(i(X0),X1) = mult(X0,mult(i(X0),mult(X0,X1))),
inference(forward_demodulation,[],[f6242,f589]) ).
fof(f6302,plain,
! [X0,X1] : ld(i(X0),X1) = mult(X0,mult(X0,mult(i(X0),X1))),
inference(forward_demodulation,[],[f6281,f4294]) ).
fof(f6418,plain,
! [X0,X1] : mult(mult(X1,X0),X1) = ld(i(X1),mult(X0,X1)),
inference(superposition,[],[f2,f4648]) ).
fof(f6708,plain,
! [X0,X1] : ld(i(X0),mult(X0,X1)) = mult(X0,rd(mult(X0,mult(X1,X0)),X0)),
inference(superposition,[],[f4834,f3163]) ).
fof(f6782,plain,
! [X0,X1] : mult(X0,mult(mult(X0,rd(X1,X0)),X0)) = ld(i(X0),mult(X0,X1)),
inference(forward_demodulation,[],[f6708,f3899]) ).
fof(f6813,plain,
! [X0,X1] : mult(mult(X0,X0),X1) = ld(i(X0),mult(X0,X1)),
inference(forward_demodulation,[],[f6782,f2066]) ).
fof(f6871,plain,
! [X0,X1] : mult(i(i(X0)),ld(i(X0),X1)) = mult(i(i(mult(X0,X0))),X1),
inference(superposition,[],[f3926,f2841]) ).
fof(f6913,plain,
! [X0,X1] : mult(i(mult(X0,X0)),X1) = mult(mult(X0,X0),mult(i(X0),ld(X0,ld(mult(X0,X0),X1)))),
inference(superposition,[],[f4413,f3926]) ).
fof(f6918,plain,
! [X0,X1] : mult(ld(mult(X0,X0),X1),mult(X0,X0)) = mult(i(X0),ld(X0,mult(X1,mult(X0,X0)))),
inference(superposition,[],[f5349,f3926]) ).
fof(f6919,plain,
! [X0,X1] : mult(i(mult(X0,X0)),X1) = mult(mult(i(X0),ld(X0,mult(X1,mult(X0,X0)))),i(mult(X0,X0))),
inference(superposition,[],[f1479,f3926]) ).
fof(f6925,plain,
! [X0,X1] : mult(X1,i(mult(X0,X0))) = mult(mult(X0,X0),mult(i(X0),ld(X0,rd(X1,mult(X0,X0))))),
inference(superposition,[],[f4955,f3926]) ).
fof(f7070,plain,
! [X0,X1] : mult(X1,i(mult(X0,X0))) = mult(X0,ld(X0,rd(X1,mult(X0,X0)))),
inference(forward_demodulation,[],[f6925,f4100]) ).
fof(f7075,plain,
! [X0,X1] : mult(i(X0),ld(X0,X1)) = mult(mult(i(X0),ld(X0,mult(X1,mult(X0,X0)))),i(mult(X0,X0))),
inference(forward_demodulation,[],[f6919,f3926]) ).
fof(f7080,plain,
! [X0,X1] : mult(i(mult(X0,X0)),X1) = mult(X0,ld(X0,ld(mult(X0,X0),X1))),
inference(forward_demodulation,[],[f6913,f4100]) ).
fof(f7116,plain,
! [X0,X1] : mult(mult(X0,X0),X1) = mult(i(i(X0)),ld(i(X0),X1)),
inference(forward_demodulation,[],[f6871,f589]) ).
fof(f7168,plain,
! [X0,X1] : mult(X1,i(mult(X0,X0))) = rd(X1,mult(X0,X0)),
inference(forward_demodulation,[],[f7070,f1]) ).
fof(f7172,plain,
! [X0,X1] : mult(i(X0),ld(X0,X1)) = mult(mult(ld(mult(X0,X0),X1),mult(X0,X0)),i(mult(X0,X0))),
inference(forward_demodulation,[],[f7075,f6918]) ).
fof(f7177,plain,
! [X0,X1] : ld(mult(X0,X0),X1) = mult(i(mult(X0,X0)),X1),
inference(forward_demodulation,[],[f7080,f1]) ).
fof(f7203,plain,
! [X0,X1] : mult(mult(X0,X0),X1) = mult(X0,ld(i(X0),X1)),
inference(forward_demodulation,[],[f7116,f589]) ).
fof(f7242,plain,
! [X0,X1] : mult(i(X0),ld(X0,X1)) = rd(mult(ld(mult(X0,X0),X1),mult(X0,X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f7172,f7168]) ).
fof(f7293,plain,
! [X0,X1] : ld(mult(X0,X0),X1) = mult(i(X0),ld(X0,X1)),
inference(forward_demodulation,[],[f7242,f4]) ).
fof(f7401,plain,
! [X0,X1] : rd(X1,i(mult(X0,X0))) = mult(X1,i(i(mult(X0,X0)))),
inference(superposition,[],[f7168,f2841]) ).
fof(f7642,plain,
! [X0,X1] : mult(X1,mult(X0,X0)) = rd(X1,i(mult(X0,X0))),
inference(forward_demodulation,[],[f7401,f589]) ).
fof(f8769,plain,
! [X0,X1] : mult(mult(X1,X0),i(X0)) = ld(i(X0),ld(X0,X1)),
inference(superposition,[],[f4827,f589]) ).
fof(f8812,plain,
! [X0,X1] : mult(X0,mult(i(X0),X1)) = ld(i(X0),ld(X0,X1)),
inference(forward_demodulation,[],[f8769,f4840]) ).
fof(f9765,plain,
! [X0,X1] : rd(mult(X1,X0),X1) = ld(i(X1),rd(X0,X1)),
inference(superposition,[],[f2,f3878]) ).
fof(f10708,plain,
! [X0,X1] : mult(mult(X0,X0),ld(X0,X1)) = mult(X0,mult(X0,mult(i(X0),X1))),
inference(superposition,[],[f7203,f8812]) ).
fof(f10728,plain,
! [X0,X1] : mult(mult(X0,X0),ld(X0,X1)) = ld(i(X0),X1),
inference(forward_demodulation,[],[f10708,f6302]) ).
fof(f11397,plain,
! [X0,X1] : mult(i(X0),X1) = mult(X0,ld(mult(X0,X0),X1)),
inference(superposition,[],[f4413,f7293]) ).
fof(f11616,plain,
! [X0,X1] : mult(mult(X1,rd(X0,X1)),X1) = ld(i(X1),X0),
inference(superposition,[],[f6418,f3]) ).
fof(f11904,plain,
! [X2,X0,X1] : mult(ld(i(X0),X1),mult(X0,X2)) = mult(X0,mult(mult(mult(rd(X1,X0),X0),X0),X2)),
inference(superposition,[],[f7,f11616]) ).
fof(f11974,plain,
! [X2,X0,X1] : mult(ld(i(X0),X1),mult(X0,X2)) = mult(X0,mult(mult(X1,X0),X2)),
inference(forward_demodulation,[],[f11904,f3]) ).
fof(f12119,plain,
! [X2,X0,X1] : mult(X1,mult(mult(X2,X1),ld(X1,X0))) = mult(ld(i(X1),X2),X0),
inference(superposition,[],[f11974,f1]) ).
fof(f12474,plain,
! [X2,X0,X1] : mult(ld(i(X1),rd(X0,X1)),X2) = mult(X1,mult(X0,ld(X1,X2))),
inference(superposition,[],[f12119,f3]) ).
fof(f12611,plain,
! [X2,X0,X1] : mult(rd(mult(X1,X0),X1),X2) = mult(X1,mult(X0,ld(X1,X2))),
inference(forward_demodulation,[],[f12474,f9765]) ).
fof(f15029,plain,
! [X0,X1] : mult(rd(X0,i(X1)),X1) = mult(X1,mult(ld(X1,mult(X0,X1)),X1)),
inference(superposition,[],[f417,f3866]) ).
fof(f15100,plain,
! [X0,X1] : mult(X0,mult(X1,X1)) = mult(rd(X0,i(X1)),X1),
inference(forward_demodulation,[],[f15029,f5950]) ).
fof(f15491,plain,
! [X0,X1] : mult(X1,mult(i(X0),i(X0))) = mult(rd(X1,X0),i(X0)),
inference(superposition,[],[f15100,f589]) ).
fof(f15500,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,i(X1)),mult(X1,X1)),
inference(superposition,[],[f15100,f4]) ).
fof(f15596,plain,
! [X0,X1] : mult(X1,rd(i(X0),X0)) = mult(rd(X1,X0),i(X0)),
inference(forward_demodulation,[],[f15491,f630]) ).
fof(f15625,plain,
! [X0,X1] : mult(X1,ld(X0,i(X0))) = mult(rd(X1,X0),i(X0)),
inference(forward_demodulation,[],[f15596,f943]) ).
fof(f15644,plain,
! [X0,X1] : mult(X1,i(mult(X0,X0))) = mult(rd(X1,X0),i(X0)),
inference(forward_demodulation,[],[f15625,f2283]) ).
fof(f15656,plain,
! [X0,X1] : rd(X1,mult(X0,X0)) = mult(rd(X1,X0),i(X0)),
inference(forward_demodulation,[],[f15644,f7168]) ).
fof(f17448,plain,
! [X2,X0,X1] : mult(mult(X1,X2),ld(X2,X0)) = mult(mult(X1,rd(X0,X2)),X2),
inference(superposition,[],[f3852,f1]) ).
fof(f19179,plain,
! [X2,X0,X1] : mult(rd(X0,X1),X2) = mult(X1,mult(ld(X1,X0),ld(X1,X2))),
inference(superposition,[],[f12611,f1]) ).
fof(f19843,plain,
! [X2,X0,X1] : ld(X1,mult(rd(X0,X1),X2)) = mult(ld(X1,X0),ld(X1,X2)),
inference(superposition,[],[f2,f19179]) ).
fof(f20910,plain,
! [X2,X0,X1] : mult(ld(X1,mult(X0,X1)),X2) = ld(X1,mult(X0,mult(X1,X2))),
inference(superposition,[],[f2,f5950]) ).
fof(f22286,plain,
! [X0,X1] : ld(X0,unit) = mult(ld(X0,mult(i(mult(X0,X1)),X0)),X1),
inference(superposition,[],[f20910,f12]) ).
fof(f22334,plain,
! [X0,X1] : i(X0) = mult(ld(X0,mult(i(mult(X0,X1)),X0)),X1),
inference(forward_demodulation,[],[f22286,f116]) ).
fof(f23936,plain,
! [X0,X1] : mult(mult(rd(X0,X1),rd(X0,X1)),X1) = ld(i(rd(X0,X1)),X0),
inference(superposition,[],[f6813,f3]) ).
fof(f24050,plain,
! [X0,X1] : ld(i(rd(X0,X1)),X0) = mult(mult(rd(X0,X1),X1),ld(X1,X0)),
inference(forward_demodulation,[],[f23936,f17448]) ).
fof(f24146,plain,
! [X0,X1] : mult(X0,ld(X1,X0)) = ld(i(rd(X0,X1)),X0),
inference(forward_demodulation,[],[f24050,f3]) ).
fof(f24452,plain,
! [X0,X1] : i(rd(X0,X1)) = rd(X0,mult(X0,ld(X1,X0))),
inference(superposition,[],[f573,f24146]) ).
fof(f27728,plain,
! [X0,X1] : mult(X0,mult(ld(X0,X1),X0)) = ld(mult(i(mult(X0,X1)),X0),mult(unit,X0)),
inference(superposition,[],[f404,f12]) ).
fof(f27795,plain,
! [X0,X1] : mult(X0,mult(ld(X0,X1),X0)) = ld(mult(i(mult(X0,X1)),X0),X0),
inference(forward_demodulation,[],[f27728,f6]) ).
fof(f28069,plain,
! [X0,X1] : rd(X1,i(X0)) = ld(mult(i(mult(X0,X1)),X0),X0),
inference(forward_demodulation,[],[f27795,f3115]) ).
fof(f28862,plain,
! [X0,X1] : rd(ld(X1,X0),i(X1)) = ld(mult(i(X0),X1),X1),
inference(superposition,[],[f28069,f1]) ).
fof(f28969,plain,
! [X0,X1] : rd(X1,rd(X0,i(X1))) = mult(i(mult(X1,X0)),X1),
inference(superposition,[],[f573,f28069]) ).
fof(f29066,plain,
! [X0,X1] : ld(X1,mult(X0,X1)) = ld(mult(i(X0),X1),X1),
inference(forward_demodulation,[],[f28862,f1900]) ).
fof(f29262,plain,
! [X0,X1] : ld(X1,mult(i(X0),X1)) = ld(mult(X0,X1),X1),
inference(superposition,[],[f29066,f589]) ).
fof(f29324,plain,
! [X0,X1] : mult(i(X1),X0) = rd(X0,ld(X0,mult(X1,X0))),
inference(superposition,[],[f573,f29066]) ).
fof(f29799,plain,
! [X0,X1] : mult(i(X0),X1) = mult(X1,ld(mult(X0,X1),X1)),
inference(superposition,[],[f1,f29262]) ).
fof(f29816,plain,
! [X0,X1] : ld(mult(X0,i(X1)),i(X1)) = mult(X1,rd(i(X0),X1)),
inference(superposition,[],[f4834,f29262]) ).
fof(f30115,plain,
! [X0,X1] : mult(X1,ld(X0,X1)) = mult(i(rd(X0,X1)),X1),
inference(superposition,[],[f29799,f3]) ).
fof(f30530,plain,
! [X0,X1] : mult(i(mult(X0,mult(i(X0),X1))),i(X0)) = mult(i(X0),ld(rd(X1,X0),i(X0))),
inference(superposition,[],[f30115,f5864]) ).
fof(f30611,plain,
! [X0,X1] : mult(X0,rd(i(rd(X1,i(X0))),X0)) = ld(i(X0),mult(i(X0),ld(X1,i(X0)))),
inference(superposition,[],[f4834,f30115]) ).
fof(f30619,plain,
! [X0,X1] : ld(X1,i(X0)) = mult(X0,rd(i(rd(X1,i(X0))),X0)),
inference(forward_demodulation,[],[f30611,f2]) ).
fof(f36264,plain,
! [X0,X1] : ld(X0,mult(i(mult(X0,X1)),X0)) = rd(i(X0),X1),
inference(superposition,[],[f4,f22334]) ).
fof(f36401,plain,
! [X0,X1] : ld(mult(mult(X0,X1),X0),X0) = rd(i(X0),X1),
inference(forward_demodulation,[],[f36264,f29262]) ).
fof(f36994,plain,
! [X0,X1] : ld(mult(X0,X1),X1) = rd(i(X1),ld(X1,X0)),
inference(superposition,[],[f36401,f1]) ).
fof(f37106,plain,
! [X0,X1] : ld(mult(X0,X1),X0) = rd(i(X0),mult(X1,i(X0))),
inference(superposition,[],[f36401,f1459]) ).
fof(f37114,plain,
! [X0,X1] : rd(i(X0),rd(mult(X0,X1),X0)) = ld(mult(mult(X0,X0),X1),X0),
inference(superposition,[],[f36401,f3852]) ).
fof(f37122,plain,
! [X0,X1] : ld(rd(ld(X0,X1),X0),i(X0)) = rd(i(i(X0)),X1),
inference(superposition,[],[f36401,f5719]) ).
fof(f37127,plain,
! [X0,X1] : mult(i(mult(X0,X1)),X0) = mult(X0,rd(i(X0),X1)),
inference(superposition,[],[f29799,f36401]) ).
fof(f37131,plain,
! [X0,X1] : mult(mult(X0,X1),X0) = rd(X0,rd(i(X0),X1)),
inference(superposition,[],[f573,f36401]) ).
fof(f37157,plain,
! [X0,X1] : rd(X0,X1) = ld(rd(ld(X0,X1),X0),i(X0)),
inference(forward_demodulation,[],[f37122,f589]) ).
fof(f37449,plain,
! [X0,X1] : rd(X0,ld(i(X0),X1)) = ld(mult(X1,i(X0)),i(X0)),
inference(superposition,[],[f36994,f589]) ).
fof(f37541,plain,
! [X0,X1] : rd(X0,ld(i(X0),X1)) = mult(X0,rd(i(X1),X0)),
inference(forward_demodulation,[],[f37449,f29816]) ).
fof(f37598,plain,
! [X0,X1] : rd(X1,X0) = mult(X1,rd(i(mult(i(X1),X0)),X1)),
inference(superposition,[],[f37541,f2]) ).
fof(f37750,plain,
! [X0,X1] : mult(X1,rd(i(rd(X0,i(X1))),X1)) = rd(X1,rd(mult(i(i(X1)),X0),i(X1))),
inference(superposition,[],[f37598,f5767]) ).
fof(f37794,plain,
! [X0,X1] : mult(rd(i(mult(i(X0),X1)),X0),X0) = mult(i(X0),mult(rd(X0,X1),X0)),
inference(superposition,[],[f4648,f37598]) ).
fof(f37865,plain,
! [X0,X1] : mult(rd(i(mult(i(X0),X1)),X0),X0) = mult(ld(X0,rd(X0,X1)),X0),
inference(forward_demodulation,[],[f37794,f5349]) ).
fof(f37904,plain,
! [X0,X1] : mult(X1,rd(i(rd(X0,i(X1))),X1)) = mult(i(mult(X1,mult(i(i(X1)),X0))),X1),
inference(forward_demodulation,[],[f37750,f28969]) ).
fof(f37967,plain,
! [X0,X1] : i(mult(i(X0),X1)) = mult(ld(X0,rd(X0,X1)),X0),
inference(forward_demodulation,[],[f37865,f3]) ).
fof(f37997,plain,
! [X0,X1] : mult(X1,rd(i(rd(X0,i(X1))),X1)) = mult(X1,rd(i(X1),mult(i(i(X1)),X0))),
inference(forward_demodulation,[],[f37904,f37127]) ).
fof(f38058,plain,
! [X0,X1] : mult(X1,rd(i(rd(X0,i(X1))),X1)) = mult(X1,rd(i(X1),mult(X1,X0))),
inference(forward_demodulation,[],[f37997,f589]) ).
fof(f38089,plain,
! [X0,X1] : ld(X0,i(X1)) = mult(X1,rd(i(X1),mult(X1,X0))),
inference(forward_demodulation,[],[f38058,f30619]) ).
fof(f39367,plain,
! [X0,X1] : ld(ld(mult(X0,X0),X1),i(X0)) = mult(X0,rd(i(X0),mult(i(X0),X1))),
inference(superposition,[],[f38089,f11397]) ).
fof(f39386,plain,
! [X0,X1] : mult(X1,rd(i(X1),mult(X0,i(X1)))) = ld(rd(ld(X1,X0),X1),i(X1)),
inference(superposition,[],[f38089,f3566]) ).
fof(f39457,plain,
! [X0,X1] : ld(mult(mult(X1,X0),X1),i(i(X1))) = mult(i(X1),rd(i(i(X1)),mult(X0,X1))),
inference(superposition,[],[f38089,f4648]) ).
fof(f39458,plain,
! [X0,X1] : ld(mult(mult(X0,X0),X1),i(i(X0))) = mult(i(X0),rd(i(i(X0)),mult(X0,X1))),
inference(superposition,[],[f38089,f4644]) ).
fof(f39462,plain,
! [X0,X1] : ld(rd(X1,i(X0)),i(i(X0))) = mult(i(X0),rd(i(i(X0)),mult(mult(i(X0),X1),X0))),
inference(superposition,[],[f38089,f3612]) ).
fof(f39483,plain,
! [X0,X1] : ld(X1,ld(X0,i(X1))) = rd(i(X1),mult(X1,X0)),
inference(superposition,[],[f2,f38089]) ).
fof(f39615,plain,
! [X0,X1] : ld(rd(X1,i(X0)),i(i(X0))) = mult(i(X0),rd(i(i(X0)),ld(X0,mult(X1,X0)))),
inference(forward_demodulation,[],[f39462,f4336]) ).
fof(f39619,plain,
! [X0,X1] : ld(mult(mult(X0,X0),X1),X0) = mult(i(X0),rd(X0,mult(X0,X1))),
inference(forward_demodulation,[],[f39458,f589]) ).
fof(f39620,plain,
! [X0,X1] : ld(mult(mult(X1,X0),X1),X1) = mult(i(X1),rd(X1,mult(X0,X1))),
inference(forward_demodulation,[],[f39457,f589]) ).
fof(f39664,plain,
! [X0,X1] : rd(X1,X0) = mult(X1,rd(i(X1),mult(X0,i(X1)))),
inference(forward_demodulation,[],[f39386,f37157]) ).
fof(f39709,plain,
! [X0,X1] : ld(rd(X1,i(X0)),X0) = mult(i(X0),rd(X0,ld(X0,mult(X1,X0)))),
inference(forward_demodulation,[],[f39615,f589]) ).
fof(f39711,plain,
! [X0,X1] : rd(i(X1),X0) = mult(i(X1),rd(X1,mult(X0,X1))),
inference(forward_demodulation,[],[f39620,f36401]) ).
fof(f39740,plain,
! [X0,X1] : rd(X1,X0) = mult(X1,ld(mult(X1,X0),X1)),
inference(forward_demodulation,[],[f39664,f37106]) ).
fof(f39767,plain,
! [X0,X1] : ld(rd(X1,i(X0)),X0) = mult(i(X0),mult(i(X1),X0)),
inference(forward_demodulation,[],[f39709,f29324]) ).
fof(f39807,plain,
! [X0,X1] : ld(rd(X1,i(X0)),X0) = mult(ld(X0,i(X1)),X0),
inference(forward_demodulation,[],[f39767,f5349]) ).
fof(f39899,plain,
! [X0,X1] : rd(X1,mult(ld(X1,X0),X1)) = mult(X1,ld(rd(X0,i(X1)),X1)),
inference(superposition,[],[f39740,f3115]) ).
fof(f39980,plain,
! [X0,X1] : rd(i(X0),mult(ld(i(X0),X1),i(X0))) = mult(i(X0),ld(mult(mult(X0,mult(i(X0),X1)),i(X0)),i(X0))),
inference(superposition,[],[f39740,f421]) ).
fof(f39986,plain,
! [X0,X1] : rd(i(X1),rd(mult(X1,X0),X1)) = mult(i(X1),ld(rd(X0,X1),i(X1))),
inference(superposition,[],[f39740,f3878]) ).
fof(f40155,plain,
! [X0,X1] : mult(i(X1),ld(rd(X0,X1),i(X1))) = ld(mult(mult(X1,X1),X0),X1),
inference(forward_demodulation,[],[f39986,f37114]) ).
fof(f40159,plain,
! [X0,X1] : rd(i(X0),mult(ld(i(X0),X1),i(X0))) = mult(i(mult(X0,mult(i(X0),X1))),i(X0)),
inference(forward_demodulation,[],[f39980,f29799]) ).
fof(f40222,plain,
! [X0,X1] : rd(X1,mult(ld(X1,X0),X1)) = mult(X1,mult(ld(X1,i(X0)),X1)),
inference(forward_demodulation,[],[f39899,f39807]) ).
fof(f40269,plain,
! [X0,X1] : rd(i(X0),mult(ld(i(X0),X1),i(X0))) = mult(i(X0),ld(rd(X1,X0),i(X0))),
inference(forward_demodulation,[],[f40159,f30530]) ).
fof(f40304,plain,
! [X0,X1] : rd(X1,mult(ld(X1,X0),X1)) = rd(i(X0),i(X1)),
inference(forward_demodulation,[],[f40222,f3115]) ).
fof(f40328,plain,
! [X0,X1] : rd(i(X0),mult(ld(i(X0),X1),i(X0))) = ld(mult(mult(X0,X0),X1),X0),
inference(forward_demodulation,[],[f40269,f40155]) ).
fof(f40362,plain,
! [X0,X1] : ld(mult(mult(X0,X0),X1),X0) = rd(i(X1),i(i(X0))),
inference(forward_demodulation,[],[f40328,f40304]) ).
fof(f40381,plain,
! [X0,X1] : rd(i(X1),X0) = ld(mult(mult(X0,X0),X1),X0),
inference(forward_demodulation,[],[f40362,f589]) ).
fof(f40581,plain,
! [X0,X1] : rd(i(X0),mult(X0,mult(X0,X1))) = mult(i(X0),rd(X0,mult(X0,mult(X0,mult(X1,X0))))),
inference(superposition,[],[f39711,f30]) ).
fof(f40693,plain,
! [X0,X1] : mult(rd(X0,mult(X1,X0)),i(X0)) = mult(i(i(X0)),mult(rd(i(X0),X1),i(X0))),
inference(superposition,[],[f4648,f39711]) ).
fof(f40733,plain,
! [X0,X1] : mult(rd(X0,mult(X1,X0)),i(X0)) = mult(ld(i(X0),rd(i(X0),X1)),i(X0)),
inference(forward_demodulation,[],[f40693,f5349]) ).
fof(f40817,plain,
! [X0,X1] : rd(i(X0),mult(X0,mult(X0,X1))) = ld(mult(mult(X0,X0),mult(X0,mult(X1,X0))),X0),
inference(forward_demodulation,[],[f40581,f39619]) ).
fof(f40858,plain,
! [X0,X1] : i(mult(i(i(X0)),X1)) = mult(rd(X0,mult(X1,X0)),i(X0)),
inference(forward_demodulation,[],[f40733,f37967]) ).
fof(f40922,plain,
! [X0,X1] : rd(i(X0),mult(X0,mult(X0,X1))) = rd(i(mult(X0,mult(X1,X0))),X0),
inference(forward_demodulation,[],[f40817,f40381]) ).
fof(f40948,plain,
! [X0,X1] : i(mult(X0,X1)) = mult(rd(X0,mult(X1,X0)),i(X0)),
inference(forward_demodulation,[],[f40858,f589]) ).
fof(f40991,plain,
! [X0,X1] : ld(X0,ld(mult(X0,X1),i(X0))) = rd(i(mult(X0,mult(X1,X0))),X0),
inference(forward_demodulation,[],[f40922,f39483]) ).
fof(f41100,plain,
! [X0,X1] : i(mult(mult(X0,mult(i(X0),X1)),X0)) = mult(rd(mult(X0,mult(i(X0),X1)),ld(i(X0),X1)),i(mult(X0,mult(i(X0),X1)))),
inference(superposition,[],[f40948,f6302]) ).
fof(f41108,plain,
! [X0,X1] : i(mult(mult(mult(X1,X0),i(X0)),X0)) = mult(rd(mult(mult(X1,X0),i(X0)),mult(mult(X0,rd(X1,X0)),X0)),i(mult(mult(X1,X0),i(X0)))),
inference(superposition,[],[f40948,f442]) ).
fof(f41165,plain,
! [X0,X1] : i(mult(X0,mult(i(X0),X1))) = mult(rd(X0,ld(X0,mult(X1,X0))),i(X0)),
inference(superposition,[],[f40948,f4336]) ).
fof(f41170,plain,
! [X0,X1] : i(mult(X1,rd(X0,X1))) = mult(rd(X1,X0),i(X1)),
inference(superposition,[],[f40948,f3]) ).
fof(f41201,plain,
! [X0,X1] : i(mult(X1,i(mult(X0,X0)))) = mult(rd(X1,ld(mult(X0,X0),X1)),i(X1)),
inference(superposition,[],[f40948,f7177]) ).
fof(f41340,plain,
! [X0,X1] : i(mult(X1,i(mult(X0,X0)))) = mult(mult(X0,X0),i(X1)),
inference(forward_demodulation,[],[f41201,f573]) ).
fof(f41373,plain,
! [X0,X1] : i(mult(X0,mult(i(X0),X1))) = mult(mult(i(X1),X0),i(X0)),
inference(forward_demodulation,[],[f41165,f29324]) ).
fof(f41417,plain,
! [X0,X1] : i(mult(mult(X0,mult(i(X0),X1)),X0)) = mult(rd(mult(X0,mult(i(X0),X1)),mult(mult(X0,rd(X1,X0)),X0)),i(mult(X0,mult(i(X0),X1)))),
inference(forward_demodulation,[],[f41108,f4840]) ).
fof(f41422,plain,
! [X0,X1] : i(mult(X0,mult(i(X0),mult(X1,X0)))) = mult(rd(mult(X0,mult(i(X0),X1)),ld(i(X0),X1)),i(mult(X0,mult(i(X0),X1)))),
inference(forward_demodulation,[],[f41100,f1661]) ).
fof(f41465,plain,
! [X0,X1] : i(rd(X1,mult(X0,X0))) = mult(mult(X0,X0),i(X1)),
inference(forward_demodulation,[],[f41340,f7168]) ).
fof(f41490,plain,
! [X0,X1] : i(mult(X0,mult(i(X0),X1))) = mult(X0,mult(i(X0),i(X1))),
inference(forward_demodulation,[],[f41373,f4840]) ).
fof(f41516,plain,
! [X0,X1] : i(mult(mult(X0,mult(i(X0),X1)),X0)) = mult(rd(mult(X0,mult(i(X0),X1)),mult(mult(X0,X0),ld(X0,X1))),i(mult(X0,mult(i(X0),X1)))),
inference(forward_demodulation,[],[f41417,f17448]) ).
fof(f41519,plain,
! [X0,X1] : i(rd(X1,i(X0))) = mult(rd(mult(X0,mult(i(X0),X1)),ld(i(X0),X1)),i(mult(X0,mult(i(X0),X1)))),
inference(forward_demodulation,[],[f41422,f4673]) ).
fof(f41580,plain,
! [X0,X1] : i(mult(mult(X0,mult(i(X0),X1)),X0)) = mult(rd(mult(X0,mult(i(X0),X1)),mult(mult(X0,X0),ld(X0,X1))),mult(X0,mult(i(X0),i(X1)))),
inference(forward_demodulation,[],[f41516,f41490]) ).
fof(f41583,plain,
! [X0,X1] : i(rd(X1,i(X0))) = mult(rd(mult(X0,mult(i(X0),X1)),ld(i(X0),X1)),mult(X0,mult(i(X0),i(X1)))),
inference(forward_demodulation,[],[f41519,f41490]) ).
fof(f41620,plain,
! [X0,X1] : i(mult(mult(X0,mult(i(X0),X1)),X0)) = mult(rd(mult(X0,mult(i(X0),X1)),ld(i(X0),X1)),mult(X0,mult(i(X0),i(X1)))),
inference(forward_demodulation,[],[f41580,f10728]) ).
fof(f41647,plain,
! [X0,X1] : i(rd(X1,i(X0))) = i(mult(mult(X0,mult(i(X0),X1)),X0)),
inference(forward_demodulation,[],[f41620,f41583]) ).
fof(f41662,plain,
! [X0,X1] : i(rd(X1,i(X0))) = i(mult(X0,mult(i(X0),mult(X1,X0)))),
inference(forward_demodulation,[],[f41647,f1661]) ).
fof(f41672,plain,
! [X0,X1] : i(rd(X1,i(X0))) = mult(X0,mult(i(X0),i(mult(X1,X0)))),
inference(forward_demodulation,[],[f41662,f41490]) ).
fof(f41704,plain,
! [X0,X1] : i(rd(X1,X0)) = mult(i(X0),mult(X0,i(mult(X1,i(X0))))),
inference(superposition,[],[f41672,f589]) ).
fof(f41742,plain,
! [X0,X1] : mult(X0,mult(i(X0),i(mult(i(X0),X1)))) = i(rd(ld(X0,rd(X1,X0)),i(X0))),
inference(superposition,[],[f41672,f5509]) ).
fof(f41753,plain,
! [X0,X1] : i(rd(mult(X0,X1),i(i(X0)))) = mult(i(X0),mult(i(i(X0)),i(mult(X0,rd(X1,X0))))),
inference(superposition,[],[f41672,f3423]) ).
fof(f41899,plain,
! [X0,X1] : ld(X1,mult(mult(i(i(X1)),i(mult(X0,i(X1)))),X1)) = mult(i(rd(X0,i(i(X1)))),X1),
inference(superposition,[],[f4336,f41672]) ).
fof(f41924,plain,
! [X0,X1] : mult(i(rd(X0,X1)),X1) = ld(X1,mult(mult(X1,i(mult(X0,i(X1)))),X1)),
inference(forward_demodulation,[],[f41899,f589]) ).
fof(f42038,plain,
! [X0,X1] : i(rd(mult(X0,X1),i(i(X0)))) = mult(i(X0),mult(i(i(X0)),mult(rd(X0,X1),i(X0)))),
inference(forward_demodulation,[],[f41753,f41170]) ).
fof(f42044,plain,
! [X0,X1] : mult(X0,mult(i(X0),i(mult(i(X0),X1)))) = i(ld(X0,mult(rd(X1,X0),X0))),
inference(forward_demodulation,[],[f41742,f1900]) ).
fof(f42069,plain,
! [X0,X1] : i(rd(X1,X0)) = mult(X0,mult(i(X0),i(mult(X1,i(X0))))),
inference(forward_demodulation,[],[f41704,f4294]) ).
fof(f42080,plain,
! [X0,X1] : mult(i(rd(X0,X1)),X1) = rd(i(mult(X0,i(X1))),i(X1)),
inference(forward_demodulation,[],[f41924,f1589]) ).
fof(f42167,plain,
! [X0,X1] : i(rd(mult(X0,X1),i(i(X0)))) = rd(rd(X0,X1),i(i(X0))),
inference(forward_demodulation,[],[f42038,f4673]) ).
fof(f42172,plain,
! [X0,X1] : mult(X0,mult(i(X0),i(mult(i(X0),X1)))) = i(mult(ld(X0,X1),ld(X0,X0))),
inference(forward_demodulation,[],[f42044,f19843]) ).
fof(f42195,plain,
! [X0,X1] : mult(X1,ld(X0,X1)) = rd(i(mult(X0,i(X1))),i(X1)),
inference(forward_demodulation,[],[f42080,f30115]) ).
fof(f42259,plain,
! [X0,X1] : i(rd(mult(X0,X1),X0)) = rd(rd(X0,X1),X0),
inference(forward_demodulation,[],[f42167,f589]) ).
fof(f42264,plain,
! [X0,X1] : mult(X0,mult(i(X0),i(mult(i(X0),X1)))) = i(mult(ld(X0,X1),unit)),
inference(forward_demodulation,[],[f42172,f125]) ).
fof(f42326,plain,
! [X0,X1] : i(ld(X0,X1)) = mult(X0,mult(i(X0),i(mult(i(X0),X1)))),
inference(forward_demodulation,[],[f42264,f5]) ).
fof(f42516,plain,
! [X0,X1] : i(ld(X0,mult(ld(i(X0),X1),i(X0)))) = mult(X0,mult(i(X0),i(mult(mult(X0,mult(i(X0),X1)),i(X0))))),
inference(superposition,[],[f42326,f421]) ).
fof(f42799,plain,
! [X0,X1] : i(ld(X0,mult(ld(i(X0),X1),i(X0)))) = i(rd(mult(X0,mult(i(X0),X1)),X0)),
inference(forward_demodulation,[],[f42516,f42069]) ).
fof(f42922,plain,
! [X0,X1] : rd(rd(X0,mult(i(X0),X1)),X0) = i(ld(X0,mult(ld(i(X0),X1),i(X0)))),
inference(forward_demodulation,[],[f42799,f42259]) ).
fof(f43010,plain,
! [X0,X1] : rd(rd(X0,mult(i(X0),X1)),X0) = i(rd(ld(X0,ld(i(X0),X1)),X0)),
inference(forward_demodulation,[],[f42922,f3793]) ).
fof(f43079,plain,
! [X0,X1] : rd(rd(X0,mult(i(X0),X1)),X0) = i(rd(mult(mult(X1,i(X0)),X0),X0)),
inference(forward_demodulation,[],[f43010,f4827]) ).
fof(f43126,plain,
! [X0,X1] : i(mult(X1,i(X0))) = rd(rd(X0,mult(i(X0),X1)),X0),
inference(forward_demodulation,[],[f43079,f4]) ).
fof(f45603,plain,
! [X0,X1] : mult(X0,ld(mult(i(i(X0)),mult(i(X0),X1)),X0)) = rd(i(mult(i(X0),mult(ld(i(X0),X1),i(X0)))),i(X0)),
inference(superposition,[],[f42195,f417]) ).
fof(f45697,plain,
! [X0,X1] : mult(X0,ld(mult(i(i(X0)),mult(i(X0),X1)),X0)) = ld(i(X0),ld(mult(i(X0),ld(i(X0),X1)),i(i(X0)))),
inference(forward_demodulation,[],[f45603,f40991]) ).
fof(f45765,plain,
! [X0,X1] : mult(X0,ld(mult(X0,mult(i(X0),X1)),X0)) = ld(i(X0),ld(mult(i(X0),ld(i(X0),X1)),X0)),
inference(forward_demodulation,[],[f45697,f589]) ).
fof(f45819,plain,
! [X0,X1] : mult(X0,ld(mult(X0,mult(i(X0),X1)),X0)) = ld(i(X0),ld(X1,X0)),
inference(forward_demodulation,[],[f45765,f1]) ).
fof(f45857,plain,
! [X0,X1] : rd(X0,mult(i(X0),X1)) = ld(i(X0),ld(X1,X0)),
inference(forward_demodulation,[],[f45819,f39740]) ).
fof(f46012,plain,
! [X0,X1] : i(mult(i(mult(X1,X1)),i(X0))) = rd(rd(X0,rd(i(X0),mult(X1,X1))),X0),
inference(superposition,[],[f43126,f7168]) ).
fof(f46071,plain,
! [X0,X1] : i(mult(i(mult(X1,X1)),i(X0))) = rd(mult(mult(X0,mult(X1,X1)),X0),X0),
inference(forward_demodulation,[],[f46012,f37131]) ).
fof(f46158,plain,
! [X0,X1] : mult(X0,mult(X1,X1)) = i(mult(i(mult(X1,X1)),i(X0))),
inference(forward_demodulation,[],[f46071,f4]) ).
fof(f46230,plain,
! [X0,X1] : mult(X0,mult(X1,X1)) = i(mult(i(X1),ld(X1,i(X0)))),
inference(forward_demodulation,[],[f46158,f3926]) ).
fof(f46287,plain,
! [X0,X1] : mult(X0,mult(X1,X1)) = i(ld(mult(X1,X1),i(X0))),
inference(forward_demodulation,[],[f46230,f7293]) ).
fof(f47733,plain,
! [X0,X1] : rd(X0,rd(X1,i(X0))) = mult(X0,rd(mult(rd(i(X0),X1),i(i(X0))),X0)),
inference(superposition,[],[f37598,f41170]) ).
fof(f47912,plain,
! [X0,X1] : rd(X0,rd(X1,i(X0))) = mult(X0,rd(mult(rd(i(X0),X1),X0),X0)),
inference(forward_demodulation,[],[f47733,f589]) ).
fof(f47984,plain,
! [X0,X1] : rd(X0,rd(X1,i(X0))) = mult(X0,rd(i(X0),X1)),
inference(forward_demodulation,[],[f47912,f4]) ).
fof(f48127,plain,
! [X0,X1] : rd(X0,mult(X0,ld(X1,X0))) = mult(X0,rd(i(X0),i(mult(X1,i(X0))))),
inference(superposition,[],[f47984,f42195]) ).
fof(f48163,plain,
! [X0,X1] : i(rd(X0,X1)) = mult(X0,rd(i(X0),i(mult(X1,i(X0))))),
inference(forward_demodulation,[],[f48127,f24452]) ).
fof(f48311,plain,
! [X0,X1] : i(rd(X1,i(mult(X0,X0)))) = mult(X1,rd(i(X1),i(ld(mult(X0,X0),i(X1))))),
inference(superposition,[],[f48163,f7177]) ).
fof(f48473,plain,
! [X0,X1] : i(rd(X1,i(mult(X0,X0)))) = mult(X1,rd(i(X1),mult(X1,mult(X0,X0)))),
inference(forward_demodulation,[],[f48311,f46287]) ).
fof(f48577,plain,
! [X0,X1] : ld(mult(X0,X0),i(X1)) = i(rd(X1,i(mult(X0,X0)))),
inference(forward_demodulation,[],[f48473,f38089]) ).
fof(f48660,plain,
! [X0,X1] : ld(mult(X0,X0),i(X1)) = i(mult(X1,mult(X0,X0))),
inference(forward_demodulation,[],[f48577,f7642]) ).
fof(f51720,plain,
! [X0,X1] : mult(i(i(rd(X0,X1))),X1) = mult(X1,rd(i(X1),mult(i(X1),i(mult(X0,i(X1)))))),
inference(superposition,[],[f37127,f42069]) ).
fof(f52129,plain,
! [X0,X1] : mult(i(i(rd(X0,X1))),X1) = ld(ld(mult(X1,X1),i(mult(X0,i(X1)))),i(X1)),
inference(forward_demodulation,[],[f51720,f39367]) ).
fof(f52298,plain,
! [X0,X1] : mult(i(i(rd(X0,X1))),X1) = ld(i(mult(mult(X0,i(X1)),mult(X1,X1))),i(X1)),
inference(forward_demodulation,[],[f52129,f48660]) ).
fof(f52406,plain,
! [X0,X1] : ld(i(mult(X0,X1)),i(X1)) = mult(i(i(rd(X0,X1))),X1),
inference(forward_demodulation,[],[f52298,f15500]) ).
fof(f52473,plain,
! [X0,X1] : mult(rd(X0,X1),X1) = ld(i(mult(X0,X1)),i(X1)),
inference(forward_demodulation,[],[f52406,f589]) ).
fof(f52514,plain,
! [X0,X1] : ld(i(mult(X0,X1)),i(X1)) = X0,
inference(forward_demodulation,[],[f52473,f3]) ).
fof(f52716,plain,
! [X0,X1] : rd(X0,X1) = ld(i(rd(X0,mult(X1,X1))),i(i(X1))),
inference(superposition,[],[f52514,f15656]) ).
fof(f52776,plain,
! [X0,X1] : i(mult(X0,X1)) = rd(i(X1),X0),
inference(superposition,[],[f573,f52514]) ).
fof(f52852,plain,
! [X0,X1] : rd(X0,X1) = ld(i(rd(X0,mult(X1,X1))),X1),
inference(forward_demodulation,[],[f52716,f589]) ).
fof(f52980,plain,
! [X0,X1] : rd(X0,X1) = ld(mult(mult(X1,X1),i(X0)),X1),
inference(forward_demodulation,[],[f52852,f41465]) ).
fof(f53033,plain,
! [X0,X1] : rd(X0,X1) = rd(i(i(X0)),X1),
inference(forward_demodulation,[],[f52980,f40381]) ).
fof(f53068,plain,
! [X0,X1] : rd(X0,X1) = i(mult(X1,i(X0))),
inference(forward_demodulation,[],[f53033,f52776]) ).
fof(f53146,plain,
! [X0,X1] : i(ld(i(i(X0)),X1)) = rd(X0,mult(i(X0),rd(X1,i(X0)))),
inference(superposition,[],[f53068,f11616]) ).
fof(f53451,plain,
! [X0,X1] : i(ld(i(i(X0)),X1)) = ld(i(X0),ld(rd(X1,i(X0)),X0)),
inference(forward_demodulation,[],[f53146,f45857]) ).
fof(f53554,plain,
! [X0,X1] : i(ld(i(i(X0)),X1)) = ld(i(X0),mult(ld(X0,i(X1)),X0)),
inference(forward_demodulation,[],[f53451,f39807]) ).
fof(f53623,plain,
! [X0,X1] : i(ld(i(i(X0)),X1)) = mult(mult(X0,ld(X0,i(X1))),X0),
inference(forward_demodulation,[],[f53554,f6418]) ).
fof(f53665,plain,
! [X0,X1] : mult(i(X1),X0) = i(ld(i(i(X0)),X1)),
inference(forward_demodulation,[],[f53623,f1]) ).
fof(f53695,plain,
! [X0,X1] : i(ld(X0,X1)) = mult(i(X1),X0),
inference(forward_demodulation,[],[f53665,f589]) ).
fof(f53774,plain,
! [X0,X1] : i(X0) = mult(i(i(X1)),i(mult(X0,X1))),
inference(superposition,[],[f53695,f52514]) ).
fof(f53974,plain,
! [X0,X1] : i(X0) = mult(X1,i(mult(X0,X1))),
inference(forward_demodulation,[],[f53774,f589]) ).
fof(f54350,plain,
i(b) != i(b),
inference(superposition,[],[f13,f53974]) ).
fof(f54351,plain,
$false,
inference(trivial_inequality_removal,[],[f54350]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP701-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 % Computer : n005.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 10:36:17 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.46 Running first-order theorem proving
% 0.13/0.46 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 47.05/7.57 % (3799172)Detected a unit-equality problem, will run specialized UEQ schedule.
% 47.05/7.57 % (3799177)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=3728143412:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 47.05/7.57 % (3799179)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3782354031:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 47.05/7.57 % (3799183)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2088518586:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 47.05/7.57 % (3799182)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3263097173:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 47.05/7.57 % (3799181)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3863349063:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 47.05/7.57 % (3799178)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2154598031:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 47.05/7.57 % (3799180)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=273163570:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 47.05/7.57 % (3799180)Instruction limit reached!
% 47.05/7.57 % (3799180)------------------------------
% 47.05/7.57 % (3799180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.05/7.57 % (3799180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.05/7.57 % (3799180)CaDiCaL version: 2.1.3
% 47.05/7.57 % (3799180)Termination reason: Instruction limit
% 47.05/7.57 % (3799180)Termination phase: Saturation
% 47.05/7.57 % (3799180)Time elapsed: 0.133 s
% 47.05/7.57 % (3799180)Peak memory usage: 89 MB
% 47.05/7.57 % (3799180)Instructions burned: 136 (million)
% 47.05/7.57 % (3799181)Instruction limit reached!
% 47.05/7.57 % (3799181)------------------------------
% 47.05/7.57 % (3799181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.05/7.57 % (3799181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.05/7.57 % (3799181)CaDiCaL version: 2.1.3
% 47.05/7.57 % (3799181)Termination reason: Instruction limit
% 47.05/7.57 % (3799181)Termination phase: Saturation
% 47.05/7.57 % (3799181)Time elapsed: 0.170 s
% 47.05/7.57 % (3799181)Peak memory usage: 89 MB
% 47.05/7.57 % (3799181)Instructions burned: 181 (million)
% 47.05/7.57 % (3799182)Instruction limit reached!
% 47.05/7.57 % (3799182)------------------------------
% 47.05/7.57 % (3799182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.05/7.57 % (3799182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.05/7.57 % (3799182)CaDiCaL version: 2.1.3
% 47.05/7.57 % (3799182)Termination reason: Instruction limit
% 47.05/7.57 % (3799182)Termination phase: Saturation
% 47.05/7.57 % (3799182)Time elapsed: 0.263 s
% 47.05/7.57 % (3799182)Peak memory usage: 90 MB
% 47.05/7.57 % (3799182)Instructions burned: 257 (million)
% 47.05/7.57 % (3799191)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1217411035:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2995 on theBenchmark for (2995ds/2051Mi)
% 47.05/7.57 % (3799192)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1806362097:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 47.05/7.57 % (3799193)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2954835449:i=215:ep=RSTC_2994 on theBenchmark for (2994ds/215Mi)
% 47.05/7.57 % (3799193)Instruction limit reached!
% 47.05/7.57 % (3799193)------------------------------
% 47.05/7.57 % (3799193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.05/7.57 % (3799193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.05/7.57 % (3799193)CaDiCaL version: 2.1.3
% 47.05/7.57 % (3799193)Termination reason: Instruction limit
% 47.05/7.57 % (3799193)Termination phase: Saturation
% 47.05/7.57 % (3799193)Time elapsed: 0.205 s
% 47.05/7.57 % (3799193)Peak memory usage: 90 MB
% 47.05/7.57 % (3799193)Instructions burned: 215 (million)
% 47.05/7.57 % (3799197)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=1393671795:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2989 on theBenchmark for (2989ds/317Mi)
% 47.05/7.57 % (3799183)Instruction limit reached!
% 47.05/7.57 % (3799183)------------------------------
% 47.05/7.57 % (3799183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.05/7.57 % (3799183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.05/7.57 % (3799183)CaDiCaL version: 2.1.3
% 47.05/7.57 % (3799183)Termination reason: Instruction limit
% 47.05/7.57 % (3799183)Termination phase: Saturation
% 47.05/7.57 % (3799183)Time elapsed: 1.074 s
% 47.05/7.57 % (3799183)Peak memory usage: 98 MB
% 47.05/7.57 % (3799183)Instructions burned: 1189 (million)
% 47.05/7.57 % (3799199)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=999931573:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/12125Mi)
% 47.05/7.57 % (3799197)Instruction limit reached!
% 47.05/7.57 % (3799197)------------------------------
% 47.05/7.57 % (3799197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.05/7.57 % (3799197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.05/7.57 % (3799197)CaDiCaL version: 2.1.3
% 47.05/7.57 % (3799197)Termination reason: Instruction limit
% 47.05/7.57 % (3799197)Termination phase: Saturation
% 47.05/7.57 % (3799197)Time elapsed: 0.325 s
% 47.05/7.57 % (3799197)Peak memory usage: 94 MB
% 47.05/7.57 % (3799197)Instructions burned: 317 (million)
% 47.05/7.57 % (3799201)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2988988122:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2983 on theBenchmark for (2983ds/2836Mi)
% 47.05/7.57 % (3799191)Instruction limit reached!
% 47.05/7.57 % (3799191)------------------------------
% 47.05/7.57 % (3799191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.05/7.57 % (3799191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.05/7.57 % (3799191)CaDiCaL version: 2.1.3
% 47.05/7.57 % (3799191)Termination reason: Instruction limit
% 47.05/7.57 % (3799191)Termination phase: Saturation
% 47.05/7.57 % (3799191)Time elapsed: 2.233 s
% 47.05/7.57 % (3799191)Peak memory usage: 138 MB
% 47.05/7.57 % (3799191)Instructions burned: 2051 (million)
% 47.05/7.57 % (3799206)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=886036456:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2970 on theBenchmark for (2970ds/14534Mi)
% 47.05/7.57 % (3799201)Instruction limit reached!
% 47.05/7.57 % (3799201)------------------------------
% 47.05/7.57 % (3799201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.05/7.57 % (3799201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.05/7.57 % (3799201)CaDiCaL version: 2.1.3
% 47.05/7.57 % (3799201)Termination reason: Instruction limit
% 47.05/7.57 % (3799201)Termination phase: Saturation
% 47.05/7.57 % (3799201)Time elapsed: 3.180 s
% 47.05/7.57 % (3799201)Peak memory usage: 122 MB
% 47.05/7.57 % (3799201)Instructions burned: 2836 (million)
% 47.05/7.57 % (3799211)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=580610924:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2948 on theBenchmark for (2948ds/11832Mi)
% 47.05/7.57 % (3799192)Instruction limit reached!
% 47.05/7.57 % (3799192)------------------------------
% 47.05/7.57 % (3799192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.05/7.57 % (3799192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.05/7.57 % (3799192)CaDiCaL version: 2.1.3
% 47.05/7.57 % (3799192)Termination reason: Instruction limit
% 47.05/7.57 % (3799192)Termination phase: Saturation
% 47.05/7.57 % (3799192)Time elapsed: 5.180 s
% 47.05/7.57 % (3799192)Peak memory usage: 167 MB
% 47.05/7.57 % (3799192)Instructions burned: 4948 (million)
% 47.05/7.57 % (3799216)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=2291963175:i=2279:fgj=on:bd=all_2941 on theBenchmark for (2941ds/2279Mi)
% 47.05/7.57 % (3799178)First to succeed.
% 47.05/7.57 % (3799178)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3799172"
% 47.05/7.57 % (3799178)Refutation found. Thanks to Tanya!
% 47.05/7.57 % SZS status Unsatisfiable for theBenchmark
% 47.05/7.57 % SZS output start Proof for theBenchmark
% See solution above
% 47.62/7.77 % (3799178)------------------------------
% 47.62/7.77 % (3799178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.62/7.77 % (3799178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.62/7.77 % (3799178)CaDiCaL version: 2.1.3
% 47.62/7.77 % (3799178)Termination reason: Refutation
% 47.62/7.77 % (3799178)Time elapsed: 5.892 s
% 47.62/7.77 % (3799178)Peak memory usage: 175 MB
% 47.62/7.77 % (3799178)Instructions burned: 5780 (million)
% 47.62/7.77 % (3799178)------------------------------
% 47.62/7.77 % (3799178)------------------------------
% 47.62/7.77 % (3799172)Success in time 6.613 s
% 47.62/7.77 % Vampire exiting
%------------------------------------------------------------------------------