%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR144^1 : TPTP v9.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n010.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:46:53 PM UTC 2025 % Result : Theorem 5.93s 6.15s % Output : Proof 6.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : CSR144^1 : TPTP v9.2.0. Released v4.1.0. % 0.11/0.14 % Command : duper %s % 0.13/0.35 % Computer : n010.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Oct 2 20:19:23 EDT 2025 % 0.13/0.35 % CPUTime : % 5.93/6.15 SZS status Theorem for theBenchmark.p % 5.93/6.15 SZS output start Proof for theBenchmark.p % 5.93/6.15 Clause #0 (by assumption #[]): Eq (inverse_THFTYPE_IIiioIIiioIoI husband_THFTYPE_IiioI wife_THFTYPE_IiioI) True % 5.93/6.15 Clause #1 (by assumption #[]): Eq % 5.93/6.15 (∀ (REL2 REL1 : Iota → Iota → Prop), % 5.93/6.15 inverse_THFTYPE_IIiioIIiioIoI REL1 REL2 → ∀ (INST1 INST2 : Iota), Iff (REL1 INST1 INST2) (REL2 INST2 INST1)) % 5.93/6.15 True % 5.93/6.15 Clause #2 (by assumption #[]): Eq % 5.93/6.15 (∀ (FORMULA : Prop) (AGENT : Iota), % 5.93/6.15 believes_THFTYPE_IiooI AGENT FORMULA → % 5.93/6.15 Exists fun TIME => holdsDuring_THFTYPE_IiooI TIME (considers_THFTYPE_IiooI AGENT FORMULA)) % 5.93/6.15 True % 5.93/6.15 Clause #3 (by assumption #[]): Eq % 5.93/6.15 (∀ (X : Iota), % 5.93/6.15 Not % 5.93/6.15 (Exists fun Z => % 5.93/6.15 holdsDuring_THFTYPE_IiooI Z (considers_THFTYPE_IiooI lMax_THFTYPE_i (wife_THFTYPE_IiioI X lMax_THFTYPE_i)))) % 5.93/6.15 True % 5.93/6.15 Clause #4 (by assumption #[]): Eq (Not (Exists fun Z => Not (believes_THFTYPE_IiooI lMax_THFTYPE_i (husband_THFTYPE_IiioI lMax_THFTYPE_i Z)))) True % 5.93/6.15 Clause #5 (by clausification #[4]): Eq (Exists fun Z => Not (believes_THFTYPE_IiooI lMax_THFTYPE_i (husband_THFTYPE_IiioI lMax_THFTYPE_i Z))) False % 5.93/6.15 Clause #6 (by clausification #[5]): ∀ (a : Iota), Eq (Not (believes_THFTYPE_IiooI lMax_THFTYPE_i (husband_THFTYPE_IiioI lMax_THFTYPE_i a))) False % 5.93/6.15 Clause #7 (by clausification #[6]): ∀ (a : Iota), Eq (believes_THFTYPE_IiooI lMax_THFTYPE_i (husband_THFTYPE_IiioI lMax_THFTYPE_i a)) True % 5.93/6.15 Clause #8 (by identity loobHoist #[7]): ∀ (a : Iota), % 5.93/6.15 Or (Eq (believes_THFTYPE_IiooI lMax_THFTYPE_i True) True) (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) False) % 5.93/6.15 Clause #9 (by identity boolHoist #[7]): ∀ (a : Iota), % 5.93/6.15 Or (Eq (believes_THFTYPE_IiooI lMax_THFTYPE_i False) True) (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 5.93/6.15 Clause #12 (by clausification #[2]): ∀ (a : Prop), % 5.93/6.15 Eq % 5.93/6.15 (∀ (AGENT : Iota), % 5.93/6.15 believes_THFTYPE_IiooI AGENT a → % 5.93/6.15 Exists fun TIME => holdsDuring_THFTYPE_IiooI TIME (considers_THFTYPE_IiooI AGENT a)) % 5.93/6.15 True % 5.93/6.15 Clause #13 (by clausification #[12]): ∀ (a : Iota) (a_1 : Prop), % 5.93/6.15 Eq (believes_THFTYPE_IiooI a a_1 → Exists fun TIME => holdsDuring_THFTYPE_IiooI TIME (considers_THFTYPE_IiooI a a_1)) % 5.93/6.15 True % 5.93/6.15 Clause #14 (by clausification #[13]): ∀ (a : Iota) (a_1 : Prop), % 5.93/6.15 Or (Eq (believes_THFTYPE_IiooI a a_1) False) % 5.93/6.15 (Eq (Exists fun TIME => holdsDuring_THFTYPE_IiooI TIME (considers_THFTYPE_IiooI a a_1)) True) % 5.93/6.15 Clause #15 (by clausification #[14]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 5.93/6.15 Or (Eq (believes_THFTYPE_IiooI a a_1) False) % 5.93/6.15 (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a a_1 a_2) (considers_THFTYPE_IiooI a a_1)) True) % 5.93/6.15 Clause #16 (by identity loobHoist #[15]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 5.93/6.15 Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a a_1 a_2) (considers_THFTYPE_IiooI a a_1)) True) % 5.93/6.15 (Or (Eq (believes_THFTYPE_IiooI a True) False) (Eq a_1 False)) % 5.93/6.15 Clause #17 (by identity boolHoist #[15]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 5.93/6.15 Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a a_1 a_2) (considers_THFTYPE_IiooI a a_1)) True) % 5.93/6.15 (Or (Eq (believes_THFTYPE_IiooI a False) False) (Eq a_1 True)) % 5.93/6.15 Clause #18 (by identity loobHoist #[16]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 5.93/6.15 Or (Eq (believes_THFTYPE_IiooI a True) False) % 5.93/6.15 (Or (Eq a_1 False) % 5.93/6.15 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a a_1 a_2) True) True) (Eq (considers_THFTYPE_IiooI a a_1) False))) % 5.93/6.15 Clause #19 (by identity boolHoist #[16]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 5.93/6.15 Or (Eq (believes_THFTYPE_IiooI a True) False) % 5.93/6.15 (Or (Eq a_1 False) % 5.93/6.15 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a a_1 a_2) False) True) (Eq (considers_THFTYPE_IiooI a a_1) True))) % 5.93/6.15 Clause #20 (by identity loobHoist #[18]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 5.93/6.15 Or (Eq (believes_THFTYPE_IiooI a True) False) % 5.93/6.15 (Or (Eq a_1 False) % 5.93/6.15 (Or (Eq (considers_THFTYPE_IiooI a a_1) False) % 5.93/6.15 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a True a_2) True) True) (Eq a_1 False)))) % 5.93/6.15 Clause #22 (by eliminate duplicate literals #[20]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 5.93/6.15 Or (Eq (believes_THFTYPE_IiooI a True) False) % 5.93/6.15 (Or (Eq a_1 False) % 5.93/6.18 (Or (Eq (considers_THFTYPE_IiooI a a_1) False) (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a True a_2) True) True))) % 5.93/6.18 Clause #23 (by identity loobHoist #[22]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 5.93/6.18 Or (Eq (believes_THFTYPE_IiooI a True) False) % 5.93/6.18 (Or (Eq a_1 False) % 5.93/6.18 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a True a_2) True) True) % 5.93/6.18 (Or (Eq (considers_THFTYPE_IiooI a True) False) (Eq a_1 False)))) % 5.93/6.18 Clause #25 (by eliminate duplicate literals #[23]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 5.93/6.18 Or (Eq (believes_THFTYPE_IiooI a True) False) % 5.93/6.18 (Or (Eq a_1 False) % 5.93/6.18 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a True a_2) True) True) (Eq (considers_THFTYPE_IiooI a True) False))) % 5.93/6.18 Clause #26 (by clausification #[1]): ∀ (a : Iota → Iota → Prop), % 5.93/6.18 Eq % 5.93/6.18 (∀ (REL1 : Iota → Iota → Prop), % 5.93/6.18 inverse_THFTYPE_IIiioIIiioIoI REL1 a → ∀ (INST1 INST2 : Iota), Iff (REL1 INST1 INST2) (a INST2 INST1)) % 5.93/6.18 True % 5.93/6.18 Clause #27 (by clausification #[26]): ∀ (a a_1 : Iota → Iota → Prop), % 5.93/6.18 Eq (inverse_THFTYPE_IIiioIIiioIoI a a_1 → ∀ (INST1 INST2 : Iota), Iff (a INST1 INST2) (a_1 INST2 INST1)) True % 5.93/6.18 Clause #28 (by clausification #[27]): ∀ (a a_1 : Iota → Iota → Prop), % 5.93/6.18 Or (Eq (inverse_THFTYPE_IIiioIIiioIoI a a_1) False) % 5.93/6.18 (Eq (∀ (INST1 INST2 : Iota), Iff (a INST1 INST2) (a_1 INST2 INST1)) True) % 5.93/6.18 Clause #29 (by clausification #[28]): ∀ (a a_1 : Iota → Iota → Prop) (a_2 : Iota), % 5.93/6.18 Or (Eq (inverse_THFTYPE_IIiioIIiioIoI a a_1) False) (Eq (∀ (INST2 : Iota), Iff (a a_2 INST2) (a_1 INST2 a_2)) True) % 5.93/6.18 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota → Iota → Prop) (a_2 a_3 : Iota), % 5.93/6.18 Or (Eq (inverse_THFTYPE_IIiioIIiioIoI a a_1) False) (Eq (Iff (a a_2 a_3) (a_1 a_3 a_2)) True) % 5.93/6.18 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota → Iota → Prop) (a_2 a_3 : Iota), % 5.93/6.18 Or (Eq (inverse_THFTYPE_IIiioIIiioIoI a a_1) False) (Or (Eq (a a_2 a_3) True) (Eq (a_1 a_3 a_2) False)) % 5.93/6.18 Clause #32 (by clausification #[30]): ∀ (a a_1 : Iota → Iota → Prop) (a_2 a_3 : Iota), % 5.93/6.18 Or (Eq (inverse_THFTYPE_IIiioIIiioIoI a a_1) False) (Or (Eq (a a_2 a_3) False) (Eq (a_1 a_3 a_2) True)) % 5.93/6.18 Clause #33 (by superposition #[31, 0]): ∀ (a a_1 : Iota), % 5.93/6.18 Or (Eq ((fun x x_1 => husband_THFTYPE_IiioI x x_1) a a_1) True) % 5.93/6.18 (Or (Eq ((fun x x_1 => wife_THFTYPE_IiioI x x_1) a_1 a) False) (Eq False True)) % 5.93/6.18 Clause #34 (by superposition #[32, 0]): ∀ (a a_1 : Iota), % 5.93/6.18 Or (Eq ((fun x x_1 => husband_THFTYPE_IiioI x x_1) a a_1) False) % 5.93/6.18 (Or (Eq ((fun x x_1 => wife_THFTYPE_IiioI x x_1) a_1 a) True) (Eq False True)) % 5.93/6.18 Clause #35 (by clausification #[3]): ∀ (a : Iota), % 5.93/6.18 Eq % 5.93/6.18 (Not % 5.93/6.18 (Exists fun Z => % 5.93/6.18 holdsDuring_THFTYPE_IiooI Z (considers_THFTYPE_IiooI lMax_THFTYPE_i (wife_THFTYPE_IiioI a lMax_THFTYPE_i)))) % 5.93/6.18 True % 5.93/6.18 Clause #36 (by clausification #[35]): ∀ (a : Iota), % 5.93/6.18 Eq % 5.93/6.18 (Exists fun Z => % 5.93/6.18 holdsDuring_THFTYPE_IiooI Z (considers_THFTYPE_IiooI lMax_THFTYPE_i (wife_THFTYPE_IiioI a lMax_THFTYPE_i))) % 5.93/6.18 False % 5.93/6.18 Clause #37 (by clausification #[36]): ∀ (a a_1 : Iota), % 5.93/6.18 Eq (holdsDuring_THFTYPE_IiooI a (considers_THFTYPE_IiooI lMax_THFTYPE_i (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i))) % 5.93/6.18 False % 5.93/6.18 Clause #38 (by identity loobHoist #[37]): ∀ (a a_1 : Iota), % 5.93/6.18 Or (Eq (holdsDuring_THFTYPE_IiooI a True) False) % 5.93/6.18 (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i)) False) % 5.93/6.18 Clause #39 (by identity boolHoist #[37]): ∀ (a a_1 : Iota), % 5.93/6.18 Or (Eq (holdsDuring_THFTYPE_IiooI a False) False) % 5.93/6.18 (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i)) True) % 5.93/6.18 Clause #40 (by identity loobHoist #[38]): ∀ (a a_1 : Iota), % 5.93/6.18 Or (Eq (holdsDuring_THFTYPE_IiooI a True) False) % 5.93/6.18 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) False) (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) False)) % 5.93/6.18 Clause #41 (by identity boolHoist #[38]): ∀ (a a_1 : Iota), % 5.93/6.18 Or (Eq (holdsDuring_THFTYPE_IiooI a True) False) % 5.93/6.18 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) False) (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) True)) % 5.93/6.18 Clause #42 (by identity loobHoist #[39]): ∀ (a a_1 : Iota), % 6.02/6.20 Or (Eq (holdsDuring_THFTYPE_IiooI a False) False) % 6.02/6.20 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) True) (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) False)) % 6.02/6.20 Clause #43 (by identity boolHoist #[39]): ∀ (a a_1 : Iota), % 6.02/6.20 Or (Eq (holdsDuring_THFTYPE_IiooI a False) False) % 6.02/6.20 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) True)) % 6.02/6.20 Clause #44 (by identity loobHoist #[17]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.20 Or (Eq (believes_THFTYPE_IiooI a False) False) % 6.02/6.20 (Or (Eq a_1 True) % 6.02/6.20 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a a_1 a_2) True) True) (Eq (considers_THFTYPE_IiooI a a_1) False))) % 6.02/6.20 Clause #45 (by identity boolHoist #[17]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.20 Or (Eq (believes_THFTYPE_IiooI a False) False) % 6.02/6.20 (Or (Eq a_1 True) % 6.02/6.20 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a a_1 a_2) False) True) (Eq (considers_THFTYPE_IiooI a a_1) True))) % 6.02/6.20 Clause #47 (by identity boolHoist #[44]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.20 Or (Eq (believes_THFTYPE_IiooI a False) False) % 6.02/6.20 (Or (Eq a_1 True) % 6.02/6.20 (Or (Eq (considers_THFTYPE_IiooI a a_1) False) % 6.02/6.20 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a False a_2) True) True) (Eq a_1 True)))) % 6.02/6.20 Clause #48 (by betaEtaReduce #[34]): ∀ (a a_1 : Iota), Or (Eq (husband_THFTYPE_IiioI a a_1) False) (Or (Eq (wife_THFTYPE_IiioI a_1 a) True) (Eq False True)) % 6.02/6.20 Clause #49 (by clausification #[48]): ∀ (a a_1 : Iota), Or (Eq (husband_THFTYPE_IiioI a a_1) False) (Eq (wife_THFTYPE_IiioI a_1 a) True) % 6.02/6.20 Clause #52 (by betaEtaReduce #[33]): ∀ (a a_1 : Iota), Or (Eq (husband_THFTYPE_IiioI a a_1) True) (Or (Eq (wife_THFTYPE_IiioI a_1 a) False) (Eq False True)) % 6.02/6.20 Clause #53 (by clausification #[52]): ∀ (a a_1 : Iota), Or (Eq (husband_THFTYPE_IiioI a a_1) True) (Eq (wife_THFTYPE_IiioI a_1 a) False) % 6.02/6.20 Clause #57 (by identity boolHoist #[45]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.20 Or (Eq (believes_THFTYPE_IiooI a False) False) % 6.02/6.20 (Or (Eq a_1 True) % 6.02/6.20 (Or (Eq (considers_THFTYPE_IiooI a a_1) True) % 6.02/6.20 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a False a_2) False) True) (Eq a_1 True)))) % 6.02/6.20 Clause #58 (by identity loobHoist #[19]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.20 Or (Eq (believes_THFTYPE_IiooI a True) False) % 6.02/6.20 (Or (Eq a_1 False) % 6.02/6.20 (Or (Eq (considers_THFTYPE_IiooI a a_1) True) % 6.02/6.20 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a True a_2) False) True) (Eq a_1 False)))) % 6.02/6.20 Clause #60 (by eliminate duplicate literals #[58]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.20 Or (Eq (believes_THFTYPE_IiooI a True) False) % 6.02/6.20 (Or (Eq a_1 False) % 6.02/6.20 (Or (Eq (considers_THFTYPE_IiooI a a_1) True) (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a True a_2) False) True))) % 6.02/6.20 Clause #61 (by identity loobHoist #[60]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.20 Or (Eq (believes_THFTYPE_IiooI a True) False) % 6.02/6.20 (Or (Eq a_1 False) % 6.02/6.20 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a True a_2) False) True) % 6.02/6.20 (Or (Eq (considers_THFTYPE_IiooI a True) True) (Eq a_1 False)))) % 6.02/6.20 Clause #63 (by eliminate duplicate literals #[61]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.21 Or (Eq (believes_THFTYPE_IiooI a True) False) % 6.02/6.21 (Or (Eq a_1 False) % 6.02/6.21 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a True a_2) False) True) (Eq (considers_THFTYPE_IiooI a True) True))) % 6.02/6.21 Clause #64 (by eliminate duplicate literals #[47]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.21 Or (Eq (believes_THFTYPE_IiooI a False) False) % 6.02/6.21 (Or (Eq a_1 True) % 6.02/6.21 (Or (Eq (considers_THFTYPE_IiooI a a_1) False) (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a False a_2) True) True))) % 6.02/6.21 Clause #66 (by identity boolHoist #[64]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.21 Or (Eq (believes_THFTYPE_IiooI a False) False) % 6.02/6.21 (Or (Eq a_1 True) % 6.02/6.21 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a False a_2) True) True) % 6.02/6.21 (Or (Eq (considers_THFTYPE_IiooI a False) False) (Eq a_1 True)))) % 6.02/6.21 Clause #67 (by eliminate duplicate literals #[66]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.21 Or (Eq (believes_THFTYPE_IiooI a False) False) % 6.02/6.21 (Or (Eq a_1 True) % 6.02/6.23 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a False a_2) True) True) % 6.02/6.23 (Eq (considers_THFTYPE_IiooI a False) False))) % 6.02/6.23 Clause #68 (by superposition #[67, 9]): ∀ (a : Prop) (a_1 a_2 : Iota), % 6.02/6.23 Or (Eq a True) % 6.02/6.23 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i False a_1) True) True) % 6.02/6.23 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) False) % 6.02/6.23 (Or (Eq False True) (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True)))) % 6.02/6.23 Clause #73 (by clausification #[68]): ∀ (a : Prop) (a_1 a_2 : Iota), % 6.02/6.23 Or (Eq a True) % 6.02/6.23 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i False a_1) True) True) % 6.02/6.23 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) False) % 6.02/6.23 (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True))) % 6.02/6.23 Clause #74 (by eliminate duplicate literals #[57]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.23 Or (Eq (believes_THFTYPE_IiooI a False) False) % 6.02/6.23 (Or (Eq a_1 True) % 6.02/6.23 (Or (Eq (considers_THFTYPE_IiooI a a_1) True) (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a False a_2) False) True))) % 6.02/6.23 Clause #76 (by identity boolHoist #[74]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.23 Or (Eq (believes_THFTYPE_IiooI a False) False) % 6.02/6.23 (Or (Eq a_1 True) % 6.02/6.23 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a False a_2) False) True) % 6.02/6.23 (Or (Eq (considers_THFTYPE_IiooI a False) True) (Eq a_1 True)))) % 6.02/6.23 Clause #77 (by eliminate duplicate literals #[76]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 6.02/6.23 Or (Eq (believes_THFTYPE_IiooI a False) False) % 6.02/6.23 (Or (Eq a_1 True) % 6.02/6.23 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 a False a_2) False) True) % 6.02/6.23 (Eq (considers_THFTYPE_IiooI a False) True))) % 6.02/6.23 Clause #78 (by superposition #[77, 9]): ∀ (a : Prop) (a_1 a_2 : Iota), % 6.02/6.23 Or (Eq a True) % 6.02/6.23 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i False a_1) False) True) % 6.02/6.23 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.23 (Or (Eq False True) (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True)))) % 6.02/6.23 Clause #81 (by clausification #[78]): ∀ (a : Prop) (a_1 a_2 : Iota), % 6.02/6.23 Or (Eq a True) % 6.02/6.23 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i False a_1) False) True) % 6.02/6.23 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.23 (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True))) % 6.02/6.23 Clause #96 (by superposition #[81, 43]): ∀ (a : Prop) (a_1 a_2 : Iota), % 6.02/6.23 Or (Eq a True) % 6.02/6.23 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.23 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_1) True) % 6.02/6.23 (Or (Eq True False) % 6.02/6.23 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.23 (Eq (wife_THFTYPE_IiioI a_2 lMax_THFTYPE_i) True))))) % 6.02/6.23 Clause #104 (by clausification #[96]): ∀ (a : Prop) (a_1 a_2 : Iota), % 6.02/6.23 Or (Eq a True) % 6.02/6.23 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.23 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_1) True) % 6.02/6.23 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.23 (Eq (wife_THFTYPE_IiioI a_2 lMax_THFTYPE_i) True)))) % 6.02/6.23 Clause #105 (by eliminate duplicate literals #[104]): ∀ (a : Prop) (a_1 a_2 : Iota), % 6.02/6.23 Or (Eq a True) % 6.02/6.23 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.23 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_1) True) (Eq (wife_THFTYPE_IiioI a_2 lMax_THFTYPE_i) True))) % 6.02/6.23 Clause #130 (by equality factoring #[105]): ∀ (a a_1 : Iota), % 6.02/6.23 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.23 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.23 (Or (Ne True True) (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) True))) % 6.02/6.23 Clause #131 (by clausification #[130]): ∀ (a a_1 : Iota), % 6.02/6.23 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.23 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.23 (Or (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) True) (Or (Eq True False) (Eq True False)))) % 6.02/6.23 Clause #133 (by clausification #[131]): ∀ (a a_1 : Iota), % 6.02/6.23 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.23 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.23 (Or (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) True) (Eq True False))) % 6.02/6.25 Clause #134 (by clausification #[133]): ∀ (a a_1 : Iota), % 6.02/6.25 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.25 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) True)) % 6.02/6.25 Clause #140 (by superposition #[134, 53]): ∀ (a a_1 : Iota), % 6.02/6.25 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.25 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.25 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_1) True) (Eq True False))) % 6.02/6.25 Clause #141 (by clausification #[140]): ∀ (a a_1 : Iota), % 6.02/6.25 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.25 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_1) True)) % 6.02/6.25 Clause #147 (by equality factoring #[141]): ∀ (a : Iota), % 6.02/6.25 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.25 (Or (Ne True True) (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True)) % 6.02/6.25 Clause #148 (by clausification #[147]): ∀ (a : Iota), % 6.02/6.25 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.25 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) (Or (Eq True False) (Eq True False))) % 6.02/6.25 Clause #150 (by clausification #[148]): ∀ (a : Iota), % 6.02/6.25 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.25 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) (Eq True False)) % 6.02/6.25 Clause #151 (by clausification #[150]): ∀ (a : Iota), % 6.02/6.25 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.25 Clause #154 (by superposition #[151, 73]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), % 6.02/6.25 Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.25 (Or (Eq a_1 True) % 6.02/6.25 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i False a_2) True) True) % 6.02/6.25 (Or (Eq True False) (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_3) True)))) % 6.02/6.25 Clause #156 (by superposition #[151, 49]): ∀ (a : Iota), % 6.02/6.25 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) % 6.02/6.25 (Or (Eq True False) (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) True)) % 6.02/6.25 Clause #157 (by clausification #[156]): ∀ (a : Iota), % 6.02/6.25 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) True) (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) True) % 6.02/6.25 Clause #245 (by clausification #[154]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), % 6.02/6.25 Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.25 (Or (Eq a_1 True) % 6.02/6.25 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i False a_2) True) True) % 6.02/6.25 (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_3) True))) % 6.02/6.25 Clause #261 (by superposition #[245, 41]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), % 6.02/6.25 Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.25 (Or (Eq a_1 True) % 6.02/6.25 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True) % 6.02/6.25 (Or (Eq True False) % 6.02/6.25 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) False) % 6.02/6.25 (Eq (wife_THFTYPE_IiioI a_3 lMax_THFTYPE_i) True))))) % 6.02/6.25 Clause #270 (by clausification #[261]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), % 6.02/6.25 Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.25 (Or (Eq a_1 True) % 6.02/6.25 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True) % 6.02/6.25 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i False) False) % 6.02/6.25 (Eq (wife_THFTYPE_IiioI a_3 lMax_THFTYPE_i) True)))) % 6.02/6.25 Clause #272 (by superposition #[270, 157]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 a_4 : Iota), % 6.02/6.25 Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.25 (Or (Eq a_1 True) % 6.02/6.25 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True) % 6.02/6.25 (Or (Eq (wife_THFTYPE_IiioI a_3 lMax_THFTYPE_i) True) % 6.02/6.25 (Or (Eq False True) (Eq (wife_THFTYPE_IiioI a_4 lMax_THFTYPE_i) True))))) % 6.02/6.25 Clause #273 (by clausification #[272]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 a_4 : Iota), % 6.02/6.25 Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.25 (Or (Eq a_1 True) % 6.02/6.25 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True) % 6.02/6.25 (Or (Eq (wife_THFTYPE_IiioI a_3 lMax_THFTYPE_i) True) (Eq (wife_THFTYPE_IiioI a_4 lMax_THFTYPE_i) True)))) % 6.02/6.25 Clause #300 (by equality factoring #[273]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), % 6.02/6.28 Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.28 (Or (Eq a_1 True) % 6.02/6.28 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True) % 6.02/6.28 (Or (Ne True True) (Eq (wife_THFTYPE_IiioI a_3 lMax_THFTYPE_i) True)))) % 6.02/6.28 Clause #301 (by clausification #[300]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), % 6.02/6.28 Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.28 (Or (Eq a_1 True) % 6.02/6.28 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True) % 6.02/6.28 (Or (Eq (wife_THFTYPE_IiioI a_3 lMax_THFTYPE_i) True) (Or (Eq True False) (Eq True False))))) % 6.02/6.28 Clause #303 (by clausification #[301]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), % 6.02/6.28 Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.28 (Or (Eq a_1 True) % 6.02/6.28 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True) % 6.02/6.28 (Or (Eq (wife_THFTYPE_IiioI a_3 lMax_THFTYPE_i) True) (Eq True False)))) % 6.02/6.28 Clause #304 (by clausification #[303]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), % 6.02/6.28 Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) % 6.02/6.28 (Or (Eq a_1 True) % 6.02/6.28 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True) (Eq (wife_THFTYPE_IiioI a_3 lMax_THFTYPE_i) True))) % 6.02/6.28 Clause #327 (by equality factoring #[304]): ∀ (a : Prop) (a_1 a_2 : Iota), % 6.02/6.28 Or (Eq a True) % 6.02/6.28 (Or (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) True) % 6.02/6.28 (Or (Ne True True) (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True))) % 6.02/6.28 Clause #330 (by clausification #[327]): ∀ (a : Prop) (a_1 a_2 : Iota), % 6.02/6.28 Or (Eq a True) % 6.02/6.28 (Or (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) True) % 6.02/6.28 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True) (Or (Eq True False) (Eq True False)))) % 6.02/6.28 Clause #332 (by clausification #[330]): ∀ (a : Prop) (a_1 a_2 : Iota), % 6.02/6.28 Or (Eq a True) % 6.02/6.28 (Or (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) True) % 6.02/6.28 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True) (Eq True False))) % 6.02/6.28 Clause #333 (by clausification #[332]): ∀ (a : Prop) (a_1 a_2 : Iota), % 6.02/6.28 Or (Eq a True) % 6.02/6.28 (Or (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) True) (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_2) True)) % 6.02/6.28 Clause #355 (by equality factoring #[333]): ∀ (a a_1 : Iota), % 6.02/6.28 Or (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) True) % 6.02/6.28 (Or (Ne True True) (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_1) True)) % 6.02/6.28 Clause #357 (by clausification #[355]): ∀ (a a_1 : Iota), % 6.02/6.28 Or (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) True) % 6.02/6.28 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_1) True) (Or (Eq True False) (Eq True False))) % 6.02/6.28 Clause #359 (by clausification #[357]): ∀ (a a_1 : Iota), % 6.02/6.28 Or (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) True) % 6.02/6.28 (Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_1) True) (Eq True False)) % 6.02/6.28 Clause #360 (by clausification #[359]): ∀ (a a_1 : Iota), % 6.02/6.28 Or (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) True) (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a_1) True) % 6.02/6.28 Clause #363 (by superposition #[360, 49]): ∀ (a a_1 : Iota), % 6.02/6.28 Or (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) True) % 6.02/6.28 (Or (Eq True False) (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) True)) % 6.02/6.28 Clause #364 (by clausification #[363]): ∀ (a a_1 : Iota), Or (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) True) (Eq (wife_THFTYPE_IiioI a_1 lMax_THFTYPE_i) True) % 6.02/6.28 Clause #365 (by equality factoring #[364]): ∀ (a : Iota), Or (Ne True True) (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) True) % 6.02/6.28 Clause #366 (by clausification #[365]): ∀ (a : Iota), Or (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) True) (Or (Eq True False) (Eq True False)) % 6.02/6.28 Clause #368 (by clausification #[366]): ∀ (a : Iota), Or (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) True) (Eq True False) % 6.02/6.28 Clause #369 (by clausification #[368]): ∀ (a : Iota), Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) True % 6.02/6.28 Clause #370 (by superposition #[369, 53]): ∀ (a : Iota), Or (Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True) (Eq True False) % 6.02/6.28 Clause #371 (by clausification #[370]): ∀ (a : Iota), Eq (husband_THFTYPE_IiioI lMax_THFTYPE_i a) True % 6.02/6.28 Clause #372 (by superposition #[371, 8]): Or (Eq (believes_THFTYPE_IiooI lMax_THFTYPE_i True) True) (Eq True False) % 6.02/6.28 Clause #375 (by clausification #[372]): Eq (believes_THFTYPE_IiooI lMax_THFTYPE_i True) True % 6.13/6.30 Clause #378 (by superposition #[375, 25]): ∀ (a : Prop) (a_1 : Iota), % 6.13/6.30 Or (Eq True False) % 6.13/6.30 (Or (Eq a False) % 6.13/6.30 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i True a_1) True) True) % 6.13/6.30 (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) False))) % 6.13/6.30 Clause #379 (by superposition #[375, 63]): ∀ (a : Prop) (a_1 : Iota), % 6.13/6.30 Or (Eq True False) % 6.13/6.30 (Or (Eq a False) % 6.13/6.30 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i True a_1) False) True) % 6.13/6.30 (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) True))) % 6.13/6.30 Clause #462 (by clausification #[379]): ∀ (a : Prop) (a_1 : Iota), % 6.13/6.30 Or (Eq a False) % 6.13/6.30 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i True a_1) False) True) % 6.13/6.30 (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) True)) % 6.13/6.30 Clause #464 (by falseElim #[462]): ∀ (a : Iota), % 6.13/6.30 Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i True a) False) True) % 6.13/6.30 (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) True) % 6.13/6.30 Clause #465 (by superposition #[464, 42]): ∀ (a : Iota), % 6.13/6.30 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) True) % 6.13/6.30 (Or (Eq True False) % 6.13/6.30 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) True) (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) False))) % 6.13/6.30 Clause #466 (by clausification #[465]): ∀ (a : Iota), % 6.13/6.30 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) True) % 6.13/6.30 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) True) (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) False)) % 6.13/6.30 Clause #467 (by eliminate duplicate literals #[466]): ∀ (a : Iota), % 6.13/6.30 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) True) (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) False) % 6.13/6.30 Clause #468 (by superposition #[467, 369]): Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) True) (Eq False True) % 6.13/6.30 Clause #470 (by clausification #[468]): Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) True % 6.13/6.30 Clause #472 (by clausification #[378]): ∀ (a : Prop) (a_1 : Iota), % 6.13/6.30 Or (Eq a False) % 6.13/6.30 (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i True a_1) True) True) % 6.13/6.30 (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) False)) % 6.13/6.30 Clause #473 (by forward demodulation #[472, 470]): ∀ (a : Prop) (a_1 : Iota), % 6.13/6.30 Or (Eq a False) (Or (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i True a_1) True) True) (Eq True False)) % 6.13/6.30 Clause #474 (by clausification #[473]): ∀ (a : Prop) (a_1 : Iota), Or (Eq a False) (Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i True a_1) True) True) % 6.13/6.30 Clause #476 (by falseElim #[474]): ∀ (a : Iota), Eq (holdsDuring_THFTYPE_IiooI (skS.0 0 lMax_THFTYPE_i True a) True) True % 6.13/6.30 Clause #477 (by superposition #[476, 40]): ∀ (a : Iota), % 6.13/6.30 Or (Eq True False) % 6.13/6.30 (Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) False) (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) False)) % 6.13/6.30 Clause #480 (by clausification #[477]): ∀ (a : Iota), % 6.13/6.30 Or (Eq (considers_THFTYPE_IiooI lMax_THFTYPE_i True) False) (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) False) % 6.13/6.30 Clause #481 (by superposition #[480, 470]): ∀ (a : Iota), Or (Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) False) (Eq False True) % 6.13/6.30 Clause #482 (by clausification #[481]): ∀ (a : Iota), Eq (wife_THFTYPE_IiioI a lMax_THFTYPE_i) False % 6.13/6.30 Clause #483 (by superposition #[482, 369]): Eq False True % 6.13/6.30 Clause #484 (by clausification #[483]): False % 6.13/6.30 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------