%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP654-10 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:21 AM UTC 2026
% Result : Unsatisfiable 50.22s 12.32s
% Output : Refutation 81.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 83
% Number of leaves : 6
% Syntax : Number of formulae : 528 ( 528 unt; 0 def)
% Number of atoms : 528 ( 527 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 11 ( 11 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 0 con; 1-2 aty)
% Number of variables : 1295 (1295 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f01) ).
fof(f2,axiom,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f04) ).
fof(f5,axiom,
! [X2,X0,X1] : mult(X0,mult(X1,mult(X0,X2))) = mult(mult(mult(X0,X1),X0),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f05) ).
fof(f6,negated_conjecture,
! [X0] : tuple(mult(X0,x1(X0)),mult(x1_2(X0),X0)) != tuple(x1(X0),x1_2(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f7,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f2,f3]) ).
fof(f8,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f9,plain,
! [X2,X0,X1] : mult(rd(X0,X1),mult(X1,mult(rd(X0,X1),X2))) = mult(mult(X0,rd(X0,X1)),X2),
inference(superposition,[],[f5,f3]) ).
fof(f10,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),mult(X1,X2))) = mult(mult(X0,X1),X2),
inference(superposition,[],[f5,f1]) ).
fof(f11,plain,
! [X2,X3,X0,X1] : mult(mult(mult(X0,X1),X0),mult(X2,mult(mult(mult(X0,X1),X0),X3))) = mult(mult(mult(X0,mult(X1,mult(X0,X2))),mult(mult(X0,X1),X0)),X3),
inference(superposition,[],[f5,f5]) ).
fof(f14,plain,
! [X2,X0,X1] : mult(mult(X0,X1),X0) = rd(mult(X0,mult(X1,mult(X0,X2))),X2),
inference(superposition,[],[f4,f5]) ).
fof(f15,plain,
! [X2,X0,X1] : ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2)))) = X2,
inference(superposition,[],[f2,f5]) ).
fof(f17,plain,
! [X0,X1] : tuple(x1(mult(mult(X0,X1),X0)),x1_2(mult(mult(X0,X1),X0))) != tuple(mult(X0,mult(X1,mult(X0,x1(mult(mult(X0,X1),X0))))),mult(x1_2(mult(mult(X0,X1),X0)),mult(mult(X0,X1),X0))),
inference(superposition,[],[f6,f5]) ).
fof(f18,plain,
! [X2,X3,X0,X1] : mult(mult(mult(X0,mult(X1,mult(X0,X2))),mult(mult(X0,X1),X0)),X3) = mult(X0,mult(X1,mult(X0,mult(X2,mult(mult(mult(X0,X1),X0),X3))))),
inference(forward_demodulation,[],[f11,f5]) ).
fof(f19,plain,
! [X2,X3,X0,X1] : mult(mult(mult(X0,mult(X1,mult(X0,X2))),mult(mult(X0,X1),X0)),X3) = mult(X0,mult(X1,mult(X0,mult(X2,mult(X0,mult(X1,mult(X0,X3))))))),
inference(forward_demodulation,[],[f18,f5]) ).
fof(f20,plain,
! [X2,X0,X1] : mult(mult(rd(X0,X1),X2),rd(X0,X1)) = rd(mult(rd(X0,X1),mult(X2,X0)),X1),
inference(superposition,[],[f14,f3]) ).
fof(f21,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X1) = rd(mult(X1,mult(X2,X0)),ld(X1,X0)),
inference(superposition,[],[f14,f1]) ).
fof(f23,plain,
! [X2,X0,X1] : mult(mult(X1,rd(X0,mult(X1,X2))),X1) = rd(mult(X1,X0),X2),
inference(superposition,[],[f14,f3]) ).
fof(f31,plain,
! [X2,X0,X1] : mult(mult(X1,rd(X0,X2)),X1) = rd(mult(X1,X0),ld(X1,X2)),
inference(superposition,[],[f21,f3]) ).
fof(f45,plain,
! [X2,X0,X1] : mult(mult(X1,rd(ld(X1,X0),X2)),X1) = rd(X0,ld(X1,X2)),
inference(superposition,[],[f31,f1]) ).
fof(f111,plain,
! [X2,X0,X1] : mult(mult(X2,rd(X0,X1)),X1) = mult(rd(X0,X1),mult(ld(rd(X0,X1),X2),X0)),
inference(superposition,[],[f10,f3]) ).
fof(f112,plain,
! [X2,X0,X1] : mult(mult(X2,X1),ld(X1,X0)) = mult(X1,mult(ld(X1,X2),X0)),
inference(superposition,[],[f10,f1]) ).
fof(f119,plain,
! [X2,X0,X1] : mult(mult(ld(X1,X0),X1),ld(X1,X0)) = rd(mult(ld(X1,X0),mult(mult(X0,X1),X2)),mult(X1,X2)),
inference(superposition,[],[f14,f10]) ).
fof(f120,plain,
! [X2,X0,X1] : mult(ld(X1,X0),mult(X1,X2)) = ld(X1,mult(mult(X0,X1),X2)),
inference(superposition,[],[f2,f10]) ).
fof(f138,plain,
! [X2,X0,X1] : rd(mult(ld(X1,X0),mult(mult(X0,X1),X2)),mult(X1,X2)) = mult(X1,mult(ld(X1,ld(X1,X0)),X0)),
inference(backward_demodulation,[],[f119,f112]) ).
fof(f144,plain,
! [X2,X3,X0,X1] : mult(ld(mult(mult(X0,X1),X0),X3),mult(X0,mult(X1,mult(X0,X2)))) = ld(mult(mult(X0,X1),X0),mult(mult(X3,mult(mult(X0,X1),X0)),X2)),
inference(superposition,[],[f120,f5]) ).
fof(f147,plain,
! [X2,X0,X1] : mult(ld(rd(X0,X1),X2),X0) = ld(rd(X0,X1),mult(mult(X2,rd(X0,X1)),X1)),
inference(superposition,[],[f120,f3]) ).
fof(f151,plain,
! [X2,X0,X1] : ld(X0,X1) = rd(ld(X0,mult(mult(X1,X0),X2)),mult(X0,X2)),
inference(superposition,[],[f4,f120]) ).
fof(f162,plain,
! [X2,X0,X1] : mult(ld(X1,X0),mult(ld(ld(X1,X0),X1),X2)) = mult(X0,ld(ld(X1,X0),X2)),
inference(superposition,[],[f112,f1]) ).
fof(f166,plain,
! [X2,X3,X0,X1] : mult(X0,mult(ld(X0,mult(X0,rd(X1,mult(X0,X2)))),X3)) = mult(rd(mult(X0,X1),X2),ld(X0,X3)),
inference(superposition,[],[f112,f23]) ).
fof(f186,plain,
! [X2,X3,X0,X1] : mult(rd(mult(X0,X1),X2),ld(X0,X3)) = mult(X0,mult(rd(X1,mult(X0,X2)),X3)),
inference(forward_demodulation,[],[f166,f2]) ).
fof(f195,plain,
! [X2,X0,X1] : ld(X1,rd(X0,X1)) = rd(ld(X1,mult(X0,X2)),mult(X1,X2)),
inference(superposition,[],[f151,f3]) ).
fof(f235,plain,
! [X2,X0,X1] : ld(X1,rd(X2,X1)) = rd(ld(X1,X0),mult(X1,ld(X2,X0))),
inference(superposition,[],[f195,f1]) ).
fof(f241,plain,
! [X2,X0,X1] : rd(ld(X1,X0),mult(X1,X2)) = ld(X1,rd(rd(X0,X2),X1)),
inference(superposition,[],[f195,f3]) ).
fof(f242,plain,
! [X0,X1] : ld(X1,rd(X1,X1)) = rd(X0,mult(X1,X0)),
inference(superposition,[],[f195,f2]) ).
fof(f244,plain,
! [X2,X0,X1] : ld(X1,rd(X2,X1)) = rd(ld(X1,mult(X2,ld(X1,X0))),X0),
inference(superposition,[],[f195,f1]) ).
fof(f250,plain,
! [X2,X0,X1] : ld(rd(X0,X1),rd(X2,rd(X0,X1))) = rd(ld(rd(X0,X1),mult(X2,X1)),X0),
inference(superposition,[],[f195,f3]) ).
fof(f273,plain,
! [X2,X0,X1] : rd(X0,mult(X1,X0)) = rd(X2,mult(X1,X2)),
inference(superposition,[],[f242,f242]) ).
fof(f274,plain,
! [X0,X1] : ld(X1,rd(X1,X1)) = rd(ld(X1,X0),X0),
inference(superposition,[],[f242,f1]) ).
fof(f283,plain,
! [X0,X1] : rd(X1,X1) = mult(X1,rd(X0,mult(X1,X0))),
inference(superposition,[],[f1,f242]) ).
fof(f285,plain,
! [X0,X1] : mult(X0,X1) = ld(ld(X0,rd(X0,X0)),X1),
inference(superposition,[],[f7,f242]) ).
fof(f300,plain,
! [X2,X0,X1] : rd(ld(X0,X1),X1) = rd(X2,mult(X0,X2)),
inference(superposition,[],[f242,f274]) ).
fof(f301,plain,
! [X0,X1] : mult(X0,rd(ld(X0,X1),X1)) = rd(X0,X0),
inference(superposition,[],[f1,f274]) ).
fof(f308,plain,
! [X0,X1] : ld(X0,X1) = mult(ld(X0,rd(X0,X0)),X1),
inference(superposition,[],[f3,f274]) ).
fof(f316,plain,
! [X2,X0,X1] : ld(X0,X2) = mult(rd(ld(X0,X1),X1),X2),
inference(superposition,[],[f308,f274]) ).
fof(f317,plain,
! [X2,X0,X1] : ld(X1,X2) = mult(rd(X0,mult(X1,X0)),X2),
inference(superposition,[],[f308,f242]) ).
fof(f322,plain,
! [X2,X0,X1] : mult(ld(X0,rd(X0,X0)),mult(X1,mult(ld(X0,rd(X0,X0)),X2))) = mult(mult(ld(X0,X1),ld(X0,rd(X0,X0))),X2),
inference(superposition,[],[f5,f308]) ).
fof(f329,plain,
! [X2,X0,X1] : ld(ld(X0,rd(X0,X0)),rd(X2,ld(X0,rd(X0,X0)))) = rd(ld(ld(X0,rd(X0,X0)),mult(X2,X1)),ld(X0,X1)),
inference(superposition,[],[f195,f308]) ).
fof(f334,plain,
! [X2,X0,X1] : mult(mult(ld(X0,rd(X0,X0)),X1),ld(X0,rd(X0,X0))) = rd(ld(X0,mult(X1,mult(ld(X0,rd(X0,X0)),X2))),X2),
inference(superposition,[],[f14,f308]) ).
fof(f340,plain,
! [X2,X0,X1] : rd(ld(X0,mult(X1,ld(X0,X2))),X2) = mult(mult(ld(X0,rd(X0,X0)),X1),ld(X0,rd(X0,X0))),
inference(forward_demodulation,[],[f334,f308]) ).
fof(f343,plain,
! [X2,X0,X1] : ld(ld(X0,rd(X0,X0)),rd(X2,ld(X0,rd(X0,X0)))) = rd(mult(X0,mult(X2,X1)),ld(X0,X1)),
inference(forward_demodulation,[],[f329,f285]) ).
fof(f348,plain,
! [X2,X0,X1] : mult(mult(ld(X0,X1),ld(X0,rd(X0,X0))),X2) = ld(X0,mult(X1,mult(ld(X0,rd(X0,X0)),X2))),
inference(forward_demodulation,[],[f322,f308]) ).
fof(f355,plain,
! [X2,X0,X1] : rd(ld(X0,mult(X1,ld(X0,X2))),X2) = mult(ld(X0,X1),ld(X0,rd(X0,X0))),
inference(forward_demodulation,[],[f340,f308]) ).
fof(f357,plain,
! [X2,X0,X1] : ld(ld(X0,rd(X0,X0)),rd(X2,ld(X0,rd(X0,X0)))) = mult(mult(X0,rd(mult(X2,X1),X1)),X0),
inference(forward_demodulation,[],[f343,f31]) ).
fof(f362,plain,
! [X2,X0,X1] : ld(X0,mult(X1,ld(X0,X2))) = mult(mult(ld(X0,X1),ld(X0,rd(X0,X0))),X2),
inference(forward_demodulation,[],[f348,f308]) ).
fof(f363,plain,
! [X0,X1] : ld(X0,rd(X1,X0)) = mult(ld(X0,X1),ld(X0,rd(X0,X0))),
inference(forward_demodulation,[],[f355,f244]) ).
fof(f364,plain,
! [X2,X0] : mult(mult(X0,X2),X0) = ld(ld(X0,rd(X0,X0)),rd(X2,ld(X0,rd(X0,X0)))),
inference(forward_demodulation,[],[f357,f4]) ).
fof(f369,plain,
! [X2,X0,X1] : mult(ld(X0,rd(X1,X0)),X2) = ld(X0,mult(X1,ld(X0,X2))),
inference(backward_demodulation,[],[f362,f363]) ).
fof(f371,plain,
! [X2,X0] : mult(mult(X0,X2),X0) = mult(X0,rd(X2,ld(X0,rd(X0,X0)))),
inference(forward_demodulation,[],[f364,f285]) ).
fof(f485,plain,
! [X2,X0,X1] : rd(X0,X1) = rd(X2,mult(rd(X1,X0),X2)),
inference(superposition,[],[f300,f7]) ).
fof(f533,plain,
! [X2,X0,X1] : mult(rd(X0,X1),X2) = ld(rd(X1,X0),X2),
inference(superposition,[],[f316,f7]) ).
fof(f589,plain,
! [X2,X0,X1] : ld(rd(X0,X1),mult(mult(X2,rd(X0,X1)),X1)) = mult(mult(rd(X1,X0),X2),X0),
inference(backward_demodulation,[],[f147,f533]) ).
fof(f590,plain,
! [X2,X0,X1] : mult(mult(X2,rd(X0,X1)),X1) = mult(rd(X0,X1),mult(mult(rd(X1,X0),X2),X0)),
inference(backward_demodulation,[],[f111,f533]) ).
fof(f594,plain,
! [X2,X0,X1] : ld(rd(X0,X1),rd(X2,rd(X0,X1))) = rd(mult(rd(X1,X0),mult(X2,X1)),X0),
inference(backward_demodulation,[],[f250,f533]) ).
fof(f615,plain,
! [X2,X0,X1] : rd(mult(rd(X1,X0),mult(X2,X1)),X0) = mult(rd(X1,X0),rd(X2,rd(X0,X1))),
inference(forward_demodulation,[],[f594,f533]) ).
fof(f617,plain,
! [X2,X0,X1] : mult(mult(rd(X1,X0),X2),X0) = mult(rd(X1,X0),mult(mult(X2,rd(X0,X1)),X1)),
inference(forward_demodulation,[],[f589,f533]) ).
fof(f653,plain,
! [X2,X3,X0,X1] : ld(mult(mult(X0,X1),X0),X3) = mult(rd(X2,mult(X0,mult(X1,mult(X0,X2)))),X3),
inference(superposition,[],[f533,f14]) ).
fof(f667,plain,
! [X2,X0,X1] : mult(rd(X1,X0),mult(rd(X0,X1),X2)) = X2,
inference(superposition,[],[f1,f533]) ).
fof(f671,plain,
! [X2,X3,X0,X1] : mult(rd(X1,X0),mult(ld(rd(X1,X0),X3),X2)) = mult(mult(X3,rd(X1,X0)),mult(rd(X0,X1),X2)),
inference(superposition,[],[f112,f533]) ).
fof(f690,plain,
! [X2,X3,X0,X1] : mult(mult(X3,rd(X1,X0)),mult(rd(X0,X1),X2)) = mult(rd(X1,X0),mult(mult(rd(X0,X1),X3),X2)),
inference(forward_demodulation,[],[f671,f533]) ).
fof(f894,plain,
! [X2,X3,X0,X1] : ld(rd(X2,mult(X0,X2)),mult(mult(X3,rd(X2,mult(X0,X2))),X1)) = mult(ld(rd(X2,mult(X0,X2)),X3),ld(X0,X1)),
inference(superposition,[],[f120,f317]) ).
fof(f925,plain,
! [X2,X3,X0,X1] : ld(rd(X2,mult(X0,X2)),mult(mult(X3,rd(X2,mult(X0,X2))),X1)) = mult(mult(rd(mult(X0,X2),X2),X3),ld(X0,X1)),
inference(forward_demodulation,[],[f894,f533]) ).
fof(f953,plain,
! [X2,X3,X0,X1] : mult(mult(X0,X3),ld(X0,X1)) = ld(rd(X2,mult(X0,X2)),mult(mult(X3,rd(X2,mult(X0,X2))),X1)),
inference(forward_demodulation,[],[f925,f4]) ).
fof(f974,plain,
! [X2,X3,X0,X1] : mult(mult(X0,X3),ld(X0,X1)) = mult(rd(mult(X0,X2),X2),mult(mult(X3,rd(X2,mult(X0,X2))),X1)),
inference(forward_demodulation,[],[f953,f533]) ).
fof(f989,plain,
! [X2,X3,X0,X1] : mult(mult(X0,X3),ld(X0,X1)) = mult(X0,mult(mult(X3,rd(X2,mult(X0,X2))),X1)),
inference(forward_demodulation,[],[f974,f4]) ).
fof(f1091,plain,
! [X2,X0,X1] : mult(X0,rd(ld(X0,X1),mult(X0,X2))) = rd(rd(X1,X2),X0),
inference(superposition,[],[f1,f241]) ).
fof(f1134,plain,
! [X2,X0,X1] : ld(X1,rd(X2,X1)) = rd(X0,mult(X1,ld(X2,mult(X1,X0)))),
inference(superposition,[],[f235,f2]) ).
fof(f1315,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X1) = mult(X1,rd(X2,rd(X0,mult(X1,X0)))),
inference(superposition,[],[f371,f242]) ).
fof(f1322,plain,
! [X0,X1] : mult(X1,ld(X0,rd(X0,X0))) = mult(mult(X1,ld(X0,ld(X1,rd(X1,X1)))),X1),
inference(superposition,[],[f371,f274]) ).
fof(f1331,plain,
! [X0,X1] : rd(X1,ld(X0,ld(X0,rd(X0,X0)))) = mult(mult(mult(X0,ld(X0,X1)),X0),X0),
inference(superposition,[],[f45,f371]) ).
fof(f1332,plain,
! [X0] : rd(X0,X0) = mult(mult(X0,ld(X0,ld(X0,rd(X0,X0)))),X0),
inference(superposition,[],[f301,f371]) ).
fof(f1333,plain,
! [X0,X1] : rd(X1,ld(X0,rd(X0,X0))) = ld(X0,mult(mult(X0,X1),X0)),
inference(superposition,[],[f2,f371]) ).
fof(f1375,plain,
! [X0] : rd(X0,X0) = mult(ld(X0,rd(X0,X0)),X0),
inference(forward_demodulation,[],[f1332,f1]) ).
fof(f1376,plain,
! [X0,X1] : rd(X1,ld(X0,ld(X0,rd(X0,X0)))) = mult(X0,mult(ld(X0,X1),mult(X0,X0))),
inference(forward_demodulation,[],[f1331,f5]) ).
fof(f1393,plain,
! [X0] : rd(X0,X0) = ld(X0,mult(X0,ld(X0,X0))),
inference(forward_demodulation,[],[f1375,f369]) ).
fof(f1394,plain,
! [X0,X1] : rd(X1,ld(X0,ld(X0,rd(X0,X0)))) = mult(X0,ld(X0,mult(mult(X1,X0),X0))),
inference(forward_demodulation,[],[f1376,f120]) ).
fof(f1406,plain,
! [X0] : rd(X0,X0) = ld(X0,X0),
inference(forward_demodulation,[],[f1393,f2]) ).
fof(f1407,plain,
! [X0,X1] : rd(X1,ld(X0,ld(X0,rd(X0,X0)))) = mult(mult(X1,X0),X0),
inference(forward_demodulation,[],[f1394,f1]) ).
fof(f1417,plain,
! [X0,X1] : rd(X0,mult(X1,X0)) = ld(X1,ld(X1,X1)),
inference(backward_demodulation,[],[f242,f1406]) ).
fof(f1418,plain,
! [X0,X1] : rd(ld(X1,X0),X0) = ld(X1,ld(X1,X1)),
inference(backward_demodulation,[],[f274,f1406]) ).
fof(f1423,plain,
! [X0,X1] : mult(X1,rd(X0,mult(X1,X0))) = ld(X1,X1),
inference(backward_demodulation,[],[f283,f1406]) ).
fof(f1455,plain,
! [X0,X1] : mult(X1,ld(X0,rd(X0,X0))) = mult(mult(X1,ld(X0,ld(X1,ld(X1,X1)))),X1),
inference(backward_demodulation,[],[f1322,f1406]) ).
fof(f1460,plain,
! [X0,X1] : ld(X0,mult(mult(X0,X1),X0)) = rd(X1,ld(X0,ld(X0,X0))),
inference(backward_demodulation,[],[f1333,f1406]) ).
fof(f1477,plain,
! [X0,X1] : mult(mult(X1,X0),X0) = rd(X1,ld(X0,ld(X0,ld(X0,X0)))),
inference(forward_demodulation,[],[f1407,f1406]) ).
fof(f1490,plain,
! [X0,X1] : mult(X1,ld(X0,ld(X0,X0))) = mult(mult(X1,ld(X0,ld(X1,ld(X1,X1)))),X1),
inference(forward_demodulation,[],[f1455,f1406]) ).
fof(f1506,plain,
! [X0,X1] : rd(ld(X1,X0),mult(X1,X0)) = ld(X1,rd(ld(X0,X0),X1)),
inference(superposition,[],[f241,f1406]) ).
fof(f1508,plain,
! [X0,X1] : mult(ld(X0,X0),X1) = ld(ld(X0,X0),X1),
inference(superposition,[],[f533,f1406]) ).
fof(f1509,plain,
! [X0] : mult(ld(X0,X0),X0) = X0,
inference(superposition,[],[f3,f1406]) ).
fof(f1510,plain,
! [X0,X1] : rd(X1,ld(X0,ld(X0,X1))) = mult(mult(X0,ld(ld(X0,X1),ld(X0,X1))),X0),
inference(superposition,[],[f45,f1406]) ).
fof(f1522,plain,
! [X0,X1] : mult(mult(ld(X0,X0),X1),ld(X0,X0)) = rd(mult(ld(X0,X0),mult(X1,X0)),X0),
inference(superposition,[],[f14,f1509]) ).
fof(f1528,plain,
! [X0,X1] : ld(ld(X0,X0),rd(X1,ld(X0,X0))) = rd(ld(ld(X0,X0),mult(X1,X0)),X0),
inference(superposition,[],[f195,f1509]) ).
fof(f1533,plain,
! [X0,X1] : ld(ld(X0,X0),rd(X1,ld(X0,X0))) = rd(X0,mult(ld(X0,X0),ld(X1,X0))),
inference(superposition,[],[f1134,f1509]) ).
fof(f1539,plain,
! [X0,X1] : rd(X0,mult(ld(X0,X0),ld(X1,X0))) = mult(ld(X0,X0),rd(X1,ld(X0,X0))),
inference(forward_demodulation,[],[f1533,f1508]) ).
fof(f1544,plain,
! [X0,X1] : rd(mult(ld(X0,X0),mult(X1,X0)),X0) = ld(ld(X0,X0),rd(X1,ld(X0,X0))),
inference(forward_demodulation,[],[f1528,f1508]) ).
fof(f1553,plain,
! [X0,X1] : rd(mult(ld(X0,X0),mult(X1,X0)),X0) = mult(ld(X0,X0),rd(X1,ld(X0,X0))),
inference(forward_demodulation,[],[f1544,f1508]) ).
fof(f1558,plain,
! [X0,X1] : rd(mult(ld(X0,X0),mult(X1,X0)),X0) = rd(X0,mult(ld(X0,X0),ld(X1,X0))),
inference(forward_demodulation,[],[f1553,f1539]) ).
fof(f1559,plain,
! [X0,X1] : rd(mult(ld(X0,X0),mult(X1,X0)),X0) = mult(ld(X0,X0),rd(X1,ld(X0,X0))),
inference(backward_demodulation,[],[f1539,f1558]) ).
fof(f1578,plain,
! [X2,X0,X1] : mult(rd(X1,ld(X0,X1)),X2) = ld(ld(X0,ld(X0,X0)),X2),
inference(superposition,[],[f533,f1418]) ).
fof(f1579,plain,
! [X0,X1] : ld(X0,X1) = mult(ld(X0,ld(X0,X0)),X1),
inference(superposition,[],[f3,f1418]) ).
fof(f1605,plain,
! [X2,X0] : mult(X0,X2) = ld(ld(X0,ld(X0,X0)),X2),
inference(forward_demodulation,[],[f1578,f8]) ).
fof(f2227,plain,
! [X0,X1] : mult(ld(X0,X0),mult(ld(X0,X0),X1)) = X1,
inference(superposition,[],[f2,f1508]) ).
fof(f2381,plain,
! [X2,X0,X1] : ld(X1,X0) = ld(mult(mult(X1,X2),X1),mult(X1,mult(X2,X0))),
inference(superposition,[],[f15,f1]) ).
fof(f2576,plain,
! [X2,X0,X1] : ld(X1,ld(X2,X0)) = ld(mult(mult(X1,X2),X1),mult(X1,X0)),
inference(superposition,[],[f2381,f1]) ).
fof(f2728,plain,
! [X2,X0,X1] : ld(mult(X0,X1),mult(X1,X2)) = ld(X1,ld(ld(X1,X0),X2)),
inference(superposition,[],[f2576,f1]) ).
fof(f2732,plain,
! [X0,X1] : ld(ld(X0,X0),ld(X0,X1)) = ld(mult(X0,ld(X0,X0)),mult(ld(X0,X0),X1)),
inference(superposition,[],[f2576,f1509]) ).
fof(f2738,plain,
! [X2,X0,X1] : ld(rd(X0,X1),ld(X1,X2)) = ld(mult(X0,rd(X0,X1)),mult(rd(X0,X1),X2)),
inference(superposition,[],[f2576,f3]) ).
fof(f2745,plain,
! [X2,X3,X0,X1] : ld(X0,ld(rd(X1,mult(X0,X2)),X3)) = ld(rd(mult(X0,X1),X2),mult(X0,X3)),
inference(superposition,[],[f2576,f23]) ).
fof(f2747,plain,
! [X2,X0,X1] : ld(mult(mult(X1,X2),X1),X0) = ld(X1,ld(X2,ld(X1,X0))),
inference(superposition,[],[f2576,f1]) ).
fof(f2771,plain,
! [X2,X3,X0,X1] : ld(mult(mult(X0,X1),X0),mult(mult(mult(X0,X2),mult(mult(X0,X1),X0)),X3)) = mult(ld(X0,ld(X1,X2)),mult(mult(mult(X0,X1),X0),X3)),
inference(superposition,[],[f120,f2576]) ).
fof(f2786,plain,
! [X2,X3,X0,X1] : ld(mult(mult(X0,X1),X0),mult(mult(mult(X0,X2),mult(mult(X0,X1),X0)),X3)) = mult(ld(X0,ld(X1,X2)),mult(X0,mult(X1,mult(X0,X3)))),
inference(forward_demodulation,[],[f2771,f5]) ).
fof(f2812,plain,
! [X0,X1] : mult(mult(X1,X0),X0) = rd(X1,ld(mult(mult(X0,X0),X0),X0)),
inference(backward_demodulation,[],[f1477,f2747]) ).
fof(f2813,plain,
! [X2,X3,X0,X1] : ld(X0,ld(rd(X1,mult(X0,X2)),X3)) = mult(rd(X2,mult(X0,X1)),mult(X0,X3)),
inference(forward_demodulation,[],[f2745,f533]) ).
fof(f2820,plain,
! [X2,X0,X1] : ld(mult(X0,rd(X0,X1)),mult(rd(X0,X1),X2)) = mult(rd(X1,X0),ld(X1,X2)),
inference(forward_demodulation,[],[f2738,f533]) ).
fof(f2826,plain,
! [X0,X1] : ld(ld(X0,X0),ld(X0,X1)) = ld(X0,mult(ld(X0,X0),X1)),
inference(forward_demodulation,[],[f2732,f1]) ).
fof(f2831,plain,
! [X2,X3,X0,X1] : ld(mult(mult(X0,X1),X0),mult(mult(mult(X0,X2),mult(mult(X0,X1),X0)),X3)) = ld(X0,mult(mult(ld(X1,X2),X0),mult(X1,mult(X0,X3)))),
inference(forward_demodulation,[],[f2786,f120]) ).
fof(f2846,plain,
! [X2,X3,X0,X1] : mult(rd(X2,mult(X0,X1)),mult(X0,X3)) = ld(X0,mult(rd(mult(X0,X2),X1),X3)),
inference(forward_demodulation,[],[f2813,f533]) ).
fof(f2854,plain,
! [X0,X1] : ld(X0,mult(ld(X0,X0),X1)) = mult(ld(X0,X0),ld(X0,X1)),
inference(forward_demodulation,[],[f2826,f1508]) ).
fof(f2902,plain,
! [X0,X1] : ld(mult(mult(X1,X1),X1),X1) = ld(X1,rd(X0,mult(X1,X0))),
inference(superposition,[],[f2747,f1417]) ).
fof(f2905,plain,
! [X2,X0,X1] : ld(X1,mult(ld(X0,X0),ld(X1,X2))) = ld(mult(mult(X1,ld(X0,X0)),X1),X2),
inference(superposition,[],[f2747,f1508]) ).
fof(f2909,plain,
! [X2,X0,X1] : mult(X0,ld(mult(mult(X0,X1),X0),X2)) = ld(X1,ld(X0,X2)),
inference(superposition,[],[f1,f2747]) ).
fof(f2969,plain,
! [X0,X1] : ld(X0,mult(ld(X0,X0),X1)) = ld(mult(X0,X0),mult(X0,X1)),
inference(superposition,[],[f2728,f1508]) ).
fof(f3012,plain,
! [X0,X1] : mult(ld(X0,X0),ld(X0,X1)) = ld(mult(X0,X0),mult(X0,X1)),
inference(backward_demodulation,[],[f2854,f2969]) ).
fof(f3079,plain,
! [X2,X0,X1] : ld(ld(X1,X0),ld(X1,X2)) = mult(X1,ld(mult(X0,X1),X2)),
inference(superposition,[],[f2909,f1]) ).
fof(f3115,plain,
! [X2,X3,X0,X1] : mult(X1,mult(ld(mult(mult(X1,X0),X1),X2),mult(X1,X3))) = mult(mult(ld(X0,ld(X1,X2)),X1),X3),
inference(superposition,[],[f5,f2909]) ).
fof(f3180,plain,
! [X0,X1] : rd(X1,ld(X0,ld(X0,X1))) = mult(mult(X0,mult(X0,ld(mult(X1,X0),X1))),X0),
inference(backward_demodulation,[],[f1510,f3079]) ).
fof(f3258,plain,
! [X0,X1] : mult(ld(X0,X0),ld(X0,X1)) = mult(X0,ld(mult(X0,X0),X1)),
inference(superposition,[],[f1508,f3079]) ).
fof(f3263,plain,
! [X2,X0,X1] : mult(mult(X0,ld(mult(X1,X0),X1)),X2) = ld(mult(X0,ld(mult(X1,X0),X1)),X2),
inference(superposition,[],[f1508,f3079]) ).
fof(f3267,plain,
! [X0,X1] : ld(X0,X1) = mult(mult(X0,ld(mult(X1,X0),X1)),ld(X0,X1)),
inference(superposition,[],[f1509,f3079]) ).
fof(f3280,plain,
! [X2,X3,X0,X1] : rd(X3,mult(ld(X0,X1),X3)) = rd(mult(X0,ld(mult(X1,X0),X2)),ld(X0,X2)),
inference(superposition,[],[f300,f3079]) ).
fof(f3291,plain,
! [X2,X3,X0,X1] : rd(X3,mult(ld(X0,X1),X3)) = mult(mult(X0,rd(ld(mult(X1,X0),X2),X2)),X0),
inference(forward_demodulation,[],[f3280,f31]) ).
fof(f3301,plain,
! [X0,X1] : ld(mult(X0,X0),mult(X0,X1)) = mult(X0,ld(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f3258,f3012]) ).
fof(f3346,plain,
! [X0,X1] : rd(rd(X1,X0),ld(X0,X0)) = mult(ld(X0,X0),rd(ld(ld(X0,X0),X1),X0)),
inference(superposition,[],[f1091,f1509]) ).
fof(f3453,plain,
! [X0,X1] : rd(rd(X1,X0),ld(X0,X0)) = mult(ld(X0,X0),rd(mult(ld(X0,X0),X1),X0)),
inference(forward_demodulation,[],[f3346,f1508]) ).
fof(f3546,plain,
! [X0,X1] : mult(mult(X0,rd(X0,X1)),X1) = mult(rd(X0,X1),mult(X1,X0)),
inference(superposition,[],[f9,f3]) ).
fof(f3563,plain,
! [X2,X0,X1] : mult(mult(rd(X0,X1),X1),rd(X0,X1)) = rd(mult(mult(X0,rd(X0,X1)),X2),X2),
inference(superposition,[],[f14,f9]) ).
fof(f3609,plain,
! [X0,X1] : mult(mult(rd(X0,X1),X1),rd(X0,X1)) = mult(X0,rd(X0,X1)),
inference(forward_demodulation,[],[f3563,f4]) ).
fof(f3650,plain,
! [X0,X1] : mult(X0,rd(X0,X1)) = rd(mult(rd(X0,X1),mult(X1,X0)),X1),
inference(forward_demodulation,[],[f3609,f20]) ).
fof(f3693,plain,
! [X0,X1] : mult(X1,ld(X0,ld(X0,X0))) = rd(mult(ld(X0,ld(X0,X0)),mult(mult(X0,X1),X1)),mult(X0,X1)),
inference(superposition,[],[f3650,f1417]) ).
fof(f3695,plain,
! [X2,X0,X1] : mult(X2,rd(X0,mult(X1,X0))) = rd(mult(rd(X0,mult(X1,X0)),mult(mult(X1,X2),X2)),mult(X1,X2)),
inference(superposition,[],[f3650,f273]) ).
fof(f3704,plain,
! [X2,X0,X1] : mult(ld(X1,X2),rd(X0,mult(X1,X0))) = rd(mult(rd(X0,mult(X1,X0)),mult(X2,ld(X1,X2))),X2),
inference(superposition,[],[f3650,f300]) ).
fof(f3713,plain,
! [X0,X1] : mult(ld(X1,X0),rd(ld(X1,X0),X1)) = rd(mult(rd(ld(X1,X0),X1),X0),X1),
inference(superposition,[],[f3650,f1]) ).
fof(f3719,plain,
! [X0] : mult(X0,rd(X0,ld(X0,X0))) = rd(mult(rd(X0,ld(X0,X0)),X0),ld(X0,X0)),
inference(superposition,[],[f3650,f1509]) ).
fof(f3732,plain,
! [X0,X1] : mult(X1,rd(X1,mult(X0,X1))) = rd(ld(X0,mult(mult(X0,X1),X1)),mult(X0,X1)),
inference(superposition,[],[f3650,f317]) ).
fof(f3748,plain,
! [X0,X1] : mult(X1,rd(X1,mult(X0,X1))) = ld(X0,rd(mult(X0,X1),X0)),
inference(forward_demodulation,[],[f3732,f195]) ).
fof(f3753,plain,
! [X0] : mult(X0,X0) = rd(mult(X0,X0),ld(X0,X0)),
inference(forward_demodulation,[],[f3719,f8]) ).
fof(f3765,plain,
! [X2,X0,X1] : mult(ld(X1,X2),rd(X0,mult(X1,X0))) = rd(ld(X1,mult(X2,ld(X1,X2))),X2),
inference(forward_demodulation,[],[f3704,f317]) ).
fof(f3774,plain,
! [X2,X0,X1] : mult(X2,rd(X0,mult(X1,X0))) = rd(ld(X1,mult(mult(X1,X2),X2)),mult(X1,X2)),
inference(forward_demodulation,[],[f3695,f317]) ).
fof(f3776,plain,
! [X0,X1] : mult(X1,ld(X0,ld(X0,X0))) = rd(ld(X0,mult(mult(X0,X1),X1)),mult(X0,X1)),
inference(forward_demodulation,[],[f3693,f1579]) ).
fof(f3782,plain,
! [X0] : mult(X0,X0) = mult(mult(X0,rd(X0,X0)),X0),
inference(forward_demodulation,[],[f3753,f31]) ).
fof(f3790,plain,
! [X2,X0,X1] : ld(X1,rd(X2,X1)) = mult(ld(X1,X2),rd(X0,mult(X1,X0))),
inference(forward_demodulation,[],[f3765,f244]) ).
fof(f3797,plain,
! [X2,X0,X1] : mult(X2,rd(X0,mult(X1,X0))) = ld(X1,rd(mult(X1,X2),X1)),
inference(forward_demodulation,[],[f3774,f195]) ).
fof(f3799,plain,
! [X0,X1] : mult(X1,ld(X0,ld(X0,X0))) = ld(X0,rd(mult(X0,X1),X0)),
inference(forward_demodulation,[],[f3776,f195]) ).
fof(f3802,plain,
! [X0] : mult(X0,X0) = mult(rd(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f3782,f3546]) ).
fof(f3821,plain,
! [X0,X1] : mult(mult(X1,ld(X0,ld(X1,ld(X1,X1)))),X1) = ld(X0,rd(mult(X0,X1),X0)),
inference(backward_demodulation,[],[f1490,f3799]) ).
fof(f3825,plain,
! [X0] : mult(X0,X0) = mult(ld(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f3802,f1406]) ).
fof(f3840,plain,
! [X0] : mult(X0,X0) = ld(X0,mult(mult(X0,X0),X0)),
inference(forward_demodulation,[],[f3825,f120]) ).
fof(f3855,plain,
! [X0,X1] : ld(X0,rd(X1,mult(X0,X1))) = ld(rd(X1,mult(X0,X1)),mult(ld(X0,rd(X1,mult(X0,X1))),rd(X1,mult(X0,X1)))),
inference(superposition,[],[f3840,f317]) ).
fof(f3859,plain,
! [X0] : ld(X0,rd(mult(X0,X0),X0)) = rd(mult(X0,X0),mult(X0,X0)),
inference(superposition,[],[f195,f3840]) ).
fof(f3860,plain,
! [X0] : mult(mult(X0,X0),X0) = mult(X0,mult(X0,X0)),
inference(superposition,[],[f1,f3840]) ).
fof(f3896,plain,
! [X0,X1] : mult(mult(X1,X0),X0) = rd(X1,ld(mult(X0,mult(X0,X0)),X0)),
inference(backward_demodulation,[],[f2812,f3860]) ).
fof(f3897,plain,
! [X0,X1] : ld(X1,rd(X0,mult(X1,X0))) = ld(mult(X1,mult(X1,X1)),X1),
inference(backward_demodulation,[],[f2902,f3860]) ).
fof(f3935,plain,
! [X0] : ld(X0,rd(mult(X0,X0),X0)) = ld(mult(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f3859,f1406]) ).
fof(f3938,plain,
! [X0,X1] : ld(X0,rd(X1,mult(X0,X1))) = mult(rd(mult(X0,X1),X1),mult(ld(X0,rd(X1,mult(X0,X1))),rd(X1,mult(X0,X1)))),
inference(forward_demodulation,[],[f3855,f533]) ).
fof(f3945,plain,
! [X0] : ld(mult(X0,X0),mult(X0,X0)) = mult(X0,rd(X0,mult(X0,X0))),
inference(forward_demodulation,[],[f3935,f3748]) ).
fof(f3946,plain,
! [X0,X1] : ld(X0,rd(X1,mult(X0,X1))) = mult(rd(mult(X0,X1),X1),ld(X0,rd(rd(X1,mult(X0,X1)),X0))),
inference(forward_demodulation,[],[f3938,f3790]) ).
fof(f3952,plain,
! [X0] : ld(X0,X0) = ld(mult(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f3945,f1423]) ).
fof(f3953,plain,
! [X0,X1] : ld(X0,rd(X1,mult(X0,X1))) = mult(X0,mult(rd(X1,mult(X0,X1)),rd(rd(X1,mult(X0,X1)),X0))),
inference(forward_demodulation,[],[f3946,f186]) ).
fof(f3959,plain,
! [X0,X1] : ld(X0,rd(X1,mult(X0,X1))) = mult(X0,ld(X0,rd(rd(X1,mult(X0,X1)),X0))),
inference(forward_demodulation,[],[f3953,f317]) ).
fof(f3965,plain,
! [X0,X1] : ld(X0,rd(X1,mult(X0,X1))) = rd(rd(X1,mult(X0,X1)),X0),
inference(forward_demodulation,[],[f3959,f1]) ).
fof(f3988,plain,
! [X0] : mult(X0,X0) = rd(mult(X0,mult(X0,X0)),X0),
inference(superposition,[],[f4,f3860]) ).
fof(f4177,plain,
! [X0] : mult(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))) = rd(ld(X0,mult(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(X0,ld(X0,X0))),
inference(superposition,[],[f3988,f1579]) ).
fof(f4203,plain,
! [X0] : mult(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))) = ld(X0,mult(mult(X0,ld(X0,mult(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),X0)),
inference(forward_demodulation,[],[f4177,f1460]) ).
fof(f4213,plain,
! [X0] : mult(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))) = ld(X0,mult(mult(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))),X0)),
inference(forward_demodulation,[],[f4203,f1]) ).
fof(f4217,plain,
! [X0] : ld(X0,rd(mult(X0,ld(X0,ld(X0,X0))),X0)) = ld(X0,mult(ld(X0,rd(mult(X0,ld(X0,ld(X0,X0))),X0)),X0)),
inference(forward_demodulation,[],[f4213,f3799]) ).
fof(f4219,plain,
! [X0] : ld(X0,rd(mult(X0,ld(X0,ld(X0,X0))),X0)) = ld(X0,ld(X0,mult(mult(X0,ld(X0,ld(X0,X0))),ld(X0,X0)))),
inference(forward_demodulation,[],[f4217,f369]) ).
fof(f4221,plain,
! [X0] : ld(X0,rd(ld(X0,X0),X0)) = ld(X0,ld(X0,mult(ld(X0,X0),ld(X0,X0)))),
inference(forward_demodulation,[],[f4219,f1]) ).
fof(f4223,plain,
! [X0] : ld(X0,rd(ld(X0,X0),X0)) = ld(X0,ld(mult(mult(X0,ld(X0,X0)),X0),X0)),
inference(forward_demodulation,[],[f4221,f2905]) ).
fof(f4225,plain,
! [X0] : ld(X0,rd(ld(X0,X0),X0)) = ld(X0,ld(mult(X0,X0),X0)),
inference(forward_demodulation,[],[f4223,f1]) ).
fof(f4227,plain,
! [X0] : ld(X0,ld(mult(X0,X0),X0)) = rd(ld(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f4225,f1506]) ).
fof(f4341,plain,
! [X0,X1] : ld(mult(X0,X0),X1) = mult(ld(mult(X0,X0),ld(X0,X0)),X1),
inference(superposition,[],[f1579,f3952]) ).
fof(f4360,plain,
! [X0] : ld(mult(X0,X0),ld(X0,X0)) = rd(ld(X0,X0),mult(X0,X0)),
inference(superposition,[],[f1418,f3952]) ).
fof(f4362,plain,
! [X0,X1] : ld(mult(mult(X0,X0),mult(X0,X0)),mult(mult(X0,X0),X1)) = ld(mult(X0,X0),ld(ld(X0,X0),X1)),
inference(superposition,[],[f2728,f3952]) ).
fof(f4364,plain,
! [X0,X1] : mult(mult(X0,X0),ld(mult(mult(X0,X0),mult(X0,X0)),X1)) = ld(ld(X0,X0),ld(mult(X0,X0),X1)),
inference(superposition,[],[f3079,f3952]) ).
fof(f4366,plain,
! [X0,X1] : mult(mult(X0,X0),ld(mult(mult(X0,X0),mult(X0,X0)),X1)) = mult(ld(X0,X0),ld(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f4364,f1508]) ).
fof(f4367,plain,
! [X0,X1] : ld(mult(mult(X0,X0),mult(X0,X0)),mult(mult(X0,X0),X1)) = ld(mult(X0,X0),mult(ld(X0,X0),X1)),
inference(forward_demodulation,[],[f4362,f1508]) ).
fof(f4369,plain,
! [X0] : ld(mult(X0,X0),ld(X0,X0)) = ld(X0,ld(mult(X0,X0),X0)),
inference(forward_demodulation,[],[f4360,f4227]) ).
fof(f4383,plain,
! [X0,X1] : ld(mult(mult(X0,X0),mult(X0,X0)),mult(mult(X0,X0),X1)) = mult(ld(X0,X0),ld(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f4366,f3301]) ).
fof(f4385,plain,
! [X0,X1] : ld(mult(X0,X0),X1) = mult(ld(X0,ld(mult(X0,X0),X0)),X1),
inference(backward_demodulation,[],[f4341,f4369]) ).
fof(f4397,plain,
! [X0,X1] : mult(ld(X0,X0),ld(mult(X0,X0),X1)) = ld(mult(X0,X0),mult(ld(X0,X0),X1)),
inference(forward_demodulation,[],[f4383,f4367]) ).
fof(f4435,plain,
! [X0,X1] : ld(ld(X0,X1),ld(mult(ld(X0,X1),ld(X0,X1)),ld(X0,X1))) = rd(mult(X0,ld(mult(X1,X0),X1)),mult(ld(X0,X1),ld(X0,X1))),
inference(superposition,[],[f4227,f3079]) ).
fof(f4443,plain,
! [X0] : rd(rd(X0,X0),X0) = mult(X0,ld(X0,ld(mult(X0,X0),X0))),
inference(superposition,[],[f1091,f4227]) ).
fof(f4449,plain,
! [X0,X1] : mult(rd(mult(X0,X0),ld(X0,X0)),X1) = ld(ld(X0,ld(mult(X0,X0),X0)),X1),
inference(superposition,[],[f533,f4227]) ).
fof(f4460,plain,
! [X0,X1] : mult(mult(mult(X0,rd(X0,X0)),X0),X1) = ld(ld(X0,ld(mult(X0,X0),X0)),X1),
inference(forward_demodulation,[],[f4449,f31]) ).
fof(f4465,plain,
! [X0] : ld(mult(X0,X0),X0) = rd(rd(X0,X0),X0),
inference(forward_demodulation,[],[f4443,f1]) ).
fof(f4476,plain,
! [X0,X1] : mult(X0,mult(rd(X0,X0),mult(X0,X1))) = ld(ld(X0,ld(mult(X0,X0),X0)),X1),
inference(forward_demodulation,[],[f4460,f5]) ).
fof(f4480,plain,
! [X0] : rd(ld(X0,X0),X0) = ld(mult(X0,X0),X0),
inference(forward_demodulation,[],[f4465,f1406]) ).
fof(f4490,plain,
! [X0,X1] : mult(X0,mult(ld(X0,X0),mult(X0,X1))) = ld(ld(X0,ld(mult(X0,X0),X0)),X1),
inference(forward_demodulation,[],[f4476,f1406]) ).
fof(f4494,plain,
! [X0] : ld(X0,ld(X0,X0)) = ld(mult(X0,X0),X0),
inference(forward_demodulation,[],[f4480,f1418]) ).
fof(f4504,plain,
! [X0,X1] : mult(X0,ld(X0,mult(mult(X0,X0),X1))) = ld(ld(X0,ld(mult(X0,X0),X0)),X1),
inference(forward_demodulation,[],[f4490,f120]) ).
fof(f4507,plain,
! [X0,X1] : rd(X0,mult(X1,X0)) = ld(mult(X1,X1),X1),
inference(backward_demodulation,[],[f1417,f4494]) ).
fof(f4508,plain,
! [X0,X1] : rd(ld(X1,X0),X0) = ld(mult(X1,X1),X1),
inference(backward_demodulation,[],[f1418,f4494]) ).
fof(f4517,plain,
! [X0,X1] : ld(X0,mult(mult(X0,X1),X0)) = rd(X1,ld(mult(X0,X0),X0)),
inference(backward_demodulation,[],[f1460,f4494]) ).
fof(f4519,plain,
! [X0,X1] : ld(X0,X1) = mult(ld(mult(X0,X0),X0),X1),
inference(backward_demodulation,[],[f1579,f4494]) ).
fof(f4520,plain,
! [X2,X0] : mult(X0,X2) = ld(ld(mult(X0,X0),X0),X2),
inference(backward_demodulation,[],[f1605,f4494]) ).
fof(f4528,plain,
! [X0,X1] : ld(X0,rd(mult(X0,X1),X0)) = mult(X1,ld(mult(X0,X0),X0)),
inference(backward_demodulation,[],[f3799,f4494]) ).
fof(f4529,plain,
! [X0,X1] : ld(X0,rd(mult(X0,X1),X0)) = mult(mult(X1,ld(X0,ld(mult(X1,X1),X1))),X1),
inference(backward_demodulation,[],[f3821,f4494]) ).
fof(f4546,plain,
! [X0,X1] : mult(mult(X0,X0),X1) = ld(ld(X0,ld(mult(X0,X0),X0)),X1),
inference(forward_demodulation,[],[f4504,f1]) ).
fof(f4555,plain,
! [X2,X0,X1] : mult(X2,rd(X0,mult(X1,X0))) = mult(X2,ld(mult(X1,X1),X1)),
inference(backward_demodulation,[],[f3797,f4528]) ).
fof(f4557,plain,
! [X0,X1] : mult(X1,ld(mult(X0,X0),X0)) = mult(mult(X1,ld(X0,ld(mult(X1,X1),X1))),X1),
inference(backward_demodulation,[],[f4529,f4528]) ).
fof(f4623,plain,
! [X0,X1] : mult(ld(X0,X1),ld(mult(X0,X0),X0)) = rd(mult(ld(mult(X0,X0),X0),mult(X1,ld(X0,X1))),X1),
inference(superposition,[],[f3650,f4508]) ).
fof(f4665,plain,
! [X0,X1] : rd(ld(X0,mult(X1,ld(X0,X1))),X1) = mult(ld(X0,X1),ld(mult(X0,X0),X0)),
inference(forward_demodulation,[],[f4623,f4519]) ).
fof(f4688,plain,
! [X0,X1] : ld(X0,rd(X1,X0)) = mult(ld(X0,X1),ld(mult(X0,X0),X0)),
inference(forward_demodulation,[],[f4665,f244]) ).
fof(f4764,plain,
! [X0,X1] : mult(mult(X1,X1),rd(X0,mult(X1,X0))) = X1,
inference(superposition,[],[f1,f4507]) ).
fof(f4765,plain,
! [X0,X1] : mult(X1,X1) = rd(X1,rd(X0,mult(X1,X0))),
inference(superposition,[],[f8,f4507]) ).
fof(f4769,plain,
! [X2,X0,X1] : mult(mult(X1,X1),mult(ld(mult(X1,X1),X2),X1)) = mult(mult(X2,mult(X1,X1)),rd(X0,mult(X1,X0))),
inference(superposition,[],[f112,f4507]) ).
fof(f4777,plain,
! [X2,X0,X1] : ld(mult(X1,X1),X2) = mult(rd(rd(X0,mult(X1,X0)),X1),X2),
inference(superposition,[],[f316,f4507]) ).
fof(f4790,plain,
! [X2,X0,X1] : ld(mult(X1,X1),X2) = mult(ld(X1,rd(X0,mult(X1,X0))),X2),
inference(forward_demodulation,[],[f4777,f3965]) ).
fof(f5078,plain,
! [X0,X1] : ld(ld(X0,X1),mult(X0,ld(mult(X1,X0),X1))) = ld(mult(ld(X0,X1),ld(X0,X1)),ld(X0,X1)),
inference(superposition,[],[f4494,f3079]) ).
fof(f5084,plain,
! [X0] : ld(mult(mult(X0,X0),X0),X0) = ld(X0,ld(mult(X0,X0),X0)),
inference(superposition,[],[f2747,f4494]) ).
fof(f5105,plain,
! [X0] : ld(mult(X0,X0),X0) = rd(ld(mult(X0,X0),X0),ld(X0,X0)),
inference(superposition,[],[f4508,f4494]) ).
fof(f5130,plain,
! [X0] : ld(mult(X0,mult(X0,X0)),X0) = ld(X0,ld(mult(X0,X0),X0)),
inference(forward_demodulation,[],[f5084,f3860]) ).
fof(f5138,plain,
! [X0,X1] : rd(mult(X0,ld(mult(X1,X0),X1)),mult(ld(X0,X1),ld(X0,X1))) = ld(ld(X0,X1),ld(ld(X0,X1),mult(X0,ld(mult(X1,X0),X1)))),
inference(backward_demodulation,[],[f4435,f5078]) ).
fof(f5152,plain,
! [X0] : ld(mult(X0,mult(X0,X0)),X0) = rd(ld(X0,X0),mult(X0,X0)),
inference(backward_demodulation,[],[f4227,f5130]) ).
fof(f5156,plain,
! [X0,X1] : ld(mult(X0,X0),X1) = mult(ld(mult(X0,mult(X0,X0)),X0),X1),
inference(backward_demodulation,[],[f4385,f5130]) ).
fof(f5158,plain,
! [X0,X1] : mult(mult(X0,X0),X1) = ld(ld(mult(X0,mult(X0,X0)),X0),X1),
inference(backward_demodulation,[],[f4546,f5130]) ).
fof(f5615,plain,
! [X2,X0,X1] : mult(ld(mult(X0,X0),X1),X0) = ld(mult(X0,X0),mult(mult(X1,mult(X0,X0)),rd(X2,mult(X0,X2)))),
inference(superposition,[],[f120,f4764]) ).
fof(f5744,plain,
! [X0,X1] : ld(X0,mult(mult(X0,X1),X0)) = mult(mult(X1,mult(X0,X0)),ld(mult(X0,X0),X0)),
inference(superposition,[],[f4528,f14]) ).
fof(f5796,plain,
! [X0,X1] : ld(X0,mult(mult(X0,X1),X0)) = mult(mult(X0,X0),mult(ld(mult(X0,X0),X1),X0)),
inference(forward_demodulation,[],[f5744,f112]) ).
fof(f5824,plain,
! [X2,X0,X1] : mult(mult(X2,mult(X1,X1)),rd(X0,mult(X1,X0))) = ld(X1,mult(mult(X1,X2),X1)),
inference(backward_demodulation,[],[f4769,f5796]) ).
fof(f5846,plain,
! [X0,X1] : mult(ld(mult(X0,X0),X1),X0) = ld(mult(X0,X0),ld(X0,mult(mult(X0,X1),X0))),
inference(backward_demodulation,[],[f5615,f5824]) ).
fof(f5914,plain,
! [X2,X0,X1] : rd(X2,rd(X0,mult(X1,X0))) = ld(X1,mult(mult(X1,X2),X1)),
inference(superposition,[],[f4517,f4507]) ).
fof(f6421,plain,
! [X0,X1] : mult(mult(X1,ld(X0,X0)),ld(X0,X0)) = rd(X1,ld(mult(ld(X0,X0),ld(mult(X0,X0),mult(X0,X0))),ld(X0,X0))),
inference(superposition,[],[f3896,f3012]) ).
fof(f6432,plain,
! [X0,X1] : ld(X0,X1) = ld(ld(X0,X0),ld(mult(X0,X0),mult(X0,X1))),
inference(superposition,[],[f2,f3012]) ).
fof(f6478,plain,
! [X0,X1] : ld(X0,X1) = mult(ld(X0,X0),ld(mult(X0,X0),mult(X0,X1))),
inference(forward_demodulation,[],[f6432,f1508]) ).
fof(f6488,plain,
! [X0,X1] : mult(mult(X1,ld(X0,X0)),ld(X0,X0)) = rd(X1,ld(ld(mult(X0,X0),mult(ld(X0,X0),mult(X0,X0))),ld(X0,X0))),
inference(forward_demodulation,[],[f6421,f4397]) ).
fof(f6521,plain,
! [X0,X1] : ld(X0,X1) = ld(mult(X0,X0),mult(ld(X0,X0),mult(X0,X1))),
inference(forward_demodulation,[],[f6478,f4397]) ).
fof(f6531,plain,
! [X0,X1] : mult(mult(X1,ld(X0,X0)),ld(X0,X0)) = rd(X1,ld(ld(mult(X0,X0),ld(X0,mult(mult(X0,X0),X0))),ld(X0,X0))),
inference(forward_demodulation,[],[f6488,f120]) ).
fof(f6558,plain,
! [X0,X1] : ld(X0,X1) = ld(mult(X0,X0),ld(X0,mult(mult(X0,X0),X1))),
inference(forward_demodulation,[],[f6521,f120]) ).
fof(f6568,plain,
! [X0,X1] : mult(mult(X1,ld(X0,X0)),ld(X0,X0)) = rd(X1,ld(mult(ld(mult(X0,X0),X0),X0),ld(X0,X0))),
inference(forward_demodulation,[],[f6531,f5846]) ).
fof(f6596,plain,
! [X0,X1] : mult(mult(X1,ld(X0,X0)),ld(X0,X0)) = rd(X1,ld(ld(X0,X0),ld(X0,X0))),
inference(forward_demodulation,[],[f6568,f4519]) ).
fof(f6614,plain,
! [X0,X1] : mult(mult(X1,ld(X0,X0)),ld(X0,X0)) = rd(X1,mult(ld(X0,X0),ld(X0,X0))),
inference(forward_demodulation,[],[f6596,f1508]) ).
fof(f6627,plain,
! [X0,X1] : rd(X1,ld(mult(X0,X0),mult(X0,X0))) = mult(mult(X1,ld(X0,X0)),ld(X0,X0)),
inference(forward_demodulation,[],[f6614,f3012]) ).
fof(f6637,plain,
! [X0,X1] : rd(X1,ld(X0,X0)) = mult(mult(X1,ld(X0,X0)),ld(X0,X0)),
inference(forward_demodulation,[],[f6627,f3952]) ).
fof(f6931,plain,
! [X0,X1] : rd(mult(X0,ld(mult(X1,X0),X1)),mult(ld(X0,X1),ld(X0,X1))) = ld(mult(ld(X0,X1),mult(ld(X0,X1),ld(X0,X1))),ld(X0,X1)),
inference(superposition,[],[f5152,f3079]) ).
fof(f8197,plain,
! [X0,X1] : ld(X1,ld(mult(X1,X1),X0)) = ld(mult(X1,X1),ld(X1,X0)),
inference(superposition,[],[f6558,f1]) ).
fof(f8254,plain,
! [X0,X1] : mult(ld(mult(X0,X0),X1),X0) = ld(X0,ld(mult(X0,X0),mult(mult(X0,X1),X0))),
inference(backward_demodulation,[],[f5846,f8197]) ).
fof(f8353,plain,
! [X0,X1] : ld(ld(mult(X0,X0),X0),ld(mult(ld(mult(X0,X0),X0),ld(mult(X0,X0),X0)),X1)) = ld(mult(ld(mult(X0,X0),X0),ld(mult(X0,X0),X0)),mult(X0,X1)),
inference(superposition,[],[f8197,f4520]) ).
fof(f8412,plain,
! [X0,X1] : ld(ld(mult(X0,X0),X0),ld(ld(X0,ld(mult(X0,X0),X0)),X1)) = ld(ld(X0,ld(mult(X0,X0),X0)),mult(X0,X1)),
inference(forward_demodulation,[],[f8353,f4519]) ).
fof(f8429,plain,
! [X0,X1] : ld(ld(mult(X0,X0),X0),ld(ld(mult(X0,mult(X0,X0)),X0),X1)) = ld(ld(mult(X0,mult(X0,X0)),X0),mult(X0,X1)),
inference(forward_demodulation,[],[f8412,f5130]) ).
fof(f8441,plain,
! [X0,X1] : mult(mult(X0,X0),mult(X0,X1)) = ld(ld(mult(X0,X0),X0),ld(ld(mult(X0,mult(X0,X0)),X0),X1)),
inference(forward_demodulation,[],[f8429,f5158]) ).
fof(f8458,plain,
! [X0,X1] : mult(mult(X0,X0),mult(X0,X1)) = mult(X0,ld(ld(mult(X0,mult(X0,X0)),X0),X1)),
inference(forward_demodulation,[],[f8441,f4520]) ).
fof(f8470,plain,
! [X0,X1] : mult(mult(X0,X0),mult(X0,X1)) = mult(X0,mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f8458,f5158]) ).
fof(f9806,plain,
! [X0,X1] : ld(mult(X0,X0),X0) = ld(ld(X0,X1),ld(X0,rd(X1,X0))),
inference(superposition,[],[f2,f4688]) ).
fof(f9852,plain,
! [X0,X1] : ld(mult(X0,X0),X0) = mult(X0,ld(mult(X1,X0),rd(X1,X0))),
inference(forward_demodulation,[],[f9806,f3079]) ).
fof(f10016,plain,
! [X0,X1] : ld(mult(X1,X1),X1) = mult(X1,ld(X0,rd(rd(X0,X1),X1))),
inference(superposition,[],[f9852,f3]) ).
fof(f10045,plain,
! [X0,X1] : ld(mult(X1,X1),X1) = mult(X1,ld(mult(mult(X0,X1),X1),X0)),
inference(superposition,[],[f9852,f4]) ).
fof(f10061,plain,
! [X0,X1] : ld(X0,ld(mult(X0,X0),X0)) = ld(mult(X1,X0),rd(X1,X0)),
inference(superposition,[],[f2,f9852]) ).
fof(f10126,plain,
! [X0,X1] : ld(mult(X0,mult(X0,X0)),X0) = ld(mult(X1,X0),rd(X1,X0)),
inference(forward_demodulation,[],[f10061,f5130]) ).
fof(f10395,plain,
! [X0,X1] : ld(X0,ld(mult(X0,X0),X0)) = ld(mult(mult(X1,X0),X0),X1),
inference(superposition,[],[f2,f10045]) ).
fof(f10462,plain,
! [X0,X1] : ld(mult(X0,mult(X0,X0)),X0) = ld(mult(mult(X1,X0),X0),X1),
inference(forward_demodulation,[],[f10395,f5130]) ).
fof(f10711,plain,
! [X0,X1] : ld(X0,ld(mult(X0,X0),X0)) = ld(X1,rd(rd(X1,X0),X0)),
inference(superposition,[],[f2,f10016]) ).
fof(f10780,plain,
! [X0,X1] : ld(mult(X0,mult(X0,X0)),X0) = ld(X1,rd(rd(X1,X0),X0)),
inference(forward_demodulation,[],[f10711,f5130]) ).
fof(f11000,plain,
! [X0,X1] : ld(mult(ld(X0,X1),mult(ld(X0,X1),ld(X0,X1))),ld(X0,X1)) = ld(mult(ld(mult(X0,X0),mult(X0,X1)),ld(X0,X1)),ld(X0,X0)),
inference(superposition,[],[f10462,f3012]) ).
fof(f11016,plain,
! [X0,X1] : ld(mult(X0,mult(X0,X0)),X0) = ld(mult(X0,mult(X1,mult(X0,X0))),mult(X0,X1)),
inference(superposition,[],[f10462,f5]) ).
fof(f11133,plain,
! [X0,X1] : rd(mult(X0,ld(mult(X1,X0),X1)),mult(ld(X0,X1),ld(X0,X1))) = ld(mult(ld(mult(X0,X0),mult(X0,X1)),ld(X0,X1)),ld(X0,X0)),
inference(forward_demodulation,[],[f11000,f6931]) ).
fof(f12480,plain,
! [X2,X0,X1] : mult(X1,ld(mult(mult(X0,X0),mult(X0,X0)),mult(X0,X0))) = mult(X1,rd(rd(X2,mult(X0,X2)),X0)),
inference(superposition,[],[f4555,f4764]) ).
fof(f12880,plain,
! [X2,X0,X1] : mult(X1,ld(mult(mult(X0,X0),mult(X0,X0)),mult(X0,X0))) = mult(X1,ld(X0,rd(X2,mult(X0,X2)))),
inference(forward_demodulation,[],[f12480,f3965]) ).
fof(f13020,plain,
! [X2,X0,X1] : mult(X1,ld(mult(X0,mult(mult(X0,X0),X0)),mult(X0,X0))) = mult(X1,ld(X0,rd(X2,mult(X0,X2)))),
inference(forward_demodulation,[],[f12880,f8470]) ).
fof(f13139,plain,
! [X2,X0,X1] : mult(X1,ld(mult(X0,mult(X0,mult(X0,X0))),mult(X0,X0))) = mult(X1,ld(X0,rd(X2,mult(X0,X2)))),
inference(forward_demodulation,[],[f13020,f3860]) ).
fof(f13230,plain,
! [X2,X0,X1] : mult(X1,ld(mult(X0,mult(X0,X0)),X0)) = mult(X1,ld(X0,rd(X2,mult(X0,X2)))),
inference(forward_demodulation,[],[f13139,f11016]) ).
fof(f13502,plain,
! [X0,X1] : mult(X1,ld(mult(X0,mult(X0,X0)),X0)) = rd(rd(X1,X0),X0),
inference(superposition,[],[f1,f10780]) ).
fof(f13563,plain,
! [X2,X0,X1] : rd(rd(X1,X0),X0) = mult(X1,ld(X0,rd(X2,mult(X0,X2)))),
inference(backward_demodulation,[],[f13230,f13502]) ).
fof(f18352,plain,
! [X0,X1] : mult(rd(X1,X0),ld(X1,X1)) = ld(mult(X0,rd(X0,X1)),X0),
inference(superposition,[],[f2820,f3]) ).
fof(f18695,plain,
! [X0,X1] : rd(X1,X0) = rd(ld(mult(X0,rd(X0,X1)),X0),ld(X1,X1)),
inference(superposition,[],[f4,f18352]) ).
fof(f19152,plain,
! [X0,X1] : ld(mult(ld(X0,X0),mult(ld(X0,X0),ld(X0,X0))),ld(X0,X0)) = ld(ld(mult(X1,rd(X1,X0)),X1),rd(rd(X0,X1),ld(X0,X0))),
inference(superposition,[],[f10780,f18695]) ).
fof(f19159,plain,
! [X0,X1] : rd(mult(X0,ld(mult(X0,X0),X0)),mult(ld(X0,X0),ld(X0,X0))) = ld(ld(mult(X1,rd(X1,X0)),X1),rd(rd(X0,X1),ld(X0,X0))),
inference(forward_demodulation,[],[f19152,f6931]) ).
fof(f19241,plain,
! [X0,X1] : ld(mult(ld(mult(X0,X0),mult(X0,X0)),ld(X0,X0)),ld(X0,X0)) = ld(ld(mult(X1,rd(X1,X0)),X1),rd(rd(X0,X1),ld(X0,X0))),
inference(forward_demodulation,[],[f19159,f11133]) ).
fof(f19295,plain,
! [X0,X1] : ld(mult(ld(X0,X0),ld(X0,X0)),ld(X0,X0)) = ld(ld(mult(X1,rd(X1,X0)),X1),rd(rd(X0,X1),ld(X0,X0))),
inference(forward_demodulation,[],[f19241,f3952]) ).
fof(f19338,plain,
! [X0,X1] : ld(ld(X0,X0),mult(X0,ld(mult(X0,X0),X0))) = ld(ld(mult(X1,rd(X1,X0)),X1),rd(rd(X0,X1),ld(X0,X0))),
inference(forward_demodulation,[],[f19295,f5078]) ).
fof(f19369,plain,
! [X0,X1] : mult(ld(X0,X0),mult(X0,ld(mult(X0,X0),X0))) = ld(ld(mult(X1,rd(X1,X0)),X1),rd(rd(X0,X1),ld(X0,X0))),
inference(forward_demodulation,[],[f19338,f1508]) ).
fof(f19393,plain,
! [X0,X1] : ld(X0,mult(mult(X0,X0),ld(mult(X0,X0),X0))) = ld(ld(mult(X1,rd(X1,X0)),X1),rd(rd(X0,X1),ld(X0,X0))),
inference(forward_demodulation,[],[f19369,f120]) ).
fof(f19408,plain,
! [X0,X1] : ld(X0,X0) = ld(ld(mult(X1,rd(X1,X0)),X1),rd(rd(X0,X1),ld(X0,X0))),
inference(forward_demodulation,[],[f19393,f1]) ).
fof(f22279,plain,
! [X2,X0,X1] : ld(ld(X0,X0),mult(X1,ld(ld(X0,X0),X2))) = mult(mult(ld(X0,X0),rd(X1,ld(X0,X0))),X2),
inference(superposition,[],[f369,f1508]) ).
fof(f22529,plain,
! [X2,X0,X1] : ld(ld(X0,X0),mult(X1,ld(ld(X0,X0),X2))) = mult(rd(mult(ld(X0,X0),mult(X1,X0)),X0),X2),
inference(forward_demodulation,[],[f22279,f1559]) ).
fof(f22643,plain,
! [X2,X0,X1] : mult(ld(X0,X0),mult(X1,ld(ld(X0,X0),X2))) = mult(rd(mult(ld(X0,X0),mult(X1,X0)),X0),X2),
inference(forward_demodulation,[],[f22529,f1508]) ).
fof(f22727,plain,
! [X2,X0,X1] : mult(ld(X0,X0),mult(X1,mult(ld(X0,X0),X2))) = mult(rd(mult(ld(X0,X0),mult(X1,X0)),X0),X2),
inference(forward_demodulation,[],[f22643,f1508]) ).
fof(f23350,plain,
! [X2,X0,X1] : ld(mult(X0,X1),rd(X0,X1)) = ld(mult(mult(X2,X1),X1),X2),
inference(superposition,[],[f10462,f10126]) ).
fof(f24883,plain,
! [X2,X0,X1] : ld(X1,X0) = rd(mult(X0,ld(ld(X1,X0),X2)),mult(ld(ld(X1,X0),X1),X2)),
inference(superposition,[],[f4,f162]) ).
fof(f24906,plain,
! [X2,X0,X1] : ld(mult(ld(X1,X0),ld(X1,X0)),ld(X1,X0)) = rd(mult(ld(ld(X1,X0),X1),X2),mult(X0,ld(ld(X1,X0),X2))),
inference(superposition,[],[f4507,f162]) ).
fof(f24924,plain,
! [X2,X0,X1] : ld(ld(X1,X0),mult(X1,ld(mult(X0,X1),X0))) = rd(mult(ld(ld(X1,X0),X1),X2),mult(X0,ld(ld(X1,X0),X2))),
inference(forward_demodulation,[],[f24906,f5078]) ).
fof(f26135,plain,
! [X2,X3,X0,X1] : mult(mult(X2,mult(mult(X0,X1),X0)),X3) = mult(mult(mult(X0,X1),X0),mult(mult(rd(X3,mult(X0,mult(X1,mult(X0,X3)))),X2),mult(X0,mult(X1,mult(X0,X3))))),
inference(superposition,[],[f590,f14]) ).
fof(f26144,plain,
! [X0,X1] : mult(mult(X1,ld(X0,X0)),X0) = mult(ld(X0,X0),mult(mult(ld(X0,X0),X1),X0)),
inference(superposition,[],[f590,f1406]) ).
fof(f26358,plain,
! [X2,X3,X0,X1] : mult(mult(X2,mult(mult(X0,X1),X0)),X3) = mult(X0,mult(X1,mult(X0,mult(mult(rd(X3,mult(X0,mult(X1,mult(X0,X3)))),X2),mult(X0,mult(X1,mult(X0,X3))))))),
inference(forward_demodulation,[],[f26135,f5]) ).
fof(f26461,plain,
! [X2,X3,X0,X1] : mult(mult(X2,mult(mult(X0,X1),X0)),X3) = mult(X0,mult(X1,mult(X0,mult(ld(mult(mult(X0,X1),X0),X2),mult(X0,mult(X1,mult(X0,X3))))))),
inference(forward_demodulation,[],[f26358,f653]) ).
fof(f26519,plain,
! [X2,X3,X0,X1] : mult(mult(X2,mult(mult(X0,X1),X0)),X3) = mult(X0,mult(X1,mult(mult(ld(X1,ld(X0,X2)),X0),mult(X1,mult(X0,X3))))),
inference(forward_demodulation,[],[f26461,f3115]) ).
fof(f27097,plain,
! [X2,X3,X0,X1] : ld(ld(X1,X0),rd(X3,ld(X1,X0))) = mult(ld(ld(X1,X0),X3),rd(mult(ld(ld(X1,X0),X1),X2),mult(X0,ld(ld(X1,X0),X2)))),
inference(superposition,[],[f3790,f162]) ).
fof(f27241,plain,
! [X3,X0,X1] : ld(ld(X1,X0),rd(X3,ld(X1,X0))) = mult(ld(ld(X1,X0),X3),ld(ld(X1,X0),mult(X1,ld(mult(X0,X1),X0)))),
inference(forward_demodulation,[],[f27097,f24924]) ).
fof(f28531,plain,
! [X2,X0,X1] : ld(X0,rd(X1,mult(X0,X1))) = ld(mult(mult(X2,X0),X0),X2),
inference(superposition,[],[f10462,f3897]) ).
fof(f32769,plain,
! [X2,X0,X1] : rd(rd(X2,X1),X1) = mult(X2,ld(mult(mult(X0,X1),X1),X0)),
inference(superposition,[],[f13502,f10462]) ).
fof(f35194,plain,
! [X2,X0,X1] : mult(ld(mult(X0,X0),X1),ld(X1,X2)) = mult(X1,mult(ld(X1,ld(mult(X0,mult(X0,X0)),X0)),X2)),
inference(superposition,[],[f112,f5156]) ).
fof(f38607,plain,
! [X2,X0,X1] : rd(X2,mult(X0,ld(mult(X1,X0),X1))) = mult(mult(X2,mult(X0,ld(mult(X1,X0),X1))),mult(X0,ld(mult(X1,X0),X1))),
inference(superposition,[],[f6637,f3079]) ).
fof(f38944,plain,
! [X0,X1] : ld(mult(ld(X0,X1),ld(X0,X1)),ld(X0,X1)) = rd(rd(ld(X0,X1),X0),rd(mult(rd(ld(X0,X1),X0),X1),X0)),
inference(superposition,[],[f4507,f3713]) ).
fof(f38966,plain,
! [X0,X1] : ld(ld(X0,X1),mult(X0,ld(mult(X1,X0),X1))) = rd(rd(ld(X0,X1),X0),rd(mult(rd(ld(X0,X1),X0),X1),X0)),
inference(forward_demodulation,[],[f38944,f5078]) ).
fof(f49306,plain,
! [X2,X3,X0,X1] : rd(rd(X2,rd(X1,X0)),rd(X3,mult(rd(X0,X1),X3))) = ld(rd(X0,X1),mult(rd(mult(rd(X0,X1),mult(X2,X0)),X1),rd(X0,X1))),
inference(superposition,[],[f5914,f615]) ).
fof(f49348,plain,
! [X2,X3,X0,X1] : rd(rd(X2,rd(X1,X0)),rd(X3,mult(rd(X0,X1),X3))) = mult(rd(mult(X2,X0),mult(rd(X0,X1),X1)),mult(rd(X0,X1),rd(X0,X1))),
inference(forward_demodulation,[],[f49306,f2846]) ).
fof(f49514,plain,
! [X2,X3,X0,X1] : rd(rd(X2,rd(X1,X0)),rd(X3,mult(rd(X0,X1),X3))) = mult(rd(mult(X2,X0),X0),mult(rd(X0,X1),rd(X0,X1))),
inference(forward_demodulation,[],[f49348,f3]) ).
fof(f49651,plain,
! [X2,X3,X0,X1] : mult(X2,mult(rd(X0,X1),rd(X0,X1))) = rd(rd(X2,rd(X1,X0)),rd(X3,mult(rd(X0,X1),X3))),
inference(forward_demodulation,[],[f49514,f4]) ).
fof(f49742,plain,
! [X2,X0,X1] : mult(X2,mult(rd(X0,X1),rd(X0,X1))) = rd(rd(X2,rd(X1,X0)),rd(X1,X0)),
inference(forward_demodulation,[],[f49651,f485]) ).
fof(f50923,plain,
! [X2,X0,X1] : rd(X0,rd(X2,X1)) = mult(mult(X0,mult(rd(X1,X2),rd(X1,X2))),rd(X2,X1)),
inference(superposition,[],[f3,f49742]) ).
fof(f53225,plain,
! [X0,X1] : mult(mult(ld(mult(X0,X0),X0),X1),ld(X0,X0)) = mult(ld(mult(X0,X0),X0),mult(mult(X1,rd(ld(X0,X0),ld(mult(X0,X0),X0))),ld(mult(X0,X0),X0))),
inference(superposition,[],[f617,f5105]) ).
fof(f53278,plain,
! [X0,X1] : mult(mult(ld(mult(X0,X0),X0),X1),ld(X0,X0)) = ld(X0,mult(mult(X1,rd(ld(X0,X0),ld(mult(X0,X0),X0))),ld(mult(X0,X0),X0))),
inference(forward_demodulation,[],[f53225,f4519]) ).
fof(f53352,plain,
! [X0,X1] : mult(mult(ld(mult(X0,X0),X0),X1),ld(X0,X0)) = ld(X0,mult(mult(X1,ld(X0,mult(mult(X0,ld(X0,X0)),X0))),ld(mult(X0,X0),X0))),
inference(forward_demodulation,[],[f53278,f4517]) ).
fof(f53421,plain,
! [X0,X1] : mult(mult(ld(mult(X0,X0),X0),X1),ld(X0,X0)) = ld(X0,mult(mult(X1,ld(X0,mult(X0,X0))),ld(mult(X0,X0),X0))),
inference(forward_demodulation,[],[f53352,f1]) ).
fof(f53486,plain,
! [X0,X1] : mult(mult(ld(mult(X0,X0),X0),X1),ld(X0,X0)) = ld(X0,mult(mult(X1,X0),ld(mult(X0,X0),X0))),
inference(forward_demodulation,[],[f53421,f2]) ).
fof(f53542,plain,
! [X0,X1] : mult(ld(X0,X1),ld(X0,X0)) = ld(X0,mult(mult(X1,X0),ld(mult(X0,X0),X0))),
inference(forward_demodulation,[],[f53486,f4519]) ).
fof(f54958,plain,
! [X0,X1] : mult(X0,ld(mult(X1,X0),X1)) = mult(mult(mult(X0,ld(mult(X1,X0),X1)),mult(X0,ld(mult(X1,X0),X1))),rd(ld(X0,X1),ld(X0,X1))),
inference(superposition,[],[f4764,f3267]) ).
fof(f54971,plain,
! [X0,X1] : ld(mult(ld(X0,X1),mult(ld(X0,X1),ld(X0,X1))),ld(X0,X1)) = ld(mult(ld(X0,X1),ld(X0,X1)),mult(X0,ld(mult(X1,X0),X1))),
inference(superposition,[],[f10462,f3267]) ).
fof(f54988,plain,
! [X0,X1] : rd(mult(X0,ld(mult(X1,X0),X1)),mult(ld(X0,X1),ld(X0,X1))) = ld(mult(ld(X0,X1),ld(X0,X1)),mult(X0,ld(mult(X1,X0),X1))),
inference(forward_demodulation,[],[f54971,f6931]) ).
fof(f54999,plain,
! [X0,X1] : mult(X0,ld(mult(X1,X0),X1)) = mult(mult(mult(X0,ld(mult(X1,X0),X1)),mult(X0,ld(mult(X1,X0),X1))),ld(ld(X0,X1),ld(X0,X1))),
inference(forward_demodulation,[],[f54958,f1406]) ).
fof(f55166,plain,
! [X0,X1] : ld(ld(X0,X1),ld(ld(X0,X1),mult(X0,ld(mult(X1,X0),X1)))) = ld(mult(ld(X0,X1),ld(X0,X1)),mult(X0,ld(mult(X1,X0),X1))),
inference(backward_demodulation,[],[f5138,f54988]) ).
fof(f55189,plain,
! [X0,X1] : mult(X0,ld(mult(X1,X0),X1)) = mult(mult(mult(X0,ld(mult(X1,X0),X1)),mult(X0,ld(mult(X1,X0),X1))),mult(X0,ld(mult(X1,X0),X1))),
inference(forward_demodulation,[],[f54999,f3079]) ).
fof(f55327,plain,
! [X0,X1] : mult(X0,ld(mult(X1,X0),X1)) = rd(mult(X0,ld(mult(X1,X0),X1)),mult(X0,ld(mult(X1,X0),X1))),
inference(forward_demodulation,[],[f55189,f38607]) ).
fof(f55429,plain,
! [X0,X1] : mult(X0,ld(mult(X1,X0),X1)) = ld(mult(X0,ld(mult(X1,X0),X1)),mult(X0,ld(mult(X1,X0),X1))),
inference(forward_demodulation,[],[f55327,f1406]) ).
fof(f55498,plain,
! [X0,X1] : mult(X0,ld(mult(X1,X0),X1)) = mult(mult(X0,ld(mult(X1,X0),X1)),mult(X0,ld(mult(X1,X0),X1))),
inference(forward_demodulation,[],[f55429,f3263]) ).
fof(f55676,plain,
! [X2,X0,X1] : ld(mult(ld(X0,X1),ld(X0,X1)),X2) = mult(ld(ld(X0,X1),rd(rd(ld(X0,X1),X0),rd(mult(rd(ld(X0,X1),X0),X1),X0))),X2),
inference(superposition,[],[f4790,f3713]) ).
fof(f56188,plain,
! [X2,X0,X1] : ld(mult(ld(X0,X1),ld(X0,X1)),X2) = mult(ld(ld(X0,X1),ld(ld(X0,X1),mult(X0,ld(mult(X1,X0),X1)))),X2),
inference(forward_demodulation,[],[f55676,f38966]) ).
fof(f56416,plain,
! [X2,X0,X1] : ld(mult(ld(X0,X1),ld(X0,X1)),X2) = mult(ld(mult(ld(X0,X1),ld(X0,X1)),mult(X0,ld(mult(X1,X0),X1))),X2),
inference(forward_demodulation,[],[f56188,f55166]) ).
fof(f65581,plain,
! [X2,X0,X1] : mult(mult(rd(X0,rd(X1,mult(X0,X1))),X2),rd(X1,mult(X0,X1))) = mult(rd(X0,rd(X1,mult(X0,X1))),mult(mult(X2,ld(X0,rd(X1,mult(X0,X1)))),X0)),
inference(superposition,[],[f617,f3965]) ).
fof(f65658,plain,
! [X2,X0,X1] : mult(mult(rd(X0,rd(X1,mult(X0,X1))),X2),rd(X1,mult(X0,X1))) = mult(rd(X0,rd(X1,mult(X0,X1))),mult(rd(rd(X2,X0),X0),X0)),
inference(forward_demodulation,[],[f65581,f13563]) ).
fof(f65777,plain,
! [X2,X0,X1] : mult(mult(rd(X0,rd(X1,mult(X0,X1))),X2),rd(X1,mult(X0,X1))) = mult(rd(X0,rd(X1,mult(X0,X1))),rd(X2,X0)),
inference(forward_demodulation,[],[f65658,f3]) ).
fof(f65873,plain,
! [X2,X0,X1] : mult(mult(X0,X0),rd(X2,X0)) = mult(mult(mult(X0,X0),X2),rd(X1,mult(X0,X1))),
inference(forward_demodulation,[],[f65777,f4765]) ).
fof(f94788,plain,
! [X2,X3,X0,X1] : rd(rd(X3,ld(X0,X1)),ld(X0,X1)) = mult(X3,ld(ld(X0,X1),mult(mult(X0,rd(ld(mult(X1,X0),X2),X2)),X0))),
inference(superposition,[],[f13563,f3291]) ).
fof(f108893,plain,
! [X2,X0,X1] : rd(rd(X1,ld(X2,X0)),ld(X2,X0)) = mult(X1,ld(mult(X0,ld(X2,X0)),X2)),
inference(superposition,[],[f32769,f1]) ).
fof(f109562,plain,
! [X2,X3,X0,X1] : mult(X3,ld(ld(X0,X1),mult(mult(X0,rd(ld(mult(X1,X0),X2),X2)),X0))) = mult(X3,ld(mult(X1,ld(X0,X1)),X0)),
inference(backward_demodulation,[],[f94788,f108893]) ).
fof(f119617,plain,
! [X0,X1] : ld(mult(X0,X0),mult(mult(X0,X1),X0)) = mult(X0,mult(ld(mult(X0,X0),X1),X0)),
inference(superposition,[],[f1,f8254]) ).
fof(f124434,plain,
! [X2,X3,X0,X1] : rd(X2,ld(X0,X1)) = mult(mult(X2,mult(rd(mult(ld(ld(X0,X1),X0),X3),mult(X1,ld(ld(X0,X1),X3))),rd(mult(ld(ld(X0,X1),X0),X3),mult(X1,ld(ld(X0,X1),X3))))),ld(X0,X1)),
inference(superposition,[],[f50923,f24883]) ).
fof(f124486,plain,
! [X0,X1] : tuple(x1(rd(rd(X0,X1),rd(X0,X1))),x1_2(rd(rd(X0,X1),rd(X0,X1)))) != tuple(mult(rd(X0,X1),mult(mult(rd(X1,X0),rd(X1,X0)),mult(rd(X0,X1),x1(rd(rd(X0,X1),rd(X0,X1)))))),mult(x1_2(rd(rd(X0,X1),rd(X0,X1))),rd(rd(X0,X1),rd(X0,X1)))),
inference(superposition,[],[f17,f50923]) ).
fof(f124647,plain,
! [X0,X1] : tuple(x1(ld(rd(X0,X1),rd(X0,X1))),x1_2(ld(rd(X0,X1),rd(X0,X1)))) != tuple(mult(rd(X0,X1),mult(mult(rd(X1,X0),rd(X1,X0)),mult(rd(X0,X1),x1(ld(rd(X0,X1),rd(X0,X1)))))),mult(x1_2(ld(rd(X0,X1),rd(X0,X1))),ld(rd(X0,X1),rd(X0,X1)))),
inference(forward_demodulation,[],[f124486,f1406]) ).
fof(f124698,plain,
! [X2,X0,X1] : rd(X2,ld(X0,X1)) = mult(mult(X2,mult(ld(ld(X0,X1),mult(X0,ld(mult(X1,X0),X1))),ld(ld(X0,X1),mult(X0,ld(mult(X1,X0),X1))))),ld(X0,X1)),
inference(forward_demodulation,[],[f124434,f24924]) ).
fof(f124880,plain,
! [X0,X1] : tuple(x1(mult(rd(X1,X0),rd(X0,X1))),x1_2(mult(rd(X1,X0),rd(X0,X1)))) != tuple(mult(rd(X0,X1),mult(mult(rd(X1,X0),rd(X1,X0)),mult(rd(X0,X1),x1(mult(rd(X1,X0),rd(X0,X1)))))),mult(x1_2(mult(rd(X1,X0),rd(X0,X1))),mult(rd(X1,X0),rd(X0,X1)))),
inference(forward_demodulation,[],[f124647,f533]) ).
fof(f124926,plain,
! [X2,X0,X1] : rd(X2,ld(X0,X1)) = mult(mult(X2,ld(ld(X0,X1),rd(mult(X0,ld(mult(X1,X0),X1)),ld(X0,X1)))),ld(X0,X1)),
inference(forward_demodulation,[],[f124698,f27241]) ).
fof(f125073,plain,
! [X0,X1] : tuple(x1(mult(rd(X1,X0),rd(X0,X1))),x1_2(mult(rd(X1,X0),rd(X0,X1)))) != tuple(mult(rd(X0,X1),mult(rd(X1,X0),mult(mult(rd(X0,X1),rd(X1,X0)),x1(mult(rd(X1,X0),rd(X0,X1)))))),mult(x1_2(mult(rd(X1,X0),rd(X0,X1))),mult(rd(X1,X0),rd(X0,X1)))),
inference(forward_demodulation,[],[f124880,f690]) ).
fof(f125100,plain,
! [X2,X0,X1] : rd(X2,ld(X0,X1)) = mult(mult(X2,ld(ld(X0,X1),mult(mult(X0,rd(ld(mult(X1,X0),X1),X1)),X0))),ld(X0,X1)),
inference(forward_demodulation,[],[f124926,f31]) ).
fof(f125206,plain,
! [X0,X1] : tuple(x1(mult(rd(X1,X0),rd(X0,X1))),x1_2(mult(rd(X1,X0),rd(X0,X1)))) != tuple(mult(mult(rd(X0,X1),rd(X1,X0)),x1(mult(rd(X1,X0),rd(X0,X1)))),mult(x1_2(mult(rd(X1,X0),rd(X0,X1))),mult(rd(X1,X0),rd(X0,X1)))),
inference(forward_demodulation,[],[f125073,f667]) ).
fof(f125219,plain,
! [X2,X0,X1] : rd(X2,ld(X0,X1)) = mult(mult(X2,ld(mult(X1,ld(X0,X1)),X0)),ld(X0,X1)),
inference(forward_demodulation,[],[f125100,f109562]) ).
fof(f126680,plain,
! [X2,X3,X0,X1,X4] : ld(X4,rd(mult(mult(X0,mult(X1,mult(X0,X2))),mult(mult(X0,X1),X0)),X4)) = rd(ld(X4,mult(X0,mult(X1,mult(X0,mult(X2,mult(X0,mult(X1,mult(X0,X3)))))))),mult(X4,X3)),
inference(superposition,[],[f195,f19]) ).
fof(f126754,plain,
! [X2,X3,X0,X1] : mult(mult(mult(X0,X1),X0),mult(ld(mult(mult(X0,X1),X0),ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2))))),mult(X0,mult(X1,mult(X0,X2))))) = rd(mult(ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2)))),mult(X0,mult(X1,mult(X0,mult(X2,mult(X0,mult(X1,mult(X0,X3)))))))),mult(mult(mult(X0,X1),X0),X3)),
inference(superposition,[],[f138,f19]) ).
fof(f126757,plain,
! [X2,X0,X1] : mult(ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2)))),ld(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0))) = ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,mult(X2,mult(X0,mult(X1,mult(X0,ld(mult(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0)),mult(mult(X0,X1),X0)))))))))),
inference(superposition,[],[f53542,f19]) ).
fof(f126939,plain,
! [X2,X0,X1] : mult(ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2)))),ld(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0))) = ld(X0,ld(X1,mult(X1,mult(X0,mult(X2,mult(X0,mult(X1,mult(X0,ld(mult(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0)),mult(mult(X0,X1),X0)))))))))),
inference(forward_demodulation,[],[f126757,f2576]) ).
fof(f126942,plain,
! [X2,X3,X0,X1] : mult(mult(mult(X0,X1),X0),mult(ld(mult(mult(X0,X1),X0),ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2))))),mult(X0,mult(X1,mult(X0,X2))))) = rd(mult(ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2)))),mult(X0,mult(X1,mult(X0,mult(X2,mult(X0,mult(X1,mult(X0,X3)))))))),mult(X0,mult(X1,mult(X0,X3)))),
inference(forward_demodulation,[],[f126754,f5]) ).
fof(f127356,plain,
! [X2,X0,X1] : mult(ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2)))),ld(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0))) = ld(X0,mult(X0,mult(X2,mult(X0,mult(X1,mult(X0,ld(mult(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0)),mult(mult(X0,X1),X0)))))))),
inference(forward_demodulation,[],[f126939,f2]) ).
fof(f127359,plain,
! [X2,X3,X0,X1] : mult(mult(mult(X0,X1),X0),mult(ld(mult(mult(X0,X1),X0),ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2))))),mult(X0,mult(X1,mult(X0,X2))))) = rd(ld(mult(mult(X0,X1),X0),mult(mult(mult(X0,mult(X1,mult(X0,X2))),mult(mult(X0,X1),X0)),mult(X2,mult(X0,mult(X1,mult(X0,X3)))))),mult(X0,mult(X1,mult(X0,X3)))),
inference(forward_demodulation,[],[f126942,f144]) ).
fof(f127636,plain,
! [X2,X0,X1] : mult(X2,mult(X0,mult(X1,mult(X0,ld(mult(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0)),mult(mult(X0,X1),X0)))))) = mult(ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2)))),ld(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0))),
inference(forward_demodulation,[],[f127356,f2]) ).
fof(f127639,plain,
! [X2,X3,X0,X1] : mult(mult(mult(X0,X1),X0),mult(ld(mult(mult(X0,X1),X0),ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2))))),mult(X0,mult(X1,mult(X0,X2))))) = rd(ld(X0,mult(mult(ld(X1,mult(X1,mult(X0,X2))),X0),mult(X1,mult(X0,mult(X2,mult(X0,mult(X1,mult(X0,X3)))))))),mult(X0,mult(X1,mult(X0,X3)))),
inference(forward_demodulation,[],[f127359,f2831]) ).
fof(f127842,plain,
! [X2,X0,X1] : mult(X2,mult(X0,mult(X1,mult(X0,ld(mult(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0)),mult(mult(X0,X1),X0)))))) = mult(ld(X0,ld(X1,mult(X1,mult(X0,X2)))),ld(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0))),
inference(forward_demodulation,[],[f127636,f2576]) ).
fof(f127845,plain,
! [X2,X3,X0,X1] : mult(mult(mult(X0,X1),X0),mult(ld(mult(mult(X0,X1),X0),ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2))))),mult(X0,mult(X1,mult(X0,X2))))) = rd(ld(X0,mult(mult(mult(X0,X2),X0),mult(X1,mult(X0,mult(X2,mult(X0,mult(X1,mult(X0,X3)))))))),mult(X0,mult(X1,mult(X0,X3)))),
inference(forward_demodulation,[],[f127639,f2]) ).
fof(f127985,plain,
! [X2,X0,X1] : mult(X2,mult(X0,mult(X1,mult(X0,ld(mult(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0)),mult(mult(X0,X1),X0)))))) = mult(ld(X0,mult(X0,X2)),ld(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0))),
inference(forward_demodulation,[],[f127842,f2]) ).
fof(f127988,plain,
! [X2,X3,X0,X1] : mult(mult(mult(X0,X1),X0),mult(ld(mult(mult(X0,X1),X0),ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2))))),mult(X0,mult(X1,mult(X0,X2))))) = rd(ld(X0,mult(X0,mult(X2,mult(X0,mult(X1,mult(X0,mult(X2,mult(X0,mult(X1,mult(X0,X3)))))))))),mult(X0,mult(X1,mult(X0,X3)))),
inference(forward_demodulation,[],[f127845,f5]) ).
fof(f128095,plain,
! [X2,X0,X1] : mult(X2,ld(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0))) = mult(X2,mult(X0,mult(X1,mult(X0,ld(mult(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0)),mult(mult(X0,X1),X0)))))),
inference(forward_demodulation,[],[f127985,f2]) ).
fof(f128098,plain,
! [X2,X0,X1] : mult(mult(mult(X0,X1),X0),mult(ld(mult(mult(X0,X1),X0),ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2))))),mult(X0,mult(X1,mult(X0,X2))))) = ld(X0,rd(mult(mult(X0,mult(X2,mult(X0,X1))),mult(mult(X0,X2),X0)),X0)),
inference(forward_demodulation,[],[f127988,f126680]) ).
fof(f128196,plain,
! [X2,X0,X1] : mult(X2,ld(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0))) = mult(X2,mult(X0,mult(X1,mult(mult(X0,ld(mult(mult(X0,X1),X0),ld(mult(X0,X0),X0))),X0)))),
inference(forward_demodulation,[],[f128095,f4557]) ).
fof(f128198,plain,
! [X2,X0,X1] : ld(X0,rd(mult(mult(X0,mult(X2,mult(X0,X1))),mult(mult(X0,X2),X0)),X0)) = mult(X0,mult(X1,mult(X0,mult(ld(mult(mult(X0,X1),X0),ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2))))),mult(X0,mult(X1,mult(X0,X2))))))),
inference(forward_demodulation,[],[f128098,f5]) ).
fof(f128269,plain,
! [X2,X0,X1] : mult(X2,ld(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0))) = mult(X2,mult(X0,mult(X1,mult(ld(X1,ld(X0,ld(mult(X0,X0),X0))),X0)))),
inference(forward_demodulation,[],[f128196,f2909]) ).
fof(f128270,plain,
! [X2,X0,X1] : ld(X0,rd(mult(mult(X0,mult(X2,mult(X0,X1))),mult(mult(X0,X2),X0)),X0)) = mult(X0,mult(X1,mult(mult(ld(X1,ld(X0,ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2)))))),X0),mult(X1,mult(X0,X2))))),
inference(forward_demodulation,[],[f128198,f3115]) ).
fof(f128325,plain,
! [X2,X0,X1] : mult(X2,ld(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0))) = mult(X2,mult(X0,mult(X1,mult(ld(X1,ld(mult(X0,mult(X0,X0)),X0)),X0)))),
inference(forward_demodulation,[],[f128269,f5130]) ).
fof(f128326,plain,
! [X2,X0,X1] : ld(X0,rd(mult(mult(X0,mult(X2,mult(X0,X1))),mult(mult(X0,X2),X0)),X0)) = mult(mult(ld(mult(mult(X0,X1),X0),mult(X0,mult(X1,mult(X0,X2)))),mult(mult(X0,X1),X0)),X2),
inference(forward_demodulation,[],[f128270,f26519]) ).
fof(f128376,plain,
! [X2,X0,X1] : mult(X2,ld(mult(mult(X0,X1),X0),mult(mult(X0,X1),X0))) = mult(X2,mult(X0,mult(ld(mult(X0,X0),X1),ld(X1,X0)))),
inference(forward_demodulation,[],[f128325,f35194]) ).
fof(f128377,plain,
! [X2,X0,X1] : ld(X0,rd(mult(mult(X0,mult(X2,mult(X0,X1))),mult(mult(X0,X2),X0)),X0)) = mult(mult(ld(X0,ld(X1,mult(X1,mult(X0,X2)))),mult(mult(X0,X1),X0)),X2),
inference(forward_demodulation,[],[f128326,f2576]) ).
fof(f128420,plain,
! [X2,X0,X1] : ld(X0,rd(mult(mult(X0,mult(X2,mult(X0,X1))),mult(mult(X0,X2),X0)),X0)) = mult(mult(ld(X0,mult(X0,X2)),mult(mult(X0,X1),X0)),X2),
inference(forward_demodulation,[],[f128377,f2]) ).
fof(f128452,plain,
! [X2,X0,X1] : mult(mult(X2,mult(mult(X0,X1),X0)),X2) = ld(X0,rd(mult(mult(X0,mult(X2,mult(X0,X1))),mult(mult(X0,X2),X0)),X0)),
inference(forward_demodulation,[],[f128420,f2]) ).
fof(f128684,plain,
! [X0,X1] : mult(ld(mult(ld(X0,X0),ld(X0,X0)),X1),ld(X1,ld(X0,X0))) = mult(ld(X0,X0),ld(mult(mult(ld(X0,X0),X1),ld(X0,X0)),mult(mult(ld(X0,X0),X1),ld(X0,X0)))),
inference(superposition,[],[f2227,f128376]) ).
fof(f129057,plain,
! [X0,X1] : mult(ld(mult(ld(X0,X0),ld(X0,X0)),X1),ld(X1,ld(X0,X0))) = ld(X1,ld(ld(X0,X0),mult(mult(ld(X0,X0),X1),ld(X0,X0)))),
inference(forward_demodulation,[],[f128684,f2909]) ).
fof(f129416,plain,
! [X0,X1] : mult(ld(mult(ld(X0,X0),ld(X0,X0)),X1),ld(X1,ld(X0,X0))) = ld(X1,mult(ld(X0,X0),mult(mult(ld(X0,X0),X1),ld(X0,X0)))),
inference(forward_demodulation,[],[f129057,f1508]) ).
fof(f129623,plain,
! [X0,X1] : mult(ld(mult(ld(X0,X0),ld(X0,X0)),X1),ld(X1,ld(X0,X0))) = ld(X1,mult(ld(X0,X0),rd(mult(ld(X0,X0),mult(X1,X0)),X0))),
inference(forward_demodulation,[],[f129416,f1522]) ).
fof(f129770,plain,
! [X0,X1] : mult(ld(mult(ld(X0,X0),ld(X0,X0)),X1),ld(X1,ld(X0,X0))) = ld(X1,rd(rd(mult(X1,X0),X0),ld(X0,X0))),
inference(forward_demodulation,[],[f129623,f3453]) ).
fof(f129901,plain,
! [X0,X1] : ld(X1,rd(X1,ld(X0,X0))) = mult(ld(mult(ld(X0,X0),ld(X0,X0)),X1),ld(X1,ld(X0,X0))),
inference(forward_demodulation,[],[f129770,f4]) ).
fof(f130016,plain,
! [X0,X1] : ld(X1,rd(X1,ld(X0,X0))) = mult(ld(ld(mult(X0,X0),mult(X0,X0)),X1),ld(X1,ld(X0,X0))),
inference(forward_demodulation,[],[f129901,f3012]) ).
fof(f130120,plain,
! [X0,X1] : ld(X1,rd(X1,ld(X0,X0))) = mult(mult(ld(mult(X0,X0),mult(X0,X0)),X1),ld(X1,ld(X0,X0))),
inference(forward_demodulation,[],[f130016,f1508]) ).
fof(f130213,plain,
! [X0,X1] : ld(X1,rd(X1,ld(X0,X0))) = mult(X1,mult(ld(X1,ld(mult(X0,X0),mult(X0,X0))),ld(X0,X0))),
inference(forward_demodulation,[],[f130120,f112]) ).
fof(f130293,plain,
! [X0,X1] : mult(X1,mult(ld(X1,ld(X0,X0)),ld(X0,X0))) = ld(X1,rd(X1,ld(X0,X0))),
inference(forward_demodulation,[],[f130213,f3952]) ).
fof(f156586,plain,
! [X2,X0,X1] : ld(mult(X1,ld(X0,X1)),X0) = ld(mult(mult(X2,ld(X0,X1)),ld(X0,X1)),X2),
inference(superposition,[],[f23350,f8]) ).
fof(f156683,plain,
! [X2,X0,X1] : ld(mult(X0,ld(X2,X0)),X2) = ld(mult(X1,ld(X2,X0)),rd(X1,ld(X2,X0))),
inference(superposition,[],[f23350,f1]) ).
fof(f156746,plain,
! [X2,X0,X1] : ld(mult(ld(X0,X1),ld(X0,X1)),mult(X0,ld(mult(X1,X0),X1))) = ld(mult(X2,ld(X0,X1)),rd(X2,ld(X0,X1))),
inference(superposition,[],[f23350,f3267]) ).
fof(f157206,plain,
! [X0,X1] : ld(mult(X1,ld(X0,X1)),X0) = ld(mult(ld(X0,X1),ld(X0,X1)),mult(X0,ld(mult(X1,X0),X1))),
inference(backward_demodulation,[],[f156746,f156683]) ).
fof(f157514,plain,
! [X2,X0,X1] : ld(mult(ld(X0,X1),ld(X0,X1)),X2) = mult(ld(mult(X1,ld(X0,X1)),X0),X2),
inference(backward_demodulation,[],[f56416,f157206]) ).
fof(f157781,plain,
! [X0,X1] : ld(ld(X0,X1),mult(X0,ld(mult(X1,X0),X1))) = mult(ld(mult(X1,ld(X0,X1)),X0),ld(X0,X1)),
inference(backward_demodulation,[],[f5078,f157514]) ).
fof(f204802,plain,
! [X2,X0,X1] : mult(mult(X1,mult(X0,X2)),X1) = ld(X2,rd(mult(mult(X2,mult(X1,X0)),mult(mult(X2,X1),X2)),X2)),
inference(superposition,[],[f128452,f1]) ).
fof(f207334,plain,
! [X2,X0,X1] : mult(mult(X1,mult(ld(X1,X0),X2)),X1) = ld(X2,rd(mult(mult(X2,X0),mult(mult(X2,X1),X2)),X2)),
inference(superposition,[],[f204802,f1]) ).
fof(f209113,plain,
! [X0,X1] : mult(ld(X0,rd(X0,ld(X1,X1))),X0) = ld(ld(X1,X1),rd(mult(mult(ld(X1,X1),ld(X1,X1)),mult(mult(ld(X1,X1),X0),ld(X1,X1))),ld(X1,X1))),
inference(superposition,[],[f207334,f130293]) ).
fof(f210110,plain,
! [X0,X1] : mult(ld(X0,rd(X0,ld(X1,X1))),X0) = mult(ld(X1,X1),rd(mult(mult(ld(X1,X1),ld(X1,X1)),mult(mult(ld(X1,X1),X0),ld(X1,X1))),ld(X1,X1))),
inference(forward_demodulation,[],[f209113,f1508]) ).
fof(f210504,plain,
! [X0,X1] : mult(ld(X0,rd(X0,ld(X1,X1))),X0) = rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),ld(X1,X1)),mult(mult(ld(X1,X1),X0),ld(X1,X1))),X1)),X1),
inference(forward_demodulation,[],[f210110,f1559]) ).
fof(f210779,plain,
! [X0,X1] : mult(ld(X0,rd(X0,ld(X1,X1))),X0) = rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),ld(X1,X1)),rd(mult(ld(X1,X1),mult(X0,X1)),X1)),X1)),X1),
inference(forward_demodulation,[],[f210504,f1522]) ).
fof(f210972,plain,
! [X0,X1] : mult(ld(X0,rd(X0,ld(X1,X1))),X0) = rd(mult(ld(X1,X1),mult(mult(ld(mult(X1,X1),mult(X1,X1)),rd(mult(ld(X1,X1),mult(X0,X1)),X1)),X1)),X1),
inference(forward_demodulation,[],[f210779,f3012]) ).
fof(f211107,plain,
! [X0,X1] : mult(ld(X0,rd(X0,ld(X1,X1))),X0) = rd(mult(ld(X1,X1),mult(mult(ld(X1,X1),rd(mult(ld(X1,X1),mult(X0,X1)),X1)),X1)),X1),
inference(forward_demodulation,[],[f210972,f3952]) ).
fof(f211205,plain,
! [X0,X1] : mult(ld(X0,rd(X0,ld(X1,X1))),X0) = rd(mult(mult(rd(mult(ld(X1,X1),mult(X0,X1)),X1),ld(X1,X1)),X1),X1),
inference(forward_demodulation,[],[f211107,f26144]) ).
fof(f211258,plain,
! [X0,X1] : mult(ld(X0,rd(X0,ld(X1,X1))),X0) = mult(rd(mult(ld(X1,X1),mult(X0,X1)),X1),ld(X1,X1)),
inference(forward_demodulation,[],[f211205,f4]) ).
fof(f211294,plain,
! [X0,X1] : mult(ld(X0,rd(X0,ld(X1,X1))),X0) = mult(ld(X1,X1),mult(X0,mult(ld(X1,X1),ld(X1,X1)))),
inference(forward_demodulation,[],[f211258,f22727]) ).
fof(f211315,plain,
! [X0,X1] : mult(ld(X0,rd(X0,ld(X1,X1))),X0) = mult(ld(X1,X1),mult(X0,ld(mult(X1,X1),mult(X1,X1)))),
inference(forward_demodulation,[],[f211294,f3012]) ).
fof(f211326,plain,
! [X0,X1] : mult(ld(X1,X1),mult(X0,ld(X1,X1))) = mult(ld(X0,rd(X0,ld(X1,X1))),X0),
inference(forward_demodulation,[],[f211315,f3952]) ).
fof(f211422,plain,
! [X0,X1] : rd(rd(X1,X0),ld(ld(X1,X1),ld(ld(X1,X1),rd(X1,X0)))) = mult(mult(ld(X1,X1),mult(ld(X1,X1),ld(ld(mult(X0,rd(X0,X1)),X0),rd(X1,X0)))),ld(X1,X1)),
inference(superposition,[],[f3180,f18352]) ).
fof(f211481,plain,
! [X0,X1] : mult(ld(mult(X0,ld(X1,X1)),X0),ld(X1,X1)) = rd(X0,ld(ld(X1,X1),ld(ld(X1,X1),X0))),
inference(superposition,[],[f3180,f2227]) ).
fof(f211509,plain,
! [X2,X0,X1] : ld(X1,ld(mult(X1,ld(mult(X0,X1),X0)),X2)) = ld(rd(X0,ld(X1,ld(X1,X0))),mult(X1,X2)),
inference(superposition,[],[f2576,f3180]) ).
fof(f211750,plain,
! [X2,X0,X1] : ld(X1,ld(mult(X1,ld(mult(X0,X1),X0)),X2)) = mult(rd(ld(X1,ld(X1,X0)),X0),mult(X1,X2)),
inference(forward_demodulation,[],[f211509,f533]) ).
fof(f211774,plain,
! [X0,X1] : mult(ld(mult(X0,ld(X1,X1)),X0),ld(X1,X1)) = rd(X0,mult(ld(X1,X1),ld(ld(X1,X1),X0))),
inference(forward_demodulation,[],[f211481,f1508]) ).
fof(f211825,plain,
! [X0,X1] : rd(rd(X1,X0),ld(ld(X1,X1),ld(ld(X1,X1),rd(X1,X0)))) = rd(mult(ld(X1,X1),mult(mult(ld(X1,X1),ld(ld(mult(X0,rd(X0,X1)),X0),rd(X1,X0))),X1)),X1),
inference(forward_demodulation,[],[f211422,f1522]) ).
fof(f211953,plain,
! [X2,X0,X1] : ld(X1,mult(mult(X1,ld(mult(X0,X1),X0)),X2)) = mult(rd(ld(X1,ld(X1,X0)),X0),mult(X1,X2)),
inference(forward_demodulation,[],[f211750,f3263]) ).
fof(f211974,plain,
! [X0,X1] : rd(X0,X0) = mult(ld(mult(X0,ld(X1,X1)),X0),ld(X1,X1)),
inference(forward_demodulation,[],[f211774,f1]) ).
fof(f212017,plain,
! [X0,X1] : rd(rd(X1,X0),ld(ld(X1,X1),ld(ld(X1,X1),rd(X1,X0)))) = rd(mult(mult(ld(ld(mult(X0,rd(X0,X1)),X0),rd(X1,X0)),ld(X1,X1)),X1),X1),
inference(forward_demodulation,[],[f211825,f26144]) ).
fof(f212140,plain,
! [X0,X1] : ld(X0,X0) = mult(ld(mult(X0,ld(X1,X1)),X0),ld(X1,X1)),
inference(forward_demodulation,[],[f211974,f1406]) ).
fof(f212178,plain,
! [X0,X1] : mult(ld(ld(mult(X0,rd(X0,X1)),X0),rd(X1,X0)),ld(X1,X1)) = rd(rd(X1,X0),ld(ld(X1,X1),ld(ld(X1,X1),rd(X1,X0)))),
inference(forward_demodulation,[],[f212017,f4]) ).
fof(f212327,plain,
! [X0,X1] : mult(ld(ld(mult(X0,rd(X0,X1)),X0),rd(X1,X0)),ld(X1,X1)) = rd(rd(X1,X0),mult(ld(X1,X1),ld(ld(X1,X1),rd(X1,X0)))),
inference(forward_demodulation,[],[f212178,f1508]) ).
fof(f212463,plain,
! [X0,X1] : rd(rd(X1,X0),rd(X1,X0)) = mult(ld(ld(mult(X0,rd(X0,X1)),X0),rd(X1,X0)),ld(X1,X1)),
inference(forward_demodulation,[],[f212327,f1]) ).
fof(f212584,plain,
! [X0,X1] : ld(rd(X1,X0),rd(X1,X0)) = mult(ld(ld(mult(X0,rd(X0,X1)),X0),rd(X1,X0)),ld(X1,X1)),
inference(forward_demodulation,[],[f212463,f1406]) ).
fof(f212694,plain,
! [X0,X1] : mult(rd(X0,X1),rd(X1,X0)) = mult(ld(ld(mult(X0,rd(X0,X1)),X0),rd(X1,X0)),ld(X1,X1)),
inference(forward_demodulation,[],[f212584,f533]) ).
fof(f213048,plain,
! [X0,X1] : ld(mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0))),mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)))) = mult(ld(rd(X0,ld(ld(X1,X1),ld(ld(X1,X1),X0))),mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)))),ld(X1,X1)),
inference(superposition,[],[f212140,f3180]) ).
fof(f213106,plain,
! [X0,X1] : ld(ld(mult(X0,ld(X1,X1)),X0),rd(X1,ld(mult(X0,ld(X1,X1)),X0))) = rd(ld(ld(mult(X0,ld(X1,X1)),X0),X1),ld(X0,X0)),
inference(superposition,[],[f235,f212140]) ).
fof(f213111,plain,
! [X0,X1] : ld(mult(X0,ld(X1,X1)),X0) = rd(ld(X0,X0),ld(X1,X1)),
inference(superposition,[],[f4,f212140]) ).
fof(f213114,plain,
! [X2,X0,X1] : mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),ld(mult(X0,ld(X1,X1)),X0)) = rd(mult(ld(mult(X0,ld(X1,X1)),X0),mult(X2,ld(X0,X0))),ld(X1,X1)),
inference(superposition,[],[f14,f212140]) ).
fof(f213133,plain,
! [X2,X0,X1] : ld(ld(mult(X0,ld(X1,X1)),X0),X2) = mult(rd(ld(X1,X1),ld(X0,X0)),X2),
inference(superposition,[],[f317,f212140]) ).
fof(f213137,plain,
! [X2,X3,X0,X1] : mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),ld(ld(mult(X0,ld(X1,X1)),X0),X3)) = mult(ld(mult(X0,ld(X1,X1)),X0),mult(mult(X2,rd(ld(X1,X1),ld(X0,X0))),X3)),
inference(superposition,[],[f989,f212140]) ).
fof(f213138,plain,
! [X2,X0,X1] : rd(rd(X2,ld(X1,X1)),ld(mult(X0,ld(X1,X1)),X0)) = mult(ld(mult(X0,ld(X1,X1)),X0),rd(ld(ld(mult(X0,ld(X1,X1)),X0),X2),ld(X0,X0))),
inference(superposition,[],[f1091,f212140]) ).
fof(f213140,plain,
! [X2,X0,X1] : mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),ld(mult(X0,ld(X1,X1)),X0)) = mult(ld(mult(X0,ld(X1,X1)),X0),rd(X2,rd(ld(X1,X1),ld(X0,X0)))),
inference(superposition,[],[f1315,f212140]) ).
fof(f213152,plain,
! [X2,X0,X1] : ld(ld(mult(X0,ld(X1,X1)),X0),rd(X2,ld(mult(X0,ld(X1,X1)),X0))) = mult(ld(ld(mult(X0,ld(X1,X1)),X0),X2),rd(ld(X1,X1),ld(X0,X0))),
inference(superposition,[],[f3790,f212140]) ).
fof(f213161,plain,
! [X0,X1] : ld(mult(X0,ld(X1,X1)),X0) = mult(mult(ld(mult(X0,ld(X1,X1)),X0),ld(mult(X0,ld(X1,X1)),X0)),rd(ld(X1,X1),ld(X0,X0))),
inference(superposition,[],[f4764,f212140]) ).
fof(f213169,plain,
! [X2,X0,X1] : ld(ld(mult(X0,ld(X2,X2)),X0),mult(mult(ld(mult(X0,ld(X2,X2)),X0),X1),ld(mult(X0,ld(X2,X2)),X0))) = mult(mult(X1,mult(ld(mult(X0,ld(X2,X2)),X0),ld(mult(X0,ld(X2,X2)),X0))),rd(ld(X2,X2),ld(X0,X0))),
inference(superposition,[],[f5824,f212140]) ).
fof(f213203,plain,
! [X2,X0,X1] : ld(ld(mult(X0,ld(X1,X1)),X0),rd(ld(X1,X1),ld(X0,X0))) = ld(mult(mult(X2,ld(mult(X0,ld(X1,X1)),X0)),ld(mult(X0,ld(X1,X1)),X0)),X2),
inference(superposition,[],[f28531,f212140]) ).
fof(f213215,plain,
! [X2,X0,X1] : mult(mult(ld(mult(X0,ld(X1,X1)),X0),ld(mult(X0,ld(X1,X1)),X0)),rd(X2,ld(mult(X0,ld(X1,X1)),X0))) = mult(mult(mult(ld(mult(X0,ld(X1,X1)),X0),ld(mult(X0,ld(X1,X1)),X0)),X2),rd(ld(X1,X1),ld(X0,X0))),
inference(superposition,[],[f65873,f212140]) ).
fof(f213225,plain,
! [X2,X0,X1] : mult(mult(ld(X1,X1),mult(ld(ld(X1,X1),X2),ld(mult(X0,ld(X1,X1)),X0))),ld(X1,X1)) = ld(ld(mult(X0,ld(X1,X1)),X0),rd(mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),mult(ld(X0,X0),ld(mult(X0,ld(X1,X1)),X0))),ld(mult(X0,ld(X1,X1)),X0))),
inference(superposition,[],[f207334,f212140]) ).
fof(f213230,plain,
! [X2,X0,X1] : ld(ld(mult(X0,ld(X1,X1)),X0),rd(mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),mult(ld(X0,X0),ld(mult(X0,ld(X1,X1)),X0))),ld(mult(X0,ld(X1,X1)),X0))) = rd(mult(ld(X1,X1),mult(mult(ld(ld(X1,X1),X2),ld(mult(X0,ld(X1,X1)),X0)),X1)),X1),
inference(forward_demodulation,[],[f213225,f1522]) ).
fof(f213242,plain,
! [X0,X1] : ld(ld(mult(X0,ld(X1,X1)),X0),rd(ld(X1,X1),ld(X0,X0))) = ld(mult(X0,ld(mult(X0,ld(X1,X1)),X0)),mult(X0,ld(X1,X1))),
inference(forward_demodulation,[],[f213203,f156586]) ).
fof(f213297,plain,
! [X2,X0,X1] : ld(ld(mult(X0,ld(X1,X1)),X0),X2) = mult(ld(mult(X1,ld(X0,X0)),X1),X2),
inference(backward_demodulation,[],[f213133,f213111]) ).
fof(f213298,plain,
! [X2,X3,X0,X1] : mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),ld(ld(mult(X0,ld(X1,X1)),X0),X3)) = mult(ld(mult(X0,ld(X1,X1)),X0),mult(mult(X2,ld(mult(X1,ld(X0,X0)),X1)),X3)),
inference(backward_demodulation,[],[f213137,f213111]) ).
fof(f213299,plain,
! [X2,X0,X1] : mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),ld(mult(X0,ld(X1,X1)),X0)) = mult(ld(mult(X0,ld(X1,X1)),X0),rd(X2,ld(mult(X1,ld(X0,X0)),X1))),
inference(backward_demodulation,[],[f213140,f213111]) ).
fof(f213300,plain,
! [X2,X0,X1] : ld(ld(mult(X0,ld(X1,X1)),X0),rd(X2,ld(mult(X0,ld(X1,X1)),X0))) = mult(ld(ld(mult(X0,ld(X1,X1)),X0),X2),ld(mult(X1,ld(X0,X0)),X1)),
inference(backward_demodulation,[],[f213152,f213111]) ).
fof(f213302,plain,
! [X0,X1] : ld(mult(X0,ld(X1,X1)),X0) = mult(mult(ld(mult(X0,ld(X1,X1)),X0),ld(mult(X0,ld(X1,X1)),X0)),ld(mult(X1,ld(X0,X0)),X1)),
inference(backward_demodulation,[],[f213161,f213111]) ).
fof(f213305,plain,
! [X2,X0,X1] : ld(ld(mult(X0,ld(X2,X2)),X0),mult(mult(ld(mult(X0,ld(X2,X2)),X0),X1),ld(mult(X0,ld(X2,X2)),X0))) = mult(mult(X1,mult(ld(mult(X0,ld(X2,X2)),X0),ld(mult(X0,ld(X2,X2)),X0))),ld(mult(X2,ld(X0,X0)),X2)),
inference(backward_demodulation,[],[f213169,f213111]) ).
fof(f213312,plain,
! [X2,X0,X1] : mult(mult(ld(mult(X0,ld(X1,X1)),X0),ld(mult(X0,ld(X1,X1)),X0)),rd(X2,ld(mult(X0,ld(X1,X1)),X0))) = mult(mult(mult(ld(mult(X0,ld(X1,X1)),X0),ld(mult(X0,ld(X1,X1)),X0)),X2),ld(mult(X1,ld(X0,X0)),X1)),
inference(backward_demodulation,[],[f213215,f213111]) ).
fof(f213360,plain,
! [X0,X1] : ld(mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0))),mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)))) = mult(mult(rd(ld(ld(X1,X1),ld(ld(X1,X1),X0)),X0),mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)))),ld(X1,X1)),
inference(forward_demodulation,[],[f213048,f533]) ).
fof(f213380,plain,
! [X2,X0,X1] : ld(ld(mult(X0,ld(X1,X1)),X0),rd(mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),mult(ld(X0,X0),ld(mult(X0,ld(X1,X1)),X0))),ld(mult(X0,ld(X1,X1)),X0))) = rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),X2),ld(mult(X0,ld(X1,X1)),X0)),X1)),X1),
inference(forward_demodulation,[],[f213230,f1508]) ).
fof(f213389,plain,
! [X0,X1] : ld(mult(X0,ld(mult(X0,ld(X1,X1)),X0)),mult(X0,ld(X1,X1))) = ld(ld(mult(X0,ld(X1,X1)),X0),ld(mult(X1,ld(X0,X0)),X1)),
inference(forward_demodulation,[],[f213242,f213111]) ).
fof(f213439,plain,
! [X0,X1] : rd(ld(ld(mult(X0,ld(X1,X1)),X0),X1),ld(X0,X0)) = mult(ld(ld(mult(X0,ld(X1,X1)),X0),X1),ld(mult(X1,ld(X0,X0)),X1)),
inference(backward_demodulation,[],[f213106,f213300]) ).
fof(f213444,plain,
! [X2,X0,X1] : rd(rd(X2,ld(X1,X1)),ld(mult(X0,ld(X1,X1)),X0)) = mult(ld(mult(X0,ld(X1,X1)),X0),rd(mult(ld(mult(X1,ld(X0,X0)),X1),X2),ld(X0,X0))),
inference(backward_demodulation,[],[f213138,f213297]) ).
fof(f213447,plain,
! [X2,X3,X0,X1] : mult(ld(mult(X0,ld(X1,X1)),X0),mult(mult(X2,ld(mult(X1,ld(X0,X0)),X1)),X3)) = mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),mult(ld(mult(X1,ld(X0,X0)),X1),X3)),
inference(backward_demodulation,[],[f213298,f213297]) ).
fof(f213456,plain,
! [X2,X0,X1] : mult(mult(X1,mult(ld(mult(X0,ld(X2,X2)),X0),ld(mult(X0,ld(X2,X2)),X0))),ld(mult(X2,ld(X0,X0)),X2)) = mult(ld(mult(X2,ld(X0,X0)),X2),mult(mult(ld(mult(X0,ld(X2,X2)),X0),X1),ld(mult(X0,ld(X2,X2)),X0))),
inference(backward_demodulation,[],[f213305,f213297]) ).
fof(f213494,plain,
! [X0,X1] : ld(mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0))),mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)))) = mult(ld(ld(X1,X1),mult(mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)))),ld(X1,X1)),
inference(forward_demodulation,[],[f213360,f211953]) ).
fof(f213512,plain,
! [X2,X0,X1] : rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),X2),ld(mult(X0,ld(X1,X1)),X0)),X1)),X1) = mult(ld(mult(X1,ld(X0,X0)),X1),rd(mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),mult(ld(X0,X0),ld(mult(X0,ld(X1,X1)),X0))),ld(mult(X0,ld(X1,X1)),X0))),
inference(forward_demodulation,[],[f213380,f213297]) ).
fof(f213518,plain,
! [X0,X1] : ld(mult(X0,ld(mult(X0,ld(X1,X1)),X0)),mult(X0,ld(X1,X1))) = mult(ld(mult(X1,ld(X0,X0)),X1),ld(mult(X1,ld(X0,X0)),X1)),
inference(forward_demodulation,[],[f213389,f213297]) ).
fof(f213555,plain,
! [X0,X1] : rd(mult(ld(mult(X1,ld(X0,X0)),X1),X1),ld(X0,X0)) = mult(mult(ld(mult(X1,ld(X0,X0)),X1),X1),ld(mult(X1,ld(X0,X0)),X1)),
inference(forward_demodulation,[],[f213439,f213297]) ).
fof(f213594,plain,
! [X0,X1] : ld(mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0))),mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)))) = mult(mult(ld(X1,X1),mult(mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)))),ld(X1,X1)),
inference(forward_demodulation,[],[f213494,f1508]) ).
fof(f213612,plain,
! [X2,X0,X1] : rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),X2),ld(mult(X0,ld(X1,X1)),X0)),X1)),X1) = mult(mult(ld(mult(X1,ld(X0,X0)),X1),mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),mult(ld(X0,X0),ld(mult(X0,ld(X1,X1)),X0)))),ld(mult(X1,ld(X0,X0)),X1)),
inference(forward_demodulation,[],[f213512,f213299]) ).
fof(f213621,plain,
! [X0,X1] : ld(mult(X0,ld(X1,X1)),X0) = mult(ld(mult(X1,ld(mult(X1,ld(X0,X0)),X1)),mult(X1,ld(X0,X0))),ld(mult(X1,ld(X0,X0)),X1)),
inference(backward_demodulation,[],[f213302,f213518]) ).
fof(f213625,plain,
! [X2,X0,X1] : mult(ld(mult(X1,ld(mult(X1,ld(X0,X0)),X1)),mult(X1,ld(X0,X0))),rd(X2,ld(mult(X0,ld(X1,X1)),X0))) = mult(mult(ld(mult(X1,ld(mult(X1,ld(X0,X0)),X1)),mult(X1,ld(X0,X0))),X2),ld(mult(X1,ld(X0,X0)),X1)),
inference(backward_demodulation,[],[f213312,f213518]) ).
fof(f213627,plain,
! [X2,X0,X1] : mult(ld(mult(X2,ld(X0,X0)),X2),mult(mult(ld(mult(X0,ld(X2,X2)),X0),X1),ld(mult(X0,ld(X2,X2)),X0))) = mult(mult(X1,ld(mult(X2,ld(mult(X2,ld(X0,X0)),X2)),mult(X2,ld(X0,X0)))),ld(mult(X2,ld(X0,X0)),X2)),
inference(backward_demodulation,[],[f213456,f213518]) ).
fof(f213675,plain,
! [X0,X1] : ld(mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0))),mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)))) = rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0))),X1)),X1),
inference(forward_demodulation,[],[f213594,f1522]) ).
fof(f213692,plain,
! [X2,X0,X1] : mult(ld(mult(X2,ld(X0,X0)),X2),mult(mult(ld(mult(X0,ld(X2,X2)),X0),X1),ld(mult(X0,ld(X2,X2)),X0))) = rd(X1,ld(mult(X2,ld(X0,X0)),X2)),
inference(forward_demodulation,[],[f213627,f125219]) ).
fof(f213694,plain,
! [X0,X1] : ld(mult(X0,ld(X1,X1)),X0) = ld(ld(mult(X1,ld(X0,X0)),X1),mult(mult(X1,ld(X0,X0)),ld(mult(X1,mult(X1,ld(X0,X0))),X1))),
inference(forward_demodulation,[],[f213621,f157781]) ).
fof(f213722,plain,
! [X0,X1] : ld(mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0))),mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)))) = rd(mult(ld(X1,X1),mult(mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)),X1)),X1),
inference(forward_demodulation,[],[f213675,f55498]) ).
fof(f213733,plain,
! [X0,X1] : ld(mult(X0,ld(X1,X1)),X0) = mult(ld(mult(X0,ld(X1,X1)),X0),mult(mult(X1,ld(X0,X0)),ld(mult(X1,mult(X1,ld(X0,X0))),X1))),
inference(forward_demodulation,[],[f213694,f213297]) ).
fof(f213754,plain,
! [X0,X1] : ld(mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0))),mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)))) = rd(mult(mult(ld(mult(X0,ld(X1,X1)),X0),ld(X1,X1)),X1),X1),
inference(forward_demodulation,[],[f213722,f26144]) ).
fof(f213777,plain,
! [X0,X1] : mult(ld(mult(X0,ld(X1,X1)),X0),ld(X1,X1)) = ld(mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0))),mult(ld(X1,X1),mult(ld(X1,X1),ld(mult(X0,ld(X1,X1)),X0)))),
inference(forward_demodulation,[],[f213754,f4]) ).
fof(f213789,plain,
! [X0,X1] : mult(ld(mult(X0,ld(X1,X1)),X0),ld(X1,X1)) = ld(ld(mult(X0,ld(X1,X1)),X0),ld(mult(X0,ld(X1,X1)),X0)),
inference(forward_demodulation,[],[f213777,f2227]) ).
fof(f213797,plain,
! [X0,X1] : mult(ld(mult(X0,ld(X1,X1)),X0),ld(X1,X1)) = mult(mult(X0,ld(X1,X1)),ld(mult(X0,mult(X0,ld(X1,X1))),X0)),
inference(forward_demodulation,[],[f213789,f3079]) ).
fof(f213803,plain,
! [X0,X1] : ld(X0,X0) = mult(mult(X0,ld(X1,X1)),ld(mult(X0,mult(X0,ld(X1,X1))),X0)),
inference(forward_demodulation,[],[f213797,f212140]) ).
fof(f213815,plain,
! [X0,X1] : ld(mult(X0,ld(X1,X1)),X0) = mult(ld(mult(X0,ld(X1,X1)),X0),ld(X1,X1)),
inference(backward_demodulation,[],[f213733,f213803]) ).
fof(f213817,plain,
! [X0,X1] : ld(X0,X0) = ld(mult(X0,ld(X1,X1)),X0),
inference(forward_demodulation,[],[f213815,f212140]) ).
fof(f213825,plain,
! [X0,X1] : ld(X0,X0) = mult(ld(X0,X0),ld(X1,X1)),
inference(backward_demodulation,[],[f212140,f213817]) ).
fof(f213831,plain,
! [X2,X0,X1] : mult(mult(ld(X0,X0),X2),ld(X0,X0)) = rd(mult(ld(X0,X0),mult(X2,ld(X0,X0))),ld(X1,X1)),
inference(backward_demodulation,[],[f213114,f213817]) ).
fof(f213844,plain,
! [X2,X0,X1] : mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),ld(mult(X0,ld(X1,X1)),X0)) = mult(ld(mult(X0,ld(X1,X1)),X0),rd(X2,ld(X1,X1))),
inference(backward_demodulation,[],[f213299,f213817]) ).
fof(f213851,plain,
! [X2,X0,X1] : rd(rd(X2,ld(X1,X1)),ld(mult(X0,ld(X1,X1)),X0)) = mult(ld(mult(X0,ld(X1,X1)),X0),rd(mult(ld(X1,X1),X2),ld(X0,X0))),
inference(backward_demodulation,[],[f213444,f213817]) ).
fof(f213853,plain,
! [X2,X3,X0,X1] : mult(ld(mult(X0,ld(X1,X1)),X0),mult(mult(X2,ld(X1,X1)),X3)) = mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),mult(ld(X1,X1),X3)),
inference(backward_demodulation,[],[f213447,f213817]) ).
fof(f213860,plain,
! [X0,X1] : rd(mult(ld(X1,X1),X1),ld(X0,X0)) = mult(mult(ld(X1,X1),X1),ld(X1,X1)),
inference(backward_demodulation,[],[f213555,f213817]) ).
fof(f213865,plain,
! [X2,X0,X1] : rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),X2),ld(mult(X0,ld(X1,X1)),X0)),X1)),X1) = mult(mult(ld(X1,X1),mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),mult(ld(X0,X0),ld(mult(X0,ld(X1,X1)),X0)))),ld(X1,X1)),
inference(backward_demodulation,[],[f213612,f213817]) ).
fof(f213868,plain,
! [X2,X0,X1] : mult(ld(mult(X1,ld(X1,X1)),mult(X1,ld(X0,X0))),rd(X2,ld(mult(X0,ld(X1,X1)),X0))) = mult(mult(ld(mult(X1,ld(X1,X1)),mult(X1,ld(X0,X0))),X2),ld(X1,X1)),
inference(backward_demodulation,[],[f213625,f213817]) ).
fof(f213873,plain,
! [X2,X0,X1] : rd(X1,ld(X2,X2)) = mult(ld(X2,X2),mult(mult(ld(mult(X0,ld(X2,X2)),X0),X1),ld(mult(X0,ld(X2,X2)),X0))),
inference(backward_demodulation,[],[f213692,f213817]) ).
fof(f213926,plain,
! [X2,X0,X1] : rd(X1,ld(X2,X2)) = mult(ld(X2,X2),mult(mult(ld(X0,X0),X1),ld(X0,X0))),
inference(forward_demodulation,[],[f213873,f213817]) ).
fof(f213931,plain,
! [X2,X0,X1] : mult(ld(X1,mult(X1,ld(X0,X0))),rd(X2,ld(mult(X0,ld(X1,X1)),X0))) = mult(mult(ld(X1,mult(X1,ld(X0,X0))),X2),ld(X1,X1)),
inference(forward_demodulation,[],[f213868,f1]) ).
fof(f213934,plain,
! [X2,X0,X1] : rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),X2),ld(mult(X0,ld(X1,X1)),X0)),X1)),X1) = rd(mult(ld(X1,X1),mult(mult(mult(ld(mult(X0,ld(X1,X1)),X0),X2),mult(ld(X0,X0),ld(mult(X0,ld(X1,X1)),X0))),X1)),X1),
inference(forward_demodulation,[],[f213865,f1522]) ).
fof(f213939,plain,
! [X0,X1] : mult(X1,mult(ld(X1,ld(X1,X1)),X1)) = rd(mult(ld(X1,X1),X1),ld(X0,X0)),
inference(forward_demodulation,[],[f213860,f112]) ).
fof(f213946,plain,
! [X2,X3,X0,X1] : mult(ld(X0,X0),mult(mult(X2,ld(X1,X1)),X3)) = mult(mult(ld(X0,X0),X2),mult(ld(X1,X1),X3)),
inference(forward_demodulation,[],[f213853,f213817]) ).
fof(f213948,plain,
! [X2,X0,X1] : rd(rd(X2,ld(X1,X1)),ld(X0,X0)) = mult(ld(X0,X0),rd(mult(ld(X1,X1),X2),ld(X0,X0))),
inference(forward_demodulation,[],[f213851,f213817]) ).
fof(f213955,plain,
! [X2,X0,X1] : mult(mult(ld(X0,X0),X2),ld(X0,X0)) = mult(ld(X0,X0),rd(X2,ld(X1,X1))),
inference(forward_demodulation,[],[f213844,f213817]) ).
fof(f213963,plain,
! [X2,X0,X1] : rd(mult(ld(X0,X0),mult(X2,X0)),X0) = rd(mult(ld(X0,X0),mult(X2,ld(X0,X0))),ld(X1,X1)),
inference(forward_demodulation,[],[f213831,f1522]) ).
fof(f213990,plain,
! [X2,X0,X1] : rd(X1,ld(X2,X2)) = mult(ld(X2,X2),rd(mult(ld(X0,X0),mult(X1,X0)),X0)),
inference(forward_demodulation,[],[f213926,f1522]) ).
fof(f213995,plain,
! [X2,X0,X1] : mult(ld(X0,X0),rd(X2,ld(mult(X0,ld(X1,X1)),X0))) = mult(mult(ld(X0,X0),X2),ld(X1,X1)),
inference(forward_demodulation,[],[f213931,f2]) ).
fof(f213998,plain,
! [X2,X0,X1] : rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),X2),ld(X0,X0)),X1)),X1) = rd(mult(ld(X1,X1),mult(mult(mult(ld(X0,X0),X2),mult(ld(X0,X0),ld(X0,X0))),X1)),X1),
inference(forward_demodulation,[],[f213934,f213817]) ).
fof(f214002,plain,
! [X0,X1] : rd(X1,ld(X0,X0)) = mult(X1,mult(ld(X1,ld(X1,X1)),X1)),
inference(forward_demodulation,[],[f213939,f1509]) ).
fof(f214010,plain,
! [X2,X0,X1] : rd(rd(X2,ld(X1,X1)),ld(X0,X0)) = rd(mult(ld(X0,X0),mult(mult(ld(X1,X1),X2),X0)),X0),
inference(forward_demodulation,[],[f213948,f1559]) ).
fof(f214017,plain,
! [X2,X0,X1] : rd(mult(ld(X0,X0),mult(X2,X0)),X0) = mult(ld(X0,X0),rd(X2,ld(X1,X1))),
inference(forward_demodulation,[],[f213955,f1522]) ).
fof(f214082,plain,
! [X2,X0,X1] : mult(ld(X0,X0),rd(X2,ld(X0,X0))) = mult(mult(ld(X0,X0),X2),ld(X1,X1)),
inference(forward_demodulation,[],[f213995,f213817]) ).
fof(f214085,plain,
! [X2,X0,X1] : rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),X2),ld(X0,X0)),X1)),X1) = rd(mult(ld(X1,X1),mult(mult(ld(X0,X0),mult(mult(X2,ld(X0,X0)),ld(X0,X0))),X1)),X1),
inference(forward_demodulation,[],[f213998,f213946]) ).
fof(f214087,plain,
! [X0,X1] : rd(X1,ld(X0,X0)) = mult(X1,mult(ld(mult(X1,X1),X1),X1)),
inference(forward_demodulation,[],[f214002,f4494]) ).
fof(f214126,plain,
! [X2,X0,X1] : rd(mult(ld(X0,X0),mult(X2,X0)),X0) = mult(mult(ld(X0,X0),X2),ld(X1,X1)),
inference(forward_demodulation,[],[f214082,f1559]) ).
fof(f214127,plain,
! [X2,X0,X1] : rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),X2),ld(X0,X0)),X1)),X1) = rd(rd(mult(mult(X2,ld(X0,X0)),ld(X0,X0)),ld(X0,X0)),ld(X1,X1)),
inference(forward_demodulation,[],[f214085,f214010]) ).
fof(f214129,plain,
! [X0,X1] : rd(X1,ld(X0,X0)) = ld(mult(X1,X1),mult(mult(X1,X1),X1)),
inference(forward_demodulation,[],[f214087,f119617]) ).
fof(f214154,plain,
! [X2,X0,X1] : rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),X2),ld(X0,X0)),X1)),X1) = rd(mult(X2,ld(X0,X0)),ld(X1,X1)),
inference(forward_demodulation,[],[f214127,f4]) ).
fof(f214156,plain,
! [X0,X1] : rd(X1,ld(X0,X0)) = X1,
inference(forward_demodulation,[],[f214129,f2]) ).
fof(f214424,plain,
! [X0,X1] : mult(ld(X0,X0),X0) = mult(ld(X1,X1),mult(X0,ld(X1,X1))),
inference(backward_demodulation,[],[f211326,f214156]) ).
fof(f214440,plain,
! [X2,X0,X1] : mult(ld(X2,X2),rd(mult(ld(X0,X0),mult(X1,X0)),X0)) = X1,
inference(backward_demodulation,[],[f213990,f214156]) ).
fof(f214442,plain,
! [X2,X0] : mult(ld(X0,X0),X2) = rd(mult(ld(X0,X0),mult(X2,X0)),X0),
inference(backward_demodulation,[],[f214017,f214156]) ).
fof(f214600,plain,
! [X2,X0,X1] : mult(X2,ld(X0,X0)) = rd(mult(ld(X1,X1),mult(mult(mult(ld(X1,X1),X2),ld(X0,X0)),X1)),X1),
inference(backward_demodulation,[],[f214154,f214156]) ).
fof(f214624,plain,
! [X2,X0] : rd(mult(ld(X0,X0),mult(X2,X0)),X0) = mult(ld(X0,X0),mult(X2,ld(X0,X0))),
inference(backward_demodulation,[],[f213963,f214156]) ).
fof(f214665,plain,
! [X0,X1] : ld(X0,X0) = ld(ld(mult(X1,rd(X1,X0)),X1),rd(X0,X1)),
inference(backward_demodulation,[],[f19408,f214156]) ).
fof(f214761,plain,
! [X0,X1] : mult(rd(X0,X1),rd(X1,X0)) = mult(ld(X1,X1),ld(X1,X1)),
inference(backward_demodulation,[],[f212694,f214665]) ).
fof(f216002,plain,
! [X2,X0,X1] : mult(ld(X0,X0),X2) = mult(mult(ld(X0,X0),X2),ld(X1,X1)),
inference(backward_demodulation,[],[f214126,f214442]) ).
fof(f216003,plain,
! [X2,X0] : mult(ld(X0,X0),X2) = mult(ld(X0,X0),mult(X2,ld(X0,X0))),
inference(backward_demodulation,[],[f214624,f214442]) ).
fof(f216025,plain,
! [X2,X0,X1] : mult(X2,ld(X0,X0)) = mult(ld(X1,X1),mult(mult(ld(X1,X1),X2),ld(X0,X0))),
inference(backward_demodulation,[],[f214600,f214442]) ).
fof(f216038,plain,
! [X2,X0,X1] : mult(ld(X2,X2),mult(ld(X0,X0),X1)) = X1,
inference(forward_demodulation,[],[f214440,f214442]) ).
fof(f216051,plain,
! [X0,X1] : mult(ld(X1,X1),mult(X0,ld(X1,X1))) = X0,
inference(forward_demodulation,[],[f214424,f1509]) ).
fof(f216240,plain,
! [X0,X1] : mult(rd(X0,X1),rd(X1,X0)) = ld(X1,X1),
inference(forward_demodulation,[],[f214761,f213825]) ).
fof(f217643,plain,
! [X2,X0,X1] : mult(X2,ld(X0,X0)) = mult(ld(X1,X1),mult(ld(X1,X1),X2)),
inference(backward_demodulation,[],[f216025,f216002]) ).
fof(f217677,plain,
! [X0,X1] : mult(ld(X1,X1),X0) = X0,
inference(forward_demodulation,[],[f216051,f216003]) ).
fof(f217969,plain,
! [X0,X1] : tuple(x1(mult(rd(X1,X0),rd(X0,X1))),x1_2(mult(rd(X1,X0),rd(X0,X1)))) != tuple(mult(ld(X1,X1),x1(mult(rd(X1,X0),rd(X0,X1)))),mult(x1_2(mult(rd(X1,X0),rd(X0,X1))),mult(rd(X1,X0),rd(X0,X1)))),
inference(backward_demodulation,[],[f125206,f216240]) ).
fof(f218898,plain,
! [X2,X0] : mult(X2,ld(X0,X0)) = X2,
inference(forward_demodulation,[],[f217643,f216038]) ).
fof(f219810,plain,
! [X0,X1] : tuple(x1(ld(X0,X0)),x1_2(ld(X0,X0))) != tuple(mult(ld(X1,X1),x1(ld(X0,X0))),mult(x1_2(ld(X0,X0)),ld(X0,X0))),
inference(forward_demodulation,[],[f217969,f216240]) ).
fof(f228917,plain,
! [X0,X1] : tuple(x1(ld(X0,X0)),x1_2(ld(X0,X0))) != tuple(mult(ld(X1,X1),x1(ld(X0,X0))),x1_2(ld(X0,X0))),
inference(forward_demodulation,[],[f219810,f218898]) ).
fof(f235168,plain,
! [X0] : tuple(x1(ld(X0,X0)),x1_2(ld(X0,X0))) != tuple(x1(ld(X0,X0)),x1_2(ld(X0,X0))),
inference(forward_demodulation,[],[f228917,f217677]) ).
fof(f235169,plain,
$false,
inference(trivial_inequality_removal,[],[f235168]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP654-10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 10:36:45 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 50.22/12.32 % (3363791)Detected a unit-equality problem, will run specialized UEQ schedule.
% 50.22/12.32 % (3363796)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=1851166110:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 50.22/12.32 % (3363798)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3855558435:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 50.22/12.32 % (3363799)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3830898579:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 50.22/12.32 % (3363801)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1705649146:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 50.22/12.32 % (3363800)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2532421231:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 50.22/12.32 % (3363802)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2966914367:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 50.22/12.32 % (3363797)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=1695949326:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 50.22/12.32 % (3363799)Instruction limit reached!
% 50.22/12.32 % (3363799)------------------------------
% 50.22/12.32 % (3363799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363799)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363799)Termination reason: Instruction limit
% 50.22/12.32 % (3363799)Termination phase: Saturation
% 50.22/12.32 % (3363799)Time elapsed: 0.068 s
% 50.22/12.32 % (3363799)Peak memory usage: 89 MB
% 50.22/12.32 % (3363799)Instructions burned: 136 (million)
% 50.22/12.32 % (3363800)Instruction limit reached!
% 50.22/12.32 % (3363800)------------------------------
% 50.22/12.32 % (3363800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363800)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363800)Termination reason: Instruction limit
% 50.22/12.32 % (3363800)Termination phase: Saturation
% 50.22/12.32 % (3363800)Time elapsed: 0.107 s
% 50.22/12.32 % (3363800)Peak memory usage: 89 MB
% 50.22/12.32 % (3363800)Instructions burned: 183 (million)
% 50.22/12.32 % (3363801)Instruction limit reached!
% 50.22/12.32 % (3363801)------------------------------
% 50.22/12.32 % (3363801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363801)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363801)Termination reason: Instruction limit
% 50.22/12.32 % (3363801)Termination phase: Saturation
% 50.22/12.32 % (3363801)Time elapsed: 0.135 s
% 50.22/12.32 % (3363801)Peak memory usage: 90 MB
% 50.22/12.32 % (3363801)Instructions burned: 258 (million)
% 50.22/12.32 % (3363810)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2386857039:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 50.22/12.32 % (3363811)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4248143823:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 50.22/12.32 % (3363812)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=566942185:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 50.22/12.32 % (3363812)Instruction limit reached!
% 50.22/12.32 % (3363812)------------------------------
% 50.22/12.32 % (3363812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363812)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363812)Termination reason: Instruction limit
% 50.22/12.32 % (3363812)Termination phase: Saturation
% 50.22/12.32 % (3363812)Time elapsed: 0.112 s
% 50.22/12.32 % (3363812)Peak memory usage: 90 MB
% 50.22/12.32 % (3363812)Instructions burned: 215 (million)
% 50.22/12.32 % (3363816)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=1871099592:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 50.22/12.32 % (3363802)Instruction limit reached!
% 50.22/12.32 % (3363802)------------------------------
% 50.22/12.32 % (3363802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363802)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363802)Termination reason: Instruction limit
% 50.22/12.32 % (3363802)Termination phase: Saturation
% 50.22/12.32 % (3363802)Time elapsed: 0.615 s
% 50.22/12.32 % (3363802)Peak memory usage: 102 MB
% 50.22/12.32 % (3363802)Instructions burned: 1189 (million)
% 50.22/12.32 % (3363816)Instruction limit reached!
% 50.22/12.32 % (3363816)------------------------------
% 50.22/12.32 % (3363816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363816)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363816)Termination reason: Instruction limit
% 50.22/12.32 % (3363816)Termination phase: Saturation
% 50.22/12.32 % (3363816)Time elapsed: 0.197 s
% 50.22/12.32 % (3363816)Peak memory usage: 92 MB
% 50.22/12.32 % (3363816)Instructions burned: 318 (million)
% 50.22/12.32 % (3363818)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=575562765:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 50.22/12.32 % (3363819)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1776526740:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 50.22/12.32 % (3363810)Instruction limit reached!
% 50.22/12.32 % (3363810)------------------------------
% 50.22/12.32 % (3363810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363810)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363810)Termination reason: Instruction limit
% 50.22/12.32 % (3363810)Termination phase: Saturation
% 50.22/12.32 % (3363810)Time elapsed: 1.308 s
% 50.22/12.32 % (3363810)Peak memory usage: 141 MB
% 50.22/12.32 % (3363810)Instructions burned: 2051 (million)
% 50.22/12.32 % (3363822)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1360409373:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2982 on theBenchmark for (2982ds/14534Mi)
% 50.22/12.32 % (3363819)Instruction limit reached!
% 50.22/12.32 % (3363819)------------------------------
% 50.22/12.32 % (3363819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363819)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363819)Termination reason: Instruction limit
% 50.22/12.32 % (3363819)Termination phase: Saturation
% 50.22/12.32 % (3363819)Time elapsed: 1.762 s
% 50.22/12.32 % (3363819)Peak memory usage: 138 MB
% 50.22/12.32 % (3363819)Instructions burned: 2836 (million)
% 50.22/12.32 % (3363824)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=2132155266:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/11832Mi)
% 50.22/12.32 % (3363811)Instruction limit reached!
% 50.22/12.32 % (3363811)------------------------------
% 50.22/12.32 % (3363811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363811)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363811)Termination reason: Instruction limit
% 50.22/12.32 % (3363811)Termination phase: Saturation
% 50.22/12.32 % (3363811)Time elapsed: 3.026 s
% 50.22/12.32 % (3363811)Peak memory usage: 164 MB
% 50.22/12.32 % (3363811)Instructions burned: 4949 (million)
% 50.22/12.32 % (3363826)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=3397683991:i=2279:fgj=on:bd=all_2965 on theBenchmark for (2965ds/2279Mi)
% 50.22/12.32 % (3363826)Instruction limit reached!
% 50.22/12.32 % (3363826)------------------------------
% 50.22/12.32 % (3363826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363826)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363826)Termination reason: Instruction limit
% 50.22/12.32 % (3363826)Termination phase: Saturation
% 50.22/12.32 % (3363826)Time elapsed: 1.345 s
% 50.22/12.32 % (3363826)Peak memory usage: 137 MB
% 50.22/12.32 % (3363826)Instructions burned: 2279 (million)
% 50.22/12.32 % (3363828)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:drc=off:fde=none:sp=reverse_arity:urr=ec_only:gs=on:s2agt=16:random_seed=3983645395:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2950 on theBenchmark for (2950ds/6225Mi)
% 50.22/12.32 % (3363828)Instruction limit reached!
% 50.22/12.32 % (3363828)------------------------------
% 50.22/12.32 % (3363828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363828)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363828)Termination reason: Instruction limit
% 50.22/12.32 % (3363828)Termination phase: Saturation
% 50.22/12.32 % (3363828)Time elapsed: 2.858 s
% 50.22/12.32 % (3363828)Peak memory usage: 193 MB
% 50.22/12.32 % (3363828)Instructions burned: 6226 (million)
% 50.22/12.32 % (3363830)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=1142715546:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2919 on theBenchmark for (2919ds/21755Mi)
% 50.22/12.32 % (3363818)Instruction limit reached!
% 50.22/12.32 % (3363818)------------------------------
% 50.22/12.32 % (3363818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363818)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363818)Termination reason: Instruction limit
% 50.22/12.32 % (3363818)Termination phase: Saturation
% 50.22/12.32 % (3363818)Time elapsed: 7.458 s
% 50.22/12.32 % (3363818)Peak memory usage: 229 MB
% 50.22/12.32 % (3363818)Instructions burned: 12125 (million)
% 50.22/12.32 % (3363832)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=233592912:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2915 on theBenchmark for (2915ds/16427Mi)
% 50.22/12.32 % (3363796)First to succeed.
% 50.22/12.32 % (3363796)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3363791"
% 50.22/12.32 % (3363824)Instruction limit reached!
% 50.22/12.32 % (3363824)------------------------------
% 50.22/12.32 % (3363824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363824)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363824)Termination reason: Instruction limit
% 50.22/12.32 % (3363824)Termination phase: Saturation
% 50.22/12.32 % (3363824)Time elapsed: 7.725 s
% 50.22/12.32 % (3363824)Peak memory usage: 221 MB
% 50.22/12.32 % (3363824)Instructions burned: 11832 (million)
% 50.22/12.32 % (3363834)lrs+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=1564816086:i=9356:fgj=on:bd=preordered:av=off_2892 on theBenchmark for (2892ds/9356Mi)
% 50.22/12.32 % (3363822)Instruction limit reached!
% 50.22/12.32 % (3363822)------------------------------
% 50.22/12.32 % (3363822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.22/12.32 % (3363822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.22/12.32 % (3363822)CaDiCaL version: 2.1.3
% 50.22/12.32 % (3363822)Termination reason: Instruction limit
% 50.22/12.32 % (3363822)Termination phase: Saturation
% 50.22/12.32 % (3363822)Time elapsed: 9.075 s
% 50.22/12.32 % (3363822)Peak memory usage: 246 MB
% 50.22/12.32 % (3363822)Instructions burned: 14535 (million)
% 50.22/12.32 % (3363836)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=2408716532:i=2070:kws=inv_precedence:slsql=off:bd=all_2890 on theBenchmark for (2890ds/2070Mi)
% 50.22/12.32 % (3363796)Refutation found. Thanks to Tanya!
% 50.22/12.32 % SZS status Unsatisfiable for theBenchmark
% 50.22/12.32 % SZS output start Proof for theBenchmark
% See solution above
% 81.07/12.52 % (3363796)------------------------------
% 81.07/12.52 % (3363796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.07/12.52 % (3363796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.07/12.52 % (3363796)CaDiCaL version: 2.1.3
% 81.07/12.52 % (3363796)Termination reason: Refutation
% 81.07/12.52 % (3363796)Time elapsed: 10.432 s
% 81.07/12.52 % (3363796)Peak memory usage: 326 MB
% 81.07/12.52 % (3363796)Instructions burned: 28777 (million)
% 81.07/12.52 % (3363796)------------------------------
% 81.07/12.52 % (3363796)------------------------------
% 81.07/12.52 % (3363791)Success in time 11.462 s
% 81.07/12.52 % Vampire exiting
%------------------------------------------------------------------------------