%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM213_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n027.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:10 PM UTC 2026 % Result : Theorem 82.74s 82.98s % Output : Proof 82.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : COM213_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : duper %s % 0.16/0.33 % Computer : n027.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Mon May 4 18:46:34 EDT 2026 % 0.16/0.34 % CPUTime : % 82.74/82.98 SZS status Theorem for theBenchmark.p % 82.74/82.98 SZS output start Proof for theBenchmark.p % 82.74/82.98 Clause #25 (by assumption #[]): Eq (∀ (VTerm0 : vTerm), Ne vZero (vPred VTerm0)) True % 82.74/82.98 Clause #28 (by assumption #[]): Eq (∀ (VTerm0 VTerm1 : vTerm), Ne (vSucc VTerm0) (vPred VTerm1)) True % 82.74/82.98 Clause #42 (by assumption #[]): Eq % 82.74/82.98 (∀ (VwildcardName0 : vTerm), % 82.74/82.98 And (Ne VwildcardName0 vZero) (∀ (Vnv0 : vTerm), Ne VwildcardName0 (vSucc Vnv0)) → Not (visNV VwildcardName0)) % 82.74/82.98 True % 82.74/82.98 Clause #105 (by assumption #[]): Eq (Not (visNV (vPred vt1) → vptchecksimple (vPred vt1) vNat)) True % 82.74/82.98 Clause #184 (by clausification #[42]): ∀ (a : vTerm), Eq (And (Ne a vZero) (∀ (Vnv0 : vTerm), Ne a (vSucc Vnv0)) → Not (visNV a)) True % 82.74/82.98 Clause #185 (by clausification #[184]): ∀ (a : vTerm), Or (Eq (And (Ne a vZero) (∀ (Vnv0 : vTerm), Ne a (vSucc Vnv0))) False) (Eq (Not (visNV a)) True) % 82.74/82.98 Clause #186 (by clausification #[185]): ∀ (a : vTerm), % 82.74/82.98 Or (Eq (Not (visNV a)) True) (Or (Eq (Ne a vZero) False) (Eq (∀ (Vnv0 : vTerm), Ne a (vSucc Vnv0)) False)) % 82.74/82.98 Clause #187 (by clausification #[186]): ∀ (a : vTerm), Or (Eq (Ne a vZero) False) (Or (Eq (∀ (Vnv0 : vTerm), Ne a (vSucc Vnv0)) False) (Eq (visNV a) False)) % 82.74/82.98 Clause #188 (by clausification #[187]): ∀ (a : vTerm), Or (Eq (∀ (Vnv0 : vTerm), Ne a (vSucc Vnv0)) False) (Or (Eq (visNV a) False) (Eq a vZero)) % 82.74/82.98 Clause #189 (by clausification #[188]): ∀ (a a_1 : vTerm), Or (Eq (visNV a) False) (Or (Eq a vZero) (Eq (Not (Ne a (vSucc (skS.0 8 a a_1)))) True)) % 82.74/82.98 Clause #190 (by clausification #[189]): ∀ (a a_1 : vTerm), Or (Eq (visNV a) False) (Or (Eq a vZero) (Eq (Ne a (vSucc (skS.0 8 a a_1))) False)) % 82.74/82.98 Clause #191 (by clausification #[190]): ∀ (a a_1 : vTerm), Or (Eq (visNV a) False) (Or (Eq a vZero) (Eq a (vSucc (skS.0 8 a a_1)))) % 82.74/82.98 Clause #225 (by clausification #[25]): ∀ (a : vTerm), Eq (Ne vZero (vPred a)) True % 82.74/82.98 Clause #226 (by clausification #[225]): ∀ (a : vTerm), Ne vZero (vPred a) % 82.74/82.98 Clause #286 (by clausification #[105]): Eq (visNV (vPred vt1) → vptchecksimple (vPred vt1) vNat) False % 82.74/82.98 Clause #287 (by clausification #[286]): Eq (visNV (vPred vt1)) True % 82.74/82.98 Clause #289 (by superposition #[287, 191]): ∀ (a : vTerm), Or (Eq True False) (Or (Eq (vPred vt1) vZero) (Eq (vPred vt1) (vSucc (skS.0 8 (vPred vt1) a)))) % 82.74/82.98 Clause #686 (by clausification #[28]): ∀ (a : vTerm), Eq (∀ (VTerm1 : vTerm), Ne (vSucc a) (vPred VTerm1)) True % 82.74/82.98 Clause #687 (by clausification #[686]): ∀ (a a_1 : vTerm), Eq (Ne (vSucc a) (vPred a_1)) True % 82.74/82.98 Clause #688 (by clausification #[687]): ∀ (a a_1 : vTerm), Ne (vSucc a) (vPred a_1) % 82.74/82.98 Clause #12464 (by clausification #[289]): ∀ (a : vTerm), Or (Eq (vPred vt1) vZero) (Eq (vPred vt1) (vSucc (skS.0 8 (vPred vt1) a))) % 82.74/82.98 Clause #12465 (by forward contextual literal cutting #[12464, 226]): ∀ (a : vTerm), Eq (vPred vt1) (vSucc (skS.0 8 (vPred vt1) a)) % 82.74/82.98 Clause #12466 (by forward contextual literal cutting #[12465, 688]): False % 82.74/82.98 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------