%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : TOP053-1 : TPTP v9.0.0. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n011.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 08:44:28 AM UTC 2025
% Result : Unsatisfiable 60.28s 60.43s
% Output : CNFRefutation 60.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 19
% Syntax : Number of clauses : 82 ( 82 unt; 0 nHn; 66 RR)
% Number of literals : 82 ( 81 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 15 con; 0-14 aty)
% Number of variables : 22 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14) != tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15),
file('theBenchmark.p',goal) ).
cnf(c1,axiom,
product(X,X) = X,
file('theBenchmark.p',involutory_quandle) ).
cnf(c2,axiom,
product(a1,a2) = a3,
file('theBenchmark.p',knot) ).
cnf(c3,axiom,
product(a3,a4) = a5,
file('theBenchmark.p',knot_03) ).
cnf(c4,axiom,
product(a5,a6) = a7,
file('theBenchmark.p',knot_04) ).
cnf(c5,axiom,
product(a7,a3) = a8,
file('theBenchmark.p',knot_05) ).
cnf(c6,axiom,
product(a8,a2) = a9,
file('theBenchmark.p',knot_06) ).
cnf(c7,axiom,
product(a9,a1) = a10,
file('theBenchmark.p',knot_07) ).
cnf(c8,axiom,
product(a10,a11) = a12,
file('theBenchmark.p',knot_08) ).
cnf(c9,axiom,
product(a12,a3) = a13,
file('theBenchmark.p',knot_09) ).
cnf(c10,axiom,
product(a13,a8) = a6,
file('theBenchmark.p',knot_10) ).
cnf(c11,axiom,
product(a6,a7) = a2,
file('theBenchmark.p',knot_11) ).
cnf(c12,axiom,
product(a2,a12) = a14,
file('theBenchmark.p',knot_12) ).
cnf(c13,axiom,
product(a14,a3) = a15,
file('theBenchmark.p',knot_13) ).
cnf(c14,axiom,
product(a15,a8) = a4,
file('theBenchmark.p',knot_14) ).
cnf(c15,axiom,
product(a4,a7) = a11,
file('theBenchmark.p',knot_15) ).
cnf(c16,axiom,
product(a11,a10) = a1,
file('theBenchmark.p',knot_16) ).
cnf(c17,axiom,
product(product(X,Y),Y) = X,
file('theBenchmark.p',involutory_quandle_01) ).
cnf(c18,plain,
product(a3,a2) = a1,
inference(equational,[status(thm)],[c2,c17]) ).
cnf(c20,plain,
product(a1,a10) = a11,
inference(equational,[status(thm)],[c16,c17]) ).
cnf(c21,plain,
product(a13,a3) = a12,
inference(equational,[status(thm)],[c9,c17]) ).
cnf(c24,plain,
product(a4,a8) = a15,
inference(equational,[status(thm)],[c14,c17]) ).
cnf(c26,plain,
product(a5,a4) = a3,
inference(equational,[status(thm)],[c3,c17]) ).
cnf(c27,plain,
product(a11,a7) = a4,
inference(equational,[status(thm)],[c15,c17]) ).
cnf(c28,plain,
product(a7,a6) = a5,
inference(equational,[status(thm)],[c4,c17]) ).
cnf(c29,plain,
product(a2,a7) = a6,
inference(equational,[status(thm)],[c11,c17]) ).
cnf(c30,plain,
product(a8,a3) = a7,
inference(equational,[status(thm)],[c5,c17]) ).
cnf(c31,plain,
product(a9,a2) = a8,
inference(equational,[status(thm)],[c6,c17]) ).
cnf(c32,plain,
product(a10,a1) = a9,
inference(equational,[status(thm)],[c7,c17]) ).
cnf(c33,axiom,
product(product(X,Y),Z) = product(product(X,Z),product(Y,Z)),
file('theBenchmark.p',involutory_quandle_02) ).
cnf(c34,plain,
product(product(X,Y),product(Z,Y)) = product(product(X,Z),Y),
inference(equational,[status(thm)],[c33]) ).
cnf(c35,plain,
product(product(X,Y),X) = product(X,product(Y,X)),
inference(equational,[status(thm)],[c1,c34]) ).
cnf(c41,plain,
product(a7,a2) = product(a5,a7),
inference(equational,[status(thm)],[c11,c28,c35]) ).
cnf(c47,plain,
product(product(a14,X),a3) = product(a15,product(X,a3)),
inference(equational,[status(thm)],[c13,c34]) ).
cnf(c53,plain,
product(product(a5,X),a6) = product(a7,product(X,a6)),
inference(equational,[status(thm)],[c4,c34]) ).
cnf(c56,plain,
product(product(a8,X),a2) = product(a9,product(X,a2)),
inference(equational,[status(thm)],[c6,c34]) ).
cnf(c57,plain,
product(a5,a7) = a10,
inference(equational,[status(thm)],[c7,c18,c30,c41,c56]) ).
cnf(c59,plain,
product(a7,a5) = product(a10,a6),
inference(equational,[status(thm)],[c28,c53,c57]) ).
cnf(c64,plain,
product(product(X,a11),a12) = product(product(X,a10),a11),
inference(equational,[status(thm)],[c8,c34]) ).
cnf(c68,plain,
product(product(X,a8),a6) = product(product(X,a13),a8),
inference(equational,[status(thm)],[c10,c34]) ).
cnf(c70,plain,
product(product(X,a8),a4) = product(product(X,a15),a8),
inference(equational,[status(thm)],[c14,c34]) ).
cnf(c71,plain,
product(product(X,a2),a12) = product(product(X,a12),a14),
inference(equational,[status(thm)],[c12,c34]) ).
cnf(c73,plain,
product(product(X,a7),a11) = product(product(X,a4),a7),
inference(equational,[status(thm)],[c15,c34]) ).
cnf(c74,plain,
product(a3,a7) = a12,
inference(equational,[status(thm)],[c8,c26,c57,c73]) ).
cnf(c75,plain,
product(a3,a8) = a13,
inference(equational,[status(thm)],[c5,c9,c35,c74]) ).
cnf(c76,plain,
a3 = a6,
inference(equational,[status(thm)],[c10,c17,c75]) ).
cnf(c77,plain,
a2 = a12,
inference(equational,[status(thm)],[c11,c74,c76]) ).
cnf(c78,plain,
a8 = a5,
inference(equational,[status(thm)],[c5,c28,c76]) ).
cnf(c79,plain,
a12 = a14,
inference(equational,[status(thm)],[c1,c12,c77]) ).
cnf(c80,plain,
product(a14,a7) = a6,
inference(equational,[status(thm)],[c17,c74,c76,c79]) ).
cnf(c81,plain,
product(a15,a5) = a6,
inference(equational,[status(thm)],[c1,c28,c47,c76,c80]) ).
cnf(c82,plain,
product(product(X,a6),a7) = product(product(X,a5),a6),
inference(equational,[status(thm)],[c4,c34]) ).
cnf(c83,plain,
product(a7,a14) = a10,
inference(equational,[status(thm)],[c11,c17,c35,c59,c77,c79,c82]) ).
cnf(c85,plain,
product(product(X,a7),a14) = product(product(X,a5),a6),
inference(equational,[status(thm)],[c11,c34,c77,c79,c82]) ).
cnf(c86,plain,
product(product(X,a7),a6) = product(product(X,a6),a5),
inference(equational,[status(thm)],[c5,c34,c76,c78]) ).
cnf(c87,plain,
product(a6,a5) = product(a14,a6),
inference(equational,[status(thm)],[c1,c11,c77,c79,c86]) ).
cnf(c91,plain,
product(a14,a6) = a15,
inference(equational,[status(thm)],[c17,c81,c87]) ).
cnf(c93,plain,
a13 = a15,
inference(equational,[status(thm)],[c9,c76,c79,c91]) ).
cnf(c94,plain,
product(a15,a6) = a14,
inference(equational,[status(thm)],[c21,c76,c79,c93]) ).
cnf(c95,plain,
product(a6,a14) = a1,
inference(equational,[status(thm)],[c18,c76,c77,c79]) ).
cnf(c102,plain,
product(product(a4,a15),a5) = a14,
inference(equational,[status(thm)],[c24,c68,c78,c93,c94]) ).
cnf(c103,plain,
product(a4,a15) = product(a14,a5),
inference(equational,[status(thm)],[c17,c102]) ).
cnf(c106,plain,
product(a5,a14) = a9,
inference(equational,[status(thm)],[c17,c31,c71,c78,c79]) ).
cnf(c107,plain,
product(a9,a14) = a5,
inference(equational,[status(thm)],[c17,c106]) ).
cnf(c108,plain,
product(a7,a15) = product(a9,a6),
inference(equational,[status(thm)],[c53,c91,c106]) ).
cnf(c109,plain,
product(a15,a4) = a14,
inference(equational,[status(thm)],[c17,c24,c70,c78,c103]) ).
cnf(c112,plain,
product(product(a14,a5),a6) = a1,
inference(equational,[status(thm)],[c29,c77,c79,c85,c95]) ).
cnf(c113,plain,
product(a1,a7) = a15,
inference(equational,[status(thm)],[c17,c82,c91,c112]) ).
cnf(c114,plain,
product(a14,a5) = product(a1,a6),
inference(equational,[status(thm)],[c17,c112]) ).
cnf(c115,plain,
product(a15,a7) = a1,
inference(equational,[status(thm)],[c4,c17,c47,c76,c114]) ).
cnf(c118,plain,
product(a1,a11) = a6,
inference(equational,[status(thm)],[c73,c80,c109,c115]) ).
cnf(c119,plain,
a11 = a1,
inference(equational,[status(thm)],[c1,c20,c64,c79,c95,c118]) ).
cnf(c120,plain,
a6 = a1,
inference(equational,[status(thm)],[c1,c118,c119]) ).
cnf(c121,plain,
a4 = a15,
inference(equational,[status(thm)],[c27,c113,c119]) ).
cnf(c122,plain,
a9 = a14,
inference(equational,[status(thm)],[c8,c32,c79,c119]) ).
cnf(c123,plain,
a5 = a14,
inference(equational,[status(thm)],[c1,c107,c122]) ).
cnf(c124,plain,
a1 = a15,
inference(equational,[status(thm)],[c1,c103,c114,c120,c121]) ).
cnf(c125,plain,
a14 = a15,
inference(equational,[status(thm)],[c1,c109,c121]) ).
cnf(c126,plain,
a10 = a15,
inference(equational,[status(thm)],[c1,c83,c108,c120,c122,c124,c125]) ).
cnf(c127,plain,
a7 = a15,
inference(equational,[status(thm)],[c1,c17,c41,c77,c79,c115,c123,c124,c125]) ).
cnf(g1,plain,
tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14) = tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15),
inference(equational,[status(thm)],[c76,c77,c78,c79,c93,c119,c120,c121,c122,c123,c124,c125,c126,c127]) ).
cnf(g2,plain,
$false,
inference(resolution,[status(thm)],[g0,g1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.11 % Problem : TOP053-1 : TPTP v9.0.0. Released v8.1.0.
% 0.04/0.11 % Command : run_Leo-III %s %d THM
% 0.11/0.32 % Computer : n011.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Mon Jul 14 23:31:19 EDT 2025
% 0.11/0.32 % CPUTime :
% 60.28/60.43 % SZS status Unsatisfiable
% 60.28/60.43 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------