%------------------------------------------------------------------------------ % File : FMB4J---0.1 % Problem : SET045-5 : TPTP v9.3.1. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n011.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:44:36 PM UTC 2026 % Result : Timeout 300.02s 287.91s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SET045-5 : TPTP v9.3.1. Released v1.0.0. % 0.00/0.03 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.08/0.35 % Computer : n011.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Thu Sep 24 09:25:42 UTC 2026 % 0.08/0.35 % CPUTime : % 0.08/0.35 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.13/0.39 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.TgiRou70mU/theBenchmark.cnf 300 % 0.41/0.61 % domain size: 1 % 0.56/0.65 % domain size: 2 % 0.56/0.66 % domain size: 3 % 0.56/0.66 % domain size: 4 % 0.56/0.67 % domain size: 5 % 0.56/0.69 % domain size: 6 % 0.79/0.70 % domain size: 7 % 0.79/0.72 % domain size: 8 % 0.79/0.73 % domain size: 9 % 0.79/0.76 % domain size: 10 % 0.79/0.79 % domain size: 11 % 1.26/0.83 % domain size: 12 % 1.26/0.88 % domain size: 13 % 1.66/0.93 % domain size: 14 % 1.66/1.00 % domain size: 15 % 2.24/1.10 % domain size: 16 % 2.87/1.28 % domain size: 17 % 4.07/1.59 % domain size: 18 % 5.28/1.89 % domain size: 19 % 6.50/2.17 % domain size: 20 % 6.91/2.45 % domain size: 21 % 7.27/2.72 % domain size: 22 % 7.64/3.12 % domain size: 23 % 8.42/3.60 % domain size: 24 % 9.29/4.23 % domain size: 25 % 10.00/4.94 % domain size: 26 % 10.74/5.67 % domain size: 27 % 11.64/6.52 % domain size: 28 % 12.54/7.50 % domain size: 29 % 13.79/8.67 % domain size: 30 % 15.32/10.16 % domain size: 31 % 16.89/11.78 % domain size: 32 % 18.71/13.57 % domain size: 33 % 20.70/15.35 % domain size: 34 % 22.20/16.41 % domain size: 35 % 23.75/17.59 % domain size: 36 % 26.38/19.52 % domain size: 37 % 29.78/22.46 % domain size: 38 % 35.17/27.33 % domain size: 39 % 38.94/30.62 % domain size: 40 % 41.88/33.57 % domain size: 41 % 44.67/36.35 % domain size: 42 % 47.92/39.51 % domain size: 43 % 51.23/42.82 % domain size: 44 % 54.24/45.87 % domain size: 45 % 58.97/50.39 % domain size: 46 % 68.18/59.58 % domain size: 47 % 79.20/70.51 % domain size: 48 % 83.72/74.82 % domain size: 49 % 88.63/79.72 % domain size: 50 % 92.96/84.11 % domain size: 51 % 98.76/89.72 % domain size: 52 % 105.48/96.35 % domain size: 53 % 115.71/106.34 % domain size: 54 % 141.39/132.03 % domain size: 55 % 149.81/140.08 % domain size: 56 % 167.20/157.48 % domain size: 57 % 180.70/170.76 % domain size: 58 % 195.84/185.35 % domain size: 59 % 205.57/195.03 % domain size: 60 % 217.77/207.05 % domain size: 61 % 236.62/225.51 % domain size: 62 % 248.03/236.90 % domain size: 63 % 256.56/245.49 % domain size: 64 % 263.72/252.38 % domain size: 65 % 277.33/265.60 % domain size: 66 % 300.02/287.91 Terminated %------------------------------------------------------------------------------