%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : TOP050-1 : TPTP v9.0.0. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n005.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:17 AM UTC 2025
% Result : Unsatisfiable 60.73s 60.78s
% Output : CNFRefutation 60.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 35
% Syntax : Number of clauses : 151 ( 151 unt; 0 nHn; 123 RR)
% Number of literals : 151 ( 150 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 : 34 ( 34 usr; 32 con; 0-31 aty)
% Number of variables : 34 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27) != tuple(a2,a31,a32,a3,a25,a26,a4,a29,a30,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28),
file('theBenchmark.p',goal) ).
cnf(c1,axiom,
product(X,X) = X,
file('theBenchmark.p',involutory_quandle) ).
cnf(c2,axiom,
product(a1,a31) = a2,
file('theBenchmark.p',knot) ).
cnf(c3,axiom,
product(a2,a25) = a3,
file('theBenchmark.p',knot_03) ).
cnf(c4,axiom,
product(a3,a29) = a4,
file('theBenchmark.p',knot_04) ).
cnf(c5,axiom,
product(a4,a11) = a5,
file('theBenchmark.p',knot_05) ).
cnf(c6,axiom,
product(a5,a15) = a6,
file('theBenchmark.p',knot_06) ).
cnf(c7,axiom,
product(a7,a19) = a8,
file('theBenchmark.p',knot_07) ).
cnf(c8,axiom,
product(a8,a5) = a9,
file('theBenchmark.p',knot_08) ).
cnf(c9,axiom,
product(a9,a17) = a10,
file('theBenchmark.p',knot_09) ).
cnf(c10,axiom,
product(a10,a7) = a11,
file('theBenchmark.p',knot_10) ).
cnf(c11,axiom,
product(a11,a5) = a12,
file('theBenchmark.p',knot_11) ).
cnf(c12,axiom,
product(a12,a19) = a13,
file('theBenchmark.p',knot_12) ).
cnf(c13,axiom,
product(a13,a7) = a14,
file('theBenchmark.p',knot_13) ).
cnf(c14,axiom,
product(a14,a17) = a15,
file('theBenchmark.p',knot_14) ).
cnf(c15,axiom,
product(a15,a5) = a16,
file('theBenchmark.p',knot_15) ).
cnf(c16,axiom,
product(a16,a19) = a17,
file('theBenchmark.p',knot_16) ).
cnf(c17,axiom,
product(a17,a9) = a18,
file('theBenchmark.p',knot_17) ).
cnf(c18,axiom,
product(a18,a15) = a19,
file('theBenchmark.p',knot_18) ).
cnf(c19,axiom,
product(a19,a11) = a20,
file('theBenchmark.p',knot_19) ).
cnf(c20,axiom,
product(a20,a29) = a21,
file('theBenchmark.p',knot_20) ).
cnf(c21,axiom,
product(a21,a25) = a22,
file('theBenchmark.p',knot_21) ).
cnf(c22,axiom,
product(a22,a31) = a23,
file('theBenchmark.p',knot_22) ).
cnf(c23,axiom,
product(a23,a21) = a24,
file('theBenchmark.p',knot_23) ).
cnf(c24,axiom,
product(a24,a3) = a25,
file('theBenchmark.p',knot_24) ).
cnf(c25,axiom,
product(a25,a23) = a26,
file('theBenchmark.p',knot_25) ).
cnf(c26,axiom,
product(a26,a1) = a27,
file('theBenchmark.p',knot_26) ).
cnf(c27,axiom,
product(a27,a21) = a28,
file('theBenchmark.p',knot_27) ).
cnf(c28,axiom,
product(a28,a3) = a29,
file('theBenchmark.p',knot_28) ).
cnf(c29,axiom,
product(a29,a1) = a30,
file('theBenchmark.p',knot_29) ).
cnf(c30,axiom,
product(a30,a23) = a31,
file('theBenchmark.p',knot_30) ).
cnf(c31,axiom,
product(a31,a3) = a32,
file('theBenchmark.p',knot_31) ).
cnf(c32,axiom,
product(a32,a21) = a1,
file('theBenchmark.p',knot_32) ).
cnf(c33,axiom,
product(product(X,Y),Y) = X,
file('theBenchmark.p',involutory_quandle_01) ).
cnf(c34,plain,
product(a2,a31) = a1,
inference(equational,[status(thm)],[c2,c33]) ).
cnf(c35,plain,
product(a11,a7) = a10,
inference(equational,[status(thm)],[c10,c33]) ).
cnf(c36,plain,
product(a12,a5) = a11,
inference(equational,[status(thm)],[c11,c33]) ).
cnf(c37,plain,
product(a13,a19) = a12,
inference(equational,[status(thm)],[c12,c33]) ).
cnf(c39,plain,
product(a15,a17) = a14,
inference(equational,[status(thm)],[c14,c33]) ).
cnf(c40,plain,
product(a16,a5) = a15,
inference(equational,[status(thm)],[c15,c33]) ).
cnf(c41,plain,
product(a17,a19) = a16,
inference(equational,[status(thm)],[c16,c33]) ).
cnf(c43,plain,
product(a19,a15) = a18,
inference(equational,[status(thm)],[c18,c33]) ).
cnf(c44,plain,
product(a20,a11) = a19,
inference(equational,[status(thm)],[c19,c33]) ).
cnf(c45,plain,
product(a3,a25) = a2,
inference(equational,[status(thm)],[c3,c33]) ).
cnf(c46,plain,
product(a21,a29) = a20,
inference(equational,[status(thm)],[c20,c33]) ).
cnf(c47,plain,
product(a22,a25) = a21,
inference(equational,[status(thm)],[c21,c33]) ).
cnf(c48,plain,
product(a23,a31) = a22,
inference(equational,[status(thm)],[c22,c33]) ).
cnf(c50,plain,
product(a25,a3) = a24,
inference(equational,[status(thm)],[c24,c33]) ).
cnf(c51,plain,
product(a26,a23) = a25,
inference(equational,[status(thm)],[c25,c33]) ).
cnf(c52,plain,
product(a27,a1) = a26,
inference(equational,[status(thm)],[c26,c33]) ).
cnf(c54,plain,
product(a29,a3) = a28,
inference(equational,[status(thm)],[c28,c33]) ).
cnf(c55,plain,
product(a30,a1) = a29,
inference(equational,[status(thm)],[c29,c33]) ).
cnf(c56,plain,
product(a4,a29) = a3,
inference(equational,[status(thm)],[c4,c33]) ).
cnf(c57,plain,
product(a31,a23) = a30,
inference(equational,[status(thm)],[c30,c33]) ).
cnf(c58,plain,
product(a32,a3) = a31,
inference(equational,[status(thm)],[c31,c33]) ).
cnf(c59,plain,
product(a1,a21) = a32,
inference(equational,[status(thm)],[c32,c33]) ).
cnf(c60,plain,
product(a5,a11) = a4,
inference(equational,[status(thm)],[c5,c33]) ).
cnf(c62,plain,
product(a8,a19) = a7,
inference(equational,[status(thm)],[c7,c33]) ).
cnf(c64,plain,
product(a10,a17) = a9,
inference(equational,[status(thm)],[c9,c33]) ).
cnf(c65,axiom,
product(product(X,Y),Z) = product(product(X,Z),product(Y,Z)),
file('theBenchmark.p',involutory_quandle_02) ).
cnf(c66,plain,
product(product(X,Y),product(Z,Y)) = product(product(X,Z),Y),
inference(equational,[status(thm)],[c65]) ).
cnf(c67,plain,
product(product(X,Y),X) = product(X,product(Y,X)),
inference(equational,[status(thm)],[c1,c66]) ).
cnf(c68,plain,
product(a11,a4) = product(a12,a11),
inference(equational,[status(thm)],[c11,c60,c67]) ).
cnf(c70,plain,
product(a17,a10) = product(a18,a17),
inference(equational,[status(thm)],[c9,c17,c67]) ).
cnf(c72,plain,
product(a25,a2) = product(a24,a25),
inference(equational,[status(thm)],[c45,c50,c67]) ).
cnf(c76,plain,
product(a31,a22) = product(a30,a31),
inference(equational,[status(thm)],[c48,c57,c67]) ).
cnf(c90,plain,
product(product(a19,X),a11) = product(a20,product(X,a11)),
inference(equational,[status(thm)],[c19,c66]) ).
cnf(c91,plain,
product(product(a2,X),a25) = product(a3,product(X,a25)),
inference(equational,[status(thm)],[c3,c66]) ).
cnf(c99,plain,
product(product(a27,X),a21) = product(a28,product(X,a21)),
inference(equational,[status(thm)],[c27,c66]) ).
cnf(c100,plain,
product(a28,a32) = product(a26,a21),
inference(equational,[status(thm)],[c52,c59,c99]) ).
cnf(c110,plain,
product(product(a8,X),a5) = product(a9,product(X,a5)),
inference(equational,[status(thm)],[c8,c66]) ).
cnf(c112,plain,
product(product(X,a31),a2) = product(product(X,a1),a31),
inference(equational,[status(thm)],[c2,c66]) ).
cnf(c116,plain,
product(product(X,a7),a14) = product(product(X,a13),a7),
inference(equational,[status(thm)],[c13,c66]) ).
cnf(c120,plain,
product(product(X,a17),a9) = product(product(X,a9),a18),
inference(equational,[status(thm)],[c17,c66]) ).
cnf(c121,plain,
product(product(a10,a9),a18) = a9,
inference(equational,[status(thm)],[c1,c64,c120]) ).
cnf(c123,plain,
product(product(X,a19),a11) = product(product(X,a11),a20),
inference(equational,[status(thm)],[c19,c66]) ).
cnf(c124,plain,
product(product(X,a25),a3) = product(product(X,a2),a25),
inference(equational,[status(thm)],[c3,c66]) ).
cnf(c125,plain,
product(product(X,a29),a21) = product(product(X,a20),a29),
inference(equational,[status(thm)],[c20,c66]) ).
cnf(c126,plain,
product(product(X,a21),a25) = product(product(X,a25),a22),
inference(equational,[status(thm)],[c21,c66]) ).
cnf(c128,plain,
product(product(X,a21),a24) = product(product(X,a23),a21),
inference(equational,[status(thm)],[c23,c66]) ).
cnf(c129,plain,
product(product(X,a3),a25) = product(product(X,a24),a3),
inference(equational,[status(thm)],[c24,c66]) ).
cnf(c137,plain,
product(product(X,a3),a32) = product(product(X,a31),a3),
inference(equational,[status(thm)],[c31,c66]) ).
cnf(c139,plain,
product(product(X,a11),a5) = product(product(X,a4),a11),
inference(equational,[status(thm)],[c5,c66]) ).
cnf(c144,plain,
product(product(X,a5),a9) = product(product(X,a8),a5),
inference(equational,[status(thm)],[c8,c66]) ).
cnf(c151,plain,
product(product(a16,a8),a5) = product(a15,a9),
inference(equational,[status(thm)],[c40,c144]) ).
cnf(c161,plain,
product(product(a29,a31),a3) = product(a26,a21),
inference(equational,[status(thm)],[c54,c100,c137]) ).
cnf(c197,plain,
product(product(a4,a20),a29) = product(a3,a21),
inference(equational,[status(thm)],[c56,c125]) ).
cnf(c198,plain,
product(product(a1,a23),a21) = product(a32,a24),
inference(equational,[status(thm)],[c59,c128]) ).
cnf(c232,plain,
product(product(a11,a13),a7) = product(a10,a14),
inference(equational,[status(thm)],[c35,c116]) ).
cnf(c246,plain,
product(a9,product(a19,a5)) = product(a7,a5),
inference(equational,[status(thm)],[c62,c110]) ).
cnf(c262,plain,
product(a3,product(a31,a25)) = product(a1,a25),
inference(equational,[status(thm)],[c34,c91]) ).
cnf(c274,plain,
product(a4,product(a12,a11)) = product(a5,a4),
inference(equational,[status(thm)],[c5,c67,c68]) ).
cnf(c295,plain,
product(a19,product(a11,a19)) = product(a20,a19),
inference(equational,[status(thm)],[c19,c67]) ).
cnf(c324,plain,
product(product(a24,a25),a2) = a25,
inference(equational,[status(thm)],[c33,c72]) ).
cnf(c328,plain,
product(product(a30,a31),a22) = a31,
inference(equational,[status(thm)],[c33,c76]) ).
cnf(c336,plain,
product(product(X,a25),a2) = product(product(X,a24),a3),
inference(equational,[status(thm)],[c45,c66,c129]) ).
cnf(c343,plain,
product(product(X,a5),a11) = product(product(X,a11),a4),
inference(equational,[status(thm)],[c60,c66]) ).
cnf(c351,plain,
product(product(X,a3),a24) = product(product(X,a2),a25),
inference(equational,[status(thm)],[c50,c66,c124]) ).
cnf(c356,plain,
product(product(X,a25),a21) = product(product(X,a22),a25),
inference(equational,[status(thm)],[c47,c66]) ).
cnf(c362,plain,
product(product(X,a11),a4) = product(product(X,a12),a5),
inference(equational,[status(thm)],[c36,c66,c343]) ).
cnf(c365,plain,
product(product(a32,X),a3) = product(a31,product(X,a3)),
inference(equational,[status(thm)],[c58,c66]) ).
cnf(c386,plain,
product(product(a17,X),a19) = product(a16,product(X,a19)),
inference(equational,[status(thm)],[c41,c66]) ).
cnf(c414,plain,
product(product(a32,a2),a25) = product(a31,a24),
inference(equational,[status(thm)],[c58,c351]) ).
cnf(c415,plain,
product(product(a30,a31),a25) = product(a25,a21),
inference(equational,[status(thm)],[c29,c51,c112,c128,c161,c351]) ).
cnf(c416,plain,
product(a31,a25) = a25,
inference(equational,[status(thm)],[c33,c328,c356,c415]) ).
cnf(c417,plain,
a31 = a25,
inference(equational,[status(thm)],[c1,c33,c416]) ).
cnf(c418,plain,
a30 = a26,
inference(equational,[status(thm)],[c25,c57,c417]) ).
cnf(c419,plain,
a3 = a1,
inference(equational,[status(thm)],[c3,c34,c417]) ).
cnf(c420,plain,
a24 = a32,
inference(equational,[status(thm)],[c31,c50,c417]) ).
cnf(c421,plain,
a21 = a23,
inference(equational,[status(thm)],[c22,c47,c417]) ).
cnf(c422,plain,
a1 = a32,
inference(equational,[status(thm)],[c1,c33,c198,c420,c421]) ).
cnf(c423,plain,
a23 = a32,
inference(equational,[status(thm)],[c1,c23,c420,c421]) ).
cnf(c424,plain,
a29 = a27,
inference(equational,[status(thm)],[c26,c55,c418]) ).
cnf(c425,plain,
a28 = a26,
inference(equational,[status(thm)],[c29,c54,c418,c419]) ).
cnf(c426,plain,
product(a25,a22) = product(a26,a25),
inference(equational,[status(thm)],[c1,c33,c126,c415,c417,c418]) ).
cnf(c427,plain,
product(a25,a32) = a26,
inference(equational,[status(thm)],[c33,c47,c67,c421,c423,c426]) ).
cnf(c428,plain,
product(a32,a25) = a2,
inference(equational,[status(thm)],[c45,c262,c416,c422]) ).
cnf(c429,plain,
a2 = a32,
inference(equational,[status(thm)],[c1,c336,c419,c420,c422,c428]) ).
cnf(c430,plain,
a26 = a32,
inference(equational,[status(thm)],[c1,c414,c417,c420,c427,c428,c429]) ).
cnf(c431,plain,
a25 = a32,
inference(equational,[status(thm)],[c1,c324,c420,c428,c429]) ).
cnf(c432,plain,
a22 = a32,
inference(equational,[status(thm)],[c1,c21,c421,c423,c431]) ).
cnf(c433,plain,
a27 = a32,
inference(equational,[status(thm)],[c1,c26,c422,c430]) ).
cnf(c434,plain,
a20 = a32,
inference(equational,[status(thm)],[c1,c46,c421,c423,c424,c433]) ).
cnf(c435,plain,
a4 = a32,
inference(equational,[status(thm)],[c1,c33,c197,c419,c421,c422,c423,c424,c433,c434]) ).
cnf(c472,plain,
product(a32,product(a11,a32)) = product(a19,a32),
inference(equational,[status(thm)],[c1,c44,c90,c123,c295,c434]) ).
cnf(c473,plain,
product(a32,a11) = a19,
inference(equational,[status(thm)],[c33,c365,c417,c419,c422,c431,c472]) ).
cnf(c474,plain,
product(a19,a5) = a19,
inference(equational,[status(thm)],[c1,c139,c435,c473]) ).
cnf(c477,plain,
product(a9,a19) = product(a7,a5),
inference(equational,[status(thm)],[c246,c474]) ).
cnf(c482,plain,
product(a16,product(a7,a5)) = product(a18,a19),
inference(equational,[status(thm)],[c17,c386,c477]) ).
cnf(c488,plain,
product(product(a32,a12),a5) = product(a5,a32),
inference(equational,[status(thm)],[c67,c68,c274,c362,c435]) ).
cnf(c489,plain,
product(a5,a32) = product(a19,a32),
inference(equational,[status(thm)],[c44,c362,c434,c435,c488]) ).
cnf(c490,plain,
a5 = a19,
inference(equational,[status(thm)],[c33,c489]) ).
cnf(c491,plain,
a17 = a15,
inference(equational,[status(thm)],[c16,c40,c490]) ).
cnf(c492,plain,
a11 = a13,
inference(equational,[status(thm)],[c12,c36,c490]) ).
cnf(c493,plain,
a9 = a7,
inference(equational,[status(thm)],[c8,c62,c490]) ).
cnf(c494,plain,
a18 = a6,
inference(equational,[status(thm)],[c6,c43,c490]) ).
cnf(c495,plain,
a15 = a14,
inference(equational,[status(thm)],[c1,c39,c491]) ).
cnf(c496,plain,
a14 = a10,
inference(equational,[status(thm)],[c13,c35,c492]) ).
cnf(c499,plain,
product(a16,a8) = product(a6,a19),
inference(equational,[status(thm)],[c7,c482,c490,c494]) ).
cnf(c500,plain,
a13 = a6,
inference(equational,[status(thm)],[c10,c33,c151,c490,c492,c493,c495,c496,c499]) ).
cnf(c501,plain,
product(a19,a6) = a32,
inference(equational,[status(thm)],[c19,c434,c492,c500]) ).
cnf(c503,plain,
a7 = a6,
inference(equational,[status(thm)],[c1,c10,c121,c492,c493,c494,c500]) ).
cnf(c504,plain,
a10 = a6,
inference(equational,[status(thm)],[c1,c232,c492,c496,c500,c503]) ).
cnf(c505,plain,
product(a6,a19) = a16,
inference(equational,[status(thm)],[c41,c491,c495,c496,c504]) ).
cnf(c506,plain,
a19 = a6,
inference(equational,[status(thm)],[c1,c18,c70,c491,c495,c496,c504]) ).
cnf(c507,plain,
a16 = a6,
inference(equational,[status(thm)],[c1,c505,c506]) ).
cnf(c508,plain,
a6 = a32,
inference(equational,[status(thm)],[c1,c501,c506]) ).
cnf(c509,plain,
a12 = a32,
inference(equational,[status(thm)],[c1,c37,c500,c506,c508]) ).
cnf(c510,plain,
a8 = a32,
inference(equational,[status(thm)],[c1,c7,c503,c506,c508]) ).
cnf(g1,plain,
tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27) = tuple(a2,a31,a32,a3,a25,a26,a4,a29,a30,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28),
inference(equational,[status(thm)],[c417,c418,c419,c420,c421,c422,c423,c424,c425,c429,c430,c431,c432,c433,c434,c435,c490,c491,c492,c493,c494,c495,c496,c500,c503,c504,c506,c507,c508,c509,c510]) ).
cnf(g2,plain,
$false,
inference(resolution,[status(thm)],[g0,g1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : TOP050-1 : TPTP v9.0.0. Released v8.1.0.
% 0.08/0.14 % Command : run_Leo-III %s %d THM
% 0.14/0.36 % Computer : n005.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Mon Jul 14 23:31:34 EDT 2025
% 0.14/0.36 % CPUTime :
% 60.73/60.78 % SZS status Unsatisfiable
% 60.73/60.78 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------