%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN428-1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n019.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 : 0s % DateTime : Thu Jul 21 03:49:54 EDT 2022 % Result : Satisfiable 0.19s 0.46s % Output : Model 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.01/0.12 % Problem : SYN428-1 : TPTP v8.1.0. Released v2.1.0. % 0.12/0.13 % Command : darwin -pl 0 -pmc true -to %d %s % 0.12/0.34 % Computer : n019.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 % DateTime : Tue Jul 12 04:55:53 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.35 Defaulting to tptp format. % 0.19/0.46 SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.46 % 0.19/0.46 MODEL (CONTEXT): % 0.19/0.46 SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.46 -__-v__(=0) % 0.19/0.46 -__con304 % 0.19/0.46 -__con306 % 0.19/0.46 -__con307 % 0.19/0.46 +__con308 % 0.19/0.46 -__con311 % 0.19/0.46 -__con312 % 0.19/0.46 -__con313 % 0.19/0.46 +__con314 % 0.19/0.46 +__con315 % 0.19/0.46 +__con316 % 0.19/0.46 -__con321 % 0.19/0.46 +__con322 % 0.19/0.46 -__con326 % 0.19/0.46 +__con327 % 0.19/0.46 +__con328 % 0.19/0.46 +__con329 % 0.19/0.46 +__con331 % 0.19/0.46 -__con332 % 0.19/0.46 -__con333 % 0.19/0.46 +__con334 % 0.19/0.46 -__con335 % 0.19/0.46 -__con336 % 0.19/0.46 +__con337 % 0.19/0.46 +__con340 % 0.19/0.46 -__con348 % 0.19/0.46 +__con349 % 0.19/0.46 +__con350 % 0.19/0.46 +__con351 % 0.19/0.46 -__con352 % 0.19/0.46 -__con353 % 0.19/0.46 -__con355 % 0.19/0.46 -__con356 % 0.19/0.46 -__con357 % 0.19/0.46 +__con358 % 0.19/0.46 +__con359 % 0.19/0.46 +__con367 % 0.19/0.46 +__con368 % 0.19/0.46 +__con369 % 0.19/0.46 +__con372 % 0.19/0.46 -c10_0 % 0.19/0.46 +c10_1(a2015) % 0.19/0.46 +c10_1(a1865) % 0.19/0.46 +c10_1(a1931) % 0.19/0.46 +c10_1(a1849) % 0.19/0.46 +c10_1(a1841) % 0.19/0.46 +c10_1(a1877) % 0.19/0.46 +c10_1(a1846) % 0.19/0.46 +c10_1(a1933) % 0.19/0.46 +c10_1(a1885) % 0.19/0.46 +c10_1(a1935) % 0.19/0.46 +c10_1(a1960) % 0.19/0.46 -c10_1(a2017) % 0.19/0.46 -c10_1(a1907) % 0.19/0.46 -c10_1(a2023) % 0.19/0.46 -c10_1(a1970) % 0.19/0.46 +c10_2(a1997, a1982) % 0.19/0.46 +c10_2(a1951, a1982) % 0.19/0.46 +c10_2(a1849, a1982) % 0.19/0.46 +c10_2(a2021, a1982) % 0.19/0.46 +c10_2(a2001, a1982) % 0.19/0.46 +c10_2(a1995, a1982) % 0.19/0.46 +c10_2(a1881, a1982) % 0.19/0.46 +c10_2(a1877, a1878) % 0.19/0.46 +c10_2(a1933, a1982) % 0.19/0.46 -c10_2(a1841, a1948) % 0.19/0.46 -c10_2(a1933, a1948) % 0.19/0.46 +c1_0 % 0.19/0.46 +c1_1(a1963) % 0.19/0.46 +c1_1(a1997) % 0.19/0.46 +c1_1(a1951) % 0.19/0.46 +c1_1(a1907) % 0.19/0.46 +c1_1(a1906) % 0.19/0.46 +c1_1(a1849) % 0.19/0.46 +c1_1(a2001) % 0.19/0.46 +c1_1(a1995) % 0.19/0.46 +c1_1(a1921) % 0.19/0.46 +c1_1(a1881) % 0.19/0.46 +c1_1(a1933) % 0.19/0.46 +c1_1(a1869) % 0.19/0.46 -c1_1(a1931) % 0.19/0.46 -c1_1(a1899) % 0.19/0.46 -c1_1(a2021) % 0.19/0.46 -c1_1(a1926) % 0.19/0.46 -c1_1(a1885) % 0.19/0.46 +c1_2(a1931, a1932) % 0.19/0.46 +c1_2(a1881, a1882) % 0.19/0.46 +c1_2(a1885, =0) % 0.19/0.46 +c1_2(a1885, a2028) % 0.19/0.46 -c1_2(a1849, a1947) % 0.19/0.46 -c1_2(a1849, a1850) % 0.19/0.46 -c1_2(a1995, a1996) % 0.19/0.46 -c1_2(a1877, a1878) % 0.19/0.46 -c1_2(a1933, a1934) % 0.19/0.46 -c1_2(a1885, a1947) % 0.19/0.46 -c2_0 % 0.19/0.46 +c2_1(=0) % 0.19/0.46 +c2_1(a2017) % 0.19/0.46 +c2_1(a1963) % 0.19/0.46 +c2_1(a1997) % 0.19/0.46 +c2_1(a1951) % 0.19/0.46 +c2_1(a1907) % 0.19/0.46 +c2_1(a1906) % 0.19/0.46 +c2_1(a2001) % 0.19/0.46 +c2_1(a1995) % 0.19/0.46 +c2_1(a1921) % 0.19/0.46 +c2_1(a1881) % 0.19/0.46 +c2_1(a1933) % 0.19/0.46 +c2_1(a1926) % 0.19/0.46 +c2_1(a1869) % 0.19/0.46 -c2_1(a1885) % 0.19/0.46 +c2_2(a2015, a1947) % 0.19/0.46 +c2_2(a1865, a1868) % 0.19/0.46 +c2_2(a1865, a1947) % 0.19/0.46 +c2_2(a1931, a1947) % 0.19/0.46 +c2_2(a1849, a1947) % 0.19/0.46 +c2_2(a1841, a1842) % 0.19/0.46 +c2_2(a1877, a1947) % 0.19/0.46 +c2_2(a1846, a1947) % 0.19/0.46 +c2_2(a1885, a1947) % 0.19/0.46 +c2_2(a1885, a2028) % 0.19/0.46 +c2_2(a1935, a1947) % 0.19/0.46 +c2_2(a1960, a1947) % 0.19/0.46 -c2_2(a1986, a1987) % 0.19/0.46 -c2_2(a1841, a1948) % 0.19/0.46 -c2_2(a2001, a2002) % 0.19/0.46 -c2_2(a1877, a1878) % 0.19/0.46 -c2_2(a1933, _0) % 0.19/0.46 +c3_0 % 0.19/0.46 +c3_1(=0) % 0.19/0.46 +c3_1(a2017) % 0.19/0.46 +c3_1(a1912) % 0.19/0.46 +c3_1(a1970) % 0.19/0.46 +c3_1(a1885) % 0.19/0.46 -c3_1(a1997) % 0.19/0.46 -c3_1(a1951) % 0.19/0.46 -c3_1(a1849) % 0.19/0.46 -c3_1(a2021) % 0.19/0.46 -c3_1(a2001) % 0.19/0.46 -c3_1(a1995) % 0.19/0.46 -c3_1(a1881) % 0.19/0.46 -c3_1(a1933) % 0.19/0.46 +c3_2(a1865, a1867) % 0.19/0.46 -c3_2(a1849, a1850) % 0.19/0.46 -c3_2(a1885, a2028) % 0.19/0.46 +c4_0 % 0.19/0.46 +c4_1(a1963) % 0.19/0.46 +c4_1(a1997) % 0.19/0.46 +c4_1(a1951) % 0.19/0.46 +c4_1(a1907) % 0.19/0.46 +c4_1(a1906) % 0.19/0.46 +c4_1(a1849) % 0.19/0.46 +c4_1(a2021) % 0.19/0.46 +c4_1(a2001) % 0.19/0.46 +c4_1(a1995) % 0.19/0.46 +c4_1(a1921) % 0.19/0.46 +c4_1(a1881) % 0.19/0.46 +c4_1(a1933) % 0.19/0.46 +c4_1(a1926) % 0.19/0.46 +c4_1(a1869) % 0.19/0.46 -c4_1(a1857) % 0.19/0.46 +c4_2(a1841, a1842) % 0.19/0.46 +c4_2(a2021, a1883) % 0.19/0.46 +c4_2(a1926, a1883) % 0.19/0.46 +c4_2(a1885, a2028) % 0.19/0.46 -c4_2(a1865, a1866) % 0.19/0.46 -c4_2(a1881, a1882) % 0.19/0.46 -c4_2(a1885, a1947) % 0.19/0.46 +c5_0 % 0.19/0.46 +c5_1(a1963) % 0.19/0.46 +c5_1(a1997) % 0.19/0.46 +c5_1(a1951) % 0.19/0.46 +c5_1(a1907) % 0.19/0.46 +c5_1(a1849) % 0.19/0.46 +c5_1(a2021) % 0.19/0.46 +c5_1(a2001) % 0.19/0.46 +c5_1(a1995) % 0.19/0.46 +c5_1(a1921) % 0.19/0.46 +c5_1(a1881) % 0.19/0.46 +c5_1(a1933) % 0.19/0.46 +c5_1(a1926) % 0.19/0.46 -c5_1(a1912) % 0.19/0.46 -c5_1(a1970) % 0.19/0.46 +c5_2(a1997, a1982) % 0.19/0.46 +c5_2(a1951, a1982) % 0.19/0.46 +c5_2(a1849, a1850) % 0.19/0.46 +c5_2(a1849, a1982) % 0.19/0.46 +c5_2(a2021, a1982) % 0.19/0.46 +c5_2(a2001, a2002) % 0.19/0.46 +c5_2(a2001, a1982) % 0.19/0.46 +c5_2(a1995, a1996) % 0.19/0.46 +c5_2(a1995, a1982) % 0.19/0.46 +c5_2(a1881, a1982) % 0.19/0.46 +c5_2(a1846, =0) % 0.19/0.46 +c5_2(a1846, a1847) % 0.19/0.46 +c5_2(a1933, a1934) % 0.19/0.46 +c5_2(a1933, a1982) % 0.19/0.46 +c5_2(a1935, a1936) % 0.19/0.46 -c5_2(a1865, a1867) % 0.19/0.46 -c5_2(a1986, a1987) % 0.19/0.46 -c6_0 % 0.19/0.46 +c6_1(a1849) % 0.19/0.46 +c6_1(a1885) % 0.19/0.46 -c6_1(a1931) % 0.19/0.46 -c6_1(a1921) % 0.19/0.46 -c6_1(a1926) % 0.19/0.46 +c6_2(a2021, a1883) % 0.19/0.46 +c6_2(a1926, a1883) % 0.19/0.46 -c6_2(a1865, a1868) % 0.19/0.46 -c6_2(a1849, a1940) % 0.19/0.46 -c6_2(a1841, a1948) % 0.19/0.46 -c6_2(a1995, a1996) % 0.19/0.46 -c6_2(a1933, a1948) % 0.19/0.46 +c7_0 % 0.19/0.46 +c7_1(a1970) % 0.19/0.46 -c7_1(a1986) % 0.19/0.46 -c7_1(a1975) % 0.19/0.46 +c7_2(a2015, a1947) % 0.19/0.46 +c7_2(a1865, a1947) % 0.19/0.46 +c7_2(a1986, a1987) % 0.19/0.46 +c7_2(a1931, a1947) % 0.19/0.46 +c7_2(a1931, a1932) % 0.19/0.46 +c7_2(a1849, a1947) % 0.19/0.46 +c7_2(a1849, a1850) % 0.19/0.46 +c7_2(a1841, a1948) % 0.19/0.46 +c7_2(a1877, a1947) % 0.19/0.46 +c7_2(a1846, a1947) % 0.19/0.46 +c7_2(a1846, a1847) % 0.19/0.46 +c7_2(a1933, a1948) % 0.19/0.46 +c7_2(a1885, a1947) % 0.19/0.46 +c7_2(a1935, a1947) % 0.19/0.46 +c7_2(a1960, a1947) % 0.19/0.46 -c7_2(a1865, a1868) % 0.19/0.46 -c7_2(a1865, a1866) % 0.19/0.46 -c7_2(a1841, a1842) % 0.19/0.46 -c7_2(a1885, a2028) % 0.19/0.46 -c8_0 % 0.19/0.46 +c8_1(a2017) % 0.19/0.46 +c8_1(a1997) % 0.19/0.46 +c8_1(a1907) % 0.19/0.46 +c8_1(a1849) % 0.19/0.46 +c8_1(a1921) % 0.19/0.46 -c8_1(a1931) % 0.19/0.46 -c8_1(a2023) % 0.19/0.46 -c8_1(a2021) % 0.19/0.46 -c8_1(a1933) % 0.19/0.46 -c8_1(a1885) % 0.19/0.46 +c8_2(a1865, a1866) % 0.19/0.46 +c8_2(a1849, a1940) % 0.19/0.46 +c8_2(a1846, a1847) % 0.19/0.46 +c8_2(a1933, a1934) % 0.19/0.46 -c8_2(a2015, a2016) % 0.19/0.46 -c8_2(a1881, a1882) % 0.19/0.46 -c8_2(a1885, a2028) % 0.19/0.46 -c8_2(a1935, a1936) % 0.19/0.46 -c9_0 % 0.19/0.46 +c9_1(a1846) % 0.19/0.46 +c9_1(a1869) % 0.19/0.46 -c9_1(a1986) % 0.19/0.46 -c9_1(a1899) % 0.19/0.46 -c9_1(a1881) % 0.19/0.46 -c9_1(a1935) % 0.19/0.46 +c9_2(a2015, a1947) % 0.19/0.46 +c9_2(a1865, a1947) % 0.19/0.46 +c9_2(a1931, a1947) % 0.19/0.46 +c9_2(a1849, a1947) % 0.19/0.46 +c9_2(a2021, a1883) % 0.19/0.46 +c9_2(a2001, a2002) % 0.19/0.46 +c9_2(a1877, a1947) % 0.19/0.46 +c9_2(a1846, a1947) % 0.19/0.46 +c9_2(a1926, a1883) % 0.19/0.46 +c9_2(a1885, a1947) % 0.19/0.46 +c9_2(a1935, a1947) % 0.19/0.46 +c9_2(a1960, a1947) % 0.19/0.46 -c9_2(a2015, a2016) % 0.19/0.46 -c9_2(a1865, a1867) % 0.19/0.46 -c9_2(a1997, a1982) % 0.19/0.46 -c9_2(a1951, a1982) % 0.19/0.46 -c9_2(a1931, a1932) % 0.19/0.46 -c9_2(a1849, a1982) % 0.19/0.46 -c9_2(a2021, a1982) % 0.19/0.46 -c9_2(a2001, a1982) % 0.19/0.46 -c9_2(a1995, a1982) % 0.19/0.46 -c9_2(a1881, a1982) % 0.19/0.46 -c9_2(a1933, a1982) % 0.19/0.46 +ndr1_0 % 0.19/0.46 +ndr1_1(=0) % 0.19/0.46 +ndr1_1(a2015) % 0.19/0.46 +ndr1_1(a1865) % 0.19/0.46 +ndr1_1(a1997) % 0.19/0.46 +ndr1_1(a1986) % 0.19/0.46 +ndr1_1(a1951) % 0.19/0.46 +ndr1_1(a1931) % 0.19/0.46 +ndr1_1(a1849) % 0.19/0.46 +ndr1_1(a1841) % 0.19/0.46 +ndr1_1(a2021) % 0.19/0.46 +ndr1_1(a2001) % 0.19/0.46 +ndr1_1(a1995) % 0.19/0.46 +ndr1_1(a1881) % 0.19/0.46 +ndr1_1(a1877) % 0.19/0.46 +ndr1_1(a1846) % 0.19/0.46 +ndr1_1(a1933) % 0.19/0.46 +ndr1_1(a1926) % 0.19/0.46 +ndr1_1(a1885) % 0.19/0.46 +ndr1_1(a1935) % 0.19/0.46 +ndr1_1(a1960) % 0.19/0.46 -ndr1_1(a2017) % 0.19/0.46 +ssSkC0 % 0.19/0.46 +ssSkC1 % 0.19/0.46 +ssSkC11 % 0.19/0.46 +ssSkC12 % 0.19/0.46 +ssSkC13 % 0.19/0.46 +ssSkC14 % 0.19/0.46 +ssSkC15 % 0.19/0.46 +ssSkC16 % 0.19/0.46 +ssSkC17 % 0.19/0.46 +ssSkC18 % 0.19/0.46 +ssSkC2 % 0.19/0.46 +ssSkC20 % 0.19/0.46 +ssSkC21 % 0.19/0.46 +ssSkC22 % 0.19/0.46 +ssSkC23 % 0.19/0.46 +ssSkC24 % 0.19/0.46 +ssSkC25 % 0.19/0.46 +ssSkC26 % 0.19/0.46 -ssSkC27 % 0.19/0.46 +ssSkC28 % 0.19/0.46 +ssSkC29 % 0.19/0.46 +ssSkC3 % 0.19/0.46 +ssSkC30 % 0.19/0.46 +ssSkC31 % 0.19/0.46 +ssSkC32 % 0.19/0.46 +ssSkC33 % 0.19/0.46 +ssSkC34 % 0.19/0.46 +ssSkC35 % 0.19/0.46 +ssSkC36 % 0.19/0.46 +ssSkC37 % 0.19/0.46 +ssSkC39 % 0.19/0.46 +ssSkC4 % 0.19/0.46 +ssSkC40 % 0.19/0.46 +ssSkC41 % 0.19/0.46 +ssSkC42 % 0.19/0.46 +ssSkC5 % 0.19/0.46 +ssSkC6 % 0.19/0.46 +ssSkC7 % 0.19/0.46 +ssSkC8 % 0.19/0.46 +ssSkC9 % 0.19/0.46 +ssSkP0(=0) % 0.19/0.46 +ssSkP0(a2017) % 0.19/0.46 +ssSkP1(=0) % 0.19/0.46 +ssSkP1(a2017) % 0.19/0.46 +ssSkP10(=0) % 0.19/0.46 +ssSkP10(a2017) % 0.19/0.46 +ssSkP11(=0) % 0.19/0.46 +ssSkP11(a2017) % 0.19/0.46 +ssSkP12(=0) % 0.19/0.46 +ssSkP12(a2017) % 0.19/0.46 +ssSkP13(=0) % 0.19/0.46 +ssSkP13(a2017) % 0.19/0.46 +ssSkP14(=0) % 0.19/0.46 +ssSkP14(a2017) % 0.19/0.46 +ssSkP15(=0) % 0.19/0.46 +ssSkP15(a2017) % 0.19/0.46 +ssSkP16(=0) % 0.19/0.46 +ssSkP16(a2017) % 0.19/0.46 +ssSkP2(=0) % 0.19/0.46 +ssSkP2(a2017) % 0.19/0.46 +ssSkP3(=0) % 0.19/0.46 +ssSkP3(a2017) % 0.19/0.46 +ssSkP4(=0) % 0.19/0.46 +ssSkP4(a2017) % 0.19/0.46 +ssSkP5(=0) % 0.19/0.46 +ssSkP5(a2017) % 0.19/0.46 +ssSkP6(a2017) % 0.19/0.46 +ssSkP6(a1846) % 0.19/0.46 +ssSkP7(=0) % 0.19/0.46 +ssSkP7(a2017) % 0.19/0.46 +ssSkP8(=0) % 0.19/0.46 +ssSkP8(a2017) % 0.19/0.46 +ssSkP8(a1841) % 0.19/0.46 +ssSkP8(a1933) % 0.19/0.46 -ssSkP8(a2015) % 0.19/0.46 -ssSkP8(a1865) % 0.19/0.46 -ssSkP8(a1931) % 0.19/0.46 -ssSkP8(a1849) % 0.19/0.46 -ssSkP8(a1877) % 0.19/0.46 -ssSkP8(a1846) % 0.19/0.46 -ssSkP8(a1885) % 0.19/0.46 -ssSkP8(a1935) % 0.19/0.46 -ssSkP8(a1960) % 0.19/0.46 +ssSkP9(=0) % 0.19/0.46 +ssSkP9(a2017) % 0.19/0.46 SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------