%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM212_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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 64.73s 64.94s % Output : Proof 64.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : COM212_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : duper %s % 0.14/0.34 % Computer : n021.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 : Mon May 4 18:45:40 EDT 2026 % 0.14/0.34 % CPUTime : % 64.73/64.94 SZS status Theorem for theBenchmark.p % 64.73/64.94 SZS output start Proof for theBenchmark.p % 64.73/64.94 Clause #14 (by assumption #[]): Eq (Ne vFalse vZero) True % 64.73/64.94 Clause #15 (by assumption #[]): Eq (∀ (VTerm0 : vTerm), Ne vFalse (vSucc VTerm0)) True % 64.73/64.94 Clause #42 (by assumption #[]): Eq % 64.73/64.94 (∀ (VwildcardName0 : vTerm), % 64.73/64.94 And (Ne VwildcardName0 vZero) (∀ (Vnv0 : vTerm), Ne VwildcardName0 (vSucc Vnv0)) → Not (visNV VwildcardName0)) % 64.73/64.94 True % 64.73/64.94 Clause #104 (by assumption #[]): Eq (Not (visNV vFalse → vptchecksimple vFalse vNat)) True % 64.73/64.94 Clause #162 (by clausification #[14]): Ne vFalse vZero % 64.73/64.94 Clause #198 (by clausification #[104]): Eq (visNV vFalse → vptchecksimple vFalse vNat) False % 64.73/64.94 Clause #199 (by clausification #[198]): Eq (visNV vFalse) True % 64.73/64.94 Clause #203 (by clausification #[42]): ∀ (a : vTerm), Eq (And (Ne a vZero) (∀ (Vnv0 : vTerm), Ne a (vSucc Vnv0)) → Not (visNV a)) True % 64.73/64.94 Clause #204 (by clausification #[203]): ∀ (a : vTerm), Or (Eq (And (Ne a vZero) (∀ (Vnv0 : vTerm), Ne a (vSucc Vnv0))) False) (Eq (Not (visNV a)) True) % 64.73/64.94 Clause #205 (by clausification #[204]): ∀ (a : vTerm), % 64.73/64.94 Or (Eq (Not (visNV a)) True) (Or (Eq (Ne a vZero) False) (Eq (∀ (Vnv0 : vTerm), Ne a (vSucc Vnv0)) False)) % 64.73/64.94 Clause #206 (by clausification #[205]): ∀ (a : vTerm), Or (Eq (Ne a vZero) False) (Or (Eq (∀ (Vnv0 : vTerm), Ne a (vSucc Vnv0)) False) (Eq (visNV a) False)) % 64.73/64.94 Clause #207 (by clausification #[206]): ∀ (a : vTerm), Or (Eq (∀ (Vnv0 : vTerm), Ne a (vSucc Vnv0)) False) (Or (Eq (visNV a) False) (Eq a vZero)) % 64.73/64.94 Clause #208 (by clausification #[207]): ∀ (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)) % 64.73/64.94 Clause #209 (by clausification #[208]): ∀ (a a_1 : vTerm), Or (Eq (visNV a) False) (Or (Eq a vZero) (Eq (Ne a (vSucc (skS.0 8 a a_1))) False)) % 64.73/64.94 Clause #210 (by clausification #[209]): ∀ (a a_1 : vTerm), Or (Eq (visNV a) False) (Or (Eq a vZero) (Eq a (vSucc (skS.0 8 a a_1)))) % 64.73/64.94 Clause #212 (by superposition #[210, 199]): ∀ (a : vTerm), Or (Eq vFalse vZero) (Or (Eq vFalse (vSucc (skS.0 8 vFalse a))) (Eq False True)) % 64.73/64.94 Clause #278 (by clausification #[15]): ∀ (a : vTerm), Eq (Ne vFalse (vSucc a)) True % 64.73/64.94 Clause #279 (by clausification #[278]): ∀ (a : vTerm), Ne vFalse (vSucc a) % 64.73/64.94 Clause #10416 (by clausification #[212]): ∀ (a : vTerm), Or (Eq vFalse vZero) (Eq vFalse (vSucc (skS.0 8 vFalse a))) % 64.73/64.94 Clause #10417 (by forward contextual literal cutting #[10416, 162]): ∀ (a : vTerm), Eq vFalse (vSucc (skS.0 8 vFalse a)) % 64.73/64.94 Clause #10418 (by forward contextual literal cutting #[10417, 279]): False % 64.73/64.94 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------