%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : LCL892+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox/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:05:11 PM UTC 2026
% Result : Unknown 0.65s 0.76s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL892+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/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 00:44:12 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.43 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.LHwKj5LFqf/theBenchmark.cnf 300
% 0.52/0.69 line 11:49 token recognition error at: '''
% 0.52/0.69 line 11:50 token recognition error at: '>'
% 0.52/0.69 line 11:51 token recognition error at: '='
% 0.52/0.69 line 11:52 token recognition error at: '''
% 0.52/0.69 line 11:53 missing LOWER_WORD at '('
% 0.52/0.69 line 11:63 token recognition error at: '''
% 0.52/0.69 line 11:64 token recognition error at: '>'
% 0.52/0.69 line 11:65 token recognition error at: '='
% 0.52/0.69 line 11:66 token recognition error at: '''
% 0.52/0.69 line 11:67 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.52/0.69 line 11:74 extraneous input ')' expecting '.'
% 0.52/0.69 line 14:60 token recognition error at: '''
% 0.52/0.69 line 14:61 token recognition error at: '='
% 0.52/0.69 line 14:62 token recognition error at: '='
% 0.52/0.69 line 14:63 token recognition error at: '>'
% 0.52/0.69 line 14:64 token recognition error at: '''
% 0.52/0.69 line 14:65 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.69 line 14:73 token recognition error at: '''
% 0.52/0.69 line 14:74 token recognition error at: '='
% 0.52/0.69 line 14:75 token recognition error at: '='
% 0.52/0.69 line 14:76 token recognition error at: '>'
% 0.52/0.69 line 14:77 token recognition error at: '''
% 0.52/0.69 line 14:72 mismatched input ',' expecting {',', ')'}
% 0.52/0.69 line 17:60 token recognition error at: '''
% 0.52/0.69 line 17:61 token recognition error at: '+'
% 0.52/0.69 line 17:62 token recognition error at: '''
% 0.52/0.69 line 17:63 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.69 line 17:71 token recognition error at: '''
% 0.52/0.69 line 17:72 token recognition error at: '+'
% 0.52/0.69 line 17:73 token recognition error at: '''
% 0.52/0.69 line 17:70 mismatched input ',' expecting {',', ')'}
% 0.52/0.69 line 20:16 token recognition error at: '''
% 0.52/0.69 line 20:17 token recognition error at: '+'
% 0.52/0.69 line 20:18 token recognition error at: '''
% 0.52/0.69 line 20:20 token recognition error at: '''
% 0.52/0.69 line 20:21 token recognition error at: '+'
% 0.52/0.69 line 20:22 token recognition error at: '''
% 0.52/0.69 line 20:19 mismatched input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.52/0.70 line 20:30 mismatched input ',' expecting {',', ')'}
% 0.52/0.70 line 20:35 token recognition error at: '''
% 0.52/0.70 line 20:36 token recognition error at: '+'
% 0.52/0.70 line 20:37 token recognition error at: '''
% 0.52/0.70 line 20:42 token recognition error at: '''
% 0.52/0.70 line 20:43 token recognition error at: '+'
% 0.52/0.70 line 20:44 token recognition error at: '''
% 0.65/0.70 line 23:16 token recognition error at: '''
% 0.65/0.70 line 23:17 token recognition error at: '+'
% 0.65/0.70 line 23:18 token recognition error at: '''
% 0.65/0.70 line 23:19 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.65/0.70 line 23:27 token recognition error at: '''
% 0.65/0.70 line 23:28 token recognition error at: '+'
% 0.65/0.70 line 23:29 token recognition error at: '''
% 0.65/0.70 line 23:26 mismatched input ',' expecting {',', ')'}
% 0.65/0.70 line 26:16 token recognition error at: '''
% 0.65/0.70 line 26:17 token recognition error at: '+'
% 0.65/0.70 line 26:18 token recognition error at: '''
% 0.65/0.70 line 26:19 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.65/0.70 line 26:23 token recognition error at: '''
% 0.65/0.70 line 26:24 token recognition error at: '0'
% 0.65/0.70 line 26:25 token recognition error at: '''
% 0.65/0.70 line 26:26 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.65/0.70 line 26:27 mismatched input ',' expecting {')', '|'}
% 0.65/0.70 line 29:4 token recognition error at: '''
% 0.65/0.70 line 29:5 token recognition error at: '>'
% 0.65/0.70 line 29:6 token recognition error at: '='
% 0.65/0.70 line 29:7 token recognition error at: '''
% 0.65/0.70 line 29:9 mismatched input 'X0' expecting {'~', LOWER_WORD}
% 0.65/0.70 line 29:15 extraneous input ')' expecting '.'
% 0.65/0.70 line 32:4 token recognition error at: '''
% 0.65/0.70 line 32:5 token recognition error at: '>'
% 0.65/0.70 line 32:6 token recognition error at: '='
% 0.65/0.70 line 32:7 token recognition error at: '''
% 0.65/0.70 line 32:9 mismatched input 'X0' expecting {'~', LOWER_WORD}
% 0.65/0.70 line 32:19 token recognition error at: '''
% 0.65/0.70 line 32:20 token recognition error at: '>'
% 0.65/0.70 line 32:21 token recognition error at: '='
% 0.65/0.70 line 32:22 token recognition error at: '''
% 0.65/0.70 line 32:23 missing LOWER_WORD at '('
% 0.65/0.70 line 32:34 token recognition error at: '''
% 0.65/0.70 line 32:35 token recognition error at: '>'
% 0.65/0.70 line 32:36 token recognition error at: '='
% 0.65/0.70 line 32:37 token recognition error at: '''
% 0.65/0.70 line 32:38 missing LOWER_WORD at '('
% 0.65/0.70 line 32:46 missing ')' at '.'
% 0.65/0.70 line 35:26 token recognition error at: '''
% 0.65/0.70 line 35:27 token recognition error at: '>'
% 0.65/0.70 line 35:28 token recognition error at: '='
% 0.65/0.70 line 35:29 token recognition error at: '''
% 0.65/0.71 line 35:30 missing LOWER_WORD at '('
% 0.65/0.71 line 35:41 token recognition error at: '''
% 0.65/0.71 line 35:42 token recognition error at: '>'
% 0.65/0.71 line 35:43 token recognition error at: '='
% 0.65/0.71 line 35:44 token recognition error at: '''
% 0.65/0.71 line 35:45 missing LOWER_WORD at '('
% 0.65/0.71 line 38:4 token recognition error at: '''
% 0.65/0.71 line 38:5 token recognition error at: '>'
% 0.65/0.71 line 38:6 token recognition error at: '='
% 0.65/0.71 line 38:7 token recognition error at: '''
% 0.65/0.71 line 38:9 token recognition error at: '''
% 0.65/0.71 line 38:10 token recognition error at: '+'
% 0.65/0.71 line 38:11 token recognition error at: '''
% 0.65/0.71 line 38:12 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.65/0.71 line 38:19 mismatched input ',' expecting '.'
% 0.65/0.71 line 38:27 token recognition error at: '''
% 0.65/0.71 line 38:28 token recognition error at: '>'
% 0.65/0.71 line 38:29 token recognition error at: '='
% 0.65/0.71 line 38:30 token recognition error at: '''
% 0.65/0.71 line 38:35 token recognition error at: '''
% 0.65/0.71 line 38:36 token recognition error at: '='
% 0.65/0.71 line 38:37 token recognition error at: '='
% 0.65/0.71 line 38:38 token recognition error at: '>'
% 0.65/0.71 line 38:39 token recognition error at: '''
% 0.65/0.71 line 41:4 token recognition error at: '''
% 0.65/0.71 line 41:5 token recognition error at: '>'
% 0.65/0.71 line 41:6 token recognition error at: '='
% 0.65/0.71 line 41:7 token recognition error at: '''
% 0.65/0.71 line 41:9 mismatched input 'X1' expecting {'~', LOWER_WORD}
% 0.65/0.71 line 41:12 token recognition error at: '''
% 0.65/0.71 line 41:13 token recognition error at: '='
% 0.65/0.71 line 41:14 token recognition error at: '='
% 0.65/0.71 line 41:15 token recognition error at: '>'
% 0.65/0.71 line 41:16 token recognition error at: '''
% 0.65/0.71 line 41:24 mismatched input ')' expecting '.'
% 0.65/0.71 line 41:29 token recognition error at: '''
% 0.65/0.71 line 41:30 token recognition error at: '>'
% 0.65/0.71 line 41:31 token recognition error at: '='
% 0.65/0.71 line 41:32 token recognition error at: '''
% 0.65/0.71 line 41:34 token recognition error at: '''
% 0.65/0.71 line 41:35 token recognition error at: '+'
% 0.65/0.71 line 41:36 token recognition error at: '''
% 0.65/0.71 line 44:4 token recognition error at: '''
% 0.65/0.71 line 44:5 token recognition error at: '>'
% 0.65/0.71 line 44:6 token recognition error at: '='
% 0.65/0.71 line 44:7 token recognition error at: '''
% 0.65/0.71 line 44:9 mismatched input 'X0' expecting {'~', LOWER_WORD}
% 0.65/0.71 line 44:12 token recognition error at: '''
% 0.65/0.71 line 44:13 token recognition error at: '0'
% 0.65/0.71 line 44:14 token recognition error at: '''
% 0.65/0.71 line 44:16 extraneous input ')' expecting '.'
% 0.65/0.71 line 47:4 token recognition error at: '''
% 0.65/0.71 line 47:5 token recognition error at: '>'
% 0.65/0.71 line 47:6 token recognition error at: '='
% 0.65/0.71 line 47:7 token recognition error at: '''
% 0.65/0.71 line 47:9 token recognition error at: '''
% 0.65/0.71 line 47:10 token recognition error at: '+'
% 0.65/0.71 line 47:11 token recognition error at: '''
% 0.65/0.71 line 47:12 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.65/0.71 line 47:20 token recognition error at: '''
% 0.65/0.71 line 47:21 token recognition error at: '+'
% 0.65/0.71 line 47:22 token recognition error at: '''
% 0.65/0.71 line 47:19 mismatched input ',' expecting '.'
% 0.65/0.71 line 47:35 token recognition error at: '''
% 0.65/0.71 line 47:36 token recognition error at: '>'
% 0.65/0.71 line 47:37 token recognition error at: '='
% 0.65/0.71 line 47:38 token recognition error at: '''
% 0.65/0.71 line 50:4 token recognition error at: '''
% 0.65/0.71 line 50:5 token recognition error at: '>'
% 0.65/0.71 line 50:6 token recognition error at: '='
% 0.65/0.72 line 50:7 token recognition error at: '''
% 0.65/0.72 line 50:9 token recognition error at: '''
% 0.65/0.72 line 50:10 token recognition error at: '='
% 0.65/0.72 line 50:11 token recognition error at: '='
% 0.65/0.72 line 50:12 token recognition error at: '>'
% 0.65/0.72 line 50:13 token recognition error at: '''
% 0.65/0.72 line 50:14 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.65/0.72 line 50:22 token recognition error at: '''
% 0.65/0.72 line 50:23 token recognition error at: '='
% 0.65/0.72 line 50:24 token recognition error at: '='
% 0.65/0.72 line 50:25 token recognition error at: '>'
% 0.65/0.72 line 50:26 token recognition error at: '''
% 0.65/0.72 line 50:21 mismatched input ',' expecting '.'
% 0.65/0.72 line 50:39 token recognition error at: '''
% 0.65/0.72 line 50:40 token recognition error at: '>'
% 0.65/0.72 line 50:41 token recognition error at: '='
% 0.65/0.72 line 50:42 token recognition error at: '''
% 0.65/0.72 line 53:4 token recognition error at: '''
% 0.65/0.72 line 53:5 token recognition error at: '>'
% 0.65/0.72 line 53:6 token recognition error at: '='
% 0.65/0.72 line 53:7 token recognition error at: '''
% 0.65/0.72 line 53:9 token recognition error at: '''
% 0.65/0.72 line 53:10 token recognition error at: '='
% 0.65/0.72 line 53:11 token recognition error at: '='
% 0.65/0.72 line 53:12 token recognition error at: '>'
% 0.65/0.72 line 53:13 token recognition error at: '''
% 0.65/0.72 line 53:14 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.65/0.72 line 53:22 token recognition error at: '''
% 0.65/0.72 line 53:23 token recognition error at: '='
% 0.65/0.72 line 53:24 token recognition error at: '='
% 0.65/0.72 line 53:25 token recognition error at: '>'
% 0.65/0.72 line 53:26 token recognition error at: '''
% 0.65/0.72 line 53:21 mismatched input ',' expecting '.'
% 0.65/0.72 line 53:39 token recognition error at: '''
% 0.65/0.72 line 53:40 token recognition error at: '>'
% 0.65/0.72 line 53:41 token recognition error at: '='
% 0.65/0.72 line 53:42 token recognition error at: '''
% 0.65/0.72 line 56:16 token recognition error at: '''
% 0.65/0.72 line 56:17 token recognition error at: '+'
% 0.65/0.72 line 56:18 token recognition error at: '''
% 0.65/0.72 line 56:19 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.65/0.72 line 56:23 token recognition error at: '''
% 0.65/0.72 line 56:24 token recognition error at: '='
% 0.65/0.72 line 56:25 token recognition error at: '='
% 0.65/0.72 line 56:26 token recognition error at: '>'
% 0.65/0.72 line 56:27 token recognition error at: '''
% 0.65/0.72 line 56:28 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.65/0.72 line 56:37 token recognition error at: '''
% 0.65/0.72 line 56:38 token recognition error at: '+'
% 0.65/0.72 line 56:39 token recognition error at: '''
% 0.65/0.72 line 56:36 mismatched input ',' expecting {',', ')'}
% 0.65/0.72 line 56:44 token recognition error at: '''
% 0.65/0.72 line 56:45 token recognition error at: '='
% 0.65/0.72 line 56:46 token recognition error at: '='
% 0.65/0.72 line 56:47 token recognition error at: '>'
% 0.65/0.72 line 56:48 token recognition error at: '''
% 0.65/0.72 line 59:16 token recognition error at: '''
% 0.65/0.72 line 59:17 token recognition error at: '1'
% 0.65/0.72 line 59:18 token recognition error at: '''
% 0.65/0.72 line 59:20 token recognition error at: '''
% 0.65/0.72 line 59:21 token recognition error at: '+'
% 0.65/0.72 line 59:22 token recognition error at: '''
% 0.65/0.72 line 59:19 mismatched input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.65/0.72 line 59:23 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.65/0.72 line 59:27 token recognition error at: '''
% 0.65/0.72 line 59:28 token recognition error at: '1'
% 0.65/0.72 line 59:29 token recognition error at: '''
% 0.65/0.72 line 59:30 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.65/0.72 line 59:32 extraneous input ')' expecting '.'
% 0.65/0.72 line 62:5 token recognition error at: '''
% 0.65/0.72 line 62:6 token recognition error at: '>'
% 0.65/0.72 line 62:7 token recognition error at: '='
% 0.65/0.72 line 62:8 token recognition error at: '''
% 0.65/0.72 line 62:9 extraneous input '(' expecting LOWER_WORD
% 0.65/0.73 line 62:13 mismatched input ',' expecting {'(', ')', '|'}
% 0.65/0.73 line 65:4 token recognition error at: '''
% 0.65/0.73 line 65:5 token recognition error at: '>'
% 0.65/0.73 line 65:6 token recognition error at: '='
% 0.65/0.73 line 65:7 token recognition error at: '''
% 0.65/0.73 line 65:9 token recognition error at: '''
% 0.65/0.73 line 65:10 token recognition error at: '='
% 0.65/0.73 line 65:11 token recognition error at: '='
% 0.65/0.73 line 65:12 token recognition error at: '>'
% 0.65/0.73 line 65:13 token recognition error at: '''
% 0.65/0.73 line 65:14 extraneous input '(' expecting {'~', LOWER_WORD}
% 0.65/0.73 line 65:18 mismatched input ',' expecting '|'
% 0.65/0.73 line 65:23 mismatched input ',' expecting {'(', '|'}
% 0.65/0.73 line 68:20 token recognition error at: '''
% 0.65/0.73 line 68:21 token recognition error at: '='
% 0.65/0.73 line 68:22 token recognition error at: '='
% 0.65/0.73 line 68:23 token recognition error at: '>'
% 0.65/0.73 line 68:24 token recognition error at: '''
% 0.65/0.73 line 68:25 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.65/0.73 line 68:35 extraneous input ')' expecting '.'
% 0.65/0.73 % SZS status Error
% 0.65/0.73 java.lang.NullPointerException: Cannot invoke "Pair.getSecond()" because "clause" is null
% 0.65/0.73 java.util.concurrent.ExecutionException: java.lang.NullPointerException: Cannot invoke "Pair.getSecond()" because "clause" is null
% 0.65/0.73 at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
% 0.65/0.73 at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:205)
% 0.65/0.73 at Main.main(Main.java:24)
% 0.65/0.73 Caused by: java.lang.NullPointerException: Cannot invoke "Pair.getSecond()" because "clause" is null
% 0.65/0.73 at Main.loadFormulas(Main.java:194)
% 0.65/0.73 at Main.runModelBuilder(Main.java:42)
% 0.65/0.73 at Main.lambda$main$0(Main.java:21)
% 0.65/0.73 at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
% 0.65/0.73 at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
% 0.65/0.73 at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
% 0.65/0.73 at java.base/java.lang.Thread.run(Thread.java:1583)
% 0.65/0.76 % FMB4L exiting
%------------------------------------------------------------------------------