%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : HWV089-1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Oct 7 10:22:43 AM UTC 2026
% Result : Unsatisfiable 33.61s 5.87s
% Output : CNFRefutation 33.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 2
% Syntax : Number of formulae : 11 ( 11 unt; 0 typ; 0 def)
% Number of atoms : 27 ( 8 equ; 0 cnn)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &; 0 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 1387 (1384 usr; 190 con; 0-3 aty)
% Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_address,type,
address: $i > $o ).
thf(tp_addressDiff,type,
addressDiff: $i > $i > $i > $o ).
thf(tp_addressVal,type,
addressVal: $i > $i > $o ).
thf(tp_b000000000000000000,type,
b000000000000000000: $i > $o ).
thf(tp_b0000000000000000000000000000000000000000000000000000000000000000000,type,
b0000000000000000000000000000000000000000000000000000000000000000000: $i > $o ).
thf(tp_b000000011000110100000000011,type,
b000000011000110100000000011: $i > $o ).
thf(tp_b000000011100110100000000011,type,
b000000011100110100000000011: $i > $o ).
thf(tp_b0000001,type,
b0000001: $i > $o ).
thf(tp_b00001,type,
b00001: $i > $o ).
thf(tp_b0000_address_term,type,
b0000_address_term: $i ).
thf(tp_b0001001,type,
b0001001: $i > $o ).
thf(tp_b0001010,type,
b0001010: $i > $o ).
thf(tp_b0001_address_term,type,
b0001_address_term: $i ).
thf(tp_b001,type,
b001: $i > $o ).
thf(tp_b0010_address_term,type,
b0010_address_term: $i ).
thf(tp_b0011_address_term,type,
b0011_address_term: $i ).
thf(tp_b01,type,
b01: $i > $o ).
thf(tp_b010,type,
b010: $i > $o ).
thf(tp_b0100000,type,
b0100000: $i > $o ).
thf(tp_b0100001,type,
b0100001: $i > $o ).
thf(tp_b0100_address_term,type,
b0100_address_term: $i ).
thf(tp_b0101_address_term,type,
b0101_address_term: $i ).
thf(tp_b0110_address_term,type,
b0110_address_term: $i ).
thf(tp_b01111,type,
b01111: $i > $o ).
thf(tp_b0111_address_term,type,
b0111_address_term: $i ).
thf(tp_b10,type,
b10: $i > $o ).
thf(tp_b100,type,
b100: $i > $o ).
thf(tp_b10000,type,
b10000: $i > $o ).
thf(tp_b1000000,type,
b1000000: $i > $o ).
thf(tp_b1000_address_term,type,
b1000_address_term: $i ).
thf(tp_b1001010,type,
b1001010: $i > $o ).
thf(tp_b1001_address_term,type,
b1001_address_term: $i ).
thf(tp_b101,type,
b101: $i > $o ).
thf(tp_b1010000,type,
b1010000: $i > $o ).
thf(tp_b1010_address_term,type,
b1010_address_term: $i ).
thf(tp_b1011000,type,
b1011000: $i > $o ).
thf(tp_b1011_address_term,type,
b1011_address_term: $i ).
thf(tp_b1100000,type,
b1100000: $i > $o ).
thf(tp_b1100_address_term,type,
b1100_address_term: $i ).
thf(tp_b1101_address_term,type,
b1101_address_term: $i ).
thf(tp_b1110000,type,
b1110000: $i > $o ).
thf(tp_b1110_address_term,type,
b1110_address_term: $i ).
thf(tp_b1111000,type,
b1111000: $i > $o ).
thf(tp_b1111010,type,
b1111010: $i > $o ).
thf(tp_b1111_address_term,type,
b1111_address_term: $i ).
thf(tp_bitIndex0,type,
bitIndex0: $i ).
thf(tp_bitIndex1,type,
bitIndex1: $i ).
thf(tp_bitIndex10,type,
bitIndex10: $i ).
thf(tp_bitIndex11,type,
bitIndex11: $i ).
thf(tp_bitIndex12,type,
bitIndex12: $i ).
thf(tp_bitIndex13,type,
bitIndex13: $i ).
thf(tp_bitIndex14,type,
bitIndex14: $i ).
thf(tp_bitIndex15,type,
bitIndex15: $i ).
thf(tp_bitIndex16,type,
bitIndex16: $i ).
thf(tp_bitIndex17,type,
bitIndex17: $i ).
thf(tp_bitIndex18,type,
bitIndex18: $i ).
thf(tp_bitIndex19,type,
bitIndex19: $i ).
thf(tp_bitIndex2,type,
bitIndex2: $i ).
thf(tp_bitIndex20,type,
bitIndex20: $i ).
thf(tp_bitIndex21,type,
bitIndex21: $i ).
thf(tp_bitIndex22,type,
bitIndex22: $i ).
thf(tp_bitIndex23,type,
bitIndex23: $i ).
thf(tp_bitIndex24,type,
bitIndex24: $i ).
thf(tp_bitIndex25,type,
bitIndex25: $i ).
thf(tp_bitIndex26,type,
bitIndex26: $i ).
thf(tp_bitIndex27,type,
bitIndex27: $i ).
thf(tp_bitIndex28,type,
bitIndex28: $i ).
thf(tp_bitIndex29,type,
bitIndex29: $i ).
thf(tp_bitIndex3,type,
bitIndex3: $i ).
thf(tp_bitIndex30,type,
bitIndex30: $i ).
thf(tp_bitIndex31,type,
bitIndex31: $i ).
thf(tp_bitIndex32,type,
bitIndex32: $i ).
thf(tp_bitIndex33,type,
bitIndex33: $i ).
thf(tp_bitIndex34,type,
bitIndex34: $i ).
thf(tp_bitIndex35,type,
bitIndex35: $i ).
thf(tp_bitIndex36,type,
bitIndex36: $i ).
thf(tp_bitIndex37,type,
bitIndex37: $i ).
thf(tp_bitIndex38,type,
bitIndex38: $i ).
thf(tp_bitIndex39,type,
bitIndex39: $i ).
thf(tp_bitIndex4,type,
bitIndex4: $i ).
thf(tp_bitIndex40,type,
bitIndex40: $i ).
thf(tp_bitIndex41,type,
bitIndex41: $i ).
thf(tp_bitIndex42,type,
bitIndex42: $i ).
thf(tp_bitIndex43,type,
bitIndex43: $i ).
thf(tp_bitIndex44,type,
bitIndex44: $i ).
thf(tp_bitIndex45,type,
bitIndex45: $i ).
thf(tp_bitIndex46,type,
bitIndex46: $i ).
thf(tp_bitIndex47,type,
bitIndex47: $i ).
thf(tp_bitIndex48,type,
bitIndex48: $i ).
thf(tp_bitIndex49,type,
bitIndex49: $i ).
thf(tp_bitIndex5,type,
bitIndex5: $i ).
thf(tp_bitIndex50,type,
bitIndex50: $i ).
thf(tp_bitIndex51,type,
bitIndex51: $i ).
thf(tp_bitIndex52,type,
bitIndex52: $i ).
thf(tp_bitIndex53,type,
bitIndex53: $i ).
thf(tp_bitIndex54,type,
bitIndex54: $i ).
thf(tp_bitIndex55,type,
bitIndex55: $i ).
thf(tp_bitIndex56,type,
bitIndex56: $i ).
thf(tp_bitIndex57,type,
bitIndex57: $i ).
thf(tp_bitIndex58,type,
bitIndex58: $i ).
thf(tp_bitIndex59,type,
bitIndex59: $i ).
thf(tp_bitIndex6,type,
bitIndex6: $i ).
thf(tp_bitIndex60,type,
bitIndex60: $i ).
thf(tp_bitIndex61,type,
bitIndex61: $i ).
thf(tp_bitIndex62,type,
bitIndex62: $i ).
thf(tp_bitIndex63,type,
bitIndex63: $i ).
thf(tp_bitIndex64,type,
bitIndex64: $i ).
thf(tp_bitIndex65,type,
bitIndex65: $i ).
thf(tp_bitIndex66,type,
bitIndex66: $i ).
thf(tp_bitIndex7,type,
bitIndex7: $i ).
thf(tp_bitIndex8,type,
bitIndex8: $i ).
thf(tp_bitIndex9,type,
bitIndex9: $i ).
thf(tp_constB0,type,
constB0: $i ).
thf(tp_constB1,type,
constB1: $i ).
thf(tp_constB10,type,
constB10: $i ).
thf(tp_constB11,type,
constB11: $i ).
thf(tp_constB12,type,
constB12: $i ).
thf(tp_constB13,type,
constB13: $i ).
thf(tp_constB14,type,
constB14: $i ).
thf(tp_constB15,type,
constB15: $i ).
thf(tp_constB16,type,
constB16: $i ).
thf(tp_constB17,type,
constB17: $i ).
thf(tp_constB18,type,
constB18: $i ).
thf(tp_constB19,type,
constB19: $i ).
thf(tp_constB2,type,
constB2: $i ).
thf(tp_constB20,type,
constB20: $i ).
thf(tp_constB3,type,
constB3: $i ).
thf(tp_constB4,type,
constB4: $i ).
thf(tp_constB5,type,
constB5: $i ).
thf(tp_constB6,type,
constB6: $i ).
thf(tp_constB7,type,
constB7: $i ).
thf(tp_constB8,type,
constB8: $i ).
thf(tp_constB9,type,
constB9: $i ).
thf(tp_nextState,type,
nextState: $i > $i > $o ).
thf(tp_range_10_0,type,
range_10_0: $i > $o ).
thf(tp_range_11_0,type,
range_11_0: $i > $o ).
thf(tp_range_13_0,type,
range_13_0: $i > $o ).
thf(tp_range_14_13,type,
range_14_13: $i > $o ).
thf(tp_range_15_0,type,
range_15_0: $i > $o ).
thf(tp_range_16_0,type,
range_16_0: $i > $o ).
thf(tp_range_17_0,type,
range_17_0: $i > $o ).
thf(tp_range_19_0,type,
range_19_0: $i > $o ).
thf(tp_range_1_0,type,
range_1_0: $i > $o ).
thf(tp_range_21_0,type,
range_21_0: $i > $o ).
thf(tp_range_23_0,type,
range_23_0: $i > $o ).
thf(tp_range_25_0,type,
range_25_0: $i > $o ).
thf(tp_range_26_0,type,
range_26_0: $i > $o ).
thf(tp_range_27_0,type,
range_27_0: $i > $o ).
thf(tp_range_29_0,type,
range_29_0: $i > $o ).
thf(tp_range_2_0,type,
range_2_0: $i > $o ).
thf(tp_range_2_1,type,
range_2_1: $i > $o ).
thf(tp_range_31_0,type,
range_31_0: $i > $o ).
thf(tp_range_33_0,type,
range_33_0: $i > $o ).
thf(tp_range_35_0,type,
range_35_0: $i > $o ).
thf(tp_range_37_0,type,
range_37_0: $i > $o ).
thf(tp_range_39_0,type,
range_39_0: $i > $o ).
thf(tp_range_3_0,type,
range_3_0: $i > $o ).
thf(tp_range_3_1,type,
range_3_1: $i > $o ).
thf(tp_range_4_0,type,
range_4_0: $i > $o ).
thf(tp_range_5_0,type,
range_5_0: $i > $o ).
thf(tp_range_60_54,type,
range_60_54: $i > $o ).
thf(tp_range_63_0,type,
range_63_0: $i > $o ).
thf(tp_range_66_0,type,
range_66_0: $i > $o ).
thf(tp_range_66_63,type,
range_66_63: $i > $o ).
thf(tp_range_6_0,type,
range_6_0: $i > $o ).
thf(tp_range_7_0,type,
range_7_0: $i > $o ).
thf(tp_range_8_5,type,
range_8_5: $i > $o ).
thf(tp_range_9_0,type,
range_9_0: $i > $o ).
thf(tp_reachableState,type,
reachableState: $i > $o ).
thf(tp_sP12_v3516_bitIndex6,type,
sP12_v3516_bitIndex6: $i > $o ).
thf(tp_sP13_aig_name,type,
sP13_aig_name: $i > $o ).
thf(tp_sP14_aig_name,type,
sP14_aig_name: $i > $o ).
thf(tp_sP15_aig_name,type,
sP15_aig_name: $i > $o ).
thf(tp_sP164_aig_name,type,
sP164_aig_name: $i > $o ).
thf(tp_sP167,type,
sP167: $i > $o ).
thf(tp_sP168,type,
sP168: $i > $o ).
thf(tp_sP169,type,
sP169: $i > $o ).
thf(tp_sP16_aig_name,type,
sP16_aig_name: $i > $o ).
thf(tp_sP170,type,
sP170: $i > $o ).
thf(tp_sP171,type,
sP171: $i > $o ).
thf(tp_sP172,type,
sP172: $i > $o ).
thf(tp_sP173,type,
sP173: $i > $o ).
thf(tp_sP174,type,
sP174: $i > $o ).
thf(tp_sP175,type,
sP175: $i > $o ).
thf(tp_sP176,type,
sP176: $i > $o ).
thf(tp_sP177,type,
sP177: $i > $o ).
thf(tp_sP178,type,
sP178: $i > $o ).
thf(tp_sP179,type,
sP179: $i > $o ).
thf(tp_sP17_aig_name,type,
sP17_aig_name: $i > $o ).
thf(tp_sP180,type,
sP180: $i > $o ).
thf(tp_sP181,type,
sP181: $i > $o ).
thf(tp_sP182,type,
sP182: $i > $o ).
thf(tp_sP183,type,
sP183: $i > $o ).
thf(tp_sP184,type,
sP184: $i > $o ).
thf(tp_sP185,type,
sP185: $i > $o ).
thf(tp_sP186,type,
sP186: $i > $o ).
thf(tp_sP187,type,
sP187: $i > $o ).
thf(tp_sP188,type,
sP188: $i > $o ).
thf(tp_sP189,type,
sP189: $i > $o ).
thf(tp_sP18_aig_name,type,
sP18_aig_name: $i > $o ).
thf(tp_sP190,type,
sP190: $i > $o ).
thf(tp_sP191,type,
sP191: $i > $o ).
thf(tp_sP192,type,
sP192: $i > $o ).
thf(tp_sP193,type,
sP193: $i > $o ).
thf(tp_sP194,type,
sP194: $i > $o ).
thf(tp_sP195,type,
sP195: $i > $o ).
thf(tp_sP196,type,
sP196: $i > $o ).
thf(tp_sP197,type,
sP197: $i > $o ).
thf(tp_sP198,type,
sP198: $i > $o ).
thf(tp_sP199,type,
sP199: $i > $i > $o ).
thf(tp_sP19_aig_name,type,
sP19_aig_name: $i > $o ).
thf(tp_sP200,type,
sP200: $i > $i > $o ).
thf(tp_sP201,type,
sP201: $i > $i > $o ).
thf(tp_sP202,type,
sP202: $i > $i > $o ).
thf(tp_sP203,type,
sP203: $i > $i > $o ).
thf(tp_sP204,type,
sP204: $i > $i > $o ).
thf(tp_sP205,type,
sP205: $i > $o ).
thf(tp_sP206,type,
sP206: $i > $o ).
thf(tp_sP207,type,
sP207: $i > $o ).
thf(tp_sP208,type,
sP208: $i > $i > $o ).
thf(tp_sP209,type,
sP209: $i > $o ).
thf(tp_sP20_aig_name,type,
sP20_aig_name: $i > $o ).
thf(tp_sP210,type,
sP210: $i > $o ).
thf(tp_sP211,type,
sP211: $i > $o ).
thf(tp_sP212,type,
sP212: $i > $o ).
thf(tp_sP213,type,
sP213: $i > $o ).
thf(tp_sP214,type,
sP214: $i > $o ).
thf(tp_sP215,type,
sP215: $i > $o ).
thf(tp_sP216,type,
sP216: $i > $o ).
thf(tp_sP217,type,
sP217: $i > $o ).
thf(tp_sP218,type,
sP218: $i > $o ).
thf(tp_sP219,type,
sP219: $i > $o ).
thf(tp_sP21_aig_name,type,
sP21_aig_name: $i > $o ).
thf(tp_sP220,type,
sP220: $i > $o ).
thf(tp_sP221,type,
sP221: $i > $o ).
thf(tp_sP222,type,
sP222: $i > $o ).
thf(tp_sP223,type,
sP223: $i > $o ).
thf(tp_sP224,type,
sP224: $i > $o ).
thf(tp_sP225,type,
sP225: $i > $o ).
thf(tp_sP226,type,
sP226: $i > $o ).
thf(tp_sP227,type,
sP227: $i > $o ).
thf(tp_sP228,type,
sP228: $i > $o ).
thf(tp_sP229,type,
sP229: $i > $o ).
thf(tp_sP22_aig_name,type,
sP22_aig_name: $i > $o ).
thf(tp_sP230,type,
sP230: $i > $i > $o ).
thf(tp_sP231,type,
sP231: $i > $o ).
thf(tp_sP232,type,
sP232: $i > $o ).
thf(tp_sP233,type,
sP233: $i > $i > $o ).
thf(tp_sP234,type,
sP234: $i > $o ).
thf(tp_sP235,type,
sP235: $i > $o ).
thf(tp_sP236,type,
sP236: $i > $o ).
thf(tp_sP237,type,
sP237: $i > $o ).
thf(tp_sP238,type,
sP238: $i > $o ).
thf(tp_sP239,type,
sP239: $i > $o ).
thf(tp_sP23_aig_name,type,
sP23_aig_name: $i > $o ).
thf(tp_sP240,type,
sP240: $i > $o ).
thf(tp_sP241,type,
sP241: $i > $o ).
thf(tp_sP242,type,
sP242: $i > $o ).
thf(tp_sP243,type,
sP243: $i > $o ).
thf(tp_sP244,type,
sP244: $i > $o ).
thf(tp_sP245,type,
sP245: $i > $o ).
thf(tp_sP246,type,
sP246: $i > $o ).
thf(tp_sP247,type,
sP247: $i > $o ).
thf(tp_sP248,type,
sP248: $i > $o ).
thf(tp_sP249,type,
sP249: $i > $o ).
thf(tp_sP24_aig_name,type,
sP24_aig_name: $i > $o ).
thf(tp_sP250,type,
sP250: $i > $o ).
thf(tp_sP251,type,
sP251: $i > $o ).
thf(tp_sP252,type,
sP252: $i > $o ).
thf(tp_sP253,type,
sP253: $i > $o ).
thf(tp_sP254,type,
sP254: $i > $o ).
thf(tp_sP255,type,
sP255: $i > $o ).
thf(tp_sP256,type,
sP256: $i > $o ).
thf(tp_sP257,type,
sP257: $i > $o ).
thf(tp_sP258,type,
sP258: $i > $o ).
thf(tp_sP259,type,
sP259: $i > $o ).
thf(tp_sP25_aig_name,type,
sP25_aig_name: $i > $o ).
thf(tp_sP260,type,
sP260: $i > $o ).
thf(tp_sP261,type,
sP261: $i > $o ).
thf(tp_sP262,type,
sP262: $i > $o ).
thf(tp_sP263,type,
sP263: $i > $o ).
thf(tp_sP264,type,
sP264: $i > $o ).
thf(tp_sP265,type,
sP265: $i > $o ).
thf(tp_sP266,type,
sP266: $i > $o ).
thf(tp_sP267,type,
sP267: $i > $o ).
thf(tp_sP268,type,
sP268: $i > $o ).
thf(tp_sP269,type,
sP269: $i > $o ).
thf(tp_sP26_aig_name,type,
sP26_aig_name: $i > $o ).
thf(tp_sP270,type,
sP270: $i > $o ).
thf(tp_sP271,type,
sP271: $i > $o ).
thf(tp_sP272,type,
sP272: $i > $o ).
thf(tp_sP273,type,
sP273: $i > $o ).
thf(tp_sP274,type,
sP274: $i > $o ).
thf(tp_sP275,type,
sP275: $i > $o ).
thf(tp_sP276,type,
sP276: $i > $o ).
thf(tp_sP277,type,
sP277: $i > $o ).
thf(tp_sP278,type,
sP278: $i > $o ).
thf(tp_sP279,type,
sP279: $i > $o ).
thf(tp_sP27_aig_name,type,
sP27_aig_name: $i > $o ).
thf(tp_sP280,type,
sP280: $i > $o ).
thf(tp_sP281,type,
sP281: $i > $o ).
thf(tp_sP282,type,
sP282: $i > $i > $o ).
thf(tp_sP283,type,
sP283: $i > $o ).
thf(tp_sP284,type,
sP284: $i > $o ).
thf(tp_sP285,type,
sP285: $i > $o ).
thf(tp_sP286,type,
sP286: $i > $o ).
thf(tp_sP287,type,
sP287: $i > $o ).
thf(tp_sP288,type,
sP288: $i > $o ).
thf(tp_sP289,type,
sP289: $i > $o ).
thf(tp_sP28_aig_name,type,
sP28_aig_name: $i > $o ).
thf(tp_sP290,type,
sP290: $i > $o ).
thf(tp_sP291,type,
sP291: $i > $o ).
thf(tp_sP292,type,
sP292: $i > $o ).
thf(tp_sP293,type,
sP293: $i > $o ).
thf(tp_sP294,type,
sP294: $i > $o ).
thf(tp_sP295,type,
sP295: $i > $i > $o ).
thf(tp_sP296,type,
sP296: $i > $o ).
thf(tp_sP29_aig_name,type,
sP29_aig_name: $i > $o ).
thf(tp_sP2_v364_bitIndex8,type,
sP2_v364_bitIndex8: $i > $o ).
thf(tp_sP30_aig_name,type,
sP30_aig_name: $i > $o ).
thf(tp_sP31_aig_name,type,
sP31_aig_name: $i > $o ).
thf(tp_sP32_aig_name,type,
sP32_aig_name: $i > $o ).
thf(tp_sP33_aig_name,type,
sP33_aig_name: $i > $o ).
thf(tp_sP37_aig_name,type,
sP37_aig_name: $i > $o ).
thf(tp_sP38_aig_name,type,
sP38_aig_name: $i > $o ).
thf(tp_sP39_aig_name,type,
sP39_aig_name: $i > $o ).
thf(tp_sP40_aig_name,type,
sP40_aig_name: $i > $o ).
thf(tp_sP41_aig_name,type,
sP41_aig_name: $i > $o ).
thf(tp_sP42_aig_name,type,
sP42_aig_name: $i > $o ).
thf(tp_sP43_aig_name,type,
sP43_aig_name: $i > $o ).
thf(tp_sP44_aig_name,type,
sP44_aig_name: $i > $o ).
thf(tp_sP45_aig_name,type,
sP45_aig_name: $i > $o ).
thf(tp_sP46_aig_name,type,
sP46_aig_name: $i > $o ).
thf(tp_sP47_aig_name,type,
sP47_aig_name: $i > $o ).
thf(tp_sP48_aig_name,type,
sP48_aig_name: $i > $o ).
thf(tp_sP49_aig_name,type,
sP49_aig_name: $i > $o ).
thf(tp_sP50_aig_name,type,
sP50_aig_name: $i > $o ).
thf(tp_v1,type,
v1: $i > $o ).
thf(tp_v1004,type,
v1004: $i > $o ).
thf(tp_v1009,type,
v1009: $i > $o ).
thf(tp_v1010,type,
v1010: $i > $o ).
thf(tp_v1012,type,
v1012: $i > $o ).
thf(tp_v1015,type,
v1015: $i > $o ).
thf(tp_v1017,type,
v1017: $i > $i > $o ).
thf(tp_v1019,type,
v1019: $i > $i > $o ).
thf(tp_v1019_range_3_to_0_address_association,type,
v1019_range_3_to_0_address_association: $i > $i > $o ).
thf(tp_v1019_range_3_to_0_address_term_bound_0,type,
v1019_range_3_to_0_address_term_bound_0: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_1,type,
v1019_range_3_to_0_address_term_bound_1: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_10,type,
v1019_range_3_to_0_address_term_bound_10: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_11,type,
v1019_range_3_to_0_address_term_bound_11: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_12,type,
v1019_range_3_to_0_address_term_bound_12: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_13,type,
v1019_range_3_to_0_address_term_bound_13: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_14,type,
v1019_range_3_to_0_address_term_bound_14: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_15,type,
v1019_range_3_to_0_address_term_bound_15: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_16,type,
v1019_range_3_to_0_address_term_bound_16: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_17,type,
v1019_range_3_to_0_address_term_bound_17: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_18,type,
v1019_range_3_to_0_address_term_bound_18: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_19,type,
v1019_range_3_to_0_address_term_bound_19: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_2,type,
v1019_range_3_to_0_address_term_bound_2: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_20,type,
v1019_range_3_to_0_address_term_bound_20: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_3,type,
v1019_range_3_to_0_address_term_bound_3: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_4,type,
v1019_range_3_to_0_address_term_bound_4: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_5,type,
v1019_range_3_to_0_address_term_bound_5: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_6,type,
v1019_range_3_to_0_address_term_bound_6: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_7,type,
v1019_range_3_to_0_address_term_bound_7: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_8,type,
v1019_range_3_to_0_address_term_bound_8: $i ).
thf(tp_v1019_range_3_to_0_address_term_bound_9,type,
v1019_range_3_to_0_address_term_bound_9: $i ).
thf(tp_v1021,type,
v1021: $i > $i > $o ).
thf(tp_v1037,type,
v1037: $i > $i > $o ).
thf(tp_v1039,type,
v1039: $i > $i > $o ).
thf(tp_v1042,type,
v1042: $i > $o ).
thf(tp_v1043,type,
v1043: $i > $i > $o ).
thf(tp_v1044,type,
v1044: $i > $o ).
thf(tp_v1045,type,
v1045: $i > $i > $o ).
thf(tp_v1046,type,
v1046: $i > $i > $o ).
thf(tp_v1047,type,
v1047: $i > $o ).
thf(tp_v1048,type,
v1048: $i > $i > $o ).
thf(tp_v1049,type,
v1049: $i > $i > $o ).
thf(tp_v1054,type,
v1054: $i > $o ).
thf(tp_v1055,type,
v1055: $i > $i > $o ).
thf(tp_v1057,type,
v1057: $i > $o ).
thf(tp_v1059,type,
v1059: $i > $o ).
thf(tp_v1061,type,
v1061: $i > $o ).
thf(tp_v1085,type,
v1085: $i > $o ).
thf(tp_v1086,type,
v1086: $i > $i > $o ).
thf(tp_v1087,type,
v1087: $i > $i > $o ).
thf(tp_v1088,type,
v1088: $i > $o ).
thf(tp_v1089,type,
v1089: $i > $i > $o ).
thf(tp_v109,type,
v109: $i > $i > $o ).
thf(tp_v1094,type,
v1094: $i > $o ).
thf(tp_v1095,type,
v1095: $i > $o ).
thf(tp_v1096,type,
v1096: $i > $o ).
thf(tp_v111,type,
v111: $i > $i > $o ).
thf(tp_v1115,type,
v1115: $i > $i > $o ).
thf(tp_v1118,type,
v1118: $i > $o ).
thf(tp_v1119,type,
v1119: $i > $o ).
thf(tp_v1120,type,
v1120: $i > $o ).
thf(tp_v1124,type,
v1124: $i > $i > $o ).
thf(tp_v1126,type,
v1126: $i > $i > $o ).
thf(tp_v1142,type,
v1142: $i > $i > $o ).
thf(tp_v1196,type,
v1196: $i > $o ).
thf(tp_v1202,type,
v1202: $i > $o ).
thf(tp_v1204,type,
v1204: $i > $i > $o ).
thf(tp_v1206,type,
v1206: $i > $i > $o ).
thf(tp_v1218,type,
v1218: $i > $o ).
thf(tp_v1222,type,
v1222: $i > $i > $o ).
thf(tp_v1233,type,
v1233: $i > $o ).
thf(tp_v1242,type,
v1242: $i > $i > $o ).
thf(tp_v1243,type,
v1243: $i > $o ).
thf(tp_v1244,type,
v1244: $i > $o ).
thf(tp_v1245,type,
v1245: $i > $o ).
thf(tp_v1247,type,
v1247: $i > $o ).
thf(tp_v1251,type,
v1251: $i > $i > $o ).
thf(tp_v1253,type,
v1253: $i > $i > $o ).
thf(tp_v1258,type,
v1258: $i > $i > $o ).
thf(tp_v1259,type,
v1259: $i > $o ).
thf(tp_v1260,type,
v1260: $i > $o ).
thf(tp_v1262,type,
v1262: $i > $o ).
thf(tp_v1266,type,
v1266: $i > $i > $o ).
thf(tp_v1267,type,
v1267: $i > $o ).
thf(tp_v1268,type,
v1268: $i > $o ).
thf(tp_v1270,type,
v1270: $i > $o ).
thf(tp_v1274,type,
v1274: $i > $o ).
thf(tp_v1280,type,
v1280: $i > $i > $o ).
thf(tp_v1281,type,
v1281: $i > $o ).
thf(tp_v1282,type,
v1282: $i > $o ).
thf(tp_v1284,type,
v1284: $i > $o ).
thf(tp_v1288,type,
v1288: $i > $i > $o ).
thf(tp_v1289,type,
v1289: $i > $o ).
thf(tp_v1290,type,
v1290: $i > $o ).
thf(tp_v1292,type,
v1292: $i > $o ).
thf(tp_v1296,type,
v1296: $i > $o ).
thf(tp_v1302,type,
v1302: $i > $i > $o ).
thf(tp_v1303,type,
v1303: $i > $o ).
thf(tp_v1304,type,
v1304: $i > $o ).
thf(tp_v1306,type,
v1306: $i > $o ).
thf(tp_v1311,type,
v1311: $i > $o ).
thf(tp_v1325,type,
v1325: $i > $i > $o ).
thf(tp_v1326,type,
v1326: $i > $o ).
thf(tp_v1327,type,
v1327: $i > $o ).
thf(tp_v1329,type,
v1329: $i > $o ).
thf(tp_v1333,type,
v1333: $i > $o ).
thf(tp_v135,type,
v135: $i > $i > $o ).
thf(tp_v1372,type,
v1372: $i > $i > $o ).
thf(tp_v1377,type,
v1377: $i > $i > $o ).
thf(tp_v1384,type,
v1384: $i > $o ).
thf(tp_v1404,type,
v1404: $i > $i > $o ).
thf(tp_v1405,type,
v1405: $i > $o ).
thf(tp_v1406,type,
v1406: $i > $o ).
thf(tp_v1407,type,
v1407: $i > $o ).
thf(tp_v1409,type,
v1409: $i > $o ).
thf(tp_v1413,type,
v1413: $i > $i > $o ).
thf(tp_v1415,type,
v1415: $i > $i > $o ).
thf(tp_v1421,type,
v1421: $i > $o ).
thf(tp_v1427,type,
v1427: $i > $i > $o ).
thf(tp_v1428,type,
v1428: $i > $o ).
thf(tp_v1429,type,
v1429: $i > $o ).
thf(tp_v143,type,
v143: $i > $o ).
thf(tp_v1431,type,
v1431: $i > $o ).
thf(tp_v1435,type,
v1435: $i > $o ).
thf(tp_v1449,type,
v1449: $i > $i > $o ).
thf(tp_v145,type,
v145: $i > $i > $o ).
thf(tp_v1450,type,
v1450: $i > $o ).
thf(tp_v1451,type,
v1451: $i > $o ).
thf(tp_v1453,type,
v1453: $i > $o ).
thf(tp_v1457,type,
v1457: $i > $o ).
thf(tp_v1462,type,
v1462: $i > $i > $o ).
thf(tp_v1463,type,
v1463: $i > $o ).
thf(tp_v1464,type,
v1464: $i > $o ).
thf(tp_v1466,type,
v1466: $i > $o ).
thf(tp_v147,type,
v147: $i > $i > $o ).
thf(tp_v1470,type,
v1470: $i > $o ).
thf(tp_v1482,type,
v1482: $i > $o ).
thf(tp_v1483,type,
v1483: $i > $o ).
thf(tp_v1484,type,
v1484: $i > $o ).
thf(tp_v1488,type,
v1488: $i > $o ).
thf(tp_v149,type,
v149: $i > $i > $o ).
thf(tp_v1490,type,
v1490: $i > $o ).
thf(tp_v1492,type,
v1492: $i > $o ).
thf(tp_v1507,type,
v1507: $i > $i > $o ).
thf(tp_v151,type,
v151: $i > $i > $o ).
thf(tp_v1512,type,
v1512: $i > $o ).
thf(tp_v1513,type,
v1513: $i > $o ).
thf(tp_v1514,type,
v1514: $i > $o ).
thf(tp_v1520,type,
v1520: $i > $o ).
thf(tp_v1527,type,
v1527: $i > $i > $o ).
thf(tp_v1529,type,
v1529: $i > $i > $o ).
thf(tp_v1530,type,
v1530: $i > $i > $o ).
thf(tp_v1536,type,
v1536: $i > $o ).
thf(tp_v1545,type,
v1545: $i > $o ).
thf(tp_v1546,type,
v1546: $i > $o ).
thf(tp_v1547,type,
v1547: $i > $o ).
thf(tp_v1549,type,
v1549: $i > $o ).
thf(tp_v1553,type,
v1553: $i > $o ).
thf(tp_v1555,type,
v1555: $i > $o ).
thf(tp_v156,type,
v156: $i > $i > $o ).
thf(tp_v1563,type,
v1563: $i > $o ).
thf(tp_v1564,type,
v1564: $i > $i > $o ).
thf(tp_v1565,type,
v1565: $i > $o ).
thf(tp_v1574,type,
v1574: $i > $i > $o ).
thf(tp_v1576,type,
v1576: $i > $o ).
thf(tp_v1585,type,
v1585: $i > $i > $o ).
thf(tp_v1589,type,
v1589: $i > $o ).
thf(tp_v1590,type,
v1590: $i > $o ).
thf(tp_v1591,type,
v1591: $i > $o ).
thf(tp_v1595,type,
v1595: $i > $i > $o ).
thf(tp_v1597,type,
v1597: $i > $i > $o ).
thf(tp_v160,type,
v160: $i > $i > $o ).
thf(tp_v1602,type,
v1602: $i > $o ).
thf(tp_v1626,type,
v1626: $i > $o ).
thf(tp_v1627,type,
v1627: $i > $o ).
thf(tp_v1643,type,
v1643: $i > $o ).
thf(tp_v1644,type,
v1644: $i > $o ).
thf(tp_v1645,type,
v1645: $i > $o ).
thf(tp_v1649,type,
v1649: $i > $o ).
thf(tp_v1651,type,
v1651: $i > $o ).
thf(tp_v1660,type,
v1660: $i > $o ).
thf(tp_v167,type,
v167: $i > $o ).
thf(tp_v170,type,
v170: $i > $o ).
thf(tp_v1717,type,
v1717: $i > $o ).
thf(tp_v1718,type,
v1718: $i > $o ).
thf(tp_v1720,type,
v1720: $i > $o ).
thf(tp_v1723,type,
v1723: $i > $o ).
thf(tp_v1725,type,
v1725: $i > $o ).
thf(tp_v1730,type,
v1730: $i > $o ).
thf(tp_v1753,type,
v1753: $i > $i > $o ).
thf(tp_v1754,type,
v1754: $i > $o ).
thf(tp_v1755,type,
v1755: $i > $o ).
thf(tp_v1757,type,
v1757: $i > $o ).
thf(tp_v1764,type,
v1764: $i > $i > $o ).
thf(tp_v1765,type,
v1765: $i > $o ).
thf(tp_v1766,type,
v1766: $i > $i > $o ).
thf(tp_v1771,type,
v1771: $i > $o ).
thf(tp_v1772,type,
v1772: $i > $o ).
thf(tp_v1787,type,
v1787: $i > $o ).
thf(tp_v1788,type,
v1788: $i > $o ).
thf(tp_v1790,type,
v1790: $i > $o ).
thf(tp_v1793,type,
v1793: $i > $i > $o ).
thf(tp_v1795,type,
v1795: $i > $i > $o ).
thf(tp_v18,type,
v18: $i > $o ).
thf(tp_v1805,type,
v1805: $i > $o ).
thf(tp_v1823,type,
v1823: $i > $i > $o ).
thf(tp_v1824,type,
v1824: $i > $o ).
thf(tp_v1825,type,
v1825: $i > $o ).
thf(tp_v1827,type,
v1827: $i > $o ).
thf(tp_v1831,type,
v1831: $i > $o ).
thf(tp_v184,type,
v184: $i > $i > $o ).
thf(tp_v1846,type,
v1846: $i > $i > $o ).
thf(tp_v1847,type,
v1847: $i > $o ).
thf(tp_v1848,type,
v1848: $i > $i > $o ).
thf(tp_v1853,type,
v1853: $i > $o ).
thf(tp_v1854,type,
v1854: $i > $o ).
thf(tp_v1869,type,
v1869: $i > $o ).
thf(tp_v1870,type,
v1870: $i > $o ).
thf(tp_v1872,type,
v1872: $i > $o ).
thf(tp_v1875,type,
v1875: $i > $i > $o ).
thf(tp_v1877,type,
v1877: $i > $i > $o ).
thf(tp_v1887,type,
v1887: $i > $o ).
thf(tp_v1888,type,
v1888: $i > $o ).
thf(tp_v1889,type,
v1889: $i > $o ).
thf(tp_v1891,type,
v1891: $i > $o ).
thf(tp_v1897,type,
v1897: $i > $o ).
thf(tp_v1901,type,
v1901: $i > $o ).
thf(tp_v1903,type,
v1903: $i > $o ).
thf(tp_v1904,type,
v1904: $i > $o ).
thf(tp_v1918,type,
v1918: $i > $i > $o ).
thf(tp_v1920,type,
v1920: $i > $i > $o ).
thf(tp_v1922,type,
v1922: $i > $i > $o ).
thf(tp_v1924,type,
v1924: $i > $i > $o ).
thf(tp_v1926,type,
v1926: $i > $i > $o ).
thf(tp_v1928,type,
v1928: $i > $i > $o ).
thf(tp_v1966,type,
v1966: $i > $i > $o ).
thf(tp_v1968,type,
v1968: $i > $i > $o ).
thf(tp_v1970,type,
v1970: $i > $i > $o ).
thf(tp_v1972,type,
v1972: $i > $i > $o ).
thf(tp_v1974,type,
v1974: $i > $i > $o ).
thf(tp_v1976,type,
v1976: $i > $i > $o ).
thf(tp_v1978,type,
v1978: $i > $i > $o ).
thf(tp_v1980,type,
v1980: $i > $i > $o ).
thf(tp_v1982,type,
v1982: $i > $i > $o ).
thf(tp_v1987,type,
v1987: $i > $i > $o ).
thf(tp_v1989,type,
v1989: $i > $i > $o ).
thf(tp_v1991,type,
v1991: $i > $i > $o ).
thf(tp_v1993,type,
v1993: $i > $i > $o ).
thf(tp_v1995,type,
v1995: $i > $i > $o ).
thf(tp_v1997,type,
v1997: $i > $i > $o ).
thf(tp_v1999,type,
v1999: $i > $i > $o ).
thf(tp_v200,type,
v200: $i > $o ).
thf(tp_v2001,type,
v2001: $i > $i > $o ).
thf(tp_v2003,type,
v2003: $i > $i > $o ).
thf(tp_v2005,type,
v2005: $i > $i > $o ).
thf(tp_v2007,type,
v2007: $i > $i > $o ).
thf(tp_v2009,type,
v2009: $i > $i > $o ).
thf(tp_v201,type,
v201: $i > $o ).
thf(tp_v202,type,
v202: $i > $o ).
thf(tp_v2023,type,
v2023: $i > $i > $o ).
thf(tp_v2024,type,
v2024: $i > $o ).
thf(tp_v2025,type,
v2025: $i > $o ).
thf(tp_v2026,type,
v2026: $i > $o ).
thf(tp_v2028,type,
v2028: $i > $o ).
thf(tp_v2032,type,
v2032: $i > $i > $o ).
thf(tp_v2034,type,
v2034: $i > $i > $o ).
thf(tp_v204,type,
v204: $i > $o ).
thf(tp_v2061,type,
v2061: $i > $o ).
thf(tp_v2063,type,
v2063: $i > $o ).
thf(tp_v2065,type,
v2065: $i > $o ).
thf(tp_v208,type,
v208: $i > $o ).
thf(tp_v2089,type,
v2089: $i > $o ).
thf(tp_v2099,type,
v2099: $i > $o ).
thf(tp_v21,type,
v21: $i > $i > $o ).
thf(tp_v210,type,
v210: $i > $o ).
thf(tp_v2123,type,
v2123: $i > $i > $o ).
thf(tp_v2129,type,
v2129: $i > $o ).
thf(tp_v2136,type,
v2136: $i > $o ).
thf(tp_v2137,type,
v2137: $i > $o ).
thf(tp_v2138,type,
v2138: $i > $o ).
thf(tp_v2142,type,
v2142: $i > $o ).
thf(tp_v2144,type,
v2144: $i > $o ).
thf(tp_v2163,type,
v2163: $i > $o ).
thf(tp_v2187,type,
v2187: $i > $o ).
thf(tp_v2190,type,
v2190: $i > $o ).
thf(tp_v2191,type,
v2191: $i > $o ).
thf(tp_v2193,type,
v2193: $i > $o ).
thf(tp_v2196,type,
v2196: $i > $o ).
thf(tp_v2198,type,
v2198: $i > $o ).
thf(tp_v2214,type,
v2214: $i > $o ).
thf(tp_v2215,type,
v2215: $i > $o ).
thf(tp_v2216,type,
v2216: $i > $o ).
thf(tp_v2218,type,
v2218: $i > $o ).
thf(tp_v2224,type,
v2224: $i > $o ).
thf(tp_v223,type,
v223: $i > $o ).
thf(tp_v2231,type,
v2231: $i > $i > $o ).
thf(tp_v224,type,
v224: $i > $i > $o ).
thf(tp_v2247,type,
v2247: $i > $o ).
thf(tp_v2249,type,
v2249: $i > $o ).
thf(tp_v225,type,
v225: $i > $o ).
thf(tp_v2250,type,
v2250: $i > $o ).
thf(tp_v2252,type,
v2252: $i > $o ).
thf(tp_v2255,type,
v2255: $i > $o ).
thf(tp_v226,type,
v226: $i > $i > $o ).
thf(tp_v2261,type,
v2261: $i > $i > $o ).
thf(tp_v2263,type,
v2263: $i > $i > $o ).
thf(tp_v2265,type,
v2265: $i > $o ).
thf(tp_v227,type,
v227: $i > $i > $o ).
thf(tp_v2275,type,
v2275: $i > $o ).
thf(tp_v228,type,
v228: $i > $o ).
thf(tp_v229,type,
v229: $i > $i > $o ).
thf(tp_v2290,type,
v2290: $i > $i > $o ).
thf(tp_v2292,type,
v2292: $i > $o ).
thf(tp_v230,type,
v230: $i > $i > $o ).
thf(tp_v2300,type,
v2300: $i > $o ).
thf(tp_v2302,type,
v2302: $i > $i > $o ).
thf(tp_v2306,type,
v2306: $i > $i > $o ).
thf(tp_v2308,type,
v2308: $i > $i > $o ).
thf(tp_v2318,type,
v2318: $i > $o ).
thf(tp_v2322,type,
v2322: $i > $o ).
thf(tp_v2324,type,
v2324: $i > $o ).
thf(tp_v2326,type,
v2326: $i > $o ).
thf(tp_v2335,type,
v2335: $i > $i > $o ).
thf(tp_v2338,type,
v2338: $i > $i > $o ).
thf(tp_v235,type,
v235: $i > $o ).
thf(tp_v236,type,
v236: $i > $i > $o ).
thf(tp_v2361,type,
v2361: $i > $o ).
thf(tp_v2363,type,
v2363: $i > $o ).
thf(tp_v2371,type,
v2371: $i > $i > $o ).
thf(tp_v239,type,
v239: $i > $o ).
thf(tp_v2394,type,
v2394: $i > $i > $o ).
thf(tp_v2397,type,
v2397: $i > $i > $o ).
thf(tp_v2399,type,
v2399: $i > $o ).
thf(tp_v2406,type,
v2406: $i > $o ).
thf(tp_v2409,type,
v2409: $i > $o ).
thf(tp_v241,type,
v241: $i > $o ).
thf(tp_v2412,type,
v2412: $i > $o ).
thf(tp_v2432,type,
v2432: $i > $o ).
thf(tp_v2447,type,
v2447: $i > $i > $o ).
thf(tp_v2449,type,
v2449: $i > $i > $o ).
thf(tp_v2451,type,
v2451: $i > $i > $o ).
thf(tp_v2453,type,
v2453: $i > $i > $o ).
thf(tp_v2454,type,
v2454: $i > $i > $o ).
thf(tp_v2456,type,
v2456: $i > $i > $o ).
thf(tp_v2457,type,
v2457: $i > $i > $o ).
thf(tp_v2458,type,
v2458: $i > $i > $o ).
thf(tp_v2459,type,
v2459: $i > $i > $o ).
thf(tp_v2460,type,
v2460: $i > $i > $o ).
thf(tp_v2461,type,
v2461: $i > $i > $o ).
thf(tp_v2462,type,
v2462: $i > $i > $o ).
thf(tp_v2463,type,
v2463: $i > $i > $o ).
thf(tp_v2464,type,
v2464: $i > $i > $o ).
thf(tp_v2465,type,
v2465: $i > $i > $o ).
thf(tp_v2467,type,
v2467: $i > $i > $o ).
thf(tp_v2469,type,
v2469: $i > $i > $o ).
thf(tp_v2470,type,
v2470: $i > $i > $o ).
thf(tp_v2471,type,
v2471: $i > $i > $o ).
thf(tp_v2472,type,
v2472: $i > $i > $o ).
thf(tp_v2474,type,
v2474: $i > $i > $o ).
thf(tp_v2475,type,
v2475: $i > $i > $o ).
thf(tp_v2476,type,
v2476: $i > $i > $o ).
thf(tp_v2477,type,
v2477: $i > $i > $o ).
thf(tp_v2478,type,
v2478: $i > $i > $o ).
thf(tp_v2479,type,
v2479: $i > $i > $o ).
thf(tp_v2480,type,
v2480: $i > $i > $o ).
thf(tp_v2481,type,
v2481: $i > $i > $o ).
thf(tp_v2482,type,
v2482: $i > $i > $o ).
thf(tp_v2483,type,
v2483: $i > $i > $o ).
thf(tp_v2485,type,
v2485: $i > $i > $o ).
thf(tp_v2486,type,
v2486: $i > $i > $o ).
thf(tp_v2487,type,
v2487: $i > $i > $o ).
thf(tp_v2488,type,
v2488: $i > $i > $o ).
thf(tp_v2489,type,
v2489: $i > $i > $o ).
thf(tp_v2490,type,
v2490: $i > $i > $o ).
thf(tp_v2491,type,
v2491: $i > $i > $o ).
thf(tp_v2492,type,
v2492: $i > $i > $o ).
thf(tp_v2493,type,
v2493: $i > $i > $o ).
thf(tp_v2494,type,
v2494: $i > $i > $o ).
thf(tp_v2495,type,
v2495: $i > $i > $o ).
thf(tp_v2496,type,
v2496: $i > $i > $o ).
thf(tp_v2497,type,
v2497: $i > $i > $o ).
thf(tp_v2498,type,
v2498: $i > $i > $o ).
thf(tp_v2499,type,
v2499: $i > $i > $o ).
thf(tp_v2500,type,
v2500: $i > $i > $o ).
thf(tp_v2501,type,
v2501: $i > $i > $o ).
thf(tp_v2502,type,
v2502: $i > $i > $o ).
thf(tp_v2503,type,
v2503: $i > $i > $o ).
thf(tp_v2504,type,
v2504: $i > $i > $o ).
thf(tp_v2505,type,
v2505: $i > $i > $o ).
thf(tp_v2506,type,
v2506: $i > $i > $o ).
thf(tp_v2508,type,
v2508: $i > $i > $o ).
thf(tp_v2509,type,
v2509: $i > $i > $o ).
thf(tp_v2511,type,
v2511: $i > $i > $o ).
thf(tp_v2512,type,
v2512: $i > $i > $o ).
thf(tp_v2513,type,
v2513: $i > $i > $o ).
thf(tp_v2514,type,
v2514: $i > $i > $o ).
thf(tp_v2515,type,
v2515: $i > $i > $o ).
thf(tp_v2516,type,
v2516: $i > $i > $o ).
thf(tp_v2517,type,
v2517: $i > $i > $o ).
thf(tp_v2518,type,
v2518: $i > $i > $o ).
thf(tp_v2519,type,
v2519: $i > $i > $o ).
thf(tp_v2520,type,
v2520: $i > $i > $o ).
thf(tp_v2521,type,
v2521: $i > $i > $o ).
thf(tp_v2522,type,
v2522: $i > $i > $o ).
thf(tp_v2523,type,
v2523: $i > $i > $o ).
thf(tp_v2524,type,
v2524: $i > $i > $o ).
thf(tp_v2525,type,
v2525: $i > $i > $o ).
thf(tp_v2526,type,
v2526: $i > $i > $o ).
thf(tp_v2527,type,
v2527: $i > $i > $o ).
thf(tp_v2528,type,
v2528: $i > $i > $o ).
thf(tp_v2529,type,
v2529: $i > $i > $o ).
thf(tp_v2530,type,
v2530: $i > $i > $o ).
thf(tp_v2531,type,
v2531: $i > $i > $o ).
thf(tp_v2532,type,
v2532: $i > $i > $o ).
thf(tp_v2533,type,
v2533: $i > $i > $o ).
thf(tp_v2534,type,
v2534: $i > $i > $o ).
thf(tp_v2535,type,
v2535: $i > $i > $o ).
thf(tp_v2536,type,
v2536: $i > $i > $o ).
thf(tp_v2537,type,
v2537: $i > $i > $o ).
thf(tp_v2538,type,
v2538: $i > $i > $o ).
thf(tp_v2539,type,
v2539: $i > $i > $o ).
thf(tp_v2540,type,
v2540: $i > $i > $o ).
thf(tp_v2541,type,
v2541: $i > $i > $o ).
thf(tp_v2542,type,
v2542: $i > $i > $o ).
thf(tp_v2543,type,
v2543: $i > $i > $o ).
thf(tp_v2544,type,
v2544: $i > $i > $o ).
thf(tp_v2545,type,
v2545: $i > $i > $o ).
thf(tp_v2546,type,
v2546: $i > $i > $o ).
thf(tp_v2547,type,
v2547: $i > $i > $o ).
thf(tp_v2548,type,
v2548: $i > $i > $o ).
thf(tp_v2549,type,
v2549: $i > $i > $o ).
thf(tp_v2550,type,
v2550: $i > $i > $o ).
thf(tp_v2551,type,
v2551: $i > $i > $o ).
thf(tp_v2552,type,
v2552: $i > $i > $o ).
thf(tp_v2553,type,
v2553: $i > $i > $o ).
thf(tp_v2554,type,
v2554: $i > $i > $o ).
thf(tp_v2556,type,
v2556: $i > $i > $o ).
thf(tp_v2557,type,
v2557: $i > $i > $o ).
thf(tp_v2559,type,
v2559: $i > $i > $o ).
thf(tp_v2560,type,
v2560: $i > $i > $o ).
thf(tp_v2561,type,
v2561: $i > $i > $o ).
thf(tp_v2562,type,
v2562: $i > $i > $o ).
thf(tp_v2563,type,
v2563: $i > $i > $o ).
thf(tp_v2564,type,
v2564: $i > $i > $o ).
thf(tp_v2565,type,
v2565: $i > $i > $o ).
thf(tp_v2566,type,
v2566: $i > $i > $o ).
thf(tp_v2567,type,
v2567: $i > $i > $o ).
thf(tp_v2568,type,
v2568: $i > $i > $o ).
thf(tp_v2569,type,
v2569: $i > $i > $o ).
thf(tp_v2570,type,
v2570: $i > $i > $o ).
thf(tp_v2571,type,
v2571: $i > $i > $o ).
thf(tp_v2572,type,
v2572: $i > $i > $o ).
thf(tp_v2573,type,
v2573: $i > $i > $o ).
thf(tp_v2574,type,
v2574: $i > $i > $o ).
thf(tp_v2575,type,
v2575: $i > $i > $o ).
thf(tp_v2576,type,
v2576: $i > $i > $o ).
thf(tp_v2577,type,
v2577: $i > $i > $o ).
thf(tp_v2578,type,
v2578: $i > $i > $o ).
thf(tp_v2579,type,
v2579: $i > $i > $o ).
thf(tp_v2580,type,
v2580: $i > $i > $o ).
thf(tp_v2581,type,
v2581: $i > $i > $o ).
thf(tp_v2582,type,
v2582: $i > $i > $o ).
thf(tp_v2583,type,
v2583: $i > $i > $o ).
thf(tp_v2584,type,
v2584: $i > $i > $o ).
thf(tp_v2585,type,
v2585: $i > $i > $o ).
thf(tp_v2586,type,
v2586: $i > $i > $o ).
thf(tp_v2587,type,
v2587: $i > $i > $o ).
thf(tp_v2588,type,
v2588: $i > $i > $o ).
thf(tp_v2589,type,
v2589: $i > $i > $o ).
thf(tp_v2590,type,
v2590: $i > $i > $o ).
thf(tp_v2591,type,
v2591: $i > $i > $o ).
thf(tp_v2592,type,
v2592: $i > $i > $o ).
thf(tp_v2593,type,
v2593: $i > $i > $o ).
thf(tp_v2594,type,
v2594: $i > $i > $o ).
thf(tp_v2595,type,
v2595: $i > $i > $o ).
thf(tp_v2596,type,
v2596: $i > $i > $o ).
thf(tp_v2597,type,
v2597: $i > $i > $o ).
thf(tp_v2598,type,
v2598: $i > $i > $o ).
thf(tp_v2599,type,
v2599: $i > $i > $o ).
thf(tp_v260,type,
v260: $i > $o ).
thf(tp_v2600,type,
v2600: $i > $i > $o ).
thf(tp_v2601,type,
v2601: $i > $i > $o ).
thf(tp_v2602,type,
v2602: $i > $i > $o ).
thf(tp_v2603,type,
v2603: $i > $i > $o ).
thf(tp_v2604,type,
v2604: $i > $i > $o ).
thf(tp_v2605,type,
v2605: $i > $i > $o ).
thf(tp_v2606,type,
v2606: $i > $i > $o ).
thf(tp_v2607,type,
v2607: $i > $i > $o ).
thf(tp_v2608,type,
v2608: $i > $i > $o ).
thf(tp_v2609,type,
v2609: $i > $i > $o ).
thf(tp_v261,type,
v261: $i > $i > $o ).
thf(tp_v2610,type,
v2610: $i > $i > $o ).
thf(tp_v2611,type,
v2611: $i > $i > $o ).
thf(tp_v2612,type,
v2612: $i > $i > $o ).
thf(tp_v2613,type,
v2613: $i > $i > $o ).
thf(tp_v2614,type,
v2614: $i > $i > $o ).
thf(tp_v2615,type,
v2615: $i > $i > $o ).
thf(tp_v2616,type,
v2616: $i > $i > $o ).
thf(tp_v2617,type,
v2617: $i > $i > $o ).
thf(tp_v2618,type,
v2618: $i > $i > $o ).
thf(tp_v2619,type,
v2619: $i > $i > $o ).
thf(tp_v262,type,
v262: $i > $i > $o ).
thf(tp_v2620,type,
v2620: $i > $i > $o ).
thf(tp_v2621,type,
v2621: $i > $i > $o ).
thf(tp_v2622,type,
v2622: $i > $i > $o ).
thf(tp_v2623,type,
v2623: $i > $i > $o ).
thf(tp_v2624,type,
v2624: $i > $i > $o ).
thf(tp_v2625,type,
v2625: $i > $i > $o ).
thf(tp_v2626,type,
v2626: $i > $i > $o ).
thf(tp_v2627,type,
v2627: $i > $i > $o ).
thf(tp_v2628,type,
v2628: $i > $i > $o ).
thf(tp_v2629,type,
v2629: $i > $i > $o ).
thf(tp_v263,type,
v263: $i > $o ).
thf(tp_v2630,type,
v2630: $i > $i > $o ).
thf(tp_v2631,type,
v2631: $i > $i > $o ).
thf(tp_v2632,type,
v2632: $i > $i > $o ).
thf(tp_v2633,type,
v2633: $i > $i > $o ).
thf(tp_v2634,type,
v2634: $i > $i > $o ).
thf(tp_v2635,type,
v2635: $i > $i > $o ).
thf(tp_v2636,type,
v2636: $i > $i > $o ).
thf(tp_v2637,type,
v2637: $i > $i > $o ).
thf(tp_v2638,type,
v2638: $i > $i > $o ).
thf(tp_v2639,type,
v2639: $i > $i > $o ).
thf(tp_v264,type,
v264: $i > $i > $o ).
thf(tp_v2640,type,
v2640: $i > $i > $o ).
thf(tp_v2641,type,
v2641: $i > $i > $o ).
thf(tp_v2642,type,
v2642: $i > $i > $o ).
thf(tp_v2643,type,
v2643: $i > $i > $o ).
thf(tp_v2644,type,
v2644: $i > $i > $o ).
thf(tp_v2645,type,
v2645: $i > $i > $o ).
thf(tp_v2646,type,
v2646: $i > $i > $o ).
thf(tp_v2647,type,
v2647: $i > $i > $o ).
thf(tp_v2648,type,
v2648: $i > $i > $o ).
thf(tp_v2649,type,
v2649: $i > $i > $o ).
thf(tp_v2654,type,
v2654: $i > $i > $o ).
thf(tp_v2655,type,
v2655: $i > $i > $o ).
thf(tp_v2657,type,
v2657: $i > $i > $o ).
thf(tp_v2658,type,
v2658: $i > $i > $o ).
thf(tp_v2659,type,
v2659: $i > $i > $o ).
thf(tp_v2660,type,
v2660: $i > $i > $o ).
thf(tp_v2661,type,
v2661: $i > $i > $o ).
thf(tp_v2662,type,
v2662: $i > $i > $o ).
thf(tp_v2663,type,
v2663: $i > $i > $o ).
thf(tp_v2664,type,
v2664: $i > $i > $o ).
thf(tp_v2665,type,
v2665: $i > $i > $o ).
thf(tp_v2667,type,
v2667: $i > $i > $o ).
thf(tp_v269,type,
v269: $i > $o ).
thf(tp_v270,type,
v270: $i > $o ).
thf(tp_v2702,type,
v2702: $i > $i > $o ).
thf(tp_v2703,type,
v2703: $i > $i > $o ).
thf(tp_v2704,type,
v2704: $i > $i > $o ).
thf(tp_v2705,type,
v2705: $i > $i > $o ).
thf(tp_v2707,type,
v2707: $i > $i > $o ).
thf(tp_v2708,type,
v2708: $i > $i > $o ).
thf(tp_v2709,type,
v2709: $i > $i > $o ).
thf(tp_v2710,type,
v2710: $i > $i > $o ).
thf(tp_v2712,type,
v2712: $i > $i > $o ).
thf(tp_v2713,type,
v2713: $i > $i > $o ).
thf(tp_v2714,type,
v2714: $i > $i > $o ).
thf(tp_v2715,type,
v2715: $i > $i > $o ).
thf(tp_v2717,type,
v2717: $i > $i > $o ).
thf(tp_v2718,type,
v2718: $i > $i > $o ).
thf(tp_v2719,type,
v2719: $i > $i > $o ).
thf(tp_v2737,type,
v2737: $i > $o ).
thf(tp_v2747,type,
v2747: $i > $o ).
thf(tp_v2750,type,
v2750: $i > $o ).
thf(tp_v2756,type,
v2756: $i > $o ).
thf(tp_v2757,type,
v2757: $i > $o ).
thf(tp_v2758,type,
v2758: $i > $o ).
thf(tp_v2762,type,
v2762: $i > $o ).
thf(tp_v2764,type,
v2764: $i > $o ).
thf(tp_v2781,type,
v2781: $i > $i > $o ).
thf(tp_v2785,type,
v2785: $i > $i > $o ).
thf(tp_v2793,type,
v2793: $i > $i > $o ).
thf(tp_v2804,type,
v2804: $i > $i > $o ).
thf(tp_v2805,type,
v2805: $i > $o ).
thf(tp_v2810,type,
v2810: $i > $o ).
thf(tp_v2825,type,
v2825: $i > $o ).
thf(tp_v2828,type,
v2828: $i > $i > $o ).
thf(tp_v2829,type,
v2829: $i > $i > $o ).
thf(tp_v2830,type,
v2830: $i > $i > $o ).
thf(tp_v2831,type,
v2831: $i > $i > $o ).
thf(tp_v2832,type,
v2832: $i > $i > $o ).
thf(tp_v2836,type,
v2836: $i > $i > $o ).
thf(tp_v2837,type,
v2837: $i > $o ).
thf(tp_v2838,type,
v2838: $i > $o ).
thf(tp_v2839,type,
v2839: $i > $o ).
thf(tp_v284,type,
v284: $i > $i > $o ).
thf(tp_v2841,type,
v2841: $i > $o ).
thf(tp_v2845,type,
v2845: $i > $i > $o ).
thf(tp_v2847,type,
v2847: $i > $i > $o ).
thf(tp_v2855,type,
v2855: $i > $o ).
thf(tp_v2856,type,
v2856: $i > $o ).
thf(tp_v2857,type,
v2857: $i > $o ).
thf(tp_v2863,type,
v2863: $i > $o ).
thf(tp_v2867,type,
v2867: $i > $o ).
thf(tp_v2872,type,
v2872: $i > $i > $o ).
thf(tp_v2874,type,
v2874: $i > $i > $o ).
thf(tp_v2875,type,
v2875: $i > $i > $o ).
thf(tp_v2876,type,
v2876: $i > $i > $o ).
thf(tp_v2881,type,
v2881: $i > $o ).
thf(tp_v2882,type,
v2882: $i > $o ).
thf(tp_v2883,type,
v2883: $i > $o ).
thf(tp_v2901,type,
v2901: $i > $i > $o ).
thf(tp_v2906,type,
v2906: $i > $o ).
thf(tp_v2908,type,
v2908: $i > $o ).
thf(tp_v291,type,
v291: $i > $o ).
thf(tp_v2910,type,
v2910: $i > $o ).
thf(tp_v292,type,
v292: $i > $o ).
thf(tp_v2927,type,
v2927: $i > $i > $o ).
thf(tp_v2929,type,
v2929: $i > $o ).
thf(tp_v293,type,
v293: $i > $o ).
thf(tp_v2940,type,
v2940: $i > $o ).
thf(tp_v2941,type,
v2941: $i > $o ).
thf(tp_v2942,type,
v2942: $i > $o ).
thf(tp_v2948,type,
v2948: $i > $o ).
thf(tp_v295,type,
v295: $i > $o ).
thf(tp_v2952,type,
v2952: $i > $o ).
thf(tp_v2955,type,
v2955: $i > $i > $o ).
thf(tp_v2957,type,
v2957: $i > $i > $o ).
thf(tp_v2958,type,
v2958: $i > $i > $o ).
thf(tp_v2959,type,
v2959: $i > $i > $o ).
thf(tp_v2964,type,
v2964: $i > $o ).
thf(tp_v2965,type,
v2965: $i > $o ).
thf(tp_v2966,type,
v2966: $i > $o ).
thf(tp_v2989,type,
v2989: $i > $i > $o ).
thf(tp_v299,type,
v299: $i > $i > $o ).
thf(tp_v2990,type,
v2990: $i > $i > $o ).
thf(tp_v2991,type,
v2991: $i > $i > $o ).
thf(tp_v2992,type,
v2992: $i > $o ).
thf(tp_v2993,type,
v2993: $i > $i > $o ).
thf(tp_v2994,type,
v2994: $i > $o ).
thf(tp_v2996,type,
v2996: $i > $i > $o ).
thf(tp_v2997,type,
v2997: $i > $o ).
thf(tp_v3004,type,
v3004: $i > $o ).
thf(tp_v3005,type,
v3005: $i > $i > $o ).
thf(tp_v3006,type,
v3006: $i > $i > $o ).
thf(tp_v3008,type,
v3008: $i > $i > $o ).
thf(tp_v3009,type,
v3009: $i > $o ).
thf(tp_v301,type,
v301: $i > $i > $o ).
thf(tp_v3010,type,
v3010: $i > $i > $o ).
thf(tp_v3015,type,
v3015: $i > $o ).
thf(tp_v3017,type,
v3017: $i > $o ).
thf(tp_v3019,type,
v3019: $i > $o ).
thf(tp_v3021,type,
v3021: $i > $o ).
thf(tp_v3022,type,
v3022: $i > $o ).
thf(tp_v3026,type,
v3026: $i > $o ).
thf(tp_v3030,type,
v3030: $i > $o ).
thf(tp_v3035,type,
v3035: $i > $o ).
thf(tp_v3058,type,
v3058: $i > $i > $o ).
thf(tp_v3059,type,
v3059: $i > $i > $o ).
thf(tp_v3060,type,
v3060: $i > $o ).
thf(tp_v3061,type,
v3061: $i > $i > $o ).
thf(tp_v3062,type,
v3062: $i > $o ).
thf(tp_v3065,type,
v3065: $i > $i > $o ).
thf(tp_v3079,type,
v3079: $i > $o ).
thf(tp_v3080,type,
v3080: $i > $o ).
thf(tp_v3081,type,
v3081: $i > $o ).
thf(tp_v3085,type,
v3085: $i > $i > $o ).
thf(tp_v3087,type,
v3087: $i > $i > $o ).
thf(tp_v31,type,
v31: $i > $i > $o ).
thf(tp_v3101,type,
v3101: $i > $i > $o ).
thf(tp_v3107,type,
v3107: $i > $o ).
thf(tp_v3133,type,
v3133: $i > $i > $o ).
thf(tp_v3134,type,
v3134: $i > $o ).
thf(tp_v3135,type,
v3135: $i > $o ).
thf(tp_v3137,type,
v3137: $i > $o ).
thf(tp_v3150,type,
v3150: $i > $o ).
thf(tp_v3151,type,
v3151: $i > $o ).
thf(tp_v3152,type,
v3152: $i > $o ).
thf(tp_v3154,type,
v3154: $i > $o ).
thf(tp_v3160,type,
v3160: $i > $o ).
thf(tp_v3163,type,
v3163: $i > $o ).
thf(tp_v3167,type,
v3167: $i > $i > $o ).
thf(tp_v3168,type,
v3168: $i > $o ).
thf(tp_v318,type,
v318: $i > $o ).
thf(tp_v3183,type,
v3183: $i > $o ).
thf(tp_v3185,type,
v3185: $i > $o ).
thf(tp_v3186,type,
v3186: $i > $o ).
thf(tp_v3188,type,
v3188: $i > $o ).
thf(tp_v3191,type,
v3191: $i > $o ).
thf(tp_v3205,type,
v3205: $i > $i > $o ).
thf(tp_v3207,type,
v3207: $i > $i > $o ).
thf(tp_v3209,type,
v3209: $i > $o ).
thf(tp_v3210,type,
v3210: $i > $i > $o ).
thf(tp_v3211,type,
v3211: $i > $o ).
thf(tp_v3212,type,
v3212: $i > $i > $o ).
thf(tp_v3213,type,
v3213: $i > $i > $o ).
thf(tp_v3214,type,
v3214: $i > $o ).
thf(tp_v3215,type,
v3215: $i > $i > $o ).
thf(tp_v3216,type,
v3216: $i > $i > $o ).
thf(tp_v3221,type,
v3221: $i > $o ).
thf(tp_v3222,type,
v3222: $i > $i > $o ).
thf(tp_v3224,type,
v3224: $i > $o ).
thf(tp_v3226,type,
v3226: $i > $o ).
thf(tp_v3228,type,
v3228: $i > $o ).
thf(tp_v3252,type,
v3252: $i > $o ).
thf(tp_v3253,type,
v3253: $i > $i > $o ).
thf(tp_v3254,type,
v3254: $i > $i > $o ).
thf(tp_v3255,type,
v3255: $i > $o ).
thf(tp_v3256,type,
v3256: $i > $i > $o ).
thf(tp_v3261,type,
v3261: $i > $o ).
thf(tp_v3262,type,
v3262: $i > $o ).
thf(tp_v3263,type,
v3263: $i > $o ).
thf(tp_v3282,type,
v3282: $i > $i > $o ).
thf(tp_v3285,type,
v3285: $i > $o ).
thf(tp_v3286,type,
v3286: $i > $o ).
thf(tp_v3287,type,
v3287: $i > $o ).
thf(tp_v3291,type,
v3291: $i > $i > $o ).
thf(tp_v3293,type,
v3293: $i > $i > $o ).
thf(tp_v3309,type,
v3309: $i > $i > $o ).
thf(tp_v3313,type,
v3313: $i > $o ).
thf(tp_v3323,type,
v3323: $i > $i > $o ).
thf(tp_v3324,type,
v3324: $i > $o ).
thf(tp_v3325,type,
v3325: $i > $o ).
thf(tp_v3327,type,
v3327: $i > $o ).
thf(tp_v3331,type,
v3331: $i > $o ).
thf(tp_v334,type,
v334: $i > $i > $o ).
thf(tp_v3358,type,
v3358: $i > $o ).
thf(tp_v3371,type,
v3371: $i > $o ).
thf(tp_v3372,type,
v3372: $i > $o ).
thf(tp_v3373,type,
v3373: $i > $o ).
thf(tp_v3375,type,
v3375: $i > $o ).
thf(tp_v3381,type,
v3381: $i > $o ).
thf(tp_v3388,type,
v3388: $i > $i > $o ).
thf(tp_v3390,type,
v3390: $i > $i > $o ).
thf(tp_v3391,type,
v3391: $i > $i > $o ).
thf(tp_v3398,type,
v3398: $i > $o ).
thf(tp_v342,type,
v342: $i > $i > $o ).
thf(tp_v3426,type,
v3426: $i > $o ).
thf(tp_v3427,type,
v3427: $i > $o ).
thf(tp_v3428,type,
v3428: $i > $o ).
thf(tp_v3432,type,
v3432: $i > $o ).
thf(tp_v3434,type,
v3434: $i > $o ).
thf(tp_v3436,type,
v3436: $i > $o ).
thf(tp_v3437,type,
v3437: $i > $o ).
thf(tp_v3453,type,
v3453: $i > $i > $o ).
thf(tp_v3455,type,
v3455: $i > $i > $o ).
thf(tp_v3463,type,
v3463: $i > $o ).
thf(tp_v3467,type,
v3467: $i > $o ).
thf(tp_v3471,type,
v3471: $i > $o ).
thf(tp_v3475,type,
v3475: $i > $o ).
thf(tp_v3479,type,
v3479: $i > $o ).
thf(tp_v348,type,
v348: $i > $i > $o ).
thf(tp_v3483,type,
v3483: $i > $o ).
thf(tp_v3487,type,
v3487: $i > $o ).
thf(tp_v3491,type,
v3491: $i > $o ).
thf(tp_v3500,type,
v3500: $i > $o ).
thf(tp_v352,type,
v352: $i > $i > $o ).
thf(tp_v3521,type,
v3521: $i > $i > $o ).
thf(tp_v3524,type,
v3524: $i > $i > $o ).
thf(tp_v3536,type,
v3536: $i > $o ).
thf(tp_v3537,type,
v3537: $i > $o ).
thf(tp_v3538,type,
v3538: $i > $o ).
thf(tp_v3540,type,
v3540: $i > $o ).
thf(tp_v3544,type,
v3544: $i > $i > $o ).
thf(tp_v3546,type,
v3546: $i > $i > $o ).
thf(tp_v3551,type,
v3551: $i > $o ).
thf(tp_v3552,type,
v3552: $i > $o ).
thf(tp_v3555,type,
v3555: $i > $i > $o ).
thf(tp_v3556,type,
v3556: $i > $i > $o ).
thf(tp_v3558,type,
v3558: $i > $i > $o ).
thf(tp_v3560,type,
v3560: $i > $i > $o ).
thf(tp_v3561,type,
v3561: $i > $o ).
thf(tp_v3562,type,
v3562: $i > $i > $o ).
thf(tp_v3563,type,
v3563: $i > $o ).
thf(tp_v3564,type,
v3564: $i > $i > $o ).
thf(tp_v3565,type,
v3565: $i > $i > $o ).
thf(tp_v3567,type,
v3567: $i > $o ).
thf(tp_v3568,type,
v3568: $i > $i > $o ).
thf(tp_v3569,type,
v3569: $i > $i > $o ).
thf(tp_v3571,type,
v3571: $i > $i > $o ).
thf(tp_v3577,type,
v3577: $i > $i > $o ).
thf(tp_v3578,type,
v3578: $i > $o ).
thf(tp_v3579,type,
v3579: $i > $o ).
thf(tp_v3580,type,
v3580: $i > $o ).
thf(tp_v3582,type,
v3582: $i > $o ).
thf(tp_v3586,type,
v3586: $i > $i > $o ).
thf(tp_v3588,type,
v3588: $i > $i > $o ).
thf(tp_v3593,type,
v3593: $i > $i > $o ).
thf(tp_v3594,type,
v3594: $i > $o ).
thf(tp_v3595,type,
v3595: $i > $o ).
thf(tp_v3597,type,
v3597: $i > $o ).
thf(tp_v36,type,
v36: $i > $i > $o ).
thf(tp_v3601,type,
v3601: $i > $i > $o ).
thf(tp_v3602,type,
v3602: $i > $o ).
thf(tp_v3603,type,
v3603: $i > $o ).
thf(tp_v3605,type,
v3605: $i > $o ).
thf(tp_v3611,type,
v3611: $i > $o ).
thf(tp_v3635,type,
v3635: $i > $i > $o ).
thf(tp_v3636,type,
v3636: $i > $o ).
thf(tp_v3637,type,
v3637: $i > $o ).
thf(tp_v3639,type,
v3639: $i > $o ).
thf(tp_v3643,type,
v3643: $i > $i > $o ).
thf(tp_v3644,type,
v3644: $i > $o ).
thf(tp_v3645,type,
v3645: $i > $i > $o ).
thf(tp_v3650,type,
v3650: $i > $o ).
thf(tp_v3660,type,
v3660: $i > $o ).
thf(tp_v3661,type,
v3661: $i > $o ).
thf(tp_v3662,type,
v3662: $i > $o ).
thf(tp_v3666,type,
v3666: $i > $i > $o ).
thf(tp_v3668,type,
v3668: $i > $i > $o ).
thf(tp_v3679,type,
v3679: $i > $i > $o ).
thf(tp_v3684,type,
v3684: $i > $i > $o ).
thf(tp_v372,type,
v372: $i > $o ).
thf(tp_v374,type,
v374: $i > $o ).
thf(tp_v385,type,
v385: $i > $i > $o ).
thf(tp_v389,type,
v389: $i > $i > $o ).
thf(tp_v407,type,
v407: $i > $o ).
thf(tp_v408,type,
v408: $i > $i > $o ).
thf(tp_v409,type,
v409: $i > $o ).
thf(tp_v410,type,
v410: $i > $i > $o ).
thf(tp_v411,type,
v411: $i > $i > $o ).
thf(tp_v412,type,
v412: $i > $o ).
thf(tp_v413,type,
v413: $i > $i > $o ).
thf(tp_v414,type,
v414: $i > $i > $o ).
thf(tp_v419,type,
v419: $i > $o ).
thf(tp_v420,type,
v420: $i > $i > $o ).
thf(tp_v422,type,
v422: $i > $o ).
thf(tp_v424,type,
v424: $i > $o ).
thf(tp_v426,type,
v426: $i > $o ).
thf(tp_v450,type,
v450: $i > $o ).
thf(tp_v451,type,
v451: $i > $i > $o ).
thf(tp_v452,type,
v452: $i > $i > $o ).
thf(tp_v453,type,
v453: $i > $o ).
thf(tp_v454,type,
v454: $i > $i > $o ).
thf(tp_v459,type,
v459: $i > $o ).
thf(tp_v460,type,
v460: $i > $o ).
thf(tp_v461,type,
v461: $i > $o ).
thf(tp_v480,type,
v480: $i > $i > $o ).
thf(tp_v491,type,
v491: $i > $o ).
thf(tp_v492,type,
v492: $i > $o ).
thf(tp_v493,type,
v493: $i > $o ).
thf(tp_v495,type,
v495: $i > $o ).
thf(tp_v499,type,
v499: $i > $i > $o ).
thf(tp_v501,type,
v501: $i > $i > $o ).
thf(tp_v507,type,
v507: $i > $o ).
thf(tp_v508,type,
v508: $i > $o ).
thf(tp_v515,type,
v515: $i > $o ).
thf(tp_v516,type,
v516: $i > $o ).
thf(tp_v520,type,
v520: $i > $o ).
thf(tp_v521,type,
v521: $i > $o ).
thf(tp_v522,type,
v522: $i > $o ).
thf(tp_v524,type,
v524: $i > $o ).
thf(tp_v528,type,
v528: $i > $o ).
thf(tp_v530,type,
v530: $i > $o ).
thf(tp_v536,type,
v536: $i > $o ).
thf(tp_v537,type,
v537: $i > $o ).
thf(tp_v538,type,
v538: $i > $o ).
thf(tp_v540,type,
v540: $i > $o ).
thf(tp_v541,type,
v541: $i > $o ).
thf(tp_v543,type,
v543: $i > $o ).
thf(tp_v544,type,
v544: $i > $i > $o ).
thf(tp_v545,type,
v545: $i > $o ).
thf(tp_v546,type,
v546: $i > $i > $o ).
thf(tp_v547,type,
v547: $i > $i > $o ).
thf(tp_v548,type,
v548: $i > $o ).
thf(tp_v549,type,
v549: $i > $i > $o ).
thf(tp_v550,type,
v550: $i > $i > $o ).
thf(tp_v555,type,
v555: $i > $o ).
thf(tp_v556,type,
v556: $i > $i > $o ).
thf(tp_v558,type,
v558: $i > $o ).
thf(tp_v56,type,
v56: $i > $i > $o ).
thf(tp_v560,type,
v560: $i > $o ).
thf(tp_v562,type,
v562: $i > $o ).
thf(tp_v586,type,
v586: $i > $o ).
thf(tp_v587,type,
v587: $i > $i > $o ).
thf(tp_v588,type,
v588: $i > $i > $o ).
thf(tp_v589,type,
v589: $i > $o ).
thf(tp_v590,type,
v590: $i > $i > $o ).
thf(tp_v595,type,
v595: $i > $o ).
thf(tp_v596,type,
v596: $i > $o ).
thf(tp_v597,type,
v597: $i > $o ).
thf(tp_v616,type,
v616: $i > $i > $o ).
thf(tp_v621,type,
v621: $i > $o ).
thf(tp_v622,type,
v622: $i > $o ).
thf(tp_v623,type,
v623: $i > $o ).
thf(tp_v625,type,
v625: $i > $o ).
thf(tp_v629,type,
v629: $i > $i > $o ).
thf(tp_v631,type,
v631: $i > $i > $o ).
thf(tp_v637,type,
v637: $i > $o ).
thf(tp_v638,type,
v638: $i > $o ).
thf(tp_v641,type,
v641: $i > $o ).
thf(tp_v642,type,
v642: $i > $o ).
thf(tp_v645,type,
v645: $i > $o ).
thf(tp_v646,type,
v646: $i > $o ).
thf(tp_v648,type,
v648: $i > $o ).
thf(tp_v651,type,
v651: $i > $o ).
thf(tp_v653,type,
v653: $i > $o ).
thf(tp_v657,type,
v657: $i > $o ).
thf(tp_v658,type,
v658: $i > $o ).
thf(tp_v659,type,
v659: $i > $o ).
thf(tp_v660,type,
v660: $i > $o ).
thf(tp_v661,type,
v661: $i > $o ).
thf(tp_v662,type,
v662: $i > $o ).
thf(tp_v668,type,
v668: $i > $o ).
thf(tp_v67,type,
v67: $i > $i > $o ).
thf(tp_v682,type,
v682: $i > $o ).
thf(tp_v696,type,
v696: $i > $o ).
thf(tp_v704,type,
v704: $i > $o ).
thf(tp_v705,type,
v705: $i > $o ).
thf(tp_v706,type,
v706: $i > $o ).
thf(tp_v708,type,
v708: $i > $o ).
thf(tp_v714,type,
v714: $i > $o ).
thf(tp_v724,type,
v724: $i > $o ).
thf(tp_v725,type,
v725: $i > $o ).
thf(tp_v726,type,
v726: $i > $o ).
thf(tp_v728,type,
v728: $i > $o ).
thf(tp_v734,type,
v734: $i > $o ).
thf(tp_v741,type,
v741: $i > $o ).
thf(tp_v743,type,
v743: $i > $i > $o ).
thf(tp_v745,type,
v745: $i > $i > $o ).
thf(tp_v747,type,
v747: $i > $i > $o ).
thf(tp_v749_1__array,type,
v749_1__array: $i > $i > $i > $o ).
thf(tp_v749_array,type,
v749_array: $i > $i > $i > $o ).
thf(tp_v756,type,
v756: $i > $i > $o ).
thf(tp_v762,type,
v762: $i > $i > $o ).
thf(tp_v768,type,
v768: $i > $i > $o ).
thf(tp_v774,type,
v774: $i > $i > $o ).
thf(tp_v780,type,
v780: $i > $i > $o ).
thf(tp_v791,type,
v791: $i > $i > $o ).
thf(tp_v791_range_3_to_0_address_association,type,
v791_range_3_to_0_address_association: $i > $i > $o ).
thf(tp_v791_range_3_to_0_address_term_bound_0,type,
v791_range_3_to_0_address_term_bound_0: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_1,type,
v791_range_3_to_0_address_term_bound_1: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_10,type,
v791_range_3_to_0_address_term_bound_10: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_11,type,
v791_range_3_to_0_address_term_bound_11: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_12,type,
v791_range_3_to_0_address_term_bound_12: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_13,type,
v791_range_3_to_0_address_term_bound_13: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_14,type,
v791_range_3_to_0_address_term_bound_14: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_15,type,
v791_range_3_to_0_address_term_bound_15: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_16,type,
v791_range_3_to_0_address_term_bound_16: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_17,type,
v791_range_3_to_0_address_term_bound_17: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_18,type,
v791_range_3_to_0_address_term_bound_18: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_19,type,
v791_range_3_to_0_address_term_bound_19: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_2,type,
v791_range_3_to_0_address_term_bound_2: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_20,type,
v791_range_3_to_0_address_term_bound_20: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_3,type,
v791_range_3_to_0_address_term_bound_3: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_4,type,
v791_range_3_to_0_address_term_bound_4: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_5,type,
v791_range_3_to_0_address_term_bound_5: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_6,type,
v791_range_3_to_0_address_term_bound_6: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_7,type,
v791_range_3_to_0_address_term_bound_7: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_8,type,
v791_range_3_to_0_address_term_bound_8: $i ).
thf(tp_v791_range_3_to_0_address_term_bound_9,type,
v791_range_3_to_0_address_term_bound_9: $i ).
thf(tp_v793,type,
v793: $i > $i > $o ).
thf(tp_v796,type,
v796: $i > $i > $o ).
thf(tp_v797,type,
v797: $i > $o ).
thf(tp_v798,type,
v798: $i > $i > $o ).
thf(tp_v8,type,
v8: $i > $i > $o ).
thf(tp_v803,type,
v803: $i > $o ).
thf(tp_v804,type,
v804: $i > $o ).
thf(tp_v819,type,
v819: $i > $o ).
thf(tp_v820,type,
v820: $i > $o ).
thf(tp_v821,type,
v821: $i > $o ).
thf(tp_v823,type,
v823: $i > $o ).
thf(tp_v827,type,
v827: $i > $i > $o ).
thf(tp_v829,type,
v829: $i > $i > $o ).
thf(tp_v847,type,
v847: $i > $o ).
thf(tp_v848,type,
v848: $i > $o ).
thf(tp_v849,type,
v849: $i > $o ).
thf(tp_v854,type,
v854: $i > $o ).
thf(tp_v859,type,
v859: $i > $o ).
thf(tp_v860,type,
v860: $i > $o ).
thf(tp_v862,type,
v862: $i > $o ).
thf(tp_v865,type,
v865: $i > $o ).
thf(tp_v867,type,
v867: $i > $i > $o ).
thf(tp_v869,type,
v869: $i > $i > $o ).
thf(tp_v869_range_3_to_0_address_association,type,
v869_range_3_to_0_address_association: $i > $i > $o ).
thf(tp_v869_range_3_to_0_address_term_bound_0,type,
v869_range_3_to_0_address_term_bound_0: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_1,type,
v869_range_3_to_0_address_term_bound_1: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_10,type,
v869_range_3_to_0_address_term_bound_10: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_11,type,
v869_range_3_to_0_address_term_bound_11: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_12,type,
v869_range_3_to_0_address_term_bound_12: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_13,type,
v869_range_3_to_0_address_term_bound_13: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_14,type,
v869_range_3_to_0_address_term_bound_14: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_15,type,
v869_range_3_to_0_address_term_bound_15: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_16,type,
v869_range_3_to_0_address_term_bound_16: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_17,type,
v869_range_3_to_0_address_term_bound_17: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_18,type,
v869_range_3_to_0_address_term_bound_18: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_19,type,
v869_range_3_to_0_address_term_bound_19: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_2,type,
v869_range_3_to_0_address_term_bound_2: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_20,type,
v869_range_3_to_0_address_term_bound_20: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_3,type,
v869_range_3_to_0_address_term_bound_3: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_4,type,
v869_range_3_to_0_address_term_bound_4: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_5,type,
v869_range_3_to_0_address_term_bound_5: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_6,type,
v869_range_3_to_0_address_term_bound_6: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_7,type,
v869_range_3_to_0_address_term_bound_7: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_8,type,
v869_range_3_to_0_address_term_bound_8: $i ).
thf(tp_v869_range_3_to_0_address_term_bound_9,type,
v869_range_3_to_0_address_term_bound_9: $i ).
thf(tp_v871,type,
v871: $i > $i > $o ).
thf(tp_v885,type,
v885: $i > $i > $o ).
thf(tp_v887,type,
v887: $i > $i > $o ).
thf(tp_v888,type,
v888: $i > $i > $o ).
thf(tp_v889,type,
v889: $i > $i > $o ).
thf(tp_v892,type,
v892: $i > $i > $o ).
thf(tp_v894,type,
v894: $i > $i > $o ).
thf(tp_v895,type,
v895: $i > $i > $o ).
thf(tp_v896,type,
v896: $i > $i > $o ).
thf(tp_v898,type,
v898: $i > $i > $o ).
thf(tp_v899,type,
v899: $i > $i > $o ).
thf(tp_v900,type,
v900: $i > $i > $o ).
thf(tp_v91,type,
v91: $i > $i > $o ).
thf(tp_v919,type,
v919: $i > $i > $o ).
thf(tp_v921,type,
v921: $i > $i > $o ).
thf(tp_v923_1__array,type,
v923_1__array: $i > $i > $i > $o ).
thf(tp_v923_array,type,
v923_array: $i > $i > $i > $o ).
thf(tp_v930,type,
v930: $i > $i > $o ).
thf(tp_v936,type,
v936: $i > $i > $o ).
thf(tp_v942,type,
v942: $i > $i > $o ).
thf(tp_v95,type,
v95: $i > $i > $o ).
thf(tp_v953,type,
v953: $i > $i > $o ).
thf(tp_v953_range_3_to_0_address_association,type,
v953_range_3_to_0_address_association: $i > $i > $o ).
thf(tp_v953_range_3_to_0_address_term_bound_0,type,
v953_range_3_to_0_address_term_bound_0: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_1,type,
v953_range_3_to_0_address_term_bound_1: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_10,type,
v953_range_3_to_0_address_term_bound_10: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_11,type,
v953_range_3_to_0_address_term_bound_11: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_12,type,
v953_range_3_to_0_address_term_bound_12: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_13,type,
v953_range_3_to_0_address_term_bound_13: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_14,type,
v953_range_3_to_0_address_term_bound_14: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_15,type,
v953_range_3_to_0_address_term_bound_15: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_16,type,
v953_range_3_to_0_address_term_bound_16: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_17,type,
v953_range_3_to_0_address_term_bound_17: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_18,type,
v953_range_3_to_0_address_term_bound_18: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_19,type,
v953_range_3_to_0_address_term_bound_19: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_2,type,
v953_range_3_to_0_address_term_bound_2: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_20,type,
v953_range_3_to_0_address_term_bound_20: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_3,type,
v953_range_3_to_0_address_term_bound_3: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_4,type,
v953_range_3_to_0_address_term_bound_4: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_5,type,
v953_range_3_to_0_address_term_bound_5: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_6,type,
v953_range_3_to_0_address_term_bound_6: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_7,type,
v953_range_3_to_0_address_term_bound_7: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_8,type,
v953_range_3_to_0_address_term_bound_8: $i ).
thf(tp_v953_range_3_to_0_address_term_bound_9,type,
v953_range_3_to_0_address_term_bound_9: $i ).
thf(tp_v955,type,
v955: $i > $i > $o ).
thf(tp_v957,type,
v957: $i > $i > $o ).
thf(tp_v958,type,
v958: $i > $o ).
thf(tp_v959,type,
v959: $i > $i > $o ).
thf(tp_v964,type,
v964: $i > $o ).
thf(tp_v965,type,
v965: $i > $o ).
thf(tp_v97,type,
v97: $i > $i > $o ).
thf(tp_v980,type,
v980: $i > $o ).
thf(tp_v981,type,
v981: $i > $o ).
thf(tp_v982,type,
v982: $i > $o ).
thf(tp_v984,type,
v984: $i > $o ).
thf(tp_v988,type,
v988: $i > $i > $o ).
thf(tp_v990,type,
v990: $i > $i > $o ).
thf(tp_v997,type,
v997: $i > $o ).
thf(tp_v998,type,
v998: $i > $o ).
thf(tp_v999,type,
v999: $i > $o ).
thf(11791,conjecture,
$false,
file('no conjecture given, we try to refute the axioms',dummy_conjecture) ).
thf(11792,negated_conjecture,
$false = $false,
inference(negate_conjecture,[status(cth)],[11791]) ).
thf(11793,negated_conjecture,
$false,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u56157) ).
thf(11794,plain,
$false = $false,
inference(unfold_def,[status(thm)],[11792]) ).
thf(11795,plain,
$false = $true,
inference(unfold_def,[status(thm)],[11793]) ).
thf(11796,plain,
( ( ~ $false ) = $true ),
inference(polarity_switch,[status(thm)],[11794]) ).
thf(11797,plain,
$false = $true,
inference(copy,[status(thm)],[11795]) ).
thf(11798,plain,
( ( ~ $false ) = $true ),
inference(copy,[status(thm)],[11796]) ).
thf(11799,plain,
$false = $false,
inference(extcnf_not_pos,[status(thm)],[11798]) ).
thf(11800,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[11797,11799]) ).
thf(11801,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[11800]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV089-1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.06/0.20 % Computer : n001.cluster.edu
% 0.06/0.20 % Model : x86_64 x86_64
% 0.06/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.20 % Memory : 8046.5625MB
% 0.06/0.20 % OS : Linux 6.8.0-71-generic
% 0.06/0.20 % CPULimit : 300
% 0.06/0.20 % WCLimit : 300
% 0.06/0.20 % DateTime : Tue Oct 6 11:08:54 UTC 2026
% 0.06/0.20 % CPUTime :
% 0.06/0.20 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.61/5.87 ...............................................................................
% 33.61/5.87
% 33.61/5.87 No.of.Axioms: 1
% 33.61/5.87
% 33.61/5.87 Length.of.Defs: 0
% 33.61/5.87
% 33.61/5.87 Contains.Choice.Funs: false
% 33.61/5.87 ................................................................................
% 33.61/5.87
% 33.61/5.87 ********************************
% 33.61/5.87 * All subproblems solved! *
% 33.61/5.87 ********************************
% 33.61/5.87 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:1,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:297,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:11800,loop_count:0,foatp_calls:1,translation:fof_full)
% 33.61/5.87
% 33.61/5.87 %**** Beginning of derivation protocol ****
% 33.61/5.87 % SZS output start CNFRefutation
% See solution above
% 33.61/5.87
% 33.61/5.87 %**** End of derivation protocol ****
% 33.61/5.87 %**** no. of clauses in derivation: 11 ****
% 33.61/5.87 %**** clause counter: 11800 ****
% 33.61/5.87
% 33.61/5.87 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:1,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:297,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:11800,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------