%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWX187+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n017.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:59:07 PM UTC 2026 % Result : Theorem 215.40s 215.64s % Output : Proof 215.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX187+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : duper %s % 0.19/0.35 % Computer : n017.cluster.edu % 0.19/0.35 % Model : x86_64 x86_64 % 0.19/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.19/0.35 % Memory : 8042.1875MB % 0.19/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.19/0.35 % CPULimit : 300 % 0.19/0.35 % WCLimit : 300 % 0.19/0.35 % DateTime : Tue May 5 09:38:42 EDT 2026 % 0.19/0.35 % CPUTime : % 215.40/215.64 SZS status Theorem for theBenchmark.p % 215.40/215.64 SZS output start Proof for theBenchmark.p % 215.40/215.64 Clause #0 (by assumption #[]): Eq (∀ (X X2 : Iota), Eq (head (cons X X2)) X) True % 215.40/215.64 Clause #4 (by assumption #[]): Eq (∀ (X : Iota), Ne (s X) z) True % 215.40/215.64 Clause #6 (by assumption #[]): Eq (∀ (Y Xs : Iota), Eq (length (cons Y Xs)) (s (length Xs))) True % 215.40/215.64 Clause #7 (by assumption #[]): Eq (∀ (Z Y2 : Iota), Iff (x2 (s Z) (s Y2)) (x2 Z Y2)) True % 215.40/215.64 Clause #9 (by assumption #[]): Eq (∀ (X2 : Iota), x2 z (s X2)) True % 215.40/215.64 Clause #11 (by assumption #[]): Eq (∀ (Y : Iota), Eq (x nil Y) Y) True % 215.40/215.64 Clause #12 (by assumption #[]): Eq (∀ (Y Z Xs : Iota), Eq (x (cons Z Xs) Y) (cons Z (x Xs Y))) True % 215.40/215.64 Clause #14 (by assumption #[]): Eq (∀ (Z X2 X3 : Iota), Eq (rotate (s Z) (cons X2 X3)) (rotate Z (x X3 (cons X2 nil)))) True % 215.40/215.64 Clause #15 (by assumption #[]): Eq (∀ (Y : Iota), Eq (rotate z Y) Y) True % 215.40/215.64 Clause #16 (by assumption #[]): Eq % 215.40/215.64 (Not % 215.40/215.64 (Exists fun N => % 215.40/215.64 Exists fun M => % 215.40/215.64 Exists fun Ys => % 215.40/215.64 Exists fun Xs => % 215.40/215.64 Not % 215.40/215.64 (x2 N (length Xs) → % 215.40/215.64 x2 M (length Ys) → Eq Xs Ys → Ne (rotate (s z) Xs) Xs → Eq (rotate N Xs) (rotate M Ys) → Eq N M))) % 215.40/215.64 True % 215.40/215.64 Clause #19 (by clausification #[9]): ∀ (a : Iota), Eq (x2 z (s a)) True % 215.40/215.64 Clause #22 (by clausification #[4]): ∀ (a : Iota), Eq (Ne (s a) z) True % 215.40/215.64 Clause #23 (by clausification #[22]): ∀ (a : Iota), Ne (s a) z % 215.40/215.64 Clause #24 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (X2 : Iota), Eq (head (cons a X2)) a) True % 215.40/215.64 Clause #25 (by clausification #[24]): ∀ (a a_1 : Iota), Eq (Eq (head (cons a a_1)) a) True % 215.40/215.64 Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota), Eq (head (cons a a_1)) a % 215.40/215.64 Clause #27 (by clausification #[11]): ∀ (a : Iota), Eq (Eq (x nil a) a) True % 215.40/215.64 Clause #28 (by clausification #[27]): ∀ (a : Iota), Eq (x nil a) a % 215.40/215.64 Clause #29 (by clausification #[15]): ∀ (a : Iota), Eq (Eq (rotate z a) a) True % 215.40/215.64 Clause #30 (by clausification #[29]): ∀ (a : Iota), Eq (rotate z a) a % 215.40/215.64 Clause #41 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (Y2 : Iota), Iff (x2 (s a) (s Y2)) (x2 a Y2)) True % 215.40/215.64 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), Eq (Iff (x2 (s a) (s a_1)) (x2 a a_1)) True % 215.40/215.64 Clause #43 (by clausification #[42]): ∀ (a a_1 : Iota), Or (Eq (x2 (s a) (s a_1)) True) (Eq (x2 a a_1) False) % 215.40/215.64 Clause #45 (by superposition #[43, 19]): ∀ (a : Iota), Or (Eq (x2 (s z) (s (s a))) True) (Eq False True) % 215.40/215.64 Clause #46 (by clausification #[45]): ∀ (a : Iota), Eq (x2 (s z) (s (s a))) True % 215.40/215.64 Clause #47 (by superposition #[46, 43]): ∀ (a : Iota), Or (Eq (x2 (s (s z)) (s (s (s a)))) True) (Eq True False) % 215.40/215.64 Clause #49 (by clausification #[47]): ∀ (a : Iota), Eq (x2 (s (s z)) (s (s (s a)))) True % 215.40/215.64 Clause #52 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (Xs : Iota), Eq (length (cons a Xs)) (s (length Xs))) True % 215.40/215.64 Clause #53 (by clausification #[52]): ∀ (a a_1 : Iota), Eq (Eq (length (cons a a_1)) (s (length a_1))) True % 215.40/215.64 Clause #54 (by clausification #[53]): ∀ (a a_1 : Iota), Eq (length (cons a a_1)) (s (length a_1)) % 215.40/215.64 Clause #61 (by clausification #[12]): ∀ (a : Iota), Eq (∀ (Z Xs : Iota), Eq (x (cons Z Xs) a) (cons Z (x Xs a))) True % 215.40/215.64 Clause #62 (by clausification #[61]): ∀ (a a_1 : Iota), Eq (∀ (Xs : Iota), Eq (x (cons a Xs) a_1) (cons a (x Xs a_1))) True % 215.40/215.64 Clause #63 (by clausification #[62]): ∀ (a a_1 a_2 : Iota), Eq (Eq (x (cons a a_1) a_2) (cons a (x a_1 a_2))) True % 215.40/215.64 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 : Iota), Eq (x (cons a a_1) a_2) (cons a (x a_1 a_2)) % 215.40/215.64 Clause #71 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (X2 X3 : Iota), Eq (rotate (s a) (cons X2 X3)) (rotate a (x X3 (cons X2 nil)))) True % 215.40/215.64 Clause #72 (by clausification #[71]): ∀ (a a_1 : Iota), Eq (∀ (X3 : Iota), Eq (rotate (s a) (cons a_1 X3)) (rotate a (x X3 (cons a_1 nil)))) True % 215.40/215.64 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), Eq (Eq (rotate (s a) (cons a_1 a_2)) (rotate a (x a_2 (cons a_1 nil)))) True % 215.40/215.64 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 : Iota), Eq (rotate (s a) (cons a_1 a_2)) (rotate a (x a_2 (cons a_1 nil))) % 215.40/215.64 Clause #75 (by superposition #[74, 30]): ∀ (a a_1 : Iota), Eq (rotate (s z) (cons a a_1)) (x a_1 (cons a nil)) % 215.40/215.67 Clause #77 (by superposition #[74, 64]): ∀ (a a_1 a_2 a_3 : Iota), Eq (rotate (s a) (cons a_1 (cons a_2 a_3))) (rotate a (cons a_2 (x a_3 (cons a_1 nil)))) % 215.40/215.67 Clause #78 (by clausification #[16]): Eq % 215.40/215.67 (Exists fun N => % 215.40/215.67 Exists fun M => % 215.40/215.67 Exists fun Ys => % 215.40/215.67 Exists fun Xs => % 215.40/215.67 Not % 215.40/215.67 (x2 N (length Xs) → % 215.40/215.67 x2 M (length Ys) → Eq Xs Ys → Ne (rotate (s z) Xs) Xs → Eq (rotate N Xs) (rotate M Ys) → Eq N M)) % 215.40/215.67 False % 215.40/215.67 Clause #79 (by clausification #[78]): ∀ (a : Iota), % 215.40/215.67 Eq % 215.40/215.67 (Exists fun M => % 215.40/215.67 Exists fun Ys => % 215.40/215.67 Exists fun Xs => % 215.40/215.67 Not % 215.40/215.67 (x2 a (length Xs) → % 215.40/215.67 x2 M (length Ys) → Eq Xs Ys → Ne (rotate (s z) Xs) Xs → Eq (rotate a Xs) (rotate M Ys) → Eq a M)) % 215.40/215.67 False % 215.40/215.67 Clause #80 (by clausification #[79]): ∀ (a a_1 : Iota), % 215.40/215.67 Eq % 215.40/215.67 (Exists fun Ys => % 215.40/215.67 Exists fun Xs => % 215.40/215.67 Not % 215.40/215.67 (x2 a (length Xs) → % 215.40/215.67 x2 a_1 (length Ys) → Eq Xs Ys → Ne (rotate (s z) Xs) Xs → Eq (rotate a Xs) (rotate a_1 Ys) → Eq a a_1)) % 215.40/215.67 False % 215.40/215.67 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 : Iota), % 215.40/215.67 Eq % 215.40/215.67 (Exists fun Xs => % 215.40/215.67 Not % 215.40/215.67 (x2 a (length Xs) → % 215.40/215.67 x2 a_1 (length a_2) → Eq Xs a_2 → Ne (rotate (s z) Xs) Xs → Eq (rotate a Xs) (rotate a_1 a_2) → Eq a a_1)) % 215.40/215.67 False % 215.40/215.67 Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.67 Eq % 215.40/215.67 (Not % 215.40/215.67 (x2 a (length a_1) → % 215.40/215.67 x2 a_2 (length a_3) → Eq a_1 a_3 → Ne (rotate (s z) a_1) a_1 → Eq (rotate a a_1) (rotate a_2 a_3) → Eq a a_2)) % 215.40/215.67 False % 215.40/215.67 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.67 Eq % 215.40/215.67 (x2 a (length a_1) → % 215.40/215.67 x2 a_2 (length a_3) → Eq a_1 a_3 → Ne (rotate (s z) a_1) a_1 → Eq (rotate a a_1) (rotate a_2 a_3) → Eq a a_2) % 215.40/215.67 True % 215.40/215.67 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.67 Or (Eq (x2 a (length a_1)) False) % 215.40/215.67 (Eq (x2 a_2 (length a_3) → Eq a_1 a_3 → Ne (rotate (s z) a_1) a_1 → Eq (rotate a a_1) (rotate a_2 a_3) → Eq a a_2) % 215.40/215.67 True) % 215.40/215.67 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.67 Or (Eq (x2 a (length a_1)) False) % 215.40/215.67 (Or (Eq (x2 a_2 (length a_3)) False) % 215.40/215.67 (Eq (Eq a_1 a_3 → Ne (rotate (s z) a_1) a_1 → Eq (rotate a a_1) (rotate a_2 a_3) → Eq a a_2) True)) % 215.40/215.67 Clause #86 (by clausification #[85]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.67 Or (Eq (x2 a (length a_1)) False) % 215.40/215.67 (Or (Eq (x2 a_2 (length a_3)) False) % 215.40/215.67 (Or (Eq (Eq a_1 a_3) False) % 215.40/215.67 (Eq (Ne (rotate (s z) a_1) a_1 → Eq (rotate a a_1) (rotate a_2 a_3) → Eq a a_2) True))) % 215.40/215.67 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.67 Or (Eq (x2 a (length a_1)) False) % 215.40/215.67 (Or (Eq (x2 a_2 (length a_3)) False) % 215.40/215.67 (Or (Eq (Ne (rotate (s z) a_1) a_1 → Eq (rotate a a_1) (rotate a_2 a_3) → Eq a a_2) True) (Ne a_1 a_3))) % 215.40/215.67 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.67 Or (Eq (x2 a (length a_1)) False) % 215.40/215.67 (Or (Eq (x2 a_2 (length a_3)) False) % 215.40/215.67 (Or (Ne a_1 a_3) % 215.40/215.67 (Or (Eq (Ne (rotate (s z) a_1) a_1) False) (Eq (Eq (rotate a a_1) (rotate a_2 a_3) → Eq a a_2) True)))) % 215.40/215.67 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.67 Or (Eq (x2 a (length a_1)) False) % 215.40/215.67 (Or (Eq (x2 a_2 (length a_3)) False) % 215.40/215.67 (Or (Ne a_1 a_3) (Or (Eq (Eq (rotate a a_1) (rotate a_2 a_3) → Eq a a_2) True) (Eq (rotate (s z) a_1) a_1)))) % 215.40/215.67 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.67 Or (Eq (x2 a (length a_1)) False) % 215.40/215.67 (Or (Eq (x2 a_2 (length a_3)) False) % 215.40/215.67 (Or (Ne a_1 a_3) % 215.40/215.67 (Or (Eq (rotate (s z) a_1) a_1) (Or (Eq (Eq (rotate a a_1) (rotate a_2 a_3)) False) (Eq (Eq a a_2) True))))) % 215.40/215.67 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.67 Or (Eq (x2 a (length a_1)) False) % 215.40/215.67 (Or (Eq (x2 a_2 (length a_3)) False) % 215.40/215.67 (Or (Ne a_1 a_3) (Or (Eq (rotate (s z) a_1) a_1) (Or (Eq (Eq a a_2) True) (Ne (rotate a a_1) (rotate a_2 a_3)))))) % 215.40/215.67 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.67 Or (Eq (x2 a (length a_1)) False) % 215.40/215.69 (Or (Eq (x2 a_2 (length a_3)) False) % 215.40/215.69 (Or (Ne a_1 a_3) (Or (Eq (rotate (s z) a_1) a_1) (Or (Ne (rotate a a_1) (rotate a_2 a_3)) (Eq a a_2))))) % 215.40/215.69 Clause #93 (by destructive equality resolution #[92]): ∀ (a a_1 a_2 : Iota), % 215.40/215.69 Or (Eq (x2 a (length a_1)) False) % 215.40/215.69 (Or (Eq (x2 a_2 (length a_1)) False) % 215.40/215.69 (Or (Eq (rotate (s z) a_1) a_1) (Or (Ne (rotate a a_1) (rotate a_2 a_1)) (Eq a a_2)))) % 215.40/215.69 Clause #95 (by superposition #[93, 54]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.69 Or (Eq (x2 a (s (length a_1))) False) % 215.40/215.69 (Or (Eq (x2 a_2 (s (length a_1))) False) % 215.40/215.69 (Or (Eq (rotate (s z) (cons a_3 a_1)) (cons a_3 a_1)) % 215.40/215.69 (Or (Ne (rotate a (cons a_3 a_1)) (rotate a_2 (cons a_3 a_1))) (Eq a a_2)))) % 215.40/215.69 Clause #98 (by superposition #[77, 75]): ∀ (a a_1 a_2 : Iota), Eq (rotate (s (s z)) (cons a (cons a_1 a_2))) (x (x a_2 (cons a nil)) (cons a_1 nil)) % 215.40/215.69 Clause #100 (by superposition #[77, 28]): ∀ (a a_1 a_2 : Iota), Eq (rotate (s a) (cons a_1 (cons a_2 nil))) (rotate a (cons a_2 (cons a_1 nil))) % 215.40/215.69 Clause #101 (by superposition #[77, 64]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.40/215.69 Eq (rotate (s a) (cons a_1 (cons a_2 (cons a_3 a_4)))) (rotate a (cons a_2 (cons a_3 (x a_4 (cons a_1 nil))))) % 215.40/215.69 Clause #102 (by superposition #[100, 75]): ∀ (a a_1 : Iota), Eq (rotate z (cons a (cons a_1 nil))) (x (cons a nil) (cons a_1 nil)) % 215.40/215.69 Clause #106 (by forward demodulation #[102, 30]): ∀ (a a_1 : Iota), Eq (cons a (cons a_1 nil)) (x (cons a nil) (cons a_1 nil)) % 215.40/215.69 Clause #107 (by superposition #[106, 77]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.69 Eq (rotate (s a) (cons a_1 (cons a_2 (cons a_3 nil)))) (rotate a (cons a_2 (cons a_3 (cons a_1 nil)))) % 215.40/215.69 Clause #114 (by superposition #[98, 77]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.40/215.69 Eq (rotate (s a) (cons a_1 (cons a_2 (x a_3 (cons a_4 nil))))) % 215.40/215.69 (rotate a (cons a_2 (rotate (s (s z)) (cons a_4 (cons a_1 a_3))))) % 215.40/215.69 Clause #116 (by superposition #[98, 106]): ∀ (a a_1 a_2 : Iota), % 215.40/215.69 Eq (rotate (s (s z)) (cons a (cons a_1 (cons a_2 nil)))) (x (cons a_2 (cons a nil)) (cons a_1 nil)) % 215.40/215.69 Clause #122 (by superposition #[95, 19]): ∀ (a a_1 a_2 : Iota), % 215.40/215.69 Or (Eq (x2 a (s (length a_1))) False) % 215.40/215.69 (Or (Eq (rotate (s z) (cons a_2 a_1)) (cons a_2 a_1)) % 215.40/215.69 (Or (Ne (rotate z (cons a_2 a_1)) (rotate a (cons a_2 a_1))) (Or (Eq z a) (Eq False True)))) % 215.40/215.69 Clause #125 (by superposition #[107, 75]): ∀ (a a_1 a_2 : Iota), Eq (rotate z (cons a (cons a_1 (cons a_2 nil)))) (x (cons a (cons a_1 nil)) (cons a_2 nil)) % 215.40/215.69 Clause #128 (by forward demodulation #[125, 30]): ∀ (a a_1 a_2 : Iota), Eq (cons a (cons a_1 (cons a_2 nil))) (x (cons a (cons a_1 nil)) (cons a_2 nil)) % 215.40/215.69 Clause #133 (by forward demodulation #[116, 128]): ∀ (a a_1 a_2 : Iota), Eq (rotate (s (s z)) (cons a (cons a_1 (cons a_2 nil)))) (cons a_2 (cons a (cons a_1 nil))) % 215.40/215.69 Clause #136 (by superposition #[101, 30]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.69 Eq (rotate (s z) (cons a (cons a_1 (cons a_2 a_3)))) (cons a_1 (cons a_2 (x a_3 (cons a nil)))) % 215.40/215.69 Clause #141 (by superposition #[136, 75]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cons a (cons a_1 (x a_2 (cons a_3 nil)))) (x (cons a (cons a_1 a_2)) (cons a_3 nil)) % 215.40/215.69 Clause #159 (by forward demodulation #[114, 101]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.40/215.69 Eq (rotate (s (s a)) (cons a_1 (cons a_2 (cons a_3 a_4)))) % 215.40/215.69 (rotate a (cons a_3 (rotate (s (s z)) (cons a_1 (cons a_2 a_4))))) % 215.40/215.69 Clause #161 (by superposition #[159, 30]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.69 Eq (rotate (s (s z)) (cons a (cons a_1 (cons a_2 a_3)))) (cons a_2 (rotate (s (s z)) (cons a (cons a_1 a_3)))) % 215.40/215.69 Clause #213 (by clausification #[122]): ∀ (a a_1 a_2 : Iota), % 215.40/215.69 Or (Eq (x2 a (s (length a_1))) False) % 215.40/215.69 (Or (Eq (rotate (s z) (cons a_2 a_1)) (cons a_2 a_1)) % 215.40/215.69 (Or (Ne (rotate z (cons a_2 a_1)) (rotate a (cons a_2 a_1))) (Eq z a))) % 215.40/215.69 Clause #214 (by forward demodulation #[213, 30]): ∀ (a a_1 a_2 : Iota), % 215.40/215.69 Or (Eq (x2 a (s (length a_1))) False) % 215.40/215.69 (Or (Eq (rotate (s z) (cons a_2 a_1)) (cons a_2 a_1)) (Or (Ne (cons a_2 a_1) (rotate a (cons a_2 a_1))) (Eq z a))) % 215.40/215.69 Clause #217 (by superposition #[214, 54]): ∀ (a a_1 a_2 a_3 : Iota), % 215.40/215.69 Or (Eq (x2 a (s (s (length a_1)))) False) % 215.40/215.69 (Or (Eq (rotate (s z) (cons a_2 (cons a_3 a_1))) (cons a_2 (cons a_3 a_1))) % 215.50/215.78 (Or (Ne (cons a_2 (cons a_3 a_1)) (rotate a (cons a_2 (cons a_3 a_1)))) (Eq z a))) % 215.50/215.78 Clause #791 (by superposition #[217, 54]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.50/215.78 Or (Eq (x2 a (s (s (s (length a_1))))) False) % 215.50/215.78 (Or (Eq (rotate (s z) (cons a_2 (cons a_3 (cons a_4 a_1)))) (cons a_2 (cons a_3 (cons a_4 a_1)))) % 215.50/215.78 (Or (Ne (cons a_2 (cons a_3 (cons a_4 a_1))) (rotate a (cons a_2 (cons a_3 (cons a_4 a_1))))) (Eq z a))) % 215.50/215.78 Clause #7101 (by superposition #[791, 49]): ∀ (a a_1 a_2 a_3 : Iota), % 215.50/215.78 Or (Eq (rotate (s z) (cons a (cons a_1 (cons a_2 a_3)))) (cons a (cons a_1 (cons a_2 a_3)))) % 215.50/215.78 (Or (Ne (cons a (cons a_1 (cons a_2 a_3))) (rotate (s (s z)) (cons a (cons a_1 (cons a_2 a_3))))) % 215.50/215.78 (Or (Eq z (s (s z))) (Eq False True))) % 215.50/215.78 Clause #7106 (by clausification #[7101]): ∀ (a a_1 a_2 a_3 : Iota), % 215.50/215.78 Or (Eq (rotate (s z) (cons a (cons a_1 (cons a_2 a_3)))) (cons a (cons a_1 (cons a_2 a_3)))) % 215.50/215.78 (Or (Ne (cons a (cons a_1 (cons a_2 a_3))) (rotate (s (s z)) (cons a (cons a_1 (cons a_2 a_3))))) (Eq z (s (s z)))) % 215.50/215.78 Clause #7107 (by forward demodulation #[7106, 75]): ∀ (a a_1 a_2 a_3 : Iota), % 215.50/215.78 Or (Eq (x (cons a (cons a_1 a_2)) (cons a_3 nil)) (cons a_3 (cons a (cons a_1 a_2)))) % 215.50/215.78 (Or (Ne (cons a_3 (cons a (cons a_1 a_2))) (rotate (s (s z)) (cons a_3 (cons a (cons a_1 a_2))))) (Eq z (s (s z)))) % 215.50/215.78 Clause #7108 (by forward demodulation #[7107, 141]): ∀ (a a_1 a_2 a_3 : Iota), % 215.50/215.78 Or (Eq (cons a (cons a_1 (x a_2 (cons a_3 nil)))) (cons a_3 (cons a (cons a_1 a_2)))) % 215.50/215.78 (Or (Ne (cons a_3 (cons a (cons a_1 a_2))) (rotate (s (s z)) (cons a_3 (cons a (cons a_1 a_2))))) (Eq z (s (s z)))) % 215.50/215.78 Clause #7109 (by forward demodulation #[7108, 161]): ∀ (a a_1 a_2 a_3 : Iota), % 215.50/215.78 Or (Eq (cons a (cons a_1 (x a_2 (cons a_3 nil)))) (cons a_3 (cons a (cons a_1 a_2)))) % 215.50/215.78 (Or (Ne (cons a_3 (cons a (cons a_1 a_2))) (cons a_1 (rotate (s (s z)) (cons a_3 (cons a a_2))))) (Eq z (s (s z)))) % 215.50/215.78 Clause #7110 (by forward contextual literal cutting #[7109, 23]): ∀ (a a_1 a_2 a_3 : Iota), % 215.50/215.78 Or (Eq (cons a (cons a_1 (x a_2 (cons a_3 nil)))) (cons a_3 (cons a (cons a_1 a_2)))) % 215.50/215.78 (Ne (cons a_3 (cons a (cons a_1 a_2))) (cons a_1 (rotate (s (s z)) (cons a_3 (cons a a_2))))) % 215.50/215.78 Clause #7114 (by superposition #[7110, 133]): ∀ (a a_1 a_2 a_3 : Iota), % 215.50/215.78 Or (Eq (cons a (cons a_1 (x (cons a_2 nil) (cons a_3 nil)))) (cons a_3 (cons a (cons a_1 (cons a_2 nil))))) % 215.50/215.78 (Ne (cons a_3 (cons a (cons a_1 (cons a_2 nil)))) (cons a_1 (cons a_2 (cons a_3 (cons a nil))))) % 215.50/215.78 Clause #7186 (by forward demodulation #[7114, 106]): ∀ (a a_1 a_2 a_3 : Iota), % 215.50/215.78 Or (Eq (cons a (cons a_1 (cons a_2 (cons a_3 nil)))) (cons a_3 (cons a (cons a_1 (cons a_2 nil))))) % 215.50/215.78 (Ne (cons a_3 (cons a (cons a_1 (cons a_2 nil)))) (cons a_1 (cons a_2 (cons a_3 (cons a nil))))) % 215.50/215.78 Clause #7187 (by equality resolution #[7186]): ∀ (a a_1 : Iota), Eq (cons a (cons a_1 (cons a (cons a_1 nil)))) (cons a_1 (cons a (cons a_1 (cons a nil)))) % 215.50/215.78 Clause #7427 (by superposition #[7187, 26]): ∀ (a a_1 : Iota), Eq (head (cons a (cons a_1 (cons a (cons a_1 nil))))) a_1 % 215.50/215.78 Clause #7528 (by superposition #[7427, 26]): ∀ (a a_1 : Iota), Eq a a_1 % 215.50/215.78 Clause #7540 (by backward contextual literal cutting #[7528, 23]): False % 215.50/215.78 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------