%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWX153_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.xMcZSD3m3f true
% Computer : n008.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 : Tue May 5 07:08:45 PM UTC 2026
% Result : Theorem 63.41s 9.70s
% Output : Refutation 63.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX153_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.xMcZSD3m3f true
% 0.15/0.34 % Computer : n008.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue May 5 09:29:58 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 % Running portfolio for 300 s
% 0.15/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Number of cores: 8
% 0.15/0.34 % Python version: Python 3.6.8
% 0.15/0.35 % Running in HO mode
% 0.54/0.66 % Total configuration time : 828
% 0.54/0.66 % Estimated wc time : 1656
% 0.54/0.66 % Estimated cpu time (8 cpus) : 207.0
% 0.54/0.71 % /export/starexec/sandbox2/solver/bin/lams/40_c.s.sh running for 80s
% 0.54/0.71 % /export/starexec/sandbox2/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.54/0.74 % /export/starexec/sandbox2/solver/bin/lams/40_c_ic.sh running for 80s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/lams/15_e_short1.sh running for 30s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/lams/40_noforms.sh running for 90s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/lams/40_b.comb.sh running for 70s
% 0.54/0.77 % /export/starexec/sandbox2/solver/bin/lams/30_sp5.sh running for 60s
% 63.41/9.70 % Solved by lams/40_c_ic.sh.
% 63.41/9.70 % done 193 iterations in 8.926s
% 63.41/9.70 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 63.41/9.70 % SZS output start Refutation
% 63.41/9.70 thf(d_unsorted_type, type, d_unsorted: $tType).
% 63.41/9.70 thf(trans_type, type, trans: ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_25_type, type, zip_tseitin_25: $i > $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(nfof_type, type, nfof: ($i > $i > $o) > $i > $i > $o).
% 63.41/9.70 thf(cr_type, type, cr: ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_30_type, type, zip_tseitin_30: ($i > $i > $o) >
% 63.41/9.70 ($i > $i > $o) > $i > $i >
% 63.41/9.70 $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(infl_type, type, infl: (($i > $i > $o) > $i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_9_type, type, zip_tseitin_9: ($i > $i > $o) > $i > $i >
% 63.41/9.70 ($i > $i > $o) > $o).
% 63.41/9.70 thf(d_unsorted_0_type, type, d_unsorted_0: d_unsorted).
% 63.41/9.70 thf(zip_tseitin_11_type, type, zip_tseitin_11: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_12_type, type, zip_tseitin_12: ($i > $i > $o) > $o).
% 63.41/9.70 thf(asymm_type, type, asymm: ($i > $i > $o) > $o).
% 63.41/9.70 thf(rc_type, type, rc: ($i > $i > $o) > $i > $i > $o).
% 63.41/9.70 thf(zip_tseitin_22_type, type, zip_tseitin_22: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_6_type, type, zip_tseitin_6: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(trsc_type, type, trsc: ($i > $i > $o) > $i > $i > $o).
% 63.41/9.70 thf(norm_type, type, norm: ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > ($i > $i > $o) >
% 63.41/9.70 ($i > $i > $o) >
% 63.41/9.70 (($i > $i > $o) > $i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_18_type, type, zip_tseitin_18: $i > $i > ($i > $o) >
% 63.41/9.70 ($i > $i > $o) > $o).
% 63.41/9.70 thf(trc_type, type, trc: ($i > $i > $o) > $i > $i > $o).
% 63.41/9.70 thf(zip_tseitin_23_type, type, zip_tseitin_23: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_19_type, type, zip_tseitin_19: $i > ($i > $o) >
% 63.41/9.70 ($i > $i > $o) > $o).
% 63.41/9.70 thf(so_type, type, so: ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_32_type, type, zip_tseitin_32: ($i > $i > $o) >
% 63.41/9.70 ($i > $i > $o) > $i > $i >
% 63.41/9.70 ($i > $i > $o) > $o).
% 63.41/9.70 thf(inv_type, type, inv: ($i > $i > $o) > $i > $i > $o).
% 63.41/9.70 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > ($i > $i > $o) >
% 63.41/9.70 (($i > $i > $o) > $i > $i > $o) > $o).
% 63.41/9.70 thf(refl_type, type, refl: ($i > $i > $o) > $o).
% 63.41/9.70 thf(symm_type, type, symm: ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_8_type, type, zip_tseitin_8: $i > $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(ind_type, type, ind: ($i > $i > $o) > $o).
% 63.41/9.70 thf(total_type, type, total: ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_16_type, type, zip_tseitin_16: $i > ($i > $o) >
% 63.41/9.70 ($i > $i > $o) > $o).
% 63.41/9.70 thf(irrefl_type, type, irrefl: ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_20_type, type, zip_tseitin_20: $i > ($i > $o) >
% 63.41/9.70 ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_29_type, type, zip_tseitin_29: ($i > $i > $o) >
% 63.41/9.70 ($i > $i > $o) > $i > $i >
% 63.41/9.70 $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(sk__135_type, type, sk__135: $i).
% 63.41/9.70 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_24_type, type, zip_tseitin_24: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_26_type, type, zip_tseitin_26: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(sk__122_type, type, sk__122: ($i > $i > $o) > $i).
% 63.41/9.70 thf(confl_type, type, confl: ($i > $i > $o) > $o).
% 63.41/9.70 thf(sk__134_type, type, sk__134: $i > $i > $o).
% 63.41/9.70 thf(mono_type, type, mono: (($i > $i > $o) > $i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > ($i > $i > $o) >
% 63.41/9.70 ($i > $i > $o) > $o).
% 63.41/9.70 thf(idem_type, type, idem: (($i > $i > $o) > $i > $i > $o) > $o).
% 63.41/9.70 thf(innf_type, type, innf: ($i > $i > $o) > $i > $o).
% 63.41/9.70 thf(antisymm_type, type, antisymm: ($i > $i > $o) > $o).
% 63.41/9.70 thf(lconfl_type, type, lconfl: ($i > $i > $o) > $o).
% 63.41/9.70 thf(subrel_type, type, subrel: ($i > $i > $o) > ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_15_type, type, zip_tseitin_15: $i > $i > ($i > $o) >
% 63.41/9.70 ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_28_type, type, zip_tseitin_28: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(term_type, type, term: ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_17_type, type, zip_tseitin_17: $i > ($i > $o) >
% 63.41/9.70 ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_31_type, type, zip_tseitin_31: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(sk__136_type, type, sk__136: $i).
% 63.41/9.70 thf(sk__133_type, type, sk__133: $i > d_unsorted).
% 63.41/9.70 thf(sconfl_type, type, sconfl: ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_21_type, type, zip_tseitin_21: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(join_type, type, join: ($i > $i > $o) > $i > $i > $o).
% 63.41/9.70 thf(po_type, type, po: ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_13_type, type, zip_tseitin_13: ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_14_type, type, zip_tseitin_14: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(sc_type, type, sc: ($i > $i > $o) > $i > $i > $o).
% 63.41/9.70 thf(tc_type, type, tc: ($i > $i > $o) > $i > $i > $o).
% 63.41/9.70 thf(d2unsorted_type, type, d2unsorted: d_unsorted > $i).
% 63.41/9.70 thf(zip_tseitin_27_type, type, zip_tseitin_27: ($i > $i > $o) >
% 63.41/9.70 ($i > $i > $o) > $i > $i >
% 63.41/9.70 $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(zip_tseitin_10_type, type, zip_tseitin_10: $i > $i > ($i > $i > $o) > $o).
% 63.41/9.70 thf(sev441_1, axiom,
% 63.41/9.70 (( ![U:$i]: ( ?[DU:d_unsorted]: ( ( U ) = ( d2unsorted @ DU ) ) ) ) &
% 63.41/9.70 ( ![DU:d_unsorted]: ( ( DU ) = ( d_unsorted_0 ) ) ) &
% 63.41/9.70 ( ![DU1:d_unsorted,DU2:d_unsorted]:
% 63.41/9.70 ( ( ( d2unsorted @ DU1 ) = ( d2unsorted @ DU2 ) ) =>
% 63.41/9.70 ( ( DU1 ) = ( DU2 ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),S:( $i > $i > $o )]:
% 63.41/9.70 ( ( subrel @ R @ S ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i]: ( ( ~( R @ X @ Y ) ) | ( S @ X @ Y ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( inv @ R @ X @ Y ) <=> ( R @ Y @ X ) ) ) &
% 63.41/9.70 ( ![F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 63.41/9.70 ( ( idem @ F ) <=>
% 63.41/9.70 ( ![R:( $i > $i > $o )]: ( ( F @ R ) = ( F @ ( F @ R ) ) ) ) ) ) &
% 63.41/9.70 ( ![F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 63.41/9.70 ( ( infl @ F ) <=>
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( ~( R @ X @ Y ) ) | ( F @ R @ X @ Y ) ) ) ) ) &
% 63.41/9.70 ( ![F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 63.41/9.70 ( ( mono @ F ) <=>
% 63.41/9.70 ( ![R:( $i > $i > $o ),S:( $i > $i > $o ),Bound_variable_510:$i,
% 63.41/9.70 Bound_variable_512:$i]:
% 63.41/9.70 ( ( ~( ![X:$i,Y:$i]: ( ( ~( R @ X @ Y ) ) | ( S @ X @ Y ) ) ) ) |
% 63.41/9.70 ( ~( F @ R @ Bound_variable_510 @ Bound_variable_512 ) ) |
% 63.41/9.70 ( F @ S @ Bound_variable_510 @ Bound_variable_512 ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]: ( ( refl @ R ) <=> ( ![X:$i]: ( R @ X @ X ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( irrefl @ R ) <=> ( ![X:$i]: ( ~( R @ X @ X ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( rc @ R @ X @ Y ) <=> ( ( R @ X @ Y ) | ( ( X ) = ( Y ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( symm @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i]: ( ( ~( R @ X @ Y ) ) | ( R @ Y @ X ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( antisymm @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i]:
% 63.41/9.70 ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ X ) ) | ( ( X ) = ( Y ) ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( asymm @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i]: ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ X ) ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( sc @ R @ X @ Y ) <=> ( ( R @ X @ Y ) | ( R @ Y @ X ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( trans @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i,Z:$i]:
% 63.41/9.70 ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ Z ) ) | ( R @ X @ Z ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( tc @ R @ X @ Y ) <=>
% 63.41/9.70 ( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 63.41/9.70 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ X @ Y ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),Flatten_var_0:$i,Flatten_var_1:$i]:
% 63.41/9.70 ( ( trc @ R @ Flatten_var_0 @ Flatten_var_1 ) <=>
% 63.41/9.70 ( ( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 63.41/9.70 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Flatten_var_0 @ Flatten_var_1 ) ) ) |
% 63.41/9.70 ( ( Flatten_var_0 ) = ( Flatten_var_1 ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),Flatten_var_0:$i,Flatten_var_1:$i]:
% 63.41/9.70 ( ( trsc @ R @ Flatten_var_0 @ Flatten_var_1 ) <=>
% 63.41/9.70 ( ( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 63.41/9.70 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Flatten_var_0 @ Flatten_var_1 ) ) ) |
% 63.41/9.70 ( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 63.41/9.70 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Flatten_var_1 @ Flatten_var_0 ) ) ) |
% 63.41/9.70 ( ( Flatten_var_0 ) = ( Flatten_var_1 ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( po @ R ) <=>
% 63.41/9.70 ( ( ![X:$i,Y:$i,Z:$i]:
% 63.41/9.70 ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ Z ) ) | ( R @ X @ Z ) ) ) &
% 63.41/9.70 ( ![X:$i,Y:$i]:
% 63.41/9.70 ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ X ) ) | ( ( X ) = ( Y ) ) ) ) &
% 63.41/9.70 ( ![X:$i]: ( R @ X @ X ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( so @ R ) <=>
% 63.41/9.70 ( ( ![X:$i,Y:$i,Z:$i]:
% 63.41/9.70 ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ Z ) ) | ( R @ X @ Z ) ) ) &
% 63.41/9.70 ( ![X:$i,Y:$i]: ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ X ) ) ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( total @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i]: ( ( ( X ) = ( Y ) ) | ( R @ X @ Y ) | ( R @ Y @ X ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( term @ R ) <=>
% 63.41/9.70 ( ![A:( $i > $o ),Bound_variable_862:$i]:
% 63.41/9.70 ( ( ~( A @ Bound_variable_862 ) ) |
% 63.41/9.70 ( ~( ![X:$i]:
% 63.41/9.70 ( ( ~( A @ X ) ) |
% 63.41/9.70 ( ~( ![Y:$i]: ( ( ~( A @ Y ) ) | ( ~( R @ X @ Y ) ) ) ) ) ) ) ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( ind @ R ) <=>
% 63.41/9.70 ( ![P:( $i > $o ),Bound_variable_917:$i]:
% 63.41/9.70 ( ( ~( ![X:$i]:
% 63.41/9.70 ( ( ~( ![Y:$i]:
% 63.41/9.70 ( ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,
% 63.41/9.70 Bound_variable_674:$i,Z:$i]:
% 63.41/9.70 ( ( ~( S @
% 63.41/9.70 Bound_variable_672 @
% 63.41/9.70 Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,
% 63.41/9.70 Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @
% 63.41/9.70 Bound_variable_661 @
% 63.41/9.70 Bound_variable_663 ) ) |
% 63.41/9.70 ( S @
% 63.41/9.70 Bound_variable_661 @
% 63.41/9.70 Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ X @ Y ) ) ) ) |
% 63.41/9.70 ( P @ Y ) ) ) ) |
% 63.41/9.70 ( P @ X ) ) ) ) |
% 63.41/9.70 ( P @ Bound_variable_917 ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i]:
% 63.41/9.70 ( ( innf @ R @ X ) <=> ( ![Y:$i]: ( ~( R @ X @ Y ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( nfof @ R @ X @ Y ) <=>
% 63.41/9.70 ( ( ![Bound_variable_985:$i]: ( ~( R @ X @ Bound_variable_985 ) ) ) &
% 63.41/9.70 ( ( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 63.41/9.70 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Y @ X ) ) ) |
% 63.41/9.70 ( ( X ) = ( Y ) ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( norm @ R ) <=>
% 63.41/9.70 ( ![X:$i,Bound_variable_1075:$i]:
% 63.41/9.70 ( ( ~( R @ X @ Bound_variable_1075 ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_1049:$i]:
% 63.41/9.70 ( ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Z:$i]:
% 63.41/9.70 ( ( ~( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ X @ Bound_variable_1049 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_985:$i]:
% 63.41/9.70 ( ~( R @ Bound_variable_1049 @ Bound_variable_985 ) ) ) ) ) ) ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( join @ R @ X @ Y ) <=>
% 63.41/9.70 ( ~( ( ![Bound_variable_1218:$i]:
% 63.41/9.70 ( ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( ( ~( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Y @ Bound_variable_1218 ) ) ) ) |
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( ( ~( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ X @ Bound_variable_1218 ) ) ) ) ) ) &
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Bound_variable_1106 ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ X @ Y ) ) ) ) &
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Bound_variable_1125 ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Y @ X ) ) ) ) &
% 63.41/9.70 ( ( X ) != ( Y ) ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( lconfl @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i,Z:$i,Bound_variable_1293:( $i > $i > $o ),
% 63.41/9.70 Bound_variable_1309:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( R @ X @ Z ) ) | ( ~( R @ X @ Y ) ) | ( ( Y ) = ( Z ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_1218:$i]:
% 63.41/9.70 ( ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( ( ~( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 63.41/9.70 ( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Y @ Bound_variable_1218 ) ) ) ) |
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( ( ~( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 63.41/9.70 ( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Z @ Bound_variable_1218 ) ) ) ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( ( ~( Bound_variable_1293 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( Bound_variable_1293 @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 63.41/9.70 ( Bound_variable_1293 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( Bound_variable_1293 @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( Bound_variable_1293 @ Y @ Z ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( ( ~( Bound_variable_1309 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( Bound_variable_1309 @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 63.41/9.70 ( Bound_variable_1309 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( Bound_variable_1309 @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( Bound_variable_1309 @ Z @ Y ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( sconfl @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i,Z:$i,Bound_variable_1371:( $i > $i > $o ),
% 63.41/9.70 Bound_variable_1387:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( R @ X @ Z ) ) |
% 63.41/9.70 ( ( ( X ) != ( Y ) ) &
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1347:$i]:
% 63.41/9.70 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Bound_variable_1347 ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Bound_variable_1347 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ X @ Y ) ) ) ) ) |
% 63.41/9.70 ( ( Y ) = ( Z ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_1218:$i]:
% 63.41/9.70 ( ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( ( ~( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 63.41/9.70 ( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Y @ Bound_variable_1218 ) ) ) ) |
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( ( ~( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 63.41/9.70 ( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Z @ Bound_variable_1218 ) ) ) ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( ( ~( Bound_variable_1371 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( Bound_variable_1371 @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 63.41/9.70 ( Bound_variable_1371 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( Bound_variable_1371 @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( Bound_variable_1371 @ Y @ Z ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( ( ~( Bound_variable_1387 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( Bound_variable_1387 @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 63.41/9.70 ( Bound_variable_1387 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( Bound_variable_1387 @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( Bound_variable_1387 @ Z @ Y ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( confl @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i,Z:$i,Bound_variable_1444:( $i > $i > $o ),
% 63.41/9.70 Bound_variable_1460:( $i > $i > $o )]:
% 63.41/9.70 ( ( ( ( X ) != ( Z ) ) &
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Bound_variable_1106 ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ X @ Z ) ) ) ) ) |
% 63.41/9.70 ( ( ( X ) != ( Y ) ) &
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1422:$i]:
% 63.41/9.70 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Bound_variable_1422 ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Bound_variable_1422 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ X @ Y ) ) ) ) ) |
% 63.41/9.70 ( ( Y ) = ( Z ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_1218:$i]:
% 63.41/9.70 ( ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( ( ~( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 63.41/9.70 ( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Y @ Bound_variable_1218 ) ) ) ) |
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( ( ~( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 63.41/9.70 ( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Z @ Bound_variable_1218 ) ) ) ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( ( ~( Bound_variable_1444 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( Bound_variable_1444 @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 63.41/9.70 ( Bound_variable_1444 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( Bound_variable_1444 @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( Bound_variable_1444 @ Y @ Z ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( ( ~( Bound_variable_1460 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( Bound_variable_1460 @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 63.41/9.70 ( Bound_variable_1460 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( Bound_variable_1460 @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( Bound_variable_1460 @ Z @ Y ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( cr @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i,Bound_variable_1522:( $i > $i > $o ),
% 63.41/9.70 Bound_variable_1538:( $i > $i > $o )]:
% 63.41/9.70 ( ( ( ( X ) != ( Y ) ) &
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 63.41/9.70 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Y @ X ) ) ) ) &
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 63.41/9.70 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 63.41/9.70 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ X @ Y ) ) ) ) ) |
% 63.41/9.70 ( ( X ) = ( Y ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_1218:$i]:
% 63.41/9.70 ( ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( ( ~( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 63.41/9.70 ( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ Y @ Bound_variable_1218 ) ) ) ) |
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( ( ~( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( S @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 63.41/9.70 ( S @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( S @ X @ Bound_variable_1218 ) ) ) ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( ( ~( Bound_variable_1522 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( Bound_variable_1522 @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 63.41/9.70 ( Bound_variable_1522 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( Bound_variable_1522 @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( Bound_variable_1522 @ Y @ X ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( ( ~( Bound_variable_1538 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_674 ) ) |
% 63.41/9.70 ( ~( Bound_variable_1538 @
% 63.41/9.70 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 63.41/9.70 ( Bound_variable_1538 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 63.41/9.70 ( Bound_variable_1538 @
% 63.41/9.70 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 63.41/9.70 ( Bound_variable_1538 @ X @ Y ) ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_0, axiom,
% 63.41/9.70 (![Flatten_var_1:$i,Flatten_var_0:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_11 @ Flatten_var_1 @ Flatten_var_0 @ R ) <=>
% 63.41/9.70 ( ( ( Flatten_var_0 ) = ( Flatten_var_1 ) ) |
% 63.41/9.70 ( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( zip_tseitin_9 @ S @ Flatten_var_0 @ Flatten_var_1 @ R ) ) |
% 63.41/9.70 ( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( zip_tseitin_9 @ S @ Flatten_var_1 @ Flatten_var_0 @ R ) ) ) ))).
% 63.41/9.70 thf(zip_derived_cl38, plain,
% 63.41/9.70 (![X0 : $i, X1 : $i, X2 : $i > $i > $o]:
% 63.41/9.70 ( (zip_tseitin_11 @ X0 @ X1 @ X2) | ((X1) != (X0)))),
% 63.41/9.70 inference('cnf', [status(esa)], [zf_stmt_0])).
% 63.41/9.70 thf(zf_stmt_1, type, zip_tseitin_32 :
% 63.41/9.70 ( $i > $i > $o ) > ( $i > $i > $o ) > $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_2, axiom,
% 63.41/9.70 (![Bound_variable_1538:( $i > $i > $o ),
% 63.41/9.70 Bound_variable_1522:( $i > $i > $o ),Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_32 @ Bound_variable_1538 @ Bound_variable_1522 @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( Bound_variable_1538 @ X @ Y ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( zip_tseitin_0 @
% 63.41/9.70 Bound_variable_663 @ Bound_variable_661 @
% 63.41/9.70 Bound_variable_1538 @ R ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( zip_tseitin_8 @
% 63.41/9.70 Bound_variable_1106 @ Bound_variable_674 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1538 ) ) ) |
% 63.41/9.70 ( Bound_variable_1522 @ Y @ X ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( zip_tseitin_0 @
% 63.41/9.70 Bound_variable_663 @ Bound_variable_661 @
% 63.41/9.70 Bound_variable_1522 @ R ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( zip_tseitin_8 @
% 63.41/9.70 Bound_variable_1125 @ Bound_variable_674 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1522 ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_1218:$i]:
% 63.41/9.70 ( zip_tseitin_25 @ Bound_variable_1218 @ Y @ X @ R ) ) ) |
% 63.41/9.70 ( ( X ) = ( Y ) ) | ( zip_tseitin_31 @ Y @ X @ R ) ) ))).
% 63.41/9.70 thf(zf_stmt_3, type, zip_tseitin_31 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_4, axiom,
% 63.41/9.70 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_31 @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( ~( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ Y @ X @ R ) ) ) &
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ X @ Y @ R ) ) ) &
% 63.41/9.70 ( ( X ) != ( Y ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_5, type, zip_tseitin_30 :
% 63.41/9.70 ( $i > $i > $o ) > ( $i > $i > $o ) > $i > $i > $i > ( $i > $i > $o ) >
% 63.41/9.70 $o).
% 63.41/9.70 thf(zf_stmt_6, axiom,
% 63.41/9.70 (![Bound_variable_1460:( $i > $i > $o ),
% 63.41/9.70 Bound_variable_1444:( $i > $i > $o ),Z:$i,Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_30 @
% 63.41/9.70 Bound_variable_1460 @ Bound_variable_1444 @ Z @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( Bound_variable_1460 @ Z @ Y ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( zip_tseitin_0 @
% 63.41/9.70 Bound_variable_663 @ Bound_variable_661 @
% 63.41/9.70 Bound_variable_1460 @ R ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( zip_tseitin_8 @
% 63.41/9.70 Bound_variable_1106 @ Bound_variable_674 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1460 ) ) ) |
% 63.41/9.70 ( Bound_variable_1444 @ Y @ Z ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( zip_tseitin_0 @
% 63.41/9.70 Bound_variable_663 @ Bound_variable_661 @
% 63.41/9.70 Bound_variable_1444 @ R ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( zip_tseitin_8 @
% 63.41/9.70 Bound_variable_1125 @ Bound_variable_674 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1444 ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_1218:$i]:
% 63.41/9.70 ( zip_tseitin_25 @ Bound_variable_1218 @ Y @ Z @ R ) ) ) |
% 63.41/9.70 ( ( Y ) = ( Z ) ) | ( zip_tseitin_28 @ Y @ X @ R ) |
% 63.41/9.70 ( zip_tseitin_28 @ Z @ X @ R ) ) ))).
% 63.41/9.70 thf(zf_stmt_7, type, zip_tseitin_29 :
% 63.41/9.70 ( $i > $i > $o ) > ( $i > $i > $o ) > $i > $i > $i > ( $i > $i > $o ) >
% 63.41/9.70 $o).
% 63.41/9.70 thf(zf_stmt_8, axiom,
% 63.41/9.70 (![Bound_variable_1387:( $i > $i > $o ),
% 63.41/9.70 Bound_variable_1371:( $i > $i > $o ),Z:$i,Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_29 @
% 63.41/9.70 Bound_variable_1387 @ Bound_variable_1371 @ Z @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( Bound_variable_1387 @ Z @ Y ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( zip_tseitin_0 @
% 63.41/9.70 Bound_variable_663 @ Bound_variable_661 @
% 63.41/9.70 Bound_variable_1387 @ R ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( zip_tseitin_8 @
% 63.41/9.70 Bound_variable_1106 @ Bound_variable_674 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1387 ) ) ) |
% 63.41/9.70 ( Bound_variable_1371 @ Y @ Z ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( zip_tseitin_0 @
% 63.41/9.70 Bound_variable_663 @ Bound_variable_661 @
% 63.41/9.70 Bound_variable_1371 @ R ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( zip_tseitin_8 @
% 63.41/9.70 Bound_variable_1125 @ Bound_variable_674 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1371 ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_1218:$i]:
% 63.41/9.70 ( zip_tseitin_25 @ Bound_variable_1218 @ Y @ Z @ R ) ) ) |
% 63.41/9.70 ( ( Y ) = ( Z ) ) | ( zip_tseitin_28 @ Y @ X @ R ) |
% 63.41/9.70 ( ~( R @ X @ Z ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_9, type, zip_tseitin_28 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_10, axiom,
% 63.41/9.70 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_28 @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( ~( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ Y @ X @ R ) ) ) &
% 63.41/9.70 ( ( X ) != ( Y ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_11, type, zip_tseitin_27 :
% 63.41/9.70 ( $i > $i > $o ) > ( $i > $i > $o ) > $i > $i > $i > ( $i > $i > $o ) >
% 63.41/9.70 $o).
% 63.41/9.70 thf(zf_stmt_12, axiom,
% 63.41/9.70 (![Bound_variable_1309:( $i > $i > $o ),
% 63.41/9.70 Bound_variable_1293:( $i > $i > $o ),Z:$i,Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_27 @
% 63.41/9.70 Bound_variable_1309 @ Bound_variable_1293 @ Z @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( Bound_variable_1309 @ Z @ Y ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( zip_tseitin_0 @
% 63.41/9.70 Bound_variable_663 @ Bound_variable_661 @
% 63.41/9.70 Bound_variable_1309 @ R ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1106:$i]:
% 63.41/9.70 ( zip_tseitin_8 @
% 63.41/9.70 Bound_variable_1106 @ Bound_variable_674 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1309 ) ) ) |
% 63.41/9.70 ( Bound_variable_1293 @ Y @ Z ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( zip_tseitin_0 @
% 63.41/9.70 Bound_variable_663 @ Bound_variable_661 @
% 63.41/9.70 Bound_variable_1293 @ R ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 63.41/9.70 Bound_variable_1125:$i]:
% 63.41/9.70 ( zip_tseitin_8 @
% 63.41/9.70 Bound_variable_1125 @ Bound_variable_674 @
% 63.41/9.70 Bound_variable_672 @ Bound_variable_1293 ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_1218:$i]:
% 63.41/9.70 ( zip_tseitin_25 @ Bound_variable_1218 @ Y @ Z @ R ) ) ) |
% 63.41/9.70 ( ( Y ) = ( Z ) ) | ( ~( R @ X @ Y ) ) | ( ~( R @ X @ Z ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_13, type, zip_tseitin_26 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_14, axiom,
% 63.41/9.70 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_26 @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( ( X ) != ( Y ) ) &
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ X @ Y @ R ) ) ) &
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ Y @ X @ R ) ) ) &
% 63.41/9.70 ( ![Bound_variable_1218:$i]:
% 63.41/9.70 ( zip_tseitin_25 @ Bound_variable_1218 @ Y @ X @ R ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_15, type, zip_tseitin_25 : $i > $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_16, axiom,
% 63.41/9.70 (![Bound_variable_1218:$i,Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_25 @ Bound_variable_1218 @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( zip_tseitin_9 @ S @ Bound_variable_1218 @ X @ R ) ) ) |
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( zip_tseitin_9 @ S @ Bound_variable_1218 @ Y @ R ) ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_17, type, zip_tseitin_24 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_18, axiom,
% 63.41/9.70 (![Bound_variable_1075:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_24 @ Bound_variable_1075 @ X @ R ) <=>
% 63.41/9.70 ( ( ~( ![Bound_variable_1049:$i]:
% 63.41/9.70 ( zip_tseitin_23 @ Bound_variable_1049 @ X @ R ) ) ) |
% 63.41/9.70 ( ~( R @ X @ Bound_variable_1075 ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_19, type, zip_tseitin_23 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_20, axiom,
% 63.41/9.70 (![Bound_variable_1049:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_23 @ Bound_variable_1049 @ X @ R ) <=>
% 63.41/9.70 ( ( ~( ![Bound_variable_985:$i]:
% 63.41/9.70 ( ~( R @ Bound_variable_1049 @ Bound_variable_985 ) ) ) ) |
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( zip_tseitin_9 @ S @ Bound_variable_1049 @ X @ R ) ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_21, type, zip_tseitin_22 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_22, axiom,
% 63.41/9.70 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_22 @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( zip_tseitin_21 @ Y @ X @ R ) &
% 63.41/9.70 ( ![Bound_variable_985:$i]: ( ~( R @ X @ Bound_variable_985 ) ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_23, type, zip_tseitin_21 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_24, axiom,
% 63.41/9.70 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_21 @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( ( X ) = ( Y ) ) |
% 63.41/9.70 ( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ X @ Y @ R ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_25, type, zip_tseitin_20 :
% 63.41/9.70 $i > ( $i > $o ) > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_26, axiom,
% 63.41/9.70 (![Bound_variable_917:$i,P:( $i > $o ),R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_20 @ Bound_variable_917 @ P @ R ) <=>
% 63.41/9.70 ( ( P @ Bound_variable_917 ) |
% 63.41/9.70 ( ~( ![X:$i]: ( zip_tseitin_19 @ X @ P @ R ) ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_27, type, zip_tseitin_19 :
% 63.41/9.70 $i > ( $i > $o ) > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_28, axiom,
% 63.41/9.70 (![X:$i,P:( $i > $o ),R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_19 @ X @ P @ R ) <=>
% 63.41/9.70 ( ( P @ X ) | ( ~( ![Y:$i]: ( zip_tseitin_18 @ Y @ X @ P @ R ) ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_29, type, zip_tseitin_18 :
% 63.41/9.70 $i > $i > ( $i > $o ) > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_30, axiom,
% 63.41/9.70 (![Y:$i,X:$i,P:( $i > $o ),R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_18 @ Y @ X @ P @ R ) <=>
% 63.41/9.70 ( ( P @ Y ) |
% 63.41/9.70 ( ~( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ Y @ X @ R ) ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_31, type, zip_tseitin_17 :
% 63.41/9.70 $i > ( $i > $o ) > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_32, axiom,
% 63.41/9.70 (![Bound_variable_862:$i,A:( $i > $o ),R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_17 @ Bound_variable_862 @ A @ R ) <=>
% 63.41/9.70 ( ( ~( ![X:$i]: ( zip_tseitin_16 @ X @ A @ R ) ) ) |
% 63.41/9.70 ( ~( A @ Bound_variable_862 ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_33, type, zip_tseitin_16 :
% 63.41/9.70 $i > ( $i > $o ) > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_34, axiom,
% 63.41/9.70 (![X:$i,A:( $i > $o ),R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_16 @ X @ A @ R ) <=>
% 63.41/9.70 ( ( ~( ![Y:$i]: ( zip_tseitin_15 @ Y @ X @ A @ R ) ) ) | ( ~( A @ X ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_35, type, zip_tseitin_15 :
% 63.41/9.70 $i > $i > ( $i > $o ) > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_36, axiom,
% 63.41/9.70 (![Y:$i,X:$i,A:( $i > $o ),R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_15 @ Y @ X @ A @ R ) <=>
% 63.41/9.70 ( ( ~( R @ X @ Y ) ) | ( ~( A @ Y ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_37, type, zip_tseitin_14 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_38, axiom,
% 63.41/9.70 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_14 @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( R @ Y @ X ) | ( R @ X @ Y ) | ( ( X ) = ( Y ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_39, type, zip_tseitin_13 : ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_40, axiom,
% 63.41/9.70 (![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_13 @ R ) <=>
% 63.41/9.70 ( ( ![X:$i,Y:$i]: ( zip_tseitin_6 @ Y @ X @ R ) ) &
% 63.41/9.70 ( ![X:$i,Y:$i,Z:$i]: ( zip_tseitin_8 @ Z @ Y @ X @ R ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_41, type, zip_tseitin_12 : ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_42, axiom,
% 63.41/9.70 (![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_12 @ R ) <=>
% 63.41/9.70 ( ( ![X:$i]: ( R @ X @ X ) ) &
% 63.41/9.70 ( ![X:$i,Y:$i]: ( zip_tseitin_5 @ Y @ X @ R ) ) &
% 63.41/9.70 ( ![X:$i,Y:$i,Z:$i]: ( zip_tseitin_8 @ Z @ Y @ X @ R ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_43, type, zip_tseitin_11 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_44, type, zip_tseitin_10 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_45, axiom,
% 63.41/9.70 (![Flatten_var_1:$i,Flatten_var_0:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_10 @ Flatten_var_1 @ Flatten_var_0 @ R ) <=>
% 63.41/9.70 ( ( ( Flatten_var_0 ) = ( Flatten_var_1 ) ) |
% 63.41/9.70 ( ![S:( $i > $i > $o )]:
% 63.41/9.70 ( zip_tseitin_9 @ S @ Flatten_var_1 @ Flatten_var_0 @ R ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_46, type, zip_tseitin_9 :
% 63.41/9.70 ( $i > $i > $o ) > $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_47, axiom,
% 63.41/9.70 (![S:( $i > $i > $o ),Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_9 @ S @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( S @ X @ Y ) |
% 63.41/9.70 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 63.41/9.70 ( zip_tseitin_0 @ Bound_variable_663 @ Bound_variable_661 @ S @ R ) ) ) |
% 63.41/9.70 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 63.41/9.70 ( zip_tseitin_8 @ Z @ Bound_variable_674 @ Bound_variable_672 @ S ) ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_48, type, zip_tseitin_8 : $i > $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_49, axiom,
% 63.41/9.70 (![Z:$i,Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_8 @ Z @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( R @ X @ Z ) | ( ~( R @ Y @ Z ) ) | ( ~( R @ X @ Y ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_50, type, zip_tseitin_7 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_51, axiom,
% 63.41/9.70 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_7 @ Y @ X @ R ) <=> ( ( R @ Y @ X ) | ( R @ X @ Y ) ) ))).
% 63.41/9.70 thf(zf_stmt_52, type, zip_tseitin_6 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_53, axiom,
% 63.41/9.70 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_6 @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( ~( R @ Y @ X ) ) | ( ~( R @ X @ Y ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_54, type, zip_tseitin_5 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_55, axiom,
% 63.41/9.70 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_5 @ Y @ X @ R ) <=>
% 63.41/9.70 ( ( ( X ) = ( Y ) ) | ( ~( R @ Y @ X ) ) | ( ~( R @ X @ Y ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_56, type, zip_tseitin_4 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_57, axiom,
% 63.41/9.70 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_4 @ Y @ X @ R ) <=> ( ( R @ Y @ X ) | ( ~( R @ X @ Y ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_58, type, zip_tseitin_3 : $i > $i > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_59, axiom,
% 63.41/9.70 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_3 @ Y @ X @ R ) <=> ( ( ( X ) = ( Y ) ) | ( R @ X @ Y ) ) ))).
% 63.41/9.70 thf(zf_stmt_60, type, zip_tseitin_2 :
% 63.41/9.70 $i > $i > ( $i > $i > $o ) > ( $i > $i > $o ) >
% 63.41/9.70 ( ( $i > $i > $o ) > $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_61, axiom,
% 63.41/9.70 (![Bound_variable_512:$i,Bound_variable_510:$i,S:( $i > $i > $o ),
% 63.41/9.70 R:( $i > $i > $o ),F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_2 @ Bound_variable_512 @ Bound_variable_510 @ S @ R @ F ) <=>
% 63.41/9.70 ( ( F @ S @ Bound_variable_510 @ Bound_variable_512 ) |
% 63.41/9.70 ( ~( F @ R @ Bound_variable_510 @ Bound_variable_512 ) ) |
% 63.41/9.70 ( ~( ![X:$i,Y:$i]: ( zip_tseitin_0 @ Y @ X @ S @ R ) ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_62, type, zip_tseitin_1 :
% 63.41/9.70 $i > $i > ( $i > $i > $o ) > ( ( $i > $i > $o ) > $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_63, axiom,
% 63.41/9.70 (![Y:$i,X:$i,R:( $i > $i > $o ),F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_1 @ Y @ X @ R @ F ) <=>
% 63.41/9.70 ( ( F @ R @ X @ Y ) | ( ~( R @ X @ Y ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_64, type, zip_tseitin_0 :
% 63.41/9.70 $i > $i > ( $i > $i > $o ) > ( $i > $i > $o ) > $o).
% 63.41/9.70 thf(zf_stmt_65, axiom,
% 63.41/9.70 (![Y:$i,X:$i,S:( $i > $i > $o ),R:( $i > $i > $o )]:
% 63.41/9.70 ( ( zip_tseitin_0 @ Y @ X @ S @ R ) <=>
% 63.41/9.70 ( ( S @ X @ Y ) | ( ~( R @ X @ Y ) ) ) ))).
% 63.41/9.70 thf(zf_stmt_66, axiom,
% 63.41/9.70 (( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( cr @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i,Bound_variable_1522:( $i > $i > $o ),
% 63.41/9.70 Bound_variable_1538:( $i > $i > $o )]:
% 63.41/9.70 ( zip_tseitin_32 @
% 63.41/9.70 Bound_variable_1538 @ Bound_variable_1522 @ Y @ X @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( confl @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i,Z:$i,Bound_variable_1444:( $i > $i > $o ),
% 63.41/9.70 Bound_variable_1460:( $i > $i > $o )]:
% 63.41/9.70 ( zip_tseitin_30 @
% 63.41/9.70 Bound_variable_1460 @ Bound_variable_1444 @ Z @ Y @ X @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( sconfl @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i,Z:$i,Bound_variable_1371:( $i > $i > $o ),
% 63.41/9.70 Bound_variable_1387:( $i > $i > $o )]:
% 63.41/9.70 ( zip_tseitin_29 @
% 63.41/9.70 Bound_variable_1387 @ Bound_variable_1371 @ Z @ Y @ X @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( lconfl @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i,Z:$i,Bound_variable_1293:( $i > $i > $o ),
% 63.41/9.70 Bound_variable_1309:( $i > $i > $o )]:
% 63.41/9.70 ( zip_tseitin_27 @
% 63.41/9.70 Bound_variable_1309 @ Bound_variable_1293 @ Z @ Y @ X @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( join @ R @ X @ Y ) <=> ( ~( zip_tseitin_26 @ Y @ X @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( norm @ R ) <=>
% 63.41/9.70 ( ![X:$i,Bound_variable_1075:$i]:
% 63.41/9.70 ( zip_tseitin_24 @ Bound_variable_1075 @ X @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( nfof @ R @ X @ Y ) <=> ( zip_tseitin_22 @ Y @ X @ R ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i]:
% 63.41/9.70 ( ( innf @ R @ X ) <=> ( ![Y:$i]: ( ~( R @ X @ Y ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( ind @ R ) <=>
% 63.41/9.70 ( ![P:( $i > $o ),Bound_variable_917:$i]:
% 63.41/9.70 ( zip_tseitin_20 @ Bound_variable_917 @ P @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( term @ R ) <=>
% 63.41/9.70 ( ![A:( $i > $o ),Bound_variable_862:$i]:
% 63.41/9.70 ( zip_tseitin_17 @ Bound_variable_862 @ A @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( total @ R ) <=> ( ![X:$i,Y:$i]: ( zip_tseitin_14 @ Y @ X @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]: ( ( so @ R ) <=> ( zip_tseitin_13 @ R ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]: ( ( po @ R ) <=> ( zip_tseitin_12 @ R ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),Flatten_var_0:$i,Flatten_var_1:$i]:
% 63.41/9.70 ( ( trsc @ R @ Flatten_var_0 @ Flatten_var_1 ) <=>
% 63.41/9.70 ( zip_tseitin_11 @ Flatten_var_1 @ Flatten_var_0 @ R ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),Flatten_var_0:$i,Flatten_var_1:$i]:
% 63.41/9.70 ( ( trc @ R @ Flatten_var_0 @ Flatten_var_1 ) <=>
% 63.41/9.70 ( zip_tseitin_10 @ Flatten_var_1 @ Flatten_var_0 @ R ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( tc @ R @ X @ Y ) <=>
% 63.41/9.70 ( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ Y @ X @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( trans @ R ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i,Z:$i]: ( zip_tseitin_8 @ Z @ Y @ X @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( sc @ R @ X @ Y ) <=> ( zip_tseitin_7 @ Y @ X @ R ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( asymm @ R ) <=> ( ![X:$i,Y:$i]: ( zip_tseitin_6 @ Y @ X @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( antisymm @ R ) <=> ( ![X:$i,Y:$i]: ( zip_tseitin_5 @ Y @ X @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( symm @ R ) <=> ( ![X:$i,Y:$i]: ( zip_tseitin_4 @ Y @ X @ R ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( rc @ R @ X @ Y ) <=> ( zip_tseitin_3 @ Y @ X @ R ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]:
% 63.41/9.70 ( ( irrefl @ R ) <=> ( ![X:$i]: ( ~( R @ X @ X ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o )]: ( ( refl @ R ) <=> ( ![X:$i]: ( R @ X @ X ) ) ) ) &
% 63.41/9.70 ( ![F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 63.41/9.70 ( ( mono @ F ) <=>
% 63.41/9.70 ( ![R:( $i > $i > $o ),S:( $i > $i > $o ),Bound_variable_510:$i,
% 63.41/9.70 Bound_variable_512:$i]:
% 63.41/9.70 ( zip_tseitin_2 @
% 63.41/9.70 Bound_variable_512 @ Bound_variable_510 @ S @ R @ F ) ) ) ) &
% 63.41/9.70 ( ![F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 63.41/9.70 ( ( infl @ F ) <=>
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]: ( zip_tseitin_1 @ Y @ X @ R @ F ) ) ) ) &
% 63.41/9.70 ( ![F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 63.41/9.70 ( ( idem @ F ) <=>
% 63.41/9.70 ( ![R:( $i > $i > $o )]: ( ( F @ R ) = ( F @ ( F @ R ) ) ) ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 63.41/9.70 ( ( inv @ R @ X @ Y ) <=> ( R @ Y @ X ) ) ) &
% 63.41/9.70 ( ![R:( $i > $i > $o ),S:( $i > $i > $o )]:
% 63.41/9.70 ( ( subrel @ R @ S ) <=>
% 63.41/9.70 ( ![X:$i,Y:$i]: ( zip_tseitin_0 @ Y @ X @ S @ R ) ) ) ) &
% 63.41/9.70 ( ![DU1:d_unsorted,DU2:d_unsorted]:
% 63.41/9.70 ( ( ( d2unsorted @ DU1 ) = ( d2unsorted @ DU2 ) ) =>
% 63.41/9.70 ( ( DU1 ) = ( DU2 ) ) ) ) &
% 63.41/9.70 ( ![DU:d_unsorted]: ( ( DU ) = ( d_unsorted_0 ) ) ) &
% 63.41/9.70 ( ![U:$i]: ( ?[DU:d_unsorted]: ( ( U ) = ( d2unsorted @ DU ) ) ) ))).
% 63.41/9.70 thf(zip_derived_cl173, plain,
% 63.41/9.70 (![X0 : $i > $i > $o, X1 : $i, X2 : $i]:
% 63.41/9.70 ( (trsc @ X0 @ X1 @ X2) | ~ (zip_tseitin_11 @ X2 @ X1 @ X0))),
% 63.41/9.70 inference('cnf', [status(esa)], [zf_stmt_66])).
% 63.41/9.70 thf(zip_derived_cl154, plain,
% 63.41/9.70 (![X0 : $i > $i > $o, X1 : $i]: ( (X0 @ X1 @ X1) | ~ (refl @ X0))),
% 63.41/9.70 inference('cnf', [status(esa)], [zf_stmt_66])).
% 63.41/9.70 thf(zip_derived_cl11, plain,
% 63.41/9.70 (![X0 : $i, X1 : $i, X2 : $i > $i > $o]:
% 63.41/9.70 ( (zip_tseitin_3 @ X0 @ X1 @ X2) | ((X1) != (X0)))),
% 63.41/9.70 inference('cnf', [status(esa)], [zf_stmt_59])).
% 63.41/9.70 thf(zip_derived_cl157, plain,
% 63.41/9.70 (![X0 : $i > $i > $o, X1 : $i, X2 : $i]:
% 63.41/9.70 ( (rc @ X0 @ X1 @ X2) | ~ (zip_tseitin_3 @ X2 @ X1 @ X0))),
% 63.41/9.70 inference('cnf', [status(esa)], [zf_stmt_66])).
% 63.41/9.70 thf(zip_derived_cl25, plain,
% 63.41/9.70 (![X0 : $i, X1 : $i, X2 : $i > $i > $o]:
% 63.41/9.70 ( (zip_tseitin_7 @ X0 @ X1 @ X2) | ~ (X2 @ X1 @ X0))),
% 63.41/9.70 inference('cnf', [status(esa)], [zf_stmt_51])).
% 63.41/9.70 thf(zip_derived_cl153, plain,
% 63.41/9.70 (![X0 : $i > $i > $o]:
% 63.41/9.70 ( (refl @ X0) | ~ (X0 @ (sk__122 @ X0) @ (sk__122 @ X0)))),
% 63.41/9.70 inference('cnf', [status(esa)], [zf_stmt_66])).
% 63.41/9.70 thf(zip_derived_cl165, plain,
% 63.41/9.70 (![X0 : $i > $i > $o, X1 : $i, X2 : $i]:
% 63.41/9.70 ( (sc @ X0 @ X1 @ X2) | ~ (zip_tseitin_7 @ X2 @ X1 @ X0))),
% 63.41/9.70 inference('cnf', [status(esa)], [zf_stmt_66])).
% 63.41/9.70 thf(transitive_reflexive_symmetric_closure, conjecture,
% 63.41/9.70 (![R:( $i > $i > $o ),X_1:$i,X_2:$i]:
% 63.41/9.70 ( ( trsc @ R @ X_1 @ X_2 ) <=> ( sc @ ( rc @ ( tc @ R ) ) @ X_1 @ X_2 ) ))).
% 63.41/9.70 thf(zf_stmt_67, negated_conjecture,
% 63.41/9.70 (~( ![R:( $i > $i > $o ),X_1:$i,X_2:$i]:
% 63.41/9.70 ( ( trsc @ R @ X_1 @ X_2 ) <=> ( sc @ ( rc @ ( tc @ R ) ) @ X_1 @ X_2 ) ) )),
% 63.41/9.70 inference('cnf.neg', [status(esa)],
% 63.41/9.70 [transitive_reflexive_symmetric_closure])).
% 63.41/9.70 thf(zip_derived_cl202, plain,
% 63.41/9.70 ((~ (sc @ (rc @ (tc @ sk__134)) @ sk__135 @ sk__136)
% 63.41/9.70 | ~ (trsc @ sk__134 @ sk__135 @ sk__136))),
% 63.41/9.70 inference('cnf', [status(esa)], [zf_stmt_67])).
% 63.41/9.70 thf(zip_derived_cl140, plain,
% 63.41/9.70 (![X0 : $i]: ((X0) = (d2unsorted @ (sk__133 @ X0)))),
% 63.41/9.70 inference('cnf', [status(esa)], [zf_stmt_66])).
% 63.41/9.70 thf(zip_derived_cl141, plain, (![X0 : d_unsorted]: ((X0) = (d_unsorted_0))),
% 63.41/9.70 inference('cnf', [status(esa)], [zf_stmt_66])).
% 63.41/9.70 thf(zip_derived_cl207, plain,
% 63.41/9.70 (![X0 : $i]: ((X0) = (d2unsorted @ d_unsorted_0))),
% 63.41/9.70 inference('demod', [status(thm)], [zip_derived_cl140, zip_derived_cl141])).
% 63.41/9.70 thf(zip_derived_cl207, plain,
% 63.41/9.70 (![X0 : $i]: ((X0) = (d2unsorted @ d_unsorted_0))),
% 63.41/9.70 inference('demod', [status(thm)], [zip_derived_cl140, zip_derived_cl141])).
% 63.41/9.70 thf(zip_derived_cl208, plain,
% 63.41/9.70 (![X0 : $i]: ((X0) = (d2unsorted @ d_unsorted_0))),
% 63.41/9.70 inference('sup+', [status(thm)], [zip_derived_cl207, zip_derived_cl207])).
% 63.41/9.70 thf(zip_derived_cl141, plain, (![X0 : d_unsorted]: ((X0) = (d_unsorted_0))),
% 63.41/9.70 inference('cnf', [status(esa)], [zf_stmt_66])).
% 63.41/9.70 thf(zip_derived_cl207, plain,
% 63.41/9.70 (![X0 : $i]: ((X0) = (d2unsorted @ d_unsorted_0))),
% 63.41/9.70 inference('demod', [status(thm)], [zip_derived_cl140, zip_derived_cl141])).
% 63.41/9.70 thf(zip_derived_cl211, plain,
% 63.41/9.70 (![X0 : $i]: ((X0) = (d2unsorted @ d_unsorted_0))),
% 63.41/9.70 inference('sup+', [status(thm)], [zip_derived_cl141, zip_derived_cl207])).
% 63.41/9.70 thf(zip_derived_cl6347, plain, ($false),
% 63.41/9.70 inference('eprover', [status(thm)],
% 63.41/9.70 [zip_derived_cl38, zip_derived_cl173, zip_derived_cl154,
% 63.41/9.70 zip_derived_cl11, zip_derived_cl157, zip_derived_cl25,
% 63.41/9.70 zip_derived_cl153, zip_derived_cl165, zip_derived_cl202,
% 63.41/9.70 zip_derived_cl208, zip_derived_cl211])).
% 63.41/9.70
% 63.41/9.70 % SZS output end Refutation
% 63.41/9.70
% 63.41/9.70
% 63.41/9.70 % Terminating...
% 63.41/9.79 % Runner terminated.
% 0.25/9.80 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------