%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS156+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n028.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:43 PM UTC 2025 % Result : Theorem 14.38s 14.59s % Output : Proof 14.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS156+1 : TPTP v9.2.0. Released v3.1.0. % 0.07/0.13 % Command : duper %s % 0.12/0.34 % Computer : n028.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Oct 2 10:22:38 EDT 2025 % 0.12/0.34 % CPUTime : % 14.38/14.59 SZS status Theorem for theBenchmark.p % 14.38/14.59 SZS output start Proof for theBenchmark.p % 14.38/14.59 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 14.38/14.59 Clause #1 (by assumption #[]): Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) True % 14.38/14.59 Clause #25 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC116 X) (And (cTOP X) (cC114xcomp X))) True % 14.38/14.59 Clause #49 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC140 X) (And (cTOP X) (cC138 X))) True % 14.38/14.59 Clause #127 (by assumption #[]): Eq (∀ (X : Iota), Iff (cTEST X) (And (cC140 X) (cC116 X))) True % 14.38/14.59 Clause #128 (by assumption #[]): Eq (cTOP iV5475) True % 14.38/14.59 Clause #130 (by assumption #[]): Eq (cC114xcomp iV5475) True % 14.38/14.59 Clause #131 (by assumption #[]): Eq (cTEST iV5475) True % 14.38/14.59 Clause #145 (by assumption #[]): Eq % 14.38/14.59 (Not % 14.38/14.59 (And % 14.38/14.59 (And % 14.38/14.59 (And % 14.38/14.59 (And % 14.38/14.59 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 14.38/14.59 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 14.38/14.59 (cC116 iV5475)) % 14.38/14.59 (cC140 iV5475)) % 14.38/14.59 (cowlThing iV5475)) % 14.38/14.59 (cC138 iV5475))) % 14.38/14.59 True % 14.38/14.59 Clause #146 (by clausification #[0]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 14.38/14.59 Clause #147 (by clausification #[146]): ∀ (a : Iota), Eq (Not (cowlNothing a)) True % 14.38/14.59 Clause #148 (by clausification #[146]): ∀ (a : Iota), Eq (cowlThing a) True % 14.38/14.59 Clause #149 (by clausification #[147]): ∀ (a : Iota), Eq (cowlNothing a) False % 14.38/14.59 Clause #150 (by clausification #[1]): ∀ (a : Iota), Eq (Iff (xsd_string a) (Not (xsd_integer a))) True % 14.38/14.59 Clause #151 (by clausification #[150]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (Not (xsd_integer a)) False) % 14.38/14.59 Clause #152 (by clausification #[150]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (Not (xsd_integer a)) True) % 14.38/14.59 Clause #153 (by clausification #[151]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (xsd_integer a) True) % 14.38/14.59 Clause #169 (by clausification #[152]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (xsd_integer a) False) % 14.38/14.59 Clause #220 (by clausification #[25]): ∀ (a : Iota), Eq (Iff (cC116 a) (And (cTOP a) (cC114xcomp a))) True % 14.38/14.59 Clause #221 (by clausification #[220]): ∀ (a : Iota), Or (Eq (cC116 a) True) (Eq (And (cTOP a) (cC114xcomp a)) False) % 14.38/14.59 Clause #223 (by clausification #[221]): ∀ (a : Iota), Or (Eq (cC116 a) True) (Or (Eq (cTOP a) False) (Eq (cC114xcomp a) False)) % 14.38/14.59 Clause #224 (by superposition #[223, 128]): Or (Eq (cC116 iV5475) True) (Or (Eq (cC114xcomp iV5475) False) (Eq False True)) % 14.38/14.59 Clause #225 (by clausification #[224]): Or (Eq (cC116 iV5475) True) (Eq (cC114xcomp iV5475) False) % 14.38/14.59 Clause #226 (by forward demodulation #[225, 130]): Or (Eq (cC116 iV5475) True) (Eq True False) % 14.38/14.59 Clause #227 (by clausification #[226]): Eq (cC116 iV5475) True % 14.38/14.59 Clause #297 (by clausification #[49]): ∀ (a : Iota), Eq (Iff (cC140 a) (And (cTOP a) (cC138 a))) True % 14.38/14.59 Clause #299 (by clausification #[297]): ∀ (a : Iota), Or (Eq (cC140 a) False) (Eq (And (cTOP a) (cC138 a)) True) % 14.38/14.59 Clause #315 (by clausification #[299]): ∀ (a : Iota), Or (Eq (cC140 a) False) (Eq (cC138 a) True) % 14.38/14.59 Clause #405 (by clausification #[127]): ∀ (a : Iota), Eq (Iff (cTEST a) (And (cC140 a) (cC116 a))) True % 14.38/14.59 Clause #407 (by clausification #[405]): ∀ (a : Iota), Or (Eq (cTEST a) False) (Eq (And (cC140 a) (cC116 a)) True) % 14.38/14.59 Clause #410 (by clausification #[407]): ∀ (a : Iota), Or (Eq (cTEST a) False) (Eq (cC140 a) True) % 14.38/14.59 Clause #418 (by superposition #[410, 131]): Or (Eq (cC140 iV5475) True) (Eq False True) % 14.38/14.59 Clause #419 (by clausification #[418]): Eq (cC140 iV5475) True % 14.38/14.59 Clause #421 (by superposition #[419, 315]): Or (Eq True False) (Eq (cC138 iV5475) True) % 14.38/14.59 Clause #424 (by clausification #[421]): Eq (cC138 iV5475) True % 14.38/14.59 Clause #1356 (by clausification #[145]): Eq % 14.38/14.59 (And % 14.38/14.59 (And % 14.38/14.59 (And % 14.38/14.59 (And % 14.38/14.59 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 14.38/14.59 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 14.38/14.59 (cC116 iV5475)) % 14.38/14.59 (cC140 iV5475)) % 14.38/14.59 (cowlThing iV5475)) % 14.38/14.59 (cC138 iV5475)) % 14.38/14.59 False % 14.38/14.59 Clause #1357 (by clausification #[1356]): Or % 14.38/14.59 (Eq % 14.38/14.59 (And % 14.38/14.59 (And % 14.38/14.59 (And % 14.45/14.62 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 14.45/14.62 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 14.45/14.62 (cC116 iV5475)) % 14.45/14.62 (cC140 iV5475)) % 14.45/14.62 (cowlThing iV5475)) % 14.45/14.62 False) % 14.45/14.62 (Eq (cC138 iV5475) False) % 14.45/14.62 Clause #1358 (by clausification #[1357]): Or (Eq (cC138 iV5475) False) % 14.45/14.62 (Or % 14.45/14.62 (Eq % 14.45/14.62 (And % 14.45/14.62 (And % 14.45/14.62 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 14.45/14.62 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 14.45/14.62 (cC116 iV5475)) % 14.45/14.62 (cC140 iV5475)) % 14.45/14.62 False) % 14.45/14.62 (Eq (cowlThing iV5475) False)) % 14.45/14.62 Clause #1359 (by clausification #[1358]): Or (Eq (cC138 iV5475) False) % 14.45/14.62 (Or (Eq (cowlThing iV5475) False) % 14.45/14.62 (Or % 14.45/14.62 (Eq % 14.45/14.62 (And % 14.45/14.62 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 14.45/14.62 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 14.45/14.62 (cC116 iV5475)) % 14.45/14.62 False) % 14.45/14.62 (Eq (cC140 iV5475) False))) % 14.45/14.62 Clause #1360 (by clausification #[1359]): Or (Eq (cC138 iV5475) False) % 14.45/14.62 (Or (Eq (cowlThing iV5475) False) % 14.45/14.62 (Or (Eq (cC140 iV5475) False) % 14.45/14.62 (Or % 14.45/14.62 (Eq % 14.45/14.62 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 14.45/14.62 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 14.45/14.62 False) % 14.45/14.62 (Eq (cC116 iV5475) False)))) % 14.45/14.62 Clause #1361 (by clausification #[1360]): Or (Eq (cC138 iV5475) False) % 14.45/14.62 (Or (Eq (cowlThing iV5475) False) % 14.45/14.62 (Or (Eq (cC140 iV5475) False) % 14.45/14.62 (Or (Eq (cC116 iV5475) False) % 14.45/14.62 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 14.45/14.62 (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False))))) % 14.45/14.62 Clause #1362 (by clausification #[1361]): ∀ (a : Iota), % 14.45/14.62 Or (Eq (cC138 iV5475) False) % 14.45/14.62 (Or (Eq (cowlThing iV5475) False) % 14.45/14.62 (Or (Eq (cC140 iV5475) False) % 14.45/14.62 (Or (Eq (cC116 iV5475) False) % 14.45/14.62 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 14.45/14.62 (Eq (Not (And (cowlThing (skS.0 94 a)) (Not (cowlNothing (skS.0 94 a))))) True))))) % 14.45/14.62 Clause #1363 (by clausification #[1362]): ∀ (a a_1 : Iota), % 14.45/14.62 Or (Eq (cC138 iV5475) False) % 14.45/14.62 (Or (Eq (cowlThing iV5475) False) % 14.45/14.62 (Or (Eq (cC140 iV5475) False) % 14.45/14.62 (Or (Eq (cC116 iV5475) False) % 14.45/14.62 (Or (Eq (Not (And (cowlThing (skS.0 94 a)) (Not (cowlNothing (skS.0 94 a))))) True) % 14.45/14.62 (Eq (Not (Iff (xsd_string (skS.0 95 a_1)) (Not (xsd_integer (skS.0 95 a_1))))) True))))) % 14.45/14.62 Clause #1364 (by clausification #[1363]): ∀ (a a_1 : Iota), % 14.45/14.62 Or (Eq (cC138 iV5475) False) % 14.45/14.62 (Or (Eq (cowlThing iV5475) False) % 14.45/14.62 (Or (Eq (cC140 iV5475) False) % 14.45/14.62 (Or (Eq (cC116 iV5475) False) % 14.45/14.62 (Or (Eq (Not (Iff (xsd_string (skS.0 95 a)) (Not (xsd_integer (skS.0 95 a))))) True) % 14.45/14.62 (Eq (And (cowlThing (skS.0 94 a_1)) (Not (cowlNothing (skS.0 94 a_1)))) False))))) % 14.45/14.62 Clause #1365 (by clausification #[1364]): ∀ (a a_1 : Iota), % 14.45/14.62 Or (Eq (cC138 iV5475) False) % 14.45/14.62 (Or (Eq (cowlThing iV5475) False) % 14.45/14.62 (Or (Eq (cC140 iV5475) False) % 14.45/14.62 (Or (Eq (cC116 iV5475) False) % 14.45/14.62 (Or (Eq (And (cowlThing (skS.0 94 a)) (Not (cowlNothing (skS.0 94 a)))) False) % 14.45/14.62 (Eq (Iff (xsd_string (skS.0 95 a_1)) (Not (xsd_integer (skS.0 95 a_1)))) False))))) % 14.45/14.62 Clause #1366 (by clausification #[1365]): ∀ (a a_1 : Iota), % 14.45/14.62 Or (Eq (cC138 iV5475) False) % 14.45/14.62 (Or (Eq (cowlThing iV5475) False) % 14.45/14.62 (Or (Eq (cC140 iV5475) False) % 14.45/14.62 (Or (Eq (cC116 iV5475) False) % 14.45/14.62 (Or (Eq (Iff (xsd_string (skS.0 95 a)) (Not (xsd_integer (skS.0 95 a)))) False) % 14.45/14.62 (Or (Eq (cowlThing (skS.0 94 a_1)) False) (Eq (Not (cowlNothing (skS.0 94 a_1))) False)))))) % 14.45/14.62 Clause #1367 (by clausification #[1366]): ∀ (a a_1 : Iota), % 14.45/14.62 Or (Eq (cC138 iV5475) False) % 14.45/14.62 (Or (Eq (cowlThing iV5475) False) % 14.45/14.62 (Or (Eq (cC140 iV5475) False) % 14.45/14.62 (Or (Eq (cC116 iV5475) False) % 14.45/14.62 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.45/14.62 (Or (Eq (Not (cowlNothing (skS.0 94 a))) False) % 14.45/14.62 (Or (Eq (xsd_string (skS.0 95 a_1)) False) (Eq (Not (xsd_integer (skS.0 95 a_1))) False))))))) % 14.45/14.62 Clause #1368 (by clausification #[1366]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq (cC138 iV5475) False) % 14.45/14.64 (Or (Eq (cowlThing iV5475) False) % 14.45/14.64 (Or (Eq (cC140 iV5475) False) % 14.45/14.64 (Or (Eq (cC116 iV5475) False) % 14.45/14.64 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.45/14.64 (Or (Eq (Not (cowlNothing (skS.0 94 a))) False) % 14.45/14.64 (Or (Eq (xsd_string (skS.0 95 a_1)) True) (Eq (Not (xsd_integer (skS.0 95 a_1))) True))))))) % 14.45/14.64 Clause #1369 (by clausification #[1367]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq (cC138 iV5475) False) % 14.45/14.64 (Or (Eq (cowlThing iV5475) False) % 14.45/14.64 (Or (Eq (cC140 iV5475) False) % 14.45/14.64 (Or (Eq (cC116 iV5475) False) % 14.45/14.64 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.45/14.64 (Or (Eq (xsd_string (skS.0 95 a_1)) False) % 14.45/14.64 (Or (Eq (Not (xsd_integer (skS.0 95 a_1))) False) (Eq (cowlNothing (skS.0 94 a)) True))))))) % 14.45/14.64 Clause #1370 (by clausification #[1369]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq (cC138 iV5475) False) % 14.45/14.64 (Or (Eq (cowlThing iV5475) False) % 14.45/14.64 (Or (Eq (cC140 iV5475) False) % 14.45/14.64 (Or (Eq (cC116 iV5475) False) % 14.45/14.64 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.45/14.64 (Or (Eq (xsd_string (skS.0 95 a_1)) False) % 14.45/14.64 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) True))))))) % 14.45/14.64 Clause #1371 (by forward demodulation #[1370, 424]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq True False) % 14.45/14.64 (Or (Eq (cowlThing iV5475) False) % 14.45/14.64 (Or (Eq (cC140 iV5475) False) % 14.45/14.64 (Or (Eq (cC116 iV5475) False) % 14.45/14.64 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.45/14.64 (Or (Eq (xsd_string (skS.0 95 a_1)) False) % 14.45/14.64 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) True))))))) % 14.45/14.64 Clause #1372 (by clausification #[1371]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq (cowlThing iV5475) False) % 14.45/14.64 (Or (Eq (cC140 iV5475) False) % 14.45/14.64 (Or (Eq (cC116 iV5475) False) % 14.45/14.64 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.45/14.64 (Or (Eq (xsd_string (skS.0 95 a_1)) False) % 14.45/14.64 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) True)))))) % 14.45/14.64 Clause #1373 (by forward demodulation #[1372, 148]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq True False) % 14.45/14.64 (Or (Eq (cC140 iV5475) False) % 14.45/14.64 (Or (Eq (cC116 iV5475) False) % 14.45/14.64 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.45/14.64 (Or (Eq (xsd_string (skS.0 95 a_1)) False) % 14.45/14.64 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) True)))))) % 14.45/14.64 Clause #1374 (by clausification #[1373]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq (cC140 iV5475) False) % 14.45/14.64 (Or (Eq (cC116 iV5475) False) % 14.45/14.64 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.45/14.64 (Or (Eq (xsd_string (skS.0 95 a_1)) False) % 14.45/14.64 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) True))))) % 14.45/14.64 Clause #1375 (by forward demodulation #[1374, 419]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq True False) % 14.45/14.64 (Or (Eq (cC116 iV5475) False) % 14.45/14.64 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.45/14.64 (Or (Eq (xsd_string (skS.0 95 a_1)) False) % 14.45/14.64 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) True))))) % 14.45/14.64 Clause #1376 (by clausification #[1375]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq (cC116 iV5475) False) % 14.45/14.64 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.45/14.64 (Or (Eq (xsd_string (skS.0 95 a_1)) False) % 14.45/14.64 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) True)))) % 14.45/14.64 Clause #1377 (by forward demodulation #[1376, 227]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq True False) % 14.45/14.64 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.45/14.64 (Or (Eq (xsd_string (skS.0 95 a_1)) False) % 14.45/14.64 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) True)))) % 14.45/14.64 Clause #1378 (by clausification #[1377]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq (cowlThing (skS.0 94 a)) False) % 14.45/14.64 (Or (Eq (xsd_string (skS.0 95 a_1)) False) % 14.45/14.64 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) True))) % 14.45/14.64 Clause #1379 (by forward demodulation #[1378, 148]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq True False) % 14.45/14.64 (Or (Eq (xsd_string (skS.0 95 a)) False) % 14.45/14.64 (Or (Eq (cowlNothing (skS.0 94 a_1)) True) (Eq (xsd_integer (skS.0 95 a)) True))) % 14.45/14.64 Clause #1380 (by clausification #[1379]): ∀ (a a_1 : Iota), % 14.45/14.64 Or (Eq (xsd_string (skS.0 95 a)) False) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a_1)) True) (Eq (xsd_integer (skS.0 95 a)) True)) % 14.51/14.67 Clause #1585 (by clausification #[1368]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq (cC138 iV5475) False) % 14.51/14.67 (Or (Eq (cowlThing iV5475) False) % 14.51/14.67 (Or (Eq (cC140 iV5475) False) % 14.51/14.67 (Or (Eq (cC116 iV5475) False) % 14.51/14.67 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.51/14.67 (Or (Eq (xsd_string (skS.0 95 a_1)) True) % 14.51/14.67 (Or (Eq (Not (xsd_integer (skS.0 95 a_1))) True) (Eq (cowlNothing (skS.0 94 a)) True))))))) % 14.51/14.67 Clause #1586 (by clausification #[1585]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq (cC138 iV5475) False) % 14.51/14.67 (Or (Eq (cowlThing iV5475) False) % 14.51/14.67 (Or (Eq (cC140 iV5475) False) % 14.51/14.67 (Or (Eq (cC116 iV5475) False) % 14.51/14.67 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.51/14.67 (Or (Eq (xsd_string (skS.0 95 a_1)) True) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) False))))))) % 14.51/14.67 Clause #1587 (by forward demodulation #[1586, 424]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq True False) % 14.51/14.67 (Or (Eq (cowlThing iV5475) False) % 14.51/14.67 (Or (Eq (cC140 iV5475) False) % 14.51/14.67 (Or (Eq (cC116 iV5475) False) % 14.51/14.67 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.51/14.67 (Or (Eq (xsd_string (skS.0 95 a_1)) True) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) False))))))) % 14.51/14.67 Clause #1588 (by clausification #[1587]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq (cowlThing iV5475) False) % 14.51/14.67 (Or (Eq (cC140 iV5475) False) % 14.51/14.67 (Or (Eq (cC116 iV5475) False) % 14.51/14.67 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.51/14.67 (Or (Eq (xsd_string (skS.0 95 a_1)) True) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) False)))))) % 14.51/14.67 Clause #1589 (by forward demodulation #[1588, 148]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq True False) % 14.51/14.67 (Or (Eq (cC140 iV5475) False) % 14.51/14.67 (Or (Eq (cC116 iV5475) False) % 14.51/14.67 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.51/14.67 (Or (Eq (xsd_string (skS.0 95 a_1)) True) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) False)))))) % 14.51/14.67 Clause #1590 (by clausification #[1589]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq (cC140 iV5475) False) % 14.51/14.67 (Or (Eq (cC116 iV5475) False) % 14.51/14.67 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.51/14.67 (Or (Eq (xsd_string (skS.0 95 a_1)) True) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) False))))) % 14.51/14.67 Clause #1591 (by forward demodulation #[1590, 419]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq True False) % 14.51/14.67 (Or (Eq (cC116 iV5475) False) % 14.51/14.67 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.51/14.67 (Or (Eq (xsd_string (skS.0 95 a_1)) True) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) False))))) % 14.51/14.67 Clause #1592 (by clausification #[1591]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq (cC116 iV5475) False) % 14.51/14.67 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.51/14.67 (Or (Eq (xsd_string (skS.0 95 a_1)) True) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) False)))) % 14.51/14.67 Clause #1593 (by forward demodulation #[1592, 227]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq True False) % 14.51/14.67 (Or (Eq (cowlThing (skS.0 94 a)) False) % 14.51/14.67 (Or (Eq (xsd_string (skS.0 95 a_1)) True) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) False)))) % 14.51/14.67 Clause #1594 (by clausification #[1593]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq (cowlThing (skS.0 94 a)) False) % 14.51/14.67 (Or (Eq (xsd_string (skS.0 95 a_1)) True) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) False))) % 14.51/14.67 Clause #1595 (by forward demodulation #[1594, 148]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq True False) % 14.51/14.67 (Or (Eq (xsd_string (skS.0 95 a)) True) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a_1)) True) (Eq (xsd_integer (skS.0 95 a)) False))) % 14.51/14.67 Clause #1596 (by clausification #[1595]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq (xsd_string (skS.0 95 a)) True) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a_1)) True) (Eq (xsd_integer (skS.0 95 a)) False)) % 14.51/14.67 Clause #1597 (by superposition #[1596, 153]): ∀ (a a_1 : Iota), % 14.51/14.67 Or (Eq (xsd_string (skS.0 95 a)) True) % 14.51/14.67 (Or (Eq (cowlNothing (skS.0 94 a_1)) True) (Or (Eq (xsd_string (skS.0 95 a)) True) (Eq False True))) % 14.51/14.69 Clause #3432 (by clausification #[1597]): ∀ (a a_1 : Iota), % 14.51/14.69 Or (Eq (xsd_string (skS.0 95 a)) True) (Or (Eq (cowlNothing (skS.0 94 a_1)) True) (Eq (xsd_string (skS.0 95 a)) True)) % 14.51/14.69 Clause #3433 (by eliminate duplicate literals #[3432]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 95 a)) True) (Eq (cowlNothing (skS.0 94 a_1)) True) % 14.51/14.69 Clause #3436 (by superposition #[3433, 149]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 95 a)) True) (Eq True False) % 14.51/14.69 Clause #3437 (by clausification #[3436]): ∀ (a : Iota), Eq (xsd_string (skS.0 95 a)) True % 14.51/14.69 Clause #3438 (by backward demodulation #[3437, 1380]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) True)) % 14.51/14.69 Clause #3439 (by superposition #[3437, 169]): ∀ (a : Iota), Or (Eq True False) (Eq (xsd_integer (skS.0 95 a)) False) % 14.51/14.69 Clause #3440 (by clausification #[3439]): ∀ (a : Iota), Eq (xsd_integer (skS.0 95 a)) False % 14.51/14.69 Clause #3443 (by clausification #[3438]): ∀ (a a_1 : Iota), Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq (xsd_integer (skS.0 95 a_1)) True) % 14.51/14.69 Clause #3445 (by superposition #[3443, 3440]): ∀ (a : Iota), Or (Eq (cowlNothing (skS.0 94 a)) True) (Eq True False) % 14.51/14.69 Clause #3448 (by clausification #[3445]): ∀ (a : Iota), Eq (cowlNothing (skS.0 94 a)) True % 14.51/14.69 Clause #3449 (by superposition #[3448, 149]): Eq True False % 14.51/14.69 Clause #3450 (by clausification #[3449]): False % 14.51/14.69 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------