%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWW328+1 : TPTP v9.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.mUDmKMW90j true
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 05:02:37 PM UTC 2025
% Result : Theorem 4.53s 1.31s
% Output : Refutation 4.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWW328+1 : TPTP v9.2.0. Released v5.2.0.
% 0.11/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.mUDmKMW90j true
% 0.14/0.35 % Computer : n016.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 11:54:08 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.36 % Running in FO mode
% 0.54/0.66 % Total configuration time : 435
% 0.54/0.66 % Estimated wc time : 1092
% 0.54/0.66 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.72 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.57/0.73 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.57/0.76 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.57/0.76 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.57/0.76 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.57/0.76 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.57/0.76 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 4.53/1.31 % Solved by fo/fo4.sh.
% 4.53/1.31 % done 115 iterations in 0.515s
% 4.53/1.31 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 4.53/1.31 % SZS output start Refutation
% 4.53/1.31 thf(v_b_type, type, v_b: $i).
% 4.53/1.31 thf(c_Natural_Oevaln_type, type, c_Natural_Oevaln: $i > $i > $i > $i > $o).
% 4.53/1.31 thf(c_Com_Ocom_OWhile_type, type, c_Com_Ocom_OWhile: $i > $i > $i).
% 4.53/1.31 thf(v_s0_type, type, v_s0: $i).
% 4.53/1.31 thf(v_s1_type, type, v_s1: $i).
% 4.53/1.31 thf(tc_Hoare__Mirabelle_Otriple_type, type, tc_Hoare__Mirabelle_Otriple:
% 4.53/1.31 $i > $i).
% 4.53/1.31 thf(v_ba_type, type, v_ba: $i).
% 4.53/1.31 thf(hAPP_type, type, hAPP: $i > $i > $i).
% 4.53/1.31 thf(sk__9_type, type, sk__9: $i > $i).
% 4.53/1.31 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $o).
% 4.53/1.31 thf(c_member_type, type, c_member: $i > $i).
% 4.53/1.31 thf(t_a_type, type, t_a: $i).
% 4.53/1.31 thf(v_na_type, type, v_na: $i).
% 4.53/1.31 thf(v_P_type, type, v_P: $i > $i > $o).
% 4.53/1.31 thf(v_s2_type, type, v_s2: $i).
% 4.53/1.31 thf(v_c_type, type, v_c: $i).
% 4.53/1.31 thf(sk__11_type, type, sk__11: $i).
% 4.53/1.31 thf(c_Hoare__Mirabelle_Otriple__valid_type, type, c_Hoare__Mirabelle_Otriple__valid:
% 4.53/1.31 $i > $i > $i > $o).
% 4.53/1.31 thf(v_G_type, type, v_G: $i).
% 4.53/1.31 thf(hBOOL_type, type, hBOOL: $i > $o).
% 4.53/1.31 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $o).
% 4.53/1.31 thf(sk__12_type, type, sk__12: $i).
% 4.53/1.31 thf(v_ca_type, type, v_ca: $i).
% 4.53/1.31 thf(conj_5, axiom,
% 4.53/1.31 (( ( c_Com_Ocom_OWhile @ v_ba @ v_ca ) = ( c_Com_Ocom_OWhile @ v_b @ v_c ) ) =>
% 4.53/1.31 ( ( ![B_x:$i]:
% 4.53/1.31 ( ( hBOOL @
% 4.53/1.31 ( hAPP @
% 4.53/1.31 ( hAPP @
% 4.53/1.31 ( c_member @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @ B_x ) @
% 4.53/1.31 v_G ) ) =>
% 4.53/1.31 ( c_Hoare__Mirabelle_Otriple__valid @ t_a @ v_na @ B_x ) ) ) =>
% 4.53/1.31 ( ![B_Z:$i]:
% 4.53/1.31 ( ( v_P @ B_Z @ v_s1 ) =>
% 4.53/1.31 ( ( ~( hBOOL @ ( hAPP @ v_b @ v_s2 ) ) ) & ( v_P @ B_Z @ v_s2 ) ) ) ) ))).
% 4.53/1.31 thf(zf_stmt_0, axiom,
% 4.53/1.31 (![B_Z:$i]:
% 4.53/1.31 ( ( zip_tseitin_5 @ B_Z ) =>
% 4.53/1.31 ( ( v_P @ B_Z @ v_s2 ) & ( ~( hBOOL @ ( hAPP @ v_b @ v_s2 ) ) ) ) ))).
% 4.53/1.31 thf(zip_derived_cl56, plain,
% 4.53/1.31 (![X0 : $i]: ( (v_P @ X0 @ v_s2) | ~ (zip_tseitin_5 @ X0))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_0])).
% 4.53/1.31 thf(conj_6, conjecture,
% 4.53/1.31 (( ( ( v_ba ) = ( v_b ) ) & ( ( v_ca ) = ( v_c ) ) ) =>
% 4.53/1.31 ( ( ![B_x:$i]:
% 4.53/1.31 ( ( hBOOL @
% 4.53/1.31 ( hAPP @
% 4.53/1.31 ( hAPP @
% 4.53/1.31 ( c_member @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @ B_x ) @
% 4.53/1.31 v_G ) ) =>
% 4.53/1.31 ( c_Hoare__Mirabelle_Otriple__valid @ t_a @ v_na @ B_x ) ) ) =>
% 4.53/1.31 ( ![B_Z:$i]:
% 4.53/1.31 ( ( v_P @ B_Z @ v_s0 ) =>
% 4.53/1.31 ( ( v_P @ B_Z @ v_s2 ) & ( ~( hBOOL @ ( hAPP @ v_b @ v_s2 ) ) ) ) ) ) ))).
% 4.53/1.31 thf(zf_stmt_1, negated_conjecture,
% 4.53/1.31 (~( ( ( ( v_ba ) = ( v_b ) ) & ( ( v_ca ) = ( v_c ) ) ) =>
% 4.53/1.31 ( ( ![B_x:$i]:
% 4.53/1.31 ( ( hBOOL @
% 4.53/1.31 ( hAPP @
% 4.53/1.31 ( hAPP @
% 4.53/1.31 ( c_member @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @ B_x ) @
% 4.53/1.31 v_G ) ) =>
% 4.53/1.31 ( c_Hoare__Mirabelle_Otriple__valid @ t_a @ v_na @ B_x ) ) ) =>
% 4.53/1.31 ( ![B_Z:$i]:
% 4.53/1.31 ( ( v_P @ B_Z @ v_s0 ) =>
% 4.53/1.31 ( ( v_P @ B_Z @ v_s2 ) & ( ~( hBOOL @ ( hAPP @ v_b @ v_s2 ) ) ) ) ) ) ) )),
% 4.53/1.31 inference('cnf.neg', [status(esa)], [conj_6])).
% 4.53/1.31 thf(zip_derived_cl61, plain,
% 4.53/1.31 ((~ (v_P @ sk__12 @ v_s2) | (hBOOL @ (hAPP @ v_b @ v_s2)))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_1])).
% 4.53/1.31 thf(zip_derived_cl57, plain,
% 4.53/1.31 (![X0 : $i]: (~ (hBOOL @ (hAPP @ v_b @ v_s2)) | ~ (zip_tseitin_5 @ X0))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_0])).
% 4.53/1.31 thf(zip_derived_cl67, plain,
% 4.53/1.31 (![X0 : $i]: (~ (v_P @ sk__12 @ v_s2) | ~ (zip_tseitin_5 @ X0))),
% 4.53/1.31 inference('sup-', [status(thm)], [zip_derived_cl61, zip_derived_cl57])).
% 4.53/1.31 thf(zip_derived_cl69, plain,
% 4.53/1.31 (![X0 : $i]: (~ (zip_tseitin_5 @ sk__12) | ~ (zip_tseitin_5 @ X0))),
% 4.53/1.31 inference('sup-', [status(thm)], [zip_derived_cl56, zip_derived_cl67])).
% 4.53/1.31 thf(zip_derived_cl70, plain, (~ (zip_tseitin_5 @ sk__12)),
% 4.53/1.31 inference('condensation', [status(thm)], [zip_derived_cl69])).
% 4.53/1.31 thf(zip_derived_cl62, plain, ( (v_P @ sk__12 @ v_s0)),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_1])).
% 4.53/1.31 thf(zip_derived_cl62, plain, ( (v_P @ sk__12 @ v_s0)),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_1])).
% 4.53/1.31 thf(conj_2, axiom, (c_Natural_Oevaln @ v_ca @ v_s0 @ v_na @ v_s1)).
% 4.53/1.31 thf(zip_derived_cl47, plain,
% 4.53/1.31 ( (c_Natural_Oevaln @ v_ca @ v_s0 @ v_na @ v_s1)),
% 4.53/1.31 inference('cnf', [status(esa)], [conj_2])).
% 4.53/1.31 thf(conj_0, axiom,
% 4.53/1.31 (![B_n:$i]:
% 4.53/1.31 ( ( ![B_x:$i]:
% 4.53/1.31 ( ( hBOOL @
% 4.53/1.31 ( hAPP @
% 4.53/1.31 ( hAPP @
% 4.53/1.31 ( c_member @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @ B_x ) @
% 4.53/1.31 v_G ) ) =>
% 4.53/1.31 ( c_Hoare__Mirabelle_Otriple__valid @ t_a @ B_n @ B_x ) ) ) =>
% 4.53/1.31 ( ![B_Z:$i,B_s:$i]:
% 4.53/1.31 ( ( ( v_P @ B_Z @ B_s ) & ( hBOOL @ ( hAPP @ v_b @ B_s ) ) ) =>
% 4.53/1.31 ( ![B_s_H:$i]:
% 4.53/1.31 ( ( c_Natural_Oevaln @ v_c @ B_s @ B_n @ B_s_H ) =>
% 4.53/1.31 ( v_P @ B_Z @ B_s_H ) ) ) ) ) ))).
% 4.53/1.31 thf(zip_derived_cl44, plain,
% 4.53/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 4.53/1.31 (~ (v_P @ X0 @ X1)
% 4.53/1.31 | ~ (hBOOL @ (hAPP @ v_b @ X1))
% 4.53/1.31 | (v_P @ X0 @ X2)
% 4.53/1.31 | ~ (c_Natural_Oevaln @ v_c @ X1 @ X3 @ X2)
% 4.53/1.31 | (hBOOL @
% 4.53/1.31 (hAPP @
% 4.53/1.31 (hAPP @ (c_member @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 4.53/1.31 (sk__9 @ X3)) @
% 4.53/1.31 v_G)))),
% 4.53/1.31 inference('cnf', [status(esa)], [conj_0])).
% 4.53/1.31 thf(zip_derived_cl60, plain, (((v_ca) = (v_c))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_1])).
% 4.53/1.31 thf(zip_derived_cl165, plain,
% 4.53/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 4.53/1.31 (~ (v_P @ X0 @ X1)
% 4.53/1.31 | ~ (hBOOL @ (hAPP @ v_b @ X1))
% 4.53/1.31 | (v_P @ X0 @ X2)
% 4.53/1.31 | ~ (c_Natural_Oevaln @ v_ca @ X1 @ X3 @ X2)
% 4.53/1.31 | (hBOOL @
% 4.53/1.31 (hAPP @
% 4.53/1.31 (hAPP @ (c_member @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 4.53/1.31 (sk__9 @ X3)) @
% 4.53/1.31 v_G)))),
% 4.53/1.31 inference('demod', [status(thm)], [zip_derived_cl44, zip_derived_cl60])).
% 4.53/1.31 thf(zip_derived_cl166, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 ( (hBOOL @
% 4.53/1.31 (hAPP @
% 4.53/1.31 (hAPP @ (c_member @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 4.53/1.31 (sk__9 @ v_na)) @
% 4.53/1.31 v_G))
% 4.53/1.31 | (v_P @ X0 @ v_s1)
% 4.53/1.31 | ~ (hBOOL @ (hAPP @ v_b @ v_s0))
% 4.53/1.31 | ~ (v_P @ X0 @ v_s0))),
% 4.53/1.31 inference('sup-', [status(thm)], [zip_derived_cl47, zip_derived_cl165])).
% 4.53/1.31 thf(conj_1, axiom, (hBOOL @ ( hAPP @ v_ba @ v_s0 ))).
% 4.53/1.31 thf(zip_derived_cl46, plain, ( (hBOOL @ (hAPP @ v_ba @ v_s0))),
% 4.53/1.31 inference('cnf', [status(esa)], [conj_1])).
% 4.53/1.31 thf(zip_derived_cl59, plain, (((v_ba) = (v_b))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_1])).
% 4.53/1.31 thf(zip_derived_cl65, plain, ( (hBOOL @ (hAPP @ v_b @ v_s0))),
% 4.53/1.31 inference('demod', [status(thm)], [zip_derived_cl46, zip_derived_cl59])).
% 4.53/1.31 thf(zip_derived_cl167, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 ( (hBOOL @
% 4.53/1.31 (hAPP @
% 4.53/1.31 (hAPP @ (c_member @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 4.53/1.31 (sk__9 @ v_na)) @
% 4.53/1.31 v_G))
% 4.53/1.31 | (v_P @ X0 @ v_s1)
% 4.53/1.31 | ~ (v_P @ X0 @ v_s0))),
% 4.53/1.31 inference('demod', [status(thm)], [zip_derived_cl166, zip_derived_cl65])).
% 4.53/1.31 thf(zip_derived_cl168, plain,
% 4.53/1.31 (( (v_P @ sk__12 @ v_s1)
% 4.53/1.31 | (hBOOL @
% 4.53/1.31 (hAPP @
% 4.53/1.31 (hAPP @ (c_member @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 4.53/1.31 (sk__9 @ v_na)) @
% 4.53/1.31 v_G)))),
% 4.53/1.31 inference('sup-', [status(thm)], [zip_derived_cl62, zip_derived_cl167])).
% 4.53/1.31 thf(fact_mem__def, axiom,
% 4.53/1.31 (![V_A_2:$i,V_x_2:$i,T_b:$i]:
% 4.53/1.31 ( ( hBOOL @ ( hAPP @ ( hAPP @ ( c_member @ T_b ) @ V_x_2 ) @ V_A_2 ) ) <=>
% 4.53/1.31 ( hBOOL @ ( hAPP @ V_A_2 @ V_x_2 ) ) ))).
% 4.53/1.31 thf(zip_derived_cl38, plain,
% 4.53/1.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 4.53/1.31 ( (hBOOL @ (hAPP @ X0 @ X1))
% 4.53/1.31 | ~ (hBOOL @ (hAPP @ (hAPP @ (c_member @ X2) @ X1) @ X0)))),
% 4.53/1.31 inference('cnf', [status(esa)], [fact_mem__def])).
% 4.53/1.31 thf(zip_derived_cl186, plain,
% 4.53/1.31 (( (v_P @ sk__12 @ v_s1) | (hBOOL @ (hAPP @ v_G @ (sk__9 @ v_na))))),
% 4.53/1.31 inference('sup-', [status(thm)], [zip_derived_cl168, zip_derived_cl38])).
% 4.53/1.31 thf(zip_derived_cl39, plain,
% 4.53/1.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 4.53/1.31 ( (hBOOL @ (hAPP @ (hAPP @ (c_member @ X0) @ X1) @ X2))
% 4.53/1.31 | ~ (hBOOL @ (hAPP @ X2 @ X1)))),
% 4.53/1.31 inference('cnf', [status(esa)], [fact_mem__def])).
% 4.53/1.31 thf(zip_derived_cl63, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 ( (c_Hoare__Mirabelle_Otriple__valid @ t_a @ v_na @ X0)
% 4.53/1.31 | ~ (hBOOL @
% 4.53/1.31 (hAPP @
% 4.53/1.31 (hAPP @ (c_member @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @ X0) @
% 4.53/1.31 v_G)))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_1])).
% 4.53/1.31 thf(zip_derived_cl96, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 (~ (hBOOL @ (hAPP @ v_G @ X0))
% 4.53/1.31 | (c_Hoare__Mirabelle_Otriple__valid @ t_a @ v_na @ X0))),
% 4.53/1.31 inference('sup-', [status(thm)], [zip_derived_cl39, zip_derived_cl63])).
% 4.53/1.31 thf(zip_derived_cl47, plain,
% 4.53/1.31 ( (c_Natural_Oevaln @ v_ca @ v_s0 @ v_na @ v_s1)),
% 4.53/1.31 inference('cnf', [status(esa)], [conj_2])).
% 4.53/1.31 thf(zip_derived_cl45, plain,
% 4.53/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 4.53/1.31 (~ (v_P @ X0 @ X1)
% 4.53/1.31 | ~ (hBOOL @ (hAPP @ v_b @ X1))
% 4.53/1.31 | (v_P @ X0 @ X2)
% 4.53/1.31 | ~ (c_Natural_Oevaln @ v_c @ X1 @ X3 @ X2)
% 4.53/1.31 | ~ (c_Hoare__Mirabelle_Otriple__valid @ t_a @ X3 @ (sk__9 @ X3)))),
% 4.53/1.31 inference('cnf', [status(esa)], [conj_0])).
% 4.53/1.31 thf(zip_derived_cl60, plain, (((v_ca) = (v_c))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_1])).
% 4.53/1.31 thf(zip_derived_cl81, plain,
% 4.53/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 4.53/1.31 (~ (v_P @ X0 @ X1)
% 4.53/1.31 | ~ (hBOOL @ (hAPP @ v_b @ X1))
% 4.53/1.31 | (v_P @ X0 @ X2)
% 4.53/1.31 | ~ (c_Natural_Oevaln @ v_ca @ X1 @ X3 @ X2)
% 4.53/1.31 | ~ (c_Hoare__Mirabelle_Otriple__valid @ t_a @ X3 @ (sk__9 @ X3)))),
% 4.53/1.31 inference('demod', [status(thm)], [zip_derived_cl45, zip_derived_cl60])).
% 4.53/1.31 thf(zip_derived_cl82, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 (~ (c_Hoare__Mirabelle_Otriple__valid @ t_a @ v_na @ (sk__9 @ v_na))
% 4.53/1.31 | (v_P @ X0 @ v_s1)
% 4.53/1.31 | ~ (hBOOL @ (hAPP @ v_b @ v_s0))
% 4.53/1.31 | ~ (v_P @ X0 @ v_s0))),
% 4.53/1.31 inference('sup-', [status(thm)], [zip_derived_cl47, zip_derived_cl81])).
% 4.53/1.31 thf(zip_derived_cl65, plain, ( (hBOOL @ (hAPP @ v_b @ v_s0))),
% 4.53/1.31 inference('demod', [status(thm)], [zip_derived_cl46, zip_derived_cl59])).
% 4.53/1.31 thf(zip_derived_cl83, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 (~ (c_Hoare__Mirabelle_Otriple__valid @ t_a @ v_na @ (sk__9 @ v_na))
% 4.53/1.31 | (v_P @ X0 @ v_s1)
% 4.53/1.31 | ~ (v_P @ X0 @ v_s0))),
% 4.53/1.31 inference('demod', [status(thm)], [zip_derived_cl82, zip_derived_cl65])).
% 4.53/1.31 thf(zip_derived_cl116, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 (~ (hBOOL @ (hAPP @ v_G @ (sk__9 @ v_na)))
% 4.53/1.31 | ~ (v_P @ X0 @ v_s0)
% 4.53/1.31 | (v_P @ X0 @ v_s1))),
% 4.53/1.31 inference('sup-', [status(thm)], [zip_derived_cl96, zip_derived_cl83])).
% 4.53/1.31 thf(zip_derived_cl207, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 ( (v_P @ sk__12 @ v_s1) | (v_P @ X0 @ v_s1) | ~ (v_P @ X0 @ v_s0))),
% 4.53/1.31 inference('sup-', [status(thm)], [zip_derived_cl186, zip_derived_cl116])).
% 4.53/1.31 thf(zip_derived_cl218, plain,
% 4.53/1.31 (( (v_P @ sk__12 @ v_s1) | (v_P @ sk__12 @ v_s1))),
% 4.53/1.31 inference('sup-', [status(thm)], [zip_derived_cl62, zip_derived_cl207])).
% 4.53/1.31 thf(zip_derived_cl219, plain, ( (v_P @ sk__12 @ v_s1)),
% 4.53/1.31 inference('simplify', [status(thm)], [zip_derived_cl218])).
% 4.53/1.31 thf(zf_stmt_2, type, zip_tseitin_5 : $i > $o).
% 4.53/1.31 thf(zf_stmt_3, type, zip_tseitin_4 : $i > $o).
% 4.53/1.31 thf(zf_stmt_4, axiom,
% 4.53/1.31 (![B_x:$i]:
% 4.53/1.31 ( ( ( hBOOL @
% 4.53/1.31 ( hAPP @
% 4.53/1.31 ( hAPP @
% 4.53/1.31 ( c_member @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @ B_x ) @
% 4.53/1.31 v_G ) ) =>
% 4.53/1.31 ( c_Hoare__Mirabelle_Otriple__valid @ t_a @ v_na @ B_x ) ) =>
% 4.53/1.31 ( zip_tseitin_4 @ B_x ) ))).
% 4.53/1.31 thf(zf_stmt_5, axiom,
% 4.53/1.31 (( ( c_Com_Ocom_OWhile @ v_ba @ v_ca ) = ( c_Com_Ocom_OWhile @ v_b @ v_c ) ) =>
% 4.53/1.31 ( ( ![B_x:$i]: ( zip_tseitin_4 @ B_x ) ) =>
% 4.53/1.31 ( ![B_Z:$i]: ( ( v_P @ B_Z @ v_s1 ) => ( zip_tseitin_5 @ B_Z ) ) ) ))).
% 4.53/1.31 thf(zip_derived_cl58, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 (~ (zip_tseitin_4 @ sk__11)
% 4.53/1.31 | ~ (v_P @ X0 @ v_s1)
% 4.53/1.31 | (zip_tseitin_5 @ X0)
% 4.53/1.31 | ((c_Com_Ocom_OWhile @ v_ba @ v_ca)
% 4.53/1.31 != (c_Com_Ocom_OWhile @ v_b @ v_c)))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_5])).
% 4.53/1.31 thf(zip_derived_cl59, plain, (((v_ba) = (v_b))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_1])).
% 4.53/1.31 thf(zip_derived_cl60, plain, (((v_ca) = (v_c))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_1])).
% 4.53/1.31 thf(zip_derived_cl77, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 (~ (zip_tseitin_4 @ sk__11)
% 4.53/1.31 | ~ (v_P @ X0 @ v_s1)
% 4.53/1.31 | (zip_tseitin_5 @ X0)
% 4.53/1.31 | ((c_Com_Ocom_OWhile @ v_b @ v_ca)
% 4.53/1.31 != (c_Com_Ocom_OWhile @ v_b @ v_ca)))),
% 4.53/1.31 inference('demod', [status(thm)],
% 4.53/1.31 [zip_derived_cl58, zip_derived_cl59, zip_derived_cl60])).
% 4.53/1.31 thf(zip_derived_cl78, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 ( (zip_tseitin_5 @ X0)
% 4.53/1.31 | ~ (v_P @ X0 @ v_s1)
% 4.53/1.31 | ~ (zip_tseitin_4 @ sk__11))),
% 4.53/1.31 inference('simplify', [status(thm)], [zip_derived_cl77])).
% 4.53/1.31 thf(zip_derived_cl55, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 ( (zip_tseitin_4 @ X0)
% 4.53/1.31 | (hBOOL @
% 4.53/1.31 (hAPP @
% 4.53/1.31 (hAPP @ (c_member @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @ X0) @
% 4.53/1.31 v_G)))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_4])).
% 4.53/1.31 thf(zip_derived_cl63, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 ( (c_Hoare__Mirabelle_Otriple__valid @ t_a @ v_na @ X0)
% 4.53/1.31 | ~ (hBOOL @
% 4.53/1.31 (hAPP @
% 4.53/1.31 (hAPP @ (c_member @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @ X0) @
% 4.53/1.31 v_G)))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_1])).
% 4.53/1.31 thf(zip_derived_cl85, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 ( (zip_tseitin_4 @ X0)
% 4.53/1.31 | (c_Hoare__Mirabelle_Otriple__valid @ t_a @ v_na @ X0))),
% 4.53/1.31 inference('sup-', [status(thm)], [zip_derived_cl55, zip_derived_cl63])).
% 4.53/1.31 thf(zip_derived_cl54, plain,
% 4.53/1.31 (![X0 : $i]:
% 4.53/1.31 ( (zip_tseitin_4 @ X0)
% 4.53/1.31 | ~ (c_Hoare__Mirabelle_Otriple__valid @ t_a @ v_na @ X0))),
% 4.53/1.31 inference('cnf', [status(esa)], [zf_stmt_4])).
% 4.53/1.31 thf(zip_derived_cl89, plain, (![X0 : $i]: (zip_tseitin_4 @ X0)),
% 4.53/1.31 inference('clc', [status(thm)], [zip_derived_cl85, zip_derived_cl54])).
% 4.53/1.31 thf(zip_derived_cl90, plain,
% 4.53/1.31 (![X0 : $i]: ( (zip_tseitin_5 @ X0) | ~ (v_P @ X0 @ v_s1))),
% 4.53/1.31 inference('demod', [status(thm)], [zip_derived_cl78, zip_derived_cl89])).
% 4.53/1.31 thf(zip_derived_cl220, plain, ( (zip_tseitin_5 @ sk__12)),
% 4.53/1.31 inference('sup-', [status(thm)], [zip_derived_cl219, zip_derived_cl90])).
% 4.53/1.31 thf(zip_derived_cl222, plain, ($false),
% 4.53/1.31 inference('demod', [status(thm)], [zip_derived_cl70, zip_derived_cl220])).
% 4.53/1.31
% 4.53/1.31 % SZS output end Refutation
% 4.53/1.31
% 4.53/1.31
% 4.53/1.31 % Terminating...
% 5.14/1.37 % Runner terminated.
% 5.14/1.38 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------