FMB4J---0.1.TMO-Non.f

%------------------------------------------------------------------------------
% File     : FMB4J---0.1
% Problem  : MSC012+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300

% Computer : n016.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:53 PM UTC 2026

% Result   : Timeout 300.04s 292.41s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : MSC012+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04  % Command  : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37  % Computer : n016.cluster.edu
% 0.09/0.37  % Model    : x86_64 x86_64
% 0.09/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37  % Memory   : 8046.5625MB
% 0.09/0.37  % OS       : Linux 6.8.0-71-generic
% 0.09/0.37  % CPULimit : 300
% 0.09/0.37  % WCLimit  : 300
% 0.09/0.37  % DateTime : Thu Sep 24 01:32:58 UTC 2026
% 0.09/0.37  % CPUTime  : 
% 0.09/0.37  Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.42  Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.9znOxtqJ4R/theBenchmark.cnf 300
% 0.47/0.70  % domain size: 1
% 0.59/0.77  % domain size: 2
% 0.59/0.78  % domain size: 3
% 0.59/0.79  % domain size: 4
% 0.80/0.81  % domain size: 5
% 0.80/0.84  % domain size: 6
% 0.80/0.88  % domain size: 7
% 1.24/0.98  % domain size: 8
% 1.77/1.07  % domain size: 9
% 2.18/1.16  % domain size: 10
% 2.85/1.34  % domain size: 11
% 4.01/1.66  % domain size: 12
% 5.18/1.94  % domain size: 13
% 6.04/2.35  % domain size: 14
% 7.27/2.92  % domain size: 15
% 8.06/3.36  % domain size: 16
% 9.65/4.39  % domain size: 17
% 11.24/5.31  % domain size: 18
% 12.97/6.88  % domain size: 19
% 14.38/8.30  % domain size: 20
% 18.10/12.00  % domain size: 21
% 19.08/12.84  % domain size: 22
% 20.13/13.81  % domain size: 23
% 20.83/14.46  % domain size: 24
% 21.49/15.04  % domain size: 25
% 23.37/16.84  % domain size: 26
% 25.10/18.56  % domain size: 27
% 29.07/22.49  % domain size: 28
% 30.27/23.66  % domain size: 29
% 31.42/24.74  % domain size: 30
% 32.92/26.26  % domain size: 31
% 35.24/28.53  % domain size: 32
% 37.82/31.04  % domain size: 33
% 48.00/41.30  % domain size: 34
% 52.71/45.96  % domain size: 35
% 58.61/51.85  % domain size: 36
% 62.52/55.79  % domain size: 37
% 66.29/59.47  % domain size: 38
% 71.20/64.38  % domain size: 39
% 77.31/70.43  % domain size: 40
% 83.51/76.67  % domain size: 41
% 88.91/81.97  % domain size: 42
% 94.92/88.00  % domain size: 43
% 101.42/94.47  % domain size: 44
% 114.94/107.99  % domain size: 45
% 123.54/116.59  % domain size: 46
% 132.55/125.58  % domain size: 47
% 141.77/134.76  % domain size: 48
% 155.18/148.04  % domain size: 49
% 166.91/159.79  % domain size: 50
% 182.68/175.44  % domain size: 51
% 197.70/190.47  % domain size: 52
% 210.38/203.00  % domain size: 53
% 225.78/218.30  % domain size: 54
% 244.41/236.92  % domain size: 55
% 268.02/260.57  % domain size: 56
% 300.04/292.41  Terminated
%------------------------------------------------------------------------------