%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWW477+7 : TPTP v9.2.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.uA8e8eDjL5 true
% Computer : n014.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:59 PM UTC 2025
% Result : Theorem 13.73s 3.61s
% Output : Refutation 13.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.10 % Problem : SWW477+7 : TPTP v9.2.0. Released v5.3.0.
% 0.02/0.11 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.uA8e8eDjL5 true
% 0.09/0.32 % Computer : n014.cluster.edu
% 0.09/0.32 % Model : x86_64 x86_64
% 0.09/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.32 % Memory : 8042.1875MB
% 0.09/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.32 % CPULimit : 300
% 0.09/0.32 % WCLimit : 300
% 0.09/0.32 % DateTime : Wed Oct 1 12:10:23 EDT 2025
% 0.09/0.32 % CPUTime :
% 0.09/0.32 % Running portfolio for 300 s
% 0.09/0.32 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.32 % Number of cores: 8
% 0.09/0.32 % Python version: Python 3.6.8
% 0.09/0.32 % Running in FO mode
% 0.46/0.61 % Total configuration time : 435
% 0.46/0.61 % Estimated wc time : 1092
% 0.46/0.61 % Estimated cpu time (7 cpus) : 156.0
% 0.47/0.83 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.47/0.84 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.49/0.84 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.49/0.84 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.49/0.85 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.49/0.85 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.49/0.86 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 13.73/3.61 % Solved by fo/fo4.sh.
% 13.73/3.61 % done 63 iterations in 2.627s
% 13.73/3.61 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 13.73/3.61 % SZS output start Refutation
% 13.73/3.61 thf(wTrt_type, type, wTrt: $i).
% 13.73/3.61 thf(h_a_type, type, h_a: $i).
% 13.73/3.61 thf(ha_type, type, ha: $i).
% 13.73/3.61 thf(fun_type, type, fun: $i > $i > $i).
% 13.73/3.61 thf(hAPP_type, type, hAPP: $i > $i > $i > $i > $i).
% 13.73/3.61 thf(hBOOL_type, type, hBOOL: $i > $o).
% 13.73/3.61 thf(product_prod_type, type, product_prod: $i > $i > $i).
% 13.73/3.61 thf(subcls1_type, type, subcls1: $i > $i).
% 13.73/3.61 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $i > $i > $i > $i > $o).
% 13.73/3.61 thf(nat_type, type, nat: $i).
% 13.73/3.61 thf(p_type, type, p: $i).
% 13.73/3.61 thf(class_type, type, class: $i).
% 13.73/3.61 thf(sk__type, type, sk_: $i > $i).
% 13.73/3.61 thf(product_Pair_type, type, product_Pair: $i > $i > $i).
% 13.73/3.61 thf(option_type, type, option: $i > $i).
% 13.73/3.61 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $i > $o).
% 13.73/3.61 thf(ty_type, type, ty: $i).
% 13.73/3.61 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $o).
% 13.73/3.61 thf(ea_type, type, ea: $i).
% 13.73/3.61 thf(e_a_type, type, e_a: $i).
% 13.73/3.61 thf(char_type, type, char: $i).
% 13.73/3.61 thf(transitive_rtrancl_type, type, transitive_rtrancl: $i > $i).
% 13.73/3.61 thf(nt_type, type, nt: $i).
% 13.73/3.61 thf(widen_type, type, widen: $i > $i).
% 13.73/3.61 thf(val_type, type, val: $i).
% 13.73/3.61 thf(bool_type, type, bool: $i).
% 13.73/3.61 thf(sk__5_type, type, sk__5: $i > $i > $i).
% 13.73/3.61 thf(sk__7_type, type, sk__7: $i > $i > $i > $i > $i).
% 13.73/3.61 thf(member_type, type, member: $i > $i).
% 13.73/3.61 thf(sk__8_type, type, sk__8: $i > $i > $i).
% 13.73/3.61 thf(e_type, type, e: $i).
% 13.73/3.61 thf(list_type, type, list: $i > $i).
% 13.73/3.61 thf(sk__6_type, type, sk__6: $i > $i > $i > $i > $i).
% 13.73/3.61 thf(exp_type, type, exp: $i > $i).
% 13.73/3.61 thf(conj_0, conjecture,
% 13.73/3.61 (hBOOL @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ty @ bool @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @
% 13.73/3.61 nat @
% 13.73/3.61 ( option @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( option @ val ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( product_prod @ ( list @ char ) @ ty ) ) @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ty ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ty @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( list @ char ) ) @
% 13.73/3.61 ( exp @ ( list @ char ) ) ) ) ) ) ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @
% 13.73/3.61 nat @
% 13.73/3.61 ( option @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( option @ val ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) ) ) @
% 13.73/3.61 wTrt @ p ) @
% 13.73/3.61 h_a ) @
% 13.73/3.61 e ) @
% 13.73/3.61 e_a ) @
% 13.73/3.61 nt ))).
% 13.73/3.61 thf(zf_stmt_0, negated_conjecture,
% 13.73/3.61 (~( hBOOL @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ty @ bool @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @
% 13.73/3.61 nat @
% 13.73/3.61 ( option @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( option @ val ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( product_prod @ ( list @ char ) @ ty ) ) @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ty ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ty @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( list @ char ) ) @
% 13.73/3.61 ( exp @ ( list @ char ) ) ) ) ) ) ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @
% 13.73/3.61 nat @
% 13.73/3.61 ( option @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( option @ val ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) ) ) @
% 13.73/3.61 wTrt @ p ) @
% 13.73/3.61 h_a ) @
% 13.73/3.61 e ) @
% 13.73/3.61 e_a ) @
% 13.73/3.61 nt ) )),
% 13.73/3.61 inference('cnf.neg', [status(esa)], [conj_0])).
% 13.73/3.61 thf(zip_derived_cl50, plain,
% 13.73/3.61 (~ (hBOOL @
% 13.73/3.61 (hAPP @ ty @ bool @
% 13.73/3.61 (hAPP @ (exp @ (list @ char)) @ (fun @ ty @ bool) @
% 13.73/3.61 (hAPP @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool))) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @
% 13.73/3.61 (list @ (product_prod @ (list @ char) @ ty)) @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ ty) @
% 13.73/3.61 (product_prod @ ty @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @
% 13.73/3.61 (exp @ (list @ char))))))))))) @
% 13.73/3.61 (fun @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)))) @
% 13.73/3.61 wTrt @ p) @
% 13.73/3.61 h_a) @
% 13.73/3.61 e) @
% 13.73/3.61 e_a) @
% 13.73/3.61 nt))),
% 13.73/3.61 inference('cnf', [status(esa)], [zf_stmt_0])).
% 13.73/3.61 thf(fact_1__096_B_BT_O_AP_ME_Mh_A_092_060turnstile_062_Ae_A_058_AT_A_061_061_062_AEX, axiom,
% 13.73/3.61 (![Ta:$i]:
% 13.73/3.61 ( ( hBOOL @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ty @ bool @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @
% 13.73/3.61 nat @
% 13.73/3.61 ( option @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( option @ val ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( product_prod @ ( list @ char ) @ ty ) ) @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ty ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ty @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( list @ char ) ) @
% 13.73/3.61 ( exp @ ( list @ char ) ) ) ) ) ) ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @
% 13.73/3.61 nat @
% 13.73/3.61 ( option @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( option @ val ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) ) ) @
% 13.73/3.61 wTrt @ p ) @
% 13.73/3.61 ha ) @
% 13.73/3.61 e ) @
% 13.73/3.61 ea ) @
% 13.73/3.61 Ta ) ) =>
% 13.73/3.61 ( ?[U_2:$i]:
% 13.73/3.61 ( ( hBOOL @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ty @ bool @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ty @ ( fun @ ty @ bool ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( product_prod @ ( list @ char ) @ ty ) ) @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ty ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ty @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( list @ char ) ) @
% 13.73/3.61 ( exp @ ( list @ char ) ) ) ) ) ) ) ) ) ) ) @
% 13.73/3.61 ( fun @ ty @ ( fun @ ty @ bool ) ) @
% 13.73/3.61 ( widen @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( list @ char ) ) @ ( exp @ ( list @ char ) ) ) ) @
% 13.73/3.61 p ) @
% 13.73/3.61 U_2 ) @
% 13.73/3.61 Ta ) ) &
% 13.73/3.61 ( hBOOL @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ty @ bool @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @
% 13.73/3.61 nat @
% 13.73/3.61 ( option @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( option @ val ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( product_prod @ ( list @ char ) @ ty ) ) @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ty ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ty @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( list @ char ) ) @
% 13.73/3.61 ( exp @ ( list @ char ) ) ) ) ) ) ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @
% 13.73/3.61 nat @
% 13.73/3.61 ( option @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( option @ val ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) ) ) @
% 13.73/3.61 wTrt @ p ) @
% 13.73/3.61 h_a ) @
% 13.73/3.61 e ) @
% 13.73/3.61 e_a ) @
% 13.73/3.61 U_2 ) ) ) ) ))).
% 13.73/3.61 thf(zip_derived_cl7, plain,
% 13.73/3.61 (![X0 : $i]:
% 13.73/3.61 ( (hBOOL @
% 13.73/3.61 (hAPP @ ty @ bool @
% 13.73/3.61 (hAPP @ ty @ (fun @ ty @ bool) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @
% 13.73/3.61 (list @ (product_prod @ (list @ char) @ ty)) @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ ty) @
% 13.73/3.61 (product_prod @ ty @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @
% 13.73/3.61 (exp @ (list @ char))))))))))) @
% 13.73/3.61 (fun @ ty @ (fun @ ty @ bool)) @
% 13.73/3.61 (widen @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @ (exp @ (list @ char)))) @
% 13.73/3.61 p) @
% 13.73/3.61 (sk_ @ X0)) @
% 13.73/3.61 X0))
% 13.73/3.61 | ~ (hBOOL @
% 13.73/3.61 (hAPP @ ty @ bool @
% 13.73/3.61 (hAPP @ (exp @ (list @ char)) @ (fun @ ty @ bool) @
% 13.73/3.61 (hAPP @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool))) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @
% 13.73/3.61 (list @ (product_prod @ (list @ char) @ ty)) @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ ty) @
% 13.73/3.61 (product_prod @ ty @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @
% 13.73/3.61 (exp @ (list @ char))))))))))) @
% 13.73/3.61 (fun @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @
% 13.73/3.61 (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)))) @
% 13.73/3.61 wTrt @ p) @
% 13.73/3.61 ha) @
% 13.73/3.61 e) @
% 13.73/3.61 ea) @
% 13.73/3.61 X0)))),
% 13.73/3.61 inference('cnf', [status(esa)],
% 13.73/3.61 [fact_1__096_B_BT_O_AP_ME_Mh_A_092_060turnstile_062_Ae_A_058_AT_A_061_061_062_AEX])).
% 13.73/3.61 thf(fact_0__096P_ME_Mh_A_092_060turnstile_062_Ae_A_058_ANT_096, axiom,
% 13.73/3.61 (hBOOL @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ty @ bool @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @
% 13.73/3.61 nat @
% 13.73/3.61 ( option @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( option @ val ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( product_prod @ ( list @ char ) @ ty ) ) @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ty ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ty @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( list @ char ) ) @
% 13.73/3.61 ( exp @ ( list @ char ) ) ) ) ) ) ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @
% 13.73/3.61 nat @
% 13.73/3.61 ( option @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( option @ val ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @ ( list @ char ) @ ( option @ ty ) ) @
% 13.73/3.61 ( fun @ ( exp @ ( list @ char ) ) @ ( fun @ ty @ bool ) ) ) ) @
% 13.73/3.61 wTrt @ p ) @
% 13.73/3.61 ha ) @
% 13.73/3.61 e ) @
% 13.73/3.61 ea ) @
% 13.73/3.61 nt ))).
% 13.73/3.61 thf(zip_derived_cl6, plain,
% 13.73/3.61 ( (hBOOL @
% 13.73/3.61 (hAPP @ ty @ bool @
% 13.73/3.61 (hAPP @ (exp @ (list @ char)) @ (fun @ ty @ bool) @
% 13.73/3.61 (hAPP @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool))) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @
% 13.73/3.61 (list @ (product_prod @ (list @ char) @ ty)) @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ ty) @
% 13.73/3.61 (product_prod @ ty @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @
% 13.73/3.61 (exp @ (list @ char))))))))))) @
% 13.73/3.61 (fun @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)))) @
% 13.73/3.61 wTrt @ p) @
% 13.73/3.61 ha) @
% 13.73/3.61 e) @
% 13.73/3.61 ea) @
% 13.73/3.61 nt))),
% 13.73/3.61 inference('cnf', [status(esa)],
% 13.73/3.61 [fact_0__096P_ME_Mh_A_092_060turnstile_062_Ae_A_058_ANT_096])).
% 13.73/3.61 thf(zip_derived_cl87, plain,
% 13.73/3.61 ( (hBOOL @
% 13.73/3.61 (hAPP @ ty @ bool @
% 13.73/3.61 (hAPP @ ty @ (fun @ ty @ bool) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ (product_prod @ (list @ char) @ ty)) @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ ty) @
% 13.73/3.61 (product_prod @ ty @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @
% 13.73/3.61 (exp @ (list @ char))))))))))) @
% 13.73/3.61 (fun @ ty @ (fun @ ty @ bool)) @
% 13.73/3.61 (widen @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @ (exp @ (list @ char)))) @
% 13.73/3.61 p) @
% 13.73/3.61 (sk_ @ nt)) @
% 13.73/3.61 nt))),
% 13.73/3.61 inference('sup+', [status(thm)], [zip_derived_cl7, zip_derived_cl6])).
% 13.73/3.61 thf(fact_606_widen_Osimps, axiom,
% 13.73/3.61 (![X_a:$i,Pa:$i,A1:$i,A2:$i]:
% 13.73/3.61 ( ( hBOOL @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ty @ bool @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ty @ ( fun @ ty @ bool ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( product_prod @ ( list @ char ) @ ty ) ) @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ty ) @ ( product_prod @ ty @ X_a ) ) ) ) ) ) ) ) @
% 13.73/3.61 ( fun @ ty @ ( fun @ ty @ bool ) ) @ ( widen @ X_a ) @ Pa ) @
% 13.73/3.61 A1 ) @
% 13.73/3.61 A2 ) ) <=>
% 13.73/3.61 ( ( ?[C_3:$i]:
% 13.73/3.61 ( ( ( A1 ) = ( nt ) ) &
% 13.73/3.61 ( ( A2 ) = ( hAPP @ ( list @ char ) @ ty @ class @ C_3 ) ) ) ) |
% 13.73/3.61 ( ?[C_3:$i,D_2:$i]:
% 13.73/3.61 ( ( ( A1 ) = ( hAPP @ ( list @ char ) @ ty @ class @ C_3 ) ) &
% 13.73/3.61 ( ( A2 ) = ( hAPP @ ( list @ char ) @ ty @ class @ D_2 ) ) &
% 13.73/3.61 ( hBOOL @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @ bool ) @
% 13.73/3.61 bool @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 bool ) @
% 13.73/3.61 bool ) @
% 13.73/3.61 ( member @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) ) @
% 13.73/3.61 ( product_Pair @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 C_3 ) @
% 13.73/3.61 D_2 ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 bool ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 bool ) @
% 13.73/3.61 ( transitive_rtrancl @ ( list @ char ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( product_prod @ ( list @ char ) @ ty ) ) @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ty ) @ ( product_prod @ ty @ X_a ) ) ) ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 bool ) @
% 13.73/3.61 ( subcls1 @ X_a ) @ Pa ) ) ) ) ) ) |
% 13.73/3.61 ( ?[T_8:$i]: ( ( ( A1 ) = ( T_8 ) ) & ( ( A2 ) = ( T_8 ) ) ) ) ) ))).
% 13.73/3.61 thf(zf_stmt_1, type, zip_tseitin_2 : $i > $i > $i > $o).
% 13.73/3.61 thf(zf_stmt_2, axiom,
% 13.73/3.61 (![T_8:$i,A2:$i,A1:$i]:
% 13.73/3.61 ( ( zip_tseitin_2 @ T_8 @ A2 @ A1 ) <=>
% 13.73/3.61 ( ( ( A2 ) = ( T_8 ) ) & ( ( A1 ) = ( T_8 ) ) ) ))).
% 13.73/3.61 thf(zf_stmt_3, type, zip_tseitin_1 : $i > $i > $i > $i > $i > $i > $o).
% 13.73/3.61 thf(zf_stmt_4, axiom,
% 13.73/3.61 (![D_2:$i,C_3:$i,A2:$i,A1:$i,Pa:$i,X_a:$i]:
% 13.73/3.61 ( ( zip_tseitin_1 @ D_2 @ C_3 @ A2 @ A1 @ Pa @ X_a ) <=>
% 13.73/3.61 ( ( hBOOL @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @ bool ) @
% 13.73/3.61 bool @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @ bool ) @
% 13.73/3.61 bool ) @
% 13.73/3.61 ( member @ ( product_prod @ ( list @ char ) @ ( list @ char ) ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) ) @
% 13.73/3.61 ( product_Pair @ ( list @ char ) @ ( list @ char ) ) @ C_3 ) @
% 13.73/3.61 D_2 ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @ bool ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @ bool ) @
% 13.73/3.61 ( transitive_rtrancl @ ( list @ char ) ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( product_prod @ ( list @ char ) @ ty ) ) @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ty ) @ ( product_prod @ ty @ X_a ) ) ) ) ) ) ) ) @
% 13.73/3.61 ( fun @
% 13.73/3.61 ( product_prod @ ( list @ char ) @ ( list @ char ) ) @ bool ) @
% 13.73/3.61 ( subcls1 @ X_a ) @ Pa ) ) ) ) &
% 13.73/3.61 ( ( A2 ) = ( hAPP @ ( list @ char ) @ ty @ class @ D_2 ) ) &
% 13.73/3.61 ( ( A1 ) = ( hAPP @ ( list @ char ) @ ty @ class @ C_3 ) ) ) ))).
% 13.73/3.61 thf(zf_stmt_5, type, zip_tseitin_0 : $i > $i > $i > $o).
% 13.73/3.61 thf(zf_stmt_6, axiom,
% 13.73/3.61 (![C_3:$i,A2:$i,A1:$i]:
% 13.73/3.61 ( ( zip_tseitin_0 @ C_3 @ A2 @ A1 ) <=>
% 13.73/3.61 ( ( ( A2 ) = ( hAPP @ ( list @ char ) @ ty @ class @ C_3 ) ) &
% 13.73/3.61 ( ( A1 ) = ( nt ) ) ) ))).
% 13.73/3.61 thf(zf_stmt_7, axiom,
% 13.73/3.61 (![X_a:$i,Pa:$i,A1:$i,A2:$i]:
% 13.73/3.61 ( ( hBOOL @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ty @ bool @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ty @ ( fun @ ty @ bool ) @
% 13.73/3.61 ( hAPP @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ( product_prod @ ( list @ char ) @ ty ) ) @
% 13.73/3.61 ( list @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ char ) @
% 13.73/3.61 ( product_prod @
% 13.73/3.61 ( list @ ty ) @ ( product_prod @ ty @ X_a ) ) ) ) ) ) ) ) @
% 13.73/3.61 ( fun @ ty @ ( fun @ ty @ bool ) ) @ ( widen @ X_a ) @ Pa ) @
% 13.73/3.61 A1 ) @
% 13.73/3.61 A2 ) ) <=>
% 13.73/3.61 ( ( ?[T_8:$i]: ( zip_tseitin_2 @ T_8 @ A2 @ A1 ) ) |
% 13.73/3.61 ( ?[C_3:$i,D_2:$i]: ( zip_tseitin_1 @ D_2 @ C_3 @ A2 @ A1 @ Pa @ X_a ) ) |
% 13.73/3.61 ( ?[C_3:$i]: ( zip_tseitin_0 @ C_3 @ A2 @ A1 ) ) ) ))).
% 13.73/3.61 thf(zip_derived_cl44, plain,
% 13.73/3.61 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 13.73/3.61 ( (zip_tseitin_0 @ (sk__5 @ X0 @ X1) @ X0 @ X1)
% 13.73/3.61 | (zip_tseitin_1 @ (sk__7 @ X0 @ X1 @ X2 @ X3) @
% 13.73/3.61 (sk__6 @ X0 @ X1 @ X2 @ X3) @ X0 @ X1 @ X2 @ X3)
% 13.73/3.61 | (zip_tseitin_2 @ (sk__8 @ X0 @ X1) @ X0 @ X1)
% 13.73/3.61 | ~ (hBOOL @
% 13.73/3.61 (hAPP @ ty @ bool @
% 13.73/3.61 (hAPP @ ty @ (fun @ ty @ bool) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @
% 13.73/3.61 (list @ (product_prod @ (list @ char) @ ty)) @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ ty) @ (product_prod @ ty @ X3)))))))) @
% 13.73/3.61 (fun @ ty @ (fun @ ty @ bool)) @ (widen @ X3) @ X2) @
% 13.73/3.61 X1) @
% 13.73/3.61 X0)))),
% 13.73/3.61 inference('cnf', [status(esa)], [zf_stmt_7])).
% 13.73/3.61 thf(zip_derived_cl89, plain,
% 13.73/3.61 (( (zip_tseitin_2 @ (sk__8 @ nt @ (sk_ @ nt)) @ nt @ (sk_ @ nt))
% 13.73/3.61 | (zip_tseitin_1 @
% 13.73/3.61 (sk__7 @ nt @ (sk_ @ nt) @ p @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @ (exp @ (list @ char)))) @
% 13.73/3.61 (sk__6 @ nt @ (sk_ @ nt) @ p @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @ (exp @ (list @ char)))) @
% 13.73/3.61 nt @ (sk_ @ nt) @ p @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @ (exp @ (list @ char))))
% 13.73/3.61 | (zip_tseitin_0 @ (sk__5 @ nt @ (sk_ @ nt)) @ nt @ (sk_ @ nt)))),
% 13.73/3.61 inference('sup-', [status(thm)], [zip_derived_cl87, zip_derived_cl44])).
% 13.73/3.61 thf(zip_derived_cl38, plain,
% 13.73/3.61 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 13.73/3.61 (((X1) = (hAPP @ (list @ char) @ ty @ class @ X0))
% 13.73/3.61 | ~ (zip_tseitin_1 @ X0 @ X2 @ X1 @ X3 @ X4 @ X5))),
% 13.73/3.61 inference('cnf', [status(esa)], [zf_stmt_4])).
% 13.73/3.61 thf(zip_derived_cl90, plain,
% 13.73/3.61 (( (zip_tseitin_0 @ (sk__5 @ nt @ (sk_ @ nt)) @ nt @ (sk_ @ nt))
% 13.73/3.61 | (zip_tseitin_2 @ (sk__8 @ nt @ (sk_ @ nt)) @ nt @ (sk_ @ nt))
% 13.73/3.61 | ((nt)
% 13.73/3.61 = (hAPP @ (list @ char) @ ty @ class @
% 13.73/3.61 (sk__7 @ nt @ (sk_ @ nt) @ p @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @ (exp @ (list @ char)))))))),
% 13.73/3.61 inference('sup-', [status(thm)], [zip_derived_cl89, zip_derived_cl38])).
% 13.73/3.61 thf(fact_579_ty_Osimps_I20_J, axiom,
% 13.73/3.61 (![List_2:$i]:
% 13.73/3.61 ( ( nt ) != ( hAPP @ ( list @ char ) @ ty @ class @ List_2 ) ))).
% 13.73/3.61 thf(zip_derived_cl25, plain,
% 13.73/3.61 (![X0 : $i]: ((nt) != (hAPP @ (list @ char) @ ty @ class @ X0))),
% 13.73/3.61 inference('cnf', [status(esa)], [fact_579_ty_Osimps_I20_J])).
% 13.73/3.61 thf(zip_derived_cl93, plain,
% 13.73/3.61 (( (zip_tseitin_0 @ (sk__5 @ nt @ (sk_ @ nt)) @ nt @ (sk_ @ nt))
% 13.73/3.61 | (zip_tseitin_2 @ (sk__8 @ nt @ (sk_ @ nt)) @ nt @ (sk_ @ nt)))),
% 13.73/3.61 inference('simplify_reflect-', [status(thm)],
% 13.73/3.61 [zip_derived_cl90, zip_derived_cl25])).
% 13.73/3.61 thf(zip_derived_cl34, plain,
% 13.73/3.61 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.73/3.61 (((X1) = (hAPP @ (list @ char) @ ty @ class @ X0))
% 13.73/3.61 | ~ (zip_tseitin_0 @ X0 @ X1 @ X2))),
% 13.73/3.61 inference('cnf', [status(esa)], [zf_stmt_6])).
% 13.73/3.61 thf(zip_derived_cl94, plain,
% 13.73/3.61 (( (zip_tseitin_2 @ (sk__8 @ nt @ (sk_ @ nt)) @ nt @ (sk_ @ nt))
% 13.73/3.61 | ((nt)
% 13.73/3.61 = (hAPP @ (list @ char) @ ty @ class @ (sk__5 @ nt @ (sk_ @ nt)))))),
% 13.73/3.61 inference('sup-', [status(thm)], [zip_derived_cl93, zip_derived_cl34])).
% 13.73/3.61 thf(zip_derived_cl25, plain,
% 13.73/3.61 (![X0 : $i]: ((nt) != (hAPP @ (list @ char) @ ty @ class @ X0))),
% 13.73/3.61 inference('cnf', [status(esa)], [fact_579_ty_Osimps_I20_J])).
% 13.73/3.61 thf(zip_derived_cl97, plain,
% 13.73/3.61 ( (zip_tseitin_2 @ (sk__8 @ nt @ (sk_ @ nt)) @ nt @ (sk_ @ nt))),
% 13.73/3.61 inference('simplify_reflect-', [status(thm)],
% 13.73/3.61 [zip_derived_cl94, zip_derived_cl25])).
% 13.73/3.61 thf(zip_derived_cl97, plain,
% 13.73/3.61 ( (zip_tseitin_2 @ (sk__8 @ nt @ (sk_ @ nt)) @ nt @ (sk_ @ nt))),
% 13.73/3.61 inference('simplify_reflect-', [status(thm)],
% 13.73/3.61 [zip_derived_cl94, zip_derived_cl25])).
% 13.73/3.61 thf(zip_derived_cl41, plain,
% 13.73/3.61 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.73/3.61 (((X1) = (X0)) | ~ (zip_tseitin_2 @ X0 @ X1 @ X2))),
% 13.73/3.61 inference('cnf', [status(esa)], [zf_stmt_2])).
% 13.73/3.61 thf(zip_derived_cl98, plain, (((nt) = (sk__8 @ nt @ (sk_ @ nt)))),
% 13.73/3.61 inference('sup-', [status(thm)], [zip_derived_cl97, zip_derived_cl41])).
% 13.73/3.61 thf(zip_derived_cl101, plain, ( (zip_tseitin_2 @ nt @ nt @ (sk_ @ nt))),
% 13.73/3.61 inference('demod', [status(thm)], [zip_derived_cl97, zip_derived_cl98])).
% 13.73/3.61 thf(zip_derived_cl42, plain,
% 13.73/3.61 (![X0 : $i, X1 : $i, X2 : $i]:
% 13.73/3.61 (((X1) = (X0)) | ~ (zip_tseitin_2 @ X0 @ X2 @ X1))),
% 13.73/3.61 inference('cnf', [status(esa)], [zf_stmt_2])).
% 13.73/3.61 thf(zip_derived_cl103, plain, (((sk_ @ nt) = (nt))),
% 13.73/3.61 inference('sup-', [status(thm)], [zip_derived_cl101, zip_derived_cl42])).
% 13.73/3.61 thf(zip_derived_cl8, plain,
% 13.73/3.61 (![X0 : $i]:
% 13.73/3.61 ( (hBOOL @
% 13.73/3.61 (hAPP @ ty @ bool @
% 13.73/3.61 (hAPP @ (exp @ (list @ char)) @ (fun @ ty @ bool) @
% 13.73/3.61 (hAPP @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool))) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @
% 13.73/3.61 (list @ (product_prod @ (list @ char) @ ty)) @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ ty) @
% 13.73/3.61 (product_prod @ ty @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @
% 13.73/3.61 (exp @ (list @ char))))))))))) @
% 13.73/3.61 (fun @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)))) @
% 13.73/3.61 wTrt @ p) @
% 13.73/3.61 h_a) @
% 13.73/3.61 e) @
% 13.73/3.61 e_a) @
% 13.73/3.61 (sk_ @ X0)))
% 13.73/3.61 | ~ (hBOOL @
% 13.73/3.61 (hAPP @ ty @ bool @
% 13.73/3.61 (hAPP @ (exp @ (list @ char)) @ (fun @ ty @ bool) @
% 13.73/3.61 (hAPP @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool))) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @
% 13.73/3.61 (list @ (product_prod @ (list @ char) @ ty)) @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ ty) @
% 13.73/3.61 (product_prod @ ty @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @
% 13.73/3.61 (exp @ (list @ char))))))))))) @
% 13.73/3.61 (fun @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @
% 13.73/3.61 (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)))) @
% 13.73/3.61 wTrt @ p) @
% 13.73/3.61 ha) @
% 13.73/3.61 e) @
% 13.73/3.61 ea) @
% 13.73/3.61 X0)))),
% 13.73/3.61 inference('cnf', [status(esa)],
% 13.73/3.61 [fact_1__096_B_BT_O_AP_ME_Mh_A_092_060turnstile_062_Ae_A_058_AT_A_061_061_062_AEX])).
% 13.73/3.61 thf(zip_derived_cl170, plain,
% 13.73/3.61 (( (hBOOL @
% 13.73/3.61 (hAPP @ ty @ bool @
% 13.73/3.61 (hAPP @ (exp @ (list @ char)) @ (fun @ ty @ bool) @
% 13.73/3.61 (hAPP @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool))) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @
% 13.73/3.61 (list @ (product_prod @ (list @ char) @ ty)) @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ ty) @
% 13.73/3.61 (product_prod @ ty @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @
% 13.73/3.61 (exp @ (list @ char))))))))))) @
% 13.73/3.61 (fun @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)))) @
% 13.73/3.61 wTrt @ p) @
% 13.73/3.61 h_a) @
% 13.73/3.61 e) @
% 13.73/3.61 e_a) @
% 13.73/3.61 nt))
% 13.73/3.61 | ~ (hBOOL @
% 13.73/3.61 (hAPP @ ty @ bool @
% 13.73/3.61 (hAPP @ (exp @ (list @ char)) @ (fun @ ty @ bool) @
% 13.73/3.61 (hAPP @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool))) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @
% 13.73/3.61 (list @ (product_prod @ (list @ char) @ ty)) @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ ty) @
% 13.73/3.61 (product_prod @ ty @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @
% 13.73/3.61 (exp @ (list @ char))))))))))) @
% 13.73/3.61 (fun @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)))) @
% 13.73/3.61 wTrt @ p) @
% 13.73/3.61 ha) @
% 13.73/3.61 e) @
% 13.73/3.61 ea) @
% 13.73/3.61 nt)))),
% 13.73/3.61 inference('sup+', [status(thm)], [zip_derived_cl103, zip_derived_cl8])).
% 13.73/3.61 thf(zip_derived_cl6, plain,
% 13.73/3.61 ( (hBOOL @
% 13.73/3.61 (hAPP @ ty @ bool @
% 13.73/3.61 (hAPP @ (exp @ (list @ char)) @ (fun @ ty @ bool) @
% 13.73/3.61 (hAPP @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool))) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @
% 13.73/3.61 (list @ (product_prod @ (list @ char) @ ty)) @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ ty) @
% 13.73/3.61 (product_prod @ ty @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @
% 13.73/3.61 (exp @ (list @ char))))))))))) @
% 13.73/3.61 (fun @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)))) @
% 13.73/3.61 wTrt @ p) @
% 13.73/3.61 ha) @
% 13.73/3.61 e) @
% 13.73/3.61 ea) @
% 13.73/3.61 nt))),
% 13.73/3.61 inference('cnf', [status(esa)],
% 13.73/3.61 [fact_0__096P_ME_Mh_A_092_060turnstile_062_Ae_A_058_ANT_096])).
% 13.73/3.61 thf(zip_derived_cl171, plain,
% 13.73/3.61 ( (hBOOL @
% 13.73/3.61 (hAPP @ ty @ bool @
% 13.73/3.61 (hAPP @ (exp @ (list @ char)) @ (fun @ ty @ bool) @
% 13.73/3.61 (hAPP @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool))) @
% 13.73/3.61 (hAPP @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @
% 13.73/3.61 (list @ (product_prod @ (list @ char) @ ty)) @
% 13.73/3.61 (list @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (product_prod @ (list @ ty) @
% 13.73/3.61 (product_prod @ ty @
% 13.73/3.61 (product_prod @ (list @ (list @ char)) @
% 13.73/3.61 (exp @ (list @ char))))))))))) @
% 13.73/3.61 (fun @
% 13.73/3.61 (fun @ nat @
% 13.73/3.61 (option @
% 13.73/3.61 (product_prod @ (list @ char) @
% 13.73/3.61 (fun @ (product_prod @ (list @ char) @ (list @ char)) @
% 13.73/3.61 (option @ val))))) @
% 13.73/3.61 (fun @ (fun @ (list @ char) @ (option @ ty)) @
% 13.73/3.61 (fun @ (exp @ (list @ char)) @ (fun @ ty @ bool)))) @
% 13.73/3.61 wTrt @ p) @
% 13.73/3.61 h_a) @
% 13.73/3.61 e) @
% 13.73/3.61 e_a) @
% 13.73/3.61 nt))),
% 13.73/3.61 inference('demod', [status(thm)], [zip_derived_cl170, zip_derived_cl6])).
% 13.73/3.61 thf(zip_derived_cl174, plain, ($false),
% 13.73/3.61 inference('demod', [status(thm)], [zip_derived_cl50, zip_derived_cl171])).
% 13.73/3.61
% 13.73/3.61 % SZS output end Refutation
% 13.73/3.61
% 13.73/3.61
% 13.73/3.61 % Terminating...
% 14.52/3.84 % Runner terminated.
% 14.58/3.87 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------