%------------------------------------------------------------------------------
% 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/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.yz7RNX5tjg true
% Computer : n006.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:46 PM UTC 2026
% Result : Theorem 67.33s 9.12s
% Output : Refutation 67.33s
% 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/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.yz7RNX5tjg true
% 0.15/0.34 % Computer : n006.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:37:31 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 % Running portfolio for 300 s
% 0.15/0.34 % File : /export/starexec/sandbox/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.43/0.59 % Total configuration time : 828
% 0.43/0.59 % Estimated wc time : 1656
% 0.43/0.59 % Estimated cpu time (8 cpus) : 207.0
% 0.49/0.68 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.49/0.68 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.49/0.68 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.49/0.68 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.49/0.69 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 0.50/0.70 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 0.50/0.70 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.50/0.74 % /export/starexec/sandbox/solver/bin/lams/30_sp5.sh running for 60s
% 67.33/9.12 % Solved by lams/40_c_ic.sh.
% 67.33/9.12 % done 213 iterations in 8.411s
% 67.33/9.12 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 67.33/9.12 % SZS output start Refutation
% 67.33/9.12 thf(d_unsorted_type, type, d_unsorted: $tType).
% 67.33/9.12 thf(trans_type, type, trans: ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_22_type, type, zip_tseitin_22: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(nfof_type, type, nfof: ($i > $i > $o) > $i > $i > $o).
% 67.33/9.12 thf(cr_type, type, cr: ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_27_type, type, zip_tseitin_27: ($i > $i > $o) >
% 67.33/9.12 ($i > $i > $o) > $i > $i >
% 67.33/9.12 $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(infl_type, type, infl: (($i > $i > $o) > $i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_6_type, type, zip_tseitin_6: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(sk__134_type, type, sk__134: $i > $i > $o).
% 67.33/9.12 thf(sk__101_type, type, sk__101: ($i > $i > $o) > $i > $i > $o).
% 67.33/9.12 thf(d_unsorted_0_type, type, d_unsorted_0: d_unsorted).
% 67.33/9.12 thf(zip_tseitin_8_type, type, zip_tseitin_8: $i > $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_9_type, type, zip_tseitin_9: ($i > $i > $o) > $i > $i >
% 67.33/9.12 ($i > $i > $o) > $o).
% 67.33/9.12 thf(asymm_type, type, asymm: ($i > $i > $o) > $o).
% 67.33/9.12 thf(rc_type, type, rc: ($i > $i > $o) > $i > $i > $o).
% 67.33/9.12 thf(zip_tseitin_19_type, type, zip_tseitin_19: $i > ($i > $o) >
% 67.33/9.12 ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(trsc_type, type, trsc: ($i > $i > $o) > $i > $i > $o).
% 67.33/9.12 thf(norm_type, type, norm: ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_15_type, type, zip_tseitin_15: $i > $i > ($i > $o) >
% 67.33/9.12 ($i > $i > $o) > $o).
% 67.33/9.12 thf(trc_type, type, trc: ($i > $i > $o) > $i > $i > $o).
% 67.33/9.12 thf(zip_tseitin_20_type, type, zip_tseitin_20: $i > ($i > $o) >
% 67.33/9.12 ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_16_type, type, zip_tseitin_16: $i > ($i > $o) >
% 67.33/9.12 ($i > $i > $o) > $o).
% 67.33/9.12 thf(so_type, type, so: ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_29_type, type, zip_tseitin_29: ($i > $i > $o) >
% 67.33/9.12 ($i > $i > $o) > $i > $i >
% 67.33/9.12 $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_30_type, type, zip_tseitin_30: ($i > $i > $o) >
% 67.33/9.12 ($i > $i > $o) > $i > $i >
% 67.33/9.12 $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(inv_type, type, inv: ($i > $i > $o) > $i > $i > $o).
% 67.33/9.12 thf(refl_type, type, refl: ($i > $i > $o) > $o).
% 67.33/9.12 thf(symm_type, type, symm: ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_32_type, type, zip_tseitin_32: ($i > $i > $o) >
% 67.33/9.12 ($i > $i > $o) > $i > $i >
% 67.33/9.12 ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(ind_type, type, ind: ($i > $i > $o) > $o).
% 67.33/9.12 thf(total_type, type, total: ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_13_type, type, zip_tseitin_13: ($i > $i > $o) > $o).
% 67.33/9.12 thf(irrefl_type, type, irrefl: ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > ($i > $i > $o) >
% 67.33/9.12 ($i > $i > $o) >
% 67.33/9.12 (($i > $i > $o) > $i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_17_type, type, zip_tseitin_17: $i > ($i > $o) >
% 67.33/9.12 ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_26_type, type, zip_tseitin_26: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(sk__98_type, type, sk__98: ($i > $i > $o) > $i).
% 67.33/9.12 thf(sk__97_type, type, sk__97: ($i > $i > $o) > $i).
% 67.33/9.12 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > ($i > $i > $o) >
% 67.33/9.12 ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_21_type, type, zip_tseitin_21: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_23_type, type, zip_tseitin_23: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_31_type, type, zip_tseitin_31: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(confl_type, type, confl: ($i > $i > $o) > $o).
% 67.33/9.12 thf(mono_type, type, mono: (($i > $i > $o) > $i > $i > $o) > $o).
% 67.33/9.12 thf(idem_type, type, idem: (($i > $i > $o) > $i > $i > $o) > $o).
% 67.33/9.12 thf(innf_type, type, innf: ($i > $i > $o) > $i > $o).
% 67.33/9.12 thf(antisymm_type, type, antisymm: ($i > $i > $o) > $o).
% 67.33/9.12 thf(lconfl_type, type, lconfl: ($i > $i > $o) > $o).
% 67.33/9.12 thf(subrel_type, type, subrel: ($i > $i > $o) > ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_12_type, type, zip_tseitin_12: ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_25_type, type, zip_tseitin_25: $i > $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(sk__100_type, type, sk__100: ($i > $i > $o) > $i > $i > $o).
% 67.33/9.12 thf(term_type, type, term: ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_14_type, type, zip_tseitin_14: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_28_type, type, zip_tseitin_28: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(sconfl_type, type, sconfl: ($i > $i > $o) > $o).
% 67.33/9.12 thf(sk__99_type, type, sk__99: ($i > $i > $o) > $i).
% 67.33/9.12 thf(zip_tseitin_18_type, type, zip_tseitin_18: $i > $i > ($i > $o) >
% 67.33/9.12 ($i > $i > $o) > $o).
% 67.33/9.12 thf(sk__137_type, type, sk__137: $i).
% 67.33/9.12 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(join_type, type, join: ($i > $i > $o) > $i > $i > $o).
% 67.33/9.12 thf(po_type, type, po: ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_10_type, type, zip_tseitin_10: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > ($i > $i > $o) >
% 67.33/9.12 (($i > $i > $o) > $i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_11_type, type, zip_tseitin_11: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(sc_type, type, sc: ($i > $i > $o) > $i > $i > $o).
% 67.33/9.12 thf(sk__133_type, type, sk__133: $i > d_unsorted).
% 67.33/9.12 thf(sk__136_type, type, sk__136: $i).
% 67.33/9.12 thf(tc_type, type, tc: ($i > $i > $o) > $i > $i > $o).
% 67.33/9.12 thf(d2unsorted_type, type, d2unsorted: d_unsorted > $i).
% 67.33/9.12 thf(zip_tseitin_24_type, type, zip_tseitin_24: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $i > ($i > $i > $o) > $o).
% 67.33/9.12 thf(sev441_1, axiom,
% 67.33/9.12 (( ![U:$i]: ( ?[DU:d_unsorted]: ( ( U ) = ( d2unsorted @ DU ) ) ) ) &
% 67.33/9.12 ( ![DU:d_unsorted]: ( ( DU ) = ( d_unsorted_0 ) ) ) &
% 67.33/9.12 ( ![DU1:d_unsorted,DU2:d_unsorted]:
% 67.33/9.12 ( ( ( d2unsorted @ DU1 ) = ( d2unsorted @ DU2 ) ) =>
% 67.33/9.12 ( ( DU1 ) = ( DU2 ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o ),S:( $i > $i > $o )]:
% 67.33/9.12 ( ( subrel @ R @ S ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i]: ( ( ~( R @ X @ Y ) ) | ( S @ X @ Y ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.12 ( ( inv @ R @ X @ Y ) <=> ( R @ Y @ X ) ) ) &
% 67.33/9.12 ( ![F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 67.33/9.12 ( ( idem @ F ) <=>
% 67.33/9.12 ( ![R:( $i > $i > $o )]: ( ( F @ R ) = ( F @ ( F @ R ) ) ) ) ) ) &
% 67.33/9.12 ( ![F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 67.33/9.12 ( ( infl @ F ) <=>
% 67.33/9.12 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.12 ( ( ~( R @ X @ Y ) ) | ( F @ R @ X @ Y ) ) ) ) ) &
% 67.33/9.12 ( ![F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 67.33/9.12 ( ( mono @ F ) <=>
% 67.33/9.12 ( ![R:( $i > $i > $o ),S:( $i > $i > $o ),Bound_variable_510:$i,
% 67.33/9.12 Bound_variable_512:$i]:
% 67.33/9.12 ( ( ~( ![X:$i,Y:$i]: ( ( ~( R @ X @ Y ) ) | ( S @ X @ Y ) ) ) ) |
% 67.33/9.12 ( ~( F @ R @ Bound_variable_510 @ Bound_variable_512 ) ) |
% 67.33/9.12 ( F @ S @ Bound_variable_510 @ Bound_variable_512 ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]: ( ( refl @ R ) <=> ( ![X:$i]: ( R @ X @ X ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( irrefl @ R ) <=> ( ![X:$i]: ( ~( R @ X @ X ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.12 ( ( rc @ R @ X @ Y ) <=> ( ( R @ X @ Y ) | ( ( X ) = ( Y ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( symm @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i]: ( ( ~( R @ X @ Y ) ) | ( R @ Y @ X ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( antisymm @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i]:
% 67.33/9.12 ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ X ) ) | ( ( X ) = ( Y ) ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( asymm @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i]: ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ X ) ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.12 ( ( sc @ R @ X @ Y ) <=> ( ( R @ X @ Y ) | ( R @ Y @ X ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( trans @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i,Z:$i]:
% 67.33/9.12 ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ Z ) ) | ( R @ X @ Z ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.12 ( ( tc @ R @ X @ Y ) <=>
% 67.33/9.12 ( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 67.33/9.12 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ X @ Y ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o ),Flatten_var_0:$i,Flatten_var_1:$i]:
% 67.33/9.12 ( ( trc @ R @ Flatten_var_0 @ Flatten_var_1 ) <=>
% 67.33/9.12 ( ( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 67.33/9.12 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Flatten_var_0 @ Flatten_var_1 ) ) ) |
% 67.33/9.12 ( ( Flatten_var_0 ) = ( Flatten_var_1 ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o ),Flatten_var_0:$i,Flatten_var_1:$i]:
% 67.33/9.12 ( ( trsc @ R @ Flatten_var_0 @ Flatten_var_1 ) <=>
% 67.33/9.12 ( ( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 67.33/9.12 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Flatten_var_0 @ Flatten_var_1 ) ) ) |
% 67.33/9.12 ( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 67.33/9.12 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Flatten_var_1 @ Flatten_var_0 ) ) ) |
% 67.33/9.12 ( ( Flatten_var_0 ) = ( Flatten_var_1 ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( po @ R ) <=>
% 67.33/9.12 ( ( ![X:$i,Y:$i,Z:$i]:
% 67.33/9.12 ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ Z ) ) | ( R @ X @ Z ) ) ) &
% 67.33/9.12 ( ![X:$i,Y:$i]:
% 67.33/9.12 ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ X ) ) | ( ( X ) = ( Y ) ) ) ) &
% 67.33/9.12 ( ![X:$i]: ( R @ X @ X ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( so @ R ) <=>
% 67.33/9.12 ( ( ![X:$i,Y:$i,Z:$i]:
% 67.33/9.12 ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ Z ) ) | ( R @ X @ Z ) ) ) &
% 67.33/9.12 ( ![X:$i,Y:$i]: ( ( ~( R @ X @ Y ) ) | ( ~( R @ Y @ X ) ) ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( total @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i]: ( ( ( X ) = ( Y ) ) | ( R @ X @ Y ) | ( R @ Y @ X ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( term @ R ) <=>
% 67.33/9.12 ( ![A:( $i > $o ),Bound_variable_862:$i]:
% 67.33/9.12 ( ( ~( A @ Bound_variable_862 ) ) |
% 67.33/9.12 ( ~( ![X:$i]:
% 67.33/9.12 ( ( ~( A @ X ) ) |
% 67.33/9.12 ( ~( ![Y:$i]: ( ( ~( A @ Y ) ) | ( ~( R @ X @ Y ) ) ) ) ) ) ) ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( ind @ R ) <=>
% 67.33/9.12 ( ![P:( $i > $o ),Bound_variable_917:$i]:
% 67.33/9.12 ( ( ~( ![X:$i]:
% 67.33/9.12 ( ( ~( ![Y:$i]:
% 67.33/9.12 ( ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,
% 67.33/9.12 Bound_variable_674:$i,Z:$i]:
% 67.33/9.12 ( ( ~( S @
% 67.33/9.12 Bound_variable_672 @
% 67.33/9.12 Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,
% 67.33/9.12 Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @
% 67.33/9.12 Bound_variable_661 @
% 67.33/9.12 Bound_variable_663 ) ) |
% 67.33/9.12 ( S @
% 67.33/9.12 Bound_variable_661 @
% 67.33/9.12 Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ X @ Y ) ) ) ) |
% 67.33/9.12 ( P @ Y ) ) ) ) |
% 67.33/9.12 ( P @ X ) ) ) ) |
% 67.33/9.12 ( P @ Bound_variable_917 ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o ),X:$i]:
% 67.33/9.12 ( ( innf @ R @ X ) <=> ( ![Y:$i]: ( ~( R @ X @ Y ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.12 ( ( nfof @ R @ X @ Y ) <=>
% 67.33/9.12 ( ( ![Bound_variable_985:$i]: ( ~( R @ X @ Bound_variable_985 ) ) ) &
% 67.33/9.12 ( ( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 67.33/9.12 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Y @ X ) ) ) |
% 67.33/9.12 ( ( X ) = ( Y ) ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( norm @ R ) <=>
% 67.33/9.12 ( ![X:$i,Bound_variable_1075:$i]:
% 67.33/9.12 ( ( ~( R @ X @ Bound_variable_1075 ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_1049:$i]:
% 67.33/9.12 ( ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Z:$i]:
% 67.33/9.12 ( ( ~( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ X @ Bound_variable_1049 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_985:$i]:
% 67.33/9.12 ( ~( R @ Bound_variable_1049 @ Bound_variable_985 ) ) ) ) ) ) ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.12 ( ( join @ R @ X @ Y ) <=>
% 67.33/9.12 ( ~( ( ![Bound_variable_1218:$i]:
% 67.33/9.12 ( ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( ( ~( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Y @ Bound_variable_1218 ) ) ) ) |
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( ( ~( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ X @ Bound_variable_1218 ) ) ) ) ) ) &
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Bound_variable_1106 ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ X @ Y ) ) ) ) &
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Bound_variable_1125 ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Y @ X ) ) ) ) &
% 67.33/9.12 ( ( X ) != ( Y ) ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( lconfl @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i,Z:$i,Bound_variable_1293:( $i > $i > $o ),
% 67.33/9.12 Bound_variable_1309:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( R @ X @ Z ) ) | ( ~( R @ X @ Y ) ) | ( ( Y ) = ( Z ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_1218:$i]:
% 67.33/9.12 ( ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( ( ~( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 67.33/9.12 ( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Y @ Bound_variable_1218 ) ) ) ) |
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( ( ~( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 67.33/9.12 ( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Z @ Bound_variable_1218 ) ) ) ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( ( ~( Bound_variable_1293 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( Bound_variable_1293 @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 67.33/9.12 ( Bound_variable_1293 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( Bound_variable_1293 @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( Bound_variable_1293 @ Y @ Z ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( ( ~( Bound_variable_1309 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( Bound_variable_1309 @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 67.33/9.12 ( Bound_variable_1309 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( Bound_variable_1309 @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( Bound_variable_1309 @ Z @ Y ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( sconfl @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i,Z:$i,Bound_variable_1371:( $i > $i > $o ),
% 67.33/9.12 Bound_variable_1387:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( R @ X @ Z ) ) |
% 67.33/9.12 ( ( ( X ) != ( Y ) ) &
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1347:$i]:
% 67.33/9.12 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Bound_variable_1347 ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Bound_variable_1347 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ X @ Y ) ) ) ) ) |
% 67.33/9.12 ( ( Y ) = ( Z ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_1218:$i]:
% 67.33/9.12 ( ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( ( ~( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 67.33/9.12 ( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Y @ Bound_variable_1218 ) ) ) ) |
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( ( ~( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 67.33/9.12 ( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Z @ Bound_variable_1218 ) ) ) ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( ( ~( Bound_variable_1371 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( Bound_variable_1371 @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 67.33/9.12 ( Bound_variable_1371 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( Bound_variable_1371 @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( Bound_variable_1371 @ Y @ Z ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( ( ~( Bound_variable_1387 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( Bound_variable_1387 @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 67.33/9.12 ( Bound_variable_1387 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( Bound_variable_1387 @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( Bound_variable_1387 @ Z @ Y ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( confl @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i,Z:$i,Bound_variable_1444:( $i > $i > $o ),
% 67.33/9.12 Bound_variable_1460:( $i > $i > $o )]:
% 67.33/9.12 ( ( ( ( X ) != ( Z ) ) &
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Bound_variable_1106 ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ X @ Z ) ) ) ) ) |
% 67.33/9.12 ( ( ( X ) != ( Y ) ) &
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1422:$i]:
% 67.33/9.12 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Bound_variable_1422 ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Bound_variable_1422 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ X @ Y ) ) ) ) ) |
% 67.33/9.12 ( ( Y ) = ( Z ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_1218:$i]:
% 67.33/9.12 ( ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( ( ~( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 67.33/9.12 ( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Y @ Bound_variable_1218 ) ) ) ) |
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( ( ~( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 67.33/9.12 ( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Z @ Bound_variable_1218 ) ) ) ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( ( ~( Bound_variable_1444 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( Bound_variable_1444 @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 67.33/9.12 ( Bound_variable_1444 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( Bound_variable_1444 @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( Bound_variable_1444 @ Y @ Z ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( ( ~( Bound_variable_1460 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( Bound_variable_1460 @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 67.33/9.12 ( Bound_variable_1460 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( Bound_variable_1460 @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( Bound_variable_1460 @ Z @ Y ) ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( cr @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i,Bound_variable_1522:( $i > $i > $o ),
% 67.33/9.12 Bound_variable_1538:( $i > $i > $o )]:
% 67.33/9.12 ( ( ( ( X ) != ( Y ) ) &
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 67.33/9.12 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Y @ X ) ) ) ) &
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 67.33/9.12 ( ( ~( S @ Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @ Bound_variable_674 @ Z ) ) |
% 67.33/9.12 ( S @ Bound_variable_672 @ Z ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ X @ Y ) ) ) ) ) |
% 67.33/9.12 ( ( X ) = ( Y ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_1218:$i]:
% 67.33/9.12 ( ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( ( ~( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 67.33/9.12 ( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ Y @ Bound_variable_1218 ) ) ) ) |
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( ( ~( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( S @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 67.33/9.12 ( S @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( S @ Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( S @ X @ Bound_variable_1218 ) ) ) ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( ( ~( Bound_variable_1522 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( Bound_variable_1522 @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1125 ) ) |
% 67.33/9.12 ( Bound_variable_1522 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1125 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( Bound_variable_1522 @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( Bound_variable_1522 @ Y @ X ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( ( ~( Bound_variable_1538 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_674 ) ) |
% 67.33/9.12 ( ~( Bound_variable_1538 @
% 67.33/9.12 Bound_variable_674 @ Bound_variable_1106 ) ) |
% 67.33/9.12 ( Bound_variable_1538 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1106 ) ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( ( ~( R @ Bound_variable_661 @ Bound_variable_663 ) ) |
% 67.33/9.12 ( Bound_variable_1538 @
% 67.33/9.12 Bound_variable_661 @ Bound_variable_663 ) ) ) ) |
% 67.33/9.12 ( Bound_variable_1538 @ X @ Y ) ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_0, type, zip_tseitin_32 :
% 67.33/9.12 ( $i > $i > $o ) > ( $i > $i > $o ) > $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_1, axiom,
% 67.33/9.12 (![Bound_variable_1538:( $i > $i > $o ),
% 67.33/9.12 Bound_variable_1522:( $i > $i > $o ),Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_32 @ Bound_variable_1538 @ Bound_variable_1522 @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( Bound_variable_1538 @ X @ Y ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( zip_tseitin_0 @
% 67.33/9.12 Bound_variable_663 @ Bound_variable_661 @
% 67.33/9.12 Bound_variable_1538 @ R ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( zip_tseitin_8 @
% 67.33/9.12 Bound_variable_1106 @ Bound_variable_674 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1538 ) ) ) |
% 67.33/9.12 ( Bound_variable_1522 @ Y @ X ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( zip_tseitin_0 @
% 67.33/9.12 Bound_variable_663 @ Bound_variable_661 @
% 67.33/9.12 Bound_variable_1522 @ R ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( zip_tseitin_8 @
% 67.33/9.12 Bound_variable_1125 @ Bound_variable_674 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1522 ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_1218:$i]:
% 67.33/9.12 ( zip_tseitin_25 @ Bound_variable_1218 @ Y @ X @ R ) ) ) |
% 67.33/9.12 ( ( X ) = ( Y ) ) | ( zip_tseitin_31 @ Y @ X @ R ) ) ))).
% 67.33/9.12 thf(zf_stmt_2, type, zip_tseitin_31 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_3, axiom,
% 67.33/9.12 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_31 @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( ~( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ Y @ X @ R ) ) ) &
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ X @ Y @ R ) ) ) &
% 67.33/9.12 ( ( X ) != ( Y ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_4, type, zip_tseitin_30 :
% 67.33/9.12 ( $i > $i > $o ) > ( $i > $i > $o ) > $i > $i > $i > ( $i > $i > $o ) >
% 67.33/9.12 $o).
% 67.33/9.12 thf(zf_stmt_5, axiom,
% 67.33/9.12 (![Bound_variable_1460:( $i > $i > $o ),
% 67.33/9.12 Bound_variable_1444:( $i > $i > $o ),Z:$i,Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_30 @
% 67.33/9.12 Bound_variable_1460 @ Bound_variable_1444 @ Z @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( Bound_variable_1460 @ Z @ Y ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( zip_tseitin_0 @
% 67.33/9.12 Bound_variable_663 @ Bound_variable_661 @
% 67.33/9.12 Bound_variable_1460 @ R ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( zip_tseitin_8 @
% 67.33/9.12 Bound_variable_1106 @ Bound_variable_674 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1460 ) ) ) |
% 67.33/9.12 ( Bound_variable_1444 @ Y @ Z ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( zip_tseitin_0 @
% 67.33/9.12 Bound_variable_663 @ Bound_variable_661 @
% 67.33/9.12 Bound_variable_1444 @ R ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( zip_tseitin_8 @
% 67.33/9.12 Bound_variable_1125 @ Bound_variable_674 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1444 ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_1218:$i]:
% 67.33/9.12 ( zip_tseitin_25 @ Bound_variable_1218 @ Y @ Z @ R ) ) ) |
% 67.33/9.12 ( ( Y ) = ( Z ) ) | ( zip_tseitin_28 @ Y @ X @ R ) |
% 67.33/9.12 ( zip_tseitin_28 @ Z @ X @ R ) ) ))).
% 67.33/9.12 thf(zf_stmt_6, type, zip_tseitin_29 :
% 67.33/9.12 ( $i > $i > $o ) > ( $i > $i > $o ) > $i > $i > $i > ( $i > $i > $o ) >
% 67.33/9.12 $o).
% 67.33/9.12 thf(zf_stmt_7, axiom,
% 67.33/9.12 (![Bound_variable_1387:( $i > $i > $o ),
% 67.33/9.12 Bound_variable_1371:( $i > $i > $o ),Z:$i,Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_29 @
% 67.33/9.12 Bound_variable_1387 @ Bound_variable_1371 @ Z @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( Bound_variable_1387 @ Z @ Y ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( zip_tseitin_0 @
% 67.33/9.12 Bound_variable_663 @ Bound_variable_661 @
% 67.33/9.12 Bound_variable_1387 @ R ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( zip_tseitin_8 @
% 67.33/9.12 Bound_variable_1106 @ Bound_variable_674 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1387 ) ) ) |
% 67.33/9.12 ( Bound_variable_1371 @ Y @ Z ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( zip_tseitin_0 @
% 67.33/9.12 Bound_variable_663 @ Bound_variable_661 @
% 67.33/9.12 Bound_variable_1371 @ R ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( zip_tseitin_8 @
% 67.33/9.12 Bound_variable_1125 @ Bound_variable_674 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1371 ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_1218:$i]:
% 67.33/9.12 ( zip_tseitin_25 @ Bound_variable_1218 @ Y @ Z @ R ) ) ) |
% 67.33/9.12 ( ( Y ) = ( Z ) ) | ( zip_tseitin_28 @ Y @ X @ R ) |
% 67.33/9.12 ( ~( R @ X @ Z ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_8, type, zip_tseitin_28 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_9, axiom,
% 67.33/9.12 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_28 @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( ~( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ Y @ X @ R ) ) ) &
% 67.33/9.12 ( ( X ) != ( Y ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_10, type, zip_tseitin_27 :
% 67.33/9.12 ( $i > $i > $o ) > ( $i > $i > $o ) > $i > $i > $i > ( $i > $i > $o ) >
% 67.33/9.12 $o).
% 67.33/9.12 thf(zf_stmt_11, axiom,
% 67.33/9.12 (![Bound_variable_1309:( $i > $i > $o ),
% 67.33/9.12 Bound_variable_1293:( $i > $i > $o ),Z:$i,Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_27 @
% 67.33/9.12 Bound_variable_1309 @ Bound_variable_1293 @ Z @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( Bound_variable_1309 @ Z @ Y ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( zip_tseitin_0 @
% 67.33/9.12 Bound_variable_663 @ Bound_variable_661 @
% 67.33/9.12 Bound_variable_1309 @ R ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1106:$i]:
% 67.33/9.12 ( zip_tseitin_8 @
% 67.33/9.12 Bound_variable_1106 @ Bound_variable_674 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1309 ) ) ) |
% 67.33/9.12 ( Bound_variable_1293 @ Y @ Z ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( zip_tseitin_0 @
% 67.33/9.12 Bound_variable_663 @ Bound_variable_661 @
% 67.33/9.12 Bound_variable_1293 @ R ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,
% 67.33/9.12 Bound_variable_1125:$i]:
% 67.33/9.12 ( zip_tseitin_8 @
% 67.33/9.12 Bound_variable_1125 @ Bound_variable_674 @
% 67.33/9.12 Bound_variable_672 @ Bound_variable_1293 ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_1218:$i]:
% 67.33/9.12 ( zip_tseitin_25 @ Bound_variable_1218 @ Y @ Z @ R ) ) ) |
% 67.33/9.12 ( ( Y ) = ( Z ) ) | ( ~( R @ X @ Y ) ) | ( ~( R @ X @ Z ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_12, type, zip_tseitin_26 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_13, axiom,
% 67.33/9.12 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_26 @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( ( X ) != ( Y ) ) &
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ X @ Y @ R ) ) ) &
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ Y @ X @ R ) ) ) &
% 67.33/9.12 ( ![Bound_variable_1218:$i]:
% 67.33/9.12 ( zip_tseitin_25 @ Bound_variable_1218 @ Y @ X @ R ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_14, type, zip_tseitin_25 : $i > $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_15, axiom,
% 67.33/9.12 (![Bound_variable_1218:$i,Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_25 @ Bound_variable_1218 @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( zip_tseitin_9 @ S @ Bound_variable_1218 @ X @ R ) ) ) |
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( zip_tseitin_9 @ S @ Bound_variable_1218 @ Y @ R ) ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_16, type, zip_tseitin_24 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_17, axiom,
% 67.33/9.12 (![Bound_variable_1075:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_24 @ Bound_variable_1075 @ X @ R ) <=>
% 67.33/9.12 ( ( ~( ![Bound_variable_1049:$i]:
% 67.33/9.12 ( zip_tseitin_23 @ Bound_variable_1049 @ X @ R ) ) ) |
% 67.33/9.12 ( ~( R @ X @ Bound_variable_1075 ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_18, type, zip_tseitin_23 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_19, axiom,
% 67.33/9.12 (![Bound_variable_1049:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_23 @ Bound_variable_1049 @ X @ R ) <=>
% 67.33/9.12 ( ( ~( ![Bound_variable_985:$i]:
% 67.33/9.12 ( ~( R @ Bound_variable_1049 @ Bound_variable_985 ) ) ) ) |
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( zip_tseitin_9 @ S @ Bound_variable_1049 @ X @ R ) ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_20, type, zip_tseitin_22 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_21, axiom,
% 67.33/9.12 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_22 @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( zip_tseitin_21 @ Y @ X @ R ) &
% 67.33/9.12 ( ![Bound_variable_985:$i]: ( ~( R @ X @ Bound_variable_985 ) ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_22, type, zip_tseitin_21 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_23, axiom,
% 67.33/9.12 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_21 @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( ( X ) = ( Y ) ) |
% 67.33/9.12 ( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ X @ Y @ R ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_24, type, zip_tseitin_20 :
% 67.33/9.12 $i > ( $i > $o ) > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_25, axiom,
% 67.33/9.12 (![Bound_variable_917:$i,P:( $i > $o ),R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_20 @ Bound_variable_917 @ P @ R ) <=>
% 67.33/9.12 ( ( P @ Bound_variable_917 ) |
% 67.33/9.12 ( ~( ![X:$i]: ( zip_tseitin_19 @ X @ P @ R ) ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_26, type, zip_tseitin_19 :
% 67.33/9.12 $i > ( $i > $o ) > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_27, axiom,
% 67.33/9.12 (![X:$i,P:( $i > $o ),R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_19 @ X @ P @ R ) <=>
% 67.33/9.12 ( ( P @ X ) | ( ~( ![Y:$i]: ( zip_tseitin_18 @ Y @ X @ P @ R ) ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_28, type, zip_tseitin_18 :
% 67.33/9.12 $i > $i > ( $i > $o ) > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_29, axiom,
% 67.33/9.12 (![Y:$i,X:$i,P:( $i > $o ),R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_18 @ Y @ X @ P @ R ) <=>
% 67.33/9.12 ( ( P @ Y ) |
% 67.33/9.12 ( ~( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ Y @ X @ R ) ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_30, type, zip_tseitin_17 :
% 67.33/9.12 $i > ( $i > $o ) > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_31, axiom,
% 67.33/9.12 (![Bound_variable_862:$i,A:( $i > $o ),R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_17 @ Bound_variable_862 @ A @ R ) <=>
% 67.33/9.12 ( ( ~( ![X:$i]: ( zip_tseitin_16 @ X @ A @ R ) ) ) |
% 67.33/9.12 ( ~( A @ Bound_variable_862 ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_32, type, zip_tseitin_16 :
% 67.33/9.12 $i > ( $i > $o ) > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_33, axiom,
% 67.33/9.12 (![X:$i,A:( $i > $o ),R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_16 @ X @ A @ R ) <=>
% 67.33/9.12 ( ( ~( ![Y:$i]: ( zip_tseitin_15 @ Y @ X @ A @ R ) ) ) | ( ~( A @ X ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_34, type, zip_tseitin_15 :
% 67.33/9.12 $i > $i > ( $i > $o ) > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_35, axiom,
% 67.33/9.12 (![Y:$i,X:$i,A:( $i > $o ),R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_15 @ Y @ X @ A @ R ) <=>
% 67.33/9.12 ( ( ~( R @ X @ Y ) ) | ( ~( A @ Y ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_36, type, zip_tseitin_14 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_37, axiom,
% 67.33/9.12 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_14 @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( R @ Y @ X ) | ( R @ X @ Y ) | ( ( X ) = ( Y ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_38, type, zip_tseitin_13 : ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_39, axiom,
% 67.33/9.12 (![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_13 @ R ) <=>
% 67.33/9.12 ( ( ![X:$i,Y:$i]: ( zip_tseitin_6 @ Y @ X @ R ) ) &
% 67.33/9.12 ( ![X:$i,Y:$i,Z:$i]: ( zip_tseitin_8 @ Z @ Y @ X @ R ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_40, type, zip_tseitin_12 : ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_41, axiom,
% 67.33/9.12 (![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_12 @ R ) <=>
% 67.33/9.12 ( ( ![X:$i]: ( R @ X @ X ) ) &
% 67.33/9.12 ( ![X:$i,Y:$i]: ( zip_tseitin_5 @ Y @ X @ R ) ) &
% 67.33/9.12 ( ![X:$i,Y:$i,Z:$i]: ( zip_tseitin_8 @ Z @ Y @ X @ R ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_42, type, zip_tseitin_11 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_43, axiom,
% 67.33/9.12 (![Flatten_var_1:$i,Flatten_var_0:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_11 @ Flatten_var_1 @ Flatten_var_0 @ R ) <=>
% 67.33/9.12 ( ( ( Flatten_var_0 ) = ( Flatten_var_1 ) ) |
% 67.33/9.12 ( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( zip_tseitin_9 @ S @ Flatten_var_0 @ Flatten_var_1 @ R ) ) |
% 67.33/9.12 ( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( zip_tseitin_9 @ S @ Flatten_var_1 @ Flatten_var_0 @ R ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_44, type, zip_tseitin_10 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_45, axiom,
% 67.33/9.12 (![Flatten_var_1:$i,Flatten_var_0:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_10 @ Flatten_var_1 @ Flatten_var_0 @ R ) <=>
% 67.33/9.12 ( ( ( Flatten_var_0 ) = ( Flatten_var_1 ) ) |
% 67.33/9.12 ( ![S:( $i > $i > $o )]:
% 67.33/9.12 ( zip_tseitin_9 @ S @ Flatten_var_1 @ Flatten_var_0 @ R ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_46, type, zip_tseitin_9 :
% 67.33/9.12 ( $i > $i > $o ) > $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_47, axiom,
% 67.33/9.12 (![S:( $i > $i > $o ),Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_9 @ S @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( S @ X @ Y ) |
% 67.33/9.12 ( ~( ![Bound_variable_661:$i,Bound_variable_663:$i]:
% 67.33/9.12 ( zip_tseitin_0 @ Bound_variable_663 @ Bound_variable_661 @ S @ R ) ) ) |
% 67.33/9.12 ( ~( ![Bound_variable_672:$i,Bound_variable_674:$i,Z:$i]:
% 67.33/9.12 ( zip_tseitin_8 @ Z @ Bound_variable_674 @ Bound_variable_672 @ S ) ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_48, type, zip_tseitin_8 : $i > $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_49, axiom,
% 67.33/9.12 (![Z:$i,Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_8 @ Z @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( R @ X @ Z ) | ( ~( R @ Y @ Z ) ) | ( ~( R @ X @ Y ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_50, type, zip_tseitin_7 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_51, axiom,
% 67.33/9.12 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_7 @ Y @ X @ R ) <=> ( ( R @ Y @ X ) | ( R @ X @ Y ) ) ))).
% 67.33/9.12 thf(zf_stmt_52, type, zip_tseitin_6 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_53, axiom,
% 67.33/9.12 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_6 @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( ~( R @ Y @ X ) ) | ( ~( R @ X @ Y ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_54, type, zip_tseitin_5 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_55, axiom,
% 67.33/9.12 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_5 @ Y @ X @ R ) <=>
% 67.33/9.12 ( ( ( X ) = ( Y ) ) | ( ~( R @ Y @ X ) ) | ( ~( R @ X @ Y ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_56, type, zip_tseitin_4 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_57, axiom,
% 67.33/9.12 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_4 @ Y @ X @ R ) <=> ( ( R @ Y @ X ) | ( ~( R @ X @ Y ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_58, type, zip_tseitin_3 : $i > $i > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_59, axiom,
% 67.33/9.12 (![Y:$i,X:$i,R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_3 @ Y @ X @ R ) <=> ( ( ( X ) = ( Y ) ) | ( R @ X @ Y ) ) ))).
% 67.33/9.12 thf(zf_stmt_60, type, zip_tseitin_2 :
% 67.33/9.12 $i > $i > ( $i > $i > $o ) > ( $i > $i > $o ) >
% 67.33/9.12 ( ( $i > $i > $o ) > $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_61, axiom,
% 67.33/9.12 (![Bound_variable_512:$i,Bound_variable_510:$i,S:( $i > $i > $o ),
% 67.33/9.12 R:( $i > $i > $o ),F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_2 @ Bound_variable_512 @ Bound_variable_510 @ S @ R @ F ) <=>
% 67.33/9.12 ( ( F @ S @ Bound_variable_510 @ Bound_variable_512 ) |
% 67.33/9.12 ( ~( F @ R @ Bound_variable_510 @ Bound_variable_512 ) ) |
% 67.33/9.12 ( ~( ![X:$i,Y:$i]: ( zip_tseitin_0 @ Y @ X @ S @ R ) ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_62, type, zip_tseitin_1 :
% 67.33/9.12 $i > $i > ( $i > $i > $o ) > ( ( $i > $i > $o ) > $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_63, axiom,
% 67.33/9.12 (![Y:$i,X:$i,R:( $i > $i > $o ),F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_1 @ Y @ X @ R @ F ) <=>
% 67.33/9.12 ( ( F @ R @ X @ Y ) | ( ~( R @ X @ Y ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_64, type, zip_tseitin_0 :
% 67.33/9.12 $i > $i > ( $i > $i > $o ) > ( $i > $i > $o ) > $o).
% 67.33/9.12 thf(zf_stmt_65, axiom,
% 67.33/9.12 (![Y:$i,X:$i,S:( $i > $i > $o ),R:( $i > $i > $o )]:
% 67.33/9.12 ( ( zip_tseitin_0 @ Y @ X @ S @ R ) <=>
% 67.33/9.12 ( ( S @ X @ Y ) | ( ~( R @ X @ Y ) ) ) ))).
% 67.33/9.12 thf(zf_stmt_66, axiom,
% 67.33/9.12 (( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( cr @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i,Bound_variable_1522:( $i > $i > $o ),
% 67.33/9.12 Bound_variable_1538:( $i > $i > $o )]:
% 67.33/9.12 ( zip_tseitin_32 @
% 67.33/9.12 Bound_variable_1538 @ Bound_variable_1522 @ Y @ X @ R ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( confl @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i,Z:$i,Bound_variable_1444:( $i > $i > $o ),
% 67.33/9.12 Bound_variable_1460:( $i > $i > $o )]:
% 67.33/9.12 ( zip_tseitin_30 @
% 67.33/9.12 Bound_variable_1460 @ Bound_variable_1444 @ Z @ Y @ X @ R ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( sconfl @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i,Z:$i,Bound_variable_1371:( $i > $i > $o ),
% 67.33/9.12 Bound_variable_1387:( $i > $i > $o )]:
% 67.33/9.12 ( zip_tseitin_29 @
% 67.33/9.12 Bound_variable_1387 @ Bound_variable_1371 @ Z @ Y @ X @ R ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.12 ( ( lconfl @ R ) <=>
% 67.33/9.12 ( ![X:$i,Y:$i,Z:$i,Bound_variable_1293:( $i > $i > $o ),
% 67.33/9.12 Bound_variable_1309:( $i > $i > $o )]:
% 67.33/9.12 ( zip_tseitin_27 @
% 67.33/9.12 Bound_variable_1309 @ Bound_variable_1293 @ Z @ Y @ X @ R ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.12 ( ( join @ R @ X @ Y ) <=> ( ~( zip_tseitin_26 @ Y @ X @ R ) ) ) ) &
% 67.33/9.12 ( ![R:( $i > $i > $o )]:
% 67.33/9.13 ( ( norm @ R ) <=>
% 67.33/9.13 ( ![X:$i,Bound_variable_1075:$i]:
% 67.33/9.13 ( zip_tseitin_24 @ Bound_variable_1075 @ X @ R ) ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.13 ( ( nfof @ R @ X @ Y ) <=> ( zip_tseitin_22 @ Y @ X @ R ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o ),X:$i]:
% 67.33/9.13 ( ( innf @ R @ X ) <=> ( ![Y:$i]: ( ~( R @ X @ Y ) ) ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o )]:
% 67.33/9.13 ( ( ind @ R ) <=>
% 67.33/9.13 ( ![P:( $i > $o ),Bound_variable_917:$i]:
% 67.33/9.13 ( zip_tseitin_20 @ Bound_variable_917 @ P @ R ) ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o )]:
% 67.33/9.13 ( ( term @ R ) <=>
% 67.33/9.13 ( ![A:( $i > $o ),Bound_variable_862:$i]:
% 67.33/9.13 ( zip_tseitin_17 @ Bound_variable_862 @ A @ R ) ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o )]:
% 67.33/9.13 ( ( total @ R ) <=> ( ![X:$i,Y:$i]: ( zip_tseitin_14 @ Y @ X @ R ) ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o )]: ( ( so @ R ) <=> ( zip_tseitin_13 @ R ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o )]: ( ( po @ R ) <=> ( zip_tseitin_12 @ R ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o ),Flatten_var_0:$i,Flatten_var_1:$i]:
% 67.33/9.13 ( ( trsc @ R @ Flatten_var_0 @ Flatten_var_1 ) <=>
% 67.33/9.13 ( zip_tseitin_11 @ Flatten_var_1 @ Flatten_var_0 @ R ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o ),Flatten_var_0:$i,Flatten_var_1:$i]:
% 67.33/9.13 ( ( trc @ R @ Flatten_var_0 @ Flatten_var_1 ) <=>
% 67.33/9.13 ( zip_tseitin_10 @ Flatten_var_1 @ Flatten_var_0 @ R ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.13 ( ( tc @ R @ X @ Y ) <=>
% 67.33/9.13 ( ![S:( $i > $i > $o )]: ( zip_tseitin_9 @ S @ Y @ X @ R ) ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o )]:
% 67.33/9.13 ( ( trans @ R ) <=>
% 67.33/9.13 ( ![X:$i,Y:$i,Z:$i]: ( zip_tseitin_8 @ Z @ Y @ X @ R ) ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.13 ( ( sc @ R @ X @ Y ) <=> ( zip_tseitin_7 @ Y @ X @ R ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o )]:
% 67.33/9.13 ( ( asymm @ R ) <=> ( ![X:$i,Y:$i]: ( zip_tseitin_6 @ Y @ X @ R ) ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o )]:
% 67.33/9.13 ( ( antisymm @ R ) <=> ( ![X:$i,Y:$i]: ( zip_tseitin_5 @ Y @ X @ R ) ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o )]:
% 67.33/9.13 ( ( symm @ R ) <=> ( ![X:$i,Y:$i]: ( zip_tseitin_4 @ Y @ X @ R ) ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.13 ( ( rc @ R @ X @ Y ) <=> ( zip_tseitin_3 @ Y @ X @ R ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o )]:
% 67.33/9.13 ( ( irrefl @ R ) <=> ( ![X:$i]: ( ~( R @ X @ X ) ) ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o )]: ( ( refl @ R ) <=> ( ![X:$i]: ( R @ X @ X ) ) ) ) &
% 67.33/9.13 ( ![F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 67.33/9.13 ( ( mono @ F ) <=>
% 67.33/9.13 ( ![R:( $i > $i > $o ),S:( $i > $i > $o ),Bound_variable_510:$i,
% 67.33/9.13 Bound_variable_512:$i]:
% 67.33/9.13 ( zip_tseitin_2 @
% 67.33/9.13 Bound_variable_512 @ Bound_variable_510 @ S @ R @ F ) ) ) ) &
% 67.33/9.13 ( ![F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 67.33/9.13 ( ( infl @ F ) <=>
% 67.33/9.13 ( ![R:( $i > $i > $o ),X:$i,Y:$i]: ( zip_tseitin_1 @ Y @ X @ R @ F ) ) ) ) &
% 67.33/9.13 ( ![F:( ( $i > $i > $o ) > $i > $i > $o )]:
% 67.33/9.13 ( ( idem @ F ) <=>
% 67.33/9.13 ( ![R:( $i > $i > $o )]: ( ( F @ R ) = ( F @ ( F @ R ) ) ) ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o ),X:$i,Y:$i]:
% 67.33/9.13 ( ( inv @ R @ X @ Y ) <=> ( R @ Y @ X ) ) ) &
% 67.33/9.13 ( ![R:( $i > $i > $o ),S:( $i > $i > $o )]:
% 67.33/9.13 ( ( subrel @ R @ S ) <=>
% 67.33/9.13 ( ![X:$i,Y:$i]: ( zip_tseitin_0 @ Y @ X @ S @ R ) ) ) ) &
% 67.33/9.13 ( ![DU1:d_unsorted,DU2:d_unsorted]:
% 67.33/9.13 ( ( ( d2unsorted @ DU1 ) = ( d2unsorted @ DU2 ) ) =>
% 67.33/9.13 ( ( DU1 ) = ( DU2 ) ) ) ) &
% 67.33/9.13 ( ![DU:d_unsorted]: ( ( DU ) = ( d_unsorted_0 ) ) ) &
% 67.33/9.13 ( ![U:$i]: ( ?[DU:d_unsorted]: ( ( U ) = ( d2unsorted @ DU ) ) ) ))).
% 67.33/9.13 thf(zip_derived_cl191, plain,
% 67.33/9.13 (![X0 : $i > $i > $o, X1 : $i, X2 : $i]:
% 67.33/9.13 ( (join @ X0 @ X1 @ X2) | (zip_tseitin_26 @ X2 @ X1 @ X0))),
% 67.33/9.13 inference('cnf', [status(esa)], [zf_stmt_66])).
% 67.33/9.13 thf(zip_derived_cl85, plain,
% 67.33/9.13 (![X0 : $i, X1 : $i, X2 : $i > $i > $o]:
% 67.33/9.13 (((X1) != (X0)) | ~ (zip_tseitin_26 @ X0 @ X1 @ X2))),
% 67.33/9.13 inference('cnf', [status(esa)], [zf_stmt_13])).
% 67.33/9.13 thf(locally_confluent, conjecture,
% 67.33/9.13 (![R:( $i > $i > $o )]:
% 67.33/9.13 ( ( lconfl @ R ) <=>
% 67.33/9.13 ( ![X:$i,Y:$i,Z:$i]:
% 67.33/9.13 ( ( ( R @ X @ Z ) & ( R @ X @ Y ) ) => ( join @ R @ Z @ Y ) ) ) ))).
% 67.33/9.13 thf(zf_stmt_67, negated_conjecture,
% 67.33/9.13 (~( ![R:( $i > $i > $o )]:
% 67.33/9.13 ( ( lconfl @ R ) <=>
% 67.33/9.13 ( ![X:$i,Y:$i,Z:$i]:
% 67.33/9.13 ( ( ( R @ X @ Z ) & ( R @ X @ Y ) ) => ( join @ R @ Z @ Y ) ) ) ) )),
% 67.33/9.13 inference('cnf.neg', [status(esa)], [locally_confluent])).
% 67.33/9.13 thf(zip_derived_cl204, plain,
% 67.33/9.13 ((~ (join @ sk__134 @ sk__137 @ sk__136) | ~ (lconfl @ sk__134))),
% 67.33/9.13 inference('cnf', [status(esa)], [zf_stmt_67])).
% 67.33/9.13 thf(zip_derived_cl98, plain,
% 67.33/9.13 (![X0 : $i > $i > $o, X1 : $i > $i > $o, X2 : $i, X3 : $i, X4 : $i,
% 67.33/9.13 X5 : $i > $i > $o]:
% 67.33/9.13 ( (zip_tseitin_27 @ X0 @ X1 @ X2 @ X3 @ X4 @ X5) | ((X3) != (X2)))),
% 67.33/9.13 inference('cnf', [status(esa)], [zf_stmt_11])).
% 67.33/9.13 thf(zip_derived_cl193, plain,
% 67.33/9.13 (![X0 : $i > $i > $o]:
% 67.33/9.13 ( (lconfl @ X0)
% 67.33/9.13 | ~ (zip_tseitin_27 @ (sk__101 @ X0) @ (sk__100 @ X0) @
% 67.33/9.13 (sk__99 @ X0) @ (sk__98 @ X0) @ (sk__97 @ X0) @ X0))),
% 67.33/9.13 inference('cnf', [status(esa)], [zf_stmt_66])).
% 67.33/9.13 thf(zip_derived_cl140, plain,
% 67.33/9.13 (![X0 : $i]: ((X0) = (d2unsorted @ (sk__133 @ X0)))),
% 67.33/9.13 inference('cnf', [status(esa)], [zf_stmt_66])).
% 67.33/9.13 thf(zip_derived_cl141, plain, (![X0 : d_unsorted]: ((X0) = (d_unsorted_0))),
% 67.33/9.13 inference('cnf', [status(esa)], [zf_stmt_66])).
% 67.33/9.13 thf(zip_derived_cl209, plain,
% 67.33/9.13 (![X0 : $i]: ((X0) = (d2unsorted @ d_unsorted_0))),
% 67.33/9.13 inference('demod', [status(thm)], [zip_derived_cl140, zip_derived_cl141])).
% 67.33/9.13 thf(zip_derived_cl209, plain,
% 67.33/9.13 (![X0 : $i]: ((X0) = (d2unsorted @ d_unsorted_0))),
% 67.33/9.13 inference('demod', [status(thm)], [zip_derived_cl140, zip_derived_cl141])).
% 67.33/9.13 thf(zip_derived_cl210, plain,
% 67.33/9.13 (![X0 : $i]: ((X0) = (d2unsorted @ d_unsorted_0))),
% 67.33/9.13 inference('sup+', [status(thm)], [zip_derived_cl209, zip_derived_cl209])).
% 67.33/9.13 thf(zip_derived_cl141, plain, (![X0 : d_unsorted]: ((X0) = (d_unsorted_0))),
% 67.33/9.13 inference('cnf', [status(esa)], [zf_stmt_66])).
% 67.33/9.13 thf(zip_derived_cl209, plain,
% 67.33/9.13 (![X0 : $i]: ((X0) = (d2unsorted @ d_unsorted_0))),
% 67.33/9.13 inference('demod', [status(thm)], [zip_derived_cl140, zip_derived_cl141])).
% 67.33/9.13 thf(zip_derived_cl213, plain,
% 67.33/9.13 (![X0 : $i]: ((X0) = (d2unsorted @ d_unsorted_0))),
% 67.33/9.13 inference('sup+', [status(thm)], [zip_derived_cl141, zip_derived_cl209])).
% 67.33/9.13 thf(zip_derived_cl6917, plain, ($false),
% 67.33/9.13 inference('eprover', [status(thm)],
% 67.33/9.13 [zip_derived_cl191, zip_derived_cl85, zip_derived_cl204,
% 67.33/9.13 zip_derived_cl98, zip_derived_cl193, zip_derived_cl210,
% 67.33/9.13 zip_derived_cl213])).
% 67.33/9.13
% 67.33/9.13 % SZS output end Refutation
% 67.33/9.13
% 67.33/9.13
% 67.33/9.13 % Terminating...
% 68.62/9.27 % Runner terminated.
% 68.62/9.28 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------