%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : ITP141^1 : TPTP v9.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.qInxv3dZmf true
% Computer : n031.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 04:38:57 PM UTC 2025
% Result : Theorem 42.55s 9.20s
% Output : Refutation 42.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.15 % Problem : ITP141^1 : TPTP v9.2.0. Released v7.5.0.
% 0.03/0.16 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.qInxv3dZmf true
% 0.12/0.36 % Computer : n031.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8042.1875MB
% 0.12/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Wed Oct 1 15:31:38 EDT 2025
% 0.12/0.36 % CPUTime :
% 0.12/0.36 % Running portfolio for 300 s
% 0.12/0.36 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.36 % Number of cores: 8
% 0.12/0.36 % Python version: Python 3.6.8
% 0.12/0.36 % Running in HO mode
% 0.49/0.61 % Total configuration time : 828
% 0.49/0.61 % Estimated wc time : 1656
% 0.49/0.61 % Estimated cpu time (8 cpus) : 207.0
% 0.70/0.75 % /export/starexec/sandbox2/solver/bin/lams/40_c.s.sh running for 80s
% 0.79/0.79 % /export/starexec/sandbox2/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.79/0.81 % /export/starexec/sandbox2/solver/bin/lams/40_c_ic.sh running for 80s
% 0.79/0.83 % /export/starexec/sandbox2/solver/bin/lams/40_noforms.sh running for 90s
% 0.79/0.84 % /export/starexec/sandbox2/solver/bin/lams/15_e_short1.sh running for 30s
% 0.79/0.84 % /export/starexec/sandbox2/solver/bin/lams/40_b.comb.sh running for 70s
% 0.79/0.85 % /export/starexec/sandbox2/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.85/0.87 % /export/starexec/sandbox2/solver/bin/lams/30_sp5.sh running for 60s
% 0.90/1.10 % /export/starexec/sandbox2/solver/bin/lams/30_b.l.sh running for 90s
% 42.55/9.20 % Solved by lams/40_c_ic.sh.
% 42.55/9.20 % done 715 iterations in 8.301s
% 42.55/9.20 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 42.55/9.20 % SZS output start Refutation
% 42.55/9.20 thf(com_type, type, com: $tType).
% 42.55/9.20 thf(state_type, type, state: $tType).
% 42.55/9.20 thf(a_type, type, a: $tType).
% 42.55/9.20 thf(set_Pr1590995257tate_o_type, type, set_Pr1590995257tate_o: $tType).
% 42.55/9.20 thf(produc696469763tate_o_type, type, produc696469763tate_o: $tType).
% 42.55/9.20 thf(produc1115495963_state_type, type, produc1115495963_state: $tType).
% 42.55/9.20 thf(set_Pr795498619_state_type, type, set_Pr795498619_state: $tType).
% 42.55/9.20 thf(produc204914599tate_o_type, type, produc204914599tate_o: $tType).
% 42.55/9.20 thf(exec_type, type, exec: state > com > state > $o).
% 42.55/9.20 thf('#l_lift4125_type', type, '#l_lift4125': state > $o).
% 42.55/9.20 thf(pHoare382919414oare_a_type, type, pHoare382919414oare_a: set_Pr1590995257tate_o >
% 42.55/9.20 (a > state > $o) >
% 42.55/9.20 com >
% 42.55/9.20 (a > state > $o) > $o).
% 42.55/9.20 thf(qa_type, type, qa: a > state > $o).
% 42.55/9.20 thf(sk__9_type, type, sk__9: a).
% 42.55/9.20 thf(sk__7_type, type, sk__7: state).
% 42.55/9.20 thf(zip_tseitin_4_type, type, zip_tseitin_4: state > state > state > $o).
% 42.55/9.20 thf(termi_type, type, termi: com > state > $o).
% 42.55/9.20 thf(sk__8_type, type, sk__8: state).
% 42.55/9.20 thf(produc33908149tate_o_type, type, produc33908149tate_o: (a > state > $o) >
% 42.55/9.20 produc204914599tate_o > produc696469763tate_o).
% 42.55/9.20 thf(call_type, type, call: com).
% 42.55/9.20 thf(produc64584659_state_type, type, produc64584659_state: state > state > produc1115495963_state).
% 42.55/9.20 thf(sk__2_type, type, sk__2: state > state > state > a).
% 42.55/9.20 thf(while_type, type, while: (state > $o) > com > com).
% 42.55/9.20 thf(body_type, type, body: com).
% 42.55/9.20 thf(zip_tseitin_3_type, type, zip_tseitin_3: a > state > state > state > $o).
% 42.55/9.20 thf(member1389040324_state_type, type, member1389040324_state: produc1115495963_state >
% 42.55/9.20 set_Pr795498619_state > $o).
% 42.55/9.20 thf(x_type, type, x: state).
% 42.55/9.20 thf(sk__11_type, type, sk__11: state).
% 42.55/9.20 thf(bot_bo170732493tate_o_type, type, bot_bo170732493tate_o: set_Pr1590995257tate_o).
% 42.55/9.20 thf(produc1948644831tate_o_type, type, produc1948644831tate_o: com >
% 42.55/9.20 (a > state > $o) > produc204914599tate_o).
% 42.55/9.20 thf(insert2053719859tate_o_type, type, insert2053719859tate_o: produc696469763tate_o >
% 42.55/9.20 set_Pr1590995257tate_o > set_Pr1590995257tate_o).
% 42.55/9.20 thf(sk__5_type, type, sk__5: state > state).
% 42.55/9.20 thf(zip_tseitin_1_type, type, zip_tseitin_1: state > a > state > $o).
% 42.55/9.20 thf(sk__6_type, type, sk__6: state > state).
% 42.55/9.20 thf(zip_tseitin_5_type, type, zip_tseitin_5: state > $o).
% 42.55/9.20 thf(zip_tseitin_0_type, type, zip_tseitin_0: state > a > state > $o).
% 42.55/9.20 thf(pa_type, type, pa: a > state > $o).
% 42.55/9.20 thf(sk__3_type, type, sk__3: state > a).
% 42.55/9.20 thf(r_type, type, r: set_Pr795498619_state).
% 42.55/9.20 thf(zip_tseitin_2_type, type, zip_tseitin_2: a > state > state > $o).
% 42.55/9.20 thf(sk__10_type, type, sk__10: a).
% 42.55/9.20 thf(sk__4_type, type, sk__4: state > state).
% 42.55/9.20 thf(conj_2, conjecture,
% 42.55/9.20 (( ![S:state,T:state]:
% 42.55/9.20 ( ( ![Z:a]:
% 42.55/9.20 ( ( qa @ Z @ T ) | ( ( S ) != ( x ) ) | ( ~( pa @ Z @ S ) ) ) ) |
% 42.55/9.20 ( ~( exec @ S @ body @ T ) ) ) ) &
% 42.55/9.20 ( ![Z:a,S:state]:
% 42.55/9.20 ( ( termi @ body @ S ) | ( ( S ) != ( x ) ) | ( ~( pa @ Z @ S ) ) ) ))).
% 42.55/9.20 thf(zf_stmt_0, negated_conjecture,
% 42.55/9.20 (~( ( ![S:state,T:state]:
% 42.55/9.20 ( ( ![Z:a]:
% 42.55/9.20 ( ( qa @ Z @ T ) | ( ( S ) != ( x ) ) | ( ~( pa @ Z @ S ) ) ) ) |
% 42.55/9.20 ( ~( exec @ S @ body @ T ) ) ) ) &
% 42.55/9.20 ( ![Z:a,S:state]:
% 42.55/9.20 ( ( termi @ body @ S ) | ( ( S ) != ( x ) ) | ( ~( pa @ Z @ S ) ) ) ) )),
% 42.55/9.20 inference('cnf.neg', [status(esa)], [conj_2])).
% 42.55/9.20 thf(zip_derived_cl32, plain, ((((sk__7) = (x)) | ((sk__11) = (x)))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl32, plain, ((((sk__7) = (x)) | ((sk__11) = (x)))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl26, plain, (( (pa @ sk__9 @ sk__7) | ((sk__11) = (x)))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl37, plain,
% 42.55/9.20 (( (pa @ sk__9 @ x) | ((sk__11) = (x)) | ((sk__11) = (x)))),
% 42.55/9.20 inference('sup+', [status(thm)], [zip_derived_cl32, zip_derived_cl26])).
% 42.55/9.20 thf(zip_derived_cl38, plain, ((((sk__11) = (x)) | (pa @ sk__9 @ x))),
% 42.55/9.20 inference('simplify', [status(thm)], [zip_derived_cl37])).
% 42.55/9.20 thf(zip_derived_cl34, plain,
% 42.55/9.20 (( (exec @ sk__7 @ body @ sk__8) | ~ (termi @ body @ sk__11))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(conj_0, axiom,
% 42.55/9.20 (![S6:state]:
% 42.55/9.20 ( ( pHoare382919414oare_a @
% 42.55/9.20 ( insert2053719859tate_o @
% 42.55/9.20 ( produc33908149tate_o @
% 42.55/9.20 ( ^[Z4:a,S4:state]:
% 42.55/9.20 ( ( member1389040324_state @
% 42.55/9.20 ( produc64584659_state @ S4 @ S6 ) @ r ) &
% 42.55/9.20 ( pa @ Z4 @ S4 ) ) ) @
% 42.55/9.20 ( produc1948644831tate_o @ call @ qa ) ) @
% 42.55/9.20 bot_bo170732493tate_o ) @
% 42.55/9.20 ( ^[Z4:a,S4:state]: ( ( ( S4 ) = ( S6 ) ) & ( pa @ Z4 @ S4 ) ) ) @
% 42.55/9.20 body @ qa ) &
% 42.55/9.20 ( ( ( ![Z:a,S:state]:
% 42.55/9.20 ( ( ( member1389040324_state @
% 42.55/9.20 ( produc64584659_state @ S @ S6 ) @ r ) &
% 42.55/9.20 ( pa @ Z @ S ) ) =>
% 42.55/9.20 ( termi @ body @ S ) ) ) &
% 42.55/9.20 ( ![S:state,T:state]:
% 42.55/9.20 ( ( exec @ S @ body @ T ) =>
% 42.55/9.20 ( ![Z:a]:
% 42.55/9.20 ( ( ( member1389040324_state @
% 42.55/9.20 ( produc64584659_state @ S @ S6 ) @ r ) &
% 42.55/9.20 ( pa @ Z @ S ) ) =>
% 42.55/9.20 ( qa @ Z @ T ) ) ) ) ) ) =>
% 42.55/9.20 ( ( ![Z2:a,S7:state]:
% 42.55/9.20 ( ( ( ( S7 ) = ( S6 ) ) & ( pa @ Z2 @ S7 ) ) =>
% 42.55/9.20 ( termi @ body @ S7 ) ) ) &
% 42.55/9.20 ( ![S7:state,T4:state]:
% 42.55/9.20 ( ( exec @ S7 @ body @ T4 ) =>
% 42.55/9.20 ( ![Z2:a]:
% 42.55/9.20 ( ( ( ( S7 ) = ( S6 ) ) & ( pa @ Z2 @ S7 ) ) =>
% 42.55/9.20 ( qa @ Z2 @ T4 ) ) ) ) ) ) ) ))).
% 42.55/9.20 thf(zf_stmt_1, axiom,
% 42.55/9.20 (![S6:state]:
% 42.55/9.20 ( ( zip_tseitin_5 @ S6 ) =>
% 42.55/9.20 ( ( ![S7:state,T4:state]:
% 42.55/9.20 ( ( exec @ S7 @ body @ T4 ) =>
% 42.55/9.20 ( ![Z2:a]:
% 42.55/9.20 ( ( ( pa @ Z2 @ S7 ) & ( ( S7 ) = ( S6 ) ) ) => ( qa @ Z2 @ T4 ) ) ) ) ) &
% 42.55/9.20 ( ![Z2:a,S7:state]:
% 42.55/9.20 ( ( ( pa @ Z2 @ S7 ) & ( ( S7 ) = ( S6 ) ) ) =>
% 42.55/9.20 ( termi @ body @ S7 ) ) ) ) ))).
% 42.55/9.20 thf(zip_derived_cl19, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : state, X3 : a]:
% 42.55/9.20 (~ (exec @ X0 @ body @ X1)
% 42.55/9.20 | ((X0) != (X2))
% 42.55/9.20 | (qa @ X3 @ X1)
% 42.55/9.20 | ~ (pa @ X3 @ X0)
% 42.55/9.20 | ~ (zip_tseitin_5 @ X2))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_1])).
% 42.55/9.20 thf(zip_derived_cl436, plain,
% 42.55/9.20 (![X1 : state, X2 : state, X3 : a]:
% 42.55/9.20 (~ (zip_tseitin_5 @ X2)
% 42.55/9.20 | ~ (pa @ X3 @ X2)
% 42.55/9.20 | (qa @ X3 @ X1)
% 42.55/9.20 | ~ (exec @ X2 @ body @ X1))),
% 42.55/9.20 inference('simplify', [status(thm)], [zip_derived_cl19])).
% 42.55/9.20 thf(zip_derived_cl439, plain,
% 42.55/9.20 (![X0 : a]:
% 42.55/9.20 (~ (termi @ body @ sk__11)
% 42.55/9.20 | (qa @ X0 @ sk__8)
% 42.55/9.20 | ~ (pa @ X0 @ sk__7)
% 42.55/9.20 | ~ (zip_tseitin_5 @ sk__7))),
% 42.55/9.20 inference('sup-', [status(thm)], [zip_derived_cl34, zip_derived_cl436])).
% 42.55/9.20 thf(zip_derived_cl28, plain,
% 42.55/9.20 ((~ (qa @ sk__9 @ sk__8) | ~ (termi @ body @ sk__11))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl477, plain,
% 42.55/9.20 ((~ (zip_tseitin_5 @ sk__7)
% 42.55/9.20 | ~ (pa @ sk__9 @ sk__7)
% 42.55/9.20 | ~ (termi @ body @ sk__11)
% 42.55/9.20 | ~ (termi @ body @ sk__11))),
% 42.55/9.20 inference('sup-', [status(thm)], [zip_derived_cl439, zip_derived_cl28])).
% 42.55/9.20 thf(zip_derived_cl493, plain,
% 42.55/9.20 ((~ (termi @ body @ sk__11)
% 42.55/9.20 | ~ (pa @ sk__9 @ sk__7)
% 42.55/9.20 | ~ (zip_tseitin_5 @ sk__7))),
% 42.55/9.20 inference('simplify', [status(thm)], [zip_derived_cl477])).
% 42.55/9.20 thf(zip_derived_cl25, plain,
% 42.55/9.20 (( (pa @ sk__9 @ sk__7) | ~ (termi @ body @ sk__11))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl498, plain,
% 42.55/9.20 ((~ (zip_tseitin_5 @ sk__7) | ~ (termi @ body @ sk__11))),
% 42.55/9.20 inference('clc', [status(thm)], [zip_derived_cl493, zip_derived_cl25])).
% 42.55/9.20 thf(zip_derived_cl27, plain,
% 42.55/9.20 (( (pa @ sk__9 @ sk__7) | (pa @ sk__10 @ sk__11))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl33, plain, ((((sk__7) = (x)) | (pa @ sk__10 @ sk__11))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl20, plain,
% 42.55/9.20 (![X0 : a, X1 : state, X2 : state]:
% 42.55/9.20 (~ (pa @ X0 @ X1)
% 42.55/9.20 | ((X1) != (X2))
% 42.55/9.20 | (termi @ body @ X1)
% 42.55/9.20 | ~ (zip_tseitin_5 @ X2))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_1])).
% 42.55/9.20 thf(zip_derived_cl70, plain,
% 42.55/9.20 (![X0 : a, X2 : state]:
% 42.55/9.20 (~ (zip_tseitin_5 @ X2) | (termi @ body @ X2) | ~ (pa @ X0 @ X2))),
% 42.55/9.20 inference('simplify', [status(thm)], [zip_derived_cl20])).
% 42.55/9.20 thf(zip_derived_cl71, plain,
% 42.55/9.20 ((((sk__7) = (x)) | (termi @ body @ sk__11) | ~ (zip_tseitin_5 @ sk__11))),
% 42.55/9.20 inference('sup-', [status(thm)], [zip_derived_cl33, zip_derived_cl70])).
% 42.55/9.20 thf(zip_derived_cl31, plain, ((((sk__7) = (x)) | ~ (termi @ body @ sk__11))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl88, plain,
% 42.55/9.20 ((~ (zip_tseitin_5 @ sk__11) | ((sk__7) = (x)))),
% 42.55/9.20 inference('clc', [status(thm)], [zip_derived_cl71, zip_derived_cl31])).
% 42.55/9.20 thf(zip_derived_cl29, plain, ((~ (qa @ sk__9 @ sk__8) | ((sk__11) = (x)))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl30, plain,
% 42.55/9.20 ((~ (qa @ sk__9 @ sk__8) | (pa @ sk__10 @ sk__11))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl32, plain, ((((sk__7) = (x)) | ((sk__11) = (x)))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl35, plain,
% 42.55/9.20 (( (exec @ sk__7 @ body @ sk__8) | ((sk__11) = (x)))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl39, plain,
% 42.55/9.20 (( (exec @ x @ body @ sk__8) | ((sk__11) = (x)) | ((sk__11) = (x)))),
% 42.55/9.20 inference('sup+', [status(thm)], [zip_derived_cl32, zip_derived_cl35])).
% 42.55/9.20 thf(zip_derived_cl40, plain,
% 42.55/9.20 ((((sk__11) = (x)) | (exec @ x @ body @ sk__8))),
% 42.55/9.20 inference('simplify', [status(thm)], [zip_derived_cl39])).
% 42.55/9.20 thf(zip_derived_cl436, plain,
% 42.55/9.20 (![X1 : state, X2 : state, X3 : a]:
% 42.55/9.20 (~ (zip_tseitin_5 @ X2)
% 42.55/9.20 | ~ (pa @ X3 @ X2)
% 42.55/9.20 | (qa @ X3 @ X1)
% 42.55/9.20 | ~ (exec @ X2 @ body @ X1))),
% 42.55/9.20 inference('simplify', [status(thm)], [zip_derived_cl19])).
% 42.55/9.20 thf(zip_derived_cl440, plain,
% 42.55/9.20 (![X0 : a]:
% 42.55/9.20 (((sk__11) = (x))
% 42.55/9.20 | (qa @ X0 @ sk__8)
% 42.55/9.20 | ~ (pa @ X0 @ x)
% 42.55/9.20 | ~ (zip_tseitin_5 @ x))),
% 42.55/9.20 inference('sup-', [status(thm)], [zip_derived_cl40, zip_derived_cl436])).
% 42.55/9.20 thf(zip_derived_cl36, plain,
% 42.55/9.20 (( (exec @ sk__7 @ body @ sk__8) | (pa @ sk__10 @ sk__11))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zf_stmt_2, axiom,
% 42.55/9.20 (![T:state,S:state,S6:state]:
% 42.55/9.20 ( ( ( exec @ S @ body @ T ) =>
% 42.55/9.20 ( ![Z:a]: ( zip_tseitin_3 @ Z @ T @ S @ S6 ) ) ) =>
% 42.55/9.20 ( zip_tseitin_4 @ T @ S @ S6 ) ))).
% 42.55/9.20 thf(zip_derived_cl17, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : state]:
% 42.55/9.20 ( (zip_tseitin_4 @ X0 @ X1 @ X2)
% 42.55/9.20 | ~ (zip_tseitin_3 @ (sk__2 @ X2 @ X1 @ X0) @ X0 @ X1 @ X2))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_2])).
% 42.55/9.20 thf(zf_stmt_3, axiom,
% 42.55/9.20 (![Z:a,T:state,S:state,S6:state]:
% 42.55/9.20 ( ( ( zip_tseitin_2 @ Z @ S @ S6 ) => ( qa @ Z @ T ) ) =>
% 42.55/9.20 ( zip_tseitin_3 @ Z @ T @ S @ S6 ) ))).
% 42.55/9.20 thf(zip_derived_cl16, plain,
% 42.55/9.20 (![X0 : a, X1 : state, X2 : state, X3 : state]:
% 42.55/9.20 ( (zip_tseitin_3 @ X0 @ X1 @ X2 @ X3)
% 42.55/9.20 | (zip_tseitin_2 @ X0 @ X2 @ X3))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_3])).
% 42.55/9.20 thf(zip_derived_cl404, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : state]:
% 42.55/9.20 ( (zip_tseitin_4 @ X2 @ X1 @ X0)
% 42.55/9.20 | (zip_tseitin_2 @ (sk__2 @ X0 @ X1 @ X2) @ X1 @ X0))),
% 42.55/9.20 inference('sup+', [status(thm)], [zip_derived_cl17, zip_derived_cl16])).
% 42.55/9.20 thf(zf_stmt_4, axiom,
% 42.55/9.20 (![Z:a,S:state,S6:state]:
% 42.55/9.20 ( ( zip_tseitin_2 @ Z @ S @ S6 ) =>
% 42.55/9.20 ( ( pa @ Z @ S ) &
% 42.55/9.20 ( member1389040324_state @ ( produc64584659_state @ S @ S6 ) @ r ) ) ))).
% 42.55/9.20 thf(zip_derived_cl13, plain,
% 42.55/9.20 (![X0 : a, X1 : state, X2 : state]:
% 42.55/9.20 ( (pa @ X0 @ X1) | ~ (zip_tseitin_2 @ X0 @ X1 @ X2))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_4])).
% 42.55/9.20 thf(zip_derived_cl939, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : state]:
% 42.55/9.20 ( (zip_tseitin_4 @ X2 @ X1 @ X0) | (pa @ (sk__2 @ X0 @ X1 @ X2) @ X1))),
% 42.55/9.20 inference('sup-', [status(thm)], [zip_derived_cl404, zip_derived_cl13])).
% 42.55/9.20 thf(zip_derived_cl34, plain,
% 42.55/9.20 (( (exec @ sk__7 @ body @ sk__8) | ~ (termi @ body @ sk__11))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 42.55/9.20 thf(zip_derived_cl19, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : state, X3 : a]:
% 42.55/9.20 (~ (exec @ X0 @ body @ X1)
% 42.55/9.20 | ((X0) != (X2))
% 42.55/9.20 | (qa @ X3 @ X1)
% 42.55/9.20 | ~ (pa @ X3 @ X0)
% 42.55/9.20 | ~ (zip_tseitin_5 @ X2))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_1])).
% 42.55/9.20 thf(zip_derived_cl17, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : state]:
% 42.55/9.20 ( (zip_tseitin_4 @ X0 @ X1 @ X2)
% 42.55/9.20 | ~ (zip_tseitin_3 @ (sk__2 @ X2 @ X1 @ X0) @ X0 @ X1 @ X2))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_2])).
% 42.55/9.20 thf(zip_derived_cl15, plain,
% 42.55/9.20 (![X0 : a, X1 : state, X2 : state, X3 : state]:
% 42.55/9.20 ( (zip_tseitin_3 @ X0 @ X1 @ X2 @ X3) | ~ (qa @ X0 @ X1))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_3])).
% 42.55/9.20 thf(zip_derived_cl405, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : state]:
% 42.55/9.20 ( (zip_tseitin_4 @ X2 @ X1 @ X0)
% 42.55/9.20 | ~ (qa @ (sk__2 @ X0 @ X1 @ X2) @ X2))),
% 42.55/9.20 inference('sup+', [status(thm)], [zip_derived_cl17, zip_derived_cl15])).
% 42.55/9.20 thf(zip_derived_cl20, plain,
% 42.55/9.20 (![X0 : a, X1 : state, X2 : state]:
% 42.55/9.20 (~ (pa @ X0 @ X1)
% 42.55/9.20 | ((X1) != (X2))
% 42.55/9.20 | (termi @ body @ X1)
% 42.55/9.20 | ~ (zip_tseitin_5 @ X2))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_1])).
% 42.55/9.20 thf(zip_derived_cl18, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : state]:
% 42.55/9.20 ( (zip_tseitin_4 @ X0 @ X1 @ X2) | (exec @ X1 @ body @ X0))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_2])).
% 42.55/9.20 thf(zf_stmt_5, axiom,
% 42.55/9.20 (![S:state,Z:a,S6:state]:
% 42.55/9.20 ( ( ( zip_tseitin_0 @ S @ Z @ S6 ) => ( termi @ body @ S ) ) =>
% 42.55/9.20 ( zip_tseitin_1 @ S @ Z @ S6 ) ))).
% 42.55/9.20 thf(zip_derived_cl11, plain,
% 42.55/9.20 (![X0 : state, X1 : a, X2 : state]:
% 42.55/9.20 ( (zip_tseitin_1 @ X0 @ X1 @ X2) | ~ (termi @ body @ X0))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_5])).
% 42.55/9.20 thf(zip_derived_cl404, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : state]:
% 42.55/9.20 ( (zip_tseitin_4 @ X2 @ X1 @ X0)
% 42.55/9.20 | (zip_tseitin_2 @ (sk__2 @ X0 @ X1 @ X2) @ X1 @ X0))),
% 42.55/9.20 inference('sup+', [status(thm)], [zip_derived_cl17, zip_derived_cl16])).
% 42.55/9.20 thf(zip_derived_cl14, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : a]:
% 42.55/9.20 ( (member1389040324_state @ (produc64584659_state @ X0 @ X1) @ r)
% 42.55/9.20 | ~ (zip_tseitin_2 @ X2 @ X0 @ X1))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_4])).
% 42.55/9.20 thf(zip_derived_cl938, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : state]:
% 42.55/9.20 ( (zip_tseitin_4 @ X2 @ X1 @ X0)
% 42.55/9.20 | (member1389040324_state @ (produc64584659_state @ X1 @ X0) @ r))),
% 42.55/9.20 inference('sup-', [status(thm)], [zip_derived_cl404, zip_derived_cl14])).
% 42.55/9.20 thf(zf_stmt_6, type, zip_tseitin_5 : state > $o).
% 42.55/9.20 thf(zf_stmt_7, type, zip_tseitin_4 : state > state > state > $o).
% 42.55/9.20 thf(zf_stmt_8, type, zip_tseitin_3 : a > state > state > state > $o).
% 42.55/9.20 thf(zf_stmt_9, type, zip_tseitin_2 : a > state > state > $o).
% 42.55/9.20 thf(zf_stmt_10, type, zip_tseitin_1 : state > a > state > $o).
% 42.55/9.20 thf(zf_stmt_11, type, zip_tseitin_0 : state > a > state > $o).
% 42.55/9.20 thf(zf_stmt_12, axiom,
% 42.55/9.20 (![S:state,Z:a,S6:state]:
% 42.55/9.20 ( ( zip_tseitin_0 @ S @ Z @ S6 ) =>
% 42.55/9.20 ( ( pa @ Z @ S ) &
% 42.55/9.20 ( member1389040324_state @ ( produc64584659_state @ S @ S6 ) @ r ) ) ))).
% 42.55/9.20 thf(zf_stmt_13, axiom,
% 42.55/9.20 (![S6:state]:
% 42.55/9.20 ( ( ( ( ![S:state,T:state]: ( zip_tseitin_4 @ T @ S @ S6 ) ) &
% 42.55/9.20 ( ![Z:a,S:state]: ( zip_tseitin_1 @ S @ Z @ S6 ) ) ) =>
% 42.55/9.20 ( zip_tseitin_5 @ S6 ) ) &
% 42.55/9.20 ( pHoare382919414oare_a @
% 42.55/9.20 ( insert2053719859tate_o @
% 42.55/9.20 ( produc33908149tate_o @
% 42.55/9.20 ( ^[Z4:a,S4:state]:
% 42.55/9.20 ( ( member1389040324_state @
% 42.55/9.20 ( produc64584659_state @ S4 @ S6 ) @ r ) &
% 42.55/9.20 ( pa @ Z4 @ S4 ) ) ) @
% 42.55/9.20 ( produc1948644831tate_o @ call @ qa ) ) @
% 42.55/9.20 bot_bo170732493tate_o ) @
% 42.55/9.20 ( ^[Z4:a,S4:state]: ( ( ( S4 ) = ( S6 ) ) & ( pa @ Z4 @ S4 ) ) ) @
% 42.55/9.20 body @ qa ) ))).
% 42.55/9.20 thf(zip_derived_cl22, plain,
% 42.55/9.20 (![X0 : state]:
% 42.55/9.20 ( (zip_tseitin_5 @ X0)
% 42.55/9.20 | ~ (zip_tseitin_1 @ (sk__4 @ X0) @ (sk__3 @ X0) @ X0)
% 42.55/9.20 | ~ (zip_tseitin_4 @ (sk__6 @ X0) @ (sk__5 @ X0) @ X0))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_13])).
% 42.55/9.20 thf(fact_220_termi_OWhileFalse, axiom,
% 42.55/9.20 (![B2:( state > $o ),S2:state,C2:com]:
% 42.55/9.20 ( ( ~( B2 @ S2 ) ) => ( termi @ ( while @ B2 @ C2 ) @ S2 ) ))).
% 42.55/9.20 thf(zip_derived_cl5, plain,
% 42.55/9.20 (![X0 : state > $o, X1 : state, X2 : com]:
% 42.55/9.20 ( (X0 @ X1) | (termi @ (while @ X0 @ X2) @ X1))),
% 42.55/9.20 inference('cnf', [status(esa)], [fact_220_termi_OWhileFalse])).
% 42.55/9.20 thf(zip_derived_cl295, plain,
% 42.55/9.20 (![X0 : state, X1 : com]:
% 42.55/9.20 (~ (zip_tseitin_1 @ (sk__4 @ X0) @ (sk__3 @ X0) @ X0)
% 42.55/9.20 | (zip_tseitin_5 @ X0)
% 42.55/9.20 | (termi @
% 42.55/9.20 (while @
% 42.55/9.20 (^[Y0 : state]:
% 42.55/9.20 (zip_tseitin_4 @
% 42.55/9.20 ((^[Y1 : state]: (sk__6 @ ((^[Y2 : state]: (Y2)) @ Y1))) @
% 42.55/9.20 Y0) @
% 42.55/9.20 ((^[Y1 : state]: (sk__5 @ ((^[Y2 : state]: (Y2)) @ Y1))) @
% 42.55/9.20 Y0) @
% 42.55/9.20 ((^[Y1 : state]: (Y1)) @ Y0))) @
% 42.55/9.20 X1) @
% 42.55/9.20 X0))),
% 42.55/9.20 inference('sup+', [status(thm)], [zip_derived_cl22, zip_derived_cl5])).
% 42.55/9.20 thf(zip_derived_cl299, plain,
% 42.55/9.20 (![X0 : state, X1 : com]:
% 42.55/9.20 (~ (zip_tseitin_1 @ (sk__4 @ X0) @ (sk__3 @ X0) @ X0)
% 42.55/9.20 | (zip_tseitin_5 @ X0)
% 42.55/9.20 | (termi @
% 42.55/9.20 (while @
% 42.55/9.20 (^[Y0 : state]:
% 42.55/9.20 (zip_tseitin_4 @ (sk__6 @ Y0) @ (sk__5 @ Y0) @ Y0)) @
% 42.55/9.20 X1) @
% 42.55/9.20 X0))),
% 42.55/9.20 inference('ho_norm', [status(thm)], [zip_derived_cl295])).
% 42.55/9.20 thf(zip_derived_cl5581, plain,
% 42.55/9.20 (![X2 : state]:
% 42.55/9.20 (('#l_lift4125' @ X2)
% 42.55/9.20 = (zip_tseitin_4 @ (sk__6 @ X2) @ (sk__5 @ X2) @ X2))),
% 42.55/9.20 define([status(thm)])).
% 42.55/9.20 thf(zip_derived_cl12, plain,
% 42.55/9.20 (![X0 : state, X1 : a, X2 : state]:
% 42.55/9.20 ( (zip_tseitin_1 @ X0 @ X1 @ X2) | (zip_tseitin_0 @ X0 @ X1 @ X2))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_5])).
% 42.55/9.20 thf(zip_derived_cl22, plain,
% 42.55/9.20 (![X0 : state]:
% 42.55/9.20 ( (zip_tseitin_5 @ X0)
% 42.55/9.20 | ~ (zip_tseitin_1 @ (sk__4 @ X0) @ (sk__3 @ X0) @ X0)
% 42.55/9.20 | ~ (zip_tseitin_4 @ (sk__6 @ X0) @ (sk__5 @ X0) @ X0))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_13])).
% 42.55/9.20 thf(zip_derived_cl10, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : a]:
% 42.55/9.20 ( (member1389040324_state @ (produc64584659_state @ X0 @ X1) @ r)
% 42.55/9.20 | ~ (zip_tseitin_0 @ X0 @ X2 @ X1))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_12])).
% 42.55/9.20 thf(conj_1, axiom,
% 42.55/9.20 (![Y4:state]:
% 42.55/9.20 ( ( member1389040324_state @ ( produc64584659_state @ Y4 @ x ) @ r ) =>
% 42.55/9.20 ( ( ![S7:state,T4:state]:
% 42.55/9.20 ( ( exec @ S7 @ body @ T4 ) =>
% 42.55/9.20 ( ![Z2:a]:
% 42.55/9.20 ( ( ( pa @ Z2 @ S7 ) & ( ( S7 ) = ( Y4 ) ) ) => ( qa @ Z2 @ T4 ) ) ) ) ) &
% 42.55/9.20 ( ![Z2:a,S7:state]:
% 42.55/9.20 ( ( ( pa @ Z2 @ S7 ) & ( ( S7 ) = ( Y4 ) ) ) =>
% 42.55/9.20 ( termi @ body @ S7 ) ) ) ) ))).
% 42.55/9.20 thf(zip_derived_cl24, plain,
% 42.55/9.20 (![X0 : a, X1 : state, X2 : state]:
% 42.55/9.20 (~ (pa @ X0 @ X1)
% 42.55/9.20 | ((X1) != (X2))
% 42.55/9.20 | (termi @ body @ X1)
% 42.55/9.20 | ~ (member1389040324_state @ (produc64584659_state @ X2 @ x) @ r))),
% 42.55/9.20 inference('cnf', [status(esa)], [conj_1])).
% 42.55/9.20 thf(zip_derived_cl23, plain,
% 42.55/9.20 (![X0 : state, X1 : state, X2 : state, X3 : a]:
% 42.55/9.20 (~ (exec @ X0 @ body @ X1)
% 42.55/9.20 | ((X0) != (X2))
% 42.55/9.20 | (qa @ X3 @ X1)
% 42.55/9.20 | ~ (pa @ X3 @ X0)
% 42.55/9.20 | ~ (member1389040324_state @ (produc64584659_state @ X2 @ x) @ r))),
% 42.55/9.20 inference('cnf', [status(esa)], [conj_1])).
% 42.55/9.20 thf(zip_derived_cl9, plain,
% 42.55/9.20 (![X0 : a, X1 : state, X2 : state]:
% 42.55/9.20 ( (pa @ X0 @ X1) | ~ (zip_tseitin_0 @ X1 @ X0 @ X2))),
% 42.55/9.20 inference('cnf', [status(esa)], [zf_stmt_12])).
% 42.55/9.20 thf(zip_derived_cl5603, plain, ($false),
% 42.55/9.20 inference('eprover', [status(thm)],
% 42.55/9.20 [zip_derived_cl32, zip_derived_cl38, zip_derived_cl498,
% 42.55/9.20 zip_derived_cl27, zip_derived_cl88, zip_derived_cl29,
% 42.55/9.20 zip_derived_cl30, zip_derived_cl440, zip_derived_cl36,
% 42.55/9.20 zip_derived_cl939, zip_derived_cl34, zip_derived_cl19,
% 42.55/9.20 zip_derived_cl405, zip_derived_cl20, zip_derived_cl18,
% 42.55/9.20 zip_derived_cl11, zip_derived_cl938, zip_derived_cl5581,
% 42.55/9.20 zip_derived_cl12, zip_derived_cl22, zip_derived_cl10,
% 42.55/9.20 zip_derived_cl24, zip_derived_cl23, zip_derived_cl9])).
% 42.55/9.20
% 42.55/9.20 % SZS output end Refutation
% 42.55/9.20
% 42.55/9.20
% 42.55/9.20 % Terminating...
% 43.03/9.38 % Runner terminated.
% 43.03/9.39 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------