%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP204^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:11:06 AM UTC 2026
% Result : Theorem 0.79s 0.45s
% Output : Refutation 0.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 13
% Syntax : Number of formulae : 76 ( 39 unt; 0 typ; 0 def)
% Number of atoms : 266 ( 152 equ; 0 cnn)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 2073 ( 69 ~; 56 |; 21 &;1915 @)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Number of types : 14 ( 13 usr)
% Number of type conns : 987 ( 987 >; 0 *; 0 +; 0 <<)
% Number of symbols : 217 ( 214 usr; 11 con; 0-4 aty)
% Number of variables : 999 ( 989 ^; 10 !; 0 ?; 999 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
produc1418842292n_game: $tType ).
thf(type_def_6,type,
produc62062515n_game: $tType ).
thf(type_def_7,type,
produc799602994n_game: $tType ).
thf(type_def_8,type,
produc1739631244on_fml: $tType ).
thf(type_def_9,type,
option_game: $tType ).
thf(type_def_10,type,
option_trm: $tType ).
thf(type_def_11,type,
option_fml: $tType ).
thf(type_def_12,type,
set_variable: $tType ).
thf(type_def_13,type,
variable: $tType ).
thf(type_def_14,type,
game: $tType ).
thf(type_def_15,type,
char: $tType ).
thf(type_def_16,type,
trm: $tType ).
thf(type_def_17,type,
fml: $tType ).
thf(type_def_18,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
if_option_fml: $o > option_fml > option_fml > option_fml ).
thf(func_def_1,type,
if_option_trm: $o > option_trm > option_trm > option_trm ).
thf(func_def_2,type,
inf_inf_variable_o: ( variable > $o ) > ( variable > $o ) > variable > $o ).
thf(func_def_3,type,
inf_inf_o: $o > $o > $o ).
thf(func_def_4,type,
inf_inf_set_variable: set_variable > set_variable > set_variable ).
thf(func_def_5,type,
none_fml: option_fml ).
thf(func_def_6,type,
none_game: option_game ).
thf(func_def_7,type,
none_trm: option_trm ).
thf(func_def_8,type,
some_fml: fml > option_fml ).
thf(func_def_9,type,
some_game: game > option_game ).
thf(func_def_10,type,
some_trm: trm > option_trm ).
thf(func_def_11,type,
case_option_o_fml: $o > ( fml > $o ) > option_fml > $o ).
thf(func_def_12,type,
case_option_o_game: $o > ( game > $o ) > option_game > $o ).
thf(func_def_13,type,
case_option_o_trm: $o > ( trm > $o ) > option_trm > $o ).
thf(func_def_14,type,
case_o209804997ml_fml: option_fml > ( fml > option_fml ) > option_fml > option_fml ).
thf(func_def_15,type,
case_o325794063ml_trm: option_fml > ( trm > option_fml ) > option_trm > option_fml ).
thf(func_def_16,type,
case_o487727941rm_trm: option_trm > ( trm > option_trm ) > option_trm > option_trm ).
thf(func_def_17,type,
the_fml: option_fml > fml ).
thf(func_def_18,type,
the_game: option_game > game ).
thf(func_def_19,type,
the_trm: option_trm > trm ).
thf(func_def_20,type,
bot_bot_variable_o: variable > $o ).
thf(func_def_21,type,
bot_bot_set_variable: set_variable ).
thf(func_def_22,type,
ord_le1407353162able_o: ( variable > $o ) > ( variable > $o ) > $o ).
thf(func_def_23,type,
ord_le282106107riable: set_variable > set_variable > $o ).
thf(func_def_24,type,
produc2124676926on_fml: option_game > option_fml > produc1739631244on_fml ).
thf(func_def_25,type,
produc1598111045on_fml: ( ( char > option_fml ) > ( char > option_game ) > char > option_fml ) > produc799602994n_game > char > option_fml ).
thf(func_def_26,type,
produc1214549391on_trm: ( ( char > option_fml ) > ( char > option_game ) > char > option_trm ) > produc799602994n_game > char > option_trm ).
thf(func_def_27,type,
produc1591622303on_fml: ( ( char > option_fml ) > ( char > option_game ) > option_fml ) > produc799602994n_game > option_fml ).
thf(func_def_28,type,
produc2129367017on_trm: ( ( char > option_fml ) > ( char > option_game ) > option_trm ) > produc799602994n_game > option_trm ).
thf(func_def_29,type,
produc377919108on_fml: ( ( char > option_trm ) > produc799602994n_game > char > option_fml ) > produc62062515n_game > char > option_fml ).
thf(func_def_30,type,
produc2141841102on_trm: ( ( char > option_trm ) > produc799602994n_game > char > option_trm ) > produc62062515n_game > char > option_trm ).
thf(func_def_31,type,
produc1903410526on_fml: ( ( char > option_trm ) > produc799602994n_game > option_fml ) > produc62062515n_game > option_fml ).
thf(func_def_32,type,
produc293671592on_trm: ( ( char > option_trm ) > produc799602994n_game > option_trm ) > produc62062515n_game > option_trm ).
thf(func_def_33,type,
produc1278328899on_fml: ( ( char > option_trm ) > produc62062515n_game > char > option_fml ) > produc1418842292n_game > char > option_fml ).
thf(func_def_34,type,
produc724717725on_fml: ( ( char > option_trm ) > produc62062515n_game > option_fml ) > produc1418842292n_game > option_fml ).
thf(func_def_35,type,
produc1420172399on_fml: ( ( char > option_fml ) > ( char > option_game ) > char > option_fml ) > produc799602994n_game > char > option_fml ).
thf(func_def_36,type,
produc1036610745on_trm: ( ( char > option_fml ) > ( char > option_game ) > char > option_trm ) > produc799602994n_game > char > option_trm ).
thf(func_def_37,type,
produc347802313on_fml: ( ( char > option_fml ) > ( char > option_game ) > option_fml ) > produc799602994n_game > option_fml ).
thf(func_def_38,type,
produc885547027on_trm: ( ( char > option_fml ) > ( char > option_game ) > option_trm ) > produc799602994n_game > option_trm ).
thf(func_def_39,type,
produc1615133358on_fml: ( ( char > option_trm ) > produc799602994n_game > char > option_fml ) > produc62062515n_game > char > option_fml ).
thf(func_def_40,type,
produc1231571704on_trm: ( ( char > option_trm ) > produc799602994n_game > char > option_trm ) > produc62062515n_game > char > option_trm ).
thf(func_def_41,type,
produc154833544on_fml: ( ( char > option_trm ) > produc799602994n_game > option_fml ) > produc62062515n_game > option_fml ).
thf(func_def_42,type,
produc692578258on_trm: ( ( char > option_trm ) > produc799602994n_game > option_trm ) > produc62062515n_game > option_trm ).
thf(func_def_43,type,
produc1250175341on_fml: ( ( char > option_trm ) > produc62062515n_game > char > option_fml ) > produc1418842292n_game > char > option_fml ).
thf(func_def_44,type,
produc866613687on_trm: ( ( char > option_trm ) > produc62062515n_game > char > option_trm ) > produc1418842292n_game > char > option_trm ).
thf(func_def_45,type,
produc1499310791on_fml: ( ( char > option_trm ) > produc62062515n_game > option_fml ) > produc1418842292n_game > option_fml ).
thf(func_def_46,type,
collect_variable: ( variable > $o ) > set_variable ).
thf(func_def_47,type,
is_empty_variable: set_variable > $o ).
thf(func_def_48,type,
static_FVF: fml > set_variable ).
thf(func_def_49,type,
static_FVT: trm > set_variable ).
thf(func_def_50,type,
geq: trm > trm > fml ).
thf(func_def_51,type,
pred: char > trm > fml ).
thf(func_def_52,type,
const: char > trm ).
thf(func_def_53,type,
func: char > trm > trm ).
thf(func_def_54,type,
uSubst152838031e_Geqo: option_trm > option_trm > option_fml ).
thf(func_def_55,type,
uSubst1408967625substt: trm > produc1418842292n_game ).
thf(func_def_56,type,
uSubst1559070963pconst: produc1418842292n_game > set_variable > char > option_trm ).
thf(func_def_57,type,
uSubst516392804stappf: produc1418842292n_game > set_variable > fml > option_fml ).
thf(func_def_58,type,
uSubst516392818stappt: produc1418842292n_game > set_variable > trm > option_trm ).
thf(func_def_59,type,
member_variable: variable > set_variable > $o ).
thf(func_def_60,type,
ua: set_variable ).
thf(func_def_61,type,
va: set_variable ).
thf(func_def_62,type,
sigma: produc1418842292n_game ).
thf(func_def_63,type,
theta: trm ).
thf(func_def_64,type,
p: char ).
thf(func_def_65,type,
vv: set_variable > set_variable > variable ).
thf(func_def_66,type,
vva: set_variable > set_variable > variable ).
thf(func_def_68,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_69,type,
vAND: $o > $o > $o ).
thf(func_def_70,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_71,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_72,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_73,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_76,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_77,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_78,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_79,type,
vNOT: $o > $o ).
thf(func_def_80,type,
vIMP: $o > $o > $o ).
thf(func_def_81,type,
vOR: $o > $o > $o ).
thf(func_def_82,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_83,type,
sP0: ( option_fml > option_fml > $o ) > option_fml > option_fml > $o ).
thf(func_def_84,type,
sP1: ( option_fml > option_trm > $o ) > option_fml > option_trm > $o ).
thf(func_def_85,type,
sP2: ( option_fml > option_game > $o ) > option_fml > option_game > $o ).
thf(func_def_86,type,
sP3: ( option_trm > option_fml > $o ) > option_trm > option_fml > $o ).
thf(func_def_87,type,
sP4: ( option_trm > option_trm > $o ) > option_trm > option_trm > $o ).
thf(func_def_88,type,
sP5: ( option_trm > option_game > $o ) > option_trm > option_game > $o ).
thf(func_def_89,type,
sP6: ( option_game > option_fml > $o ) > option_game > option_fml > $o ).
thf(func_def_90,type,
sP7: ( option_game > option_trm > $o ) > option_game > option_trm > $o ).
thf(func_def_91,type,
sP8: ( option_game > option_game > $o ) > option_game > option_game > $o ).
thf(func_def_92,type,
sP9: option_trm > option_trm > option_fml > $o ).
thf(func_def_93,type,
sK10: set_variable > set_variable > variable ).
thf(func_def_94,type,
sK11: ( option_fml > option_fml > $o ) > option_fml > option_fml > fml ).
thf(func_def_95,type,
sK12: ( option_fml > option_fml > $o ) > option_fml > option_fml > fml ).
thf(func_def_96,type,
sK13: ( option_fml > option_trm > $o ) > option_fml > option_trm > fml ).
thf(func_def_97,type,
sK14: ( option_fml > option_trm > $o ) > option_fml > option_trm > trm ).
thf(func_def_98,type,
sK15: ( option_fml > option_game > $o ) > option_fml > option_game > fml ).
thf(func_def_99,type,
sK16: ( option_fml > option_game > $o ) > option_fml > option_game > game ).
thf(func_def_100,type,
sK17: ( option_trm > option_fml > $o ) > option_trm > option_fml > trm ).
thf(func_def_101,type,
sK18: ( option_trm > option_fml > $o ) > option_trm > option_fml > fml ).
thf(func_def_102,type,
sK19: ( option_trm > option_trm > $o ) > option_trm > option_trm > trm ).
thf(func_def_103,type,
sK20: ( option_trm > option_trm > $o ) > option_trm > option_trm > trm ).
thf(func_def_104,type,
sK21: ( option_trm > option_game > $o ) > option_trm > option_game > trm ).
thf(func_def_105,type,
sK22: ( option_trm > option_game > $o ) > option_trm > option_game > game ).
thf(func_def_106,type,
sK23: ( option_game > option_fml > $o ) > option_game > option_fml > game ).
thf(func_def_107,type,
sK24: ( option_game > option_fml > $o ) > option_game > option_fml > fml ).
thf(func_def_108,type,
sK25: ( option_game > option_trm > $o ) > option_game > option_trm > game ).
thf(func_def_109,type,
sK26: ( option_game > option_trm > $o ) > option_game > option_trm > trm ).
thf(func_def_110,type,
sK27: ( option_game > option_game > $o ) > option_game > option_game > game ).
thf(func_def_111,type,
sK28: ( option_game > option_game > $o ) > option_game > option_game > game ).
thf(func_def_112,type,
sK29: ( option_fml > $o ) > fml ).
thf(func_def_113,type,
sK30: ( option_trm > $o ) > trm ).
thf(func_def_114,type,
sK31: ( option_game > $o ) > game ).
thf(func_def_115,type,
sK32: option_fml > fml ).
thf(func_def_116,type,
sK33: option_trm > trm ).
thf(func_def_117,type,
sK34: option_game > game ).
thf(func_def_118,type,
sK35: ( variable > option_fml > $o ) > variable ).
thf(func_def_119,type,
sK36: ( variable > option_fml > $o ) > variable ).
thf(func_def_120,type,
sK37: ( variable > option_fml > $o ) > fml ).
thf(func_def_121,type,
sK38: ( option_fml > $o ) > fml ).
thf(func_def_122,type,
sK39: option_fml > fml ).
thf(func_def_123,type,
sK40: ( variable > $o ) > ( variable > $o ) > variable ).
thf(func_def_124,type,
sK41: ( option_fml > option_fml > $o ) > fml ).
thf(func_def_125,type,
sK42: ( option_fml > option_fml > $o ) > option_fml ).
thf(func_def_126,type,
sK43: ( option_fml > option_fml > $o ) > fml ).
thf(func_def_127,type,
sK44: ( option_fml > option_fml > $o ) > fml ).
thf(func_def_128,type,
sK45: char > set_variable > produc1418842292n_game > fml ).
thf(func_def_129,type,
sK46: set_variable > set_variable > variable ).
thf(func_def_130,type,
sK47: ( char > option_trm > $o ) > char ).
thf(func_def_131,type,
sK48: ( char > option_trm > $o ) > char ).
thf(func_def_132,type,
sK49: ( char > option_trm > $o ) > trm ).
thf(func_def_133,type,
sK50: ( option_trm > option_trm > $o ) > trm ).
thf(func_def_134,type,
sK51: ( option_trm > option_trm > $o ) > option_trm ).
thf(func_def_135,type,
sK52: ( option_trm > option_trm > $o ) > trm ).
thf(func_def_136,type,
sK53: ( option_trm > option_trm > $o ) > trm ).
thf(func_def_137,type,
sK54: ( variable > option_trm > $o ) > variable ).
thf(func_def_138,type,
sK55: ( variable > option_trm > $o ) > variable ).
thf(func_def_139,type,
sK56: ( variable > option_trm > $o ) > trm ).
thf(func_def_140,type,
sK57: option_trm > trm ).
thf(func_def_141,type,
sK58: ( option_trm > $o ) > trm ).
thf(func_def_142,type,
sK59: ( option_game > option_fml > $o ) > game ).
thf(func_def_143,type,
sK60: ( option_game > option_fml > $o ) > option_fml ).
thf(func_def_144,type,
sK61: ( option_game > option_fml > $o ) > game ).
thf(func_def_145,type,
sK62: ( option_game > option_fml > $o ) > fml ).
thf(func_def_146,type,
sK63: option_fml > ( fml > $o ) > fml ).
thf(func_def_147,type,
sK64: option_trm > ( trm > $o ) > trm ).
thf(func_def_148,type,
sK65: option_game > ( game > $o ) > game ).
thf(func_def_149,type,
sK66: set_variable > variable ).
thf(func_def_150,type,
sK67: ( variable > $o ) > ( variable > $o ) > variable ).
thf(func_def_151,type,
sK68: ( set_variable > set_variable > set_variable ) > set_variable ).
thf(func_def_152,type,
sK69: ( set_variable > set_variable > set_variable ) > set_variable ).
thf(func_def_153,type,
sK70: ( set_variable > set_variable > set_variable ) > set_variable ).
thf(func_def_154,type,
sK71: ( set_variable > set_variable > set_variable ) > set_variable ).
thf(func_def_155,type,
sK72: ( set_variable > set_variable > set_variable ) > set_variable ).
thf(func_def_156,type,
sK73: ( set_variable > set_variable > set_variable ) > set_variable ).
thf(func_def_157,type,
sK74: ( set_variable > set_variable > set_variable ) > set_variable ).
thf(func_def_158,type,
sK75: set_variable > set_variable > variable ).
thf(func_def_159,type,
sK76: ( variable > $o ) > ( variable > $o ) > set_variable > variable ).
thf(func_def_160,type,
sK77: set_variable > variable ).
thf(func_def_161,type,
sK78: option_game > game ).
thf(func_def_162,type,
sK79: ( option_game > $o ) > game ).
thf(func_def_163,type,
sK80: ( option_game > option_game > $o ) > game ).
thf(func_def_164,type,
sK81: ( option_game > option_game > $o ) > option_game ).
thf(func_def_165,type,
sK82: ( option_game > option_game > $o ) > game ).
thf(func_def_166,type,
sK83: ( option_game > option_game > $o ) > game ).
thf(func_def_167,type,
sK84: ( set_variable > set_variable ) > set_variable ).
thf(func_def_168,type,
sK85: ( set_variable > set_variable ) > set_variable ).
thf(func_def_169,type,
sK86: ( set_variable > set_variable ) > set_variable ).
thf(func_def_170,type,
sK87: ( set_variable > set_variable ) > set_variable ).
thf(func_def_171,type,
sK88: ( set_variable > set_variable ) > set_variable ).
thf(func_def_172,type,
sK89: ( set_variable > set_variable ) > set_variable ).
thf(func_def_173,type,
sK90: ( set_variable > set_variable ) > set_variable ).
thf(func_def_174,type,
sK91: ( set_variable > set_variable ) > set_variable ).
thf(func_def_175,type,
sK92: ( fml > option_fml ) > ( option_fml > $o ) > ( fml > $o ) > fml ).
thf(func_def_176,type,
sK93: ( trm > option_fml ) > ( option_fml > $o ) > ( trm > $o ) > trm ).
thf(func_def_177,type,
sK94: ( trm > option_trm ) > ( option_trm > $o ) > ( trm > $o ) > trm ).
thf(func_def_178,type,
sK95: option_trm > option_trm > option_fml > trm ).
thf(func_def_179,type,
sK96: option_trm > option_trm > option_fml > trm ).
thf(func_def_180,type,
sK97: option_trm > trm ).
thf(func_def_181,type,
sK98: char > set_variable > produc1418842292n_game > trm ).
thf(func_def_182,type,
sK99: char > set_variable > produc1418842292n_game > trm ).
thf(func_def_183,type,
sK100: char > set_variable > produc1418842292n_game > trm ).
thf(func_def_184,type,
sK101: ( variable > $o ) > ( variable > $o ) > set_variable > variable ).
thf(func_def_185,type,
sK102: produc1739631244on_fml > game ).
thf(func_def_186,type,
sK103: produc1739631244on_fml > option_fml ).
thf(func_def_187,type,
sK104: produc1739631244on_fml > game ).
thf(func_def_188,type,
sK105: produc1739631244on_fml > fml ).
thf(func_def_189,type,
sK106: set_variable > ( variable > $o ) > variable ).
thf(func_def_190,type,
db7:
!>[X0: $tType] : X0 ).
thf(func_def_191,type,
db6:
!>[X0: $tType] : X0 ).
thf(func_def_192,type,
db10:
!>[X0: $tType] : X0 ).
thf(func_def_193,type,
db9:
!>[X0: $tType] : X0 ).
thf(func_def_194,type,
db8:
!>[X0: $tType] : X0 ).
thf(func_def_195,type,
db5:
!>[X0: $tType] : X0 ).
thf(func_def_196,type,
sK107: option_game > game ).
thf(func_def_197,type,
sK108: set_variable > set_variable > variable ).
thf(func_def_198,type,
sK109: set_variable > set_variable > variable ).
thf(func_def_199,type,
sK110: set_variable > set_variable > variable ).
thf(func_def_200,type,
sK111: ( variable > $o ) > ( variable > $o ) > variable ).
thf(func_def_201,type,
sK112: set_variable > variable ).
thf(func_def_202,type,
sK113: option_trm > trm ).
thf(func_def_203,type,
sK114: set_variable > variable ).
thf(func_def_204,type,
sK115: ( variable > $o ) > variable ).
thf(func_def_205,type,
sK116: ( variable > $o ) > variable ).
thf(func_def_206,type,
sK117: option_fml > fml ).
thf(func_def_207,type,
sK118: option_game > game ).
thf(func_def_208,type,
sK119: option_trm > trm ).
thf(func_def_209,type,
sK120: option_fml > fml ).
thf(func_def_210,type,
sK121: option_game > game ).
thf(func_def_211,type,
sK122: option_trm > trm ).
thf(func_def_212,type,
sK123: option_fml > fml ).
thf(func_def_213,type,
sK124: set_variable > set_variable > variable ).
thf(func_def_214,type,
sK125: set_variable > set_variable > variable ).
thf(func_def_215,type,
sK126: set_variable > set_variable > variable ).
thf(f3,axiom,
~ ( ( ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) )
@ va )
= bot_bot_set_variable )
=> ( ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) )
= none_fml ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2__092_060open_062_Iif_AFVF_A_Ithe_A_ISPreds_A_092_060sigma_062_Ap_J_J_A_092_060inter_062_AV_A_061_A_123_125_Athen_Ausubstappf_A_Idotsubstt_A_Ithe_A_Iusubstappt_A_092_060sigma_062_AV_A_092_060theta_062_J_J_J_A_123_125_A_Ithe_A_ISPreds_A_092_060sigma_062_Ap_J_J_Aelse_Aundeff_J_A_092_060noteq_062_Aundeff_092_060close_062) ).
thf(f4,axiom,
( ~ ( ( ( ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) )
@ va )
!= bot_bot_set_variable )
=> ( none_fml
= ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) ) ) )
& ( ( ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) )
@ va )
= bot_bot_set_variable )
=> ( ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) )
= ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) ) ) ) )
=> ( ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p )
= none_fml ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3__092_060open_062_Iif_AFVF_A_Ithe_A_ISPreds_A_092_060sigma_062_Ap_J_J_A_092_060inter_062_AV_A_061_A_123_125_Athen_Ausubstappf_A_Idotsubstt_A_Ithe_A_Iusubstappt_A_092_060sigma_062_AV_A_092_060theta_062_J_J_J_A_123_125_A_Ithe_A_ISPreds_A_092_060sigma_062_Ap_J_J_Aelse_Aundeff_J_A_092_060noteq_062_Ausubstappf_A_092_060sigma_062_AV_A_IPred_Ap_A_092_060theta_062_J_A_092_060Longrightarrow_062_ASPreds_A_092_060sigma_062_Ap_A_061_Aundeff_092_060close_062) ).
thf(f7,axiom,
( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) )
!= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) ) )
| ~ ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) )
@ va )
| ~ ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6__092_060open_062vv_AV_A_IFVF_A_Ithe_A_ISPreds_A_092_060sigma_062_Ap_J_J_J_A_092_060notin_062_AFVF_A_Ithe_A_ISPreds_A_092_060sigma_062_Ap_J_J_A_092_060or_062_Avva_AV_A_IFVF_A_Ithe_A_ISPreds_A_092_060sigma_062_Ap_J_J_J_A_092_060notin_062_AV_A_092_060or_062_Avv_AV_A_IFVF_A_Ithe_A_ISPreds_A_092_060sigma_062_Ap_J_J_J_A_092_060noteq_062_Avva_AV_A_IFVF_A_Ithe_A_ISPreds_A_092_060sigma_062_Ap_J_J_J_092_060close_062) ).
thf(f10,axiom,
( produc1250175341on_fml
= ( ^ [X0: ( char > option_trm ) > produc62062515n_game > char > option_fml,X1: produc1418842292n_game,X2: char] :
( produc1499310791on_fml
@ ^ [X3: char > option_trm,X4: produc62062515n_game] : ( X0 @ X3 @ X4 @ X2 )
@ X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_case__prod__app) ).
thf(f12,axiom,
( produc1615133358on_fml
= ( ^ [X0: ( char > option_trm ) > produc799602994n_game > char > option_fml,X1: produc62062515n_game,X2: char] :
( produc154833544on_fml
@ ^ [X3: char > option_trm,X4: produc799602994n_game] : ( X0 @ X3 @ X4 @ X2 )
@ X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_case__prod__app) ).
thf(f14,axiom,
( produc1420172399on_fml
= ( ^ [X0: ( char > option_fml ) > ( char > option_game ) > char > option_fml,X1: produc799602994n_game,X2: char] :
( produc347802313on_fml
@ ^ [X3: char > option_fml,X4: char > option_game] : ( X0 @ X3 @ X4 @ X2 )
@ X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_case__prod__app) ).
thf(f16,axiom,
( ( ( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) )
= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) ) )
& ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) )
@ va )
& ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) ) )
| ( ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) )
@ va )
= bot_bot_set_variable ) )
& ( ! [X4: variable] :
( ! [X5: variable] :
( ( X4 != X5 )
| ~ ( member_variable @ X5 @ va ) )
| ~ ( member_variable @ X4
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) ) )
| ( ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) )
@ va )
!= bot_bot_set_variable ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_f10) ).
thf(f165,axiom,
( inf_inf_variable_o
= ( ^ [X0: variable > $o,X1: variable > $o,X2: variable] : ( inf_inf_o @ ( X0 @ X2 ) @ ( X1 @ X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_164_inf__apply) ).
thf(f177,axiom,
( inf_inf_set_variable
= ( ^ [X0: set_variable,X1: set_variable] :
( collect_variable
@ ( inf_inf_variable_o
@ ^ [X2: variable] : ( member_variable @ X2 @ X0 )
@ ^ [X2: variable] : ( member_variable @ X2 @ X1 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_inf__set__def) ).
thf(f331,axiom,
produc1591622303on_fml = produc347802313on_fml,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_330_internal__case__prod__def) ).
thf(f333,axiom,
produc1903410526on_fml = produc154833544on_fml,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_332_internal__case__prod__def) ).
thf(f335,axiom,
produc724717725on_fml = produc1499310791on_fml,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_334_internal__case__prod__def) ).
thf(f358,conjecture,
( ( ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p )
= none_fml )
| ( ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) )
!= none_fml ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(f359,negated_conjecture,
~ ( ( ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p )
= none_fml )
| ( ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) )
!= none_fml ) ),
inference(negated_conjecture,[status(cth)],[f358]) ).
thf(f362,plain,
~ ( ( ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) )
@ va )
= bot_bot_set_variable )
=> ( ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X4: char > option_trm] :
( produc1615133358on_fml
@ ^ [X5: char > option_trm] :
( produc1420172399on_fml
@ ^ [X6: char > option_fml,X7: char > option_game] : X6 ) )
@ sigma
@ p ) ) )
= none_fml ) ),
inference(rectify,[],[f3]) ).
thf(f363,plain,
~ ( ( bot_bot_set_variable
= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) )
=> ( none_fml
= ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) ),
inference(fool_elimination,[],[f362]) ).
thf(f364,plain,
( ~ ( ( ( ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) )
@ va )
!= bot_bot_set_variable )
=> ( none_fml
= ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) ) ) )
& ( ( ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X4: char > option_trm] :
( produc1615133358on_fml
@ ^ [X5: char > option_trm] :
( produc1420172399on_fml
@ ^ [X6: char > option_fml,X7: char > option_game] : X6 ) )
@ sigma
@ p ) ) )
@ va )
= bot_bot_set_variable )
=> ( ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X8: char > option_trm] :
( produc1615133358on_fml
@ ^ [X9: char > option_trm] :
( produc1420172399on_fml
@ ^ [X10: char > option_fml,X11: char > option_game] : X10 ) )
@ sigma
@ p ) ) )
= ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) ) ) ) )
=> ( ( produc1250175341on_fml
@ ^ [X12: char > option_trm] :
( produc1615133358on_fml
@ ^ [X13: char > option_trm] :
( produc1420172399on_fml
@ ^ [X14: char > option_fml,X15: char > option_game] : X14 ) )
@ sigma
@ p )
= none_fml ) ),
inference(rectify,[],[f4]) ).
thf(f365,plain,
( ~ ( ( ( bot_bot_set_variable
!= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) )
=> ( none_fml
= ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) ) ) )
& ( ( bot_bot_set_variable
= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) )
=> ( ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) )
= ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) ) )
=> ( none_fml
= ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ),
inference(fool_elimination,[],[f364]) ).
thf(f368,plain,
( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) )
!= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X4: char > option_trm] :
( produc1615133358on_fml
@ ^ [X5: char > option_trm] :
( produc1420172399on_fml
@ ^ [X6: char > option_fml,X7: char > option_game] : X6 ) )
@ sigma
@ p ) ) ) ) )
| ~ ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X8: char > option_trm] :
( produc1615133358on_fml
@ ^ [X9: char > option_trm] :
( produc1420172399on_fml
@ ^ [X10: char > option_fml,X11: char > option_game] : X10 ) )
@ sigma
@ p ) ) ) )
@ va )
| ~ ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X12: char > option_trm] :
( produc1615133358on_fml
@ ^ [X13: char > option_trm] :
( produc1420172399on_fml
@ ^ [X14: char > option_fml,X15: char > option_game] : X14 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X16: char > option_trm] :
( produc1615133358on_fml
@ ^ [X17: char > option_trm] :
( produc1420172399on_fml
@ ^ [X18: char > option_fml,X19: char > option_game] : X18 ) )
@ sigma
@ p ) ) ) ) ),
inference(rectify,[],[f7]) ).
thf(f369,plain,
( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
!= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) )
| ( $true
!= ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ va ) )
| ( ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
!= $true ) ),
inference(fool_elimination,[],[f368]) ).
thf(f371,plain,
( produc1250175341on_fml
= ( ^ [X0: ( char > option_trm ) > produc62062515n_game > char > option_fml,X1: produc1418842292n_game,X2: char] :
( produc1499310791on_fml
@ ^ [X3: char > option_trm,X4: produc62062515n_game] : ( X0 @ X3 @ X4 @ X2 )
@ X1 ) ) ),
inference(rectify,[],[f10]) ).
thf(f372,plain,
( produc1250175341on_fml
= ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc1499310791on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 ) ) ),
inference(fool_elimination,[],[f371]) ).
thf(f375,plain,
( produc1615133358on_fml
= ( ^ [X0: ( char > option_trm ) > produc799602994n_game > char > option_fml,X1: produc62062515n_game,X2: char] :
( produc154833544on_fml
@ ^ [X3: char > option_trm,X4: produc799602994n_game] : ( X0 @ X3 @ X4 @ X2 )
@ X1 ) ) ),
inference(rectify,[],[f12]) ).
thf(f376,plain,
( produc1615133358on_fml
= ( ^ [Y0: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y1: produc62062515n_game,Y2: char] :
( produc154833544on_fml
@ ^ [Y3: char > option_trm,Y4: produc799602994n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 ) ) ),
inference(fool_elimination,[],[f375]) ).
thf(f379,plain,
( produc1420172399on_fml
= ( ^ [X0: ( char > option_fml ) > ( char > option_game ) > char > option_fml,X1: produc799602994n_game,X2: char] :
( produc347802313on_fml
@ ^ [X3: char > option_fml,X4: char > option_game] : ( X0 @ X3 @ X4 @ X2 )
@ X1 ) ) ),
inference(rectify,[],[f14]) ).
thf(f380,plain,
( produc1420172399on_fml
= ( ^ [Y0: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y1: produc799602994n_game,Y2: char] :
( produc347802313on_fml
@ ^ [Y3: char > option_fml,Y4: char > option_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 ) ) ),
inference(fool_elimination,[],[f379]) ).
thf(f383,plain,
( ( ( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p ) ) ) )
= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X4: char > option_trm] :
( produc1615133358on_fml
@ ^ [X5: char > option_trm] :
( produc1420172399on_fml
@ ^ [X6: char > option_fml,X7: char > option_game] : X6 ) )
@ sigma
@ p ) ) ) ) )
& ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X8: char > option_trm] :
( produc1615133358on_fml
@ ^ [X9: char > option_trm] :
( produc1420172399on_fml
@ ^ [X10: char > option_fml,X11: char > option_game] : X10 ) )
@ sigma
@ p ) ) ) )
@ va )
& ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X12: char > option_trm] :
( produc1615133358on_fml
@ ^ [X13: char > option_trm] :
( produc1420172399on_fml
@ ^ [X14: char > option_fml,X15: char > option_game] : X14 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X16: char > option_trm] :
( produc1615133358on_fml
@ ^ [X17: char > option_trm] :
( produc1420172399on_fml
@ ^ [X18: char > option_fml,X19: char > option_game] : X18 ) )
@ sigma
@ p ) ) ) ) )
| ( ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X20: char > option_trm] :
( produc1615133358on_fml
@ ^ [X21: char > option_trm] :
( produc1420172399on_fml
@ ^ [X22: char > option_fml,X23: char > option_game] : X22 ) )
@ sigma
@ p ) ) )
@ va )
= bot_bot_set_variable ) )
& ( ! [X24: variable] :
( ! [X25: variable] :
( ( X24 != X25 )
| ~ ( member_variable @ X25 @ va ) )
| ~ ( member_variable @ X24
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X26: char > option_trm] :
( produc1615133358on_fml
@ ^ [X27: char > option_trm] :
( produc1420172399on_fml
@ ^ [X28: char > option_fml,X29: char > option_game] : X28 ) )
@ sigma
@ p ) ) ) ) )
| ( ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [X30: char > option_trm] :
( produc1615133358on_fml
@ ^ [X31: char > option_trm] :
( produc1420172399on_fml
@ ^ [X32: char > option_fml,X33: char > option_game] : X32 ) )
@ sigma
@ p ) ) )
@ va )
!= bot_bot_set_variable ) ) ),
inference(rectify,[],[f16]) ).
thf(f384,plain,
( ( ( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) )
& ( $true
= ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ va ) )
& ( ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
= $true ) )
| ( bot_bot_set_variable
= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) )
& ( ! [X24: variable] :
( ! [X25: variable] :
( ( X24 != X25 )
| ( $true
!= ( member_variable @ X25 @ va ) ) )
| ( $true
!= ( member_variable @ X24
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) ) )
| ( bot_bot_set_variable
!= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ) ),
inference(fool_elimination,[],[f383]) ).
thf(f561,plain,
( inf_inf_variable_o
= ( ^ [Y0: variable > $o,Y1: variable > $o,Y2: variable] : ( inf_inf_o @ ( Y0 @ Y2 ) @ ( Y1 @ Y2 ) ) ) ),
inference(fool_elimination,[],[f165]) ).
thf(f577,plain,
( inf_inf_set_variable
= ( ^ [X0: set_variable,X1: set_variable] :
( collect_variable
@ ( inf_inf_variable_o
@ ^ [X2: variable] : ( member_variable @ X2 @ X0 )
@ ^ [X3: variable] : ( member_variable @ X3 @ X1 ) ) ) ) ),
inference(rectify,[],[f177]) ).
thf(f578,plain,
( inf_inf_set_variable
= ( ^ [Y0: set_variable,Y1: set_variable] :
( collect_variable
@ ( inf_inf_variable_o
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y0 )
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y1 ) ) ) ) ),
inference(fool_elimination,[],[f577]) ).
thf(f829,plain,
~ ( ( ( produc1250175341on_fml
@ ^ [X0: char > option_trm] :
( produc1615133358on_fml
@ ^ [X1: char > option_trm] :
( produc1420172399on_fml
@ ^ [X2: char > option_fml,X3: char > option_game] : X2 ) )
@ sigma
@ p )
= none_fml )
| ( ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) )
!= none_fml ) ),
inference(rectify,[],[f359]) ).
thf(f830,plain,
~ ( ( none_fml
= ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) )
| ( none_fml
!= ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) ) ) ),
inference(fool_elimination,[],[f829]) ).
thf(f831,plain,
( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
!= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) )
| ( $true
!= ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ va ) )
| ( ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
!= $true ) ),
inference(flattening,[],[f369]) ).
thf(f833,plain,
( ( ( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) )
& ( $true
= ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ va ) )
& ( ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
= $true ) )
| ( bot_bot_set_variable
= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) )
& ( ! [X0: variable] :
( ! [X1: variable] :
( ( X0 != X1 )
| ( $true
!= ( member_variable @ X1 @ va ) ) )
| ( $true
!= ( member_variable @ X0
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) ) )
| ( bot_bot_set_variable
!= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ) ),
inference(rectify,[],[f384]) ).
thf(f834,plain,
( ( ( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) )
& ( $true
= ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ va ) )
& ( ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
= $true ) )
| ( bot_bot_set_variable
= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) )
& ( ! [X0: variable] :
( ! [X1: variable] :
( ( X0 != X1 )
| ( $true
!= ( member_variable @ X1 @ va ) ) )
| ( $true
!= ( member_variable @ X0
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) ) )
| ( bot_bot_set_variable
!= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ) ),
inference(flattening,[],[f833]) ).
thf(f851,plain,
( ( none_fml
!= ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
& ( bot_bot_set_variable
= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ),
inference(ennf_transformation,[],[f363]) ).
thf(f852,plain,
( ( none_fml
= ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) )
| ( ( ( none_fml
= ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) ) )
| ( bot_bot_set_variable
= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) )
& ( ( ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) )
= ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
| ( bot_bot_set_variable
!= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ) ) ),
inference(ennf_transformation,[],[f365]) ).
thf(f1055,plain,
( ( none_fml
!= ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) )
& ( none_fml
= ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) ) ) ),
inference(ennf_transformation,[],[f830]) ).
thf(f1164,plain,
( none_fml
!= ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ),
inference(cnf_transformation,[],[f851]) ).
thf(f1165,plain,
( ( none_fml
= ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) )
| ( ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) )
= ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
| ( bot_bot_set_variable
!= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ),
inference(cnf_transformation,[],[f852]) ).
thf(f1169,plain,
( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
!= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) )
| ( $true
!= ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ va ) )
| ( ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
!= $true ) ),
inference(cnf_transformation,[],[f831]) ).
thf(f1172,plain,
( produc1250175341on_fml
= ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc1499310791on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 ) ) ),
inference(cnf_transformation,[],[f372]) ).
thf(f1174,plain,
( produc1615133358on_fml
= ( ^ [Y0: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y1: produc62062515n_game,Y2: char] :
( produc154833544on_fml
@ ^ [Y3: char > option_trm,Y4: produc799602994n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 ) ) ),
inference(cnf_transformation,[],[f376]) ).
thf(f1176,plain,
( produc1420172399on_fml
= ( ^ [Y0: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y1: produc799602994n_game,Y2: char] :
( produc347802313on_fml
@ ^ [Y3: char > option_fml,Y4: char > option_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 ) ) ),
inference(cnf_transformation,[],[f380]) ).
thf(f1179,plain,
( ( ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
= $true )
| ( bot_bot_set_variable
= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ),
inference(cnf_transformation,[],[f834]) ).
thf(f1180,plain,
( ( $true
= ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ va ) )
| ( bot_bot_set_variable
= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ),
inference(cnf_transformation,[],[f834]) ).
thf(f1181,plain,
( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) )
| ( bot_bot_set_variable
= ( inf_inf_set_variable
@ ( static_FVF
@ ( the_fml
@ ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ),
inference(cnf_transformation,[],[f834]) ).
thf(f1401,plain,
( inf_inf_variable_o
= ( ^ [Y0: variable > $o,Y1: variable > $o,Y2: variable] : ( inf_inf_o @ ( Y0 @ Y2 ) @ ( Y1 @ Y2 ) ) ) ),
inference(cnf_transformation,[],[f561]) ).
thf(f1413,plain,
( inf_inf_set_variable
= ( ^ [Y0: set_variable,Y1: set_variable] :
( collect_variable
@ ( inf_inf_variable_o
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y0 )
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y1 ) ) ) ) ),
inference(cnf_transformation,[],[f578]) ).
thf(f1608,plain,
produc347802313on_fml = produc1591622303on_fml,
inference(cnf_transformation,[],[f331]) ).
thf(f1610,plain,
produc154833544on_fml = produc1903410526on_fml,
inference(cnf_transformation,[],[f333]) ).
thf(f1612,plain,
produc1499310791on_fml = produc724717725on_fml,
inference(cnf_transformation,[],[f335]) ).
thf(f1641,plain,
( none_fml
= ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) ) ),
inference(cnf_transformation,[],[f1055]) ).
thf(f1642,plain,
( none_fml
!= ( produc1250175341on_fml
@ ^ [Y0: char > option_trm] :
( produc1615133358on_fml
@ ^ [Y1: char > option_trm] :
( produc1420172399on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ),
inference(cnf_transformation,[],[f1055]) ).
thf(f1645,plain,
( inf_inf_set_variable
= ( ^ [Y0: set_variable,Y1: set_variable] :
( collect_variable
@ ( ^ [Y2: variable > $o,Y3: variable > $o,Y4: variable] : ( inf_inf_o @ ( Y2 @ Y4 ) @ ( Y3 @ Y4 ) )
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y0 )
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y1 ) ) ) ) ),
inference(definition_unfolding,[],[f1413,f1401]) ).
thf(f1646,plain,
( produc1420172399on_fml
= ( ^ [Y0: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y1: produc799602994n_game,Y2: char] :
( produc1591622303on_fml
@ ^ [Y3: char > option_fml,Y4: char > option_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 ) ) ),
inference(definition_unfolding,[],[f1176,f1608]) ).
thf(f1650,plain,
( produc1615133358on_fml
= ( ^ [Y0: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y1: produc62062515n_game,Y2: char] :
( produc1903410526on_fml
@ ^ [Y3: char > option_trm,Y4: produc799602994n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 ) ) ),
inference(definition_unfolding,[],[f1174,f1610]) ).
thf(f1654,plain,
( produc1250175341on_fml
= ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 ) ) ),
inference(definition_unfolding,[],[f1172,f1612]) ).
thf(f1657,plain,
( none_fml
!= ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ),
inference(definition_unfolding,[],[f1164,f1654,f1650,f1646]) ).
thf(f1660,plain,
( ( none_fml
= ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) )
| ( ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) )
= ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
| ( bot_bot_set_variable
!= ( ^ [Y0: set_variable,Y1: set_variable] :
( collect_variable
@ ( ^ [Y2: variable > $o,Y3: variable > $o,Y4: variable] : ( inf_inf_o @ ( Y2 @ Y4 ) @ ( Y3 @ Y4 ) )
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y0 )
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y1 ) ) )
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ),
inference(definition_unfolding,[],[f1165,f1654,f1650,f1646,f1654,f1650,f1646,f1645,f1654,f1650,f1646]) ).
thf(f1662,plain,
( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
!= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) )
| ( $true
!= ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ va ) )
| ( $true
!= ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) ) ),
inference(definition_unfolding,[],[f1169,f1654,f1650,f1646,f1654,f1650,f1646,f1654,f1650,f1646,f1654,f1650,f1646,f1654,f1650,f1646]) ).
thf(f1663,plain,
( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) )
| ( bot_bot_set_variable
= ( ^ [Y0: set_variable,Y1: set_variable] :
( collect_variable
@ ( ^ [Y2: variable > $o,Y3: variable > $o,Y4: variable] : ( inf_inf_o @ ( Y2 @ Y4 ) @ ( Y3 @ Y4 ) )
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y0 )
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y1 ) ) )
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ),
inference(definition_unfolding,[],[f1181,f1654,f1650,f1646,f1654,f1650,f1646,f1645,f1654,f1650,f1646]) ).
thf(f1664,plain,
( ( $true
= ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ va ) )
| ( bot_bot_set_variable
= ( ^ [Y0: set_variable,Y1: set_variable] :
( collect_variable
@ ( ^ [Y2: variable > $o,Y3: variable > $o,Y4: variable] : ( inf_inf_o @ ( Y2 @ Y4 ) @ ( Y3 @ Y4 ) )
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y0 )
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y1 ) ) )
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ),
inference(definition_unfolding,[],[f1180,f1654,f1650,f1646,f1645,f1654,f1650,f1646]) ).
thf(f1665,plain,
( ( $true
= ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) ) ) )
| ( bot_bot_set_variable
= ( ^ [Y0: set_variable,Y1: set_variable] :
( collect_variable
@ ( ^ [Y2: variable > $o,Y3: variable > $o,Y4: variable] : ( inf_inf_o @ ( Y2 @ Y4 ) @ ( Y3 @ Y4 ) )
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y0 )
@ ^ [Y2: variable] : ( member_variable @ Y2 @ Y1 ) ) )
@ ( static_FVF
@ ( the_fml
@ ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ) )
@ va ) ) ),
inference(definition_unfolding,[],[f1179,f1654,f1650,f1646,f1654,f1650,f1646,f1645,f1654,f1650,f1646]) ).
thf(f1933,plain,
( none_fml
!= ( ^ [Y0: ( char > option_trm ) > produc62062515n_game > char > option_fml,Y1: produc1418842292n_game,Y2: char] :
( produc724717725on_fml
@ ^ [Y3: char > option_trm,Y4: produc62062515n_game] : ( Y0 @ Y3 @ Y4 @ Y2 )
@ Y1 )
@ ^ [Y0: char > option_trm] :
( ^ [Y1: ( char > option_trm ) > produc799602994n_game > char > option_fml,Y2: produc62062515n_game,Y3: char] :
( produc1903410526on_fml
@ ^ [Y4: char > option_trm,Y5: produc799602994n_game] : ( Y1 @ Y4 @ Y5 @ Y3 )
@ Y2 )
@ ^ [Y1: char > option_trm] :
( ^ [Y2: ( char > option_fml ) > ( char > option_game ) > char > option_fml,Y3: produc799602994n_game,Y4: char] :
( produc1591622303on_fml
@ ^ [Y5: char > option_fml,Y6: char > option_game] : ( Y2 @ Y5 @ Y6 @ Y4 )
@ Y3 )
@ ^ [Y2: char > option_fml,Y3: char > option_game] : Y2 ) )
@ sigma
@ p ) ),
inference(definition_unfolding,[],[f1642,f1654,f1650,f1646]) ).
thf(f1970,plain,
( none_fml
!= ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ),
inference(beta-eta_normalization,[],[f1933]) ).
thf(f3641,plain,
( ( $true
= ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) ) )
| ( bot_bot_set_variable
= ( collect_variable
@ ^ [Y0: variable] :
( inf_inf_o
@ ( member_variable @ Y0
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y1: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y2: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y3: char > option_fml,Y4: char > option_game] : ( Y3 @ p ) ) )
@ sigma ) ) ) )
@ ( member_variable @ Y0 @ va ) ) ) ) ),
inference(beta-eta_normalization,[],[f1665]) ).
thf(f3642,plain,
( ( $true
= ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) )
@ va ) )
| ( bot_bot_set_variable
= ( collect_variable
@ ^ [Y0: variable] :
( inf_inf_o
@ ( member_variable @ Y0
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y1: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y2: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y3: char > option_fml,Y4: char > option_game] : ( Y3 @ p ) ) )
@ sigma ) ) ) )
@ ( member_variable @ Y0 @ va ) ) ) ) ),
inference(beta-eta_normalization,[],[f1664]) ).
thf(f3643,plain,
( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) )
= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) ) )
| ( bot_bot_set_variable
= ( collect_variable
@ ^ [Y0: variable] :
( inf_inf_o
@ ( member_variable @ Y0
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y1: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y2: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y3: char > option_fml,Y4: char > option_game] : ( Y3 @ p ) ) )
@ sigma ) ) ) )
@ ( member_variable @ Y0 @ va ) ) ) ) ),
inference(beta-eta_normalization,[],[f1663]) ).
thf(f3655,plain,
( ( ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) )
!= ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) ) )
| ( $true
!= ( member_variable
@ ( vva @ va
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) )
@ va ) )
| ( $true
!= ( member_variable
@ ( vv @ va
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) )
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1662]) ).
thf(f3657,plain,
( ( none_fml
= ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) )
| ( ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) )
= ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) )
| ( bot_bot_set_variable
!= ( collect_variable
@ ^ [Y0: variable] :
( inf_inf_o
@ ( member_variable @ Y0
@ ( static_FVF
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y1: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y2: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y3: char > option_fml,Y4: char > option_game] : ( Y3 @ p ) ) )
@ sigma ) ) ) )
@ ( member_variable @ Y0 @ va ) ) ) ) ),
inference(beta-eta_normalization,[],[f1660]) ).
thf(f3660,plain,
( none_fml
!= ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) ),
inference(beta-eta_normalization,[],[f1657]) ).
thf(f3735,plain,
( ( uSubst516392804stappf @ sigma @ va @ ( pred @ p @ theta ) )
= ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) ),
inference(global_subsumption,[],[f3657,f3655,f3643,f3642,f3641,f1970]) ).
thf(f4536,plain,
( none_fml
= ( uSubst516392804stappf @ ( uSubst1408967625substt @ ( the_trm @ ( uSubst516392818stappt @ sigma @ va @ theta ) ) ) @ bot_bot_set_variable
@ ( the_fml
@ ( produc724717725on_fml
@ ^ [Y0: char > option_trm] :
( produc1903410526on_fml
@ ^ [Y1: char > option_trm] :
( produc1591622303on_fml
@ ^ [Y2: char > option_fml,Y3: char > option_game] : ( Y2 @ p ) ) )
@ sigma ) ) ) ),
inference(forward_demodulation,[],[f3735,f1641]) ).
thf(f4537,plain,
$false,
inference(forward_subsumption_resolution,[],[f4536,f3660]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP204^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n014.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 20:11:15 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 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.79/0.45 % (3158121)Will run a generic schedule for satisfiability detection.
% 0.79/0.45 % (3158129)dis+10_1_sil=32000:sp=arity:random_seed=1153350362:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.79/0.45 % (3158127)% WARNING: option uhcvi not known.
% 0.79/0.45 % (3158126)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2511679277_2999 on theBenchmark for (2999ds/0Mi)
% 0.79/0.45 % (3158127)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3324193749:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.79/0.45 % (3158128)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=877608289:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.79/0.45 % (3158130)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1603225421:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.79/0.45 % (3158131)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3647160007:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.79/0.45 % (3158132)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3045957513:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.79/0.45 % (3158129)Instruction limit reached!
% 0.79/0.45 % (3158129)------------------------------
% 0.79/0.45 % (3158129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.45 % (3158129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.45 % (3158129)CaDiCaL version: 2.1.3
% 0.79/0.45 % (3158129)Termination reason: Instruction limit
% 0.79/0.45 % (3158129)Termination phase: Property scanning
% 0.79/0.45 % (3158129)Time elapsed: 0.023 s
% 0.79/0.45 % (3158129)Peak memory usage: 11 MB
% 0.79/0.45 % (3158129)Instructions burned: 105 (million)
% 0.79/0.45 % (3158127)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.79/0.45 % (3158130)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.79/0.45 % (3158140)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3075299571:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.79/0.45 % (3158130)Instruction limit reached!
% 0.79/0.45 % (3158130)------------------------------
% 0.79/0.45 % (3158130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.45 % (3158130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.45 % (3158130)CaDiCaL version: 2.1.3
% 0.79/0.45 % (3158130)Termination reason: Instruction limit
% 0.79/0.45 % (3158130)Termination phase: Property scanning
% 0.79/0.45 % (3158130)Time elapsed: 0.048 s
% 0.79/0.45 % (3158130)Peak memory usage: 11 MB
% 0.79/0.45 % (3158130)Instructions burned: 116 (million)
% 0.79/0.45 % Exception at run slice level
% 0.79/0.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.79/0.45 % Exception at run slice level
% 0.79/0.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.79/0.45 % (3158127)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.79/0.45 % (3158132)Instruction limit reached!
% 0.79/0.45 % (3158132)------------------------------
% 0.79/0.45 % (3158132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.45 % (3158132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.45 % (3158132)CaDiCaL version: 2.1.3
% 0.79/0.45 % (3158132)Termination reason: Instruction limit
% 0.79/0.45 % (3158132)Termination phase: Saturation
% 0.79/0.45 % (3158132)Time elapsed: 0.066 s
% 0.79/0.45 % (3158132)Peak memory usage: 13 MB
% 0.79/0.45 % (3158132)Instructions burned: 161 (million)
% 0.79/0.45 % (3158142)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1020688717:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.79/0.45 % (3158131)Instruction limit reached!
% 0.79/0.45 % (3158131)------------------------------
% 0.79/0.45 % (3158131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.45 % (3158131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.45 % (3158131)CaDiCaL version: 2.1.3
% 0.79/0.45 % (3158131)Termination reason: Instruction limit
% 0.79/0.45 % (3158131)Termination phase: Property scanning
% 0.79/0.45 % (3158131)Time elapsed: 0.068 s
% 0.79/0.45 % (3158131)Peak memory usage: 11 MB
% 0.79/0.45 % (3158131)Instructions burned: 132 (million)
% 0.79/0.45 % (3158143)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=113560020:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.79/0.45 % (3158143)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.79/0.45 % (3158144)ott-21_1_sil=16000:fs=off:random_seed=3477802286:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.79/0.45 % (3158148)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4043887244:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 0.79/0.45 % (3158143)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.79/0.45 % (3158146)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2534940307:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 0.79/0.45 % (3158142)Instruction limit reached!
% 0.79/0.45 % (3158142)------------------------------
% 0.79/0.45 % (3158142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.45 % (3158142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.45 % (3158142)CaDiCaL version: 2.1.3
% 0.79/0.45 % (3158142)Termination reason: Instruction limit
% 0.79/0.45 % (3158142)Termination phase: Property scanning
% 0.79/0.45 % (3158142)Time elapsed: 0.054 s
% 0.79/0.45 % (3158142)Peak memory usage: 11 MB
% 0.79/0.45 % (3158142)Instructions burned: 131 (million)
% 0.79/0.45 % (3158152)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3667890154:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 0.79/0.45 % (3158128) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3158121-3158128"...
% 0.79/0.45 % (3158128)...printing done.
% 0.79/0.45 % (3158128)Refutation found. Thanks to Tanya!
% 0.79/0.45 % SZS status Theorem for theBenchmark
% 0.79/0.45 % SZS output start Proof for theBenchmark
% See solution above
% 0.79/0.46 % (3158128)------------------------------
% 0.79/0.46 % (3158128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.46 % (3158128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.46 % (3158128)CaDiCaL version: 2.1.3
% 0.79/0.46 % (3158128)Termination reason: Refutation
% 0.79/0.46 % (3158128)Time elapsed: 0.162 s
% 0.79/0.46 % (3158128)Peak memory usage: 15 MB
% 0.79/0.46 % (3158128)Instructions burned: 350 (million)
% 0.79/0.46 % (3158121)Success in time 0.22 s
% 0.79/0.46 % Vampire exiting
%------------------------------------------------------------------------------