%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KLE135+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 : n012.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:01 PM UTC 2026
% Result : Theorem 1.17s 0.57s
% Output : CNFRefutation 1.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 17
% Syntax : Number of formulae : 111 ( 86 unt; 0 def)
% Number of atoms : 136 ( 135 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 52 ( 27 ~; 20 |; 2 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-2 aty)
% Number of variables : 150 ( 149 !; 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(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(f21,axiom,
! [X0] : c(X0) = antidomain(domain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X0,X1] : domain_difference(X0,X1) = multiplication(domain(X0),antidomain(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [X0,X1,X2] :
( addition(domain(X0),addition(forward_diamond(X1,domain(X0)),domain(X2))) = addition(forward_diamond(X1,domain(X0)),domain(X2))
=> addition(domain(X0),addition(divergence(X1),forward_diamond(star(X1),domain(X2)))) = addition(divergence(X1),forward_diamond(star(X1),domain(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,conjecture,
! [X0] :
( divergence(X0) = zero
=> forward_diamond(star(X0),antidomain(X0)) = one ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
~ ! [X0] :
( divergence(X0) = zero
=> forward_diamond(star(X0),antidomain(X0)) = one ),
inference(negated_conjecture,[status(cth)],[f29]) ).
fof(f31,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f32,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(addition(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f33,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f34,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f36,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f37,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f38,plain,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f39,plain,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f46,plain,
! [X0] : multiplication(antidomain(X0),X0) = zero,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f48,plain,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f49,plain,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f54,plain,
! [X0] : c(X0) = antidomain(domain(X0)),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f55,plain,
! [X0,X1] : domain_difference(X0,X1) = multiplication(domain(X0),antidomain(X1)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f56,plain,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f58,plain,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f61,plain,
! [X0,X1,X2] :
( addition(domain(X0),addition(divergence(X1),forward_diamond(star(X1),domain(X2)))) = addition(divergence(X1),forward_diamond(star(X1),domain(X2)))
| addition(domain(X0),addition(forward_diamond(X1,domain(X0)),domain(X2))) != addition(forward_diamond(X1,domain(X0)),domain(X2)) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f62,plain,
! [X0,X1,X2] :
( addition(domain(X0),addition(divergence(X1),forward_diamond(star(X1),domain(X2)))) = addition(divergence(X1),forward_diamond(star(X1),domain(X2)))
| addition(domain(X0),addition(forward_diamond(X1,domain(X0)),domain(X2))) != addition(forward_diamond(X1,domain(X0)),domain(X2)) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
? [X0] :
( forward_diamond(star(X0),antidomain(X0)) != one
& divergence(X0) = zero ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f64,plain,
( forward_diamond(star(sK0_skl),antidomain(sK0_skl)) != one
& divergence(sK0_skl) = zero ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f63]) ).
fof(f65,plain,
divergence(sK0_skl) = zero,
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
forward_diamond(star(sK0_skl),antidomain(sK0_skl)) != one,
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f67,plain,
! [X0] : addition(domain(X0),antidomain(X0)) = one,
inference(backward_demodulation,[status(thm)],[f49,f48]) ).
fof(f82,plain,
antidomain(one) = zero,
inference(paramodulation,[status(thm)],[f36,f46]) ).
fof(f93,plain,
addition(domain(one),zero) = one,
inference(paramodulation,[status(thm)],[f82,f67]) ).
fof(f94,plain,
domain(one) = one,
inference(forward_demodulation,[status(thm)],[f33,f93]) ).
fof(f105,plain,
! [X0] : forward_diamond(X0,one) = domain(multiplication(X0,one)),
inference(paramodulation,[status(thm)],[f94,f56]) ).
fof(f108,plain,
! [X0] : forward_diamond(X0,one) = domain(X0),
inference(forward_demodulation,[status(thm)],[f36,f105]) ).
fof(f111,plain,
! [X0,X1] :
( addition(domain(X0),addition(zero,forward_diamond(star(sK0_skl),domain(X1)))) = addition(divergence(sK0_skl),forward_diamond(star(sK0_skl),domain(X1)))
| addition(domain(X0),addition(forward_diamond(sK0_skl,domain(X0)),domain(X1))) != addition(forward_diamond(sK0_skl,domain(X0)),domain(X1)) ),
inference(paramodulation,[status(thm)],[f65,f62]) ).
fof(f122,plain,
! [X0,X1] :
( addition(domain(X0),addition(zero,forward_diamond(star(sK0_skl),domain(X1)))) = addition(zero,forward_diamond(star(sK0_skl),domain(X1)))
| addition(domain(X0),addition(forward_diamond(sK0_skl,domain(X0)),domain(X1))) != addition(forward_diamond(sK0_skl,domain(X0)),domain(X1)) ),
inference(forward_demodulation,[status(thm)],[f65,f111]) ).
fof(f136,plain,
! [X0] : one = addition(antidomain(X0),domain(X0)),
inference(paramodulation,[status(thm)],[f67,f31]) ).
fof(f137,plain,
! [X0] : X0 = addition(zero,X0),
inference(paramodulation,[status(thm)],[f33,f31]) ).
fof(f153,plain,
! [X0,X1] :
( addition(domain(X0),addition(zero,forward_diamond(star(sK0_skl),domain(X1)))) = forward_diamond(star(sK0_skl),domain(X1))
| addition(domain(X0),addition(forward_diamond(sK0_skl,domain(X0)),domain(X1))) != addition(forward_diamond(sK0_skl,domain(X0)),domain(X1)) ),
inference(backward_demodulation,[status(thm)],[f137,f122]) ).
fof(f156,plain,
! [X0,X1] :
( addition(domain(X0),forward_diamond(star(sK0_skl),domain(X1))) = forward_diamond(star(sK0_skl),domain(X1))
| addition(domain(X0),addition(forward_diamond(sK0_skl,domain(X0)),domain(X1))) != addition(forward_diamond(sK0_skl,domain(X0)),domain(X1)) ),
inference(forward_demodulation,[status(thm)],[f137,f153]) ).
fof(f165,plain,
! [X0] : domain(antidomain(X0)) = antidomain(domain(X0)),
inference(paramodulation,[status(thm)],[f49,f49]) ).
fof(f169,plain,
! [X0] : domain(antidomain(X0)) = c(X0),
inference(forward_demodulation,[status(thm)],[f54,f165]) ).
fof(f219,plain,
! [X0,X1] : c(multiplication(X0,domain(X1))) = antidomain(forward_diamond(X0,X1)),
inference(paramodulation,[status(thm)],[f56,f54]) ).
fof(f271,plain,
! [X0,X1] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(paramodulation,[status(thm)],[f34,f32]) ).
fof(f307,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X0,X1)) = addition(zero,multiplication(antidomain(X0),X1)),
inference(paramodulation,[status(thm)],[f46,f38]) ).
fof(f329,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X0,X1)) = multiplication(antidomain(X0),X1),
inference(forward_demodulation,[status(thm)],[f137,f307]) ).
fof(f351,plain,
! [X0] :
( addition(one,forward_diamond(star(sK0_skl),domain(X0))) = forward_diamond(star(sK0_skl),domain(X0))
| addition(domain(one),addition(forward_diamond(sK0_skl,domain(one)),domain(X0))) != addition(forward_diamond(sK0_skl,domain(one)),domain(X0)) ),
inference(paramodulation,[status(thm)],[f94,f156]) ).
fof(f370,plain,
! [X0] :
( addition(one,forward_diamond(star(sK0_skl),domain(X0))) = forward_diamond(star(sK0_skl),domain(X0))
| addition(one,addition(forward_diamond(sK0_skl,domain(one)),domain(X0))) != addition(forward_diamond(sK0_skl,domain(one)),domain(X0)) ),
inference(forward_demodulation,[status(thm)],[f94,f351]) ).
fof(f371,plain,
! [X0] :
( addition(one,forward_diamond(star(sK0_skl),domain(X0))) = forward_diamond(star(sK0_skl),domain(X0))
| addition(one,addition(forward_diamond(sK0_skl,one),domain(X0))) != addition(forward_diamond(sK0_skl,domain(one)),domain(X0)) ),
inference(forward_demodulation,[status(thm)],[f94,f370]) ).
fof(f372,plain,
! [X0] :
( addition(one,forward_diamond(star(sK0_skl),domain(X0))) = forward_diamond(star(sK0_skl),domain(X0))
| addition(one,addition(domain(sK0_skl),domain(X0))) != addition(forward_diamond(sK0_skl,domain(one)),domain(X0)) ),
inference(forward_demodulation,[status(thm)],[f108,f371]) ).
fof(f373,plain,
! [X0] :
( addition(one,forward_diamond(star(sK0_skl),domain(X0))) = forward_diamond(star(sK0_skl),domain(X0))
| addition(one,addition(domain(sK0_skl),domain(X0))) != addition(forward_diamond(sK0_skl,one),domain(X0)) ),
inference(forward_demodulation,[status(thm)],[f94,f372]) ).
fof(f374,plain,
! [X0] :
( addition(one,forward_diamond(star(sK0_skl),domain(X0))) = forward_diamond(star(sK0_skl),domain(X0))
| addition(one,addition(domain(sK0_skl),domain(X0))) != addition(domain(sK0_skl),domain(X0)) ),
inference(forward_demodulation,[status(thm)],[f108,f373]) ).
fof(f547,plain,
! [X0] : one = addition(domain(X0),domain(antidomain(X0))),
inference(paramodulation,[status(thm)],[f49,f136]) ).
fof(f556,plain,
! [X0] : one = addition(domain(X0),c(X0)),
inference(forward_demodulation,[status(thm)],[f169,f547]) ).
fof(f998,plain,
! [X0] : addition(domain(X0),one) = addition(domain(X0),c(X0)),
inference(paramodulation,[status(thm)],[f556,f271]) ).
fof(f1030,plain,
! [X0] : addition(domain(X0),one) = one,
inference(forward_demodulation,[status(thm)],[f556,f998]) ).
fof(f1085,plain,
! [X0] : addition(one,domain(X0)) = one,
inference(paramodulation,[status(thm)],[f31,f1030]) ).
fof(f1126,plain,
! [X0,X1] : addition(one,forward_diamond(X0,X1)) = one,
inference(paramodulation,[status(thm)],[f56,f1085]) ).
fof(f1129,plain,
! [X0,X1] : addition(one,addition(domain(X0),X1)) = addition(one,X1),
inference(paramodulation,[status(thm)],[f1085,f32]) ).
fof(f1130,plain,
! [X0] :
( one = forward_diamond(star(sK0_skl),domain(X0))
| addition(one,addition(domain(sK0_skl),domain(X0))) != addition(domain(sK0_skl),domain(X0)) ),
inference(backward_demodulation,[status(thm)],[f1126,f374]) ).
fof(f1134,plain,
! [X0] :
( one = forward_diamond(star(sK0_skl),domain(X0))
| addition(one,domain(X0)) != addition(domain(sK0_skl),domain(X0)) ),
inference(forward_demodulation,[status(thm)],[f1129,f1130]) ).
fof(f1135,plain,
! [X0] :
( one = forward_diamond(star(sK0_skl),domain(X0))
| one != addition(domain(sK0_skl),domain(X0)) ),
inference(forward_demodulation,[status(thm)],[f1085,f1134]) ).
fof(f1170,plain,
! [X0,X1] : multiplication(addition(antidomain(X0),X1),X0) = addition(zero,multiplication(X1,X0)),
inference(paramodulation,[status(thm)],[f46,f39]) ).
fof(f1200,plain,
! [X0,X1] : multiplication(addition(antidomain(X0),X1),X0) = multiplication(X1,X0),
inference(forward_demodulation,[status(thm)],[f137,f1170]) ).
fof(f1223,plain,
! [X0,X1] : domain_difference(antidomain(X0),X1) = multiplication(c(X0),antidomain(X1)),
inference(paramodulation,[status(thm)],[f169,f55]) ).
fof(f1229,plain,
! [X0,X1] : domain_difference(X0,antidomain(X1)) = multiplication(domain(X0),domain(X1)),
inference(paramodulation,[status(thm)],[f49,f55]) ).
fof(f2449,plain,
! [X0] :
( one = forward_diamond(star(sK0_skl),domain(antidomain(X0)))
| one != addition(domain(sK0_skl),c(X0)) ),
inference(paramodulation,[status(thm)],[f169,f1135]) ).
fof(f2457,plain,
! [X0] :
( one = forward_diamond(star(sK0_skl),c(X0))
| one != addition(domain(sK0_skl),c(X0)) ),
inference(forward_demodulation,[status(thm)],[f169,f2449]) ).
fof(f3605,plain,
! [X0] : multiplication(one,X0) = multiplication(domain(X0),X0),
inference(paramodulation,[status(thm)],[f136,f1200]) ).
fof(f3635,plain,
! [X0] : X0 = multiplication(domain(X0),X0),
inference(forward_demodulation,[status(thm)],[f37,f3605]) ).
fof(f3658,plain,
! [X0] : antidomain(X0) = domain_difference(antidomain(X0),X0),
inference(paramodulation,[status(thm)],[f55,f3635]) ).
fof(f3764,plain,
! [X0] : antidomain(antidomain(X0)) = domain_difference(domain(X0),antidomain(X0)),
inference(paramodulation,[status(thm)],[f49,f3658]) ).
fof(f3779,plain,
! [X0] : domain(X0) = domain_difference(domain(X0),antidomain(X0)),
inference(forward_demodulation,[status(thm)],[f49,f3764]) ).
fof(f4834,plain,
! [X0,X1] : domain(multiplication(X0,domain(X1))) = domain_difference(forward_diamond(X0,X1),antidomain(multiplication(X0,domain(X1)))),
inference(paramodulation,[status(thm)],[f56,f3779]) ).
fof(f4854,plain,
! [X0,X1] : forward_diamond(X0,X1) = domain_difference(forward_diamond(X0,X1),antidomain(multiplication(X0,domain(X1)))),
inference(forward_demodulation,[status(thm)],[f56,f4834]) ).
fof(f5501,plain,
! [X0] : multiplication(antidomain(antidomain(X0)),one) = multiplication(antidomain(antidomain(X0)),domain(X0)),
inference(paramodulation,[status(thm)],[f136,f329]) ).
fof(f5519,plain,
! [X0] : multiplication(antidomain(domain(X0)),one) = multiplication(antidomain(domain(X0)),antidomain(X0)),
inference(paramodulation,[status(thm)],[f67,f329]) ).
fof(f5672,plain,
! [X0] : antidomain(antidomain(X0)) = multiplication(antidomain(antidomain(X0)),domain(X0)),
inference(forward_demodulation,[status(thm)],[f36,f5501]) ).
fof(f5673,plain,
! [X0] : domain(X0) = multiplication(antidomain(antidomain(X0)),domain(X0)),
inference(forward_demodulation,[status(thm)],[f49,f5672]) ).
fof(f5674,plain,
! [X0] : domain(X0) = multiplication(domain(X0),domain(X0)),
inference(forward_demodulation,[status(thm)],[f49,f5673]) ).
fof(f5675,plain,
! [X0] : domain(X0) = domain_difference(X0,antidomain(X0)),
inference(forward_demodulation,[status(thm)],[f1229,f5674]) ).
fof(f5690,plain,
! [X0] : antidomain(domain(X0)) = multiplication(antidomain(domain(X0)),antidomain(X0)),
inference(forward_demodulation,[status(thm)],[f36,f5519]) ).
fof(f5691,plain,
! [X0] : c(X0) = multiplication(antidomain(domain(X0)),antidomain(X0)),
inference(forward_demodulation,[status(thm)],[f54,f5690]) ).
fof(f5692,plain,
! [X0] : c(X0) = multiplication(c(X0),antidomain(X0)),
inference(forward_demodulation,[status(thm)],[f54,f5691]) ).
fof(f5693,plain,
! [X0] : c(X0) = domain_difference(antidomain(X0),X0),
inference(forward_demodulation,[status(thm)],[f1223,f5692]) ).
fof(f5694,plain,
! [X0,X1] : antidomain(multiplication(X0,domain(X1))) = antidomain(forward_diamond(X0,X1)),
inference(backward_demodulation,[status(thm)],[f5861,f219]) ).
fof(f5701,plain,
! [X0,X1] : forward_box(X0,X1) = antidomain(forward_diamond(X0,c(X1))),
inference(backward_demodulation,[status(thm)],[f5861,f58]) ).
fof(f5717,plain,
! [X0] :
( one = forward_diamond(star(sK0_skl),antidomain(X0))
| one != addition(domain(sK0_skl),c(X0)) ),
inference(backward_demodulation,[status(thm)],[f5861,f2457]) ).
fof(f5861,plain,
! [X0] : c(X0) = antidomain(X0),
inference(forward_demodulation,[status(thm)],[f3658,f5693]) ).
fof(f6057,plain,
! [X0,X1] : forward_diamond(X0,X1) = domain_difference(forward_diamond(X0,X1),antidomain(forward_diamond(X0,X1))),
inference(backward_demodulation,[status(thm)],[f5694,f4854]) ).
fof(f6071,plain,
! [X0,X1] : forward_box(X0,X1) = antidomain(forward_diamond(X0,antidomain(X1))),
inference(forward_demodulation,[status(thm)],[f5861,f5701]) ).
fof(f6081,plain,
! [X0] :
( one = forward_diamond(star(sK0_skl),antidomain(X0))
| one != addition(domain(sK0_skl),antidomain(X0)) ),
inference(forward_demodulation,[status(thm)],[f5861,f5717]) ).
fof(f6268,plain,
! [X0,X1] : forward_diamond(X0,X1) = domain(forward_diamond(X0,X1)),
inference(forward_demodulation,[status(thm)],[f5675,f6057]) ).
fof(f6868,plain,
! [X0,X1] : domain(forward_diamond(X0,antidomain(X1))) = antidomain(forward_box(X0,X1)),
inference(paramodulation,[status(thm)],[f6071,f49]) ).
fof(f6899,plain,
antidomain(forward_box(star(sK0_skl),sK0_skl)) != one,
inference(backward_demodulation,[status(thm)],[f6937,f66]) ).
fof(f6912,plain,
! [X0] :
( one = antidomain(forward_box(star(sK0_skl),X0))
| one != addition(domain(sK0_skl),antidomain(X0)) ),
inference(backward_demodulation,[status(thm)],[f6937,f6081]) ).
fof(f6937,plain,
! [X0,X1] : forward_diamond(X0,antidomain(X1)) = antidomain(forward_box(X0,X1)),
inference(forward_demodulation,[status(thm)],[f6268,f6868]) ).
fof(f7230,plain,
one != addition(domain(sK0_skl),antidomain(sK0_skl)),
inference(resolution,[status(thm)],[f6912,f6899]) ).
fof(f7234,plain,
one != one,
inference(forward_demodulation,[status(thm)],[f67,f7230]) ).
fof(f7235,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f7234]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : KLE135+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Sun Sep 20 22:45:22 UTC 2026
% 0.02/0.29 % CPUTime :
% 0.02/0.30 % Drodi V4.1.1
% 1.17/0.57 % Refutation found
% 1.17/0.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.17/0.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.17/0.60 % Elapsed time: 0.297114 seconds
% 1.17/0.60 % CPU time: 2.125635 seconds
% 1.17/0.60 % Total memory used: 130.238 MB
% 1.17/0.60 % Net memory used: 128.053 MB
%------------------------------------------------------------------------------