%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : TOP051-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.1NmXEezN0i true
% Computer : n004.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 0.50s 1.05s
% Output : Refutation 0.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : TOP051-1 : TPTP v9.2.0. Released v8.1.0.
% 0.13/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.1NmXEezN0i true
% 0.13/0.33 % Computer : n004.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed Oct 1 15:42:08 EDT 2025
% 0.13/0.33 % CPUTime :
% 0.13/0.33 % Running portfolio for 300 s
% 0.13/0.33 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.33 % Number of cores: 8
% 0.13/0.34 % Python version: Python 3.6.8
% 0.13/0.34 % Running in FO mode
% 0.46/0.60 % Total configuration time : 435
% 0.46/0.60 % Estimated wc time : 1092
% 0.46/0.60 % Estimated cpu time (7 cpus) : 156.0
% 0.49/0.69 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.49/0.72 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.49/0.72 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.49/0.72 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.49/0.72 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.50/0.72 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.50/0.72 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.50/1.05 % Solved by fo/fo4.sh.
% 0.50/1.05 % done 175 iterations in 0.298s
% 0.50/1.05 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.50/1.05 % SZS output start Refutation
% 0.50/1.05 thf(a7_type, type, a7: $i).
% 0.50/1.05 thf(a10_type, type, a10: $i).
% 0.50/1.05 thf(a9_type, type, a9: $i).
% 0.50/1.05 thf(a2_type, type, a2: $i).
% 0.50/1.05 thf(a6_type, type, a6: $i).
% 0.50/1.05 thf(product_type, type, product: $i > $i > $i).
% 0.50/1.05 thf(tuple_type, type, tuple: $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i).
% 0.50/1.05 thf(a11_type, type, a11: $i).
% 0.50/1.05 thf(a4_type, type, a4: $i).
% 0.50/1.05 thf(a3_type, type, a3: $i).
% 0.50/1.05 thf(a1_type, type, a1: $i).
% 0.50/1.05 thf(a8_type, type, a8: $i).
% 0.50/1.05 thf(a5_type, type, a5: $i).
% 0.50/1.05 thf(goal, conjecture,
% 0.50/1.05 (( tuple @ a1 @ a6 @ a5 @ a2 @ a7 @ a3 @ a4 @ a9 @ a10 @ a8 ) =
% 0.50/1.05 ( tuple @ a2 @ a7 @ a6 @ a3 @ a8 @ a4 @ a5 @ a10 @ a11 @ a9 ))).
% 0.50/1.05 thf(zf_stmt_0, negated_conjecture,
% 0.50/1.05 (( tuple @ a1 @ a6 @ a5 @ a2 @ a7 @ a3 @ a4 @ a9 @ a10 @ a8 ) !=
% 0.50/1.05 ( tuple @ a2 @ a7 @ a6 @ a3 @ a8 @ a4 @ a5 @ a10 @ a11 @ a9 )),
% 0.50/1.05 inference('cnf.neg', [status(esa)], [goal])).
% 0.50/1.05 thf(zip_derived_cl13, plain,
% 0.50/1.05 (((tuple @ a1 @ a6 @ a5 @ a2 @ a7 @ a3 @ a4 @ a9 @ a10 @ a8)
% 0.50/1.05 != (tuple @ a2 @ a7 @ a6 @ a3 @ a8 @ a4 @ a5 @ a10 @ a11 @ a9))),
% 0.50/1.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.50/1.05 thf(knot_08, axiom, (( product @ a7 @ a3 ) = ( a8 ))).
% 0.50/1.05 thf(zip_derived_cl9, plain, (((product @ a7 @ a3) = (a8))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_08])).
% 0.50/1.05 thf(involutory_quandle, axiom, (( product @ X @ X ) = ( X ))).
% 0.50/1.05 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle])).
% 0.50/1.05 thf(involutory_quandle_02, axiom,
% 0.50/1.05 (( product @ ( product @ X @ Y ) @ Z ) =
% 0.50/1.05 ( product @ ( product @ X @ Z ) @ ( product @ Y @ Z ) ))).
% 0.50/1.05 thf(zip_derived_cl2, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X2) @ X1)
% 0.50/1.05 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 0.50/1.05 thf(zip_derived_cl64, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X1) @ X0)
% 0.50/1.05 = (product @ X0 @ (product @ X1 @ X0)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl269, plain,
% 0.50/1.05 (((product @ a8 @ a7) = (product @ a7 @ (product @ a3 @ a7)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl9, zip_derived_cl64])).
% 0.50/1.05 thf(knot_03, axiom, (( product @ a2 @ a7 ) = ( a3 ))).
% 0.50/1.05 thf(zip_derived_cl4, plain, (((product @ a2 @ a7) = (a3))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_03])).
% 0.50/1.05 thf(involutory_quandle_01, axiom,
% 0.50/1.05 (( product @ ( product @ X @ Y ) @ Y ) = ( X ))).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl19, plain, (((product @ a3 @ a7) = (a2))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl4, zip_derived_cl1])).
% 0.50/1.05 thf(knot_07, axiom, (( product @ a6 @ a2 ) = ( a7 ))).
% 0.50/1.05 thf(zip_derived_cl8, plain, (((product @ a6 @ a2) = (a7))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_07])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl18, plain, (((product @ a7 @ a2) = (a6))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl8, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl294, plain, (((product @ a8 @ a7) = (a6))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl269, zip_derived_cl19, zip_derived_cl18])).
% 0.50/1.05 thf(zip_derived_cl64, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X1) @ X0)
% 0.50/1.05 = (product @ X0 @ (product @ X1 @ X0)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl331, plain,
% 0.50/1.05 (((product @ a6 @ a8) = (product @ a8 @ (product @ a7 @ a8)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl294, zip_derived_cl64])).
% 0.50/1.05 thf(knot_06, axiom, (( product @ a5 @ a9 ) = ( a6 ))).
% 0.50/1.05 thf(zip_derived_cl7, plain, (((product @ a5 @ a9) = (a6))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_06])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl24, plain, (((product @ a6 @ a9) = (a5))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl7, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl64, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X1) @ X0)
% 0.50/1.05 = (product @ X0 @ (product @ X1 @ X0)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl264, plain,
% 0.50/1.05 (((product @ a5 @ a6) = (product @ a6 @ (product @ a9 @ a6)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl24, zip_derived_cl64])).
% 0.50/1.05 thf(knot_09, axiom, (( product @ a8 @ a6 ) = ( a9 ))).
% 0.50/1.05 thf(zip_derived_cl10, plain, (((product @ a8 @ a6) = (a9))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_09])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl26, plain, (((product @ a9 @ a6) = (a8))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl10, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl290, plain, (((product @ a5 @ a6) = (product @ a6 @ a8))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl264, zip_derived_cl26])).
% 0.50/1.05 thf(zip_derived_cl9, plain, (((product @ a7 @ a3) = (a8))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_08])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl20, plain, (((product @ a8 @ a3) = (a7))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl9, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl64, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X1) @ X0)
% 0.50/1.05 = (product @ X0 @ (product @ X1 @ X0)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl282, plain,
% 0.50/1.05 (((product @ a7 @ a8) = (product @ a8 @ (product @ a3 @ a8)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl20, zip_derived_cl64])).
% 0.50/1.05 thf(zip_derived_cl19, plain, (((product @ a3 @ a7) = (a2))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl4, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl64, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X1) @ X0)
% 0.50/1.05 = (product @ X0 @ (product @ X1 @ X0)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl271, plain,
% 0.50/1.05 (((product @ a2 @ a3) = (product @ a3 @ (product @ a7 @ a3)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl19, zip_derived_cl64])).
% 0.50/1.05 thf(zip_derived_cl9, plain, (((product @ a7 @ a3) = (a8))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_08])).
% 0.50/1.05 thf(zip_derived_cl295, plain, (((product @ a2 @ a3) = (product @ a3 @ a8))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl271, zip_derived_cl9])).
% 0.50/1.05 thf(knot, axiom, (( product @ a1 @ a6 ) = ( a2 ))).
% 0.50/1.05 thf(zip_derived_cl3, plain, (((product @ a1 @ a6) = (a2))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl17, plain, (((product @ a2 @ a6) = (a1))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl3, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl3, plain, (((product @ a1 @ a6) = (a2))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot])).
% 0.50/1.05 thf(zip_derived_cl2, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X2) @ X1)
% 0.50/1.05 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 0.50/1.05 thf(zip_derived_cl44, plain,
% 0.50/1.05 (![X0 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ a1) @ a6)
% 0.50/1.05 = (product @ (product @ X0 @ a6) @ a2))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl3, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl95, plain,
% 0.50/1.05 (((product @ (product @ a2 @ a1) @ a6) = (product @ a1 @ a2))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl17, zip_derived_cl44])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl182, plain,
% 0.50/1.05 (((product @ (product @ a1 @ a2) @ a6) = (product @ a2 @ a1))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl95, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl17, plain, (((product @ a2 @ a6) = (a1))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl3, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl64, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X1) @ X0)
% 0.50/1.05 = (product @ X0 @ (product @ X1 @ X0)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl265, plain,
% 0.50/1.05 (((product @ a1 @ a2) = (product @ a2 @ (product @ a6 @ a2)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl17, zip_derived_cl64])).
% 0.50/1.05 thf(zip_derived_cl8, plain, (((product @ a6 @ a2) = (a7))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_07])).
% 0.50/1.05 thf(zip_derived_cl4, plain, (((product @ a2 @ a7) = (a3))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_03])).
% 0.50/1.05 thf(zip_derived_cl291, plain, (((product @ a1 @ a2) = (a3))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl265, zip_derived_cl8, zip_derived_cl4])).
% 0.50/1.05 thf(zip_derived_cl307, plain, (((product @ a3 @ a6) = (product @ a2 @ a1))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl182, zip_derived_cl291])).
% 0.50/1.05 thf(zip_derived_cl64, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X1) @ X0)
% 0.50/1.05 = (product @ X0 @ (product @ X1 @ X0)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl570, plain,
% 0.50/1.05 (((product @ (product @ a3 @ a6) @ a2)
% 0.50/1.05 = (product @ a2 @ (product @ a1 @ a2)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl307, zip_derived_cl64])).
% 0.50/1.05 thf(zip_derived_cl44, plain,
% 0.50/1.05 (![X0 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ a1) @ a6)
% 0.50/1.05 = (product @ (product @ X0 @ a6) @ a2))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl3, zip_derived_cl2])).
% 0.50/1.05 thf(knot_04, axiom, (( product @ a3 @ a1 ) = ( a4 ))).
% 0.50/1.05 thf(zip_derived_cl5, plain, (((product @ a3 @ a1) = (a4))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_04])).
% 0.50/1.05 thf(zip_derived_cl291, plain, (((product @ a1 @ a2) = (a3))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl265, zip_derived_cl8, zip_derived_cl4])).
% 0.50/1.05 thf(zip_derived_cl576, plain, (((product @ a4 @ a6) = (product @ a2 @ a3))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl570, zip_derived_cl44, zip_derived_cl5,
% 0.50/1.05 zip_derived_cl291])).
% 0.50/1.05 thf(zip_derived_cl601, plain, (((product @ a4 @ a6) = (product @ a3 @ a8))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl295, zip_derived_cl576])).
% 0.50/1.05 thf(zip_derived_cl1406, plain,
% 0.50/1.05 (((product @ a7 @ a8) = (product @ a8 @ (product @ a4 @ a6)))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl282, zip_derived_cl601])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl2, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X2) @ X1)
% 0.50/1.05 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 0.50/1.05 thf(zip_derived_cl42, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/1.05 ((product @ (product @ X2 @ (product @ X0 @ X1)) @ X1)
% 0.50/1.05 = (product @ (product @ X2 @ X1) @ X0))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl1, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl1420, plain,
% 0.50/1.05 (((product @ (product @ a7 @ a8) @ a6)
% 0.50/1.05 = (product @ (product @ a8 @ a6) @ a4))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl1406, zip_derived_cl42])).
% 0.50/1.05 thf(zip_derived_cl10, plain, (((product @ a8 @ a6) = (a9))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_09])).
% 0.50/1.05 thf(knot_10, axiom, (( product @ a9 @ a4 ) = ( a10 ))).
% 0.50/1.05 thf(zip_derived_cl11, plain, (((product @ a9 @ a4) = (a10))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_10])).
% 0.50/1.05 thf(zip_derived_cl1424, plain,
% 0.50/1.05 (((product @ (product @ a7 @ a8) @ a6) = (a10))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1420, zip_derived_cl10, zip_derived_cl11])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl1425, plain,
% 0.50/1.05 (((product @ a10 @ a6) = (product @ a7 @ a8))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl1424, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl1554, plain,
% 0.50/1.05 (((product @ a5 @ a6) = (product @ a8 @ (product @ a10 @ a6)))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl331, zip_derived_cl290, zip_derived_cl1425])).
% 0.50/1.05 thf(zip_derived_cl42, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/1.05 ((product @ (product @ X2 @ (product @ X0 @ X1)) @ X1)
% 0.50/1.05 = (product @ (product @ X2 @ X1) @ X0))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl1, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl1568, plain,
% 0.50/1.05 (((product @ (product @ a5 @ a6) @ a6)
% 0.50/1.05 = (product @ (product @ a8 @ a6) @ a10))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl1554, zip_derived_cl42])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl10, plain, (((product @ a8 @ a6) = (a9))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_09])).
% 0.50/1.05 thf(zip_derived_cl11, plain, (((product @ a9 @ a4) = (a10))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_10])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl25, plain, (((product @ a10 @ a4) = (a9))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl11, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl64, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X1) @ X0)
% 0.50/1.05 = (product @ X0 @ (product @ X1 @ X0)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl274, plain,
% 0.50/1.05 (((product @ a9 @ a10) = (product @ a10 @ (product @ a4 @ a10)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl25, zip_derived_cl64])).
% 0.50/1.05 thf(knot_05, axiom, (( product @ a4 @ a10 ) = ( a5 ))).
% 0.50/1.05 thf(zip_derived_cl6, plain, (((product @ a4 @ a10) = (a5))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_05])).
% 0.50/1.05 thf(knot_11, axiom, (( product @ a10 @ a5 ) = ( a11 ))).
% 0.50/1.05 thf(zip_derived_cl12, plain, (((product @ a10 @ a5) = (a11))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_11])).
% 0.50/1.05 thf(zip_derived_cl297, plain, (((product @ a9 @ a10) = (a11))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl274, zip_derived_cl6, zip_derived_cl12])).
% 0.50/1.05 thf(zip_derived_cl1574, plain, (((a5) = (a11))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1568, zip_derived_cl1, zip_derived_cl10,
% 0.50/1.05 zip_derived_cl297])).
% 0.50/1.05 thf(zip_derived_cl1576, plain,
% 0.50/1.05 (((tuple @ a1 @ a6 @ a5 @ a2 @ a7 @ a3 @ a4 @ a9 @ a10 @ a8)
% 0.50/1.05 != (tuple @ a2 @ a7 @ a6 @ a3 @ a8 @ a4 @ a5 @ a10 @ a5 @ a9))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl13, zip_derived_cl1574])).
% 0.50/1.05 thf(zip_derived_cl6, plain, (((product @ a4 @ a10) = (a5))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_05])).
% 0.50/1.05 thf(zip_derived_cl64, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X1) @ X0)
% 0.50/1.05 = (product @ X0 @ (product @ X1 @ X0)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl273, plain,
% 0.50/1.05 (((product @ a5 @ a4) = (product @ a4 @ (product @ a10 @ a4)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl64])).
% 0.50/1.05 thf(zip_derived_cl25, plain, (((product @ a10 @ a4) = (a9))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl11, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl296, plain, (((product @ a5 @ a4) = (product @ a4 @ a9))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl273, zip_derived_cl25])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl361, plain,
% 0.50/1.05 (((product @ (product @ a4 @ a9) @ a4) = (a5))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl296, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl12, plain, (((product @ a10 @ a5) = (a11))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_11])).
% 0.50/1.05 thf(zip_derived_cl64, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X1) @ X0)
% 0.50/1.05 = (product @ X0 @ (product @ X1 @ X0)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl275, plain,
% 0.50/1.05 (((product @ a11 @ a10) = (product @ a10 @ (product @ a5 @ a10)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl12, zip_derived_cl64])).
% 0.50/1.05 thf(zip_derived_cl6, plain, (((product @ a4 @ a10) = (a5))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_05])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl22, plain, (((product @ a5 @ a10) = (a4))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl25, plain, (((product @ a10 @ a4) = (a9))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl11, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl298, plain, (((product @ a11 @ a10) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl275, zip_derived_cl22, zip_derived_cl25])).
% 0.50/1.05 thf(zip_derived_cl1574, plain, (((a5) = (a11))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1568, zip_derived_cl1, zip_derived_cl10,
% 0.50/1.05 zip_derived_cl297])).
% 0.50/1.05 thf(zip_derived_cl22, plain, (((product @ a5 @ a10) = (a4))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl1579, plain, (((a4) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl298, zip_derived_cl1574, zip_derived_cl22])).
% 0.50/1.05 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle])).
% 0.50/1.05 thf(zip_derived_cl1579, plain, (((a4) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl298, zip_derived_cl1574, zip_derived_cl22])).
% 0.50/1.05 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle])).
% 0.50/1.05 thf(zip_derived_cl1597, plain, (((a9) = (a5))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl361, zip_derived_cl1579, zip_derived_cl0,
% 0.50/1.05 zip_derived_cl1579, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl296, plain, (((product @ a5 @ a4) = (product @ a4 @ a9))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl273, zip_derived_cl25])).
% 0.50/1.05 thf(zip_derived_cl1579, plain, (((a4) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl298, zip_derived_cl1574, zip_derived_cl22])).
% 0.50/1.05 thf(zip_derived_cl7, plain, (((product @ a5 @ a9) = (a6))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_06])).
% 0.50/1.05 thf(zip_derived_cl1579, plain, (((a4) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl298, zip_derived_cl1574, zip_derived_cl22])).
% 0.50/1.05 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle])).
% 0.50/1.05 thf(zip_derived_cl1596, plain, (((a6) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl296, zip_derived_cl1579, zip_derived_cl7,
% 0.50/1.05 zip_derived_cl1579, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1647, plain, (((a6) = (a5))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1597, zip_derived_cl1596])).
% 0.50/1.05 thf(zip_derived_cl576, plain, (((product @ a4 @ a6) = (product @ a2 @ a3))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl570, zip_derived_cl44, zip_derived_cl5,
% 0.50/1.05 zip_derived_cl291])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl602, plain,
% 0.50/1.05 (((product @ (product @ a4 @ a6) @ a3) = (a2))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl576, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl1579, plain, (((a4) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl298, zip_derived_cl1574, zip_derived_cl22])).
% 0.50/1.05 thf(zip_derived_cl26, plain, (((product @ a9 @ a6) = (a8))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl10, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl20, plain, (((product @ a8 @ a3) = (a7))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl9, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl1602, plain, (((a7) = (a2))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl602, zip_derived_cl1579, zip_derived_cl26,
% 0.50/1.05 zip_derived_cl20])).
% 0.50/1.05 thf(zip_derived_cl1425, plain,
% 0.50/1.05 (((product @ a10 @ a6) = (product @ a7 @ a8))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl1424, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl1449, plain,
% 0.50/1.05 (((product @ (product @ a10 @ a6) @ a8) = (a7))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl1425, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl12, plain, (((product @ a10 @ a5) = (a11))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_11])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl23, plain, (((product @ a11 @ a5) = (a10))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl12, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl1574, plain, (((a5) = (a11))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1568, zip_derived_cl1, zip_derived_cl10,
% 0.50/1.05 zip_derived_cl297])).
% 0.50/1.05 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle])).
% 0.50/1.05 thf(zip_derived_cl1577, plain, (((a5) = (a10))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl23, zip_derived_cl1574, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl290, plain, (((product @ a5 @ a6) = (product @ a6 @ a8))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl264, zip_derived_cl26])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl347, plain,
% 0.50/1.05 (((product @ (product @ a5 @ a6) @ a8) = (a6))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl290, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl1589, plain, (((a6) = (a7))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1449, zip_derived_cl1577, zip_derived_cl347])).
% 0.50/1.05 thf(zip_derived_cl1648, plain, (((a6) = (a2))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1602, zip_derived_cl1589])).
% 0.50/1.05 thf(zip_derived_cl1589, plain, (((a6) = (a7))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1449, zip_derived_cl1577, zip_derived_cl347])).
% 0.50/1.05 thf(zip_derived_cl5, plain, (((product @ a3 @ a1) = (a4))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_04])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl21, plain, (((product @ a4 @ a1) = (a3))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl5, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl1579, plain, (((a4) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl298, zip_derived_cl1574, zip_derived_cl22])).
% 0.50/1.05 thf(zip_derived_cl26, plain, (((product @ a9 @ a6) = (a8))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl10, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl44, plain,
% 0.50/1.05 (![X0 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ a1) @ a6)
% 0.50/1.05 = (product @ (product @ X0 @ a6) @ a2))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl3, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl96, plain,
% 0.50/1.05 (((product @ (product @ a9 @ a1) @ a6) = (product @ a8 @ a2))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl26, zip_derived_cl44])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl191, plain,
% 0.50/1.05 (((product @ (product @ (product @ a9 @ a1) @ a6) @ a2) = (a8))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl96, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl2, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X2) @ X1)
% 0.50/1.05 = (product @ (product @ X0 @ X1) @ (product @ X2 @ X1)))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_02])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl38, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/1.05 ((product @ (product @ (product @ X2 @ X1) @ X0) @ (product @ X1 @ X0))
% 0.50/1.05 = (product @ X2 @ X0))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl2, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl218, plain,
% 0.50/1.05 (((product @ a8 @ (product @ a6 @ a2))
% 0.50/1.05 = (product @ (product @ a9 @ a1) @ a2))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl191, zip_derived_cl38])).
% 0.50/1.05 thf(zip_derived_cl8, plain, (((product @ a6 @ a2) = (a7))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_07])).
% 0.50/1.05 thf(zip_derived_cl220, plain,
% 0.50/1.05 (((product @ a8 @ a7) = (product @ (product @ a9 @ a1) @ a2))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl218, zip_derived_cl8])).
% 0.50/1.05 thf(zip_derived_cl294, plain, (((product @ a8 @ a7) = (a6))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl269, zip_derived_cl19, zip_derived_cl18])).
% 0.50/1.05 thf(zip_derived_cl328, plain,
% 0.50/1.05 (((a6) = (product @ (product @ a9 @ a1) @ a2))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl220, zip_derived_cl294])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl622, plain, (((product @ a6 @ a2) = (product @ a9 @ a1))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl328, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl8, plain, (((product @ a6 @ a2) = (a7))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_07])).
% 0.50/1.05 thf(zip_derived_cl632, plain, (((a7) = (product @ a9 @ a1))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl622, zip_derived_cl8])).
% 0.50/1.05 thf(zip_derived_cl1593, plain, (((a7) = (a3))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl21, zip_derived_cl1579, zip_derived_cl632])).
% 0.50/1.05 thf(zip_derived_cl1589, plain, (((a6) = (a7))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1449, zip_derived_cl1577, zip_derived_cl347])).
% 0.50/1.05 thf(zip_derived_cl1633, plain, (((a6) = (a3))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1593, zip_derived_cl1589])).
% 0.50/1.05 thf(zip_derived_cl1596, plain, (((a6) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl296, zip_derived_cl1579, zip_derived_cl7,
% 0.50/1.05 zip_derived_cl1579, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl601, plain, (((product @ a4 @ a6) = (product @ a3 @ a8))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl295, zip_derived_cl576])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl612, plain,
% 0.50/1.05 (((product @ (product @ a4 @ a6) @ a8) = (a3))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl601, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl1579, plain, (((a4) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl298, zip_derived_cl1574, zip_derived_cl22])).
% 0.50/1.05 thf(zip_derived_cl26, plain, (((product @ a9 @ a6) = (a8))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl10, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle])).
% 0.50/1.05 thf(zip_derived_cl1603, plain, (((a8) = (a3))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl612, zip_derived_cl1579, zip_derived_cl26,
% 0.50/1.05 zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1633, plain, (((a6) = (a3))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1593, zip_derived_cl1589])).
% 0.50/1.05 thf(zip_derived_cl1654, plain, (((a8) = (a6))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1603, zip_derived_cl1633])).
% 0.50/1.05 thf(zip_derived_cl1648, plain, (((a6) = (a2))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1602, zip_derived_cl1589])).
% 0.50/1.05 thf(zip_derived_cl1589, plain, (((a6) = (a7))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1449, zip_derived_cl1577, zip_derived_cl347])).
% 0.50/1.05 thf(zip_derived_cl1633, plain, (((a6) = (a3))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1593, zip_derived_cl1589])).
% 0.50/1.05 thf(zip_derived_cl1654, plain, (((a8) = (a6))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1603, zip_derived_cl1633])).
% 0.50/1.05 thf(zip_derived_cl1647, plain, (((a6) = (a5))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1597, zip_derived_cl1596])).
% 0.50/1.05 thf(zip_derived_cl1647, plain, (((a6) = (a5))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1597, zip_derived_cl1596])).
% 0.50/1.05 thf(zip_derived_cl1596, plain, (((a6) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl296, zip_derived_cl1579, zip_derived_cl7,
% 0.50/1.05 zip_derived_cl1579, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1655, plain,
% 0.50/1.05 (((tuple @ a1 @ a6 @ a6 @ a6 @ a6 @ a6 @ a4 @ a6 @ a10 @ a6)
% 0.50/1.05 != (tuple @ a6 @ a6 @ a6 @ a6 @ a6 @ a4 @ a6 @ a10 @ a6 @ a6))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1576, zip_derived_cl1647, zip_derived_cl1648,
% 0.50/1.05 zip_derived_cl1589, zip_derived_cl1633, zip_derived_cl1596,
% 0.50/1.05 zip_derived_cl1654, zip_derived_cl1648, zip_derived_cl1589,
% 0.50/1.05 zip_derived_cl1633, zip_derived_cl1654, zip_derived_cl1647,
% 0.50/1.05 zip_derived_cl1647, zip_derived_cl1596])).
% 0.50/1.05 thf(zip_derived_cl1577, plain, (((a5) = (a10))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl23, zip_derived_cl1574, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl22, plain, (((product @ a5 @ a10) = (a4))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl64, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]:
% 0.50/1.05 ((product @ (product @ X0 @ X1) @ X0)
% 0.50/1.05 = (product @ X0 @ (product @ X1 @ X0)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 0.50/1.05 thf(zip_derived_cl276, plain,
% 0.50/1.05 (((product @ a4 @ a5) = (product @ a5 @ (product @ a10 @ a5)))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl22, zip_derived_cl64])).
% 0.50/1.05 thf(zip_derived_cl12, plain, (((product @ a10 @ a5) = (a11))),
% 0.50/1.05 inference('cnf', [status(esa)], [knot_11])).
% 0.50/1.05 thf(zip_derived_cl299, plain, (((product @ a4 @ a5) = (product @ a5 @ a11))),
% 0.50/1.05 inference('demod', [status(thm)], [zip_derived_cl276, zip_derived_cl12])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl367, plain,
% 0.50/1.05 (((product @ (product @ a4 @ a5) @ a11) = (a5))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl299, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl1574, plain, (((a5) = (a11))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1568, zip_derived_cl1, zip_derived_cl10,
% 0.50/1.05 zip_derived_cl297])).
% 0.50/1.05 thf(zip_derived_cl1, plain,
% 0.50/1.05 (![X0 : $i, X1 : $i]: ((product @ (product @ X0 @ X1) @ X1) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle_01])).
% 0.50/1.05 thf(zip_derived_cl1581, plain, (((a4) = (a5))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl367, zip_derived_cl1574, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl1579, plain, (((a4) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl298, zip_derived_cl1574, zip_derived_cl22])).
% 0.50/1.05 thf(zip_derived_cl1609, plain, (((a9) = (a5))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1581, zip_derived_cl1579])).
% 0.50/1.05 thf(zip_derived_cl1619, plain, (((a9) = (a10))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1577, zip_derived_cl1609])).
% 0.50/1.05 thf(zip_derived_cl1596, plain, (((a6) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl296, zip_derived_cl1579, zip_derived_cl7,
% 0.50/1.05 zip_derived_cl1579, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1659, plain, (((a6) = (a10))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1619, zip_derived_cl1596])).
% 0.50/1.05 thf(zip_derived_cl1659, plain, (((a6) = (a10))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1619, zip_derived_cl1596])).
% 0.50/1.05 thf(zip_derived_cl1660, plain,
% 0.50/1.05 (((tuple @ a1 @ a6 @ a6 @ a6 @ a6 @ a6 @ a4 @ a6 @ a6 @ a6)
% 0.50/1.05 != (tuple @ a6 @ a6 @ a6 @ a6 @ a6 @ a4 @ a6 @ a6 @ a6 @ a6))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1655, zip_derived_cl1659, zip_derived_cl1659])).
% 0.50/1.05 thf(zip_derived_cl17, plain, (((product @ a2 @ a6) = (a1))),
% 0.50/1.05 inference('sup+', [status(thm)], [zip_derived_cl3, zip_derived_cl1])).
% 0.50/1.05 thf(zip_derived_cl1648, plain, (((a6) = (a2))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1602, zip_derived_cl1589])).
% 0.50/1.05 thf(zip_derived_cl0, plain, (![X0 : $i]: ((product @ X0 @ X0) = (X0))),
% 0.50/1.05 inference('cnf', [status(esa)], [involutory_quandle])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1579, plain, (((a4) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl298, zip_derived_cl1574, zip_derived_cl22])).
% 0.50/1.05 thf(zip_derived_cl1596, plain, (((a6) = (a9))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl296, zip_derived_cl1579, zip_derived_cl7,
% 0.50/1.05 zip_derived_cl1579, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1645, plain, (((a4) = (a6))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1579, zip_derived_cl1596])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1719, plain, (((a4) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1645, zip_derived_cl1650])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1719, plain, (((a4) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1645, zip_derived_cl1650])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1650, plain, (((a6) = (a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl17, zip_derived_cl1648, zip_derived_cl0])).
% 0.50/1.05 thf(zip_derived_cl1726, plain,
% 0.50/1.05 (((tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1)
% 0.50/1.05 != (tuple @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1 @ a1))),
% 0.50/1.05 inference('demod', [status(thm)],
% 0.50/1.05 [zip_derived_cl1660, zip_derived_cl1650, zip_derived_cl1650,
% 0.50/1.05 zip_derived_cl1650, zip_derived_cl1650, zip_derived_cl1650,
% 0.50/1.05 zip_derived_cl1719, zip_derived_cl1650, zip_derived_cl1650,
% 0.50/1.05 zip_derived_cl1650, zip_derived_cl1650, zip_derived_cl1650,
% 0.50/1.05 zip_derived_cl1650, zip_derived_cl1650, zip_derived_cl1650,
% 0.50/1.05 zip_derived_cl1719, zip_derived_cl1650, zip_derived_cl1650,
% 0.50/1.05 zip_derived_cl1650, zip_derived_cl1650])).
% 0.50/1.05 thf(zip_derived_cl1727, plain, ($false),
% 0.50/1.05 inference('simplify', [status(thm)], [zip_derived_cl1726])).
% 0.50/1.05
% 0.50/1.05 % SZS output end Refutation
% 0.50/1.05
% 0.50/1.05
% 0.50/1.05 % Terminating...
% 3.64/1.12 % Runner terminated.
% 3.64/1.13 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------