%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO091^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n028.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 : Fri Oct 3 08:08:34 PM UTC 2025 % Result : Theorem 6.84s 7.00s % Output : Proof 7.04s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYO091^5 : TPTP v9.2.0. Released v4.0.0. % 0.06/0.13 % Command : duper %s % 0.13/0.33 % Computer : n028.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Fri Oct 3 14:16:53 EDT 2025 % 0.13/0.33 % CPUTime : % 6.84/7.00 SZS status Theorem for theBenchmark.p % 6.84/7.00 SZS output start Proof for theBenchmark.p % 6.84/7.00 Clause #0 (by assumption #[]): Eq (Not (∀ (P Q R : Prop), Iff (Iff (Iff P Q) R) (Iff P (Iff Q R)))) True % 6.84/7.00 Clause #1 (by clausification #[0]): Eq (∀ (P Q R : Prop), Iff (Iff (Iff P Q) R) (Iff P (Iff Q R))) False % 6.84/7.00 Clause #2 (by clausification #[1]): ∀ (a : Prop), Eq (Not (∀ (Q R : Prop), Iff (Iff (Iff (skS.0 0 a) Q) R) (Iff (skS.0 0 a) (Iff Q R)))) True % 6.84/7.00 Clause #3 (by clausification #[2]): ∀ (a : Prop), Eq (∀ (Q R : Prop), Iff (Iff (Iff (skS.0 0 a) Q) R) (Iff (skS.0 0 a) (Iff Q R))) False % 6.84/7.00 Clause #4 (by clausification #[3]): ∀ (a a_1 : Prop), % 6.84/7.00 Eq (Not (∀ (R : Prop), Iff (Iff (Iff (skS.0 0 a) (skS.0 1 a a_1)) R) (Iff (skS.0 0 a) (Iff (skS.0 1 a a_1) R)))) True % 6.84/7.00 Clause #5 (by clausification #[4]): ∀ (a a_1 : Prop), % 6.84/7.00 Eq (∀ (R : Prop), Iff (Iff (Iff (skS.0 0 a) (skS.0 1 a a_1)) R) (Iff (skS.0 0 a) (Iff (skS.0 1 a a_1) R))) False % 6.84/7.00 Clause #6 (by clausification #[5]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Eq % 6.84/7.00 (Not % 6.84/7.00 (Iff (Iff (Iff (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 2 a a_1 a_2)) % 6.84/7.00 (Iff (skS.0 0 a) (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))))) % 6.84/7.00 True % 6.84/7.00 Clause #7 (by clausification #[6]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Eq % 6.84/7.00 (Iff (Iff (Iff (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 2 a a_1 a_2)) % 6.84/7.00 (Iff (skS.0 0 a) (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 6.84/7.00 False % 6.84/7.00 Clause #8 (by clausification #[7]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Or (Eq (Iff (Iff (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 2 a a_1 a_2)) False) % 6.84/7.00 (Eq (Iff (skS.0 0 a) (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) False) % 6.84/7.00 Clause #9 (by clausification #[7]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Or (Eq (Iff (Iff (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 2 a a_1 a_2)) True) % 6.84/7.00 (Eq (Iff (skS.0 0 a) (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) True) % 6.84/7.00 Clause #10 (by clausification #[8]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Or (Eq (Iff (skS.0 0 a) (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) False) % 6.84/7.00 (Or (Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) False) (Eq (skS.0 2 a a_1 a_2) False)) % 6.84/7.00 Clause #11 (by clausification #[8]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Or (Eq (Iff (skS.0 0 a) (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) False) % 6.84/7.00 (Or (Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq (skS.0 2 a a_1 a_2) True)) % 6.84/7.00 Clause #12 (by clausification #[10]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Or (Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) False) % 6.84/7.00 (Or (Eq (skS.0 2 a a_1 a_2) False) (Or (Eq (skS.0 0 a) False) (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) False))) % 6.84/7.00 Clause #13 (by clausification #[10]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Or (Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) False) % 6.84/7.00 (Or (Eq (skS.0 2 a a_1 a_2) False) (Or (Eq (skS.0 0 a) True) (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True))) % 6.84/7.00 Clause #14 (by clausification #[12]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Or (Eq (skS.0 2 a a_1 a_2) False) % 6.84/7.00 (Or (Eq (skS.0 0 a) False) % 6.84/7.00 (Or (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) False) (Or (Eq (skS.0 0 a) False) (Eq (skS.0 1 a a_1) False)))) % 6.84/7.00 Clause #16 (by clausification #[14]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Or (Eq (skS.0 2 a a_1 a_2) False) % 6.84/7.00 (Or (Eq (skS.0 0 a) False) % 6.84/7.00 (Or (Eq (skS.0 0 a) False) % 6.84/7.00 (Or (Eq (skS.0 1 a a_1) False) (Or (Eq (skS.0 1 a a_1) False) (Eq (skS.0 2 a a_1 a_2) False))))) % 6.84/7.00 Clause #18 (by eliminate duplicate literals #[16]): ∀ (a a_1 a_2 : Prop), Or (Eq (skS.0 2 a a_1 a_2) False) (Or (Eq (skS.0 0 a) False) (Eq (skS.0 1 a a_1) False)) % 6.84/7.00 Clause #19 (by identity loobHoist #[18]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Or (Eq (skS.0 0 a) False) (Or (Eq (skS.0 1 a a_1) False) (Or (Eq (skS.0 2 a a_1 True) False) (Eq a_2 False))) % 6.84/7.00 Clause #21 (by identity loobHoist #[19]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Or (Eq (skS.0 1 a a_1) False) % 6.84/7.00 (Or (Eq (skS.0 2 a a_1 True) False) (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) False) (Eq a False)))) % 6.84/7.00 Clause #23 (by identity loobHoist #[21]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Or (Eq (skS.0 2 a a_1 True) False) % 6.84/7.00 (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) False) (Or (Eq a False) (Or (Eq (skS.0 1 a True) False) (Eq a_1 False))))) % 6.84/7.00 Clause #25 (by identity loobHoist #[23]): ∀ (a a_1 a_2 : Prop), % 6.84/7.00 Or (Eq a False) % 6.84/7.00 (Or (Eq (skS.0 0 True) False) % 6.87/7.04 (Or (Eq a_1 False) % 6.87/7.04 (Or (Eq (skS.0 1 a_1 True) False) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) False) (Eq a_2 False)))))) % 6.87/7.04 Clause #27 (by eliminate duplicate literals #[25]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq a False) % 6.87/7.04 (Or (Eq (skS.0 0 True) False) % 6.87/7.04 (Or (Eq a_1 False) (Or (Eq (skS.0 1 a_1 True) False) (Or (Eq a_2 False) (Eq (skS.0 2 a_1 True True) False))))) % 6.87/7.04 Clause #28 (by identity loobHoist #[27]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq a False) % 6.87/7.04 (Or (Eq (skS.0 0 True) False) % 6.87/7.04 (Or (Eq a_1 False) % 6.87/7.04 (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) False) (Or (Eq (skS.0 1 True True) False) (Eq a_1 False)))))) % 6.87/7.04 Clause #30 (by eliminate duplicate literals #[28]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq a False) % 6.87/7.04 (Or (Eq (skS.0 0 True) False) % 6.87/7.04 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) False) (Eq (skS.0 1 True True) False))))) % 6.87/7.04 Clause #31 (by identity loobHoist #[30]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq a False) % 6.87/7.04 (Or (Eq (skS.0 0 True) False) % 6.87/7.04 (Or (Eq a_1 False) % 6.87/7.04 (Or (Eq a_2 False) % 6.87/7.04 (Or (Eq (skS.0 1 True True) False) (Or (Eq (skS.0 2 True True True) False) (Eq a_1 False)))))) % 6.87/7.04 Clause #33 (by eliminate duplicate literals #[31]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq a False) % 6.87/7.04 (Or (Eq (skS.0 0 True) False) % 6.87/7.04 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) False))))) % 6.87/7.04 Clause #34 (by falseElim #[33]): ∀ (a a_1 : Prop), % 6.87/7.04 Or (Eq (skS.0 0 True) False) % 6.87/7.04 (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) False)))) % 6.87/7.04 Clause #62 (by clausification #[9]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq (Iff (skS.0 0 a) (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) True) % 6.87/7.04 (Or (Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq (skS.0 2 a a_1 a_2) False)) % 6.87/7.04 Clause #63 (by clausification #[9]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq (Iff (skS.0 0 a) (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) True) % 6.87/7.04 (Or (Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) False) (Eq (skS.0 2 a a_1 a_2) True)) % 6.87/7.04 Clause #64 (by clausification #[62]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) True) % 6.87/7.04 (Or (Eq (skS.0 2 a a_1 a_2) False) (Or (Eq (skS.0 0 a) True) (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) False))) % 6.87/7.04 Clause #65 (by clausification #[62]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) True) % 6.87/7.04 (Or (Eq (skS.0 2 a a_1 a_2) False) (Or (Eq (skS.0 0 a) False) (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True))) % 6.87/7.04 Clause #66 (by clausification #[64]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq (skS.0 2 a a_1 a_2) False) % 6.87/7.04 (Or (Eq (skS.0 0 a) True) % 6.87/7.04 (Or (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) False) (Or (Eq (skS.0 0 a) True) (Eq (skS.0 1 a a_1) False)))) % 6.87/7.04 Clause #68 (by clausification #[66]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq (skS.0 2 a a_1 a_2) False) % 6.87/7.04 (Or (Eq (skS.0 0 a) True) % 6.87/7.04 (Or (Eq (skS.0 0 a) True) % 6.87/7.04 (Or (Eq (skS.0 1 a a_1) False) (Or (Eq (skS.0 1 a a_1) False) (Eq (skS.0 2 a a_1 a_2) False))))) % 6.87/7.04 Clause #70 (by eliminate duplicate literals #[68]): ∀ (a a_1 a_2 : Prop), Or (Eq (skS.0 2 a a_1 a_2) False) (Or (Eq (skS.0 0 a) True) (Eq (skS.0 1 a a_1) False)) % 6.87/7.04 Clause #71 (by identity loobHoist #[70]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq (skS.0 0 a) True) (Or (Eq (skS.0 1 a a_1) False) (Or (Eq (skS.0 2 a a_1 True) False) (Eq a_2 False))) % 6.87/7.04 Clause #73 (by identity loobHoist #[71]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq (skS.0 1 a a_1) False) % 6.87/7.04 (Or (Eq (skS.0 2 a a_1 True) False) (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) True) (Eq a False)))) % 6.87/7.04 Clause #75 (by identity loobHoist #[73]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq (skS.0 2 a a_1 True) False) % 6.87/7.04 (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Or (Eq (skS.0 1 a True) False) (Eq a_1 False))))) % 6.87/7.04 Clause #77 (by identity loobHoist #[75]): ∀ (a a_1 a_2 : Prop), % 6.87/7.04 Or (Eq a False) % 6.87/7.04 (Or (Eq (skS.0 0 True) True) % 6.87/7.04 (Or (Eq a_1 False) % 6.87/7.04 (Or (Eq (skS.0 1 a_1 True) False) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) False) (Eq a_2 False)))))) % 6.87/7.04 Clause #79 (by eliminate duplicate literals #[77]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq a False) % 6.87/7.07 (Or (Eq (skS.0 0 True) True) % 6.87/7.07 (Or (Eq a_1 False) (Or (Eq (skS.0 1 a_1 True) False) (Or (Eq a_2 False) (Eq (skS.0 2 a_1 True True) False))))) % 6.87/7.07 Clause #80 (by identity loobHoist #[79]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq a False) % 6.87/7.07 (Or (Eq (skS.0 0 True) True) % 6.87/7.07 (Or (Eq a_1 False) % 6.87/7.07 (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) False) (Or (Eq (skS.0 1 True True) False) (Eq a_1 False)))))) % 6.87/7.07 Clause #82 (by eliminate duplicate literals #[80]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq a False) % 6.87/7.07 (Or (Eq (skS.0 0 True) True) % 6.87/7.07 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) False) (Eq (skS.0 1 True True) False))))) % 6.87/7.07 Clause #83 (by identity loobHoist #[82]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq a False) % 6.87/7.07 (Or (Eq (skS.0 0 True) True) % 6.87/7.07 (Or (Eq a_1 False) % 6.87/7.07 (Or (Eq a_2 False) % 6.87/7.07 (Or (Eq (skS.0 1 True True) False) (Or (Eq (skS.0 2 True True True) False) (Eq a_1 False)))))) % 6.87/7.07 Clause #85 (by eliminate duplicate literals #[83]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq a False) % 6.87/7.07 (Or (Eq (skS.0 0 True) True) % 6.87/7.07 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) False))))) % 6.87/7.07 Clause #86 (by falseElim #[85]): ∀ (a a_1 : Prop), % 6.87/7.07 Or (Eq (skS.0 0 True) True) % 6.87/7.07 (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) False)))) % 6.87/7.07 Clause #116 (by clausification #[11]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) True) % 6.87/7.07 (Or (Eq (skS.0 2 a a_1 a_2) True) (Or (Eq (skS.0 0 a) False) (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) False))) % 6.87/7.07 Clause #117 (by clausification #[11]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) True) % 6.87/7.07 (Or (Eq (skS.0 2 a a_1 a_2) True) (Or (Eq (skS.0 0 a) True) (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True))) % 6.87/7.07 Clause #119 (by clausification #[116]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq (skS.0 2 a a_1 a_2) True) % 6.87/7.07 (Or (Eq (skS.0 0 a) False) % 6.87/7.07 (Or (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) False) (Or (Eq (skS.0 0 a) False) (Eq (skS.0 1 a a_1) True)))) % 6.87/7.07 Clause #122 (by falseElim #[86]): ∀ (a : Prop), % 6.87/7.07 Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) False))) % 6.87/7.07 Clause #123 (by falseElim #[122]): Or (Eq (skS.0 0 True) True) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) False)) % 6.87/7.07 Clause #129 (by clausification #[13]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq (skS.0 2 a a_1 a_2) False) % 6.87/7.07 (Or (Eq (skS.0 0 a) True) % 6.87/7.07 (Or (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True) (Or (Eq (skS.0 0 a) True) (Eq (skS.0 1 a a_1) True)))) % 6.87/7.07 Clause #203 (by clausification #[63]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) False) % 6.87/7.07 (Or (Eq (skS.0 2 a a_1 a_2) True) (Or (Eq (skS.0 0 a) True) (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) False))) % 6.87/7.07 Clause #204 (by clausification #[63]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) False) % 6.87/7.07 (Or (Eq (skS.0 2 a a_1 a_2) True) (Or (Eq (skS.0 0 a) False) (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True))) % 6.87/7.07 Clause #206 (by clausification #[203]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq (skS.0 2 a a_1 a_2) True) % 6.87/7.07 (Or (Eq (skS.0 0 a) True) % 6.87/7.07 (Or (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) False) (Or (Eq (skS.0 0 a) True) (Eq (skS.0 1 a a_1) True)))) % 6.87/7.07 Clause #219 (by clausification #[65]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq (skS.0 2 a a_1 a_2) False) % 6.87/7.07 (Or (Eq (skS.0 0 a) False) % 6.87/7.07 (Or (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True) (Or (Eq (skS.0 0 a) False) (Eq (skS.0 1 a a_1) True)))) % 6.87/7.07 Clause #240 (by clausification #[129]): ∀ (a a_1 a_2 : Prop), % 6.87/7.07 Or (Eq (skS.0 2 a a_1 a_2) False) % 6.87/7.07 (Or (Eq (skS.0 0 a) True) % 6.87/7.07 (Or (Eq (skS.0 0 a) True) % 6.87/7.07 (Or (Eq (skS.0 1 a a_1) True) (Or (Eq (skS.0 1 a a_1) True) (Eq (skS.0 2 a a_1 a_2) False))))) % 6.87/7.07 Clause #242 (by eliminate duplicate literals #[240]): ∀ (a a_1 a_2 : Prop), Or (Eq (skS.0 2 a a_1 a_2) False) (Or (Eq (skS.0 0 a) True) (Eq (skS.0 1 a a_1) True)) % 6.87/7.07 Clause #243 (by identity loobHoist #[242]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq (skS.0 0 a) True) (Or (Eq (skS.0 1 a a_1) True) (Or (Eq (skS.0 2 a a_1 True) False) (Eq a_2 False))) % 6.87/7.10 Clause #245 (by identity loobHoist #[243]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq (skS.0 1 a a_1) True) % 6.87/7.10 (Or (Eq (skS.0 2 a a_1 True) False) (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) True) (Eq a False)))) % 6.87/7.10 Clause #247 (by identity loobHoist #[245]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq (skS.0 2 a a_1 True) False) % 6.87/7.10 (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Or (Eq (skS.0 1 a True) True) (Eq a_1 False))))) % 6.87/7.10 Clause #249 (by identity loobHoist #[247]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq a False) % 6.87/7.10 (Or (Eq (skS.0 0 True) True) % 6.87/7.10 (Or (Eq a_1 False) % 6.87/7.10 (Or (Eq (skS.0 1 a_1 True) True) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) False) (Eq a_2 False)))))) % 6.87/7.10 Clause #251 (by eliminate duplicate literals #[249]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq a False) % 6.87/7.10 (Or (Eq (skS.0 0 True) True) % 6.87/7.10 (Or (Eq a_1 False) (Or (Eq (skS.0 1 a_1 True) True) (Or (Eq a_2 False) (Eq (skS.0 2 a_1 True True) False))))) % 6.87/7.10 Clause #252 (by identity loobHoist #[251]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq a False) % 6.87/7.10 (Or (Eq (skS.0 0 True) True) % 6.87/7.10 (Or (Eq a_1 False) % 6.87/7.10 (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) False) (Or (Eq (skS.0 1 True True) True) (Eq a_1 False)))))) % 6.87/7.10 Clause #254 (by eliminate duplicate literals #[252]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq a False) % 6.87/7.10 (Or (Eq (skS.0 0 True) True) % 6.87/7.10 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) False) (Eq (skS.0 1 True True) True))))) % 6.87/7.10 Clause #255 (by identity loobHoist #[254]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq a False) % 6.87/7.10 (Or (Eq (skS.0 0 True) True) % 6.87/7.10 (Or (Eq a_1 False) % 6.87/7.10 (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) True) (Or (Eq (skS.0 2 True True True) False) (Eq a_1 False)))))) % 6.87/7.10 Clause #257 (by eliminate duplicate literals #[255]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq a False) % 6.87/7.10 (Or (Eq (skS.0 0 True) True) % 6.87/7.10 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) False))))) % 6.87/7.10 Clause #258 (by falseElim #[257]): ∀ (a a_1 : Prop), % 6.87/7.10 Or (Eq (skS.0 0 True) True) % 6.87/7.10 (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) False)))) % 6.87/7.10 Clause #288 (by clausification #[117]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq (skS.0 2 a a_1 a_2) True) % 6.87/7.10 (Or (Eq (skS.0 0 a) True) % 6.87/7.10 (Or (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True) (Or (Eq (skS.0 0 a) True) (Eq (skS.0 1 a a_1) False)))) % 6.87/7.10 Clause #291 (by clausification #[288]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq (skS.0 2 a a_1 a_2) True) % 6.87/7.10 (Or (Eq (skS.0 0 a) True) % 6.87/7.10 (Or (Eq (skS.0 0 a) True) % 6.87/7.10 (Or (Eq (skS.0 1 a a_1) False) (Or (Eq (skS.0 1 a a_1) False) (Eq (skS.0 2 a a_1 a_2) True))))) % 6.87/7.10 Clause #292 (by falseElim #[258]): ∀ (a : Prop), % 6.87/7.10 Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) False))) % 6.87/7.10 Clause #293 (by falseElim #[292]): Or (Eq (skS.0 0 True) True) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) False)) % 6.87/7.10 Clause #299 (by clausification #[119]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq (skS.0 2 a a_1 a_2) True) % 6.87/7.10 (Or (Eq (skS.0 0 a) False) % 6.87/7.10 (Or (Eq (skS.0 0 a) False) % 6.87/7.10 (Or (Eq (skS.0 1 a a_1) True) (Or (Eq (skS.0 1 a a_1) True) (Eq (skS.0 2 a a_1 a_2) True))))) % 6.87/7.10 Clause #325 (by clausification #[204]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq (skS.0 2 a a_1 a_2) True) % 6.87/7.10 (Or (Eq (skS.0 0 a) False) % 6.87/7.10 (Or (Eq (Iff (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True) (Or (Eq (skS.0 0 a) False) (Eq (skS.0 1 a a_1) False)))) % 6.87/7.10 Clause #328 (by clausification #[325]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq (skS.0 2 a a_1 a_2) True) % 6.87/7.10 (Or (Eq (skS.0 0 a) False) % 6.87/7.10 (Or (Eq (skS.0 0 a) False) % 6.87/7.10 (Or (Eq (skS.0 1 a a_1) False) (Or (Eq (skS.0 1 a a_1) False) (Eq (skS.0 2 a a_1 a_2) True))))) % 6.87/7.10 Clause #338 (by clausification #[206]): ∀ (a a_1 a_2 : Prop), % 6.87/7.10 Or (Eq (skS.0 2 a a_1 a_2) True) % 6.87/7.10 (Or (Eq (skS.0 0 a) True) % 6.87/7.10 (Or (Eq (skS.0 0 a) True) % 6.87/7.10 (Or (Eq (skS.0 1 a a_1) True) (Or (Eq (skS.0 1 a a_1) True) (Eq (skS.0 2 a a_1 a_2) True))))) % 6.96/7.13 Clause #353 (by clausification #[219]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq (skS.0 2 a a_1 a_2) False) % 6.96/7.13 (Or (Eq (skS.0 0 a) False) % 6.96/7.13 (Or (Eq (skS.0 0 a) False) % 6.96/7.13 (Or (Eq (skS.0 1 a a_1) True) (Or (Eq (skS.0 1 a a_1) True) (Eq (skS.0 2 a a_1 a_2) False))))) % 6.96/7.13 Clause #355 (by eliminate duplicate literals #[353]): ∀ (a a_1 a_2 : Prop), Or (Eq (skS.0 2 a a_1 a_2) False) (Or (Eq (skS.0 0 a) False) (Eq (skS.0 1 a a_1) True)) % 6.96/7.13 Clause #356 (by identity loobHoist #[355]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq (skS.0 0 a) False) (Or (Eq (skS.0 1 a a_1) True) (Or (Eq (skS.0 2 a a_1 True) False) (Eq a_2 False))) % 6.96/7.13 Clause #358 (by identity loobHoist #[356]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq (skS.0 1 a a_1) True) % 6.96/7.13 (Or (Eq (skS.0 2 a a_1 True) False) (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) False) (Eq a False)))) % 6.96/7.13 Clause #360 (by identity loobHoist #[358]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq (skS.0 2 a a_1 True) False) % 6.96/7.13 (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) False) (Or (Eq a False) (Or (Eq (skS.0 1 a True) True) (Eq a_1 False))))) % 6.96/7.13 Clause #362 (by identity loobHoist #[360]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq a False) % 6.96/7.13 (Or (Eq (skS.0 0 True) False) % 6.96/7.13 (Or (Eq a_1 False) % 6.96/7.13 (Or (Eq (skS.0 1 a_1 True) True) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) False) (Eq a_2 False)))))) % 6.96/7.13 Clause #364 (by eliminate duplicate literals #[362]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq a False) % 6.96/7.13 (Or (Eq (skS.0 0 True) False) % 6.96/7.13 (Or (Eq a_1 False) (Or (Eq (skS.0 1 a_1 True) True) (Or (Eq a_2 False) (Eq (skS.0 2 a_1 True True) False))))) % 6.96/7.13 Clause #365 (by identity loobHoist #[364]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq a False) % 6.96/7.13 (Or (Eq (skS.0 0 True) False) % 6.96/7.13 (Or (Eq a_1 False) % 6.96/7.13 (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) False) (Or (Eq (skS.0 1 True True) True) (Eq a_1 False)))))) % 6.96/7.13 Clause #367 (by eliminate duplicate literals #[365]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq a False) % 6.96/7.13 (Or (Eq (skS.0 0 True) False) % 6.96/7.13 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) False) (Eq (skS.0 1 True True) True))))) % 6.96/7.13 Clause #368 (by identity loobHoist #[367]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq a False) % 6.96/7.13 (Or (Eq (skS.0 0 True) False) % 6.96/7.13 (Or (Eq a_1 False) % 6.96/7.13 (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) True) (Or (Eq (skS.0 2 True True True) False) (Eq a_1 False)))))) % 6.96/7.13 Clause #370 (by eliminate duplicate literals #[368]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq a False) % 6.96/7.13 (Or (Eq (skS.0 0 True) False) % 6.96/7.13 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) False))))) % 6.96/7.13 Clause #371 (by falseElim #[370]): ∀ (a a_1 : Prop), % 6.96/7.13 Or (Eq (skS.0 0 True) False) % 6.96/7.13 (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) False)))) % 6.96/7.13 Clause #444 (by eliminate duplicate literals #[291]): ∀ (a a_1 a_2 : Prop), Or (Eq (skS.0 2 a a_1 a_2) True) (Or (Eq (skS.0 0 a) True) (Eq (skS.0 1 a a_1) False)) % 6.96/7.13 Clause #445 (by identity loobHoist #[444]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq (skS.0 0 a) True) (Or (Eq (skS.0 1 a a_1) False) (Or (Eq (skS.0 2 a a_1 True) True) (Eq a_2 False))) % 6.96/7.13 Clause #447 (by identity loobHoist #[445]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq (skS.0 1 a a_1) False) % 6.96/7.13 (Or (Eq (skS.0 2 a a_1 True) True) (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) True) (Eq a False)))) % 6.96/7.13 Clause #449 (by identity loobHoist #[447]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq (skS.0 2 a a_1 True) True) % 6.96/7.13 (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Or (Eq (skS.0 1 a True) False) (Eq a_1 False))))) % 6.96/7.13 Clause #451 (by identity loobHoist #[449]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq a False) % 6.96/7.13 (Or (Eq (skS.0 0 True) True) % 6.96/7.13 (Or (Eq a_1 False) % 6.96/7.13 (Or (Eq (skS.0 1 a_1 True) False) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) True) (Eq a_2 False)))))) % 6.96/7.13 Clause #453 (by eliminate duplicate literals #[451]): ∀ (a a_1 a_2 : Prop), % 6.96/7.13 Or (Eq a False) % 6.96/7.13 (Or (Eq (skS.0 0 True) True) % 6.96/7.13 (Or (Eq a_1 False) (Or (Eq (skS.0 1 a_1 True) False) (Or (Eq a_2 False) (Eq (skS.0 2 a_1 True True) True))))) % 6.96/7.16 Clause #454 (by identity loobHoist #[453]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq a False) % 6.96/7.16 (Or (Eq (skS.0 0 True) True) % 6.96/7.16 (Or (Eq a_1 False) % 6.96/7.16 (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) True) (Or (Eq (skS.0 1 True True) False) (Eq a_1 False)))))) % 6.96/7.16 Clause #456 (by eliminate duplicate literals #[454]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq a False) % 6.96/7.16 (Or (Eq (skS.0 0 True) True) % 6.96/7.16 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) True) (Eq (skS.0 1 True True) False))))) % 6.96/7.16 Clause #457 (by identity loobHoist #[456]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq a False) % 6.96/7.16 (Or (Eq (skS.0 0 True) True) % 6.96/7.16 (Or (Eq a_1 False) % 6.96/7.16 (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) False) (Or (Eq (skS.0 2 True True True) True) (Eq a_1 False)))))) % 6.96/7.16 Clause #459 (by eliminate duplicate literals #[457]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq a False) % 6.96/7.16 (Or (Eq (skS.0 0 True) True) % 6.96/7.16 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) True))))) % 6.96/7.16 Clause #460 (by falseElim #[459]): ∀ (a a_1 : Prop), % 6.96/7.16 Or (Eq (skS.0 0 True) True) % 6.96/7.16 (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) True)))) % 6.96/7.16 Clause #482 (by falseElim #[460]): ∀ (a : Prop), % 6.96/7.16 Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) True))) % 6.96/7.16 Clause #483 (by falseElim #[482]): Or (Eq (skS.0 0 True) True) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) True)) % 6.96/7.16 Clause #484 (by eliminate duplicate literals #[299]): ∀ (a a_1 a_2 : Prop), Or (Eq (skS.0 2 a a_1 a_2) True) (Or (Eq (skS.0 0 a) False) (Eq (skS.0 1 a a_1) True)) % 6.96/7.16 Clause #485 (by identity loobHoist #[484]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq (skS.0 0 a) False) (Or (Eq (skS.0 1 a a_1) True) (Or (Eq (skS.0 2 a a_1 True) True) (Eq a_2 False))) % 6.96/7.16 Clause #487 (by identity loobHoist #[485]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq (skS.0 1 a a_1) True) % 6.96/7.16 (Or (Eq (skS.0 2 a a_1 True) True) (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) False) (Eq a False)))) % 6.96/7.16 Clause #489 (by identity loobHoist #[487]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq (skS.0 2 a a_1 True) True) % 6.96/7.16 (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) False) (Or (Eq a False) (Or (Eq (skS.0 1 a True) True) (Eq a_1 False))))) % 6.96/7.16 Clause #491 (by identity loobHoist #[489]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq a False) % 6.96/7.16 (Or (Eq (skS.0 0 True) False) % 6.96/7.16 (Or (Eq a_1 False) % 6.96/7.16 (Or (Eq (skS.0 1 a_1 True) True) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) True) (Eq a_2 False)))))) % 6.96/7.16 Clause #493 (by eliminate duplicate literals #[491]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq a False) % 6.96/7.16 (Or (Eq (skS.0 0 True) False) % 6.96/7.16 (Or (Eq a_1 False) (Or (Eq (skS.0 1 a_1 True) True) (Or (Eq a_2 False) (Eq (skS.0 2 a_1 True True) True))))) % 6.96/7.16 Clause #494 (by identity loobHoist #[493]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq a False) % 6.96/7.16 (Or (Eq (skS.0 0 True) False) % 6.96/7.16 (Or (Eq a_1 False) % 6.96/7.16 (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) True) (Or (Eq (skS.0 1 True True) True) (Eq a_1 False)))))) % 6.96/7.16 Clause #496 (by eliminate duplicate literals #[494]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq a False) % 6.96/7.16 (Or (Eq (skS.0 0 True) False) % 6.96/7.16 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) True) (Eq (skS.0 1 True True) True))))) % 6.96/7.16 Clause #497 (by identity loobHoist #[496]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq a False) % 6.96/7.16 (Or (Eq (skS.0 0 True) False) % 6.96/7.16 (Or (Eq a_1 False) % 6.96/7.16 (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) True) (Or (Eq (skS.0 2 True True True) True) (Eq a_1 False)))))) % 6.96/7.16 Clause #499 (by eliminate duplicate literals #[497]): ∀ (a a_1 a_2 : Prop), % 6.96/7.16 Or (Eq a False) % 6.96/7.16 (Or (Eq (skS.0 0 True) False) % 6.96/7.16 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) True))))) % 6.96/7.16 Clause #500 (by falseElim #[499]): ∀ (a a_1 : Prop), % 6.96/7.16 Or (Eq (skS.0 0 True) False) % 6.96/7.16 (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) True)))) % 6.96/7.16 Clause #544 (by eliminate duplicate literals #[328]): ∀ (a a_1 a_2 : Prop), Or (Eq (skS.0 2 a a_1 a_2) True) (Or (Eq (skS.0 0 a) False) (Eq (skS.0 1 a a_1) False)) % 7.04/7.20 Clause #545 (by identity loobHoist #[544]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq (skS.0 0 a) False) (Or (Eq (skS.0 1 a a_1) False) (Or (Eq (skS.0 2 a a_1 True) True) (Eq a_2 False))) % 7.04/7.20 Clause #547 (by identity loobHoist #[545]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq (skS.0 1 a a_1) False) % 7.04/7.20 (Or (Eq (skS.0 2 a a_1 True) True) (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) False) (Eq a False)))) % 7.04/7.20 Clause #549 (by identity loobHoist #[547]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq (skS.0 2 a a_1 True) True) % 7.04/7.20 (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) False) (Or (Eq a False) (Or (Eq (skS.0 1 a True) False) (Eq a_1 False))))) % 7.04/7.20 Clause #551 (by identity loobHoist #[549]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq a False) % 7.04/7.20 (Or (Eq (skS.0 0 True) False) % 7.04/7.20 (Or (Eq a_1 False) % 7.04/7.20 (Or (Eq (skS.0 1 a_1 True) False) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) True) (Eq a_2 False)))))) % 7.04/7.20 Clause #553 (by eliminate duplicate literals #[551]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq a False) % 7.04/7.20 (Or (Eq (skS.0 0 True) False) % 7.04/7.20 (Or (Eq a_1 False) (Or (Eq (skS.0 1 a_1 True) False) (Or (Eq a_2 False) (Eq (skS.0 2 a_1 True True) True))))) % 7.04/7.20 Clause #554 (by identity loobHoist #[553]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq a False) % 7.04/7.20 (Or (Eq (skS.0 0 True) False) % 7.04/7.20 (Or (Eq a_1 False) % 7.04/7.20 (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) True) (Or (Eq (skS.0 1 True True) False) (Eq a_1 False)))))) % 7.04/7.20 Clause #556 (by eliminate duplicate literals #[554]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq a False) % 7.04/7.20 (Or (Eq (skS.0 0 True) False) % 7.04/7.20 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) True) (Eq (skS.0 1 True True) False))))) % 7.04/7.20 Clause #557 (by identity loobHoist #[556]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq a False) % 7.04/7.20 (Or (Eq (skS.0 0 True) False) % 7.04/7.20 (Or (Eq a_1 False) % 7.04/7.20 (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) False) (Or (Eq (skS.0 2 True True True) True) (Eq a_1 False)))))) % 7.04/7.20 Clause #559 (by eliminate duplicate literals #[557]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq a False) % 7.04/7.20 (Or (Eq (skS.0 0 True) False) % 7.04/7.20 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) True))))) % 7.04/7.20 Clause #560 (by falseElim #[559]): ∀ (a a_1 : Prop), % 7.04/7.20 Or (Eq (skS.0 0 True) False) % 7.04/7.20 (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) True)))) % 7.04/7.20 Clause #590 (by eliminate duplicate literals #[338]): ∀ (a a_1 a_2 : Prop), Or (Eq (skS.0 2 a a_1 a_2) True) (Or (Eq (skS.0 0 a) True) (Eq (skS.0 1 a a_1) True)) % 7.04/7.20 Clause #591 (by identity loobHoist #[590]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq (skS.0 0 a) True) (Or (Eq (skS.0 1 a a_1) True) (Or (Eq (skS.0 2 a a_1 True) True) (Eq a_2 False))) % 7.04/7.20 Clause #593 (by identity loobHoist #[591]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq (skS.0 1 a a_1) True) % 7.04/7.20 (Or (Eq (skS.0 2 a a_1 True) True) (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) True) (Eq a False)))) % 7.04/7.20 Clause #595 (by identity loobHoist #[593]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq (skS.0 2 a a_1 True) True) % 7.04/7.20 (Or (Eq a_2 False) (Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Or (Eq (skS.0 1 a True) True) (Eq a_1 False))))) % 7.04/7.20 Clause #597 (by identity loobHoist #[595]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq a False) % 7.04/7.20 (Or (Eq (skS.0 0 True) True) % 7.04/7.20 (Or (Eq a_1 False) % 7.04/7.20 (Or (Eq (skS.0 1 a_1 True) True) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) True) (Eq a_2 False)))))) % 7.04/7.20 Clause #599 (by eliminate duplicate literals #[597]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq a False) % 7.04/7.20 (Or (Eq (skS.0 0 True) True) % 7.04/7.20 (Or (Eq a_1 False) (Or (Eq (skS.0 1 a_1 True) True) (Or (Eq a_2 False) (Eq (skS.0 2 a_1 True True) True))))) % 7.04/7.20 Clause #600 (by identity loobHoist #[599]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq a False) % 7.04/7.20 (Or (Eq (skS.0 0 True) True) % 7.04/7.20 (Or (Eq a_1 False) % 7.04/7.20 (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) True) (Or (Eq (skS.0 1 True True) True) (Eq a_1 False)))))) % 7.04/7.20 Clause #602 (by eliminate duplicate literals #[600]): ∀ (a a_1 a_2 : Prop), % 7.04/7.20 Or (Eq a False) % 7.04/7.23 (Or (Eq (skS.0 0 True) True) % 7.04/7.23 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 2 a_1 True True) True) (Eq (skS.0 1 True True) True))))) % 7.04/7.23 Clause #603 (by identity loobHoist #[602]): ∀ (a a_1 a_2 : Prop), % 7.04/7.23 Or (Eq a False) % 7.04/7.23 (Or (Eq (skS.0 0 True) True) % 7.04/7.23 (Or (Eq a_1 False) % 7.04/7.23 (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) True) (Or (Eq (skS.0 2 True True True) True) (Eq a_1 False)))))) % 7.04/7.23 Clause #605 (by eliminate duplicate literals #[603]): ∀ (a a_1 a_2 : Prop), % 7.04/7.23 Or (Eq a False) % 7.04/7.23 (Or (Eq (skS.0 0 True) True) % 7.04/7.23 (Or (Eq a_1 False) (Or (Eq a_2 False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) True))))) % 7.04/7.23 Clause #606 (by falseElim #[605]): ∀ (a a_1 : Prop), % 7.04/7.23 Or (Eq (skS.0 0 True) True) % 7.04/7.23 (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) True)))) % 7.04/7.23 Clause #645 (by falseElim #[606]): ∀ (a : Prop), % 7.04/7.23 Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) True))) % 7.04/7.23 Clause #647 (by falseElim #[645]): Or (Eq (skS.0 0 True) True) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) True)) % 7.04/7.23 Clause #648 (by superposition #[647, 293]): Or (Eq (skS.0 0 True) True) % 7.04/7.23 (Or (Eq (skS.0 1 True True) True) (Or (Eq (skS.0 0 True) True) (Or (Eq (skS.0 1 True True) True) (Eq True False)))) % 7.04/7.23 Clause #682 (by clausification #[648]): Or (Eq (skS.0 0 True) True) % 7.04/7.23 (Or (Eq (skS.0 1 True True) True) (Or (Eq (skS.0 0 True) True) (Eq (skS.0 1 True True) True))) % 7.04/7.23 Clause #683 (by eliminate duplicate literals #[682]): Or (Eq (skS.0 0 True) True) (Eq (skS.0 1 True True) True) % 7.04/7.23 Clause #685 (by superposition #[683, 123]): Or (Eq (skS.0 0 True) True) (Or (Eq (skS.0 0 True) True) (Or (Eq True False) (Eq (skS.0 2 True True True) False))) % 7.04/7.23 Clause #686 (by superposition #[683, 483]): Or (Eq (skS.0 0 True) True) (Or (Eq (skS.0 0 True) True) (Or (Eq True False) (Eq (skS.0 2 True True True) True))) % 7.04/7.23 Clause #688 (by clausification #[686]): Or (Eq (skS.0 0 True) True) (Or (Eq (skS.0 0 True) True) (Eq (skS.0 2 True True True) True)) % 7.04/7.23 Clause #689 (by eliminate duplicate literals #[688]): Or (Eq (skS.0 0 True) True) (Eq (skS.0 2 True True True) True) % 7.04/7.23 Clause #690 (by clausification #[685]): Or (Eq (skS.0 0 True) True) (Or (Eq (skS.0 0 True) True) (Eq (skS.0 2 True True True) False)) % 7.04/7.23 Clause #691 (by eliminate duplicate literals #[690]): Or (Eq (skS.0 0 True) True) (Eq (skS.0 2 True True True) False) % 7.04/7.23 Clause #692 (by superposition #[691, 689]): Or (Eq (skS.0 0 True) True) (Or (Eq (skS.0 0 True) True) (Eq False True)) % 7.04/7.23 Clause #693 (by clausification #[692]): Or (Eq (skS.0 0 True) True) (Eq (skS.0 0 True) True) % 7.04/7.23 Clause #694 (by eliminate duplicate literals #[693]): Eq (skS.0 0 True) True % 7.04/7.23 Clause #696 (by backward demodulation #[694, 34]): ∀ (a a_1 : Prop), % 7.04/7.23 Or (Eq True False) % 7.04/7.23 (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) False)))) % 7.04/7.23 Clause #705 (by backward demodulation #[694, 371]): ∀ (a a_1 : Prop), % 7.04/7.23 Or (Eq True False) % 7.04/7.23 (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) False)))) % 7.04/7.23 Clause #710 (by backward demodulation #[694, 500]): ∀ (a a_1 : Prop), % 7.04/7.23 Or (Eq True False) % 7.04/7.23 (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) True)))) % 7.04/7.23 Clause #712 (by backward demodulation #[694, 560]): ∀ (a a_1 : Prop), % 7.04/7.23 Or (Eq True False) % 7.04/7.23 (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) True)))) % 7.04/7.23 Clause #719 (by clausification #[712]): ∀ (a a_1 : Prop), % 7.04/7.23 Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) True))) % 7.04/7.23 Clause #721 (by falseElim #[719]): ∀ (a : Prop), Or (Eq a False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) True)) % 7.04/7.23 Clause #723 (by falseElim #[721]): Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) True) % 7.04/7.23 Clause #727 (by clausification #[696]): ∀ (a a_1 : Prop), % 7.04/7.23 Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) False))) % 7.04/7.25 Clause #729 (by falseElim #[727]): ∀ (a : Prop), Or (Eq a False) (Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) False)) % 7.04/7.25 Clause #731 (by falseElim #[729]): Or (Eq (skS.0 1 True True) False) (Eq (skS.0 2 True True True) False) % 7.04/7.25 Clause #732 (by clausification #[710]): ∀ (a a_1 : Prop), % 7.04/7.25 Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) True))) % 7.04/7.25 Clause #734 (by falseElim #[732]): ∀ (a : Prop), Or (Eq a False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) True)) % 7.04/7.25 Clause #736 (by falseElim #[734]): Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) True) % 7.04/7.25 Clause #741 (by clausification #[705]): ∀ (a a_1 : Prop), % 7.04/7.25 Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) False))) % 7.04/7.25 Clause #744 (by falseElim #[741]): ∀ (a : Prop), Or (Eq a False) (Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) False)) % 7.04/7.25 Clause #747 (by falseElim #[744]): Or (Eq (skS.0 1 True True) True) (Eq (skS.0 2 True True True) False) % 7.04/7.25 Clause #748 (by superposition #[747, 736]): Or (Eq (skS.0 1 True True) True) (Or (Eq (skS.0 1 True True) True) (Eq False True)) % 7.04/7.25 Clause #749 (by clausification #[748]): Or (Eq (skS.0 1 True True) True) (Eq (skS.0 1 True True) True) % 7.04/7.25 Clause #750 (by eliminate duplicate literals #[749]): Eq (skS.0 1 True True) True % 7.04/7.25 Clause #751 (by backward demodulation #[750, 723]): Or (Eq True False) (Eq (skS.0 2 True True True) True) % 7.04/7.25 Clause #752 (by backward demodulation #[750, 731]): Or (Eq True False) (Eq (skS.0 2 True True True) False) % 7.04/7.25 Clause #753 (by clausification #[752]): Eq (skS.0 2 True True True) False % 7.04/7.25 Clause #754 (by clausification #[751]): Eq (skS.0 2 True True True) True % 7.04/7.25 Clause #755 (by superposition #[754, 753]): Eq True False % 7.04/7.25 Clause #756 (by clausification #[755]): False % 7.04/7.25 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------