%------------------------------------------------------------------------------ % File : Equinox---6.0.1a % Problem : ALG006-1 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : tptp:short % Command : equinox --modelfile /tmp/model --no-progress --time %d --tstp %s % Computer : n023.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 : 600s % DateTime : Thu Jul 14 15:39:18 EDT 2022 % Result : Unsatisfiable 271.41s 271.07s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : ALG006-1 : TPTP v8.1.0. Released v2.2.0. % 0.00/0.12 % Command : equinox --modelfile /tmp/model --no-progress --time %d --tstp %s % 0.12/0.33 % Computer : n023.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 9 06:48:08 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 Equinox, version 6.0.1alpha, 2011-12-07, pre-release. % 0.12/0.33 +++ PROBLEM: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.33 Reading '/export/starexec/sandbox/benchmark/theBenchmark.p' ... OK % 0.12/0.33 +++ SOLVING: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.33 #elt|#instances % 0.12/0.33 (SAT)(equ)(fun)(SAT) 8| -. -. -. % 0.12/0.34 (SAT)(equ)(fun)(SAT) 8+ -1 -. -1 % 0.18/0.34 (SAT)(equ)(fun)(SAT) 10| -. -. -. % 0.18/0.34 (SAT)(equ)(fun)(SAT) 10+ -12345678 -123456789X -1 % 0.18/0.34 (SAT)(equ)(fun)(SAT) 31| -1 -. -1 % 0.18/0.36 (SAT)(equ)(fun)(SAT) 30| -. -. -. % 0.18/0.37 (SAT)(equ)(fun)(SAT) 30+ -123456789XL -123456789X -123456789XL % 0.18/0.43 (SAT)(equ)(fun)(SAT) 122| -. -. -1 % 0.61/0.85 (SAT)(equ)(fun)(SAT) 121| -. -. -. % 0.92/1.16 (SAT)(equ)(fun)(SAT) 121+ -123456789XLC> -123456789XLC> -123456789XLC> % 1.23/1.42 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 350| -123456789X -. -123456789X % 13.49/13.66 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 325| -. -12 -1 % 21.31/21.51 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 322| -. -. -. % 30.28/30.51 (SAT)(equ)(fun)(SAT) 322+ -123456789XLC> -123456789XLC> -123456789XLC> % 31.15/31.31 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 542| -123456789XL -. -123456789XL % 50.71/50.83 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 483| -123456789X -. -123456789XL % 72.71/72.78 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 444| -123456789X -. -123456789XL % 93.34/93.33 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 391| -123456789X -. -123456789XL % 112.56/112.55 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 342| -123456789X -. -123456789XL % 128.95/128.91 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 267| -123456 -. -123456789XL % 136.07/136.02 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 239| -. -. -1234567 % 144.90/144.90 (SAT)(equ)(fun)(SAT) 235| -. -. -. % 153.53/153.47 (SAT)(equ)(fun)(SAT) 235+ -123456789XLC> -123456789XLC> -123456789XLC> % 155.39/155.31 (SAT)(equ)(fun)(SAT) 378| -123456789XL -. -123456789XLC> % 170.49/170.37 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 298| -123456789X -. -123456789XL % 181.03/180.87 (SAT)(equ)(fun)(SAT) 257| -12 -. -123456789X % 199.52/199.39 (SAT)(equ)(fun)(SAT) 246| -123456789X -. -123456789 % 211.19/210.97 (SAT)(equ)(fun)(SAT) 240| -. -. -. % 219.50/219.26 (SAT)(equ)(fun)(SAT) 240+ -123456789XLC> -123456789XLC> -123456789XLC> % 221.97/221.75 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 404| -123 -123456789X -123456789XLC> % 238.11/237.83 (SAT)(equ)(fun)(SAT)(equ)(fun)(SAT) 341| -123456789 -. -123456789XL % 271.41/271.07 (SAT)(equ)(fun)(SAT)(equ)(SAT)+++ RESULT: Unsatisfiable % 271.41/271.07 SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------