%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : TOP050-1 : TPTP v9.2.0. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.0JJZVdxu53 true
% Computer : n020.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 : Thu Oct 2 05:08:49 PM UTC 2025
% Result : Unsatisfiable 37.49s 6.00s
% Output : Refutation 37.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : TOP050-1 : TPTP v9.2.0. Released v8.1.0.
% 0.07/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.0JJZVdxu53 true
% 0.14/0.35 % Computer : n020.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Oct 1 15:42:23 EDT 2025
% 0.14/0.35 % CPUTime :
% 0.14/0.35 % Running portfolio for 300 s
% 0.14/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.35 % Number of cores: 8
% 0.14/0.35 % Python version: Python 3.6.8
% 0.14/0.35 % Running in FO mode
% 0.56/0.66 % Total configuration time : 435
% 0.56/0.66 % Estimated wc time : 1092
% 0.56/0.66 % Estimated cpu time (7 cpus) : 156.0
% 0.58/0.76 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.58/0.77 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.58/0.77 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.58/0.78 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.58/0.78 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.58/0.79 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.58/0.79 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.60/0.83 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 37.49/6.00 % Solved by fo/fo1_av.sh.
% 37.49/6.00 % done 1211 iterations in 5.177s
% 37.49/6.00 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 37.49/6.00 % SZS output start Refutation
% 37.49/6.00 thf(a25_type, type, a25: $i).
% 37.49/6.00 thf(a4_type, type, a4: $i).
% 37.49/6.00 thf(a14_type, type, a14: $i).
% 37.49/6.00 thf(a20_type, type, a20: $i).
% 37.49/6.00 thf(a19_type, type, a19: $i).
% 37.49/6.00 thf(a17_type, type, a17: $i).
% 37.49/6.00 thf(a32_type, type, a32: $i).
% 37.49/6.00 thf(a5_type, type, a5: $i).
% 37.49/6.00 thf(a2_type, type, a2: $i).
% 37.49/6.00 thf(a16_type, type, a16: $i).
% 37.49/6.00 thf(a31_type, type, a31: $i).
% 37.49/6.00 thf(a12_type, type, a12: $i).
% 37.49/6.00 thf(a13_type, type, a13: $i).
% 37.49/6.00 thf(a22_type, type, a22: $i).
% 37.49/6.00 thf(a30_type, type, a30: $i).
% 37.49/6.00 thf(a23_type, type, a23: $i).
% 37.49/6.00 thf(a9_type, type, a9: $i).
% 37.49/6.00 thf(product_type, type, product: $i > $i > $i).
% 37.49/6.00 thf(a10_type, type, a10: $i).
% 37.49/6.00 thf(a24_type, type, a24: $i).
% 37.49/6.00 thf(a8_type, type, a8: $i).
% 37.49/6.00 thf(a21_type, type, a21: $i).
% 37.49/6.00 thf(a27_type, type, a27: $i).
% 37.49/6.00 thf(tuple_type, type, tuple: $i > $i > $i > $i > $i > $i > $i > $i > $i >
% 37.49/6.00 $i > $i > $i > $i > $i > $i > $i > $i > $i >
% 37.49/6.00 $i > $i > $i > $i > $i > $i > $i > $i > $i >
% 37.49/6.00 $i > $i > $i > $i > $i).
% 37.49/6.00 thf(a18_type, type, a18: $i).
% 37.49/6.00 thf(a6_type, type, a6: $i).
% 37.49/6.00 thf(a26_type, type, a26: $i).
% 37.49/6.00 thf(a29_type, type, a29: $i).
% 37.49/6.00 thf(a28_type, type, a28: $i).
% 37.49/6.00 thf(a3_type, type, a3: $i).
% 37.49/6.00 thf(a1_type, type, a1: $i).
% 37.49/6.00 thf(a15_type, type, a15: $i).
% 37.49/6.00 thf(a7_type, type, a7: $i).
% 37.49/6.00 thf(a11_type, type, a11: $i).
% 37.49/6.00 thf(goal, conjecture,
% 37.49/6.00 (( tuple @
% 37.49/6.00 a1 @ a30 @ a31 @ a2 @ a24 @ a25 @ a3 @ a28 @ a29 @ a4 @ a10 @ a11 @
% 37.49/6.00 a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @ a12 @
% 37.49/6.00 a13 @ a20 @ a21 @ a22 @ a23 @ a26 @ a27 ) =
% 37.49/6.00 ( tuple @
% 37.49/6.00 a2 @ a31 @ a32 @ a3 @ a25 @ a26 @ a4 @ a29 @ a30 @ a5 @ a11 @ a12 @
% 37.49/6.00 a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @ a17 @ a18 @ a13 @
% 37.49/6.00 a14 @ a21 @ a22 @ a23 @ a24 @ a27 @ a28 ))).
% 37.49/6.00 thf(zf_stmt_0, negated_conjecture,
% 37.49/6.00 (( tuple @
% 37.49/6.00 a1 @ a30 @ a31 @ a2 @ a24 @ a25 @ a3 @ a28 @ a29 @ a4 @ a10 @ a11 @
% 37.49/6.00 a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @ a12 @
% 37.49/6.00 a13 @ a20 @ a21 @ a22 @ a23 @ a26 @ a27 ) !=
% 37.49/6.00 ( tuple @
% 37.49/6.00 a2 @ a31 @ a32 @ a3 @ a25 @ a26 @ a4 @ a29 @ a30 @ a5 @ a11 @ a12 @
% 37.49/6.00 a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @ a17 @ a18 @ a13 @
% 37.49/6.00 a14 @ a21 @ a22 @ a23 @ a24 @ a27 @ a28 )),
% 37.49/6.00 inference('cnf.neg', [status(esa)], [goal])).
% 37.49/6.00 thf(zip_derived_cl34, plain,
% 37.49/6.00 (((tuple @ a1 @ a30 @ a31 @ a2 @ a24 @ a25 @ a3 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a21 @ a22 @ a23 @ a26 @ a27)
% 37.49/6.00 != (tuple @ a2 @ a31 @ a32 @ a3 @ a25 @ a26 @ a4 @ a29 @ a30 @ a5 @
% 37.49/6.00 a11 @ a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @
% 37.49/6.00 a17 @ a18 @ a13 @ a14 @ a21 @ a22 @ a23 @ a24 @ a27 @ a28))),
% 37.49/6.00 inference('cnf', [status(esa)], [zf_stmt_0])).
% 37.49/6.00 thf(knot_26, axiom, (( product @ a26 @ a1 ) = ( a27 ))).
% 37.49/6.00 thf(zip_derived_cl27, plain, (((product @ a26 @ a1) = (a27))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_26])).
% 37.49/6.00 thf(involutory_quandle_01, axiom,
% 37.49/6.00 (( product @ ( product @ X @ Y ) @ Y ) = ( X ))).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl122, plain, (((product @ a27 @ a1) = (a26))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl27, zip_derived_cl1])).
% 37.49/6.00 thf(knot_27, axiom, (( product @ a27 @ a21 ) = ( a28 ))).
% 37.49/6.00 thf(zip_derived_cl28, plain, (((product @ a27 @ a21) = (a28))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_27])).
% 37.49/6.00 thf(involutory_quandle_02, axiom,
% 37.49/6.00 (( product @ ( product @ X @ Y ) @ Z ) =
% 37.49/6.00 ( product @ ( product @ X @ Z ) @ ( product @ Y @ Z ) ))).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl126, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ a27 @ X0) @ a21)
% 37.49/6.00 = (product @ a28 @ (product @ X0 @ a21)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl28, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl10300, plain,
% 37.49/6.00 (((product @ a26 @ a21) = (product @ a28 @ (product @ a1 @ a21)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl122, zip_derived_cl126])).
% 37.49/6.00 thf(knot_32, axiom, (( product @ a32 @ a21 ) = ( a1 ))).
% 37.49/6.00 thf(zip_derived_cl33, plain, (((product @ a32 @ a21) = (a1))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_32])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl140, plain, (((product @ a1 @ a21) = (a32))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl33, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl10305, plain,
% 37.49/6.00 (((product @ a26 @ a21) = (product @ a28 @ a32))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl10300, zip_derived_cl140])).
% 37.49/6.00 thf(knot_28, axiom, (( product @ a28 @ a3 ) = ( a29 ))).
% 37.49/6.00 thf(zip_derived_cl29, plain, (((product @ a28 @ a3) = (a29))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_28])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl129, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ a28 @ X0) @ a3)
% 37.49/6.00 = (product @ a29 @ (product @ X0 @ a3)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl29, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl10546, plain,
% 37.49/6.00 (((product @ (product @ a26 @ a21) @ a3)
% 37.49/6.00 = (product @ a29 @ (product @ a32 @ a3)))),
% 37.49/6.00 inference('s_sup+', [status(thm)],
% 37.49/6.00 [zip_derived_cl10305, zip_derived_cl129])).
% 37.49/6.00 thf(knot_31, axiom, (( product @ a31 @ a3 ) = ( a32 ))).
% 37.49/6.00 thf(zip_derived_cl32, plain, (((product @ a31 @ a3) = (a32))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_31])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl137, plain, (((product @ a32 @ a3) = (a31))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl32, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl10552, plain,
% 37.49/6.00 (((product @ (product @ a26 @ a21) @ a3) = (product @ a29 @ a31))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl10546, zip_derived_cl137])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl10581, plain,
% 37.49/6.00 (((product @ (product @ a29 @ a31) @ a3) = (product @ a26 @ a21))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl10552, zip_derived_cl1])).
% 37.49/6.00 thf(knot_24, axiom, (( product @ a24 @ a3 ) = ( a25 ))).
% 37.49/6.00 thf(zip_derived_cl25, plain, (((product @ a24 @ a3) = (a25))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_24])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl60, plain, (((product @ a25 @ a3) = (a24))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl25, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl211, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ a25) @ a3)
% 37.49/6.00 = (product @ (product @ X0 @ a3) @ a24))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl60, zip_derived_cl2])).
% 37.49/6.00 thf(knot_03, axiom, (( product @ a2 @ a25 ) = ( a3 ))).
% 37.49/6.00 thf(zip_derived_cl4, plain, (((product @ a2 @ a25) = (a3))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_03])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl69, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ a2) @ a25)
% 37.49/6.00 = (product @ (product @ X0 @ a25) @ a3))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl4, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl17202, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ a2) @ a25)
% 37.49/6.00 = (product @ (product @ X0 @ a3) @ a24))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl211, zip_derived_cl69])).
% 37.49/6.00 thf(zip_derived_cl17245, plain,
% 37.49/6.00 (((product @ (product @ (product @ a29 @ a31) @ a2) @ a25)
% 37.49/6.00 = (product @ (product @ a26 @ a21) @ a24))),
% 37.49/6.00 inference('s_sup+', [status(thm)],
% 37.49/6.00 [zip_derived_cl10581, zip_derived_cl17202])).
% 37.49/6.00 thf(knot_30, axiom, (( product @ a30 @ a23 ) = ( a31 ))).
% 37.49/6.00 thf(zip_derived_cl31, plain, (((product @ a30 @ a23) = (a31))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_30])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl134, plain, (((product @ a31 @ a23) = (a30))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl31, zip_derived_cl1])).
% 37.49/6.00 thf(involutory_quandle, axiom, (( product @ X @ X ) = ( X ))).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl91, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X1) @ X0)
% 37.49/6.00 = (product @ X0 @ (product @ X1 @ X0)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl912, plain,
% 37.49/6.00 (((product @ a30 @ a31) = (product @ a31 @ (product @ a23 @ a31)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl134, zip_derived_cl91])).
% 37.49/6.00 thf(knot_22, axiom, (( product @ a22 @ a31 ) = ( a23 ))).
% 37.49/6.00 thf(zip_derived_cl23, plain, (((product @ a22 @ a31) = (a23))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_22])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl58, plain, (((product @ a23 @ a31) = (a22))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl23, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl978, plain,
% 37.49/6.00 (((product @ a30 @ a31) = (product @ a31 @ a22))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl912, zip_derived_cl58])).
% 37.49/6.00 thf(knot, axiom, (( product @ a1 @ a31 ) = ( a2 ))).
% 37.49/6.00 thf(zip_derived_cl3, plain, (((product @ a1 @ a31) = (a2))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl68, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ a1) @ a31)
% 37.49/6.00 = (product @ (product @ X0 @ a31) @ a2))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl3, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl1010, plain,
% 37.49/6.00 (((product @ (product @ a30 @ a1) @ a31)
% 37.49/6.00 = (product @ (product @ a31 @ a22) @ a2))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl978, zip_derived_cl68])).
% 37.49/6.00 thf(knot_29, axiom, (( product @ a29 @ a1 ) = ( a30 ))).
% 37.49/6.00 thf(zip_derived_cl30, plain, (((product @ a29 @ a1) = (a30))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_29])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl131, plain, (((product @ a30 @ a1) = (a29))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl30, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl1011, plain,
% 37.49/6.00 (((product @ a29 @ a31) = (product @ (product @ a31 @ a22) @ a2))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl1010, zip_derived_cl131])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl2940, plain,
% 37.49/6.00 (((product @ (product @ a29 @ a31) @ a2) = (product @ a31 @ a22))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl1011, zip_derived_cl1])).
% 37.49/6.00 thf(knot_21, axiom, (( product @ a21 @ a25 ) = ( a22 ))).
% 37.49/6.00 thf(zip_derived_cl22, plain, (((product @ a21 @ a25) = (a22))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_21])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl57, plain, (((product @ a22 @ a25) = (a21))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl22, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl202, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ a22) @ a25)
% 37.49/6.00 = (product @ (product @ X0 @ a25) @ a21))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl57, zip_derived_cl2])).
% 37.49/6.00 thf(knot_25, axiom, (( product @ a25 @ a23 ) = ( a26 ))).
% 37.49/6.00 thf(zip_derived_cl26, plain, (((product @ a25 @ a23) = (a26))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_25])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl119, plain, (((product @ a26 @ a23) = (a25))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl26, zip_derived_cl1])).
% 37.49/6.00 thf(knot_23, axiom, (( product @ a23 @ a21 ) = ( a24 ))).
% 37.49/6.00 thf(zip_derived_cl24, plain, (((product @ a23 @ a21) = (a24))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_23])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl89, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ a23) @ a21)
% 37.49/6.00 = (product @ (product @ X0 @ a21) @ a24))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl24, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl4845, plain,
% 37.49/6.00 (((product @ a25 @ a21) = (product @ (product @ a26 @ a21) @ a24))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl119, zip_derived_cl89])).
% 37.49/6.00 thf(zip_derived_cl17281, plain,
% 37.49/6.00 (((product @ (product @ a31 @ a25) @ a21) = (product @ a25 @ a21))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17245, zip_derived_cl2940, zip_derived_cl202,
% 37.49/6.00 zip_derived_cl4845])).
% 37.49/6.00 thf(zip_derived_cl91, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X1) @ X0)
% 37.49/6.00 = (product @ X0 @ (product @ X1 @ X0)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl873, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ (product @ X1 @ X0)) @ X0)
% 37.49/6.00 = (product @ X0 @ X1))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl91, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl17351, plain,
% 37.49/6.00 (((product @ (product @ a21 @ (product @ a25 @ a21)) @ a21)
% 37.49/6.00 = (product @ a21 @ (product @ a31 @ a25)))),
% 37.49/6.00 inference('s_sup+', [status(thm)],
% 37.49/6.00 [zip_derived_cl17281, zip_derived_cl873])).
% 37.49/6.00 thf(zip_derived_cl22, plain, (((product @ a21 @ a25) = (a22))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_21])).
% 37.49/6.00 thf(zip_derived_cl91, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X1) @ X0)
% 37.49/6.00 = (product @ X0 @ (product @ X1 @ X0)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl953, plain,
% 37.49/6.00 (((product @ a22 @ a21) = (product @ a21 @ (product @ a25 @ a21)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl22, zip_derived_cl91])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl23, plain, (((product @ a22 @ a31) = (a23))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_22])).
% 37.49/6.00 thf(zip_derived_cl57, plain, (((product @ a22 @ a25) = (a21))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl22, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl201, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ a22 @ X0) @ a25)
% 37.49/6.00 = (product @ a21 @ (product @ X0 @ a25)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl57, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl16527, plain,
% 37.49/6.00 (((product @ a23 @ a25) = (product @ a21 @ (product @ a31 @ a25)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl23, zip_derived_cl201])).
% 37.49/6.00 thf(zip_derived_cl17367, plain, (((a22) = (product @ a23 @ a25))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17351, zip_derived_cl953, zip_derived_cl1,
% 37.49/6.00 zip_derived_cl16527])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl17408, plain, (((product @ a22 @ a25) = (a23))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl17367, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl57, plain, (((product @ a22 @ a25) = (a21))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl22, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl17424, plain, (((a21) = (a23))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl17408, zip_derived_cl57])).
% 37.49/6.00 thf(zip_derived_cl17424, plain, (((a21) = (a23))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl17408, zip_derived_cl57])).
% 37.49/6.00 thf(zip_derived_cl17434, plain,
% 37.49/6.00 (((tuple @ a1 @ a30 @ a31 @ a2 @ a24 @ a25 @ a3 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a21 @ a22 @ a21 @ a26 @ a27)
% 37.49/6.00 != (tuple @ a2 @ a31 @ a32 @ a3 @ a25 @ a26 @ a4 @ a29 @ a30 @ a5 @
% 37.49/6.00 a11 @ a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @
% 37.49/6.00 a17 @ a18 @ a13 @ a14 @ a21 @ a22 @ a21 @ a24 @ a27 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl34, zip_derived_cl17424, zip_derived_cl17424])).
% 37.49/6.00 thf(zip_derived_cl24, plain, (((product @ a23 @ a21) = (a24))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_23])).
% 37.49/6.00 thf(zip_derived_cl17424, plain, (((a21) = (a23))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl17408, zip_derived_cl57])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl17431, plain, (((a21) = (a24))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24, zip_derived_cl17424, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl17431, plain, (((a21) = (a24))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24, zip_derived_cl17424, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl17539, plain,
% 37.49/6.00 (((tuple @ a1 @ a30 @ a31 @ a2 @ a21 @ a25 @ a3 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a21 @ a22 @ a21 @ a26 @ a27)
% 37.49/6.00 != (tuple @ a2 @ a31 @ a32 @ a3 @ a25 @ a26 @ a4 @ a29 @ a30 @ a5 @
% 37.49/6.00 a11 @ a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @
% 37.49/6.00 a17 @ a18 @ a13 @ a14 @ a21 @ a22 @ a21 @ a21 @ a27 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17434, zip_derived_cl17431, zip_derived_cl17431])).
% 37.49/6.00 thf(zip_derived_cl134, plain, (((product @ a31 @ a23) = (a30))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl31, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl26, plain, (((product @ a25 @ a23) = (a26))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_25])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl121, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ a25) @ a23)
% 37.49/6.00 = (product @ (product @ X0 @ a23) @ a26))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl26, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl9900, plain,
% 37.49/6.00 (((product @ (product @ a31 @ a25) @ a23) = (product @ a30 @ a26))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl134, zip_derived_cl121])).
% 37.49/6.00 thf(zip_derived_cl17281, plain,
% 37.49/6.00 (((product @ (product @ a31 @ a25) @ a21) = (product @ a25 @ a21))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17245, zip_derived_cl2940, zip_derived_cl202,
% 37.49/6.00 zip_derived_cl4845])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl17339, plain,
% 37.49/6.00 (((product @ (product @ a25 @ a21) @ a21) = (product @ a31 @ a25))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl17281, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl17358, plain, (((a25) = (product @ a31 @ a25))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl17339, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl26, plain, (((product @ a25 @ a23) = (a26))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_25])).
% 37.49/6.00 thf(zip_derived_cl17373, plain, (((a26) = (product @ a30 @ a26))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl9900, zip_derived_cl17358, zip_derived_cl26])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl17558, plain, (((product @ a26 @ a26) = (a30))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl17373, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl17572, plain, (((a26) = (a30))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl17558, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl17572, plain, (((a26) = (a30))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl17558, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl17605, plain,
% 37.49/6.00 (((tuple @ a1 @ a26 @ a31 @ a2 @ a21 @ a25 @ a3 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a21 @ a22 @ a21 @ a26 @ a27)
% 37.49/6.00 != (tuple @ a2 @ a31 @ a32 @ a3 @ a25 @ a26 @ a4 @ a29 @ a26 @ a5 @
% 37.49/6.00 a11 @ a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @
% 37.49/6.00 a17 @ a18 @ a13 @ a14 @ a21 @ a22 @ a21 @ a21 @ a27 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17539, zip_derived_cl17572, zip_derived_cl17572])).
% 37.49/6.00 thf(zip_derived_cl131, plain, (((product @ a30 @ a1) = (a29))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl30, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl17572, plain, (((a26) = (a30))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl17558, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl27, plain, (((product @ a26 @ a1) = (a27))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_26])).
% 37.49/6.00 thf(zip_derived_cl17583, plain, (((a27) = (a29))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl131, zip_derived_cl17572, zip_derived_cl27])).
% 37.49/6.00 thf(zip_derived_cl17583, plain, (((a27) = (a29))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl131, zip_derived_cl17572, zip_derived_cl27])).
% 37.49/6.00 thf(zip_derived_cl19456, plain,
% 37.49/6.00 (((tuple @ a1 @ a26 @ a31 @ a2 @ a21 @ a25 @ a3 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a21 @ a22 @ a21 @ a26 @ a29)
% 37.49/6.00 != (tuple @ a2 @ a31 @ a32 @ a3 @ a25 @ a26 @ a4 @ a29 @ a26 @ a5 @
% 37.49/6.00 a11 @ a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @
% 37.49/6.00 a17 @ a18 @ a13 @ a14 @ a21 @ a22 @ a21 @ a21 @ a29 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17605, zip_derived_cl17583, zip_derived_cl17583])).
% 37.49/6.00 thf(zip_derived_cl17358, plain, (((a25) = (product @ a31 @ a25))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl17339, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl17378, plain, (((product @ a25 @ a25) = (a31))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl17358, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl19458, plain, (((a31) = (a25))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl17378, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl19458, plain, (((a31) = (a25))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl17378, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl19522, plain,
% 37.49/6.00 (((tuple @ a1 @ a26 @ a31 @ a2 @ a21 @ a31 @ a3 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a21 @ a22 @ a21 @ a26 @ a29)
% 37.49/6.00 != (tuple @ a2 @ a31 @ a32 @ a3 @ a31 @ a26 @ a4 @ a29 @ a26 @ a5 @
% 37.49/6.00 a11 @ a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @
% 37.49/6.00 a17 @ a18 @ a13 @ a14 @ a21 @ a22 @ a21 @ a21 @ a29 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl19456, zip_derived_cl19458, zip_derived_cl19458])).
% 37.49/6.00 thf(zip_derived_cl4, plain, (((product @ a2 @ a25) = (a3))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_03])).
% 37.49/6.00 thf(zip_derived_cl19458, plain, (((a31) = (a25))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl17378, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl3, plain, (((product @ a1 @ a31) = (a2))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl38, plain, (((product @ a2 @ a31) = (a1))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl3, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl19484, plain, (((a1) = (a3))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl4, zip_derived_cl19458, zip_derived_cl38])).
% 37.49/6.00 thf(zip_derived_cl19484, plain, (((a1) = (a3))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl4, zip_derived_cl19458, zip_derived_cl38])).
% 37.49/6.00 thf(zip_derived_cl21210, plain,
% 37.49/6.00 (((tuple @ a1 @ a26 @ a31 @ a2 @ a21 @ a31 @ a1 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a21 @ a22 @ a21 @ a26 @ a29)
% 37.49/6.00 != (tuple @ a2 @ a31 @ a32 @ a1 @ a31 @ a26 @ a4 @ a29 @ a26 @ a5 @
% 37.49/6.00 a11 @ a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @
% 37.49/6.00 a17 @ a18 @ a13 @ a14 @ a21 @ a22 @ a21 @ a21 @ a29 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl19522, zip_derived_cl19484, zip_derived_cl19484])).
% 37.49/6.00 thf(zip_derived_cl17358, plain, (((a25) = (product @ a31 @ a25))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl17339, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl32, plain, (((product @ a31 @ a3) = (a32))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_31])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl138, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ a31 @ X0) @ a3)
% 37.49/6.00 = (product @ a32 @ (product @ X0 @ a3)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl32, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl17392, plain,
% 37.49/6.00 (((product @ a25 @ a3) = (product @ a32 @ (product @ a25 @ a3)))),
% 37.49/6.00 inference('s_sup+', [status(thm)],
% 37.49/6.00 [zip_derived_cl17358, zip_derived_cl138])).
% 37.49/6.00 thf(zip_derived_cl60, plain, (((product @ a25 @ a3) = (a24))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl25, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl60, plain, (((product @ a25 @ a3) = (a24))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl25, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl17401, plain, (((a24) = (product @ a32 @ a24))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17392, zip_derived_cl60, zip_derived_cl60])).
% 37.49/6.00 thf(zip_derived_cl17431, plain, (((a21) = (a24))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24, zip_derived_cl17424, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl17431, plain, (((a21) = (a24))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24, zip_derived_cl17424, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl33, plain, (((product @ a32 @ a21) = (a1))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_32])).
% 37.49/6.00 thf(zip_derived_cl21212, plain, (((a21) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17401, zip_derived_cl17431,
% 37.49/6.00 zip_derived_cl17431, zip_derived_cl33])).
% 37.49/6.00 thf(zip_derived_cl21212, plain, (((a21) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17401, zip_derived_cl17431,
% 37.49/6.00 zip_derived_cl17431, zip_derived_cl33])).
% 37.49/6.00 thf(zip_derived_cl21212, plain, (((a21) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17401, zip_derived_cl17431,
% 37.49/6.00 zip_derived_cl17431, zip_derived_cl33])).
% 37.49/6.00 thf(zip_derived_cl21212, plain, (((a21) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17401, zip_derived_cl17431,
% 37.49/6.00 zip_derived_cl17431, zip_derived_cl33])).
% 37.49/6.00 thf(zip_derived_cl21212, plain, (((a21) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17401, zip_derived_cl17431,
% 37.49/6.00 zip_derived_cl17431, zip_derived_cl33])).
% 37.49/6.00 thf(zip_derived_cl21212, plain, (((a21) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17401, zip_derived_cl17431,
% 37.49/6.00 zip_derived_cl17431, zip_derived_cl33])).
% 37.49/6.00 thf(zip_derived_cl21245, plain,
% 37.49/6.00 (((tuple @ a1 @ a26 @ a31 @ a2 @ a1 @ a31 @ a1 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a1 @ a22 @ a1 @ a26 @ a29)
% 37.49/6.00 != (tuple @ a2 @ a31 @ a32 @ a1 @ a31 @ a26 @ a4 @ a29 @ a26 @ a5 @
% 37.49/6.00 a11 @ a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @
% 37.49/6.00 a17 @ a18 @ a13 @ a14 @ a1 @ a22 @ a1 @ a1 @ a29 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl21210, zip_derived_cl21212,
% 37.49/6.00 zip_derived_cl21212, zip_derived_cl21212,
% 37.49/6.00 zip_derived_cl21212, zip_derived_cl21212, zip_derived_cl21212])).
% 37.49/6.00 thf(zip_derived_cl140, plain, (((product @ a1 @ a21) = (a32))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl33, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl21212, plain, (((a21) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17401, zip_derived_cl17431,
% 37.49/6.00 zip_derived_cl17431, zip_derived_cl33])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl21218, plain, (((a1) = (a32))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl140, zip_derived_cl21212, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl21248, plain,
% 37.49/6.00 (((tuple @ a1 @ a26 @ a31 @ a2 @ a1 @ a31 @ a1 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a1 @ a22 @ a1 @ a26 @ a29)
% 37.49/6.00 != (tuple @ a2 @ a31 @ a1 @ a1 @ a31 @ a26 @ a4 @ a29 @ a26 @ a5 @
% 37.49/6.00 a11 @ a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @
% 37.49/6.00 a17 @ a18 @ a13 @ a14 @ a1 @ a22 @ a1 @ a1 @ a29 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl21245, zip_derived_cl21218])).
% 37.49/6.00 thf(zip_derived_cl23, plain, (((product @ a22 @ a31) = (a23))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_22])).
% 37.49/6.00 thf(zip_derived_cl17424, plain, (((a21) = (a23))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl17408, zip_derived_cl57])).
% 37.49/6.00 thf(zip_derived_cl17430, plain, (((product @ a22 @ a31) = (a21))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl23, zip_derived_cl17424])).
% 37.49/6.00 thf(zip_derived_cl21212, plain, (((a21) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17401, zip_derived_cl17431,
% 37.49/6.00 zip_derived_cl17431, zip_derived_cl33])).
% 37.49/6.00 thf(zip_derived_cl23320, plain, (((product @ a22 @ a31) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17430, zip_derived_cl21212])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl23321, plain, (((product @ a1 @ a31) = (a22))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl23320, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl3, plain, (((product @ a1 @ a31) = (a2))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot])).
% 37.49/6.00 thf(zip_derived_cl23341, plain, (((a2) = (a22))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl23321, zip_derived_cl3])).
% 37.49/6.00 thf(zip_derived_cl23341, plain, (((a2) = (a22))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl23321, zip_derived_cl3])).
% 37.49/6.00 thf(zip_derived_cl23348, plain,
% 37.49/6.00 (((tuple @ a1 @ a26 @ a31 @ a2 @ a1 @ a31 @ a1 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a1 @ a2 @ a1 @ a26 @ a29)
% 37.49/6.00 != (tuple @ a2 @ a31 @ a1 @ a1 @ a31 @ a26 @ a4 @ a29 @ a26 @ a5 @
% 37.49/6.00 a11 @ a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @
% 37.49/6.00 a17 @ a18 @ a13 @ a14 @ a1 @ a2 @ a1 @ a1 @ a29 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl21248, zip_derived_cl23341, zip_derived_cl23341])).
% 37.49/6.00 thf(zip_derived_cl25, plain, (((product @ a24 @ a3) = (a25))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_24])).
% 37.49/6.00 thf(zip_derived_cl17431, plain, (((a21) = (a24))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24, zip_derived_cl17424, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl17499, plain, (((product @ a21 @ a3) = (a25))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl25, zip_derived_cl17431])).
% 37.49/6.00 thf(zip_derived_cl21212, plain, (((a21) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17401, zip_derived_cl17431,
% 37.49/6.00 zip_derived_cl17431, zip_derived_cl33])).
% 37.49/6.00 thf(zip_derived_cl19484, plain, (((a1) = (a3))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl4, zip_derived_cl19458, zip_derived_cl38])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl19458, plain, (((a31) = (a25))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl17378, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl23404, plain, (((a1) = (a31))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17499, zip_derived_cl21212,
% 37.49/6.00 zip_derived_cl19484, zip_derived_cl0, zip_derived_cl19458])).
% 37.49/6.00 thf(zip_derived_cl23404, plain, (((a1) = (a31))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17499, zip_derived_cl21212,
% 37.49/6.00 zip_derived_cl19484, zip_derived_cl0, zip_derived_cl19458])).
% 37.49/6.00 thf(zip_derived_cl23404, plain, (((a1) = (a31))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17499, zip_derived_cl21212,
% 37.49/6.00 zip_derived_cl19484, zip_derived_cl0, zip_derived_cl19458])).
% 37.49/6.00 thf(zip_derived_cl23404, plain, (((a1) = (a31))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17499, zip_derived_cl21212,
% 37.49/6.00 zip_derived_cl19484, zip_derived_cl0, zip_derived_cl19458])).
% 37.49/6.00 thf(zip_derived_cl23415, plain,
% 37.49/6.00 (((tuple @ a1 @ a26 @ a1 @ a2 @ a1 @ a1 @ a1 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a1 @ a2 @ a1 @ a26 @ a29)
% 37.49/6.00 != (tuple @ a2 @ a1 @ a1 @ a1 @ a1 @ a26 @ a4 @ a29 @ a26 @ a5 @
% 37.49/6.00 a11 @ a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @
% 37.49/6.00 a17 @ a18 @ a13 @ a14 @ a1 @ a2 @ a1 @ a1 @ a29 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl23348, zip_derived_cl23404,
% 37.49/6.00 zip_derived_cl23404, zip_derived_cl23404, zip_derived_cl23404])).
% 37.49/6.00 thf(zip_derived_cl3, plain, (((product @ a1 @ a31) = (a2))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot])).
% 37.49/6.00 thf(zip_derived_cl23404, plain, (((a1) = (a31))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17499, zip_derived_cl21212,
% 37.49/6.00 zip_derived_cl19484, zip_derived_cl0, zip_derived_cl19458])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl23405, plain, (((a1) = (a2))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl3, zip_derived_cl23404, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl23405, plain, (((a1) = (a2))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl3, zip_derived_cl23404, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl23405, plain, (((a1) = (a2))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl3, zip_derived_cl23404, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl23405, plain, (((a1) = (a2))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl3, zip_derived_cl23404, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl24475, plain,
% 37.49/6.00 (((tuple @ a1 @ a26 @ a1 @ a1 @ a1 @ a1 @ a1 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a1 @ a1 @ a1 @ a26 @ a29)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a26 @ a4 @ a29 @ a26 @ a5 @
% 37.49/6.00 a11 @ a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @
% 37.49/6.00 a17 @ a18 @ a13 @ a14 @ a1 @ a1 @ a1 @ a1 @ a29 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl23415, zip_derived_cl23405,
% 37.49/6.00 zip_derived_cl23405, zip_derived_cl23405, zip_derived_cl23405])).
% 37.49/6.00 thf(zip_derived_cl17367, plain, (((a22) = (product @ a23 @ a25))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17351, zip_derived_cl953, zip_derived_cl1,
% 37.49/6.00 zip_derived_cl16527])).
% 37.49/6.00 thf(zip_derived_cl873, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ (product @ X1 @ X0)) @ X0)
% 37.49/6.00 = (product @ X0 @ X1))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl91, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl17420, plain,
% 37.49/6.00 (((product @ (product @ a25 @ a22) @ a25) = (product @ a25 @ a23))),
% 37.49/6.00 inference('s_sup+', [status(thm)],
% 37.49/6.00 [zip_derived_cl17367, zip_derived_cl873])).
% 37.49/6.00 thf(zip_derived_cl22, plain, (((product @ a21 @ a25) = (a22))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_21])).
% 37.49/6.00 thf(zip_derived_cl873, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ (product @ X1 @ X0)) @ X0)
% 37.49/6.00 = (product @ X0 @ X1))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl91, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl8073, plain,
% 37.49/6.00 (((product @ (product @ a25 @ a22) @ a25) = (product @ a25 @ a21))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl22, zip_derived_cl873])).
% 37.49/6.00 thf(zip_derived_cl26, plain, (((product @ a25 @ a23) = (a26))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_25])).
% 37.49/6.00 thf(zip_derived_cl17428, plain, (((product @ a25 @ a21) = (a26))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17420, zip_derived_cl8073, zip_derived_cl26])).
% 37.49/6.00 thf(zip_derived_cl19458, plain, (((a31) = (a25))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl17378, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl21212, plain, (((a21) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17401, zip_derived_cl17431,
% 37.49/6.00 zip_derived_cl17431, zip_derived_cl33])).
% 37.49/6.00 thf(zip_derived_cl23294, plain, (((product @ a31 @ a1) = (a26))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17428, zip_derived_cl19458, zip_derived_cl21212])).
% 37.49/6.00 thf(zip_derived_cl23404, plain, (((a1) = (a31))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17499, zip_derived_cl21212,
% 37.49/6.00 zip_derived_cl19484, zip_derived_cl0, zip_derived_cl19458])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl23414, plain, (((a1) = (a26))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl23294, zip_derived_cl23404, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl23414, plain, (((a1) = (a26))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl23294, zip_derived_cl23404, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl23414, plain, (((a1) = (a26))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl23294, zip_derived_cl23404, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl23414, plain, (((a1) = (a26))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl23294, zip_derived_cl23404, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl24477, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a28 @ a29 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a1 @ a1 @ a1 @ a1 @ a29)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a4 @ a29 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @ a17 @
% 37.49/6.00 a18 @ a13 @ a14 @ a1 @ a1 @ a1 @ a1 @ a29 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24475, zip_derived_cl23414,
% 37.49/6.00 zip_derived_cl23414, zip_derived_cl23414, zip_derived_cl23414])).
% 37.49/6.00 thf(zip_derived_cl30, plain, (((product @ a29 @ a1) = (a30))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_29])).
% 37.49/6.00 thf(zip_derived_cl17572, plain, (((a26) = (a30))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl17558, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl17582, plain, (((product @ a29 @ a1) = (a26))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl30, zip_derived_cl17572])).
% 37.49/6.00 thf(zip_derived_cl23414, plain, (((a1) = (a26))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl23294, zip_derived_cl23404, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl24487, plain, (((product @ a29 @ a1) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17582, zip_derived_cl23414])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl24488, plain, (((product @ a1 @ a1) = (a29))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl24487, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl24509, plain, (((a1) = (a29))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl24488, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl24509, plain, (((a1) = (a29))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl24488, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl24509, plain, (((a1) = (a29))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl24488, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl24509, plain, (((a1) = (a29))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl24488, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl24533, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a28 @ a1 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a20 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a4 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a20 @ a9 @ a10 @ a17 @
% 37.49/6.00 a18 @ a13 @ a14 @ a1 @ a1 @ a1 @ a1 @ a1 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24477, zip_derived_cl24509,
% 37.49/6.00 zip_derived_cl24509, zip_derived_cl24509, zip_derived_cl24509])).
% 37.49/6.00 thf(zip_derived_cl24487, plain, (((product @ a29 @ a1) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17582, zip_derived_cl23414])).
% 37.49/6.00 thf(zip_derived_cl873, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ (product @ X1 @ X0)) @ X0)
% 37.49/6.00 = (product @ X0 @ X1))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl91, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl24502, plain,
% 37.49/6.00 (((product @ (product @ a1 @ a1) @ a1) = (product @ a1 @ a29))),
% 37.49/6.00 inference('s_sup+', [status(thm)],
% 37.49/6.00 [zip_derived_cl24487, zip_derived_cl873])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl24, plain, (((product @ a23 @ a21) = (a24))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_23])).
% 37.49/6.00 thf(knot_20, axiom, (( product @ a20 @ a29 ) = ( a21 ))).
% 37.49/6.00 thf(zip_derived_cl21, plain, (((product @ a20 @ a29) = (a21))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_20])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl56, plain, (((product @ a21 @ a29) = (a20))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl21, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl199, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ a21) @ a29)
% 37.49/6.00 = (product @ (product @ X0 @ a29) @ a20))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl56, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl16343, plain,
% 37.49/6.00 (((product @ a24 @ a29) = (product @ (product @ a23 @ a29) @ a20))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl24, zip_derived_cl199])).
% 37.49/6.00 thf(zip_derived_cl17424, plain, (((a21) = (a23))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl17408, zip_derived_cl57])).
% 37.49/6.00 thf(zip_derived_cl56, plain, (((product @ a21 @ a29) = (a20))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl21, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl17494, plain, (((product @ a24 @ a29) = (a20))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl16343, zip_derived_cl17424, zip_derived_cl56,
% 37.49/6.00 zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl17431, plain, (((a21) = (a24))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24, zip_derived_cl17424, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl21212, plain, (((a21) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17401, zip_derived_cl17431,
% 37.49/6.00 zip_derived_cl17431, zip_derived_cl33])).
% 37.49/6.00 thf(zip_derived_cl21244, plain, (((a1) = (a24))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17431, zip_derived_cl21212])).
% 37.49/6.00 thf(zip_derived_cl23382, plain, (((product @ a1 @ a29) = (a20))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17494, zip_derived_cl21244])).
% 37.49/6.00 thf(zip_derived_cl24519, plain, (((a1) = (a20))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24502, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl23382])).
% 37.49/6.00 thf(zip_derived_cl24519, plain, (((a1) = (a20))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24502, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl23382])).
% 37.49/6.00 thf(zip_derived_cl26235, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a28 @ a1 @ a4 @ a10 @
% 37.49/6.00 a11 @ a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @
% 37.49/6.00 a12 @ a13 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a4 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a1 @ a9 @ a10 @ a17 @
% 37.49/6.00 a18 @ a13 @ a14 @ a1 @ a1 @ a1 @ a1 @ a1 @ a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24533, zip_derived_cl24519, zip_derived_cl24519])).
% 37.49/6.00 thf(zip_derived_cl28, plain, (((product @ a27 @ a21) = (a28))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_27])).
% 37.49/6.00 thf(zip_derived_cl17583, plain, (((a27) = (a29))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl131, zip_derived_cl17572, zip_derived_cl27])).
% 37.49/6.00 thf(zip_derived_cl19428, plain, (((product @ a29 @ a21) = (a28))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl28, zip_derived_cl17583])).
% 37.49/6.00 thf(zip_derived_cl24509, plain, (((a1) = (a29))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl24488, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl21212, plain, (((a21) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17401, zip_derived_cl17431,
% 37.49/6.00 zip_derived_cl17431, zip_derived_cl33])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl26238, plain, (((a1) = (a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl19428, zip_derived_cl24509,
% 37.49/6.00 zip_derived_cl21212, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl26238, plain, (((a1) = (a28))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl19428, zip_derived_cl24509,
% 37.49/6.00 zip_derived_cl21212, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl26239, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a4 @ a10 @ a11 @
% 37.49/6.00 a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @ a12 @
% 37.49/6.00 a13 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a4 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a1 @ a9 @ a10 @ a17 @
% 37.49/6.00 a18 @ a13 @ a14 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26235, zip_derived_cl26238, zip_derived_cl26238])).
% 37.49/6.00 thf(knot_04, axiom, (( product @ a3 @ a29 ) = ( a4 ))).
% 37.49/6.00 thf(zip_derived_cl5, plain, (((product @ a3 @ a29) = (a4))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_04])).
% 37.49/6.00 thf(zip_derived_cl19484, plain, (((a1) = (a3))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl4, zip_derived_cl19458, zip_derived_cl38])).
% 37.49/6.00 thf(zip_derived_cl21158, plain, (((product @ a1 @ a29) = (a4))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl5, zip_derived_cl19484])).
% 37.49/6.00 thf(zip_derived_cl24509, plain, (((a1) = (a29))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl24488, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl26248, plain, (((a1) = (a4))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl21158, zip_derived_cl24509, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl26248, plain, (((a1) = (a4))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl21158, zip_derived_cl24509, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl26292, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a10 @ a11 @
% 37.49/6.00 a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a19 @ a8 @ a9 @ a16 @ a17 @ a12 @
% 37.49/6.00 a13 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a19 @ a1 @ a9 @ a10 @ a17 @
% 37.49/6.00 a18 @ a13 @ a14 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26239, zip_derived_cl26248, zip_derived_cl26248])).
% 37.49/6.00 thf(knot_19, axiom, (( product @ a19 @ a11 ) = ( a20 ))).
% 37.49/6.00 thf(zip_derived_cl20, plain, (((product @ a19 @ a11) = (a20))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_19])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl55, plain, (((product @ a20 @ a11) = (a19))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl20, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl24519, plain, (((a1) = (a20))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24502, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl23382])).
% 37.49/6.00 thf(zip_derived_cl24536, plain, (((product @ a1 @ a11) = (a19))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl55, zip_derived_cl24519])).
% 37.49/6.00 thf(knot_05, axiom, (( product @ a4 @ a11 ) = ( a5 ))).
% 37.49/6.00 thf(zip_derived_cl6, plain, (((product @ a4 @ a11) = (a5))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_05])).
% 37.49/6.00 thf(zip_derived_cl26248, plain, (((a1) = (a4))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl21158, zip_derived_cl24509, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl26249, plain, (((product @ a1 @ a11) = (a5))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl6, zip_derived_cl26248])).
% 37.49/6.00 thf(zip_derived_cl26647, plain, (((a5) = (a19))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24536, zip_derived_cl26249])).
% 37.49/6.00 thf(zip_derived_cl26647, plain, (((a5) = (a19))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24536, zip_derived_cl26249])).
% 37.49/6.00 thf(zip_derived_cl26765, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a10 @ a11 @
% 37.49/6.00 a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a5 @ a8 @ a9 @ a16 @ a17 @ a12 @
% 37.49/6.00 a13 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a5 @ a1 @ a9 @ a10 @ a17 @ a18 @
% 37.49/6.00 a13 @ a14 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26292, zip_derived_cl26647, zip_derived_cl26647])).
% 37.49/6.00 thf(knot_12, axiom, (( product @ a12 @ a19 ) = ( a13 ))).
% 37.49/6.00 thf(zip_derived_cl13, plain, (((product @ a12 @ a19) = (a13))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_12])).
% 37.49/6.00 thf(zip_derived_cl26647, plain, (((a5) = (a19))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24536, zip_derived_cl26249])).
% 37.49/6.00 thf(knot_11, axiom, (( product @ a11 @ a5 ) = ( a12 ))).
% 37.49/6.00 thf(zip_derived_cl12, plain, (((product @ a11 @ a5) = (a12))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_11])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl42, plain, (((product @ a12 @ a5) = (a11))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl12, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl26679, plain, (((a11) = (a13))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl13, zip_derived_cl26647, zip_derived_cl42])).
% 37.49/6.00 thf(zip_derived_cl26679, plain, (((a11) = (a13))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl13, zip_derived_cl26647, zip_derived_cl42])).
% 37.49/6.00 thf(zip_derived_cl26786, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a10 @ a11 @
% 37.49/6.00 a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a5 @ a8 @ a9 @ a16 @ a17 @ a12 @
% 37.49/6.00 a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a5 @ a1 @ a9 @ a10 @ a17 @ a18 @
% 37.49/6.00 a11 @ a14 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26765, zip_derived_cl26679, zip_derived_cl26679])).
% 37.49/6.00 thf(knot_16, axiom, (( product @ a16 @ a19 ) = ( a17 ))).
% 37.49/6.00 thf(zip_derived_cl17, plain, (((product @ a16 @ a19) = (a17))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_16])).
% 37.49/6.00 thf(zip_derived_cl26647, plain, (((a5) = (a19))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24536, zip_derived_cl26249])).
% 37.49/6.00 thf(knot_15, axiom, (( product @ a15 @ a5 ) = ( a16 ))).
% 37.49/6.00 thf(zip_derived_cl16, plain, (((product @ a15 @ a5) = (a16))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_15])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl44, plain, (((product @ a16 @ a5) = (a15))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl16, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl26680, plain, (((a15) = (a17))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17, zip_derived_cl26647, zip_derived_cl44])).
% 37.49/6.00 thf(zip_derived_cl26680, plain, (((a15) = (a17))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17, zip_derived_cl26647, zip_derived_cl44])).
% 37.49/6.00 thf(zip_derived_cl26846, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a10 @ a11 @
% 37.49/6.00 a5 @ a14 @ a15 @ a6 @ a7 @ a18 @ a5 @ a8 @ a9 @ a16 @ a15 @ a12 @
% 37.49/6.00 a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a5 @ a1 @ a9 @ a10 @ a15 @ a18 @
% 37.49/6.00 a11 @ a14 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26786, zip_derived_cl26680, zip_derived_cl26680])).
% 37.49/6.00 thf(knot_18, axiom, (( product @ a18 @ a15 ) = ( a19 ))).
% 37.49/6.00 thf(zip_derived_cl19, plain, (((product @ a18 @ a15) = (a19))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_18])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl54, plain, (((product @ a19 @ a15) = (a18))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl19, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl26647, plain, (((a5) = (a19))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24536, zip_derived_cl26249])).
% 37.49/6.00 thf(knot_06, axiom, (( product @ a5 @ a15 ) = ( a6 ))).
% 37.49/6.00 thf(zip_derived_cl7, plain, (((product @ a5 @ a15) = (a6))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_06])).
% 37.49/6.00 thf(zip_derived_cl26685, plain, (((a6) = (a18))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl54, zip_derived_cl26647, zip_derived_cl7])).
% 37.49/6.00 thf(knot_07, axiom, (( product @ a7 @ a19 ) = ( a8 ))).
% 37.49/6.00 thf(zip_derived_cl8, plain, (((product @ a7 @ a19) = (a8))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_07])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl45, plain, (((product @ a8 @ a19) = (a7))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl8, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl26647, plain, (((a5) = (a19))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24536, zip_derived_cl26249])).
% 37.49/6.00 thf(knot_08, axiom, (( product @ a8 @ a5 ) = ( a9 ))).
% 37.49/6.00 thf(zip_derived_cl9, plain, (((product @ a8 @ a5) = (a9))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_08])).
% 37.49/6.00 thf(zip_derived_cl26682, plain, (((a9) = (a7))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl45, zip_derived_cl26647, zip_derived_cl9])).
% 37.49/6.00 thf(zip_derived_cl26682, plain, (((a9) = (a7))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl45, zip_derived_cl26647, zip_derived_cl9])).
% 37.49/6.00 thf(zip_derived_cl26685, plain, (((a6) = (a18))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl54, zip_derived_cl26647, zip_derived_cl7])).
% 37.49/6.00 thf(zip_derived_cl26877, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a10 @ a11 @
% 37.49/6.00 a5 @ a14 @ a15 @ a6 @ a7 @ a6 @ a5 @ a8 @ a7 @ a16 @ a15 @ a12 @
% 37.49/6.00 a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a5 @ a1 @ a7 @ a10 @ a15 @ a6 @
% 37.49/6.00 a11 @ a14 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26846, zip_derived_cl26685,
% 37.49/6.00 zip_derived_cl26682, zip_derived_cl26682, zip_derived_cl26685])).
% 37.49/6.00 thf(zip_derived_cl17, plain, (((product @ a16 @ a19) = (a17))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_16])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl52, plain, (((product @ a17 @ a19) = (a16))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl17, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl91, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X1) @ X0)
% 37.49/6.00 = (product @ X0 @ (product @ X1 @ X0)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl937, plain,
% 37.49/6.00 (((product @ a16 @ a17) = (product @ a17 @ (product @ a19 @ a17)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl52, zip_derived_cl91])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl2069, plain,
% 37.49/6.00 (((product @ (product @ a16 @ a17) @ (product @ a19 @ a17)) = (a17))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl937, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl26647, plain, (((a5) = (a19))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24536, zip_derived_cl26249])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl44, plain, (((product @ a16 @ a5) = (a15))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl16, zip_derived_cl1])).
% 37.49/6.00 thf(knot_14, axiom, (( product @ a14 @ a17 ) = ( a15 ))).
% 37.49/6.00 thf(zip_derived_cl15, plain, (((product @ a14 @ a17) = (a15))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_14])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl51, plain, (((product @ a15 @ a17) = (a14))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl15, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl26717, plain, (((a14) = (a17))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl2069, zip_derived_cl26647, zip_derived_cl2,
% 37.49/6.00 zip_derived_cl44, zip_derived_cl51])).
% 37.49/6.00 thf(zip_derived_cl26680, plain, (((a15) = (a17))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17, zip_derived_cl26647, zip_derived_cl44])).
% 37.49/6.00 thf(zip_derived_cl26878, plain, (((a14) = (a15))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26717, zip_derived_cl26680])).
% 37.49/6.00 thf(zip_derived_cl26878, plain, (((a14) = (a15))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26717, zip_derived_cl26680])).
% 37.49/6.00 thf(zip_derived_cl26879, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a10 @ a11 @
% 37.49/6.00 a5 @ a15 @ a15 @ a6 @ a7 @ a6 @ a5 @ a8 @ a7 @ a16 @ a15 @ a12 @
% 37.49/6.00 a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a5 @ a1 @ a7 @ a10 @ a15 @ a6 @
% 37.49/6.00 a11 @ a15 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26877, zip_derived_cl26878, zip_derived_cl26878])).
% 37.49/6.00 thf(knot_13, axiom, (( product @ a13 @ a7 ) = ( a14 ))).
% 37.49/6.00 thf(zip_derived_cl14, plain, (((product @ a13 @ a7) = (a14))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_13])).
% 37.49/6.00 thf(zip_derived_cl26679, plain, (((a11) = (a13))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl13, zip_derived_cl26647, zip_derived_cl42])).
% 37.49/6.00 thf(knot_10, axiom, (( product @ a10 @ a7 ) = ( a11 ))).
% 37.49/6.00 thf(zip_derived_cl11, plain, (((product @ a10 @ a7) = (a11))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_10])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl48, plain, (((product @ a11 @ a7) = (a10))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl11, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl26766, plain, (((a10) = (a14))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl14, zip_derived_cl26679, zip_derived_cl48])).
% 37.49/6.00 thf(zip_derived_cl26878, plain, (((a14) = (a15))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26717, zip_derived_cl26680])).
% 37.49/6.00 thf(zip_derived_cl26880, plain, (((a10) = (a15))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26766, zip_derived_cl26878])).
% 37.49/6.00 thf(zip_derived_cl26880, plain, (((a10) = (a15))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26766, zip_derived_cl26878])).
% 37.49/6.00 thf(zip_derived_cl26898, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a15 @ a11 @
% 37.49/6.00 a5 @ a15 @ a15 @ a6 @ a7 @ a6 @ a5 @ a8 @ a7 @ a16 @ a15 @ a12 @
% 37.49/6.00 a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a15 @ a16 @ a7 @ a8 @ a5 @ a1 @ a7 @ a15 @ a15 @ a6 @
% 37.49/6.00 a11 @ a15 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26879, zip_derived_cl26880, zip_derived_cl26880])).
% 37.49/6.00 thf(knot_09, axiom, (( product @ a9 @ a17 ) = ( a10 ))).
% 37.49/6.00 thf(zip_derived_cl10, plain, (((product @ a9 @ a17) = (a10))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_09])).
% 37.49/6.00 thf(zip_derived_cl26680, plain, (((a15) = (a17))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17, zip_derived_cl26647, zip_derived_cl44])).
% 37.49/6.00 thf(zip_derived_cl26787, plain, (((product @ a9 @ a15) = (a10))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl10, zip_derived_cl26680])).
% 37.49/6.00 thf(zip_derived_cl26682, plain, (((a9) = (a7))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl45, zip_derived_cl26647, zip_derived_cl9])).
% 37.49/6.00 thf(zip_derived_cl26880, plain, (((a10) = (a15))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26766, zip_derived_cl26878])).
% 37.49/6.00 thf(zip_derived_cl27134, plain, (((product @ a7 @ a15) = (a15))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26787, zip_derived_cl26682, zip_derived_cl26880])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl27135, plain, (((product @ a15 @ a15) = (a7))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl27134, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl27161, plain, (((a15) = (a7))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl27135, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl27161, plain, (((a15) = (a7))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl27135, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl27161, plain, (((a15) = (a7))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl27135, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl27161, plain, (((a15) = (a7))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl27135, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl27184, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a15 @ a11 @
% 37.49/6.00 a5 @ a15 @ a15 @ a6 @ a15 @ a6 @ a5 @ a8 @ a15 @ a16 @ a15 @ a12 @
% 37.49/6.00 a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a15 @ a16 @ a15 @ a8 @ a5 @ a1 @ a15 @ a15 @ a15 @
% 37.49/6.00 a6 @ a11 @ a15 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26898, zip_derived_cl27161,
% 37.49/6.00 zip_derived_cl27161, zip_derived_cl27161, zip_derived_cl27161])).
% 37.49/6.00 thf(zip_derived_cl27134, plain, (((product @ a7 @ a15) = (a15))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26787, zip_derived_cl26682, zip_derived_cl26880])).
% 37.49/6.00 thf(zip_derived_cl873, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ (product @ X1 @ X0)) @ X0)
% 37.49/6.00 = (product @ X0 @ X1))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl91, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl27151, plain,
% 37.49/6.00 (((product @ (product @ a15 @ a15) @ a15) = (product @ a15 @ a7))),
% 37.49/6.00 inference('s_sup+', [status(thm)],
% 37.49/6.00 [zip_derived_cl27134, zip_derived_cl873])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl14, plain, (((product @ a13 @ a7) = (a14))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_13])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl50, plain, (((product @ a14 @ a7) = (a13))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl14, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl26679, plain, (((a11) = (a13))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl13, zip_derived_cl26647, zip_derived_cl42])).
% 37.49/6.00 thf(zip_derived_cl26767, plain, (((product @ a14 @ a7) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl50, zip_derived_cl26679])).
% 37.49/6.00 thf(zip_derived_cl26878, plain, (((a14) = (a15))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26717, zip_derived_cl26680])).
% 37.49/6.00 thf(zip_derived_cl27103, plain, (((product @ a15 @ a7) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26767, zip_derived_cl26878])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27222, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a11 @ a11 @
% 37.49/6.00 a5 @ a11 @ a11 @ a6 @ a11 @ a6 @ a5 @ a8 @ a11 @ a16 @ a11 @ a12 @
% 37.49/6.00 a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a11 @ a16 @ a11 @ a8 @ a5 @ a1 @ a11 @ a11 @ a11 @
% 37.49/6.00 a6 @ a11 @ a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27184, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27172, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27172, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27172, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27172, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27172, zip_derived_cl27172, zip_derived_cl27172])).
% 37.49/6.00 thf(zip_derived_cl8, plain, (((product @ a7 @ a19) = (a8))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_07])).
% 37.49/6.00 thf(zip_derived_cl26647, plain, (((a5) = (a19))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl24536, zip_derived_cl26249])).
% 37.49/6.00 thf(zip_derived_cl26678, plain, (((product @ a7 @ a5) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl8, zip_derived_cl26647])).
% 37.49/6.00 thf(zip_derived_cl27161, plain, (((a15) = (a7))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl27135, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl16, plain, (((product @ a15 @ a5) = (a16))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_15])).
% 37.49/6.00 thf(zip_derived_cl27182, plain, (((a16) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26678, zip_derived_cl27161, zip_derived_cl16])).
% 37.49/6.00 thf(zip_derived_cl27182, plain, (((a16) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26678, zip_derived_cl27161, zip_derived_cl16])).
% 37.49/6.00 thf(zip_derived_cl27382, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a11 @ a11 @
% 37.49/6.00 a5 @ a11 @ a11 @ a6 @ a11 @ a6 @ a5 @ a8 @ a11 @ a8 @ a11 @ a12 @
% 37.49/6.00 a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a6 @ a11 @ a8 @ a11 @ a8 @ a5 @ a1 @ a11 @ a11 @ a11 @ a6 @
% 37.49/6.00 a11 @ a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27222, zip_derived_cl27182, zip_derived_cl27182])).
% 37.49/6.00 thf(zip_derived_cl7, plain, (((product @ a5 @ a15) = (a6))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_06])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl6, plain, (((product @ a4 @ a11) = (a5))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_05])).
% 37.49/6.00 thf(zip_derived_cl1, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 37.49/6.00 thf(zip_derived_cl41, plain, (((product @ a5 @ a11) = (a4))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl26248, plain, (((a1) = (a4))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl21158, zip_derived_cl24509, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl26250, plain, (((product @ a5 @ a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl41, zip_derived_cl26248])).
% 37.49/6.00 thf(zip_derived_cl27188, plain, (((a1) = (a6))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl7, zip_derived_cl27172, zip_derived_cl26250])).
% 37.49/6.00 thf(zip_derived_cl27188, plain, (((a1) = (a6))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl7, zip_derived_cl27172, zip_derived_cl26250])).
% 37.49/6.00 thf(zip_derived_cl27188, plain, (((a1) = (a6))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl7, zip_derived_cl27172, zip_derived_cl26250])).
% 37.49/6.00 thf(zip_derived_cl27188, plain, (((a1) = (a6))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl7, zip_derived_cl27172, zip_derived_cl26250])).
% 37.49/6.00 thf(zip_derived_cl27384, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a11 @ a11 @
% 37.49/6.00 a5 @ a11 @ a11 @ a1 @ a11 @ a1 @ a5 @ a8 @ a11 @ a8 @ a11 @ a12 @
% 37.49/6.00 a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a12 @ a1 @ a11 @ a8 @ a11 @ a8 @ a5 @ a1 @ a11 @ a11 @ a11 @ a1 @
% 37.49/6.00 a11 @ a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27382, zip_derived_cl27188,
% 37.49/6.00 zip_derived_cl27188, zip_derived_cl27188, zip_derived_cl27188])).
% 37.49/6.00 thf(zip_derived_cl16, plain, (((product @ a15 @ a5) = (a16))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_15])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl12, plain, (((product @ a11 @ a5) = (a12))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_11])).
% 37.49/6.00 thf(zip_derived_cl27189, plain, (((a12) = (a16))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl16, zip_derived_cl27172, zip_derived_cl12])).
% 37.49/6.00 thf(zip_derived_cl27182, plain, (((a16) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26678, zip_derived_cl27161, zip_derived_cl16])).
% 37.49/6.00 thf(zip_derived_cl27385, plain, (((a12) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27189, zip_derived_cl27182])).
% 37.49/6.00 thf(zip_derived_cl27385, plain, (((a12) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27189, zip_derived_cl27182])).
% 37.49/6.00 thf(zip_derived_cl27392, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a11 @ a11 @
% 37.49/6.00 a5 @ a11 @ a11 @ a1 @ a11 @ a1 @ a5 @ a8 @ a11 @ a8 @ a11 @ a8 @
% 37.49/6.00 a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a11 @
% 37.49/6.00 a8 @ a1 @ a11 @ a8 @ a11 @ a8 @ a5 @ a1 @ a11 @ a11 @ a11 @ a1 @
% 37.49/6.00 a11 @ a11 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27384, zip_derived_cl27385, zip_derived_cl27385])).
% 37.49/6.00 thf(knot_17, axiom, (( product @ a17 @ a9 ) = ( a18 ))).
% 37.49/6.00 thf(zip_derived_cl18, plain, (((product @ a17 @ a9) = (a18))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_17])).
% 37.49/6.00 thf(zip_derived_cl26680, plain, (((a15) = (a17))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17, zip_derived_cl26647, zip_derived_cl44])).
% 37.49/6.00 thf(zip_derived_cl26789, plain, (((product @ a15 @ a9) = (a18))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl18, zip_derived_cl26680])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl26682, plain, (((a9) = (a7))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl45, zip_derived_cl26647, zip_derived_cl9])).
% 37.49/6.00 thf(zip_derived_cl27161, plain, (((a15) = (a7))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl27135, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl27183, plain, (((a9) = (a15))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26682, zip_derived_cl27161])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27229, plain, (((a9) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27183, zip_derived_cl27172])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl26685, plain, (((a6) = (a18))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl54, zip_derived_cl26647, zip_derived_cl7])).
% 37.49/6.00 thf(zip_derived_cl27188, plain, (((a1) = (a6))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl7, zip_derived_cl27172, zip_derived_cl26250])).
% 37.49/6.00 thf(zip_derived_cl27383, plain, (((a1) = (a18))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26685, zip_derived_cl27188])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27554, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @
% 37.49/6.00 a5 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a8 @ a1 @ a8 @ a1 @ a8 @ a1 @ a1 @
% 37.49/6.00 a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a5 @ a1 @
% 37.49/6.00 a8 @ a1 @ a1 @ a8 @ a1 @ a8 @ a5 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @
% 37.49/6.00 a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27392, zip_derived_cl27544,
% 37.49/6.00 zip_derived_cl27544, zip_derived_cl27544,
% 37.49/6.00 zip_derived_cl27544, zip_derived_cl27544,
% 37.49/6.00 zip_derived_cl27544, zip_derived_cl27544,
% 37.49/6.00 zip_derived_cl27544, zip_derived_cl27544,
% 37.49/6.00 zip_derived_cl27544, zip_derived_cl27544,
% 37.49/6.00 zip_derived_cl27544, zip_derived_cl27544,
% 37.49/6.00 zip_derived_cl27544, zip_derived_cl27544, zip_derived_cl27544])).
% 37.49/6.00 thf(zip_derived_cl26249, plain, (((product @ a1 @ a11) = (a5))),
% 37.49/6.00 inference('demod', [status(thm)], [zip_derived_cl6, zip_derived_cl26248])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl27545, plain, (((a1) = (a5))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26249, zip_derived_cl27544, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl27545, plain, (((a1) = (a5))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26249, zip_derived_cl27544, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl27545, plain, (((a1) = (a5))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26249, zip_derived_cl27544, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl27545, plain, (((a1) = (a5))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26249, zip_derived_cl27544, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl27556, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @
% 37.49/6.00 a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a8 @ a1 @ a8 @ a1 @ a8 @ a1 @ a1 @
% 37.49/6.00 a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @
% 37.49/6.00 a8 @ a1 @ a1 @ a8 @ a1 @ a8 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @
% 37.49/6.00 a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27554, zip_derived_cl27545,
% 37.49/6.00 zip_derived_cl27545, zip_derived_cl27545, zip_derived_cl27545])).
% 37.49/6.00 thf(zip_derived_cl51, plain, (((product @ a15 @ a17) = (a14))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl15, zip_derived_cl1])).
% 37.49/6.00 thf(zip_derived_cl16, plain, (((product @ a15 @ a5) = (a16))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_15])).
% 37.49/6.00 thf(zip_derived_cl2, plain,
% 37.49/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.49/6.00 ((product @ (product @ X0 @ X2) @ X1)
% 37.49/6.00 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 37.49/6.00 thf(zip_derived_cl100, plain,
% 37.49/6.00 (![X0 : $i]:
% 37.49/6.00 ((product @ (product @ a15 @ X0) @ a5)
% 37.49/6.00 = (product @ a16 @ (product @ X0 @ a5)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl16, zip_derived_cl2])).
% 37.49/6.00 thf(zip_derived_cl6650, plain,
% 37.49/6.00 (((product @ a14 @ a5) = (product @ a16 @ (product @ a17 @ a5)))),
% 37.49/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl51, zip_derived_cl100])).
% 37.49/6.00 thf(zip_derived_cl26680, plain, (((a15) = (a17))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl17, zip_derived_cl26647, zip_derived_cl44])).
% 37.49/6.00 thf(zip_derived_cl16, plain, (((product @ a15 @ a5) = (a16))),
% 37.49/6.00 inference('cnf', [status(esa)], [knot_15])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl26824, plain, (((product @ a14 @ a5) = (a16))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl6650, zip_derived_cl26680, zip_derived_cl16,
% 37.49/6.00 zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl26878, plain, (((a14) = (a15))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26717, zip_derived_cl26680])).
% 37.49/6.00 thf(zip_derived_cl27172, plain, (((a15) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27151, zip_derived_cl0, zip_derived_cl0,
% 37.49/6.00 zip_derived_cl27103])).
% 37.49/6.00 thf(zip_derived_cl27219, plain, (((a14) = (a11))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26878, zip_derived_cl27172])).
% 37.49/6.00 thf(zip_derived_cl27544, plain, (((a11) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26789, zip_derived_cl27172,
% 37.49/6.00 zip_derived_cl27229, zip_derived_cl0, zip_derived_cl27383])).
% 37.49/6.00 thf(zip_derived_cl27550, plain, (((a14) = (a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27219, zip_derived_cl27544])).
% 37.49/6.00 thf(zip_derived_cl27545, plain, (((a1) = (a5))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26249, zip_derived_cl27544, zip_derived_cl0])).
% 37.49/6.00 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 37.49/6.00 inference('cnf', [status(esa)], [involutory_quandle])).
% 37.49/6.00 thf(zip_derived_cl27182, plain, (((a16) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26678, zip_derived_cl27161, zip_derived_cl16])).
% 37.49/6.00 thf(zip_derived_cl27562, plain, (((a1) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26824, zip_derived_cl27550,
% 37.49/6.00 zip_derived_cl27545, zip_derived_cl0, zip_derived_cl27182])).
% 37.49/6.00 thf(zip_derived_cl27562, plain, (((a1) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26824, zip_derived_cl27550,
% 37.49/6.00 zip_derived_cl27545, zip_derived_cl0, zip_derived_cl27182])).
% 37.49/6.00 thf(zip_derived_cl27562, plain, (((a1) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26824, zip_derived_cl27550,
% 37.49/6.00 zip_derived_cl27545, zip_derived_cl0, zip_derived_cl27182])).
% 37.49/6.00 thf(zip_derived_cl27562, plain, (((a1) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26824, zip_derived_cl27550,
% 37.49/6.00 zip_derived_cl27545, zip_derived_cl0, zip_derived_cl27182])).
% 37.49/6.00 thf(zip_derived_cl27562, plain, (((a1) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26824, zip_derived_cl27550,
% 37.49/6.00 zip_derived_cl27545, zip_derived_cl0, zip_derived_cl27182])).
% 37.49/6.00 thf(zip_derived_cl27562, plain, (((a1) = (a8))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl26824, zip_derived_cl27550,
% 37.49/6.00 zip_derived_cl27545, zip_derived_cl0, zip_derived_cl27182])).
% 37.49/6.00 thf(zip_derived_cl27565, plain,
% 37.49/6.00 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @
% 37.49/6.00 a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @
% 37.49/6.00 a1 @ a1 @ a1 @ a1 @ a1)
% 37.49/6.00 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @
% 37.49/6.00 a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @
% 37.49/6.00 a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 37.49/6.00 inference('demod', [status(thm)],
% 37.49/6.00 [zip_derived_cl27556, zip_derived_cl27562,
% 37.49/6.00 zip_derived_cl27562, zip_derived_cl27562,
% 37.49/6.00 zip_derived_cl27562, zip_derived_cl27562, zip_derived_cl27562])).
% 37.49/6.00 thf(zip_derived_cl27566, plain, ($false),
% 37.49/6.00 inference('simplify', [status(thm)], [zip_derived_cl27565])).
% 37.49/6.00
% 37.49/6.00 % SZS output end Refutation
% 37.49/6.00
% 37.49/6.00
% 37.49/6.00 % Terminating...
% 37.95/6.10 % Runner terminated.
% 37.95/6.12 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------