%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : NLP247-10 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n011.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:16:40 EDT 2022 % Result : Satisfiable 1.32s 1.49s % Output : Saturation 1.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : NLP247-10 : TPTP v8.1.0. Released v7.3.0. % 0.07/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n011.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 : Thu Jun 30 19:11:33 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 1.32/1.49 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.32/1.49 % 1.32/1.49 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.32/1.49 |- ifeq3 $A $A $B $C = $B % 1.32/1.49 |- ifeq2 $A $A $B $C = $B % 1.32/1.49 |- ifeq $A $A $B $C = $B % 1.32/1.49 |- ifeq2 (smoke $U $V) true (event $U $V) true = true % 1.32/1.49 |- ifeq2 (event $U $V) true (eventuality $U $V) true = true % 1.32/1.49 |- ifeq2 (eventuality $U $V) true (thing $U $V) true = true % 1.32/1.49 |- ifeq2 (thing $U $V) true (singleton $U $V) true = true % 1.32/1.49 |- ifeq2 (eventuality $U $V) true (specific $U $V) true = true % 1.32/1.49 |- ifeq2 (eventuality $U $V) true (nonexistent $U $V) true = true % 1.32/1.49 |- ifeq2 (eventuality $U $V) true (unisex $U $V) true = true % 1.32/1.49 |- ifeq2 (proposition $U $V) true (relation $U $V) true = true % 1.32/1.49 |- ifeq2 (relation $U $V) true (abstraction $U $V) true = true % 1.32/1.49 |- ifeq2 (abstraction $U $V) true (thing $U $V) true = true % 1.32/1.49 |- ifeq2 (abstraction $U $V) true (nonhuman $U $V) true = true % 1.32/1.49 |- ifeq2 (abstraction $U $V) true (general $U $V) true = true % 1.32/1.49 |- ifeq2 (abstraction $U $V) true (unisex $U $V) true = true % 1.32/1.49 |- ifeq2 (state $U $V) true (eventuality $U $V) true = true % 1.32/1.49 |- ifeq2 (state $U $V) true (event $U $V) true = true % 1.32/1.49 |- ifeq2 (man $U $V) true (human_person $U $V) true = true % 1.32/1.49 |- ifeq2 (human_person $U $V) true (organism $U $V) true = true % 1.32/1.49 |- ifeq2 (organism $U $V) true (entity $U $V) true = true % 1.32/1.49 |- ifeq2 (entity $U $V) true (thing $U $V) true = true % 1.32/1.49 |- ifeq2 (entity $U $V) true (specific $U $V) true = true % 1.32/1.49 |- ifeq2 (entity $U $V) true (existent $U $V) true = true % 1.32/1.49 |- ifeq2 (organism $U $V) true (impartial $U $V) true = true % 1.32/1.49 |- ifeq2 (organism $U $V) true (living $U $V) true = true % 1.32/1.49 |- ifeq2 (human_person $U $V) true (human $U $V) true = true % 1.32/1.49 |- ifeq2 (human_person $U $V) true (animate $U $V) true = true % 1.32/1.49 |- ifeq2 (man $U $V) true (male $U $V) true = true % 1.32/1.49 |- ifeq2 (forename $U $V) true (relname $U $V) true = true % 1.32/1.49 |- ifeq2 (relname $U $V) true (relation $U $V) true = true % 1.32/1.49 |- ifeq2 (vincent_forename $U $V) true (forename $U $V) true = true % 1.32/1.49 |- ifeq2 (jules_forename $U $V) true (forename $U $V) true = true % 1.32/1.49 |- ifeq3 (be $U $V $W $X) true $W $X = $X % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (smoke $U $W) true (smoke $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (event $U $W) true (event $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (eventuality $U $W) true (eventuality $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (thing $U $W) true (thing $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (singleton $U $W) true (singleton $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (specific $U $W) true (specific $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (nonexistent $U $W) true (nonexistent $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (unisex $U $W) true (unisex $V $W) true) true = true % 1.32/1.49 |- ifeq2 (present $U $W) true % 1.32/1.49 (ifeq2 (accessible_world $U $V) true (present $V $W) true) true = true % 1.32/1.49 |- ifeq2 (think_believe_consider $U $W) true % 1.32/1.49 (ifeq2 (accessible_world $U $V) true (think_believe_consider $V $W) % 1.32/1.49 true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (proposition $U $W) true (proposition $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (relation $U $W) true (relation $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (abstraction $U $W) true (abstraction $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (nonhuman $U $W) true (nonhuman $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (general $U $W) true (general $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (state $U $W) true (state $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (man $U $W) true (man $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (human_person $U $W) true (human_person $V $W) true) true = % 1.32/1.49 true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (organism $U $W) true (organism $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (entity $U $W) true (entity $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (existent $U $W) true (existent $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (impartial $U $W) true (impartial $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (living $U $W) true (living $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (human $U $W) true (human $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (animate $U $W) true (animate $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (male $U $W) true (male $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (forename $U $W) true (forename $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (relname $U $W) true (relname $V $W) true) true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (vincent_forename $U $W) true (vincent_forename $V $W) true) % 1.32/1.49 true = true % 1.32/1.49 |- ifeq2 (accessible_world $U $V) true % 1.32/1.49 (ifeq2 (jules_forename $U $W) true (jules_forename $V $W) true) true = % 1.32/1.49 true % 1.32/1.49 |- ifeq2 (agent $U $W $X) true % 1.32/1.49 (ifeq2 (accessible_world $U $V) true (agent $V $W $X) true) true = % 1.32/1.49 true % 1.32/1.50 |- ifeq2 (theme $U $W $X) true % 1.32/1.50 (ifeq2 (accessible_world $U $V) true (theme $V $W $X) true) true = % 1.32/1.50 true % 1.32/1.50 |- ifeq2 (of $U $W $X) true % 1.32/1.50 (ifeq2 (accessible_world $U $V) true (of $V $W $X) true) true = true % 1.32/1.50 |- ifeq2 (be $U $W $X $Y) true % 1.32/1.50 (ifeq2 (accessible_world $U $V) true (be $V $W $X $Y) true) true = % 1.32/1.50 true % 1.32/1.50 |- ifeq3 (of $U $W $X) true % 1.32/1.50 (ifeq3 (of $U $V $X) true % 1.32/1.50 (ifeq3 (forename $U $W) true % 1.32/1.50 (ifeq3 (forename $U $V) true (ifeq3 (entity $U $X) true $W $V) % 1.32/1.50 $V) $V) $V) $V = $V % 1.32/1.50 |- ifeq3 (theme $U $Y $W) true % 1.32/1.50 (ifeq3 (theme $U $X $V) true % 1.32/1.50 (ifeq3 (agent $U $Y $Z) true % 1.32/1.50 (ifeq3 (agent $U $X $Z) true % 1.32/1.50 (ifeq3 (think_believe_consider $U $Y) true % 1.32/1.50 (ifeq3 (think_believe_consider $U $X) true % 1.32/1.50 (ifeq3 (proposition $U $W) true % 1.32/1.50 (ifeq3 (proposition $U $V) true $V $W) $W) $W) $W) % 1.32/1.50 $W) $W) $W) $W = $W % 1.32/1.50 |- ifeq (tuple (unisex $U $V) (male $U $V)) (tuple true true) a b = b % 1.32/1.50 |- ifeq (tuple (specific $U $V) (general $U $V)) (tuple true true) a b = b % 1.32/1.50 |- ifeq (tuple (nonhuman $U $V) (human $U $V)) (tuple true true) a b = b % 1.32/1.50 |- ifeq (tuple (nonexistent $U $V) (existent $U $V)) (tuple true true) a % 1.32/1.50 b = b % 1.32/1.50 |- actual_world skc14 = true % 1.32/1.50 |- forename skc14 skc28 = true % 1.32/1.50 |- jules_forename skc14 skc28 = true % 1.32/1.50 |- man skc14 skc27 = true % 1.32/1.50 |- event skc15 skc25 = true % 1.32/1.50 |- man skc14 skc24 = true % 1.32/1.50 |- present skc15 skc25 = true % 1.32/1.50 |- smoke skc15 skc25 = true % 1.32/1.50 |- man skc14 skc20 = true % 1.32/1.50 |- vincent_forename skc14 skc19 = true % 1.32/1.50 |- forename skc14 skc19 = true % 1.32/1.50 |- think_believe_consider skc14 skc18 = true % 1.32/1.50 |- present skc14 skc18 = true % 1.32/1.50 |- event skc14 skc18 = true % 1.32/1.50 |- event skc14 skc16 = true % 1.32/1.50 |- present skc14 skc16 = true % 1.32/1.50 |- think_believe_consider skc14 skc16 = true % 1.32/1.50 |- accessible_world skc14 skc15 = true % 1.32/1.50 |- proposition skc14 skc15 = true % 1.32/1.50 |- forename skc14 skc23 = true % 1.32/1.50 |- jules_forename skc14 skc23 = true % 1.32/1.50 |- state skc14 skc26 = true % 1.32/1.50 |- of skc14 skc28 skc27 = true % 1.32/1.50 |- of skc14 skc23 skc24 = true % 1.32/1.50 |- agent skc15 skc25 skc24 = true % 1.32/1.50 |- agent skc14 skc16 skc20 = true % 1.32/1.50 |- agent skc14 skc18 skc20 = true % 1.32/1.50 |- of skc14 skc19 skc20 = true % 1.32/1.50 |- theme skc14 skc18 skc15 = true % 1.32/1.50 |- theme skc14 skc16 skc15 = true % 1.32/1.50 |- be skc14 skc26 skc27 skc27 = true % 1.32/1.50 |- ifeq2 (man skc15 $U) true true true = true % 1.32/1.50 |- ifeq2 (man skc15 $U) true (agent skc15 (skf1 $U) $U) true = true % 1.32/1.50 |- ~(a = b) % 1.32/1.50 |- eventuality skc14 skc16 = true % 1.32/1.50 |- eventuality skc14 skc18 = true % 1.32/1.50 |- eventuality skc15 skc25 = true % 1.32/1.50 |- thing skc14 skc16 = true % 1.32/1.50 |- thing skc14 skc18 = true % 1.32/1.50 |- thing skc15 skc25 = true % 1.32/1.50 |- nonexistent skc14 skc16 = true % 1.32/1.50 |- nonexistent skc14 skc18 = true % 1.32/1.50 |- nonexistent skc15 skc25 = true % 1.32/1.50 |- unisex skc14 skc16 = true % 1.32/1.50 |- unisex skc14 skc18 = true % 1.32/1.50 |- unisex skc15 skc25 = true % 1.32/1.50 |- ifeq2 (abstraction skc14 skc16) true true true = true % 1.32/1.50 |- ifeq2 (abstraction skc14 skc18) true true true = true % 1.32/1.50 |- ifeq2 (abstraction skc15 skc25) true true true = true % 1.32/1.50 |- ifeq2 (state skc14 skc16) true true true = true % 1.32/1.50 |- ifeq2 (state skc14 skc18) true true true = true % 1.32/1.50 |- ifeq2 (state skc15 skc25) true true true = true % 1.32/1.50 |- eventuality skc14 skc26 = true % 1.32/1.50 |- unisex skc14 skc26 = true % 1.32/1.50 |- nonexistent skc14 skc26 = true % 1.32/1.50 |- thing skc14 skc26 = true % 1.32/1.50 |- ifeq2 (abstraction skc14 skc26) true true true = true % 1.32/1.50 |- event skc14 skc26 = true % 1.32/1.50 |- ifeq2 (entity skc14 skc16) true true true = true % 1.32/1.50 |- ifeq2 (entity skc14 skc18) true true true = true % 1.32/1.50 |- ifeq2 (entity skc14 skc26) true true true = true % 1.32/1.50 |- ifeq2 (entity skc15 skc25) true true true = true % 1.32/1.50 |- male skc14 skc20 = true % 1.32/1.50 |- male skc14 skc24 = true % 1.32/1.50 |- male skc14 skc27 = true % 1.32/1.50 |- relname skc14 skc19 = true % 1.32/1.50 |- relname skc14 skc23 = true % 1.32/1.50 |- relname skc14 skc28 = true % 1.32/1.50 |- ifeq2 (jules_forename skc14 skc19) true true true = true % 1.32/1.50 |- ifeq2 (smoke skc14 skc16) true true true = true % 1.32/1.50 |- ifeq2 (smoke skc14 skc18) true true true = true % 1.32/1.50 |- ifeq2 (smoke skc14 skc26) true true true = true % 1.32/1.50 |- singleton skc14 skc16 = true % 1.32/1.50 |- singleton skc14 skc18 = true % 1.32/1.50 |- singleton skc14 skc26 = true % 1.32/1.50 |- singleton skc15 skc25 = true % 1.32/1.50 |- specific skc14 skc16 = true % 1.32/1.50 |- specific skc14 skc18 = true % 1.32/1.50 |- specific skc14 skc26 = true % 1.32/1.50 |- specific skc15 skc25 = true % 1.32/1.50 |- relation skc14 skc15 = true % 1.32/1.50 |- abstraction skc14 skc15 = true % 1.32/1.50 |- nonhuman skc14 skc15 = true % 1.32/1.50 |- thing skc14 skc15 = true % 1.32/1.50 |- singleton skc14 skc15 = true % 1.32/1.50 |- ifeq2 (entity skc14 skc15) true true true = true % 1.32/1.50 |- ifeq2 (eventuality skc14 skc15) true true true = true % 1.32/1.50 |- general skc14 skc15 = true % 1.32/1.50 |- unisex skc14 skc15 = true % 1.32/1.50 |- human_person skc14 skc20 = true % 1.32/1.50 |- human_person skc14 skc24 = true % 1.32/1.50 |- human_person skc14 skc27 = true % 1.32/1.50 |- organism skc14 skc20 = true % 1.32/1.50 |- organism skc14 skc24 = true % 1.32/1.50 |- organism skc14 skc27 = true % 1.32/1.50 |- living skc14 skc24 = true % 1.32/1.50 |- impartial skc14 skc24 = true % 1.32/1.50 |- entity skc14 skc24 = true % 1.32/1.50 |- living skc14 skc27 = true % 1.32/1.50 |- impartial skc14 skc27 = true % 1.32/1.50 |- entity skc14 skc27 = true % 1.32/1.50 |- thing skc14 skc24 = true % 1.32/1.50 |- thing skc14 skc27 = true % 1.32/1.50 |- singleton skc14 skc24 = true % 1.32/1.50 |- ifeq2 (abstraction skc14 skc24) true true true = true % 1.32/1.50 |- ifeq2 (eventuality skc14 skc24) true true true = true % 1.32/1.50 |- singleton skc14 skc27 = true % 1.32/1.50 |- ifeq2 (abstraction skc14 skc27) true true true = true % 1.32/1.50 |- ifeq2 (eventuality skc14 skc27) true true true = true % 1.32/1.50 |- living skc14 skc20 = true % 1.32/1.50 |- impartial skc14 skc20 = true % 1.32/1.50 |- entity skc14 skc20 = true % 1.32/1.50 |- thing skc14 skc20 = true % 1.32/1.50 |- singleton skc14 skc20 = true % 1.32/1.50 |- ifeq2 (abstraction skc14 skc20) true true true = true % 1.32/1.50 |- ifeq2 (eventuality skc14 skc20) true true true = true % 1.32/1.50 |- specific skc14 skc20 = true % 1.32/1.50 |- specific skc14 skc24 = true % 1.32/1.50 |- specific skc14 skc27 = true % 1.32/1.50 |- existent skc14 skc20 = true % 1.32/1.50 |- existent skc14 skc24 = true % 1.32/1.50 |- existent skc14 skc27 = true % 1.32/1.50 |- human skc14 skc20 = true % 1.32/1.50 |- human skc14 skc24 = true % 1.32/1.50 |- human skc14 skc27 = true % 1.32/1.50 |- animate skc14 skc20 = true % 1.32/1.50 |- animate skc14 skc24 = true % 1.32/1.50 |- animate skc14 skc27 = true % 1.32/1.50 |- ifeq2 (relname skc14 skc15) true true true = true % 1.32/1.50 |- relation skc14 skc19 = true % 1.32/1.50 |- relation skc14 skc23 = true % 1.32/1.50 |- relation skc14 skc28 = true % 1.32/1.50 |- abstraction skc14 skc19 = true % 1.32/1.50 |- ifeq2 (proposition skc14 skc19) true true true = true % 1.32/1.50 |- abstraction skc14 skc23 = true % 1.32/1.50 |- ifeq2 (proposition skc14 skc23) true true true = true % 1.32/1.50 |- unisex skc14 skc23 = true % 1.32/1.50 |- general skc14 skc23 = true % 1.32/1.50 |- nonhuman skc14 skc23 = true % 1.32/1.50 |- thing skc14 skc23 = true % 1.32/1.50 |- ifeq2 (eventuality skc14 skc23) true true true = true % 1.32/1.50 |- singleton skc14 skc23 = true % 1.32/1.50 |- ifeq2 (entity skc14 skc23) true true true = true % 1.32/1.50 |- abstraction skc14 skc28 = true % 1.32/1.50 |- ifeq2 (proposition skc14 skc28) true true true = true % 1.32/1.50 |- unisex skc14 skc28 = true % 1.32/1.50 |- general skc14 skc28 = true % 1.32/1.50 |- nonhuman skc14 skc28 = true % 1.32/1.50 |- thing skc14 skc28 = true % 1.32/1.50 |- ifeq2 (eventuality skc14 skc28) true true true = true % 1.32/1.50 |- singleton skc14 skc28 = true % 1.32/1.50 |- ifeq2 (entity skc14 skc28) true true true = true % 1.32/1.50 |- unisex skc14 skc19 = true % 1.32/1.50 |- general skc14 skc19 = true % 1.32/1.50 |- nonhuman skc14 skc19 = true % 1.32/1.50 |- thing skc14 skc19 = true % 1.32/1.50 |- ifeq2 (eventuality skc14 skc19) true true true = true % 1.32/1.50 |- singleton skc14 skc19 = true % 1.32/1.50 |- ifeq2 (entity skc14 skc19) true true true = true % 1.32/1.50 |- ifeq2 (vincent_forename skc14 skc23) true true true = true % 1.32/1.50 |- ifeq2 (vincent_forename skc14 skc28) true true true = true % 1.32/1.50 |- ifeq (tuple (nonhuman skc14 skc20) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple (nonhuman skc14 skc24) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple (nonhuman skc14 skc27) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (human skc14 skc15)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (human skc14 skc19)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (human skc14 skc23)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (human skc14 skc28)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple (nonexistent skc14 skc20) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple (nonexistent skc14 skc24) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple (nonexistent skc14 skc27) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (existent skc14 skc16)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (existent skc14 skc18)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (existent skc14 skc26)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (existent skc15 skc25)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple (unisex skc14 skc20) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple (unisex skc14 skc24) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple (unisex skc14 skc27) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (male skc14 skc15)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (male skc14 skc16)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (male skc14 skc18)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (male skc14 skc19)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (male skc14 skc23)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (male skc14 skc26)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (male skc14 skc28)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (male skc15 skc25)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple (specific skc14 skc15) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple (specific skc14 skc19) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple (specific skc14 skc23) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple (specific skc14 skc28) true) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (general skc14 skc16)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (general skc14 skc18)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (general skc14 skc20)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (general skc14 skc24)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (general skc14 skc26)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (general skc14 skc27)) (tuple true true) a b = b % 1.32/1.51 |- ifeq (tuple true (general skc15 skc25)) (tuple true true) a b = b % 1.32/1.51 |- ifeq2 (accessible_world $_88 skc15) true % 1.32/1.51 (ifeq2 (smoke $_88 skc25) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $_89) true (smoke $_89 skc25) true = true % 1.32/1.51 |- ifeq2 (smoke skc14 $_90) true (smoke skc15 $_90) true = true % 1.32/1.51 |- ifeq2 (accessible_world skc15 skc15) true true true = true % 1.32/1.51 |- ifeq2 (smoke skc14 skc25) true true true = true % 1.32/1.51 |- ifeq2 (accessible_world $_95 skc14) true % 1.32/1.51 (ifeq2 (event $_95 skc16) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_95 skc14) true % 1.32/1.51 (ifeq2 (event $_95 skc18) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_95 skc14) true % 1.32/1.51 (ifeq2 (event $_95 skc26) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_95 skc15) true % 1.32/1.51 (ifeq2 (event $_95 skc25) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_96) true (event $_96 skc16) true = true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_96) true (event $_96 skc18) true = true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_96) true (event $_96 skc26) true = true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $_96) true (event $_96 skc25) true = true % 1.32/1.51 |- ifeq2 (event skc14 $_97) true (event skc15 $_97) true = true % 1.32/1.51 |- ifeq2 (accessible_world skc14 skc14) true true true = true % 1.32/1.51 |- event skc15 skc16 = true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $V) true (event $V skc16) true = true % 1.32/1.51 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.51 (ifeq2 (event $U skc16) true true true) true = true % 1.32/1.51 |- ifeq2 (smoke skc15 skc16) true true true = true % 1.32/1.51 |- ifeq2 (state skc15 skc16) true true true = true % 1.32/1.51 |- eventuality skc15 skc16 = true % 1.32/1.51 |- specific skc15 skc16 = true % 1.32/1.51 |- unisex skc15 skc16 = true % 1.32/1.51 |- nonexistent skc15 skc16 = true % 1.32/1.51 |- thing skc15 skc16 = true % 1.32/1.51 |- ifeq (tuple true (general skc15 skc16)) (tuple true true) a b = b % 1.32/1.51 |- ifeq2 (entity skc15 skc16) true true true = true % 1.32/1.51 |- ifeq (tuple true (male skc15 skc16)) (tuple true true) a b = b % 1.32/1.51 |- ifeq2 (abstraction skc15 skc16) true true true = true % 1.32/1.51 |- ifeq (tuple true (existent skc15 skc16)) (tuple true true) a b = b % 1.32/1.51 |- singleton skc15 skc16 = true % 1.32/1.51 |- event skc15 skc18 = true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $V) true (event $V skc18) true = true % 1.32/1.51 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.51 (ifeq2 (event $U skc18) true true true) true = true % 1.32/1.51 |- ifeq2 (smoke skc15 skc18) true true true = true % 1.32/1.51 |- ifeq2 (state skc15 skc18) true true true = true % 1.32/1.51 |- eventuality skc15 skc18 = true % 1.32/1.51 |- specific skc15 skc18 = true % 1.32/1.51 |- unisex skc15 skc18 = true % 1.32/1.51 |- nonexistent skc15 skc18 = true % 1.32/1.51 |- thing skc15 skc18 = true % 1.32/1.51 |- ifeq (tuple true (general skc15 skc18)) (tuple true true) a b = b % 1.32/1.51 |- ifeq2 (entity skc15 skc18) true true true = true % 1.32/1.51 |- ifeq (tuple true (male skc15 skc18)) (tuple true true) a b = b % 1.32/1.51 |- ifeq2 (abstraction skc15 skc18) true true true = true % 1.32/1.51 |- ifeq (tuple true (existent skc15 skc18)) (tuple true true) a b = b % 1.32/1.51 |- singleton skc15 skc18 = true % 1.32/1.51 |- event skc15 skc26 = true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $V) true (event $V skc26) true = true % 1.32/1.51 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.51 (ifeq2 (event $U skc26) true true true) true = true % 1.32/1.51 |- ifeq2 (smoke skc15 skc26) true true true = true % 1.32/1.51 |- eventuality skc15 skc26 = true % 1.32/1.51 |- specific skc15 skc26 = true % 1.32/1.51 |- unisex skc15 skc26 = true % 1.32/1.51 |- nonexistent skc15 skc26 = true % 1.32/1.51 |- thing skc15 skc26 = true % 1.32/1.51 |- ifeq (tuple true (general skc15 skc26)) (tuple true true) a b = b % 1.32/1.51 |- ifeq2 (entity skc15 skc26) true true true = true % 1.32/1.51 |- ifeq (tuple true (male skc15 skc26)) (tuple true true) a b = b % 1.32/1.51 |- ifeq2 (abstraction skc15 skc26) true true true = true % 1.32/1.51 |- ifeq (tuple true (existent skc15 skc26)) (tuple true true) a b = b % 1.32/1.51 |- singleton skc15 skc26 = true % 1.32/1.51 |- ifeq2 (event skc14 skc25) true true true = true % 1.32/1.51 |- ifeq2 (accessible_world skc15 skc14) true true true = true % 1.32/1.51 |- ifeq2 (accessible_world $_117 skc14) true % 1.32/1.51 (ifeq2 (eventuality $_117 skc16) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_117 skc14) true % 1.32/1.51 (ifeq2 (eventuality $_117 skc18) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_117 skc14) true % 1.32/1.51 (ifeq2 (eventuality $_117 skc26) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_117 skc15) true % 1.32/1.51 (ifeq2 (eventuality $_117 skc16) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_117 skc15) true % 1.32/1.51 (ifeq2 (eventuality $_117 skc18) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_117 skc15) true % 1.32/1.51 (ifeq2 (eventuality $_117 skc25) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_117 skc15) true % 1.32/1.51 (ifeq2 (eventuality $_117 skc26) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_118) true (eventuality $_118 skc16) % 1.32/1.51 true = true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_118) true (eventuality $_118 skc18) % 1.32/1.51 true = true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_118) true (eventuality $_118 skc26) % 1.32/1.51 true = true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $_118) true (eventuality $_118 skc16) % 1.32/1.51 true = true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $_118) true (eventuality $_118 skc18) % 1.32/1.51 true = true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $_118) true (eventuality $_118 skc25) % 1.32/1.51 true = true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $_118) true (eventuality $_118 skc26) % 1.32/1.51 true = true % 1.32/1.51 |- ifeq2 (eventuality skc14 $_119) true (eventuality skc15 $_119) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (eventuality skc14 skc25) true true true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc14) true % 1.32/1.51 (ifeq2 (thing $_142 skc15) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc14) true % 1.32/1.51 (ifeq2 (thing $_142 skc16) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc14) true % 1.32/1.51 (ifeq2 (thing $_142 skc18) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc14) true % 1.32/1.51 (ifeq2 (thing $_142 skc19) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc14) true % 1.32/1.51 (ifeq2 (thing $_142 skc20) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc14) true % 1.32/1.51 (ifeq2 (thing $_142 skc23) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc14) true % 1.32/1.51 (ifeq2 (thing $_142 skc24) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc14) true % 1.32/1.51 (ifeq2 (thing $_142 skc26) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc14) true % 1.32/1.51 (ifeq2 (thing $_142 skc27) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc14) true % 1.32/1.51 (ifeq2 (thing $_142 skc28) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc15) true % 1.32/1.51 (ifeq2 (thing $_142 skc16) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc15) true % 1.32/1.51 (ifeq2 (thing $_142 skc18) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc15) true % 1.32/1.51 (ifeq2 (thing $_142 skc25) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world $_142 skc15) true % 1.32/1.51 (ifeq2 (thing $_142 skc26) true true true) true = true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_143) true (thing $_143 skc15) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_143) true (thing $_143 skc16) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_143) true (thing $_143 skc18) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_143) true (thing $_143 skc19) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_143) true (thing $_143 skc20) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_143) true (thing $_143 skc23) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_143) true (thing $_143 skc24) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_143) true (thing $_143 skc26) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_143) true (thing $_143 skc27) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc14 $_143) true (thing $_143 skc28) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $_143) true (thing $_143 skc16) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $_143) true (thing $_143 skc18) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $_143) true (thing $_143 skc25) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $_143) true (thing $_143 skc26) true = % 1.32/1.51 true % 1.32/1.51 |- ifeq2 (thing skc14 $_144) true (thing skc15 $_144) true = true % 1.32/1.51 |- thing skc15 skc15 = true % 1.32/1.51 |- ifeq2 (accessible_world skc15 $V) true (thing $V skc15) true = true % 1.32/1.52 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.52 (ifeq2 (thing $U skc15) true true true) true = true % 1.32/1.52 |- singleton skc15 skc15 = true % 1.32/1.52 |- ifeq2 (entity skc15 skc15) true true true = true % 1.32/1.52 |- ifeq2 (eventuality skc15 skc15) true true true = true % 1.32/1.52 |- thing skc15 skc19 = true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $V) true (thing $V skc19) true = true % 1.32/1.52 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.52 (ifeq2 (thing $U skc19) true true true) true = true % 1.32/1.52 |- singleton skc15 skc19 = true % 1.32/1.52 |- ifeq2 (entity skc15 skc19) true true true = true % 1.32/1.52 |- ifeq2 (eventuality skc15 skc19) true true true = true % 1.32/1.52 |- thing skc15 skc20 = true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $V) true (thing $V skc20) true = true % 1.32/1.52 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.52 (ifeq2 (thing $U skc20) true true true) true = true % 1.32/1.52 |- singleton skc15 skc20 = true % 1.32/1.52 |- ifeq2 (abstraction skc15 skc20) true true true = true % 1.32/1.52 |- ifeq2 (eventuality skc15 skc20) true true true = true % 1.32/1.52 |- thing skc15 skc23 = true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $V) true (thing $V skc23) true = true % 1.32/1.52 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.52 (ifeq2 (thing $U skc23) true true true) true = true % 1.32/1.52 |- singleton skc15 skc23 = true % 1.32/1.52 |- ifeq2 (entity skc15 skc23) true true true = true % 1.32/1.52 |- ifeq2 (eventuality skc15 skc23) true true true = true % 1.32/1.52 |- thing skc15 skc24 = true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $V) true (thing $V skc24) true = true % 1.32/1.52 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.52 (ifeq2 (thing $U skc24) true true true) true = true % 1.32/1.52 |- singleton skc15 skc24 = true % 1.32/1.52 |- ifeq2 (abstraction skc15 skc24) true true true = true % 1.32/1.52 |- ifeq2 (eventuality skc15 skc24) true true true = true % 1.32/1.52 |- thing skc15 skc27 = true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $V) true (thing $V skc27) true = true % 1.32/1.52 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.52 (ifeq2 (thing $U skc27) true true true) true = true % 1.32/1.52 |- singleton skc15 skc27 = true % 1.32/1.52 |- ifeq2 (abstraction skc15 skc27) true true true = true % 1.32/1.52 |- ifeq2 (eventuality skc15 skc27) true true true = true % 1.32/1.52 |- thing skc15 skc28 = true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $V) true (thing $V skc28) true = true % 1.32/1.52 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.52 (ifeq2 (thing $U skc28) true true true) true = true % 1.32/1.52 |- singleton skc15 skc28 = true % 1.32/1.52 |- ifeq2 (entity skc15 skc28) true true true = true % 1.32/1.52 |- ifeq2 (eventuality skc15 skc28) true true true = true % 1.32/1.52 |- ifeq2 (thing skc14 skc25) true true true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc14) true % 1.32/1.52 (ifeq2 (singleton $_203 skc15) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc14) true % 1.32/1.52 (ifeq2 (singleton $_203 skc16) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc14) true % 1.32/1.52 (ifeq2 (singleton $_203 skc18) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc14) true % 1.32/1.52 (ifeq2 (singleton $_203 skc19) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc14) true % 1.32/1.52 (ifeq2 (singleton $_203 skc20) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc14) true % 1.32/1.52 (ifeq2 (singleton $_203 skc23) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc14) true % 1.32/1.52 (ifeq2 (singleton $_203 skc24) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc14) true % 1.32/1.52 (ifeq2 (singleton $_203 skc26) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc14) true % 1.32/1.52 (ifeq2 (singleton $_203 skc27) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc14) true % 1.32/1.52 (ifeq2 (singleton $_203 skc28) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc15) true % 1.32/1.52 (ifeq2 (singleton $_203 skc15) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc15) true % 1.32/1.52 (ifeq2 (singleton $_203 skc16) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc15) true % 1.32/1.52 (ifeq2 (singleton $_203 skc18) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc15) true % 1.32/1.52 (ifeq2 (singleton $_203 skc19) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc15) true % 1.32/1.52 (ifeq2 (singleton $_203 skc20) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc15) true % 1.32/1.52 (ifeq2 (singleton $_203 skc23) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc15) true % 1.32/1.52 (ifeq2 (singleton $_203 skc24) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc15) true % 1.32/1.52 (ifeq2 (singleton $_203 skc25) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc15) true % 1.32/1.52 (ifeq2 (singleton $_203 skc26) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc15) true % 1.32/1.52 (ifeq2 (singleton $_203 skc27) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_203 skc15) true % 1.32/1.52 (ifeq2 (singleton $_203 skc28) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_204) true (singleton $_204 skc15) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_204) true (singleton $_204 skc16) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_204) true (singleton $_204 skc18) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_204) true (singleton $_204 skc19) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_204) true (singleton $_204 skc20) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_204) true (singleton $_204 skc23) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_204) true (singleton $_204 skc24) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_204) true (singleton $_204 skc26) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_204) true (singleton $_204 skc27) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_204) true (singleton $_204 skc28) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_204) true (singleton $_204 skc15) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_204) true (singleton $_204 skc16) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_204) true (singleton $_204 skc18) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_204) true (singleton $_204 skc19) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_204) true (singleton $_204 skc20) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_204) true (singleton $_204 skc23) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_204) true (singleton $_204 skc24) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_204) true (singleton $_204 skc25) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_204) true (singleton $_204 skc26) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_204) true (singleton $_204 skc27) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_204) true (singleton $_204 skc28) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (singleton skc14 $_205) true (singleton skc15 $_205) true = true % 1.32/1.52 |- ifeq2 (singleton skc14 skc25) true true true = true % 1.32/1.52 |- ifeq2 (accessible_world $_245 skc14) true % 1.32/1.52 (ifeq2 (specific $_245 skc16) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_245 skc14) true % 1.32/1.52 (ifeq2 (specific $_245 skc18) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_245 skc14) true % 1.32/1.52 (ifeq2 (specific $_245 skc20) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_245 skc14) true % 1.32/1.52 (ifeq2 (specific $_245 skc24) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_245 skc14) true % 1.32/1.52 (ifeq2 (specific $_245 skc26) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_245 skc14) true % 1.32/1.52 (ifeq2 (specific $_245 skc27) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_245 skc15) true % 1.32/1.52 (ifeq2 (specific $_245 skc16) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_245 skc15) true % 1.32/1.52 (ifeq2 (specific $_245 skc18) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_245 skc15) true % 1.32/1.52 (ifeq2 (specific $_245 skc25) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_245 skc15) true % 1.32/1.52 (ifeq2 (specific $_245 skc26) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_246) true (specific $_246 skc16) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_246) true (specific $_246 skc18) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_246) true (specific $_246 skc20) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_246) true (specific $_246 skc24) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_246) true (specific $_246 skc26) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_246) true (specific $_246 skc27) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_246) true (specific $_246 skc16) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_246) true (specific $_246 skc18) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_246) true (specific $_246 skc25) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_246) true (specific $_246 skc26) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (specific skc14 $_247) true (specific skc15 $_247) true = true % 1.32/1.52 |- specific skc15 skc20 = true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $V) true (specific $V skc20) true = true % 1.32/1.52 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.52 (ifeq2 (specific $U skc20) true true true) true = true % 1.32/1.52 |- ifeq (tuple true (general skc15 skc20)) (tuple true true) a b = b % 1.32/1.52 |- specific skc15 skc24 = true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $V) true (specific $V skc24) true = true % 1.32/1.52 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.52 (ifeq2 (specific $U skc24) true true true) true = true % 1.32/1.52 |- ifeq (tuple true (general skc15 skc24)) (tuple true true) a b = b % 1.32/1.52 |- specific skc15 skc27 = true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $V) true (specific $V skc27) true = true % 1.32/1.52 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.52 (ifeq2 (specific $U skc27) true true true) true = true % 1.32/1.52 |- ifeq (tuple true (general skc15 skc27)) (tuple true true) a b = b % 1.32/1.52 |- ifeq2 (specific skc14 skc25) true true true = true % 1.32/1.52 |- ifeq2 (accessible_world $_288 skc14) true % 1.32/1.52 (ifeq2 (unisex $_288 skc15) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_288 skc14) true % 1.32/1.52 (ifeq2 (unisex $_288 skc16) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_288 skc14) true % 1.32/1.52 (ifeq2 (unisex $_288 skc18) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_288 skc14) true % 1.32/1.52 (ifeq2 (unisex $_288 skc19) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_288 skc14) true % 1.32/1.52 (ifeq2 (unisex $_288 skc23) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_288 skc14) true % 1.32/1.52 (ifeq2 (unisex $_288 skc26) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_288 skc14) true % 1.32/1.52 (ifeq2 (unisex $_288 skc28) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_288 skc15) true % 1.32/1.52 (ifeq2 (unisex $_288 skc16) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_288 skc15) true % 1.32/1.52 (ifeq2 (unisex $_288 skc18) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_288 skc15) true % 1.32/1.52 (ifeq2 (unisex $_288 skc25) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world $_288 skc15) true % 1.32/1.52 (ifeq2 (unisex $_288 skc26) true true true) true = true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_289) true (unisex $_289 skc15) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_289) true (unisex $_289 skc16) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_289) true (unisex $_289 skc18) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_289) true (unisex $_289 skc19) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_289) true (unisex $_289 skc23) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_289) true (unisex $_289 skc26) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc14 $_289) true (unisex $_289 skc28) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_289) true (unisex $_289 skc16) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_289) true (unisex $_289 skc18) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_289) true (unisex $_289 skc25) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $_289) true (unisex $_289 skc26) true = % 1.32/1.52 true % 1.32/1.52 |- ifeq2 (unisex skc14 $_290) true (unisex skc15 $_290) true = true % 1.32/1.52 |- unisex skc15 skc15 = true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $V) true (unisex $V skc15) true = true % 1.32/1.52 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.52 (ifeq2 (unisex $U skc15) true true true) true = true % 1.32/1.52 |- ifeq (tuple true (male skc15 skc15)) (tuple true true) a b = b % 1.32/1.52 |- unisex skc15 skc19 = true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $V) true (unisex $V skc19) true = true % 1.32/1.52 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.52 (ifeq2 (unisex $U skc19) true true true) true = true % 1.32/1.52 |- ifeq (tuple true (male skc15 skc19)) (tuple true true) a b = b % 1.32/1.52 |- unisex skc15 skc23 = true % 1.32/1.52 |- ifeq2 (accessible_world skc15 $V) true (unisex $V skc23) true = true % 1.32/1.53 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.53 (ifeq2 (unisex $U skc23) true true true) true = true % 1.32/1.53 |- ifeq (tuple true (male skc15 skc23)) (tuple true true) a b = b % 1.32/1.53 |- unisex skc15 skc28 = true % 1.32/1.53 |- ifeq2 (accessible_world skc15 $V) true (unisex $V skc28) true = true % 1.32/1.53 |- ifeq2 (accessible_world $U skc15) true % 1.32/1.53 (ifeq2 (unisex $U skc28) true true true) true = true % 1.32/1.53 |- ifeq (tuple true (male skc15 skc28)) (tuple true true) a b = b % 1.32/1.53 |- ifeq2 (unisex skc14 skc25) true true true = true % 1.32/1.53 |- ifeq2 (present $_337 skc16) true % 1.32/1.53 (ifeq2 (accessible_world $_337 skc14) true true true) true = true % 1.32/1.53 |- ifeq2 (present $_337 skc18) true % 1.32/1.53 (ifeq2 (accessible_world $_337 skc14) true true true) true = true % 1.32/1.53 |- ifeq2 (present $_337 skc25) true % 1.32/1.53 (ifeq2 (accessible_world $_337 skc15) true true true) true = true % 1.32/1.53 |- ifeq2 (present skc14 $_339) true (present skc15 $_339) true = true % 1.32/1.53 |- ifeq2 (accessible_world skc14 $_338) true (present $_338 skc16) true = % 1.32/1.53 true % 1.32/1.53 |- ifeq2 (accessible_world skc14 $_338) true (present $_338 skc18) true = % 1.32/1.53 true % 1.32/1.53 |- ifeq2 (accessible_world skc15 $_338) true (present $_338 skc25) true = % 1.32/1.53 true % 1.32/1.53 |- ifeq2 (present skc14 skc25) true true true = true % 1.32/1.53 |- present skc15 skc16 = true % 1.32/1.53 |- present skc15 skc18 = true % 1.32/1.53 |- ifeq2 (accessible_world skc15 $V) true (present $V skc16) true = true % 1.32/1.53 |- ifeq2 (present $U skc16) true % 1.32/1.53 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.32/1.53 |- ifeq2 (accessible_world skc15 $V) true (present $V skc18) true = true % 1.32/1.53 |- ifeq2 (present $U skc18) true % 1.32/1.53 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.32/1.53 |- ifeq2 (think_believe_consider $_355 skc16) true % 1.32/1.53 (ifeq2 (accessible_world $_355 skc14) true true true) true = true % 1.32/1.53 |- ifeq2 (think_believe_consider $_355 skc18) true % 1.32/1.53 (ifeq2 (accessible_world $_355 skc14) true true true) true = true % 1.32/1.53 |- ifeq2 (think_believe_consider skc14 $_357) true % 1.32/1.53 (think_believe_consider skc15 $_357) true = true % 1.32/1.53 |- ifeq2 (accessible_world skc14 $_356) true % 1.32/1.53 (think_believe_consider $_356 skc16) true = true % 1.32/1.53 |- ifeq2 (accessible_world skc14 $_356) true % 1.32/1.53 (think_believe_consider $_356 skc18) true = true % 1.32/1.53 |- think_believe_consider skc15 skc16 = true % 1.32/1.53 |- think_believe_consider skc15 skc18 = true % 1.32/1.53 |- ifeq2 (accessible_world skc15 $V) true (think_believe_consider $V skc16) % 1.32/1.53 true = true % 1.37/1.54 |- ifeq2 (think_believe_consider $U skc16) true % 1.37/1.54 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world skc15 $V) true (think_believe_consider $V skc18) % 1.37/1.54 true = true % 1.37/1.54 |- ifeq2 (think_believe_consider $U skc18) true % 1.37/1.54 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world $_372 skc14) true % 1.37/1.54 (ifeq2 (proposition $_372 skc15) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world skc14 $_373) true (proposition $_373 skc15) % 1.37/1.54 true = true % 1.37/1.54 |- ifeq2 (proposition skc14 $_374) true (proposition skc15 $_374) true = % 1.37/1.54 true % 1.37/1.54 |- proposition skc15 skc15 = true % 1.37/1.54 |- ifeq2 (accessible_world skc15 $V) true (proposition $V skc15) true = % 1.37/1.54 true % 1.37/1.54 |- ifeq2 (accessible_world $U skc15) true % 1.37/1.54 (ifeq2 (proposition $U skc15) true true true) true = true % 1.37/1.54 |- relation skc15 skc15 = true % 1.37/1.54 |- ifeq2 (relname skc15 skc15) true true true = true % 1.37/1.54 |- abstraction skc15 skc15 = true % 1.37/1.54 |- general skc15 skc15 = true % 1.37/1.54 |- nonhuman skc15 skc15 = true % 1.37/1.54 |- ifeq (tuple (specific skc15 skc15) true) (tuple true true) a b = b % 1.37/1.54 |- ifeq (tuple true (human skc15 skc15)) (tuple true true) a b = b % 1.37/1.54 |- ifeq2 (accessible_world $_389 skc14) true % 1.37/1.54 (ifeq2 (relation $_389 skc15) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world $_389 skc14) true % 1.37/1.54 (ifeq2 (relation $_389 skc19) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world $_389 skc14) true % 1.37/1.54 (ifeq2 (relation $_389 skc23) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world $_389 skc14) true % 1.37/1.54 (ifeq2 (relation $_389 skc28) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world $_389 skc15) true % 1.37/1.54 (ifeq2 (relation $_389 skc15) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world skc14 $_390) true (relation $_390 skc15) true = % 1.37/1.54 true % 1.37/1.54 |- ifeq2 (accessible_world skc14 $_390) true (relation $_390 skc19) true = % 1.37/1.54 true % 1.37/1.54 |- ifeq2 (accessible_world skc14 $_390) true (relation $_390 skc23) true = % 1.37/1.54 true % 1.37/1.54 |- ifeq2 (accessible_world skc14 $_390) true (relation $_390 skc28) true = % 1.37/1.54 true % 1.37/1.54 |- ifeq2 (accessible_world skc15 $_390) true (relation $_390 skc15) true = % 1.37/1.54 true % 1.37/1.54 |- ifeq2 (relation skc14 $_391) true (relation skc15 $_391) true = true % 1.37/1.54 |- relation skc15 skc19 = true % 1.37/1.54 |- ifeq2 (accessible_world skc15 $V) true (relation $V skc19) true = true % 1.37/1.54 |- ifeq2 (accessible_world $U skc15) true % 1.37/1.54 (ifeq2 (relation $U skc19) true true true) true = true % 1.37/1.54 |- abstraction skc15 skc19 = true % 1.37/1.54 |- ifeq2 (proposition skc15 skc19) true true true = true % 1.37/1.54 |- general skc15 skc19 = true % 1.37/1.54 |- nonhuman skc15 skc19 = true % 1.37/1.54 |- ifeq (tuple (specific skc15 skc19) true) (tuple true true) a b = b % 1.37/1.54 |- ifeq (tuple true (human skc15 skc19)) (tuple true true) a b = b % 1.37/1.54 |- relation skc15 skc23 = true % 1.37/1.54 |- ifeq2 (accessible_world skc15 $V) true (relation $V skc23) true = true % 1.37/1.54 |- ifeq2 (accessible_world $U skc15) true % 1.37/1.54 (ifeq2 (relation $U skc23) true true true) true = true % 1.37/1.54 |- abstraction skc15 skc23 = true % 1.37/1.54 |- ifeq2 (proposition skc15 skc23) true true true = true % 1.37/1.54 |- general skc15 skc23 = true % 1.37/1.54 |- nonhuman skc15 skc23 = true % 1.37/1.54 |- ifeq (tuple (specific skc15 skc23) true) (tuple true true) a b = b % 1.37/1.54 |- ifeq (tuple true (human skc15 skc23)) (tuple true true) a b = b % 1.37/1.54 |- relation skc15 skc28 = true % 1.37/1.54 |- ifeq2 (accessible_world skc15 $V) true (relation $V skc28) true = true % 1.37/1.54 |- ifeq2 (accessible_world $U skc15) true % 1.37/1.54 (ifeq2 (relation $U skc28) true true true) true = true % 1.37/1.54 |- abstraction skc15 skc28 = true % 1.37/1.54 |- ifeq2 (proposition skc15 skc28) true true true = true % 1.37/1.54 |- general skc15 skc28 = true % 1.37/1.54 |- nonhuman skc15 skc28 = true % 1.37/1.54 |- ifeq (tuple (specific skc15 skc28) true) (tuple true true) a b = b % 1.37/1.54 |- ifeq (tuple true (human skc15 skc28)) (tuple true true) a b = b % 1.37/1.54 |- ifeq2 (accessible_world $_428 skc14) true % 1.37/1.54 (ifeq2 (abstraction $_428 skc15) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world $_428 skc14) true % 1.37/1.54 (ifeq2 (abstraction $_428 skc19) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world $_428 skc14) true % 1.37/1.54 (ifeq2 (abstraction $_428 skc23) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world $_428 skc14) true % 1.37/1.54 (ifeq2 (abstraction $_428 skc28) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world $_428 skc15) true % 1.37/1.54 (ifeq2 (abstraction $_428 skc15) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world $_428 skc15) true % 1.37/1.54 (ifeq2 (abstraction $_428 skc19) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world $_428 skc15) true % 1.37/1.54 (ifeq2 (abstraction $_428 skc23) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world $_428 skc15) true % 1.37/1.54 (ifeq2 (abstraction $_428 skc28) true true true) true = true % 1.37/1.54 |- ifeq2 (accessible_world skc14 $_429) true (abstraction $_429 skc15) % 1.37/1.54 true = true % 1.38/1.54 |- ifeq2 (accessible_world skc14 $_429) true (abstraction $_429 skc19) % 1.38/1.54 true = true % 1.38/1.54 |- ifeq2 (accessible_world skc14 $_429) true (abstraction $_429 skc23) % 1.38/1.54 true = true % 1.38/1.54 |- ifeq2 (accessible_world skc14 $_429) true (abstraction $_429 skc28) % 1.38/1.54 true = true % 1.38/1.54 |- ifeq2 (accessible_world skc15 $_429) true (abstraction $_429 skc15) % 1.38/1.54 true = true % 1.38/1.54 |- ifeq2 (accessible_world skc15 $_429) true (abstraction $_429 skc19) % 1.38/1.54 true = true % 1.38/1.54 |- ifeq2 (accessible_world skc15 $_429) true (abstraction $_429 skc23) % 1.38/1.54 true = true % 1.38/1.54 |- ifeq2 (accessible_world skc15 $_429) true (abstraction $_429 skc28) % 1.38/1.54 true = true % 1.38/1.54 |- ifeq2 (abstraction skc14 $_430) true (abstraction skc15 $_430) true = % 1.38/1.54 true % 1.38/1.54 |- ifeq2 (accessible_world $_469 skc14) true % 1.38/1.54 (ifeq2 (nonhuman $_469 skc15) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world $_469 skc14) true % 1.38/1.54 (ifeq2 (nonhuman $_469 skc19) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world $_469 skc14) true % 1.38/1.54 (ifeq2 (nonhuman $_469 skc23) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world $_469 skc14) true % 1.38/1.54 (ifeq2 (nonhuman $_469 skc28) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world $_469 skc15) true % 1.38/1.54 (ifeq2 (nonhuman $_469 skc15) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world $_469 skc15) true % 1.38/1.54 (ifeq2 (nonhuman $_469 skc19) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world $_469 skc15) true % 1.38/1.54 (ifeq2 (nonhuman $_469 skc23) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world $_469 skc15) true % 1.38/1.54 (ifeq2 (nonhuman $_469 skc28) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world skc14 $_470) true (nonhuman $_470 skc15) true = % 1.38/1.54 true % 1.38/1.54 |- ifeq2 (accessible_world skc14 $_470) true (nonhuman $_470 skc19) true = % 1.38/1.54 true % 1.38/1.54 |- ifeq2 (accessible_world skc14 $_470) true (nonhuman $_470 skc23) true = % 1.38/1.54 true % 1.38/1.54 |- ifeq2 (accessible_world skc14 $_470) true (nonhuman $_470 skc28) true = % 1.38/1.54 true % 1.38/1.54 |- ifeq2 (accessible_world skc15 $_470) true (nonhuman $_470 skc15) true = % 1.38/1.54 true % 1.38/1.54 |- ifeq2 (accessible_world skc15 $_470) true (nonhuman $_470 skc19) true = % 1.38/1.54 true % 1.38/1.54 |- ifeq2 (accessible_world skc15 $_470) true (nonhuman $_470 skc23) true = % 1.38/1.54 true % 1.38/1.54 |- ifeq2 (accessible_world skc15 $_470) true (nonhuman $_470 skc28) true = % 1.38/1.54 true % 1.38/1.54 |- ifeq2 (nonhuman skc14 $_471) true (nonhuman skc15 $_471) true = true % 1.38/1.54 |- ifeq2 (accessible_world $_510 skc14) true % 1.38/1.54 (ifeq2 (state $_510 skc26) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world skc14 $_511) true (state $_511 skc26) true = % 1.38/1.54 true % 1.38/1.54 |- ifeq2 (state skc14 $_512) true (state skc15 $_512) true = true % 1.38/1.54 |- state skc15 skc26 = true % 1.38/1.54 |- ifeq2 (accessible_world skc15 $V) true (state $V skc26) true = true % 1.38/1.54 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.54 (ifeq2 (state $U skc26) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world $_521 skc14) true % 1.38/1.54 (ifeq2 (man $_521 skc20) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world $_521 skc14) true % 1.38/1.54 (ifeq2 (man $_521 skc24) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world $_521 skc14) true % 1.38/1.54 (ifeq2 (man $_521 skc27) true true true) true = true % 1.38/1.54 |- ifeq2 (accessible_world skc14 $_522) true (man $_522 skc20) true = true % 1.38/1.54 |- ifeq2 (accessible_world skc14 $_522) true (man $_522 skc24) true = true % 1.38/1.54 |- ifeq2 (accessible_world skc14 $_522) true (man $_522 skc27) true = true % 1.38/1.54 |- ifeq2 (man skc14 $_523) true (man skc15 $_523) true = true % 1.38/1.54 |- man skc15 skc20 = true % 1.38/1.54 |- smoke skc15 (skf1 $V) = true % 1.38/1.54 |- event skc15 (skf1 $V) = true % 1.38/1.54 |- present skc15 (skf1 $V) = true % 1.38/1.54 |- agent skc15 (skf1 skc20) skc20 = true % 1.38/1.54 |- ifeq2 (accessible_world skc15 $V) true (man $V skc20) true = true % 1.38/1.54 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.54 (ifeq2 (man $U skc20) true true true) true = true % 1.38/1.54 |- human_person skc15 skc20 = true % 1.38/1.54 |- male skc15 skc20 = true % 1.38/1.54 |- animate skc15 skc20 = true % 1.38/1.54 |- human skc15 skc20 = true % 1.38/1.54 |- organism skc15 skc20 = true % 1.38/1.54 |- ifeq (tuple (unisex skc15 skc20) true) (tuple true true) a b = b % 1.38/1.54 |- ifeq (tuple (nonhuman skc15 skc20) true) (tuple true true) a b = b % 1.38/1.54 |- living skc15 skc20 = true % 1.38/1.54 |- impartial skc15 skc20 = true % 1.38/1.54 |- entity skc15 skc20 = true % 1.38/1.54 |- existent skc15 skc20 = true % 1.38/1.54 |- ifeq (tuple (nonexistent skc15 skc20) true) (tuple true true) a b = b % 1.38/1.54 |- ifeq2 (accessible_world skc15 $V) true (present $V (skf1 $_525)) true = % 1.38/1.54 true % 1.38/1.54 |- ifeq2 (present $U (skf1 $_525)) true % 1.38/1.54 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.38/1.54 |- ifeq2 (present skc14 (skf1 $_525)) true true true = true % 1.38/1.54 |- ifeq2 (accessible_world skc15 $V) true (event $V (skf1 $_526)) true = % 1.38/1.54 true % 1.38/1.54 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.54 (ifeq2 (event $U (skf1 $_526)) true true true) true = true % 1.38/1.54 |- ifeq2 (state skc15 (skf1 $_526)) true true true = true % 1.38/1.54 |- eventuality skc15 (skf1 $_526) = true % 1.38/1.54 |- ifeq2 (event skc14 (skf1 $_526)) true true true = true % 1.38/1.54 |- ifeq2 (accessible_world skc15 $V) true (eventuality $V (skf1 $_527)) % 1.38/1.54 true = true % 1.38/1.55 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.55 (ifeq2 (eventuality $U (skf1 $_527)) true true true) true = true % 1.38/1.55 |- specific skc15 (skf1 $_527) = true % 1.38/1.55 |- unisex skc15 (skf1 $_527) = true % 1.38/1.55 |- nonexistent skc15 (skf1 $_527) = true % 1.38/1.55 |- thing skc15 (skf1 $_527) = true % 1.38/1.55 |- ifeq2 (eventuality skc14 (skf1 $_527)) true true true = true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $V) true (smoke $V (skf1 $_528)) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.55 (ifeq2 (smoke $U (skf1 $_528)) true true true) true = true % 1.38/1.55 |- ifeq2 (smoke skc14 (skf1 $_528)) true true true = true % 1.38/1.55 |- ifeq (tuple true (existent skc15 (skf1 $_529))) (tuple true true) a b = % 1.38/1.55 b % 1.38/1.55 |- ifeq2 (accessible_world skc15 $V) true (thing $V (skf1 $_530)) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.55 (ifeq2 (thing $U (skf1 $_530)) true true true) true = true % 1.38/1.55 |- singleton skc15 (skf1 $_530) = true % 1.38/1.55 |- ifeq2 (entity skc15 (skf1 $_530)) true true true = true % 1.38/1.55 |- ifeq2 (abstraction skc15 (skf1 $_530)) true true true = true % 1.38/1.55 |- ifeq2 (thing skc14 (skf1 $_530)) true true true = true % 1.38/1.55 |- man skc15 skc24 = true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $V) true (man $V skc24) true = true % 1.38/1.55 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.55 (ifeq2 (man $U skc24) true true true) true = true % 1.38/1.55 |- human_person skc15 skc24 = true % 1.38/1.55 |- male skc15 skc24 = true % 1.38/1.55 |- agent skc15 (skf1 skc24) skc24 = true % 1.38/1.55 |- animate skc15 skc24 = true % 1.38/1.55 |- human skc15 skc24 = true % 1.38/1.55 |- organism skc15 skc24 = true % 1.38/1.55 |- ifeq (tuple (unisex skc15 skc24) true) (tuple true true) a b = b % 1.38/1.55 |- ifeq (tuple (nonhuman skc15 skc24) true) (tuple true true) a b = b % 1.38/1.55 |- living skc15 skc24 = true % 1.38/1.55 |- impartial skc15 skc24 = true % 1.38/1.55 |- entity skc15 skc24 = true % 1.38/1.55 |- existent skc15 skc24 = true % 1.38/1.55 |- ifeq (tuple (nonexistent skc15 skc24) true) (tuple true true) a b = b % 1.38/1.55 |- man skc15 skc27 = true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $V) true (man $V skc27) true = true % 1.38/1.55 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.55 (ifeq2 (man $U skc27) true true true) true = true % 1.38/1.55 |- human_person skc15 skc27 = true % 1.38/1.55 |- male skc15 skc27 = true % 1.38/1.55 |- agent skc15 (skf1 skc27) skc27 = true % 1.38/1.55 |- animate skc15 skc27 = true % 1.38/1.55 |- human skc15 skc27 = true % 1.38/1.55 |- organism skc15 skc27 = true % 1.38/1.55 |- ifeq (tuple (unisex skc15 skc27) true) (tuple true true) a b = b % 1.38/1.55 |- ifeq (tuple (nonhuman skc15 skc27) true) (tuple true true) a b = b % 1.38/1.55 |- living skc15 skc27 = true % 1.38/1.55 |- impartial skc15 skc27 = true % 1.38/1.55 |- entity skc15 skc27 = true % 1.38/1.55 |- existent skc15 skc27 = true % 1.38/1.55 |- ifeq (tuple (nonexistent skc15 skc27) true) (tuple true true) a b = b % 1.38/1.55 |- ifeq2 (accessible_world skc15 $V) true (specific $V (skf1 $_535)) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.55 (ifeq2 (specific $U (skf1 $_535)) true true true) true = true % 1.38/1.55 |- ifeq (tuple true (general skc15 (skf1 $_535))) (tuple true true) a b = b % 1.38/1.55 |- ifeq2 (specific skc14 (skf1 $_535)) true true true = true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $V) true (singleton $V (skf1 $_536)) % 1.38/1.55 true = true % 1.38/1.55 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.55 (ifeq2 (singleton $U (skf1 $_536)) true true true) true = true % 1.38/1.55 |- ifeq2 (singleton skc14 (skf1 $_536)) true true true = true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $V) true (unisex $V (skf1 $_538)) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.55 (ifeq2 (unisex $U (skf1 $_538)) true true true) true = true % 1.38/1.55 |- ifeq (tuple true (male skc15 (skf1 $_538))) (tuple true true) a b = b % 1.38/1.55 |- ifeq2 (unisex skc14 (skf1 $_538)) true true true = true % 1.38/1.55 |- ifeq2 (accessible_world $_558 skc14) true % 1.38/1.55 (ifeq2 (human_person $_558 skc20) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_558 skc14) true % 1.38/1.55 (ifeq2 (human_person $_558 skc24) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_558 skc14) true % 1.38/1.55 (ifeq2 (human_person $_558 skc27) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_558 skc15) true % 1.38/1.55 (ifeq2 (human_person $_558 skc20) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_558 skc15) true % 1.38/1.55 (ifeq2 (human_person $_558 skc24) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_558 skc15) true % 1.38/1.55 (ifeq2 (human_person $_558 skc27) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_559) true (human_person $_559 skc20) % 1.38/1.55 true = true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_559) true (human_person $_559 skc24) % 1.38/1.55 true = true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_559) true (human_person $_559 skc27) % 1.38/1.55 true = true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_559) true (human_person $_559 skc20) % 1.38/1.55 true = true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_559) true (human_person $_559 skc24) % 1.38/1.55 true = true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_559) true (human_person $_559 skc27) % 1.38/1.55 true = true % 1.38/1.55 |- ifeq2 (human_person skc14 $_560) true (human_person skc15 $_560) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world $_581 skc14) true % 1.38/1.55 (ifeq2 (organism $_581 skc20) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_581 skc14) true % 1.38/1.55 (ifeq2 (organism $_581 skc24) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_581 skc14) true % 1.38/1.55 (ifeq2 (organism $_581 skc27) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_581 skc15) true % 1.38/1.55 (ifeq2 (organism $_581 skc20) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_581 skc15) true % 1.38/1.55 (ifeq2 (organism $_581 skc24) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_581 skc15) true % 1.38/1.55 (ifeq2 (organism $_581 skc27) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_582) true (organism $_582 skc20) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_582) true (organism $_582 skc24) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_582) true (organism $_582 skc27) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_582) true (organism $_582 skc20) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_582) true (organism $_582 skc24) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_582) true (organism $_582 skc27) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (organism skc14 $_583) true (organism skc15 $_583) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_604 skc14) true % 1.38/1.55 (ifeq2 (entity $_604 skc20) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_604 skc14) true % 1.38/1.55 (ifeq2 (entity $_604 skc24) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_604 skc14) true % 1.38/1.55 (ifeq2 (entity $_604 skc27) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_604 skc15) true % 1.38/1.55 (ifeq2 (entity $_604 skc20) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_604 skc15) true % 1.38/1.55 (ifeq2 (entity $_604 skc24) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_604 skc15) true % 1.38/1.55 (ifeq2 (entity $_604 skc27) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_605) true (entity $_605 skc20) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_605) true (entity $_605 skc24) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_605) true (entity $_605 skc27) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_605) true (entity $_605 skc20) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_605) true (entity $_605 skc24) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_605) true (entity $_605 skc27) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (entity skc14 $_606) true (entity skc15 $_606) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_627 skc14) true % 1.38/1.55 (ifeq2 (existent $_627 skc20) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_627 skc14) true % 1.38/1.55 (ifeq2 (existent $_627 skc24) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_627 skc14) true % 1.38/1.55 (ifeq2 (existent $_627 skc27) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_627 skc15) true % 1.38/1.55 (ifeq2 (existent $_627 skc20) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_627 skc15) true % 1.38/1.55 (ifeq2 (existent $_627 skc24) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_627 skc15) true % 1.38/1.55 (ifeq2 (existent $_627 skc27) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_628) true (existent $_628 skc20) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_628) true (existent $_628 skc24) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_628) true (existent $_628 skc27) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_628) true (existent $_628 skc20) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_628) true (existent $_628 skc24) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_628) true (existent $_628 skc27) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (existent skc14 $_629) true (existent skc15 $_629) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_650 skc14) true % 1.38/1.55 (ifeq2 (impartial $_650 skc20) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_650 skc14) true % 1.38/1.55 (ifeq2 (impartial $_650 skc24) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_650 skc14) true % 1.38/1.55 (ifeq2 (impartial $_650 skc27) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_650 skc15) true % 1.38/1.55 (ifeq2 (impartial $_650 skc20) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_650 skc15) true % 1.38/1.55 (ifeq2 (impartial $_650 skc24) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world $_650 skc15) true % 1.38/1.55 (ifeq2 (impartial $_650 skc27) true true true) true = true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_651) true (impartial $_651 skc20) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_651) true (impartial $_651 skc24) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc14 $_651) true (impartial $_651 skc27) true = % 1.38/1.55 true % 1.38/1.55 |- ifeq2 (accessible_world skc15 $_651) true (impartial $_651 skc20) true = % 1.38/1.55 true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_651) true (impartial $_651 skc24) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_651) true (impartial $_651 skc27) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (impartial skc14 $_652) true (impartial skc15 $_652) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_673 skc14) true % 1.38/1.56 (ifeq2 (human $_673 skc20) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_673 skc14) true % 1.38/1.56 (ifeq2 (human $_673 skc24) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_673 skc14) true % 1.38/1.56 (ifeq2 (human $_673 skc27) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_673 skc15) true % 1.38/1.56 (ifeq2 (human $_673 skc20) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_673 skc15) true % 1.38/1.56 (ifeq2 (human $_673 skc24) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_673 skc15) true % 1.38/1.56 (ifeq2 (human $_673 skc27) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_674) true (human $_674 skc20) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_674) true (human $_674 skc24) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_674) true (human $_674 skc27) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_674) true (human $_674 skc20) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_674) true (human $_674 skc24) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_674) true (human $_674 skc27) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (human skc14 $_675) true (human skc15 $_675) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_696 skc14) true % 1.38/1.56 (ifeq2 (animate $_696 skc20) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_696 skc14) true % 1.38/1.56 (ifeq2 (animate $_696 skc24) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_696 skc14) true % 1.38/1.56 (ifeq2 (animate $_696 skc27) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_696 skc15) true % 1.38/1.56 (ifeq2 (animate $_696 skc20) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_696 skc15) true % 1.38/1.56 (ifeq2 (animate $_696 skc24) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_696 skc15) true % 1.38/1.56 (ifeq2 (animate $_696 skc27) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_697) true (animate $_697 skc20) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_697) true (animate $_697 skc24) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_697) true (animate $_697 skc27) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_697) true (animate $_697 skc20) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_697) true (animate $_697 skc24) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_697) true (animate $_697 skc27) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (animate skc14 $_698) true (animate skc15 $_698) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_719 skc14) true % 1.38/1.56 (ifeq2 (male $_719 skc20) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_719 skc14) true % 1.38/1.56 (ifeq2 (male $_719 skc24) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_719 skc14) true % 1.38/1.56 (ifeq2 (male $_719 skc27) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_719 skc15) true % 1.38/1.56 (ifeq2 (male $_719 skc20) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_719 skc15) true % 1.38/1.56 (ifeq2 (male $_719 skc24) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_719 skc15) true % 1.38/1.56 (ifeq2 (male $_719 skc27) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_720) true (male $_720 skc20) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_720) true (male $_720 skc24) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_720) true (male $_720 skc27) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_720) true (male $_720 skc20) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_720) true (male $_720 skc24) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_720) true (male $_720 skc27) true = true % 1.38/1.56 |- ifeq2 (male skc14 $_721) true (male skc15 $_721) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_742 skc14) true % 1.38/1.56 (ifeq2 (forename $_742 skc19) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_742 skc14) true % 1.38/1.56 (ifeq2 (forename $_742 skc23) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_742 skc14) true % 1.38/1.56 (ifeq2 (forename $_742 skc28) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_743) true (forename $_743 skc19) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_743) true (forename $_743 skc23) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_743) true (forename $_743 skc28) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (forename skc14 $_744) true (forename skc15 $_744) true = true % 1.38/1.56 |- forename skc15 skc19 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (forename $V skc19) true = true % 1.38/1.56 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.56 (ifeq2 (forename $U skc19) true true true) true = true % 1.38/1.56 |- ifeq2 (jules_forename skc15 skc19) true true true = true % 1.38/1.56 |- relname skc15 skc19 = true % 1.38/1.56 |- forename skc15 skc23 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (forename $V skc23) true = true % 1.38/1.56 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.56 (ifeq2 (forename $U skc23) true true true) true = true % 1.38/1.56 |- ifeq2 (vincent_forename skc15 skc23) true true true = true % 1.38/1.56 |- relname skc15 skc23 = true % 1.38/1.56 |- forename skc15 skc28 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (forename $V skc28) true = true % 1.38/1.56 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.56 (ifeq2 (forename $U skc28) true true true) true = true % 1.38/1.56 |- ifeq2 (vincent_forename skc15 skc28) true true true = true % 1.38/1.56 |- relname skc15 skc28 = true % 1.38/1.56 |- ifeq2 (accessible_world $_766 skc14) true % 1.38/1.56 (ifeq2 (relname $_766 skc19) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_766 skc14) true % 1.38/1.56 (ifeq2 (relname $_766 skc23) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_766 skc14) true % 1.38/1.56 (ifeq2 (relname $_766 skc28) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_766 skc15) true % 1.38/1.56 (ifeq2 (relname $_766 skc19) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_766 skc15) true % 1.38/1.56 (ifeq2 (relname $_766 skc23) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_766 skc15) true % 1.38/1.56 (ifeq2 (relname $_766 skc28) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_767) true (relname $_767 skc19) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_767) true (relname $_767 skc23) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_767) true (relname $_767 skc28) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_767) true (relname $_767 skc19) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_767) true (relname $_767 skc23) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_767) true (relname $_767 skc28) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (relname skc14 $_768) true (relname skc15 $_768) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_795 skc14) true % 1.38/1.56 (ifeq2 (vincent_forename $_795 skc19) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_796) true (vincent_forename $_796 skc19) % 1.38/1.56 true = true % 1.38/1.56 |- ifeq2 (vincent_forename skc14 $_797) true (vincent_forename skc15 $_797) % 1.38/1.56 true = true % 1.38/1.56 |- vincent_forename skc15 skc19 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (vincent_forename $V skc19) % 1.38/1.56 true = true % 1.38/1.56 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.56 (ifeq2 (vincent_forename $U skc19) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_812 skc14) true % 1.38/1.56 (ifeq2 (jules_forename $_812 skc23) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_812 skc14) true % 1.38/1.56 (ifeq2 (jules_forename $_812 skc28) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_813) true (jules_forename $_813 skc23) % 1.38/1.56 true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_813) true (jules_forename $_813 skc28) % 1.38/1.56 true = true % 1.38/1.56 |- ifeq2 (jules_forename skc14 $_814) true (jules_forename skc15 $_814) % 1.38/1.56 true = true % 1.38/1.56 |- jules_forename skc15 skc23 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (jules_forename $V skc23) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.56 (ifeq2 (jules_forename $U skc23) true true true) true = true % 1.38/1.56 |- jules_forename skc15 skc28 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (jules_forename $V skc28) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world $U skc15) true % 1.38/1.56 (ifeq2 (jules_forename $U skc28) true true true) true = true % 1.38/1.56 |- ifeq2 (agent $_921 skc16 skc20) true % 1.38/1.56 (ifeq2 (accessible_world $_921 skc14) true true true) true = true % 1.38/1.56 |- ifeq2 (agent $_921 skc18 skc20) true % 1.38/1.56 (ifeq2 (accessible_world $_921 skc14) true true true) true = true % 1.38/1.56 |- ifeq2 (agent $_921 skc25 skc24) true % 1.38/1.56 (ifeq2 (accessible_world $_921 skc15) true true true) true = true % 1.38/1.56 |- ifeq2 (agent $_921 (skf1 skc20) skc20) true % 1.38/1.56 (ifeq2 (accessible_world $_921 skc15) true true true) true = true % 1.38/1.56 |- ifeq2 (agent $_921 (skf1 skc24) skc24) true % 1.38/1.56 (ifeq2 (accessible_world $_921 skc15) true true true) true = true % 1.38/1.56 |- ifeq2 (agent $_921 (skf1 skc27) skc27) true % 1.38/1.56 (ifeq2 (accessible_world $_921 skc15) true true true) true = true % 1.38/1.56 |- ifeq2 (agent skc14 $_923 $_924) true (agent skc15 $_923 $_924) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_922) true (agent $_922 skc16 skc20) % 1.38/1.56 true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_922) true (agent $_922 skc18 skc20) % 1.38/1.56 true = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_922) true (agent $_922 skc25 skc24) % 1.38/1.56 true = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_922) true % 1.38/1.56 (agent $_922 (skf1 skc20) skc20) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_922) true % 1.38/1.56 (agent $_922 (skf1 skc24) skc24) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $_922) true % 1.38/1.56 (agent $_922 (skf1 skc27) skc27) true = true % 1.38/1.56 |- agent skc15 skc16 skc20 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (agent $V skc16 skc20) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (agent $U skc16 skc20) true % 1.38/1.56 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.38/1.56 |- agent skc15 skc18 skc20 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (agent $V skc18 skc20) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (agent $U skc18 skc20) true % 1.38/1.56 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.38/1.56 |- ifeq2 (agent skc14 skc25 skc24) true true true = true % 1.38/1.56 |- ifeq2 (agent skc14 (skf1 skc20) skc20) true true true = true % 1.38/1.56 |- ifeq2 (agent skc14 (skf1 skc24) skc24) true true true = true % 1.38/1.56 |- ifeq2 (agent skc14 (skf1 skc27) skc27) true true true = true % 1.38/1.56 |- ifeq2 (theme $_949 skc16 skc15) true % 1.38/1.56 (ifeq2 (accessible_world $_949 skc14) true true true) true = true % 1.38/1.56 |- ifeq2 (theme $_949 skc18 skc15) true % 1.38/1.56 (ifeq2 (accessible_world $_949 skc14) true true true) true = true % 1.38/1.56 |- ifeq2 (theme skc14 $_951 $_952) true (theme skc15 $_951 $_952) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_950) true (theme $_950 skc16 skc15) % 1.38/1.56 true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_950) true (theme $_950 skc18 skc15) % 1.38/1.56 true = true % 1.38/1.56 |- theme skc15 skc16 skc15 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (theme $V skc16 skc15) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (theme $U skc16 skc15) true % 1.38/1.56 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.38/1.56 |- theme skc15 skc18 skc15 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (theme $V skc18 skc15) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (theme $U skc18 skc15) true % 1.38/1.56 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.38/1.56 |- ifeq2 (of $_969 skc19 skc20) true % 1.38/1.56 (ifeq2 (accessible_world $_969 skc14) true true true) true = true % 1.38/1.56 |- ifeq2 (of $_969 skc23 skc24) true % 1.38/1.56 (ifeq2 (accessible_world $_969 skc14) true true true) true = true % 1.38/1.56 |- ifeq2 (of $_969 skc28 skc27) true % 1.38/1.56 (ifeq2 (accessible_world $_969 skc14) true true true) true = true % 1.38/1.56 |- ifeq2 (of skc14 $_971 $_972) true (of skc15 $_971 $_972) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_970) true (of $_970 skc19 skc20) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_970) true (of $_970 skc23 skc24) true = % 1.38/1.56 true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_970) true (of $_970 skc28 skc27) true = % 1.38/1.56 true % 1.38/1.56 |- of skc15 skc19 skc20 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (of $V skc19 skc20) true = true % 1.38/1.56 |- ifeq2 (of $U skc19 skc20) true % 1.38/1.56 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.38/1.56 |- of skc15 skc23 skc24 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (of $V skc23 skc24) true = true % 1.38/1.56 |- ifeq2 (of $U skc23 skc24) true % 1.38/1.56 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.38/1.56 |- of skc15 skc28 skc27 = true % 1.38/1.56 |- ifeq2 (accessible_world skc15 $V) true (of $V skc28 skc27) true = true % 1.38/1.56 |- ifeq2 (of $U skc28 skc27) true % 1.38/1.56 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_1016 skc14) true % 1.38/1.56 (ifeq2 (nonexistent $_1016 skc16) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_1016 skc14) true % 1.38/1.56 (ifeq2 (nonexistent $_1016 skc18) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_1016 skc14) true % 1.38/1.56 (ifeq2 (nonexistent $_1016 skc26) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_1016 skc15) true % 1.38/1.56 (ifeq2 (nonexistent $_1016 skc16) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_1016 skc15) true % 1.38/1.56 (ifeq2 (nonexistent $_1016 skc18) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_1016 skc15) true % 1.38/1.56 (ifeq2 (nonexistent $_1016 skc25) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_1016 skc15) true % 1.38/1.56 (ifeq2 (nonexistent $_1016 skc26) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world $_1016 skc15) true % 1.38/1.56 (ifeq2 (nonexistent $_1016 (skf1 $_527)) true true true) true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_1017) true (nonexistent $_1017 skc16) % 1.38/1.56 true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_1017) true (nonexistent $_1017 skc18) % 1.38/1.56 true = true % 1.38/1.56 |- ifeq2 (accessible_world skc14 $_1017) true (nonexistent $_1017 skc26) % 1.38/1.56 true = true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $_1017) true (nonexistent $_1017 skc16) % 1.38/1.57 true = true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $_1017) true (nonexistent $_1017 skc18) % 1.38/1.57 true = true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $_1017) true (nonexistent $_1017 skc25) % 1.38/1.57 true = true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $_1017) true (nonexistent $_1017 skc26) % 1.38/1.57 true = true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $_1017) true % 1.38/1.57 (nonexistent $_1017 (skf1 $_527)) true = true % 1.38/1.57 |- ifeq2 (nonexistent skc14 $_1018) true (nonexistent skc15 $_1018) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (nonexistent skc14 skc25) true true true = true % 1.38/1.57 |- ifeq2 (nonexistent skc14 (skf1 $_527)) true true true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1046 skc14) true % 1.38/1.57 (ifeq2 (general $_1046 skc15) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1046 skc14) true % 1.38/1.57 (ifeq2 (general $_1046 skc19) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1046 skc14) true % 1.38/1.57 (ifeq2 (general $_1046 skc23) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1046 skc14) true % 1.38/1.57 (ifeq2 (general $_1046 skc28) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1046 skc15) true % 1.38/1.57 (ifeq2 (general $_1046 skc15) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1046 skc15) true % 1.38/1.57 (ifeq2 (general $_1046 skc19) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1046 skc15) true % 1.38/1.57 (ifeq2 (general $_1046 skc23) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1046 skc15) true % 1.38/1.57 (ifeq2 (general $_1046 skc28) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world skc14 $_1047) true (general $_1047 skc15) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (accessible_world skc14 $_1047) true (general $_1047 skc19) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (accessible_world skc14 $_1047) true (general $_1047 skc23) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (accessible_world skc14 $_1047) true (general $_1047 skc28) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $_1047) true (general $_1047 skc15) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $_1047) true (general $_1047 skc19) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $_1047) true (general $_1047 skc23) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $_1047) true (general $_1047 skc28) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (general skc14 $_1048) true (general skc15 $_1048) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1087 skc14) true % 1.38/1.57 (ifeq2 (living $_1087 skc20) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1087 skc14) true % 1.38/1.57 (ifeq2 (living $_1087 skc24) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1087 skc14) true % 1.38/1.57 (ifeq2 (living $_1087 skc27) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1087 skc15) true % 1.38/1.57 (ifeq2 (living $_1087 skc20) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1087 skc15) true % 1.38/1.57 (ifeq2 (living $_1087 skc24) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world $_1087 skc15) true % 1.38/1.57 (ifeq2 (living $_1087 skc27) true true true) true = true % 1.38/1.57 |- ifeq2 (accessible_world skc14 $_1088) true (living $_1088 skc20) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (accessible_world skc14 $_1088) true (living $_1088 skc24) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (accessible_world skc14 $_1088) true (living $_1088 skc27) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $_1088) true (living $_1088 skc20) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $_1088) true (living $_1088 skc24) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $_1088) true (living $_1088 skc27) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (living skc14 $_1089) true (living skc15 $_1089) true = true % 1.38/1.57 |- ifeq2 (be $_1114 skc26 skc27 skc27) true % 1.38/1.57 (ifeq2 (accessible_world $_1114 skc14) true true true) true = true % 1.38/1.57 |- ifeq2 (be skc14 $_1116 $_1117 $_1118) true % 1.38/1.57 (be skc15 $_1116 $_1117 $_1118) true = true % 1.38/1.57 |- ifeq2 (accessible_world skc14 $_1115) true (be $_1115 skc26 skc27 skc27) % 1.38/1.57 true = true % 1.38/1.57 |- be skc15 skc26 skc27 skc27 = true % 1.38/1.57 |- ifeq2 (accessible_world skc15 $V) true (be $V skc26 skc27 skc27) true = % 1.38/1.57 true % 1.38/1.57 |- ifeq2 (be $U skc26 skc27 skc27) true % 1.38/1.57 (ifeq2 (accessible_world $U skc15) true true true) true = true % 1.38/1.57 |- ifeq3 (of skc14 $_1137 skc20) true % 1.38/1.57 (ifeq3 (of skc14 $_1136 skc20) true % 1.38/1.57 (ifeq3 (forename skc14 $_1137) true % 1.38/1.57 (ifeq3 (forename skc14 $_1136) true $_1137 $_1136) $_1136) % 1.38/1.57 $_1136) $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc14 $_1137 skc24) true % 1.38/1.57 (ifeq3 (of skc14 $_1136 skc24) true % 1.38/1.57 (ifeq3 (forename skc14 $_1137) true % 1.38/1.57 (ifeq3 (forename skc14 $_1136) true $_1137 $_1136) $_1136) % 1.38/1.57 $_1136) $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc14 $_1137 skc27) true % 1.38/1.57 (ifeq3 (of skc14 $_1136 skc27) true % 1.38/1.57 (ifeq3 (forename skc14 $_1137) true % 1.38/1.57 (ifeq3 (forename skc14 $_1136) true $_1137 $_1136) $_1136) % 1.38/1.57 $_1136) $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc15 $_1137 skc20) true % 1.38/1.57 (ifeq3 (of skc15 $_1136 skc20) true % 1.38/1.57 (ifeq3 (forename skc15 $_1137) true % 1.38/1.57 (ifeq3 (forename skc15 $_1136) true $_1137 $_1136) $_1136) % 1.38/1.57 $_1136) $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc15 $_1137 skc24) true % 1.38/1.57 (ifeq3 (of skc15 $_1136 skc24) true % 1.38/1.57 (ifeq3 (forename skc15 $_1137) true % 1.38/1.57 (ifeq3 (forename skc15 $_1136) true $_1137 $_1136) $_1136) % 1.38/1.57 $_1136) $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc15 $_1137 skc27) true % 1.38/1.57 (ifeq3 (of skc15 $_1136 skc27) true % 1.38/1.57 (ifeq3 (forename skc15 $_1137) true % 1.38/1.57 (ifeq3 (forename skc15 $_1136) true $_1137 $_1136) $_1136) % 1.38/1.57 $_1136) $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc14 $_1137 $_1138) true % 1.38/1.57 (ifeq3 (of skc14 skc19 $_1138) true % 1.38/1.57 (ifeq3 (forename skc14 $_1137) true % 1.38/1.57 (ifeq3 (entity skc14 $_1138) true $_1137 skc19) skc19) skc19) % 1.38/1.57 skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc14 $_1137 $_1138) true % 1.38/1.57 (ifeq3 (of skc14 skc23 $_1138) true % 1.38/1.57 (ifeq3 (forename skc14 $_1137) true % 1.38/1.57 (ifeq3 (entity skc14 $_1138) true $_1137 skc23) skc23) skc23) % 1.38/1.57 skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc14 $_1137 $_1138) true % 1.38/1.57 (ifeq3 (of skc14 skc28 $_1138) true % 1.38/1.57 (ifeq3 (forename skc14 $_1137) true % 1.38/1.57 (ifeq3 (entity skc14 $_1138) true $_1137 skc28) skc28) skc28) % 1.38/1.57 skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc15 $_1137 $_1138) true % 1.38/1.57 (ifeq3 (of skc15 skc19 $_1138) true % 1.38/1.57 (ifeq3 (forename skc15 $_1137) true % 1.38/1.57 (ifeq3 (entity skc15 $_1138) true $_1137 skc19) skc19) skc19) % 1.38/1.57 skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc15 $_1137 $_1138) true % 1.38/1.57 (ifeq3 (of skc15 skc23 $_1138) true % 1.38/1.57 (ifeq3 (forename skc15 $_1137) true % 1.38/1.57 (ifeq3 (entity skc15 $_1138) true $_1137 skc23) skc23) skc23) % 1.38/1.57 skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc15 $_1137 $_1138) true % 1.38/1.57 (ifeq3 (of skc15 skc28 $_1138) true % 1.38/1.57 (ifeq3 (forename skc15 $_1137) true % 1.38/1.57 (ifeq3 (entity skc15 $_1138) true $_1137 skc28) skc28) skc28) % 1.38/1.57 skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc14 skc19 $_1138) true % 1.38/1.57 (ifeq3 (of skc14 $_1136 $_1138) true % 1.38/1.57 (ifeq3 (forename skc14 $_1136) true % 1.38/1.57 (ifeq3 (entity skc14 $_1138) true skc19 $_1136) $_1136) $_1136) % 1.38/1.57 $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc14 skc23 $_1138) true % 1.38/1.57 (ifeq3 (of skc14 $_1136 $_1138) true % 1.38/1.57 (ifeq3 (forename skc14 $_1136) true % 1.38/1.57 (ifeq3 (entity skc14 $_1138) true skc23 $_1136) $_1136) $_1136) % 1.38/1.57 $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc14 skc28 $_1138) true % 1.38/1.57 (ifeq3 (of skc14 $_1136 $_1138) true % 1.38/1.57 (ifeq3 (forename skc14 $_1136) true % 1.38/1.57 (ifeq3 (entity skc14 $_1138) true skc28 $_1136) $_1136) $_1136) % 1.38/1.57 $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc15 skc19 $_1138) true % 1.38/1.57 (ifeq3 (of skc15 $_1136 $_1138) true % 1.38/1.57 (ifeq3 (forename skc15 $_1136) true % 1.38/1.57 (ifeq3 (entity skc15 $_1138) true skc19 $_1136) $_1136) $_1136) % 1.38/1.57 $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc15 skc23 $_1138) true % 1.38/1.57 (ifeq3 (of skc15 $_1136 $_1138) true % 1.38/1.57 (ifeq3 (forename skc15 $_1136) true % 1.38/1.57 (ifeq3 (entity skc15 $_1138) true skc23 $_1136) $_1136) $_1136) % 1.38/1.57 $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc15 skc28 $_1138) true % 1.38/1.57 (ifeq3 (of skc15 $_1136 $_1138) true % 1.38/1.57 (ifeq3 (forename skc15 $_1136) true % 1.38/1.57 (ifeq3 (entity skc15 $_1138) true skc28 $_1136) $_1136) $_1136) % 1.38/1.57 $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc14 $_1137 skc20) true % 1.38/1.57 (ifeq3 (forename skc14 $_1137) true $_1137 skc19) skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc14 $_1137 skc24) true % 1.38/1.57 (ifeq3 (forename skc14 $_1137) true $_1137 skc23) skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc14 $_1137 skc27) true % 1.38/1.57 (ifeq3 (forename skc14 $_1137) true $_1137 skc28) skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc15 $_1137 skc20) true % 1.38/1.57 (ifeq3 (forename skc15 $_1137) true $_1137 skc19) skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc15 $_1137 skc24) true % 1.38/1.57 (ifeq3 (forename skc15 $_1137) true $_1137 skc23) skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc15 $_1137 skc27) true % 1.38/1.57 (ifeq3 (forename skc15 $_1137) true $_1137 skc28) skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc14 $_1136 skc20) true % 1.38/1.57 (ifeq3 (forename skc14 $_1136) true skc19 $_1136) $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc14 $_1136 skc24) true % 1.38/1.57 (ifeq3 (forename skc14 $_1136) true skc23 $_1136) $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc14 $_1136 skc27) true % 1.38/1.57 (ifeq3 (forename skc14 $_1136) true skc28 $_1136) $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc15 $_1136 skc20) true % 1.38/1.57 (ifeq3 (forename skc15 $_1136) true skc19 $_1136) $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc15 $_1136 skc24) true % 1.38/1.57 (ifeq3 (forename skc15 $_1136) true skc23 $_1136) $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc15 $_1136 skc27) true % 1.38/1.57 (ifeq3 (forename skc15 $_1136) true skc28 $_1136) $_1136 = $_1136 % 1.38/1.57 |- ifeq3 (of skc14 skc19 skc27) true skc19 skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc14 skc23 skc27) true skc23 skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc15 skc19 skc27) true skc19 skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc15 skc23 skc27) true skc23 skc28 = skc28 % 1.38/1.57 |- skc19 = skc21 % 1.38/1.57 |- ifeq3 (of skc14 skc23 skc20) true skc19 skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc14 skc28 skc20) true skc19 skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc14 skc19 skc24) true skc23 skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc14 skc28 skc24) true skc23 skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc14 skc19 skc27) true skc28 skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc14 skc23 skc27) true skc28 skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc15 skc23 skc20) true skc19 skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc15 skc28 skc20) true skc19 skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc15 skc19 skc24) true skc23 skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc15 skc28 skc24) true skc23 skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc15 skc19 skc27) true skc28 skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc15 skc23 skc27) true skc28 skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc14 skc23 skc20) true skc23 skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc14 skc28 skc20) true skc28 skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc14 skc19 skc24) true skc19 skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc14 skc28 skc24) true skc28 skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc15 skc23 skc20) true skc23 skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc15 skc28 skc20) true skc28 skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc15 skc19 skc24) true skc19 skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc15 skc28 skc24) true skc28 skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc14 $_1158 skc20) true % 1.38/1.57 (ifeq3 (of skc14 skc23 skc20) true % 1.38/1.57 (ifeq3 (forename skc14 $_1158) true $_1158 skc23) skc23) skc23 = % 1.38/1.57 skc23 % 1.38/1.57 |- ifeq3 (of skc14 $_1158 skc20) true % 1.38/1.57 (ifeq3 (of skc14 skc28 skc20) true % 1.38/1.57 (ifeq3 (forename skc14 $_1158) true $_1158 skc28) skc28) skc28 = % 1.38/1.57 skc28 % 1.38/1.57 |- ifeq3 (of skc14 skc23 skc20) true % 1.38/1.57 (ifeq3 (of skc14 $_1157 skc20) true % 1.38/1.57 (ifeq3 (forename skc14 $_1157) true skc23 $_1157) $_1157) $_1157 = % 1.38/1.57 $_1157 % 1.38/1.57 |- ifeq3 (of skc14 skc28 skc20) true % 1.38/1.57 (ifeq3 (of skc14 $_1157 skc20) true % 1.38/1.57 (ifeq3 (forename skc14 $_1157) true skc28 $_1157) $_1157) $_1157 = % 1.38/1.57 $_1157 % 1.38/1.57 |- ifeq3 (of skc14 skc23 skc20) true % 1.38/1.57 (ifeq3 (of skc14 skc23 skc20) true skc23 skc23) skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc14 skc23 skc20) true % 1.38/1.57 (ifeq3 (of skc14 skc28 skc20) true skc23 skc28) skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc14 skc28 skc20) true % 1.38/1.57 (ifeq3 (of skc14 skc23 skc20) true skc28 skc23) skc23 = skc23 % 1.38/1.57 |- ifeq3 (of skc14 skc28 skc20) true % 1.38/1.57 (ifeq3 (of skc14 skc28 skc20) true skc28 skc28) skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc14 $_1164 skc24) true % 1.38/1.57 (ifeq3 (of skc14 skc19 skc24) true % 1.38/1.57 (ifeq3 (forename skc14 $_1164) true $_1164 skc19) skc19) skc19 = % 1.38/1.57 skc19 % 1.38/1.57 |- ifeq3 (of skc14 $_1164 skc24) true % 1.38/1.57 (ifeq3 (of skc14 skc28 skc24) true % 1.38/1.57 (ifeq3 (forename skc14 $_1164) true $_1164 skc28) skc28) skc28 = % 1.38/1.57 skc28 % 1.38/1.57 |- ifeq3 (of skc14 skc19 skc24) true % 1.38/1.57 (ifeq3 (of skc14 $_1163 skc24) true % 1.38/1.57 (ifeq3 (forename skc14 $_1163) true skc19 $_1163) $_1163) $_1163 = % 1.38/1.57 $_1163 % 1.38/1.57 |- ifeq3 (of skc14 skc28 skc24) true % 1.38/1.57 (ifeq3 (of skc14 $_1163 skc24) true % 1.38/1.57 (ifeq3 (forename skc14 $_1163) true skc28 $_1163) $_1163) $_1163 = % 1.38/1.57 $_1163 % 1.38/1.57 |- ifeq3 (of skc14 skc19 skc24) true % 1.38/1.57 (ifeq3 (of skc14 skc19 skc24) true skc19 skc19) skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc14 skc19 skc24) true % 1.38/1.57 (ifeq3 (of skc14 skc28 skc24) true skc19 skc28) skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc14 skc28 skc24) true % 1.38/1.57 (ifeq3 (of skc14 skc19 skc24) true skc28 skc19) skc19 = skc19 % 1.38/1.57 |- ifeq3 (of skc14 skc28 skc24) true % 1.38/1.57 (ifeq3 (of skc14 skc28 skc24) true skc28 skc28) skc28 = skc28 % 1.38/1.57 |- ifeq3 (of skc14 $_1170 skc27) true % 1.38/1.57 (ifeq3 (of skc14 skc19 skc27) true % 1.38/1.57 (ifeq3 (forename skc14 $_1170) true $_1170 skc19) skc19) skc19 = % 1.38/1.57 skc19 % 1.38/1.58 |- ifeq3 (of skc14 $_1170 skc27) true % 1.38/1.58 (ifeq3 (of skc14 skc23 skc27) true % 1.38/1.58 (ifeq3 (forename skc14 $_1170) true $_1170 skc23) skc23) skc23 = % 1.38/1.58 skc23 % 1.38/1.58 |- ifeq3 (of skc14 skc19 skc27) true % 1.38/1.58 (ifeq3 (of skc14 $_1169 skc27) true % 1.38/1.58 (ifeq3 (forename skc14 $_1169) true skc19 $_1169) $_1169) $_1169 = % 1.38/1.58 $_1169 % 1.38/1.58 |- ifeq3 (of skc14 skc23 skc27) true % 1.38/1.58 (ifeq3 (of skc14 $_1169 skc27) true % 1.38/1.58 (ifeq3 (forename skc14 $_1169) true skc23 $_1169) $_1169) $_1169 = % 1.38/1.58 $_1169 % 1.38/1.58 |- ifeq3 (of skc14 skc19 skc27) true % 1.38/1.58 (ifeq3 (of skc14 skc19 skc27) true skc19 skc19) skc19 = skc19 % 1.38/1.58 |- ifeq3 (of skc14 skc19 skc27) true % 1.38/1.58 (ifeq3 (of skc14 skc23 skc27) true skc19 skc23) skc23 = skc23 % 1.38/1.58 |- ifeq3 (of skc14 skc23 skc27) true % 1.38/1.58 (ifeq3 (of skc14 skc19 skc27) true skc23 skc19) skc19 = skc19 % 1.38/1.58 |- ifeq3 (of skc14 skc23 skc27) true % 1.38/1.58 (ifeq3 (of skc14 skc23 skc27) true skc23 skc23) skc23 = skc23 % 1.38/1.58 |- ifeq3 (of skc15 $_1176 skc20) true % 1.38/1.58 (ifeq3 (of skc15 skc23 skc20) true % 1.38/1.58 (ifeq3 (forename skc15 $_1176) true $_1176 skc23) skc23) skc23 = % 1.38/1.58 skc23 % 1.38/1.58 |- ifeq3 (of skc15 $_1176 skc20) true % 1.38/1.58 (ifeq3 (of skc15 skc28 skc20) true % 1.38/1.58 (ifeq3 (forename skc15 $_1176) true $_1176 skc28) skc28) skc28 = % 1.38/1.58 skc28 % 1.38/1.58 |- ifeq3 (of skc15 skc23 skc20) true % 1.38/1.58 (ifeq3 (of skc15 $_1175 skc20) true % 1.38/1.58 (ifeq3 (forename skc15 $_1175) true skc23 $_1175) $_1175) $_1175 = % 1.38/1.58 $_1175 % 1.38/1.58 |- ifeq3 (of skc15 skc28 skc20) true % 1.38/1.58 (ifeq3 (of skc15 $_1175 skc20) true % 1.38/1.58 (ifeq3 (forename skc15 $_1175) true skc28 $_1175) $_1175) $_1175 = % 1.38/1.58 $_1175 % 1.38/1.58 |- ifeq3 (of skc15 skc23 skc20) true % 1.38/1.58 (ifeq3 (of skc15 skc23 skc20) true skc23 skc23) skc23 = skc23 % 1.38/1.58 |- ifeq3 (of skc15 skc23 skc20) true % 1.38/1.58 (ifeq3 (of skc15 skc28 skc20) true skc23 skc28) skc28 = skc28 % 1.38/1.58 |- ifeq3 (of skc15 skc28 skc20) true % 1.38/1.58 (ifeq3 (of skc15 skc23 skc20) true skc28 skc23) skc23 = skc23 % 1.38/1.58 |- ifeq3 (of skc15 skc28 skc20) true % 1.38/1.58 (ifeq3 (of skc15 skc28 skc20) true skc28 skc28) skc28 = skc28 % 1.38/1.58 |- ifeq3 (of skc15 $_1182 skc24) true % 1.38/1.58 (ifeq3 (of skc15 skc19 skc24) true % 1.38/1.58 (ifeq3 (forename skc15 $_1182) true $_1182 skc19) skc19) skc19 = % 1.38/1.58 skc19 % 1.38/1.58 |- ifeq3 (of skc15 $_1182 skc24) true % 1.38/1.58 (ifeq3 (of skc15 skc28 skc24) true % 1.38/1.58 (ifeq3 (forename skc15 $_1182) true $_1182 skc28) skc28) skc28 = % 1.38/1.58 skc28 % 1.38/1.58 |- ifeq3 (of skc15 skc19 skc24) true % 1.38/1.58 (ifeq3 (of skc15 $_1181 skc24) true % 1.38/1.58 (ifeq3 (forename skc15 $_1181) true skc19 $_1181) $_1181) $_1181 = % 1.38/1.58 $_1181 % 1.38/1.58 |- ifeq3 (of skc15 skc28 skc24) true % 1.38/1.58 (ifeq3 (of skc15 $_1181 skc24) true % 1.38/1.58 (ifeq3 (forename skc15 $_1181) true skc28 $_1181) $_1181) $_1181 = % 1.38/1.58 $_1181 % 1.38/1.58 |- ifeq3 (of skc15 skc19 skc24) true % 1.38/1.58 (ifeq3 (of skc15 skc19 skc24) true skc19 skc19) skc19 = skc19 % 1.38/1.58 |- ifeq3 (of skc15 skc19 skc24) true % 1.38/1.58 (ifeq3 (of skc15 skc28 skc24) true skc19 skc28) skc28 = skc28 % 1.38/1.58 |- ifeq3 (of skc15 skc28 skc24) true % 1.38/1.58 (ifeq3 (of skc15 skc19 skc24) true skc28 skc19) skc19 = skc19 % 1.38/1.58 |- ifeq3 (of skc15 skc28 skc24) true % 1.38/1.58 (ifeq3 (of skc15 skc28 skc24) true skc28 skc28) skc28 = skc28 % 1.38/1.58 |- ifeq3 (of skc15 $_1188 skc27) true % 1.38/1.58 (ifeq3 (of skc15 skc19 skc27) true % 1.38/1.58 (ifeq3 (forename skc15 $_1188) true $_1188 skc19) skc19) skc19 = % 1.38/1.58 skc19 % 1.38/1.58 |- ifeq3 (of skc15 $_1188 skc27) true % 1.38/1.58 (ifeq3 (of skc15 skc23 skc27) true % 1.38/1.58 (ifeq3 (forename skc15 $_1188) true $_1188 skc23) skc23) skc23 = % 1.38/1.58 skc23 % 1.38/1.58 |- ifeq3 (of skc15 skc19 skc27) true % 1.38/1.58 (ifeq3 (of skc15 $_1187 skc27) true % 1.38/1.58 (ifeq3 (forename skc15 $_1187) true skc19 $_1187) $_1187) $_1187 = % 1.38/1.58 $_1187 % 1.38/1.58 |- ifeq3 (of skc15 skc23 skc27) true % 1.38/1.58 (ifeq3 (of skc15 $_1187 skc27) true % 1.38/1.58 (ifeq3 (forename skc15 $_1187) true skc23 $_1187) $_1187) $_1187 = % 1.38/1.58 $_1187 % 1.38/1.58 |- ifeq3 (of skc15 skc19 skc27) true % 1.38/1.58 (ifeq3 (of skc15 skc19 skc27) true skc19 skc19) skc19 = skc19 % 1.38/1.58 |- ifeq3 (of skc15 skc19 skc27) true % 1.38/1.58 (ifeq3 (of skc15 skc23 skc27) true skc19 skc23) skc23 = skc23 % 1.38/1.58 |- ifeq3 (of skc15 skc23 skc27) true % 1.38/1.58 (ifeq3 (of skc15 skc19 skc27) true skc23 skc19) skc19 = skc19 % 1.38/1.58 |- ifeq3 (of skc15 skc23 skc27) true % 1.38/1.58 (ifeq3 (of skc15 skc23 skc27) true skc23 skc23) skc23 = skc23 % 1.38/1.58 |- ifeq3 (of skc14 skc19 $_1212) true % 1.38/1.58 (ifeq3 (of skc14 skc19 $_1212) true % 1.38/1.58 (ifeq3 (entity skc14 $_1212) true skc19 skc19) skc19) skc19 = skc19 % 1.38/1.58 |- ifeq3 (of skc14 skc23 $_1212) true % 1.38/1.58 (ifeq3 (of skc14 skc19 $_1212) true % 1.38/1.58 (ifeq3 (entity skc14 $_1212) true skc23 skc19) skc19) skc19 = skc19 % 1.38/1.58 |- ifeq3 (of skc14 skc28 $_1212) true % 1.38/1.58 (ifeq3 (of skc14 skc19 $_1212) true % 1.38/1.58 (ifeq3 (entity skc14 $_1212) true skc28 skc19) skc19) skc19 = skc19 % 1.38/1.58 |- ifeq3 (of skc14 skc19 $_1217) true % 1.38/1.58 (ifeq3 (of skc14 skc23 $_1217) true % 1.38/1.58 (ifeq3 (entity skc14 $_1217) true skc19 skc23) skc23) skc23 = skc23 % 1.38/1.58 |- ifeq3 (of skc14 skc23 $_1217) true % 1.38/1.58 (ifeq3 (of skc14 skc23 $_1217) true % 1.38/1.58 (ifeq3 (entity skc14 $_1217) true skc23 skc23) skc23) skc23 = skc23 % 1.38/1.58 |- ifeq3 (of skc14 skc28 $_1217) true % 1.38/1.58 (ifeq3 (of skc14 skc23 $_1217) true % 1.38/1.58 (ifeq3 (entity skc14 $_1217) true skc28 skc23) skc23) skc23 = skc23 % 1.38/1.58 |- ifeq3 (of skc14 skc19 $_1222) true % 1.38/1.58 (ifeq3 (of skc14 skc28 $_1222) true % 1.38/1.58 (ifeq3 (entity skc14 $_1222) true skc19 skc28) skc28) skc28 = skc28 % 1.38/1.58 |- ifeq3 (of skc14 skc23 $_1222) true % 1.38/1.58 (ifeq3 (of skc14 skc28 $_1222) true % 1.38/1.58 (ifeq3 (entity skc14 $_1222) true skc23 skc28) skc28) skc28 = skc28 % 1.38/1.58 |- ifeq3 (of skc14 skc28 $_1222) true % 1.38/1.58 (ifeq3 (of skc14 skc28 $_1222) true % 1.38/1.58 (ifeq3 (entity skc14 $_1222) true skc28 skc28) skc28) skc28 = skc28 % 1.38/1.58 |- ifeq3 (of skc15 skc19 $_1227) true % 1.38/1.58 (ifeq3 (of skc15 skc19 $_1227) true % 1.38/1.58 (ifeq3 (entity skc15 $_1227) true skc19 skc19) skc19) skc19 = skc19 % 1.38/1.58 |- ifeq3 (of skc15 skc23 $_1227) true % 1.38/1.58 (ifeq3 (of skc15 skc19 $_1227) true % 1.38/1.58 (ifeq3 (entity skc15 $_1227) true skc23 skc19) skc19) skc19 = skc19 % 1.38/1.58 |- ifeq3 (of skc15 skc28 $_1227) true % 1.38/1.58 (ifeq3 (of skc15 skc19 $_1227) true % 1.38/1.58 (ifeq3 (entity skc15 $_1227) true skc28 skc19) skc19) skc19 = skc19 % 1.38/1.58 |- ifeq3 (of skc15 skc19 $_1232) true % 1.38/1.58 (ifeq3 (of skc15 skc23 $_1232) true % 1.38/1.58 (ifeq3 (entity skc15 $_1232) true skc19 skc23) skc23) skc23 = skc23 % 1.38/1.58 |- ifeq3 (of skc15 skc23 $_1232) true % 1.38/1.58 (ifeq3 (of skc15 skc23 $_1232) true % 1.38/1.58 (ifeq3 (entity skc15 $_1232) true skc23 skc23) skc23) skc23 = skc23 % 1.38/1.58 |- ifeq3 (of skc15 skc28 $_1232) true % 1.38/1.58 (ifeq3 (of skc15 skc23 $_1232) true % 1.38/1.58 (ifeq3 (entity skc15 $_1232) true skc28 skc23) skc23) skc23 = skc23 % 1.38/1.58 |- ifeq3 (of skc15 skc19 $_1237) true % 1.38/1.58 (ifeq3 (of skc15 skc28 $_1237) true % 1.38/1.58 (ifeq3 (entity skc15 $_1237) true skc19 skc28) skc28) skc28 = skc28 % 1.38/1.58 |- ifeq3 (of skc15 skc23 $_1237) true % 1.38/1.58 (ifeq3 (of skc15 skc28 $_1237) true % 1.38/1.58 (ifeq3 (entity skc15 $_1237) true skc23 skc28) skc28) skc28 = skc28 % 1.38/1.58 |- ifeq3 (of skc15 skc28 $_1237) true % 1.38/1.58 (ifeq3 (of skc15 skc28 $_1237) true % 1.38/1.58 (ifeq3 (entity skc15 $_1237) true skc28 skc28) skc28) skc28 = skc28 % 1.38/1.58 |- ifeq3 (theme skc14 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc14 $_1283 skc15) true % 1.38/1.58 (ifeq3 (agent skc14 $_1284 $_1285) true % 1.38/1.58 (ifeq3 (agent skc14 $_1283 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1284) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1282) true skc15 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 $_1283 skc15) true % 1.38/1.58 (ifeq3 (agent skc15 $_1284 $_1285) true % 1.38/1.58 (ifeq3 (agent skc15 $_1283 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1284) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true skc15 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc14 $_1284 skc15) true % 1.38/1.58 (ifeq3 (theme skc14 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc14 $_1284 $_1285) true % 1.38/1.58 (ifeq3 (agent skc14 $_1283 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1284) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1281) true $_1281 skc15) % 1.38/1.58 skc15) skc15) skc15) skc15) skc15) skc15 = skc15 % 1.38/1.58 |- ifeq3 (theme skc15 $_1284 skc15) true % 1.38/1.58 (ifeq3 (theme skc15 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1284 $_1285) true % 1.38/1.58 (ifeq3 (agent skc15 $_1283 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1284) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 skc15) % 1.38/1.58 skc15) skc15) skc15) skc15) skc15) skc15 = skc15 % 1.38/1.58 |- ifeq3 (theme skc14 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc14 skc16 $_1281) true % 1.38/1.58 (ifeq3 (agent skc14 $_1284 $_1285) true % 1.38/1.58 (ifeq3 (agent skc14 skc16 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1284) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc14 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc14 skc18 $_1281) true % 1.38/1.58 (ifeq3 (agent skc14 $_1284 $_1285) true % 1.38/1.58 (ifeq3 (agent skc14 skc18 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1284) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 skc16 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1284 $_1285) true % 1.38/1.58 (ifeq3 (agent skc15 skc16 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1284) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 skc18 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1284 $_1285) true % 1.38/1.58 (ifeq3 (agent skc15 skc18 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1284) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc14 skc16 $_1282) true % 1.38/1.58 (ifeq3 (theme skc14 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc14 skc16 $_1285) true % 1.38/1.58 (ifeq3 (agent skc14 $_1283 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc14 skc18 $_1282) true % 1.38/1.58 (ifeq3 (theme skc14 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc14 skc18 $_1285) true % 1.38/1.58 (ifeq3 (agent skc14 $_1283 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 skc16 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 skc16 $_1285) true % 1.38/1.58 (ifeq3 (agent skc15 $_1283 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 skc18 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 skc18 $_1285) true % 1.38/1.58 (ifeq3 (agent skc15 $_1283 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc14 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc14 skc16 $_1281) true % 1.38/1.58 (ifeq3 (agent skc14 $_1284 skc20) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1284) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc14 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc14 skc18 $_1281) true % 1.38/1.58 (ifeq3 (agent skc14 $_1284 skc20) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1284) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 skc16 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1284 skc20) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1284) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 skc18 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1284 skc20) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1284) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 skc25 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1284 skc24) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1284) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 (skf1 skc20) $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1284 skc20) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1284) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 (skf1 skc24) $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1284 skc24) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1284) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 (skf1 skc27) $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1284 skc27) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1284) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc14 skc16 $_1282) true % 1.38/1.58 (ifeq3 (theme skc14 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc14 $_1283 skc20) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc14 skc18 $_1282) true % 1.38/1.58 (ifeq3 (theme skc14 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc14 $_1283 skc20) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 skc16 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1283 skc20) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 skc18 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1283 skc20) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 skc25 $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1283 skc24) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 (skf1 skc20) $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1283 skc20) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 (skf1 skc24) $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1283 skc24) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 (skf1 skc27) $_1282) true % 1.38/1.58 (ifeq3 (theme skc15 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 $_1283 skc27) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 $_1282) % 1.38/1.58 $_1282) $_1282) $_1282) $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc14 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (agent skc14 $_1284 $_1285) true % 1.38/1.58 (ifeq3 (agent skc14 skc16 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1284) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1282) true skc15 $_1282) $_1282) % 1.38/1.58 $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc14 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (agent skc14 $_1284 $_1285) true % 1.38/1.58 (ifeq3 (agent skc14 skc18 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1284) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1282) true skc15 $_1282) $_1282) % 1.38/1.58 $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (agent skc15 $_1284 $_1285) true % 1.38/1.58 (ifeq3 (agent skc15 skc16 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1284) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true skc15 $_1282) $_1282) % 1.38/1.58 $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc15 $_1284 $_1282) true % 1.38/1.58 (ifeq3 (agent skc15 $_1284 $_1285) true % 1.38/1.58 (ifeq3 (agent skc15 skc18 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1284) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1282) true skc15 $_1282) $_1282) % 1.38/1.58 $_1282) $_1282) $_1282 = $_1282 % 1.38/1.58 |- ifeq3 (theme skc14 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc14 skc16 $_1285) true % 1.38/1.58 (ifeq3 (agent skc14 $_1283 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1281) true $_1281 skc15) skc15) % 1.38/1.58 skc15) skc15) skc15 = skc15 % 1.38/1.58 |- ifeq3 (theme skc14 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc14 skc18 $_1285) true % 1.38/1.58 (ifeq3 (agent skc14 $_1283 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1281) true $_1281 skc15) skc15) % 1.38/1.58 skc15) skc15) skc15 = skc15 % 1.38/1.58 |- ifeq3 (theme skc15 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 skc16 $_1285) true % 1.38/1.58 (ifeq3 (agent skc15 $_1283 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 skc15) skc15) % 1.38/1.58 skc15) skc15) skc15 = skc15 % 1.38/1.58 |- ifeq3 (theme skc15 $_1283 $_1281) true % 1.38/1.58 (ifeq3 (agent skc15 skc18 $_1285) true % 1.38/1.58 (ifeq3 (agent skc15 $_1283 $_1285) true % 1.38/1.58 (ifeq3 (think_believe_consider skc15 $_1283) true % 1.38/1.58 (ifeq3 (proposition skc15 $_1281) true $_1281 skc15) skc15) % 1.38/1.58 skc15) skc15) skc15 = skc15 % 1.38/1.58 |- ifeq3 (theme skc14 $_1287 skc15) true % 1.38/1.58 (ifeq3 (agent skc14 $_1287 $_1288) true % 1.38/1.58 (ifeq3 (agent skc14 skc16 $_1288) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1287) true skc15 skc15) % 1.38/1.58 skc15) skc15) skc15 = skc15 % 1.38/1.58 |- ifeq3 (theme skc14 skc16 $_1286) true % 1.38/1.58 (ifeq3 (agent skc14 skc16 $_1288) true % 1.38/1.58 (ifeq3 (agent skc14 skc16 $_1288) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1286) true skc15 $_1286) $_1286) % 1.38/1.58 $_1286) $_1286 = $_1286 % 1.38/1.58 |- ifeq3 (theme skc14 skc18 $_1286) true % 1.38/1.58 (ifeq3 (agent skc14 skc18 $_1288) true % 1.38/1.58 (ifeq3 (agent skc14 skc16 $_1288) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1286) true skc15 $_1286) $_1286) % 1.38/1.58 $_1286) $_1286 = $_1286 % 1.38/1.58 |- ifeq3 (theme skc14 $_1287 $_1286) true % 1.38/1.58 (ifeq3 (agent skc14 $_1287 skc20) true % 1.38/1.58 (ifeq3 (think_believe_consider skc14 $_1287) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1286) true skc15 $_1286) $_1286) % 1.38/1.58 $_1286) $_1286 = $_1286 % 1.38/1.58 |- ifeq3 (theme skc14 skc16 $_1286) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1286) true skc15 $_1286) $_1286 = $_1286 % 1.38/1.58 |- ifeq3 (theme skc14 skc18 $_1286) true % 1.38/1.58 (ifeq3 (proposition skc14 $_1286) true skc15 $_1286) $_1286 = $_1286 % 1.38/1.58 |- ifeq3 (agent skc14 skc16 $_1288) true % 1.38/1.58 (ifeq3 (agent skc14 skc16 $_1288) true skc15 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (agent skc14 skc18 $_1288) true % 1.38/1.59 (ifeq3 (agent skc14 skc16 $_1288) true skc15 skc15) skc15 = skc15 % 1.38/1.59 |- skc15 = skc17 % 1.38/1.59 |- ifeq3 (theme skc14 $_1357 skc15) true % 1.38/1.59 (ifeq3 (agent skc14 $_1357 skc20) true % 1.38/1.59 (ifeq3 (think_believe_consider skc14 $_1357) true skc15 skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 $_1366 skc15) true % 1.38/1.59 (ifeq3 (agent skc14 $_1366 $_1367) true % 1.38/1.59 (ifeq3 (agent skc14 skc18 $_1367) true % 1.38/1.59 (ifeq3 (think_believe_consider skc14 $_1366) true skc15 skc15) % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 skc16 $_1365) true % 1.38/1.59 (ifeq3 (agent skc14 skc16 $_1367) true % 1.38/1.59 (ifeq3 (agent skc14 skc18 $_1367) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1365) true skc15 $_1365) $_1365) % 1.38/1.59 $_1365) $_1365 = $_1365 % 1.38/1.59 |- ifeq3 (theme skc14 skc18 $_1365) true % 1.38/1.59 (ifeq3 (agent skc14 skc18 $_1367) true % 1.38/1.59 (ifeq3 (agent skc14 skc18 $_1367) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1365) true skc15 $_1365) $_1365) % 1.38/1.59 $_1365) $_1365 = $_1365 % 1.38/1.59 |- ifeq3 (agent skc14 skc16 $_1367) true % 1.38/1.59 (ifeq3 (agent skc14 skc18 $_1367) true skc15 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (agent skc14 skc18 $_1367) true % 1.38/1.59 (ifeq3 (agent skc14 skc18 $_1367) true skc15 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 $_1375 skc15) true % 1.38/1.59 (ifeq3 (agent skc15 $_1375 $_1376) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 $_1376) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 $_1375) true skc15 skc15) % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc16 $_1374) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 $_1376) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 $_1376) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1374) true skc15 $_1374) $_1374) % 1.38/1.59 $_1374) $_1374 = $_1374 % 1.38/1.59 |- ifeq3 (theme skc15 skc18 $_1374) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 $_1376) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 $_1376) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1374) true skc15 $_1374) $_1374) % 1.38/1.59 $_1374) $_1374 = $_1374 % 1.38/1.59 |- ifeq3 (theme skc15 $_1375 $_1374) true % 1.38/1.59 (ifeq3 (agent skc15 $_1375 skc20) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 $_1375) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1374) true skc15 $_1374) $_1374) % 1.38/1.59 $_1374) $_1374 = $_1374 % 1.38/1.59 |- ifeq3 (theme skc15 skc16 $_1374) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1374) true skc15 $_1374) $_1374 = $_1374 % 1.38/1.59 |- ifeq3 (theme skc15 skc18 $_1374) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1374) true skc15 $_1374) $_1374 = $_1374 % 1.38/1.59 |- ifeq3 (theme skc15 skc25 $_1374) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 skc24) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1374) true skc15 $_1374) $_1374) % 1.38/1.59 $_1374) $_1374 = $_1374 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc20) $_1374) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1374) true skc15 $_1374) $_1374) % 1.38/1.59 $_1374 = $_1374 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc24) $_1374) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 skc24) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1374) true skc15 $_1374) $_1374) % 1.38/1.59 $_1374) $_1374 = $_1374 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc27) $_1374) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 skc27) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1374) true skc15 $_1374) $_1374) % 1.38/1.59 $_1374) $_1374 = $_1374 % 1.38/1.59 |- ifeq3 (agent skc15 skc16 $_1376) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 $_1376) true skc15 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (agent skc15 skc18 $_1376) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 $_1376) true skc15 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true skc15 skc15) % 1.38/1.59 skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 skc24) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 skc25) true skc15 skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 skc24) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true skc15 % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 skc27) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true skc15 % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 $_1386 skc15) true % 1.38/1.59 (ifeq3 (agent skc15 $_1386 skc20) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 $_1386) true skc15 skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 $_1395 skc15) true % 1.38/1.59 (ifeq3 (agent skc15 $_1395 $_1396) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 $_1396) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 $_1395) true skc15 skc15) % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc16 $_1394) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 $_1396) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 $_1396) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1394) true skc15 $_1394) $_1394) % 1.38/1.59 $_1394) $_1394 = $_1394 % 1.38/1.59 |- ifeq3 (theme skc15 skc18 $_1394) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 $_1396) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 $_1396) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1394) true skc15 $_1394) $_1394) % 1.38/1.59 $_1394) $_1394 = $_1394 % 1.38/1.59 |- ifeq3 (theme skc15 skc25 $_1394) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 skc24) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1394) true skc15 $_1394) $_1394) % 1.38/1.59 $_1394) $_1394 = $_1394 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc24) $_1394) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 skc24) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1394) true skc15 $_1394) $_1394) % 1.38/1.59 $_1394) $_1394 = $_1394 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc27) $_1394) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 skc27) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1394) true skc15 $_1394) $_1394) % 1.38/1.59 $_1394) $_1394 = $_1394 % 1.38/1.59 |- ifeq3 (agent skc15 skc16 $_1396) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 $_1396) true skc15 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (agent skc15 skc18 $_1396) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 $_1396) true skc15 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 skc24) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 skc25) true skc15 skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 skc24) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true skc15 % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 skc27) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true skc15 % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 $_1407 skc15) true % 1.38/1.59 (ifeq3 (agent skc14 skc16 $_1408) true % 1.38/1.59 (ifeq3 (agent skc14 $_1407 $_1408) true % 1.38/1.59 (ifeq3 (think_believe_consider skc14 $_1407) true skc15 skc15) % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 skc16 $_1406) true % 1.38/1.59 (ifeq3 (agent skc14 skc16 $_1408) true % 1.38/1.59 (ifeq3 (agent skc14 skc16 $_1408) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1406) true $_1406 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 skc18 $_1406) true % 1.38/1.59 (ifeq3 (agent skc14 skc16 $_1408) true % 1.38/1.59 (ifeq3 (agent skc14 skc18 $_1408) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1406) true $_1406 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 skc16 $_1406) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1406) true $_1406 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 skc18 $_1406) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1406) true $_1406 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 $_1407 $_1406) true % 1.38/1.59 (ifeq3 (agent skc14 $_1407 skc20) true % 1.38/1.59 (ifeq3 (think_believe_consider skc14 $_1407) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1406) true $_1406 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 $_1418 skc15) true % 1.38/1.59 (ifeq3 (agent skc14 skc18 $_1419) true % 1.38/1.59 (ifeq3 (agent skc14 $_1418 $_1419) true % 1.38/1.59 (ifeq3 (think_believe_consider skc14 $_1418) true skc15 skc15) % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 skc16 $_1417) true % 1.38/1.59 (ifeq3 (agent skc14 skc18 $_1419) true % 1.38/1.59 (ifeq3 (agent skc14 skc16 $_1419) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1417) true $_1417 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 skc18 $_1417) true % 1.38/1.59 (ifeq3 (agent skc14 skc18 $_1419) true % 1.38/1.59 (ifeq3 (agent skc14 skc18 $_1419) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1417) true $_1417 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 $_1425 skc15) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 $_1426) true % 1.38/1.59 (ifeq3 (agent skc15 $_1425 $_1426) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 $_1425) true skc15 skc15) % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc16 $_1424) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 $_1426) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 $_1426) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1424) true $_1424 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc18 $_1424) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 $_1426) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 $_1426) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1424) true $_1424 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc16 $_1424) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1424) true $_1424 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc18 $_1424) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1424) true $_1424 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc25 $_1424) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 skc24) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1424) true $_1424 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc20) $_1424) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1424) true $_1424 skc15) skc15) skc15 = % 1.38/1.59 skc15 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc24) $_1424) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 skc24) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1424) true $_1424 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc27) $_1424) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 skc27) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1424) true $_1424 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 $_1425 $_1424) true % 1.38/1.59 (ifeq3 (agent skc15 $_1425 skc20) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 $_1425) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1424) true $_1424 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 $_1442 skc15) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 $_1443) true % 1.38/1.59 (ifeq3 (agent skc15 $_1442 $_1443) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 $_1442) true skc15 skc15) % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc16 $_1441) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 $_1443) true % 1.38/1.59 (ifeq3 (agent skc15 skc16 $_1443) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1441) true $_1441 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc18 $_1441) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 $_1443) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 $_1443) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1441) true $_1441 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc25 $_1441) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 skc24) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1441) true $_1441 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc24) $_1441) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 skc24) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1441) true $_1441 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc27) $_1441) true % 1.38/1.59 (ifeq3 (agent skc15 skc18 skc27) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1441) true $_1441 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 $_1453 skc15) true % 1.38/1.59 (ifeq3 (theme skc14 skc16 $_1451) true % 1.38/1.59 (ifeq3 (agent skc14 $_1453 skc20) true % 1.38/1.59 (ifeq3 (think_believe_consider skc14 $_1453) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1451) true $_1451 skc15) skc15) % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 skc16 $_1452) true % 1.38/1.59 (ifeq3 (theme skc14 skc16 $_1451) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1452) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1451) true $_1451 $_1452) $_1452) % 1.38/1.59 $_1452) $_1452 = $_1452 % 1.38/1.59 |- ifeq3 (theme skc14 skc18 $_1452) true % 1.38/1.59 (ifeq3 (theme skc14 skc16 $_1451) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1452) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1451) true $_1451 $_1452) $_1452) % 1.38/1.59 $_1452) $_1452 = $_1452 % 1.38/1.59 |- ifeq3 (theme skc14 $_1462 skc15) true % 1.38/1.59 (ifeq3 (theme skc14 skc18 $_1460) true % 1.38/1.59 (ifeq3 (agent skc14 $_1462 skc20) true % 1.38/1.59 (ifeq3 (think_believe_consider skc14 $_1462) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1460) true $_1460 skc15) skc15) % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 skc16 $_1461) true % 1.38/1.59 (ifeq3 (theme skc14 skc18 $_1460) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1461) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1460) true $_1460 $_1461) $_1461) % 1.38/1.59 $_1461) $_1461 = $_1461 % 1.38/1.59 |- ifeq3 (theme skc14 skc18 $_1461) true % 1.38/1.59 (ifeq3 (theme skc14 skc18 $_1460) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1461) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1460) true $_1460 $_1461) $_1461) % 1.38/1.59 $_1461) $_1461 = $_1461 % 1.38/1.59 |- ifeq3 (theme skc15 $_1471 skc15) true % 1.38/1.59 (ifeq3 (theme skc15 skc16 $_1469) true % 1.38/1.59 (ifeq3 (agent skc15 $_1471 skc20) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 $_1471) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1469) true $_1469 skc15) skc15) % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc16 $_1470) true % 1.38/1.59 (ifeq3 (theme skc15 skc16 $_1469) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1470) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1469) true $_1469 $_1470) $_1470) % 1.38/1.59 $_1470) $_1470 = $_1470 % 1.38/1.59 |- ifeq3 (theme skc15 skc18 $_1470) true % 1.38/1.59 (ifeq3 (theme skc15 skc16 $_1469) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1470) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1469) true $_1469 $_1470) $_1470) % 1.38/1.59 $_1470) $_1470 = $_1470 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc20) $_1470) true % 1.38/1.59 (ifeq3 (theme skc15 skc16 $_1469) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1470) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1469) true $_1469 $_1470) $_1470) % 1.38/1.59 $_1470) $_1470) $_1470 = $_1470 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.38/1.59 (ifeq3 (theme skc15 skc16 $_1476) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1476) true $_1476 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 $_1483 skc15) true % 1.38/1.59 (ifeq3 (theme skc15 skc18 $_1481) true % 1.38/1.59 (ifeq3 (agent skc15 $_1483 skc20) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 $_1483) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1481) true $_1481 skc15) skc15) % 1.38/1.59 skc15) skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc15 skc16 $_1482) true % 1.38/1.59 (ifeq3 (theme skc15 skc18 $_1481) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1482) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1481) true $_1481 $_1482) $_1482) % 1.38/1.59 $_1482) $_1482 = $_1482 % 1.38/1.59 |- ifeq3 (theme skc15 skc18 $_1482) true % 1.38/1.59 (ifeq3 (theme skc15 skc18 $_1481) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1482) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1481) true $_1481 $_1482) $_1482) % 1.38/1.59 $_1482) $_1482 = $_1482 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc20) $_1482) true % 1.38/1.59 (ifeq3 (theme skc15 skc18 $_1481) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1482) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1481) true $_1481 $_1482) $_1482) % 1.38/1.59 $_1482) $_1482) $_1482 = $_1482 % 1.38/1.59 |- ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.38/1.59 (ifeq3 (theme skc15 skc18 $_1488) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1488) true $_1488 skc15) skc15) % 1.38/1.59 skc15) skc15 = skc15 % 1.38/1.59 |- ifeq3 (theme skc14 skc16 $_1494) true % 1.38/1.59 (ifeq3 (theme skc14 $_1495 skc15) true % 1.38/1.59 (ifeq3 (agent skc14 $_1495 skc20) true % 1.38/1.59 (ifeq3 (think_believe_consider skc14 $_1495) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1494) true skc15 $_1494) $_1494) % 1.38/1.59 $_1494) $_1494) $_1494 = $_1494 % 1.38/1.59 |- ifeq3 (theme skc14 skc18 $_1497) true % 1.38/1.59 (ifeq3 (theme skc14 $_1498 skc15) true % 1.38/1.59 (ifeq3 (agent skc14 $_1498 skc20) true % 1.38/1.59 (ifeq3 (think_believe_consider skc14 $_1498) true % 1.38/1.59 (ifeq3 (proposition skc14 $_1497) true skc15 $_1497) $_1497) % 1.38/1.59 $_1497) $_1497) $_1497 = $_1497 % 1.38/1.59 |- ifeq3 (theme skc15 skc16 $_1500) true % 1.38/1.59 (ifeq3 (theme skc15 $_1501 skc15) true % 1.38/1.59 (ifeq3 (agent skc15 $_1501 skc20) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 $_1501) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1500) true skc15 $_1500) $_1500) % 1.38/1.59 $_1500) $_1500) $_1500 = $_1500 % 1.38/1.59 |- ifeq3 (theme skc15 skc16 $_1500) true % 1.38/1.59 (ifeq3 (theme skc15 (skf1 skc20) $_1499) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1500) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1499) true $_1499 $_1500) $_1500) % 1.38/1.59 $_1500) $_1500) $_1500 = $_1500 % 1.38/1.59 |- ifeq3 (theme skc15 skc16 $_1503) true % 1.38/1.59 (ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.38/1.59 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.59 (ifeq3 (proposition skc15 $_1503) true skc15 $_1503) $_1503) % 1.38/1.59 $_1503) $_1503 = $_1503 % 1.38/1.60 |- ifeq3 (theme skc15 skc18 $_1506) true % 1.38/1.60 (ifeq3 (theme skc15 $_1507 skc15) true % 1.38/1.60 (ifeq3 (agent skc15 $_1507 skc20) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1507) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1506) true skc15 $_1506) $_1506) % 1.38/1.60 $_1506) $_1506) $_1506 = $_1506 % 1.38/1.60 |- ifeq3 (theme skc15 skc18 $_1506) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc20) $_1505) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1506) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1505) true $_1505 $_1506) $_1506) % 1.38/1.60 $_1506) $_1506) $_1506 = $_1506 % 1.38/1.60 |- ifeq3 (theme skc15 skc18 $_1509) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1509) true skc15 $_1509) $_1509) % 1.38/1.60 $_1509) $_1509 = $_1509 % 1.38/1.60 |- ifeq3 (theme skc15 $_1513 $_1512) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (agent skc15 $_1513 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1513) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1512) true skc15 $_1512) % 1.38/1.60 $_1512) $_1512) $_1512) $_1512) $_1512 = $_1512 % 1.38/1.60 |- ifeq3 (theme skc15 $_1513 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 $_1511) true % 1.38/1.60 (ifeq3 (agent skc15 $_1513 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1513) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1511) true $_1511 skc15) % 1.38/1.60 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 skc16 $_1512) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 $_1511) true % 1.38/1.60 (ifeq3 (agent skc15 skc16 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1512) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1511) true $_1511 $_1512) % 1.38/1.60 $_1512) $_1512) $_1512) $_1512) $_1512 = $_1512 % 1.38/1.60 |- ifeq3 (theme skc15 skc18 $_1512) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 $_1511) true % 1.38/1.60 (ifeq3 (agent skc15 skc18 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1512) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1511) true $_1511 $_1512) % 1.38/1.60 $_1512) $_1512) $_1512) $_1512) $_1512 = $_1512 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 $_1512) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 $_1511) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1512) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1511) true $_1511 $_1512) % 1.38/1.60 $_1512) $_1512) $_1512) $_1512) $_1512 = $_1512 % 1.38/1.60 |- ifeq3 (theme skc15 (skf1 skc24) $_1512) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 $_1511) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1512) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1511) true $_1511 $_1512) % 1.38/1.60 $_1512) $_1512) $_1512) $_1512) $_1512 = $_1512 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 $_1515) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1515) true skc15 $_1515) $_1515) % 1.38/1.60 $_1515) $_1515) $_1515 = $_1515 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 $_1514) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1514) true $_1514 skc15) skc15) % 1.38/1.60 skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true skc15 skc15) % 1.38/1.60 skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 $_1519 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (agent skc15 $_1519 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1519) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true skc15 skc15) % 1.38/1.60 skc15) skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 skc16 $_1518) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (agent skc15 skc16 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1518) true skc15 $_1518) $_1518) % 1.38/1.60 $_1518) $_1518) $_1518 = $_1518 % 1.38/1.60 |- ifeq3 (theme skc15 skc18 $_1518) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (agent skc15 skc18 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1518) true skc15 $_1518) $_1518) % 1.38/1.60 $_1518) $_1518) $_1518 = $_1518 % 1.38/1.60 |- ifeq3 (theme skc15 (skf1 skc24) $_1518) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1518) true skc15 $_1518) $_1518) % 1.38/1.60 $_1518) $_1518) $_1518 = $_1518 % 1.38/1.60 |- ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true skc15 skc15) % 1.38/1.60 skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.38/1.60 (ifeq3 (theme skc15 skc25 $_1524) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1524) true $_1524 skc15) skc15) % 1.38/1.60 skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 $_1534) true % 1.38/1.60 (ifeq3 (theme skc15 $_1535 skc15) true % 1.38/1.60 (ifeq3 (agent skc15 $_1535 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1535) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1534) true skc15 $_1534) % 1.38/1.60 $_1534) $_1534) $_1534) $_1534) $_1534 = $_1534 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 $_1535 $_1533) true % 1.38/1.60 (ifeq3 (agent skc15 $_1535 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1535) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1533) true $_1533 skc15) % 1.38/1.60 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 $_1534) true % 1.38/1.60 (ifeq3 (theme skc15 skc16 $_1533) true % 1.38/1.60 (ifeq3 (agent skc15 skc16 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1534) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1533) true $_1533 $_1534) % 1.38/1.60 $_1534) $_1534) $_1534) $_1534) $_1534 = $_1534 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 $_1534) true % 1.38/1.60 (ifeq3 (theme skc15 skc18 $_1533) true % 1.38/1.60 (ifeq3 (agent skc15 skc18 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1534) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1533) true $_1533 $_1534) % 1.38/1.60 $_1534) $_1534) $_1534) $_1534) $_1534 = $_1534 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 $_1534) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc24) $_1533) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1534) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1533) true $_1533 $_1534) % 1.38/1.60 $_1534) $_1534) $_1534) $_1534) $_1534 = $_1534 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 $_1537 skc15) true % 1.38/1.60 (ifeq3 (agent skc15 $_1537 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1537) true skc15 % 1.38/1.60 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 $_1536) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1536) true skc15 $_1536) $_1536) % 1.38/1.60 $_1536) $_1536) $_1536 = $_1536 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true skc15 % 1.38/1.60 skc15) skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 skc16 $_1540) true % 1.38/1.60 (ifeq3 (agent skc15 skc16 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1540) true $_1540 skc15) skc15) % 1.38/1.60 skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 skc18 $_1543) true % 1.38/1.60 (ifeq3 (agent skc15 skc18 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1543) true $_1543 skc15) skc15) % 1.38/1.60 skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 skc25 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc24) $_1546) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 skc25) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1546) true $_1546 skc15) skc15) % 1.38/1.60 skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 $_1553 $_1552) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.38/1.60 (ifeq3 (agent skc15 $_1553 skc20) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1553) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1552) true skc15 $_1552) % 1.38/1.60 $_1552) $_1552) $_1552) $_1552) $_1552 = $_1552 % 1.38/1.60 |- ifeq3 (theme skc15 $_1553 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc20) $_1551) true % 1.38/1.60 (ifeq3 (agent skc15 $_1553 skc20) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1553) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1551) true $_1551 skc15) % 1.38/1.60 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 (skf1 skc20) $_1552) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc20) $_1551) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1552) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1551) true $_1551 $_1552) % 1.38/1.60 $_1552) $_1552) $_1552) $_1552) $_1552 = $_1552 % 1.38/1.60 |- ifeq3 (theme skc15 $_1555 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.38/1.60 (ifeq3 (agent skc15 $_1555 skc20) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1555) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true skc15 % 1.38/1.60 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 (skf1 skc20) $_1554) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1554) true skc15 $_1554) $_1554) % 1.38/1.60 $_1554) $_1554) $_1554 = $_1554 % 1.38/1.60 |- ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true skc15 % 1.38/1.60 skc15) skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc20) $_1558) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1558) true $_1558 skc15) skc15) % 1.38/1.60 skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 $_1565 $_1564) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.38/1.60 (ifeq3 (agent skc15 $_1565 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1565) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1564) true skc15 $_1564) % 1.38/1.60 $_1564) $_1564) $_1564) $_1564) $_1564 = $_1564 % 1.38/1.60 |- ifeq3 (theme skc15 $_1565 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc24) $_1563) true % 1.38/1.60 (ifeq3 (agent skc15 $_1565 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1565) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1563) true $_1563 skc15) % 1.38/1.60 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 skc16 $_1564) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc24) $_1563) true % 1.38/1.60 (ifeq3 (agent skc15 skc16 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1564) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1563) true $_1563 $_1564) % 1.38/1.60 $_1564) $_1564) $_1564) $_1564) $_1564 = $_1564 % 1.38/1.60 |- ifeq3 (theme skc15 skc18 $_1564) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc24) $_1563) true % 1.38/1.60 (ifeq3 (agent skc15 skc18 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1564) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1563) true $_1563 $_1564) % 1.38/1.60 $_1564) $_1564) $_1564) $_1564) $_1564 = $_1564 % 1.38/1.60 |- ifeq3 (theme skc15 (skf1 skc24) $_1564) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc24) $_1563) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1564) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1563) true $_1563 $_1564) % 1.38/1.60 $_1564) $_1564) $_1564) $_1564) $_1564 = $_1564 % 1.38/1.60 |- ifeq3 (theme skc15 $_1567 skc15) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.38/1.60 (ifeq3 (agent skc15 $_1567 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 $_1567) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true skc15 % 1.38/1.60 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.38/1.60 |- ifeq3 (theme skc15 skc16 $_1566) true % 1.38/1.60 (ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.38/1.60 (ifeq3 (agent skc15 skc16 skc24) true % 1.38/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.38/1.60 (ifeq3 (proposition skc15 $_1566) true skc15 $_1566) $_1566) % 1.38/1.60 $_1566) $_1566) $_1566 = $_1566 % 1.44/1.60 |- ifeq3 (theme skc15 skc18 $_1566) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.44/1.60 (ifeq3 (agent skc15 skc18 skc24) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1566) true skc15 $_1566) $_1566) % 1.44/1.60 $_1566) $_1566) $_1566 = $_1566 % 1.44/1.60 |- ifeq3 (theme skc15 (skf1 skc24) $_1566) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1566) true skc15 $_1566) $_1566) % 1.44/1.60 $_1566) $_1566) $_1566 = $_1566 % 1.44/1.60 |- ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true skc15 % 1.44/1.60 skc15) skc15) skc15) skc15 = skc15 % 1.44/1.60 |- ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc24) $_1576) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1576) true $_1576 skc15) skc15) % 1.44/1.60 skc15) skc15) skc15 = skc15 % 1.44/1.60 |- ifeq3 (theme skc15 $_1583 $_1582) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.44/1.60 (ifeq3 (agent skc15 $_1583 skc27) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 $_1583) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1582) true skc15 $_1582) % 1.44/1.60 $_1582) $_1582) $_1582) $_1582) $_1582 = $_1582 % 1.44/1.60 |- ifeq3 (theme skc15 $_1583 skc15) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc27) $_1581) true % 1.44/1.60 (ifeq3 (agent skc15 $_1583 skc27) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 $_1583) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1581) true $_1581 skc15) % 1.44/1.60 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.60 |- ifeq3 (theme skc15 skc16 $_1582) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc27) $_1581) true % 1.44/1.60 (ifeq3 (agent skc15 skc16 skc27) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1582) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1581) true $_1581 $_1582) % 1.44/1.60 $_1582) $_1582) $_1582) $_1582) $_1582 = $_1582 % 1.44/1.60 |- ifeq3 (theme skc15 skc18 $_1582) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc27) $_1581) true % 1.44/1.60 (ifeq3 (agent skc15 skc18 skc27) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1582) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1581) true $_1581 $_1582) % 1.44/1.60 $_1582) $_1582) $_1582) $_1582) $_1582 = $_1582 % 1.44/1.60 |- ifeq3 (theme skc15 (skf1 skc27) $_1582) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc27) $_1581) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1582) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1581) true $_1581 $_1582) % 1.44/1.60 $_1582) $_1582) $_1582) $_1582) $_1582 = $_1582 % 1.44/1.60 |- ifeq3 (theme skc15 $_1585 skc15) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.44/1.60 (ifeq3 (agent skc15 $_1585 skc27) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 $_1585) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true skc15 % 1.44/1.60 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.60 |- ifeq3 (theme skc15 skc16 $_1584) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.44/1.60 (ifeq3 (agent skc15 skc16 skc27) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1584) true skc15 $_1584) $_1584) % 1.44/1.60 $_1584) $_1584) $_1584 = $_1584 % 1.44/1.60 |- ifeq3 (theme skc15 skc18 $_1584) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.44/1.60 (ifeq3 (agent skc15 skc18 skc27) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1584) true skc15 $_1584) $_1584) % 1.44/1.60 $_1584) $_1584) $_1584 = $_1584 % 1.44/1.60 |- ifeq3 (theme skc15 (skf1 skc27) $_1584) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1584) true skc15 $_1584) $_1584) % 1.44/1.60 $_1584) $_1584) $_1584 = $_1584 % 1.44/1.60 |- ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true skc15 % 1.44/1.60 skc15) skc15) skc15) skc15 = skc15 % 1.44/1.60 |- ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.44/1.60 (ifeq3 (theme skc15 (skf1 skc27) $_1590) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1590) true $_1590 skc15) skc15) % 1.44/1.60 skc15) skc15) skc15 = skc15 % 1.44/1.60 |- ifeq3 (theme skc15 (skf1 skc20) $_1600) true % 1.44/1.60 (ifeq3 (theme skc15 $_1601 skc15) true % 1.44/1.60 (ifeq3 (agent skc15 $_1601 skc20) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 $_1601) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1600) true skc15 $_1600) % 1.44/1.60 $_1600) $_1600) $_1600) $_1600) $_1600 = $_1600 % 1.44/1.60 |- ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.44/1.60 (ifeq3 (theme skc15 $_1601 $_1599) true % 1.44/1.60 (ifeq3 (agent skc15 $_1601 skc20) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 $_1601) true % 1.44/1.60 (ifeq3 (proposition skc15 $_1599) true $_1599 skc15) % 1.44/1.60 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.60 |- ifeq3 (theme skc15 (skf1 skc20) skc15) true % 1.44/1.60 (ifeq3 (theme skc15 $_1603 skc15) true % 1.44/1.60 (ifeq3 (agent skc15 $_1603 skc20) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 (skf1 skc20)) true % 1.44/1.60 (ifeq3 (think_believe_consider skc15 $_1603) true skc15 % 1.44/1.60 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc24) $_1608) true % 1.44/1.61 (ifeq3 (theme skc15 $_1609 skc15) true % 1.44/1.61 (ifeq3 (agent skc15 $_1609 skc24) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 $_1609) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1608) true skc15 $_1608) % 1.44/1.61 $_1608) $_1608) $_1608) $_1608) $_1608 = $_1608 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.44/1.61 (ifeq3 (theme skc15 $_1609 $_1607) true % 1.44/1.61 (ifeq3 (agent skc15 $_1609 skc24) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 $_1609) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1607) true $_1607 skc15) % 1.44/1.61 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc24) $_1608) true % 1.44/1.61 (ifeq3 (theme skc15 skc16 $_1607) true % 1.44/1.61 (ifeq3 (agent skc15 skc16 skc24) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1608) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1607) true $_1607 $_1608) % 1.44/1.61 $_1608) $_1608) $_1608) $_1608) $_1608 = $_1608 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc24) $_1608) true % 1.44/1.61 (ifeq3 (theme skc15 skc18 $_1607) true % 1.44/1.61 (ifeq3 (agent skc15 skc18 skc24) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1608) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1607) true $_1607 $_1608) % 1.44/1.61 $_1608) $_1608) $_1608) $_1608) $_1608 = $_1608 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.44/1.61 (ifeq3 (theme skc15 $_1611 skc15) true % 1.44/1.61 (ifeq3 (agent skc15 $_1611 skc24) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 $_1611) true skc15 % 1.44/1.61 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.44/1.61 (ifeq3 (theme skc15 skc16 $_1613) true % 1.44/1.61 (ifeq3 (agent skc15 skc16 skc24) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1613) true $_1613 skc15) skc15) % 1.44/1.61 skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc24) skc15) true % 1.44/1.61 (ifeq3 (theme skc15 skc18 $_1616) true % 1.44/1.61 (ifeq3 (agent skc15 skc18 skc24) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc24)) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1616) true $_1616 skc15) skc15) % 1.44/1.61 skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc27) $_1622) true % 1.44/1.61 (ifeq3 (theme skc15 $_1623 skc15) true % 1.44/1.61 (ifeq3 (agent skc15 $_1623 skc27) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 $_1623) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1622) true skc15 $_1622) % 1.44/1.61 $_1622) $_1622) $_1622) $_1622) $_1622 = $_1622 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.44/1.61 (ifeq3 (theme skc15 $_1623 $_1621) true % 1.44/1.61 (ifeq3 (agent skc15 $_1623 skc27) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 $_1623) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1621) true $_1621 skc15) % 1.44/1.61 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc27) $_1622) true % 1.44/1.61 (ifeq3 (theme skc15 skc16 $_1621) true % 1.44/1.61 (ifeq3 (agent skc15 skc16 skc27) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1622) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1621) true $_1621 $_1622) % 1.44/1.61 $_1622) $_1622) $_1622) $_1622) $_1622 = $_1622 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc27) $_1622) true % 1.44/1.61 (ifeq3 (theme skc15 skc18 $_1621) true % 1.44/1.61 (ifeq3 (agent skc15 skc18 skc27) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1622) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1621) true $_1621 $_1622) % 1.44/1.61 $_1622) $_1622) $_1622) $_1622) $_1622 = $_1622 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.44/1.61 (ifeq3 (theme skc15 $_1625 skc15) true % 1.44/1.61 (ifeq3 (agent skc15 $_1625 skc27) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 $_1625) true skc15 % 1.44/1.61 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.44/1.61 (ifeq3 (theme skc15 skc16 $_1627) true % 1.44/1.61 (ifeq3 (agent skc15 skc16 skc27) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1627) true $_1627 skc15) skc15) % 1.44/1.61 skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc15 (skf1 skc27) skc15) true % 1.44/1.61 (ifeq3 (theme skc15 skc18 $_1630) true % 1.44/1.61 (ifeq3 (agent skc15 skc18 skc27) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 (skf1 skc27)) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1630) true $_1630 skc15) skc15) % 1.44/1.61 skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc14 $_1655 skc15) true % 1.44/1.61 (ifeq3 (theme skc14 $_1654 skc15) true % 1.44/1.61 (ifeq3 (agent skc14 $_1655 $_1656) true % 1.44/1.61 (ifeq3 (agent skc14 $_1654 $_1656) true % 1.44/1.61 (ifeq3 (think_believe_consider skc14 $_1655) true % 1.44/1.61 (ifeq3 (think_believe_consider skc14 $_1654) true skc15 % 1.44/1.61 skc15) skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc14 skc16 $_1653) true % 1.44/1.61 (ifeq3 (theme skc14 $_1654 skc15) true % 1.44/1.61 (ifeq3 (agent skc14 skc16 $_1656) true % 1.44/1.61 (ifeq3 (agent skc14 $_1654 $_1656) true % 1.44/1.61 (ifeq3 (think_believe_consider skc14 $_1654) true % 1.44/1.61 (ifeq3 (proposition skc14 $_1653) true skc15 $_1653) % 1.44/1.61 $_1653) $_1653) $_1653) $_1653) $_1653 = $_1653 % 1.44/1.61 |- ifeq3 (theme skc14 skc18 $_1653) true % 1.44/1.61 (ifeq3 (theme skc14 $_1654 skc15) true % 1.44/1.61 (ifeq3 (agent skc14 skc18 $_1656) true % 1.44/1.61 (ifeq3 (agent skc14 $_1654 $_1656) true % 1.44/1.61 (ifeq3 (think_believe_consider skc14 $_1654) true % 1.44/1.61 (ifeq3 (proposition skc14 $_1653) true skc15 $_1653) % 1.44/1.61 $_1653) $_1653) $_1653) $_1653) $_1653 = $_1653 % 1.44/1.61 |- ifeq3 (theme skc15 $_1668 skc15) true % 1.44/1.61 (ifeq3 (theme skc15 $_1667 skc15) true % 1.44/1.61 (ifeq3 (agent skc15 $_1668 $_1669) true % 1.44/1.61 (ifeq3 (agent skc15 $_1667 $_1669) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 $_1668) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 $_1667) true skc15 % 1.44/1.61 skc15) skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc15 skc16 $_1666) true % 1.44/1.61 (ifeq3 (theme skc15 $_1667 skc15) true % 1.44/1.61 (ifeq3 (agent skc15 skc16 $_1669) true % 1.44/1.61 (ifeq3 (agent skc15 $_1667 $_1669) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 $_1667) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1666) true skc15 $_1666) % 1.44/1.61 $_1666) $_1666) $_1666) $_1666) $_1666 = $_1666 % 1.44/1.61 |- ifeq3 (theme skc15 skc18 $_1666) true % 1.44/1.61 (ifeq3 (theme skc15 $_1667 skc15) true % 1.44/1.61 (ifeq3 (agent skc15 skc18 $_1669) true % 1.44/1.61 (ifeq3 (agent skc15 $_1667 $_1669) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 $_1667) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1666) true skc15 $_1666) % 1.44/1.61 $_1666) $_1666) $_1666) $_1666) $_1666 = $_1666 % 1.44/1.61 |- ifeq3 (theme skc14 $_1681 skc15) true % 1.44/1.61 (ifeq3 (theme skc14 skc16 $_1679) true % 1.44/1.61 (ifeq3 (agent skc14 $_1681 $_1682) true % 1.44/1.61 (ifeq3 (agent skc14 skc16 $_1682) true % 1.44/1.61 (ifeq3 (think_believe_consider skc14 $_1681) true % 1.44/1.61 (ifeq3 (proposition skc14 $_1679) true $_1679 skc15) % 1.44/1.61 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc14 skc16 $_1680) true % 1.44/1.61 (ifeq3 (theme skc14 skc16 $_1679) true % 1.44/1.61 (ifeq3 (agent skc14 skc16 $_1682) true % 1.44/1.61 (ifeq3 (agent skc14 skc16 $_1682) true % 1.44/1.61 (ifeq3 (proposition skc14 $_1680) true % 1.44/1.61 (ifeq3 (proposition skc14 $_1679) true $_1679 $_1680) % 1.44/1.61 $_1680) $_1680) $_1680) $_1680) $_1680 = $_1680 % 1.44/1.61 |- ifeq3 (theme skc14 skc18 $_1680) true % 1.44/1.61 (ifeq3 (theme skc14 skc16 $_1679) true % 1.44/1.61 (ifeq3 (agent skc14 skc18 $_1682) true % 1.44/1.61 (ifeq3 (agent skc14 skc16 $_1682) true % 1.44/1.61 (ifeq3 (proposition skc14 $_1680) true % 1.44/1.61 (ifeq3 (proposition skc14 $_1679) true $_1679 $_1680) % 1.44/1.61 $_1680) $_1680) $_1680) $_1680) $_1680 = $_1680 % 1.44/1.61 |- ifeq3 (theme skc14 $_1694 skc15) true % 1.44/1.61 (ifeq3 (theme skc14 skc18 $_1692) true % 1.44/1.61 (ifeq3 (agent skc14 $_1694 $_1695) true % 1.44/1.61 (ifeq3 (agent skc14 skc18 $_1695) true % 1.44/1.61 (ifeq3 (think_believe_consider skc14 $_1694) true % 1.44/1.61 (ifeq3 (proposition skc14 $_1692) true $_1692 skc15) % 1.44/1.61 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc14 skc16 $_1693) true % 1.44/1.61 (ifeq3 (theme skc14 skc18 $_1692) true % 1.44/1.61 (ifeq3 (agent skc14 skc16 $_1695) true % 1.44/1.61 (ifeq3 (agent skc14 skc18 $_1695) true % 1.44/1.61 (ifeq3 (proposition skc14 $_1693) true % 1.44/1.61 (ifeq3 (proposition skc14 $_1692) true $_1692 $_1693) % 1.44/1.61 $_1693) $_1693) $_1693) $_1693) $_1693 = $_1693 % 1.44/1.61 |- ifeq3 (theme skc14 skc18 $_1693) true % 1.44/1.61 (ifeq3 (theme skc14 skc18 $_1692) true % 1.44/1.61 (ifeq3 (agent skc14 skc18 $_1695) true % 1.44/1.61 (ifeq3 (agent skc14 skc18 $_1695) true % 1.44/1.61 (ifeq3 (proposition skc14 $_1693) true % 1.44/1.61 (ifeq3 (proposition skc14 $_1692) true $_1692 $_1693) % 1.44/1.61 $_1693) $_1693) $_1693) $_1693) $_1693 = $_1693 % 1.44/1.61 |- ifeq3 (theme skc15 $_1704 skc15) true % 1.44/1.61 (ifeq3 (theme skc15 skc16 $_1702) true % 1.44/1.61 (ifeq3 (agent skc15 $_1704 $_1705) true % 1.44/1.61 (ifeq3 (agent skc15 skc16 $_1705) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 $_1704) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1702) true $_1702 skc15) % 1.44/1.61 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc15 skc16 $_1703) true % 1.44/1.61 (ifeq3 (theme skc15 skc16 $_1702) true % 1.44/1.61 (ifeq3 (agent skc15 skc16 $_1705) true % 1.44/1.61 (ifeq3 (agent skc15 skc16 $_1705) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1703) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1702) true $_1702 $_1703) % 1.44/1.61 $_1703) $_1703) $_1703) $_1703) $_1703 = $_1703 % 1.44/1.61 |- ifeq3 (theme skc15 skc18 $_1703) true % 1.44/1.61 (ifeq3 (theme skc15 skc16 $_1702) true % 1.44/1.61 (ifeq3 (agent skc15 skc18 $_1705) true % 1.44/1.61 (ifeq3 (agent skc15 skc16 $_1705) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1703) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1702) true $_1702 $_1703) % 1.44/1.61 $_1703) $_1703) $_1703) $_1703) $_1703 = $_1703 % 1.44/1.61 |- ifeq3 (theme skc15 $_1717 skc15) true % 1.44/1.61 (ifeq3 (theme skc15 skc18 $_1715) true % 1.44/1.61 (ifeq3 (agent skc15 $_1717 $_1718) true % 1.44/1.61 (ifeq3 (agent skc15 skc18 $_1718) true % 1.44/1.61 (ifeq3 (think_believe_consider skc15 $_1717) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1715) true $_1715 skc15) % 1.44/1.61 skc15) skc15) skc15) skc15) skc15 = skc15 % 1.44/1.61 |- ifeq3 (theme skc15 skc16 $_1716) true % 1.44/1.61 (ifeq3 (theme skc15 skc18 $_1715) true % 1.44/1.61 (ifeq3 (agent skc15 skc16 $_1718) true % 1.44/1.61 (ifeq3 (agent skc15 skc18 $_1718) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1716) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1715) true $_1715 $_1716) % 1.44/1.61 $_1716) $_1716) $_1716) $_1716) $_1716 = $_1716 % 1.44/1.61 |- ifeq3 (theme skc15 skc18 $_1716) true % 1.44/1.61 (ifeq3 (theme skc15 skc18 $_1715) true % 1.44/1.61 (ifeq3 (agent skc15 skc18 $_1718) true % 1.44/1.61 (ifeq3 (agent skc15 skc18 $_1718) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1716) true % 1.44/1.61 (ifeq3 (proposition skc15 $_1715) true $_1715 $_1716) % 1.44/1.61 $_1716) $_1716) $_1716) $_1716) $_1716 = $_1716 % 1.44/1.61 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.44/1.61 %------------------------------------------------------------------------------