%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC524_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 : n007.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.35s 0.32s
% Output : Refutation 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC524_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.17 % Computer : n007.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Mon Sep 28 09:39:41 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.21 Running first-order model finding
% 0.06/0.21 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.35/0.32 % (2276708)Will run a generic schedule for satisfiability detection.
% 0.35/0.32 % (2276724)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=737459829:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.35/0.32 % (2276720)% WARNING: option uhcvi not known.
% 0.35/0.32 % (2276719)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4288010872_2999 on theBenchmark for (2999ds/0Mi)
% 0.35/0.32 % (2276723)dis+10_1_sil=32000:sp=arity:random_seed=1206460820:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.35/0.32 % (2276721)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3542849855:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.35/0.32 % (2276725)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3940768095:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.35/0.32 % (2276726)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2825608633:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.35/0.32 % (2276720)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3105225795:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.35/0.32 % (2276719)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.35/0.32 % (2276719)Terminated due to inappropriate strategy.
% 0.35/0.32 % (2276719)------------------------------
% 0.35/0.32 % (2276719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.35/0.32 % (2276719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/0.32 % (2276719)CaDiCaL version: 2.1.3
% 0.35/0.32 % (2276719)Termination reason: Inappropriate
% 0.35/0.32 % (2276719)Time elapsed: 0.012 s
% 0.35/0.32 % (2276719)Peak memory usage: 11 MB
% 0.35/0.32 % (2276719)Instructions burned: 24 (million)
% 0.35/0.32 % (2276719)------------------------------
% 0.35/0.32 % (2276719)------------------------------
% 0.35/0.32 % (2276724)Instruction limit reached!
% 0.35/0.32 % (2276724)------------------------------
% 0.35/0.32 % (2276724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.35/0.32 % (2276724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/0.32 % (2276724)CaDiCaL version: 2.1.3
% 0.35/0.32 % (2276724)Termination reason: Instruction limit
% 0.35/0.32 % (2276724)Termination phase: Saturation
% 0.35/0.32 % (2276724)Time elapsed: 0.034 s
% 0.35/0.32 % (2276724)Peak memory usage: 14 MB
% 0.35/0.32 % (2276724)Instructions burned: 119 (million)
% 0.35/0.32 % (2276735)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3452795575:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.35/0.32 % (2276736)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2944589608:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.35/0.32 % (2276735)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.35/0.32 % (2276735)Terminated due to inappropriate strategy.
% 0.35/0.32 % (2276735)------------------------------
% 0.35/0.32 % (2276735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.35/0.32 % (2276735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/0.32 % (2276735)CaDiCaL version: 2.1.3
% 0.35/0.32 % (2276735)Termination reason: Inappropriate
% 0.35/0.32 % (2276735)Time elapsed: 0.010 s
% 0.35/0.32 % (2276735)Peak memory usage: 11 MB
% 0.35/0.32 % (2276735)Instructions burned: 20 (million)
% 0.35/0.32 % (2276735)------------------------------
% 0.35/0.32 % (2276735)------------------------------
% 0.35/0.32 % (2276723)Instruction limit reached!
% 0.35/0.32 % (2276723)------------------------------
% 0.35/0.32 % (2276723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.35/0.32 % (2276723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/0.32 % (2276723)CaDiCaL version: 2.1.3
% 0.35/0.32 % (2276723)Termination reason: Instruction limit
% 0.35/0.32 % (2276723)Termination phase: Saturation
% 0.35/0.32 % (2276723)Time elapsed: 0.058 s
% 0.35/0.32 % (2276723)Peak memory usage: 14 MB
% 0.35/0.32 % (2276723)Instructions burned: 103 (million)
% 0.35/0.32 % (2276725) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2276708-2276725"...
% 0.35/0.32 % (2276739)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4169382279:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.35/0.32 % (2276725)...printing done.
% 0.35/0.32 % (2276725)Refutation found. Thanks to Tanya!
% 0.35/0.32 % SZS status Theorem for theBenchmark
% 0.35/0.32 % SZS output start Proof for theBenchmark
% 0.35/0.32 tff(type_def_5, type, set_0: $tType).
% 0.35/0.32 tff(type_def_6, type, set_2: $tType).
% 0.35/0.32 tff(type_def_7, type, set_3: $tType).
% 0.35/0.32 tff(type_def_8, type, set_4: $tType).
% 0.35/0.32 tff(func_def_0, type, min_int: $int).
% 0.35/0.32 tff(func_def_1, type, max_int: $int).
% 0.35/0.32 tff(func_def_5, type, g_s0_0: set_0).
% 0.35/0.32 tff(func_def_6, type, g_s1_1: $int).
% 0.35/0.32 tff(func_def_7, type, g_s2_2: $int).
% 0.35/0.32 tff(func_def_8, type, g_s3_3: set_0).
% 0.35/0.32 tff(func_def_9, type, g_s4_4: $int).
% 0.35/0.32 tff(func_def_10, type, g_s5_5: $int).
% 0.35/0.32 tff(func_def_11, type, g_s6_6: set_0).
% 0.35/0.32 tff(func_def_12, type, g_s7_7: $int).
% 0.35/0.32 tff(func_def_13, type, g_s8_8: $int).
% 0.35/0.32 tff(func_def_14, type, g_s9_9: set_0).
% 0.35/0.32 tff(func_def_15, type, g_s10_10: $int).
% 0.35/0.32 tff(func_def_16, type, g_s11_11: $int).
% 0.35/0.32 tff(func_def_17, type, g_s12_12: $int).
% 0.35/0.32 tff(func_def_18, type, g_s13_13: $int).
% 0.35/0.32 tff(func_def_19, type, g_s14_14: $int).
% 0.35/0.32 tff(func_def_20, type, g_s15_15: $int).
% 0.35/0.32 tff(func_def_21, type, g_s16_16: $int).
% 0.35/0.32 tff(func_def_22, type, g_s17_17: $int).
% 0.35/0.32 tff(func_def_23, type, g_s18_18: $int).
% 0.35/0.32 tff(func_def_24, type, g_s19_19: set_0).
% 0.35/0.32 tff(func_def_25, type, g_s20_20: $int).
% 0.35/0.32 tff(func_def_26, type, g_s21_21: $int).
% 0.35/0.32 tff(func_def_27, type, g_s22_22: set_0).
% 0.35/0.32 tff(func_def_28, type, g_s23_23: $int).
% 0.35/0.32 tff(func_def_29, type, g_s24_24: $int).
% 0.35/0.32 tff(func_def_30, type, g_s25_25: $int).
% 0.35/0.32 tff(func_def_31, type, g_s26_26: $int).
% 0.35/0.32 tff(func_def_32, type, g_s27_27: $int).
% 0.35/0.32 tff(func_def_33, type, g_s28_28: $int).
% 0.35/0.32 tff(func_def_34, type, g_s29_29: $int).
% 0.35/0.32 tff(func_def_35, type, g_s30_30: $int).
% 0.35/0.32 tff(func_def_36, type, g_s31_31: $int).
% 0.35/0.32 tff(func_def_37, type, g_s33_32: set_0).
% 0.35/0.32 tff(func_def_38, type, g_s32_33: $int).
% 0.35/0.32 tff(func_def_39, type, g_s35_34: set_0).
% 0.35/0.32 tff(func_def_40, type, g_s34_35: $int).
% 0.35/0.32 tff(func_def_41, type, g_s37_36: set_0).
% 0.35/0.32 tff(func_def_42, type, g_s36_37: $int).
% 0.35/0.32 tff(func_def_43, type, g_s38_38: $int).
% 0.35/0.32 tff(func_def_44, type, g_s39_39: $int).
% 0.35/0.32 tff(func_def_45, type, g_s40_40: set_0).
% 0.35/0.32 tff(func_def_46, type, set_2_empty: set_2).
% 0.35/0.32 tff(func_def_47, type, set_2_insert: set_2 > set_2).
% 0.35/0.32 tff(func_def_48, type, g_s41_41: set_2).
% 0.35/0.32 tff(func_def_49, type, g_s42_42: $int).
% 0.35/0.32 tff(func_def_50, type, g_s43_43: $int).
% 0.35/0.32 tff(func_def_51, type, g_s44_44: $int).
% 0.35/0.32 tff(func_def_52, type, g_s45_45: $int).
% 0.35/0.32 tff(func_def_53, type, g_s46_46: $int).
% 0.35/0.32 tff(func_def_54, type, g_s47_47: $int).
% 0.35/0.32 tff(func_def_55, type, g_s48_48: $int).
% 0.35/0.32 tff(func_def_56, type, g_s49_49: $int).
% 0.35/0.32 tff(func_def_57, type, g_s50_50: $int).
% 0.35/0.32 tff(func_def_58, type, g_s51_51: $int).
% 0.35/0.32 tff(func_def_59, type, g_s52_52: $int).
% 0.35/0.32 tff(func_def_60, type, g_s53_53: $int).
% 0.35/0.32 tff(func_def_61, type, g_s54_54: $int).
% 0.35/0.32 tff(func_def_62, type, g_s55_55: $int).
% 0.35/0.32 tff(func_def_63, type, g_s56_56: $int).
% 0.35/0.32 tff(func_def_64, type, g_s57_57: $int).
% 0.35/0.32 tff(func_def_65, type, g_s58_58: $int).
% 0.35/0.32 tff(func_def_66, type, g_s59_59: $int).
% 0.35/0.32 tff(func_def_67, type, g_s60_60: $int).
% 0.35/0.32 tff(func_def_68, type, g_s61_61: $int).
% 0.35/0.32 tff(func_def_69, type, g_s62_62: $int).
% 0.35/0.32 tff(func_def_70, type, g_s63_63: $int).
% 0.35/0.32 tff(func_def_71, type, g_s64_64: $int).
% 0.35/0.32 tff(func_def_72, type, g_s65_65: $int).
% 0.35/0.32 tff(func_def_73, type, g_s66_66: $int).
% 0.35/0.32 tff(func_def_74, type, g_s67_67: $int).
% 0.35/0.32 tff(func_def_75, type, g_s68_68: $int).
% 0.35/0.32 tff(func_def_76, type, g_s69_69: $int).
% 0.35/0.32 tff(func_def_77, type, g_s70_70: $int).
% 0.35/0.32 tff(func_def_78, type, g_s71_71: $int).
% 0.35/0.32 tff(func_def_79, type, g_s72_72: $int).
% 0.35/0.32 tff(func_def_80, type, g_s73_73: $int).
% 0.35/0.32 tff(func_def_81, type, g_s74_74: $int).
% 0.35/0.32 tff(func_def_82, type, g_s75_75: $int).
% 0.35/0.32 tff(func_def_83, type, g_s76_76: $int).
% 0.35/0.32 tff(func_def_84, type, g_s77_77: $int).
% 0.35/0.32 tff(func_def_85, type, g_s78_78: $int).
% 0.35/0.32 tff(func_def_86, type, g_s79_79: $int).
% 0.35/0.32 tff(func_def_87, type, g_s80_80: $int).
% 0.35/0.32 tff(func_def_88, type, g_s81_81: $int).
% 0.35/0.32 tff(func_def_89, type, g_s82_82: $int).
% 0.35/0.32 tff(func_def_90, type, g_s83_83: $int).
% 0.35/0.32 tff(func_def_91, type, g_s84_84: $int).
% 0.35/0.32 tff(func_def_92, type, g_s85_85: $int).
% 0.35/0.32 tff(func_def_93, type, g_s86_86: $int).
% 0.35/0.32 tff(func_def_94, type, g_s87_87: $int).
% 0.35/0.32 tff(func_def_95, type, g_s88_88: $int).
% 0.35/0.32 tff(func_def_96, type, g_s89_89: $int).
% 0.35/0.32 tff(func_def_97, type, g_s90_90: $int).
% 0.35/0.32 tff(func_def_98, type, g_s91_91: $int).
% 0.35/0.32 tff(func_def_99, type, g_s92_92: $int).
% 0.35/0.32 tff(func_def_100, type, g_s93_93: $int).
% 0.35/0.32 tff(func_def_101, type, g_s94_94: $int).
% 0.35/0.32 tff(func_def_102, type, g_s95_95: $int).
% 0.35/0.32 tff(func_def_103, type, g_s96_96: $int).
% 0.35/0.32 tff(func_def_104, type, g_s97_97: $int).
% 0.35/0.32 tff(func_def_105, type, g_s98_98: $int).
% 0.35/0.32 tff(func_def_106, type, g_s99_99: $int).
% 0.35/0.32 tff(func_def_107, type, g_s100_100: $int).
% 0.35/0.32 tff(func_def_108, type, g_s101_101: $int).
% 0.35/0.32 tff(func_def_109, type, g_s102_102: $int).
% 0.35/0.32 tff(func_def_110, type, g_s103_103: $int).
% 0.35/0.32 tff(func_def_111, type, g_s104_104: $int).
% 0.35/0.32 tff(func_def_112, type, g_s105_105: $int).
% 0.35/0.32 tff(func_def_113, type, g_s106_106: $int).
% 0.35/0.32 tff(func_def_114, type, g_s107_107: $int).
% 0.35/0.32 tff(func_def_115, type, g_s108_108: $int).
% 0.35/0.32 tff(func_def_116, type, g_s109_109: $int).
% 0.35/0.32 tff(func_def_117, type, g_s110_110: $int).
% 0.35/0.32 tff(func_def_118, type, g_s111_111: $int).
% 0.35/0.32 tff(func_def_119, type, g_s112_112: $int).
% 0.35/0.32 tff(func_def_120, type, g_s113_113: $int).
% 0.35/0.32 tff(func_def_121, type, g_s114_114: $int).
% 0.35/0.32 tff(func_def_122, type, g_s115_115: $int).
% 0.35/0.32 tff(func_def_123, type, g_s116_116: $int).
% 0.35/0.32 tff(func_def_124, type, g_s117_117: $int).
% 0.35/0.32 tff(func_def_125, type, g_s118_118: $int).
% 0.35/0.32 tff(func_def_126, type, g_s119_119: $int).
% 0.35/0.32 tff(func_def_127, type, g_s120_120: $int).
% 0.35/0.32 tff(func_def_128, type, g_s121_121: $int).
% 0.35/0.32 tff(func_def_129, type, g_s122_122: $int).
% 0.35/0.32 tff(func_def_130, type, g_s123_123: $int).
% 0.35/0.32 tff(func_def_131, type, g_s124_124: $int).
% 0.35/0.32 tff(func_def_132, type, g_s125_125: $int).
% 0.35/0.32 tff(func_def_133, type, g_s126_126: $int).
% 0.35/0.32 tff(func_def_134, type, g_s127_127: $int).
% 0.35/0.32 tff(func_def_135, type, g_s128_128: $int).
% 0.35/0.32 tff(func_def_136, type, g_s129_129: $int).
% 0.35/0.32 tff(func_def_137, type, g_s130_130: $int).
% 0.35/0.32 tff(func_def_138, type, g_s131_131: $int).
% 0.35/0.32 tff(func_def_139, type, g_s132_132: $int).
% 0.35/0.32 tff(func_def_140, type, g_s133_133: $int).
% 0.35/0.32 tff(func_def_141, type, g_s134_134: $int).
% 0.35/0.32 tff(func_def_142, type, g_s135_135: $int).
% 0.35/0.32 tff(func_def_143, type, g_s136_136: $int).
% 0.35/0.32 tff(func_def_144, type, g_s137_137: $int).
% 0.35/0.32 tff(func_def_145, type, g_s138_138: $int).
% 0.35/0.32 tff(func_def_146, type, g_s139_139: $int).
% 0.35/0.32 tff(func_def_147, type, g_s140_140: $int).
% 0.35/0.32 tff(func_def_148, type, g_s141_141: $int).
% 0.35/0.32 tff(func_def_149, type, g_s142_142: $int).
% 0.35/0.32 tff(func_def_150, type, g_s143_143: $int).
% 0.35/0.32 tff(func_def_151, type, g_s144_144: $int).
% 0.35/0.32 tff(func_def_152, type, g_s145_145: $int).
% 0.35/0.32 tff(func_def_153, type, g_s146_146: $int).
% 0.35/0.32 tff(func_def_154, type, g_s147_147: $int).
% 0.35/0.32 tff(func_def_155, type, g_s148_148: $int).
% 0.35/0.32 tff(func_def_156, type, g_s149_149: $int).
% 0.35/0.32 tff(func_def_157, type, g_s150_150: $int).
% 0.35/0.32 tff(func_def_158, type, g_s151_151: $int).
% 0.35/0.32 tff(func_def_159, type, g_s152_152: $int).
% 0.35/0.32 tff(func_def_160, type, g_s153_153: $int).
% 0.35/0.32 tff(func_def_161, type, g_s154_154: $int).
% 0.35/0.32 tff(func_def_162, type, g_s155_155: $int).
% 0.35/0.32 tff(func_def_163, type, g_s156_156: $int).
% 0.35/0.32 tff(func_def_164, type, g_s157_157: $int).
% 0.35/0.32 tff(func_def_165, type, g_s158_158: $int).
% 0.35/0.32 tff(func_def_166, type, g_s159_159: $int).
% 0.35/0.32 tff(func_def_167, type, g_s160_160: $int).
% 0.35/0.32 tff(func_def_168, type, g_s161_161: set_0).
% 0.35/0.32 tff(func_def_169, type, g_s162_162: set_0).
% 0.35/0.32 tff(func_def_170, type, g_s163_163: $int).
% 0.35/0.32 tff(func_def_171, type, g_s164_164: $int).
% 0.35/0.32 tff(func_def_172, type, g_s165_165: $int).
% 0.35/0.32 tff(func_def_173, type, g_s166_166: $int).
% 0.35/0.32 tff(func_def_174, type, g_s167_167: $int).
% 0.35/0.32 tff(func_def_175, type, g_s168_168: $int).
% 0.35/0.32 tff(func_def_176, type, g_s169_169: $int).
% 0.35/0.32 tff(func_def_177, type, g_s170_170: $int).
% 0.35/0.32 tff(func_def_178, type, g_s171_171: $int).
% 0.35/0.32 tff(func_def_179, type, g_s172_172: $int).
% 0.35/0.32 tff(func_def_180, type, g_s173_173: $int).
% 0.35/0.32 tff(func_def_181, type, g_s174_174: $int).
% 0.35/0.32 tff(func_def_182, type, g_s175_175: $int).
% 0.35/0.32 tff(func_def_183, type, g_s176_176: $int).
% 0.35/0.32 tff(func_def_184, type, g_s177_177: $int).
% 0.35/0.32 tff(func_def_185, type, g_s178_178: $int).
% 0.35/0.32 tff(func_def_186, type, g_s179_179: $int).
% 0.35/0.32 tff(func_def_187, type, g_s180_180: $int).
% 0.35/0.32 tff(func_def_188, type, g_s181_181: $int).
% 0.35/0.32 tff(func_def_189, type, g_s182_182: $int).
% 0.35/0.32 tff(func_def_190, type, g_s183_183: $int).
% 0.35/0.32 tff(func_def_191, type, g_s184_184: $int).
% 0.35/0.32 tff(func_def_192, type, g_s185_185: $int).
% 0.35/0.32 tff(func_def_193, type, g_s186_186: $int).
% 0.35/0.32 tff(func_def_194, type, g_s187_187: $int).
% 0.35/0.32 tff(func_def_195, type, g_s188_188: $int).
% 0.35/0.32 tff(func_def_196, type, g_s189_189: $int).
% 0.35/0.32 tff(func_def_197, type, g_s190_190: $int).
% 0.35/0.32 tff(func_def_198, type, g_s191_191: $int).
% 0.35/0.32 tff(func_def_199, type, g_s192_192: $int).
% 0.35/0.32 tff(func_def_200, type, g_s193_193: $int).
% 0.35/0.32 tff(func_def_201, type, g_s194_194: $int).
% 0.35/0.32 tff(func_def_202, type, g_s195_195: $int).
% 0.35/0.32 tff(func_def_203, type, g_s196_196: $int).
% 0.35/0.32 tff(func_def_204, type, g_s197_197: $int).
% 0.35/0.32 tff(func_def_205, type, g_s198_198: $int).
% 0.35/0.32 tff(func_def_206, type, g_s199_199: $int).
% 0.35/0.32 tff(func_def_207, type, g_s200_200: $int).
% 0.35/0.32 tff(func_def_208, type, g_s201_201: $int).
% 0.35/0.32 tff(func_def_209, type, g_s202_202: $int).
% 0.35/0.32 tff(func_def_210, type, g_s203_203: $int).
% 0.35/0.32 tff(func_def_211, type, g_s204_204: $int).
% 0.35/0.32 tff(func_def_212, type, g_s205_205: $int).
% 0.35/0.32 tff(func_def_213, type, g_s206_206: $int).
% 0.35/0.32 tff(func_def_214, type, g_s207_207: $int).
% 0.35/0.32 tff(func_def_215, type, g_s208_208: $int).
% 0.35/0.32 tff(func_def_216, type, g_s209_209: $int).
% 0.35/0.32 tff(func_def_217, type, g_s210_210: $int).
% 0.35/0.32 tff(func_def_218, type, g_s211_211: $int).
% 0.35/0.32 tff(func_def_219, type, g_s212_212: $int).
% 0.35/0.32 tff(func_def_220, type, g_s213_213: $int).
% 0.35/0.32 tff(func_def_221, type, g_s214_214: $int).
% 0.35/0.32 tff(func_def_222, type, g_s215_215: $int).
% 0.35/0.32 tff(func_def_223, type, g_s216_216: $int).
% 0.35/0.32 tff(func_def_224, type, g_s217_217: $int).
% 0.35/0.32 tff(func_def_225, type, g_s218_218: $int).
% 0.35/0.32 tff(func_def_226, type, g_s219_219: $int).
% 0.35/0.32 tff(func_def_227, type, g_s220_220: $int).
% 0.35/0.32 tff(func_def_228, type, g_s221_221: $int).
% 0.35/0.32 tff(func_def_229, type, g_s222_222: $int).
% 0.35/0.32 tff(func_def_230, type, g_s223_223: $int).
% 0.35/0.32 tff(func_def_231, type, g_s224_224: $int).
% 0.35/0.32 tff(func_def_232, type, g_s225_225: $int).
% 0.35/0.32 tff(func_def_233, type, g_s226_226: $int).
% 0.35/0.32 tff(func_def_234, type, g_s227_227: $int).
% 0.35/0.32 tff(func_def_235, type, g_s228_228: $int).
% 0.35/0.32 tff(func_def_236, type, g_s229_229: $int).
% 0.35/0.32 tff(func_def_237, type, g_s230_230: $int).
% 0.35/0.32 tff(func_def_238, type, g_s231_231: $int).
% 0.35/0.32 tff(func_def_239, type, g_s232_232: $int).
% 0.35/0.32 tff(func_def_240, type, g_s233_233: $int).
% 0.35/0.32 tff(func_def_241, type, g_s234_234: $int).
% 0.35/0.32 tff(func_def_242, type, g_s235_235: $int).
% 0.35/0.32 tff(func_def_243, type, g_s236_236: $int).
% 0.35/0.32 tff(func_def_244, type, g_s237_237: $int).
% 0.35/0.32 tff(func_def_245, type, g_s238_238: $int).
% 0.35/0.32 tff(func_def_246, type, g_s239_239: $int).
% 0.35/0.32 tff(func_def_247, type, g_s240_240: $int).
% 0.35/0.32 tff(func_def_248, type, g_s241_241: $int).
% 0.35/0.32 tff(func_def_249, type, g_s242_242: $int).
% 0.35/0.32 tff(func_def_250, type, g_s243_243: $int).
% 0.35/0.32 tff(func_def_251, type, g_s244_244: $int).
% 0.35/0.32 tff(func_def_252, type, g_s245_245: $int).
% 0.35/0.32 tff(func_def_253, type, g_s246_246: $int).
% 0.35/0.32 tff(func_def_254, type, g_s247_247: $int).
% 0.35/0.32 tff(func_def_255, type, g_s248_248: $int).
% 0.35/0.32 tff(func_def_256, type, g_s249_249: $int).
% 0.35/0.32 tff(func_def_257, type, g_s250_250: $int).
% 0.35/0.32 tff(func_def_258, type, g_s251_251: $int).
% 0.35/0.32 tff(func_def_259, type, g_s252_252: $int).
% 0.35/0.32 tff(func_def_260, type, g_s253_253: $int).
% 0.35/0.32 tff(func_def_261, type, g_s254_254: $int).
% 0.35/0.32 tff(func_def_262, type, g_s255_255: $int).
% 0.35/0.32 tff(func_def_263, type, g_s256_256: $int).
% 0.35/0.32 tff(func_def_264, type, g_s257_257: $int).
% 0.35/0.32 tff(func_def_265, type, g_s258_258: $int).
% 0.35/0.32 tff(func_def_266, type, g_s259_259: $int).
% 0.35/0.32 tff(func_def_267, type, g_s260_260: $int).
% 0.35/0.32 tff(func_def_268, type, g_s261_261: $int).
% 0.35/0.32 tff(func_def_269, type, g_s262_262: $int).
% 0.35/0.32 tff(func_def_270, type, g_s263_263: $int).
% 0.35/0.32 tff(func_def_271, type, g_s264_264: $int).
% 0.35/0.32 tff(func_def_272, type, g_s265_265: $int).
% 0.35/0.32 tff(func_def_273, type, g_s266_266: $int).
% 0.35/0.32 tff(func_def_274, type, g_s267_267: $int).
% 0.35/0.32 tff(func_def_275, type, g_s268_268: $int).
% 0.35/0.32 tff(func_def_276, type, g_s269_269: $int).
% 0.35/0.32 tff(func_def_277, type, g_s270_270: $int).
% 0.35/0.32 tff(func_def_278, type, g_s271_271: $int).
% 0.35/0.32 tff(func_def_279, type, g_s272_272: $int).
% 0.35/0.32 tff(func_def_280, type, g_s273_273: $int).
% 0.35/0.32 tff(func_def_281, type, g_s274_274: $int).
% 0.35/0.32 tff(func_def_282, type, g_s275_275: $int).
% 0.35/0.32 tff(func_def_283, type, g_s276_276: $int).
% 0.35/0.32 tff(func_def_284, type, set_3_empty: set_3).
% 0.35/0.32 tff(func_def_285, type, set_3_insert: set_3 > set_3).
% 0.35/0.32 tff(func_def_286, type, g_s277_277: set_3).
% 0.35/0.32 tff(func_def_287, type, set_4_empty: set_4).
% 0.35/0.32 tff(func_def_288, type, set_4_insert: set_4 > set_4).
% 0.35/0.32 tff(func_def_289, type, g_s278_278: set_4).
% 0.35/0.32 tff(func_def_290, type, g_s279_279: set_3).
% 0.35/0.32 tff(func_def_291, type, g_s280_280: set_4).
% 0.35/0.32 tff(func_def_292, type, g_s281_281: set_3).
% 0.35/0.32 tff(func_def_293, type, g_s282_282: set_0).
% 0.35/0.32 tff(func_def_294, type, g_s283_283: set_0).
% 0.35/0.32 tff(func_def_295, type, g_s284_284: set_0).
% 0.35/0.32 tff(func_def_296, type, g_s285_285: set_0).
% 0.35/0.32 tff(func_def_297, type, g_s286_286: set_4).
% 0.35/0.32 tff(func_def_298, type, g_s287_287: set_4).
% 0.35/0.32 tff(func_def_299, type, g_s288_288: set_4).
% 0.35/0.32 tff(func_def_300, type, g_s289_289: set_4).
% 0.35/0.32 tff(func_def_301, type, g_s290_290: set_0).
% 0.35/0.32 tff(func_def_302, type, g_s291_291: set_0).
% 0.35/0.32 tff(func_def_303, type, g_s292_292: set_0).
% 0.35/0.32 tff(func_def_304, type, g_s293_293: set_0).
% 0.35/0.32 tff(func_def_305, type, g_s294_294: set_4).
% 0.35/0.32 tff(func_def_306, type, g_s295_295: set_4).
% 0.35/0.32 tff(func_def_307, type, g_s296_296: set_0).
% 0.35/0.32 tff(func_def_308, type, g_s297_297: set_4).
% 0.35/0.32 tff(func_def_309, type, g_s298_298: $int).
% 0.35/0.32 tff(func_def_310, type, g_s299_299: $int).
% 0.35/0.32 tff(func_def_311, type, g_s302_300: $int).
% 0.35/0.32 tff(func_def_312, type, g_s305_301: $int).
% 0.35/0.32 tff(func_def_313, type, g_s306_302: set_4).
% 0.35/0.32 tff(func_def_314, type, g_s307_303: set_4).
% 0.35/0.32 tff(func_def_315, type, g_s308_304: set_4).
% 0.35/0.32 tff(func_def_316, type, g_s299_1_313: $int).
% 0.35/0.32 tff(func_def_317, type, g_s302_1_314: $int).
% 0.35/0.32 tff(func_def_318, type, g_s305_1_315: $int).
% 0.35/0.32 tff(func_def_319, type, g_s309_1_316: $int).
% 0.35/0.32 tff(func_def_320, type, g_s311_1_317: $int).
% 0.35/0.32 tff(func_def_321, type, g_s310_1_318: $int).
% 0.35/0.32 tff(func_def_322, type, g_s312_1_319: $int).
% 0.35/0.32 tff(func_def_323, type, g_s314_1_320: $int).
% 0.35/0.32 tff(func_def_324, type, g_s313_1_321: $int).
% 0.35/0.32 tff(func_def_337, type, bG0: $o > $o).
% 0.35/0.32 tff(func_def_338, type, bG1: $o > $o).
% 0.35/0.32 tff(func_def_339, type, bG2: $o > $o).
% 0.35/0.32 tff(func_def_340, type, bG3: $o > $o).
% 0.35/0.32 tff(func_def_341, type, bG4: $o > $o).
% 0.35/0.32 tff(func_def_342, type, bG5: $o > $o).
% 0.35/0.32 tff(func_def_343, type, bG6: $o > $o).
% 0.35/0.32 tff(func_def_344, type, bG7: $o > $o).
% 0.35/0.32 tff(func_def_345, type, bG8: $o > $o).
% 0.35/0.32 tff(func_def_346, type, bG9: $o > $o).
% 0.35/0.32 tff(func_def_347, type, sK11: $int > $int).
% 0.35/0.32 tff(func_def_348, type, sK12: $int > $int).
% 0.35/0.32 tff(func_def_349, type, sK13: $int > $int).
% 0.35/0.32 tff(func_def_350, type, sK14: set_3).
% 0.35/0.32 tff(func_def_351, type, sK15: ($int * $int) > $int).
% 0.35/0.32 tff(func_def_352, type, sK16: ($int * $int) > $int).
% 0.35/0.32 tff(func_def_353, type, sK17: set_3).
% 0.35/0.32 tff(func_def_354, type, sK18: ($int * $int) > $int).
% 0.35/0.32 tff(func_def_355, type, sK19: set_3).
% 0.35/0.32 tff(func_def_356, type, sK20: ($int * $int) > $int).
% 0.35/0.32 tff(func_def_357, type, sK21: ($int * $int) > $int).
% 0.35/0.32 tff(func_def_358, type, sK22: $int).
% 0.35/0.32 tff(func_def_359, type, sK23: $int).
% 0.35/0.32 tff(func_def_360, type, sK24: $int).
% 0.35/0.32 tff(func_def_361, type, sK25: $int).
% 0.35/0.32 tff(func_def_362, type, sK26: $int).
% 0.35/0.32 tff(func_def_363, type, sK27: $int).
% 0.35/0.32 tff(func_def_364, type, sK28: set_4).
% 0.35/0.32 tff(func_def_365, type, sK29: $int > $int).
% 0.35/0.32 tff(func_def_366, type, sK30: set_4).
% 0.35/0.32 tff(func_def_367, type, sK31: $int > $int).
% 0.35/0.32 tff(func_def_368, type, sK32: set_4).
% 0.35/0.32 tff(func_def_369, type, sK33: $int > $int).
% 0.35/0.32 tff(func_def_370, type, sK34: set_4).
% 0.35/0.32 tff(func_def_371, type, sK35: $int > $int).
% 0.35/0.32 tff(func_def_372, type, sK36: set_4).
% 0.35/0.32 tff(func_def_373, type, sK37: $int > $int).
% 0.35/0.32 tff(pred_def_1, type, mem0: ($int * set_0) > $o).
% 0.35/0.32 tff(pred_def_2, type, mem2: ($o * $int * set_2) > $o).
% 0.35/0.32 tff(pred_def_3, type, mem3: ($int * $int * $int * set_3) > $o).
% 0.35/0.32 tff(pred_def_4, type, mem4: ($int * $int * set_4) > $o).
% 0.35/0.32 tff(pred_def_17, type, sP10: $int > $o).
% 0.35/0.32 tff(f151,axiom,(
% 0.35/0.32 $greatereq(g_s180_180,1)),
% 0.35/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:ctx:216')).
% 0.35/0.32 tff(f434,axiom,(
% 0.35/0.32 g_s302_300 = g_s302_1_314),
% 0.35/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:inv:5')).
% 0.35/0.32 tff(f460,axiom,(
% 0.35/0.32 mem4(g_s298_298,g_s302_300,g_s307_303)),
% 0.35/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gh_2_def)).
% 0.35/0.32 tff(f462,axiom,(
% 0.35/0.32 g_s302_1_314 = g_s102_102),
% 0.35/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Local_Hyp:0')).
% 0.35/0.32 tff(f463,conjecture,(
% 0.35/0.32 ~ ! [X0 : $int] : (((X0 = $difference(g_s102_102,1) | X0 = g_s102_102) & ? [X1 : $int] : ($greatereq(X1,$sum($difference(g_s298_298,g_s180_180),1)) & $lesseq(X1,g_s298_298) & mem4(X1,X0,g_s307_303))) <=> $false)),
% 0.35/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Goal')).
% 0.35/0.32 tff(f464,negated_conjecture,(
% 0.35/0.32 ~ ~ ! [X0 : $int] : (((X0 = $difference(g_s102_102,1) | X0 = g_s102_102) & ? [X1 : $int] : ($greatereq(X1,$sum($difference(g_s298_298,g_s180_180),1)) & $lesseq(X1,g_s298_298) & mem4(X1,X0,g_s307_303))) <=> $false)),
% 0.35/0.32 inference(negated_conjecture,[status(cth)],[f463])).
% 0.35/0.32 tff(f509,plain,(
% 0.35/0.32 ~$less(g_s180_180,1)),
% 0.35/0.32 inference(theory_normalization,[],[f151])).
% 0.35/0.32 tff(f623,plain,(
% 0.35/0.32 ! [X0 : $int] : ((($sum(g_s102_102,$uminus(1)) = X0 | X0 = g_s102_102) & ? [X1 : $int] : (~$less(X1,$sum($sum(g_s298_298,$uminus(g_s180_180)),1)) & ~$less(g_s298_298,X1) & mem4(X1,X0,g_s307_303))) <=> $false)),
% 0.35/0.32 inference(theory_normalization,[],[f464])).
% 0.35/0.32 tff(f624,definition,(
% 0.35/0.32 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 0.35/0.32 introduced(theory,[tha_commutativity])).
% 0.35/0.32 tff(f625,definition,(
% 0.35/0.32 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 0.35/0.32 introduced(theory,[tha_associativity])).
% 0.35/0.32 tff(f628,definition,(
% 0.35/0.32 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 0.35/0.32 introduced(theory,[tha_inverse_op_unit])).
% 0.35/0.32 tff(f629,definition,(
% 0.35/0.32 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 0.35/0.32 introduced(theory,[tha_non-reflexivity])).
% 0.35/0.32 tff(f632,definition,(
% 0.35/0.32 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less($sum(X0,X2),$sum(X1,X2))) )),
% 0.35/0.32 introduced(theory,[tha_order_monotonicity])).
% 0.35/0.32 tff(f677,plain,(
% 0.35/0.32 ! [X0 : $int] : ~(($sum(g_s102_102,$uminus(1)) = X0 | X0 = g_s102_102) & ? [X1 : $int] : (~$less(X1,$sum($sum(g_s298_298,$uminus(g_s180_180)),1)) & ~$less(g_s298_298,X1) & mem4(X1,X0,g_s307_303)))),
% 0.35/0.32 inference(true_and_false_elimination,[],[f623])).
% 0.35/0.32 tff(f736,plain,(
% 0.35/0.32 ! [X0 : $int] : (($sum(g_s102_102,$uminus(1)) != X0 & g_s102_102 != X0) | ! [X1 : $int] : ($less(X1,$sum($sum(g_s298_298,$uminus(g_s180_180)),1)) | $less(g_s298_298,X1) | ~mem4(X1,X0,g_s307_303)))),
% 0.35/0.32 inference(ennf_transformation,[],[f677])).
% 0.35/0.32 tff(f1049,plain,(
% 0.35/0.32 ~$less(g_s180_180,1)),
% 0.35/0.32 inference(cnf_transformation,[],[f509])).
% 0.35/0.32 tff(f1401,plain,(
% 0.35/0.32 g_s302_300 = g_s302_1_314),
% 0.35/0.32 inference(cnf_transformation,[],[f434])).
% 0.35/0.32 tff(f1472,plain,(
% 0.35/0.32 mem4(g_s298_298,g_s302_300,g_s307_303)),
% 0.35/0.32 inference(cnf_transformation,[],[f460])).
% 0.35/0.32 tff(f1474,plain,(
% 0.35/0.32 g_s102_102 = g_s302_1_314),
% 0.35/0.32 inference(cnf_transformation,[],[f462])).
% 0.35/0.32 tff(f1475,plain,(
% 0.35/0.32 ( ! [X0 : $int,X1 : $int] : (g_s102_102 != X0 | $less(X1,$sum($sum(g_s298_298,$uminus(g_s180_180)),1)) | $less(g_s298_298,X1) | ~mem4(X1,X0,g_s307_303)) )),
% 0.35/0.32 inference(cnf_transformation,[],[f736])).
% 0.35/0.32 tff(f1552,plain,(
% 0.35/0.32 mem4(g_s298_298,g_s302_1_314,g_s307_303)),
% 0.35/0.32 inference(definition_unfolding,[],[f1472,f1401])).
% 0.35/0.32 tff(f1555,plain,(
% 0.35/0.32 ( ! [X0 : $int,X1 : $int] : (~mem4(X1,X0,g_s307_303) | $less(X1,$sum($sum(g_s298_298,$uminus(g_s180_180)),1)) | $less(g_s298_298,X1) | g_s302_1_314 != X0) )),
% 0.35/0.32 inference(definition_unfolding,[],[f1475,f1474])).
% 0.35/0.32 tff(f1768,plain,(
% 0.35/0.32 $less(g_s298_298,$sum($sum(g_s298_298,$uminus(g_s180_180)),1)) | $less(g_s298_298,g_s298_298) | g_s302_1_314 != g_s302_1_314),
% 0.35/0.32 inference(resolution,[],[f1552,f1555])).
% 0.35/0.32 tff(f1769,plain,(
% 0.35/0.32 $less(g_s298_298,$sum($sum(g_s298_298,$uminus(g_s180_180)),1)) | $less(g_s298_298,g_s298_298)),
% 0.35/0.32 inference(trivial_inequality_removal,[],[f1768])).
% 0.35/0.32 tff(f1770,plain,(
% 0.35/0.32 $less(g_s298_298,$sum($sum(g_s298_298,$uminus(g_s180_180)),1))),
% 0.35/0.32 inference(forward_subsumption_resolution,[],[f1769,f629])).
% 0.35/0.32 tff(f1772,plain,(
% 0.35/0.32 $less(g_s298_298,$sum(g_s298_298,$sum($uminus(g_s180_180),1)))),
% 0.35/0.32 inference(forward_demodulation,[],[f1770,f625])).
% 0.35/0.32 tff(f1774,plain,(
% 0.35/0.32 $less(g_s298_298,$sum(g_s298_298,$sum(1,$uminus(g_s180_180))))),
% 0.35/0.32 inference(forward_demodulation,[],[f1772,f624])).
% 0.35/0.32 tff(f4655,plain,(
% 0.35/0.32 ( ! [X0 : $int] : ($less($sum(g_s298_298,X0),$sum($sum(g_s298_298,$sum(1,$uminus(g_s180_180))),X0))) )),
% 0.35/0.32 inference(resolution,[],[f632,f1774])).
% 0.35/0.32 tff(f4682,plain,(
% 0.35/0.32 ( ! [X0 : $int] : ($less($sum(g_s298_298,X0),$sum(g_s298_298,$sum($sum(1,$uminus(g_s180_180)),X0)))) )),
% 0.35/0.32 inference(forward_demodulation,[],[f4655,f625])).
% 0.35/0.32 tff(f4696,plain,(
% 0.35/0.32 ( ! [X0 : $int] : ($less($sum(g_s298_298,X0),$sum(g_s298_298,$sum(1,$sum($uminus(g_s180_180),X0))))) )),
% 0.35/0.32 inference(forward_demodulation,[],[f4682,f625])).
% 0.35/0.32 tff(f4738,plain,(
% 0.35/0.32 $less($sum(g_s298_298,$uminus($uminus(g_s180_180))),$sum(g_s298_298,$sum(1,0)))),
% 0.35/0.32 inference(superposition,[],[f4696,f628])).
% 0.35/0.32 tff(f4741,plain,(
% 0.35/0.32 $less($sum(g_s298_298,g_s180_180),$sum(g_s298_298,1))),
% 0.35/0.32 inference(evaluation,[],[f4738])).
% 0.35/0.32 tff(f4743,plain,(
% 0.35/0.32 $less($sum(g_s298_298,g_s180_180),$sum(1,g_s298_298))),
% 0.35/0.32 inference(forward_demodulation,[],[f4741,f624])).
% 0.35/0.32 tff(f4746,plain,(
% 0.35/0.32 $less($sum(g_s180_180,g_s298_298),$sum(1,g_s298_298))),
% 0.35/0.32 inference(forward_demodulation,[],[f4743,f624])).
% 0.35/0.32 tff(f4750,plain,(
% 0.35/0.32 ( ! [X0 : $int] : ($less($sum($sum(g_s180_180,g_s298_298),X0),$sum($sum(1,g_s298_298),X0))) )),
% 0.35/0.32 inference(resolution,[],[f4746,f632])).
% 0.35/0.32 tff(f4754,plain,(
% 0.35/0.32 ( ! [X0 : $int] : ($less($sum($sum(g_s180_180,g_s298_298),X0),$sum(1,$sum(g_s298_298,X0)))) )),
% 0.35/0.32 inference(forward_demodulation,[],[f4750,f625])).
% 0.35/0.32 tff(f4756,plain,(
% 0.35/0.32 ( ! [X0 : $int] : ($less($sum(g_s180_180,$sum(g_s298_298,X0)),$sum(1,$sum(g_s298_298,X0)))) )),
% 0.35/0.32 inference(forward_demodulation,[],[f4754,f625])).
% 0.35/0.32 tff(f4801,plain,(
% 0.35/0.32 $less($sum(g_s180_180,0),$sum(1,0))),
% 0.35/0.32 inference(superposition,[],[f4756,f628])).
% 0.35/0.32 tff(f4803,plain,(
% 0.35/0.32 $less(g_s180_180,1)),
% 0.35/0.32 inference(evaluation,[],[f4801])).
% 0.35/0.32 tff(f4804,plain,(
% 0.35/0.32 $false),
% 0.35/0.32 inference(forward_subsumption_resolution,[],[f4803,f1049])).
% 0.35/0.32 % SZS output end Proof for theBenchmark
% 0.35/0.32 % (2276725)------------------------------
% 0.35/0.32 % (2276725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.35/0.32 % (2276725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/0.32 % (2276725)CaDiCaL version: 2.1.3
% 0.35/0.32 % (2276725)Termination reason: Refutation
% 0.35/0.32 % (2276725)Time elapsed: 0.065 s
% 0.35/0.32 % (2276725)Peak memory usage: 14 MB
% 0.35/0.32 % (2276725)Instructions burned: 119 (million)
% 0.35/0.32 % (2276708)Success in time 0.099 s
% 0.35/0.32 % Vampire exiting
%------------------------------------------------------------------------------