%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM216_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 06:18:11 PM UTC 2026 % Result : Theorem 213.40s 213.63s % Output : Proof 214.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM216_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : duper %s % 0.16/0.34 % Computer : n020.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon May 4 18:56:49 EDT 2026 % 0.16/0.34 % CPUTime : % 213.40/213.63 SZS status Theorem for theBenchmark.p % 213.40/213.63 SZS output start Proof for theBenchmark.p % 213.40/213.63 Clause #13 (by assumption #[]): Eq (∀ (VTerm0 VTerm1 VTerm2 : vTerm), Ne vFalse (vIfelse VTerm0 VTerm1 VTerm2)) True % 213.40/213.63 Clause #15 (by assumption #[]): Eq (∀ (VTerm0 : vTerm), Ne vFalse (vSucc VTerm0)) True % 213.40/213.63 Clause #16 (by assumption #[]): Eq (∀ (VTerm0 : vTerm), Ne vFalse (vPred VTerm0)) True % 213.40/213.63 Clause #17 (by assumption #[]): Eq (∀ (VTerm0 : vTerm), Ne vFalse (vIszero VTerm0)) True % 213.40/213.63 Clause #18 (by assumption #[]): Eq (∀ (VTerm0 VTerm1 : vTerm), Ne vFalse (vPlus VTerm0 VTerm1)) True % 213.40/213.63 Clause #36 (by assumption #[]): Eq (∀ (VTerm0 : vTerm), Ne vnoTerm (vsomeTerm VTerm0)) True % 213.40/213.63 Clause #81 (by assumption #[]): Eq % 213.40/213.63 (∀ (VwildcardName0 : vTerm), % 213.40/213.63 And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And (∀ (Vt20 Vt30 : vTerm), Ne VwildcardName0 (vIfelse vTrue Vt20 Vt30)) % 213.40/213.63 (∀ (Vt20 Vt30 : vTerm), Ne VwildcardName0 (vIfelse vFalse Vt20 Vt30))) % 213.40/213.63 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne VwildcardName0 (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.63 (∀ (Vt10 : vTerm), Ne VwildcardName0 (vSucc Vt10))) % 213.40/213.63 (Ne VwildcardName0 (vPred vZero))) % 213.40/213.63 (∀ (Vnv0 : vTerm), Ne VwildcardName0 (vPred (vSucc Vnv0)))) % 213.40/213.63 (∀ (Vt10 : vTerm), Ne VwildcardName0 (vPred Vt10))) % 213.40/213.63 (Ne VwildcardName0 (vIszero vZero))) % 213.40/213.63 (∀ (Vnv0 : vTerm), Ne VwildcardName0 (vIszero (vSucc Vnv0)))) % 213.40/213.63 (∀ (Vt10 : vTerm), Ne VwildcardName0 (vIszero Vt10))) % 213.40/213.63 (∀ (Vt10 Vt20 : vTerm), Ne VwildcardName0 (vPlus Vt10 Vt20)) → % 213.40/213.63 Eq (vreduce VwildcardName0) vnoTerm) % 213.40/213.63 True % 213.40/213.63 Clause #104 (by assumption #[]): Eq % 213.40/213.63 (Not % 213.40/213.63 (∀ (VT : vTy) (Vtres : vTerm), % 213.40/213.63 And (vptchecksimple vFalse VT) (Eq (vreduce vFalse) (vsomeTerm Vtres)) → vptchecksimple Vtres VT)) % 213.40/213.63 True % 213.40/213.63 Clause #223 (by clausification #[36]): ∀ (a : vTerm), Eq (Ne vnoTerm (vsomeTerm a)) True % 213.40/213.63 Clause #224 (by clausification #[223]): ∀ (a : vTerm), Ne vnoTerm (vsomeTerm a) % 213.40/213.63 Clause #272 (by clausification #[15]): ∀ (a : vTerm), Eq (Ne vFalse (vSucc a)) True % 213.40/213.63 Clause #273 (by clausification #[272]): ∀ (a : vTerm), Ne vFalse (vSucc a) % 213.40/213.63 Clause #298 (by clausification #[17]): ∀ (a : vTerm), Eq (Ne vFalse (vIszero a)) True % 213.40/213.63 Clause #299 (by clausification #[298]): ∀ (a : vTerm), Ne vFalse (vIszero a) % 213.40/213.63 Clause #301 (by clausification #[16]): ∀ (a : vTerm), Eq (Ne vFalse (vPred a)) True % 213.40/213.63 Clause #302 (by clausification #[301]): ∀ (a : vTerm), Ne vFalse (vPred a) % 213.40/213.63 Clause #355 (by clausification #[13]): ∀ (a : vTerm), Eq (∀ (VTerm1 VTerm2 : vTerm), Ne vFalse (vIfelse a VTerm1 VTerm2)) True % 213.40/213.63 Clause #356 (by clausification #[355]): ∀ (a a_1 : vTerm), Eq (∀ (VTerm2 : vTerm), Ne vFalse (vIfelse a a_1 VTerm2)) True % 213.40/213.63 Clause #357 (by clausification #[356]): ∀ (a a_1 a_2 : vTerm), Eq (Ne vFalse (vIfelse a a_1 a_2)) True % 213.40/213.63 Clause #358 (by clausification #[357]): ∀ (a a_1 a_2 : vTerm), Ne vFalse (vIfelse a a_1 a_2) % 213.40/213.63 Clause #362 (by clausification #[81]): ∀ (a : vTerm), % 213.40/213.63 Eq % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And % 213.40/213.63 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.63 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.63 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.63 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.63 (Ne a (vPred vZero))) % 213.40/213.63 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.63 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.63 (Ne a (vIszero vZero))) % 213.40/213.63 (∀ (Vnv0 : vTerm), Ne a (vIszero (vSucc Vnv0)))) % 213.40/213.63 (∀ (Vt10 : vTerm), Ne a (vIszero Vt10))) % 213.40/213.63 (∀ (Vt10 Vt20 : vTerm), Ne a (vPlus Vt10 Vt20)) → % 213.40/213.63 Eq (vreduce a) vnoTerm) % 213.40/213.63 True % 213.40/213.63 Clause #363 (by clausification #[362]): ∀ (a : vTerm), % 213.40/213.64 Or % 213.40/213.64 (Eq % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.64 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.64 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.64 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.64 (Ne a (vPred vZero))) % 213.40/213.64 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.64 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.64 (Ne a (vIszero vZero))) % 213.40/213.64 (∀ (Vnv0 : vTerm), Ne a (vIszero (vSucc Vnv0)))) % 213.40/213.64 (∀ (Vt10 : vTerm), Ne a (vIszero Vt10))) % 213.40/213.64 (∀ (Vt10 Vt20 : vTerm), Ne a (vPlus Vt10 Vt20))) % 213.40/213.64 False) % 213.40/213.64 (Eq (Eq (vreduce a) vnoTerm) True) % 213.40/213.64 Clause #364 (by clausification #[363]): ∀ (a : vTerm), % 213.40/213.64 Or (Eq (Eq (vreduce a) vnoTerm) True) % 213.40/213.64 (Or % 213.40/213.64 (Eq % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.64 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.64 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.64 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.64 (Ne a (vPred vZero))) % 213.40/213.64 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.64 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.64 (Ne a (vIszero vZero))) % 213.40/213.64 (∀ (Vnv0 : vTerm), Ne a (vIszero (vSucc Vnv0)))) % 213.40/213.64 (∀ (Vt10 : vTerm), Ne a (vIszero Vt10))) % 213.40/213.64 False) % 213.40/213.64 (Eq (∀ (Vt10 Vt20 : vTerm), Ne a (vPlus Vt10 Vt20)) False)) % 213.40/213.64 Clause #365 (by clausification #[364]): ∀ (a : vTerm), % 213.40/213.64 Or % 213.40/213.64 (Eq % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.64 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.64 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.64 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.64 (Ne a (vPred vZero))) % 213.40/213.64 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.64 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.64 (Ne a (vIszero vZero))) % 213.40/213.64 (∀ (Vnv0 : vTerm), Ne a (vIszero (vSucc Vnv0)))) % 213.40/213.64 (∀ (Vt10 : vTerm), Ne a (vIszero Vt10))) % 213.40/213.64 False) % 213.40/213.64 (Or (Eq (∀ (Vt10 Vt20 : vTerm), Ne a (vPlus Vt10 Vt20)) False) (Eq (vreduce a) vnoTerm)) % 213.40/213.64 Clause #366 (by clausification #[365]): ∀ (a : vTerm), % 213.40/213.64 Or (Eq (∀ (Vt10 Vt20 : vTerm), Ne a (vPlus Vt10 Vt20)) False) % 213.40/213.64 (Or (Eq (vreduce a) vnoTerm) % 213.40/213.64 (Or % 213.40/213.64 (Eq % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.64 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.64 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.64 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.64 (Ne a (vPred vZero))) % 213.40/213.64 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.64 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.64 (Ne a (vIszero vZero))) % 213.40/213.64 (∀ (Vnv0 : vTerm), Ne a (vIszero (vSucc Vnv0)))) % 213.40/213.64 False) % 213.40/213.64 (Eq (∀ (Vt10 : vTerm), Ne a (vIszero Vt10)) False))) % 213.40/213.64 Clause #367 (by clausification #[366]): ∀ (a a_1 : vTerm), % 213.40/213.64 Or (Eq (vreduce a) vnoTerm) % 213.40/213.64 (Or % 213.40/213.64 (Eq % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.64 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.66 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.66 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.66 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.66 (Ne a (vPred vZero))) % 213.40/213.66 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.66 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.66 (Ne a (vIszero vZero))) % 213.40/213.66 (∀ (Vnv0 : vTerm), Ne a (vIszero (vSucc Vnv0)))) % 213.40/213.66 False) % 213.40/213.66 (Or (Eq (∀ (Vt10 : vTerm), Ne a (vIszero Vt10)) False) % 213.40/213.66 (Eq (Not (∀ (Vt20 : vTerm), Ne a (vPlus (skS.0 9 a a_1) Vt20))) True))) % 213.40/213.66 Clause #368 (by clausification #[367]): ∀ (a a_1 : vTerm), % 213.40/213.66 Or (Eq (vreduce a) vnoTerm) % 213.40/213.66 (Or (Eq (∀ (Vt10 : vTerm), Ne a (vIszero Vt10)) False) % 213.40/213.66 (Or (Eq (Not (∀ (Vt20 : vTerm), Ne a (vPlus (skS.0 9 a a_1) Vt20))) True) % 213.40/213.66 (Or % 213.40/213.66 (Eq % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.66 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.66 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.66 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.66 (Ne a (vPred vZero))) % 213.40/213.66 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.66 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.66 (Ne a (vIszero vZero))) % 213.40/213.66 False) % 213.40/213.66 (Eq (∀ (Vnv0 : vTerm), Ne a (vIszero (vSucc Vnv0))) False)))) % 213.40/213.66 Clause #369 (by clausification #[368]): ∀ (a a_1 a_2 : vTerm), % 213.40/213.66 Or (Eq (vreduce a) vnoTerm) % 213.40/213.66 (Or (Eq (Not (∀ (Vt20 : vTerm), Ne a (vPlus (skS.0 9 a a_1) Vt20))) True) % 213.40/213.66 (Or % 213.40/213.66 (Eq % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.66 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.66 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.66 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.66 (Ne a (vPred vZero))) % 213.40/213.66 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.66 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.66 (Ne a (vIszero vZero))) % 213.40/213.66 False) % 213.40/213.66 (Or (Eq (∀ (Vnv0 : vTerm), Ne a (vIszero (vSucc Vnv0))) False) % 213.40/213.66 (Eq (Not (Ne a (vIszero (skS.0 10 a a_2)))) True)))) % 213.40/213.66 Clause #370 (by clausification #[369]): ∀ (a a_1 a_2 : vTerm), % 213.40/213.66 Or (Eq (vreduce a) vnoTerm) % 213.40/213.66 (Or % 213.40/213.66 (Eq % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And % 213.40/213.66 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.66 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.66 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.66 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.66 (Ne a (vPred vZero))) % 213.40/213.66 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.66 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.66 (Ne a (vIszero vZero))) % 213.40/213.66 False) % 213.40/213.66 (Or (Eq (∀ (Vnv0 : vTerm), Ne a (vIszero (vSucc Vnv0))) False) % 213.40/213.66 (Or (Eq (Not (Ne a (vIszero (skS.0 10 a a_1)))) True) % 213.40/213.66 (Eq (∀ (Vt20 : vTerm), Ne a (vPlus (skS.0 9 a a_2) Vt20)) False)))) % 213.40/213.66 Clause #371 (by clausification #[370]): ∀ (a a_1 a_2 : vTerm), % 213.40/213.66 Or (Eq (vreduce a) vnoTerm) % 213.40/213.66 (Or (Eq (∀ (Vnv0 : vTerm), Ne a (vIszero (vSucc Vnv0))) False) % 213.40/213.66 (Or (Eq (Not (Ne a (vIszero (skS.0 10 a a_1)))) True) % 213.40/213.66 (Or (Eq (∀ (Vt20 : vTerm), Ne a (vPlus (skS.0 9 a a_2) Vt20)) False) % 213.40/213.66 (Or % 213.40/213.66 (Eq % 213.40/213.66 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.68 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.68 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.68 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.68 (Ne a (vPred vZero))) % 213.40/213.68 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.68 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.68 False) % 213.40/213.68 (Eq (Ne a (vIszero vZero)) False))))) % 213.40/213.68 Clause #372 (by clausification #[371]): ∀ (a a_1 a_2 a_3 : vTerm), % 213.40/213.68 Or (Eq (vreduce a) vnoTerm) % 213.40/213.68 (Or (Eq (Not (Ne a (vIszero (skS.0 10 a a_1)))) True) % 213.40/213.68 (Or (Eq (∀ (Vt20 : vTerm), Ne a (vPlus (skS.0 9 a a_2) Vt20)) False) % 213.40/213.68 (Or % 213.40/213.68 (Eq % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.68 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.68 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.68 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.68 (Ne a (vPred vZero))) % 213.40/213.68 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.68 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.68 False) % 213.40/213.68 (Or (Eq (Ne a (vIszero vZero)) False) (Eq (Not (Ne a (vIszero (vSucc (skS.0 11 a a_3))))) True))))) % 213.40/213.68 Clause #373 (by clausification #[372]): ∀ (a a_1 a_2 a_3 : vTerm), % 213.40/213.68 Or (Eq (vreduce a) vnoTerm) % 213.40/213.68 (Or (Eq (∀ (Vt20 : vTerm), Ne a (vPlus (skS.0 9 a a_1) Vt20)) False) % 213.40/213.68 (Or % 213.40/213.68 (Eq % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.68 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.68 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.68 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.68 (Ne a (vPred vZero))) % 213.40/213.68 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.68 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.68 False) % 213.40/213.68 (Or (Eq (Ne a (vIszero vZero)) False) % 213.40/213.68 (Or (Eq (Not (Ne a (vIszero (vSucc (skS.0 11 a a_2))))) True) (Eq (Ne a (vIszero (skS.0 10 a a_3))) False))))) % 213.40/213.68 Clause #374 (by clausification #[373]): ∀ (a a_1 a_2 a_3 a_4 : vTerm), % 213.40/213.68 Or (Eq (vreduce a) vnoTerm) % 213.40/213.68 (Or % 213.40/213.68 (Eq % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.68 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.40/213.68 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.40/213.68 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.40/213.68 (Ne a (vPred vZero))) % 213.40/213.68 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.40/213.68 (∀ (Vt10 : vTerm), Ne a (vPred Vt10))) % 213.40/213.68 False) % 213.40/213.68 (Or (Eq (Ne a (vIszero vZero)) False) % 213.40/213.68 (Or (Eq (Not (Ne a (vIszero (vSucc (skS.0 11 a a_1))))) True) % 213.40/213.68 (Or (Eq (Ne a (vIszero (skS.0 10 a a_2))) False) % 213.40/213.68 (Eq (Not (Ne a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4)))) True))))) % 213.40/213.68 Clause #375 (by clausification #[374]): ∀ (a a_1 a_2 a_3 a_4 : vTerm), % 213.40/213.68 Or (Eq (vreduce a) vnoTerm) % 213.40/213.68 (Or (Eq (Ne a (vIszero vZero)) False) % 213.40/213.68 (Or (Eq (Not (Ne a (vIszero (vSucc (skS.0 11 a a_1))))) True) % 213.40/213.68 (Or (Eq (Ne a (vIszero (skS.0 10 a a_2))) False) % 213.40/213.68 (Or (Eq (Not (Ne a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4)))) True) % 213.40/213.68 (Or % 213.40/213.68 (Eq % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And % 213.40/213.68 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.40/213.68 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.70 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.70 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.50/213.70 (Ne a (vPred vZero))) % 213.50/213.70 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.50/213.70 False) % 213.50/213.70 (Eq (∀ (Vt10 : vTerm), Ne a (vPred Vt10)) False)))))) % 213.50/213.70 Clause #376 (by clausification #[375]): ∀ (a a_1 a_2 a_3 a_4 : vTerm), % 213.50/213.70 Or (Eq (vreduce a) vnoTerm) % 213.50/213.70 (Or (Eq (Not (Ne a (vIszero (vSucc (skS.0 11 a a_1))))) True) % 213.50/213.70 (Or (Eq (Ne a (vIszero (skS.0 10 a a_2))) False) % 213.50/213.70 (Or (Eq (Not (Ne a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4)))) True) % 213.50/213.70 (Or % 213.50/213.70 (Eq % 213.50/213.70 (And % 213.50/213.70 (And % 213.50/213.70 (And % 213.50/213.70 (And % 213.50/213.70 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.70 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.70 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.70 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.50/213.70 (Ne a (vPred vZero))) % 213.50/213.70 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.50/213.70 False) % 213.50/213.70 (Or (Eq (∀ (Vt10 : vTerm), Ne a (vPred Vt10)) False) (Eq a (vIszero vZero))))))) % 213.50/213.70 Clause #377 (by clausification #[376]): ∀ (a a_1 a_2 a_3 a_4 : vTerm), % 213.50/213.70 Or (Eq (vreduce a) vnoTerm) % 213.50/213.70 (Or (Eq (Ne a (vIszero (skS.0 10 a a_1))) False) % 213.50/213.70 (Or (Eq (Not (Ne a (vPlus (skS.0 9 a a_2) (skS.0 12 a a_2 a_3)))) True) % 213.50/213.70 (Or % 213.50/213.70 (Eq % 213.50/213.70 (And % 213.50/213.70 (And % 213.50/213.70 (And % 213.50/213.70 (And % 213.50/213.70 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.70 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.70 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.70 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.50/213.70 (Ne a (vPred vZero))) % 213.50/213.70 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.50/213.70 False) % 213.50/213.70 (Or (Eq (∀ (Vt10 : vTerm), Ne a (vPred Vt10)) False) % 213.50/213.70 (Or (Eq a (vIszero vZero)) (Eq (Ne a (vIszero (vSucc (skS.0 11 a a_4)))) False)))))) % 213.50/213.70 Clause #378 (by clausification #[377]): ∀ (a a_1 a_2 a_3 a_4 : vTerm), % 213.50/213.70 Or (Eq (vreduce a) vnoTerm) % 213.50/213.70 (Or (Eq (Not (Ne a (vPlus (skS.0 9 a a_1) (skS.0 12 a a_1 a_2)))) True) % 213.50/213.70 (Or % 213.50/213.70 (Eq % 213.50/213.70 (And % 213.50/213.70 (And % 213.50/213.70 (And % 213.50/213.70 (And % 213.50/213.70 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.70 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.70 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.70 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.50/213.70 (Ne a (vPred vZero))) % 213.50/213.70 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.50/213.70 False) % 213.50/213.70 (Or (Eq (∀ (Vt10 : vTerm), Ne a (vPred Vt10)) False) % 213.50/213.70 (Or (Eq a (vIszero vZero)) % 213.50/213.70 (Or (Eq (Ne a (vIszero (vSucc (skS.0 11 a a_3)))) False) (Eq a (vIszero (skS.0 10 a a_4)))))))) % 213.50/213.70 Clause #379 (by clausification #[378]): ∀ (a a_1 a_2 a_3 a_4 : vTerm), % 213.50/213.70 Or (Eq (vreduce a) vnoTerm) % 213.50/213.70 (Or % 213.50/213.70 (Eq % 213.50/213.70 (And % 213.50/213.70 (And % 213.50/213.70 (And % 213.50/213.70 (And % 213.50/213.70 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.70 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.70 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.70 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.50/213.70 (Ne a (vPred vZero))) % 213.50/213.70 (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0)))) % 213.50/213.70 False) % 213.50/213.70 (Or (Eq (∀ (Vt10 : vTerm), Ne a (vPred Vt10)) False) % 213.50/213.70 (Or (Eq a (vIszero vZero)) % 213.50/213.70 (Or (Eq (Ne a (vIszero (vSucc (skS.0 11 a a_1)))) False) % 213.50/213.70 (Or (Eq a (vIszero (skS.0 10 a a_2))) (Eq (Ne a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) False)))))) % 213.50/213.70 Clause #380 (by clausification #[379]): ∀ (a a_1 a_2 a_3 a_4 : vTerm), % 213.50/213.72 Or (Eq (vreduce a) vnoTerm) % 213.50/213.72 (Or (Eq (∀ (Vt10 : vTerm), Ne a (vPred Vt10)) False) % 213.50/213.72 (Or (Eq a (vIszero vZero)) % 213.50/213.72 (Or (Eq (Ne a (vIszero (vSucc (skS.0 11 a a_1)))) False) % 213.50/213.72 (Or (Eq a (vIszero (skS.0 10 a a_2))) % 213.50/213.72 (Or (Eq (Ne a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) False) % 213.50/213.72 (Or % 213.50/213.72 (Eq % 213.50/213.72 (And % 213.50/213.72 (And % 213.50/213.72 (And % 213.50/213.72 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.72 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.72 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.72 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.50/213.72 (Ne a (vPred vZero))) % 213.50/213.72 False) % 213.50/213.72 (Eq (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0))) False))))))) % 213.50/213.72 Clause #381 (by clausification #[380]): ∀ (a a_1 a_2 a_3 a_4 a_5 : vTerm), % 213.50/213.72 Or (Eq (vreduce a) vnoTerm) % 213.50/213.72 (Or (Eq a (vIszero vZero)) % 213.50/213.72 (Or (Eq (Ne a (vIszero (vSucc (skS.0 11 a a_1)))) False) % 213.50/213.72 (Or (Eq a (vIszero (skS.0 10 a a_2))) % 213.50/213.72 (Or (Eq (Ne a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) False) % 213.50/213.72 (Or % 213.50/213.72 (Eq % 213.50/213.72 (And % 213.50/213.72 (And % 213.50/213.72 (And % 213.50/213.72 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.72 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.72 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.72 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.50/213.72 (Ne a (vPred vZero))) % 213.50/213.72 False) % 213.50/213.72 (Or (Eq (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0))) False) % 213.50/213.72 (Eq (Not (Ne a (vPred (skS.0 13 a a_5)))) True))))))) % 213.50/213.72 Clause #382 (by clausification #[381]): ∀ (a a_1 a_2 a_3 a_4 a_5 : vTerm), % 213.50/213.72 Or (Eq (vreduce a) vnoTerm) % 213.50/213.72 (Or (Eq a (vIszero vZero)) % 213.50/213.72 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.72 (Or (Eq (Ne a (vPlus (skS.0 9 a a_2) (skS.0 12 a a_2 a_3))) False) % 213.50/213.72 (Or % 213.50/213.72 (Eq % 213.50/213.72 (And % 213.50/213.72 (And % 213.50/213.72 (And % 213.50/213.72 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.72 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.72 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.72 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.50/213.72 (Ne a (vPred vZero))) % 213.50/213.72 False) % 213.50/213.72 (Or (Eq (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0))) False) % 213.50/213.72 (Or (Eq (Not (Ne a (vPred (skS.0 13 a a_4)))) True) (Eq a (vIszero (vSucc (skS.0 11 a a_5)))))))))) % 213.50/213.72 Clause #383 (by clausification #[382]): ∀ (a a_1 a_2 a_3 a_4 a_5 : vTerm), % 213.50/213.72 Or (Eq (vreduce a) vnoTerm) % 213.50/213.72 (Or (Eq a (vIszero vZero)) % 213.50/213.72 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.72 (Or % 213.50/213.72 (Eq % 213.50/213.72 (And % 213.50/213.72 (And % 213.50/213.72 (And % 213.50/213.72 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.72 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.72 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.72 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.50/213.72 (Ne a (vPred vZero))) % 213.50/213.72 False) % 213.50/213.72 (Or (Eq (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0))) False) % 213.50/213.72 (Or (Eq (Not (Ne a (vPred (skS.0 13 a a_2)))) True) % 213.50/213.72 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_3)))) (Eq a (vPlus (skS.0 9 a a_4) (skS.0 12 a a_4 a_5))))))))) % 213.50/213.72 Clause #384 (by clausification #[383]): ∀ (a a_1 a_2 a_3 a_4 a_5 : vTerm), % 213.50/213.72 Or (Eq (vreduce a) vnoTerm) % 213.50/213.72 (Or (Eq a (vIszero vZero)) % 213.50/213.72 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.72 (Or (Eq (∀ (Vnv0 : vTerm), Ne a (vPred (vSucc Vnv0))) False) % 213.50/213.72 (Or (Eq (Not (Ne a (vPred (skS.0 13 a a_2)))) True) % 213.50/213.72 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_3)))) % 213.50/213.72 (Or (Eq a (vPlus (skS.0 9 a a_4) (skS.0 12 a a_4 a_5))) % 213.50/213.72 (Or % 213.50/213.74 (Eq % 213.50/213.74 (And % 213.50/213.74 (And % 213.50/213.74 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.74 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.74 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.74 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.50/213.74 False) % 213.50/213.74 (Eq (Ne a (vPred vZero)) False)))))))) % 213.50/213.74 Clause #385 (by clausification #[384]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : vTerm), % 213.50/213.74 Or (Eq (vreduce a) vnoTerm) % 213.50/213.74 (Or (Eq a (vIszero vZero)) % 213.50/213.74 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.74 (Or (Eq (Not (Ne a (vPred (skS.0 13 a a_2)))) True) % 213.50/213.74 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_3)))) % 213.50/213.74 (Or (Eq a (vPlus (skS.0 9 a a_4) (skS.0 12 a a_4 a_5))) % 213.50/213.74 (Or % 213.50/213.74 (Eq % 213.50/213.74 (And % 213.50/213.74 (And % 213.50/213.74 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.74 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.74 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.74 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.50/213.74 False) % 213.50/213.74 (Or (Eq (Ne a (vPred vZero)) False) (Eq (Not (Ne a (vPred (vSucc (skS.0 14 a a_6))))) True)))))))) % 213.50/213.74 Clause #386 (by clausification #[385]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : vTerm), % 213.50/213.74 Or (Eq (vreduce a) vnoTerm) % 213.50/213.74 (Or (Eq a (vIszero vZero)) % 213.50/213.74 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.74 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.74 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.74 (Or % 213.50/213.74 (Eq % 213.50/213.74 (And % 213.50/213.74 (And % 213.50/213.74 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.74 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.74 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.74 (∀ (Vt10 : vTerm), Ne a (vSucc Vt10))) % 213.50/213.74 False) % 213.50/213.74 (Or (Eq (Ne a (vPred vZero)) False) % 213.50/213.74 (Or (Eq (Not (Ne a (vPred (vSucc (skS.0 14 a a_5))))) True) % 213.50/213.74 (Eq (Ne a (vPred (skS.0 13 a a_6))) False)))))))) % 213.50/213.74 Clause #387 (by clausification #[386]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : vTerm), % 213.50/213.74 Or (Eq (vreduce a) vnoTerm) % 213.50/213.74 (Or (Eq a (vIszero vZero)) % 213.50/213.74 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.74 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.74 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.74 (Or (Eq (Ne a (vPred vZero)) False) % 213.50/213.74 (Or (Eq (Not (Ne a (vPred (vSucc (skS.0 14 a a_5))))) True) % 213.50/213.74 (Or (Eq (Ne a (vPred (skS.0 13 a a_6))) False) % 213.50/213.74 (Or % 213.50/213.74 (Eq % 213.50/213.74 (And % 213.50/213.74 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.74 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.74 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.74 False) % 213.50/213.74 (Eq (∀ (Vt10 : vTerm), Ne a (vSucc Vt10)) False))))))))) % 213.50/213.74 Clause #388 (by clausification #[387]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : vTerm), % 213.50/213.74 Or (Eq (vreduce a) vnoTerm) % 213.50/213.74 (Or (Eq a (vIszero vZero)) % 213.50/213.74 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.74 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.74 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.74 (Or (Eq (Not (Ne a (vPred (vSucc (skS.0 14 a a_5))))) True) % 213.50/213.74 (Or (Eq (Ne a (vPred (skS.0 13 a a_6))) False) % 213.50/213.74 (Or % 213.50/213.74 (Eq % 213.50/213.74 (And % 213.50/213.74 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.74 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.74 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.74 False) % 213.50/213.74 (Or (Eq (∀ (Vt10 : vTerm), Ne a (vSucc Vt10)) False) (Eq a (vPred vZero)))))))))) % 213.50/213.76 Clause #389 (by clausification #[388]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : vTerm), % 213.50/213.76 Or (Eq (vreduce a) vnoTerm) % 213.50/213.76 (Or (Eq a (vIszero vZero)) % 213.50/213.76 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.76 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.76 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.76 (Or (Eq (Ne a (vPred (skS.0 13 a a_5))) False) % 213.50/213.76 (Or % 213.50/213.76 (Eq % 213.50/213.76 (And % 213.50/213.76 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.76 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.76 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.76 False) % 213.50/213.76 (Or (Eq (∀ (Vt10 : vTerm), Ne a (vSucc Vt10)) False) % 213.50/213.76 (Or (Eq a (vPred vZero)) (Eq (Ne a (vPred (vSucc (skS.0 14 a a_6)))) False))))))))) % 213.50/213.76 Clause #390 (by clausification #[389]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : vTerm), % 213.50/213.76 Or (Eq (vreduce a) vnoTerm) % 213.50/213.76 (Or (Eq a (vIszero vZero)) % 213.50/213.76 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.76 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.76 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.76 (Or % 213.50/213.76 (Eq % 213.50/213.76 (And % 213.50/213.76 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.76 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.76 (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30))) % 213.50/213.76 False) % 213.50/213.76 (Or (Eq (∀ (Vt10 : vTerm), Ne a (vSucc Vt10)) False) % 213.50/213.76 (Or (Eq a (vPred vZero)) % 213.50/213.76 (Or (Eq (Ne a (vPred (vSucc (skS.0 14 a a_5)))) False) (Eq a (vPred (skS.0 13 a a_6))))))))))) % 213.50/213.76 Clause #391 (by clausification #[390]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : vTerm), % 213.50/213.76 Or (Eq (vreduce a) vnoTerm) % 213.50/213.76 (Or (Eq a (vIszero vZero)) % 213.50/213.76 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.76 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.76 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.76 (Or (Eq (∀ (Vt10 : vTerm), Ne a (vSucc Vt10)) False) % 213.50/213.76 (Or (Eq a (vPred vZero)) % 213.50/213.76 (Or (Eq (Ne a (vPred (vSucc (skS.0 14 a a_5)))) False) % 213.50/213.76 (Or (Eq a (vPred (skS.0 13 a a_6))) % 213.50/213.76 (Or % 213.50/213.76 (Eq % 213.50/213.76 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.76 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.76 False) % 213.50/213.76 (Eq (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30)) False)))))))))) % 213.50/213.76 Clause #392 (by clausification #[391]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : vTerm), % 213.50/213.76 Or (Eq (vreduce a) vnoTerm) % 213.50/213.76 (Or (Eq a (vIszero vZero)) % 213.50/213.76 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.76 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.76 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.76 (Or (Eq a (vPred vZero)) % 213.50/213.76 (Or (Eq (Ne a (vPred (vSucc (skS.0 14 a a_5)))) False) % 213.50/213.76 (Or (Eq a (vPred (skS.0 13 a a_6))) % 213.50/213.76 (Or % 213.50/213.76 (Eq % 213.50/213.76 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.76 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.76 False) % 213.50/213.76 (Or (Eq (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30)) False) % 213.50/213.76 (Eq (Not (Ne a (vSucc (skS.0 15 a a_7)))) True)))))))))) % 213.50/213.76 Clause #393 (by clausification #[392]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : vTerm), % 213.50/213.76 Or (Eq (vreduce a) vnoTerm) % 213.50/213.76 (Or (Eq a (vIszero vZero)) % 213.50/213.76 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.76 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.76 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.76 (Or (Eq a (vPred vZero)) % 213.50/213.76 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.50/213.76 (Or % 213.50/213.76 (Eq % 213.50/213.76 (And (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) % 213.50/213.76 (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30))) % 213.50/213.79 False) % 213.50/213.79 (Or (Eq (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30)) False) % 213.50/213.79 (Or (Eq (Not (Ne a (vSucc (skS.0 15 a a_6)))) True) (Eq a (vPred (vSucc (skS.0 14 a a_7))))))))))))) % 213.50/213.79 Clause #394 (by clausification #[393]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : vTerm), % 213.50/213.79 Or (Eq (vreduce a) vnoTerm) % 213.50/213.79 (Or (Eq a (vIszero vZero)) % 213.50/213.79 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.79 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.79 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.79 (Or (Eq a (vPred vZero)) % 213.50/213.79 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.50/213.79 (Or (Eq (∀ (Vt10 Vt20 Vt30 : vTerm), Ne a (vIfelse Vt10 Vt20 Vt30)) False) % 213.50/213.79 (Or (Eq (Not (Ne a (vSucc (skS.0 15 a a_6)))) True) % 213.50/213.79 (Or (Eq a (vPred (vSucc (skS.0 14 a a_7)))) % 213.50/213.79 (Or (Eq (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) False) % 213.50/213.79 (Eq (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30)) False))))))))))) % 213.50/213.79 Clause #395 (by clausification #[394]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : vTerm), % 213.50/213.79 Or (Eq (vreduce a) vnoTerm) % 213.50/213.79 (Or (Eq a (vIszero vZero)) % 213.50/213.79 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.79 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.79 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.79 (Or (Eq a (vPred vZero)) % 213.50/213.79 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.50/213.79 (Or (Eq (Not (Ne a (vSucc (skS.0 15 a a_6)))) True) % 213.50/213.79 (Or (Eq a (vPred (vSucc (skS.0 14 a a_7)))) % 213.50/213.79 (Or (Eq (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) False) % 213.50/213.79 (Or (Eq (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30)) False) % 213.50/213.79 (Eq (Not (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_8) Vt20 Vt30))) True))))))))))) % 213.50/213.79 Clause #396 (by clausification #[395]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : vTerm), % 213.50/213.79 Or (Eq (vreduce a) vnoTerm) % 213.50/213.79 (Or (Eq a (vIszero vZero)) % 213.50/213.79 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.79 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.79 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.79 (Or (Eq a (vPred vZero)) % 213.50/213.79 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.50/213.79 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.50/213.79 (Or (Eq (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vTrue Vt20 Vt30)) False) % 213.50/213.79 (Or (Eq (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30)) False) % 213.50/213.79 (Or (Eq (Not (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_7) Vt20 Vt30))) True) % 213.50/213.79 (Eq (Ne a (vSucc (skS.0 15 a a_8))) False))))))))))) % 213.50/213.79 Clause #397 (by clausification #[396]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : vTerm), % 213.50/213.79 Or (Eq (vreduce a) vnoTerm) % 213.50/213.79 (Or (Eq a (vIszero vZero)) % 213.50/213.79 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.79 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.79 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.79 (Or (Eq a (vPred vZero)) % 213.50/213.79 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.50/213.79 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.50/213.79 (Or (Eq (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse vFalse Vt20 Vt30)) False) % 213.50/213.79 (Or (Eq (Not (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_7) Vt20 Vt30))) True) % 213.50/213.79 (Or (Eq (Ne a (vSucc (skS.0 15 a a_8))) False) % 213.50/213.79 (Eq (Not (∀ (Vt30 : vTerm), Ne a (vIfelse vTrue (skS.0 17 a a_9) Vt30))) True))))))))))) % 213.50/213.79 Clause #398 (by clausification #[397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : vTerm), % 213.50/213.79 Or (Eq (vreduce a) vnoTerm) % 213.50/213.79 (Or (Eq a (vIszero vZero)) % 213.50/213.79 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.50/213.79 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.50/213.79 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.50/213.79 (Or (Eq a (vPred vZero)) % 213.50/213.79 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.50/213.79 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.81 (Or (Eq (Not (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_7) Vt20 Vt30))) True) % 213.60/213.81 (Or (Eq (Ne a (vSucc (skS.0 15 a a_8))) False) % 213.60/213.81 (Or (Eq (Not (∀ (Vt30 : vTerm), Ne a (vIfelse vTrue (skS.0 17 a a_9) Vt30))) True) % 213.60/213.81 (Eq (Not (∀ (Vt30 : vTerm), Ne a (vIfelse vFalse (skS.0 18 a a_10) Vt30))) True))))))))))) % 213.60/213.81 Clause #399 (by clausification #[398]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : vTerm), % 213.60/213.81 Or (Eq (vreduce a) vnoTerm) % 213.60/213.81 (Or (Eq a (vIszero vZero)) % 213.60/213.81 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.81 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.81 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.81 (Or (Eq a (vPred vZero)) % 213.60/213.81 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.81 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.81 (Or (Eq (Ne a (vSucc (skS.0 15 a a_7))) False) % 213.60/213.81 (Or (Eq (Not (∀ (Vt30 : vTerm), Ne a (vIfelse vTrue (skS.0 17 a a_8) Vt30))) True) % 213.60/213.81 (Or (Eq (Not (∀ (Vt30 : vTerm), Ne a (vIfelse vFalse (skS.0 18 a a_9) Vt30))) True) % 213.60/213.81 (Eq (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_10) Vt20 Vt30)) False))))))))))) % 213.60/213.81 Clause #400 (by clausification #[399]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : vTerm), % 213.60/213.81 Or (Eq (vreduce a) vnoTerm) % 213.60/213.81 (Or (Eq a (vIszero vZero)) % 213.60/213.81 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.81 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.81 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.81 (Or (Eq a (vPred vZero)) % 213.60/213.81 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.81 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.81 (Or (Eq (Not (∀ (Vt30 : vTerm), Ne a (vIfelse vTrue (skS.0 17 a a_7) Vt30))) True) % 213.60/213.81 (Or (Eq (Not (∀ (Vt30 : vTerm), Ne a (vIfelse vFalse (skS.0 18 a a_8) Vt30))) True) % 213.60/213.81 (Or (Eq (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_9) Vt20 Vt30)) False) % 213.60/213.81 (Eq a (vSucc (skS.0 15 a a_10))))))))))))) % 213.60/213.81 Clause #401 (by clausification #[400]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : vTerm), % 213.60/213.81 Or (Eq (vreduce a) vnoTerm) % 213.60/213.81 (Or (Eq a (vIszero vZero)) % 213.60/213.81 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.81 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.81 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.81 (Or (Eq a (vPred vZero)) % 213.60/213.81 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.81 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.81 (Or (Eq (Not (∀ (Vt30 : vTerm), Ne a (vIfelse vFalse (skS.0 18 a a_7) Vt30))) True) % 213.60/213.81 (Or (Eq (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_8) Vt20 Vt30)) False) % 213.60/213.81 (Or (Eq a (vSucc (skS.0 15 a a_9))) % 213.60/213.81 (Eq (∀ (Vt30 : vTerm), Ne a (vIfelse vTrue (skS.0 17 a a_10) Vt30)) False))))))))))) % 213.60/213.81 Clause #402 (by clausification #[401]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : vTerm), % 213.60/213.81 Or (Eq (vreduce a) vnoTerm) % 213.60/213.81 (Or (Eq a (vIszero vZero)) % 213.60/213.81 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.81 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.81 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.81 (Or (Eq a (vPred vZero)) % 213.60/213.81 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.81 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.81 (Or (Eq (∀ (Vt20 Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_7) Vt20 Vt30)) False) % 213.60/213.81 (Or (Eq a (vSucc (skS.0 15 a a_8))) % 213.60/213.81 (Or (Eq (∀ (Vt30 : vTerm), Ne a (vIfelse vTrue (skS.0 17 a a_9) Vt30)) False) % 213.60/213.81 (Eq (∀ (Vt30 : vTerm), Ne a (vIfelse vFalse (skS.0 18 a a_10) Vt30)) False))))))))))) % 213.60/213.81 Clause #403 (by clausification #[402]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : vTerm), % 213.60/213.81 Or (Eq (vreduce a) vnoTerm) % 213.60/213.81 (Or (Eq a (vIszero vZero)) % 213.60/213.81 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.81 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.81 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.84 (Or (Eq a (vPred vZero)) % 213.60/213.84 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.84 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.84 (Or (Eq a (vSucc (skS.0 15 a a_7))) % 213.60/213.84 (Or (Eq (∀ (Vt30 : vTerm), Ne a (vIfelse vTrue (skS.0 17 a a_8) Vt30)) False) % 213.60/213.84 (Or (Eq (∀ (Vt30 : vTerm), Ne a (vIfelse vFalse (skS.0 18 a a_9) Vt30)) False) % 213.60/213.84 (Eq (Not (∀ (Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_10) (skS.0 19 a a_10 a_11) Vt30))) % 213.60/213.84 True))))))))))) % 213.60/213.84 Clause #404 (by clausification #[403]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : vTerm), % 213.60/213.84 Or (Eq (vreduce a) vnoTerm) % 213.60/213.84 (Or (Eq a (vIszero vZero)) % 213.60/213.84 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.84 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.84 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.84 (Or (Eq a (vPred vZero)) % 213.60/213.84 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.84 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.84 (Or (Eq a (vSucc (skS.0 15 a a_7))) % 213.60/213.84 (Or (Eq (∀ (Vt30 : vTerm), Ne a (vIfelse vFalse (skS.0 18 a a_8) Vt30)) False) % 213.60/213.84 (Or (Eq (Not (∀ (Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_9) (skS.0 19 a a_9 a_10) Vt30))) True) % 213.60/213.84 (Eq (Not (Ne a (vIfelse vTrue (skS.0 17 a a_11) (skS.0 20 a a_11 a_12)))) True))))))))))) % 213.60/213.84 Clause #405 (by clausification #[404]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : vTerm), % 213.60/213.84 Or (Eq (vreduce a) vnoTerm) % 213.60/213.84 (Or (Eq a (vIszero vZero)) % 213.60/213.84 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.84 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.84 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.84 (Or (Eq a (vPred vZero)) % 213.60/213.84 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.84 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.84 (Or (Eq a (vSucc (skS.0 15 a a_7))) % 213.60/213.84 (Or (Eq (Not (∀ (Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_8) (skS.0 19 a a_8 a_9) Vt30))) True) % 213.60/213.84 (Or (Eq (Not (Ne a (vIfelse vTrue (skS.0 17 a a_10) (skS.0 20 a a_10 a_11)))) True) % 213.60/213.84 (Eq (Not (Ne a (vIfelse vFalse (skS.0 18 a a_12) (skS.0 21 a a_12 a_13)))) True))))))))))) % 213.60/213.84 Clause #406 (by clausification #[405]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : vTerm), % 213.60/213.84 Or (Eq (vreduce a) vnoTerm) % 213.60/213.84 (Or (Eq a (vIszero vZero)) % 213.60/213.84 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.84 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.84 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.84 (Or (Eq a (vPred vZero)) % 213.60/213.84 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.84 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.84 (Or (Eq a (vSucc (skS.0 15 a a_7))) % 213.60/213.84 (Or (Eq (Not (Ne a (vIfelse vTrue (skS.0 17 a a_8) (skS.0 20 a a_8 a_9)))) True) % 213.60/213.84 (Or (Eq (Not (Ne a (vIfelse vFalse (skS.0 18 a a_10) (skS.0 21 a a_10 a_11)))) True) % 213.60/213.84 (Eq (∀ (Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_12) (skS.0 19 a a_12 a_13) Vt30)) % 213.60/213.84 False))))))))))) % 213.60/213.84 Clause #407 (by clausification #[406]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : vTerm), % 213.60/213.84 Or (Eq (vreduce a) vnoTerm) % 213.60/213.84 (Or (Eq a (vIszero vZero)) % 213.60/213.84 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.84 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.84 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.84 (Or (Eq a (vPred vZero)) % 213.60/213.84 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.84 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.84 (Or (Eq a (vSucc (skS.0 15 a a_7))) % 213.60/213.84 (Or (Eq (Not (Ne a (vIfelse vFalse (skS.0 18 a a_8) (skS.0 21 a a_8 a_9)))) True) % 213.60/213.84 (Or (Eq (∀ (Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_10) (skS.0 19 a a_10 a_11) Vt30)) False) % 213.60/213.84 (Eq (Ne a (vIfelse vTrue (skS.0 17 a a_12) (skS.0 20 a a_12 a_13))) False))))))))))) % 213.60/213.86 Clause #408 (by clausification #[407]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : vTerm), % 213.60/213.86 Or (Eq (vreduce a) vnoTerm) % 213.60/213.86 (Or (Eq a (vIszero vZero)) % 213.60/213.86 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.86 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.86 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.86 (Or (Eq a (vPred vZero)) % 213.60/213.86 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.86 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.86 (Or (Eq a (vSucc (skS.0 15 a a_7))) % 213.60/213.86 (Or (Eq (∀ (Vt30 : vTerm), Ne a (vIfelse (skS.0 16 a a_8) (skS.0 19 a a_8 a_9) Vt30)) False) % 213.60/213.86 (Or (Eq (Ne a (vIfelse vTrue (skS.0 17 a a_10) (skS.0 20 a a_10 a_11))) False) % 213.60/213.86 (Eq (Ne a (vIfelse vFalse (skS.0 18 a a_12) (skS.0 21 a a_12 a_13))) False))))))))))) % 213.60/213.86 Clause #409 (by clausification #[408]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 : vTerm), % 213.60/213.86 Or (Eq (vreduce a) vnoTerm) % 213.60/213.86 (Or (Eq a (vIszero vZero)) % 213.60/213.86 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.86 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.86 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.86 (Or (Eq a (vPred vZero)) % 213.60/213.86 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.86 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.86 (Or (Eq a (vSucc (skS.0 15 a a_7))) % 213.60/213.86 (Or (Eq (Ne a (vIfelse vTrue (skS.0 17 a a_8) (skS.0 20 a a_8 a_9))) False) % 213.60/213.86 (Or (Eq (Ne a (vIfelse vFalse (skS.0 18 a a_10) (skS.0 21 a a_10 a_11))) False) % 213.60/213.86 (Eq (Not (Ne a (vIfelse (skS.0 16 a a_12) (skS.0 19 a a_12 a_13) (skS.0 22 a a_12 a_13 a_14)))) % 213.60/213.86 True))))))))))) % 213.60/213.86 Clause #410 (by clausification #[409]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 : vTerm), % 213.60/213.86 Or (Eq (vreduce a) vnoTerm) % 213.60/213.86 (Or (Eq a (vIszero vZero)) % 213.60/213.86 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.86 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.86 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.86 (Or (Eq a (vPred vZero)) % 213.60/213.86 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.86 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.86 (Or (Eq a (vSucc (skS.0 15 a a_7))) % 213.60/213.86 (Or (Eq (Ne a (vIfelse vFalse (skS.0 18 a a_8) (skS.0 21 a a_8 a_9))) False) % 213.60/213.86 (Or % 213.60/213.86 (Eq (Not (Ne a (vIfelse (skS.0 16 a a_10) (skS.0 19 a a_10 a_11) (skS.0 22 a a_10 a_11 a_12)))) % 213.60/213.86 True) % 213.60/213.86 (Eq a (vIfelse vTrue (skS.0 17 a a_13) (skS.0 20 a a_13 a_14))))))))))))) % 213.60/213.86 Clause #411 (by clausification #[410]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 : vTerm), % 213.60/213.86 Or (Eq (vreduce a) vnoTerm) % 213.60/213.86 (Or (Eq a (vIszero vZero)) % 213.60/213.86 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.86 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.86 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.86 (Or (Eq a (vPred vZero)) % 213.60/213.86 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.86 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.86 (Or (Eq a (vSucc (skS.0 15 a a_7))) % 213.60/213.86 (Or (Eq (Not (Ne a (vIfelse (skS.0 16 a a_8) (skS.0 19 a a_8 a_9) (skS.0 22 a a_8 a_9 a_10)))) True) % 213.60/213.86 (Or (Eq a (vIfelse vTrue (skS.0 17 a a_11) (skS.0 20 a a_11 a_12))) % 213.60/213.86 (Eq a (vIfelse vFalse (skS.0 18 a a_13) (skS.0 21 a a_13 a_14))))))))))))) % 213.60/213.86 Clause #412 (by clausification #[411]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 : vTerm), % 213.60/213.86 Or (Eq (vreduce a) vnoTerm) % 213.60/213.86 (Or (Eq a (vIszero vZero)) % 213.60/213.86 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.86 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.86 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.86 (Or (Eq a (vPred vZero)) % 213.60/213.86 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.86 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.86 (Or (Eq a (vSucc (skS.0 15 a a_7))) % 213.60/213.89 (Or (Eq a (vIfelse vTrue (skS.0 17 a a_8) (skS.0 20 a a_8 a_9))) % 213.60/213.89 (Or (Eq a (vIfelse vFalse (skS.0 18 a a_10) (skS.0 21 a a_10 a_11))) % 213.60/213.89 (Eq (Ne a (vIfelse (skS.0 16 a a_12) (skS.0 19 a a_12 a_13) (skS.0 22 a a_12 a_13 a_14))) % 213.60/213.89 False))))))))))) % 213.60/213.89 Clause #413 (by clausification #[412]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 : vTerm), % 213.60/213.89 Or (Eq (vreduce a) vnoTerm) % 213.60/213.89 (Or (Eq a (vIszero vZero)) % 213.60/213.89 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.89 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.89 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.89 (Or (Eq a (vPred vZero)) % 213.60/213.89 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.89 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.89 (Or (Eq a (vSucc (skS.0 15 a a_7))) % 213.60/213.89 (Or (Eq a (vIfelse vTrue (skS.0 17 a a_8) (skS.0 20 a a_8 a_9))) % 213.60/213.89 (Or (Eq a (vIfelse vFalse (skS.0 18 a a_10) (skS.0 21 a a_10 a_11))) % 213.60/213.89 (Eq a (vIfelse (skS.0 16 a a_12) (skS.0 19 a a_12 a_13) (skS.0 22 a a_12 a_13 a_14))))))))))))) % 213.60/213.89 Clause #421 (by superposition #[413, 299]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 : vTerm), % 213.60/213.89 Or (Eq (vreduce a) vnoTerm) % 213.60/213.89 (Or (Eq a (vIszero (skS.0 10 a a_1))) % 213.60/213.89 (Or (Eq a (vIszero (vSucc (skS.0 11 a a_2)))) % 213.60/213.89 (Or (Eq a (vPlus (skS.0 9 a a_3) (skS.0 12 a a_3 a_4))) % 213.60/213.89 (Or (Eq a (vPred vZero)) % 213.60/213.89 (Or (Eq a (vPred (skS.0 13 a a_5))) % 213.60/213.89 (Or (Eq a (vPred (vSucc (skS.0 14 a a_6)))) % 213.60/213.89 (Or (Eq a (vSucc (skS.0 15 a a_7))) % 213.60/213.89 (Or (Eq a (vIfelse vTrue (skS.0 17 a a_8) (skS.0 20 a a_8 a_9))) % 213.60/213.89 (Or (Eq a (vIfelse vFalse (skS.0 18 a a_10) (skS.0 21 a a_10 a_11))) % 213.60/213.89 (Or (Eq a (vIfelse (skS.0 16 a a_12) (skS.0 19 a a_12 a_13) (skS.0 22 a a_12 a_13 a_14))) % 213.60/213.89 (Ne vFalse a))))))))))) % 213.60/213.89 Clause #513 (by clausification #[18]): ∀ (a : vTerm), Eq (∀ (VTerm1 : vTerm), Ne vFalse (vPlus a VTerm1)) True % 213.60/213.89 Clause #514 (by clausification #[513]): ∀ (a a_1 : vTerm), Eq (Ne vFalse (vPlus a a_1)) True % 213.60/213.89 Clause #515 (by clausification #[514]): ∀ (a a_1 : vTerm), Ne vFalse (vPlus a a_1) % 213.60/213.89 Clause #612 (by clausification #[104]): Eq % 213.60/213.89 (∀ (VT : vTy) (Vtres : vTerm), % 213.60/213.89 And (vptchecksimple vFalse VT) (Eq (vreduce vFalse) (vsomeTerm Vtres)) → vptchecksimple Vtres VT) % 213.60/213.89 False % 213.60/213.89 Clause #613 (by clausification #[612]): ∀ (a : vTy), % 213.60/213.89 Eq % 213.60/213.89 (Not % 213.60/213.89 (∀ (Vtres : vTerm), % 213.60/213.89 And (vptchecksimple vFalse (skS.0 23 a)) (Eq (vreduce vFalse) (vsomeTerm Vtres)) → % 213.60/213.89 vptchecksimple Vtres (skS.0 23 a))) % 213.60/213.89 True % 213.60/213.89 Clause #614 (by clausification #[613]): ∀ (a : vTy), % 213.60/213.89 Eq % 213.60/213.89 (∀ (Vtres : vTerm), % 213.60/213.89 And (vptchecksimple vFalse (skS.0 23 a)) (Eq (vreduce vFalse) (vsomeTerm Vtres)) → % 213.60/213.89 vptchecksimple Vtres (skS.0 23 a)) % 213.60/213.89 False % 213.60/213.89 Clause #615 (by clausification #[614]): ∀ (a : vTy) (a_1 : vTerm), % 213.60/213.89 Eq % 213.60/213.89 (Not % 213.60/213.89 (And (vptchecksimple vFalse (skS.0 23 a)) (Eq (vreduce vFalse) (vsomeTerm (skS.0 24 a a_1))) → % 213.60/213.89 vptchecksimple (skS.0 24 a a_1) (skS.0 23 a))) % 213.60/213.89 True % 213.60/213.89 Clause #616 (by clausification #[615]): ∀ (a : vTy) (a_1 : vTerm), % 213.60/213.89 Eq % 213.60/213.89 (And (vptchecksimple vFalse (skS.0 23 a)) (Eq (vreduce vFalse) (vsomeTerm (skS.0 24 a a_1))) → % 213.60/213.89 vptchecksimple (skS.0 24 a a_1) (skS.0 23 a)) % 213.60/213.89 False % 213.60/213.89 Clause #617 (by clausification #[616]): ∀ (a : vTy) (a_1 : vTerm), % 213.60/213.89 Eq (And (vptchecksimple vFalse (skS.0 23 a)) (Eq (vreduce vFalse) (vsomeTerm (skS.0 24 a a_1)))) True % 213.60/213.89 Clause #619 (by clausification #[617]): ∀ (a : vTy) (a_1 : vTerm), Eq (Eq (vreduce vFalse) (vsomeTerm (skS.0 24 a a_1))) True % 213.60/213.89 Clause #621 (by clausification #[619]): ∀ (a : vTy) (a_1 : vTerm), Eq (vreduce vFalse) (vsomeTerm (skS.0 24 a a_1)) % 213.60/213.89 Clause #623 (by superposition #[621, 224]): Ne vnoTerm (vreduce vFalse) % 213.60/213.89 Clause #20978 (by destructive equality resolution #[421]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : vTerm), % 213.70/213.91 Or (Eq (vreduce vFalse) vnoTerm) % 213.70/213.91 (Or (Eq vFalse (vIszero (skS.0 10 vFalse a))) % 213.70/213.91 (Or (Eq vFalse (vIszero (vSucc (skS.0 11 vFalse a_1)))) % 213.70/213.91 (Or (Eq vFalse (vPlus (skS.0 9 vFalse a_2) (skS.0 12 vFalse a_2 a_3))) % 213.70/213.91 (Or (Eq vFalse (vPred vZero)) % 213.70/213.91 (Or (Eq vFalse (vPred (skS.0 13 vFalse a_4))) % 213.70/213.91 (Or (Eq vFalse (vPred (vSucc (skS.0 14 vFalse a_5)))) % 213.70/213.91 (Or (Eq vFalse (vSucc (skS.0 15 vFalse a_6))) % 213.70/213.91 (Or (Eq vFalse (vIfelse vTrue (skS.0 17 vFalse a_7) (skS.0 20 vFalse a_7 a_8))) % 213.70/213.91 (Or (Eq vFalse (vIfelse vFalse (skS.0 18 vFalse a_9) (skS.0 21 vFalse a_9 a_10))) % 213.70/213.91 (Eq vFalse % 213.70/213.91 (vIfelse (skS.0 16 vFalse a_11) (skS.0 19 vFalse a_11 a_12) % 213.70/213.91 (skS.0 22 vFalse a_11 a_12 a_13)))))))))))) % 213.70/213.91 Clause #20979 (by forward contextual literal cutting #[20978, 623]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : vTerm), % 213.70/213.91 Or (Eq vFalse (vIszero (skS.0 10 vFalse a))) % 213.70/213.91 (Or (Eq vFalse (vIszero (vSucc (skS.0 11 vFalse a_1)))) % 213.70/213.91 (Or (Eq vFalse (vPlus (skS.0 9 vFalse a_2) (skS.0 12 vFalse a_2 a_3))) % 213.70/213.91 (Or (Eq vFalse (vPred vZero)) % 213.70/213.91 (Or (Eq vFalse (vPred (skS.0 13 vFalse a_4))) % 213.70/213.91 (Or (Eq vFalse (vPred (vSucc (skS.0 14 vFalse a_5)))) % 213.70/213.91 (Or (Eq vFalse (vSucc (skS.0 15 vFalse a_6))) % 213.70/213.91 (Or (Eq vFalse (vIfelse vTrue (skS.0 17 vFalse a_7) (skS.0 20 vFalse a_7 a_8))) % 213.70/213.91 (Or (Eq vFalse (vIfelse vFalse (skS.0 18 vFalse a_9) (skS.0 21 vFalse a_9 a_10))) % 213.70/213.91 (Eq vFalse % 213.70/213.91 (vIfelse (skS.0 16 vFalse a_11) (skS.0 19 vFalse a_11 a_12) % 213.70/213.91 (skS.0 22 vFalse a_11 a_12 a_13))))))))))) % 213.70/213.91 Clause #20980 (by forward contextual literal cutting #[20979, 299]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : vTerm), % 213.70/213.91 Or (Eq vFalse (vIszero (vSucc (skS.0 11 vFalse a)))) % 213.70/213.91 (Or (Eq vFalse (vPlus (skS.0 9 vFalse a_1) (skS.0 12 vFalse a_1 a_2))) % 213.70/213.91 (Or (Eq vFalse (vPred vZero)) % 213.70/213.91 (Or (Eq vFalse (vPred (skS.0 13 vFalse a_3))) % 213.70/213.91 (Or (Eq vFalse (vPred (vSucc (skS.0 14 vFalse a_4)))) % 213.70/213.91 (Or (Eq vFalse (vSucc (skS.0 15 vFalse a_5))) % 213.70/213.91 (Or (Eq vFalse (vIfelse vTrue (skS.0 17 vFalse a_6) (skS.0 20 vFalse a_6 a_7))) % 213.70/213.91 (Or (Eq vFalse (vIfelse vFalse (skS.0 18 vFalse a_8) (skS.0 21 vFalse a_8 a_9))) % 213.70/213.91 (Eq vFalse % 213.70/213.91 (vIfelse (skS.0 16 vFalse a_10) (skS.0 19 vFalse a_10 a_11) % 213.70/213.91 (skS.0 22 vFalse a_10 a_11 a_12)))))))))) % 213.70/213.91 Clause #20981 (by forward contextual literal cutting #[20980, 299]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : vTerm), % 213.70/213.91 Or (Eq vFalse (vPlus (skS.0 9 vFalse a) (skS.0 12 vFalse a a_1))) % 213.70/213.91 (Or (Eq vFalse (vPred vZero)) % 213.70/213.91 (Or (Eq vFalse (vPred (skS.0 13 vFalse a_2))) % 213.70/213.91 (Or (Eq vFalse (vPred (vSucc (skS.0 14 vFalse a_3)))) % 213.70/213.91 (Or (Eq vFalse (vSucc (skS.0 15 vFalse a_4))) % 213.70/213.91 (Or (Eq vFalse (vIfelse vTrue (skS.0 17 vFalse a_5) (skS.0 20 vFalse a_5 a_6))) % 213.70/213.91 (Or (Eq vFalse (vIfelse vFalse (skS.0 18 vFalse a_7) (skS.0 21 vFalse a_7 a_8))) % 213.70/213.91 (Eq vFalse % 213.70/213.91 (vIfelse (skS.0 16 vFalse a_9) (skS.0 19 vFalse a_9 a_10) (skS.0 22 vFalse a_9 a_10 a_11))))))))) % 213.70/213.91 Clause #20982 (by forward contextual literal cutting #[20981, 515]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : vTerm), % 213.70/213.91 Or (Eq vFalse (vPred vZero)) % 213.70/213.91 (Or (Eq vFalse (vPred (skS.0 13 vFalse a))) % 213.70/213.91 (Or (Eq vFalse (vPred (vSucc (skS.0 14 vFalse a_1)))) % 213.70/213.91 (Or (Eq vFalse (vSucc (skS.0 15 vFalse a_2))) % 213.70/213.91 (Or (Eq vFalse (vIfelse vTrue (skS.0 17 vFalse a_3) (skS.0 20 vFalse a_3 a_4))) % 213.70/213.91 (Or (Eq vFalse (vIfelse vFalse (skS.0 18 vFalse a_5) (skS.0 21 vFalse a_5 a_6))) % 213.70/213.91 (Eq vFalse (vIfelse (skS.0 16 vFalse a_7) (skS.0 19 vFalse a_7 a_8) (skS.0 22 vFalse a_7 a_8 a_9)))))))) % 213.70/213.91 Clause #20983 (by forward contextual literal cutting #[20982, 302]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : vTerm), % 213.70/213.91 Or (Eq vFalse (vPred (skS.0 13 vFalse a))) % 214.01/214.26 (Or (Eq vFalse (vPred (vSucc (skS.0 14 vFalse a_1)))) % 214.01/214.26 (Or (Eq vFalse (vSucc (skS.0 15 vFalse a_2))) % 214.01/214.26 (Or (Eq vFalse (vIfelse vTrue (skS.0 17 vFalse a_3) (skS.0 20 vFalse a_3 a_4))) % 214.01/214.26 (Or (Eq vFalse (vIfelse vFalse (skS.0 18 vFalse a_5) (skS.0 21 vFalse a_5 a_6))) % 214.01/214.26 (Eq vFalse (vIfelse (skS.0 16 vFalse a_7) (skS.0 19 vFalse a_7 a_8) (skS.0 22 vFalse a_7 a_8 a_9))))))) % 214.01/214.26 Clause #20984 (by forward contextual literal cutting #[20983, 302]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : vTerm), % 214.01/214.26 Or (Eq vFalse (vPred (vSucc (skS.0 14 vFalse a)))) % 214.01/214.26 (Or (Eq vFalse (vSucc (skS.0 15 vFalse a_1))) % 214.01/214.26 (Or (Eq vFalse (vIfelse vTrue (skS.0 17 vFalse a_2) (skS.0 20 vFalse a_2 a_3))) % 214.01/214.26 (Or (Eq vFalse (vIfelse vFalse (skS.0 18 vFalse a_4) (skS.0 21 vFalse a_4 a_5))) % 214.01/214.26 (Eq vFalse (vIfelse (skS.0 16 vFalse a_6) (skS.0 19 vFalse a_6 a_7) (skS.0 22 vFalse a_6 a_7 a_8)))))) % 214.01/214.26 Clause #20985 (by forward contextual literal cutting #[20984, 302]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : vTerm), % 214.01/214.26 Or (Eq vFalse (vSucc (skS.0 15 vFalse a))) % 214.01/214.26 (Or (Eq vFalse (vIfelse vTrue (skS.0 17 vFalse a_1) (skS.0 20 vFalse a_1 a_2))) % 214.01/214.26 (Or (Eq vFalse (vIfelse vFalse (skS.0 18 vFalse a_3) (skS.0 21 vFalse a_3 a_4))) % 214.01/214.26 (Eq vFalse (vIfelse (skS.0 16 vFalse a_5) (skS.0 19 vFalse a_5 a_6) (skS.0 22 vFalse a_5 a_6 a_7))))) % 214.01/214.26 Clause #20986 (by forward contextual literal cutting #[20985, 273]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : vTerm), % 214.01/214.26 Or (Eq vFalse (vIfelse vTrue (skS.0 17 vFalse a) (skS.0 20 vFalse a a_1))) % 214.01/214.26 (Or (Eq vFalse (vIfelse vFalse (skS.0 18 vFalse a_2) (skS.0 21 vFalse a_2 a_3))) % 214.01/214.26 (Eq vFalse (vIfelse (skS.0 16 vFalse a_4) (skS.0 19 vFalse a_4 a_5) (skS.0 22 vFalse a_4 a_5 a_6)))) % 214.01/214.26 Clause #20987 (by forward contextual literal cutting #[20986, 358]): ∀ (a a_1 a_2 a_3 a_4 : vTerm), % 214.01/214.26 Or (Eq vFalse (vIfelse vFalse (skS.0 18 vFalse a) (skS.0 21 vFalse a a_1))) % 214.01/214.26 (Eq vFalse (vIfelse (skS.0 16 vFalse a_2) (skS.0 19 vFalse a_2 a_3) (skS.0 22 vFalse a_2 a_3 a_4))) % 214.01/214.26 Clause #20988 (by forward contextual literal cutting #[20987, 358]): ∀ (a a_1 a_2 : vTerm), Eq vFalse (vIfelse (skS.0 16 vFalse a) (skS.0 19 vFalse a a_1) (skS.0 22 vFalse a a_1 a_2)) % 214.01/214.26 Clause #20989 (by forward contextual literal cutting #[20988, 358]): False % 214.01/214.26 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------