%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KLE132+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -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:22 PM UTC 2026
% Result : Theorem 8.09s 6.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : KLE132+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.04/5.51 % Computer : n012.cluster.edu
% 0.04/5.51 % Model : x86_64 x86_64
% 0.04/5.51 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/5.51 % Memory : 8046.5625MB
% 0.04/5.51 % OS : Linux 6.8.0-71-generic
% 0.04/5.51 % CPULimit : 300
% 0.04/5.51 % WCLimit : 300
% 0.04/5.51 % DateTime : Sun Sep 20 22:45:08 UTC 2026
% 0.04/5.52 % CPUTime :
% 0.04/5.53 % Drodi V4.1.1
% 8.09/6.61 % Refutation found
% 8.09/6.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.09/6.61 % SZS output start CNFRefutation for theBenchmark
% 8.09/6.61 fof(f1,axiom,(
% 8.09/6.61 (! [A,B] : addition(A,B) = addition(B,A) )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f2,axiom,(
% 8.09/6.61 (! [C,B,A] : addition(A,addition(B,C)) = addition(addition(A,B),C) )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f3,axiom,(
% 8.09/6.61 (! [A] : addition(A,zero) = A )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f4,axiom,(
% 8.09/6.61 (! [A] : addition(A,A) = A )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f6,axiom,(
% 8.09/6.61 (! [A] : multiplication(A,one) = A )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f7,axiom,(
% 8.09/6.61 (! [A] : multiplication(one,A) = A )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f8,axiom,(
% 8.09/6.61 (! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)) )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f9,axiom,(
% 8.09/6.61 (! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)) )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f10,axiom,(
% 8.09/6.61 (! [A] : multiplication(A,zero) = zero )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f11,axiom,(
% 8.09/6.61 (! [A] : multiplication(zero,A) = zero )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f13,axiom,(
% 8.09/6.61 (! [X0] : multiplication(antidomain(X0),X0) = zero )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f15,axiom,(
% 8.09/6.61 (! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f16,axiom,(
% 8.09/6.61 (! [X0] : domain(X0) = antidomain(antidomain(X0)) )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f21,axiom,(
% 8.09/6.61 (! [X0] : c(X0) = antidomain(domain(X0)) )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f22,axiom,(
% 8.09/6.61 (! [X0,X1] : domain_difference(X0,X1) = multiplication(domain(X0),antidomain(X1)) )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f23,axiom,(
% 8.09/6.61 (! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))) )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f27,axiom,(
% 8.09/6.61 (! [X0] : forward_diamond(X0,divergence(X0)) = divergence(X0) )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f28,axiom,(
% 8.09/6.61 (! [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))) ) )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f29,conjecture,(
% 8.09/6.61 (! [X0] :( (! [X1] : addition(forward_diamond(X0,domain(X1)),forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1))))) = forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1)))))=> (! [X2] :( addition(domain(X2),forward_diamond(X0,domain(X2))) = forward_diamond(X0,domain(X2))=> domain(X2) = zero ) )) )),
% 8.09/6.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.09/6.61 fof(f30,negated_conjecture,(
% 8.09/6.61 ~((! [X0] :( (! [X1] : addition(forward_diamond(X0,domain(X1)),forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1))))) = forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1)))))=> (! [X2] :( addition(domain(X2),forward_diamond(X0,domain(X2))) = forward_diamond(X0,domain(X2))=> domain(X2) = zero ) )) ))),
% 8.09/6.61 inference(negated_conjecture,[status(cth)],[f29])).
% 8.09/6.61 fof(f31,plain,(
% 8.09/6.61 ![X0,X1]: (addition(X0,X1)=addition(X1,X0))),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f1])).
% 8.09/6.61 fof(f32,plain,(
% 8.09/6.61 ![X0,X1,X2]: (addition(X0,addition(X1,X2))=addition(addition(X0,X1),X2))),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f2])).
% 8.09/6.61 fof(f33,plain,(
% 8.09/6.61 ![X0]: (addition(X0,zero)=X0)),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f3])).
% 8.09/6.61 fof(f34,plain,(
% 8.09/6.61 ![X0]: (addition(X0,X0)=X0)),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f4])).
% 8.09/6.61 fof(f36,plain,(
% 8.09/6.61 ![X0]: (multiplication(X0,one)=X0)),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f6])).
% 8.09/6.61 fof(f37,plain,(
% 8.09/6.61 ![X0]: (multiplication(one,X0)=X0)),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f7])).
% 8.09/6.61 fof(f38,plain,(
% 8.09/6.61 ![X0,X1,X2]: (multiplication(X0,addition(X1,X2))=addition(multiplication(X0,X1),multiplication(X0,X2)))),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f8])).
% 8.09/6.61 fof(f39,plain,(
% 8.09/6.61 ![X0,X1,X2]: (multiplication(addition(X0,X1),X2)=addition(multiplication(X0,X2),multiplication(X1,X2)))),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f9])).
% 8.09/6.61 fof(f40,plain,(
% 8.09/6.61 ![X0]: (multiplication(X0,zero)=zero)),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f10])).
% 8.09/6.61 fof(f41,plain,(
% 8.09/6.61 ![X0]: (multiplication(zero,X0)=zero)),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f11])).
% 8.09/6.61 fof(f46,plain,(
% 8.09/6.61 ![X0]: (multiplication(antidomain(X0),X0)=zero)),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f13])).
% 8.09/6.61 fof(f48,plain,(
% 8.09/6.61 ![X0]: (addition(antidomain(antidomain(X0)),antidomain(X0))=one)),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f15])).
% 8.09/6.61 fof(f49,plain,(
% 8.09/6.61 ![X0]: (domain(X0)=antidomain(antidomain(X0)))),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f16])).
% 8.09/6.61 fof(f54,plain,(
% 8.09/6.61 ![X0]: (c(X0)=antidomain(domain(X0)))),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f21])).
% 8.09/6.61 fof(f55,plain,(
% 8.09/6.61 ![X0,X1]: (domain_difference(X0,X1)=multiplication(domain(X0),antidomain(X1)))),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f22])).
% 8.09/6.61 fof(f56,plain,(
% 8.09/6.61 ![X0,X1]: (forward_diamond(X0,X1)=domain(multiplication(X0,domain(X1))))),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f23])).
% 8.09/6.61 fof(f60,plain,(
% 8.09/6.61 ![X0]: (forward_diamond(X0,divergence(X0))=divergence(X0))),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f27])).
% 8.09/6.61 fof(f61,plain,(
% 8.09/6.61 ![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))))),
% 8.09/6.61 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 8.09/6.61 fof(f62,plain,(
% 8.09/6.61 ![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))))),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f61])).
% 8.09/6.61 fof(f63,plain,(
% 8.09/6.61 (?[X0]: ((![X1]: addition(forward_diamond(X0,domain(X1)),forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1)))))=forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1)))))&(?[X2]: (addition(domain(X2),forward_diamond(X0,domain(X2)))=forward_diamond(X0,domain(X2))&~domain(X2)=zero))))),
% 8.09/6.61 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 8.09/6.61 fof(f64,plain,(
% 8.09/6.61 ((![X1]: addition(forward_diamond(sK0_skl,domain(X1)),forward_diamond(star(sK0_skl),domain_difference(domain(X1),forward_diamond(sK0_skl,domain(X1)))))=forward_diamond(star(sK0_skl),domain_difference(domain(X1),forward_diamond(sK0_skl,domain(X1)))))&(addition(domain(sK1_skl),forward_diamond(sK0_skl,domain(sK1_skl)))=forward_diamond(sK0_skl,domain(sK1_skl))&~domain(sK1_skl)=zero))),
% 8.09/6.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X2,sK1_skl)],[f63])).
% 8.09/6.61 fof(f65,plain,(
% 8.09/6.61 ![X0]: (addition(forward_diamond(sK0_skl,domain(X0)),forward_diamond(star(sK0_skl),domain_difference(domain(X0),forward_diamond(sK0_skl,domain(X0)))))=forward_diamond(star(sK0_skl),domain_difference(domain(X0),forward_diamond(sK0_skl,domain(X0)))))),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f64])).
% 8.09/6.61 fof(f66,plain,(
% 8.09/6.61 addition(domain(sK1_skl),forward_diamond(sK0_skl,domain(sK1_skl)))=forward_diamond(sK0_skl,domain(sK1_skl))),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f64])).
% 8.09/6.61 fof(f67,plain,(
% 8.09/6.61 ~domain(sK1_skl)=zero),
% 8.09/6.61 inference(cnf_transformation,[status(thm)],[f64])).
% 8.09/6.61 fof(f68,plain,(
% 8.09/6.61 ![X0]: (addition(domain(X0),antidomain(X0))=one)),
% 8.09/6.61 inference(backward_demodulation,[status(thm)],[f49,f48])).
% 8.09/6.61 fof(f76,plain,(
% 8.09/6.61 ![X0]: (X0=addition(zero,X0))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f33,f31])).
% 8.09/6.61 fof(f97,plain,(
% 8.09/6.61 ![X0]: (forward_diamond(zero,X0)=domain(zero))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f41,f56])).
% 8.09/6.61 fof(f98,plain,(
% 8.09/6.61 ![X0,X1,X2]: (forward_diamond(X0,multiplication(X1,domain(X2)))=domain(multiplication(X0,forward_diamond(X1,X2))))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f56,f56])).
% 8.09/6.61 fof(f100,plain,(
% 8.09/6.61 ![X0,X1]: (addition(forward_diamond(sK0_skl,domain(multiplication(X0,domain(X1)))),forward_diamond(star(sK0_skl),domain_difference(domain(multiplication(X0,domain(X1))),forward_diamond(sK0_skl,forward_diamond(X0,X1)))))=forward_diamond(star(sK0_skl),domain_difference(domain(multiplication(X0,domain(X1))),forward_diamond(sK0_skl,domain(multiplication(X0,domain(X1)))))))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f56,f65])).
% 8.09/6.61 fof(f104,plain,(
% 8.09/6.61 ![X0,X1]: (addition(forward_diamond(sK0_skl,forward_diamond(X0,X1)),forward_diamond(star(sK0_skl),domain_difference(domain(multiplication(X0,domain(X1))),forward_diamond(sK0_skl,forward_diamond(X0,X1)))))=forward_diamond(star(sK0_skl),domain_difference(domain(multiplication(X0,domain(X1))),forward_diamond(sK0_skl,domain(multiplication(X0,domain(X1)))))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f56,f100])).
% 8.09/6.61 fof(f105,plain,(
% 8.09/6.61 ![X0,X1]: (addition(forward_diamond(sK0_skl,forward_diamond(X0,X1)),forward_diamond(star(sK0_skl),domain_difference(forward_diamond(X0,X1),forward_diamond(sK0_skl,forward_diamond(X0,X1)))))=forward_diamond(star(sK0_skl),domain_difference(domain(multiplication(X0,domain(X1))),forward_diamond(sK0_skl,domain(multiplication(X0,domain(X1)))))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f56,f104])).
% 8.09/6.61 fof(f106,plain,(
% 8.09/6.61 ![X0,X1]: (addition(forward_diamond(sK0_skl,forward_diamond(X0,X1)),forward_diamond(star(sK0_skl),domain_difference(forward_diamond(X0,X1),forward_diamond(sK0_skl,forward_diamond(X0,X1)))))=forward_diamond(star(sK0_skl),domain_difference(forward_diamond(X0,X1),forward_diamond(sK0_skl,domain(multiplication(X0,domain(X1)))))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f56,f105])).
% 8.09/6.61 fof(f107,plain,(
% 8.09/6.61 ![X0,X1]: (addition(forward_diamond(sK0_skl,forward_diamond(X0,X1)),forward_diamond(star(sK0_skl),domain_difference(forward_diamond(X0,X1),forward_diamond(sK0_skl,forward_diamond(X0,X1)))))=forward_diamond(star(sK0_skl),domain_difference(forward_diamond(X0,X1),forward_diamond(sK0_skl,forward_diamond(X0,X1)))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f56,f106])).
% 8.09/6.61 fof(f117,plain,(
% 8.09/6.61 ![X0,X1,X2]: (addition(X0,addition(X1,X2))=addition(X2,addition(X0,X1)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f31,f32])).
% 8.09/6.61 fof(f123,plain,(
% 8.09/6.61 ![X0]: (addition(domain(sK1_skl),addition(forward_diamond(sK0_skl,domain(sK1_skl)),X0))=addition(forward_diamond(sK0_skl,domain(sK1_skl)),X0))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f66,f32])).
% 8.09/6.61 fof(f127,plain,(
% 8.09/6.61 ![X0,X1]: (addition(X0,addition(X0,X1))=addition(X0,X1))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f34,f32])).
% 8.09/6.61 fof(f142,plain,(
% 8.09/6.61 ![X0,X1]: (addition(X0,addition(X1,X0))=addition(X0,X1))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f31,f127])).
% 8.09/6.61 fof(f216,plain,(
% 8.09/6.61 ![X0,X1]: (addition(X0,X1)=addition(X1,addition(X0,X1)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f34,f117])).
% 8.09/6.61 fof(f561,plain,(
% 8.09/6.61 zero=antidomain(one)),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f46,f36])).
% 8.09/6.61 fof(f570,plain,(
% 8.09/6.61 ![X0]: (forward_diamond(one,X0)=domain(domain(X0)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f37,f56])).
% 8.09/6.61 fof(f576,plain,(
% 8.09/6.61 ![X0]: (domain(antidomain(X0))=antidomain(domain(X0)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f49,f49])).
% 8.09/6.61 fof(f577,plain,(
% 8.09/6.61 domain(one)=antidomain(zero)),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f561,f49])).
% 8.09/6.61 fof(f579,plain,(
% 8.09/6.61 ![X0]: (multiplication(domain(X0),antidomain(X0))=zero)),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f49,f46])).
% 8.09/6.61 fof(f580,plain,(
% 8.09/6.61 ![X0]: (domain(antidomain(X0))=c(X0))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f54,f576])).
% 8.09/6.61 fof(f581,plain,(
% 8.09/6.61 ![X0]: (domain_difference(X0,X0)=zero)),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f55,f579])).
% 8.09/6.61 fof(f588,plain,(
% 8.09/6.61 ![X0]: (domain(domain(X0))=c(antidomain(X0)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f49,f580])).
% 8.09/6.61 fof(f589,plain,(
% 8.09/6.61 domain(zero)=c(one)),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f561,f580])).
% 8.09/6.61 fof(f595,plain,(
% 8.09/6.61 ![X0,X1]: (domain_difference(antidomain(X0),X1)=multiplication(c(X0),antidomain(X1)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f580,f55])).
% 8.09/6.61 fof(f599,plain,(
% 8.09/6.61 ![X0]: (forward_diamond(one,X0)=c(antidomain(X0)))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f570,f588])).
% 8.09/6.61 fof(f600,plain,(
% 8.09/6.61 ![X0]: (forward_diamond(zero,X0)=c(one))),
% 8.09/6.61 inference(backward_demodulation,[status(thm)],[f589,f97])).
% 8.09/6.61 fof(f692,plain,(
% 8.09/6.61 divergence(zero)=c(one)),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f60,f600])).
% 8.09/6.61 fof(f696,plain,(
% 8.09/6.61 domain(zero)=divergence(zero)),
% 8.09/6.61 inference(backward_demodulation,[status(thm)],[f692,f589])).
% 8.09/6.61 fof(f726,plain,(
% 8.09/6.61 addition(domain(one),zero)=one),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f561,f68])).
% 8.09/6.61 fof(f731,plain,(
% 8.09/6.61 ![X0]: (addition(domain(X0),antidomain(X0))=addition(antidomain(X0),one))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f68,f216])).
% 8.09/6.61 fof(f734,plain,(
% 8.09/6.61 ![X0]: (addition(antidomain(X0),one)=addition(antidomain(X0),domain(X0)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f68,f142])).
% 8.09/6.61 fof(f740,plain,(
% 8.09/6.61 one=antidomain(zero)),
% 8.09/6.61 inference(backward_demodulation,[status(thm)],[f741,f577])).
% 8.09/6.61 fof(f741,plain,(
% 8.09/6.61 domain(one)=one),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f33,f726])).
% 8.09/6.61 fof(f742,plain,(
% 8.09/6.61 ![X0]: (one=addition(antidomain(X0),one))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f68,f731])).
% 8.09/6.61 fof(f744,plain,(
% 8.09/6.61 ![X0]: (one=addition(antidomain(X0),domain(X0)))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f742,f734])).
% 8.09/6.61 fof(f748,plain,(
% 8.09/6.61 domain(zero)=antidomain(one)),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f740,f49])).
% 8.09/6.61 fof(f753,plain,(
% 8.09/6.61 divergence(zero)=antidomain(one)),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f696,f748])).
% 8.09/6.61 fof(f755,plain,(
% 8.09/6.61 domain(zero)=zero),
% 8.09/6.61 inference(backward_demodulation,[status(thm)],[f759,f696])).
% 8.09/6.61 fof(f759,plain,(
% 8.09/6.61 divergence(zero)=zero),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f561,f753])).
% 8.09/6.61 fof(f798,plain,(
% 8.09/6.61 ![X0,X1]: (multiplication(antidomain(X0),addition(X0,X1))=addition(zero,multiplication(antidomain(X0),X1)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f46,f38])).
% 8.09/6.61 fof(f828,plain,(
% 8.09/6.61 ![X0,X1]: (multiplication(antidomain(X0),addition(X0,X1))=multiplication(antidomain(X0),X1))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f76,f798])).
% 8.09/6.61 fof(f857,plain,(
% 8.09/6.61 ![X0,X1]: (multiplication(addition(antidomain(X0),X1),X0)=addition(zero,multiplication(X1,X0)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f46,f39])).
% 8.09/6.61 fof(f885,plain,(
% 8.09/6.61 ![X0,X1]: (multiplication(addition(antidomain(X0),X1),X0)=multiplication(X1,X0))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f76,f857])).
% 8.09/6.61 fof(f1090,plain,(
% 8.09/6.61 ![X0]: (forward_diamond(X0,zero)=domain(multiplication(X0,zero)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f755,f56])).
% 8.09/6.61 fof(f1122,plain,(
% 8.09/6.61 ![X0]: (forward_diamond(X0,zero)=domain(zero))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f40,f1090])).
% 8.09/6.61 fof(f1125,plain,(
% 8.09/6.61 ![X0]: (forward_diamond(X0,zero)=zero)),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f755,f1122])).
% 8.09/6.61 fof(f1334,plain,(
% 8.09/6.61 ![X0,X1]: (forward_diamond(one,multiplication(X0,domain(X1)))=domain(forward_diamond(X0,X1)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f56,f570])).
% 8.09/6.61 fof(f1932,plain,(
% 8.09/6.61 ![X0]: (multiplication(one,X0)=multiplication(domain(X0),X0))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f744,f885])).
% 8.09/6.61 fof(f1961,plain,(
% 8.09/6.61 ![X0]: (X0=multiplication(domain(X0),X0))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f37,f1932])).
% 8.09/6.61 fof(f1977,plain,(
% 8.09/6.61 ![X0]: (antidomain(X0)=domain_difference(antidomain(X0),X0))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f55,f1961])).
% 8.09/6.61 fof(f2424,plain,(
% 8.09/6.61 ![X0]: (addition(domain(sK1_skl),addition(divergence(sK0_skl),forward_diamond(star(sK0_skl),domain(X0))))=addition(divergence(sK0_skl),forward_diamond(star(sK0_skl),domain(X0))))),
% 8.09/6.61 inference(resolution,[status(thm)],[f123,f62])).
% 8.09/6.61 fof(f5340,plain,(
% 8.09/6.61 ![X0]: (multiplication(antidomain(domain(X0)),one)=multiplication(antidomain(domain(X0)),antidomain(X0)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f68,f828])).
% 8.09/6.61 fof(f5390,plain,(
% 8.09/6.61 ![X0]: (antidomain(domain(X0))=multiplication(antidomain(domain(X0)),antidomain(X0)))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f36,f5340])).
% 8.09/6.61 fof(f5391,plain,(
% 8.09/6.61 ![X0]: (c(X0)=multiplication(antidomain(domain(X0)),antidomain(X0)))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f54,f5390])).
% 8.09/6.61 fof(f5392,plain,(
% 8.09/6.61 ![X0]: (c(X0)=multiplication(c(X0),antidomain(X0)))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f54,f5391])).
% 8.09/6.61 fof(f5393,plain,(
% 8.09/6.61 ![X0]: (antidomain(X0)=c(X0))),
% 8.09/6.61 inference(backward_demodulation,[status(thm)],[f5394,f1977])).
% 8.09/6.61 fof(f5394,plain,(
% 8.09/6.61 ![X0]: (c(X0)=domain_difference(antidomain(X0),X0))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f595,f5392])).
% 8.09/6.61 fof(f5412,plain,(
% 8.09/6.61 ![X0]: (domain(X0)=c(antidomain(X0)))),
% 8.09/6.61 inference(backward_demodulation,[status(thm)],[f5393,f49])).
% 8.09/6.61 fof(f5424,plain,(
% 8.09/6.61 ![X0]: (forward_diamond(one,X0)=c(c(X0)))),
% 8.09/6.61 inference(backward_demodulation,[status(thm)],[f5393,f599])).
% 8.09/6.61 fof(f5585,plain,(
% 8.09/6.61 ![X0]: (domain(X0)=c(c(X0)))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f5393,f5412])).
% 8.09/6.61 fof(f5596,plain,(
% 8.09/6.61 ![X0,X1]: (domain(multiplication(X0,domain(X1)))=domain(forward_diamond(X0,X1)))),
% 8.09/6.61 inference(backward_demodulation,[status(thm)],[f5613,f1334])).
% 8.09/6.61 fof(f5613,plain,(
% 8.09/6.61 ![X0]: (forward_diamond(one,X0)=domain(X0))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f5585,f5424])).
% 8.09/6.61 fof(f5812,plain,(
% 8.09/6.61 ![X0,X1]: (forward_diamond(X0,X1)=domain(forward_diamond(X0,X1)))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f56,f5596])).
% 8.09/6.61 fof(f5946,plain,(
% 8.09/6.61 ![X0,X1]: (forward_diamond(X0,multiplication(one,domain(X1)))=domain(multiplication(X0,domain(X1))))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f5613,f98])).
% 8.09/6.61 fof(f5947,plain,(
% 8.09/6.61 ![X0]: (addition(forward_diamond(sK0_skl,forward_diamond(one,X0)),forward_diamond(star(sK0_skl),domain_difference(forward_diamond(one,X0),forward_diamond(sK0_skl,domain(X0)))))=forward_diamond(star(sK0_skl),domain_difference(forward_diamond(one,X0),forward_diamond(sK0_skl,forward_diamond(one,X0)))))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f5613,f107])).
% 8.09/6.61 fof(f5973,plain,(
% 8.09/6.61 ![X0,X1]: (forward_diamond(X0,domain(X1))=domain(multiplication(X0,domain(X1))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f37,f5946])).
% 8.09/6.61 fof(f6029,plain,(
% 8.09/6.61 ![X0]: (addition(domain(sK1_skl),addition(divergence(sK0_skl),forward_diamond(star(sK0_skl),domain(X0))))=addition(divergence(sK0_skl),forward_diamond(star(sK0_skl),X0)))),
% 8.09/6.61 inference(backward_demodulation,[status(thm)],[f6045,f2424])).
% 8.09/6.61 fof(f6045,plain,(
% 8.09/6.61 ![X0,X1]: (forward_diamond(X0,domain(X1))=forward_diamond(X0,X1))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f56,f5973])).
% 8.09/6.61 fof(f6046,plain,(
% 8.09/6.61 ![X0]: (addition(forward_diamond(sK0_skl,domain(X0)),forward_diamond(star(sK0_skl),domain_difference(forward_diamond(one,X0),forward_diamond(sK0_skl,domain(X0)))))=forward_diamond(star(sK0_skl),domain_difference(forward_diamond(one,X0),forward_diamond(sK0_skl,forward_diamond(one,X0)))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f5613,f5947])).
% 8.09/6.61 fof(f6047,plain,(
% 8.09/6.61 ![X0]: (addition(forward_diamond(sK0_skl,X0),forward_diamond(star(sK0_skl),domain_difference(forward_diamond(one,X0),forward_diamond(sK0_skl,domain(X0)))))=forward_diamond(star(sK0_skl),domain_difference(forward_diamond(one,X0),forward_diamond(sK0_skl,forward_diamond(one,X0)))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f6045,f6046])).
% 8.09/6.61 fof(f6048,plain,(
% 8.09/6.61 ![X0]: (addition(forward_diamond(sK0_skl,X0),forward_diamond(star(sK0_skl),domain_difference(domain(X0),forward_diamond(sK0_skl,domain(X0)))))=forward_diamond(star(sK0_skl),domain_difference(forward_diamond(one,X0),forward_diamond(sK0_skl,forward_diamond(one,X0)))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f5613,f6047])).
% 8.09/6.61 fof(f6049,plain,(
% 8.09/6.61 ![X0]: (addition(forward_diamond(sK0_skl,X0),forward_diamond(star(sK0_skl),domain_difference(domain(X0),forward_diamond(sK0_skl,X0))))=forward_diamond(star(sK0_skl),domain_difference(forward_diamond(one,X0),forward_diamond(sK0_skl,forward_diamond(one,X0)))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f6045,f6048])).
% 8.09/6.61 fof(f6050,plain,(
% 8.09/6.61 ![X0]: (addition(forward_diamond(sK0_skl,X0),forward_diamond(star(sK0_skl),domain_difference(domain(X0),forward_diamond(sK0_skl,X0))))=forward_diamond(star(sK0_skl),domain_difference(domain(X0),forward_diamond(sK0_skl,forward_diamond(one,X0)))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f5613,f6049])).
% 8.09/6.61 fof(f6051,plain,(
% 8.09/6.61 ![X0]: (addition(forward_diamond(sK0_skl,X0),forward_diamond(star(sK0_skl),domain_difference(domain(X0),forward_diamond(sK0_skl,X0))))=forward_diamond(star(sK0_skl),domain_difference(domain(X0),forward_diamond(sK0_skl,domain(X0)))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f5613,f6050])).
% 8.09/6.61 fof(f6052,plain,(
% 8.09/6.61 ![X0]: (addition(forward_diamond(sK0_skl,X0),forward_diamond(star(sK0_skl),domain_difference(domain(X0),forward_diamond(sK0_skl,X0))))=forward_diamond(star(sK0_skl),domain_difference(domain(X0),forward_diamond(sK0_skl,X0))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f6045,f6051])).
% 8.09/6.61 fof(f6143,plain,(
% 8.09/6.61 ![X0]: (addition(domain(sK1_skl),addition(divergence(sK0_skl),forward_diamond(star(sK0_skl),X0)))=addition(divergence(sK0_skl),forward_diamond(star(sK0_skl),X0)))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f6045,f6029])).
% 8.09/6.61 fof(f6273,plain,(
% 8.09/6.61 ![X0]: (forward_diamond(X0,divergence(X0))=domain(divergence(X0)))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f60,f5812])).
% 8.09/6.61 fof(f6290,plain,(
% 8.09/6.61 ![X0]: (divergence(X0)=domain(divergence(X0)))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f60,f6273])).
% 8.09/6.61 fof(f6694,plain,(
% 8.09/6.61 addition(divergence(sK0_skl),forward_diamond(star(sK0_skl),domain_difference(domain(divergence(sK0_skl)),forward_diamond(sK0_skl,divergence(sK0_skl)))))=forward_diamond(star(sK0_skl),domain_difference(domain(divergence(sK0_skl)),forward_diamond(sK0_skl,divergence(sK0_skl))))),
% 8.09/6.61 inference(paramodulation,[status(thm)],[f60,f6052])).
% 8.09/6.61 fof(f6733,plain,(
% 8.09/6.61 addition(divergence(sK0_skl),forward_diamond(star(sK0_skl),domain_difference(divergence(sK0_skl),forward_diamond(sK0_skl,divergence(sK0_skl)))))=forward_diamond(star(sK0_skl),domain_difference(domain(divergence(sK0_skl)),forward_diamond(sK0_skl,divergence(sK0_skl))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f6290,f6694])).
% 8.09/6.61 fof(f6734,plain,(
% 8.09/6.61 addition(divergence(sK0_skl),forward_diamond(star(sK0_skl),domain_difference(divergence(sK0_skl),divergence(sK0_skl))))=forward_diamond(star(sK0_skl),domain_difference(domain(divergence(sK0_skl)),forward_diamond(sK0_skl,divergence(sK0_skl))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f60,f6733])).
% 8.09/6.61 fof(f6735,plain,(
% 8.09/6.61 addition(divergence(sK0_skl),forward_diamond(star(sK0_skl),zero))=forward_diamond(star(sK0_skl),domain_difference(domain(divergence(sK0_skl)),forward_diamond(sK0_skl,divergence(sK0_skl))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f581,f6734])).
% 8.09/6.61 fof(f6736,plain,(
% 8.09/6.61 addition(divergence(sK0_skl),zero)=forward_diamond(star(sK0_skl),domain_difference(domain(divergence(sK0_skl)),forward_diamond(sK0_skl,divergence(sK0_skl))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f1125,f6735])).
% 8.09/6.61 fof(f6737,plain,(
% 8.09/6.61 divergence(sK0_skl)=forward_diamond(star(sK0_skl),domain_difference(domain(divergence(sK0_skl)),forward_diamond(sK0_skl,divergence(sK0_skl))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f33,f6736])).
% 8.09/6.61 fof(f6738,plain,(
% 8.09/6.61 divergence(sK0_skl)=forward_diamond(star(sK0_skl),domain_difference(divergence(sK0_skl),forward_diamond(sK0_skl,divergence(sK0_skl))))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f6290,f6737])).
% 8.09/6.61 fof(f6739,plain,(
% 8.09/6.61 divergence(sK0_skl)=forward_diamond(star(sK0_skl),domain_difference(divergence(sK0_skl),divergence(sK0_skl)))),
% 8.09/6.61 inference(forward_demodulation,[status(thm)],[f60,f6738])).
% 8.09/6.61 fof(f6740,plain,(
% 8.09/6.61 divergence(sK0_skl)=forward_diamond(star(sK0_skl),zero)),
% 8.09/6.63 inference(forward_demodulation,[status(thm)],[f581,f6739])).
% 8.09/6.63 fof(f6741,plain,(
% 8.09/6.63 ![X0]: (addition(domain(sK1_skl),addition(divergence(sK0_skl),forward_diamond(star(sK0_skl),X0)))=addition(zero,forward_diamond(star(sK0_skl),X0)))),
% 8.09/6.63 inference(backward_demodulation,[status(thm)],[f6742,f6143])).
% 8.09/6.63 fof(f6742,plain,(
% 8.09/6.63 divergence(sK0_skl)=zero),
% 8.09/6.63 inference(forward_demodulation,[status(thm)],[f1125,f6740])).
% 8.09/6.63 fof(f6792,plain,(
% 8.09/6.63 ![X0]: (addition(domain(sK1_skl),addition(zero,forward_diamond(star(sK0_skl),X0)))=addition(zero,forward_diamond(star(sK0_skl),X0)))),
% 8.09/6.63 inference(forward_demodulation,[status(thm)],[f6742,f6741])).
% 8.09/6.63 fof(f6793,plain,(
% 8.09/6.63 ![X0]: (addition(domain(sK1_skl),forward_diamond(star(sK0_skl),X0))=addition(zero,forward_diamond(star(sK0_skl),X0)))),
% 8.09/6.63 inference(forward_demodulation,[status(thm)],[f76,f6792])).
% 8.09/6.63 fof(f6795,plain,(
% 8.09/6.63 ![X0]: (addition(domain(sK1_skl),forward_diamond(star(sK0_skl),X0))=forward_diamond(star(sK0_skl),X0))),
% 8.09/6.63 inference(forward_demodulation,[status(thm)],[f76,f6793])).
% 8.09/6.63 fof(f6799,plain,(
% 8.09/6.63 addition(domain(sK1_skl),zero)=forward_diamond(star(sK0_skl),zero)),
% 8.09/6.63 inference(paramodulation,[status(thm)],[f1125,f6795])).
% 8.09/6.63 fof(f6821,plain,(
% 8.09/6.63 domain(sK1_skl)=forward_diamond(star(sK0_skl),zero)),
% 8.09/6.63 inference(forward_demodulation,[status(thm)],[f33,f6799])).
% 8.09/6.63 fof(f6822,plain,(
% 8.09/6.63 domain(sK1_skl)=zero),
% 8.09/6.63 inference(forward_demodulation,[status(thm)],[f1125,f6821])).
% 8.09/6.63 fof(f6823,plain,(
% 8.09/6.63 $false),
% 8.09/6.63 inference(forward_subsumption_resolution,[status(thm)],[f6822,f67])).
% 8.09/6.63 % SZS output end CNFRefutation for theBenchmark.p
% 8.09/6.63 % Elapsed time: 1.112539 seconds
% 8.09/6.63 % CPU time: 8.512076 seconds
% 8.09/6.63 % Total memory used: 173.123 MB
% 8.09/6.63 % Net memory used: 168.930 MB
%------------------------------------------------------------------------------