%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO500^1.002 : TPTP v9.2.0. Released v4.1.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 08:09:11 PM UTC 2025 % Result : Theorem 3.82s 3.99s % Output : Proof 4.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYO500^1.002 : TPTP v9.2.0. Released v4.1.0. % 0.03/0.14 % Command : duper %s % 0.14/0.35 % Computer : n008.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Fri Oct 3 13:16:23 EDT 2025 % 0.14/0.35 % CPUTime : % 3.82/3.99 SZS status Theorem for theBenchmark.p % 3.82/3.99 SZS output start Proof for theBenchmark.p % 3.82/3.99 Clause #0 (by assumption #[]): Eq (Not (Eq (f0 (f0 (f0 (f1 x)))) (f0 (f1 (f1 (f1 x)))))) True % 3.82/3.99 Clause #1 (by clausification #[0]): Eq (Eq (f0 (f0 (f0 (f1 x)))) (f0 (f1 (f1 (f1 x))))) False % 3.82/3.99 Clause #2 (by clausification #[1]): Ne (f0 (f0 (f0 (f1 x)))) (f0 (f1 (f1 (f1 x)))) % 3.82/3.99 Clause #3 (by clausification #[2]): Or (Eq (f0 (f0 (f0 (f1 x)))) False) (Eq (f0 (f1 (f1 (f1 x)))) False) % 3.82/3.99 Clause #4 (by clausification #[2]): Or (Eq (f0 (f0 (f0 (f1 x)))) True) (Eq (f0 (f1 (f1 (f1 x)))) True) % 3.82/3.99 Clause #5 (by identity loobHoist #[3]): Or (Eq (f0 (f1 (f1 (f1 x)))) False) (Or (Eq (f0 True) False) (Eq (f0 (f0 (f1 x))) False)) % 3.82/3.99 Clause #6 (by identity boolHoist #[3]): Or (Eq (f0 (f1 (f1 (f1 x)))) False) (Or (Eq (f0 False) False) (Eq (f0 (f0 (f1 x))) True)) % 3.82/3.99 Clause #7 (by identity loobHoist #[5]): Or (Eq (f0 True) False) (Or (Eq (f0 (f0 (f1 x))) False) (Or (Eq (f0 True) False) (Eq (f1 (f1 (f1 x))) False))) % 3.82/3.99 Clause #8 (by identity boolHoist #[5]): Or (Eq (f0 True) False) (Or (Eq (f0 (f0 (f1 x))) False) (Or (Eq (f0 False) False) (Eq (f1 (f1 (f1 x))) True))) % 3.82/3.99 Clause #9 (by eliminate duplicate literals #[7]): Or (Eq (f0 True) False) (Or (Eq (f0 (f0 (f1 x))) False) (Eq (f1 (f1 (f1 x))) False)) % 3.82/3.99 Clause #10 (by identity loobHoist #[9]): Or (Eq (f0 True) False) (Or (Eq (f1 (f1 (f1 x))) False) (Or (Eq (f0 True) False) (Eq (f0 (f1 x)) False))) % 3.82/3.99 Clause #12 (by eliminate duplicate literals #[10]): Or (Eq (f0 True) False) (Or (Eq (f1 (f1 (f1 x))) False) (Eq (f0 (f1 x)) False)) % 3.82/3.99 Clause #13 (by identity loobHoist #[12]): Or (Eq (f0 True) False) (Or (Eq (f0 (f1 x)) False) (Or (Eq (f1 True) False) (Eq (f1 (f1 x)) False))) % 3.82/3.99 Clause #14 (by identity boolHoist #[12]): Or (Eq (f0 True) False) (Or (Eq (f0 (f1 x)) False) (Or (Eq (f1 False) False) (Eq (f1 (f1 x)) True))) % 3.82/3.99 Clause #15 (by identity loobHoist #[13]): Or (Eq (f0 True) False) % 3.82/3.99 (Or (Eq (f1 True) False) (Or (Eq (f1 (f1 x)) False) (Or (Eq (f0 True) False) (Eq (f1 x) False)))) % 3.82/3.99 Clause #17 (by eliminate duplicate literals #[15]): Or (Eq (f0 True) False) (Or (Eq (f1 True) False) (Or (Eq (f1 (f1 x)) False) (Eq (f1 x) False))) % 3.82/3.99 Clause #18 (by identity loobHoist #[17]): Or (Eq (f0 True) False) (Or (Eq (f1 True) False) (Or (Eq (f1 x) False) (Or (Eq (f1 True) False) (Eq (f1 x) False)))) % 3.82/3.99 Clause #20 (by eliminate duplicate literals #[18]): Or (Eq (f0 True) False) (Or (Eq (f1 True) False) (Eq (f1 x) False)) % 3.82/3.99 Clause #21 (by identity loobHoist #[20]): Or (Eq (f0 True) False) (Or (Eq (f1 True) False) (Or (Eq (f1 True) False) (Eq x False))) % 3.82/3.99 Clause #22 (by identity boolHoist #[20]): Or (Eq (f0 True) False) (Or (Eq (f1 True) False) (Or (Eq (f1 False) False) (Eq x True))) % 3.82/3.99 Clause #23 (by eliminate duplicate literals #[21]): Or (Eq (f0 True) False) (Or (Eq (f1 True) False) (Eq x False)) % 3.82/3.99 Clause #24 (by identity loobHoist #[4]): Or (Eq (f0 (f1 (f1 (f1 x)))) True) (Or (Eq (f0 True) True) (Eq (f0 (f0 (f1 x))) False)) % 3.82/3.99 Clause #25 (by identity boolHoist #[4]): Or (Eq (f0 (f1 (f1 (f1 x)))) True) (Or (Eq (f0 False) True) (Eq (f0 (f0 (f1 x))) True)) % 3.82/3.99 Clause #26 (by identity loobHoist #[24]): Or (Eq (f0 True) True) (Or (Eq (f0 (f0 (f1 x))) False) (Or (Eq (f0 True) True) (Eq (f1 (f1 (f1 x))) False))) % 3.82/3.99 Clause #28 (by eliminate duplicate literals #[26]): Or (Eq (f0 True) True) (Or (Eq (f0 (f0 (f1 x))) False) (Eq (f1 (f1 (f1 x))) False)) % 3.82/3.99 Clause #30 (by identity boolHoist #[28]): Or (Eq (f0 True) True) (Or (Eq (f1 (f1 (f1 x))) False) (Or (Eq (f0 False) False) (Eq (f0 (f1 x)) True))) % 3.82/3.99 Clause #31 (by identity loobHoist #[14]): Or (Eq (f0 True) False) % 3.82/3.99 (Or (Eq (f1 False) False) (Or (Eq (f1 (f1 x)) True) (Or (Eq (f0 True) False) (Eq (f1 x) False)))) % 3.82/3.99 Clause #33 (by eliminate duplicate literals #[31]): Or (Eq (f0 True) False) (Or (Eq (f1 False) False) (Or (Eq (f1 (f1 x)) True) (Eq (f1 x) False))) % 3.82/3.99 Clause #34 (by identity loobHoist #[33]): Or (Eq (f0 True) False) (Or (Eq (f1 False) False) (Or (Eq (f1 x) False) (Or (Eq (f1 True) True) (Eq (f1 x) False)))) % 3.82/3.99 Clause #36 (by eliminate duplicate literals #[34]): Or (Eq (f0 True) False) (Or (Eq (f1 False) False) (Or (Eq (f1 x) False) (Eq (f1 True) True))) % 3.82/4.02 Clause #38 (by identity boolHoist #[36]): Or (Eq (f0 True) False) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Eq x True)))) % 3.82/4.02 Clause #39 (by eliminate duplicate literals #[38]): Or (Eq (f0 True) False) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Eq x True))) % 3.82/4.02 Clause #41 (by identity boolHoist #[6]): Or (Eq (f0 False) False) (Or (Eq (f0 (f0 (f1 x))) True) (Or (Eq (f0 False) False) (Eq (f1 (f1 (f1 x))) True))) % 3.82/4.02 Clause #44 (by identity loobHoist #[25]): Or (Eq (f0 False) True) (Or (Eq (f0 (f0 (f1 x))) True) (Or (Eq (f0 True) True) (Eq (f1 (f1 (f1 x))) False))) % 3.82/4.02 Clause #45 (by identity boolHoist #[25]): Or (Eq (f0 False) True) (Or (Eq (f0 (f0 (f1 x))) True) (Or (Eq (f0 False) True) (Eq (f1 (f1 (f1 x))) True))) % 3.82/4.02 Clause #47 (by identity boolHoist #[44]): Or (Eq (f0 False) True) % 3.82/4.02 (Or (Eq (f0 True) True) (Or (Eq (f1 (f1 (f1 x))) False) (Or (Eq (f0 False) True) (Eq (f0 (f1 x)) True)))) % 3.82/4.02 Clause #53 (by identity loobHoist #[30]): Or (Eq (f0 True) True) % 3.82/4.02 (Or (Eq (f0 False) False) (Or (Eq (f0 (f1 x)) True) (Or (Eq (f1 True) False) (Eq (f1 (f1 x)) False)))) % 3.82/4.02 Clause #54 (by identity boolHoist #[30]): Or (Eq (f0 True) True) % 3.82/4.02 (Or (Eq (f0 False) False) (Or (Eq (f0 (f1 x)) True) (Or (Eq (f1 False) False) (Eq (f1 (f1 x)) True)))) % 3.82/4.02 Clause #55 (by identity loobHoist #[53]): Or (Eq (f0 True) True) % 3.82/4.02 (Or (Eq (f0 False) False) % 3.82/4.02 (Or (Eq (f1 True) False) (Or (Eq (f1 (f1 x)) False) (Or (Eq (f0 True) True) (Eq (f1 x) False))))) % 3.82/4.02 Clause #57 (by eliminate duplicate literals #[55]): Or (Eq (f0 True) True) % 3.82/4.02 (Or (Eq (f0 False) False) (Or (Eq (f1 True) False) (Or (Eq (f1 (f1 x)) False) (Eq (f1 x) False)))) % 3.82/4.02 Clause #58 (by identity loobHoist #[57]): Or (Eq (f0 True) True) % 3.82/4.02 (Or (Eq (f0 False) False) % 3.82/4.02 (Or (Eq (f1 True) False) (Or (Eq (f1 x) False) (Or (Eq (f1 True) False) (Eq (f1 x) False))))) % 3.82/4.02 Clause #60 (by eliminate duplicate literals #[58]): Or (Eq (f0 True) True) (Or (Eq (f0 False) False) (Or (Eq (f1 True) False) (Eq (f1 x) False))) % 3.82/4.02 Clause #61 (by identity loobHoist #[60]): Or (Eq (f0 True) True) (Or (Eq (f0 False) False) (Or (Eq (f1 True) False) (Or (Eq (f1 True) False) (Eq x False)))) % 3.82/4.02 Clause #62 (by identity boolHoist #[60]): Or (Eq (f0 True) True) (Or (Eq (f0 False) False) (Or (Eq (f1 True) False) (Or (Eq (f1 False) False) (Eq x True)))) % 3.82/4.02 Clause #63 (by eliminate duplicate literals #[61]): Or (Eq (f0 True) True) (Or (Eq (f0 False) False) (Or (Eq (f1 True) False) (Eq x False))) % 3.82/4.02 Clause #68 (by identity loobHoist #[8]): Or (Eq (f0 True) False) % 3.82/4.02 (Or (Eq (f0 False) False) (Or (Eq (f1 (f1 (f1 x))) True) (Or (Eq (f0 True) False) (Eq (f0 (f1 x)) False)))) % 3.82/4.02 Clause #70 (by eliminate duplicate literals #[68]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 (f1 (f1 x))) True) (Eq (f0 (f1 x)) False))) % 3.82/4.02 Clause #71 (by identity loobHoist #[70]): Or (Eq (f0 True) False) % 3.82/4.02 (Or (Eq (f0 False) False) (Or (Eq (f0 (f1 x)) False) (Or (Eq (f1 True) True) (Eq (f1 (f1 x)) False)))) % 3.82/4.02 Clause #72 (by identity boolHoist #[70]): Or (Eq (f0 True) False) % 3.82/4.02 (Or (Eq (f0 False) False) (Or (Eq (f0 (f1 x)) False) (Or (Eq (f1 False) True) (Eq (f1 (f1 x)) True)))) % 3.82/4.02 Clause #74 (by identity boolHoist #[71]): Or (Eq (f0 True) False) % 3.82/4.02 (Or (Eq (f0 False) False) % 3.82/4.02 (Or (Eq (f1 True) True) (Or (Eq (f1 (f1 x)) False) (Or (Eq (f0 False) False) (Eq (f1 x) True))))) % 3.82/4.02 Clause #82 (by eliminate duplicate literals #[41]): Or (Eq (f0 False) False) (Or (Eq (f0 (f0 (f1 x))) True) (Eq (f1 (f1 (f1 x))) True)) % 3.82/4.02 Clause #83 (by identity loobHoist #[82]): Or (Eq (f0 False) False) (Or (Eq (f1 (f1 (f1 x))) True) (Or (Eq (f0 True) True) (Eq (f0 (f1 x)) False))) % 3.82/4.02 Clause #85 (by identity loobHoist #[83]): Or (Eq (f0 False) False) % 3.82/4.02 (Or (Eq (f0 True) True) (Or (Eq (f0 (f1 x)) False) (Or (Eq (f1 True) True) (Eq (f1 (f1 x)) False)))) % 3.82/4.02 Clause #86 (by identity boolHoist #[83]): Or (Eq (f0 False) False) % 3.82/4.02 (Or (Eq (f0 True) True) (Or (Eq (f0 (f1 x)) False) (Or (Eq (f1 False) True) (Eq (f1 (f1 x)) True)))) % 3.82/4.02 Clause #88 (by identity boolHoist #[85]): Or (Eq (f0 False) False) % 3.82/4.02 (Or (Eq (f0 True) True) % 3.82/4.02 (Or (Eq (f1 True) True) (Or (Eq (f1 (f1 x)) False) (Or (Eq (f0 False) False) (Eq (f1 x) True))))) % 3.89/4.05 Clause #91 (by eliminate duplicate literals #[45]): Or (Eq (f0 False) True) (Or (Eq (f0 (f0 (f1 x))) True) (Eq (f1 (f1 (f1 x))) True)) % 3.89/4.05 Clause #93 (by identity boolHoist #[91]): Or (Eq (f0 False) True) (Or (Eq (f1 (f1 (f1 x))) True) (Or (Eq (f0 False) True) (Eq (f0 (f1 x)) True))) % 3.89/4.05 Clause #98 (by eliminate duplicate literals #[93]): Or (Eq (f0 False) True) (Or (Eq (f1 (f1 (f1 x))) True) (Eq (f0 (f1 x)) True)) % 3.89/4.05 Clause #99 (by identity loobHoist #[98]): Or (Eq (f0 False) True) (Or (Eq (f0 (f1 x)) True) (Or (Eq (f1 True) True) (Eq (f1 (f1 x)) False))) % 3.89/4.05 Clause #100 (by identity boolHoist #[98]): Or (Eq (f0 False) True) (Or (Eq (f0 (f1 x)) True) (Or (Eq (f1 False) True) (Eq (f1 (f1 x)) True))) % 3.89/4.05 Clause #102 (by identity boolHoist #[99]): Or (Eq (f0 False) True) (Or (Eq (f1 True) True) (Or (Eq (f1 (f1 x)) False) (Or (Eq (f0 False) True) (Eq (f1 x) True)))) % 3.89/4.05 Clause #106 (by identity boolHoist #[100]): Or (Eq (f0 False) True) (Or (Eq (f1 False) True) (Or (Eq (f1 (f1 x)) True) (Or (Eq (f0 False) True) (Eq (f1 x) True)))) % 3.89/4.05 Clause #112 (by eliminate duplicate literals #[106]): Or (Eq (f0 False) True) (Or (Eq (f1 False) True) (Or (Eq (f1 (f1 x)) True) (Eq (f1 x) True))) % 3.89/4.05 Clause #114 (by identity boolHoist #[112]): Or (Eq (f0 False) True) (Or (Eq (f1 False) True) (Or (Eq (f1 x) True) (Or (Eq (f1 False) True) (Eq (f1 x) True)))) % 3.89/4.05 Clause #115 (by eliminate duplicate literals #[114]): Or (Eq (f0 False) True) (Or (Eq (f1 False) True) (Eq (f1 x) True)) % 3.89/4.05 Clause #116 (by identity loobHoist #[115]): Or (Eq (f0 False) True) (Or (Eq (f1 False) True) (Or (Eq (f1 True) True) (Eq x False))) % 3.89/4.05 Clause #117 (by identity boolHoist #[115]): Or (Eq (f0 False) True) (Or (Eq (f1 False) True) (Or (Eq (f1 False) True) (Eq x True))) % 3.89/4.05 Clause #118 (by eliminate duplicate literals #[117]): Or (Eq (f0 False) True) (Or (Eq (f1 False) True) (Eq x True)) % 3.89/4.05 Clause #122 (by eliminate duplicate literals #[102]): Or (Eq (f0 False) True) (Or (Eq (f1 True) True) (Or (Eq (f1 (f1 x)) False) (Eq (f1 x) True))) % 3.89/4.05 Clause #124 (by identity boolHoist #[122]): Or (Eq (f0 False) True) (Or (Eq (f1 True) True) (Or (Eq (f1 x) True) (Or (Eq (f1 False) False) (Eq (f1 x) True)))) % 3.89/4.05 Clause #125 (by eliminate duplicate literals #[124]): Or (Eq (f0 False) True) (Or (Eq (f1 True) True) (Or (Eq (f1 x) True) (Eq (f1 False) False))) % 3.89/4.05 Clause #126 (by identity loobHoist #[125]): Or (Eq (f0 False) True) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Eq x False)))) % 3.89/4.05 Clause #128 (by eliminate duplicate literals #[126]): Or (Eq (f0 False) True) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Eq x False))) % 3.89/4.05 Clause #129 (by eliminate duplicate literals #[47]): Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq (f1 (f1 (f1 x))) False) (Eq (f0 (f1 x)) True))) % 3.89/4.05 Clause #130 (by identity loobHoist #[129]): Or (Eq (f0 False) True) % 3.89/4.05 (Or (Eq (f0 True) True) (Or (Eq (f0 (f1 x)) True) (Or (Eq (f1 True) False) (Eq (f1 (f1 x)) False)))) % 3.89/4.05 Clause #131 (by identity boolHoist #[129]): Or (Eq (f0 False) True) % 3.89/4.05 (Or (Eq (f0 True) True) (Or (Eq (f0 (f1 x)) True) (Or (Eq (f1 False) False) (Eq (f1 (f1 x)) True)))) % 3.89/4.05 Clause #132 (by identity loobHoist #[130]): Or (Eq (f0 False) True) % 3.89/4.05 (Or (Eq (f0 True) True) % 3.89/4.05 (Or (Eq (f1 True) False) (Or (Eq (f1 (f1 x)) False) (Or (Eq (f0 True) True) (Eq (f1 x) False))))) % 3.89/4.05 Clause #134 (by eliminate duplicate literals #[132]): Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) False) (Or (Eq (f1 (f1 x)) False) (Eq (f1 x) False)))) % 3.89/4.05 Clause #135 (by identity loobHoist #[134]): Or (Eq (f0 False) True) % 3.89/4.05 (Or (Eq (f0 True) True) (Or (Eq (f1 True) False) (Or (Eq (f1 x) False) (Or (Eq (f1 True) False) (Eq (f1 x) False))))) % 3.89/4.05 Clause #137 (by eliminate duplicate literals #[135]): Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) False) (Eq (f1 x) False))) % 3.89/4.05 Clause #138 (by identity loobHoist #[137]): Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) False) (Or (Eq (f1 True) False) (Eq x False)))) % 3.89/4.05 Clause #139 (by identity boolHoist #[137]): Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) False) (Or (Eq (f1 False) False) (Eq x True)))) % 3.92/4.08 Clause #140 (by eliminate duplicate literals #[138]): Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) False) (Eq x False))) % 3.92/4.08 Clause #145 (by identity loobHoist #[131]): Or (Eq (f0 False) True) % 3.92/4.08 (Or (Eq (f0 True) True) % 3.92/4.08 (Or (Eq (f1 False) False) (Or (Eq (f1 (f1 x)) True) (Or (Eq (f0 True) True) (Eq (f1 x) False))))) % 3.92/4.08 Clause #147 (by eliminate duplicate literals #[145]): Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq (f1 False) False) (Or (Eq (f1 (f1 x)) True) (Eq (f1 x) False)))) % 3.92/4.08 Clause #148 (by identity loobHoist #[147]): Or (Eq (f0 False) True) % 3.92/4.08 (Or (Eq (f0 True) True) (Or (Eq (f1 False) False) (Or (Eq (f1 x) False) (Or (Eq (f1 True) True) (Eq (f1 x) False))))) % 3.92/4.08 Clause #150 (by eliminate duplicate literals #[148]): Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq (f1 False) False) (Or (Eq (f1 x) False) (Eq (f1 True) True)))) % 3.92/4.08 Clause #152 (by identity boolHoist #[150]): Or (Eq (f0 False) True) % 3.92/4.08 (Or (Eq (f0 True) True) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Eq x True))))) % 3.92/4.08 Clause #153 (by eliminate duplicate literals #[152]): Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Eq x True)))) % 3.92/4.08 Clause #155 (by identity boolHoist #[72]): Or (Eq (f0 True) False) % 3.92/4.08 (Or (Eq (f0 False) False) % 3.92/4.08 (Or (Eq (f1 False) True) (Or (Eq (f1 (f1 x)) True) (Or (Eq (f0 False) False) (Eq (f1 x) True))))) % 3.92/4.08 Clause #162 (by identity loobHoist #[54]): Or (Eq (f0 True) True) % 3.92/4.08 (Or (Eq (f0 False) False) % 3.92/4.08 (Or (Eq (f1 False) False) (Or (Eq (f1 (f1 x)) True) (Or (Eq (f0 True) True) (Eq (f1 x) False))))) % 3.92/4.08 Clause #164 (by eliminate duplicate literals #[162]): Or (Eq (f0 True) True) % 3.92/4.08 (Or (Eq (f0 False) False) (Or (Eq (f1 False) False) (Or (Eq (f1 (f1 x)) True) (Eq (f1 x) False)))) % 3.92/4.08 Clause #165 (by identity loobHoist #[164]): Or (Eq (f0 True) True) % 3.92/4.08 (Or (Eq (f0 False) False) % 3.92/4.08 (Or (Eq (f1 False) False) (Or (Eq (f1 x) False) (Or (Eq (f1 True) True) (Eq (f1 x) False))))) % 3.92/4.08 Clause #167 (by eliminate duplicate literals #[165]): Or (Eq (f0 True) True) (Or (Eq (f0 False) False) (Or (Eq (f1 False) False) (Or (Eq (f1 x) False) (Eq (f1 True) True)))) % 3.92/4.08 Clause #169 (by identity boolHoist #[167]): Or (Eq (f0 True) True) % 3.92/4.08 (Or (Eq (f0 False) False) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Eq x True))))) % 3.92/4.08 Clause #170 (by eliminate duplicate literals #[169]): Or (Eq (f0 True) True) (Or (Eq (f0 False) False) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Eq x True)))) % 3.92/4.08 Clause #175 (by identity boolHoist #[86]): Or (Eq (f0 False) False) % 3.92/4.08 (Or (Eq (f0 True) True) % 3.92/4.08 (Or (Eq (f1 False) True) (Or (Eq (f1 (f1 x)) True) (Or (Eq (f0 False) False) (Eq (f1 x) True))))) % 3.92/4.08 Clause #188 (by eliminate duplicate literals #[74]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 True) True) (Or (Eq (f1 (f1 x)) False) (Eq (f1 x) True)))) % 3.92/4.08 Clause #190 (by identity boolHoist #[188]): Or (Eq (f0 True) False) % 3.92/4.08 (Or (Eq (f0 False) False) (Or (Eq (f1 True) True) (Or (Eq (f1 x) True) (Or (Eq (f1 False) False) (Eq (f1 x) True))))) % 3.92/4.08 Clause #191 (by eliminate duplicate literals #[190]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 True) True) (Or (Eq (f1 x) True) (Eq (f1 False) False)))) % 3.92/4.08 Clause #192 (by identity loobHoist #[191]): Or (Eq (f0 True) False) % 3.92/4.08 (Or (Eq (f0 False) False) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Eq x False))))) % 3.92/4.08 Clause #194 (by eliminate duplicate literals #[192]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Eq x False)))) % 3.92/4.08 Clause #195 (by eliminate duplicate literals #[88]): Or (Eq (f0 False) False) (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Or (Eq (f1 (f1 x)) False) (Eq (f1 x) True)))) % 3.92/4.08 Clause #197 (by identity boolHoist #[195]): Or (Eq (f0 False) False) % 3.92/4.08 (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Or (Eq (f1 x) True) (Or (Eq (f1 False) False) (Eq (f1 x) True))))) % 3.92/4.08 Clause #198 (by eliminate duplicate literals #[197]): Or (Eq (f0 False) False) (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Or (Eq (f1 x) True) (Eq (f1 False) False)))) % 3.92/4.11 Clause #199 (by identity loobHoist #[198]): Or (Eq (f0 False) False) % 3.92/4.11 (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Eq x False))))) % 3.92/4.11 Clause #201 (by eliminate duplicate literals #[199]): Or (Eq (f0 False) False) (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Eq x False)))) % 3.92/4.11 Clause #204 (by eliminate duplicate literals #[175]): Or (Eq (f0 False) False) (Or (Eq (f0 True) True) (Or (Eq (f1 False) True) (Or (Eq (f1 (f1 x)) True) (Eq (f1 x) True)))) % 3.92/4.11 Clause #206 (by identity boolHoist #[204]): Or (Eq (f0 False) False) % 3.92/4.11 (Or (Eq (f0 True) True) (Or (Eq (f1 False) True) (Or (Eq (f1 x) True) (Or (Eq (f1 False) True) (Eq (f1 x) True))))) % 3.92/4.11 Clause #213 (by eliminate duplicate literals #[206]): Or (Eq (f0 False) False) (Or (Eq (f0 True) True) (Or (Eq (f1 False) True) (Eq (f1 x) True))) % 3.92/4.11 Clause #214 (by identity loobHoist #[213]): Or (Eq (f0 False) False) (Or (Eq (f0 True) True) (Or (Eq (f1 False) True) (Or (Eq (f1 True) True) (Eq x False)))) % 3.92/4.11 Clause #215 (by identity boolHoist #[213]): Or (Eq (f0 False) False) (Or (Eq (f0 True) True) (Or (Eq (f1 False) True) (Or (Eq (f1 False) True) (Eq x True)))) % 3.92/4.11 Clause #217 (by eliminate duplicate literals #[215]): Or (Eq (f0 False) False) (Or (Eq (f0 True) True) (Or (Eq (f1 False) True) (Eq x True))) % 3.92/4.11 Clause #218 (by superposition #[217, 118]): Or (Eq (f0 True) True) % 3.92/4.11 (Or (Eq (f1 False) True) (Or (Eq x True) (Or (Eq False True) (Or (Eq (f1 False) True) (Eq x True))))) % 3.92/4.11 Clause #219 (by clausification #[218]): Or (Eq (f0 True) True) (Or (Eq (f1 False) True) (Or (Eq x True) (Or (Eq (f1 False) True) (Eq x True)))) % 3.92/4.11 Clause #220 (by eliminate duplicate literals #[219]): Or (Eq (f0 True) True) (Or (Eq (f1 False) True) (Eq x True)) % 3.92/4.11 Clause #230 (by eliminate duplicate literals #[155]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 False) True) (Or (Eq (f1 (f1 x)) True) (Eq (f1 x) True)))) % 3.92/4.11 Clause #232 (by identity boolHoist #[230]): Or (Eq (f0 True) False) % 3.92/4.11 (Or (Eq (f0 False) False) (Or (Eq (f1 False) True) (Or (Eq (f1 x) True) (Or (Eq (f1 False) True) (Eq (f1 x) True))))) % 3.92/4.11 Clause #233 (by eliminate duplicate literals #[232]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 False) True) (Eq (f1 x) True))) % 3.92/4.11 Clause #234 (by identity loobHoist #[233]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 False) True) (Or (Eq (f1 True) True) (Eq x False)))) % 3.92/4.11 Clause #235 (by identity boolHoist #[233]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 False) True) (Or (Eq (f1 False) True) (Eq x True)))) % 3.92/4.11 Clause #240 (by eliminate duplicate literals #[235]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 False) True) (Eq x True))) % 3.92/4.11 Clause #241 (by superposition #[240, 220]): Or (Eq (f0 False) False) % 3.92/4.11 (Or (Eq (f1 False) True) (Or (Eq x True) (Or (Eq False True) (Or (Eq (f1 False) True) (Eq x True))))) % 3.92/4.11 Clause #242 (by clausification #[241]): Or (Eq (f0 False) False) (Or (Eq (f1 False) True) (Or (Eq x True) (Or (Eq (f1 False) True) (Eq x True)))) % 3.92/4.11 Clause #243 (by eliminate duplicate literals #[242]): Or (Eq (f0 False) False) (Or (Eq (f1 False) True) (Eq x True)) % 3.92/4.11 Clause #244 (by superposition #[243, 118]): Or (Eq (f1 False) True) (Or (Eq x True) (Or (Eq False True) (Or (Eq (f1 False) True) (Eq x True)))) % 3.92/4.11 Clause #245 (by clausification #[244]): Or (Eq (f1 False) True) (Or (Eq x True) (Or (Eq (f1 False) True) (Eq x True))) % 3.92/4.11 Clause #246 (by eliminate duplicate literals #[245]): Or (Eq (f1 False) True) (Eq x True) % 3.92/4.11 Clause #248 (by superposition #[246, 153]): Or (Eq x True) % 3.92/4.11 (Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq True False) (Or (Eq (f1 True) True) (Eq x True))))) % 3.92/4.11 Clause #250 (by clausification #[248]): Or (Eq x True) (Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Eq x True)))) % 3.92/4.11 Clause #251 (by eliminate duplicate literals #[250]): Or (Eq x True) (Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Eq (f1 True) True))) % 3.92/4.11 Clause #254 (by superposition #[251, 170]): Or (Eq x True) % 3.98/4.14 (Or (Eq (f0 True) True) % 3.98/4.14 (Or (Eq (f1 True) True) % 3.98/4.14 (Or (Eq (f0 True) True) (Or (Eq True False) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Eq x True))))))) % 3.98/4.14 Clause #261 (by clausification #[254]): Or (Eq x True) % 3.98/4.14 (Or (Eq (f0 True) True) % 3.98/4.14 (Or (Eq (f1 True) True) (Or (Eq (f0 True) True) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Eq x True)))))) % 3.98/4.14 Clause #262 (by eliminate duplicate literals #[261]): Or (Eq x True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Eq (f1 False) False))) % 3.98/4.14 Clause #263 (by superposition #[262, 246]): Or (Eq x True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Or (Eq False True) (Eq x True)))) % 3.98/4.14 Clause #265 (by clausification #[263]): Or (Eq x True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Eq x True))) % 3.98/4.14 Clause #266 (by eliminate duplicate literals #[265]): Or (Eq x True) (Or (Eq (f0 True) True) (Eq (f1 True) True)) % 3.98/4.14 Clause #269 (by superposition #[266, 39]): Or (Eq x True) % 3.98/4.14 (Or (Eq (f1 True) True) (Or (Eq True False) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Eq x True))))) % 3.98/4.14 Clause #273 (by clausification #[269]): Or (Eq x True) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Eq x True)))) % 3.98/4.14 Clause #274 (by eliminate duplicate literals #[273]): Or (Eq x True) (Or (Eq (f1 True) True) (Eq (f1 False) False)) % 3.98/4.14 Clause #275 (by superposition #[274, 246]): Or (Eq x True) (Or (Eq (f1 True) True) (Or (Eq False True) (Eq x True))) % 3.98/4.14 Clause #276 (by clausification #[275]): Or (Eq x True) (Or (Eq (f1 True) True) (Eq x True)) % 3.98/4.14 Clause #277 (by eliminate duplicate literals #[276]): Or (Eq x True) (Eq (f1 True) True) % 3.98/4.14 Clause #279 (by superposition #[277, 139]): Or (Eq x True) % 3.98/4.14 (Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq True False) (Or (Eq (f1 False) False) (Eq x True))))) % 3.98/4.14 Clause #282 (by clausification #[279]): Or (Eq x True) (Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq (f1 False) False) (Eq x True)))) % 3.98/4.14 Clause #283 (by eliminate duplicate literals #[282]): Or (Eq x True) (Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Eq (f1 False) False))) % 3.98/4.14 Clause #284 (by superposition #[283, 246]): Or (Eq x True) (Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq False True) (Eq x True)))) % 3.98/4.14 Clause #285 (by clausification #[284]): Or (Eq x True) (Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Eq x True))) % 3.98/4.14 Clause #286 (by eliminate duplicate literals #[285]): Or (Eq x True) (Or (Eq (f0 False) True) (Eq (f0 True) True)) % 3.98/4.14 Clause #288 (by superposition #[286, 62]): Or (Eq x True) % 3.98/4.14 (Or (Eq (f0 True) True) % 3.98/4.14 (Or (Eq (f0 True) True) (Or (Eq True False) (Or (Eq (f1 True) False) (Or (Eq (f1 False) False) (Eq x True)))))) % 3.98/4.14 Clause #292 (by clausification #[288]): Or (Eq x True) % 3.98/4.14 (Or (Eq (f0 True) True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) False) (Or (Eq (f1 False) False) (Eq x True))))) % 3.98/4.14 Clause #293 (by eliminate duplicate literals #[292]): Or (Eq x True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) False) (Eq (f1 False) False))) % 3.98/4.14 Clause #294 (by superposition #[293, 277]): Or (Eq x True) (Or (Eq (f0 True) True) (Or (Eq (f1 False) False) (Or (Eq x True) (Eq False True)))) % 3.98/4.14 Clause #295 (by clausification #[294]): Or (Eq x True) (Or (Eq (f0 True) True) (Or (Eq (f1 False) False) (Eq x True))) % 3.98/4.14 Clause #296 (by eliminate duplicate literals #[295]): Or (Eq x True) (Or (Eq (f0 True) True) (Eq (f1 False) False)) % 3.98/4.14 Clause #297 (by superposition #[296, 246]): Or (Eq x True) (Or (Eq (f0 True) True) (Or (Eq False True) (Eq x True))) % 3.98/4.14 Clause #299 (by clausification #[297]): Or (Eq x True) (Or (Eq (f0 True) True) (Eq x True)) % 3.98/4.14 Clause #300 (by eliminate duplicate literals #[299]): Or (Eq x True) (Eq (f0 True) True) % 3.98/4.14 Clause #302 (by superposition #[300, 22]): Or (Eq x True) (Or (Eq True False) (Or (Eq (f1 True) False) (Or (Eq (f1 False) False) (Eq x True)))) % 3.98/4.14 Clause #306 (by clausification #[302]): Or (Eq x True) (Or (Eq (f1 True) False) (Or (Eq (f1 False) False) (Eq x True))) % 3.98/4.14 Clause #307 (by eliminate duplicate literals #[306]): Or (Eq x True) (Or (Eq (f1 True) False) (Eq (f1 False) False)) % 3.98/4.14 Clause #308 (by superposition #[307, 277]): Or (Eq x True) (Or (Eq (f1 False) False) (Or (Eq x True) (Eq False True))) % 4.02/4.16 Clause #309 (by clausification #[308]): Or (Eq x True) (Or (Eq (f1 False) False) (Eq x True)) % 4.02/4.16 Clause #310 (by eliminate duplicate literals #[309]): Or (Eq x True) (Eq (f1 False) False) % 4.02/4.16 Clause #311 (by superposition #[310, 246]): Or (Eq x True) (Or (Eq False True) (Eq x True)) % 4.02/4.16 Clause #312 (by clausification #[311]): Or (Eq x True) (Eq x True) % 4.02/4.16 Clause #313 (by eliminate duplicate literals #[312]): Eq x True % 4.02/4.16 Clause #314 (by backward demodulation #[313, 23]): Or (Eq (f0 True) False) (Or (Eq (f1 True) False) (Eq True False)) % 4.02/4.16 Clause #315 (by backward demodulation #[313, 63]): Or (Eq (f0 True) True) (Or (Eq (f0 False) False) (Or (Eq (f1 True) False) (Eq True False))) % 4.02/4.16 Clause #316 (by backward demodulation #[313, 116]): Or (Eq (f0 False) True) (Or (Eq (f1 False) True) (Or (Eq (f1 True) True) (Eq True False))) % 4.02/4.16 Clause #317 (by backward demodulation #[313, 128]): Or (Eq (f0 False) True) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Eq True False))) % 4.02/4.16 Clause #318 (by backward demodulation #[313, 140]): Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) False) (Eq True False))) % 4.02/4.16 Clause #319 (by backward demodulation #[313, 194]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Eq True False)))) % 4.02/4.16 Clause #320 (by backward demodulation #[313, 201]): Or (Eq (f0 False) False) (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Eq True False)))) % 4.02/4.16 Clause #321 (by backward demodulation #[313, 214]): Or (Eq (f0 False) False) (Or (Eq (f0 True) True) (Or (Eq (f1 False) True) (Or (Eq (f1 True) True) (Eq True False)))) % 4.02/4.16 Clause #322 (by backward demodulation #[313, 234]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 False) True) (Or (Eq (f1 True) True) (Eq True False)))) % 4.02/4.16 Clause #328 (by clausification #[314]): Or (Eq (f0 True) False) (Eq (f1 True) False) % 4.02/4.16 Clause #330 (by clausification #[318]): Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Eq (f1 True) False)) % 4.02/4.16 Clause #331 (by clausification #[317]): Or (Eq (f0 False) True) (Or (Eq (f1 True) True) (Eq (f1 False) False)) % 4.02/4.16 Clause #332 (by clausification #[316]): Or (Eq (f0 False) True) (Or (Eq (f1 False) True) (Eq (f1 True) True)) % 4.02/4.16 Clause #333 (by clausification #[315]): Or (Eq (f0 True) True) (Or (Eq (f0 False) False) (Eq (f1 True) False)) % 4.02/4.16 Clause #335 (by clausification #[320]): Or (Eq (f0 False) False) (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Eq (f1 False) False))) % 4.02/4.16 Clause #338 (by clausification #[319]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 True) True) (Eq (f1 False) False))) % 4.02/4.16 Clause #339 (by clausification #[322]): Or (Eq (f0 True) False) (Or (Eq (f0 False) False) (Or (Eq (f1 False) True) (Eq (f1 True) True))) % 4.02/4.16 Clause #341 (by clausification #[321]): Or (Eq (f0 False) False) (Or (Eq (f0 True) True) (Or (Eq (f1 False) True) (Eq (f1 True) True))) % 4.02/4.16 Clause #342 (by superposition #[341, 332]): Or (Eq (f0 True) True) % 4.02/4.16 (Or (Eq (f1 False) True) (Or (Eq (f1 True) True) (Or (Eq False True) (Or (Eq (f1 False) True) (Eq (f1 True) True))))) % 4.02/4.16 Clause #345 (by clausification #[342]): Or (Eq (f0 True) True) (Or (Eq (f1 False) True) (Or (Eq (f1 True) True) (Or (Eq (f1 False) True) (Eq (f1 True) True)))) % 4.02/4.16 Clause #346 (by eliminate duplicate literals #[345]): Or (Eq (f0 True) True) (Or (Eq (f1 False) True) (Eq (f1 True) True)) % 4.02/4.16 Clause #349 (by superposition #[346, 339]): Or (Eq (f1 False) True) % 4.02/4.16 (Or (Eq (f1 True) True) (Or (Eq True False) (Or (Eq (f0 False) False) (Or (Eq (f1 False) True) (Eq (f1 True) True))))) % 4.02/4.16 Clause #351 (by clausification #[349]): Or (Eq (f1 False) True) % 4.02/4.16 (Or (Eq (f1 True) True) (Or (Eq (f0 False) False) (Or (Eq (f1 False) True) (Eq (f1 True) True)))) % 4.02/4.16 Clause #352 (by eliminate duplicate literals #[351]): Or (Eq (f1 False) True) (Or (Eq (f1 True) True) (Eq (f0 False) False)) % 4.02/4.16 Clause #353 (by superposition #[352, 332]): Or (Eq (f1 False) True) (Or (Eq (f1 True) True) (Or (Eq False True) (Or (Eq (f1 False) True) (Eq (f1 True) True)))) % 4.02/4.16 Clause #354 (by clausification #[353]): Or (Eq (f1 False) True) (Or (Eq (f1 True) True) (Or (Eq (f1 False) True) (Eq (f1 True) True))) % 4.02/4.18 Clause #355 (by eliminate duplicate literals #[354]): Or (Eq (f1 False) True) (Eq (f1 True) True) % 4.02/4.18 Clause #356 (by superposition #[355, 331]): Or (Eq (f1 True) True) (Or (Eq (f0 False) True) (Or (Eq (f1 True) True) (Eq True False))) % 4.02/4.18 Clause #357 (by clausification #[356]): Or (Eq (f1 True) True) (Or (Eq (f0 False) True) (Eq (f1 True) True)) % 4.02/4.18 Clause #358 (by eliminate duplicate literals #[357]): Or (Eq (f1 True) True) (Eq (f0 False) True) % 4.02/4.18 Clause #360 (by superposition #[358, 335]): Or (Eq (f1 True) True) (Or (Eq True False) (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Eq (f1 False) False)))) % 4.02/4.18 Clause #363 (by clausification #[360]): Or (Eq (f1 True) True) (Or (Eq (f0 True) True) (Or (Eq (f1 True) True) (Eq (f1 False) False))) % 4.02/4.18 Clause #364 (by eliminate duplicate literals #[363]): Or (Eq (f1 True) True) (Or (Eq (f0 True) True) (Eq (f1 False) False)) % 4.02/4.18 Clause #365 (by superposition #[364, 355]): Or (Eq (f1 True) True) (Or (Eq (f0 True) True) (Or (Eq False True) (Eq (f1 True) True))) % 4.02/4.18 Clause #366 (by clausification #[365]): Or (Eq (f1 True) True) (Or (Eq (f0 True) True) (Eq (f1 True) True)) % 4.02/4.18 Clause #367 (by eliminate duplicate literals #[366]): Or (Eq (f1 True) True) (Eq (f0 True) True) % 4.02/4.18 Clause #369 (by superposition #[367, 338]): Or (Eq (f1 True) True) (Or (Eq True False) (Or (Eq (f0 False) False) (Or (Eq (f1 True) True) (Eq (f1 False) False)))) % 4.02/4.18 Clause #371 (by clausification #[369]): Or (Eq (f1 True) True) (Or (Eq (f0 False) False) (Or (Eq (f1 True) True) (Eq (f1 False) False))) % 4.02/4.18 Clause #372 (by eliminate duplicate literals #[371]): Or (Eq (f1 True) True) (Or (Eq (f0 False) False) (Eq (f1 False) False)) % 4.02/4.18 Clause #373 (by superposition #[372, 358]): Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Or (Eq (f1 True) True) (Eq False True))) % 4.02/4.18 Clause #375 (by clausification #[373]): Or (Eq (f1 True) True) (Or (Eq (f1 False) False) (Eq (f1 True) True)) % 4.02/4.18 Clause #376 (by eliminate duplicate literals #[375]): Or (Eq (f1 True) True) (Eq (f1 False) False) % 4.02/4.18 Clause #377 (by superposition #[376, 355]): Or (Eq (f1 True) True) (Or (Eq False True) (Eq (f1 True) True)) % 4.02/4.18 Clause #378 (by clausification #[377]): Or (Eq (f1 True) True) (Eq (f1 True) True) % 4.02/4.18 Clause #379 (by eliminate duplicate literals #[378]): Eq (f1 True) True % 4.02/4.18 Clause #380 (by backward demodulation #[379, 328]): Or (Eq (f0 True) False) (Eq True False) % 4.02/4.18 Clause #381 (by backward demodulation #[379, 330]): Or (Eq (f0 False) True) (Or (Eq (f0 True) True) (Eq True False)) % 4.02/4.18 Clause #382 (by backward demodulation #[379, 333]): Or (Eq (f0 True) True) (Or (Eq (f0 False) False) (Eq True False)) % 4.02/4.18 Clause #384 (by clausification #[380]): Eq (f0 True) False % 4.02/4.18 Clause #385 (by clausification #[382]): Or (Eq (f0 True) True) (Eq (f0 False) False) % 4.02/4.18 Clause #386 (by forward demodulation #[385, 384]): Or (Eq False True) (Eq (f0 False) False) % 4.02/4.18 Clause #387 (by clausification #[386]): Eq (f0 False) False % 4.02/4.18 Clause #388 (by clausification #[381]): Or (Eq (f0 False) True) (Eq (f0 True) True) % 4.02/4.18 Clause #389 (by forward demodulation #[388, 384]): Or (Eq (f0 False) True) (Eq False True) % 4.02/4.18 Clause #390 (by clausification #[389]): Eq (f0 False) True % 4.02/4.18 Clause #391 (by superposition #[390, 387]): Eq True False % 4.02/4.18 Clause #392 (by clausification #[391]): False % 4.02/4.18 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------