%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : PUZ075+1 : TPTP v9.2.0. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.H0SYIol2lS true
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 04:49:38 PM UTC 2025
% Result : Theorem 0.49s 0.99s
% Output : Refutation 0.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : PUZ075+1 : TPTP v9.2.0. Released v3.5.0.
% 0.04/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.H0SYIol2lS true
% 0.12/0.33 % Computer : n011.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 1 15:08:53 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.34 % Running portfolio for 300 s
% 0.12/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.34 % Number of cores: 8
% 0.12/0.34 % Python version: Python 3.6.8
% 0.12/0.34 % Running in FO mode
% 0.46/0.58 % Total configuration time : 435
% 0.46/0.58 % Estimated wc time : 1092
% 0.46/0.58 % Estimated cpu time (7 cpus) : 156.0
% 0.48/0.66 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.48/0.69 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.48/0.70 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.48/0.70 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.48/0.70 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.48/0.70 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.48/0.70 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.49/0.99 % Solved by fo/fo1_av.sh.
% 0.49/0.99 % done 430 iterations in 0.230s
% 0.49/0.99 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.49/0.99 % SZS output start Refutation
% 0.49/0.99 thf(cell3_type, type, cell3: $i).
% 0.49/0.99 thf(zip_tseitin_158_type, type, zip_tseitin_158: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_29_type, type, zip_tseitin_29: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_6_type, type, zip_tseitin_6: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_92_type, type, zip_tseitin_92: $i > $i > $o).
% 0.49/0.99 thf(cell8_type, type, cell8: $i).
% 0.49/0.99 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_150_type, type, zip_tseitin_150: $i > $i > $o).
% 0.49/0.99 thf(cell68_type, type, cell68: $i).
% 0.49/0.99 thf(cell11_type, type, cell11: $i).
% 0.49/0.99 thf(zip_tseitin_133_type, type, zip_tseitin_133: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_39_type, type, zip_tseitin_39: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_50_type, type, zip_tseitin_50: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_147_type, type, zip_tseitin_147: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_108_type, type, zip_tseitin_108: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_80_type, type, zip_tseitin_80: $i > $i > $o).
% 0.49/0.99 thf(cell24_type, type, cell24: $i).
% 0.49/0.99 thf(zip_tseitin_161_type, type, zip_tseitin_161: $i > $i > $o).
% 0.49/0.99 thf(cell80_type, type, cell80: $i).
% 0.49/0.99 thf(cell77_type, type, cell77: $i).
% 0.49/0.99 thf(zip_tseitin_110_type, type, zip_tseitin_110: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_83_type, type, zip_tseitin_83: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_53_type, type, zip_tseitin_53: $i > $i > $o).
% 0.49/0.99 thf(cell65_type, type, cell65: $i).
% 0.49/0.99 thf(zip_tseitin_15_type, type, zip_tseitin_15: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_75_type, type, zip_tseitin_75: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_160_type, type, zip_tseitin_160: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_84_type, type, zip_tseitin_84: $i > $i > $o).
% 0.49/0.99 thf(cell74_type, type, cell74: $i).
% 0.49/0.99 thf(zip_tseitin_94_type, type, zip_tseitin_94: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_122_type, type, zip_tseitin_122: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_38_type, type, zip_tseitin_38: $i > $i > $o).
% 0.49/0.99 thf(cell89_type, type, cell89: $i).
% 0.49/0.99 thf(zip_tseitin_68_type, type, zip_tseitin_68: $i > $i > $o).
% 0.49/0.99 thf(cell92_type, type, cell92: $i).
% 0.49/0.99 thf(zip_tseitin_105_type, type, zip_tseitin_105: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_71_type, type, zip_tseitin_71: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_165_type, type, zip_tseitin_165: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_77_type, type, zip_tseitin_77: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_118_type, type, zip_tseitin_118: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $o).
% 0.49/0.99 thf(cell27_type, type, cell27: $i).
% 0.49/0.99 thf(cell100_type, type, cell100: $i).
% 0.49/0.99 thf(cell51_type, type, cell51: $i).
% 0.49/0.99 thf(cell97_type, type, cell97: $i).
% 0.49/0.99 thf(cell61_type, type, cell61: $i).
% 0.49/0.99 thf(cell37_type, type, cell37: $i).
% 0.49/0.99 thf(zip_tseitin_42_type, type, zip_tseitin_42: $i > $i > $o).
% 0.49/0.99 thf(cell54_type, type, cell54: $i).
% 0.49/0.99 thf(zip_tseitin_128_type, type, zip_tseitin_128: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_95_type, type, zip_tseitin_95: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_45_type, type, zip_tseitin_45: $i > $i > $o).
% 0.49/0.99 thf(cell2_type, type, cell2: $i).
% 0.49/0.99 thf(cell79_type, type, cell79: $i).
% 0.49/0.99 thf(zip_tseitin_163_type, type, zip_tseitin_163: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $i > $o).
% 0.49/0.99 thf(cell66_type, type, cell66: $i).
% 0.49/0.99 thf(cell75_type, type, cell75: $i).
% 0.49/0.99 thf(cell17_type, type, cell17: $i).
% 0.49/0.99 thf(zip_tseitin_78_type, type, zip_tseitin_78: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_106_type, type, zip_tseitin_106: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_33_type, type, zip_tseitin_33: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_138_type, type, zip_tseitin_138: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_37_type, type, zip_tseitin_37: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_132_type, type, zip_tseitin_132: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_27_type, type, zip_tseitin_27: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_101_type, type, zip_tseitin_101: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_131_type, type, zip_tseitin_131: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_141_type, type, zip_tseitin_141: $i > $i > $o).
% 0.49/0.99 thf(cell20_type, type, cell20: $i).
% 0.49/0.99 thf(cell36_type, type, cell36: $i).
% 0.49/0.99 thf(zip_tseitin_85_type, type, zip_tseitin_85: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_172_type, type, zip_tseitin_172: $i > $i > $o).
% 0.49/0.99 thf(cell83_type, type, cell83: $i).
% 0.49/0.99 thf(cell4_type, type, cell4: $i).
% 0.49/0.99 thf(zip_tseitin_125_type, type, zip_tseitin_125: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_102_type, type, zip_tseitin_102: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_88_type, type, zip_tseitin_88: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_152_type, type, zip_tseitin_152: $i > $i > $o).
% 0.49/0.99 thf(cell94_type, type, cell94: $i).
% 0.49/0.99 thf(zip_tseitin_81_type, type, zip_tseitin_81: $i > $i > $o).
% 0.49/0.99 thf(cell62_type, type, cell62: $i).
% 0.49/0.99 thf(cell46_type, type, cell46: $i).
% 0.49/0.99 thf(cell13_type, type, cell13: $i).
% 0.49/0.99 thf(zip_tseitin_134_type, type, zip_tseitin_134: $i > $i > $o).
% 0.49/0.99 thf(cell43_type, type, cell43: $i).
% 0.49/0.99 thf(cell87_type, type, cell87: $i).
% 0.49/0.99 thf(cell73_type, type, cell73: $i).
% 0.49/0.99 thf(zip_tseitin_55_type, type, zip_tseitin_55: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_171_type, type, zip_tseitin_171: $i > $i > $o).
% 0.49/0.99 thf(cell76_type, type, cell76: $i).
% 0.49/0.99 thf(zip_tseitin_157_type, type, zip_tseitin_157: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_155_type, type, zip_tseitin_155: $i > $i > $o).
% 0.49/0.99 thf(cell49_type, type, cell49: $i).
% 0.49/0.99 thf(zip_tseitin_82_type, type, zip_tseitin_82: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_98_type, type, zip_tseitin_98: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_63_type, type, zip_tseitin_63: $i > $i > $o).
% 0.49/0.99 thf(cell88_type, type, cell88: $i).
% 0.49/0.99 thf(cell63_type, type, cell63: $i).
% 0.49/0.99 thf(zip_tseitin_69_type, type, zip_tseitin_69: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_148_type, type, zip_tseitin_148: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_86_type, type, zip_tseitin_86: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_8_type, type, zip_tseitin_8: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_24_type, type, zip_tseitin_24: $i > $i > $o).
% 0.49/0.99 thf(cell90_type, type, cell90: $i).
% 0.49/0.99 thf(zip_tseitin_58_type, type, zip_tseitin_58: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_96_type, type, zip_tseitin_96: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_139_type, type, zip_tseitin_139: $i > $i > $o).
% 0.49/0.99 thf(cell1_type, type, cell1: $i).
% 0.49/0.99 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $i > $o).
% 0.49/0.99 thf(cell95_type, type, cell95: $i).
% 0.49/0.99 thf(zip_tseitin_99_type, type, zip_tseitin_99: $i > $i > $o).
% 0.49/0.99 thf(cell52_type, type, cell52: $i).
% 0.49/0.99 thf(zip_tseitin_18_type, type, zip_tseitin_18: $i > $i > $o).
% 0.49/0.99 thf(cell86_type, type, cell86: $i).
% 0.49/0.99 thf(cell7_type, type, cell7: $i).
% 0.49/0.99 thf(cell25_type, type, cell25: $i).
% 0.49/0.99 thf(cell6_type, type, cell6: $i).
% 0.49/0.99 thf(zip_tseitin_144_type, type, zip_tseitin_144: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_156_type, type, zip_tseitin_156: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_17_type, type, zip_tseitin_17: $i > $i > $o).
% 0.49/0.99 thf(cell48_type, type, cell48: $i).
% 0.49/0.99 thf(edge_type, type, edge: $i > $i > $o).
% 0.49/0.99 thf(cell64_type, type, cell64: $i).
% 0.49/0.99 thf(zip_tseitin_143_type, type, zip_tseitin_143: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_127_type, type, zip_tseitin_127: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_153_type, type, zip_tseitin_153: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_117_type, type, zip_tseitin_117: $i > $i > $o).
% 0.49/0.99 thf(cell22_type, type, cell22: $i).
% 0.49/0.99 thf(cell84_type, type, cell84: $i).
% 0.49/0.99 thf(zip_tseitin_136_type, type, zip_tseitin_136: $i > $i > $o).
% 0.49/0.99 thf(cell96_type, type, cell96: $i).
% 0.49/0.99 thf(zip_tseitin_43_type, type, zip_tseitin_43: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_167_type, type, zip_tseitin_167: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_87_type, type, zip_tseitin_87: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_16_type, type, zip_tseitin_16: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_174_type, type, zip_tseitin_174: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_130_type, type, zip_tseitin_130: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_14_type, type, zip_tseitin_14: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_176_type, type, zip_tseitin_176: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_111_type, type, zip_tseitin_111: $i > $i > $o).
% 0.49/0.99 thf(cell58_type, type, cell58: $i).
% 0.49/0.99 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_72_type, type, zip_tseitin_72: $i > $i > $o).
% 0.49/0.99 thf(cell67_type, type, cell67: $i).
% 0.49/0.99 thf(zip_tseitin_49_type, type, zip_tseitin_49: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_135_type, type, zip_tseitin_135: $i > $i > $o).
% 0.49/0.99 thf(cell69_type, type, cell69: $i).
% 0.49/0.99 thf(zip_tseitin_145_type, type, zip_tseitin_145: $i > $i > $o).
% 0.49/0.99 thf(cell38_type, type, cell38: $i).
% 0.49/0.99 thf(zip_tseitin_62_type, type, zip_tseitin_62: $i > $i > $o).
% 0.49/0.99 thf(cell23_type, type, cell23: $i).
% 0.49/0.99 thf(zip_tseitin_168_type, type, zip_tseitin_168: $i > $i > $o).
% 0.49/0.99 thf(cell29_type, type, cell29: $i).
% 0.49/0.99 thf(cell41_type, type, cell41: $i).
% 0.49/0.99 thf(cell71_type, type, cell71: $i).
% 0.49/0.99 thf(zip_tseitin_119_type, type, zip_tseitin_119: $i > $i > $o).
% 0.49/0.99 thf(cell93_type, type, cell93: $i).
% 0.49/0.99 thf(zip_tseitin_120_type, type, zip_tseitin_120: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_90_type, type, zip_tseitin_90: $i > $i > $o).
% 0.49/0.99 thf(adj_type, type, adj: $i > $i > $o).
% 0.49/0.99 thf(cell47_type, type, cell47: $i).
% 0.49/0.99 thf(zip_tseitin_74_type, type, zip_tseitin_74: $i > $i > $o).
% 0.49/0.99 thf(cell57_type, type, cell57: $i).
% 0.49/0.99 thf(cell39_type, type, cell39: $i).
% 0.49/0.99 thf(zip_tseitin_13_type, type, zip_tseitin_13: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_146_type, type, zip_tseitin_146: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_140_type, type, zip_tseitin_140: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_64_type, type, zip_tseitin_64: $i > $i > $o).
% 0.49/0.99 thf(cell35_type, type, cell35: $i).
% 0.49/0.99 thf(cell40_type, type, cell40: $i).
% 0.49/0.99 thf(zip_tseitin_28_type, type, zip_tseitin_28: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_35_type, type, zip_tseitin_35: $i > $i > $o).
% 0.49/0.99 thf(cell45_type, type, cell45: $i).
% 0.49/0.99 thf(zip_tseitin_19_type, type, zip_tseitin_19: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_124_type, type, zip_tseitin_124: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_91_type, type, zip_tseitin_91: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_31_type, type, zip_tseitin_31: $i > $i > $o).
% 0.49/0.99 thf(cell30_type, type, cell30: $i).
% 0.49/0.99 thf(cell98_type, type, cell98: $i).
% 0.49/0.99 thf(zip_tseitin_103_type, type, zip_tseitin_103: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_175_type, type, zip_tseitin_175: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_93_type, type, zip_tseitin_93: $i > $i > $o).
% 0.49/0.99 thf(cell42_type, type, cell42: $i).
% 0.49/0.99 thf(cell19_type, type, cell19: $i).
% 0.49/0.99 thf(cell78_type, type, cell78: $i).
% 0.49/0.99 thf(cell55_type, type, cell55: $i).
% 0.49/0.99 thf(zip_tseitin_166_type, type, zip_tseitin_166: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_116_type, type, zip_tseitin_116: $i > $i > $o).
% 0.49/0.99 thf(cell21_type, type, cell21: $i).
% 0.49/0.99 thf(zip_tseitin_129_type, type, zip_tseitin_129: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_142_type, type, zip_tseitin_142: $i > $i > $o).
% 0.49/0.99 thf(cell31_type, type, cell31: $i).
% 0.49/0.99 thf(zip_tseitin_104_type, type, zip_tseitin_104: $i > $i > $o).
% 0.49/0.99 thf(cell18_type, type, cell18: $i).
% 0.49/0.99 thf(cell72_type, type, cell72: $i).
% 0.49/0.99 thf(cell28_type, type, cell28: $i).
% 0.49/0.99 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $o).
% 0.49/0.99 thf(cell33_type, type, cell33: $i).
% 0.49/0.99 thf(zip_tseitin_149_type, type, zip_tseitin_149: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_67_type, type, zip_tseitin_67: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_179_type, type, zip_tseitin_179: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_36_type, type, zip_tseitin_36: $i > $i > $o).
% 0.49/0.99 thf(cell26_type, type, cell26: $i).
% 0.49/0.99 thf(zip_tseitin_54_type, type, zip_tseitin_54: $i > $i > $o).
% 0.49/0.99 thf(cell82_type, type, cell82: $i).
% 0.49/0.99 thf(zip_tseitin_76_type, type, zip_tseitin_76: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_61_type, type, zip_tseitin_61: $i > $i > $o).
% 0.49/0.99 thf(cell70_type, type, cell70: $i).
% 0.49/0.99 thf(zip_tseitin_154_type, type, zip_tseitin_154: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_22_type, type, zip_tseitin_22: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_11_type, type, zip_tseitin_11: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_12_type, type, zip_tseitin_12: $i > $i > $o).
% 0.49/0.99 thf(cell15_type, type, cell15: $i).
% 0.49/0.99 thf(cell32_type, type, cell32: $i).
% 0.49/0.99 thf(zip_tseitin_66_type, type, zip_tseitin_66: $i > $i > $o).
% 0.49/0.99 thf(cell91_type, type, cell91: $i).
% 0.49/0.99 thf(cell56_type, type, cell56: $i).
% 0.49/0.99 thf(zip_tseitin_40_type, type, zip_tseitin_40: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_126_type, type, zip_tseitin_126: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_10_type, type, zip_tseitin_10: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_56_type, type, zip_tseitin_56: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_89_type, type, zip_tseitin_89: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_151_type, type, zip_tseitin_151: $i > $i > $o).
% 0.49/0.99 thf(cell53_type, type, cell53: $i).
% 0.49/0.99 thf(zip_tseitin_79_type, type, zip_tseitin_79: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_121_type, type, zip_tseitin_121: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_162_type, type, zip_tseitin_162: $i > $i > $o).
% 0.49/0.99 thf(cell99_type, type, cell99: $i).
% 0.49/0.99 thf(cell44_type, type, cell44: $i).
% 0.49/0.99 thf(zip_tseitin_48_type, type, zip_tseitin_48: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_47_type, type, zip_tseitin_47: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_97_type, type, zip_tseitin_97: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_115_type, type, zip_tseitin_115: $i > $i > $o).
% 0.49/0.99 thf(cell10_type, type, cell10: $i).
% 0.49/0.99 thf(zip_tseitin_51_type, type, zip_tseitin_51: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_173_type, type, zip_tseitin_173: $i > $i > $o).
% 0.49/0.99 thf(cell85_type, type, cell85: $i).
% 0.49/0.99 thf(zip_tseitin_65_type, type, zip_tseitin_65: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_109_type, type, zip_tseitin_109: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_46_type, type, zip_tseitin_46: $i > $i > $o).
% 0.49/0.99 thf(cell50_type, type, cell50: $i).
% 0.49/0.99 thf(zip_tseitin_21_type, type, zip_tseitin_21: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_23_type, type, zip_tseitin_23: $i > $i > $o).
% 0.49/0.99 thf(cell34_type, type, cell34: $i).
% 0.49/0.99 thf(zip_tseitin_123_type, type, zip_tseitin_123: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_44_type, type, zip_tseitin_44: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_34_type, type, zip_tseitin_34: $i > $i > $o).
% 0.49/0.99 thf(cell9_type, type, cell9: $i).
% 0.49/0.99 thf(cell5_type, type, cell5: $i).
% 0.49/0.99 thf(cell81_type, type, cell81: $i).
% 0.49/0.99 thf(zip_tseitin_32_type, type, zip_tseitin_32: $i > $i > $o).
% 0.49/0.99 thf(cell59_type, type, cell59: $i).
% 0.49/0.99 thf(zip_tseitin_26_type, type, zip_tseitin_26: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_159_type, type, zip_tseitin_159: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_70_type, type, zip_tseitin_70: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_100_type, type, zip_tseitin_100: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_9_type, type, zip_tseitin_9: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_41_type, type, zip_tseitin_41: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_137_type, type, zip_tseitin_137: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_170_type, type, zip_tseitin_170: $i > $i > $o).
% 0.49/0.99 thf(cell14_type, type, cell14: $i).
% 0.49/0.99 thf(zip_tseitin_59_type, type, zip_tseitin_59: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_177_type, type, zip_tseitin_177: $i > $i > $o).
% 0.49/0.99 thf(cell16_type, type, cell16: $i).
% 0.49/0.99 thf(zip_tseitin_20_type, type, zip_tseitin_20: $i > $i > $o).
% 0.49/0.99 thf(cell60_type, type, cell60: $i).
% 0.49/0.99 thf(zip_tseitin_107_type, type, zip_tseitin_107: $i > $i > $o).
% 0.49/0.99 thf(cell12_type, type, cell12: $i).
% 0.49/0.99 thf(zip_tseitin_178_type, type, zip_tseitin_178: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_25_type, type, zip_tseitin_25: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_73_type, type, zip_tseitin_73: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_57_type, type, zip_tseitin_57: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_169_type, type, zip_tseitin_169: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_113_type, type, zip_tseitin_113: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_112_type, type, zip_tseitin_112: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_52_type, type, zip_tseitin_52: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_60_type, type, zip_tseitin_60: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_164_type, type, zip_tseitin_164: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_114_type, type, zip_tseitin_114: $i > $i > $o).
% 0.49/0.99 thf(zip_tseitin_30_type, type, zip_tseitin_30: $i > $i > $o).
% 0.49/0.99 thf(tlhfof24987, axiom,
% 0.49/0.99 (![TLH24985:$i,TLH24986:$i]:
% 0.49/0.99 ( ( edge @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( ( TLH24985 ) = ( cell100 ) ) & ( ( TLH24986 ) = ( cell90 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell99 ) ) & ( ( TLH24986 ) = ( cell89 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell98 ) ) & ( ( TLH24986 ) = ( cell88 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell97 ) ) & ( ( TLH24986 ) = ( cell87 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell96 ) ) & ( ( TLH24986 ) = ( cell86 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell95 ) ) & ( ( TLH24986 ) = ( cell85 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell94 ) ) & ( ( TLH24986 ) = ( cell84 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell93 ) ) & ( ( TLH24986 ) = ( cell83 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell92 ) ) & ( ( TLH24986 ) = ( cell82 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell91 ) ) & ( ( TLH24986 ) = ( cell81 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell90 ) ) & ( ( TLH24986 ) = ( cell80 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell89 ) ) & ( ( TLH24986 ) = ( cell79 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell88 ) ) & ( ( TLH24986 ) = ( cell78 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell87 ) ) & ( ( TLH24986 ) = ( cell77 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell86 ) ) & ( ( TLH24986 ) = ( cell76 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell85 ) ) & ( ( TLH24986 ) = ( cell75 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell84 ) ) & ( ( TLH24986 ) = ( cell74 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell83 ) ) & ( ( TLH24986 ) = ( cell73 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell82 ) ) & ( ( TLH24986 ) = ( cell72 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell81 ) ) & ( ( TLH24986 ) = ( cell71 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell80 ) ) & ( ( TLH24986 ) = ( cell70 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell79 ) ) & ( ( TLH24986 ) = ( cell69 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell78 ) ) & ( ( TLH24986 ) = ( cell68 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell77 ) ) & ( ( TLH24986 ) = ( cell67 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell76 ) ) & ( ( TLH24986 ) = ( cell66 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell75 ) ) & ( ( TLH24986 ) = ( cell65 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell74 ) ) & ( ( TLH24986 ) = ( cell64 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell73 ) ) & ( ( TLH24986 ) = ( cell63 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell72 ) ) & ( ( TLH24986 ) = ( cell62 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell71 ) ) & ( ( TLH24986 ) = ( cell61 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell70 ) ) & ( ( TLH24986 ) = ( cell60 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell69 ) ) & ( ( TLH24986 ) = ( cell59 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell68 ) ) & ( ( TLH24986 ) = ( cell58 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell67 ) ) & ( ( TLH24986 ) = ( cell57 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell66 ) ) & ( ( TLH24986 ) = ( cell56 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell65 ) ) & ( ( TLH24986 ) = ( cell55 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell64 ) ) & ( ( TLH24986 ) = ( cell54 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell63 ) ) & ( ( TLH24986 ) = ( cell53 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell62 ) ) & ( ( TLH24986 ) = ( cell52 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell61 ) ) & ( ( TLH24986 ) = ( cell51 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell60 ) ) & ( ( TLH24986 ) = ( cell50 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell59 ) ) & ( ( TLH24986 ) = ( cell49 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell58 ) ) & ( ( TLH24986 ) = ( cell48 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell57 ) ) & ( ( TLH24986 ) = ( cell47 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell56 ) ) & ( ( TLH24986 ) = ( cell46 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell55 ) ) & ( ( TLH24986 ) = ( cell45 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell54 ) ) & ( ( TLH24986 ) = ( cell44 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell53 ) ) & ( ( TLH24986 ) = ( cell43 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell52 ) ) & ( ( TLH24986 ) = ( cell42 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell51 ) ) & ( ( TLH24986 ) = ( cell41 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell50 ) ) & ( ( TLH24986 ) = ( cell40 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell49 ) ) & ( ( TLH24986 ) = ( cell39 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell48 ) ) & ( ( TLH24986 ) = ( cell38 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell47 ) ) & ( ( TLH24986 ) = ( cell37 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell46 ) ) & ( ( TLH24986 ) = ( cell36 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell45 ) ) & ( ( TLH24986 ) = ( cell35 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell44 ) ) & ( ( TLH24986 ) = ( cell34 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell43 ) ) & ( ( TLH24986 ) = ( cell33 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell42 ) ) & ( ( TLH24986 ) = ( cell32 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell41 ) ) & ( ( TLH24986 ) = ( cell31 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell40 ) ) & ( ( TLH24986 ) = ( cell30 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell39 ) ) & ( ( TLH24986 ) = ( cell29 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell38 ) ) & ( ( TLH24986 ) = ( cell28 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell37 ) ) & ( ( TLH24986 ) = ( cell27 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell36 ) ) & ( ( TLH24986 ) = ( cell26 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell35 ) ) & ( ( TLH24986 ) = ( cell25 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell34 ) ) & ( ( TLH24986 ) = ( cell24 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell33 ) ) & ( ( TLH24986 ) = ( cell23 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell32 ) ) & ( ( TLH24986 ) = ( cell22 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell31 ) ) & ( ( TLH24986 ) = ( cell21 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell30 ) ) & ( ( TLH24986 ) = ( cell20 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell29 ) ) & ( ( TLH24986 ) = ( cell19 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell28 ) ) & ( ( TLH24986 ) = ( cell18 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell27 ) ) & ( ( TLH24986 ) = ( cell17 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell26 ) ) & ( ( TLH24986 ) = ( cell16 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell25 ) ) & ( ( TLH24986 ) = ( cell15 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell24 ) ) & ( ( TLH24986 ) = ( cell14 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell23 ) ) & ( ( TLH24986 ) = ( cell13 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell22 ) ) & ( ( TLH24986 ) = ( cell12 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell21 ) ) & ( ( TLH24986 ) = ( cell11 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell20 ) ) & ( ( TLH24986 ) = ( cell10 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell19 ) ) & ( ( TLH24986 ) = ( cell9 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell18 ) ) & ( ( TLH24986 ) = ( cell8 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell17 ) ) & ( ( TLH24986 ) = ( cell7 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell16 ) ) & ( ( TLH24986 ) = ( cell6 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell15 ) ) & ( ( TLH24986 ) = ( cell5 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell14 ) ) & ( ( TLH24986 ) = ( cell4 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell13 ) ) & ( ( TLH24986 ) = ( cell3 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell12 ) ) & ( ( TLH24986 ) = ( cell2 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell11 ) ) & ( ( TLH24986 ) = ( cell1 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell100 ) ) & ( ( TLH24986 ) = ( cell99 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell99 ) ) & ( ( TLH24986 ) = ( cell98 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell98 ) ) & ( ( TLH24986 ) = ( cell97 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell97 ) ) & ( ( TLH24986 ) = ( cell96 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell96 ) ) & ( ( TLH24986 ) = ( cell95 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell95 ) ) & ( ( TLH24986 ) = ( cell94 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell94 ) ) & ( ( TLH24986 ) = ( cell93 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell93 ) ) & ( ( TLH24986 ) = ( cell92 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell92 ) ) & ( ( TLH24986 ) = ( cell91 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell90 ) ) & ( ( TLH24986 ) = ( cell89 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell89 ) ) & ( ( TLH24986 ) = ( cell88 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell88 ) ) & ( ( TLH24986 ) = ( cell87 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell87 ) ) & ( ( TLH24986 ) = ( cell86 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell86 ) ) & ( ( TLH24986 ) = ( cell85 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell85 ) ) & ( ( TLH24986 ) = ( cell84 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell84 ) ) & ( ( TLH24986 ) = ( cell83 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell83 ) ) & ( ( TLH24986 ) = ( cell82 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell82 ) ) & ( ( TLH24986 ) = ( cell81 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell80 ) ) & ( ( TLH24986 ) = ( cell79 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell79 ) ) & ( ( TLH24986 ) = ( cell78 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell78 ) ) & ( ( TLH24986 ) = ( cell77 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell77 ) ) & ( ( TLH24986 ) = ( cell76 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell76 ) ) & ( ( TLH24986 ) = ( cell75 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell75 ) ) & ( ( TLH24986 ) = ( cell74 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell74 ) ) & ( ( TLH24986 ) = ( cell73 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell73 ) ) & ( ( TLH24986 ) = ( cell72 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell72 ) ) & ( ( TLH24986 ) = ( cell71 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell70 ) ) & ( ( TLH24986 ) = ( cell69 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell69 ) ) & ( ( TLH24986 ) = ( cell68 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell68 ) ) & ( ( TLH24986 ) = ( cell67 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell67 ) ) & ( ( TLH24986 ) = ( cell66 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell66 ) ) & ( ( TLH24986 ) = ( cell65 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell65 ) ) & ( ( TLH24986 ) = ( cell64 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell64 ) ) & ( ( TLH24986 ) = ( cell63 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell63 ) ) & ( ( TLH24986 ) = ( cell62 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell62 ) ) & ( ( TLH24986 ) = ( cell61 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell60 ) ) & ( ( TLH24986 ) = ( cell59 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell59 ) ) & ( ( TLH24986 ) = ( cell58 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell58 ) ) & ( ( TLH24986 ) = ( cell57 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell57 ) ) & ( ( TLH24986 ) = ( cell56 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell56 ) ) & ( ( TLH24986 ) = ( cell55 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell55 ) ) & ( ( TLH24986 ) = ( cell54 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell54 ) ) & ( ( TLH24986 ) = ( cell53 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell53 ) ) & ( ( TLH24986 ) = ( cell52 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell52 ) ) & ( ( TLH24986 ) = ( cell51 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell50 ) ) & ( ( TLH24986 ) = ( cell49 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell49 ) ) & ( ( TLH24986 ) = ( cell48 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell48 ) ) & ( ( TLH24986 ) = ( cell47 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell47 ) ) & ( ( TLH24986 ) = ( cell46 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell46 ) ) & ( ( TLH24986 ) = ( cell45 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell45 ) ) & ( ( TLH24986 ) = ( cell44 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell44 ) ) & ( ( TLH24986 ) = ( cell43 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell43 ) ) & ( ( TLH24986 ) = ( cell42 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell42 ) ) & ( ( TLH24986 ) = ( cell41 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell40 ) ) & ( ( TLH24986 ) = ( cell39 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell39 ) ) & ( ( TLH24986 ) = ( cell38 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell38 ) ) & ( ( TLH24986 ) = ( cell37 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell37 ) ) & ( ( TLH24986 ) = ( cell36 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell36 ) ) & ( ( TLH24986 ) = ( cell35 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell35 ) ) & ( ( TLH24986 ) = ( cell34 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell34 ) ) & ( ( TLH24986 ) = ( cell33 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell33 ) ) & ( ( TLH24986 ) = ( cell32 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell32 ) ) & ( ( TLH24986 ) = ( cell31 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell30 ) ) & ( ( TLH24986 ) = ( cell29 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell29 ) ) & ( ( TLH24986 ) = ( cell28 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell28 ) ) & ( ( TLH24986 ) = ( cell27 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell27 ) ) & ( ( TLH24986 ) = ( cell26 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell26 ) ) & ( ( TLH24986 ) = ( cell25 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell25 ) ) & ( ( TLH24986 ) = ( cell24 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell24 ) ) & ( ( TLH24986 ) = ( cell23 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell23 ) ) & ( ( TLH24986 ) = ( cell22 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell22 ) ) & ( ( TLH24986 ) = ( cell21 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell20 ) ) & ( ( TLH24986 ) = ( cell19 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell19 ) ) & ( ( TLH24986 ) = ( cell18 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell18 ) ) & ( ( TLH24986 ) = ( cell17 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell17 ) ) & ( ( TLH24986 ) = ( cell16 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell16 ) ) & ( ( TLH24986 ) = ( cell15 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell15 ) ) & ( ( TLH24986 ) = ( cell14 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell14 ) ) & ( ( TLH24986 ) = ( cell13 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell13 ) ) & ( ( TLH24986 ) = ( cell12 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell12 ) ) & ( ( TLH24986 ) = ( cell11 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell10 ) ) & ( ( TLH24986 ) = ( cell9 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell9 ) ) & ( ( TLH24986 ) = ( cell8 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell8 ) ) & ( ( TLH24986 ) = ( cell7 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell7 ) ) & ( ( TLH24986 ) = ( cell6 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell6 ) ) & ( ( TLH24986 ) = ( cell5 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell5 ) ) & ( ( TLH24986 ) = ( cell4 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell4 ) ) & ( ( TLH24986 ) = ( cell3 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell3 ) ) & ( ( TLH24986 ) = ( cell2 ) ) ) |
% 0.49/0.99 ( ( ( TLH24985 ) = ( cell2 ) ) & ( ( TLH24986 ) = ( cell1 ) ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_0, type, zip_tseitin_179 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_1, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_179 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell1 ) ) & ( ( TLH24985 ) = ( cell2 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_2, type, zip_tseitin_178 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_3, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_178 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell2 ) ) & ( ( TLH24985 ) = ( cell3 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_4, type, zip_tseitin_177 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_5, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_177 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell3 ) ) & ( ( TLH24985 ) = ( cell4 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_6, type, zip_tseitin_176 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_7, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_176 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell4 ) ) & ( ( TLH24985 ) = ( cell5 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_8, type, zip_tseitin_175 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_9, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_175 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell5 ) ) & ( ( TLH24985 ) = ( cell6 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_10, type, zip_tseitin_174 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_11, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_174 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell6 ) ) & ( ( TLH24985 ) = ( cell7 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_12, type, zip_tseitin_173 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_13, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_173 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell7 ) ) & ( ( TLH24985 ) = ( cell8 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_14, type, zip_tseitin_172 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_15, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_172 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell8 ) ) & ( ( TLH24985 ) = ( cell9 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_16, type, zip_tseitin_171 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_17, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_171 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell9 ) ) & ( ( TLH24985 ) = ( cell10 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_18, type, zip_tseitin_170 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_19, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_170 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell11 ) ) & ( ( TLH24985 ) = ( cell12 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_20, type, zip_tseitin_169 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_21, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_169 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell12 ) ) & ( ( TLH24985 ) = ( cell13 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_22, type, zip_tseitin_168 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_23, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_168 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell13 ) ) & ( ( TLH24985 ) = ( cell14 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_24, type, zip_tseitin_167 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_25, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_167 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell14 ) ) & ( ( TLH24985 ) = ( cell15 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_26, type, zip_tseitin_166 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_27, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_166 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell15 ) ) & ( ( TLH24985 ) = ( cell16 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_28, type, zip_tseitin_165 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_29, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_165 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell16 ) ) & ( ( TLH24985 ) = ( cell17 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_30, type, zip_tseitin_164 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_31, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_164 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell17 ) ) & ( ( TLH24985 ) = ( cell18 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_32, type, zip_tseitin_163 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_33, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_163 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell18 ) ) & ( ( TLH24985 ) = ( cell19 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_34, type, zip_tseitin_162 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_35, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_162 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell19 ) ) & ( ( TLH24985 ) = ( cell20 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_36, type, zip_tseitin_161 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_37, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_161 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell21 ) ) & ( ( TLH24985 ) = ( cell22 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_38, type, zip_tseitin_160 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_39, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_160 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell22 ) ) & ( ( TLH24985 ) = ( cell23 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_40, type, zip_tseitin_159 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_41, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_159 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell23 ) ) & ( ( TLH24985 ) = ( cell24 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_42, type, zip_tseitin_158 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_43, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_158 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell24 ) ) & ( ( TLH24985 ) = ( cell25 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_44, type, zip_tseitin_157 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_45, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_157 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell25 ) ) & ( ( TLH24985 ) = ( cell26 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_46, type, zip_tseitin_156 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_47, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_156 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell26 ) ) & ( ( TLH24985 ) = ( cell27 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_48, type, zip_tseitin_155 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_49, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_155 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell27 ) ) & ( ( TLH24985 ) = ( cell28 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_50, type, zip_tseitin_154 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_51, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_154 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell28 ) ) & ( ( TLH24985 ) = ( cell29 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_52, type, zip_tseitin_153 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_53, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_153 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell29 ) ) & ( ( TLH24985 ) = ( cell30 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_54, type, zip_tseitin_152 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_55, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_152 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell31 ) ) & ( ( TLH24985 ) = ( cell32 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_56, type, zip_tseitin_151 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_57, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_151 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell32 ) ) & ( ( TLH24985 ) = ( cell33 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_58, type, zip_tseitin_150 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_59, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_150 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell33 ) ) & ( ( TLH24985 ) = ( cell34 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_60, type, zip_tseitin_149 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_61, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_149 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell34 ) ) & ( ( TLH24985 ) = ( cell35 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_62, type, zip_tseitin_148 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_63, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_148 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell35 ) ) & ( ( TLH24985 ) = ( cell36 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_64, type, zip_tseitin_147 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_65, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_147 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell36 ) ) & ( ( TLH24985 ) = ( cell37 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_66, type, zip_tseitin_146 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_67, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_146 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell37 ) ) & ( ( TLH24985 ) = ( cell38 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_68, type, zip_tseitin_145 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_69, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_145 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell38 ) ) & ( ( TLH24985 ) = ( cell39 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_70, type, zip_tseitin_144 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_71, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_144 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell39 ) ) & ( ( TLH24985 ) = ( cell40 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_72, type, zip_tseitin_143 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_73, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_143 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell41 ) ) & ( ( TLH24985 ) = ( cell42 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_74, type, zip_tseitin_142 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_75, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_142 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell42 ) ) & ( ( TLH24985 ) = ( cell43 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_76, type, zip_tseitin_141 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_77, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_141 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell43 ) ) & ( ( TLH24985 ) = ( cell44 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_78, type, zip_tseitin_140 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_79, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_140 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell44 ) ) & ( ( TLH24985 ) = ( cell45 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_80, type, zip_tseitin_139 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_81, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_139 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell45 ) ) & ( ( TLH24985 ) = ( cell46 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_82, type, zip_tseitin_138 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_83, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_138 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell46 ) ) & ( ( TLH24985 ) = ( cell47 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_84, type, zip_tseitin_137 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_85, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_137 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell47 ) ) & ( ( TLH24985 ) = ( cell48 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_86, type, zip_tseitin_136 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_87, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_136 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell48 ) ) & ( ( TLH24985 ) = ( cell49 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_88, type, zip_tseitin_135 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_89, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_135 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell49 ) ) & ( ( TLH24985 ) = ( cell50 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_90, type, zip_tseitin_134 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_91, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_134 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell51 ) ) & ( ( TLH24985 ) = ( cell52 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_92, type, zip_tseitin_133 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_93, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_133 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell52 ) ) & ( ( TLH24985 ) = ( cell53 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_94, type, zip_tseitin_132 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_95, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_132 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell53 ) ) & ( ( TLH24985 ) = ( cell54 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_96, type, zip_tseitin_131 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_97, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_131 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell54 ) ) & ( ( TLH24985 ) = ( cell55 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_98, type, zip_tseitin_130 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_99, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_130 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell55 ) ) & ( ( TLH24985 ) = ( cell56 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_100, type, zip_tseitin_129 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_101, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_129 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell56 ) ) & ( ( TLH24985 ) = ( cell57 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_102, type, zip_tseitin_128 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_103, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_128 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell57 ) ) & ( ( TLH24985 ) = ( cell58 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_104, type, zip_tseitin_127 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_105, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_127 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell58 ) ) & ( ( TLH24985 ) = ( cell59 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_106, type, zip_tseitin_126 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_107, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_126 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell59 ) ) & ( ( TLH24985 ) = ( cell60 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_108, type, zip_tseitin_125 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_109, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_125 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell61 ) ) & ( ( TLH24985 ) = ( cell62 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_110, type, zip_tseitin_124 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_111, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_124 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell62 ) ) & ( ( TLH24985 ) = ( cell63 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_112, type, zip_tseitin_123 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_113, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_123 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell63 ) ) & ( ( TLH24985 ) = ( cell64 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_114, type, zip_tseitin_122 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_115, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_122 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell64 ) ) & ( ( TLH24985 ) = ( cell65 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_116, type, zip_tseitin_121 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_117, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_121 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell65 ) ) & ( ( TLH24985 ) = ( cell66 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_118, type, zip_tseitin_120 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_119, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_120 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell66 ) ) & ( ( TLH24985 ) = ( cell67 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_120, type, zip_tseitin_119 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_121, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_119 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell67 ) ) & ( ( TLH24985 ) = ( cell68 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_122, type, zip_tseitin_118 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_123, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_118 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell68 ) ) & ( ( TLH24985 ) = ( cell69 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_124, type, zip_tseitin_117 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_125, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_117 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell69 ) ) & ( ( TLH24985 ) = ( cell70 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_126, type, zip_tseitin_116 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_127, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_116 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell71 ) ) & ( ( TLH24985 ) = ( cell72 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_128, type, zip_tseitin_115 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_129, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_115 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell72 ) ) & ( ( TLH24985 ) = ( cell73 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_130, type, zip_tseitin_114 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_131, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_114 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell73 ) ) & ( ( TLH24985 ) = ( cell74 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_132, type, zip_tseitin_113 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_133, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_113 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell74 ) ) & ( ( TLH24985 ) = ( cell75 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_134, type, zip_tseitin_112 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_135, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_112 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell75 ) ) & ( ( TLH24985 ) = ( cell76 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_136, type, zip_tseitin_111 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_137, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_111 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell76 ) ) & ( ( TLH24985 ) = ( cell77 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_138, type, zip_tseitin_110 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_139, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_110 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell77 ) ) & ( ( TLH24985 ) = ( cell78 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_140, type, zip_tseitin_109 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_141, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_109 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell78 ) ) & ( ( TLH24985 ) = ( cell79 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_142, type, zip_tseitin_108 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_143, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_108 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell79 ) ) & ( ( TLH24985 ) = ( cell80 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_144, type, zip_tseitin_107 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_145, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_107 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell81 ) ) & ( ( TLH24985 ) = ( cell82 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_146, type, zip_tseitin_106 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_147, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_106 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell82 ) ) & ( ( TLH24985 ) = ( cell83 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_148, type, zip_tseitin_105 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_149, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_105 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell83 ) ) & ( ( TLH24985 ) = ( cell84 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_150, type, zip_tseitin_104 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_151, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_104 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell84 ) ) & ( ( TLH24985 ) = ( cell85 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_152, type, zip_tseitin_103 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_153, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_103 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell85 ) ) & ( ( TLH24985 ) = ( cell86 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_154, type, zip_tseitin_102 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_155, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_102 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell86 ) ) & ( ( TLH24985 ) = ( cell87 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_156, type, zip_tseitin_101 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_157, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_101 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell87 ) ) & ( ( TLH24985 ) = ( cell88 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_158, type, zip_tseitin_100 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_159, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_100 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell88 ) ) & ( ( TLH24985 ) = ( cell89 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_160, type, zip_tseitin_99 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_161, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_99 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell89 ) ) & ( ( TLH24985 ) = ( cell90 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_162, type, zip_tseitin_98 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_163, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_98 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell91 ) ) & ( ( TLH24985 ) = ( cell92 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_164, type, zip_tseitin_97 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_165, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_97 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell92 ) ) & ( ( TLH24985 ) = ( cell93 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_166, type, zip_tseitin_96 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_167, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_96 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell93 ) ) & ( ( TLH24985 ) = ( cell94 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_168, type, zip_tseitin_95 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_169, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_95 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell94 ) ) & ( ( TLH24985 ) = ( cell95 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_170, type, zip_tseitin_94 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_171, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_94 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell95 ) ) & ( ( TLH24985 ) = ( cell96 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_172, type, zip_tseitin_93 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_173, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_93 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell96 ) ) & ( ( TLH24985 ) = ( cell97 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_174, type, zip_tseitin_92 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_175, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_92 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell97 ) ) & ( ( TLH24985 ) = ( cell98 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_176, type, zip_tseitin_91 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_177, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_91 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell98 ) ) & ( ( TLH24985 ) = ( cell99 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_178, type, zip_tseitin_90 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_179, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_90 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell99 ) ) & ( ( TLH24985 ) = ( cell100 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_180, type, zip_tseitin_89 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_181, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_89 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell1 ) ) & ( ( TLH24985 ) = ( cell11 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_182, type, zip_tseitin_88 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_183, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_88 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell2 ) ) & ( ( TLH24985 ) = ( cell12 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_184, type, zip_tseitin_87 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_185, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_87 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell3 ) ) & ( ( TLH24985 ) = ( cell13 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_186, type, zip_tseitin_86 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_187, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_86 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell4 ) ) & ( ( TLH24985 ) = ( cell14 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_188, type, zip_tseitin_85 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_189, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_85 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell5 ) ) & ( ( TLH24985 ) = ( cell15 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_190, type, zip_tseitin_84 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_191, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_84 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell6 ) ) & ( ( TLH24985 ) = ( cell16 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_192, type, zip_tseitin_83 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_193, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_83 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell7 ) ) & ( ( TLH24985 ) = ( cell17 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_194, type, zip_tseitin_82 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_195, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_82 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell8 ) ) & ( ( TLH24985 ) = ( cell18 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_196, type, zip_tseitin_81 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_197, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_81 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell9 ) ) & ( ( TLH24985 ) = ( cell19 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_198, type, zip_tseitin_80 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_199, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_80 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell10 ) ) & ( ( TLH24985 ) = ( cell20 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_200, type, zip_tseitin_79 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_201, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_79 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell11 ) ) & ( ( TLH24985 ) = ( cell21 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_202, type, zip_tseitin_78 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_203, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_78 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell12 ) ) & ( ( TLH24985 ) = ( cell22 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_204, type, zip_tseitin_77 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_205, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_77 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell13 ) ) & ( ( TLH24985 ) = ( cell23 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_206, type, zip_tseitin_76 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_207, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_76 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell14 ) ) & ( ( TLH24985 ) = ( cell24 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_208, type, zip_tseitin_75 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_209, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_75 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell15 ) ) & ( ( TLH24985 ) = ( cell25 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_210, type, zip_tseitin_74 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_211, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_74 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell16 ) ) & ( ( TLH24985 ) = ( cell26 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_212, type, zip_tseitin_73 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_213, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_73 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell17 ) ) & ( ( TLH24985 ) = ( cell27 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_214, type, zip_tseitin_72 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_215, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_72 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell18 ) ) & ( ( TLH24985 ) = ( cell28 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_216, type, zip_tseitin_71 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_217, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_71 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell19 ) ) & ( ( TLH24985 ) = ( cell29 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_218, type, zip_tseitin_70 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_219, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_70 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell20 ) ) & ( ( TLH24985 ) = ( cell30 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_220, type, zip_tseitin_69 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_221, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_69 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell21 ) ) & ( ( TLH24985 ) = ( cell31 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_222, type, zip_tseitin_68 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_223, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_68 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell22 ) ) & ( ( TLH24985 ) = ( cell32 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_224, type, zip_tseitin_67 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_225, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_67 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell23 ) ) & ( ( TLH24985 ) = ( cell33 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_226, type, zip_tseitin_66 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_227, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_66 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell24 ) ) & ( ( TLH24985 ) = ( cell34 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_228, type, zip_tseitin_65 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_229, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_65 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell25 ) ) & ( ( TLH24985 ) = ( cell35 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_230, type, zip_tseitin_64 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_231, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_64 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell26 ) ) & ( ( TLH24985 ) = ( cell36 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_232, type, zip_tseitin_63 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_233, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_63 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell27 ) ) & ( ( TLH24985 ) = ( cell37 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_234, type, zip_tseitin_62 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_235, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_62 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell28 ) ) & ( ( TLH24985 ) = ( cell38 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_236, type, zip_tseitin_61 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_237, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_61 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell29 ) ) & ( ( TLH24985 ) = ( cell39 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_238, type, zip_tseitin_60 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_239, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_60 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell30 ) ) & ( ( TLH24985 ) = ( cell40 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_240, type, zip_tseitin_59 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_241, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_59 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell31 ) ) & ( ( TLH24985 ) = ( cell41 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_242, type, zip_tseitin_58 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_243, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_58 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell32 ) ) & ( ( TLH24985 ) = ( cell42 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_244, type, zip_tseitin_57 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_245, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_57 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell33 ) ) & ( ( TLH24985 ) = ( cell43 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_246, type, zip_tseitin_56 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_247, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_56 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell34 ) ) & ( ( TLH24985 ) = ( cell44 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_248, type, zip_tseitin_55 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_249, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_55 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell35 ) ) & ( ( TLH24985 ) = ( cell45 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_250, type, zip_tseitin_54 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_251, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_54 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell36 ) ) & ( ( TLH24985 ) = ( cell46 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_252, type, zip_tseitin_53 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_253, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_53 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell37 ) ) & ( ( TLH24985 ) = ( cell47 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_254, type, zip_tseitin_52 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_255, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_52 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell38 ) ) & ( ( TLH24985 ) = ( cell48 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_256, type, zip_tseitin_51 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_257, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_51 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell39 ) ) & ( ( TLH24985 ) = ( cell49 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_258, type, zip_tseitin_50 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_259, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_50 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell40 ) ) & ( ( TLH24985 ) = ( cell50 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_260, type, zip_tseitin_49 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_261, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_49 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell41 ) ) & ( ( TLH24985 ) = ( cell51 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_262, type, zip_tseitin_48 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_263, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_48 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell42 ) ) & ( ( TLH24985 ) = ( cell52 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_264, type, zip_tseitin_47 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_265, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_47 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell43 ) ) & ( ( TLH24985 ) = ( cell53 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_266, type, zip_tseitin_46 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_267, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_46 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell44 ) ) & ( ( TLH24985 ) = ( cell54 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_268, type, zip_tseitin_45 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_269, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_45 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell45 ) ) & ( ( TLH24985 ) = ( cell55 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_270, type, zip_tseitin_44 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_271, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_44 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell46 ) ) & ( ( TLH24985 ) = ( cell56 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_272, type, zip_tseitin_43 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_273, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_43 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell47 ) ) & ( ( TLH24985 ) = ( cell57 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_274, type, zip_tseitin_42 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_275, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_42 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell48 ) ) & ( ( TLH24985 ) = ( cell58 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_276, type, zip_tseitin_41 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_277, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_41 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell49 ) ) & ( ( TLH24985 ) = ( cell59 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_278, type, zip_tseitin_40 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_279, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_40 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell50 ) ) & ( ( TLH24985 ) = ( cell60 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_280, type, zip_tseitin_39 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_281, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_39 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell51 ) ) & ( ( TLH24985 ) = ( cell61 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_282, type, zip_tseitin_38 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_283, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_38 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell52 ) ) & ( ( TLH24985 ) = ( cell62 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_284, type, zip_tseitin_37 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_285, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_37 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell53 ) ) & ( ( TLH24985 ) = ( cell63 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_286, type, zip_tseitin_36 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_287, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_36 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell54 ) ) & ( ( TLH24985 ) = ( cell64 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_288, type, zip_tseitin_35 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_289, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_35 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell55 ) ) & ( ( TLH24985 ) = ( cell65 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_290, type, zip_tseitin_34 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_291, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_34 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell56 ) ) & ( ( TLH24985 ) = ( cell66 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_292, type, zip_tseitin_33 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_293, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_33 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell57 ) ) & ( ( TLH24985 ) = ( cell67 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_294, type, zip_tseitin_32 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_295, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_32 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell58 ) ) & ( ( TLH24985 ) = ( cell68 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_296, type, zip_tseitin_31 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_297, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_31 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell59 ) ) & ( ( TLH24985 ) = ( cell69 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_298, type, zip_tseitin_30 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_299, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_30 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell60 ) ) & ( ( TLH24985 ) = ( cell70 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_300, type, zip_tseitin_29 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_301, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_29 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell61 ) ) & ( ( TLH24985 ) = ( cell71 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_302, type, zip_tseitin_28 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_303, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_28 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell62 ) ) & ( ( TLH24985 ) = ( cell72 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_304, type, zip_tseitin_27 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_305, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_27 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell63 ) ) & ( ( TLH24985 ) = ( cell73 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_306, type, zip_tseitin_26 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_307, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_26 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell64 ) ) & ( ( TLH24985 ) = ( cell74 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_308, type, zip_tseitin_25 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_309, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_25 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell65 ) ) & ( ( TLH24985 ) = ( cell75 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_310, type, zip_tseitin_24 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_311, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_24 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell66 ) ) & ( ( TLH24985 ) = ( cell76 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_312, type, zip_tseitin_23 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_313, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_23 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell67 ) ) & ( ( TLH24985 ) = ( cell77 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_314, type, zip_tseitin_22 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_315, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_22 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell68 ) ) & ( ( TLH24985 ) = ( cell78 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_316, type, zip_tseitin_21 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_317, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_21 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell69 ) ) & ( ( TLH24985 ) = ( cell79 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_318, type, zip_tseitin_20 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_319, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_20 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell70 ) ) & ( ( TLH24985 ) = ( cell80 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_320, type, zip_tseitin_19 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_321, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_19 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell71 ) ) & ( ( TLH24985 ) = ( cell81 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_322, type, zip_tseitin_18 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_323, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_18 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell72 ) ) & ( ( TLH24985 ) = ( cell82 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_324, type, zip_tseitin_17 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_325, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_17 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell73 ) ) & ( ( TLH24985 ) = ( cell83 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_326, type, zip_tseitin_16 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_327, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_16 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell74 ) ) & ( ( TLH24985 ) = ( cell84 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_328, type, zip_tseitin_15 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_329, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_15 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell75 ) ) & ( ( TLH24985 ) = ( cell85 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_330, type, zip_tseitin_14 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_331, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_14 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell76 ) ) & ( ( TLH24985 ) = ( cell86 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_332, type, zip_tseitin_13 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_333, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_13 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell77 ) ) & ( ( TLH24985 ) = ( cell87 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_334, type, zip_tseitin_12 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_335, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_12 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell78 ) ) & ( ( TLH24985 ) = ( cell88 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_336, type, zip_tseitin_11 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_337, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_11 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell79 ) ) & ( ( TLH24985 ) = ( cell89 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_338, type, zip_tseitin_10 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_339, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_10 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell80 ) ) & ( ( TLH24985 ) = ( cell90 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_340, type, zip_tseitin_9 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_341, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_9 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell81 ) ) & ( ( TLH24985 ) = ( cell91 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_342, type, zip_tseitin_8 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_343, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_8 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell82 ) ) & ( ( TLH24985 ) = ( cell92 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_344, type, zip_tseitin_7 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_345, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_7 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell83 ) ) & ( ( TLH24985 ) = ( cell93 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_346, type, zip_tseitin_6 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_347, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_6 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell84 ) ) & ( ( TLH24985 ) = ( cell94 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_348, type, zip_tseitin_5 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_349, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_5 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell85 ) ) & ( ( TLH24985 ) = ( cell95 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_350, type, zip_tseitin_4 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_351, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_4 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell86 ) ) & ( ( TLH24985 ) = ( cell96 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_352, type, zip_tseitin_3 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_353, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_3 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell87 ) ) & ( ( TLH24985 ) = ( cell97 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_354, type, zip_tseitin_2 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_355, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_2 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell88 ) ) & ( ( TLH24985 ) = ( cell98 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_356, type, zip_tseitin_1 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_357, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_1 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell89 ) ) & ( ( TLH24985 ) = ( cell99 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_358, type, zip_tseitin_0 : $i > $i > $o).
% 0.49/0.99 thf(zf_stmt_359, axiom,
% 0.49/0.99 (![TLH24986:$i,TLH24985:$i]:
% 0.49/0.99 ( ( zip_tseitin_0 @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( ( TLH24986 ) = ( cell90 ) ) & ( ( TLH24985 ) = ( cell100 ) ) ) ))).
% 0.49/0.99 thf(zf_stmt_360, axiom,
% 0.49/0.99 (![TLH24985:$i,TLH24986:$i]:
% 0.49/0.99 ( ( edge @ TLH24986 @ TLH24985 ) <=>
% 0.49/0.99 ( ( zip_tseitin_179 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_178 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_177 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_176 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_175 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_174 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_173 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_172 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_171 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_170 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_169 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_168 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_167 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_166 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_165 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_164 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_163 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_162 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_161 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_160 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_159 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_158 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_157 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_156 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_155 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_154 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_153 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_152 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_151 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_150 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_149 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_148 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_147 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_146 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_145 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_144 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_143 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_142 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_141 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_140 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_139 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_138 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_137 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_136 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_135 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_134 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_133 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_132 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_131 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_130 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_129 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_128 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_127 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_126 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_125 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_124 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_123 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_122 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_121 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_120 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_119 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_118 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_117 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_116 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_115 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_114 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_113 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_112 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_111 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_110 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_109 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_108 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_107 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_106 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_105 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_104 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_103 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_102 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_101 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_100 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_99 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_98 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_97 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_96 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_95 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_94 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_93 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_92 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_91 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_90 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_89 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_88 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_87 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_86 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_85 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_84 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_83 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_82 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_81 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_80 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_79 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_78 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_77 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_76 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_75 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_74 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_73 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_72 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_71 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_70 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_69 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_68 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_67 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_66 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_65 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_64 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_63 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_62 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_61 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_60 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_59 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_58 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_57 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_56 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_55 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_54 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_53 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_52 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_51 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_50 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_49 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_48 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_47 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_46 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_45 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_44 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_43 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_42 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_41 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_40 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_39 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_38 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_37 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_36 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_35 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_34 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_33 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_32 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_31 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_30 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_29 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_28 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_27 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_26 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_25 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_24 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_23 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_22 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_21 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_20 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_19 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_18 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_17 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_16 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_15 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_14 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_13 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_12 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_11 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_10 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_9 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_8 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_7 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_6 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_5 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_4 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_3 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_2 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_1 @ TLH24986 @ TLH24985 ) |
% 0.49/0.99 ( zip_tseitin_0 @ TLH24986 @ TLH24985 ) ) ))).
% 0.49/0.99 thf(zip_derived_cl551, plain,
% 0.49/0.99 (![X0 : $i, X1 : $i]: ( (edge @ X0 @ X1) | ~ (zip_tseitin_169 @ X0 @ X1))),
% 0.49/0.99 inference('cnf', [status(esa)], [zf_stmt_360])).
% 0.49/0.99 thf(zip_derived_cl509, plain,
% 0.49/0.99 (![X0 : $i, X1 : $i]:
% 0.49/0.99 ( (zip_tseitin_169 @ X0 @ X1)
% 0.49/0.99 | ((X1) != (cell13))
% 0.49/0.99 | ((X0) != (cell12)))),
% 0.49/0.99 inference('cnf', [status(esa)], [zf_stmt_21])).
% 0.49/0.99 thf(zip_derived_cl833, plain,
% 0.49/0.99 (![X0 : $i, X1 : $i]:
% 0.49/0.99 ( (edge @ X1 @ X0) | ((X0) != (cell13)) | ((X1) != (cell12)))),
% 0.49/0.99 inference('s_sup+', [status(thm)], [zip_derived_cl551, zip_derived_cl509])).
% 0.49/0.99 thf(tlhfof24988, axiom,
% 0.49/0.99 (![Y:$i,X:$i]:
% 0.49/0.99 ( ( adj @ X @ Y ) <=> ( ( edge @ X @ Y ) | ( edge @ Y @ X ) ) ))).
% 0.49/0.99 thf(zip_derived_cl722, plain,
% 0.49/0.99 (![X0 : $i, X1 : $i]: ( (adj @ X0 @ X1) | ~ (edge @ X0 @ X1))),
% 0.49/0.99 inference('cnf', [status(esa)], [tlhfof24988])).
% 0.49/0.99 thf(tlhfof24989, conjecture, (adj @ cell12 @ cell13)).
% 0.49/0.99 thf(zf_stmt_361, negated_conjecture, (~( adj @ cell12 @ cell13 )),
% 0.49/0.99 inference('cnf.neg', [status(esa)], [tlhfof24989])).
% 0.49/0.99 thf(zip_derived_cl724, plain, (~ (adj @ cell12 @ cell13)),
% 0.49/0.99 inference('cnf', [status(esa)], [zf_stmt_361])).
% 0.49/0.99 thf(zip_derived_cl797, plain, (~ (edge @ cell12 @ cell13)),
% 0.49/0.99 inference('s_sup-', [status(thm)], [zip_derived_cl722, zip_derived_cl724])).
% 0.49/0.99 thf(zip_derived_cl837, plain,
% 0.49/0.99 ((((cell12) != (cell12)) | ((cell13) != (cell13)))),
% 0.49/0.99 inference('s_sup-', [status(thm)], [zip_derived_cl833, zip_derived_cl797])).
% 0.49/0.99 thf(zip_derived_cl839, plain, ($false),
% 0.49/0.99 inference('simplify', [status(thm)], [zip_derived_cl837])).
% 0.49/0.99
% 0.49/0.99 % SZS output end Refutation
% 0.49/0.99
% 0.49/0.99
% 0.49/0.99 % Terminating...
% 3.66/1.12 % Runner terminated.
% 3.66/1.14 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------