%------------------------------------------------------------------------------ % File : FMB4J---0.1 % Problem : LAT267-2 : TPTP v9.3.1. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_fmb4j /export/starexec/sandbox/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 01:57:32 PM UTC 2026 % Result : Timeout 289.08s 281.51s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LAT267-2 : TPTP v9.3.1. Released v3.2.0. % 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.10/0.36 % Computer : n009.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Wed Sep 23 20:44:58 UTC 2026 % 0.10/0.36 % CPUTime : % 0.10/0.36 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.10/0.40 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.4PVVafoyHx/theBenchmark.cnf 300 % 0.52/0.70 % domain size: 1 % 0.82/0.81 % domain size: 2 % 0.82/0.82 % domain size: 3 % 0.82/0.84 % domain size: 4 % 0.82/0.87 % domain size: 5 % 1.11/0.90 % domain size: 6 % 1.11/0.94 % domain size: 7 % 1.11/1.00 % domain size: 8 % 1.69/1.08 % domain size: 9 % 2.13/1.17 % domain size: 10 % 2.75/1.31 % domain size: 11 % 3.15/1.49 % domain size: 12 % 3.95/1.66 % domain size: 13 % 4.76/1.82 % domain size: 14 % 5.17/2.03 % domain size: 15 % 6.53/2.35 % domain size: 16 % 6.89/2.66 % domain size: 17 % 7.43/3.09 % domain size: 18 % 8.34/3.61 % domain size: 19 % 9.78/4.31 % domain size: 20 % 11.22/5.14 % domain size: 21 % 12.24/6.15 % domain size: 22 % 13.47/7.34 % domain size: 23 % 15.45/8.83 % domain size: 24 % 17.30/10.67 % domain size: 25 % 19.62/12.92 % domain size: 26 % 22.40/15.62 % domain size: 27 % 25.46/18.52 % domain size: 28 % 29.37/22.44 % domain size: 29 % 34.00/27.03 % domain size: 30 % 40.59/33.63 % domain size: 31 % 46.97/39.96 % domain size: 32 % 55.51/48.44 % domain size: 33 % 62.24/55.17 % domain size: 34 % 69.53/62.49 % domain size: 35 % 83.45/76.31 % domain size: 36 % 95.76/88.65 % domain size: 37 % 107.48/100.34 % domain size: 38 % 123.29/116.02 % domain size: 39 % 142.55/135.16 % domain size: 40 % 164.24/156.87 % domain size: 41 % 189.05/181.69 % domain size: 42 % 217.38/209.98 % domain size: 43 % 250.72/243.26 % domain size: 44 % 289.08/281.51 % domain size: 45 % 300.08/292.51 Terminated %------------------------------------------------------------------------------