%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP384_1 : TPTP v9.2.0. Released v8.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:52:12 PM UTC 2025 % Result : Theorem 138.57s 138.73s % Output : Proof 138.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : ITP384_1 : TPTP v9.2.0. Released v8.0.0. % 0.08/0.14 % Command : duper %s % 0.15/0.35 % Computer : n016.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Fri Oct 3 00:18:08 EDT 2025 % 0.15/0.35 % CPUTime : % 138.57/138.73 SZS status Theorem for theBenchmark.p % 138.57/138.73 SZS output start Proof for theBenchmark.p % 138.57/138.73 Clause #29 (by assumption #[]): Eq % 138.57/138.73 (Not % 138.57/138.73 (Eq («comp$» («fun_app$v» («fun_app$w» «comp$a» «g$») «f$») («fun_app$x» («fun_app$y» «comp$b» «f$a») «g$a»)) % 138.57/138.73 «id$»)) % 138.57/138.73 True % 138.57/138.73 Clause #42 (by assumption #[]): Eq (Eq («fun_app$ae» («fun_app$af» «comp$d» «g$») «g$a») «id$») True % 138.57/138.73 Clause #64 (by assumption #[]): Eq (Eq («fun_app$aj» («fun_app$ak» «comp$e» «f$a») «f$») «id$a») True % 138.57/138.73 Clause #66 (by assumption #[]): Eq (Eq («fun_app$ac» («fun_app$ad» «comp$c» «f$») «f$a») «id$b») True % 138.57/138.73 Clause #129 (by assumption #[]): Eq % 138.57/138.73 (∀ (A__questionmark_v0 : «B_update_a_update_fun$») (A__questionmark_v1 : «C_update_b_update_fun$») % 138.57/138.73 (A__questionmark_v2 : «C_update_a_update_fun$») (A__questionmark_v3 : «A_update_c_update_fun$»), % 138.57/138.73 Eq («comp$ae» A__questionmark_v0 A__questionmark_v1) A__questionmark_v2 → % 138.57/138.73 Eq («comp$» («fun_app$v» («fun_app$w» «comp$a» A__questionmark_v3) A__questionmark_v0) A__questionmark_v1) % 138.57/138.73 («fun_app$ae» («fun_app$af» «comp$d» A__questionmark_v3) A__questionmark_v2)) % 138.57/138.73 True % 138.57/138.73 Clause #133 (by assumption #[]): Eq % 138.57/138.73 (∀ (A__questionmark_v0 : «B_update_a_update_fun$») (A__questionmark_v1 : «C_update_b_update_fun$») % 138.57/138.73 (A__questionmark_v2 : «C_update_a_update_fun$») (A__questionmark_v3 : «A_update_b_update_fun$»), % 138.57/138.73 Eq («comp$ae» A__questionmark_v0 A__questionmark_v1) A__questionmark_v2 → % 138.57/138.73 Eq («comp$i» («fun_app$aj» («fun_app$ak» «comp$e» A__questionmark_v3) A__questionmark_v0) A__questionmark_v1) % 138.57/138.73 («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v3) A__questionmark_v2)) % 138.57/138.73 True % 138.57/138.73 Clause #141 (by assumption #[]): Eq % 138.57/138.73 (∀ (A__questionmark_v0 : «B_update_c_update_fun$») (A__questionmark_v1 : «A_update_b_update_fun$») % 138.57/138.73 (A__questionmark_v2 : «A_update_c_update_fun$») (A__questionmark_v3 : «C_update_a_update_fun$»), % 138.57/138.73 Eq («comp$aj» A__questionmark_v0 A__questionmark_v1) A__questionmark_v2 → % 138.57/138.73 Eq («comp$» A__questionmark_v0 («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v1) A__questionmark_v3)) % 138.57/138.73 («fun_app$ae» («fun_app$af» «comp$d» A__questionmark_v2) A__questionmark_v3)) % 138.57/138.73 True % 138.57/138.73 Clause #142 (by assumption #[]): Eq % 138.57/138.73 (∀ (A__questionmark_v0 : «B_update_b_update_fun$») (A__questionmark_v1 A__questionmark_v2 : «A_update_b_update_fun$») % 138.57/138.73 (A__questionmark_v3 : «C_update_a_update_fun$»), % 138.57/138.73 Eq («comp$x» A__questionmark_v0 A__questionmark_v1) A__questionmark_v2 → % 138.57/138.73 Eq («comp$i» A__questionmark_v0 («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v1) A__questionmark_v3)) % 138.57/138.73 («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v2) A__questionmark_v3)) % 138.57/138.73 True % 138.57/138.73 Clause #161 (by assumption #[]): Eq % 138.57/138.73 (∀ (A__questionmark_v0 : «B_update_a_update_fun$») (A__questionmark_v1 : «A_update_b_update_fun$») % 138.57/138.73 (A__questionmark_v2 : «C_update_a_update_fun$»), % 138.57/138.73 Eq («comp$aa» («fun_app$ac» («fun_app$ad» «comp$c» A__questionmark_v0) A__questionmark_v1) A__questionmark_v2) % 138.57/138.73 («comp$ae» A__questionmark_v0 («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v1) A__questionmark_v2))) % 138.57/138.73 True % 138.57/138.73 Clause #221 (by assumption #[]): Eq % 138.57/138.73 (∀ (A__questionmark_v0 : «A_update_b_update_fun$») (A__questionmark_v1 : «B_update_a_update_fun$»), % 138.57/138.73 Eq («fcomp$» A__questionmark_v0 A__questionmark_v1) % 138.57/138.73 («fun_app$ac» («fun_app$ad» «comp$c» A__questionmark_v1) A__questionmark_v0)) % 138.57/138.73 True % 138.57/138.73 Clause #222 (by assumption #[]): Eq % 138.57/138.73 (∀ (A__questionmark_v0 : «C_update_a_update_fun$») (A__questionmark_v1 : «A_update_c_update_fun$»), % 138.57/138.73 Eq («fcomp$a» A__questionmark_v0 A__questionmark_v1) % 138.57/138.73 («fun_app$ae» («fun_app$af» «comp$d» A__questionmark_v1) A__questionmark_v0)) % 138.57/138.73 True % 138.57/138.73 Clause #223 (by assumption #[]): Eq % 138.57/138.73 (∀ (A__questionmark_v0 : «B_update_a_update_fun$») (A__questionmark_v1 : «A_update_c_update_fun$»), % 138.57/138.73 Eq («fcomp$b» A__questionmark_v0 A__questionmark_v1) % 138.57/138.73 («fun_app$v» («fun_app$w» «comp$a» A__questionmark_v1) A__questionmark_v0)) % 138.57/138.76 True % 138.57/138.76 Clause #224 (by assumption #[]): Eq % 138.57/138.76 (∀ (A__questionmark_v0 : «C_update_a_update_fun$») (A__questionmark_v1 : «A_update_b_update_fun$»), % 138.57/138.76 Eq («fcomp$c» A__questionmark_v0 A__questionmark_v1) % 138.57/138.76 («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v1) A__questionmark_v0)) % 138.57/138.76 True % 138.57/138.76 Clause #225 (by assumption #[]): Eq % 138.57/138.76 (∀ (A__questionmark_v0 : «B_update_a_update_fun$») (A__questionmark_v1 : «A_update_b_update_fun$»), % 138.57/138.76 Eq («fcomp$d» A__questionmark_v0 A__questionmark_v1) % 138.57/138.76 («fun_app$aj» («fun_app$ak» «comp$e» A__questionmark_v1) A__questionmark_v0)) % 138.57/138.76 True % 138.57/138.76 Clause #447 (by assumption #[]): Eq % 138.57/138.76 (∀ (A__questionmark_v0 : «A_update_b_update_fun$») (A__questionmark_v1 : «B_update_a_update_fun$»), % 138.57/138.76 And (Eq («fun_app$aj» («fun_app$ak» «comp$e» A__questionmark_v0) A__questionmark_v1) «id$a») % 138.57/138.76 (Eq («fun_app$ac» («fun_app$ad» «comp$c» A__questionmark_v1) A__questionmark_v0) «id$b») → % 138.57/138.76 Eq («inv_into$b» «top$» A__questionmark_v0) A__questionmark_v1) % 138.57/138.76 True % 138.57/138.76 Clause #471 (by assumption #[]): Eq % 138.57/138.76 (∀ (A__questionmark_v0 : «A_update_b_update_fun$») (A__questionmark_v1 : «A_update_c_update_fun$»), % 138.57/138.76 «inj_on$» A__questionmark_v0 «top$» → % 138.57/138.76 Eq % 138.57/138.76 («comp$aj» («fun_app$v» («fun_app$w» «comp$a» A__questionmark_v1) («inv_into$b» «top$» A__questionmark_v0)) % 138.57/138.76 A__questionmark_v0) % 138.57/138.76 A__questionmark_v1) % 138.57/138.76 True % 138.57/138.76 Clause #473 (by assumption #[]): Eq % 138.57/138.76 (∀ (A__questionmark_v0 A__questionmark_v1 : «A_update_b_update_fun$»), % 138.57/138.76 «inj_on$» A__questionmark_v0 «top$» → % 138.57/138.76 Eq % 138.57/138.76 («comp$x» («fun_app$aj» («fun_app$ak» «comp$e» A__questionmark_v1) («inv_into$b» «top$» A__questionmark_v0)) % 138.57/138.76 A__questionmark_v0) % 138.57/138.76 A__questionmark_v1) % 138.57/138.76 True % 138.57/138.76 Clause #518 (by assumption #[]): Eq % 138.57/138.76 (∀ (A__questionmark_v0 : «B_update_a_update_fun$») (A__questionmark_v1 : «A_update_b_update_fun$») % 138.57/138.76 (A__questionmark_v2 : «A_update_set$»), % 138.57/138.76 «inj_on$i» («fun_app$ac» («fun_app$ad» «comp$c» A__questionmark_v0) A__questionmark_v1) A__questionmark_v2 → % 138.57/138.76 «inj_on$» A__questionmark_v1 A__questionmark_v2) % 138.57/138.76 True % 138.57/138.76 Clause #525 (by assumption #[]): Eq (∀ (A__questionmark_v0 : «A_update_set$»), «inj_on$i» «id$b» A__questionmark_v0) True % 138.57/138.76 Clause #686 (by clausification #[525]): ∀ (a : «A_update_set$»), Eq («inj_on$i» «id$b» a) True % 138.57/138.76 Clause #1162 (by clausification #[518]): ∀ (a : «B_update_a_update_fun$»), % 138.57/138.76 Eq % 138.57/138.76 (∀ (A__questionmark_v1 : «A_update_b_update_fun$») (A__questionmark_v2 : «A_update_set$»), % 138.57/138.76 «inj_on$i» («fun_app$ac» («fun_app$ad» «comp$c» a) A__questionmark_v1) A__questionmark_v2 → % 138.57/138.76 «inj_on$» A__questionmark_v1 A__questionmark_v2) % 138.57/138.76 True % 138.57/138.76 Clause #1163 (by clausification #[1162]): ∀ (a : «B_update_a_update_fun$») (a_1 : «A_update_b_update_fun$»), % 138.57/138.76 Eq % 138.57/138.76 (∀ (A__questionmark_v2 : «A_update_set$»), % 138.57/138.76 «inj_on$i» («fun_app$ac» («fun_app$ad» «comp$c» a) a_1) A__questionmark_v2 → «inj_on$» a_1 A__questionmark_v2) % 138.57/138.76 True % 138.57/138.76 Clause #1164 (by clausification #[1163]): ∀ (a : «B_update_a_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «A_update_set$»), % 138.57/138.76 Eq («inj_on$i» («fun_app$ac» («fun_app$ad» «comp$c» a) a_1) a_2 → «inj_on$» a_1 a_2) True % 138.57/138.76 Clause #1165 (by clausification #[1164]): ∀ (a : «B_update_a_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «A_update_set$»), % 138.57/138.76 Or (Eq («inj_on$i» («fun_app$ac» («fun_app$ad» «comp$c» a) a_1) a_2) False) (Eq («inj_on$» a_1 a_2) True) % 138.57/138.76 Clause #1166 (by clausification #[29]): Eq (Eq («comp$» («fun_app$v» («fun_app$w» «comp$a» «g$») «f$») («fun_app$x» («fun_app$y» «comp$b» «f$a») «g$a»)) «id$») % 138.57/138.76 False % 138.57/138.76 Clause #1167 (by clausification #[1166]): Ne («comp$» («fun_app$v» («fun_app$w» «comp$a» «g$») «f$») («fun_app$x» («fun_app$y» «comp$b» «f$a») «g$a»)) «id$» % 138.57/138.76 Clause #1187 (by clausification #[66]): Eq («fun_app$ac» («fun_app$ad» «comp$c» «f$») «f$a») «id$b» % 138.61/138.79 Clause #1191 (by superposition #[1187, 1165]): ∀ (a : «A_update_set$»), Or (Eq («inj_on$i» «id$b» a) False) (Eq («inj_on$» «f$a» a) True) % 138.61/138.79 Clause #1192 (by superposition #[1191, 686]): ∀ (a : «A_update_set$»), Or (Eq («inj_on$» «f$a» a) True) (Eq False True) % 138.61/138.79 Clause #1193 (by clausification #[1192]): ∀ (a : «A_update_set$»), Eq («inj_on$» «f$a» a) True % 138.61/138.79 Clause #1216 (by clausification #[64]): Eq («fun_app$aj» («fun_app$ak» «comp$e» «f$a») «f$») «id$a» % 138.61/138.79 Clause #1242 (by clausification #[42]): Eq («fun_app$ae» («fun_app$af» «comp$d» «g$») «g$a») «id$» % 138.61/138.79 Clause #1635 (by clausification #[447]): ∀ (a : «A_update_b_update_fun$»), % 138.61/138.79 Eq % 138.61/138.79 (∀ (A__questionmark_v1 : «B_update_a_update_fun$»), % 138.61/138.79 And (Eq («fun_app$aj» («fun_app$ak» «comp$e» a) A__questionmark_v1) «id$a») % 138.61/138.79 (Eq («fun_app$ac» («fun_app$ad» «comp$c» A__questionmark_v1) a) «id$b») → % 138.61/138.79 Eq («inv_into$b» «top$» a) A__questionmark_v1) % 138.61/138.79 True % 138.61/138.79 Clause #1636 (by clausification #[1635]): ∀ (a : «A_update_b_update_fun$») (a_1 : «B_update_a_update_fun$»), % 138.61/138.79 Eq % 138.61/138.79 (And (Eq («fun_app$aj» («fun_app$ak» «comp$e» a) a_1) «id$a») % 138.61/138.79 (Eq («fun_app$ac» («fun_app$ad» «comp$c» a_1) a) «id$b») → % 138.61/138.79 Eq («inv_into$b» «top$» a) a_1) % 138.61/138.79 True % 138.61/138.79 Clause #1637 (by clausification #[1636]): ∀ (a : «A_update_b_update_fun$») (a_1 : «B_update_a_update_fun$»), % 138.61/138.79 Or % 138.61/138.79 (Eq % 138.61/138.79 (And (Eq («fun_app$aj» («fun_app$ak» «comp$e» a) a_1) «id$a») % 138.61/138.79 (Eq («fun_app$ac» («fun_app$ad» «comp$c» a_1) a) «id$b»)) % 138.61/138.79 False) % 138.61/138.79 (Eq (Eq («inv_into$b» «top$» a) a_1) True) % 138.61/138.79 Clause #1638 (by clausification #[1637]): ∀ (a : «A_update_b_update_fun$») (a_1 : «B_update_a_update_fun$»), % 138.61/138.79 Or (Eq (Eq («inv_into$b» «top$» a) a_1) True) % 138.61/138.79 (Or (Eq (Eq («fun_app$aj» («fun_app$ak» «comp$e» a) a_1) «id$a») False) % 138.61/138.79 (Eq (Eq («fun_app$ac» («fun_app$ad» «comp$c» a_1) a) «id$b») False)) % 138.61/138.79 Clause #1639 (by clausification #[1638]): ∀ (a : «A_update_b_update_fun$») (a_1 : «B_update_a_update_fun$»), % 138.61/138.79 Or (Eq (Eq («fun_app$aj» («fun_app$ak» «comp$e» a) a_1) «id$a») False) % 138.61/138.79 (Or (Eq (Eq («fun_app$ac» («fun_app$ad» «comp$c» a_1) a) «id$b») False) (Eq («inv_into$b» «top$» a) a_1)) % 138.61/138.79 Clause #1640 (by clausification #[1639]): ∀ (a : «B_update_a_update_fun$») (a_1 : «A_update_b_update_fun$»), % 138.61/138.79 Or (Eq (Eq («fun_app$ac» («fun_app$ad» «comp$c» a) a_1) «id$b») False) % 138.61/138.79 (Or (Eq («inv_into$b» «top$» a_1) a) (Ne («fun_app$aj» («fun_app$ak» «comp$e» a_1) a) «id$a»)) % 138.61/138.79 Clause #1641 (by clausification #[1640]): ∀ (a : «A_update_b_update_fun$») (a_1 : «B_update_a_update_fun$»), % 138.61/138.79 Or (Eq («inv_into$b» «top$» a) a_1) % 138.61/138.79 (Or (Ne («fun_app$aj» («fun_app$ak» «comp$e» a) a_1) «id$a») % 138.61/138.79 (Ne («fun_app$ac» («fun_app$ad» «comp$c» a_1) a) «id$b»)) % 138.61/138.79 Clause #1642 (by superposition #[1641, 1216]): Or (Eq («inv_into$b» «top$» «f$a») «f$») % 138.61/138.79 (Or (Ne «id$a» «id$a») (Ne («fun_app$ac» («fun_app$ad» «comp$c» «f$») «f$a») «id$b»)) % 138.61/138.79 Clause #2826 (by clausification #[129]): ∀ (a : «B_update_a_update_fun$»), % 138.61/138.79 Eq % 138.61/138.79 (∀ (A__questionmark_v1 : «C_update_b_update_fun$») (A__questionmark_v2 : «C_update_a_update_fun$») % 138.61/138.79 (A__questionmark_v3 : «A_update_c_update_fun$»), % 138.61/138.79 Eq («comp$ae» a A__questionmark_v1) A__questionmark_v2 → % 138.61/138.79 Eq («comp$» («fun_app$v» («fun_app$w» «comp$a» A__questionmark_v3) a) A__questionmark_v1) % 138.61/138.79 («fun_app$ae» («fun_app$af» «comp$d» A__questionmark_v3) A__questionmark_v2)) % 138.61/138.79 True % 138.61/138.79 Clause #2827 (by clausification #[2826]): ∀ (a : «B_update_a_update_fun$») (a_1 : «C_update_b_update_fun$»), % 138.61/138.79 Eq % 138.61/138.79 (∀ (A__questionmark_v2 : «C_update_a_update_fun$») (A__questionmark_v3 : «A_update_c_update_fun$»), % 138.61/138.79 Eq («comp$ae» a a_1) A__questionmark_v2 → % 138.61/138.79 Eq («comp$» («fun_app$v» («fun_app$w» «comp$a» A__questionmark_v3) a) a_1) % 138.61/138.79 («fun_app$ae» («fun_app$af» «comp$d» A__questionmark_v3) A__questionmark_v2)) % 138.61/138.82 True % 138.61/138.82 Clause #2828 (by clausification #[2827]): ∀ (a : «B_update_a_update_fun$») (a_1 : «C_update_b_update_fun$») (a_2 : «C_update_a_update_fun$»), % 138.61/138.82 Eq % 138.61/138.82 (∀ (A__questionmark_v3 : «A_update_c_update_fun$»), % 138.61/138.82 Eq («comp$ae» a a_1) a_2 → % 138.61/138.82 Eq («comp$» («fun_app$v» («fun_app$w» «comp$a» A__questionmark_v3) a) a_1) % 138.61/138.82 («fun_app$ae» («fun_app$af» «comp$d» A__questionmark_v3) a_2)) % 138.61/138.82 True % 138.61/138.82 Clause #2829 (by clausification #[2828]): ∀ (a : «B_update_a_update_fun$») (a_1 : «C_update_b_update_fun$») (a_2 : «C_update_a_update_fun$») % 138.61/138.82 (a_3 : «A_update_c_update_fun$»), % 138.61/138.82 Eq % 138.61/138.82 (Eq («comp$ae» a a_1) a_2 → % 138.61/138.82 Eq («comp$» («fun_app$v» («fun_app$w» «comp$a» a_3) a) a_1) («fun_app$ae» («fun_app$af» «comp$d» a_3) a_2)) % 138.61/138.82 True % 138.61/138.82 Clause #2830 (by clausification #[2829]): ∀ (a : «B_update_a_update_fun$») (a_1 : «C_update_b_update_fun$») (a_2 : «C_update_a_update_fun$») % 138.61/138.82 (a_3 : «A_update_c_update_fun$»), % 138.61/138.82 Or (Eq (Eq («comp$ae» a a_1) a_2) False) % 138.61/138.82 (Eq (Eq («comp$» («fun_app$v» («fun_app$w» «comp$a» a_3) a) a_1) («fun_app$ae» («fun_app$af» «comp$d» a_3) a_2)) % 138.61/138.82 True) % 138.61/138.82 Clause #2831 (by clausification #[2830]): ∀ (a : «A_update_c_update_fun$») (a_1 : «B_update_a_update_fun$») (a_2 : «C_update_b_update_fun$») % 138.61/138.82 (a_3 : «C_update_a_update_fun$»), % 138.61/138.82 Or % 138.61/138.82 (Eq (Eq («comp$» («fun_app$v» («fun_app$w» «comp$a» a) a_1) a_2) («fun_app$ae» («fun_app$af» «comp$d» a) a_3)) True) % 138.61/138.82 (Ne («comp$ae» a_1 a_2) a_3) % 138.61/138.82 Clause #2832 (by clausification #[2831]): ∀ (a : «B_update_a_update_fun$») (a_1 : «C_update_b_update_fun$») (a_2 : «C_update_a_update_fun$») % 138.61/138.82 (a_3 : «A_update_c_update_fun$»), % 138.61/138.82 Or (Ne («comp$ae» a a_1) a_2) % 138.61/138.82 (Eq («comp$» («fun_app$v» («fun_app$w» «comp$a» a_3) a) a_1) («fun_app$ae» («fun_app$af» «comp$d» a_3) a_2)) % 138.61/138.82 Clause #2833 (by destructive equality resolution #[2832]): ∀ (a : «A_update_c_update_fun$») (a_1 : «B_update_a_update_fun$») (a_2 : «C_update_b_update_fun$»), % 138.61/138.82 Eq («comp$» («fun_app$v» («fun_app$w» «comp$a» a) a_1) a_2) % 138.61/138.82 («fun_app$ae» («fun_app$af» «comp$d» a) («comp$ae» a_1 a_2)) % 138.61/138.82 Clause #2834 (by backward demodulation #[2833, 1167]): Ne («fun_app$ae» («fun_app$af» «comp$d» «g$») («comp$ae» «f$» («fun_app$x» («fun_app$y» «comp$b» «f$a») «g$a»))) «id$» % 138.61/138.82 Clause #2925 (by clausification #[133]): ∀ (a : «B_update_a_update_fun$»), % 138.61/138.82 Eq % 138.61/138.82 (∀ (A__questionmark_v1 : «C_update_b_update_fun$») (A__questionmark_v2 : «C_update_a_update_fun$») % 138.61/138.82 (A__questionmark_v3 : «A_update_b_update_fun$»), % 138.61/138.82 Eq («comp$ae» a A__questionmark_v1) A__questionmark_v2 → % 138.61/138.82 Eq («comp$i» («fun_app$aj» («fun_app$ak» «comp$e» A__questionmark_v3) a) A__questionmark_v1) % 138.61/138.82 («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v3) A__questionmark_v2)) % 138.61/138.82 True % 138.61/138.82 Clause #2926 (by clausification #[2925]): ∀ (a : «B_update_a_update_fun$») (a_1 : «C_update_b_update_fun$»), % 138.61/138.82 Eq % 138.61/138.82 (∀ (A__questionmark_v2 : «C_update_a_update_fun$») (A__questionmark_v3 : «A_update_b_update_fun$»), % 138.61/138.82 Eq («comp$ae» a a_1) A__questionmark_v2 → % 138.61/138.82 Eq («comp$i» («fun_app$aj» («fun_app$ak» «comp$e» A__questionmark_v3) a) a_1) % 138.61/138.82 («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v3) A__questionmark_v2)) % 138.61/138.82 True % 138.61/138.82 Clause #2927 (by clausification #[2926]): ∀ (a : «B_update_a_update_fun$») (a_1 : «C_update_b_update_fun$») (a_2 : «C_update_a_update_fun$»), % 138.61/138.82 Eq % 138.61/138.82 (∀ (A__questionmark_v3 : «A_update_b_update_fun$»), % 138.61/138.82 Eq («comp$ae» a a_1) a_2 → % 138.61/138.82 Eq («comp$i» («fun_app$aj» («fun_app$ak» «comp$e» A__questionmark_v3) a) a_1) % 138.61/138.82 («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v3) a_2)) % 138.61/138.82 True % 138.61/138.82 Clause #2928 (by clausification #[2927]): ∀ (a : «B_update_a_update_fun$») (a_1 : «C_update_b_update_fun$») (a_2 : «C_update_a_update_fun$») % 138.61/138.82 (a_3 : «A_update_b_update_fun$»), % 138.61/138.82 Eq % 138.61/138.82 (Eq («comp$ae» a a_1) a_2 → % 138.61/138.82 Eq («comp$i» («fun_app$aj» («fun_app$ak» «comp$e» a_3) a) a_1) («fun_app$x» («fun_app$y» «comp$b» a_3) a_2)) % 138.68/138.85 True % 138.68/138.85 Clause #2929 (by clausification #[2928]): ∀ (a : «B_update_a_update_fun$») (a_1 : «C_update_b_update_fun$») (a_2 : «C_update_a_update_fun$») % 138.68/138.85 (a_3 : «A_update_b_update_fun$»), % 138.68/138.85 Or (Eq (Eq («comp$ae» a a_1) a_2) False) % 138.68/138.85 (Eq (Eq («comp$i» («fun_app$aj» («fun_app$ak» «comp$e» a_3) a) a_1) («fun_app$x» («fun_app$y» «comp$b» a_3) a_2)) % 138.68/138.85 True) % 138.68/138.85 Clause #2930 (by clausification #[2929]): ∀ (a : «A_update_b_update_fun$») (a_1 : «B_update_a_update_fun$») (a_2 : «C_update_b_update_fun$») % 138.68/138.85 (a_3 : «C_update_a_update_fun$»), % 138.68/138.85 Or % 138.68/138.85 (Eq (Eq («comp$i» («fun_app$aj» («fun_app$ak» «comp$e» a) a_1) a_2) («fun_app$x» («fun_app$y» «comp$b» a) a_3)) % 138.68/138.85 True) % 138.68/138.85 (Ne («comp$ae» a_1 a_2) a_3) % 138.68/138.85 Clause #2931 (by clausification #[2930]): ∀ (a : «B_update_a_update_fun$») (a_1 : «C_update_b_update_fun$») (a_2 : «C_update_a_update_fun$») % 138.68/138.85 (a_3 : «A_update_b_update_fun$»), % 138.68/138.85 Or (Ne («comp$ae» a a_1) a_2) % 138.68/138.85 (Eq («comp$i» («fun_app$aj» («fun_app$ak» «comp$e» a_3) a) a_1) («fun_app$x» («fun_app$y» «comp$b» a_3) a_2)) % 138.68/138.85 Clause #2932 (by destructive equality resolution #[2931]): ∀ (a : «A_update_b_update_fun$») (a_1 : «B_update_a_update_fun$») (a_2 : «C_update_b_update_fun$»), % 138.68/138.85 Eq («comp$i» («fun_app$aj» («fun_app$ak» «comp$e» a) a_1) a_2) % 138.68/138.85 («fun_app$x» («fun_app$y» «comp$b» a) («comp$ae» a_1 a_2)) % 138.68/138.85 Clause #2934 (by superposition #[2932, 1216]): ∀ (a : «C_update_b_update_fun$»), Eq («comp$i» «id$a» a) («fun_app$x» («fun_app$y» «comp$b» «f$a») («comp$ae» «f$» a)) % 138.68/138.85 Clause #3164 (by clausification #[141]): ∀ (a : «B_update_c_update_fun$»), % 138.68/138.85 Eq % 138.68/138.85 (∀ (A__questionmark_v1 : «A_update_b_update_fun$») (A__questionmark_v2 : «A_update_c_update_fun$») % 138.68/138.85 (A__questionmark_v3 : «C_update_a_update_fun$»), % 138.68/138.85 Eq («comp$aj» a A__questionmark_v1) A__questionmark_v2 → % 138.68/138.85 Eq («comp$» a («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v1) A__questionmark_v3)) % 138.68/138.85 («fun_app$ae» («fun_app$af» «comp$d» A__questionmark_v2) A__questionmark_v3)) % 138.68/138.85 True % 138.68/138.85 Clause #3165 (by clausification #[3164]): ∀ (a : «B_update_c_update_fun$») (a_1 : «A_update_b_update_fun$»), % 138.68/138.85 Eq % 138.68/138.85 (∀ (A__questionmark_v2 : «A_update_c_update_fun$») (A__questionmark_v3 : «C_update_a_update_fun$»), % 138.68/138.85 Eq («comp$aj» a a_1) A__questionmark_v2 → % 138.68/138.85 Eq («comp$» a («fun_app$x» («fun_app$y» «comp$b» a_1) A__questionmark_v3)) % 138.68/138.85 («fun_app$ae» («fun_app$af» «comp$d» A__questionmark_v2) A__questionmark_v3)) % 138.68/138.85 True % 138.68/138.85 Clause #3166 (by clausification #[3165]): ∀ (a : «B_update_c_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «A_update_c_update_fun$»), % 138.68/138.85 Eq % 138.68/138.85 (∀ (A__questionmark_v3 : «C_update_a_update_fun$»), % 138.68/138.85 Eq («comp$aj» a a_1) a_2 → % 138.68/138.85 Eq («comp$» a («fun_app$x» («fun_app$y» «comp$b» a_1) A__questionmark_v3)) % 138.68/138.85 («fun_app$ae» («fun_app$af» «comp$d» a_2) A__questionmark_v3)) % 138.68/138.85 True % 138.68/138.85 Clause #3167 (by clausification #[3166]): ∀ (a : «B_update_c_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «A_update_c_update_fun$») % 138.68/138.85 (a_3 : «C_update_a_update_fun$»), % 138.68/138.85 Eq % 138.68/138.85 (Eq («comp$aj» a a_1) a_2 → % 138.68/138.85 Eq («comp$» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_3)) («fun_app$ae» («fun_app$af» «comp$d» a_2) a_3)) % 138.68/138.85 True % 138.68/138.85 Clause #3168 (by clausification #[3167]): ∀ (a : «B_update_c_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «A_update_c_update_fun$») % 138.68/138.85 (a_3 : «C_update_a_update_fun$»), % 138.68/138.85 Or (Eq (Eq («comp$aj» a a_1) a_2) False) % 138.68/138.85 (Eq (Eq («comp$» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_3)) («fun_app$ae» («fun_app$af» «comp$d» a_2) a_3)) % 138.68/138.85 True) % 138.68/138.85 Clause #3169 (by clausification #[3168]): ∀ (a : «B_update_c_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «C_update_a_update_fun$») % 138.68/138.85 (a_3 : «A_update_c_update_fun$»), % 138.68/138.85 Or % 138.68/138.85 (Eq (Eq («comp$» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_2)) («fun_app$ae» («fun_app$af» «comp$d» a_3) a_2)) % 138.68/138.88 True) % 138.68/138.88 (Ne («comp$aj» a a_1) a_3) % 138.68/138.88 Clause #3170 (by clausification #[3169]): ∀ (a : «B_update_c_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «A_update_c_update_fun$») % 138.68/138.88 (a_3 : «C_update_a_update_fun$»), % 138.68/138.88 Or (Ne («comp$aj» a a_1) a_2) % 138.68/138.88 (Eq («comp$» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_3)) («fun_app$ae» («fun_app$af» «comp$d» a_2) a_3)) % 138.68/138.88 Clause #3171 (by destructive equality resolution #[3170]): ∀ (a : «B_update_c_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «C_update_a_update_fun$»), % 138.68/138.88 Eq («comp$» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_2)) % 138.68/138.88 («fun_app$ae» («fun_app$af» «comp$d» («comp$aj» a a_1)) a_2) % 138.68/138.88 Clause #3178 (by clausification #[142]): ∀ (a : «B_update_b_update_fun$»), % 138.68/138.88 Eq % 138.68/138.88 (∀ (A__questionmark_v1 A__questionmark_v2 : «A_update_b_update_fun$») % 138.68/138.88 (A__questionmark_v3 : «C_update_a_update_fun$»), % 138.68/138.88 Eq («comp$x» a A__questionmark_v1) A__questionmark_v2 → % 138.68/138.88 Eq («comp$i» a («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v1) A__questionmark_v3)) % 138.68/138.88 («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v2) A__questionmark_v3)) % 138.68/138.88 True % 138.68/138.88 Clause #3179 (by clausification #[3178]): ∀ (a : «B_update_b_update_fun$») (a_1 : «A_update_b_update_fun$»), % 138.68/138.88 Eq % 138.68/138.88 (∀ (A__questionmark_v2 : «A_update_b_update_fun$») (A__questionmark_v3 : «C_update_a_update_fun$»), % 138.68/138.88 Eq («comp$x» a a_1) A__questionmark_v2 → % 138.68/138.88 Eq («comp$i» a («fun_app$x» («fun_app$y» «comp$b» a_1) A__questionmark_v3)) % 138.68/138.88 («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v2) A__questionmark_v3)) % 138.68/138.88 True % 138.68/138.88 Clause #3180 (by clausification #[3179]): ∀ (a : «B_update_b_update_fun$») (a_1 a_2 : «A_update_b_update_fun$»), % 138.68/138.88 Eq % 138.68/138.88 (∀ (A__questionmark_v3 : «C_update_a_update_fun$»), % 138.68/138.88 Eq («comp$x» a a_1) a_2 → % 138.68/138.88 Eq («comp$i» a («fun_app$x» («fun_app$y» «comp$b» a_1) A__questionmark_v3)) % 138.72/138.88 («fun_app$x» («fun_app$y» «comp$b» a_2) A__questionmark_v3)) % 138.72/138.88 True % 138.72/138.88 Clause #3181 (by clausification #[3180]): ∀ (a : «B_update_b_update_fun$») (a_1 a_2 : «A_update_b_update_fun$») (a_3 : «C_update_a_update_fun$»), % 138.72/138.88 Eq % 138.72/138.88 (Eq («comp$x» a a_1) a_2 → % 138.72/138.88 Eq («comp$i» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_3)) («fun_app$x» («fun_app$y» «comp$b» a_2) a_3)) % 138.72/138.88 True % 138.72/138.88 Clause #3182 (by clausification #[3181]): ∀ (a : «B_update_b_update_fun$») (a_1 a_2 : «A_update_b_update_fun$») (a_3 : «C_update_a_update_fun$»), % 138.72/138.88 Or (Eq (Eq («comp$x» a a_1) a_2) False) % 138.72/138.88 (Eq (Eq («comp$i» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_3)) («fun_app$x» («fun_app$y» «comp$b» a_2) a_3)) % 138.72/138.88 True) % 138.72/138.88 Clause #3183 (by clausification #[3182]): ∀ (a : «B_update_b_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «C_update_a_update_fun$») % 138.72/138.88 (a_3 : «A_update_b_update_fun$»), % 138.72/138.88 Or % 138.72/138.88 (Eq (Eq («comp$i» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_2)) («fun_app$x» («fun_app$y» «comp$b» a_3) a_2)) % 138.72/138.88 True) % 138.72/138.88 (Ne («comp$x» a a_1) a_3) % 138.72/138.88 Clause #3184 (by clausification #[3183]): ∀ (a : «B_update_b_update_fun$») (a_1 a_2 : «A_update_b_update_fun$») (a_3 : «C_update_a_update_fun$»), % 138.72/138.88 Or (Ne («comp$x» a a_1) a_2) % 138.72/138.88 (Eq («comp$i» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_3)) («fun_app$x» («fun_app$y» «comp$b» a_2) a_3)) % 138.72/138.88 Clause #3185 (by destructive equality resolution #[3184]): ∀ (a : «B_update_b_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «C_update_a_update_fun$»), % 138.72/138.88 Eq («comp$i» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_2)) («fun_app$x» («fun_app$y» «comp$b» («comp$x» a a_1)) a_2) % 138.72/138.88 Clause #3544 (by clausification #[161]): ∀ (a : «B_update_a_update_fun$»), % 138.72/138.88 Eq % 138.72/138.88 (∀ (A__questionmark_v1 : «A_update_b_update_fun$») (A__questionmark_v2 : «C_update_a_update_fun$»), % 138.72/138.88 Eq («comp$aa» («fun_app$ac» («fun_app$ad» «comp$c» a) A__questionmark_v1) A__questionmark_v2) % 138.72/138.91 («comp$ae» a («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v1) A__questionmark_v2))) % 138.72/138.91 True % 138.72/138.91 Clause #3545 (by clausification #[3544]): ∀ (a : «B_update_a_update_fun$») (a_1 : «A_update_b_update_fun$»), % 138.72/138.91 Eq % 138.72/138.91 (∀ (A__questionmark_v2 : «C_update_a_update_fun$»), % 138.72/138.91 Eq («comp$aa» («fun_app$ac» («fun_app$ad» «comp$c» a) a_1) A__questionmark_v2) % 138.72/138.91 («comp$ae» a («fun_app$x» («fun_app$y» «comp$b» a_1) A__questionmark_v2))) % 138.72/138.91 True % 138.72/138.91 Clause #3546 (by clausification #[3545]): ∀ (a : «B_update_a_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «C_update_a_update_fun$»), % 138.72/138.91 Eq % 138.72/138.91 (Eq («comp$aa» («fun_app$ac» («fun_app$ad» «comp$c» a) a_1) a_2) % 138.72/138.91 («comp$ae» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_2))) % 138.72/138.91 True % 138.72/138.91 Clause #3547 (by clausification #[3546]): ∀ (a : «B_update_a_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «C_update_a_update_fun$»), % 138.72/138.91 Eq («comp$aa» («fun_app$ac» («fun_app$ad» «comp$c» a) a_1) a_2) % 138.72/138.91 («comp$ae» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_2)) % 138.72/138.91 Clause #4216 (by forward demodulation #[2834, 3547]): Ne («fun_app$ae» («fun_app$af» «comp$d» «g$») («comp$aa» («fun_app$ac» («fun_app$ad» «comp$c» «f$») «f$a») «g$a»)) «id$» % 138.72/138.91 Clause #4217 (by forward demodulation #[4216, 1187]): Ne («fun_app$ae» («fun_app$af» «comp$d» «g$») («comp$aa» «id$b» «g$a»)) «id$» % 138.72/138.91 Clause #4323 (by eliminate resolved literals #[1642]): Or (Eq («inv_into$b» «top$» «f$a») «f$») (Ne («fun_app$ac» («fun_app$ad» «comp$c» «f$») «f$a») «id$b») % 138.72/138.91 Clause #4324 (by forward demodulation #[4323, 1187]): Or (Eq («inv_into$b» «top$» «f$a») «f$») (Ne «id$b» «id$b») % 138.72/138.91 Clause #4325 (by eliminate resolved literals #[4324]): Eq («inv_into$b» «top$» «f$a») «f$» % 138.72/138.91 Clause #4905 (by clausification #[221]): ∀ (a : «A_update_b_update_fun$»), % 138.72/138.91 Eq % 138.72/138.91 (∀ (A__questionmark_v1 : «B_update_a_update_fun$»), % 138.72/138.91 Eq («fcomp$» a A__questionmark_v1) («fun_app$ac» («fun_app$ad» «comp$c» A__questionmark_v1) a)) % 138.72/138.91 True % 138.72/138.91 Clause #4906 (by clausification #[4905]): ∀ (a : «A_update_b_update_fun$») (a_1 : «B_update_a_update_fun$»), % 138.72/138.91 Eq (Eq («fcomp$» a a_1) («fun_app$ac» («fun_app$ad» «comp$c» a_1) a)) True % 138.72/138.91 Clause #4907 (by clausification #[4906]): ∀ (a : «A_update_b_update_fun$») (a_1 : «B_update_a_update_fun$»), % 138.72/138.91 Eq («fcomp$» a a_1) («fun_app$ac» («fun_app$ad» «comp$c» a_1) a) % 138.72/138.91 Clause #4929 (by backward demodulation #[4907, 3547]): ∀ (a : «A_update_b_update_fun$») (a_1 : «B_update_a_update_fun$») (a_2 : «C_update_a_update_fun$»), % 138.72/138.91 Eq («comp$aa» («fcomp$» a a_1) a_2) («comp$ae» a_1 («fun_app$x» («fun_app$y» «comp$b» a) a_2)) % 138.72/138.91 Clause #4935 (by superposition #[4907, 1187]): Eq («fcomp$» «f$a» «f$») «id$b» % 138.72/138.91 Clause #4948 (by clausification #[222]): ∀ (a : «C_update_a_update_fun$»), % 138.72/138.91 Eq % 138.72/138.91 (∀ (A__questionmark_v1 : «A_update_c_update_fun$»), % 138.72/138.91 Eq («fcomp$a» a A__questionmark_v1) («fun_app$ae» («fun_app$af» «comp$d» A__questionmark_v1) a)) % 138.72/138.91 True % 138.72/138.91 Clause #4949 (by clausification #[4948]): ∀ (a : «C_update_a_update_fun$») (a_1 : «A_update_c_update_fun$»), % 138.72/138.91 Eq (Eq («fcomp$a» a a_1) («fun_app$ae» («fun_app$af» «comp$d» a_1) a)) True % 138.72/138.91 Clause #4950 (by clausification #[4949]): ∀ (a : «C_update_a_update_fun$») (a_1 : «A_update_c_update_fun$»), % 138.72/138.91 Eq («fcomp$a» a a_1) («fun_app$ae» («fun_app$af» «comp$d» a_1) a) % 138.72/138.91 Clause #4953 (by backward demodulation #[4950, 4217]): Ne («fcomp$a» («comp$aa» «id$b» «g$a») «g$») «id$» % 138.72/138.91 Clause #4974 (by backward demodulation #[4950, 3171]): ∀ (a : «B_update_c_update_fun$») (a_1 : «A_update_b_update_fun$») (a_2 : «C_update_a_update_fun$»), % 138.72/138.91 Eq («comp$» a («fun_app$x» («fun_app$y» «comp$b» a_1) a_2)) («fcomp$a» a_2 («comp$aj» a a_1)) % 138.72/138.91 Clause #4978 (by superposition #[4950, 1242]): Eq («fcomp$a» «g$a» «g$») «id$» % 138.72/138.91 Clause #4995 (by clausification #[223]): ∀ (a : «B_update_a_update_fun$»), % 138.78/138.94 Eq % 138.78/138.94 (∀ (A__questionmark_v1 : «A_update_c_update_fun$»), % 138.78/138.94 Eq («fcomp$b» a A__questionmark_v1) («fun_app$v» («fun_app$w» «comp$a» A__questionmark_v1) a)) % 138.78/138.94 True % 138.78/138.94 Clause #4996 (by clausification #[4995]): ∀ (a : «B_update_a_update_fun$») (a_1 : «A_update_c_update_fun$»), % 138.78/138.94 Eq (Eq («fcomp$b» a a_1) («fun_app$v» («fun_app$w» «comp$a» a_1) a)) True % 138.78/138.94 Clause #4997 (by clausification #[4996]): ∀ (a : «B_update_a_update_fun$») (a_1 : «A_update_c_update_fun$»), % 138.78/138.94 Eq («fcomp$b» a a_1) («fun_app$v» («fun_app$w» «comp$a» a_1) a) % 138.78/138.94 Clause #5024 (by clausification #[224]): ∀ (a : «C_update_a_update_fun$»), % 138.78/138.94 Eq % 138.78/138.94 (∀ (A__questionmark_v1 : «A_update_b_update_fun$»), % 138.78/138.94 Eq («fcomp$c» a A__questionmark_v1) («fun_app$x» («fun_app$y» «comp$b» A__questionmark_v1) a)) % 138.78/138.94 True % 138.78/138.94 Clause #5025 (by clausification #[5024]): ∀ (a : «C_update_a_update_fun$») (a_1 : «A_update_b_update_fun$»), % 138.78/138.94 Eq (Eq («fcomp$c» a a_1) («fun_app$x» («fun_app$y» «comp$b» a_1) a)) True % 138.78/138.94 Clause #5026 (by clausification #[5025]): ∀ (a : «C_update_a_update_fun$») (a_1 : «A_update_b_update_fun$»), % 138.78/138.94 Eq («fcomp$c» a a_1) («fun_app$x» («fun_app$y» «comp$b» a_1) a) % 138.78/138.94 Clause #5043 (by backward demodulation #[5026, 3185]): ∀ (a : «B_update_b_update_fun$») (a_1 : «C_update_a_update_fun$») (a_2 : «A_update_b_update_fun$»), % 138.78/138.94 Eq («comp$i» a («fcomp$c» a_1 a_2)) («fun_app$x» («fun_app$y» «comp$b» («comp$x» a a_2)) a_1) % 138.78/138.94 Clause #5046 (by superposition #[5026, 2934]): ∀ (a : «C_update_b_update_fun$»), Eq («comp$i» «id$a» a) («fcomp$c» («comp$ae» «f$» a) «f$a») % 138.78/138.94 Clause #5070 (by clausification #[225]): ∀ (a : «B_update_a_update_fun$»), % 138.78/138.94 Eq % 138.78/138.94 (∀ (A__questionmark_v1 : «A_update_b_update_fun$»), % 138.78/138.94 Eq («fcomp$d» a A__questionmark_v1) («fun_app$aj» («fun_app$ak» «comp$e» A__questionmark_v1) a)) % 138.78/138.94 True % 138.78/138.94 Clause #5071 (by clausification #[5070]): ∀ (a : «B_update_a_update_fun$») (a_1 : «A_update_b_update_fun$»), % 138.78/138.94 Eq (Eq («fcomp$d» a a_1) («fun_app$aj» («fun_app$ak» «comp$e» a_1) a)) True % 138.78/138.94 Clause #5072 (by clausification #[5071]): ∀ (a : «B_update_a_update_fun$») (a_1 : «A_update_b_update_fun$»), % 138.78/138.94 Eq («fcomp$d» a a_1) («fun_app$aj» («fun_app$ak» «comp$e» a_1) a) % 138.78/138.94 Clause #5089 (by superposition #[5072, 1216]): Eq («fcomp$d» «f$» «f$a») «id$a» % 138.78/138.94 Clause #5444 (by superposition #[5043, 5026]): ∀ (a : «C_update_a_update_fun$») (a_1 : «B_update_b_update_fun$») (a_2 : «A_update_b_update_fun$»), % 138.78/138.94 Eq («fcomp$c» a («comp$x» a_1 a_2)) («comp$i» a_1 («fcomp$c» a a_2)) % 138.78/138.94 Clause #5927 (by forward demodulation #[4974, 5026]): ∀ (a : «B_update_c_update_fun$») (a_1 : «C_update_a_update_fun$») (a_2 : «A_update_b_update_fun$»), % 138.78/138.94 Eq («comp$» a («fcomp$c» a_1 a_2)) («fcomp$a» a_1 («comp$aj» a a_2)) % 138.78/138.94 Clause #6255 (by forward demodulation #[4929, 5026]): ∀ (a : «A_update_b_update_fun$») (a_1 : «B_update_a_update_fun$») (a_2 : «C_update_a_update_fun$»), % 138.78/138.94 Eq («comp$aa» («fcomp$» a a_1) a_2) («comp$ae» a_1 («fcomp$c» a_2 a)) % 138.78/138.94 Clause #6258 (by superposition #[6255, 5046]): ∀ (a : «C_update_a_update_fun$») (a_1 : «A_update_b_update_fun$»), % 138.78/138.94 Eq («comp$i» «id$a» («fcomp$c» a a_1)) («fcomp$c» («comp$aa» («fcomp$» a_1 «f$») a) «f$a») % 138.78/138.94 Clause #6296 (by superposition #[6258, 4935]): ∀ (a : «C_update_a_update_fun$»), Eq («comp$i» «id$a» («fcomp$c» a «f$a»)) («fcomp$c» («comp$aa» «id$b» a) «f$a») % 138.78/138.94 Clause #9918 (by clausification #[471]): ∀ (a : «A_update_b_update_fun$»), % 138.78/138.94 Eq % 138.78/138.94 (∀ (A__questionmark_v1 : «A_update_c_update_fun$»), % 138.78/138.94 «inj_on$» a «top$» → % 138.78/138.94 Eq («comp$aj» («fun_app$v» («fun_app$w» «comp$a» A__questionmark_v1) («inv_into$b» «top$» a)) a) % 138.78/138.94 A__questionmark_v1) % 138.78/138.94 True % 138.78/138.94 Clause #9919 (by clausification #[9918]): ∀ (a : «A_update_b_update_fun$») (a_1 : «A_update_c_update_fun$»), % 138.78/138.94 Eq («inj_on$» a «top$» → Eq («comp$aj» («fun_app$v» («fun_app$w» «comp$a» a_1) («inv_into$b» «top$» a)) a) a_1) True % 138.82/138.98 Clause #9920 (by clausification #[9919]): ∀ (a : «A_update_b_update_fun$») (a_1 : «A_update_c_update_fun$»), % 138.82/138.98 Or (Eq («inj_on$» a «top$») False) % 138.82/138.98 (Eq (Eq («comp$aj» («fun_app$v» («fun_app$w» «comp$a» a_1) («inv_into$b» «top$» a)) a) a_1) True) % 138.82/138.98 Clause #9921 (by clausification #[9920]): ∀ (a : «A_update_b_update_fun$») (a_1 : «A_update_c_update_fun$»), % 138.82/138.98 Or (Eq («inj_on$» a «top$») False) % 138.82/138.98 (Eq («comp$aj» («fun_app$v» («fun_app$w» «comp$a» a_1) («inv_into$b» «top$» a)) a) a_1) % 138.82/138.98 Clause #9922 (by forward demodulation #[9921, 4997]): ∀ (a : «A_update_b_update_fun$») (a_1 : «A_update_c_update_fun$»), % 138.82/138.98 Or (Eq («inj_on$» a «top$») False) (Eq («comp$aj» («fcomp$b» («inv_into$b» «top$» a) a_1) a) a_1) % 138.82/138.98 Clause #9923 (by superposition #[9922, 1193]): ∀ (a : «A_update_c_update_fun$»), Or (Eq («comp$aj» («fcomp$b» («inv_into$b» «top$» «f$a») a) «f$a») a) (Eq False True) % 138.82/138.98 Clause #9966 (by clausification #[473]): ∀ (a : «A_update_b_update_fun$»), % 138.82/138.98 Eq % 138.82/138.98 (∀ (A__questionmark_v1 : «A_update_b_update_fun$»), % 138.82/138.98 «inj_on$» a «top$» → % 138.82/138.98 Eq («comp$x» («fun_app$aj» («fun_app$ak» «comp$e» A__questionmark_v1) («inv_into$b» «top$» a)) a) % 138.82/138.98 A__questionmark_v1) % 138.82/138.98 True % 138.82/138.98 Clause #9967 (by clausification #[9966]): ∀ (a a_1 : «A_update_b_update_fun$»), % 138.82/138.98 Eq («inj_on$» a «top$» → Eq («comp$x» («fun_app$aj» («fun_app$ak» «comp$e» a_1) («inv_into$b» «top$» a)) a) a_1) True % 138.82/138.98 Clause #9968 (by clausification #[9967]): ∀ (a a_1 : «A_update_b_update_fun$»), % 138.82/138.98 Or (Eq («inj_on$» a «top$») False) % 138.82/138.98 (Eq (Eq («comp$x» («fun_app$aj» («fun_app$ak» «comp$e» a_1) («inv_into$b» «top$» a)) a) a_1) True) % 138.82/138.98 Clause #9969 (by clausification #[9968]): ∀ (a a_1 : «A_update_b_update_fun$»), % 138.82/138.98 Or (Eq («inj_on$» a «top$») False) % 138.82/138.98 (Eq («comp$x» («fun_app$aj» («fun_app$ak» «comp$e» a_1) («inv_into$b» «top$» a)) a) a_1) % 138.82/138.98 Clause #9970 (by forward demodulation #[9969, 5072]): ∀ (a a_1 : «A_update_b_update_fun$»), % 138.82/138.98 Or (Eq («inj_on$» a «top$») False) (Eq («comp$x» («fcomp$d» («inv_into$b» «top$» a) a_1) a) a_1) % 138.82/138.98 Clause #9971 (by superposition #[9970, 1193]): ∀ (a : «A_update_b_update_fun$»), Or (Eq («comp$x» («fcomp$d» («inv_into$b» «top$» «f$a») a) «f$a») a) (Eq False True) % 138.82/138.98 Clause #10190 (by clausification #[9971]): ∀ (a : «A_update_b_update_fun$»), Eq («comp$x» («fcomp$d» («inv_into$b» «top$» «f$a») a) «f$a») a % 138.82/138.98 Clause #10191 (by forward demodulation #[10190, 4325]): ∀ (a : «A_update_b_update_fun$»), Eq («comp$x» («fcomp$d» «f$» a) «f$a») a % 138.82/138.98 Clause #10199 (by superposition #[10191, 5089]): Eq («comp$x» «id$a» «f$a») «f$a» % 138.82/138.98 Clause #10208 (by superposition #[10199, 5444]): ∀ (a : «C_update_a_update_fun$»), Eq («fcomp$c» a «f$a») («comp$i» «id$a» («fcomp$c» a «f$a»)) % 138.82/138.98 Clause #10238 (by backward demodulation #[10208, 6296]): ∀ (a : «C_update_a_update_fun$»), Eq («fcomp$c» a «f$a») («fcomp$c» («comp$aa» «id$b» a) «f$a») % 138.82/138.98 Clause #10410 (by clausification #[9923]): ∀ (a : «A_update_c_update_fun$»), Eq («comp$aj» («fcomp$b» («inv_into$b» «top$» «f$a») a) «f$a») a % 138.82/138.98 Clause #10411 (by forward demodulation #[10410, 4325]): ∀ (a : «A_update_c_update_fun$»), Eq («comp$aj» («fcomp$b» «f$» a) «f$a») a % 138.82/138.98 Clause #10417 (by superposition #[10411, 5927]): ∀ (a : «A_update_c_update_fun$») (a_1 : «C_update_a_update_fun$»), % 138.82/138.98 Eq («comp$» («fcomp$b» «f$» a) («fcomp$c» a_1 «f$a»)) («fcomp$a» a_1 a) % 138.82/138.98 Clause #10468 (by superposition #[10417, 10238]): ∀ (a : «A_update_c_update_fun$») (a_1 : «C_update_a_update_fun$»), % 138.82/138.98 Eq («comp$» («fcomp$b» «f$» a) («fcomp$c» a_1 «f$a»)) («fcomp$a» («comp$aa» «id$b» a_1) a) % 138.82/138.98 Clause #11186 (by superposition #[10468, 10417]): ∀ (a : «C_update_a_update_fun$») (a_1 : «A_update_c_update_fun$»), % 138.82/138.98 Eq («fcomp$a» («comp$aa» «id$b» a) a_1) («fcomp$a» a a_1) % 138.82/138.98 Clause #11205 (by backward demodulation #[11186, 4953]): Ne («fcomp$a» «g$a» «g$») «id$» % 138.87/139.05 Clause #11218 (by forward demodulation #[11205, 4978]): Ne «id$» «id$» % 138.87/139.05 Clause #11219 (by eliminate resolved literals #[11218]): False % 138.87/139.05 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------