%------------------------------------------------------------------------------ % File : FMB4J---0.1 % Problem : MSC019+1 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Sep 25 02:13:54 PM UTC 2026 % Result : Timeout 300.06s 260.16s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : MSC019+1 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.06 % Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.16/0.43 % Computer : n009.cluster.edu % 0.16/0.43 % Model : x86_64 x86_64 % 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.43 % Memory : 8046.5625MB % 0.16/0.43 % OS : Linux 6.8.0-71-generic % 0.16/0.43 % CPULimit : 300 % 0.16/0.43 % WCLimit : 300 % 0.16/0.43 % DateTime : Thu Sep 24 01:31:28 UTC 2026 % 0.16/0.43 % CPUTime : % 0.16/0.43 Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.26/0.53 Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.b0wTQOG37n/theBenchmark.cnf 300 % 1.15/0.92 % domain size: 1 % 1.70/1.04 % domain size: 2 % 1.70/1.09 % domain size: 3 % 2.15/1.17 % domain size: 4 % 2.43/1.29 % domain size: 5 % 3.26/1.47 % domain size: 6 % 4.50/1.76 % domain size: 7 % 6.35/2.17 % domain size: 8 % 9.37/2.92 % domain size: 9 % 13.38/3.99 % domain size: 10 % 15.63/4.55 % domain size: 11 % 16.74/5.23 % domain size: 12 % 17.63/5.90 % domain size: 13 % 18.56/6.56 % domain size: 14 % 20.35/7.55 % domain size: 15 % 21.94/9.06 % domain size: 16 % 24.78/10.98 % domain size: 17 % 26.51/12.60 % domain size: 18 % 29.24/14.95 % domain size: 19 % 32.49/17.43 % domain size: 20 % 35.98/19.95 % domain size: 21 % 38.69/22.62 % domain size: 22 % 42.02/25.67 % domain size: 23 % 44.46/27.80 % domain size: 24 % 47.27/30.67 % domain size: 25 % 51.66/34.78 % domain size: 26 % 56.58/39.56 % domain size: 27 % 60.87/43.28 % domain size: 28 % 65.27/47.49 % domain size: 29 % 70.07/52.24 % domain size: 30 % 75.88/57.90 % domain size: 31 % 82.30/63.67 % domain size: 32 % 89.26/70.55 % domain size: 33 % 96.90/78.04 % domain size: 34 % 106.12/86.62 % domain size: 35 % 117.04/96.80 % domain size: 36 % 128.81/107.93 % domain size: 37 % 144.07/121.15 % domain size: 38 % 160.11/135.15 % domain size: 39 % 177.53/150.75 % domain size: 40 % 196.04/167.51 % domain size: 41 % 219.18/188.15 % domain size: 42 % 242.19/209.28 % domain size: 43 % 274.82/239.34 % domain size: 44 % 300.06/260.16 Terminated %------------------------------------------------------------------------------