%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : AGT014+2 : TPTP v9.2.0. Bugfixed v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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:43:50 PM UTC 2025 % Result : Theorem 83.55s 84.10s % Output : Proof 83.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : AGT014+2 : TPTP v9.2.0. Bugfixed v3.1.0. % 0.07/0.13 % Command : duper %s % 0.12/0.34 % Computer : n021.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 09:02:53 EDT 2025 % 0.12/0.34 % CPUTime : % 83.55/84.10 SZS status Theorem for theBenchmark.p % 83.55/84.10 SZS output start Proof for theBenchmark.p % 83.55/84.10 Clause #13 (by assumption #[]): Eq % 83.55/84.10 (∀ (A : Iota), % 83.55/84.10 Iff % 83.55/84.10 (And % 83.55/84.10 (And % 83.55/84.10 (And (And (accept_population A atheist n12) (accept_population A christian n3)) % 83.55/84.10 (accept_population A muslim n0)) % 83.55/84.10 (accept_population A native n85)) % 83.55/84.10 (accept_population A other n0)) % 83.55/84.10 (accept_city A coastvillage)) % 83.55/84.10 True % 83.55/84.10 Clause #281 (by assumption #[]): Eq (Not (accept_city countryamedicalorganization coastvillage)) True % 83.55/84.10 Clause #885 (by assumption #[]): Eq (Not (Exists fun X => Exists fun Y => Exists fun Z => Not (accept_population X Y Z))) True % 83.55/84.10 Clause #1002 (by clausification #[13]): ∀ (a : Iota), % 83.55/84.10 Eq % 83.55/84.10 (Iff % 83.55/84.10 (And % 83.55/84.10 (And % 83.55/84.10 (And (And (accept_population a atheist n12) (accept_population a christian n3)) % 83.55/84.10 (accept_population a muslim n0)) % 83.55/84.10 (accept_population a native n85)) % 83.55/84.10 (accept_population a other n0)) % 83.55/84.10 (accept_city a coastvillage)) % 83.55/84.10 True % 83.55/84.10 Clause #1004 (by clausification #[1002]): ∀ (a : Iota), % 83.55/84.10 Or % 83.55/84.10 (Eq % 83.55/84.10 (And % 83.55/84.10 (And % 83.55/84.10 (And (And (accept_population a atheist n12) (accept_population a christian n3)) % 83.55/84.10 (accept_population a muslim n0)) % 83.55/84.10 (accept_population a native n85)) % 83.55/84.10 (accept_population a other n0)) % 83.55/84.10 False) % 83.55/84.10 (Eq (accept_city a coastvillage) True) % 83.55/84.10 Clause #1257 (by clausification #[281]): Eq (accept_city countryamedicalorganization coastvillage) False % 83.55/84.10 Clause #10574 (by clausification #[885]): Eq (Exists fun X => Exists fun Y => Exists fun Z => Not (accept_population X Y Z)) False % 83.55/84.10 Clause #10575 (by clausification #[10574]): ∀ (a : Iota), Eq (Exists fun Y => Exists fun Z => Not (accept_population a Y Z)) False % 83.55/84.10 Clause #10576 (by clausification #[10575]): ∀ (a a_1 : Iota), Eq (Exists fun Z => Not (accept_population a a_1 Z)) False % 83.55/84.10 Clause #10577 (by clausification #[10576]): ∀ (a a_1 a_2 : Iota), Eq (Not (accept_population a a_1 a_2)) False % 83.55/84.10 Clause #10578 (by clausification #[10577]): ∀ (a a_1 a_2 : Iota), Eq (accept_population a a_1 a_2) True % 83.55/84.10 Clause #12109 (by clausification #[1004]): ∀ (a : Iota), % 83.55/84.10 Or (Eq (accept_city a coastvillage) True) % 83.55/84.10 (Or % 83.55/84.10 (Eq % 83.55/84.10 (And % 83.55/84.10 (And (And (accept_population a atheist n12) (accept_population a christian n3)) % 83.55/84.10 (accept_population a muslim n0)) % 83.55/84.10 (accept_population a native n85)) % 83.55/84.10 False) % 83.55/84.10 (Eq (accept_population a other n0) False)) % 83.55/84.10 Clause #12110 (by clausification #[12109]): ∀ (a : Iota), % 83.55/84.10 Or (Eq (accept_city a coastvillage) True) % 83.55/84.10 (Or (Eq (accept_population a other n0) False) % 83.55/84.10 (Or % 83.55/84.10 (Eq % 83.55/84.10 (And (And (accept_population a atheist n12) (accept_population a christian n3)) % 83.55/84.10 (accept_population a muslim n0)) % 83.55/84.10 False) % 83.55/84.10 (Eq (accept_population a native n85) False))) % 83.55/84.10 Clause #12111 (by clausification #[12110]): ∀ (a : Iota), % 83.55/84.10 Or (Eq (accept_city a coastvillage) True) % 83.55/84.10 (Or (Eq (accept_population a other n0) False) % 83.55/84.10 (Or (Eq (accept_population a native n85) False) % 83.55/84.10 (Or (Eq (And (accept_population a atheist n12) (accept_population a christian n3)) False) % 83.55/84.10 (Eq (accept_population a muslim n0) False)))) % 83.55/84.10 Clause #12112 (by clausification #[12111]): ∀ (a : Iota), % 83.55/84.10 Or (Eq (accept_city a coastvillage) True) % 83.55/84.10 (Or (Eq (accept_population a other n0) False) % 83.55/84.10 (Or (Eq (accept_population a native n85) False) % 83.55/84.10 (Or (Eq (accept_population a muslim n0) False) % 83.55/84.10 (Or (Eq (accept_population a atheist n12) False) (Eq (accept_population a christian n3) False))))) % 83.55/84.10 Clause #12113 (by forward demodulation #[12112, 10578]): ∀ (a : Iota), % 83.55/84.10 Or (Eq (accept_city a coastvillage) True) % 83.55/84.10 (Or (Eq True False) % 83.55/84.10 (Or (Eq (accept_population a native n85) False) % 83.55/84.10 (Or (Eq (accept_population a muslim n0) False) % 83.55/84.10 (Or (Eq (accept_population a atheist n12) False) (Eq (accept_population a christian n3) False))))) % 83.55/84.10 Clause #12114 (by clausification #[12113]): ∀ (a : Iota), % 83.55/84.10 Or (Eq (accept_city a coastvillage) True) % 83.55/84.10 (Or (Eq (accept_population a native n85) False) % 83.60/84.19 (Or (Eq (accept_population a muslim n0) False) % 83.60/84.19 (Or (Eq (accept_population a atheist n12) False) (Eq (accept_population a christian n3) False)))) % 83.60/84.19 Clause #12115 (by forward demodulation #[12114, 10578]): ∀ (a : Iota), % 83.60/84.19 Or (Eq (accept_city a coastvillage) True) % 83.60/84.19 (Or (Eq (accept_population a native n85) False) % 83.60/84.19 (Or (Eq True False) % 83.60/84.19 (Or (Eq (accept_population a atheist n12) False) (Eq (accept_population a christian n3) False)))) % 83.60/84.19 Clause #12116 (by clausification #[12115]): ∀ (a : Iota), % 83.60/84.19 Or (Eq (accept_city a coastvillage) True) % 83.60/84.19 (Or (Eq (accept_population a native n85) False) % 83.60/84.19 (Or (Eq (accept_population a atheist n12) False) (Eq (accept_population a christian n3) False))) % 83.60/84.19 Clause #12117 (by forward demodulation #[12116, 10578]): ∀ (a : Iota), % 83.60/84.19 Or (Eq (accept_city a coastvillage) True) % 83.60/84.19 (Or (Eq (accept_population a native n85) False) (Or (Eq True False) (Eq (accept_population a christian n3) False))) % 83.60/84.19 Clause #12118 (by clausification #[12117]): ∀ (a : Iota), % 83.60/84.19 Or (Eq (accept_city a coastvillage) True) % 83.60/84.19 (Or (Eq (accept_population a native n85) False) (Eq (accept_population a christian n3) False)) % 83.60/84.19 Clause #12119 (by forward demodulation #[12118, 10578]): ∀ (a : Iota), Or (Eq (accept_city a coastvillage) True) (Or (Eq (accept_population a native n85) False) (Eq True False)) % 83.60/84.19 Clause #12120 (by clausification #[12119]): ∀ (a : Iota), Or (Eq (accept_city a coastvillage) True) (Eq (accept_population a native n85) False) % 83.60/84.19 Clause #12121 (by superposition #[12120, 10578]): ∀ (a : Iota), Or (Eq (accept_city a coastvillage) True) (Eq False True) % 83.60/84.19 Clause #12126 (by clausification #[12121]): ∀ (a : Iota), Eq (accept_city a coastvillage) True % 83.60/84.19 Clause #12128 (by superposition #[12126, 1257]): Eq True False % 83.60/84.19 Clause #12155 (by clausification #[12128]): False % 83.60/84.19 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------