%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ALG036+1 : TPTP v9.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n010.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 07:43:56 PM UTC 2025 % Result : Theorem 5.72s 5.88s % Output : Proof 5.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : ALG036+1 : TPTP v9.2.0. Released v2.7.0. % 0.11/0.13 % Command : duper %s % 0.12/0.33 % Computer : n010.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Oct 3 09:33:23 EDT 2025 % 0.12/0.33 % CPUTime : % 5.72/5.88 SZS status Theorem for theBenchmark.p % 5.72/5.88 SZS output start Proof for theBenchmark.p % 5.72/5.88 Clause #1 (by assumption #[]): Eq % 5.72/5.88 (And % 5.72/5.88 (And % 5.72/5.88 (And % 5.72/5.88 (And % 5.72/5.88 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 5.72/5.88 (Eq (op unit e2) e2)) % 5.72/5.88 (Eq (op e2 unit) e2)) % 5.72/5.88 (Eq (op unit e3) e3)) % 5.72/5.88 (Eq (op e3 unit) e3)) % 5.72/5.88 (Or (Or (Or (Eq unit e0) (Eq unit e1)) (Eq unit e2)) (Eq unit e3))) % 5.72/5.88 True % 5.72/5.88 Clause #3 (by assumption #[]): Eq (Eq unit e0) True % 5.72/5.88 Clause #5 (by assumption #[]): Eq (And (And (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e1 e2)) (Ne e1 e3)) (Ne e2 e3)) True % 5.72/5.88 Clause #6 (by assumption #[]): Eq % 5.72/5.88 (Not % 5.72/5.88 (Or % 5.72/5.88 (Or % 5.72/5.88 (Or % 5.72/5.88 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.72/5.88 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.72/5.88 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 5.72/5.88 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 5.72/5.88 (Not % 5.72/5.88 (Or % 5.72/5.88 (Or % 5.72/5.88 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.72/5.88 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.72/5.88 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 5.72/5.88 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3)))))) % 5.72/5.88 True % 5.72/5.88 Clause #7 (by clausification #[3]): Eq unit e0 % 5.72/5.88 Clause #8 (by clausification #[5]): Eq (Ne e2 e3) True % 5.72/5.88 Clause #9 (by clausification #[5]): Eq (And (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e1 e2)) (Ne e1 e3)) True % 5.72/5.88 Clause #10 (by clausification #[8]): Ne e2 e3 % 5.72/5.88 Clause #11 (by clausification #[9]): Eq (Ne e1 e3) True % 5.72/5.88 Clause #12 (by clausification #[9]): Eq (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e1 e2)) True % 5.72/5.88 Clause #13 (by clausification #[11]): Ne e1 e3 % 5.72/5.88 Clause #14 (by clausification #[12]): Eq (Ne e1 e2) True % 5.72/5.88 Clause #15 (by clausification #[12]): Eq (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) True % 5.72/5.88 Clause #16 (by clausification #[14]): Ne e1 e2 % 5.72/5.88 Clause #17 (by clausification #[15]): Eq (Ne e0 e3) True % 5.72/5.88 Clause #18 (by clausification #[15]): Eq (And (Ne e0 e1) (Ne e0 e2)) True % 5.72/5.88 Clause #19 (by clausification #[17]): Ne e0 e3 % 5.72/5.88 Clause #32 (by clausification #[18]): Eq (Ne e0 e2) True % 5.72/5.88 Clause #33 (by clausification #[18]): Eq (Ne e0 e1) True % 5.72/5.88 Clause #34 (by clausification #[32]): Ne e0 e2 % 5.72/5.88 Clause #35 (by clausification #[33]): Ne e0 e1 % 5.72/5.88 Clause #37 (by clausification #[1]): Eq % 5.72/5.88 (And % 5.72/5.88 (And % 5.72/5.88 (And % 5.72/5.88 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 5.72/5.88 (Eq (op unit e2) e2)) % 5.72/5.88 (Eq (op e2 unit) e2)) % 5.72/5.88 (Eq (op unit e3) e3)) % 5.72/5.88 (Eq (op e3 unit) e3)) % 5.72/5.88 True % 5.72/5.88 Clause #48 (by clausification #[37]): Eq % 5.72/5.88 (And % 5.72/5.88 (And % 5.72/5.88 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 5.72/5.88 (Eq (op unit e2) e2)) % 5.72/5.88 (Eq (op e2 unit) e2)) % 5.72/5.88 (Eq (op unit e3) e3)) % 5.72/5.88 True % 5.72/5.88 Clause #52 (by clausification #[48]): Eq % 5.72/5.88 (And % 5.72/5.88 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 5.72/5.88 (Eq (op unit e2) e2)) % 5.72/5.88 (Eq (op e2 unit) e2)) % 5.72/5.88 True % 5.72/5.88 Clause #56 (by clausification #[52]): Eq % 5.72/5.88 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 5.72/5.88 (Eq (op unit e2) e2)) % 5.72/5.88 True % 5.72/5.88 Clause #60 (by clausification #[56]): Eq (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) True % 5.72/5.88 Clause #64 (by clausification #[60]): Eq (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) True % 5.72/5.88 Clause #78 (by clausification #[64]): Eq (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) True % 5.72/5.88 Clause #81 (by clausification #[78]): Eq (Eq (op e0 unit) e0) True % 5.72/5.88 Clause #83 (by clausification #[81]): Eq (op e0 unit) e0 % 5.74/5.91 Clause #84 (by forward demodulation #[83, 7]): Eq (op e0 e0) e0 % 5.74/5.91 Clause #86 (by clausification #[6]): Eq % 5.74/5.91 (Or % 5.74/5.91 (Or % 5.74/5.91 (Or % 5.74/5.91 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 5.74/5.91 (Not % 5.74/5.91 (Or % 5.74/5.91 (Or % 5.74/5.91 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))))) % 5.74/5.91 False % 5.74/5.91 Clause #87 (by clausification #[86]): Eq % 5.74/5.91 (Not % 5.74/5.91 (Or % 5.74/5.91 (Or % 5.74/5.91 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3)))) % 5.74/5.91 False % 5.74/5.91 Clause #88 (by clausification #[86]): Eq % 5.74/5.91 (Or % 5.74/5.91 (Or % 5.74/5.91 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 5.74/5.91 False % 5.74/5.91 Clause #89 (by clausification #[87]): Eq % 5.74/5.91 (Or % 5.74/5.91 (Or % 5.74/5.91 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 5.74/5.91 True % 5.74/5.91 Clause #90 (by clausification #[89]): Or % 5.74/5.91 (Eq % 5.74/5.91 (Or % 5.74/5.91 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 5.74/5.91 True) % 5.74/5.91 (Eq (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3)) True) % 5.74/5.91 Clause #91 (by clausification #[90]): Or (Eq (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3)) True) % 5.74/5.91 (Or % 5.74/5.91 (Eq % 5.74/5.91 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.74/5.91 True) % 5.74/5.91 (Eq (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2)) True)) % 5.74/5.91 Clause #92 (by clausification #[91]): Or % 5.74/5.91 (Eq % 5.74/5.91 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.74/5.91 True) % 5.74/5.91 (Or (Eq (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2)) True) % 5.74/5.91 (Eq (Eq (op e3 e3) e3) True)) % 5.74/5.91 Clause #93 (by clausification #[91]): Or % 5.74/5.91 (Eq % 5.74/5.91 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.74/5.91 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.76/5.95 True) % 5.76/5.95 (Or (Eq (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2)) True) % 5.76/5.95 (Eq (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) True)) % 5.76/5.95 Clause #94 (by clausification #[92]): Or (Eq (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2)) True) % 5.76/5.95 (Or (Eq (Eq (op e3 e3) e3) True) % 5.76/5.95 (Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 5.76/5.95 (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True))) % 5.76/5.95 Clause #95 (by clausification #[94]): Or (Eq (Eq (op e3 e3) e3) True) % 5.76/5.95 (Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 5.76/5.95 (Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 5.76/5.95 (Eq (Eq (op e3 e3) e2) True))) % 5.76/5.95 Clause #96 (by clausification #[94]): Or (Eq (Eq (op e3 e3) e3) True) % 5.76/5.95 (Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 5.76/5.95 (Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 5.76/5.95 (Eq (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) True))) % 5.76/5.95 Clause #97 (by clausification #[95]): Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 5.76/5.95 (Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 5.76/5.95 (Or (Eq (Eq (op e3 e3) e2) True) (Eq (op e3 e3) e3))) % 5.76/5.95 Clause #98 (by clausification #[97]): Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 5.76/5.95 (Or (Eq (Eq (op e3 e3) e2) True) (Or (Eq (op e3 e3) e3) (Eq (Eq (op e3 e3) e0) True))) % 5.76/5.95 Clause #99 (by clausification #[97]): Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 5.76/5.95 (Or (Eq (Eq (op e3 e3) e2) True) % 5.76/5.95 (Or (Eq (op e3 e3) e3) (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True))) % 5.76/5.95 Clause #100 (by clausification #[98]): Or (Eq (Eq (op e3 e3) e2) True) % 5.76/5.95 (Or (Eq (op e3 e3) e3) % 5.76/5.95 (Or (Eq (Eq (op e3 e3) e0) True) (Eq (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) True))) % 5.76/5.95 Clause #101 (by clausification #[100]): Or (Eq (op e3 e3) e3) % 5.76/5.95 (Or (Eq (Eq (op e3 e3) e0) True) % 5.76/5.95 (Or (Eq (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) True) (Eq (op e3 e3) e2))) % 5.76/5.95 Clause #102 (by clausification #[101]): Or (Eq (op e3 e3) e3) % 5.76/5.95 (Or (Eq (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) True) % 5.76/5.95 (Or (Eq (op e3 e3) e2) (Eq (op e3 e3) e0))) % 5.76/5.95 Clause #104 (by clausification #[102]): Or (Eq (op e3 e3) e3) % 5.76/5.95 (Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e0) (Eq (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) True))) % 5.76/5.95 Clause #110 (by clausification #[104]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e0) (Eq (Eq (op e0 e0) e1) True))) % 5.76/5.95 Clause #114 (by clausification #[110]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e0) (Eq (op e0 e0) e1))) % 5.76/5.95 Clause #115 (by forward demodulation #[114, 84]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e0) (Eq e0 e1))) % 5.76/5.95 Clause #116 (by forward contextual literal cutting #[115, 35]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Eq (op e3 e3) e0)) % 5.76/5.95 Clause #148 (by clausification #[99]): Or (Eq (Eq (op e3 e3) e2) True) % 5.76/5.95 (Or (Eq (op e3 e3) e3) % 5.76/5.95 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) % 5.76/5.95 (Eq (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) True))) % 5.76/5.95 Clause #155 (by clausification #[88]): Eq % 5.76/5.95 (Or % 5.76/5.95 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.76/5.95 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.76/5.95 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 5.76/5.95 False % 5.76/5.98 Clause #177 (by clausification #[93]): Or (Eq (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2)) True) % 5.76/5.98 (Or (Eq (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) True) % 5.76/5.98 (Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 5.76/5.98 (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True))) % 5.76/5.98 Clause #178 (by clausification #[177]): Or (Eq (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) True) % 5.76/5.98 (Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 5.76/5.98 (Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 5.76/5.98 (Eq (Eq (op e3 e3) e2) True))) % 5.76/5.98 Clause #181 (by clausification #[178]): Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 5.76/5.98 (Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 5.76/5.98 (Or (Eq (Eq (op e3 e3) e2) True) (Eq (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) True))) % 5.76/5.98 Clause #200 (by clausification #[96]): Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 5.76/5.98 (Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 5.76/5.98 (Or (Eq (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) True) (Eq (op e3 e3) e3))) % 5.76/5.98 Clause #201 (by clausification #[200]): Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 5.76/5.98 (Or (Eq (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) True) % 5.76/5.98 (Or (Eq (op e3 e3) e3) (Eq (Eq (op e3 e3) e0) True))) % 5.76/5.98 Clause #203 (by clausification #[201]): Or (Eq (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) True) % 5.76/5.98 (Or (Eq (op e3 e3) e3) (Or (Eq (Eq (op e3 e3) e0) True) (Eq (Eq (op e3 e3) e1) True))) % 5.76/5.98 Clause #206 (by clausification #[203]): Or (Eq (op e3 e3) e3) % 5.76/5.98 (Or (Eq (Eq (op e3 e3) e0) True) % 5.76/5.98 (Or (Eq (Eq (op e3 e3) e1) True) (Eq (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) True))) % 5.76/5.98 Clause #268 (by clausification #[148]): Or (Eq (op e3 e3) e3) % 5.76/5.98 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) % 5.76/5.98 (Or (Eq (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) True) (Eq (op e3 e3) e2))) % 5.76/5.98 Clause #269 (by clausification #[268]): Or (Eq (op e3 e3) e3) % 5.76/5.98 (Or (Eq (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) True) % 5.76/5.98 (Or (Eq (op e3 e3) e2) (Eq (Eq (op e2 e2) e0) True))) % 5.76/5.98 Clause #270 (by clausification #[268]): Or (Eq (op e3 e3) e3) % 5.76/5.98 (Or (Eq (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) True) % 5.76/5.98 (Or (Eq (op e3 e3) e2) (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) True))) % 5.76/5.98 Clause #272 (by clausification #[269]): Or (Eq (op e3 e3) e3) % 5.76/5.98 (Or (Eq (op e3 e3) e2) (Or (Eq (Eq (op e2 e2) e0) True) (Eq (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) True))) % 5.76/5.98 Clause #283 (by clausification #[155]): Eq % 5.76/5.98 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 5.76/5.98 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 5.76/5.98 False % 5.76/5.98 Clause #293 (by clausification #[272]): Or (Eq (op e3 e3) e3) % 5.76/5.98 (Or (Eq (op e3 e3) e2) (Or (Eq (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) True) (Eq (op e2 e2) e0))) % 5.76/5.98 Clause #295 (by clausification #[293]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e2) e0) (Eq (Eq (op e0 e0) e1) True))) % 5.76/5.98 Clause #299 (by clausification #[295]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e2) e0) (Eq (op e0 e0) e1))) % 5.76/5.98 Clause #300 (by forward demodulation #[299, 84]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e2) e0) (Eq e0 e1))) % 5.76/5.98 Clause #301 (by forward contextual literal cutting #[300, 35]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Eq (op e2 e2) e0)) % 5.76/5.98 Clause #324 (by clausification #[181]): Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 5.76/6.01 (Or (Eq (Eq (op e3 e3) e2) True) % 5.76/6.01 (Or (Eq (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) True) (Eq (Eq (op e3 e3) e0) True))) % 5.76/6.01 Clause #326 (by clausification #[324]): Or (Eq (Eq (op e3 e3) e2) True) % 5.76/6.01 (Or (Eq (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) True) % 5.76/6.01 (Or (Eq (Eq (op e3 e3) e0) True) (Eq (Eq (op e3 e3) e1) True))) % 5.76/6.01 Clause #328 (by clausification #[326]): Or (Eq (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) True) % 5.76/6.01 (Or (Eq (Eq (op e3 e3) e0) True) (Or (Eq (Eq (op e3 e3) e1) True) (Eq (op e3 e3) e2))) % 5.76/6.01 Clause #330 (by clausification #[328]): Or (Eq (Eq (op e3 e3) e0) True) (Or (Eq (Eq (op e3 e3) e1) True) (Or (Eq (op e3 e3) e2) (Eq (Eq (op e0 e0) e3) True))) % 5.76/6.01 Clause #341 (by clausification #[330]): Or (Eq (Eq (op e3 e3) e1) True) (Or (Eq (op e3 e3) e2) (Or (Eq (Eq (op e0 e0) e3) True) (Eq (op e3 e3) e0))) % 5.76/6.01 Clause #342 (by clausification #[341]): Or (Eq (op e3 e3) e2) (Or (Eq (Eq (op e0 e0) e3) True) (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1))) % 5.76/6.01 Clause #343 (by clausification #[342]): Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Eq (op e0 e0) e3))) % 5.76/6.01 Clause #344 (by forward demodulation #[343, 84]): Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Eq e0 e3))) % 5.76/6.01 Clause #345 (by forward contextual literal cutting #[344, 19]): Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1)) % 5.76/6.01 Clause #410 (by clausification #[206]): Or (Eq (op e3 e3) e3) % 5.76/6.01 (Or (Eq (Eq (op e3 e3) e1) True) (Or (Eq (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) True) (Eq (op e3 e3) e0))) % 5.76/6.01 Clause #411 (by clausification #[410]): Or (Eq (op e3 e3) e3) % 5.76/6.01 (Or (Eq (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) True) (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1))) % 5.76/6.01 Clause #413 (by clausification #[411]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Eq (Eq (op e0 e0) e2) True))) % 5.76/6.01 Clause #463 (by clausification #[413]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Eq (op e0 e0) e2))) % 5.76/6.01 Clause #464 (by forward demodulation #[463, 84]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Eq e0 e2))) % 5.76/6.01 Clause #465 (by forward contextual literal cutting #[464, 34]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1)) % 5.76/6.01 Clause #468 (by superposition #[465, 345]): Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Or (Eq e3 e2) (Or (Eq e3 e0) (Eq e3 e1)))) % 5.76/6.01 Clause #475 (by forward contextual literal cutting #[468, 10]): Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Or (Eq e3 e0) (Eq e3 e1))) % 5.76/6.01 Clause #476 (by forward contextual literal cutting #[475, 19]): Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Eq e3 e1)) % 5.76/6.01 Clause #477 (by forward contextual literal cutting #[476, 13]): Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1) % 5.76/6.01 Clause #478 (by superposition #[477, 116]): Or (Eq (op e3 e3) e0) (Or (Eq e1 e3) (Or (Eq e1 e2) (Eq e1 e0))) % 5.76/6.01 Clause #502 (by forward contextual literal cutting #[478, 13]): Or (Eq (op e3 e3) e0) (Or (Eq e1 e2) (Eq e1 e0)) % 5.76/6.01 Clause #503 (by forward contextual literal cutting #[502, 16]): Or (Eq (op e3 e3) e0) (Eq e1 e0) % 5.76/6.01 Clause #504 (by forward contextual literal cutting #[503, 35]): Eq (op e3 e3) e0 % 5.76/6.01 Clause #516 (by backward demodulation #[504, 301]): Or (Eq e0 e3) (Or (Eq (op e3 e3) e2) (Eq (op e2 e2) e0)) % 5.76/6.01 Clause #530 (by forward demodulation #[516, 504]): Or (Eq e0 e3) (Or (Eq e0 e2) (Eq (op e2 e2) e0)) % 5.76/6.01 Clause #531 (by forward contextual literal cutting #[530, 19]): Or (Eq e0 e2) (Eq (op e2 e2) e0) % 5.76/6.01 Clause #532 (by forward contextual literal cutting #[531, 34]): Eq (op e2 e2) e0 % 5.76/6.01 Clause #533 (by clausification #[270]): Or (Eq (op e3 e3) e3) % 5.76/6.01 (Or (Eq (op e3 e3) e2) (Or (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) True) (Eq (Eq (op e2 e2) e1) True))) % 5.76/6.01 Clause #535 (by clausification #[533]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (Eq (op e2 e2) e1) True) (Eq (Eq (op e1 e1) e0) True))) % 5.76/6.01 Clause #537 (by clausification #[535]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (Eq (op e1 e1) e0) True) (Eq (op e2 e2) e1))) % 5.76/6.01 Clause #538 (by clausification #[537]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e2) e1) (Eq (op e1 e1) e0))) % 5.86/6.02 Clause #539 (by forward demodulation #[538, 504]): Or (Eq e0 e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e2) e1) (Eq (op e1 e1) e0))) % 5.86/6.02 Clause #540 (by forward demodulation #[539, 504]): Or (Eq e0 e3) (Or (Eq e0 e2) (Or (Eq (op e2 e2) e1) (Eq (op e1 e1) e0))) % 5.86/6.02 Clause #541 (by forward contextual literal cutting #[540, 19]): Or (Eq e0 e2) (Or (Eq (op e2 e2) e1) (Eq (op e1 e1) e0)) % 5.86/6.02 Clause #542 (by forward contextual literal cutting #[541, 34]): Or (Eq (op e2 e2) e1) (Eq (op e1 e1) e0) % 5.86/6.02 Clause #543 (by superposition #[542, 532]): Or (Eq (op e1 e1) e0) (Eq e1 e0) % 5.86/6.02 Clause #544 (by forward contextual literal cutting #[543, 35]): Eq (op e1 e1) e0 % 5.86/6.02 Clause #550 (by clausification #[283]): Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) False % 5.86/6.02 Clause #743 (by clausification #[550]): Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) False) (Eq (Eq (op e3 e3) e0) False) % 5.86/6.02 Clause #744 (by clausification #[743]): Or (Eq (Eq (op e3 e3) e0) False) % 5.86/6.02 (Or (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) False) (Eq (Eq (op e2 e2) e0) False)) % 5.86/6.02 Clause #745 (by clausification #[744]): Or (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) False) (Or (Eq (Eq (op e2 e2) e0) False) (Ne (op e3 e3) e0)) % 5.86/6.02 Clause #746 (by clausification #[745]): Or (Eq (Eq (op e2 e2) e0) False) % 5.86/6.02 (Or (Ne (op e3 e3) e0) (Or (Eq (Eq (op e0 e0) e0) False) (Eq (Eq (op e1 e1) e0) False))) % 5.86/6.02 Clause #747 (by clausification #[746]): Or (Ne (op e3 e3) e0) (Or (Eq (Eq (op e0 e0) e0) False) (Or (Eq (Eq (op e1 e1) e0) False) (Ne (op e2 e2) e0))) % 5.86/6.02 Clause #748 (by clausification #[747]): Or (Ne (op e3 e3) e0) (Or (Eq (Eq (op e1 e1) e0) False) (Or (Ne (op e2 e2) e0) (Ne (op e0 e0) e0))) % 5.86/6.02 Clause #749 (by clausification #[748]): Or (Ne (op e3 e3) e0) (Or (Ne (op e2 e2) e0) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0))) % 5.86/6.02 Clause #750 (by forward demodulation #[749, 504]): Or (Ne e0 e0) (Or (Ne (op e2 e2) e0) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0))) % 5.86/6.02 Clause #751 (by eliminate resolved literals #[750]): Or (Ne (op e2 e2) e0) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0)) % 5.86/6.02 Clause #752 (by forward demodulation #[751, 532]): Or (Ne e0 e0) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0)) % 5.86/6.02 Clause #753 (by eliminate resolved literals #[752]): Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0) % 5.86/6.02 Clause #754 (by forward demodulation #[753, 84]): Or (Ne e0 e0) (Ne (op e1 e1) e0) % 5.86/6.02 Clause #755 (by eliminate resolved literals #[754]): Ne (op e1 e1) e0 % 5.86/6.02 Clause #756 (by forward demodulation #[755, 544]): Ne e0 e0 % 5.86/6.02 Clause #757 (by eliminate resolved literals #[756]): False % 5.86/6.02 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------