%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM003_1 : TPTP v9.2.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.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 27.01s 27.24s % Output : Proof 27.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.10 % Problem : COM003_1 : TPTP v9.2.0. Released v5.0.0. % 0.05/0.11 % Command : duper %s % 0.10/0.31 % Computer : n008.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Thu Oct 2 16:06:23 EDT 2025 % 0.10/0.31 % CPUTime : % 27.01/27.24 SZS status Theorem for theBenchmark.p % 27.01/27.24 SZS output start Proof for theBenchmark.p % 27.01/27.24 Clause #0 (by assumption #[]): Eq % 27.01/27.24 ((Exists fun X => ∀ (Y : program) (Z : input), decides X Y Z) → % 27.01/27.24 Exists fun W => ∀ (Y : program) (Z : input), decides (algorithm_of W) Y Z) % 27.01/27.24 True % 27.01/27.24 Clause #1 (by assumption #[]): Eq % 27.01/27.24 (∀ (W Y : program) (Z : input), % 27.01/27.24 decides (algorithm_of W) Y Z → % 27.01/27.24 ∀ (Y : program) (Z : input), % 27.01/27.24 And (halts2 Y Z → And (halts3 W Y Z) (outputs W good)) (Not (halts2 Y Z) → And (halts3 W Y Z) (outputs W bad))) % 27.01/27.24 True % 27.01/27.24 Clause #2 (by assumption #[]): Eq % 27.01/27.24 ((Exists fun W => % 27.01/27.24 ∀ (Y : program), % 27.01/27.24 And (halts2 Y (as_input Y) → And (halts3 W Y (as_input Y)) (outputs W good)) % 27.01/27.24 (Not (halts2 Y (as_input Y)) → And (halts3 W Y (as_input Y)) (outputs W bad))) → % 27.01/27.24 Exists fun V => % 27.01/27.24 ∀ (Y : program), % 27.01/27.24 And (halts2 Y (as_input Y) → And (halts2 V (as_input Y)) (outputs V good)) % 27.01/27.24 (Not (halts2 Y (as_input Y)) → And (halts2 V (as_input Y)) (outputs V bad))) % 27.01/27.24 True % 27.01/27.24 Clause #3 (by assumption #[]): Eq % 27.01/27.24 ((Exists fun V => % 27.01/27.24 ∀ (Y : program), % 27.01/27.24 And (halts2 Y (as_input Y) → And (halts2 V (as_input Y)) (outputs V good)) % 27.01/27.24 (Not (halts2 Y (as_input Y)) → And (halts2 V (as_input Y)) (outputs V bad))) → % 27.01/27.24 Exists fun U => % 27.01/27.24 ∀ (Y : program), % 27.01/27.24 And (halts2 Y (as_input Y) → Not (halts2 U (as_input Y))) % 27.01/27.24 (Not (halts2 Y (as_input Y)) → And (halts2 U (as_input Y)) (outputs U bad))) % 27.01/27.24 True % 27.01/27.24 Clause #4 (by assumption #[]): Eq (Not (Not (Exists fun X1 => ∀ (Y1 : program) (Z1 : input), decides X1 Y1 Z1))) True % 27.01/27.24 Clause #5 (by clausification #[4]): Eq (Not (Exists fun X1 => ∀ (Y1 : program) (Z1 : input), decides X1 Y1 Z1)) False % 27.01/27.24 Clause #6 (by clausification #[5]): Eq (Exists fun X1 => ∀ (Y1 : program) (Z1 : input), decides X1 Y1 Z1) True % 27.01/27.24 Clause #7 (by clausification #[6]): ∀ (a : algorithm), Eq (∀ (Y1 : program) (Z1 : input), decides (skS.0 0 a) Y1 Z1) True % 27.01/27.24 Clause #8 (by clausification #[7]): ∀ (a : algorithm) (a_1 : program), Eq (∀ (Z1 : input), decides (skS.0 0 a) a_1 Z1) True % 27.01/27.24 Clause #9 (by clausification #[8]): ∀ (a : algorithm) (a_1 : program) (a_2 : input), Eq (decides (skS.0 0 a) a_1 a_2) True % 27.01/27.24 Clause #10 (by clausification #[0]): Or (Eq (Exists fun X => ∀ (Y : program) (Z : input), decides X Y Z) False) % 27.01/27.24 (Eq (Exists fun W => ∀ (Y : program) (Z : input), decides (algorithm_of W) Y Z) True) % 27.01/27.24 Clause #11 (by clausification #[10]): ∀ (a : algorithm), % 27.01/27.24 Or (Eq (Exists fun W => ∀ (Y : program) (Z : input), decides (algorithm_of W) Y Z) True) % 27.01/27.24 (Eq (∀ (Y : program) (Z : input), decides a Y Z) False) % 27.01/27.24 Clause #12 (by clausification #[11]): ∀ (a : algorithm) (a_1 : program), % 27.01/27.24 Or (Eq (∀ (Y : program) (Z : input), decides a Y Z) False) % 27.01/27.24 (Eq (∀ (Y : program) (Z : input), decides (algorithm_of (skS.0 1 a_1)) Y Z) True) % 27.01/27.24 Clause #13 (by clausification #[12]): ∀ (a : program) (a_1 : algorithm) (a_2 : program), % 27.01/27.24 Or (Eq (∀ (Y : program) (Z : input), decides (algorithm_of (skS.0 1 a)) Y Z) True) % 27.01/27.24 (Eq (Not (∀ (Z : input), decides a_1 (skS.0 2 a_1 a_2) Z)) True) % 27.01/27.24 Clause #14 (by clausification #[13]): ∀ (a : algorithm) (a_1 a_2 a_3 : program), % 27.01/27.24 Or (Eq (Not (∀ (Z : input), decides a (skS.0 2 a a_1) Z)) True) % 27.01/27.24 (Eq (∀ (Z : input), decides (algorithm_of (skS.0 1 a_2)) a_3 Z) True) % 27.01/27.24 Clause #15 (by clausification #[14]): ∀ (a a_1 : program) (a_2 : algorithm) (a_3 : program), % 27.01/27.24 Or (Eq (∀ (Z : input), decides (algorithm_of (skS.0 1 a)) a_1 Z) True) % 27.01/27.24 (Eq (∀ (Z : input), decides a_2 (skS.0 2 a_2 a_3) Z) False) % 27.01/27.24 Clause #16 (by clausification #[15]): ∀ (a : algorithm) (a_1 a_2 a_3 : program) (a_4 : input), % 27.01/27.24 Or (Eq (∀ (Z : input), decides a (skS.0 2 a a_1) Z) False) (Eq (decides (algorithm_of (skS.0 1 a_2)) a_3 a_4) True) % 27.01/27.24 Clause #17 (by clausification #[16]): ∀ (a a_1 : program) (a_2 : input) (a_3 : algorithm) (a_4 : program) (a_5 : input), % 27.01/27.24 Or (Eq (decides (algorithm_of (skS.0 1 a)) a_1 a_2) True) % 27.01/27.24 (Eq (Not (decides a_3 (skS.0 2 a_3 a_4) (skS.0 3 a_3 a_4 a_5))) True) % 27.01/27.24 Clause #18 (by clausification #[17]): ∀ (a a_1 : program) (a_2 : input) (a_3 : algorithm) (a_4 : program) (a_5 : input), % 27.04/27.26 Or (Eq (decides (algorithm_of (skS.0 1 a)) a_1 a_2) True) % 27.04/27.26 (Eq (decides a_3 (skS.0 2 a_3 a_4) (skS.0 3 a_3 a_4 a_5)) False) % 27.04/27.26 Clause #19 (by superposition #[18, 9]): ∀ (a a_1 : program) (a_2 : input), Or (Eq (decides (algorithm_of (skS.0 1 a)) a_1 a_2) True) (Eq False True) % 27.04/27.26 Clause #20 (by clausification #[19]): ∀ (a a_1 : program) (a_2 : input), Eq (decides (algorithm_of (skS.0 1 a)) a_1 a_2) True % 27.04/27.26 Clause #21 (by clausification #[3]): Or % 27.04/27.26 (Eq % 27.04/27.26 (Exists fun V => % 27.04/27.26 ∀ (Y : program), % 27.04/27.26 And (halts2 Y (as_input Y) → And (halts2 V (as_input Y)) (outputs V good)) % 27.04/27.26 (Not (halts2 Y (as_input Y)) → And (halts2 V (as_input Y)) (outputs V bad))) % 27.04/27.26 False) % 27.04/27.26 (Eq % 27.04/27.26 (Exists fun U => % 27.04/27.26 ∀ (Y : program), % 27.04/27.26 And (halts2 Y (as_input Y) → Not (halts2 U (as_input Y))) % 27.04/27.26 (Not (halts2 Y (as_input Y)) → And (halts2 U (as_input Y)) (outputs U bad))) % 27.04/27.26 True) % 27.04/27.26 Clause #22 (by clausification #[21]): ∀ (a : program), % 27.04/27.26 Or % 27.04/27.26 (Eq % 27.04/27.26 (Exists fun U => % 27.04/27.26 ∀ (Y : program), % 27.04/27.26 And (halts2 Y (as_input Y) → Not (halts2 U (as_input Y))) % 27.04/27.26 (Not (halts2 Y (as_input Y)) → And (halts2 U (as_input Y)) (outputs U bad))) % 27.04/27.26 True) % 27.04/27.26 (Eq % 27.04/27.26 (∀ (Y : program), % 27.04/27.26 And (halts2 Y (as_input Y) → And (halts2 a (as_input Y)) (outputs a good)) % 27.04/27.26 (Not (halts2 Y (as_input Y)) → And (halts2 a (as_input Y)) (outputs a bad))) % 27.04/27.26 False) % 27.04/27.26 Clause #23 (by clausification #[22]): ∀ (a a_1 : program), % 27.04/27.26 Or % 27.04/27.26 (Eq % 27.04/27.26 (∀ (Y : program), % 27.04/27.26 And (halts2 Y (as_input Y) → And (halts2 a (as_input Y)) (outputs a good)) % 27.04/27.26 (Not (halts2 Y (as_input Y)) → And (halts2 a (as_input Y)) (outputs a bad))) % 27.04/27.26 False) % 27.04/27.26 (Eq % 27.04/27.26 (∀ (Y : program), % 27.04/27.26 And (halts2 Y (as_input Y) → Not (halts2 (skS.0 4 a_1) (as_input Y))) % 27.04/27.26 (Not (halts2 Y (as_input Y)) → And (halts2 (skS.0 4 a_1) (as_input Y)) (outputs (skS.0 4 a_1) bad))) % 27.04/27.26 True) % 27.04/27.26 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 : program), % 27.04/27.26 Or % 27.04/27.26 (Eq % 27.04/27.26 (∀ (Y : program), % 27.04/27.26 And (halts2 Y (as_input Y) → Not (halts2 (skS.0 4 a) (as_input Y))) % 27.04/27.26 (Not (halts2 Y (as_input Y)) → And (halts2 (skS.0 4 a) (as_input Y)) (outputs (skS.0 4 a) bad))) % 27.04/27.26 True) % 27.04/27.26 (Eq % 27.04/27.26 (Not % 27.04/27.26 (And % 27.04/27.26 (halts2 (skS.0 5 a_1 a_2) (as_input (skS.0 5 a_1 a_2)) → % 27.04/27.26 And (halts2 a_1 (as_input (skS.0 5 a_1 a_2))) (outputs a_1 good)) % 27.04/27.26 (Not (halts2 (skS.0 5 a_1 a_2) (as_input (skS.0 5 a_1 a_2))) → % 27.04/27.26 And (halts2 a_1 (as_input (skS.0 5 a_1 a_2))) (outputs a_1 bad)))) % 27.04/27.26 True) % 27.04/27.26 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.26 Or % 27.04/27.26 (Eq % 27.04/27.26 (Not % 27.04/27.26 (And % 27.04/27.26 (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1)) → % 27.04/27.26 And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a good)) % 27.04/27.26 (Not (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1))) → % 27.04/27.26 And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a bad)))) % 27.04/27.26 True) % 27.04/27.26 (Eq % 27.04/27.26 (And (halts2 a_2 (as_input a_2) → Not (halts2 (skS.0 4 a_3) (as_input a_2))) % 27.04/27.26 (Not (halts2 a_2 (as_input a_2)) → And (halts2 (skS.0 4 a_3) (as_input a_2)) (outputs (skS.0 4 a_3) bad))) % 27.04/27.26 True) % 27.04/27.26 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.26 Or % 27.04/27.26 (Eq % 27.04/27.26 (And (halts2 a (as_input a) → Not (halts2 (skS.0 4 a_1) (as_input a))) % 27.04/27.26 (Not (halts2 a (as_input a)) → And (halts2 (skS.0 4 a_1) (as_input a)) (outputs (skS.0 4 a_1) bad))) % 27.04/27.26 True) % 27.04/27.26 (Eq % 27.04/27.26 (And % 27.04/27.26 (halts2 (skS.0 5 a_2 a_3) (as_input (skS.0 5 a_2 a_3)) → % 27.04/27.26 And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 good)) % 27.04/27.26 (Not (halts2 (skS.0 5 a_2 a_3) (as_input (skS.0 5 a_2 a_3))) → % 27.04/27.26 And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 bad))) % 27.04/27.26 False) % 27.04/27.26 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.26 Or % 27.04/27.26 (Eq % 27.04/27.26 (And % 27.04/27.26 (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1)) → And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a good)) % 27.04/27.28 (Not (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1))) → % 27.04/27.28 And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a bad))) % 27.04/27.28 False) % 27.04/27.28 (Eq (Not (halts2 a_2 (as_input a_2)) → And (halts2 (skS.0 4 a_3) (as_input a_2)) (outputs (skS.0 4 a_3) bad)) True) % 27.04/27.28 Clause #28 (by clausification #[26]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.28 Or % 27.04/27.28 (Eq % 27.04/27.28 (And % 27.04/27.28 (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1)) → And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a good)) % 27.04/27.28 (Not (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1))) → % 27.04/27.28 And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a bad))) % 27.04/27.28 False) % 27.04/27.28 (Eq (halts2 a_2 (as_input a_2) → Not (halts2 (skS.0 4 a_3) (as_input a_2))) True) % 27.04/27.28 Clause #29 (by clausification #[27]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.28 Or (Eq (Not (halts2 a (as_input a)) → And (halts2 (skS.0 4 a_1) (as_input a)) (outputs (skS.0 4 a_1) bad)) True) % 27.04/27.28 (Or % 27.04/27.28 (Eq % 27.04/27.28 (halts2 (skS.0 5 a_2 a_3) (as_input (skS.0 5 a_2 a_3)) → % 27.04/27.28 And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 good)) % 27.04/27.28 False) % 27.04/27.28 (Eq % 27.04/27.28 (Not (halts2 (skS.0 5 a_2 a_3) (as_input (skS.0 5 a_2 a_3))) → % 27.04/27.28 And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 bad)) % 27.04/27.28 False)) % 27.04/27.28 Clause #30 (by clausification #[29]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.28 Or % 27.04/27.28 (Eq (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1)) → And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a good)) % 27.04/27.28 False) % 27.04/27.28 (Or % 27.04/27.28 (Eq % 27.04/27.28 (Not (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1))) → % 27.04/27.28 And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a bad)) % 27.04/27.28 False) % 27.04/27.28 (Or (Eq (Not (halts2 a_2 (as_input a_2))) False) % 27.04/27.28 (Eq (And (halts2 (skS.0 4 a_3) (as_input a_2)) (outputs (skS.0 4 a_3) bad)) True))) % 27.04/27.28 Clause #32 (by clausification #[30]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.28 Or % 27.04/27.28 (Eq % 27.04/27.28 (Not (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1))) → % 27.04/27.28 And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a bad)) % 27.04/27.28 False) % 27.04/27.28 (Or (Eq (Not (halts2 a_2 (as_input a_2))) False) % 27.04/27.28 (Or (Eq (And (halts2 (skS.0 4 a_3) (as_input a_2)) (outputs (skS.0 4 a_3) bad)) True) % 27.04/27.28 (Eq (And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a good)) False))) % 27.04/27.28 Clause #39 (by clausification #[2]): Or % 27.04/27.28 (Eq % 27.04/27.28 (Exists fun W => % 27.04/27.28 ∀ (Y : program), % 27.04/27.28 And (halts2 Y (as_input Y) → And (halts3 W Y (as_input Y)) (outputs W good)) % 27.04/27.28 (Not (halts2 Y (as_input Y)) → And (halts3 W Y (as_input Y)) (outputs W bad))) % 27.04/27.28 False) % 27.04/27.28 (Eq % 27.04/27.28 (Exists fun V => % 27.04/27.28 ∀ (Y : program), % 27.04/27.28 And (halts2 Y (as_input Y) → And (halts2 V (as_input Y)) (outputs V good)) % 27.04/27.28 (Not (halts2 Y (as_input Y)) → And (halts2 V (as_input Y)) (outputs V bad))) % 27.04/27.28 True) % 27.04/27.28 Clause #40 (by clausification #[39]): ∀ (a : program), % 27.04/27.28 Or % 27.04/27.28 (Eq % 27.04/27.28 (Exists fun V => % 27.04/27.28 ∀ (Y : program), % 27.04/27.28 And (halts2 Y (as_input Y) → And (halts2 V (as_input Y)) (outputs V good)) % 27.04/27.28 (Not (halts2 Y (as_input Y)) → And (halts2 V (as_input Y)) (outputs V bad))) % 27.04/27.28 True) % 27.04/27.28 (Eq % 27.04/27.28 (∀ (Y : program), % 27.04/27.28 And (halts2 Y (as_input Y) → And (halts3 a Y (as_input Y)) (outputs a good)) % 27.04/27.28 (Not (halts2 Y (as_input Y)) → And (halts3 a Y (as_input Y)) (outputs a bad))) % 27.04/27.28 False) % 27.04/27.28 Clause #41 (by clausification #[40]): ∀ (a a_1 : program), % 27.04/27.28 Or % 27.04/27.28 (Eq % 27.04/27.28 (∀ (Y : program), % 27.04/27.28 And (halts2 Y (as_input Y) → And (halts3 a Y (as_input Y)) (outputs a good)) % 27.04/27.28 (Not (halts2 Y (as_input Y)) → And (halts3 a Y (as_input Y)) (outputs a bad))) % 27.04/27.28 False) % 27.04/27.28 (Eq % 27.04/27.28 (∀ (Y : program), % 27.04/27.28 And (halts2 Y (as_input Y) → And (halts2 (skS.0 6 a_1) (as_input Y)) (outputs (skS.0 6 a_1) good)) % 27.04/27.28 (Not (halts2 Y (as_input Y)) → And (halts2 (skS.0 6 a_1) (as_input Y)) (outputs (skS.0 6 a_1) bad))) % 27.04/27.28 True) % 27.04/27.28 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 : program), % 27.04/27.28 Or % 27.04/27.28 (Eq % 27.04/27.28 (∀ (Y : program), % 27.04/27.28 And (halts2 Y (as_input Y) → And (halts2 (skS.0 6 a) (as_input Y)) (outputs (skS.0 6 a) good)) % 27.04/27.30 (Not (halts2 Y (as_input Y)) → And (halts2 (skS.0 6 a) (as_input Y)) (outputs (skS.0 6 a) bad))) % 27.04/27.30 True) % 27.04/27.30 (Eq % 27.04/27.30 (Not % 27.04/27.30 (And % 27.04/27.30 (halts2 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2)) → % 27.04/27.30 And (halts3 a_1 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) (outputs a_1 good)) % 27.04/27.30 (Not (halts2 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) → % 27.04/27.30 And (halts3 a_1 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) (outputs a_1 bad)))) % 27.04/27.30 True) % 27.04/27.30 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.30 Or % 27.04/27.30 (Eq % 27.04/27.30 (Not % 27.04/27.30 (And % 27.04/27.30 (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1)) → % 27.04/27.30 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a good)) % 27.04/27.30 (Not (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) → % 27.04/27.30 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad)))) % 27.04/27.30 True) % 27.04/27.30 (Eq % 27.04/27.30 (And (halts2 a_2 (as_input a_2) → And (halts2 (skS.0 6 a_3) (as_input a_2)) (outputs (skS.0 6 a_3) good)) % 27.04/27.30 (Not (halts2 a_2 (as_input a_2)) → And (halts2 (skS.0 6 a_3) (as_input a_2)) (outputs (skS.0 6 a_3) bad))) % 27.04/27.30 True) % 27.04/27.30 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.30 Or % 27.04/27.30 (Eq % 27.04/27.30 (And (halts2 a (as_input a) → And (halts2 (skS.0 6 a_1) (as_input a)) (outputs (skS.0 6 a_1) good)) % 27.04/27.30 (Not (halts2 a (as_input a)) → And (halts2 (skS.0 6 a_1) (as_input a)) (outputs (skS.0 6 a_1) bad))) % 27.04/27.30 True) % 27.04/27.30 (Eq % 27.04/27.30 (And % 27.04/27.30 (halts2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3)) → % 27.04/27.30 And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 good)) % 27.04/27.30 (Not (halts2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) → % 27.04/27.30 And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 bad))) % 27.04/27.30 False) % 27.04/27.30 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.30 Or % 27.04/27.30 (Eq % 27.04/27.30 (And % 27.04/27.30 (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1)) → % 27.04/27.30 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a good)) % 27.04/27.30 (Not (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) → % 27.04/27.30 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad))) % 27.04/27.30 False) % 27.04/27.30 (Eq (Not (halts2 a_2 (as_input a_2)) → And (halts2 (skS.0 6 a_3) (as_input a_2)) (outputs (skS.0 6 a_3) bad)) True) % 27.04/27.30 Clause #46 (by clausification #[44]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.30 Or % 27.04/27.30 (Eq % 27.04/27.30 (And % 27.04/27.30 (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1)) → % 27.04/27.30 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a good)) % 27.04/27.30 (Not (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) → % 27.04/27.30 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad))) % 27.04/27.30 False) % 27.04/27.30 (Eq (halts2 a_2 (as_input a_2) → And (halts2 (skS.0 6 a_3) (as_input a_2)) (outputs (skS.0 6 a_3) good)) True) % 27.04/27.30 Clause #47 (by clausification #[45]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.30 Or (Eq (Not (halts2 a (as_input a)) → And (halts2 (skS.0 6 a_1) (as_input a)) (outputs (skS.0 6 a_1) bad)) True) % 27.04/27.30 (Or % 27.04/27.30 (Eq % 27.04/27.30 (halts2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3)) → % 27.04/27.30 And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 good)) % 27.04/27.30 False) % 27.04/27.30 (Eq % 27.04/27.30 (Not (halts2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) → % 27.04/27.30 And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 bad)) % 27.04/27.30 False)) % 27.04/27.30 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.30 Or % 27.04/27.30 (Eq % 27.04/27.30 (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1)) → % 27.04/27.30 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a good)) % 27.04/27.30 False) % 27.04/27.30 (Or % 27.04/27.30 (Eq % 27.04/27.30 (Not (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) → % 27.04/27.30 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad)) % 27.04/27.30 False) % 27.04/27.30 (Or (Eq (Not (halts2 a_2 (as_input a_2))) False) % 27.04/27.30 (Eq (And (halts2 (skS.0 6 a_3) (as_input a_2)) (outputs (skS.0 6 a_3) bad)) True))) % 27.04/27.30 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.32 Or % 27.04/27.32 (Eq % 27.04/27.32 (Not (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) → % 27.04/27.32 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad)) % 27.04/27.32 False) % 27.04/27.32 (Or (Eq (Not (halts2 a_2 (as_input a_2))) False) % 27.04/27.32 (Or (Eq (And (halts2 (skS.0 6 a_3) (as_input a_2)) (outputs (skS.0 6 a_3) bad)) True) % 27.04/27.32 (Eq (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) True))) % 27.04/27.32 Clause #50 (by clausification #[48]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.32 Or % 27.04/27.32 (Eq % 27.04/27.32 (Not (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) → % 27.04/27.32 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad)) % 27.04/27.32 False) % 27.04/27.32 (Or (Eq (Not (halts2 a_2 (as_input a_2))) False) % 27.04/27.32 (Or (Eq (And (halts2 (skS.0 6 a_3) (as_input a_2)) (outputs (skS.0 6 a_3) bad)) True) % 27.04/27.32 (Eq (And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a good)) False))) % 27.04/27.32 Clause #52 (by clausification #[49]): ∀ (a a_1 a_2 a_3 : program), % 27.04/27.32 Or (Eq (Not (halts2 a (as_input a))) False) % 27.04/27.32 (Or (Eq (And (halts2 (skS.0 6 a_1) (as_input a)) (outputs (skS.0 6 a_1) bad)) True) % 27.04/27.32 (Or (Eq (halts2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) True) % 27.04/27.32 (Eq (And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 bad)) False))) % 27.04/27.32 Clause #57 (by clausification #[1]): ∀ (a : program), % 27.04/27.32 Eq % 27.04/27.32 (∀ (Y : program) (Z : input), % 27.04/27.32 decides (algorithm_of a) Y Z → % 27.04/27.32 ∀ (Y : program) (Z : input), % 27.04/27.32 And (halts2 Y Z → And (halts3 a Y Z) (outputs a good)) % 27.04/27.32 (Not (halts2 Y Z) → And (halts3 a Y Z) (outputs a bad))) % 27.04/27.32 True % 27.04/27.32 Clause #58 (by clausification #[57]): ∀ (a a_1 : program), % 27.04/27.32 Eq % 27.04/27.32 (∀ (Z : input), % 27.04/27.32 decides (algorithm_of a) a_1 Z → % 27.04/27.32 ∀ (Y : program) (Z : input), % 27.04/27.32 And (halts2 Y Z → And (halts3 a Y Z) (outputs a good)) % 27.04/27.32 (Not (halts2 Y Z) → And (halts3 a Y Z) (outputs a bad))) % 27.04/27.32 True % 27.04/27.32 Clause #59 (by clausification #[58]): ∀ (a a_1 : program) (a_2 : input), % 27.04/27.32 Eq % 27.04/27.32 (decides (algorithm_of a) a_1 a_2 → % 27.04/27.32 ∀ (Y : program) (Z : input), % 27.04/27.32 And (halts2 Y Z → And (halts3 a Y Z) (outputs a good)) (Not (halts2 Y Z) → And (halts3 a Y Z) (outputs a bad))) % 27.04/27.32 True % 27.04/27.32 Clause #60 (by clausification #[59]): ∀ (a a_1 : program) (a_2 : input), % 27.04/27.32 Or (Eq (decides (algorithm_of a) a_1 a_2) False) % 27.04/27.32 (Eq % 27.04/27.32 (∀ (Y : program) (Z : input), % 27.04/27.32 And (halts2 Y Z → And (halts3 a Y Z) (outputs a good)) (Not (halts2 Y Z) → And (halts3 a Y Z) (outputs a bad))) % 27.04/27.32 True) % 27.04/27.32 Clause #61 (by clausification #[60]): ∀ (a a_1 : program) (a_2 : input) (a_3 : program), % 27.04/27.32 Or (Eq (decides (algorithm_of a) a_1 a_2) False) % 27.04/27.32 (Eq % 27.04/27.32 (∀ (Z : input), % 27.04/27.32 And (halts2 a_3 Z → And (halts3 a a_3 Z) (outputs a good)) % 27.04/27.32 (Not (halts2 a_3 Z) → And (halts3 a a_3 Z) (outputs a bad))) % 27.04/27.32 True) % 27.04/27.32 Clause #62 (by clausification #[61]): ∀ (a a_1 : program) (a_2 : input) (a_3 : program) (a_4 : input), % 27.04/27.32 Or (Eq (decides (algorithm_of a) a_1 a_2) False) % 27.04/27.32 (Eq % 27.04/27.32 (And (halts2 a_3 a_4 → And (halts3 a a_3 a_4) (outputs a good)) % 27.04/27.32 (Not (halts2 a_3 a_4) → And (halts3 a a_3 a_4) (outputs a bad))) % 27.04/27.32 True) % 27.04/27.32 Clause #63 (by clausification #[62]): ∀ (a a_1 : program) (a_2 : input) (a_3 : program) (a_4 : input), % 27.04/27.32 Or (Eq (decides (algorithm_of a) a_1 a_2) False) % 27.04/27.32 (Eq (Not (halts2 a_3 a_4) → And (halts3 a a_3 a_4) (outputs a bad)) True) % 27.04/27.32 Clause #64 (by clausification #[62]): ∀ (a a_1 : program) (a_2 : input) (a_3 : program) (a_4 : input), % 27.04/27.32 Or (Eq (decides (algorithm_of a) a_1 a_2) False) (Eq (halts2 a_3 a_4 → And (halts3 a a_3 a_4) (outputs a good)) True) % 27.04/27.32 Clause #65 (by clausification #[63]): ∀ (a a_1 : program) (a_2 : input) (a_3 : program) (a_4 : input), % 27.04/27.32 Or (Eq (decides (algorithm_of a) a_1 a_2) False) % 27.04/27.32 (Or (Eq (Not (halts2 a_3 a_4)) False) (Eq (And (halts3 a a_3 a_4) (outputs a bad)) True)) % 27.04/27.32 Clause #66 (by clausification #[65]): ∀ (a a_1 : program) (a_2 : input) (a_3 : program) (a_4 : input), % 27.04/27.32 Or (Eq (decides (algorithm_of a) a_1 a_2) False) % 27.04/27.32 (Or (Eq (And (halts3 a a_3 a_4) (outputs a bad)) True) (Eq (halts2 a_3 a_4) True)) % 27.12/27.34 Clause #67 (by clausification #[66]): ∀ (a a_1 : program) (a_2 : input) (a_3 : program) (a_4 : input), % 27.12/27.34 Or (Eq (decides (algorithm_of a) a_1 a_2) False) (Or (Eq (halts2 a_3 a_4) True) (Eq (outputs a bad) True)) % 27.12/27.34 Clause #68 (by clausification #[66]): ∀ (a a_1 : program) (a_2 : input) (a_3 : program) (a_4 : input), % 27.12/27.34 Or (Eq (decides (algorithm_of a) a_1 a_2) False) (Or (Eq (halts2 a_3 a_4) True) (Eq (halts3 a a_3 a_4) True)) % 27.12/27.34 Clause #69 (by superposition #[67, 20]): ∀ (a : program) (a_1 : input) (a_2 : program), % 27.12/27.34 Or (Eq (halts2 a a_1) True) (Or (Eq (outputs (skS.0 1 a_2) bad) True) (Eq False True)) % 27.12/27.34 Clause #70 (by clausification #[69]): ∀ (a : program) (a_1 : input) (a_2 : program), Or (Eq (halts2 a a_1) True) (Eq (outputs (skS.0 1 a_2) bad) True) % 27.12/27.34 Clause #71 (by superposition #[68, 20]): ∀ (a : program) (a_1 : input) (a_2 : program), % 27.12/27.34 Or (Eq (halts2 a a_1) True) (Or (Eq (halts3 (skS.0 1 a_2) a a_1) True) (Eq False True)) % 27.12/27.34 Clause #72 (by clausification #[64]): ∀ (a a_1 : program) (a_2 : input) (a_3 : program) (a_4 : input), % 27.12/27.34 Or (Eq (decides (algorithm_of a) a_1 a_2) False) % 27.12/27.34 (Or (Eq (halts2 a_3 a_4) False) (Eq (And (halts3 a a_3 a_4) (outputs a good)) True)) % 27.12/27.34 Clause #73 (by clausification #[72]): ∀ (a a_1 : program) (a_2 : input) (a_3 : program) (a_4 : input), % 27.12/27.34 Or (Eq (decides (algorithm_of a) a_1 a_2) False) (Or (Eq (halts2 a_3 a_4) False) (Eq (outputs a good) True)) % 27.12/27.34 Clause #74 (by clausification #[72]): ∀ (a a_1 : program) (a_2 : input) (a_3 : program) (a_4 : input), % 27.12/27.34 Or (Eq (decides (algorithm_of a) a_1 a_2) False) (Or (Eq (halts2 a_3 a_4) False) (Eq (halts3 a a_3 a_4) True)) % 27.12/27.34 Clause #75 (by superposition #[73, 20]): ∀ (a : program) (a_1 : input) (a_2 : program), % 27.12/27.34 Or (Eq (halts2 a a_1) False) (Or (Eq (outputs (skS.0 1 a_2) good) True) (Eq False True)) % 27.12/27.34 Clause #76 (by clausification #[75]): ∀ (a : program) (a_1 : input) (a_2 : program), Or (Eq (halts2 a a_1) False) (Eq (outputs (skS.0 1 a_2) good) True) % 27.12/27.34 Clause #77 (by superposition #[76, 70]): ∀ (a a_1 : program), Or (Eq (outputs (skS.0 1 a) good) True) (Or (Eq False True) (Eq (outputs (skS.0 1 a_1) bad) True)) % 27.12/27.34 Clause #78 (by superposition #[74, 20]): ∀ (a : program) (a_1 : input) (a_2 : program), % 27.12/27.34 Or (Eq (halts2 a a_1) False) (Or (Eq (halts3 (skS.0 1 a_2) a a_1) True) (Eq False True)) % 27.12/27.34 Clause #79 (by clausification #[28]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.34 Or (Eq (halts2 a (as_input a) → Not (halts2 (skS.0 4 a_1) (as_input a))) True) % 27.12/27.34 (Or % 27.12/27.34 (Eq % 27.12/27.34 (halts2 (skS.0 5 a_2 a_3) (as_input (skS.0 5 a_2 a_3)) → % 27.12/27.34 And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 good)) % 27.12/27.34 False) % 27.12/27.34 (Eq % 27.12/27.34 (Not (halts2 (skS.0 5 a_2 a_3) (as_input (skS.0 5 a_2 a_3))) → % 27.12/27.34 And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 bad)) % 27.12/27.34 False)) % 27.12/27.34 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.34 Or % 27.12/27.34 (Eq (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1)) → And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a good)) % 27.12/27.34 False) % 27.12/27.34 (Or % 27.12/27.34 (Eq % 27.12/27.34 (Not (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1))) → % 27.12/27.34 And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a bad)) % 27.12/27.34 False) % 27.12/27.34 (Or (Eq (halts2 a_2 (as_input a_2)) False) (Eq (Not (halts2 (skS.0 4 a_3) (as_input a_2))) True))) % 27.12/27.34 Clause #82 (by clausification #[80]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.34 Or % 27.12/27.34 (Eq % 27.12/27.34 (Not (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1))) → % 27.12/27.34 And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a bad)) % 27.12/27.34 False) % 27.12/27.34 (Or (Eq (halts2 a_2 (as_input a_2)) False) % 27.12/27.34 (Or (Eq (Not (halts2 (skS.0 4 a_3) (as_input a_2))) True) % 27.12/27.34 (Eq (And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a good)) False))) % 27.12/27.34 Clause #87 (by clausification #[71]): ∀ (a : program) (a_1 : input) (a_2 : program), Or (Eq (halts2 a a_1) True) (Eq (halts3 (skS.0 1 a_2) a a_1) True) % 27.12/27.34 Clause #88 (by clausification #[78]): ∀ (a : program) (a_1 : input) (a_2 : program), Or (Eq (halts2 a a_1) False) (Eq (halts3 (skS.0 1 a_2) a a_1) True) % 27.12/27.34 Clause #90 (by clausification #[77]): ∀ (a a_1 : program), Or (Eq (outputs (skS.0 1 a) good) True) (Eq (outputs (skS.0 1 a_1) bad) True) % 27.12/27.37 Clause #92 (by clausification #[82]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.37 Or (Eq (halts2 a (as_input a)) False) % 27.12/27.37 (Or (Eq (Not (halts2 (skS.0 4 a_1) (as_input a))) True) % 27.12/27.37 (Or (Eq (And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 good)) False) % 27.12/27.37 (Eq (Not (halts2 (skS.0 5 a_2 a_3) (as_input (skS.0 5 a_2 a_3)))) True))) % 27.12/27.37 Clause #93 (by clausification #[82]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.37 Or (Eq (halts2 a (as_input a)) False) % 27.12/27.37 (Or (Eq (Not (halts2 (skS.0 4 a_1) (as_input a))) True) % 27.12/27.37 (Or (Eq (And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 good)) False) % 27.12/27.37 (Eq (And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 bad)) False))) % 27.12/27.37 Clause #94 (by clausification #[92]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.37 Or (Eq (halts2 a (as_input a)) False) % 27.12/27.37 (Or (Eq (And (halts2 a_1 (as_input (skS.0 5 a_1 a_2))) (outputs a_1 good)) False) % 27.12/27.37 (Or (Eq (Not (halts2 (skS.0 5 a_1 a_2) (as_input (skS.0 5 a_1 a_2)))) True) % 27.12/27.37 (Eq (halts2 (skS.0 4 a_3) (as_input a)) False))) % 27.12/27.37 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.37 Or (Eq (halts2 a (as_input a)) False) % 27.12/27.37 (Or (Eq (Not (halts2 (skS.0 5 a_1 a_2) (as_input (skS.0 5 a_1 a_2)))) True) % 27.12/27.37 (Or (Eq (halts2 (skS.0 4 a_3) (as_input a)) False) % 27.12/27.37 (Or (Eq (halts2 a_1 (as_input (skS.0 5 a_1 a_2))) False) (Eq (outputs a_1 good) False)))) % 27.12/27.37 Clause #96 (by clausification #[95]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.37 Or (Eq (halts2 a (as_input a)) False) % 27.12/27.37 (Or (Eq (halts2 (skS.0 4 a_1) (as_input a)) False) % 27.12/27.37 (Or (Eq (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) False) % 27.12/27.37 (Or (Eq (outputs a_2 good) False) (Eq (halts2 (skS.0 5 a_2 a_3) (as_input (skS.0 5 a_2 a_3))) False)))) % 27.12/27.37 Clause #97 (by superposition #[96, 70]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.12/27.37 Or (Eq (halts2 (skS.0 4 a) (as_input a_1)) False) % 27.12/27.37 (Or (Eq (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) False) % 27.12/27.37 (Or (Eq (outputs a_2 good) False) % 27.12/27.37 (Or (Eq (halts2 (skS.0 5 a_2 a_3) (as_input (skS.0 5 a_2 a_3))) False) % 27.12/27.37 (Or (Eq False True) (Eq (outputs (skS.0 1 a_4) bad) True))))) % 27.12/27.37 Clause #99 (by clausification #[32]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.37 Or (Eq (Not (halts2 a (as_input a))) False) % 27.12/27.37 (Or (Eq (And (halts2 (skS.0 4 a_1) (as_input a)) (outputs (skS.0 4 a_1) bad)) True) % 27.12/27.37 (Or (Eq (And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 good)) False) % 27.12/27.37 (Eq (And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 bad)) False))) % 27.12/27.37 Clause #107 (by clausification #[93]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.37 Or (Eq (halts2 a (as_input a)) False) % 27.12/27.37 (Or (Eq (And (halts2 a_1 (as_input (skS.0 5 a_1 a_2))) (outputs a_1 good)) False) % 27.12/27.37 (Or (Eq (And (halts2 a_1 (as_input (skS.0 5 a_1 a_2))) (outputs a_1 bad)) False) % 27.12/27.37 (Eq (halts2 (skS.0 4 a_3) (as_input a)) False))) % 27.12/27.37 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.37 Or (Eq (halts2 a (as_input a)) False) % 27.12/27.37 (Or (Eq (And (halts2 a_1 (as_input (skS.0 5 a_1 a_2))) (outputs a_1 bad)) False) % 27.12/27.37 (Or (Eq (halts2 (skS.0 4 a_3) (as_input a)) False) % 27.12/27.37 (Or (Eq (halts2 a_1 (as_input (skS.0 5 a_1 a_2))) False) (Eq (outputs a_1 good) False)))) % 27.12/27.37 Clause #109 (by clausification #[108]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.37 Or (Eq (halts2 a (as_input a)) False) % 27.12/27.37 (Or (Eq (halts2 (skS.0 4 a_1) (as_input a)) False) % 27.12/27.37 (Or (Eq (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) False) % 27.12/27.37 (Or (Eq (outputs a_2 good) False) % 27.12/27.37 (Or (Eq (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) False) (Eq (outputs a_2 bad) False))))) % 27.12/27.37 Clause #110 (by eliminate duplicate literals #[109]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.37 Or (Eq (halts2 a (as_input a)) False) % 27.12/27.37 (Or (Eq (halts2 (skS.0 4 a_1) (as_input a)) False) % 27.12/27.37 (Or (Eq (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) False) % 27.12/27.37 (Or (Eq (outputs a_2 good) False) (Eq (outputs a_2 bad) False)))) % 27.12/27.37 Clause #142 (by clausification #[46]): ∀ (a a_1 a_2 a_3 : program), % 27.12/27.37 Or (Eq (halts2 a (as_input a) → And (halts2 (skS.0 6 a_1) (as_input a)) (outputs (skS.0 6 a_1) good)) True) % 27.17/27.39 (Or % 27.17/27.39 (Eq % 27.17/27.39 (halts2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3)) → % 27.17/27.39 And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 good)) % 27.17/27.39 False) % 27.17/27.39 (Eq % 27.17/27.39 (Not (halts2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) → % 27.17/27.39 And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 bad)) % 27.17/27.39 False)) % 27.17/27.39 Clause #143 (by clausification #[142]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.39 Or % 27.17/27.39 (Eq % 27.17/27.39 (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1)) → % 27.17/27.39 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a good)) % 27.17/27.39 False) % 27.17/27.39 (Or % 27.17/27.39 (Eq % 27.17/27.39 (Not (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) → % 27.17/27.39 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad)) % 27.17/27.39 False) % 27.17/27.39 (Or (Eq (halts2 a_2 (as_input a_2)) False) % 27.17/27.39 (Eq (And (halts2 (skS.0 6 a_3) (as_input a_2)) (outputs (skS.0 6 a_3) good)) True))) % 27.17/27.39 Clause #145 (by clausification #[143]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.39 Or % 27.17/27.39 (Eq % 27.17/27.39 (Not (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) → % 27.17/27.39 And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad)) % 27.17/27.39 False) % 27.17/27.39 (Or (Eq (halts2 a_2 (as_input a_2)) False) % 27.17/27.39 (Or (Eq (And (halts2 (skS.0 6 a_3) (as_input a_2)) (outputs (skS.0 6 a_3) good)) True) % 27.17/27.39 (Eq (And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a good)) False))) % 27.17/27.39 Clause #154 (by clausification #[97]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.17/27.39 Or (Eq (halts2 (skS.0 4 a) (as_input a_1)) False) % 27.17/27.39 (Or (Eq (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) False) % 27.17/27.39 (Or (Eq (outputs a_2 good) False) % 27.17/27.39 (Or (Eq (halts2 (skS.0 5 a_2 a_3) (as_input (skS.0 5 a_2 a_3))) False) (Eq (outputs (skS.0 1 a_4) bad) True)))) % 27.17/27.39 Clause #155 (by superposition #[154, 70]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.39 Or (Eq (halts2 a (as_input (skS.0 5 a a_1))) False) % 27.17/27.39 (Or (Eq (outputs a good) False) % 27.17/27.39 (Or (Eq (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1))) False) % 27.17/27.39 (Or (Eq (outputs (skS.0 1 a_2) bad) True) (Or (Eq False True) (Eq (outputs (skS.0 1 a_3) bad) True))))) % 27.17/27.39 Clause #156 (by clausification #[155]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.39 Or (Eq (halts2 a (as_input (skS.0 5 a a_1))) False) % 27.17/27.39 (Or (Eq (outputs a good) False) % 27.17/27.39 (Or (Eq (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1))) False) % 27.17/27.39 (Or (Eq (outputs (skS.0 1 a_2) bad) True) (Eq (outputs (skS.0 1 a_3) bad) True)))) % 27.17/27.39 Clause #157 (by superposition #[156, 70]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.17/27.39 Or (Eq (outputs a good) False) % 27.17/27.39 (Or (Eq (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1))) False) % 27.17/27.39 (Or (Eq (outputs (skS.0 1 a_2) bad) True) % 27.17/27.39 (Or (Eq (outputs (skS.0 1 a_3) bad) True) (Or (Eq False True) (Eq (outputs (skS.0 1 a_4) bad) True))))) % 27.17/27.39 Clause #159 (by clausification #[50]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.39 Or (Eq (Not (halts2 a (as_input a))) False) % 27.17/27.39 (Or (Eq (And (halts2 (skS.0 6 a_1) (as_input a)) (outputs (skS.0 6 a_1) bad)) True) % 27.17/27.39 (Or (Eq (And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 good)) False) % 27.17/27.39 (Eq (And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 bad)) False))) % 27.17/27.39 Clause #167 (by clausification #[157]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.17/27.39 Or (Eq (outputs a good) False) % 27.17/27.39 (Or (Eq (halts2 (skS.0 5 a a_1) (as_input (skS.0 5 a a_1))) False) % 27.17/27.39 (Or (Eq (outputs (skS.0 1 a_2) bad) True) % 27.17/27.39 (Or (Eq (outputs (skS.0 1 a_3) bad) True) (Eq (outputs (skS.0 1 a_4) bad) True)))) % 27.17/27.39 Clause #168 (by superposition #[167, 90]): ∀ (a a_1 a_2 a_3 a_4 a_5 : program), % 27.17/27.39 Or (Eq (halts2 (skS.0 5 (skS.0 1 a) a_1) (as_input (skS.0 5 (skS.0 1 a) a_1))) False) % 27.17/27.39 (Or (Eq (outputs (skS.0 1 a_2) bad) True) % 27.17/27.39 (Or (Eq (outputs (skS.0 1 a_3) bad) True) % 27.17/27.39 (Or (Eq (outputs (skS.0 1 a_4) bad) True) (Or (Eq False True) (Eq (outputs (skS.0 1 a_5) bad) True))))) % 27.17/27.39 Clause #169 (by clausification #[99]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.39 Or (Eq (And (halts2 (skS.0 4 a) (as_input a_1)) (outputs (skS.0 4 a) bad)) True) % 27.17/27.41 (Or (Eq (And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 good)) False) % 27.17/27.41 (Or (Eq (And (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) (outputs a_2 bad)) False) % 27.17/27.41 (Eq (halts2 a_1 (as_input a_1)) True))) % 27.17/27.41 Clause #171 (by clausification #[169]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.41 Or (Eq (And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a good)) False) % 27.17/27.41 (Or (Eq (And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a bad)) False) % 27.17/27.41 (Or (Eq (halts2 a_2 (as_input a_2)) True) (Eq (halts2 (skS.0 4 a_3) (as_input a_2)) True))) % 27.17/27.41 Clause #177 (by clausification #[171]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.41 Or (Eq (And (halts2 a (as_input (skS.0 5 a a_1))) (outputs a bad)) False) % 27.17/27.41 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.17/27.41 (Or (Eq (halts2 (skS.0 4 a_3) (as_input a_2)) True) % 27.17/27.41 (Or (Eq (halts2 a (as_input (skS.0 5 a a_1))) False) (Eq (outputs a good) False)))) % 27.17/27.41 Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.41 Or (Eq (halts2 a (as_input a)) True) % 27.17/27.41 (Or (Eq (halts2 (skS.0 4 a_1) (as_input a)) True) % 27.17/27.41 (Or (Eq (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) False) % 27.17/27.41 (Or (Eq (outputs a_2 good) False) % 27.17/27.41 (Or (Eq (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) False) (Eq (outputs a_2 bad) False))))) % 27.17/27.41 Clause #179 (by eliminate duplicate literals #[178]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.41 Or (Eq (halts2 a (as_input a)) True) % 27.17/27.41 (Or (Eq (halts2 (skS.0 4 a_1) (as_input a)) True) % 27.17/27.41 (Or (Eq (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) False) % 27.17/27.41 (Or (Eq (outputs a_2 good) False) (Eq (outputs a_2 bad) False)))) % 27.17/27.41 Clause #182 (by clausification #[52]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.41 Or (Eq (And (halts2 (skS.0 6 a) (as_input a_1)) (outputs (skS.0 6 a) bad)) True) % 27.17/27.41 (Or (Eq (halts2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) True) % 27.17/27.41 (Or (Eq (And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 bad)) False) % 27.17/27.41 (Eq (halts2 a_1 (as_input a_1)) True))) % 27.17/27.41 Clause #183 (by clausification #[182]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.41 Or (Eq (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) True) % 27.17/27.41 (Or (Eq (And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad)) False) % 27.17/27.41 (Or (Eq (halts2 a_2 (as_input a_2)) True) (Eq (outputs (skS.0 6 a_3) bad) True))) % 27.17/27.41 Clause #184 (by clausification #[182]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.41 Or (Eq (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) True) % 27.17/27.41 (Or (Eq (And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad)) False) % 27.17/27.41 (Or (Eq (halts2 a_2 (as_input a_2)) True) (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True))) % 27.17/27.41 Clause #185 (by clausification #[183]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.41 Or (Eq (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) True) % 27.17/27.41 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.17/27.41 (Or (Eq (outputs (skS.0 6 a_3) bad) True) % 27.17/27.41 (Or (Eq (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) False) (Eq (outputs a bad) False)))) % 27.17/27.41 Clause #186 (by superposition #[185, 87]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.41 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.17/27.41 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.17/27.41 (Or (Eq (outputs (skS.0 6 a_3) bad) True) % 27.17/27.41 (Or (Eq (outputs (skS.0 1 a) bad) False) % 27.17/27.41 (Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) (Eq False True))))) % 27.17/27.41 Clause #188 (by clausification #[184]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.41 Or (Eq (halts2 (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) True) % 27.17/27.41 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.17/27.41 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True) % 27.17/27.41 (Or (Eq (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) False) (Eq (outputs a bad) False)))) % 27.17/27.41 Clause #189 (by superposition #[188, 87]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.41 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.17/27.41 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.17/27.41 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True) % 27.17/27.41 (Or (Eq (outputs (skS.0 1 a) bad) False) % 27.17/27.41 (Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) (Eq False True))))) % 27.17/27.44 Clause #199 (by clausification #[145]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.44 Or (Eq (halts2 a (as_input a)) False) % 27.17/27.44 (Or (Eq (And (halts2 (skS.0 6 a_1) (as_input a)) (outputs (skS.0 6 a_1) good)) True) % 27.17/27.44 (Or (Eq (And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 good)) False) % 27.17/27.44 (Eq (And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 bad)) False))) % 27.17/27.44 Clause #213 (by clausification #[168]): ∀ (a a_1 a_2 a_3 a_4 a_5 : program), % 27.17/27.44 Or (Eq (halts2 (skS.0 5 (skS.0 1 a) a_1) (as_input (skS.0 5 (skS.0 1 a) a_1))) False) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_2) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_3) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_4) bad) True) (Eq (outputs (skS.0 1 a_5) bad) True)))) % 27.17/27.44 Clause #214 (by superposition #[213, 70]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.17/27.44 Or (Eq (outputs (skS.0 1 a) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_1) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_2) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_3) bad) True) (Or (Eq False True) (Eq (outputs (skS.0 1 a_4) bad) True))))) % 27.17/27.44 Clause #219 (by clausification #[214]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.17/27.44 Or (Eq (outputs (skS.0 1 a) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_1) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_2) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_3) bad) True) (Eq (outputs (skS.0 1 a_4) bad) True)))) % 27.17/27.44 Clause #221 (by equality factoring #[219]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.44 Or (Eq (outputs (skS.0 1 a) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_1) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_2) bad) True) (Or (Ne True True) (Eq (outputs (skS.0 1 a_3) bad) True)))) % 27.17/27.44 Clause #222 (by clausification #[221]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.44 Or (Eq (outputs (skS.0 1 a) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_1) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_2) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_3) bad) True) (Or (Eq True False) (Eq True False))))) % 27.17/27.44 Clause #224 (by clausification #[222]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.44 Or (Eq (outputs (skS.0 1 a) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_1) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_2) bad) True) (Or (Eq (outputs (skS.0 1 a_3) bad) True) (Eq True False)))) % 27.17/27.44 Clause #225 (by clausification #[224]): ∀ (a a_1 a_2 a_3 : program), % 27.17/27.44 Or (Eq (outputs (skS.0 1 a) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_1) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_2) bad) True) (Eq (outputs (skS.0 1 a_3) bad) True))) % 27.17/27.44 Clause #226 (by equality factoring #[225]): ∀ (a a_1 a_2 : program), % 27.17/27.44 Or (Eq (outputs (skS.0 1 a) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_1) bad) True) (Or (Ne True True) (Eq (outputs (skS.0 1 a_2) bad) True))) % 27.17/27.44 Clause #227 (by clausification #[226]): ∀ (a a_1 a_2 : program), % 27.17/27.44 Or (Eq (outputs (skS.0 1 a) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_1) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_2) bad) True) (Or (Eq True False) (Eq True False)))) % 27.17/27.44 Clause #229 (by clausification #[227]): ∀ (a a_1 a_2 : program), % 27.17/27.44 Or (Eq (outputs (skS.0 1 a) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_1) bad) True) (Or (Eq (outputs (skS.0 1 a_2) bad) True) (Eq True False))) % 27.17/27.44 Clause #230 (by clausification #[229]): ∀ (a a_1 a_2 : program), % 27.17/27.44 Or (Eq (outputs (skS.0 1 a) bad) True) % 27.17/27.44 (Or (Eq (outputs (skS.0 1 a_1) bad) True) (Eq (outputs (skS.0 1 a_2) bad) True)) % 27.17/27.44 Clause #231 (by equality factoring #[230]): ∀ (a a_1 : program), Or (Eq (outputs (skS.0 1 a) bad) True) (Or (Ne True True) (Eq (outputs (skS.0 1 a_1) bad) True)) % 27.17/27.44 Clause #232 (by clausification #[231]): ∀ (a a_1 : program), % 27.17/27.44 Or (Eq (outputs (skS.0 1 a) bad) True) (Or (Eq (outputs (skS.0 1 a_1) bad) True) (Or (Eq True False) (Eq True False))) % 27.17/27.44 Clause #234 (by clausification #[232]): ∀ (a a_1 : program), Or (Eq (outputs (skS.0 1 a) bad) True) (Or (Eq (outputs (skS.0 1 a_1) bad) True) (Eq True False)) % 27.17/27.44 Clause #235 (by clausification #[234]): ∀ (a a_1 : program), Or (Eq (outputs (skS.0 1 a) bad) True) (Eq (outputs (skS.0 1 a_1) bad) True) % 27.17/27.44 Clause #236 (by equality factoring #[235]): ∀ (a : program), Or (Ne True True) (Eq (outputs (skS.0 1 a) bad) True) % 27.24/27.46 Clause #237 (by clausification #[236]): ∀ (a : program), Or (Eq (outputs (skS.0 1 a) bad) True) (Or (Eq True False) (Eq True False)) % 27.24/27.46 Clause #239 (by clausification #[237]): ∀ (a : program), Or (Eq (outputs (skS.0 1 a) bad) True) (Eq True False) % 27.24/27.46 Clause #240 (by clausification #[239]): ∀ (a : program), Eq (outputs (skS.0 1 a) bad) True % 27.24/27.46 Clause #241 (by clausification #[159]): ∀ (a a_1 a_2 a_3 : program), % 27.24/27.46 Or (Eq (And (halts2 (skS.0 6 a) (as_input a_1)) (outputs (skS.0 6 a) bad)) True) % 27.24/27.46 (Or (Eq (And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 good)) False) % 27.24/27.46 (Or (Eq (And (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) (outputs a_2 bad)) False) % 27.24/27.46 (Eq (halts2 a_1 (as_input a_1)) True))) % 27.24/27.46 Clause #242 (by clausification #[241]): ∀ (a a_1 a_2 a_3 : program), % 27.24/27.46 Or (Eq (And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a good)) False) % 27.24/27.46 (Or (Eq (And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad)) False) % 27.24/27.46 (Or (Eq (halts2 a_2 (as_input a_2)) True) (Eq (outputs (skS.0 6 a_3) bad) True))) % 27.24/27.46 Clause #243 (by clausification #[241]): ∀ (a a_1 a_2 a_3 : program), % 27.24/27.46 Or (Eq (And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a good)) False) % 27.24/27.46 (Or (Eq (And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad)) False) % 27.24/27.46 (Or (Eq (halts2 a_2 (as_input a_2)) True) (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True))) % 27.24/27.46 Clause #244 (by clausification #[242]): ∀ (a a_1 a_2 a_3 : program), % 27.24/27.46 Or (Eq (And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad)) False) % 27.24/27.46 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.24/27.46 (Or (Eq (outputs (skS.0 6 a_3) bad) True) % 27.24/27.46 (Or (Eq (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) False) (Eq (outputs a good) False)))) % 27.24/27.46 Clause #245 (by clausification #[244]): ∀ (a a_1 a_2 a_3 : program), % 27.24/27.46 Or (Eq (halts2 a (as_input a)) True) % 27.24/27.46 (Or (Eq (outputs (skS.0 6 a_1) bad) True) % 27.24/27.46 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) % 27.24/27.46 (Or (Eq (outputs a_2 good) False) % 27.24/27.46 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) (Eq (outputs a_2 bad) False))))) % 27.24/27.46 Clause #246 (by eliminate duplicate literals #[245]): ∀ (a a_1 a_2 a_3 : program), % 27.24/27.46 Or (Eq (halts2 a (as_input a)) True) % 27.24/27.46 (Or (Eq (outputs (skS.0 6 a_1) bad) True) % 27.24/27.46 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) % 27.24/27.46 (Or (Eq (outputs a_2 good) False) (Eq (outputs a_2 bad) False)))) % 27.24/27.46 Clause #254 (by clausification #[243]): ∀ (a a_1 a_2 a_3 : program), % 27.24/27.46 Or (Eq (And (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) (outputs a bad)) False) % 27.24/27.46 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.24/27.46 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True) % 27.24/27.46 (Or (Eq (halts3 a (skS.0 7 a a_1) (as_input (skS.0 7 a a_1))) False) (Eq (outputs a good) False)))) % 27.24/27.46 Clause #255 (by clausification #[254]): ∀ (a a_1 a_2 a_3 : program), % 27.24/27.46 Or (Eq (halts2 a (as_input a)) True) % 27.24/27.46 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.24/27.46 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) % 27.24/27.46 (Or (Eq (outputs a_2 good) False) % 27.24/27.46 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) (Eq (outputs a_2 bad) False))))) % 27.24/27.46 Clause #256 (by eliminate duplicate literals #[255]): ∀ (a a_1 a_2 a_3 : program), % 27.24/27.46 Or (Eq (halts2 a (as_input a)) True) % 27.24/27.46 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.24/27.46 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) % 27.24/27.46 (Or (Eq (outputs a_2 good) False) (Eq (outputs a_2 bad) False)))) % 27.24/27.46 Clause #262 (by clausification #[186]): ∀ (a a_1 a_2 a_3 : program), % 27.24/27.46 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.24/27.46 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.24/27.46 (Or (Eq (outputs (skS.0 6 a_3) bad) True) % 27.24/27.46 (Or (Eq (outputs (skS.0 1 a) bad) False) % 27.24/27.46 (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True)))) % 27.27/27.49 Clause #263 (by eliminate duplicate literals #[262]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.49 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.27/27.49 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.27/27.49 (Or (Eq (outputs (skS.0 6 a_3) bad) True) (Eq (outputs (skS.0 1 a) bad) False))) % 27.27/27.49 Clause #264 (by forward demodulation #[263, 240]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.49 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.27/27.49 (Or (Eq (halts2 a_2 (as_input a_2)) True) (Or (Eq (outputs (skS.0 6 a_3) bad) True) (Eq True False))) % 27.27/27.49 Clause #265 (by clausification #[264]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.49 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.27/27.49 (Or (Eq (halts2 a_2 (as_input a_2)) True) (Eq (outputs (skS.0 6 a_3) bad) True)) % 27.27/27.49 Clause #284 (by equality factoring #[265]): ∀ (a a_1 a_2 : program), % 27.27/27.49 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.27/27.49 (Or (Ne True True) (Eq (halts2 (skS.0 7 (skS.0 1 a_1) a_2) (as_input (skS.0 7 (skS.0 1 a_1) a_2))) True)) % 27.27/27.49 Clause #305 (by clausification #[189]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.49 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.27/27.49 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.27/27.49 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True) % 27.27/27.49 (Or (Eq (outputs (skS.0 1 a) bad) False) % 27.27/27.49 (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True)))) % 27.27/27.49 Clause #306 (by eliminate duplicate literals #[305]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.49 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.27/27.49 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.27/27.49 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True) (Eq (outputs (skS.0 1 a) bad) False))) % 27.27/27.49 Clause #307 (by forward demodulation #[306, 240]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.49 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.27/27.49 (Or (Eq (halts2 a_2 (as_input a_2)) True) (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True) (Eq True False))) % 27.27/27.49 Clause #308 (by clausification #[307]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.49 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.27/27.49 (Or (Eq (halts2 a_2 (as_input a_2)) True) (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True)) % 27.27/27.49 Clause #316 (by superposition #[308, 76]): ∀ (a a_1 a_2 : program), % 27.27/27.49 Or (Eq (halts2 a (as_input a)) True) % 27.27/27.49 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) (Or (Eq True False) (Eq (outputs (skS.0 1 a_2) good) True))) % 27.27/27.49 Clause #317 (by superposition #[308, 88]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.27/27.49 Or (Eq (halts2 a (as_input a)) True) % 27.27/27.49 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.27/27.49 (Or (Eq True False) % 27.27/27.49 (Eq (halts3 (skS.0 1 a_2) (skS.0 7 (skS.0 1 a_3) a_4) (as_input (skS.0 7 (skS.0 1 a_3) a_4))) True))) % 27.27/27.49 Clause #330 (by equality factoring #[308]): ∀ (a a_1 a_2 : program), % 27.27/27.49 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.27/27.49 (Or (Ne True True) (Eq (halts2 (skS.0 6 a_2) (as_input (skS.0 6 a_2))) True)) % 27.27/27.49 Clause #331 (by clausification #[316]): ∀ (a a_1 a_2 : program), % 27.27/27.49 Or (Eq (halts2 a (as_input a)) True) % 27.27/27.49 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) (Eq (outputs (skS.0 1 a_2) good) True)) % 27.27/27.49 Clause #341 (by superposition #[331, 76]): ∀ (a a_1 a_2 : program), % 27.27/27.49 Or (Eq (halts2 a (as_input a)) True) % 27.27/27.49 (Or (Eq (outputs (skS.0 1 a_1) good) True) (Or (Eq True False) (Eq (outputs (skS.0 1 a_2) good) True))) % 27.27/27.49 Clause #344 (by clausification #[341]): ∀ (a a_1 a_2 : program), % 27.27/27.49 Or (Eq (halts2 a (as_input a)) True) % 27.27/27.49 (Or (Eq (outputs (skS.0 1 a_1) good) True) (Eq (outputs (skS.0 1 a_2) good) True)) % 27.27/27.49 Clause #354 (by equality factoring #[344]): ∀ (a a_1 : program), Or (Eq (halts2 a (as_input a)) True) (Or (Ne True True) (Eq (outputs (skS.0 1 a_1) good) True)) % 27.27/27.49 Clause #355 (by clausification #[354]): ∀ (a a_1 : program), % 27.27/27.49 Or (Eq (halts2 a (as_input a)) True) (Or (Eq (outputs (skS.0 1 a_1) good) True) (Or (Eq True False) (Eq True False))) % 27.27/27.49 Clause #357 (by clausification #[355]): ∀ (a a_1 : program), Or (Eq (halts2 a (as_input a)) True) (Or (Eq (outputs (skS.0 1 a_1) good) True) (Eq True False)) % 27.27/27.51 Clause #358 (by clausification #[357]): ∀ (a a_1 : program), Or (Eq (halts2 a (as_input a)) True) (Eq (outputs (skS.0 1 a_1) good) True) % 27.27/27.51 Clause #366 (by superposition #[358, 76]): ∀ (a a_1 : program), Or (Eq (outputs (skS.0 1 a) good) True) (Or (Eq True False) (Eq (outputs (skS.0 1 a_1) good) True)) % 27.27/27.51 Clause #368 (by clausification #[366]): ∀ (a a_1 : program), Or (Eq (outputs (skS.0 1 a) good) True) (Eq (outputs (skS.0 1 a_1) good) True) % 27.27/27.51 Clause #369 (by equality factoring #[368]): ∀ (a : program), Or (Ne True True) (Eq (outputs (skS.0 1 a) good) True) % 27.27/27.51 Clause #371 (by clausification #[369]): ∀ (a : program), Or (Eq (outputs (skS.0 1 a) good) True) (Or (Eq True False) (Eq True False)) % 27.27/27.51 Clause #373 (by clausification #[371]): ∀ (a : program), Or (Eq (outputs (skS.0 1 a) good) True) (Eq True False) % 27.27/27.51 Clause #374 (by clausification #[373]): ∀ (a : program), Eq (outputs (skS.0 1 a) good) True % 27.27/27.51 Clause #380 (by clausification #[199]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.51 Or (Eq (halts2 a (as_input a)) False) % 27.27/27.51 (Or (Eq (And (halts3 a_1 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) (outputs a_1 good)) False) % 27.27/27.51 (Or (Eq (And (halts3 a_1 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) (outputs a_1 bad)) False) % 27.27/27.51 (Eq (outputs (skS.0 6 a_3) good) True))) % 27.27/27.51 Clause #381 (by clausification #[199]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.51 Or (Eq (halts2 a (as_input a)) False) % 27.27/27.51 (Or (Eq (And (halts3 a_1 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) (outputs a_1 good)) False) % 27.27/27.51 (Or (Eq (And (halts3 a_1 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) (outputs a_1 bad)) False) % 27.27/27.51 (Eq (halts2 (skS.0 6 a_3) (as_input a)) True))) % 27.27/27.51 Clause #382 (by clausification #[380]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.51 Or (Eq (halts2 a (as_input a)) False) % 27.27/27.51 (Or (Eq (And (halts3 a_1 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) (outputs a_1 bad)) False) % 27.27/27.51 (Or (Eq (outputs (skS.0 6 a_3) good) True) % 27.27/27.51 (Or (Eq (halts3 a_1 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) False) (Eq (outputs a_1 good) False)))) % 27.27/27.51 Clause #383 (by clausification #[382]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.51 Or (Eq (halts2 a (as_input a)) False) % 27.27/27.51 (Or (Eq (outputs (skS.0 6 a_1) good) True) % 27.27/27.51 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) % 27.27/27.51 (Or (Eq (outputs a_2 good) False) % 27.27/27.51 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) (Eq (outputs a_2 bad) False))))) % 27.27/27.51 Clause #384 (by eliminate duplicate literals #[383]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.51 Or (Eq (halts2 a (as_input a)) False) % 27.27/27.51 (Or (Eq (outputs (skS.0 6 a_1) good) True) % 27.27/27.51 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) % 27.27/27.51 (Or (Eq (outputs a_2 good) False) (Eq (outputs a_2 bad) False)))) % 27.27/27.51 Clause #395 (by clausification #[284]): ∀ (a a_1 a_2 : program), % 27.27/27.51 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.27/27.51 (Or (Eq (halts2 (skS.0 7 (skS.0 1 a_1) a_2) (as_input (skS.0 7 (skS.0 1 a_1) a_2))) True) % 27.27/27.51 (Or (Eq True False) (Eq True False))) % 27.27/27.51 Clause #397 (by clausification #[395]): ∀ (a a_1 a_2 : program), % 27.27/27.51 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.27/27.51 (Or (Eq (halts2 (skS.0 7 (skS.0 1 a_1) a_2) (as_input (skS.0 7 (skS.0 1 a_1) a_2))) True) (Eq True False)) % 27.27/27.51 Clause #398 (by clausification #[397]): ∀ (a a_1 a_2 : program), % 27.27/27.51 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.27/27.51 (Eq (halts2 (skS.0 7 (skS.0 1 a_1) a_2) (as_input (skS.0 7 (skS.0 1 a_1) a_2))) True) % 27.27/27.51 Clause #407 (by superposition #[398, 88]): ∀ (a a_1 a_2 a_3 : program), % 27.27/27.51 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.27/27.51 (Or (Eq True False) % 27.27/27.51 (Eq (halts3 (skS.0 1 a_1) (skS.0 7 (skS.0 1 a_2) a_3) (as_input (skS.0 7 (skS.0 1 a_2) a_3))) True)) % 27.27/27.51 Clause #410 (by clausification #[330]): ∀ (a a_1 a_2 : program), % 27.27/27.51 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.27/27.51 (Or (Eq (halts2 (skS.0 6 a_2) (as_input (skS.0 6 a_2))) True) (Or (Eq True False) (Eq True False))) % 27.27/27.51 Clause #412 (by clausification #[410]): ∀ (a a_1 a_2 : program), % 27.32/27.54 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.32/27.54 (Or (Eq (halts2 (skS.0 6 a_2) (as_input (skS.0 6 a_2))) True) (Eq True False)) % 27.32/27.54 Clause #413 (by clausification #[412]): ∀ (a a_1 a_2 : program), % 27.32/27.54 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.32/27.54 (Eq (halts2 (skS.0 6 a_2) (as_input (skS.0 6 a_2))) True) % 27.32/27.54 Clause #422 (by superposition #[413, 88]): ∀ (a a_1 a_2 a_3 : program), % 27.32/27.54 Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) % 27.32/27.54 (Or (Eq True False) % 27.32/27.54 (Eq (halts3 (skS.0 1 a_1) (skS.0 7 (skS.0 1 a_2) a_3) (as_input (skS.0 7 (skS.0 1 a_2) a_3))) True)) % 27.32/27.54 Clause #433 (by clausification #[407]): ∀ (a a_1 a_2 a_3 : program), % 27.32/27.54 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.32/27.54 (Eq (halts3 (skS.0 1 a_1) (skS.0 7 (skS.0 1 a_2) a_3) (as_input (skS.0 7 (skS.0 1 a_2) a_3))) True) % 27.32/27.54 Clause #438 (by superposition #[433, 246]): ∀ (a a_1 a_2 a_3 : program), % 27.32/27.54 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.32/27.54 (Or (Eq (halts2 a_1 (as_input a_1)) True) % 27.32/27.54 (Or (Eq (outputs (skS.0 6 a_2) bad) True) % 27.32/27.54 (Or (Eq True False) (Or (Eq (outputs (skS.0 1 a_3) good) False) (Eq (outputs (skS.0 1 a_3) bad) False))))) % 27.32/27.54 Clause #440 (by clausification #[438]): ∀ (a a_1 a_2 a_3 : program), % 27.32/27.54 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.32/27.54 (Or (Eq (halts2 a_1 (as_input a_1)) True) % 27.32/27.54 (Or (Eq (outputs (skS.0 6 a_2) bad) True) % 27.32/27.54 (Or (Eq (outputs (skS.0 1 a_3) good) False) (Eq (outputs (skS.0 1 a_3) bad) False)))) % 27.32/27.54 Clause #441 (by forward demodulation #[440, 240]): ∀ (a a_1 a_2 a_3 : program), % 27.32/27.54 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.32/27.54 (Or (Eq (halts2 a_1 (as_input a_1)) True) % 27.32/27.54 (Or (Eq (outputs (skS.0 6 a_2) bad) True) (Or (Eq (outputs (skS.0 1 a_3) good) False) (Eq True False)))) % 27.32/27.54 Clause #442 (by clausification #[441]): ∀ (a a_1 a_2 a_3 : program), % 27.32/27.54 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.32/27.54 (Or (Eq (halts2 a_1 (as_input a_1)) True) % 27.32/27.54 (Or (Eq (outputs (skS.0 6 a_2) bad) True) (Eq (outputs (skS.0 1 a_3) good) False))) % 27.32/27.54 Clause #443 (by superposition #[442, 374]): ∀ (a a_1 a_2 : program), % 27.32/27.54 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.32/27.54 (Or (Eq (halts2 a_1 (as_input a_1)) True) (Or (Eq (outputs (skS.0 6 a_2) bad) True) (Eq False True))) % 27.32/27.54 Clause #444 (by clausification #[443]): ∀ (a a_1 a_2 : program), % 27.32/27.54 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.32/27.54 (Or (Eq (halts2 a_1 (as_input a_1)) True) (Eq (outputs (skS.0 6 a_2) bad) True)) % 27.32/27.54 Clause #454 (by equality factoring #[444]): ∀ (a a_1 : program), Or (Eq (halts2 a (as_input a)) True) (Or (Ne True True) (Eq (outputs (skS.0 6 a_1) bad) True)) % 27.32/27.54 Clause #455 (by clausification #[454]): ∀ (a a_1 : program), % 27.32/27.54 Or (Eq (halts2 a (as_input a)) True) (Or (Eq (outputs (skS.0 6 a_1) bad) True) (Or (Eq True False) (Eq True False))) % 27.32/27.54 Clause #457 (by clausification #[455]): ∀ (a a_1 : program), Or (Eq (halts2 a (as_input a)) True) (Or (Eq (outputs (skS.0 6 a_1) bad) True) (Eq True False)) % 27.32/27.54 Clause #458 (by clausification #[457]): ∀ (a a_1 : program), Or (Eq (halts2 a (as_input a)) True) (Eq (outputs (skS.0 6 a_1) bad) True) % 27.32/27.54 Clause #459 (by superposition #[458, 96]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.32/27.54 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.32/27.54 (Or (Eq True False) % 27.32/27.54 (Or (Eq (halts2 (skS.0 4 a_1) (as_input a_2)) False) % 27.32/27.54 (Or (Eq (halts2 a_3 (as_input (skS.0 5 a_3 a_4))) False) % 27.32/27.54 (Or (Eq (outputs a_3 good) False) (Eq (halts2 (skS.0 5 a_3 a_4) (as_input (skS.0 5 a_3 a_4))) False))))) % 27.32/27.54 Clause #464 (by superposition #[458, 88]): ∀ (a a_1 a_2 : program), % 27.32/27.54 Or (Eq (outputs (skS.0 6 a) bad) True) (Or (Eq True False) (Eq (halts3 (skS.0 1 a_1) a_2 (as_input a_2)) True)) % 27.32/27.54 Clause #466 (by clausification #[464]): ∀ (a a_1 a_2 : program), Or (Eq (outputs (skS.0 6 a) bad) True) (Eq (halts3 (skS.0 1 a_1) a_2 (as_input a_2)) True) % 27.32/27.54 Clause #510 (by clausification #[422]): ∀ (a a_1 a_2 a_3 : program), % 27.32/27.54 Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) % 27.32/27.54 (Eq (halts3 (skS.0 1 a_1) (skS.0 7 (skS.0 1 a_2) a_3) (as_input (skS.0 7 (skS.0 1 a_2) a_3))) True) % 27.32/27.54 Clause #522 (by superposition #[510, 256]): ∀ (a a_1 a_2 a_3 : program), % 27.32/27.56 Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) % 27.32/27.56 (Or (Eq (halts2 a_1 (as_input a_1)) True) % 27.32/27.56 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_1)) True) % 27.32/27.56 (Or (Eq True False) (Or (Eq (outputs (skS.0 1 a_3) good) False) (Eq (outputs (skS.0 1 a_3) bad) False))))) % 27.32/27.56 Clause #523 (by clausification #[522]): ∀ (a a_1 a_2 a_3 : program), % 27.32/27.56 Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) % 27.32/27.56 (Or (Eq (halts2 a_1 (as_input a_1)) True) % 27.32/27.56 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_1)) True) % 27.32/27.56 (Or (Eq (outputs (skS.0 1 a_3) good) False) (Eq (outputs (skS.0 1 a_3) bad) False)))) % 27.32/27.56 Clause #524 (by forward demodulation #[523, 240]): ∀ (a a_1 a_2 a_3 : program), % 27.32/27.56 Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) % 27.32/27.56 (Or (Eq (halts2 a_1 (as_input a_1)) True) % 27.32/27.56 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_1)) True) (Or (Eq (outputs (skS.0 1 a_3) good) False) (Eq True False)))) % 27.32/27.56 Clause #525 (by clausification #[524]): ∀ (a a_1 a_2 a_3 : program), % 27.32/27.56 Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) % 27.32/27.56 (Or (Eq (halts2 a_1 (as_input a_1)) True) % 27.32/27.56 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_1)) True) (Eq (outputs (skS.0 1 a_3) good) False))) % 27.32/27.56 Clause #526 (by superposition #[525, 374]): ∀ (a a_1 a_2 : program), % 27.32/27.56 Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) % 27.32/27.56 (Or (Eq (halts2 a_1 (as_input a_1)) True) (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_1)) True) (Eq False True))) % 27.32/27.56 Clause #527 (by clausification #[526]): ∀ (a a_1 a_2 : program), % 27.32/27.56 Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) % 27.32/27.56 (Or (Eq (halts2 a_1 (as_input a_1)) True) (Eq (halts2 (skS.0 6 a_2) (as_input a_1)) True)) % 27.32/27.56 Clause #548 (by equality factoring #[527]): ∀ (a a_1 : program), % 27.32/27.56 Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) % 27.32/27.56 (Or (Ne True True) (Eq (halts2 (skS.0 6 a_1) (as_input (skS.0 6 a_1))) True)) % 27.32/27.56 Clause #549 (by clausification #[548]): ∀ (a a_1 : program), % 27.32/27.56 Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) % 27.32/27.56 (Or (Eq (halts2 (skS.0 6 a_1) (as_input (skS.0 6 a_1))) True) (Or (Eq True False) (Eq True False))) % 27.32/27.56 Clause #551 (by clausification #[549]): ∀ (a a_1 : program), % 27.32/27.56 Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) % 27.32/27.56 (Or (Eq (halts2 (skS.0 6 a_1) (as_input (skS.0 6 a_1))) True) (Eq True False)) % 27.32/27.56 Clause #552 (by clausification #[551]): ∀ (a a_1 : program), % 27.32/27.56 Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) (Eq (halts2 (skS.0 6 a_1) (as_input (skS.0 6 a_1))) True) % 27.32/27.56 Clause #559 (by equality factoring #[552]): ∀ (a : program), Or (Ne True True) (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) % 27.32/27.56 Clause #560 (by clausification #[559]): ∀ (a : program), Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) (Or (Eq True False) (Eq True False)) % 27.32/27.56 Clause #562 (by clausification #[560]): ∀ (a : program), Or (Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True) (Eq True False) % 27.32/27.56 Clause #563 (by clausification #[562]): ∀ (a : program), Eq (halts2 (skS.0 6 a) (as_input (skS.0 6 a))) True % 27.32/27.56 Clause #571 (by superposition #[563, 384]): ∀ (a a_1 a_2 : program), % 27.32/27.56 Or (Eq True False) % 27.32/27.56 (Or (Eq (outputs (skS.0 6 a) good) True) % 27.32/27.56 (Or (Eq (halts3 a_1 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) False) % 27.32/27.56 (Or (Eq (outputs a_1 good) False) (Eq (outputs a_1 bad) False)))) % 27.32/27.56 Clause #590 (by clausification #[571]): ∀ (a a_1 a_2 : program), % 27.32/27.56 Or (Eq (outputs (skS.0 6 a) good) True) % 27.32/27.56 (Or (Eq (halts3 a_1 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) False) % 27.32/27.56 (Or (Eq (outputs a_1 good) False) (Eq (outputs a_1 bad) False))) % 27.32/27.56 Clause #592 (by superposition #[590, 87]): ∀ (a a_1 a_2 : program), % 27.32/27.56 Or (Eq (outputs (skS.0 6 a) good) True) % 27.32/27.56 (Or (Eq (outputs (skS.0 1 a_1) good) False) % 27.32/27.56 (Or (Eq (outputs (skS.0 1 a_1) bad) False) % 27.32/27.56 (Or (Eq (halts2 (skS.0 7 (skS.0 1 a_1) a_2) (as_input (skS.0 7 (skS.0 1 a_1) a_2))) True) (Eq False True)))) % 27.32/27.56 Clause #601 (by clausification #[317]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.32/27.56 Or (Eq (halts2 a (as_input a)) True) % 27.32/27.56 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.32/27.56 (Eq (halts3 (skS.0 1 a_2) (skS.0 7 (skS.0 1 a_3) a_4) (as_input (skS.0 7 (skS.0 1 a_3) a_4))) True)) % 27.36/27.58 Clause #614 (by superposition #[601, 256]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.36/27.58 Or (Eq (halts2 a (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.36/27.58 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True) % 27.36/27.58 (Or (Eq True False) (Or (Eq (outputs (skS.0 1 a_4) good) False) (Eq (outputs (skS.0 1 a_4) bad) False)))))) % 27.36/27.58 Clause #666 (by clausification #[614]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.36/27.58 Or (Eq (halts2 a (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.36/27.58 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True) % 27.36/27.58 (Or (Eq (outputs (skS.0 1 a_4) good) False) (Eq (outputs (skS.0 1 a_4) bad) False))))) % 27.36/27.58 Clause #667 (by forward demodulation #[666, 240]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.36/27.58 Or (Eq (halts2 a (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.36/27.58 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True) % 27.36/27.58 (Or (Eq (outputs (skS.0 1 a_4) good) False) (Eq True False))))) % 27.36/27.58 Clause #668 (by clausification #[667]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.36/27.58 Or (Eq (halts2 a (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 a_2 (as_input a_2)) True) % 27.36/27.58 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True) (Eq (outputs (skS.0 1 a_4) good) False)))) % 27.36/27.58 Clause #669 (by superposition #[668, 374]): ∀ (a a_1 a_2 a_3 : program), % 27.36/27.58 Or (Eq (halts2 a (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 a_2 (as_input a_2)) True) (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True) (Eq False True)))) % 27.36/27.58 Clause #671 (by clausification #[669]): ∀ (a a_1 a_2 a_3 : program), % 27.36/27.58 Or (Eq (halts2 a (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 a_2 (as_input a_2)) True) (Eq (halts2 (skS.0 6 a_3) (as_input a_2)) True))) % 27.36/27.58 Clause #696 (by equality factoring #[671]): ∀ (a a_1 : program), % 27.36/27.58 Or (Eq (halts2 a (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 a (as_input a)) True) (Or (Ne True True) (Eq (halts2 (skS.0 6 a_1) (as_input a)) True))) % 27.36/27.58 Clause #697 (by clausification #[696]): ∀ (a a_1 : program), % 27.36/27.58 Or (Eq (halts2 a (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 a (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) (Or (Eq True False) (Eq True False)))) % 27.36/27.58 Clause #699 (by clausification #[697]): ∀ (a a_1 : program), % 27.36/27.58 Or (Eq (halts2 a (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 a (as_input a)) True) (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) (Eq True False))) % 27.36/27.58 Clause #700 (by clausification #[699]): ∀ (a a_1 : program), % 27.36/27.58 Or (Eq (halts2 a (as_input a)) True) % 27.36/27.58 (Or (Eq (halts2 a (as_input a)) True) (Eq (halts2 (skS.0 6 a_1) (as_input a)) True)) % 27.36/27.58 Clause #701 (by eliminate duplicate literals #[700]): ∀ (a a_1 : program), Or (Eq (halts2 a (as_input a)) True) (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.36/27.58 Clause #817 (by clausification #[459]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.36/27.58 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.36/27.58 (Or (Eq (halts2 (skS.0 4 a_1) (as_input a_2)) False) % 27.36/27.58 (Or (Eq (halts2 a_3 (as_input (skS.0 5 a_3 a_4))) False) % 27.36/27.58 (Or (Eq (outputs a_3 good) False) (Eq (halts2 (skS.0 5 a_3 a_4) (as_input (skS.0 5 a_3 a_4))) False)))) % 27.36/27.58 Clause #819 (by superposition #[817, 458]): ∀ (a a_1 a_2 a_3 : program), % 27.36/27.58 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.36/27.58 (Or (Eq (halts2 a_1 (as_input (skS.0 5 a_1 a_2))) False) % 27.36/27.58 (Or (Eq (outputs a_1 good) False) % 27.36/27.58 (Or (Eq (halts2 (skS.0 5 a_1 a_2) (as_input (skS.0 5 a_1 a_2))) False) % 27.36/27.58 (Or (Eq False True) (Eq (outputs (skS.0 6 a_3) bad) True))))) % 27.36/27.58 Clause #823 (by clausification #[819]): ∀ (a a_1 a_2 a_3 : program), % 27.36/27.58 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.36/27.58 (Or (Eq (halts2 a_1 (as_input (skS.0 5 a_1 a_2))) False) % 27.36/27.58 (Or (Eq (outputs a_1 good) False) % 27.36/27.58 (Or (Eq (halts2 (skS.0 5 a_1 a_2) (as_input (skS.0 5 a_1 a_2))) False) (Eq (outputs (skS.0 6 a_3) bad) True)))) % 27.36/27.61 Clause #859 (by clausification #[592]): ∀ (a a_1 a_2 : program), % 27.36/27.61 Or (Eq (outputs (skS.0 6 a) good) True) % 27.36/27.61 (Or (Eq (outputs (skS.0 1 a_1) good) False) % 27.36/27.61 (Or (Eq (outputs (skS.0 1 a_1) bad) False) % 27.36/27.61 (Eq (halts2 (skS.0 7 (skS.0 1 a_1) a_2) (as_input (skS.0 7 (skS.0 1 a_1) a_2))) True))) % 27.36/27.61 Clause #860 (by forward demodulation #[859, 374]): ∀ (a a_1 a_2 : program), % 27.36/27.61 Or (Eq (outputs (skS.0 6 a) good) True) % 27.36/27.61 (Or (Eq True False) % 27.36/27.61 (Or (Eq (outputs (skS.0 1 a_1) bad) False) % 27.36/27.61 (Eq (halts2 (skS.0 7 (skS.0 1 a_1) a_2) (as_input (skS.0 7 (skS.0 1 a_1) a_2))) True))) % 27.36/27.61 Clause #861 (by clausification #[860]): ∀ (a a_1 a_2 : program), % 27.36/27.61 Or (Eq (outputs (skS.0 6 a) good) True) % 27.36/27.61 (Or (Eq (outputs (skS.0 1 a_1) bad) False) % 27.36/27.61 (Eq (halts2 (skS.0 7 (skS.0 1 a_1) a_2) (as_input (skS.0 7 (skS.0 1 a_1) a_2))) True)) % 27.36/27.61 Clause #862 (by forward demodulation #[861, 240]): ∀ (a a_1 a_2 : program), % 27.36/27.61 Or (Eq (outputs (skS.0 6 a) good) True) % 27.36/27.61 (Or (Eq True False) (Eq (halts2 (skS.0 7 (skS.0 1 a_1) a_2) (as_input (skS.0 7 (skS.0 1 a_1) a_2))) True)) % 27.36/27.61 Clause #863 (by clausification #[862]): ∀ (a a_1 a_2 : program), % 27.36/27.61 Or (Eq (outputs (skS.0 6 a) good) True) % 27.36/27.61 (Eq (halts2 (skS.0 7 (skS.0 1 a_1) a_2) (as_input (skS.0 7 (skS.0 1 a_1) a_2))) True) % 27.36/27.61 Clause #869 (by superposition #[863, 88]): ∀ (a a_1 a_2 a_3 : program), % 27.36/27.61 Or (Eq (outputs (skS.0 6 a) good) True) % 27.36/27.61 (Or (Eq True False) % 27.36/27.61 (Eq (halts3 (skS.0 1 a_1) (skS.0 7 (skS.0 1 a_2) a_3) (as_input (skS.0 7 (skS.0 1 a_2) a_3))) True)) % 27.36/27.61 Clause #870 (by clausification #[869]): ∀ (a a_1 a_2 a_3 : program), % 27.36/27.61 Or (Eq (outputs (skS.0 6 a) good) True) % 27.36/27.61 (Eq (halts3 (skS.0 1 a_1) (skS.0 7 (skS.0 1 a_2) a_3) (as_input (skS.0 7 (skS.0 1 a_2) a_3))) True) % 27.36/27.61 Clause #872 (by superposition #[870, 590]): ∀ (a a_1 a_2 : program), % 27.36/27.61 Or (Eq (outputs (skS.0 6 a) good) True) % 27.36/27.61 (Or (Eq (outputs (skS.0 6 a_1) good) True) % 27.36/27.61 (Or (Eq True False) (Or (Eq (outputs (skS.0 1 a_2) good) False) (Eq (outputs (skS.0 1 a_2) bad) False)))) % 27.36/27.61 Clause #875 (by clausification #[872]): ∀ (a a_1 a_2 : program), % 27.36/27.61 Or (Eq (outputs (skS.0 6 a) good) True) % 27.36/27.61 (Or (Eq (outputs (skS.0 6 a_1) good) True) % 27.36/27.61 (Or (Eq (outputs (skS.0 1 a_2) good) False) (Eq (outputs (skS.0 1 a_2) bad) False))) % 27.36/27.61 Clause #876 (by forward demodulation #[875, 240]): ∀ (a a_1 a_2 : program), % 27.36/27.61 Or (Eq (outputs (skS.0 6 a) good) True) % 27.36/27.61 (Or (Eq (outputs (skS.0 6 a_1) good) True) (Or (Eq (outputs (skS.0 1 a_2) good) False) (Eq True False))) % 27.36/27.61 Clause #877 (by clausification #[876]): ∀ (a a_1 a_2 : program), % 27.36/27.61 Or (Eq (outputs (skS.0 6 a) good) True) % 27.36/27.61 (Or (Eq (outputs (skS.0 6 a_1) good) True) (Eq (outputs (skS.0 1 a_2) good) False)) % 27.36/27.61 Clause #878 (by superposition #[877, 374]): ∀ (a a_1 : program), Or (Eq (outputs (skS.0 6 a) good) True) (Or (Eq (outputs (skS.0 6 a_1) good) True) (Eq False True)) % 27.36/27.61 Clause #880 (by clausification #[878]): ∀ (a a_1 : program), Or (Eq (outputs (skS.0 6 a) good) True) (Eq (outputs (skS.0 6 a_1) good) True) % 27.36/27.61 Clause #881 (by equality factoring #[880]): ∀ (a : program), Or (Ne True True) (Eq (outputs (skS.0 6 a) good) True) % 27.36/27.61 Clause #882 (by clausification #[881]): ∀ (a : program), Or (Eq (outputs (skS.0 6 a) good) True) (Or (Eq True False) (Eq True False)) % 27.36/27.61 Clause #884 (by clausification #[882]): ∀ (a : program), Or (Eq (outputs (skS.0 6 a) good) True) (Eq True False) % 27.36/27.61 Clause #885 (by clausification #[884]): ∀ (a : program), Eq (outputs (skS.0 6 a) good) True % 27.36/27.61 Clause #933 (by clausification #[381]): ∀ (a a_1 a_2 a_3 : program), % 27.36/27.61 Or (Eq (halts2 a (as_input a)) False) % 27.36/27.61 (Or (Eq (And (halts3 a_1 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) (outputs a_1 bad)) False) % 27.36/27.61 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a)) True) % 27.36/27.61 (Or (Eq (halts3 a_1 (skS.0 7 a_1 a_2) (as_input (skS.0 7 a_1 a_2))) False) (Eq (outputs a_1 good) False)))) % 27.36/27.61 Clause #934 (by clausification #[933]): ∀ (a a_1 a_2 a_3 : program), % 27.36/27.61 Or (Eq (halts2 a (as_input a)) False) % 27.36/27.61 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.36/27.61 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) % 27.42/27.63 (Or (Eq (outputs a_2 good) False) % 27.42/27.63 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) (Eq (outputs a_2 bad) False))))) % 27.42/27.63 Clause #935 (by eliminate duplicate literals #[934]): ∀ (a a_1 a_2 a_3 : program), % 27.42/27.63 Or (Eq (halts2 a (as_input a)) False) % 27.42/27.63 (Or (Eq (halts2 (skS.0 6 a_1) (as_input a)) True) % 27.42/27.63 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) % 27.42/27.63 (Or (Eq (outputs a_2 good) False) (Eq (outputs a_2 bad) False)))) % 27.42/27.63 Clause #939 (by superposition #[935, 458]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.63 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.42/27.63 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) % 27.42/27.63 (Or (Eq (outputs a_2 good) False) % 27.42/27.63 (Or (Eq (outputs a_2 bad) False) (Or (Eq False True) (Eq (outputs (skS.0 6 a_4) bad) True))))) % 27.42/27.63 Clause #940 (by superposition #[935, 701]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.63 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.42/27.63 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) % 27.42/27.63 (Or (Eq (outputs a_2 good) False) % 27.42/27.63 (Or (Eq (outputs a_2 bad) False) (Or (Eq False True) (Eq (halts2 (skS.0 6 a_4) (as_input a_1)) True))))) % 27.42/27.63 Clause #962 (by clausification #[939]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.63 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.42/27.63 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) % 27.42/27.63 (Or (Eq (outputs a_2 good) False) (Or (Eq (outputs a_2 bad) False) (Eq (outputs (skS.0 6 a_4) bad) True)))) % 27.42/27.63 Clause #963 (by superposition #[962, 466]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.63 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.42/27.63 (Or (Eq (outputs (skS.0 1 a_2) good) False) % 27.42/27.63 (Or (Eq (outputs (skS.0 1 a_2) bad) False) % 27.42/27.63 (Or (Eq (outputs (skS.0 6 a_3) bad) True) (Or (Eq (outputs (skS.0 6 a_4) bad) True) (Eq False True))))) % 27.42/27.63 Clause #967 (by clausification #[963]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.63 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.42/27.63 (Or (Eq (outputs (skS.0 1 a_2) good) False) % 27.42/27.63 (Or (Eq (outputs (skS.0 1 a_2) bad) False) % 27.42/27.63 (Or (Eq (outputs (skS.0 6 a_3) bad) True) (Eq (outputs (skS.0 6 a_4) bad) True)))) % 27.42/27.63 Clause #968 (by forward demodulation #[967, 240]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.63 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.42/27.63 (Or (Eq (outputs (skS.0 1 a_2) good) False) % 27.42/27.63 (Or (Eq True False) (Or (Eq (outputs (skS.0 6 a_3) bad) True) (Eq (outputs (skS.0 6 a_4) bad) True)))) % 27.42/27.63 Clause #969 (by clausification #[968]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.63 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.42/27.63 (Or (Eq (outputs (skS.0 1 a_2) good) False) % 27.42/27.63 (Or (Eq (outputs (skS.0 6 a_3) bad) True) (Eq (outputs (skS.0 6 a_4) bad) True))) % 27.42/27.63 Clause #970 (by superposition #[969, 374]): ∀ (a a_1 a_2 a_3 : program), % 27.42/27.63 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.42/27.63 (Or (Eq (outputs (skS.0 6 a_2) bad) True) (Or (Eq (outputs (skS.0 6 a_3) bad) True) (Eq False True))) % 27.42/27.63 Clause #972 (by clausification #[970]): ∀ (a a_1 a_2 a_3 : program), % 27.42/27.63 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.42/27.63 (Or (Eq (outputs (skS.0 6 a_2) bad) True) (Eq (outputs (skS.0 6 a_3) bad) True)) % 27.42/27.63 Clause #993 (by equality factoring #[972]): ∀ (a a_1 a_2 : program), % 27.42/27.63 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) (Or (Ne True True) (Eq (outputs (skS.0 6 a_2) bad) True)) % 27.42/27.63 Clause #994 (by clausification #[993]): ∀ (a a_1 a_2 : program), % 27.42/27.63 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.42/27.63 (Or (Eq (outputs (skS.0 6 a_2) bad) True) (Or (Eq True False) (Eq True False))) % 27.42/27.63 Clause #996 (by clausification #[994]): ∀ (a a_1 a_2 : program), % 27.42/27.63 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) (Or (Eq (outputs (skS.0 6 a_2) bad) True) (Eq True False)) % 27.42/27.63 Clause #997 (by clausification #[996]): ∀ (a a_1 a_2 : program), Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) (Eq (outputs (skS.0 6 a_2) bad) True) % 27.42/27.63 Clause #1007 (by superposition #[997, 823]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.63 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.42/27.63 (Or (Eq (outputs (skS.0 6 a_1) bad) True) % 27.42/27.63 (Or (Eq True False) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_2) good) False) % 27.42/27.66 (Or (Eq (halts2 (skS.0 5 (skS.0 6 a_2) a_3) (as_input (skS.0 5 (skS.0 6 a_2) a_3))) False) % 27.42/27.66 (Eq (outputs (skS.0 6 a_4) bad) True))))) % 27.42/27.66 Clause #1031 (by clausification #[940]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.66 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.42/27.66 (Or (Eq (halts3 a_2 (skS.0 7 a_2 a_3) (as_input (skS.0 7 a_2 a_3))) False) % 27.42/27.66 (Or (Eq (outputs a_2 good) False) % 27.42/27.66 (Or (Eq (outputs a_2 bad) False) (Eq (halts2 (skS.0 6 a_4) (as_input a_1)) True)))) % 27.42/27.66 Clause #1035 (by superposition #[1031, 87]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.66 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 1 a_2) good) False) % 27.42/27.66 (Or (Eq (outputs (skS.0 1 a_2) bad) False) % 27.42/27.66 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_1)) True) % 27.42/27.66 (Or (Eq (halts2 (skS.0 7 (skS.0 1 a_2) a_4) (as_input (skS.0 7 (skS.0 1 a_2) a_4))) True) (Eq False True))))) % 27.42/27.66 Clause #1302 (by clausification #[1007]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.66 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_1) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_2) good) False) % 27.42/27.66 (Or (Eq (halts2 (skS.0 5 (skS.0 6 a_2) a_3) (as_input (skS.0 5 (skS.0 6 a_2) a_3))) False) % 27.42/27.66 (Eq (outputs (skS.0 6 a_4) bad) True)))) % 27.42/27.66 Clause #1303 (by forward demodulation #[1302, 885]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.66 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_1) bad) True) % 27.42/27.66 (Or (Eq True False) % 27.42/27.66 (Or (Eq (halts2 (skS.0 5 (skS.0 6 a_2) a_3) (as_input (skS.0 5 (skS.0 6 a_2) a_3))) False) % 27.42/27.66 (Eq (outputs (skS.0 6 a_4) bad) True)))) % 27.42/27.66 Clause #1304 (by clausification #[1303]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.42/27.66 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_1) bad) True) % 27.42/27.66 (Or (Eq (halts2 (skS.0 5 (skS.0 6 a_2) a_3) (as_input (skS.0 5 (skS.0 6 a_2) a_3))) False) % 27.42/27.66 (Eq (outputs (skS.0 6 a_4) bad) True))) % 27.42/27.66 Clause #1306 (by superposition #[1304, 458]): ∀ (a a_1 a_2 a_3 : program), % 27.42/27.66 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_1) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_2) bad) True) (Or (Eq False True) (Eq (outputs (skS.0 6 a_3) bad) True)))) % 27.42/27.66 Clause #1309 (by clausification #[1306]): ∀ (a a_1 a_2 a_3 : program), % 27.42/27.66 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_1) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_2) bad) True) (Eq (outputs (skS.0 6 a_3) bad) True))) % 27.42/27.66 Clause #1311 (by equality factoring #[1309]): ∀ (a a_1 a_2 : program), % 27.42/27.66 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_1) bad) True) (Or (Ne True True) (Eq (outputs (skS.0 6 a_2) bad) True))) % 27.42/27.66 Clause #1313 (by clausification #[1311]): ∀ (a a_1 a_2 : program), % 27.42/27.66 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_1) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_2) bad) True) (Or (Eq True False) (Eq True False)))) % 27.42/27.66 Clause #1315 (by clausification #[1313]): ∀ (a a_1 a_2 : program), % 27.42/27.66 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_1) bad) True) (Or (Eq (outputs (skS.0 6 a_2) bad) True) (Eq True False))) % 27.42/27.66 Clause #1316 (by clausification #[1315]): ∀ (a a_1 a_2 : program), % 27.42/27.66 Or (Eq (outputs (skS.0 6 a) bad) True) % 27.42/27.66 (Or (Eq (outputs (skS.0 6 a_1) bad) True) (Eq (outputs (skS.0 6 a_2) bad) True)) % 27.42/27.66 Clause #1317 (by equality factoring #[1316]): ∀ (a a_1 : program), Or (Eq (outputs (skS.0 6 a) bad) True) (Or (Ne True True) (Eq (outputs (skS.0 6 a_1) bad) True)) % 27.42/27.66 Clause #1318 (by clausification #[1317]): ∀ (a a_1 : program), % 27.42/27.66 Or (Eq (outputs (skS.0 6 a) bad) True) (Or (Eq (outputs (skS.0 6 a_1) bad) True) (Or (Eq True False) (Eq True False))) % 27.42/27.66 Clause #1320 (by clausification #[1318]): ∀ (a a_1 : program), Or (Eq (outputs (skS.0 6 a) bad) True) (Or (Eq (outputs (skS.0 6 a_1) bad) True) (Eq True False)) % 27.42/27.66 Clause #1321 (by clausification #[1320]): ∀ (a a_1 : program), Or (Eq (outputs (skS.0 6 a) bad) True) (Eq (outputs (skS.0 6 a_1) bad) True) % 27.42/27.66 Clause #1322 (by equality factoring #[1321]): ∀ (a : program), Or (Ne True True) (Eq (outputs (skS.0 6 a) bad) True) % 27.46/27.68 Clause #1323 (by clausification #[1322]): ∀ (a : program), Or (Eq (outputs (skS.0 6 a) bad) True) (Or (Eq True False) (Eq True False)) % 27.46/27.68 Clause #1325 (by clausification #[1323]): ∀ (a : program), Or (Eq (outputs (skS.0 6 a) bad) True) (Eq True False) % 27.46/27.68 Clause #1326 (by clausification #[1325]): ∀ (a : program), Eq (outputs (skS.0 6 a) bad) True % 27.46/27.68 Clause #1382 (by clausification #[1035]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.68 (Or (Eq (outputs (skS.0 1 a_2) good) False) % 27.46/27.68 (Or (Eq (outputs (skS.0 1 a_2) bad) False) % 27.46/27.68 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_1)) True) % 27.46/27.68 (Eq (halts2 (skS.0 7 (skS.0 1 a_2) a_4) (as_input (skS.0 7 (skS.0 1 a_2) a_4))) True)))) % 27.46/27.68 Clause #1383 (by forward demodulation #[1382, 374]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.68 (Or (Eq True False) % 27.46/27.68 (Or (Eq (outputs (skS.0 1 a_2) bad) False) % 27.46/27.68 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_1)) True) % 27.46/27.68 (Eq (halts2 (skS.0 7 (skS.0 1 a_2) a_4) (as_input (skS.0 7 (skS.0 1 a_2) a_4))) True)))) % 27.46/27.68 Clause #1384 (by clausification #[1383]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.68 (Or (Eq (outputs (skS.0 1 a_2) bad) False) % 27.46/27.68 (Or (Eq (halts2 (skS.0 6 a_3) (as_input a_1)) True) % 27.46/27.68 (Eq (halts2 (skS.0 7 (skS.0 1 a_2) a_4) (as_input (skS.0 7 (skS.0 1 a_2) a_4))) True))) % 27.46/27.68 Clause #1385 (by forward demodulation #[1384, 240]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.68 (Or (Eq True False) % 27.46/27.68 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_1)) True) % 27.46/27.68 (Eq (halts2 (skS.0 7 (skS.0 1 a_3) a_4) (as_input (skS.0 7 (skS.0 1 a_3) a_4))) True))) % 27.46/27.68 Clause #1386 (by clausification #[1385]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.68 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_1)) True) % 27.46/27.68 (Eq (halts2 (skS.0 7 (skS.0 1 a_3) a_4) (as_input (skS.0 7 (skS.0 1 a_3) a_4))) True)) % 27.46/27.68 Clause #1412 (by equality factoring #[1386]): ∀ (a a_1 a_2 a_3 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.46/27.68 (Or (Ne True True) (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True)) % 27.46/27.68 Clause #1413 (by clausification #[1412]): ∀ (a a_1 a_2 a_3 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.46/27.68 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True) (Or (Eq True False) (Eq True False))) % 27.46/27.68 Clause #1415 (by clausification #[1413]): ∀ (a a_1 a_2 a_3 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.46/27.68 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True) (Eq True False)) % 27.46/27.68 Clause #1416 (by clausification #[1415]): ∀ (a a_1 a_2 a_3 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 7 (skS.0 1 a) a_1) (as_input (skS.0 7 (skS.0 1 a) a_1))) True) % 27.46/27.68 (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True) % 27.46/27.68 Clause #1423 (by superposition #[1416, 88]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.68 (Or (Eq True False) % 27.46/27.68 (Eq (halts3 (skS.0 1 a_2) (skS.0 7 (skS.0 1 a_3) a_4) (as_input (skS.0 7 (skS.0 1 a_3) a_4))) True)) % 27.46/27.68 Clause #1445 (by clausification #[1423]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.68 (Eq (halts3 (skS.0 1 a_2) (skS.0 7 (skS.0 1 a_3) a_4) (as_input (skS.0 7 (skS.0 1 a_3) a_4))) True) % 27.46/27.68 Clause #1459 (by superposition #[1445, 1031]): ∀ (a a_1 a_2 a_3 a_4 a_5 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.68 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True) % 27.46/27.68 (Or (Eq True False) % 27.46/27.68 (Or (Eq (outputs (skS.0 1 a_4) good) False) % 27.46/27.68 (Or (Eq (outputs (skS.0 1 a_4) bad) False) (Eq (halts2 (skS.0 6 a_5) (as_input a_3)) True))))) % 27.46/27.68 Clause #1463 (by clausification #[1459]): ∀ (a a_1 a_2 a_3 a_4 a_5 : program), % 27.46/27.68 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.68 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True) % 27.46/27.68 (Or (Eq (outputs (skS.0 1 a_4) good) False) % 27.46/27.71 (Or (Eq (outputs (skS.0 1 a_4) bad) False) (Eq (halts2 (skS.0 6 a_5) (as_input a_3)) True)))) % 27.46/27.71 Clause #1464 (by forward demodulation #[1463, 240]): ∀ (a a_1 a_2 a_3 a_4 a_5 : program), % 27.46/27.71 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.71 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True) % 27.46/27.71 (Or (Eq (outputs (skS.0 1 a_4) good) False) (Or (Eq True False) (Eq (halts2 (skS.0 6 a_5) (as_input a_3)) True)))) % 27.46/27.71 Clause #1465 (by clausification #[1464]): ∀ (a a_1 a_2 a_3 a_4 a_5 : program), % 27.46/27.71 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.71 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True) % 27.46/27.71 (Or (Eq (outputs (skS.0 1 a_4) good) False) (Eq (halts2 (skS.0 6 a_5) (as_input a_3)) True))) % 27.46/27.71 Clause #1466 (by superposition #[1465, 374]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.46/27.71 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.71 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True) % 27.46/27.71 (Or (Eq (halts2 (skS.0 6 a_4) (as_input a_3)) True) (Eq False True))) % 27.46/27.71 Clause #1467 (by clausification #[1466]): ∀ (a a_1 a_2 a_3 a_4 : program), % 27.46/27.71 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.71 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True) (Eq (halts2 (skS.0 6 a_4) (as_input a_3)) True)) % 27.46/27.71 Clause #1505 (by equality factoring #[1467]): ∀ (a a_1 a_2 a_3 : program), % 27.46/27.71 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) (Or (Ne True True) (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True)) % 27.46/27.71 Clause #1506 (by clausification #[1505]): ∀ (a a_1 a_2 a_3 : program), % 27.46/27.71 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.71 (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True) (Or (Eq True False) (Eq True False))) % 27.46/27.71 Clause #1508 (by clausification #[1506]): ∀ (a a_1 a_2 a_3 : program), % 27.46/27.71 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) (Or (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True) (Eq True False)) % 27.46/27.71 Clause #1509 (by clausification #[1508]): ∀ (a a_1 a_2 a_3 : program), % 27.46/27.71 Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) (Eq (halts2 (skS.0 6 a_2) (as_input a_3)) True) % 27.46/27.71 Clause #1525 (by equality factoring #[1509]): ∀ (a a_1 : program), Or (Ne True True) (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) % 27.46/27.71 Clause #1527 (by clausification #[1525]): ∀ (a a_1 : program), Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) (Or (Eq True False) (Eq True False)) % 27.46/27.71 Clause #1529 (by clausification #[1527]): ∀ (a a_1 : program), Or (Eq (halts2 (skS.0 6 a) (as_input a_1)) True) (Eq True False) % 27.46/27.71 Clause #1530 (by clausification #[1529]): ∀ (a a_1 : program), Eq (halts2 (skS.0 6 a) (as_input a_1)) True % 27.46/27.71 Clause #1536 (by superposition #[1530, 179]): ∀ (a a_1 a_2 : program), % 27.46/27.71 Or (Eq (halts2 a (as_input a)) True) % 27.46/27.71 (Or (Eq (halts2 (skS.0 4 a_1) (as_input a)) True) % 27.46/27.71 (Or (Eq True False) (Or (Eq (outputs (skS.0 6 a_2) good) False) (Eq (outputs (skS.0 6 a_2) bad) False)))) % 27.46/27.71 Clause #1557 (by clausification #[1536]): ∀ (a a_1 a_2 : program), % 27.46/27.71 Or (Eq (halts2 a (as_input a)) True) % 27.46/27.71 (Or (Eq (halts2 (skS.0 4 a_1) (as_input a)) True) % 27.46/27.71 (Or (Eq (outputs (skS.0 6 a_2) good) False) (Eq (outputs (skS.0 6 a_2) bad) False))) % 27.46/27.71 Clause #1558 (by forward demodulation #[1557, 1326]): ∀ (a a_1 a_2 : program), % 27.46/27.71 Or (Eq (halts2 a (as_input a)) True) % 27.46/27.71 (Or (Eq (halts2 (skS.0 4 a_1) (as_input a)) True) (Or (Eq (outputs (skS.0 6 a_2) good) False) (Eq True False))) % 27.46/27.71 Clause #1559 (by clausification #[1558]): ∀ (a a_1 a_2 : program), % 27.46/27.71 Or (Eq (halts2 a (as_input a)) True) % 27.46/27.71 (Or (Eq (halts2 (skS.0 4 a_1) (as_input a)) True) (Eq (outputs (skS.0 6 a_2) good) False)) % 27.46/27.71 Clause #1560 (by superposition #[1559, 885]): ∀ (a a_1 : program), % 27.46/27.71 Or (Eq (halts2 a (as_input a)) True) (Or (Eq (halts2 (skS.0 4 a_1) (as_input a)) True) (Eq False True)) % 27.46/27.71 Clause #1561 (by clausification #[1560]): ∀ (a a_1 : program), Or (Eq (halts2 a (as_input a)) True) (Eq (halts2 (skS.0 4 a_1) (as_input a)) True) % 27.46/27.71 Clause #1570 (by equality factoring #[1561]): ∀ (a : program), Or (Ne True True) (Eq (halts2 (skS.0 4 a) (as_input (skS.0 4 a))) True) % 27.46/27.71 Clause #1571 (by clausification #[1570]): ∀ (a : program), Or (Eq (halts2 (skS.0 4 a) (as_input (skS.0 4 a))) True) (Or (Eq True False) (Eq True False)) % 27.46/27.72 Clause #1573 (by clausification #[1571]): ∀ (a : program), Or (Eq (halts2 (skS.0 4 a) (as_input (skS.0 4 a))) True) (Eq True False) % 27.46/27.72 Clause #1574 (by clausification #[1573]): ∀ (a : program), Eq (halts2 (skS.0 4 a) (as_input (skS.0 4 a))) True % 27.46/27.72 Clause #1576 (by superposition #[1574, 110]): ∀ (a a_1 a_2 a_3 : program), % 27.46/27.72 Or (Eq True False) % 27.46/27.72 (Or (Eq (halts2 (skS.0 4 a) (as_input (skS.0 4 a_1))) False) % 27.46/27.72 (Or (Eq (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) False) % 27.46/27.72 (Or (Eq (outputs a_2 good) False) (Eq (outputs a_2 bad) False)))) % 27.46/27.72 Clause #1598 (by clausification #[1576]): ∀ (a a_1 a_2 a_3 : program), % 27.46/27.72 Or (Eq (halts2 (skS.0 4 a) (as_input (skS.0 4 a_1))) False) % 27.46/27.72 (Or (Eq (halts2 a_2 (as_input (skS.0 5 a_2 a_3))) False) % 27.46/27.72 (Or (Eq (outputs a_2 good) False) (Eq (outputs a_2 bad) False))) % 27.46/27.72 Clause #1600 (by superposition #[1598, 1574]): ∀ (a a_1 : program), % 27.46/27.72 Or (Eq (halts2 a (as_input (skS.0 5 a a_1))) False) % 27.46/27.72 (Or (Eq (outputs a good) False) (Or (Eq (outputs a bad) False) (Eq False True))) % 27.46/27.72 Clause #1605 (by clausification #[1600]): ∀ (a a_1 : program), % 27.46/27.72 Or (Eq (halts2 a (as_input (skS.0 5 a a_1))) False) (Or (Eq (outputs a good) False) (Eq (outputs a bad) False)) % 27.46/27.72 Clause #1606 (by superposition #[1605, 1530]): ∀ (a : program), Or (Eq (outputs (skS.0 6 a) good) False) (Or (Eq (outputs (skS.0 6 a) bad) False) (Eq False True)) % 27.46/27.72 Clause #1607 (by clausification #[1606]): ∀ (a : program), Or (Eq (outputs (skS.0 6 a) good) False) (Eq (outputs (skS.0 6 a) bad) False) % 27.46/27.72 Clause #1608 (by forward demodulation #[1607, 1326]): ∀ (a : program), Or (Eq (outputs (skS.0 6 a) good) False) (Eq True False) % 27.46/27.72 Clause #1609 (by clausification #[1608]): ∀ (a : program), Eq (outputs (skS.0 6 a) good) False % 27.46/27.72 Clause #1610 (by superposition #[1609, 885]): Eq False True % 27.46/27.72 Clause #1611 (by clausification #[1610]): False % 27.46/27.72 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------