%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS103+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n029.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:52:37 PM UTC 2025 % Result : Unsatisfiable 8.80s 8.97s % Output : Proof 9.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : KRS103+1 : TPTP v9.2.0. Released v3.1.0. % 0.10/0.12 % Command : duper %s % 0.11/0.32 % Computer : n029.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Thu Oct 2 10:22:53 EDT 2025 % 0.11/0.32 % CPUTime : % 8.80/8.97 SZS status Theorem for theBenchmark.p % 8.80/8.97 SZS output start Proof for theBenchmark.p % 8.80/8.97 Clause #3 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus3 X) (cminus5 X)) (cminus8 X)) True % 8.80/8.97 Clause #4 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus3 X) (cplus7 X)) (cplus8 X)) True % 8.80/8.97 Clause #8 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus7 X) (cplus9 X)) (cminus6 X)) True % 8.80/8.97 Clause #9 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus9 X) (cminus4 X)) (cminus8 X)) True % 8.80/8.97 Clause #15 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus3 X) (cplus5 X)) (cminus8 X)) True % 8.80/8.97 Clause #18 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus2 X) (cplus6 X)) (cplus9 X)) True % 8.80/8.97 Clause #20 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus3 X) (cplus2 X)) (cplus8 X)) True % 8.80/8.97 Clause #21 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus2 X) (cplus4 X)) (cminus6 X)) True % 8.80/8.97 Clause #22 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus2 X) (cplus6 X)) (cminus7 X)) True % 8.80/8.97 Clause #25 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cplus3 X) (cplus4 X)) (cplus9 X)) True % 8.80/8.97 Clause #28 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus9 X) (cplus3 X)) (cplus4 X)) True % 8.80/8.97 Clause #29 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus4 X) (cminus3 X)) (cminus7 X)) True % 8.80/8.97 Clause #31 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus4 X) (cminus8 X)) (cplus9 X)) True % 8.80/8.97 Clause #33 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus9 X) (cminus2 X)) (cplus7 X)) True % 8.80/8.97 Clause #34 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus4 X) (cplus9 X)) (cplus7 X)) True % 8.80/8.97 Clause #35 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus9 X) (cminus2 X)) (cplus3 X)) True % 8.80/8.97 Clause #38 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cplus3 X) (cplus4 X)) (cplus6 X)) True % 8.80/8.97 Clause #45 (by assumption #[]): Eq (∀ (X : Iota), cTest X → Or (Or (cminus4 X) (cplus2 X)) (cplus8 X)) True % 8.80/8.97 Clause #47 (by assumption #[]): Eq (cTest i2003_11_14_17_20_46476) True % 8.80/8.97 Clause #48 (by assumption #[]): Eq (∀ (X : Iota), Not (And (cminus8 X) (cplus8 X))) True % 8.80/8.97 Clause #49 (by assumption #[]): Eq (∀ (X : Iota), Not (And (cminus9 X) (cplus9 X))) True % 8.80/8.97 Clause #50 (by assumption #[]): Eq (∀ (X : Iota), Not (And (cplus4 X) (cminus4 X))) True % 8.80/8.97 Clause #51 (by assumption #[]): Eq (∀ (X : Iota), Not (And (cminus7 X) (cplus7 X))) True % 8.80/8.97 Clause #52 (by assumption #[]): Eq (∀ (X : Iota), Not (And (cplus3 X) (cminus3 X))) True % 8.80/8.97 Clause #53 (by assumption #[]): Eq (∀ (X : Iota), Not (And (cplus5 X) (cminus5 X))) True % 8.80/8.97 Clause #54 (by assumption #[]): Eq (∀ (X : Iota), Not (And (cminus2 X) (cplus2 X))) True % 8.80/8.97 Clause #56 (by assumption #[]): Eq (∀ (X : Iota), Not (And (cplus6 X) (cminus6 X))) True % 8.80/8.97 Clause #57 (by clausification #[56]): ∀ (a : Iota), Eq (Not (And (cplus6 a) (cminus6 a))) True % 8.80/8.97 Clause #58 (by clausification #[57]): ∀ (a : Iota), Eq (And (cplus6 a) (cminus6 a)) False % 8.80/8.97 Clause #59 (by clausification #[58]): ∀ (a : Iota), Or (Eq (cplus6 a) False) (Eq (cminus6 a) False) % 8.80/8.97 Clause #63 (by clausification #[54]): ∀ (a : Iota), Eq (Not (And (cminus2 a) (cplus2 a))) True % 8.80/8.97 Clause #64 (by clausification #[63]): ∀ (a : Iota), Eq (And (cminus2 a) (cplus2 a)) False % 8.80/8.97 Clause #65 (by clausification #[64]): ∀ (a : Iota), Or (Eq (cminus2 a) False) (Eq (cplus2 a) False) % 8.80/8.97 Clause #66 (by clausification #[53]): ∀ (a : Iota), Eq (Not (And (cplus5 a) (cminus5 a))) True % 8.80/8.97 Clause #67 (by clausification #[66]): ∀ (a : Iota), Eq (And (cplus5 a) (cminus5 a)) False % 8.80/8.97 Clause #68 (by clausification #[67]): ∀ (a : Iota), Or (Eq (cplus5 a) False) (Eq (cminus5 a) False) % 8.80/8.97 Clause #73 (by clausification #[52]): ∀ (a : Iota), Eq (Not (And (cplus3 a) (cminus3 a))) True % 8.80/8.97 Clause #74 (by clausification #[73]): ∀ (a : Iota), Eq (And (cplus3 a) (cminus3 a)) False % 8.80/8.97 Clause #75 (by clausification #[74]): ∀ (a : Iota), Or (Eq (cplus3 a) False) (Eq (cminus3 a) False) % 8.80/8.97 Clause #76 (by clausification #[51]): ∀ (a : Iota), Eq (Not (And (cminus7 a) (cplus7 a))) True % 8.86/9.02 Clause #77 (by clausification #[76]): ∀ (a : Iota), Eq (And (cminus7 a) (cplus7 a)) False % 8.86/9.02 Clause #78 (by clausification #[77]): ∀ (a : Iota), Or (Eq (cminus7 a) False) (Eq (cplus7 a) False) % 8.86/9.02 Clause #79 (by clausification #[50]): ∀ (a : Iota), Eq (Not (And (cplus4 a) (cminus4 a))) True % 8.86/9.02 Clause #80 (by clausification #[79]): ∀ (a : Iota), Eq (And (cplus4 a) (cminus4 a)) False % 8.86/9.02 Clause #81 (by clausification #[80]): ∀ (a : Iota), Or (Eq (cplus4 a) False) (Eq (cminus4 a) False) % 8.86/9.02 Clause #82 (by clausification #[49]): ∀ (a : Iota), Eq (Not (And (cminus9 a) (cplus9 a))) True % 8.86/9.02 Clause #83 (by clausification #[82]): ∀ (a : Iota), Eq (And (cminus9 a) (cplus9 a)) False % 8.86/9.02 Clause #84 (by clausification #[83]): ∀ (a : Iota), Or (Eq (cminus9 a) False) (Eq (cplus9 a) False) % 8.86/9.02 Clause #90 (by clausification #[48]): ∀ (a : Iota), Eq (Not (And (cminus8 a) (cplus8 a))) True % 8.86/9.02 Clause #91 (by clausification #[90]): ∀ (a : Iota), Eq (And (cminus8 a) (cplus8 a)) False % 8.86/9.02 Clause #92 (by clausification #[91]): ∀ (a : Iota), Or (Eq (cminus8 a) False) (Eq (cplus8 a) False) % 8.86/9.02 Clause #99 (by clausification #[3]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus3 a) (cminus5 a)) (cminus8 a)) True % 8.86/9.02 Clause #100 (by clausification #[99]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus3 a) (cminus5 a)) (cminus8 a)) True) % 8.86/9.02 Clause #101 (by clausification #[100]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus3 a) (cminus5 a)) True) (Eq (cminus8 a) True)) % 8.86/9.02 Clause #102 (by clausification #[101]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cminus8 a) True) (Or (Eq (cminus3 a) True) (Eq (cminus5 a) True))) % 8.86/9.02 Clause #103 (by superposition #[102, 47]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) % 8.86/9.02 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Or (Eq (cminus5 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.86/9.02 Clause #110 (by clausification #[103]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) % 8.86/9.02 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Eq (cminus5 i2003_11_14_17_20_46476) True)) % 8.86/9.02 Clause #111 (by clausification #[45]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus4 a) (cplus2 a)) (cplus8 a)) True % 8.86/9.02 Clause #112 (by clausification #[111]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus4 a) (cplus2 a)) (cplus8 a)) True) % 8.86/9.02 Clause #113 (by clausification #[112]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus4 a) (cplus2 a)) True) (Eq (cplus8 a) True)) % 8.86/9.02 Clause #114 (by clausification #[113]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cplus8 a) True) (Or (Eq (cminus4 a) True) (Eq (cplus2 a) True))) % 8.86/9.02 Clause #115 (by superposition #[114, 47]): Or (Eq (cplus8 i2003_11_14_17_20_46476) True) % 8.86/9.02 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq (cplus2 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.86/9.02 Clause #116 (by clausification #[115]): Or (Eq (cplus8 i2003_11_14_17_20_46476) True) % 8.86/9.02 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) True)) % 8.86/9.02 Clause #122 (by clausification #[4]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus3 a) (cplus7 a)) (cplus8 a)) True % 8.86/9.02 Clause #123 (by clausification #[122]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus3 a) (cplus7 a)) (cplus8 a)) True) % 8.86/9.02 Clause #124 (by clausification #[123]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus3 a) (cplus7 a)) True) (Eq (cplus8 a) True)) % 8.86/9.02 Clause #125 (by clausification #[124]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cplus8 a) True) (Or (Eq (cminus3 a) True) (Eq (cplus7 a) True))) % 8.86/9.02 Clause #126 (by superposition #[125, 47]): Or (Eq (cplus8 i2003_11_14_17_20_46476) True) % 8.86/9.02 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Or (Eq (cplus7 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.86/9.02 Clause #127 (by clausification #[126]): Or (Eq (cplus8 i2003_11_14_17_20_46476) True) % 8.86/9.02 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Eq (cplus7 i2003_11_14_17_20_46476) True)) % 8.86/9.02 Clause #175 (by clausification #[8]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus7 a) (cplus9 a)) (cminus6 a)) True % 8.86/9.02 Clause #176 (by clausification #[175]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus7 a) (cplus9 a)) (cminus6 a)) True) % 8.87/9.07 Clause #177 (by clausification #[176]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus7 a) (cplus9 a)) True) (Eq (cminus6 a) True)) % 8.87/9.07 Clause #178 (by clausification #[177]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cminus6 a) True) (Or (Eq (cminus7 a) True) (Eq (cplus9 a) True))) % 8.87/9.07 Clause #179 (by superposition #[178, 47]): Or (Eq (cminus6 i2003_11_14_17_20_46476) True) % 8.87/9.07 (Or (Eq (cminus7 i2003_11_14_17_20_46476) True) (Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.87/9.07 Clause #180 (by clausification #[179]): Or (Eq (cminus6 i2003_11_14_17_20_46476) True) % 8.87/9.07 (Or (Eq (cminus7 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) True)) % 8.87/9.07 Clause #181 (by clausification #[31]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus4 a) (cminus8 a)) (cplus9 a)) True % 8.87/9.07 Clause #182 (by clausification #[181]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus4 a) (cminus8 a)) (cplus9 a)) True) % 8.87/9.07 Clause #183 (by clausification #[182]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus4 a) (cminus8 a)) True) (Eq (cplus9 a) True)) % 8.87/9.07 Clause #184 (by clausification #[183]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cplus9 a) True) (Or (Eq (cminus4 a) True) (Eq (cminus8 a) True))) % 8.87/9.07 Clause #185 (by superposition #[184, 47]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 8.87/9.07 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq (cminus8 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.87/9.07 Clause #186 (by clausification #[185]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 8.87/9.07 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cminus8 i2003_11_14_17_20_46476) True)) % 8.87/9.07 Clause #187 (by superposition #[186, 92]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 8.87/9.07 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus8 i2003_11_14_17_20_46476) False))) % 8.87/9.07 Clause #188 (by clausification #[187]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 8.87/9.07 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus8 i2003_11_14_17_20_46476) False)) % 8.87/9.07 Clause #189 (by superposition #[188, 116]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 8.87/9.07 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 8.87/9.07 (Or (Eq False True) (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) True)))) % 8.87/9.07 Clause #192 (by clausification #[29]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus4 a) (cminus3 a)) (cminus7 a)) True % 8.87/9.07 Clause #193 (by clausification #[192]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus4 a) (cminus3 a)) (cminus7 a)) True) % 8.87/9.07 Clause #194 (by clausification #[193]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus4 a) (cminus3 a)) True) (Eq (cminus7 a) True)) % 8.87/9.07 Clause #195 (by clausification #[194]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cminus7 a) True) (Or (Eq (cminus4 a) True) (Eq (cminus3 a) True))) % 8.87/9.07 Clause #196 (by superposition #[195, 47]): Or (Eq (cminus7 i2003_11_14_17_20_46476) True) % 8.87/9.07 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.87/9.07 Clause #197 (by clausification #[9]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus9 a) (cminus4 a)) (cminus8 a)) True % 8.87/9.07 Clause #198 (by clausification #[197]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus9 a) (cminus4 a)) (cminus8 a)) True) % 8.87/9.07 Clause #199 (by clausification #[198]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus9 a) (cminus4 a)) True) (Eq (cminus8 a) True)) % 8.87/9.07 Clause #200 (by clausification #[199]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cminus8 a) True) (Or (Eq (cminus9 a) True) (Eq (cminus4 a) True))) % 8.87/9.07 Clause #201 (by superposition #[200, 47]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) % 8.87/9.07 (Or (Eq (cminus9 i2003_11_14_17_20_46476) True) (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.87/9.07 Clause #202 (by clausification #[201]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) % 8.87/9.07 (Or (Eq (cminus9 i2003_11_14_17_20_46476) True) (Eq (cminus4 i2003_11_14_17_20_46476) True)) % 8.87/9.07 Clause #203 (by superposition #[202, 84]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus9 i2003_11_14_17_20_46476) False))) % 8.95/9.11 Clause #204 (by clausification #[203]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) False)) % 8.95/9.11 Clause #205 (by clausification #[196]): Or (Eq (cminus7 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cminus3 i2003_11_14_17_20_46476) True)) % 8.95/9.11 Clause #206 (by clausification #[28]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus9 a) (cplus3 a)) (cplus4 a)) True % 8.95/9.11 Clause #207 (by clausification #[206]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus9 a) (cplus3 a)) (cplus4 a)) True) % 8.95/9.11 Clause #208 (by clausification #[207]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus9 a) (cplus3 a)) True) (Eq (cplus4 a) True)) % 8.95/9.11 Clause #209 (by clausification #[208]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cplus4 a) True) (Or (Eq (cminus9 a) True) (Eq (cplus3 a) True))) % 8.95/9.11 Clause #210 (by superposition #[209, 47]): Or (Eq (cplus4 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cminus9 i2003_11_14_17_20_46476) True) (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.95/9.11 Clause #211 (by clausification #[210]): Or (Eq (cplus4 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cminus9 i2003_11_14_17_20_46476) True) (Eq (cplus3 i2003_11_14_17_20_46476) True)) % 8.95/9.11 Clause #212 (by superposition #[211, 84]): Or (Eq (cplus4 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus9 i2003_11_14_17_20_46476) False))) % 8.95/9.11 Clause #229 (by clausification #[212]): Or (Eq (cplus4 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) False)) % 8.95/9.11 Clause #241 (by clausification #[15]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus3 a) (cplus5 a)) (cminus8 a)) True % 8.95/9.11 Clause #242 (by clausification #[241]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus3 a) (cplus5 a)) (cminus8 a)) True) % 8.95/9.11 Clause #243 (by clausification #[242]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus3 a) (cplus5 a)) True) (Eq (cminus8 a) True)) % 8.95/9.11 Clause #244 (by clausification #[243]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cminus8 a) True) (Or (Eq (cminus3 a) True) (Eq (cplus5 a) True))) % 8.95/9.11 Clause #245 (by superposition #[244, 47]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Or (Eq (cplus5 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.95/9.11 Clause #246 (by clausification #[245]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Eq (cplus5 i2003_11_14_17_20_46476) True)) % 8.95/9.11 Clause #247 (by superposition #[246, 68]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cminus5 i2003_11_14_17_20_46476) False))) % 8.95/9.11 Clause #248 (by clausification #[247]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Eq (cminus5 i2003_11_14_17_20_46476) False)) % 8.95/9.11 Clause #249 (by superposition #[248, 110]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) % 8.95/9.11 (Or (Eq (cminus8 i2003_11_14_17_20_46476) True) (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Eq False True)))) % 8.95/9.11 Clause #286 (by clausification #[21]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus2 a) (cplus4 a)) (cminus6 a)) True % 8.95/9.11 Clause #287 (by clausification #[286]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus2 a) (cplus4 a)) (cminus6 a)) True) % 8.95/9.11 Clause #288 (by clausification #[287]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus2 a) (cplus4 a)) True) (Eq (cminus6 a) True)) % 8.95/9.11 Clause #289 (by clausification #[288]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cminus6 a) True) (Or (Eq (cminus2 a) True) (Eq (cplus4 a) True))) % 8.95/9.11 Clause #290 (by superposition #[289, 47]): Or (Eq (cminus6 i2003_11_14_17_20_46476) True) % 8.95/9.16 (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Or (Eq (cplus4 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.95/9.16 Clause #302 (by clausification #[290]): Or (Eq (cminus6 i2003_11_14_17_20_46476) True) % 8.95/9.16 (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Eq (cplus4 i2003_11_14_17_20_46476) True)) % 8.95/9.16 Clause #303 (by clausification #[22]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus2 a) (cplus6 a)) (cminus7 a)) True % 8.95/9.16 Clause #304 (by clausification #[303]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus2 a) (cplus6 a)) (cminus7 a)) True) % 8.95/9.16 Clause #305 (by clausification #[304]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus2 a) (cplus6 a)) True) (Eq (cminus7 a) True)) % 8.95/9.16 Clause #306 (by clausification #[305]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cminus7 a) True) (Or (Eq (cminus2 a) True) (Eq (cplus6 a) True))) % 8.95/9.16 Clause #307 (by superposition #[306, 47]): Or (Eq (cminus7 i2003_11_14_17_20_46476) True) % 8.95/9.16 (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.95/9.16 Clause #308 (by clausification #[307]): Or (Eq (cminus7 i2003_11_14_17_20_46476) True) % 8.95/9.16 (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Eq (cplus6 i2003_11_14_17_20_46476) True)) % 8.95/9.16 Clause #309 (by superposition #[308, 78]): Or (Eq (cminus2 i2003_11_14_17_20_46476) True) % 8.95/9.16 (Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus7 i2003_11_14_17_20_46476) False))) % 8.95/9.16 Clause #317 (by clausification #[309]): Or (Eq (cminus2 i2003_11_14_17_20_46476) True) % 8.95/9.16 (Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq (cplus7 i2003_11_14_17_20_46476) False)) % 8.95/9.16 Clause #321 (by clausification #[20]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus3 a) (cplus2 a)) (cplus8 a)) True % 8.95/9.16 Clause #322 (by clausification #[321]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus3 a) (cplus2 a)) (cplus8 a)) True) % 8.95/9.16 Clause #323 (by clausification #[322]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus3 a) (cplus2 a)) True) (Eq (cplus8 a) True)) % 8.95/9.16 Clause #324 (by clausification #[323]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cplus8 a) True) (Or (Eq (cminus3 a) True) (Eq (cplus2 a) True))) % 8.95/9.16 Clause #325 (by superposition #[324, 47]): Or (Eq (cplus8 i2003_11_14_17_20_46476) True) % 8.95/9.16 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Or (Eq (cplus2 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.95/9.16 Clause #326 (by clausification #[325]): Or (Eq (cplus8 i2003_11_14_17_20_46476) True) % 8.95/9.16 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) True)) % 8.95/9.16 Clause #334 (by clausification #[18]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus2 a) (cplus6 a)) (cplus9 a)) True % 8.95/9.16 Clause #335 (by clausification #[334]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus2 a) (cplus6 a)) (cplus9 a)) True) % 8.95/9.16 Clause #336 (by clausification #[335]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus2 a) (cplus6 a)) True) (Eq (cplus9 a) True)) % 8.95/9.16 Clause #337 (by clausification #[336]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cplus9 a) True) (Or (Eq (cminus2 a) True) (Eq (cplus6 a) True))) % 8.95/9.16 Clause #338 (by superposition #[337, 47]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 8.95/9.16 (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq False True))) % 8.95/9.16 Clause #339 (by clausification #[338]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 8.95/9.16 (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Eq (cplus6 i2003_11_14_17_20_46476) True)) % 8.95/9.16 Clause #340 (by superposition #[339, 65]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 8.95/9.16 (Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus2 i2003_11_14_17_20_46476) False))) % 8.95/9.16 Clause #341 (by clausification #[340]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 8.95/9.16 (Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) False)) % 8.95/9.16 Clause #350 (by clausification #[38]): ∀ (a : Iota), Eq (cTest a → Or (Or (cplus3 a) (cplus4 a)) (cplus6 a)) True % 8.95/9.16 Clause #351 (by clausification #[350]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cplus3 a) (cplus4 a)) (cplus6 a)) True) % 9.03/9.21 Clause #352 (by clausification #[351]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cplus3 a) (cplus4 a)) True) (Eq (cplus6 a) True)) % 9.03/9.21 Clause #353 (by clausification #[352]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cplus6 a) True) (Or (Eq (cplus3 a) True) (Eq (cplus4 a) True))) % 9.03/9.21 Clause #354 (by superposition #[353, 47]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) % 9.03/9.21 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Or (Eq (cplus4 i2003_11_14_17_20_46476) True) (Eq False True))) % 9.03/9.21 Clause #361 (by clausification #[354]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) % 9.03/9.21 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq (cplus4 i2003_11_14_17_20_46476) True)) % 9.03/9.21 Clause #362 (by superposition #[361, 81]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) % 9.03/9.21 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cminus4 i2003_11_14_17_20_46476) False))) % 9.03/9.21 Clause #363 (by clausification #[362]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) % 9.03/9.21 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq (cminus4 i2003_11_14_17_20_46476) False)) % 9.03/9.21 Clause #381 (by clausification #[35]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus9 a) (cminus2 a)) (cplus3 a)) True % 9.03/9.21 Clause #382 (by clausification #[381]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus9 a) (cminus2 a)) (cplus3 a)) True) % 9.03/9.21 Clause #383 (by clausification #[382]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus9 a) (cminus2 a)) True) (Eq (cplus3 a) True)) % 9.03/9.21 Clause #384 (by clausification #[383]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cplus3 a) True) (Or (Eq (cminus9 a) True) (Eq (cminus2 a) True))) % 9.03/9.21 Clause #385 (by superposition #[384, 47]): Or (Eq (cplus3 i2003_11_14_17_20_46476) True) % 9.03/9.21 (Or (Eq (cminus9 i2003_11_14_17_20_46476) True) (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Eq False True))) % 9.03/9.21 Clause #386 (by clausification #[385]): Or (Eq (cplus3 i2003_11_14_17_20_46476) True) % 9.03/9.21 (Or (Eq (cminus9 i2003_11_14_17_20_46476) True) (Eq (cminus2 i2003_11_14_17_20_46476) True)) % 9.03/9.21 Clause #387 (by superposition #[386, 84]): Or (Eq (cplus3 i2003_11_14_17_20_46476) True) % 9.03/9.21 (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus9 i2003_11_14_17_20_46476) False))) % 9.03/9.21 Clause #388 (by clausification #[387]): Or (Eq (cplus3 i2003_11_14_17_20_46476) True) % 9.03/9.21 (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) False)) % 9.03/9.21 Clause #389 (by clausification #[34]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus4 a) (cplus9 a)) (cplus7 a)) True % 9.03/9.21 Clause #390 (by clausification #[389]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus4 a) (cplus9 a)) (cplus7 a)) True) % 9.03/9.21 Clause #391 (by clausification #[390]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus4 a) (cplus9 a)) True) (Eq (cplus7 a) True)) % 9.03/9.21 Clause #392 (by clausification #[391]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cplus7 a) True) (Or (Eq (cminus4 a) True) (Eq (cplus9 a) True))) % 9.03/9.21 Clause #393 (by superposition #[392, 47]): Or (Eq (cplus7 i2003_11_14_17_20_46476) True) % 9.03/9.21 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq False True))) % 9.03/9.21 Clause #394 (by clausification #[25]): ∀ (a : Iota), Eq (cTest a → Or (Or (cplus3 a) (cplus4 a)) (cplus9 a)) True % 9.03/9.21 Clause #395 (by clausification #[394]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cplus3 a) (cplus4 a)) (cplus9 a)) True) % 9.03/9.21 Clause #396 (by clausification #[395]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cplus3 a) (cplus4 a)) True) (Eq (cplus9 a) True)) % 9.03/9.21 Clause #397 (by clausification #[396]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cplus9 a) True) (Or (Eq (cplus3 a) True) (Eq (cplus4 a) True))) % 9.03/9.21 Clause #398 (by superposition #[397, 47]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.21 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Or (Eq (cplus4 i2003_11_14_17_20_46476) True) (Eq False True))) % 9.03/9.21 Clause #399 (by clausification #[398]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.21 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq (cplus4 i2003_11_14_17_20_46476) True)) % 9.03/9.24 Clause #400 (by superposition #[399, 81]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cminus4 i2003_11_14_17_20_46476) False))) % 9.03/9.24 Clause #401 (by clausification #[400]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq (cminus4 i2003_11_14_17_20_46476) False)) % 9.03/9.24 Clause #402 (by clausification #[393]): Or (Eq (cplus7 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) True)) % 9.03/9.24 Clause #425 (by clausification #[33]): ∀ (a : Iota), Eq (cTest a → Or (Or (cminus9 a) (cminus2 a)) (cplus7 a)) True % 9.03/9.24 Clause #426 (by clausification #[425]): ∀ (a : Iota), Or (Eq (cTest a) False) (Eq (Or (Or (cminus9 a) (cminus2 a)) (cplus7 a)) True) % 9.03/9.24 Clause #427 (by clausification #[426]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (Or (cminus9 a) (cminus2 a)) True) (Eq (cplus7 a) True)) % 9.03/9.24 Clause #428 (by clausification #[427]): ∀ (a : Iota), Or (Eq (cTest a) False) (Or (Eq (cplus7 a) True) (Or (Eq (cminus9 a) True) (Eq (cminus2 a) True))) % 9.03/9.24 Clause #429 (by superposition #[428, 47]): Or (Eq (cplus7 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus9 i2003_11_14_17_20_46476) True) (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Eq False True))) % 9.03/9.24 Clause #430 (by clausification #[429]): Or (Eq (cplus7 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus9 i2003_11_14_17_20_46476) True) (Eq (cminus2 i2003_11_14_17_20_46476) True)) % 9.03/9.24 Clause #490 (by clausification #[189]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) True))) % 9.03/9.24 Clause #491 (by eliminate duplicate literals #[490]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) True)) % 9.03/9.24 Clause #492 (by superposition #[491, 341]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq True False)))) % 9.03/9.24 Clause #495 (by clausification #[492]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq (cplus6 i2003_11_14_17_20_46476) True))) % 9.03/9.24 Clause #496 (by eliminate duplicate literals #[495]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus6 i2003_11_14_17_20_46476) True)) % 9.03/9.24 Clause #497 (by superposition #[496, 59]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cminus6 i2003_11_14_17_20_46476) False))) % 9.03/9.24 Clause #498 (by clausification #[497]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cminus6 i2003_11_14_17_20_46476) False)) % 9.03/9.24 Clause #502 (by superposition #[498, 180]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq False True) (Or (Eq (cminus7 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) True)))) % 9.03/9.24 Clause #509 (by clausification #[502]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus7 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) True))) % 9.03/9.24 Clause #510 (by eliminate duplicate literals #[509]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cminus7 i2003_11_14_17_20_46476) True)) % 9.03/9.24 Clause #511 (by superposition #[510, 78]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus7 i2003_11_14_17_20_46476) False))) % 9.03/9.24 Clause #512 (by clausification #[511]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.03/9.24 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus7 i2003_11_14_17_20_46476) False)) % 9.11/9.28 Clause #516 (by superposition #[512, 402]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq False True) (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) True)))) % 9.11/9.28 Clause #581 (by clausification #[516]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) True))) % 9.11/9.28 Clause #582 (by eliminate duplicate literals #[581]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 Clause #583 (by superposition #[582, 204]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cminus8 i2003_11_14_17_20_46476) True) (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq True False))) % 9.11/9.28 Clause #585 (by superposition #[582, 388]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Eq True False))) % 9.11/9.28 Clause #586 (by clausification #[585]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq (cminus2 i2003_11_14_17_20_46476) True)) % 9.11/9.28 Clause #587 (by superposition #[586, 65]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus2 i2003_11_14_17_20_46476) False))) % 9.11/9.28 Clause #588 (by clausification #[587]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) False)) % 9.11/9.28 Clause #590 (by clausification #[583]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cminus8 i2003_11_14_17_20_46476) True) (Eq (cminus4 i2003_11_14_17_20_46476) True)) % 9.11/9.28 Clause #591 (by eliminate duplicate literals #[590]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cminus8 i2003_11_14_17_20_46476) True) % 9.11/9.28 Clause #592 (by superposition #[591, 92]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus8 i2003_11_14_17_20_46476) False)) % 9.11/9.28 Clause #594 (by clausification #[592]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus8 i2003_11_14_17_20_46476) False) % 9.11/9.28 Clause #595 (by superposition #[594, 116]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq False True) (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) True))) % 9.11/9.28 Clause #599 (by clausification #[595]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) True)) % 9.11/9.28 Clause #600 (by eliminate duplicate literals #[599]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) True) % 9.11/9.28 Clause #602 (by superposition #[600, 588]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq True False))) % 9.11/9.28 Clause #603 (by clausification #[602]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus3 i2003_11_14_17_20_46476) True)) % 9.11/9.28 Clause #604 (by eliminate duplicate literals #[603]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus3 i2003_11_14_17_20_46476) True) % 9.11/9.28 Clause #605 (by superposition #[604, 75]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cminus3 i2003_11_14_17_20_46476) False)) % 9.11/9.28 Clause #606 (by clausification #[605]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cminus3 i2003_11_14_17_20_46476) False) % 9.11/9.28 Clause #607 (by superposition #[606, 205]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cminus7 i2003_11_14_17_20_46476) True) (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq False True))) % 9.11/9.28 Clause #609 (by clausification #[607]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.11/9.28 (Or (Eq (cminus7 i2003_11_14_17_20_46476) True) (Eq (cminus4 i2003_11_14_17_20_46476) True)) % 9.11/9.28 Clause #610 (by eliminate duplicate literals #[609]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cminus7 i2003_11_14_17_20_46476) True) % 9.13/9.31 Clause #611 (by superposition #[610, 78]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus7 i2003_11_14_17_20_46476) False)) % 9.13/9.31 Clause #612 (by clausification #[249]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) % 9.13/9.31 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) % 9.13/9.31 (Or (Eq (cminus8 i2003_11_14_17_20_46476) True) (Eq (cminus3 i2003_11_14_17_20_46476) True))) % 9.13/9.31 Clause #613 (by eliminate duplicate literals #[612]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) (Eq (cminus3 i2003_11_14_17_20_46476) True) % 9.13/9.31 Clause #616 (by clausification #[611]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus7 i2003_11_14_17_20_46476) False) % 9.13/9.31 Clause #620 (by superposition #[616, 430]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.13/9.31 (Or (Eq False True) (Or (Eq (cminus9 i2003_11_14_17_20_46476) True) (Eq (cminus2 i2003_11_14_17_20_46476) True))) % 9.13/9.31 Clause #624 (by clausification #[620]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.13/9.31 (Or (Eq (cminus9 i2003_11_14_17_20_46476) True) (Eq (cminus2 i2003_11_14_17_20_46476) True)) % 9.13/9.31 Clause #625 (by superposition #[624, 84]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.13/9.31 (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus9 i2003_11_14_17_20_46476) False))) % 9.13/9.31 Clause #626 (by clausification #[625]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.13/9.31 (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) False)) % 9.13/9.31 Clause #627 (by superposition #[626, 582]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.13/9.31 (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Or (Eq False True) (Eq (cminus4 i2003_11_14_17_20_46476) True))) % 9.13/9.31 Clause #629 (by clausification #[627]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.13/9.31 (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Eq (cminus4 i2003_11_14_17_20_46476) True)) % 9.13/9.31 Clause #630 (by eliminate duplicate literals #[629]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cminus2 i2003_11_14_17_20_46476) True) % 9.13/9.31 Clause #631 (by superposition #[630, 65]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus2 i2003_11_14_17_20_46476) False)) % 9.13/9.31 Clause #632 (by clausification #[631]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) False) % 9.13/9.31 Clause #633 (by superposition #[632, 600]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq False True)) % 9.13/9.31 Clause #634 (by clausification #[633]): Or (Eq (cminus4 i2003_11_14_17_20_46476) True) (Eq (cminus4 i2003_11_14_17_20_46476) True) % 9.13/9.31 Clause #635 (by eliminate duplicate literals #[634]): Eq (cminus4 i2003_11_14_17_20_46476) True % 9.13/9.31 Clause #636 (by backward demodulation #[635, 363]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq True False)) % 9.13/9.31 Clause #637 (by backward demodulation #[635, 401]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq True False)) % 9.13/9.31 Clause #659 (by clausification #[637]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq (cplus3 i2003_11_14_17_20_46476) True) % 9.13/9.31 Clause #660 (by superposition #[659, 75]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cminus3 i2003_11_14_17_20_46476) False)) % 9.13/9.31 Clause #661 (by clausification #[660]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq (cminus3 i2003_11_14_17_20_46476) False) % 9.13/9.31 Clause #663 (by superposition #[661, 613]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Or (Eq (cminus8 i2003_11_14_17_20_46476) True) (Eq False True)) % 9.13/9.31 Clause #665 (by clausification #[663]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq (cminus8 i2003_11_14_17_20_46476) True) % 9.13/9.31 Clause #666 (by superposition #[665, 92]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus8 i2003_11_14_17_20_46476) False)) % 9.13/9.31 Clause #667 (by clausification #[666]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq (cplus8 i2003_11_14_17_20_46476) False) % 9.13/9.31 Clause #671 (by clausification #[636]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq (cplus3 i2003_11_14_17_20_46476) True) % 9.16/9.35 Clause #672 (by superposition #[671, 75]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cminus3 i2003_11_14_17_20_46476) False)) % 9.16/9.35 Clause #673 (by clausification #[672]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq (cminus3 i2003_11_14_17_20_46476) False) % 9.16/9.35 Clause #675 (by superposition #[673, 613]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Or (Eq (cminus8 i2003_11_14_17_20_46476) True) (Eq False True)) % 9.16/9.35 Clause #676 (by clausification #[675]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq (cminus8 i2003_11_14_17_20_46476) True) % 9.16/9.35 Clause #677 (by superposition #[676, 92]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus8 i2003_11_14_17_20_46476) False)) % 9.16/9.35 Clause #679 (by clausification #[677]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq (cplus8 i2003_11_14_17_20_46476) False) % 9.16/9.35 Clause #681 (by superposition #[679, 326]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) % 9.16/9.35 (Or (Eq False True) (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) True))) % 9.16/9.35 Clause #700 (by clausification #[681]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) % 9.16/9.35 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) True)) % 9.16/9.35 Clause #702 (by superposition #[700, 673]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) % 9.16/9.35 (Or (Eq (cplus2 i2003_11_14_17_20_46476) True) (Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq True False))) % 9.16/9.35 Clause #704 (by clausification #[702]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) % 9.16/9.35 (Or (Eq (cplus2 i2003_11_14_17_20_46476) True) (Eq (cplus6 i2003_11_14_17_20_46476) True)) % 9.16/9.35 Clause #705 (by eliminate duplicate literals #[704]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) True) % 9.16/9.35 Clause #706 (by superposition #[705, 341]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) % 9.16/9.35 (Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq True False))) % 9.16/9.35 Clause #710 (by clausification #[706]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) % 9.16/9.35 (Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq (cplus6 i2003_11_14_17_20_46476) True)) % 9.16/9.35 Clause #711 (by eliminate duplicate literals #[710]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.16/9.35 Clause #712 (by superposition #[711, 59]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cminus6 i2003_11_14_17_20_46476) False)) % 9.16/9.35 Clause #713 (by clausification #[712]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq (cminus6 i2003_11_14_17_20_46476) False) % 9.16/9.35 Clause #716 (by superposition #[713, 180]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.16/9.35 (Or (Eq False True) (Or (Eq (cminus7 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) True))) % 9.16/9.35 Clause #725 (by clausification #[716]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.16/9.35 (Or (Eq (cminus7 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) True)) % 9.16/9.35 Clause #726 (by eliminate duplicate literals #[725]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq (cminus7 i2003_11_14_17_20_46476) True) % 9.16/9.35 Clause #727 (by superposition #[726, 78]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus7 i2003_11_14_17_20_46476) False)) % 9.16/9.35 Clause #728 (by clausification #[727]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq (cplus7 i2003_11_14_17_20_46476) False) % 9.16/9.35 Clause #730 (by superposition #[728, 127]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.16/9.35 (Or (Eq (cplus8 i2003_11_14_17_20_46476) True) (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Eq False True))) % 9.16/9.35 Clause #743 (by clausification #[730]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.16/9.35 (Or (Eq (cplus8 i2003_11_14_17_20_46476) True) (Eq (cminus3 i2003_11_14_17_20_46476) True)) % 9.16/9.35 Clause #745 (by superposition #[743, 667]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.16/9.35 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq True False))) % 9.16/9.35 Clause #750 (by clausification #[745]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.16/9.35 (Or (Eq (cminus3 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) True)) % 9.16/9.38 Clause #751 (by eliminate duplicate literals #[750]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq (cminus3 i2003_11_14_17_20_46476) True) % 9.16/9.38 Clause #752 (by superposition #[751, 661]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq True False)) % 9.16/9.38 Clause #755 (by clausification #[752]): Or (Eq (cplus9 i2003_11_14_17_20_46476) True) (Eq (cplus9 i2003_11_14_17_20_46476) True) % 9.16/9.38 Clause #756 (by eliminate duplicate literals #[755]): Eq (cplus9 i2003_11_14_17_20_46476) True % 9.16/9.38 Clause #757 (by backward demodulation #[756, 229]): Or (Eq (cplus4 i2003_11_14_17_20_46476) True) (Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq True False)) % 9.16/9.38 Clause #775 (by clausification #[757]): Or (Eq (cplus4 i2003_11_14_17_20_46476) True) (Eq (cplus3 i2003_11_14_17_20_46476) True) % 9.16/9.38 Clause #776 (by superposition #[775, 81]): Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cminus4 i2003_11_14_17_20_46476) False)) % 9.16/9.38 Clause #777 (by clausification #[776]): Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq (cminus4 i2003_11_14_17_20_46476) False) % 9.16/9.38 Clause #778 (by forward demodulation #[777, 635]): Or (Eq (cplus3 i2003_11_14_17_20_46476) True) (Eq True False) % 9.16/9.38 Clause #779 (by clausification #[778]): Eq (cplus3 i2003_11_14_17_20_46476) True % 9.16/9.38 Clause #783 (by superposition #[779, 75]): Or (Eq True False) (Eq (cminus3 i2003_11_14_17_20_46476) False) % 9.16/9.38 Clause #784 (by clausification #[783]): Eq (cminus3 i2003_11_14_17_20_46476) False % 9.16/9.38 Clause #785 (by backward demodulation #[784, 127]): Or (Eq (cplus8 i2003_11_14_17_20_46476) True) (Or (Eq False True) (Eq (cplus7 i2003_11_14_17_20_46476) True)) % 9.16/9.38 Clause #786 (by backward demodulation #[784, 326]): Or (Eq (cplus8 i2003_11_14_17_20_46476) True) (Or (Eq False True) (Eq (cplus2 i2003_11_14_17_20_46476) True)) % 9.16/9.38 Clause #789 (by superposition #[784, 613]): Or (Eq (cminus8 i2003_11_14_17_20_46476) True) (Eq False True) % 9.16/9.38 Clause #790 (by clausification #[789]): Eq (cminus8 i2003_11_14_17_20_46476) True % 9.16/9.38 Clause #791 (by superposition #[790, 92]): Or (Eq True False) (Eq (cplus8 i2003_11_14_17_20_46476) False) % 9.16/9.38 Clause #794 (by clausification #[791]): Eq (cplus8 i2003_11_14_17_20_46476) False % 9.16/9.38 Clause #797 (by clausification #[786]): Or (Eq (cplus8 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) True) % 9.16/9.38 Clause #798 (by superposition #[797, 794]): Or (Eq (cplus2 i2003_11_14_17_20_46476) True) (Eq True False) % 9.16/9.38 Clause #799 (by clausification #[798]): Eq (cplus2 i2003_11_14_17_20_46476) True % 9.16/9.38 Clause #806 (by clausification #[785]): Or (Eq (cplus8 i2003_11_14_17_20_46476) True) (Eq (cplus7 i2003_11_14_17_20_46476) True) % 9.16/9.38 Clause #807 (by forward demodulation #[806, 794]): Or (Eq False True) (Eq (cplus7 i2003_11_14_17_20_46476) True) % 9.16/9.38 Clause #808 (by clausification #[807]): Eq (cplus7 i2003_11_14_17_20_46476) True % 9.16/9.38 Clause #809 (by superposition #[808, 317]): Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq True False)) % 9.16/9.38 Clause #810 (by clausification #[809]): Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Eq (cplus6 i2003_11_14_17_20_46476) True) % 9.16/9.38 Clause #811 (by superposition #[810, 65]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus2 i2003_11_14_17_20_46476) False)) % 9.16/9.38 Clause #812 (by clausification #[811]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) False) % 9.16/9.38 Clause #813 (by superposition #[812, 799]): Or (Eq (cplus6 i2003_11_14_17_20_46476) True) (Eq False True) % 9.16/9.38 Clause #814 (by clausification #[813]): Eq (cplus6 i2003_11_14_17_20_46476) True % 9.16/9.38 Clause #817 (by superposition #[814, 59]): Or (Eq True False) (Eq (cminus6 i2003_11_14_17_20_46476) False) % 9.16/9.38 Clause #820 (by clausification #[817]): Eq (cminus6 i2003_11_14_17_20_46476) False % 9.16/9.38 Clause #822 (by superposition #[820, 302]): Or (Eq False True) (Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Eq (cplus4 i2003_11_14_17_20_46476) True)) % 9.16/9.38 Clause #836 (by clausification #[822]): Or (Eq (cminus2 i2003_11_14_17_20_46476) True) (Eq (cplus4 i2003_11_14_17_20_46476) True) % 9.16/9.39 Clause #837 (by superposition #[836, 65]): Or (Eq (cplus4 i2003_11_14_17_20_46476) True) (Or (Eq True False) (Eq (cplus2 i2003_11_14_17_20_46476) False)) % 9.16/9.39 Clause #840 (by clausification #[837]): Or (Eq (cplus4 i2003_11_14_17_20_46476) True) (Eq (cplus2 i2003_11_14_17_20_46476) False) % 9.16/9.39 Clause #841 (by superposition #[840, 799]): Or (Eq (cplus4 i2003_11_14_17_20_46476) True) (Eq False True) % 9.16/9.39 Clause #842 (by clausification #[841]): Eq (cplus4 i2003_11_14_17_20_46476) True % 9.16/9.39 Clause #843 (by superposition #[842, 81]): Or (Eq True False) (Eq (cminus4 i2003_11_14_17_20_46476) False) % 9.16/9.39 Clause #844 (by clausification #[843]): Eq (cminus4 i2003_11_14_17_20_46476) False % 9.16/9.39 Clause #845 (by superposition #[844, 635]): Eq False True % 9.16/9.39 Clause #846 (by clausification #[845]): False % 9.16/9.39 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------