%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ALG014+1 : TPTP v9.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.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:54 PM UTC 2025 % Result : Theorem 11.58s 11.76s % Output : Proof 11.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.09 % Problem : ALG014+1 : TPTP v9.2.0. Released v2.7.0. % 0.04/0.10 % Command : duper %s % 0.09/0.29 % Computer : n014.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Fri Oct 3 09:50:53 EDT 2025 % 0.09/0.30 % CPUTime : % 11.58/11.76 SZS status Theorem for theBenchmark.p % 11.58/11.76 SZS output start Proof for theBenchmark.p % 11.58/11.76 Clause #2 (by assumption #[]): Eq % 11.58/11.76 (And % 11.58/11.76 (And % 11.58/11.76 (And % 11.58/11.76 (And % 11.58/11.76 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 11.58/11.76 (Eq (op unit e2) e2)) % 11.58/11.76 (Eq (op e2 unit) e2)) % 11.58/11.76 (Eq (op unit e3) e3)) % 11.58/11.76 (Eq (op e3 unit) e3)) % 11.58/11.76 (Or (Or (Or (Eq unit e0) (Eq unit e1)) (Eq unit e2)) (Eq unit e3))) % 11.58/11.76 True % 11.58/11.76 Clause #4 (by assumption #[]): Eq (Eq unit e0) True % 11.58/11.76 Clause #10 (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 % 11.58/11.76 Clause #11 (by assumption #[]): Eq % 11.58/11.76 (Not % 11.58/11.76 (Or % 11.58/11.76 (Or % 11.58/11.76 (Or % 11.58/11.76 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.58/11.76 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.58/11.76 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 11.58/11.76 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 11.58/11.76 (Not % 11.58/11.76 (Or % 11.58/11.76 (Or % 11.58/11.76 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.58/11.76 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.58/11.76 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 11.58/11.76 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3)))))) % 11.58/11.76 True % 11.58/11.76 Clause #12 (by clausification #[4]): Eq unit e0 % 11.58/11.76 Clause #38 (by clausification #[10]): Eq (Ne e2 e3) True % 11.58/11.76 Clause #39 (by clausification #[10]): Eq (And (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e1 e2)) (Ne e1 e3)) True % 11.58/11.76 Clause #40 (by clausification #[38]): Ne e2 e3 % 11.58/11.76 Clause #45 (by clausification #[39]): Eq (Ne e1 e3) True % 11.58/11.76 Clause #46 (by clausification #[39]): Eq (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e1 e2)) True % 11.58/11.76 Clause #47 (by clausification #[45]): Ne e1 e3 % 11.58/11.76 Clause #48 (by clausification #[46]): Eq (Ne e1 e2) True % 11.58/11.76 Clause #49 (by clausification #[46]): Eq (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) True % 11.58/11.76 Clause #50 (by clausification #[48]): Ne e1 e2 % 11.58/11.76 Clause #51 (by clausification #[49]): Eq (Ne e0 e3) True % 11.58/11.76 Clause #52 (by clausification #[49]): Eq (And (Ne e0 e1) (Ne e0 e2)) True % 11.58/11.76 Clause #53 (by clausification #[51]): Ne e0 e3 % 11.58/11.76 Clause #54 (by clausification #[52]): Eq (Ne e0 e2) True % 11.58/11.76 Clause #55 (by clausification #[52]): Eq (Ne e0 e1) True % 11.58/11.76 Clause #56 (by clausification #[54]): Ne e0 e2 % 11.58/11.76 Clause #58 (by clausification #[2]): Eq % 11.58/11.76 (And % 11.58/11.76 (And % 11.58/11.76 (And % 11.58/11.76 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 11.58/11.76 (Eq (op unit e2) e2)) % 11.58/11.76 (Eq (op e2 unit) e2)) % 11.58/11.76 (Eq (op unit e3) e3)) % 11.58/11.76 (Eq (op e3 unit) e3)) % 11.58/11.76 True % 11.58/11.76 Clause #68 (by clausification #[55]): Ne e0 e1 % 11.58/11.76 Clause #116 (by clausification #[58]): Eq % 11.58/11.76 (And % 11.58/11.76 (And % 11.58/11.76 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 11.58/11.76 (Eq (op unit e2) e2)) % 11.58/11.76 (Eq (op e2 unit) e2)) % 11.58/11.76 (Eq (op unit e3) e3)) % 11.58/11.76 True % 11.58/11.76 Clause #120 (by clausification #[116]): Eq % 11.58/11.76 (And % 11.58/11.76 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 11.58/11.76 (Eq (op unit e2) e2)) % 11.58/11.76 (Eq (op e2 unit) e2)) % 11.58/11.76 True % 11.58/11.76 Clause #124 (by clausification #[120]): Eq % 11.58/11.76 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 11.58/11.76 (Eq (op unit e2) e2)) % 11.58/11.76 True % 11.58/11.76 Clause #128 (by clausification #[124]): 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 % 11.58/11.76 Clause #131 (by clausification #[11]): Eq % 11.58/11.76 (Or % 11.58/11.76 (Or % 11.58/11.76 (Or % 11.58/11.76 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.58/11.76 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 11.58/11.78 (Not % 11.58/11.78 (Or % 11.58/11.78 (Or % 11.58/11.78 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))))) % 11.58/11.78 False % 11.58/11.78 Clause #132 (by clausification #[131]): Eq % 11.58/11.78 (Not % 11.58/11.78 (Or % 11.58/11.78 (Or % 11.58/11.78 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3)))) % 11.58/11.78 False % 11.58/11.78 Clause #133 (by clausification #[131]): Eq % 11.58/11.78 (Or % 11.58/11.78 (Or % 11.58/11.78 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 11.58/11.78 False % 11.58/11.78 Clause #134 (by clausification #[132]): Eq % 11.58/11.78 (Or % 11.58/11.78 (Or % 11.58/11.78 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 11.58/11.78 True % 11.58/11.78 Clause #135 (by clausification #[134]): Or % 11.58/11.78 (Eq % 11.58/11.78 (Or % 11.58/11.78 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 11.58/11.78 True) % 11.58/11.78 (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) % 11.58/11.78 Clause #136 (by clausification #[135]): 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) % 11.58/11.78 (Or % 11.58/11.78 (Eq % 11.58/11.78 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.58/11.78 True) % 11.58/11.78 (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)) % 11.58/11.78 Clause #137 (by clausification #[136]): Or % 11.58/11.78 (Eq % 11.58/11.78 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.58/11.78 True) % 11.58/11.78 (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) % 11.58/11.78 (Eq (Eq (op e3 e3) e3) True)) % 11.58/11.78 Clause #138 (by clausification #[136]): Or % 11.58/11.78 (Eq % 11.58/11.78 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.58/11.78 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.58/11.78 True) % 11.58/11.78 (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) % 11.58/11.78 (Eq (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) True)) % 11.58/11.78 Clause #139 (by clausification #[137]): 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) % 11.58/11.78 (Or (Eq (Eq (op e3 e3) e3) True) % 11.58/11.81 (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) % 11.58/11.81 (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))) % 11.58/11.81 Clause #140 (by clausification #[139]): Or (Eq (Eq (op e3 e3) e3) True) % 11.58/11.81 (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) % 11.58/11.81 (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) % 11.58/11.81 (Eq (Eq (op e3 e3) e2) True))) % 11.58/11.81 Clause #141 (by clausification #[139]): Or (Eq (Eq (op e3 e3) e3) True) % 11.58/11.81 (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) % 11.58/11.81 (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) % 11.58/11.81 (Eq (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) True))) % 11.58/11.81 Clause #142 (by clausification #[140]): 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) % 11.58/11.81 (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) % 11.58/11.81 (Or (Eq (Eq (op e3 e3) e2) True) (Eq (op e3 e3) e3))) % 11.58/11.81 Clause #143 (by clausification #[142]): 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) % 11.58/11.81 (Or (Eq (Eq (op e3 e3) e2) True) (Or (Eq (op e3 e3) e3) (Eq (Eq (op e3 e3) e0) True))) % 11.58/11.81 Clause #144 (by clausification #[142]): 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) % 11.58/11.81 (Or (Eq (Eq (op e3 e3) e2) True) % 11.58/11.81 (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))) % 11.58/11.81 Clause #145 (by clausification #[143]): Or (Eq (Eq (op e3 e3) e2) True) % 11.58/11.81 (Or (Eq (op e3 e3) e3) % 11.58/11.81 (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))) % 11.58/11.81 Clause #147 (by clausification #[128]): Eq (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) True % 11.58/11.81 Clause #151 (by clausification #[147]): Eq (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) True % 11.58/11.81 Clause #154 (by clausification #[151]): Eq (Eq (op e0 unit) e0) True % 11.58/11.81 Clause #156 (by clausification #[154]): Eq (op e0 unit) e0 % 11.58/11.81 Clause #157 (by forward demodulation #[156, 12]): Eq (op e0 e0) e0 % 11.58/11.81 Clause #159 (by clausification #[145]): Or (Eq (op e3 e3) e3) % 11.58/11.81 (Or (Eq (Eq (op e3 e3) e0) True) % 11.58/11.81 (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))) % 11.58/11.81 Clause #160 (by clausification #[159]): Or (Eq (op e3 e3) e3) % 11.58/11.81 (Or (Eq (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) True) % 11.58/11.81 (Or (Eq (op e3 e3) e2) (Eq (op e3 e3) e0))) % 11.58/11.81 Clause #162 (by clausification #[160]): Or (Eq (op e3 e3) e3) % 11.58/11.81 (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))) % 11.58/11.81 Clause #189 (by clausification #[162]): 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))) % 11.58/11.81 Clause #226 (by clausification #[189]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e0) (Eq (op e0 e0) e1))) % 11.58/11.81 Clause #227 (by forward demodulation #[226, 157]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e0) (Eq e0 e1))) % 11.58/11.81 Clause #228 (by forward contextual literal cutting #[227, 68]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Eq (op e3 e3) e0)) % 11.58/11.81 Clause #236 (by clausification #[133]): Eq % 11.58/11.81 (Or % 11.58/11.81 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.58/11.81 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.58/11.81 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 11.58/11.81 False % 11.58/11.81 Clause #247 (by clausification #[138]): 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) % 11.58/11.81 (Or (Eq (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) True) % 11.65/11.84 (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) % 11.65/11.84 (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))) % 11.65/11.84 Clause #248 (by clausification #[247]): Or (Eq (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) True) % 11.65/11.84 (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) % 11.65/11.84 (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) % 11.65/11.84 (Eq (Eq (op e3 e3) e2) True))) % 11.65/11.84 Clause #249 (by clausification #[247]): Or (Eq (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) True) % 11.65/11.84 (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) % 11.65/11.84 (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) % 11.65/11.84 (Eq (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) True))) % 11.65/11.84 Clause #251 (by clausification #[248]): 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) % 11.65/11.84 (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) % 11.65/11.84 (Or (Eq (Eq (op e3 e3) e2) True) (Eq (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) True))) % 11.65/11.84 Clause #265 (by clausification #[141]): 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) % 11.65/11.84 (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) % 11.65/11.84 (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))) % 11.65/11.84 Clause #266 (by clausification #[265]): 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) % 11.65/11.84 (Or (Eq (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) True) % 11.65/11.84 (Or (Eq (op e3 e3) e3) (Eq (Eq (op e3 e3) e0) True))) % 11.65/11.84 Clause #268 (by clausification #[266]): Or (Eq (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) True) % 11.65/11.84 (Or (Eq (op e3 e3) e3) (Or (Eq (Eq (op e3 e3) e0) True) (Eq (Eq (op e3 e3) e1) True))) % 11.65/11.84 Clause #271 (by clausification #[268]): Or (Eq (op e3 e3) e3) % 11.65/11.84 (Or (Eq (Eq (op e3 e3) e0) True) % 11.65/11.84 (Or (Eq (Eq (op e3 e3) e1) True) (Eq (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) True))) % 11.65/11.84 Clause #281 (by clausification #[144]): Or (Eq (Eq (op e3 e3) e2) True) % 11.65/11.84 (Or (Eq (op e3 e3) e3) % 11.65/11.84 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) (Eq (Eq (op e3 e3) e1) True))) % 11.65/11.84 Clause #282 (by clausification #[144]): Or (Eq (Eq (op e3 e3) e2) True) % 11.65/11.84 (Or (Eq (op e3 e3) e3) % 11.65/11.84 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) % 11.65/11.84 (Eq (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) True))) % 11.65/11.84 Clause #283 (by clausification #[281]): Or (Eq (op e3 e3) e3) % 11.65/11.84 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) % 11.65/11.84 (Or (Eq (Eq (op e3 e3) e1) True) (Eq (op e3 e3) e2))) % 11.65/11.84 Clause #285 (by clausification #[283]): Or (Eq (op e3 e3) e3) % 11.65/11.84 (Or (Eq (Eq (op e3 e3) e1) True) (Or (Eq (op e3 e3) e2) (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) True))) % 11.65/11.84 Clause #293 (by clausification #[285]): Or (Eq (op e3 e3) e3) % 11.65/11.84 (Or (Eq (op e3 e3) e2) (Or (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) True) (Eq (op e3 e3) e1))) % 11.65/11.84 Clause #294 (by clausification #[293]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e1) (Eq (Eq (op e1 e1) e0) True))) % 11.65/11.84 Clause #296 (by clausification #[294]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e1) (Eq (op e1 e1) e0))) % 11.65/11.84 Clause #393 (by clausification #[236]): Eq % 11.65/11.84 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 11.65/11.84 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 11.65/11.84 False % 11.65/11.84 Clause #405 (by clausification #[249]): 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) % 11.65/11.87 (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) % 11.65/11.87 (Or (Eq (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) True) (Eq (Eq (op e2 e2) e3) True))) % 11.65/11.87 Clause #408 (by clausification #[405]): 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) % 11.65/11.87 (Or (Eq (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) True) % 11.65/11.87 (Or (Eq (Eq (op e2 e2) e3) True) (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True))) % 11.65/11.87 Clause #432 (by clausification #[251]): 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) % 11.65/11.87 (Or (Eq (Eq (op e3 e3) e2) True) % 11.65/11.87 (Or (Eq (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) True) (Eq (Eq (op e3 e3) e0) True))) % 11.65/11.87 Clause #434 (by clausification #[432]): Or (Eq (Eq (op e3 e3) e2) True) % 11.65/11.87 (Or (Eq (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) True) % 11.65/11.87 (Or (Eq (Eq (op e3 e3) e0) True) (Eq (Eq (op e3 e3) e1) True))) % 11.65/11.87 Clause #436 (by clausification #[434]): Or (Eq (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) True) % 11.65/11.87 (Or (Eq (Eq (op e3 e3) e0) True) (Or (Eq (Eq (op e3 e3) e1) True) (Eq (op e3 e3) e2))) % 11.65/11.87 Clause #438 (by clausification #[436]): 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))) % 11.65/11.87 Clause #557 (by clausification #[271]): Or (Eq (op e3 e3) e3) % 11.65/11.87 (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))) % 11.65/11.87 Clause #558 (by clausification #[557]): Or (Eq (op e3 e3) e3) % 11.65/11.87 (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))) % 11.65/11.87 Clause #560 (by clausification #[558]): 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))) % 11.65/11.87 Clause #573 (by clausification #[560]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Eq (op e0 e0) e2))) % 11.65/11.87 Clause #574 (by forward demodulation #[573, 157]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Eq e0 e2))) % 11.65/11.87 Clause #575 (by forward contextual literal cutting #[574, 56]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1)) % 11.65/11.87 Clause #630 (by clausification #[282]): Or (Eq (op e3 e3) e3) % 11.65/11.87 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) % 11.65/11.87 (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))) % 11.65/11.87 Clause #631 (by clausification #[630]): Or (Eq (op e3 e3) e3) % 11.65/11.87 (Or (Eq (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) True) % 11.65/11.87 (Or (Eq (op e3 e3) e2) (Eq (Eq (op e2 e2) e0) True))) % 11.65/11.87 Clause #633 (by clausification #[631]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (Eq (op e2 e2) e0) True) (Eq (Eq (op e2 e2) e1) True))) % 11.65/11.87 Clause #635 (by clausification #[633]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (Eq (op e2 e2) e1) True) (Eq (op e2 e2) e0))) % 11.65/11.87 Clause #636 (by clausification #[635]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e2) e0) (Eq (op e2 e2) e1))) % 11.65/11.87 Clause #766 (by clausification #[438]): 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))) % 11.65/11.87 Clause #767 (by clausification #[766]): 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))) % 11.65/11.87 Clause #768 (by clausification #[767]): Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Eq (op e0 e0) e3))) % 11.65/11.87 Clause #769 (by forward demodulation #[768, 157]): Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Eq e0 e3))) % 11.65/11.87 Clause #770 (by forward contextual literal cutting #[769, 53]): Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1)) % 11.65/11.87 Clause #778 (by superposition #[770, 575]): Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Or (Eq e2 e3) (Or (Eq e2 e0) (Eq e2 e1)))) % 11.65/11.87 Clause #786 (by forward contextual literal cutting #[778, 40]): Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Or (Eq e2 e0) (Eq e2 e1))) % 11.70/11.89 Clause #787 (by forward contextual literal cutting #[786, 56]): Or (Eq (op e3 e3) e0) (Or (Eq (op e3 e3) e1) (Eq e2 e1)) % 11.70/11.89 Clause #788 (by forward contextual literal cutting #[787, 50]): Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1) % 11.70/11.89 Clause #793 (by superposition #[788, 228]): Or (Eq (op e3 e3) e0) (Or (Eq e1 e3) (Or (Eq e1 e2) (Eq e1 e0))) % 11.70/11.89 Clause #815 (by forward contextual literal cutting #[793, 47]): Or (Eq (op e3 e3) e0) (Or (Eq e1 e2) (Eq e1 e0)) % 11.70/11.89 Clause #816 (by forward contextual literal cutting #[815, 50]): Or (Eq (op e3 e3) e0) (Eq e1 e0) % 11.70/11.89 Clause #817 (by forward contextual literal cutting #[816, 68]): Eq (op e3 e3) e0 % 11.70/11.89 Clause #830 (by backward demodulation #[817, 296]): Or (Eq e0 e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e1) (Eq (op e1 e1) e0))) % 11.70/11.89 Clause #845 (by backward demodulation #[817, 636]): Or (Eq e0 e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e2) e0) (Eq (op e2 e2) e1))) % 11.70/11.89 Clause #876 (by clausification #[393]): 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 % 11.70/11.89 Clause #921 (by clausification #[408]): Or (Eq (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) True) % 11.70/11.89 (Or (Eq (Eq (op e2 e2) e3) True) % 11.70/11.89 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) (Eq (Eq (op e3 e3) e1) True))) % 11.70/11.89 Clause #923 (by clausification #[921]): Or (Eq (Eq (op e2 e2) e3) True) % 11.70/11.89 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) % 11.70/11.89 (Or (Eq (Eq (op e3 e3) e1) True) (Eq (Eq (op e2 e2) e2) True))) % 11.70/11.89 Clause #925 (by clausification #[923]): Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) % 11.70/11.89 (Or (Eq (Eq (op e3 e3) e1) True) (Or (Eq (Eq (op e2 e2) e2) True) (Eq (op e2 e2) e3))) % 11.70/11.89 Clause #926 (by clausification #[925]): Or (Eq (Eq (op e3 e3) e1) True) (Or (Eq (Eq (op e2 e2) e2) True) (Or (Eq (op e2 e2) e3) (Eq (Eq (op e2 e2) e0) True))) % 11.70/11.89 Clause #928 (by clausification #[926]): Or (Eq (Eq (op e2 e2) e2) True) (Or (Eq (op e2 e2) e3) (Or (Eq (Eq (op e2 e2) e0) True) (Eq (op e3 e3) e1))) % 11.70/11.89 Clause #929 (by clausification #[928]): Or (Eq (op e2 e2) e3) (Or (Eq (Eq (op e2 e2) e0) True) (Or (Eq (op e3 e3) e1) (Eq (op e2 e2) e2))) % 11.70/11.89 Clause #930 (by clausification #[929]): Or (Eq (op e2 e2) e3) (Or (Eq (op e3 e3) e1) (Or (Eq (op e2 e2) e2) (Eq (op e2 e2) e0))) % 11.70/11.89 Clause #931 (by forward demodulation #[930, 817]): Or (Eq (op e2 e2) e3) (Or (Eq e0 e1) (Or (Eq (op e2 e2) e2) (Eq (op e2 e2) e0))) % 11.70/11.89 Clause #932 (by forward contextual literal cutting #[931, 68]): Or (Eq (op e2 e2) e3) (Or (Eq (op e2 e2) e2) (Eq (op e2 e2) e0)) % 11.70/11.89 Clause #936 (by forward demodulation #[845, 817]): Or (Eq e0 e3) (Or (Eq e0 e2) (Or (Eq (op e2 e2) e0) (Eq (op e2 e2) e1))) % 11.70/11.89 Clause #937 (by forward contextual literal cutting #[936, 53]): Or (Eq e0 e2) (Or (Eq (op e2 e2) e0) (Eq (op e2 e2) e1)) % 11.70/11.89 Clause #938 (by forward contextual literal cutting #[937, 56]): Or (Eq (op e2 e2) e0) (Eq (op e2 e2) e1) % 11.70/11.89 Clause #939 (by superposition #[938, 932]): Or (Eq (op e2 e2) e0) (Or (Eq e1 e3) (Or (Eq e1 e2) (Eq e1 e0))) % 11.70/11.89 Clause #950 (by forward contextual literal cutting #[939, 47]): Or (Eq (op e2 e2) e0) (Or (Eq e1 e2) (Eq e1 e0)) % 11.70/11.89 Clause #951 (by forward contextual literal cutting #[950, 50]): Or (Eq (op e2 e2) e0) (Eq e1 e0) % 11.70/11.89 Clause #952 (by forward contextual literal cutting #[951, 68]): Eq (op e2 e2) e0 % 11.70/11.89 Clause #971 (by forward demodulation #[830, 817]): Or (Eq e0 e3) (Or (Eq (op e3 e3) e2) (Or (Eq e0 e1) (Eq (op e1 e1) e0))) % 11.70/11.89 Clause #972 (by forward contextual literal cutting #[971, 53]): Or (Eq (op e3 e3) e2) (Or (Eq e0 e1) (Eq (op e1 e1) e0)) % 11.70/11.89 Clause #973 (by forward contextual literal cutting #[972, 68]): Or (Eq (op e3 e3) e2) (Eq (op e1 e1) e0) % 11.70/11.89 Clause #974 (by superposition #[973, 817]): Or (Eq (op e1 e1) e0) (Eq e2 e0) % 11.70/11.89 Clause #975 (by forward contextual literal cutting #[974, 56]): Eq (op e1 e1) e0 % 11.70/11.89 Clause #1164 (by clausification #[876]): 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) % 11.70/11.89 Clause #1165 (by clausification #[1164]): Or (Eq (Eq (op e3 e3) e0) False) % 11.70/11.90 (Or (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) False) (Eq (Eq (op e2 e2) e0) False)) % 11.70/11.90 Clause #1166 (by clausification #[1165]): 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)) % 11.70/11.90 Clause #1167 (by clausification #[1166]): Or (Eq (Eq (op e2 e2) e0) False) % 11.70/11.90 (Or (Ne (op e3 e3) e0) (Or (Eq (Eq (op e0 e0) e0) False) (Eq (Eq (op e1 e1) e0) False))) % 11.70/11.90 Clause #1168 (by clausification #[1167]): 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))) % 11.70/11.90 Clause #1169 (by clausification #[1168]): 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))) % 11.70/11.90 Clause #1170 (by clausification #[1169]): Or (Ne (op e3 e3) e0) (Or (Ne (op e2 e2) e0) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0))) % 11.70/11.90 Clause #1171 (by forward demodulation #[1170, 817]): Or (Ne e0 e0) (Or (Ne (op e2 e2) e0) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0))) % 11.70/11.90 Clause #1172 (by eliminate resolved literals #[1171]): Or (Ne (op e2 e2) e0) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0)) % 11.70/11.90 Clause #1173 (by forward demodulation #[1172, 952]): Or (Ne e0 e0) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0)) % 11.70/11.90 Clause #1174 (by eliminate resolved literals #[1173]): Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0) % 11.70/11.90 Clause #1175 (by forward demodulation #[1174, 157]): Or (Ne e0 e0) (Ne (op e1 e1) e0) % 11.70/11.90 Clause #1176 (by eliminate resolved literals #[1175]): Ne (op e1 e1) e0 % 11.70/11.90 Clause #1177 (by forward demodulation #[1176, 975]): Ne e0 e0 % 11.70/11.90 Clause #1178 (by eliminate resolved literals #[1177]): False % 11.70/11.90 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------