%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR145^2 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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 07:47:21 AM UTC 2026
% Result : Theorem 0.97s 0.47s
% Output : Refutation 1.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR145^2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n018.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Sep 29 17:59:26 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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.97/0.47 % (428581)Will run a generic schedule for satisfiability detection.
% 0.97/0.47 % (428587)% WARNING: option uhcvi not known.
% 0.97/0.47 % (428587)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2948652797:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.97/0.47 % (428587)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.97/0.47 % (428586)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2688459132_2999 on theBenchmark for (2999ds/0Mi)
% 0.97/0.47 % (428588)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2578773016:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.97/0.47 % (428589)dis+10_1_sil=32000:sp=arity:random_seed=3653222677:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.97/0.47 % (428590)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1812910757:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.97/0.47 % (428587)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.97/0.47 % (428590)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.97/0.47 % (428591)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=877525786:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.97/0.47 % (428592)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3105353941:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.97/0.47 % Exception at run slice level
% 0.97/0.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.97/0.47 % (428600)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3508167319:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.97/0.47 % (428589)Instruction limit reached!
% 0.97/0.47 % (428589)------------------------------
% 0.97/0.47 % (428589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.47 % (428589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.47 % (428589)CaDiCaL version: 2.1.3
% 0.97/0.47 % (428589)Termination reason: Instruction limit
% 0.97/0.47 % (428589)Termination phase: Saturation
% 0.97/0.47 % (428589)Time elapsed: 0.049 s
% 0.97/0.47 % (428589)Peak memory usage: 12 MB
% 0.97/0.47 % (428589)Instructions burned: 104 (million)
% 0.97/0.47 % Exception at run slice level
% 0.97/0.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.97/0.47 % (428590)Instruction limit reached!
% 0.97/0.47 % (428590)------------------------------
% 0.97/0.47 % (428590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.47 % (428590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.47 % (428590)CaDiCaL version: 2.1.3
% 0.97/0.47 % (428590)Termination reason: Instruction limit
% 0.97/0.47 % (428590)Termination phase: Saturation
% 0.97/0.47 % (428590)Time elapsed: 0.053 s
% 0.97/0.47 % (428590)Peak memory usage: 13 MB
% 0.97/0.47 % (428590)Instructions burned: 116 (million)
% 0.97/0.47 % (428602)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2076679484:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.97/0.47 % (428603)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=2687055681:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.97/0.47 % (428604)ott-21_1_sil=16000:fs=off:random_seed=2104787739:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.97/0.47 % (428603)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.97/0.47 % (428603)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.97/0.47 % (428592)Instruction limit reached!
% 0.97/0.47 % (428592)------------------------------
% 0.97/0.47 % (428592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.47 % (428592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.47 % (428592)CaDiCaL version: 2.1.3
% 0.97/0.47 % (428592)Termination reason: Instruction limit
% 0.97/0.47 % (428592)Termination phase: Saturation
% 0.97/0.47 % (428592)Time elapsed: 0.077 s
% 0.97/0.47 % (428592)Peak memory usage: 13 MB
% 0.97/0.47 % (428592)Instructions burned: 160 (million)
% 0.97/0.47 % (428591)Instruction limit reached!
% 0.97/0.47 % (428591)------------------------------
% 0.97/0.47 % (428591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.47 % (428591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.47 % (428591)CaDiCaL version: 2.1.3
% 0.97/0.47 % (428591)Termination reason: Instruction limit
% 0.97/0.47 % (428591)Termination phase: Saturation
% 0.97/0.47 % (428591)Time elapsed: 0.079 s
% 0.97/0.47 % (428591)Peak memory usage: 13 MB
% 0.97/0.47 % (428591)Instructions burned: 131 (million)
% 0.97/0.47 % (428608)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=966339832:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 0.97/0.47 % (428609)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1174914511:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 0.97/0.47 % Exception at run slice level
% 0.97/0.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.97/0.47 % (428602)Instruction limit reached!
% 0.97/0.47 % (428602)------------------------------
% 0.97/0.47 % (428602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.47 % (428602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.47 % (428602)CaDiCaL version: 2.1.3
% 0.97/0.47 % (428602)Termination reason: Instruction limit
% 0.97/0.47 % (428602)Termination phase: Saturation
% 0.97/0.47 % (428602)Time elapsed: 0.069 s
% 0.97/0.47 % (428602)Peak memory usage: 14 MB
% 0.97/0.47 % (428602)Instructions burned: 132 (million)
% 0.97/0.47 % (428612)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3511414646:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 0.97/0.47 % (428613)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2401953730:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 0.97/0.47 % (428604)Instruction limit reached!
% 0.97/0.47 % (428604)------------------------------
% 0.97/0.47 % (428604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.47 % (428604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.47 % (428604)CaDiCaL version: 2.1.3
% 0.97/0.47 % (428604)Termination reason: Instruction limit
% 0.97/0.47 % (428604)Termination phase: Saturation
% 0.97/0.47 % (428604)Time elapsed: 0.097 s
% 0.97/0.47 % (428604)Peak memory usage: 13 MB
% 0.97/0.47 % (428604)Instructions burned: 181 (million)
% 0.97/0.47 % Exception at run slice level
% 0.97/0.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.97/0.47 % (428622)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1834879530:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 0.97/0.47 % (428625)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3869972415:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 0.97/0.47 % (428625)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.97/0.47 % (428622)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.97/0.47 % (428603) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-428581-428603"...
% 0.97/0.47 % (428603)...printing done.
% 0.97/0.47 % (428603)Refutation found. Thanks to Tanya!
% 0.97/0.47 % SZS status Theorem for theBenchmark
% 0.97/0.47 % SZS output start Proof for theBenchmark
% 0.97/0.47 thf(type_def_5, type, num: $tType).
% 0.97/0.47 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.97/0.47 thf(func_def_0, type, agent_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_2, type, believes_THFTYPE_IiooI: ($i > $o > $o)).
% 0.97/0.47 thf(func_def_4, type, containsInformation_THFTYPE_IiooI: ($i > $o > $o)).
% 0.97/0.47 thf(func_def_5, type, contraryAttribute_THFTYPE_IioI: ($i > $o)).
% 0.97/0.47 thf(func_def_6, type, contraryAttribute_THFTYPE_IoooI: ($o > $o > $o)).
% 0.97/0.47 thf(func_def_7, type, disjointDecomposition_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_8, type, disjointDecomposition_THFTYPE_IioI: ($i > $o)).
% 0.97/0.47 thf(func_def_9, type, disjointRelation_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 0.97/0.47 thf(func_def_10, type, disjointRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_11, type, disjoint_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_13, type, domainSubclass_THFTYPE_IIioIiioI: (($i > $o) > $i > $i > $o)).
% 0.97/0.47 thf(func_def_14, type, domainSubclass_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 0.97/0.47 thf(func_def_15, type, domain_THFTYPE_IIIiioIIiioIoIiioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $i > $o)).
% 0.97/0.47 thf(func_def_16, type, domain_THFTYPE_IIIioIiioIiioI: ((($i > $o) > $i > $i > $o) > $i > $i > $o)).
% 0.97/0.47 thf(func_def_17, type, domain_THFTYPE_IIiiIiioI: (($i > $i) > $i > $i > $o)).
% 0.97/0.47 thf(func_def_18, type, domain_THFTYPE_IIiiiIiioI: (($i > $i > $i) > $i > $i > $o)).
% 0.97/0.47 thf(func_def_19, type, domain_THFTYPE_IIiiioIiioI: (($i > $i > $i > $o) > $i > $i > $o)).
% 0.97/0.47 thf(func_def_20, type, domain_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 0.97/0.47 thf(func_def_21, type, domain_THFTYPE_IIioIiioI: (($i > $o) > $i > $i > $o)).
% 0.97/0.47 thf(func_def_22, type, domain_THFTYPE_IIiooIiioI: (($i > $o > $o) > $i > $i > $o)).
% 0.97/0.47 thf(func_def_23, type, domain_THFTYPE_IIoooIiioI: (($o > $o > $o) > $i > $i > $o)).
% 0.97/0.47 thf(func_def_24, type, domain_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 0.97/0.47 thf(func_def_26, type, greaterThanOrEqualTo_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_27, type, greaterThan_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_28, type, gt_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_29, type, gtet_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_30, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 0.97/0.47 thf(func_def_31, type, husband_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_32, type, inList_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_33, type, instance_THFTYPE_IIIiioIIiioIoIioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $o)).
% 0.97/0.47 thf(func_def_34, type, instance_THFTYPE_IIIiioIiioIioI: ((($i > $i > $o) > $i > $i > $o) > $i > $o)).
% 0.97/0.47 thf(func_def_35, type, instance_THFTYPE_IIIioIiioIioI: ((($i > $o) > $i > $i > $o) > $i > $o)).
% 0.97/0.47 thf(func_def_36, type, instance_THFTYPE_IIiIiioIoIioI: (($i > ($i > $i > $o) > $o) > $i > $o)).
% 0.97/0.47 thf(func_def_37, type, instance_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 0.97/0.47 thf(func_def_38, type, instance_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 0.97/0.47 thf(func_def_39, type, instance_THFTYPE_IIiiioIioI: (($i > $i > $i > $o) > $i > $o)).
% 0.97/0.47 thf(func_def_40, type, instance_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 0.97/0.47 thf(func_def_41, type, instance_THFTYPE_IIiooIioI: (($i > $o > $o) > $i > $o)).
% 0.97/0.47 thf(func_def_42, type, instance_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_43, type, instance_THFTYPE_IoioI: ($o > $i > $o)).
% 0.97/0.47 thf(func_def_44, type, instrument_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_45, type, inverse_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 0.97/0.47 thf(func_def_46, type, knows_THFTYPE_IiooI: ($i > $o > $o)).
% 0.97/0.47 thf(func_def_51, type, lBeginFn_THFTYPE_IiiI: ($i > $i)).
% 0.97/0.47 thf(func_def_62, type, lEndFn_THFTYPE_IiiI: ($i > $i)).
% 0.97/0.47 thf(func_def_74, type, lListFn_THFTYPE_IiiI: ($i > $i)).
% 0.97/0.47 thf(func_def_76, type, lListOrderFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 0.97/0.47 thf(func_def_79, type, lMeasureFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 0.97/0.47 thf(func_def_108, type, lWhenFn_THFTYPE_IiiI: ($i > $i)).
% 0.97/0.47 thf(func_def_110, type, lessThanOrEqualTo_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_111, type, lessThan_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_112, type, located_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_113, type, lt_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_114, type, ltet_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_115, type, meetsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_116, type, member_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_121, type, orientation_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 0.97/0.47 thf(func_def_122, type, part_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_123, type, partition_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 0.97/0.47 thf(func_def_125, type, property_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_126, type, range_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_128, type, relatedInternalConcept_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 0.97/0.47 thf(func_def_129, type, relatedInternalConcept_THFTYPE_IIioIIiioIoI: (($i > $o) > ($i > $i > $o) > $o)).
% 0.97/0.47 thf(func_def_130, type, relatedInternalConcept_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 0.97/0.47 thf(func_def_131, type, relatedInternalConcept_THFTYPE_IiIiooIoI: ($i > ($i > $o > $o) > $o)).
% 0.97/0.47 thf(func_def_132, type, relatedInternalConcept_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_135, type, subAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_136, type, subProcess_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_137, type, subclass_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_138, type, subrelation_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 0.97/0.47 thf(func_def_139, type, subrelation_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 0.97/0.47 thf(func_def_140, type, subrelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 0.97/0.47 thf(func_def_141, type, subrelation_THFTYPE_IIoooIIiioIoI: (($o > $o > $o) > ($i > $i > $o) > $o)).
% 0.97/0.47 thf(func_def_142, type, subrelation_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 0.97/0.47 thf(func_def_143, type, subrelation_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_144, type, temporalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_145, type, truth_THFTYPE_IoooI: ($o > $o > $o)).
% 0.97/0.47 thf(func_def_146, type, wife_THFTYPE_IiioI: ($i > $i > $o)).
% 0.97/0.47 thf(func_def_148, type, vNOT: ($o > $o)).
% 0.97/0.47 thf(func_def_151, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.97/0.47 thf(func_def_152, type, vAND: ($o > $o > $o)).
% 0.97/0.47 thf(func_def_153, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.97/0.47 thf(func_def_154, type, sK0: ($i > $o)).
% 0.97/0.47 thf(func_def_155, type, sK1: (($i > $i > $o) > $i)).
% 0.97/0.47 thf(func_def_156, type, sK2: (($i > $i > $o) > $i)).
% 0.97/0.47 thf(func_def_157, type, sK3: (($i > $i > $o) > $i)).
% 0.97/0.47 thf(func_def_160, type, sK6: (($i > $i > $o) > $i)).
% 0.97/0.47 thf(func_def_161, type, sK7: ($i > $i)).
% 0.97/0.47 thf(func_def_162, type, sK8: (($i > $i > $o) > $i)).
% 0.97/0.47 thf(func_def_163, type, sK9: (($i > $i > $o) > $i)).
% 0.97/0.47 thf(func_def_164, type, sK10: ($i > $i)).
% 0.97/0.47 thf(func_def_165, type, sK11: ($i > $i > $i)).
% 0.97/0.47 thf(func_def_167, type, sK13: ($i > $i > $i)).
% 0.97/0.47 thf(func_def_168, type, sK14: ($i > $i)).
% 0.97/0.47 thf(func_def_169, type, sK15: ($i > $i > $i)).
% 0.97/0.47 thf(func_def_170, type, db0: !>[X0: $tType]:(X0)).
% 0.97/0.47 thf(func_def_171, type, db1: !>[X0: $tType]:(X0)).
% 0.97/0.47 thf(func_def_173, type, db2: !>[X0: $tType]:(X0)).
% 0.97/0.47 thf(f32,axiom,(
% 0.97/0.47 ! [X0 : ($i > $i > $o)] : ((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i) <=> ! [X1 : $i] : (~ (X0 @ X1 @ X1)))),
% 0.97/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_031)).
% 0.97/0.47 thf(f96,axiom,(
% 0.97/0.47 (wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i)),
% 0.97/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_095)).
% 0.97/0.47 thf(f172,axiom,(
% 0.97/0.47 (instance_THFTYPE_IIiioIioI @ wife_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)),
% 0.97/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_171)).
% 0.97/0.47 thf(f317,conjecture,(
% 0.97/0.47 ? [X0 : ($i > $i > $o)] : ((~ (X0 = (^[X1 : $i, X2 : $i] : ($true)))) & (X0 @ lChris_THFTYPE_i @ lCorina_THFTYPE_i))),
% 0.97/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 0.97/0.47 thf(f318,negated_conjecture,(
% 0.97/0.47 ~ ? [X0 : ($i > $i > $o)] : ((~ (X0 = (^[X1 : $i, X2 : $i] : ($true)))) & (X0 @ lChris_THFTYPE_i @ lCorina_THFTYPE_i))),
% 0.97/0.47 inference(negated_conjecture,[status(cth)],[f317])).
% 0.97/0.47 thf(f381,plain,(
% 0.97/0.47 ! [X0 : ($i > $i > $o)] : ((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i) <=> ! [X1 : $i] : (~ (X0 @ X1 @ X1)))),
% 0.97/0.47 inference(rectify,[],[f32])).
% 0.97/0.47 thf(f382,plain,(
% 0.97/0.47 ! [X0 : ($i > $i > $o)] : ((((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) = $true) <=> ! [X1 : $i] : (((~ (X0 @ X1 @ X1))) = $true))),
% 0.97/0.47 inference(fool_elimination,[],[f381])).
% 0.97/0.47 thf(f507,plain,(
% 0.97/0.47 (wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i)),
% 0.97/0.47 inference(rectify,[],[f96])).
% 0.97/0.47 thf(f508,plain,(
% 0.97/0.47 (((wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i)) = $true)),
% 0.97/0.47 inference(fool_elimination,[],[f507])).
% 0.97/0.47 thf(f657,plain,(
% 0.97/0.47 (instance_THFTYPE_IIiioIioI @ wife_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)),
% 0.97/0.47 inference(rectify,[],[f172])).
% 0.97/0.47 thf(f658,plain,(
% 0.97/0.47 (((instance_THFTYPE_IIiioIioI @ wife_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)) = $true)),
% 0.97/0.47 inference(fool_elimination,[],[f657])).
% 0.97/0.47 thf(f947,plain,(
% 0.97/0.47 ~ ? [X0 : ($i > $i > $o)] : ((~ (X0 = (^[X1 : $i, X2 : $i] : ($true)))) & (X0 @ lChris_THFTYPE_i @ lCorina_THFTYPE_i))),
% 0.97/0.47 inference(rectify,[],[f318])).
% 0.97/0.47 thf(f948,plain,(
% 0.97/0.47 ~ ? [X0 : ($i > $i > $o)] : (($true = ((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))) & (((X0 @ lChris_THFTYPE_i @ lCorina_THFTYPE_i)) = $true))),
% 1.68/0.48 inference(fool_elimination,[],[f947])).
% 1.68/0.48 thf(f1029,plain,(
% 1.68/0.48 ! [X0 : ($i > $i > $o)] : (($true != ((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))) | (((X0 @ lChris_THFTYPE_i @ lCorina_THFTYPE_i)) != $true))),
% 1.68/0.48 inference(ennf_transformation,[],[f948])).
% 1.68/0.48 thf(f1038,plain,(
% 1.68/0.48 ! [X0 : ($i > $i > $o)] : (((((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) = $true) | ? [X1 : $i] : (((~ (X0 @ X1 @ X1))) != $true)) & (! [X1 : $i] : (((~ (X0 @ X1 @ X1))) = $true) | (((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) != $true)))),
% 1.68/0.48 inference(nnf_transformation,[],[f382])).
% 1.68/0.48 thf(f1039,plain,(
% 1.68/0.48 ! [X0 : ($i > $i > $o)] : (((((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) = $true) | ? [X1 : $i] : (((~ (X0 @ X1 @ X1))) != $true)) & (! [X2 : $i] : ($true = ((~ (X0 @ X2 @ X2)))) | (((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) != $true)))),
% 1.68/0.48 inference(rectify,[],[f1038])).
% 1.68/0.48 thf(f1040,plain,(
% 1.68/0.48 ! [X0 : ($i > $i > $o)] : (((((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) = $true) | ($true != ((~ (X0 @ (sK6 @ X0) @ (sK6 @ X0)))))) & (! [X2 : $i] : ($true = ((~ (X0 @ X2 @ X2)))) | (((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) != $true)))),
% 1.68/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X1,sK0 @ X0)],[f1039])).
% 1.68/0.48 thf(f1096,plain,(
% 1.68/0.48 ( ! [X2 : $i,X0 : ($i > $i > $o)] : (($true = ((~ (X0 @ X2 @ X2)))) | (((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) != $true)) )),
% 1.68/0.48 inference(cnf_transformation,[],[f1040])).
% 1.68/0.48 thf(f1168,plain,(
% 1.68/0.48 (((wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ lChris_THFTYPE_i)) = $true)),
% 1.68/0.48 inference(cnf_transformation,[],[f508])).
% 1.68/0.48 thf(f1246,plain,(
% 1.68/0.48 (((instance_THFTYPE_IIiioIioI @ wife_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)) = $true)),
% 1.68/0.48 inference(cnf_transformation,[],[f658])).
% 1.68/0.48 thf(f1391,plain,(
% 1.68/0.48 ( ! [X0 : ($i > $i > $o)] : (($true != ((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))) | (((X0 @ lChris_THFTYPE_i @ lCorina_THFTYPE_i)) != $true)) )),
% 1.68/0.48 inference(cnf_transformation,[],[f1029])).
% 1.68/0.48 thf(f1404,plain,(
% 1.68/0.48 ( ! [X0 : ($i > $i > $o)] : (($true = ((X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))) | (((X0 @ lChris_THFTYPE_i @ lCorina_THFTYPE_i)) != $true)) )),
% 1.68/0.48 inference(not_proxy_clausification,[],[f1391])).
% 1.68/0.48 thf(f1405,plain,(
% 1.68/0.48 ( ! [X0 : ($i > $i > $o)] : ((((X0 @ lChris_THFTYPE_i @ lCorina_THFTYPE_i)) != $true) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0)) )),
% 1.68/0.48 inference(equality_proxy_clausification,[],[f1404])).
% 1.68/0.48 thf(f1423,plain,(
% 1.68/0.48 ( ! [X2 : $i,X0 : ($i > $i > $o)] : ((((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) != $true) | ($false = ((X0 @ X2 @ X2)))) )),
% 1.68/0.48 inference(not_proxy_clausification,[],[f1096])).
% 1.68/0.48 thf(f1439,plain,(
% 1.68/0.48 ($true != (((^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))) @ lChris_THFTYPE_i @ lCorina_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))))),
% 1.68/0.48 inference(primitive_instantiation,[],[f1405])).
% 1.68/0.48 thf(f1440,plain,(
% 1.68/0.48 ($true != (((^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1))))) @ lChris_THFTYPE_i @ lCorina_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1))))))),
% 1.68/0.48 inference(primitive_instantiation,[],[f1405])).
% 1.68/0.48 thf(f1448,plain,(
% 1.68/0.48 ($true != ((~ (lChris_THFTYPE_i = lCorina_THFTYPE_i)))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1))))))),
% 1.68/0.48 inference(beta-eta_normalization,[],[f1440])).
% 1.68/0.48 thf(f1449,plain,(
% 1.68/0.48 ($true = ((lChris_THFTYPE_i = lCorina_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1))))))),
% 1.68/0.48 inference(not_proxy_clausification,[],[f1448])).
% 1.68/0.48 thf(f1450,plain,(
% 1.68/0.48 (lChris_THFTYPE_i = lCorina_THFTYPE_i) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1))))))),
% 1.68/0.48 inference(equality_proxy_clausification,[],[f1449])).
% 1.68/0.48 thf(f1451,plain,(
% 1.68/0.48 ($true != ((lChris_THFTYPE_i = lCorina_THFTYPE_i))) | (= = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))),
% 1.68/0.48 inference(beta-eta_normalization,[],[f1439])).
% 1.68/0.48 thf(f1452,plain,(
% 1.68/0.48 (lChris_THFTYPE_i != lCorina_THFTYPE_i) | (= = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))),
% 1.68/0.48 inference(equality_proxy_clausification,[],[f1451])).
% 1.68/0.48 thf(f1463,definition,(
% 1.68/0.48 spl16_3 <=> ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1))))))),
% 1.68/0.48 introduced(definition,[new_symbols(definition,[spl16_3])],[avatar_definition])).
% 1.68/0.48 thf(f1465,plain,(
% 1.68/0.48 ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1)))))) | ~spl16_3),
% 1.68/0.48 inference(avatar_component_clause,[],[f1463])).
% 1.68/0.48 thf(f1467,definition,(
% 1.68/0.48 spl16_4 <=> (lChris_THFTYPE_i = lCorina_THFTYPE_i)),
% 1.68/0.48 introduced(definition,[new_symbols(definition,[spl16_4])],[avatar_definition])).
% 1.68/0.48 thf(f1470,plain,(
% 1.68/0.48 spl16_3 | spl16_4),
% 1.68/0.48 inference(avatar_split_clause,[],[f1450,f1467,f1463])).
% 1.68/0.48 thf(f1472,definition,(
% 1.68/0.48 spl16_5 <=> (= = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))),
% 1.68/0.48 introduced(definition,[new_symbols(definition,[spl16_5])],[avatar_definition])).
% 1.68/0.48 thf(f1474,plain,(
% 1.68/0.48 (= = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | ~spl16_5),
% 1.68/0.48 inference(avatar_component_clause,[],[f1472])).
% 1.68/0.48 thf(f1475,plain,(
% 1.68/0.48 spl16_5 | ~spl16_4),
% 1.68/0.48 inference(avatar_split_clause,[],[f1452,f1467,f1472])).
% 1.68/0.48 thf(f1486,plain,(
% 1.68/0.48 ( ! [X1 : $i] : ((((= @ X1)) = (((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) @ X1)))) ) | ~spl16_5),
% 1.68/0.48 inference(argument_congruence,[],[f1474])).
% 1.68/0.48 thf(f1487,plain,(
% 1.68/0.48 ( ! [X1 : $i] : ((((= @ X1)) = (^[Y0 : $i]: ($true)))) ) | ~spl16_5),
% 1.68/0.48 inference(beta-eta_normalization,[],[f1486])).
% 1.68/0.48 thf(f1493,plain,(
% 1.68/0.48 ( ! [X2 : $i,X1 : $i] : ((((X1 = X2)) = (((^[Y0 : $i]: ($true)) @ X2)))) ) | ~spl16_5),
% 1.68/0.48 inference(argument_congruence,[],[f1487])).
% 1.68/0.48 thf(f1494,plain,(
% 1.68/0.48 ( ! [X2 : $i,X1 : $i] : (($true = ((X1 = X2))) | ($false = (((^[Y0 : $i]: ($true)) @ X2)))) ) | ~spl16_5),
% 1.68/0.48 inference(iff_proxy_clausification,[],[f1493])).
% 1.68/0.48 thf(f1498,plain,(
% 1.68/0.48 ( ! [X2 : $i,X1 : $i] : ((X1 = X2) | ($false = (((^[Y0 : $i]: ($true)) @ X2)))) ) | ~spl16_5),
% 1.68/0.48 inference(equality_proxy_clausification,[],[f1494])).
% 1.68/0.48 thf(f1499,plain,(
% 1.68/0.48 ( ! [X2 : $i,X1 : $i] : ((X1 = X2) | ($true = $false)) ) | ~spl16_5),
% 1.68/0.48 inference(beta-eta_normalization,[],[f1498])).
% 1.68/0.48 thf(f1500,plain,(
% 1.68/0.48 ( ! [X2 : $i,X1 : $i] : ((X1 = X2)) ) | ~spl16_5),
% 1.68/0.48 inference(trivial_inequality_removal,[],[f1499])).
% 1.68/0.48 thf(f1535,plain,(
% 1.68/0.48 ( ! [X0 : $i] : (($true = ((wife_THFTYPE_IiioI @ lCorina_THFTYPE_i @ X0)))) ) | ~spl16_5),
% 1.68/0.48 inference(constrained_superposition,[],[f1168,f1500])).
% 1.68/0.48 thf(f1604,plain,(
% 1.68/0.48 ( ! [X0 : $i,X1 : $i] : (($true = ((wife_THFTYPE_IiioI @ X0 @ X1)))) ) | ~spl16_5),
% 1.68/0.48 inference(constrained_superposition,[],[f1535,f1500])).
% 1.68/0.48 thf(f2835,plain,(
% 1.68/0.48 ( ! [X0 : $i] : (($true != $true) | ($false = ((wife_THFTYPE_IiioI @ X0 @ X0)))) )),
% 1.68/0.48 inference(constrained_superposition,[],[f1423,f1246])).
% 1.68/0.48 thf(f2836,plain,(
% 1.68/0.48 ( ! [X0 : $i] : (($false = ((wife_THFTYPE_IiioI @ X0 @ X0)))) )),
% 1.68/0.48 inference(trivial_inequality_removal,[],[f2835])).
% 1.68/0.48 thf(f2839,plain,(
% 1.68/0.48 ($true = $false) | ~spl16_5),
% 1.68/0.48 inference(forward_demodulation,[],[f2836,f1604])).
% 1.68/0.48 thf(f2840,plain,(
% 1.68/0.48 $false | ~spl16_5),
% 1.68/0.48 inference(trivial_inequality_removal,[],[f2839])).
% 1.68/0.48 thf(f2841,plain,(
% 1.68/0.48 ~spl16_5),
% 1.68/0.48 inference(avatar_contradiction_clause,[],[f2840])).
% 1.68/0.48 thf(f3203,plain,(
% 1.68/0.48 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) @ X1)) = (((^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1))))) @ X1)))) ) | ~spl16_3),
% 1.68/0.48 inference(argument_congruence,[],[f1465])).
% 1.68/0.48 thf(f3204,plain,(
% 1.68/0.48 ( ! [X1 : $i] : (((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: (~ (X1 = Y0))))) ) | ~spl16_3),
% 1.68/0.48 inference(beta-eta_normalization,[],[f3203])).
% 1.68/0.48 thf(f3223,plain,(
% 1.68/0.48 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ($true)) @ X2)) = (((^[Y0 : $i]: (~ (X1 = Y0))) @ X2)))) ) | ~spl16_3),
% 1.68/0.48 inference(argument_congruence,[],[f3204])).
% 1.68/0.48 thf(f3225,plain,(
% 1.68/0.48 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ($true)) @ X2))) | ($true = (((^[Y0 : $i]: (~ (X1 = Y0))) @ X2)))) ) | ~spl16_3),
% 1.68/0.48 inference(iff_proxy_clausification,[],[f3223])).
% 1.68/0.48 thf(f3226,plain,(
% 1.68/0.48 ( ! [X2 : $i,X1 : $i] : (($true = $false) | ($true = ((~ (X1 = X2))))) ) | ~spl16_3),
% 1.68/0.48 inference(beta-eta_normalization,[],[f3225])).
% 1.68/0.48 thf(f3227,plain,(
% 1.68/0.48 ( ! [X2 : $i,X1 : $i] : (($true = $false) | ($false = ((X1 = X2)))) ) | ~spl16_3),
% 1.68/0.48 inference(not_proxy_clausification,[],[f3226])).
% 1.68/0.48 thf(f3228,plain,(
% 1.68/0.48 ( ! [X2 : $i,X1 : $i] : (($true = $false) | (X1 != X2)) ) | ~spl16_3),
% 1.68/0.48 inference(equality_proxy_clausification,[],[f3227])).
% 1.68/0.48 thf(f3229,plain,(
% 1.68/0.48 ( ! [X2 : $i,X1 : $i] : ((X1 != X2)) ) | ~spl16_3),
% 1.68/0.48 inference(trivial_inequality_removal,[],[f3228])).
% 1.68/0.48 thf(f3230,plain,(
% 1.68/0.48 $false | ~spl16_3),
% 1.68/0.48 inference(flex-flex_simplification,[],[f3229])).
% 1.68/0.48 thf(f3231,plain,(
% 1.68/0.48 ~spl16_3),
% 1.68/0.48 inference(avatar_contradiction_clause,[],[f3230])).
% 1.68/0.48 cnf(s2, plain, spl16_3 | spl16_4, inference(sat_conversion,[],[f1470])).
% 1.68/0.48 cnf(s3, plain, ~spl16_4 | spl16_5, inference(sat_conversion,[],[f1475])).
% 1.68/0.48 cnf(s40, plain, ~spl16_5, inference(sat_conversion,[],[f2841])).
% 1.68/0.48 cnf(s50, plain, ~spl16_3, inference(sat_conversion,[],[f3231])).
% 1.68/0.48 cnf(s53, plain, ~spl16_4, inference(rat,[],[s3,s40])).
% 1.68/0.48 cnf(s54, plain, $false, inference(rat,[],[s2,s53,s50])).
% 1.68/0.48 thf(f3235,plain,(
% 1.68/0.48 $false),
% 1.68/0.48 inference(avatar_sat_refutation,[],[s54])).
% 1.68/0.48 % SZS output end Proof for theBenchmark
% 1.68/0.48 % (428603)------------------------------
% 1.68/0.48 % (428603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.68/0.48 % (428603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.68/0.48 % (428603)CaDiCaL version: 2.1.3
% 1.68/0.48 % (428603)Termination reason: Refutation
% 1.68/0.48 % (428603)Time elapsed: 0.140 s
% 1.68/0.48 % (428603)Peak memory usage: 15 MB
% 1.68/0.48 % (428603)Instructions burned: 276 (million)
% 1.68/0.48 % (428581)Success in time 0.26 s
% 1.68/0.48 % Vampire exiting
%------------------------------------------------------------------------------