%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : HWV095+1 : TPTP v9.2.0. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n028.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:50:31 PM UTC 2025 % Result : Theorem 140.82s 141.01s % Output : Proof 140.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : HWV095+1 : TPTP v9.2.0. Released v6.1.0. % 0.08/0.14 % Command : duper %s % 0.13/0.35 % Computer : n028.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 09:12:53 EDT 2025 % 0.13/0.35 % CPUTime : % 140.82/141.01 SZS status Theorem for theBenchmark.p % 140.82/141.01 SZS output start Proof for theBenchmark.p % 140.82/141.01 Clause #34 (by assumption #[]): Eq (Not (∀ (VarCurr : Iota), reachableState VarCurr → v4 VarCurr)) True % 140.82/141.01 Clause #35 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (Not (v4 VarCurr)) (v995 VarCurr)) True % 140.82/141.01 Clause #36 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (Not (v995 VarCurr)) (v996 VarCurr)) True % 140.82/141.01 Clause #37 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v996 VarCurr) (And (v998 VarCurr) (v1010 VarCurr))) True % 140.82/141.01 Clause #38 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v1010 VarCurr) (Or (v1000 VarCurr bitIndex0) (v1000 VarCurr bitIndex1))) True % 140.82/141.01 Clause #39 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (Not (v998 VarCurr)) (v999 VarCurr)) True % 140.82/141.01 Clause #40 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v999 VarCurr) (And (v1000 VarCurr bitIndex0) (v1000 VarCurr bitIndex1))) True % 140.82/141.01 Clause #41 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v1000 VarCurr bitIndex0) (v1001 VarCurr)) True % 140.82/141.01 Clause #42 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v1000 VarCurr bitIndex1) True) True % 140.82/141.01 Clause #43 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v1001 VarCurr) (And (v1003 VarCurr) (v1007 VarCurr bitIndex5))) True % 140.82/141.01 Clause #44 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v1003 VarCurr) (And (v1004 VarCurr) (v1007 VarCurr bitIndex4))) True % 140.82/141.01 Clause #50 (by assumption #[]): Eq (∀ (VarCurr : Iota), Not (v1007 VarCurr bitIndex4)) True % 140.82/141.01 Clause #1272 (by clausification #[34]): Eq (∀ (VarCurr : Iota), reachableState VarCurr → v4 VarCurr) False % 140.82/141.01 Clause #1273 (by clausification #[1272]): ∀ (a : Iota), Eq (Not (reachableState (skS.0 0 a) → v4 (skS.0 0 a))) True % 140.82/141.01 Clause #1274 (by clausification #[1273]): ∀ (a : Iota), Eq (reachableState (skS.0 0 a) → v4 (skS.0 0 a)) False % 140.82/141.01 Clause #1276 (by clausification #[1274]): ∀ (a : Iota), Eq (v4 (skS.0 0 a)) False % 140.82/141.01 Clause #1283 (by clausification #[35]): ∀ (a : Iota), Eq (Iff (Not (v4 a)) (v995 a)) True % 140.82/141.01 Clause #1285 (by clausification #[1283]): ∀ (a : Iota), Or (Eq (Not (v4 a)) False) (Eq (v995 a) True) % 140.82/141.01 Clause #1292 (by clausification #[36]): ∀ (a : Iota), Eq (Iff (Not (v995 a)) (v996 a)) True % 140.82/141.01 Clause #1293 (by clausification #[1292]): ∀ (a : Iota), Or (Eq (Not (v995 a)) True) (Eq (v996 a) False) % 140.82/141.01 Clause #1295 (by clausification #[1293]): ∀ (a : Iota), Or (Eq (v996 a) False) (Eq (v995 a) False) % 140.82/141.01 Clause #1301 (by clausification #[37]): ∀ (a : Iota), Eq (Iff (v996 a) (And (v998 a) (v1010 a))) True % 140.82/141.01 Clause #1302 (by clausification #[1301]): ∀ (a : Iota), Or (Eq (v996 a) True) (Eq (And (v998 a) (v1010 a)) False) % 140.82/141.01 Clause #1304 (by clausification #[1302]): ∀ (a : Iota), Or (Eq (v996 a) True) (Or (Eq (v998 a) False) (Eq (v1010 a) False)) % 140.82/141.01 Clause #1310 (by clausification #[38]): ∀ (a : Iota), Eq (Iff (v1010 a) (Or (v1000 a bitIndex0) (v1000 a bitIndex1))) True % 140.82/141.01 Clause #1311 (by clausification #[1310]): ∀ (a : Iota), Or (Eq (v1010 a) True) (Eq (Or (v1000 a bitIndex0) (v1000 a bitIndex1)) False) % 140.82/141.01 Clause #1313 (by clausification #[1311]): ∀ (a : Iota), Or (Eq (v1010 a) True) (Eq (v1000 a bitIndex1) False) % 140.82/141.01 Clause #1320 (by clausification #[39]): ∀ (a : Iota), Eq (Iff (Not (v998 a)) (v999 a)) True % 140.82/141.01 Clause #1322 (by clausification #[1320]): ∀ (a : Iota), Or (Eq (Not (v998 a)) False) (Eq (v999 a) True) % 140.82/141.01 Clause #1329 (by clausification #[40]): ∀ (a : Iota), Eq (Iff (v999 a) (And (v1000 a bitIndex0) (v1000 a bitIndex1))) True % 140.82/141.01 Clause #1331 (by clausification #[1329]): ∀ (a : Iota), Or (Eq (v999 a) False) (Eq (And (v1000 a bitIndex0) (v1000 a bitIndex1)) True) % 140.82/141.01 Clause #1338 (by clausification #[41]): ∀ (a : Iota), Eq (Iff (v1000 a bitIndex0) (v1001 a)) True % 140.82/141.01 Clause #1340 (by clausification #[1338]): ∀ (a : Iota), Or (Eq (v1000 a bitIndex0) False) (Eq (v1001 a) True) % 140.82/141.01 Clause #1346 (by clausification #[42]): ∀ (a : Iota), Eq (Iff (v1000 a bitIndex1) True) True % 140.82/141.01 Clause #1347 (by clausification #[1346]): ∀ (a : Iota), Or (Eq (v1000 a bitIndex1) True) (Eq True False) % 140.82/141.01 Clause #1349 (by clausification #[1347]): ∀ (a : Iota), Eq (v1000 a bitIndex1) True % 140.82/141.01 Clause #1351 (by superposition #[1349, 1313]): ∀ (a : Iota), Or (Eq (v1010 a) True) (Eq True False) % 140.91/141.12 Clause #1357 (by clausification #[43]): ∀ (a : Iota), Eq (Iff (v1001 a) (And (v1003 a) (v1007 a bitIndex5))) True % 140.91/141.12 Clause #1359 (by clausification #[1357]): ∀ (a : Iota), Or (Eq (v1001 a) False) (Eq (And (v1003 a) (v1007 a bitIndex5)) True) % 140.91/141.12 Clause #1366 (by clausification #[44]): ∀ (a : Iota), Eq (Iff (v1003 a) (And (v1004 a) (v1007 a bitIndex4))) True % 140.91/141.12 Clause #1368 (by clausification #[1366]): ∀ (a : Iota), Or (Eq (v1003 a) False) (Eq (And (v1004 a) (v1007 a bitIndex4)) True) % 140.91/141.12 Clause #1421 (by clausification #[50]): ∀ (a : Iota), Eq (Not (v1007 a bitIndex4)) True % 140.91/141.12 Clause #1422 (by clausification #[1421]): ∀ (a : Iota), Eq (v1007 a bitIndex4) False % 140.91/141.12 Clause #1643 (by clausification #[1351]): ∀ (a : Iota), Eq (v1010 a) True % 140.91/141.12 Clause #1644 (by backward demodulation #[1643, 1304]): ∀ (a : Iota), Or (Eq (v996 a) True) (Or (Eq (v998 a) False) (Eq True False)) % 140.91/141.12 Clause #1801 (by clausification #[1285]): ∀ (a : Iota), Or (Eq (v995 a) True) (Eq (v4 a) True) % 140.91/141.12 Clause #2100 (by clausification #[1322]): ∀ (a : Iota), Or (Eq (v999 a) True) (Eq (v998 a) True) % 140.91/141.12 Clause #3152 (by superposition #[1276, 1801]): ∀ (a : Iota), Or (Eq (v995 (skS.0 0 a)) True) (Eq True False) % 140.91/141.12 Clause #6062 (by clausification #[1644]): ∀ (a : Iota), Or (Eq (v996 a) True) (Eq (v998 a) False) % 140.91/141.12 Clause #6063 (by superposition #[6062, 2100]): ∀ (a : Iota), Or (Eq (v996 a) True) (Or (Eq (v999 a) True) (Eq False True)) % 140.91/141.12 Clause #6064 (by clausification #[6063]): ∀ (a : Iota), Or (Eq (v996 a) True) (Eq (v999 a) True) % 140.91/141.12 Clause #6065 (by superposition #[6064, 1295]): ∀ (a : Iota), Or (Eq (v999 a) True) (Or (Eq True False) (Eq (v995 a) False)) % 140.91/141.12 Clause #6066 (by clausification #[6065]): ∀ (a : Iota), Or (Eq (v999 a) True) (Eq (v995 a) False) % 140.91/141.12 Clause #9379 (by clausification #[3152]): ∀ (a : Iota), Eq (v995 (skS.0 0 a)) True % 140.91/141.12 Clause #9381 (by superposition #[9379, 6066]): ∀ (a : Iota), Or (Eq (v999 (skS.0 0 a)) True) (Eq True False) % 140.91/141.12 Clause #9382 (by clausification #[9381]): ∀ (a : Iota), Eq (v999 (skS.0 0 a)) True % 140.91/141.12 Clause #9703 (by clausification #[1368]): ∀ (a : Iota), Or (Eq (v1003 a) False) (Eq (v1007 a bitIndex4) True) % 140.91/141.12 Clause #9706 (by clausification #[1359]): ∀ (a : Iota), Or (Eq (v1001 a) False) (Eq (v1003 a) True) % 140.91/141.12 Clause #9944 (by clausification #[1331]): ∀ (a : Iota), Or (Eq (v999 a) False) (Eq (v1000 a bitIndex0) True) % 140.91/141.12 Clause #10011 (by superposition #[9944, 9382]): ∀ (a : Iota), Or (Eq (v1000 (skS.0 0 a) bitIndex0) True) (Eq False True) % 140.91/141.12 Clause #14286 (by clausification #[10011]): ∀ (a : Iota), Eq (v1000 (skS.0 0 a) bitIndex0) True % 140.91/141.12 Clause #14287 (by superposition #[14286, 1340]): ∀ (a : Iota), Or (Eq True False) (Eq (v1001 (skS.0 0 a)) True) % 140.91/141.12 Clause #14330 (by clausification #[14287]): ∀ (a : Iota), Eq (v1001 (skS.0 0 a)) True % 140.91/141.12 Clause #14333 (by superposition #[14330, 9706]): ∀ (a : Iota), Or (Eq True False) (Eq (v1003 (skS.0 0 a)) True) % 140.91/141.12 Clause #14336 (by clausification #[14333]): ∀ (a : Iota), Eq (v1003 (skS.0 0 a)) True % 140.91/141.12 Clause #14337 (by superposition #[14336, 9703]): ∀ (a : Iota), Or (Eq True False) (Eq (v1007 (skS.0 0 a) bitIndex4) True) % 140.91/141.12 Clause #14371 (by clausification #[14337]): ∀ (a : Iota), Eq (v1007 (skS.0 0 a) bitIndex4) True % 140.91/141.12 Clause #14372 (by superposition #[14371, 1422]): Eq True False % 140.91/141.12 Clause #14374 (by clausification #[14372]): False % 140.91/141.12 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------