%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM783^1 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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:57:19 PM UTC 2025 % Result : Theorem 4.33s 4.50s % Output : Proof 4.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : NUM783^1 : TPTP v9.2.0. Released v3.7.0. % 0.08/0.13 % Command : duper %s % 0.14/0.34 % Computer : n019.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 07:07:38 EDT 2025 % 0.14/0.35 % CPUTime : % 4.33/4.50 SZS status Theorem for theBenchmark.p % 4.33/4.50 SZS output start Proof for theBenchmark.p % 4.33/4.50 Clause #1 (by assumption #[]): Eq % 4.33/4.50 (∀ (Xx0 Xy0 : rat), % 4.33/4.50 Not (or3 (is Xx0 Xy0) (more Xx0 Xy0) (less Xx0 Xy0) → Not (ec3 (is Xx0 Xy0) (more Xx0 Xy0) (less Xx0 Xy0)))) % 4.33/4.50 True % 4.33/4.50 Clause #2 (by assumption #[]): Eq (Not (or3 (is x0 y0) (more x0 y0) (less x0 y0))) True % 4.33/4.50 Clause #7 (by clausification #[2]): Eq (or3 (is x0 y0) (more x0 y0) (less x0 y0)) False % 4.33/4.50 Clause #8 (by identity loobHoist #[7]): Or (Eq (or3 (is x0 y0) (more x0 y0) True) False) (Eq (less x0 y0) False) % 4.33/4.50 Clause #9 (by identity boolHoist #[7]): Or (Eq (or3 (is x0 y0) (more x0 y0) False) False) (Eq (less x0 y0) True) % 4.33/4.50 Clause #10 (by identity loobHoist #[8]): Or (Eq (less x0 y0) False) (Or (Eq (or3 (is x0 y0) True True) False) (Eq (more x0 y0) False)) % 4.33/4.50 Clause #11 (by identity boolHoist #[8]): Or (Eq (less x0 y0) False) (Or (Eq (or3 (is x0 y0) False True) False) (Eq (more x0 y0) True)) % 4.33/4.50 Clause #12 (by identity loobHoist #[10]): Or (Eq (less x0 y0) False) (Or (Eq (more x0 y0) False) (Or (Eq (or3 True True True) False) (Eq (is x0 y0) False))) % 4.33/4.50 Clause #13 (by identity boolHoist #[10]): Or (Eq (less x0 y0) False) (Or (Eq (more x0 y0) False) (Or (Eq (or3 False True True) False) (Eq (is x0 y0) True))) % 4.33/4.50 Clause #14 (by identity loobHoist #[9]): Or (Eq (less x0 y0) True) (Or (Eq (or3 (is x0 y0) True False) False) (Eq (more x0 y0) False)) % 4.33/4.50 Clause #15 (by identity boolHoist #[9]): Or (Eq (less x0 y0) True) (Or (Eq (or3 (is x0 y0) False False) False) (Eq (more x0 y0) True)) % 4.33/4.50 Clause #16 (by identity loobHoist #[14]): Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) False) (Or (Eq (or3 True True False) False) (Eq (is x0 y0) False))) % 4.33/4.50 Clause #17 (by identity boolHoist #[14]): Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) False) (Or (Eq (or3 False True False) False) (Eq (is x0 y0) True))) % 4.33/4.50 Clause #18 (by identity loobHoist #[11]): Or (Eq (less x0 y0) False) (Or (Eq (more x0 y0) True) (Or (Eq (or3 True False True) False) (Eq (is x0 y0) False))) % 4.33/4.50 Clause #19 (by identity boolHoist #[11]): Or (Eq (less x0 y0) False) (Or (Eq (more x0 y0) True) (Or (Eq (or3 False False True) False) (Eq (is x0 y0) True))) % 4.33/4.50 Clause #20 (by identity loobHoist #[15]): Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Or (Eq (or3 True False False) False) (Eq (is x0 y0) False))) % 4.33/4.50 Clause #21 (by identity boolHoist #[15]): Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Or (Eq (or3 False False False) False) (Eq (is x0 y0) True))) % 4.33/4.50 Clause #22 (by clausification #[1]): ∀ (a : rat), % 4.33/4.50 Eq (∀ (Xy0 : rat), Not (or3 (is a Xy0) (more a Xy0) (less a Xy0) → Not (ec3 (is a Xy0) (more a Xy0) (less a Xy0)))) % 4.33/4.50 True % 4.33/4.50 Clause #23 (by clausification #[22]): ∀ (a a_1 : rat), % 4.33/4.50 Eq (Not (or3 (is a a_1) (more a a_1) (less a a_1) → Not (ec3 (is a a_1) (more a a_1) (less a a_1)))) True % 4.33/4.50 Clause #24 (by clausification #[23]): ∀ (a a_1 : rat), Eq (or3 (is a a_1) (more a a_1) (less a a_1) → Not (ec3 (is a a_1) (more a a_1) (less a a_1))) False % 4.33/4.50 Clause #25 (by clausification #[24]): ∀ (a a_1 : rat), Eq (or3 (is a a_1) (more a a_1) (less a a_1)) True % 4.33/4.50 Clause #27 (by identity loobHoist #[25]): ∀ (a a_1 : rat), Or (Eq (or3 (is a a_1) (more a a_1) True) True) (Eq (less a a_1) False) % 4.33/4.50 Clause #28 (by identity boolHoist #[25]): ∀ (a a_1 : rat), Or (Eq (or3 (is a a_1) (more a a_1) False) True) (Eq (less a a_1) True) % 4.33/4.50 Clause #29 (by identity loobHoist #[27]): ∀ (a a_1 : rat), Or (Eq (less a a_1) False) (Or (Eq (or3 (is a a_1) True True) True) (Eq (more a a_1) False)) % 4.33/4.50 Clause #30 (by identity boolHoist #[27]): ∀ (a a_1 : rat), Or (Eq (less a a_1) False) (Or (Eq (or3 (is a a_1) False True) True) (Eq (more a a_1) True)) % 4.33/4.50 Clause #31 (by identity loobHoist #[29]): ∀ (a a_1 : rat), % 4.33/4.50 Or (Eq (less a a_1) False) (Or (Eq (more a a_1) False) (Or (Eq (or3 True True True) True) (Eq (is a a_1) False))) % 4.33/4.50 Clause #32 (by identity boolHoist #[29]): ∀ (a a_1 : rat), % 4.33/4.50 Or (Eq (less a a_1) False) (Or (Eq (more a a_1) False) (Or (Eq (or3 False True True) True) (Eq (is a a_1) True))) % 4.33/4.50 Clause #40 (by identity loobHoist #[28]): ∀ (a a_1 : rat), Or (Eq (less a a_1) True) (Or (Eq (or3 (is a a_1) True False) True) (Eq (more a a_1) False)) % 4.36/4.53 Clause #41 (by identity boolHoist #[28]): ∀ (a a_1 : rat), Or (Eq (less a a_1) True) (Or (Eq (or3 (is a a_1) False False) True) (Eq (more a a_1) True)) % 4.36/4.53 Clause #42 (by identity loobHoist #[40]): ∀ (a a_1 : rat), % 4.36/4.53 Or (Eq (less a a_1) True) (Or (Eq (more a a_1) False) (Or (Eq (or3 True True False) True) (Eq (is a a_1) False))) % 4.36/4.53 Clause #43 (by identity boolHoist #[40]): ∀ (a a_1 : rat), % 4.36/4.53 Or (Eq (less a a_1) True) (Or (Eq (more a a_1) False) (Or (Eq (or3 False True False) True) (Eq (is a a_1) True))) % 4.36/4.53 Clause #50 (by identity loobHoist #[30]): ∀ (a a_1 : rat), % 4.36/4.53 Or (Eq (less a a_1) False) (Or (Eq (more a a_1) True) (Or (Eq (or3 True False True) True) (Eq (is a a_1) False))) % 4.36/4.53 Clause #51 (by identity boolHoist #[30]): ∀ (a a_1 : rat), % 4.36/4.53 Or (Eq (less a a_1) False) (Or (Eq (more a a_1) True) (Or (Eq (or3 False False True) True) (Eq (is a a_1) True))) % 4.36/4.53 Clause #54 (by identity loobHoist #[41]): ∀ (a a_1 : rat), % 4.36/4.53 Or (Eq (less a a_1) True) (Or (Eq (more a a_1) True) (Or (Eq (or3 True False False) True) (Eq (is a a_1) False))) % 4.36/4.53 Clause #55 (by identity boolHoist #[41]): ∀ (a a_1 : rat), % 4.36/4.53 Or (Eq (less a a_1) True) (Or (Eq (more a a_1) True) (Or (Eq (or3 False False False) True) (Eq (is a a_1) True))) % 4.36/4.53 Clause #58 (by superposition #[55, 21]): ∀ (a a_1 : rat), % 4.36/4.53 Or (Eq (less a a_1) True) % 4.36/4.53 (Or (Eq (more a a_1) True) % 4.36/4.53 (Or (Eq (is a a_1) True) % 4.36/4.53 (Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Or (Eq True False) (Eq (is x0 y0) True)))))) % 4.36/4.53 Clause #61 (by clausification #[58]): ∀ (a a_1 : rat), % 4.36/4.53 Or (Eq (less a a_1) True) % 4.36/4.53 (Or (Eq (more a a_1) True) % 4.36/4.53 (Or (Eq (is a a_1) True) (Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Eq (is x0 y0) True))))) % 4.36/4.53 Clause #66 (by equality factoring #[61]): Or (Eq (less x0 y0) True) % 4.36/4.53 (Or (Eq (more x0 y0) True) % 4.36/4.53 (Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Or (Ne True True) (Eq (is x0 y0) True))))) % 4.36/4.53 Clause #67 (by clausification #[66]): Or (Eq (less x0 y0) True) % 4.36/4.53 (Or (Eq (more x0 y0) True) % 4.36/4.53 (Or (Eq (less x0 y0) True) % 4.36/4.53 (Or (Eq (more x0 y0) True) (Or (Eq (is x0 y0) True) (Or (Eq True False) (Eq True False)))))) % 4.36/4.53 Clause #69 (by clausification #[67]): Or (Eq (less x0 y0) True) % 4.36/4.53 (Or (Eq (more x0 y0) True) % 4.36/4.53 (Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Or (Eq (is x0 y0) True) (Eq True False))))) % 4.36/4.53 Clause #70 (by clausification #[69]): Or (Eq (less x0 y0) True) % 4.36/4.53 (Or (Eq (more x0 y0) True) (Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Eq (is x0 y0) True)))) % 4.36/4.53 Clause #71 (by eliminate duplicate literals #[70]): Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Eq (is x0 y0) True)) % 4.36/4.53 Clause #73 (by superposition #[71, 54]): Or (Eq (less x0 y0) True) % 4.36/4.53 (Or (Eq (more x0 y0) True) % 4.36/4.53 (Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Or (Eq (or3 True False False) True) (Eq True False))))) % 4.36/4.53 Clause #76 (by clausification #[73]): Or (Eq (less x0 y0) True) % 4.36/4.53 (Or (Eq (more x0 y0) True) (Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Eq (or3 True False False) True)))) % 4.36/4.53 Clause #77 (by eliminate duplicate literals #[76]): Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Eq (or3 True False False) True)) % 4.36/4.53 Clause #78 (by superposition #[77, 20]): Or (Eq (less x0 y0) True) % 4.36/4.53 (Or (Eq (more x0 y0) True) % 4.36/4.53 (Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Or (Eq True False) (Eq (is x0 y0) False))))) % 4.36/4.53 Clause #85 (by clausification #[78]): Or (Eq (less x0 y0) True) % 4.36/4.53 (Or (Eq (more x0 y0) True) (Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Eq (is x0 y0) False)))) % 4.36/4.53 Clause #86 (by eliminate duplicate literals #[85]): Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Eq (is x0 y0) False)) % 4.36/4.53 Clause #87 (by superposition #[86, 71]): Or (Eq (less x0 y0) True) % 4.36/4.53 (Or (Eq (more x0 y0) True) (Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Eq False True)))) % 4.36/4.53 Clause #88 (by clausification #[87]): Or (Eq (less x0 y0) True) (Or (Eq (more x0 y0) True) (Or (Eq (less x0 y0) True) (Eq (more x0 y0) True))) % 4.36/4.53 Clause #89 (by eliminate duplicate literals #[88]): Or (Eq (less x0 y0) True) (Eq (more x0 y0) True) % 4.40/4.56 Clause #90 (by superposition #[89, 16]): Or (Eq (less x0 y0) True) % 4.40/4.56 (Or (Eq (less x0 y0) True) (Or (Eq True False) (Or (Eq (or3 True True False) False) (Eq (is x0 y0) False)))) % 4.40/4.56 Clause #91 (by superposition #[89, 17]): Or (Eq (less x0 y0) True) % 4.40/4.56 (Or (Eq (less x0 y0) True) (Or (Eq True False) (Or (Eq (or3 False True False) False) (Eq (is x0 y0) True)))) % 4.40/4.56 Clause #92 (by superposition #[89, 42]): Or (Eq (less x0 y0) True) % 4.40/4.56 (Or (Eq (less x0 y0) True) (Or (Eq True False) (Or (Eq (or3 True True False) True) (Eq (is x0 y0) False)))) % 4.40/4.56 Clause #94 (by superposition #[89, 43]): Or (Eq (less x0 y0) True) % 4.40/4.56 (Or (Eq (less x0 y0) True) (Or (Eq True False) (Or (Eq (or3 False True False) True) (Eq (is x0 y0) True)))) % 4.40/4.56 Clause #96 (by clausification #[90]): Or (Eq (less x0 y0) True) (Or (Eq (less x0 y0) True) (Or (Eq (or3 True True False) False) (Eq (is x0 y0) False))) % 4.40/4.56 Clause #97 (by eliminate duplicate literals #[96]): Or (Eq (less x0 y0) True) (Or (Eq (or3 True True False) False) (Eq (is x0 y0) False)) % 4.40/4.56 Clause #100 (by clausification #[92]): Or (Eq (less x0 y0) True) (Or (Eq (less x0 y0) True) (Or (Eq (or3 True True False) True) (Eq (is x0 y0) False))) % 4.40/4.56 Clause #101 (by eliminate duplicate literals #[100]): Or (Eq (less x0 y0) True) (Or (Eq (or3 True True False) True) (Eq (is x0 y0) False)) % 4.40/4.56 Clause #108 (by clausification #[91]): Or (Eq (less x0 y0) True) (Or (Eq (less x0 y0) True) (Or (Eq (or3 False True False) False) (Eq (is x0 y0) True))) % 4.40/4.56 Clause #109 (by eliminate duplicate literals #[108]): Or (Eq (less x0 y0) True) (Or (Eq (or3 False True False) False) (Eq (is x0 y0) True)) % 4.40/4.56 Clause #110 (by clausification #[94]): Or (Eq (less x0 y0) True) (Or (Eq (less x0 y0) True) (Or (Eq (or3 False True False) True) (Eq (is x0 y0) True))) % 4.40/4.56 Clause #111 (by eliminate duplicate literals #[110]): Or (Eq (less x0 y0) True) (Or (Eq (or3 False True False) True) (Eq (is x0 y0) True)) % 4.40/4.56 Clause #112 (by superposition #[111, 109]): Or (Eq (less x0 y0) True) % 4.40/4.56 (Or (Eq (is x0 y0) True) (Or (Eq (less x0 y0) True) (Or (Eq True False) (Eq (is x0 y0) True)))) % 4.40/4.56 Clause #113 (by clausification #[112]): Or (Eq (less x0 y0) True) (Or (Eq (is x0 y0) True) (Or (Eq (less x0 y0) True) (Eq (is x0 y0) True))) % 4.40/4.56 Clause #114 (by eliminate duplicate literals #[113]): Or (Eq (less x0 y0) True) (Eq (is x0 y0) True) % 4.40/4.56 Clause #115 (by superposition #[114, 101]): Or (Eq (less x0 y0) True) (Or (Eq (less x0 y0) True) (Or (Eq (or3 True True False) True) (Eq True False))) % 4.40/4.56 Clause #118 (by clausification #[115]): Or (Eq (less x0 y0) True) (Or (Eq (less x0 y0) True) (Eq (or3 True True False) True)) % 4.40/4.56 Clause #119 (by eliminate duplicate literals #[118]): Or (Eq (less x0 y0) True) (Eq (or3 True True False) True) % 4.40/4.56 Clause #120 (by superposition #[119, 97]): Or (Eq (less x0 y0) True) (Or (Eq (less x0 y0) True) (Or (Eq True False) (Eq (is x0 y0) False))) % 4.40/4.56 Clause #121 (by clausification #[120]): Or (Eq (less x0 y0) True) (Or (Eq (less x0 y0) True) (Eq (is x0 y0) False)) % 4.40/4.56 Clause #122 (by eliminate duplicate literals #[121]): Or (Eq (less x0 y0) True) (Eq (is x0 y0) False) % 4.40/4.56 Clause #123 (by superposition #[122, 114]): Or (Eq (less x0 y0) True) (Or (Eq (less x0 y0) True) (Eq False True)) % 4.40/4.56 Clause #130 (by clausification #[123]): Or (Eq (less x0 y0) True) (Eq (less x0 y0) True) % 4.40/4.56 Clause #131 (by eliminate duplicate literals #[130]): Eq (less x0 y0) True % 4.40/4.56 Clause #132 (by backward demodulation #[131, 12]): Or (Eq True False) (Or (Eq (more x0 y0) False) (Or (Eq (or3 True True True) False) (Eq (is x0 y0) False))) % 4.40/4.56 Clause #133 (by backward demodulation #[131, 18]): Or (Eq True False) (Or (Eq (more x0 y0) True) (Or (Eq (or3 True False True) False) (Eq (is x0 y0) False))) % 4.40/4.56 Clause #134 (by backward demodulation #[131, 13]): Or (Eq True False) (Or (Eq (more x0 y0) False) (Or (Eq (or3 False True True) False) (Eq (is x0 y0) True))) % 4.40/4.56 Clause #135 (by backward demodulation #[131, 19]): Or (Eq True False) (Or (Eq (more x0 y0) True) (Or (Eq (or3 False False True) False) (Eq (is x0 y0) True))) % 4.40/4.56 Clause #140 (by superposition #[131, 31]): Or (Eq True False) (Or (Eq (more x0 y0) False) (Or (Eq (or3 True True True) True) (Eq (is x0 y0) False))) % 4.40/4.59 Clause #143 (by superposition #[131, 50]): Or (Eq True False) (Or (Eq (more x0 y0) True) (Or (Eq (or3 True False True) True) (Eq (is x0 y0) False))) % 4.40/4.59 Clause #146 (by superposition #[131, 32]): Or (Eq True False) (Or (Eq (more x0 y0) False) (Or (Eq (or3 False True True) True) (Eq (is x0 y0) True))) % 4.40/4.59 Clause #147 (by superposition #[131, 51]): Or (Eq True False) (Or (Eq (more x0 y0) True) (Or (Eq (or3 False False True) True) (Eq (is x0 y0) True))) % 4.40/4.59 Clause #154 (by clausification #[147]): Or (Eq (more x0 y0) True) (Or (Eq (or3 False False True) True) (Eq (is x0 y0) True)) % 4.40/4.59 Clause #157 (by clausification #[146]): Or (Eq (more x0 y0) False) (Or (Eq (or3 False True True) True) (Eq (is x0 y0) True)) % 4.40/4.59 Clause #158 (by clausification #[143]): Or (Eq (more x0 y0) True) (Or (Eq (or3 True False True) True) (Eq (is x0 y0) False)) % 4.40/4.59 Clause #163 (by clausification #[140]): Or (Eq (more x0 y0) False) (Or (Eq (or3 True True True) True) (Eq (is x0 y0) False)) % 4.40/4.59 Clause #165 (by clausification #[135]): Or (Eq (more x0 y0) True) (Or (Eq (or3 False False True) False) (Eq (is x0 y0) True)) % 4.40/4.59 Clause #166 (by superposition #[165, 154]): Or (Eq (more x0 y0) True) % 4.40/4.59 (Or (Eq (is x0 y0) True) (Or (Eq (more x0 y0) True) (Or (Eq False True) (Eq (is x0 y0) True)))) % 4.40/4.59 Clause #167 (by clausification #[134]): Or (Eq (more x0 y0) False) (Or (Eq (or3 False True True) False) (Eq (is x0 y0) True)) % 4.40/4.59 Clause #171 (by clausification #[133]): Or (Eq (more x0 y0) True) (Or (Eq (or3 True False True) False) (Eq (is x0 y0) False)) % 4.40/4.59 Clause #172 (by clausification #[132]): Or (Eq (more x0 y0) False) (Or (Eq (or3 True True True) False) (Eq (is x0 y0) False)) % 4.40/4.59 Clause #173 (by clausification #[166]): Or (Eq (more x0 y0) True) (Or (Eq (is x0 y0) True) (Or (Eq (more x0 y0) True) (Eq (is x0 y0) True))) % 4.40/4.59 Clause #174 (by eliminate duplicate literals #[173]): Or (Eq (more x0 y0) True) (Eq (is x0 y0) True) % 4.40/4.59 Clause #175 (by superposition #[174, 158]): Or (Eq (more x0 y0) True) (Or (Eq (more x0 y0) True) (Or (Eq (or3 True False True) True) (Eq True False))) % 4.40/4.59 Clause #181 (by clausification #[175]): Or (Eq (more x0 y0) True) (Or (Eq (more x0 y0) True) (Eq (or3 True False True) True)) % 4.40/4.59 Clause #182 (by eliminate duplicate literals #[181]): Or (Eq (more x0 y0) True) (Eq (or3 True False True) True) % 4.40/4.59 Clause #183 (by superposition #[182, 171]): Or (Eq (more x0 y0) True) (Or (Eq (more x0 y0) True) (Or (Eq True False) (Eq (is x0 y0) False))) % 4.40/4.59 Clause #187 (by clausification #[183]): Or (Eq (more x0 y0) True) (Or (Eq (more x0 y0) True) (Eq (is x0 y0) False)) % 4.40/4.59 Clause #188 (by eliminate duplicate literals #[187]): Or (Eq (more x0 y0) True) (Eq (is x0 y0) False) % 4.40/4.59 Clause #189 (by superposition #[188, 174]): Or (Eq (more x0 y0) True) (Or (Eq (more x0 y0) True) (Eq False True)) % 4.40/4.59 Clause #190 (by clausification #[189]): Or (Eq (more x0 y0) True) (Eq (more x0 y0) True) % 4.40/4.59 Clause #191 (by eliminate duplicate literals #[190]): Eq (more x0 y0) True % 4.40/4.59 Clause #193 (by backward demodulation #[191, 157]): Or (Eq True False) (Or (Eq (or3 False True True) True) (Eq (is x0 y0) True)) % 4.40/4.59 Clause #195 (by backward demodulation #[191, 163]): Or (Eq True False) (Or (Eq (or3 True True True) True) (Eq (is x0 y0) False)) % 4.40/4.59 Clause #196 (by backward demodulation #[191, 167]): Or (Eq True False) (Or (Eq (or3 False True True) False) (Eq (is x0 y0) True)) % 4.40/4.59 Clause #197 (by backward demodulation #[191, 172]): Or (Eq True False) (Or (Eq (or3 True True True) False) (Eq (is x0 y0) False)) % 4.40/4.59 Clause #204 (by clausification #[196]): Or (Eq (or3 False True True) False) (Eq (is x0 y0) True) % 4.40/4.59 Clause #208 (by clausification #[195]): Or (Eq (or3 True True True) True) (Eq (is x0 y0) False) % 4.40/4.59 Clause #210 (by clausification #[193]): Or (Eq (or3 False True True) True) (Eq (is x0 y0) True) % 4.40/4.59 Clause #211 (by superposition #[210, 204]): Or (Eq (is x0 y0) True) (Or (Eq True False) (Eq (is x0 y0) True)) % 4.40/4.59 Clause #212 (by clausification #[211]): Or (Eq (is x0 y0) True) (Eq (is x0 y0) True) % 4.40/4.59 Clause #213 (by eliminate duplicate literals #[212]): Eq (is x0 y0) True % 4.40/4.59 Clause #215 (by backward demodulation #[213, 208]): Or (Eq (or3 True True True) True) (Eq True False) % 4.40/4.59 Clause #221 (by clausification #[215]): Eq (or3 True True True) True % 4.40/4.59 Clause #224 (by clausification #[197]): Or (Eq (or3 True True True) False) (Eq (is x0 y0) False) % 4.40/4.59 Clause #225 (by forward demodulation #[224, 213]): Or (Eq (or3 True True True) False) (Eq True False) % 4.40/4.59 Clause #226 (by clausification #[225]): Eq (or3 True True True) False % 4.40/4.59 Clause #227 (by superposition #[226, 221]): Eq False True % 4.40/4.59 Clause #233 (by clausification #[227]): False % 4.40/4.59 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------