%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : NLP024-10 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% Computer : n015.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 : 600s
% DateTime : Mon Jul 18 03:11:15 EDT 2022
% Result : Unknown 8.94s 2.67s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : NLP024-10 : TPTP v8.1.0. Released v7.5.0.
% 0.07/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.12/0.33 % Computer : n015.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Fri Jul 1 04:05:42 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.34 6403: Facts:
% 0.12/0.34 6403: Id : 2, {_}: ifeq4 ?2 ?2 ?3 ?4 =>= ?3 [4, 3, 2] by ifeq_axiom ?2 ?3 ?4
% 0.12/0.34 6403: Id : 3, {_}: ifeq3 ?6 ?6 ?7 ?8 =>= ?7 [8, 7, 6] by ifeq_axiom_001 ?6 ?7 ?8
% 0.12/0.34 6403: Id : 4, {_}:
% 0.12/0.34 ifeq2 ?10 ?10 ?11 ?12 =>= ?11
% 0.12/0.34 [12, 11, 10] by ifeq_axiom_002 ?10 ?11 ?12
% 0.12/0.34 6403: Id : 5, {_}:
% 0.12/0.34 ifeq ?14 ?14 ?15 ?16 =>= ?15
% 0.12/0.34 [16, 15, 14] by ifeq_axiom_003 ?14 ?15 ?16
% 0.12/0.34 6403: Id : 6, {_}:
% 0.12/0.34 ifeq3 (dance ?18 ?19) true (event ?18 ?19) true =>= true
% 0.12/0.34 [19, 18] by clause1 ?18 ?19
% 0.12/0.34 6403: Id : 7, {_}:
% 0.12/0.34 ifeq3 (event ?21 ?22) true (eventuality ?21 ?22) true =>= true
% 0.12/0.34 [22, 21] by clause2 ?21 ?22
% 0.12/0.34 6403: Id : 8, {_}:
% 0.12/0.34 ifeq3 (eventuality ?24 ?25) true (thing ?24 ?25) true =>= true
% 0.12/0.34 [25, 24] by clause3 ?24 ?25
% 0.12/0.34 6403: Id : 9, {_}:
% 0.12/0.34 ifeq3 (thing ?27 ?28) true (singleton ?27 ?28) true =>= true
% 0.12/0.34 [28, 27] by clause4 ?27 ?28
% 0.12/0.34 6403: Id : 10, {_}:
% 0.12/0.34 ifeq3 (eventuality ?30 ?31) true (specific ?30 ?31) true =>= true
% 0.12/0.34 [31, 30] by clause5 ?30 ?31
% 0.12/0.34 6403: Id : 11, {_}:
% 0.12/0.34 ifeq3 (eventuality ?33 ?34) true (nonexistent ?33 ?34) true =>= true
% 0.12/0.34 [34, 33] by clause6 ?33 ?34
% 0.12/0.34 6403: Id : 12, {_}:
% 0.12/0.34 ifeq3 (eventuality ?36 ?37) true (unisex ?36 ?37) true =>= true
% 0.12/0.34 [37, 36] by clause7 ?36 ?37
% 0.12/0.34 6403: Id : 13, {_}:
% 0.12/0.34 ifeq3 (desire_want ?39 ?40) true (event ?39 ?40) true =>= true
% 0.12/0.34 [40, 39] by clause8 ?39 ?40
% 0.12/0.34 6403: Id : 14, {_}:
% 0.12/0.34 ifeq3 (proposition ?42 ?43) true (relation ?42 ?43) true =>= true
% 0.12/0.34 [43, 42] by clause9 ?42 ?43
% 0.12/0.34 6403: Id : 15, {_}:
% 0.12/0.34 ifeq3 (relation ?45 ?46) true (abstraction ?45 ?46) true =>= true
% 0.12/0.34 [46, 45] by clause10 ?45 ?46
% 0.12/0.34 6403: Id : 16, {_}:
% 0.12/0.34 ifeq3 (abstraction ?48 ?49) true (thing ?48 ?49) true =>= true
% 0.12/0.34 [49, 48] by clause11 ?48 ?49
% 0.12/0.34 6403: Id : 17, {_}:
% 0.12/0.34 ifeq3 (abstraction ?51 ?52) true (nonhuman ?51 ?52) true =>= true
% 0.12/0.34 [52, 51] by clause12 ?51 ?52
% 0.12/0.34 6403: Id : 18, {_}:
% 0.12/0.34 ifeq3 (abstraction ?54 ?55) true (general ?54 ?55) true =>= true
% 0.12/0.34 [55, 54] by clause13 ?54 ?55
% 0.12/0.34 6403: Id : 19, {_}:
% 0.12/0.34 ifeq3 (abstraction ?57 ?58) true (unisex ?57 ?58) true =>= true
% 0.12/0.34 [58, 57] by clause14 ?57 ?58
% 0.12/0.34 6403: Id : 20, {_}:
% 0.12/0.34 ifeq3 (forename ?60 ?61) true (relname ?60 ?61) true =>= true
% 0.12/0.34 [61, 60] by clause15 ?60 ?61
% 0.12/0.34 6403: Id : 21, {_}:
% 0.12/0.34 ifeq3 (relname ?63 ?64) true (relation ?63 ?64) true =>= true
% 0.12/0.34 [64, 63] by clause16 ?63 ?64
% 0.12/0.34 6403: Id : 22, {_}:
% 0.12/0.34 ifeq3 (mia_forename ?66 ?67) true (forename ?66 ?67) true =>= true
% 0.12/0.34 [67, 66] by clause17 ?66 ?67
% 0.12/0.34 6403: Id : 23, {_}:
% 0.12/0.34 ifeq3 (woman ?69 ?70) true (human_person ?69 ?70) true =>= true
% 0.12/0.34 [70, 69] by clause18 ?69 ?70
% 0.12/0.34 6403: Id : 24, {_}:
% 0.12/0.34 ifeq3 (human_person ?72 ?73) true (organism ?72 ?73) true =>= true
% 0.12/0.34 [73, 72] by clause19 ?72 ?73
% 0.12/0.34 6403: Id : 25, {_}:
% 0.12/0.34 ifeq3 (organism ?75 ?76) true (entity ?75 ?76) true =>= true
% 0.12/0.34 [76, 75] by clause20 ?75 ?76
% 0.12/0.34 6403: Id : 26, {_}:
% 0.12/0.34 ifeq3 (entity ?78 ?79) true (thing ?78 ?79) true =>= true
% 0.12/0.34 [79, 78] by clause21 ?78 ?79
% 0.12/0.34 6403: Id : 27, {_}:
% 0.12/0.34 ifeq3 (entity ?81 ?82) true (specific ?81 ?82) true =>= true
% 0.12/0.34 [82, 81] by clause22 ?81 ?82
% 0.12/0.34 6403: Id : 28, {_}:
% 0.12/0.34 ifeq3 (entity ?84 ?85) true (existent ?84 ?85) true =>= true
% 0.12/0.34 [85, 84] by clause23 ?84 ?85
% 0.12/0.34 6403: Id : 29, {_}:
% 0.12/0.34 ifeq3 (organism ?87 ?88) true (impartial ?87 ?88) true =>= true
% 0.12/0.34 [88, 87] by clause24 ?87 ?88
% 0.12/0.34 6403: Id : 30, {_}:
% 0.12/0.34 ifeq3 (organism ?90 ?91) true (living ?90 ?91) true =>= true
% 0.12/0.34 [91, 90] by clause25 ?90 ?91
% 0.12/0.34 6403: Id : 31, {_}:
% 0.12/0.34 ifeq3 (human_person ?93 ?94) true (human ?93 ?94) true =>= true
% 0.12/0.34 [94, 93] by clause26 ?93 ?94
% 0.12/0.34 6403: Id : 32, {_}:
% 0.12/0.34 ifeq3 (human_person ?96 ?97) true (animate ?96 ?97) true =>= true
% 0.12/0.34 [97, 96] by clause27 ?96 ?97
% 0.12/0.34 6403: Id : 33, {_}:
% 0.12/0.34 ifeq3 (woman ?99 ?100) true (female ?99 ?100) true =>= true
% 0.12/0.34 [100, 99] by clause28 ?99 ?100
% 0.12/0.34 6403: Id : 34, {_}:
% 0.12/0.34 ifeq3 (vincent_forename ?102 ?103) true (forename ?102 ?103) true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [103, 102] by clause29 ?102 ?103
% 0.12/0.34 6403: Id : 35, {_}:
% 0.12/0.34 ifeq3 (man ?105 ?106) true (human_person ?105 ?106) true =>= true
% 0.12/0.34 [106, 105] by clause30 ?105 ?106
% 0.12/0.34 6403: Id : 36, {_}:
% 0.12/0.34 ifeq3 (man ?108 ?109) true (male ?108 ?109) true =>= true
% 0.12/0.34 [109, 108] by clause31 ?108 ?109
% 0.12/0.34 6403: Id : 37, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?111 ?112) true
% 0.12/0.34 (ifeq3 (dance ?111 ?113) true (dance ?112 ?113) true) true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [113, 112, 111] by clause38 ?111 ?112 ?113
% 0.12/0.34 6403: Id : 38, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?115 ?116) true
% 0.12/0.34 (ifeq3 (event ?115 ?117) true (event ?116 ?117) true) true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [117, 116, 115] by clause39 ?115 ?116 ?117
% 0.12/0.34 6403: Id : 39, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?119 ?120) true
% 0.12/0.34 (ifeq3 (eventuality ?119 ?121) true (eventuality ?120 ?121) true)
% 0.12/0.34 true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [121, 120, 119] by clause40 ?119 ?120 ?121
% 0.12/0.34 6403: Id : 40, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?123 ?124) true
% 0.12/0.34 (ifeq3 (thing ?123 ?125) true (thing ?124 ?125) true) true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [125, 124, 123] by clause41 ?123 ?124 ?125
% 0.12/0.34 6403: Id : 41, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?127 ?128) true
% 0.12/0.34 (ifeq3 (singleton ?127 ?129) true (singleton ?128 ?129) true) true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [129, 128, 127] by clause42 ?127 ?128 ?129
% 0.12/0.34 6403: Id : 42, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?131 ?132) true
% 0.12/0.34 (ifeq3 (specific ?131 ?133) true (specific ?132 ?133) true) true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [133, 132, 131] by clause43 ?131 ?132 ?133
% 0.12/0.34 6403: Id : 43, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?135 ?136) true
% 0.12/0.34 (ifeq3 (nonexistent ?135 ?137) true (nonexistent ?136 ?137) true)
% 0.12/0.34 true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [137, 136, 135] by clause44 ?135 ?136 ?137
% 0.12/0.34 6403: Id : 44, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?139 ?140) true
% 0.12/0.34 (ifeq3 (unisex ?139 ?141) true (unisex ?140 ?141) true) true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [141, 140, 139] by clause45 ?139 ?140 ?141
% 0.12/0.34 6403: Id : 45, {_}:
% 0.12/0.34 ifeq3 (present ?143 ?144) true
% 0.12/0.34 (ifeq3 (accessible_world ?143 ?145) true (present ?145 ?144) true)
% 0.12/0.34 true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [145, 144, 143] by clause46 ?143 ?144 ?145
% 0.12/0.34 6403: Id : 46, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?147 ?148) true
% 0.12/0.34 (ifeq3 (desire_want ?147 ?149) true (desire_want ?148 ?149) true)
% 0.12/0.34 true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [149, 148, 147] by clause47 ?147 ?148 ?149
% 0.12/0.34 6403: Id : 47, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?151 ?152) true
% 0.12/0.34 (ifeq3 (proposition ?151 ?153) true (proposition ?152 ?153) true)
% 0.12/0.34 true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [153, 152, 151] by clause48 ?151 ?152 ?153
% 0.12/0.34 6403: Id : 48, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?155 ?156) true
% 0.12/0.34 (ifeq3 (relation ?155 ?157) true (relation ?156 ?157) true) true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [157, 156, 155] by clause49 ?155 ?156 ?157
% 0.12/0.34 6403: Id : 49, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?159 ?160) true
% 0.12/0.34 (ifeq3 (abstraction ?159 ?161) true (abstraction ?160 ?161) true)
% 0.12/0.34 true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [161, 160, 159] by clause50 ?159 ?160 ?161
% 0.12/0.34 6403: Id : 50, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?163 ?164) true
% 0.12/0.34 (ifeq3 (nonhuman ?163 ?165) true (nonhuman ?164 ?165) true) true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [165, 164, 163] by clause51 ?163 ?164 ?165
% 0.12/0.34 6403: Id : 51, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?167 ?168) true
% 0.12/0.34 (ifeq3 (general ?167 ?169) true (general ?168 ?169) true) true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [169, 168, 167] by clause52 ?167 ?168 ?169
% 0.12/0.34 6403: Id : 52, {_}:
% 0.12/0.34 ifeq3 (accessible_world ?171 ?172) true
% 0.12/0.34 (ifeq3 (forename ?171 ?173) true (forename ?172 ?173) true) true
% 0.12/0.34 =>=
% 0.12/0.34 true
% 0.12/0.34 [173, 172, 171] by clause53 ?171 ?172 ?173
% 0.12/0.35 6403: Id : 53, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?175 ?176) true
% 0.12/0.35 (ifeq3 (relname ?175 ?177) true (relname ?176 ?177) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [177, 176, 175] by clause54 ?175 ?176 ?177
% 0.12/0.35 6403: Id : 54, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?179 ?180) true
% 0.12/0.35 (ifeq3 (mia_forename ?179 ?181) true (mia_forename ?180 ?181) true)
% 0.12/0.35 true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [181, 180, 179] by clause55 ?179 ?180 ?181
% 0.12/0.35 6403: Id : 55, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?183 ?184) true
% 0.12/0.35 (ifeq3 (woman ?183 ?185) true (woman ?184 ?185) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [185, 184, 183] by clause56 ?183 ?184 ?185
% 0.12/0.35 6403: Id : 56, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?187 ?188) true
% 0.12/0.35 (ifeq3 (human_person ?187 ?189) true (human_person ?188 ?189) true)
% 0.12/0.35 true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [189, 188, 187] by clause57 ?187 ?188 ?189
% 0.12/0.35 6403: Id : 57, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?191 ?192) true
% 0.12/0.35 (ifeq3 (organism ?191 ?193) true (organism ?192 ?193) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [193, 192, 191] by clause58 ?191 ?192 ?193
% 0.12/0.35 6403: Id : 58, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?195 ?196) true
% 0.12/0.35 (ifeq3 (entity ?195 ?197) true (entity ?196 ?197) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [197, 196, 195] by clause59 ?195 ?196 ?197
% 0.12/0.35 6403: Id : 59, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?199 ?200) true
% 0.12/0.35 (ifeq3 (existent ?199 ?201) true (existent ?200 ?201) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [201, 200, 199] by clause60 ?199 ?200 ?201
% 0.12/0.35 6403: Id : 60, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?203 ?204) true
% 0.12/0.35 (ifeq3 (impartial ?203 ?205) true (impartial ?204 ?205) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [205, 204, 203] by clause61 ?203 ?204 ?205
% 0.12/0.35 6403: Id : 61, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?207 ?208) true
% 0.12/0.35 (ifeq3 (living ?207 ?209) true (living ?208 ?209) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [209, 208, 207] by clause62 ?207 ?208 ?209
% 0.12/0.35 6403: Id : 62, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?211 ?212) true
% 0.12/0.35 (ifeq3 (human ?211 ?213) true (human ?212 ?213) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [213, 212, 211] by clause63 ?211 ?212 ?213
% 0.12/0.35 6403: Id : 63, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?215 ?216) true
% 0.12/0.35 (ifeq3 (animate ?215 ?217) true (animate ?216 ?217) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [217, 216, 215] by clause64 ?215 ?216 ?217
% 0.12/0.35 6403: Id : 64, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?219 ?220) true
% 0.12/0.35 (ifeq3 (female ?219 ?221) true (female ?220 ?221) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [221, 220, 219] by clause65 ?219 ?220 ?221
% 0.12/0.35 6403: Id : 65, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?223 ?224) true
% 0.12/0.35 (ifeq3 (vincent_forename ?223 ?225) true
% 0.12/0.35 (vincent_forename ?224 ?225) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [225, 224, 223] by clause66 ?223 ?224 ?225
% 0.12/0.35 6403: Id : 66, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?227 ?228) true
% 0.12/0.35 (ifeq3 (man ?227 ?229) true (man ?228 ?229) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [229, 228, 227] by clause67 ?227 ?228 ?229
% 0.12/0.35 6403: Id : 67, {_}:
% 0.12/0.35 ifeq3 (accessible_world ?231 ?232) true
% 0.12/0.35 (ifeq3 (male ?231 ?233) true (male ?232 ?233) true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [233, 232, 231] by clause68 ?231 ?232 ?233
% 0.12/0.35 6403: Id : 68, {_}:
% 0.12/0.35 ifeq3 (agent ?235 ?236 ?237) true
% 0.12/0.35 (ifeq3 (accessible_world ?235 ?238) true (agent ?238 ?236 ?237)
% 0.12/0.35 true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [238, 237, 236, 235] by clause69 ?235 ?236 ?237 ?238
% 0.12/0.35 6403: Id : 69, {_}:
% 0.12/0.35 ifeq3 (theme ?240 ?241 ?242) true
% 0.12/0.35 (ifeq3 (accessible_world ?240 ?243) true (theme ?243 ?241 ?242)
% 0.12/0.35 true) true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [243, 242, 241, 240] by clause70 ?240 ?241 ?242 ?243
% 0.12/0.35 6403: Id : 70, {_}:
% 0.12/0.35 ifeq3 (of ?245 ?246 ?247) true
% 0.12/0.35 (ifeq3 (accessible_world ?245 ?248) true (of ?248 ?246 ?247) true)
% 0.12/0.35 true
% 0.12/0.35 =>=
% 0.12/0.35 true
% 0.12/0.35 [248, 247, 246, 245] by clause71 ?245 ?246 ?247 ?248
% 0.12/0.35 6403: Id : 71, {_}:
% 0.12/0.35 ifeq4 (of ?250 ?251 ?252) true
% 0.12/0.35 (ifeq4 (of ?250 ?253 ?252) true
% 0.12/0.35 (ifeq4 (entity ?250 ?252) true
% 0.12/0.35 (ifeq4 (forename ?250 ?251) true
% 0.12/0.35 (ifeq4 (forename ?250 ?253) true ?251 ?253) ?253) ?253) ?253)
% 0.12/0.35 ?253
% 0.12/0.35 =>=
% 0.12/0.35 ?253
% 0.12/0.35 [253, 252, 251, 250] by clause72 ?250 ?251 ?252 ?253
% 0.12/0.35 6403: Id : 72, {_}:
% 0.12/0.35 ifeq4 (theme ?255 ?256 ?257) true
% 0.12/0.35 (ifeq4 (theme ?255 ?258 ?259) true
% 0.12/0.35 (ifeq4 (proposition ?255 ?257) true
% 0.12/0.35 (ifeq4 (proposition ?255 ?259) true
% 0.12/0.35 (ifeq4 (desire_want ?255 ?256) true
% 0.12/0.35 (ifeq4 (desire_want ?255 ?258) true ?257 ?259) ?259) ?259)
% 0.12/0.35 ?259) ?259) ?259
% 0.12/0.35 =>=
% 0.12/0.35 ?259
% 0.12/0.35 [259, 258, 257, 256, 255] by clause73 ?255 ?256 ?257 ?258 ?259
% 0.12/0.35 6403: Id : 73, {_}: actual_world skc8 =>= true [] by clause74
% 0.12/0.35 6403: Id : 74, {_}: man skc8 skc15 =>= true [] by clause75
% 0.12/0.35 6403: Id : 75, {_}: event skc10 skc13 =>= true [] by clause76
% 0.12/0.35 6403: Id : 76, {_}: woman skc8 skc12 =>= true [] by clause77
% 0.12/0.35 6403: Id : 77, {_}: present skc10 skc13 =>= true [] by clause78
% 0.12/0.35 6403: Id : 78, {_}: dance skc10 skc13 =>= true [] by clause79
% 0.12/0.35 6403: Id : 79, {_}: forename skc8 skc11 =>= true [] by clause80
% 0.12/0.35 6403: Id : 80, {_}: mia_forename skc8 skc11 =>= true [] by clause81
% 0.12/0.35 6403: Id : 81, {_}: proposition skc8 skc10 =>= true [] by clause82
% 0.12/0.35 6403: Id : 82, {_}: accessible_world skc8 skc10 =>= true [] by clause83
% 0.12/0.35 6403: Id : 83, {_}: desire_want skc8 skc9 =>= true [] by clause84
% 0.12/0.35 6403: Id : 84, {_}: present skc8 skc9 =>= true [] by clause85
% 0.12/0.35 6403: Id : 85, {_}: forename skc8 skc14 =>= true [] by clause86
% 0.12/0.35 6403: Id : 86, {_}: vincent_forename skc8 skc14 =>= true [] by clause87
% 0.12/0.35 6403: Id : 87, {_}: of skc8 skc14 skc15 =>= true [] by clause88
% 0.12/0.35 6403: Id : 88, {_}: of skc8 skc11 skc12 =>= true [] by clause89
% 0.12/0.35 6403: Id : 89, {_}: agent skc8 skc9 skc12 =>= true [] by clause90
% 0.12/0.35 6403: Id : 90, {_}: agent skc10 skc13 skc12 =>= true [] by clause91
% 0.12/0.35 6403: Id : 91, {_}: theme skc8 skc9 skc10 =>= true [] by clause92
% 0.12/0.35 6403: Id : 92, {_}:
% 0.12/0.35 ifeq2 (tuple2 (unisex ?280 ?281) (male ?280 ?281)) (tuple2 true true)
% 0.12/0.35 a b
% 0.12/0.35 =>=
% 0.12/0.35 b
% 0.12/0.35 [281, 280] by clause32 ?280 ?281
% 0.12/0.35 6403: Id : 93, {_}:
% 0.12/0.35 ifeq2 (tuple2 (unisex ?283 ?284) (female ?283 ?284))
% 0.12/0.35 (tuple2 true true) a b
% 0.12/0.35 =>=
% 0.12/0.35 b
% 0.12/0.35 [284, 283] by clause33 ?283 ?284
% 0.12/0.35 6403: Id : 94, {_}:
% 0.12/0.35 ifeq2 (tuple2 (specific ?286 ?287) (general ?286 ?287))
% 0.12/0.35 (tuple2 true true) a b
% 0.12/0.35 =>=
% 0.12/0.35 b
% 0.12/0.35 [287, 286] by clause34 ?286 ?287
% 0.12/0.35 6403: Id : 95, {_}:
% 0.12/0.35 ifeq2 (tuple2 (nonhuman ?289 ?290) (human ?289 ?290))
% 0.12/0.35 (tuple2 true true) a b
% 0.12/0.35 =>=
% 0.12/0.35 b
% 0.12/0.35 [290, 289] by clause35 ?289 ?290
% 0.12/0.35 6403: Id : 96, {_}:
% 0.12/0.35 ifeq2 (tuple2 (female ?292 ?293) (male ?292 ?293)) (tuple2 true true)
% 0.12/0.35 a b
% 0.12/0.35 =>=
% 0.12/0.35 b
% 0.12/0.35 [293, 292] by clause36 ?292 ?293
% 0.12/0.35 6403: Id : 97, {_}:
% 0.12/0.35 ifeq2 (tuple2 (nonexistent ?295 ?296) (existent ?295 ?296))
% 0.12/0.35 (tuple2 true true) a b
% 0.12/0.35 =>=
% 0.12/0.35 b
% 0.12/0.35 [296, 295] by clause37 ?295 ?296
% 0.12/0.35 6403: Id : 98, {_}:
% 0.12/0.35 ifeq
% 0.12/0.35 (tuple (dance ?298 ?299) (event ?298 ?299) (desire_want skc8 ?300)
% 0.12/0.35 (proposition skc8 ?298) (accessible_world skc8 ?298)
% 0.12/0.35 (present ?298 ?299) (present skc8 ?300) (agent ?298 ?299 skc15)
% 0.12/0.35 (agent skc8 ?300 skc15) (theme skc8 ?300 ?298))
% 0.12/0.35 (tuple true true true true true true true true true true) a b
% 0.12/0.35 =>=
% 0.12/0.35 b
% 0.12/0.35 [300, 299, 298] by clause93 ?298 ?299 ?300
% 0.12/0.35 6403: Goal:
% 0.12/0.35 6403: Id : 1, {_}: a =>= b [] by goal
% 8.94/2.67 % SZS status Timeout for theBenchmark.p
%------------------------------------------------------------------------------