%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KLE120+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:58:00 PM UTC 2026
% Result : Theorem 98.49s 13.00s
% Output : CNFRefutation 98.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 19
% Syntax : Number of formulae : 134 ( 134 unt; 0 def)
% Number of atoms : 134 ( 133 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 9 ( 9 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-2 aty)
% Number of variables : 153 ( 152 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] : addition(A,B) = addition(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [C,B,A] : addition(A,addition(B,C)) = addition(addition(A,B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] : addition(A,zero) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] : addition(A,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B,C] : multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] : multiplication(A,one) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] : multiplication(one,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X0] : c(X0) = antidomain(domain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,conjecture,
! [X0] : addition(backward_diamond(one,domain(X0)),domain(X0)) = domain(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,negated_conjecture,
~ ! [X0] : addition(backward_diamond(one,domain(X0)),domain(X0)) = domain(X0),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f29,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f30,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(addition(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f31,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f32,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f33,plain,
! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f34,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f35,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f36,plain,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f37,plain,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f44,plain,
! [X0] : multiplication(antidomain(X0),X0) = zero,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f46,plain,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f47,plain,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f48,plain,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f49,plain,
! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f50,plain,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f51,plain,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f52,plain,
! [X0] : c(X0) = antidomain(domain(X0)),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f55,plain,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f58,plain,
? [X0] : addition(backward_diamond(one,domain(X0)),domain(X0)) != domain(X0),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f59,plain,
addition(backward_diamond(one,domain(sK0_skl)),domain(sK0_skl)) != domain(sK0_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f58]) ).
fof(f60,plain,
addition(backward_diamond(one,domain(sK0_skl)),domain(sK0_skl)) != domain(sK0_skl),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f65,plain,
! [X0] : X0 = addition(zero,X0),
inference(paramodulation,[status(thm)],[f31,f29]) ).
fof(f82,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)),
inference(paramodulation,[status(thm)],[f29,f30]) ).
fof(f90,plain,
! [X0,X1] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(paramodulation,[status(thm)],[f32,f30]) ).
fof(f106,plain,
antidomain(one) = zero,
inference(paramodulation,[status(thm)],[f34,f44]) ).
fof(f109,plain,
! [X0] : domain(antidomain(X0)) = antidomain(domain(X0)),
inference(paramodulation,[status(thm)],[f47,f47]) ).
fof(f159,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X0,X1)) = addition(zero,multiplication(antidomain(X0),X1)),
inference(paramodulation,[status(thm)],[f44,f36]) ).
fof(f163,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(paramodulation,[status(thm)],[f34,f36]) ).
fof(f181,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X0,X1)) = multiplication(antidomain(X0),X1),
inference(forward_demodulation,[status(thm)],[f65,f159]) ).
fof(f196,plain,
! [X0] : domain(antidomain(X0)) = c(X0),
inference(forward_demodulation,[status(thm)],[f52,f109]) ).
fof(f208,plain,
! [X0,X1] : addition(X0,addition(X1,X0)) = addition(X0,X1),
inference(paramodulation,[status(thm)],[f29,f90]) ).
fof(f279,plain,
! [X0,X1] : multiplication(addition(X0,antidomain(X1)),X1) = addition(multiplication(X0,X1),zero),
inference(paramodulation,[status(thm)],[f44,f37]) ).
fof(f301,plain,
! [X0,X1] : multiplication(addition(X0,antidomain(X1)),X1) = multiplication(X0,X1),
inference(forward_demodulation,[status(thm)],[f31,f279]) ).
fof(f313,plain,
! [X0] : addition(domain(X0),antidomain(X0)) = one,
inference(forward_demodulation,[status(thm)],[f47,f46]) ).
fof(f314,plain,
! [X0] : addition(antidomain(X0),domain(X0)) = one,
inference(paramodulation,[status(thm)],[f29,f313]) ).
fof(f320,plain,
! [X0] : addition(domain(X0),one) = addition(domain(X0),antidomain(X0)),
inference(paramodulation,[status(thm)],[f313,f90]) ).
fof(f328,plain,
! [X0] : addition(domain(X0),one) = one,
inference(forward_demodulation,[status(thm)],[f313,f320]) ).
fof(f414,plain,
! [X0,X1] : multiplication(X0,multiplication(X1,coantidomain(multiplication(X0,X1)))) = zero,
inference(paramodulation,[status(thm)],[f33,f48]) ).
fof(f416,plain,
coantidomain(one) = zero,
inference(paramodulation,[status(thm)],[f35,f48]) ).
fof(f421,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = addition(multiplication(X0,coantidomain(X1)),zero),
inference(paramodulation,[status(thm)],[f48,f37]) ).
fof(f423,plain,
! [X0,X1] : multiplication(X0,addition(X1,coantidomain(X0))) = addition(multiplication(X0,X1),zero),
inference(paramodulation,[status(thm)],[f48,f36]) ).
fof(f426,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = multiplication(X0,coantidomain(X1)),
inference(forward_demodulation,[status(thm)],[f31,f421]) ).
fof(f428,plain,
! [X0,X1] : multiplication(X0,addition(X1,coantidomain(X0))) = multiplication(X0,X1),
inference(forward_demodulation,[status(thm)],[f31,f423]) ).
fof(f441,plain,
! [X0] : addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(antidomain(X0))),X0))) = coantidomain(multiplication(coantidomain(coantidomain(antidomain(X0))),X0)),
inference(paramodulation,[status(thm)],[f44,f49]) ).
fof(f478,plain,
! [X0] : addition(coantidomain(X0),coantidomain(coantidomain(X0))) = one,
inference(paramodulation,[status(thm)],[f29,f50]) ).
fof(f480,plain,
! [X0] : addition(coantidomain(X0),one) = addition(coantidomain(X0),coantidomain(coantidomain(X0))),
inference(paramodulation,[status(thm)],[f50,f208]) ).
fof(f496,plain,
! [X0] : addition(codomain(X0),coantidomain(X0)) = one,
inference(backward_demodulation,[status(thm)],[f51,f50]) ).
fof(f616,plain,
! [X0] : backward_diamond(one,X0) = codomain(codomain(X0)),
inference(paramodulation,[status(thm)],[f34,f55]) ).
fof(f711,plain,
addition(codomain(codomain(domain(sK0_skl))),domain(sK0_skl)) != domain(sK0_skl),
inference(forward_demodulation,[status(thm)],[f616,f60]) ).
fof(f712,plain,
addition(domain(sK0_skl),codomain(codomain(domain(sK0_skl)))) != domain(sK0_skl),
inference(paramodulation,[status(thm)],[f29,f711]) ).
fof(f743,plain,
! [X0] : addition(coantidomain(X0),codomain(X0)) = one,
inference(forward_demodulation,[status(thm)],[f51,f478]) ).
fof(f872,plain,
! [X0,X1] : addition(X0,one) = addition(antidomain(X1),addition(X0,domain(X1))),
inference(paramodulation,[status(thm)],[f313,f82]) ).
fof(f1367,plain,
addition(domain(one),zero) = one,
inference(paramodulation,[status(thm)],[f106,f313]) ).
fof(f1369,plain,
domain(one) = antidomain(zero),
inference(paramodulation,[status(thm)],[f106,f47]) ).
fof(f1374,plain,
domain(one) = one,
inference(forward_demodulation,[status(thm)],[f31,f1367]) ).
fof(f1391,plain,
one = antidomain(zero),
inference(forward_demodulation,[status(thm)],[f1374,f1369]) ).
fof(f2199,plain,
! [X0] : multiplication(antidomain(coantidomain(X0)),one) = multiplication(antidomain(coantidomain(X0)),codomain(X0)),
inference(paramodulation,[status(thm)],[f743,f181]) ).
fof(f2216,plain,
! [X0] : multiplication(antidomain(domain(X0)),one) = multiplication(antidomain(domain(X0)),antidomain(X0)),
inference(paramodulation,[status(thm)],[f313,f181]) ).
fof(f2251,plain,
! [X0] : antidomain(coantidomain(X0)) = multiplication(antidomain(coantidomain(X0)),codomain(X0)),
inference(forward_demodulation,[status(thm)],[f34,f2199]) ).
fof(f2274,plain,
! [X0] : antidomain(domain(X0)) = multiplication(antidomain(domain(X0)),antidomain(X0)),
inference(forward_demodulation,[status(thm)],[f34,f2216]) ).
fof(f2275,plain,
! [X0] : c(X0) = multiplication(antidomain(domain(X0)),antidomain(X0)),
inference(forward_demodulation,[status(thm)],[f52,f2274]) ).
fof(f2276,plain,
! [X0] : c(X0) = multiplication(c(X0),antidomain(X0)),
inference(forward_demodulation,[status(thm)],[f52,f2275]) ).
fof(f2359,plain,
! [X0,X1] : multiplication(X0,addition(X1,one)) = addition(X0,multiplication(X0,X1)),
inference(paramodulation,[status(thm)],[f29,f163]) ).
fof(f5267,plain,
! [X0] : multiplication(one,X0) = multiplication(domain(X0),X0),
inference(paramodulation,[status(thm)],[f313,f301]) ).
fof(f5321,plain,
! [X0] : X0 = multiplication(domain(X0),X0),
inference(forward_demodulation,[status(thm)],[f35,f5267]) ).
fof(f5366,plain,
! [X0] : antidomain(X0) = multiplication(c(X0),antidomain(X0)),
inference(paramodulation,[status(thm)],[f196,f5321]) ).
fof(f5400,plain,
! [X0] : antidomain(X0) = c(X0),
inference(forward_demodulation,[status(thm)],[f2276,f5366]) ).
fof(f5432,plain,
! [X0] : domain(antidomain(X0)) = antidomain(X0),
inference(backward_demodulation,[status(thm)],[f5400,f196]) ).
fof(f5433,plain,
! [X0] : antidomain(X0) = antidomain(domain(X0)),
inference(backward_demodulation,[status(thm)],[f5400,f52]) ).
fof(f10533,plain,
codomain(one) = coantidomain(zero),
inference(paramodulation,[status(thm)],[f416,f51]) ).
fof(f10548,plain,
antidomain(coantidomain(one)) = multiplication(antidomain(coantidomain(one)),coantidomain(zero)),
inference(paramodulation,[status(thm)],[f10533,f2251]) ).
fof(f10591,plain,
antidomain(zero) = multiplication(antidomain(coantidomain(one)),coantidomain(zero)),
inference(forward_demodulation,[status(thm)],[f416,f10548]) ).
fof(f10592,plain,
one = multiplication(antidomain(coantidomain(one)),coantidomain(zero)),
inference(forward_demodulation,[status(thm)],[f1391,f10591]) ).
fof(f10593,plain,
one = multiplication(antidomain(zero),coantidomain(zero)),
inference(forward_demodulation,[status(thm)],[f416,f10592]) ).
fof(f10594,plain,
one = multiplication(one,coantidomain(zero)),
inference(forward_demodulation,[status(thm)],[f1391,f10593]) ).
fof(f10595,plain,
one = coantidomain(zero),
inference(forward_demodulation,[status(thm)],[f35,f10594]) ).
fof(f10900,plain,
! [X0] : multiplication(one,coantidomain(domain(X0))) = multiplication(antidomain(X0),coantidomain(domain(X0))),
inference(paramodulation,[status(thm)],[f314,f426]) ).
fof(f11044,plain,
! [X0] : coantidomain(domain(X0)) = multiplication(antidomain(X0),coantidomain(domain(X0))),
inference(forward_demodulation,[status(thm)],[f35,f10900]) ).
fof(f13362,plain,
! [X0] : addition(one,coantidomain(multiplication(coantidomain(coantidomain(antidomain(X0))),X0))) = coantidomain(multiplication(coantidomain(coantidomain(antidomain(X0))),X0)),
inference(forward_demodulation,[status(thm)],[f10595,f441]) ).
fof(f13363,plain,
! [X0] : addition(one,coantidomain(multiplication(codomain(antidomain(X0)),X0))) = coantidomain(multiplication(coantidomain(coantidomain(antidomain(X0))),X0)),
inference(forward_demodulation,[status(thm)],[f51,f13362]) ).
fof(f13364,plain,
! [X0] : addition(one,coantidomain(multiplication(codomain(antidomain(X0)),X0))) = coantidomain(multiplication(codomain(antidomain(X0)),X0)),
inference(forward_demodulation,[status(thm)],[f51,f13363]) ).
fof(f13386,plain,
! [X0] : multiplication(multiplication(codomain(antidomain(X0)),X0),coantidomain(multiplication(codomain(antidomain(X0)),X0))) = multiplication(multiplication(codomain(antidomain(X0)),X0),one),
inference(paramodulation,[status(thm)],[f13364,f428]) ).
fof(f13434,plain,
! [X0] : multiplication(codomain(antidomain(X0)),multiplication(X0,coantidomain(multiplication(codomain(antidomain(X0)),X0)))) = multiplication(multiplication(codomain(antidomain(X0)),X0),one),
inference(forward_demodulation,[status(thm)],[f33,f13386]) ).
fof(f13435,plain,
! [X0] : zero = multiplication(multiplication(codomain(antidomain(X0)),X0),one),
inference(forward_demodulation,[status(thm)],[f414,f13434]) ).
fof(f13436,plain,
! [X0] : zero = multiplication(codomain(antidomain(X0)),multiplication(X0,one)),
inference(forward_demodulation,[status(thm)],[f33,f13435]) ).
fof(f13437,plain,
! [X0] : zero = multiplication(codomain(antidomain(X0)),X0),
inference(forward_demodulation,[status(thm)],[f34,f13436]) ).
fof(f13515,plain,
! [X0,X1] : multiplication(addition(codomain(antidomain(X0)),X1),X0) = addition(zero,multiplication(X1,X0)),
inference(paramodulation,[status(thm)],[f13437,f37]) ).
fof(f13601,plain,
! [X0,X1] : multiplication(addition(codomain(antidomain(X0)),X1),X0) = multiplication(X1,X0),
inference(forward_demodulation,[status(thm)],[f65,f13515]) ).
fof(f14045,plain,
! [X0] : multiplication(one,X0) = multiplication(coantidomain(antidomain(X0)),X0),
inference(paramodulation,[status(thm)],[f496,f13601]) ).
fof(f14147,plain,
! [X0] : X0 = multiplication(coantidomain(antidomain(X0)),X0),
inference(forward_demodulation,[status(thm)],[f35,f14045]) ).
fof(f14226,plain,
! [X0] : domain(X0) = multiplication(coantidomain(antidomain(X0)),domain(X0)),
inference(paramodulation,[status(thm)],[f5433,f14147]) ).
fof(f14785,plain,
! [X0] : multiplication(coantidomain(antidomain(X0)),addition(domain(X0),one)) = addition(coantidomain(antidomain(X0)),domain(X0)),
inference(paramodulation,[status(thm)],[f14226,f2359]) ).
fof(f14856,plain,
! [X0] : multiplication(coantidomain(antidomain(X0)),one) = addition(coantidomain(antidomain(X0)),domain(X0)),
inference(forward_demodulation,[status(thm)],[f328,f14785]) ).
fof(f14857,plain,
! [X0] : coantidomain(antidomain(X0)) = addition(coantidomain(antidomain(X0)),domain(X0)),
inference(forward_demodulation,[status(thm)],[f34,f14856]) ).
fof(f27482,plain,
! [X0] : addition(coantidomain(X0),one) = addition(coantidomain(X0),codomain(X0)),
inference(forward_demodulation,[status(thm)],[f51,f480]) ).
fof(f27486,plain,
! [X0] : addition(coantidomain(X0),one) = one,
inference(forward_demodulation,[status(thm)],[f743,f27482]) ).
fof(f58580,plain,
! [X0] : addition(coantidomain(antidomain(X0)),one) = addition(antidomain(X0),coantidomain(antidomain(X0))),
inference(paramodulation,[status(thm)],[f14857,f872]) ).
fof(f58682,plain,
! [X0] : one = addition(antidomain(X0),coantidomain(antidomain(X0))),
inference(forward_demodulation,[status(thm)],[f27486,f58580]) ).
fof(f58806,plain,
! [X0] : multiplication(antidomain(antidomain(X0)),one) = multiplication(antidomain(antidomain(X0)),coantidomain(antidomain(X0))),
inference(paramodulation,[status(thm)],[f58682,f181]) ).
fof(f58882,plain,
! [X0] : antidomain(antidomain(X0)) = multiplication(antidomain(antidomain(X0)),coantidomain(antidomain(X0))),
inference(forward_demodulation,[status(thm)],[f34,f58806]) ).
fof(f58883,plain,
! [X0] : domain(X0) = multiplication(antidomain(antidomain(X0)),coantidomain(antidomain(X0))),
inference(forward_demodulation,[status(thm)],[f47,f58882]) ).
fof(f58884,plain,
! [X0] : domain(X0) = multiplication(domain(X0),coantidomain(antidomain(X0))),
inference(forward_demodulation,[status(thm)],[f47,f58883]) ).
fof(f59987,plain,
! [X0] : domain(antidomain(X0)) = multiplication(antidomain(X0),coantidomain(antidomain(antidomain(X0)))),
inference(paramodulation,[status(thm)],[f5432,f58884]) ).
fof(f60072,plain,
! [X0] : antidomain(X0) = multiplication(antidomain(X0),coantidomain(antidomain(antidomain(X0)))),
inference(forward_demodulation,[status(thm)],[f5432,f59987]) ).
fof(f60073,plain,
! [X0] : antidomain(X0) = multiplication(antidomain(X0),coantidomain(domain(X0))),
inference(forward_demodulation,[status(thm)],[f47,f60072]) ).
fof(f60074,plain,
! [X0] : antidomain(X0) = coantidomain(domain(X0)),
inference(forward_demodulation,[status(thm)],[f11044,f60073]) ).
fof(f60143,plain,
! [X0] : antidomain(antidomain(X0)) = coantidomain(antidomain(X0)),
inference(paramodulation,[status(thm)],[f5432,f60074]) ).
fof(f60195,plain,
! [X0] : codomain(domain(X0)) = coantidomain(antidomain(X0)),
inference(paramodulation,[status(thm)],[f60074,f51]) ).
fof(f60205,plain,
! [X0] : domain(X0) = coantidomain(antidomain(X0)),
inference(forward_demodulation,[status(thm)],[f47,f60143]) ).
fof(f61095,plain,
addition(domain(sK0_skl),codomain(domain(sK0_skl))) != domain(sK0_skl),
inference(backward_demodulation,[status(thm)],[f61099,f712]) ).
fof(f61099,plain,
! [X0] : codomain(domain(X0)) = domain(X0),
inference(forward_demodulation,[status(thm)],[f60205,f60195]) ).
fof(f61237,plain,
addition(domain(sK0_skl),domain(sK0_skl)) != domain(sK0_skl),
inference(forward_demodulation,[status(thm)],[f61099,f61095]) ).
fof(f61238,plain,
domain(sK0_skl) != domain(sK0_skl),
inference(forward_demodulation,[status(thm)],[f32,f61237]) ).
fof(f61239,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f61238]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE120+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n019.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 22:45:08 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 98.49/13.00 % Refutation found
% 98.49/13.00 % SZS status Theorem for theBenchmark: Theorem is valid
% 98.49/13.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 28.77/13.25 % Elapsed time: 12.869259 seconds
% 28.77/13.25 % CPU time: 101.064098 seconds
% 28.77/13.25 % Total memory used: 607.839 MB
% 28.77/13.25 % Net memory used: 583.893 MB
%------------------------------------------------------------------------------