%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP367_1 : TPTP v9.2.0. Released v8.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:52:11 PM UTC 2025 % Result : Theorem 206.04s 206.24s % Output : Proof 206.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : ITP367_1 : TPTP v9.2.0. Released v8.0.0. % 0.08/0.15 % Command : duper %s % 0.16/0.37 % Computer : n012.cluster.edu % 0.16/0.37 % Model : x86_64 x86_64 % 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.37 % Memory : 8042.1875MB % 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.37 % CPULimit : 300 % 0.16/0.37 % WCLimit : 300 % 0.16/0.37 % DateTime : Fri Oct 3 00:48:38 EDT 2025 % 0.16/0.37 % CPUTime : % 206.04/206.24 SZS status Theorem for theBenchmark.p % 206.04/206.24 SZS output start Proof for theBenchmark.p % 206.04/206.24 Clause #2 (by assumption #[]): Eq (Not («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» «x$») «y$»))) True % 206.04/206.24 Clause #4 (by assumption #[]): Eq % 206.04/206.24 (∀ (A__questionmark_v0 A__questionmark_v1 : «A_ltln_set$»), % 206.04/206.24 Iff («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» A__questionmark_v0) A__questionmark_v1)) % 206.04/206.24 (And («fun_app$a» «finite$» A__questionmark_v0) («fun_app$a» «finite$» A__questionmark_v1))) % 206.04/206.24 True % 206.04/206.24 Clause #14 (by assumption #[]): Eq % 206.04/206.24 (∀ (A__questionmark_v0 A__questionmark_v1 : «A_ltln_set$»), % 206.04/206.24 Eq % 206.04/206.24 («fun_app$c» («fun_app$d» «sup$» («fun_app$c» («fun_app$d» «sup$» A__questionmark_v0) A__questionmark_v1)) % 206.04/206.24 A__questionmark_v1) % 206.04/206.24 («fun_app$c» («fun_app$d» «sup$» A__questionmark_v0) A__questionmark_v1)) % 206.04/206.24 True % 206.04/206.24 Clause #22 (by assumption #[]): Eq % 206.04/206.24 (∀ (A__questionmark_v0 A__questionmark_v1 : «A_ltln_set$»), % 206.04/206.24 Eq («fun_app$c» («fun_app$d» «sup$» A__questionmark_v0) A__questionmark_v1) % 206.04/206.25 («fun_app$c» («fun_app$d» «sup$» A__questionmark_v1) A__questionmark_v0)) % 206.04/206.25 True % 206.04/206.25 Clause #36 (by assumption #[]): Eq % 206.04/206.25 (∀ (A__questionmark_v0 A__questionmark_v1 : «A_ltln_set$»), % 206.04/206.25 Iff (Not («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» A__questionmark_v0) A__questionmark_v1))) % 206.04/206.25 (Or (Not («fun_app$a» «finite$» A__questionmark_v0)) (Not («fun_app$a» «finite$» A__questionmark_v1)))) % 206.04/206.25 True % 206.04/206.25 Clause #41 (by assumption #[]): Eq («fun_app$a» («fun_app$g» «less_eq$» «y$») («fun_app$h» «subformulas_nu$» «phi$»)) True % 206.04/206.25 Clause #42 (by assumption #[]): Eq («fun_app$a» («fun_app$g» «less_eq$» «x$») («fun_app$h» «subformulas_mu$» «phi$»)) True % 206.04/206.25 Clause #115 (by assumption #[]): Eq % 206.04/206.25 (∀ (A__questionmark_v0 A__questionmark_v1 : «A_ltln_set$»), % 206.04/206.25 And (Eq A__questionmark_v0 A__questionmark_v1) % 206.04/206.25 (And («fun_app$a» («fun_app$g» «less_eq$» A__questionmark_v0) A__questionmark_v1) % 206.04/206.25 («fun_app$a» («fun_app$g» «less_eq$» A__questionmark_v1) A__questionmark_v0) → % 206.04/206.25 False) → % 206.04/206.25 False) % 206.04/206.25 True % 206.04/206.25 Clause #170 (by assumption #[]): Eq % 206.04/206.25 (∀ (A__questionmark_v0 A__questionmark_v1 : «A_ltln_set$»), % 206.04/206.25 And («fun_app$a» («fun_app$g» «less_eq$» A__questionmark_v0) A__questionmark_v1) % 206.04/206.25 (Eq A__questionmark_v1 («fun_app$c» («fun_app$d» «sup$» A__questionmark_v1) A__questionmark_v0) → False) → % 206.04/206.25 False) % 206.04/206.25 True % 206.04/206.25 Clause #195 (by assumption #[]): Eq (∀ (A__questionmark_v0 : «A_ltln$»), «fun_app$a» «finite$» («fun_app$h» «subformulas_mu$» A__questionmark_v0)) True % 206.04/206.25 Clause #196 (by assumption #[]): Eq (∀ (A__questionmark_v0 : «A_ltln$»), «fun_app$a» «finite$» («fun_app$h» «subformulas_nu$» A__questionmark_v0)) True % 206.04/206.25 Clause #460 (by assumption #[]): Eq % 206.04/206.25 (∀ (A__questionmark_v0 A__questionmark_v1 A__questionmark_v2 : «A_ltln_set$»), % 206.04/206.25 And % 206.04/206.25 («fun_app$a» («fun_app$g» «less_eq$» A__questionmark_v0) % 206.04/206.25 («fun_app$c» («fun_app$d» «inf$» A__questionmark_v1) A__questionmark_v2)) % 206.04/206.25 (And («fun_app$a» («fun_app$g» «less_eq$» A__questionmark_v0) A__questionmark_v1) % 206.04/206.25 («fun_app$a» («fun_app$g» «less_eq$» A__questionmark_v0) A__questionmark_v2) → % 206.04/206.25 False) → % 206.04/206.25 False) % 206.04/206.25 True % 206.04/206.25 Clause #463 (by assumption #[]): Eq % 206.04/206.25 (∀ (A__questionmark_v0 A__questionmark_v1 : «A_ltln_set$»), % 206.04/206.25 And («fun_app$a» («fun_app$g» «less_eq$» A__questionmark_v0) A__questionmark_v1) % 206.04/206.25 (Eq A__questionmark_v0 («fun_app$c» («fun_app$d» «inf$» A__questionmark_v0) A__questionmark_v1) → False) → % 206.04/206.25 False) % 206.04/206.25 True % 206.04/206.25 Clause #532 (by clausification #[170]): ∀ (a : «A_ltln_set$»), % 206.04/206.25 Eq % 206.04/206.25 (∀ (A__questionmark_v1 : «A_ltln_set$»), % 206.04/206.25 And («fun_app$a» («fun_app$g» «less_eq$» a) A__questionmark_v1) % 206.04/206.25 (Eq A__questionmark_v1 («fun_app$c» («fun_app$d» «sup$» A__questionmark_v1) a) → False) → % 206.04/206.25 False) % 206.04/206.25 True % 206.04/206.25 Clause #533 (by clausification #[532]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Eq % 206.04/206.27 (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) (Eq a_1 («fun_app$c» («fun_app$d» «sup$» a_1) a) → False) → False) % 206.04/206.27 True % 206.04/206.27 Clause #534 (by clausification #[533]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Or % 206.04/206.27 (Eq (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) (Eq a_1 («fun_app$c» («fun_app$d» «sup$» a_1) a) → False)) % 206.04/206.27 False) % 206.04/206.27 (Eq False True) % 206.04/206.27 Clause #535 (by clausification #[534]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Or (Eq False True) % 206.04/206.27 (Or (Eq («fun_app$a» («fun_app$g» «less_eq$» a) a_1) False) % 206.04/206.27 (Eq (Eq a_1 («fun_app$c» («fun_app$d» «sup$» a_1) a) → False) False)) % 206.04/206.27 Clause #536 (by clausification #[535]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Or (Eq («fun_app$a» («fun_app$g» «less_eq$» a) a_1) False) % 206.04/206.27 (Eq (Eq a_1 («fun_app$c» («fun_app$d» «sup$» a_1) a) → False) False) % 206.04/206.27 Clause #537 (by clausification #[536]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Or (Eq («fun_app$a» («fun_app$g» «less_eq$» a) a_1) False) (Eq (Eq a_1 («fun_app$c» («fun_app$d» «sup$» a_1) a)) True) % 206.04/206.27 Clause #539 (by clausification #[537]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Or (Eq («fun_app$a» («fun_app$g» «less_eq$» a) a_1) False) (Eq a_1 («fun_app$c» («fun_app$d» «sup$» a_1) a)) % 206.04/206.27 Clause #572 (by clausification #[463]): ∀ (a : «A_ltln_set$»), % 206.04/206.27 Eq % 206.04/206.27 (∀ (A__questionmark_v1 : «A_ltln_set$»), % 206.04/206.27 And («fun_app$a» («fun_app$g» «less_eq$» a) A__questionmark_v1) % 206.04/206.27 (Eq a («fun_app$c» («fun_app$d» «inf$» a) A__questionmark_v1) → False) → % 206.04/206.27 False) % 206.04/206.27 True % 206.04/206.27 Clause #573 (by clausification #[572]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Eq (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) (Eq a («fun_app$c» («fun_app$d» «inf$» a) a_1) → False) → False) % 206.04/206.27 True % 206.04/206.27 Clause #574 (by clausification #[573]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Or % 206.04/206.27 (Eq (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) (Eq a («fun_app$c» («fun_app$d» «inf$» a) a_1) → False)) % 206.04/206.27 False) % 206.04/206.27 (Eq False True) % 206.04/206.27 Clause #575 (by clausification #[574]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Or (Eq False True) % 206.04/206.27 (Or (Eq («fun_app$a» («fun_app$g» «less_eq$» a) a_1) False) % 206.04/206.27 (Eq (Eq a («fun_app$c» («fun_app$d» «inf$» a) a_1) → False) False)) % 206.04/206.27 Clause #576 (by clausification #[575]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Or (Eq («fun_app$a» («fun_app$g» «less_eq$» a) a_1) False) % 206.04/206.27 (Eq (Eq a («fun_app$c» («fun_app$d» «inf$» a) a_1) → False) False) % 206.04/206.27 Clause #577 (by clausification #[576]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Or (Eq («fun_app$a» («fun_app$g» «less_eq$» a) a_1) False) (Eq (Eq a («fun_app$c» («fun_app$d» «inf$» a) a_1)) True) % 206.04/206.27 Clause #578 (by clausification #[577]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Or (Eq («fun_app$a» («fun_app$g» «less_eq$» a) a_1) False) (Eq a («fun_app$c» («fun_app$d» «inf$» a) a_1)) % 206.04/206.27 Clause #579 (by clausification #[2]): Eq («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» «x$») «y$»)) False % 206.04/206.27 Clause #628 (by clausification #[115]): ∀ (a : «A_ltln_set$»), % 206.04/206.27 Eq % 206.04/206.27 (∀ (A__questionmark_v1 : «A_ltln_set$»), % 206.04/206.27 And (Eq a A__questionmark_v1) % 206.04/206.27 (And («fun_app$a» («fun_app$g» «less_eq$» a) A__questionmark_v1) % 206.04/206.27 («fun_app$a» («fun_app$g» «less_eq$» A__questionmark_v1) a) → % 206.04/206.27 False) → % 206.04/206.27 False) % 206.04/206.27 True % 206.04/206.27 Clause #629 (by clausification #[628]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Eq % 206.04/206.27 (And (Eq a a_1) % 206.04/206.27 (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) («fun_app$a» («fun_app$g» «less_eq$» a_1) a) → False) → % 206.04/206.27 False) % 206.04/206.27 True % 206.04/206.27 Clause #630 (by clausification #[629]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Or % 206.04/206.27 (Eq % 206.04/206.27 (And (Eq a a_1) % 206.04/206.27 (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) («fun_app$a» («fun_app$g» «less_eq$» a_1) a) → False)) % 206.04/206.27 False) % 206.04/206.27 (Eq False True) % 206.04/206.27 Clause #631 (by clausification #[630]): ∀ (a a_1 : «A_ltln_set$»), % 206.04/206.27 Or (Eq False True) % 206.04/206.27 (Or (Eq (Eq a a_1) False) % 206.04/206.27 (Eq (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) («fun_app$a» («fun_app$g» «less_eq$» a_1) a) → False) % 206.14/206.29 False)) % 206.14/206.29 Clause #632 (by clausification #[631]): ∀ (a a_1 : «A_ltln_set$»), % 206.14/206.29 Or (Eq (Eq a a_1) False) % 206.14/206.29 (Eq (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) («fun_app$a» («fun_app$g» «less_eq$» a_1) a) → False) False) % 206.14/206.29 Clause #633 (by clausification #[632]): ∀ (a a_1 : «A_ltln_set$»), % 206.14/206.29 Or (Eq (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) («fun_app$a» («fun_app$g» «less_eq$» a_1) a) → False) False) % 206.14/206.29 (Ne a a_1) % 206.14/206.29 Clause #634 (by clausification #[633]): ∀ (a a_1 : «A_ltln_set$»), % 206.14/206.29 Or (Ne a a_1) % 206.14/206.29 (Eq (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) («fun_app$a» («fun_app$g» «less_eq$» a_1) a)) True) % 206.14/206.29 Clause #636 (by clausification #[634]): ∀ (a a_1 : «A_ltln_set$»), Or (Ne a a_1) (Eq («fun_app$a» («fun_app$g» «less_eq$» a_1) a) True) % 206.14/206.29 Clause #638 (by destructive equality resolution #[636]): ∀ (a : «A_ltln_set$»), Eq («fun_app$a» («fun_app$g» «less_eq$» a) a) True % 206.14/206.29 Clause #675 (by clausification #[4]): ∀ (a : «A_ltln_set$»), % 206.14/206.29 Eq % 206.14/206.29 (∀ (A__questionmark_v1 : «A_ltln_set$»), % 206.14/206.29 Iff («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» a) A__questionmark_v1)) % 206.14/206.29 (And («fun_app$a» «finite$» a) («fun_app$a» «finite$» A__questionmark_v1))) % 206.14/206.29 True % 206.14/206.29 Clause #676 (by clausification #[675]): ∀ (a a_1 : «A_ltln_set$»), % 206.14/206.29 Eq % 206.14/206.29 (Iff («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» a) a_1)) % 206.14/206.29 (And («fun_app$a» «finite$» a) («fun_app$a» «finite$» a_1))) % 206.14/206.29 True % 206.14/206.29 Clause #677 (by clausification #[676]): ∀ (a a_1 : «A_ltln_set$»), % 206.14/206.29 Or (Eq («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» a) a_1)) True) % 206.14/206.29 (Eq (And («fun_app$a» «finite$» a) («fun_app$a» «finite$» a_1)) False) % 206.14/206.29 Clause #679 (by clausification #[677]): ∀ (a a_1 : «A_ltln_set$»), % 206.14/206.29 Or (Eq («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» a) a_1)) True) % 206.14/206.29 (Or (Eq («fun_app$a» «finite$» a) False) (Eq («fun_app$a» «finite$» a_1) False)) % 206.14/206.29 Clause #693 (by clausification #[460]): ∀ (a : «A_ltln_set$»), % 206.14/206.29 Eq % 206.14/206.29 (∀ (A__questionmark_v1 A__questionmark_v2 : «A_ltln_set$»), % 206.14/206.29 And % 206.14/206.29 («fun_app$a» («fun_app$g» «less_eq$» a) % 206.14/206.29 («fun_app$c» («fun_app$d» «inf$» A__questionmark_v1) A__questionmark_v2)) % 206.14/206.29 (And («fun_app$a» («fun_app$g» «less_eq$» a) A__questionmark_v1) % 206.14/206.29 («fun_app$a» («fun_app$g» «less_eq$» a) A__questionmark_v2) → % 206.14/206.29 False) → % 206.14/206.29 False) % 206.14/206.29 True % 206.14/206.29 Clause #694 (by clausification #[693]): ∀ (a a_1 : «A_ltln_set$»), % 206.14/206.29 Eq % 206.14/206.29 (∀ (A__questionmark_v2 : «A_ltln_set$»), % 206.14/206.29 And («fun_app$a» («fun_app$g» «less_eq$» a) («fun_app$c» («fun_app$d» «inf$» a_1) A__questionmark_v2)) % 206.14/206.29 (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) % 206.14/206.29 («fun_app$a» («fun_app$g» «less_eq$» a) A__questionmark_v2) → % 206.14/206.29 False) → % 206.14/206.29 False) % 206.14/206.29 True % 206.14/206.29 Clause #695 (by clausification #[694]): ∀ (a a_1 a_2 : «A_ltln_set$»), % 206.14/206.29 Eq % 206.14/206.29 (And («fun_app$a» («fun_app$g» «less_eq$» a) («fun_app$c» («fun_app$d» «inf$» a_1) a_2)) % 206.14/206.29 (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) («fun_app$a» («fun_app$g» «less_eq$» a) a_2) → False) → % 206.14/206.29 False) % 206.14/206.29 True % 206.14/206.29 Clause #696 (by clausification #[695]): ∀ (a a_1 a_2 : «A_ltln_set$»), % 206.14/206.29 Or % 206.14/206.29 (Eq % 206.14/206.29 (And («fun_app$a» («fun_app$g» «less_eq$» a) («fun_app$c» («fun_app$d» «inf$» a_1) a_2)) % 206.14/206.29 (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) («fun_app$a» («fun_app$g» «less_eq$» a) a_2) → False)) % 206.14/206.29 False) % 206.14/206.29 (Eq False True) % 206.14/206.29 Clause #697 (by clausification #[696]): ∀ (a a_1 a_2 : «A_ltln_set$»), % 206.14/206.29 Or (Eq False True) % 206.14/206.29 (Or (Eq («fun_app$a» («fun_app$g» «less_eq$» a) («fun_app$c» («fun_app$d» «inf$» a_1) a_2)) False) % 206.14/206.29 (Eq (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) («fun_app$a» («fun_app$g» «less_eq$» a) a_2) → False) % 206.14/206.29 False)) % 206.14/206.29 Clause #698 (by clausification #[697]): ∀ (a a_1 a_2 : «A_ltln_set$»), % 206.16/206.31 Or (Eq («fun_app$a» («fun_app$g» «less_eq$» a) («fun_app$c» («fun_app$d» «inf$» a_1) a_2)) False) % 206.16/206.31 (Eq (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) («fun_app$a» («fun_app$g» «less_eq$» a) a_2) → False) False) % 206.16/206.31 Clause #699 (by clausification #[698]): ∀ (a a_1 a_2 : «A_ltln_set$»), % 206.16/206.31 Or (Eq («fun_app$a» («fun_app$g» «less_eq$» a) («fun_app$c» («fun_app$d» «inf$» a_1) a_2)) False) % 206.16/206.31 (Eq (And («fun_app$a» («fun_app$g» «less_eq$» a) a_1) («fun_app$a» («fun_app$g» «less_eq$» a) a_2)) True) % 206.16/206.31 Clause #701 (by clausification #[699]): ∀ (a a_1 a_2 : «A_ltln_set$»), % 206.16/206.31 Or (Eq («fun_app$a» («fun_app$g» «less_eq$» a) («fun_app$c» («fun_app$d» «inf$» a_1) a_2)) False) % 206.16/206.31 (Eq («fun_app$a» («fun_app$g» «less_eq$» a) a_2) True) % 206.16/206.31 Clause #703 (by superposition #[701, 638]): ∀ (a a_1 : «A_ltln_set$»), % 206.16/206.31 Or (Eq («fun_app$a» («fun_app$g» «less_eq$» («fun_app$c» («fun_app$d» «inf$» a) a_1)) a_1) True) (Eq False True) % 206.16/206.31 Clause #823 (by clausification #[195]): ∀ (a : «A_ltln$»), Eq («fun_app$a» «finite$» («fun_app$h» «subformulas_mu$» a)) True % 206.16/206.31 Clause #1118 (by clausification #[14]): ∀ (a : «A_ltln_set$»), % 206.16/206.31 Eq % 206.16/206.31 (∀ (A__questionmark_v1 : «A_ltln_set$»), % 206.16/206.31 Eq («fun_app$c» («fun_app$d» «sup$» («fun_app$c» («fun_app$d» «sup$» a) A__questionmark_v1)) A__questionmark_v1) % 206.16/206.31 («fun_app$c» («fun_app$d» «sup$» a) A__questionmark_v1)) % 206.16/206.31 True % 206.16/206.31 Clause #1119 (by clausification #[1118]): ∀ (a a_1 : «A_ltln_set$»), % 206.16/206.31 Eq % 206.16/206.31 (Eq («fun_app$c» («fun_app$d» «sup$» («fun_app$c» («fun_app$d» «sup$» a) a_1)) a_1) % 206.16/206.31 («fun_app$c» («fun_app$d» «sup$» a) a_1)) % 206.16/206.31 True % 206.16/206.31 Clause #1120 (by clausification #[1119]): ∀ (a a_1 : «A_ltln_set$»), % 206.16/206.31 Eq («fun_app$c» («fun_app$d» «sup$» («fun_app$c» («fun_app$d» «sup$» a) a_1)) a_1) % 206.16/206.31 («fun_app$c» («fun_app$d» «sup$» a) a_1) % 206.16/206.31 Clause #1124 (by clausification #[196]): ∀ (a : «A_ltln$»), Eq («fun_app$a» «finite$» («fun_app$h» «subformulas_nu$» a)) True % 206.16/206.31 Clause #1190 (by superposition #[42, 578]): Or (Eq «x$» («fun_app$c» («fun_app$d» «inf$» «x$») («fun_app$h» «subformulas_mu$» «phi$»))) (Eq False True) % 206.16/206.31 Clause #1192 (by superposition #[41, 578]): Or (Eq «y$» («fun_app$c» («fun_app$d» «inf$» «y$») («fun_app$h» «subformulas_nu$» «phi$»))) (Eq False True) % 206.16/206.31 Clause #1430 (by clausification #[22]): ∀ (a : «A_ltln_set$»), % 206.16/206.31 Eq % 206.16/206.31 (∀ (A__questionmark_v1 : «A_ltln_set$»), % 206.16/206.31 Eq («fun_app$c» («fun_app$d» «sup$» a) A__questionmark_v1) % 206.16/206.31 («fun_app$c» («fun_app$d» «sup$» A__questionmark_v1) a)) % 206.16/206.31 True % 206.16/206.31 Clause #1431 (by clausification #[1430]): ∀ (a a_1 : «A_ltln_set$»), % 206.16/206.31 Eq (Eq («fun_app$c» («fun_app$d» «sup$» a) a_1) («fun_app$c» («fun_app$d» «sup$» a_1) a)) True % 206.16/206.31 Clause #1432 (by clausification #[1431]): ∀ (a a_1 : «A_ltln_set$»), Eq («fun_app$c» («fun_app$d» «sup$» a) a_1) («fun_app$c» («fun_app$d» «sup$» a_1) a) % 206.16/206.31 Clause #1433 (by superposition #[1432, 579]): Eq («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» «y$») «x$»)) False % 206.16/206.31 Clause #1910 (by clausification #[36]): ∀ (a : «A_ltln_set$»), % 206.16/206.31 Eq % 206.16/206.31 (∀ (A__questionmark_v1 : «A_ltln_set$»), % 206.16/206.31 Iff (Not («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» a) A__questionmark_v1))) % 206.16/206.31 (Or (Not («fun_app$a» «finite$» a)) (Not («fun_app$a» «finite$» A__questionmark_v1)))) % 206.16/206.31 True % 206.16/206.31 Clause #1911 (by clausification #[1910]): ∀ (a a_1 : «A_ltln_set$»), % 206.16/206.31 Eq % 206.16/206.31 (Iff (Not («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» a) a_1))) % 206.16/206.31 (Or (Not («fun_app$a» «finite$» a)) (Not («fun_app$a» «finite$» a_1)))) % 206.16/206.31 True % 206.16/206.31 Clause #1912 (by clausification #[1911]): ∀ (a a_1 : «A_ltln_set$»), % 206.16/206.31 Or (Eq (Not («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» a) a_1))) True) % 206.16/206.31 (Eq (Or (Not («fun_app$a» «finite$» a)) (Not («fun_app$a» «finite$» a_1))) False) % 206.27/206.50 Clause #1914 (by clausification #[1912]): ∀ (a a_1 : «A_ltln_set$»), % 206.27/206.50 Or (Eq (Or (Not («fun_app$a» «finite$» a)) (Not («fun_app$a» «finite$» a_1))) False) % 206.27/206.50 (Eq («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» a) a_1)) False) % 206.27/206.50 Clause #1915 (by clausification #[1914]): ∀ (a a_1 : «A_ltln_set$»), % 206.27/206.50 Or (Eq («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» a) a_1)) False) % 206.27/206.50 (Eq (Not («fun_app$a» «finite$» a_1)) False) % 206.27/206.50 Clause #1917 (by clausification #[1915]): ∀ (a a_1 : «A_ltln_set$»), % 206.27/206.50 Or (Eq («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» a) a_1)) False) (Eq («fun_app$a» «finite$» a_1) True) % 206.27/206.50 Clause #2002 (by clausification #[1190]): Eq «x$» («fun_app$c» («fun_app$d» «inf$» «x$») («fun_app$h» «subformulas_mu$» «phi$»)) % 206.27/206.50 Clause #2036 (by clausification #[1192]): Eq «y$» («fun_app$c» («fun_app$d» «inf$» «y$») («fun_app$h» «subformulas_nu$» «phi$»)) % 206.27/206.50 Clause #2903 (by clausification #[703]): ∀ (a a_1 : «A_ltln_set$»), Eq («fun_app$a» («fun_app$g» «less_eq$» («fun_app$c» («fun_app$d» «inf$» a) a_1)) a_1) True % 206.27/206.50 Clause #2913 (by superposition #[2903, 539]): ∀ (a a_1 : «A_ltln_set$»), % 206.27/206.50 Or (Eq True False) (Eq a («fun_app$c» («fun_app$d» «sup$» a) («fun_app$c» («fun_app$d» «inf$» a_1) a))) % 206.27/206.50 Clause #2921 (by clausification #[2913]): ∀ (a a_1 : «A_ltln_set$»), Eq a («fun_app$c» («fun_app$d» «sup$» a) («fun_app$c» («fun_app$d» «inf$» a_1) a)) % 206.27/206.50 Clause #2925 (by superposition #[2921, 1120]): ∀ (a a_1 : «A_ltln_set$»), Eq («fun_app$c» («fun_app$d» «sup$» a) («fun_app$c» («fun_app$d» «inf$» a_1) a)) a % 206.27/206.50 Clause #2947 (by superposition #[2925, 2002]): Eq («fun_app$c» («fun_app$d» «sup$» («fun_app$h» «subformulas_mu$» «phi$»)) «x$») («fun_app$h» «subformulas_mu$» «phi$») % 206.27/206.50 Clause #2948 (by superposition #[2925, 2036]): Eq («fun_app$c» («fun_app$d» «sup$» («fun_app$h» «subformulas_nu$» «phi$»)) «y$») («fun_app$h» «subformulas_nu$» «phi$») % 206.27/206.50 Clause #2961 (by superposition #[2948, 1917]): Or (Eq («fun_app$a» «finite$» («fun_app$h» «subformulas_nu$» «phi$»)) False) (Eq («fun_app$a» «finite$» «y$») True) % 206.27/206.50 Clause #2962 (by superposition #[2961, 1124]): Or (Eq («fun_app$a» «finite$» «y$») True) (Eq False True) % 206.27/206.50 Clause #2963 (by clausification #[2962]): Eq («fun_app$a» «finite$» «y$») True % 206.27/206.50 Clause #2966 (by superposition #[2963, 679]): ∀ (a : «A_ltln_set$»), % 206.27/206.50 Or (Eq («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» «y$») a)) True) % 206.27/206.50 (Or (Eq True False) (Eq («fun_app$a» «finite$» a) False)) % 206.27/206.50 Clause #3125 (by superposition #[2947, 1917]): Or (Eq («fun_app$a» «finite$» («fun_app$h» «subformulas_mu$» «phi$»)) False) (Eq («fun_app$a» «finite$» «x$») True) % 206.27/206.50 Clause #3126 (by superposition #[3125, 823]): Or (Eq («fun_app$a» «finite$» «x$») True) (Eq False True) % 206.27/206.50 Clause #3127 (by clausification #[3126]): Eq («fun_app$a» «finite$» «x$») True % 206.27/206.50 Clause #23749 (by clausification #[2966]): ∀ (a : «A_ltln_set$»), % 206.27/206.50 Or (Eq («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» «y$») a)) True) (Eq («fun_app$a» «finite$» a) False) % 206.27/206.50 Clause #23761 (by superposition #[23749, 3127]): Or (Eq («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» «y$») «x$»)) True) (Eq False True) % 206.27/206.50 Clause #23827 (by clausification #[23761]): Eq («fun_app$a» «finite$» («fun_app$c» («fun_app$d» «sup$» «y$») «x$»)) True % 206.27/206.50 Clause #23828 (by superposition #[23827, 1433]): Eq True False % 206.27/206.50 Clause #23863 (by clausification #[23828]): False % 206.27/206.50 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------