%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC522_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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 : Tue Sep 29 01:06:11 PM UTC 2026
% Result : Theorem 0.23s 0.36s
% Output : Refutation 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC522_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 % Computer : n005.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.23 % CPULimit : 300
% 0.09/0.23 % WCLimit : 300
% 0.09/0.23 % DateTime : Mon Sep 28 09:41:32 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.26 Running first-order model finding
% 0.09/0.26 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.23/0.36 % (672992)Will run a generic schedule for satisfiability detection.
% 0.23/0.36 % (672998)% WARNING: option uhcvi not known.
% 0.23/0.36 % (672998)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1929997440:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.23/0.36 % (672997)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1235209548_2999 on theBenchmark for (2999ds/0Mi)
% 0.23/0.36 % (672999)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3027898295:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.23/0.36 % (673001)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1487067854:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.23/0.36 % (673000)dis+10_1_sil=32000:sp=arity:random_seed=2007913101:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.23/0.36 % (673002)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1001877971:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.23/0.36 % (673003)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2591012463:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.23/0.36 % (672997)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.23/0.36 % (672997)Terminated due to inappropriate strategy.
% 0.23/0.36 % (672997)------------------------------
% 0.23/0.36 % (672997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.36 % (672997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.36 % (672997)CaDiCaL version: 2.1.3
% 0.23/0.36 % (672997)Termination reason: Inappropriate
% 0.23/0.36 % (672997)Time elapsed: 0.020 s
% 0.23/0.36 % (672997)Peak memory usage: 12 MB
% 0.23/0.36 % (672997)Instructions burned: 42 (million)
% 0.23/0.36 % (672997)------------------------------
% 0.23/0.36 % (672997)------------------------------
% 0.23/0.36 % (673012)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3564716232:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.23/0.36 % (672998) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-672992-672998"...
% 0.23/0.36 % (673001) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-672992-673001"...
% 0.23/0.36 % (672998)...printing done.
% 0.23/0.36 % (672998)Refutation found. Thanks to Tanya!
% 0.23/0.36 % SZS status Theorem for theBenchmark
% 0.23/0.36 % SZS output start Proof for theBenchmark
% 0.23/0.36 tff(type_def_5, type, set_0: $tType).
% 0.23/0.36 tff(type_def_6, type, set_2: $tType).
% 0.23/0.36 tff(type_def_7, type, set_3: $tType).
% 0.23/0.36 tff(type_def_8, type, set_4: $tType).
% 0.23/0.36 tff(func_def_0, type, min_int: $int).
% 0.23/0.36 tff(func_def_1, type, max_int: $int).
% 0.23/0.36 tff(func_def_5, type, divB: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_8, type, g_s0_0: set_0).
% 0.23/0.36 tff(func_def_9, type, g_s1_1: $int).
% 0.23/0.36 tff(func_def_10, type, g_s2_2: $int).
% 0.23/0.36 tff(func_def_11, type, g_s3_3: set_0).
% 0.23/0.36 tff(func_def_12, type, g_s4_4: $int).
% 0.23/0.36 tff(func_def_13, type, g_s5_5: $int).
% 0.23/0.36 tff(func_def_14, type, g_s6_6: set_0).
% 0.23/0.36 tff(func_def_15, type, g_s7_7: $int).
% 0.23/0.36 tff(func_def_16, type, g_s8_8: $int).
% 0.23/0.36 tff(func_def_17, type, g_s9_9: set_0).
% 0.23/0.36 tff(func_def_18, type, g_s10_10: $int).
% 0.23/0.36 tff(func_def_19, type, g_s11_11: $int).
% 0.23/0.36 tff(func_def_20, type, g_s12_12: $int).
% 0.23/0.36 tff(func_def_21, type, g_s13_13: $int).
% 0.23/0.36 tff(func_def_22, type, g_s14_14: $int).
% 0.23/0.36 tff(func_def_23, type, g_s15_15: $int).
% 0.23/0.36 tff(func_def_24, type, g_s16_16: $int).
% 0.23/0.36 tff(func_def_25, type, g_s17_17: $int).
% 0.23/0.36 tff(func_def_26, type, g_s18_18: $int).
% 0.23/0.36 tff(func_def_27, type, g_s19_19: set_0).
% 0.23/0.36 tff(func_def_28, type, g_s20_20: $int).
% 0.23/0.36 tff(func_def_29, type, g_s21_21: $int).
% 0.23/0.36 tff(func_def_30, type, g_s22_22: set_0).
% 0.23/0.36 tff(func_def_31, type, g_s23_23: $int).
% 0.23/0.36 tff(func_def_32, type, g_s24_24: $int).
% 0.23/0.36 tff(func_def_33, type, g_s25_25: $int).
% 0.23/0.36 tff(func_def_34, type, g_s26_26: $int).
% 0.23/0.36 tff(func_def_35, type, g_s27_27: $int).
% 0.23/0.36 tff(func_def_36, type, g_s28_28: $int).
% 0.23/0.36 tff(func_def_37, type, g_s29_29: $int).
% 0.23/0.36 tff(func_def_38, type, g_s30_30: $int).
% 0.23/0.36 tff(func_def_39, type, g_s31_31: $int).
% 0.23/0.36 tff(func_def_40, type, g_s33_32: set_0).
% 0.23/0.36 tff(func_def_41, type, g_s32_33: $int).
% 0.23/0.36 tff(func_def_42, type, g_s35_34: set_0).
% 0.23/0.36 tff(func_def_43, type, g_s34_35: $int).
% 0.23/0.36 tff(func_def_44, type, g_s37_36: set_0).
% 0.23/0.36 tff(func_def_45, type, g_s36_37: $int).
% 0.23/0.36 tff(func_def_46, type, g_s38_38: $int).
% 0.23/0.36 tff(func_def_47, type, g_s39_39: $int).
% 0.23/0.36 tff(func_def_48, type, g_s40_40: set_0).
% 0.23/0.36 tff(func_def_49, type, set_2_empty: set_2).
% 0.23/0.36 tff(func_def_50, type, set_2_insert: set_2 > set_2).
% 0.23/0.36 tff(func_def_51, type, g_s41_41: set_2).
% 0.23/0.36 tff(func_def_52, type, set_3_empty: set_3).
% 0.23/0.36 tff(func_def_53, type, set_3_insert: set_3 > set_3).
% 0.23/0.36 tff(func_def_54, type, g_s42_42: set_3).
% 0.23/0.36 tff(func_def_55, type, set_4_empty: set_4).
% 0.23/0.36 tff(func_def_56, type, set_4_insert: set_4 > set_4).
% 0.23/0.36 tff(func_def_57, type, g_s43_43: set_4).
% 0.23/0.36 tff(func_def_58, type, g_s44_44: set_4).
% 0.23/0.36 tff(func_def_59, type, g_s45_45: set_3).
% 0.23/0.36 tff(func_def_60, type, g_s46_46: set_4).
% 0.23/0.36 tff(func_def_61, type, g_s47_47: set_4).
% 0.23/0.36 tff(func_def_62, type, g_s48_48: set_3).
% 0.23/0.36 tff(func_def_63, type, g_s49_49: set_4).
% 0.23/0.36 tff(func_def_64, type, g_s50_50: set_4).
% 0.23/0.36 tff(func_def_65, type, g_s51_51: set_4).
% 0.23/0.36 tff(func_def_66, type, g_s52_52: set_4).
% 0.23/0.36 tff(func_def_67, type, g_s53_53: set_4).
% 0.23/0.36 tff(func_def_68, type, g_s54_54: set_4).
% 0.23/0.36 tff(func_def_69, type, g_s55_55: set_4).
% 0.23/0.36 tff(func_def_70, type, g_s56_56: set_4).
% 0.23/0.36 tff(func_def_71, type, g_s57_57: set_4).
% 0.23/0.36 tff(func_def_72, type, g_s58_58: set_4).
% 0.23/0.36 tff(func_def_73, type, g_s59_59: set_4).
% 0.23/0.36 tff(func_def_74, type, g_s60_60: set_4).
% 0.23/0.36 tff(func_def_75, type, g_s66_61: $int).
% 0.23/0.36 tff(func_def_76, type, g_s67_62: $int).
% 0.23/0.36 tff(func_def_77, type, g_s68_63: $int).
% 0.23/0.36 tff(func_def_78, type, g_s69_64: $int).
% 0.23/0.36 tff(func_def_79, type, g_s70_65: $int).
% 0.23/0.36 tff(func_def_80, type, g_s71_66: $int).
% 0.23/0.36 tff(func_def_81, type, g_s72_67: $int).
% 0.23/0.36 tff(func_def_82, type, g_s73_68: $int).
% 0.23/0.36 tff(func_def_83, type, g_s74_69: $int).
% 0.23/0.36 tff(func_def_84, type, g_s75_70: $int).
% 0.23/0.36 tff(func_def_85, type, g_s76_71: $int).
% 0.23/0.36 tff(func_def_86, type, g_s77_72: $int).
% 0.23/0.36 tff(func_def_87, type, g_s78_73: $int).
% 0.23/0.36 tff(func_def_88, type, g_s79_74: $int).
% 0.23/0.36 tff(func_def_89, type, g_s80_75: $int).
% 0.23/0.36 tff(func_def_90, type, g_s81_76: $int).
% 0.23/0.36 tff(func_def_91, type, g_s82_77: $int).
% 0.23/0.36 tff(func_def_92, type, g_s83_78: $int).
% 0.23/0.36 tff(func_def_93, type, g_s84_79: $int).
% 0.23/0.36 tff(func_def_94, type, g_s85_80: $int).
% 0.23/0.36 tff(func_def_95, type, g_s86_81: $int).
% 0.23/0.36 tff(func_def_96, type, g_s87_82: $int).
% 0.23/0.36 tff(func_def_97, type, g_s88_83: $int).
% 0.23/0.36 tff(func_def_98, type, g_s89_84: $int).
% 0.23/0.36 tff(func_def_99, type, g_s90_85: $int).
% 0.23/0.36 tff(func_def_100, type, g_s91_86: $int).
% 0.23/0.36 tff(func_def_101, type, g_s92_87: $int).
% 0.23/0.36 tff(func_def_102, type, g_s93_88: $int).
% 0.23/0.36 tff(func_def_103, type, g_s94_89: $int).
% 0.23/0.36 tff(func_def_104, type, g_s95_90: $int).
% 0.23/0.36 tff(func_def_105, type, g_s96_91: $int).
% 0.23/0.36 tff(func_def_106, type, g_s97_92: $int).
% 0.23/0.36 tff(func_def_107, type, g_s98_93: $int).
% 0.23/0.36 tff(func_def_108, type, g_s99_94: $int).
% 0.23/0.36 tff(func_def_109, type, g_s100_95: $int).
% 0.23/0.36 tff(func_def_110, type, g_s101_96: $int).
% 0.23/0.36 tff(func_def_111, type, g_s102_97: $int).
% 0.23/0.36 tff(func_def_112, type, g_s103_98: $int).
% 0.23/0.36 tff(func_def_113, type, g_s104_99: $int).
% 0.23/0.36 tff(func_def_114, type, g_s105_100: $int).
% 0.23/0.36 tff(func_def_115, type, g_s106_101: $int).
% 0.23/0.36 tff(func_def_116, type, g_s107_102: $int).
% 0.23/0.36 tff(func_def_117, type, g_s108_103: $int).
% 0.23/0.36 tff(func_def_118, type, g_s109_104: $int).
% 0.23/0.36 tff(func_def_119, type, g_s110_105: $int).
% 0.23/0.36 tff(func_def_120, type, g_s111_106: $int).
% 0.23/0.36 tff(func_def_121, type, g_s112_107: $int).
% 0.23/0.36 tff(func_def_122, type, g_s113_108: $int).
% 0.23/0.36 tff(func_def_123, type, g_s114_109: $int).
% 0.23/0.36 tff(func_def_124, type, g_s115_110: $int).
% 0.23/0.36 tff(func_def_125, type, g_s116_111: $int).
% 0.23/0.36 tff(func_def_126, type, g_s117_112: $int).
% 0.23/0.36 tff(func_def_127, type, g_s118_113: $int).
% 0.23/0.36 tff(func_def_128, type, g_s119_114: $int).
% 0.23/0.36 tff(func_def_129, type, g_s120_115: $int).
% 0.23/0.36 tff(func_def_130, type, g_s121_116: $int).
% 0.23/0.36 tff(func_def_131, type, g_s122_117: $int).
% 0.23/0.36 tff(func_def_132, type, g_s123_118: $int).
% 0.23/0.36 tff(func_def_133, type, g_s124_119: $int).
% 0.23/0.36 tff(func_def_134, type, g_s125_120: $int).
% 0.23/0.36 tff(func_def_135, type, g_s126_121: $int).
% 0.23/0.36 tff(func_def_136, type, g_s127_122: $int).
% 0.23/0.36 tff(func_def_137, type, g_s128_123: $int).
% 0.23/0.36 tff(func_def_138, type, g_s129_124: $int).
% 0.23/0.36 tff(func_def_139, type, g_s130_125: $int).
% 0.23/0.36 tff(func_def_140, type, g_s131_126: $int).
% 0.23/0.36 tff(func_def_141, type, g_s132_127: $int).
% 0.23/0.36 tff(func_def_142, type, g_s133_128: $int).
% 0.23/0.36 tff(func_def_143, type, g_s134_129: $int).
% 0.23/0.36 tff(func_def_144, type, g_s135_130: $int).
% 0.23/0.36 tff(func_def_145, type, g_s136_131: $int).
% 0.23/0.36 tff(func_def_146, type, g_s137_132: $int).
% 0.23/0.36 tff(func_def_147, type, g_s138_133: $int).
% 0.23/0.36 tff(func_def_148, type, g_s139_134: $int).
% 0.23/0.36 tff(func_def_149, type, g_s140_135: $int).
% 0.23/0.36 tff(func_def_150, type, g_s141_136: $int).
% 0.23/0.36 tff(func_def_151, type, g_s142_137: $int).
% 0.23/0.36 tff(func_def_152, type, g_s143_138: $int).
% 0.23/0.36 tff(func_def_153, type, g_s144_139: $int).
% 0.23/0.36 tff(func_def_154, type, g_s145_140: $int).
% 0.23/0.36 tff(func_def_155, type, g_s146_141: $int).
% 0.23/0.36 tff(func_def_156, type, g_s147_142: $int).
% 0.23/0.36 tff(func_def_157, type, g_s148_143: $int).
% 0.23/0.36 tff(func_def_158, type, g_s149_144: $int).
% 0.23/0.36 tff(func_def_159, type, g_s150_145: $int).
% 0.23/0.36 tff(func_def_160, type, g_s151_146: $int).
% 0.23/0.36 tff(func_def_161, type, g_s152_147: $int).
% 0.23/0.36 tff(func_def_162, type, g_s153_148: $int).
% 0.23/0.36 tff(func_def_163, type, g_s154_149: $int).
% 0.23/0.36 tff(func_def_164, type, g_s155_150: $int).
% 0.23/0.36 tff(func_def_165, type, g_s156_151: $int).
% 0.23/0.36 tff(func_def_166, type, g_s157_152: $int).
% 0.23/0.36 tff(func_def_167, type, g_s158_153: $int).
% 0.23/0.36 tff(func_def_168, type, g_s159_154: $int).
% 0.23/0.36 tff(func_def_169, type, g_s160_155: $int).
% 0.23/0.36 tff(func_def_170, type, g_s161_156: $int).
% 0.23/0.36 tff(func_def_171, type, g_s162_157: $int).
% 0.23/0.36 tff(func_def_172, type, g_s163_158: $int).
% 0.23/0.36 tff(func_def_173, type, g_s164_159: $int).
% 0.23/0.36 tff(func_def_174, type, g_s165_160: $int).
% 0.23/0.36 tff(func_def_175, type, g_s166_161: $int).
% 0.23/0.36 tff(func_def_176, type, g_s167_162: $int).
% 0.23/0.36 tff(func_def_177, type, g_s168_163: $int).
% 0.23/0.36 tff(func_def_178, type, g_s169_164: $int).
% 0.23/0.36 tff(func_def_179, type, g_s170_165: $int).
% 0.23/0.36 tff(func_def_180, type, g_s171_166: $int).
% 0.23/0.36 tff(func_def_181, type, g_s172_167: $int).
% 0.23/0.36 tff(func_def_182, type, g_s173_168: $int).
% 0.23/0.36 tff(func_def_183, type, g_s174_169: $int).
% 0.23/0.36 tff(func_def_184, type, g_s175_170: $int).
% 0.23/0.36 tff(func_def_185, type, g_s176_171: $int).
% 0.23/0.36 tff(func_def_186, type, g_s177_172: $int).
% 0.23/0.36 tff(func_def_187, type, g_s178_173: $int).
% 0.23/0.36 tff(func_def_188, type, g_s179_174: $int).
% 0.23/0.36 tff(func_def_189, type, g_s180_175: $int).
% 0.23/0.36 tff(func_def_190, type, g_s181_176: $int).
% 0.23/0.36 tff(func_def_191, type, g_s182_177: $int).
% 0.23/0.36 tff(func_def_192, type, g_s183_178: $int).
% 0.23/0.36 tff(func_def_193, type, g_s184_179: $int).
% 0.23/0.36 tff(func_def_194, type, g_s185_180: set_0).
% 0.23/0.36 tff(func_def_195, type, g_s186_181: set_0).
% 0.23/0.36 tff(func_def_196, type, g_s187_182: $int).
% 0.23/0.36 tff(func_def_197, type, g_s188_183: $int).
% 0.23/0.36 tff(func_def_198, type, g_s189_184: $int).
% 0.23/0.36 tff(func_def_199, type, g_s190_185: $int).
% 0.23/0.36 tff(func_def_200, type, g_s191_186: $int).
% 0.23/0.36 tff(func_def_201, type, g_s192_187: $int).
% 0.23/0.36 tff(func_def_202, type, g_s193_188: $int).
% 0.23/0.36 tff(func_def_203, type, g_s194_189: $int).
% 0.23/0.36 tff(func_def_204, type, g_s195_190: $int).
% 0.23/0.36 tff(func_def_205, type, g_s196_191: $int).
% 0.23/0.36 tff(func_def_206, type, g_s197_192: $int).
% 0.23/0.36 tff(func_def_207, type, g_s198_193: $int).
% 0.23/0.36 tff(func_def_208, type, g_s199_194: $int).
% 0.23/0.36 tff(func_def_209, type, g_s200_195: $int).
% 0.23/0.36 tff(func_def_210, type, g_s201_196: $int).
% 0.23/0.36 tff(func_def_211, type, g_s202_197: $int).
% 0.23/0.36 tff(func_def_212, type, g_s203_198: $int).
% 0.23/0.36 tff(func_def_213, type, g_s204_199: $int).
% 0.23/0.36 tff(func_def_214, type, g_s205_200: $int).
% 0.23/0.36 tff(func_def_215, type, g_s206_201: $int).
% 0.23/0.36 tff(func_def_216, type, g_s207_202: $int).
% 0.23/0.36 tff(func_def_217, type, g_s208_203: $int).
% 0.23/0.36 tff(func_def_218, type, g_s209_204: $int).
% 0.23/0.36 tff(func_def_219, type, g_s210_205: $int).
% 0.23/0.36 tff(func_def_220, type, g_s211_206: $int).
% 0.23/0.36 tff(func_def_221, type, g_s212_207: $int).
% 0.23/0.36 tff(func_def_222, type, g_s213_208: $int).
% 0.23/0.36 tff(func_def_223, type, g_s214_209: $int).
% 0.23/0.36 tff(func_def_224, type, g_s215_210: $int).
% 0.23/0.36 tff(func_def_225, type, g_s216_211: $int).
% 0.23/0.36 tff(func_def_226, type, g_s217_212: $int).
% 0.23/0.36 tff(func_def_227, type, g_s218_213: $int).
% 0.23/0.36 tff(func_def_228, type, g_s219_214: $int).
% 0.23/0.36 tff(func_def_229, type, g_s220_215: $int).
% 0.23/0.36 tff(func_def_230, type, g_s221_216: $int).
% 0.23/0.36 tff(func_def_231, type, g_s222_217: $int).
% 0.23/0.36 tff(func_def_232, type, g_s223_218: $int).
% 0.23/0.36 tff(func_def_233, type, g_s224_219: $int).
% 0.23/0.36 tff(func_def_234, type, g_s225_220: $int).
% 0.23/0.36 tff(func_def_235, type, g_s226_221: $int).
% 0.23/0.36 tff(func_def_236, type, g_s227_222: $int).
% 0.23/0.36 tff(func_def_237, type, g_s228_223: $int).
% 0.23/0.36 tff(func_def_238, type, g_s229_224: $int).
% 0.23/0.36 tff(func_def_239, type, g_s230_225: $int).
% 0.23/0.36 tff(func_def_240, type, g_s231_226: $int).
% 0.23/0.36 tff(func_def_241, type, g_s232_227: $int).
% 0.23/0.36 tff(func_def_242, type, g_s233_228: $int).
% 0.23/0.36 tff(func_def_243, type, g_s234_229: $int).
% 0.23/0.36 tff(func_def_244, type, g_s235_230: $int).
% 0.23/0.36 tff(func_def_245, type, g_s236_231: $int).
% 0.23/0.36 tff(func_def_246, type, g_s237_232: $int).
% 0.23/0.36 tff(func_def_247, type, g_s238_233: $int).
% 0.23/0.36 tff(func_def_248, type, g_s239_234: $int).
% 0.23/0.36 tff(func_def_249, type, g_s240_235: $int).
% 0.23/0.36 tff(func_def_250, type, g_s241_236: $int).
% 0.23/0.36 tff(func_def_251, type, g_s242_237: $int).
% 0.23/0.36 tff(func_def_252, type, g_s243_238: $int).
% 0.23/0.36 tff(func_def_253, type, g_s244_239: $int).
% 0.23/0.36 tff(func_def_254, type, g_s245_240: $int).
% 0.23/0.36 tff(func_def_255, type, g_s246_241: $int).
% 0.23/0.36 tff(func_def_256, type, g_s247_242: $int).
% 0.23/0.36 tff(func_def_257, type, g_s248_243: $int).
% 0.23/0.36 tff(func_def_258, type, g_s249_244: $int).
% 0.23/0.36 tff(func_def_259, type, g_s250_245: $int).
% 0.23/0.36 tff(func_def_260, type, g_s251_246: $int).
% 0.23/0.36 tff(func_def_261, type, g_s252_247: $int).
% 0.23/0.36 tff(func_def_262, type, g_s253_248: $int).
% 0.23/0.36 tff(func_def_263, type, g_s254_249: $int).
% 0.23/0.36 tff(func_def_264, type, g_s255_250: $int).
% 0.23/0.36 tff(func_def_265, type, g_s256_251: $int).
% 0.23/0.36 tff(func_def_266, type, g_s257_252: $int).
% 0.23/0.36 tff(func_def_267, type, g_s258_253: $int).
% 0.23/0.36 tff(func_def_268, type, g_s259_254: $int).
% 0.23/0.36 tff(func_def_269, type, g_s260_255: $int).
% 0.23/0.36 tff(func_def_270, type, g_s261_256: $int).
% 0.23/0.36 tff(func_def_271, type, g_s262_257: $int).
% 0.23/0.36 tff(func_def_272, type, g_s263_258: $int).
% 0.23/0.36 tff(func_def_273, type, g_s264_259: $int).
% 0.23/0.36 tff(func_def_274, type, g_s265_260: $int).
% 0.23/0.36 tff(func_def_275, type, g_s266_261: $int).
% 0.23/0.36 tff(func_def_276, type, g_s267_262: $int).
% 0.23/0.36 tff(func_def_277, type, g_s268_263: $int).
% 0.23/0.36 tff(func_def_278, type, g_s269_264: $int).
% 0.23/0.36 tff(func_def_279, type, g_s270_265: $int).
% 0.23/0.36 tff(func_def_280, type, g_s271_266: $int).
% 0.23/0.36 tff(func_def_281, type, g_s272_267: $int).
% 0.23/0.36 tff(func_def_282, type, g_s273_268: $int).
% 0.23/0.36 tff(func_def_283, type, g_s274_269: $int).
% 0.23/0.36 tff(func_def_284, type, g_s275_270: $int).
% 0.23/0.36 tff(func_def_285, type, g_s276_271: $int).
% 0.23/0.36 tff(func_def_286, type, g_s277_272: $int).
% 0.23/0.36 tff(func_def_287, type, g_s278_273: $int).
% 0.23/0.36 tff(func_def_288, type, g_s279_274: $int).
% 0.23/0.36 tff(func_def_289, type, g_s280_275: $int).
% 0.23/0.36 tff(func_def_290, type, g_s281_276: $int).
% 0.23/0.36 tff(func_def_291, type, g_s282_277: $int).
% 0.23/0.36 tff(func_def_292, type, g_s283_278: $int).
% 0.23/0.36 tff(func_def_293, type, g_s284_279: $int).
% 0.23/0.36 tff(func_def_294, type, g_s285_280: $int).
% 0.23/0.36 tff(func_def_295, type, g_s286_281: $int).
% 0.23/0.36 tff(func_def_296, type, g_s287_282: $int).
% 0.23/0.36 tff(func_def_297, type, g_s288_283: $int).
% 0.23/0.36 tff(func_def_298, type, g_s289_284: $int).
% 0.23/0.36 tff(func_def_299, type, g_s290_285: $int).
% 0.23/0.36 tff(func_def_300, type, g_s291_286: $int).
% 0.23/0.36 tff(func_def_301, type, g_s292_287: $int).
% 0.23/0.36 tff(func_def_302, type, g_s293_288: $int).
% 0.23/0.36 tff(func_def_303, type, g_s294_289: $int).
% 0.23/0.36 tff(func_def_304, type, g_s295_290: $int).
% 0.23/0.36 tff(func_def_305, type, g_s296_291: $int).
% 0.23/0.36 tff(func_def_306, type, g_s297_292: $int).
% 0.23/0.36 tff(func_def_307, type, g_s298_293: $int).
% 0.23/0.36 tff(func_def_308, type, g_s299_294: $int).
% 0.23/0.36 tff(func_def_309, type, g_s300_295: $int).
% 0.23/0.36 tff(func_def_310, type, g_s301_296: set_4).
% 0.23/0.36 tff(func_def_311, type, g_s302_297: set_3).
% 0.23/0.36 tff(func_def_312, type, g_s303_298: set_4).
% 0.23/0.36 tff(func_def_313, type, g_s304_299: set_3).
% 0.23/0.36 tff(func_def_314, type, g_s305_300: set_4).
% 0.23/0.36 tff(func_def_315, type, g_s322_301: set_4).
% 0.23/0.36 tff(func_def_316, type, g_s323_302: set_4).
% 0.23/0.36 tff(func_def_317, type, g_s328_1_336: set_4).
% 0.23/0.36 tff(func_def_318, type, g_s329_1_337: set_4).
% 0.23/0.36 tff(func_def_319, type, g_s331_1_338: set_4).
% 0.23/0.36 tff(func_def_320, type, g_s332_1_339: set_4).
% 0.23/0.36 tff(func_def_321, type, g_s339_1_340: set_0).
% 0.23/0.36 tff(func_def_322, type, g_s340_1_341: set_0).
% 0.23/0.36 tff(func_def_323, type, g_s326_1_342: $int).
% 0.23/0.36 tff(func_def_324, type, g_s335_1_343: set_3).
% 0.23/0.36 tff(func_def_325, type, g_s336_1_344: set_3).
% 0.23/0.36 tff(func_def_326, type, g_s337_1_345: set_3).
% 0.23/0.36 tff(func_def_327, type, g_s338_1_346: set_3).
% 0.23/0.36 tff(func_def_328, type, g_s306_303: set_0).
% 0.23/0.36 tff(func_def_329, type, g_s307_304: set_0).
% 0.23/0.36 tff(func_def_330, type, g_s308_305: set_0).
% 0.23/0.36 tff(func_def_331, type, g_s309_306: set_0).
% 0.23/0.36 tff(func_def_332, type, g_s310_307: set_3).
% 0.23/0.36 tff(func_def_333, type, g_s311_308: set_3).
% 0.23/0.36 tff(func_def_334, type, g_s312_309: set_3).
% 0.23/0.36 tff(func_def_335, type, g_s313_310: set_3).
% 0.23/0.36 tff(func_def_336, type, g_s314_311: set_0).
% 0.23/0.36 tff(func_def_337, type, g_s315_312: set_0).
% 0.23/0.36 tff(func_def_338, type, g_s316_313: set_0).
% 0.23/0.36 tff(func_def_339, type, g_s317_314: set_0).
% 0.23/0.36 tff(func_def_340, type, g_s318_315: set_3).
% 0.23/0.36 tff(func_def_341, type, g_s319_316: set_3).
% 0.23/0.36 tff(func_def_342, type, g_s320_317: set_0).
% 0.23/0.36 tff(func_def_343, type, g_s321_318: set_3).
% 0.23/0.36 tff(func_def_344, type, g_s326_325: $int).
% 0.23/0.36 tff(func_def_345, type, g_s328_319: set_4).
% 0.23/0.36 tff(func_def_346, type, g_s329_320: set_4).
% 0.23/0.36 tff(func_def_347, type, g_s331_321: set_4).
% 0.23/0.36 tff(func_def_348, type, g_s332_322: set_4).
% 0.23/0.36 tff(func_def_349, type, g_s335_326: set_3).
% 0.23/0.36 tff(func_def_350, type, g_s336_327: set_3).
% 0.23/0.36 tff(func_def_351, type, g_s337_328: set_3).
% 0.23/0.36 tff(func_def_352, type, g_s338_329: set_3).
% 0.23/0.36 tff(func_def_353, type, g_s339_323: set_0).
% 0.23/0.36 tff(func_def_354, type, g_s340_324: set_0).
% 0.23/0.36 tff(func_def_355, type, g_s358_335: $int).
% 0.23/0.36 tff(func_def_356, type, g_s369_361: $int).
% 0.23/0.36 tff(func_def_357, type, g_s369_1_362: $int).
% 0.23/0.36 tff(func_def_358, type, g_s375_364: $int).
% 0.23/0.36 tff(func_def_370, type, sK0: set_3).
% 0.23/0.36 tff(func_def_371, type, sK1: $int > $int).
% 0.23/0.36 tff(func_def_372, type, sK2: set_3).
% 0.23/0.36 tff(func_def_373, type, sK3: $int > $int).
% 0.23/0.36 tff(func_def_374, type, sK4: set_4).
% 0.23/0.36 tff(func_def_375, type, sK5: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_376, type, sK6: set_4).
% 0.23/0.36 tff(func_def_377, type, sK7: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_378, type, sK8: set_4).
% 0.23/0.36 tff(func_def_379, type, sK9: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_380, type, sK10: set_4).
% 0.23/0.36 tff(func_def_381, type, sK11: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_382, type, sK12: set_3).
% 0.23/0.36 tff(func_def_383, type, sK13: $int > $int).
% 0.23/0.36 tff(func_def_384, type, sK14: set_4).
% 0.23/0.36 tff(func_def_385, type, sK15: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_386, type, sK16: set_4).
% 0.23/0.36 tff(func_def_387, type, sK17: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_390, type, sK22: set_3).
% 0.23/0.36 tff(func_def_391, type, sK23: $int > $int).
% 0.23/0.36 tff(func_def_392, type, sK24: set_4).
% 0.23/0.36 tff(func_def_393, type, sK25: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_394, type, sK26: set_4).
% 0.23/0.36 tff(func_def_395, type, sK27: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_396, type, sK28: set_3).
% 0.23/0.36 tff(func_def_397, type, sK29: $int > $int).
% 0.23/0.36 tff(func_def_398, type, sK30: set_4).
% 0.23/0.36 tff(func_def_399, type, sK31: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_400, type, sK32: set_4).
% 0.23/0.36 tff(func_def_401, type, sK33: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_402, type, sK34: set_3).
% 0.23/0.36 tff(func_def_403, type, sK35: $int > $int).
% 0.23/0.36 tff(func_def_404, type, sK36: set_4).
% 0.23/0.36 tff(func_def_405, type, sK37: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_406, type, sK38: set_4).
% 0.23/0.36 tff(func_def_407, type, sK39: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_408, type, sK40: set_4).
% 0.23/0.36 tff(func_def_409, type, sK41: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_410, type, sK42: set_4).
% 0.23/0.36 tff(func_def_411, type, sK43: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_412, type, sK44: set_4).
% 0.23/0.36 tff(func_def_413, type, sK45: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_414, type, sK46: set_4).
% 0.23/0.36 tff(func_def_415, type, sK47: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_416, type, sK48: set_4).
% 0.23/0.36 tff(func_def_417, type, sK49: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_418, type, sK50: set_4).
% 0.23/0.36 tff(func_def_419, type, sK51: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_420, type, sK52: set_4).
% 0.23/0.36 tff(func_def_421, type, sK53: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_422, type, sK54: set_4).
% 0.23/0.36 tff(func_def_423, type, sK55: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_424, type, sK56: set_4).
% 0.23/0.36 tff(func_def_425, type, sK57: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_426, type, sK58: set_4).
% 0.23/0.36 tff(func_def_427, type, sK59: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_428, type, sK60: set_4).
% 0.23/0.36 tff(func_def_429, type, sK61: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_430, type, sK62: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_431, type, sK63: set_4).
% 0.23/0.36 tff(func_def_432, type, sK64: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_433, type, sK65: set_4).
% 0.23/0.36 tff(func_def_434, type, sK66: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_435, type, sK67: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_436, type, sK68: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_437, type, sK69: set_3).
% 0.23/0.36 tff(func_def_438, type, sK70: $int > $int).
% 0.23/0.36 tff(func_def_439, type, sK71: set_3).
% 0.23/0.36 tff(func_def_440, type, sK72: $int > $int).
% 0.23/0.36 tff(func_def_441, type, sK73: set_3).
% 0.23/0.36 tff(func_def_442, type, sK74: $int > $int).
% 0.23/0.36 tff(func_def_443, type, sK75: set_4).
% 0.23/0.36 tff(func_def_444, type, sK76: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_445, type, sK77: set_4).
% 0.23/0.36 tff(func_def_446, type, sK78: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_447, type, sK79: set_4).
% 0.23/0.36 tff(func_def_448, type, sK80: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_449, type, sK81: set_4).
% 0.23/0.36 tff(func_def_450, type, sK82: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_451, type, sK83: set_4).
% 0.23/0.36 tff(func_def_452, type, sK84: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_453, type, sK85: set_4).
% 0.23/0.36 tff(func_def_454, type, sK86: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_455, type, sK87: set_4).
% 0.23/0.36 tff(func_def_456, type, sK88: ($int * $int) > $int).
% 0.23/0.36 tff(func_def_457, type, sK89: set_3).
% 0.23/0.36 tff(func_def_458, type, sK90: $int > $int).
% 0.23/0.36 tff(func_def_459, type, sK91: set_3).
% 0.23/0.36 tff(func_def_460, type, sK92: $int > $int).
% 0.23/0.36 tff(func_def_461, type, sK93: set_3).
% 0.23/0.36 tff(func_def_462, type, sK94: $int > $int).
% 0.23/0.36 tff(func_def_463, type, sK95: set_3).
% 0.23/0.36 tff(func_def_464, type, sK96: $int > $int).
% 0.23/0.36 tff(func_def_465, type, sK97: set_3).
% 0.23/0.36 tff(func_def_466, type, sK98: $int > $int).
% 0.23/0.36 tff(func_def_467, type, sK99: $int).
% 0.23/0.36 tff(func_def_468, type, sK101: $int).
% 0.23/0.36 tff(func_def_469, type, sK103: $int).
% 0.23/0.36 tff(func_def_470, type, sK104: $int > $int).
% 0.23/0.36 tff(func_def_471, type, sK105: $int).
% 0.23/0.36 tff(func_def_472, type, sK106: $int).
% 0.23/0.36 tff(func_def_473, type, sK107: $int > $int).
% 0.23/0.36 tff(pred_def_1, type, mem0: ($int * set_0) > $o).
% 0.23/0.36 tff(pred_def_4, type, mem2: ($o * $int * set_2) > $o).
% 0.23/0.36 tff(pred_def_5, type, mem3: ($int * $int * set_3) > $o).
% 0.23/0.36 tff(pred_def_6, type, mem4: ($int * $int * $int * set_4) > $o).
% 0.23/0.36 tff(pred_def_16, type, sP18: $o > $o).
% 0.23/0.36 tff(pred_def_18, type, sP20: $o > $o).
% 0.23/0.36 tff(pred_def_20, type, sK100: $int > $o).
% 0.23/0.36 tff(f110,axiom,(
% 0.23/0.36 ! [X0 : $int] : (mem0(X0,g_s40_40) <=> (X0 = g_s38_38 | X0 = g_s39_39))),
% 0.23/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:ctx:17')).
% 0.23/0.36 tff(f121,axiom,(
% 0.23/0.36 ! [X0 : $int,X1 : $o] : (mem2(X1,X0,g_s41_41) <=> (((X1 <=> $true) & X0 = g_s38_38) | ((X1 <=> $false) & X0 = g_s39_39)))),
% 0.23/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:ctx:18')).
% 0.23/0.36 tff(f506,conjecture,(
% 0.23/0.36 ! [X0 : $int] : (! [X1 : $o] : ((X1 <=> ? [X2 : $int] : ! [X3 : $int] : (X3 = $sum(g_s358_335,1) => mem3(X3,X2,g_s319_316))) => mem2(X1,X0,g_s41_41)) => mem0(X0,g_s40_40))),
% 0.23/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Goal')).
% 0.23/0.36 tff(f507,negated_conjecture,(
% 0.23/0.36 ~ ! [X0 : $int] : (! [X1 : $o] : ((X1 <=> ? [X2 : $int] : ! [X3 : $int] : (X3 = $sum(g_s358_335,1) => mem3(X3,X2,g_s319_316))) => mem2(X1,X0,g_s41_41)) => mem0(X0,g_s40_40))),
% 0.23/0.36 inference(negated_conjecture,[status(cth)],[f506])).
% 0.23/0.36 tff(f540,plain,(
% 0.23/0.36 ! [X0 : $int,X1 : $o] : (mem2(X1,X0,g_s41_41) <=> (((X1 <=> $true) & X0 = g_s38_38) | ((X1 <=> $false) & X0 = g_s39_39)))),
% 0.23/0.36 inference(theory_normalization,[],[f121])).
% 0.23/0.36 tff(f672,plain,(
% 0.23/0.36 ~ ! [X0 : $int] : (! [X1 : $o] : ((X1 <=> ? [X2 : $int] : ! [X3 : $int] : (X3 = $sum(g_s358_335,1) => mem3(X3,X2,g_s319_316))) => mem2(X1,X0,g_s41_41)) => mem0(X0,g_s40_40))),
% 0.23/0.36 inference(theory_normalization,[],[f507])).
% 0.23/0.36 tff(f673,definition,(
% 0.23/0.36 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 0.23/0.36 introduced(theory,[tha_commutativity])).
% 0.23/0.36 tff(f691,plain,(
% 0.23/0.36 ! [X0 : $int,X1 : $o] : (mem2(X1,X0,g_s41_41) <=> (((X1 <=> $true) & X0 = g_s38_38) | ((X1 <=> $false) & X0 = g_s39_39)))),
% 0.23/0.36 inference(rectify,[],[f540])).
% 0.23/0.36 tff(f698,plain,(
% 0.23/0.36 ~ ! [X0 : $int] : (! [X1 : $o] : ((X1 <=> ? [X2 : $int] : ! [X3 : $int] : (X3 = $sum(g_s358_335,1) => mem3(X3,X2,g_s319_316))) => mem2(X1,X0,g_s41_41)) => mem0(X0,g_s40_40))),
% 0.23/0.36 inference(rectify,[],[f672])).
% 0.23/0.36 tff(f848,plain,(
% 0.23/0.36 ? [X0 : $int] : (~mem0(X0,g_s40_40) & ! [X1 : $o] : (mem2(X1,X0,g_s41_41) | (X1 <~> ? [X2 : $int] : ! [X3 : $int] : (mem3(X3,X2,g_s319_316) | $sum(g_s358_335,1) != X3))))),
% 0.23/0.36 inference(ennf_transformation,[],[f698])).
% 0.23/0.36 tff(f1037,plain,(
% 0.23/0.36 ( ! [X0 : $int] : (g_s39_39 != X0 | mem0(X0,g_s40_40)) )),
% 0.23/0.36 inference(cnf_transformation,[],[f110])).
% 0.23/0.36 tff(f1038,plain,(
% 0.23/0.36 ( ! [X0 : $int] : (g_s38_38 != X0 | mem0(X0,g_s40_40)) )),
% 0.23/0.36 inference(cnf_transformation,[],[f110])).
% 0.23/0.36 tff(f1049,plain,(
% 0.23/0.36 sP21),
% 0.23/0.36 inference(cnf_transformation,[],[f691])).
% 0.23/0.36 tff(f1051,plain,(
% 0.23/0.36 ~sP20($false)),
% 0.23/0.36 inference(cnf_transformation,[],[f691])).
% 0.23/0.36 tff(f1052,plain,(
% 0.23/0.36 ~sP19),
% 0.23/0.36 inference(cnf_transformation,[],[f691])).
% 0.23/0.36 tff(f1053,plain,(
% 0.23/0.36 sP18($true)),
% 0.23/0.36 inference(cnf_transformation,[],[f691])).
% 0.23/0.36 tff(f1055,plain,(
% 0.23/0.36 ( ! [X0 : $int] : (g_s39_39 = X0 | ~sP21 | sP20($false) | ~mem2($false,X0,g_s41_41)) )),
% 0.23/0.36 inference(cnf_transformation,[],[f691])).
% 0.23/0.36 tff(f1078,plain,(
% 0.23/0.36 ( ! [X0 : $int] : (sP19 | ~sP18($true) | g_s38_38 = X0 | ~mem2($true,X0,g_s41_41)) )),
% 0.23/0.36 inference(cnf_transformation,[],[f691])).
% 0.23/0.36 tff(f1849,plain,(
% 0.23/0.36 ( ! [X3 : $int] : ($sum(g_s358_335,1) != X3 | mem3(X3,sK106,g_s319_316) | mem2($false,sK105,g_s41_41)) )),
% 0.23/0.36 inference(cnf_transformation,[],[f848])).
% 0.23/0.36 tff(f1850,plain,(
% 0.23/0.36 ( ! [X2 : $int] : ($sum(g_s358_335,1) = sK107(X2) | mem2($true,sK105,g_s41_41)) )),
% 0.23/0.36 inference(cnf_transformation,[],[f848])).
% 0.23/0.36 tff(f1851,plain,(
% 0.23/0.36 ( ! [X2 : $int] : (~mem3(sK107(X2),X2,g_s319_316) | mem2($true,sK105,g_s41_41)) )),
% 0.23/0.36 inference(cnf_transformation,[],[f848])).
% 0.23/0.36 tff(f1852,plain,(
% 0.23/0.36 ~mem0(sK105,g_s40_40)),
% 0.23/0.36 inference(cnf_transformation,[],[f848])).
% 0.23/0.36 tff(f1908,plain,(
% 0.23/0.36 mem0(g_s38_38,g_s40_40)),
% 0.23/0.36 inference(equality_resolution,[],[f1038])).
% 0.23/0.36 tff(f1909,plain,(
% 0.23/0.36 mem0(g_s39_39,g_s40_40)),
% 0.23/0.36 inference(equality_resolution,[],[f1037])).
% 0.23/0.36 tff(f1969,plain,(
% 0.23/0.36 mem3($sum(g_s358_335,1),sK106,g_s319_316) | mem2($false,sK105,g_s41_41)),
% 0.23/0.36 inference(equality_resolution,[],[f1849])).
% 0.23/0.36 tff(f1972,plain,(
% 0.23/0.36 ( ! [X0 : $int] : (~sP19 | sP18($true) | g_s38_38 = X0 | mem2($true,X0,g_s41_41)) )),
% 0.23/0.36 inference(consistent_polarity_flipping,[],[f1078])).
% 0.23/0.36 tff(f1995,plain,(
% 0.23/0.36 ( ! [X0 : $int] : (g_s39_39 = X0 | sP21 | sP20($false) | mem2($false,X0,g_s41_41)) )),
% 0.23/0.36 inference(consistent_polarity_flipping,[],[f1055])).
% 0.23/0.36 tff(f1997,plain,(
% 0.23/0.36 ~sP18($true)),
% 0.23/0.36 inference(consistent_polarity_flipping,[],[f1053])).
% 0.23/0.36 tff(f1998,plain,(
% 0.23/0.36 sP19),
% 0.23/0.36 inference(consistent_polarity_flipping,[],[f1052])).
% 0.23/0.36 tff(f1999,plain,(
% 0.23/0.36 ~sP21),
% 0.23/0.36 inference(consistent_polarity_flipping,[],[f1049])).
% 0.23/0.36 tff(f2025,plain,(
% 0.23/0.36 ( ! [X2 : $int] : (~mem3(sK107(X2),X2,g_s319_316) | ~mem2($true,sK105,g_s41_41)) )),
% 0.23/0.36 inference(consistent_polarity_flipping,[],[f1851])).
% 0.23/0.36 tff(f2026,plain,(
% 0.23/0.36 ( ! [X2 : $int] : ($sum(g_s358_335,1) = sK107(X2) | ~mem2($true,sK105,g_s41_41)) )),
% 0.23/0.36 inference(consistent_polarity_flipping,[],[f1850])).
% 0.23/0.36 tff(f2027,plain,(
% 0.23/0.36 mem3($sum(g_s358_335,1),sK106,g_s319_316) | ~mem2($false,sK105,g_s41_41)),
% 0.23/0.36 inference(consistent_polarity_flipping,[],[f1969])).
% 0.23/0.36 tff(f2065,definition,(
% 0.23/0.36 spl108_1 <=> mem2($false,sK105,g_s41_41)),
% 0.23/0.36 introduced(definition,[new_symbols(definition,[spl108_1])],[avatar_definition])).
% 0.23/0.36 tff(f2067,plain,(
% 0.23/0.36 ~mem2($false,sK105,g_s41_41) | spl108_1),
% 0.23/0.36 inference(avatar_component_clause,[],[f2065])).
% 0.23/0.36 tff(f2069,definition,(
% 0.23/0.36 spl108_2 <=> mem3($sum(g_s358_335,1),sK106,g_s319_316)),
% 0.23/0.36 introduced(definition,[new_symbols(definition,[spl108_2])],[avatar_definition])).
% 0.23/0.36 tff(f2071,plain,(
% 0.23/0.36 mem3($sum(g_s358_335,1),sK106,g_s319_316) | ~spl108_2),
% 0.23/0.36 inference(avatar_component_clause,[],[f2069])).
% 0.23/0.36 tff(f2072,plain,(
% 0.23/0.36 ~spl108_1 | spl108_2),
% 0.23/0.36 inference(avatar_split_clause,[],[f2027,f2069,f2065])).
% 0.23/0.36 tff(f2074,definition,(
% 0.23/0.36 spl108_3 <=> mem2($true,sK105,g_s41_41)),
% 0.23/0.36 introduced(definition,[new_symbols(definition,[spl108_3])],[avatar_definition])).
% 0.23/0.36 tff(f2076,plain,(
% 0.23/0.36 ~mem2($true,sK105,g_s41_41) | spl108_3),
% 0.23/0.36 inference(avatar_component_clause,[],[f2074])).
% 0.23/0.36 tff(f2078,definition,(
% 0.23/0.36 spl108_4 <=> ! [X2 : $int] : $sum(g_s358_335,1) = sK107(X2)),
% 0.23/0.36 introduced(definition,[new_symbols(definition,[spl108_4])],[avatar_definition])).
% 0.23/0.36 tff(f2079,plain,(
% 0.23/0.36 ( ! [X2 : $int] : ($sum(g_s358_335,1) = sK107(X2)) ) | ~spl108_4),
% 0.23/0.36 inference(avatar_component_clause,[],[f2078])).
% 0.23/0.36 tff(f2080,plain,(
% 0.23/0.36 ~spl108_3 | spl108_4),
% 0.23/0.36 inference(avatar_split_clause,[],[f2026,f2078,f2074])).
% 0.23/0.36 tff(f2082,definition,(
% 0.23/0.36 spl108_5 <=> ! [X2 : $int] : ~mem3(sK107(X2),X2,g_s319_316)),
% 0.23/0.36 introduced(definition,[new_symbols(definition,[spl108_5])],[avatar_definition])).
% 0.23/0.36 tff(f2083,plain,(
% 0.23/0.36 ( ! [X2 : $int] : (~mem3(sK107(X2),X2,g_s319_316)) ) | ~spl108_5),
% 0.23/0.36 inference(avatar_component_clause,[],[f2082])).
% 0.23/0.36 tff(f2084,plain,(
% 0.23/0.36 ~spl108_3 | spl108_5),
% 0.23/0.36 inference(avatar_split_clause,[],[f2025,f2082,f2074])).
% 0.23/0.36 tff(f2146,definition,(
% 0.23/0.36 spl108_19 <=> sP20($false)),
% 0.23/0.36 introduced(definition,[new_symbols(definition,[spl108_19])],[avatar_definition])).
% 0.23/0.36 tff(f2150,definition,(
% 0.23/0.36 spl108_20 <=> sP21),
% 0.23/0.36 introduced(definition,[new_symbols(definition,[spl108_20])],[avatar_definition])).
% 0.23/0.36 tff(f2154,definition,(
% 0.23/0.36 spl108_21 <=> ! [X0 : $int] : (g_s39_39 = X0 | mem2($false,X0,g_s41_41))),
% 0.23/0.36 introduced(definition,[new_symbols(definition,[spl108_21])],[avatar_definition])).
% 0.23/0.36 tff(f2155,plain,(
% 0.23/0.36 ( ! [X0 : $int] : (mem2($false,X0,g_s41_41) | g_s39_39 = X0) ) | ~spl108_21),
% 0.23/0.36 inference(avatar_component_clause,[],[f2154])).
% 0.23/0.36 tff(f2156,plain,(
% 0.23/0.36 spl108_19 | spl108_20 | spl108_21),
% 0.23/0.36 inference(avatar_split_clause,[],[f1995,f2154,f2150,f2146])).
% 0.23/0.36 tff(f2175,definition,(
% 0.23/0.36 spl108_25 <=> sP18($true)),
% 0.23/0.36 introduced(definition,[new_symbols(definition,[spl108_25])],[avatar_definition])).
% 0.23/0.36 tff(f2179,definition,(
% 0.23/0.36 spl108_26 <=> sP19),
% 0.23/0.36 introduced(definition,[new_symbols(definition,[spl108_26])],[avatar_definition])).
% 0.23/0.36 tff(f2215,definition,(
% 0.23/0.36 spl108_32 <=> ! [X0 : $int] : (g_s38_38 = X0 | mem2($true,X0,g_s41_41))),
% 0.23/0.36 introduced(definition,[new_symbols(definition,[spl108_32])],[avatar_definition])).
% 0.23/0.36 tff(f2216,plain,(
% 0.23/0.36 ( ! [X0 : $int] : (mem2($true,X0,g_s41_41) | g_s38_38 = X0) ) | ~spl108_32),
% 0.23/0.36 inference(avatar_component_clause,[],[f2215])).
% 0.23/0.36 tff(f2218,plain,(
% 0.23/0.36 spl108_32 | spl108_25 | ~spl108_26),
% 0.23/0.36 inference(avatar_split_clause,[],[f1972,f2179,f2175,f2215])).
% 0.23/0.36 tff(f2219,plain,(
% 0.23/0.36 spl108_26),
% 0.23/0.36 inference(avatar_split_clause,[],[f1998,f2179])).
% 0.23/0.36 tff(f2220,plain,(
% 0.23/0.36 ~spl108_20),
% 0.23/0.36 inference(avatar_split_clause,[],[f1999,f2150])).
% 0.23/0.36 tff(f2222,plain,(
% 0.23/0.36 ~spl108_19),
% 0.23/0.36 inference(avatar_split_clause,[],[f1051,f2146])).
% 0.23/0.36 tff(f2224,plain,(
% 0.23/0.36 ~spl108_25),
% 0.23/0.36 inference(avatar_split_clause,[],[f1997,f2175])).
% 0.23/0.36 tff(f2406,plain,(
% 0.23/0.36 g_s39_39 = sK105 | (spl108_1 | ~spl108_21)),
% 0.23/0.36 inference(resolution,[],[f2155,f2067])).
% 0.23/0.36 tff(f2409,plain,(
% 0.23/0.36 g_s38_38 = sK105 | (spl108_3 | ~spl108_32)),
% 0.23/0.36 inference(resolution,[],[f2216,f2076])).
% 0.23/0.36 tff(f2467,plain,(
% 0.23/0.36 ~mem0(g_s39_39,g_s40_40) | (spl108_1 | ~spl108_21)),
% 0.23/0.36 inference(superposition,[],[f1852,f2406])).
% 0.23/0.36 tff(f2476,plain,(
% 0.23/0.36 $false | (spl108_1 | ~spl108_21)),
% 0.23/0.36 inference(forward_subsumption_resolution,[],[f2467,f1909])).
% 0.23/0.36 tff(f2477,plain,(
% 0.23/0.36 spl108_1 | ~spl108_21),
% 0.23/0.36 inference(avatar_contradiction_clause,[],[f2476])).
% 0.23/0.36 tff(f2478,plain,(
% 0.23/0.36 mem3($sum(1,g_s358_335),sK106,g_s319_316) | ~spl108_2),
% 0.23/0.36 inference(forward_demodulation,[],[f2071,f673])).
% 0.23/0.36 tff(f2482,plain,(
% 0.23/0.36 ~mem0(g_s38_38,g_s40_40) | (spl108_3 | ~spl108_32)),
% 0.23/0.36 inference(superposition,[],[f1852,f2409])).
% 0.23/0.36 tff(f2489,plain,(
% 0.23/0.36 $false | (spl108_3 | ~spl108_32)),
% 0.23/0.36 inference(forward_subsumption_resolution,[],[f2482,f1908])).
% 0.23/0.36 tff(f2490,plain,(
% 0.23/0.36 spl108_3 | ~spl108_32),
% 0.23/0.36 inference(avatar_contradiction_clause,[],[f2489])).
% 0.23/0.36 tff(f2492,plain,(
% 0.23/0.36 ( ! [X0 : $int,X1 : $int] : (sK107(X0) = sK107(X1)) ) | ~spl108_4),
% 0.23/0.36 inference(superposition,[],[f2079,f2079])).
% 0.23/0.36 tff(f2494,plain,(
% 0.23/0.36 ( ! [X0 : $int] : ($sum(1,g_s358_335) = sK107(X0)) ) | ~spl108_4),
% 0.23/0.36 inference(superposition,[],[f2079,f673])).
% 0.23/0.36 tff(f2516,plain,(
% 0.23/0.36 ( ! [X0 : $int,X1 : $int] : (~mem3(sK107(X0),X1,g_s319_316)) ) | (~spl108_4 | ~spl108_5)),
% 0.23/0.36 inference(superposition,[],[f2083,f2492])).
% 0.23/0.36 tff(f2553,plain,(
% 0.23/0.36 ( ! [X0 : $int] : (mem3(sK107(X0),sK106,g_s319_316)) ) | (~spl108_2 | ~spl108_4)),
% 0.23/0.36 inference(superposition,[],[f2478,f2494])).
% 0.23/0.36 tff(f2564,plain,(
% 0.23/0.36 $false | (~spl108_2 | ~spl108_4 | ~spl108_5)),
% 0.23/0.36 inference(forward_subsumption_resolution,[],[f2553,f2516])).
% 0.23/0.36 tff(f2565,plain,(
% 0.23/0.36 ~spl108_2 | ~spl108_4 | ~spl108_5),
% 0.23/0.36 inference(avatar_contradiction_clause,[],[f2564])).
% 0.23/0.36 cnf(s1, plain, ~spl108_1 | spl108_2, inference(sat_conversion,[],[f2072])).
% 0.23/0.36 cnf(s2, plain, ~spl108_3 | spl108_4, inference(sat_conversion,[],[f2080])).
% 0.23/0.36 cnf(s3, plain, ~spl108_3 | spl108_5, inference(sat_conversion,[],[f2084])).
% 0.23/0.36 cnf(s16, plain, spl108_19 | spl108_20 | spl108_21, inference(sat_conversion,[],[f2156])).
% 0.23/0.36 cnf(s39, plain, spl108_25 | ~spl108_26 | spl108_32, inference(sat_conversion,[],[f2218])).
% 0.23/0.36 cnf(s40, plain, spl108_26, inference(sat_conversion,[],[f2219])).
% 0.23/0.36 cnf(s41, plain, ~spl108_20, inference(sat_conversion,[],[f2220])).
% 0.23/0.36 cnf(s43, plain, ~spl108_19, inference(sat_conversion,[],[f2222])).
% 0.23/0.36 cnf(s45, plain, ~spl108_25, inference(sat_conversion,[],[f2224])).
% 0.23/0.36 cnf(s49, plain, spl108_1 | ~spl108_21, inference(sat_conversion,[],[f2477])).
% 0.23/0.36 cnf(s50, plain, spl108_3 | ~spl108_32, inference(sat_conversion,[],[f2490])).
% 0.23/0.36 cnf(s51, plain, ~spl108_2 | ~spl108_4 | ~spl108_5, inference(sat_conversion,[],[f2565])).
% 0.23/0.36 cnf(s52, plain, spl108_32, inference(rat,[],[s39,s40,s45])).
% 0.23/0.36 cnf(s53, plain, spl108_3, inference(rat,[],[s50,s52])).
% 0.23/0.36 cnf(s57, plain, spl108_21, inference(rat,[],[s16,s41,s43])).
% 0.23/0.36 cnf(s58, plain, spl108_1, inference(rat,[],[s49,s57])).
% 0.23/0.36 cnf(s63, plain, spl108_5, inference(rat,[],[s3,s53])).
% 0.23/0.36 cnf(s64, plain, spl108_4, inference(rat,[],[s2,s53])).
% 0.23/0.36 cnf(s65, plain, ~spl108_2, inference(rat,[],[s51,s63,s64])).
% 0.23/0.36 cnf(s66, plain, $false, inference(rat,[],[s1,s65,s58])).
% 0.23/0.36 tff(f2566,plain,(
% 0.23/0.36 $false),
% 0.23/0.36 inference(avatar_sat_refutation,[],[s66])).
% 0.23/0.36 % SZS output end Proof for theBenchmark
% 0.23/0.36 % (672998)------------------------------
% 0.23/0.36 % (672998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.36 % (672998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.36 % (672998)CaDiCaL version: 2.1.3
% 0.23/0.36 % (672998)Termination reason: Refutation
% 0.23/0.36 % (672998)Time elapsed: 0.050 s
% 0.23/0.36 % (672998)Peak memory usage: 15 MB
% 0.23/0.36 % (672998)Instructions burned: 88 (million)
% 0.23/0.36 % (672992)Success in time 0.089 s
% 0.23/0.36 % Vampire exiting
%------------------------------------------------------------------------------