Metis---2.4.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : NLP224-10 : TPTP v8.1.0. Released v7.5.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:16 EDT 2022

% Result   : Satisfiable 0.71s 0.87s
% Output   : Saturation 0.77s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12  % Problem  : NLP224-10 : TPTP v8.1.0. Released v7.5.0.
% 0.10/0.12  % Command  : metis --show proof --show saturation %s
% 0.13/0.33  % Computer : n011.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33  % CPULimit : 300
% 0.13/0.33  % WCLimit  : 600
% 0.13/0.33  % DateTime : Thu Jun 30 21:57:48 EDT 2022
% 0.13/0.33  % CPUTime  : 
% 0.13/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.71/0.87  % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.71/0.87  
% 0.71/0.87  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.71/0.87  |- ifeq3 $A $A $B $C = $B
% 0.71/0.87  |- ifeq2 $A $A $B $C = $B
% 0.71/0.87  |- ifeq $A $A $B $C = $B
% 0.71/0.87  |- ifeq2 (state $U $V) true (eventuality $U $V) true = true
% 0.71/0.87  |- ifeq2 (eventuality $U $V) true (thing $U $V) true = true
% 0.71/0.87  |- ifeq2 (thing $U $V) true (singleton $U $V) true = true
% 0.71/0.87  |- ifeq2 (eventuality $U $V) true (specific $U $V) true = true
% 0.71/0.87  |- ifeq2 (eventuality $U $V) true (nonexistent $U $V) true = true
% 0.71/0.87  |- ifeq2 (eventuality $U $V) true (unisex $U $V) true = true
% 0.71/0.87  |- ifeq2 (state $U $V) true (event $U $V) true = true
% 0.71/0.87  |- ifeq2 (event $U $V) true (eventuality $U $V) true = true
% 0.71/0.87  |- ifeq2 (man $U $V) true (human_person $U $V) true = true
% 0.71/0.87  |- ifeq2 (human_person $U $V) true (organism $U $V) true = true
% 0.71/0.87  |- ifeq2 (organism $U $V) true (entity $U $V) true = true
% 0.71/0.87  |- ifeq2 (entity $U $V) true (thing $U $V) true = true
% 0.71/0.87  |- ifeq2 (entity $U $V) true (specific $U $V) true = true
% 0.71/0.87  |- ifeq2 (entity $U $V) true (existent $U $V) true = true
% 0.71/0.87  |- ifeq2 (organism $U $V) true (impartial $U $V) true = true
% 0.71/0.87  |- ifeq2 (organism $U $V) true (living $U $V) true = true
% 0.71/0.87  |- ifeq2 (human_person $U $V) true (human $U $V) true = true
% 0.71/0.87  |- ifeq2 (human_person $U $V) true (animate $U $V) true = true
% 0.71/0.87  |- ifeq2 (man $U $V) true (male $U $V) true = true
% 0.71/0.87  |- ifeq2 (forename $U $V) true (relname $U $V) true = true
% 0.71/0.87  |- ifeq2 (relname $U $V) true (relation $U $V) true = true
% 0.71/0.87  |- ifeq2 (relation $U $V) true (abstraction $U $V) true = true
% 0.71/0.87  |- ifeq2 (abstraction $U $V) true (thing $U $V) true = true
% 0.71/0.87  |- ifeq2 (abstraction $U $V) true (nonhuman $U $V) true = true
% 0.71/0.87  |- ifeq2 (abstraction $U $V) true (general $U $V) true = true
% 0.71/0.87  |- ifeq2 (abstraction $U $V) true (unisex $U $V) true = true
% 0.71/0.87  |- ifeq2 (jules_forename $U $V) true (forename $U $V) true = true
% 0.71/0.87  |- ifeq2 (smoke $U $V) true (event $U $V) true = true
% 0.71/0.87  |- ifeq2 (proposition $U $V) true (relation $U $V) true = true
% 0.71/0.87  |- ifeq2 (vincent_forename $U $V) true (forename $U $V) true = true
% 0.71/0.87  |- ifeq3 (be $U $V $W $X) true $W $X = $X
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (state $U $W) true (state $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (eventuality $U $W) true (eventuality $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (thing $U $W) true (thing $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (singleton $U $W) true (singleton $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (specific $U $W) true (specific $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (nonexistent $U $W) true (nonexistent $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (unisex $U $W) true (unisex $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (event $U $W) true (event $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (man $U $W) true (man $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (human_person $U $W) true (human_person $V $W) true) true =
% 0.71/0.87     true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (organism $U $W) true (organism $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (entity $U $W) true (entity $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (existent $U $W) true (existent $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (impartial $U $W) true (impartial $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (living $U $W) true (living $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (human $U $W) true (human $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (animate $U $W) true (animate $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (male $U $W) true (male $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (forename $U $W) true (forename $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (relname $U $W) true (relname $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (relation $U $W) true (relation $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (abstraction $U $W) true (abstraction $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (nonhuman $U $W) true (nonhuman $V $W) true) true = true
% 0.71/0.87  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.87       (ifeq2 (general $U $W) true (general $V $W) true) true = true
% 0.71/0.88  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.88       (ifeq2 (jules_forename $U $W) true (jules_forename $V $W) true) true =
% 0.71/0.88     true
% 0.71/0.88  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.88       (ifeq2 (smoke $U $W) true (smoke $V $W) true) true = true
% 0.71/0.88  |- ifeq2 (present $U $W) true
% 0.71/0.88       (ifeq2 (accessible_world $U $V) true (present $V $W) true) true = true
% 0.71/0.88  |- ifeq2 (think_believe_consider $U $W) true
% 0.71/0.88       (ifeq2 (accessible_world $U $V) true (think_believe_consider $V $W)
% 0.71/0.88          true) true = true
% 0.71/0.88  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.88       (ifeq2 (proposition $U $W) true (proposition $V $W) true) true = true
% 0.71/0.88  |- ifeq2 (accessible_world $U $V) true
% 0.71/0.88       (ifeq2 (vincent_forename $U $W) true (vincent_forename $V $W) true)
% 0.71/0.88       true = true
% 0.71/0.88  |- ifeq2 (of $U $W $X) true
% 0.71/0.88       (ifeq2 (accessible_world $U $V) true (of $V $W $X) true) true = true
% 0.71/0.88  |- ifeq2 (agent $U $W $X) true
% 0.71/0.88       (ifeq2 (accessible_world $U $V) true (agent $V $W $X) true) true =
% 0.71/0.88     true
% 0.71/0.88  |- ifeq2 (theme $U $W $X) true
% 0.71/0.88       (ifeq2 (accessible_world $U $V) true (theme $V $W $X) true) true =
% 0.71/0.88     true
% 0.71/0.88  |- ifeq2 (be $U $W $X $Y) true
% 0.71/0.88       (ifeq2 (accessible_world $U $V) true (be $V $W $X $Y) true) true =
% 0.71/0.88     true
% 0.71/0.88  |- ifeq3 (of $U $W $X) true
% 0.71/0.88       (ifeq3 (of $U $V $X) true
% 0.71/0.88          (ifeq3 (forename $U $W) true
% 0.71/0.88             (ifeq3 (forename $U $V) true (ifeq3 (entity $U $X) true $W $V)
% 0.71/0.88                $V) $V) $V) $V = $V
% 0.71/0.88  |- ifeq3 (theme $U $Y $W) true
% 0.71/0.88       (ifeq3 (theme $U $X $V) true
% 0.71/0.88          (ifeq3 (agent $U $Y $Z) true
% 0.71/0.88             (ifeq3 (agent $U $X $Z) true
% 0.71/0.88                (ifeq3 (think_believe_consider $U $Y) true
% 0.71/0.88                   (ifeq3 (think_believe_consider $U $X) true
% 0.71/0.88                      (ifeq3 (proposition $U $W) true
% 0.71/0.88                         (ifeq3 (proposition $U $V) true $V $W) $W) $W) $W)
% 0.71/0.88                $W) $W) $W) $W = $W
% 0.71/0.88  |- ifeq (tuple (unisex $U $V) (male $U $V)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple (specific $U $V) (general $U $V)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple (human $U $V) (nonhuman $U $V)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple (nonexistent $U $V) (existent $U $V)) (tuple true true) a
% 0.71/0.88       b = b
% 0.71/0.88  |- actual_world skc9 = true
% 0.71/0.88  |- man skc9 skc17 = true
% 0.71/0.88  |- forename skc9 skc16 = true
% 0.71/0.88  |- vincent_forename skc9 skc16 = true
% 0.71/0.88  |- event skc9 skc15 = true
% 0.71/0.88  |- present skc9 skc15 = true
% 0.71/0.88  |- think_believe_consider skc9 skc15 = true
% 0.71/0.88  |- forename skc9 skc12 = true
% 0.71/0.88  |- jules_forename skc9 skc12 = true
% 0.71/0.88  |- man skc9 skc11 = true
% 0.71/0.88  |- state skc9 skc10 = true
% 0.71/0.88  |- accessible_world skc9 skc14 = true
% 0.71/0.88  |- proposition skc9 skc14 = true
% 0.71/0.88  |- of skc9 skc16 skc17 = true
% 0.71/0.88  |- agent skc9 skc15 skc17 = true
% 0.71/0.88  |- theme skc9 skc15 skc14 = true
% 0.71/0.88  |- of skc9 skc12 skc11 = true
% 0.71/0.88  |- be skc9 skc10 skc11 skc11 = true
% 0.71/0.88  |- ifeq2 (man skc14 $U) true true true = true
% 0.71/0.88  |- ifeq2 (man skc14 $U) true (agent skc14 (skf1 $U) $U) true = true
% 0.71/0.88  |- ~(a = b)
% 0.71/0.88  |- ifeq2 (state skc9 skc15) true true true = true
% 0.71/0.88  |- event skc9 skc10 = true
% 0.71/0.88  |- male skc9 skc11 = true
% 0.71/0.88  |- male skc9 skc17 = true
% 0.71/0.88  |- ifeq2 (jules_forename skc9 skc16) true true true = true
% 0.71/0.88  |- ifeq2 (vincent_forename skc9 skc12) true true true = true
% 0.71/0.88  |- eventuality skc9 skc10 = true
% 0.71/0.88  |- unisex skc9 skc10 = true
% 0.71/0.88  |- thing skc9 skc10 = true
% 0.71/0.88  |- ifeq2 (abstraction skc9 skc10) true true true = true
% 0.71/0.88  |- singleton skc9 skc10 = true
% 0.71/0.88  |- specific skc9 skc10 = true
% 0.71/0.88  |- nonexistent skc9 skc10 = true
% 0.71/0.88  |- eventuality skc9 skc15 = true
% 0.71/0.88  |- nonexistent skc9 skc15 = true
% 0.71/0.88  |- specific skc9 skc15 = true
% 0.71/0.88  |- unisex skc9 skc15 = true
% 0.71/0.88  |- thing skc9 skc15 = true
% 0.71/0.88  |- ifeq2 (abstraction skc9 skc15) true true true = true
% 0.71/0.88  |- singleton skc9 skc15 = true
% 0.71/0.88  |- human_person skc9 skc11 = true
% 0.71/0.88  |- human_person skc9 skc17 = true
% 0.71/0.88  |- animate skc9 skc11 = true
% 0.71/0.88  |- organism skc9 skc11 = true
% 0.71/0.88  |- animate skc9 skc17 = true
% 0.71/0.88  |- organism skc9 skc17 = true
% 0.71/0.88  |- impartial skc9 skc11 = true
% 0.71/0.88  |- entity skc9 skc11 = true
% 0.71/0.88  |- existent skc9 skc11 = true
% 0.71/0.88  |- impartial skc9 skc17 = true
% 0.71/0.88  |- entity skc9 skc17 = true
% 0.71/0.88  |- existent skc9 skc17 = true
% 0.71/0.88  |- ifeq2 (entity skc9 skc10) true true true = true
% 0.71/0.88  |- ifeq2 (entity skc9 skc15) true true true = true
% 0.71/0.88  |- thing skc9 skc11 = true
% 0.71/0.88  |- thing skc9 skc17 = true
% 0.71/0.88  |- ifeq2 (abstraction skc9 skc11) true true true = true
% 0.71/0.88  |- singleton skc9 skc11 = true
% 0.71/0.88  |- ifeq2 (eventuality skc9 skc11) true true true = true
% 0.71/0.88  |- ifeq2 (abstraction skc9 skc17) true true true = true
% 0.71/0.88  |- singleton skc9 skc17 = true
% 0.71/0.88  |- ifeq2 (eventuality skc9 skc17) true true true = true
% 0.71/0.88  |- specific skc9 skc11 = true
% 0.71/0.88  |- specific skc9 skc17 = true
% 0.71/0.88  |- living skc9 skc11 = true
% 0.71/0.88  |- living skc9 skc17 = true
% 0.71/0.88  |- human skc9 skc11 = true
% 0.71/0.88  |- human skc9 skc17 = true
% 0.71/0.88  |- relname skc9 skc12 = true
% 0.71/0.88  |- relname skc9 skc16 = true
% 0.71/0.88  |- relation skc9 skc12 = true
% 0.71/0.88  |- relation skc9 skc16 = true
% 0.71/0.88  |- abstraction skc9 skc16 = true
% 0.71/0.88  |- unisex skc9 skc16 = true
% 0.71/0.88  |- thing skc9 skc16 = true
% 0.71/0.88  |- ifeq2 (eventuality skc9 skc16) true true true = true
% 0.71/0.88  |- abstraction skc9 skc12 = true
% 0.71/0.88  |- unisex skc9 skc12 = true
% 0.71/0.88  |- thing skc9 skc12 = true
% 0.71/0.88  |- ifeq2 (eventuality skc9 skc12) true true true = true
% 0.71/0.88  |- ifeq2 (entity skc9 skc12) true true true = true
% 0.71/0.88  |- singleton skc9 skc12 = true
% 0.71/0.88  |- ifeq2 (entity skc9 skc16) true true true = true
% 0.71/0.88  |- singleton skc9 skc16 = true
% 0.71/0.88  |- nonhuman skc9 skc12 = true
% 0.71/0.88  |- nonhuman skc9 skc16 = true
% 0.71/0.88  |- general skc9 skc12 = true
% 0.71/0.88  |- general skc9 skc16 = true
% 0.71/0.88  |- ifeq2 (smoke skc9 skc10) true true true = true
% 0.71/0.88  |- ifeq2 (smoke skc9 skc15) true true true = true
% 0.71/0.88  |- ifeq2 (proposition skc9 skc12) true true true = true
% 0.71/0.88  |- ifeq2 (proposition skc9 skc16) true true true = true
% 0.71/0.88  |- relation skc9 skc14 = true
% 0.71/0.88  |- ifeq2 (relname skc9 skc14) true true true = true
% 0.71/0.88  |- abstraction skc9 skc14 = true
% 0.71/0.88  |- general skc9 skc14 = true
% 0.71/0.88  |- nonhuman skc9 skc14 = true
% 0.71/0.88  |- unisex skc9 skc14 = true
% 0.71/0.88  |- thing skc9 skc14 = true
% 0.71/0.88  |- ifeq2 (eventuality skc9 skc14) true true true = true
% 0.71/0.88  |- ifeq2 (entity skc9 skc14) true true true = true
% 0.71/0.88  |- singleton skc9 skc14 = true
% 0.71/0.88  |- ifeq (tuple (specific skc9 skc12) true) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple (specific skc9 skc14) true) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple (specific skc9 skc16) true) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (general skc9 skc10)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (general skc9 skc11)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (general skc9 skc15)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (general skc9 skc17)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple (human skc9 skc12) true) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple (human skc9 skc14) true) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple (human skc9 skc16) true) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (nonhuman skc9 skc11)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (nonhuman skc9 skc17)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple (unisex skc9 skc11) true) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple (unisex skc9 skc17) true) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (male skc9 skc10)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (male skc9 skc12)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (male skc9 skc14)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (male skc9 skc15)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (male skc9 skc16)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple (nonexistent skc9 skc11) true) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple (nonexistent skc9 skc17) true) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (existent skc9 skc10)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (existent skc9 skc15)) (tuple true true) a b = b
% 0.71/0.88  |- skc13 = skc11
% 0.71/0.88  |- ifeq2 (accessible_world $_88 skc9) true
% 0.71/0.88       (ifeq2 (state $_88 skc10) true true true) true = true
% 0.71/0.88  |- ifeq2 (accessible_world skc9 $_89) true (state $_89 skc10) true = true
% 0.71/0.88  |- ifeq2 (state skc9 $_90) true (state skc14 $_90) true = true
% 0.71/0.88  |- ifeq2 (accessible_world skc9 skc9) true true true = true
% 0.71/0.88  |- state skc14 skc10 = true
% 0.71/0.88  |- ifeq2 (accessible_world skc14 $V) true (state $V skc10) true = true
% 0.71/0.88  |- ifeq2 (accessible_world $U skc14) true
% 0.71/0.88       (ifeq2 (state $U skc10) true true true) true = true
% 0.71/0.88  |- eventuality skc14 skc10 = true
% 0.71/0.88  |- event skc14 skc10 = true
% 0.71/0.88  |- nonexistent skc14 skc10 = true
% 0.71/0.88  |- specific skc14 skc10 = true
% 0.71/0.88  |- unisex skc14 skc10 = true
% 0.71/0.88  |- thing skc14 skc10 = true
% 0.71/0.88  |- ifeq2 (smoke skc14 skc10) true true true = true
% 0.71/0.88  |- ifeq (tuple true (existent skc14 skc10)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq (tuple true (general skc14 skc10)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq2 (entity skc14 skc10) true true true = true
% 0.71/0.88  |- ifeq (tuple true (male skc14 skc10)) (tuple true true) a b = b
% 0.71/0.88  |- ifeq2 (abstraction skc14 skc10) true true true = true
% 0.71/0.89  |- singleton skc14 skc10 = true
% 0.71/0.89  |- ifeq2 (accessible_world skc14 skc9) true true true = true
% 0.71/0.89  |- ifeq2 (accessible_world skc14 skc14) true true true = true
% 0.71/0.89  |- ifeq2 (accessible_world $_96 skc14) true
% 0.71/0.89       (ifeq2 (eventuality $_96 skc10) true true true) true = true
% 0.71/0.89  |- ifeq2 (accessible_world $_96 skc9) true
% 0.71/0.89       (ifeq2 (eventuality $_96 skc10) true true true) true = true
% 0.71/0.89  |- ifeq2 (accessible_world $_96 skc9) true
% 0.71/0.89       (ifeq2 (eventuality $_96 skc15) true true true) true = true
% 0.71/0.89  |- ifeq2 (accessible_world skc14 $_97) true (eventuality $_97 skc10) true =
% 0.71/0.89     true
% 0.71/0.89  |- ifeq2 (accessible_world skc9 $_97) true (eventuality $_97 skc10) true =
% 0.71/0.89     true
% 0.71/0.89  |- ifeq2 (accessible_world skc9 $_97) true (eventuality $_97 skc15) true =
% 0.71/0.89     true
% 0.71/0.89  |- ifeq2 (eventuality skc9 $_98) true (eventuality skc14 $_98) true = true
% 0.71/0.89  |- eventuality skc14 skc15 = true
% 0.71/0.89  |- ifeq2 (accessible_world skc14 $V) true (eventuality $V skc15) true =
% 0.71/0.89     true
% 0.71/0.89  |- ifeq2 (accessible_world $U skc14) true
% 0.71/0.89       (ifeq2 (eventuality $U skc15) true true true) true = true
% 0.71/0.89  |- nonexistent skc14 skc15 = true
% 0.71/0.89  |- specific skc14 skc15 = true
% 0.71/0.89  |- ifeq2 (state skc14 skc15) true true true = true
% 0.71/0.89  |- unisex skc14 skc15 = true
% 0.71/0.89  |- thing skc14 skc15 = true
% 0.71/0.89  |- ifeq (tuple true (existent skc14 skc15)) (tuple true true) a b = b
% 0.71/0.89  |- ifeq (tuple true (general skc14 skc15)) (tuple true true) a b = b
% 0.71/0.89  |- ifeq2 (entity skc14 skc15) true true true = true
% 0.71/0.89  |- ifeq (tuple true (male skc14 skc15)) (tuple true true) a b = b
% 0.71/0.89  |- ifeq2 (abstraction skc14 skc15) true true true = true
% 0.71/0.89  |- singleton skc14 skc15 = true
% 0.71/0.89  |- ifeq2 (accessible_world $_107 skc14) true
% 0.71/0.89       (ifeq2 (thing $_107 skc10) true true true) true = true
% 0.71/0.89  |- ifeq2 (accessible_world $_107 skc14) true
% 0.71/0.89       (ifeq2 (thing $_107 skc15) true true true) true = true
% 0.71/0.89  |- ifeq2 (accessible_world $_107 skc9) true
% 0.71/0.89       (ifeq2 (thing $_107 skc10) true true true) true = true
% 0.71/0.89  |- ifeq2 (accessible_world $_107 skc9) true
% 0.71/0.89       (ifeq2 (thing $_107 skc11) true true true) true = true
% 0.71/0.89  |- ifeq2 (accessible_world $_107 skc9) true
% 0.71/0.89       (ifeq2 (thing $_107 skc12) true true true) true = true
% 0.71/0.89  |- ifeq2 (accessible_world $_107 skc9) true
% 0.71/0.89       (ifeq2 (thing $_107 skc14) true true true) true = true
% 0.71/0.89  |- ifeq2 (accessible_world $_107 skc9) true
% 0.71/0.89       (ifeq2 (thing $_107 skc15) true true true) true = true
% 0.71/0.89  |- ifeq2 (accessible_world $_107 skc9) true
% 0.71/0.89       (ifeq2 (thing $_107 skc16) true true true) true = true
% 0.71/0.89  |- ifeq2 (accessible_world $_107 skc9) true
% 0.71/0.89       (ifeq2 (thing $_107 skc17) true true true) true = true
% 0.71/0.89  |- ifeq2 (accessible_world skc14 $_108) true (thing $_108 skc10) true =
% 0.71/0.89     true
% 0.71/0.89  |- ifeq2 (accessible_world skc14 $_108) true (thing $_108 skc15) true =
% 0.71/0.89     true
% 0.71/0.89  |- ifeq2 (accessible_world skc9 $_108) true (thing $_108 skc10) true = true
% 0.71/0.89  |- ifeq2 (accessible_world skc9 $_108) true (thing $_108 skc11) true = true
% 0.71/0.89  |- ifeq2 (accessible_world skc9 $_108) true (thing $_108 skc12) true = true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_108) true (thing $_108 skc14) true = true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_108) true (thing $_108 skc15) true = true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_108) true (thing $_108 skc16) true = true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_108) true (thing $_108 skc17) true = true
% 0.73/0.89  |- ifeq2 (thing skc9 $_109) true (thing skc14 $_109) true = true
% 0.73/0.89  |- thing skc14 skc11 = true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $V) true (thing $V skc11) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.89       (ifeq2 (thing $U skc11) true true true) true = true
% 0.73/0.89  |- ifeq2 (abstraction skc14 skc11) true true true = true
% 0.73/0.89  |- singleton skc14 skc11 = true
% 0.73/0.89  |- ifeq2 (eventuality skc14 skc11) true true true = true
% 0.73/0.89  |- thing skc14 skc12 = true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $V) true (thing $V skc12) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.89       (ifeq2 (thing $U skc12) true true true) true = true
% 0.73/0.89  |- ifeq2 (entity skc14 skc12) true true true = true
% 0.73/0.89  |- singleton skc14 skc12 = true
% 0.73/0.89  |- ifeq2 (eventuality skc14 skc12) true true true = true
% 0.73/0.89  |- thing skc14 skc14 = true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $V) true (thing $V skc14) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.89       (ifeq2 (thing $U skc14) true true true) true = true
% 0.73/0.89  |- ifeq2 (entity skc14 skc14) true true true = true
% 0.73/0.89  |- singleton skc14 skc14 = true
% 0.73/0.89  |- ifeq2 (eventuality skc14 skc14) true true true = true
% 0.73/0.89  |- thing skc14 skc16 = true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $V) true (thing $V skc16) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.89       (ifeq2 (thing $U skc16) true true true) true = true
% 0.73/0.89  |- ifeq2 (entity skc14 skc16) true true true = true
% 0.73/0.89  |- singleton skc14 skc16 = true
% 0.73/0.89  |- ifeq2 (eventuality skc14 skc16) true true true = true
% 0.73/0.89  |- thing skc14 skc17 = true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $V) true (thing $V skc17) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.89       (ifeq2 (thing $U skc17) true true true) true = true
% 0.73/0.89  |- ifeq2 (abstraction skc14 skc17) true true true = true
% 0.73/0.89  |- singleton skc14 skc17 = true
% 0.73/0.89  |- ifeq2 (eventuality skc14 skc17) true true true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc14) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc10) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc14) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc11) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc14) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc12) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc14) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc14) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc14) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc15) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc14) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc16) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc14) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc17) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc9) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc10) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc9) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc11) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc9) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc12) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc9) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc14) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc9) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc15) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc9) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc16) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_136 skc9) true
% 0.73/0.89       (ifeq2 (singleton $_136 skc17) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $_137) true (singleton $_137 skc10) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $_137) true (singleton $_137 skc11) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $_137) true (singleton $_137 skc12) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $_137) true (singleton $_137 skc14) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $_137) true (singleton $_137 skc15) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $_137) true (singleton $_137 skc16) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $_137) true (singleton $_137 skc17) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_137) true (singleton $_137 skc10) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_137) true (singleton $_137 skc11) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_137) true (singleton $_137 skc12) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_137) true (singleton $_137 skc14) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_137) true (singleton $_137 skc15) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_137) true (singleton $_137 skc16) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_137) true (singleton $_137 skc17) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (singleton skc9 $_138) true (singleton skc14 $_138) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_168 skc14) true
% 0.73/0.89       (ifeq2 (specific $_168 skc10) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_168 skc14) true
% 0.73/0.89       (ifeq2 (specific $_168 skc15) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_168 skc9) true
% 0.73/0.89       (ifeq2 (specific $_168 skc10) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_168 skc9) true
% 0.73/0.89       (ifeq2 (specific $_168 skc11) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_168 skc9) true
% 0.73/0.89       (ifeq2 (specific $_168 skc15) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_168 skc9) true
% 0.73/0.89       (ifeq2 (specific $_168 skc17) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $_169) true (specific $_169 skc10) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $_169) true (specific $_169 skc15) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_169) true (specific $_169 skc10) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_169) true (specific $_169 skc11) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_169) true (specific $_169 skc15) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_169) true (specific $_169 skc17) true =
% 0.73/0.89     true
% 0.73/0.89  |- ifeq2 (specific skc9 $_170) true (specific skc14 $_170) true = true
% 0.73/0.89  |- specific skc14 skc11 = true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $V) true (specific $V skc11) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.89       (ifeq2 (specific $U skc11) true true true) true = true
% 0.73/0.89  |- ifeq (tuple true (general skc14 skc11)) (tuple true true) a b = b
% 0.73/0.89  |- specific skc14 skc17 = true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $V) true (specific $V skc17) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.89       (ifeq2 (specific $U skc17) true true true) true = true
% 0.73/0.89  |- ifeq (tuple true (general skc14 skc17)) (tuple true true) a b = b
% 0.73/0.89  |- ifeq2 (accessible_world $_188 skc14) true
% 0.73/0.89       (ifeq2 (nonexistent $_188 skc10) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_188 skc14) true
% 0.73/0.89       (ifeq2 (nonexistent $_188 skc15) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_188 skc9) true
% 0.73/0.89       (ifeq2 (nonexistent $_188 skc10) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world $_188 skc9) true
% 0.73/0.89       (ifeq2 (nonexistent $_188 skc15) true true true) true = true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $_189) true (nonexistent $_189 skc10)
% 0.73/0.89       true = true
% 0.73/0.89  |- ifeq2 (accessible_world skc14 $_189) true (nonexistent $_189 skc15)
% 0.73/0.89       true = true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_189) true (nonexistent $_189 skc10)
% 0.73/0.89       true = true
% 0.73/0.89  |- ifeq2 (accessible_world skc9 $_189) true (nonexistent $_189 skc15)
% 0.73/0.89       true = true
% 0.73/0.89  |- ifeq2 (nonexistent skc9 $_190) true (nonexistent skc14 $_190) true =
% 0.73/0.89     true
% 0.73/0.90  |- ifeq2 (accessible_world $_200 skc14) true
% 0.73/0.90       (ifeq2 (event $_200 skc10) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world $_200 skc9) true
% 0.73/0.90       (ifeq2 (event $_200 skc10) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world $_200 skc9) true
% 0.73/0.90       (ifeq2 (event $_200 skc15) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $_201) true (event $_201 skc10) true =
% 0.73/0.90     true
% 0.73/0.90  |- ifeq2 (accessible_world skc9 $_201) true (event $_201 skc10) true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc9 $_201) true (event $_201 skc15) true = true
% 0.73/0.90  |- ifeq2 (event skc9 $_202) true (event skc14 $_202) true = true
% 0.73/0.90  |- event skc14 skc15 = true
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $V) true (event $V skc15) true = true
% 0.73/0.90  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.90       (ifeq2 (event $U skc15) true true true) true = true
% 0.73/0.90  |- ifeq2 (smoke skc14 skc15) true true true = true
% 0.73/0.90  |- ifeq2 (accessible_world $_212 skc9) true
% 0.73/0.90       (ifeq2 (man $_212 skc11) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world $_212 skc9) true
% 0.73/0.90       (ifeq2 (man $_212 skc17) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc9 $_213) true (man $_213 skc11) true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc9 $_213) true (man $_213 skc17) true = true
% 0.73/0.90  |- ifeq2 (man skc9 $_214) true (man skc14 $_214) true = true
% 0.73/0.90  |- man skc14 skc11 = true
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $V) true (man $V skc11) true = true
% 0.73/0.90  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.90       (ifeq2 (man $U skc11) true true true) true = true
% 0.73/0.90  |- human_person skc14 skc11 = true
% 0.73/0.90  |- male skc14 skc11 = true
% 0.73/0.90  |- smoke skc14 (skf1 $V) = true
% 0.73/0.90  |- event skc14 (skf1 $V) = true
% 0.73/0.90  |- present skc14 (skf1 $V) = true
% 0.73/0.90  |- agent skc14 (skf1 skc11) skc11 = true
% 0.73/0.90  |- human skc14 skc11 = true
% 0.73/0.90  |- animate skc14 skc11 = true
% 0.73/0.90  |- organism skc14 skc11 = true
% 0.73/0.90  |- ifeq (tuple (unisex skc14 skc11) true) (tuple true true) a b = b
% 0.73/0.90  |- ifeq (tuple true (nonhuman skc14 skc11)) (tuple true true) a b = b
% 0.73/0.90  |- living skc14 skc11 = true
% 0.73/0.90  |- impartial skc14 skc11 = true
% 0.73/0.90  |- entity skc14 skc11 = true
% 0.73/0.90  |- existent skc14 skc11 = true
% 0.73/0.90  |- ifeq (tuple (nonexistent skc14 skc11) true) (tuple true true) a b = b
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $V) true (event $V (skf1 $_217)) true =
% 0.73/0.90     true
% 0.73/0.90  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.90       (ifeq2 (event $U (skf1 $_217)) true true true) true = true
% 0.73/0.90  |- eventuality skc14 (skf1 $_217) = true
% 0.73/0.90  |- ifeq2 (state skc14 (skf1 $_217)) true true true = true
% 0.73/0.90  |- ifeq2 (event skc9 (skf1 $_217)) true true true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $V) true (eventuality $V (skf1 $_218))
% 0.73/0.90       true = true
% 0.73/0.90  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.90       (ifeq2 (eventuality $U (skf1 $_218)) true true true) true = true
% 0.73/0.90  |- nonexistent skc14 (skf1 $_218) = true
% 0.73/0.90  |- specific skc14 (skf1 $_218) = true
% 0.73/0.90  |- unisex skc14 (skf1 $_218) = true
% 0.73/0.90  |- thing skc14 (skf1 $_218) = true
% 0.73/0.90  |- ifeq2 (eventuality skc9 (skf1 $_218)) true true true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $V) true (nonexistent $V (skf1 $_220))
% 0.73/0.90       true = true
% 0.73/0.90  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.90       (ifeq2 (nonexistent $U (skf1 $_220)) true true true) true = true
% 0.73/0.90  |- ifeq (tuple true (existent skc14 (skf1 $_220))) (tuple true true) a b =
% 0.73/0.90     b
% 0.73/0.90  |- ifeq2 (nonexistent skc9 (skf1 $_220)) true true true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $V) true (specific $V (skf1 $_221)) true =
% 0.73/0.90     true
% 0.73/0.90  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.90       (ifeq2 (specific $U (skf1 $_221)) true true true) true = true
% 0.73/0.90  |- ifeq (tuple true (general skc14 (skf1 $_221))) (tuple true true) a b = b
% 0.73/0.90  |- ifeq2 (entity skc14 (skf1 $_221)) true true true = true
% 0.73/0.90  |- ifeq2 (specific skc9 (skf1 $_221)) true true true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $V) true (thing $V (skf1 $_222)) true =
% 0.73/0.90     true
% 0.73/0.90  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.90       (ifeq2 (thing $U (skf1 $_222)) true true true) true = true
% 0.73/0.90  |- ifeq2 (abstraction skc14 (skf1 $_222)) true true true = true
% 0.73/0.90  |- singleton skc14 (skf1 $_222) = true
% 0.73/0.90  |- ifeq2 (thing skc9 (skf1 $_222)) true true true = true
% 0.73/0.90  |- man skc14 skc17 = true
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $V) true (man $V skc17) true = true
% 0.73/0.90  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.90       (ifeq2 (man $U skc17) true true true) true = true
% 0.73/0.90  |- human_person skc14 skc17 = true
% 0.73/0.90  |- male skc14 skc17 = true
% 0.73/0.90  |- agent skc14 (skf1 skc17) skc17 = true
% 0.73/0.90  |- human skc14 skc17 = true
% 0.73/0.90  |- animate skc14 skc17 = true
% 0.73/0.90  |- organism skc14 skc17 = true
% 0.73/0.90  |- ifeq (tuple (unisex skc14 skc17) true) (tuple true true) a b = b
% 0.73/0.90  |- ifeq (tuple true (nonhuman skc14 skc17)) (tuple true true) a b = b
% 0.73/0.90  |- living skc14 skc17 = true
% 0.73/0.90  |- impartial skc14 skc17 = true
% 0.73/0.90  |- entity skc14 skc17 = true
% 0.73/0.90  |- existent skc14 skc17 = true
% 0.73/0.90  |- ifeq (tuple (nonexistent skc14 skc17) true) (tuple true true) a b = b
% 0.73/0.90  |- ifeq (tuple true (male skc14 (skf1 $_225))) (tuple true true) a b = b
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $V) true (singleton $V (skf1 $_229))
% 0.73/0.90       true = true
% 0.73/0.90  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.90       (ifeq2 (singleton $U (skf1 $_229)) true true true) true = true
% 0.73/0.90  |- ifeq2 (singleton skc9 (skf1 $_229)) true true true = true
% 0.73/0.90  |- ifeq2 (accessible_world $_241 skc14) true
% 0.73/0.90       (ifeq2 (human_person $_241 skc11) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world $_241 skc14) true
% 0.73/0.90       (ifeq2 (human_person $_241 skc17) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world $_241 skc9) true
% 0.73/0.90       (ifeq2 (human_person $_241 skc11) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world $_241 skc9) true
% 0.73/0.90       (ifeq2 (human_person $_241 skc17) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $_242) true (human_person $_242 skc11)
% 0.73/0.90       true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $_242) true (human_person $_242 skc17)
% 0.73/0.90       true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc9 $_242) true (human_person $_242 skc11)
% 0.73/0.90       true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc9 $_242) true (human_person $_242 skc17)
% 0.73/0.90       true = true
% 0.73/0.90  |- ifeq2 (human_person skc9 $_243) true (human_person skc14 $_243) true =
% 0.73/0.90     true
% 0.73/0.90  |- ifeq2 (accessible_world $_253 skc14) true
% 0.73/0.90       (ifeq2 (organism $_253 skc11) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world $_253 skc14) true
% 0.73/0.90       (ifeq2 (organism $_253 skc17) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world $_253 skc9) true
% 0.73/0.90       (ifeq2 (organism $_253 skc11) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world $_253 skc9) true
% 0.73/0.90       (ifeq2 (organism $_253 skc17) true true true) true = true
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $_254) true (organism $_254 skc11) true =
% 0.73/0.90     true
% 0.73/0.90  |- ifeq2 (accessible_world skc14 $_254) true (organism $_254 skc17) true =
% 0.73/0.90     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_254) true (organism $_254 skc11) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_254) true (organism $_254 skc17) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (organism skc9 $_255) true (organism skc14 $_255) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_265 skc14) true
% 0.73/0.91       (ifeq2 (entity $_265 skc11) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_265 skc14) true
% 0.73/0.91       (ifeq2 (entity $_265 skc17) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_265 skc9) true
% 0.73/0.91       (ifeq2 (entity $_265 skc11) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_265 skc9) true
% 0.73/0.91       (ifeq2 (entity $_265 skc17) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_266) true (entity $_266 skc11) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_266) true (entity $_266 skc17) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_266) true (entity $_266 skc11) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_266) true (entity $_266 skc17) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (entity skc9 $_267) true (entity skc14 $_267) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_277 skc14) true
% 0.73/0.91       (ifeq2 (existent $_277 skc11) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_277 skc14) true
% 0.73/0.91       (ifeq2 (existent $_277 skc17) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_277 skc9) true
% 0.73/0.91       (ifeq2 (existent $_277 skc11) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_277 skc9) true
% 0.73/0.91       (ifeq2 (existent $_277 skc17) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_278) true (existent $_278 skc11) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_278) true (existent $_278 skc17) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_278) true (existent $_278 skc11) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_278) true (existent $_278 skc17) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (existent skc9 $_279) true (existent skc14 $_279) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_289 skc14) true
% 0.73/0.91       (ifeq2 (impartial $_289 skc11) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_289 skc14) true
% 0.73/0.91       (ifeq2 (impartial $_289 skc17) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_289 skc9) true
% 0.73/0.91       (ifeq2 (impartial $_289 skc11) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_289 skc9) true
% 0.73/0.91       (ifeq2 (impartial $_289 skc17) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_290) true (impartial $_290 skc11) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_290) true (impartial $_290 skc17) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_290) true (impartial $_290 skc11) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_290) true (impartial $_290 skc17) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (impartial skc9 $_291) true (impartial skc14 $_291) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_301 skc14) true
% 0.73/0.91       (ifeq2 (human $_301 skc11) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_301 skc14) true
% 0.73/0.91       (ifeq2 (human $_301 skc17) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_301 skc9) true
% 0.73/0.91       (ifeq2 (human $_301 skc11) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_301 skc9) true
% 0.73/0.91       (ifeq2 (human $_301 skc17) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_302) true (human $_302 skc11) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_302) true (human $_302 skc17) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_302) true (human $_302 skc11) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_302) true (human $_302 skc17) true = true
% 0.73/0.91  |- ifeq2 (human skc9 $_303) true (human skc14 $_303) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_313 skc14) true
% 0.73/0.91       (ifeq2 (animate $_313 skc11) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_313 skc14) true
% 0.73/0.91       (ifeq2 (animate $_313 skc17) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_313 skc9) true
% 0.73/0.91       (ifeq2 (animate $_313 skc11) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_313 skc9) true
% 0.73/0.91       (ifeq2 (animate $_313 skc17) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_314) true (animate $_314 skc11) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_314) true (animate $_314 skc17) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_314) true (animate $_314 skc11) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_314) true (animate $_314 skc17) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (animate skc9 $_315) true (animate skc14 $_315) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_325 skc14) true
% 0.73/0.91       (ifeq2 (male $_325 skc11) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_325 skc14) true
% 0.73/0.91       (ifeq2 (male $_325 skc17) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_325 skc9) true
% 0.73/0.91       (ifeq2 (male $_325 skc11) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_325 skc9) true
% 0.73/0.91       (ifeq2 (male $_325 skc17) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_326) true (male $_326 skc11) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_326) true (male $_326 skc17) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_326) true (male $_326 skc11) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_326) true (male $_326 skc17) true = true
% 0.73/0.91  |- ifeq2 (male skc9 $_327) true (male skc14 $_327) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_337 skc9) true
% 0.73/0.91       (ifeq2 (forename $_337 skc12) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_337 skc9) true
% 0.73/0.91       (ifeq2 (forename $_337 skc16) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_338) true (forename $_338 skc12) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_338) true (forename $_338 skc16) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (forename skc9 $_339) true (forename skc14 $_339) true = true
% 0.73/0.91  |- forename skc14 skc12 = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $V) true (forename $V skc12) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.91       (ifeq2 (forename $U skc12) true true true) true = true
% 0.73/0.91  |- relname skc14 skc12 = true
% 0.73/0.91  |- ifeq2 (vincent_forename skc14 skc12) true true true = true
% 0.73/0.91  |- relation skc14 skc12 = true
% 0.73/0.91  |- ifeq2 (proposition skc14 skc12) true true true = true
% 0.73/0.91  |- abstraction skc14 skc12 = true
% 0.73/0.91  |- general skc14 skc12 = true
% 0.73/0.91  |- nonhuman skc14 skc12 = true
% 0.73/0.91  |- unisex skc14 skc12 = true
% 0.73/0.91  |- ifeq (tuple (specific skc14 skc12) true) (tuple true true) a b = b
% 0.73/0.91  |- ifeq (tuple (human skc14 skc12) true) (tuple true true) a b = b
% 0.73/0.91  |- ifeq (tuple true (male skc14 skc12)) (tuple true true) a b = b
% 0.73/0.91  |- forename skc14 skc16 = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $V) true (forename $V skc16) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.91       (ifeq2 (forename $U skc16) true true true) true = true
% 0.73/0.91  |- relname skc14 skc16 = true
% 0.73/0.91  |- ifeq2 (jules_forename skc14 skc16) true true true = true
% 0.73/0.91  |- relation skc14 skc16 = true
% 0.73/0.91  |- ifeq2 (proposition skc14 skc16) true true true = true
% 0.73/0.91  |- abstraction skc14 skc16 = true
% 0.73/0.91  |- general skc14 skc16 = true
% 0.73/0.91  |- nonhuman skc14 skc16 = true
% 0.73/0.91  |- unisex skc14 skc16 = true
% 0.73/0.91  |- ifeq (tuple (human skc14 skc16) true) (tuple true true) a b = b
% 0.73/0.91  |- ifeq (tuple (specific skc14 skc16) true) (tuple true true) a b = b
% 0.73/0.91  |- ifeq (tuple true (male skc14 skc16)) (tuple true true) a b = b
% 0.73/0.91  |- ifeq2 (accessible_world $_349 skc14) true
% 0.73/0.91       (ifeq2 (relname $_349 skc12) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_349 skc14) true
% 0.73/0.91       (ifeq2 (relname $_349 skc16) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_349 skc9) true
% 0.73/0.91       (ifeq2 (relname $_349 skc12) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_349 skc9) true
% 0.73/0.91       (ifeq2 (relname $_349 skc16) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_350) true (relname $_350 skc12) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_350) true (relname $_350 skc16) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_350) true (relname $_350 skc12) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_350) true (relname $_350 skc16) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (relname skc9 $_351) true (relname skc14 $_351) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_361 skc14) true
% 0.73/0.91       (ifeq2 (relation $_361 skc12) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_361 skc14) true
% 0.73/0.91       (ifeq2 (relation $_361 skc16) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_361 skc9) true
% 0.73/0.91       (ifeq2 (relation $_361 skc12) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_361 skc9) true
% 0.73/0.91       (ifeq2 (relation $_361 skc14) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_361 skc9) true
% 0.73/0.91       (ifeq2 (relation $_361 skc16) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_362) true (relation $_362 skc12) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_362) true (relation $_362 skc16) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_362) true (relation $_362 skc12) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_362) true (relation $_362 skc14) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_362) true (relation $_362 skc16) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (relation skc9 $_363) true (relation skc14 $_363) true = true
% 0.73/0.91  |- relation skc14 skc14 = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $V) true (relation $V skc14) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.91       (ifeq2 (relation $U skc14) true true true) true = true
% 0.73/0.91  |- ifeq2 (relname skc14 skc14) true true true = true
% 0.73/0.91  |- abstraction skc14 skc14 = true
% 0.73/0.91  |- general skc14 skc14 = true
% 0.73/0.91  |- nonhuman skc14 skc14 = true
% 0.73/0.91  |- unisex skc14 skc14 = true
% 0.73/0.91  |- ifeq (tuple (human skc14 skc14) true) (tuple true true) a b = b
% 0.73/0.91  |- ifeq (tuple (specific skc14 skc14) true) (tuple true true) a b = b
% 0.73/0.91  |- ifeq (tuple true (male skc14 skc14)) (tuple true true) a b = b
% 0.73/0.91  |- ifeq2 (accessible_world $_377 skc14) true
% 0.73/0.91       (ifeq2 (abstraction $_377 skc12) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_377 skc14) true
% 0.73/0.91       (ifeq2 (abstraction $_377 skc14) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_377 skc14) true
% 0.73/0.91       (ifeq2 (abstraction $_377 skc16) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_377 skc9) true
% 0.73/0.91       (ifeq2 (abstraction $_377 skc12) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_377 skc9) true
% 0.73/0.91       (ifeq2 (abstraction $_377 skc14) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_377 skc9) true
% 0.73/0.91       (ifeq2 (abstraction $_377 skc16) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_378) true (abstraction $_378 skc12)
% 0.73/0.91       true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_378) true (abstraction $_378 skc14)
% 0.73/0.91       true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_378) true (abstraction $_378 skc16)
% 0.73/0.91       true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_378) true (abstraction $_378 skc12)
% 0.73/0.91       true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_378) true (abstraction $_378 skc14)
% 0.73/0.91       true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_378) true (abstraction $_378 skc16)
% 0.73/0.91       true = true
% 0.73/0.91  |- ifeq2 (abstraction skc9 $_379) true (abstraction skc14 $_379) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world $_393 skc14) true
% 0.73/0.91       (ifeq2 (general $_393 skc12) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_393 skc14) true
% 0.73/0.91       (ifeq2 (general $_393 skc14) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_393 skc14) true
% 0.73/0.91       (ifeq2 (general $_393 skc16) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_393 skc9) true
% 0.73/0.91       (ifeq2 (general $_393 skc12) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_393 skc9) true
% 0.73/0.91       (ifeq2 (general $_393 skc14) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_393 skc9) true
% 0.73/0.91       (ifeq2 (general $_393 skc16) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_394) true (general $_394 skc12) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_394) true (general $_394 skc14) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc14 $_394) true (general $_394 skc16) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_394) true (general $_394 skc12) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_394) true (general $_394 skc14) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_394) true (general $_394 skc16) true =
% 0.73/0.91     true
% 0.73/0.91  |- ifeq2 (general skc9 $_395) true (general skc14 $_395) true = true
% 0.73/0.91  |- ifeq2 (accessible_world $_409 skc9) true
% 0.73/0.91       (ifeq2 (jules_forename $_409 skc12) true true true) true = true
% 0.73/0.91  |- ifeq2 (accessible_world skc9 $_410) true (jules_forename $_410 skc12)
% 0.73/0.91       true = true
% 0.73/0.91  |- ifeq2 (jules_forename skc9 $_411) true (jules_forename skc14 $_411)
% 0.73/0.91       true = true
% 0.73/0.91  |- jules_forename skc14 skc12 = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $V) true (jules_forename $V skc12) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.92       (ifeq2 (jules_forename $U skc12) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_417 skc14) true
% 0.73/0.92       (ifeq2 (smoke $_417 (skf1 $V)) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $_418) true (smoke $_418 (skf1 $V)) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (smoke skc9 $_419) true (smoke skc14 $_419) true = true
% 0.73/0.92  |- ifeq2 (smoke skc9 (skf1 $V)) true true true = true
% 0.73/0.92  |- ifeq2 (present $_426 (skf1 $V)) true
% 0.73/0.92       (ifeq2 (accessible_world $_426 skc14) true true true) true = true
% 0.73/0.92  |- ifeq2 (present $_426 skc15) true
% 0.73/0.92       (ifeq2 (accessible_world $_426 skc9) true true true) true = true
% 0.73/0.92  |- ifeq2 (present skc9 $_428) true (present skc14 $_428) true = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $_427) true (present $_427 (skf1 $V))
% 0.73/0.92       true = true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_427) true (present $_427 skc15) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (present skc9 (skf1 $V)) true true true = true
% 0.73/0.92  |- present skc14 skc15 = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $V) true (present $V skc15) true = true
% 0.73/0.92  |- ifeq2 (present $U skc15) true
% 0.73/0.92       (ifeq2 (accessible_world $U skc14) true true true) true = true
% 0.73/0.92  |- ifeq2 (think_believe_consider $_437 skc15) true
% 0.73/0.92       (ifeq2 (accessible_world $_437 skc9) true true true) true = true
% 0.73/0.92  |- ifeq2 (think_believe_consider skc9 $_439) true
% 0.73/0.92       (think_believe_consider skc14 $_439) true = true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_438) true
% 0.73/0.92       (think_believe_consider $_438 skc15) true = true
% 0.73/0.92  |- think_believe_consider skc14 skc15 = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $V) true (think_believe_consider $V skc15)
% 0.73/0.92       true = true
% 0.73/0.92  |- ifeq2 (think_believe_consider $U skc15) true
% 0.73/0.92       (ifeq2 (accessible_world $U skc14) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_445 skc9) true
% 0.73/0.92       (ifeq2 (proposition $_445 skc14) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_446) true (proposition $_446 skc14)
% 0.73/0.92       true = true
% 0.73/0.92  |- ifeq2 (proposition skc9 $_447) true (proposition skc14 $_447) true =
% 0.73/0.92     true
% 0.73/0.92  |- proposition skc14 skc14 = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $V) true (proposition $V skc14) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.92       (ifeq2 (proposition $U skc14) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_453 skc9) true
% 0.73/0.92       (ifeq2 (vincent_forename $_453 skc16) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_454) true (vincent_forename $_454 skc16)
% 0.73/0.92       true = true
% 0.73/0.92  |- ifeq2 (vincent_forename skc9 $_455) true (vincent_forename skc14 $_455)
% 0.73/0.92       true = true
% 0.73/0.92  |- vincent_forename skc14 skc16 = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $V) true (vincent_forename $V skc16)
% 0.73/0.92       true = true
% 0.73/0.92  |- ifeq2 (accessible_world $U skc14) true
% 0.73/0.92       (ifeq2 (vincent_forename $U skc16) true true true) true = true
% 0.73/0.92  |- ifeq2 (of $_474 skc12 skc11) true
% 0.73/0.92       (ifeq2 (accessible_world $_474 skc9) true true true) true = true
% 0.73/0.92  |- ifeq2 (of $_474 skc16 skc17) true
% 0.73/0.92       (ifeq2 (accessible_world $_474 skc9) true true true) true = true
% 0.73/0.92  |- ifeq2 (of skc9 $_476 $_477) true (of skc14 $_476 $_477) true = true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_475) true (of $_475 skc12 skc11) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_475) true (of $_475 skc16 skc17) true =
% 0.73/0.92     true
% 0.73/0.92  |- of skc14 skc12 skc11 = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $V) true (of $V skc12 skc11) true = true
% 0.73/0.92  |- ifeq2 (of $U skc12 skc11) true
% 0.73/0.92       (ifeq2 (accessible_world $U skc14) true true true) true = true
% 0.73/0.92  |- of skc14 skc16 skc17 = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $V) true (of $V skc16 skc17) true = true
% 0.73/0.92  |- ifeq2 (of $U skc16 skc17) true
% 0.73/0.92       (ifeq2 (accessible_world $U skc14) true true true) true = true
% 0.73/0.92  |- ifeq2 (agent $_488 (skf1 skc11) skc11) true
% 0.73/0.92       (ifeq2 (accessible_world $_488 skc14) true true true) true = true
% 0.73/0.92  |- ifeq2 (agent $_488 (skf1 skc17) skc17) true
% 0.73/0.92       (ifeq2 (accessible_world $_488 skc14) true true true) true = true
% 0.73/0.92  |- ifeq2 (agent $_488 skc15 skc17) true
% 0.73/0.92       (ifeq2 (accessible_world $_488 skc9) true true true) true = true
% 0.73/0.92  |- ifeq2 (agent skc9 $_490 $_491) true (agent skc14 $_490 $_491) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $_489) true
% 0.73/0.92       (agent $_489 (skf1 skc11) skc11) true = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $_489) true
% 0.73/0.92       (agent $_489 (skf1 skc17) skc17) true = true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_489) true (agent $_489 skc15 skc17)
% 0.73/0.92       true = true
% 0.73/0.92  |- agent skc14 skc15 skc17 = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $V) true (agent $V skc15 skc17) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (agent $U skc15 skc17) true
% 0.73/0.92       (ifeq2 (accessible_world $U skc14) true true true) true = true
% 0.73/0.92  |- ifeq2 (agent skc9 (skf1 skc11) skc11) true true true = true
% 0.73/0.92  |- ifeq2 (agent skc9 (skf1 skc17) skc17) true true true = true
% 0.73/0.92  |- ifeq2 (theme $_502 skc15 skc14) true
% 0.73/0.92       (ifeq2 (accessible_world $_502 skc9) true true true) true = true
% 0.73/0.92  |- ifeq2 (theme skc9 $_504 $_505) true (theme skc14 $_504 $_505) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_503) true (theme $_503 skc15 skc14)
% 0.73/0.92       true = true
% 0.73/0.92  |- theme skc14 skc15 skc14 = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $V) true (theme $V skc15 skc14) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (theme $U skc15 skc14) true
% 0.73/0.92       (ifeq2 (accessible_world $U skc14) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_526 skc14) true
% 0.73/0.92       (ifeq2 (unisex $_526 skc10) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_526 skc14) true
% 0.73/0.92       (ifeq2 (unisex $_526 skc12) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_526 skc14) true
% 0.73/0.92       (ifeq2 (unisex $_526 skc14) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_526 skc14) true
% 0.73/0.92       (ifeq2 (unisex $_526 skc15) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_526 skc14) true
% 0.73/0.92       (ifeq2 (unisex $_526 skc16) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_526 skc14) true
% 0.73/0.92       (ifeq2 (unisex $_526 (skf1 $_218)) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_526 skc9) true
% 0.73/0.92       (ifeq2 (unisex $_526 skc10) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_526 skc9) true
% 0.73/0.92       (ifeq2 (unisex $_526 skc12) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_526 skc9) true
% 0.73/0.92       (ifeq2 (unisex $_526 skc14) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_526 skc9) true
% 0.73/0.92       (ifeq2 (unisex $_526 skc15) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_526 skc9) true
% 0.73/0.92       (ifeq2 (unisex $_526 skc16) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $_527) true (unisex $_527 skc10) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $_527) true (unisex $_527 skc12) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $_527) true (unisex $_527 skc14) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $_527) true (unisex $_527 skc15) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $_527) true (unisex $_527 skc16) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $_527) true (unisex $_527 (skf1 $_218))
% 0.73/0.92       true = true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_527) true (unisex $_527 skc10) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_527) true (unisex $_527 skc12) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_527) true (unisex $_527 skc14) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_527) true (unisex $_527 skc15) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_527) true (unisex $_527 skc16) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (unisex skc9 $_528) true (unisex skc14 $_528) true = true
% 0.73/0.92  |- ifeq2 (unisex skc9 (skf1 $_218)) true true true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_555 skc14) true
% 0.73/0.92       (ifeq2 (living $_555 skc11) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_555 skc14) true
% 0.73/0.92       (ifeq2 (living $_555 skc17) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_555 skc9) true
% 0.73/0.92       (ifeq2 (living $_555 skc11) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_555 skc9) true
% 0.73/0.92       (ifeq2 (living $_555 skc17) true true true) true = true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $_556) true (living $_556 skc11) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc14 $_556) true (living $_556 skc17) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_556) true (living $_556 skc11) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (accessible_world skc9 $_556) true (living $_556 skc17) true =
% 0.73/0.92     true
% 0.73/0.92  |- ifeq2 (living skc9 $_557) true (living skc14 $_557) true = true
% 0.73/0.92  |- ifeq2 (accessible_world $_567 skc14) true
% 0.73/0.92       (ifeq2 (nonhuman $_567 skc12) true true true) true = true
% 0.76/0.92  |- ifeq2 (accessible_world $_567 skc14) true
% 0.76/0.92       (ifeq2 (nonhuman $_567 skc14) true true true) true = true
% 0.76/0.92  |- ifeq2 (accessible_world $_567 skc14) true
% 0.76/0.92       (ifeq2 (nonhuman $_567 skc16) true true true) true = true
% 0.76/0.92  |- ifeq2 (accessible_world $_567 skc9) true
% 0.76/0.92       (ifeq2 (nonhuman $_567 skc12) true true true) true = true
% 0.76/0.92  |- ifeq2 (accessible_world $_567 skc9) true
% 0.76/0.92       (ifeq2 (nonhuman $_567 skc14) true true true) true = true
% 0.76/0.92  |- ifeq2 (accessible_world $_567 skc9) true
% 0.76/0.92       (ifeq2 (nonhuman $_567 skc16) true true true) true = true
% 0.76/0.92  |- ifeq2 (accessible_world skc14 $_568) true (nonhuman $_568 skc12) true =
% 0.76/0.92     true
% 0.76/0.92  |- ifeq2 (accessible_world skc14 $_568) true (nonhuman $_568 skc14) true =
% 0.76/0.92     true
% 0.76/0.92  |- ifeq2 (accessible_world skc14 $_568) true (nonhuman $_568 skc16) true =
% 0.76/0.92     true
% 0.76/0.92  |- ifeq2 (accessible_world skc9 $_568) true (nonhuman $_568 skc12) true =
% 0.76/0.92     true
% 0.76/0.92  |- ifeq2 (accessible_world skc9 $_568) true (nonhuman $_568 skc14) true =
% 0.76/0.92     true
% 0.76/0.92  |- ifeq2 (accessible_world skc9 $_568) true (nonhuman $_568 skc16) true =
% 0.76/0.92     true
% 0.76/0.92  |- ifeq2 (nonhuman skc9 $_569) true (nonhuman skc14 $_569) true = true
% 0.76/0.92  |- ifeq2 (be $_589 skc10 skc11 skc11) true
% 0.76/0.92       (ifeq2 (accessible_world $_589 skc9) true true true) true = true
% 0.76/0.92  |- ifeq2 (be skc9 $_591 $_592 $_593) true (be skc14 $_591 $_592 $_593)
% 0.76/0.92       true = true
% 0.76/0.92  |- ifeq2 (accessible_world skc9 $_590) true (be $_590 skc10 skc11 skc11)
% 0.76/0.92       true = true
% 0.76/0.92  |- be skc14 skc10 skc11 skc11 = true
% 0.76/0.92  |- ifeq2 (accessible_world skc14 $V) true (be $V skc10 skc11 skc11) true =
% 0.76/0.92     true
% 0.76/0.92  |- ifeq2 (be $U skc10 skc11 skc11) true
% 0.76/0.92       (ifeq2 (accessible_world $U skc14) true true true) true = true
% 0.76/0.92  |- ifeq3 (of skc14 $_603 skc11) true
% 0.76/0.92       (ifeq3 (of skc14 $_602 skc11) true
% 0.76/0.92          (ifeq3 (forename skc14 $_603) true
% 0.76/0.92             (ifeq3 (forename skc14 $_602) true $_603 $_602) $_602) $_602)
% 0.76/0.92       $_602 = $_602
% 0.76/0.92  |- ifeq3 (of skc14 $_603 skc17) true
% 0.76/0.92       (ifeq3 (of skc14 $_602 skc17) true
% 0.76/0.92          (ifeq3 (forename skc14 $_603) true
% 0.76/0.92             (ifeq3 (forename skc14 $_602) true $_603 $_602) $_602) $_602)
% 0.76/0.92       $_602 = $_602
% 0.76/0.92  |- ifeq3 (of skc9 $_603 skc11) true
% 0.76/0.92       (ifeq3 (of skc9 $_602 skc11) true
% 0.76/0.92          (ifeq3 (forename skc9 $_603) true
% 0.76/0.92             (ifeq3 (forename skc9 $_602) true $_603 $_602) $_602) $_602)
% 0.76/0.92       $_602 = $_602
% 0.76/0.92  |- ifeq3 (of skc9 $_603 skc17) true
% 0.76/0.92       (ifeq3 (of skc9 $_602 skc17) true
% 0.76/0.92          (ifeq3 (forename skc9 $_603) true
% 0.76/0.92             (ifeq3 (forename skc9 $_602) true $_603 $_602) $_602) $_602)
% 0.76/0.92       $_602 = $_602
% 0.76/0.92  |- ifeq3 (of skc14 $_603 $_604) true
% 0.76/0.92       (ifeq3 (of skc14 skc12 $_604) true
% 0.76/0.92          (ifeq3 (forename skc14 $_603) true
% 0.76/0.92             (ifeq3 (entity skc14 $_604) true $_603 skc12) skc12) skc12)
% 0.76/0.92       skc12 = skc12
% 0.76/0.92  |- ifeq3 (of skc14 $_603 $_604) true
% 0.76/0.92       (ifeq3 (of skc14 skc16 $_604) true
% 0.76/0.92          (ifeq3 (forename skc14 $_603) true
% 0.76/0.92             (ifeq3 (entity skc14 $_604) true $_603 skc16) skc16) skc16)
% 0.76/0.92       skc16 = skc16
% 0.76/0.92  |- ifeq3 (of skc9 $_603 $_604) true
% 0.76/0.92       (ifeq3 (of skc9 skc12 $_604) true
% 0.76/0.92          (ifeq3 (forename skc9 $_603) true
% 0.76/0.92             (ifeq3 (entity skc9 $_604) true $_603 skc12) skc12) skc12)
% 0.76/0.92       skc12 = skc12
% 0.76/0.92  |- ifeq3 (of skc9 $_603 $_604) true
% 0.76/0.92       (ifeq3 (of skc9 skc16 $_604) true
% 0.76/0.92          (ifeq3 (forename skc9 $_603) true
% 0.76/0.92             (ifeq3 (entity skc9 $_604) true $_603 skc16) skc16) skc16)
% 0.76/0.92       skc16 = skc16
% 0.76/0.92  |- ifeq3 (of skc14 skc12 $_604) true
% 0.76/0.92       (ifeq3 (of skc14 $_602 $_604) true
% 0.76/0.92          (ifeq3 (forename skc14 $_602) true
% 0.76/0.92             (ifeq3 (entity skc14 $_604) true skc12 $_602) $_602) $_602)
% 0.76/0.92       $_602 = $_602
% 0.76/0.92  |- ifeq3 (of skc14 skc16 $_604) true
% 0.76/0.92       (ifeq3 (of skc14 $_602 $_604) true
% 0.76/0.92          (ifeq3 (forename skc14 $_602) true
% 0.76/0.92             (ifeq3 (entity skc14 $_604) true skc16 $_602) $_602) $_602)
% 0.76/0.92       $_602 = $_602
% 0.76/0.92  |- ifeq3 (of skc9 skc12 $_604) true
% 0.76/0.92       (ifeq3 (of skc9 $_602 $_604) true
% 0.76/0.92          (ifeq3 (forename skc9 $_602) true
% 0.76/0.92             (ifeq3 (entity skc9 $_604) true skc12 $_602) $_602) $_602)
% 0.76/0.92       $_602 = $_602
% 0.76/0.92  |- ifeq3 (of skc9 skc16 $_604) true
% 0.76/0.92       (ifeq3 (of skc9 $_602 $_604) true
% 0.76/0.92          (ifeq3 (forename skc9 $_602) true
% 0.76/0.92             (ifeq3 (entity skc9 $_604) true skc16 $_602) $_602) $_602)
% 0.76/0.92       $_602 = $_602
% 0.76/0.92  |- ifeq3 (of skc14 $_603 skc11) true
% 0.76/0.92       (ifeq3 (forename skc14 $_603) true $_603 skc12) skc12 = skc12
% 0.76/0.92  |- ifeq3 (of skc14 $_603 skc17) true
% 0.76/0.92       (ifeq3 (forename skc14 $_603) true $_603 skc16) skc16 = skc16
% 0.76/0.92  |- ifeq3 (of skc9 $_603 skc11) true
% 0.76/0.92       (ifeq3 (forename skc9 $_603) true $_603 skc12) skc12 = skc12
% 0.76/0.92  |- ifeq3 (of skc9 $_603 skc17) true
% 0.76/0.92       (ifeq3 (forename skc9 $_603) true $_603 skc16) skc16 = skc16
% 0.76/0.92  |- ifeq3 (of skc14 $_602 skc11) true
% 0.76/0.92       (ifeq3 (forename skc14 $_602) true skc12 $_602) $_602 = $_602
% 0.76/0.92  |- ifeq3 (of skc14 $_602 skc17) true
% 0.76/0.92       (ifeq3 (forename skc14 $_602) true skc16 $_602) $_602 = $_602
% 0.76/0.92  |- ifeq3 (of skc9 $_602 skc11) true
% 0.76/0.92       (ifeq3 (forename skc9 $_602) true skc12 $_602) $_602 = $_602
% 0.76/0.92  |- ifeq3 (of skc9 $_602 skc17) true
% 0.76/0.92       (ifeq3 (forename skc9 $_602) true skc16 $_602) $_602 = $_602
% 0.76/0.92  |- ifeq3 (of skc14 skc16 skc11) true skc16 skc12 = skc12
% 0.76/0.92  |- ifeq3 (of skc9 skc16 skc11) true skc16 skc12 = skc12
% 0.76/0.92  |- ifeq3 (of skc14 skc16 skc11) true skc12 skc16 = skc16
% 0.76/0.92  |- ifeq3 (of skc14 skc12 skc17) true skc16 skc12 = skc12
% 0.76/0.92  |- ifeq3 (of skc9 skc16 skc11) true skc12 skc16 = skc16
% 0.76/0.93  |- ifeq3 (of skc9 skc12 skc17) true skc16 skc12 = skc12
% 0.76/0.93  |- ifeq3 (of skc14 skc12 skc17) true skc12 skc16 = skc16
% 0.76/0.93  |- ifeq3 (of skc9 skc12 skc17) true skc12 skc16 = skc16
% 0.76/0.93  |- ifeq3 (of skc14 $_614 skc11) true
% 0.76/0.93       (ifeq3 (of skc14 skc16 skc11) true
% 0.76/0.93          (ifeq3 (forename skc14 $_614) true $_614 skc16) skc16) skc16 =
% 0.76/0.93     skc16
% 0.76/0.93  |- ifeq3 (of skc14 skc16 skc11) true
% 0.76/0.93       (ifeq3 (of skc14 $_613 skc11) true
% 0.76/0.93          (ifeq3 (forename skc14 $_613) true skc16 $_613) $_613) $_613 =
% 0.76/0.93     $_613
% 0.76/0.93  |- ifeq3 (of skc14 skc16 skc11) true
% 0.76/0.93       (ifeq3 (of skc14 skc16 skc11) true skc16 skc16) skc16 = skc16
% 0.76/0.93  |- ifeq3 (of skc14 $_618 skc17) true
% 0.76/0.93       (ifeq3 (of skc14 skc12 skc17) true
% 0.76/0.93          (ifeq3 (forename skc14 $_618) true $_618 skc12) skc12) skc12 =
% 0.76/0.93     skc12
% 0.76/0.93  |- ifeq3 (of skc14 skc12 skc17) true
% 0.76/0.93       (ifeq3 (of skc14 $_617 skc17) true
% 0.76/0.93          (ifeq3 (forename skc14 $_617) true skc12 $_617) $_617) $_617 =
% 0.76/0.93     $_617
% 0.76/0.93  |- ifeq3 (of skc14 skc12 skc17) true
% 0.76/0.93       (ifeq3 (of skc14 skc12 skc17) true skc12 skc12) skc12 = skc12
% 0.76/0.93  |- ifeq3 (of skc9 $_622 skc11) true
% 0.76/0.93       (ifeq3 (of skc9 skc16 skc11) true
% 0.76/0.93          (ifeq3 (forename skc9 $_622) true $_622 skc16) skc16) skc16 = skc16
% 0.76/0.93  |- ifeq3 (of skc9 skc16 skc11) true
% 0.76/0.93       (ifeq3 (of skc9 $_621 skc11) true
% 0.76/0.93          (ifeq3 (forename skc9 $_621) true skc16 $_621) $_621) $_621 = $_621
% 0.76/0.93  |- ifeq3 (of skc9 skc16 skc11) true
% 0.76/0.93       (ifeq3 (of skc9 skc16 skc11) true skc16 skc16) skc16 = skc16
% 0.76/0.93  |- ifeq3 (of skc9 $_626 skc17) true
% 0.76/0.93       (ifeq3 (of skc9 skc12 skc17) true
% 0.76/0.93          (ifeq3 (forename skc9 $_626) true $_626 skc12) skc12) skc12 = skc12
% 0.76/0.93  |- ifeq3 (of skc9 skc12 skc17) true
% 0.76/0.93       (ifeq3 (of skc9 $_625 skc17) true
% 0.76/0.93          (ifeq3 (forename skc9 $_625) true skc12 $_625) $_625) $_625 = $_625
% 0.76/0.93  |- ifeq3 (of skc9 skc12 skc17) true
% 0.76/0.93       (ifeq3 (of skc9 skc12 skc17) true skc12 skc12) skc12 = skc12
% 0.76/0.93  |- ifeq3 (of skc14 skc12 $_630) true
% 0.76/0.93       (ifeq3 (of skc14 skc12 $_630) true
% 0.76/0.93          (ifeq3 (entity skc14 $_630) true skc12 skc12) skc12) skc12 = skc12
% 0.76/0.93  |- ifeq3 (of skc14 skc16 $_630) true
% 0.76/0.93       (ifeq3 (of skc14 skc12 $_630) true
% 0.76/0.93          (ifeq3 (entity skc14 $_630) true skc16 skc12) skc12) skc12 = skc12
% 0.76/0.93  |- ifeq3 (of skc14 skc12 $_634) true
% 0.76/0.93       (ifeq3 (of skc14 skc16 $_634) true
% 0.76/0.93          (ifeq3 (entity skc14 $_634) true skc12 skc16) skc16) skc16 = skc16
% 0.76/0.93  |- ifeq3 (of skc14 skc16 $_634) true
% 0.76/0.93       (ifeq3 (of skc14 skc16 $_634) true
% 0.76/0.93          (ifeq3 (entity skc14 $_634) true skc16 skc16) skc16) skc16 = skc16
% 0.76/0.93  |- ifeq3 (of skc9 skc12 $_638) true
% 0.76/0.93       (ifeq3 (of skc9 skc12 $_638) true
% 0.76/0.93          (ifeq3 (entity skc9 $_638) true skc12 skc12) skc12) skc12 = skc12
% 0.76/0.93  |- ifeq3 (of skc9 skc16 $_638) true
% 0.76/0.93       (ifeq3 (of skc9 skc12 $_638) true
% 0.76/0.93          (ifeq3 (entity skc9 $_638) true skc16 skc12) skc12) skc12 = skc12
% 0.76/0.93  |- ifeq3 (of skc9 skc12 $_642) true
% 0.76/0.93       (ifeq3 (of skc9 skc16 $_642) true
% 0.76/0.93          (ifeq3 (entity skc9 $_642) true skc12 skc16) skc16) skc16 = skc16
% 0.76/0.93  |- ifeq3 (of skc9 skc16 $_642) true
% 0.76/0.93       (ifeq3 (of skc9 skc16 $_642) true
% 0.76/0.93          (ifeq3 (entity skc9 $_642) true skc16 skc16) skc16) skc16 = skc16
% 0.76/0.93  |- ifeq3 (theme skc14 $_659 $_657) true
% 0.76/0.93       (ifeq3 (theme skc14 $_658 skc14) true
% 0.76/0.93          (ifeq3 (agent skc14 $_659 $_660) true
% 0.76/0.93             (ifeq3 (agent skc14 $_658 $_660) true
% 0.76/0.93                (ifeq3 (think_believe_consider skc14 $_659) true
% 0.76/0.93                   (ifeq3 (think_believe_consider skc14 $_658) true
% 0.76/0.93                      (ifeq3 (proposition skc14 $_657) true skc14 $_657)
% 0.76/0.93                      $_657) $_657) $_657) $_657) $_657) $_657 = $_657
% 0.76/0.93  |- ifeq3 (theme skc9 $_659 $_657) true
% 0.76/0.93       (ifeq3 (theme skc9 $_658 skc14) true
% 0.76/0.93          (ifeq3 (agent skc9 $_659 $_660) true
% 0.76/0.93             (ifeq3 (agent skc9 $_658 $_660) true
% 0.76/0.93                (ifeq3 (think_believe_consider skc9 $_659) true
% 0.76/0.93                   (ifeq3 (think_believe_consider skc9 $_658) true
% 0.76/0.93                      (ifeq3 (proposition skc9 $_657) true skc14 $_657)
% 0.76/0.93                      $_657) $_657) $_657) $_657) $_657) $_657 = $_657
% 0.76/0.93  |- ifeq3 (theme skc14 $_659 skc14) true
% 0.76/0.93       (ifeq3 (theme skc14 $_658 $_656) true
% 0.76/0.93          (ifeq3 (agent skc14 $_659 $_660) true
% 0.76/0.93             (ifeq3 (agent skc14 $_658 $_660) true
% 0.76/0.93                (ifeq3 (think_believe_consider skc14 $_659) true
% 0.76/0.93                   (ifeq3 (think_believe_consider skc14 $_658) true
% 0.76/0.93                      (ifeq3 (proposition skc14 $_656) true $_656 skc14)
% 0.76/0.93                      skc14) skc14) skc14) skc14) skc14) skc14 = skc14
% 0.76/0.93  |- ifeq3 (theme skc9 $_659 skc14) true
% 0.76/0.93       (ifeq3 (theme skc9 $_658 $_656) true
% 0.76/0.93          (ifeq3 (agent skc9 $_659 $_660) true
% 0.76/0.93             (ifeq3 (agent skc9 $_658 $_660) true
% 0.76/0.93                (ifeq3 (think_believe_consider skc9 $_659) true
% 0.76/0.93                   (ifeq3 (think_believe_consider skc9 $_658) true
% 0.76/0.93                      (ifeq3 (proposition skc9 $_656) true $_656 skc14)
% 0.76/0.93                      skc14) skc14) skc14) skc14) skc14) skc14 = skc14
% 0.76/0.93  |- ifeq3 (theme skc14 $_659 $_657) true
% 0.76/0.93       (ifeq3 (theme skc14 skc15 $_656) true
% 0.76/0.93          (ifeq3 (agent skc14 $_659 $_660) true
% 0.76/0.93             (ifeq3 (agent skc14 skc15 $_660) true
% 0.76/0.93                (ifeq3 (think_believe_consider skc14 $_659) true
% 0.76/0.93                   (ifeq3 (proposition skc14 $_657) true
% 0.76/0.93                      (ifeq3 (proposition skc14 $_656) true $_656 $_657)
% 0.76/0.93                      $_657) $_657) $_657) $_657) $_657) $_657 = $_657
% 0.76/0.93  |- ifeq3 (theme skc9 $_659 $_657) true
% 0.76/0.93       (ifeq3 (theme skc9 skc15 $_656) true
% 0.76/0.93          (ifeq3 (agent skc9 $_659 $_660) true
% 0.76/0.93             (ifeq3 (agent skc9 skc15 $_660) true
% 0.76/0.93                (ifeq3 (think_believe_consider skc9 $_659) true
% 0.76/0.93                   (ifeq3 (proposition skc9 $_657) true
% 0.76/0.93                      (ifeq3 (proposition skc9 $_656) true $_656 $_657)
% 0.76/0.93                      $_657) $_657) $_657) $_657) $_657) $_657 = $_657
% 0.76/0.93  |- ifeq3 (theme skc14 skc15 $_657) true
% 0.76/0.93       (ifeq3 (theme skc14 $_658 $_656) true
% 0.76/0.93          (ifeq3 (agent skc14 skc15 $_660) true
% 0.76/0.93             (ifeq3 (agent skc14 $_658 $_660) true
% 0.76/0.93                (ifeq3 (think_believe_consider skc14 $_658) true
% 0.76/0.93                   (ifeq3 (proposition skc14 $_657) true
% 0.76/0.93                      (ifeq3 (proposition skc14 $_656) true $_656 $_657)
% 0.76/0.93                      $_657) $_657) $_657) $_657) $_657) $_657 = $_657
% 0.76/0.93  |- ifeq3 (theme skc9 skc15 $_657) true
% 0.76/0.93       (ifeq3 (theme skc9 $_658 $_656) true
% 0.76/0.93          (ifeq3 (agent skc9 skc15 $_660) true
% 0.76/0.93             (ifeq3 (agent skc9 $_658 $_660) true
% 0.76/0.93                (ifeq3 (think_believe_consider skc9 $_658) true
% 0.76/0.93                   (ifeq3 (proposition skc9 $_657) true
% 0.76/0.93                      (ifeq3 (proposition skc9 $_656) true $_656 $_657)
% 0.76/0.93                      $_657) $_657) $_657) $_657) $_657) $_657 = $_657
% 0.76/0.93  |- ifeq3 (theme skc14 $_659 $_657) true
% 0.76/0.93       (ifeq3 (theme skc14 skc15 $_656) true
% 0.76/0.93          (ifeq3 (agent skc14 $_659 skc17) true
% 0.76/0.93             (ifeq3 (think_believe_consider skc14 $_659) true
% 0.76/0.93                (ifeq3 (proposition skc14 $_657) true
% 0.76/0.93                   (ifeq3 (proposition skc14 $_656) true $_656 $_657) $_657)
% 0.76/0.93                $_657) $_657) $_657) $_657 = $_657
% 0.77/0.93  |- ifeq3 (theme skc14 $_659 $_657) true
% 0.77/0.93       (ifeq3 (theme skc14 (skf1 skc11) $_656) true
% 0.77/0.93          (ifeq3 (agent skc14 $_659 skc11) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc14 $_659) true
% 0.77/0.93                (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.93                   (ifeq3 (proposition skc14 $_657) true
% 0.77/0.93                      (ifeq3 (proposition skc14 $_656) true $_656 $_657)
% 0.77/0.93                      $_657) $_657) $_657) $_657) $_657) $_657 = $_657
% 0.77/0.93  |- ifeq3 (theme skc14 $_659 $_657) true
% 0.77/0.93       (ifeq3 (theme skc14 (skf1 skc17) $_656) true
% 0.77/0.93          (ifeq3 (agent skc14 $_659 skc17) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc14 $_659) true
% 0.77/0.93                (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.93                   (ifeq3 (proposition skc14 $_657) true
% 0.77/0.93                      (ifeq3 (proposition skc14 $_656) true $_656 $_657)
% 0.77/0.93                      $_657) $_657) $_657) $_657) $_657) $_657 = $_657
% 0.77/0.93  |- ifeq3 (theme skc9 $_659 $_657) true
% 0.77/0.93       (ifeq3 (theme skc9 skc15 $_656) true
% 0.77/0.93          (ifeq3 (agent skc9 $_659 skc17) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc9 $_659) true
% 0.77/0.93                (ifeq3 (proposition skc9 $_657) true
% 0.77/0.93                   (ifeq3 (proposition skc9 $_656) true $_656 $_657) $_657)
% 0.77/0.93                $_657) $_657) $_657) $_657 = $_657
% 0.77/0.93  |- ifeq3 (theme skc14 skc15 $_657) true
% 0.77/0.93       (ifeq3 (theme skc14 $_658 $_656) true
% 0.77/0.93          (ifeq3 (agent skc14 $_658 skc17) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc14 $_658) true
% 0.77/0.93                (ifeq3 (proposition skc14 $_657) true
% 0.77/0.93                   (ifeq3 (proposition skc14 $_656) true $_656 $_657) $_657)
% 0.77/0.93                $_657) $_657) $_657) $_657 = $_657
% 0.77/0.93  |- ifeq3 (theme skc14 (skf1 skc11) $_657) true
% 0.77/0.93       (ifeq3 (theme skc14 $_658 $_656) true
% 0.77/0.93          (ifeq3 (agent skc14 $_658 skc11) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.93                (ifeq3 (think_believe_consider skc14 $_658) true
% 0.77/0.93                   (ifeq3 (proposition skc14 $_657) true
% 0.77/0.93                      (ifeq3 (proposition skc14 $_656) true $_656 $_657)
% 0.77/0.93                      $_657) $_657) $_657) $_657) $_657) $_657 = $_657
% 0.77/0.93  |- ifeq3 (theme skc14 (skf1 skc17) $_657) true
% 0.77/0.93       (ifeq3 (theme skc14 $_658 $_656) true
% 0.77/0.93          (ifeq3 (agent skc14 $_658 skc17) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.93                (ifeq3 (think_believe_consider skc14 $_658) true
% 0.77/0.93                   (ifeq3 (proposition skc14 $_657) true
% 0.77/0.93                      (ifeq3 (proposition skc14 $_656) true $_656 $_657)
% 0.77/0.93                      $_657) $_657) $_657) $_657) $_657) $_657 = $_657
% 0.77/0.93  |- ifeq3 (theme skc9 skc15 $_657) true
% 0.77/0.93       (ifeq3 (theme skc9 $_658 $_656) true
% 0.77/0.93          (ifeq3 (agent skc9 $_658 skc17) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc9 $_658) true
% 0.77/0.93                (ifeq3 (proposition skc9 $_657) true
% 0.77/0.93                   (ifeq3 (proposition skc9 $_656) true $_656 $_657) $_657)
% 0.77/0.93                $_657) $_657) $_657) $_657 = $_657
% 0.77/0.93  |- ifeq3 (theme skc14 $_659 $_657) true
% 0.77/0.93       (ifeq3 (agent skc14 $_659 $_660) true
% 0.77/0.93          (ifeq3 (agent skc14 skc15 $_660) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc14 $_659) true
% 0.77/0.93                (ifeq3 (proposition skc14 $_657) true skc14 $_657) $_657)
% 0.77/0.93             $_657) $_657) $_657 = $_657
% 0.77/0.93  |- ifeq3 (theme skc9 $_659 $_657) true
% 0.77/0.93       (ifeq3 (agent skc9 $_659 $_660) true
% 0.77/0.93          (ifeq3 (agent skc9 skc15 $_660) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc9 $_659) true
% 0.77/0.93                (ifeq3 (proposition skc9 $_657) true skc14 $_657) $_657)
% 0.77/0.93             $_657) $_657) $_657 = $_657
% 0.77/0.93  |- ifeq3 (theme skc14 $_658 $_656) true
% 0.77/0.93       (ifeq3 (agent skc14 skc15 $_660) true
% 0.77/0.93          (ifeq3 (agent skc14 $_658 $_660) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc14 $_658) true
% 0.77/0.93                (ifeq3 (proposition skc14 $_656) true $_656 skc14) skc14)
% 0.77/0.93             skc14) skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc9 $_658 $_656) true
% 0.77/0.93       (ifeq3 (agent skc9 skc15 $_660) true
% 0.77/0.93          (ifeq3 (agent skc9 $_658 $_660) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc9 $_658) true
% 0.77/0.93                (ifeq3 (proposition skc9 $_656) true $_656 skc14) skc14)
% 0.77/0.93             skc14) skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc14 $_662 skc14) true
% 0.77/0.93       (ifeq3 (agent skc14 $_662 $_663) true
% 0.77/0.93          (ifeq3 (agent skc14 skc15 $_663) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc14 $_662) true skc14 skc14)
% 0.77/0.93             skc14) skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc14 skc15 $_661) true
% 0.77/0.93       (ifeq3 (agent skc14 skc15 $_663) true
% 0.77/0.93          (ifeq3 (agent skc14 skc15 $_663) true
% 0.77/0.93             (ifeq3 (proposition skc14 $_661) true skc14 $_661) $_661) $_661)
% 0.77/0.93       $_661 = $_661
% 0.77/0.93  |- ifeq3 (theme skc14 $_662 $_661) true
% 0.77/0.93       (ifeq3 (agent skc14 $_662 skc17) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc14 $_662) true
% 0.77/0.93             (ifeq3 (proposition skc14 $_661) true skc14 $_661) $_661) $_661)
% 0.77/0.93       $_661 = $_661
% 0.77/0.93  |- ifeq3 (theme skc14 skc15 $_661) true
% 0.77/0.93       (ifeq3 (proposition skc14 $_661) true skc14 $_661) $_661 = $_661
% 0.77/0.93  |- ifeq3 (theme skc14 (skf1 skc11) $_661) true
% 0.77/0.93       (ifeq3 (agent skc14 skc15 skc11) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.93             (ifeq3 (proposition skc14 $_661) true skc14 $_661) $_661) $_661)
% 0.77/0.93       $_661 = $_661
% 0.77/0.93  |- ifeq3 (theme skc14 (skf1 skc17) $_661) true
% 0.77/0.93       (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.93          (ifeq3 (proposition skc14 $_661) true skc14 $_661) $_661) $_661 =
% 0.77/0.93     $_661
% 0.77/0.93  |- ifeq3 (agent skc14 skc15 $_663) true
% 0.77/0.93       (ifeq3 (agent skc14 skc15 $_663) true skc14 skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc14 (skf1 skc11) skc14) true
% 0.77/0.93       (ifeq3 (agent skc14 skc15 skc11) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true skc14
% 0.77/0.93             skc14) skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc14 (skf1 skc17) skc14) true
% 0.77/0.93       (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true skc14 skc14)
% 0.77/0.93       skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc14 $_669 skc14) true
% 0.77/0.93       (ifeq3 (agent skc14 $_669 skc17) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc14 $_669) true skc14 skc14)
% 0.77/0.93          skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc9 $_676 skc14) true
% 0.77/0.93       (ifeq3 (agent skc9 $_676 $_677) true
% 0.77/0.93          (ifeq3 (agent skc9 skc15 $_677) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc9 $_676) true skc14 skc14)
% 0.77/0.93             skc14) skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc9 skc15 $_675) true
% 0.77/0.93       (ifeq3 (agent skc9 skc15 $_677) true
% 0.77/0.93          (ifeq3 (agent skc9 skc15 $_677) true
% 0.77/0.93             (ifeq3 (proposition skc9 $_675) true skc14 $_675) $_675) $_675)
% 0.77/0.93       $_675 = $_675
% 0.77/0.93  |- ifeq3 (theme skc9 $_676 $_675) true
% 0.77/0.93       (ifeq3 (agent skc9 $_676 skc17) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc9 $_676) true
% 0.77/0.93             (ifeq3 (proposition skc9 $_675) true skc14 $_675) $_675) $_675)
% 0.77/0.93       $_675 = $_675
% 0.77/0.93  |- ifeq3 (theme skc9 skc15 $_675) true
% 0.77/0.93       (ifeq3 (proposition skc9 $_675) true skc14 $_675) $_675 = $_675
% 0.77/0.93  |- ifeq3 (agent skc9 skc15 $_677) true
% 0.77/0.93       (ifeq3 (agent skc9 skc15 $_677) true skc14 skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc9 $_681 skc14) true
% 0.77/0.93       (ifeq3 (agent skc9 $_681 skc17) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc9 $_681) true skc14 skc14) skc14)
% 0.77/0.93       skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc14 $_688 skc14) true
% 0.77/0.93       (ifeq3 (agent skc14 skc15 $_689) true
% 0.77/0.93          (ifeq3 (agent skc14 $_688 $_689) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc14 $_688) true skc14 skc14)
% 0.77/0.93             skc14) skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc14 skc15 $_687) true
% 0.77/0.93       (ifeq3 (agent skc14 skc15 $_689) true
% 0.77/0.93          (ifeq3 (agent skc14 skc15 $_689) true
% 0.77/0.93             (ifeq3 (proposition skc14 $_687) true $_687 skc14) skc14) skc14)
% 0.77/0.93       skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc14 skc15 $_687) true
% 0.77/0.93       (ifeq3 (proposition skc14 $_687) true $_687 skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc14 (skf1 skc11) $_687) true
% 0.77/0.93       (ifeq3 (agent skc14 skc15 skc11) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.93             (ifeq3 (proposition skc14 $_687) true $_687 skc14) skc14) skc14)
% 0.77/0.93       skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc14 (skf1 skc17) $_687) true
% 0.77/0.93       (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.93          (ifeq3 (proposition skc14 $_687) true $_687 skc14) skc14) skc14 =
% 0.77/0.93     skc14
% 0.77/0.93  |- ifeq3 (theme skc14 $_688 $_687) true
% 0.77/0.93       (ifeq3 (agent skc14 $_688 skc17) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc14 $_688) true
% 0.77/0.93             (ifeq3 (proposition skc14 $_687) true $_687 skc14) skc14) skc14)
% 0.77/0.93       skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc9 $_700 skc14) true
% 0.77/0.93       (ifeq3 (agent skc9 skc15 $_701) true
% 0.77/0.93          (ifeq3 (agent skc9 $_700 $_701) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc9 $_700) true skc14 skc14)
% 0.77/0.93             skc14) skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc9 skc15 $_699) true
% 0.77/0.93       (ifeq3 (agent skc9 skc15 $_701) true
% 0.77/0.93          (ifeq3 (agent skc9 skc15 $_701) true
% 0.77/0.93             (ifeq3 (proposition skc9 $_699) true $_699 skc14) skc14) skc14)
% 0.77/0.93       skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc9 skc15 $_699) true
% 0.77/0.93       (ifeq3 (proposition skc9 $_699) true $_699 skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc9 $_700 $_699) true
% 0.77/0.93       (ifeq3 (agent skc9 $_700 skc17) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc9 $_700) true
% 0.77/0.93             (ifeq3 (proposition skc9 $_699) true $_699 skc14) skc14) skc14)
% 0.77/0.93       skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc14 $_709 skc14) true
% 0.77/0.93       (ifeq3 (theme skc14 skc15 $_707) true
% 0.77/0.93          (ifeq3 (agent skc14 $_709 skc17) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc14 $_709) true
% 0.77/0.93                (ifeq3 (proposition skc14 $_707) true $_707 skc14) skc14)
% 0.77/0.93             skc14) skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc14 skc15 $_708) true
% 0.77/0.93       (ifeq3 (theme skc14 skc15 $_707) true
% 0.77/0.93          (ifeq3 (proposition skc14 $_708) true
% 0.77/0.93             (ifeq3 (proposition skc14 $_707) true $_707 $_708) $_708) $_708)
% 0.77/0.93       $_708 = $_708
% 0.77/0.93  |- ifeq3 (theme skc14 (skf1 skc17) $_708) true
% 0.77/0.93       (ifeq3 (theme skc14 skc15 $_707) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.93             (ifeq3 (proposition skc14 $_708) true
% 0.77/0.93                (ifeq3 (proposition skc14 $_707) true $_707 $_708) $_708)
% 0.77/0.93             $_708) $_708) $_708 = $_708
% 0.77/0.93  |- ifeq3 (theme skc14 (skf1 skc17) skc14) true
% 0.77/0.93       (ifeq3 (theme skc14 skc15 $_712) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.93             (ifeq3 (proposition skc14 $_712) true $_712 skc14) skc14) skc14)
% 0.77/0.93       skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc9 $_719 skc14) true
% 0.77/0.93       (ifeq3 (theme skc9 skc15 $_717) true
% 0.77/0.93          (ifeq3 (agent skc9 $_719 skc17) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc9 $_719) true
% 0.77/0.93                (ifeq3 (proposition skc9 $_717) true $_717 skc14) skc14)
% 0.77/0.93             skc14) skc14) skc14 = skc14
% 0.77/0.93  |- ifeq3 (theme skc9 skc15 $_718) true
% 0.77/0.93       (ifeq3 (theme skc9 skc15 $_717) true
% 0.77/0.93          (ifeq3 (proposition skc9 $_718) true
% 0.77/0.93             (ifeq3 (proposition skc9 $_717) true $_717 $_718) $_718) $_718)
% 0.77/0.93       $_718 = $_718
% 0.77/0.93  |- ifeq3 (theme skc14 skc15 $_725) true
% 0.77/0.93       (ifeq3 (theme skc14 $_726 skc14) true
% 0.77/0.93          (ifeq3 (agent skc14 $_726 skc17) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc14 $_726) true
% 0.77/0.93                (ifeq3 (proposition skc14 $_725) true skc14 $_725) $_725)
% 0.77/0.93             $_725) $_725) $_725 = $_725
% 0.77/0.93  |- ifeq3 (theme skc14 skc15 $_725) true
% 0.77/0.93       (ifeq3 (theme skc14 (skf1 skc17) $_724) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.93             (ifeq3 (proposition skc14 $_725) true
% 0.77/0.93                (ifeq3 (proposition skc14 $_724) true $_724 $_725) $_725)
% 0.77/0.93             $_725) $_725) $_725 = $_725
% 0.77/0.93  |- ifeq3 (theme skc14 skc15 $_728) true
% 0.77/0.93       (ifeq3 (theme skc14 (skf1 skc17) skc14) true
% 0.77/0.93          (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.93             (ifeq3 (proposition skc14 $_728) true skc14 $_728) $_728) $_728)
% 0.77/0.93       $_728 = $_728
% 0.77/0.93  |- ifeq3 (theme skc9 skc15 $_731) true
% 0.77/0.93       (ifeq3 (theme skc9 $_732 skc14) true
% 0.77/0.93          (ifeq3 (agent skc9 $_732 skc17) true
% 0.77/0.93             (ifeq3 (think_believe_consider skc9 $_732) true
% 0.77/0.93                (ifeq3 (proposition skc9 $_731) true skc14 $_731) $_731)
% 0.77/0.93             $_731) $_731) $_731 = $_731
% 0.77/0.94  |- ifeq3 (theme skc14 $_735 $_734) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc11) skc14) true
% 0.77/0.94          (ifeq3 (agent skc14 $_735 skc11) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 $_735) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_734) true skc14 $_734) $_734)
% 0.77/0.94                $_734) $_734) $_734) $_734 = $_734
% 0.77/0.94  |- ifeq3 (theme skc14 $_735 skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc11) $_733) true
% 0.77/0.94          (ifeq3 (agent skc14 $_735 skc11) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 $_735) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_733) true $_733 skc14) skc14)
% 0.77/0.94                skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 skc15 $_734) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc11) $_733) true
% 0.77/0.94          (ifeq3 (agent skc14 skc15 skc11) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94                (ifeq3 (proposition skc14 $_734) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_733) true $_733 $_734) $_734)
% 0.77/0.94                $_734) $_734) $_734) $_734 = $_734
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc11) $_734) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc11) $_733) true
% 0.77/0.94          (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94                (ifeq3 (proposition skc14 $_734) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_733) true $_733 $_734) $_734)
% 0.77/0.94                $_734) $_734) $_734) $_734 = $_734
% 0.77/0.94  |- ifeq3 (theme skc14 $_737 skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc11) skc14) true
% 0.77/0.94          (ifeq3 (agent skc14 $_737 skc11) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 $_737) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true skc14
% 0.77/0.94                   skc14) skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 skc15 $_736) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc11) skc14) true
% 0.77/0.94          (ifeq3 (agent skc14 skc15 skc11) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94                (ifeq3 (proposition skc14 $_736) true skc14 $_736) $_736)
% 0.77/0.94             $_736) $_736) $_736 = $_736
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc11) $_736) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc11) skc14) true
% 0.77/0.94          (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94                (ifeq3 (proposition skc14 $_736) true skc14 $_736) $_736)
% 0.77/0.94             $_736) $_736) $_736 = $_736
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc11) skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc11) skc14) true
% 0.77/0.94          (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true skc14
% 0.77/0.94                skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc11) skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc11) $_741) true
% 0.77/0.94          (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94                (ifeq3 (proposition skc14 $_741) true $_741 skc14) skc14)
% 0.77/0.94             skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 $_750 $_749) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc17) skc14) true
% 0.77/0.94          (ifeq3 (agent skc14 $_750 skc17) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 $_750) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_749) true skc14 $_749) $_749)
% 0.77/0.94                $_749) $_749) $_749) $_749 = $_749
% 0.77/0.94  |- ifeq3 (theme skc14 $_750 skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc17) $_748) true
% 0.77/0.94          (ifeq3 (agent skc14 $_750 skc17) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 $_750) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_748) true $_748 skc14) skc14)
% 0.77/0.94                skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc17) $_749) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc17) $_748) true
% 0.77/0.94          (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.94                (ifeq3 (proposition skc14 $_749) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_748) true $_748 $_749) $_749)
% 0.77/0.94                $_749) $_749) $_749) $_749 = $_749
% 0.77/0.94  |- ifeq3 (theme skc14 $_752 skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc17) skc14) true
% 0.77/0.94          (ifeq3 (agent skc14 $_752 skc17) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 $_752) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true skc14
% 0.77/0.94                   skc14) skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc17) $_751) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc17) skc14) true
% 0.77/0.94          (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.94                (ifeq3 (proposition skc14 $_751) true skc14 $_751) $_751)
% 0.77/0.94             $_751) $_751) $_751 = $_751
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc17) skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc17) skc14) true
% 0.77/0.94          (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true skc14
% 0.77/0.94                skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc17) skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 (skf1 skc17) $_755) true
% 0.77/0.94          (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.94                (ifeq3 (proposition skc14 $_755) true $_755 skc14) skc14)
% 0.77/0.94             skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc11) $_761) true
% 0.77/0.94       (ifeq3 (theme skc14 $_762 skc14) true
% 0.77/0.94          (ifeq3 (agent skc14 $_762 skc11) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 $_762) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_761) true skc14 $_761) $_761)
% 0.77/0.94                $_761) $_761) $_761) $_761 = $_761
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc11) skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 $_762 $_760) true
% 0.77/0.94          (ifeq3 (agent skc14 $_762 skc11) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 $_762) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_760) true $_760 skc14) skc14)
% 0.77/0.94                skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc11) $_761) true
% 0.77/0.94       (ifeq3 (theme skc14 skc15 $_760) true
% 0.77/0.94          (ifeq3 (agent skc14 skc15 skc11) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94                (ifeq3 (proposition skc14 $_761) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_760) true $_760 $_761) $_761)
% 0.77/0.94                $_761) $_761) $_761) $_761 = $_761
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc11) skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 $_764 skc14) true
% 0.77/0.94          (ifeq3 (agent skc14 $_764 skc11) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 $_764) true skc14 skc14)
% 0.77/0.94                skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc11) skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 skc15 $_766) true
% 0.77/0.94          (ifeq3 (agent skc14 skc15 skc11) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc11)) true
% 0.77/0.94                (ifeq3 (proposition skc14 $_766) true $_766 skc14) skc14)
% 0.77/0.94             skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc17) $_772) true
% 0.77/0.94       (ifeq3 (theme skc14 $_773 skc14) true
% 0.77/0.94          (ifeq3 (agent skc14 $_773 skc17) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 $_773) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_772) true skc14 $_772) $_772)
% 0.77/0.94                $_772) $_772) $_772) $_772 = $_772
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc17) skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 $_773 $_771) true
% 0.77/0.94          (ifeq3 (agent skc14 $_773 skc17) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 $_773) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_771) true $_771 skc14) skc14)
% 0.77/0.94                skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 (skf1 skc17) skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 $_775 skc14) true
% 0.77/0.94          (ifeq3 (agent skc14 $_775 skc17) true
% 0.77/0.94             (ifeq3 (think_believe_consider skc14 (skf1 skc17)) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 $_775) true skc14 skc14)
% 0.77/0.94                skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 $_787 skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 $_786 skc14) true
% 0.77/0.94          (ifeq3 (agent skc14 $_787 $_788) true
% 0.77/0.94             (ifeq3 (agent skc14 $_786 $_788) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 $_787) true
% 0.77/0.94                   (ifeq3 (think_believe_consider skc14 $_786) true skc14
% 0.77/0.94                      skc14) skc14) skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 skc15 $_785) true
% 0.77/0.94       (ifeq3 (theme skc14 $_786 skc14) true
% 0.77/0.94          (ifeq3 (agent skc14 skc15 $_788) true
% 0.77/0.94             (ifeq3 (agent skc14 $_786 $_788) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 $_786) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_785) true skc14 $_785) $_785)
% 0.77/0.94                $_785) $_785) $_785) $_785 = $_785
% 0.77/0.94  |- ifeq3 (theme skc9 $_797 skc14) true
% 0.77/0.94       (ifeq3 (theme skc9 $_796 skc14) true
% 0.77/0.94          (ifeq3 (agent skc9 $_797 $_798) true
% 0.77/0.94             (ifeq3 (agent skc9 $_796 $_798) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc9 $_797) true
% 0.77/0.94                   (ifeq3 (think_believe_consider skc9 $_796) true skc14
% 0.77/0.94                      skc14) skc14) skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc9 skc15 $_795) true
% 0.77/0.94       (ifeq3 (theme skc9 $_796 skc14) true
% 0.77/0.94          (ifeq3 (agent skc9 skc15 $_798) true
% 0.77/0.94             (ifeq3 (agent skc9 $_796 $_798) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc9 $_796) true
% 0.77/0.94                   (ifeq3 (proposition skc9 $_795) true skc14 $_795) $_795)
% 0.77/0.94                $_795) $_795) $_795) $_795 = $_795
% 0.77/0.94  |- ifeq3 (theme skc14 $_807 skc14) true
% 0.77/0.94       (ifeq3 (theme skc14 skc15 $_805) true
% 0.77/0.94          (ifeq3 (agent skc14 $_807 $_808) true
% 0.77/0.94             (ifeq3 (agent skc14 skc15 $_808) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc14 $_807) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_805) true $_805 skc14) skc14)
% 0.77/0.94                skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc14 skc15 $_806) true
% 0.77/0.94       (ifeq3 (theme skc14 skc15 $_805) true
% 0.77/0.94          (ifeq3 (agent skc14 skc15 $_808) true
% 0.77/0.94             (ifeq3 (agent skc14 skc15 $_808) true
% 0.77/0.94                (ifeq3 (proposition skc14 $_806) true
% 0.77/0.94                   (ifeq3 (proposition skc14 $_805) true $_805 $_806) $_806)
% 0.77/0.94                $_806) $_806) $_806) $_806 = $_806
% 0.77/0.94  |- ifeq3 (theme skc9 $_817 skc14) true
% 0.77/0.94       (ifeq3 (theme skc9 skc15 $_815) true
% 0.77/0.94          (ifeq3 (agent skc9 $_817 $_818) true
% 0.77/0.94             (ifeq3 (agent skc9 skc15 $_818) true
% 0.77/0.94                (ifeq3 (think_believe_consider skc9 $_817) true
% 0.77/0.94                   (ifeq3 (proposition skc9 $_815) true $_815 skc14) skc14)
% 0.77/0.94                skc14) skc14) skc14) skc14 = skc14
% 0.77/0.94  |- ifeq3 (theme skc9 skc15 $_816) true
% 0.77/0.94       (ifeq3 (theme skc9 skc15 $_815) true
% 0.77/0.94          (ifeq3 (agent skc9 skc15 $_818) true
% 0.77/0.94             (ifeq3 (agent skc9 skc15 $_818) true
% 0.77/0.94                (ifeq3 (proposition skc9 $_816) true
% 0.77/0.94                   (ifeq3 (proposition skc9 $_815) true $_815 $_816) $_816)
% 0.77/0.94                $_816) $_816) $_816) $_816 = $_816
% 0.77/0.94  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.77/0.94  
%------------------------------------------------------------------------------