%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1.1 % Problem : LCL855-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n014.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:35 PM UTC 2026 % Result : Unknown 0.09s 0.37s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL855-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.09/0.36 % Computer : n014.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Fri Sep 4 18:35:27 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.36 Running /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.09/0.37 % 0.09/0.37 % Input Clauses: % 0.09/0.37 % 1:2:3:INP:TopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x2,x1,x0)) % 0.09/0.37 % 2:1:0:INP:: -> =(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 3:2:1:INP:Top: class_OrderedGroup_Olordered__ab__group__add(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(x0),c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 4:1:2:INP:TopTop: -> =(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x1,x0,tc_nat)) % 0.09/0.37 % 5:2:3:INP:TopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x2,x1,x0)) % 0.09/0.37 % 6:2:3:INP:TopTopTop: class_OrderedGroup_Ogroup__add(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(x1,x2,x0),x2,x0),x1) % 0.09/0.37 % 7:3:4:INP:TopTopTopTop: class_Ring__and__Field_Oidom(x0),class_Int_Onumber__ring(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x1,x3,x0),x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x3,x0),c_HOL_Otimes__class_Otimes(x1,x2,x0),x0)) % 0.09/0.37 % 8:3:4:INP:TopTopTopTop: class_Ring__and__Field_Oidom(x0),class_Int_Onumber__ring(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x1,x3,x0),x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x3,x0),c_HOL_Otimes__class_Otimes(x1,x2,x0),x0)) % 0.09/0.37 % 9:1:3:INP:TopTopTop: -> =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),tc_nat)) % 0.09/0.37 % 10:1:3:INP:TopTopTop: -> =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),tc_nat)) % 0.09/0.37 % 11:1:0:INP:: -> =(c_HOL_Oplus__class_Oplus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 12:2:5:INP:TopTopTopTopTop: class_Ring__and__Field_Oring(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),x3,x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x4,x2,x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(x1,x4,x0),x2,x0),x3,x0),x0)) % 0.09/0.37 % 13:1:2:INP:TopTop: -> =(c_HOL_Oplus__class_Oplus(x0,c_Suc(x1),tc_nat),c_Suc(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat))) % 0.09/0.37 % 14:1:2:INP:TopTop: -> =(c_HOL_Oplus__class_Oplus(c_Suc(x0),x1,tc_nat),c_Suc(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat))) % 0.09/0.37 % 15:2:5:INP:TopTopTopTopTop: class_Ring__and__Field_Oring(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(x3,x1,x0),x2,x0),x4,x0),x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x3,x2,x0),x4,x0)) % 0.09/0.37 % 16:3:6:INP:TopTopTopTopTopTop: class_Ring__and__Field_Oring(x0),=(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),x3,x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x4,x2,x0),x5,x0)) -> =(x3,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(x4,x1,x0),x2,x0),x5,x0)) % 0.09/0.37 % 17:3:6:INP:TopTopTopTopTopTop: class_Ring__and__Field_Oring(x0),=(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),x3,x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x4,x2,x0),x5,x0)) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(x1,x4,x0),x2,x0),x3,x0),x5) % 0.09/0.37 % 18:1:2:INP:TopTop: -> c_HOL_Oord__class_Oless(x0,c_Suc(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat)),tc_nat) % 0.09/0.37 % 19:1:2:INP:TopTop: -> c_HOL_Oord__class_Oless(x0,c_Suc(c_HOL_Oplus__class_Oplus(x1,x0,tc_nat)),tc_nat) % 0.09/0.37 % 20:1:2:INP:TopTop: -> c_HOL_Oord__class_Oless(x0,c_Suc(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat)),tc_nat) % 0.09/0.37 % 21:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(x0,c_HOL_Oplus__class_Oplus(x1,x2,tc_nat),tc_nat) % 0.09/0.37 % 22:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(x0,c_HOL_Oplus__class_Oplus(x2,x1,tc_nat),tc_nat) % 0.09/0.37 % 23:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),x2,tc_nat) -> c_HOL_Oord__class_Oless(x0,x2,tc_nat) % 0.09/0.37 % 24:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(x0,c_HOL_Oplus__class_Oplus(x1,x2,tc_nat),tc_nat) % 0.09/0.37 % 25:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(x0,c_HOL_Oplus__class_Oplus(x2,x1,tc_nat),tc_nat) % 0.09/0.37 % 26:2:3:INP:TopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Oplus__class_Oplus(x1,x2,x0),c_HOL_Oplus__class_Oplus(x2,x1,x0)) % 0.09/0.37 % 27:2:3:INP:TopTopTop: class_OrderedGroup_Ocomm__monoid__add(x0) -> =(c_HOL_Oplus__class_Oplus(x1,x2,x0),c_HOL_Oplus__class_Oplus(x2,x1,x0)) % 0.09/0.37 % 28:1:2:INP:TopTop: -> =(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_HOL_Oplus__class_Oplus(x1,x0,tc_nat)) % 0.09/0.37 % 29:3:4:INP:TopTopTopTop: =(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_HOL_Oplus__class_Oplus(x2,x3,tc_nat)),c_HOL_Oord__class_Oless(x2,x1,tc_nat) -> c_HOL_Oord__class_Oless(x0,x3,tc_nat) % 0.09/0.37 % 30:2:3:INP:TopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Oplus__class_Oplus(x1,x2,x0),c_HOL_Oplus__class_Oplus(x2,x1,x0)) % 0.09/0.37 % 31:2:2:INP:TopTop: =(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) -> =(x0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 32:2:2:INP:TopTop: =(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) -> =(x1,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 33:3:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat),c_HOL_Oord__class_Oless(x0,x2,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(x1,x2,tc_nat),c_HOL_Ominus__class_Ominus(x1,x0,tc_nat),tc_nat) % 0.09/0.37 % 34:3:3:INP:TopTopTop: class_Nat_Osemiring__char__0(x0),=(c_Nat_Osemiring__1__class_Oof__nat(x1,x0),c_Nat_Osemiring__1__class_Oof__nat(x2,x0)) -> =(x1,x2) % 0.09/0.37 % 35:4:3:INP:TopTopTop: class_Ring__and__Field_Oidom(x0),class_Int_Onumber__ring(x0),=(x1,c_HOL_Oplus__class_Oplus(x1,x2,x0)) -> =(x2,c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 36:2:2:INP:TopTop: =(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),x0) -> =(x1,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 37:2:2:INP:TopTop: =(x0,c_HOL_Oplus__class_Oplus(x0,x1,tc_nat)) -> =(x1,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 38: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.09/0.37 % 39:2:2:INP:TopTop: class_OrderedGroup_Ogroup__add(x0) -> =(c_HOL_Ominus__class_Ominus(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 40:2:2:INP:TopTop: class_OrderedGroup_Ogroup__add(x0) -> =(c_HOL_Ominus__class_Ominus(x1,c_HOL_Ozero__class_Ozero(x0),x0),x1) % 0.09/0.37 % 41:2:2:INP:TopTop: class_OrderedGroup_Ogroup__add(x0) -> =(c_HOL_Ominus__class_Ominus(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 42: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.09/0.37 % 43:1:1:INP:Top: -> =(c_HOL_Ominus__class_Ominus(x0,x0,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 44:1:1:INP:Top: -> =(c_HOL_Ominus__class_Ominus(x0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),x0) % 0.09/0.37 % 45:3:3:INP:TopTopTop: =(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x0,x2,tc_nat)) -> =(x1,x2),=(x0,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 46:3:3:INP:TopTopTop: =(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x0,x2,tc_nat)) -> =(x0,c_HOL_Ozero__class_Ozero(tc_nat)),=(x1,x2) % 0.09/0.37 % 47:3:3:INP:TopTopTop: =(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x2,x1,tc_nat)) -> =(x1,c_HOL_Ozero__class_Ozero(tc_nat)),=(x0,x2) % 0.09/0.37 % 48:2:2:INP:TopTop: =(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) -> =(x0,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 49:2:2:INP:TopTop: =(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) -> =(x1,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 50:3:2:INP:TopTop: class_OrderedGroup_Olordered__ab__group__add(x0),=(c_HOL_Oplus__class_Oplus(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0)) -> =(x1,c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 51:3:6:INP:TopTopTopTopTopTop: class_Ring__and__Field_Opordered__ring(x0),c_HOL_Oord__class_Oless(x1,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(x2,x3,x0),x4,x0),x5,x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x3,x4,x0),x1,x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x2,x4,x0),x5,x0),x0) % 0.09/0.37 % 52:3:6:INP:TopTopTopTopTopTop: class_Ring__and__Field_Opordered__ring(x0),c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),x3,x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x4,x2,x0),x5,x0),x0) -> c_HOL_Oord__class_Oless(x3,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(x4,x1,x0),x2,x0),x5,x0),x0) % 0.09/0.37 % 53:3:6:INP:TopTopTopTopTopTop: class_Ring__and__Field_Opordered__ring(x0),c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(x1,x2,x0),x3,x0),x4,x0),x5,x0) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x3,x0),x4,x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x2,x3,x0),x5,x0),x0) % 0.09/0.37 % 54:3:6:INP:TopTopTopTopTopTop: class_Ring__and__Field_Opordered__ring(x0),c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),x3,x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x4,x2,x0),x5,x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(x1,x4,x0),x2,x0),x3,x0),x5,x0) % 0.09/0.37 % 55:4:3:INP:TopTopTop: class_Ring__and__Field_Oring__no__zero__divisors(x0),=(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Ozero__class_Ozero(x0)) -> =(x2,c_HOL_Ozero__class_Ozero(x0)),=(x1,c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 56:4:3:INP:TopTopTop: class_Ring__and__Field_Ono__zero__divisors(x0),=(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Ozero__class_Ozero(x0)) -> =(x2,c_HOL_Ozero__class_Ozero(x0)),=(x1,c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 57:1:2:INP:TopTop: -> c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(x0,x1,tc_nat),c_Suc(x0),tc_nat) % 0.09/0.37 % 58:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Oplus__class_Oplus(x1,c_HOL_Oplus__class_Oplus(x2,x3,x0),x0),c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(x1,x2,x0),x3,x0)) % 0.09/0.37 % 59:2:4:INP:TopTopTopTop: class_OrderedGroup_Oab__group__add(x0) -> =(c_HOL_Oplus__class_Oplus(x1,c_HOL_Oplus__class_Oplus(x2,x3,x0),x0),c_HOL_Oplus__class_Oplus(x2,c_HOL_Oplus__class_Oplus(x1,x3,x0),x0)) % 0.09/0.37 % 60:1:3:INP:TopTopTop: -> =(c_HOL_Oplus__class_Oplus(x0,c_HOL_Oplus__class_Oplus(x1,x2,tc_nat),tc_nat),c_HOL_Oplus__class_Oplus(x1,c_HOL_Oplus__class_Oplus(x0,x2,tc_nat),tc_nat)) % 0.09/0.37 % 61:1:3:INP:TopTopTop: -> =(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),x2,tc_nat),c_HOL_Oplus__class_Oplus(x0,c_HOL_Oplus__class_Oplus(x1,x2,tc_nat),tc_nat)) % 0.09/0.37 % 62:2:4:INP:TopTopTopTop: class_OrderedGroup_Ocomm__monoid__add(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(x1,x2,x0),x3,x0),c_HOL_Oplus__class_Oplus(x1,c_HOL_Oplus__class_Oplus(x2,x3,x0),x0)) % 0.09/0.37 % 63:2:4:INP:TopTopTopTop: class_OrderedGroup_Ocomm__monoid__add(x0) -> =(c_HOL_Oplus__class_Oplus(x1,c_HOL_Oplus__class_Oplus(x2,x3,x0),x0),c_HOL_Oplus__class_Oplus(x2,c_HOL_Oplus__class_Oplus(x1,x3,x0),x0)) % 0.09/0.37 % 64:2:4:INP:TopTopTopTop: class_OrderedGroup_Oab__semigroup__add(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(x1,x2,x0),x3,x0),c_HOL_Oplus__class_Oplus(x1,c_HOL_Oplus__class_Oplus(x2,x3,x0),x0)) % 0.09/0.37 % 65:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Oplus__class_Oplus(x1,c_HOL_Oplus__class_Oplus(x2,x3,x0),x0),c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(x1,x2,x0),x3,x0)) % 0.09/0.37 % 66:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(x1,x2,x0),x3,x0),c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(x1,x3,x0),x2,x0)) % 0.09/0.37 % 67:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Oplus__class_Oplus(x1,c_HOL_Oplus__class_Oplus(x2,x3,x0),x0),c_HOL_Oplus__class_Oplus(x2,c_HOL_Oplus__class_Oplus(x1,x3,x0),x0)) % 0.09/0.37 % 68:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(x1,x2,x0),x3,x0),c_HOL_Oplus__class_Oplus(x1,c_HOL_Oplus__class_Oplus(x2,x3,x0),x0)) % 0.09/0.37 % 69:3:2:INP:TopTop: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x1,tc_nat),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat) % 0.09/0.37 % 70:3:5:INP:TopTopTopTopTop: class_OrderedGroup_Oab__group__add(x0),=(c_HOL_Oplus__class_Oplus(x1,c_HOL_Oplus__class_Oplus(x2,x3,x0),x0),c_HOL_Oplus__class_Oplus(x2,x4,x0)) -> =(c_HOL_Oplus__class_Oplus(x1,x3,x0),x4) % 0.09/0.37 % 71:1:0:INP:: -> =(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 72:1:2:INP:TopTop: -> =(c_HOL_Ominus__class_Ominus(x0,c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 73: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(x0,c_HOL_Oplus__class_Oplus(x1,x2,tc_nat),tc_nat)) % 0.09/0.37 % 74: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.09/0.37 % 75: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.09/0.37 % 76:3:3:INP:TopTopTop: =(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x0,x2,tc_nat)),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat) -> =(x1,x2) % 0.09/0.37 % 77:3:2:INP:TopTop: =(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(x0,x1,tc_nat)) -> =(x1,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),=(x1,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 78:3:2:INP:TopTop: =(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(x0,x1,tc_nat)) -> =(x0,c_HOL_Ozero__class_Ozero(tc_nat)),=(x0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 79:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x2,x1,tc_nat),tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x1,tc_nat) % 0.09/0.37 % 80:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat) % 0.09/0.37 % 81:1:2:INP:TopTop: -> =(c_HOL_Oplus__class_Oplus(c_Suc(x0),x1,tc_nat),c_HOL_Oplus__class_Oplus(x0,c_Suc(x1),tc_nat)) % 0.09/0.37 % 82: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.09/0.37 % 83:1:3:INP:TopTopTop: -> =(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_HOL_Oplus__class_Oplus(x2,x1,tc_nat),tc_nat),c_HOL_Ominus__class_Ominus(x0,x2,tc_nat)) % 0.09/0.37 % 84:1:3:INP:TopTopTop: -> =(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_HOL_Oplus__class_Oplus(x0,x2,tc_nat),tc_nat),c_HOL_Ominus__class_Ominus(x1,x2,tc_nat)) % 0.09/0.37 % 85:1:4:INP:TopTopTopTop: -> =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x2,x1,tc_nat),x3,tc_nat),tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(x0,x2,tc_nat),x1,tc_nat),x3,tc_nat)) % 0.09/0.37 % 86:2:5:INP:TopTopTopTopTop: class_Ring__and__Field_Osemiring(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x3,x2,x0),x4,x0),x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(x1,x3,x0),x2,x0),x4,x0)) % 0.09/0.37 % 87:2:1:INP:Top: class_Ring__and__Field_Osemiring__1(x0) -> =(c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Ozero__class_Ozero(tc_nat),x0),c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 88:2:2:INP:TopTop: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x1,tc_nat) % 0.09/0.37 % 89:2:2:INP:TopTop: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat) % 0.09/0.37 % 90:4:3:INP:TopTopTop: class_OrderedGroup_Opordered__comm__monoid__add(x0),c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Oord__class_Oless(x2,c_HOL_Ozero__class_Ozero(x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x2,x1,x0),c_HOL_Ozero__class_Ozero(x0),x0) % 0.09/0.37 % 91: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.09/0.37 % 92: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.09/0.37 % 93: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.09/0.37 % 94:1:3:INP:TopTopTop: -> =(c_HOL_Otimes__class_Otimes(x0,c_HOL_Ominus__class_Ominus(x1,x2,tc_nat),tc_nat),c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),tc_nat)) % 0.09/0.37 % 95:1:3:INP:TopTopTop: -> =(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(x0,x1,tc_nat),x2,tc_nat),c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),c_HOL_Otimes__class_Otimes(x1,x2,tc_nat),tc_nat)) % 0.09/0.37 % 96: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.09/0.37 % 97:2:2:INP:TopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0),x0) -> % 0.09/0.37 % 98:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Suc(x2),x0,tc_nat),c_HOL_Otimes__class_Otimes(c_Suc(x2),x1,tc_nat),tc_nat) % 0.09/0.37 % 99:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Suc(x0),x1,tc_nat),c_HOL_Otimes__class_Otimes(c_Suc(x0),x2,tc_nat),tc_nat) -> c_HOL_Oord__class_Oless(x1,x2,tc_nat) % 0.09/0.37 % 100:2:3:INP:TopTopTop: =(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_HOL_Oplus__class_Oplus(x0,x2,tc_nat)) -> =(x1,x2) % 0.09/0.37 % 101:2:3:INP:TopTopTop: =(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_HOL_Oplus__class_Oplus(x2,x1,tc_nat)) -> =(x0,x2) % 0.09/0.37 % 102:2:3:INP:TopTopTop: =(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_HOL_Oplus__class_Oplus(x0,x2,tc_nat)) -> =(x1,x2) % 0.09/0.37 % 103:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oidom(x0),class_Int_Onumber__ring(x0),=(c_HOL_Oplus__class_Oplus(x1,x2,x0),c_HOL_Oplus__class_Oplus(x1,x3,x0)) -> =(x2,x3) % 0.09/0.37 % 104:3:4:INP:TopTopTopTop: class_OrderedGroup_Ocancel__ab__semigroup__add(x0),=(c_HOL_Oplus__class_Oplus(x1,x2,x0),c_HOL_Oplus__class_Oplus(x1,x3,x0)) -> =(x2,x3) % 0.09/0.37 % 105:3:4:INP:TopTopTopTop: class_OrderedGroup_Ocancel__semigroup__add(x0),=(c_HOL_Oplus__class_Oplus(x1,x2,x0),c_HOL_Oplus__class_Oplus(x1,x3,x0)) -> =(x2,x3) % 0.09/0.37 % 106:3:4:INP:TopTopTopTop: class_OrderedGroup_Ocancel__semigroup__add(x0),=(c_HOL_Oplus__class_Oplus(x1,x2,x0),c_HOL_Oplus__class_Oplus(x3,x2,x0)) -> =(x1,x3) % 0.09/0.37 % 107:3:2:INP:TopTop: =(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) -> =(x1,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),=(x1,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 108:3:2:INP:TopTop: =(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) -> =(x0,c_HOL_Ozero__class_Ozero(tc_nat)),=(x0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 109:1:3:INP:TopTopTop: -> =(c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(c_Suc(x0),x1,tc_nat),c_Suc(x2),tc_nat),c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(x0,x1,tc_nat),x2,tc_nat)) % 0.09/0.37 % 110:3:3:INP:TopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x1,x0),c_HOL_Otimes__class_Otimes(x2,x2,x0),x0),x0),=(x1,c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 111:3:3:INP:TopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x1,x0),c_HOL_Otimes__class_Otimes(x2,x2,x0),x0),x0),=(x2,c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 112:2:5:INP:TopTopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(x1,x2,x0),c_HOL_Oplus__class_Oplus(x3,x4,x0),x0),c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(x1,x3,x0),c_HOL_Oplus__class_Oplus(x2,x4,x0),x0)) % 0.09/0.37 % 113:2:2:INP:TopTop: class_Ring__and__Field_Oordered__semidom(x0),c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(x1,x0),c_HOL_Ozero__class_Ozero(x0),x0) -> % 0.09/0.37 % 114:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x1,x3,x0),x0) -> c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0) % 0.09/0.37 % 115:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x1,x3,x0),x0) -> c_HOL_Oord__class_Oless(x3,x2,x0),c_HOL_Oord__class_Oless(x2,x3,x0) % 0.09/0.37 % 116:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x3,x2,x0),x0) -> c_HOL_Oord__class_Oless(x2,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x2,x0) % 0.09/0.37 % 117:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x3,x2,x0),x0) -> c_HOL_Oord__class_Oless(x3,x1,x0),c_HOL_Oord__class_Oless(x1,x3,x0) % 0.09/0.37 % 118:3:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x2,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),c_HOL_Otimes__class_Otimes(x1,x2,tc_nat),tc_nat) % 0.09/0.37 % 119:3:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x2,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x2,x0,tc_nat),c_HOL_Otimes__class_Otimes(x2,x1,tc_nat),tc_nat) % 0.09/0.37 % 120:3:3:INP:TopTopTop: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat),c_HOL_Oord__class_Oless(x1,x2,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),tc_nat) % 0.09/0.37 % 121:3:3:INP:TopTopTop: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat),c_HOL_Oord__class_Oless(x1,x2,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x0,tc_nat),c_HOL_Otimes__class_Otimes(x2,x0,tc_nat),tc_nat) % 0.09/0.37 % 122:3:3:INP:TopTopTop: c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),tc_nat),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat) -> c_HOL_Oord__class_Oless(x1,x2,tc_nat) % 0.09/0.37 % 123:3:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x2,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x2,x0,tc_nat),c_HOL_Otimes__class_Otimes(x2,x1,tc_nat),tc_nat) % 0.09/0.37 % 124:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x1,x3,x0),x0),c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0) -> c_HOL_Oord__class_Oless(x3,x2,x0) % 0.09/0.37 % 125:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x3,c_HOL_Ozero__class_Ozero(x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x3,x2,x0),c_HOL_Otimes__class_Otimes(x3,x1,x0),x0) % 0.09/0.37 % 126:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x1,x3,x0),x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0) -> c_HOL_Oord__class_Oless(x2,x3,x0) % 0.09/0.37 % 127:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x3,x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x3,x1,x0),c_HOL_Otimes__class_Otimes(x3,x2,x0),x0) % 0.09/0.37 % 128:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Oord__class_Oless(x2,x3,x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x3,x0),c_HOL_Otimes__class_Otimes(x1,x2,x0),x0) % 0.09/0.37 % 129:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__semiring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Oord__class_Oless(x2,x3,x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x1,x3,x0),x0) % 0.09/0.37 % 130:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x3,x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x3,x1,x0),c_HOL_Otimes__class_Otimes(x3,x2,x0),x0) % 0.09/0.37 % 131:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x3,c_HOL_Ozero__class_Ozero(x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x3,x2,x0),c_HOL_Otimes__class_Otimes(x3,x1,x0),x0) % 0.09/0.37 % 132:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Oord__class_Oless(x2,x3,x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x3,x1,x0),c_HOL_Otimes__class_Otimes(x2,x1,x0),x0) % 0.09/0.37 % 133:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__semiring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Oord__class_Oless(x2,x3,x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x2,x1,x0),c_HOL_Otimes__class_Otimes(x3,x1,x0),x0) % 0.09/0.37 % 134:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x3,x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x3,x0),c_HOL_Otimes__class_Otimes(x2,x3,x0),x0) % 0.09/0.37 % 135:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x3,c_HOL_Ozero__class_Ozero(x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x2,x3,x0),c_HOL_Otimes__class_Otimes(x1,x3,x0),x0) % 0.09/0.37 % 136:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__comm__semiring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Oord__class_Oless(x2,x3,x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x1,x3,x0),x0) % 0.09/0.37 % 137:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x3,x2,x0),x0),c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(x1,x3,x0),x2,x0)) % 0.09/0.37 % 138:2:2:INP:TopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(x0),x1,x0),x1) % 0.09/0.37 % 139:2:2:INP:TopTop: class_OrderedGroup_Ocomm__monoid__add(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(x0),x1,x0),x1) % 0.09/0.37 % 140:1:1:INP:Top: -> =(x0,c_HOL_Oplus__class_Oplus(x0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)) % 0.09/0.37 % 141:1:1:INP:Top: -> =(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat),x0) % 0.09/0.37 % 142:1:1:INP:Top: -> =(c_HOL_Oplus__class_Oplus(x0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),x0) % 0.09/0.37 % 143:3:2:INP:TopTop: class_Ring__and__Field_Oidom(x0),class_Int_Onumber__ring(x0) -> =(x1,c_HOL_Oplus__class_Oplus(x1,c_HOL_Ozero__class_Ozero(x0),x0)) % 0.09/0.37 % 144:2:2:INP:TopTop: class_OrderedGroup_Ocomm__monoid__add(x0) -> =(c_HOL_Oplus__class_Oplus(x1,c_HOL_Ozero__class_Ozero(x0),x0),x1) % 0.09/0.37 % 145:2:2:INP:TopTop: class_OrderedGroup_Omonoid__add(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(x0),x1,x0),x1) % 0.09/0.37 % 146:2:2:INP:TopTop: class_OrderedGroup_Omonoid__add(x0) -> =(c_HOL_Oplus__class_Oplus(x1,c_HOL_Ozero__class_Ozero(x0),x0),x1) % 0.09/0.37 % 147:2:2:INP:TopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Oplus__class_Oplus(x1,c_HOL_Ozero__class_Ozero(x0),x0),x1) % 0.09/0.37 % 148:2:2:INP:TopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(x0),x1,x0),x1) % 0.09/0.37 % 149:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(x0),c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(x0),c_HOL_Ozero__class_Ozero(x0),x0),x0),x0) -> % 0.09/0.37 % 150:1:2:INP:TopTop: -> =(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),x1,tc_nat),x0) % 0.09/0.37 % 151:1:2:INP:TopTop: -> =(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),x0,tc_nat),x1) % 0.09/0.37 % 152:2:3:INP:TopTopTop: class_OrderedGroup_Ogroup__add(x0) -> =(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(x1,x2,x0),x2,x0),x1) % 0.09/0.37 % 153:2:2:INP:TopTop: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Oplus__class_Oplus(x1,x0,tc_nat),tc_nat) % 0.09/0.37 % 154:2:2:INP:TopTop: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),tc_nat) % 0.09/0.37 % 155:3:2:INP:TopTop: class_OrderedGroup_Olordered__ab__group__add(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),c_HOL_Oplus__class_Oplus(x1,x1,x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0) % 0.09/0.37 % 156:3:2:INP:TopTop: class_OrderedGroup_Olordered__ab__group__add(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),c_HOL_Oplus__class_Oplus(x1,x1,x0),x0) % 0.09/0.37 % 157:4:3:INP:TopTopTop: class_Ring__and__Field_Ono__zero__divisors(x0),=(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Ozero__class_Ozero(x0)) -> =(x1,c_HOL_Ozero__class_Ozero(x0)),=(x2,c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 158:3:2:INP:TopTop: =(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) -> =(x1,c_HOL_Ozero__class_Ozero(tc_nat)),=(x0,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 159:3:2:INP:TopTop: class_OrderedGroup_Olordered__ab__group__add(x0),c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0),x0) % 0.09/0.37 % 160:3:2:INP:TopTop: class_OrderedGroup_Olordered__ab__group__add(x0),c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0),x0) -> c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0) % 0.09/0.37 % 161:3:2:INP:TopTop: class_Ring__and__Field_Oordered__idom(x0),c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0),x0) -> c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0) % 0.09/0.37 % 162:3:2:INP:TopTop: class_Ring__and__Field_Oordered__idom(x0),c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x1,x1,x0),c_HOL_Ozero__class_Ozero(x0),x0) % 0.09/0.37 % 163:3:2:INP:TopTop: =(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(x0,x1,tc_nat)) -> =(x1,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),=(x0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 164:3:2:INP:TopTop: =(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(x0,x1,tc_nat)) -> =(x0,c_HOL_Ozero__class_Ozero(tc_nat)),=(x1,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 165:4:3:INP:TopTopTop: class_Ring__and__Field_Oordered__semiring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),c_HOL_Otimes__class_Otimes(x2,x1,x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x2,x0) % 0.09/0.37 % 166:4:3:INP:TopTopTop: class_Ring__and__Field_Oordered__semiring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),c_HOL_Otimes__class_Otimes(x1,x2,x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x2,x0) % 0.09/0.37 % 167:4:3:INP:TopTopTop: class_Ring__and__Field_Oordered__semiring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x2,x0) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),c_HOL_Otimes__class_Otimes(x2,x1,x0),x0) % 0.09/0.37 % 168:4:3:INP:TopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Oord__class_Oless(x2,c_HOL_Ozero__class_Ozero(x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),c_HOL_Otimes__class_Otimes(x2,x1,x0),x0) % 0.09/0.37 % 169:3:2:INP:TopTop: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x1,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Otimes__class_Otimes(x1,x0,tc_nat),tc_nat) % 0.09/0.37 % 170:1:2:INP:TopTop: -> =(c_HOL_Otimes__class_Otimes(x0,c_Suc(x1),tc_nat),c_HOL_Oplus__class_Oplus(x0,c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),tc_nat)) % 0.09/0.37 % 171:1:2:INP:TopTop: -> =(c_HOL_Otimes__class_Otimes(c_Suc(x0),x1,tc_nat),c_HOL_Oplus__class_Oplus(x1,c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),tc_nat)) % 0.09/0.37 % 172:2:3:INP:TopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x1,x0),c_HOL_Otimes__class_Otimes(x2,x2,x0),x0),c_HOL_Ozero__class_Ozero(x0),x0) -> % 0.09/0.37 % 173:2:3:INP:TopTopTop: class_Ring__and__Field_Osemiring__1(x0) -> =(c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Otimes__class_Otimes(x1,x2,tc_nat),x0),c_HOL_Otimes__class_Otimes(c_Nat_Osemiring__1__class_Oof__nat(x1,x0),c_Nat_Osemiring__1__class_Oof__nat(x2,x0),x0)) % 0.09/0.37 % 174:5:5:INP:TopTopTopTopTop: class_Ring__and__Field_Oidom(x0),class_Int_Onumber__ring(x0),=(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x3,x4,x0),x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x4,x0),c_HOL_Otimes__class_Otimes(x3,x2,x0),x0)) -> =(x2,x4),=(x1,x3) % 0.09/0.37 % 175:5:5:INP:TopTopTopTopTop: class_Ring__and__Field_Oidom(x0),class_Int_Onumber__ring(x0),=(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x3,x4,x0),x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x4,x0),c_HOL_Otimes__class_Otimes(x3,x2,x0),x0)) -> =(x2,x4),=(x1,x3) % 0.09/0.37 % 176:3:4:INP:TopTopTopTop: =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x2,x3,tc_nat),tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x0,x3,tc_nat),c_HOL_Otimes__class_Otimes(x2,x1,tc_nat),tc_nat)) -> =(x1,x3),=(x0,x2) % 0.09/0.37 % 177:3:4:INP:TopTopTopTop: =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x2,x3,tc_nat),tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x0,x3,tc_nat),c_HOL_Otimes__class_Otimes(x2,x1,tc_nat),tc_nat)) -> =(x1,x3),=(x0,x2) % 0.09/0.37 % 178:1:2:INP:TopTop: -> =(c_HOL_Ominus__class_Ominus(c_Suc(x0),c_Suc(x1),tc_nat),c_HOL_Ominus__class_Ominus(x0,x1,tc_nat)) % 0.09/0.37 % 179:1:0:INP:: -> =(c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 180:2:5:INP:TopTopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x3,x4,x0),x0),c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(x1,x3,x0),c_HOL_Otimes__class_Otimes(x2,x4,x0),x0)) % 0.09/0.37 % 181:2:5:INP:TopTopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x3,x4,x0),x0),c_HOL_Otimes__class_Otimes(x1,c_HOL_Otimes__class_Otimes(x2,c_HOL_Otimes__class_Otimes(x3,x4,x0),x0),x0)) % 0.09/0.37 % 182:2:5:INP:TopTopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x3,x4,x0),x0),c_HOL_Otimes__class_Otimes(x3,c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(x1,x2,x0),x4,x0),x0)) % 0.09/0.37 % 183:2:2:INP:TopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 184:2:2:INP:TopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(x1,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 185:2:2:INP:TopTop: class_Ring__and__Field_Oring__no__zero__divisors(x0) -> =(c_HOL_Otimes__class_Otimes(x1,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 186:2:2:INP:TopTop: class_Ring__and__Field_Oring__no__zero__divisors(x0) -> =(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 187:2:2:INP:TopTop: class_Ring__and__Field_Omult__zero(x0) -> =(c_HOL_Otimes__class_Otimes(x1,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 188:2:2:INP:TopTop: class_Ring__and__Field_Omult__zero(x0) -> =(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 189:1:1:INP:Top: -> =(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 190:1:1:INP:Top: -> =(c_HOL_Otimes__class_Otimes(x0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 191:2:2:INP:TopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 192:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(x0,x2,tc_nat),x1,tc_nat) % 0.09/0.37 % 193:1:0:INP:: -> =(c_HOL_Oplus__class_Oplus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 194:4:3:INP:TopTopTop: class_OrderedGroup_Opordered__comm__monoid__add(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x2,x0) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),c_HOL_Oplus__class_Oplus(x2,x1,x0),x0) % 0.09/0.37 % 195: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.09/0.37 % 196:4:5:INP:TopTopTopTopTop: class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x3,x4,x0) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x3,x1,x0),c_HOL_Oplus__class_Oplus(x4,x2,x0),x0) % 0.09/0.37 % 197:3:4:INP:TopTopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat),c_HOL_Oord__class_Oless(x2,x3,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x2,x0,tc_nat),c_HOL_Oplus__class_Oplus(x3,x1,tc_nat),tc_nat) % 0.09/0.37 % 198:3:3:INP:TopTopTop: class_OrderedGroup_Opordered__ab__group__add(x0),c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(x1,x2,x0),c_HOL_Ozero__class_Ozero(x0),x0) -> c_HOL_Oord__class_Oless(x1,x2,x0) % 0.09/0.37 % 199:3:3:INP:TopTopTop: class_OrderedGroup_Opordered__ab__group__add(x0),c_HOL_Oord__class_Oless(x1,x2,x0) -> c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(x1,x2,x0),c_HOL_Ozero__class_Ozero(x0),x0) % 0.09/0.37 % 200:3:3:INP:TopTopTop: class_Ring__and__Field_Oordered__semidom(x0),c_HOL_Oord__class_Oless(x1,x2,tc_nat) -> c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(x1,x0),c_Nat_Osemiring__1__class_Oof__nat(x2,x0),x0) % 0.09/0.37 % 201:3:3:INP:TopTopTop: class_Ring__and__Field_Oordered__semidom(x0),c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(x1,x0),c_Nat_Osemiring__1__class_Oof__nat(x2,x0),x0) -> c_HOL_Oord__class_Oless(x1,x2,tc_nat) % 0.09/0.37 % 202:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),tc_nat) -> c_HOL_Oord__class_Oless(x1,x2,tc_nat) % 0.09/0.37 % 203:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x2,x1,tc_nat),tc_nat) -> c_HOL_Oord__class_Oless(x0,x2,tc_nat) % 0.09/0.37 % 204:2:3:INP:TopTopTop: class_OrderedGroup_Oab__semigroup__idem__mult(x0) -> =(c_HOL_Otimes__class_Otimes(x1,c_HOL_Otimes__class_Otimes(x1,x2,x0),x0),c_HOL_Otimes__class_Otimes(x1,x2,x0)) % 0.09/0.37 % 205:4:3:INP:TopTopTop: class_Ring__and__Field_Oordered__semiring__strict(x0),c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x2,x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Ozero__class_Ozero(x0),x0) % 0.09/0.37 % 206:4:3:INP:TopTopTop: class_Ring__and__Field_Oordered__semiring__strict(x0),c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x2,x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x2,x1,x0),c_HOL_Ozero__class_Ozero(x0),x0) % 0.09/0.37 % 207:4:3:INP:TopTopTop: class_Ring__and__Field_Oordered__semiring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0),c_HOL_Oord__class_Oless(x2,c_HOL_Ozero__class_Ozero(x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x2,x1,x0),c_HOL_Ozero__class_Ozero(x0),x0) % 0.09/0.37 % 208:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__semidom(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x3,x0) -> c_HOL_Oord__class_Oless(x1,c_HOL_Oplus__class_Oplus(x3,x2,x0),x0) % 0.09/0.37 % 209:1:2:INP:TopTop: -> =(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),x1,tc_nat)) % 0.09/0.37 % 210:1:2:INP:TopTop: -> =(c_HOL_Otimes__class_Otimes(x0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Otimes__class_Otimes(x1,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)) % 0.09/0.37 % 211:1:2:INP:TopTop: c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),x0,tc_nat) -> % 0.09/0.37 % 212:1:2:INP:TopTop: c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),x1,tc_nat) -> % 0.09/0.37 % 213:5:5:INP:TopTopTopTopTop: class_Ring__and__Field_Oidom(x0),class_Int_Onumber__ring(x0),=(c_HOL_Oplus__class_Oplus(x1,c_HOL_Otimes__class_Otimes(x2,x3,x0),x0),c_HOL_Oplus__class_Oplus(x1,c_HOL_Otimes__class_Otimes(x2,x4,x0),x0)) -> =(x3,x4),=(x2,c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 214:3:4:INP:TopTopTopTop: =(c_HOL_Oplus__class_Oplus(x0,c_HOL_Otimes__class_Otimes(x1,x2,tc_nat),tc_nat),c_HOL_Oplus__class_Oplus(x0,c_HOL_Otimes__class_Otimes(x1,x3,tc_nat),tc_nat)) -> =(x2,x3),=(x1,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 215:3:3:INP:TopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),=(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x1,x0),c_HOL_Otimes__class_Otimes(x2,x2,x0),x0),c_HOL_Ozero__class_Ozero(x0)) -> =(x2,c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 216:3:3:INP:TopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),=(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x1,x0),c_HOL_Otimes__class_Otimes(x2,x2,x0),x0),c_HOL_Ozero__class_Ozero(x0)) -> =(x1,c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 217:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,c_HOL_Ominus__class_Ominus(x1,x2,tc_nat),tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x0,x2,tc_nat),x1,tc_nat) % 0.09/0.37 % 218:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),x2,tc_nat) -> c_HOL_Oord__class_Oless(x0,c_HOL_Ominus__class_Ominus(x2,x1,tc_nat),tc_nat) % 0.09/0.37 % 219:3:4:INP:TopTopTopTop: class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0),c_HOL_Oord__class_Oless(x1,x2,x0) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x1,x3,x0),c_HOL_Oplus__class_Oplus(x2,x3,x0),x0) % 0.09/0.37 % 220:3:4:INP:TopTopTopTop: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0),c_HOL_Oord__class_Oless(x1,x2,x0) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x1,x3,x0),c_HOL_Oplus__class_Oplus(x2,x3,x0),x0) % 0.09/0.37 % 221:3:4:INP:TopTopTopTop: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0),c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x1,x2,x0),c_HOL_Oplus__class_Oplus(x3,x2,x0),x0) -> c_HOL_Oord__class_Oless(x1,x3,x0) % 0.09/0.37 % 222:3:4:INP:TopTopTopTop: class_OrderedGroup_Opordered__cancel__ab__semigroup__add(x0),c_HOL_Oord__class_Oless(x1,x2,x0) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x3,x1,x0),c_HOL_Oplus__class_Oplus(x3,x2,x0),x0) % 0.09/0.37 % 223:3:4:INP:TopTopTopTop: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0),c_HOL_Oord__class_Oless(x1,x2,x0) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x3,x1,x0),c_HOL_Oplus__class_Oplus(x3,x2,x0),x0) % 0.09/0.37 % 224:3:4:INP:TopTopTopTop: class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(x0),c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x1,x2,x0),c_HOL_Oplus__class_Oplus(x1,x3,x0),x0) -> c_HOL_Oord__class_Oless(x2,x3,x0) % 0.09/0.37 % 225:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x0,x2,tc_nat),c_HOL_Oplus__class_Oplus(x1,x2,tc_nat),tc_nat) % 0.09/0.37 % 226:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_HOL_Oplus__class_Oplus(x0,x2,tc_nat),tc_nat) -> c_HOL_Oord__class_Oless(x1,x2,tc_nat) % 0.09/0.37 % 227:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(x2,x0,tc_nat),c_HOL_Oplus__class_Oplus(x2,x1,tc_nat),tc_nat) % 0.09/0.37 % 228:1:0:INP:: -> =(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 229:2:2:INP:TopTop: class_OrderedGroup_Oab__semigroup__idem__mult(x0) -> =(c_HOL_Otimes__class_Otimes(x1,x1,x0),x1) % 0.09/0.37 % 230:2:2:INP:TopTop: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ominus__class_Ominus(x0,x1,tc_nat),tc_nat) -> c_HOL_Oord__class_Oless(x1,x0,tc_nat) % 0.09/0.37 % 231:2:2:INP:TopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ominus__class_Ominus(x1,x0,tc_nat),tc_nat) % 0.09/0.37 % 232:2:1:INP:Top: class_Ring__and__Field_Oordered__ring__strict(x0) -> =(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(x0),c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(x0),c_HOL_Ozero__class_Ozero(x0),x0),x0),c_HOL_Ozero__class_Ozero(x0)) % 0.09/0.37 % 233:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x3,x2,x0),x0) -> c_HOL_Oord__class_Oless(x2,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Oord__class_Oless(x1,x3,x0) % 0.09/0.37 % 234:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x3,x2,x0),x0) -> c_HOL_Oord__class_Oless(x3,x1,x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x2,x0) % 0.09/0.37 % 235:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x1,x3,x0),x0) -> c_HOL_Oord__class_Oless(x1,c_HOL_Ozero__class_Ozero(x0),x0),c_HOL_Oord__class_Oless(x2,x3,x0) % 0.09/0.37 % 236:4:4:INP:TopTopTopTop: class_Ring__and__Field_Oordered__ring__strict(x0),c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x1,x3,x0),x0) -> c_HOL_Oord__class_Oless(x3,x2,x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),x1,x0) % 0.09/0.37 % 237:2:3:INP:TopTopTop: =(c_HOL_Otimes__class_Otimes(c_Suc(x0),x1,tc_nat),c_HOL_Otimes__class_Otimes(c_Suc(x0),x2,tc_nat)) -> =(x1,x2) % 0.09/0.37 % 238:2:3:INP:TopTopTop: class_Ring__and__Field_Osemiring__1(x0) -> =(c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Oplus__class_Oplus(x1,x2,tc_nat),x0),c_HOL_Oplus__class_Oplus(c_Nat_Osemiring__1__class_Oof__nat(x1,x0),c_Nat_Osemiring__1__class_Oof__nat(x2,x0),x0)) % 0.09/0.37 % 239:3:2:INP:TopTop: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x1,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(x0,x1,tc_nat),x0,tc_nat) % 0.09/0.37 % 240: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_HOL_Oord__class_Oless(x1,x2,x0) -> c_HOL_Oord__class_Oless(x3,x4,x0) % 0.09/0.37 % 241: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_HOL_Oord__class_Oless(x3,x4,x0) -> c_HOL_Oord__class_Oless(x1,x2,x0) % 0.09/0.37 % 242:2:2:INP:TopTop: -> =(c_HOL_Oplus__class_Oplus(x0,c_HOL_Ominus__class_Ominus(x1,x0,tc_nat),tc_nat),x1),c_HOL_Oord__class_Oless(x1,x0,tc_nat) % 0.09/0.37 % 243:3:2:INP:TopTop: =(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) -> =(x1,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),=(x0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 244:3:2:INP:TopTop: =(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) -> =(x0,c_HOL_Ozero__class_Ozero(tc_nat)),=(x1,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 245:2:4:INP:TopTopTopTop: class_OrderedGroup_Oab__semigroup__mult(x0) -> =(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(x1,x2,x0),x3,x0),c_HOL_Otimes__class_Otimes(x1,c_HOL_Otimes__class_Otimes(x2,x3,x0),x0)) % 0.09/0.37 % 246:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(x1,x2,x0),x3,x0),c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(x1,x3,x0),x2,x0)) % 0.09/0.37 % 247:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(x1,x2,x0),x3,x0),c_HOL_Otimes__class_Otimes(x1,c_HOL_Otimes__class_Otimes(x2,x3,x0),x0)) % 0.09/0.37 % 248:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(x1,c_HOL_Otimes__class_Otimes(x2,x3,x0),x0),c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(x1,x2,x0),x3,x0)) % 0.09/0.37 % 249:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(x1,c_HOL_Otimes__class_Otimes(x2,x3,x0),x0),c_HOL_Otimes__class_Otimes(x2,c_HOL_Otimes__class_Otimes(x1,x3,x0),x0)) % 0.09/0.37 % 250:1:3:INP:TopTopTop: -> =(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),x2,tc_nat),c_HOL_Otimes__class_Otimes(x0,c_HOL_Otimes__class_Otimes(x1,x2,tc_nat),tc_nat)) % 0.09/0.37 % 251:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(x1,c_HOL_Otimes__class_Otimes(x2,x3,x0),x0),c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(x1,x2,x0),x3,x0)) % 0.09/0.37 % 252:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(x1,x2,x0),x3,x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x3,x0),c_HOL_Otimes__class_Otimes(x2,x3,x0),x0)) % 0.09/0.37 % 253:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring(x0) -> =(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(x1,x2,x0),x3,x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x3,x0),c_HOL_Otimes__class_Otimes(x2,x3,x0),x0)) % 0.09/0.37 % 254:1:3:INP:TopTopTop: -> =(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(x0,x1,tc_nat),x2,tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),c_HOL_Otimes__class_Otimes(x1,x2,tc_nat),tc_nat)) % 0.09/0.37 % 255:1:3:INP:TopTopTop: -> =(c_HOL_Otimes__class_Otimes(x0,c_HOL_Oplus__class_Oplus(x1,x2,tc_nat),tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),c_HOL_Otimes__class_Otimes(x0,x2,tc_nat),tc_nat)) % 0.09/0.37 % 256:2:4:INP:TopTopTopTop: class_Ring__and__Field_Ocomm__semiring__1(x0) -> =(c_HOL_Otimes__class_Otimes(x1,c_HOL_Oplus__class_Oplus(x2,x3,x0),x0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(x1,x2,x0),c_HOL_Otimes__class_Otimes(x1,x3,x0),x0)) % 0.09/0.37 % 257:3:3:INP:TopTopTop: class_Orderings_Opreorder(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x2,x1,x0) -> % 0.09/0.37 % 258:3:3:INP:TopTopTop: class_Orderings_Opreorder(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x2,x1,x0) -> % 0.09/0.37 % 259:3:3:INP:TopTopTop: class_Orderings_Olinorder(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x2,x1,x0) -> % 0.09/0.37 % 260:3:3:INP:TopTopTop: class_Orderings_Oorder(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x2,x1,x0) -> % 0.09/0.37 % 261:2:2:INP:TopTop: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(x0,c_Suc(x1),tc_nat),x0,tc_nat) % 0.09/0.37 % 262:2:1:INP:Top: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat) -> =(c_Suc(c_HOL_Ominus__class_Ominus(x0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)),x0) % 0.09/0.37 % 263:2:2:INP:TopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(x0,c_Suc(x1),tc_nat) % 0.09/0.37 % 264:2:2:INP:TopTop: c_HOL_Oord__class_Oless(c_Suc(x0),x1,tc_nat) -> c_HOL_Oord__class_Oless(x0,x1,tc_nat) % 0.09/0.37 % 265:1:1:INP:Top: =(x0,c_Suc(x0)) -> % 0.09/0.37 % 266:1:1:INP:Top: =(c_Suc(x0),x0) -> % 0.09/0.37 % 267:3:2:INP:TopTop: c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),x0,tc_nat),c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),x1,tc_nat) -> c_HOL_Oord__class_Oless(x1,c_HOL_Otimes__class_Otimes(x1,x0,tc_nat),tc_nat) % 0.09/0.37 % 268:3:2:INP:TopTop: c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),x0,tc_nat),c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),x1,tc_nat) -> c_HOL_Oord__class_Oless(x1,c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),tc_nat) % 0.09/0.37 % 269:1:0:INP:: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) -> % 0.09/0.37 % 270:1:2:INP:TopTop: -> =(c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),x0,x1),x0) % 0.09/0.37 % 271:2:1:INP:Top: -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat),=(x0,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 272:3:2:INP:TopTop: class_Ring__and__Field_Oordered__semidom(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),c_Nat_Osemiring__1__class_Oof__nat(x1,x0),x0) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x1,tc_nat) % 0.09/0.37 % 273:3:2:INP:TopTop: class_Ring__and__Field_Oordered__semidom(x0),c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x1,tc_nat) -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(x0),c_Nat_Osemiring__1__class_Oof__nat(x1,x0),x0) % 0.09/0.37 % 274:3:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat),c_HOL_Oord__class_Oless(x2,x0,tc_nat) -> c_HOL_Oord__class_Oless(c_Suc(x2),x1,tc_nat) % 0.09/0.37 % 275:1:1:INP:Top: -> c_HOL_Oord__class_Oless(x0,c_Suc(x0),tc_nat) % 0.09/0.37 % 276:1:1:INP:Top: -> c_HOL_Oord__class_Oless(x0,c_Suc(x0),tc_nat) % 0.09/0.37 % 277:1:1:INP:Top: =(c_Suc(x0),c_HOL_Ozero__class_Ozero(tc_nat)) -> % 0.09/0.37 % 278:1:1:INP:Top: =(c_Suc(x0),c_HOL_Ozero__class_Ozero(tc_nat)) -> % 0.09/0.37 % 279:4:3:INP:TopTopTop: class_Orderings_Olinorder(x0) -> =(x1,x2),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x2,x1,x0) % 0.09/0.37 % 280:4:3:INP:TopTopTop: class_Orderings_Olinorder(x0) -> c_HOL_Oord__class_Oless(x1,x2,x0),=(x2,x1),c_HOL_Oord__class_Oless(x2,x1,x0) % 0.09/0.37 % 281:4:3:INP:TopTopTop: class_Orderings_Olinorder(x0) -> c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x2,x1,x0),=(x2,x1) % 0.09/0.37 % 282:3:2:INP:TopTop: -> c_HOL_Oord__class_Oless(x0,x1,tc_nat),c_HOL_Oord__class_Oless(x1,x0,tc_nat),=(x1,x0) % 0.09/0.37 % 283:3:2:INP:TopTop: -> c_HOL_Oord__class_Oless(x0,x1,tc_nat),c_HOL_Oord__class_Oless(x1,x0,tc_nat),=(x1,x0) % 0.09/0.37 % 284:4:3:INP:TopTopTop: class_Orderings_Olinorder(x0) -> =(x1,x2),c_HOL_Oord__class_Oless(x2,x1,x0),c_HOL_Oord__class_Oless(x1,x2,x0) % 0.09/0.37 % 285:4:3:INP:TopTopTop: class_Ring__and__Field_Oordered__idom(x0) -> c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x2,x1,x0),=(x2,x1) % 0.09/0.37 % 286:2:3:INP:TopTopTop: -> =(c_Lambda_Oliftn(x0,c_Lambda_OdB_OVar(x1),x2),c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(x1,x0,tc_nat))),c_HOL_Oord__class_Oless(x1,x2,tc_nat) % 0.09/0.37 % 287:2:2:INP:TopTop: class_Orderings_Opreorder(x0),c_HOL_Oord__class_Oless(x1,x1,x0) -> % 0.09/0.37 % 288:2:2:INP:TopTop: class_Orderings_Olinorder(x0),c_HOL_Oord__class_Oless(x1,x1,x0) -> % 0.09/0.37 % 289:2:2:INP:TopTop: class_Orderings_Oorder(x0),c_HOL_Oord__class_Oless(x1,x1,x0) -> % 0.09/0.37 % 290:1:1:INP:Top: c_HOL_Oord__class_Oless(x0,x0,tc_nat) -> % 0.09/0.37 % 291:1:1:INP:Top: c_HOL_Oord__class_Oless(x0,x0,tc_nat) -> % 0.09/0.37 % 292:3:2:INP:TopTop: c_HOL_Oord__class_Oless(x0,c_Suc(x1),tc_nat) -> =(x0,c_Suc(c_ATP__Linkup_Osko__Nat__Xless__Suc__eq__0__disj__1__1(x0,x1))),=(x0,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 293:3:2:INP:TopTop: c_HOL_Oord__class_Oless(x0,c_Suc(x1),tc_nat) -> =(x0,x1),c_HOL_Oord__class_Oless(x0,x1,tc_nat) % 0.09/0.37 % 294:3:2:INP:TopTop: c_HOL_Oord__class_Oless(x0,c_Suc(x1),tc_nat) -> =(x1,x0),c_HOL_Oord__class_Oless(x0,x1,tc_nat) % 0.09/0.37 % 295:3:2:INP:TopTop: c_HOL_Oord__class_Oless(x0,c_Suc(x1),tc_nat) -> =(x0,x1),c_HOL_Oord__class_Oless(x0,x1,tc_nat) % 0.09/0.37 % 296:1:0:INP:: -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) % 0.09/0.37 % 297:2:2:INP:TopTop: =(c_Suc(x0),c_Suc(x1)) -> =(x0,x1) % 0.09/0.37 % 298:2:2:INP:TopTop: =(c_Suc(x0),c_Suc(x1)) -> =(x0,x1) % 0.09/0.37 % 299:1:1:INP:Top: =(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(x0)) -> % 0.09/0.37 % 300:1:1:INP:Top: =(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(x0)) -> % 0.09/0.37 % 301:2:1:INP:Top: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat) -> =(x0,c_Suc(c_ATP__Linkup_Osko__Nat__Xgr0__implies__Suc__1__1(x0))) % 0.09/0.37 % 302:2:1:INP:Top: c_HOL_Oord__class_Oless(x0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) -> =(x0,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 303:2:1:INP:Top: c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),x0,tc_nat) -> =(x0,c_Suc(c_ATP__Linkup_Osko__Nat__Xgr0__conv__Suc__1__1(x0))) % 0.09/0.37 % 304:3:2:INP:TopTop: c_HOL_Oord__class_Oless(x0,c_Suc(x1),tc_nat) -> c_HOL_Oord__class_Oless(c_ATP__Linkup_Osko__Nat__Xless__Suc__eq__0__disj__1__1(x0,x1),x1,tc_nat),=(x0,c_HOL_Ozero__class_Ozero(tc_nat)) % 0.09/0.37 % 305:4:4:INP:TopTopTopTop: class_Orderings_Opreorder(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x3,x1,x0) -> c_HOL_Oord__class_Oless(x3,x2,x0) % 0.09/0.37 % 306:4:4:INP:TopTopTopTop: class_Orderings_Oorder(x0),c_HOL_Oord__class_Oless(x1,x2,x0),c_HOL_Oord__class_Oless(x2,x3,x0) -> c_HOL_Oord__class_Oless(x1,x3,x0) % 0.09/0.37 % 307:1:1:INP:Top: c_HOL_Oord__class_Oless(x0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) -> % 0.09/0.37 % 308:1:1:INP:Top: c_HOL_Oord__class_Oless(x0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) -> % 0.09/0.37 % 309:3:2:INP:TopTop: c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),x0,tc_nat),c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),x1,tc_nat) -> c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Otimes__class_Otimes(x0,x1,tc_nat),tc_nat) % 0.09/0.37 % 310:1:1:INP:Top: -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(x0),tc_nat) % 0.09/0.37 % 311:1:1:INP:Top: -> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(x0),tc_nat) % 0.09/0.37 % 312:3:2:INP:TopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(c_Suc(x0),x1,tc_nat),=(c_Suc(x0),x1) % 0.09/0.37 % 313:2:1:INP:Top: -> c_HOL_Oord__class_Oless(x0,x0,tc_nat),c_HOL_Oord__class_Oless(x0,c_Suc(x0),tc_nat) % 0.09/0.37 % 314:2:2:INP:TopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat),c_HOL_Oord__class_Oless(x1,c_Suc(x0),tc_nat) -> % 0.09/0.37 % 315:2:2:INP:TopTop: -> c_HOL_Oord__class_Oless(x0,c_Suc(x1),tc_nat),c_HOL_Oord__class_Oless(x1,x0,tc_nat) % 0.09/0.37 % 316:2:2:INP:TopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(c_Suc(x0),c_Suc(x1),tc_nat) % 0.09/0.37 % 317:2:2:INP:TopTop: c_HOL_Oord__class_Oless(c_Suc(x0),c_Suc(x1),tc_nat) -> c_HOL_Oord__class_Oless(x0,x1,tc_nat) % 0.09/0.37 % 318:2:2:INP:TopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> c_HOL_Oord__class_Oless(c_Suc(x0),c_Suc(x1),tc_nat) % 0.09/0.37 % 319:2:2:INP:TopTop: c_Lambda_Obeta(x0,x1) -> c_Lambda_Obeta(c_Lambda_OdB_OAbs(x0),c_Lambda_OdB_OAbs(x1)) % 0.09/0.37 % 320:2:2:INP:TopTop: c_Lambda_Obeta(c_Lambda_OdB_OAbs(x0),x1) -> =(x1,c_Lambda_OdB_OAbs(c_Lambda_Osko__Lambda__Xbeta__cases__2__1(x0,x1))) % 0.09/0.37 % 321:2:2:INP:TopTop: -> c_HOL_Oord__class_Oless(x0,x0,tc_nat),=(c_Lambda_Osubstn(c_Lambda_OdB_OVar(x0),x1,x0),c_Lambda_Oliftn(x0,x1,c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 322:2:3:INP:TopTopTop: c_Lambda_Obeta(x0,x1) -> c_Lambda_Obeta(c_Lambda_Olift(x0,x2),c_Lambda_Olift(x1,x2)) % 0.09/0.37 % 323:2:2:INP:TopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> =(c_Lambda_Olift(c_Lambda_OdB_OVar(x0),x1),c_Lambda_OdB_OVar(x0)) % 0.09/0.37 % 324:1:3:INP:TopTopTop: -> =(c_Lambda_Osubst(c_Lambda_Olift(x0,x1),x2,x1),x0) % 0.09/0.37 % 325:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> =(c_Lambda_Oliftn(x2,c_Lambda_OdB_OVar(x0),x1),c_Lambda_OdB_OVar(x0)) % 0.09/0.37 % 326:2:2:INP:TopTop: -> c_HOL_Oord__class_Oless(x0,x0,tc_nat),=(c_Lambda_Osubst(c_Lambda_OdB_OVar(x0),x1,x0),x1) % 0.09/0.37 % 327:1:3:INP:TopTopTop: -> =(c_Lambda_Osubstn(x0,x1,x2),c_Lambda_Osubst(x0,c_Lambda_Oliftn(x2,x1,c_HOL_Ozero__class_Ozero(tc_nat)),x2)) % 0.09/0.37 % 328:3:3:INP:TopTopTop: -> =(c_Lambda_Osubst(c_Lambda_OdB_OVar(x0),x1,x2),c_Lambda_OdB_OVar(x0)),=(x0,x2),c_HOL_Oord__class_Oless(x2,x0,tc_nat) % 0.09/0.37 % 329:2:4:INP:TopTopTopTop: c_Lambda_Obeta(x0,x1) -> c_Lambda_Obeta(c_Lambda_Osubst(x0,x2,x3),c_Lambda_Osubst(x1,x2,x3)) % 0.09/0.37 % 330:1:3:INP:TopTopTop: -> =(c_Lambda_Oliftn(c_Suc(x0),x1,x2),c_Lambda_Olift(c_Lambda_Oliftn(x0,x1,x2),x2)) % 0.09/0.37 % 331:1:2:INP:TopTop: =(c_Lambda_OdB_OVar(x0),c_Lambda_OdB_OAbs(x1)) -> % 0.09/0.37 % 332:3:3:INP:TopTopTop: -> =(c_Lambda_Osubstn(c_Lambda_OdB_OVar(x0),x1,x2),c_Lambda_OdB_OVar(x0)),=(x0,x2),c_HOL_Oord__class_Oless(x2,x0,tc_nat) % 0.09/0.37 % 333:2:2:INP:TopTop: =(c_Lambda_OdB_OAbs(x0),c_Lambda_OdB_OAbs(x1)) -> =(x0,x1) % 0.09/0.37 % 334:1:2:INP:TopTop: -> c_Lambda_Obeta(c_Lambda_OdB_OApp(c_Lambda_OdB_OAbs(x0),x1),c_Lambda_Osubst(x0,x1,c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 335:1:2:INP:TopTop: c_Lambda_Obeta(c_Lambda_OdB_OVar(x0),x1) -> % 0.09/0.37 % 336:2:2:INP:TopTop: c_Lambda_Obeta(c_Lambda_OdB_OAbs(x0),x1) -> c_Lambda_Obeta(x0,c_Lambda_Osko__Lambda__Xbeta__cases__2__1(x0,x1)) % 0.09/0.37 % 337:1:2:INP:TopTop: -> =(c_Lambda_Osubstn(x0,x1,c_HOL_Ozero__class_Ozero(tc_nat)),c_Lambda_Osubst(x0,x1,c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 338:2:3:INP:TopTopTop: c_HOL_Oord__class_Oless(x0,x1,tc_nat) -> =(c_Lambda_Osubst(c_Lambda_OdB_OVar(x0),x2,x1),c_Lambda_OdB_OVar(x0)) % 0.09/0.37 % 339:2:3:INP:TopTopTop: c_InductTermi_OIT(x0) -> c_InductTermi_OIT(c_Lambda_Osubst(x0,c_Lambda_OdB_OVar(x1),x2)) % 0.09/0.37 % 340:1:2:INP:TopTop: -> =(c_Lambda_Osubst(c_Lambda_OdB_OVar(x0),x1,x0),x1) % 0.09/0.37 % 341:2:2:INP:TopTop: =(c_Lambda_OdB_OVar(x0),c_Lambda_OdB_OVar(x1)) -> =(x0,x1) % 0.09/0.37 % 342:1:2:INP:TopTop: =(c_Lambda_OdB_OAbs(x0),c_Lambda_OdB_OVar(x1)) -> % 0.09/0.37 % 343:1:4:INP:TopTopTopTop: -> =(c_Lambda_Osubst(c_Lambda_OdB_OApp(x0,x1),x2,x3),c_Lambda_OdB_OApp(c_Lambda_Osubst(x0,x2,x3),c_Lambda_Osubst(x1,x2,x3))) % 0.09/0.37 % 344:1:3:INP:TopTopTop: =(c_Lambda_OdB_OApp(x0,x1),c_Lambda_OdB_OAbs(x2)) -> % 0.09/0.37 % 345:1:3:INP:TopTopTop: =(c_Lambda_OdB_OAbs(x0),c_Lambda_OdB_OApp(x1,x2)) -> % 0.09/0.37 % 346:2:4:INP:TopTopTopTop: =(c_Lambda_OdB_OApp(x0,x1),c_Lambda_OdB_OApp(x2,x3)) -> =(x0,x2) % 0.09/0.37 % 347:2:4:INP:TopTopTopTop: =(c_Lambda_OdB_OApp(x0,x1),c_Lambda_OdB_OApp(x2,x3)) -> =(x1,x3) % 0.09/0.37 % 348:1:3:INP:TopTopTop: =(c_Lambda_OdB_OVar(x0),c_Lambda_OdB_OApp(x1,x2)) -> % 0.09/0.37 % 349:1:0:INP:: -> c_InductTermi_OIT(v_s____) % 0.09/0.37 % 350:2:2:INP:TopTop: c_InductTermi_OIT(x0) -> c_InductTermi_OIT(c_Lambda_Olift(x0,x1)) % 0.09/0.37 % 351:1:1:INP:Top: -> c_InductTermi_OIT(c_Lambda_OdB_OVar(x0)) % 0.09/0.37 % 352:1:3:INP:TopTopTop: -> =(c_Lambda_Olift(c_Lambda_OdB_OApp(x0,x1),x2),c_Lambda_OdB_OApp(c_Lambda_Olift(x0,x2),c_Lambda_Olift(x1,x2))) % 0.09/0.37 % 353:1:0:INP:: -> c_InductTermi_OIT(v_ta____) % 0.09/0.37 % 354:2:1:INP:Top: c_InductTermi_OIT(x0) -> c_InductTermi_OIT(c_Lambda_OdB_OAbs(x0)) % 0.09/0.37 % 355:2:3:INP:TopTopTop: c_Lambda_Obeta(x0,x1) -> c_Lambda_Obeta(c_Lambda_OdB_OApp(x2,x0),c_Lambda_OdB_OApp(x2,x1)) % 0.09/0.37 % 356:2:3:INP:TopTopTop: c_Lambda_Obeta(x0,x1) -> c_Lambda_Obeta(c_Lambda_OdB_OApp(x0,x2),c_Lambda_OdB_OApp(x1,x2)) % 0.09/0.37 % 357:1:4:INP:TopTopTopTop: -> =(c_Lambda_Oliftn(x0,c_Lambda_OdB_OApp(x1,x2),x3),c_Lambda_OdB_OApp(c_Lambda_Oliftn(x0,x1,x3),c_Lambda_Oliftn(x0,x2,x3))) % 0.09/0.37 % 358:2:2:INP:TopTop: c_InductTermi_OIT(x0) -> c_InductTermi_OIT(c_Lambda_OdB_OApp(x0,c_Lambda_OdB_OVar(x1))) % 0.09/0.37 % 359:1:4:INP:TopTopTopTop: -> =(c_Lambda_Osubstn(c_Lambda_OdB_OApp(x0,x1),x2,x3),c_Lambda_OdB_OApp(c_Lambda_Osubstn(x0,x2,x3),c_Lambda_Osubstn(x1,x2,x3))) % 0.09/0.37 % 360:1:3:INP:TopTopTop: =(c_Lambda_OdB_OApp(x0,x1),c_Lambda_OdB_OVar(x2)) -> % 0.09/0.37 % 361:1:0:INP:: -> c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OApp(c_Lambda_OdB_OVar(c_HOL_Ozero__class_Ozero(tc_nat)),c_Lambda_Olift(v_ta____,c_HOL_Ozero__class_Ozero(tc_nat))),v_s____,c_HOL_Ozero__class_Ozero(tc_nat))) % 0.09/0.37 % 362:1:0:INP:: c_InductTermi_OIT(c_Lambda_OdB_OApp(v_s____,v_ta____)) -> % 0.09/0.37 % 363:1:0:INP:: -> class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat) % 0.09/0.37 % 364:1:0:INP:: -> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) % 0.09/0.37 % 365:1:0:INP:: -> class_Ring__and__Field_Oordered__comm__semiring__strict(tc_nat) % 0.09/0.37 % 366:1:0:INP:: -> class_Ring__and__Field_Oordered__semiring__strict(tc_nat) % 0.09/0.37 % 367:1:0:INP:: -> class_OrderedGroup_Opordered__comm__monoid__add(tc_nat) % 0.09/0.37 % 368:1:0:INP:: -> class_OrderedGroup_Ocancel__ab__semigroup__add(tc_nat) % 0.09/0.37 % 369:1:0:INP:: -> class_OrderedGroup_Ocancel__semigroup__add(tc_nat) % 0.09/0.37 % 370:1:0:INP:: -> class_Ring__and__Field_Ono__zero__divisors(tc_nat) % 0.09/0.37 % 371:1:0:INP:: -> class_Ring__and__Field_Oordered__semidom(tc_nat) % 0.09/0.37 % 372:1:0:INP:: -> class_Ring__and__Field_Ocomm__semiring__1(tc_nat) % 0.09/0.37 % 373:1:0:INP:: -> class_OrderedGroup_Oab__semigroup__mult(tc_nat) % 0.09/0.37 % 374:1:0:INP:: -> class_OrderedGroup_Oab__semigroup__add(tc_nat) % 0.09/0.37 % 375:1:0:INP:: -> class_Ring__and__Field_Ocomm__semiring(tc_nat) % 0.09/0.37 % 376:1:0:INP:: -> class_OrderedGroup_Ocomm__monoid__add(tc_nat) % 0.09/0.37 % 377:1:0:INP:: -> class_Ring__and__Field_Osemiring__1(tc_nat) % 0.09/0.37 % 378:1:0:INP:: -> class_Ring__and__Field_Omult__zero(tc_nat) % 0.09/0.37 % 379:1:0:INP:: -> class_Ring__and__Field_Osemiring(tc_nat) % 0.09/0.37 % 380:1:0:INP:: -> class_OrderedGroup_Omonoid__add(tc_nat) % 0.09/0.37 % 381:1:0:INP:: -> class_Nat_Osemiring__char__0(tc_nat) % 0.09/0.37 % 382:1:0:INP:: -> class_Orderings_Opreorder(tc_nat) % 0.09/0.37 % 383:1:0:INP:: -> class_Orderings_Olinorder(tc_nat) % 0.09/0.37 % 384:1:0:INP:: -> class_Orderings_Oorder(tc_nat) % 0.09/0.37 % 0.09/0.37 % Predicates: class_Ring__and__Field_Ocomm__semiring__1 = class_OrderedGroup_Olordered__ab__group__add class_OrderedGroup_Ogroup__add class_Ring__and__Field_Oidom class_Int_Onumber__ring class_Ring__and__Field_Oring c_HOL_Oord__class_Oless class_OrderedGroup_Ocomm__monoid__add class_Nat_Osemiring__char__0 class_OrderedGroup_Oab__group__add class_Ring__and__Field_Opordered__ring class_Ring__and__Field_Oring__no__zero__divisors class_Ring__and__Field_Ono__zero__divisors class_OrderedGroup_Oab__semigroup__add class_Ring__and__Field_Osemiring class_Ring__and__Field_Osemiring__1 class_OrderedGroup_Opordered__comm__monoid__add class_Ring__and__Field_Oordered__ring__strict class_OrderedGroup_Ocancel__ab__semigroup__add class_OrderedGroup_Ocancel__semigroup__add class_Ring__and__Field_Oordered__semidom class_Ring__and__Field_Oordered__semiring__strict class_Ring__and__Field_Oordered__comm__semiring__strict class_OrderedGroup_Omonoid__add class_Ring__and__Field_Oordered__idom class_Ring__and__Field_Omult__zero class_OrderedGroup_Opordered__cancel__ab__semigroup__add class_OrderedGroup_Opordered__ab__group__add class_OrderedGroup_Oab__semigroup__idem__mult class_OrderedGroup_Opordered__ab__semigroup__add__imp__le class_OrderedGroup_Oab__semigroup__mult class_Ring__and__Field_Ocomm__semiring class_Orderings_Opreorder class_Orderings_Olinorder class_Orderings_Oorder c_Lambda_Obeta c_InductTermi_OIT % 0.09/0.37 % Fol Constants: tc_nat v_s____ v_ta____ % 0.09/0.37 % Fol Functions: c_HOL_Otimes__class_Otimes c_HOL_Ozero__class_Ozero c_HOL_Oplus__class_Oplus c_HOL_Ominus__class_Ominus c_Suc c_Nat_Osemiring__1__class_Oof__nat c_Lambda_Oliftn c_Lambda_OdB_OVar c_ATP__Linkup_Osko__Nat__Xless__Suc__eq__0__disj__1__1 c_ATP__Linkup_Osko__Nat__Xgr0__implies__Suc__1__1 c_ATP__Linkup_Osko__Nat__Xgr0__conv__Suc__1__1 c_Lambda_OdB_OAbs c_Lambda_Osko__Lambda__Xbeta__cases__2__1 c_Lambda_Osubstn c_Lambda_Olift c_Lambda_Osubst c_Lambda_OdB_OApp % 0.09/0.37 % Problem Properties: % 0.09/0.37 % This is a full first-order problem with equality. The Problem is non-linear. % 0.09/0.37 % 0.09/0.37 % 0.09/0.37 % SZS status GaveUp % 0.09/0.37 % 0.09/0.37 % SPASS beiseite: SPASS does currently not support equality problems. % 0.09/0.37 % Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.09/0.37 % 0.09/0.37 % SPASS-SCL-FOL Statistics: % 0.09/0.37 % Number of learned clauses: 0 % 0.09/0.37 % Number of propagations: 0 % 0.09/0.37 % Number of decisions: 0 % 0.09/0.37 % Number of resolutions: 0 % 0.09/0.37 % Number of condensations: 0 % 0.09/0.37 % Number of sub resolutions: 0 %------------------------------------------------------------------------------