%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : NLP024-10 : TPTP v8.1.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n018.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:13:57 EDT 2022 % Result : Satisfiable 0.54s 0.77s % Output : Saturation 0.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP024-10 : TPTP v8.1.0. Released v7.5.0. % 0.07/0.13 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n018.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jul 1 03:58:17 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.54/0.77 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.54/0.77 % 0.54/0.77 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.54/0.77 |- ifeq4 $A $A $B $C = $B % 0.54/0.77 |- ifeq3 $A $A $B $C = $B % 0.54/0.77 |- ifeq2 $A $A $B $C = $B % 0.54/0.77 |- ifeq $A $A $B $C = $B % 0.54/0.77 |- ifeq3 (dance $U $V) true (event $U $V) true = true % 0.54/0.77 |- ifeq3 (event $U $V) true (eventuality $U $V) true = true % 0.54/0.77 |- ifeq3 (eventuality $U $V) true (thing $U $V) true = true % 0.54/0.77 |- ifeq3 (thing $U $V) true (singleton $U $V) true = true % 0.54/0.77 |- ifeq3 (eventuality $U $V) true (specific $U $V) true = true % 0.54/0.77 |- ifeq3 (eventuality $U $V) true (nonexistent $U $V) true = true % 0.54/0.77 |- ifeq3 (eventuality $U $V) true (unisex $U $V) true = true % 0.54/0.77 |- ifeq3 (desire_want $U $V) true (event $U $V) true = true % 0.54/0.77 |- ifeq3 (proposition $U $V) true (relation $U $V) true = true % 0.54/0.77 |- ifeq3 (relation $U $V) true (abstraction $U $V) true = true % 0.54/0.77 |- ifeq3 (abstraction $U $V) true (thing $U $V) true = true % 0.54/0.77 |- ifeq3 (abstraction $U $V) true (nonhuman $U $V) true = true % 0.54/0.77 |- ifeq3 (abstraction $U $V) true (general $U $V) true = true % 0.54/0.77 |- ifeq3 (abstraction $U $V) true (unisex $U $V) true = true % 0.54/0.77 |- ifeq3 (forename $U $V) true (relname $U $V) true = true % 0.54/0.77 |- ifeq3 (relname $U $V) true (relation $U $V) true = true % 0.54/0.77 |- ifeq3 (mia_forename $U $V) true (forename $U $V) true = true % 0.54/0.77 |- ifeq3 (woman $U $V) true (human_person $U $V) true = true % 0.54/0.77 |- ifeq3 (human_person $U $V) true (organism $U $V) true = true % 0.54/0.77 |- ifeq3 (organism $U $V) true (entity $U $V) true = true % 0.54/0.77 |- ifeq3 (entity $U $V) true (thing $U $V) true = true % 0.54/0.77 |- ifeq3 (entity $U $V) true (specific $U $V) true = true % 0.54/0.77 |- ifeq3 (entity $U $V) true (existent $U $V) true = true % 0.54/0.77 |- ifeq3 (organism $U $V) true (impartial $U $V) true = true % 0.54/0.77 |- ifeq3 (organism $U $V) true (living $U $V) true = true % 0.54/0.77 |- ifeq3 (human_person $U $V) true (human $U $V) true = true % 0.54/0.77 |- ifeq3 (human_person $U $V) true (animate $U $V) true = true % 0.54/0.77 |- ifeq3 (woman $U $V) true (female $U $V) true = true % 0.54/0.77 |- ifeq3 (vincent_forename $U $V) true (forename $U $V) true = true % 0.54/0.77 |- ifeq3 (man $U $V) true (human_person $U $V) true = true % 0.54/0.77 |- ifeq3 (man $U $V) true (male $U $V) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (dance $U $W) true (dance $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (event $U $W) true (event $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (eventuality $U $W) true (eventuality $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (thing $U $W) true (thing $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (singleton $U $W) true (singleton $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (specific $U $W) true (specific $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (nonexistent $U $W) true (nonexistent $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (unisex $U $W) true (unisex $V $W) true) true = true % 0.54/0.77 |- ifeq3 (present $U $W) true % 0.54/0.77 (ifeq3 (accessible_world $U $V) true (present $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (desire_want $U $W) true (desire_want $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (proposition $U $W) true (proposition $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (relation $U $W) true (relation $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (abstraction $U $W) true (abstraction $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (nonhuman $U $W) true (nonhuman $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (general $U $W) true (general $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (forename $U $W) true (forename $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (relname $U $W) true (relname $V $W) true) true = true % 0.54/0.77 |- ifeq3 (accessible_world $U $V) true % 0.54/0.77 (ifeq3 (mia_forename $U $W) true (mia_forename $V $W) true) true = % 0.54/0.77 true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (woman $U $W) true (woman $V $W) true) true = true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (human_person $U $W) true (human_person $V $W) true) true = % 0.54/0.78 true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (organism $U $W) true (organism $V $W) true) true = true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (entity $U $W) true (entity $V $W) true) true = true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (existent $U $W) true (existent $V $W) true) true = true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (impartial $U $W) true (impartial $V $W) true) true = true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (living $U $W) true (living $V $W) true) true = true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (human $U $W) true (human $V $W) true) true = true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (animate $U $W) true (animate $V $W) true) true = true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (female $U $W) true (female $V $W) true) true = true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (vincent_forename $U $W) true (vincent_forename $V $W) true) % 0.54/0.78 true = true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (man $U $W) true (man $V $W) true) true = true % 0.54/0.78 |- ifeq3 (accessible_world $U $V) true % 0.54/0.78 (ifeq3 (male $U $W) true (male $V $W) true) true = true % 0.54/0.78 |- ifeq3 (agent $U $W $X) true % 0.54/0.78 (ifeq3 (accessible_world $U $V) true (agent $V $W $X) true) true = % 0.54/0.78 true % 0.54/0.78 |- ifeq3 (theme $U $W $X) true % 0.54/0.78 (ifeq3 (accessible_world $U $V) true (theme $V $W $X) true) true = % 0.54/0.78 true % 0.54/0.78 |- ifeq3 (of $U $W $X) true % 0.54/0.78 (ifeq3 (accessible_world $U $V) true (of $V $W $X) true) true = true % 0.54/0.78 |- ifeq4 (of $U $W $X) true % 0.54/0.78 (ifeq4 (of $U $V $X) true % 0.54/0.78 (ifeq4 (entity $U $X) true % 0.54/0.78 (ifeq4 (forename $U $W) true (ifeq4 (forename $U $V) true $W $V) % 0.54/0.78 $V) $V) $V) $V = $V % 0.54/0.78 |- ifeq4 (theme $U $Y $X) true % 0.54/0.78 (ifeq4 (theme $U $V $W) true % 0.54/0.78 (ifeq4 (proposition $U $X) true % 0.54/0.78 (ifeq4 (proposition $U $W) true % 0.54/0.78 (ifeq4 (desire_want $U $Y) true % 0.54/0.78 (ifeq4 (desire_want $U $V) true $X $W) $W) $W) $W) $W) % 0.54/0.78 $W = $W % 0.54/0.78 |- ifeq2 (tuple2 (unisex $U $V) (male $U $V)) (tuple2 true true) a b = b % 0.54/0.78 |- ifeq2 (tuple2 (unisex $U $V) (female $U $V)) (tuple2 true true) a b = b % 0.54/0.78 |- ifeq2 (tuple2 (specific $U $V) (general $U $V)) (tuple2 true true) a b = % 0.54/0.78 b % 0.54/0.78 |- ifeq2 (tuple2 (nonhuman $U $V) (human $U $V)) (tuple2 true true) a b = b % 0.54/0.78 |- ifeq2 (tuple2 (female $U $V) (male $U $V)) (tuple2 true true) a b = b % 0.54/0.78 |- ifeq2 (tuple2 (nonexistent $U $V) (existent $U $V)) (tuple2 true true) a % 0.54/0.78 b = b % 0.54/0.78 |- actual_world skc8 = true % 0.54/0.78 |- man skc8 skc15 = true % 0.54/0.78 |- event skc10 skc13 = true % 0.54/0.78 |- woman skc8 skc12 = true % 0.54/0.78 |- present skc10 skc13 = true % 0.54/0.78 |- dance skc10 skc13 = true % 0.54/0.78 |- forename skc8 skc11 = true % 0.54/0.78 |- mia_forename skc8 skc11 = true % 0.54/0.78 |- proposition skc8 skc10 = true % 0.54/0.78 |- accessible_world skc8 skc10 = true % 0.54/0.78 |- desire_want skc8 skc9 = true % 0.54/0.78 |- present skc8 skc9 = true % 0.54/0.78 |- forename skc8 skc14 = true % 0.54/0.78 |- vincent_forename skc8 skc14 = true % 0.54/0.78 |- of skc8 skc14 skc15 = true % 0.54/0.78 |- of skc8 skc11 skc12 = true % 0.54/0.78 |- agent skc8 skc9 skc12 = true % 0.54/0.78 |- agent skc10 skc13 skc12 = true % 0.54/0.78 |- theme skc8 skc9 skc10 = true % 0.54/0.78 |- ifeq % 0.54/0.78 (tuple (dance $V $W) (event $V $W) (desire_want skc8 $U) % 0.54/0.78 (proposition skc8 $V) (accessible_world skc8 $V) (present $V $W) % 0.54/0.78 (present skc8 $U) (agent $V $W skc15) (agent skc8 $U skc15) % 0.54/0.78 (theme skc8 $U $V)) % 0.54/0.78 (tuple true true true true true true true true true true) a b = b % 0.54/0.78 |- ~(a = b) % 0.54/0.78 |- eventuality skc10 skc13 = true % 0.54/0.78 |- thing skc10 skc13 = true % 0.54/0.78 |- nonexistent skc10 skc13 = true % 0.54/0.78 |- unisex skc10 skc13 = true % 0.54/0.78 |- ifeq3 (abstraction skc10 skc13) true true true = true % 0.54/0.78 |- relname skc8 skc11 = true % 0.54/0.78 |- relname skc8 skc14 = true % 0.54/0.78 |- human_person skc8 skc12 = true % 0.54/0.78 |- organism skc8 skc12 = true % 0.54/0.78 |- human skc8 skc12 = true % 0.54/0.78 |- animate skc8 skc12 = true % 0.54/0.78 |- ifeq3 (man skc8 skc12) true true true = true % 0.54/0.78 |- human_person skc8 skc15 = true % 0.54/0.78 |- animate skc8 skc15 = true % 0.54/0.78 |- human skc8 skc15 = true % 0.54/0.78 |- organism skc8 skc15 = true % 0.54/0.78 |- ifeq3 (woman skc8 skc15) true true true = true % 0.54/0.78 |- male skc8 skc15 = true % 0.54/0.78 |- singleton skc10 skc13 = true % 0.54/0.78 |- specific skc10 skc13 = true % 0.54/0.78 |- ifeq3 (entity skc10 skc13) true true true = true % 0.54/0.78 |- ifeq3 (desire_want skc10 skc13) true true true = true % 0.54/0.78 |- event skc8 skc9 = true % 0.54/0.78 |- ifeq3 (dance skc8 skc9) true true true = true % 0.54/0.78 |- eventuality skc8 skc9 = true % 0.54/0.78 |- specific skc8 skc9 = true % 0.54/0.78 |- unisex skc8 skc9 = true % 0.54/0.78 |- nonexistent skc8 skc9 = true % 0.54/0.78 |- thing skc8 skc9 = true % 0.54/0.78 |- ifeq3 (entity skc8 skc9) true true true = true % 0.54/0.78 |- ifeq3 (abstraction skc8 skc9) true true true = true % 0.54/0.78 |- singleton skc8 skc9 = true % 0.54/0.78 |- relation skc8 skc10 = true % 0.54/0.78 |- abstraction skc8 skc10 = true % 0.54/0.78 |- unisex skc8 skc10 = true % 0.54/0.78 |- thing skc8 skc10 = true % 0.54/0.78 |- ifeq3 (eventuality skc8 skc10) true true true = true % 0.54/0.78 |- singleton skc8 skc10 = true % 0.54/0.78 |- nonhuman skc8 skc10 = true % 0.54/0.78 |- general skc8 skc10 = true % 0.54/0.78 |- ifeq3 (relname skc8 skc10) true true true = true % 0.54/0.78 |- relation skc8 skc11 = true % 0.54/0.78 |- relation skc8 skc14 = true % 0.62/0.78 |- ifeq3 (proposition skc8 skc11) true true true = true % 0.62/0.78 |- abstraction skc8 skc11 = true % 0.62/0.78 |- ifeq3 (proposition skc8 skc14) true true true = true % 0.62/0.78 |- abstraction skc8 skc14 = true % 0.62/0.78 |- general skc8 skc11 = true % 0.62/0.78 |- nonhuman skc8 skc11 = true % 0.62/0.78 |- unisex skc8 skc11 = true % 0.62/0.78 |- thing skc8 skc11 = true % 0.62/0.78 |- general skc8 skc14 = true % 0.62/0.78 |- nonhuman skc8 skc14 = true % 0.62/0.78 |- unisex skc8 skc14 = true % 0.62/0.78 |- thing skc8 skc14 = true % 0.62/0.78 |- ifeq3 (eventuality skc8 skc11) true true true = true % 0.62/0.78 |- singleton skc8 skc11 = true % 0.62/0.78 |- ifeq3 (eventuality skc8 skc14) true true true = true % 0.62/0.78 |- singleton skc8 skc14 = true % 0.62/0.78 |- ifeq3 (mia_forename skc8 skc14) true true true = true % 0.62/0.78 |- entity skc8 skc12 = true % 0.62/0.78 |- entity skc8 skc15 = true % 0.62/0.78 |- existent skc8 skc12 = true % 0.62/0.78 |- specific skc8 skc12 = true % 0.62/0.78 |- existent skc8 skc15 = true % 0.62/0.78 |- specific skc8 skc15 = true % 0.62/0.78 |- ifeq3 (eventuality skc8 skc12) true true true = true % 0.62/0.78 |- ifeq3 (eventuality skc8 skc15) true true true = true % 0.62/0.78 |- ifeq3 (entity skc8 skc10) true true true = true % 0.62/0.78 |- ifeq3 (entity skc8 skc11) true true true = true % 0.62/0.78 |- ifeq3 (entity skc8 skc14) true true true = true % 0.62/0.78 |- thing skc8 skc12 = true % 0.62/0.78 |- thing skc8 skc15 = true % 0.62/0.78 |- singleton skc8 skc12 = true % 0.62/0.78 |- ifeq3 (abstraction skc8 skc12) true true true = true % 0.62/0.78 |- singleton skc8 skc15 = true % 0.62/0.78 |- ifeq3 (abstraction skc8 skc15) true true true = true % 0.62/0.78 |- impartial skc8 skc12 = true % 0.62/0.78 |- impartial skc8 skc15 = true % 0.62/0.78 |- living skc8 skc12 = true % 0.62/0.78 |- living skc8 skc15 = true % 0.62/0.78 |- female skc8 skc12 = true % 0.62/0.78 |- ifeq3 (vincent_forename skc8 skc11) true true true = true % 0.62/0.78 |- ifeq2 (tuple2 (unisex skc8 skc15) true) (tuple2 true true) a b = b % 0.62/0.78 |- ifeq2 (tuple2 true (male skc10 skc13)) (tuple2 true true) a b = b % 0.62/0.78 |- ifeq2 (tuple2 true (male skc8 skc10)) (tuple2 true true) a b = b % 0.62/0.78 |- ifeq2 (tuple2 true (male skc8 skc11)) (tuple2 true true) a b = b % 0.62/0.78 |- ifeq2 (tuple2 true (male skc8 skc14)) (tuple2 true true) a b = b % 0.62/0.78 |- ifeq2 (tuple2 true (male skc8 skc9)) (tuple2 true true) a b = b % 0.62/0.78 |- ifeq2 (tuple2 (unisex skc8 skc12) true) (tuple2 true true) a b = b % 0.62/0.78 |- ifeq2 (tuple2 true (female skc10 skc13)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (female skc8 skc10)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (female skc8 skc11)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (female skc8 skc14)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (female skc8 skc9)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 (female skc8 skc15) true) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (male skc8 skc12)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 (nonexistent skc8 skc12) true) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 (nonexistent skc8 skc15) true) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (existent skc10 skc13)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (existent skc8 skc9)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 (specific skc8 skc10) true) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 (specific skc8 skc11) true) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 (specific skc8 skc14) true) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (general skc10 skc13)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (general skc8 skc12)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (general skc8 skc15)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (general skc8 skc9)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 (nonhuman skc8 skc12) true) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 (nonhuman skc8 skc15) true) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (human skc8 skc10)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (human skc8 skc11)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (human skc8 skc14)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq3 (accessible_world $_86 skc10) true % 0.62/0.79 (ifeq3 (dance $_86 skc13) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $_87) true (dance $_87 skc13) true = true % 0.62/0.79 |- ifeq3 (dance skc8 $_88) true (dance skc10 $_88) true = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 skc10) true true true = true % 0.62/0.79 |- ifeq3 (dance skc8 skc13) true true true = true % 0.62/0.79 |- ifeq3 (accessible_world $_92 skc10) true % 0.62/0.79 (ifeq3 (event $_92 skc13) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_92 skc8) true % 0.62/0.79 (ifeq3 (event $_92 skc9) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $_93) true (event $_93 skc13) true = true % 0.62/0.79 |- ifeq3 (accessible_world skc8 $_93) true (event $_93 skc9) true = true % 0.62/0.79 |- ifeq3 (event skc8 $_94) true (event skc10 $_94) true = true % 0.62/0.79 |- ifeq3 (accessible_world skc8 skc8) true true true = true % 0.62/0.79 |- event skc10 skc9 = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $V) true (event $V skc9) true = true % 0.62/0.79 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.79 (ifeq3 (event $U skc9) true true true) true = true % 0.62/0.79 |- ifeq3 (dance skc10 skc9) true true true = true % 0.62/0.79 |- eventuality skc10 skc9 = true % 0.62/0.79 |- specific skc10 skc9 = true % 0.62/0.79 |- unisex skc10 skc9 = true % 0.62/0.79 |- nonexistent skc10 skc9 = true % 0.62/0.79 |- thing skc10 skc9 = true % 0.62/0.79 |- ifeq2 (tuple2 true (general skc10 skc9)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq3 (entity skc10 skc9) true true true = true % 0.62/0.79 |- ifeq2 (tuple2 true (female skc10 skc9)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq2 (tuple2 true (male skc10 skc9)) (tuple2 true true) a b = b % 0.62/0.79 |- ifeq3 (abstraction skc10 skc9) true true true = true % 0.62/0.79 |- ifeq2 (tuple2 true (existent skc10 skc9)) (tuple2 true true) a b = b % 0.62/0.79 |- singleton skc10 skc9 = true % 0.62/0.79 |- ifeq3 (event skc8 skc13) true true true = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 skc8) true true true = true % 0.62/0.79 |- ifeq3 (accessible_world $_102 skc10) true % 0.62/0.79 (ifeq3 (eventuality $_102 skc13) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_102 skc10) true % 0.62/0.79 (ifeq3 (eventuality $_102 skc9) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_102 skc8) true % 0.62/0.79 (ifeq3 (eventuality $_102 skc9) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $_103) true (eventuality $_103 skc13) % 0.62/0.79 true = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $_103) true (eventuality $_103 skc9) % 0.62/0.79 true = true % 0.62/0.79 |- ifeq3 (accessible_world skc8 $_103) true (eventuality $_103 skc9) true = % 0.62/0.79 true % 0.62/0.79 |- ifeq3 (eventuality skc8 $_104) true (eventuality skc10 $_104) true = % 0.62/0.79 true % 0.62/0.79 |- ifeq3 (eventuality skc8 skc13) true true true = true % 0.62/0.79 |- ifeq3 (accessible_world $_112 skc10) true % 0.62/0.79 (ifeq3 (singleton $_112 skc13) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_112 skc10) true % 0.62/0.79 (ifeq3 (singleton $_112 skc9) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_112 skc8) true % 0.62/0.79 (ifeq3 (singleton $_112 skc10) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_112 skc8) true % 0.62/0.79 (ifeq3 (singleton $_112 skc11) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_112 skc8) true % 0.62/0.79 (ifeq3 (singleton $_112 skc12) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_112 skc8) true % 0.62/0.79 (ifeq3 (singleton $_112 skc14) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_112 skc8) true % 0.62/0.79 (ifeq3 (singleton $_112 skc15) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_112 skc8) true % 0.62/0.79 (ifeq3 (singleton $_112 skc9) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $_113) true (singleton $_113 skc13) true = % 0.62/0.79 true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $_113) true (singleton $_113 skc9) true = % 0.62/0.79 true % 0.62/0.79 |- ifeq3 (accessible_world skc8 $_113) true (singleton $_113 skc10) true = % 0.62/0.79 true % 0.62/0.79 |- ifeq3 (accessible_world skc8 $_113) true (singleton $_113 skc11) true = % 0.62/0.79 true % 0.62/0.79 |- ifeq3 (accessible_world skc8 $_113) true (singleton $_113 skc12) true = % 0.62/0.79 true % 0.62/0.79 |- ifeq3 (accessible_world skc8 $_113) true (singleton $_113 skc14) true = % 0.62/0.79 true % 0.62/0.79 |- ifeq3 (accessible_world skc8 $_113) true (singleton $_113 skc15) true = % 0.62/0.79 true % 0.62/0.79 |- ifeq3 (accessible_world skc8 $_113) true (singleton $_113 skc9) true = % 0.62/0.79 true % 0.62/0.79 |- ifeq3 (singleton skc8 $_114) true (singleton skc10 $_114) true = true % 0.62/0.79 |- singleton skc10 skc10 = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $V) true (singleton $V skc10) true = true % 0.62/0.79 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.79 (ifeq3 (singleton $U skc10) true true true) true = true % 0.62/0.79 |- singleton skc10 skc11 = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $V) true (singleton $V skc11) true = true % 0.62/0.79 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.79 (ifeq3 (singleton $U skc11) true true true) true = true % 0.62/0.79 |- singleton skc10 skc12 = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $V) true (singleton $V skc12) true = true % 0.62/0.79 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.79 (ifeq3 (singleton $U skc12) true true true) true = true % 0.62/0.79 |- singleton skc10 skc14 = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $V) true (singleton $V skc14) true = true % 0.62/0.79 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.79 (ifeq3 (singleton $U skc14) true true true) true = true % 0.62/0.79 |- singleton skc10 skc15 = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $V) true (singleton $V skc15) true = true % 0.62/0.79 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.79 (ifeq3 (singleton $U skc15) true true true) true = true % 0.62/0.79 |- ifeq3 (singleton skc8 skc13) true true true = true % 0.62/0.79 |- ifeq3 (accessible_world $_138 skc10) true % 0.62/0.79 (ifeq3 (specific $_138 skc13) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_138 skc10) true % 0.62/0.79 (ifeq3 (specific $_138 skc9) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_138 skc8) true % 0.62/0.79 (ifeq3 (specific $_138 skc12) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_138 skc8) true % 0.62/0.79 (ifeq3 (specific $_138 skc15) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world $_138 skc8) true % 0.62/0.79 (ifeq3 (specific $_138 skc9) true true true) true = true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $_139) true (specific $_139 skc13) true = % 0.62/0.79 true % 0.62/0.79 |- ifeq3 (accessible_world skc10 $_139) true (specific $_139 skc9) true = % 0.62/0.79 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_139) true (specific $_139 skc12) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_139) true (specific $_139 skc15) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_139) true (specific $_139 skc9) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (specific skc8 $_140) true (specific skc10 $_140) true = true % 0.62/0.80 |- specific skc10 skc12 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (specific $V skc12) true = true % 0.62/0.80 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.80 (ifeq3 (specific $U skc12) true true true) true = true % 0.62/0.80 |- ifeq2 (tuple2 true (general skc10 skc12)) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq3 (eventuality skc10 skc12) true true true = true % 0.62/0.80 |- specific skc10 skc15 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (specific $V skc15) true = true % 0.62/0.80 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.80 (ifeq3 (specific $U skc15) true true true) true = true % 0.62/0.80 |- ifeq2 (tuple2 true (general skc10 skc15)) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq3 (eventuality skc10 skc15) true true true = true % 0.62/0.80 |- ifeq3 (specific skc8 skc13) true true true = true % 0.62/0.80 |- ifeq3 (accessible_world $_156 skc10) true % 0.62/0.80 (ifeq3 (nonexistent $_156 skc13) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_156 skc10) true % 0.62/0.80 (ifeq3 (nonexistent $_156 skc9) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_156 skc8) true % 0.62/0.80 (ifeq3 (nonexistent $_156 skc9) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_157) true (nonexistent $_157 skc13) % 0.62/0.80 true = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_157) true (nonexistent $_157 skc9) % 0.62/0.80 true = true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_157) true (nonexistent $_157 skc9) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (nonexistent skc8 $_158) true (nonexistent skc10 $_158) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (nonexistent skc8 skc13) true true true = true % 0.62/0.80 |- ifeq3 (accessible_world $_166 skc10) true % 0.62/0.80 (ifeq3 (unisex $_166 skc13) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_166 skc10) true % 0.62/0.80 (ifeq3 (unisex $_166 skc9) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_166 skc8) true % 0.62/0.80 (ifeq3 (unisex $_166 skc10) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_166 skc8) true % 0.62/0.80 (ifeq3 (unisex $_166 skc11) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_166 skc8) true % 0.62/0.80 (ifeq3 (unisex $_166 skc14) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_166 skc8) true % 0.62/0.80 (ifeq3 (unisex $_166 skc9) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_167) true (unisex $_167 skc13) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_167) true (unisex $_167 skc9) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_167) true (unisex $_167 skc10) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_167) true (unisex $_167 skc11) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_167) true (unisex $_167 skc14) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_167) true (unisex $_167 skc9) true = true % 0.62/0.80 |- ifeq3 (unisex skc8 $_168) true (unisex skc10 $_168) true = true % 0.62/0.80 |- unisex skc10 skc10 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (unisex $V skc10) true = true % 0.62/0.80 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.80 (ifeq3 (unisex $U skc10) true true true) true = true % 0.62/0.80 |- ifeq2 (tuple2 true (female skc10 skc10)) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq2 (tuple2 true (male skc10 skc10)) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq3 (eventuality skc10 skc10) true true true = true % 0.62/0.80 |- unisex skc10 skc11 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (unisex $V skc11) true = true % 0.62/0.80 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.80 (ifeq3 (unisex $U skc11) true true true) true = true % 0.62/0.80 |- ifeq2 (tuple2 true (female skc10 skc11)) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq2 (tuple2 true (male skc10 skc11)) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq3 (eventuality skc10 skc11) true true true = true % 0.62/0.80 |- unisex skc10 skc14 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (unisex $V skc14) true = true % 0.62/0.80 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.80 (ifeq3 (unisex $U skc14) true true true) true = true % 0.62/0.80 |- ifeq2 (tuple2 true (female skc10 skc14)) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq2 (tuple2 true (male skc10 skc14)) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq3 (eventuality skc10 skc14) true true true = true % 0.62/0.80 |- ifeq3 (unisex skc8 skc13) true true true = true % 0.62/0.80 |- ifeq3 (present $_186 skc13) true % 0.62/0.80 (ifeq3 (accessible_world $_186 skc10) true true true) true = true % 0.62/0.80 |- ifeq3 (present $_186 skc9) true % 0.62/0.80 (ifeq3 (accessible_world $_186 skc8) true true true) true = true % 0.62/0.80 |- ifeq3 (present skc8 $_188) true (present skc10 $_188) true = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_187) true (present $_187 skc13) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_187) true (present $_187 skc9) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (present skc8 skc13) true true true = true % 0.62/0.80 |- present skc10 skc9 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (present $V skc9) true = true % 0.62/0.80 |- ifeq3 (present $U skc9) true % 0.62/0.80 (ifeq3 (accessible_world $U skc10) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_196 skc8) true % 0.62/0.80 (ifeq3 (desire_want $_196 skc9) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_197) true (desire_want $_197 skc9) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (desire_want skc8 $_198) true (desire_want skc10 $_198) true = % 0.62/0.80 true % 0.62/0.80 |- desire_want skc10 skc9 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (desire_want $V skc9) true = true % 0.62/0.80 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.80 (ifeq3 (desire_want $U skc9) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_204 skc8) true % 0.62/0.80 (ifeq3 (proposition $_204 skc10) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_205) true (proposition $_205 skc10) % 0.62/0.80 true = true % 0.62/0.80 |- ifeq3 (proposition skc8 $_206) true (proposition skc10 $_206) true = % 0.62/0.80 true % 0.62/0.80 |- proposition skc10 skc10 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (proposition $V skc10) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.80 (ifeq3 (proposition $U skc10) true true true) true = true % 0.62/0.80 |- relation skc10 skc10 = true % 0.62/0.80 |- ifeq3 (relname skc10 skc10) true true true = true % 0.62/0.80 |- abstraction skc10 skc10 = true % 0.62/0.80 |- general skc10 skc10 = true % 0.62/0.80 |- nonhuman skc10 skc10 = true % 0.62/0.80 |- thing skc10 skc10 = true % 0.62/0.80 |- ifeq2 (tuple2 true (human skc10 skc10)) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq2 (tuple2 (specific skc10 skc10) true) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq3 (entity skc10 skc10) true true true = true % 0.62/0.80 |- ifeq3 (accessible_world $_212 skc10) true % 0.62/0.80 (ifeq3 (abstraction $_212 skc10) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_212 skc8) true % 0.62/0.80 (ifeq3 (abstraction $_212 skc10) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_212 skc8) true % 0.62/0.80 (ifeq3 (abstraction $_212 skc11) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_212 skc8) true % 0.62/0.80 (ifeq3 (abstraction $_212 skc14) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_213) true (abstraction $_213 skc10) % 0.62/0.80 true = true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_213) true (abstraction $_213 skc10) % 0.62/0.80 true = true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_213) true (abstraction $_213 skc11) % 0.62/0.80 true = true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_213) true (abstraction $_213 skc14) % 0.62/0.80 true = true % 0.62/0.80 |- ifeq3 (abstraction skc8 $_214) true (abstraction skc10 $_214) true = % 0.62/0.80 true % 0.62/0.80 |- abstraction skc10 skc11 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (abstraction $V skc11) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.80 (ifeq3 (abstraction $U skc11) true true true) true = true % 0.62/0.80 |- general skc10 skc11 = true % 0.62/0.80 |- nonhuman skc10 skc11 = true % 0.62/0.80 |- thing skc10 skc11 = true % 0.62/0.80 |- ifeq2 (tuple2 true (human skc10 skc11)) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq2 (tuple2 (specific skc10 skc11) true) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq3 (entity skc10 skc11) true true true = true % 0.62/0.80 |- abstraction skc10 skc14 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (abstraction $V skc14) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.80 (ifeq3 (abstraction $U skc14) true true true) true = true % 0.62/0.80 |- general skc10 skc14 = true % 0.62/0.80 |- nonhuman skc10 skc14 = true % 0.62/0.80 |- thing skc10 skc14 = true % 0.62/0.80 |- ifeq2 (tuple2 (specific skc10 skc14) true) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq2 (tuple2 true (human skc10 skc14)) (tuple2 true true) a b = b % 0.62/0.80 |- ifeq3 (entity skc10 skc14) true true true = true % 0.62/0.80 |- ifeq3 (accessible_world $_227 skc10) true % 0.62/0.80 (ifeq3 (nonhuman $_227 skc10) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_227 skc10) true % 0.62/0.80 (ifeq3 (nonhuman $_227 skc11) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_227 skc10) true % 0.62/0.80 (ifeq3 (nonhuman $_227 skc14) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_227 skc8) true % 0.62/0.80 (ifeq3 (nonhuman $_227 skc10) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_227 skc8) true % 0.62/0.80 (ifeq3 (nonhuman $_227 skc11) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_227 skc8) true % 0.62/0.80 (ifeq3 (nonhuman $_227 skc14) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_228) true (nonhuman $_228 skc10) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_228) true (nonhuman $_228 skc11) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_228) true (nonhuman $_228 skc14) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_228) true (nonhuman $_228 skc10) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_228) true (nonhuman $_228 skc11) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_228) true (nonhuman $_228 skc14) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (nonhuman skc8 $_229) true (nonhuman skc10 $_229) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_243 skc10) true % 0.62/0.80 (ifeq3 (general $_243 skc10) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_243 skc10) true % 0.62/0.80 (ifeq3 (general $_243 skc11) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_243 skc10) true % 0.62/0.80 (ifeq3 (general $_243 skc14) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_243 skc8) true % 0.62/0.80 (ifeq3 (general $_243 skc10) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_243 skc8) true % 0.62/0.80 (ifeq3 (general $_243 skc11) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_243 skc8) true % 0.62/0.80 (ifeq3 (general $_243 skc14) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_244) true (general $_244 skc10) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_244) true (general $_244 skc11) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_244) true (general $_244 skc14) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_244) true (general $_244 skc10) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_244) true (general $_244 skc11) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_244) true (general $_244 skc14) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (general skc8 $_245) true (general skc10 $_245) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_259 skc8) true % 0.62/0.80 (ifeq3 (forename $_259 skc11) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_259 skc8) true % 0.62/0.80 (ifeq3 (forename $_259 skc14) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_260) true (forename $_260 skc11) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_260) true (forename $_260 skc14) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (forename skc8 $_261) true (forename skc10 $_261) true = true % 0.62/0.80 |- forename skc10 skc11 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (forename $V skc11) true = true % 0.62/0.80 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.80 (ifeq3 (forename $U skc11) true true true) true = true % 0.62/0.80 |- ifeq3 (vincent_forename skc10 skc11) true true true = true % 0.62/0.80 |- relname skc10 skc11 = true % 0.62/0.80 |- relation skc10 skc11 = true % 0.62/0.80 |- ifeq3 (proposition skc10 skc11) true true true = true % 0.62/0.80 |- forename skc10 skc14 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (forename $V skc14) true = true % 0.62/0.80 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.80 (ifeq3 (forename $U skc14) true true true) true = true % 0.62/0.80 |- ifeq3 (mia_forename skc10 skc14) true true true = true % 0.62/0.80 |- relname skc10 skc14 = true % 0.62/0.80 |- relation skc10 skc14 = true % 0.62/0.80 |- ifeq3 (proposition skc10 skc14) true true true = true % 0.62/0.80 |- ifeq3 (accessible_world $_271 skc10) true % 0.62/0.80 (ifeq3 (relname $_271 skc11) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_271 skc10) true % 0.62/0.80 (ifeq3 (relname $_271 skc14) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_271 skc8) true % 0.62/0.80 (ifeq3 (relname $_271 skc11) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_271 skc8) true % 0.62/0.80 (ifeq3 (relname $_271 skc14) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_272) true (relname $_272 skc11) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $_272) true (relname $_272 skc14) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_272) true (relname $_272 skc11) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_272) true (relname $_272 skc14) true = % 0.62/0.80 true % 0.62/0.80 |- ifeq3 (relname skc8 $_273) true (relname skc10 $_273) true = true % 0.62/0.80 |- ifeq3 (accessible_world $_283 skc8) true % 0.62/0.80 (ifeq3 (mia_forename $_283 skc11) true true true) true = true % 0.62/0.80 |- ifeq3 (accessible_world skc8 $_284) true (mia_forename $_284 skc11) % 0.62/0.80 true = true % 0.62/0.80 |- ifeq3 (mia_forename skc8 $_285) true (mia_forename skc10 $_285) true = % 0.62/0.80 true % 0.62/0.80 |- mia_forename skc10 skc11 = true % 0.62/0.80 |- ifeq3 (accessible_world skc10 $V) true (mia_forename $V skc11) true = % 0.62/0.80 true % 0.62/0.81 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.81 (ifeq3 (mia_forename $U skc11) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_291 skc8) true % 0.62/0.81 (ifeq3 (woman $_291 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_292) true (woman $_292 skc12) true = true % 0.62/0.81 |- ifeq3 (woman skc8 $_293) true (woman skc10 $_293) true = true % 0.62/0.81 |- woman skc10 skc12 = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $V) true (woman $V skc12) true = true % 0.62/0.81 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.81 (ifeq3 (woman $U skc12) true true true) true = true % 0.62/0.81 |- female skc10 skc12 = true % 0.62/0.81 |- human_person skc10 skc12 = true % 0.62/0.81 |- ifeq2 (tuple2 true (male skc10 skc12)) (tuple2 true true) a b = b % 0.62/0.81 |- ifeq2 (tuple2 (unisex skc10 skc12) true) (tuple2 true true) a b = b % 0.62/0.81 |- ifeq3 (man skc10 skc12) true true true = true % 0.62/0.81 |- animate skc10 skc12 = true % 0.62/0.81 |- human skc10 skc12 = true % 0.62/0.81 |- organism skc10 skc12 = true % 0.62/0.81 |- ifeq2 (tuple2 (nonhuman skc10 skc12) true) (tuple2 true true) a b = b % 0.62/0.81 |- living skc10 skc12 = true % 0.62/0.81 |- impartial skc10 skc12 = true % 0.62/0.81 |- entity skc10 skc12 = true % 0.62/0.81 |- thing skc10 skc12 = true % 0.62/0.81 |- existent skc10 skc12 = true % 0.62/0.81 |- ifeq2 (tuple2 (nonexistent skc10 skc12) true) (tuple2 true true) a b = b % 0.62/0.81 |- ifeq3 (abstraction skc10 skc12) true true true = true % 0.62/0.81 |- ifeq3 (accessible_world $_299 skc10) true % 0.62/0.81 (ifeq3 (organism $_299 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_299 skc8) true % 0.62/0.81 (ifeq3 (organism $_299 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_299 skc8) true % 0.62/0.81 (ifeq3 (organism $_299 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_300) true (organism $_300 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_300) true (organism $_300 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_300) true (organism $_300 skc15) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (organism skc8 $_301) true (organism skc10 $_301) true = true % 0.62/0.81 |- organism skc10 skc15 = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $V) true (organism $V skc15) true = true % 0.62/0.81 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.81 (ifeq3 (organism $U skc15) true true true) true = true % 0.62/0.81 |- living skc10 skc15 = true % 0.62/0.81 |- impartial skc10 skc15 = true % 0.62/0.81 |- entity skc10 skc15 = true % 0.62/0.81 |- thing skc10 skc15 = true % 0.62/0.81 |- existent skc10 skc15 = true % 0.62/0.81 |- ifeq3 (abstraction skc10 skc15) true true true = true % 0.62/0.81 |- ifeq2 (tuple2 (nonexistent skc10 skc15) true) (tuple2 true true) a b = b % 0.62/0.81 |- ifeq3 (accessible_world $_311 skc10) true % 0.62/0.81 (ifeq3 (entity $_311 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_311 skc10) true % 0.62/0.81 (ifeq3 (entity $_311 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_311 skc8) true % 0.62/0.81 (ifeq3 (entity $_311 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_311 skc8) true % 0.62/0.81 (ifeq3 (entity $_311 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_312) true (entity $_312 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_312) true (entity $_312 skc15) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_312) true (entity $_312 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_312) true (entity $_312 skc15) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (entity skc8 $_313) true (entity skc10 $_313) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_323 skc10) true % 0.62/0.81 (ifeq3 (existent $_323 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_323 skc10) true % 0.62/0.81 (ifeq3 (existent $_323 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_323 skc8) true % 0.62/0.81 (ifeq3 (existent $_323 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_323 skc8) true % 0.62/0.81 (ifeq3 (existent $_323 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_324) true (existent $_324 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_324) true (existent $_324 skc15) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_324) true (existent $_324 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_324) true (existent $_324 skc15) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (existent skc8 $_325) true (existent skc10 $_325) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_335 skc10) true % 0.62/0.81 (ifeq3 (impartial $_335 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_335 skc10) true % 0.62/0.81 (ifeq3 (impartial $_335 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_335 skc8) true % 0.62/0.81 (ifeq3 (impartial $_335 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_335 skc8) true % 0.62/0.81 (ifeq3 (impartial $_335 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_336) true (impartial $_336 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_336) true (impartial $_336 skc15) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_336) true (impartial $_336 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_336) true (impartial $_336 skc15) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (impartial skc8 $_337) true (impartial skc10 $_337) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_347 skc10) true % 0.62/0.81 (ifeq3 (living $_347 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_347 skc10) true % 0.62/0.81 (ifeq3 (living $_347 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_347 skc8) true % 0.62/0.81 (ifeq3 (living $_347 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_347 skc8) true % 0.62/0.81 (ifeq3 (living $_347 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_348) true (living $_348 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_348) true (living $_348 skc15) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_348) true (living $_348 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_348) true (living $_348 skc15) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (living skc8 $_349) true (living skc10 $_349) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_359 skc10) true % 0.62/0.81 (ifeq3 (human $_359 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_359 skc8) true % 0.62/0.81 (ifeq3 (human $_359 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_359 skc8) true % 0.62/0.81 (ifeq3 (human $_359 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_360) true (human $_360 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_360) true (human $_360 skc12) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_360) true (human $_360 skc15) true = true % 0.62/0.81 |- ifeq3 (human skc8 $_361) true (human skc10 $_361) true = true % 0.62/0.81 |- human skc10 skc15 = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $V) true (human $V skc15) true = true % 0.62/0.81 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.81 (ifeq3 (human $U skc15) true true true) true = true % 0.62/0.81 |- ifeq2 (tuple2 (nonhuman skc10 skc15) true) (tuple2 true true) a b = b % 0.62/0.81 |- ifeq3 (accessible_world $_371 skc10) true % 0.62/0.81 (ifeq3 (animate $_371 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_371 skc8) true % 0.62/0.81 (ifeq3 (animate $_371 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_371 skc8) true % 0.62/0.81 (ifeq3 (animate $_371 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_372) true (animate $_372 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_372) true (animate $_372 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_372) true (animate $_372 skc15) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (animate skc8 $_373) true (animate skc10 $_373) true = true % 0.62/0.81 |- animate skc10 skc15 = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $V) true (animate $V skc15) true = true % 0.62/0.81 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.81 (ifeq3 (animate $U skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_383 skc8) true % 0.62/0.81 (ifeq3 (vincent_forename $_383 skc14) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_384) true (vincent_forename $_384 skc14) % 0.62/0.81 true = true % 0.62/0.81 |- ifeq3 (vincent_forename skc8 $_385) true (vincent_forename skc10 $_385) % 0.62/0.81 true = true % 0.62/0.81 |- vincent_forename skc10 skc14 = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $V) true (vincent_forename $V skc14) % 0.62/0.81 true = true % 0.62/0.81 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.81 (ifeq3 (vincent_forename $U skc14) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_391 skc8) true % 0.62/0.81 (ifeq3 (man $_391 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_392) true (man $_392 skc15) true = true % 0.62/0.81 |- ifeq3 (man skc8 $_393) true (man skc10 $_393) true = true % 0.62/0.81 |- man skc10 skc15 = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $V) true (man $V skc15) true = true % 0.62/0.81 |- ifeq3 (accessible_world $U skc10) true % 0.62/0.81 (ifeq3 (man $U skc15) true true true) true = true % 0.62/0.81 |- male skc10 skc15 = true % 0.62/0.81 |- human_person skc10 skc15 = true % 0.62/0.81 |- ifeq2 (tuple2 (female skc10 skc15) true) (tuple2 true true) a b = b % 0.62/0.81 |- ifeq2 (tuple2 (unisex skc10 skc15) true) (tuple2 true true) a b = b % 0.62/0.81 |- ifeq3 (woman skc10 skc15) true true true = true % 0.62/0.81 |- ifeq3 (accessible_world $_399 skc10) true % 0.62/0.81 (ifeq3 (male $_399 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_399 skc8) true % 0.62/0.81 (ifeq3 (male $_399 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_400) true (male $_400 skc15) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_400) true (male $_400 skc15) true = true % 0.62/0.81 |- ifeq3 (male skc8 $_401) true (male skc10 $_401) true = true % 0.62/0.81 |- ifeq3 (agent $_414 skc13 skc12) true % 0.62/0.81 (ifeq3 (accessible_world $_414 skc10) true true true) true = true % 0.62/0.81 |- ifeq3 (agent $_414 skc9 skc12) true % 0.62/0.81 (ifeq3 (accessible_world $_414 skc8) true true true) true = true % 0.62/0.81 |- ifeq3 (agent skc8 $_416 $_417) true (agent skc10 $_416 $_417) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_415) true (agent $_415 skc13 skc12) % 0.62/0.81 true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_415) true (agent $_415 skc9 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- agent skc10 skc9 skc12 = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $V) true (agent $V skc9 skc12) true = true % 0.62/0.81 |- ifeq3 (agent $U skc9 skc12) true % 0.62/0.81 (ifeq3 (accessible_world $U skc10) true true true) true = true % 0.62/0.81 |- ifeq3 (agent skc8 skc13 skc12) true true true = true % 0.62/0.81 |- ifeq3 (theme $_426 skc9 skc10) true % 0.62/0.81 (ifeq3 (accessible_world $_426 skc8) true true true) true = true % 0.62/0.81 |- ifeq3 (theme skc8 $_428 $_429) true (theme skc10 $_428 $_429) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_427) true (theme $_427 skc9 skc10) true = % 0.62/0.81 true % 0.62/0.81 |- theme skc10 skc9 skc10 = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $V) true (theme $V skc9 skc10) true = true % 0.62/0.81 |- ifeq3 (theme $U skc9 skc10) true % 0.62/0.81 (ifeq3 (accessible_world $U skc10) true true true) true = true % 0.62/0.81 |- ifeq3 (of $_436 skc11 skc12) true % 0.62/0.81 (ifeq3 (accessible_world $_436 skc8) true true true) true = true % 0.62/0.81 |- ifeq3 (of $_436 skc14 skc15) true % 0.62/0.81 (ifeq3 (accessible_world $_436 skc8) true true true) true = true % 0.62/0.81 |- ifeq3 (of skc8 $_438 $_439) true (of skc10 $_438 $_439) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_437) true (of $_437 skc11 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_437) true (of $_437 skc14 skc15) true = % 0.62/0.81 true % 0.62/0.81 |- of skc10 skc11 skc12 = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $V) true (of $V skc11 skc12) true = true % 0.62/0.81 |- ifeq3 (of $U skc11 skc12) true % 0.62/0.81 (ifeq3 (accessible_world $U skc10) true true true) true = true % 0.62/0.81 |- of skc10 skc14 skc15 = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $V) true (of $V skc14 skc15) true = true % 0.62/0.81 |- ifeq3 (of $U skc14 skc15) true % 0.62/0.81 (ifeq3 (accessible_world $U skc10) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc10) true % 0.62/0.81 (ifeq3 (thing $_450 skc10) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc10) true % 0.62/0.81 (ifeq3 (thing $_450 skc11) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc10) true % 0.62/0.81 (ifeq3 (thing $_450 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc10) true % 0.62/0.81 (ifeq3 (thing $_450 skc13) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc10) true % 0.62/0.81 (ifeq3 (thing $_450 skc14) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc10) true % 0.62/0.81 (ifeq3 (thing $_450 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc10) true % 0.62/0.81 (ifeq3 (thing $_450 skc9) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc8) true % 0.62/0.81 (ifeq3 (thing $_450 skc10) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc8) true % 0.62/0.81 (ifeq3 (thing $_450 skc11) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc8) true % 0.62/0.81 (ifeq3 (thing $_450 skc12) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc8) true % 0.62/0.81 (ifeq3 (thing $_450 skc14) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc8) true % 0.62/0.81 (ifeq3 (thing $_450 skc15) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world $_450 skc8) true % 0.62/0.81 (ifeq3 (thing $_450 skc9) true true true) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_451) true (thing $_451 skc10) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_451) true (thing $_451 skc11) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_451) true (thing $_451 skc12) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_451) true (thing $_451 skc13) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_451) true (thing $_451 skc14) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_451) true (thing $_451 skc15) true = % 0.62/0.81 true % 0.62/0.81 |- ifeq3 (accessible_world skc10 $_451) true (thing $_451 skc9) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_451) true (thing $_451 skc10) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_451) true (thing $_451 skc11) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_451) true (thing $_451 skc12) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_451) true (thing $_451 skc14) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_451) true (thing $_451 skc15) true = true % 0.62/0.81 |- ifeq3 (accessible_world skc8 $_451) true (thing $_451 skc9) true = true % 0.62/0.81 |- ifeq3 (thing skc8 $_452) true (thing skc10 $_452) true = true % 0.62/0.81 |- ifeq3 (thing skc8 skc13) true true true = true % 0.62/0.81 |- ifeq3 (accessible_world $_480 skc10) true % 0.62/0.81 (ifeq3 (relation $_480 skc10) true true true) true = true % 0.62/0.82 |- ifeq3 (accessible_world $_480 skc10) true % 0.62/0.82 (ifeq3 (relation $_480 skc11) true true true) true = true % 0.62/0.82 |- ifeq3 (accessible_world $_480 skc10) true % 0.62/0.82 (ifeq3 (relation $_480 skc14) true true true) true = true % 0.62/0.82 |- ifeq3 (accessible_world $_480 skc8) true % 0.62/0.82 (ifeq3 (relation $_480 skc10) true true true) true = true % 0.62/0.82 |- ifeq3 (accessible_world $_480 skc8) true % 0.62/0.82 (ifeq3 (relation $_480 skc11) true true true) true = true % 0.62/0.82 |- ifeq3 (accessible_world $_480 skc8) true % 0.62/0.82 (ifeq3 (relation $_480 skc14) true true true) true = true % 0.62/0.82 |- ifeq3 (accessible_world skc10 $_481) true (relation $_481 skc10) true = % 0.62/0.82 true % 0.62/0.82 |- ifeq3 (accessible_world skc10 $_481) true (relation $_481 skc11) true = % 0.62/0.82 true % 0.62/0.82 |- ifeq3 (accessible_world skc10 $_481) true (relation $_481 skc14) true = % 0.62/0.82 true % 0.62/0.82 |- ifeq3 (accessible_world skc8 $_481) true (relation $_481 skc10) true = % 0.62/0.82 true % 0.62/0.82 |- ifeq3 (accessible_world skc8 $_481) true (relation $_481 skc11) true = % 0.62/0.82 true % 0.62/0.82 |- ifeq3 (accessible_world skc8 $_481) true (relation $_481 skc14) true = % 0.62/0.82 true % 0.62/0.82 |- ifeq3 (relation skc8 $_482) true (relation skc10 $_482) true = true % 0.62/0.82 |- ifeq3 (accessible_world $_496 skc10) true % 0.62/0.82 (ifeq3 (human_person $_496 skc12) true true true) true = true % 0.62/0.82 |- ifeq3 (accessible_world $_496 skc10) true % 0.62/0.82 (ifeq3 (human_person $_496 skc15) true true true) true = true % 0.62/0.82 |- ifeq3 (accessible_world $_496 skc8) true % 0.62/0.82 (ifeq3 (human_person $_496 skc12) true true true) true = true % 0.62/0.82 |- ifeq3 (accessible_world $_496 skc8) true % 0.62/0.82 (ifeq3 (human_person $_496 skc15) true true true) true = true % 0.62/0.82 |- ifeq3 (accessible_world skc10 $_497) true (human_person $_497 skc12) % 0.62/0.82 true = true % 0.62/0.82 |- ifeq3 (accessible_world skc10 $_497) true (human_person $_497 skc15) % 0.62/0.82 true = true % 0.62/0.82 |- ifeq3 (accessible_world skc8 $_497) true (human_person $_497 skc12) % 0.62/0.82 true = true % 0.62/0.82 |- ifeq3 (accessible_world skc8 $_497) true (human_person $_497 skc15) % 0.62/0.82 true = true % 0.62/0.82 |- ifeq3 (human_person skc8 $_498) true (human_person skc10 $_498) true = % 0.62/0.82 true % 0.62/0.82 |- ifeq3 (accessible_world $_508 skc10) true % 0.62/0.82 (ifeq3 (female $_508 skc12) true true true) true = true % 0.62/0.82 |- ifeq3 (accessible_world $_508 skc8) true % 0.62/0.82 (ifeq3 (female $_508 skc12) true true true) true = true % 0.62/0.82 |- ifeq3 (accessible_world skc10 $_509) true (female $_509 skc12) true = % 0.62/0.82 true % 0.62/0.82 |- ifeq3 (accessible_world skc8 $_509) true (female $_509 skc12) true = % 0.62/0.82 true % 0.62/0.82 |- ifeq3 (female skc8 $_510) true (female skc10 $_510) true = true % 0.62/0.82 |- ifeq4 (of skc10 $_518 $_519) true % 0.62/0.82 (ifeq4 (of skc10 skc11 $_519) true % 0.62/0.82 (ifeq4 (entity skc10 $_519) true % 0.62/0.82 (ifeq4 (forename skc10 $_518) true $_518 skc11) skc11) skc11) % 0.62/0.82 skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc10 $_518 $_519) true % 0.62/0.82 (ifeq4 (of skc10 skc14 $_519) true % 0.62/0.82 (ifeq4 (entity skc10 $_519) true % 0.62/0.82 (ifeq4 (forename skc10 $_518) true $_518 skc14) skc14) skc14) % 0.62/0.82 skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc8 $_518 $_519) true % 0.62/0.82 (ifeq4 (of skc8 skc11 $_519) true % 0.62/0.82 (ifeq4 (entity skc8 $_519) true % 0.62/0.82 (ifeq4 (forename skc8 $_518) true $_518 skc11) skc11) skc11) % 0.62/0.82 skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc8 $_518 $_519) true % 0.62/0.82 (ifeq4 (of skc8 skc14 $_519) true % 0.62/0.82 (ifeq4 (entity skc8 $_519) true % 0.62/0.82 (ifeq4 (forename skc8 $_518) true $_518 skc14) skc14) skc14) % 0.62/0.82 skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc10 skc11 $_519) true % 0.62/0.82 (ifeq4 (of skc10 $_517 $_519) true % 0.62/0.82 (ifeq4 (entity skc10 $_519) true % 0.62/0.82 (ifeq4 (forename skc10 $_517) true skc11 $_517) $_517) $_517) % 0.62/0.82 $_517 = $_517 % 0.62/0.82 |- ifeq4 (of skc10 skc14 $_519) true % 0.62/0.82 (ifeq4 (of skc10 $_517 $_519) true % 0.62/0.82 (ifeq4 (entity skc10 $_519) true % 0.62/0.82 (ifeq4 (forename skc10 $_517) true skc14 $_517) $_517) $_517) % 0.62/0.82 $_517 = $_517 % 0.62/0.82 |- ifeq4 (of skc8 skc11 $_519) true % 0.62/0.82 (ifeq4 (of skc8 $_517 $_519) true % 0.62/0.82 (ifeq4 (entity skc8 $_519) true % 0.62/0.82 (ifeq4 (forename skc8 $_517) true skc11 $_517) $_517) $_517) % 0.62/0.82 $_517 = $_517 % 0.62/0.82 |- ifeq4 (of skc8 skc14 $_519) true % 0.62/0.82 (ifeq4 (of skc8 $_517 $_519) true % 0.62/0.82 (ifeq4 (entity skc8 $_519) true % 0.62/0.82 (ifeq4 (forename skc8 $_517) true skc14 $_517) $_517) $_517) % 0.62/0.82 $_517 = $_517 % 0.62/0.82 |- ifeq4 (of skc10 $_518 skc12) true % 0.62/0.82 (ifeq4 (of skc10 $_517 skc12) true % 0.62/0.82 (ifeq4 (forename skc10 $_518) true % 0.62/0.82 (ifeq4 (forename skc10 $_517) true $_518 $_517) $_517) $_517) % 0.62/0.82 $_517 = $_517 % 0.62/0.82 |- ifeq4 (of skc10 $_518 skc15) true % 0.62/0.82 (ifeq4 (of skc10 $_517 skc15) true % 0.62/0.82 (ifeq4 (forename skc10 $_518) true % 0.62/0.82 (ifeq4 (forename skc10 $_517) true $_518 $_517) $_517) $_517) % 0.62/0.82 $_517 = $_517 % 0.62/0.82 |- ifeq4 (of skc8 $_518 skc12) true % 0.62/0.82 (ifeq4 (of skc8 $_517 skc12) true % 0.62/0.82 (ifeq4 (forename skc8 $_518) true % 0.62/0.82 (ifeq4 (forename skc8 $_517) true $_518 $_517) $_517) $_517) % 0.62/0.82 $_517 = $_517 % 0.62/0.82 |- ifeq4 (of skc8 $_518 skc15) true % 0.62/0.82 (ifeq4 (of skc8 $_517 skc15) true % 0.62/0.82 (ifeq4 (forename skc8 $_518) true % 0.62/0.82 (ifeq4 (forename skc8 $_517) true $_518 $_517) $_517) $_517) % 0.62/0.82 $_517 = $_517 % 0.62/0.82 |- ifeq4 (of skc10 $_518 skc12) true % 0.62/0.82 (ifeq4 (forename skc10 $_518) true $_518 skc11) skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc10 $_518 skc15) true % 0.62/0.82 (ifeq4 (forename skc10 $_518) true $_518 skc14) skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc8 $_518 skc12) true % 0.62/0.82 (ifeq4 (forename skc8 $_518) true $_518 skc11) skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc8 $_518 skc15) true % 0.62/0.82 (ifeq4 (forename skc8 $_518) true $_518 skc14) skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc10 $_517 skc12) true % 0.62/0.82 (ifeq4 (forename skc10 $_517) true skc11 $_517) $_517 = $_517 % 0.62/0.82 |- ifeq4 (of skc10 $_517 skc15) true % 0.62/0.82 (ifeq4 (forename skc10 $_517) true skc14 $_517) $_517 = $_517 % 0.62/0.82 |- ifeq4 (of skc8 $_517 skc12) true % 0.62/0.82 (ifeq4 (forename skc8 $_517) true skc11 $_517) $_517 = $_517 % 0.62/0.82 |- ifeq4 (of skc8 $_517 skc15) true % 0.62/0.82 (ifeq4 (forename skc8 $_517) true skc14 $_517) $_517 = $_517 % 0.62/0.82 |- ifeq4 (of skc10 skc14 skc12) true skc11 skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc10 skc11 skc15) true skc14 skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc8 skc14 skc12) true skc11 skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc8 skc11 skc15) true skc14 skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc10 skc14 skc12) true skc14 skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc10 skc11 skc15) true skc11 skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc8 skc14 skc12) true skc14 skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc8 skc11 skc15) true skc11 skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc10 skc11 $_529) true % 0.62/0.82 (ifeq4 (of skc10 skc11 $_529) true % 0.62/0.82 (ifeq4 (entity skc10 $_529) true skc11 skc11) skc11) skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc10 skc14 $_529) true % 0.62/0.82 (ifeq4 (of skc10 skc11 $_529) true % 0.62/0.82 (ifeq4 (entity skc10 $_529) true skc14 skc11) skc11) skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc10 $_528 skc15) true % 0.62/0.82 (ifeq4 (of skc10 skc11 skc15) true % 0.62/0.82 (ifeq4 (forename skc10 $_528) true $_528 skc11) skc11) skc11 = % 0.62/0.82 skc11 % 0.62/0.82 |- ifeq4 (of skc10 skc11 skc15) true % 0.62/0.82 (ifeq4 (of skc10 skc11 skc15) true skc11 skc11) skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc10 skc11 $_534) true % 0.62/0.82 (ifeq4 (of skc10 skc14 $_534) true % 0.62/0.82 (ifeq4 (entity skc10 $_534) true skc11 skc14) skc14) skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc10 skc14 $_534) true % 0.62/0.82 (ifeq4 (of skc10 skc14 $_534) true % 0.62/0.82 (ifeq4 (entity skc10 $_534) true skc14 skc14) skc14) skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc10 $_533 skc12) true % 0.62/0.82 (ifeq4 (of skc10 skc14 skc12) true % 0.62/0.82 (ifeq4 (forename skc10 $_533) true $_533 skc14) skc14) skc14 = % 0.62/0.82 skc14 % 0.62/0.82 |- ifeq4 (of skc10 skc14 skc12) true % 0.62/0.82 (ifeq4 (of skc10 skc14 skc12) true skc14 skc14) skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc8 skc11 $_539) true % 0.62/0.82 (ifeq4 (of skc8 skc11 $_539) true % 0.62/0.82 (ifeq4 (entity skc8 $_539) true skc11 skc11) skc11) skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc8 skc14 $_539) true % 0.62/0.82 (ifeq4 (of skc8 skc11 $_539) true % 0.62/0.82 (ifeq4 (entity skc8 $_539) true skc14 skc11) skc11) skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc8 $_538 skc15) true % 0.62/0.82 (ifeq4 (of skc8 skc11 skc15) true % 0.62/0.82 (ifeq4 (forename skc8 $_538) true $_538 skc11) skc11) skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc8 skc11 skc15) true % 0.62/0.82 (ifeq4 (of skc8 skc11 skc15) true skc11 skc11) skc11 = skc11 % 0.62/0.82 |- ifeq4 (of skc8 skc11 $_544) true % 0.62/0.82 (ifeq4 (of skc8 skc14 $_544) true % 0.62/0.82 (ifeq4 (entity skc8 $_544) true skc11 skc14) skc14) skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc8 skc14 $_544) true % 0.62/0.82 (ifeq4 (of skc8 skc14 $_544) true % 0.62/0.82 (ifeq4 (entity skc8 $_544) true skc14 skc14) skc14) skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc8 $_543 skc12) true % 0.62/0.82 (ifeq4 (of skc8 skc14 skc12) true % 0.62/0.82 (ifeq4 (forename skc8 $_543) true $_543 skc14) skc14) skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc8 skc14 skc12) true % 0.62/0.82 (ifeq4 (of skc8 skc14 skc12) true skc14 skc14) skc14 = skc14 % 0.62/0.82 |- ifeq4 (of skc10 skc11 skc15) true % 0.62/0.82 (ifeq4 (of skc10 $_548 skc15) true % 0.62/0.82 (ifeq4 (forename skc10 $_548) true skc11 $_548) $_548) $_548 = % 0.62/0.82 $_548 % 0.62/0.82 |- ifeq4 (of skc10 skc14 skc12) true % 0.62/0.82 (ifeq4 (of skc10 $_551 skc12) true % 0.62/0.82 (ifeq4 (forename skc10 $_551) true skc14 $_551) $_551) $_551 = % 0.62/0.82 $_551 % 0.62/0.82 |- ifeq4 (of skc8 skc11 skc15) true % 0.62/0.82 (ifeq4 (of skc8 $_554 skc15) true % 0.62/0.82 (ifeq4 (forename skc8 $_554) true skc11 $_554) $_554) $_554 = $_554 % 0.62/0.82 |- ifeq4 (of skc8 skc14 skc12) true % 0.62/0.82 (ifeq4 (of skc8 $_557 skc12) true % 0.62/0.82 (ifeq4 (forename skc8 $_557) true skc14 $_557) $_557) $_557 = $_557 % 0.62/0.82 |- ifeq % 0.62/0.82 (tuple (dance skc10 $_570) (event skc10 $_570) true true true % 0.62/0.82 (present skc10 $_570) true (agent skc10 $_570 skc15) % 0.62/0.82 (agent skc8 skc9 skc15) true) % 0.62/0.82 (tuple true true true true true true true true true true) a b = b % 0.62/0.82 |- ifeq % 0.62/0.82 (tuple (dance $_569 $_570) (event $_569 $_570) true % 0.62/0.82 (proposition skc8 $_569) (accessible_world skc8 $_569) % 0.62/0.82 (present $_569 $_570) true (agent $_569 $_570 skc15) % 0.62/0.82 (agent skc8 skc9 skc15) (theme skc8 skc9 $_569)) % 0.62/0.82 (tuple true true true true true true true true true true) a b = b % 0.62/0.82 |- ifeq % 0.62/0.82 (tuple true true (desire_want skc8 $_568) true true true % 0.62/0.82 (present skc8 $_568) (agent skc10 skc13 skc15) % 0.62/0.82 (agent skc8 $_568 skc15) (theme skc8 $_568 skc10)) % 0.62/0.82 (tuple true true true true true true true true true true) a b = b % 0.62/0.82 |- ifeq % 0.62/0.82 (tuple (dance skc10 skc9) true (desire_want skc8 $_568) true true true % 0.62/0.82 (present skc8 $_568) (agent skc10 skc9 skc15) % 0.62/0.82 (agent skc8 $_568 skc15) (theme skc8 $_568 skc10)) % 0.62/0.82 (tuple true true true true true true true true true true) a b = b % 0.62/0.82 |- ifeq % 0.62/0.82 (tuple (dance skc8 skc9) true (desire_want skc8 $_568) % 0.62/0.82 (proposition skc8 skc8) (accessible_world skc8 skc8) true % 0.62/0.82 (present skc8 $_568) (agent skc8 skc9 skc15) % 0.62/0.82 (agent skc8 $_568 skc15) (theme skc8 $_568 skc8)) % 0.62/0.82 (tuple true true true true true true true true true true) a b = b % 0.62/0.82 |- ifeq % 0.62/0.82 (tuple (dance skc10 $_570) (event skc10 $_570) % 0.62/0.82 (desire_want skc8 $_568) true true (present skc10 $_570) % 0.62/0.82 (present skc8 $_568) (agent skc10 $_570 skc15) % 0.62/0.82 (agent skc8 $_568 skc15) (theme skc8 $_568 skc10)) % 0.62/0.82 (tuple true true true true true true true true true true) a b = b % 0.62/0.82 |- ifeq % 0.62/0.82 (tuple true true true true true true true (agent skc10 skc13 skc15) % 0.62/0.82 (agent skc8 skc9 skc15) true) % 0.62/0.82 (tuple true true true true true true true true true true) a b = b % 0.62/0.82 |- ifeq % 0.62/0.82 (tuple (dance skc10 skc9) true true true true true true % 0.62/0.82 (agent skc10 skc9 skc15) (agent skc8 skc9 skc15) true) % 0.62/0.82 (tuple true true true true true true true true true true) a b = b % 0.62/0.82 |- ifeq % 0.62/0.82 (tuple (dance skc8 skc9) true true (proposition skc8 skc8) % 0.62/0.82 (accessible_world skc8 skc8) true true (agent skc8 skc9 skc15) % 0.62/0.82 (agent skc8 skc9 skc15) (theme skc8 skc9 skc8)) % 0.62/0.82 (tuple true true true true true true true true true true) a b = b % 0.62/0.82 |- ifeq4 (theme skc10 $_583 $_582) true % 0.62/0.82 (ifeq4 (theme skc10 skc9 $_581) true % 0.62/0.82 (ifeq4 (proposition skc10 $_582) true % 0.62/0.82 (ifeq4 (proposition skc10 $_581) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_583) true $_582 $_581) $_581) % 0.62/0.82 $_581) $_581) $_581 = $_581 % 0.62/0.82 |- ifeq4 (theme skc8 $_583 $_582) true % 0.62/0.82 (ifeq4 (theme skc8 skc9 $_581) true % 0.62/0.82 (ifeq4 (proposition skc8 $_582) true % 0.62/0.82 (ifeq4 (proposition skc8 $_581) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_583) true $_582 $_581) $_581) % 0.62/0.82 $_581) $_581) $_581 = $_581 % 0.62/0.82 |- ifeq4 (theme skc10 skc9 $_582) true % 0.62/0.82 (ifeq4 (theme skc10 $_580 $_581) true % 0.62/0.82 (ifeq4 (proposition skc10 $_582) true % 0.62/0.82 (ifeq4 (proposition skc10 $_581) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_580) true $_582 $_581) $_581) % 0.62/0.82 $_581) $_581) $_581 = $_581 % 0.62/0.82 |- ifeq4 (theme skc8 skc9 $_582) true % 0.62/0.82 (ifeq4 (theme skc8 $_580 $_581) true % 0.62/0.82 (ifeq4 (proposition skc8 $_582) true % 0.62/0.82 (ifeq4 (proposition skc8 $_581) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_580) true $_582 $_581) $_581) % 0.62/0.82 $_581) $_581) $_581 = $_581 % 0.62/0.82 |- ifeq4 (theme skc10 $_583 $_582) true % 0.62/0.82 (ifeq4 (theme skc10 $_580 skc10) true % 0.62/0.82 (ifeq4 (proposition skc10 $_582) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_583) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_580) true $_582 skc10) skc10) % 0.62/0.82 skc10) skc10) skc10 = skc10 % 0.62/0.82 |- ifeq4 (theme skc8 $_583 $_582) true % 0.62/0.82 (ifeq4 (theme skc8 $_580 skc10) true % 0.62/0.82 (ifeq4 (proposition skc8 $_582) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_583) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_580) true $_582 skc10) skc10) % 0.62/0.82 skc10) skc10) skc10 = skc10 % 0.62/0.82 |- ifeq4 (theme skc10 $_583 skc10) true % 0.62/0.82 (ifeq4 (theme skc10 $_580 $_581) true % 0.62/0.82 (ifeq4 (proposition skc10 $_581) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_583) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_580) true skc10 $_581) $_581) % 0.62/0.82 $_581) $_581) $_581 = $_581 % 0.62/0.82 |- ifeq4 (theme skc8 $_583 skc10) true % 0.62/0.82 (ifeq4 (theme skc8 $_580 $_581) true % 0.62/0.82 (ifeq4 (proposition skc8 $_581) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_583) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_580) true skc10 $_581) $_581) % 0.62/0.82 $_581) $_581) $_581 = $_581 % 0.62/0.82 |- ifeq4 (theme skc10 $_583 $_582) true % 0.62/0.82 (ifeq4 (proposition skc10 $_582) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_583) true $_582 skc10) skc10) skc10 = % 0.62/0.82 skc10 % 0.62/0.82 |- ifeq4 (theme skc8 $_583 $_582) true % 0.62/0.82 (ifeq4 (proposition skc8 $_582) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_583) true $_582 skc10) skc10) skc10 = % 0.62/0.82 skc10 % 0.62/0.82 |- ifeq4 (theme skc10 $_580 $_581) true % 0.62/0.82 (ifeq4 (proposition skc10 $_581) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_580) true skc10 $_581) $_581) $_581 = % 0.62/0.82 $_581 % 0.62/0.82 |- ifeq4 (theme skc8 $_580 $_581) true % 0.62/0.82 (ifeq4 (proposition skc8 $_581) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_580) true skc10 $_581) $_581) $_581 = % 0.62/0.82 $_581 % 0.62/0.82 |- ifeq4 (theme skc10 skc9 $_585) true % 0.62/0.82 (ifeq4 (proposition skc10 $_585) true skc10 $_585) $_585 = $_585 % 0.62/0.82 |- ifeq4 (theme skc10 $_584 skc10) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_584) true skc10 skc10) skc10 = skc10 % 0.62/0.82 |- ifeq4 (theme skc8 skc9 $_589) true % 0.62/0.82 (ifeq4 (proposition skc8 $_589) true skc10 $_589) $_589 = $_589 % 0.62/0.82 |- ifeq4 (theme skc8 $_588 skc10) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_588) true skc10 skc10) skc10 = skc10 % 0.62/0.82 |- ifeq4 (theme skc10 skc9 $_592) true % 0.62/0.82 (ifeq4 (proposition skc10 $_592) true $_592 skc10) skc10 = skc10 % 0.62/0.82 |- ifeq4 (theme skc8 skc9 $_595) true % 0.62/0.82 (ifeq4 (proposition skc8 $_595) true $_595 skc10) skc10 = skc10 % 0.62/0.82 |- ifeq4 (theme skc10 skc9 $_599) true % 0.62/0.82 (ifeq4 (theme skc10 skc9 $_598) true % 0.62/0.82 (ifeq4 (proposition skc10 $_599) true % 0.62/0.82 (ifeq4 (proposition skc10 $_598) true $_599 $_598) $_598) $_598) % 0.62/0.82 $_598 = $_598 % 0.62/0.82 |- ifeq4 (theme skc10 $_600 skc10) true % 0.62/0.82 (ifeq4 (theme skc10 skc9 $_598) true % 0.62/0.82 (ifeq4 (proposition skc10 $_598) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_600) true skc10 $_598) $_598) $_598) % 0.62/0.82 $_598 = $_598 % 0.62/0.82 |- ifeq4 (theme skc8 skc9 $_606) true % 0.62/0.82 (ifeq4 (theme skc8 skc9 $_605) true % 0.62/0.82 (ifeq4 (proposition skc8 $_606) true % 0.62/0.82 (ifeq4 (proposition skc8 $_605) true $_606 $_605) $_605) $_605) % 0.62/0.82 $_605 = $_605 % 0.62/0.82 |- ifeq4 (theme skc8 $_607 skc10) true % 0.62/0.82 (ifeq4 (theme skc8 skc9 $_605) true % 0.62/0.82 (ifeq4 (proposition skc8 $_605) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_607) true skc10 $_605) $_605) $_605) % 0.62/0.82 $_605 = $_605 % 0.62/0.82 |- ifeq4 (theme skc10 skc9 $_613) true % 0.62/0.82 (ifeq4 (theme skc10 $_612 skc10) true % 0.62/0.82 (ifeq4 (proposition skc10 $_613) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_612) true $_613 skc10) skc10) skc10) % 0.62/0.82 skc10 = skc10 % 0.62/0.82 |- ifeq4 (theme skc10 $_614 skc10) true % 0.62/0.82 (ifeq4 (theme skc10 $_612 skc10) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_614) true % 0.62/0.82 (ifeq4 (desire_want skc10 $_612) true skc10 skc10) skc10) skc10) % 0.62/0.82 skc10 = skc10 % 0.62/0.82 |- ifeq4 (theme skc8 skc9 $_620) true % 0.62/0.82 (ifeq4 (theme skc8 $_619 skc10) true % 0.62/0.82 (ifeq4 (proposition skc8 $_620) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_619) true $_620 skc10) skc10) skc10) % 0.62/0.82 skc10 = skc10 % 0.62/0.82 |- ifeq4 (theme skc8 $_621 skc10) true % 0.62/0.82 (ifeq4 (theme skc8 $_619 skc10) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_621) true % 0.62/0.82 (ifeq4 (desire_want skc8 $_619) true skc10 skc10) skc10) skc10) % 0.62/0.82 skc10 = skc10 % 0.62/0.82 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.62/0.82 %------------------------------------------------------------------------------