%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS107+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.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:52:38 PM UTC 2025 % Result : Unsatisfiable 3.97s 4.13s % Output : Proof 3.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : KRS107+1 : TPTP v9.2.0. Released v3.1.0. % 0.10/0.13 % Command : duper %s % 0.13/0.34 % Computer : n012.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 10:16:38 EDT 2025 % 0.13/0.34 % CPUTime : % 3.97/4.13 SZS status Theorem for theBenchmark.p % 3.97/4.13 SZS output start Proof for theBenchmark.p % 3.97/4.13 Clause #34 (by assumption #[]): Eq % 3.97/4.13 (∀ (X : Iota), % 3.97/4.13 Iff (cUnsatisfiable X) % 3.97/4.13 (And (And (Exists fun Y => And (rrx3 X Y) (cc1 Y)) (Exists fun Y => And (rrx4 X Y) (cc2 Y))) (ca_Cx1 X))) % 3.97/4.13 True % 3.97/4.13 Clause #35 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Ax2 X) (And (cc2 X) (cc1 X))) True % 3.97/4.13 Clause #36 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Cx1 X) (Exists fun Y0 => ra_Px1 X Y0)) True % 3.97/4.13 Clause #37 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Cx1xcomp X) (Exists fun Y => And (rrx3 X Y) (ca_Ax2 Y))) True % 3.97/4.13 Clause #38 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Cx1xcomp X) (Not (Exists fun Y => ra_Px1 X Y))) True % 3.97/4.13 Clause #39 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (rrx X Y) (rrx X Z) → Eq Y Z) True % 3.97/4.13 Clause #44 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_21_01226) True % 3.97/4.13 Clause #49 (by assumption #[]): Eq (∀ (X Y : Iota), rrx4 X Y → rrx X Y) True % 3.97/4.13 Clause #52 (by assumption #[]): Eq (∀ (X Y : Iota), rrx3 X Y → rrx X Y) True % 3.97/4.14 Clause #126 (by clausification #[49]): ∀ (a : Iota), Eq (∀ (Y : Iota), rrx4 a Y → rrx a Y) True % 3.97/4.14 Clause #127 (by clausification #[126]): ∀ (a a_1 : Iota), Eq (rrx4 a a_1 → rrx a a_1) True % 3.97/4.14 Clause #128 (by clausification #[127]): ∀ (a a_1 : Iota), Or (Eq (rrx4 a a_1) False) (Eq (rrx a a_1) True) % 3.97/4.14 Clause #147 (by clausification #[52]): ∀ (a : Iota), Eq (∀ (Y : Iota), rrx3 a Y → rrx a Y) True % 3.97/4.14 Clause #148 (by clausification #[147]): ∀ (a a_1 : Iota), Eq (rrx3 a a_1 → rrx a a_1) True % 3.97/4.14 Clause #149 (by clausification #[148]): ∀ (a a_1 : Iota), Or (Eq (rrx3 a a_1) False) (Eq (rrx a a_1) True) % 3.97/4.14 Clause #301 (by clausification #[34]): ∀ (a : Iota), % 3.97/4.14 Eq % 3.97/4.14 (Iff (cUnsatisfiable a) % 3.97/4.14 (And (And (Exists fun Y => And (rrx3 a Y) (cc1 Y)) (Exists fun Y => And (rrx4 a Y) (cc2 Y))) (ca_Cx1 a))) % 3.97/4.14 True % 3.97/4.14 Clause #303 (by clausification #[301]): ∀ (a : Iota), % 3.97/4.14 Or (Eq (cUnsatisfiable a) False) % 3.97/4.14 (Eq (And (And (Exists fun Y => And (rrx3 a Y) (cc1 Y)) (Exists fun Y => And (rrx4 a Y) (cc2 Y))) (ca_Cx1 a)) True) % 3.97/4.14 Clause #310 (by clausification #[39]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (rrx a Y) (rrx a Z) → Eq Y Z) True % 3.97/4.14 Clause #311 (by clausification #[310]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (rrx a a_1) (rrx a Z) → Eq a_1 Z) True % 3.97/4.14 Clause #312 (by clausification #[311]): ∀ (a a_1 a_2 : Iota), Eq (And (rrx a a_1) (rrx a a_2) → Eq a_1 a_2) True % 3.97/4.14 Clause #313 (by clausification #[312]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (rrx a a_1) (rrx a a_2)) False) (Eq (Eq a_1 a_2) True) % 3.97/4.14 Clause #314 (by clausification #[313]): ∀ (a a_1 a_2 : Iota), Or (Eq (Eq a a_1) True) (Or (Eq (rrx a_2 a) False) (Eq (rrx a_2 a_1) False)) % 3.97/4.14 Clause #315 (by clausification #[314]): ∀ (a a_1 a_2 : Iota), Or (Eq (rrx a a_1) False) (Or (Eq (rrx a a_2) False) (Eq a_1 a_2)) % 3.97/4.14 Clause #328 (by clausification #[35]): ∀ (a : Iota), Eq (Iff (ca_Ax2 a) (And (cc2 a) (cc1 a))) True % 3.97/4.14 Clause #329 (by clausification #[328]): ∀ (a : Iota), Or (Eq (ca_Ax2 a) True) (Eq (And (cc2 a) (cc1 a)) False) % 3.97/4.14 Clause #331 (by clausification #[329]): ∀ (a : Iota), Or (Eq (ca_Ax2 a) True) (Or (Eq (cc2 a) False) (Eq (cc1 a) False)) % 3.97/4.14 Clause #334 (by betaEtaReduce #[36]): Eq (∀ (X : Iota), Iff (ca_Cx1 X) (Exists (ra_Px1 X))) True % 3.97/4.14 Clause #335 (by clausification #[334]): ∀ (a : Iota), Eq (Iff (ca_Cx1 a) (Exists (ra_Px1 a))) True % 3.97/4.14 Clause #337 (by clausification #[335]): ∀ (a : Iota), Or (Eq (ca_Cx1 a) False) (Eq (Exists (ra_Px1 a)) True) % 3.97/4.14 Clause #339 (by clausification #[337]): ∀ (a a_1 : Iota), Or (Eq (ca_Cx1 a) False) (Eq (ra_Px1 a (skS.0 0 a a_1)) True) % 3.97/4.14 Clause #340 (by betaEtaReduce #[38]): Eq (∀ (X : Iota), Iff (ca_Cx1xcomp X) (Not (Exists (ra_Px1 X)))) True % 3.97/4.14 Clause #341 (by clausification #[340]): ∀ (a : Iota), Eq (Iff (ca_Cx1xcomp a) (Not (Exists (ra_Px1 a)))) True % 3.97/4.14 Clause #343 (by clausification #[341]): ∀ (a : Iota), Or (Eq (ca_Cx1xcomp a) False) (Eq (Not (Exists (ra_Px1 a))) True) % 3.97/4.14 Clause #348 (by clausification #[343]): ∀ (a : Iota), Or (Eq (ca_Cx1xcomp a) False) (Eq (Exists (ra_Px1 a)) False) % 3.97/4.14 Clause #349 (by clausification #[348]): ∀ (a a_1 : Iota), Or (Eq (ca_Cx1xcomp a) False) (Eq (ra_Px1 a a_1) False) % 3.97/4.16 Clause #351 (by clausification #[37]): ∀ (a : Iota), Eq (Iff (ca_Cx1xcomp a) (Exists fun Y => And (rrx3 a Y) (ca_Ax2 Y))) True % 3.97/4.16 Clause #352 (by clausification #[351]): ∀ (a : Iota), Or (Eq (ca_Cx1xcomp a) True) (Eq (Exists fun Y => And (rrx3 a Y) (ca_Ax2 Y)) False) % 3.97/4.16 Clause #354 (by clausification #[352]): ∀ (a a_1 : Iota), Or (Eq (ca_Cx1xcomp a) True) (Eq (And (rrx3 a a_1) (ca_Ax2 a_1)) False) % 3.97/4.16 Clause #355 (by clausification #[354]): ∀ (a a_1 : Iota), Or (Eq (ca_Cx1xcomp a) True) (Or (Eq (rrx3 a a_1) False) (Eq (ca_Ax2 a_1) False)) % 3.97/4.16 Clause #367 (by clausification #[303]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (ca_Cx1 a) True) % 3.97/4.16 Clause #368 (by clausification #[303]): ∀ (a : Iota), % 3.97/4.16 Or (Eq (cUnsatisfiable a) False) % 3.97/4.16 (Eq (And (Exists fun Y => And (rrx3 a Y) (cc1 Y)) (Exists fun Y => And (rrx4 a Y) (cc2 Y))) True) % 3.97/4.16 Clause #369 (by superposition #[367, 44]): Or (Eq (ca_Cx1 i2003_11_14_17_21_01226) True) (Eq False True) % 3.97/4.16 Clause #370 (by clausification #[369]): Eq (ca_Cx1 i2003_11_14_17_21_01226) True % 3.97/4.16 Clause #372 (by superposition #[370, 339]): ∀ (a : Iota), Or (Eq True False) (Eq (ra_Px1 i2003_11_14_17_21_01226 (skS.0 0 i2003_11_14_17_21_01226 a)) True) % 3.97/4.16 Clause #373 (by clausification #[372]): ∀ (a : Iota), Eq (ra_Px1 i2003_11_14_17_21_01226 (skS.0 0 i2003_11_14_17_21_01226 a)) True % 3.97/4.16 Clause #390 (by clausification #[368]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y => And (rrx4 a Y) (cc2 Y)) True) % 3.97/4.16 Clause #391 (by clausification #[368]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y => And (rrx3 a Y) (cc1 Y)) True) % 3.97/4.16 Clause #392 (by clausification #[390]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (rrx4 a (skS.0 3 a a_1)) (cc2 (skS.0 3 a a_1))) True) % 3.97/4.16 Clause #393 (by clausification #[392]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cc2 (skS.0 3 a a_1)) True) % 3.97/4.16 Clause #394 (by clausification #[392]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rrx4 a (skS.0 3 a a_1)) True) % 3.97/4.16 Clause #395 (by superposition #[393, 44]): ∀ (a : Iota), Or (Eq (cc2 (skS.0 3 i2003_11_14_17_21_01226 a)) True) (Eq False True) % 3.97/4.16 Clause #396 (by clausification #[395]): ∀ (a : Iota), Eq (cc2 (skS.0 3 i2003_11_14_17_21_01226 a)) True % 3.97/4.16 Clause #397 (by superposition #[396, 331]): ∀ (a : Iota), % 3.97/4.16 Or (Eq (ca_Ax2 (skS.0 3 i2003_11_14_17_21_01226 a)) True) % 3.97/4.16 (Or (Eq True False) (Eq (cc1 (skS.0 3 i2003_11_14_17_21_01226 a)) False)) % 3.97/4.16 Clause #398 (by clausification #[391]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (rrx3 a (skS.0 4 a a_1)) (cc1 (skS.0 4 a a_1))) True) % 3.97/4.16 Clause #399 (by clausification #[398]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cc1 (skS.0 4 a a_1)) True) % 3.97/4.16 Clause #400 (by clausification #[398]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rrx3 a (skS.0 4 a a_1)) True) % 3.97/4.16 Clause #401 (by superposition #[399, 44]): ∀ (a : Iota), Or (Eq (cc1 (skS.0 4 i2003_11_14_17_21_01226 a)) True) (Eq False True) % 3.97/4.16 Clause #402 (by clausification #[401]): ∀ (a : Iota), Eq (cc1 (skS.0 4 i2003_11_14_17_21_01226 a)) True % 3.97/4.16 Clause #403 (by superposition #[394, 44]): ∀ (a : Iota), Or (Eq (rrx4 i2003_11_14_17_21_01226 (skS.0 3 i2003_11_14_17_21_01226 a)) True) (Eq False True) % 3.97/4.16 Clause #404 (by clausification #[403]): ∀ (a : Iota), Eq (rrx4 i2003_11_14_17_21_01226 (skS.0 3 i2003_11_14_17_21_01226 a)) True % 3.97/4.16 Clause #405 (by superposition #[404, 128]): ∀ (a : Iota), Or (Eq True False) (Eq (rrx i2003_11_14_17_21_01226 (skS.0 3 i2003_11_14_17_21_01226 a)) True) % 3.97/4.16 Clause #411 (by clausification #[405]): ∀ (a : Iota), Eq (rrx i2003_11_14_17_21_01226 (skS.0 3 i2003_11_14_17_21_01226 a)) True % 3.97/4.16 Clause #412 (by superposition #[411, 315]): ∀ (a a_1 : Iota), % 3.97/4.16 Or (Eq True False) (Or (Eq (rrx i2003_11_14_17_21_01226 a) False) (Eq (skS.0 3 i2003_11_14_17_21_01226 a_1) a)) % 3.97/4.16 Clause #414 (by superposition #[400, 44]): ∀ (a : Iota), Or (Eq (rrx3 i2003_11_14_17_21_01226 (skS.0 4 i2003_11_14_17_21_01226 a)) True) (Eq False True) % 3.97/4.16 Clause #415 (by clausification #[414]): ∀ (a : Iota), Eq (rrx3 i2003_11_14_17_21_01226 (skS.0 4 i2003_11_14_17_21_01226 a)) True % 3.97/4.17 Clause #417 (by superposition #[415, 149]): ∀ (a : Iota), Or (Eq True False) (Eq (rrx i2003_11_14_17_21_01226 (skS.0 4 i2003_11_14_17_21_01226 a)) True) % 3.97/4.17 Clause #419 (by superposition #[415, 355]): ∀ (a : Iota), % 3.97/4.17 Or (Eq (ca_Cx1xcomp i2003_11_14_17_21_01226) True) % 3.97/4.17 (Or (Eq True False) (Eq (ca_Ax2 (skS.0 4 i2003_11_14_17_21_01226 a)) False)) % 3.97/4.17 Clause #421 (by clausification #[417]): ∀ (a : Iota), Eq (rrx i2003_11_14_17_21_01226 (skS.0 4 i2003_11_14_17_21_01226 a)) True % 3.97/4.17 Clause #433 (by clausification #[412]): ∀ (a a_1 : Iota), Or (Eq (rrx i2003_11_14_17_21_01226 a) False) (Eq (skS.0 3 i2003_11_14_17_21_01226 a_1) a) % 3.97/4.17 Clause #435 (by superposition #[433, 421]): ∀ (a a_1 : Iota), Or (Eq (skS.0 3 i2003_11_14_17_21_01226 a) (skS.0 4 i2003_11_14_17_21_01226 a_1)) (Eq False True) % 3.97/4.17 Clause #442 (by clausification #[419]): ∀ (a : Iota), Or (Eq (ca_Cx1xcomp i2003_11_14_17_21_01226) True) (Eq (ca_Ax2 (skS.0 4 i2003_11_14_17_21_01226 a)) False) % 3.97/4.17 Clause #447 (by clausification #[397]): ∀ (a : Iota), % 3.97/4.17 Or (Eq (ca_Ax2 (skS.0 3 i2003_11_14_17_21_01226 a)) True) (Eq (cc1 (skS.0 3 i2003_11_14_17_21_01226 a)) False) % 3.97/4.17 Clause #450 (by clausification #[435]): ∀ (a a_1 : Iota), Eq (skS.0 3 i2003_11_14_17_21_01226 a) (skS.0 4 i2003_11_14_17_21_01226 a_1) % 3.97/4.17 Clause #456 (by superposition #[450, 402]): ∀ (a : Iota), Eq (cc1 (skS.0 3 i2003_11_14_17_21_01226 a)) True % 3.97/4.17 Clause #459 (by superposition #[450, 442]): ∀ (a : Iota), Or (Eq (ca_Cx1xcomp i2003_11_14_17_21_01226) True) (Eq (ca_Ax2 (skS.0 3 i2003_11_14_17_21_01226 a)) False) % 3.97/4.17 Clause #462 (by backward demodulation #[456, 447]): ∀ (a : Iota), Or (Eq (ca_Ax2 (skS.0 3 i2003_11_14_17_21_01226 a)) True) (Eq True False) % 3.97/4.17 Clause #473 (by clausification #[462]): ∀ (a : Iota), Eq (ca_Ax2 (skS.0 3 i2003_11_14_17_21_01226 a)) True % 3.97/4.17 Clause #476 (by superposition #[459, 473]): Or (Eq (ca_Cx1xcomp i2003_11_14_17_21_01226) True) (Eq True False) % 3.97/4.17 Clause #477 (by clausification #[476]): Eq (ca_Cx1xcomp i2003_11_14_17_21_01226) True % 3.97/4.17 Clause #480 (by superposition #[477, 349]): ∀ (a : Iota), Or (Eq True False) (Eq (ra_Px1 i2003_11_14_17_21_01226 a) False) % 3.97/4.17 Clause #483 (by clausification #[480]): ∀ (a : Iota), Eq (ra_Px1 i2003_11_14_17_21_01226 a) False % 3.97/4.17 Clause #484 (by superposition #[483, 373]): Eq False True % 3.97/4.17 Clause #486 (by clausification #[484]): False % 3.97/4.17 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------