%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO178^5 : TPTP v9.2.0. Released v4.0.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 08:08:41 PM UTC 2025 % Result : Theorem 3.78s 3.94s % Output : Proof 3.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYO178^5 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n010.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 12:55:23 EDT 2025 % 0.13/0.34 % CPUTime : % 3.78/3.94 SZS status Theorem for theBenchmark.p % 3.78/3.94 SZS output start Proof for theBenchmark.p % 3.78/3.94 Clause #0 (by assumption #[]): Eq % 3.78/3.94 (Not % 3.78/3.94 (Not % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) % 3.78/3.94 (Or (Or (Not cG) cR) cM)) % 3.78/3.94 (Or (Or cG cP) cR)) % 3.78/3.94 (Or (Or (Not cK) (Not cB)) cC)) % 3.78/3.94 (Or (Or (Not cL) (Not cM)) cC)) % 3.78/3.94 (Or (Or cG cR) cK)) % 3.78/3.94 (Or (Or (Not cR) (Not cE)) (Not cC))) % 3.78/3.94 (Or (Or (Or (Not cR) cN) cF) cP)) % 3.78/3.94 (Or (Or (Or (Not cK) (Not cL)) (Not cE)) (Not cM))) % 3.78/3.94 (Or (Or (Or (Not cG) cK) cM) (Not cB))) % 3.78/3.94 (Or (Or (Or (Not cN) cP) cF) cC)) % 3.78/3.94 (Or (Or (Or (Not cG) (Not cB)) cR) (Not cC))) % 3.78/3.94 (Or (Or (Or cK (Not cN)) (Not cM)) cF)) % 3.78/3.94 (Or (Or (Or (Not cR) cK) cM) cG)) % 3.78/3.94 (Or (Or (Or (Or (Not cE) cK) (Not cG)) cN) (Not cM))))) % 3.78/3.94 True % 3.78/3.94 Clause #1 (by clausification #[0]): Eq % 3.78/3.94 (Not % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) % 3.78/3.94 (Or (Or (Not cG) cR) cM)) % 3.78/3.94 (Or (Or cG cP) cR)) % 3.78/3.94 (Or (Or (Not cK) (Not cB)) cC)) % 3.78/3.94 (Or (Or (Not cL) (Not cM)) cC)) % 3.78/3.94 (Or (Or cG cR) cK)) % 3.78/3.94 (Or (Or (Not cR) (Not cE)) (Not cC))) % 3.78/3.94 (Or (Or (Or (Not cR) cN) cF) cP)) % 3.78/3.94 (Or (Or (Or (Not cK) (Not cL)) (Not cE)) (Not cM))) % 3.78/3.94 (Or (Or (Or (Not cG) cK) cM) (Not cB))) % 3.78/3.94 (Or (Or (Or (Not cN) cP) cF) cC)) % 3.78/3.94 (Or (Or (Or (Not cG) (Not cB)) cR) (Not cC))) % 3.78/3.94 (Or (Or (Or cK (Not cN)) (Not cM)) cF)) % 3.78/3.94 (Or (Or (Or (Not cR) cK) cM) cG)) % 3.78/3.94 (Or (Or (Or (Or (Not cE) cK) (Not cG)) cN) (Not cM)))) % 3.78/3.94 False % 3.78/3.94 Clause #2 (by clausification #[1]): Eq % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) % 3.78/3.94 (Or (Or (Not cG) cR) cM)) % 3.78/3.94 (Or (Or cG cP) cR)) % 3.78/3.94 (Or (Or (Not cK) (Not cB)) cC)) % 3.78/3.94 (Or (Or (Not cL) (Not cM)) cC)) % 3.78/3.94 (Or (Or cG cR) cK)) % 3.78/3.94 (Or (Or (Not cR) (Not cE)) (Not cC))) % 3.78/3.94 (Or (Or (Or (Not cR) cN) cF) cP)) % 3.78/3.94 (Or (Or (Or (Not cK) (Not cL)) (Not cE)) (Not cM))) % 3.78/3.94 (Or (Or (Or (Not cG) cK) cM) (Not cB))) % 3.78/3.94 (Or (Or (Or (Not cN) cP) cF) cC)) % 3.78/3.94 (Or (Or (Or (Not cG) (Not cB)) cR) (Not cC))) % 3.78/3.94 (Or (Or (Or cK (Not cN)) (Not cM)) cF)) % 3.78/3.94 (Or (Or (Or (Not cR) cK) cM) cG)) % 3.78/3.94 (Or (Or (Or (Or (Not cE) cK) (Not cG)) cN) (Not cM))) % 3.78/3.94 True % 3.78/3.94 Clause #3 (by clausification #[2]): Eq (Or (Or (Or (Or (Not cE) cK) (Not cG)) cN) (Not cM)) True % 3.78/3.94 Clause #4 (by clausification #[2]): Eq % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And % 3.78/3.94 (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) % 3.78/3.96 (Or (Or (Not cG) cR) cM)) % 3.78/3.96 (Or (Or cG cP) cR)) % 3.78/3.96 (Or (Or (Not cK) (Not cB)) cC)) % 3.78/3.96 (Or (Or (Not cL) (Not cM)) cC)) % 3.78/3.96 (Or (Or cG cR) cK)) % 3.78/3.96 (Or (Or (Not cR) (Not cE)) (Not cC))) % 3.78/3.96 (Or (Or (Or (Not cR) cN) cF) cP)) % 3.78/3.96 (Or (Or (Or (Not cK) (Not cL)) (Not cE)) (Not cM))) % 3.78/3.96 (Or (Or (Or (Not cG) cK) cM) (Not cB))) % 3.78/3.96 (Or (Or (Or (Not cN) cP) cF) cC)) % 3.78/3.96 (Or (Or (Or (Not cG) (Not cB)) cR) (Not cC))) % 3.78/3.96 (Or (Or (Or cK (Not cN)) (Not cM)) cF)) % 3.78/3.96 (Or (Or (Or (Not cR) cK) cM) cG)) % 3.78/3.96 True % 3.78/3.96 Clause #5 (by clausification #[3]): Or (Eq (Or (Or (Or (Not cE) cK) (Not cG)) cN) True) (Eq (Not cM) True) % 3.78/3.96 Clause #6 (by clausification #[5]): Or (Eq (Not cM) True) (Or (Eq (Or (Or (Not cE) cK) (Not cG)) True) (Eq cN True)) % 3.78/3.96 Clause #7 (by clausification #[6]): Or (Eq (Or (Or (Not cE) cK) (Not cG)) True) (Or (Eq cN True) (Eq cM False)) % 3.78/3.96 Clause #8 (by clausification #[7]): Or (Eq cN True) (Or (Eq cM False) (Or (Eq (Or (Not cE) cK) True) (Eq (Not cG) True))) % 3.78/3.96 Clause #9 (by clausification #[8]): Or (Eq cN True) (Or (Eq cM False) (Or (Eq (Not cG) True) (Or (Eq (Not cE) True) (Eq cK True)))) % 3.78/3.96 Clause #10 (by clausification #[9]): Or (Eq cN True) (Or (Eq cM False) (Or (Eq (Not cE) True) (Or (Eq cK True) (Eq cG False)))) % 3.78/3.96 Clause #11 (by clausification #[10]): Or (Eq cN True) (Or (Eq cM False) (Or (Eq cK True) (Or (Eq cG False) (Eq cE False)))) % 3.78/3.96 Clause #12 (by clausification #[4]): Eq (Or (Or (Or (Not cR) cK) cM) cG) True % 3.78/3.96 Clause #13 (by clausification #[4]): Eq % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) % 3.78/3.96 (Or (Or (Not cG) cR) cM)) % 3.78/3.96 (Or (Or cG cP) cR)) % 3.78/3.96 (Or (Or (Not cK) (Not cB)) cC)) % 3.78/3.96 (Or (Or (Not cL) (Not cM)) cC)) % 3.78/3.96 (Or (Or cG cR) cK)) % 3.78/3.96 (Or (Or (Not cR) (Not cE)) (Not cC))) % 3.78/3.96 (Or (Or (Or (Not cR) cN) cF) cP)) % 3.78/3.96 (Or (Or (Or (Not cK) (Not cL)) (Not cE)) (Not cM))) % 3.78/3.96 (Or (Or (Or (Not cG) cK) cM) (Not cB))) % 3.78/3.96 (Or (Or (Or (Not cN) cP) cF) cC)) % 3.78/3.96 (Or (Or (Or (Not cG) (Not cB)) cR) (Not cC))) % 3.78/3.96 (Or (Or (Or cK (Not cN)) (Not cM)) cF)) % 3.78/3.96 True % 3.78/3.96 Clause #14 (by clausification #[12]): Or (Eq (Or (Or (Not cR) cK) cM) True) (Eq cG True) % 3.78/3.96 Clause #15 (by clausification #[14]): Or (Eq cG True) (Or (Eq (Or (Not cR) cK) True) (Eq cM True)) % 3.78/3.96 Clause #16 (by clausification #[15]): Or (Eq cG True) (Or (Eq cM True) (Or (Eq (Not cR) True) (Eq cK True))) % 3.78/3.96 Clause #17 (by clausification #[16]): Or (Eq cG True) (Or (Eq cM True) (Or (Eq cK True) (Eq cR False))) % 3.78/3.96 Clause #18 (by clausification #[13]): Eq (Or (Or (Or cK (Not cN)) (Not cM)) cF) True % 3.78/3.96 Clause #19 (by clausification #[13]): Eq % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And % 3.78/3.96 (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) % 3.78/3.96 (Or (Or (Not cG) cR) cM)) % 3.78/3.96 (Or (Or cG cP) cR)) % 3.78/3.96 (Or (Or (Not cK) (Not cB)) cC)) % 3.78/3.96 (Or (Or (Not cL) (Not cM)) cC)) % 3.78/3.96 (Or (Or cG cR) cK)) % 3.78/3.96 (Or (Or (Not cR) (Not cE)) (Not cC))) % 3.78/3.96 (Or (Or (Or (Not cR) cN) cF) cP)) % 3.78/3.96 (Or (Or (Or (Not cK) (Not cL)) (Not cE)) (Not cM))) % 3.78/3.96 (Or (Or (Or (Not cG) cK) cM) (Not cB))) % 3.78/3.96 (Or (Or (Or (Not cN) cP) cF) cC)) % 3.78/3.96 (Or (Or (Or (Not cG) (Not cB)) cR) (Not cC))) % 3.78/3.96 True % 3.78/3.96 Clause #20 (by clausification #[18]): Or (Eq (Or (Or cK (Not cN)) (Not cM)) True) (Eq cF True) % 3.78/3.96 Clause #21 (by clausification #[20]): Or (Eq cF True) (Or (Eq (Or cK (Not cN)) True) (Eq (Not cM) True)) % 3.78/3.96 Clause #22 (by clausification #[21]): Or (Eq cF True) (Or (Eq (Not cM) True) (Or (Eq cK True) (Eq (Not cN) True))) % 3.78/3.99 Clause #23 (by clausification #[22]): Or (Eq cF True) (Or (Eq cK True) (Or (Eq (Not cN) True) (Eq cM False))) % 3.78/3.99 Clause #24 (by clausification #[23]): Or (Eq cF True) (Or (Eq cK True) (Or (Eq cM False) (Eq cN False))) % 3.78/3.99 Clause #25 (by clausification #[19]): Eq (Or (Or (Or (Not cG) (Not cB)) cR) (Not cC)) True % 3.78/3.99 Clause #26 (by clausification #[19]): Eq % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) % 3.78/3.99 (Or (Or (Not cG) cR) cM)) % 3.78/3.99 (Or (Or cG cP) cR)) % 3.78/3.99 (Or (Or (Not cK) (Not cB)) cC)) % 3.78/3.99 (Or (Or (Not cL) (Not cM)) cC)) % 3.78/3.99 (Or (Or cG cR) cK)) % 3.78/3.99 (Or (Or (Not cR) (Not cE)) (Not cC))) % 3.78/3.99 (Or (Or (Or (Not cR) cN) cF) cP)) % 3.78/3.99 (Or (Or (Or (Not cK) (Not cL)) (Not cE)) (Not cM))) % 3.78/3.99 (Or (Or (Or (Not cG) cK) cM) (Not cB))) % 3.78/3.99 (Or (Or (Or (Not cN) cP) cF) cC)) % 3.78/3.99 True % 3.78/3.99 Clause #27 (by clausification #[25]): Or (Eq (Or (Or (Not cG) (Not cB)) cR) True) (Eq (Not cC) True) % 3.78/3.99 Clause #28 (by clausification #[27]): Or (Eq (Not cC) True) (Or (Eq (Or (Not cG) (Not cB)) True) (Eq cR True)) % 3.78/3.99 Clause #29 (by clausification #[28]): Or (Eq (Or (Not cG) (Not cB)) True) (Or (Eq cR True) (Eq cC False)) % 3.78/3.99 Clause #30 (by clausification #[29]): Or (Eq cR True) (Or (Eq cC False) (Or (Eq (Not cG) True) (Eq (Not cB) True))) % 3.78/3.99 Clause #31 (by clausification #[30]): Or (Eq cR True) (Or (Eq cC False) (Or (Eq (Not cB) True) (Eq cG False))) % 3.78/3.99 Clause #32 (by clausification #[31]): Or (Eq cR True) (Or (Eq cC False) (Or (Eq cG False) (Eq cB False))) % 3.78/3.99 Clause #33 (by clausification #[26]): Eq (Or (Or (Or (Not cN) cP) cF) cC) True % 3.78/3.99 Clause #34 (by clausification #[26]): Eq % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) (Or (Or (Not cG) cR) cM)) % 3.78/3.99 (Or (Or cG cP) cR)) % 3.78/3.99 (Or (Or (Not cK) (Not cB)) cC)) % 3.78/3.99 (Or (Or (Not cL) (Not cM)) cC)) % 3.78/3.99 (Or (Or cG cR) cK)) % 3.78/3.99 (Or (Or (Not cR) (Not cE)) (Not cC))) % 3.78/3.99 (Or (Or (Or (Not cR) cN) cF) cP)) % 3.78/3.99 (Or (Or (Or (Not cK) (Not cL)) (Not cE)) (Not cM))) % 3.78/3.99 (Or (Or (Or (Not cG) cK) cM) (Not cB))) % 3.78/3.99 True % 3.78/3.99 Clause #35 (by clausification #[33]): Or (Eq (Or (Or (Not cN) cP) cF) True) (Eq cC True) % 3.78/3.99 Clause #36 (by clausification #[35]): Or (Eq cC True) (Or (Eq (Or (Not cN) cP) True) (Eq cF True)) % 3.78/3.99 Clause #37 (by clausification #[36]): Or (Eq cC True) (Or (Eq cF True) (Or (Eq (Not cN) True) (Eq cP True))) % 3.78/3.99 Clause #38 (by clausification #[37]): Or (Eq cC True) (Or (Eq cF True) (Or (Eq cP True) (Eq cN False))) % 3.78/3.99 Clause #39 (by clausification #[34]): Eq (Or (Or (Or (Not cG) cK) cM) (Not cB)) True % 3.78/3.99 Clause #40 (by clausification #[34]): Eq % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And % 3.78/3.99 (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) (Or (Or (Not cG) cR) cM)) % 3.78/3.99 (Or (Or cG cP) cR)) % 3.78/3.99 (Or (Or (Not cK) (Not cB)) cC)) % 3.78/3.99 (Or (Or (Not cL) (Not cM)) cC)) % 3.78/3.99 (Or (Or cG cR) cK)) % 3.78/3.99 (Or (Or (Not cR) (Not cE)) (Not cC))) % 3.78/3.99 (Or (Or (Or (Not cR) cN) cF) cP)) % 3.78/3.99 (Or (Or (Or (Not cK) (Not cL)) (Not cE)) (Not cM))) % 3.78/3.99 True % 3.78/3.99 Clause #41 (by clausification #[39]): Or (Eq (Or (Or (Not cG) cK) cM) True) (Eq (Not cB) True) % 3.78/3.99 Clause #42 (by clausification #[41]): Or (Eq (Not cB) True) (Or (Eq (Or (Not cG) cK) True) (Eq cM True)) % 3.78/3.99 Clause #43 (by clausification #[42]): Or (Eq (Or (Not cG) cK) True) (Or (Eq cM True) (Eq cB False)) % 3.78/3.99 Clause #44 (by clausification #[43]): Or (Eq cM True) (Or (Eq cB False) (Or (Eq (Not cG) True) (Eq cK True))) % 3.78/3.99 Clause #45 (by clausification #[44]): Or (Eq cM True) (Or (Eq cB False) (Or (Eq cK True) (Eq cG False))) % 3.78/3.99 Clause #46 (by clausification #[40]): Eq (Or (Or (Or (Not cK) (Not cL)) (Not cE)) (Not cM)) True % 3.84/4.02 Clause #47 (by clausification #[40]): Eq % 3.84/4.02 (And % 3.84/4.02 (And % 3.84/4.02 (And % 3.84/4.02 (And % 3.84/4.02 (And % 3.84/4.02 (And (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) (Or (Or (Not cG) cR) cM)) % 3.84/4.02 (Or (Or cG cP) cR)) % 3.84/4.02 (Or (Or (Not cK) (Not cB)) cC)) % 3.84/4.02 (Or (Or (Not cL) (Not cM)) cC)) % 3.84/4.02 (Or (Or cG cR) cK)) % 3.84/4.02 (Or (Or (Not cR) (Not cE)) (Not cC))) % 3.84/4.02 (Or (Or (Or (Not cR) cN) cF) cP)) % 3.84/4.02 True % 3.84/4.02 Clause #48 (by clausification #[46]): Or (Eq (Or (Or (Not cK) (Not cL)) (Not cE)) True) (Eq (Not cM) True) % 3.84/4.02 Clause #49 (by clausification #[48]): Or (Eq (Not cM) True) (Or (Eq (Or (Not cK) (Not cL)) True) (Eq (Not cE) True)) % 3.84/4.02 Clause #50 (by clausification #[49]): Or (Eq (Or (Not cK) (Not cL)) True) (Or (Eq (Not cE) True) (Eq cM False)) % 3.84/4.02 Clause #51 (by clausification #[50]): Or (Eq (Not cE) True) (Or (Eq cM False) (Or (Eq (Not cK) True) (Eq (Not cL) True))) % 3.84/4.02 Clause #52 (by clausification #[51]): Or (Eq cM False) (Or (Eq (Not cK) True) (Or (Eq (Not cL) True) (Eq cE False))) % 3.84/4.02 Clause #53 (by clausification #[52]): Or (Eq cM False) (Or (Eq (Not cL) True) (Or (Eq cE False) (Eq cK False))) % 3.84/4.02 Clause #54 (by clausification #[53]): Or (Eq cM False) (Or (Eq cE False) (Or (Eq cK False) (Eq cL False))) % 3.84/4.02 Clause #55 (by clausification #[47]): Eq (Or (Or (Or (Not cR) cN) cF) cP) True % 3.84/4.02 Clause #56 (by clausification #[47]): Eq % 3.84/4.02 (And % 3.84/4.02 (And % 3.84/4.02 (And % 3.84/4.02 (And % 3.84/4.02 (And (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) (Or (Or (Not cG) cR) cM)) % 3.84/4.02 (Or (Or cG cP) cR)) % 3.84/4.02 (Or (Or (Not cK) (Not cB)) cC)) % 3.84/4.02 (Or (Or (Not cL) (Not cM)) cC)) % 3.84/4.02 (Or (Or cG cR) cK)) % 3.84/4.02 (Or (Or (Not cR) (Not cE)) (Not cC))) % 3.84/4.02 True % 3.84/4.02 Clause #57 (by clausification #[55]): Or (Eq (Or (Or (Not cR) cN) cF) True) (Eq cP True) % 3.84/4.02 Clause #58 (by clausification #[57]): Or (Eq cP True) (Or (Eq (Or (Not cR) cN) True) (Eq cF True)) % 3.84/4.02 Clause #59 (by clausification #[58]): Or (Eq cP True) (Or (Eq cF True) (Or (Eq (Not cR) True) (Eq cN True))) % 3.84/4.02 Clause #60 (by clausification #[59]): Or (Eq cP True) (Or (Eq cF True) (Or (Eq cN True) (Eq cR False))) % 3.84/4.02 Clause #61 (by clausification #[56]): Eq (Or (Or (Not cR) (Not cE)) (Not cC)) True % 3.84/4.02 Clause #62 (by clausification #[56]): Eq % 3.84/4.02 (And % 3.84/4.02 (And % 3.84/4.02 (And % 3.84/4.02 (And (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) (Or (Or (Not cG) cR) cM)) % 3.84/4.02 (Or (Or cG cP) cR)) % 3.84/4.02 (Or (Or (Not cK) (Not cB)) cC)) % 3.84/4.02 (Or (Or (Not cL) (Not cM)) cC)) % 3.84/4.02 (Or (Or cG cR) cK)) % 3.84/4.02 True % 3.84/4.02 Clause #63 (by clausification #[61]): Or (Eq (Or (Not cR) (Not cE)) True) (Eq (Not cC) True) % 3.84/4.02 Clause #64 (by clausification #[63]): Or (Eq (Not cC) True) (Or (Eq (Not cR) True) (Eq (Not cE) True)) % 3.84/4.02 Clause #65 (by clausification #[64]): Or (Eq (Not cR) True) (Or (Eq (Not cE) True) (Eq cC False)) % 3.84/4.02 Clause #66 (by clausification #[65]): Or (Eq (Not cE) True) (Or (Eq cC False) (Eq cR False)) % 3.84/4.02 Clause #67 (by clausification #[66]): Or (Eq cC False) (Or (Eq cR False) (Eq cE False)) % 3.84/4.02 Clause #68 (by clausification #[62]): Eq (Or (Or cG cR) cK) True % 3.84/4.02 Clause #69 (by clausification #[62]): Eq % 3.84/4.02 (And % 3.84/4.02 (And % 3.84/4.02 (And (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) (Or (Or (Not cG) cR) cM)) % 3.84/4.02 (Or (Or cG cP) cR)) % 3.84/4.02 (Or (Or (Not cK) (Not cB)) cC)) % 3.84/4.02 (Or (Or (Not cL) (Not cM)) cC)) % 3.84/4.02 True % 3.84/4.02 Clause #70 (by clausification #[68]): Or (Eq (Or cG cR) True) (Eq cK True) % 3.84/4.02 Clause #71 (by clausification #[70]): Or (Eq cK True) (Or (Eq cG True) (Eq cR True)) % 3.84/4.02 Clause #72 (by clausification #[69]): Eq (Or (Or (Not cL) (Not cM)) cC) True % 3.84/4.02 Clause #73 (by clausification #[69]): Eq % 3.84/4.02 (And % 3.84/4.02 (And (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) (Or (Or (Not cG) cR) cM)) % 3.84/4.02 (Or (Or cG cP) cR)) % 3.84/4.02 (Or (Or (Not cK) (Not cB)) cC)) % 3.84/4.02 True % 3.84/4.02 Clause #74 (by clausification #[72]): Or (Eq (Or (Not cL) (Not cM)) True) (Eq cC True) % 3.84/4.02 Clause #75 (by clausification #[74]): Or (Eq cC True) (Or (Eq (Not cL) True) (Eq (Not cM) True)) % 3.84/4.02 Clause #76 (by clausification #[75]): Or (Eq cC True) (Or (Eq (Not cM) True) (Eq cL False)) % 3.84/4.04 Clause #77 (by clausification #[76]): Or (Eq cC True) (Or (Eq cL False) (Eq cM False)) % 3.84/4.04 Clause #78 (by clausification #[73]): Eq (Or (Or (Not cK) (Not cB)) cC) True % 3.84/4.04 Clause #79 (by clausification #[73]): Eq % 3.84/4.04 (And (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) (Or (Or (Not cG) cR) cM)) % 3.84/4.04 (Or (Or cG cP) cR)) % 3.84/4.04 True % 3.84/4.04 Clause #80 (by clausification #[78]): Or (Eq (Or (Not cK) (Not cB)) True) (Eq cC True) % 3.84/4.04 Clause #81 (by clausification #[80]): Or (Eq cC True) (Or (Eq (Not cK) True) (Eq (Not cB) True)) % 3.84/4.04 Clause #82 (by clausification #[81]): Or (Eq cC True) (Or (Eq (Not cB) True) (Eq cK False)) % 3.84/4.04 Clause #83 (by clausification #[82]): Or (Eq cC True) (Or (Eq cK False) (Eq cB False)) % 3.84/4.04 Clause #84 (by clausification #[79]): Eq (Or (Or cG cP) cR) True % 3.84/4.04 Clause #85 (by clausification #[79]): Eq (And (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) (Or (Or (Not cG) cR) cM)) True % 3.84/4.04 Clause #86 (by clausification #[84]): Or (Eq (Or cG cP) True) (Eq cR True) % 3.84/4.04 Clause #87 (by clausification #[86]): Or (Eq cR True) (Or (Eq cG True) (Eq cP True)) % 3.84/4.04 Clause #88 (by clausification #[85]): Eq (Or (Or (Not cG) cR) cM) True % 3.84/4.04 Clause #89 (by clausification #[85]): Eq (And (And (And cL cE) (Or (Not cF) cB)) (Or (Or (Not cL) (Not cP)) cM)) True % 3.84/4.04 Clause #90 (by clausification #[88]): Or (Eq (Or (Not cG) cR) True) (Eq cM True) % 3.84/4.04 Clause #91 (by clausification #[90]): Or (Eq cM True) (Or (Eq (Not cG) True) (Eq cR True)) % 3.84/4.04 Clause #92 (by clausification #[91]): Or (Eq cM True) (Or (Eq cR True) (Eq cG False)) % 3.84/4.04 Clause #98 (by clausification #[89]): Eq (Or (Or (Not cL) (Not cP)) cM) True % 3.84/4.04 Clause #99 (by clausification #[89]): Eq (And (And cL cE) (Or (Not cF) cB)) True % 3.84/4.04 Clause #100 (by clausification #[98]): Or (Eq (Or (Not cL) (Not cP)) True) (Eq cM True) % 3.84/4.04 Clause #101 (by clausification #[100]): Or (Eq cM True) (Or (Eq (Not cL) True) (Eq (Not cP) True)) % 3.84/4.04 Clause #102 (by clausification #[101]): Or (Eq cM True) (Or (Eq (Not cP) True) (Eq cL False)) % 3.84/4.04 Clause #103 (by clausification #[102]): Or (Eq cM True) (Or (Eq cL False) (Eq cP False)) % 3.84/4.04 Clause #104 (by clausification #[99]): Eq (Or (Not cF) cB) True % 3.84/4.04 Clause #105 (by clausification #[99]): Eq (And cL cE) True % 3.84/4.04 Clause #106 (by clausification #[104]): Or (Eq (Not cF) True) (Eq cB True) % 3.84/4.04 Clause #107 (by clausification #[106]): Or (Eq cB True) (Eq cF False) % 3.84/4.04 Clause #108 (by clausification #[105]): Eq cE True % 3.84/4.04 Clause #109 (by clausification #[105]): Eq cL True % 3.84/4.04 Clause #110 (by backward demodulation #[108, 11]): Or (Eq cN True) (Or (Eq cM False) (Or (Eq cK True) (Or (Eq cG False) (Eq True False)))) % 3.84/4.04 Clause #111 (by backward demodulation #[109, 54]): Or (Eq cM False) (Or (Eq cE False) (Or (Eq cK False) (Eq True False))) % 3.84/4.04 Clause #112 (by backward demodulation #[109, 103]): Or (Eq cM True) (Or (Eq True False) (Eq cP False)) % 3.84/4.04 Clause #113 (by superposition #[109, 77]): Or (Eq cC True) (Or (Eq True False) (Eq cM False)) % 3.84/4.04 Clause #114 (by clausification #[113]): Or (Eq cC True) (Eq cM False) % 3.84/4.04 Clause #115 (by clausification #[112]): Or (Eq cM True) (Eq cP False) % 3.84/4.04 Clause #116 (by superposition #[115, 87]): Or (Eq cM True) (Or (Eq cR True) (Or (Eq cG True) (Eq False True))) % 3.84/4.04 Clause #117 (by clausification #[116]): Or (Eq cM True) (Or (Eq cR True) (Eq cG True)) % 3.84/4.04 Clause #118 (by superposition #[117, 92]): Or (Eq cM True) (Or (Eq cR True) (Or (Eq cM True) (Or (Eq cR True) (Eq True False)))) % 3.84/4.04 Clause #119 (by clausification #[110]): Or (Eq cN True) (Or (Eq cM False) (Or (Eq cK True) (Eq cG False))) % 3.84/4.04 Clause #120 (by clausification #[111]): Or (Eq cM False) (Or (Eq cE False) (Eq cK False)) % 3.84/4.04 Clause #121 (by clausification #[118]): Or (Eq cM True) (Or (Eq cR True) (Or (Eq cM True) (Eq cR True))) % 3.84/4.04 Clause #122 (by eliminate duplicate literals #[121]): Or (Eq cM True) (Eq cR True) % 3.84/4.04 Clause #123 (by superposition #[122, 17]): Or (Eq cM True) (Or (Eq cG True) (Or (Eq cM True) (Or (Eq cK True) (Eq True False)))) % 3.84/4.04 Clause #124 (by superposition #[122, 60]): Or (Eq cM True) (Or (Eq cP True) (Or (Eq cF True) (Or (Eq cN True) (Eq True False)))) % 3.84/4.04 Clause #125 (by clausification #[124]): Or (Eq cM True) (Or (Eq cP True) (Or (Eq cF True) (Eq cN True))) % 3.92/4.07 Clause #126 (by superposition #[125, 38]): Or (Eq cM True) % 3.92/4.07 (Or (Eq cP True) (Or (Eq cF True) (Or (Eq cC True) (Or (Eq cF True) (Or (Eq cP True) (Eq True False)))))) % 3.92/4.07 Clause #127 (by clausification #[123]): Or (Eq cM True) (Or (Eq cG True) (Or (Eq cM True) (Eq cK True))) % 3.92/4.07 Clause #128 (by eliminate duplicate literals #[127]): Or (Eq cM True) (Or (Eq cG True) (Eq cK True)) % 3.92/4.07 Clause #129 (by clausification #[126]): Or (Eq cM True) (Or (Eq cP True) (Or (Eq cF True) (Or (Eq cC True) (Or (Eq cF True) (Eq cP True))))) % 3.92/4.07 Clause #130 (by eliminate duplicate literals #[129]): Or (Eq cM True) (Or (Eq cP True) (Or (Eq cF True) (Eq cC True))) % 3.92/4.07 Clause #131 (by superposition #[130, 107]): Or (Eq cM True) (Or (Eq cP True) (Or (Eq cC True) (Or (Eq cB True) (Eq True False)))) % 3.92/4.07 Clause #132 (by clausification #[131]): Or (Eq cM True) (Or (Eq cP True) (Or (Eq cC True) (Eq cB True))) % 3.92/4.07 Clause #133 (by superposition #[132, 45]): Or (Eq cM True) % 3.92/4.07 (Or (Eq cP True) (Or (Eq cC True) (Or (Eq cM True) (Or (Eq True False) (Or (Eq cK True) (Eq cG False)))))) % 3.92/4.07 Clause #134 (by clausification #[133]): Or (Eq cM True) (Or (Eq cP True) (Or (Eq cC True) (Or (Eq cM True) (Or (Eq cK True) (Eq cG False))))) % 3.92/4.07 Clause #135 (by eliminate duplicate literals #[134]): Or (Eq cM True) (Or (Eq cP True) (Or (Eq cC True) (Or (Eq cK True) (Eq cG False)))) % 3.92/4.07 Clause #137 (by superposition #[135, 128]): Or (Eq cM True) % 3.92/4.07 (Or (Eq cP True) (Or (Eq cC True) (Or (Eq cK True) (Or (Eq cM True) (Or (Eq False True) (Eq cK True)))))) % 3.92/4.07 Clause #138 (by clausification #[137]): Or (Eq cM True) (Or (Eq cP True) (Or (Eq cC True) (Or (Eq cK True) (Or (Eq cM True) (Eq cK True))))) % 3.92/4.07 Clause #139 (by eliminate duplicate literals #[138]): Or (Eq cM True) (Or (Eq cP True) (Or (Eq cC True) (Eq cK True))) % 3.92/4.07 Clause #140 (by superposition #[139, 115]): Or (Eq cM True) (Or (Eq cC True) (Or (Eq cK True) (Or (Eq cM True) (Eq True False)))) % 3.92/4.07 Clause #141 (by clausification #[140]): Or (Eq cM True) (Or (Eq cC True) (Or (Eq cK True) (Eq cM True))) % 3.92/4.07 Clause #142 (by eliminate duplicate literals #[141]): Or (Eq cM True) (Or (Eq cC True) (Eq cK True)) % 3.92/4.07 Clause #144 (by superposition #[142, 67]): Or (Eq cM True) (Or (Eq cK True) (Or (Eq True False) (Or (Eq cR False) (Eq cE False)))) % 3.92/4.07 Clause #145 (by clausification #[144]): Or (Eq cM True) (Or (Eq cK True) (Or (Eq cR False) (Eq cE False))) % 3.92/4.07 Clause #146 (by superposition #[145, 122]): Or (Eq cM True) (Or (Eq cK True) (Or (Eq cE False) (Or (Eq cM True) (Eq False True)))) % 3.92/4.07 Clause #147 (by clausification #[146]): Or (Eq cM True) (Or (Eq cK True) (Or (Eq cE False) (Eq cM True))) % 3.92/4.07 Clause #148 (by eliminate duplicate literals #[147]): Or (Eq cM True) (Or (Eq cK True) (Eq cE False)) % 3.92/4.07 Clause #149 (by superposition #[148, 108]): Or (Eq cM True) (Or (Eq cK True) (Eq False True)) % 3.92/4.07 Clause #152 (by clausification #[149]): Or (Eq cM True) (Eq cK True) % 3.92/4.07 Clause #153 (by superposition #[152, 83]): Or (Eq cM True) (Or (Eq cC True) (Or (Eq True False) (Eq cB False))) % 3.92/4.07 Clause #154 (by clausification #[153]): Or (Eq cM True) (Or (Eq cC True) (Eq cB False)) % 3.92/4.07 Clause #155 (by superposition #[154, 132]): Or (Eq cM True) (Or (Eq cC True) (Or (Eq cM True) (Or (Eq cP True) (Or (Eq cC True) (Eq False True))))) % 3.92/4.07 Clause #156 (by clausification #[155]): Or (Eq cM True) (Or (Eq cC True) (Or (Eq cM True) (Or (Eq cP True) (Eq cC True)))) % 3.92/4.07 Clause #157 (by eliminate duplicate literals #[156]): Or (Eq cM True) (Or (Eq cC True) (Eq cP True)) % 3.92/4.07 Clause #158 (by superposition #[157, 115]): Or (Eq cM True) (Or (Eq cC True) (Or (Eq cM True) (Eq True False))) % 3.92/4.07 Clause #159 (by clausification #[158]): Or (Eq cM True) (Or (Eq cC True) (Eq cM True)) % 3.92/4.07 Clause #160 (by eliminate duplicate literals #[159]): Or (Eq cM True) (Eq cC True) % 3.92/4.07 Clause #162 (by superposition #[160, 67]): Or (Eq cM True) (Or (Eq True False) (Or (Eq cR False) (Eq cE False))) % 3.92/4.07 Clause #163 (by clausification #[162]): Or (Eq cM True) (Or (Eq cR False) (Eq cE False)) % 3.92/4.07 Clause #164 (by superposition #[163, 122]): Or (Eq cM True) (Or (Eq cE False) (Or (Eq cM True) (Eq False True))) % 3.92/4.07 Clause #166 (by clausification #[164]): Or (Eq cM True) (Or (Eq cE False) (Eq cM True)) % 3.92/4.09 Clause #167 (by eliminate duplicate literals #[166]): Or (Eq cM True) (Eq cE False) % 3.92/4.09 Clause #168 (by superposition #[167, 108]): Or (Eq cM True) (Eq False True) % 3.92/4.09 Clause #169 (by clausification #[168]): Eq cM True % 3.92/4.09 Clause #170 (by backward demodulation #[169, 24]): Or (Eq cF True) (Or (Eq cK True) (Or (Eq True False) (Eq cN False))) % 3.92/4.09 Clause #171 (by backward demodulation #[169, 114]): Or (Eq cC True) (Eq True False) % 3.92/4.09 Clause #173 (by backward demodulation #[169, 119]): Or (Eq cN True) (Or (Eq True False) (Or (Eq cK True) (Eq cG False))) % 3.92/4.09 Clause #174 (by backward demodulation #[169, 120]): Or (Eq True False) (Or (Eq cE False) (Eq cK False)) % 3.92/4.09 Clause #182 (by clausification #[171]): Eq cC True % 3.92/4.09 Clause #183 (by backward demodulation #[182, 32]): Or (Eq cR True) (Or (Eq True False) (Or (Eq cG False) (Eq cB False))) % 3.92/4.09 Clause #185 (by backward demodulation #[182, 67]): Or (Eq True False) (Or (Eq cR False) (Eq cE False)) % 3.92/4.09 Clause #187 (by clausification #[174]): Or (Eq cE False) (Eq cK False) % 3.92/4.09 Clause #188 (by superposition #[187, 108]): Or (Eq cK False) (Eq False True) % 3.92/4.09 Clause #189 (by clausification #[170]): Or (Eq cF True) (Or (Eq cK True) (Eq cN False)) % 3.92/4.09 Clause #190 (by clausification #[188]): Eq cK False % 3.92/4.09 Clause #191 (by backward demodulation #[190, 71]): Or (Eq False True) (Or (Eq cG True) (Eq cR True)) % 3.92/4.09 Clause #193 (by backward demodulation #[190, 189]): Or (Eq cF True) (Or (Eq False True) (Eq cN False)) % 3.92/4.09 Clause #194 (by clausification #[191]): Or (Eq cG True) (Eq cR True) % 3.92/4.09 Clause #195 (by clausification #[193]): Or (Eq cF True) (Eq cN False) % 3.92/4.09 Clause #196 (by clausification #[185]): Or (Eq cR False) (Eq cE False) % 3.92/4.09 Clause #197 (by clausification #[173]): Or (Eq cN True) (Or (Eq cK True) (Eq cG False)) % 3.92/4.09 Clause #198 (by forward demodulation #[197, 190]): Or (Eq cN True) (Or (Eq False True) (Eq cG False)) % 3.92/4.09 Clause #199 (by clausification #[198]): Or (Eq cN True) (Eq cG False) % 3.92/4.09 Clause #200 (by superposition #[199, 194]): Or (Eq cN True) (Or (Eq False True) (Eq cR True)) % 3.92/4.09 Clause #201 (by clausification #[200]): Or (Eq cN True) (Eq cR True) % 3.92/4.09 Clause #202 (by superposition #[201, 195]): Or (Eq cR True) (Or (Eq cF True) (Eq True False)) % 3.92/4.09 Clause #203 (by clausification #[202]): Or (Eq cR True) (Eq cF True) % 3.92/4.09 Clause #204 (by superposition #[203, 107]): Or (Eq cR True) (Or (Eq cB True) (Eq True False)) % 3.92/4.09 Clause #205 (by clausification #[204]): Or (Eq cR True) (Eq cB True) % 3.92/4.09 Clause #206 (by clausification #[183]): Or (Eq cR True) (Or (Eq cG False) (Eq cB False)) % 3.92/4.09 Clause #207 (by superposition #[206, 194]): Or (Eq cR True) (Or (Eq cB False) (Or (Eq False True) (Eq cR True))) % 3.92/4.09 Clause #208 (by clausification #[207]): Or (Eq cR True) (Or (Eq cB False) (Eq cR True)) % 3.92/4.09 Clause #209 (by eliminate duplicate literals #[208]): Or (Eq cR True) (Eq cB False) % 3.92/4.09 Clause #210 (by superposition #[209, 205]): Or (Eq cR True) (Or (Eq cR True) (Eq False True)) % 3.92/4.09 Clause #211 (by clausification #[210]): Or (Eq cR True) (Eq cR True) % 3.92/4.09 Clause #212 (by eliminate duplicate literals #[211]): Eq cR True % 3.92/4.09 Clause #215 (by backward demodulation #[212, 196]): Or (Eq True False) (Eq cE False) % 3.92/4.09 Clause #222 (by clausification #[215]): Eq cE False % 3.92/4.09 Clause #223 (by superposition #[222, 108]): Eq False True % 3.92/4.09 Clause #224 (by clausification #[223]): False % 3.92/4.09 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------