%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1.1 % Problem : LCL830-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n020.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:10:32 PM UTC 2026 % Result : Unknown 0.14s 0.37s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL830-1 : TPTP v9.3.1. Released v4.1.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.35 % Computer : n020.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.10/0.35 % CPULimit : 300 % 0.10/0.35 % WCLimit : 300 % 0.10/0.35 % DateTime : Fri Sep 4 16:05:27 UTC 2026 % 0.14/0.35 % CPUTime : % 0.14/0.35 Running /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.14/0.37 % 0.14/0.37 % Input Clauses: % 0.14/0.37 % 1:1:4:INP:TopTopTopTop: -> =(c_List_Odrop(x0,c_List_Oreplicate(x1,x2,x3),x3),c_List_Oreplicate(c_HOL_Ominus__class_Ominus(x1,x0,tc_nat),x2,x3)) % 0.14/0.37 % 2:1:3:INP:TopTopTop: -> =(c_List_Orotate(x0,x1,x2),c_List_Orotate(c_Divides_Odiv__class_Omod(x0,c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),tc_nat),x1,x2)) % 0.14/0.37 % 3:1:4:INP:TopTopTopTop: -> =(c_List_Odrop(x0,c_List_Otake(x1,x2,x3),x3),c_List_Otake(c_HOL_Ominus__class_Ominus(x1,x0,tc_nat),c_List_Odrop(x0,x2,x3),x3)) % 0.14/0.37 % 4:1:3:INP:TopTopTop: -> c_lessequals(c_Nat_Osize__class_Osize(c_List_OdropWhile(x0,x1,x2),tc_List_Olist(x2)),c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),tc_nat) % 0.14/0.37 % 5:1:3:INP:TopTopTop: -> c_lessequals(c_Nat_Osize__class_Osize(c_List_OtakeWhile(x0,x1,x2),tc_List_Olist(x2)),c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),tc_nat) % 0.14/0.37 % 6:2:4:INP:TopTopTopTop: c_lessequals(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),x2,tc_nat) -> =(c_List_Olist__update(x0,x2,x3,x1),x0) % 0.14/0.37 % 7:3:5:INP:TopTopTopTopTop: c_Type_Otyping(x0,x1,x2),c_Type_Otyping(x0,x3,c_Type_Otype_OFun(x2,x4)) -> c_Type_Otyping(x0,hAPP(hAPP(c_Lambda_OdB_OApp,x3),x1),x4) % 0.14/0.37 % 8:1:3:INP:TopTopTop: -> =(c_Nat_Osize__class_Osize(c_List_Odrop(x0,x1,x2),tc_List_Olist(x2)),c_HOL_Ominus__class_Ominus(c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),x0,tc_nat)) % 0.14/0.37 % 9:4:4:INP:TopTopTopTop: class_Orderings_Olinorder(x0),c_List_Olinorder__class_Osorted(c_List_Olist_OCons(x1,x2,x0),x0),c_lessequals(x3,x1,x0) -> c_List_Olinorder__class_Osorted(c_List_Olist_OCons(x3,c_List_Olist_OCons(x1,x2,x0),x0),x0) % 0.14/0.37 % 10:3:4:INP:TopTopTopTop: class_Orderings_Olinorder(x0),c_List_Olinorder__class_Osorted(c_List_Olist_OCons(x1,c_List_Olist_OCons(x2,x3,x0),x0),x0) -> c_lessequals(x1,x2,x0) % 0.14/0.37 % 11:1:3:INP:TopTopTop: -> c_lessequals(c_Nat_Osize__class_Osize(c_List_Ofilter(x0,x1,x2),tc_List_Olist(x2)),c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),tc_nat) % 0.14/0.37 % 12:2:3:INP:TopTopTop: c_lessequals(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),x2,tc_nat) -> =(c_List_Otake(x2,x0,x1),x0) % 0.14/0.37 % 13:1:3:INP:TopTopTop: c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(x0,x1,x2),tc_List_Olist(x2)),c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),tc_nat) -> % 0.14/0.37 % 14:1:3:INP:TopTopTop: -> =(c_List_Orotate(x0,c_List_Orev(x1,x2),x2),c_List_Orev(c_List_Orotate(c_HOL_Ominus__class_Ominus(c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),c_Divides_Odiv__class_Omod(x0,c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),tc_nat),tc_nat),x1,x2),x2)) % 0.14/0.37 % 15:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0) -> c_lessequals(x1,x2,x0),c_lessequals(x2,x1,x0) % 0.14/0.37 % 16:2:2:INP:TopTop: -> c_lessequals(x0,x1,tc_nat),c_lessequals(x1,x0,tc_nat) % 0.14/0.37 % 17:4:5:INP:TopTopTopTopTop: class_OrderedGroup_Opordered__ab__group__add(x0),=(c_HOL_Ominus__class_Ominus(x1,x2,x0),c_HOL_Ominus__class_Ominus(x3,x4,x0)),c_lessequals(x4,x3,x0) -> c_lessequals(x2,x1,x0) % 0.14/0.37 % 18:4:5:INP:TopTopTopTopTop: class_OrderedGroup_Opordered__ab__group__add(x0),=(c_HOL_Ominus__class_Ominus(x1,x2,x0),c_HOL_Ominus__class_Ominus(x3,x4,x0)),c_lessequals(x2,x1,x0) -> c_lessequals(x4,x3,x0) % 0.14/0.37 % 19:2:2:INP:TopTop: class_Orderings_Opreorder(x0) -> c_lessequals(x1,x1,x0) % 0.14/0.37 % 20:2:2:INP:TopTop: class_Orderings_Oorder(x0) -> c_lessequals(x1,x1,x0) % 0.14/0.37 % 21:1:1:INP:Top: -> c_lessequals(x0,x0,tc_nat) % 0.14/0.37 % 22:3:3:INP:TopTopTop: c_lessequals(x0,x1,tc_nat),c_lessequals(x2,x0,tc_nat) -> c_lessequals(x2,x1,tc_nat) % 0.14/0.37 % 23:1:1:INP:Top: -> c_lessequals(x0,x0,tc_nat) % 0.14/0.37 % 24:4:4:INP:TopTopTopTop: class_Orderings_Opreorder(x0),c_lessequals(x1,x2,x0),c_lessequals(x3,x1,x0) -> c_lessequals(x3,x2,x0) % 0.14/0.37 % 25:4:4:INP:TopTopTopTop: class_Orderings_Oorder(x0),c_lessequals(x1,x2,x0),c_lessequals(x2,x3,x0) -> c_lessequals(x1,x3,x0) % 0.14/0.37 % 26:2:2:INP:TopTop: hBOOL(hAPP(x0,x1)) -> hBOOL(hAPP(x0,c_Divides_Odiv__class_Omod(x1,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat))) % 0.14/0.37 % 27:2:2:INP:TopTop: hBOOL(hAPP(x0,c_Divides_Odiv__class_Omod(x1,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat))) -> hBOOL(hAPP(x0,x1)) % 0.14/0.37 % 28:1:0:INP:: -> c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) % 0.14/0.37 % 29:2:4:INP:TopTopTopTop: =(c_Type_Otype_OFun(x0,x1),c_Type_Otype_OFun(x2,x3)) -> =(x0,x2) % 0.14/0.37 % 30:2:4:INP:TopTopTopTop: =(c_Type_Otype_OFun(x0,x1),c_Type_Otype_OFun(x2,x3)) -> =(x1,x3) % 0.14/0.37 % 31:2:3:INP:TopTopTop: class_Lattices_Olower__semilattice(x0) -> c_lessequals(c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0),x1,x0) % 0.14/0.37 % 32:2:3:INP:TopTopTop: class_Lattices_Olower__semilattice(x0) -> c_lessequals(c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0),x2,x0) % 0.14/0.37 % 33:4:4:INP:TopTopTopTop: class_Lattices_Olower__semilattice(x0),c_lessequals(x1,x2,x0),c_lessequals(x1,x3,x0) -> c_lessequals(x1,c_Lattices_Olower__semilattice__class_Oinf(x3,x2,x0),x0) % 0.14/0.37 % 34:4:4:INP:TopTopTopTop: class_Lattices_Olower__semilattice(x0),c_lessequals(x1,x2,x0),c_lessequals(x1,x3,x0) -> c_lessequals(x1,c_Lattices_Olower__semilattice__class_Oinf(x3,x2,x0),x0) % 0.14/0.37 % 35:4:4:INP:TopTopTopTop: class_Lattices_Olower__semilattice(x0),c_lessequals(x1,x2,x0),c_lessequals(x1,x3,x0) -> c_lessequals(x1,c_Lattices_Olower__semilattice__class_Oinf(x3,x2,x0),x0) % 0.14/0.37 % 36:2:3:INP:TopTopTop: class_Lattices_Olattice(x0) -> c_lessequals(c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0),x2,x0) % 0.14/0.37 % 37:2:3:INP:TopTopTop: class_Lattices_Olattice(x0) -> c_lessequals(c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0),x1,x0) % 0.14/0.37 % 38:3:3:INP:TopTopTop: class_OrderedGroup_Opordered__ab__group__add(x0),c_lessequals(x1,x2,x0) -> c_lessequals(c_HOL_Ominus__class_Ominus(x1,x2,x0),c_HOL_Ozero__class_Ozero(x0),x0) % 0.14/0.37 % 39:3:3:INP:TopTopTop: class_OrderedGroup_Opordered__ab__group__add(x0),c_lessequals(c_HOL_Ominus__class_Ominus(x1,x2,x0),c_HOL_Ozero__class_Ozero(x0),x0) -> c_lessequals(x1,x2,x0) % 0.14/0.37 % 40:4:6:INP:TopTopTopTopTopTop: class_Divides_Oring__div(x0),=(c_Divides_Odiv__class_Omod(x1,x2,x0),c_Divides_Odiv__class_Omod(x3,x2,x0)),=(c_Divides_Odiv__class_Omod(x4,x2,x0),c_Divides_Odiv__class_Omod(x5,x2,x0)) -> =(c_Divides_Odiv__class_Omod(c_HOL_Ominus__class_Ominus(x4,x1,x0),x2,x0),c_Divides_Odiv__class_Omod(c_HOL_Ominus__class_Ominus(x5,x3,x0),x2,x0)) % 0.14/0.37 % 41:4:3:INP:TopTopTop: class_Orderings_Oorder(x0),c_lessequals(x1,x2,x0),c_lessequals(x2,x1,x0) -> =(x1,x2) % 0.14/0.37 % 42:4:3:INP:TopTopTop: class_Orderings_Oorder(x0),c_lessequals(x1,x2,x0),c_lessequals(x2,x1,x0) -> =(x2,x1) % 0.14/0.37 % 43:4:3:INP:TopTopTop: class_Orderings_Oorder(x0),c_lessequals(x1,x2,x0),c_lessequals(x2,x1,x0) -> =(x2,x1) % 0.14/0.37 % 44:3:2:INP:TopTop: =(c_HOL_Ominus__class_Ominus(x0,x1,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),=(c_HOL_Ominus__class_Ominus(x1,x0,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) -> =(x1,x0) % 0.14/0.37 % 45:3:2:INP:TopTop: c_lessequals(x0,x1,tc_nat),c_lessequals(x1,x0,tc_nat) -> =(x1,x0) % 0.14/0.37 % 46:2:1:INP:Top: c_lessequals(x0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) -> =(x0,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.14/0.37 % 47:2:2:INP:TopTop: c_lessequals(x0,x1,tc_nat) -> =(c_Divides_Odiv__class_Omod(x1,x0,tc_nat),c_Divides_Odiv__class_Omod(c_HOL_Ominus__class_Ominus(x1,x0,tc_nat),x0,tc_nat)) % 0.14/0.37 % 48:1:1:INP:Top: -> =(c_HOL_Ominus__class_Ominus(x0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),x0) % 0.14/0.37 % 49:1:1:INP:Top: -> =(c_HOL_Ominus__class_Ominus(x0,x0,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) % 0.14/0.37 % 50:3:2:INP:TopTop: class_Ring__and__Field_Oidom(x0),class_Int_Onumber__ring(x0) -> =(c_HOL_Ominus__class_Ominus(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0)) % 0.14/0.37 % 51:2:2:INP:TopTop: class_OrderedGroup_Ogroup__add(x0) -> =(c_HOL_Ominus__class_Ominus(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0)) % 0.14/0.37 % 52:2:2:INP:TopTop: class_OrderedGroup_Ogroup__add(x0) -> =(c_HOL_Ominus__class_Ominus(x1,c_HOL_Ozero__class_Ozero(x0),x0),x1) % 0.14/0.37 % 53:2:2:INP:TopTop: class_OrderedGroup_Ogroup__add(x0) -> =(c_HOL_Ominus__class_Ominus(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0)) % 0.14/0.37 % 54:2:2:INP:TopTop: class_OrderedGroup_Oab__group__add(x0) -> =(c_HOL_Ominus__class_Ominus(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0)) % 0.14/0.37 % 55:2:2:INP:TopTop: class_Divides_Osemiring__div(x0) -> =(c_Divides_Odiv__class_Omod(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0)) % 0.14/0.37 % 56:2:2:INP:TopTop: class_Divides_Osemiring__div(x0) -> =(c_Divides_Odiv__class_Omod(x1,c_HOL_Ozero__class_Ozero(x0),x0),x1) % 0.14/0.37 % 57:2:2:INP:TopTop: c_lessequals(x0,x1,tc_nat) -> =(c_HOL_Ominus__class_Ominus(x0,x1,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) % 0.14/0.37 % 58:2:2:INP:TopTop: =(c_HOL_Ominus__class_Ominus(x0,x1,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) -> c_lessequals(x0,x1,tc_nat) % 0.14/0.37 % 59:2:3:INP:TopTopTop: class_Divides_Osemiring__div(x0) -> =(c_Divides_Odiv__class_Omod(c_Divides_Odiv__class_Omod(x1,x2,x0),x2,x0),c_Divides_Odiv__class_Omod(x1,x2,x0)) % 0.14/0.37 % 60:2:2:INP:TopTop: class_Divides_Osemiring__div(x0) -> =(c_Divides_Odiv__class_Omod(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Ozero__class_Ozero(x0)) % 0.14/0.37 % 61:2:4:INP:TopTopTopTop: class_Divides_Oring__div(x0) -> =(c_Divides_Odiv__class_Omod(c_HOL_Ominus__class_Ominus(x1,x2,x0),x3,x0),c_Divides_Odiv__class_Omod(c_HOL_Ominus__class_Ominus(c_Divides_Odiv__class_Omod(x1,x3,x0),x2,x0),x3,x0)) % 0.14/0.37 % 62:2:4:INP:TopTopTopTop: class_Divides_Oring__div(x0) -> =(c_Divides_Odiv__class_Omod(c_HOL_Ominus__class_Ominus(x1,x2,x0),x3,x0),c_Divides_Odiv__class_Omod(c_HOL_Ominus__class_Ominus(x1,c_Divides_Odiv__class_Omod(x2,x3,x0),x0),x3,x0)) % 0.14/0.37 % 63:2:3:INP:TopTopTop: c_lessequals(x0,x1,tc_nat) -> c_lessequals(c_HOL_Ominus__class_Ominus(x2,x1,tc_nat),c_HOL_Ominus__class_Ominus(x2,x0,tc_nat),tc_nat) % 0.14/0.37 % 64:2:3:INP:TopTopTop: c_lessequals(x0,x1,tc_nat) -> c_lessequals(c_HOL_Ominus__class_Ominus(x0,x2,tc_nat),c_HOL_Ominus__class_Ominus(x1,x2,tc_nat),tc_nat) % 0.14/0.37 % 65:4:3:INP:TopTopTop: c_lessequals(x0,x1,tc_nat),c_lessequals(x2,x1,tc_nat),c_lessequals(x2,x0,tc_nat) -> c_lessequals(c_HOL_Ominus__class_Ominus(x0,x2,tc_nat),c_HOL_Ominus__class_Ominus(x1,x2,tc_nat),tc_nat) % 0.14/0.37 % 66:4:3:INP:TopTopTop: c_lessequals(c_HOL_Ominus__class_Ominus(x0,x1,tc_nat),c_HOL_Ominus__class_Ominus(x2,x1,tc_nat),tc_nat),c_lessequals(x1,x2,tc_nat),c_lessequals(x1,x0,tc_nat) -> c_lessequals(x0,x2,tc_nat) % 0.14/0.37 % 67:3:4:INP:TopTopTopTop: class_OrderedGroup_Oab__group__add(x0),=(c_HOL_Ominus__class_Ominus(x1,x2,x0),c_HOL_Ominus__class_Ominus(x3,x3,x0)) -> =(x1,x2) % 0.14/0.37 % 68:3:4:INP:TopTopTopTop: class_OrderedGroup_Oab__group__add(x0),=(c_HOL_Ominus__class_Ominus(x1,x1,x0),c_HOL_Ominus__class_Ominus(x2,x3,x0)) -> =(x2,x3) % 0.14/0.37 % 69:4:3:INP:TopTopTop: =(c_HOL_Ominus__class_Ominus(x0,x1,tc_nat),c_HOL_Ominus__class_Ominus(x2,x1,tc_nat)),c_lessequals(x1,x2,tc_nat),c_lessequals(x1,x0,tc_nat) -> =(x0,x2) % 0.14/0.37 % 70:4:3:INP:TopTopTop: class_Int_Oring__char__0(x0),class_Int_Onumber__ring(x0),=(c_Int_Onumber__class_Onumber__of(x1,x0),c_Int_Onumber__class_Onumber__of(x2,x0)) -> =(x1,x2) % 0.14/0.37 % 71:1:1:INP:Top: -> =(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) % 0.14/0.37 % 72:3:3:INP:TopTopTop: class_Lattices_Olower__semilattice(x0),c_lessequals(x1,x2,x0) -> =(c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0),x1) % 0.14/0.37 % 73:3:3:INP:TopTopTop: class_Lattices_Olower__semilattice(x0),=(c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0),x1) -> c_lessequals(x1,x2,x0) % 0.14/0.37 % 74:3:3:INP:TopTopTop: class_Lattices_Olower__semilattice(x0),c_lessequals(x1,x2,x0) -> =(c_Lattices_Olower__semilattice__class_Oinf(x2,x1,x0),x1) % 0.14/0.37 % 75:1:2:INP:TopTop: -> c_lessequals(c_HOL_Ominus__class_Ominus(x0,x1,tc_nat),x0,tc_nat) % 0.14/0.37 % 76:4:3:INP:TopTopTop: class_Ring__and__Field_Oidom(x0),class_Int_Onumber__ring(x0),=(c_HOL_Ominus__class_Ominus(x1,x2,x0),c_HOL_Ozero__class_Ozero(x0)) -> =(x1,x2) % 0.14/0.37 % 77:3:3:INP:TopTopTop: class_OrderedGroup_Ogroup__add(x0),=(c_HOL_Ominus__class_Ominus(x1,x2,x0),c_HOL_Ozero__class_Ozero(x0)) -> =(x1,x2) % 0.14/0.37 % 78:3:3:INP:TopTopTop: class_OrderedGroup_Oab__group__add(x0),=(c_HOL_Ominus__class_Ominus(x1,x2,x0),c_HOL_Ozero__class_Ozero(x0)) -> =(x1,x2) % 0.14/0.37 % 79:3:3:INP:TopTopTop: c_lessequals(x0,x1,tc_nat),c_lessequals(x0,x2,tc_nat) -> =(c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(x2,x0,tc_nat),c_HOL_Ominus__class_Ominus(x1,x0,tc_nat),tc_nat),c_HOL_Ominus__class_Ominus(x2,x1,tc_nat)) % 0.14/0.37 % 80:1:3:INP:TopTopTop: -> =(c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(x0,x1,tc_nat),x2,tc_nat),c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(x0,x2,tc_nat),x1,tc_nat)) % 0.14/0.37 % 81:1:1:INP:Top: -> c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat) % 0.14/0.37 % 82:1:2:INP:TopTop: -> c_lessequals(c_Divides_Odiv__class_Omod(x0,x1,tc_nat),x0,tc_nat) % 0.14/0.37 % 83:2:4:INP:TopTopTopTop: class_Divides_Oring__div(x0) -> =(c_Divides_Odiv__class_Omod(c_HOL_Ominus__class_Ominus(x1,x2,x0),x3,x0),c_Divides_Odiv__class_Omod(c_HOL_Ominus__class_Ominus(c_Divides_Odiv__class_Omod(x1,x3,x0),c_Divides_Odiv__class_Omod(x2,x3,x0),x0),x3,x0)) % 0.14/0.37 % 84:3:4:INP:TopTopTopTop: class_Lattices_Olower__semilattice(x0),c_lessequals(x1,c_Lattices_Olower__semilattice__class_Oinf(x2,x3,x0),x0) -> c_lessequals(x1,x2,x0) % 0.14/0.37 % 85:3:4:INP:TopTopTopTop: class_Lattices_Olower__semilattice(x0),c_lessequals(x1,c_Lattices_Olower__semilattice__class_Oinf(x2,x3,x0),x0) -> c_lessequals(x1,x3,x0) % 0.14/0.37 % 86:3:4:INP:TopTopTopTop: class_Lattices_Olower__semilattice(x0),c_lessequals(x1,x2,x0) -> c_lessequals(c_Lattices_Olower__semilattice__class_Oinf(x1,x3,x0),x2,x0) % 0.14/0.37 % 87:3:4:INP:TopTopTopTop: class_Lattices_Olower__semilattice(x0),c_lessequals(x1,x2,x0) -> c_lessequals(c_Lattices_Olower__semilattice__class_Oinf(x3,x1,x0),x2,x0) % 0.14/0.37 % 88:3:4:INP:TopTopTopTop: class_Lattices_Olower__semilattice(x0),c_lessequals(x1,c_Lattices_Olower__semilattice__class_Oinf(x2,x3,x0),x0) -> c_lessequals(x1,x2,x0) % 0.14/0.37 % 89:3:4:INP:TopTopTopTop: class_Lattices_Olower__semilattice(x0),c_lessequals(x1,c_Lattices_Olower__semilattice__class_Oinf(x2,x3,x0),x0) -> c_lessequals(x1,x3,x0) % 0.14/0.37 % 90:2:2:INP:TopTop: c_lessequals(x0,x1,tc_nat) -> =(c_HOL_Ominus__class_Ominus(x1,c_HOL_Ominus__class_Ominus(x1,x0,tc_nat),tc_nat),x0) % 0.14/0.37 % 91:2:4:INP:TopTopTopTop: =(c_Int_Onumber__class_Onumber__of(x0,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) -> =(c_List_Odrop(c_Int_Onumber__class_Onumber__of(x0,tc_nat),c_List_Olist_OCons(x1,x2,x3),x3),c_List_Olist_OCons(x1,x2,x3)) % 0.14/0.37 % 92:2:3:INP:TopTopTop: =(c_List_Odrop(x0,x1,x2),c_List_Olist_ONil(x2)) -> c_lessequals(c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),x0,tc_nat) % 0.14/0.37 % 93:2:3:INP:TopTopTop: c_lessequals(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),x2,tc_nat) -> =(c_List_Odrop(x2,x0,x1),c_List_Olist_ONil(x1)) % 0.14/0.37 % 94:3:5:INP:TopTopTopTopTop: =(c_List_Oappend(x0,x1,x2),c_List_Oappend(x3,x4,x2)) -> =(c_List_Otake(c_Nat_Osize__class_Osize(x3,tc_List_Olist(x2)),x0,x2),x3),c_lessequals(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x2)),c_Nat_Osize__class_Osize(x3,tc_List_Olist(x2)),tc_nat) % 0.14/0.37 % 95:1:4:INP:TopTopTopTop: -> =(c_List_Otake(x0,c_List_Oappend(x1,x2,x3),x3),c_List_Oappend(c_List_Otake(x0,x1,x3),c_List_Otake(c_HOL_Ominus__class_Ominus(x0,c_Nat_Osize__class_Osize(x1,tc_List_Olist(x3)),tc_nat),x2,x3),x3)) % 0.14/0.37 % 96:3:5:INP:TopTopTopTopTop: =(c_List_Oappend(x0,x1,x2),c_List_Oappend(x3,x4,x2)),c_lessequals(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x2)),c_Nat_Osize__class_Osize(x3,tc_List_Olist(x2)),tc_nat) -> =(x0,c_List_Otake(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x2)),x3,x2)) % 0.14/0.37 % 97:3:5:INP:TopTopTopTopTop: =(c_List_Oappend(x0,x1,x2),c_List_Oappend(x3,x4,x2)),c_lessequals(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x2)),c_Nat_Osize__class_Osize(x3,tc_List_Olist(x2)),tc_nat) -> =(x1,c_List_Oappend(c_List_Odrop(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x2)),x3,x2),x4,x2)) % 0.14/0.37 % 98:3:5:INP:TopTopTopTopTop: =(c_List_Oappend(x0,x1,x2),c_List_Oappend(x3,x4,x2)) -> =(c_List_Oappend(c_List_Odrop(c_Nat_Osize__class_Osize(x3,tc_List_Olist(x2)),x0,x2),x1,x2),x4),c_lessequals(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x2)),c_Nat_Osize__class_Osize(x3,tc_List_Olist(x2)),tc_nat) % 0.14/0.37 % 99:1:4:INP:TopTopTopTop: -> =(c_List_Odrop(x0,c_List_Oappend(x1,x2,x3),x3),c_List_Oappend(c_List_Odrop(x0,x1,x3),c_List_Odrop(c_HOL_Ominus__class_Ominus(x0,c_Nat_Osize__class_Osize(x1,tc_List_Olist(x3)),tc_nat),x2,x3),x3)) % 0.14/0.37 % 100:2:3:INP:TopTopTop: =(c_Divides_Odiv__class_Omod(x0,c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) -> =(c_List_Orotate(x0,x1,x2),x1) % 0.14/0.37 % 101:1:2:INP:TopTop: -> =(x0,c_List_Oappend(c_List_Olist_ONil(x1),x0,x1)) % 0.14/0.37 % 102:2:3:INP:TopTopTop: c_List_Odistinct(c_List_Oappend(x0,x1,x2),x2) -> c_List_Odistinct(x0,x2) % 0.14/0.37 % 103:2:3:INP:TopTopTop: c_List_Odistinct(c_List_Oappend(x0,x1,x2),x2) -> c_List_Odistinct(x1,x2) % 0.14/0.37 % 104:1:2:INP:TopTop: -> =(x0,c_List_Orev(c_List_Orev(x0,x1),x1)) % 0.14/0.37 % 105:1:2:INP:TopTop: -> =(c_List_Orev(c_List_Orev(x0,x1),x1),x0) % 0.14/0.37 % 106:1:2:INP:TopTop: -> =(c_List_Orev(c_List_Orev(x0,x1),x1),x0) % 0.14/0.37 % 107:1:2:INP:TopTop: -> =(c_List_OdropWhile(x0,c_List_Olist_ONil(x1),x1),c_List_Olist_ONil(x1)) % 0.14/0.37 % 108:1:3:INP:TopTopTop: -> =(x0,c_List_Otake(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),c_List_Oappend(x0,x2,x1),x1)) % 0.14/0.37 % 109:2:3:INP:TopTopTop: c_List_Odistinct(x0,x1) -> c_List_Odistinct(c_List_OdropWhile(x2,x0,x1),x1) % 0.14/0.37 % 110:1:5:INP:TopTopTopTopTop: -> =(c_List_Omap__filter(x0,x1,x2,x3,x4),c_List_Omap(x0,c_List_Ofilter(x1,x2,x3),x3,x4)) % 0.14/0.37 % 111:2:5:INP:TopTopTopTopTop: c_List_Olist__all2(x0,c_List_Orev(x1,x2),c_List_Orev(x3,x4),x2,x4) -> c_List_Olist__all2(x0,x1,x3,x2,x4) % 0.14/0.37 % 112:2:5:INP:TopTopTopTopTop: c_List_Olist__all2(x0,x1,x2,x3,x4) -> c_List_Olist__all2(x0,c_List_Orev(x1,x3),c_List_Orev(x2,x4),x3,x4) % 0.14/0.37 % 113:1:3:INP:TopTopTop: -> =(hAPP(hAPP(c_Lambda_Olift,hAPP(hAPP(c_Lambda_OdB_OApp,x0),x1)),x2),hAPP(hAPP(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_Olift,x0),x2)),hAPP(hAPP(c_Lambda_Olift,x1),x2))) % 0.14/0.37 % 114:1:3:INP:TopTopTop: -> =(c_List_Orev(c_List_Oreplicate(x0,x1,x2),x2),c_List_Oreplicate(x0,x1,x2)) % 0.14/0.37 % 115:3:6:INP:TopTopTopTopTopTop: c_ListOrder_Ostep1(x0,c_List_Oappend(x1,c_List_Olist_OCons(x2,c_List_Olist_ONil(x3),x3),x3),c_List_Oappend(x4,c_List_Olist_OCons(x5,c_List_Olist_ONil(x3),x3),x3),x3) -> hBOOL(hAPP(hAPP(x0,x2),x5)),=(x2,x5) % 0.14/0.37 % 116:2:3:INP:TopTopTop: =(c_List_Orev(x0,x1),c_List_Olist_OCons(x2,c_List_Olist_ONil(x1),x1)) -> =(x0,c_List_Olist_OCons(x2,c_List_Olist_ONil(x1),x1)) % 0.14/0.37 % 117:2:3:INP:TopTopTop: c_Type_Otyping(x0,c_Lambda_OdB_OVar(x1),x2) -> =(hAPP(x0,x1),x2) % 0.14/0.37 % 118:1:2:INP:TopTop: -> =(c_List_Odrop(x0,c_List_Olist_ONil(x1),x1),c_List_Olist_ONil(x1)) % 0.14/0.37 % 119:1:6:INP:TopTopTopTopTopTop: -> =(hAPP(c_Fun_Ocomp(x0,x1,x2,x3,x4),x5),hAPP(x0,hAPP(x1,x5))) % 0.14/0.37 % 120:1:6:INP:TopTopTopTopTopTop: -> =(hAPP(x0,hAPP(x1,x2)),hAPP(c_Fun_Ocomp(x0,x1,x3,x4,x5),x2)) % 0.14/0.37 % 121:1:2:INP:TopTop: =(c_Lambda_OdB_OVar(x0),c_Lambda_OdB_OAbs(x1)) -> % 0.14/0.37 % 122:2:5:INP:TopTopTopTopTop: c_List_Olist__all2(x0,x1,x2,x3,x4) -> =(c_Nat_Osize__class_Osize(x1,tc_List_Olist(x3)),c_Nat_Osize__class_Osize(x2,tc_List_Olist(x4))) % 0.14/0.37 % 123:1:3:INP:TopTopTop: c_ListOrder_Ostep1(x0,c_List_Olist_ONil(x1),x2,x1) -> % 0.14/0.37 % 124:1:3:INP:TopTopTop: c_ListOrder_Ostep1(x0,x1,c_List_Olist_ONil(x2),x2) -> % 0.14/0.37 % 125:3:3:INP:TopTopTop: hBOOL(hAPP(c_InductTermi_OIT,x0)),hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,x1),x0),c_HOL_Ozero__class_Ozero(tc_nat)),x2,tc_Lambda_OdB,tc_Lambda_OdB))) -> hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(x1)),x0),x2,tc_Lambda_OdB,tc_Lambda_OdB))) % 0.14/0.37 % 126:2:4:INP:TopTopTopTop: hBOOL(hAPP(x0,x1)) -> =(c_List_Ofilter(x0,c_List_Oreplicate(x2,x1,x3),x3),c_List_Oreplicate(x2,x1,x3)) % 0.14/0.37 % 127:1:4:INP:TopTopTopTop: -> =(c_List_Ofoldl(x0,x1,c_List_Olist_ONil(x2),x3,x2),x1) % 0.14/0.37 % 128:1:4:INP:TopTopTopTop: -> =(hAPP(c_Type_Oshift(x0,x1,x2,x3),x1),x2) % 0.14/0.37 % 129:1:4:INP:TopTopTopTop: =(c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x0),x1,tc_Lambda_OdB,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(x2),x3,tc_Lambda_OdB,tc_Lambda_OdB)) -> % 0.14/0.37 % 130:2:4:INP:TopTopTopTop: class_Lattices_Olattice(x0) -> =(c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0),x3,x0),c_Lattices_Olower__semilattice__class_Oinf(x1,c_Lattices_Olower__semilattice__class_Oinf(x2,x3,x0),x0)) % 0.14/0.37 % 131:2:4:INP:TopTopTopTop: class_Lattices_Olattice(x0) -> =(c_Lattices_Olower__semilattice__class_Oinf(x1,c_Lattices_Olower__semilattice__class_Oinf(x2,x3,x0),x0),c_Lattices_Olower__semilattice__class_Oinf(x2,c_Lattices_Olower__semilattice__class_Oinf(x1,x3,x0),x0)) % 0.14/0.37 % 132:2:4:INP:TopTopTopTop: class_Lattices_Olower__semilattice(x0) -> =(c_Lattices_Olower__semilattice__class_Oinf(x1,c_Lattices_Olower__semilattice__class_Oinf(x2,x3,x0),x0),c_Lattices_Olower__semilattice__class_Oinf(x2,c_Lattices_Olower__semilattice__class_Oinf(x1,x3,x0),x0)) % 0.14/0.37 % 133:2:4:INP:TopTopTopTop: class_Lattices_Olower__semilattice(x0) -> =(c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0),x3,x0),c_Lattices_Olower__semilattice__class_Oinf(x1,c_Lattices_Olower__semilattice__class_Oinf(x2,x3,x0),x0)) % 0.14/0.37 % 134:1:4:INP:TopTopTopTop: -> =(c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(x0,x1,tc_fun(x2,tc_bool)),x3,tc_fun(x2,tc_bool)),c_Lattices_Olower__semilattice__class_Oinf(x0,c_Lattices_Olower__semilattice__class_Oinf(x1,x3,tc_fun(x2,tc_bool)),tc_fun(x2,tc_bool))) % 0.14/0.37 % 135:6:7:INP:TopTopTopTopTopTopTop: =(v_T____,c_Type_Otype_OFun(x0,x1)),c_Type_Otyping(x2,x3,x0),hBOOL(hAPP(c_InductTermi_OIT,x3)),c_Type_Otyping(c_Type_Oshift(x2,x4,x0,tc_Type_Otype),x5,x6),hBOOL(hAPP(c_InductTermi_OIT,x5)) -> hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,x5),x3),x4))) % 0.14/0.37 % 136:6:7:INP:TopTopTopTopTopTopTop: =(v_T____,c_Type_Otype_OFun(x0,x1)),c_Type_Otyping(x2,x3,x1),hBOOL(hAPP(c_InductTermi_OIT,x3)),c_Type_Otyping(c_Type_Oshift(x2,x4,x1,tc_Type_Otype),x5,x6),hBOOL(hAPP(c_InductTermi_OIT,x5)) -> hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,x5),x3),x4))) % 0.14/0.37 % 137:4:7:INP:TopTopTopTopTopTopTop: c_Type_Otyping(x0,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x1),x2,tc_Lambda_OdB,tc_Lambda_OdB),x3),c_Type_Otypings(x0,x2,x4),c_Type_Otyping(x0,c_List_Ofoldl(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x1),x2,tc_Lambda_OdB,tc_Lambda_OdB),x5,tc_Lambda_OdB,tc_Lambda_OdB),x6) -> c_Type_Otypings(x0,x5,c_Type_Osko__Type__Xvar__app__types__1__1(x6,x3,x0,x5)) % 0.14/0.37 % 138:2:4:INP:TopTopTopTop: c_Type_Otyping(x0,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x1),x2,tc_Lambda_OdB,tc_Lambda_OdB),x3) -> c_Type_Otypings(x0,x2,c_Type_Osko__Type__Xvar__app__typesE__1__1(x3,x0,x1,x2)) % 0.14/0.37 % 139:1:3:INP:TopTopTop: -> =(c_List_Orotate(x0,x1,x2),c_List_Oappend(c_List_Odrop(c_Divides_Odiv__class_Omod(x0,c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),tc_nat),x1,x2),c_List_Otake(c_Divides_Odiv__class_Omod(x0,c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),tc_nat),x1,x2),x2)) % 0.14/0.37 % 140:1:0:INP:: -> c_Type_Otyping(v_ea______,v_ua______,v_T____) % 0.14/0.37 % 141:2:4:INP:TopTopTopTop: c_Type_Otyping(c_Type_Oshift(x0,c_HOL_Ozero__class_Ozero(tc_nat),x1,tc_Type_Otype),x2,x3) -> c_Type_Otyping(x0,c_Lambda_OdB_OAbs(x2),c_Type_Otype_OFun(x1,x3)) % 0.14/0.37 % 142:2:4:INP:TopTopTopTop: c_Type_Otyping(x0,c_List_Ofoldl(c_Lambda_OdB_OApp,x1,x2,tc_Lambda_OdB,tc_Lambda_OdB),x3) -> c_Type_Otypings(x0,x2,c_Type_Osko__Type__Xlist__app__typeE__1__1(x3,x0,x1,x2)) % 0.14/0.37 % 143:2:4:INP:TopTopTopTop: c_Type_Otyping(x0,c_List_Ofoldl(c_Lambda_OdB_OApp,x1,x2,tc_Lambda_OdB,tc_Lambda_OdB),x3) -> c_Type_Otypings(x0,x2,c_Type_Osko__Type__Xlist__app__typeD__1__1(x3,x0,x1,x2)) % 0.14/0.37 % 144:1:3:INP:TopTopTop: -> =(c_List_Orev(c_List_Odrop(x0,x1,x2),x2),c_List_Otake(c_HOL_Ominus__class_Ominus(c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),x0,tc_nat),c_List_Orev(x1,x2),x2)) % 0.14/0.37 % 145:1:3:INP:TopTopTop: -> =(c_List_Orev(c_List_Otake(x0,x1,x2),x2),c_List_Odrop(c_HOL_Ominus__class_Ominus(c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),x0,tc_nat),c_List_Orev(x1,x2),x2)) % 0.14/0.37 % 146:1:0:INP:: -> c_Type_Otyping(v_e____,v_u____,v_T____) % 0.14/0.37 % 147:3:4:INP:TopTopTopTop: =(x0,c_List_Otake(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),x2,x1)),c_lessequals(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),c_Nat_Osize__class_Osize(x2,tc_List_Olist(x1)),tc_nat) -> =(c_List_Oappend(x0,c_List_Oappend(c_List_Odrop(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),x2,x1),x3,x1),x1),c_List_Oappend(x2,x3,x1)) % 0.14/0.37 % 148:3:4:INP:TopTopTopTop: =(c_List_Otake(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),x2,x1),x0) -> c_lessequals(c_Nat_Osize__class_Osize(x2,tc_List_Olist(x1)),c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),tc_nat),=(c_List_Oappend(x2,x3,x1),c_List_Oappend(x0,c_List_Oappend(c_List_Odrop(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),x2,x1),x3,x1),x1)) % 0.14/0.37 % 149:2:3:INP:TopTopTop: c_Lambda_Obeta(c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x0),x1,tc_Lambda_OdB,tc_Lambda_OdB),x2) -> =(x2,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x0),c_ListBeta_Osko__ListBeta__Xhead__Var__reduction__1__1(x0,x1,x2),tc_Lambda_OdB,tc_Lambda_OdB)) % 0.14/0.37 % 150:2:4:INP:TopTopTopTop: =(c_Int_Onumber__class_Onumber__of(x0,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) -> =(c_List_Otake(c_Int_Onumber__class_Onumber__of(x0,tc_nat),c_List_Olist_OCons(x1,x2,x3),x3),c_List_Olist_ONil(x3)) % 0.14/0.37 % 151:1:2:INP:TopTop: -> =(c_List_Oappend(c_List_Olist_ONil(x0),x1,x0),x1) % 0.14/0.37 % 152:1:2:INP:TopTop: -> =(x0,c_List_Oappend(x0,c_List_Olist_ONil(x1),x1)) % 0.14/0.37 % 153:1:2:INP:TopTop: -> =(x0,c_List_Oappend(c_List_Olist_ONil(x1),x0,x1)) % 0.14/0.37 % 154:1:2:INP:TopTop: -> =(c_List_Oappend(x0,c_List_Olist_ONil(x1),x1),x0) % 0.14/0.37 % 155:1:3:INP:TopTopTop: -> =(c_List_OtakeWhile(x0,x1,x2),c_List_Otake(c_Nat_Osize__class_Osize(c_List_OtakeWhile(x0,x1,x2),tc_List_Olist(x2)),x1,x2)) % 0.14/0.37 % 156:1:2:INP:TopTop: -> =(c_List_Otake(x0,c_List_Olist_ONil(x1),x1),c_List_Olist_ONil(x1)) % 0.14/0.37 % 157:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_List_Olinorder__class_Osorted(x1,x0) -> c_List_Olinorder__class_Osorted(c_List_Otake(x2,x1,x0),x0) % 0.14/0.37 % 158:2:4:INP:TopTopTopTop: =(c_List_Oappend(x0,x1,x2),c_List_Oappend(x0,x3,x2)) -> =(x1,x3) % 0.14/0.37 % 159:2:4:INP:TopTopTopTop: =(c_List_Oappend(x0,x1,x2),c_List_Oappend(x3,x1,x2)) -> =(x0,x3) % 0.14/0.37 % 160:2:5:INP:TopTopTopTopTop: =(c_List_Oreplicate(x0,x1,x2),c_List_Oreplicate(x3,x4,x2)) -> =(x0,x3) % 0.14/0.37 % 161:1:2:INP:TopTop: -> c_List_Olist__all(x0,c_List_Olist_ONil(x1),x1) % 0.14/0.37 % 162:2:4:INP:TopTopTopTop: -> =(c_List_OtakeWhile(x0,c_List_Olist_OCons(x1,x2,x3),x3),c_List_Olist_ONil(x3)),hBOOL(hAPP(x0,x1)) % 0.14/0.37 % 163:1:2:INP:TopTop: c_List_Olist__ex(x0,c_List_Olist_ONil(x1),x1) -> % 0.14/0.37 % 164:2:5:INP:TopTopTopTopTop: c_ListOrder_Ostep1(x0,x1,x2,x3) -> c_ListOrder_Ostep1(x0,c_List_Oappend(x4,x1,x3),c_List_Oappend(x4,x2,x3),x3) % 0.14/0.37 % 165:2:5:INP:TopTopTopTopTop: c_ListOrder_Ostep1(x0,x1,x2,x3) -> c_ListOrder_Ostep1(x0,c_List_Oappend(x1,x4,x3),c_List_Oappend(x2,x4,x3),x3) % 0.14/0.37 % 166:2:3:INP:TopTopTop: =(c_List_Olist_OCons(x0,c_List_Olist_ONil(x1),x1),c_List_Orev(x2,x1)) -> =(x2,c_List_Olist_OCons(x0,c_List_Olist_ONil(x1),x1)) % 0.14/0.37 % 167:2:3:INP:TopTopTop: hBOOL(hAPP(x0,c_List_Olist_Olist__case(x1,x2,c_List_Olist_ONil(t_b),t_a,t_b))) -> hBOOL(hAPP(x0,x1)) % 0.14/0.37 % 168:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_List_Olinorder__class_Osorted(x1,x0) -> c_List_Olinorder__class_Osorted(c_List_Odrop(x2,x1,x0),x0) % 0.14/0.37 % 169:1:3:INP:TopTopTop: -> =(c_List_Odrop(c_HOL_Ozero__class_Ozero(tc_nat),c_List_Olist_OCons(x0,x1,x2),x2),c_List_Olist_OCons(x0,x1,x2)) % 0.14/0.37 % 170:2:6:INP:TopTopTopTopTopTop: c_List_Olist__all2(x0,x1,x2,x3,x4) -> c_List_Olist__all2(x0,c_List_Otake(x5,x1,x3),c_List_Otake(x5,x2,x4),x3,x4) % 0.14/0.37 % 171:2:4:INP:TopTopTopTop: -> =(c_List_OremoveAll(x0,c_List_Ofilter(x1,x2,x3),x3),c_List_Ofilter(x1,x2,x3)),hBOOL(hAPP(x1,x0)) % 0.14/0.37 % 172:1:3:INP:TopTopTop: -> =(c_List_Orev(c_List_Olist_OCons(x0,x1,x2),x2),c_List_Oappend(c_List_Orev(x1,x2),c_List_Olist_OCons(x0,c_List_Olist_ONil(x2),x2),x2)) % 0.14/0.37 % 173:2:3:INP:TopTopTop: c_List_Olist__all2(c_fequal(x0),x1,x2,x0,x0) -> =(x1,x2) % 0.14/0.37 % 174:2:1:INP:Top: class_Orderings_Olinorder(x0) -> c_List_Olinorder__class_Osorted(c_List_Olist_ONil(x0),x0) % 0.14/0.37 % 175:1:2:INP:TopTop: -> =(c_List_Odrop(c_HOL_Ozero__class_Ozero(tc_nat),x0,x1),x0) % 0.14/0.37 % 176:3:6:INP:TopTopTopTopTopTop: c_ListOrder_Ostep1(x0,c_List_Oappend(x1,c_List_Olist_OCons(x2,c_List_Olist_ONil(x3),x3),x3),c_List_Oappend(x4,c_List_Olist_OCons(x5,c_List_Olist_ONil(x3),x3),x3),x3) -> hBOOL(hAPP(hAPP(x0,x2),x5)),c_ListOrder_Ostep1(x0,x1,x4,x3) % 0.14/0.37 % 177:1:2:INP:TopTop: -> =(c_List_Orev(c_List_Olist_OCons(x0,c_List_Olist_ONil(x1),x1),x1),c_List_Olist_OCons(x0,c_List_Olist_ONil(x1),x1)) % 0.14/0.37 % 178:2:4:INP:TopTopTopTop: =(c_List_Orev(x0,x1),c_List_Olist_OCons(x2,x3,x1)) -> =(x0,c_List_Oappend(c_List_Orev(x3,x1),c_List_Olist_OCons(x2,c_List_Olist_ONil(x1),x1),x1)) % 0.14/0.37 % 179:1:3:INP:TopTopTop: -> =(c_Lattices_Olower__semilattice__class_Oinf(x0,x1,tc_fun(x2,tc_bool)),c_Lattices_Olower__semilattice__class_Oinf(x1,x0,tc_fun(x2,tc_bool))) % 0.14/0.37 % 180:2:3:INP:TopTopTop: class_Lattices_Olower__semilattice(x0) -> =(c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0),c_Lattices_Olower__semilattice__class_Oinf(x2,x1,x0)) % 0.14/0.37 % 181:2:3:INP:TopTopTop: class_Lattices_Olattice(x0) -> =(c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0),c_Lattices_Olower__semilattice__class_Oinf(x2,x1,x0)) % 0.14/0.37 % 182:1:2:INP:TopTop: -> c_Type_Otyping(x0,c_Lambda_OdB_OVar(x1),hAPP(x0,x1)) % 0.14/0.37 % 183:2:3:INP:TopTopTop: =(c_Lambda_OdB_OAbs(x0),c_List_Ofoldl(c_Lambda_OdB_OApp,x1,x2,tc_Lambda_OdB,tc_Lambda_OdB)) -> =(c_Lambda_OdB_OAbs(x0),x1) % 0.14/0.37 % 184:3:7:INP:TopTopTopTopTopTopTop: c_List_Olist__all2(x0,x1,x2,x3,x4),c_List_Olist__all2(x0,x5,x6,x3,x4) -> c_List_Olist__all2(x0,c_List_Oappend(x5,x1,x3),c_List_Oappend(x6,x2,x4),x3,x4) % 0.14/0.37 % 185:5:7:INP:TopTopTopTopTopTopTop: =(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),c_Nat_Osize__class_Osize(x2,tc_List_Olist(x3))),=(c_Nat_Osize__class_Osize(x4,tc_List_Olist(x1)),c_Nat_Osize__class_Osize(x5,tc_List_Olist(x3))),c_List_Olist__all2(x6,x0,x2,x1,x3),c_List_Olist__all2(x6,x4,x5,x1,x3) -> c_List_Olist__all2(x6,c_List_Oappend(x4,x0,x1),c_List_Oappend(x5,x2,x3),x1,x3) % 0.14/0.37 % 186:5:7:INP:TopTopTopTopTopTopTop: =(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),c_Nat_Osize__class_Osize(x2,tc_List_Olist(x3))),=(c_Nat_Osize__class_Osize(x4,tc_List_Olist(x1)),c_Nat_Osize__class_Osize(x5,tc_List_Olist(x3))),c_List_Olist__all2(x6,x2,x0,x3,x1),c_List_Olist__all2(x6,x5,x4,x3,x1) -> c_List_Olist__all2(x6,c_List_Oappend(x5,x2,x3),c_List_Oappend(x4,x0,x1),x3,x1) % 0.14/0.37 % 187:1:3:INP:TopTopTop: -> =(x0,c_List_Odrop(c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),c_List_Oappend(x1,x0,x2),x2)) % 0.14/0.37 % 188:2:3:INP:TopTopTop: c_List_Odistinct(x0,x1) -> c_List_Odistinct(c_List_Ofilter(x2,x0,x1),x1) % 0.14/0.37 % 189:1:2:INP:TopTop: -> =(c_List_Ofilter(x0,c_List_Olist_ONil(x1),x1),c_List_Olist_ONil(x1)) % 0.14/0.37 % 190:3:3:INP:TopTopTop: =(c_List_Otake(x0,x1,x2),c_List_Olist_ONil(x2)) -> =(x1,c_List_Olist_ONil(x2)),=(x0,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.14/0.37 % 191:1:3:INP:TopTopTop: -> =(c_List_Olist__update(c_List_Olist_ONil(x0),x1,x2,x0),c_List_Olist_ONil(x0)) % 0.14/0.37 % 192:1:3:INP:TopTopTop: -> =(c_List_Olist__update(c_List_Olist_ONil(x0),x1,x2,x0),c_List_Olist_ONil(x0)) % 0.14/0.37 % 193:1:3:INP:TopTopTop: -> =(c_List_Olist__update(c_List_Olist_ONil(x0),x1,x2,x0),c_List_Olist_ONil(x0)) % 0.14/0.37 % 194:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_List_Olinorder__class_Osorted(x1,x0) -> c_List_Olinorder__class_Osorted(c_List_OtakeWhile(x2,x1,x0),x0) % 0.14/0.37 % 195:2:3:INP:TopTopTop: =(c_List_Ofoldl(c_Lambda_OdB_OApp,x0,x1,tc_Lambda_OdB,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,x2,x1,tc_Lambda_OdB,tc_Lambda_OdB)) -> =(x0,x2) % 0.14/0.37 % 196:1:3:INP:TopTopTop: -> =(c_List_Oappend(c_List_Otake(x0,x1,x2),c_List_Odrop(x0,x1,x2),x2),x1) % 0.14/0.37 % 197:1:2:INP:TopTop: -> =(c_List_Oremove1(x0,c_List_Olist_ONil(x1),x1),c_List_Olist_ONil(x1)) % 0.14/0.37 % 198:2:3:INP:TopTopTop: c_Lambda_Obeta(x0,x1) -> c_Lambda_Obeta(hAPP(hAPP(c_Lambda_OdB_OApp,x2),x0),hAPP(hAPP(c_Lambda_OdB_OApp,x2),x1)) % 0.14/0.37 % 199:2:3:INP:TopTopTop: c_Lambda_Obeta(x0,x1) -> c_Lambda_Obeta(hAPP(hAPP(c_Lambda_OdB_OApp,x0),x2),hAPP(hAPP(c_Lambda_OdB_OApp,x1),x2)) % 0.14/0.37 % 200:1:3:INP:TopTopTop: -> =(c_List_Orev(c_List_Oappend(c_List_Orev(x0,x1),c_List_Olist_OCons(x2,c_List_Olist_ONil(x1),x1),x1),x1),c_List_Olist_OCons(x2,x0,x1)) % 0.14/0.37 % 201:1:3:INP:TopTopTop: -> =(c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),x0,x1),c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),x2,x1)) % 0.14/0.37 % 202:2:3:INP:TopTopTop: c_List_Odistinct(x0,x1) -> c_List_Odistinct(c_List_Odrop(x2,x0,x1),x1) % 0.14/0.37 % 203:2:2:INP:TopTop: c_List_Odistinct(x0,x1) -> c_List_Odistinct(c_List_Orev(x0,x1),x1) % 0.14/0.37 % 204:2:2:INP:TopTop: c_List_Odistinct(c_List_Orev(x0,x1),x1) -> c_List_Odistinct(x0,x1) % 0.14/0.37 % 205:1:2:INP:TopTop: -> =(c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),x0,x1),c_List_Olist_ONil(x1)) % 0.14/0.37 % 206:1:4:INP:TopTopTopTop: -> =(c_List_Olist_Olist__case(x0,x1,c_List_Olist_ONil(x2),x3,x2),x0) % 0.14/0.37 % 207:2:2:INP:TopTop: =(c_List_Orev(x0,x1),c_List_Olist_ONil(x1)) -> =(x0,c_List_Olist_ONil(x1)) % 0.14/0.37 % 208:4:7:INP:TopTopTopTopTopTopTop: =(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),c_Nat_Osize__class_Osize(x2,tc_List_Olist(x3))),c_List_Olist__all2(x4,x5,x6,x1,x3),c_List_Olist__all2(x4,x0,x2,x1,x3) -> c_List_Olist__all2(x4,c_List_Oappend(x0,x5,x1),c_List_Oappend(x2,x6,x3),x1,x3) % 0.14/0.37 % 209:2:3:INP:TopTopTop: c_Lambda_Obeta(x0,x1) -> c_Lambda_Obeta(hAPP(hAPP(c_Lambda_Olift,x0),x2),hAPP(hAPP(c_Lambda_Olift,x1),x2)) % 0.14/0.37 % 210:1:2:INP:TopTop: -> =(c_List_Orotate(x0,c_List_Olist_ONil(x1),x1),c_List_Olist_ONil(x1)) % 0.14/0.37 % 211:1:4:INP:TopTopTopTop: -> =(c_List_Olist__update(c_List_Olist_OCons(x0,x1,x2),c_HOL_Ozero__class_Ozero(tc_nat),x3,x2),c_List_Olist_OCons(x3,x1,x2)) % 0.14/0.37 % 212:1:4:INP:TopTopTopTop: -> =(c_Nat_Osize__class_Osize(c_List_Olist__update(x0,x1,x2,x3),tc_List_Olist(x3)),c_Nat_Osize__class_Osize(x0,tc_List_Olist(x3))) % 0.14/0.37 % 213:1:3:INP:TopTopTop: -> =(c_List_Olist_OCons(x0,x1,x2),c_List_Oappend(c_List_Olist_ONil(x2),c_List_Olist_OCons(x0,x1,x2),x2)) % 0.14/0.37 % 214:1:2:INP:TopTop: -> =(c_List_Olist_OCons(x0,c_List_Olist_ONil(x1),x1),c_List_Orev(c_List_Olist_OCons(x0,c_List_Olist_ONil(x1),x1),x1)) % 0.14/0.37 % 215:2:2:INP:TopTop: hBOOL(hAPP(c_InductTermi_OIT,x0)) -> hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,x0),c_Lambda_OdB_OVar(x1)))) % 0.14/0.37 % 216:3:5:INP:TopTopTopTopTop: =(c_List_Oreplicate(x0,x1,x2),c_List_Oreplicate(x3,x4,x2)) -> =(x1,x4),=(x0,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.14/0.37 % 217:3:6:INP:TopTopTopTopTopTop: c_Type_Otyping(x0,x1,x2),c_Type_Otyping(c_Type_Oshift(x0,x3,x2,tc_Type_Otype),x4,x5) -> c_Type_Otyping(x0,hAPP(hAPP(hAPP(c_Lambda_Osubst,x4),x1),x3),x5) % 0.14/0.37 % 218:3:6:INP:TopTopTopTopTopTop: c_ListOrder_Ostep1(x0,c_List_Oappend(x1,c_List_Olist_OCons(x2,c_List_Olist_ONil(x3),x3),x3),c_List_Oappend(x4,c_List_Olist_OCons(x5,c_List_Olist_ONil(x3),x3),x3),x3) -> =(x1,x4),c_ListOrder_Ostep1(x0,x1,x4,x3) % 0.14/0.37 % 219:1:1:INP:Top: -> =(c_List_Olist_ONil(x0),c_List_Oappend(c_List_Olist_ONil(x0),c_List_Olist_ONil(x0),x0)) % 0.14/0.37 % 220:2:4:INP:TopTopTopTop: hBOOL(hAPP(c_Lattices_Olower__semilattice__class_Oinf(x0,x1,tc_fun(x2,tc_bool)),x3)) -> hBOOL(hAPP(x1,x3)) % 0.14/0.37 % 221:2:4:INP:TopTopTopTop: hBOOL(hAPP(c_Lattices_Olower__semilattice__class_Oinf(x0,x1,tc_fun(x2,tc_bool)),x3)) -> hBOOL(hAPP(x0,x3)) % 0.14/0.37 % 222:3:4:INP:TopTopTopTop: c_List_Olist__all(x0,x1,x2),c_List_Olist__all(x0,x3,x2) -> c_List_Olist__all(x0,c_List_Oappend(x3,x1,x2),x2) % 0.14/0.37 % 223:2:2:INP:TopTop: class_Orderings_Olinorder(x0) -> c_List_Olinorder__class_Osorted(c_List_Olist_OCons(x1,c_List_Olist_ONil(x0),x0),x0) % 0.14/0.37 % 224:1:4:INP:TopTopTopTop: =(hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(x0)),x1),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x2),x3,tc_Lambda_OdB,tc_Lambda_OdB)) -> % 0.14/0.37 % 225:2:3:INP:TopTopTop: c_List_Odistinct(x0,x1) -> c_List_Odistinct(c_List_Otake(x2,x0,x1),x1) % 0.14/0.37 % 226:2:2:INP:TopTop: c_Lambda_Obeta(x0,x1) -> c_Lambda_Obeta(c_Lambda_OdB_OAbs(x0),c_Lambda_OdB_OAbs(x1)) % 0.14/0.37 % 227:1:3:INP:TopTopTop: -> =(c_List_Oappend(c_List_Oreplicate(x0,x1,x2),c_List_Olist_OCons(x1,c_List_Olist_ONil(x2),x2),x2),c_List_Olist_OCons(x1,c_List_Oreplicate(x0,x1,x2),x2)) % 0.14/0.37 % 228:1:2:INP:TopTop: -> c_List_Olistrelp(x0,c_List_Olist_ONil(x1),c_List_Olist_ONil(x1),x1) % 0.14/0.37 % 229:1:1:INP:Top: -> =(c_List_Orev(c_List_Olist_ONil(x0),x0),c_List_Olist_ONil(x0)) % 0.14/0.37 % 230:2:3:INP:TopTopTop: c_List_Odistinct(x0,x1) -> c_List_Odistinct(c_List_OtakeWhile(x2,x0,x1),x1) % 0.14/0.37 % 231:1:3:INP:TopTopTop: -> =(c_List_Orev(c_List_Oappend(x0,x1,x2),x2),c_List_Oappend(c_List_Orev(x1,x2),c_List_Orev(x0,x2),x2)) % 0.14/0.37 % 232:1:6:INP:TopTopTopTopTopTop: -> =(c_List_Ofoldl(x0,x1,c_List_Oappend(x2,x3,x4),x5,x4),c_List_Ofoldl(x0,c_List_Ofoldl(x0,x1,x2,x5,x4),x3,x5,x4)) % 0.14/0.37 % 233:1:3:INP:TopTopTop: =(hAPP(hAPP(c_Lambda_OdB_OApp,x0),x1),c_Lambda_OdB_OVar(x2)) -> % 0.14/0.37 % 234:1:4:INP:TopTopTopTop: -> =(c_List_Ofilter(x0,c_List_Oappend(x1,x2,x3),x3),c_List_Oappend(c_List_Ofilter(x0,x1,x3),c_List_Ofilter(x0,x2,x3),x3)) % 0.14/0.37 % 235:2:4:INP:TopTopTopTop: =(c_List_Olist__update(x0,x1,x2,x3),c_List_Olist_ONil(x3)) -> =(x0,c_List_Olist_ONil(x3)) % 0.14/0.37 % 236:2:5:INP:TopTopTopTopTop: c_List_Olist__all2(x0,x1,c_List_Orev(x2,x3),x4,x3) -> c_List_Olist__all2(x0,c_List_Orev(x1,x4),x2,x4,x3) % 0.14/0.37 % 237:2:5:INP:TopTopTopTopTop: c_List_Olist__all2(x0,c_List_Orev(x1,x2),x3,x2,x4) -> c_List_Olist__all2(x0,x1,c_List_Orev(x3,x4),x2,x4) % 0.14/0.37 % 238:2:2:INP:TopTop: c_List_Olistsp(c_InductTermi_OIT,x0,tc_Lambda_OdB) -> hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x1),x0,tc_Lambda_OdB,tc_Lambda_OdB))) % 0.14/0.37 % 239:2:5:INP:TopTopTopTopTop: hBOOL(hAPP(x0,c_List_Olist_Olist__case(x1,x2,c_List_Olist_OCons(x3,x4,t_b),t_a,t_b))) -> hBOOL(hAPP(x0,hAPP(hAPP(x2,x3),x4))) % 0.14/0.37 % 240:2:5:INP:TopTopTopTopTop: hBOOL(hAPP(x0,c_List_Olist_Olist__case(x1,x2,c_List_Olist_OCons(x3,x4,t_b),t_a,t_b))) -> hBOOL(hAPP(x0,hAPP(hAPP(x2,x3),x4))) % 0.14/0.37 % 241:2:4:INP:TopTopTopTop: -> =(c_List_Ofilter(x0,c_List_Olist_OCons(x1,x2,x3),x3),c_List_Ofilter(x0,x2,x3)),hBOOL(hAPP(x0,x1)) % 0.14/0.37 % 242:3:4:INP:TopTopTopTop: c_List_Olist__all(x0,x1,x2),hBOOL(hAPP(x0,x3)) -> c_List_Olist__all(x0,c_List_Olist_OCons(x3,x1,x2),x2) % 0.14/0.37 % 243:2:5:INP:TopTopTopTopTop: c_ListOrder_Ostep1(x0,x1,x2,x3) -> c_ListOrder_Ostep1(x0,c_List_Olist_OCons(x4,x1,x3),c_List_Olist_OCons(x4,x2,x3),x3) % 0.14/0.37 % 244:3:6:INP:TopTopTopTopTopTop: c_ListOrder_Ostep1(x0,c_List_Olist_OCons(x1,x2,x3),c_List_Olist_OCons(x4,x5,x3),x3) -> c_ListOrder_Ostep1(x0,x2,x5,x3),hBOOL(hAPP(hAPP(x0,x1),x4)) % 0.14/0.37 % 245:1:3:INP:TopTopTop: -> =(c_List_OremoveAll(x0,c_List_Olist_OCons(x0,x1,x2),x2),c_List_OremoveAll(x0,x1,x2)) % 0.14/0.37 % 246:1:3:INP:TopTopTop: =(c_List_Olist_ONil(x0),c_List_Olist_OCons(x1,x2,x0)) -> % 0.14/0.37 % 247:2:6:INP:TopTopTopTopTopTop: hBOOL(hAPP(x0,x1)) -> =(c_List_Omap__filter(x2,x0,c_List_Olist_OCons(x1,x3,x4),x4,x5),c_List_Olist_OCons(hAPP(x2,x1),c_List_Omap__filter(x2,x0,x3,x4,x5),x5)) % 0.14/0.37 % 248:3:6:INP:TopTopTopTopTopTop: c_ListOrder_Ostep1(x0,c_List_Olist_OCons(x1,x2,x3),c_List_Olist_OCons(x4,x5,x3),x3) -> c_ListOrder_Ostep1(x0,x2,x5,x3),=(x5,x2) % 0.14/0.37 % 249:2:4:INP:TopTopTopTop: -> =(c_List_OdropWhile(x0,c_List_Olist_OCons(x1,x2,x3),x3),c_List_Olist_OCons(x1,x2,x3)),hBOOL(hAPP(x0,x1)) % 0.14/0.37 % 250:2:4:INP:TopTopTopTop: hBOOL(hAPP(x0,x1)) -> =(c_List_OdropWhile(x0,c_List_Olist_OCons(x1,x2,x3),x3),c_List_OdropWhile(x0,x2,x3)) % 0.14/0.37 % 251:1:4:INP:TopTopTopTop: -> =(c_Lattices_Olower__semilattice__class_Oinf(x0,c_Lattices_Olower__semilattice__class_Oinf(x1,x2,tc_fun(x3,tc_bool)),tc_fun(x3,tc_bool)),c_Lattices_Olower__semilattice__class_Oinf(x1,c_Lattices_Olower__semilattice__class_Oinf(x0,x2,tc_fun(x3,tc_bool)),tc_fun(x3,tc_bool))) % 0.14/0.37 % 252:2:3:INP:TopTopTop: =(c_List_Olist_ONil(x0),c_List_Oappend(x1,x2,x0)) -> =(x1,c_List_Olist_ONil(x0)) % 0.14/0.37 % 253:2:3:INP:TopTopTop: =(c_List_Olist_ONil(x0),c_List_Oappend(x1,x2,x0)) -> =(x2,c_List_Olist_ONil(x0)) % 0.14/0.37 % 254:2:2:INP:TopTop: =(c_Lambda_OdB_OAbs(x0),c_Lambda_OdB_OAbs(x1)) -> =(x0,x1) % 0.14/0.37 % 255:2:5:INP:TopTopTopTopTop: =(c_List_OdropWhile(x0,x1,x2),c_List_Olist_OCons(x3,x4,x2)) -> =(x1,c_List_Oappend(c_List_OtakeWhile(x0,x1,x2),c_List_Olist_OCons(x3,x4,x2),x2)) % 0.14/0.37 % 256:3:5:INP:TopTopTopTopTop: =(x0,c_List_Oappend(c_List_OtakeWhile(x1,x0,x2),c_List_Olist_OCons(x3,x4,x2),x2)) -> =(c_List_OdropWhile(x1,x0,x2),c_List_Olist_OCons(x3,x4,x2)),hBOOL(hAPP(x1,x3)) % 0.14/0.37 % 257:2:3:INP:TopTopTop: =(c_List_Oappend(x0,x1,x2),c_List_Olist_ONil(x2)) -> =(x0,c_List_Olist_ONil(x2)) % 0.14/0.37 % 258:2:3:INP:TopTopTop: =(c_List_Oappend(x0,x1,x2),c_List_Olist_ONil(x2)) -> =(x1,c_List_Olist_ONil(x2)) % 0.14/0.37 % 259:1:1:INP:Top: -> =(c_Nat_Osize__class_Osize(c_List_Olist_ONil(x0),tc_List_Olist(x0)),c_HOL_Ozero__class_Ozero(tc_nat)) % 0.14/0.37 % 260:2:3:INP:TopTopTop: =(x0,c_List_Otake(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),x2,x1)) -> =(c_List_Oappend(x0,c_List_Odrop(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),x2,x1),x1),x2) % 0.14/0.37 % 261:1:3:INP:TopTopTop: =(c_Lambda_OdB_OVar(x0),hAPP(hAPP(c_Lambda_OdB_OApp,x1),x2)) -> % 0.14/0.37 % 262:2:3:INP:TopTopTop: c_List_Odistinct(x0,x1) -> c_List_Odistinct(c_List_Oremove1(x2,x0,x1),x1) % 0.14/0.37 % 263:2:3:INP:TopTopTop: =(c_Lambda_OdB_OVar(x0),c_List_Ofoldl(c_Lambda_OdB_OApp,x1,x2,tc_Lambda_OdB,tc_Lambda_OdB)) -> =(c_Lambda_OdB_OVar(x0),x1) % 0.14/0.37 % 264:3:7:INP:TopTopTopTopTopTopTop: =(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),c_Nat_Osize__class_Osize(x2,tc_List_Olist(x3))),c_List_Olist__all2(x4,c_List_Oappend(x0,x5,x1),c_List_Oappend(x2,x6,x3),x1,x3) -> c_List_Olist__all2(x4,x0,x2,x1,x3) % 0.14/0.37 % 265:3:7:INP:TopTopTopTopTopTopTop: =(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),c_Nat_Osize__class_Osize(x2,tc_List_Olist(x3))),c_List_Olist__all2(x4,c_List_Oappend(x0,x5,x1),c_List_Oappend(x2,x6,x3),x1,x3) -> c_List_Olist__all2(x4,x5,x6,x1,x3) % 0.14/0.37 % 266:1:4:INP:TopTopTopTop: -> =(c_List_OremoveAll(x0,c_List_Oappend(x1,x2,x3),x3),c_List_Oappend(c_List_OremoveAll(x0,x1,x3),c_List_OremoveAll(x0,x2,x3),x3)) % 0.14/0.37 % 267:2:3:INP:TopTopTop: c_Lambda_Obeta(x0,x1) -> c_Lambda_Obeta(c_List_Ofoldl(c_Lambda_OdB_OApp,x0,x2,tc_Lambda_OdB,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,x1,x2,tc_Lambda_OdB,tc_Lambda_OdB)) % 0.14/0.37 % 268:1:3:INP:TopTopTop: -> =(c_Nat_Osize__class_Osize(c_List_Orotate(x0,x1,x2),tc_List_Olist(x2)),c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2))) % 0.14/0.37 % 269:2:5:INP:TopTopTopTopTop: -> =(c_List_OtakeWhile(x0,c_List_Oappend(x1,c_List_Olist_OCons(x2,x3,x4),x4),x4),c_List_OtakeWhile(x0,x1,x4)),hBOOL(hAPP(x0,x2)) % 0.14/0.37 % 270:1:2:INP:TopTop: -> =(c_List_Olist_ONil(x0),c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),x1,x0)) % 0.14/0.37 % 271:1:2:INP:TopTop: -> c_Lambda_Obeta(hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(x0)),x1),hAPP(hAPP(hAPP(c_Lambda_Osubst,x0),x1),c_HOL_Ozero__class_Ozero(tc_nat))) % 0.14/0.37 % 272:3:5:INP:TopTopTopTopTop: c_Type_Otyping(x0,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x1),x2,tc_Lambda_OdB,tc_Lambda_OdB),x3),c_Type_Otyping(x0,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x1),x2,tc_Lambda_OdB,tc_Lambda_OdB),x4) -> =(x4,x3) % 0.14/0.37 % 273:1:4:INP:TopTopTopTop: -> =(c_List_Oappend(c_List_Oreplicate(x0,x1,x2),c_List_Oreplicate(x3,x1,x2),x2),c_List_Oappend(c_List_Oreplicate(x3,x1,x2),c_List_Oreplicate(x0,x1,x2),x2)) % 0.14/0.37 % 274:2:4:INP:TopTopTopTop: =(hAPP(hAPP(c_Lambda_OdB_OApp,x0),x1),hAPP(hAPP(c_Lambda_OdB_OApp,x2),x3)) -> =(x1,x3) % 0.14/0.37 % 275:2:4:INP:TopTopTopTop: =(hAPP(hAPP(c_Lambda_OdB_OApp,x0),x1),hAPP(hAPP(c_Lambda_OdB_OApp,x2),x3)) -> =(x0,x2) % 0.14/0.37 % 276:2:6:INP:TopTopTopTopTopTop: c_List_Olist__all2(x0,x1,x2,x3,x4) -> c_List_Olist__all2(x0,c_List_Odrop(x5,x1,x3),c_List_Odrop(x5,x2,x4),x3,x4) % 0.14/0.37 % 277:2:4:INP:TopTopTopTop: =(c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(x0),x1,tc_Lambda_OdB,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(x2),x3,tc_Lambda_OdB,tc_Lambda_OdB)) -> =(x1,x3) % 0.14/0.37 % 278:2:4:INP:TopTopTopTop: =(c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(x0),x1,tc_Lambda_OdB,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(x2),x3,tc_Lambda_OdB,tc_Lambda_OdB)) -> =(x0,x2) % 0.14/0.37 % 279:2:3:INP:TopTopTop: =(c_List_Ofoldl(c_Lambda_OdB_OApp,x0,x1,tc_Lambda_OdB,tc_Lambda_OdB),c_Lambda_OdB_OAbs(x2)) -> =(x0,c_Lambda_OdB_OAbs(x2)) % 0.14/0.37 % 280:1:1:INP:Top: -> c_List_Odistinct(c_List_Olist_ONil(x0),x0) % 0.14/0.37 % 281:1:2:INP:TopTop: c_Lambda_Obeta(c_Lambda_OdB_OVar(x0),x1) -> % 0.14/0.37 % 282:2:3:INP:TopTopTop: c_List_Odistinct(x0,x1) -> =(c_List_Oremove1(x2,x0,x1),c_List_OremoveAll(x2,x0,x1)) % 0.14/0.37 % 283:2:4:INP:TopTopTopTop: -> =(c_List_Oremove1(x0,c_List_Ofilter(x1,x2,x3),x3),c_List_Ofilter(x1,x2,x3)),hBOOL(hAPP(x1,x0)) % 0.14/0.37 % 284:2:4:INP:TopTopTopTop: -> =(c_List_Ofilter(x0,c_List_Oreplicate(x1,x2,x3),x3),c_List_Olist_ONil(x3)),hBOOL(hAPP(x0,x2)) % 0.14/0.37 % 285:1:3:INP:TopTopTop: -> =(c_List_Oappend(c_List_OtakeWhile(x0,x1,x2),c_List_OdropWhile(x0,x1,x2),x2),x1) % 0.14/0.37 % 286:2:4:INP:TopTopTopTop: c_List_Olist__all2(x0,c_List_Olist_ONil(x1),x2,x1,x3) -> =(x2,c_List_Olist_ONil(x3)) % 0.14/0.37 % 287:2:4:INP:TopTopTopTop: c_List_Olist__all2(x0,x1,c_List_Olist_ONil(x2),x3,x2) -> =(x1,c_List_Olist_ONil(x3)) % 0.14/0.37 % 288:1:2:INP:TopTop: -> =(c_List_Otake(c_HOL_Ozero__class_Ozero(tc_nat),x0,x1),c_List_Olist_ONil(x1)) % 0.14/0.37 % 289:2:3:INP:TopTopTop: =(c_List_Orev(x0,x1),c_List_Orev(x2,x1)) -> =(x0,x2) % 0.14/0.37 % 290:3:6:INP:TopTopTopTopTopTop: c_ListOrder_Ostep1(x0,c_List_Oappend(x1,c_List_Olist_OCons(x2,c_List_Olist_ONil(x3),x3),x3),c_List_Oappend(x4,c_List_Olist_OCons(x5,c_List_Olist_ONil(x3),x3),x3),x3) -> =(x1,x4),=(x2,x5) % 0.14/0.37 % 291:1:3:INP:TopTopTop: -> =(c_List_Otake(c_HOL_Ozero__class_Ozero(tc_nat),c_List_Olist_OCons(x0,x1,x2),x2),c_List_Olist_ONil(x2)) % 0.14/0.37 % 292:2:3:INP:TopTopTop: c_List_Odistinct(c_List_Orotate(x0,x1,x2),x2) -> c_List_Odistinct(x1,x2) % 0.14/0.37 % 293:2:3:INP:TopTopTop: c_List_Odistinct(x0,x1) -> c_List_Odistinct(c_List_Orotate(x2,x0,x1),x1) % 0.14/0.37 % 294:2:3:INP:TopTopTop: =(c_List_Oreplicate(x0,x1,x2),c_List_Olist_ONil(x2)) -> =(x0,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.14/0.37 % 295:1:7:INP:TopTopTopTopTopTopTop: -> =(c_Fun_Ocomp(x0,c_Fun_Ocomp(x1,x2,x3,x4,x5),x4,x6,x5),c_Fun_Ocomp(c_Fun_Ocomp(x0,x1,x4,x6,x3),x2,x3,x6,x5)) % 0.14/0.37 % 296:1:3:INP:TopTopTop: -> =(c_Nat_Osize__class_Osize(c_List_Oreplicate(x0,x1,x2),tc_List_Olist(x2)),x0) % 0.14/0.37 % 297:2:3:INP:TopTopTop: =(c_List_Olist_ONil(x0),c_List_Oreplicate(x1,x2,x0)) -> =(x1,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.14/0.37 % 298:2:2:INP:TopTop: =(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),c_HOL_Ozero__class_Ozero(tc_nat)) -> =(x0,c_List_Olist_ONil(x1)) % 0.14/0.37 % 299:2:2:INP:TopTop: =(c_List_Olist_ONil(x0),c_List_Orev(x1,x0)) -> =(x1,c_List_Olist_ONil(x0)) % 0.14/0.37 % 300:2:3:INP:TopTopTop: class_Lattices_Olattice(x0) -> =(c_Lattices_Olower__semilattice__class_Oinf(x1,c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0),x0),c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0)) % 0.14/0.37 % 301:2:3:INP:TopTopTop: class_Lattices_Olower__semilattice(x0) -> =(c_Lattices_Olower__semilattice__class_Oinf(x1,c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0),x0),c_Lattices_Olower__semilattice__class_Oinf(x1,x2,x0)) % 0.14/0.37 % 302:1:3:INP:TopTopTop: -> =(c_Lattices_Olower__semilattice__class_Oinf(x0,c_Lattices_Olower__semilattice__class_Oinf(x0,x1,tc_fun(x2,tc_bool)),tc_fun(x2,tc_bool)),c_Lattices_Olower__semilattice__class_Oinf(x0,x1,tc_fun(x2,tc_bool))) % 0.14/0.37 % 303:2:3:INP:TopTopTop: =(c_List_Orotate(x0,x1,x2),c_List_Olist_ONil(x2)) -> =(x1,c_List_Olist_ONil(x2)) % 0.14/0.37 % 304:1:3:INP:TopTopTop: -> =(c_List_OdropWhile(x0,x1,x2),c_List_Odrop(c_Nat_Osize__class_Osize(c_List_OtakeWhile(x0,x1,x2),tc_List_Olist(x2)),x1,x2)) % 0.14/0.37 % 305:1:5:INP:TopTopTopTopTop: -> =(c_List_Olist__update(c_List_Oappend(x0,c_List_Olist_OCons(x1,x2,x3),x3),c_Nat_Osize__class_Osize(x0,tc_List_Olist(x3)),x4,x3),c_List_Oappend(x0,c_List_Olist_OCons(x4,x2,x3),x3)) % 0.14/0.37 % 306:2:3:INP:TopTopTop: =(c_List_Oappend(x0,x1,x2),x0) -> =(x1,c_List_Olist_ONil(x2)) % 0.14/0.37 % 307:2:3:INP:TopTopTop: =(x0,c_List_Oappend(x0,x1,x2)) -> =(x1,c_List_Olist_ONil(x2)) % 0.14/0.37 % 308:2:3:INP:TopTopTop: =(c_List_Oappend(x0,x1,x2),x1) -> =(x0,c_List_Olist_ONil(x2)) % 0.14/0.37 % 309:2:3:INP:TopTopTop: =(x0,c_List_Oappend(x1,x0,x2)) -> =(x1,c_List_Olist_ONil(x2)) % 0.14/0.37 % 310:1:3:INP:TopTopTop: -> =(c_List_Oappend(c_List_Olist_ONil(x0),c_List_Olist_OCons(x1,x2,x0),x0),c_List_Olist_OCons(x1,x2,x0)) % 0.14/0.37 % 311:1:2:INP:TopTop: -> =(c_List_OtakeWhile(x0,c_List_Olist_ONil(x1),x1),c_List_Olist_ONil(x1)) % 0.14/0.37 % 312:2:2:INP:TopTop: class_Lattices_Olower__semilattice(x0) -> =(c_Lattices_Olower__semilattice__class_Oinf(x1,x1,x0),x1) % 0.14/0.37 % 313:1:2:INP:TopTop: -> =(c_Lattices_Olower__semilattice__class_Oinf(x0,x0,tc_fun(x1,tc_bool)),x0) % 0.14/0.37 % 314:4:4:INP:TopTopTopTop: =(c_List_Oappend(c_List_Odrop(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),x2,x1),c_List_Oappend(c_List_Odrop(c_Nat_Osize__class_Osize(x2,tc_List_Olist(x1)),x0,x1),x3,x1),x1),x3),=(c_List_Otake(c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1)),x2,x1),x0),=(x2,c_List_Otake(c_Nat_Osize__class_Osize(x2,tc_List_Olist(x1)),x0,x1)) -> =(c_List_Oappend(x2,c_List_Oappend(c_List_Odrop(c_Nat_Osize__class_Osize(x2,tc_List_Olist(x1)),x0,x1),x3,x1),x1),c_List_Oappend(x0,x3,x1)) % 0.14/0.37 % 315:2:4:INP:TopTopTopTop: =(c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x0),x1,tc_Lambda_OdB,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x2),x3,tc_Lambda_OdB,tc_Lambda_OdB)) -> =(x1,x3) % 0.14/0.37 % 316:2:4:INP:TopTopTopTop: =(c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x0),x1,tc_Lambda_OdB,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(x2),x3,tc_Lambda_OdB,tc_Lambda_OdB)) -> =(x0,x2) % 0.14/0.37 % 317:3:4:INP:TopTopTopTop: c_Lambda_Obeta(x0,x1),c_Type_Otyping(x2,x0,x3) -> c_Type_Otyping(x2,x1,x3) % 0.14/0.37 % 318:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_List_Olinorder__class_Osorted(c_List_Oappend(x1,x2,x0),x0) -> c_List_Olinorder__class_Osorted(x1,x0) % 0.14/0.37 % 319:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_List_Olinorder__class_Osorted(c_List_Oappend(x1,x2,x0),x0) -> c_List_Olinorder__class_Osorted(x2,x0) % 0.14/0.37 % 320:1:3:INP:TopTopTop: =(c_Lambda_OdB_OAbs(x0),hAPP(hAPP(c_Lambda_OdB_OApp,x1),x2)) -> % 0.14/0.37 % 321:2:6:INP:TopTopTopTopTopTop: -> =(c_List_Olist__update(c_List_Olist__update(x0,x1,x2,x3),x4,x5,x3),c_List_Olist__update(c_List_Olist__update(x0,x4,x5,x3),x1,x2,x3)),=(x1,x4) % 0.14/0.37 % 322:1:4:INP:TopTopTopTop: -> =(c_List_Omap__filter(x0,x1,c_List_Olist_ONil(x2),x2,x3),c_List_Olist_ONil(x3)) % 0.14/0.37 % 323:2:2:INP:TopTop: =(c_Lambda_OdB_OVar(x0),c_Lambda_OdB_OVar(x1)) -> =(x0,x1) % 0.14/0.37 % 324:2:3:INP:TopTopTop: c_List_Olist__all(x0,c_List_Orev(x1,x2),x2) -> c_List_Olist__all(x0,x1,x2) % 0.14/0.37 % 325:2:3:INP:TopTopTop: c_List_Olist__all(x0,x1,x2) -> c_List_Olist__all(x0,c_List_Orev(x1,x2),x2) % 0.14/0.37 % 326:1:3:INP:TopTopTop: =(hAPP(hAPP(c_Lambda_OdB_OApp,x0),x1),c_Lambda_OdB_OAbs(x2)) -> % 0.14/0.37 % 327:1:2:INP:TopTop: =(c_Lambda_OdB_OAbs(x0),c_Lambda_OdB_OVar(x1)) -> % 0.14/0.37 % 328:1:4:INP:TopTopTopTop: -> =(c_List_Oappend(c_List_Oreplicate(x0,x1,x2),c_List_Olist_OCons(x1,x3,x2),x2),c_List_Olist_OCons(x1,c_List_Oappend(c_List_Oreplicate(x0,x1,x2),x3,x2),x2)) % 0.14/0.37 % 329:2:9:INP:TopTopTopTopTopTopTopTopTop: =(c_Fun_Ocomp(x0,x1,x2,x3,x4),c_Fun_Ocomp(x5,x6,x7,x3,x4)) -> =(hAPP(x0,hAPP(x1,x8)),hAPP(x5,hAPP(x6,x8))) % 0.14/0.37 % 330:2:11:INP:TopTopTopTopTopTopTopTopTopTopTop: =(hAPP(x0,hAPP(x1,x2)),hAPP(x3,hAPP(x4,x5))) -> =(hAPP(c_Fun_Ocomp(x0,x1,x6,x7,x8),x2),hAPP(c_Fun_Ocomp(x3,x4,x9,x7,x10),x5)) % 0.14/0.37 % 331:1:1:INP:Top: -> =(c_List_Olist_ONil(x0),c_List_Orev(c_List_Olist_ONil(x0),x0)) % 0.14/0.37 % 332:1:2:INP:TopTop: -> =(c_List_OremoveAll(x0,c_List_Olist_ONil(x1),x1),c_List_Olist_ONil(x1)) % 0.14/0.37 % 333:1:2:INP:TopTop: -> =(c_Nat_Osize__class_Osize(c_List_Orev(x0,x1),tc_List_Olist(x1)),c_Nat_Osize__class_Osize(x0,tc_List_Olist(x1))) % 0.14/0.37 % 334:1:3:INP:TopTopTop: -> c_List_Olist__all2(x0,c_List_Olist_ONil(x1),c_List_Olist_ONil(x2),x1,x2) % 0.14/0.37 % 335:3:4:INP:TopTopTopTop: hBOOL(hAPP(x0,x1)),hBOOL(hAPP(x2,x1)) -> hBOOL(hAPP(c_Lattices_Olower__semilattice__class_Oinf(x2,x0,tc_fun(x3,tc_bool)),x1)) % 0.14/0.37 % 336:1:3:INP:TopTopTop: -> =(c_List_Orev(c_List_Ofilter(x0,x1,x2),x2),c_List_Ofilter(x0,c_List_Orev(x1,x2),x2)) % 0.14/0.37 % 337:1:2:INP:TopTop: -> c_List_Olist__all2(c_fequal(x0),x1,x1,x0,x0) % 0.14/0.37 % 338:2:5:INP:TopTopTopTopTop: =(c_List_Oappend(x0,c_List_Olist_OCons(x1,c_List_Olist_ONil(x2),x2),x2),c_List_Oappend(x3,c_List_Olist_OCons(x4,c_List_Olist_ONil(x2),x2),x2)) -> =(x0,x3) % 0.14/0.37 % 339:2:5:INP:TopTopTopTopTop: =(c_List_Oappend(x0,c_List_Olist_OCons(x1,c_List_Olist_ONil(x2),x2),x2),c_List_Oappend(x3,c_List_Olist_OCons(x4,c_List_Olist_ONil(x2),x2),x2)) -> =(x1,x4) % 0.14/0.37 % 340:2:4:INP:TopTopTopTop: c_List_Olist__all(x0,c_List_Oappend(x1,x2,x3),x3) -> c_List_Olist__all(x0,x1,x3) % 0.14/0.37 % 341:2:4:INP:TopTopTopTop: c_List_Olist__all(x0,c_List_Oappend(x1,x2,x3),x3) -> c_List_Olist__all(x0,x2,x3) % 0.14/0.37 % 342:1:1:INP:Top: -> =(c_List_Oappend(c_List_Olist_ONil(x0),c_List_Olist_ONil(x0),x0),c_List_Olist_ONil(x0)) % 0.14/0.37 % 343:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_List_Olinorder__class_Osorted(x1,x0) -> c_List_Olinorder__class_Osorted(c_List_OdropWhile(x2,x1,x0),x0) % 0.14/0.37 % 344:1:5:INP:TopTopTopTopTop: -> =(c_List_Olist__update(c_List_Olist__update(x0,x1,x2,x3),x1,x4,x3),c_List_Olist__update(x0,x1,x4,x3)) % 0.14/0.37 % 345:1:4:INP:TopTopTopTop: -> =(c_List_Oappend(c_List_Oappend(x0,x1,x2),x3,x2),c_List_Oappend(x0,c_List_Oappend(x1,x3,x2),x2)) % 0.14/0.37 % 346:1:4:INP:TopTopTopTop: -> =(c_List_Oappend(x0,c_List_Oappend(x1,x2,x3),x3),c_List_Oappend(c_List_Oappend(x0,x1,x3),x2,x3)) % 0.14/0.37 % 347:1:4:INP:TopTopTopTop: -> =(c_List_Oappend(c_List_Oappend(x0,x1,x2),x3,x2),c_List_Oappend(x0,c_List_Oappend(x1,x3,x2),x2)) % 0.14/0.37 % 348:1:4:INP:TopTopTopTop: -> =(c_List_Oappend(x0,c_List_Oappend(x1,x2,x3),x3),c_List_Oappend(c_List_Oappend(x0,x1,x3),x2,x3)) % 0.14/0.37 % 349:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_List_Olinorder__class_Osorted(x1,x0) -> c_List_Olinorder__class_Osorted(c_List_Oremove1(x2,x1,x0),x0) % 0.14/0.37 % 350:2:5:INP:TopTopTopTopTop: c_Type_Otyping(x0,x1,x2) -> c_Type_Otyping(c_Type_Oshift(x0,x3,x4,tc_Type_Otype),hAPP(hAPP(c_Lambda_Olift,x1),x3),x2) % 0.14/0.37 % 351:2:4:INP:TopTopTopTop: -> =(c_List_Oremove1(x0,c_List_Olist_OCons(x1,x2,x3),x3),c_List_Olist_OCons(x1,c_List_Oremove1(x0,x2,x3),x3)),=(x0,x1) % 0.14/0.37 % 352:3:6:INP:TopTopTopTopTopTop: c_List_Olistrelp(x0,x1,x2,x3),hBOOL(hAPP(hAPP(x0,x4),x5)) -> c_List_Olistrelp(x0,c_List_Olist_OCons(x4,x1,x3),c_List_Olist_OCons(x5,x2,x3),x3) % 0.14/0.37 % 353:3:4:INP:TopTopTopTop: c_List_Olist__ex(x0,c_List_Olist_OCons(x1,x2,x3),x3) -> c_List_Olist__ex(x0,x2,x3),hBOOL(hAPP(x0,x1)) % 0.14/0.37 % 354:2:4:INP:TopTopTopTop: c_List_Olist__ex(x0,x1,x2) -> c_List_Olist__ex(x0,c_List_Olist_OCons(x3,x1,x2),x2) % 0.14/0.37 % 355:3:7:INP:TopTopTopTopTopTopTop: c_List_Olist__all2(x0,x1,x2,x3,x4),hBOOL(hAPP(hAPP(x0,x5),x6)) -> c_List_Olist__all2(x0,c_List_Olist_OCons(x5,x1,x3),c_List_Olist_OCons(x6,x2,x4),x3,x4) % 0.14/0.37 % 356:3:7:INP:TopTopTopTopTopTopTop: c_List_Olist__all2(x0,x1,x2,x3,x4),hBOOL(hAPP(hAPP(x0,x5),x6)) -> c_List_Olist__all2(x0,c_List_Olist_OCons(x5,x1,x3),c_List_Olist_OCons(x6,x2,x4),x3,x4) % 0.14/0.37 % 357:3:7:INP:TopTopTopTopTopTopTop: c_List_Olist__all2(x0,x1,x2,x3,x4),hBOOL(hAPP(hAPP(x0,x5),x6)) -> c_List_Olist__all2(x0,c_List_Olist_OCons(x5,x1,x3),c_List_Olist_OCons(x6,x2,x4),x3,x4) % 0.14/0.37 % 358:2:4:INP:TopTopTopTop: -> =(c_List_OremoveAll(x0,c_List_Olist_OCons(x1,x2,x3),x3),c_List_Olist_OCons(x1,c_List_OremoveAll(x0,x2,x3),x3)),=(x0,x1) % 0.14/0.37 % 359:2:5:INP:TopTopTopTopTop: =(c_List_OdropWhile(x0,x1,x2),c_List_Olist_OCons(x3,x4,x2)),hBOOL(hAPP(x0,x3)) -> % 0.14/0.37 % 360:2:4:INP:TopTopTopTop: hBOOL(hAPP(x0,x1)) -> c_List_Olist__ex(x0,c_List_Olist_OCons(x1,x2,x3),x3) % 0.14/0.37 % 361:2:6:INP:TopTopTopTopTopTop: -> =(c_List_Omap__filter(x0,x1,c_List_Olist_OCons(x2,x3,x4),x4,x5),c_List_Omap__filter(x0,x1,x3,x4,x5)),hBOOL(hAPP(x1,x2)) % 0.14/0.37 % 362:1:3:INP:TopTopTop: -> c_List_OListMem(x0,c_List_Olist_OCons(x0,x1,x2),x2) % 0.14/0.37 % 363:2:7:INP:TopTopTopTopTopTopTop: c_List_Olist__all2(x0,c_List_Olist_OCons(x1,x2,x3),c_List_Olist_OCons(x4,x5,x6),x3,x6) -> c_List_Olist__all2(x0,x2,x5,x3,x6) % 0.14/0.37 % 364:2:5:INP:TopTopTopTopTop: =(c_List_Ofilter(x0,x1,x2),c_List_Olist_OCons(x3,x4,x2)) -> hBOOL(hAPP(x0,x3)) % 0.14/0.37 % 365:2:5:INP:TopTopTopTopTop: hBOOL(hAPP(hAPP(x0,x1),x2)) -> c_ListOrder_Ostep1(x0,c_List_Olist_OCons(x1,x3,x4),c_List_Olist_OCons(x2,x3,x4),x4) % 0.14/0.37 % 366:3:6:INP:TopTopTopTopTopTop: c_ListOrder_Ostep1(x0,c_List_Olist_OCons(x1,x2,x3),c_List_Olist_OCons(x4,x5,x3),x3) -> =(x4,x1),=(x5,x2) % 0.14/0.37 % 367:2:4:INP:TopTopTopTop: hBOOL(hAPP(x0,x1)) -> =(c_List_Ofilter(x0,c_List_Olist_OCons(x1,x2,x3),x3),c_List_Olist_OCons(x1,c_List_Ofilter(x0,x2,x3),x3)) % 0.14/0.37 % 368:2:5:INP:TopTopTopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Ofilter(x3,x4,x2)) -> hBOOL(hAPP(x3,x0)) % 0.14/0.37 % 369:1:6:INP:TopTopTopTopTopTop: -> =(c_List_Ofoldl(x0,x1,c_List_Olist_OCons(x2,x3,x4),x5,x4),c_List_Ofoldl(x0,hAPP(hAPP(x0,x1),x2),x3,x5,x4)) % 0.14/0.37 % 370:3:4:INP:TopTopTopTop: class_Orderings_Olinorder(x0),c_List_Olinorder__class_Osorted(c_List_Olist_OCons(x1,c_List_Olist_OCons(x2,x3,x0),x0),x0) -> c_List_Olinorder__class_Osorted(c_List_Olist_OCons(x2,x3,x0),x0) % 0.14/0.37 % 371:1:4:INP:TopTopTopTop: -> =(c_List_Oappend(c_List_Olist_OCons(x0,x1,x2),x3,x2),c_List_Olist_OCons(x0,c_List_Oappend(x1,x3,x2),x2)) % 0.14/0.37 % 372:1:4:INP:TopTopTopTop: -> =(c_List_Oappend(c_List_Olist_OCons(x0,x1,x2),x3,x2),c_List_Olist_OCons(x0,c_List_Oappend(x1,x3,x2),x2)) % 0.14/0.37 % 373:1:6:INP:TopTopTopTopTopTop: -> =(c_List_Olist_Olist__case(x0,x1,c_List_Olist_OCons(x2,x3,x4),x5,x4),hAPP(hAPP(x1,x2),x3)) % 0.14/0.37 % 374:1:3:INP:TopTopTop: -> =(c_List_Oremove1(x0,c_List_Olist_OCons(x0,x1,x2),x2),x1) % 0.14/0.37 % 375:2:7:INP:TopTopTopTopTopTopTop: c_List_Olist__all2(x0,c_List_Olist_OCons(x1,x2,x3),c_List_Olist_OCons(x4,x5,x6),x3,x6) -> hBOOL(hAPP(hAPP(x0,x1),x4)) % 0.14/0.37 % 376:1:4:INP:TopTopTopTop: -> =(c_List_Olist_OCons(x0,c_List_Oappend(x1,x2,x3),x3),c_List_Oappend(c_List_Olist_OCons(x0,x1,x3),x2,x3)) % 0.14/0.37 % 377:1:4:INP:TopTopTopTop: -> =(c_List_Olist_OCons(x0,c_List_Oappend(x1,x2,x3),x3),c_List_Oappend(c_List_Olist_OCons(x0,x1,x3),x2,x3)) % 0.14/0.37 % 378:1:3:INP:TopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Olist_ONil(x2)) -> % 0.14/0.37 % 379:1:3:INP:TopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Olist_ONil(x2)) -> % 0.14/0.37 % 380:3:6:INP:TopTopTopTopTopTop: c_ListOrder_Ostep1(x0,c_List_Olist_OCons(x1,x2,x3),c_List_Olist_OCons(x4,x5,x3),x3) -> =(x4,x1),hBOOL(hAPP(hAPP(x0,x1),x4)) % 0.14/0.37 % 381:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_List_Olinorder__class_Osorted(c_List_Olist_OCons(x1,x2,x0),x0) -> c_List_Olinorder__class_Osorted(x2,x0) % 0.14/0.37 % 382:2:4:INP:TopTopTopTop: hBOOL(hAPP(x0,x1)) -> =(c_List_OtakeWhile(x0,c_List_Olist_OCons(x1,x2,x3),x3),c_List_Olist_OCons(x1,c_List_OtakeWhile(x0,x2,x3),x3)) % 0.14/0.37 % 383:2:4:INP:TopTopTopTop: c_List_Olist__all(x0,c_List_Olist_OCons(x1,x2,x3),x3) -> c_List_Olist__all(x0,x2,x3) % 0.14/0.37 % 384:2:4:INP:TopTopTopTop: c_List_Olist__all(x0,c_List_Olist_OCons(x1,x2,x3),x3) -> hBOOL(hAPP(x0,x1)) % 0.14/0.37 % 385:2:4:INP:TopTopTopTop: c_List_OListMem(x0,x1,x2) -> c_List_OListMem(x0,c_List_Olist_OCons(x3,x1,x2),x2) % 0.14/0.37 % 386:2:3:INP:TopTopTop: c_List_Odistinct(c_List_Olist_OCons(x0,x1,x2),x2) -> c_List_Odistinct(x1,x2) % 0.14/0.37 % 387:2:6:INP:TopTopTopTopTopTop: =(c_List_Omap(x0,x1,x2,x3),c_List_Olist_OCons(x4,x5,x3)) -> =(x1,c_List_Olist_OCons(c_List_Osko__List__Xmap__eq__Cons__conv__1__1(x0,x1,x4,x5,x2,x3),c_List_Osko__List__Xmap__eq__Cons__conv__1__2(x0,x1,x4,x5,x2,x3),x2)) % 0.14/0.37 % 388:2:6:INP:TopTopTopTopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Omap(x3,x4,x5,x2)) -> =(x4,c_List_Olist_OCons(c_List_Osko__List__XCons__eq__map__conv__1__1(x3,x0,x1,x4,x5,x2),c_List_Osko__List__XCons__eq__map__conv__1__2(x3,x0,x1,x4,x5,x2),x5)) % 0.14/0.37 % 389:2:6:INP:TopTopTopTopTopTop: =(c_List_Omap(x0,x1,x2,x3),c_List_Olist_OCons(x4,x5,x3)) -> =(x1,c_List_Olist_OCons(c_List_Osko__List__Xmap__eq__Cons__D__1__1(x0,x1,x4,x5,x2,x3),c_List_Osko__List__Xmap__eq__Cons__D__1__2(x0,x1,x4,x5,x2,x3),x2)) % 0.14/0.37 % 390:2:6:INP:TopTopTopTopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Omap(x3,x4,x5,x2)) -> =(x4,c_List_Olist_OCons(c_List_Osko__List__XCons__eq__map__D__1__1(x3,x0,x1,x4,x5,x2),c_List_Osko__List__XCons__eq__map__D__1__2(x3,x0,x1,x4,x5,x2),x5)) % 0.14/0.37 % 391:1:3:INP:TopTopTop: -> =(hAPP(hAPP(c_Lambda_Olift,c_List_Ofoldl(c_Lambda_OdB_OApp,x0,x1,tc_Lambda_OdB,tc_Lambda_OdB)),x2),c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_Olift,x0),x2),c_List_Omap(c_COMBC(c_Lambda_Olift,x2,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),x1,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)) % 0.14/0.37 % 392:2:5:INP:TopTopTopTopTop: c_Type_Otypings(x0,x1,x2) -> c_Type_Otypings(c_Type_Oshift(x0,x3,x4,tc_Type_Otype),c_List_Omap(c_COMBC(c_Lambda_Olift,x3,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),x1,tc_Lambda_OdB,tc_Lambda_OdB),x2) % 0.14/0.37 % 393:2:4:INP:TopTopTopTop: =(c_List_Omap(x0,x1,x2,x3),c_List_Olist_ONil(x3)) -> =(x1,c_List_Olist_ONil(x2)) % 0.14/0.37 % 394:1:5:INP:TopTopTopTopTop: -> =(c_List_Odrop(x0,c_List_Omap(x1,x2,x3,x4),x4),c_List_Omap(x1,c_List_Odrop(x0,x2,x3),x3,x4)) % 0.14/0.37 % 395:2:3:INP:TopTopTop: =(hAPP(x0,c_List_Osko__List__Xmap__idI__1__1(x0,x1,x2)),c_List_Osko__List__Xmap__idI__1__1(x0,x1,x2)) -> =(c_List_Omap(x0,x1,x2,x2),x1) % 0.14/0.37 % 396:2:4:INP:TopTopTopTop: c_List_Odistinct(c_List_Omap(x0,x1,x2,x3),x3) -> c_List_Odistinct(x1,x2) % 0.14/0.37 % 397:1:5:INP:TopTopTopTopTop: -> =(c_List_Omap(x0,c_List_Oappend(x1,x2,x3),x3,x4),c_List_Oappend(c_List_Omap(x0,x1,x3,x4),c_List_Omap(x0,x2,x3,x4),x4)) % 0.14/0.37 % 398:2:5:INP:TopTopTopTopTop: =(c_List_Omap(x0,x1,x2,x3),c_List_Omap(x0,x4,x2,x3)) -> =(c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2)),c_Nat_Osize__class_Osize(x4,tc_List_Olist(x2))) % 0.14/0.37 % 399:2:4:INP:TopTopTopTop: =(c_List_Olist_ONil(x0),c_List_Omap(x1,x2,x3,x0)) -> =(x2,c_List_Olist_ONil(x3)) % 0.14/0.37 % 400:1:5:INP:TopTopTopTopTop: -> =(c_List_Omap(x0,c_List_Oreplicate(x1,x2,x3),x3,x4),c_List_Oreplicate(x1,hAPP(x0,x2),x4)) % 0.14/0.37 % 401:1:4:INP:TopTopTopTop: -> =(c_Nat_Osize__class_Osize(c_List_Omap(x0,x1,x2,x3),tc_List_Olist(x3)),c_Nat_Osize__class_Osize(x1,tc_List_Olist(x2))) % 0.14/0.37 % 402:1:5:INP:TopTopTopTopTop: -> =(c_List_Orotate(x0,c_List_Omap(x1,x2,x3,x4),x4),c_List_Omap(x1,c_List_Orotate(x0,x2,x3),x3,x4)) % 0.14/0.37 % 403:1:4:INP:TopTopTopTop: -> =(c_List_Orev(c_List_Omap(x0,x1,x2,x3),x3),c_List_Omap(x0,c_List_Orev(x1,x2),x2,x3)) % 0.14/0.37 % 404:2:5:INP:TopTopTopTopTop: =(hAPP(x0,c_List_Osko__List__Xmap__ext__1__1(x0,x1,x2,x3,x4)),hAPP(x1,c_List_Osko__List__Xmap__ext__1__1(x0,x1,x2,x3,x4))) -> =(c_List_Omap(x0,x2,x3,x4),c_List_Omap(x1,x2,x3,x4)) % 0.14/0.37 % 405:1:5:INP:TopTopTopTopTop: -> =(c_List_Otake(x0,c_List_Omap(x1,x2,x3,x4),x4),c_List_Omap(x1,c_List_Otake(x0,x2,x3),x3,x4)) % 0.14/0.37 % 406:1:3:INP:TopTopTop: -> =(c_List_Omap(x0,c_List_Olist_ONil(x1),x1,x2),c_List_Olist_ONil(x2)) % 0.14/0.37 % 407:1:6:INP:TopTopTopTopTopTop: -> =(c_List_Omap(x0,c_List_Omap(x1,x2,x3,x4),x4,x5),c_List_Omap(c_Fun_Ocomp(x0,x1,x4,x5,x3),x2,x3,x5)) % 0.14/0.37 % 408:2:5:INP:TopTopTopTopTop: =(hAPP(x0,c_List_Osko__List__Xmap__cong__1__1(x0,x1,x2,x3,x4)),hAPP(x1,c_List_Osko__List__Xmap__cong__1__1(x0,x1,x2,x3,x4))) -> =(c_List_Omap(x0,x2,x3,x4),c_List_Omap(x1,x2,x3,x4)) % 0.14/0.37 % 409:2:5:INP:TopTopTopTopTop: =(hAPP(x0,c_List_Osko__List__Xmap__eq__conv__1__1(x0,x1,x2,x3,x4)),hAPP(x1,c_List_Osko__List__Xmap__eq__conv__1__1(x0,x1,x2,x3,x4))) -> =(c_List_Omap(x0,x2,x3,x4),c_List_Omap(x1,x2,x3,x4)) % 0.14/0.37 % 410:1:6:INP:TopTopTopTopTopTop: -> =(c_List_Omap(x0,c_List_Olist__update(x1,x2,x3,x4),x4,x5),c_List_Olist__update(c_List_Omap(x0,x1,x4,x5),x2,hAPP(x0,x3),x5)) % 0.14/0.37 % 411:1:3:INP:TopTopTop: -> =(c_List_Olist_ONil(x0),c_List_Omap(x1,c_List_Olist_ONil(x2),x2,x0)) % 0.14/0.37 % 412:1:4:INP:TopTopTopTop: -> =(hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(c_Lambda_OdB_OApp,x0),x1)),x2),x3),hAPP(hAPP(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,x0),x2),x3)),hAPP(hAPP(hAPP(c_Lambda_Osubst,x1),x2),x3))) % 0.14/0.37 % 413:1:2:INP:TopTop: -> =(hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(x0)),x1),x0),x1) % 0.14/0.37 % 414:2:4:INP:TopTopTopTop: c_Lambda_Obeta(x0,x1) -> c_Lambda_Obeta(hAPP(hAPP(hAPP(c_Lambda_Osubst,x0),x2),x3),hAPP(hAPP(hAPP(c_Lambda_Osubst,x1),x2),x3)) % 0.14/0.37 % 415:1:3:INP:TopTopTop: -> =(hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(c_Lambda_Olift,x0),x1)),x2),x1),x0) % 0.14/0.37 % 416:2:2:INP:TopTop: hBOOL(hAPP(c_InductTermi_OIT,x0)) -> hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_Olift,x0),x1))) % 0.14/0.37 % 417:1:1:INP:Top: -> hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OVar(x0))) % 0.14/0.37 % 418:1:0:INP:: -> hBOOL(hAPP(c_InductTermi_OIT,v_ua______)) % 0.14/0.37 % 419:2:1:INP:Top: hBOOL(hAPP(c_InductTermi_OIT,x0)) -> hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OAbs(x0))) % 0.14/0.37 % 420:3:4:INP:TopTopTopTop: c_List_Olistsp(x0,x1,x2),c_List_Olistsp(x0,x3,x2) -> c_List_Olistsp(x0,c_List_Oappend(x3,x1,x2),x2) % 0.14/0.37 % 421:2:3:INP:TopTopTop: hBOOL(hAPP(x0,c_List_Osko__List__Xin__listsp__conv__set__1__1(x0,x1,x2))) -> c_List_Olistsp(x0,x1,x2) % 0.14/0.37 % 422:3:4:INP:TopTopTopTop: c_List_Olistsp(x0,x1,x2),c_List_Olistsp(x3,x1,x2) -> c_List_Olistsp(c_Lattices_Olower__semilattice__class_Oinf(x3,x0,tc_fun(x2,tc_bool)),x1,x2) % 0.14/0.37 % 423:1:2:INP:TopTop: -> c_List_Olistsp(x0,c_List_Olist_ONil(x1),x1) % 0.14/0.37 % 424:2:4:INP:TopTopTopTop: c_List_Olistsp(x0,c_List_Oappend(x1,x2,x3),x3) -> c_List_Olistsp(x0,x2,x3) % 0.14/0.37 % 425:2:4:INP:TopTopTopTop: c_List_Olistsp(x0,c_List_Oappend(x1,x2,x3),x3) -> c_List_Olistsp(x0,x1,x3) % 0.14/0.37 % 426:4:4:INP:TopTopTopTop: c_Type_Otyping(x0,x1,v_T____),hBOOL(hAPP(c_InductTermi_OIT,x1)),c_Type_Otyping(c_Type_Oshift(x0,x2,v_T____,tc_Type_Otype),v_a____,x3) -> hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),x1),x2))) % 0.14/0.37 % 427:4:4:INP:TopTopTopTop: c_Type_Otyping(x0,x1,v_T____),hBOOL(hAPP(c_InductTermi_OIT,x1)),c_Type_Otyping(c_Type_Oshift(x0,x2,v_T____,tc_Type_Otype),v_a____,x3) -> hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),x1),x2))) % 0.14/0.37 % 428:1:0:INP:: =(v_i____,v_n____) -> % 0.14/0.37 % 429:3:6:INP:TopTopTopTopTopTop: c_Type_Otypings(c_Type_Oshift(x0,x1,x2,tc_Type_Otype),x3,x4),c_Type_Otyping(x0,x5,x2) -> c_Type_Otypings(x0,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,x5,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),x1,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),x3,tc_Lambda_OdB,tc_Lambda_OdB),x4) % 0.14/0.37 % 430:2:6:INP:TopTopTopTopTopTop: =(c_List_Omap(x0,x1,x2,x3),c_List_Olist_OCons(x4,x5,x3)) -> =(c_List_Omap(x0,c_List_Osko__List__Xmap__eq__Cons__D__1__2(x0,x1,x4,x5,x2,x3),x2,x3),x5) % 0.14/0.37 % 431:2:6:INP:TopTopTopTopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Omap(x3,x4,x5,x2)) -> =(x1,c_List_Omap(x3,c_List_Osko__List__XCons__eq__map__conv__1__2(x3,x0,x1,x4,x5,x2),x5,x2)) % 0.14/0.37 % 432:2:6:INP:TopTopTopTopTopTop: =(c_List_Omap(x0,x1,x2,x3),c_List_Olist_OCons(x4,x5,x3)) -> =(hAPP(x0,c_List_Osko__List__Xmap__eq__Cons__D__1__1(x0,x1,x4,x5,x2,x3)),x4) % 0.14/0.37 % 433:2:6:INP:TopTopTopTopTopTop: =(c_List_Omap(x0,x1,x2,x3),c_List_Olist_OCons(x4,x5,x3)) -> =(hAPP(x0,c_List_Osko__List__Xmap__eq__Cons__conv__1__1(x0,x1,x4,x5,x2,x3)),x4) % 0.14/0.37 % 434:2:6:INP:TopTopTopTopTopTop: =(c_List_Omap(x0,x1,x2,x3),c_List_Olist_OCons(x4,x5,x3)) -> =(c_List_Omap(x0,c_List_Osko__List__Xmap__eq__Cons__conv__1__2(x0,x1,x4,x5,x2,x3),x2,x3),x5) % 0.14/0.37 % 435:2:6:INP:TopTopTopTopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Omap(x3,x4,x5,x2)) -> =(x0,hAPP(x3,c_List_Osko__List__XCons__eq__map__conv__1__1(x3,x0,x1,x4,x5,x2))) % 0.14/0.37 % 436:2:6:INP:TopTopTopTopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Omap(x3,x4,x5,x2)) -> =(x0,hAPP(x3,c_List_Osko__List__XCons__eq__map__D__1__1(x3,x0,x1,x4,x5,x2))) % 0.14/0.37 % 437:2:6:INP:TopTopTopTopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Omap(x3,x4,x5,x2)) -> =(x1,c_List_Omap(x3,c_List_Osko__List__XCons__eq__map__D__1__2(x3,x0,x1,x4,x5,x2),x5,x2)) % 0.14/0.37 % 438:2:3:INP:TopTopTop: hBOOL(hAPP(c_InductTermi_OIT,x0)) -> hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,x0),c_Lambda_OdB_OVar(x1)),x2))) % 0.14/0.37 % 439:2:1:INP:Top: c_List_Olistsp(c_InductTermi_OIT,x0,tc_Lambda_OdB) -> c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_Lambda_Olift,c_HOL_Ozero__class_Ozero(tc_nat),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),x0,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB) % 0.14/0.37 % 440:1:4:INP:TopTopTopTop: -> =(hAPP(hAPP(hAPP(c_Lambda_Osubst,c_List_Ofoldl(c_Lambda_OdB_OApp,x0,x1,tc_Lambda_OdB,tc_Lambda_OdB)),x2),x3),c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,x0),x2),x3),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,x2,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),x3,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),x1,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)) % 0.14/0.37 % 441:2:5:INP:TopTopTopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Olist_OCons(x3,x4,x2)) -> =(x1,x4) % 0.14/0.37 % 442:2:5:INP:TopTopTopTopTop: =(c_List_Olist_OCons(x0,x1,x2),c_List_Olist_OCons(x3,x4,x2)) -> =(x0,x3) % 0.14/0.37 % 443:1:6:INP:TopTopTopTopTopTop: -> =(hAPP(c_COMBC(x0,x1,x2,x3,x4),x5),hAPP(hAPP(x0,x5),x1)) % 0.14/0.37 % 444:1:0:INP:: -> c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB) % 0.14/0.37 % 445:1:5:INP:TopTopTopTopTop: -> =(c_List_Omap(x0,c_List_Olist_OCons(x1,x2,x3),x3,x4),c_List_Olist_OCons(hAPP(x0,x1),c_List_Omap(x0,x2,x3,x4),x4)) % 0.14/0.37 % 446:1:5:INP:TopTopTopTopTop: -> =(c_List_Olist_OCons(hAPP(x0,x1),c_List_Omap(x0,x2,x3,x4),x4),c_List_Omap(x0,c_List_Olist_OCons(x1,x2,x3),x3,x4)) % 0.14/0.37 % 447:1:5:INP:TopTopTopTopTop: -> =(c_List_Omap(x0,c_List_Olist_OCons(x1,x2,x3),x3,x4),c_List_Olist_OCons(hAPP(x0,x1),c_List_Omap(x0,x2,x3,x4),x4)) % 0.14/0.37 % 448:1:0:INP:: -> hBOOL(hAPP(c_InductTermi_OIT,v_u____)) % 0.14/0.37 % 449:1:3:INP:TopTopTop: =(c_List_Olist_OCons(x0,x1,x2),x1) -> % 0.14/0.37 % 450:1:3:INP:TopTopTop: =(x0,c_List_Olist_OCons(x1,x0,x2)) -> % 0.14/0.37 % 451:1:0:INP:: -> c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_OCons(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_a____),v_u____),v_i____),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB) % 0.14/0.37 % 452:1:0:INP:: c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,v_u____,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_i____,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB) -> % 0.14/0.37 % 453:2:2:INP:TopTop: class_Lattices_Olattice(x0) -> class_Lattices_Olower__semilattice(tc_fun(x1,x0)) % 0.14/0.37 % 454:2:2:INP:TopTop: class_Orderings_Opreorder(x0) -> class_Orderings_Opreorder(tc_fun(x1,x0)) % 0.14/0.37 % 455:2:2:INP:TopTop: class_Lattices_Olattice(x0) -> class_Lattices_Olattice(tc_fun(x1,x0)) % 0.14/0.37 % 456:2:2:INP:TopTop: class_Orderings_Oorder(x0) -> class_Orderings_Oorder(tc_fun(x1,x0)) % 0.14/0.37 % 457:1:0:INP:: -> class_Lattices_Olower__semilattice(tc_nat) % 0.14/0.37 % 458:1:0:INP:: -> class_Divides_Osemiring__div(tc_nat) % 0.14/0.37 % 459:1:0:INP:: -> class_Orderings_Opreorder(tc_nat) % 0.14/0.37 % 460:1:0:INP:: -> class_Orderings_Olinorder(tc_nat) % 0.14/0.37 % 461:1:0:INP:: -> class_Lattices_Olattice(tc_nat) % 0.14/0.37 % 462:1:0:INP:: -> class_Orderings_Oorder(tc_nat) % 0.14/0.37 % 463:1:0:INP:: -> class_Lattices_Olower__semilattice(tc_bool) % 0.14/0.37 % 464:1:0:INP:: -> class_Orderings_Opreorder(tc_bool) % 0.14/0.37 % 465:1:0:INP:: -> class_Lattices_Olattice(tc_bool) % 0.14/0.37 % 466:1:0:INP:: -> class_Orderings_Oorder(tc_bool) % 0.14/0.37 % 467:1:0:INP:: -> class_OrderedGroup_Opordered__ab__group__add(tc_Int_Oint) % 0.14/0.37 % 468:1:0:INP:: -> class_Lattices_Olower__semilattice(tc_Int_Oint) % 0.14/0.37 % 469:1:0:INP:: -> class_OrderedGroup_Oab__group__add(tc_Int_Oint) % 0.14/0.37 % 470:1:0:INP:: -> class_OrderedGroup_Ogroup__add(tc_Int_Oint) % 0.14/0.37 % 471:1:0:INP:: -> class_Divides_Osemiring__div(tc_Int_Oint) % 0.14/0.37 % 472:1:0:INP:: -> class_Ring__and__Field_Oidom(tc_Int_Oint) % 0.14/0.37 % 473:1:0:INP:: -> class_Orderings_Opreorder(tc_Int_Oint) % 0.14/0.37 % 474:1:0:INP:: -> class_Orderings_Olinorder(tc_Int_Oint) % 0.14/0.37 % 475:1:0:INP:: -> class_Lattices_Olattice(tc_Int_Oint) % 0.14/0.37 % 476:1:0:INP:: -> class_Divides_Oring__div(tc_Int_Oint) % 0.14/0.37 % 477:1:0:INP:: -> class_Orderings_Oorder(tc_Int_Oint) % 0.14/0.37 % 478:1:0:INP:: -> class_Int_Oring__char__0(tc_Int_Oint) % 0.14/0.37 % 479:1:0:INP:: -> class_Int_Onumber__ring(tc_Int_Oint) % 0.14/0.37 % 480:1:6:INP:TopTopTopTopTopTop: -> =(hAPP(c_COMBC(x0,x1,x2,x3,x4),x5),hAPP(hAPP(x0,x5),x1)) % 0.14/0.37 % 481:1:6:INP:TopTopTopTopTopTop: -> =(c_COMBB(x0,x1,x2,x3,x4,x5),hAPP(x0,hAPP(x1,x2))) % 0.14/0.37 % 482:1:2:INP:TopTop: -> hBOOL(hAPP(hAPP(c_fequal(x0),x1),x1)) % 0.14/0.37 % 483:2:3:INP:TopTopTop: hBOOL(hAPP(hAPP(c_fequal(x0),x1),x2)) -> =(x1,x2) % 0.14/0.37 % 0.14/0.37 % Predicates: = c_lessequals c_Type_Otyping class_Orderings_Olinorder c_List_Olinorder__class_Osorted class_OrderedGroup_Opordered__ab__group__add class_Orderings_Opreorder class_Orderings_Oorder hBOOL class_Lattices_Olower__semilattice class_Lattices_Olattice class_Divides_Oring__div class_Ring__and__Field_Oidom class_Int_Onumber__ring class_OrderedGroup_Ogroup__add class_OrderedGroup_Oab__group__add class_Divides_Osemiring__div class_Int_Oring__char__0 c_List_Odistinct c_List_Olist__all2 c_ListOrder_Ostep1 c_Type_Otypings c_Lambda_Obeta c_List_Olist__all c_List_Olist__ex c_List_Olistrelp c_List_Olistsp c_List_OListMem % 0.14/0.37 % Fol Constants: tc_nat c_Lambda_OdB_OApp c_Lambda_Olift c_InductTermi_OIT tc_Lambda_OdB c_Lambda_Osubst tc_bool v_T____ tc_Type_Otype v_ea______ v_ua______ v_e____ v_u____ t_b t_a v_a____ v_n____ v_i____ v_as____ tc_Int_Oint % 0.14/0.37 % Fol Functions: c_List_Oreplicate c_List_Odrop c_HOL_Ominus__class_Ominus c_List_Orotate tc_List_Olist c_Nat_Osize__class_Osize c_Divides_Odiv__class_Omod c_List_Otake c_List_OdropWhile c_List_OtakeWhile c_List_Olist__update hAPP c_Type_Otype_OFun c_List_Olist_OCons c_List_Ofilter c_List_Orev c_HOL_Ozero__class_Ozero c_Lattices_Olower__semilattice__class_Oinf c_Int_Onumber__class_Onumber__of c_List_Olist_ONil c_List_Oappend c_List_Omap__filter c_List_Omap c_Lambda_OdB_OVar c_Fun_Ocomp c_Lambda_OdB_OAbs c_List_Ofoldl c_Type_Oshift tc_fun c_Type_Osko__Type__Xvar__app__types__1__1 c_Type_Osko__Type__Xvar__app__typesE__1__1 c_Type_Osko__Type__Xlist__app__typeE__1__1 c_Type_Osko__Type__Xlist__app__typeD__1__1 c_ListBeta_Osko__ListBeta__Xhead__Var__reduction__1__1 c_List_Olist_Olist__case c_List_OremoveAll c_fequal c_List_Oremove1 c_List_Osko__List__Xmap__eq__Cons__conv__1__1 c_List_Osko__List__Xmap__eq__Cons__conv__1__2 c_List_Osko__List__XCons__eq__map__conv__1__1 c_List_Osko__List__XCons__eq__map__conv__1__2 c_List_Osko__List__Xmap__eq__Cons__D__1__1 c_List_Osko__List__Xmap__eq__Cons__D__1__2 c_List_Osko__List__XCons__eq__map__D__1__1 c_List_Osko__List__XCons__eq__map__D__1__2 c_COMBC c_List_Osko__List__Xmap__idI__1__1 c_List_Osko__List__Xmap__ext__1__1 c_List_Osko__List__Xmap__cong__1__1 c_List_Osko__List__Xmap__eq__conv__1__1 c_List_Osko__List__Xin__listsp__conv__set__1__1 c_COMBB % 0.14/0.37 % Problem Properties: % 0.14/0.37 % This is a full first-order problem with equality. The Problem is non-linear. % 0.14/0.37 % 0.14/0.37 % 0.14/0.37 % SZS status GaveUp % 0.14/0.37 % 0.14/0.37 % SPASS beiseite: SPASS does currently not support equality problems. % 0.14/0.37 % Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.14/0.37 % 0.14/0.37 % SPASS-SCL-FOL Statistics: % 0.14/0.37 % Number of learned clauses: 0 % 0.14/0.37 % Number of propagations: 0 % 0.14/0.37 % Number of decisions: 0 % 0.14/0.37 % Number of resolutions: 0 % 0.14/0.37 % Number of condensations: 0 % 0.14/0.37 % Number of sub resolutions: 0 %------------------------------------------------------------------------------