%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWB017+2 : TPTP v9.2.0. Released v5.2.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 08:03:25 PM UTC 2025 % Result : Theorem 5.03s 5.26s % Output : Proof 5.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.14 % Problem : SWB017+2 : TPTP v9.2.0. Released v5.2.0. % 0.09/0.15 % Command : duper %s % 0.15/0.37 % Computer : n026.cluster.edu % 0.15/0.37 % Model : x86_64 x86_64 % 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.37 % Memory : 8042.1875MB % 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.37 % CPULimit : 300 % 0.15/0.37 % WCLimit : 300 % 0.15/0.37 % DateTime : Thu Oct 2 11:48:23 EDT 2025 % 0.15/0.37 % CPUTime : % 5.03/5.26 SZS status Theorem for theBenchmark.p % 5.03/5.26 SZS output start Proof for theBenchmark.p % 5.03/5.26 Clause #0 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (iext uri_owl_differentFrom X Y) (Ne X Y)) True % 5.03/5.26 Clause #1 (by assumption #[]): Eq % 5.03/5.26 (∀ (P1 P2 : Iota), % 5.03/5.26 Iff (iext uri_owl_propertyDisjointWith P1 P2) % 5.03/5.26 (And (And (ip P1) (ip P2)) (∀ (X Y : Iota), Not (And (iext P1 X Y) (iext P2 X Y))))) % 5.03/5.26 True % 5.03/5.26 Clause #2 (by assumption #[]): Eq (Not (iext uri_owl_differentFrom uri_ex_w uri_ex_u)) True % 5.03/5.26 Clause #3 (by assumption #[]): Eq % 5.03/5.26 (And (And (iext uri_owl_propertyDisjointWith uri_ex_notInstanceOf uri_rdf_type) (iext uri_rdf_type uri_ex_w uri_ex_c)) % 5.03/5.26 (iext uri_ex_notInstanceOf uri_ex_u uri_ex_c)) % 5.03/5.26 True % 5.03/5.26 Clause #4 (by clausification #[2]): Eq (iext uri_owl_differentFrom uri_ex_w uri_ex_u) False % 5.03/5.26 Clause #5 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (iext uri_owl_differentFrom a Y) (Ne a Y)) True % 5.03/5.26 Clause #6 (by clausification #[5]): ∀ (a a_1 : Iota), Eq (Iff (iext uri_owl_differentFrom a a_1) (Ne a a_1)) True % 5.03/5.27 Clause #7 (by clausification #[6]): ∀ (a a_1 : Iota), Or (Eq (iext uri_owl_differentFrom a a_1) True) (Eq (Ne a a_1) False) % 5.03/5.27 Clause #9 (by clausification #[7]): ∀ (a a_1 : Iota), Or (Eq (iext uri_owl_differentFrom a a_1) True) (Eq a a_1) % 5.03/5.27 Clause #10 (by superposition #[9, 4]): Or (Eq uri_ex_w uri_ex_u) (Eq True False) % 5.03/5.27 Clause #19 (by clausification #[10]): Eq uri_ex_w uri_ex_u % 5.03/5.27 Clause #29 (by clausification #[1]): ∀ (a : Iota), % 5.03/5.27 Eq % 5.03/5.27 (∀ (P2 : Iota), % 5.03/5.27 Iff (iext uri_owl_propertyDisjointWith a P2) % 5.03/5.27 (And (And (ip a) (ip P2)) (∀ (X Y : Iota), Not (And (iext a X Y) (iext P2 X Y))))) % 5.03/5.27 True % 5.03/5.27 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), % 5.03/5.27 Eq % 5.03/5.27 (Iff (iext uri_owl_propertyDisjointWith a a_1) % 5.03/5.27 (And (And (ip a) (ip a_1)) (∀ (X Y : Iota), Not (And (iext a X Y) (iext a_1 X Y))))) % 5.03/5.27 True % 5.03/5.27 Clause #32 (by clausification #[30]): ∀ (a a_1 : Iota), % 5.03/5.27 Or (Eq (iext uri_owl_propertyDisjointWith a a_1) False) % 5.03/5.27 (Eq (And (And (ip a) (ip a_1)) (∀ (X Y : Iota), Not (And (iext a X Y) (iext a_1 X Y)))) True) % 5.03/5.27 Clause #43 (by clausification #[3]): Eq (iext uri_ex_notInstanceOf uri_ex_u uri_ex_c) True % 5.03/5.27 Clause #44 (by clausification #[3]): Eq (And (iext uri_owl_propertyDisjointWith uri_ex_notInstanceOf uri_rdf_type) (iext uri_rdf_type uri_ex_w uri_ex_c)) % 5.03/5.27 True % 5.03/5.27 Clause #45 (by forward demodulation #[43, 19]): Eq (iext uri_ex_notInstanceOf uri_ex_w uri_ex_c) True % 5.03/5.27 Clause #70 (by clausification #[44]): Eq (iext uri_rdf_type uri_ex_w uri_ex_c) True % 5.03/5.27 Clause #71 (by clausification #[44]): Eq (iext uri_owl_propertyDisjointWith uri_ex_notInstanceOf uri_rdf_type) True % 5.03/5.27 Clause #438 (by clausification #[32]): ∀ (a a_1 : Iota), % 5.03/5.27 Or (Eq (iext uri_owl_propertyDisjointWith a a_1) False) % 5.03/5.27 (Eq (∀ (X Y : Iota), Not (And (iext a X Y) (iext a_1 X Y))) True) % 5.03/5.27 Clause #440 (by clausification #[438]): ∀ (a a_1 a_2 : Iota), % 5.03/5.27 Or (Eq (iext uri_owl_propertyDisjointWith a a_1) False) % 5.03/5.27 (Eq (∀ (Y : Iota), Not (And (iext a a_2 Y) (iext a_1 a_2 Y))) True) % 5.03/5.27 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 : Iota), % 5.03/5.27 Or (Eq (iext uri_owl_propertyDisjointWith a a_1) False) (Eq (Not (And (iext a a_2 a_3) (iext a_1 a_2 a_3))) True) % 5.03/5.27 Clause #442 (by clausification #[441]): ∀ (a a_1 a_2 a_3 : Iota), % 5.03/5.27 Or (Eq (iext uri_owl_propertyDisjointWith a a_1) False) (Eq (And (iext a a_2 a_3) (iext a_1 a_2 a_3)) False) % 5.03/5.27 Clause #443 (by clausification #[442]): ∀ (a a_1 a_2 a_3 : Iota), % 5.03/5.27 Or (Eq (iext uri_owl_propertyDisjointWith a a_1) False) (Or (Eq (iext a a_2 a_3) False) (Eq (iext a_1 a_2 a_3) False)) % 5.03/5.27 Clause #444 (by superposition #[443, 71]): ∀ (a a_1 : Iota), % 5.03/5.27 Or (Eq (iext uri_ex_notInstanceOf a a_1) False) (Or (Eq (iext uri_rdf_type a a_1) False) (Eq False True)) % 5.03/5.27 Clause #581 (by clausification #[444]): ∀ (a a_1 : Iota), Or (Eq (iext uri_ex_notInstanceOf a a_1) False) (Eq (iext uri_rdf_type a a_1) False) % 5.03/5.27 Clause #582 (by superposition #[581, 45]): Or (Eq (iext uri_rdf_type uri_ex_w uri_ex_c) False) (Eq False True) % 5.03/5.27 Clause #591 (by clausification #[582]): Eq (iext uri_rdf_type uri_ex_w uri_ex_c) False % 5.03/5.27 Clause #592 (by superposition #[591, 70]): Eq False True % 5.03/5.27 Clause #640 (by clausification #[592]): False % 5.03/5.27 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------