%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM003+2 : TPTP v9.2.0. Bugfixed v2.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.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:45:46 PM UTC 2025 % Result : Theorem 33.73s 33.95s % Output : Proof 33.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : COM003+2 : TPTP v9.2.0. Bugfixed v2.2.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n012.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 : Thu Oct 2 15:55:23 EDT 2025 % 0.13/0.35 % CPUTime : % 33.73/33.95 SZS status Theorem for theBenchmark.p % 33.73/33.95 SZS output start Proof for theBenchmark.p % 33.73/33.95 Clause #1 (by assumption #[]): Eq (∀ (X : Iota), Iff (program_program_decides X) (And (program X) (program_decides X))) True % 33.73/33.95 Clause #3 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (program_halts2 X Y) (And (program X) (halts2 X Y))) True % 33.73/33.95 Clause #5 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (program_not_halts2 X Y) (And (program X) (Not (halts2 X Y)))) True % 33.73/33.95 Clause #6 (by assumption #[]): Eq (∀ (X Y W : Iota), Iff (halts2_outputs X Y W) (And (halts2 X Y) (outputs X W))) True % 33.73/33.95 Clause #10 (by assumption #[]): Eq (∀ (X Y W : Iota), Iff (program_not_halts2_halts2_outputs X Y W) (program_not_halts2 Y Y → halts2_outputs X Y W)) % 33.73/33.95 True % 33.73/33.95 Clause #11 (by assumption #[]): Eq ((Exists fun X => algorithm_program_decides X) → Exists fun W => program_program_decides W) True % 33.73/33.95 Clause #12 (by assumption #[]): Eq % 33.73/33.95 (∀ (W : Iota), % 33.73/33.95 program_program_decides W → % 33.73/33.95 ∀ (Y Z : Iota), And (program_halts2_halts3_outputs W Y Z good) (program_not_halts2_halts3_outputs W Y Z bad)) % 33.73/33.95 True % 33.73/33.95 Clause #13 (by assumption #[]): Eq % 33.73/33.95 ((Exists fun W => % 33.73/33.95 And (program W) % 33.73/33.95 (∀ (Y : Iota), And (program_halts2_halts3_outputs W Y Y good) (program_not_halts2_halts3_outputs W Y Y bad))) → % 33.73/33.95 Exists fun V => % 33.73/33.95 And (program V) % 33.73/33.95 (∀ (Y : Iota), And (program_halts2_halts2_outputs V Y good) (program_not_halts2_halts2_outputs V Y bad))) % 33.73/33.95 True % 33.73/33.95 Clause #14 (by assumption #[]): Eq % 33.73/33.95 ((Exists fun V => % 33.73/33.95 And (program V) % 33.73/33.95 (∀ (Y : Iota), And (program_halts2_halts2_outputs V Y good) (program_not_halts2_halts2_outputs V Y bad))) → % 33.73/33.95 Exists fun U => % 33.73/33.95 And (program U) % 33.73/33.95 (∀ (Y : Iota), And (program_halts2 Y Y → Not (halts2 U Y)) (program_not_halts2_halts2_outputs U Y good))) % 33.73/33.95 True % 33.73/33.95 Clause #15 (by assumption #[]): Eq (Not (Not (Exists fun X => algorithm_program_decides X))) True % 33.73/33.95 Clause #16 (by betaEtaReduce #[11]): Eq (Exists algorithm_program_decides → Exists program_program_decides) True % 33.73/33.95 Clause #17 (by clausification #[16]): Or (Eq (Exists algorithm_program_decides) False) (Eq (Exists program_program_decides) True) % 33.73/33.95 Clause #18 (by clausification #[17]): ∀ (a : Iota), Or (Eq (Exists program_program_decides) True) (Eq (algorithm_program_decides a) False) % 33.73/33.95 Clause #19 (by clausification #[18]): ∀ (a a_1 : Iota), Or (Eq (algorithm_program_decides a) False) (Eq (program_program_decides (skS.0 0 a_1)) True) % 33.73/33.95 Clause #20 (by betaEtaReduce #[15]): Eq (Not (Not (Exists algorithm_program_decides))) True % 33.73/33.95 Clause #21 (by clausification #[20]): Eq (Not (Exists algorithm_program_decides)) False % 33.73/33.95 Clause #22 (by clausification #[21]): Eq (Exists algorithm_program_decides) True % 33.73/33.95 Clause #23 (by clausification #[22]): ∀ (a : Iota), Eq (algorithm_program_decides (skS.0 1 a)) True % 33.73/33.95 Clause #24 (by superposition #[23, 19]): ∀ (a : Iota), Or (Eq True False) (Eq (program_program_decides (skS.0 0 a)) True) % 33.73/33.95 Clause #25 (by clausification #[24]): ∀ (a : Iota), Eq (program_program_decides (skS.0 0 a)) True % 33.73/33.95 Clause #43 (by clausification #[1]): ∀ (a : Iota), Eq (Iff (program_program_decides a) (And (program a) (program_decides a))) True % 33.73/33.95 Clause #45 (by clausification #[43]): ∀ (a : Iota), Or (Eq (program_program_decides a) False) (Eq (And (program a) (program_decides a)) True) % 33.73/33.95 Clause #49 (by clausification #[45]): ∀ (a : Iota), Or (Eq (program_program_decides a) False) (Eq (program a) True) % 33.73/33.95 Clause #51 (by superposition #[49, 25]): ∀ (a : Iota), Or (Eq (program (skS.0 0 a)) True) (Eq False True) % 33.73/33.95 Clause #52 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (program_halts2 a Y) (And (program a) (halts2 a Y))) True % 33.73/33.95 Clause #53 (by clausification #[52]): ∀ (a a_1 : Iota), Eq (Iff (program_halts2 a a_1) (And (program a) (halts2 a a_1))) True % 33.73/33.95 Clause #54 (by clausification #[53]): ∀ (a a_1 : Iota), Or (Eq (program_halts2 a a_1) True) (Eq (And (program a) (halts2 a a_1)) False) % 33.73/33.95 Clause #56 (by clausification #[54]): ∀ (a a_1 : Iota), Or (Eq (program_halts2 a a_1) True) (Or (Eq (program a) False) (Eq (halts2 a a_1) False)) % 33.73/33.95 Clause #58 (by clausification #[51]): ∀ (a : Iota), Eq (program (skS.0 0 a)) True % 33.73/33.97 Clause #77 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (program_not_halts2 a Y) (And (program a) (Not (halts2 a Y)))) True % 33.73/33.97 Clause #78 (by clausification #[77]): ∀ (a a_1 : Iota), Eq (Iff (program_not_halts2 a a_1) (And (program a) (Not (halts2 a a_1)))) True % 33.73/33.97 Clause #79 (by clausification #[78]): ∀ (a a_1 : Iota), Or (Eq (program_not_halts2 a a_1) True) (Eq (And (program a) (Not (halts2 a a_1))) False) % 33.73/33.97 Clause #80 (by clausification #[78]): ∀ (a a_1 : Iota), Or (Eq (program_not_halts2 a a_1) False) (Eq (And (program a) (Not (halts2 a a_1))) True) % 33.73/33.97 Clause #81 (by clausification #[79]): ∀ (a a_1 : Iota), Or (Eq (program_not_halts2 a a_1) True) (Or (Eq (program a) False) (Eq (Not (halts2 a a_1)) False)) % 33.73/33.97 Clause #82 (by clausification #[81]): ∀ (a a_1 : Iota), Or (Eq (program_not_halts2 a a_1) True) (Or (Eq (program a) False) (Eq (halts2 a a_1) True)) % 33.73/33.97 Clause #85 (by clausification #[80]): ∀ (a a_1 : Iota), Or (Eq (program_not_halts2 a a_1) False) (Eq (Not (halts2 a a_1)) True) % 33.73/33.97 Clause #87 (by clausification #[85]): ∀ (a a_1 : Iota), Or (Eq (program_not_halts2 a a_1) False) (Eq (halts2 a a_1) False) % 33.73/33.97 Clause #97 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (Y W : Iota), Iff (halts2_outputs a Y W) (And (halts2 a Y) (outputs a W))) True % 33.73/33.97 Clause #98 (by clausification #[97]): ∀ (a a_1 : Iota), Eq (∀ (W : Iota), Iff (halts2_outputs a a_1 W) (And (halts2 a a_1) (outputs a W))) True % 33.73/33.97 Clause #99 (by clausification #[98]): ∀ (a a_1 a_2 : Iota), Eq (Iff (halts2_outputs a a_1 a_2) (And (halts2 a a_1) (outputs a a_2))) True % 33.73/33.97 Clause #101 (by clausification #[99]): ∀ (a a_1 a_2 : Iota), Or (Eq (halts2_outputs a a_1 a_2) False) (Eq (And (halts2 a a_1) (outputs a a_2)) True) % 33.73/33.97 Clause #111 (by clausification #[101]): ∀ (a a_1 a_2 : Iota), Or (Eq (halts2_outputs a a_1 a_2) False) (Eq (halts2 a a_1) True) % 33.73/33.97 Clause #123 (by clausification #[10]): ∀ (a : Iota), % 33.73/33.97 Eq (∀ (Y W : Iota), Iff (program_not_halts2_halts2_outputs a Y W) (program_not_halts2 Y Y → halts2_outputs a Y W)) % 33.73/33.97 True % 33.73/33.97 Clause #124 (by clausification #[123]): ∀ (a a_1 : Iota), % 33.73/33.97 Eq % 33.73/33.97 (∀ (W : Iota), % 33.73/33.97 Iff (program_not_halts2_halts2_outputs a a_1 W) (program_not_halts2 a_1 a_1 → halts2_outputs a a_1 W)) % 33.73/33.97 True % 33.73/33.97 Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 : Iota), % 33.73/33.97 Eq (Iff (program_not_halts2_halts2_outputs a a_1 a_2) (program_not_halts2 a_1 a_1 → halts2_outputs a a_1 a_2)) True % 33.73/33.97 Clause #126 (by clausification #[125]): ∀ (a a_1 a_2 : Iota), % 33.73/33.97 Or (Eq (program_not_halts2_halts2_outputs a a_1 a_2) True) % 33.73/33.97 (Eq (program_not_halts2 a_1 a_1 → halts2_outputs a a_1 a_2) False) % 33.73/33.97 Clause #127 (by clausification #[125]): ∀ (a a_1 a_2 : Iota), % 33.73/33.97 Or (Eq (program_not_halts2_halts2_outputs a a_1 a_2) False) % 33.73/33.97 (Eq (program_not_halts2 a_1 a_1 → halts2_outputs a a_1 a_2) True) % 33.73/33.97 Clause #128 (by clausification #[126]): ∀ (a a_1 a_2 : Iota), Or (Eq (program_not_halts2_halts2_outputs a a_1 a_2) True) (Eq (program_not_halts2 a_1 a_1) True) % 33.73/33.97 Clause #130 (by superposition #[128, 87]): ∀ (a a_1 a_2 : Iota), % 33.73/33.97 Or (Eq (program_not_halts2_halts2_outputs a a_1 a_2) True) (Or (Eq True False) (Eq (halts2 a_1 a_1) False)) % 33.73/33.97 Clause #141 (by clausification #[130]): ∀ (a a_1 a_2 : Iota), Or (Eq (program_not_halts2_halts2_outputs a a_1 a_2) True) (Eq (halts2 a_1 a_1) False) % 33.73/33.97 Clause #143 (by clausification #[127]): ∀ (a a_1 a_2 : Iota), % 33.73/33.97 Or (Eq (program_not_halts2_halts2_outputs a a_1 a_2) False) % 33.73/33.97 (Or (Eq (program_not_halts2 a_1 a_1) False) (Eq (halts2_outputs a a_1 a_2) True)) % 33.73/33.97 Clause #149 (by clausification #[12]): ∀ (a : Iota), % 33.73/33.97 Eq % 33.73/33.97 (program_program_decides a → % 33.73/33.97 ∀ (Y Z : Iota), And (program_halts2_halts3_outputs a Y Z good) (program_not_halts2_halts3_outputs a Y Z bad)) % 33.73/33.97 True % 33.73/33.97 Clause #150 (by clausification #[149]): ∀ (a : Iota), % 33.73/33.97 Or (Eq (program_program_decides a) False) % 33.73/33.97 (Eq (∀ (Y Z : Iota), And (program_halts2_halts3_outputs a Y Z good) (program_not_halts2_halts3_outputs a Y Z bad)) % 33.73/33.97 True) % 33.73/33.97 Clause #151 (by clausification #[150]): ∀ (a a_1 : Iota), % 33.82/33.98 Or (Eq (program_program_decides a) False) % 33.82/33.98 (Eq (∀ (Z : Iota), And (program_halts2_halts3_outputs a a_1 Z good) (program_not_halts2_halts3_outputs a a_1 Z bad)) % 33.82/33.98 True) % 33.82/33.98 Clause #152 (by clausification #[151]): ∀ (a a_1 a_2 : Iota), % 33.82/33.98 Or (Eq (program_program_decides a) False) % 33.82/33.98 (Eq (And (program_halts2_halts3_outputs a a_1 a_2 good) (program_not_halts2_halts3_outputs a a_1 a_2 bad)) True) % 33.82/33.98 Clause #153 (by clausification #[152]): ∀ (a a_1 a_2 : Iota), % 33.82/33.98 Or (Eq (program_program_decides a) False) (Eq (program_not_halts2_halts3_outputs a a_1 a_2 bad) True) % 33.82/33.98 Clause #154 (by clausification #[152]): ∀ (a a_1 a_2 : Iota), Or (Eq (program_program_decides a) False) (Eq (program_halts2_halts3_outputs a a_1 a_2 good) True) % 33.82/33.98 Clause #155 (by superposition #[153, 25]): ∀ (a a_1 a_2 : Iota), Or (Eq (program_not_halts2_halts3_outputs (skS.0 0 a) a_1 a_2 bad) True) (Eq False True) % 33.82/33.98 Clause #156 (by superposition #[154, 25]): ∀ (a a_1 a_2 : Iota), Or (Eq (program_halts2_halts3_outputs (skS.0 0 a) a_1 a_2 good) True) (Eq False True) % 33.82/33.98 Clause #159 (by clausification #[155]): ∀ (a a_1 a_2 : Iota), Eq (program_not_halts2_halts3_outputs (skS.0 0 a) a_1 a_2 bad) True % 33.82/33.98 Clause #161 (by clausification #[156]): ∀ (a a_1 a_2 : Iota), Eq (program_halts2_halts3_outputs (skS.0 0 a) a_1 a_2 good) True % 33.82/33.98 Clause #163 (by clausification #[13]): Or % 33.82/33.98 (Eq % 33.82/33.98 (Exists fun W => % 33.82/33.98 And (program W) % 33.82/33.98 (∀ (Y : Iota), And (program_halts2_halts3_outputs W Y Y good) (program_not_halts2_halts3_outputs W Y Y bad))) % 33.82/33.98 False) % 33.82/33.98 (Eq % 33.82/33.98 (Exists fun V => % 33.82/33.98 And (program V) % 33.82/33.98 (∀ (Y : Iota), And (program_halts2_halts2_outputs V Y good) (program_not_halts2_halts2_outputs V Y bad))) % 33.82/33.98 True) % 33.82/33.98 Clause #164 (by clausification #[163]): ∀ (a : Iota), % 33.82/33.98 Or % 33.82/33.98 (Eq % 33.82/33.98 (Exists fun V => % 33.82/33.98 And (program V) % 33.82/33.98 (∀ (Y : Iota), And (program_halts2_halts2_outputs V Y good) (program_not_halts2_halts2_outputs V Y bad))) % 33.82/33.98 True) % 33.82/33.98 (Eq % 33.82/33.98 (And (program a) % 33.82/33.98 (∀ (Y : Iota), And (program_halts2_halts3_outputs a Y Y good) (program_not_halts2_halts3_outputs a Y Y bad))) % 33.82/33.98 False) % 33.82/33.98 Clause #165 (by clausification #[164]): ∀ (a a_1 : Iota), % 33.82/33.98 Or % 33.82/33.98 (Eq % 33.82/33.98 (And (program a) % 33.82/33.98 (∀ (Y : Iota), And (program_halts2_halts3_outputs a Y Y good) (program_not_halts2_halts3_outputs a Y Y bad))) % 33.82/33.98 False) % 33.82/33.98 (Eq % 33.82/33.98 (And (program (skS.0 3 a_1)) % 33.82/33.98 (∀ (Y : Iota), % 33.82/33.98 And (program_halts2_halts2_outputs (skS.0 3 a_1) Y good) % 33.82/33.98 (program_not_halts2_halts2_outputs (skS.0 3 a_1) Y bad))) % 33.82/33.98 True) % 33.82/33.98 Clause #166 (by clausification #[165]): ∀ (a a_1 : Iota), % 33.82/33.98 Or % 33.82/33.98 (Eq % 33.82/33.98 (And (program (skS.0 3 a)) % 33.82/33.98 (∀ (Y : Iota), % 33.82/33.98 And (program_halts2_halts2_outputs (skS.0 3 a) Y good) (program_not_halts2_halts2_outputs (skS.0 3 a) Y bad))) % 33.82/33.98 True) % 33.82/33.98 (Or (Eq (program a_1) False) % 33.82/33.98 (Eq % 33.82/33.98 (∀ (Y : Iota), And (program_halts2_halts3_outputs a_1 Y Y good) (program_not_halts2_halts3_outputs a_1 Y Y bad)) % 33.82/33.98 False)) % 33.82/33.98 Clause #167 (by clausification #[166]): ∀ (a a_1 : Iota), % 33.82/33.98 Or (Eq (program a) False) % 33.82/33.98 (Or % 33.82/33.98 (Eq (∀ (Y : Iota), And (program_halts2_halts3_outputs a Y Y good) (program_not_halts2_halts3_outputs a Y Y bad)) % 33.82/33.98 False) % 33.82/33.98 (Eq % 33.82/33.98 (∀ (Y : Iota), % 33.82/33.98 And (program_halts2_halts2_outputs (skS.0 3 a_1) Y good) % 33.82/33.98 (program_not_halts2_halts2_outputs (skS.0 3 a_1) Y bad)) % 33.82/33.98 True)) % 33.82/33.98 Clause #168 (by clausification #[166]): ∀ (a a_1 : Iota), % 33.82/33.98 Or (Eq (program a) False) % 33.82/33.98 (Or % 33.82/33.98 (Eq (∀ (Y : Iota), And (program_halts2_halts3_outputs a Y Y good) (program_not_halts2_halts3_outputs a Y Y bad)) % 33.82/33.98 False) % 33.82/33.98 (Eq (program (skS.0 3 a_1)) True)) % 33.82/33.98 Clause #169 (by clausification #[167]): ∀ (a a_1 a_2 : Iota), % 33.82/33.98 Or (Eq (program a) False) % 33.82/33.98 (Or % 33.82/33.98 (Eq % 33.82/33.98 (∀ (Y : Iota), % 33.82/33.98 And (program_halts2_halts2_outputs (skS.0 3 a_1) Y good) % 33.82/33.98 (program_not_halts2_halts2_outputs (skS.0 3 a_1) Y bad)) % 33.82/33.98 True) % 33.82/33.98 (Eq % 33.82/33.98 (Not % 33.82/33.98 (And (program_halts2_halts3_outputs a (skS.0 4 a a_2) (skS.0 4 a a_2) good) % 33.83/34.00 (program_not_halts2_halts3_outputs a (skS.0 4 a a_2) (skS.0 4 a a_2) bad))) % 33.83/34.00 True)) % 33.83/34.00 Clause #170 (by clausification #[169]): ∀ (a a_1 a_2 a_3 : Iota), % 33.83/34.00 Or (Eq (program a) False) % 33.83/34.00 (Or % 33.83/34.00 (Eq % 33.83/34.00 (Not % 33.83/34.00 (And (program_halts2_halts3_outputs a (skS.0 4 a a_1) (skS.0 4 a a_1) good) % 33.83/34.00 (program_not_halts2_halts3_outputs a (skS.0 4 a a_1) (skS.0 4 a a_1) bad))) % 33.83/34.00 True) % 33.83/34.00 (Eq % 33.83/34.00 (And (program_halts2_halts2_outputs (skS.0 3 a_2) a_3 good) % 33.83/34.00 (program_not_halts2_halts2_outputs (skS.0 3 a_2) a_3 bad)) % 33.83/34.00 True)) % 33.83/34.00 Clause #171 (by clausification #[170]): ∀ (a a_1 a_2 a_3 : Iota), % 33.83/34.00 Or (Eq (program a) False) % 33.83/34.00 (Or % 33.83/34.00 (Eq % 33.83/34.00 (And (program_halts2_halts2_outputs (skS.0 3 a_1) a_2 good) % 33.83/34.00 (program_not_halts2_halts2_outputs (skS.0 3 a_1) a_2 bad)) % 33.83/34.00 True) % 33.83/34.00 (Eq % 33.83/34.00 (And (program_halts2_halts3_outputs a (skS.0 4 a a_3) (skS.0 4 a a_3) good) % 33.83/34.00 (program_not_halts2_halts3_outputs a (skS.0 4 a a_3) (skS.0 4 a a_3) bad)) % 33.83/34.00 False)) % 33.83/34.00 Clause #172 (by clausification #[171]): ∀ (a a_1 a_2 a_3 : Iota), % 33.83/34.00 Or (Eq (program a) False) % 33.83/34.00 (Or % 33.83/34.00 (Eq % 33.83/34.00 (And (program_halts2_halts3_outputs a (skS.0 4 a a_1) (skS.0 4 a a_1) good) % 33.83/34.00 (program_not_halts2_halts3_outputs a (skS.0 4 a a_1) (skS.0 4 a a_1) bad)) % 33.83/34.00 False) % 33.83/34.00 (Eq (program_not_halts2_halts2_outputs (skS.0 3 a_2) a_3 bad) True)) % 33.83/34.00 Clause #173 (by clausification #[171]): ∀ (a a_1 a_2 a_3 : Iota), % 33.83/34.00 Or (Eq (program a) False) % 33.83/34.00 (Or % 33.83/34.00 (Eq % 33.83/34.00 (And (program_halts2_halts3_outputs a (skS.0 4 a a_1) (skS.0 4 a a_1) good) % 33.83/34.00 (program_not_halts2_halts3_outputs a (skS.0 4 a a_1) (skS.0 4 a a_1) bad)) % 33.83/34.00 False) % 33.83/34.00 (Eq (program_halts2_halts2_outputs (skS.0 3 a_2) a_3 good) True)) % 33.83/34.00 Clause #174 (by clausification #[172]): ∀ (a a_1 a_2 a_3 : Iota), % 33.83/34.00 Or (Eq (program a) False) % 33.83/34.00 (Or (Eq (program_not_halts2_halts2_outputs (skS.0 3 a_1) a_2 bad) True) % 33.83/34.00 (Or (Eq (program_halts2_halts3_outputs a (skS.0 4 a a_3) (skS.0 4 a a_3) good) False) % 33.83/34.00 (Eq (program_not_halts2_halts3_outputs a (skS.0 4 a a_3) (skS.0 4 a a_3) bad) False))) % 33.83/34.00 Clause #176 (by superposition #[174, 58]): ∀ (a a_1 a_2 a_3 : Iota), % 33.83/34.00 Or (Eq (program_not_halts2_halts2_outputs (skS.0 3 a) a_1 bad) True) % 33.83/34.00 (Or % 33.83/34.00 (Eq (program_halts2_halts3_outputs (skS.0 0 a_2) (skS.0 4 (skS.0 0 a_2) a_3) (skS.0 4 (skS.0 0 a_2) a_3) good) % 33.83/34.00 False) % 33.83/34.00 (Or % 33.83/34.00 (Eq % 33.83/34.00 (program_not_halts2_halts3_outputs (skS.0 0 a_2) (skS.0 4 (skS.0 0 a_2) a_3) (skS.0 4 (skS.0 0 a_2) a_3) bad) % 33.83/34.00 False) % 33.83/34.00 (Eq False True))) % 33.83/34.00 Clause #186 (by clausification #[14]): Or % 33.83/34.00 (Eq % 33.83/34.00 (Exists fun V => % 33.83/34.00 And (program V) % 33.83/34.00 (∀ (Y : Iota), And (program_halts2_halts2_outputs V Y good) (program_not_halts2_halts2_outputs V Y bad))) % 33.83/34.00 False) % 33.83/34.00 (Eq % 33.83/34.00 (Exists fun U => % 33.83/34.00 And (program U) % 33.83/34.00 (∀ (Y : Iota), And (program_halts2 Y Y → Not (halts2 U Y)) (program_not_halts2_halts2_outputs U Y good))) % 33.83/34.00 True) % 33.83/34.00 Clause #187 (by clausification #[186]): ∀ (a : Iota), % 33.83/34.00 Or % 33.83/34.00 (Eq % 33.83/34.00 (Exists fun U => % 33.83/34.00 And (program U) % 33.83/34.00 (∀ (Y : Iota), And (program_halts2 Y Y → Not (halts2 U Y)) (program_not_halts2_halts2_outputs U Y good))) % 33.83/34.00 True) % 33.83/34.00 (Eq % 33.83/34.00 (And (program a) % 33.83/34.00 (∀ (Y : Iota), And (program_halts2_halts2_outputs a Y good) (program_not_halts2_halts2_outputs a Y bad))) % 33.83/34.00 False) % 33.83/34.00 Clause #188 (by clausification #[187]): ∀ (a a_1 : Iota), % 33.83/34.00 Or % 33.83/34.00 (Eq % 33.83/34.00 (And (program a) % 33.83/34.00 (∀ (Y : Iota), And (program_halts2_halts2_outputs a Y good) (program_not_halts2_halts2_outputs a Y bad))) % 33.83/34.00 False) % 33.83/34.00 (Eq % 33.83/34.00 (And (program (skS.0 5 a_1)) % 33.83/34.00 (∀ (Y : Iota), % 33.83/34.00 And (program_halts2 Y Y → Not (halts2 (skS.0 5 a_1) Y)) % 33.83/34.00 (program_not_halts2_halts2_outputs (skS.0 5 a_1) Y good))) % 33.83/34.00 True) % 33.83/34.00 Clause #189 (by clausification #[188]): ∀ (a a_1 : Iota), % 33.83/34.00 Or % 33.83/34.00 (Eq % 33.83/34.00 (And (program (skS.0 5 a)) % 33.83/34.00 (∀ (Y : Iota), % 33.83/34.00 And (program_halts2 Y Y → Not (halts2 (skS.0 5 a) Y)) (program_not_halts2_halts2_outputs (skS.0 5 a) Y good))) % 33.85/34.02 True) % 33.85/34.02 (Or (Eq (program a_1) False) % 33.85/34.02 (Eq (∀ (Y : Iota), And (program_halts2_halts2_outputs a_1 Y good) (program_not_halts2_halts2_outputs a_1 Y bad)) % 33.85/34.02 False)) % 33.85/34.02 Clause #190 (by clausification #[189]): ∀ (a a_1 : Iota), % 33.85/34.02 Or (Eq (program a) False) % 33.85/34.02 (Or % 33.85/34.02 (Eq (∀ (Y : Iota), And (program_halts2_halts2_outputs a Y good) (program_not_halts2_halts2_outputs a Y bad)) % 33.85/34.02 False) % 33.85/34.02 (Eq % 33.85/34.02 (∀ (Y : Iota), % 33.85/34.02 And (program_halts2 Y Y → Not (halts2 (skS.0 5 a_1) Y)) % 33.85/34.02 (program_not_halts2_halts2_outputs (skS.0 5 a_1) Y good)) % 33.85/34.02 True)) % 33.85/34.02 Clause #191 (by clausification #[189]): ∀ (a a_1 : Iota), % 33.85/34.02 Or (Eq (program a) False) % 33.85/34.02 (Or % 33.85/34.02 (Eq (∀ (Y : Iota), And (program_halts2_halts2_outputs a Y good) (program_not_halts2_halts2_outputs a Y bad)) % 33.85/34.02 False) % 33.85/34.02 (Eq (program (skS.0 5 a_1)) True)) % 33.85/34.02 Clause #192 (by clausification #[190]): ∀ (a a_1 a_2 : Iota), % 33.85/34.02 Or (Eq (program a) False) % 33.85/34.02 (Or % 33.85/34.02 (Eq % 33.85/34.02 (∀ (Y : Iota), % 33.85/34.02 And (program_halts2 Y Y → Not (halts2 (skS.0 5 a_1) Y)) % 33.85/34.02 (program_not_halts2_halts2_outputs (skS.0 5 a_1) Y good)) % 33.85/34.02 True) % 33.85/34.02 (Eq % 33.85/34.02 (Not % 33.85/34.02 (And (program_halts2_halts2_outputs a (skS.0 6 a a_2) good) % 33.85/34.02 (program_not_halts2_halts2_outputs a (skS.0 6 a a_2) bad))) % 33.85/34.02 True)) % 33.85/34.02 Clause #193 (by clausification #[192]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.02 Or (Eq (program a) False) % 33.85/34.02 (Or % 33.85/34.02 (Eq % 33.85/34.02 (Not % 33.85/34.02 (And (program_halts2_halts2_outputs a (skS.0 6 a a_1) good) % 33.85/34.02 (program_not_halts2_halts2_outputs a (skS.0 6 a a_1) bad))) % 33.85/34.02 True) % 33.85/34.02 (Eq % 33.85/34.02 (And (program_halts2 a_2 a_2 → Not (halts2 (skS.0 5 a_3) a_2)) % 33.85/34.02 (program_not_halts2_halts2_outputs (skS.0 5 a_3) a_2 good)) % 33.85/34.02 True)) % 33.85/34.02 Clause #194 (by clausification #[193]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.02 Or (Eq (program a) False) % 33.85/34.02 (Or % 33.85/34.02 (Eq % 33.85/34.02 (And (program_halts2 a_1 a_1 → Not (halts2 (skS.0 5 a_2) a_1)) % 33.85/34.02 (program_not_halts2_halts2_outputs (skS.0 5 a_2) a_1 good)) % 33.85/34.02 True) % 33.85/34.02 (Eq % 33.85/34.02 (And (program_halts2_halts2_outputs a (skS.0 6 a a_3) good) % 33.85/34.02 (program_not_halts2_halts2_outputs a (skS.0 6 a a_3) bad)) % 33.85/34.02 False)) % 33.85/34.02 Clause #195 (by clausification #[194]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.02 Or (Eq (program a) False) % 33.85/34.02 (Or % 33.85/34.02 (Eq % 33.85/34.02 (And (program_halts2_halts2_outputs a (skS.0 6 a a_1) good) % 33.85/34.02 (program_not_halts2_halts2_outputs a (skS.0 6 a a_1) bad)) % 33.85/34.02 False) % 33.85/34.02 (Eq (program_not_halts2_halts2_outputs (skS.0 5 a_2) a_3 good) True)) % 33.85/34.02 Clause #196 (by clausification #[194]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.02 Or (Eq (program a) False) % 33.85/34.02 (Or % 33.85/34.02 (Eq % 33.85/34.02 (And (program_halts2_halts2_outputs a (skS.0 6 a a_1) good) % 33.85/34.02 (program_not_halts2_halts2_outputs a (skS.0 6 a a_1) bad)) % 33.85/34.02 False) % 33.85/34.02 (Eq (program_halts2 a_2 a_2 → Not (halts2 (skS.0 5 a_3) a_2)) True)) % 33.85/34.02 Clause #197 (by clausification #[195]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.02 Or (Eq (program a) False) % 33.85/34.02 (Or (Eq (program_not_halts2_halts2_outputs (skS.0 5 a_1) a_2 good) True) % 33.85/34.02 (Or (Eq (program_halts2_halts2_outputs a (skS.0 6 a a_3) good) False) % 33.85/34.02 (Eq (program_not_halts2_halts2_outputs a (skS.0 6 a a_3) bad) False))) % 33.85/34.02 Clause #289 (by clausification #[168]): ∀ (a a_1 a_2 : Iota), % 33.85/34.02 Or (Eq (program a) False) % 33.85/34.02 (Or (Eq (program (skS.0 3 a_1)) True) % 33.85/34.02 (Eq % 33.85/34.02 (Not % 33.85/34.02 (And (program_halts2_halts3_outputs a (skS.0 8 a a_2) (skS.0 8 a a_2) good) % 33.85/34.02 (program_not_halts2_halts3_outputs a (skS.0 8 a a_2) (skS.0 8 a a_2) bad))) % 33.85/34.02 True)) % 33.85/34.02 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 : Iota), % 33.85/34.02 Or (Eq (program a) False) % 33.85/34.02 (Or (Eq (program (skS.0 3 a_1)) True) % 33.85/34.02 (Eq % 33.85/34.02 (And (program_halts2_halts3_outputs a (skS.0 8 a a_2) (skS.0 8 a a_2) good) % 33.85/34.02 (program_not_halts2_halts3_outputs a (skS.0 8 a a_2) (skS.0 8 a a_2) bad)) % 33.85/34.02 False)) % 33.85/34.02 Clause #291 (by clausification #[290]): ∀ (a a_1 a_2 : Iota), % 33.85/34.02 Or (Eq (program a) False) % 33.85/34.02 (Or (Eq (program (skS.0 3 a_1)) True) % 33.85/34.02 (Or (Eq (program_halts2_halts3_outputs a (skS.0 8 a a_2) (skS.0 8 a a_2) good) False) % 33.85/34.04 (Eq (program_not_halts2_halts3_outputs a (skS.0 8 a a_2) (skS.0 8 a a_2) bad) False))) % 33.85/34.04 Clause #293 (by superposition #[291, 58]): ∀ (a a_1 a_2 : Iota), % 33.85/34.04 Or (Eq (program (skS.0 3 a)) True) % 33.85/34.04 (Or % 33.85/34.04 (Eq (program_halts2_halts3_outputs (skS.0 0 a_1) (skS.0 8 (skS.0 0 a_1) a_2) (skS.0 8 (skS.0 0 a_1) a_2) good) % 33.85/34.04 False) % 33.85/34.04 (Or % 33.85/34.04 (Eq % 33.85/34.04 (program_not_halts2_halts3_outputs (skS.0 0 a_1) (skS.0 8 (skS.0 0 a_1) a_2) (skS.0 8 (skS.0 0 a_1) a_2) bad) % 33.85/34.04 False) % 33.85/34.04 (Eq False True))) % 33.85/34.04 Clause #300 (by clausification #[173]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.04 Or (Eq (program a) False) % 33.85/34.04 (Or (Eq (program_halts2_halts2_outputs (skS.0 3 a_1) a_2 good) True) % 33.85/34.04 (Or (Eq (program_halts2_halts3_outputs a (skS.0 4 a a_3) (skS.0 4 a a_3) good) False) % 33.85/34.04 (Eq (program_not_halts2_halts3_outputs a (skS.0 4 a a_3) (skS.0 4 a a_3) bad) False))) % 33.85/34.04 Clause #302 (by superposition #[300, 58]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.04 Or (Eq (program_halts2_halts2_outputs (skS.0 3 a) a_1 good) True) % 33.85/34.04 (Or % 33.85/34.04 (Eq (program_halts2_halts3_outputs (skS.0 0 a_2) (skS.0 4 (skS.0 0 a_2) a_3) (skS.0 4 (skS.0 0 a_2) a_3) good) % 33.85/34.04 False) % 33.85/34.04 (Or % 33.85/34.04 (Eq % 33.85/34.04 (program_not_halts2_halts3_outputs (skS.0 0 a_2) (skS.0 4 (skS.0 0 a_2) a_3) (skS.0 4 (skS.0 0 a_2) a_3) bad) % 33.85/34.04 False) % 33.85/34.04 (Eq False True))) % 33.85/34.04 Clause #315 (by clausification #[191]): ∀ (a a_1 a_2 : Iota), % 33.85/34.04 Or (Eq (program a) False) % 33.85/34.04 (Or (Eq (program (skS.0 5 a_1)) True) % 33.85/34.04 (Eq % 33.85/34.04 (Not % 33.85/34.04 (And (program_halts2_halts2_outputs a (skS.0 9 a a_2) good) % 33.85/34.04 (program_not_halts2_halts2_outputs a (skS.0 9 a a_2) bad))) % 33.85/34.04 True)) % 33.85/34.04 Clause #316 (by clausification #[315]): ∀ (a a_1 a_2 : Iota), % 33.85/34.04 Or (Eq (program a) False) % 33.85/34.04 (Or (Eq (program (skS.0 5 a_1)) True) % 33.85/34.04 (Eq % 33.85/34.04 (And (program_halts2_halts2_outputs a (skS.0 9 a a_2) good) % 33.85/34.04 (program_not_halts2_halts2_outputs a (skS.0 9 a a_2) bad)) % 33.85/34.04 False)) % 33.85/34.04 Clause #317 (by clausification #[316]): ∀ (a a_1 a_2 : Iota), % 33.85/34.04 Or (Eq (program a) False) % 33.85/34.04 (Or (Eq (program (skS.0 5 a_1)) True) % 33.85/34.04 (Or (Eq (program_halts2_halts2_outputs a (skS.0 9 a a_2) good) False) % 33.85/34.04 (Eq (program_not_halts2_halts2_outputs a (skS.0 9 a a_2) bad) False))) % 33.85/34.04 Clause #324 (by clausification #[176]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.04 Or (Eq (program_not_halts2_halts2_outputs (skS.0 3 a) a_1 bad) True) % 33.85/34.04 (Or % 33.85/34.04 (Eq (program_halts2_halts3_outputs (skS.0 0 a_2) (skS.0 4 (skS.0 0 a_2) a_3) (skS.0 4 (skS.0 0 a_2) a_3) good) % 33.85/34.04 False) % 33.85/34.04 (Eq (program_not_halts2_halts3_outputs (skS.0 0 a_2) (skS.0 4 (skS.0 0 a_2) a_3) (skS.0 4 (skS.0 0 a_2) a_3) bad) % 33.85/34.04 False)) % 33.85/34.04 Clause #325 (by forward demodulation #[324, 161]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.04 Or (Eq (program_not_halts2_halts2_outputs (skS.0 3 a) a_1 bad) True) % 33.85/34.04 (Or (Eq True False) % 33.85/34.04 (Eq (program_not_halts2_halts3_outputs (skS.0 0 a_2) (skS.0 4 (skS.0 0 a_2) a_3) (skS.0 4 (skS.0 0 a_2) a_3) bad) % 33.85/34.04 False)) % 33.85/34.04 Clause #326 (by clausification #[325]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.04 Or (Eq (program_not_halts2_halts2_outputs (skS.0 3 a) a_1 bad) True) % 33.85/34.04 (Eq (program_not_halts2_halts3_outputs (skS.0 0 a_2) (skS.0 4 (skS.0 0 a_2) a_3) (skS.0 4 (skS.0 0 a_2) a_3) bad) % 33.85/34.04 False) % 33.85/34.04 Clause #327 (by superposition #[326, 159]): ∀ (a a_1 : Iota), Or (Eq (program_not_halts2_halts2_outputs (skS.0 3 a) a_1 bad) True) (Eq False True) % 33.85/34.04 Clause #329 (by clausification #[327]): ∀ (a a_1 : Iota), Eq (program_not_halts2_halts2_outputs (skS.0 3 a) a_1 bad) True % 33.85/34.04 Clause #348 (by clausification #[196]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.04 Or (Eq (program a) False) % 33.85/34.04 (Or (Eq (program_halts2 a_1 a_1 → Not (halts2 (skS.0 5 a_2) a_1)) True) % 33.85/34.04 (Or (Eq (program_halts2_halts2_outputs a (skS.0 6 a a_3) good) False) % 33.85/34.04 (Eq (program_not_halts2_halts2_outputs a (skS.0 6 a a_3) bad) False))) % 33.85/34.04 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.04 Or (Eq (program a) False) % 33.85/34.04 (Or (Eq (program_halts2_halts2_outputs a (skS.0 6 a a_1) good) False) % 33.85/34.04 (Or (Eq (program_not_halts2_halts2_outputs a (skS.0 6 a a_1) bad) False) % 33.85/34.06 (Or (Eq (program_halts2 a_2 a_2) False) (Eq (Not (halts2 (skS.0 5 a_3) a_2)) True)))) % 33.85/34.06 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.06 Or (Eq (program a) False) % 33.85/34.06 (Or (Eq (program_halts2_halts2_outputs a (skS.0 6 a a_1) good) False) % 33.85/34.06 (Or (Eq (program_not_halts2_halts2_outputs a (skS.0 6 a a_1) bad) False) % 33.85/34.06 (Or (Eq (program_halts2 a_2 a_2) False) (Eq (halts2 (skS.0 5 a_3) a_2) False)))) % 33.85/34.06 Clause #636 (by clausification #[293]): ∀ (a a_1 a_2 : Iota), % 33.85/34.06 Or (Eq (program (skS.0 3 a)) True) % 33.85/34.06 (Or % 33.85/34.06 (Eq (program_halts2_halts3_outputs (skS.0 0 a_1) (skS.0 8 (skS.0 0 a_1) a_2) (skS.0 8 (skS.0 0 a_1) a_2) good) % 33.85/34.06 False) % 33.85/34.06 (Eq (program_not_halts2_halts3_outputs (skS.0 0 a_1) (skS.0 8 (skS.0 0 a_1) a_2) (skS.0 8 (skS.0 0 a_1) a_2) bad) % 33.85/34.06 False)) % 33.85/34.06 Clause #637 (by forward demodulation #[636, 161]): ∀ (a a_1 a_2 : Iota), % 33.85/34.06 Or (Eq (program (skS.0 3 a)) True) % 33.85/34.06 (Or (Eq True False) % 33.85/34.06 (Eq (program_not_halts2_halts3_outputs (skS.0 0 a_1) (skS.0 8 (skS.0 0 a_1) a_2) (skS.0 8 (skS.0 0 a_1) a_2) bad) % 33.85/34.06 False)) % 33.85/34.06 Clause #638 (by clausification #[637]): ∀ (a a_1 a_2 : Iota), % 33.85/34.06 Or (Eq (program (skS.0 3 a)) True) % 33.85/34.06 (Eq (program_not_halts2_halts3_outputs (skS.0 0 a_1) (skS.0 8 (skS.0 0 a_1) a_2) (skS.0 8 (skS.0 0 a_1) a_2) bad) % 33.85/34.06 False) % 33.85/34.06 Clause #639 (by superposition #[638, 159]): ∀ (a : Iota), Or (Eq (program (skS.0 3 a)) True) (Eq False True) % 33.85/34.06 Clause #641 (by clausification #[639]): ∀ (a : Iota), Eq (program (skS.0 3 a)) True % 33.85/34.06 Clause #647 (by superposition #[641, 197]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.06 Or (Eq True False) % 33.85/34.06 (Or (Eq (program_not_halts2_halts2_outputs (skS.0 5 a) a_1 good) True) % 33.85/34.06 (Or (Eq (program_halts2_halts2_outputs (skS.0 3 a_2) (skS.0 6 (skS.0 3 a_2) a_3) good) False) % 33.85/34.06 (Eq (program_not_halts2_halts2_outputs (skS.0 3 a_2) (skS.0 6 (skS.0 3 a_2) a_3) bad) False))) % 33.85/34.06 Clause #649 (by superposition #[641, 317]): ∀ (a a_1 a_2 : Iota), % 33.85/34.06 Or (Eq True False) % 33.85/34.06 (Or (Eq (program (skS.0 5 a)) True) % 33.85/34.06 (Or (Eq (program_halts2_halts2_outputs (skS.0 3 a_1) (skS.0 9 (skS.0 3 a_1) a_2) good) False) % 33.85/34.06 (Eq (program_not_halts2_halts2_outputs (skS.0 3 a_1) (skS.0 9 (skS.0 3 a_1) a_2) bad) False))) % 33.85/34.06 Clause #650 (by superposition #[641, 350]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.06 Or (Eq True False) % 33.85/34.06 (Or (Eq (program_halts2_halts2_outputs (skS.0 3 a) (skS.0 6 (skS.0 3 a) a_1) good) False) % 33.85/34.06 (Or (Eq (program_not_halts2_halts2_outputs (skS.0 3 a) (skS.0 6 (skS.0 3 a) a_1) bad) False) % 33.85/34.06 (Or (Eq (program_halts2 a_2 a_2) False) (Eq (halts2 (skS.0 5 a_3) a_2) False)))) % 33.85/34.06 Clause #688 (by clausification #[302]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.06 Or (Eq (program_halts2_halts2_outputs (skS.0 3 a) a_1 good) True) % 33.85/34.06 (Or % 33.85/34.06 (Eq (program_halts2_halts3_outputs (skS.0 0 a_2) (skS.0 4 (skS.0 0 a_2) a_3) (skS.0 4 (skS.0 0 a_2) a_3) good) % 33.85/34.06 False) % 33.85/34.06 (Eq (program_not_halts2_halts3_outputs (skS.0 0 a_2) (skS.0 4 (skS.0 0 a_2) a_3) (skS.0 4 (skS.0 0 a_2) a_3) bad) % 33.85/34.06 False)) % 33.85/34.06 Clause #689 (by forward demodulation #[688, 161]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.06 Or (Eq (program_halts2_halts2_outputs (skS.0 3 a) a_1 good) True) % 33.85/34.06 (Or (Eq True False) % 33.85/34.06 (Eq (program_not_halts2_halts3_outputs (skS.0 0 a_2) (skS.0 4 (skS.0 0 a_2) a_3) (skS.0 4 (skS.0 0 a_2) a_3) bad) % 33.85/34.06 False)) % 33.85/34.06 Clause #690 (by clausification #[689]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.06 Or (Eq (program_halts2_halts2_outputs (skS.0 3 a) a_1 good) True) % 33.85/34.06 (Eq (program_not_halts2_halts3_outputs (skS.0 0 a_2) (skS.0 4 (skS.0 0 a_2) a_3) (skS.0 4 (skS.0 0 a_2) a_3) bad) % 33.85/34.06 False) % 33.85/34.06 Clause #691 (by superposition #[690, 159]): ∀ (a a_1 : Iota), Or (Eq (program_halts2_halts2_outputs (skS.0 3 a) a_1 good) True) (Eq False True) % 33.85/34.06 Clause #693 (by clausification #[691]): ∀ (a a_1 : Iota), Eq (program_halts2_halts2_outputs (skS.0 3 a) a_1 good) True % 33.85/34.06 Clause #3407 (by clausification #[647]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.06 Or (Eq (program_not_halts2_halts2_outputs (skS.0 5 a) a_1 good) True) % 33.85/34.06 (Or (Eq (program_halts2_halts2_outputs (skS.0 3 a_2) (skS.0 6 (skS.0 3 a_2) a_3) good) False) % 33.85/34.09 (Eq (program_not_halts2_halts2_outputs (skS.0 3 a_2) (skS.0 6 (skS.0 3 a_2) a_3) bad) False)) % 33.85/34.09 Clause #3408 (by forward demodulation #[3407, 329]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.09 Or (Eq (program_not_halts2_halts2_outputs (skS.0 5 a) a_1 good) True) % 33.85/34.09 (Or (Eq (program_halts2_halts2_outputs (skS.0 3 a_2) (skS.0 6 (skS.0 3 a_2) a_3) good) False) (Eq True False)) % 33.85/34.09 Clause #3409 (by clausification #[3408]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.09 Or (Eq (program_not_halts2_halts2_outputs (skS.0 5 a) a_1 good) True) % 33.85/34.09 (Eq (program_halts2_halts2_outputs (skS.0 3 a_2) (skS.0 6 (skS.0 3 a_2) a_3) good) False) % 33.85/34.09 Clause #3410 (by superposition #[3409, 693]): ∀ (a a_1 : Iota), Or (Eq (program_not_halts2_halts2_outputs (skS.0 5 a) a_1 good) True) (Eq False True) % 33.85/34.09 Clause #3423 (by clausification #[3410]): ∀ (a a_1 : Iota), Eq (program_not_halts2_halts2_outputs (skS.0 5 a) a_1 good) True % 33.85/34.09 Clause #3424 (by superposition #[3423, 143]): ∀ (a a_1 : Iota), % 33.85/34.09 Or (Eq True False) (Or (Eq (program_not_halts2 a a) False) (Eq (halts2_outputs (skS.0 5 a_1) a good) True)) % 33.85/34.09 Clause #3425 (by clausification #[3424]): ∀ (a a_1 : Iota), Or (Eq (program_not_halts2 a a) False) (Eq (halts2_outputs (skS.0 5 a_1) a good) True) % 33.85/34.09 Clause #3429 (by superposition #[3425, 128]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.09 Or (Eq (halts2_outputs (skS.0 5 a) a_1 good) True) % 33.85/34.09 (Or (Eq (program_not_halts2_halts2_outputs a_2 a_1 a_3) True) (Eq False True)) % 33.85/34.09 Clause #3430 (by clausification #[3429]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.09 Or (Eq (halts2_outputs (skS.0 5 a) a_1 good) True) (Eq (program_not_halts2_halts2_outputs a_2 a_1 a_3) True) % 33.85/34.09 Clause #3433 (by superposition #[3430, 111]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.09 Or (Eq (program_not_halts2_halts2_outputs a a_1 a_2) True) (Or (Eq True False) (Eq (halts2 (skS.0 5 a_3) a_1) True)) % 33.85/34.09 Clause #3436 (by clausification #[3433]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.09 Or (Eq (program_not_halts2_halts2_outputs a a_1 a_2) True) (Eq (halts2 (skS.0 5 a_3) a_1) True) % 33.85/34.09 Clause #3439 (by superposition #[3436, 141]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 33.85/34.09 Or (Eq (program_not_halts2_halts2_outputs a (skS.0 5 a_1) a_2) True) % 33.85/34.09 (Or (Eq (program_not_halts2_halts2_outputs a_3 (skS.0 5 a_1) a_4) True) (Eq True False)) % 33.85/34.09 Clause #3457 (by clausification #[649]): ∀ (a a_1 a_2 : Iota), % 33.85/34.09 Or (Eq (program (skS.0 5 a)) True) % 33.85/34.09 (Or (Eq (program_halts2_halts2_outputs (skS.0 3 a_1) (skS.0 9 (skS.0 3 a_1) a_2) good) False) % 33.85/34.09 (Eq (program_not_halts2_halts2_outputs (skS.0 3 a_1) (skS.0 9 (skS.0 3 a_1) a_2) bad) False)) % 33.85/34.09 Clause #3458 (by forward demodulation #[3457, 329]): ∀ (a a_1 a_2 : Iota), % 33.85/34.09 Or (Eq (program (skS.0 5 a)) True) % 33.85/34.09 (Or (Eq (program_halts2_halts2_outputs (skS.0 3 a_1) (skS.0 9 (skS.0 3 a_1) a_2) good) False) (Eq True False)) % 33.85/34.09 Clause #3459 (by clausification #[3458]): ∀ (a a_1 a_2 : Iota), % 33.85/34.09 Or (Eq (program (skS.0 5 a)) True) % 33.85/34.09 (Eq (program_halts2_halts2_outputs (skS.0 3 a_1) (skS.0 9 (skS.0 3 a_1) a_2) good) False) % 33.85/34.09 Clause #3460 (by superposition #[3459, 693]): ∀ (a : Iota), Or (Eq (program (skS.0 5 a)) True) (Eq False True) % 33.85/34.09 Clause #3473 (by clausification #[3460]): ∀ (a : Iota), Eq (program (skS.0 5 a)) True % 33.85/34.09 Clause #3475 (by superposition #[3473, 56]): ∀ (a a_1 : Iota), Or (Eq (program_halts2 (skS.0 5 a) a_1) True) (Or (Eq True False) (Eq (halts2 (skS.0 5 a) a_1) False)) % 33.85/34.09 Clause #3476 (by superposition #[3473, 82]): ∀ (a a_1 : Iota), % 33.85/34.09 Or (Eq (program_not_halts2 (skS.0 5 a) a_1) True) (Or (Eq True False) (Eq (halts2 (skS.0 5 a) a_1) True)) % 33.85/34.09 Clause #3483 (by clausification #[3476]): ∀ (a a_1 : Iota), Or (Eq (program_not_halts2 (skS.0 5 a) a_1) True) (Eq (halts2 (skS.0 5 a) a_1) True) % 33.85/34.09 Clause #3512 (by clausification #[650]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.09 Or (Eq (program_halts2_halts2_outputs (skS.0 3 a) (skS.0 6 (skS.0 3 a) a_1) good) False) % 33.85/34.09 (Or (Eq (program_not_halts2_halts2_outputs (skS.0 3 a) (skS.0 6 (skS.0 3 a) a_1) bad) False) % 33.85/34.09 (Or (Eq (program_halts2 a_2 a_2) False) (Eq (halts2 (skS.0 5 a_3) a_2) False))) % 33.85/34.09 Clause #3513 (by forward demodulation #[3512, 329]): ∀ (a a_1 a_2 a_3 : Iota), % 33.85/34.09 Or (Eq (program_halts2_halts2_outputs (skS.0 3 a) (skS.0 6 (skS.0 3 a) a_1) good) False) % 33.94/34.14 (Or (Eq True False) (Or (Eq (program_halts2 a_2 a_2) False) (Eq (halts2 (skS.0 5 a_3) a_2) False))) % 33.94/34.14 Clause #3514 (by clausification #[3513]): ∀ (a a_1 a_2 a_3 : Iota), % 33.94/34.14 Or (Eq (program_halts2_halts2_outputs (skS.0 3 a) (skS.0 6 (skS.0 3 a) a_1) good) False) % 33.94/34.14 (Or (Eq (program_halts2 a_2 a_2) False) (Eq (halts2 (skS.0 5 a_3) a_2) False)) % 33.94/34.14 Clause #3515 (by superposition #[3514, 693]): ∀ (a a_1 : Iota), Or (Eq (program_halts2 a a) False) (Or (Eq (halts2 (skS.0 5 a_1) a) False) (Eq False True)) % 33.94/34.14 Clause #3528 (by clausification #[3515]): ∀ (a a_1 : Iota), Or (Eq (program_halts2 a a) False) (Eq (halts2 (skS.0 5 a_1) a) False) % 33.94/34.14 Clause #3558 (by clausification #[3475]): ∀ (a a_1 : Iota), Or (Eq (program_halts2 (skS.0 5 a) a_1) True) (Eq (halts2 (skS.0 5 a) a_1) False) % 33.94/34.14 Clause #3602 (by clausification #[3439]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 33.94/34.14 Or (Eq (program_not_halts2_halts2_outputs a (skS.0 5 a_1) a_2) True) % 33.94/34.14 (Eq (program_not_halts2_halts2_outputs a_3 (skS.0 5 a_1) a_4) True) % 33.94/34.14 Clause #3604 (by equality factoring #[3602]): ∀ (a a_1 a_2 : Iota), Or (Ne True True) (Eq (program_not_halts2_halts2_outputs a (skS.0 5 a_1) a_2) True) % 33.94/34.14 Clause #3607 (by clausification #[3604]): ∀ (a a_1 a_2 : Iota), % 33.94/34.14 Or (Eq (program_not_halts2_halts2_outputs a (skS.0 5 a_1) a_2) True) (Or (Eq True False) (Eq True False)) % 33.94/34.14 Clause #3609 (by clausification #[3607]): ∀ (a a_1 a_2 : Iota), Or (Eq (program_not_halts2_halts2_outputs a (skS.0 5 a_1) a_2) True) (Eq True False) % 33.94/34.14 Clause #3610 (by clausification #[3609]): ∀ (a a_1 a_2 : Iota), Eq (program_not_halts2_halts2_outputs a (skS.0 5 a_1) a_2) True % 33.94/34.14 Clause #3611 (by superposition #[3610, 143]): ∀ (a a_1 a_2 : Iota), % 33.94/34.14 Or (Eq True False) % 33.94/34.14 (Or (Eq (program_not_halts2 (skS.0 5 a) (skS.0 5 a)) False) (Eq (halts2_outputs a_1 (skS.0 5 a) a_2) True)) % 33.94/34.14 Clause #3652 (by clausification #[3611]): ∀ (a a_1 a_2 : Iota), % 33.94/34.14 Or (Eq (program_not_halts2 (skS.0 5 a) (skS.0 5 a)) False) (Eq (halts2_outputs a_1 (skS.0 5 a) a_2) True) % 33.94/34.14 Clause #3653 (by superposition #[3652, 3483]): ∀ (a a_1 a_2 : Iota), % 33.94/34.14 Or (Eq (halts2_outputs a (skS.0 5 a_1) a_2) True) (Or (Eq False True) (Eq (halts2 (skS.0 5 a_1) (skS.0 5 a_1)) True)) % 33.94/34.14 Clause #3656 (by clausification #[3653]): ∀ (a a_1 a_2 : Iota), Or (Eq (halts2_outputs a (skS.0 5 a_1) a_2) True) (Eq (halts2 (skS.0 5 a_1) (skS.0 5 a_1)) True) % 33.94/34.14 Clause #3659 (by superposition #[3656, 111]): ∀ (a a_1 : Iota), Or (Eq (halts2 (skS.0 5 a) (skS.0 5 a)) True) (Or (Eq True False) (Eq (halts2 a_1 (skS.0 5 a)) True)) % 33.94/34.14 Clause #4089 (by clausification #[3659]): ∀ (a a_1 : Iota), Or (Eq (halts2 (skS.0 5 a) (skS.0 5 a)) True) (Eq (halts2 a_1 (skS.0 5 a)) True) % 33.94/34.14 Clause #4100 (by equality factoring #[4089]): ∀ (a : Iota), Or (Ne True True) (Eq (halts2 (skS.0 5 a) (skS.0 5 a)) True) % 33.94/34.14 Clause #4101 (by clausification #[4100]): ∀ (a : Iota), Or (Eq (halts2 (skS.0 5 a) (skS.0 5 a)) True) (Or (Eq True False) (Eq True False)) % 33.94/34.14 Clause #4103 (by clausification #[4101]): ∀ (a : Iota), Or (Eq (halts2 (skS.0 5 a) (skS.0 5 a)) True) (Eq True False) % 33.94/34.14 Clause #4104 (by clausification #[4103]): ∀ (a : Iota), Eq (halts2 (skS.0 5 a) (skS.0 5 a)) True % 33.94/34.14 Clause #4106 (by superposition #[4104, 3558]): ∀ (a : Iota), Or (Eq (program_halts2 (skS.0 5 a) (skS.0 5 a)) True) (Eq True False) % 33.94/34.14 Clause #4108 (by clausification #[4106]): ∀ (a : Iota), Eq (program_halts2 (skS.0 5 a) (skS.0 5 a)) True % 33.94/34.14 Clause #4119 (by superposition #[4108, 3528]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (halts2 (skS.0 5 a) (skS.0 5 a_1)) False) % 33.94/34.14 Clause #4126 (by clausification #[4119]): ∀ (a a_1 : Iota), Eq (halts2 (skS.0 5 a) (skS.0 5 a_1)) False % 33.94/34.14 Clause #4127 (by superposition #[4126, 4104]): Eq False True % 33.94/34.14 Clause #4130 (by clausification #[4127]): False % 33.94/34.14 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------