%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW834_1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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:45:02 PM UTC 2026
% Result : Unsatisfiable 0.18s 0.29s
% Output : Refutation 0.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW834_1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.16 % Computer : n016.cluster.edu
% 0.08/0.16 % Model : x86_64 x86_64
% 0.08/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.16 % Memory : 8046.5625MB
% 0.08/0.16 % OS : Linux 6.8.0-71-generic
% 0.08/0.16 % CPULimit : 300
% 0.08/0.16 % WCLimit : 300
% 0.08/0.16 % DateTime : Mon Sep 28 14:36:03 UTC 2026
% 0.08/0.16 % CPUTime :
% 0.08/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 Running first-order model finding
% 0.08/0.19 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.29 % (3671939)Will run a generic schedule for satisfiability detection.
% 0.18/0.29 % (3671944)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3076477916_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.29 % (3671945)% WARNING: option uhcvi not known.
% 0.18/0.29 % (3671945)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2587337542:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.29 % (3671948)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2873582634:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.29 % (3671946)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=72116908:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.29 % (3671947)dis+10_1_sil=32000:sp=arity:random_seed=1100903776:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.29 % (3671944)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.18/0.29 % (3671944)Terminated due to inappropriate strategy.
% 0.18/0.29 % (3671944)------------------------------
% 0.18/0.29 % (3671944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.29 % (3671944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.29 % (3671944)CaDiCaL version: 2.1.3
% 0.18/0.29 % (3671944)Termination reason: Inappropriate
% 0.18/0.29 % (3671944)Time elapsed: 0.009 s
% 0.18/0.29 % (3671944)Peak memory usage: 11 MB
% 0.18/0.29 % (3671944)Instructions burned: 34 (million)
% 0.18/0.29 % (3671944)------------------------------
% 0.18/0.29 % (3671944)------------------------------
% 0.18/0.29 % (3671949)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3798733959:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.29 % (3671957)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2286791003:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.18/0.29 % (3671950)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=521390844:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.29 % (3671957)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.18/0.29 % (3671957)Terminated due to inappropriate strategy.
% 0.18/0.29 % (3671957)------------------------------
% 0.18/0.29 % (3671957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.29 % (3671957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.29 % (3671957)CaDiCaL version: 2.1.3
% 0.18/0.29 % (3671957)Termination reason: Inappropriate
% 0.18/0.29 % (3671957)Time elapsed: 0.008 s
% 0.18/0.29 % (3671957)Peak memory usage: 12 MB
% 0.18/0.29 % (3671957)Instructions burned: 32 (million)
% 0.18/0.29 % (3671957)------------------------------
% 0.18/0.29 % (3671957)------------------------------
% 0.18/0.29 % (3671947) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3671939-3671947"...
% 0.18/0.29 % (3671945) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3671939-3671945"...
% 0.18/0.29 % (3671947)...printing done.
% 0.18/0.29 % (3671945)...printing done.
% 0.18/0.29 % (3671947)Refutation found. Thanks to Tanya!
% 0.18/0.29 % SZS status Unsatisfiable for theBenchmark
% 0.18/0.29 % SZS output start Proof for theBenchmark
% 0.18/0.29 tff(type_def_5, type, 'S2': $tType).
% 0.18/0.29 tff(type_def_6, type, 'S8': $tType).
% 0.18/0.29 tff(type_def_7, type, 'S9': $tType).
% 0.18/0.29 tff(type_def_8, type, 'S4': $tType).
% 0.18/0.29 tff(type_def_9, type, 'S6': $tType).
% 0.18/0.29 tff(type_def_10, type, 'S5': $tType).
% 0.18/0.29 tff(type_def_11, type, 'S1': $tType).
% 0.18/0.29 tff(type_def_12, type, 'S3': $tType).
% 0.18/0.29 tff(type_def_13, type, 'S7': $tType).
% 0.18/0.29 tff(func_def_0, type, f18: 'S7').
% 0.18/0.29 tff(func_def_1, type, f22: ('S9' * $int) > $int).
% 0.18/0.29 tff(func_def_2, type, f16: 'S6').
% 0.18/0.29 tff(func_def_3, type, f11: 'S2').
% 0.18/0.29 tff(func_def_4, type, f13: ('S5' * $real) > 'S3').
% 0.18/0.29 tff(func_def_5, type, f4: 'S2').
% 0.18/0.29 tff(func_def_6, type, f26: 'S2').
% 0.18/0.29 tff(func_def_7, type, f10: 'S2').
% 0.18/0.29 tff(func_def_8, type, f20: 'S8').
% 0.18/0.29 tff(func_def_9, type, f9: 'S2').
% 0.18/0.29 tff(func_def_10, type, f19: ('S8' * 'S4') > $int).
% 0.18/0.29 tff(func_def_11, type, f6: 'S2').
% 0.18/0.29 tff(func_def_12, type, f3: ('S2' * $real) > $real).
% 0.18/0.29 tff(func_def_13, type, f8: 'S2').
% 0.18/0.29 tff(func_def_14, type, f23: 'S9').
% 0.18/0.29 tff(func_def_15, type, f5: $real).
% 0.18/0.29 tff(func_def_16, type, f1: 'S1').
% 0.18/0.29 tff(func_def_17, type, f7: $real).
% 0.18/0.29 tff(func_def_18, type, f21: 'S2').
% 0.18/0.29 tff(func_def_19, type, f24: 'S2').
% 0.18/0.29 tff(func_def_20, type, f2: 'S1').
% 0.18/0.29 tff(func_def_21, type, f15: ('S6' * $int) > 'S4').
% 0.18/0.29 tff(func_def_22, type, f12: ('S3' * 'S4') > $real).
% 0.18/0.29 tff(func_def_23, type, f17: ('S7' * $int) > $real).
% 0.18/0.29 tff(func_def_24, type, f14: 'S5').
% 0.18/0.29 tff(func_def_25, type, f25: ('S2' * $real * $real) > 'S1').
% 0.18/0.29 tff(func_def_44, type, sK3: $real).
% 0.18/0.29 tff(func_def_45, type, sK4: $real).
% 0.18/0.29 tff(func_def_46, type, sK5: $real > $real).
% 0.18/0.29 tff(func_def_47, type, sK6: $real > $real).
% 0.18/0.29 tff(func_def_48, type, sK7: $real > $real).
% 0.18/0.29 tff(func_def_49, type, sK8: $real > $real).
% 0.18/0.29 tff(func_def_50, type, sK9: $real > $real).
% 0.18/0.29 tff(func_def_51, type, sK10: $real).
% 0.18/0.29 tff(func_def_52, type, sK11: $real).
% 0.18/0.29 tff(func_def_53, type, sK12: $real).
% 0.18/0.29 tff(func_def_54, type, sK13: $real > $real).
% 0.18/0.29 tff(func_def_55, type, sK14: $real > $real).
% 0.18/0.29 tff(func_def_56, type, sK15: $real > $real).
% 0.18/0.29 tff(func_def_57, type, sK16: $real > $real).
% 0.18/0.29 tff(func_def_58, type, sK17: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_59, type, sK18: $real > $real).
% 0.18/0.29 tff(func_def_60, type, sK19: $real > $real).
% 0.18/0.29 tff(func_def_61, type, sK20: $real > $real).
% 0.18/0.29 tff(func_def_62, type, sK21: $real > $real).
% 0.18/0.29 tff(func_def_63, type, sK22: $real > $real).
% 0.18/0.29 tff(func_def_64, type, sK23: $real > $real).
% 0.18/0.29 tff(func_def_65, type, sK24: $real > $real).
% 0.18/0.29 tff(func_def_66, type, sK25: $real).
% 0.18/0.29 tff(func_def_67, type, sK26: $real > $real).
% 0.18/0.29 tff(func_def_68, type, sK27: $real > $real).
% 0.18/0.29 tff(func_def_69, type, sK28: $real > $real).
% 0.18/0.29 tff(func_def_70, type, sK29: $real).
% 0.18/0.29 tff(func_def_71, type, sK30: $real).
% 0.18/0.29 tff(func_def_72, type, sK31: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_73, type, sK32: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_74, type, sK33: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_75, type, sK34: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_76, type, sK35: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_77, type, sK36: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_78, type, sK37: $real > $real).
% 0.18/0.29 tff(func_def_79, type, sK38: $real > $real).
% 0.18/0.29 tff(func_def_80, type, sK39: $real > $real).
% 0.18/0.29 tff(func_def_81, type, sK40: $real > $real).
% 0.18/0.29 tff(func_def_82, type, sK41: $real > $real).
% 0.18/0.29 tff(func_def_83, type, sK42: $real > $real).
% 0.18/0.29 tff(func_def_84, type, sK43: $real > $real).
% 0.18/0.29 tff(func_def_85, type, sK44: $real).
% 0.18/0.29 tff(func_def_86, type, sK45: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_87, type, sK46: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_88, type, sK47: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_89, type, sK48: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_90, type, sK49: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_91, type, sK50: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_92, type, sK51: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_93, type, sK52: $real > $real).
% 0.18/0.29 tff(func_def_94, type, sK53: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_95, type, sK54: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_96, type, sK55: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_97, type, sK56: $real > $real).
% 0.18/0.29 tff(func_def_98, type, sK57: $real > $real).
% 0.18/0.29 tff(func_def_99, type, sK58: $real > $real).
% 0.18/0.29 tff(func_def_100, type, sK59: $real > $real).
% 0.18/0.29 tff(func_def_101, type, sK60: $real > $real).
% 0.18/0.29 tff(func_def_102, type, sK61: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_103, type, sK62: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_104, type, sK63: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_105, type, sK64: $real > $real).
% 0.18/0.29 tff(func_def_106, type, sK65: $real > $real).
% 0.18/0.29 tff(func_def_107, type, sK66: $real > $real).
% 0.18/0.29 tff(func_def_108, type, sK67: $real > $real).
% 0.18/0.29 tff(func_def_109, type, sK68: $real > $real).
% 0.18/0.29 tff(func_def_110, type, sK69: $real > $real).
% 0.18/0.29 tff(func_def_111, type, sK70: $real > $real).
% 0.18/0.29 tff(func_def_112, type, sK71: $real > $real).
% 0.18/0.29 tff(func_def_113, type, sK72: $real > $real).
% 0.18/0.29 tff(func_def_114, type, sK73: $real > $real).
% 0.18/0.29 tff(func_def_115, type, sK74: $real > $real).
% 0.18/0.29 tff(func_def_116, type, sK75: $real > $real).
% 0.18/0.29 tff(func_def_117, type, sK76: $real > $real).
% 0.18/0.29 tff(func_def_118, type, sK77: $real > $real).
% 0.18/0.29 tff(func_def_119, type, sK78: $real > $real).
% 0.18/0.29 tff(func_def_120, type, sK79: $real > $real).
% 0.18/0.29 tff(func_def_121, type, sK80: $real > $real).
% 0.18/0.29 tff(func_def_122, type, sK81: $real > $real).
% 0.18/0.29 tff(func_def_123, type, sK82: $real).
% 0.18/0.29 tff(func_def_124, type, sK83: $real > $real).
% 0.18/0.29 tff(func_def_125, type, sK84: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_126, type, sK85: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_127, type, sK86: $real > $real).
% 0.18/0.29 tff(func_def_128, type, sK87: $real > $real).
% 0.18/0.29 tff(func_def_129, type, sK88: $real).
% 0.18/0.29 tff(func_def_130, type, sK89: $real > 'S4').
% 0.18/0.29 tff(func_def_131, type, sK90: $real > 'S4').
% 0.18/0.29 tff(func_def_132, type, sK91: $real > 'S4').
% 0.18/0.29 tff(func_def_133, type, sK92: $real > 'S4').
% 0.18/0.29 tff(func_def_134, type, sK93: $real > 'S4').
% 0.18/0.29 tff(func_def_135, type, sK94: $real > 'S4').
% 0.18/0.29 tff(func_def_136, type, sK95: $real > $real).
% 0.18/0.29 tff(func_def_137, type, sK96: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_138, type, sK97: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_139, type, sK98: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_140, type, sK99: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_141, type, sK100: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_142, type, sK101: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_143, type, sK102: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_144, type, sK103: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_145, type, sK104: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_146, type, sK105: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_147, type, sK106: $real > 'S4').
% 0.18/0.29 tff(func_def_148, type, sK107: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_149, type, sK108: ($real * 'S4') > $real).
% 0.18/0.29 tff(func_def_150, type, sK109: ('S4' * $real) > $real).
% 0.18/0.29 tff(func_def_151, type, sK110: ('S4' * $real) > $real).
% 0.18/0.29 tff(func_def_152, type, sK111: $real > 'S4').
% 0.18/0.29 tff(func_def_153, type, sK112: $real > $real).
% 0.18/0.29 tff(func_def_154, type, sK113: ($int * $real) > $real).
% 0.18/0.29 tff(func_def_155, type, sK114: ($int * $int) > $int).
% 0.18/0.29 tff(func_def_156, type, sK115: $real > 'S4').
% 0.18/0.29 tff(func_def_157, type, sK116: $real > $real).
% 0.18/0.29 tff(func_def_158, type, sK117: $real).
% 0.18/0.29 tff(func_def_159, type, sK118: ($real * $real * $real * $real) > $real).
% 0.18/0.29 tff(func_def_160, type, sK119: ($real * $real * $real * $real) > $real).
% 0.18/0.29 tff(func_def_161, type, sK120: $real > $real).
% 0.18/0.29 tff(func_def_162, type, sK121: $real > $real).
% 0.18/0.29 tff(func_def_163, type, sK122: $real > $real).
% 0.18/0.29 tff(func_def_164, type, sK123: $real > $real).
% 0.18/0.29 tff(func_def_165, type, sK124: $real).
% 0.18/0.29 tff(func_def_166, type, sK125: $real).
% 0.18/0.29 tff(func_def_167, type, sK126: $real).
% 0.18/0.29 tff(func_def_168, type, sK127: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_169, type, sK128: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_170, type, sK129: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_171, type, sK130: ($real * $real * $real * $real) > 'S4').
% 0.18/0.29 tff(func_def_172, type, sK131: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_173, type, sK132: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_174, type, sK133: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_175, type, sK134: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_176, type, sK135: ($real * $real * $real * $real) > 'S4').
% 0.18/0.29 tff(func_def_177, type, sK136: ($real * $real * $real * $real) > 'S4').
% 0.18/0.29 tff(func_def_178, type, sK137: ($real * $real * $real * $real) > $real).
% 0.18/0.29 tff(func_def_179, type, sK138: $real > $real).
% 0.18/0.29 tff(func_def_180, type, sK139: ($real * $real * $real) > $real).
% 0.18/0.29 tff(func_def_181, type, sK140: ($real * $real * $real) > 'S4').
% 0.18/0.29 tff(func_def_182, type, sK141: ($real * $real * $real) > $real).
% 0.18/0.29 tff(func_def_183, type, sK142: ($real * $real * $real) > $real).
% 0.18/0.29 tff(func_def_184, type, sK143: ($real * $real * $real) > 'S4').
% 0.18/0.29 tff(func_def_185, type, sK144: ($real * $real * $real) > $real).
% 0.18/0.29 tff(func_def_186, type, sK145: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_187, type, sK146: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_188, type, sK147: $real).
% 0.18/0.29 tff(func_def_189, type, sK148: $real).
% 0.18/0.29 tff(func_def_190, type, sK149: $real > $real).
% 0.18/0.29 tff(func_def_191, type, sK150: $real > $real).
% 0.18/0.29 tff(func_def_192, type, sK151: $real > $real).
% 0.18/0.29 tff(func_def_193, type, sK152: $real > $real).
% 0.18/0.29 tff(func_def_194, type, sK153: $real > $real).
% 0.18/0.29 tff(func_def_195, type, sK154: $real > $real).
% 0.18/0.29 tff(func_def_196, type, sK155: $real > $real).
% 0.18/0.29 tff(func_def_197, type, sK156: $real > $real).
% 0.18/0.29 tff(func_def_198, type, sK157: $real > $real).
% 0.18/0.29 tff(func_def_199, type, sK158: $real > $real).
% 0.18/0.29 tff(func_def_200, type, sK159: $real > $real).
% 0.18/0.29 tff(func_def_201, type, sK160: $real > $real).
% 0.18/0.29 tff(func_def_202, type, sK161: $real > $real).
% 0.18/0.29 tff(func_def_203, type, sK162: $real > $real).
% 0.18/0.29 tff(func_def_204, type, sK163: $real > $real).
% 0.18/0.29 tff(func_def_205, type, sK164: $real).
% 0.18/0.29 tff(func_def_206, type, sK165: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_207, type, sK166: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_208, type, sK167: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_209, type, sK168: $real > $real).
% 0.18/0.29 tff(func_def_210, type, sK169: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_211, type, sK170: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_212, type, sK171: $real > $real).
% 0.18/0.29 tff(func_def_213, type, sK172: $real > $real).
% 0.18/0.29 tff(func_def_214, type, sK173: ($real * $real) > 'S4').
% 0.18/0.29 tff(func_def_215, type, sK174: ($real * $real) > $real).
% 0.18/0.29 tff(func_def_216, type, sK175: $real > $real).
% 0.18/0.29 tff(func_def_217, type, sK176: 'S2' > $real).
% 0.18/0.29 tff(func_def_218, type, sK177: ($real * $real * 'S2' * $real) > $real).
% 0.18/0.29 tff(func_def_219, type, sK178: ('S2' * $real) > $real).
% 0.18/0.29 tff(pred_def_5, type, sP0: $real > $o).
% 0.18/0.29 tff(pred_def_6, type, sP1: ($real * $real * $real) > $o).
% 0.18/0.29 tff(pred_def_7, type, sP2: ($real * $real * $real) > $o).
% 0.18/0.29 tff(f2,axiom,(
% 0.18/0.29 ~(f3(f4,f5) != 0/1 | f3(f6,f5) != 1/1)),
% 0.18/0.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_2)).
% 0.18/0.29 tff(f3,axiom,(
% 0.18/0.29 ? [X0 : $real] : (X0 = 0/1 & ($less(X0,f5) => ($less(f5,f7) => f3(f4,f5) != X0)))),
% 0.18/0.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_3)).
% 0.18/0.29 tff(f4,axiom,(
% 0.18/0.29 f5 = f7 => f3(f6,f5) != 1/1),
% 0.18/0.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_4)).
% 0.18/0.29 tff(f5,axiom,(
% 0.18/0.29 $less(f7,f5) => ($less(f5,$product(2/1,f7)) => f3(f4,f5) != 0/1)),
% 0.18/0.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_5)).
% 0.18/0.29 tff(f8,axiom,(
% 0.18/0.29 $less(0/1,f5)),
% 0.18/0.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_8)).
% 0.18/0.29 tff(f9,axiom,(
% 0.18/0.29 $less(f5,$product(2/1,f7))),
% 0.18/0.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_9)).
% 0.18/0.29 tff(f372,definition,(
% 0.18/0.29 ( ! [X0 : $real,X1 : $real] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 0.18/0.29 introduced(theory,[tha_order_totality])).
% 0.18/0.29 tff(f384,plain,(
% 0.18/0.29 f3(f4,f5) = 0/1 & f3(f6,f5) = 1/1),
% 0.18/0.29 inference(ennf_transformation,[],[f2])).
% 0.18/0.29 tff(f385,plain,(
% 0.18/0.29 ? [X0 : $real] : (X0 = 0/1 & ((f3(f4,f5) != X0 | ~$less(f5,f7)) | ~$less(X0,f5)))),
% 0.18/0.29 inference(ennf_transformation,[],[f3])).
% 0.18/0.29 tff(f386,plain,(
% 0.18/0.29 ? [X0 : $real] : (X0 = 0/1 & (f3(f4,f5) != X0 | ~$less(f5,f7) | ~$less(X0,f5)))),
% 0.18/0.29 inference(flattening,[],[f385])).
% 0.18/0.29 tff(f387,plain,(
% 0.18/0.29 f3(f6,f5) != 1/1 | f5 != f7),
% 0.18/0.29 inference(ennf_transformation,[],[f4])).
% 0.18/0.29 tff(f388,plain,(
% 0.18/0.29 (f3(f4,f5) != 0/1 | ~$less(f5,$product(2/1,f7))) | ~$less(f7,f5)),
% 0.18/0.29 inference(ennf_transformation,[],[f5])).
% 0.18/0.29 tff(f389,plain,(
% 0.18/0.29 f3(f4,f5) != 0/1 | ~$less(f5,$product(2/1,f7)) | ~$less(f7,f5)),
% 0.18/0.29 inference(flattening,[],[f388])).
% 0.18/0.29 tff(f570,plain,(
% 0.18/0.29 0/1 = sK3 & (f3(f4,f5) != sK3 | ~$less(f5,f7) | ~$less(sK3,f5))),
% 0.18/0.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X0,sK3)],[f386])).
% 0.18/0.29 tff(f738,plain,(
% 0.18/0.29 f3(f6,f5) = 1/1),
% 0.18/0.29 inference(cnf_transformation,[],[f384])).
% 0.18/0.29 tff(f739,plain,(
% 0.18/0.29 f3(f4,f5) = 0/1),
% 0.18/0.29 inference(cnf_transformation,[],[f384])).
% 0.18/0.29 tff(f740,plain,(
% 0.18/0.29 f3(f4,f5) != sK3 | ~$less(f5,f7) | ~$less(sK3,f5)),
% 0.18/0.29 inference(cnf_transformation,[],[f570])).
% 0.18/0.29 tff(f741,plain,(
% 0.18/0.29 0/1 = sK3),
% 0.18/0.29 inference(cnf_transformation,[],[f570])).
% 0.18/0.29 tff(f742,plain,(
% 0.18/0.29 f3(f6,f5) != 1/1 | f5 != f7),
% 0.18/0.29 inference(cnf_transformation,[],[f387])).
% 0.18/0.29 tff(f743,plain,(
% 0.18/0.29 f3(f4,f5) != 0/1 | ~$less(f5,$product(2/1,f7)) | ~$less(f7,f5)),
% 0.18/0.29 inference(cnf_transformation,[],[f389])).
% 0.18/0.29 tff(f746,plain,(
% 0.18/0.29 $less(0/1,f5)),
% 0.18/0.29 inference(cnf_transformation,[],[f8])).
% 0.18/0.29 tff(f747,plain,(
% 0.18/0.29 $less(f5,$product(2/1,f7))),
% 0.18/0.29 inference(cnf_transformation,[],[f9])).
% 0.18/0.29 tff(f1268,plain,(
% 0.18/0.29 f3(f4,f5) != 0/1 | ~$less(f5,f7) | ~$less(0/1,f5)),
% 0.18/0.29 inference(definition_unfolding,[],[f740,f741,f741])).
% 0.18/0.29 tff(f1514,definition,(
% 0.18/0.29 spl179_1 <=> $less(f7,f5)),
% 0.18/0.29 introduced(definition,[new_symbols(definition,[spl179_1])],[avatar_definition])).
% 0.18/0.29 tff(f1516,plain,(
% 0.18/0.29 ~$less(f7,f5) | spl179_1),
% 0.18/0.29 inference(avatar_component_clause,[],[f1514])).
% 0.18/0.29 tff(f1518,definition,(
% 0.18/0.29 spl179_2 <=> $less(f5,$product(2/1,f7))),
% 0.18/0.29 introduced(definition,[new_symbols(definition,[spl179_2])],[avatar_definition])).
% 0.18/0.29 tff(f1522,definition,(
% 0.18/0.29 spl179_3 <=> f3(f4,f5) = 0/1),
% 0.18/0.29 introduced(definition,[new_symbols(definition,[spl179_3])],[avatar_definition])).
% 0.18/0.29 tff(f1527,definition,(
% 0.18/0.29 spl179_4 <=> $less(0/1,f5)),
% 0.18/0.29 introduced(definition,[new_symbols(definition,[spl179_4])],[avatar_definition])).
% 0.18/0.29 tff(f1531,definition,(
% 0.18/0.29 spl179_5 <=> $less(f5,f7)),
% 0.18/0.29 introduced(definition,[new_symbols(definition,[spl179_5])],[avatar_definition])).
% 0.18/0.29 tff(f1533,plain,(
% 0.18/0.29 ~$less(f5,f7) | spl179_5),
% 0.18/0.29 inference(avatar_component_clause,[],[f1531])).
% 0.18/0.29 tff(f1536,definition,(
% 0.18/0.29 spl179_6 <=> f5 = f7),
% 0.18/0.29 introduced(definition,[new_symbols(definition,[spl179_6])],[avatar_definition])).
% 0.18/0.29 tff(f1538,plain,(
% 0.18/0.29 f5 != f7 | spl179_6),
% 0.18/0.29 inference(avatar_component_clause,[],[f1536])).
% 0.18/0.29 tff(f1540,definition,(
% 0.18/0.29 spl179_7 <=> f3(f6,f5) = 1/1),
% 0.18/0.29 introduced(definition,[new_symbols(definition,[spl179_7])],[avatar_definition])).
% 0.18/0.29 tff(f1544,plain,(
% 0.18/0.29 spl179_2),
% 0.18/0.29 inference(avatar_split_clause,[],[f747,f1518])).
% 0.18/0.29 tff(f1545,plain,(
% 0.18/0.29 spl179_4),
% 0.18/0.29 inference(avatar_split_clause,[],[f746,f1527])).
% 0.18/0.29 tff(f1546,plain,(
% 0.18/0.29 ~spl179_1 | ~spl179_2 | ~spl179_3),
% 0.18/0.29 inference(avatar_split_clause,[],[f743,f1522,f1518,f1514])).
% 0.18/0.29 tff(f1547,plain,(
% 0.18/0.29 ~spl179_6 | ~spl179_7),
% 0.18/0.29 inference(avatar_split_clause,[],[f742,f1540,f1536])).
% 0.18/0.29 tff(f1548,plain,(
% 0.18/0.29 ~spl179_4 | ~spl179_5 | ~spl179_3),
% 0.18/0.29 inference(avatar_split_clause,[],[f1268,f1522,f1531,f1527])).
% 0.18/0.29 tff(f1549,plain,(
% 0.18/0.29 spl179_7),
% 0.18/0.29 inference(avatar_split_clause,[],[f738,f1540])).
% 0.18/0.29 tff(f1550,plain,(
% 0.18/0.29 spl179_3),
% 0.18/0.29 inference(avatar_split_clause,[],[f739,f1522])).
% 0.18/0.29 tff(f1736,plain,(
% 0.18/0.29 $less(f5,f7) | f5 = f7 | spl179_1),
% 0.18/0.29 inference(resolution,[],[f372,f1516])).
% 0.18/0.29 tff(f1777,plain,(
% 0.18/0.29 f5 = f7 | (spl179_1 | spl179_5)),
% 0.18/0.29 inference(forward_subsumption_resolution,[],[f1736,f1533])).
% 0.18/0.29 tff(f1781,plain,(
% 0.18/0.29 $false | (spl179_1 | spl179_5 | spl179_6)),
% 0.18/0.29 inference(forward_subsumption_resolution,[],[f1777,f1538])).
% 0.18/0.29 tff(f1782,plain,(
% 0.18/0.29 spl179_1 | spl179_5 | spl179_6),
% 0.18/0.29 inference(avatar_contradiction_clause,[],[f1781])).
% 0.18/0.29 cnf(s4, plain, spl179_2, inference(sat_conversion,[],[f1544])).
% 0.18/0.29 cnf(s5, plain, spl179_4, inference(sat_conversion,[],[f1545])).
% 0.18/0.29 cnf(s8, plain, ~spl179_1 | ~spl179_2 | ~spl179_3, inference(sat_conversion,[],[f1546])).
% 0.18/0.29 cnf(s9, plain, ~spl179_6 | ~spl179_7, inference(sat_conversion,[],[f1547])).
% 0.18/0.29 cnf(s10, plain, ~spl179_3 | ~spl179_4 | ~spl179_5, inference(sat_conversion,[],[f1548])).
% 0.18/0.29 cnf(s11, plain, spl179_7, inference(sat_conversion,[],[f1549])).
% 0.18/0.29 cnf(s12, plain, spl179_3, inference(sat_conversion,[],[f1550])).
% 0.18/0.29 cnf(s18, plain, spl179_1 | spl179_5 | spl179_6, inference(sat_conversion,[],[f1782])).
% 0.18/0.29 cnf(s19, plain, ~spl179_4 | ~spl179_5, inference(rat,[],[s10,s12])).
% 0.18/0.29 cnf(s20, plain, ~spl179_6, inference(rat,[],[s9,s11])).
% 0.18/0.29 cnf(s21, plain, ~spl179_1 | ~spl179_2, inference(rat,[],[s8,s12])).
% 0.18/0.29 cnf(s22, plain, ~spl179_5, inference(rat,[],[s19,s5])).
% 0.18/0.29 cnf(s23, plain, spl179_1, inference(rat,[],[s18,s20,s22])).
% 0.18/0.29 cnf(s24, plain, ~spl179_2, inference(rat,[],[s21,s23])).
% 0.18/0.29 cnf(s25, plain, $false, inference(rat,[],[s4,s24])).
% 0.18/0.29 tff(f1783,plain,(
% 0.18/0.29 $false),
% 0.18/0.29 inference(avatar_sat_refutation,[],[s25])).
% 0.18/0.29 % SZS output end Proof for theBenchmark
% 0.18/0.29 % (3671947)------------------------------
% 0.18/0.29 % (3671947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.29 % (3671947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.29 % (3671947)CaDiCaL version: 2.1.3
% 0.18/0.29 % (3671947)Termination reason: Refutation
% 0.18/0.29 % (3671947)Time elapsed: 0.032 s
% 0.18/0.29 % (3671947)Peak memory usage: 13 MB
% 0.18/0.29 % (3671947)Instructions burned: 57 (million)
% 0.18/0.29 % (3671939)Success in time 0.084 s
% 0.18/0.29 % Vampire exiting
%------------------------------------------------------------------------------