%------------------------------------------------------------------------------ % File : FMB4J---0.1 % Problem : SET044-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 : n004.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.01s 292.21s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SET044-5 : TPTP v9.3.1. Released v1.0.0. % 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.09/0.35 % Computer : n004.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Thu Sep 24 09:25:20 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.36 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.14/0.40 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.JVGuZA2Z5D/theBenchmark.cnf 300 % 0.49/0.69 % domain size: 1 % 0.58/0.77 % domain size: 2 % 0.58/0.78 % domain size: 3 % 0.58/0.79 % domain size: 4 % 0.77/0.80 % domain size: 5 % 0.77/0.82 % domain size: 6 % 0.77/0.84 % domain size: 7 % 0.77/0.86 % domain size: 8 % 0.77/0.89 % domain size: 9 % 1.18/0.94 % domain size: 10 % 1.18/0.99 % domain size: 11 % 1.72/1.09 % domain size: 12 % 3.20/1.48 % domain size: 13 % 6.88/2.43 % domain size: 14 % 8.37/2.91 % domain size: 15 % 9.89/3.53 % domain size: 16 % 11.19/4.52 % domain size: 17 % 12.70/5.85 % domain size: 18 % 16.11/9.27 % domain size: 19 % 16.62/9.77 % domain size: 20 % 20.23/13.33 % domain size: 21 % 26.01/19.01 % domain size: 22 % 27.61/20.53 % domain size: 23 % 28.51/21.45 % domain size: 24 % 95.39/88.14 % domain size: 25 % 96.30/89.12 % domain size: 26 % 99.38/92.08 % domain size: 27 % 101.25/94.00 % domain size: 28 % 103.49/96.17 % domain size: 29 % 162.85/155.42 % domain size: 30 % 169.67/162.26 % domain size: 31 % 181.78/174.32 % domain size: 32 % 199.39/191.93 % domain size: 33 % 201.01/193.51 % domain size: 34 % 219.02/211.51 % domain size: 35 % 222.33/214.85 % domain size: 36 % 225.57/218.04 % domain size: 37 % 229.45/222.01 % domain size: 38 % 236.09/228.49 % domain size: 39 % 243.04/235.34 % domain size: 40 % 249.24/241.50 % domain size: 41 % 261.45/253.74 % domain size: 42 % 267.58/259.83 % domain size: 43 % 300.01/292.21 Terminated %------------------------------------------------------------------------------