%------------------------------------------------------------------------------
% File : CiME---2.01
% Problem : NLP110-10 : TPTP v7.3.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : tptp2X_and_run_cime %s
% Computer : n186.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.5MB
% OS : Linux 3.10.0-862.11.6.el7.x86_64
% CPULimit : 300s
% DateTime : Wed Feb 27 13:36:00 EST 2019
% Result : Satisfiable 1.43s
% Output : Assurance 0s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NLP110-10 : TPTP v7.3.0. Released v7.3.0.
% 0.00/0.04 % Command : tptp2X_and_run_cime %s
% 0.03/0.27 % Computer : n186.star.cs.uiowa.edu
% 0.03/0.27 % Model : x86_64 x86_64
% 0.03/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.27 % Memory : 32218.5MB
% 0.03/0.27 % OS : Linux 3.10.0-862.11.6.el7.x86_64
% 0.03/0.27 % CPULimit : 300
% 0.03/0.27 % DateTime : Fri Feb 22 06:01:25 CST 2019
% 0.03/0.27 % CPUTime :
% 1.13/1.43 Processing problem /tmp/CiME_31528_n186.star.cs.uiowa.edu
% 1.13/1.43 #verbose 1;
% 1.13/1.43 let F = signature " b,a,skc5,skc6,skc8,skc4,true : constant; tuple : 3; tuple2 : 2; skf1 : 1; in : 3; nonreflexive : 2; past : 2; actual_world : 1; patient : 3; agent : 3; artifact : 2; building : 2; restaurant : 2; customer : 2; animate : 2; human : 2; living : 2; organism : 2; human_person : 2; impartial : 2; nonliving : 2; existent : 2; entity : 2; object : 2; substance_matter : 2; food : 2; beverage : 2; coffee : 2; drink : 2; unisex : 2; nonexistent : 2; specific : 2; singleton : 2; thing : 2; eventuality : 2; event : 2; see : 2; ifeq : 4; ifeq2 : 4; ifeq3 : 4;";
% 1.13/1.43 let X = vars "A B C U V X W";
% 1.13/1.43 let Axioms = equations F X "
% 1.13/1.43 ifeq3(A,A,B,C) = B;
% 1.13/1.43 ifeq2(A,A,B,C) = B;
% 1.13/1.43 ifeq(A,A,B,C) = B;
% 1.13/1.43 ifeq3(see(U,V),true,event(U,V),true) = true;
% 1.13/1.43 ifeq3(event(U,V),true,eventuality(U,V),true) = true;
% 1.13/1.43 ifeq3(eventuality(U,V),true,thing(U,V),true) = true;
% 1.13/1.43 ifeq3(thing(U,V),true,singleton(U,V),true) = true;
% 1.13/1.43 ifeq3(eventuality(U,V),true,specific(U,V),true) = true;
% 1.13/1.43 ifeq3(eventuality(U,V),true,nonexistent(U,V),true) = true;
% 1.13/1.43 ifeq3(eventuality(U,V),true,unisex(U,V),true) = true;
% 1.13/1.43 ifeq3(drink(U,V),true,event(U,V),true) = true;
% 1.13/1.43 ifeq3(coffee(U,V),true,beverage(U,V),true) = true;
% 1.13/1.43 ifeq3(beverage(U,V),true,food(U,V),true) = true;
% 1.13/1.43 ifeq3(food(U,V),true,substance_matter(U,V),true) = true;
% 1.13/1.43 ifeq3(substance_matter(U,V),true,object(U,V),true) = true;
% 1.13/1.43 ifeq3(object(U,V),true,entity(U,V),true) = true;
% 1.13/1.43 ifeq3(entity(U,V),true,thing(U,V),true) = true;
% 1.13/1.43 ifeq3(entity(U,V),true,specific(U,V),true) = true;
% 1.13/1.43 ifeq3(entity(U,V),true,existent(U,V),true) = true;
% 1.13/1.43 ifeq3(object(U,V),true,nonliving(U,V),true) = true;
% 1.13/1.43 ifeq3(object(U,V),true,impartial(U,V),true) = true;
% 1.13/1.43 ifeq3(object(U,V),true,unisex(U,V),true) = true;
% 1.13/1.43 ifeq3(human_person(U,V),true,organism(U,V),true) = true;
% 1.13/1.43 ifeq3(organism(U,V),true,entity(U,V),true) = true;
% 1.13/1.43 ifeq3(organism(U,V),true,impartial(U,V),true) = true;
% 1.13/1.43 ifeq3(organism(U,V),true,living(U,V),true) = true;
% 1.13/1.43 ifeq3(human_person(U,V),true,human(U,V),true) = true;
% 1.13/1.43 ifeq3(human_person(U,V),true,animate(U,V),true) = true;
% 1.13/1.43 ifeq3(customer(U,V),true,human_person(U,V),true) = true;
% 1.13/1.43 ifeq3(restaurant(U,V),true,building(U,V),true) = true;
% 1.13/1.43 ifeq3(building(U,V),true,artifact(U,V),true) = true;
% 1.13/1.43 ifeq3(artifact(U,V),true,object(U,V),true) = true;
% 1.13/1.43 ifeq3(agent(U,V,X),true,ifeq3(patient(U,V,W),true,ifeq3(drink(U,V),true,beverage(U,W),true),true),true) = true;
% 1.13/1.43 actual_world(skc4) = true;
% 1.13/1.43 coffee(skc4,skc8) = true;
% 1.13/1.43 human_person(skc4,skc6) = true;
% 1.13/1.43 event(skc4,skc5) = true;
% 1.13/1.43 past(skc4,skc5) = true;
% 1.13/1.43 nonreflexive(skc4,skc5) = true;
% 1.13/1.43 drink(skc4,skc5) = true;
% 1.13/1.43 agent(skc4,skc5,skc6) = true;
% 1.13/1.43 patient(skc4,skc5,skc8) = true;
% 1.13/1.43 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,ifeq3(customer(skc4,V),true,event(skc4,skf1(W)),true),true),true) = true;
% 1.13/1.43 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,ifeq3(customer(skc4,V),true,past(skc4,skf1(W)),true),true),true) = true;
% 1.13/1.43 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,ifeq3(customer(skc4,V),true,nonreflexive(skc4,skf1(W)),true),true),true) = true;
% 1.13/1.43 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,ifeq3(customer(skc4,V),true,see(skc4,skf1(W)),true),true),true) = true;
% 1.13/1.43 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,ifeq3(customer(skc4,V),true,agent(skc4,skf1(V),V),true),true),true) = true;
% 1.13/1.43 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,ifeq3(customer(skc4,V),true,patient(skc4,skf1(W),skc6),true),true),true) = true;
% 1.13/1.43 ifeq2(tuple2(nonliving(U,V),living(U,V)),tuple2(true,true),a,b) = b;
% 1.13/1.43 ifeq2(tuple2(nonexistent(U,V),existent(U,V)),tuple2(true,true),a,b) = b;
% 1.13/1.43 ifeq2(tuple2(nonliving(U,V),animate(U,V)),tuple2(true,true),a,b) = b;
% 1.13/1.43 ifeq(tuple(patient(U,V,W),nonreflexive(U,V),agent(U,V,W)),tuple(true,true,true),a,b) = b;
% 1.13/1.43 ";
% 1.13/1.43
% 1.13/1.43 let s1 = status F "
% 1.13/1.43 tuple lr_lex;
% 1.13/1.43 b lr_lex;
% 1.13/1.43 a lr_lex;
% 1.13/1.43 tuple2 lr_lex;
% 1.13/1.43 skf1 lr_lex;
% 1.13/1.43 in lr_lex;
% 1.13/1.43 nonreflexive lr_lex;
% 1.13/1.43 past lr_lex;
% 1.13/1.43 skc5 lr_lex;
% 1.13/1.43 skc6 lr_lex;
% 1.13/1.43 skc8 lr_lex;
% 1.13/1.43 actual_world lr_lex;
% 1.13/1.43 skc4 lr_lex;
% 1.13/1.43 patient lr_lex;
% 1.13/1.43 agent lr_lex;
% 1.13/1.43 artifact lr_lex;
% 1.21/1.43 building lr_lex;
% 1.21/1.43 restaurant lr_lex;
% 1.21/1.43 customer lr_lex;
% 1.21/1.43 animate lr_lex;
% 1.21/1.43 human lr_lex;
% 1.21/1.43 living lr_lex;
% 1.21/1.43 organism lr_lex;
% 1.21/1.43 human_person lr_lex;
% 1.21/1.43 impartial lr_lex;
% 1.21/1.43 nonliving lr_lex;
% 1.21/1.43 existent lr_lex;
% 1.21/1.43 entity lr_lex;
% 1.21/1.43 object lr_lex;
% 1.21/1.43 substance_matter lr_lex;
% 1.21/1.43 food lr_lex;
% 1.21/1.43 beverage lr_lex;
% 1.21/1.43 coffee lr_lex;
% 1.21/1.43 drink lr_lex;
% 1.21/1.43 unisex lr_lex;
% 1.21/1.43 nonexistent lr_lex;
% 1.21/1.43 specific lr_lex;
% 1.21/1.43 singleton lr_lex;
% 1.21/1.43 thing lr_lex;
% 1.21/1.43 eventuality lr_lex;
% 1.21/1.43 event lr_lex;
% 1.21/1.43 true lr_lex;
% 1.21/1.43 see lr_lex;
% 1.21/1.43 ifeq lr_lex;
% 1.21/1.43 ifeq2 lr_lex;
% 1.21/1.43 ifeq3 lr_lex;
% 1.21/1.43 ";
% 1.21/1.43
% 1.21/1.43 let p1 = precedence F "
% 1.21/1.43 singleton > human > ifeq3 > ifeq2 > ifeq > agent > patient > in > tuple > see > event > eventuality > thing > specific > nonexistent > unisex > drink > coffee > beverage > food > substance_matter > object > entity > existent > nonliving > impartial > human_person > organism > living > animate > customer > restaurant > building > artifact > past > nonreflexive > tuple2 > actual_world > skf1 > true > skc4 > skc8 > skc6 > skc5 > a > b";
% 1.21/1.43
% 1.21/1.43 let s2 = status F "
% 1.21/1.43 tuple mul;
% 1.21/1.43 b mul;
% 1.21/1.43 a mul;
% 1.21/1.43 tuple2 mul;
% 1.21/1.43 skf1 mul;
% 1.21/1.43 in mul;
% 1.21/1.43 nonreflexive mul;
% 1.21/1.43 past mul;
% 1.21/1.43 skc5 mul;
% 1.21/1.43 skc6 mul;
% 1.21/1.43 skc8 mul;
% 1.21/1.43 actual_world mul;
% 1.21/1.43 skc4 mul;
% 1.21/1.43 patient mul;
% 1.21/1.43 agent mul;
% 1.21/1.43 artifact mul;
% 1.21/1.43 building mul;
% 1.21/1.43 restaurant mul;
% 1.21/1.43 customer mul;
% 1.21/1.43 animate mul;
% 1.21/1.43 human mul;
% 1.21/1.43 living mul;
% 1.21/1.43 organism mul;
% 1.21/1.43 human_person mul;
% 1.21/1.43 impartial mul;
% 1.21/1.43 nonliving mul;
% 1.21/1.43 existent mul;
% 1.21/1.43 entity mul;
% 1.21/1.43 object mul;
% 1.21/1.43 substance_matter mul;
% 1.21/1.43 food mul;
% 1.21/1.43 beverage mul;
% 1.21/1.43 coffee mul;
% 1.21/1.43 drink mul;
% 1.21/1.43 unisex mul;
% 1.21/1.43 nonexistent mul;
% 1.21/1.43 specific mul;
% 1.21/1.43 singleton mul;
% 1.21/1.43 thing mul;
% 1.21/1.43 eventuality mul;
% 1.21/1.43 event mul;
% 1.21/1.43 true mul;
% 1.21/1.43 see mul;
% 1.21/1.43 ifeq mul;
% 1.21/1.43 ifeq2 mul;
% 1.21/1.43 ifeq3 mul;
% 1.21/1.43 ";
% 1.21/1.43
% 1.21/1.43 let p2 = precedence F "
% 1.21/1.43 singleton > human > ifeq3 > ifeq2 > ifeq > agent > patient > in > tuple > see > event > eventuality > thing > specific > nonexistent > unisex > drink > coffee > beverage > food > substance_matter > object > entity > existent > nonliving > impartial > human_person > organism > living > animate > customer > restaurant > building > artifact > past > nonreflexive > tuple2 > actual_world > skf1 > true = skc4 = skc8 = skc6 = skc5 = a = b";
% 1.21/1.43
% 1.21/1.43 let o_auto = AUTO Axioms;
% 1.21/1.43
% 1.21/1.43 let o = LEX o_auto (LEX (ACRPO s1 p1) (ACRPO s2 p2));
% 1.21/1.43
% 1.21/1.43 let Conjectures = equations F X " a = b;"
% 1.21/1.43 ;
% 1.21/1.43 (*
% 1.21/1.43 let Red_Axioms = normalize_equations Defining_rules Axioms;
% 1.21/1.43
% 1.21/1.43 let Red_Conjectures = normalize_equations Defining_rules Conjectures;
% 1.21/1.43 *)
% 1.21/1.43 #time on;
% 1.21/1.43
% 1.21/1.43 let res = prove_conj_by_ordered_completion o Axioms Conjectures;
% 1.21/1.43
% 1.21/1.43 #time off;
% 1.21/1.43
% 1.21/1.43
% 1.21/1.43 let status = if res then "unsatisfiable" else "satisfiable";
% 1.21/1.43 #quit;
% 1.21/1.43 Verbose level is now 1
% 1.21/1.43
% 1.21/1.43 F : signature = <signature>
% 1.21/1.43 X : variable_set = <variable set>
% 1.21/1.43
% 1.21/1.43 Axioms : (F,X) equations = { ifeq3(A,A,B,C) = B,
% 1.21/1.43 ifeq2(A,A,B,C) = B,
% 1.21/1.43 ifeq(A,A,B,C) = B,
% 1.21/1.43 ifeq3(see(U,V),true,event(U,V),true) = true,
% 1.21/1.43 ifeq3(event(U,V),true,eventuality(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(eventuality(U,V),true,thing(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(thing(U,V),true,singleton(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(eventuality(U,V),true,specific(U,V),true)
% 1.21/1.43 = true,
% 1.21/1.43 ifeq3(eventuality(U,V),true,nonexistent(U,V),true)
% 1.21/1.43 = true,
% 1.21/1.43 ifeq3(eventuality(U,V),true,unisex(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(drink(U,V),true,event(U,V),true) = true,
% 1.21/1.43 ifeq3(coffee(U,V),true,beverage(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(beverage(U,V),true,food(U,V),true) = true,
% 1.21/1.43 ifeq3(food(U,V),true,substance_matter(U,V),true)
% 1.21/1.43 = true,
% 1.21/1.43 ifeq3(substance_matter(U,V),true,object(U,V),true)
% 1.21/1.43 = true,
% 1.21/1.43 ifeq3(object(U,V),true,entity(U,V),true) = true,
% 1.21/1.43 ifeq3(entity(U,V),true,thing(U,V),true) = true,
% 1.21/1.43 ifeq3(entity(U,V),true,specific(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(entity(U,V),true,existent(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(object(U,V),true,nonliving(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(object(U,V),true,impartial(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(object(U,V),true,unisex(U,V),true) = true,
% 1.21/1.43 ifeq3(human_person(U,V),true,organism(U,V),true)
% 1.21/1.43 = true,
% 1.21/1.43 ifeq3(organism(U,V),true,entity(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(organism(U,V),true,impartial(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(organism(U,V),true,living(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(human_person(U,V),true,human(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(human_person(U,V),true,animate(U,V),true)
% 1.21/1.43 = true,
% 1.21/1.43 ifeq3(customer(U,V),true,human_person(U,V),true)
% 1.21/1.43 = true,
% 1.21/1.43 ifeq3(restaurant(U,V),true,building(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(building(U,V),true,artifact(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(artifact(U,V),true,object(U,V),true) =
% 1.21/1.43 true,
% 1.21/1.43 ifeq3(agent(U,V,X),true,ifeq3(patient(U,V,W),true,
% 1.21/1.43 ifeq3(drink(U,V),true,
% 1.21/1.43 beverage(U,W),true),true),true)
% 1.21/1.43 = true,
% 1.21/1.43 actual_world(skc4) = true,
% 1.21/1.43 coffee(skc4,skc8) = true,
% 1.21/1.43 human_person(skc4,skc6) = true,
% 1.21/1.43 event(skc4,skc5) = true,
% 1.21/1.43 past(skc4,skc5) = true,
% 1.21/1.43 nonreflexive(skc4,skc5) = true,
% 1.21/1.43 drink(skc4,skc5) = true,
% 1.21/1.43 agent(skc4,skc5,skc6) = true,
% 1.21/1.43 patient(skc4,skc5,skc8) = true,
% 1.21/1.43 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,
% 1.21/1.43 ifeq3(customer(skc4,V),true,
% 1.21/1.43 event(skc4,skf1(W)),true),true),true)
% 1.21/1.43 = true,
% 1.21/1.43 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,
% 1.21/1.43 ifeq3(customer(skc4,V),true,
% 1.21/1.43 past(skc4,skf1(W)),true),true),true)
% 1.21/1.43 = true,
% 1.21/1.43 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,
% 1.21/1.43 ifeq3(customer(skc4,V),true,
% 1.21/1.43 nonreflexive(skc4,
% 1.21/1.43 skf1(W)),true),true),true)
% 1.21/1.43 = true,
% 1.21/1.43 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,
% 1.21/1.43 ifeq3(customer(skc4,V),true,
% 1.21/1.43 see(skc4,skf1(W)),true),true),true)
% 1.21/1.43 = true,
% 1.21/1.43 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,
% 1.21/1.43 ifeq3(customer(skc4,V),true,
% 1.21/1.43 agent(skc4,skf1(V),V),true),true),true)
% 1.21/1.43 = true,
% 1.21/1.43 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,
% 1.21/1.43 ifeq3(customer(skc4,V),true,
% 1.21/1.48 patient(skc4,skf1(W),skc6),true),true),true)
% 1.21/1.48 = true,
% 1.21/1.48 ifeq2(tuple2(nonliving(U,V),living(U,V)),
% 1.21/1.48 tuple2(true,true),a,b) = b,
% 1.21/1.48 ifeq2(tuple2(nonexistent(U,V),existent(U,V)),
% 1.21/1.48 tuple2(true,true),a,b) = b,
% 1.21/1.48 ifeq2(tuple2(nonliving(U,V),animate(U,V)),
% 1.21/1.48 tuple2(true,true),a,b) = b,
% 1.21/1.48 ifeq(tuple(patient(U,V,W),nonreflexive(U,V),
% 1.21/1.48 agent(U,V,W)),tuple(true,true,true),a,b) =
% 1.21/1.48 b } (52 equation(s))
% 1.21/1.48 s1 : F status = <status>
% 1.21/1.48 p1 : F precedence = <precedence>
% 1.21/1.48 s2 : F status = <status>
% 1.21/1.48 p2 : F precedence = <precedence>
% 1.21/1.48 o_auto : F term_ordering = <term ordering>
% 1.21/1.48 o : F term_ordering = <term ordering>
% 1.21/1.48 Conjectures : (F,X) equations = { a = b } (1 equation(s))
% 1.21/1.48 time is now on
% 1.21/1.48
% 1.21/1.48 Initializing completion ...
% 1.21/1.48 New rule produced : [1] actual_world(skc4) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 51
% 1.21/1.48 Current number of rules: 1
% 1.21/1.48 New rule produced : [2] nonreflexive(skc4,skc5) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 50
% 1.21/1.48 Current number of rules: 2
% 1.21/1.48 New rule produced : [3] past(skc4,skc5) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 49
% 1.21/1.48 Current number of rules: 3
% 1.21/1.48 New rule produced : [4] human_person(skc4,skc6) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 48
% 1.21/1.48 Current number of rules: 4
% 1.21/1.48 New rule produced : [5] coffee(skc4,skc8) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 47
% 1.21/1.48 Current number of rules: 5
% 1.21/1.48 New rule produced : [6] drink(skc4,skc5) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 46
% 1.21/1.48 Current number of rules: 6
% 1.21/1.48 New rule produced : [7] event(skc4,skc5) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 45
% 1.21/1.48 Current number of rules: 7
% 1.21/1.48 New rule produced : [8] agent(skc4,skc5,skc6) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 44
% 1.21/1.48 Current number of rules: 8
% 1.21/1.48 New rule produced : [9] patient(skc4,skc5,skc8) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 43
% 1.21/1.48 Current number of rules: 9
% 1.21/1.48 New rule produced : [10] ifeq(A,A,B,C) -> B
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 42
% 1.21/1.48 Current number of rules: 10
% 1.21/1.48 New rule produced : [11] ifeq2(A,A,B,C) -> B
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 41
% 1.21/1.48 Current number of rules: 11
% 1.21/1.48 New rule produced : [12] ifeq3(A,A,B,C) -> B
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 40
% 1.21/1.48 Current number of rules: 12
% 1.21/1.48 New rule produced : [13] ifeq3(organism(U,V),true,living(U,V),true) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 39
% 1.21/1.48 Current number of rules: 13
% 1.21/1.48 New rule produced : [14] ifeq3(thing(U,V),true,singleton(U,V),true) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 38
% 1.21/1.48 Current number of rules: 14
% 1.21/1.48 New rule produced : [15] ifeq3(event(U,V),true,eventuality(U,V),true) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 37
% 1.21/1.48 Current number of rules: 15
% 1.21/1.48 New rule produced :
% 1.21/1.48 [16] ifeq3(customer(U,V),true,human_person(U,V),true) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 36
% 1.21/1.48 Current number of rules: 16
% 1.21/1.48 New rule produced :
% 1.21/1.48 [17] ifeq3(human_person(U,V),true,organism(U,V),true) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 35
% 1.21/1.48 Current number of rules: 17
% 1.21/1.48 New rule produced :
% 1.21/1.48 [18] ifeq3(human_person(U,V),true,human(U,V),true) -> true
% 1.21/1.48 Current number of equations to process: 0
% 1.21/1.48 Current number of ordered equations: 34
% 1.21/1.48 Current number of rules: 18
% 1.21/1.49 New rule produced :
% 1.21/1.49 [19] ifeq3(human_person(U,V),true,animate(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 33
% 1.21/1.49 Current number of rules: 19
% 1.21/1.49 New rule produced : [20] ifeq3(entity(U,V),true,thing(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 32
% 1.21/1.49 Current number of rules: 20
% 1.21/1.49 New rule produced : [21] ifeq3(entity(U,V),true,specific(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 31
% 1.21/1.49 Current number of rules: 21
% 1.21/1.49 New rule produced : [22] ifeq3(entity(U,V),true,existent(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 30
% 1.21/1.49 Current number of rules: 22
% 1.21/1.49 New rule produced : [23] ifeq3(drink(U,V),true,event(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 29
% 1.21/1.49 Current number of rules: 23
% 1.21/1.49 New rule produced :
% 1.21/1.49 [24] ifeq3(substance_matter(U,V),true,object(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 28
% 1.21/1.49 Current number of rules: 24
% 1.21/1.49 New rule produced : [25] ifeq3(see(U,V),true,event(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 27
% 1.21/1.49 Current number of rules: 25
% 1.21/1.49 New rule produced : [26] ifeq3(building(U,V),true,artifact(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 26
% 1.21/1.49 Current number of rules: 26
% 1.21/1.49 New rule produced : [27] ifeq3(beverage(U,V),true,food(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 25
% 1.21/1.49 Current number of rules: 27
% 1.21/1.49 New rule produced : [28] ifeq3(eventuality(U,V),true,thing(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 24
% 1.21/1.49 Current number of rules: 28
% 1.21/1.49 New rule produced :
% 1.21/1.49 [29] ifeq3(eventuality(U,V),true,specific(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 23
% 1.21/1.49 Current number of rules: 29
% 1.21/1.49 New rule produced :
% 1.21/1.49 [30] ifeq3(eventuality(U,V),true,nonexistent(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 22
% 1.21/1.49 Current number of rules: 30
% 1.21/1.49 New rule produced :
% 1.21/1.49 [31] ifeq3(eventuality(U,V),true,unisex(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 21
% 1.21/1.49 Current number of rules: 31
% 1.21/1.49 New rule produced :
% 1.21/1.49 [32] ifeq3(restaurant(U,V),true,building(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 20
% 1.21/1.49 Current number of rules: 32
% 1.21/1.49 New rule produced : [33] ifeq3(coffee(U,V),true,beverage(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 19
% 1.21/1.49 Current number of rules: 33
% 1.21/1.49 New rule produced : [34] ifeq3(object(U,V),true,unisex(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 18
% 1.21/1.49 Current number of rules: 34
% 1.21/1.49 New rule produced : [35] ifeq3(object(U,V),true,entity(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 17
% 1.21/1.49 Current number of rules: 35
% 1.21/1.49 New rule produced : [36] ifeq3(object(U,V),true,nonliving(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 16
% 1.21/1.49 Current number of rules: 36
% 1.21/1.49 New rule produced : [37] ifeq3(object(U,V),true,impartial(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 15
% 1.21/1.49 Current number of rules: 37
% 1.21/1.49 New rule produced : [38] ifeq3(artifact(U,V),true,object(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 14
% 1.21/1.49 Current number of rules: 38
% 1.21/1.49 New rule produced :
% 1.21/1.49 [39] ifeq3(food(U,V),true,substance_matter(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 13
% 1.21/1.49 Current number of rules: 39
% 1.21/1.49 New rule produced : [40] ifeq3(organism(U,V),true,entity(U,V),true) -> true
% 1.21/1.49 Current number of equations to process: 0
% 1.21/1.49 Current number of ordered equations: 12
% 1.21/1.50 Current number of rules: 40
% 1.21/1.50 New rule produced :
% 1.21/1.50 [41] ifeq3(organism(U,V),true,impartial(U,V),true) -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 11
% 1.21/1.50 Current number of rules: 41
% 1.21/1.50 New rule produced :
% 1.21/1.50 [42] ifeq2(tuple2(nonliving(U,V),animate(U,V)),tuple2(true,true),a,b) -> b
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 10
% 1.21/1.50 Current number of rules: 42
% 1.21/1.50 New rule produced :
% 1.21/1.50 [43] ifeq2(tuple2(nonexistent(U,V),existent(U,V)),tuple2(true,true),a,b) -> b
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 9
% 1.21/1.50 Current number of rules: 43
% 1.21/1.50 New rule produced :
% 1.21/1.50 [44] ifeq2(tuple2(nonliving(U,V),living(U,V)),tuple2(true,true),a,b) -> b
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 8
% 1.21/1.50 Current number of rules: 44
% 1.21/1.50 New rule produced :
% 1.21/1.50 [45]
% 1.21/1.50 ifeq(tuple(patient(U,V,W),nonreflexive(U,V),agent(U,V,W)),tuple(true,true,true),a,b)
% 1.21/1.50 -> b
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 7
% 1.21/1.50 Current number of rules: 45
% 1.21/1.50 New rule produced :
% 1.21/1.50 [46]
% 1.21/1.50 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,ifeq3(customer(skc4,V),true,
% 1.21/1.50 event(skc4,skf1(W)),true),true),true)
% 1.21/1.50 -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 6
% 1.21/1.50 Current number of rules: 46
% 1.21/1.50 New rule produced :
% 1.21/1.50 [47]
% 1.21/1.50 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,ifeq3(customer(skc4,V),true,
% 1.21/1.50 past(skc4,skf1(W)),true),true),true)
% 1.21/1.50 -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 5
% 1.21/1.50 Current number of rules: 47
% 1.21/1.50 New rule produced :
% 1.21/1.50 [48]
% 1.21/1.50 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,ifeq3(customer(skc4,V),true,
% 1.21/1.50 nonreflexive(skc4,
% 1.21/1.50 skf1(W)),true),true),true)
% 1.21/1.50 -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 4
% 1.21/1.50 Current number of rules: 48
% 1.21/1.50 New rule produced :
% 1.21/1.50 [49]
% 1.21/1.50 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,ifeq3(customer(skc4,V),true,
% 1.21/1.50 see(skc4,skf1(W)),true),true),true)
% 1.21/1.50 -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 3
% 1.21/1.50 Current number of rules: 49
% 1.21/1.50 New rule produced :
% 1.21/1.50 [50]
% 1.21/1.50 ifeq3(agent(U,V,X),true,ifeq3(patient(U,V,W),true,ifeq3(drink(U,V),true,
% 1.21/1.50 beverage(U,W),true),true),true)
% 1.21/1.50 -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 2
% 1.21/1.50 Current number of rules: 50
% 1.21/1.50 New rule produced :
% 1.21/1.50 [51]
% 1.21/1.50 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,ifeq3(customer(skc4,V),true,
% 1.21/1.50 agent(skc4,skf1(V),V),true),true),true)
% 1.21/1.50 -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 1
% 1.21/1.50 Current number of rules: 51
% 1.21/1.50 New rule produced :
% 1.21/1.50 [52]
% 1.21/1.50 ifeq3(in(skc4,V,U),true,ifeq3(restaurant(skc4,U),true,ifeq3(customer(skc4,V),true,
% 1.21/1.50 patient(skc4,skf1(W),skc6),true),true),true)
% 1.21/1.50 -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 0
% 1.21/1.50 Current number of rules: 52
% 1.21/1.50 New rule produced : [53] eventuality(skc4,skc5) -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 0
% 1.21/1.50 Current number of rules: 53
% 1.21/1.50 New rule produced : [54] ifeq3(customer(skc4,skc6),true,true,true) -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 0
% 1.21/1.50 Current number of rules: 54
% 1.21/1.50 New rule produced : [55] organism(skc4,skc6) -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 0
% 1.21/1.50 Current number of rules: 55
% 1.21/1.50 New rule produced : [56] human(skc4,skc6) -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.50 Current number of ordered equations: 0
% 1.21/1.50 Current number of rules: 56
% 1.21/1.50 New rule produced : [57] animate(skc4,skc6) -> true
% 1.21/1.50 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 57
% 1.21/1.57 New rule produced : [58] ifeq3(see(skc4,skc5),true,true,true) -> true
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 58
% 1.21/1.57 New rule produced : [59] beverage(skc4,skc8) -> true
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 59
% 1.21/1.57 New rule produced :
% 1.21/1.57 [60]
% 1.21/1.57 ifeq(tuple(patient(skc4,skc5,A),true,agent(skc4,skc5,A)),tuple(true,true,true),a,b)
% 1.21/1.57 -> b
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 60
% 1.21/1.57 New rule produced :
% 1.21/1.57 [61]
% 1.21/1.57 ifeq3(agent(skc4,skc5,A),true,ifeq3(patient(skc4,skc5,B),true,beverage(skc4,B),true),true)
% 1.21/1.57 -> true
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 61
% 1.21/1.57 New rule produced : [62] thing(skc4,skc5) -> true
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 62
% 1.21/1.57 New rule produced : [63] specific(skc4,skc5) -> true
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 63
% 1.21/1.57 New rule produced : [64] nonexistent(skc4,skc5) -> true
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 64
% 1.21/1.57 New rule produced : [65] unisex(skc4,skc5) -> true
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 65
% 1.21/1.57 New rule produced : [66] living(skc4,skc6) -> true
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 66
% 1.21/1.57 New rule produced : [67] entity(skc4,skc6) -> true
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 67
% 1.21/1.57 New rule produced : [68] impartial(skc4,skc6) -> true
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 68
% 1.21/1.57 New rule produced :
% 1.21/1.57 [69] ifeq2(tuple2(nonliving(skc4,skc6),true),tuple2(true,true),a,b) -> b
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 69
% 1.21/1.57 New rule produced : [70] food(skc4,skc8) -> true
% 1.21/1.57 Current number of equations to process: 0
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 70
% 1.21/1.57 New rule produced :
% 1.21/1.57 [71]
% 1.21/1.57 ifeq(tuple(patient(skc4,skc5,skc6),true,true),tuple(true,true,true),a,b) -> b
% 1.21/1.57 Current number of equations to process: 2
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 71
% 1.21/1.57 New rule produced :
% 1.21/1.57 [72]
% 1.21/1.57 ifeq(tuple(true,true,agent(skc4,skc5,skc8)),tuple(true,true,true),a,b) -> b
% 1.21/1.57 Current number of equations to process: 1
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 72
% 1.21/1.57 New rule produced :
% 1.21/1.57 [73] ifeq3(patient(skc4,skc5,A),true,beverage(skc4,A),true) -> true
% 1.21/1.57 Rule
% 1.21/1.57 [61]
% 1.21/1.57 ifeq3(agent(skc4,skc5,A),true,ifeq3(patient(skc4,skc5,B),true,beverage(skc4,B),true),true)
% 1.21/1.57 -> true collapsed.
% 1.21/1.57 Current number of equations to process: 2
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 72
% 1.21/1.57 New rule produced : [74] singleton(skc4,skc5) -> true
% 1.21/1.57 Current number of equations to process: 2
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 73
% 1.21/1.57 New rule produced : [75] ifeq3(entity(skc4,skc5),true,true,true) -> true
% 1.21/1.57 Current number of equations to process: 2
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 74
% 1.21/1.57 New rule produced : [76] ifeq3(agent(skc4,skc5,A),true,true,true) -> true
% 1.21/1.57 Current number of equations to process: 1
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 75
% 1.21/1.57 New rule produced :
% 1.21/1.57 [77] ifeq2(tuple2(true,existent(skc4,skc5)),tuple2(true,true),a,b) -> b
% 1.21/1.57 Current number of equations to process: 1
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 76
% 1.21/1.57 New rule produced : [78] ifeq3(object(skc4,skc5),true,true,true) -> true
% 1.21/1.57 Current number of equations to process: 1
% 1.21/1.57 Current number of ordered equations: 0
% 1.21/1.57 Current number of rules: 77
% 1.21/1.57 New rule produced : [79] thing(skc4,skc6) -> true
% 1.21/1.57 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 78
% 1.43/1.67 New rule produced : [80] specific(skc4,skc6) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 79
% 1.43/1.67 New rule produced : [81] existent(skc4,skc6) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 80
% 1.43/1.67 New rule produced : [82] ifeq3(object(skc4,skc6),true,true,true) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 81
% 1.43/1.67 New rule produced : [83] substance_matter(skc4,skc8) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 82
% 1.43/1.67 New rule produced : [84] singleton(skc4,skc6) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 83
% 1.43/1.67 New rule produced : [85] ifeq3(eventuality(skc4,skc6),true,true,true) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 84
% 1.43/1.67 New rule produced :
% 1.43/1.67 [86] ifeq2(tuple2(nonexistent(skc4,skc6),true),tuple2(true,true),a,b) -> b
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 85
% 1.43/1.67 New rule produced : [87] object(skc4,skc8) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 86
% 1.43/1.67 New rule produced : [88] unisex(skc4,skc8) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 87
% 1.43/1.67 New rule produced : [89] entity(skc4,skc8) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 88
% 1.43/1.67 New rule produced : [90] nonliving(skc4,skc8) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 89
% 1.43/1.67 New rule produced : [91] impartial(skc4,skc8) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 90
% 1.43/1.67 New rule produced : [92] ifeq3(artifact(skc4,skc8),true,true,true) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 91
% 1.43/1.67 New rule produced : [93] ifeq3(eventuality(skc4,skc8),true,true,true) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 92
% 1.43/1.67 New rule produced : [94] thing(skc4,skc8) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 93
% 1.43/1.67 New rule produced : [95] specific(skc4,skc8) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 94
% 1.43/1.67 New rule produced : [96] existent(skc4,skc8) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 95
% 1.43/1.67 New rule produced : [97] ifeq3(organism(skc4,skc8),true,true,true) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 96
% 1.43/1.67 New rule produced :
% 1.43/1.67 [98] ifeq2(tuple2(true,animate(skc4,skc8)),tuple2(true,true),a,b) -> b
% 1.43/1.67 Current number of equations to process: 2
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 97
% 1.43/1.67 New rule produced :
% 1.43/1.67 [99] ifeq2(tuple2(true,living(skc4,skc8)),tuple2(true,true),a,b) -> b
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 98
% 1.43/1.67 New rule produced : [100] singleton(skc4,skc8) -> true
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 99
% 1.43/1.67 New rule produced :
% 1.43/1.67 [101] ifeq2(tuple2(nonexistent(skc4,skc8),true),tuple2(true,true),a,b) -> b
% 1.43/1.67 Current number of equations to process: 1
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 100
% 1.43/1.67 New rule produced :
% 1.43/1.67 [102]
% 1.43/1.67 ifeq3(agent(skc4,A,B),true,ifeq3(patient(skc4,A,skc8),true,ifeq3(drink(skc4,A),true,true,true),true),true)
% 1.43/1.67 -> true
% 1.43/1.67 Current number of equations to process: 0
% 1.43/1.67 Current number of ordered equations: 0
% 1.43/1.67 Current number of rules: 101
% 1.43/1.67 Warning: some conjectures remain
% 1.43/1.67
% 1.43/1.67 Execution time: 0.190000 sec
% 1.43/1.67 res : bool = false
% 1.43/1.67 time is now off
% 1.43/1.67
% 1.43/1.67 status : string = "satisfiable"
% 1.43/1.67 % SZS status Satisfiable
% 1.43/1.67 CiME interrupted
%------------------------------------------------------------------------------