%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : KLE084-10 : TPTP v9.0.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Jul 15 06:57:49 AM UTC 2025
% Result : Unsatisfiable 228.25s 228.60s
% Output : CNFRefutation 228.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 19
% Syntax : Number of clauses : 94 ( 94 unt; 0 nHn; 9 RR)
% Number of literals : 94 ( 93 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 151 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
domain(multiplication(sK2_goals_X0,sK1_goals_X1)) != domain(multiplication(sK2_goals_X0,domain(sK1_goals_X1))),
file('theBenchmark.p',goals) ).
cnf(c1,axiom,
addition(X,X) = X,
file('theBenchmark.p',additive_idempotence) ).
cnf(c2,axiom,
addition(X,zero) = X,
file('theBenchmark.p',additive_identity) ).
cnf(c3,axiom,
multiplication(X,one) = X,
file('theBenchmark.p',multiplicative_right_identity) ).
cnf(c4,axiom,
multiplication(one,X) = X,
file('theBenchmark.p',multiplicative_left_identity) ).
cnf(c6,axiom,
multiplication(zero,X) = zero,
file('theBenchmark.p',left_annihilation) ).
cnf(c7,axiom,
domain(X) = antidomain(antidomain(X)),
file('theBenchmark.p',domain4) ).
cnf(c8,plain,
antidomain(antidomain(X)) = domain(X),
inference(equational,[status(thm)],[c7]) ).
cnf(c9,axiom,
codomain(X) = coantidomain(coantidomain(X)),
file('theBenchmark.p',codomain4) ).
cnf(c10,plain,
coantidomain(coantidomain(X)) = codomain(X),
inference(equational,[status(thm)],[c9]) ).
cnf(c11,axiom,
addition(X,Y) = addition(Y,X),
file('theBenchmark.p',additive_commutativity) ).
cnf(c12,plain,
addition(zero,X) = X,
inference(equational,[status(thm)],[c2,c11]) ).
cnf(c13,axiom,
multiplication(antidomain(X),X) = zero,
file('theBenchmark.p',domain1) ).
cnf(c14,plain,
antidomain(one) = zero,
inference(equational,[status(thm)],[c3,c13]) ).
cnf(c15,plain,
antidomain(zero) = domain(one),
inference(equational,[status(thm)],[c8,c14]) ).
cnf(c16,axiom,
multiplication(X,coantidomain(X)) = zero,
file('theBenchmark.p',codomain1) ).
cnf(c17,plain,
coantidomain(one) = zero,
inference(equational,[status(thm)],[c4,c16]) ).
cnf(c18,plain,
coantidomain(zero) = codomain(one),
inference(equational,[status(thm)],[c10,c17]) ).
cnf(c19,plain,
antidomain(domain(X)) = domain(antidomain(X)),
inference(equational,[status(thm)],[c8]) ).
cnf(c23,plain,
multiplication(domain(X),antidomain(X)) = zero,
inference(equational,[status(thm)],[c8,c13]) ).
cnf(c24,plain,
multiplication(coantidomain(X),codomain(X)) = zero,
inference(equational,[status(thm)],[c10,c16]) ).
cnf(c25,axiom,
addition(X,addition(Y,Z)) = addition(addition(X,Y),Z),
file('theBenchmark.p',additive_associativity) ).
cnf(c26,plain,
addition(addition(X,Y),Z) = addition(X,addition(Y,Z)),
inference(equational,[status(thm)],[c25]) ).
cnf(c27,axiom,
multiplication(X,multiplication(Y,Z)) = multiplication(multiplication(X,Y),Z),
file('theBenchmark.p',multiplicative_associativity) ).
cnf(c28,plain,
multiplication(multiplication(X,Y),Z) = multiplication(X,multiplication(Y,Z)),
inference(equational,[status(thm)],[c27]) ).
cnf(c29,plain,
addition(X,addition(X,Y)) = addition(X,Y),
inference(equational,[status(thm)],[c1,c26]) ).
cnf(c30,axiom,
addition(coantidomain(coantidomain(X)),coantidomain(X)) = one,
file('theBenchmark.p',codomain3) ).
cnf(c31,plain,
addition(codomain(X),coantidomain(X)) = one,
inference(equational,[status(thm)],[c10,c30]) ).
cnf(c32,plain,
codomain(one) = one,
inference(equational,[status(thm)],[c2,c17,c31]) ).
cnf(c34,plain,
addition(one,codomain(X)) = one,
inference(equational,[status(thm)],[c11,c29,c31]) ).
cnf(c35,axiom,
addition(antidomain(antidomain(X)),antidomain(X)) = one,
file('theBenchmark.p',domain3) ).
cnf(c36,plain,
addition(domain(X),antidomain(X)) = one,
inference(equational,[status(thm)],[c8,c35]) ).
cnf(c37,plain,
domain(one) = one,
inference(equational,[status(thm)],[c2,c14,c36]) ).
cnf(c40,plain,
addition(X,addition(Y,Z)) = addition(Y,addition(X,Z)),
inference(equational,[status(thm)],[c11,c26]) ).
cnf(c41,plain,
addition(X,addition(Y,X)) = addition(Y,X),
inference(equational,[status(thm)],[c1,c40]) ).
cnf(c42,plain,
addition(one,coantidomain(X)) = one,
inference(equational,[status(thm)],[c11,c31,c41]) ).
cnf(c43,plain,
addition(one,antidomain(X)) = one,
inference(equational,[status(thm)],[c11,c36,c41]) ).
cnf(c45,plain,
multiplication(antidomain(X),multiplication(X,Y)) = zero,
inference(equational,[status(thm)],[c6,c13,c28]) ).
cnf(c50,axiom,
multiplication(addition(X,Y),Z) = addition(multiplication(X,Z),multiplication(Y,Z)),
file('theBenchmark.p',left_distributivity) ).
cnf(c51,plain,
addition(multiplication(X,Y),multiplication(Z,Y)) = multiplication(addition(X,Z),Y),
inference(equational,[status(thm)],[c50]) ).
cnf(c52,plain,
addition(X,multiplication(Y,X)) = multiplication(addition(one,Y),X),
inference(equational,[status(thm)],[c4,c51]) ).
cnf(c54,plain,
multiplication(addition(X,antidomain(Y)),Y) = multiplication(X,Y),
inference(equational,[status(thm)],[c2,c13,c51]) ).
cnf(c55,plain,
multiplication(domain(X),X) = X,
inference(equational,[status(thm)],[c4,c36,c54]) ).
cnf(c65,plain,
multiplication(addition(X,Y),coantidomain(X)) = multiplication(Y,coantidomain(X)),
inference(equational,[status(thm)],[c12,c16,c51]) ).
cnf(c66,plain,
addition(X,multiplication(codomain(Y),X)) = X,
inference(equational,[status(thm)],[c4,c34,c52]) ).
cnf(c71,plain,
multiplication(antidomain(X),coantidomain(domain(X))) = coantidomain(domain(X)),
inference(equational,[status(thm)],[c4,c36,c65]) ).
cnf(c74,axiom,
multiplication(X,addition(Y,Z)) = addition(multiplication(X,Y),multiplication(X,Z)),
file('theBenchmark.p',right_distributivity) ).
cnf(c75,plain,
addition(multiplication(X,Y),multiplication(X,Z)) = multiplication(X,addition(Y,Z)),
inference(equational,[status(thm)],[c74]) ).
cnf(c76,plain,
addition(X,multiplication(X,Y)) = multiplication(X,addition(one,Y)),
inference(equational,[status(thm)],[c3,c75]) ).
cnf(c79,plain,
multiplication(X,addition(Y,coantidomain(X))) = multiplication(X,Y),
inference(equational,[status(thm)],[c2,c16,c75]) ).
cnf(c80,plain,
multiplication(X,codomain(X)) = X,
inference(equational,[status(thm)],[c3,c31,c79]) ).
cnf(c85,plain,
multiplication(antidomain(X),addition(X,Y)) = multiplication(antidomain(X),Y),
inference(equational,[status(thm)],[c12,c13,c75]) ).
cnf(c86,plain,
domain(antidomain(X)) = antidomain(X),
inference(equational,[status(thm)],[c3,c19,c36,c55,c85]) ).
cnf(c103,plain,
multiplication(antidomain(codomain(X)),coantidomain(X)) = antidomain(codomain(X)),
inference(equational,[status(thm)],[c3,c31,c85]) ).
cnf(c106,plain,
addition(coantidomain(X),antidomain(codomain(X))) = coantidomain(X),
inference(equational,[status(thm)],[c4,c43,c52,c103]) ).
cnf(c110,plain,
addition(antidomain(X),coantidomain(domain(X))) = antidomain(X),
inference(equational,[status(thm)],[c3,c42,c71,c76]) ).
cnf(c126,plain,
multiplication(X,multiplication(Y,coantidomain(multiplication(X,Y)))) = zero,
inference(equational,[status(thm)],[c16,c28]) ).
cnf(c133,plain,
addition(codomain(X),addition(Y,coantidomain(X))) = addition(Y,one),
inference(equational,[status(thm)],[c31,c40]) ).
cnf(c134,plain,
addition(domain(X),addition(Y,antidomain(X))) = addition(Y,one),
inference(equational,[status(thm)],[c36,c40]) ).
cnf(c172,plain,
multiplication(coantidomain(X),addition(Y,codomain(X))) = multiplication(coantidomain(X),Y),
inference(equational,[status(thm)],[c2,c24,c75]) ).
cnf(c175,plain,
multiplication(addition(X,domain(Y)),antidomain(Y)) = multiplication(X,antidomain(Y)),
inference(equational,[status(thm)],[c2,c23,c51]) ).
cnf(c188,plain,
multiplication(addition(X,Y),codomain(Y)) = addition(Y,multiplication(X,codomain(Y))),
inference(equational,[status(thm)],[c11,c51,c80]) ).
cnf(c202,plain,
addition(antidomain(X),codomain(antidomain(X))) = codomain(antidomain(X)),
inference(equational,[status(thm)],[c4,c43,c188]) ).
cnf(c225,plain,
addition(antidomain(X),codomain(domain(X))) = one,
inference(equational,[status(thm)],[c11,c43,c110,c133]) ).
cnf(c226,plain,
addition(coantidomain(X),domain(codomain(X))) = one,
inference(equational,[status(thm)],[c11,c42,c106,c134]) ).
cnf(c271,plain,
multiplication(coantidomain(domain(X)),antidomain(X)) = coantidomain(domain(X)),
inference(equational,[status(thm)],[c3,c172,c225]) ).
cnf(c275,plain,
multiplication(coantidomain(X),antidomain(codomain(X))) = antidomain(codomain(X)),
inference(equational,[status(thm)],[c4,c175,c226]) ).
cnf(c396,plain,
multiplication(coantidomain(antidomain(X)),domain(X)) = coantidomain(antidomain(X)),
inference(equational,[status(thm)],[c8,c86,c271]) ).
cnf(c615,plain,
addition(multiplication(X,Y),addition(multiplication(X,Z),W)) = addition(multiplication(X,addition(Y,Z)),W),
inference(equational,[status(thm)],[c26,c75]) ).
cnf(c625,plain,
addition(multiplication(X,Y),addition(multiplication(Z,Y),W)) = addition(multiplication(addition(X,Z),Y),W),
inference(equational,[status(thm)],[c26,c51]) ).
cnf(c722,plain,
multiplication(antidomain(multiplication(X,Y)),multiplication(X,multiplication(Y,Z))) = zero,
inference(equational,[status(thm)],[c28,c45]) ).
cnf(c723,plain,
multiplication(antidomain(multiplication(X,domain(Y))),multiplication(X,Y)) = zero,
inference(equational,[status(thm)],[c55,c722]) ).
cnf(c945,plain,
addition(multiplication(X,Y),addition(Z,multiplication(X,W))) = addition(multiplication(X,addition(Y,W)),Z),
inference(equational,[status(thm)],[c11,c615]) ).
cnf(c999,plain,
addition(X,multiplication(codomain(Y),addition(Z,X))) = addition(multiplication(codomain(Y),Z),X),
inference(equational,[status(thm)],[c11,c66,c945]) ).
cnf(c1334,plain,
addition(multiplication(X,Y),multiplication(Z,addition(Y,W))) = addition(multiplication(addition(X,Z),Y),multiplication(Z,W)),
inference(equational,[status(thm)],[c75,c625]) ).
cnf(c1335,plain,
addition(X,multiplication(antidomain(Y),addition(X,Z))) = addition(X,multiplication(antidomain(Y),Z)),
inference(equational,[status(thm)],[c4,c43,c1334]) ).
cnf(c1528,plain,
addition(antidomain(X),multiplication(codomain(Y),domain(X))) = addition(antidomain(X),codomain(Y)),
inference(equational,[status(thm)],[c3,c11,c36,c999]) ).
cnf(c1550,plain,
addition(domain(X),multiplication(antidomain(Y),antidomain(X))) = addition(domain(X),antidomain(Y)),
inference(equational,[status(thm)],[c3,c36,c1335]) ).
cnf(c1891,axiom,
addition(coantidomain(multiplication(X,Y)),coantidomain(multiplication(coantidomain(coantidomain(X)),Y))) = coantidomain(multiplication(coantidomain(coantidomain(X)),Y)),
file('theBenchmark.p',codomain2) ).
cnf(c1892,plain,
addition(coantidomain(multiplication(X,Y)),coantidomain(multiplication(codomain(X),Y))) = coantidomain(multiplication(codomain(X),Y)),
inference(equational,[status(thm)],[c10,c1891]) ).
cnf(c1893,plain,
coantidomain(multiplication(codomain(antidomain(X)),X)) = one,
inference(equational,[status(thm)],[c13,c18,c32,c42,c1892]) ).
cnf(c1894,plain,
multiplication(codomain(antidomain(X)),X) = zero,
inference(equational,[status(thm)],[c3,c16,c28,c1893]) ).
cnf(c1895,plain,
codomain(antidomain(X)) = antidomain(X),
inference(equational,[status(thm)],[c2,c19,c86,c202,c1528,c1894]) ).
cnf(c1898,plain,
coantidomain(antidomain(X)) = domain(X),
inference(equational,[status(thm)],[c8,c275,c396,c1895]) ).
cnf(c2043,axiom,
addition(antidomain(multiplication(X,Y)),antidomain(multiplication(X,antidomain(antidomain(Y))))) = antidomain(multiplication(X,antidomain(antidomain(Y)))),
file('theBenchmark.p',domain2) ).
cnf(c2044,plain,
addition(antidomain(multiplication(X,Y)),antidomain(multiplication(X,domain(Y)))) = antidomain(multiplication(X,domain(Y))),
inference(equational,[status(thm)],[c8,c2043]) ).
cnf(c2060,plain,
multiplication(antidomain(multiplication(X,Y)),multiplication(X,domain(Y))) = zero,
inference(equational,[status(thm)],[c13,c54,c2044]) ).
cnf(c2073,plain,
multiplication(X,domain(multiplication(Y,coantidomain(multiplication(X,Y))))) = zero,
inference(equational,[status(thm)],[c4,c15,c37,c126,c2060]) ).
cnf(c2385,plain,
multiplication(antidomain(multiplication(X,domain(Y))),domain(multiplication(X,Y))) = zero,
inference(equational,[status(thm)],[c3,c18,c28,c32,c723,c2073]) ).
cnf(c2709,plain,
addition(antidomain(X),multiplication(antidomain(Y),domain(X))) = addition(antidomain(X),antidomain(Y)),
inference(equational,[status(thm)],[c8,c86,c1550]) ).
cnf(c2710,plain,
antidomain(multiplication(X,domain(Y))) = antidomain(multiplication(X,Y)),
inference(equational,[status(thm)],[c2,c2044,c2385,c2709]) ).
cnf(c2711,plain,
domain(multiplication(X,domain(Y))) = domain(multiplication(X,Y)),
inference(equational,[status(thm)],[c1898,c2710]) ).
cnf(g1,plain,
domain(multiplication(sK2_goals_X0,sK1_goals_X1)) = domain(multiplication(sK2_goals_X0,domain(sK1_goals_X1))),
inference(equational,[status(thm)],[c2711]) ).
cnf(g2,plain,
$false,
inference(resolution,[status(thm)],[g0,g1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KLE084-10 : TPTP v9.0.0. Released v7.5.0.
% 0.07/0.12 % Command : run_Leo-III %s %d THM
% 0.13/0.34 % Computer : n001.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Jul 14 11:13:04 EDT 2025
% 0.13/0.34 % CPUTime :
% 228.25/228.60 % SZS status Unsatisfiable
% 228.25/228.60 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------