%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : KLE090-10 : TPTP v9.0.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n016.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:50 AM UTC 2025
% Result : Unsatisfiable 9.38s 9.56s
% Output : CNFRefutation 9.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 14
% Syntax : Number of clauses : 37 ( 37 unt; 0 nHn; 12 RR)
% Number of literals : 37 ( 36 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 : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 39 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
addition(antidomain(sK1_goals_X1),antidomain(sK2_goals_X0)) != antidomain(sK2_goals_X0),
file('theBenchmark.p',goals_1) ).
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(c7,axiom,
addition(sK2_goals_X0,sK1_goals_X1) = sK1_goals_X1,
file('theBenchmark.p',goals) ).
cnf(c10,axiom,
addition(X,Y) = addition(Y,X),
file('theBenchmark.p',additive_commutativity) ).
cnf(c11,plain,
addition(zero,X) = X,
inference(equational,[status(thm)],[c2,c10]) ).
cnf(c12,axiom,
multiplication(antidomain(X),X) = zero,
file('theBenchmark.p',domain1) ).
cnf(c13,plain,
antidomain(one) = zero,
inference(equational,[status(thm)],[c3,c12]) ).
cnf(c14,axiom,
multiplication(X,coantidomain(X)) = zero,
file('theBenchmark.p',codomain1) ).
cnf(c15,plain,
zero = coantidomain(one),
inference(equational,[status(thm)],[c4,c14]) ).
cnf(c18,plain,
addition(X,coantidomain(one)) = X,
inference(equational,[status(thm)],[c2,c15]) ).
cnf(c19,plain,
addition(coantidomain(one),X) = X,
inference(equational,[status(thm)],[c11,c15]) ).
cnf(c22,axiom,
addition(X,addition(Y,Z)) = addition(addition(X,Y),Z),
file('theBenchmark.p',additive_associativity) ).
cnf(c23,plain,
addition(addition(X,Y),Z) = addition(X,addition(Y,Z)),
inference(equational,[status(thm)],[c22]) ).
cnf(c26,plain,
addition(X,addition(X,Y)) = addition(X,Y),
inference(equational,[status(thm)],[c1,c23]) ).
cnf(c27,axiom,
addition(antidomain(antidomain(X)),antidomain(X)) = one,
file('theBenchmark.p',domain3) ).
cnf(c28,plain,
addition(antidomain(X),antidomain(antidomain(X))) = one,
inference(equational,[status(thm)],[c10,c27]) ).
cnf(c29,plain,
antidomain(coantidomain(one)) = one,
inference(equational,[status(thm)],[c13,c15,c19,c28]) ).
cnf(c30,plain,
addition(one,antidomain(X)) = one,
inference(equational,[status(thm)],[c10,c26,c28]) ).
cnf(c43,axiom,
multiplication(addition(X,Y),Z) = addition(multiplication(X,Z),multiplication(Y,Z)),
file('theBenchmark.p',left_distributivity) ).
cnf(c44,plain,
addition(X,multiplication(antidomain(Y),X)) = X,
inference(equational,[status(thm)],[c4,c30,c43]) ).
cnf(c46,axiom,
multiplication(X,addition(Y,Z)) = addition(multiplication(X,Y),multiplication(X,Z)),
file('theBenchmark.p',right_distributivity) ).
cnf(c49,plain,
addition(multiplication(X,sK2_goals_X0),multiplication(X,sK1_goals_X1)) = multiplication(X,sK1_goals_X1),
inference(equational,[status(thm)],[c7,c46]) ).
cnf(c50,plain,
multiplication(antidomain(sK1_goals_X1),sK2_goals_X0) = coantidomain(one),
inference(equational,[status(thm)],[c12,c15,c18,c49]) ).
cnf(c212,plain,
addition(multiplication(X,antidomain(Y)),multiplication(X,antidomain(antidomain(Y)))) = X,
inference(equational,[status(thm)],[c3,c28,c46]) ).
cnf(c214,plain,
multiplication(antidomain(antidomain(antidomain(X))),antidomain(X)) = antidomain(antidomain(antidomain(X))),
inference(equational,[status(thm)],[c12,c15,c18,c212]) ).
cnf(c227,plain,
addition(multiplication(antidomain(X),Y),multiplication(antidomain(antidomain(X)),Y)) = Y,
inference(equational,[status(thm)],[c4,c28,c43]) ).
cnf(c228,plain,
antidomain(antidomain(antidomain(X))) = antidomain(X),
inference(equational,[status(thm)],[c12,c15,c19,c214,c227]) ).
cnf(c802,axiom,
addition(antidomain(multiplication(X,Y)),antidomain(multiplication(X,antidomain(antidomain(Y))))) = antidomain(multiplication(X,antidomain(antidomain(Y)))),
file('theBenchmark.p',domain2) ).
cnf(c808,plain,
antidomain(multiplication(antidomain(sK1_goals_X1),antidomain(antidomain(sK2_goals_X0)))) = one,
inference(equational,[status(thm)],[c29,c30,c50,c802]) ).
cnf(c809,plain,
multiplication(antidomain(sK1_goals_X1),antidomain(antidomain(sK2_goals_X0))) = coantidomain(one),
inference(equational,[status(thm)],[c4,c12,c15,c808]) ).
cnf(c810,plain,
multiplication(antidomain(sK1_goals_X1),antidomain(sK2_goals_X0)) = antidomain(sK1_goals_X1),
inference(equational,[status(thm)],[c19,c212,c228,c809]) ).
cnf(c812,plain,
addition(antidomain(sK2_goals_X0),antidomain(sK1_goals_X1)) = antidomain(sK2_goals_X0),
inference(equational,[status(thm)],[c44,c810]) ).
cnf(g1,plain,
addition(antidomain(sK1_goals_X1),antidomain(sK2_goals_X0)) = antidomain(sK2_goals_X0),
inference(equational,[status(thm)],[c10,c812]) ).
cnf(g2,plain,
$false,
inference(resolution,[status(thm)],[g0,g1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : KLE090-10 : TPTP v9.0.0. Released v7.3.0.
% 0.02/0.09 % Command : run_Leo-III %s %d THM
% 0.09/0.30 % Computer : n016.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Mon Jul 14 11:13:04 EDT 2025
% 0.09/0.30 % CPUTime :
% 9.38/9.56 % SZS status Unsatisfiable
% 9.38/9.56 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------