%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWW814_1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n003.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 : Fri Sep 25 03:30:24 PM UTC 2026
% Result : Unsatisfiable 2.58s 1.69s
% Output : CNFRefutation 2.58s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f242ERROR: Could not build tree for root c_13607ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
pset_acc_range_left: ( $int * ( c_ssorted * c_ssorted ) ) > c_unique ).
tff(pred_def_1,type,
fresh: ( c_ssorted * c_ssorted ) > $o ).
tff(pred_def_2,type,
gt_pointer: ( c_ssorted * c_ssorted ) > $o ).
tff(pred_def_3,type,
valid_acc_range: ( $int * c_ssorted ) > $o ).
tff(pred_def_4,type,
on_stack: ( c_ssorted * c_ssorted ) > $o ).
tff(pred_def_5,type,
valid_acc: c_ssorted > $o ).
tff(pred_def_6,type,
le_pointer: ( c_ssorted * c_ssorted ) > $o ).
tff(pred_def_7,type,
not_assigns: ( c_ssorted * ( c_ssorted * ( c_ssorted * c_ssorted ) ) ) > $o ).
tff(pred_def_8,type,
valid_range: ( $int * ( $int * ( c_ssorted * c_ssorted ) ) ) > $o ).
tff(pred_def_9,type,
valid_index: ( $int * ( c_ssorted * c_ssorted ) ) > $o ).
tff(pred_def_10,type,
not_in_pset: ( c_ssorted * c_ssorted ) > $o ).
tff(pred_def_11,type,
ge_pointer: ( c_ssorted * c_ssorted ) > $o ).
tff(pred_def_12,type,
free_stack: ( c_ssorted * ( c_ssorted * c_ssorted ) ) > $o ).
tff(pred_def_13,type,
valid: ( c_ssorted * c_ssorted ) > $o ).
tff(pred_def_14,type,
separation1: ( c_ssorted * c_ssorted ) > $o ).
tff(pred_def_15,type,
alloc_extends: ( c_ssorted * c_ssorted ) > $o ).
tff(pred_def_16,type,
separation1_range: ( $int * c_ssorted ) > $o ).
tff(pred_def_17,type,
lt_pointer: ( c_ssorted * c_ssorted ) > $o ).
tff(pred_def_18,type,
on_heap: ( c_ssorted * c_ssorted ) > $o ).
tff(pred_def_19,type,
separation1_range1: ( $int * ( c_ssorted * c_ssorted ) ) > $o ).
tff(pred_def_20,type,
separation2_range1: ( $int * ( c_ssorted * c_ssorted ) ) > $o ).
tff(pred_def_21,type,
separation2: ( c_ssorted * c_ssorted ) > $o ).
tff(func_def_22,type,
pset_range: ( $int * ( $int * c_ssorted ) ) > c_unique ).
tff(func_def_23,type,
ss2Int: c_ssorted > $int ).
tff(func_def_24,type,
pset_union: ( c_ssorted * c_ssorted ) > c_unique ).
tff(func_def_25,type,
le_int_bool: ( $int * $int ) > c_Boolean ).
tff(pred_def_26,type,
sP0: ( $int * ( c_type * ( c_unique * c_type ) ) ) > $o ).
tff(pred_def_27,type,
sP1: ( $int * ( $int * ( $int * ( $int * $int ) ) ) ) > $o ).
tff(pred_def_28,type,
sP2: ( $int * ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_type * ( $int * ( $int * $int ) ) ) ) ) ) ) ) ) > $o ).
tff(func_def_29,type,
pset_range_left: ( $int * c_ssorted ) > c_unique ).
tff(func_def_30,type,
block_length: ( c_ssorted * c_ssorted ) > $int ).
tff(func_def_31,type,
c_sort: ( c_unique * c_type ) > c_ssorted ).
tff(func_def_32,type,
eq_int_bool: ( $int * $int ) > c_Boolean ).
tff(func_def_33,type,
sub_pointer: ( c_ssorted * c_ssorted ) > $int ).
tff(func_def_34,type,
pset_empty: c_unique ).
tff(func_def_35,type,
c_bool: c_type ).
tff(func_def_36,type,
ss2Bool: c_ssorted > c_Boolean ).
tff(func_def_37,type,
type_memory: ( c_type * c_type ) > c_type ).
tff(func_def_38,type,
acc: ( c_ssorted * c_ssorted ) > c_unique ).
tff(func_def_39,type,
c_int: c_type ).
tff(func_def_40,type,
type_global: c_type ).
tff(func_def_41,type,
pset_range_right: ( $int * c_ssorted ) > c_unique ).
tff(func_def_42,type,
pset_acc_all: ( c_ssorted * c_ssorted ) > c_unique ).
tff(func_def_43,type,
pset_star: ( c_ssorted * c_ssorted ) > c_unique ).
tff(func_def_44,type,
ge_int_bool: ( $int * $int ) > c_Boolean ).
tff(func_def_45,type,
offset: c_ssorted > $int ).
tff(func_def_58,type,
sK3: ( c_unique * ( c_unique * c_type ) ) > c_type ).
tff(func_def_59,type,
sK4: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_60,type,
sK5: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_61,type,
sK6: ( c_unique * ( c_unique * c_type ) ) > c_type ).
tff(func_def_62,type,
sK7: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_63,type,
sK8: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_64,type,
sK9: ( c_unique * ( c_unique * c_type ) ) > c_type ).
tff(func_def_65,type,
sK10: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_66,type,
sK11: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_67,type,
sK12: ( c_unique * ( c_unique * c_type ) ) > c_type ).
tff(func_def_68,type,
sK13: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_69,type,
sK14: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_70,type,
sK15: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_71,type,
sK16: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_72,type,
sK17: ( c_unique * ( c_unique * c_type ) ) > $int ).
tff(func_def_73,type,
sK18: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_74,type,
sK19: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_75,type,
sK20: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > $int ).
tff(func_def_76,type,
sK21: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_ssorted ).
tff(func_def_77,type,
sK22: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_ssorted ).
tff(func_def_78,type,
sK23: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > $int ).
tff(func_def_79,type,
sK24: ( $int * ( c_unique * c_type ) ) > c_type ).
tff(func_def_80,type,
sK25: ( $int * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_81,type,
sK26: ( $int * ( $int * ( c_unique * c_type ) ) ) > c_type ).
tff(func_def_82,type,
sK27: ( $int * ( $int * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_83,type,
sK28: ( $int * ( c_unique * c_type ) ) > c_type ).
tff(func_def_84,type,
sK29: ( $int * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_85,type,
sK30: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_86,type,
sK31: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_type ).
tff(func_def_87,type,
sK32: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_88,type,
sK33: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_type ).
tff(func_def_89,type,
sK34: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_90,type,
sK35: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_91,type,
sK36: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_92,type,
sK37: ( c_unique * ( c_unique * c_type ) ) > c_type ).
tff(func_def_93,type,
sK38: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_94,type,
sK39: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_95,type,
sK40: ( c_unique * ( c_unique * c_type ) ) > c_type ).
tff(func_def_96,type,
sK41: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_97,type,
sK42: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_98,type,
sK43: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_type ).
tff(func_def_99,type,
sK44: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_ssorted ).
tff(func_def_100,type,
sK45: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_ssorted ).
tff(func_def_101,type,
sK46: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_type ).
tff(func_def_102,type,
sK47: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_ssorted ).
tff(func_def_103,type,
sK48: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_ssorted ).
tff(func_def_104,type,
sK49: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_type ).
tff(func_def_105,type,
sK50: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_ssorted ).
tff(func_def_106,type,
sK51: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_ssorted ).
tff(func_def_107,type,
sK52: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_108,type,
sK53: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_type ).
tff(func_def_109,type,
sK54: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_110,type,
sK55: ( $int * ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_111,type,
sK56: ( $int * ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) ) > c_type ).
tff(func_def_112,type,
sK57: ( $int * ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_113,type,
sK58: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_ssorted ).
tff(func_def_114,type,
sK59: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_ssorted ).
tff(func_def_115,type,
sK60: ( $int * ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_116,type,
sK61: ( $int * ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_117,type,
sK62: ( c_unique * ( c_unique * c_type ) ) > c_type ).
tff(func_def_118,type,
sK63: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_119,type,
sK64: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_120,type,
sK65: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_type ).
tff(func_def_121,type,
sK66: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_ssorted ).
tff(func_def_122,type,
sK67: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_type ).
tff(func_def_123,type,
sK68: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_124,type,
sK69: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_type ).
tff(func_def_125,type,
sK70: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_126,type,
sK71: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_type ).
tff(func_def_127,type,
sK72: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_unique ).
tff(func_def_128,type,
sK73: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_ssorted ).
tff(func_def_129,type,
sK74: ( c_unique * ( c_unique * c_type ) ) > c_type ).
tff(func_def_130,type,
sK75: ( c_unique * ( c_unique * c_type ) ) > c_type ).
tff(func_def_131,type,
sK76: ( c_unique * c_type ) > c_ssorted ).
tff(func_def_132,type,
sK77: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_133,type,
sK78: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_type ).
tff(func_def_134,type,
sK79: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_135,type,
sK80: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_136,type,
sK81: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_137,type,
sK82: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_type ).
tff(func_def_138,type,
sK83: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_139,type,
sK84: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_140,type,
sK85: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_type ).
tff(func_def_141,type,
sK86: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_142,type,
sK87: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_type ).
tff(func_def_143,type,
sK88: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_unique ).
tff(func_def_144,type,
sK89: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_type ).
tff(func_def_145,type,
sK90: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_146,type,
sK91: ( c_unique * ( c_unique * c_type ) ) > c_type ).
tff(func_def_147,type,
sK92: ( c_unique * ( c_unique * c_type ) ) > c_unique ).
tff(func_def_148,type,
sK93: ( c_unique * ( c_unique * c_type ) ) > c_type ).
tff(func_def_149,type,
sK94: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_type ).
tff(func_def_150,type,
sK95: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_151,type,
sK96: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_type ).
tff(func_def_152,type,
sK97: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_unique ).
tff(func_def_153,type,
sK98: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > $int ).
tff(func_def_154,type,
sK99: ( $int * ( $int * ( c_unique * ( c_unique * c_type ) ) ) ) > c_type ).
tff(func_def_155,type,
sK100: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_type ).
tff(func_def_156,type,
sK101: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_unique ).
tff(func_def_157,type,
sK102: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > $int ).
tff(func_def_158,type,
sK103: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_type ).
tff(func_def_159,type,
sK104: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_type ).
tff(func_def_160,type,
sK105: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_unique ).
tff(func_def_161,type,
sK106: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > $int ).
tff(func_def_162,type,
sK107: ( $int * ( c_unique * ( c_unique * c_type ) ) ) > c_type ).
tff(func_def_163,type,
sK108: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_type ).
tff(func_def_164,type,
sK109: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_unique ).
tff(func_def_165,type,
sK110: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > $int ).
tff(func_def_166,type,
sK111: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_type ).
tff(func_def_167,type,
sK112: ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_type ).
tff(func_def_168,type,
sK113: ( $int * ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_type ).
tff(func_def_169,type,
sK114: ( $int * ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_unique ).
tff(func_def_170,type,
sK115: ( $int * ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > $int ).
tff(func_def_171,type,
sK116: ( $int * ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_type ).
tff(func_def_172,type,
sK117: ( $int * ( c_unique * ( $int * ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) ) ) > c_type ).
tff(func_def_173,type,
sK118: ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_type ).
tff(func_def_174,type,
sK119: ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_unique ).
tff(func_def_175,type,
sK120: ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > $int ).
tff(func_def_176,type,
sK121: ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_type ).
tff(func_def_177,type,
sK122: ( $int * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) ) > c_type ).
tff(func_def_178,type,
sK123: ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_type ).
tff(func_def_179,type,
sK124: ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_unique ).
tff(func_def_180,type,
sK125: ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > $int ).
tff(func_def_181,type,
sK126: ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_type ).
tff(func_def_182,type,
sK127: ( $int * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) ) > c_type ).
tff(func_def_183,type,
sK128: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_ssorted ).
tff(func_def_184,type,
sK129: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_type ).
tff(func_def_185,type,
sK130: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_ssorted ).
tff(func_def_186,type,
sK131: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_ssorted ).
tff(func_def_187,type,
sK132: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_ssorted ).
tff(func_def_188,type,
sK133: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_ssorted ).
tff(func_def_189,type,
sK134: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_ssorted ).
tff(func_def_190,type,
sK135: ( c_unique * ( c_type * c_type ) ) > c_unique ).
tff(func_def_191,type,
sK136: ( c_unique * ( c_type * c_type ) ) > c_unique ).
tff(func_def_192,type,
sK137: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_type ).
tff(func_def_193,type,
sK138: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_ssorted ).
tff(func_def_194,type,
sK139: ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_ssorted ).
tff(func_def_195,type,
sK140: ( $int * ( c_unique * ( c_type * c_type ) ) ) > c_unique ).
tff(func_def_196,type,
sK141: ( $int * ( c_unique * ( c_type * c_type ) ) ) > c_unique ).
tff(func_def_197,type,
sK142: ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_type ).
tff(func_def_198,type,
sK143: ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_199,type,
sK144: ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_200,type,
sK145: ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_type ).
tff(func_def_201,type,
sK146: ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_202,type,
sK147: ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_203,type,
sK148: ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_204,type,
sK149: ( c_unique * ( c_unique * ( c_type * c_type ) ) ) > c_type ).
tff(func_def_205,type,
sK150: ( c_unique * ( c_unique * ( c_type * c_type ) ) ) > c_unique ).
tff(func_def_206,type,
sK151: ( c_unique * ( c_unique * ( c_type * c_type ) ) ) > c_unique ).
tff(func_def_207,type,
sK152: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_type ).
tff(func_def_208,type,
sK153: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_209,type,
sK154: ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_type ).
tff(func_def_210,type,
sK155: ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_unique ).
tff(func_def_211,type,
sK156: ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_unique ).
tff(func_def_212,type,
sK157: ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > $int ).
tff(func_def_213,type,
sK158: ( $int * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_type ).
tff(func_def_214,type,
sK159: ( $int * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_type ).
tff(func_def_215,type,
sK160: ( $int * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) > c_ssorted ).
tff(func_def_216,type,
sK161: ( $int * ( c_type * ( c_unique * c_type ) ) ) > c_unique ).
tff(func_def_217,type,
sK162: ( $int * ( c_type * ( c_unique * c_type ) ) ) > c_unique ).
tff(func_def_218,type,
sK163: ( $int * ( c_type * ( c_unique * c_type ) ) ) > $int ).
tff(func_def_219,type,
sK164: ( $int * ( c_type * ( c_unique * c_type ) ) ) > $int ).
tff(func_def_220,type,
sK165: ( $int * ( $int * ( c_unique * ( $int * ( c_type * ( c_unique * c_type ) ) ) ) ) ) > c_type ).
tff(func_def_221,type,
sK166: ( $int * ( $int * ( c_unique * ( $int * ( c_type * ( c_unique * c_type ) ) ) ) ) ) > c_ssorted ).
tff(func_def_222,type,
sK167: ( $int * ( $int * ( c_unique * ( $int * ( c_type * ( c_unique * c_type ) ) ) ) ) ) > c_type ).
tff(func_def_223,type,
sK168: ( $int * ( $int * ( c_unique * ( $int * ( c_type * ( c_unique * c_type ) ) ) ) ) ) > c_ssorted ).
tff(func_def_224,type,
sK169: ( c_unique * ( c_unique * ( c_type * c_type ) ) ) > c_type ).
tff(func_def_225,type,
sK170: ( c_unique * ( c_unique * ( c_type * c_type ) ) ) > c_unique ).
tff(func_def_226,type,
sK171: ( c_unique * ( c_unique * ( c_type * c_type ) ) ) > c_unique ).
tff(func_def_227,type,
sK172: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_type ).
tff(func_def_228,type,
sK173: ( c_unique * ( c_unique * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) > c_type ).
tff(func_def_229,type,
sK174: ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_type ).
tff(func_def_230,type,
sK175: ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_unique ).
tff(func_def_231,type,
sK176: ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > c_unique ).
tff(func_def_232,type,
sK177: ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) > $int ).
tff(func_def_233,type,
sK178: ( $int * ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) ) > c_type ).
tff(func_def_234,type,
sK179: ( $int * ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_type * c_type ) ) ) ) ) ) ) > c_type ).
tff(func_def_235,type,
sK180: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_236,type,
sK181: ( c_unique * ( c_unique * c_type ) ) > c_ssorted ).
tff(func_def_237,type,
sK182: ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) > c_ssorted ).
tff(func_def_238,type,
sK183: ( $int * ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) ) > c_ssorted ).
tff(func_def_239,type,
sK184: ( $int * ( $int * ( c_unique * ( c_unique * ( c_unique * c_type ) ) ) ) ) > c_ssorted ).
tff(func_def_240,type,
sK185: c_unique > c_ssorted ).
tff(func_def_241,type,
sK186: ( c_unique * ( c_unique * c_unique ) ) > c_ssorted ).
tff(func_def_242,type,
sK187: ( c_unique * ( c_unique * c_unique ) ) > c_ssorted ).
tff(func_def_243,type,
sK188: ( c_unique * ( c_unique * c_unique ) ) > c_ssorted ).
tff(func_def_244,type,
sK189: $int > $int ).
tff(func_def_245,type,
sK190: ( $int * ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_type * ( $int * ( $int * $int ) ) ) ) ) ) ) ) ) > $int ).
tff(func_def_246,type,
sK191: ( $int * ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_type * ( $int * ( $int * $int ) ) ) ) ) ) ) ) ) > c_unique ).
tff(func_def_247,type,
sK192: ( $int * ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_type * ( $int * ( $int * $int ) ) ) ) ) ) ) ) ) > $int ).
tff(func_def_248,type,
sK193: ( $int * ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_type * ( $int * ( $int * $int ) ) ) ) ) ) ) ) ) > $int ).
tff(func_def_249,type,
sK194: ( $int * ( c_unique * ( c_unique * ( $int * ( c_unique * ( c_unique * ( c_type * ( $int * ( $int * $int ) ) ) ) ) ) ) ) ) > c_unique ).
tff(func_def_250,type,
sK195: ( $int * ( $int * ( $int * ( $int * $int ) ) ) ) > $int ).
tff(func_def_251,type,
sK196: ( $int * ( $int * ( $int * ( $int * $int ) ) ) ) > $int ).
tff(func_def_252,type,
sK197: ( $int * ( $int * ( $int * ( $int * $int ) ) ) ) > $int ).
tff(func_def_253,type,
sK198: ( $int * ( $int * $int ) ) > $int ).
tff(func_def_254,type,
sK199: ( $int * $int ) > $int ).
tff(func_def_255,type,
sK200: $int ).
tff(func_def_256,type,
sK201: c_unique ).
tff(func_def_257,type,
sK202: $int ).
tff(func_def_258,type,
sK203: $int ).
tff(func_def_259,type,
sK204: c_unique ).
tff(func_def_260,type,
sK205: $int ).
tff(func_def_261,type,
sK206: c_unique ).
tff(func_def_262,type,
sK207: $int ).
tff(func_def_263,type,
sK208: $int ).
tff(func_def_264,type,
sK209: $int ).
tff(func_def_265,type,
sK210: $int ).
tff(func_def_266,type,
sK211: $int ).
tff(func_def_267,type,
sK212: $int ).
tff(func_def_268,type,
sK213: $int ).
tff(func_def_269,type,
sK214: c_unique ).
tff(func_def_270,type,
sK215: c_unique ).
tff(func_def_271,type,
sK216: c_type > c_unique ).
tff(func_def_272,type,
sK217: $int > c_type ).
tff(f357,plain,
? [X0: $int,X1: c_unique,X2: $int,X3: $int,X4: c_unique] :
( valid_range(c_sort(type_alloc_table,X1),c_sort(type_pointer(type_global),X4),0,2800)
& ( X0 = 10000 )
& ( X3 = 2800 )
& ( X2 = 0 )
& ? [X5: $int,X6: c_unique] :
( ! [X18: $int] :
? [X19: c_type] :
( ( ~ $less(X18,X5)
| $less(X18,0)
| ( 2000 = ss2Int(c_sort(c_int,acc(c_sort(type_memory(c_int,type_global),X6),c_sort(X19,shift(c_sort(X19,X4),X18))))) ) )
& ( type_pointer(type_global) = X19 ) )
& ~ $less(2800,X5)
& ~ $less(X5,0)
& ( 0 = $sum(X5,$uminus(X3)) )
& ? [X7: $int] :
( ( 0 = '%'(X7,14) )
& ~ $less(2800,X7)
& ~ $less(X7,0)
& ? [X8: $int] :
( ( 0 = X8 )
& ? [X9: $int] :
( ( $product(X7,2) = X9 )
& ( 0 != X9 )
& ? [X10: $int] :
( ( X7 = X10 )
& ? [X11: $int,X12: $int,X13: $int,X14: c_unique] :
( ( $product(X11,2) = X13 )
& ~ $less(X7,X11)
& ~ $less(X11,1)
& ( 1 != 0 )
& ? [X15: c_unique] :
! [X16: c_type] :
( ( ( shift(c_sort(X16,X4),X11) = X15 )
& valid(c_sort(type_alloc_table,X1),c_sort(X16,X15))
& ? [X17: c_unique] :
( ( acc(c_sort(type_memory(c_int,type_global),X14),c_sort(X16,X15)) = X17 )
& sP2(X11,X7,X0,X16,X14,X1,X13,X4,X17,X12) ) )
| ( type_pointer(type_global) != X16 ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f242]) ).
tff(f358,plain,
( valid_range(c_sort(type_alloc_table,sK201),c_sort(type_pointer(type_global),sK204),0,2800)
& ( 10000 = sK200 )
& ( 2800 = sK203 )
& ( 0 = sK202 )
& ! [X18: $int] :
( ( ~ $less(X18,sK205)
| $less(X18,0)
| ( 2000 = ss2Int(c_sort(c_int,acc(c_sort(type_memory(c_int,type_global),sK206),c_sort(sK217(X18),shift(c_sort(sK217(X18),sK204),X18))))) ) )
& ( type_pointer(type_global) = sK217(X18) ) )
& ~ $less(2800,sK205)
& ~ $less(sK205,0)
& ( 0 = $sum(sK205,$uminus(sK203)) )
& ( 0 = '%'(sK207,14) )
& ~ $less(2800,sK207)
& ~ $less(sK207,0)
& ( 0 = sK208 )
& ( sK209 = $product(sK207,2) )
& ( 0 != sK209 )
& ( sK207 = sK210 )
& ( sK213 = $product(sK211,2) )
& ~ $less(sK207,sK211)
& ~ $less(sK211,1)
& ( 1 != 0 )
& ! [X16: c_type] :
( ( ( sK215 = shift(c_sort(X16,sK204),sK211) )
& valid(c_sort(type_alloc_table,sK201),c_sort(X16,sK215))
& ( sK216(X16) = acc(c_sort(type_memory(c_int,type_global),sK214),c_sort(X16,sK215)) )
& sP2(sK211,sK207,sK200,X16,sK214,sK201,sK213,sK204,sK216(X16),sK212) )
| ( type_pointer(type_global) != X16 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK200,sK201,sK202,sK203,sK204,sK205,sK206,sK207,sK208,sK209,sK210,sK211,sK212,sK213,sK214,sK215,sK216,sK217]),skolemize(X0,sK200),skolemize(X1,sK201),skolemize(X2,sK202),skolemize(X3,sK203),skolemize(X4,sK204),skolemize(X5,sK205),skolemize(X6,sK206),skolemize(X7,sK207),skolemize(X8,sK208),skolemize(X9,sK209),skolemize(X10,sK210),skolemize(X11,sK211),skolemize(X12,sK212),skolemize(X13,sK213),skolemize(X14,sK214),skolemize(X15,sK215),skolemize(X17,sK216(X16)),skolemize(X19,sK217(X18))],[f357]) ).
tff(f694,plain,
~ $less(2800,sK205),
inference(cnf_transformation,[],[f358]) ).
tff(f695,plain,
~ $less(sK205,0),
inference(cnf_transformation,[],[f358]) ).
tff(f698,plain,
~ $less(2800,sK207),
inference(cnf_transformation,[],[f358]) ).
tff(f699,plain,
~ $less(sK207,0),
inference(cnf_transformation,[],[f358]) ).
tff(f703,plain,
sK207 = sK210,
inference(cnf_transformation,[],[f358]) ).
tff(f705,plain,
~ $less(sK207,sK211),
inference(cnf_transformation,[],[f358]) ).
tff(f706,plain,
~ $less(sK211,1),
inference(cnf_transformation,[],[f358]) ).
tff(f876,plain,
~ $less(sK210,sK211),
inference(definition_unfolding,[],[f705,f703]) ).
tff(f878,plain,
~ $less(sK210,0),
inference(definition_unfolding,[],[f699,f703]) ).
tff(f879,plain,
~ $less(2800,sK210),
inference(definition_unfolding,[],[f698,f703]) ).
tcf(c_61,negated_conjecture,
! [X0_int: $int] : ~ $less(X0_int,X0_int),
inference(cnf_transformation,[],[f140]) ).
tcf(c_277,negated_conjecture,
~ $less(sK211,1),
inference(cnf_transformation,[],[f706]) ).
tcf(c_278,negated_conjecture,
~ $less(sK210,sK211),
inference(cnf_transformation,[],[f876]) ).
tcf(c_282,negated_conjecture,
~ $less(sK210,0),
inference(cnf_transformation,[],[f878]) ).
tcf(c_283,negated_conjecture,
~ $less(2800,sK210),
inference(cnf_transformation,[],[f879]) ).
tcf(c_286,negated_conjecture,
~ $less(sK205,0),
inference(cnf_transformation,[],[f695]) ).
tcf(c_287,negated_conjecture,
~ $less(2800,sK205),
inference(cnf_transformation,[],[f694]) ).
tcf(c_290,plain,
$less(0,1),
theory(arith) ).
tcf(c_291,plain,
$less(1,2),
theory(arith) ).
tcf(c_292,plain,
$less(2,5),
theory(arith) ).
tcf(c_293,plain,
$less(5,14),
theory(arith) ).
tcf(c_294,plain,
$less(14,2000),
theory(arith) ).
tcf(c_295,plain,
$less(2000,2800),
theory(arith) ).
tcf(c_296,plain,
$less(2800,10000),
theory(arith) ).
tcf(c_13607,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_296,c_295,c_294,c_293,c_292,c_291,c_290,c_287,c_286,c_283,c_282,c_278,c_277,c_61]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW814_1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.35 % Computer : n003.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.03/0.35 % CPULimit : 300
% 0.03/0.35 % WCLimit : 300
% 0.03/0.35 % DateTime : Thu Sep 24 22:57:23 UTC 2026
% 0.03/0.36 % CPUTime :
% 0.03/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.03/0.39 Running TFA theorem proving
% 0.03/0.39 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s tfa_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.40
% 0.03/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.03/0.40
% 0.03/0.40 % Detected problem language: tptp
% 0.03/0.41 % Proving...
% 2.58/1.69 % SZS status Started for theBenchmark.p
% 2.58/1.69 ERROR - "ProverProcess:heur/schedule_none:304.9999792575836" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 2.58/1.69 Fatal error: exception Failure("undefined enum value")
% 2.58/1.69 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --schedule none --sub_typing false --suppress_sat_res true --tptp_safe_out true --stats_out none --out_options none --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 101.67 --show_fool true" --time_out_real 305.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_38ynykwh/ut70_qve 2>> /export/starexec/sandbox2/tmp/iprover_out_38ynykwh/ut70_qve_error
% 2.58/1.69 ERROR - "ProverProcess:heur/vip_65520:11.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 2.58/1.69 Fatal error: exception Failure("undefined enum value")
% 2.58/1.69 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --comb_mode time_based --comb_res_mult 6 --comb_sup_deep_mult 0 --comb_sup_mult 6 --conj_cone_tolerance 1.8969679945890683 --demod_completeness_check fullold --demod_use_ground false --extra_neg_conj all_neg --instantiation_flag false --out_options none --preprocessed_out false --preprocessing_flag false --prolific_symb_bound 1024 --proof_out true --prop_solver_per_cl 512 --res_to_smt_solver false --resolution_flag true --schedule none --share_sel_clauses true --stats_out none --subs_bck_mult 16 --sup_bw_gjoin_interval 100 --sup_cache_sim none --sup_full_bw "[Subsumption;SubsumptionRes;UnitSubsAndRes]" --sup_full_fixpoint false --sup_full_fw "[]" --sup_fun_splitting false --sup_immed_bw_immed "[Subsumption;SubsumptionRes;UnitSubsAndRes]" --sup_immed_bw_main "[SubsumptionRes;UnitSubsAndRes;FullSubsAndRes;Demod;ACDemod]" --sup_immed_fixpoint false --sup_immed_fw_immed "[Subsumption;SubsumptionRes;FullSubsAndRes;Demod;LightNorm;ACDemod]" --sup_immed_fw_main "[Subsumption;UnitSubsAndRes;FullSubsAndRes;Demod;LightNorm;ACNormalisation;GroundJoinability;Connectedness]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_fixpoint false --sup_main_fixpoint true --sup_ordering lpo --sup_passive_queue_type priority_queues --sup_passive_queues "[[+has_eq;-has_eq];[-num_var;-num_var];[+conj_dist;+ground;-max_atom_input_occur]]" --sup_passive_queues_freq "[1;4;4]" --sup_prop_simpl_given false --sup_prop_simpl_new false --sup_score sim_d_gen --sup_share_max_num_cl 10 --sup_share_score_frac 0.2 --sup_smt_interval 32 --sup_symb_ordering invfreq_arity --sup_term_weight default --sup_to_prop_solver passive --sup_unprocessed_bound 10 --superposition_flag true --suppress_sat_res true --tptp_safe_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 3.67 --show_fool true" --time_out_real 11.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_38ynykwh/gayx8kq8 2>> /export/starexec/sandbox2/tmp/iprover_out_38ynykwh/gayx8kq8_error
% 2.58/1.69 ERROR - "ProverProcess:heur/vip_65097:3.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 2.58/1.69 Fatal error: exception Failure("undefined enum value")
% 2.58/1.69 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 3 --comb_sup_deep_mult 0 --comb_sup_mult 0 --conj_cone_tolerance 4.0357851670394345 --extra_neg_conj none --inst_activity_threshold 512 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp true --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 2048 --inst_lit_activity_flag true --inst_lit_sel "[+split;-sign;-depth]" --inst_lit_sel_side none --inst_orphan_elimination true --inst_passive_queue_type queue --inst_passive_queues "[[+age;+num_lits;-age];[-age;-min_def_symb;+bc_imp_inh]]" --inst_passive_queues_freq "[2;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given true --inst_sel_renew solver --inst_solver_calls_frac 1.0 --inst_solver_per_active 1024 --inst_sos_flag true --inst_sos_phase false --inst_sos_sth_lit_sel "[+split;-ground;-depth]" --inst_start_prop_sim_after_learn 3 --inst_subs_given true --inst_subs_new false --instantiation_flag true --out_options none --prep_sup_sim_all true --prep_sup_sim_sup false --preprocessed_out false --preprocessing_flag true --prolific_symb_bound 256 --proof_out true --prop_solver_per_cl 16384 --resolution_flag true --schedule none --share_sel_clauses false --stats_out none --subs_bck_mult 8 --suppress_sat_res true --tptp_safe_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 1.00 --show_fool true" --time_out_real 3.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_38ynykwh/su9emh_l 2>> /export/starexec/sandbox2/tmp/iprover_out_38ynykwh/su9emh_l_error
% 2.58/1.69 ERROR - "ProverProcess:heur/vip_65080:40.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 2.58/1.69 Fatal error: exception Failure("undefined enum value")
% 2.58/1.69 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --comb_mode time_based --comb_res_mult 6 --comb_sup_deep_mult 4 --comb_sup_mult 6 --conj_cone_tolerance 1.895766803319499 --demod_completeness_check fullold --demod_use_ground false --extra_neg_conj all_pos_neg --instantiation_flag false --out_options none --preprocessed_out false --preprocessing_flag false --prolific_symb_bound 1024 --proof_out true --prop_solver_per_cl 128 --res_to_smt_solver false --resolution_flag true --schedule none --share_sel_clauses true --stats_out none --subs_bck_mult 16 --sup_bw_gjoin_interval 100 --sup_cache_sim none --sup_full_bw "[Subsumption;SubsumptionRes;UnitSubsAndRes]" --sup_full_fixpoint false --sup_full_fw "[]" --sup_fun_splitting false --sup_immed_bw_immed "[Subsumption;SubsumptionRes;UnitSubsAndRes]" --sup_immed_bw_main "[SubsumptionRes;UnitSubsAndRes;FullSubsAndRes;Demod;ACDemod]" --sup_immed_fixpoint false --sup_immed_fw_immed "[Subsumption;SubsumptionRes;FullSubsAndRes;Demod;LightNorm;ACDemod]" --sup_immed_fw_main "[Subsumption;UnitSubsAndRes;FullSubsAndRes;Demod;LightNorm;ACNormalisation;GroundJoinability;Connectedness]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_fixpoint false --sup_iter_deepening 2 --sup_main_fixpoint true --sup_ordering lpo --sup_passive_queue_type priority_queues --sup_passive_queues "[[+has_eq;-has_eq];[-num_var;-num_var];[+conj_dist;+ground;-max_atom_input_occur]]" --sup_passive_queues_freq "[1;4;4]" --sup_prop_simpl_given false --sup_prop_simpl_new false --sup_restarts_mult 4 --sup_score sim_d_gen --sup_share_max_num_cl 10 --sup_share_score_frac 0.2 --sup_smt_interval 32 --sup_symb_ordering invfreq_arity --sup_term_weight default --sup_to_prop_solver passive --sup_unprocessed_bound 10 --superposition_flag true --suppress_sat_res true --tptp_safe_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 13.33 --show_fool true" --time_out_real 40.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_38ynykwh/myt24q31 2>> /export/starexec/sandbox2/tmp/iprover_out_38ynykwh/myt24q31_error
% 2.58/1.69 ERROR - "ProverProcess:heur/vip_66020:200.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 2.58/1.69 Fatal error: exception Failure("undefined enum value")
% 2.58/1.69 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --comb_inst_mult 16 --comb_mode time_based --comb_res_mult 3 --comb_sup_deep_mult 1 --comb_sup_mult 0 --conj_cone_tolerance 2.250068292082666 --demod_completeness_check fastold --demod_use_ground true --extra_neg_conj none --inst_activity_threshold 16 --inst_dismatching false --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 3 --inst_learning_loop_flag true --inst_learning_start 32 --inst_lit_activity_flag false --inst_lit_sel "[+ground;+num_var]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type queue --inst_passive_queues "[[-num_lits;-has_eq]]" --inst_passive_queues_freq "[512]" --inst_prop_sim_given false --inst_prop_sim_new false --inst_restr_to_given true --inst_sel_renew solver --inst_solver_calls_frac 0.13028534399813618 --inst_solver_per_active 4096 --inst_sos_flag true --inst_sos_phase true --inst_sos_sth_lit_sel "[+non_prol_conj_symb;-depth;-non_prol_conj_symb;+non_prol_conj_symb;+eq]" --inst_start_prop_sim_after_learn 7 --inst_subs_given false --inst_subs_new true --inst_to_smt_solver false --instantiation_flag true --out_options none --preprocessed_out false --preprocessing_flag false --prolific_symb_bound 128 --proof_out true --prop_solver_per_cl 512 --res_to_smt_solver true --resolution_flag true --schedule none --share_sel_clauses true --stats_out none --subs_bck_mult 8 --sup_bw_gjoin_interval 10000 --sup_cache_sim none --sup_full_bw "[]" --sup_full_fixpoint true --sup_full_fw "[Subsumption;SubsumptionRes;FullSubsAndRes;ACJoinability;Connectedness]" --sup_fun_splitting false --sup_immed_bw_immed "[SubsumptionRes;UnitSubsAndRes;FullSubsAndRes;Demod;ACDemod]" --sup_immed_bw_main "[SubsumptionRes;UnitSubsAndRes;Demod]" --sup_immed_fixpoint false --sup_immed_fw_immed "[SubsumptionRes;UnitSubsAndRes;Demod;ACDemod;GroundJoinability;Connectedness]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_fixpoint true --sup_iter_deepening 2 --sup_main_fixpoint true --sup_ordering kbo --sup_passive_queue_type queue --sup_passive_queues "[[-min_def_symb;+reachable_state;-age];[-epr];[+horn;-reachable_state;-num_var]]" --sup_passive_queues_freq "[2;5;15]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 12 --sup_score sim --sup_share_max_num_cl 80 --sup_share_score_frac 0.1 --sup_smt_interval 16384 --sup_symb_ordering random --sup_term_weight default --sup_to_prop_solver none --sup_unprocessed_bound 1000 --superposition_flag true --suppress_sat_res true --tptp_safe_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 66.67 --show_fool true" --time_out_real 200.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_38ynykwh/ekz0bo6f 2>> /export/starexec/sandbox2/tmp/iprover_out_38ynykwh/ekz0bo6f_error
% 2.58/1.69 ERROR - "ProverProcess:heur/vip_65511:44.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 2.58/1.69 Fatal error: exception Failure("undefined enum value")
% 2.58/1.69 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --comb_inst_mult 2 --comb_mode clause_based --comb_sup_deep_mult 3 --comb_sup_mult 0 --conj_cone_tolerance 3.378762210374529 --demod_completeness_check full --demod_use_ground false --extra_neg_conj all_pos --inst_activity_threshold 4 --inst_dismatching false --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 6 --inst_learning_loop_flag true --inst_learning_start 8192 --inst_lit_activity_flag true --inst_lit_sel "[-conj_symb;-conj_symb;+conj_symb;+num_var;-non_prol_conj_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type queue --inst_passive_queues "[[-has_eq;-conj_dist];[+ground;-min_def_symb]]" --inst_passive_queues_freq "[5;3]" --inst_prop_sim_given true --inst_prop_sim_new true --inst_restr_to_given false --inst_sel_renew model --inst_solver_calls_frac 0.60162165485836 --inst_solver_per_active 1024 --inst_sos_flag true --inst_sos_phase true --inst_sos_sth_lit_sel "[-conj_symb;-num_symb;+num_var;-eq;+num_var]" --inst_start_prop_sim_after_learn 9 --inst_subs_given false --inst_subs_new true --inst_to_smt_solver false --instantiation_flag true --out_options none --preprocessed_out false --preprocessing_flag false --prolific_symb_bound 16384 --proof_out true --prop_solver_per_cl 128 --resolution_flag false --schedule none --share_sel_clauses false --stats_out none --subs_bck_mult 4 --sup_bw_gjoin_interval 1000 --sup_cache_sim none --sup_full_bw "[]" --sup_full_fixpoint false --sup_full_fw "[]" --sup_fun_splitting true --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fixpoint false --sup_immed_fw_immed "[Subsumption;SubsumptionRes;UnitSubsAndRes;Demod;ACJoinability;Connectedness]" --sup_immed_fw_main "[]" --sup_immed_triv "[PropSubs]" --sup_indices_passive "[UnitSubsumption;NonunitSubsumption;Subsumption;FwDemod;BwDemod;LightNorm;FwACDemod;BwACDemod;SMTIncr;SMTSet;BwGjoin]" --sup_input_fixpoint true --sup_iter_deepening 8 --sup_main_fixpoint true --sup_ordering lpo --sup_passive_queue_type queue --sup_passive_queues "[[+next_state;-horn;-epr];[+max_atom_input_occur];[-num_lits;-num_lits]]" --sup_passive_queues_freq "[2;1;5]" --sup_prop_simpl_given true --sup_prop_simpl_new false --sup_restarts_mult 16 --sup_smt_interval 8192 --sup_symb_ordering invfreq_arity --sup_term_weight default --sup_to_prop_solver none --sup_unprocessed_bound 10000 --superposition_flag true --suppress_sat_res true --tptp_safe_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 14.67 --show_fool true" --time_out_real 44.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_38ynykwh/ynswnja9 2>> /export/starexec/sandbox2/tmp/iprover_out_38ynykwh/ynswnja9_error
% 2.58/1.69 % SZS status Unsatisfiable for theBenchmark.p
% 2.58/1.69
% 2.58/1.69 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.58/1.69
% 2.58/1.69 % ------ iProver source info
% 2.58/1.69
% 2.58/1.69 % git: date: 2026-07-19 20:42:38 +0200
% 2.58/1.69 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.58/1.69 % git: non_committed_changes: false
% 2.58/1.69
% 2.58/1.69 % ------ Parsing...
% 2.58/1.69 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.58/1.69
% 2.58/1.69 % ------ Preprocessing... sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sf_s rm: 3 0s sf_e pe_s pe_e %
% 2.58/1.69
% 2.58/1.69 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.58/1.69
% 2.58/1.69 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 2.58/1.69 % ------ Proving...
% 2.58/1.69 % ------ Problem Properties
% 2.58/1.69
% 2.58/1.69 %
% 2.58/1.69 % clauses 243
% 2.58/1.69 % conjectures 23
% 2.58/1.69 % EPR 21
% 2.58/1.69 % Horn 189
% 2.58/1.69 % unary 73
% 2.58/1.69 % binary 118
% 2.58/1.69 % lits 482
% 2.58/1.69 % lits eq 173
% 2.58/1.69 % fd_pure 1
% 2.58/1.69 % fd_pseudo 0
% 2.58/1.69 % fd_cond 0
% 2.58/1.69 % fd_pseudo_cond 16
% 2.58/1.69 % AC symbols 2
% 2.58/1.69
% 2.58/1.69 % ------ Input Options Time Limit: Unbounded
% 2.58/1.69
% 2.58/1.69
% 2.58/1.69 % ------
% 2.58/1.69 % Current options:
% 2.58/1.69 % ------
% 2.58/1.69
% 2.58/1.69
% 2.58/1.69 %
% 2.58/1.69
% 2.58/1.69 % ------ Proving...
% 2.58/1.69 %
% 2.58/1.69
% 2.58/1.69 % SZS status Unsatisfiable for theBenchmark.p
% 2.58/1.69
% 2.58/1.69 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.58/1.69
% 2.58/1.69
%------------------------------------------------------------------------------