%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : HWV093-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/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:44 AM UTC 2026
% Result : Unsatisfiable 6.08s 1.24s
% Output : CNFRefutation 6.08s
% 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 : 972 ( 969 usr; 400 con; 0-2 aty)
% Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_b001,type,
b001: $i > $o ).
thf(tp_b01,type,
b01: $i > $o ).
thf(tp_b010,type,
b010: $i > $o ).
thf(tp_b01111,type,
b01111: $i > $o ).
thf(tp_b10,type,
b10: $i > $o ).
thf(tp_b100,type,
b100: $i > $o ).
thf(tp_b1000,type,
b1000: $i > $o ).
thf(tp_b1110,type,
b1110: $i > $o ).
thf(tp_bitIndex0,type,
bitIndex0: $i ).
thf(tp_bitIndex1,type,
bitIndex1: $i ).
thf(tp_bitIndex10,type,
bitIndex10: $i ).
thf(tp_bitIndex100,type,
bitIndex100: $i ).
thf(tp_bitIndex101,type,
bitIndex101: $i ).
thf(tp_bitIndex102,type,
bitIndex102: $i ).
thf(tp_bitIndex103,type,
bitIndex103: $i ).
thf(tp_bitIndex104,type,
bitIndex104: $i ).
thf(tp_bitIndex105,type,
bitIndex105: $i ).
thf(tp_bitIndex106,type,
bitIndex106: $i ).
thf(tp_bitIndex107,type,
bitIndex107: $i ).
thf(tp_bitIndex108,type,
bitIndex108: $i ).
thf(tp_bitIndex109,type,
bitIndex109: $i ).
thf(tp_bitIndex11,type,
bitIndex11: $i ).
thf(tp_bitIndex110,type,
bitIndex110: $i ).
thf(tp_bitIndex111,type,
bitIndex111: $i ).
thf(tp_bitIndex112,type,
bitIndex112: $i ).
thf(tp_bitIndex113,type,
bitIndex113: $i ).
thf(tp_bitIndex114,type,
bitIndex114: $i ).
thf(tp_bitIndex115,type,
bitIndex115: $i ).
thf(tp_bitIndex116,type,
bitIndex116: $i ).
thf(tp_bitIndex117,type,
bitIndex117: $i ).
thf(tp_bitIndex118,type,
bitIndex118: $i ).
thf(tp_bitIndex119,type,
bitIndex119: $i ).
thf(tp_bitIndex12,type,
bitIndex12: $i ).
thf(tp_bitIndex120,type,
bitIndex120: $i ).
thf(tp_bitIndex121,type,
bitIndex121: $i ).
thf(tp_bitIndex122,type,
bitIndex122: $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_bitIndex393,type,
bitIndex393: $i ).
thf(tp_bitIndex394,type,
bitIndex394: $i ).
thf(tp_bitIndex395,type,
bitIndex395: $i ).
thf(tp_bitIndex396,type,
bitIndex396: $i ).
thf(tp_bitIndex397,type,
bitIndex397: $i ).
thf(tp_bitIndex398,type,
bitIndex398: $i ).
thf(tp_bitIndex399,type,
bitIndex399: $i ).
thf(tp_bitIndex4,type,
bitIndex4: $i ).
thf(tp_bitIndex40,type,
bitIndex40: $i ).
thf(tp_bitIndex400,type,
bitIndex400: $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_bitIndex492,type,
bitIndex492: $i ).
thf(tp_bitIndex493,type,
bitIndex493: $i ).
thf(tp_bitIndex494,type,
bitIndex494: $i ).
thf(tp_bitIndex495,type,
bitIndex495: $i ).
thf(tp_bitIndex496,type,
bitIndex496: $i ).
thf(tp_bitIndex497,type,
bitIndex497: $i ).
thf(tp_bitIndex498,type,
bitIndex498: $i ).
thf(tp_bitIndex499,type,
bitIndex499: $i ).
thf(tp_bitIndex5,type,
bitIndex5: $i ).
thf(tp_bitIndex50,type,
bitIndex50: $i ).
thf(tp_bitIndex500,type,
bitIndex500: $i ).
thf(tp_bitIndex501,type,
bitIndex501: $i ).
thf(tp_bitIndex502,type,
bitIndex502: $i ).
thf(tp_bitIndex503,type,
bitIndex503: $i ).
thf(tp_bitIndex504,type,
bitIndex504: $i ).
thf(tp_bitIndex505,type,
bitIndex505: $i ).
thf(tp_bitIndex506,type,
bitIndex506: $i ).
thf(tp_bitIndex507,type,
bitIndex507: $i ).
thf(tp_bitIndex508,type,
bitIndex508: $i ).
thf(tp_bitIndex509,type,
bitIndex509: $i ).
thf(tp_bitIndex51,type,
bitIndex51: $i ).
thf(tp_bitIndex510,type,
bitIndex510: $i ).
thf(tp_bitIndex511,type,
bitIndex511: $i ).
thf(tp_bitIndex512,type,
bitIndex512: $i ).
thf(tp_bitIndex513,type,
bitIndex513: $i ).
thf(tp_bitIndex514,type,
bitIndex514: $i ).
thf(tp_bitIndex515,type,
bitIndex515: $i ).
thf(tp_bitIndex516,type,
bitIndex516: $i ).
thf(tp_bitIndex517,type,
bitIndex517: $i ).
thf(tp_bitIndex518,type,
bitIndex518: $i ).
thf(tp_bitIndex519,type,
bitIndex519: $i ).
thf(tp_bitIndex52,type,
bitIndex52: $i ).
thf(tp_bitIndex520,type,
bitIndex520: $i ).
thf(tp_bitIndex521,type,
bitIndex521: $i ).
thf(tp_bitIndex522,type,
bitIndex522: $i ).
thf(tp_bitIndex523,type,
bitIndex523: $i ).
thf(tp_bitIndex524,type,
bitIndex524: $i ).
thf(tp_bitIndex525,type,
bitIndex525: $i ).
thf(tp_bitIndex526,type,
bitIndex526: $i ).
thf(tp_bitIndex527,type,
bitIndex527: $i ).
thf(tp_bitIndex528,type,
bitIndex528: $i ).
thf(tp_bitIndex529,type,
bitIndex529: $i ).
thf(tp_bitIndex53,type,
bitIndex53: $i ).
thf(tp_bitIndex530,type,
bitIndex530: $i ).
thf(tp_bitIndex531,type,
bitIndex531: $i ).
thf(tp_bitIndex532,type,
bitIndex532: $i ).
thf(tp_bitIndex533,type,
bitIndex533: $i ).
thf(tp_bitIndex534,type,
bitIndex534: $i ).
thf(tp_bitIndex535,type,
bitIndex535: $i ).
thf(tp_bitIndex536,type,
bitIndex536: $i ).
thf(tp_bitIndex537,type,
bitIndex537: $i ).
thf(tp_bitIndex538,type,
bitIndex538: $i ).
thf(tp_bitIndex539,type,
bitIndex539: $i ).
thf(tp_bitIndex54,type,
bitIndex54: $i ).
thf(tp_bitIndex540,type,
bitIndex540: $i ).
thf(tp_bitIndex541,type,
bitIndex541: $i ).
thf(tp_bitIndex542,type,
bitIndex542: $i ).
thf(tp_bitIndex543,type,
bitIndex543: $i ).
thf(tp_bitIndex544,type,
bitIndex544: $i ).
thf(tp_bitIndex545,type,
bitIndex545: $i ).
thf(tp_bitIndex546,type,
bitIndex546: $i ).
thf(tp_bitIndex547,type,
bitIndex547: $i ).
thf(tp_bitIndex548,type,
bitIndex548: $i ).
thf(tp_bitIndex549,type,
bitIndex549: $i ).
thf(tp_bitIndex55,type,
bitIndex55: $i ).
thf(tp_bitIndex550,type,
bitIndex550: $i ).
thf(tp_bitIndex551,type,
bitIndex551: $i ).
thf(tp_bitIndex552,type,
bitIndex552: $i ).
thf(tp_bitIndex553,type,
bitIndex553: $i ).
thf(tp_bitIndex554,type,
bitIndex554: $i ).
thf(tp_bitIndex555,type,
bitIndex555: $i ).
thf(tp_bitIndex556,type,
bitIndex556: $i ).
thf(tp_bitIndex557,type,
bitIndex557: $i ).
thf(tp_bitIndex558,type,
bitIndex558: $i ).
thf(tp_bitIndex559,type,
bitIndex559: $i ).
thf(tp_bitIndex56,type,
bitIndex56: $i ).
thf(tp_bitIndex560,type,
bitIndex560: $i ).
thf(tp_bitIndex561,type,
bitIndex561: $i ).
thf(tp_bitIndex562,type,
bitIndex562: $i ).
thf(tp_bitIndex563,type,
bitIndex563: $i ).
thf(tp_bitIndex564,type,
bitIndex564: $i ).
thf(tp_bitIndex565,type,
bitIndex565: $i ).
thf(tp_bitIndex566,type,
bitIndex566: $i ).
thf(tp_bitIndex567,type,
bitIndex567: $i ).
thf(tp_bitIndex568,type,
bitIndex568: $i ).
thf(tp_bitIndex569,type,
bitIndex569: $i ).
thf(tp_bitIndex57,type,
bitIndex57: $i ).
thf(tp_bitIndex570,type,
bitIndex570: $i ).
thf(tp_bitIndex571,type,
bitIndex571: $i ).
thf(tp_bitIndex572,type,
bitIndex572: $i ).
thf(tp_bitIndex573,type,
bitIndex573: $i ).
thf(tp_bitIndex574,type,
bitIndex574: $i ).
thf(tp_bitIndex575,type,
bitIndex575: $i ).
thf(tp_bitIndex576,type,
bitIndex576: $i ).
thf(tp_bitIndex577,type,
bitIndex577: $i ).
thf(tp_bitIndex578,type,
bitIndex578: $i ).
thf(tp_bitIndex579,type,
bitIndex579: $i ).
thf(tp_bitIndex58,type,
bitIndex58: $i ).
thf(tp_bitIndex580,type,
bitIndex580: $i ).
thf(tp_bitIndex581,type,
bitIndex581: $i ).
thf(tp_bitIndex582,type,
bitIndex582: $i ).
thf(tp_bitIndex583,type,
bitIndex583: $i ).
thf(tp_bitIndex584,type,
bitIndex584: $i ).
thf(tp_bitIndex585,type,
bitIndex585: $i ).
thf(tp_bitIndex586,type,
bitIndex586: $i ).
thf(tp_bitIndex587,type,
bitIndex587: $i ).
thf(tp_bitIndex588,type,
bitIndex588: $i ).
thf(tp_bitIndex589,type,
bitIndex589: $i ).
thf(tp_bitIndex59,type,
bitIndex59: $i ).
thf(tp_bitIndex590,type,
bitIndex590: $i ).
thf(tp_bitIndex591,type,
bitIndex591: $i ).
thf(tp_bitIndex592,type,
bitIndex592: $i ).
thf(tp_bitIndex593,type,
bitIndex593: $i ).
thf(tp_bitIndex594,type,
bitIndex594: $i ).
thf(tp_bitIndex595,type,
bitIndex595: $i ).
thf(tp_bitIndex596,type,
bitIndex596: $i ).
thf(tp_bitIndex597,type,
bitIndex597: $i ).
thf(tp_bitIndex598,type,
bitIndex598: $i ).
thf(tp_bitIndex599,type,
bitIndex599: $i ).
thf(tp_bitIndex6,type,
bitIndex6: $i ).
thf(tp_bitIndex60,type,
bitIndex60: $i ).
thf(tp_bitIndex600,type,
bitIndex600: $i ).
thf(tp_bitIndex601,type,
bitIndex601: $i ).
thf(tp_bitIndex602,type,
bitIndex602: $i ).
thf(tp_bitIndex603,type,
bitIndex603: $i ).
thf(tp_bitIndex604,type,
bitIndex604: $i ).
thf(tp_bitIndex605,type,
bitIndex605: $i ).
thf(tp_bitIndex606,type,
bitIndex606: $i ).
thf(tp_bitIndex607,type,
bitIndex607: $i ).
thf(tp_bitIndex608,type,
bitIndex608: $i ).
thf(tp_bitIndex609,type,
bitIndex609: $i ).
thf(tp_bitIndex61,type,
bitIndex61: $i ).
thf(tp_bitIndex610,type,
bitIndex610: $i ).
thf(tp_bitIndex611,type,
bitIndex611: $i ).
thf(tp_bitIndex612,type,
bitIndex612: $i ).
thf(tp_bitIndex613,type,
bitIndex613: $i ).
thf(tp_bitIndex614,type,
bitIndex614: $i ).
thf(tp_bitIndex615,type,
bitIndex615: $i ).
thf(tp_bitIndex616,type,
bitIndex616: $i ).
thf(tp_bitIndex617,type,
bitIndex617: $i ).
thf(tp_bitIndex618,type,
bitIndex618: $i ).
thf(tp_bitIndex619,type,
bitIndex619: $i ).
thf(tp_bitIndex62,type,
bitIndex62: $i ).
thf(tp_bitIndex620,type,
bitIndex620: $i ).
thf(tp_bitIndex621,type,
bitIndex621: $i ).
thf(tp_bitIndex622,type,
bitIndex622: $i ).
thf(tp_bitIndex623,type,
bitIndex623: $i ).
thf(tp_bitIndex624,type,
bitIndex624: $i ).
thf(tp_bitIndex625,type,
bitIndex625: $i ).
thf(tp_bitIndex626,type,
bitIndex626: $i ).
thf(tp_bitIndex627,type,
bitIndex627: $i ).
thf(tp_bitIndex628,type,
bitIndex628: $i ).
thf(tp_bitIndex629,type,
bitIndex629: $i ).
thf(tp_bitIndex63,type,
bitIndex63: $i ).
thf(tp_bitIndex630,type,
bitIndex630: $i ).
thf(tp_bitIndex631,type,
bitIndex631: $i ).
thf(tp_bitIndex632,type,
bitIndex632: $i ).
thf(tp_bitIndex633,type,
bitIndex633: $i ).
thf(tp_bitIndex634,type,
bitIndex634: $i ).
thf(tp_bitIndex635,type,
bitIndex635: $i ).
thf(tp_bitIndex636,type,
bitIndex636: $i ).
thf(tp_bitIndex637,type,
bitIndex637: $i ).
thf(tp_bitIndex638,type,
bitIndex638: $i ).
thf(tp_bitIndex639,type,
bitIndex639: $i ).
thf(tp_bitIndex64,type,
bitIndex64: $i ).
thf(tp_bitIndex640,type,
bitIndex640: $i ).
thf(tp_bitIndex641,type,
bitIndex641: $i ).
thf(tp_bitIndex642,type,
bitIndex642: $i ).
thf(tp_bitIndex643,type,
bitIndex643: $i ).
thf(tp_bitIndex644,type,
bitIndex644: $i ).
thf(tp_bitIndex645,type,
bitIndex645: $i ).
thf(tp_bitIndex646,type,
bitIndex646: $i ).
thf(tp_bitIndex647,type,
bitIndex647: $i ).
thf(tp_bitIndex648,type,
bitIndex648: $i ).
thf(tp_bitIndex649,type,
bitIndex649: $i ).
thf(tp_bitIndex65,type,
bitIndex65: $i ).
thf(tp_bitIndex650,type,
bitIndex650: $i ).
thf(tp_bitIndex651,type,
bitIndex651: $i ).
thf(tp_bitIndex652,type,
bitIndex652: $i ).
thf(tp_bitIndex653,type,
bitIndex653: $i ).
thf(tp_bitIndex654,type,
bitIndex654: $i ).
thf(tp_bitIndex655,type,
bitIndex655: $i ).
thf(tp_bitIndex656,type,
bitIndex656: $i ).
thf(tp_bitIndex657,type,
bitIndex657: $i ).
thf(tp_bitIndex658,type,
bitIndex658: $i ).
thf(tp_bitIndex659,type,
bitIndex659: $i ).
thf(tp_bitIndex66,type,
bitIndex66: $i ).
thf(tp_bitIndex660,type,
bitIndex660: $i ).
thf(tp_bitIndex661,type,
bitIndex661: $i ).
thf(tp_bitIndex662,type,
bitIndex662: $i ).
thf(tp_bitIndex663,type,
bitIndex663: $i ).
thf(tp_bitIndex664,type,
bitIndex664: $i ).
thf(tp_bitIndex665,type,
bitIndex665: $i ).
thf(tp_bitIndex666,type,
bitIndex666: $i ).
thf(tp_bitIndex667,type,
bitIndex667: $i ).
thf(tp_bitIndex668,type,
bitIndex668: $i ).
thf(tp_bitIndex669,type,
bitIndex669: $i ).
thf(tp_bitIndex67,type,
bitIndex67: $i ).
thf(tp_bitIndex670,type,
bitIndex670: $i ).
thf(tp_bitIndex671,type,
bitIndex671: $i ).
thf(tp_bitIndex672,type,
bitIndex672: $i ).
thf(tp_bitIndex673,type,
bitIndex673: $i ).
thf(tp_bitIndex674,type,
bitIndex674: $i ).
thf(tp_bitIndex675,type,
bitIndex675: $i ).
thf(tp_bitIndex676,type,
bitIndex676: $i ).
thf(tp_bitIndex677,type,
bitIndex677: $i ).
thf(tp_bitIndex678,type,
bitIndex678: $i ).
thf(tp_bitIndex679,type,
bitIndex679: $i ).
thf(tp_bitIndex68,type,
bitIndex68: $i ).
thf(tp_bitIndex680,type,
bitIndex680: $i ).
thf(tp_bitIndex681,type,
bitIndex681: $i ).
thf(tp_bitIndex682,type,
bitIndex682: $i ).
thf(tp_bitIndex683,type,
bitIndex683: $i ).
thf(tp_bitIndex684,type,
bitIndex684: $i ).
thf(tp_bitIndex685,type,
bitIndex685: $i ).
thf(tp_bitIndex686,type,
bitIndex686: $i ).
thf(tp_bitIndex687,type,
bitIndex687: $i ).
thf(tp_bitIndex688,type,
bitIndex688: $i ).
thf(tp_bitIndex689,type,
bitIndex689: $i ).
thf(tp_bitIndex69,type,
bitIndex69: $i ).
thf(tp_bitIndex690,type,
bitIndex690: $i ).
thf(tp_bitIndex691,type,
bitIndex691: $i ).
thf(tp_bitIndex692,type,
bitIndex692: $i ).
thf(tp_bitIndex693,type,
bitIndex693: $i ).
thf(tp_bitIndex694,type,
bitIndex694: $i ).
thf(tp_bitIndex695,type,
bitIndex695: $i ).
thf(tp_bitIndex696,type,
bitIndex696: $i ).
thf(tp_bitIndex697,type,
bitIndex697: $i ).
thf(tp_bitIndex698,type,
bitIndex698: $i ).
thf(tp_bitIndex699,type,
bitIndex699: $i ).
thf(tp_bitIndex7,type,
bitIndex7: $i ).
thf(tp_bitIndex70,type,
bitIndex70: $i ).
thf(tp_bitIndex700,type,
bitIndex700: $i ).
thf(tp_bitIndex701,type,
bitIndex701: $i ).
thf(tp_bitIndex702,type,
bitIndex702: $i ).
thf(tp_bitIndex703,type,
bitIndex703: $i ).
thf(tp_bitIndex704,type,
bitIndex704: $i ).
thf(tp_bitIndex705,type,
bitIndex705: $i ).
thf(tp_bitIndex706,type,
bitIndex706: $i ).
thf(tp_bitIndex707,type,
bitIndex707: $i ).
thf(tp_bitIndex708,type,
bitIndex708: $i ).
thf(tp_bitIndex709,type,
bitIndex709: $i ).
thf(tp_bitIndex71,type,
bitIndex71: $i ).
thf(tp_bitIndex710,type,
bitIndex710: $i ).
thf(tp_bitIndex711,type,
bitIndex711: $i ).
thf(tp_bitIndex712,type,
bitIndex712: $i ).
thf(tp_bitIndex713,type,
bitIndex713: $i ).
thf(tp_bitIndex714,type,
bitIndex714: $i ).
thf(tp_bitIndex715,type,
bitIndex715: $i ).
thf(tp_bitIndex716,type,
bitIndex716: $i ).
thf(tp_bitIndex717,type,
bitIndex717: $i ).
thf(tp_bitIndex718,type,
bitIndex718: $i ).
thf(tp_bitIndex719,type,
bitIndex719: $i ).
thf(tp_bitIndex72,type,
bitIndex72: $i ).
thf(tp_bitIndex720,type,
bitIndex720: $i ).
thf(tp_bitIndex721,type,
bitIndex721: $i ).
thf(tp_bitIndex722,type,
bitIndex722: $i ).
thf(tp_bitIndex723,type,
bitIndex723: $i ).
thf(tp_bitIndex724,type,
bitIndex724: $i ).
thf(tp_bitIndex725,type,
bitIndex725: $i ).
thf(tp_bitIndex726,type,
bitIndex726: $i ).
thf(tp_bitIndex727,type,
bitIndex727: $i ).
thf(tp_bitIndex728,type,
bitIndex728: $i ).
thf(tp_bitIndex729,type,
bitIndex729: $i ).
thf(tp_bitIndex73,type,
bitIndex73: $i ).
thf(tp_bitIndex730,type,
bitIndex730: $i ).
thf(tp_bitIndex731,type,
bitIndex731: $i ).
thf(tp_bitIndex732,type,
bitIndex732: $i ).
thf(tp_bitIndex733,type,
bitIndex733: $i ).
thf(tp_bitIndex734,type,
bitIndex734: $i ).
thf(tp_bitIndex735,type,
bitIndex735: $i ).
thf(tp_bitIndex736,type,
bitIndex736: $i ).
thf(tp_bitIndex737,type,
bitIndex737: $i ).
thf(tp_bitIndex74,type,
bitIndex74: $i ).
thf(tp_bitIndex75,type,
bitIndex75: $i ).
thf(tp_bitIndex76,type,
bitIndex76: $i ).
thf(tp_bitIndex77,type,
bitIndex77: $i ).
thf(tp_bitIndex78,type,
bitIndex78: $i ).
thf(tp_bitIndex79,type,
bitIndex79: $i ).
thf(tp_bitIndex8,type,
bitIndex8: $i ).
thf(tp_bitIndex80,type,
bitIndex80: $i ).
thf(tp_bitIndex81,type,
bitIndex81: $i ).
thf(tp_bitIndex82,type,
bitIndex82: $i ).
thf(tp_bitIndex83,type,
bitIndex83: $i ).
thf(tp_bitIndex84,type,
bitIndex84: $i ).
thf(tp_bitIndex85,type,
bitIndex85: $i ).
thf(tp_bitIndex86,type,
bitIndex86: $i ).
thf(tp_bitIndex87,type,
bitIndex87: $i ).
thf(tp_bitIndex88,type,
bitIndex88: $i ).
thf(tp_bitIndex89,type,
bitIndex89: $i ).
thf(tp_bitIndex9,type,
bitIndex9: $i ).
thf(tp_bitIndex90,type,
bitIndex90: $i ).
thf(tp_bitIndex91,type,
bitIndex91: $i ).
thf(tp_bitIndex92,type,
bitIndex92: $i ).
thf(tp_bitIndex93,type,
bitIndex93: $i ).
thf(tp_bitIndex94,type,
bitIndex94: $i ).
thf(tp_bitIndex95,type,
bitIndex95: $i ).
thf(tp_bitIndex96,type,
bitIndex96: $i ).
thf(tp_bitIndex97,type,
bitIndex97: $i ).
thf(tp_bitIndex98,type,
bitIndex98: $i ).
thf(tp_bitIndex99,type,
bitIndex99: $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_122_0,type,
range_122_0: $i > $o ).
thf(tp_range_122_116,type,
range_122_116: $i > $o ).
thf(tp_range_1_0,type,
range_1_0: $i > $o ).
thf(tp_range_2_0,type,
range_2_0: $i > $o ).
thf(tp_range_31_0,type,
range_31_0: $i > $o ).
thf(tp_range_3_0,type,
range_3_0: $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_7_0,type,
range_7_0: $i > $o ).
thf(tp_range_8_0,type,
range_8_0: $i > $o ).
thf(tp_range_8_1,type,
range_8_1: $i > $o ).
thf(tp_reachableState,type,
reachableState: $i > $o ).
thf(tp_sP11_v558_bitIndex1,type,
sP11_v558_bitIndex1: $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_sP1_v52_bitIndex8,type,
sP1_v52_bitIndex8: $i > $o ).
thf(tp_sP292_aig_name,type,
sP292_aig_name: $i > $o ).
thf(tp_sP293_aig_name,type,
sP293_aig_name: $i > $o ).
thf(tp_sP294_aig_name,type,
sP294_aig_name: $i > $o ).
thf(tp_sP295,type,
sP295: $i > $o ).
thf(tp_sP296,type,
sP296: $i > $o ).
thf(tp_sP297,type,
sP297: $i > $o ).
thf(tp_sP298,type,
sP298: $i > $o ).
thf(tp_sP299,type,
sP299: $i > $o ).
thf(tp_sP300,type,
sP300: $i > $o ).
thf(tp_sP301,type,
sP301: $i > $o ).
thf(tp_sP302,type,
sP302: $i > $o ).
thf(tp_sP303,type,
sP303: $i > $o ).
thf(tp_sP304,type,
sP304: $i > $o ).
thf(tp_sP305,type,
sP305: $i > $o ).
thf(tp_sP306,type,
sP306: $i > $o ).
thf(tp_sP307,type,
sP307: $i > $o ).
thf(tp_sP308,type,
sP308: $i > $o ).
thf(tp_sP309,type,
sP309: $i > $o ).
thf(tp_sP310,type,
sP310: $i > $o ).
thf(tp_sP311,type,
sP311: $i > $o ).
thf(tp_sP312,type,
sP312: $i > $o ).
thf(tp_sP313,type,
sP313: $i > $o ).
thf(tp_sP314,type,
sP314: $i > $o ).
thf(tp_sP315,type,
sP315: $i > $o ).
thf(tp_sP316,type,
sP316: $i > $o ).
thf(tp_sP317,type,
sP317: $i > $o ).
thf(tp_sP318,type,
sP318: $i > $o ).
thf(tp_sP319,type,
sP319: $i > $o ).
thf(tp_sP320,type,
sP320: $i > $o ).
thf(tp_sP321,type,
sP321: $i > $o ).
thf(tp_sP322,type,
sP322: $i > $o ).
thf(tp_sP323,type,
sP323: $i > $o ).
thf(tp_sP324,type,
sP324: $i > $o ).
thf(tp_sP325,type,
sP325: $i > $o ).
thf(tp_sP326,type,
sP326: $i > $o ).
thf(tp_sP327,type,
sP327: $i > $o ).
thf(tp_sP328,type,
sP328: $i > $o ).
thf(tp_sP329,type,
sP329: $i > $o ).
thf(tp_sP330,type,
sP330: $i > $o ).
thf(tp_sP331,type,
sP331: $i > $o ).
thf(tp_sP332,type,
sP332: $i > $o ).
thf(tp_sP333,type,
sP333: $i > $o ).
thf(tp_sP334,type,
sP334: $i > $o ).
thf(tp_sP335,type,
sP335: $i > $o ).
thf(tp_sP336,type,
sP336: $i > $o ).
thf(tp_sP337,type,
sP337: $i > $o ).
thf(tp_sP338,type,
sP338: $i > $o ).
thf(tp_sP339,type,
sP339: $i > $o ).
thf(tp_sP340,type,
sP340: $i > $o ).
thf(tp_sP341,type,
sP341: $i > $o ).
thf(tp_sP342,type,
sP342: $i > $o ).
thf(tp_sP343,type,
sP343: $i > $o ).
thf(tp_sP344,type,
sP344: $i > $o ).
thf(tp_sP345,type,
sP345: $i > $o ).
thf(tp_sP346,type,
sP346: $i > $o ).
thf(tp_sP347,type,
sP347: $i > $o ).
thf(tp_sP348,type,
sP348: $i > $o ).
thf(tp_sP349,type,
sP349: $i > $o ).
thf(tp_sP350,type,
sP350: $i > $o ).
thf(tp_sP351,type,
sP351: $i > $o ).
thf(tp_sP352,type,
sP352: $i > $o ).
thf(tp_sP353,type,
sP353: $i > $o ).
thf(tp_sP354,type,
sP354: $i > $o ).
thf(tp_sP355,type,
sP355: $i > $o ).
thf(tp_sP356,type,
sP356: $i > $o ).
thf(tp_sP357,type,
sP357: $i > $o ).
thf(tp_sP358,type,
sP358: $i > $o ).
thf(tp_sP359,type,
sP359: $i > $o ).
thf(tp_sP360,type,
sP360: $i > $o ).
thf(tp_sP361,type,
sP361: $i > $o ).
thf(tp_sP362,type,
sP362: $i > $o ).
thf(tp_sP363,type,
sP363: $i > $o ).
thf(tp_sP364,type,
sP364: $i > $o ).
thf(tp_sP365,type,
sP365: $i > $o ).
thf(tp_sP366,type,
sP366: $i > $o ).
thf(tp_sP367,type,
sP367: $i > $o ).
thf(tp_sP368,type,
sP368: $i > $o ).
thf(tp_sP369,type,
sP369: $i > $o ).
thf(tp_sP370,type,
sP370: $i > $o ).
thf(tp_sP371,type,
sP371: $i > $o ).
thf(tp_sP372,type,
sP372: $i > $o ).
thf(tp_sP373,type,
sP373: $i > $o ).
thf(tp_sP374,type,
sP374: $i > $o ).
thf(tp_sP375,type,
sP375: $i > $o ).
thf(tp_sP376,type,
sP376: $i > $o ).
thf(tp_sP377,type,
sP377: $i > $o ).
thf(tp_sP378,type,
sP378: $i > $o ).
thf(tp_sP379,type,
sP379: $i > $o ).
thf(tp_sP380,type,
sP380: $i > $o ).
thf(tp_sP381,type,
sP381: $i > $o ).
thf(tp_sP382,type,
sP382: $i > $o ).
thf(tp_sP383,type,
sP383: $i > $o ).
thf(tp_sP384,type,
sP384: $i > $o ).
thf(tp_sP385,type,
sP385: $i > $o ).
thf(tp_sP386,type,
sP386: $i > $o ).
thf(tp_sP387,type,
sP387: $i > $o ).
thf(tp_sP388,type,
sP388: $i > $o ).
thf(tp_sP389,type,
sP389: $i > $o ).
thf(tp_sP390,type,
sP390: $i > $o ).
thf(tp_sP391,type,
sP391: $i > $o ).
thf(tp_sP392,type,
sP392: $i > $o ).
thf(tp_sP393,type,
sP393: $i > $o ).
thf(tp_sP394,type,
sP394: $i > $o ).
thf(tp_sP395,type,
sP395: $i > $o ).
thf(tp_sP396,type,
sP396: $i > $o ).
thf(tp_sP397,type,
sP397: $i > $o ).
thf(tp_sP398,type,
sP398: $i > $o ).
thf(tp_sP399,type,
sP399: $i > $o ).
thf(tp_sP400,type,
sP400: $i > $o ).
thf(tp_sP401,type,
sP401: $i > $o ).
thf(tp_sP402,type,
sP402: $i > $o ).
thf(tp_sP403,type,
sP403: $i > $o ).
thf(tp_sP404,type,
sP404: $i > $o ).
thf(tp_sP405,type,
sP405: $i > $o ).
thf(tp_sP406,type,
sP406: $i > $o ).
thf(tp_sP407,type,
sP407: $i > $o ).
thf(tp_sP408,type,
sP408: $i > $o ).
thf(tp_sP409,type,
sP409: $i > $o ).
thf(tp_sP410,type,
sP410: $i > $o ).
thf(tp_sP411,type,
sP411: $i > $o ).
thf(tp_sP412,type,
sP412: $i > $o ).
thf(tp_sP413,type,
sP413: $i > $o ).
thf(tp_sP414,type,
sP414: $i > $o ).
thf(tp_sP415,type,
sP415: $i > $o ).
thf(tp_sP416,type,
sP416: $i > $o ).
thf(tp_sP417,type,
sP417: $i > $o ).
thf(tp_sP418,type,
sP418: $i > $o ).
thf(tp_sP419,type,
sP419: $i > $o ).
thf(tp_sP420,type,
sP420: $i > $o ).
thf(tp_sP421,type,
sP421: $i > $o ).
thf(tp_sP422,type,
sP422: $i > $o ).
thf(tp_sP423,type,
sP423: $i > $o ).
thf(tp_sP424,type,
sP424: $i > $o ).
thf(tp_sP425,type,
sP425: $i > $o ).
thf(tp_sP426,type,
sP426: $i > $o ).
thf(tp_sP427,type,
sP427: $i > $o ).
thf(tp_sP428,type,
sP428: $i > $o ).
thf(tp_sP429,type,
sP429: $i > $o ).
thf(tp_sP430,type,
sP430: $i > $o ).
thf(tp_sP431,type,
sP431: $i > $o ).
thf(tp_sP432,type,
sP432: $i > $o ).
thf(tp_sP433,type,
sP433: $i > $o ).
thf(tp_sP434,type,
sP434: $i > $o ).
thf(tp_sP435,type,
sP435: $i > $o ).
thf(tp_sP436,type,
sP436: $i > $o ).
thf(tp_sP437,type,
sP437: $i > $o ).
thf(tp_sP438,type,
sP438: $i > $o ).
thf(tp_sP439,type,
sP439: $i > $o ).
thf(tp_sP440,type,
sP440: $i > $o ).
thf(tp_sP441,type,
sP441: $i > $o ).
thf(tp_sP442,type,
sP442: $i > $o ).
thf(tp_sP443,type,
sP443: $i > $i > $o ).
thf(tp_sP444,type,
sP444: $i > $i > $o ).
thf(tp_sP445,type,
sP445: $i > $i > $o ).
thf(tp_sP446,type,
sP446: $i > $i > $o ).
thf(tp_sP447,type,
sP447: $i > $i > $o ).
thf(tp_sP448,type,
sP448: $i > $i > $o ).
thf(tp_sP449,type,
sP449: $i > $i > $o ).
thf(tp_sP450,type,
sP450: $i > $i > $o ).
thf(tp_sP451,type,
sP451: $i > $i > $o ).
thf(tp_sP452,type,
sP452: $i > $i > $o ).
thf(tp_sP453,type,
sP453: $i > $i > $o ).
thf(tp_sP454,type,
sP454: $i > $i > $o ).
thf(tp_sP455,type,
sP455: $i > $i > $o ).
thf(tp_sP456,type,
sP456: $i > $i > $o ).
thf(tp_sP457,type,
sP457: $i > $i > $o ).
thf(tp_sP458,type,
sP458: $i > $i > $o ).
thf(tp_sP459,type,
sP459: $i > $i > $o ).
thf(tp_sP460,type,
sP460: $i > $i > $o ).
thf(tp_sP461,type,
sP461: $i > $i > $o ).
thf(tp_sP462,type,
sP462: $i > $i > $o ).
thf(tp_sP463,type,
sP463: $i > $i > $o ).
thf(tp_sP464,type,
sP464: $i > $i > $o ).
thf(tp_sP465,type,
sP465: $i > $i > $o ).
thf(tp_sP466,type,
sP466: $i > $i > $o ).
thf(tp_sP467,type,
sP467: $i > $i > $o ).
thf(tp_sP468,type,
sP468: $i > $i > $o ).
thf(tp_sP469,type,
sP469: $i > $i > $o ).
thf(tp_sP470,type,
sP470: $i > $i > $o ).
thf(tp_sP471,type,
sP471: $i > $i > $o ).
thf(tp_sP472,type,
sP472: $i > $i > $o ).
thf(tp_sP473,type,
sP473: $i > $i > $o ).
thf(tp_sP474,type,
sP474: $i > $i > $o ).
thf(tp_sP475,type,
sP475: $i > $i > $o ).
thf(tp_sP476,type,
sP476: $i > $i > $o ).
thf(tp_sP477,type,
sP477: $i > $i > $o ).
thf(tp_sP478,type,
sP478: $i > $i > $o ).
thf(tp_sP479,type,
sP479: $i > $i > $o ).
thf(tp_sP480,type,
sP480: $i > $i > $o ).
thf(tp_sP481,type,
sP481: $i > $i > $o ).
thf(tp_sP482,type,
sP482: $i > $i > $o ).
thf(tp_sP483,type,
sP483: $i > $i > $o ).
thf(tp_sP484,type,
sP484: $i > $i > $o ).
thf(tp_sP485,type,
sP485: $i > $i > $o ).
thf(tp_sP486,type,
sP486: $i > $i > $o ).
thf(tp_sP487,type,
sP487: $i > $i > $o ).
thf(tp_sP488,type,
sP488: $i > $i > $o ).
thf(tp_sP489,type,
sP489: $i > $i > $o ).
thf(tp_sP490,type,
sP490: $i > $i > $o ).
thf(tp_sP491,type,
sP491: $i > $i > $o ).
thf(tp_sP492,type,
sP492: $i > $i > $o ).
thf(tp_sP493,type,
sP493: $i > $i > $o ).
thf(tp_sP494,type,
sP494: $i > $i > $o ).
thf(tp_sP495,type,
sP495: $i > $i > $o ).
thf(tp_sP496,type,
sP496: $i > $i > $o ).
thf(tp_sP497,type,
sP497: $i > $i > $o ).
thf(tp_sP498,type,
sP498: $i > $i > $o ).
thf(tp_sP499,type,
sP499: $i > $i > $o ).
thf(tp_sP500,type,
sP500: $i > $i > $o ).
thf(tp_sP501,type,
sP501: $i > $i > $o ).
thf(tp_sP502,type,
sP502: $i > $i > $o ).
thf(tp_sP503,type,
sP503: $i > $i > $o ).
thf(tp_sP504,type,
sP504: $i > $i > $o ).
thf(tp_sP505,type,
sP505: $i > $i > $o ).
thf(tp_sP506,type,
sP506: $i > $i > $o ).
thf(tp_sP507,type,
sP507: $i > $i > $o ).
thf(tp_sP508,type,
sP508: $i > $i > $o ).
thf(tp_sP509,type,
sP509: $i > $i > $o ).
thf(tp_sP510,type,
sP510: $i > $i > $o ).
thf(tp_sP511,type,
sP511: $i > $i > $o ).
thf(tp_sP512,type,
sP512: $i > $i > $o ).
thf(tp_sP513,type,
sP513: $i > $i > $o ).
thf(tp_sP514,type,
sP514: $i > $i > $o ).
thf(tp_sP515,type,
sP515: $i > $i > $o ).
thf(tp_sP516,type,
sP516: $i > $i > $o ).
thf(tp_sP517,type,
sP517: $i > $i > $o ).
thf(tp_sP518,type,
sP518: $i > $i > $o ).
thf(tp_sP519,type,
sP519: $i > $i > $o ).
thf(tp_sP520,type,
sP520: $i > $i > $o ).
thf(tp_sP521,type,
sP521: $i > $i > $o ).
thf(tp_sP522,type,
sP522: $i > $i > $o ).
thf(tp_sP523,type,
sP523: $i > $i > $o ).
thf(tp_sP524,type,
sP524: $i > $i > $o ).
thf(tp_sP525,type,
sP525: $i > $i > $o ).
thf(tp_sP526,type,
sP526: $i > $i > $o ).
thf(tp_sP527,type,
sP527: $i > $i > $o ).
thf(tp_sP528,type,
sP528: $i > $i > $o ).
thf(tp_sP529,type,
sP529: $i > $i > $o ).
thf(tp_sP530,type,
sP530: $i > $i > $o ).
thf(tp_sP531,type,
sP531: $i > $i > $o ).
thf(tp_sP532,type,
sP532: $i > $i > $o ).
thf(tp_sP533,type,
sP533: $i > $i > $o ).
thf(tp_sP534,type,
sP534: $i > $i > $o ).
thf(tp_sP535,type,
sP535: $i > $i > $o ).
thf(tp_sP536,type,
sP536: $i > $i > $o ).
thf(tp_sP537,type,
sP537: $i > $i > $o ).
thf(tp_sP538,type,
sP538: $i > $i > $o ).
thf(tp_sP539,type,
sP539: $i > $i > $o ).
thf(tp_sP540,type,
sP540: $i > $i > $o ).
thf(tp_sP541,type,
sP541: $i > $i > $o ).
thf(tp_sP542,type,
sP542: $i > $i > $o ).
thf(tp_sP543,type,
sP543: $i > $i > $o ).
thf(tp_sP544,type,
sP544: $i > $i > $o ).
thf(tp_sP545,type,
sP545: $i > $i > $o ).
thf(tp_sP546,type,
sP546: $i > $i > $o ).
thf(tp_sP547,type,
sP547: $i > $i > $o ).
thf(tp_sP548,type,
sP548: $i > $i > $o ).
thf(tp_sP549,type,
sP549: $i > $i > $o ).
thf(tp_sP550,type,
sP550: $i > $i > $o ).
thf(tp_sP551,type,
sP551: $i > $i > $o ).
thf(tp_sP552,type,
sP552: $i > $i > $o ).
thf(tp_sP553,type,
sP553: $i > $i > $o ).
thf(tp_sP554,type,
sP554: $i > $i > $o ).
thf(tp_sP555,type,
sP555: $i > $i > $o ).
thf(tp_sP556,type,
sP556: $i > $i > $o ).
thf(tp_sP557,type,
sP557: $i > $i > $o ).
thf(tp_sP558,type,
sP558: $i > $i > $o ).
thf(tp_sP559,type,
sP559: $i > $i > $o ).
thf(tp_sP560,type,
sP560: $i > $i > $o ).
thf(tp_sP561,type,
sP561: $i > $i > $o ).
thf(tp_sP562,type,
sP562: $i > $i > $o ).
thf(tp_sP563,type,
sP563: $i > $i > $o ).
thf(tp_sP564,type,
sP564: $i > $i > $o ).
thf(tp_sP565,type,
sP565: $i > $i > $o ).
thf(tp_sP566,type,
sP566: $i > $i > $o ).
thf(tp_sP567,type,
sP567: $i > $i > $o ).
thf(tp_sP568,type,
sP568: $i > $o ).
thf(tp_sP569,type,
sP569: $i > $o ).
thf(tp_sP570,type,
sP570: $i > $o ).
thf(tp_sP571,type,
sP571: $i > $o ).
thf(tp_sP572,type,
sP572: $i > $o ).
thf(tp_sP6_v310_bitIndex2,type,
sP6_v310_bitIndex2: $i > $o ).
thf(tp_sP9_v318_bitIndex6,type,
sP9_v318_bitIndex6: $i > $o ).
thf(tp_v1,type,
v1: $i > $o ).
thf(tp_v1000,type,
v1000: $i > $i > $o ).
thf(tp_v1007,type,
v1007: $i > $i > $o ).
thf(tp_v118,type,
v118: $i > $o ).
thf(tp_v119,type,
v119: $i > $i > $o ).
thf(tp_v120,type,
v120: $i > $i > $o ).
thf(tp_v121,type,
v121: $i > $o ).
thf(tp_v122,type,
v122: $i > $i > $o ).
thf(tp_v127,type,
v127: $i > $o ).
thf(tp_v128,type,
v128: $i > $o ).
thf(tp_v129,type,
v129: $i > $o ).
thf(tp_v148,type,
v148: $i > $i > $o ).
thf(tp_v159,type,
v159: $i > $o ).
thf(tp_v160,type,
v160: $i > $o ).
thf(tp_v161,type,
v161: $i > $o ).
thf(tp_v163,type,
v163: $i > $o ).
thf(tp_v167,type,
v167: $i > $i > $o ).
thf(tp_v169,type,
v169: $i > $i > $o ).
thf(tp_v179,type,
v179: $i > $i > $o ).
thf(tp_v183,type,
v183: $i > $i > $o ).
thf(tp_v20,type,
v20: $i > $o ).
thf(tp_v201,type,
v201: $i > $o ).
thf(tp_v203,type,
v203: $i > $i > $o ).
thf(tp_v207,type,
v207: $i > $o ).
thf(tp_v23,type,
v23: $i > $i > $o ).
thf(tp_v237,type,
v237: $i > $i > $o ).
thf(tp_v242,type,
v242: $i > $i > $o ).
thf(tp_v260,type,
v260: $i > $i > $o ).
thf(tp_v269,type,
v269: $i > $o ).
thf(tp_v271,type,
v271: $i > $i > $o ).
thf(tp_v274,type,
v274: $i > $i > $o ).
thf(tp_v29,type,
v29: $i > $i > $o ).
thf(tp_v31,type,
v31: $i > $i > $o ).
thf(tp_v323,type,
v323: $i > $i > $o ).
thf(tp_v327,type,
v327: $i > $i > $o ).
thf(tp_v329,type,
v329: $i > $i > $o ).
thf(tp_v334,type,
v334: $i > $i > $o ).
thf(tp_v340,type,
v340: $i > $i > $o ).
thf(tp_v350,type,
v350: $i > $i > $o ).
thf(tp_v352,type,
v352: $i > $i > $o ).
thf(tp_v354,type,
v354: $i > $i > $o ).
thf(tp_v358,type,
v358: $i > $o ).
thf(tp_v365,type,
v365: $i > $o ).
thf(tp_v366,type,
v366: $i > $o ).
thf(tp_v367,type,
v367: $i > $i > $o ).
thf(tp_v37,type,
v37: $i > $i > $o ).
thf(tp_v371,type,
v371: $i > $i > $o ).
thf(tp_v372,type,
v372: $i > $o ).
thf(tp_v376,type,
v376: $i > $o ).
thf(tp_v378,type,
v378: $i > $o ).
thf(tp_v380,type,
v380: $i > $o ).
thf(tp_v381,type,
v381: $i > $o ).
thf(tp_v385,type,
v385: $i > $o ).
thf(tp_v387,type,
v387: $i > $o ).
thf(tp_v388,type,
v388: $i > $o ).
thf(tp_v392,type,
v392: $i > $o ).
thf(tp_v393,type,
v393: $i > $i > $o ).
thf(tp_v394,type,
v394: $i > $i > $o ).
thf(tp_v399,type,
v399: $i > $o ).
thf(tp_v40,type,
v40: $i > $i > $o ).
thf(tp_v415,type,
v415: $i > $o ).
thf(tp_v416,type,
v416: $i > $i > $o ).
thf(tp_v417,type,
v417: $i > $i > $o ).
thf(tp_v422,type,
v422: $i > $o ).
thf(tp_v423,type,
v423: $i > $o ).
thf(tp_v431,type,
v431: $i > $o ).
thf(tp_v434,type,
v434: $i > $i > $o ).
thf(tp_v436,type,
v436: $i > $i > $o ).
thf(tp_v443,type,
v443: $i > $o ).
thf(tp_v444,type,
v444: $i > $o ).
thf(tp_v445,type,
v445: $i > $o ).
thf(tp_v447,type,
v447: $i > $o ).
thf(tp_v451,type,
v451: $i > $i > $o ).
thf(tp_v453,type,
v453: $i > $i > $o ).
thf(tp_v461,type,
v461: $i > $o ).
thf(tp_v465,type,
v465: $i > $o ).
thf(tp_v468,type,
v468: $i > $o ).
thf(tp_v469,type,
v469: $i > $i > $o ).
thf(tp_v470,type,
v470: $i > $o ).
thf(tp_v471,type,
v471: $i > $i > $o ).
thf(tp_v472,type,
v472: $i > $i > $o ).
thf(tp_v473,type,
v473: $i > $o ).
thf(tp_v474,type,
v474: $i > $i > $o ).
thf(tp_v475,type,
v475: $i > $i > $o ).
thf(tp_v480,type,
v480: $i > $o ).
thf(tp_v481,type,
v481: $i > $i > $o ).
thf(tp_v484,type,
v484: $i > $o ).
thf(tp_v498,type,
v498: $i > $o ).
thf(tp_v499,type,
v499: $i > $i > $o ).
thf(tp_v500,type,
v500: $i > $i > $o ).
thf(tp_v501,type,
v501: $i > $o ).
thf(tp_v502,type,
v502: $i > $i > $o ).
thf(tp_v507,type,
v507: $i > $o ).
thf(tp_v516,type,
v516: $i > $i > $o ).
thf(tp_v521,type,
v521: $i > $o ).
thf(tp_v522,type,
v522: $i > $o ).
thf(tp_v523,type,
v523: $i > $o ).
thf(tp_v525,type,
v525: $i > $o ).
thf(tp_v529,type,
v529: $i > $i > $o ).
thf(tp_v531,type,
v531: $i > $i > $o ).
thf(tp_v537,type,
v537: $i > $o ).
thf(tp_v539,type,
v539: $i > $i > $o ).
thf(tp_v544,type,
v544: $i > $o ).
thf(tp_v546,type,
v546: $i > $o ).
thf(tp_v550,type,
v550: $i > $o ).
thf(tp_v553,type,
v553: $i > $o ).
thf(tp_v554,type,
v554: $i > $o ).
thf(tp_v555,type,
v555: $i > $o ).
thf(tp_v556,type,
v556: $i > $o ).
thf(tp_v560,type,
v560: $i > $i > $o ).
thf(tp_v561,type,
v561: $i > $i > $o ).
thf(tp_v562,type,
v562: $i > $i > $o ).
thf(tp_v568,type,
v568: $i > $o ).
thf(tp_v569,type,
v569: $i > $o ).
thf(tp_v570,type,
v570: $i > $o ).
thf(tp_v572,type,
v572: $i > $o ).
thf(tp_v578,type,
v578: $i > $o ).
thf(tp_v586,type,
v586: $i > $o ).
thf(tp_v588,type,
v588: $i > $o ).
thf(tp_v589,type,
v589: $i > $o ).
thf(tp_v593,type,
v593: $i > $i > $o ).
thf(tp_v595,type,
v595: $i > $i > $o ).
thf(tp_v597,type,
v597: $i > $i > $o ).
thf(tp_v599,type,
v599: $i > $i > $o ).
thf(tp_v60,type,
v60: $i > $o ).
thf(tp_v602,type,
v602: $i > $i > $o ).
thf(tp_v608,type,
v608: $i > $i > $o ).
thf(tp_v610,type,
v610: $i > $i > $o ).
thf(tp_v611,type,
v611: $i > $i > $o ).
thf(tp_v612,type,
v612: $i > $o ).
thf(tp_v613,type,
v613: $i > $i > $o ).
thf(tp_v614,type,
v614: $i > $o ).
thf(tp_v615,type,
v615: $i > $i > $o ).
thf(tp_v616,type,
v616: $i > $i > $o ).
thf(tp_v618,type,
v618: $i > $o ).
thf(tp_v619,type,
v619: $i > $i > $o ).
thf(tp_v62,type,
v62: $i > $o ).
thf(tp_v620,type,
v620: $i > $i > $o ).
thf(tp_v623,type,
v623: $i > $i > $o ).
thf(tp_v625,type,
v625: $i > $i > $o ).
thf(tp_v627,type,
v627: $i > $i > $o ).
thf(tp_v629,type,
v629: $i > $i > $o ).
thf(tp_v631,type,
v631: $i > $i > $o ).
thf(tp_v633,type,
v633: $i > $i > $o ).
thf(tp_v635,type,
v635: $i > $i > $o ).
thf(tp_v637,type,
v637: $i > $i > $o ).
thf(tp_v639,type,
v639: $i > $i > $o ).
thf(tp_v641,type,
v641: $i > $i > $o ).
thf(tp_v642,type,
v642: $i > $i > $o ).
thf(tp_v644,type,
v644: $i > $i > $o ).
thf(tp_v648,type,
v648: $i > $i > $o ).
thf(tp_v649,type,
v649: $i > $i > $o ).
thf(tp_v651,type,
v651: $i > $i > $o ).
thf(tp_v652,type,
v652: $i > $o ).
thf(tp_v653,type,
v653: $i > $o ).
thf(tp_v654,type,
v654: $i > $o ).
thf(tp_v660,type,
v660: $i > $o ).
thf(tp_v666,type,
v666: $i > $o ).
thf(tp_v667,type,
v667: $i > $i > $o ).
thf(tp_v668,type,
v668: $i > $o ).
thf(tp_v669,type,
v669: $i > $i > $o ).
thf(tp_v671,type,
v671: $i > $i > $o ).
thf(tp_v676,type,
v676: $i > $i > $o ).
thf(tp_v677,type,
v677: $i > $i > $o ).
thf(tp_v679,type,
v679: $i > $i > $o ).
thf(tp_v680,type,
v680: $i > $i > $o ).
thf(tp_v692,type,
v692: $i > $i > $o ).
thf(tp_v694,type,
v694: $i > $o ).
thf(tp_v695,type,
v695: $i > $o ).
thf(tp_v697,type,
v697: $i > $o ).
thf(tp_v705,type,
v705: $i > $i > $o ).
thf(tp_v73,type,
v73: $i > $o ).
thf(tp_v74,type,
v74: $i > $i > $o ).
thf(tp_v75,type,
v75: $i > $o ).
thf(tp_v750,type,
v750: $i > $i > $o ).
thf(tp_v759,type,
v759: $i > $o ).
thf(tp_v76,type,
v76: $i > $i > $o ).
thf(tp_v77,type,
v77: $i > $i > $o ).
thf(tp_v775,type,
v775: $i > $o ).
thf(tp_v777,type,
v777: $i > $o ).
thf(tp_v78,type,
v78: $i > $o ).
thf(tp_v780,type,
v780: $i > $o ).
thf(tp_v783,type,
v783: $i > $o ).
thf(tp_v784,type,
v784: $i > $o ).
thf(tp_v785,type,
v785: $i > $o ).
thf(tp_v789,type,
v789: $i > $o ).
thf(tp_v79,type,
v79: $i > $i > $o ).
thf(tp_v791,type,
v791: $i > $o ).
thf(tp_v8,type,
v8: $i > $i > $o ).
thf(tp_v80,type,
v80: $i > $i > $o ).
thf(tp_v800,type,
v800: $i > $o ).
thf(tp_v801,type,
v801: $i > $o ).
thf(tp_v808,type,
v808: $i > $o ).
thf(tp_v809,type,
v809: $i > $o ).
thf(tp_v813,type,
v813: $i > $o ).
thf(tp_v814,type,
v814: $i > $o ).
thf(tp_v815,type,
v815: $i > $o ).
thf(tp_v817,type,
v817: $i > $o ).
thf(tp_v821,type,
v821: $i > $o ).
thf(tp_v823,type,
v823: $i > $o ).
thf(tp_v829,type,
v829: $i > $o ).
thf(tp_v830,type,
v830: $i > $o ).
thf(tp_v831,type,
v831: $i > $o ).
thf(tp_v833,type,
v833: $i > $o ).
thf(tp_v834,type,
v834: $i > $o ).
thf(tp_v836,type,
v836: $i > $o ).
thf(tp_v837,type,
v837: $i > $i > $o ).
thf(tp_v838,type,
v838: $i > $o ).
thf(tp_v839,type,
v839: $i > $i > $o ).
thf(tp_v840,type,
v840: $i > $i > $o ).
thf(tp_v841,type,
v841: $i > $o ).
thf(tp_v842,type,
v842: $i > $i > $o ).
thf(tp_v843,type,
v843: $i > $i > $o ).
thf(tp_v848,type,
v848: $i > $o ).
thf(tp_v849,type,
v849: $i > $i > $o ).
thf(tp_v85,type,
v85: $i > $o ).
thf(tp_v851,type,
v851: $i > $o ).
thf(tp_v853,type,
v853: $i > $o ).
thf(tp_v855,type,
v855: $i > $o ).
thf(tp_v86,type,
v86: $i > $i > $o ).
thf(tp_v879,type,
v879: $i > $o ).
thf(tp_v880,type,
v880: $i > $i > $o ).
thf(tp_v881,type,
v881: $i > $i > $o ).
thf(tp_v882,type,
v882: $i > $o ).
thf(tp_v883,type,
v883: $i > $i > $o ).
thf(tp_v888,type,
v888: $i > $o ).
thf(tp_v889,type,
v889: $i > $o ).
thf(tp_v89,type,
v89: $i > $o ).
thf(tp_v890,type,
v890: $i > $o ).
thf(tp_v909,type,
v909: $i > $i > $o ).
thf(tp_v91,type,
v91: $i > $o ).
thf(tp_v914,type,
v914: $i > $o ).
thf(tp_v915,type,
v915: $i > $o ).
thf(tp_v916,type,
v916: $i > $o ).
thf(tp_v918,type,
v918: $i > $o ).
thf(tp_v922,type,
v922: $i > $i > $o ).
thf(tp_v924,type,
v924: $i > $i > $o ).
thf(tp_v93,type,
v93: $i > $o ).
thf(tp_v930,type,
v930: $i > $o ).
thf(tp_v931,type,
v931: $i > $o ).
thf(tp_v934,type,
v934: $i > $o ).
thf(tp_v935,type,
v935: $i > $o ).
thf(tp_v938,type,
v938: $i > $o ).
thf(tp_v939,type,
v939: $i > $o ).
thf(tp_v941,type,
v941: $i > $o ).
thf(tp_v944,type,
v944: $i > $o ).
thf(tp_v946,type,
v946: $i > $o ).
thf(tp_v950,type,
v950: $i > $o ).
thf(tp_v951,type,
v951: $i > $o ).
thf(tp_v952,type,
v952: $i > $o ).
thf(tp_v953,type,
v953: $i > $o ).
thf(tp_v954,type,
v954: $i > $o ).
thf(tp_v955,type,
v955: $i > $o ).
thf(tp_v958,type,
v958: $i > $i > $o ).
thf(tp_v959,type,
v959: $i > $o ).
thf(tp_v960,type,
v960: $i > $i > $o ).
thf(tp_v965,type,
v965: $i > $o ).
thf(tp_v966,type,
v966: $i > $o ).
thf(tp_v981,type,
v981: $i > $o ).
thf(tp_v982,type,
v982: $i > $o ).
thf(tp_v983,type,
v983: $i > $o ).
thf(tp_v987,type,
v987: $i > $i > $o ).
thf(tp_v989,type,
v989: $i > $i > $o ).
thf(2652,conjecture,
$false,
file('no conjecture given, we try to refute the axioms',dummy_conjecture) ).
thf(2653,negated_conjecture,
$false = $false,
inference(negate_conjecture,[status(cth)],[2652]) ).
thf(2654,negated_conjecture,
$false,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u12823) ).
thf(2655,plain,
$false = $false,
inference(unfold_def,[status(thm)],[2653]) ).
thf(2656,plain,
$false = $true,
inference(unfold_def,[status(thm)],[2654]) ).
thf(2657,plain,
( ( ~ $false ) = $true ),
inference(polarity_switch,[status(thm)],[2655]) ).
thf(2658,plain,
$false = $true,
inference(copy,[status(thm)],[2656]) ).
thf(2659,plain,
( ( ~ $false ) = $true ),
inference(copy,[status(thm)],[2657]) ).
thf(2660,plain,
$false = $false,
inference(extcnf_not_pos,[status(thm)],[2659]) ).
thf(2661,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[2658,2660]) ).
thf(2662,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[2661]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV093-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/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.19 % Computer : n015.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Oct 6 11:06:58 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.08/1.24 ..................
% 6.08/1.24
% 6.08/1.24 No.of.Axioms: 1
% 6.08/1.24
% 6.08/1.24 Length.of.Defs: 0
% 6.08/1.24
% 6.08/1.24 Contains.Choice.Funs: false
% 6.08/1.24 ..................
% 6.08/1.24
% 6.08/1.24 ********************************
% 6.08/1.24 * All subproblems solved! *
% 6.08/1.24 ********************************
% 6.08/1.24 % SZS status Unsatisfiable for /export/starexec/sandbox2/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:299,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:2661,loop_count:0,foatp_calls:1,translation:fof_full)
% 6.08/1.24
% 6.08/1.24 %**** Beginning of derivation protocol ****
% 6.08/1.24 % SZS output start CNFRefutation
% See solution above
% 6.08/1.24
% 6.08/1.24 %**** End of derivation protocol ****
% 6.08/1.24 %**** no. of clauses in derivation: 11 ****
% 6.08/1.24 %**** clause counter: 2661 ****
% 6.08/1.24
% 6.08/1.24 % SZS status Unsatisfiable for /export/starexec/sandbox2/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:299,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:2661,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------