%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWV825-1 : TPTP v9.2.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.x6VnN1DUYQ true
% Computer : n010.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:02 PM UTC 2025
% Result : Unsatisfiable 135.62s 20.04s
% Output : Refutation 135.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SWV825-1 : TPTP v9.2.0. Released v4.1.0.
% 0.08/0.15 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.x6VnN1DUYQ true
% 0.14/0.35 % Computer : n010.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 12:34:53 EDT 2025
% 0.14/0.35 % CPUTime :
% 0.14/0.35 % Running portfolio for 300 s
% 0.14/0.35 % File : /export/starexec/sandbox2/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.19/0.59 % Total configuration time : 435
% 0.19/0.59 % Estimated wc time : 1092
% 0.19/0.59 % Estimated cpu time (7 cpus) : 156.0
% 0.19/0.66 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.19/0.69 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.19/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.19/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.19/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.19/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 1.32/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 135.62/20.04 % Solved by fo/fo6_bce.sh.
% 135.62/20.04 % BCE start: 537
% 135.62/20.04 % BCE eliminated: 50
% 135.62/20.04 % PE start: 487
% 135.62/20.04 logic: eq
% 135.62/20.04 % PE eliminated: 0
% 135.62/20.04 % done 2252 iterations in 19.360s
% 135.62/20.04 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 135.62/20.04 % SZS output start Refutation
% 135.62/20.04 thf(c_Set_Oinsert_type, type, c_Set_Oinsert: $i > $i).
% 135.62/20.04 thf(v_G_type, type, v_G: $i).
% 135.62/20.04 thf(v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3_type, type, v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3:
% 135.62/20.04 $i > $i > $i > $i > $i > $i > $i).
% 135.62/20.04 thf(v_P_H_type, type, v_P_H: $i).
% 135.62/20.04 thf(v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2_type, type, v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2:
% 135.62/20.04 $i > $i > $i > $i > $i).
% 135.62/20.04 thf(tc_fun_type, type, tc_fun: $i > $i > $i).
% 135.62/20.04 thf(c_Orderings_Obot__class_Obot_type, type, c_Orderings_Obot__class_Obot:
% 135.62/20.04 $i > $i).
% 135.62/20.04 thf(tc_bool_type, type, tc_bool: $i).
% 135.62/20.04 thf(v_c_type, type, v_c: $i).
% 135.62/20.04 thf(v_Z_type, type, v_Z: $i > $i > $i > $i).
% 135.62/20.04 thf(v_P_type, type, v_P: $i).
% 135.62/20.04 thf(c_Hoare__Mirabelle_Otriple_Otriple_type, type, c_Hoare__Mirabelle_Otriple_Otriple:
% 135.62/20.04 $i > $i > $i > $i > $i).
% 135.62/20.04 thf(hAPP_type, type, hAPP: $i > $i > $i).
% 135.62/20.04 thf(tc_Hoare__Mirabelle_Otriple_type, type, tc_Hoare__Mirabelle_Otriple:
% 135.62/20.04 $i > $i).
% 135.62/20.04 thf(t_a_type, type, t_a: $i).
% 135.62/20.04 thf(v_Q_type, type, v_Q: $i).
% 135.62/20.04 thf(v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1_type, type, v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1:
% 135.62/20.04 $i > $i > $i > $i > $i).
% 135.62/20.04 thf(c_Hoare__Mirabelle_Ohoare__derivs_type, type, c_Hoare__Mirabelle_Ohoare__derivs:
% 135.62/20.04 $i > $i > $i > $o).
% 135.62/20.04 thf(hBOOL_type, type, hBOOL: $i > $o).
% 135.62/20.04 thf(v_Q_H_type, type, v_Q_H: $i).
% 135.62/20.04 thf(cls_conjecture_2, conjecture,
% 135.62/20.04 (~( ( ~( hBOOL @ ( hAPP @ ( hAPP @ v_P @ V_s ) @ V_sa ) ) ) |
% 135.62/20.04 ( hBOOL @
% 135.62/20.04 ( hAPP @ ( hAPP @ v_P_H @ ( v_Z @ V_s @ V_sa @ V_s_H ) ) @ V_sa ) ) |
% 135.62/20.04 ( hBOOL @ ( hAPP @ ( hAPP @ v_Q @ V_s ) @ V_s_H ) ) ))).
% 135.62/20.04 thf(zf_stmt_0, negated_conjecture,
% 135.62/20.04 (( ~( hBOOL @ ( hAPP @ ( hAPP @ v_P @ V_s ) @ V_sa ) ) ) |
% 135.62/20.04 ( hBOOL @
% 135.62/20.04 ( hAPP @ ( hAPP @ v_P_H @ ( v_Z @ V_s @ V_sa @ V_s_H ) ) @ V_sa ) ) |
% 135.62/20.04 ( hBOOL @ ( hAPP @ ( hAPP @ v_Q @ V_s ) @ V_s_H ) )),
% 135.62/20.04 inference('cnf.neg', [status(esa)], [cls_conjecture_2])).
% 135.62/20.04 thf(zip_derived_cl509, plain,
% 135.62/20.04 (![X0 : $i, X1 : $i, X2 : $i]:
% 135.62/20.04 (~ (hBOOL @ (hAPP @ (hAPP @ v_P @ X0) @ X1))
% 135.62/20.04 | (hBOOL @ (hAPP @ (hAPP @ v_P_H @ (v_Z @ X0 @ X1 @ X2)) @ X1))
% 135.62/20.04 | (hBOOL @ (hAPP @ (hAPP @ v_Q @ X0) @ X2)))),
% 135.62/20.04 inference('cnf', [status(esa)], [zf_stmt_0])).
% 135.62/20.04 thf(cls_conseq_1, axiom,
% 135.62/20.04 (( c_Hoare__Mirabelle_Ohoare__derivs @
% 135.62/20.04 V_G @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( c_Set_Oinsert @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @
% 135.62/20.04 ( c_Hoare__Mirabelle_Otriple_Otriple @ V_P @ V_c @ V_Q @ t_a ) ) @
% 135.62/20.04 ( c_Orderings_Obot__class_Obot @
% 135.62/20.04 ( tc_fun @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) @ tc_bool ) ) ) @
% 135.62/20.04 t_a ) |
% 135.62/20.04 ( hBOOL @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( hAPP @ V_xa @ V_Z_H ) @
% 135.62/20.04 ( v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3 @
% 135.62/20.04 V_G @ V_P @ V_Q @ V_c @ V_x @ V_xa ) ) ) |
% 135.62/20.04 ( ~( hBOOL @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( hAPP @ V_x @ V_Z_H ) @
% 135.62/20.04 ( v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2 @
% 135.62/20.04 V_G @ V_P @ V_Q @ V_c ) ) ) ) |
% 135.62/20.04 ( ~( c_Hoare__Mirabelle_Ohoare__derivs @
% 135.62/20.04 V_G @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( c_Set_Oinsert @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @
% 135.62/20.04 ( c_Hoare__Mirabelle_Otriple_Otriple @ V_x @ V_c @ V_xa @ t_a ) ) @
% 135.62/20.04 ( c_Orderings_Obot__class_Obot @
% 135.62/20.04 ( tc_fun @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) @ tc_bool ) ) ) @
% 135.62/20.04 t_a ) ))).
% 135.62/20.04 thf(zip_derived_cl478, plain,
% 135.62/20.04 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i]:
% 135.62/20.04 ( (c_Hoare__Mirabelle_Ohoare__derivs @ X0 @
% 135.62/20.04 (hAPP @
% 135.62/20.04 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.04 (c_Hoare__Mirabelle_Otriple_Otriple @ X1 @ X2 @ X3 @ t_a)) @
% 135.62/20.04 (c_Orderings_Obot__class_Obot @
% 135.62/20.04 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.04 t_a)
% 135.62/20.04 | (hBOOL @
% 135.62/20.04 (hAPP @ (hAPP @ X4 @ X5) @
% 135.62/20.04 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3 @ X0 @
% 135.62/20.04 X1 @ X3 @ X2 @ X6 @ X4)))
% 135.62/20.04 | ~ (hBOOL @
% 135.62/20.04 (hAPP @ (hAPP @ X6 @ X5) @
% 135.62/20.04 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2 @ X0 @
% 135.62/20.04 X1 @ X3 @ X2)))
% 135.62/20.04 | ~ (c_Hoare__Mirabelle_Ohoare__derivs @ X0 @
% 135.62/20.04 (hAPP @
% 135.62/20.04 (hAPP @
% 135.62/20.04 (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.04 (c_Hoare__Mirabelle_Otriple_Otriple @ X6 @ X2 @ X4 @ t_a)) @
% 135.62/20.04 (c_Orderings_Obot__class_Obot @
% 135.62/20.04 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.04 t_a))),
% 135.62/20.04 inference('cnf', [status(esa)], [cls_conseq_1])).
% 135.62/20.04 thf(zip_derived_cl31178, plain,
% 135.62/20.04 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i]:
% 135.62/20.04 ( (hBOOL @ (hAPP @ (hAPP @ v_Q @ X5) @ X4))
% 135.62/20.04 | ~ (hBOOL @
% 135.62/20.04 (hAPP @ (hAPP @ v_P @ X5) @
% 135.62/20.04 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2 @ X3 @
% 135.62/20.04 X2 @ X1 @ X0)))
% 135.62/20.04 | (c_Hoare__Mirabelle_Ohoare__derivs @ X3 @
% 135.62/20.04 (hAPP @
% 135.62/20.04 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.04 (c_Hoare__Mirabelle_Otriple_Otriple @ X2 @ X0 @ X1 @ t_a)) @
% 135.62/20.04 (c_Orderings_Obot__class_Obot @
% 135.62/20.04 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.04 t_a)
% 135.62/20.04 | (hBOOL @
% 135.62/20.04 (hAPP @
% 135.62/20.04 (hAPP @ X6 @
% 135.62/20.04 (v_Z @ X5 @
% 135.62/20.04 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2 @ X3 @
% 135.62/20.04 X2 @ X1 @ X0) @
% 135.62/20.04 X4)) @
% 135.62/20.04 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3 @ X3 @
% 135.62/20.04 X2 @ X1 @ X0 @ v_P_H @ X6)))
% 135.62/20.04 | ~ (c_Hoare__Mirabelle_Ohoare__derivs @ X3 @
% 135.62/20.04 (hAPP @
% 135.62/20.04 (hAPP @
% 135.62/20.04 (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.04 (c_Hoare__Mirabelle_Otriple_Otriple @ v_P_H @ X0 @ X6 @ t_a)) @
% 135.62/20.04 (c_Orderings_Obot__class_Obot @
% 135.62/20.04 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.04 t_a))),
% 135.62/20.04 inference('s_sup-', [status(thm)], [zip_derived_cl509, zip_derived_cl478])).
% 135.62/20.04 thf(cls_conseq_0, axiom,
% 135.62/20.04 (( c_Hoare__Mirabelle_Ohoare__derivs @
% 135.62/20.04 V_G @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( c_Set_Oinsert @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @
% 135.62/20.04 ( c_Hoare__Mirabelle_Otriple_Otriple @ V_P @ V_c @ V_Q @ t_a ) ) @
% 135.62/20.04 ( c_Orderings_Obot__class_Obot @
% 135.62/20.04 ( tc_fun @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) @ tc_bool ) ) ) @
% 135.62/20.04 t_a ) |
% 135.62/20.04 ( hBOOL @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 V_P @
% 135.62/20.04 ( v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @
% 135.62/20.04 V_G @ V_P @ V_Q @ V_c ) ) @
% 135.62/20.04 ( v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2 @
% 135.62/20.04 V_G @ V_P @ V_Q @ V_c ) ) ))).
% 135.62/20.04 thf(zip_derived_cl482, plain,
% 135.62/20.04 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 135.62/20.04 ( (c_Hoare__Mirabelle_Ohoare__derivs @ X0 @
% 135.62/20.04 (hAPP @
% 135.62/20.04 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.04 (c_Hoare__Mirabelle_Otriple_Otriple @ X1 @ X2 @ X3 @ t_a)) @
% 135.62/20.04 (c_Orderings_Obot__class_Obot @
% 135.62/20.04 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.04 t_a)
% 135.62/20.04 | (hBOOL @
% 135.62/20.04 (hAPP @
% 135.62/20.04 (hAPP @ X1 @
% 135.62/20.04 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @ X0 @
% 135.62/20.04 X1 @ X3 @ X2)) @
% 135.62/20.04 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2 @ X0 @
% 135.62/20.04 X1 @ X3 @ X2))))),
% 135.62/20.04 inference('cnf', [status(esa)], [cls_conseq_0])).
% 135.62/20.04 thf(cls_conjecture_1, conjecture,
% 135.62/20.04 (c_Hoare__Mirabelle_Ohoare__derivs @
% 135.62/20.04 v_G @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( c_Set_Oinsert @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @
% 135.62/20.04 ( c_Hoare__Mirabelle_Otriple_Otriple @ v_P @ v_c @ v_Q @ t_a ) ) @
% 135.62/20.04 ( c_Orderings_Obot__class_Obot @
% 135.62/20.04 ( tc_fun @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) @ tc_bool ) ) ) @
% 135.62/20.04 t_a)).
% 135.62/20.04 thf(zf_stmt_1, negated_conjecture,
% 135.62/20.04 (~( c_Hoare__Mirabelle_Ohoare__derivs @
% 135.62/20.04 v_G @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( hAPP @
% 135.62/20.04 ( c_Set_Oinsert @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @
% 135.62/20.04 ( c_Hoare__Mirabelle_Otriple_Otriple @ v_P @ v_c @ v_Q @ t_a ) ) @
% 135.62/20.04 ( c_Orderings_Obot__class_Obot @
% 135.62/20.04 ( tc_fun @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) @ tc_bool ) ) ) @
% 135.62/20.04 t_a )),
% 135.62/20.04 inference('cnf.neg', [status(esa)], [cls_conjecture_1])).
% 135.62/20.04 thf(zip_derived_cl508, plain,
% 135.62/20.04 (~ (c_Hoare__Mirabelle_Ohoare__derivs @ v_G @
% 135.62/20.04 (hAPP @
% 135.62/20.04 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.04 (c_Hoare__Mirabelle_Otriple_Otriple @ v_P @ v_c @ v_Q @ t_a)) @
% 135.62/20.04 (c_Orderings_Obot__class_Obot @
% 135.62/20.04 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.04 t_a)),
% 135.62/20.04 inference('cnf', [status(esa)], [zf_stmt_1])).
% 135.62/20.04 thf(zip_derived_cl30449, plain,
% 135.62/20.04 ( (hBOOL @
% 135.62/20.04 (hAPP @
% 135.62/20.04 (hAPP @ v_P @
% 135.62/20.04 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @ v_G @ v_P @
% 135.62/20.04 v_Q @ v_c)) @
% 135.62/20.04 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2 @ v_G @ v_P @
% 135.62/20.04 v_Q @ v_c)))),
% 135.62/20.04 inference('s_sup-', [status(thm)], [zip_derived_cl482, zip_derived_cl508])).
% 135.62/20.04 thf(cls_conjecture_3, conjecture,
% 135.62/20.04 (~( ( ~( hBOOL @ ( hAPP @ ( hAPP @ v_P @ V_s ) @ V_sa ) ) ) |
% 135.62/20.04 ( ~( hBOOL @
% 135.62/20.04 ( hAPP @ ( hAPP @ v_Q_H @ ( v_Z @ V_s @ V_sa @ V_s_H ) ) @ V_s_H ) ) ) |
% 135.62/20.04 ( hBOOL @ ( hAPP @ ( hAPP @ v_Q @ V_s ) @ V_s_H ) ) ))).
% 135.62/20.04 thf(zf_stmt_2, negated_conjecture,
% 135.62/20.04 (( ~( hBOOL @ ( hAPP @ ( hAPP @ v_P @ V_s ) @ V_sa ) ) ) |
% 135.62/20.04 ( ~( hBOOL @
% 135.62/20.04 ( hAPP @ ( hAPP @ v_Q_H @ ( v_Z @ V_s @ V_sa @ V_s_H ) ) @ V_s_H ) ) ) |
% 135.62/20.04 ( hBOOL @ ( hAPP @ ( hAPP @ v_Q @ V_s ) @ V_s_H ) )),
% 135.62/20.04 inference('cnf.neg', [status(esa)], [cls_conjecture_3])).
% 135.62/20.04 thf(zip_derived_cl510, plain,
% 135.62/20.04 (![X0 : $i, X1 : $i, X2 : $i]:
% 135.62/20.04 (~ (hBOOL @ (hAPP @ (hAPP @ v_P @ X0) @ X1))
% 135.62/20.04 | ~ (hBOOL @ (hAPP @ (hAPP @ v_Q_H @ (v_Z @ X0 @ X1 @ X2)) @ X2))
% 135.62/20.04 | (hBOOL @ (hAPP @ (hAPP @ v_Q @ X0) @ X2)))),
% 135.62/20.04 inference('cnf', [status(esa)], [zf_stmt_2])).
% 135.62/20.05 thf(zip_derived_cl30714, plain,
% 135.62/20.05 (![X0 : $i]:
% 135.62/20.05 (~ (hBOOL @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ v_Q_H @
% 135.62/20.05 (v_Z @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @ v_G @
% 135.62/20.05 v_P @ v_Q @ v_c) @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2 @ v_G @
% 135.62/20.05 v_P @ v_Q @ v_c) @
% 135.62/20.05 X0)) @
% 135.62/20.05 X0))
% 135.62/20.05 | (hBOOL @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ v_Q @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @ v_G @
% 135.62/20.05 v_P @ v_Q @ v_c)) @
% 135.62/20.05 X0)))),
% 135.62/20.05 inference('s_sup-', [status(thm)],
% 135.62/20.05 [zip_derived_cl30449, zip_derived_cl510])).
% 135.62/20.05 thf(zip_derived_cl42448, plain,
% 135.62/20.05 ((~ (c_Hoare__Mirabelle_Ohoare__derivs @ v_G @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.05 (c_Hoare__Mirabelle_Otriple_Otriple @ v_P_H @ v_c @ v_Q_H @ t_a)) @
% 135.62/20.05 (c_Orderings_Obot__class_Obot @
% 135.62/20.05 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.05 t_a)
% 135.62/20.05 | (c_Hoare__Mirabelle_Ohoare__derivs @ v_G @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.05 (c_Hoare__Mirabelle_Otriple_Otriple @ v_P @ v_c @ v_Q @ t_a)) @
% 135.62/20.05 (c_Orderings_Obot__class_Obot @
% 135.62/20.05 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.05 t_a)
% 135.62/20.05 | ~ (hBOOL @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ v_P @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @ v_G @
% 135.62/20.05 v_P @ v_Q @ v_c)) @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2 @ v_G @
% 135.62/20.05 v_P @ v_Q @ v_c)))
% 135.62/20.05 | (hBOOL @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ v_Q @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @ v_G @
% 135.62/20.05 v_P @ v_Q @ v_c)) @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3 @ v_G @
% 135.62/20.05 v_P @ v_Q @ v_c @ v_P_H @ v_Q_H)))
% 135.62/20.05 | (hBOOL @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ v_Q @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @ v_G @
% 135.62/20.05 v_P @ v_Q @ v_c)) @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3 @ v_G @
% 135.62/20.05 v_P @ v_Q @ v_c @ v_P_H @ v_Q_H))))),
% 135.62/20.05 inference('s_sup-', [status(thm)],
% 135.62/20.05 [zip_derived_cl31178, zip_derived_cl30714])).
% 135.62/20.05 thf(cls_conjecture_0, conjecture,
% 135.62/20.05 (~( c_Hoare__Mirabelle_Ohoare__derivs @
% 135.62/20.05 v_G @
% 135.62/20.05 ( hAPP @
% 135.62/20.05 ( hAPP @
% 135.62/20.05 ( c_Set_Oinsert @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @
% 135.62/20.05 ( c_Hoare__Mirabelle_Otriple_Otriple @ v_P_H @ v_c @ v_Q_H @ t_a ) ) @
% 135.62/20.05 ( c_Orderings_Obot__class_Obot @
% 135.62/20.05 ( tc_fun @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) @ tc_bool ) ) ) @
% 135.62/20.05 t_a ))).
% 135.62/20.05 thf(zf_stmt_3, negated_conjecture,
% 135.62/20.05 (c_Hoare__Mirabelle_Ohoare__derivs @
% 135.62/20.05 v_G @
% 135.62/20.05 ( hAPP @
% 135.62/20.05 ( hAPP @
% 135.62/20.05 ( c_Set_Oinsert @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @
% 135.62/20.05 ( c_Hoare__Mirabelle_Otriple_Otriple @ v_P_H @ v_c @ v_Q_H @ t_a ) ) @
% 135.62/20.05 ( c_Orderings_Obot__class_Obot @
% 135.62/20.05 ( tc_fun @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) @ tc_bool ) ) ) @
% 135.62/20.05 t_a),
% 135.62/20.05 inference('cnf.neg', [status(esa)], [cls_conjecture_0])).
% 135.62/20.05 thf(zip_derived_cl507, plain,
% 135.62/20.05 ( (c_Hoare__Mirabelle_Ohoare__derivs @ v_G @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.05 (c_Hoare__Mirabelle_Otriple_Otriple @ v_P_H @ v_c @ v_Q_H @ t_a)) @
% 135.62/20.05 (c_Orderings_Obot__class_Obot @
% 135.62/20.05 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.05 t_a)),
% 135.62/20.05 inference('cnf', [status(esa)], [zf_stmt_3])).
% 135.62/20.05 thf(zip_derived_cl508, plain,
% 135.62/20.05 (~ (c_Hoare__Mirabelle_Ohoare__derivs @ v_G @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.05 (c_Hoare__Mirabelle_Otriple_Otriple @ v_P @ v_c @ v_Q @ t_a)) @
% 135.62/20.05 (c_Orderings_Obot__class_Obot @
% 135.62/20.05 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.05 t_a)),
% 135.62/20.05 inference('cnf', [status(esa)], [zf_stmt_1])).
% 135.62/20.05 thf(zip_derived_cl30449, plain,
% 135.62/20.05 ( (hBOOL @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ v_P @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @ v_G @ v_P @
% 135.62/20.05 v_Q @ v_c)) @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2 @ v_G @ v_P @
% 135.62/20.05 v_Q @ v_c)))),
% 135.62/20.05 inference('s_sup-', [status(thm)], [zip_derived_cl482, zip_derived_cl508])).
% 135.62/20.05 thf(zip_derived_cl42585, plain,
% 135.62/20.05 (( (hBOOL @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ v_Q @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @ v_G @ v_P @
% 135.62/20.05 v_Q @ v_c)) @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3 @ v_G @ v_P @
% 135.62/20.05 v_Q @ v_c @ v_P_H @ v_Q_H)))
% 135.62/20.05 | (hBOOL @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ v_Q @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @ v_G @
% 135.62/20.05 v_P @ v_Q @ v_c)) @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3 @ v_G @
% 135.62/20.05 v_P @ v_Q @ v_c @ v_P_H @ v_Q_H))))),
% 135.62/20.05 inference('demod', [status(thm)],
% 135.62/20.05 [zip_derived_cl42448, zip_derived_cl507, zip_derived_cl508,
% 135.62/20.05 zip_derived_cl30449])).
% 135.62/20.05 thf(zip_derived_cl42586, plain,
% 135.62/20.05 ( (hBOOL @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ v_Q @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @ v_G @ v_P @
% 135.62/20.05 v_Q @ v_c)) @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3 @ v_G @ v_P @
% 135.62/20.05 v_Q @ v_c @ v_P_H @ v_Q_H)))),
% 135.62/20.05 inference('simplify', [status(thm)], [zip_derived_cl42585])).
% 135.62/20.05 thf(cls_conseq_2, axiom,
% 135.62/20.05 (( c_Hoare__Mirabelle_Ohoare__derivs @
% 135.62/20.05 V_G @
% 135.62/20.05 ( hAPP @
% 135.62/20.05 ( hAPP @
% 135.62/20.05 ( c_Set_Oinsert @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @
% 135.62/20.05 ( c_Hoare__Mirabelle_Otriple_Otriple @ V_P @ V_c @ V_Q @ t_a ) ) @
% 135.62/20.05 ( c_Orderings_Obot__class_Obot @
% 135.62/20.05 ( tc_fun @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) @ tc_bool ) ) ) @
% 135.62/20.05 t_a ) |
% 135.62/20.05 ( ~( hBOOL @
% 135.62/20.05 ( hAPP @
% 135.62/20.05 ( hAPP @
% 135.62/20.05 V_Q @
% 135.62/20.05 ( v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @
% 135.62/20.05 V_G @ V_P @ V_Q @ V_c ) ) @
% 135.62/20.05 ( v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3 @
% 135.62/20.05 V_G @ V_P @ V_Q @ V_c @ V_x @ V_xa ) ) ) ) |
% 135.62/20.05 ( ~( c_Hoare__Mirabelle_Ohoare__derivs @
% 135.62/20.05 V_G @
% 135.62/20.05 ( hAPP @
% 135.62/20.05 ( hAPP @
% 135.62/20.05 ( c_Set_Oinsert @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) ) @
% 135.62/20.05 ( c_Hoare__Mirabelle_Otriple_Otriple @ V_x @ V_c @ V_xa @ t_a ) ) @
% 135.62/20.05 ( c_Orderings_Obot__class_Obot @
% 135.62/20.05 ( tc_fun @ ( tc_Hoare__Mirabelle_Otriple @ t_a ) @ tc_bool ) ) ) @
% 135.62/20.05 t_a ) ))).
% 135.62/20.05 thf(zip_derived_cl483, plain,
% 135.62/20.05 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 135.62/20.05 ( (c_Hoare__Mirabelle_Ohoare__derivs @ X0 @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.05 (c_Hoare__Mirabelle_Otriple_Otriple @ X1 @ X2 @ X3 @ t_a)) @
% 135.62/20.05 (c_Orderings_Obot__class_Obot @
% 135.62/20.05 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.05 t_a)
% 135.62/20.05 | ~ (hBOOL @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ X3 @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1 @ X0 @
% 135.62/20.05 X1 @ X3 @ X2)) @
% 135.62/20.05 (v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3 @ X0 @
% 135.62/20.05 X1 @ X3 @ X2 @ X4 @ X5)))
% 135.62/20.05 | ~ (c_Hoare__Mirabelle_Ohoare__derivs @ X0 @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.05 (c_Hoare__Mirabelle_Otriple_Otriple @ X4 @ X2 @ X5 @ t_a)) @
% 135.62/20.05 (c_Orderings_Obot__class_Obot @
% 135.62/20.05 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.05 t_a))),
% 135.62/20.05 inference('cnf', [status(esa)], [cls_conseq_2])).
% 135.62/20.05 thf(zip_derived_cl42942, plain,
% 135.62/20.05 (( (c_Hoare__Mirabelle_Ohoare__derivs @ v_G @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.05 (c_Hoare__Mirabelle_Otriple_Otriple @ v_P @ v_c @ v_Q @ t_a)) @
% 135.62/20.05 (c_Orderings_Obot__class_Obot @
% 135.62/20.05 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.05 t_a)
% 135.62/20.05 | ~ (c_Hoare__Mirabelle_Ohoare__derivs @ v_G @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.05 (c_Hoare__Mirabelle_Otriple_Otriple @ v_P_H @ v_c @ v_Q_H @ t_a)) @
% 135.62/20.05 (c_Orderings_Obot__class_Obot @
% 135.62/20.05 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.05 t_a))),
% 135.62/20.05 inference('s_sup-', [status(thm)],
% 135.62/20.05 [zip_derived_cl42586, zip_derived_cl483])).
% 135.62/20.05 thf(zip_derived_cl508, plain,
% 135.62/20.05 (~ (c_Hoare__Mirabelle_Ohoare__derivs @ v_G @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.05 (c_Hoare__Mirabelle_Otriple_Otriple @ v_P @ v_c @ v_Q @ t_a)) @
% 135.62/20.05 (c_Orderings_Obot__class_Obot @
% 135.62/20.05 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.05 t_a)),
% 135.62/20.05 inference('cnf', [status(esa)], [zf_stmt_1])).
% 135.62/20.05 thf(zip_derived_cl507, plain,
% 135.62/20.05 ( (c_Hoare__Mirabelle_Ohoare__derivs @ v_G @
% 135.62/20.05 (hAPP @
% 135.62/20.05 (hAPP @ (c_Set_Oinsert @ (tc_Hoare__Mirabelle_Otriple @ t_a)) @
% 135.62/20.05 (c_Hoare__Mirabelle_Otriple_Otriple @ v_P_H @ v_c @ v_Q_H @ t_a)) @
% 135.62/20.05 (c_Orderings_Obot__class_Obot @
% 135.62/20.05 (tc_fun @ (tc_Hoare__Mirabelle_Otriple @ t_a) @ tc_bool))) @
% 135.62/20.05 t_a)),
% 135.62/20.05 inference('cnf', [status(esa)], [zf_stmt_3])).
% 135.62/20.05 thf(zip_derived_cl42945, plain, ($false),
% 135.62/20.05 inference('demod', [status(thm)],
% 135.62/20.05 [zip_derived_cl42942, zip_derived_cl508, zip_derived_cl507])).
% 135.62/20.05
% 135.62/20.05 % SZS output end Refutation
% 135.62/20.05
% 135.62/20.05
% 135.62/20.05 % Terminating...
% 136.17/20.14 % Runner terminated.
% 136.17/20.16 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------