%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP322_1 : TPTP v9.2.0. Released v8.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n026.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:08 PM UTC 2025 % Result : Theorem 5.48s 5.73s % Output : Proof 5.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : ITP322_1 : TPTP v9.2.0. Released v8.0.0. % 0.07/0.13 % Command : duper %s % 0.12/0.34 % Computer : n026.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Oct 2 23:37:53 EDT 2025 % 0.12/0.34 % CPUTime : % 5.48/5.73 SZS status Theorem for theBenchmark.p % 5.48/5.73 SZS output start Proof for theBenchmark.p % 5.48/5.73 Clause #1 (by assumption #[]): Eq % 5.48/5.73 (Not % 5.48/5.73 (Eq «top$» % 5.48/5.73 («fun_app$b» % 5.48/5.73 («fun_app$c» «sup$» («fun_app$b» («fun_app$c» «minus$» «top$») («fun_app$b» («insert$» «a$») «bot$»))) % 5.48/5.73 («fun_app$b» («insert$» «a$») «bot$»)))) % 5.48/5.73 True % 5.48/5.73 Clause #6 (by assumption #[]): Eq % 5.48/5.73 (∀ (A__questionmark_v0 A__questionmark_v1 : «B_set$»), % 5.48/5.73 Eq % 5.48/5.73 («fun_app$b» («fun_app$c» «sup$» («fun_app$b» («fun_app$c» «minus$» A__questionmark_v0) A__questionmark_v1)) % 5.48/5.73 A__questionmark_v1) % 5.48/5.73 («fun_app$b» («fun_app$c» «sup$» A__questionmark_v0) A__questionmark_v1)) % 5.48/5.73 True % 5.48/5.73 Clause #10 (by assumption #[]): Eq % 5.48/5.73 (∀ (A__questionmark_v0 : «B_set$») (A__questionmark_v1 : «B$») (A__questionmark_v2 : «B_set$»), % 5.48/5.73 Eq % 5.48/5.73 («fun_app$b» («fun_app$c» «sup$» A__questionmark_v0) % 5.48/5.73 («fun_app$b» («insert$» A__questionmark_v1) A__questionmark_v2)) % 5.48/5.73 («fun_app$b» («insert$» A__questionmark_v1) % 5.48/5.73 («fun_app$b» («fun_app$c» «sup$» A__questionmark_v0) A__questionmark_v2))) % 5.48/5.73 True % 5.48/5.73 Clause #19 (by assumption #[]): Eq (∀ (A__questionmark_v0 : «B$»), «member$» A__questionmark_v0 «top$») True % 5.48/5.73 Clause #38 (by assumption #[]): Eq % 5.48/5.73 (∀ (A__questionmark_v0 : «B$») (A__questionmark_v1 : «B_set$»), % 5.48/5.73 «member$» A__questionmark_v0 A__questionmark_v1 → % 5.48/5.73 Eq («fun_app$b» («insert$» A__questionmark_v0) A__questionmark_v1) A__questionmark_v1) % 5.48/5.73 True % 5.48/5.73 Clause #145 (by assumption #[]): Eq (∀ (A__questionmark_v0 : «B_set$»), «fun_app$i» («fun_app$j» «less_eq$» «bot$») A__questionmark_v0) True % 5.48/5.73 Clause #246 (by assumption #[]): Eq % 5.48/5.73 (∀ (A__questionmark_v0 A__questionmark_v1 : «B_set$»), % 5.48/5.73 And («fun_app$i» («fun_app$j» «less_eq$» A__questionmark_v0) A__questionmark_v1) % 5.48/5.73 (Eq A__questionmark_v1 («fun_app$b» («fun_app$c» «sup$» A__questionmark_v1) A__questionmark_v0) → False) → % 5.48/5.73 False) % 5.48/5.73 True % 5.48/5.73 Clause #559 (by clausification #[246]): ∀ (a : «B_set$»), % 5.48/5.73 Eq % 5.48/5.73 (∀ (A__questionmark_v1 : «B_set$»), % 5.48/5.73 And («fun_app$i» («fun_app$j» «less_eq$» a) A__questionmark_v1) % 5.48/5.73 (Eq A__questionmark_v1 («fun_app$b» («fun_app$c» «sup$» A__questionmark_v1) a) → False) → % 5.48/5.73 False) % 5.48/5.73 True % 5.48/5.73 Clause #560 (by clausification #[559]): ∀ (a a_1 : «B_set$»), % 5.48/5.73 Eq % 5.48/5.73 (And («fun_app$i» («fun_app$j» «less_eq$» a) a_1) (Eq a_1 («fun_app$b» («fun_app$c» «sup$» a_1) a) → False) → False) % 5.48/5.73 True % 5.48/5.73 Clause #561 (by clausification #[560]): ∀ (a a_1 : «B_set$»), % 5.48/5.73 Or % 5.48/5.73 (Eq (And («fun_app$i» («fun_app$j» «less_eq$» a) a_1) (Eq a_1 («fun_app$b» («fun_app$c» «sup$» a_1) a) → False)) % 5.48/5.73 False) % 5.48/5.73 (Eq False True) % 5.48/5.73 Clause #562 (by clausification #[561]): ∀ (a a_1 : «B_set$»), % 5.48/5.73 Or (Eq False True) % 5.48/5.73 (Or (Eq («fun_app$i» («fun_app$j» «less_eq$» a) a_1) False) % 5.48/5.73 (Eq (Eq a_1 («fun_app$b» («fun_app$c» «sup$» a_1) a) → False) False)) % 5.48/5.73 Clause #563 (by clausification #[562]): ∀ (a a_1 : «B_set$»), % 5.48/5.73 Or (Eq («fun_app$i» («fun_app$j» «less_eq$» a) a_1) False) % 5.48/5.73 (Eq (Eq a_1 («fun_app$b» («fun_app$c» «sup$» a_1) a) → False) False) % 5.48/5.73 Clause #564 (by clausification #[563]): ∀ (a a_1 : «B_set$»), % 5.48/5.73 Or (Eq («fun_app$i» («fun_app$j» «less_eq$» a) a_1) False) (Eq (Eq a_1 («fun_app$b» («fun_app$c» «sup$» a_1) a)) True) % 5.48/5.73 Clause #566 (by clausification #[564]): ∀ (a a_1 : «B_set$»), % 5.48/5.73 Or (Eq («fun_app$i» («fun_app$j» «less_eq$» a) a_1) False) (Eq a_1 («fun_app$b» («fun_app$c» «sup$» a_1) a)) % 5.48/5.73 Clause #568 (by clausification #[1]): Eq % 5.48/5.73 (Eq «top$» % 5.48/5.73 («fun_app$b» («fun_app$c» «sup$» («fun_app$b» («fun_app$c» «minus$» «top$») («fun_app$b» («insert$» «a$») «bot$»))) % 5.48/5.73 («fun_app$b» («insert$» «a$») «bot$»))) % 5.48/5.73 False % 5.48/5.73 Clause #569 (by clausification #[568]): Ne «top$» % 5.48/5.73 («fun_app$b» («fun_app$c» «sup$» («fun_app$b» («fun_app$c» «minus$» «top$») («fun_app$b» («insert$» «a$») «bot$»))) % 5.48/5.73 («fun_app$b» («insert$» «a$») «bot$»)) % 5.58/5.75 Clause #571 (by clausification #[19]): ∀ (a : «B$»), Eq («member$» a «top$») True % 5.58/5.75 Clause #694 (by clausification #[6]): ∀ (a : «B_set$»), % 5.58/5.75 Eq % 5.58/5.75 (∀ (A__questionmark_v1 : «B_set$»), % 5.58/5.75 Eq («fun_app$b» («fun_app$c» «sup$» («fun_app$b» («fun_app$c» «minus$» a) A__questionmark_v1)) A__questionmark_v1) % 5.58/5.75 («fun_app$b» («fun_app$c» «sup$» a) A__questionmark_v1)) % 5.58/5.75 True % 5.58/5.75 Clause #695 (by clausification #[694]): ∀ (a a_1 : «B_set$»), % 5.58/5.75 Eq % 5.58/5.75 (Eq («fun_app$b» («fun_app$c» «sup$» («fun_app$b» («fun_app$c» «minus$» a) a_1)) a_1) % 5.58/5.75 («fun_app$b» («fun_app$c» «sup$» a) a_1)) % 5.58/5.75 True % 5.58/5.75 Clause #696 (by clausification #[695]): ∀ (a a_1 : «B_set$»), % 5.58/5.75 Eq («fun_app$b» («fun_app$c» «sup$» («fun_app$b» («fun_app$c» «minus$» a) a_1)) a_1) % 5.58/5.75 («fun_app$b» («fun_app$c» «sup$» a) a_1) % 5.58/5.75 Clause #697 (by backward demodulation #[696, 569]): Ne «top$» («fun_app$b» («fun_app$c» «sup$» «top$») («fun_app$b» («insert$» «a$») «bot$»)) % 5.58/5.75 Clause #741 (by clausification #[145]): ∀ (a : «B_set$»), Eq («fun_app$i» («fun_app$j» «less_eq$» «bot$») a) True % 5.58/5.75 Clause #743 (by superposition #[741, 566]): ∀ (a : «B_set$»), Or (Eq True False) (Eq a («fun_app$b» («fun_app$c» «sup$» a) «bot$»)) % 5.58/5.75 Clause #815 (by clausification #[10]): ∀ (a : «B_set$»), % 5.58/5.75 Eq % 5.58/5.75 (∀ (A__questionmark_v1 : «B$») (A__questionmark_v2 : «B_set$»), % 5.58/5.75 Eq («fun_app$b» («fun_app$c» «sup$» a) («fun_app$b» («insert$» A__questionmark_v1) A__questionmark_v2)) % 5.58/5.75 («fun_app$b» («insert$» A__questionmark_v1) («fun_app$b» («fun_app$c» «sup$» a) A__questionmark_v2))) % 5.58/5.75 True % 5.58/5.75 Clause #816 (by clausification #[815]): ∀ (a : «B_set$») (a_1 : «B$»), % 5.58/5.75 Eq % 5.58/5.75 (∀ (A__questionmark_v2 : «B_set$»), % 5.58/5.75 Eq («fun_app$b» («fun_app$c» «sup$» a) («fun_app$b» («insert$» a_1) A__questionmark_v2)) % 5.58/5.75 («fun_app$b» («insert$» a_1) («fun_app$b» («fun_app$c» «sup$» a) A__questionmark_v2))) % 5.58/5.75 True % 5.58/5.75 Clause #817 (by clausification #[816]): ∀ (a : «B_set$») (a_1 : «B$») (a_2 : «B_set$»), % 5.58/5.75 Eq % 5.58/5.75 (Eq («fun_app$b» («fun_app$c» «sup$» a) («fun_app$b» («insert$» a_1) a_2)) % 5.58/5.75 («fun_app$b» («insert$» a_1) («fun_app$b» («fun_app$c» «sup$» a) a_2))) % 5.58/5.75 True % 5.58/5.75 Clause #818 (by clausification #[817]): ∀ (a : «B_set$») (a_1 : «B$») (a_2 : «B_set$»), % 5.58/5.75 Eq («fun_app$b» («fun_app$c» «sup$» a) («fun_app$b» («insert$» a_1) a_2)) % 5.58/5.75 («fun_app$b» («insert$» a_1) («fun_app$b» («fun_app$c» «sup$» a) a_2)) % 5.58/5.75 Clause #1333 (by clausification #[743]): ∀ (a : «B_set$»), Eq a («fun_app$b» («fun_app$c» «sup$» a) «bot$») % 5.58/5.75 Clause #1344 (by clausification #[38]): ∀ (a : «B$»), % 5.58/5.75 Eq % 5.58/5.75 (∀ (A__questionmark_v1 : «B_set$»), % 5.58/5.75 «member$» a A__questionmark_v1 → Eq («fun_app$b» («insert$» a) A__questionmark_v1) A__questionmark_v1) % 5.58/5.75 True % 5.58/5.75 Clause #1345 (by clausification #[1344]): ∀ (a : «B$») (a_1 : «B_set$»), Eq («member$» a a_1 → Eq («fun_app$b» («insert$» a) a_1) a_1) True % 5.58/5.75 Clause #1346 (by clausification #[1345]): ∀ (a : «B$») (a_1 : «B_set$»), Or (Eq («member$» a a_1) False) (Eq (Eq («fun_app$b» («insert$» a) a_1) a_1) True) % 5.58/5.75 Clause #1347 (by clausification #[1346]): ∀ (a : «B$») (a_1 : «B_set$»), Or (Eq («member$» a a_1) False) (Eq («fun_app$b» («insert$» a) a_1) a_1) % 5.58/5.75 Clause #1348 (by superposition #[1347, 571]): ∀ (a : «B$»), Or (Eq («fun_app$b» («insert$» a) «top$») «top$») (Eq False True) % 5.58/5.75 Clause #1355 (by clausification #[1348]): ∀ (a : «B$»), Eq («fun_app$b» («insert$» a) «top$») «top$» % 5.58/5.75 Clause #1643 (by forward demodulation #[697, 818]): Ne «top$» («fun_app$b» («insert$» «a$») («fun_app$b» («fun_app$c» «sup$» «top$») «bot$»)) % 5.58/5.75 Clause #1644 (by forward demodulation #[1643, 1333]): Ne «top$» («fun_app$b» («insert$» «a$») «top$») % 5.58/5.75 Clause #1645 (by forward demodulation #[1644, 1355]): Ne «top$» «top$» % 5.58/5.75 Clause #1646 (by eliminate resolved literals #[1645]): False % 5.58/5.75 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------