%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : CSR045+2 : TPTP v8.1.2. Released v3.4.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Aug 30 21:36:45 EDT 2023 % Result : Theorem 179.23s 24.13s % Output : Proof 200.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.08 % Problem : CSR045+2 : TPTP v8.1.2. Released v3.4.0. % 0.07/0.09 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.08/0.28 % Computer : n020.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Mon Aug 28 13:07:13 EDT 2023 % 0.08/0.28 % CPUTime : % 0.12/0.54 ________ _____ % 0.12/0.54 ___ __ \_________(_)________________________________ % 0.12/0.54 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.12/0.54 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.12/0.54 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.12/0.54 % 0.12/0.54 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.12/0.54 (2023-06-19) % 0.12/0.54 % 0.12/0.54 (c) Philipp Rümmer, 2009-2023 % 0.12/0.54 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.12/0.54 Amanda Stjerna. % 0.12/0.54 Free software under BSD-3-Clause. % 0.12/0.54 % 0.12/0.54 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.12/0.54 % 0.12/0.54 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.12/0.55 Running up to 7 provers in parallel. % 0.12/0.56 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.12/0.56 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.12/0.56 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.12/0.56 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.12/0.56 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.12/0.56 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.12/0.56 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 12.62/2.50 Prover 1: Preprocessing ... % 13.79/2.57 Prover 2: Preprocessing ... % 13.79/2.57 Prover 3: Preprocessing ... % 13.79/2.58 Prover 0: Preprocessing ... % 13.79/2.59 Prover 4: Preprocessing ... % 14.27/2.65 Prover 5: Preprocessing ... % 14.60/2.68 Prover 6: Preprocessing ... % 34.71/5.34 Prover 5: Proving ... % 34.98/5.38 Prover 2: Proving ... % 36.44/5.60 Prover 6: Constructing countermodel ... % 36.88/5.64 Prover 3: Constructing countermodel ... % 39.32/6.02 Prover 1: Constructing countermodel ... % 44.04/6.58 Prover 4: Constructing countermodel ... % 50.44/7.45 Prover 0: Proving ... % 83.19/11.72 Prover 2: stopped % 83.19/11.73 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 87.17/12.22 Prover 7: Preprocessing ... % 91.47/12.83 Prover 7: Constructing countermodel ... % 100.29/13.89 Prover 5: stopped % 100.29/13.90 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 104.01/14.36 Prover 8: Preprocessing ... % 111.12/15.29 Prover 8: Warning: ignoring some quantifiers % 111.83/15.35 Prover 8: Constructing countermodel ... % 116.21/15.93 Prover 1: stopped % 116.21/15.94 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 119.44/16.37 Prover 9: Preprocessing ... % 127.54/17.38 Prover 9: Constructing countermodel ... % 130.63/17.81 Prover 6: stopped % 130.63/17.81 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 133.76/18.25 Prover 10: Preprocessing ... % 137.13/18.67 Prover 10: Constructing countermodel ... % 179.23/24.13 Prover 9: proved (8180ms) % 179.23/24.13 % 179.23/24.13 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 179.23/24.13 % 179.50/24.13 Prover 3: stopped % 179.50/24.13 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 179.53/24.14 Prover 0: stopped % 179.53/24.14 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 179.53/24.15 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 181.97/24.50 Prover 16: Preprocessing ... % 181.97/24.50 Prover 13: Preprocessing ... % 181.97/24.53 Prover 11: Preprocessing ... % 185.23/24.91 Prover 13: Warning: ignoring some quantifiers % 185.23/24.91 Prover 16: Warning: ignoring some quantifiers % 185.23/24.94 Prover 13: Constructing countermodel ... % 185.23/24.95 Prover 16: Constructing countermodel ... % 190.76/25.62 Prover 11: Constructing countermodel ... % 199.63/26.80 Prover 10: Found proof (size 41) % 199.63/26.80 Prover 10: proved (8990ms) % 199.63/26.80 Prover 7: stopped % 199.63/26.80 Prover 11: stopped % 199.63/26.80 Prover 13: stopped % 199.63/26.80 Prover 16: stopped % 199.63/26.80 Prover 4: stopped % 199.63/26.80 Prover 8: stopped % 199.63/26.80 % 199.63/26.81 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 199.63/26.81 % 199.63/26.81 % SZS output start Proof for theBenchmark % 199.63/26.83 Assumptions after simplification: % 199.63/26.83 --------------------------------- % 199.63/26.83 % 199.63/26.83 (ax1_1014) % 199.99/26.84 $i(c_individual) & ! [v0: $i] : ( ~ $i(v0) | ~ individual(v0) | isa(v0, % 199.99/26.84 c_individual)) % 199.99/26.84 % 199.99/26.84 (ax1_1016) % 199.99/26.84 $i(c_partiallyintangibleindividual) & ! [v0: $i] : ( ~ $i(v0) | ~ % 199.99/26.84 partiallyintangibleindividual(v0) | isa(v0, % 199.99/26.84 c_partiallyintangibleindividual)) % 199.99/26.84 % 199.99/26.84 (ax1_1079) % 199.99/26.84 $i(c_microtheory) & ! [v0: $i] : ( ~ $i(v0) | ~ microtheory(v0) | isa(v0, % 199.99/26.84 c_microtheory)) % 199.99/26.84 % 199.99/26.84 (ax1_1094) % 199.99/26.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 199.99/26.84 ~ isa(v0, v1) | ~ genls(v1, v2) | isa(v0, v2)) % 199.99/26.84 % 199.99/26.84 (ax1_1107) % 199.99/26.84 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ genls(v0, v1) | % 199.99/26.84 collection(v0)) % 199.99/26.84 % 199.99/26.84 (ax1_1108) % 199.99/26.84 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ genls(v0, v1) | % 199.99/26.84 collection(v0)) % 199.99/26.84 % 199.99/26.84 (ax1_1112) % 199.99/26.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 199.99/26.84 ~ genls(v2, v0) | ~ genls(v0, v1) | genls(v2, v1)) % 199.99/26.84 % 199.99/26.84 (ax1_1121) % 199.99/26.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 199.99/26.84 ~ genls(v2, v1) | ~ disjointwith(v0, v1) | disjointwith(v0, v2)) % 199.99/26.84 % 199.99/26.84 (ax1_126) % 200.12/26.87 $i(s_terroristthathasbeenamemberofaterroristorganization) & % 200.12/26.87 $i(c_terroristgroup) & $i(c_hasmembers) & $i(c_terrorist) & $i(c_englishmt) & % 200.12/26.87 ? [v0: $i] : ( ~ mtvisible(c_englishmt) | % 200.12/26.87 (f_subcollectionofwithrelationfromtypefn(c_terrorist, c_hasmembers, % 200.12/26.87 c_terroristgroup) = v0 & $i(v0) & prettystring(v0, % 200.12/26.87 s_terroristthathasbeenamemberofaterroristorganization))) % 200.12/26.87 % 200.12/26.87 (ax1_155) % 200.12/26.87 $i(c_aspatialinformationstore) & $i(c_microtheory) & genls(c_microtheory, % 200.12/26.87 c_aspatialinformationstore) % 200.12/26.87 % 200.12/26.87 (ax1_170) % 200.12/26.87 $i(c_applicationcontext) & $i(c_microtheory) & genls(c_applicationcontext, % 200.12/26.87 c_microtheory) % 200.12/26.87 % 200.12/26.87 (ax1_229) % 200.12/26.87 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ genls(v0, v1) | % 200.12/26.87 collection(v0)) % 200.12/26.87 % 200.12/26.87 (ax1_290) % 200.12/26.87 $i(c_collection) & $i(c_individual) & disjointwith(c_collection, c_individual) % 200.12/26.87 % 200.12/26.87 (ax1_319) % 200.12/26.87 $i(c_intangibleindividual) & $i(c_partiallyintangibleindividual) & % 200.12/26.87 genls(c_intangibleindividual, c_partiallyintangibleindividual) % 200.12/26.87 % 200.12/26.87 (ax1_32) % 200.12/26.87 $i(c_individual) & $i(c_partiallyintangibleindividual) & % 200.12/26.87 genls(c_partiallyintangibleindividual, c_individual) % 200.12/26.87 % 200.12/26.87 (ax1_363) % 200.12/26.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 200.12/26.87 ~ isa(v0, v2) | ~ isa(v0, v1) | ~ disjointwith(v1, v2)) % 200.12/26.87 % 200.12/26.87 (ax1_381) % 200.12/26.87 $i(c_intangibleindividual) & $i(c_aspatialinformationstore) & % 200.12/26.87 genls(c_aspatialinformationstore, c_intangibleindividual) % 200.12/26.87 % 200.12/26.87 (ax1_452) % 200.12/26.87 $i(s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege) & % 200.12/26.87 $i(c_beloitcollege) & $i(c_affiliatedwith) & $i(c_footballteam) & % 200.12/26.87 $i(c_englishmt) & ? [v0: $i] : ( ~ mtvisible(c_englishmt) | % 200.12/26.87 (f_instancewithrelationtofn(c_footballteam, c_affiliatedwith, % 200.12/26.87 c_beloitcollege) = v0 & $i(v0) & prettystring(v0, % 200.12/26.87 s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege))) % 200.12/26.87 % 200.12/26.87 (ax1_607) % 200.12/26.87 $i(c_intangibleindividual) & ! [v0: $i] : ( ~ $i(v0) | ~ % 200.12/26.87 intangibleindividual(v0) | isa(v0, c_intangibleindividual)) % 200.12/26.87 % 200.12/26.87 (ax1_812) % 200.12/26.87 $i(c_aspatialinformationstore) & ! [v0: $i] : ( ~ $i(v0) | ~ % 200.12/26.87 aspatialinformationstore(v0) | isa(v0, c_aspatialinformationstore)) % 200.12/26.87 % 200.12/26.87 (ax1_814) % 200.12/26.87 $i(c_collection) & ! [v0: $i] : ( ~ $i(v0) | ~ collection(v0) | isa(v0, % 200.12/26.87 c_collection)) % 200.12/26.87 % 200.12/26.87 (ax1_83) % 200.12/26.87 $i(c_wamt_evalinitial_p14) & applicationcontext(c_wamt_evalinitial_p14) % 200.12/26.87 % 200.12/26.87 (ax1_930) % 200.12/26.88 $i(c_applicationcontext) & ! [v0: $i] : ( ~ $i(v0) | ~ % 200.12/26.88 applicationcontext(v0) | isa(v0, c_applicationcontext)) % 200.12/26.88 % 200.12/26.88 (query95) % 200.12/26.88 $i(c_tptpcol_15_80088) & $i(c_wamt_evalinitial_p14) & % 200.12/26.88 genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088) % 200.12/26.88 % 200.12/26.88 Further assumptions not needed in the proof: % 200.12/26.88 -------------------------------------------- % 200.12/26.88 ax1_1, ax1_10, ax1_100, ax1_1000, ax1_1001, ax1_1002, ax1_1003, ax1_1004, % 200.12/26.88 ax1_1005, ax1_1006, ax1_1007, ax1_1008, ax1_1009, ax1_101, ax1_1010, ax1_1011, % 200.12/26.88 ax1_1012, ax1_1013, ax1_1015, ax1_1017, ax1_1018, ax1_1019, ax1_102, ax1_1020, % 200.12/26.88 ax1_1021, ax1_1022, ax1_1023, ax1_1024, ax1_1025, ax1_1026, ax1_1027, ax1_1028, % 200.12/26.88 ax1_1029, ax1_103, ax1_1030, ax1_1031, ax1_1032, ax1_1033, ax1_1034, ax1_1035, % 200.12/26.88 ax1_1036, ax1_1037, ax1_1038, ax1_1039, ax1_104, ax1_1040, ax1_1041, ax1_1042, % 200.12/26.88 ax1_1043, ax1_1044, ax1_1045, ax1_1046, ax1_1047, ax1_1048, ax1_1049, ax1_105, % 200.12/26.88 ax1_1050, ax1_1051, ax1_1052, ax1_1053, ax1_1054, ax1_1055, ax1_1056, ax1_1057, % 200.12/26.88 ax1_1058, ax1_1059, ax1_106, ax1_1060, ax1_1061, ax1_1062, ax1_1063, ax1_1064, % 200.12/26.88 ax1_1065, ax1_1066, ax1_1067, ax1_1068, ax1_1069, ax1_107, ax1_1070, ax1_1071, % 200.12/26.88 ax1_1072, ax1_1073, ax1_1074, ax1_1075, ax1_1076, ax1_1077, ax1_1078, ax1_108, % 200.12/26.88 ax1_1080, ax1_1081, ax1_1082, ax1_1083, ax1_1084, ax1_1085, ax1_1086, ax1_1087, % 200.12/26.88 ax1_1088, ax1_1089, ax1_109, ax1_1090, ax1_1091, ax1_1092, ax1_1093, ax1_1095, % 200.12/26.88 ax1_1096, ax1_1097, ax1_1098, ax1_1099, ax1_11, ax1_110, ax1_1100, ax1_1101, % 200.12/26.88 ax1_1102, ax1_1103, ax1_1104, ax1_1105, ax1_1106, ax1_1109, ax1_111, ax1_1110, % 200.12/26.88 ax1_1111, ax1_1113, ax1_1114, ax1_1115, ax1_1116, ax1_1117, ax1_1118, ax1_1119, % 200.12/26.88 ax1_112, ax1_1120, ax1_1122, ax1_1123, ax1_1124, ax1_1125, ax1_1126, ax1_1127, % 200.12/26.88 ax1_1128, ax1_1129, ax1_113, ax1_1130, ax1_1131, ax1_114, ax1_115, ax1_116, % 200.12/26.88 ax1_117, ax1_118, ax1_119, ax1_12, ax1_120, ax1_121, ax1_122, ax1_123, ax1_124, % 200.12/26.88 ax1_125, ax1_127, ax1_128, ax1_129, ax1_13, ax1_130, ax1_131, ax1_132, ax1_133, % 200.12/26.88 ax1_134, ax1_135, ax1_136, ax1_137, ax1_138, ax1_139, ax1_14, ax1_140, ax1_141, % 200.12/26.88 ax1_142, ax1_143, ax1_144, ax1_145, ax1_146, ax1_147, ax1_148, ax1_149, ax1_15, % 200.12/26.88 ax1_150, ax1_151, ax1_152, ax1_153, ax1_154, ax1_156, ax1_157, ax1_158, ax1_159, % 200.12/26.88 ax1_16, ax1_160, ax1_161, ax1_162, ax1_163, ax1_164, ax1_165, ax1_166, ax1_167, % 200.12/26.88 ax1_168, ax1_169, ax1_17, ax1_171, ax1_172, ax1_173, ax1_174, ax1_175, ax1_176, % 200.12/26.88 ax1_177, ax1_178, ax1_179, ax1_18, ax1_180, ax1_181, ax1_182, ax1_183, ax1_184, % 200.12/26.88 ax1_185, ax1_186, ax1_187, ax1_188, ax1_189, ax1_19, ax1_190, ax1_191, ax1_192, % 200.12/26.88 ax1_193, ax1_194, ax1_195, ax1_196, ax1_197, ax1_198, ax1_199, ax1_2, ax1_20, % 200.12/26.88 ax1_200, ax1_201, ax1_202, ax1_203, ax1_204, ax1_205, ax1_206, ax1_207, ax1_208, % 200.12/26.88 ax1_209, ax1_21, ax1_210, ax1_211, ax1_212, ax1_213, ax1_214, ax1_215, ax1_216, % 200.12/26.88 ax1_217, ax1_218, ax1_219, ax1_22, ax1_220, ax1_221, ax1_222, ax1_223, ax1_224, % 200.12/26.88 ax1_225, ax1_226, ax1_227, ax1_228, ax1_23, ax1_230, ax1_231, ax1_232, ax1_233, % 200.12/26.88 ax1_234, ax1_235, ax1_236, ax1_237, ax1_238, ax1_239, ax1_24, ax1_240, ax1_241, % 200.12/26.88 ax1_242, ax1_243, ax1_244, ax1_245, ax1_246, ax1_247, ax1_248, ax1_249, ax1_25, % 200.12/26.88 ax1_250, ax1_251, ax1_252, ax1_253, ax1_254, ax1_255, ax1_256, ax1_257, ax1_258, % 200.12/26.88 ax1_259, ax1_26, ax1_260, ax1_261, ax1_262, ax1_263, ax1_264, ax1_265, ax1_266, % 200.12/26.88 ax1_267, ax1_268, ax1_269, ax1_27, ax1_270, ax1_271, ax1_272, ax1_273, ax1_274, % 200.12/26.88 ax1_275, ax1_276, ax1_277, ax1_278, ax1_279, ax1_28, ax1_280, ax1_281, ax1_282, % 200.12/26.88 ax1_283, ax1_284, ax1_285, ax1_286, ax1_287, ax1_288, ax1_289, ax1_29, ax1_291, % 200.12/26.88 ax1_292, ax1_293, ax1_294, ax1_295, ax1_296, ax1_297, ax1_298, ax1_299, ax1_3, % 200.12/26.88 ax1_30, ax1_300, ax1_301, ax1_302, ax1_303, ax1_304, ax1_305, ax1_306, ax1_307, % 200.12/26.88 ax1_308, ax1_309, ax1_31, ax1_310, ax1_311, ax1_312, ax1_313, ax1_314, ax1_315, % 200.12/26.88 ax1_316, ax1_317, ax1_318, ax1_320, ax1_321, ax1_322, ax1_323, ax1_324, ax1_325, % 200.12/26.88 ax1_326, ax1_327, ax1_328, ax1_329, ax1_33, ax1_330, ax1_331, ax1_332, ax1_333, % 200.12/26.88 ax1_334, ax1_335, ax1_336, ax1_337, ax1_338, ax1_339, ax1_34, ax1_340, ax1_341, % 200.12/26.88 ax1_342, ax1_343, ax1_344, ax1_345, ax1_346, ax1_347, ax1_348, ax1_349, ax1_35, % 200.12/26.88 ax1_350, ax1_351, ax1_352, ax1_353, ax1_354, ax1_355, ax1_356, ax1_357, ax1_358, % 200.12/26.88 ax1_359, ax1_36, ax1_360, ax1_361, ax1_362, ax1_364, ax1_365, ax1_366, ax1_367, % 200.12/26.88 ax1_368, ax1_369, ax1_37, ax1_370, ax1_371, ax1_372, ax1_373, ax1_374, ax1_375, % 200.12/26.88 ax1_376, ax1_377, ax1_378, ax1_379, ax1_38, ax1_380, ax1_382, ax1_383, ax1_384, % 200.12/26.88 ax1_385, ax1_386, ax1_387, ax1_388, ax1_389, ax1_39, ax1_390, ax1_391, ax1_392, % 200.12/26.88 ax1_393, ax1_394, ax1_395, ax1_396, ax1_397, ax1_398, ax1_399, ax1_4, ax1_40, % 200.12/26.88 ax1_400, ax1_401, ax1_402, ax1_403, ax1_404, ax1_405, ax1_406, ax1_407, ax1_408, % 200.12/26.88 ax1_409, ax1_41, ax1_410, ax1_411, ax1_412, ax1_413, ax1_414, ax1_415, ax1_416, % 200.12/26.88 ax1_417, ax1_418, ax1_419, ax1_42, ax1_420, ax1_421, ax1_422, ax1_423, ax1_424, % 200.12/26.88 ax1_425, ax1_426, ax1_427, ax1_428, ax1_429, ax1_43, ax1_430, ax1_431, ax1_432, % 200.12/26.88 ax1_433, ax1_434, ax1_435, ax1_436, ax1_437, ax1_438, ax1_439, ax1_44, ax1_440, % 200.12/26.88 ax1_441, ax1_442, ax1_443, ax1_444, ax1_445, ax1_446, ax1_447, ax1_448, ax1_449, % 200.12/26.88 ax1_45, ax1_450, ax1_451, ax1_453, ax1_454, ax1_455, ax1_456, ax1_457, ax1_458, % 200.12/26.88 ax1_459, ax1_46, ax1_460, ax1_461, ax1_462, ax1_463, ax1_464, ax1_465, ax1_466, % 200.12/26.88 ax1_467, ax1_468, ax1_469, ax1_47, ax1_470, ax1_471, ax1_472, ax1_473, ax1_474, % 200.12/26.88 ax1_475, ax1_476, ax1_477, ax1_478, ax1_479, ax1_48, ax1_480, ax1_481, ax1_482, % 200.12/26.88 ax1_483, ax1_484, ax1_485, ax1_486, ax1_487, ax1_488, ax1_489, ax1_49, ax1_490, % 200.12/26.88 ax1_491, ax1_492, ax1_493, ax1_494, ax1_495, ax1_496, ax1_497, ax1_498, ax1_499, % 200.12/26.88 ax1_5, ax1_50, ax1_500, ax1_501, ax1_502, ax1_503, ax1_504, ax1_505, ax1_506, % 200.12/26.88 ax1_507, ax1_508, ax1_509, ax1_51, ax1_510, ax1_511, ax1_512, ax1_513, ax1_514, % 200.12/26.88 ax1_515, ax1_516, ax1_517, ax1_518, ax1_519, ax1_52, ax1_520, ax1_521, ax1_522, % 200.12/26.88 ax1_523, ax1_524, ax1_525, ax1_526, ax1_527, ax1_528, ax1_529, ax1_53, ax1_530, % 200.12/26.88 ax1_531, ax1_532, ax1_533, ax1_534, ax1_535, ax1_536, ax1_537, ax1_538, ax1_539, % 200.12/26.88 ax1_54, ax1_540, ax1_541, ax1_542, ax1_543, ax1_544, ax1_545, ax1_546, ax1_547, % 200.12/26.88 ax1_548, ax1_549, ax1_55, ax1_550, ax1_551, ax1_552, ax1_553, ax1_554, ax1_555, % 200.12/26.88 ax1_556, ax1_557, ax1_558, ax1_559, ax1_56, ax1_560, ax1_561, ax1_562, ax1_563, % 200.12/26.88 ax1_564, ax1_565, ax1_566, ax1_567, ax1_568, ax1_569, ax1_57, ax1_570, ax1_571, % 200.12/26.88 ax1_572, ax1_573, ax1_574, ax1_575, ax1_576, ax1_577, ax1_578, ax1_579, ax1_58, % 200.12/26.88 ax1_580, ax1_581, ax1_582, ax1_583, ax1_584, ax1_585, ax1_586, ax1_587, ax1_588, % 200.12/26.88 ax1_589, ax1_59, ax1_590, ax1_591, ax1_592, ax1_593, ax1_594, ax1_595, ax1_596, % 200.12/26.88 ax1_597, ax1_598, ax1_599, ax1_6, ax1_60, ax1_600, ax1_601, ax1_602, ax1_603, % 200.12/26.88 ax1_604, ax1_605, ax1_606, ax1_608, ax1_609, ax1_61, ax1_610, ax1_611, ax1_612, % 200.12/26.88 ax1_613, ax1_614, ax1_615, ax1_616, ax1_617, ax1_618, ax1_619, ax1_62, ax1_620, % 200.12/26.88 ax1_621, ax1_622, ax1_623, ax1_624, ax1_625, ax1_626, ax1_627, ax1_628, ax1_629, % 200.12/26.88 ax1_63, ax1_630, ax1_631, ax1_632, ax1_633, ax1_634, ax1_635, ax1_636, ax1_637, % 200.12/26.88 ax1_638, ax1_639, ax1_64, ax1_640, ax1_641, ax1_642, ax1_643, ax1_644, ax1_645, % 200.12/26.88 ax1_646, ax1_647, ax1_648, ax1_649, ax1_65, ax1_650, ax1_651, ax1_652, ax1_653, % 200.12/26.88 ax1_654, ax1_655, ax1_656, ax1_657, ax1_658, ax1_659, ax1_66, ax1_660, ax1_661, % 200.12/26.88 ax1_662, ax1_663, ax1_664, ax1_665, ax1_666, ax1_667, ax1_668, ax1_669, ax1_67, % 200.12/26.88 ax1_670, ax1_671, ax1_672, ax1_673, ax1_674, ax1_675, ax1_676, ax1_677, ax1_678, % 200.12/26.88 ax1_679, ax1_68, ax1_680, ax1_681, ax1_682, ax1_683, ax1_684, ax1_685, ax1_686, % 200.12/26.88 ax1_687, ax1_688, ax1_689, ax1_69, ax1_690, ax1_691, ax1_692, ax1_693, ax1_694, % 200.12/26.88 ax1_695, ax1_696, ax1_697, ax1_698, ax1_699, ax1_7, ax1_70, ax1_700, ax1_701, % 200.12/26.88 ax1_702, ax1_703, ax1_704, ax1_705, ax1_706, ax1_707, ax1_708, ax1_709, ax1_71, % 200.12/26.88 ax1_710, ax1_711, ax1_712, ax1_713, ax1_714, ax1_715, ax1_716, ax1_717, ax1_718, % 200.12/26.88 ax1_719, ax1_72, ax1_720, ax1_721, ax1_722, ax1_723, ax1_724, ax1_725, ax1_726, % 200.12/26.88 ax1_727, ax1_728, ax1_729, ax1_73, ax1_730, ax1_731, ax1_732, ax1_733, ax1_734, % 200.12/26.88 ax1_735, ax1_736, ax1_737, ax1_738, ax1_739, ax1_74, ax1_740, ax1_741, ax1_742, % 200.12/26.88 ax1_743, ax1_744, ax1_745, ax1_746, ax1_747, ax1_748, ax1_749, ax1_75, ax1_750, % 200.12/26.88 ax1_751, ax1_752, ax1_753, ax1_754, ax1_755, ax1_756, ax1_757, ax1_758, ax1_759, % 200.12/26.88 ax1_76, ax1_760, ax1_761, ax1_762, ax1_763, ax1_764, ax1_765, ax1_766, ax1_767, % 200.12/26.88 ax1_768, ax1_769, ax1_77, ax1_770, ax1_771, ax1_772, ax1_773, ax1_774, ax1_775, % 200.12/26.88 ax1_776, ax1_777, ax1_778, ax1_779, ax1_78, ax1_780, ax1_781, ax1_782, ax1_783, % 200.12/26.88 ax1_784, ax1_785, ax1_786, ax1_787, ax1_788, ax1_789, ax1_79, ax1_790, ax1_791, % 200.12/26.88 ax1_792, ax1_793, ax1_794, ax1_795, ax1_796, ax1_797, ax1_798, ax1_799, ax1_8, % 200.12/26.88 ax1_80, ax1_800, ax1_801, ax1_802, ax1_803, ax1_804, ax1_805, ax1_806, ax1_807, % 200.12/26.88 ax1_808, ax1_809, ax1_81, ax1_810, ax1_811, ax1_813, ax1_815, ax1_816, ax1_817, % 200.12/26.88 ax1_818, ax1_819, ax1_82, ax1_820, ax1_821, ax1_822, ax1_823, ax1_824, ax1_825, % 200.12/26.88 ax1_826, ax1_827, ax1_828, ax1_829, ax1_830, ax1_831, ax1_832, ax1_833, ax1_834, % 200.12/26.88 ax1_835, ax1_836, ax1_837, ax1_838, ax1_839, ax1_84, ax1_840, ax1_841, ax1_842, % 200.12/26.88 ax1_843, ax1_844, ax1_845, ax1_846, ax1_847, ax1_848, ax1_849, ax1_85, ax1_850, % 200.12/26.88 ax1_851, ax1_852, ax1_853, ax1_854, ax1_855, ax1_856, ax1_857, ax1_858, ax1_859, % 200.12/26.88 ax1_86, ax1_860, ax1_861, ax1_862, ax1_863, ax1_864, ax1_865, ax1_866, ax1_867, % 200.12/26.88 ax1_868, ax1_869, ax1_87, ax1_870, ax1_871, ax1_872, ax1_873, ax1_874, ax1_875, % 200.12/26.88 ax1_876, ax1_877, ax1_878, ax1_879, ax1_88, ax1_880, ax1_881, ax1_882, ax1_883, % 200.12/26.88 ax1_884, ax1_885, ax1_886, ax1_887, ax1_888, ax1_889, ax1_89, ax1_890, ax1_891, % 200.12/26.88 ax1_892, ax1_893, ax1_894, ax1_895, ax1_896, ax1_897, ax1_898, ax1_899, ax1_9, % 200.12/26.88 ax1_90, ax1_900, ax1_901, ax1_902, ax1_903, ax1_904, ax1_905, ax1_906, ax1_907, % 200.12/26.88 ax1_908, ax1_909, ax1_91, ax1_910, ax1_911, ax1_912, ax1_913, ax1_914, ax1_915, % 200.12/26.88 ax1_916, ax1_917, ax1_918, ax1_919, ax1_92, ax1_920, ax1_921, ax1_922, ax1_923, % 200.12/26.88 ax1_924, ax1_925, ax1_926, ax1_927, ax1_928, ax1_929, ax1_93, ax1_931, ax1_932, % 200.12/26.88 ax1_933, ax1_934, ax1_935, ax1_936, ax1_937, ax1_938, ax1_939, ax1_94, ax1_940, % 200.12/26.88 ax1_941, ax1_942, ax1_943, ax1_944, ax1_945, ax1_946, ax1_947, ax1_948, ax1_949, % 200.12/26.88 ax1_95, ax1_950, ax1_951, ax1_952, ax1_953, ax1_954, ax1_955, ax1_956, ax1_957, % 200.12/26.88 ax1_958, ax1_959, ax1_96, ax1_960, ax1_961, ax1_962, ax1_963, ax1_964, ax1_965, % 200.12/26.88 ax1_966, ax1_967, ax1_968, ax1_969, ax1_97, ax1_970, ax1_971, ax1_972, ax1_973, % 200.12/26.88 ax1_974, ax1_975, ax1_976, ax1_977, ax1_978, ax1_979, ax1_98, ax1_980, ax1_981, % 200.12/26.88 ax1_982, ax1_983, ax1_984, ax1_985, ax1_986, ax1_987, ax1_988, ax1_989, ax1_99, % 200.12/26.88 ax1_990, ax1_991, ax1_992, ax1_993, ax1_994, ax1_995, ax1_996, ax1_997, ax1_998, % 200.12/26.88 ax1_999 % 200.12/26.88 % 200.12/26.88 Those formulas are unsatisfiable: % 200.12/26.88 --------------------------------- % 200.12/26.88 % 200.12/26.88 Begin of proof % 200.12/26.88 | % 200.12/26.88 | ALPHA: (ax1_32) implies: % 200.12/26.88 | (1) genls(c_partiallyintangibleindividual, c_individual) % 200.12/26.88 | % 200.12/26.88 | ALPHA: (ax1_83) implies: % 200.12/26.88 | (2) applicationcontext(c_wamt_evalinitial_p14) % 200.12/26.88 | % 200.12/26.88 | ALPHA: (ax1_126) implies: % 200.12/26.88 | (3) ? [v0: $i] : ( ~ mtvisible(c_englishmt) | % 200.12/26.88 | (f_subcollectionofwithrelationfromtypefn(c_terrorist, c_hasmembers, % 200.12/26.88 | c_terroristgroup) = v0 & $i(v0) & prettystring(v0, % 200.12/26.88 | s_terroristthathasbeenamemberofaterroristorganization))) % 200.12/26.88 | % 200.12/26.88 | ALPHA: (ax1_155) implies: % 200.12/26.88 | (4) genls(c_microtheory, c_aspatialinformationstore) % 200.12/26.88 | % 200.12/26.88 | ALPHA: (ax1_170) implies: % 200.12/26.88 | (5) genls(c_applicationcontext, c_microtheory) % 200.12/26.88 | % 200.12/26.88 | ALPHA: (ax1_290) implies: % 200.12/26.88 | (6) disjointwith(c_collection, c_individual) % 200.12/26.88 | % 200.12/26.88 | ALPHA: (ax1_319) implies: % 200.12/26.88 | (7) genls(c_intangibleindividual, c_partiallyintangibleindividual) % 200.12/26.88 | % 200.12/26.88 | ALPHA: (ax1_381) implies: % 200.12/26.88 | (8) genls(c_aspatialinformationstore, c_intangibleindividual) % 200.12/26.88 | % 200.12/26.88 | ALPHA: (ax1_452) implies: % 200.12/26.88 | (9) ? [v0: $i] : ( ~ mtvisible(c_englishmt) | % 200.12/26.88 | (f_instancewithrelationtofn(c_footballteam, c_affiliatedwith, % 200.12/26.88 | c_beloitcollege) = v0 & $i(v0) & prettystring(v0, % 200.12/26.88 | s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege))) % 200.12/26.88 | % 200.12/26.88 | ALPHA: (ax1_607) implies: % 200.12/26.88 | (10) $i(c_intangibleindividual) % 200.12/26.88 | % 200.12/26.88 | ALPHA: (ax1_812) implies: % 200.12/26.88 | (11) $i(c_aspatialinformationstore) % 200.12/26.88 | % 200.12/26.88 | ALPHA: (ax1_814) implies: % 200.12/26.89 | (12) $i(c_collection) % 200.12/26.89 | (13) ! [v0: $i] : ( ~ $i(v0) | ~ collection(v0) | isa(v0, c_collection)) % 200.12/26.89 | % 200.12/26.89 | ALPHA: (ax1_930) implies: % 200.12/26.89 | (14) $i(c_applicationcontext) % 200.12/26.89 | (15) ! [v0: $i] : ( ~ $i(v0) | ~ applicationcontext(v0) | isa(v0, % 200.12/26.89 | c_applicationcontext)) % 200.12/26.89 | % 200.12/26.89 | ALPHA: (ax1_1014) implies: % 200.12/26.89 | (16) $i(c_individual) % 200.12/26.89 | % 200.12/26.89 | ALPHA: (ax1_1016) implies: % 200.12/26.89 | (17) $i(c_partiallyintangibleindividual) % 200.12/26.89 | % 200.12/26.89 | ALPHA: (ax1_1079) implies: % 200.12/26.89 | (18) $i(c_microtheory) % 200.12/26.89 | % 200.12/26.89 | ALPHA: (query95) implies: % 200.12/26.89 | (19) genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088) % 200.12/26.89 | (20) $i(c_wamt_evalinitial_p14) % 200.12/26.89 | (21) $i(c_tptpcol_15_80088) % 200.12/26.89 | % 200.12/26.89 | DELTA: instantiating (9) with fresh symbol all_812_0 gives: % 200.12/26.89 | (22) ~ mtvisible(c_englishmt) | % 200.12/26.89 | (f_instancewithrelationtofn(c_footballteam, c_affiliatedwith, % 200.12/26.89 | c_beloitcollege) = all_812_0 & $i(all_812_0) & % 200.12/26.89 | prettystring(all_812_0, % 200.12/26.89 | s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege)) % 200.12/26.89 | % 200.12/26.89 | DELTA: instantiating (3) with fresh symbol all_820_0 gives: % 200.12/26.89 | (23) ~ mtvisible(c_englishmt) | % 200.12/26.89 | (f_subcollectionofwithrelationfromtypefn(c_terrorist, c_hasmembers, % 200.12/26.89 | c_terroristgroup) = all_820_0 & $i(all_820_0) & % 200.12/26.89 | prettystring(all_820_0, % 200.12/26.89 | s_terroristthathasbeenamemberofaterroristorganization)) % 200.12/26.89 | % 200.12/26.89 | GROUND_INST: instantiating (ax1_1121) with c_collection, c_individual, % 200.12/26.89 | c_partiallyintangibleindividual, simplifying with (1), (6), (12), % 200.12/26.89 | (16), (17) gives: % 200.12/26.89 | (24) disjointwith(c_collection, c_partiallyintangibleindividual) % 200.12/26.89 | % 200.12/26.89 | GROUND_INST: instantiating (ax1_229) with c_wamt_evalinitial_p14, % 200.12/26.89 | c_tptpcol_15_80088, simplifying with (19), (20), (21) gives: % 200.12/26.89 | (25) collection(c_wamt_evalinitial_p14) % 200.12/26.89 | % 200.12/26.89 | GROUND_INST: instantiating (ax1_1112) with c_microtheory, % 200.12/26.89 | c_aspatialinformationstore, c_applicationcontext, simplifying % 200.12/26.89 | with (4), (5), (11), (14), (18) gives: % 200.12/26.89 | (26) genls(c_applicationcontext, c_aspatialinformationstore) % 200.12/26.89 | % 200.12/26.89 | GROUND_INST: instantiating (ax1_1112) with c_intangibleindividual, % 200.12/26.89 | c_partiallyintangibleindividual, c_aspatialinformationstore, % 200.12/26.89 | simplifying with (7), (8), (10), (11), (17) gives: % 200.12/26.89 | (27) genls(c_aspatialinformationstore, c_partiallyintangibleindividual) % 200.12/26.89 | % 200.12/26.89 | GROUND_INST: instantiating (15) with c_wamt_evalinitial_p14, simplifying with % 200.12/26.89 | (2), (20) gives: % 200.12/26.89 | (28) isa(c_wamt_evalinitial_p14, c_applicationcontext) % 200.12/26.89 | % 200.12/26.89 | BETA: splitting (22) gives: % 200.12/26.89 | % 200.12/26.89 | Case 1: % 200.12/26.89 | | % 200.12/26.89 | | % 200.12/26.89 | | REF_CLOSE: (11), (12), (13), (14), (17), (20), (24), (25), (26), (27), (28), % 200.12/26.89 | | (ax1_1094), (ax1_1121), (ax1_363) are inconsistent by sub-proof % 200.12/26.89 | | #1. % 200.12/26.89 | | % 200.12/26.89 | Case 2: % 200.12/26.89 | | % 200.12/26.90 | | (29) mtvisible(c_englishmt) % 200.12/26.90 | | % 200.12/26.90 | | BETA: splitting (23) gives: % 200.12/26.90 | | % 200.12/26.90 | | Case 1: % 200.12/26.90 | | | % 200.12/26.90 | | | (30) ~ mtvisible(c_englishmt) % 200.12/26.90 | | | % 200.12/26.90 | | | PRED_UNIFY: (29), (30) imply: % 200.12/26.90 | | | (31) $false % 200.12/26.90 | | | % 200.12/26.90 | | | CLOSE: (31) is inconsistent. % 200.12/26.90 | | | % 200.12/26.90 | | Case 2: % 200.12/26.90 | | | % 200.12/26.90 | | | % 200.12/26.90 | | | REF_CLOSE: (11), (12), (13), (14), (17), (20), (24), (25), (26), (27), % 200.12/26.90 | | | (28), (ax1_1094), (ax1_1121), (ax1_363) are inconsistent by % 200.12/26.90 | | | sub-proof #1. % 200.12/26.90 | | | % 200.12/26.90 | | End of split % 200.12/26.90 | | % 200.12/26.90 | End of split % 200.12/26.90 | % 200.12/26.90 End of proof % 200.12/26.90 % 200.12/26.90 Sub-proof #1 shows that the following formulas are inconsistent: % 200.12/26.90 ---------------------------------------------------------------- % 200.12/26.90 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 200.12/26.90 $i(v0) | ~ genls(v2, v1) | ~ disjointwith(v0, v1) | disjointwith(v0, % 200.12/26.90 v2)) % 200.12/26.90 (2) genls(c_applicationcontext, c_aspatialinformationstore) % 200.12/26.90 (3) $i(c_aspatialinformationstore) % 200.12/26.90 (4) disjointwith(c_collection, c_partiallyintangibleindividual) % 200.12/26.90 (5) isa(c_wamt_evalinitial_p14, c_applicationcontext) % 200.12/26.90 (6) $i(c_partiallyintangibleindividual) % 200.12/26.90 (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 200.12/26.90 $i(v0) | ~ isa(v0, v1) | ~ genls(v1, v2) | isa(v0, v2)) % 200.12/26.90 (8) ! [v0: $i] : ( ~ $i(v0) | ~ collection(v0) | isa(v0, c_collection)) % 200.12/26.90 (9) $i(c_applicationcontext) % 200.12/26.90 (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 200.12/26.90 $i(v0) | ~ isa(v0, v2) | ~ isa(v0, v1) | ~ disjointwith(v1, v2)) % 200.12/26.90 (11) $i(c_collection) % 200.12/26.90 (12) $i(c_wamt_evalinitial_p14) % 200.12/26.90 (13) genls(c_aspatialinformationstore, c_partiallyintangibleindividual) % 200.12/26.90 (14) collection(c_wamt_evalinitial_p14) % 200.12/26.90 % 200.12/26.90 Begin of proof % 200.12/26.90 | % 200.12/26.90 | GROUND_INST: instantiating (1) with c_collection, % 200.12/26.90 | c_partiallyintangibleindividual, c_aspatialinformationstore, % 200.12/26.90 | simplifying with (3), (4), (6), (11), (13) gives: % 200.12/26.90 | (15) disjointwith(c_collection, c_aspatialinformationstore) % 200.12/26.90 | % 200.12/26.90 | GROUND_INST: instantiating (7) with c_wamt_evalinitial_p14, % 200.12/26.90 | c_applicationcontext, c_aspatialinformationstore, simplifying % 200.12/26.90 | with (2), (3), (5), (9), (12) gives: % 200.12/26.90 | (16) isa(c_wamt_evalinitial_p14, c_aspatialinformationstore) % 200.12/26.90 | % 200.12/26.90 | GROUND_INST: instantiating (8) with c_wamt_evalinitial_p14, simplifying with % 200.12/26.90 | (12), (14) gives: % 200.12/26.90 | (17) isa(c_wamt_evalinitial_p14, c_collection) % 200.12/26.90 | % 200.12/26.90 | GROUND_INST: instantiating (10) with c_wamt_evalinitial_p14, c_collection, % 200.12/26.90 | c_aspatialinformationstore, simplifying with (3), (11), (12), % 200.12/26.90 | (15), (16), (17) gives: % 200.12/26.90 | (18) $false % 200.12/26.90 | % 200.12/26.90 | CLOSE: (18) is inconsistent. % 200.12/26.90 | % 200.12/26.90 End of proof % 200.12/26.90 % SZS output end Proof for theBenchmark % 200.12/26.90 % 200.12/26.90 26366ms %------------------------------------------------------------------------------