%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP655-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 : n014.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:22 AM UTC 2026
% Result : Unsatisfiable 95.67s 30.46s
% Output : Refutation 208.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 83
% Number of leaves : 6
% Syntax : Number of formulae : 345 ( 345 unt; 0 def)
% Number of atoms : 345 ( 344 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 16 ( 16 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 14 ( 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 : 679 ( 679 !; 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(X2,X1))) = mult(mult(mult(X0,X1),X2),X1),
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(f10,plain,
! [X2,X0,X1] : mult(X0,X2) = mult(X1,mult(X2,mult(ld(mult(X1,X2),X0),X2))),
inference(superposition,[],[f5,f1]) ).
fof(f12,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f13,plain,
! [X2,X0,X1] : mult(mult(X0,X1),X2) = rd(mult(X0,mult(X1,mult(X2,X1))),X1),
inference(superposition,[],[f4,f5]) ).
fof(f15,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f2,f3]) ).
fof(f23,plain,
! [X2,X0,X1] : mult(X1,X2) = mult(rd(X0,X2),mult(X2,mult(ld(X0,X1),X2))),
inference(superposition,[],[f10,f3]) ).
fof(f38,plain,
! [X2,X0,X1] : mult(X0,X2) = rd(mult(rd(X0,X1),mult(X1,mult(X2,X1))),X1),
inference(superposition,[],[f13,f3]) ).
fof(f58,plain,
! [X2,X0,X1] : mult(X1,rd(X0,X2)) = rd(mult(rd(X1,X2),mult(X2,X0)),X2),
inference(superposition,[],[f38,f3]) ).
fof(f71,plain,
! [X2,X0,X1] : mult(X1,rd(ld(X2,X0),X2)) = rd(mult(rd(X1,X2),X0),X2),
inference(superposition,[],[f58,f1]) ).
fof(f91,plain,
! [X2,X0,X1] : rd(X0,X2) = mult(X1,rd(ld(X2,ld(rd(X1,X2),X0)),X2)),
inference(superposition,[],[f71,f1]) ).
fof(f94,plain,
! [X0,X1] : rd(X0,X1) = mult(X0,rd(ld(X1,X1),X1)),
inference(superposition,[],[f4,f71]) ).
fof(f108,plain,
! [X2,X0,X1] : mult(rd(X0,X1),X2) = rd(mult(X0,mult(rd(ld(X1,X1),X1),mult(X2,rd(ld(X1,X1),X1)))),rd(ld(X1,X1),X1)),
inference(superposition,[],[f13,f94]) ).
fof(f109,plain,
! [X0,X1] : rd(rd(X0,X1),rd(ld(X1,X1),X1)) = X0,
inference(superposition,[],[f4,f94]) ).
fof(f111,plain,
! [X0,X1] : rd(ld(X1,X1),X1) = ld(X0,rd(X0,X1)),
inference(superposition,[],[f2,f94]) ).
fof(f114,plain,
! [X2,X0,X1] : mult(X0,mult(rd(ld(X1,X1),X1),mult(X2,rd(ld(X1,X1),X1)))) = rd(mult(mult(X0,rd(ld(X1,X1),X1)),X2),X1),
inference(superposition,[],[f5,f94]) ).
fof(f115,plain,
! [X0,X1] : rd(rd(X0,rd(ld(X1,X1),X1)),X1) = X0,
inference(superposition,[],[f3,f94]) ).
fof(f118,plain,
! [X2,X0,X1] : rd(mult(rd(X0,X1),X2),X1) = mult(X0,mult(rd(ld(X1,X1),X1),mult(X2,rd(ld(X1,X1),X1)))),
inference(forward_demodulation,[],[f114,f94]) ).
fof(f120,plain,
! [X2,X0,X1] : mult(rd(X0,X1),X2) = rd(mult(X0,mult(rd(ld(X1,X1),X1),rd(X2,X1))),rd(ld(X1,X1),X1)),
inference(forward_demodulation,[],[f108,f94]) ).
fof(f123,plain,
! [X2,X0,X1] : rd(mult(rd(X0,X1),X2),X1) = mult(X0,mult(rd(ld(X1,X1),X1),rd(X2,X1))),
inference(forward_demodulation,[],[f118,f94]) ).
fof(f126,plain,
! [X2,X0,X1] : mult(X0,rd(ld(X1,X2),X1)) = mult(X0,mult(rd(ld(X1,X1),X1),rd(X2,X1))),
inference(forward_demodulation,[],[f123,f71]) ).
fof(f129,plain,
! [X2,X0,X1] : mult(rd(X0,X1),X2) = rd(mult(X0,rd(ld(X1,X2),X1)),rd(ld(X1,X1),X1)),
inference(backward_demodulation,[],[f120,f126]) ).
fof(f134,plain,
! [X2,X0,X1] : mult(X1,X2) = rd(mult(X0,rd(ld(X2,mult(X2,mult(ld(X0,X1),X2))),X2)),rd(ld(X2,X2),X2)),
inference(backward_demodulation,[],[f23,f129]) ).
fof(f153,plain,
! [X2,X0,X1] : mult(X1,X2) = rd(mult(X0,rd(mult(ld(X0,X1),X2),X2)),rd(ld(X2,X2),X2)),
inference(forward_demodulation,[],[f134,f2]) ).
fof(f158,plain,
! [X2,X0,X1] : mult(X1,X2) = rd(mult(X0,ld(X0,X1)),rd(ld(X2,X2),X2)),
inference(forward_demodulation,[],[f153,f4]) ).
fof(f162,plain,
! [X2,X1] : mult(X1,X2) = rd(X1,rd(ld(X2,X2),X2)),
inference(forward_demodulation,[],[f158,f1]) ).
fof(f185,plain,
! [X0,X1] : ld(X0,rd(X0,rd(ld(X1,X1),X1))) = X1,
inference(backward_demodulation,[],[f2,f162]) ).
fof(f200,plain,
! [X2,X0,X1] : rd(X0,X2) = rd(X1,rd(ld(rd(ld(X2,ld(rd(X1,X2),X0)),X2),rd(ld(X2,ld(rd(X1,X2),X0)),X2)),rd(ld(X2,ld(rd(X1,X2),X0)),X2))),
inference(backward_demodulation,[],[f91,f162]) ).
fof(f202,plain,
! [X0] : tuple(x1(X0),x1_2(X0)) != tuple(rd(X0,rd(ld(x1(X0),x1(X0)),x1(X0))),mult(x1_2(X0),X0)),
inference(backward_demodulation,[],[f6,f162]) ).
fof(f226,plain,
! [X0] : tuple(x1(X0),x1_2(X0)) != tuple(rd(X0,rd(ld(x1(X0),x1(X0)),x1(X0))),rd(x1_2(X0),rd(ld(X0,X0),X0))),
inference(forward_demodulation,[],[f202,f162]) ).
fof(f402,plain,
! [X2,X0,X1] : ld(X0,rd(X0,X1)) = ld(X2,rd(X2,X1)),
inference(superposition,[],[f111,f111]) ).
fof(f403,plain,
! [X0,X1] : ld(X0,rd(X0,X1)) = ld(ld(X1,X1),ld(X0,rd(X0,X1))),
inference(superposition,[],[f111,f111]) ).
fof(f406,plain,
! [X0,X1] : tuple(x1(X1),x1_2(X1)) != tuple(rd(X1,rd(ld(x1(X1),x1(X1)),x1(X1))),rd(x1_2(X1),ld(X0,rd(X0,X1)))),
inference(superposition,[],[f226,f111]) ).
fof(f407,plain,
! [X0,X1] : ld(ld(X0,rd(X0,X1)),ld(X1,X1)) = X1,
inference(superposition,[],[f15,f111]) ).
fof(f419,plain,
! [X2,X0,X1] : ld(X2,X0) = ld(X1,rd(X1,ld(X0,X2))),
inference(superposition,[],[f402,f12]) ).
fof(f430,plain,
! [X2,X0,X1] : rd(rd(X2,X1),ld(X0,rd(X0,X1))) = X2,
inference(superposition,[],[f12,f402]) ).
fof(f447,plain,
! [X2,X0,X1] : rd(rd(X2,ld(X1,X0)),ld(X0,X1)) = X2,
inference(superposition,[],[f12,f419]) ).
fof(f463,plain,
! [X2,X3,X0,X1] : rd(rd(X1,ld(X2,rd(X2,X3))),ld(rd(X0,X3),X0)) = X1,
inference(superposition,[],[f430,f430]) ).
fof(f478,plain,
! [X2,X3,X1] : rd(rd(X1,ld(X2,rd(X2,X3))),X3) = X1,
inference(forward_demodulation,[],[f463,f15]) ).
fof(f532,plain,
! [X2,X0,X1] : ld(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2))) = rd(ld(X0,rd(X0,ld(X1,rd(X1,X2)))),X2),
inference(superposition,[],[f478,f111]) ).
fof(f552,plain,
! [X2,X1] : ld(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2))) = rd(ld(rd(X1,X2),X1),X2),
inference(forward_demodulation,[],[f532,f419]) ).
fof(f557,plain,
! [X2,X1] : ld(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2))) = rd(X2,X2),
inference(forward_demodulation,[],[f552,f15]) ).
fof(f562,plain,
! [X2,X0,X1] : rd(X0,rd(ld(X2,X2),X2)) = rd(X0,ld(X1,rd(X1,X2))),
inference(superposition,[],[f109,f478]) ).
fof(f581,plain,
! [X0,X1] : ld(rd(ld(X1,X1),X1),rd(ld(X1,X1),X1)) = rd(ld(X0,rd(X0,rd(ld(X1,X1),X1))),X1),
inference(superposition,[],[f115,f111]) ).
fof(f602,plain,
! [X1] : ld(rd(ld(X1,X1),X1),rd(ld(X1,X1),X1)) = rd(X1,X1),
inference(forward_demodulation,[],[f581,f185]) ).
fof(f609,plain,
! [X2,X0,X1] : ld(X2,rd(X2,X1)) = ld(ld(rd(X0,X1),X0),ld(ld(X2,rd(X2,X1)),ld(X2,rd(X2,X1)))),
inference(superposition,[],[f407,f430]) ).
fof(f616,plain,
! [X0,X1] : ld(X1,X0) = ld(ld(X0,X1),ld(ld(X1,X0),ld(X1,X0))),
inference(superposition,[],[f407,f419]) ).
fof(f627,plain,
! [X2,X1] : ld(X2,rd(X2,X1)) = ld(X1,ld(ld(X2,rd(X2,X1)),ld(X2,rd(X2,X1)))),
inference(forward_demodulation,[],[f609,f15]) ).
fof(f736,plain,
! [X2,X0] : rd(X0,X0) = ld(X2,rd(X2,rd(X0,X0))),
inference(superposition,[],[f419,f557]) ).
fof(f750,plain,
! [X2,X0,X1] : rd(ld(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))),ld(X2,rd(X2,X1))) = X1,
inference(superposition,[],[f430,f557]) ).
fof(f803,plain,
! [X0] : rd(X0,X0) = ld(rd(X0,X0),ld(rd(X0,X0),rd(X0,X0))),
inference(superposition,[],[f407,f736]) ).
fof(f2980,plain,
! [X0] : rd(ld(rd(X0,X0),rd(X0,X0)),X0) = rd(X0,rd(ld(rd(ld(X0,rd(X0,X0)),X0),rd(ld(X0,rd(X0,X0)),X0)),rd(ld(X0,rd(X0,X0)),X0))),
inference(superposition,[],[f200,f803]) ).
fof(f2999,plain,
! [X2,X0,X1] : rd(ld(X1,ld(rd(X2,X1),X0)),X1) = ld(X2,rd(X0,X1)),
inference(superposition,[],[f185,f200]) ).
fof(f3075,plain,
! [X2,X0,X1] : rd(ld(X1,ld(X0,X2)),X1) = ld(rd(X0,rd(ld(X1,X1),X1)),rd(X2,X1)),
inference(superposition,[],[f2999,f115]) ).
fof(f3078,plain,
! [X2,X3,X0,X1] : ld(rd(X0,ld(X2,X1)),rd(X3,ld(X1,X2))) = rd(ld(ld(X1,X2),ld(X0,X3)),ld(X1,X2)),
inference(superposition,[],[f2999,f447]) ).
fof(f3085,plain,
! [X0] : rd(ld(X0,rd(X0,X0)),X0) = ld(ld(X0,X0),rd(rd(ld(X0,X0),X0),X0)),
inference(superposition,[],[f2999,f602]) ).
fof(f3090,plain,
! [X2,X3,X0,X1] : ld(X3,rd(rd(rd(X3,X2),X1),X2)) = rd(ld(X2,ld(X0,rd(X0,X1))),X2),
inference(superposition,[],[f2999,f402]) ).
fof(f3091,plain,
! [X2,X0,X1] : ld(X2,rd(rd(rd(X2,X1),X0),X1)) = rd(ld(X1,rd(ld(X0,X0),X0)),X1),
inference(superposition,[],[f2999,f111]) ).
fof(f3094,plain,
! [X0,X1] : rd(ld(rd(X0,ld(X1,X1)),rd(rd(X0,ld(X1,X1)),X1)),ld(X1,X1)) = ld(X0,rd(rd(rd(X0,ld(X1,X1)),X1),ld(X1,X1))),
inference(superposition,[],[f2999,f403]) ).
fof(f3101,plain,
! [X2,X0,X1] : ld(ld(X0,rd(X1,X2)),ld(X2,ld(rd(X0,X2),X1))) = X2,
inference(superposition,[],[f15,f2999]) ).
fof(f3102,plain,
! [X2,X0,X1] : ld(X2,ld(rd(X0,X2),X1)) = rd(ld(X0,rd(X1,X2)),rd(ld(X2,X2),X2)),
inference(superposition,[],[f109,f2999]) ).
fof(f3103,plain,
! [X2,X0,X1] : rd(ld(X2,X2),X2) = ld(ld(X2,ld(rd(X0,X2),X1)),ld(X0,rd(X1,X2))),
inference(superposition,[],[f111,f2999]) ).
fof(f3110,plain,
! [X2,X3,X0,X1] : ld(X2,ld(rd(X0,X2),X1)) = rd(ld(X0,rd(X1,X2)),ld(X3,rd(X3,X2))),
inference(superposition,[],[f430,f2999]) ).
fof(f3125,plain,
! [X2,X3,X0,X1] : ld(X3,X2) = ld(ld(ld(X2,X3),ld(rd(X0,ld(X2,X3)),X1)),ld(X0,rd(X1,ld(X2,X3)))),
inference(superposition,[],[f419,f2999]) ).
fof(f3133,plain,
! [X2,X0,X1] : ld(ld(rd(ld(X2,X2),X2),ld(rd(X0,rd(ld(X2,X2),X2)),X1)),ld(X0,rd(X1,rd(ld(X2,X2),X2)))) = X2,
inference(superposition,[],[f185,f2999]) ).
fof(f3315,plain,
! [X2,X0,X1] : ld(X0,ld(X2,ld(rd(rd(rd(X1,X2),X0),X2),X1))) = X2,
inference(superposition,[],[f3101,f15]) ).
fof(f3324,plain,
! [X2,X0,X1] : ld(X0,X1) = ld(ld(X1,rd(X2,ld(X0,X1))),ld(ld(X0,X1),ld(X0,X2))),
inference(superposition,[],[f3101,f12]) ).
fof(f3379,plain,
! [X2,X0,X1] : ld(X0,X2) = ld(X1,ld(ld(X0,X2),ld(rd(rd(X0,X1),ld(X0,X2)),X2))),
inference(superposition,[],[f3315,f12]) ).
fof(f3636,plain,
! [X2,X0,X1] : ld(X1,X2) = ld(ld(X2,ld(X0,rd(X0,ld(X1,X2)))),ld(ld(X1,X2),ld(X1,ld(ld(X1,X2),ld(X1,X2))))),
inference(superposition,[],[f3324,f111]) ).
fof(f3691,plain,
! [X0] : ld(X0,rd(X0,X0)) = ld(ld(rd(X0,X0),rd(X0,ld(X0,rd(X0,X0)))),X0),
inference(superposition,[],[f3324,f407]) ).
fof(f3714,plain,
! [X2,X1] : ld(X1,X2) = ld(ld(X2,ld(X2,X1)),ld(ld(X1,X2),ld(X1,ld(ld(X1,X2),ld(X1,X2))))),
inference(forward_demodulation,[],[f3636,f419]) ).
fof(f4160,plain,
! [X2,X3,X0,X1] : rd(ld(X1,X1),X1) = ld(ld(X1,ld(X3,rd(X3,X2))),ld(X0,rd(rd(rd(X0,X1),X2),X1))),
inference(superposition,[],[f111,f3090]) ).
fof(f4198,plain,
! [X2,X3,X0,X1] : ld(ld(rd(ld(X1,X1),X1),ld(X3,rd(X3,X2))),ld(X0,rd(rd(rd(X0,rd(ld(X1,X1),X1)),X2),rd(ld(X1,X1),X1)))) = X1,
inference(superposition,[],[f185,f3090]) ).
fof(f4229,plain,
! [X1] : rd(ld(rd(ld(X1,X1),X1),rd(ld(X1,X1),X1)),rd(ld(X1,X1),X1)) = X1,
inference(backward_demodulation,[],[f4198,f4160]) ).
fof(f4305,plain,
! [X1] : ld(X1,ld(rd(rd(ld(X1,X1),X1),X1),ld(X1,X1))) = X1,
inference(forward_demodulation,[],[f4229,f3102]) ).
fof(f4351,plain,
! [X0,X1] : ld(X1,ld(rd(ld(X0,rd(X0,X1)),X1),ld(X1,X1))) = X1,
inference(superposition,[],[f4305,f111]) ).
fof(f4361,plain,
! [X0,X1] : ld(X0,rd(X0,X1)) = ld(ld(X0,rd(X0,X1)),ld(rd(rd(ld(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))),ld(X0,rd(X0,X1))),rd(ld(X1,X1),X1)),ld(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))))),
inference(superposition,[],[f4305,f562]) ).
fof(f4402,plain,
! [X0,X1] : ld(X0,rd(X0,X1)) = ld(ld(X0,rd(X0,X1)),ld(rd(X1,rd(ld(X1,X1),X1)),ld(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))))),
inference(forward_demodulation,[],[f4361,f750]) ).
fof(f4452,plain,
! [X0,X1] : rd(X0,X0) = ld(ld(X1,rd(X1,X0)),rd(ld(X0,X0),X0)),
inference(superposition,[],[f2999,f4351]) ).
fof(f4453,plain,
! [X0,X1] : rd(ld(rd(ld(X1,rd(X1,X0)),X0),ld(X0,X0)),X0) = X0,
inference(superposition,[],[f12,f4351]) ).
fof(f4562,plain,
! [X2,X0,X1] : rd(X1,X1) = ld(ld(X2,rd(X2,X1)),ld(X0,rd(X0,X1))),
inference(superposition,[],[f4452,f111]) ).
fof(f5332,plain,
! [X0,X1] : rd(ld(X0,X0),X0) = rd(ld(rd(ld(X1,rd(X1,rd(ld(X0,X0),X0))),rd(ld(X0,X0),X0)),rd(X0,X0)),rd(ld(X0,X0),X0)),
inference(superposition,[],[f4453,f602]) ).
fof(f5334,plain,
! [X2,X0,X1] : ld(X2,rd(X2,X0)) = rd(ld(rd(ld(X1,rd(X1,ld(X2,rd(X2,X0)))),ld(X2,rd(X2,X0))),rd(X0,X0)),ld(X2,rd(X2,X0))),
inference(superposition,[],[f4453,f4562]) ).
fof(f5342,plain,
! [X0,X1] : rd(X0,rd(ld(X0,X0),X0)) = ld(rd(ld(X1,rd(X1,X0)),X0),ld(X0,X0)),
inference(superposition,[],[f109,f4453]) ).
fof(f5383,plain,
! [X2,X0,X1] : rd(ld(X0,rd(X0,X1)),X1) = ld(rd(ld(X2,rd(X2,ld(X0,rd(X0,X1)))),ld(X0,rd(X0,X1))),ld(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1)))),
inference(superposition,[],[f478,f4453]) ).
fof(f5386,plain,
! [X0,X1] : rd(rd(ld(X0,X0),X0),X0) = ld(rd(ld(X1,rd(X1,rd(ld(X0,X0),X0))),rd(ld(X0,X0),X0)),ld(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0))),
inference(superposition,[],[f115,f4453]) ).
fof(f5396,plain,
! [X0,X1] : rd(rd(ld(X0,X0),X0),X0) = ld(rd(ld(X1,rd(X1,rd(ld(X0,X0),X0))),rd(ld(X0,X0),X0)),rd(X0,X0)),
inference(forward_demodulation,[],[f5386,f602]) ).
fof(f5399,plain,
! [X0,X1] : rd(ld(X0,rd(X0,X1)),X1) = ld(rd(ld(rd(X0,X1),X0),ld(X0,rd(X0,X1))),ld(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1)))),
inference(forward_demodulation,[],[f5383,f419]) ).
fof(f5451,plain,
! [X2,X0,X1] : ld(X2,rd(X2,X0)) = ld(X0,ld(rd(rd(ld(X1,rd(X1,ld(X2,rd(X2,X0)))),ld(X2,rd(X2,X0))),X0),X0)),
inference(forward_demodulation,[],[f5334,f3110]) ).
fof(f5453,plain,
! [X0,X1] : rd(ld(X0,X0),X0) = ld(X0,ld(rd(rd(ld(X1,rd(X1,rd(ld(X0,X0),X0))),rd(ld(X0,X0),X0)),X0),X0)),
inference(forward_demodulation,[],[f5332,f3102]) ).
fof(f5491,plain,
! [X0] : rd(rd(ld(X0,X0),X0),X0) = ld(rd(X0,rd(ld(X0,X0),X0)),rd(X0,X0)),
inference(forward_demodulation,[],[f5396,f185]) ).
fof(f5494,plain,
! [X0,X1] : rd(ld(X0,rd(X0,X1)),X1) = ld(rd(X1,ld(X0,rd(X0,X1))),ld(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1)))),
inference(forward_demodulation,[],[f5399,f15]) ).
fof(f5505,plain,
! [X2,X0,X1] : ld(X2,rd(X2,X0)) = ld(X0,ld(ld(X1,rd(X1,ld(X2,rd(X2,X0)))),X0)),
inference(forward_demodulation,[],[f5451,f478]) ).
fof(f5507,plain,
! [X0,X1] : rd(ld(X0,X0),X0) = ld(X0,ld(ld(X1,rd(X1,rd(ld(X0,X0),X0))),X0)),
inference(forward_demodulation,[],[f5453,f115]) ).
fof(f5533,plain,
! [X0] : rd(ld(X0,rd(X0,X0)),X0) = ld(ld(X0,X0),ld(rd(X0,rd(ld(X0,X0),X0)),rd(X0,X0))),
inference(backward_demodulation,[],[f3085,f5491]) ).
fof(f5551,plain,
! [X0] : rd(ld(rd(X0,X0),rd(X0,X0)),X0) = rd(X0,rd(ld(ld(rd(X0,ld(X0,rd(X0,X0))),ld(ld(X0,rd(X0,X0)),ld(X0,rd(X0,X0)))),ld(rd(X0,ld(X0,rd(X0,X0))),ld(ld(X0,rd(X0,X0)),ld(X0,rd(X0,X0))))),ld(rd(X0,ld(X0,rd(X0,X0))),ld(ld(X0,rd(X0,X0)),ld(X0,rd(X0,X0)))))),
inference(backward_demodulation,[],[f2980,f5494]) ).
fof(f5553,plain,
! [X0,X1] : rd(X0,rd(ld(X0,X0),X0)) = ld(ld(rd(X0,ld(X1,rd(X1,X0))),ld(ld(X1,rd(X1,X0)),ld(X1,rd(X1,X0)))),ld(X0,X0)),
inference(backward_demodulation,[],[f5342,f5494]) ).
fof(f5557,plain,
! [X2,X0] : ld(X2,rd(X2,X0)) = ld(X0,ld(ld(rd(X2,X0),X2),X0)),
inference(forward_demodulation,[],[f5505,f419]) ).
fof(f5559,plain,
! [X0] : rd(ld(X0,X0),X0) = ld(X0,ld(X0,X0)),
inference(forward_demodulation,[],[f5507,f185]) ).
fof(f5572,plain,
! [X0] : ld(ld(X0,X0),ld(rd(X0,rd(ld(X0,X0),X0)),rd(X0,X0))) = ld(rd(X0,ld(X0,rd(X0,X0))),ld(ld(X0,rd(X0,X0)),ld(X0,rd(X0,X0)))),
inference(forward_demodulation,[],[f5533,f5494]) ).
fof(f5575,plain,
! [X0] : rd(ld(rd(X0,X0),rd(X0,X0)),X0) = rd(X0,ld(rd(rd(X0,ld(X0,rd(X0,X0))),ld(ld(ld(X0,rd(X0,X0)),ld(X0,rd(X0,X0))),rd(X0,ld(X0,rd(X0,X0))))),rd(ld(ld(X0,rd(X0,X0)),ld(X0,rd(X0,X0))),ld(rd(X0,ld(X0,rd(X0,X0))),ld(ld(X0,rd(X0,X0)),ld(X0,rd(X0,X0))))))),
inference(forward_demodulation,[],[f5551,f3078]) ).
fof(f5577,plain,
! [X2,X0] : ld(X2,rd(X2,X0)) = ld(X0,ld(X0,X0)),
inference(forward_demodulation,[],[f5557,f15]) ).
fof(f5579,plain,
! [X0,X1] : rd(rd(X0,X1),ld(X1,ld(X1,X1))) = X0,
inference(backward_demodulation,[],[f109,f5559]) ).
fof(f5581,plain,
! [X0,X1] : rd(rd(X0,ld(X1,ld(X1,X1))),X1) = X0,
inference(backward_demodulation,[],[f115,f5559]) ).
fof(f5606,plain,
! [X1] : rd(X1,X1) = ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))),
inference(backward_demodulation,[],[f602,f5559]) ).
fof(f5611,plain,
! [X2,X0,X1] : rd(ld(X1,ld(X0,X2)),X1) = ld(rd(X0,ld(X1,ld(X1,X1))),rd(X2,X1)),
inference(backward_demodulation,[],[f3075,f5559]) ).
fof(f5614,plain,
! [X2,X0,X1] : ld(X2,rd(rd(rd(X2,X1),X0),X1)) = rd(ld(X1,ld(X0,ld(X0,X0))),X1),
inference(backward_demodulation,[],[f3091,f5559]) ).
fof(f5615,plain,
! [X2,X0,X1] : ld(X2,ld(rd(X0,X2),X1)) = rd(ld(X0,rd(X1,X2)),ld(X2,ld(X2,X2))),
inference(backward_demodulation,[],[f3102,f5559]) ).
fof(f5616,plain,
! [X2,X0,X1] : ld(ld(X2,ld(rd(X0,X2),X1)),ld(X0,rd(X1,X2))) = ld(X2,ld(X2,X2)),
inference(backward_demodulation,[],[f3103,f5559]) ).
fof(f5622,plain,
! [X2,X0,X1] : ld(ld(ld(X2,ld(X2,X2)),ld(rd(X0,ld(X2,ld(X2,X2))),X1)),ld(X0,rd(X1,ld(X2,ld(X2,X2))))) = X2,
inference(backward_demodulation,[],[f3133,f5559]) ).
fof(f5720,plain,
! [X0,X1] : ld(X0,rd(X0,X1)) = ld(ld(X0,rd(X0,X1)),ld(rd(X1,ld(X1,ld(X1,X1))),ld(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))))),
inference(backward_demodulation,[],[f4402,f5559]) ).
fof(f5753,plain,
! [X0,X1] : ld(ld(rd(X0,ld(X1,rd(X1,X0))),ld(ld(X1,rd(X1,X0)),ld(X1,rd(X1,X0)))),ld(X0,X0)) = rd(X0,ld(X0,ld(X0,X0))),
inference(backward_demodulation,[],[f5553,f5559]) ).
fof(f5763,plain,
! [X0,X1] : tuple(x1(X1),x1_2(X1)) != tuple(rd(X1,ld(x1(X1),ld(x1(X1),x1(X1)))),rd(x1_2(X1),ld(X0,rd(X0,X1)))),
inference(backward_demodulation,[],[f406,f5559]) ).
fof(f5776,plain,
! [X0] : ld(rd(X0,ld(X0,rd(X0,X0))),ld(ld(X0,rd(X0,X0)),ld(X0,rd(X0,X0)))) = ld(ld(X0,X0),ld(rd(X0,ld(X0,ld(X0,X0))),rd(X0,X0))),
inference(forward_demodulation,[],[f5572,f5559]) ).
fof(f5778,plain,
! [X0] : rd(ld(rd(X0,X0),rd(X0,X0)),X0) = rd(X0,ld(rd(rd(X0,ld(X0,rd(X0,X0))),ld(ld(ld(X0,rd(X0,X0)),ld(X0,rd(X0,X0))),rd(X0,ld(X0,rd(X0,X0))))),rd(X0,ld(X0,rd(X0,X0))))),
inference(forward_demodulation,[],[f5575,f12]) ).
fof(f5780,plain,
! [X0] : ld(X0,ld(X0,X0)) = ld(ld(rd(X0,X0),rd(X0,ld(X0,ld(X0,X0)))),X0),
inference(backward_demodulation,[],[f3691,f5577]) ).
fof(f5784,plain,
! [X1] : ld(ld(X1,ld(X1,X1)),ld(X1,X1)) = X1,
inference(backward_demodulation,[],[f407,f5577]) ).
fof(f5789,plain,
! [X1] : ld(X1,ld(X1,X1)) = ld(X1,ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),
inference(backward_demodulation,[],[f627,f5577]) ).
fof(f6014,plain,
! [X2,X0] : ld(X2,X0) = ld(ld(X0,X2),ld(ld(X0,X2),ld(X0,X2))),
inference(backward_demodulation,[],[f419,f5577]) ).
fof(f6024,plain,
! [X0,X1] : ld(X0,rd(rd(rd(X0,ld(X1,X1)),X1),ld(X1,X1))) = rd(ld(X1,ld(X1,X1)),ld(X1,X1)),
inference(backward_demodulation,[],[f3094,f5577]) ).
fof(f6028,plain,
! [X1] : tuple(x1(X1),x1_2(X1)) != tuple(rd(X1,ld(x1(X1),ld(x1(X1),x1(X1)))),rd(x1_2(X1),ld(X1,ld(X1,X1)))),
inference(forward_demodulation,[],[f5763,f5577]) ).
fof(f6036,plain,
! [X0] : rd(X0,ld(X0,ld(X0,X0))) = ld(ld(rd(X0,ld(X0,ld(X0,X0))),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(X0,X0)),
inference(forward_demodulation,[],[f5753,f5577]) ).
fof(f6053,plain,
! [X1] : ld(X1,ld(X1,X1)) = ld(ld(X1,ld(X1,X1)),ld(rd(X1,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),
inference(forward_demodulation,[],[f5720,f5577]) ).
fof(f6114,plain,
! [X2] : ld(ld(X2,X2),X2) = X2,
inference(forward_demodulation,[],[f5622,f3125]) ).
fof(f6157,plain,
! [X2,X0,X1] : ld(X2,rd(rd(rd(X2,X1),X0),X1)) = ld(rd(X0,ld(X1,ld(X1,X1))),rd(ld(X0,X0),X1)),
inference(backward_demodulation,[],[f5614,f5611]) ).
fof(f6256,plain,
! [X0] : ld(rd(X0,ld(X0,ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),ld(ld(X0,ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(X0,ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))))) = ld(ld(X0,X0),ld(rd(X0,ld(X0,ld(X0,X0))),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),
inference(forward_demodulation,[],[f5776,f5606]) ).
fof(f6258,plain,
! [X0] : rd(ld(rd(X0,X0),rd(X0,X0)),X0) = rd(X0,ld(ld(ld(X0,rd(X0,X0)),ld(X0,rd(X0,X0))),rd(X0,ld(X0,rd(X0,X0))))),
inference(forward_demodulation,[],[f5778,f15]) ).
fof(f6428,plain,
! [X0] : ld(X0,ld(X0,X0)) = ld(ld(ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))),rd(X0,ld(X0,ld(X0,X0)))),X0),
inference(forward_demodulation,[],[f5780,f5606]) ).
fof(f6516,plain,
! [X1] : rd(ld(X1,ld(X1,X1)),ld(X1,X1)) = ld(rd(X1,ld(ld(X1,X1),ld(ld(X1,X1),ld(X1,X1)))),rd(ld(X1,X1),ld(X1,X1))),
inference(backward_demodulation,[],[f6024,f6157]) ).
fof(f6558,plain,
! [X0] : ld(rd(X0,ld(X0,ld(X0,X0))),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))) = ld(ld(X0,X0),ld(rd(X0,ld(X0,ld(X0,X0))),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),
inference(forward_demodulation,[],[f6256,f5789]) ).
fof(f6560,plain,
! [X0] : rd(ld(rd(X0,X0),rd(X0,X0)),X0) = rd(X0,ld(ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))),rd(X0,ld(X0,ld(X0,X0))))),
inference(forward_demodulation,[],[f6258,f5577]) ).
fof(f6672,plain,
! [X1] : rd(ld(X1,ld(X1,X1)),ld(X1,X1)) = ld(rd(X1,ld(ld(X1,X1),ld(ld(X1,X1),ld(X1,X1)))),ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(X1,X1))),ld(ld(X1,X1),ld(ld(X1,X1),ld(X1,X1))))),
inference(forward_demodulation,[],[f6516,f5606]) ).
fof(f6699,plain,
! [X0] : rd(ld(ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),X0) = rd(X0,ld(ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))),rd(X0,ld(X0,ld(X0,X0))))),
inference(forward_demodulation,[],[f6560,f5606]) ).
fof(f6769,plain,
! [X1] : rd(ld(X1,ld(X1,X1)),ld(X1,X1)) = ld(rd(X1,ld(X1,X1)),ld(ld(X1,X1),ld(X1,X1))),
inference(forward_demodulation,[],[f6672,f616]) ).
fof(f6827,plain,
! [X1] : rd(ld(X1,ld(X1,X1)),ld(X1,X1)) = ld(X1,ld(ld(X1,X1),ld(X1,X1))),
inference(forward_demodulation,[],[f6769,f12]) ).
fof(f6880,plain,
! [X0] : ld(X0,X0) = rd(X0,X0),
inference(superposition,[],[f12,f6114]) ).
fof(f6891,plain,
! [X0,X1] : ld(X1,ld(X0,ld(rd(rd(ld(X0,X0),X1),X0),X0))) = X0,
inference(superposition,[],[f3379,f6114]) ).
fof(f6893,plain,
! [X0] : ld(X0,X0) = ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))),
inference(forward_demodulation,[],[f6880,f5606]) ).
fof(f6894,plain,
! [X1] : ld(X1,X1) = rd(X1,X1),
inference(backward_demodulation,[],[f5606,f6893]) ).
fof(f6900,plain,
! [X0] : rd(X0,ld(X0,ld(X0,X0))) = ld(ld(rd(X0,ld(X0,ld(X0,X0))),ld(X0,X0)),ld(X0,X0)),
inference(backward_demodulation,[],[f6036,f6893]) ).
fof(f6902,plain,
! [X1] : ld(X1,ld(X1,X1)) = ld(ld(X1,ld(X1,X1)),ld(rd(X1,ld(X1,ld(X1,X1))),ld(X1,X1))),
inference(backward_demodulation,[],[f6053,f6893]) ).
fof(f6916,plain,
! [X0] : ld(X0,ld(X0,X0)) = ld(ld(ld(X0,X0),rd(X0,ld(X0,ld(X0,X0)))),X0),
inference(backward_demodulation,[],[f6428,f6893]) ).
fof(f6918,plain,
! [X0] : ld(rd(X0,ld(X0,ld(X0,X0))),ld(X0,X0)) = ld(ld(X0,X0),ld(rd(X0,ld(X0,ld(X0,X0))),ld(X0,X0))),
inference(backward_demodulation,[],[f6558,f6893]) ).
fof(f6920,plain,
! [X0] : rd(ld(ld(X0,X0),ld(X0,X0)),X0) = rd(X0,ld(ld(X0,X0),rd(X0,ld(X0,ld(X0,X0))))),
inference(backward_demodulation,[],[f6699,f6893]) ).
fof(f6977,plain,
! [X0,X1] : ld(ld(X0,X1),ld(X0,X1)) = rd(ld(ld(X0,X1),ld(ld(X0,X1),ld(X0,X1))),ld(X1,X0)),
inference(superposition,[],[f447,f5559]) ).
fof(f6978,plain,
! [X0,X1] : ld(ld(X0,X1),ld(X0,X1)) = rd(ld(X1,X0),ld(X1,X0)),
inference(forward_demodulation,[],[f6977,f6014]) ).
fof(f6981,plain,
! [X0,X1] : ld(ld(X1,X0),ld(X1,X0)) = ld(ld(X0,X1),ld(X0,X1)),
inference(forward_demodulation,[],[f6978,f6894]) ).
fof(f7056,plain,
! [X0] : ld(X0,ld(X0,X0)) = rd(ld(X0,ld(X0,X0)),ld(X0,X0)),
inference(superposition,[],[f12,f6893]) ).
fof(f7068,plain,
! [X0] : ld(X0,ld(X0,X0)) = ld(X0,ld(ld(X0,X0),ld(X0,X0))),
inference(forward_demodulation,[],[f7056,f6827]) ).
fof(f7075,plain,
! [X1] : ld(X1,ld(X1,X1)) = rd(ld(X1,ld(X1,X1)),ld(X1,X1)),
inference(backward_demodulation,[],[f6827,f7068]) ).
fof(f7080,plain,
! [X0] : ld(X0,X0) = ld(ld(X0,ld(X0,ld(X0,X0))),ld(ld(X0,X0),ld(X0,ld(X0,ld(X0,X0))))),
inference(superposition,[],[f3324,f7075]) ).
fof(f7148,plain,
! [X0] : ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))) = ld(ld(ld(X0,X0),ld(X0,X0)),X0),
inference(superposition,[],[f6014,f7068]) ).
fof(f7150,plain,
! [X0] : ld(ld(X0,X0),X0) = ld(ld(ld(X0,X0),ld(X0,X0)),X0),
inference(forward_demodulation,[],[f7148,f6014]) ).
fof(f7154,plain,
! [X0] : ld(ld(ld(X0,X0),ld(X0,X0)),X0) = X0,
inference(forward_demodulation,[],[f7150,f6114]) ).
fof(f7161,plain,
! [X0] : rd(X0,X0) = ld(ld(X0,X0),ld(X0,X0)),
inference(superposition,[],[f12,f7154]) ).
fof(f7181,plain,
! [X0] : ld(X0,X0) = ld(ld(X0,X0),ld(X0,X0)),
inference(forward_demodulation,[],[f7161,f6894]) ).
fof(f7186,plain,
! [X0] : rd(ld(X0,X0),X0) = rd(X0,ld(ld(X0,X0),rd(X0,ld(X0,ld(X0,X0))))),
inference(backward_demodulation,[],[f6920,f7181]) ).
fof(f7204,plain,
! [X0] : ld(X0,ld(X0,X0)) = rd(X0,ld(ld(X0,X0),rd(X0,ld(X0,ld(X0,X0))))),
inference(forward_demodulation,[],[f7186,f5559]) ).
fof(f7382,plain,
! [X0] : ld(X0,ld(X0,ld(rd(ld(X0,ld(X0,X0)),X0),X0))) = X0,
inference(superposition,[],[f6891,f5559]) ).
fof(f7426,plain,
! [X0] : ld(X0,ld(X0,ld(ld(rd(X0,ld(X0,ld(X0,X0))),rd(X0,X0)),X0))) = X0,
inference(forward_demodulation,[],[f7382,f5611]) ).
fof(f7432,plain,
! [X0] : ld(X0,ld(X0,ld(ld(rd(X0,ld(X0,ld(X0,X0))),ld(X0,X0)),X0))) = X0,
inference(forward_demodulation,[],[f7426,f6894]) ).
fof(f7591,plain,
! [X0] : ld(ld(X0,X0),rd(X0,ld(X0,ld(X0,X0)))) = ld(ld(X0,ld(X0,X0)),X0),
inference(superposition,[],[f15,f7204]) ).
fof(f7595,plain,
! [X0] : ld(X0,ld(X0,ld(X0,X0))) = ld(ld(ld(X0,X0),rd(X0,ld(X0,ld(X0,X0)))),ld(ld(ld(X0,X0),rd(X0,ld(X0,ld(X0,X0)))),ld(ld(X0,X0),rd(X0,ld(X0,ld(X0,X0)))))),
inference(superposition,[],[f5577,f7204]) ).
fof(f7600,plain,
! [X0] : ld(rd(X0,ld(X0,ld(X0,X0))),ld(X0,X0)) = ld(X0,ld(X0,ld(X0,X0))),
inference(forward_demodulation,[],[f7595,f6014]) ).
fof(f7601,plain,
! [X0] : ld(X0,ld(X0,X0)) = ld(ld(ld(X0,ld(X0,X0)),X0),X0),
inference(backward_demodulation,[],[f6916,f7591]) ).
fof(f7617,plain,
! [X0] : ld(X0,ld(X0,ld(ld(X0,ld(X0,ld(X0,X0))),X0))) = X0,
inference(backward_demodulation,[],[f7432,f7600]) ).
fof(f7618,plain,
! [X0] : rd(X0,ld(X0,ld(X0,X0))) = ld(ld(X0,ld(X0,ld(X0,X0))),ld(X0,X0)),
inference(backward_demodulation,[],[f6900,f7600]) ).
fof(f7620,plain,
! [X1] : ld(X1,ld(X1,X1)) = ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,ld(X1,X1)))),
inference(backward_demodulation,[],[f6902,f7600]) ).
fof(f7621,plain,
! [X0] : ld(X0,ld(X0,ld(X0,X0))) = ld(ld(X0,X0),ld(X0,ld(X0,ld(X0,X0)))),
inference(backward_demodulation,[],[f6918,f7600]) ).
fof(f7627,plain,
! [X0] : ld(X0,X0) = ld(ld(X0,ld(X0,ld(X0,X0))),ld(X0,ld(X0,ld(X0,X0)))),
inference(backward_demodulation,[],[f7080,f7621]) ).
fof(f7630,plain,
! [X0] : ld(X0,ld(X0,ld(X0,X0))) = ld(ld(ld(X0,ld(X0,ld(X0,X0))),ld(X0,X0)),ld(X0,X0)),
inference(backward_demodulation,[],[f7600,f7618]) ).
fof(f7646,plain,
! [X0,X1] : ld(X0,X1) = ld(ld(ld(X0,X1),ld(X1,X0)),ld(X1,X0)),
inference(superposition,[],[f7601,f6014]) ).
fof(f7647,plain,
! [X0] : rd(X0,ld(X0,ld(X0,X0))) = ld(ld(X0,ld(X0,X0)),X0),
inference(superposition,[],[f12,f7601]) ).
fof(f7659,plain,
! [X0] : ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))) = ld(X0,ld(ld(X0,ld(X0,X0)),X0)),
inference(superposition,[],[f6014,f7601]) ).
fof(f7671,plain,
! [X0] : ld(ld(X0,X0),X0) = ld(X0,ld(ld(X0,ld(X0,X0)),X0)),
inference(forward_demodulation,[],[f7659,f6014]) ).
fof(f7674,plain,
! [X0] : ld(ld(X0,ld(X0,X0)),X0) = ld(ld(X0,ld(X0,ld(X0,X0))),ld(X0,X0)),
inference(forward_demodulation,[],[f7647,f7618]) ).
fof(f7682,plain,
! [X0] : ld(X0,ld(ld(X0,ld(X0,X0)),X0)) = X0,
inference(forward_demodulation,[],[f7671,f6114]) ).
fof(f7688,plain,
! [X0] : ld(X0,ld(X0,ld(X0,X0))) = ld(ld(ld(X0,ld(X0,X0)),X0),ld(X0,X0)),
inference(backward_demodulation,[],[f7630,f7674]) ).
fof(f7690,plain,
! [X0] : rd(X0,ld(X0,ld(X0,X0))) = ld(ld(X0,ld(X0,X0)),X0),
inference(backward_demodulation,[],[f7618,f7674]) ).
fof(f7704,plain,
! [X0,X1] : ld(X1,X0) = ld(ld(X1,X0),ld(ld(X0,X1),ld(X1,X0))),
inference(superposition,[],[f7682,f6014]) ).
fof(f7705,plain,
! [X0] : rd(ld(ld(X0,ld(X0,X0)),X0),X0) = X0,
inference(superposition,[],[f12,f7682]) ).
fof(f7754,plain,
! [X0,X1] : rd(ld(X0,X1),ld(X1,X0)) = ld(ld(ld(X0,X1),ld(ld(X0,X1),ld(X0,X1))),ld(X0,X1)),
inference(superposition,[],[f447,f7705]) ).
fof(f7757,plain,
! [X0,X1] : rd(ld(X0,X1),ld(X1,X0)) = ld(ld(X1,X0),ld(X0,X1)),
inference(forward_demodulation,[],[f7754,f6014]) ).
fof(f7974,plain,
! [X0] : ld(X0,ld(X0,X0)) = ld(ld(X0,ld(ld(X0,ld(X0,ld(X0,X0))),X0)),X0),
inference(superposition,[],[f6014,f7617]) ).
fof(f8591,plain,
! [X2,X0,X1] : ld(X1,ld(X1,X1)) = ld(ld(X1,ld(X0,X2)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X2,X1))),
inference(superposition,[],[f5616,f5581]) ).
fof(f8724,plain,
! [X0] : ld(ld(ld(X0,ld(ld(X0,ld(X0,ld(X0,X0))),X0)),X0),X0) = rd(X0,ld(ld(X0,ld(ld(X0,ld(X0,ld(X0,X0))),X0)),X0)),
inference(superposition,[],[f7757,f7617]) ).
fof(f8835,plain,
! [X0] : ld(X0,ld(ld(X0,ld(X0,ld(X0,X0))),X0)) = ld(ld(ld(X0,ld(ld(X0,ld(X0,ld(X0,X0))),X0)),X0),X0),
inference(forward_demodulation,[],[f8724,f12]) ).
fof(f8856,plain,
! [X0] : ld(ld(X0,ld(X0,X0)),X0) = ld(X0,ld(ld(X0,ld(X0,ld(X0,X0))),X0)),
inference(forward_demodulation,[],[f8835,f7974]) ).
fof(f8906,plain,
! [X0,X1] : ld(ld(X1,X0),ld(X0,X1)) = ld(ld(ld(X0,X1),ld(X1,X0)),ld(ld(X1,X0),ld(X1,X0))),
inference(superposition,[],[f7688,f6014]) ).
fof(f9344,plain,
! [X2,X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X2,ld(X1,ld(X1,X1))),rd(X0,X1))) = rd(ld(X2,X0),ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),
inference(superposition,[],[f5615,f5579]) ).
fof(f9357,plain,
! [X0,X1] : rd(rd(X0,X1),ld(X1,ld(X1,X1))) = ld(X1,ld(rd(ld(rd(X0,X1),rd(X0,X1)),X1),X0)),
inference(superposition,[],[f5615,f6114]) ).
fof(f9398,plain,
! [X0,X1] : ld(X1,ld(rd(ld(rd(X0,X1),rd(X0,X1)),X1),X0)) = X0,
inference(forward_demodulation,[],[f9357,f5579]) ).
fof(f9410,plain,
! [X2,X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X2,ld(X1,ld(X1,X1))),rd(X0,X1))) = rd(ld(X2,X0),ld(ld(X1,X1),X1)),
inference(forward_demodulation,[],[f9344,f6014]) ).
fof(f9474,plain,
! [X2,X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X2,ld(X1,ld(X1,X1))),rd(X0,X1))) = rd(ld(X2,X0),X1),
inference(forward_demodulation,[],[f9410,f6114]) ).
fof(f9638,plain,
! [X0,X1] : ld(X1,ld(ld(ld(X1,ld(X1,X1)),ld(rd(rd(X0,X1),ld(X1,ld(X1,X1))),rd(rd(X0,X1),X1))),X0)) = X0,
inference(backward_demodulation,[],[f9398,f9474]) ).
fof(f9772,plain,
! [X0,X1] : ld(X1,ld(ld(ld(X1,ld(X1,X1)),ld(X0,rd(rd(X0,X1),X1))),X0)) = X0,
inference(forward_demodulation,[],[f9638,f5579]) ).
fof(f10669,plain,
! [X0,X1] : ld(ld(X0,X1),ld(ld(ld(ld(X0,X1),ld(ld(X0,X1),ld(X0,X1))),ld(X1,rd(X0,ld(X0,X1)))),X1)) = X1,
inference(superposition,[],[f9772,f12]) ).
fof(f10675,plain,
! [X0,X1] : ld(ld(X1,X1),ld(ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(X1,X1))),ld(X0,X0)),X0)) = X0,
inference(superposition,[],[f9772,f447]) ).
fof(f10711,plain,
! [X0,X1] : ld(ld(X1,X1),ld(ld(ld(X1,X1),ld(X0,X0)),X0)) = X0,
inference(forward_demodulation,[],[f10675,f616]) ).
fof(f10716,plain,
! [X0,X1] : ld(ld(X0,X1),ld(ld(ld(X1,X0),ld(X1,rd(X0,ld(X0,X1)))),X1)) = X1,
inference(forward_demodulation,[],[f10669,f6014]) ).
fof(f10794,plain,
! [X0,X1] : ld(X1,X1) = rd(ld(ld(ld(X1,X1),ld(X0,X0)),X0),X0),
inference(superposition,[],[f12,f10711]) ).
fof(f10806,plain,
! [X0,X1] : ld(X0,ld(X0,X0)) = ld(ld(ld(ld(X1,X1),ld(X0,X0)),X0),ld(X1,X1)),
inference(superposition,[],[f6014,f10711]) ).
fof(f10824,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,ld(X0,X0)),ld(rd(ld(ld(X1,X1),ld(X0,X0)),ld(X0,ld(X0,X0))),rd(X0,X0))),
inference(forward_demodulation,[],[f10794,f9474]) ).
fof(f10835,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,ld(X0,X0)),ld(rd(ld(ld(X1,X1),ld(X0,X0)),ld(X0,ld(X0,X0))),ld(X0,X0))),
inference(forward_demodulation,[],[f10824,f6894]) ).
fof(f10842,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,ld(X0,X0)),ld(ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(rd(ld(X1,X1),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),rd(ld(X0,X0),ld(X0,ld(X0,X0))))),ld(X0,X0))),
inference(forward_demodulation,[],[f10835,f9474]) ).
fof(f10846,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,ld(X0,X0)),ld(ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(rd(ld(X1,X1),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),X0)),ld(X0,X0))),
inference(forward_demodulation,[],[f10842,f12]) ).
fof(f10850,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,ld(X0,X0)),ld(ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(ld(ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))))),ld(rd(X1,ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))))),rd(X1,ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))))),X0)),ld(X0,X0))),
inference(forward_demodulation,[],[f10846,f9474]) ).
fof(f10854,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,ld(X0,X0)),ld(ld(ld(ld(X0,X0),X0),ld(ld(ld(ld(ld(X0,X0),X0),ld(ld(ld(X0,X0),X0),ld(ld(X0,X0),X0))),ld(rd(X1,ld(ld(ld(X0,X0),X0),ld(ld(ld(X0,X0),X0),ld(ld(X0,X0),X0)))),rd(X1,ld(ld(X0,X0),X0)))),X0)),ld(X0,X0))),
inference(forward_demodulation,[],[f10850,f6014]) ).
fof(f10858,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),rd(X1,X0))),X0)),ld(X0,X0))),
inference(forward_demodulation,[],[f10854,f6114]) ).
fof(f10901,plain,
! [X0,X1] : ld(ld(ld(X1,X1),ld(X0,X0)),X0) = ld(X0,ld(ld(ld(ld(ld(ld(X1,X1),ld(X0,X0)),X0),ld(X1,X1)),ld(ld(ld(ld(X1,X1),ld(X0,X0)),X0),rd(ld(X1,X1),X0))),ld(ld(ld(X1,X1),ld(X0,X0)),X0))),
inference(superposition,[],[f10716,f10711]) ).
fof(f10904,plain,
! [X0,X1] : ld(ld(X1,X0),ld(X0,X1)) = ld(ld(X0,X1),ld(ld(ld(ld(ld(X1,X0),ld(X0,X1)),ld(X0,X1)),ld(ld(ld(X1,X0),ld(X0,X1)),rd(ld(X0,X1),ld(X0,X1)))),ld(ld(X1,X0),ld(X0,X1)))),
inference(superposition,[],[f10716,f7704]) ).
fof(f10979,plain,
! [X0,X1] : ld(ld(X1,X0),ld(X0,X1)) = ld(ld(X0,X1),ld(ld(ld(ld(ld(X1,X0),ld(X0,X1)),ld(X0,X1)),ld(ld(ld(X1,X0),ld(X0,X1)),ld(ld(X0,X1),ld(X0,X1)))),ld(ld(X1,X0),ld(X0,X1)))),
inference(forward_demodulation,[],[f10904,f6894]) ).
fof(f10982,plain,
! [X0,X1] : ld(ld(ld(X1,X1),ld(X0,X0)),X0) = ld(X0,ld(ld(ld(ld(ld(ld(X1,X1),ld(X0,X0)),X0),ld(X1,X1)),ld(ld(ld(ld(X1,X1),ld(X0,X0)),X0),ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),rd(X1,X0))))),ld(ld(ld(X1,X1),ld(X0,X0)),X0))),
inference(forward_demodulation,[],[f10901,f9474]) ).
fof(f11048,plain,
! [X0,X1] : ld(ld(X1,X0),ld(X0,X1)) = ld(ld(X0,X1),ld(ld(ld(ld(ld(X1,X0),ld(X0,X1)),ld(X0,X1)),ld(ld(X0,X1),ld(X1,X0))),ld(ld(X1,X0),ld(X0,X1)))),
inference(forward_demodulation,[],[f10979,f8906]) ).
fof(f11051,plain,
! [X0,X1] : ld(ld(ld(X1,X1),ld(X0,X0)),X0) = ld(X0,ld(ld(ld(X0,ld(X0,X0)),ld(ld(ld(ld(X1,X1),ld(X0,X0)),X0),ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),rd(X1,X0))))),ld(ld(ld(X1,X1),ld(X0,X0)),X0))),
inference(forward_demodulation,[],[f10982,f10806]) ).
fof(f11108,plain,
! [X0,X1] : ld(ld(X1,X0),ld(X0,X1)) = ld(ld(X0,X1),ld(ld(ld(X1,X0),ld(ld(X0,X1),ld(X1,X0))),ld(ld(X1,X0),ld(X0,X1)))),
inference(forward_demodulation,[],[f11048,f7646]) ).
fof(f11155,plain,
! [X0,X1] : ld(ld(X1,X0),ld(X0,X1)) = ld(ld(X0,X1),ld(ld(X1,X0),ld(ld(X1,X0),ld(X0,X1)))),
inference(forward_demodulation,[],[f11108,f7704]) ).
fof(f11705,plain,
! [X0,X1] : rd(ld(X1,X1),ld(X0,ld(X0,X0))) = ld(ld(ld(X1,X1),ld(X0,X0)),X0),
inference(superposition,[],[f12,f10806]) ).
fof(f11744,plain,
! [X0,X1] : ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(rd(X1,ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),rd(X1,ld(X0,ld(X0,X0))))) = ld(ld(ld(X1,X1),ld(X0,X0)),X0),
inference(forward_demodulation,[],[f11705,f9474]) ).
fof(f11762,plain,
! [X0,X1] : ld(ld(ld(X0,X0),X0),ld(rd(X1,ld(ld(X0,X0),X0)),rd(X1,ld(X0,ld(X0,X0))))) = ld(ld(ld(X1,X1),ld(X0,X0)),X0),
inference(forward_demodulation,[],[f11744,f6014]) ).
fof(f11767,plain,
! [X0,X1] : ld(X0,ld(rd(X1,X0),rd(X1,ld(X0,ld(X0,X0))))) = ld(ld(ld(X1,X1),ld(X0,X0)),X0),
inference(forward_demodulation,[],[f11762,f6114]) ).
fof(f12159,plain,
! [X0] : ld(ld(ld(X0,ld(X0,X0)),ld(X0,X0)),ld(X0,ld(X0,X0))) = ld(ld(X0,ld(X0,X0)),ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,X0))),ld(X0,ld(X0,X0)))),
inference(superposition,[],[f8856,f6893]) ).
fof(f12202,plain,
! [X0] : ld(X0,ld(X0,ld(X0,X0))) = ld(ld(X0,ld(X0,X0)),ld(ld(ld(X0,ld(X0,X0)),X0),ld(X0,ld(X0,X0)))),
inference(forward_demodulation,[],[f12159,f5784]) ).
fof(f12430,plain,
! [X0,X1] : rd(ld(X0,X0),X1) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,X0),ld(X1,ld(X1,X1))),rd(ld(X0,X0),X1))),
inference(superposition,[],[f9474,f7181]) ).
fof(f12443,plain,
! [X0,X1] : rd(ld(X0,X0),X1) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,ld(X0,X0)),ld(X1,ld(X1,X1))),rd(ld(X0,ld(X0,X0)),X1))),
inference(superposition,[],[f9474,f6893]) ).
fof(f12444,plain,
! [X0,X1] : rd(ld(X0,ld(X0,X0)),X1) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,ld(X0,X0)),ld(X1,ld(X1,X1))),rd(ld(X0,ld(X0,ld(X0,X0))),X1))),
inference(superposition,[],[f9474,f7620]) ).
fof(f12446,plain,
! [X0,X1] : rd(ld(X0,X0),X1) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,ld(X0,ld(X0,X0))),ld(X1,ld(X1,X1))),rd(ld(X0,ld(X0,ld(X0,X0))),X1))),
inference(superposition,[],[f9474,f7627]) ).
fof(f12470,plain,
! [X2,X0,X1] : ld(X1,X2) = rd(ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),rd(X2,X0))),ld(X0,ld(X0,X0))),
inference(superposition,[],[f5579,f9474]) ).
fof(f12495,plain,
! [X2,X0,X1] : ld(X1,X2) = ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(rd(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),rd(ld(rd(X1,ld(X0,ld(X0,X0))),rd(X2,X0)),ld(X0,ld(X0,X0))))),
inference(forward_demodulation,[],[f12470,f9474]) ).
fof(f12515,plain,
! [X0,X1] : rd(ld(X0,X0),X1) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,ld(X0,ld(X0,X0))),ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(ld(X0,ld(X0,X0)),X1))))),
inference(forward_demodulation,[],[f12446,f9474]) ).
fof(f12517,plain,
! [X0,X1] : rd(ld(X0,ld(X0,X0)),X1) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,ld(X0,X0)),ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(ld(X0,ld(X0,X0)),X1))))),
inference(forward_demodulation,[],[f12444,f9474]) ).
fof(f12518,plain,
! [X0,X1] : rd(ld(X0,X0),X1) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,ld(X0,X0)),ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(ld(X0,X0),X1))))),
inference(forward_demodulation,[],[f12443,f9474]) ).
fof(f12531,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,X0),ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))),
inference(forward_demodulation,[],[f12430,f9474]) ).
fof(f12545,plain,
! [X2,X0,X1] : ld(X1,X2) = ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(rd(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(rd(rd(X1,ld(X0,ld(X0,X0))),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),rd(rd(X2,X0),ld(X0,ld(X0,X0))))))),
inference(forward_demodulation,[],[f12495,f9474]) ).
fof(f12564,plain,
! [X0,X1] : rd(ld(X0,X0),X1) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,ld(X0,ld(X0,X0))),ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(ld(X0,X0),X1))))))),
inference(forward_demodulation,[],[f12515,f9474]) ).
fof(f12566,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(ld(X0,X0),X1))) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,ld(X0,X0)),ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(ld(X0,X0),X1))))))),
inference(forward_demodulation,[],[f12517,f9474]) ).
fof(f12567,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,ld(X0,X0)),ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))),
inference(forward_demodulation,[],[f12518,f9474]) ).
fof(f12580,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),rd(X0,ld(X1,ld(X1,X1))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))),
inference(forward_demodulation,[],[f12531,f9474]) ).
fof(f12591,plain,
! [X2,X0,X1] : ld(X1,X2) = ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(rd(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(rd(rd(X1,ld(X0,ld(X0,X0))),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),X2)))),
inference(forward_demodulation,[],[f12545,f5579]) ).
fof(f12607,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,ld(X0,ld(X0,X0))),ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12564,f9474]) ).
fof(f12609,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))) = ld(ld(X1,ld(X1,X1)),ld(rd(ld(X0,ld(X0,X0)),ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12566,f9474]) ).
fof(f12610,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),rd(ld(X0,X0),ld(X1,ld(X1,X1))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))),
inference(forward_demodulation,[],[f12567,f9474]) ).
fof(f12623,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X1,X1),X1),ld(rd(X0,ld(ld(X1,X1),X1)),rd(X0,ld(X1,ld(X1,X1))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))),
inference(forward_demodulation,[],[f12580,f6014]) ).
fof(f12632,plain,
! [X2,X0,X1] : ld(X1,X2) = ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(rd(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0))))),ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(X0,X0)),ld(X0,ld(X0,X0)))),ld(X1,X2)))),
inference(forward_demodulation,[],[f12591,f5579]) ).
fof(f12648,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),rd(ld(X0,ld(X0,X0)),ld(X1,ld(X1,X1))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12607,f9474]) ).
fof(f12650,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),rd(ld(X0,X0),ld(X1,ld(X1,X1))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12609,f9474]) ).
fof(f12651,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),rd(X0,ld(X1,ld(X1,X1))))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))),
inference(forward_demodulation,[],[f12610,f9474]) ).
fof(f12664,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),rd(X0,ld(X1,ld(X1,X1))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))),
inference(forward_demodulation,[],[f12623,f6114]) ).
fof(f12672,plain,
! [X2,X0,X1] : ld(X1,X2) = ld(ld(ld(X0,X0),X0),ld(rd(ld(X0,ld(X0,X0)),ld(ld(X0,X0),X0)),ld(ld(ld(X0,X0),X0),ld(X1,X2)))),
inference(forward_demodulation,[],[f12632,f6014]) ).
fof(f12688,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),rd(ld(X0,X0),ld(X1,ld(X1,X1))))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12648,f9474]) ).
fof(f12690,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),rd(X0,ld(X1,ld(X1,X1))))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12650,f9474]) ).
fof(f12691,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X1,X1),X1),ld(rd(X0,ld(ld(X1,X1),X1)),ld(ld(ld(X1,X1),X1),ld(rd(X0,ld(ld(X1,X1),X1)),rd(X0,ld(X1,ld(X1,X1))))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))),
inference(forward_demodulation,[],[f12651,f6014]) ).
fof(f12704,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X0,X0),ld(X1,X1)),X1),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))),
inference(forward_demodulation,[],[f12664,f11767]) ).
fof(f12712,plain,
! [X2,X0,X1] : ld(X1,X2) = ld(X0,ld(rd(ld(X0,ld(X0,X0)),X0),ld(X0,ld(X1,X2)))),
inference(forward_demodulation,[],[f12672,f6114]) ).
fof(f12726,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),ld(ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1)))),ld(rd(X0,ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))),rd(X0,ld(X1,ld(X1,X1))))))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12688,f9474]) ).
fof(f12728,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X1,X1),X1),ld(rd(X0,ld(ld(X1,X1),X1)),ld(ld(ld(X1,X1),X1),ld(rd(X0,ld(ld(X1,X1),X1)),rd(X0,ld(X1,ld(X1,X1))))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12690,f6014]) ).
fof(f12729,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(X1,ld(rd(X0,X1),rd(X0,ld(X1,ld(X1,X1))))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))),
inference(forward_demodulation,[],[f12691,f6114]) ).
fof(f12742,plain,
! [X0,X1] : ld(ld(ld(X1,X1),ld(X0,X0)),X0) = ld(X0,ld(ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),rd(X1,X0))),ld(ld(ld(X1,X1),ld(X0,X0)),X0))),
inference(backward_demodulation,[],[f11051,f12704]) ).
fof(f12750,plain,
! [X2,X0,X1] : ld(X1,X2) = ld(X0,ld(ld(ld(X0,ld(X0,X0)),ld(rd(X0,ld(X0,ld(X0,X0))),rd(ld(X0,X0),X0))),ld(X0,ld(X1,X2)))),
inference(forward_demodulation,[],[f12712,f9474]) ).
fof(f12761,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(ld(ld(X1,X1),X1),ld(rd(X0,ld(ld(X1,X1),X1)),ld(ld(ld(X1,X1),X1),ld(rd(X0,ld(ld(X1,X1),X1)),ld(ld(ld(X1,X1),X1),ld(rd(X0,ld(ld(X1,X1),X1)),rd(X0,ld(X1,ld(X1,X1))))))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12726,f6014]) ).
fof(f12763,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(X1,ld(rd(X0,X1),rd(X0,ld(X1,ld(X1,X1))))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12728,f6114]) ).
fof(f12764,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(ld(ld(X0,X0),ld(X1,X1)),X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))),
inference(forward_demodulation,[],[f12729,f11767]) ).
fof(f12780,plain,
! [X2,X0,X1] : ld(X1,X2) = ld(X0,ld(ld(ld(X0,ld(X0,X0)),ld(rd(X0,ld(X0,ld(X0,X0))),ld(ld(X0,ld(X0,X0)),ld(rd(X0,ld(X0,ld(X0,X0))),rd(X0,X0))))),ld(X0,ld(X1,X2)))),
inference(forward_demodulation,[],[f12750,f9474]) ).
fof(f12788,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(X1,ld(rd(X0,X1),ld(X1,ld(rd(X0,X1),rd(X0,ld(X1,ld(X1,X1))))))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12761,f6114]) ).
fof(f12790,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(ld(ld(X0,X0),ld(X1,X1)),X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12763,f11767]) ).
fof(f12806,plain,
! [X2,X0,X1] : ld(X1,X2) = ld(X0,ld(ld(ld(X0,ld(X0,X0)),ld(rd(X0,ld(X0,ld(X0,X0))),ld(X0,ld(X0,X0)))),ld(X0,ld(X1,X2)))),
inference(forward_demodulation,[],[f12780,f8591]) ).
fof(f12814,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(X1,ld(rd(X0,X1),ld(ld(ld(X0,X0),ld(X1,X1)),X1))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(forward_demodulation,[],[f12788,f11767]) ).
fof(f12824,plain,
! [X2,X0,X1] : ld(X1,X2) = ld(X0,ld(ld(ld(X0,ld(X0,X0)),ld(ld(ld(X0,ld(X0,X0)),X0),ld(X0,ld(X0,X0)))),ld(X0,ld(X1,X2)))),
inference(forward_demodulation,[],[f12806,f7690]) ).
fof(f12832,plain,
! [X2,X0,X1] : ld(X1,X2) = ld(X0,ld(ld(X0,ld(X0,ld(X0,X0))),ld(X0,ld(X1,X2)))),
inference(forward_demodulation,[],[f12824,f12202]) ).
fof(f12896,plain,
! [X0,X1] : ld(X1,ld(ld(X1,ld(X1,ld(X1,X1))),ld(X1,X0))) = X0,
inference(superposition,[],[f12832,f6114]) ).
fof(f12905,plain,
! [X0,X1] : ld(ld(ld(X1,ld(X1,X1)),ld(X0,rd(rd(X0,X1),X1))),X0) = ld(X1,ld(ld(X1,ld(X1,ld(X1,X1))),X0)),
inference(superposition,[],[f12832,f9772]) ).
fof(f12910,plain,
! [X0,X1] : ld(ld(ld(X1,X1),ld(X0,X0)),X0) = ld(ld(X1,X1),ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(ld(X1,X1),ld(X1,X1)))),X0)),
inference(superposition,[],[f12832,f10711]) ).
fof(f13004,plain,
! [X0,X1] : ld(ld(ld(X1,X1),ld(X0,X0)),X0) = ld(ld(X1,X1),ld(ld(ld(X1,X1),ld(X1,X1)),X0)),
inference(forward_demodulation,[],[f12910,f11155]) ).
fof(f13008,plain,
! [X0,X1] : ld(X1,ld(X1,ld(ld(X1,ld(X1,ld(X1,X1))),X0))) = X0,
inference(backward_demodulation,[],[f9772,f12905]) ).
fof(f13131,plain,
! [X0,X1] : ld(ld(ld(X1,X1),ld(X0,X0)),X0) = ld(ld(X1,X1),ld(ld(X1,X1),X0)),
inference(forward_demodulation,[],[f13004,f7181]) ).
fof(f13191,plain,
! [X0,X1] : ld(ld(X1,X1),ld(ld(X1,X1),ld(ld(X1,X1),X0))) = X0,
inference(backward_demodulation,[],[f10711,f13131]) ).
fof(f13194,plain,
! [X0,X1] : ld(X0,ld(X0,X0)) = ld(ld(ld(X1,X1),ld(ld(X1,X1),X0)),ld(X1,X1)),
inference(backward_demodulation,[],[f10806,f13131]) ).
fof(f13235,plain,
! [X0,X1] : ld(ld(X1,X1),ld(ld(X1,X1),X0)) = ld(X0,ld(ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),rd(X1,X0))),ld(ld(X1,X1),ld(ld(X1,X1),X0)))),
inference(backward_demodulation,[],[f12742,f13131]) ).
fof(f13238,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))),
inference(backward_demodulation,[],[f12764,f13131]) ).
fof(f13241,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(backward_demodulation,[],[f12790,f13131]) ).
fof(f13246,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))))))),
inference(backward_demodulation,[],[f12814,f13131]) ).
fof(f13380,plain,
! [X0,X1] : rd(ld(X1,ld(X1,ld(X1,X1))),X0) = ld(X1,ld(X1,ld(X0,ld(X0,X0)))),
inference(superposition,[],[f13008,f5577]) ).
fof(f13416,plain,
! [X0,X1] : ld(X1,ld(X1,ld(X0,ld(X0,X0)))) = ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),rd(ld(X1,ld(X1,X1)),X0))),
inference(forward_demodulation,[],[f13380,f9474]) ).
fof(f13446,plain,
! [X0,X1] : ld(X1,ld(X1,ld(X0,ld(X0,X0)))) = ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),rd(ld(X1,X1),X0))))),
inference(forward_demodulation,[],[f13416,f9474]) ).
fof(f13457,plain,
! [X0,X1] : ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),rd(X1,X0))))))) = ld(X1,ld(X1,ld(X0,ld(X0,X0)))),
inference(forward_demodulation,[],[f13446,f9474]) ).
fof(f13466,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))),ld(X0,ld(X0,ld(X1,ld(X1,X1)))))),
inference(backward_demodulation,[],[f13241,f13457]) ).
fof(f13467,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))))),ld(X0,ld(X0,ld(X1,ld(X1,X1)))))),
inference(backward_demodulation,[],[f13246,f13457]) ).
fof(f13489,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(rd(X1,X0),ld(X0,ld(rd(X1,X0),ld(ld(X1,X1),ld(ld(X1,X1),X0)))))),ld(X1,ld(X1,ld(X0,ld(X0,X0)))))),X0)),ld(X0,X0))),
inference(backward_demodulation,[],[f10858,f13467]) ).
fof(f13511,plain,
! [X0,X1] : ld(ld(X1,X1),ld(ld(X1,X1),X0)) = ld(X0,ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(rd(X1,X0),ld(X0,ld(rd(X1,X0),ld(ld(X1,X1),ld(ld(X1,X1),X0)))))),ld(X1,ld(X1,ld(X0,ld(X0,X0)))))),ld(ld(X1,X1),ld(ld(X1,X1),X0)))),
inference(backward_demodulation,[],[f13235,f13467]) ).
fof(f13512,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))))),ld(X0,ld(X0,ld(X1,ld(X1,X1)))))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))),ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))))),ld(X0,ld(X0,ld(X1,ld(X1,X1)))))))))),
inference(backward_demodulation,[],[f13238,f13467]) ).
fof(f13526,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))),ld(X0,ld(X0,ld(X1,ld(X1,X1)))))) = ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))))),ld(X0,ld(X0,ld(X1,ld(X1,X1)))))))),
inference(forward_demodulation,[],[f13466,f13467]) ).
fof(f13549,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))))),ld(X0,ld(X0,ld(X1,ld(X1,X1)))))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))),ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))),ld(X0,ld(X0,ld(X1,ld(X1,X1)))))))),
inference(backward_demodulation,[],[f13512,f13526]) ).
fof(f13565,plain,
! [X0,X1] : ld(ld(X1,ld(X1,X1)),ld(rd(X0,ld(X1,ld(X1,X1))),rd(X0,X1))) = ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))),ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(rd(X0,X1),ld(ld(X0,X0),ld(ld(X0,X0),X1)))),ld(X0,ld(X0,ld(X1,ld(X1,X1)))))))),
inference(backward_demodulation,[],[f13467,f13549]) ).
fof(f13573,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(rd(X1,X0),ld(ld(X1,X1),ld(ld(X1,X1),X0)))),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(rd(X1,X0),ld(ld(X1,X1),ld(ld(X1,X1),X0)))),ld(X1,ld(X1,ld(X0,ld(X0,X0)))))))),X0)),ld(X0,X0))),
inference(backward_demodulation,[],[f13489,f13549]) ).
fof(f13586,plain,
! [X0,X1] : ld(ld(X1,X1),ld(ld(X1,X1),X0)) = ld(X0,ld(ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(rd(X1,X0),ld(ld(X1,X1),ld(ld(X1,X1),X0)))),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(rd(X1,X0),ld(ld(X1,X1),ld(ld(X1,X1),X0)))),ld(X1,ld(X1,ld(X0,ld(X0,X0)))))))),ld(ld(X1,X1),ld(ld(X1,X1),X0)))),
inference(backward_demodulation,[],[f13511,f13549]) ).
fof(f13641,plain,
! [X0,X1] : rd(ld(X1,X1),X0) = ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,ld(X0,X0)))),
inference(superposition,[],[f13191,f5577]) ).
fof(f13682,plain,
! [X0,X1] : ld(ld(X0,ld(X0,X0)),ld(rd(X1,ld(X0,ld(X0,X0))),rd(X1,X0))) = ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,ld(X0,X0)))),
inference(forward_demodulation,[],[f13641,f9474]) ).
fof(f13711,plain,
! [X0,X1] : ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(rd(X1,X0),ld(ld(X1,X1),ld(ld(X1,X1),X0)))),ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(rd(X1,X0),ld(ld(X1,X1),ld(ld(X1,X1),X0)))),ld(X1,ld(X1,ld(X0,ld(X0,X0)))))))) = ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,ld(X0,X0)))),
inference(forward_demodulation,[],[f13682,f13565]) ).
fof(f13727,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,ld(X0,X0)),ld(ld(X0,ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,ld(X0,X0)))),X0)),ld(X0,X0))),
inference(backward_demodulation,[],[f13573,f13711]) ).
fof(f13740,plain,
! [X0,X1] : ld(ld(X1,X1),ld(ld(X1,X1),X0)) = ld(X0,ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,ld(X0,X0)))),ld(ld(X1,X1),ld(ld(X1,X1),X0)))),
inference(backward_demodulation,[],[f13586,f13711]) ).
fof(f13781,plain,
! [X0,X1] : ld(ld(X1,ld(X1,ld(X1,X1))),ld(X1,X0)) = ld(X1,ld(ld(X1,ld(X1,ld(X1,X1))),X0)),
inference(superposition,[],[f12896,f12896]) ).
fof(f13782,plain,
! [X0,X1] : rd(X1,X0) = ld(X1,ld(ld(X1,ld(X1,ld(X1,X1))),ld(X0,ld(X0,X0)))),
inference(superposition,[],[f12896,f5577]) ).
fof(f14302,plain,
! [X1] : tuple(x1(X1),x1_2(X1)) != tuple(ld(X1,ld(ld(X1,ld(X1,ld(X1,X1))),ld(ld(x1(X1),ld(x1(X1),x1(X1))),ld(ld(x1(X1),ld(x1(X1),x1(X1))),ld(x1(X1),ld(x1(X1),x1(X1))))))),rd(x1_2(X1),ld(X1,ld(X1,X1)))),
inference(backward_demodulation,[],[f6028,f13782]) ).
fof(f14349,plain,
! [X1] : tuple(x1(X1),x1_2(X1)) != tuple(ld(X1,ld(ld(X1,ld(X1,ld(X1,X1))),ld(ld(x1(X1),ld(x1(X1),x1(X1))),ld(ld(x1(X1),ld(x1(X1),x1(X1))),ld(x1(X1),ld(x1(X1),x1(X1))))))),ld(x1_2(X1),ld(ld(x1_2(X1),ld(x1_2(X1),ld(x1_2(X1),x1_2(X1)))),ld(ld(X1,ld(X1,X1)),ld(ld(X1,ld(X1,X1)),ld(X1,ld(X1,X1))))))),
inference(forward_demodulation,[],[f14302,f13782]) ).
fof(f14759,plain,
! [X1] : tuple(x1(X1),x1_2(X1)) != tuple(ld(X1,ld(ld(X1,ld(X1,ld(X1,X1))),ld(ld(x1(X1),ld(x1(X1),x1(X1))),ld(ld(x1(X1),ld(x1(X1),x1(X1))),ld(x1(X1),ld(x1(X1),x1(X1))))))),ld(x1_2(X1),ld(ld(x1_2(X1),ld(x1_2(X1),ld(x1_2(X1),x1_2(X1)))),ld(ld(X1,X1),X1)))),
inference(forward_demodulation,[],[f14349,f6014]) ).
fof(f15075,plain,
! [X1] : tuple(x1(X1),x1_2(X1)) != tuple(ld(X1,ld(ld(X1,ld(X1,ld(X1,X1))),ld(ld(x1(X1),ld(x1(X1),x1(X1))),ld(ld(x1(X1),ld(x1(X1),x1(X1))),ld(x1(X1),ld(x1(X1),x1(X1))))))),ld(x1_2(X1),ld(ld(x1_2(X1),ld(x1_2(X1),ld(x1_2(X1),x1_2(X1)))),X1))),
inference(forward_demodulation,[],[f14759,f6114]) ).
fof(f15347,plain,
! [X1] : tuple(x1(X1),x1_2(X1)) != tuple(ld(X1,ld(ld(X1,ld(X1,ld(X1,X1))),ld(ld(x1(X1),x1(X1)),x1(X1)))),ld(x1_2(X1),ld(ld(x1_2(X1),ld(x1_2(X1),ld(x1_2(X1),x1_2(X1)))),X1))),
inference(forward_demodulation,[],[f15075,f6014]) ).
fof(f15535,plain,
! [X1] : tuple(x1(X1),x1_2(X1)) != tuple(ld(X1,ld(ld(X1,ld(X1,ld(X1,X1))),x1(X1))),ld(x1_2(X1),ld(ld(x1_2(X1),ld(x1_2(X1),ld(x1_2(X1),x1_2(X1)))),X1))),
inference(forward_demodulation,[],[f15347,f6114]) ).
fof(f17340,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(ld(X0,X0),ld(X0,X0)),ld(ld(ld(X0,X0),ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(ld(X0,X0),ld(X0,X0)))),ld(X0,X0))),ld(X0,X0))),
inference(superposition,[],[f13727,f7181]) ).
fof(f17363,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,X0),ld(ld(ld(X0,X0),ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,X0))),ld(X0,X0))),ld(X0,X0))),
inference(forward_demodulation,[],[f17340,f7181]) ).
fof(f17474,plain,
! [X0] : tuple(x1(ld(X0,X0)),x1_2(ld(X0,X0))) != tuple(ld(ld(X0,X0),ld(ld(X0,X0),x1(ld(X0,X0)))),ld(x1_2(ld(X0,X0)),ld(ld(x1_2(ld(X0,X0)),ld(x1_2(ld(X0,X0)),ld(x1_2(ld(X0,X0)),x1_2(ld(X0,X0))))),ld(X0,X0)))),
inference(superposition,[],[f15535,f13191]) ).
fof(f17487,plain,
! [X2,X0,X1] : ld(ld(ld(X2,X2),ld(ld(X0,X1),ld(X0,X1))),ld(X1,X0)) = ld(ld(X2,X2),ld(ld(X2,X2),ld(X1,X0))),
inference(superposition,[],[f13131,f6981]) ).
fof(f17511,plain,
! [X0,X1] : ld(X1,ld(ld(X0,X0),ld(X1,X1))) = ld(ld(ld(X0,X0),ld(ld(X0,X0),X1)),ld(ld(ld(X0,X0),ld(ld(X0,X0),X1)),ld(ld(X0,X0),ld(ld(X0,X0),X1)))),
inference(superposition,[],[f6014,f13131]) ).
fof(f17520,plain,
! [X0,X1] : ld(ld(ld(X0,X0),X1),ld(X0,X0)) = ld(X1,ld(ld(X0,X0),ld(X1,X1))),
inference(forward_demodulation,[],[f17511,f6014]) ).
fof(f17539,plain,
! [X0,X1] : ld(X0,ld(X0,X0)) = ld(ld(ld(X1,X1),X0),ld(ld(X1,X1),ld(ld(ld(X1,X1),X0),ld(ld(X1,X1),X0)))),
inference(backward_demodulation,[],[f13194,f17520]) ).
fof(f17541,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,X0),ld(ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,X0))),ld(X0,X0)),ld(ld(X0,X0),ld(ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,X0))),ld(X0,X0)),ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,X0))),ld(X0,X0)))))),
inference(backward_demodulation,[],[f17363,f17520]) ).
fof(f17802,plain,
! [X0,X1] : ld(ld(ld(ld(X1,X1),ld(ld(X1,X1),X0)),ld(ld(ld(X1,X1),ld(ld(X1,X1),X0)),ld(X1,X1))),ld(X0,ld(ld(X1,X1),ld(X0,X0)))) = X0,
inference(superposition,[],[f3714,f13191]) ).
fof(f17876,plain,
! [X0,X1] : ld(ld(ld(ld(X1,X1),ld(ld(X1,X1),X0)),ld(ld(ld(X1,X1),X0),ld(ld(X1,X1),ld(ld(ld(X1,X1),X0),ld(ld(X1,X1),X0))))),ld(X0,ld(ld(X1,X1),ld(X0,X0)))) = X0,
inference(forward_demodulation,[],[f17802,f17520]) ).
fof(f17948,plain,
! [X0,X1] : ld(ld(ld(ld(X1,X1),ld(ld(X1,X1),X0)),ld(X0,ld(X0,X0))),ld(X0,ld(ld(X1,X1),ld(X0,X0)))) = X0,
inference(forward_demodulation,[],[f17876,f17539]) ).
fof(f19822,plain,
! [X2,X0,X1] : ld(ld(X2,X2),ld(ld(X2,X2),ld(X1,X0))) = ld(ld(X1,X0),ld(ld(ld(X2,X2),ld(ld(X2,X2),ld(X0,X1))),ld(ld(X2,X2),ld(ld(X2,X2),ld(X1,X0))))),
inference(superposition,[],[f13740,f6014]) ).
fof(f19887,plain,
! [X0,X1] : ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))),ld(X1,X1)) = ld(ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(ld(X1,X1),ld(ld(X1,X1),ld(X1,X1))))),ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1)))),ld(ld(X1,X1),ld(ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(ld(X1,X1),ld(ld(X1,X1),ld(X1,X1))))),ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1)))),ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(ld(X1,X1),ld(ld(X1,X1),ld(X1,X1))))),ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))))))),
inference(superposition,[],[f17520,f13740]) ).
fof(f19902,plain,
! [X0,X1] : ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))),ld(X1,X1)) = ld(ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))),ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1)))),ld(ld(X1,X1),ld(ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))),ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1)))),ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))),ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))))))),
inference(forward_demodulation,[],[f19887,f616]) ).
fof(f19948,plain,
! [X0,X1] : ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))),ld(X1,X1)) = ld(ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))),ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1)))),ld(ld(X1,X1),ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))),ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1)))))),
inference(forward_demodulation,[],[f19902,f7181]) ).
fof(f19983,plain,
! [X0,X1] : ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))),ld(X1,X1)) = ld(ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))),ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1)))),ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1)))),
inference(forward_demodulation,[],[f19948,f19822]) ).
fof(f20026,plain,
! [X0,X1] : ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))) = ld(ld(ld(X0,X0),ld(ld(X0,X0),ld(X1,X1))),ld(X1,X1)),
inference(forward_demodulation,[],[f19983,f6114]) ).
fof(f20046,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,X0),ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,X0))),ld(ld(X0,X0),ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,X0))),ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,X0))))))),
inference(backward_demodulation,[],[f17541,f20026]) ).
fof(f20058,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X0,X0),ld(ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,X0))),ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,X0))))),
inference(forward_demodulation,[],[f20046,f19822]) ).
fof(f20064,plain,
! [X0,X1] : ld(X1,X1) = ld(ld(X1,X1),ld(ld(X1,X1),ld(X0,X0))),
inference(forward_demodulation,[],[f20058,f19822]) ).
fof(f20070,plain,
! [X0,X1] : ld(X0,X0) = ld(ld(X0,X0),ld(X1,X1)),
inference(backward_demodulation,[],[f20026,f20064]) ).
fof(f20079,plain,
! [X0,X1] : ld(ld(X1,X1),X0) = ld(ld(X1,X1),ld(ld(X1,X1),X0)),
inference(backward_demodulation,[],[f13131,f20070]) ).
fof(f20099,plain,
! [X0,X1] : ld(ld(ld(ld(X1,X1),ld(ld(X1,X1),X0)),ld(X0,ld(X0,X0))),ld(X0,ld(X1,X1))) = X0,
inference(backward_demodulation,[],[f17948,f20070]) ).
fof(f20125,plain,
! [X2,X0,X1] : ld(ld(X2,X2),ld(X1,X0)) = ld(ld(X2,X2),ld(ld(X2,X2),ld(X1,X0))),
inference(backward_demodulation,[],[f17487,f20070]) ).
fof(f20234,plain,
! [X0,X1] : ld(ld(X1,X1),ld(ld(X1,X1),X0)) = X0,
inference(backward_demodulation,[],[f13191,f20125]) ).
fof(f20312,plain,
! [X0,X1] : ld(ld(ld(ld(X1,X1),X0),ld(X0,ld(X0,X0))),ld(X0,ld(X1,X1))) = X0,
inference(backward_demodulation,[],[f20099,f20079]) ).
fof(f20320,plain,
! [X0] : tuple(x1(ld(X0,X0)),x1_2(ld(X0,X0))) != tuple(ld(ld(X0,X0),x1(ld(X0,X0))),ld(x1_2(ld(X0,X0)),ld(ld(x1_2(ld(X0,X0)),ld(x1_2(ld(X0,X0)),ld(x1_2(ld(X0,X0)),x1_2(ld(X0,X0))))),ld(X0,X0)))),
inference(backward_demodulation,[],[f17474,f20079]) ).
fof(f20339,plain,
! [X0,X1] : ld(ld(X1,X1),X0) = X0,
inference(forward_demodulation,[],[f20234,f20079]) ).
fof(f20471,plain,
! [X0,X1] : ld(ld(X0,ld(X0,ld(X0,X0))),ld(X0,ld(X1,X1))) = X0,
inference(backward_demodulation,[],[f20312,f20339]) ).
fof(f20589,plain,
! [X0] : tuple(x1(ld(X0,X0)),x1_2(ld(X0,X0))) != tuple(x1(ld(X0,X0)),ld(x1_2(ld(X0,X0)),ld(ld(x1_2(ld(X0,X0)),ld(x1_2(ld(X0,X0)),ld(x1_2(ld(X0,X0)),x1_2(ld(X0,X0))))),ld(X0,X0)))),
inference(backward_demodulation,[],[f20320,f20339]) ).
fof(f20711,plain,
! [X0,X1] : ld(X0,ld(ld(X0,ld(X0,ld(X0,X0))),ld(X1,X1))) = X0,
inference(forward_demodulation,[],[f20471,f13781]) ).
fof(f20818,plain,
! [X0] : tuple(x1(ld(X0,X0)),x1_2(ld(X0,X0))) != tuple(x1(ld(X0,X0)),x1_2(ld(X0,X0))),
inference(backward_demodulation,[],[f20589,f20711]) ).
fof(f20819,plain,
$false,
inference(trivial_inequality_removal,[],[f20818]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP655-10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.19/0.43 % Computer : n014.cluster.edu
% 0.19/0.43 % Model : x86_64 x86_64
% 0.19/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.43 % Memory : 8046.5625MB
% 0.19/0.43 % OS : Linux 6.8.0-71-generic
% 0.19/0.43 % CPULimit : 300
% 0.19/0.43 % WCLimit : 300
% 0.19/0.43 % DateTime : Sun Sep 27 10:31:31 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.44 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.49 Running first-order theorem proving
% 0.22/0.49 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
% 121.56/18.28 % (596233)Detected a unit-equality problem, will run specialized UEQ schedule.
% 121.56/18.28 % (596243)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3009040213:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 121.56/18.28 % (596239)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=1037713469:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 121.56/18.28 % (596241)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1584272141:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 121.56/18.28 % (596240)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2062329665:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 121.56/18.28 % (596238)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=2831171497:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 121.56/18.28 % (596242)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2791723655:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 121.56/18.28 % (596244)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2531525994:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 121.56/18.28 % (596241)Instruction limit reached!
% 121.56/18.28 % (596241)------------------------------
% 121.56/18.28 % (596241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.56/18.28 % (596241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.56/18.28 % (596241)CaDiCaL version: 2.1.3
% 121.56/18.28 % (596241)Termination reason: Instruction limit
% 121.56/18.28 % (596241)Termination phase: Saturation
% 121.56/18.28 % (596241)Time elapsed: 0.129 s
% 121.56/18.28 % (596241)Peak memory usage: 88 MB
% 121.56/18.28 % (596241)Instructions burned: 136 (million)
% 121.56/18.28 % (596243)Instruction limit reached!
% 121.56/18.28 % (596243)------------------------------
% 121.56/18.28 % (596243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.56/18.28 % (596243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.56/18.28 % (596243)CaDiCaL version: 2.1.3
% 121.56/18.28 % (596243)Termination reason: Instruction limit
% 121.56/18.28 % (596243)Termination phase: Saturation
% 121.56/18.28 % (596243)Time elapsed: 0.159 s
% 121.56/18.28 % (596243)Peak memory usage: 89 MB
% 121.56/18.28 % (596243)Instructions burned: 259 (million)
% 121.56/18.28 % (596242)Instruction limit reached!
% 121.56/18.28 % (596242)------------------------------
% 121.56/18.28 % (596242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.56/18.28 % (596242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.56/18.28 % (596242)CaDiCaL version: 2.1.3
% 121.56/18.28 % (596242)Termination reason: Instruction limit
% 121.56/18.28 % (596242)Termination phase: Saturation
% 121.56/18.28 % (596242)Time elapsed: 0.178 s
% 121.56/18.28 % (596242)Peak memory usage: 89 MB
% 121.56/18.28 % (596242)Instructions burned: 181 (million)
% 121.56/18.28 % (596254)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2225349096:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 121.56/18.28 % (596252)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2314172986:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 121.56/18.28 % (596254)Instruction limit reached!
% 121.56/18.28 % (596254)------------------------------
% 121.56/18.28 % (596254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.56/18.28 % (596254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.56/18.28 % (596254)CaDiCaL version: 2.1.3
% 121.56/18.28 % (596254)Termination reason: Instruction limit
% 121.56/18.28 % (596254)Termination phase: Saturation
% 121.56/18.28 % (596254)Time elapsed: 0.070 s
% 121.56/18.28 % (596254)Peak memory usage: 90 MB
% 121.56/18.28 % (596254)Instructions burned: 215 (million)
% 121.56/18.28 % (596253)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3570874193:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 154.22/22.81 % (596257)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=797822588:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 154.22/22.81 % (596257)Instruction limit reached!
% 154.22/22.81 % (596257)------------------------------
% 154.22/22.81 % (596257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.22/22.81 % (596257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.22/22.81 % (596257)CaDiCaL version: 2.1.3
% 154.22/22.81 % (596257)Termination reason: Instruction limit
% 154.22/22.81 % (596257)Termination phase: Saturation
% 154.22/22.81 % (596257)Time elapsed: 0.163 s
% 154.22/22.81 % (596257)Peak memory usage: 92 MB
% 154.22/22.81 % (596257)Instructions burned: 317 (million)
% 154.22/22.81 % (596260)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=3581288789:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/12125Mi)
% 154.22/22.81 % (596244)Instruction limit reached!
% 154.22/22.81 % (596244)------------------------------
% 154.22/22.81 % (596244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.22/22.81 % (596244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.22/22.81 % (596244)CaDiCaL version: 2.1.3
% 154.22/22.81 % (596244)Termination reason: Instruction limit
% 154.22/22.81 % (596244)Termination phase: Saturation
% 154.22/22.81 % (596244)Time elapsed: 1.121 s
% 154.22/22.81 % (596244)Peak memory usage: 100 MB
% 154.22/22.81 % (596244)Instructions burned: 1187 (million)
% 154.22/22.81 % (596262)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2897164514:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2985 on theBenchmark for (2985ds/2836Mi)
% 154.22/22.81 % (596252)Instruction limit reached!
% 154.22/22.81 % (596252)------------------------------
% 154.22/22.81 % (596252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.22/22.81 % (596252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.22/22.81 % (596252)CaDiCaL version: 2.1.3
% 154.22/22.81 % (596252)Termination reason: Instruction limit
% 154.22/22.81 % (596252)Termination phase: Saturation
% 154.22/22.81 % (596252)Time elapsed: 2.210 s
% 154.22/22.81 % (596252)Peak memory usage: 141 MB
% 154.22/22.81 % (596252)Instructions burned: 2052 (million)
% 154.22/22.81 % (596264)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=119502949:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2971 on theBenchmark for (2971ds/14534Mi)
% 154.22/22.81 % (596262)Instruction limit reached!
% 154.22/22.81 % (596262)------------------------------
% 154.22/22.81 % (596262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.22/22.81 % (596262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.22/22.81 % (596262)CaDiCaL version: 2.1.3
% 154.22/22.81 % (596262)Termination reason: Instruction limit
% 154.22/22.81 % (596262)Termination phase: Saturation
% 154.22/22.81 % (596262)Time elapsed: 3.027 s
% 154.22/22.81 % (596262)Peak memory usage: 138 MB
% 154.22/22.81 % (596262)Instructions burned: 2836 (million)
% 154.22/22.81 % (596269)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=1772709821:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2952 on theBenchmark for (2952ds/11832Mi)
% 154.22/22.81 % (596253)Instruction limit reached!
% 154.22/22.81 % (596253)------------------------------
% 154.22/22.81 % (596253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.22/22.81 % (596253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.22/22.81 % (596253)CaDiCaL version: 2.1.3
% 154.22/22.81 % (596253)Termination reason: Instruction limit
% 154.22/22.81 % (596253)Termination phase: Saturation
% 154.22/22.81 % (596253)Time elapsed: 5.175 s
% 154.22/22.81 % (596253)Peak memory usage: 165 MB
% 154.22/22.81 % (596253)Instructions burned: 4948 (million)
% 154.22/22.81 % (596271)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=372673628:i=2279:fgj=on:bd=all_2941 on theBenchmark for (2941ds/2279Mi)
% 154.22/22.81 % (596260)Instruction limit reached!
% 154.22/22.81 % (596260)------------------------------
% 154.22/22.81 % (596260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596260)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596260)Termination reason: Instruction limit
% 95.67/30.46 % (596260)Termination phase: Saturation
% 95.67/30.46 % (596260)Time elapsed: 6.614 s
% 95.67/30.46 % (596260)Peak memory usage: 232 MB
% 95.67/30.46 % (596260)Instructions burned: 12126 (million)
% 95.67/30.46 % (596273)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=540147554:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2921 on theBenchmark for (2921ds/6225Mi)
% 95.67/30.46 % (596271)Instruction limit reached!
% 95.67/30.46 % (596271)------------------------------
% 95.67/30.46 % (596271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596271)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596271)Termination reason: Instruction limit
% 95.67/30.46 % (596271)Termination phase: Saturation
% 95.67/30.46 % (596271)Time elapsed: 2.292 s
% 95.67/30.46 % (596271)Peak memory usage: 138 MB
% 95.67/30.46 % (596271)Instructions burned: 2279 (million)
% 95.67/30.46 % (596275)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=4289993667:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2916 on theBenchmark for (2916ds/21755Mi)
% 95.67/30.46 % (596273)Instruction limit reached!
% 95.67/30.46 % (596273)------------------------------
% 95.67/30.46 % (596273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596273)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596273)Termination reason: Instruction limit
% 95.67/30.46 % (596273)Termination phase: Saturation
% 95.67/30.46 % (596273)Time elapsed: 2.576 s
% 95.67/30.46 % (596273)Peak memory usage: 165 MB
% 95.67/30.46 % (596273)Instructions burned: 6226 (million)
% 95.67/30.46 % (596277)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=274406782:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2893 on theBenchmark for (2893ds/16427Mi)
% 95.67/30.46 % (596269)Instruction limit reached!
% 95.67/30.46 % (596269)------------------------------
% 95.67/30.46 % (596269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596269)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596269)Termination reason: Instruction limit
% 95.67/30.46 % (596269)Termination phase: Saturation
% 95.67/30.46 % (596269)Time elapsed: 10.300 s
% 95.67/30.46 % (596269)Peak memory usage: 224 MB
% 95.67/30.46 % (596269)Instructions burned: 11833 (million)
% 95.67/30.46 % (596436)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=193286868:i=9356:fgj=on:bd=preordered:av=off_2846 on theBenchmark for (2846ds/9356Mi)
% 95.67/30.46 % (596264)Instruction limit reached!
% 95.67/30.46 % (596264)------------------------------
% 95.67/30.46 % (596264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596264)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596264)Termination reason: Instruction limit
% 95.67/30.46 % (596264)Termination phase: Saturation
% 95.67/30.46 % (596264)Time elapsed: 12.712 s
% 95.67/30.46 % (596264)Peak memory usage: 247 MB
% 95.67/30.46 % (596264)Instructions burned: 14534 (million)
% 95.67/30.46 % (596438)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=2055674853:i=2070:kws=inv_precedence:slsql=off:bd=all_2841 on theBenchmark for (2841ds/2070Mi)
% 95.67/30.46 % (596277)Instruction limit reached!
% 95.67/30.46 % (596277)------------------------------
% 95.67/30.46 % (596277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596277)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596277)Termination reason: Instruction limit
% 95.67/30.46 % (596277)Termination phase: Saturation
% 95.67/30.46 % (596277)Time elapsed: 6.012 s
% 95.67/30.46 % (596277)Peak memory usage: 254 MB
% 95.67/30.46 % (596277)Instructions burned: 16429 (million)
% 95.67/30.46 % (596440)lrs+1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=8000:tgt=ground:npcc=on:fde=unused:sp=const_min:urr=ec_only:s2agt=32:random_seed=2699818207:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2830 on theBenchmark for (2830ds/6461Mi)
% 95.67/30.46 % (596438)Instruction limit reached!
% 95.67/30.46 % (596438)------------------------------
% 95.67/30.46 % (596438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596438)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596438)Termination reason: Instruction limit
% 95.67/30.46 % (596438)Termination phase: Saturation
% 95.67/30.46 % (596438)Time elapsed: 1.253 s
% 95.67/30.46 % (596438)Peak memory usage: 124 MB
% 95.67/30.46 % (596438)Instructions burned: 2071 (million)
% 95.67/30.46 % (596442)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=3065606737:i=2310:bd=all:ss=included_2827 on theBenchmark for (2827ds/2310Mi)
% 95.67/30.46 % (596442)Instruction limit reached!
% 95.67/30.46 % (596442)------------------------------
% 95.67/30.46 % (596442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596442)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596442)Termination reason: Instruction limit
% 95.67/30.46 % (596442)Termination phase: Saturation
% 95.67/30.46 % (596442)Time elapsed: 1.137 s
% 95.67/30.46 % (596442)Peak memory usage: 109 MB
% 95.67/30.46 % (596442)Instructions burned: 2312 (million)
% 95.67/30.46 % (596444)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=2824423218:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2813 on theBenchmark for (2813ds/2616Mi)
% 95.67/30.46 % (596440)Instruction limit reached!
% 95.67/30.46 % (596440)------------------------------
% 95.67/30.46 % (596440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596440)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596440)Termination reason: Instruction limit
% 95.67/30.46 % (596440)Termination phase: Saturation
% 95.67/30.46 % (596440)Time elapsed: 1.817 s
% 95.67/30.46 % (596440)Peak memory usage: 199 MB
% 95.67/30.46 % (596440)Instructions burned: 6465 (million)
% 95.67/30.46 % (596446)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=51628796:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2810 on theBenchmark for (2810ds/30521Mi)
% 95.67/30.46 % (596436)Instruction limit reached!
% 95.67/30.46 % (596436)------------------------------
% 95.67/30.46 % (596436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596436)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596436)Termination reason: Instruction limit
% 95.67/30.46 % (596436)Termination phase: Saturation
% 95.67/30.46 % (596436)Time elapsed: 3.990 s
% 95.67/30.46 % (596436)Peak memory usage: 228 MB
% 95.67/30.46 % (596436)Instructions burned: 9358 (million)
% 95.67/30.46 % (596448)lrs+11_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:tgt=full:npcc=on:prc=on:fde=unused:sp=reverse_frequency:spb=goal:acc=on:urr=ec_only:s2agt=32:random_seed=1821918623:i=3258:fgj=on:bd=all:ins=1_2804 on theBenchmark for (2804ds/3258Mi)
% 95.67/30.46 % (596444)Instruction limit reached!
% 95.67/30.46 % (596444)------------------------------
% 95.67/30.46 % (596444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596444)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596444)Termination reason: Instruction limit
% 95.67/30.46 % (596444)Termination phase: Saturation
% 95.67/30.46 % (596444)Time elapsed: 1.585 s
% 95.67/30.46 % (596444)Peak memory usage: 122 MB
% 95.67/30.46 % (596444)Instructions burned: 2616 (million)
% 95.67/30.46 % (596450)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=2110160541:i=5037:kws=precedence_2796 on theBenchmark for (2796ds/5037Mi)
% 95.67/30.46 % (596448)Instruction limit reached!
% 95.67/30.46 % (596448)------------------------------
% 95.67/30.46 % (596448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596448)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596448)Termination reason: Instruction limit
% 95.67/30.46 % (596448)Termination phase: Saturation
% 95.67/30.46 % (596448)Time elapsed: 1.896 s
% 95.67/30.46 % (596448)Peak memory usage: 159 MB
% 95.67/30.46 % (596448)Instructions burned: 3259 (million)
% 95.67/30.46 % (596452)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=3522979400:i=65240_2783 on theBenchmark for (2783ds/65240Mi)
% 95.67/30.46 % (596450)Instruction limit reached!
% 95.67/30.46 % (596450)------------------------------
% 95.67/30.46 % (596450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596450)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596450)Termination reason: Instruction limit
% 95.67/30.46 % (596450)Termination phase: Saturation
% 95.67/30.46 % (596450)Time elapsed: 3.057 s
% 95.67/30.46 % (596450)Peak memory usage: 167 MB
% 95.67/30.46 % (596450)Instructions burned: 5037 (million)
% 95.67/30.46 % (596454)lrs-1011_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:urr=ec_only:random_seed=427418855:i=16502:kws=inv_precedence:fgj=on:bd=preordered:ins=3:av=off_2764 on theBenchmark for (2764ds/16502Mi)
% 95.67/30.46 % (596275)Instruction limit reached!
% 95.67/30.46 % (596275)------------------------------
% 95.67/30.46 % (596275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.67/30.46 % (596275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.67/30.46 % (596275)CaDiCaL version: 2.1.3
% 95.67/30.46 % (596275)Termination reason: Instruction limit
% 95.67/30.46 % (596275)Termination phase: Saturation
% 95.67/30.46 % (596275)Time elapsed: 16.381 s
% 95.67/30.46 % (596275)Peak memory usage: 258 MB
% 95.67/30.46 % (596275)Instructions burned: 21755 (million)
% 95.67/30.46 % (596456)lrs-1011_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=32000:npcc=on:drc=off:sp=const_max:spb=goal_then_units:urr=ec_only:fd=preordered:random_seed=806455442:i=7623:bd=preordered:er=filter_2749 on theBenchmark for (2749ds/7623Mi)
% 95.67/30.46 % (596456)First to succeed.
% 95.67/30.46 % (596456)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-596233"
% 95.67/30.46 % (596456)Refutation found. Thanks to Tanya!
% 95.67/30.46 % SZS status Unsatisfiable for theBenchmark
% 95.67/30.46 % SZS output start Proof for theBenchmark
% See solution above
% 208.63/30.65 % (596456)------------------------------
% 208.63/30.65 % (596456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 208.63/30.65 % (596456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.63/30.65 % (596456)CaDiCaL version: 2.1.3
% 208.63/30.65 % (596456)Termination reason: Refutation
% 208.63/30.65 % (596456)Time elapsed: 3.667 s
% 208.63/30.65 % (596456)Peak memory usage: 162 MB
% 208.63/30.65 % (596456)Instructions burned: 6186 (million)
% 208.63/30.65 % (596456)------------------------------
% 208.63/30.65 % (596456)------------------------------
% 208.63/30.65 % (596233)Success in time 29.267 s
% 208.63/30.65 % Vampire exiting
%------------------------------------------------------------------------------