%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : HWV093+1 : TPTP v9.2.0. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.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:30 PM UTC 2025 % Result : Theorem 89.82s 90.05s % Output : Proof 89.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : HWV093+1 : TPTP v9.2.0. Released v6.1.0. % 0.07/0.13 % Command : duper %s % 0.14/0.34 % Computer : n014.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu Oct 2 09:15:53 EDT 2025 % 0.14/0.34 % CPUTime : % 89.82/90.05 SZS status Theorem for theBenchmark.p % 89.82/90.05 SZS output start Proof for theBenchmark.p % 89.82/90.05 Clause #34 (by assumption #[]): Eq (Not (∀ (VarCurr : Iota), reachableState VarCurr → v4 VarCurr)) True % 89.82/90.05 Clause #35 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (Not (v4 VarCurr)) (v995 VarCurr)) True % 89.82/90.05 Clause #36 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (Not (v995 VarCurr)) (v996 VarCurr)) True % 89.82/90.05 Clause #37 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v996 VarCurr) (And (v998 VarCurr) (v1010 VarCurr))) True % 89.82/90.05 Clause #38 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v1010 VarCurr) (Or (v1000 VarCurr bitIndex0) (v1000 VarCurr bitIndex1))) True % 89.82/90.05 Clause #39 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (Not (v998 VarCurr)) (v999 VarCurr)) True % 89.82/90.05 Clause #40 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v999 VarCurr) (And (v1000 VarCurr bitIndex0) (v1000 VarCurr bitIndex1))) True % 89.82/90.05 Clause #41 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v1000 VarCurr bitIndex0) (v1001 VarCurr)) True % 89.82/90.05 Clause #42 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v1000 VarCurr bitIndex1) True) True % 89.82/90.05 Clause #43 (by assumption #[]): Eq (∀ (VarCurr : Iota), Iff (v1001 VarCurr) (And (v1003 VarCurr) (v1007 VarCurr bitIndex5))) True % 89.82/90.05 Clause #51 (by assumption #[]): Eq (∀ (VarCurr : Iota), Not (v1007 VarCurr bitIndex5)) True % 89.82/90.05 Clause #1278 (by clausification #[34]): Eq (∀ (VarCurr : Iota), reachableState VarCurr → v4 VarCurr) False % 89.82/90.05 Clause #1279 (by clausification #[1278]): ∀ (a : Iota), Eq (Not (reachableState (skS.0 0 a) → v4 (skS.0 0 a))) True % 89.82/90.05 Clause #1280 (by clausification #[1279]): ∀ (a : Iota), Eq (reachableState (skS.0 0 a) → v4 (skS.0 0 a)) False % 89.82/90.05 Clause #1282 (by clausification #[1280]): ∀ (a : Iota), Eq (v4 (skS.0 0 a)) False % 89.82/90.05 Clause #1289 (by clausification #[35]): ∀ (a : Iota), Eq (Iff (Not (v4 a)) (v995 a)) True % 89.82/90.05 Clause #1291 (by clausification #[1289]): ∀ (a : Iota), Or (Eq (Not (v4 a)) False) (Eq (v995 a) True) % 89.82/90.05 Clause #1298 (by clausification #[36]): ∀ (a : Iota), Eq (Iff (Not (v995 a)) (v996 a)) True % 89.82/90.05 Clause #1299 (by clausification #[1298]): ∀ (a : Iota), Or (Eq (Not (v995 a)) True) (Eq (v996 a) False) % 89.82/90.05 Clause #1301 (by clausification #[1299]): ∀ (a : Iota), Or (Eq (v996 a) False) (Eq (v995 a) False) % 89.82/90.05 Clause #1307 (by clausification #[37]): ∀ (a : Iota), Eq (Iff (v996 a) (And (v998 a) (v1010 a))) True % 89.82/90.05 Clause #1308 (by clausification #[1307]): ∀ (a : Iota), Or (Eq (v996 a) True) (Eq (And (v998 a) (v1010 a)) False) % 89.82/90.05 Clause #1310 (by clausification #[1308]): ∀ (a : Iota), Or (Eq (v996 a) True) (Or (Eq (v998 a) False) (Eq (v1010 a) False)) % 89.82/90.05 Clause #1316 (by clausification #[38]): ∀ (a : Iota), Eq (Iff (v1010 a) (Or (v1000 a bitIndex0) (v1000 a bitIndex1))) True % 89.82/90.05 Clause #1317 (by clausification #[1316]): ∀ (a : Iota), Or (Eq (v1010 a) True) (Eq (Or (v1000 a bitIndex0) (v1000 a bitIndex1)) False) % 89.82/90.05 Clause #1319 (by clausification #[1317]): ∀ (a : Iota), Or (Eq (v1010 a) True) (Eq (v1000 a bitIndex1) False) % 89.82/90.05 Clause #1326 (by clausification #[39]): ∀ (a : Iota), Eq (Iff (Not (v998 a)) (v999 a)) True % 89.82/90.05 Clause #1328 (by clausification #[1326]): ∀ (a : Iota), Or (Eq (Not (v998 a)) False) (Eq (v999 a) True) % 89.82/90.05 Clause #1335 (by clausification #[40]): ∀ (a : Iota), Eq (Iff (v999 a) (And (v1000 a bitIndex0) (v1000 a bitIndex1))) True % 89.82/90.05 Clause #1337 (by clausification #[1335]): ∀ (a : Iota), Or (Eq (v999 a) False) (Eq (And (v1000 a bitIndex0) (v1000 a bitIndex1)) True) % 89.82/90.05 Clause #1344 (by clausification #[41]): ∀ (a : Iota), Eq (Iff (v1000 a bitIndex0) (v1001 a)) True % 89.82/90.05 Clause #1346 (by clausification #[1344]): ∀ (a : Iota), Or (Eq (v1000 a bitIndex0) False) (Eq (v1001 a) True) % 89.82/90.05 Clause #1352 (by clausification #[42]): ∀ (a : Iota), Eq (Iff (v1000 a bitIndex1) True) True % 89.82/90.05 Clause #1353 (by clausification #[1352]): ∀ (a : Iota), Or (Eq (v1000 a bitIndex1) True) (Eq True False) % 89.82/90.05 Clause #1355 (by clausification #[1353]): ∀ (a : Iota), Eq (v1000 a bitIndex1) True % 89.82/90.05 Clause #1357 (by superposition #[1355, 1319]): ∀ (a : Iota), Or (Eq (v1010 a) True) (Eq True False) % 89.82/90.05 Clause #1363 (by clausification #[43]): ∀ (a : Iota), Eq (Iff (v1001 a) (And (v1003 a) (v1007 a bitIndex5))) True % 89.97/90.13 Clause #1365 (by clausification #[1363]): ∀ (a : Iota), Or (Eq (v1001 a) False) (Eq (And (v1003 a) (v1007 a bitIndex5)) True) % 89.97/90.13 Clause #1434 (by clausification #[51]): ∀ (a : Iota), Eq (Not (v1007 a bitIndex5)) True % 89.97/90.13 Clause #1435 (by clausification #[1434]): ∀ (a : Iota), Eq (v1007 a bitIndex5) False % 89.97/90.13 Clause #1631 (by clausification #[1357]): ∀ (a : Iota), Eq (v1010 a) True % 89.97/90.13 Clause #1632 (by backward demodulation #[1631, 1310]): ∀ (a : Iota), Or (Eq (v996 a) True) (Or (Eq (v998 a) False) (Eq True False)) % 89.97/90.13 Clause #1755 (by clausification #[1328]): ∀ (a : Iota), Or (Eq (v999 a) True) (Eq (v998 a) True) % 89.97/90.13 Clause #1912 (by clausification #[1291]): ∀ (a : Iota), Or (Eq (v995 a) True) (Eq (v4 a) True) % 89.97/90.13 Clause #3600 (by superposition #[1282, 1912]): ∀ (a : Iota), Or (Eq (v995 (skS.0 0 a)) True) (Eq True False) % 89.97/90.13 Clause #4672 (by clausification #[1632]): ∀ (a : Iota), Or (Eq (v996 a) True) (Eq (v998 a) False) % 89.97/90.13 Clause #4673 (by superposition #[4672, 1755]): ∀ (a : Iota), Or (Eq (v996 a) True) (Or (Eq (v999 a) True) (Eq False True)) % 89.97/90.13 Clause #4674 (by clausification #[4673]): ∀ (a : Iota), Or (Eq (v996 a) True) (Eq (v999 a) True) % 89.97/90.13 Clause #4675 (by superposition #[4674, 1301]): ∀ (a : Iota), Or (Eq (v999 a) True) (Or (Eq True False) (Eq (v995 a) False)) % 89.97/90.13 Clause #4682 (by clausification #[4675]): ∀ (a : Iota), Or (Eq (v999 a) True) (Eq (v995 a) False) % 89.97/90.13 Clause #8632 (by clausification #[1365]): ∀ (a : Iota), Or (Eq (v1001 a) False) (Eq (v1007 a bitIndex5) True) % 89.97/90.13 Clause #8956 (by clausification #[3600]): ∀ (a : Iota), Eq (v995 (skS.0 0 a)) True % 89.97/90.13 Clause #8958 (by superposition #[8956, 4682]): ∀ (a : Iota), Or (Eq (v999 (skS.0 0 a)) True) (Eq True False) % 89.97/90.13 Clause #8959 (by clausification #[8958]): ∀ (a : Iota), Eq (v999 (skS.0 0 a)) True % 89.97/90.13 Clause #9912 (by clausification #[1337]): ∀ (a : Iota), Or (Eq (v999 a) False) (Eq (v1000 a bitIndex0) True) % 89.97/90.13 Clause #9994 (by superposition #[9912, 8959]): ∀ (a : Iota), Or (Eq (v1000 (skS.0 0 a) bitIndex0) True) (Eq False True) % 89.97/90.13 Clause #11053 (by clausification #[9994]): ∀ (a : Iota), Eq (v1000 (skS.0 0 a) bitIndex0) True % 89.97/90.13 Clause #11054 (by superposition #[11053, 1346]): ∀ (a : Iota), Or (Eq True False) (Eq (v1001 (skS.0 0 a)) True) % 89.97/90.13 Clause #11058 (by clausification #[11054]): ∀ (a : Iota), Eq (v1001 (skS.0 0 a)) True % 89.97/90.13 Clause #11060 (by superposition #[11058, 8632]): ∀ (a : Iota), Or (Eq True False) (Eq (v1007 (skS.0 0 a) bitIndex5) True) % 89.97/90.13 Clause #11083 (by clausification #[11060]): ∀ (a : Iota), Eq (v1007 (skS.0 0 a) bitIndex5) True % 89.97/90.13 Clause #11084 (by superposition #[11083, 1435]): Eq True False % 89.97/90.13 Clause #11086 (by clausification #[11084]): False % 89.97/90.13 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------