%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : LCL897-10 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n019.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:05:12 PM UTC 2026
% Result : Unknown 0.52s 0.68s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL897-10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n019.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.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 00:39:50 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.42 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.G0fe4FYqOU/theBenchmark.cnf 300
% 0.40/0.63 line 13:60 token recognition error at: '''
% 0.40/0.63 line 13:62 token recognition error at: '='
% 0.52/0.63 line 13:64 token recognition error at: '='
% 0.52/0.63 line 13:65 token recognition error at: '>'
% 0.52/0.63 line 13:66 token recognition error at: '''
% 0.52/0.63 line 13:67 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.63 line 13:75 token recognition error at: '''
% 0.52/0.63 line 13:77 token recognition error at: '='
% 0.52/0.63 line 13:79 token recognition error at: '='
% 0.52/0.63 line 13:80 token recognition error at: '>'
% 0.52/0.63 line 13:81 token recognition error at: '''
% 0.52/0.63 line 13:74 mismatched input ',' expecting {',', ')'}
% 0.52/0.63 line 16:60 token recognition error at: '''
% 0.52/0.63 line 16:61 token recognition error at: '+'
% 0.52/0.63 line 16:62 token recognition error at: '''
% 0.52/0.63 line 16:63 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.63 line 16:71 token recognition error at: '''
% 0.52/0.63 line 16:72 token recognition error at: '+'
% 0.52/0.63 line 16:73 token recognition error at: '''
% 0.52/0.63 line 16:70 mismatched input ',' expecting {',', ')'}
% 0.52/0.64 line 19:16 token recognition error at: '''
% 0.52/0.64 line 19:17 token recognition error at: '+'
% 0.52/0.64 line 19:18 token recognition error at: '''
% 0.52/0.64 line 19:20 token recognition error at: '''
% 0.52/0.64 line 19:21 token recognition error at: '+'
% 0.52/0.64 line 19:22 token recognition error at: '''
% 0.52/0.64 line 19:19 mismatched input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.64 line 19:30 mismatched input ',' expecting {',', ')'}
% 0.52/0.64 line 19:35 token recognition error at: '''
% 0.52/0.64 line 19:36 token recognition error at: '+'
% 0.52/0.64 line 19:37 token recognition error at: '''
% 0.52/0.64 line 19:42 token recognition error at: '''
% 0.52/0.64 line 19:43 token recognition error at: '+'
% 0.52/0.64 line 19:44 token recognition error at: '''
% 0.52/0.64 line 22:16 token recognition error at: '''
% 0.52/0.64 line 22:17 token recognition error at: '+'
% 0.52/0.64 line 22:18 token recognition error at: '''
% 0.52/0.64 line 22:19 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.64 line 22:27 token recognition error at: '''
% 0.52/0.64 line 22:28 token recognition error at: '+'
% 0.52/0.64 line 22:29 token recognition error at: '''
% 0.52/0.64 line 22:26 mismatched input ',' expecting {',', ')'}
% 0.52/0.64 line 25:16 token recognition error at: '''
% 0.52/0.64 line 25:17 token recognition error at: '+'
% 0.52/0.64 line 25:18 token recognition error at: '''
% 0.52/0.64 line 25:19 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.64 line 25:23 token recognition error at: '''
% 0.52/0.64 line 25:24 token recognition error at: '0'
% 0.52/0.64 line 25:25 token recognition error at: '''
% 0.52/0.64 line 25:26 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.64 line 25:27 mismatched input ',' expecting {')', '|'}
% 0.52/0.64 line 28:16 token recognition error at: '''
% 0.52/0.64 line 28:17 token recognition error at: '0'
% 0.52/0.64 line 28:18 token recognition error at: '''
% 0.52/0.64 line 28:20 token recognition error at: '''
% 0.52/0.64 line 28:22 token recognition error at: '='
% 0.52/0.64 line 28:24 token recognition error at: '='
% 0.52/0.64 line 28:25 token recognition error at: '>'
% 0.52/0.64 line 28:26 token recognition error at: '''
% 0.52/0.64 line 28:19 mismatched input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.64 line 28:27 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.64 line 28:35 extraneous input ')' expecting '.'
% 0.52/0.64 line 31:16 token recognition error at: '''
% 0.52/0.64 line 31:17 token recognition error at: '0'
% 0.52/0.64 line 31:18 token recognition error at: '''
% 0.52/0.64 line 31:20 token recognition error at: '''
% 0.52/0.64 line 31:22 token recognition error at: '='
% 0.52/0.64 line 31:24 token recognition error at: '='
% 0.52/0.64 line 31:25 token recognition error at: '>'
% 0.52/0.64 line 31:26 token recognition error at: '''
% 0.52/0.64 line 31:19 mismatched input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.64 line 31:27 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.64 line 31:31 token recognition error at: '''
% 0.52/0.64 line 31:32 token recognition error at: '0'
% 0.52/0.65 line 31:33 token recognition error at: '''
% 0.52/0.65 line 31:34 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.65 line 31:36 extraneous input ')' expecting '.'
% 0.52/0.65 line 34:16 token recognition error at: '''
% 0.52/0.65 line 34:18 token recognition error at: '='
% 0.52/0.65 line 34:20 token recognition error at: '='
% 0.52/0.65 line 34:21 token recognition error at: '>'
% 0.52/0.65 line 34:22 token recognition error at: '''
% 0.52/0.65 line 34:24 token recognition error at: '''
% 0.52/0.65 line 34:25 token recognition error at: '0'
% 0.52/0.65 line 34:26 token recognition error at: '''
% 0.52/0.65 line 34:23 mismatched input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.65 line 34:31 mismatched input ',' expecting {',', ')'}
% 0.52/0.65 line 37:16 token recognition error at: '''
% 0.52/0.65 line 37:18 token recognition error at: '='
% 0.52/0.65 line 37:20 token recognition error at: '='
% 0.52/0.65 line 37:21 token recognition error at: '>'
% 0.52/0.65 line 37:22 token recognition error at: '''
% 0.52/0.65 line 37:24 token recognition error at: '''
% 0.52/0.65 line 37:25 token recognition error at: '+'
% 0.52/0.65 line 37:26 token recognition error at: '''
% 0.52/0.65 line 37:23 mismatched input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.65 line 37:34 mismatched input ',' expecting {',', ')'}
% 0.52/0.65 line 37:39 token recognition error at: '''
% 0.52/0.65 line 37:41 token recognition error at: '='
% 0.52/0.65 line 37:43 token recognition error at: '='
% 0.52/0.65 line 37:44 token recognition error at: '>'
% 0.52/0.65 line 37:45 token recognition error at: '''
% 0.52/0.65 line 37:50 token recognition error at: '''
% 0.52/0.65 line 37:52 token recognition error at: '='
% 0.52/0.65 line 37:54 token recognition error at: '='
% 0.52/0.65 line 37:55 token recognition error at: '>'
% 0.52/0.65 line 37:56 token recognition error at: '''
% 0.52/0.65 line 40:16 token recognition error at: '''
% 0.52/0.65 line 40:17 token recognition error at: '+'
% 0.52/0.65 line 40:18 token recognition error at: '''
% 0.52/0.65 line 40:19 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.65 line 40:23 token recognition error at: '''
% 0.52/0.65 line 40:25 token recognition error at: '='
% 0.52/0.65 line 40:27 token recognition error at: '='
% 0.52/0.65 line 40:28 token recognition error at: '>'
% 0.52/0.65 line 40:29 token recognition error at: '''
% 0.52/0.65 line 40:30 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.65 line 40:39 token recognition error at: '''
% 0.52/0.65 line 40:40 token recognition error at: '+'
% 0.52/0.65 line 40:41 token recognition error at: '''
% 0.52/0.65 line 40:38 mismatched input ',' expecting {',', ')'}
% 0.52/0.65 line 40:46 token recognition error at: '''
% 0.52/0.65 line 40:48 token recognition error at: '='
% 0.52/0.65 line 40:50 token recognition error at: '='
% 0.52/0.65 line 40:51 token recognition error at: '>'
% 0.52/0.65 line 40:52 token recognition error at: '''
% 0.52/0.65 line 43:17 token recognition error at: '''
% 0.52/0.65 line 43:18 token recognition error at: '+'
% 0.52/0.65 line 43:19 token recognition error at: '''
% 0.52/0.65 line 43:21 token recognition error at: '''
% 0.52/0.65 line 43:22 token recognition error at: '+'
% 0.52/0.66 line 43:23 token recognition error at: '''
% 0.52/0.66 line 43:20 mismatched input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.66 line 43:27 token recognition error at: '''
% 0.52/0.66 line 43:29 token recognition error at: '='
% 0.52/0.66 line 43:31 token recognition error at: '='
% 0.52/0.66 line 43:32 token recognition error at: '>'
% 0.52/0.66 line 43:33 token recognition error at: '''
% 0.52/0.66 line 43:34 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.66 line 43:41 token recognition error at: '''
% 0.52/0.66 line 43:43 token recognition error at: '='
% 0.52/0.66 line 43:45 token recognition error at: '='
% 0.52/0.66 line 43:46 token recognition error at: '>'
% 0.52/0.66 line 43:47 token recognition error at: '''
% 0.52/0.66 line 43:40 mismatched input ',' expecting {'(', ',', ')'}
% 0.52/0.66 line 43:49 token recognition error at: '''
% 0.52/0.66 line 43:50 token recognition error at: '+'
% 0.52/0.66 line 43:51 token recognition error at: '''
% 0.52/0.66 line 43:55 token recognition error at: '''
% 0.52/0.66 line 43:57 token recognition error at: '='
% 0.52/0.66 line 43:59 token recognition error at: '='
% 0.52/0.66 line 43:60 token recognition error at: '>'
% 0.52/0.66 line 43:61 token recognition error at: '''
% 0.52/0.66 line 43:73 token recognition error at: '''
% 0.52/0.66 line 43:74 token recognition error at: '+'
% 0.52/0.66 line 43:75 token recognition error at: '''
% 0.52/0.66 line 43:79 token recognition error at: '''
% 0.52/0.66 line 43:81 token recognition error at: '='
% 0.52/0.66 line 43:83 token recognition error at: '='
% 0.52/0.66 line 43:84 token recognition error at: '>'
% 0.52/0.66 line 43:85 token recognition error at: '''
% 0.52/0.66 line 43:89 token recognition error at: '''
% 0.52/0.66 line 43:90 token recognition error at: '+'
% 0.52/0.66 line 43:91 token recognition error at: '''
% 0.52/0.66 line 43:95 token recognition error at: '''
% 0.52/0.66 line 43:97 token recognition error at: '='
% 0.52/0.66 line 43:99 token recognition error at: '='
% 0.52/0.66 line 43:100 token recognition error at: '>'
% 0.52/0.66 line 43:101 token recognition error at: '''
% 0.52/0.66 % SZS status Error
% 0.52/0.66 java.lang.NullPointerException: Cannot invoke "Pair.getSecond()" because "clause" is null
% 0.52/0.66 java.util.concurrent.ExecutionException: java.lang.NullPointerException: Cannot invoke "Pair.getSecond()" because "clause" is null
% 0.52/0.66 at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
% 0.52/0.66 at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:205)
% 0.52/0.66 at Main.main(Main.java:24)
% 0.52/0.66 Caused by: java.lang.NullPointerException: Cannot invoke "Pair.getSecond()" because "clause" is null
% 0.52/0.66 at Main.loadFormulas(Main.java:194)
% 0.52/0.66 at Main.runModelBuilder(Main.java:42)
% 0.52/0.66 at Main.lambda$main$0(Main.java:21)
% 0.52/0.66 at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
% 0.52/0.66 at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
% 0.52/0.66 at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
% 0.52/0.66 at java.base/java.lang.Thread.run(Thread.java:1583)
% 0.52/0.68 % FMB4L exiting
%------------------------------------------------------------------------------