%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM256_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:13 PM UTC 2026 % Result : Theorem 190.21s 190.47s % Output : Proof 190.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM256_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : duper %s % 0.17/0.35 % Computer : n021.cluster.edu % 0.17/0.35 % Model : x86_64 x86_64 % 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.35 % Memory : 8042.1875MB % 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Mon May 4 19:50:10 EDT 2026 % 0.17/0.35 % CPUTime : % 190.21/190.47 SZS status Theorem for theBenchmark.p % 190.21/190.47 SZS output start Proof for theBenchmark.p % 190.21/190.47 Clause #57 (by assumption #[]): Eq (∀ (VQConf0 : vQConf), Ne vnoQConf (vsomeQConf VQConf0)) True % 190.21/190.47 Clause #262 (by assumption #[]): Eq (∀ (VwildcardName0 : vAnsMap) (VwildcardName1 : vQMap), Eq (vreduce vqempty VwildcardName0 VwildcardName1) vnoQConf) % 190.21/190.47 True % 190.21/190.47 Clause #359 (by assumption #[]): Eq % 190.21/190.47 (Not % 190.21/190.47 (∀ (Vqtm1 : vATMap) (Vqr : vQuestionnaire) (Vqm : vQMap) (Vamr : vAnsMap) (Vatm1 : vATMap) (Vam : vAnsMap) % 190.21/190.47 (Vqmr : vQMap), % 190.21/190.47 And (vptcheck (vMC (vtypeAM Vam) (vtypeQM Vqm)) vqempty (vMC Vatm1 Vqtm1)) % 190.21/190.47 (Eq (vreduce vqempty Vam Vqm) (vsomeQConf (vQC Vamr Vqmr Vqr))) → % 190.21/190.47 vptcheck (vMC (vtypeAM Vamr) (vtypeQM Vqmr)) Vqr (vMC Vatm1 Vqtm1))) % 190.21/190.47 True % 190.21/190.47 Clause #943 (by clausification #[57]): ∀ (a : vQConf), Eq (Ne vnoQConf (vsomeQConf a)) True % 190.21/190.47 Clause #944 (by clausification #[943]): ∀ (a : vQConf), Ne vnoQConf (vsomeQConf a) % 190.21/190.47 Clause #9846 (by clausification #[262]): ∀ (a : vAnsMap), Eq (∀ (VwildcardName1 : vQMap), Eq (vreduce vqempty a VwildcardName1) vnoQConf) True % 190.21/190.47 Clause #9847 (by clausification #[9846]): ∀ (a : vAnsMap) (a_1 : vQMap), Eq (Eq (vreduce vqempty a a_1) vnoQConf) True % 190.21/190.47 Clause #9848 (by clausification #[9847]): ∀ (a : vAnsMap) (a_1 : vQMap), Eq (vreduce vqempty a a_1) vnoQConf % 190.21/190.47 Clause #18843 (by clausification #[359]): Eq % 190.21/190.47 (∀ (Vqtm1 : vATMap) (Vqr : vQuestionnaire) (Vqm : vQMap) (Vamr : vAnsMap) (Vatm1 : vATMap) (Vam : vAnsMap) % 190.21/190.47 (Vqmr : vQMap), % 190.21/190.47 And (vptcheck (vMC (vtypeAM Vam) (vtypeQM Vqm)) vqempty (vMC Vatm1 Vqtm1)) % 190.21/190.47 (Eq (vreduce vqempty Vam Vqm) (vsomeQConf (vQC Vamr Vqmr Vqr))) → % 190.21/190.47 vptcheck (vMC (vtypeAM Vamr) (vtypeQM Vqmr)) Vqr (vMC Vatm1 Vqtm1)) % 190.21/190.47 False % 190.21/190.47 Clause #18844 (by clausification #[18843]): ∀ (a : vATMap), % 190.21/190.47 Eq % 190.21/190.47 (Not % 190.21/190.47 (∀ (Vqr : vQuestionnaire) (Vqm : vQMap) (Vamr : vAnsMap) (Vatm1 : vATMap) (Vam : vAnsMap) (Vqmr : vQMap), % 190.21/190.47 And (vptcheck (vMC (vtypeAM Vam) (vtypeQM Vqm)) vqempty (vMC Vatm1 (skS.0 383 a))) % 190.21/190.47 (Eq (vreduce vqempty Vam Vqm) (vsomeQConf (vQC Vamr Vqmr Vqr))) → % 190.21/190.47 vptcheck (vMC (vtypeAM Vamr) (vtypeQM Vqmr)) Vqr (vMC Vatm1 (skS.0 383 a)))) % 190.21/190.47 True % 190.21/190.47 Clause #18845 (by clausification #[18844]): ∀ (a : vATMap), % 190.21/190.47 Eq % 190.21/190.47 (∀ (Vqr : vQuestionnaire) (Vqm : vQMap) (Vamr : vAnsMap) (Vatm1 : vATMap) (Vam : vAnsMap) (Vqmr : vQMap), % 190.21/190.47 And (vptcheck (vMC (vtypeAM Vam) (vtypeQM Vqm)) vqempty (vMC Vatm1 (skS.0 383 a))) % 190.21/190.47 (Eq (vreduce vqempty Vam Vqm) (vsomeQConf (vQC Vamr Vqmr Vqr))) → % 190.21/190.47 vptcheck (vMC (vtypeAM Vamr) (vtypeQM Vqmr)) Vqr (vMC Vatm1 (skS.0 383 a))) % 190.21/190.47 False % 190.21/190.47 Clause #18846 (by clausification #[18845]): ∀ (a : vATMap) (a_1 : vQuestionnaire), % 190.21/190.47 Eq % 190.21/190.47 (Not % 190.21/190.47 (∀ (Vqm : vQMap) (Vamr : vAnsMap) (Vatm1 : vATMap) (Vam : vAnsMap) (Vqmr : vQMap), % 190.21/190.47 And (vptcheck (vMC (vtypeAM Vam) (vtypeQM Vqm)) vqempty (vMC Vatm1 (skS.0 383 a))) % 190.21/190.47 (Eq (vreduce vqempty Vam Vqm) (vsomeQConf (vQC Vamr Vqmr (skS.0 384 a a_1)))) → % 190.21/190.47 vptcheck (vMC (vtypeAM Vamr) (vtypeQM Vqmr)) (skS.0 384 a a_1) (vMC Vatm1 (skS.0 383 a)))) % 190.21/190.47 True % 190.21/190.47 Clause #18847 (by clausification #[18846]): ∀ (a : vATMap) (a_1 : vQuestionnaire), % 190.21/190.47 Eq % 190.21/190.47 (∀ (Vqm : vQMap) (Vamr : vAnsMap) (Vatm1 : vATMap) (Vam : vAnsMap) (Vqmr : vQMap), % 190.21/190.47 And (vptcheck (vMC (vtypeAM Vam) (vtypeQM Vqm)) vqempty (vMC Vatm1 (skS.0 383 a))) % 190.21/190.47 (Eq (vreduce vqempty Vam Vqm) (vsomeQConf (vQC Vamr Vqmr (skS.0 384 a a_1)))) → % 190.21/190.47 vptcheck (vMC (vtypeAM Vamr) (vtypeQM Vqmr)) (skS.0 384 a a_1) (vMC Vatm1 (skS.0 383 a))) % 190.21/190.47 False % 190.21/190.47 Clause #18848 (by clausification #[18847]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap), % 190.21/190.47 Eq % 190.21/190.47 (Not % 190.21/190.47 (∀ (Vamr : vAnsMap) (Vatm1 : vATMap) (Vam : vAnsMap) (Vqmr : vQMap), % 190.21/190.47 And (vptcheck (vMC (vtypeAM Vam) (vtypeQM (skS.0 385 a a_1 a_2))) vqempty (vMC Vatm1 (skS.0 383 a))) % 190.21/190.47 (Eq (vreduce vqempty Vam (skS.0 385 a a_1 a_2)) (vsomeQConf (vQC Vamr Vqmr (skS.0 384 a a_1)))) → % 190.21/190.47 vptcheck (vMC (vtypeAM Vamr) (vtypeQM Vqmr)) (skS.0 384 a a_1) (vMC Vatm1 (skS.0 383 a)))) % 190.21/190.47 True % 190.31/190.50 Clause #18849 (by clausification #[18848]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap), % 190.31/190.50 Eq % 190.31/190.50 (∀ (Vamr : vAnsMap) (Vatm1 : vATMap) (Vam : vAnsMap) (Vqmr : vQMap), % 190.31/190.50 And (vptcheck (vMC (vtypeAM Vam) (vtypeQM (skS.0 385 a a_1 a_2))) vqempty (vMC Vatm1 (skS.0 383 a))) % 190.31/190.50 (Eq (vreduce vqempty Vam (skS.0 385 a a_1 a_2)) (vsomeQConf (vQC Vamr Vqmr (skS.0 384 a a_1)))) → % 190.31/190.50 vptcheck (vMC (vtypeAM Vamr) (vtypeQM Vqmr)) (skS.0 384 a a_1) (vMC Vatm1 (skS.0 383 a))) % 190.31/190.50 False % 190.31/190.50 Clause #18850 (by clausification #[18849]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap) (a_3 : vAnsMap), % 190.31/190.50 Eq % 190.31/190.50 (Not % 190.31/190.50 (∀ (Vatm1 : vATMap) (Vam : vAnsMap) (Vqmr : vQMap), % 190.31/190.50 And (vptcheck (vMC (vtypeAM Vam) (vtypeQM (skS.0 385 a a_1 a_2))) vqempty (vMC Vatm1 (skS.0 383 a))) % 190.31/190.50 (Eq (vreduce vqempty Vam (skS.0 385 a a_1 a_2)) % 190.31/190.50 (vsomeQConf (vQC (skS.0 386 a a_1 a_2 a_3) Vqmr (skS.0 384 a a_1)))) → % 190.31/190.50 vptcheck (vMC (vtypeAM (skS.0 386 a a_1 a_2 a_3)) (vtypeQM Vqmr)) (skS.0 384 a a_1) % 190.31/190.50 (vMC Vatm1 (skS.0 383 a)))) % 190.31/190.50 True % 190.31/190.50 Clause #18851 (by clausification #[18850]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap) (a_3 : vAnsMap), % 190.31/190.50 Eq % 190.31/190.50 (∀ (Vatm1 : vATMap) (Vam : vAnsMap) (Vqmr : vQMap), % 190.31/190.50 And (vptcheck (vMC (vtypeAM Vam) (vtypeQM (skS.0 385 a a_1 a_2))) vqempty (vMC Vatm1 (skS.0 383 a))) % 190.31/190.50 (Eq (vreduce vqempty Vam (skS.0 385 a a_1 a_2)) % 190.31/190.50 (vsomeQConf (vQC (skS.0 386 a a_1 a_2 a_3) Vqmr (skS.0 384 a a_1)))) → % 190.31/190.50 vptcheck (vMC (vtypeAM (skS.0 386 a a_1 a_2 a_3)) (vtypeQM Vqmr)) (skS.0 384 a a_1) (vMC Vatm1 (skS.0 383 a))) % 190.31/190.50 False % 190.31/190.50 Clause #18852 (by clausification #[18851]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap) (a_3 : vAnsMap) (a_4 : vATMap), % 190.31/190.50 Eq % 190.31/190.50 (Not % 190.31/190.50 (∀ (Vam : vAnsMap) (Vqmr : vQMap), % 190.31/190.50 And % 190.31/190.50 (vptcheck (vMC (vtypeAM Vam) (vtypeQM (skS.0 385 a a_1 a_2))) vqempty % 190.31/190.50 (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a))) % 190.31/190.50 (Eq (vreduce vqempty Vam (skS.0 385 a a_1 a_2)) % 190.31/190.50 (vsomeQConf (vQC (skS.0 386 a a_1 a_2 a_3) Vqmr (skS.0 384 a a_1)))) → % 190.31/190.50 vptcheck (vMC (vtypeAM (skS.0 386 a a_1 a_2 a_3)) (vtypeQM Vqmr)) (skS.0 384 a a_1) % 190.31/190.50 (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a)))) % 190.31/190.50 True % 190.31/190.50 Clause #18853 (by clausification #[18852]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap) (a_3 : vAnsMap) (a_4 : vATMap), % 190.31/190.50 Eq % 190.31/190.50 (∀ (Vam : vAnsMap) (Vqmr : vQMap), % 190.31/190.50 And % 190.31/190.50 (vptcheck (vMC (vtypeAM Vam) (vtypeQM (skS.0 385 a a_1 a_2))) vqempty % 190.31/190.50 (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a))) % 190.31/190.50 (Eq (vreduce vqempty Vam (skS.0 385 a a_1 a_2)) % 190.31/190.50 (vsomeQConf (vQC (skS.0 386 a a_1 a_2 a_3) Vqmr (skS.0 384 a a_1)))) → % 190.31/190.50 vptcheck (vMC (vtypeAM (skS.0 386 a a_1 a_2 a_3)) (vtypeQM Vqmr)) (skS.0 384 a a_1) % 190.31/190.50 (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a))) % 190.31/190.50 False % 190.31/190.50 Clause #18854 (by clausification #[18853]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap) (a_3 : vAnsMap) (a_4 : vATMap) (a_5 : vAnsMap), % 190.31/190.50 Eq % 190.31/190.50 (Not % 190.31/190.50 (∀ (Vqmr : vQMap), % 190.31/190.50 And % 190.31/190.50 (vptcheck (vMC (vtypeAM (skS.0 388 a a_1 a_2 a_3 a_4 a_5)) (vtypeQM (skS.0 385 a a_1 a_2))) vqempty % 190.31/190.50 (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a))) % 190.31/190.50 (Eq (vreduce vqempty (skS.0 388 a a_1 a_2 a_3 a_4 a_5) (skS.0 385 a a_1 a_2)) % 190.31/190.50 (vsomeQConf (vQC (skS.0 386 a a_1 a_2 a_3) Vqmr (skS.0 384 a a_1)))) → % 190.31/190.50 vptcheck (vMC (vtypeAM (skS.0 386 a a_1 a_2 a_3)) (vtypeQM Vqmr)) (skS.0 384 a a_1) % 190.31/190.50 (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a)))) % 190.31/190.50 True % 190.31/190.50 Clause #18855 (by clausification #[18854]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap) (a_3 : vAnsMap) (a_4 : vATMap) (a_5 : vAnsMap), % 190.31/190.50 Eq % 190.31/190.50 (∀ (Vqmr : vQMap), % 190.31/190.50 And % 190.31/190.50 (vptcheck (vMC (vtypeAM (skS.0 388 a a_1 a_2 a_3 a_4 a_5)) (vtypeQM (skS.0 385 a a_1 a_2))) vqempty % 190.31/190.50 (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a))) % 190.31/190.50 (Eq (vreduce vqempty (skS.0 388 a a_1 a_2 a_3 a_4 a_5) (skS.0 385 a a_1 a_2)) % 190.41/190.68 (vsomeQConf (vQC (skS.0 386 a a_1 a_2 a_3) Vqmr (skS.0 384 a a_1)))) → % 190.41/190.68 vptcheck (vMC (vtypeAM (skS.0 386 a a_1 a_2 a_3)) (vtypeQM Vqmr)) (skS.0 384 a a_1) % 190.41/190.68 (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a))) % 190.41/190.68 False % 190.41/190.68 Clause #18856 (by clausification #[18855]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap) (a_3 : vAnsMap) (a_4 : vATMap) (a_5 : vAnsMap) (a_6 : vQMap), % 190.41/190.68 Eq % 190.41/190.68 (Not % 190.41/190.68 (And % 190.41/190.68 (vptcheck (vMC (vtypeAM (skS.0 388 a a_1 a_2 a_3 a_4 a_5)) (vtypeQM (skS.0 385 a a_1 a_2))) vqempty % 190.41/190.68 (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a))) % 190.41/190.68 (Eq (vreduce vqempty (skS.0 388 a a_1 a_2 a_3 a_4 a_5) (skS.0 385 a a_1 a_2)) % 190.41/190.68 (vsomeQConf (vQC (skS.0 386 a a_1 a_2 a_3) (skS.0 389 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 384 a a_1)))) → % 190.41/190.68 vptcheck (vMC (vtypeAM (skS.0 386 a a_1 a_2 a_3)) (vtypeQM (skS.0 389 a a_1 a_2 a_3 a_4 a_5 a_6))) % 190.41/190.68 (skS.0 384 a a_1) (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a)))) % 190.41/190.68 True % 190.41/190.68 Clause #18857 (by clausification #[18856]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap) (a_3 : vAnsMap) (a_4 : vATMap) (a_5 : vAnsMap) (a_6 : vQMap), % 190.41/190.68 Eq % 190.41/190.68 (And % 190.41/190.68 (vptcheck (vMC (vtypeAM (skS.0 388 a a_1 a_2 a_3 a_4 a_5)) (vtypeQM (skS.0 385 a a_1 a_2))) vqempty % 190.41/190.68 (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a))) % 190.41/190.68 (Eq (vreduce vqempty (skS.0 388 a a_1 a_2 a_3 a_4 a_5) (skS.0 385 a a_1 a_2)) % 190.41/190.68 (vsomeQConf (vQC (skS.0 386 a a_1 a_2 a_3) (skS.0 389 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 384 a a_1)))) → % 190.41/190.68 vptcheck (vMC (vtypeAM (skS.0 386 a a_1 a_2 a_3)) (vtypeQM (skS.0 389 a a_1 a_2 a_3 a_4 a_5 a_6))) % 190.41/190.68 (skS.0 384 a a_1) (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a))) % 190.41/190.68 False % 190.41/190.68 Clause #18858 (by clausification #[18857]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap) (a_3 : vAnsMap) (a_4 : vATMap) (a_5 : vAnsMap) (a_6 : vQMap), % 190.41/190.68 Eq % 190.41/190.68 (And % 190.41/190.68 (vptcheck (vMC (vtypeAM (skS.0 388 a a_1 a_2 a_3 a_4 a_5)) (vtypeQM (skS.0 385 a a_1 a_2))) vqempty % 190.41/190.68 (vMC (skS.0 387 a a_1 a_2 a_3 a_4) (skS.0 383 a))) % 190.41/190.68 (Eq (vreduce vqempty (skS.0 388 a a_1 a_2 a_3 a_4 a_5) (skS.0 385 a a_1 a_2)) % 190.41/190.68 (vsomeQConf (vQC (skS.0 386 a a_1 a_2 a_3) (skS.0 389 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 384 a a_1))))) % 190.41/190.68 True % 190.41/190.68 Clause #18860 (by clausification #[18858]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap) (a_3 : vAnsMap) (a_4 : vATMap) (a_5 : vAnsMap) (a_6 : vQMap), % 190.41/190.68 Eq % 190.41/190.68 (Eq (vreduce vqempty (skS.0 388 a a_1 a_2 a_3 a_4 a_5) (skS.0 385 a a_1 a_2)) % 190.41/190.68 (vsomeQConf (vQC (skS.0 386 a a_1 a_2 a_3) (skS.0 389 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 384 a a_1)))) % 190.41/190.68 True % 190.41/190.68 Clause #18862 (by clausification #[18860]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap) (a_3 : vAnsMap) (a_4 : vATMap) (a_5 : vAnsMap) (a_6 : vQMap), % 190.41/190.68 Eq (vreduce vqempty (skS.0 388 a a_1 a_2 a_3 a_4 a_5) (skS.0 385 a a_1 a_2)) % 190.41/190.68 (vsomeQConf (vQC (skS.0 386 a a_1 a_2 a_3) (skS.0 389 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 384 a a_1))) % 190.41/190.68 Clause #18863 (by forward demodulation #[18862, 9848]): ∀ (a : vATMap) (a_1 : vQuestionnaire) (a_2 : vQMap) (a_3 : vAnsMap) (a_4 : vATMap) (a_5 : vAnsMap) (a_6 : vQMap), % 190.41/190.68 Eq vnoQConf (vsomeQConf (vQC (skS.0 386 a a_1 a_2 a_3) (skS.0 389 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 384 a a_1))) % 190.41/190.68 Clause #18864 (by forward contextual literal cutting #[18863, 944]): False % 190.41/190.68 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------