%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL686+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:36:27 AM UTC 2026 % Result : Theorem 13.37s 13.64s % Output : Proof 13.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL686+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : duper %s % 0.10/0.36 % Computer : n018.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Sat Sep 5 09:52:18 UTC 2026 % 0.10/0.36 % CPUTime : % 13.37/13.64 SZS status Theorem for theBenchmark.p % 13.37/13.64 SZS output start Proof for theBenchmark.p % 13.37/13.64 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), r1 X X) True % 13.37/13.64 Clause #2 (by assumption #[]): Eq % 13.37/13.64 (Not % 13.37/13.64 (Not % 13.37/13.64 (Exists fun X => % 13.37/13.64 Not % 13.37/13.64 (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (Not (p3 Y))) (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X)))) % 13.37/13.64 (∀ (Y : Iota), % 13.37/13.64 Or (Not (r1 X Y)) % 13.37/13.64 (Not % 13.37/13.64 (∀ (X : Iota), % 13.37/13.64 Or (Not (r1 Y X)) % 13.37/13.64 (Not % 13.37/13.64 (Or % 13.37/13.64 (Or % 13.37/13.64 (Or (∀ (Y : Iota), Or (Not (r1 X Y)) False) % 13.37/13.64 (Not % 13.37/13.64 (∀ (Y : Iota), % 13.37/13.64 Or (Not (r1 X Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.37/13.64 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 13.37/13.64 (∀ (Y : Iota), % 13.37/13.64 Or (Or (Not (r1 X Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y)))))))))))) % 13.37/13.64 True % 13.37/13.64 Clause #3 (by clausification #[0]): ∀ (a : Iota), Eq (r1 a a) True % 13.37/13.64 Clause #11 (by clausification #[2]): Eq % 13.37/13.64 (Not % 13.37/13.64 (Exists fun X => % 13.37/13.64 Not % 13.37/13.64 (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (Not (p3 Y))) (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X)))) % 13.37/13.64 (∀ (Y : Iota), % 13.37/13.64 Or (Not (r1 X Y)) % 13.37/13.64 (Not % 13.37/13.64 (∀ (X : Iota), % 13.37/13.64 Or (Not (r1 Y X)) % 13.37/13.64 (Not % 13.37/13.64 (Or % 13.37/13.64 (Or % 13.37/13.64 (Or (∀ (Y : Iota), Or (Not (r1 X Y)) False) % 13.37/13.64 (Not % 13.37/13.64 (∀ (Y : Iota), % 13.37/13.64 Or (Not (r1 X Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.37/13.64 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 13.37/13.64 (∀ (Y : Iota), % 13.37/13.64 Or (Or (Not (r1 X Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y))))))))))) % 13.37/13.64 False % 13.37/13.64 Clause #12 (by clausification #[11]): Eq % 13.37/13.64 (Exists fun X => % 13.37/13.64 Not % 13.37/13.64 (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (Not (p3 Y))) (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X)))) % 13.37/13.64 (∀ (Y : Iota), % 13.37/13.64 Or (Not (r1 X Y)) % 13.37/13.64 (Not % 13.37/13.64 (∀ (X : Iota), % 13.37/13.64 Or (Not (r1 Y X)) % 13.37/13.64 (Not % 13.37/13.64 (Or % 13.37/13.64 (Or % 13.37/13.64 (Or (∀ (Y : Iota), Or (Not (r1 X Y)) False) % 13.37/13.64 (Not % 13.37/13.64 (∀ (Y : Iota), % 13.37/13.64 Or (Not (r1 X Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.37/13.64 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 13.37/13.64 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y)))))))))) % 13.37/13.64 True % 13.37/13.64 Clause #13 (by clausification #[12]): ∀ (a : Iota), % 13.37/13.64 Eq % 13.37/13.64 (Not % 13.37/13.64 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p3 Y))) (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X)))) % 13.37/13.64 (∀ (Y : Iota), % 13.37/13.64 Or (Not (r1 (skS.0 0 a) Y)) % 13.37/13.64 (Not % 13.37/13.64 (∀ (X : Iota), % 13.37/13.64 Or (Not (r1 Y X)) % 13.37/13.64 (Not % 13.37/13.64 (Or % 13.37/13.64 (Or % 13.37/13.64 (Or (∀ (Y : Iota), Or (Not (r1 X Y)) False) % 13.37/13.64 (Not % 13.37/13.64 (∀ (Y : Iota), % 13.37/13.64 Or (Not (r1 X Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.37/13.64 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 13.37/13.64 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y)))))))))) % 13.37/13.64 True % 13.37/13.64 Clause #14 (by clausification #[13]): ∀ (a : Iota), % 13.37/13.64 Eq % 13.37/13.64 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p3 Y))) (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X)))) % 13.37/13.64 (∀ (Y : Iota), % 13.37/13.64 Or (Not (r1 (skS.0 0 a) Y)) % 13.37/13.64 (Not % 13.37/13.64 (∀ (X : Iota), % 13.37/13.64 Or (Not (r1 Y X)) % 13.37/13.69 (Not % 13.37/13.69 (Or % 13.37/13.69 (Or % 13.37/13.69 (Or (∀ (Y : Iota), Or (Not (r1 X Y)) False) % 13.37/13.69 (Not % 13.37/13.69 (∀ (Y : Iota), % 13.37/13.69 Or (Not (r1 X Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.37/13.69 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 13.37/13.69 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y))))))))) % 13.37/13.69 False % 13.37/13.69 Clause #15 (by clausification #[14]): ∀ (a : Iota), % 13.37/13.69 Eq % 13.37/13.69 (∀ (Y : Iota), % 13.37/13.69 Or (Not (r1 (skS.0 0 a) Y)) % 13.37/13.69 (Not % 13.37/13.69 (∀ (X : Iota), % 13.37/13.69 Or (Not (r1 Y X)) % 13.37/13.69 (Not % 13.37/13.69 (Or % 13.37/13.69 (Or % 13.37/13.69 (Or (∀ (Y : Iota), Or (Not (r1 X Y)) False) % 13.37/13.69 (Not % 13.37/13.69 (∀ (Y : Iota), % 13.37/13.69 Or (Not (r1 X Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.37/13.69 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 13.37/13.69 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y)))))))) % 13.37/13.69 False % 13.37/13.69 Clause #17 (by clausification #[15]): ∀ (a a_1 : Iota), % 13.37/13.69 Eq % 13.37/13.69 (Not % 13.37/13.69 (Or (Not (r1 (skS.0 0 a) (skS.0 1 a a_1))) % 13.37/13.69 (Not % 13.37/13.69 (∀ (X : Iota), % 13.37/13.69 Or (Not (r1 (skS.0 1 a a_1) X)) % 13.37/13.69 (Not % 13.37/13.69 (Or % 13.37/13.69 (Or % 13.37/13.69 (Or (∀ (Y : Iota), Or (Not (r1 X Y)) False) % 13.37/13.69 (Not % 13.37/13.69 (∀ (Y : Iota), % 13.37/13.69 Or (Not (r1 X Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.37/13.69 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 13.37/13.69 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y))))))))) % 13.37/13.69 True % 13.37/13.69 Clause #18 (by clausification #[17]): ∀ (a a_1 : Iota), % 13.37/13.69 Eq % 13.37/13.69 (Or (Not (r1 (skS.0 0 a) (skS.0 1 a a_1))) % 13.37/13.69 (Not % 13.37/13.69 (∀ (X : Iota), % 13.37/13.69 Or (Not (r1 (skS.0 1 a a_1) X)) % 13.37/13.69 (Not % 13.37/13.69 (Or % 13.37/13.69 (Or % 13.37/13.69 (Or (∀ (Y : Iota), Or (Not (r1 X Y)) False) % 13.37/13.69 (Not % 13.37/13.69 (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.37/13.69 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 13.37/13.69 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y)))))))) % 13.37/13.69 False % 13.37/13.69 Clause #19 (by clausification #[18]): ∀ (a a_1 : Iota), % 13.37/13.69 Eq % 13.37/13.69 (Not % 13.37/13.69 (∀ (X : Iota), % 13.37/13.69 Or (Not (r1 (skS.0 1 a a_1) X)) % 13.37/13.69 (Not % 13.37/13.69 (Or % 13.37/13.69 (Or % 13.37/13.69 (Or (∀ (Y : Iota), Or (Not (r1 X Y)) False) % 13.37/13.69 (Not % 13.37/13.69 (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.37/13.69 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 13.37/13.69 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y))))))) % 13.37/13.69 False % 13.37/13.69 Clause #21 (by clausification #[19]): ∀ (a a_1 : Iota), % 13.37/13.69 Eq % 13.37/13.69 (∀ (X : Iota), % 13.37/13.69 Or (Not (r1 (skS.0 1 a a_1) X)) % 13.37/13.69 (Not % 13.37/13.69 (Or % 13.37/13.69 (Or % 13.37/13.69 (Or (∀ (Y : Iota), Or (Not (r1 X Y)) False) % 13.37/13.69 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.37/13.69 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 13.37/13.69 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y)))))) % 13.37/13.69 True % 13.37/13.69 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 : Iota), % 13.37/13.69 Eq % 13.37/13.69 (Or (Not (r1 (skS.0 1 a a_1) a_2)) % 13.37/13.69 (Not % 13.37/13.69 (Or % 13.37/13.69 (Or % 13.37/13.69 (Or (∀ (Y : Iota), Or (Not (r1 a_2 Y)) False) % 13.37/13.69 (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.37/13.69 (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p3 Y))) % 13.37/13.69 (∀ (Y : Iota), Or (Or (Not (r1 a_2 Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y)))))) % 13.47/13.76 True % 13.47/13.76 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 : Iota), % 13.47/13.76 Or (Eq (Not (r1 (skS.0 1 a a_1) a_2)) True) % 13.47/13.76 (Eq % 13.47/13.76 (Not % 13.47/13.76 (Or % 13.47/13.76 (Or % 13.47/13.76 (Or (∀ (Y : Iota), Or (Not (r1 a_2 Y)) False) % 13.47/13.76 (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.47/13.76 (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p3 Y))) % 13.47/13.76 (∀ (Y : Iota), Or (Or (Not (r1 a_2 Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y))))) % 13.47/13.76 True) % 13.47/13.76 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 : Iota), % 13.47/13.76 Or % 13.47/13.76 (Eq % 13.47/13.76 (Not % 13.47/13.76 (Or % 13.47/13.76 (Or % 13.47/13.76 (Or (∀ (Y : Iota), Or (Not (r1 a Y)) False) % 13.47/13.76 (Not (∀ (Y : Iota), Or (Not (r1 a Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.47/13.76 (∀ (Y : Iota), Or (Not (r1 a Y)) (p3 Y))) % 13.47/13.76 (∀ (Y : Iota), Or (Or (Not (r1 a Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y))))) % 13.47/13.76 True) % 13.47/13.76 (Eq (r1 (skS.0 1 a_1 a_2) a) False) % 13.47/13.76 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), % 13.47/13.76 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.47/13.76 (Eq % 13.47/13.76 (Or % 13.47/13.76 (Or % 13.47/13.76 (Or (∀ (Y : Iota), Or (Not (r1 a_2 Y)) False) % 13.47/13.76 (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.47/13.76 (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p3 Y))) % 13.47/13.76 (∀ (Y : Iota), Or (Or (Not (r1 a_2 Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y)))) % 13.47/13.76 False) % 13.47/13.76 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), % 13.47/13.76 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.47/13.76 (Eq (∀ (Y : Iota), Or (Or (Not (r1 a_2 Y)) (And (Not (p1 Y)) (Not (p2 Y)))) (And (p2 Y) (p1 Y))) False) % 13.47/13.76 Clause #27 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), % 13.47/13.76 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.47/13.76 (Eq % 13.47/13.76 (Or % 13.47/13.76 (Or (∀ (Y : Iota), Or (Not (r1 a_2 Y)) False) % 13.47/13.76 (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.47/13.76 (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p3 Y))) % 13.47/13.76 False) % 13.47/13.76 Clause #28 (by clausification #[26]): ∀ (a a_1 a_2 a_3 : Iota), % 13.47/13.76 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.47/13.76 (Eq % 13.47/13.76 (Not % 13.47/13.76 (Or (Or (Not (r1 a_2 (skS.0 2 a_2 a_3))) (And (Not (p1 (skS.0 2 a_2 a_3))) (Not (p2 (skS.0 2 a_2 a_3))))) % 13.47/13.76 (And (p2 (skS.0 2 a_2 a_3)) (p1 (skS.0 2 a_2 a_3))))) % 13.47/13.76 True) % 13.47/13.76 Clause #29 (by clausification #[28]): ∀ (a a_1 a_2 a_3 : Iota), % 13.47/13.76 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.47/13.76 (Eq % 13.47/13.76 (Or (Or (Not (r1 a_2 (skS.0 2 a_2 a_3))) (And (Not (p1 (skS.0 2 a_2 a_3))) (Not (p2 (skS.0 2 a_2 a_3))))) % 13.47/13.76 (And (p2 (skS.0 2 a_2 a_3)) (p1 (skS.0 2 a_2 a_3)))) % 13.47/13.76 False) % 13.47/13.76 Clause #30 (by clausification #[29]): ∀ (a a_1 a_2 a_3 : Iota), % 13.47/13.76 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Eq (And (p2 (skS.0 2 a_2 a_3)) (p1 (skS.0 2 a_2 a_3))) False) % 13.47/13.76 Clause #31 (by clausification #[29]): ∀ (a a_1 a_2 a_3 : Iota), % 13.47/13.76 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.47/13.76 (Eq (Or (Not (r1 a_2 (skS.0 2 a_2 a_3))) (And (Not (p1 (skS.0 2 a_2 a_3))) (Not (p2 (skS.0 2 a_2 a_3))))) False) % 13.47/13.76 Clause #32 (by clausification #[30]): ∀ (a a_1 a_2 a_3 : Iota), % 13.47/13.76 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (p2 (skS.0 2 a_2 a_3)) False) (Eq (p1 (skS.0 2 a_2 a_3)) False)) % 13.47/13.76 Clause #33 (by superposition #[32, 3]): ∀ (a a_1 a_2 : Iota), % 13.47/13.76 Or (Eq (p2 (skS.0 2 (skS.0 1 a a_1) a_2)) False) (Or (Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) False) (Eq False True)) % 13.47/13.76 Clause #52 (by clausification #[27]): ∀ (a a_1 a_2 : Iota), % 13.47/13.76 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.47/13.76 (Eq % 13.47/13.76 (Or (∀ (Y : Iota), Or (Not (r1 a_2 Y)) False) % 13.47/13.76 (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))))) % 13.47/13.76 False) % 13.47/13.76 Clause #70 (by clausification #[31]): ∀ (a a_1 a_2 a_3 : Iota), % 13.47/13.76 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Eq (And (Not (p1 (skS.0 2 a_2 a_3))) (Not (p2 (skS.0 2 a_2 a_3)))) False) % 13.47/13.76 Clause #71 (by clausification #[31]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Eq (Not (r1 a_2 (skS.0 2 a_2 a_3))) False) % 13.57/13.83 Clause #72 (by clausification #[70]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.57/13.83 (Or (Eq (Not (p1 (skS.0 2 a_2 a_3))) False) (Eq (Not (p2 (skS.0 2 a_2 a_3))) False)) % 13.57/13.83 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (Not (p2 (skS.0 2 a_2 a_3))) False) (Eq (p1 (skS.0 2 a_2 a_3)) True)) % 13.57/13.83 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (p1 (skS.0 2 a_2 a_3)) True) (Eq (p2 (skS.0 2 a_2 a_3)) True)) % 13.57/13.83 Clause #76 (by superposition #[74, 3]): ∀ (a a_1 a_2 : Iota), % 13.57/13.83 Or (Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) True) (Or (Eq (p2 (skS.0 2 (skS.0 1 a a_1) a_2)) True) (Eq False True)) % 13.57/13.83 Clause #77 (by clausification #[71]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Eq (r1 a_2 (skS.0 2 a_2 a_3)) True) % 13.57/13.83 Clause #79 (by superposition #[77, 3]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 1 a a_1) (skS.0 2 (skS.0 1 a a_1) a_2)) True) (Eq False True) % 13.57/13.83 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 1 a a_1) (skS.0 2 (skS.0 1 a a_1) a_2)) True % 13.57/13.83 Clause #94 (by clausification #[33]): ∀ (a a_1 a_2 : Iota), Or (Eq (p2 (skS.0 2 (skS.0 1 a a_1) a_2)) False) (Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) False) % 13.57/13.83 Clause #103 (by clausification #[52]): ∀ (a a_1 a_2 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.57/13.83 (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y)))))) False) % 13.57/13.83 Clause #105 (by clausification #[103]): ∀ (a a_1 a_2 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.57/13.83 (Eq (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (Or (And (p2 Y) (Not (p1 Y))) (And (Not (p2 Y)) (p1 Y))))) True) % 13.57/13.83 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.57/13.83 (Eq (Or (Not (r1 a_2 a_3)) (Not (Or (And (p2 a_3) (Not (p1 a_3))) (And (Not (p2 a_3)) (p1 a_3))))) True) % 13.57/13.83 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.57/13.83 (Or (Eq (Not (r1 a_2 a_3)) True) (Eq (Not (Or (And (p2 a_3) (Not (p1 a_3))) (And (Not (p2 a_3)) (p1 a_3)))) True)) % 13.57/13.83 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.57/13.83 (Or (Eq (Not (Or (And (p2 a_3) (Not (p1 a_3))) (And (Not (p2 a_3)) (p1 a_3)))) True) (Eq (r1 a_2 a_3) False)) % 13.57/13.83 Clause #109 (by clausification #[108]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 13.57/13.83 (Or (Eq (r1 a_2 a_3) False) (Eq (Or (And (p2 a_3) (Not (p1 a_3))) (And (Not (p2 a_3)) (p1 a_3))) False)) % 13.57/13.83 Clause #110 (by clausification #[109]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (r1 a_2 a_3) False) (Eq (And (Not (p2 a_3)) (p1 a_3)) False)) % 13.57/13.83 Clause #111 (by clausification #[109]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (r1 a_2 a_3) False) (Eq (And (p2 a_3) (Not (p1 a_3))) False)) % 13.57/13.83 Clause #112 (by clausification #[110]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (r1 a_2 a_3) False) (Or (Eq (Not (p2 a_3)) False) (Eq (p1 a_3) False))) % 13.57/13.83 Clause #113 (by clausification #[112]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (r1 a_2 a_3) False) (Or (Eq (p1 a_3) False) (Eq (p2 a_3) True))) % 13.57/13.83 Clause #116 (by superposition #[113, 3]): ∀ (a a_1 a_2 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (p1 a_2) False) (Or (Eq (p2 a_2) True) (Eq False True))) % 13.57/13.83 Clause #117 (by clausification #[116]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (p1 a_2) False) (Eq (p2 a_2) True)) % 13.57/13.83 Clause #119 (by superposition #[117, 80]): ∀ (a a_1 a_2 : Iota), % 13.57/13.83 Or (Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) False) (Or (Eq (p2 (skS.0 2 (skS.0 1 a a_1) a_2)) True) (Eq False True)) % 13.57/13.83 Clause #125 (by clausification #[111]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.83 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (r1 a_2 a_3) False) (Or (Eq (p2 a_3) False) (Eq (Not (p1 a_3)) False))) % 13.57/13.83 Clause #126 (by clausification #[125]): ∀ (a a_1 a_2 a_3 : Iota), % 13.57/13.87 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (r1 a_2 a_3) False) (Or (Eq (p2 a_3) False) (Eq (p1 a_3) True))) % 13.57/13.87 Clause #129 (by superposition #[126, 3]): ∀ (a a_1 a_2 : Iota), % 13.57/13.87 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (p2 a_2) False) (Or (Eq (p1 a_2) True) (Eq False True))) % 13.57/13.87 Clause #130 (by clausification #[129]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (p2 a_2) False) (Eq (p1 a_2) True)) % 13.57/13.87 Clause #132 (by superposition #[130, 80]): ∀ (a a_1 a_2 : Iota), % 13.57/13.87 Or (Eq (p2 (skS.0 2 (skS.0 1 a a_1) a_2)) False) (Or (Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) True) (Eq False True)) % 13.57/13.87 Clause #184 (by clausification #[76]): ∀ (a a_1 a_2 : Iota), Or (Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) True) (Eq (p2 (skS.0 2 (skS.0 1 a a_1) a_2)) True) % 13.57/13.87 Clause #257 (by clausification #[119]): ∀ (a a_1 a_2 : Iota), Or (Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) False) (Eq (p2 (skS.0 2 (skS.0 1 a a_1) a_2)) True) % 13.57/13.87 Clause #258 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), Or (Eq (p2 (skS.0 2 (skS.0 1 a a_1) a_2)) False) (Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) True) % 13.57/13.87 Clause #259 (by superposition #[258, 184]): ∀ (a a_1 a_2 : Iota), % 13.57/13.87 Or (Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) True) (Or (Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) True) (Eq False True)) % 13.57/13.87 Clause #287 (by clausification #[259]): ∀ (a a_1 a_2 : Iota), Or (Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) True) (Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) True) % 13.57/13.87 Clause #288 (by eliminate duplicate literals #[287]): ∀ (a a_1 a_2 : Iota), Eq (p1 (skS.0 2 (skS.0 1 a a_1) a_2)) True % 13.57/13.87 Clause #289 (by backward demodulation #[288, 94]): ∀ (a a_1 a_2 : Iota), Or (Eq (p2 (skS.0 2 (skS.0 1 a a_1) a_2)) False) (Eq True False) % 13.57/13.87 Clause #291 (by backward demodulation #[288, 257]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (p2 (skS.0 2 (skS.0 1 a a_1) a_2)) True) % 13.57/13.87 Clause #299 (by clausification #[291]): ∀ (a a_1 a_2 : Iota), Eq (p2 (skS.0 2 (skS.0 1 a a_1) a_2)) True % 13.57/13.87 Clause #300 (by clausification #[289]): ∀ (a a_1 a_2 : Iota), Eq (p2 (skS.0 2 (skS.0 1 a a_1) a_2)) False % 13.57/13.87 Clause #301 (by superposition #[300, 299]): Eq False True % 13.57/13.87 Clause #302 (by clausification #[301]): False % 13.57/13.87 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------