%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1.1 % Problem : LCL446-1 : TPTP v9.3.1. Released v3.2.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:09:35 PM UTC 2026 % Result : Unknown 0.10s 0.39s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL446-1 : TPTP v9.3.1. Released v3.2.0. % 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.10/0.36 % Computer : n017.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Sat Sep 5 02:41:51 UTC 2026 % 0.10/0.36 % CPUTime : % 0.10/0.36 Running /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.10/0.38 % 0.10/0.38 % Input Clauses: % 0.10/0.38 % 1:1:2:INP:TopTop: =(c_PropLog_Opl_Ofalse,c_PropLog_Opl_Ovar(x0,x1)) -> % 0.10/0.38 % 2:1:2:INP:TopTop: =(c_PropLog_Opl_Ovar(x0,x1),c_PropLog_Opl_Ofalse) -> % 0.10/0.38 % 3:1:3:INP:TopTopTop: =(c_PropLog_Opl_Ofalse,c_PropLog_Opl_Oop_A_N_62(x0,x1,x2)) -> % 0.10/0.38 % 4:1:3:INP:TopTopTop: =(c_PropLog_Opl_Oop_A_N_62(x0,x1,x2),c_PropLog_Opl_Ofalse) -> % 0.10/0.38 % 5:1:4:INP:TopTopTopTop: =(c_PropLog_Opl_Ovar(x0,x1),c_PropLog_Opl_Oop_A_N_62(x2,x3,x1)) -> % 0.10/0.38 % 6:1:4:INP:TopTopTopTop: =(c_PropLog_Opl_Oop_A_N_62(x0,x1,x2),c_PropLog_Opl_Ovar(x3,x2)) -> % 0.10/0.38 % 7:2:3:INP:TopTopTop: =(c_PropLog_Opl_Ovar(x0,x1),c_PropLog_Opl_Ovar(x2,x1)) -> =(x0,x2) % 0.10/0.38 % 8:2:5:INP:TopTopTopTopTop: =(c_PropLog_Opl_Oop_A_N_62(x0,x1,x2),c_PropLog_Opl_Oop_A_N_62(x3,x4,x2)) -> =(x0,x3) % 0.10/0.38 % 9:2:5:INP:TopTopTopTopTop: =(c_PropLog_Opl_Oop_A_N_62(x0,x1,x2),c_PropLog_Opl_Oop_A_N_62(x3,x4,x2)) -> =(x1,x4) % 0.10/0.38 % 10:2:3:INP:TopTopTop: c_in(x0,x1,tc_PropLog_Opl(x2)) -> c_in(x0,c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)) % 0.10/0.38 % 11:2:3:INP:TopTopTop: c_in(x0,c_Datatype_Oo2s(x1,x2),x2) -> =(x1,c_Datatype_Ooption_OSome(x0,x2)) % 0.10/0.38 % 12:1:2:INP:TopTop: -> c_in(x0,c_Datatype_Oo2s(c_Datatype_Ooption_OSome(x0,x1),x1),x1) % 0.10/0.38 % 13:2:2:INP:TopTop: -> =(x0,c_Datatype_Ooption_ONone),=(x0,c_Datatype_Ooption_OSome(c_Main_Onot__None__eq__iff1__1(x0,x1),x1)) % 0.10/0.38 % 14:2:2:INP:TopTop: -> =(x0,c_Datatype_Ooption_ONone),=(x0,c_Datatype_Ooption_OSome(c_Main_Onot__Some__eq__iff1__1(x0,x1),x1)) % 0.10/0.38 % 15:1:2:INP:TopTop: =(c_Datatype_Ooption_ONone,c_Datatype_Ooption_OSome(x0,x1)) -> % 0.10/0.38 % 16:1:2:INP:TopTop: =(c_Datatype_Ooption_OSome(x0,x1),c_Datatype_Ooption_ONone) -> % 0.10/0.38 % 17:2:3:INP:TopTopTop: =(c_Datatype_Ooption_OSome(x0,x1),c_Datatype_Ooption_OSome(x2,x1)) -> =(x0,x2) % 0.10/0.38 % 18:2:4:INP:TopTopTopTop: =(c_Datatype__Universe_OAtom(x0,x1,x2),c_Datatype__Universe_OAtom(x3,x1,x2)) -> =(x0,x3) % 0.10/0.38 % 19:1:5:INP:TopTopTopTopTop: =(c_Datatype__Universe_OAtom(x0,x1,x2),c_Datatype__Universe_OScons(x3,x4,x1,x2)) -> % 0.10/0.38 % 20:2:4:INP:TopTopTopTop: =(c_Datatype__Universe_OIn0(x0,x1,x2),c_Datatype__Universe_OIn0(x3,x1,x2)) -> =(x0,x3) % 0.10/0.38 % 21:1:4:INP:TopTopTopTop: =(c_Datatype__Universe_OIn0(x0,x1,x2),c_Datatype__Universe_OIn1(x3,x1,x2)) -> % 0.10/0.38 % 22:2:4:INP:TopTopTopTop: =(c_Datatype__Universe_OIn1(x0,x1,x2),c_Datatype__Universe_OIn1(x3,x1,x2)) -> =(x0,x3) % 0.10/0.38 % 23:1:4:INP:TopTopTopTop: =(c_Datatype__Universe_OIn1(x0,x1,x2),c_Datatype__Universe_OIn0(x3,x1,x2)) -> % 0.10/0.38 % 24:1:4:INP:TopTopTopTop: =(c_Datatype__Universe_OLeaf(x0,x1,x2),c_Datatype__Universe_ONumb(x3,x1,x2)) -> % 0.10/0.38 % 25:1:5:INP:TopTopTopTopTop: =(c_Datatype__Universe_OLeaf(x0,x1,x2),c_Datatype__Universe_OScons(x3,x4,x1,x2)) -> % 0.10/0.38 % 26:1:4:INP:TopTopTopTop: =(c_Datatype__Universe_ONumb(x0,x1,x2),c_Datatype__Universe_OLeaf(x3,x1,x2)) -> % 0.10/0.38 % 27:1:5:INP:TopTopTopTopTop: =(c_Datatype__Universe_ONumb(x0,x1,x2),c_Datatype__Universe_OScons(x3,x4,x1,x2)) -> % 0.10/0.38 % 28:2:6:INP:TopTopTopTopTopTop: =(c_Datatype__Universe_OScons(x0,x1,x2,x3),c_Datatype__Universe_OScons(x4,x5,x2,x3)) -> =(x0,x4) % 0.10/0.38 % 29:2:6:INP:TopTopTopTopTopTop: =(c_Datatype__Universe_OScons(x0,x1,x2,x3),c_Datatype__Universe_OScons(x4,x5,x2,x3)) -> =(x1,x5) % 0.10/0.38 % 30:1:5:INP:TopTopTopTopTop: =(c_Datatype__Universe_OScons(x0,x1,x2,x3),c_Datatype__Universe_OAtom(x4,x2,x3)) -> % 0.10/0.38 % 31:1:5:INP:TopTopTopTopTop: =(c_Datatype__Universe_OScons(x0,x1,x2,x3),c_Datatype__Universe_OLeaf(x4,x2,x3)) -> % 0.10/0.38 % 32:1:5:INP:TopTopTopTopTop: =(c_Datatype__Universe_OScons(x0,x1,x2,x3),c_Datatype__Universe_ONumb(x4,x2,x3)) -> % 0.10/0.38 % 33:2:1:INP:Top: c_Divides_Oop_Advd(c_0,x0,tc_nat) -> =(x0,c_0) % 0.10/0.38 % 34:1:0:INP:: -> c_Divides_Oop_Advd(c_0,c_0,tc_nat) % 0.10/0.38 % 35:2:3:INP:TopTopTop: =(c_emptyset,c_Equiv__Relations_Oquotient(x0,x1,x2)) -> =(x0,c_emptyset) % 0.10/0.38 % 36:1:2:INP:TopTop: -> =(c_emptyset,c_Equiv__Relations_Oquotient(c_emptyset,x0,x1)) % 0.10/0.38 % 37:2:3:INP:TopTopTop: =(c_Equiv__Relations_Oquotient(x0,x1,x2),c_emptyset) -> =(x0,c_emptyset) % 0.10/0.38 % 38:1:2:INP:TopTop: -> =(c_Equiv__Relations_Oquotient(c_emptyset,x0,x1),c_emptyset) % 0.10/0.38 % 39:1:0:INP:: =(c_Extraction_Osumbool_ORight,c_Extraction_Osumbool_OLeft) -> % 0.10/0.38 % 40:1:0:INP:: =(c_Extraction_Osumbool_ORight,c_Extraction_Osumbool_OLeft) -> % 0.10/0.38 % 41:2:4:INP:TopTopTopTop: c_in(c_minus(x0,c_insert(x1,x2,x3),tc_set(x3)),c_Finite__Set_OFinites,tc_set(x3)) -> c_in(c_minus(x0,x2,tc_set(x3)),c_Finite__Set_OFinites,tc_set(x3)) % 0.10/0.38 % 42:2:4:INP:TopTopTopTop: c_in(c_minus(x0,x1,tc_set(x2)),c_Finite__Set_OFinites,tc_set(x2)) -> c_in(c_minus(x0,c_insert(x3,x1,x2),tc_set(x2)),c_Finite__Set_OFinites,tc_set(x2)) % 0.10/0.38 % 43:2:2:INP:TopTop: c_in(c_Pow(x0,x1),c_Finite__Set_OFinites,tc_set(tc_set(x1))) -> c_in(x0,c_Finite__Set_OFinites,tc_set(x1)) % 0.10/0.38 % 44:2:2:INP:TopTop: c_in(x0,c_Finite__Set_OFinites,tc_set(x1)) -> c_in(c_Pow(x0,x1),c_Finite__Set_OFinites,tc_set(tc_set(x1))) % 0.10/0.38 % 45:2:3:INP:TopTopTop: c_in(c_union(x0,x1,x2),c_Finite__Set_OFinites,tc_set(x2)) -> c_in(x0,c_Finite__Set_OFinites,tc_set(x2)) % 0.10/0.38 % 46:2:3:INP:TopTopTop: c_in(c_union(x0,x1,x2),c_Finite__Set_OFinites,tc_set(x2)) -> c_in(x1,c_Finite__Set_OFinites,tc_set(x2)) % 0.10/0.38 % 47:3:3:INP:TopTopTop: c_in(x0,c_Finite__Set_OFinites,tc_set(x1)),c_in(x2,c_Finite__Set_OFinites,tc_set(x1)) -> c_in(c_union(x2,x0,x1),c_Finite__Set_OFinites,tc_set(x1)) % 0.10/0.38 % 48:2:3:INP:TopTopTop: c_in(c_Relation_Oconverse(x0,x1,x2),c_Finite__Set_OFinites,tc_set(tc_prod(x2,x1))) -> c_in(x0,c_Finite__Set_OFinites,tc_set(tc_prod(x1,x2))) % 0.10/0.38 % 49:2:3:INP:TopTopTop: c_in(x0,c_Finite__Set_OFinites,tc_set(tc_prod(x1,x2))) -> c_in(c_Relation_Oconverse(x0,x1,x2),c_Finite__Set_OFinites,tc_set(tc_prod(x2,x1))) % 0.10/0.38 % 50:2:3:INP:TopTopTop: c_Divides_Oop_Advd(x0,c_GCD_Ogcd(c_Pair(x1,x2,tc_nat,tc_nat)),tc_nat) -> c_Divides_Oop_Advd(x0,x1,tc_nat) % 0.10/0.38 % 51:2:3:INP:TopTopTop: c_Divides_Oop_Advd(x0,c_GCD_Ogcd(c_Pair(x1,x2,tc_nat,tc_nat)),tc_nat) -> c_Divides_Oop_Advd(x0,x2,tc_nat) % 0.10/0.38 % 52:3:3:INP:TopTopTop: c_Divides_Oop_Advd(x0,x1,tc_nat),c_Divides_Oop_Advd(x0,x2,tc_nat) -> c_Divides_Oop_Advd(x0,c_GCD_Ogcd(c_Pair(x2,x1,tc_nat,tc_nat)),tc_nat) % 0.10/0.38 % 53:1:0:INP:: c_in(c_UNIV,c_Finite__Set_OFinites,tc_set(tc_nat)) -> % 0.10/0.38 % 54:2:2:INP:TopTop: =(c_IntDef_Oint(x0),c_IntDef_Oint(x1)) -> =(x0,x1) % 0.10/0.38 % 55:2:2:INP:TopTop: c_Divides_Oop_Advd(x0,c_uminus(x1,tc_IntDef_Oint),tc_IntDef_Oint) -> c_Divides_Oop_Advd(x0,x1,tc_IntDef_Oint) % 0.10/0.38 % 56:2:2:INP:TopTop: c_Divides_Oop_Advd(x0,x1,tc_IntDef_Oint) -> c_Divides_Oop_Advd(x0,c_uminus(x1,tc_IntDef_Oint),tc_IntDef_Oint) % 0.10/0.38 % 57:2:1:INP:Top: c_Divides_Oop_Advd(c_0,x0,tc_IntDef_Oint) -> =(x0,c_0) % 0.10/0.38 % 58:1:0:INP:: -> c_Divides_Oop_Advd(c_0,c_0,tc_IntDef_Oint) % 0.10/0.38 % 59:2:2:INP:TopTop: c_Divides_Oop_Advd(c_uminus(x0,tc_IntDef_Oint),x1,tc_IntDef_Oint) -> c_Divides_Oop_Advd(x0,x1,tc_IntDef_Oint) % 0.10/0.38 % 60:2:2:INP:TopTop: c_Divides_Oop_Advd(x0,x1,tc_IntDef_Oint) -> c_Divides_Oop_Advd(c_uminus(x0,tc_IntDef_Oint),x1,tc_IntDef_Oint) % 0.10/0.38 % 61:1:3:INP:TopTopTop: c_in(c_Pair(x0,c_List_Olist_ONil,tc_List_Olist(x1),tc_List_Olist(x1)),c_List_Olex(x2,x1),tc_prod(tc_List_Olist(x1),tc_List_Olist(x1))) -> % 0.10/0.38 % 62:2:3:INP:TopTopTop: =(c_List_Olist_ONil,c_append(x0,x1,x2)) -> =(x0,c_List_Olist_ONil) % 0.10/0.38 % 63:2:3:INP:TopTopTop: =(c_List_Olist_ONil,c_append(x0,x1,x2)) -> =(x1,c_List_Olist_ONil) % 0.10/0.38 % 64:1:1:INP:Top: -> =(c_List_Olist_ONil,c_append(c_List_Olist_ONil,c_List_Olist_ONil,x0)) % 0.10/0.38 % 65:2:2:INP:TopTop: =(c_List_Olist_ONil,c_List_Orev(x0,x1)) -> =(x0,c_List_Olist_ONil) % 0.10/0.38 % 66:1:1:INP:Top: -> =(c_List_Olist_ONil,c_List_Orev(c_List_Olist_ONil,x0)) % 0.10/0.38 % 67:1:3:INP:TopTopTop: c_in(c_Pair(c_List_Olist_ONil,x0,tc_List_Olist(x1),tc_List_Olist(x1)),c_List_Olex(x2,x1),tc_prod(tc_List_Olist(x1),tc_List_Olist(x1))) -> % 0.10/0.38 % 68:2:5:INP:TopTopTopTopTop: =(c_append(x0,c_List_Olist_OCons(x1,c_List_Olist_ONil,x2),x2),c_append(x3,c_List_Olist_OCons(x4,c_List_Olist_ONil,x2),x2)) -> =(x0,x3) % 0.10/0.38 % 69:2:5:INP:TopTopTopTopTop: =(c_append(x0,c_List_Olist_OCons(x1,c_List_Olist_ONil,x2),x2),c_append(x3,c_List_Olist_OCons(x4,c_List_Olist_ONil,x2),x2)) -> =(x1,x4) % 0.10/0.38 % 70:2:4:INP:TopTopTopTop: c_in(c_append(x0,x1,x2),c_List_Olists(x3,x2),tc_List_Olist(x2)) -> c_in(x0,c_List_Olists(x3,x2),tc_List_Olist(x2)) % 0.10/0.38 % 71:2:4:INP:TopTopTopTop: c_in(c_append(x0,x1,x2),c_List_Olists(x3,x2),tc_List_Olist(x2)) -> c_in(x1,c_List_Olists(x3,x2),tc_List_Olist(x2)) % 0.10/0.38 % 72:3:4:INP:TopTopTopTop: c_in(x0,c_List_Olists(x1,x2),tc_List_Olist(x2)),c_in(x3,c_List_Olists(x1,x2),tc_List_Olist(x2)) -> c_in(c_append(x3,x0,x2),c_List_Olists(x1,x2),tc_List_Olist(x2)) % 0.10/0.38 % 73:2:3:INP:TopTopTop: =(c_append(x0,x1,x2),c_List_Olist_ONil) -> =(x0,c_List_Olist_ONil) % 0.10/0.38 % 74:2:3:INP:TopTopTop: =(c_append(x0,x1,x2),c_List_Olist_ONil) -> =(x1,c_List_Olist_ONil) % 0.10/0.38 % 75:1:1:INP:Top: -> =(c_append(c_List_Olist_ONil,c_List_Olist_ONil,x0),c_List_Olist_ONil) % 0.10/0.38 % 76:2:4:INP:TopTopTopTop: =(c_append(x0,x1,x2),c_append(x3,x1,x2)) -> =(x0,x3) % 0.10/0.38 % 77:2:3:INP:TopTopTop: =(c_append(x0,x1,x2),x1) -> =(x0,c_List_Olist_ONil) % 0.10/0.38 % 78:1:2:INP:TopTop: -> =(c_append(c_List_Olist_ONil,x0,x1),x0) % 0.10/0.38 % 79:2:3:INP:TopTopTop: =(c_append(x0,x1,x2),x0) -> =(x1,c_List_Olist_ONil) % 0.10/0.38 % 80:1:2:INP:TopTop: -> =(c_append(x0,c_List_Olist_ONil,x1),x0) % 0.10/0.38 % 81:2:4:INP:TopTopTopTop: =(c_List_Ochar_OChar(x0,x1),c_List_Ochar_OChar(x2,x3)) -> =(x0,x2) % 0.10/0.38 % 82:2:4:INP:TopTopTopTop: =(c_List_Ochar_OChar(x0,x1),c_List_Ochar_OChar(x2,x3)) -> =(x1,x3) % 0.10/0.38 % 83:2:2:INP:TopTop: =(c_Nat_Osize(x0,tc_List_Olist(x1)),c_0) -> =(x0,c_List_Olist_ONil) % 0.10/0.38 % 84:1:1:INP:Top: -> =(c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(x0)),c_0) % 0.10/0.38 % 85:1:1:INP:Top: c_less(c_0,c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(x0)),tc_nat) -> % 0.10/0.38 % 86:2:2:INP:TopTop: -> c_less(c_0,c_Nat_Osize(x0,tc_List_Olist(x1)),tc_nat),=(x0,c_List_Olist_ONil) % 0.10/0.38 % 87:2:2:INP:TopTop: =(c_Nat_Osize(c_List_Oremdups(x0,x1),tc_List_Olist(x1)),c_Nat_Osize(x0,tc_List_Olist(x1))) -> =(c_List_Oremdups(x0,x1),x0) % 0.10/0.38 % 88:2:2:INP:TopTop: =(c_List_Oremdups(x0,x1),x0) -> =(c_Nat_Osize(c_List_Oremdups(x0,x1),tc_List_Olist(x1)),c_Nat_Osize(x0,tc_List_Olist(x1))) % 0.10/0.38 % 89:1:3:INP:TopTopTop: =(c_List_Olist_ONil,c_List_Olist_OCons(x0,x1,x2)) -> % 0.10/0.38 % 90:1:3:INP:TopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Olist_ONil) -> % 0.10/0.38 % 91:2:5:INP:TopTopTopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Olist_OCons(x3,x4,x2)) -> =(x0,x3) % 0.10/0.38 % 92:2:5:INP:TopTopTopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Olist_OCons(x3,x4,x2)) -> =(x1,x4) % 0.10/0.38 % 93:2:4:INP:TopTopTopTop: =(c_List_Orev(x0,x1),c_List_Olist_OCons(x2,x3,x1)) -> =(x0,c_append(c_List_Orev(x3,x1),c_List_Olist_OCons(x2,c_List_Olist_ONil,x1),x1)) % 0.10/0.38 % 94:1:3:INP:TopTopTop: -> =(c_List_Orev(c_append(c_List_Orev(x0,x1),c_List_Olist_OCons(x2,c_List_Olist_ONil,x1),x1),x1),c_List_Olist_OCons(x2,x0,x1)) % 0.10/0.38 % 95:2:2:INP:TopTop: =(c_List_Orev(x0,x1),c_List_Olist_ONil) -> =(x0,c_List_Olist_ONil) % 0.10/0.38 % 96:1:1:INP:Top: -> =(c_List_Orev(c_List_Olist_ONil,x0),c_List_Olist_ONil) % 0.10/0.38 % 97:2:3:INP:TopTopTop: =(c_List_Orev(x0,x1),c_List_Orev(x2,x1)) -> =(x0,x2) % 0.10/0.38 % 98:2:4:INP:TopTopTopTop: =(c_append(x0,x1,x2),c_append(x0,x3,x2)) -> =(x1,x3) % 0.10/0.38 % 99:2:3:INP:TopTopTop: =(x0,c_append(x1,x0,x2)) -> =(x1,c_List_Olist_ONil) % 0.10/0.38 % 100:1:2:INP:TopTop: -> =(x0,c_append(c_List_Olist_ONil,x0,x1)) % 0.10/0.38 % 101:2:3:INP:TopTopTop: =(x0,c_append(x0,x1,x2)) -> =(x1,c_List_Olist_ONil) % 0.10/0.38 % 102:1:2:INP:TopTop: -> =(x0,c_append(x0,c_List_Olist_ONil,x1)) % 0.10/0.38 % 103:2:2:INP:TopTop: =(c_emptyset,c_List_Oset(x0,x1)) -> =(x0,c_List_Olist_ONil) % 0.10/0.38 % 104:1:1:INP:Top: -> =(c_emptyset,c_List_Oset(c_List_Olist_ONil,x0)) % 0.10/0.38 % 105:2:2:INP:TopTop: =(c_List_Oset(x0,x1),c_emptyset) -> =(x0,c_List_Olist_ONil) % 0.10/0.38 % 106:1:1:INP:Top: -> =(c_List_Oset(c_List_Olist_ONil,x0),c_emptyset) % 0.10/0.38 % 107:2:2:INP:TopTop: =(c_Suc(x0),c_Suc(x1)) -> =(x0,x1) % 0.10/0.38 % 108:2:2:INP:TopTop: c_lessequals(c_Suc(x0),c_Suc(x1),tc_nat) -> c_lessequals(x0,x1,tc_nat) % 0.10/0.38 % 109:2:2:INP:TopTop: c_lessequals(x0,x1,tc_nat) -> c_lessequals(c_Suc(x0),c_Suc(x1),tc_nat) % 0.10/0.38 % 110:2:2:INP:TopTop: c_less(c_Suc(x0),c_Suc(x1),tc_nat) -> c_less(x0,x1,tc_nat) % 0.10/0.38 % 111:2:2:INP:TopTop: c_less(x0,x1,tc_nat) -> c_less(c_Suc(x0),c_Suc(x1),tc_nat) % 0.10/0.38 % 112:1:1:INP:Top: =(c_Suc(x0),c_0) -> % 0.10/0.38 % 113:1:1:INP:Top: =(c_0,c_Suc(x0)) -> % 0.10/0.38 % 114:3:2:INP:TopTop: c_less(c_0,c_plus(x0,x1,tc_nat),tc_nat) -> c_less(c_0,x1,tc_nat),c_less(c_0,x0,tc_nat) % 0.10/0.38 % 115:2:2:INP:TopTop: c_less(c_0,x0,tc_nat) -> c_less(c_0,c_plus(x0,x1,tc_nat),tc_nat) % 0.10/0.38 % 116:2:2:INP:TopTop: c_less(c_0,x0,tc_nat) -> c_less(c_0,c_plus(x1,x0,tc_nat),tc_nat) % 0.10/0.38 % 117:2:2:INP:TopTop: =(c_plus(x0,x1,tc_nat),c_0) -> =(x0,c_0) % 0.10/0.38 % 118:2:2:INP:TopTop: =(c_plus(x0,x1,tc_nat),c_0) -> =(x1,c_0) % 0.10/0.38 % 119:1:0:INP:: -> =(c_plus(c_0,c_0,tc_nat),c_0) % 0.10/0.38 % 120:2:1:INP:Top: c_lessequals(x0,c_0,tc_nat) -> =(x0,c_0) % 0.10/0.38 % 121:1:0:INP:: -> c_lessequals(c_0,c_0,tc_nat) % 0.10/0.38 % 122:2:1:INP:Top: c_less(x0,c_Suc(c_0),tc_nat) -> =(x0,c_0) % 0.10/0.38 % 123:1:0:INP:: -> c_less(c_0,c_Suc(c_0),tc_nat) % 0.10/0.38 % 124:2:1:INP:Top: c_less(x0,c_1,tc_nat) -> =(x0,c_0) % 0.10/0.38 % 125:1:0:INP:: -> c_less(c_0,c_1,tc_nat) % 0.10/0.38 % 126:2:1:INP:Top: -> c_less(c_0,x0,tc_nat),=(x0,c_0) % 0.10/0.38 % 127:1:0:INP:: c_less(c_0,c_0,tc_nat) -> % 0.10/0.38 % 128:1:2:INP:TopTop: c_less(c_plus(x0,x1,tc_nat),x0,tc_nat) -> % 0.10/0.38 % 129:1:2:INP:TopTop: c_less(c_plus(x0,x1,tc_nat),x1,tc_nat) -> % 0.10/0.38 % 130:1:1:INP:Top: c_less(x0,c_0,tc_nat) -> % 0.10/0.38 % 131:1:0:INP:: =(c_Numeral_Obit_OB1,c_Numeral_Obit_OB0) -> % 0.10/0.38 % 132:1:0:INP:: =(c_Numeral_Obit_OB1,c_Numeral_Obit_OB0) -> % 0.10/0.38 % 133:2:2:INP:TopTop: class_Orderings_Oorder(x0),c_less(x1,x1,x0) -> % 0.10/0.38 % 134:2:6:INP:TopTopTopTopTopTop: =(c_Pair(x0,x1,x2,x3),c_Pair(x4,x5,x2,x3)) -> =(x0,x4) % 0.10/0.38 % 135:2:6:INP:TopTopTopTopTopTop: =(c_Pair(x0,x1,x2,x3),c_Pair(x4,x5,x2,x3)) -> =(x1,x5) % 0.10/0.38 % 136:1:2:INP:TopTop: -> c_in(c_Pair(x0,x0,x1,x1),c_Relation_OId,tc_prod(x1,x1)) % 0.10/0.38 % 137:2:5:INP:TopTopTopTopTop: c_in(x0,c_Relation_OImage(x1,c_insert(x2,c_emptyset,x3),x3,x4),x4) -> c_in(c_Pair(x2,x0,x3,x4),x1,tc_prod(x3,x4)) % 0.10/0.38 % 138:2:5:INP:TopTopTopTopTop: c_in(c_Pair(x0,x1,x2,x3),x4,tc_prod(x2,x3)) -> c_in(x1,c_Relation_OImage(x4,c_insert(x0,c_emptyset,x2),x2,x3),x3) % 0.10/0.38 % 139:2:5:INP:TopTopTopTopTop: c_in(c_Pair(x0,x1,x2,x3),c_Relation_Oconverse(x4,x3,x2),tc_prod(x2,x3)) -> c_in(c_Pair(x1,x0,x3,x2),x4,tc_prod(x3,x2)) % 0.10/0.38 % 140:2:5:INP:TopTopTopTopTop: c_in(c_Pair(x0,x1,x2,x3),x4,tc_prod(x2,x3)) -> c_in(c_Pair(x1,x0,x3,x2),c_Relation_Oconverse(x4,x2,x3),tc_prod(x3,x2)) % 0.10/0.38 % 141:2:3:INP:TopTopTop: c_in(c_Pair(x0,x1,x2,x2),c_Relation_OId,tc_prod(x2,x2)) -> =(x0,x1) % 0.10/0.38 % 142:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),=(c_SetInterval_OatLeast(x1,x0),c_SetInterval_OatLeast(x2,x0)) -> =(x1,x2) % 0.10/0.38 % 143:3:3:INP:TopTopTop: class_Orderings_Oord(x0),c_in(x1,c_SetInterval_OatLeast(x2,x0),x0) -> c_lessequals(x2,x1,x0) % 0.10/0.38 % 144:3:3:INP:TopTopTop: class_Orderings_Oord(x0),c_lessequals(x1,x2,x0) -> c_in(x2,c_SetInterval_OatLeast(x1,x0),x0) % 0.10/0.38 % 145:3:3:INP:TopTopTop: class_Orderings_Oorder(x0),c_lessequals(c_SetInterval_OatLeast(x1,x0),c_SetInterval_OatLeast(x2,x0),tc_set(x0)) -> c_lessequals(x2,x1,x0) % 0.10/0.38 % 146:3:3:INP:TopTopTop: class_Orderings_Oorder(x0),c_lessequals(x1,x2,x0) -> c_lessequals(c_SetInterval_OatLeast(x2,x0),c_SetInterval_OatLeast(x1,x0),tc_set(x0)) % 0.10/0.38 % 147:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),=(c_SetInterval_OatMost(x1,x0),c_SetInterval_OatMost(x2,x0)) -> =(x1,x2) % 0.10/0.38 % 148:3:3:INP:TopTopTop: class_Orderings_Oord(x0),c_in(x1,c_SetInterval_OatMost(x2,x0),x0) -> c_lessequals(x1,x2,x0) % 0.10/0.38 % 149:3:3:INP:TopTopTop: class_Orderings_Oord(x0),c_lessequals(x1,x2,x0) -> c_in(x1,c_SetInterval_OatMost(x2,x0),x0) % 0.10/0.38 % 150:3:3:INP:TopTopTop: class_Orderings_Oorder(x0),c_lessequals(c_SetInterval_OatMost(x1,x0),c_SetInterval_OatMost(x2,x0),tc_set(x0)) -> c_lessequals(x1,x2,x0) % 0.10/0.38 % 151:3:3:INP:TopTopTop: class_Orderings_Oorder(x0),c_lessequals(x1,x2,x0) -> c_lessequals(c_SetInterval_OatMost(x1,x0),c_SetInterval_OatMost(x2,x0),tc_set(x0)) % 0.10/0.38 % 152:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),=(c_SetInterval_OgreaterThan(x1,x0),c_SetInterval_OgreaterThan(x2,x0)) -> =(x1,x2) % 0.10/0.38 % 153:3:3:INP:TopTopTop: class_Orderings_Oord(x0),c_in(x1,c_SetInterval_OgreaterThan(x2,x0),x0) -> c_less(x2,x1,x0) % 0.10/0.38 % 154:3:3:INP:TopTopTop: class_Orderings_Oord(x0),c_less(x1,x2,x0) -> c_in(x2,c_SetInterval_OgreaterThan(x1,x0),x0) % 0.10/0.38 % 155:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_lessequals(c_SetInterval_OgreaterThan(x1,x0),c_SetInterval_OgreaterThan(x2,x0),tc_set(x0)) -> c_lessequals(x2,x1,x0) % 0.10/0.38 % 156:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_lessequals(x1,x2,x0) -> c_lessequals(c_SetInterval_OgreaterThan(x2,x0),c_SetInterval_OgreaterThan(x1,x0),tc_set(x0)) % 0.10/0.38 % 157:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),=(c_SetInterval_OlessThan(x1,x0),c_SetInterval_OlessThan(x2,x0)) -> =(x1,x2) % 0.10/0.38 % 158:3:3:INP:TopTopTop: class_Orderings_Oord(x0),c_in(x1,c_SetInterval_OlessThan(x2,x0),x0) -> c_less(x1,x2,x0) % 0.10/0.38 % 159:3:3:INP:TopTopTop: class_Orderings_Oord(x0),c_less(x1,x2,x0) -> c_in(x1,c_SetInterval_OlessThan(x2,x0),x0) % 0.10/0.38 % 160:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_lessequals(c_SetInterval_OlessThan(x1,x0),c_SetInterval_OlessThan(x2,x0),tc_set(x0)) -> c_lessequals(x1,x2,x0) % 0.10/0.38 % 161:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_lessequals(x1,x2,x0) -> c_lessequals(c_SetInterval_OlessThan(x1,x0),c_SetInterval_OlessThan(x2,x0),tc_set(x0)) % 0.10/0.38 % 162:2:3:INP:TopTopTop: c_in(x0,x1,x2),c_in(x0,c_uminus(x1,tc_set(x2)),x2) -> % 0.10/0.38 % 163:2:3:INP:TopTopTop: -> c_in(x0,x1,x2),c_in(x0,c_uminus(x1,tc_set(x2)),x2) % 0.10/0.38 % 164:2:3:INP:TopTopTop: =(c_uminus(x0,tc_set(x1)),c_uminus(x2,tc_set(x1))) -> =(x0,x2) % 0.10/0.38 % 165:2:3:INP:TopTopTop: c_lessequals(c_uminus(x0,tc_set(x1)),c_uminus(x2,tc_set(x1)),tc_set(x1)) -> c_lessequals(x2,x0,tc_set(x1)) % 0.10/0.38 % 166:2:3:INP:TopTopTop: c_lessequals(x0,x1,tc_set(x2)) -> c_lessequals(c_uminus(x1,tc_set(x2)),c_uminus(x0,tc_set(x2)),tc_set(x2)) % 0.10/0.38 % 167:2:4:INP:TopTopTopTop: c_in(x0,x1,x2),c_in(x0,c_minus(x3,x1,tc_set(x2)),x2) -> % 0.10/0.38 % 168:2:4:INP:TopTopTopTop: c_in(x0,c_minus(x1,x2,tc_set(x3)),x3) -> c_in(x0,x1,x3) % 0.10/0.38 % 169:3:4:INP:TopTopTopTop: c_in(x0,x1,x2) -> c_in(x0,x3,x2),c_in(x0,c_minus(x1,x3,tc_set(x2)),x2) % 0.10/0.38 % 170:2:4:INP:TopTopTopTop: c_in(x0,c_inter(x1,x2,x3),x3) -> c_in(x0,x2,x3) % 0.10/0.38 % 171:2:4:INP:TopTopTopTop: c_in(x0,c_inter(x1,x2,x3),x3) -> c_in(x0,x1,x3) % 0.10/0.38 % 172:3:4:INP:TopTopTopTop: c_in(x0,x1,x2),c_in(x0,x3,x2) -> c_in(x0,c_inter(x3,x1,x2),x2) % 0.10/0.38 % 173:3:4:INP:TopTopTopTop: c_in(x0,x1,tc_set(x2)),c_in(x3,c_Inter(x1,x2),x2) -> c_in(x3,x0,x2) % 0.10/0.38 % 174:2:3:INP:TopTopTop: c_in(x0,c_Pow(x1,x2),tc_set(x2)) -> c_lessequals(x0,x1,tc_set(x2)) % 0.10/0.38 % 175:2:3:INP:TopTopTop: c_lessequals(x0,x1,tc_set(x2)) -> c_in(x0,c_Pow(x1,x2),tc_set(x2)) % 0.10/0.38 % 176:1:0:INP:: =(c_UNIV,c_emptyset) -> % 0.10/0.38 % 177:2:4:INP:TopTopTopTop: c_in(x0,x1,x2) -> c_in(x0,c_union(x3,x1,x2),x2) % 0.10/0.38 % 178:2:4:INP:TopTopTopTop: c_in(x0,x1,x2) -> c_in(x0,c_union(x1,x3,x2),x2) % 0.10/0.38 % 179:3:4:INP:TopTopTopTop: c_in(x0,c_union(x1,x2,x3),x3) -> c_in(x0,x2,x3),c_in(x0,x1,x3) % 0.10/0.38 % 180:2:3:INP:TopTopTop: =(c_union(x0,x1,x2),c_emptyset) -> =(x0,c_emptyset) % 0.10/0.38 % 181:2:3:INP:TopTopTop: =(c_union(x0,x1,x2),c_emptyset) -> =(x1,c_emptyset) % 0.10/0.38 % 182:1:1:INP:Top: -> =(c_union(c_emptyset,c_emptyset,x0),c_emptyset) % 0.10/0.38 % 183:3:4:INP:TopTopTopTop: c_in(x0,x1,x2),c_in(x1,x3,tc_set(x2)) -> c_in(x0,c_Union(x3,x2),x2) % 0.10/0.38 % 184:1:2:INP:TopTop: c_in(x0,c_emptyset,x1) -> % 0.10/0.38 % 185:2:4:INP:TopTopTopTop: c_in(x0,x1,x2) -> c_in(x0,c_insert(x3,x1,x2),x2) % 0.10/0.38 % 186:1:3:INP:TopTopTop: -> c_in(x0,c_insert(x0,x1,x2),x2) % 0.10/0.38 % 187:3:4:INP:TopTopTopTop: c_in(x0,c_insert(x1,x2,x3),x3) -> c_in(x0,x2,x3),=(x0,x1) % 0.10/0.38 % 188:1:2:INP:TopTop: c_less(x0,c_emptyset,tc_set(x1)) -> % 0.10/0.38 % 189:2:4:INP:TopTopTopTop: =(c_insert(x0,x1,x2),c_insert(x3,c_emptyset,x2)) -> =(x0,x3) % 0.10/0.38 % 190:2:4:INP:TopTopTopTop: =(c_insert(x0,x1,x2),c_insert(x3,c_emptyset,x2)) -> c_lessequals(x1,c_insert(x3,c_emptyset,x2),tc_set(x2)) % 0.10/0.38 % 191:2:3:INP:TopTopTop: c_lessequals(x0,c_insert(x1,c_emptyset,x2),tc_set(x2)) -> =(c_insert(x1,x0,x2),c_insert(x1,c_emptyset,x2)) % 0.10/0.38 % 192:2:4:INP:TopTopTopTop: =(c_insert(x0,c_emptyset,x1),c_insert(x2,x3,x1)) -> =(x2,x0) % 0.10/0.38 % 193:2:4:INP:TopTopTopTop: =(c_insert(x0,c_emptyset,x1),c_insert(x2,x3,x1)) -> c_lessequals(x3,c_insert(x0,c_emptyset,x1),tc_set(x1)) % 0.10/0.38 % 194:2:3:INP:TopTopTop: c_lessequals(x0,c_insert(x1,c_emptyset,x2),tc_set(x2)) -> =(c_insert(x1,c_emptyset,x2),c_insert(x1,x0,x2)) % 0.10/0.38 % 195:2:4:INP:TopTopTopTop: =(c_Sum__Type_OInl(x0,x1,x2),c_Sum__Type_OInl(x3,x1,x2)) -> =(x0,x3) % 0.10/0.38 % 196:1:4:INP:TopTopTopTop: =(c_Sum__Type_OInl(x0,x1,x2),c_Sum__Type_OInr(x3,x2,x1)) -> % 0.10/0.38 % 197:2:4:INP:TopTopTopTop: =(c_Sum__Type_OInr(x0,x1,x2),c_Sum__Type_OInr(x3,x1,x2)) -> =(x0,x3) % 0.10/0.38 % 198:1:4:INP:TopTopTopTop: =(c_Sum__Type_OInr(x0,x1,x2),c_Sum__Type_OInl(x3,x2,x1)) -> % 0.10/0.38 % 199:2:2:INP:TopTop: c_Wellfounded__Recursion_Oacyclic(c_Relation_Oconverse(x0,x1,x1),x1) -> c_Wellfounded__Recursion_Oacyclic(x0,x1) % 0.10/0.38 % 200:2:2:INP:TopTop: c_Wellfounded__Recursion_Oacyclic(x0,x1) -> c_Wellfounded__Recursion_Oacyclic(c_Relation_Oconverse(x0,x1,x1),x1) % 0.10/0.38 % 201:2:4:INP:TopTopTopTop: c_Wellfounded__Recursion_Oacyclic(c_insert(c_Pair(x0,x1,x2,x2),x3,tc_prod(x2,x2)),x2) -> c_Wellfounded__Recursion_Oacyclic(x3,x2) % 0.10/0.38 % 202:2:4:INP:TopTopTopTop: c_Wellfounded__Recursion_Oacyclic(c_insert(c_Pair(x0,x1,x2,x2),x3,tc_prod(x2,x2)),x2),c_in(c_Pair(x1,x0,x2,x2),c_Transitive__Closure_Ortrancl(x3,x2),tc_prod(x2,x2)) -> % 0.10/0.38 % 203:3:4:INP:TopTopTopTop: c_Wellfounded__Recursion_Oacyclic(x0,x1) -> c_Wellfounded__Recursion_Oacyclic(c_insert(c_Pair(x2,x3,x1,x1),x0,tc_prod(x1,x1)),x1),c_in(c_Pair(x3,x2,x1,x1),c_Transitive__Closure_Ortrancl(x0,x1),tc_prod(x1,x1)) % 0.10/0.38 % 204:2:4:INP:TopTopTopTop: c_Wellfounded__Recursion_Owf(c_insert(c_Pair(x0,x1,x2,x2),x3,tc_prod(x2,x2)),x2) -> c_Wellfounded__Recursion_Owf(x3,x2) % 0.10/0.38 % 205:2:4:INP:TopTopTopTop: c_Wellfounded__Recursion_Owf(c_insert(c_Pair(x0,x1,x2,x2),x3,tc_prod(x2,x2)),x2),c_in(c_Pair(x1,x0,x2,x2),c_Transitive__Closure_Ortrancl(x3,x2),tc_prod(x2,x2)) -> % 0.10/0.38 % 206:3:4:INP:TopTopTopTop: c_Wellfounded__Recursion_Owf(x0,x1) -> c_Wellfounded__Recursion_Owf(c_insert(c_Pair(x2,x3,x1,x1),x0,tc_prod(x1,x1)),x1),c_in(c_Pair(x3,x2,x1,x1),c_Transitive__Closure_Ortrancl(x0,x1),tc_prod(x1,x1)) % 0.10/0.38 % 207:2:2:INP:TopTop: c_in(c_Pair(x0,x1,tc_nat,tc_nat),c_Wellfounded__Relations_Oless__than,tc_prod(tc_nat,tc_nat)) -> c_less(x0,x1,tc_nat) % 0.10/0.38 % 208:2:2:INP:TopTop: c_less(x0,x1,tc_nat) -> c_in(c_Pair(x0,x1,tc_nat,tc_nat),c_Wellfounded__Relations_Oless__than,tc_prod(tc_nat,tc_nat)) % 0.10/0.38 % 209:2:4:INP:TopTopTopTop: =(c_Datatype__Universe_OLeaf(x0,x1,x2),c_Datatype__Universe_OLeaf(x3,x1,x2)) -> =(x0,x3) % 0.10/0.38 % 210:2:4:INP:TopTopTopTop: =(c_Datatype__Universe_ONumb(x0,x1,x2),c_Datatype__Universe_ONumb(x3,x1,x2)) -> =(x0,x3) % 0.10/0.38 % 211:2:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Odprod(x1,x2,x3,x4),tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) -> =(x0,c_Pair(c_Datatype__Universe_OScons(c_Main_OdprodE__1(x0,x1,x2,x3,x4),c_Main_OdprodE__2(x0,x1,x2,x3,x4),x3,x4),c_Datatype__Universe_OScons(c_Main_OdprodE__3(x0,x1,x2,x3,x4),c_Main_OdprodE__4(x0,x1,x2,x3,x4),x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) % 0.10/0.38 % 212:2:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Odprod(x1,x2,x3,x4),tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) -> c_in(c_Pair(c_Main_OdprodE__2(x0,x1,x2,x3,x4),c_Main_OdprodE__4(x0,x1,x2,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4))),x2,tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) % 0.10/0.38 % 213:2:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Odprod(x1,x2,x3,x4),tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) -> c_in(c_Pair(c_Main_OdprodE__1(x0,x1,x2,x3,x4),c_Main_OdprodE__3(x0,x1,x2,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4))),x1,tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) % 0.10/0.38 % 214:3:8:INP:TopTopTopTopTopTopTopTop: c_in(c_Pair(x0,x1,tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3))),x4,tc_prod(tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3)))),c_in(c_Pair(x5,x6,tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3))),x7,tc_prod(tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3)))) -> c_in(c_Pair(c_Datatype__Universe_OScons(x5,x0,x2,x3),c_Datatype__Universe_OScons(x6,x1,x2,x3),tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3))),c_Datatype__Universe_Odprod(x7,x4,x2,x3),tc_prod(tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3)))) % 0.10/0.38 % 215:3:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Odsum(x1,x2,x3,x4),tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) -> =(x0,c_Pair(c_Datatype__Universe_OIn0(c_Main_OdsumE__1(x1,x0,x3,x4),x3,x4),c_Datatype__Universe_OIn0(c_Main_OdsumE__2(x1,x0,x3,x4),x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))),=(x0,c_Pair(c_Datatype__Universe_OIn1(c_Main_OdsumE__3(x2,x0,x3,x4),x3,x4),c_Datatype__Universe_OIn1(c_Main_OdsumE__4(x2,x0,x3,x4),x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) % 0.10/0.38 % 216:3:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Odsum(x1,x2,x3,x4),tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) -> c_in(c_Pair(c_Main_OdsumE__3(x2,x0,x3,x4),c_Main_OdsumE__4(x2,x0,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4))),x2,tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))),=(x0,c_Pair(c_Datatype__Universe_OIn0(c_Main_OdsumE__1(x1,x0,x3,x4),x3,x4),c_Datatype__Universe_OIn0(c_Main_OdsumE__2(x1,x0,x3,x4),x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) % 0.10/0.38 % 217:3:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Odsum(x1,x2,x3,x4),tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) -> c_in(c_Pair(c_Main_OdsumE__1(x1,x0,x3,x4),c_Main_OdsumE__2(x1,x0,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4))),x1,tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))),=(x0,c_Pair(c_Datatype__Universe_OIn1(c_Main_OdsumE__3(x2,x0,x3,x4),x3,x4),c_Datatype__Universe_OIn1(c_Main_OdsumE__4(x2,x0,x3,x4),x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) % 0.10/0.38 % 218:3:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Odsum(x1,x2,x3,x4),tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) -> c_in(c_Pair(c_Main_OdsumE__1(x1,x0,x3,x4),c_Main_OdsumE__2(x1,x0,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4))),x1,tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))),c_in(c_Pair(c_Main_OdsumE__3(x2,x0,x3,x4),c_Main_OdsumE__4(x2,x0,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4))),x2,tc_prod(tc_set(tc_Datatype__Universe_Onode(x3,x4)),tc_set(tc_Datatype__Universe_Onode(x3,x4)))) % 0.10/0.38 % 219:2:6:INP:TopTopTopTopTopTop: c_in(c_Pair(x0,x1,tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3))),x4,tc_prod(tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3)))) -> c_in(c_Pair(c_Datatype__Universe_OIn0(x0,x2,x3),c_Datatype__Universe_OIn0(x1,x2,x3),tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3))),c_Datatype__Universe_Odsum(x4,x5,x2,x3),tc_prod(tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3)))) % 0.10/0.38 % 220:2:6:INP:TopTopTopTopTopTop: c_in(c_Pair(x0,x1,tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3))),x4,tc_prod(tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3)))) -> c_in(c_Pair(c_Datatype__Universe_OIn1(x0,x2,x3),c_Datatype__Universe_OIn1(x1,x2,x3),tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3))),c_Datatype__Universe_Odsum(x5,x4,x2,x3),tc_prod(tc_set(tc_Datatype__Universe_Onode(x2,x3)),tc_set(tc_Datatype__Universe_Onode(x2,x3)))) % 0.10/0.38 % 221:2:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Ouprod(x1,x2,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4))) -> =(x0,c_Datatype__Universe_OScons(c_Main_OuprodE__1(x1,x2,x0,x3,x4),c_Main_OuprodE__2(x1,x2,x0,x3,x4),x3,x4)) % 0.10/0.38 % 222:2:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Ouprod(x1,x2,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4))) -> c_in(c_Main_OuprodE__2(x1,x2,x0,x3,x4),x2,tc_set(tc_Datatype__Universe_Onode(x3,x4))) % 0.10/0.38 % 223:2:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Ouprod(x1,x2,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4))) -> c_in(c_Main_OuprodE__1(x1,x2,x0,x3,x4),x1,tc_set(tc_Datatype__Universe_Onode(x3,x4))) % 0.10/0.38 % 224:3:6:INP:TopTopTopTopTopTop: c_in(x0,x1,tc_set(tc_Datatype__Universe_Onode(x2,x3))),c_in(x4,x5,tc_set(tc_Datatype__Universe_Onode(x2,x3))) -> c_in(c_Datatype__Universe_OScons(x4,x0,x2,x3),c_Datatype__Universe_Ouprod(x5,x1,x2,x3),tc_set(tc_Datatype__Universe_Onode(x2,x3))) % 0.10/0.38 % 225:3:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Ousum(x1,x2,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4))) -> =(x0,c_Datatype__Universe_OIn0(c_Main_OusumE__1(x1,x0,x3,x4),x3,x4)),=(x0,c_Datatype__Universe_OIn1(c_Main_OusumE__2(x2,x0,x3,x4),x3,x4)) % 0.10/0.38 % 226:3:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Ousum(x1,x2,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4))) -> c_in(c_Main_OusumE__2(x2,x0,x3,x4),x2,tc_set(tc_Datatype__Universe_Onode(x3,x4))),=(x0,c_Datatype__Universe_OIn0(c_Main_OusumE__1(x1,x0,x3,x4),x3,x4)) % 0.10/0.38 % 227:3:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Ousum(x1,x2,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4))) -> c_in(c_Main_OusumE__1(x1,x0,x3,x4),x1,tc_set(tc_Datatype__Universe_Onode(x3,x4))),=(x0,c_Datatype__Universe_OIn1(c_Main_OusumE__2(x2,x0,x3,x4),x3,x4)) % 0.10/0.38 % 228:3:5:INP:TopTopTopTopTop: c_in(x0,c_Datatype__Universe_Ousum(x1,x2,x3,x4),tc_set(tc_Datatype__Universe_Onode(x3,x4))) -> c_in(c_Main_OusumE__1(x1,x0,x3,x4),x1,tc_set(tc_Datatype__Universe_Onode(x3,x4))),c_in(c_Main_OusumE__2(x2,x0,x3,x4),x2,tc_set(tc_Datatype__Universe_Onode(x3,x4))) % 0.10/0.38 % 229:2:5:INP:TopTopTopTopTop: c_in(x0,x1,tc_set(tc_Datatype__Universe_Onode(x2,x3))) -> c_in(c_Datatype__Universe_OIn0(x0,x2,x3),c_Datatype__Universe_Ousum(x1,x4,x2,x3),tc_set(tc_Datatype__Universe_Onode(x2,x3))) % 0.10/0.38 % 230:2:5:INP:TopTopTopTopTop: c_in(x0,x1,tc_set(tc_Datatype__Universe_Onode(x2,x3))) -> c_in(c_Datatype__Universe_OIn1(x0,x2,x3),c_Datatype__Universe_Ousum(x4,x1,x2,x3),tc_set(tc_Datatype__Universe_Onode(x2,x3))) % 0.10/0.38 % 231:1:1:INP:Top: -> c_Divides_Oop_Advd(x0,c_0,tc_nat) % 0.10/0.38 % 232:1:1:INP:Top: -> c_Divides_Oop_Advd(c_Suc(c_0),x0,tc_nat) % 0.10/0.38 % 233:1:2:INP:TopTop: -> c_Divides_Oop_Advd(x0,c_times(x0,x1,tc_nat),tc_nat) % 0.10/0.38 % 234:1:2:INP:TopTop: -> c_Divides_Oop_Advd(x0,c_times(x1,x0,tc_nat),tc_nat) % 0.10/0.38 % 235:2:2:INP:TopTop: =(c_Divides_Oop_Amod(x0,x1,tc_nat),c_0) -> =(x0,c_times(x1,c_Main_Omod__eq__0D__dest__1(x1,x0),tc_nat)) % 0.10/0.38 % 236:1:1:INP:Top: -> c_in(c_emptyset,c_Finite__Set_OFinites,tc_set(x0)) % 0.10/0.38 % 237:2:3:INP:TopTopTop: c_in(x0,c_Finite__Set_OFinites,tc_set(x1)) -> c_in(c_insert(x2,x0,x1),c_Finite__Set_OFinites,tc_set(x1)) % 0.10/0.38 % 238:2:3:INP:TopTopTop: c_in(x0,c_Finite__Set_OFinites,tc_set(x1)) -> c_in(c_inter(x0,x2,x1),c_Finite__Set_OFinites,tc_set(x1)) % 0.10/0.38 % 239:2:3:INP:TopTopTop: c_in(x0,c_Finite__Set_OFinites,tc_set(x1)) -> c_in(c_inter(x2,x0,x1),c_Finite__Set_OFinites,tc_set(x1)) % 0.10/0.38 % 240:3:2:INP:TopTop: c_in(x0,c_Finite__Set_OFinites,tc_set(tc_set(x1))) -> c_in(c_Main_Ofinite__Union__1(x0,x1),x0,tc_set(x1)),c_in(c_Union(x0,x1),c_Finite__Set_OFinites,tc_set(x1)) % 0.10/0.38 % 241:3:2:INP:TopTop: c_in(x0,c_Finite__Set_OFinites,tc_set(tc_set(x1))),c_in(c_Main_Ofinite__Union__1(x0,x1),c_Finite__Set_OFinites,tc_set(x1)) -> c_in(c_Union(x0,x1),c_Finite__Set_OFinites,tc_set(x1)) % 0.10/0.38 % 242:1:2:INP:TopTop: -> c_Divides_Oop_Advd(c_GCD_Ogcd(c_Pair(x0,x1,tc_nat,tc_nat)),x0,tc_nat) % 0.10/0.38 % 243:1:2:INP:TopTop: -> c_Divides_Oop_Advd(c_GCD_Ogcd(c_Pair(x0,x1,tc_nat,tc_nat)),x1,tc_nat) % 0.10/0.38 % 244:4:4:INP:TopTopTopTop: c_Infinite__Set_Oatmost__one(x0,x1),c_in(x2,x0,x1),c_in(x3,x0,x1) -> =(x2,x3) % 0.10/0.38 % 245:1:2:INP:TopTop: -> c_lessequals(c_uminus(c_IntDef_Oint(x0),tc_IntDef_Oint),c_IntDef_Oint(x1),tc_IntDef_Oint) % 0.10/0.38 % 246:1:2:INP:TopTop: -> c_less(c_uminus(c_IntDef_Oint(c_Suc(x0)),tc_IntDef_Oint),c_IntDef_Oint(x1),tc_IntDef_Oint) % 0.10/0.38 % 247:1:1:INP:Top: -> c_Divides_Oop_Advd(x0,c_0,tc_IntDef_Oint) % 0.10/0.38 % 248:1:1:INP:Top: -> c_Divides_Oop_Advd(c_1,x0,tc_IntDef_Oint) % 0.10/0.38 % 249:1:2:INP:TopTop: -> c_Divides_Oop_Advd(x0,c_times(x0,x1,tc_IntDef_Oint),tc_IntDef_Oint) % 0.10/0.38 % 250:1:2:INP:TopTop: -> c_Divides_Oop_Advd(x0,c_times(x1,x0,tc_IntDef_Oint),tc_IntDef_Oint) % 0.10/0.38 % 251:2:2:INP:TopTop: =(c_Divides_Oop_Amod(x0,x1,tc_IntDef_Oint),c_0) -> =(x0,c_times(x1,c_Main_Ozmod__eq__0D__dest__1(x1,x0),tc_IntDef_Oint)) % 0.10/0.38 % 252:1:2:INP:TopTop: -> c_List_Odistinct(c_List_Oremdups(x0,x1),x1) % 0.10/0.38 % 253:1:2:INP:TopTop: -> c_in(c_List_Oset(x0,x1),c_Finite__Set_OFinites,tc_set(x1)) % 0.10/0.38 % 254:3:4:INP:TopTopTopTop: c_in(x0,c_List_Olists(x1,x2),tc_List_Olist(x2)),c_in(x3,c_List_Oset(x0,x2),x2) -> c_in(x3,x1,x2) % 0.10/0.38 % 255:2:3:INP:TopTopTop: -> c_in(x0,c_List_Olists(x1,x2),tc_List_Olist(x2)),c_in(c_Main_Oin__listsI__1(x1,x0,x2),c_List_Oset(x0,x2),x2) % 0.10/0.38 % 256:2:3:INP:TopTopTop: c_in(c_Main_Oin__listsI__1(x0,x1,x2),x0,x2) -> c_in(x1,c_List_Olists(x0,x2),tc_List_Olist(x2)) % 0.10/0.38 % 257:1:2:INP:TopTop: -> c_lessequals(c_Nat_Osize(c_List_Oremdups(x0,x1),tc_List_Olist(x1)),c_Nat_Osize(x0,tc_List_Olist(x1)),tc_nat) % 0.10/0.38 % 258:2:5:INP:TopTopTopTopTop: c_in(c_Pair(c_List_Olist_OCons(x0,x1,x2),x3,tc_List_Olist(x2),tc_List_Olist(x2)),c_List_Olistrel(x4,x2),tc_prod(tc_List_Olist(x2),tc_List_Olist(x2))) -> =(x3,c_List_Olist_OCons(c_Main_Olistrel__Cons1__1(x4,x3,x0,x1,x2),c_Main_Olistrel__Cons1__2(x4,x3,x0,x1,x2),x2)) % 0.10/0.38 % 259:2:5:INP:TopTopTopTopTop: c_in(c_Pair(c_List_Olist_OCons(x0,x1,x2),x3,tc_List_Olist(x2),tc_List_Olist(x2)),c_List_Olistrel(x4,x2),tc_prod(tc_List_Olist(x2),tc_List_Olist(x2))) -> c_in(c_Pair(x1,c_Main_Olistrel__Cons1__2(x4,x3,x0,x1,x2),tc_List_Olist(x2),tc_List_Olist(x2)),c_List_Olistrel(x4,x2),tc_prod(tc_List_Olist(x2),tc_List_Olist(x2))) % 0.10/0.38 % 260:2:5:INP:TopTopTopTopTop: c_in(c_Pair(c_List_Olist_OCons(x0,x1,x2),x3,tc_List_Olist(x2),tc_List_Olist(x2)),c_List_Olistrel(x4,x2),tc_prod(tc_List_Olist(x2),tc_List_Olist(x2))) -> c_in(c_Pair(x0,c_Main_Olistrel__Cons1__1(x4,x3,x0,x1,x2),x2,x2),x4,tc_prod(x2,x2)) % 0.10/0.38 % 261:2:5:INP:TopTopTopTopTop: c_in(c_Pair(x0,c_List_Olist_OCons(x1,x2,x3),tc_List_Olist(x3),tc_List_Olist(x3)),c_List_Olistrel(x4,x3),tc_prod(tc_List_Olist(x3),tc_List_Olist(x3))) -> =(x0,c_List_Olist_OCons(c_Main_Olistrel__Cons2__1(x4,x0,x1,x2,x3),c_Main_Olistrel__Cons2__2(x4,x0,x1,x2,x3),x3)) % 0.10/0.38 % 262:2:5:INP:TopTopTopTopTop: c_in(c_Pair(x0,c_List_Olist_OCons(x1,x2,x3),tc_List_Olist(x3),tc_List_Olist(x3)),c_List_Olistrel(x4,x3),tc_prod(tc_List_Olist(x3),tc_List_Olist(x3))) -> c_in(c_Pair(c_Main_Olistrel__Cons2__2(x4,x0,x1,x2,x3),x2,tc_List_Olist(x3),tc_List_Olist(x3)),c_List_Olistrel(x4,x3),tc_prod(tc_List_Olist(x3),tc_List_Olist(x3))) % 0.10/0.38 % 263:2:5:INP:TopTopTopTopTop: c_in(c_Pair(x0,c_List_Olist_OCons(x1,x2,x3),tc_List_Olist(x3),tc_List_Olist(x3)),c_List_Olistrel(x4,x3),tc_prod(tc_List_Olist(x3),tc_List_Olist(x3))) -> c_in(c_Pair(c_Main_Olistrel__Cons2__1(x4,x0,x1,x2,x3),x1,x3,x3),x4,tc_prod(x3,x3)) % 0.10/0.38 % 264:2:3:INP:TopTopTop: c_in(c_Pair(c_List_Olist_ONil,x0,tc_List_Olist(x1),tc_List_Olist(x1)),c_List_Olistrel(x2,x1),tc_prod(tc_List_Olist(x1),tc_List_Olist(x1))) -> =(x0,c_List_Olist_ONil) % 0.10/0.38 % 265:2:3:INP:TopTopTop: c_in(c_Pair(x0,c_List_Olist_ONil,tc_List_Olist(x1),tc_List_Olist(x1)),c_List_Olistrel(x2,x1),tc_prod(tc_List_Olist(x1),tc_List_Olist(x1))) -> =(x0,c_List_Olist_ONil) % 0.10/0.38 % 266:2:4:INP:TopTopTopTop: c_in(c_List_Olist_OCons(x0,x1,x2),c_List_Olists(x3,x2),tc_List_Olist(x2)) -> c_in(x1,c_List_Olists(x3,x2),tc_List_Olist(x2)) % 0.10/0.38 % 267:2:4:INP:TopTopTopTop: c_in(c_List_Olist_OCons(x0,x1,x2),c_List_Olists(x3,x2),tc_List_Olist(x2)) -> c_in(x0,x3,x2) % 0.10/0.38 % 268:3:4:INP:TopTopTopTop: c_in(x0,x1,x2),c_in(x3,c_List_Olists(x1,x2),tc_List_Olist(x2)) -> c_in(c_List_Olist_OCons(x0,x3,x2),c_List_Olists(x1,x2),tc_List_Olist(x2)) % 0.10/0.38 % 269:1:2:INP:TopTop: -> c_in(c_List_Olist_ONil,c_List_Olists(x0,x1),tc_List_Olist(x1)) % 0.10/0.38 % 270:2:2:INP:TopTop: c_Wellfounded__Recursion_Owf(x0,x1) -> c_Wellfounded__Recursion_Owf(c_List_Olenlex(x0,x1),tc_List_Olist(x1)) % 0.10/0.38 % 271:2:2:INP:TopTop: c_Wellfounded__Recursion_Owf(x0,x1) -> c_Wellfounded__Recursion_Owf(c_List_Olex(x0,x1),tc_List_Olist(x1)) % 0.10/0.38 % 272:1:1:INP:Top: -> c_lessequals(c_0,x0,tc_nat) % 0.10/0.38 % 273:1:1:INP:Top: -> c_less(x0,c_Suc(x0),tc_nat) % 0.10/0.38 % 274:1:1:INP:Top: c_less(x0,x0,tc_nat) -> % 0.10/0.38 % 275:1:1:INP:Top: -> c_less(c_0,c_Suc(x0),tc_nat) % 0.10/0.38 % 276:2:2:INP:TopTop: class_Orderings_Oorder(x0) -> c_lessequals(x1,x1,x0) % 0.10/0.38 % 277:2:4:INP:TopTopTopTop: c_in(x0,c_Relation_ODomain(x1,x2,x3),x2) -> c_in(c_Pair(x0,c_Main_ODomainE__1(x0,x1,x2,x3),x2,x3),x1,tc_prod(x2,x3)) % 0.10/0.38 % 278:2:5:INP:TopTopTopTopTop: c_in(c_Pair(x0,x1,x2,x3),x4,tc_prod(x2,x3)) -> c_in(x0,c_Relation_ODomain(x4,x2,x3),x2) % 0.10/0.38 % 279:2:2:INP:TopTop: c_in(x0,c_Relation_OId,tc_prod(x1,x1)) -> =(x0,c_Pair(c_Main_OIdE__1(x0,x1),c_Main_OIdE__1(x0,x1),x1,x1)) % 0.10/0.38 % 280:2:5:INP:TopTopTopTopTop: c_in(x0,c_Relation_OImage(x1,x2,x3,x4),x4) -> c_in(c_Main_OImageE__1(x2,x0,x1,x3,x4),x2,x3) % 0.10/0.38 % 281:2:5:INP:TopTopTopTopTop: c_in(x0,c_Relation_OImage(x1,x2,x3,x4),x4) -> c_in(c_Pair(c_Main_OImageE__1(x2,x0,x1,x3,x4),x0,x3,x4),x1,tc_prod(x3,x4)) % 0.10/0.38 % 282:3:6:INP:TopTopTopTopTopTop: c_in(x0,x1,x2),c_in(c_Pair(x0,x3,x2,x4),x5,tc_prod(x2,x4)) -> c_in(x3,c_Relation_OImage(x5,x1,x2,x4),x4) % 0.10/0.38 % 283:2:4:INP:TopTopTopTop: c_in(x0,c_Relation_ORange(x1,x2,x3),x3) -> c_in(c_Pair(c_Main_ORangeE__1(x0,x1,x3,x2),x0,x2,x3),x1,tc_prod(x2,x3)) % 0.10/0.38 % 284:2:5:INP:TopTopTopTopTop: c_in(c_Pair(x0,x1,x2,x3),x4,tc_prod(x2,x3)) -> c_in(x1,c_Relation_ORange(x4,x2,x3),x3) % 0.10/0.38 % 285:2:4:INP:TopTopTopTop: c_in(x0,c_Relation_Oconverse(x1,x2,x3),tc_prod(x3,x2)) -> c_in(c_Pair(c_Main_OconverseE__1(x1,x0,x2,x3),c_Main_OconverseE__2(x1,x0,x2,x3),x2,x3),x1,tc_prod(x2,x3)) % 0.10/0.38 % 286:2:4:INP:TopTopTopTop: c_in(x0,c_Relation_Oconverse(x1,x2,x3),tc_prod(x3,x2)) -> =(x0,c_Pair(c_Main_OconverseE__2(x1,x0,x2,x3),c_Main_OconverseE__1(x1,x0,x2,x3),x3,x2)) % 0.10/0.38 % 287:2:3:INP:TopTopTop: c_in(x0,c_Relation_Odiag(x1,x2),tc_prod(x2,x2)) -> =(x0,c_Pair(c_Main_OdiagE__1(x1,x0,x2),c_Main_OdiagE__1(x1,x0,x2),x2,x2)) % 0.10/0.38 % 288:2:3:INP:TopTopTop: c_in(x0,c_Relation_Odiag(x1,x2),tc_prod(x2,x2)) -> c_in(c_Main_OdiagE__1(x1,x0,x2),x1,x2) % 0.10/0.38 % 289:2:3:INP:TopTopTop: c_in(x0,x1,x2) -> c_in(c_Pair(x0,x0,x2,x2),c_Relation_Odiag(x1,x2),tc_prod(x2,x2)) % 0.10/0.38 % 290:2:6:INP:TopTopTopTopTopTop: c_in(x0,c_Relation_Orel__comp(x1,x2,x3,x4,x5),tc_prod(x5,x4)) -> c_in(c_Pair(c_Main_Orel__compE__2(x1,x2,x0,x3,x4,x5),c_Main_Orel__compE__3(x1,x2,x0,x3,x4,x5),x3,x4),x1,tc_prod(x3,x4)) % 0.10/0.38 % 291:2:6:INP:TopTopTopTopTopTop: c_in(x0,c_Relation_Orel__comp(x1,x2,x3,x4,x5),tc_prod(x5,x4)) -> c_in(c_Pair(c_Main_Orel__compE__1(x1,x2,x0,x3,x4,x5),c_Main_Orel__compE__2(x1,x2,x0,x3,x4,x5),x5,x3),x2,tc_prod(x5,x3)) % 0.10/0.38 % 292:2:6:INP:TopTopTopTopTopTop: c_in(x0,c_Relation_Orel__comp(x1,x2,x3,x4,x5),tc_prod(x5,x4)) -> =(x0,c_Pair(c_Main_Orel__compE__1(x1,x2,x0,x3,x4,x5),c_Main_Orel__compE__3(x1,x2,x0,x3,x4,x5),x5,x4)) % 0.10/0.38 % 293:3:8:INP:TopTopTopTopTopTopTopTop: c_in(c_Pair(x0,x1,x2,x3),x4,tc_prod(x2,x3)),c_in(c_Pair(x5,x0,x6,x2),x7,tc_prod(x6,x2)) -> c_in(c_Pair(x5,x1,x6,x3),c_Relation_Orel__comp(x4,x7,x2,x3,x6),tc_prod(x6,x3)) % 0.10/0.38 % 294:1:2:INP:TopTop: -> c_in(c_SetInterval_OatLeastAtMost(x0,x1,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)) % 0.10/0.38 % 295:1:2:INP:TopTop: -> c_in(c_SetInterval_OatLeastAtMost(x0,x1,tc_IntDef_Oint),c_Finite__Set_OFinites,tc_set(tc_IntDef_Oint)) % 0.10/0.38 % 296:1:2:INP:TopTop: -> c_in(c_SetInterval_OatLeastLessThan(x0,x1,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)) % 0.10/0.38 % 297:1:2:INP:TopTop: -> c_in(c_SetInterval_OatLeastLessThan(x0,x1,tc_IntDef_Oint),c_Finite__Set_OFinites,tc_set(tc_IntDef_Oint)) % 0.10/0.38 % 298:1:1:INP:Top: -> c_in(c_SetInterval_OatMost(x0,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)) % 0.10/0.38 % 299:1:2:INP:TopTop: -> c_in(c_SetInterval_OgreaterThanAtMost(x0,x1,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)) % 0.10/0.38 % 300:1:2:INP:TopTop: -> c_in(c_SetInterval_OgreaterThanAtMost(x0,x1,tc_IntDef_Oint),c_Finite__Set_OFinites,tc_set(tc_IntDef_Oint)) % 0.10/0.38 % 301:1:2:INP:TopTop: -> c_in(c_SetInterval_OgreaterThanLessThan(x0,x1,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)) % 0.10/0.38 % 302:1:2:INP:TopTop: -> c_in(c_SetInterval_OgreaterThanLessThan(x0,x1,tc_IntDef_Oint),c_Finite__Set_OFinites,tc_set(tc_IntDef_Oint)) % 0.10/0.38 % 303:1:1:INP:Top: -> c_in(c_SetInterval_OlessThan(x0,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)) % 0.10/0.38 % 304:2:3:INP:TopTopTop: -> c_in(x0,c_Inter(x1,x2),x2),c_in(c_Main_OInterI__1(x0,x1,x2),x1,tc_set(x2)) % 0.10/0.38 % 305:2:3:INP:TopTopTop: c_in(x0,c_Main_OInterI__1(x0,x1,x2),x2) -> c_in(x0,c_Inter(x1,x2),x2) % 0.10/0.38 % 306:1:2:INP:TopTop: -> c_in(x0,c_UNIV,x1) % 0.10/0.38 % 307:2:3:INP:TopTopTop: c_in(x0,c_Union(x1,x2),x2) -> c_in(c_Main_OUnionE__1(x0,x1,x2),x1,tc_set(x2)) % 0.10/0.38 % 308:2:3:INP:TopTopTop: c_in(x0,c_Union(x1,x2),x2) -> c_in(x0,c_Main_OUnionE__1(x0,x1,x2),x2) % 0.10/0.38 % 309:1:2:INP:TopTop: -> c_lessequals(c_emptyset,x0,tc_set(x1)) % 0.10/0.38 % 310:2:3:INP:TopTopTop: c_less(x0,x1,tc_set(x2)),c_lessequals(x1,x0,tc_set(x2)) -> % 0.10/0.38 % 311:2:3:INP:TopTopTop: c_less(x0,x1,tc_set(x2)) -> c_lessequals(x0,x1,tc_set(x2)) % 0.10/0.38 % 312:3:3:INP:TopTopTop: c_lessequals(x0,x1,tc_set(x2)) -> c_less(x0,x1,tc_set(x2)),=(x0,x1) % 0.10/0.38 % 313:2:3:INP:TopTopTop: c_in(x0,c_insert(x1,c_emptyset,x2),x2) -> =(x0,x1) % 0.10/0.38 % 314:1:2:INP:TopTop: -> c_in(x0,c_insert(x0,c_emptyset,x1),x1) % 0.10/0.38 % 315:2:3:INP:TopTopTop: =(c_insert(x0,c_emptyset,x1),c_insert(x2,c_emptyset,x1)) -> =(x0,x2) % 0.10/0.38 % 316:3:4:INP:TopTopTopTop: c_in(x0,x1,x2),c_lessequals(x1,x3,tc_set(x2)) -> c_in(x0,x3,x2) % 0.10/0.38 % 317:2:3:INP:TopTopTop: -> c_in(c_Main_OsubsetI__1(x0,x1,x2),x0,x2),c_lessequals(x0,x1,tc_set(x2)) % 0.10/0.38 % 318:2:3:INP:TopTopTop: c_in(c_Main_OsubsetI__1(x0,x1,x2),x1,x2) -> c_lessequals(x0,x1,tc_set(x2)) % 0.10/0.38 % 319:3:3:INP:TopTopTop: c_lessequals(x0,x1,tc_set(x2)),c_lessequals(x1,x0,tc_set(x2)) -> =(x1,x0) % 0.10/0.38 % 320:1:2:INP:TopTop: -> c_lessequals(x0,x0,tc_set(x1)) % 0.10/0.38 % 321:2:5:INP:TopTopTopTopTop: c_in(x0,x1,x2) -> c_in(c_Sum__Type_OInl(x0,x2,x3),c_Sum__Type_OPlus(x1,x4,x2,x3),tc_sum(x2,x3)) % 0.10/0.38 % 322:2:5:INP:TopTopTopTopTop: c_in(x0,x1,x2) -> c_in(c_Sum__Type_OInr(x0,x2,x3),c_Sum__Type_OPlus(x4,x1,x3,x2),tc_sum(x3,x2)) % 0.10/0.38 % 323:3:5:INP:TopTopTopTopTop: c_in(x0,c_Sum__Type_OPlus(x1,x2,x3,x4),tc_sum(x3,x4)) -> =(x0,c_Sum__Type_OInl(c_Main_OPlusE__1(x1,x0,x3,x4),x3,x4)),=(x0,c_Sum__Type_OInr(c_Main_OPlusE__2(x2,x0,x4,x3),x4,x3)) % 0.10/0.38 % 324:3:5:INP:TopTopTopTopTop: c_in(x0,c_Sum__Type_OPlus(x1,x2,x3,x4),tc_sum(x3,x4)) -> c_in(c_Main_OPlusE__2(x2,x0,x4,x3),x2,x4),=(x0,c_Sum__Type_OInl(c_Main_OPlusE__1(x1,x0,x3,x4),x3,x4)) % 0.10/0.38 % 325:3:5:INP:TopTopTopTopTop: c_in(x0,c_Sum__Type_OPlus(x1,x2,x3,x4),tc_sum(x3,x4)) -> c_in(c_Main_OPlusE__1(x1,x0,x3,x4),x1,x3),=(x0,c_Sum__Type_OInr(c_Main_OPlusE__2(x2,x0,x4,x3),x4,x3)) % 0.10/0.38 % 326:3:5:INP:TopTopTopTopTop: c_in(x0,c_Sum__Type_OPlus(x1,x2,x3,x4),tc_sum(x3,x4)) -> c_in(c_Main_OPlusE__1(x1,x0,x3,x4),x1,x3),c_in(c_Main_OPlusE__2(x2,x0,x4,x3),x2,x4) % 0.10/0.38 % 327:2:3:INP:TopTopTop: c_in(x0,x1,tc_prod(x2,x2)) -> c_in(x0,c_Transitive__Closure_Ortrancl(x1,x2),tc_prod(x2,x2)) % 0.10/0.38 % 328:1:3:INP:TopTopTop: -> c_in(c_Pair(x0,x0,x1,x1),c_Transitive__Closure_Ortrancl(x2,x1),tc_prod(x1,x1)) % 0.10/0.38 % 329:2:4:INP:TopTopTopTop: c_in(c_Pair(x0,x1,x2,x2),x3,tc_prod(x2,x2)) -> c_in(c_Pair(x0,x1,x2,x2),c_Transitive__Closure_Otrancl(x3,x2),tc_prod(x2,x2)) % 0.10/0.38 % 330:2:4:INP:TopTopTopTop: c_in(c_Pair(x0,x1,x2,x2),c_Transitive__Closure_Otrancl(x3,x2),tc_prod(x2,x2)) -> c_in(c_Pair(x0,x1,x2,x2),c_Transitive__Closure_Ortrancl(x3,x2),tc_prod(x2,x2)) % 0.10/0.38 % 331:1:1:INP:Top: -> c_Wellfounded__Recursion_Owf(c_emptyset,x0) % 0.10/0.38 % 332:1:0:INP:: -> c_Relation_Otrans(c_Wellfounded__Relations_Oless__than,tc_nat) % 0.10/0.38 % 333:3:4:INP:TopTopTopTop: c_Relation_Otrans(x0,x1),c_Relation_Otrans(x2,x3) -> c_Relation_Otrans(c_Wellfounded__Relations_Olex__prod(x2,x0,x3,x1),tc_prod(x3,x1)) % 0.10/0.38 % 334:1:0:INP:: -> c_Wellfounded__Recursion_Owf(c_Wellfounded__Relations_Oless__than,tc_nat) % 0.10/0.38 % 335:3:4:INP:TopTopTopTop: c_Wellfounded__Recursion_Owf(x0,x1),c_Wellfounded__Recursion_Owf(x2,x3) -> c_Wellfounded__Recursion_Owf(c_Wellfounded__Relations_Olex__prod(x2,x0,x3,x1),tc_prod(x3,x1)) % 0.10/0.38 % 336:2:1:INP:Top: class_Finite__Set_Ofinite(x0) -> class_Finite__Set_Ofinite(tc_Datatype_Ooption(x0)) % 0.10/0.38 % 337:1:0:INP:: -> class_HOL_Ominus(tc_IntDef_Oint) % 0.10/0.38 % 338:1:0:INP:: -> class_HOL_Oone(tc_IntDef_Oint) % 0.10/0.38 % 339:1:0:INP:: -> class_Ring__and__Field_Osemiring(tc_IntDef_Oint) % 0.10/0.38 % 340:1:0:INP:: -> class_Ring__and__Field_Ocomm__semiring(tc_IntDef_Oint) % 0.10/0.38 % 341:1:0:INP:: -> class_OrderedGroup_Ocomm__monoid__add(tc_IntDef_Oint) % 0.10/0.38 % 342:1:0:INP:: -> class_Ring__and__Field_Osemiring__0(tc_IntDef_Oint) % 0.10/0.38 % 343:1:0:INP:: -> class_Ring__and__Field_Ocomm__semiring__0(tc_IntDef_Oint) % 0.10/0.38 % 344:1:0:INP:: -> class_OrderedGroup_Ocancel__semigroup__add(tc_IntDef_Oint) % 0.10/0.38 % 345:1:0:INP:: -> class_OrderedGroup_Ocancel__ab__semigroup__add(tc_IntDef_Oint) % 0.10/0.38 % 346:1:0:INP:: -> class_OrderedGroup_Oab__group__add(tc_IntDef_Oint) % 0.10/0.38 % 347:1:0:INP:: -> class_Ring__and__Field_Osemiring__0__cancel(tc_IntDef_Oint) % 0.10/0.38 % 348:1:0:INP:: -> class_Ring__and__Field_Oring(tc_IntDef_Oint) % 0.10/0.38 % 349:1:0:INP:: -> class_HOL_Oplus(tc_IntDef_Oint) % 0.10/0.38 % 350:1:0:INP:: -> class_Ring__and__Field_Ocomm__semiring__0__cancel(tc_IntDef_Oint) % 0.10/0.38 % 351:1:0:INP:: -> class_Ring__and__Field_Ocomm__ring(tc_IntDef_Oint) % 0.10/0.38 % 352:1:0:INP:: -> class_Ring__and__Field_Oaxclass__0__neq__1(tc_IntDef_Oint) % 0.10/0.38 % 353:1:0:INP:: -> class_OrderedGroup_Omonoid__mult(tc_IntDef_Oint) % 0.10/0.38 % 354:1:0:INP:: -> class_OrderedGroup_Ocomm__monoid__mult(tc_IntDef_Oint) % 0.10/0.38 % 355:1:0:INP:: -> class_Ring__and__Field_Osemiring__1(tc_IntDef_Oint) % 0.10/0.38 % 356:1:0:INP:: -> class_Ring__and__Field_Ocomm__semiring__1(tc_IntDef_Oint) % 0.10/0.38 % 357:1:0:INP:: -> class_Ring__and__Field_Osemiring__1__cancel(tc_IntDef_Oint) % 0.10/0.38 % 358:1:0:INP:: -> class_Ring__and__Field_Oring__1(tc_IntDef_Oint) % 0.10/0.38 % 359:1:0:INP:: -> class_Ring__and__Field_Ocomm__semiring__1__cancel(tc_IntDef_Oint) % 0.10/0.38 % 360:1:0:INP:: -> class_HOL_Otimes(tc_IntDef_Oint) % 0.10/0.38 % 361:1:0:INP:: -> class_Ring__and__Field_Ocomm__ring__1(tc_IntDef_Oint) % 0.10/0.38 % 362:1:0:INP:: -> class_Orderings_Oorder(tc_IntDef_Oint) % 0.10/0.38 % 363:1:0:INP:: -> class_LOrder_Omeet__semilorder(tc_IntDef_Oint) % 0.10/0.38 % 364:1:0:INP:: -> class_LOrder_Ojoin__semilorder(tc_IntDef_Oint) % 0.10/0.38 % 365:1:0:INP:: -> class_LOrder_Olorder(tc_IntDef_Oint) % 0.10/0.38 % 366:1:0:INP:: -> class_Orderings_Olinorder(tc_IntDef_Oint) % 0.10/0.38 % 367:1:0:INP:: -> class_OrderedGroup_Opordered__ab__semigroup__add(tc_IntDef_Oint) % 0.10/0.38 % 368:1:0:INP:: -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_IntDef_Oint) % 0.10/0.38 % 369:1:0:INP:: -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_IntDef_Oint) % 0.10/0.38 % 370:1:0:INP:: -> class_OrderedGroup_Oordered__cancel__ab__semigroup__add(tc_IntDef_Oint) % 0.10/0.38 % 371:1:0:INP:: -> class_HOL_Ozero(tc_IntDef_Oint) % 0.10/0.38 % 372:1:0:INP:: -> class_Ring__and__Field_Opordered__semiring(tc_IntDef_Oint) % 0.10/0.38 % 373:1:0:INP:: -> class_Ring__and__Field_Opordered__cancel__semiring(tc_IntDef_Oint) % 0.10/0.38 % 374:1:0:INP:: -> class_Ring__and__Field_Oordered__semiring__strict(tc_IntDef_Oint) % 0.10/0.38 % 375:1:0:INP:: -> class_Ring__and__Field_Opordered__comm__semiring(tc_IntDef_Oint) % 0.10/0.38 % 376:1:0:INP:: -> class_Ring__and__Field_Opordered__cancel__comm__semiring(tc_IntDef_Oint) % 0.10/0.38 % 377:1:0:INP:: -> class_Ring__and__Field_Oordered__comm__semiring__strict(tc_IntDef_Oint) % 0.10/0.38 % 378:1:0:INP:: -> class_Ring__and__Field_Oaxclass__abs__if(tc_IntDef_Oint) % 0.10/0.38 % 379:1:0:INP:: -> class_OrderedGroup_Opordered__ab__group__add(tc_IntDef_Oint) % 0.10/0.38 % 380:1:0:INP:: -> class_OrderedGroup_Olordered__ab__group(tc_IntDef_Oint) % 0.10/0.38 % 381:1:0:INP:: -> class_Ring__and__Field_Opordered__ring(tc_IntDef_Oint) % 0.10/0.38 % 382:1:0:INP:: -> class_Orderings_Oord(tc_IntDef_Oint) % 0.10/0.38 % 383:1:0:INP:: -> class_OrderedGroup_Olordered__ab__group__abs(tc_IntDef_Oint) % 0.10/0.38 % 384:1:0:INP:: -> class_OrderedGroup_Olordered__ab__group__meet(tc_IntDef_Oint) % 0.10/0.38 % 385:1:0:INP:: -> class_OrderedGroup_Olordered__ab__group__join(tc_IntDef_Oint) % 0.10/0.38 % 386:1:0:INP:: -> class_Ring__and__Field_Olordered__ring(tc_IntDef_Oint) % 0.10/0.38 % 387:1:0:INP:: -> class_Ring__and__Field_Oaxclass__no__zero__divisors(tc_IntDef_Oint) % 0.10/0.38 % 388:1:0:INP:: -> class_Ring__and__Field_Oordered__ring__strict(tc_IntDef_Oint) % 0.10/0.38 % 389:1:0:INP:: -> class_Ring__and__Field_Oordered__semidom(tc_IntDef_Oint) % 0.10/0.38 % 390:1:0:INP:: -> class_Ring__and__Field_Oidom(tc_IntDef_Oint) % 0.10/0.38 % 391:1:0:INP:: -> class_Ring__and__Field_Oordered__idom(tc_IntDef_Oint) % 0.10/0.38 % 392:1:0:INP:: -> class_Numeral_Onumber(tc_IntDef_Oint) % 0.10/0.38 % 393:1:0:INP:: -> class_OrderedGroup_Osemigroup__add(tc_IntDef_Oint) % 0.10/0.38 % 394:1:0:INP:: -> class_Numeral_Onumber__ring(tc_IntDef_Oint) % 0.10/0.38 % 395:1:0:INP:: -> class_Divides_Odiv(tc_IntDef_Oint) % 0.10/0.38 % 396:1:0:INP:: -> class_Nat_Opower(tc_IntDef_Oint) % 0.10/0.38 % 397:1:0:INP:: -> class_Power_Orecpower(tc_IntDef_Oint) % 0.10/0.38 % 398:1:0:INP:: -> class_Parity_Oeven__odd(tc_IntDef_Oint) % 0.10/0.38 % 399:1:0:INP:: -> class_OrderedGroup_Oab__semigroup__add(tc_IntDef_Oint) % 0.10/0.38 % 400:1:0:INP:: -> class_OrderedGroup_Osemigroup__mult(tc_IntDef_Oint) % 0.10/0.38 % 401:1:0:INP:: -> class_OrderedGroup_Oab__semigroup__mult(tc_IntDef_Oint) % 0.10/0.38 % 402:1:0:INP:: -> class_Finite__Set_Ofinite(tc_Product__Type_Ounit) % 0.10/0.38 % 403:1:0:INP:: -> class_Finite__Set_Ofinite(tc_bool) % 0.10/0.38 % 404:3:2:INP:TopTop: class_Finite__Set_Ofinite(x0),class_Finite__Set_Ofinite(x1) -> class_Finite__Set_Ofinite(tc_fun(x1,x0)) % 0.10/0.38 % 405:1:2:INP:TopTop: -> class_Nat_Opower(tc_fun(x0,x1)) % 0.10/0.38 % 406:1:0:INP:: -> class_HOL_Oone(tc_nat) % 0.10/0.38 % 407:1:0:INP:: -> class_HOL_Ozero(tc_nat) % 0.10/0.38 % 408:1:0:INP:: -> class_HOL_Oplus(tc_nat) % 0.10/0.38 % 409:1:0:INP:: -> class_HOL_Otimes(tc_nat) % 0.10/0.38 % 410:1:0:INP:: -> class_Nat_Opower(tc_nat) % 0.10/0.38 % 411:1:0:INP:: -> class_Ring__and__Field_Oaxclass__0__neq__1(tc_nat) % 0.10/0.38 % 412:1:0:INP:: -> class_OrderedGroup_Osemigroup__add(tc_nat) % 0.10/0.38 % 413:1:0:INP:: -> class_OrderedGroup_Oab__semigroup__add(tc_nat) % 0.10/0.38 % 414:1:0:INP:: -> class_OrderedGroup_Osemigroup__mult(tc_nat) % 0.10/0.38 % 415:1:0:INP:: -> class_OrderedGroup_Oab__semigroup__mult(tc_nat) % 0.10/0.38 % 416:1:0:INP:: -> class_Ring__and__Field_Osemiring(tc_nat) % 0.10/0.38 % 417:1:0:INP:: -> class_Ring__and__Field_Ocomm__semiring(tc_nat) % 0.10/0.38 % 418:1:0:INP:: -> class_Orderings_Oord(tc_nat) % 0.10/0.38 % 419:1:0:INP:: -> class_OrderedGroup_Ocomm__monoid__add(tc_nat) % 0.10/0.38 % 420:1:0:INP:: -> class_Ring__and__Field_Osemiring__0(tc_nat) % 0.10/0.38 % 421:1:0:INP:: -> class_Ring__and__Field_Ocomm__semiring__0(tc_nat) % 0.10/0.38 % 422:1:0:INP:: -> class_OrderedGroup_Omonoid__mult(tc_nat) % 0.10/0.38 % 423:1:0:INP:: -> class_OrderedGroup_Ocomm__monoid__mult(tc_nat) % 0.10/0.38 % 424:1:0:INP:: -> class_Ring__and__Field_Osemiring__1(tc_nat) % 0.10/0.38 % 425:1:0:INP:: -> class_Ring__and__Field_Ocomm__semiring__1(tc_nat) % 0.10/0.38 % 426:1:0:INP:: -> class_OrderedGroup_Ocancel__semigroup__add(tc_nat) % 0.10/0.38 % 427:1:0:INP:: -> class_OrderedGroup_Ocancel__ab__semigroup__add(tc_nat) % 0.10/0.38 % 428:1:0:INP:: -> class_Ring__and__Field_Osemiring__0__cancel(tc_nat) % 0.10/0.38 % 429:1:0:INP:: -> class_Orderings_Oorder(tc_nat) % 0.10/0.38 % 430:1:0:INP:: -> class_Ring__and__Field_Osemiring__1__cancel(tc_nat) % 0.10/0.38 % 431:1:0:INP:: -> class_Ring__and__Field_Ocomm__semiring__0__cancel(tc_nat) % 0.10/0.38 % 432:1:0:INP:: -> class_Ring__and__Field_Ocomm__semiring__1__cancel(tc_nat) % 0.10/0.38 % 433:1:0:INP:: -> class_OrderedGroup_Opordered__ab__semigroup__add(tc_nat) % 0.10/0.38 % 434:1:0:INP:: -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat) % 0.10/0.38 % 435:1:0:INP:: -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) % 0.10/0.38 % 436:1:0:INP:: -> class_OrderedGroup_Oordered__cancel__ab__semigroup__add(tc_nat) % 0.10/0.38 % 437:1:0:INP:: -> class_Ring__and__Field_Opordered__semiring(tc_nat) % 0.10/0.38 % 438:1:0:INP:: -> class_Ring__and__Field_Opordered__cancel__semiring(tc_nat) % 0.10/0.38 % 439:1:0:INP:: -> class_Ring__and__Field_Oordered__semiring__strict(tc_nat) % 0.10/0.38 % 440:1:0:INP:: -> class_LOrder_Omeet__semilorder(tc_nat) % 0.10/0.38 % 441:1:0:INP:: -> class_Ring__and__Field_Opordered__comm__semiring(tc_nat) % 0.10/0.38 % 442:1:0:INP:: -> class_Ring__and__Field_Opordered__cancel__comm__semiring(tc_nat) % 0.10/0.38 % 443:1:0:INP:: -> class_Ring__and__Field_Oordered__comm__semiring__strict(tc_nat) % 0.10/0.38 % 444:1:0:INP:: -> class_Ring__and__Field_Oordered__semidom(tc_nat) % 0.10/0.38 % 445:1:0:INP:: -> class_Divides_Odiv(tc_nat) % 0.10/0.38 % 446:1:0:INP:: -> class_Power_Orecpower(tc_nat) % 0.10/0.38 % 447:1:0:INP:: -> class_Numeral_Onumber(tc_nat) % 0.10/0.38 % 448:1:0:INP:: -> class_Parity_Oeven__odd(tc_nat) % 0.10/0.38 % 449:1:0:INP:: -> class_LOrder_Ojoin__semilorder(tc_nat) % 0.10/0.38 % 450:1:0:INP:: -> class_LOrder_Olorder(tc_nat) % 0.10/0.38 % 451:1:0:INP:: -> class_Orderings_Olinorder(tc_nat) % 0.10/0.38 % 452:1:0:INP:: -> class_Wellfounded__Recursion_Owellorder(tc_nat) % 0.10/0.38 % 453:1:0:INP:: -> class_HOL_Ominus(tc_nat) % 0.10/0.38 % 454:3:2:INP:TopTop: class_Finite__Set_Ofinite(x0),class_Finite__Set_Ofinite(x1) -> class_Finite__Set_Ofinite(tc_prod(x1,x0)) % 0.10/0.38 % 455:1:1:INP:Top: -> class_HOL_Ominus(tc_set(x0)) % 0.10/0.38 % 456:1:1:INP:Top: -> class_Orderings_Oord(tc_set(x0)) % 0.10/0.38 % 457:1:1:INP:Top: -> class_Orderings_Oorder(tc_set(x0)) % 0.10/0.38 % 458:2:1:INP:Top: class_Finite__Set_Ofinite(x0) -> class_Finite__Set_Ofinite(tc_set(x0)) % 0.10/0.38 % 459:1:1:INP:Top: -> class_Nat_Opower(tc_set(x0)) % 0.10/0.38 % 460:3:2:INP:TopTop: class_Finite__Set_Ofinite(x0),class_Finite__Set_Ofinite(x1) -> class_Finite__Set_Ofinite(tc_sum(x1,x0)) % 0.10/0.38 % 461:2:1:INP:Top: class_LOrder_Ojoin__semilorder(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 462:2:1:INP:Top: class_LOrder_Ojoin__semilorder(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 463:2:1:INP:Top: class_LOrder_Olorder(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.38 % 464:2:1:INP:Top: class_LOrder_Olorder(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 465:2:1:INP:Top: class_LOrder_Olorder(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 466:2:1:INP:Top: class_LOrder_Olorder(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.38 % 467:2:1:INP:Top: class_LOrder_Omeet__semilorder(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 468:2:1:INP:Top: class_LOrder_Omeet__semilorder(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 469:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 470:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 471:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.38 % 472:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.38 % 473:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_HOL_Ominus(x0) % 0.10/0.38 % 474:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 475:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 476:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.38 % 477:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.38 % 478:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Oring(x0) % 0.10/0.38 % 479:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) % 0.10/0.38 % 480:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Ocomm__ring(x0) % 0.10/0.38 % 481:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 482:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_HOL_Oone(x0) % 0.10/0.38 % 483:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.38 % 484:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.38 % 485:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_OrderedGroup_Ocomm__monoid__mult(x0) % 0.10/0.38 % 486:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Osemiring__1(x0) % 0.10/0.38 % 487:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Ocomm__semiring__1(x0) % 0.10/0.38 % 488:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Osemiring__1__cancel(x0) % 0.10/0.38 % 489:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Oring__1(x0) % 0.10/0.38 % 490:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) % 0.10/0.38 % 491:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Ocomm__ring__1(x0) % 0.10/0.38 % 492:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 493:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Numeral_Onumber(x0) % 0.10/0.38 % 494:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 495:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.38 % 496:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.38 % 497:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.38 % 498:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 499:2:1:INP:Top: class_Numeral_Onumber__ring(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 500:2:1:INP:Top: class_OrderedGroup_Oab__group__add(x0) -> class_HOL_Ominus(x0) % 0.10/0.38 % 501:2:1:INP:Top: class_OrderedGroup_Oab__group__add(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 502:2:1:INP:Top: class_OrderedGroup_Oab__group__add(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 503:2:1:INP:Top: class_OrderedGroup_Oab__group__add(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 504:2:1:INP:Top: class_OrderedGroup_Oab__group__add(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 505:2:1:INP:Top: class_OrderedGroup_Oab__group__add(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 506:2:1:INP:Top: class_OrderedGroup_Oab__group__add(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 507:2:1:INP:Top: class_OrderedGroup_Oab__group__add(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 508:2:1:INP:Top: class_OrderedGroup_Oab__semigroup__add(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 509:2:1:INP:Top: class_OrderedGroup_Oab__semigroup__add(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 510:2:1:INP:Top: class_OrderedGroup_Oab__semigroup__mult(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 511:2:1:INP:Top: class_OrderedGroup_Oab__semigroup__mult(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 512:2:1:INP:Top: class_OrderedGroup_Ocancel__ab__semigroup__add(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 513:2:1:INP:Top: class_OrderedGroup_Ocancel__ab__semigroup__add(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 514:2:1:INP:Top: class_OrderedGroup_Ocancel__ab__semigroup__add(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 515:2:1:INP:Top: class_OrderedGroup_Ocancel__ab__semigroup__add(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 516:2:1:INP:Top: class_OrderedGroup_Ocancel__semigroup__add(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 517:2:1:INP:Top: class_OrderedGroup_Ocancel__semigroup__add(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 518:2:1:INP:Top: class_OrderedGroup_Ocomm__monoid__add(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 519:2:1:INP:Top: class_OrderedGroup_Ocomm__monoid__add(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 520:2:1:INP:Top: class_OrderedGroup_Ocomm__monoid__add(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 521:2:1:INP:Top: class_OrderedGroup_Ocomm__monoid__add(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 522:2:1:INP:Top: class_OrderedGroup_Ocomm__monoid__mult(x0) -> class_HOL_Oone(x0) % 0.10/0.38 % 523:2:1:INP:Top: class_OrderedGroup_Ocomm__monoid__mult(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.38 % 524:2:1:INP:Top: class_OrderedGroup_Ocomm__monoid__mult(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 525:2:1:INP:Top: class_OrderedGroup_Ocomm__monoid__mult(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 526:2:1:INP:Top: class_OrderedGroup_Ocomm__monoid__mult(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.38 % 527:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_OrderedGroup_Opordered__ab__group__add(x0) % 0.10/0.38 % 528:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.38 % 529:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 530:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 531:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 532:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 533:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 534:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_LOrder_Olorder(x0) % 0.10/0.38 % 535:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.38 % 536:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.38 % 537:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_HOL_Ominus(x0) % 0.10/0.38 % 538:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 539:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 540:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.38 % 541:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.38 % 542:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.38 % 543:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 544:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 545:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_OrderedGroup_Olordered__ab__group(x0) % 0.10/0.38 % 546:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_OrderedGroup_Opordered__ab__group__add(x0) % 0.10/0.38 % 547:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 548:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 549:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 550:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 551:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_LOrder_Olorder(x0) % 0.10/0.38 % 552:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.38 % 553:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.38 % 554:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 555:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 556:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.38 % 557:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_HOL_Ominus(x0) % 0.10/0.38 % 558:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 559:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 560:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.38 % 561:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.38 % 562:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.38 % 563:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__abs(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 564:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_OrderedGroup_Opordered__ab__group__add(x0) % 0.10/0.38 % 565:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.38 % 566:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 567:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 568:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 569:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 570:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 571:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.38 % 572:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_OrderedGroup_Olordered__ab__group(x0) % 0.10/0.38 % 573:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_LOrder_Olorder(x0) % 0.10/0.38 % 574:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.38 % 575:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_HOL_Ominus(x0) % 0.10/0.38 % 576:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 577:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 578:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.38 % 579:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.38 % 580:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.38 % 581:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 582:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__join(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 583:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_OrderedGroup_Opordered__ab__group__add(x0) % 0.10/0.38 % 584:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.38 % 585:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 586:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 587:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 588:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 589:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 590:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.38 % 591:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_OrderedGroup_Olordered__ab__group(x0) % 0.10/0.38 % 592:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_LOrder_Olorder(x0) % 0.10/0.38 % 593:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.38 % 594:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_HOL_Ominus(x0) % 0.10/0.38 % 595:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 596:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 597:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.38 % 598:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.38 % 599:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.38 % 600:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 601:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__meet(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 602:2:1:INP:Top: class_OrderedGroup_Omonoid__mult(x0) -> class_HOL_Oone(x0) % 0.10/0.38 % 603:2:1:INP:Top: class_OrderedGroup_Omonoid__mult(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 604:2:1:INP:Top: class_OrderedGroup_Omonoid__mult(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 605:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.38 % 606:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.38 % 607:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_LOrder_Olorder(x0) % 0.10/0.38 % 608:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.38 % 609:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.38 % 610:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.38 % 611:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 612:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 613:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 614:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 615:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 616:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 617:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 618:2:1:INP:Top: class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) -> class_Orderings_Olinorder(x0) % 0.10/0.38 % 619:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.38 % 620:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_HOL_Ominus(x0) % 0.10/0.38 % 621:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 622:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 623:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.38 % 624:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.38 % 625:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 626:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 627:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 628:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 629:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 630:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 631:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 632:2:1:INP:Top: class_OrderedGroup_Opordered__ab__group__add(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.38 % 633:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 634:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 635:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 636:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 637:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 638:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.38 % 639:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.38 % 640:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 641:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 642:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 643:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 644:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 645:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 646:2:1:INP:Top: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 647:2:1:INP:Top: class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.38 % 648:2:1:INP:Top: class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 649:2:1:INP:Top: class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 650:2:1:INP:Top: class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 651:2:1:INP:Top: class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 652:2:1:INP:Top: class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 653:2:1:INP:Top: class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 654:2:1:INP:Top: class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 655:2:1:INP:Top: class_OrderedGroup_Osemigroup__add(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 656:2:1:INP:Top: class_OrderedGroup_Osemigroup__mult(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 657:2:1:INP:Top: class_Orderings_Olinorder(x0) -> class_LOrder_Olorder(x0) % 0.10/0.38 % 658:2:1:INP:Top: class_Orderings_Olinorder(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.38 % 659:2:1:INP:Top: class_Orderings_Olinorder(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.38 % 660:2:1:INP:Top: class_Orderings_Olinorder(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 661:2:1:INP:Top: class_Orderings_Olinorder(x0) -> class_Orderings_Oorder(x0) % 0.10/0.38 % 662:2:1:INP:Top: class_Orderings_Oorder(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 663:2:1:INP:Top: class_Power_Orecpower(x0) -> class_Nat_Opower(x0) % 0.10/0.38 % 664:2:1:INP:Top: class_Power_Orecpower(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 665:2:1:INP:Top: class_Power_Orecpower(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.38 % 666:2:1:INP:Top: class_Power_Orecpower(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.38 % 667:2:1:INP:Top: class_Power_Orecpower(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 668:2:1:INP:Top: class_Power_Orecpower(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.38 % 669:2:1:INP:Top: class_Power_Orecpower(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.38 % 670:2:1:INP:Top: class_Power_Orecpower(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.38 % 671:2:1:INP:Top: class_Power_Orecpower(x0) -> class_OrderedGroup_Ocomm__monoid__mult(x0) % 0.10/0.38 % 672:2:1:INP:Top: class_Power_Orecpower(x0) -> class_Ring__and__Field_Osemiring__1(x0) % 0.10/0.38 % 673:2:1:INP:Top: class_Power_Orecpower(x0) -> class_Ring__and__Field_Ocomm__semiring__1(x0) % 0.10/0.38 % 674:2:1:INP:Top: class_Power_Orecpower(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 675:2:1:INP:Top: class_Power_Orecpower(x0) -> class_HOL_Oone(x0) % 0.10/0.38 % 676:2:1:INP:Top: class_Power_Orecpower(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 677:2:1:INP:Top: class_Power_Orecpower(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.38 % 678:2:1:INP:Top: class_Power_Orecpower(x0) -> class_Ring__and__Field_Osemiring__1__cancel(x0) % 0.10/0.38 % 679:2:1:INP:Top: class_Power_Orecpower(x0) -> class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) % 0.10/0.38 % 680:2:1:INP:Top: class_Power_Orecpower(x0) -> class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) % 0.10/0.38 % 681:2:1:INP:Top: class_Power_Orecpower(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.38 % 682:2:1:INP:Top: class_Power_Orecpower(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 683:2:1:INP:Top: class_Power_Orecpower(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 684:2:1:INP:Top: class_Power_Orecpower(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 685:2:1:INP:Top: class_Power_Orecpower(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 686:2:1:INP:Top: class_Power_Orecpower(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 687:2:1:INP:Top: class_Power_Orecpower(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.38 % 688:2:1:INP:Top: class_Ring__and__Field_Oaxclass__0__neq__1(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 689:2:1:INP:Top: class_Ring__and__Field_Oaxclass__0__neq__1(x0) -> class_HOL_Oone(x0) % 0.10/0.38 % 690:2:1:INP:Top: class_Ring__and__Field_Oaxclass__abs__if(x0) -> class_HOL_Ominus(x0) % 0.10/0.38 % 691:2:1:INP:Top: class_Ring__and__Field_Oaxclass__abs__if(x0) -> class_Orderings_Oord(x0) % 0.10/0.38 % 692:2:1:INP:Top: class_Ring__and__Field_Oaxclass__abs__if(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 693:2:1:INP:Top: class_Ring__and__Field_Oaxclass__no__zero__divisors(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 694:2:1:INP:Top: class_Ring__and__Field_Oaxclass__no__zero__divisors(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 695:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.38 % 696:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.38 % 697:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 698:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 699:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.38 % 700:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_HOL_Ominus(x0) % 0.10/0.38 % 701:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 702:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 703:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_Ring__and__Field_Oring(x0) % 0.10/0.38 % 704:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.38 % 705:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) % 0.10/0.38 % 706:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.38 % 707:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.38 % 708:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.38 % 709:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 710:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 711:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 712:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 713:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 714:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Ocomm__ring(x0) % 0.10/0.38 % 715:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Oring(x0) % 0.10/0.38 % 716:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.38 % 717:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 718:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 719:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 720:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 721:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 722:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 723:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 724:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 725:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 726:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.38 % 727:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Ocomm__semiring__1(x0) % 0.10/0.38 % 728:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_OrderedGroup_Ocomm__monoid__mult(x0) % 0.10/0.38 % 729:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Osemiring__1(x0) % 0.10/0.38 % 730:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.38 % 731:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.38 % 732:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_HOL_Oone(x0) % 0.10/0.38 % 733:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Oring__1(x0) % 0.10/0.38 % 734:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Osemiring__1__cancel(x0) % 0.10/0.38 % 735:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) % 0.10/0.38 % 736:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_HOL_Ominus(x0) % 0.10/0.38 % 737:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) % 0.10/0.38 % 738:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.38 % 739:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.38 % 740:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.38 % 741:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.38 % 742:2:1:INP:Top: class_Ring__and__Field_Ocomm__ring__1(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.38 % 743:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 744:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 745:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 746:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.38 % 747:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 748:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 749:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.38 % 750:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.38 % 751:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.38 % 752:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.38 % 753:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.38 % 754:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 755:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 756:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 757:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 758:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 759:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 760:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 761:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.38 % 762:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.38 % 763:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 764:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 765:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 766:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 767:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.38 % 768:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.38 % 769:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.38 % 770:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.38 % 771:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 772:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 773:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 774:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 775:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 776:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.38 % 777:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 778:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 779:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 780:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 781:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 782:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_OrderedGroup_Ocomm__monoid__mult(x0) % 0.10/0.38 % 783:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.38 % 784:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_Ring__and__Field_Osemiring__1(x0) % 0.10/0.38 % 785:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_HOL_Oone(x0) % 0.10/0.38 % 786:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.38 % 787:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.38 % 788:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.38 % 789:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.38 % 790:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.38 % 791:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 792:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 793:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_Ring__and__Field_Ocomm__semiring__1(x0) % 0.10/0.38 % 794:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.38 % 795:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 796:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 797:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 798:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 799:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.38 % 800:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_HOL_Oone(x0) % 0.10/0.38 % 801:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 802:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 803:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 804:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 805:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.38 % 806:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_Ring__and__Field_Osemiring__1__cancel(x0) % 0.10/0.38 % 807:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.38 % 808:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) % 0.10/0.38 % 809:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_OrderedGroup_Ocomm__monoid__mult(x0) % 0.10/0.38 % 810:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.38 % 811:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_Ring__and__Field_Osemiring__1(x0) % 0.10/0.38 % 812:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.38 % 813:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.38 % 814:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.38 % 815:2:1:INP:Top: class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 816:2:1:INP:Top: class_Ring__and__Field_Odivision__by__zero(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 817:2:1:INP:Top: class_Ring__and__Field_Odivision__by__zero(x0) -> class_HOL_Oinverse(x0) % 0.10/0.38 % 818:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Ocomm__ring__1(x0) % 0.10/0.38 % 819:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Ocomm__ring(x0) % 0.10/0.38 % 820:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Osemiring__1(x0) % 0.10/0.38 % 821:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.38 % 822:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.38 % 823:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_HOL_Oone(x0) % 0.10/0.38 % 824:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) % 0.10/0.38 % 825:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.38 % 826:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.38 % 827:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.38 % 828:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.38 % 829:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.38 % 830:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Oring__1(x0) % 0.10/0.38 % 831:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.38 % 832:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 833:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 834:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 835:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 836:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 837:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 838:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 839:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 840:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 841:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Oring(x0) % 0.10/0.38 % 842:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_HOL_Oinverse(x0) % 0.10/0.38 % 843:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Oidom(x0) % 0.10/0.38 % 844:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Oaxclass__no__zero__divisors(x0) % 0.10/0.38 % 845:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.38 % 846:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_HOL_Ominus(x0) % 0.10/0.38 % 847:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) % 0.10/0.38 % 848:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Ocomm__semiring__1(x0) % 0.10/0.38 % 849:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_OrderedGroup_Ocomm__monoid__mult(x0) % 0.10/0.38 % 850:2:1:INP:Top: class_Ring__and__Field_Ofield(x0) -> class_Ring__and__Field_Osemiring__1__cancel(x0) % 0.10/0.38 % 851:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Ocomm__ring__1(x0) % 0.10/0.38 % 852:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Ocomm__ring(x0) % 0.10/0.38 % 853:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Osemiring__1(x0) % 0.10/0.38 % 854:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.38 % 855:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.38 % 856:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_HOL_Oone(x0) % 0.10/0.38 % 857:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) % 0.10/0.38 % 858:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.38 % 859:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.38 % 860:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.38 % 861:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.38 % 862:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.38 % 863:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Oring__1(x0) % 0.10/0.38 % 864:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.38 % 865:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.38 % 866:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_HOL_Otimes(x0) % 0.10/0.38 % 867:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.38 % 868:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_HOL_Ozero(x0) % 0.10/0.38 % 869:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.38 % 870:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.38 % 871:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.38 % 872:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.38 % 873:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_HOL_Oplus(x0) % 0.10/0.38 % 874:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Oring(x0) % 0.10/0.39 % 875:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Oaxclass__no__zero__divisors(x0) % 0.10/0.39 % 876:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.39 % 877:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_HOL_Ominus(x0) % 0.10/0.39 % 878:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) % 0.10/0.39 % 879:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Ocomm__semiring__1(x0) % 0.10/0.39 % 880:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_OrderedGroup_Ocomm__monoid__mult(x0) % 0.10/0.39 % 881:2:1:INP:Top: class_Ring__and__Field_Oidom(x0) -> class_Ring__and__Field_Osemiring__1__cancel(x0) % 0.10/0.39 % 882:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_Ring__and__Field_Opordered__ring(x0) % 0.10/0.39 % 883:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_Ring__and__Field_Oring(x0) % 0.10/0.39 % 884:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 885:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 886:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 887:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 888:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 889:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 890:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 891:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 892:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 893:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 894:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Opordered__ab__group__add(x0) % 0.10/0.39 % 895:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 896:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 897:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 898:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 899:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Olordered__ab__group__abs(x0) % 0.10/0.39 % 900:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Olordered__ab__group(x0) % 0.10/0.39 % 901:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_LOrder_Olorder(x0) % 0.10/0.39 % 902:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.39 % 903:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.39 % 904:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Olordered__ab__group__meet(x0) % 0.10/0.39 % 905:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.39 % 906:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Olordered__ab__group__join(x0) % 0.10/0.39 % 907:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_HOL_Ominus(x0) % 0.10/0.39 % 908:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.39 % 909:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 910:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_Ring__and__Field_Opordered__cancel__semiring(x0) % 0.10/0.39 % 911:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_Ring__and__Field_Opordered__semiring(x0) % 0.10/0.39 % 912:2:1:INP:Top: class_Ring__and__Field_Olordered__ring(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 913:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.39 % 914:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.39 % 915:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 916:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 917:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 918:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Orderings_Olinorder(x0) % 0.10/0.39 % 919:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_LOrder_Olorder(x0) % 0.10/0.39 % 920:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.39 % 921:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.39 % 922:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.39 % 923:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 924:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 925:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.39 % 926:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 927:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 928:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 929:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 930:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Ring__and__Field_Oordered__semiring__strict(x0) % 0.10/0.39 % 931:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Ring__and__Field_Opordered__cancel__semiring(x0) % 0.10/0.39 % 932:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 933:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Ring__and__Field_Opordered__semiring(x0) % 0.10/0.39 % 934:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) % 0.10/0.39 % 935:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Ring__and__Field_Opordered__comm__semiring(x0) % 0.10/0.39 % 936:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 937:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 938:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 939:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 940:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 941:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 942:2:1:INP:Top: class_Ring__and__Field_Oordered__comm__semiring__strict(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 943:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Ofield(x0) % 0.10/0.39 % 944:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_HOL_Oinverse(x0) % 0.10/0.39 % 945:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Ocomm__semiring__1(x0) % 0.10/0.39 % 946:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Ocomm__monoid__mult(x0) % 0.10/0.39 % 947:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Osemiring__1__cancel(x0) % 0.10/0.39 % 948:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Osemiring__1(x0) % 0.10/0.39 % 949:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.39 % 950:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.39 % 951:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_HOL_Oone(x0) % 0.10/0.39 % 952:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) % 0.10/0.39 % 953:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.39 % 954:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.39 % 955:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Oidom(x0) % 0.10/0.39 % 956:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.39 % 957:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 958:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 959:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 960:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 961:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 962:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 963:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 964:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 965:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 966:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Ocomm__ring__1(x0) % 0.10/0.39 % 967:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 968:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Oaxclass__no__zero__divisors(x0) % 0.10/0.39 % 969:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 970:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 971:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Oordered__idom(x0) % 0.10/0.39 % 972:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Oordered__comm__semiring__strict(x0) % 0.10/0.39 % 973:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) % 0.10/0.39 % 974:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Opordered__comm__semiring(x0) % 0.10/0.39 % 975:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Oordered__ring__strict(x0) % 0.10/0.39 % 976:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Oordered__semiring__strict(x0) % 0.10/0.39 % 977:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Ocomm__ring(x0) % 0.10/0.39 % 978:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 979:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Orderings_Olinorder(x0) % 0.10/0.39 % 980:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Oaxclass__abs__if(x0) % 0.10/0.39 % 981:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Olordered__ring(x0) % 0.10/0.39 % 982:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Opordered__ring(x0) % 0.10/0.39 % 983:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Opordered__cancel__semiring(x0) % 0.10/0.39 % 984:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Opordered__semiring(x0) % 0.10/0.39 % 985:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Olordered__ab__group__abs(x0) % 0.10/0.39 % 986:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Olordered__ab__group__meet(x0) % 0.10/0.39 % 987:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Olordered__ab__group__join(x0) % 0.10/0.39 % 988:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Oring__1(x0) % 0.10/0.39 % 989:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Olordered__ab__group(x0) % 0.10/0.39 % 990:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_LOrder_Olorder(x0) % 0.10/0.39 % 991:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.39 % 992:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.39 % 993:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Opordered__ab__group__add(x0) % 0.10/0.39 % 994:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.39 % 995:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 996:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 997:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 998:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 999:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Oring(x0) % 0.10/0.39 % 1000:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Oordered__semidom(x0) % 0.10/0.39 % 1001:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.39 % 1002:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_HOL_Ominus(x0) % 0.10/0.39 % 1003:2:1:INP:Top: class_Ring__and__Field_Oordered__field(x0) -> class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) % 0.10/0.39 % 1004:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Ocomm__ring__1(x0) % 0.10/0.39 % 1005:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Ocomm__ring(x0) % 0.10/0.39 % 1006:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Osemiring__1(x0) % 0.10/0.39 % 1007:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.39 % 1008:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.39 % 1009:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_HOL_Oone(x0) % 0.10/0.39 % 1010:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) % 0.10/0.39 % 1011:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.39 % 1012:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.39 % 1013:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.39 % 1014:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 1015:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1016:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Oring__1(x0) % 0.10/0.39 % 1017:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1018:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1019:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1020:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1021:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1022:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 1023:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1024:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 1025:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1026:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1027:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Oring(x0) % 0.10/0.39 % 1028:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Oordered__comm__semiring__strict(x0) % 0.10/0.39 % 1029:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Oordered__semiring__strict(x0) % 0.10/0.39 % 1030:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 1031:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Orderings_Olinorder(x0) % 0.10/0.39 % 1032:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_LOrder_Olorder(x0) % 0.10/0.39 % 1033:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.39 % 1034:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.39 % 1035:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.39 % 1036:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 1037:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) % 0.10/0.39 % 1038:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.39 % 1039:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Opordered__cancel__semiring(x0) % 0.10/0.39 % 1040:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Opordered__comm__semiring(x0) % 0.10/0.39 % 1041:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Opordered__semiring(x0) % 0.10/0.39 % 1042:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 1043:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 1044:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 1045:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Oaxclass__abs__if(x0) % 0.10/0.39 % 1046:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Oordered__ring__strict(x0) % 0.10/0.39 % 1047:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Olordered__ring(x0) % 0.10/0.39 % 1048:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Opordered__ring(x0) % 0.10/0.39 % 1049:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_HOL_Ominus(x0) % 0.10/0.39 % 1050:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Olordered__ab__group__abs(x0) % 0.10/0.39 % 1051:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Olordered__ab__group__meet(x0) % 0.10/0.39 % 1052:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Olordered__ab__group__join(x0) % 0.10/0.39 % 1053:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Olordered__ab__group(x0) % 0.10/0.39 % 1054:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Opordered__ab__group__add(x0) % 0.10/0.39 % 1055:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Oordered__semidom(x0) % 0.10/0.39 % 1056:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Oaxclass__no__zero__divisors(x0) % 0.10/0.39 % 1057:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Oidom(x0) % 0.10/0.39 % 1058:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) % 0.10/0.39 % 1059:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Ocomm__semiring__1(x0) % 0.10/0.39 % 1060:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_OrderedGroup_Ocomm__monoid__mult(x0) % 0.10/0.39 % 1061:2:1:INP:Top: class_Ring__and__Field_Oordered__idom(x0) -> class_Ring__and__Field_Osemiring__1__cancel(x0) % 0.10/0.39 % 1062:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Ring__and__Field_Oring(x0) % 0.10/0.39 % 1063:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.39 % 1064:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1065:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1066:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1067:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1068:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1069:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Ring__and__Field_Oordered__semiring__strict(x0) % 0.10/0.39 % 1070:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 1071:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Orderings_Olinorder(x0) % 0.10/0.39 % 1072:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_LOrder_Olorder(x0) % 0.10/0.39 % 1073:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.39 % 1074:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_HOL_Ominus(x0) % 0.10/0.39 % 1075:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.39 % 1076:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.39 % 1077:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 1078:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Ring__and__Field_Opordered__cancel__semiring(x0) % 0.10/0.39 % 1079:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Ring__and__Field_Opordered__semiring(x0) % 0.10/0.39 % 1080:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 1081:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 1082:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 1083:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Ring__and__Field_Oaxclass__abs__if(x0) % 0.10/0.39 % 1084:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Olordered__ab__group(x0) % 0.10/0.39 % 1085:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 1086:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Opordered__ab__group__add(x0) % 0.10/0.39 % 1087:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Ring__and__Field_Olordered__ring(x0) % 0.10/0.39 % 1088:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Ring__and__Field_Opordered__ring(x0) % 0.10/0.39 % 1089:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Olordered__ab__group__abs(x0) % 0.10/0.39 % 1090:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Olordered__ab__group__meet(x0) % 0.10/0.39 % 1091:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Olordered__ab__group__join(x0) % 0.10/0.39 % 1092:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Ring__and__Field_Oaxclass__no__zero__divisors(x0) % 0.10/0.39 % 1093:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 1094:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 1095:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1096:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1097:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1098:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1099:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Ocomm__semiring__1__cancel(x0) % 0.10/0.39 % 1100:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Ocomm__semiring__1(x0) % 0.10/0.39 % 1101:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.39 % 1102:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.39 % 1103:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 1104:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1105:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1106:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1107:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1108:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1109:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1110:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 1111:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Ocomm__monoid__mult(x0) % 0.10/0.39 % 1112:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1113:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 1114:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1115:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1116:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Oordered__comm__semiring__strict(x0) % 0.10/0.39 % 1117:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Oordered__semiring__strict(x0) % 0.10/0.39 % 1118:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 1119:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Orderings_Olinorder(x0) % 0.10/0.39 % 1120:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_LOrder_Olorder(x0) % 0.10/0.39 % 1121:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.39 % 1122:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Osemiring__1__cancel(x0) % 0.10/0.39 % 1123:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.39 % 1124:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.39 % 1125:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 1126:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) % 0.10/0.39 % 1127:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Opordered__cancel__semiring(x0) % 0.10/0.39 % 1128:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Opordered__comm__semiring(x0) % 0.10/0.39 % 1129:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Opordered__semiring(x0) % 0.10/0.39 % 1130:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 1131:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 1132:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 1133:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Osemiring__1(x0) % 0.10/0.39 % 1134:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.39 % 1135:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.39 % 1136:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_HOL_Oone(x0) % 0.10/0.39 % 1137:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) % 0.10/0.39 % 1138:2:1:INP:Top: class_Ring__and__Field_Oordered__semidom(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.39 % 1139:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1140:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1141:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_Orderings_Olinorder(x0) % 0.10/0.39 % 1142:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_LOrder_Olorder(x0) % 0.10/0.39 % 1143:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.39 % 1144:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.39 % 1145:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.39 % 1146:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 1147:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 1148:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 1149:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 1150:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 1151:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1152:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 1153:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 1154:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_Ring__and__Field_Opordered__cancel__semiring(x0) % 0.10/0.39 % 1155:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_Ring__and__Field_Opordered__semiring(x0) % 0.10/0.39 % 1156:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1157:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1158:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1159:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1160:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1161:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1162:2:1:INP:Top: class_Ring__and__Field_Oordered__semiring__strict(x0) -> class_OrderedGroup_Oordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 1163:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_Ring__and__Field_Opordered__comm__semiring(x0) % 0.10/0.39 % 1164:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.39 % 1165:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 1166:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1167:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1168:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1169:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 1170:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 1171:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 1172:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 1173:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_Ring__and__Field_Opordered__semiring(x0) % 0.10/0.39 % 1174:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_Ring__and__Field_Opordered__cancel__semiring(x0) % 0.10/0.39 % 1175:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.39 % 1176:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 1177:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.39 % 1178:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1179:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1180:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1181:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1182:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1183:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__comm__semiring(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1184:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_Ring__and__Field_Opordered__semiring(x0) % 0.10/0.39 % 1185:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1186:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1187:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 1188:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 1189:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 1190:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 1191:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 1192:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1193:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1194:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1195:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1196:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1197:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 1198:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1199:2:1:INP:Top: class_Ring__and__Field_Opordered__cancel__semiring(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1200:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_Ring__and__Field_Ocomm__ring(x0) % 0.10/0.39 % 1201:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_Ring__and__Field_Oring(x0) % 0.10/0.39 % 1202:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1203:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1204:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1205:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1206:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1207:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 1208:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1209:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 1210:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1211:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1212:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.39 % 1213:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_Ring__and__Field_Opordered__comm__semiring(x0) % 0.10/0.39 % 1214:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_Ring__and__Field_Opordered__semiring(x0) % 0.10/0.39 % 1215:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 1216:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 1217:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 1218:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_HOL_Ominus(x0) % 0.10/0.39 % 1219:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_Ring__and__Field_Ocomm__semiring__0__cancel(x0) % 0.10/0.39 % 1220:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.39 % 1221:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.39 % 1222:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.39 % 1223:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 1224:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__ring(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1225:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_Ring__and__Field_Ocomm__semiring__0(x0) % 0.10/0.39 % 1226:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_Ring__and__Field_Ocomm__semiring(x0) % 0.10/0.39 % 1227:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1228:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1229:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 1230:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 1231:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 1232:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_Ring__and__Field_Opordered__semiring(x0) % 0.10/0.39 % 1233:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_OrderedGroup_Oab__semigroup__mult(x0) % 0.10/0.39 % 1234:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1235:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1236:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1237:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1238:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1239:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1240:2:1:INP:Top: class_Ring__and__Field_Opordered__comm__semiring(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1241:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_Ring__and__Field_Oring(x0) % 0.10/0.39 % 1242:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.39 % 1243:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1244:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1245:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1246:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1247:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1248:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_Ring__and__Field_Opordered__semiring(x0) % 0.10/0.39 % 1249:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 1250:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 1251:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 1252:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_OrderedGroup_Opordered__ab__group__add(x0) % 0.10/0.39 % 1253:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_HOL_Ominus(x0) % 0.10/0.39 % 1254:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0) % 0.10/0.39 % 1255:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0) % 0.10/0.39 % 1256:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_Ring__and__Field_Opordered__cancel__semiring(x0) % 0.10/0.39 % 1257:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 1258:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 1259:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 1260:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1261:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1262:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1263:2:1:INP:Top: class_Ring__and__Field_Opordered__ring(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1264:2:1:INP:Top: class_Ring__and__Field_Opordered__semiring(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1265:2:1:INP:Top: class_Ring__and__Field_Opordered__semiring(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1266:2:1:INP:Top: class_Ring__and__Field_Opordered__semiring(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 1267:2:1:INP:Top: class_Ring__and__Field_Opordered__semiring(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 1268:2:1:INP:Top: class_Ring__and__Field_Opordered__semiring(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1269:2:1:INP:Top: class_Ring__and__Field_Opordered__semiring(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1270:2:1:INP:Top: class_Ring__and__Field_Opordered__semiring(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1271:2:1:INP:Top: class_Ring__and__Field_Opordered__semiring(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1272:2:1:INP:Top: class_Ring__and__Field_Opordered__semiring(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1273:2:1:INP:Top: class_Ring__and__Field_Opordered__semiring(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1274:2:1:INP:Top: class_Ring__and__Field_Opordered__semiring(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1275:2:1:INP:Top: class_Ring__and__Field_Opordered__semiring(x0) -> class_OrderedGroup_Opordered__ab__semigroup__add(x0) % 0.10/0.39 % 1276:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1277:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1278:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 1279:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 1280:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 1281:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1282:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1283:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1284:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1285:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1286:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.39 % 1287:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_HOL_Ominus(x0) % 0.10/0.39 % 1288:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1289:2:1:INP:Top: class_Ring__and__Field_Oring(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1290:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_Ring__and__Field_Oring(x0) % 0.10/0.39 % 1291:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_OrderedGroup_Oab__group__add(x0) % 0.10/0.39 % 1292:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1293:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1294:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1295:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1296:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1297:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_Ring__and__Field_Osemiring__1(x0) % 0.10/0.39 % 1298:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.39 % 1299:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.39 % 1300:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_HOL_Oone(x0) % 0.10/0.39 % 1301:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_Ring__and__Field_Osemiring__1__cancel(x0) % 0.10/0.39 % 1302:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_HOL_Ominus(x0) % 0.10/0.39 % 1303:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 1304:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 1305:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 1306:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1307:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1308:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1309:2:1:INP:Top: class_Ring__and__Field_Oring__1(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1310:2:1:INP:Top: class_Ring__and__Field_Osemiring(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1311:2:1:INP:Top: class_Ring__and__Field_Osemiring(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1312:2:1:INP:Top: class_Ring__and__Field_Osemiring(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1313:2:1:INP:Top: class_Ring__and__Field_Osemiring(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1314:2:1:INP:Top: class_Ring__and__Field_Osemiring(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1315:2:1:INP:Top: class_Ring__and__Field_Osemiring__0(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1316:2:1:INP:Top: class_Ring__and__Field_Osemiring__0(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1317:2:1:INP:Top: class_Ring__and__Field_Osemiring__0(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1318:2:1:INP:Top: class_Ring__and__Field_Osemiring__0(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1319:2:1:INP:Top: class_Ring__and__Field_Osemiring__0(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1320:2:1:INP:Top: class_Ring__and__Field_Osemiring__0(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1321:2:1:INP:Top: class_Ring__and__Field_Osemiring__0(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1322:2:1:INP:Top: class_Ring__and__Field_Osemiring__0(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1323:2:1:INP:Top: class_Ring__and__Field_Osemiring__0__cancel(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1324:2:1:INP:Top: class_Ring__and__Field_Osemiring__0__cancel(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1325:2:1:INP:Top: class_Ring__and__Field_Osemiring__0__cancel(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 1326:2:1:INP:Top: class_Ring__and__Field_Osemiring__0__cancel(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1327:2:1:INP:Top: class_Ring__and__Field_Osemiring__0__cancel(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1328:2:1:INP:Top: class_Ring__and__Field_Osemiring__0__cancel(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1329:2:1:INP:Top: class_Ring__and__Field_Osemiring__0__cancel(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1330:2:1:INP:Top: class_Ring__and__Field_Osemiring__0__cancel(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1331:2:1:INP:Top: class_Ring__and__Field_Osemiring__0__cancel(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1332:2:1:INP:Top: class_Ring__and__Field_Osemiring__0__cancel(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1333:2:1:INP:Top: class_Ring__and__Field_Osemiring__0__cancel(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 1334:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.39 % 1335:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1336:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1337:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.39 % 1338:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> class_HOL_Oone(x0) % 0.10/0.39 % 1339:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1340:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1341:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1342:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1343:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1344:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1345:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1346:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_Ring__and__Field_Osemiring__1(x0) % 0.10/0.39 % 1347:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_Ring__and__Field_Oaxclass__0__neq__1(x0) % 0.10/0.39 % 1348:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_HOL_Oone(x0) % 0.10/0.39 % 1349:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_OrderedGroup_Osemigroup__mult(x0) % 0.10/0.39 % 1350:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_HOL_Otimes(x0) % 0.10/0.39 % 1351:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_OrderedGroup_Ocancel__ab__semigroup__add(x0) % 0.10/0.39 % 1352:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_OrderedGroup_Ocancel__semigroup__add(x0) % 0.10/0.39 % 1353:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_Ring__and__Field_Osemiring__0__cancel(x0) % 0.10/0.39 % 1354:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_Ring__and__Field_Osemiring__0(x0) % 0.10/0.39 % 1355:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_Ring__and__Field_Osemiring(x0) % 0.10/0.39 % 1356:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_OrderedGroup_Ocomm__monoid__add(x0) % 0.10/0.39 % 1357:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_HOL_Ozero(x0) % 0.10/0.39 % 1358:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_OrderedGroup_Oab__semigroup__add(x0) % 0.10/0.39 % 1359:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_OrderedGroup_Osemigroup__add(x0) % 0.10/0.39 % 1360:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_HOL_Oplus(x0) % 0.10/0.39 % 1361:2:1:INP:Top: class_Ring__and__Field_Osemiring__1__cancel(x0) -> class_OrderedGroup_Omonoid__mult(x0) % 0.10/0.39 % 1362:2:1:INP:Top: class_Wellfounded__Recursion_Owellorder(x0) -> class_Orderings_Oord(x0) % 0.10/0.39 % 1363:2:1:INP:Top: class_Wellfounded__Recursion_Owellorder(x0) -> class_Orderings_Oorder(x0) % 0.10/0.39 % 1364:2:1:INP:Top: class_Wellfounded__Recursion_Owellorder(x0) -> class_LOrder_Omeet__semilorder(x0) % 0.10/0.39 % 1365:2:1:INP:Top: class_Wellfounded__Recursion_Owellorder(x0) -> class_LOrder_Ojoin__semilorder(x0) % 0.10/0.39 % 1366:2:1:INP:Top: class_Wellfounded__Recursion_Owellorder(x0) -> class_LOrder_Olorder(x0) % 0.10/0.39 % 1367:2:1:INP:Top: class_Wellfounded__Recursion_Owellorder(x0) -> class_Orderings_Olinorder(x0) % 0.10/0.39 % 1368:1:4:INP:TopTopTopTop: -> c_in(c_PropLog_Opl_Oop_A_N_62(x0,c_PropLog_Opl_Oop_A_N_62(x1,x0,x2),x2),c_PropLog_Othms(x3,x2),tc_PropLog_Opl(x2)) % 0.10/0.39 % 1369:3:4:INP:TopTopTopTop: c_in(x0,c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)),c_in(c_PropLog_Opl_Oop_A_N_62(x0,x3,x2),c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)) -> c_in(x3,c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)) % 0.10/0.39 % 1370:1:5:INP:TopTopTopTopTop: -> c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(x0,c_PropLog_Opl_Oop_A_N_62(x1,x2,x3),x3),c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(x0,x1,x3),c_PropLog_Opl_Oop_A_N_62(x0,x2,x3),x3),x3),c_PropLog_Othms(x4,x3),tc_PropLog_Opl(x3)) % 0.10/0.39 % 1371:1:0:INP:: c_in(c_PropLog_Opl_Oop_A_N_62(v_p,v_p,t_a),c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)) -> % 0.10/0.39 % 0.10/0.39 % Predicates: = c_in c_Divides_Oop_Advd c_less c_lessequals class_Orderings_Oorder class_Orderings_Olinorder class_Orderings_Oord c_Wellfounded__Recursion_Oacyclic c_Wellfounded__Recursion_Owf c_Infinite__Set_Oatmost__one c_List_Odistinct c_Relation_Otrans class_Finite__Set_Ofinite class_HOL_Ominus class_HOL_Oone class_Ring__and__Field_Osemiring class_Ring__and__Field_Ocomm__semiring class_OrderedGroup_Ocomm__monoid__add class_Ring__and__Field_Osemiring__0 class_Ring__and__Field_Ocomm__semiring__0 class_OrderedGroup_Ocancel__semigroup__add class_OrderedGroup_Ocancel__ab__semigroup__add class_OrderedGroup_Oab__group__add class_Ring__and__Field_Osemiring__0__cancel class_Ring__and__Field_Oring class_HOL_Oplus class_Ring__and__Field_Ocomm__semiring__0__cancel class_Ring__and__Field_Ocomm__ring class_Ring__and__Field_Oaxclass__0__neq__1 class_OrderedGroup_Omonoid__mult class_OrderedGroup_Ocomm__monoid__mult class_Ring__and__Field_Osemiring__1 class_Ring__and__Field_Ocomm__semiring__1 class_Ring__and__Field_Osemiring__1__cancel class_Ring__and__Field_Oring__1 class_Ring__and__Field_Ocomm__semiring__1__cancel class_HOL_Otimes class_Ring__and__Field_Ocomm__ring__1 class_LOrder_Omeet__semilorder class_LOrder_Ojoin__semilorder class_LOrder_Olorder class_OrderedGroup_Opordered__ab__semigroup__add class_OrderedGroup_Opordered__cancel__ab__semigroup__add class_OrderedGroup_Opordered__ab__semigroup__add__imp__le class_OrderedGroup_Oordered__cancel__ab__semigroup__add class_HOL_Ozero class_Ring__and__Field_Opordered__semiring class_Ring__and__Field_Opordered__cancel__semiring class_Ring__and__Field_Oordered__semiring__strict class_Ring__and__Field_Opordered__comm__semiring class_Ring__and__Field_Opordered__cancel__comm__semiring class_Ring__and__Field_Oordered__comm__semiring__strict class_Ring__and__Field_Oaxclass__abs__if class_OrderedGroup_Opordered__ab__group__add class_OrderedGroup_Olordered__ab__group class_Ring__and__Field_Opordered__ring class_OrderedGroup_Olordered__ab__group__abs class_OrderedGroup_Olordered__ab__group__meet class_OrderedGroup_Olordered__ab__group__join class_Ring__and__Field_Olordered__ring class_Ring__and__Field_Oaxclass__no__zero__divisors class_Ring__and__Field_Oordered__ring__strict class_Ring__and__Field_Oordered__semidom class_Ring__and__Field_Oidom class_Ring__and__Field_Oordered__idom class_Numeral_Onumber class_OrderedGroup_Osemigroup__add class_Numeral_Onumber__ring class_Divides_Odiv class_Nat_Opower class_Power_Orecpower class_Parity_Oeven__odd class_OrderedGroup_Oab__semigroup__add class_OrderedGroup_Osemigroup__mult class_OrderedGroup_Oab__semigroup__mult class_Wellfounded__Recursion_Owellorder class_Ring__and__Field_Odivision__by__zero class_HOL_Oinverse class_Ring__and__Field_Ofield class_Ring__and__Field_Oordered__field class_Ring__and__Field_Opordered__comm__ring % 0.10/0.39 % Fol Constants: c_PropLog_Opl_Ofalse c_Datatype_Ooption_ONone c_0 tc_nat c_emptyset c_Extraction_Osumbool_OLeft c_Extraction_Osumbool_ORight c_Finite__Set_OFinites c_UNIV tc_IntDef_Oint c_List_Olist_ONil c_1 c_Numeral_Obit_OB0 c_Numeral_Obit_OB1 c_Relation_OId c_Wellfounded__Relations_Oless__than tc_Product__Type_Ounit tc_bool v_p t_a v_H % 0.10/0.39 % Fol Functions: c_PropLog_Opl_Ovar c_PropLog_Opl_Oop_A_N_62 tc_PropLog_Opl c_PropLog_Othms c_Datatype_Oo2s c_Datatype_Ooption_OSome c_Main_Onot__None__eq__iff1__1 c_Main_Onot__Some__eq__iff1__1 c_Datatype__Universe_OAtom c_Datatype__Universe_OScons c_Datatype__Universe_OIn0 c_Datatype__Universe_OIn1 c_Datatype__Universe_OLeaf c_Datatype__Universe_ONumb c_Equiv__Relations_Oquotient c_insert tc_set c_minus c_Pow c_union c_Relation_Oconverse tc_prod c_Pair c_GCD_Ogcd c_IntDef_Oint c_uminus tc_List_Olist c_List_Olex c_append c_List_Orev c_List_Olist_OCons c_List_Olists c_List_Ochar_OChar c_Nat_Osize c_List_Oremdups c_List_Oset c_Suc c_plus c_Relation_OImage c_SetInterval_OatLeast c_SetInterval_OatMost c_SetInterval_OgreaterThan c_SetInterval_OlessThan c_inter c_Inter c_Union c_Sum__Type_OInl c_Sum__Type_OInr c_Transitive__Closure_Ortrancl c_Datatype__Universe_Odprod tc_Datatype__Universe_Onode c_Main_OdprodE__1 c_Main_OdprodE__2 c_Main_OdprodE__3 c_Main_OdprodE__4 c_Datatype__Universe_Odsum c_Main_OdsumE__1 c_Main_OdsumE__2 c_Main_OdsumE__3 c_Main_OdsumE__4 c_Datatype__Universe_Ouprod c_Main_OuprodE__1 c_Main_OuprodE__2 c_Datatype__Universe_Ousum c_Main_OusumE__1 c_Main_OusumE__2 c_times c_Divides_Oop_Amod c_Main_Omod__eq__0D__dest__1 c_Main_Ofinite__Union__1 c_Main_Ozmod__eq__0D__dest__1 c_Main_Oin__listsI__1 c_List_Olistrel c_Main_Olistrel__Cons1__1 c_Main_Olistrel__Cons1__2 c_Main_Olistrel__Cons2__1 c_Main_Olistrel__Cons2__2 c_List_Olenlex c_Relation_ODomain c_Main_ODomainE__1 c_Main_OIdE__1 c_Main_OImageE__1 c_Relation_ORange c_Main_ORangeE__1 c_Main_OconverseE__1 c_Main_OconverseE__2 c_Relation_Odiag c_Main_OdiagE__1 c_Relation_Orel__comp c_Main_Orel__compE__2 c_Main_Orel__compE__3 c_Main_Orel__compE__1 c_SetInterval_OatLeastAtMost c_SetInterval_OatLeastLessThan c_SetInterval_OgreaterThanAtMost c_SetInterval_OgreaterThanLessThan c_Main_OInterI__1 c_Main_OUnionE__1 c_Main_OsubsetI__1 c_Sum__Type_OPlus tc_sum c_Main_OPlusE__1 c_Main_OPlusE__2 c_Transitive__Closure_Otrancl c_Wellfounded__Relations_Olex__prod tc_Datatype_Ooption tc_fun % 0.10/0.39 % Problem Properties: % 0.10/0.39 % This is a full first-order problem with equality. The Problem is non-linear. % 0.10/0.39 % 0.10/0.39 % 0.10/0.39 % SZS status GaveUp % 0.10/0.39 % 0.10/0.39 % SPASS beiseite: SPASS does currently not support equality problems. % 0.10/0.39 % Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.10/0.39 % 0.10/0.39 % SPASS-SCL-FOL Statistics: % 0.10/0.39 % Number of learned clauses: 0 % 0.10/0.39 % Number of propagations: 0 % 0.10/0.39 % Number of decisions: 0 % 0.10/0.39 % Number of resolutions: 0 % 0.10/0.39 % Number of condensations: 0 % 0.10/0.39 % Number of sub resolutions: 0 %------------------------------------------------------------------------------