%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP660+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 : Thu Sep 24 12:35:03 PM UTC 2026
% Result : Theorem 184.71s 29.01s
% Output : CNFRefutation 157.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 6
% Syntax : Number of formulae : 151 ( 144 unt; 0 def)
% Number of atoms : 158 ( 157 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 20 ( 13 ~; 5 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 294 ( 288 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [B,A] : mult(A,ld(A,B)) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [B,A] : ld(A,mult(A,B)) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [B,A] : mult(rd(A,B),B) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [B,A] : rd(mult(A,B),B) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [C,B,A] : mult(mult(mult(A,B),C),A) = mult(A,mult(B,mult(C,A))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,conjecture,
! [X0,X1] :
( mult(rd(X1,X1),X0) = X0
& mult(X0,rd(X1,X1)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,negated_conjecture,
~ ! [X0,X1] :
( mult(rd(X1,X1),X0) = X0
& mult(X0,rd(X1,X1)) = X0 ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f9,plain,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f10,plain,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f11,plain,
! [X0,X1] : X0 = rd(mult(X0,X1),X1),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f12,plain,
! [X0,X1,X2] : mult(mult(mult(X0,X1),X2),X0) = mult(X0,mult(X1,mult(X2,X0))),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f13,plain,
? [X0,X1] :
( mult(rd(X1,X1),X0) != X0
| mult(X0,rd(X1,X1)) != X0 ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f14,plain,
( ? [X0,X1] : mult(rd(X1,X1),X0) != X0
| ? [X0,X1] : mult(X0,rd(X1,X1)) != X0 ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f15,plain,
( mult(rd(sK3_skl,sK3_skl),sK2_skl) != sK2_skl
| mult(sK0_skl,rd(sK1_skl,sK1_skl)) != sK0_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl),skolemize(X0,sK2_skl),skolemize(X1,sK3_skl)],[f14]) ).
fof(f16,plain,
( mult(sK0_skl,rd(sK1_skl,sK1_skl)) != sK0_skl
| sK2_skl != mult(rd(sK3_skl,sK3_skl),sK2_skl) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f19,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(paramodulation,[status(thm)],[f10,f9]) ).
fof(f21,plain,
! [X0,X1] : X0 = rd(X1,ld(X0,X1)),
inference(paramodulation,[status(thm)],[f8,f11]) ).
fof(f30,plain,
! [X0,X1,X2] : mult(X0,X1) = mult(X1,mult(X2,mult(ld(mult(X1,X2),X0),X1))),
inference(paramodulation,[status(thm)],[f8,f12]) ).
fof(f33,plain,
! [X0,X1,X2] : mult(X0,mult(ld(X0,X1),mult(X2,X0))) = mult(mult(X1,X2),X0),
inference(paramodulation,[status(thm)],[f8,f12]) ).
fof(f34,plain,
! [X0,X1,X2] : mult(mult(X0,X1),X2) = rd(mult(X0,mult(X1,mult(X2,X0))),X0),
inference(paramodulation,[status(thm)],[f12,f11]) ).
fof(f52,plain,
! [X0,X1,X2] : rd(mult(X0,X1),X0) = mult(mult(X0,rd(X1,mult(X2,X0))),X2),
inference(paramodulation,[status(thm)],[f10,f34]) ).
fof(f54,plain,
! [X0,X1,X2] : mult(mult(X0,X1),rd(X2,X0)) = rd(mult(X0,mult(X1,X2)),X0),
inference(paramodulation,[status(thm)],[f10,f34]) ).
fof(f67,plain,
! [X0,X1,X2] : mult(mult(X0,rd(X1,X2)),X2) = mult(X2,mult(ld(X2,X0),X1)),
inference(paramodulation,[status(thm)],[f10,f33]) ).
fof(f78,plain,
! [X0,X1,X2] : ld(X0,mult(mult(X1,X2),X0)) = mult(ld(X0,X1),mult(X2,X0)),
inference(paramodulation,[status(thm)],[f33,f9]) ).
fof(f100,plain,
! [X0,X1,X2] : mult(X0,mult(ld(mult(X1,X0),X2),X1)) = ld(X1,mult(X2,X1)),
inference(paramodulation,[status(thm)],[f30,f9]) ).
fof(f147,plain,
! [X0,X1,X2] : rd(mult(X0,X1),X0) = mult(mult(X0,rd(X1,X2)),rd(X2,X0)),
inference(paramodulation,[status(thm)],[f10,f54]) ).
fof(f149,plain,
! [X0,X1,X2] : rd(mult(X0,X1),X0) = mult(mult(X0,X2),rd(ld(X2,X1),X0)),
inference(paramodulation,[status(thm)],[f8,f54]) ).
fof(f186,plain,
! [X0,X1,X2] : rd(rd(mult(X0,X1),X0),X2) = mult(X0,rd(X1,mult(X2,X0))),
inference(paramodulation,[status(thm)],[f52,f11]) ).
fof(f289,plain,
! [X0,X1,X2] : mult(X0,X1) = mult(X1,mult(ld(X1,rd(X0,rd(X2,X1))),X2)),
inference(paramodulation,[status(thm)],[f10,f67]) ).
fof(f326,plain,
! [X0,X1] : mult(X0,X1) = mult(ld(mult(X0,X1),X0),mult(X1,mult(X0,X1))),
inference(paramodulation,[status(thm)],[f9,f78]) ).
fof(f337,plain,
! [X0,X1,X2] : mult(ld(X0,rd(X1,X2)),mult(X2,X0)) = ld(X0,mult(X1,X0)),
inference(paramodulation,[status(thm)],[f10,f78]) ).
fof(f339,plain,
! [X0,X1,X2] : mult(ld(X0,X1),mult(ld(X1,X2),X0)) = ld(X0,mult(X2,X0)),
inference(paramodulation,[status(thm)],[f8,f78]) ).
fof(f481,plain,
! [X0,X1,X2] : mult(X0,mult(ld(X1,X2),rd(X1,X0))) = ld(rd(X1,X0),mult(X2,rd(X1,X0))),
inference(paramodulation,[status(thm)],[f10,f100]) ).
fof(f514,plain,
! [X0,X1,X2] : mult(ld(mult(X0,X1),X2),X0) = ld(X1,ld(X0,mult(X2,X0))),
inference(paramodulation,[status(thm)],[f100,f9]) ).
fof(f715,plain,
! [X0,X1,X2] : mult(X0,rd(ld(ld(X1,X0),X2),X1)) = rd(mult(X1,X2),X1),
inference(paramodulation,[status(thm)],[f8,f149]) ).
fof(f1024,plain,
! [X0,X1] : rd(X0,X1) = mult(X0,rd(X0,mult(X1,X0))),
inference(paramodulation,[status(thm)],[f11,f186]) ).
fof(f1037,plain,
! [X0,X1,X2] : mult(X0,rd(ld(X0,X1),mult(X2,X0))) = rd(rd(X1,X0),X2),
inference(paramodulation,[status(thm)],[f8,f186]) ).
fof(f1079,plain,
! [X0,X1] : mult(X0,rd(X0,X1)) = rd(X0,rd(X1,X0)),
inference(paramodulation,[status(thm)],[f10,f1024]) ).
fof(f1083,plain,
! [X0,X1] : mult(ld(X0,X1),rd(ld(X0,X1),X1)) = rd(ld(X0,X1),X0),
inference(paramodulation,[status(thm)],[f8,f1024]) ).
fof(f1116,plain,
! [X0,X1] : rd(rd(X0,X1),rd(X0,mult(X1,X0))) = X0,
inference(paramodulation,[status(thm)],[f1024,f11]) ).
fof(f1117,plain,
! [X0,X1] : ld(X0,rd(X0,X1)) = rd(X0,mult(X1,X0)),
inference(paramodulation,[status(thm)],[f1024,f9]) ).
fof(f1198,plain,
! [X0,X1] : rd(X0,mult(ld(X1,X0),X0)) = ld(X0,X1),
inference(paramodulation,[status(thm)],[f21,f1117]) ).
fof(f1233,plain,
! [X0,X1] : rd(X0,X1) = ld(mult(X1,rd(X1,X0)),X1),
inference(paramodulation,[status(thm)],[f1079,f19]) ).
fof(f1266,plain,
! [X0,X1,X2] : mult(mult(mult(ld(X0,X1),X1),rd(X2,X1)),ld(X1,X0)) = rd(mult(mult(ld(X0,X1),X1),X2),mult(ld(X0,X1),X1)),
inference(paramodulation,[status(thm)],[f1198,f147]) ).
fof(f1273,plain,
! [X0,X1] : ld(ld(X0,X1),X0) = mult(ld(X1,X0),X0),
inference(paramodulation,[status(thm)],[f1198,f19]) ).
fof(f1611,plain,
! [X0,X1] : rd(ld(X0,X1),X1) = ld(mult(X1,X0),X1),
inference(paramodulation,[status(thm)],[f21,f1233]) ).
fof(f1628,plain,
! [X0,X1] : mult(X0,X1) = mult(rd(ld(X1,X0),X0),mult(X1,mult(X0,X1))),
inference(backward_demodulation,[status(thm)],[f1611,f326]) ).
fof(f1780,plain,
! [X0,X1,X2] : mult(ld(X0,rd(X1,rd(X2,X0))),X2) = ld(X0,mult(X1,X0)),
inference(paramodulation,[status(thm)],[f289,f9]) ).
fof(f2084,plain,
! [X0,X1,X2] : ld(ld(X0,X1),mult(X2,ld(X0,X1))) = mult(ld(ld(X0,X1),rd(X2,X0)),X1),
inference(paramodulation,[status(thm)],[f8,f337]) ).
fof(f2122,plain,
! [X0,X1,X2] : rd(ld(X0,mult(X1,X0)),mult(X2,X0)) = ld(X0,rd(X1,X2)),
inference(paramodulation,[status(thm)],[f337,f11]) ).
fof(f2414,plain,
! [X0,X1,X2] : mult(ld(mult(X0,X1),rd(X2,X0)),X0) = ld(X1,ld(X0,X2)),
inference(paramodulation,[status(thm)],[f10,f514]) ).
fof(f2996,plain,
! [X0,X1,X2] : ld(X0,rd(mult(X1,X2),X1)) = rd(ld(ld(X1,X0),X2),X1),
inference(paramodulation,[status(thm)],[f715,f9]) ).
fof(f3115,plain,
! [X0,X1,X2] : rd(rd(X0,X1),rd(X2,X1)) = mult(X1,rd(ld(X1,X0),X2)),
inference(paramodulation,[status(thm)],[f10,f1037]) ).
fof(f3172,plain,
! [X0,X1,X2] : rd(ld(X0,X1),mult(X2,X0)) = ld(X0,rd(rd(X1,X0),X2)),
inference(paramodulation,[status(thm)],[f1037,f9]) ).
fof(f3795,plain,
! [X0,X1] : rd(mult(X0,X1),mult(X1,mult(X0,X1))) = rd(ld(X1,X0),X0),
inference(paramodulation,[status(thm)],[f1628,f11]) ).
fof(f4440,plain,
! [X0,X1,X2] : ld(X0,rd(X1,rd(X2,X0))) = rd(ld(X0,mult(X1,X0)),X2),
inference(paramodulation,[status(thm)],[f1780,f11]) ).
fof(f4731,plain,
! [X0,X1,X2] : mult(ld(X0,rd(X1,X2)),X2) = ld(ld(X2,X0),ld(X2,X1)),
inference(paramodulation,[status(thm)],[f8,f2414]) ).
fof(f5123,plain,
! [X0,X1] : rd(ld(ld(X0,mult(X0,X1)),X1),X0) = rd(mult(X0,X1),mult(X0,mult(X0,X1))),
inference(paramodulation,[status(thm)],[f2996,f1117]) ).
fof(f5175,plain,
! [X0,X1] : rd(ld(X0,X0),X1) = rd(mult(X1,X0),mult(X1,mult(X1,X0))),
inference(forward_demodulation,[status(thm)],[f9,f5123]) ).
fof(f5235,plain,
! [X0,X1] : rd(ld(X0,X1),mult(rd(X1,mult(X0,X1)),X0)) = ld(X0,X1),
inference(paramodulation,[status(thm)],[f1116,f3172]) ).
fof(f5239,plain,
! [X0,X1,X2] : ld(X0,X1) = rd(ld(X0,X2),mult(ld(X1,rd(X2,X0)),X0)),
inference(paramodulation,[status(thm)],[f21,f3172]) ).
fof(f6913,plain,
! [X0] : rd(ld(X0,X0),ld(X0,X0)) = rd(mult(ld(X0,X0),X0),ld(X0,mult(X0,X0))),
inference(paramodulation,[status(thm)],[f339,f5175]) ).
fof(f7002,plain,
! [X0] : rd(ld(X0,X0),ld(X0,X0)) = rd(mult(ld(X0,X0),X0),X0),
inference(forward_demodulation,[status(thm)],[f9,f6913]) ).
fof(f7003,plain,
! [X0] : rd(ld(X0,X0),ld(X0,X0)) = ld(X0,X0),
inference(forward_demodulation,[status(thm)],[f11,f7002]) ).
fof(f7316,plain,
! [X0,X1] : ld(ld(X0,X0),rd(X1,ld(X0,X0))) = rd(ld(ld(X0,X0),mult(X1,ld(X0,X0))),ld(X0,X0)),
inference(paramodulation,[status(thm)],[f7003,f4440]) ).
fof(f7327,plain,
! [X0] : mult(ld(X0,X0),rd(ld(X0,X0),ld(X0,X0))) = rd(ld(X0,X0),ld(X0,X0)),
inference(paramodulation,[status(thm)],[f7003,f1079]) ).
fof(f7335,plain,
! [X0,X1] : mult(mult(X0,ld(X1,X1)),ld(X1,X1)) = mult(ld(X1,X1),mult(ld(ld(X1,X1),X0),ld(X1,X1))),
inference(paramodulation,[status(thm)],[f7003,f67]) ).
fof(f7337,plain,
! [X0] : ld(ld(X0,X0),ld(X0,X0)) = ld(X0,X0),
inference(paramodulation,[status(thm)],[f7003,f19]) ).
fof(f7353,plain,
! [X0,X1] : ld(ld(X0,X0),rd(X1,ld(X0,X0))) = rd(mult(ld(ld(X0,X0),rd(X1,X0)),X0),ld(X0,X0)),
inference(forward_demodulation,[status(thm)],[f2084,f7316]) ).
fof(f7361,plain,
! [X0] : mult(ld(X0,X0),ld(X0,X0)) = rd(ld(X0,X0),ld(X0,X0)),
inference(forward_demodulation,[status(thm)],[f7003,f7327]) ).
fof(f7363,plain,
! [X0] : ld(X0,X0) = mult(ld(X0,X0),ld(X0,X0)),
inference(forward_demodulation,[status(thm)],[f7003,f7361]) ).
fof(f7375,plain,
! [X0] : mult(ld(X0,rd(X0,X0)),X0) = ld(X0,X0),
inference(forward_demodulation,[status(thm)],[f4731,f7337]) ).
fof(f7379,plain,
! [X0] : mult(rd(X0,mult(X0,X0)),X0) = ld(X0,X0),
inference(forward_demodulation,[status(thm)],[f1117,f7375]) ).
fof(f7440,plain,
! [X0] : mult(ld(ld(X0,X0),X0),ld(X0,X0)) = ld(ld(X0,X0),mult(X0,ld(X0,X0))),
inference(paramodulation,[status(thm)],[f7363,f339]) ).
fof(f7482,plain,
! [X0,X1] : mult(ld(X0,X0),mult(ld(ld(X0,X0),X1),ld(X0,X0))) = ld(ld(X0,X0),mult(X1,ld(X0,X0))),
inference(paramodulation,[status(thm)],[f7363,f100]) ).
fof(f7544,plain,
! [X0,X1] : mult(mult(X0,ld(X1,X1)),ld(X1,X1)) = ld(ld(X1,X1),mult(X0,ld(X1,X1))),
inference(forward_demodulation,[status(thm)],[f7335,f7482]) ).
fof(f7546,plain,
! [X0,X1] : ld(ld(X0,X0),rd(X1,ld(X0,X0))) = rd(mult(mult(X1,ld(X0,X0)),ld(X0,X0)),ld(X0,X0)),
inference(backward_demodulation,[status(thm)],[f7547,f7353]) ).
fof(f7547,plain,
! [X0,X1] : mult(ld(ld(X0,X0),rd(X1,X0)),X0) = mult(mult(X1,ld(X0,X0)),ld(X0,X0)),
inference(forward_demodulation,[status(thm)],[f2084,f7544]) ).
fof(f7602,plain,
! [X0,X1] : mult(X0,ld(X1,X1)) = ld(ld(X1,X1),rd(X0,ld(X1,X1))),
inference(forward_demodulation,[status(thm)],[f11,f7546]) ).
fof(f7704,plain,
! [X0] : mult(mult(ld(X0,X0),X0),ld(X0,X0)) = ld(ld(X0,X0),mult(X0,ld(X0,X0))),
inference(forward_demodulation,[status(thm)],[f1273,f7440]) ).
fof(f7705,plain,
! [X0] : mult(mult(ld(X0,X0),X0),ld(X0,X0)) = mult(ld(ld(X0,X0),rd(X0,X0)),X0),
inference(forward_demodulation,[status(thm)],[f2084,f7704]) ).
fof(f7706,plain,
! [X0] : mult(mult(ld(X0,X0),X0),ld(X0,X0)) = mult(mult(X0,ld(X0,X0)),ld(X0,X0)),
inference(forward_demodulation,[status(thm)],[f7547,f7705]) ).
fof(f7707,plain,
! [X0] : mult(mult(ld(X0,X0),X0),ld(X0,X0)) = mult(X0,ld(X0,X0)),
inference(forward_demodulation,[status(thm)],[f8,f7706]) ).
fof(f7708,plain,
! [X0] : X0 = mult(mult(ld(X0,X0),X0),ld(X0,X0)),
inference(forward_demodulation,[status(thm)],[f8,f7707]) ).
fof(f7781,plain,
! [X0] : rd(ld(X0,X0),X0) = rd(X0,mult(X0,X0)),
inference(paramodulation,[status(thm)],[f7379,f11]) ).
fof(f7910,plain,
! [X0] : rd(mult(mult(ld(X0,X0),X0),ld(X0,X0)),mult(ld(X0,X0),X0)) = rd(ld(ld(X0,X0),mult(ld(X0,X0),X0)),mult(ld(X0,X0),X0)),
inference(paramodulation,[status(thm)],[f7708,f3795]) ).
fof(f7935,plain,
! [X0,X1] : rd(rd(X0,mult(ld(X0,X0),X0)),X1) = mult(mult(ld(X0,X0),X0),rd(ld(X0,X0),mult(X1,mult(ld(X0,X0),X0)))),
inference(paramodulation,[status(thm)],[f7708,f186]) ).
fof(f7938,plain,
! [X0,X1] : rd(mult(mult(ld(X0,X0),X0),X1),mult(ld(X0,X0),X0)) = mult(X0,rd(ld(ld(X0,X0),X1),mult(ld(X0,X0),X0))),
inference(paramodulation,[status(thm)],[f7708,f149]) ).
fof(f7955,plain,
! [X0] : mult(ld(X0,X0),X0) = rd(X0,ld(X0,X0)),
inference(paramodulation,[status(thm)],[f7708,f11]) ).
fof(f8060,plain,
! [X0] : mult(ld(X0,X0),X0) = X0,
inference(forward_demodulation,[status(thm)],[f21,f7955]) ).
fof(f8127,plain,
! [X0,X1] : rd(ld(X0,X0),X1) = mult(mult(ld(X0,X0),X0),rd(ld(X0,X0),mult(X1,mult(ld(X0,X0),X0)))),
inference(forward_demodulation,[status(thm)],[f1198,f7935]) ).
fof(f8128,plain,
! [X0,X1] : rd(ld(X0,X0),X1) = mult(X0,rd(ld(X0,X0),mult(X1,mult(ld(X0,X0),X0)))),
inference(forward_demodulation,[status(thm)],[f8060,f8127]) ).
fof(f8129,plain,
! [X0,X1] : rd(ld(X0,X0),X1) = mult(X0,rd(ld(X0,X0),mult(X1,X0))),
inference(forward_demodulation,[status(thm)],[f8060,f8128]) ).
fof(f8164,plain,
! [X0] : rd(rd(X0,X0),X0) = rd(X0,mult(X0,X0)),
inference(backward_demodulation,[status(thm)],[f8187,f7781]) ).
fof(f8187,plain,
! [X0,X1] : rd(rd(X0,X0),X1) = rd(ld(X0,X0),X1),
inference(forward_demodulation,[status(thm)],[f1037,f8129]) ).
fof(f8214,plain,
! [X0,X1] : mult(mult(mult(ld(X0,X0),X0),rd(X1,X0)),ld(X0,X0)) = mult(X0,rd(ld(ld(X0,X0),X1),mult(ld(X0,X0),X0))),
inference(forward_demodulation,[status(thm)],[f1266,f7938]) ).
fof(f8215,plain,
! [X0,X1] : mult(ld(X0,X0),mult(X0,mult(rd(X1,X0),ld(X0,X0)))) = mult(X0,rd(ld(ld(X0,X0),X1),mult(ld(X0,X0),X0))),
inference(forward_demodulation,[status(thm)],[f12,f8214]) ).
fof(f8216,plain,
! [X0,X1] : mult(ld(X0,X0),mult(X0,mult(rd(X1,X0),ld(X0,X0)))) = mult(X0,rd(ld(ld(X0,X0),X1),X0)),
inference(forward_demodulation,[status(thm)],[f8060,f8215]) ).
fof(f8217,plain,
! [X0,X1] : mult(ld(X0,X0),mult(X0,mult(rd(X1,X0),ld(X0,X0)))) = rd(mult(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f715,f8216]) ).
fof(f8261,plain,
! [X0] : mult(mult(mult(ld(X0,X0),X0),rd(ld(X0,X0),X0)),ld(X0,X0)) = rd(ld(ld(X0,X0),mult(ld(X0,X0),X0)),mult(ld(X0,X0),X0)),
inference(forward_demodulation,[status(thm)],[f1266,f7910]) ).
fof(f8262,plain,
! [X0] : mult(ld(X0,X0),mult(X0,mult(rd(ld(X0,X0),X0),ld(X0,X0)))) = rd(ld(ld(X0,X0),mult(ld(X0,X0),X0)),mult(ld(X0,X0),X0)),
inference(forward_demodulation,[status(thm)],[f12,f8261]) ).
fof(f8263,plain,
! [X0] : rd(mult(X0,ld(X0,X0)),X0) = rd(ld(ld(X0,X0),mult(ld(X0,X0),X0)),mult(ld(X0,X0),X0)),
inference(forward_demodulation,[status(thm)],[f8217,f8262]) ).
fof(f8264,plain,
! [X0] : rd(X0,X0) = rd(ld(ld(X0,X0),mult(ld(X0,X0),X0)),mult(ld(X0,X0),X0)),
inference(forward_demodulation,[status(thm)],[f8,f8263]) ).
fof(f8265,plain,
! [X0] : rd(X0,X0) = rd(X0,mult(ld(X0,X0),X0)),
inference(forward_demodulation,[status(thm)],[f9,f8264]) ).
fof(f8267,plain,
! [X0] : ld(X0,X0) = mult(ld(X0,X0),rd(X0,X0)),
inference(backward_demodulation,[status(thm)],[f8330,f7363]) ).
fof(f8320,plain,
! [X0,X1] : mult(X0,ld(X1,X1)) = ld(ld(X1,X1),rd(X0,rd(X1,X1))),
inference(backward_demodulation,[status(thm)],[f8330,f7602]) ).
fof(f8330,plain,
! [X0] : rd(X0,X0) = ld(X0,X0),
inference(forward_demodulation,[status(thm)],[f1198,f8265]) ).
fof(f8412,plain,
! [X0] : rd(X0,X0) = mult(ld(X0,X0),rd(X0,X0)),
inference(forward_demodulation,[status(thm)],[f8330,f8267]) ).
fof(f8413,plain,
! [X0] : rd(X0,X0) = mult(rd(X0,X0),rd(X0,X0)),
inference(forward_demodulation,[status(thm)],[f8330,f8412]) ).
fof(f8427,plain,
! [X0,X1] : mult(X0,rd(X1,X1)) = ld(ld(X1,X1),rd(X0,rd(X1,X1))),
inference(forward_demodulation,[status(thm)],[f8330,f8320]) ).
fof(f8428,plain,
! [X0,X1] : ld(rd(X0,X0),rd(X1,rd(X0,X0))) = mult(X1,rd(X0,X0)),
inference(forward_demodulation,[status(thm)],[f8330,f8427]) ).
fof(f8498,plain,
! [X0,X1] : rd(ld(X0,X1),ld(X0,X1)) = mult(ld(X1,rd(X1,X0)),X0),
inference(paramodulation,[status(thm)],[f4731,f8330]) ).
fof(f8545,plain,
! [X0,X1] : mult(rd(X0,mult(X1,X0)),X1) = rd(ld(X1,X0),ld(X1,X0)),
inference(forward_demodulation,[status(thm)],[f1117,f8498]) ).
fof(f11242,plain,
! [X0,X1] : rd(ld(rd(X0,X0),mult(X1,rd(X0,X0))),rd(X0,X0)) = ld(rd(X0,X0),rd(X1,rd(X0,X0))),
inference(paramodulation,[status(thm)],[f8413,f2122]) ).
fof(f11253,plain,
! [X0,X1] : mult(ld(rd(X0,X0),rd(X1,rd(X0,X0))),rd(X0,X0)) = ld(rd(X0,X0),mult(X1,rd(X0,X0))),
inference(paramodulation,[status(thm)],[f8413,f337]) ).
fof(f11287,plain,
! [X0,X1] : mult(mult(X0,rd(X1,X1)),rd(X1,X1)) = ld(rd(X1,X1),mult(X0,rd(X1,X1))),
inference(forward_demodulation,[status(thm)],[f8428,f11253]) ).
fof(f11290,plain,
! [X0,X1] : mult(mult(X0,rd(X1,X1)),rd(X1,X1)) = mult(X1,mult(ld(X1,X0),rd(X1,X1))),
inference(forward_demodulation,[status(thm)],[f481,f11287]) ).
fof(f11291,plain,
! [X0,X1] : rd(mult(X0,mult(ld(X0,X1),rd(X0,X0))),rd(X0,X0)) = ld(rd(X0,X0),rd(X1,rd(X0,X0))),
inference(forward_demodulation,[status(thm)],[f481,f11242]) ).
fof(f11292,plain,
! [X0,X1] : mult(X0,rd(X1,X1)) = rd(mult(X1,mult(ld(X1,X0),rd(X1,X1))),rd(X1,X1)),
inference(forward_demodulation,[status(thm)],[f8428,f11291]) ).
fof(f17504,plain,
! [X0,X1] : ld(rd(X0,X0),X1) = mult(mult(X1,rd(X0,X0)),rd(X0,X0)),
inference(paramodulation,[status(thm)],[f11,f8428]) ).
fof(f17512,plain,
! [X0,X1] : ld(rd(X0,X0),rd(X0,X0)) = rd(ld(rd(X0,X0),X1),mult(mult(X1,rd(X0,X0)),rd(X0,X0))),
inference(paramodulation,[status(thm)],[f8428,f5239]) ).
fof(f17519,plain,
! [X0,X1] : rd(mult(X0,rd(X1,X1)),mult(rd(rd(X0,rd(X1,X1)),mult(rd(X1,X1),rd(X0,rd(X1,X1)))),rd(X1,X1))) = ld(rd(X1,X1),rd(X0,rd(X1,X1))),
inference(paramodulation,[status(thm)],[f8428,f5235]) ).
fof(f17538,plain,
! [X0,X1] : mult(ld(rd(X0,X0),rd(X1,rd(X0,X0))),rd(mult(X1,rd(X0,X0)),rd(X1,rd(X0,X0)))) = rd(ld(rd(X0,X0),rd(X1,rd(X0,X0))),rd(X0,X0)),
inference(paramodulation,[status(thm)],[f8428,f1083]) ).
fof(f17551,plain,
! [X0,X1] : rd(X0,rd(X1,X1)) = mult(rd(X1,X1),mult(X0,rd(X1,X1))),
inference(paramodulation,[status(thm)],[f8428,f8]) ).
fof(f17569,plain,
! [X0,X1] : rd(ld(rd(X0,X0),X1),rd(X0,X0)) = mult(X1,rd(X0,X0)),
inference(backward_demodulation,[status(thm)],[f17574,f11292]) ).
fof(f17574,plain,
! [X0,X1] : mult(X0,mult(ld(X0,X1),rd(X0,X0))) = ld(rd(X0,X0),X1),
inference(forward_demodulation,[status(thm)],[f11290,f17504]) ).
fof(f17584,plain,
! [X0,X1] : rd(rd(X0,X0),rd(X0,X0)) = rd(ld(rd(X0,X0),X1),mult(mult(X1,rd(X0,X0)),rd(X0,X0))),
inference(forward_demodulation,[status(thm)],[f8330,f17512]) ).
fof(f17585,plain,
! [X0,X1] : mult(X0,rd(ld(X0,X0),X0)) = rd(ld(rd(X0,X0),X1),mult(mult(X1,rd(X0,X0)),rd(X0,X0))),
inference(forward_demodulation,[status(thm)],[f3115,f17584]) ).
fof(f17586,plain,
! [X0,X1] : mult(X0,rd(rd(X0,X0),X0)) = rd(ld(rd(X0,X0),X1),mult(mult(X1,rd(X0,X0)),rd(X0,X0))),
inference(forward_demodulation,[status(thm)],[f8330,f17585]) ).
fof(f17587,plain,
! [X0,X1] : mult(X0,rd(X0,mult(X0,X0))) = rd(ld(rd(X0,X0),X1),mult(mult(X1,rd(X0,X0)),rd(X0,X0))),
inference(forward_demodulation,[status(thm)],[f8164,f17586]) ).
fof(f17588,plain,
! [X0,X1] : rd(X0,X0) = rd(ld(rd(X0,X0),X1),mult(mult(X1,rd(X0,X0)),rd(X0,X0))),
inference(forward_demodulation,[status(thm)],[f1024,f17587]) ).
fof(f17589,plain,
! [X0,X1] : rd(X0,X0) = rd(ld(rd(X0,X0),X1),mult(X0,mult(ld(X0,X1),rd(X0,X0)))),
inference(forward_demodulation,[status(thm)],[f11290,f17588]) ).
fof(f17590,plain,
! [X0,X1] : rd(X0,X0) = rd(ld(rd(X0,X0),X1),ld(rd(X0,X0),X1)),
inference(forward_demodulation,[status(thm)],[f17574,f17589]) ).
fof(f17591,plain,
! [X0,X1] : mult(rd(X0,mult(rd(X1,X1),X0)),rd(X1,X1)) = rd(X1,X1),
inference(forward_demodulation,[status(thm)],[f8545,f17590]) ).
fof(f17637,plain,
! [X0,X1] : rd(mult(X0,rd(X1,X1)),rd(X1,X1)) = ld(rd(X1,X1),rd(X0,rd(X1,X1))),
inference(forward_demodulation,[status(thm)],[f17591,f17519]) ).
fof(f17638,plain,
! [X0,X1] : X0 = ld(rd(X1,X1),rd(X0,rd(X1,X1))),
inference(forward_demodulation,[status(thm)],[f11,f17637]) ).
fof(f17640,plain,
( sK0_skl != sK0_skl
| sK2_skl != mult(rd(sK3_skl,sK3_skl),sK2_skl) ),
inference(backward_demodulation,[status(thm)],[f17757,f16]) ).
fof(f17730,plain,
! [X0,X1] : mult(rd(X0,X0),X1) = rd(X1,rd(X0,X0)),
inference(backward_demodulation,[status(thm)],[f17757,f17551]) ).
fof(f17757,plain,
! [X0,X1] : mult(X0,rd(X1,X1)) = X0,
inference(forward_demodulation,[status(thm)],[f8428,f17638]) ).
fof(f17829,plain,
! [X0,X1] : mult(mult(X0,rd(X1,X1)),rd(mult(X0,rd(X1,X1)),rd(X0,rd(X1,X1)))) = rd(ld(rd(X1,X1),rd(X0,rd(X1,X1))),rd(X1,X1)),
inference(forward_demodulation,[status(thm)],[f8428,f17538]) ).
fof(f17830,plain,
! [X0,X1] : mult(X0,rd(mult(X0,rd(X1,X1)),rd(X0,rd(X1,X1)))) = rd(ld(rd(X1,X1),rd(X0,rd(X1,X1))),rd(X1,X1)),
inference(forward_demodulation,[status(thm)],[f17757,f17829]) ).
fof(f17831,plain,
! [X0,X1] : mult(X0,rd(X0,rd(X0,rd(X1,X1)))) = rd(ld(rd(X1,X1),rd(X0,rd(X1,X1))),rd(X1,X1)),
inference(forward_demodulation,[status(thm)],[f17757,f17830]) ).
fof(f17832,plain,
! [X0,X1] : mult(X0,rd(X0,rd(X0,rd(X1,X1)))) = mult(rd(X0,rd(X1,X1)),rd(X1,X1)),
inference(forward_demodulation,[status(thm)],[f17569,f17831]) ).
fof(f17833,plain,
! [X0,X1] : mult(X0,rd(X0,rd(X0,rd(X1,X1)))) = X0,
inference(forward_demodulation,[status(thm)],[f10,f17832]) ).
fof(f17847,plain,
! [X0,X1] : mult(X0,rd(X0,mult(rd(X1,X1),X0))) = X0,
inference(backward_demodulation,[status(thm)],[f17730,f17833]) ).
fof(f17917,plain,
sK2_skl != mult(rd(sK3_skl,sK3_skl),sK2_skl),
inference(trivial_equality_resolution,[status(thm)],[f17640]) ).
fof(f17952,plain,
! [X0,X1] : rd(X0,rd(X1,X1)) = X0,
inference(forward_demodulation,[status(thm)],[f1024,f17847]) ).
fof(f17954,plain,
sK2_skl != sK2_skl,
inference(backward_demodulation,[status(thm)],[f18018,f17917]) ).
fof(f18018,plain,
! [X0,X1] : mult(rd(X0,X0),X1) = X1,
inference(forward_demodulation,[status(thm)],[f17730,f17952]) ).
fof(f18744,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f17954]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP660+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.58 % Computer : n018.cluster.edu
% 0.09/5.58 % Model : x86_64 x86_64
% 0.09/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.58 % Memory : 8046.5625MB
% 0.09/5.58 % OS : Linux 6.8.0-71-generic
% 0.09/5.58 % CPULimit : 300
% 0.09/5.58 % WCLimit : 300
% 0.09/5.58 % DateTime : Sun Sep 20 20:32:20 UTC 2026
% 0.09/5.58 % CPUTime :
% 0.09/5.59 % Drodi V4.1.1
% 184.71/29.01 % Refutation found
% 184.71/29.01 % SZS status Theorem for theBenchmark: Theorem is valid
% 184.71/29.01 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 35.00/29.39 % Elapsed time: 23.785491 seconds
% 35.00/29.39 % CPU time: 187.972417 seconds
% 35.00/29.39 % Total memory used: 2.187 GB
% 35.00/29.39 % Net memory used: 2.177 GB
%------------------------------------------------------------------------------