%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : NLP225-10 : TPTP v7.3.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n187.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.5MB % OS : Linux 3.10.0-862.11.6.el7.x86_64 % CPULimit : 300s % DateTime : Wed Feb 27 13:38:03 EST 2019 % Result : Satisfiable 32.60s % Output : Model 32.98s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : NLP225-10 : TPTP v7.3.0. Released v7.3.0. % 0.00/0.05 % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % 0.03/0.28 % Computer : n187.star.cs.uiowa.edu % 0.03/0.28 % Model : x86_64 x86_64 % 0.03/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.28 % Memory : 32218.5MB % 0.03/0.28 % OS : Linux 3.10.0-862.11.6.el7.x86_64 % 0.03/0.28 % CPULimit : 300 % 0.03/0.28 % DateTime : Fri Feb 22 07:40:55 CST 2019 % 0.03/0.28 % CPUTime : % 0.03/0.28 E-Darwin 1.5 2012/06/20 (based on Darwin 1.3) % 0.03/0.28 % 0.03/0.28 % 0.03/0.28 Defaulting to tptp format. % 0.03/0.28 Parsing /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.03/0.28 % 0.03/0.29 % 0.03/0.29 % 0.08/0.30 Proving ... % 0.08/0.30 % 32.60/32.84 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 32.60/32.84 % 32.60/32.84 START OF MODEL (DIG): % 32.90/33.19 (skc13 = skc15) % 32.90/33.19 (true = forename(skc8, skc13)) % 32.90/33.19 (true = forename(skc8, skc15)) % 32.90/33.19 (true = forename(skc11, skc13)) % 32.90/33.19 (true = forename(skc11, skc15)) % 32.90/33.19 (true = eventuality(skc8, skc9)) % 32.90/33.19 (true = eventuality(skc8, skc12)) % 32.90/33.19 (true = eventuality(skc11, skc9)) % 32.90/33.19 (true = eventuality(skc11, skc12)) % 32.90/33.19 (eventuality(skc11, skf1(_0)) = true) % 32.90/33.19 (true = relname(skc8, skc13)) % 32.90/33.19 (true = relname(skc8, skc15)) % 32.90/33.19 (true = relname(skc11, skc13)) % 32.90/33.19 (true = relname(skc11, skc15)) % 32.90/33.19 (true = thing(skc8, skc9)) % 32.90/33.19 (true = thing(skc8, skc13)) % 32.90/33.19 (true = thing(skc8, skc12)) % 32.90/33.19 (true = thing(skc8, skc11)) % 32.90/33.19 (true = thing(skc8, skc15)) % 32.90/33.19 (true = thing(skc8, skc10)) % 32.90/33.19 (true = thing(skc11, skc9)) % 32.90/33.19 (true = thing(skc11, skc13)) % 32.90/33.19 (true = thing(skc11, skc12)) % 32.90/33.19 (thing(skc11, skf1(_0)) = true) % 32.90/33.19 (true = thing(skc11, skc11)) % 32.90/33.19 (true = thing(skc11, skc10)) % 32.90/33.19 (true = relation(skc8, skc13)) % 32.90/33.19 (true = relation(skc8, skc11)) % 32.90/33.19 (true = relation(skc8, skc15)) % 32.90/33.19 (true = relation(skc11, skc13)) % 32.90/33.19 (true = relation(skc11, skc11)) % 32.90/33.19 (true = relation(skc11, skc15)) % 32.90/33.19 (true = singleton(skc8, skc9)) % 32.90/33.19 (true = singleton(skc8, skc13)) % 32.90/33.19 (true = singleton(skc8, skc12)) % 32.90/33.19 (true = singleton(skc8, skc11)) % 32.90/33.19 (true = singleton(skc8, skc10)) % 32.90/33.19 (true = singleton(skc11, skc9)) % 32.90/33.19 (true = singleton(skc11, skc13)) % 32.90/33.19 (true = singleton(skc11, skc12)) % 32.90/33.19 (singleton(skc11, skf1(_0)) = true) % 32.90/33.19 (true = singleton(skc11, skc11)) % 32.90/33.19 (true = singleton(skc11, skc10)) % 32.90/33.19 (true = abstraction(skc8, skc13)) % 32.90/33.19 (true = abstraction(skc8, skc11)) % 32.90/33.19 (true = abstraction(skc8, skc15)) % 32.90/33.19 (true = abstraction(skc11, skc13)) % 32.90/33.19 (true = abstraction(skc11, skc11)) % 32.90/33.19 (true = abstraction(skc11, skc15)) % 32.90/33.19 (true = specific(skc8, skc9)) % 32.90/33.19 (true = specific(skc8, skc12)) % 32.90/33.19 (true = specific(skc8, skc10)) % 32.90/33.19 (true = specific(skc11, skc9)) % 32.90/33.19 (true = specific(skc11, skc12)) % 32.90/33.19 (specific(skc11, skf1(_0)) = true) % 32.90/33.19 (true = specific(skc11, skc10)) % 32.90/33.19 (true = nonhuman(skc8, skc13)) % 32.90/33.19 (true = nonhuman(skc8, skc11)) % 32.90/33.19 (true = nonhuman(skc8, skc15)) % 32.90/33.19 (true = nonhuman(skc11, skc13)) % 32.90/33.19 (true = nonhuman(skc11, skc11)) % 32.90/33.19 (true = nonexistent(skc8, skc9)) % 32.90/33.19 (true = nonexistent(skc8, skc12)) % 32.90/33.19 (true = nonexistent(skc11, skc9)) % 32.90/33.19 (true = nonexistent(skc11, skc12)) % 32.90/33.19 (nonexistent(skc11, skf1(_0)) = true) % 32.90/33.19 (true = general(skc8, skc13)) % 32.90/33.19 (true = general(skc8, skc11)) % 32.90/33.19 (true = general(skc8, skc15)) % 32.90/33.19 (true = general(skc11, skc13)) % 32.90/33.19 (true = general(skc11, skc11)) % 32.90/33.19 (true = unisex(skc8, skc9)) % 32.90/33.19 (true = unisex(skc8, skc13)) % 32.90/33.19 (true = unisex(skc8, skc12)) % 32.90/33.19 (true = unisex(skc8, skc11)) % 32.90/33.19 (true = unisex(skc8, skc15)) % 32.90/33.19 (true = unisex(skc11, skc9)) % 32.90/33.19 (true = unisex(skc11, skc13)) % 32.90/33.19 (true = unisex(skc11, skc12)) % 32.90/33.19 (unisex(skc11, skf1(_0)) = true) % 32.90/33.19 (true = unisex(skc11, skc11)) % 32.90/33.19 (true = jules_forename(skc8, skc13)) % 32.90/33.19 (true = jules_forename(skc8, skc15)) % 32.90/33.19 (true = jules_forename(skc11, skc13)) % 32.90/33.19 (true = jules_forename(skc11, skc15)) % 32.90/33.19 (skc10 = skc14) % 32.90/33.19 (event(skc8, skc9) = true) % 32.90/33.19 (event(skc8, skc12) = true) % 32.90/33.19 (event(skc11, skc9) = true) % 32.90/33.19 (event(skc11, skc12) = true) % 32.90/33.19 (event(skc11, skf1(_0)) = true) % 32.90/33.19 (smoke(skc11, skf1(_0)) = true) % 32.90/33.19 (man(skc8, skc14) = true) % 32.90/33.19 (man(skc8, skc10) = true) % 32.90/33.19 (man(skc11, skc14) = true) % 32.90/33.19 (man(skc11, skc10) = true) % 32.90/33.19 (proposition(skc8, skc11) = true) % 32.90/33.19 (proposition(skc11, skc11) = true) % 32.90/33.19 (human_person(skc8, skc14) = true) % 32.90/33.19 (human_person(skc8, skc10) = true) % 32.90/33.19 (human_person(skc11, skc10) = true) % 32.90/33.19 (vincent_forename(skc8, skc13) = true) % 32.90/33.19 (vincent_forename(skc11, skc13) = true) % 32.90/33.19 (organism(skc8, skc10) = true) % 32.90/33.19 (organism(skc11, skc10) = true) % 32.90/33.19 (be(skc8, skc9, skc14, skc10) = true) % 32.90/33.19 (be(skc8, skc9, skc10, skc10) = true) % 32.90/33.19 (be(skc11, skc9, skc14, skc10) = true) % 32.90/33.19 (be(skc11, skc9, skc10, skc10) = true) % 32.90/33.19 (entity(skc8, skc10) = true) % 32.90/33.19 (entity(skc11, skc10) = true) % 32.90/33.19 (accessible_world(skc8, skc11) = true) % 32.90/33.19 (existent(skc8, skc10) = true) % 32.90/33.19 (existent(skc11, skc10) = true) % 32.90/33.19 (present(skc8, skc12) = true) % 32.90/33.19 (present(skc11, skc12) = true) % 32.90/33.19 (present(skc11, skf1(_0)) = true) % 32.90/33.19 (impartial(skc8, skc10) = true) % 32.90/33.19 (impartial(skc11, skc10) = true) % 32.90/33.19 (think_believe_consider(skc8, skc12) = true) % 32.90/33.19 (think_believe_consider(skc11, skc12) = true) % 32.90/33.19 (living(skc8, skc10) = true) % 32.90/33.19 (living(skc11, skc10) = true) % 32.90/33.19 (of(skc8, skc13, skc14) = true) % 32.90/33.19 (of(skc8, skc13, skc10) = true) % 32.90/33.19 (of(skc8, skc15, skc14) = true) % 32.90/33.19 (of(skc8, skc15, skc10) = true) % 32.90/33.19 (of(skc11, skc13, skc14) = true) % 32.90/33.19 (of(skc11, skc13, skc10) = true) % 32.90/33.19 (of(skc11, skc15, skc14) = true) % 32.90/33.19 (of(skc11, skc15, skc10) = true) % 32.90/33.19 (ifeq3(entity(skc8, skc14), true, skc13, skc13) = skc13) % 32.90/33.19 (ifeq3(entity(skc8, skc14), true, skc13, skc15) = skc15) % 32.90/33.19 (ifeq3(entity(skc8, skc14), true, skc15, skc13) = skc13) % 32.90/33.19 (ifeq3(entity(skc8, skc14), true, skc15, skc15) = skc15) % 32.90/33.19 (ifeq3(entity(skc8, skc10), true, skc13, skc13) = skc13) % 32.90/33.19 (ifeq3(entity(skc8, skc10), true, skc13, skc15) = skc15) % 32.90/33.19 (ifeq3(entity(skc8, skc10), true, skc15, skc13) = skc13) % 32.90/33.19 (ifeq3(entity(skc8, skc10), true, skc15, skc15) = skc15) % 32.90/33.19 (ifeq3(entity(skc11, skc10), true, skc13, skc13) = skc13) % 32.90/33.19 (ifeq3(entity(skc11, skc10), true, skc13, skc15) = skc15) % 32.90/33.19 (ifeq3(entity(skc11, skc10), true, skc15, skc13) = skc13) % 32.90/33.19 (ifeq3(entity(skc11, skc10), true, skc15, skc15) = skc15) % 32.90/33.19 (ifeq3(_0, _0, _1, _2) = _1) % 32.90/33.19 (ifeq3(be(_0, _1, _2, _3), true, _2, _3) = _3) % 32.90/33.19 (ifeq3(of(_0, _1, _2), true, ifeq3(of(_0, _3, _2), true, ifeq3(forename(_0, _1), true, ifeq3(forename(_0, _3), true, ifeq3(entity(_0, _2), true, _1, _3), _3), _3), _3), _3) = _3) % 32.98/33.19 (ifeq3(of(skc8, _0, _1), true, ifeq3(of(skc8, skc13, _1), true, ifeq3(forename(skc8, _0), true, ifeq3(entity(skc8, _1), true, _0, skc13), skc13), skc13), skc13) = skc13) % 32.98/33.19 (ifeq3(of(skc8, _0, _1), true, ifeq3(of(skc8, skc15, _1), true, ifeq3(forename(skc8, _0), true, ifeq3(entity(skc8, _1), true, _0, skc15), skc15), skc15), skc15) = skc15) % 32.98/33.19 (ifeq3(of(skc8, _0, skc14), true, ifeq3(forename(skc8, _0), true, ifeq3(entity(skc8, skc14), true, _0, skc13), skc13), skc13) = skc13) % 32.98/33.19 (ifeq3(of(skc8, _0, skc14), true, ifeq3(forename(skc8, _0), true, ifeq3(entity(skc8, skc14), true, _0, skc15), skc15), skc15) = skc15) % 32.98/33.19 (ifeq3(of(skc8, _0, skc14), true, ifeq3(forename(skc8, _0), true, ifeq3(entity(skc8, skc14), true, skc13, _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(of(skc8, _0, skc14), true, ifeq3(forename(skc8, _0), true, ifeq3(entity(skc8, skc14), true, skc15, _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(of(skc8, _0, skc10), true, ifeq3(of(skc8, _1, skc10), true, ifeq3(forename(skc8, _0), true, ifeq3(forename(skc8, _1), true, _0, _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(of(skc8, _0, skc10), true, ifeq3(forename(skc8, _0), true, _0, skc13), skc13) = skc13) % 32.98/33.19 (ifeq3(of(skc8, _0, skc10), true, ifeq3(forename(skc8, _0), true, _0, skc15), skc15) = skc15) % 32.98/33.19 (ifeq3(of(skc8, _0, skc10), true, ifeq3(forename(skc8, _0), true, skc13, _0), _0) = _0) % 32.98/33.19 (ifeq3(of(skc8, _0, skc10), true, ifeq3(forename(skc8, _0), true, ifeq3(entity(skc8, skc10), true, _0, skc13), skc13), skc13) = skc13) % 32.98/33.19 (ifeq3(of(skc8, _0, skc10), true, ifeq3(forename(skc8, _0), true, ifeq3(entity(skc8, skc10), true, _0, skc15), skc15), skc15) = skc15) % 32.98/33.19 (ifeq3(of(skc8, _0, skc10), true, ifeq3(forename(skc8, _0), true, ifeq3(entity(skc8, skc10), true, skc13, _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(of(skc8, _0, skc10), true, ifeq3(forename(skc8, _0), true, ifeq3(entity(skc8, skc10), true, skc15, _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(of(skc8, _0, skc10), true, ifeq3(forename(skc8, _0), true, skc15, _0), _0) = _0) % 32.98/33.19 (ifeq3(of(skc8, skc13, _0), true, ifeq3(of(skc8, skc13, _0), true, ifeq3(entity(skc8, _0), true, skc13, skc13), skc13), skc13) = skc13) % 32.98/33.19 (ifeq3(of(skc8, skc13, _0), true, ifeq3(of(skc8, _1, _0), true, ifeq3(forename(skc8, _1), true, ifeq3(entity(skc8, _0), true, skc13, _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(of(skc8, skc13, _0), true, ifeq3(of(skc8, skc15, _0), true, ifeq3(entity(skc8, _0), true, skc13, skc15), skc15), skc15) = skc15) % 32.98/33.19 (ifeq3(of(skc8, skc15, _0), true, ifeq3(of(skc8, skc13, _0), true, ifeq3(entity(skc8, _0), true, skc15, skc13), skc13), skc13) = skc13) % 32.98/33.19 (ifeq3(of(skc8, skc15, _0), true, ifeq3(of(skc8, _1, _0), true, ifeq3(forename(skc8, _1), true, ifeq3(entity(skc8, _0), true, skc15, _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(of(skc8, skc15, _0), true, ifeq3(of(skc8, skc15, _0), true, ifeq3(entity(skc8, _0), true, skc15, skc15), skc15), skc15) = skc15) % 32.98/33.19 (ifeq3(of(skc11, _0, _1), true, ifeq3(of(skc11, skc13, _1), true, ifeq3(forename(skc11, _0), true, ifeq3(entity(skc11, _1), true, _0, skc13), skc13), skc13), skc13) = skc13) % 32.98/33.19 (ifeq3(of(skc11, _0, _1), true, ifeq3(of(skc11, skc15, _1), true, ifeq3(forename(skc11, _0), true, ifeq3(entity(skc11, _1), true, _0, skc15), skc15), skc15), skc15) = skc15) % 32.98/33.19 (ifeq3(of(skc11, _0, skc10), true, ifeq3(of(skc11, _1, skc10), true, ifeq3(forename(skc11, _0), true, ifeq3(forename(skc11, _1), true, _0, _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(of(skc11, _0, skc10), true, ifeq3(forename(skc11, _0), true, _0, skc13), skc13) = skc13) % 32.98/33.19 (ifeq3(of(skc11, _0, skc10), true, ifeq3(forename(skc11, _0), true, skc13, _0), _0) = _0) % 32.98/33.19 (ifeq3(of(skc11, _0, skc10), true, ifeq3(forename(skc11, _0), true, ifeq3(entity(skc11, skc10), true, _0, skc13), skc13), skc13) = skc13) % 32.98/33.19 (ifeq3(of(skc11, _0, skc10), true, ifeq3(forename(skc11, _0), true, ifeq3(entity(skc11, skc10), true, _0, skc15), skc15), skc15) = skc15) % 32.98/33.19 (ifeq3(of(skc11, _0, skc10), true, ifeq3(forename(skc11, _0), true, ifeq3(entity(skc11, skc10), true, skc13, _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(of(skc11, _0, skc10), true, ifeq3(forename(skc11, _0), true, ifeq3(entity(skc11, skc10), true, skc15, _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(of(skc11, skc13, _0), true, ifeq3(of(skc11, skc13, _0), true, ifeq3(entity(skc11, _0), true, skc13, skc13), skc13), skc13) = skc13) % 32.98/33.19 (ifeq3(of(skc11, skc13, _0), true, ifeq3(of(skc11, _1, _0), true, ifeq3(forename(skc11, _1), true, ifeq3(entity(skc11, _0), true, skc13, _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(of(skc11, skc13, _0), true, ifeq3(of(skc11, skc15, _0), true, ifeq3(entity(skc11, _0), true, skc13, skc15), skc15), skc15) = skc15) % 32.98/33.19 (ifeq3(of(skc11, skc15, _0), true, ifeq3(of(skc11, skc13, _0), true, ifeq3(entity(skc11, _0), true, skc15, skc13), skc13), skc13) = skc13) % 32.98/33.19 (ifeq3(of(skc11, skc15, _0), true, ifeq3(of(skc11, _1, _0), true, ifeq3(forename(skc11, _1), true, ifeq3(entity(skc11, _0), true, skc15, _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(of(skc11, skc15, _0), true, ifeq3(of(skc11, skc15, _0), true, ifeq3(entity(skc11, _0), true, skc15, skc15), skc15), skc15) = skc15) % 32.98/33.19 (ifeq3(agent(skc8, skc12, _0), true, ifeq3(agent(skc8, skc12, _0), true, skc11, skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(agent(skc11, skc12, _0), true, ifeq3(agent(skc11, skc12, _0), true, skc11, skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(_0, _1, _2), true, ifeq3(theme(_0, _3, _4), true, ifeq3(agent(_0, _1, _5), true, ifeq3(agent(_0, _3, _5), true, ifeq3(think_believe_consider(_0, _1), true, ifeq3(think_believe_consider(_0, _3), true, ifeq3(proposition(_0, _2), true, ifeq3(proposition(_0, _4), true, _4, _2), _2), _2), _2), _2), _2), _2), _2) = _2) % 32.98/33.19 (ifeq3(theme(skc8, _0, _1), true, ifeq3(agent(skc8, _0, _2), true, ifeq3(agent(skc8, skc12, _2), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, skc11, _1), _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc8, _0, _1), true, ifeq3(agent(skc8, _0, skc14), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, _1, skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, _0, _1), true, ifeq3(agent(skc8, _0, skc14), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, skc11, _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc8, _0, _1), true, ifeq3(agent(skc8, _0, skc10), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, _1, skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, _0, _1), true, ifeq3(agent(skc8, _0, skc10), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, skc11, _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc8, _0, _1), true, ifeq3(agent(skc8, skc12, _2), true, ifeq3(agent(skc8, _0, _2), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, _1, skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, _0, _1), true, ifeq3(theme(skc8, _2, skc11), true, ifeq3(agent(skc8, _0, _3), true, ifeq3(agent(skc8, _2, _3), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(think_believe_consider(skc8, _2), true, ifeq3(proposition(skc8, _1), true, skc11, _1), _1), _1), _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc8, _0, _1), true, ifeq3(theme(skc8, skc12, _2), true, ifeq3(agent(skc8, _0, _3), true, ifeq3(agent(skc8, skc12, _3), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, ifeq3(proposition(skc8, _2), true, _2, _1), _1), _1), _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc8, _0, _1), true, ifeq3(theme(skc8, skc12, _2), true, ifeq3(agent(skc8, _0, skc14), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, ifeq3(proposition(skc8, _2), true, _2, _1), _1), _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc8, _0, _1), true, ifeq3(theme(skc8, skc12, _2), true, ifeq3(agent(skc8, _0, skc10), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, ifeq3(proposition(skc8, _2), true, _2, _1), _1), _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc8, _0, _1), true, ifeq3(theme(skc8, skc12, skc11), true, ifeq3(agent(skc8, _0, _2), true, ifeq3(agent(skc8, skc12, _2), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, skc11, _1), _1), _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc8, _0, skc11), true, ifeq3(agent(skc8, _0, _1), true, ifeq3(agent(skc8, skc12, _1), true, ifeq3(think_believe_consider(skc8, _0), true, skc11, skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, _0, skc11), true, ifeq3(agent(skc8, _0, skc10), true, ifeq3(think_believe_consider(skc8, _0), true, skc11, skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, _0, skc11), true, ifeq3(agent(skc8, skc12, _1), true, ifeq3(agent(skc8, _0, _1), true, ifeq3(think_believe_consider(skc8, _0), true, skc11, skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, _0, skc11), true, ifeq3(theme(skc8, _1, _2), true, ifeq3(agent(skc8, _0, _3), true, ifeq3(agent(skc8, _1, _3), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(think_believe_consider(skc8, _1), true, ifeq3(proposition(skc8, _2), true, _2, skc11), skc11), skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, _0, skc11), true, ifeq3(theme(skc8, _1, skc11), true, ifeq3(agent(skc8, _0, _2), true, ifeq3(agent(skc8, _1, _2), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(think_believe_consider(skc8, _1), true, skc11, skc11), skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, _0, skc11), true, ifeq3(theme(skc8, skc12, _1), true, ifeq3(agent(skc8, _0, _2), true, ifeq3(agent(skc8, skc12, _2), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, _1, skc11), skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, _0, skc11), true, ifeq3(theme(skc8, skc12, _1), true, ifeq3(agent(skc8, _0, skc14), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, _1, skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, _0, skc11), true, ifeq3(theme(skc8, skc12, _1), true, ifeq3(agent(skc8, _0, skc10), true, ifeq3(think_believe_consider(skc8, _0), true, ifeq3(proposition(skc8, _1), true, _1, skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, skc12, _0), true, ifeq3(agent(skc8, skc12, _1), true, ifeq3(agent(skc8, skc12, _1), true, ifeq3(proposition(skc8, _0), true, _0, skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, skc12, _0), true, ifeq3(agent(skc8, skc12, _1), true, ifeq3(agent(skc8, skc12, _1), true, ifeq3(proposition(skc8, _0), true, skc11, _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc8, skc12, _0), true, ifeq3(proposition(skc8, _0), true, _0, skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc8, skc12, _0), true, ifeq3(proposition(skc8, _0), true, skc11, _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc8, skc12, _0), true, ifeq3(theme(skc8, _1, _2), true, ifeq3(agent(skc8, _1, skc14), true, ifeq3(think_believe_consider(skc8, _1), true, ifeq3(proposition(skc8, _0), true, ifeq3(proposition(skc8, _2), true, _2, _0), _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc8, skc12, _0), true, ifeq3(theme(skc8, _1, _2), true, ifeq3(agent(skc8, _1, skc10), true, ifeq3(think_believe_consider(skc8, _1), true, ifeq3(proposition(skc8, _0), true, ifeq3(proposition(skc8, _2), true, _2, _0), _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc8, skc12, _0), true, ifeq3(theme(skc8, _1, _2), true, ifeq3(agent(skc8, skc12, _3), true, ifeq3(agent(skc8, _1, _3), true, ifeq3(think_believe_consider(skc8, _1), true, ifeq3(proposition(skc8, _0), true, ifeq3(proposition(skc8, _2), true, _2, _0), _0), _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc8, skc12, _0), true, ifeq3(theme(skc8, _1, skc11), true, ifeq3(agent(skc8, _1, skc14), true, ifeq3(think_believe_consider(skc8, _1), true, ifeq3(proposition(skc8, _0), true, skc11, _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc8, skc12, _0), true, ifeq3(theme(skc8, _1, skc11), true, ifeq3(agent(skc8, _1, skc10), true, ifeq3(think_believe_consider(skc8, _1), true, ifeq3(proposition(skc8, _0), true, skc11, _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc8, skc12, _0), true, ifeq3(theme(skc8, _1, skc11), true, ifeq3(agent(skc8, skc12, _2), true, ifeq3(agent(skc8, _1, _2), true, ifeq3(think_believe_consider(skc8, _1), true, ifeq3(proposition(skc8, _0), true, skc11, _0), _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc8, skc12, _0), true, ifeq3(theme(skc8, skc12, _1), true, ifeq3(agent(skc8, skc12, _2), true, ifeq3(agent(skc8, skc12, _2), true, ifeq3(proposition(skc8, _0), true, ifeq3(proposition(skc8, _1), true, _1, _0), _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc8, skc12, _0), true, ifeq3(theme(skc8, skc12, _1), true, ifeq3(proposition(skc8, _0), true, ifeq3(proposition(skc8, _1), true, _1, _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, _0, _1), true, ifeq3(agent(skc11, _0, _2), true, ifeq3(agent(skc11, skc12, _2), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(proposition(skc11, _1), true, skc11, _1), _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc11, _0, _1), true, ifeq3(agent(skc11, _0, skc10), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(proposition(skc11, _1), true, _1, skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, _0, _1), true, ifeq3(agent(skc11, _0, skc10), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(proposition(skc11, _1), true, skc11, _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc11, _0, _1), true, ifeq3(agent(skc11, skc12, _2), true, ifeq3(agent(skc11, _0, _2), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(proposition(skc11, _1), true, _1, skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, _0, _1), true, ifeq3(theme(skc11, _2, skc11), true, ifeq3(agent(skc11, _0, _3), true, ifeq3(agent(skc11, _2, _3), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(think_believe_consider(skc11, _2), true, ifeq3(proposition(skc11, _1), true, skc11, _1), _1), _1), _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc11, _0, _1), true, ifeq3(theme(skc11, skc12, _2), true, ifeq3(agent(skc11, _0, _3), true, ifeq3(agent(skc11, skc12, _3), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(proposition(skc11, _1), true, ifeq3(proposition(skc11, _2), true, _2, _1), _1), _1), _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc11, _0, _1), true, ifeq3(theme(skc11, skc12, _2), true, ifeq3(agent(skc11, _0, skc10), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(proposition(skc11, _1), true, ifeq3(proposition(skc11, _2), true, _2, _1), _1), _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc11, _0, _1), true, ifeq3(theme(skc11, skf1(skc10), _2), true, ifeq3(agent(skc11, _0, skc10), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, _1), true, ifeq3(proposition(skc11, _2), true, _2, _1), _1), _1), _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc11, _0, _1), true, ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(agent(skc11, _0, skc10), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, _1), true, skc11, _1), _1), _1), _1), _1), _1) = _1) % 32.98/33.19 (ifeq3(theme(skc11, _0, skc11), true, ifeq3(agent(skc11, _0, _1), true, ifeq3(agent(skc11, skc12, _1), true, ifeq3(think_believe_consider(skc11, _0), true, skc11, skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, _0, skc11), true, ifeq3(agent(skc11, _0, skc10), true, ifeq3(think_believe_consider(skc11, _0), true, skc11, skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, _0, skc11), true, ifeq3(agent(skc11, skc12, _1), true, ifeq3(agent(skc11, _0, _1), true, ifeq3(think_believe_consider(skc11, _0), true, skc11, skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, _0, skc11), true, ifeq3(theme(skc11, _1, _2), true, ifeq3(agent(skc11, _0, _3), true, ifeq3(agent(skc11, _1, _3), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(think_believe_consider(skc11, _1), true, ifeq3(proposition(skc11, _2), true, _2, skc11), skc11), skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, _0, skc11), true, ifeq3(theme(skc11, _1, skc11), true, ifeq3(agent(skc11, _0, _2), true, ifeq3(agent(skc11, _1, _2), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(think_believe_consider(skc11, _1), true, skc11, skc11), skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, _0, skc11), true, ifeq3(theme(skc11, skc12, _1), true, ifeq3(agent(skc11, _0, _2), true, ifeq3(agent(skc11, skc12, _2), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(proposition(skc11, _1), true, _1, skc11), skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, _0, skc11), true, ifeq3(theme(skc11, skc12, _1), true, ifeq3(agent(skc11, _0, skc10), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(proposition(skc11, _1), true, _1, skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, _0, skc11), true, ifeq3(theme(skc11, skf1(skc10), _1), true, ifeq3(agent(skc11, _0, skc10), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, _1), true, _1, skc11), skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, _0, skc11), true, ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(agent(skc11, _0, skc10), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, skc11, skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, skc12, _0), true, ifeq3(agent(skc11, skc12, _1), true, ifeq3(agent(skc11, skc12, _1), true, ifeq3(proposition(skc11, _0), true, _0, skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, skc12, _0), true, ifeq3(agent(skc11, skc12, _1), true, ifeq3(agent(skc11, skc12, _1), true, ifeq3(proposition(skc11, _0), true, skc11, _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skc12, _0), true, ifeq3(theme(skc11, _1, _2), true, ifeq3(agent(skc11, _1, skc10), true, ifeq3(think_believe_consider(skc11, _1), true, ifeq3(proposition(skc11, _0), true, ifeq3(proposition(skc11, _2), true, _2, _0), _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skc12, _0), true, ifeq3(theme(skc11, _1, _2), true, ifeq3(agent(skc11, skc12, _3), true, ifeq3(agent(skc11, _1, _3), true, ifeq3(think_believe_consider(skc11, _1), true, ifeq3(proposition(skc11, _0), true, ifeq3(proposition(skc11, _2), true, _2, _0), _0), _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skc12, _0), true, ifeq3(theme(skc11, _1, skc11), true, ifeq3(agent(skc11, _1, skc10), true, ifeq3(think_believe_consider(skc11, _1), true, ifeq3(proposition(skc11, _0), true, skc11, _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skc12, _0), true, ifeq3(theme(skc11, _1, skc11), true, ifeq3(agent(skc11, skc12, _2), true, ifeq3(agent(skc11, _1, _2), true, ifeq3(think_believe_consider(skc11, _1), true, ifeq3(proposition(skc11, _0), true, skc11, _0), _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skc12, _0), true, ifeq3(theme(skc11, skc12, _1), true, ifeq3(agent(skc11, skc12, _2), true, ifeq3(agent(skc11, skc12, _2), true, ifeq3(proposition(skc11, _0), true, ifeq3(proposition(skc11, _1), true, _1, _0), _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skc12, _0), true, ifeq3(theme(skc11, skc12, _1), true, ifeq3(proposition(skc11, _0), true, ifeq3(proposition(skc11, _1), true, _1, _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skc12, _0), true, ifeq3(theme(skc11, skf1(skc10), _1), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, _0), true, ifeq3(proposition(skc11, _1), true, _1, _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skc12, _0), true, ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, _0), true, skc11, _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skc12, _0), true, ifeq3(proposition(skc11, _0), true, _0, skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, skc12, _0), true, ifeq3(proposition(skc11, _0), true, skc11, _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), _0), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, _0), true, _0, skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), _0), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, _0), true, skc11, _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), _0), true, ifeq3(theme(skc11, _1, _2), true, ifeq3(agent(skc11, _1, skc10), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, _1), true, ifeq3(proposition(skc11, _0), true, ifeq3(proposition(skc11, _2), true, _2, _0), _0), _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), _0), true, ifeq3(theme(skc11, _1, skc11), true, ifeq3(agent(skc11, _1, skc10), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, _1), true, ifeq3(proposition(skc11, _0), true, skc11, _0), _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), _0), true, ifeq3(theme(skc11, skc12, _1), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, _0), true, ifeq3(proposition(skc11, _1), true, _1, _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), _0), true, ifeq3(theme(skc11, skf1(skc10), _1), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, _0), true, ifeq3(proposition(skc11, _1), true, _1, _0), _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), _0), true, ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, _0), true, skc11, _0), _0), _0), _0), _0) = _0) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, skc11, skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(theme(skc11, _0, _1), true, ifeq3(agent(skc11, _0, skc10), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, _0), true, ifeq3(proposition(skc11, _1), true, _1, skc11), skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(theme(skc11, _0, skc11), true, ifeq3(agent(skc11, _0, skc10), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, _0), true, skc11, skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(theme(skc11, skc12, _0), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, _0), true, _0, skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(theme(skc11, skf1(skc10), _0), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(proposition(skc11, _0), true, _0, skc11), skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(theme(skc11, skf1(skc10), skc11), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, ifeq3(think_believe_consider(skc11, skf1(skc10)), true, skc11, skc11), skc11), skc11), skc11) = skc11) % 32.98/33.19 (human(skc8, skc10) = true) % 32.98/33.19 (human(skc11, skc10) = true) % 32.98/33.19 (agent(skc8, skc12, skc14) = true) % 32.98/33.19 (agent(skc8, skc12, skc10) = true) % 32.98/33.19 (agent(skc11, skc12, skc14) = true) % 32.98/33.19 (agent(skc11, skc12, skc10) = true) % 32.98/33.19 (agent(skc11, skf1(skc10), skc10) = true) % 32.98/33.19 (ifeq2(forename(_0, _1), true, relname(_0, _1), true) = true) % 32.98/33.19 (ifeq2(forename(skc8, _0), true, forename(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(_0, _0, _1, _2) = _1) % 32.98/33.19 (ifeq2(eventuality(_0, _1), true, specific(_0, _1), true) = true) % 32.98/33.19 (ifeq2(eventuality(_0, _1), true, nonexistent(_0, _1), true) = true) % 32.98/33.19 (ifeq2(eventuality(_0, _1), true, thing(_0, _1), true) = true) % 32.98/33.19 (ifeq2(eventuality(_0, _1), true, unisex(_0, _1), true) = true) % 32.98/33.19 (ifeq2(eventuality(skc8, _0), true, eventuality(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(eventuality(skc8, skc13), true, true, true) = true) % 32.98/33.19 (ifeq2(eventuality(skc8, skf1(_0)), true, true, true) = true) % 32.98/33.19 (ifeq2(eventuality(skc8, skc11), true, true, true) = true) % 32.98/33.19 (ifeq2(eventuality(skc8, skc10), true, true, true) = true) % 32.98/33.19 (ifeq2(eventuality(skc11, skc13), true, true, true) = true) % 32.98/33.19 (ifeq2(eventuality(skc11, skc11), true, true, true) = true) % 32.98/33.19 (ifeq2(eventuality(skc11, skc10), true, true, true) = true) % 32.98/33.19 (ifeq2(relname(_0, _1), true, relation(_0, _1), true) = true) % 32.98/33.19 (ifeq2(relname(skc8, _0), true, relname(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(relname(skc8, skc11), true, true, true) = true) % 32.98/33.19 (ifeq2(relname(skc11, skc11), true, true, true) = true) % 32.98/33.19 (ifeq2(thing(_0, _1), true, singleton(_0, _1), true) = true) % 32.98/33.19 (ifeq2(thing(skc8, _0), true, thing(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(thing(skc8, skf1(_0)), true, true, true) = true) % 32.98/33.19 (ifeq2(relation(_0, _1), true, abstraction(_0, _1), true) = true) % 32.98/33.19 (ifeq2(relation(skc8, _0), true, relation(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(singleton(skc8, _0), true, singleton(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(singleton(skc8, skf1(_0)), true, true, true) = true) % 32.98/33.19 (ifeq2(abstraction(_0, _1), true, general(_0, _1), true) = true) % 32.98/33.19 (ifeq2(abstraction(_0, _1), true, thing(_0, _1), true) = true) % 32.98/33.19 (ifeq2(abstraction(_0, _1), true, nonhuman(_0, _1), true) = true) % 32.98/33.19 (ifeq2(abstraction(_0, _1), true, unisex(_0, _1), true) = true) % 32.98/33.19 (ifeq2(abstraction(skc8, _0), true, abstraction(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(abstraction(skc8, skc9), true, true, true) = true) % 32.98/33.19 (ifeq2(abstraction(skc8, skc12), true, true, true) = true) % 32.98/33.19 (ifeq2(abstraction(skc8, skc10), true, true, true) = true) % 32.98/33.19 (ifeq2(abstraction(skc11, skc9), true, true, true) = true) % 32.98/33.19 (ifeq2(abstraction(skc11, skc12), true, true, true) = true) % 32.98/33.19 (ifeq2(abstraction(skc11, skf1(_0)), true, true, true) = true) % 32.98/33.19 (ifeq2(abstraction(skc11, skc10), true, true, true) = true) % 32.98/33.19 (ifeq2(specific(skc8, _0), true, specific(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(specific(skc8, skf1(_0)), true, true, true) = true) % 32.98/33.19 (ifeq2(nonhuman(skc8, _0), true, nonhuman(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(nonexistent(skc8, _0), true, nonexistent(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(nonexistent(skc8, skf1(_0)), true, true, true) = true) % 32.98/33.19 (ifeq2(general(skc8, _0), true, general(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(unisex(skc8, _0), true, unisex(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(unisex(skc8, skf1(_0)), true, true, true) = true) % 32.98/33.19 (ifeq2(jules_forename(_0, _1), true, forename(_0, _1), true) = true) % 32.98/33.19 (ifeq2(jules_forename(skc8, skc13), true, true, true) = true) % 32.98/33.19 (ifeq2(jules_forename(skc8, _0), true, jules_forename(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(jules_forename(skc11, skc13), true, true, true) = true) % 32.98/33.19 (ifeq2(event(_0, _1), true, eventuality(_0, _1), true) = true) % 32.98/33.19 (ifeq2(event(skc8, _0), true, event(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(event(skc8, skf1(_0)), true, true, true) = true) % 32.98/33.19 (ifeq2(smoke(_0, _1), true, event(_0, _1), true) = true) % 32.98/33.19 (ifeq2(smoke(skc8, _0), true, smoke(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(smoke(skc8, skc9), true, true, true) = true) % 32.98/33.19 (ifeq2(smoke(skc8, skc12), true, true, true) = true) % 32.98/33.19 (ifeq2(smoke(skc8, skf1(_0)), true, true, true) = true) % 32.98/33.19 (ifeq2(smoke(skc11, skc9), true, true, true) = true) % 32.98/33.19 (ifeq2(smoke(skc11, skc12), true, true, true) = true) % 32.98/33.19 (ifeq2(man(_0, _1), true, human_person(_0, _1), true) = true) % 32.98/33.19 (ifeq2(man(_0, _1), true, male(_0, _1), true) = true) % 32.98/33.19 (ifeq2(man(skc8, _0), true, man(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(man(skc11, _0), true, event(skc11, skf1(_1)), true) = true) % 32.98/33.19 (ifeq2(man(skc11, _0), true, smoke(skc11, skf1(_1)), true) = true) % 32.98/33.19 (ifeq2(man(skc11, _0), true, agent(skc11, skf1(_0), _0), true) = true) % 32.98/33.19 (ifeq2(man(skc11, _0), true, true, true) = true) % 32.98/33.19 (ifeq2(man(skc11, _0), true, present(skc11, skf1(_1)), true) = true) % 32.98/33.19 (ifeq2(proposition(_0, _1), true, relation(_0, _1), true) = true) % 32.98/33.19 (ifeq2(proposition(skc8, _0), true, proposition(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(proposition(skc8, skc13), true, true, true) = true) % 32.98/33.19 (ifeq2(proposition(skc8, skc15), true, true, true) = true) % 32.98/33.19 (ifeq2(proposition(skc11, skc13), true, true, true) = true) % 32.98/33.19 (ifeq2(proposition(skc11, skc15), true, true, true) = true) % 32.98/33.19 (ifeq2(human_person(_0, _1), true, human(_0, _1), true) = true) % 32.98/33.19 (ifeq2(human_person(_0, _1), true, animate(_0, _1), true) = true) % 32.98/33.19 (ifeq2(human_person(_0, _1), true, organism(_0, _1), true) = true) % 32.98/33.19 (ifeq2(human_person(skc8, _0), true, human_person(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(vincent_forename(_0, _1), true, forename(_0, _1), true) = true) % 32.98/33.19 (ifeq2(vincent_forename(skc8, _0), true, vincent_forename(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(vincent_forename(skc8, skc15), true, true, true) = true) % 32.98/33.19 (ifeq2(vincent_forename(skc11, skc15), true, true, true) = true) % 32.98/33.19 (ifeq2(organism(_0, _1), true, entity(_0, _1), true) = true) % 32.98/33.19 (ifeq2(organism(_0, _1), true, impartial(_0, _1), true) = true) % 32.98/33.19 (ifeq2(organism(_0, _1), true, living(_0, _1), true) = true) % 32.98/33.19 (ifeq2(organism(skc8, _0), true, organism(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(be(_0, _1, _2, _3), true, ifeq2(accessible_world(_0, _4), true, be(_4, _1, _2, _3), true), true) = true) % 32.98/33.19 (ifeq2(be(_0, skc9, skc14, skc10), true, ifeq2(accessible_world(_0, skc8), true, true, true), true) = true) % 32.98/33.19 (ifeq2(be(_0, skc9, skc10, skc10), true, ifeq2(accessible_world(_0, skc8), true, true, true), true) = true) % 32.98/33.19 (ifeq2(be(_0, skc9, skc10, skc10), true, ifeq2(accessible_world(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(be(skc8, _0, _1, _2), true, be(skc11, _0, _1, _2), true) = true) % 32.98/33.19 (ifeq2(entity(_0, _1), true, specific(_0, _1), true) = true) % 32.98/33.19 (ifeq2(entity(_0, _1), true, existent(_0, _1), true) = true) % 32.98/33.19 (ifeq2(entity(_0, _1), true, thing(_0, _1), true) = true) % 32.98/33.19 (ifeq2(entity(skc8, _0), true, entity(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(entity(skc8, skc9), true, true, true) = true) % 32.98/33.19 (ifeq2(entity(skc8, skc13), true, true, true) = true) % 32.98/33.19 (ifeq2(entity(skc8, skc12), true, true, true) = true) % 32.98/33.19 (ifeq2(entity(skc8, skc11), true, true, true) = true) % 32.98/33.19 (ifeq2(entity(skc11, skc9), true, true, true) = true) % 32.98/33.19 (ifeq2(entity(skc11, skc13), true, true, true) = true) % 32.98/33.19 (ifeq2(entity(skc11, skc12), true, true, true) = true) % 32.98/33.19 (ifeq2(entity(skc11, skf1(_0)), true, true, true) = true) % 32.98/33.19 (ifeq2(entity(skc11, skc11), true, true, true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(male(_0, _2), true, male(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(state(_0, _2), true, state(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(proposition(_0, _2), true, proposition(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(human_person(_0, _2), true, human_person(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(forename(_0, _2), true, forename(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(eventuality(_0, _2), true, eventuality(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(organism(_0, _2), true, organism(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(vincent_forename(_0, _2), true, vincent_forename(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(thing(_0, _2), true, thing(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(relname(_0, _2), true, relname(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(entity(_0, _2), true, entity(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(relation(_0, _2), true, relation(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(singleton(_0, _2), true, singleton(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(existent(_0, _2), true, existent(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(abstraction(_0, _2), true, abstraction(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(specific(_0, _2), true, specific(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(impartial(_0, _2), true, impartial(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(nonexistent(_0, _2), true, nonexistent(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(nonhuman(_0, _2), true, nonhuman(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(living(_0, _2), true, living(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(unisex(_0, _2), true, unisex(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(general(_0, _2), true, general(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(human(_0, _2), true, human(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(event(_0, _2), true, event(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(jules_forename(_0, _2), true, jules_forename(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(animate(_0, _2), true, animate(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(man(_0, _2), true, man(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, _1), true, ifeq2(smoke(_0, _2), true, smoke(_1, _2), true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(male(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(state(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(proposition(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(human_person(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(forename(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(forename(_0, skc15), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(eventuality(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(eventuality(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(organism(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(vincent_forename(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(thing(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(thing(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(thing(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(thing(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(thing(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(relname(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(relname(_0, skc15), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(entity(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(relation(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(relation(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(relation(_0, skc15), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(singleton(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(singleton(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(singleton(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(singleton(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(singleton(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(existent(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(abstraction(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(abstraction(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(abstraction(_0, skc15), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(specific(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(specific(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(specific(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(impartial(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(nonexistent(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(nonexistent(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(nonhuman(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(nonhuman(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(living(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(unisex(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(unisex(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(unisex(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(unisex(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(general(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(general(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(human(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(event(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(event(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(jules_forename(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(jules_forename(_0, skc15), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(animate(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(man(_0, skc14), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc8), true, ifeq2(man(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(male(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(state(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(proposition(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(human_person(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(forename(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(forename(_0, skc15), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(eventuality(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(eventuality(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(eventuality(_0, skf1(_1)), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(organism(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(vincent_forename(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(thing(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(thing(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(thing(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(thing(_0, skf1(_1)), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(thing(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(thing(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(relname(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(relname(_0, skc15), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(entity(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(relation(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(relation(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(relation(_0, skc15), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(singleton(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(singleton(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(singleton(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(singleton(_0, skf1(_1)), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(singleton(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(singleton(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(existent(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(abstraction(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(abstraction(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(specific(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(specific(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(specific(_0, skf1(_1)), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(specific(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(impartial(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(nonexistent(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(nonexistent(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(nonexistent(_0, skf1(_1)), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(nonhuman(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(nonhuman(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(living(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(unisex(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(unisex(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(unisex(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(unisex(_0, skf1(_1)), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(unisex(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(general(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(general(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(human(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(event(_0, skc9), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(event(_0, skc12), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(event(_0, skf1(_1)), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(jules_forename(_0, skc13), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(jules_forename(_0, skc15), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(animate(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(man(_0, skc10), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(_0, skc11), true, ifeq2(smoke(_0, skf1(_1)), true, true, true), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, theme(_0, skc12, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, male(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, state(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, proposition(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, human_person(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, forename(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, forename(_0, skc15), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, eventuality(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, eventuality(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, organism(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, vincent_forename(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, thing(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, thing(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, thing(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, thing(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, thing(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, relname(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, relname(_0, skc15), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, be(_0, skc9, skc14, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, be(_0, skc9, skc10, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, entity(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, relation(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, relation(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, relation(_0, skc15), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, singleton(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, singleton(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, singleton(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, singleton(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, singleton(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, existent(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, specific(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, specific(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, specific(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, abstraction(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, abstraction(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, abstraction(_0, skc15), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, present(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, impartial(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, nonexistent(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, nonexistent(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, nonhuman(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, nonhuman(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, think_believe_consider(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, living(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, unisex(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, unisex(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, unisex(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, unisex(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, general(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, general(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, of(_0, skc13, skc14), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, of(_0, skc13, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, of(_0, skc15, skc14), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, of(_0, skc15, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, human(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, event(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, event(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, jules_forename(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, jules_forename(_0, skc15), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, agent(_0, skc12, skc14), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, agent(_0, skc12, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, animate(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, man(_0, skc14), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, _0), true, man(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc8, skc8), true, true, true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, theme(_0, skc12, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, male(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, state(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, proposition(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, human_person(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, forename(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, forename(_0, skc15), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, eventuality(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, eventuality(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, eventuality(_0, skf1(_1)), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, organism(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, vincent_forename(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, thing(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, thing(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, thing(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, thing(_0, skf1(_1)), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, thing(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, thing(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, relname(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, relname(_0, skc15), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, be(_0, skc9, skc10, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, entity(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, relation(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, relation(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, relation(_0, skc15), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, singleton(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, singleton(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, singleton(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, singleton(_0, skf1(_1)), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, singleton(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, singleton(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, existent(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, specific(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, specific(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, specific(_0, skf1(_1)), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, specific(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, abstraction(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, abstraction(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, present(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, present(_0, skf1(_1)), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, impartial(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, nonexistent(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, nonexistent(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, nonexistent(_0, skf1(_1)), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, nonhuman(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, nonhuman(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, think_believe_consider(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, living(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, unisex(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, unisex(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, unisex(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, unisex(_0, skf1(_1)), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, unisex(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, general(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, general(_0, skc11), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, of(_0, skc13, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, of(_0, skc15, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, human(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, event(_0, skc9), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, event(_0, skc12), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, event(_0, skf1(_1)), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, jules_forename(_0, skc13), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, jules_forename(_0, skc15), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, agent(_0, skc12, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, agent(_0, skf1(skc10), skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, animate(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, man(_0, skc10), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, _0), true, smoke(_0, skf1(_1)), true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, skc8), true, true, true) = true) % 32.98/33.19 (ifeq2(accessible_world(skc11, skc11), true, true, true) = true) % 32.98/33.19 (ifeq2(existent(skc8, _0), true, existent(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(present(_0, _1), true, ifeq2(accessible_world(_0, _2), true, present(_2, _1), true), true) = true) % 32.98/33.19 (ifeq2(present(_0, skc12), true, ifeq2(accessible_world(_0, skc8), true, true, true), true) = true) % 32.98/33.19 (ifeq2(present(_0, skc12), true, ifeq2(accessible_world(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(present(_0, skf1(_1)), true, ifeq2(accessible_world(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(present(skc8, _0), true, present(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(present(skc8, skf1(_0)), true, true, true) = true) % 32.98/33.19 (ifeq2(impartial(skc8, _0), true, impartial(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(think_believe_consider(_0, _1), true, ifeq2(accessible_world(_0, _2), true, think_believe_consider(_2, _1), true), true) = true) % 32.98/33.19 (ifeq2(think_believe_consider(_0, skc12), true, ifeq2(accessible_world(_0, skc8), true, true, true), true) = true) % 32.98/33.19 (ifeq2(think_believe_consider(_0, skc12), true, ifeq2(accessible_world(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(think_believe_consider(skc8, _0), true, think_believe_consider(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(living(skc8, _0), true, living(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(of(_0, _1, _2), true, ifeq2(accessible_world(_0, _3), true, of(_3, _1, _2), true), true) = true) % 32.98/33.19 (ifeq2(of(_0, skc13, skc14), true, ifeq2(accessible_world(_0, skc8), true, true, true), true) = true) % 32.98/33.19 (ifeq2(of(_0, skc13, skc10), true, ifeq2(accessible_world(_0, skc8), true, true, true), true) = true) % 32.98/33.19 (ifeq2(of(_0, skc13, skc10), true, ifeq2(accessible_world(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(of(_0, skc15, skc14), true, ifeq2(accessible_world(_0, skc8), true, true, true), true) = true) % 32.98/33.19 (ifeq2(of(_0, skc15, skc10), true, ifeq2(accessible_world(_0, skc8), true, true, true), true) = true) % 32.98/33.19 (ifeq2(of(_0, skc15, skc10), true, ifeq2(accessible_world(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(of(skc8, _0, _1), true, of(skc11, _0, _1), true) = true) % 32.98/33.19 (ifeq2(human(skc8, _0), true, human(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(agent(_0, _1, _2), true, ifeq2(accessible_world(_0, _3), true, agent(_3, _1, _2), true), true) = true) % 32.98/33.19 (ifeq2(agent(_0, skc12, skc14), true, ifeq2(accessible_world(_0, skc8), true, true, true), true) = true) % 32.98/33.19 (ifeq2(agent(_0, skc12, skc10), true, ifeq2(accessible_world(_0, skc8), true, true, true), true) = true) % 32.98/33.19 (ifeq2(agent(_0, skc12, skc10), true, ifeq2(accessible_world(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(agent(_0, skf1(skc10), skc10), true, ifeq2(accessible_world(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(agent(skc8, _0, _1), true, agent(skc11, _0, _1), true) = true) % 32.98/33.19 (ifeq2(agent(skc8, skf1(skc10), skc10), true, true, true) = true) % 32.98/33.19 (ifeq2(animate(skc8, _0), true, animate(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(theme(_0, _1, _2), true, ifeq2(accessible_world(_0, _3), true, theme(_3, _1, _2), true), true) = true) % 32.98/33.19 (ifeq2(theme(_0, skc12, skc11), true, ifeq2(accessible_world(_0, skc8), true, true, true), true) = true) % 32.98/33.19 (ifeq2(theme(_0, skc12, skc11), true, ifeq2(accessible_world(_0, skc11), true, true, true), true) = true) % 32.98/33.19 (ifeq2(theme(skc8, _0, _1), true, theme(skc11, _0, _1), true) = true) % 32.98/33.19 (ifeq2(male(skc8, _0), true, male(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(state(_0, _1), true, event(_0, _1), true) = true) % 32.98/33.19 (ifeq2(state(_0, _1), true, eventuality(_0, _1), true) = true) % 32.98/33.19 (ifeq2(state(skc8, _0), true, state(skc11, _0), true) = true) % 32.98/33.19 (ifeq2(state(skc8, skc12), true, true, true) = true) % 32.98/33.19 (ifeq2(state(skc11, skc12), true, true, true) = true) % 32.98/33.19 (ifeq2(state(skc11, skf1(_0)), true, true, true) = true) % 32.98/33.19 (animate(skc8, skc10) = true) % 32.98/33.19 (animate(skc11, skc10) = true) % 32.98/33.19 (theme(skc8, skc12, skc11) = true) % 32.98/33.19 (theme(skc11, skc12, skc11) = true) % 32.98/33.19 (ifeq(_0, _0, _1, _2) = _1) % 32.98/33.19 (ifeq(tuple(human(_0, _1), nonhuman(_0, _1)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(human(skc8, skc13), true), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(human(skc8, skc11), true), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(human(skc11, skc13), true), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(human(skc11, skc11), true), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(specific(_0, _1), general(_0, _1)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(specific(skc8, skc13), true), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(specific(skc8, skc11), true), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(specific(skc11, skc13), true), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(specific(skc11, skc11), true), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(nonexistent(_0, _1), existent(_0, _1)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(nonexistent(skc8, skc10), true), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(nonexistent(skc11, skc10), true), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, general(skc8, skc9)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, general(skc8, skc12)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, general(skc8, skc10)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, general(skc11, skc9)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, general(skc11, skc12)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, general(skc11, skf1(_0))), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, general(skc11, skc10)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, existent(skc8, skc9)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, existent(skc8, skc12)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, existent(skc11, skc9)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, existent(skc11, skc12)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, existent(skc11, skf1(_0))), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, male(skc8, skc9)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, male(skc8, skc13)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, male(skc8, skc12)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, male(skc8, skc11)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, male(skc11, skc9)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, male(skc11, skc13)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, male(skc11, skc12)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, male(skc11, skf1(_0))), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, male(skc11, skc11)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, nonhuman(skc8, skc10)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(true, nonhuman(skc11, skc10)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(unisex(_0, _1), male(_0, _1)), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(unisex(skc8, skc10), true), tuple(true, true), a, b) = b) % 32.98/33.19 (ifeq(tuple(unisex(skc11, skc10), true), tuple(true, true), a, b) = b) % 32.98/33.19 (male(skc8, skc14) = true) % 32.98/33.19 (male(skc8, skc10) = true) % 32.98/33.19 (male(skc11, skc10) = true) % 32.98/33.19 (state(skc8, skc9) = true) % 32.98/33.19 (state(skc11, skc9) = true) % 32.98/33.19 (actual_world(skc8) = true) % 32.98/33.19 END OF MODEL %------------------------------------------------------------------------------