%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM244_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.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 : Tue May 5 06:18:12 PM UTC 2026 % Result : Theorem 6.74s 7.00s % Output : Proof 6.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : COM244_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.14 % Command : duper %s % 0.17/0.36 % Computer : n008.cluster.edu % 0.17/0.36 % Model : x86_64 x86_64 % 0.17/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.36 % Memory : 8042.1875MB % 0.17/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.36 % CPULimit : 300 % 0.17/0.36 % WCLimit : 300 % 0.17/0.36 % DateTime : Mon May 4 19:33:28 EDT 2026 % 0.17/0.36 % CPUTime : % 6.74/7.00 SZS status Theorem for theBenchmark.p % 6.74/7.00 SZS output start Proof for theBenchmark.p % 6.74/7.00 Clause #8 (by assumption #[]): Eq (Ne vTrue vZero) True % 6.74/7.00 Clause #14 (by assumption #[]): Eq (Ne vFalse vZero) True % 6.74/7.00 Clause #40 (by assumption #[]): Eq (visNV vZero) True % 6.74/7.00 Clause #47 (by assumption #[]): Eq (∀ (Vt1 : vTerm), And (Ne Vt1 vTrue) (Ne Vt1 vFalse) → Iff (visValue Vt1) (visNV Vt1)) True % 6.74/7.00 Clause #104 (by assumption #[]): Eq (Not (∀ (VT : vTy), And (vptchecksimple vZero VT) (Not (visValue vZero)) → Ne (vreduce vZero) vnoTerm)) True % 6.74/7.00 Clause #162 (by clausification #[14]): Ne vFalse vZero % 6.74/7.00 Clause #180 (by clausification #[8]): Ne vTrue vZero % 6.74/7.00 Clause #589 (by clausification #[47]): ∀ (a : vTerm), Eq (And (Ne a vTrue) (Ne a vFalse) → Iff (visValue a) (visNV a)) True % 6.74/7.00 Clause #590 (by clausification #[589]): ∀ (a : vTerm), Or (Eq (And (Ne a vTrue) (Ne a vFalse)) False) (Eq (Iff (visValue a) (visNV a)) True) % 6.74/7.00 Clause #591 (by clausification #[590]): ∀ (a : vTerm), Or (Eq (Iff (visValue a) (visNV a)) True) (Or (Eq (Ne a vTrue) False) (Eq (Ne a vFalse) False)) % 6.74/7.00 Clause #592 (by clausification #[591]): ∀ (a : vTerm), Or (Eq (Ne a vTrue) False) (Or (Eq (Ne a vFalse) False) (Or (Eq (visValue a) True) (Eq (visNV a) False))) % 6.74/7.00 Clause #594 (by clausification #[592]): ∀ (a : vTerm), Or (Eq (Ne a vFalse) False) (Or (Eq (visValue a) True) (Or (Eq (visNV a) False) (Eq a vTrue))) % 6.74/7.00 Clause #595 (by clausification #[594]): ∀ (a : vTerm), Or (Eq (visValue a) True) (Or (Eq (visNV a) False) (Or (Eq a vTrue) (Eq a vFalse))) % 6.74/7.00 Clause #596 (by superposition #[595, 40]): Or (Eq (visValue vZero) True) (Or (Eq vZero vTrue) (Or (Eq vZero vFalse) (Eq False True))) % 6.74/7.00 Clause #621 (by clausification #[104]): Eq (∀ (VT : vTy), And (vptchecksimple vZero VT) (Not (visValue vZero)) → Ne (vreduce vZero) vnoTerm) False % 6.74/7.00 Clause #622 (by clausification #[621]): ∀ (a : vTy), Eq (Not (And (vptchecksimple vZero (skS.0 23 a)) (Not (visValue vZero)) → Ne (vreduce vZero) vnoTerm)) True % 6.74/7.00 Clause #623 (by clausification #[622]): ∀ (a : vTy), Eq (And (vptchecksimple vZero (skS.0 23 a)) (Not (visValue vZero)) → Ne (vreduce vZero) vnoTerm) False % 6.74/7.00 Clause #624 (by clausification #[623]): ∀ (a : vTy), Eq (And (vptchecksimple vZero (skS.0 23 a)) (Not (visValue vZero))) True % 6.74/7.00 Clause #626 (by clausification #[624]): Eq (Not (visValue vZero)) True % 6.74/7.00 Clause #628 (by clausification #[626]): Eq (visValue vZero) False % 6.74/7.00 Clause #783 (by clausification #[596]): Or (Eq (visValue vZero) True) (Or (Eq vZero vTrue) (Eq vZero vFalse)) % 6.74/7.00 Clause #784 (by forward contextual literal cutting #[783, 180]): Or (Eq (visValue vZero) True) (Eq vZero vFalse) % 6.74/7.00 Clause #785 (by forward contextual literal cutting #[784, 162]): Eq (visValue vZero) True % 6.74/7.00 Clause #786 (by superposition #[785, 628]): Eq True False % 6.74/7.00 Clause #789 (by clausification #[786]): False % 6.74/7.00 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------