%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN870-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n004.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:53:27 EDT 2022 % Result : Satisfiable 0.12s 0.37s % Output : Model 0.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN870-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.12 % Command : darwin -pl 0 -pmc true -to %d %s % 0.12/0.34 % Computer : n004.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 08:22:37 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 Defaulting to tptp format. % 0.12/0.37 SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.37 % 0.12/0.37 MODEL (CONTEXT): % 0.12/0.37 SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.37 -__-v__(=0) % 0.12/0.37 +ssNder1_0 % 0.12/0.37 +ssNder1_10r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9) % 0.12/0.37 +ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10) % 0.12/0.37 +ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11) % 0.12/0.37 +ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12) % 0.12/0.37 +ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13) % 0.12/0.37 +ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14) % 0.12/0.37 +ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15) % 0.12/0.37 +ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16) % 0.12/0.37 +ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17) % 0.12/0.37 +ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % 0.12/0.37 +ssNder1_1r1(_0) % 0.12/0.37 +ssNder1_2r1r1(_0, _1) % 0.12/0.37 +ssNder1_3r1r1r1(_0, _1, _2) % 0.12/0.37 +ssNder1_4r1r1r1r1(_0, _1, _2, _3) % 0.12/0.37 +ssNder1_5r1r1r1r1r1(_0, _1, _2, _3, _4) % 0.12/0.37 +ssNder1_6r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5) % 0.12/0.37 +ssNder1_7r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6) % 0.12/0.37 +ssNder1_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7) % 0.12/0.37 +ssNder1_9r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8) % 0.12/0.37 -ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(=0, =1, =2, =3, =4, =5, =6, skc25, =7, =8, __sko90) % 0.12/0.37 -ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(=0, =1, =2, =3, =4, =5, skc26, =6, =7, =8, __sko113) % 0.12/0.37 -ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(=0, =1, =2, =3, =4, skc28, =5, =6, =7, =8, __sko136) % 0.12/0.37 +ssPv11_10r1r1r1r1r1r1r1r1r1r1(=0, =1, =2, =3, =4, =5, =6, skc25, =7, =8) % 0.12/0.37 +ssPv11_10r1r1r1r1r1r1r1r1r1r1(=0, =1, =2, =3, =4, =5, skc26, =6, =7, =8) % 0.12/0.37 +ssPv11_10r1r1r1r1r1r1r1r1r1r1(=0, =1, =2, =3, =4, skc28, =5, =6, =7, =8) % 0.12/0.37 +ssPv12_9r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8) % 0.12/0.37 +ssPv13_8r1r1r1r1r1r1r1r1(=0, =1, =2, =3, =4, =5, =6, =7) % 0.12/0.37 +ssPv13_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc24) % 0.12/0.37 -ssPv13_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc25) % 0.12/0.37 +ssPv14_7r1r1r1r1r1r1r1(=0, =1, =2, =3, =4, skc28, =5) % 0.12/0.37 +ssPv14_7r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc26) % 0.12/0.37 -ssPv14_7r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc27) % 0.12/0.37 +ssPv15_6r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc28) % 0.12/0.37 -ssPv15_6r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc29) % 0.12/0.37 +ssPv16_5r1r1r1r1r1(_0, _1, _2, _3, skc30) % 0.12/0.37 -ssPv16_5r1r1r1r1r1(_0, _1, _2, _3, skc31) % 0.12/0.37 +ssPv17_4r1r1r1r1(=0, =1, =2, =3) % 0.12/0.37 -ssPv18_3r1r1r1(_0, _1, _2) % 0.12/0.37 +ssPv20_1r1(=0) % 0.12/0.37 +ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(=0, =1, =2, =3, =4, skc28, skc27, =5, =6, =7, =8, =9, =10, =11, =12, =13, =14, _15, _16) % 0.12/0.37 +ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, skc16) % 0.12/0.37 -ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, skc17) % 0.12/0.37 +ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, skc18) % 0.12/0.37 -ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, skc19) % 0.12/0.37 +ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, skc20) % 0.12/0.37 -ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, skc21) % 0.12/0.37 +ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, skc22) % 0.12/0.37 -ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, skc23) % 0.12/0.37 SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------