Toma---0.7.SAT-Ass.s

%------------------------------------------------------------------------------
% File     : Toma---0.7
% Problem  : NLP024-10 : TPTP v9.0.0. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_Leo-III %s %d THM

% Computer : n010.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  : 300s
% DateTime : Tue Jul 15 07:23:33 AM UTC 2025

% Result   : Satisfiable 16.86s 15.98s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : NLP024-10 : TPTP v9.0.0. Released v7.5.0.
% 0.03/0.13  % Command  : run_Leo-III %s %d THM
% 0.13/0.34  % Computer : n010.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Mon Jul 14 14:10:49 EDT 2025
% 0.13/0.34  % CPUTime  : 
% 16.86/15.98  % SZS status Satisfiable
% 16.86/15.98  The following TRS is a complete presentation of the axioms, but the goal is not joinable.
% 16.86/15.98  1: actual_world(skc8) -> true
% 16.86/15.98  2: man(skc8, skc15) -> true
% 16.86/15.98  3: event(skc10, skc13) -> true
% 16.86/15.98  4: woman(skc8, skc12) -> true
% 16.86/15.98  5: present(skc10, skc13) -> true
% 16.86/15.98  6: dance(skc10, skc13) -> true
% 16.86/15.98  7: forename(skc8, skc11) -> true
% 16.86/15.98  8: mia_forename(skc8, skc11) -> true
% 16.86/15.98  9: proposition(skc8, skc10) -> true
% 16.86/15.98  10: accessible_world(skc8, skc10) -> true
% 16.86/15.98  11: desire_want(skc8, skc9) -> true
% 16.86/15.98  12: present(skc8, skc9) -> true
% 16.86/15.98  13: forename(skc8, skc14) -> true
% 16.86/15.98  14: vincent_forename(skc8, skc14) -> true
% 16.86/15.98  15: of(skc8, skc14, skc15) -> true
% 16.86/15.98  16: of(skc8, skc11, skc12) -> true
% 16.86/15.98  17: agent(skc8, skc9, skc12) -> true
% 16.86/15.98  18: agent(skc10, skc13, skc12) -> true
% 16.86/15.98  19: theme(skc8, skc9, skc10) -> true
% 16.86/15.98  20: ifeq4(X, X, Y, Z) -> Y
% 16.86/15.98  21: ifeq3(X, X, Y, Z) -> Y
% 16.86/15.98  22: ifeq(X, X, Y, Z) -> Y
% 16.86/15.98  23: ifeq2(X, X, Y, Z) -> Y
% 16.86/15.98  24: ifeq3(dance(X, Y), true, event(X, Y), true) -> true
% 16.86/15.98  25: ifeq3(event(X, Y), true, eventuality(X, Y), true) -> true
% 16.86/15.98  26: eventuality(skc10, skc13) -> true
% 16.86/15.98  27: ifeq3(thing(X, Y), true, singleton(X, Y), true) -> true
% 16.86/15.98  28: ifeq3(eventuality(X, Y), true, thing(X, Y), true) -> true
% 16.86/15.98  29: thing(skc10, skc13) -> true
% 16.86/15.98  30: singleton(skc10, skc13) -> true
% 16.86/15.98  31: ifeq3(eventuality(X, Y), true, specific(X, Y), true) -> true
% 16.86/15.98  32: specific(skc10, skc13) -> true
% 16.86/15.98  33: ifeq3(eventuality(X, Y), true, nonexistent(X, Y), true) -> true
% 16.86/15.98  34: nonexistent(skc10, skc13) -> true
% 16.86/15.98  35: ifeq3(abstraction(X, Y), true, thing(X, Y), true) -> true
% 16.86/15.98  36: ifeq3(relation(X, Y), true, abstraction(X, Y), true) -> true
% 16.86/15.98  37: ifeq3(eventuality(X, Y), true, unisex(X, Y), true) -> true
% 16.86/15.98  38: unisex(skc10, skc13) -> true
% 16.86/15.98  39: ifeq3(desire_want(X, Y), true, event(X, Y), true) -> true
% 16.86/15.98  40: event(skc8, skc9) -> true
% 16.86/15.98  41: eventuality(skc8, skc9) -> true
% 16.86/15.98  42: unisex(skc8, skc9) -> true
% 16.86/15.98  43: nonexistent(skc8, skc9) -> true
% 16.86/15.98  44: specific(skc8, skc9) -> true
% 16.86/15.98  45: thing(skc8, skc9) -> true
% 16.86/15.98  46: singleton(skc8, skc9) -> true
% 16.86/15.98  47: ifeq3(desire_want(skc10, skc13), true, true, true) -> true
% 16.86/15.98  48: ifeq3(dance(skc8, skc9), true, true, true) -> true
% 16.86/15.98  49: ifeq3(proposition(X, Y), true, relation(X, Y), true) -> true
% 16.86/15.98  50: relation(skc8, skc10) -> true
% 16.86/15.98  51: abstraction(skc8, skc10) -> true
% 16.86/15.98  52: thing(skc8, skc10) -> true
% 16.86/15.98  53: singleton(skc8, skc10) -> true
% 16.86/15.98  54: ifeq3(abstraction(X, Y), true, nonhuman(X, Y), true) -> true
% 16.86/15.98  55: nonhuman(skc8, skc10) -> true
% 16.86/15.98  56: ifeq3(abstraction(X, Y), true, unisex(X, Y), true) -> true
% 16.86/15.98  57: unisex(skc8, skc10) -> true
% 16.86/15.98  58: ifeq3(abstraction(X, Y), true, general(X, Y), true) -> true
% 16.86/15.98  59: general(skc8, skc10) -> true
% 16.86/15.98  60: ifeq3(forename(X, Y), true, relname(X, Y), true) -> true
% 16.86/15.98  61: relname(skc8, skc11) -> true
% 16.86/15.98  62: relname(skc8, skc14) -> true
% 16.86/15.98  63: ifeq3(woman(X, Y), true, human_person(X, Y), true) -> true
% 16.86/15.98  64: human_person(skc8, skc12) -> true
% 16.86/15.98  65: ifeq3(relname(X, Y), true, relation(X, Y), true) -> true
% 16.86/15.98  66: relation(skc8, skc11) -> true
% 16.86/15.98  67: relation(skc8, skc14) -> true
% 16.86/15.98  68: abstraction(skc8, skc14) -> true
% 16.86/15.98  69: abstraction(skc8, skc11) -> true
% 16.86/15.98  70: general(skc8, skc11) -> true
% 16.86/15.98  71: unisex(skc8, skc11) -> true
% 16.86/15.98  72: nonhuman(skc8, skc11) -> true
% 16.86/15.98  73: thing(skc8, skc11) -> true
% 16.86/15.98  74: general(skc8, skc14) -> true
% 16.86/15.98  75: thing(skc8, skc14) -> true
% 16.86/15.98  76: unisex(skc8, skc14) -> true
% 16.86/15.98  77: nonhuman(skc8, skc14) -> true
% 16.86/15.98  78: singleton(skc8, skc14) -> true
% 16.86/15.98  79: singleton(skc8, skc11) -> true
% 16.86/15.98  80: ifeq3(relname(skc8, skc10), true, true, true) -> true
% 16.86/15.98  81: ifeq3(mia_forename(X, Y), true, forename(X, Y), true) -> true
% 16.86/15.98  82: ifeq3(mia_forename(skc8, skc14), true, true, true) -> true
% 16.86/15.98  83: ifeq3(human_person(X, Y), true, organism(X, Y), true) -> true
% 16.86/15.98  84: organism(skc8, skc12) -> true
% 16.86/15.98  85: ifeq3(entity(X, Y), true, thing(X, Y), true) -> true
% 16.86/15.98  86: ifeq3(organism(X, Y), true, entity(X, Y), true) -> true
% 16.86/15.98  87: entity(skc8, skc12) -> true
% 16.86/15.98  88: thing(skc8, skc12) -> true
% 16.86/15.98  89: singleton(skc8, skc12) -> true
% 16.86/15.98  90: ifeq3(entity(X, Y), true, specific(X, Y), true) -> true
% 16.86/15.98  91: specific(skc8, skc12) -> true
% 16.86/15.98  92: ifeq3(human_person(X, Y), true, human(X, Y), true) -> true
% 16.86/15.98  93: human(skc8, skc12) -> true
% 16.86/15.98  94: ifeq3(organism(X, Y), true, living(X, Y), true) -> true
% 16.86/15.98  95: living(skc8, skc12) -> true
% 16.86/15.98  96: ifeq3(entity(X, Y), true, existent(X, Y), true) -> true
% 16.86/15.98  97: existent(skc8, skc12) -> true
% 16.86/15.98  98: ifeq3(organism(X, Y), true, impartial(X, Y), true) -> true
% 16.86/15.98  99: impartial(skc8, skc12) -> true
% 16.86/15.98  100: ifeq3(human_person(X, Y), true, animate(X, Y), true) -> true
% 16.86/15.98  101: animate(skc8, skc12) -> true
% 16.86/15.98  102: ifeq3(vincent_forename(X, Y), true, forename(X, Y), true) -> true
% 16.86/15.98  103: ifeq3(vincent_forename(skc8, skc11), true, true, true) -> true
% 16.86/15.98  104: ifeq3(woman(X, Y), true, female(X, Y), true) -> true
% 16.86/15.98  105: female(skc8, skc12) -> true
% 16.86/15.98  106: ifeq3(man(X, Y), true, human_person(X, Y), true) -> true
% 16.86/15.98  107: human_person(skc8, skc15) -> true
% 16.86/15.98  108: animate(skc8, skc15) -> true
% 16.86/15.98  109: human(skc8, skc15) -> true
% 16.86/15.98  110: organism(skc8, skc15) -> true
% 16.86/15.98  111: impartial(skc8, skc15) -> true
% 16.86/15.98  112: living(skc8, skc15) -> true
% 16.86/15.98  113: entity(skc8, skc15) -> true
% 16.86/15.98  114: existent(skc8, skc15) -> true
% 16.86/15.98  115: specific(skc8, skc15) -> true
% 16.86/15.98  116: thing(skc8, skc15) -> true
% 16.86/15.98  117: singleton(skc8, skc15) -> true
% 16.86/15.98  118: ifeq3(woman(skc8, skc15), true, true, true) -> true
% 16.86/15.99  119: ifeq3(man(skc8, skc12), true, true, true) -> true
% 16.86/15.99  120: ifeq3(man(X, Y), true, male(X, Y), true) -> true
% 16.86/15.99  121: male(skc8, skc15) -> true
% 16.86/15.99  122: ifeq3(entity(skc10, skc13), true, true, true) -> true
% 16.86/15.99  123: ifeq3(abstraction(skc10, skc13), true, true, true) -> true
% 16.86/15.99  124: ifeq3(proposition(skc8, skc11), true, true, true) -> true
% 16.86/15.99  125: ifeq3(proposition(skc8, skc14), true, true, true) -> true
% 16.86/15.99  126: ifeq3(abstraction(skc8, skc9), true, true, true) -> true
% 16.86/15.99  127: ifeq3(entity(skc8, skc10), true, true, true) -> true
% 16.86/15.99  128: ifeq3(eventuality(skc8, skc10), true, true, true) -> true
% 16.86/15.99  129: ifeq3(entity(skc8, skc9), true, true, true) -> true
% 16.86/15.99  130: ifeq3(entity(skc8, skc14), true, true, true) -> true
% 16.86/15.99  131: ifeq3(eventuality(skc8, skc12), true, true, true) -> true
% 16.86/15.99  132: ifeq3(abstraction(skc8, skc15), true, true, true) -> true
% 16.86/15.99  133: ifeq3(eventuality(skc8, skc15), true, true, true) -> true
% 16.86/15.99  134: ifeq3(abstraction(skc8, skc12), true, true, true) -> true
% 16.86/15.99  135: ifeq3(eventuality(skc8, skc11), true, true, true) -> true
% 16.86/15.99  136: ifeq3(eventuality(skc8, skc14), true, true, true) -> true
% 16.86/15.99  137: ifeq3(entity(skc8, skc11), true, true, true) -> true
% 16.86/15.99  138: ifeq2(tuple2(unisex(X, Y), male(X, Y)), tuple2(true, true), a, b) -> b
% 16.86/15.99  139: ifeq2(tuple2(unisex(skc8, skc15), true), tuple2(true, true), a, b) -> b
% 16.86/15.99  140: ifeq2(tuple2(unisex(X, Y), female(X, Y)), tuple2(true, true), a, b) -> b
% 16.86/15.99  141: ifeq2(tuple2(unisex(skc8, skc12), true), tuple2(true, true), a, b) -> b
% 16.86/15.99  142: ifeq2(tuple2(specific(X, Y), general(X, Y)), tuple2(true, true), a, b) -> b
% 16.86/15.99  143: ifeq2(tuple2(nonhuman(X, Y), human(X, Y)), tuple2(true, true), a, b) -> b
% 16.86/15.99  144: ifeq2(tuple2(female(X, Y), male(X, Y)), tuple2(true, true), a, b) -> b
% 16.86/15.99  145: ifeq2(tuple2(true, male(skc8, skc12)), tuple2(true, true), a, b) -> b
% 16.86/15.99  146: ifeq2(tuple2(female(skc8, skc15), true), tuple2(true, true), a, b) -> b
% 16.86/15.99  147: ifeq2(tuple2(nonexistent(X, Y), existent(X, Y)), tuple2(true, true), a, b) -> b
% 16.86/15.99  148: ifeq2(tuple2(true, existent(skc10, skc13)), tuple2(true, true), a, b) -> b
% 16.86/15.99  149: ifeq2(tuple2(nonhuman(skc8, skc15), true), tuple2(true, true), a, b) -> b
% 16.86/15.99  150: ifeq2(tuple2(nonhuman(skc8, skc12), true), tuple2(true, true), a, b) -> b
% 16.86/15.99  151: ifeq2(tuple2(true, general(skc10, skc13)), tuple2(true, true), a, b) -> b
% 16.86/15.99  152: ifeq2(tuple2(true, female(skc10, skc13)), tuple2(true, true), a, b) -> b
% 16.86/15.99  153: ifeq2(tuple2(true, male(skc10, skc13)), tuple2(true, true), a, b) -> b
% 16.86/15.99  154: ifeq2(tuple2(true, male(skc8, skc10)), tuple2(true, true), a, b) -> b
% 16.86/15.99  155: ifeq2(tuple2(true, female(skc8, skc10)), tuple2(true, true), a, b) -> b
% 16.86/15.99  156: ifeq2(tuple2(true, male(skc8, skc9)), tuple2(true, true), a, b) -> b
% 16.86/15.99  157: ifeq2(tuple2(true, female(skc8, skc9)), tuple2(true, true), a, b) -> b
% 16.86/15.99  158: ifeq2(tuple2(true, existent(skc8, skc9)), tuple2(true, true), a, b) -> b
% 16.86/15.99  159: ifeq2(tuple2(true, human(skc8, skc10)), tuple2(true, true), a, b) -> b
% 16.86/15.99  160: ifeq2(tuple2(true, general(skc8, skc9)), tuple2(true, true), a, b) -> b
% 16.86/15.99  161: ifeq2(tuple2(specific(skc8, skc10), true), tuple2(true, true), a, b) -> b
% 16.86/15.99  162: ifeq2(tuple2(true, general(skc8, skc15)), tuple2(true, true), a, b) -> b
% 16.86/15.99  163: ifeq2(tuple2(specific(skc8, skc11), true), tuple2(true, true), a, b) -> b
% 16.86/15.99  164: ifeq2(tuple2(nonexistent(skc8, skc12), true), tuple2(true, true), a, b) -> b
% 16.86/15.99  165: ifeq2(tuple2(nonexistent(skc8, skc15), true), tuple2(true, true), a, b) -> b
% 16.86/15.99  166: ifeq2(tuple2(specific(skc8, skc14), true), tuple2(true, true), a, b) -> b
% 16.86/15.99  167: ifeq2(tuple2(true, female(skc8, skc14)), tuple2(true, true), a, b) -> b
% 16.86/15.99  168: ifeq2(tuple2(true, human(skc8, skc11)), tuple2(true, true), a, b) -> b
% 16.86/15.99  169: ifeq2(tuple2(true, human(skc8, skc14)), tuple2(true, true), a, b) -> b
% 16.86/15.99  170: ifeq2(tuple2(true, male(skc8, skc14)), tuple2(true, true), a, b) -> b
% 16.86/15.99  171: ifeq2(tuple2(true, male(skc8, skc11)), tuple2(true, true), a, b) -> b
% 16.86/15.99  172: ifeq2(tuple2(true, female(skc8, skc11)), tuple2(true, true), a, b) -> b
% 16.86/15.99  173: ifeq2(tuple2(true, general(skc8, skc12)), tuple2(true, true), a, b) -> b
% 16.86/15.99  174: ifeq3(accessible_world(X, Y), true, ifeq3(human(X, Z), true, human(Y, Z), true), true) -> true
% 16.86/15.99  175: ifeq3(human(skc8, X), true, human(skc10, X), true) -> true
% 16.86/15.99  176: human(skc10, skc12) -> true
% 16.86/15.99  177: human(skc10, skc15) -> true
% 16.86/15.99  178: ifeq3(human_person(skc10, skc15), true, true, true) -> true
% 16.86/15.99  179: ifeq3(human_person(skc10, skc12), true, true, true) -> true
% 16.86/15.99  180: ifeq3(accessible_world(skc8, X), true, human(X, skc12), true) -> true
% 16.86/15.99  181: ifeq3(accessible_world(skc8, skc8), true, true, true) -> true
% 16.86/15.99  182: ifeq3(accessible_world(skc8, X), true, human(X, skc15), true) -> true
% 16.86/15.99  183: ifeq3(accessible_world(skc10, X), true, human(X, skc12), true) -> true
% 16.86/15.99  184: ifeq3(accessible_world(skc10, skc10), true, true, true) -> true
% 16.86/15.99  185: ifeq3(accessible_world(skc10, skc8), true, true, true) -> true
% 16.86/15.99  186: ifeq3(accessible_world(skc10, X), true, human(X, skc15), true) -> true
% 16.86/15.99  187: ifeq2(tuple2(nonhuman(skc10, skc15), true), tuple2(true, true), a, b) -> b
% 16.86/15.99  188: ifeq2(tuple2(nonhuman(skc10, skc12), true), tuple2(true, true), a, b) -> b
% 16.86/15.99  189: ifeq3(accessible_world(X, Y), true, ifeq3(impartial(X, Z), true, impartial(Y, Z), true), true) -> true
% 16.86/15.99  190: ifeq3(impartial(skc8, X), true, impartial(skc10, X), true) -> true
% 16.86/15.99  191: true -> impartial(skc10, skc12)
% 16.86/15.99  192: impartial(skc10, skc15) -> impartial(skc10, skc12)
% 16.86/15.99  193: ifeq3(accessible_world(skc8, X), impartial(skc10, skc12), impartial(X, skc12), impartial(skc10, skc12)) -> impartial(skc10, skc12)
% 16.86/15.99  194: ifeq3(accessible_world(skc8, X), impartial(skc10, skc12), impartial(X, skc15), impartial(skc10, skc12)) -> impartial(skc10, skc12)
% 16.86/15.99  196: ifeq3(accessible_world(X, Y), impartial(skc10, skc12), ifeq3(living(X, Z), impartial(skc10, skc12), living(Y, Z), impartial(skc10, skc12)), impartial(skc10, skc12)) -> impartial(skc10, skc12)
% 16.86/15.99  197: ifeq3(living(skc8, X), impartial(skc10, skc12), living(skc10, X), impartial(skc10, skc12)) -> impartial(skc10, skc12)
% 16.86/15.99  198: living(skc10, skc12) -> impartial(skc10, skc12)
% 16.86/15.99  199: living(skc10, skc15) -> impartial(skc10, skc12)
% 16.86/15.99  201: ifeq3(accessible_world(X, Y), impartial(skc10, skc12), ifeq3(animate(X, Z), impartial(skc10, skc12), animate(Y, Z), impartial(skc10, skc12)), impartial(skc10, skc12)) -> impartial(skc10, skc12)
% 16.86/15.99  202: ifeq3(animate(skc8, X), impartial(skc10, skc12), animate(skc10, X), impartial(skc10, skc12)) -> impartial(skc10, skc12)
% 16.86/15.99  203: animate(skc10, skc12) -> impartial(skc10, skc12)
% 16.86/15.99  204: animate(skc10, skc15) -> impartial(skc10, skc12)
% 16.86/15.99  206: ifeq3(accessible_world(X, Y), impartial(skc10, skc12), ifeq3(vincent_forename(X, Z), impartial(skc10, skc12), vincent_forename(Y, Z), impartial(skc10, skc12)), impartial(skc10, skc12)) -> impartial(skc10, skc12)
% 16.86/15.99  207: ifeq3(vincent_forename(skc8, X), impartial(skc10, skc12), vincent_forename(skc10, X), impartial(skc10, skc12)) -> impartial(skc10, skc12)
% 16.86/15.99  208: impartial(skc10, skc12) -> vincent_forename(skc10, skc14)
% 16.86/15.99  209: ifeq3(accessible_world(skc8, X), vincent_forename(skc10, skc14), vincent_forename(X, skc14), vincent_forename(skc10, skc14)) -> vincent_forename(skc10, skc14)
% 16.86/15.99  211: ifeq3(accessible_world(X, Y), vincent_forename(skc10, skc14), ifeq3(female(X, Z), vincent_forename(skc10, skc14), female(Y, Z), vincent_forename(skc10, skc14)), vincent_forename(skc10, skc14)) -> vincent_forename(skc10, skc14)
% 16.86/15.99  212: ifeq3(female(skc8, X), vincent_forename(skc10, skc14), female(skc10, X), vincent_forename(skc10, skc14)) -> vincent_forename(skc10, skc14)
% 16.86/15.99  213: female(skc10, skc12) -> vincent_forename(skc10, skc14)
% 16.86/15.99  215: ifeq3(accessible_world(X, Y), vincent_forename(skc10, skc14), ifeq3(man(X, Z), vincent_forename(skc10, skc14), man(Y, Z), vincent_forename(skc10, skc14)), vincent_forename(skc10, skc14)) -> vincent_forename(skc10, skc14)
% 16.86/15.99  216: ifeq3(man(skc8, X), vincent_forename(skc10, skc14), man(skc10, X), vincent_forename(skc10, skc14)) -> vincent_forename(skc10, skc14)
% 16.86/15.99  217: man(skc10, skc15) -> vincent_forename(skc10, skc14)
% 16.86/15.99  218: male(skc10, skc15) -> vincent_forename(skc10, skc14)
% 16.86/15.99  219: human_person(skc10, skc15) -> vincent_forename(skc10, skc14)
% 16.86/15.99  220: organism(skc10, skc15) -> vincent_forename(skc10, skc14)
% 16.86/15.99  221: entity(skc10, skc15) -> vincent_forename(skc10, skc14)
% 16.86/15.99  222: existent(skc10, skc15) -> vincent_forename(skc10, skc14)
% 16.86/15.99  223: specific(skc10, skc15) -> vincent_forename(skc10, skc14)
% 16.86/15.99  224: thing(skc10, skc15) -> vincent_forename(skc10, skc14)
% 16.86/15.99  225: singleton(skc10, skc15) -> vincent_forename(skc10, skc14)
% 16.86/15.99  226: ifeq3(accessible_world(skc8, X), vincent_forename(skc10, skc14), man(X, skc15), vincent_forename(skc10, skc14)) -> vincent_forename(skc10, skc14)
% 16.86/15.99  228: ifeq3(accessible_world(X, Y), vincent_forename(skc10, skc14), ifeq3(proposition(X, Z), vincent_forename(skc10, skc14), proposition(Y, Z), vincent_forename(skc10, skc14)), vincent_forename(skc10, skc14)) -> vincent_forename(skc10, skc14)
% 16.86/15.99  229: ifeq3(proposition(skc8, X), vincent_forename(skc10, skc14), proposition(skc10, X), vincent_forename(skc10, skc14)) -> vincent_forename(skc10, skc14)
% 16.86/15.99  230: proposition(skc10, skc10) -> vincent_forename(skc10, skc14)
% 16.86/15.99  231: relation(skc10, skc10) -> vincent_forename(skc10, skc14)
% 16.86/15.99  232: vincent_forename(skc10, skc14) -> abstraction(skc10, skc10)
% 16.86/15.99  233: forename(skc10, skc14) -> abstraction(skc10, skc10)
% 16.86/15.99  234: relname(skc10, skc14) -> abstraction(skc10, skc10)
% 16.86/15.99  235: relation(skc10, skc14) -> abstraction(skc10, skc10)
% 16.86/15.99  236: abstraction(skc10, skc10) -> abstraction(skc10, skc14)
% 16.86/15.99  237: general(skc10, skc10) -> abstraction(skc10, skc14)
% 16.86/15.99  238: unisex(skc10, skc10) -> abstraction(skc10, skc14)
% 16.86/15.99  239: nonhuman(skc10, skc10) -> abstraction(skc10, skc14)
% 16.86/15.99  240: thing(skc10, skc10) -> abstraction(skc10, skc14)
% 16.86/15.99  241: singleton(skc10, skc10) -> abstraction(skc10, skc14)
% 16.86/15.99  242: ifeq3(accessible_world(skc8, X), abstraction(skc10, skc14), proposition(X, skc10), abstraction(skc10, skc14)) -> abstraction(skc10, skc14)
% 16.86/15.99  244: ifeq3(accessible_world(X, Y), abstraction(skc10, skc14), ifeq3(unisex(X, Z), abstraction(skc10, skc14), unisex(Y, Z), abstraction(skc10, skc14)), abstraction(skc10, skc14)) -> abstraction(skc10, skc14)
% 16.86/15.99  245: ifeq3(unisex(skc8, X), abstraction(skc10, skc14), unisex(skc10, X), abstraction(skc10, skc14)) -> abstraction(skc10, skc14)
% 16.86/15.99  246: unisex(skc10, skc9) -> abstraction(skc10, skc14)
% 16.86/15.99  247: unisex(skc10, skc14) -> abstraction(skc10, skc14)
% 16.86/15.99  248: unisex(skc10, skc11) -> abstraction(skc10, skc14)
% 16.86/15.99  250: ifeq3(present(X, Y), abstraction(skc10, skc14), ifeq3(accessible_world(X, Z), abstraction(skc10, skc14), present(Z, Y), abstraction(skc10, skc14)), abstraction(skc10, skc14)) -> abstraction(skc10, skc14)
% 16.86/15.99  251: ifeq3(accessible_world(skc10, X), abstraction(skc10, skc14), present(X, skc13), abstraction(skc10, skc14)) -> abstraction(skc10, skc14)
% 16.86/15.99  252: ifeq3(accessible_world(skc8, X), abstraction(skc10, skc14), present(X, skc9), abstraction(skc10, skc14)) -> abstraction(skc10, skc14)
% 16.86/15.99  253: present(skc10, skc9) -> abstraction(skc10, skc14)
% 16.86/15.99  254: ifeq3(present(skc8, X), abstraction(skc10, skc14), present(skc10, X), abstraction(skc10, skc14)) -> abstraction(skc10, skc14)
% 16.86/15.99  256: ifeq3(accessible_world(X, Y), abstraction(skc10, skc14), ifeq3(relation(X, Z), abstraction(skc10, skc14), relation(Y, Z), abstraction(skc10, skc14)), abstraction(skc10, skc14)) -> abstraction(skc10, skc14)
% 16.86/15.99  257: ifeq3(relation(skc8, X), abstraction(skc10, skc14), relation(skc10, X), abstraction(skc10, skc14)) -> abstraction(skc10, skc14)
% 16.86/15.99  258: relation(skc10, skc11) -> abstraction(skc10, skc14)
% 16.86/15.99  259: abstraction(skc10, skc11) -> abstraction(skc10, skc14)
% 16.86/15.99  260: general(skc10, skc11) -> abstraction(skc10, skc14)
% 16.86/15.99  261: nonhuman(skc10, skc11) -> abstraction(skc10, skc14)
% 16.86/15.99  262: thing(skc10, skc11) -> abstraction(skc10, skc14)
% 16.86/15.99  263: singleton(skc10, skc11) -> abstraction(skc10, skc14)
% 16.86/15.99  265: ifeq3(accessible_world(X, Y), abstraction(skc10, skc14), ifeq3(desire_want(X, Z), abstraction(skc10, skc14), desire_want(Y, Z), abstraction(skc10, skc14)), abstraction(skc10, skc14)) -> abstraction(skc10, skc14)
% 16.86/15.99  266: ifeq3(desire_want(skc8, X), abstraction(skc10, skc14), desire_want(skc10, X), abstraction(skc10, skc14)) -> abstraction(skc10, skc14)
% 16.86/15.99  267: desire_want(skc10, skc9) -> abstraction(skc10, skc14)
% 16.86/15.99  268: event(skc10, skc9) -> abstraction(skc10, skc14)
% 16.86/15.99  269: eventuality(skc10, skc9) -> abstraction(skc10, skc14)
% 16.86/15.99  270: abstraction(skc10, skc14) -> nonexistent(skc10, skc9)
% 16.86/15.99  271: specific(skc10, skc9) -> nonexistent(skc10, skc9)
% 16.86/15.99  272: thing(skc10, skc9) -> nonexistent(skc10, skc9)
% 16.86/15.99  273: singleton(skc10, skc9) -> nonexistent(skc10, skc9)
% 16.86/15.99  274: thing(skc10, skc14) -> nonexistent(skc10, skc9)
% 16.86/15.99  275: nonhuman(skc10, skc14) -> nonexistent(skc10, skc9)
% 16.86/15.99  276: general(skc10, skc14) -> nonexistent(skc10, skc9)
% 16.86/15.99  277: singleton(skc10, skc14) -> nonexistent(skc10, skc9)
% 16.86/15.99  278: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), desire_want(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  280: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(nonhuman(X, Z), nonexistent(skc10, skc9), nonhuman(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  281: ifeq3(nonhuman(skc8, X), nonexistent(skc10, skc9), nonhuman(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  283: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(abstraction(X, Z), nonexistent(skc10, skc9), abstraction(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  284: ifeq3(abstraction(skc8, X), nonexistent(skc10, skc9), abstraction(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  286: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(general(X, Z), nonexistent(skc10, skc9), general(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  287: ifeq3(general(skc8, X), nonexistent(skc10, skc9), general(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  289: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(mia_forename(X, Z), nonexistent(skc10, skc9), mia_forename(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  290: ifeq3(mia_forename(skc8, X), nonexistent(skc10, skc9), mia_forename(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  291: mia_forename(skc10, skc11) -> nonexistent(skc10, skc9)
% 16.86/15.99  292: forename(skc10, skc11) -> nonexistent(skc10, skc9)
% 16.86/15.99  293: relname(skc10, skc11) -> nonexistent(skc10, skc9)
% 16.86/15.99  294: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), mia_forename(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  296: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(forename(X, Z), nonexistent(skc10, skc9), forename(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  297: ifeq3(forename(skc8, X), nonexistent(skc10, skc9), forename(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  298: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), forename(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  299: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), forename(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  301: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(relname(X, Z), nonexistent(skc10, skc9), relname(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  302: ifeq3(relname(skc8, X), nonexistent(skc10, skc9), relname(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  304: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(woman(X, Z), nonexistent(skc10, skc9), woman(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  305: ifeq3(woman(skc8, X), nonexistent(skc10, skc9), woman(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  306: woman(skc10, skc12) -> nonexistent(skc10, skc9)
% 16.86/15.99  307: human_person(skc10, skc12) -> nonexistent(skc10, skc9)
% 16.86/15.99  308: organism(skc10, skc12) -> nonexistent(skc10, skc9)
% 16.86/15.99  309: entity(skc10, skc12) -> nonexistent(skc10, skc9)
% 16.86/15.99  310: existent(skc10, skc12) -> nonexistent(skc10, skc9)
% 16.86/15.99  311: specific(skc10, skc12) -> nonexistent(skc10, skc9)
% 16.86/15.99  312: thing(skc10, skc12) -> nonexistent(skc10, skc9)
% 16.86/15.99  313: singleton(skc10, skc12) -> nonexistent(skc10, skc9)
% 16.86/15.99  314: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), woman(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  316: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(organism(X, Z), nonexistent(skc10, skc9), organism(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  317: ifeq3(organism(skc8, X), nonexistent(skc10, skc9), organism(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  319: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(human_person(X, Z), nonexistent(skc10, skc9), human_person(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  320: ifeq3(human_person(skc8, X), nonexistent(skc10, skc9), human_person(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  322: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(entity(X, Z), nonexistent(skc10, skc9), entity(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  323: ifeq3(entity(skc8, X), nonexistent(skc10, skc9), entity(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  325: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(event(X, Z), nonexistent(skc10, skc9), event(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  326: ifeq3(event(skc8, X), nonexistent(skc10, skc9), event(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  327: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), event(X, skc13), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  329: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(dance(X, Z), nonexistent(skc10, skc9), dance(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  330: ifeq3(dance(skc8, X), nonexistent(skc10, skc9), dance(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  331: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), dance(X, skc13), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  333: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(eventuality(X, Z), nonexistent(skc10, skc9), eventuality(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  334: ifeq3(eventuality(skc8, X), nonexistent(skc10, skc9), eventuality(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  336: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(singleton(X, Z), nonexistent(skc10, skc9), singleton(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  337: ifeq3(singleton(skc8, X), nonexistent(skc10, skc9), singleton(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  339: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(thing(X, Z), nonexistent(skc10, skc9), thing(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  340: ifeq3(thing(skc8, X), nonexistent(skc10, skc9), thing(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  342: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(specific(X, Z), nonexistent(skc10, skc9), specific(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  343: ifeq3(specific(skc8, X), nonexistent(skc10, skc9), specific(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  345: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(existent(X, Z), nonexistent(skc10, skc9), existent(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  346: ifeq3(existent(skc8, X), nonexistent(skc10, skc9), existent(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  348: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(nonexistent(X, Z), nonexistent(skc10, skc9), nonexistent(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  349: ifeq3(nonexistent(skc8, X), nonexistent(skc10, skc9), nonexistent(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  350: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), nonexistent(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  352: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(male(X, Z), nonexistent(skc10, skc9), male(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  353: ifeq3(male(skc8, X), nonexistent(skc10, skc9), male(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  354: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), male(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  355: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), human_person(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  356: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), human_person(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  357: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), eventuality(X, skc13), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  358: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), event(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  359: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), relation(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  360: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), relname(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  361: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), relname(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  362: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), female(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  363: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(human(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  364: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(human(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  365: ifeq3(accessible_world(skc8, skc8), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  366: ifeq3(event(skc8, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  367: ifeq3(present(skc8, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  368: ifeq3(dance(skc8, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  369: ifeq3(eventuality(skc8, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  370: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), eventuality(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  371: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), desire_want(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  372: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), abstraction(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  373: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), organism(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  374: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), present(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  375: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), unisex(X, skc13), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  376: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), relation(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  377: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), relation(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  378: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), thing(X, skc13), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  379: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), nonexistent(X, skc13), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  380: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), man(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  381: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), specific(X, skc13), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  382: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), proposition(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  383: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), organism(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  384: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), woman(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  385: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), mia_forename(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  386: ifeq3(vincent_forename(skc8, X), nonexistent(skc10, skc9), vincent_forename(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  387: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), impartial(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  388: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), female(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  389: ifeq3(living(skc8, X), nonexistent(skc10, skc9), living(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  390: ifeq3(animate(skc8, X), nonexistent(skc10, skc9), animate(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  391: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), animate(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  392: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), animate(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  393: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(human(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  394: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(human(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  395: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(impartial(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  396: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(impartial(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  397: ifeq3(nonexistent(skc8, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  398: ifeq3(thing(skc8, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  399: ifeq3(specific(skc8, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  400: ifeq3(unisex(skc8, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  401: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), entity(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  402: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), entity(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  403: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), male(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  404: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), singleton(X, skc13), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  405: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), human_person(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  406: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), human_person(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  407: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), unisex(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  408: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), unisex(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  409: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), general(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  410: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), abstraction(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  411: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), abstraction(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  412: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), nonhuman(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  413: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), thing(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  414: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), thing(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  415: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), nonexistent(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  416: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), relation(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  417: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), relation(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  418: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), forename(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  419: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), event(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  420: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), specific(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  421: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), living(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  422: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), living(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  423: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), animate(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  424: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), animate(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  425: ifeq3(accessible_world(skc10, skc8), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  426: ifeq3(event(X, Y), nonexistent(skc10, skc9), eventuality(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  427: ifeq3(thing(X, Y), nonexistent(skc10, skc9), singleton(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  428: ifeq3(dance(X, Y), nonexistent(skc10, skc9), event(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  429: ifeq3(abstraction(X, Y), nonexistent(skc10, skc9), thing(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  430: ifeq3(abstraction(X, Y), nonexistent(skc10, skc9), nonhuman(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  431: ifeq3(entity(X, Y), nonexistent(skc10, skc9), existent(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  432: ifeq3(eventuality(X, Y), nonexistent(skc10, skc9), nonexistent(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  433: ifeq3(eventuality(X, Y), nonexistent(skc10, skc9), specific(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  434: ifeq3(eventuality(X, Y), nonexistent(skc10, skc9), thing(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  435: ifeq3(man(skc10, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  436: ifeq3(vincent_forename(skc10, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  437: ifeq3(relname(skc10, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  438: ifeq3(proposition(skc10, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  439: ifeq3(proposition(X, Y), nonexistent(skc10, skc9), relation(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  440: ifeq3(desire_want(X, Y), nonexistent(skc10, skc9), event(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  441: ifeq3(eventuality(X, Y), nonexistent(skc10, skc9), unisex(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  442: ifeq3(relation(X, Y), nonexistent(skc10, skc9), abstraction(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  443: ifeq3(human_person(X, Y), nonexistent(skc10, skc9), human(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  444: ifeq3(organism(X, Y), nonexistent(skc10, skc9), living(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  445: ifeq3(entity(X, Y), nonexistent(skc10, skc9), specific(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  446: ifeq3(organism(X, Y), nonexistent(skc10, skc9), entity(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  447: ifeq3(human_person(X, Y), nonexistent(skc10, skc9), organism(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  448: ifeq3(entity(X, Y), nonexistent(skc10, skc9), thing(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  449: ifeq3(relname(X, Y), nonexistent(skc10, skc9), relation(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  450: ifeq3(mia_forename(X, Y), nonexistent(skc10, skc9), forename(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  451: ifeq3(woman(X, Y), nonexistent(skc10, skc9), human_person(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  452: ifeq3(forename(X, Y), nonexistent(skc10, skc9), relname(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  453: ifeq3(abstraction(X, Y), nonexistent(skc10, skc9), general(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  454: ifeq3(abstraction(X, Y), nonexistent(skc10, skc9), unisex(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  455: ifeq3(man(X, Y), nonexistent(skc10, skc9), male(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  456: ifeq3(man(X, Y), nonexistent(skc10, skc9), human_person(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  457: ifeq3(woman(X, Y), nonexistent(skc10, skc9), female(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  458: ifeq3(vincent_forename(X, Y), nonexistent(skc10, skc9), forename(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  459: ifeq3(human_person(X, Y), nonexistent(skc10, skc9), animate(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  460: ifeq3(organism(X, Y), nonexistent(skc10, skc9), impartial(X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  461: ifeq3(woman(skc10, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  462: ifeq3(dance(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  463: ifeq3(singleton(skc8, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  465: ifeq3(theme(X, Y, Z), nonexistent(skc10, skc9), ifeq3(accessible_world(X, W), nonexistent(skc10, skc9), theme(W, Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  466: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), theme(X, skc9, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  467: theme(skc10, skc9, skc10) -> nonexistent(skc10, skc9)
% 16.86/15.99  468: ifeq3(theme(skc8, X, Y), nonexistent(skc10, skc9), theme(skc10, X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  470: ifeq3(agent(X, Y, Z), nonexistent(skc10, skc9), ifeq3(accessible_world(X, W), nonexistent(skc10, skc9), agent(W, Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  471: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), agent(X, skc13, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  472: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), agent(X, skc9, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  473: agent(skc10, skc9, skc12) -> nonexistent(skc10, skc9)
% 16.86/15.99  474: ifeq3(agent(skc8, X, Y), nonexistent(skc10, skc9), agent(skc10, X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  475: ifeq3(agent(skc8, skc13, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  477: ifeq3(of(X, Y, Z), nonexistent(skc10, skc9), ifeq3(accessible_world(X, W), nonexistent(skc10, skc9), of(W, Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  478: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), of(X, skc11, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  479: of(skc10, skc11, skc12) -> nonexistent(skc10, skc9)
% 16.86/15.99  480: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), of(X, skc14, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  481: of(skc10, skc14, skc15) -> nonexistent(skc10, skc9)
% 16.86/15.99  482: ifeq3(of(skc8, X, Y), nonexistent(skc10, skc9), of(skc10, X, Y), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  483: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), of(X, skc11, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  484: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), of(X, skc14, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  485: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), agent(X, skc9, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  486: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), theme(X, skc9, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  487: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), eventuality(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  488: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), living(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  489: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), living(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  490: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), impartial(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  491: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), impartial(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  492: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), relname(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  493: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), vincent_forename(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  494: ifeq3(proposition(skc8, X), nonexistent(skc10, skc9), proposition(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  495: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), organism(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  496: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), organism(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  497: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), specific(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  498: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), specific(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  499: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), human(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  500: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), impartial(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  501: ifeq3(impartial(skc8, X), nonexistent(skc10, skc9), impartial(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  502: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), human(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  503: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), abstraction(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  504: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), thing(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  505: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), thing(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  506: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), human(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  507: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), human(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  508: ifeq3(human(skc8, X), nonexistent(skc10, skc9), human(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  509: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), singleton(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  510: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), singleton(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  511: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), thing(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  512: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), thing(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  513: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), unisex(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  514: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), unisex(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  515: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), unisex(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  516: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), existent(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  517: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), existent(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  518: ifeq3(female(skc8, X), nonexistent(skc10, skc9), female(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  519: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), man(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  520: ifeq3(man(skc8, X), nonexistent(skc10, skc9), man(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  521: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), vincent_forename(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  522: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), nonhuman(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  523: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), nonhuman(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  524: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), general(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  525: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), general(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  526: ifeq3(abstraction(skc10, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  527: ifeq3(proposition(skc8, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  528: ifeq3(entity(skc10, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  529: ifeq3(proposition(skc8, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  530: ifeq3(man(skc8, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  531: ifeq3(woman(skc8, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  532: ifeq3(vincent_forename(skc8, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  533: ifeq3(abstraction(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  534: ifeq3(desire_want(skc10, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  535: ifeq3(dance(skc8, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  536: ifeq3(entity(skc8, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  537: ifeq3(eventuality(skc8, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  538: ifeq3(entity(skc8, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  539: ifeq3(abstraction(skc8, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  540: ifeq3(relname(skc8, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  541: ifeq3(mia_forename(skc8, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  542: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), abstraction(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  543: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), specific(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  544: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), forename(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  545: ifeq3(relation(skc8, X), nonexistent(skc10, skc9), relation(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  546: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), present(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  547: ifeq3(present(skc8, X), nonexistent(skc10, skc9), present(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  548: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), present(X, skc13), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  549: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), proposition(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  550: ifeq3(desire_want(skc8, X), nonexistent(skc10, skc9), desire_want(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  551: ifeq3(unisex(skc8, X), nonexistent(skc10, skc9), unisex(skc10, X), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  552: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), entity(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  553: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), entity(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  554: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), general(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  555: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), nonhuman(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  556: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), unisex(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  557: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), thing(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  558: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), unisex(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  559: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), singleton(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  560: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), singleton(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  561: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), singleton(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  562: ifeq3(accessible_world(skc8, X), nonexistent(skc10, skc9), singleton(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  563: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), thing(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  564: ifeq3(eventuality(skc10, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  565: ifeq3(eventuality(skc10, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  566: ifeq3(entity(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  567: ifeq3(eventuality(skc8, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  568: ifeq3(entity(skc8, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  569: ifeq3(eventuality(skc8, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  570: ifeq3(mia_forename(skc10, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  571: ifeq3(abstraction(skc8, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  572: ifeq3(eventuality(skc8, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  573: ifeq3(abstraction(skc8, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  574: ifeq3(eventuality(skc8, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  575: ifeq3(entity(skc8, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  576: ifeq3(entity(skc10, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  577: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), specific(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  578: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), specific(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  579: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), relname(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  580: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), nonhuman(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  581: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), singleton(X, skc11), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  582: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), general(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  583: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), existent(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  584: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), existent(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  585: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), thing(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  586: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), singleton(X, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  587: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), thing(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  588: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), thing(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  589: ifeq3(abstraction(skc10, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  590: ifeq3(entity(skc10, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  591: ifeq3(eventuality(skc10, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  592: ifeq3(eventuality(skc10, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  593: ifeq3(abstraction(skc10, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  594: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), relation(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  595: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), singleton(X, skc12), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  596: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), singleton(X, skc15), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  597: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), singleton(X, skc14), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  598: ifeq3(proposition(skc10, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  599: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), abstraction(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  600: ifeq2(tuple2(nonexistent(skc10, skc9), male(skc10, skc12)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  601: ifeq2(tuple2(unisex(skc10, skc12), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  602: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), nonhuman(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  603: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), general(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  604: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), thing(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  605: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), unisex(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  606: ifeq3(eventuality(skc10, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  607: ifeq3(entity(skc10, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  608: ifeq2(tuple2(female(skc10, skc15), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  609: ifeq2(tuple2(unisex(skc10, skc15), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  610: ifeq2(tuple2(unisex(X, Y), female(X, Y)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  611: ifeq2(tuple2(unisex(X, Y), male(X, Y)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  612: ifeq2(tuple2(nonexistent(X, Y), existent(X, Y)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  613: ifeq2(tuple2(female(X, Y), male(X, Y)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  614: ifeq2(tuple2(nonhuman(X, Y), human(X, Y)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  615: ifeq2(tuple2(specific(X, Y), general(X, Y)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  616: ifeq3(accessible_world(skc10, X), nonexistent(skc10, skc9), singleton(X, skc10), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  617: ifeq2(tuple2(nonhuman(skc10, skc12), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  618: ifeq2(tuple2(nonhuman(skc10, skc15), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  619: ifeq2(tuple2(nonexistent(skc10, skc9), male(skc8, skc12)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  620: ifeq2(tuple2(female(skc8, skc15), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  621: ifeq2(tuple2(nonexistent(skc10, skc9), existent(skc10, skc13)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  622: ifeq2(tuple2(unisex(skc8, skc12), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  623: ifeq2(tuple2(nonexistent(skc10, skc9), human(skc8, skc10)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  624: ifeq2(tuple2(unisex(skc8, skc15), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  625: ifeq2(tuple2(specific(skc8, skc10), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  626: ifeq2(tuple2(nonexistent(skc10, skc9), general(skc8, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  627: ifeq2(tuple2(nonexistent(skc10, skc9), female(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  628: ifeq2(tuple2(nonexistent(skc10, skc9), male(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  629: ifeq2(tuple2(nonexistent(skc10, skc9), female(skc8, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  630: ifeq2(tuple2(nonexistent(skc10, skc9), existent(skc8, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  631: ifeq2(tuple2(nonexistent(skc10, skc9), male(skc8, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  632: ifeq2(tuple2(nonexistent(skc10, skc9), female(skc8, skc10)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  633: ifeq2(tuple2(nonexistent(skc10, skc9), male(skc8, skc10)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  634: ifeq2(tuple2(nonexistent(skc10, skc9), male(skc10, skc13)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  635: ifeq2(tuple2(nonexistent(skc10, skc9), female(skc10, skc13)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  636: ifeq2(tuple2(nonexistent(skc10, skc9), general(skc10, skc13)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  637: ifeq2(tuple2(nonhuman(skc8, skc12), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  638: ifeq2(tuple2(nonhuman(skc8, skc15), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  639: ifeq2(tuple2(nonexistent(skc10, skc9), female(skc10, skc14)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  640: ifeq2(tuple2(nonexistent(skc10, skc9), male(skc10, skc14)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  641: ifeq2(tuple2(nonexistent(skc10, skc9), general(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  642: ifeq2(tuple2(nonexistent(skc10, skc9), human(skc10, skc11)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  643: ifeq2(tuple2(nonexistent(skc10, skc9), female(skc10, skc11)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  644: ifeq2(tuple2(nonexistent(skc10, skc9), male(skc10, skc11)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  645: ifeq2(tuple2(specific(skc8, skc11), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  646: ifeq2(tuple2(nonexistent(skc10, skc9), general(skc8, skc15)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  647: ifeq2(tuple2(nonexistent(skc10, skc9), human(skc8, skc14)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  648: ifeq2(tuple2(nonexistent(skc8, skc12), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  649: ifeq2(tuple2(nonexistent(skc10, skc9), human(skc8, skc11)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  650: ifeq2(tuple2(nonexistent(skc10, skc9), female(skc8, skc14)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  651: ifeq2(tuple2(specific(skc8, skc14), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  652: ifeq2(tuple2(nonexistent(skc8, skc15), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  653: ifeq2(tuple2(specific(skc10, skc11), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  654: ifeq2(tuple2(nonexistent(skc10, skc9), general(skc8, skc12)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  655: ifeq2(tuple2(nonexistent(skc10, skc9), male(skc8, skc11)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  656: ifeq2(tuple2(nonexistent(skc10, skc9), male(skc8, skc14)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  657: ifeq2(tuple2(nonexistent(skc10, skc9), female(skc8, skc11)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  658: ifeq2(tuple2(nonexistent(skc10, skc9), human(skc10, skc14)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  659: ifeq2(tuple2(nonexistent(skc10, skc15), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  660: ifeq2(tuple2(nonexistent(skc10, skc9), general(skc10, skc12)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  661: ifeq2(tuple2(specific(skc10, skc14), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  662: ifeq2(tuple2(nonexistent(skc10, skc12), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  663: ifeq2(tuple2(nonexistent(skc10, skc9), general(skc10, skc15)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  664: ifeq2(tuple2(nonexistent(skc10, skc9), female(skc10, skc10)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  665: ifeq2(tuple2(nonexistent(skc10, skc9), male(skc10, skc10)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  666: ifeq2(tuple2(specific(skc10, skc10), nonexistent(skc10, skc9)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  667: ifeq2(tuple2(nonexistent(skc10, skc9), human(skc10, skc10)), tuple2(nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  668: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(desire_want(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  669: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(event(X, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  670: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(forename(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  671: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(forename(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  672: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(mia_forename(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  673: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(woman(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  674: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(proposition(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  675: ifeq3(present(X, skc13), nonexistent(skc10, skc9), ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  676: ifeq3(present(X, skc9), nonexistent(skc10, skc9), ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  677: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(vincent_forename(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  678: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(man(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  679: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(dance(X, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  680: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(living(X, Z), nonexistent(skc10, skc9), living(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  681: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(male(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  682: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(relation(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  683: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(vincent_forename(X, Z), nonexistent(skc10, skc9), vincent_forename(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  684: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(event(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  685: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(relname(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  686: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(relname(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  687: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(female(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  688: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(human_person(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  689: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(human_person(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  690: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(animate(X, Z), nonexistent(skc10, skc9), animate(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  691: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(eventuality(X, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  692: ifeq3(agent(X, skc13, skc12), nonexistent(skc10, skc9), ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  693: ifeq3(agent(X, skc9, skc12), nonexistent(skc10, skc9), ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  694: ifeq3(theme(X, skc9, skc10), nonexistent(skc10, skc9), ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  695: ifeq3(of(X, skc14, skc15), nonexistent(skc10, skc9), ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  696: ifeq3(of(X, skc11, skc12), nonexistent(skc10, skc9), ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  697: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(eventuality(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  698: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(impartial(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  699: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(relation(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  700: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(animate(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  701: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(man(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  702: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(nonexistent(X, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  703: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(specific(X, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  704: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(animate(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  705: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(female(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  706: ifeq3(present(X, skc9), nonexistent(skc10, skc9), ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  707: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(thing(X, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  708: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(organism(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  709: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(unisex(X, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  710: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(proposition(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  711: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(abstraction(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  712: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(woman(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  713: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(relation(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  714: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(mia_forename(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  715: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(desire_want(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  716: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(organism(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  717: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(animate(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  718: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(animate(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  719: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(forename(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  720: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(living(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  721: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(human(X, Z), nonexistent(skc10, skc9), human(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  722: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(impartial(X, Z), nonexistent(skc10, skc9), impartial(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  723: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(entity(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  724: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(relation(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  725: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(man(X, Z), nonexistent(skc10, skc9), man(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  726: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(female(X, Z), nonexistent(skc10, skc9), female(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  727: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(proposition(X, Z), nonexistent(skc10, skc9), proposition(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  728: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(thing(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  729: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(living(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  730: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(nonhuman(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  731: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(unisex(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  732: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(abstraction(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  733: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(abstraction(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  734: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(unisex(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  735: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(human_person(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  736: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(event(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  737: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(entity(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  738: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(thing(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  739: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(male(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  740: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(relation(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  741: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(general(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  742: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(singleton(X, skc13), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  743: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(nonexistent(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  744: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(specific(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  745: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(human_person(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  746: ifeq3(theme(X, skc9, skc10), nonexistent(skc10, skc9), ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  747: ifeq3(of(X, skc11, skc12), nonexistent(skc10, skc9), ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  748: ifeq3(of(X, skc14, skc15), nonexistent(skc10, skc9), ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  749: ifeq3(agent(X, skc9, skc12), nonexistent(skc10, skc9), ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  750: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(eventuality(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  751: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(relname(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  752: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(nonhuman(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  753: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(unisex(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  754: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(living(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  755: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(thing(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  756: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(thing(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  757: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(thing(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  758: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(thing(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  759: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(singleton(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  760: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(singleton(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  761: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(desire_want(X, Z), nonexistent(skc10, skc9), desire_want(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  762: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(impartial(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  763: ifeq3(present(X, Y), nonexistent(skc10, skc9), ifeq3(accessible_world(X, Z), nonexistent(skc10, skc9), present(Z, Y), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  764: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(unisex(X, Z), nonexistent(skc10, skc9), unisex(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  765: ifeq3(accessible_world(X, Y), nonexistent(skc10, skc9), ifeq3(relation(X, Z), nonexistent(skc10, skc9), relation(Y, Z), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  766: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(specific(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  767: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(living(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  768: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(specific(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  769: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(unisex(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  770: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(existent(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  771: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(existent(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  772: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(nonhuman(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  773: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(unisex(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  774: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(vincent_forename(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  775: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(organism(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  776: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(organism(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  777: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(abstraction(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  778: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(general(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  779: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(general(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  780: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(abstraction(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  781: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(unisex(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  782: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(forename(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  783: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(unisex(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  784: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(thing(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  785: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(general(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  786: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(singleton(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  787: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(singleton(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  788: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(entity(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  789: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(entity(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  790: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(singleton(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  791: ifeq3(accessible_world(X, skc8), nonexistent(skc10, skc9), ifeq3(singleton(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  792: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(thing(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  793: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(nonhuman(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  794: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(specific(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  795: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(existent(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  796: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(thing(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  797: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(specific(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  798: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(specific(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  799: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(nonhuman(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  800: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(existent(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  801: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(singleton(X, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  802: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(thing(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  803: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(singleton(X, skc11), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  804: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(general(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  805: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(relname(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  806: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(thing(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  807: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(singleton(X, skc15), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  808: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(relation(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  809: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(singleton(X, skc12), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  810: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(singleton(X, skc14), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  811: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(abstraction(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  812: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(unisex(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  813: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(thing(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  814: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(general(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  815: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(nonhuman(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  816: ifeq3(accessible_world(X, skc10), nonexistent(skc10, skc9), ifeq3(singleton(X, skc10), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), nonexistent(skc10, skc9)) -> nonexistent(skc10, skc9)
% 16.86/15.99  818: ifeq4(of(X, Y, Z), nonexistent(skc10, skc9), ifeq4(of(X, W, Z), nonexistent(skc10, skc9), ifeq4(entity(X, Z), nonexistent(skc10, skc9), ifeq4(forename(X, Y), nonexistent(skc10, skc9), ifeq4(forename(X, W), nonexistent(skc10, skc9), Y, W), W), W), W), W) -> W
% 16.86/15.99  819: ifeq4(of(skc8, X, skc12), nonexistent(skc10, skc9), ifeq4(forename(skc8, X), nonexistent(skc10, skc9), skc11, X), X) -> X
% 16.86/15.99  820: ifeq4(of(skc8, skc14, skc12), nonexistent(skc10, skc9), skc11, skc14) -> skc14
% 16.86/15.99  821: ifeq4(of(skc8, X, skc15), nonexistent(skc10, skc9), ifeq4(forename(skc8, X), nonexistent(skc10, skc9), skc14, X), X) -> X
% 16.86/15.99  822: ifeq4(of(skc8, skc11, skc15), nonexistent(skc10, skc9), skc14, skc11) -> skc11
% 16.86/15.99  823: ifeq4(of(skc8, X, skc12), nonexistent(skc10, skc9), ifeq4(forename(skc8, X), nonexistent(skc10, skc9), X, skc11), skc11) -> skc11
% 16.86/15.99  824: ifeq4(of(skc8, skc14, skc12), nonexistent(skc10, skc9), skc14, skc11) -> skc11
% 16.86/15.99  825: ifeq4(of(skc8, X, skc15), nonexistent(skc10, skc9), ifeq4(forename(skc8, X), nonexistent(skc10, skc9), X, skc14), skc14) -> skc14
% 16.86/15.99  826: ifeq4(of(skc8, skc11, skc15), nonexistent(skc10, skc9), skc11, skc14) -> skc14
% 16.86/15.99  827: ifeq4(of(skc10, X, skc15), nonexistent(skc10, skc9), ifeq4(forename(skc10, X), nonexistent(skc10, skc9), skc14, X), X) -> X
% 16.86/15.99  828: ifeq4(of(skc10, skc11, skc15), nonexistent(skc10, skc9), skc14, skc11) -> skc11
% 16.86/15.99  829: ifeq4(of(skc10, X, skc12), nonexistent(skc10, skc9), ifeq4(forename(skc10, X), nonexistent(skc10, skc9), skc11, X), X) -> X
% 16.86/15.99  830: ifeq4(of(skc10, skc14, skc12), nonexistent(skc10, skc9), skc11, skc14) -> skc14
% 16.86/15.99  831: ifeq4(of(skc10, X, skc12), nonexistent(skc10, skc9), ifeq4(forename(skc10, X), nonexistent(skc10, skc9), X, skc11), skc11) -> skc11
% 16.86/15.99  832: ifeq4(of(skc10, skc14, skc12), nonexistent(skc10, skc9), skc14, skc11) -> skc11
% 16.86/15.99  833: ifeq4(of(skc10, X, skc15), nonexistent(skc10, skc9), ifeq4(forename(skc10, X), nonexistent(skc10, skc9), X, skc14), skc14) -> skc14
% 16.86/15.99  834: ifeq4(of(skc10, skc11, skc15), nonexistent(skc10, skc9), skc11, skc14) -> skc14
% 16.86/15.99  835: ifeq4(of(skc8, skc11, X), nonexistent(skc10, skc9), ifeq4(of(skc8, Y, X), nonexistent(skc10, skc9), ifeq4(entity(skc8, X), nonexistent(skc10, skc9), ifeq4(forename(skc8, Y), nonexistent(skc10, skc9), skc11, Y), Y), Y), Y) -> Y
% 16.86/15.99  836: ifeq4(of(skc8, skc11, X), nonexistent(skc10, skc9), ifeq4(of(skc8, skc11, X), nonexistent(skc10, skc9), ifeq4(entity(skc8, X), nonexistent(skc10, skc9), skc11, skc11), skc11), skc11) -> skc11
% 16.86/15.99  837: ifeq4(of(skc8, skc11, skc15), nonexistent(skc10, skc9), ifeq4(of(skc8, skc11, skc15), nonexistent(skc10, skc9), skc11, skc11), skc11) -> skc11
% 16.86/15.99  838: ifeq4(of(skc8, skc11, X), nonexistent(skc10, skc9), ifeq4(of(skc8, skc14, X), nonexistent(skc10, skc9), ifeq4(entity(skc8, X), nonexistent(skc10, skc9), skc11, skc14), skc14), skc14) -> skc14
% 16.86/15.99  839: ifeq4(of(skc8, skc11, skc15), nonexistent(skc10, skc9), ifeq4(of(skc8, X, skc15), nonexistent(skc10, skc9), ifeq4(forename(skc8, X), nonexistent(skc10, skc9), skc11, X), X), X) -> X
% 16.86/15.99  840: ifeq4(of(skc8, skc14, X), nonexistent(skc10, skc9), ifeq4(of(skc8, Y, X), nonexistent(skc10, skc9), ifeq4(entity(skc8, X), nonexistent(skc10, skc9), ifeq4(forename(skc8, Y), nonexistent(skc10, skc9), skc14, Y), Y), Y), Y) -> Y
% 16.86/15.99  841: ifeq4(of(skc8, skc14, X), nonexistent(skc10, skc9), ifeq4(of(skc8, skc11, X), nonexistent(skc10, skc9), ifeq4(entity(skc8, X), nonexistent(skc10, skc9), skc14, skc11), skc11), skc11) -> skc11
% 16.86/15.99  842: ifeq4(of(skc8, skc14, X), nonexistent(skc10, skc9), ifeq4(of(skc8, skc14, X), nonexistent(skc10, skc9), ifeq4(entity(skc8, X), nonexistent(skc10, skc9), skc14, skc14), skc14), skc14) -> skc14
% 16.86/15.99  843: ifeq4(of(skc8, skc14, skc12), nonexistent(skc10, skc9), ifeq4(of(skc8, skc14, skc12), nonexistent(skc10, skc9), skc14, skc14), skc14) -> skc14
% 16.86/15.99  844: ifeq4(of(skc8, skc14, skc12), nonexistent(skc10, skc9), ifeq4(of(skc8, X, skc12), nonexistent(skc10, skc9), ifeq4(forename(skc8, X), nonexistent(skc10, skc9), skc14, X), X), X) -> X
% 16.86/15.99  845: ifeq4(of(skc8, X, Y), nonexistent(skc10, skc9), ifeq4(of(skc8, skc11, Y), nonexistent(skc10, skc9), ifeq4(entity(skc8, Y), nonexistent(skc10, skc9), ifeq4(forename(skc8, X), nonexistent(skc10, skc9), X, skc11), skc11), skc11), skc11) -> skc11
% 16.86/15.99  846: ifeq4(of(skc8, X, skc15), nonexistent(skc10, skc9), ifeq4(of(skc8, skc11, skc15), nonexistent(skc10, skc9), ifeq4(forename(skc8, X), nonexistent(skc10, skc9), X, skc11), skc11), skc11) -> skc11
% 16.86/15.99  847: ifeq4(of(skc8, X, Y), nonexistent(skc10, skc9), ifeq4(of(skc8, skc14, Y), nonexistent(skc10, skc9), ifeq4(entity(skc8, Y), nonexistent(skc10, skc9), ifeq4(forename(skc8, X), nonexistent(skc10, skc9), X, skc14), skc14), skc14), skc14) -> skc14
% 16.86/15.99  848: ifeq4(of(skc8, X, skc12), nonexistent(skc10, skc9), ifeq4(of(skc8, skc14, skc12), nonexistent(skc10, skc9), ifeq4(forename(skc8, X), nonexistent(skc10, skc9), X, skc14), skc14), skc14) -> skc14
% 16.86/15.99  850: ifeq4(theme(X, Y, Z), nonexistent(skc10, skc9), ifeq4(theme(X, W, V), nonexistent(skc10, skc9), ifeq4(proposition(X, Z), nonexistent(skc10, skc9), ifeq4(proposition(X, V), nonexistent(skc10, skc9), ifeq4(desire_want(X, Y), nonexistent(skc10, skc9), ifeq4(desire_want(X, W), nonexistent(skc10, skc9), Z, V), V), V), V), V), V) -> V
% 16.86/15.99  851: ifeq4(theme(skc8, X, Y), nonexistent(skc10, skc9), ifeq4(proposition(skc8, Y), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, X), nonexistent(skc10, skc9), skc10, Y), Y), Y) -> Y
% 16.86/15.99  852: ifeq4(theme(skc8, skc9, X), nonexistent(skc10, skc9), ifeq4(proposition(skc8, X), nonexistent(skc10, skc9), skc10, X), X) -> X
% 16.86/15.99  853: ifeq4(theme(skc8, X, skc10), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, X), nonexistent(skc10, skc9), skc10, skc10), skc10) -> skc10
% 16.86/15.99  854: ifeq4(theme(skc8, X, Y), nonexistent(skc10, skc9), ifeq4(proposition(skc8, Y), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, X), nonexistent(skc10, skc9), Y, skc10), skc10), skc10) -> skc10
% 16.86/15.99  855: ifeq4(theme(skc8, skc9, X), nonexistent(skc10, skc9), ifeq4(proposition(skc8, X), nonexistent(skc10, skc9), X, skc10), skc10) -> skc10
% 16.86/15.99  856: ifeq4(theme(skc10, X, Y), nonexistent(skc10, skc9), ifeq4(proposition(skc10, Y), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, X), nonexistent(skc10, skc9), skc10, Y), Y), Y) -> Y
% 16.86/15.99  857: ifeq4(theme(skc10, skc9, X), nonexistent(skc10, skc9), ifeq4(proposition(skc10, X), nonexistent(skc10, skc9), skc10, X), X) -> X
% 16.86/15.99  858: ifeq4(theme(skc10, X, skc10), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, X), nonexistent(skc10, skc9), skc10, skc10), skc10) -> skc10
% 16.86/15.99  859: ifeq4(theme(skc10, X, Y), nonexistent(skc10, skc9), ifeq4(proposition(skc10, Y), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, X), nonexistent(skc10, skc9), Y, skc10), skc10), skc10) -> skc10
% 16.86/15.99  860: ifeq4(theme(skc10, skc9, X), nonexistent(skc10, skc9), ifeq4(proposition(skc10, X), nonexistent(skc10, skc9), X, skc10), skc10) -> skc10
% 16.86/15.99  861: ifeq4(of(skc8, X, skc12), nonexistent(skc10, skc9), ifeq4(of(skc8, Y, skc12), nonexistent(skc10, skc9), ifeq4(forename(skc8, X), nonexistent(skc10, skc9), ifeq4(forename(skc8, Y), nonexistent(skc10, skc9), X, Y), Y), Y), Y) -> Y
% 16.86/15.99  862: ifeq4(of(skc8, X, skc15), nonexistent(skc10, skc9), ifeq4(of(skc8, Y, skc15), nonexistent(skc10, skc9), ifeq4(forename(skc8, X), nonexistent(skc10, skc9), ifeq4(forename(skc8, Y), nonexistent(skc10, skc9), X, Y), Y), Y), Y) -> Y
% 16.86/15.99  863: ifeq4(of(skc10, skc11, X), nonexistent(skc10, skc9), ifeq4(of(skc10, Y, X), nonexistent(skc10, skc9), ifeq4(entity(skc10, X), nonexistent(skc10, skc9), ifeq4(forename(skc10, Y), nonexistent(skc10, skc9), skc11, Y), Y), Y), Y) -> Y
% 16.86/15.99  864: ifeq4(of(skc10, skc11, X), nonexistent(skc10, skc9), ifeq4(of(skc10, skc11, X), nonexistent(skc10, skc9), ifeq4(entity(skc10, X), nonexistent(skc10, skc9), skc11, skc11), skc11), skc11) -> skc11
% 16.86/15.99  865: ifeq4(of(skc10, skc11, skc15), nonexistent(skc10, skc9), ifeq4(of(skc10, skc11, skc15), nonexistent(skc10, skc9), skc11, skc11), skc11) -> skc11
% 16.86/15.99  866: ifeq4(of(skc10, skc11, skc15), nonexistent(skc10, skc9), ifeq4(of(skc10, X, skc15), nonexistent(skc10, skc9), ifeq4(forename(skc10, X), nonexistent(skc10, skc9), skc11, X), X), X) -> X
% 16.86/15.99  867: ifeq4(of(skc10, skc11, X), nonexistent(skc10, skc9), ifeq4(of(skc10, skc14, X), nonexistent(skc10, skc9), ifeq4(entity(skc10, X), nonexistent(skc10, skc9), skc11, skc14), skc14), skc14) -> skc14
% 16.86/15.99  868: ifeq4(of(skc10, X, Y), nonexistent(skc10, skc9), ifeq4(of(skc10, skc11, Y), nonexistent(skc10, skc9), ifeq4(entity(skc10, Y), nonexistent(skc10, skc9), ifeq4(forename(skc10, X), nonexistent(skc10, skc9), X, skc11), skc11), skc11), skc11) -> skc11
% 16.86/15.99  869: ifeq4(of(skc10, X, skc15), nonexistent(skc10, skc9), ifeq4(of(skc10, skc11, skc15), nonexistent(skc10, skc9), ifeq4(forename(skc10, X), nonexistent(skc10, skc9), X, skc11), skc11), skc11) -> skc11
% 16.86/15.99  870: ifeq4(of(skc10, skc14, X), nonexistent(skc10, skc9), ifeq4(of(skc10, skc11, X), nonexistent(skc10, skc9), ifeq4(entity(skc10, X), nonexistent(skc10, skc9), skc14, skc11), skc11), skc11) -> skc11
% 16.86/15.99  871: ifeq4(of(skc10, skc14, X), nonexistent(skc10, skc9), ifeq4(of(skc10, Y, X), nonexistent(skc10, skc9), ifeq4(entity(skc10, X), nonexistent(skc10, skc9), ifeq4(forename(skc10, Y), nonexistent(skc10, skc9), skc14, Y), Y), Y), Y) -> Y
% 16.86/15.99  872: ifeq4(of(skc10, skc14, skc12), nonexistent(skc10, skc9), ifeq4(of(skc10, X, skc12), nonexistent(skc10, skc9), ifeq4(forename(skc10, X), nonexistent(skc10, skc9), skc14, X), X), X) -> X
% 16.86/15.99  873: ifeq4(of(skc10, skc14, skc12), nonexistent(skc10, skc9), ifeq4(of(skc10, skc14, skc12), nonexistent(skc10, skc9), skc14, skc14), skc14) -> skc14
% 16.86/15.99  874: ifeq4(of(skc10, skc14, X), nonexistent(skc10, skc9), ifeq4(of(skc10, skc14, X), nonexistent(skc10, skc9), ifeq4(entity(skc10, X), nonexistent(skc10, skc9), skc14, skc14), skc14), skc14) -> skc14
% 16.86/15.99  875: ifeq4(of(skc10, X, skc12), nonexistent(skc10, skc9), ifeq4(of(skc10, Y, skc12), nonexistent(skc10, skc9), ifeq4(forename(skc10, X), nonexistent(skc10, skc9), ifeq4(forename(skc10, Y), nonexistent(skc10, skc9), X, Y), Y), Y), Y) -> Y
% 16.86/15.99  876: ifeq4(of(skc10, X, skc12), nonexistent(skc10, skc9), ifeq4(of(skc10, skc14, skc12), nonexistent(skc10, skc9), ifeq4(forename(skc10, X), nonexistent(skc10, skc9), X, skc14), skc14), skc14) -> skc14
% 16.86/15.99  877: ifeq4(of(skc10, X, skc15), nonexistent(skc10, skc9), ifeq4(of(skc10, Y, skc15), nonexistent(skc10, skc9), ifeq4(forename(skc10, X), nonexistent(skc10, skc9), ifeq4(forename(skc10, Y), nonexistent(skc10, skc9), X, Y), Y), Y), Y) -> Y
% 16.86/15.99  878: ifeq4(of(skc10, X, Y), nonexistent(skc10, skc9), ifeq4(of(skc10, skc14, Y), nonexistent(skc10, skc9), ifeq4(entity(skc10, Y), nonexistent(skc10, skc9), ifeq4(forename(skc10, X), nonexistent(skc10, skc9), X, skc14), skc14), skc14), skc14) -> skc14
% 16.86/15.99  879: ifeq4(theme(skc8, skc9, X), nonexistent(skc10, skc9), ifeq4(theme(skc8, Y, Z), nonexistent(skc10, skc9), ifeq4(proposition(skc8, X), nonexistent(skc10, skc9), ifeq4(proposition(skc8, Z), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, Y), nonexistent(skc10, skc9), X, Z), Z), Z), Z), Z) -> Z
% 16.86/15.99  880: ifeq4(theme(skc8, skc9, X), nonexistent(skc10, skc9), ifeq4(theme(skc8, skc9, Y), nonexistent(skc10, skc9), ifeq4(proposition(skc8, X), nonexistent(skc10, skc9), ifeq4(proposition(skc8, Y), nonexistent(skc10, skc9), X, Y), Y), Y), Y) -> Y
% 16.86/15.99  881: ifeq4(theme(skc8, skc9, X), nonexistent(skc10, skc9), ifeq4(theme(skc8, Y, skc10), nonexistent(skc10, skc9), ifeq4(proposition(skc8, X), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, Y), nonexistent(skc10, skc9), X, skc10), skc10), skc10), skc10) -> skc10
% 16.86/15.99  882: ifeq4(theme(skc8, X, Y), nonexistent(skc10, skc9), ifeq4(theme(skc8, skc9, Z), nonexistent(skc10, skc9), ifeq4(proposition(skc8, Y), nonexistent(skc10, skc9), ifeq4(proposition(skc8, Z), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, X), nonexistent(skc10, skc9), Y, Z), Z), Z), Z), Z) -> Z
% 16.86/15.99  883: ifeq4(theme(skc8, X, skc10), nonexistent(skc10, skc9), ifeq4(theme(skc8, skc9, Y), nonexistent(skc10, skc9), ifeq4(proposition(skc8, Y), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, X), nonexistent(skc10, skc9), skc10, Y), Y), Y), Y) -> Y
% 16.86/15.99  884: ifeq4(theme(skc8, X, skc10), nonexistent(skc10, skc9), ifeq4(theme(skc8, Y, Z), nonexistent(skc10, skc9), ifeq4(proposition(skc8, Z), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, X), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, Y), nonexistent(skc10, skc9), skc10, Z), Z), Z), Z), Z) -> Z
% 16.86/15.99  885: ifeq4(theme(skc8, X, skc10), nonexistent(skc10, skc9), ifeq4(theme(skc8, Y, skc10), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, X), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, Y), nonexistent(skc10, skc9), skc10, skc10), skc10), skc10), skc10) -> skc10
% 16.86/15.99  886: ifeq4(theme(skc8, X, Y), nonexistent(skc10, skc9), ifeq4(theme(skc8, Z, skc10), nonexistent(skc10, skc9), ifeq4(proposition(skc8, Y), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, X), nonexistent(skc10, skc9), ifeq4(desire_want(skc8, Z), nonexistent(skc10, skc9), Y, skc10), skc10), skc10), skc10), skc10) -> skc10
% 16.86/15.99  887: ifeq4(theme(skc10, skc9, X), nonexistent(skc10, skc9), ifeq4(theme(skc10, Y, Z), nonexistent(skc10, skc9), ifeq4(proposition(skc10, X), nonexistent(skc10, skc9), ifeq4(proposition(skc10, Z), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, Y), nonexistent(skc10, skc9), X, Z), Z), Z), Z), Z) -> Z
% 16.86/15.99  888: ifeq4(theme(skc10, skc9, X), nonexistent(skc10, skc9), ifeq4(theme(skc10, skc9, Y), nonexistent(skc10, skc9), ifeq4(proposition(skc10, X), nonexistent(skc10, skc9), ifeq4(proposition(skc10, Y), nonexistent(skc10, skc9), X, Y), Y), Y), Y) -> Y
% 16.86/15.99  889: ifeq4(theme(skc10, skc9, X), nonexistent(skc10, skc9), ifeq4(theme(skc10, Y, skc10), nonexistent(skc10, skc9), ifeq4(proposition(skc10, X), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, Y), nonexistent(skc10, skc9), X, skc10), skc10), skc10), skc10) -> skc10
% 16.86/15.99  890: ifeq4(theme(skc10, X, Y), nonexistent(skc10, skc9), ifeq4(theme(skc10, skc9, Z), nonexistent(skc10, skc9), ifeq4(proposition(skc10, Y), nonexistent(skc10, skc9), ifeq4(proposition(skc10, Z), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, X), nonexistent(skc10, skc9), Y, Z), Z), Z), Z), Z) -> Z
% 16.86/15.99  891: ifeq4(theme(skc10, X, skc10), nonexistent(skc10, skc9), ifeq4(theme(skc10, skc9, Y), nonexistent(skc10, skc9), ifeq4(proposition(skc10, Y), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, X), nonexistent(skc10, skc9), skc10, Y), Y), Y), Y) -> Y
% 16.86/15.99  892: ifeq4(theme(skc10, X, skc10), nonexistent(skc10, skc9), ifeq4(theme(skc10, Y, Z), nonexistent(skc10, skc9), ifeq4(proposition(skc10, Z), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, X), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, Y), nonexistent(skc10, skc9), skc10, Z), Z), Z), Z), Z) -> Z
% 16.86/15.99  893: ifeq4(theme(skc10, X, skc10), nonexistent(skc10, skc9), ifeq4(theme(skc10, Y, skc10), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, X), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, Y), nonexistent(skc10, skc9), skc10, skc10), skc10), skc10), skc10) -> skc10
% 16.86/15.99  894: ifeq4(theme(skc10, X, Y), nonexistent(skc10, skc9), ifeq4(theme(skc10, Z, skc10), nonexistent(skc10, skc9), ifeq4(proposition(skc10, Y), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, X), nonexistent(skc10, skc9), ifeq4(desire_want(skc10, Z), nonexistent(skc10, skc9), Y, skc10), skc10), skc10), skc10), skc10) -> skc10
% 16.86/15.99  896: ifeq(tuple(dance(X, Y), event(X, Y), desire_want(skc8, Z), proposition(skc8, X), accessible_world(skc8, X), present(X, Y), present(skc8, Z), agent(X, Y, skc15), agent(skc8, Z, skc15), theme(skc8, Z, X)), tuple(nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  897: ifeq(tuple(dance(X, Y), event(X, Y), nonexistent(skc10, skc9), proposition(skc8, X), accessible_world(skc8, X), present(X, Y), nonexistent(skc10, skc9), agent(X, Y, skc15), agent(skc8, skc9, skc15), theme(skc8, skc9, X)), tuple(nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  898: ifeq(tuple(dance(skc10, X), event(skc10, X), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), present(skc10, X), nonexistent(skc10, skc9), agent(skc10, X, skc15), agent(skc8, skc9, skc15), nonexistent(skc10, skc9)), tuple(nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  899: ifeq(tuple(dance(skc10, X), event(skc10, X), desire_want(skc8, Y), nonexistent(skc10, skc9), nonexistent(skc10, skc9), present(skc10, X), present(skc8, Y), agent(skc10, X, skc15), agent(skc8, Y, skc15), theme(skc8, Y, skc10)), tuple(nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  900: ifeq(tuple(nonexistent(skc10, skc9), nonexistent(skc10, skc9), desire_want(skc8, X), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), present(skc8, X), agent(skc10, skc13, skc15), agent(skc8, X, skc15), theme(skc8, X, skc10)), tuple(nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  901: ifeq(tuple(dance(skc8, skc9), nonexistent(skc10, skc9), desire_want(skc8, X), proposition(skc8, skc8), accessible_world(skc8, skc8), nonexistent(skc10, skc9), present(skc8, X), agent(skc8, skc9, skc15), agent(skc8, X, skc15), theme(skc8, X, skc8)), tuple(nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  902: ifeq(tuple(nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), agent(skc10, skc13, skc15), agent(skc8, skc9, skc15), nonexistent(skc10, skc9)), tuple(nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  903: ifeq(tuple(dance(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), agent(skc10, skc9, skc15), agent(skc8, skc9, skc15), nonexistent(skc10, skc9)), tuple(nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  904: ifeq(tuple(dance(skc10, skc9), nonexistent(skc10, skc9), desire_want(skc8, X), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), present(skc8, X), agent(skc10, skc9, skc15), agent(skc8, X, skc15), theme(skc8, X, skc10)), tuple(nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  905: ifeq(tuple(dance(skc8, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), proposition(skc8, skc8), accessible_world(skc8, skc8), nonexistent(skc10, skc9), nonexistent(skc10, skc9), agent(skc8, skc9, skc15), agent(skc8, skc9, skc15), theme(skc8, skc9, skc8)), tuple(nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9), nonexistent(skc10, skc9)), a, b) -> b
% 16.86/15.99  
%------------------------------------------------------------------------------