%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : LCL893+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 : 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:05:11 PM UTC 2026
% Result : Unknown 0.51s 0.68s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL893+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 : n004.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:39:07 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.QY1TLzqZek/theBenchmark.cnf 300
% 0.40/0.62 line 11:49 token recognition error at: '''
% 0.40/0.62 line 11:50 token recognition error at: '>'
% 0.40/0.62 line 11:51 token recognition error at: '='
% 0.40/0.62 line 11:52 token recognition error at: '''
% 0.40/0.62 line 11:53 missing LOWER_WORD at '('
% 0.40/0.62 line 11:63 token recognition error at: '''
% 0.40/0.62 line 11:64 token recognition error at: '>'
% 0.40/0.62 line 11:65 token recognition error at: '='
% 0.40/0.62 line 11:66 token recognition error at: '''
% 0.40/0.62 line 11:67 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.40/0.62 line 11:74 extraneous input ')' expecting '.'
% 0.40/0.63 line 17:60 token recognition error at: '''
% 0.40/0.63 line 17:61 token recognition error at: '='
% 0.40/0.63 line 17:62 token recognition error at: '='
% 0.40/0.63 line 17:63 token recognition error at: '>'
% 0.40/0.63 line 17:64 token recognition error at: '''
% 0.40/0.63 line 17:65 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.40/0.63 line 17:73 token recognition error at: '''
% 0.40/0.63 line 17:74 token recognition error at: '='
% 0.40/0.63 line 17:75 token recognition error at: '='
% 0.40/0.63 line 17:76 token recognition error at: '>'
% 0.40/0.63 line 17:77 token recognition error at: '''
% 0.40/0.63 line 17:72 mismatched input ',' expecting {',', ')'}
% 0.40/0.63 line 20:60 token recognition error at: '''
% 0.40/0.63 line 20:61 token recognition error at: '+'
% 0.40/0.63 line 20:62 token recognition error at: '''
% 0.40/0.63 line 20:63 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.40/0.63 line 20:71 token recognition error at: '''
% 0.40/0.63 line 20:72 token recognition error at: '+'
% 0.40/0.63 line 20:73 token recognition error at: '''
% 0.40/0.63 line 20:70 mismatched input ',' expecting {',', ')'}
% 0.40/0.63 line 23:16 token recognition error at: '''
% 0.40/0.63 line 23:17 token recognition error at: '+'
% 0.40/0.63 line 23:18 token recognition error at: '''
% 0.40/0.63 line 23:20 token recognition error at: '''
% 0.40/0.63 line 23:21 token recognition error at: '+'
% 0.40/0.63 line 23:22 token recognition error at: '''
% 0.40/0.63 line 23:19 mismatched input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.40/0.63 line 23:30 mismatched input ',' expecting {',', ')'}
% 0.40/0.63 line 23:35 token recognition error at: '''
% 0.40/0.63 line 23:36 token recognition error at: '+'
% 0.40/0.63 line 23:37 token recognition error at: '''
% 0.40/0.63 line 23:42 token recognition error at: '''
% 0.40/0.63 line 23:43 token recognition error at: '+'
% 0.40/0.63 line 23:44 token recognition error at: '''
% 0.51/0.63 line 26:16 token recognition error at: '''
% 0.51/0.63 line 26:17 token recognition error at: '+'
% 0.51/0.63 line 26:18 token recognition error at: '''
% 0.51/0.63 line 26:19 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.51/0.63 line 26:27 token recognition error at: '''
% 0.51/0.63 line 26:28 token recognition error at: '+'
% 0.51/0.63 line 26:29 token recognition error at: '''
% 0.51/0.63 line 26:26 mismatched input ',' expecting {',', ')'}
% 0.51/0.63 line 29:16 token recognition error at: '''
% 0.51/0.63 line 29:17 token recognition error at: '+'
% 0.51/0.63 line 29:18 token recognition error at: '''
% 0.51/0.63 line 29:19 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.51/0.63 line 29:23 token recognition error at: '''
% 0.51/0.63 line 29:24 token recognition error at: '0'
% 0.51/0.63 line 29:25 token recognition error at: '''
% 0.51/0.63 line 29:26 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.51/0.63 line 29:27 mismatched input ',' expecting {')', '|'}
% 0.51/0.63 line 32:16 token recognition error at: '''
% 0.51/0.63 line 32:17 token recognition error at: '1'
% 0.51/0.63 line 32:18 token recognition error at: '''
% 0.51/0.63 line 32:20 token recognition error at: '''
% 0.51/0.63 line 32:21 token recognition error at: '+'
% 0.51/0.63 line 32:22 token recognition error at: '''
% 0.51/0.63 line 32:19 mismatched input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.51/0.63 line 32:23 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.51/0.63 line 32:27 token recognition error at: '''
% 0.51/0.63 line 32:28 token recognition error at: '1'
% 0.51/0.63 line 32:29 token recognition error at: '''
% 0.51/0.63 line 32:30 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.51/0.63 line 32:32 extraneous input ')' expecting '.'
% 0.51/0.63 line 35:4 token recognition error at: '''
% 0.51/0.63 line 35:5 token recognition error at: '>'
% 0.51/0.63 line 35:6 token recognition error at: '='
% 0.51/0.63 line 35:7 token recognition error at: '''
% 0.51/0.63 line 35:9 mismatched input 'X0' expecting {'~', LOWER_WORD}
% 0.51/0.63 line 35:15 extraneous input ')' expecting '.'
% 0.51/0.63 line 38:4 token recognition error at: '''
% 0.51/0.63 line 38:5 token recognition error at: '>'
% 0.51/0.63 line 38:6 token recognition error at: '='
% 0.51/0.63 line 38:7 token recognition error at: '''
% 0.51/0.63 line 38:9 mismatched input 'X0' expecting {'~', LOWER_WORD}
% 0.51/0.63 line 38:19 token recognition error at: '''
% 0.51/0.63 line 38:20 token recognition error at: '>'
% 0.51/0.63 line 38:21 token recognition error at: '='
% 0.51/0.63 line 38:22 token recognition error at: '''
% 0.51/0.63 line 38:23 missing LOWER_WORD at '('
% 0.51/0.63 line 38:34 token recognition error at: '''
% 0.51/0.63 line 38:35 token recognition error at: '>'
% 0.51/0.63 line 38:36 token recognition error at: '='
% 0.51/0.63 line 38:37 token recognition error at: '''
% 0.51/0.63 line 38:38 missing LOWER_WORD at '('
% 0.51/0.63 line 38:46 missing ')' at '.'
% 0.51/0.63 line 41:26 token recognition error at: '''
% 0.51/0.63 line 41:27 token recognition error at: '>'
% 0.51/0.63 line 41:28 token recognition error at: '='
% 0.51/0.63 line 41:29 token recognition error at: '''
% 0.51/0.64 line 41:30 missing LOWER_WORD at '('
% 0.51/0.64 line 41:41 token recognition error at: '''
% 0.51/0.64 line 41:42 token recognition error at: '>'
% 0.51/0.64 line 41:43 token recognition error at: '='
% 0.51/0.64 line 41:44 token recognition error at: '''
% 0.51/0.64 line 41:45 missing LOWER_WORD at '('
% 0.51/0.64 line 44:4 token recognition error at: '''
% 0.51/0.64 line 44:5 token recognition error at: '>'
% 0.51/0.64 line 44:6 token recognition error at: '='
% 0.51/0.64 line 44:7 token recognition error at: '''
% 0.51/0.64 line 44:9 token recognition error at: '''
% 0.51/0.64 line 44:10 token recognition error at: '+'
% 0.51/0.64 line 44:11 token recognition error at: '''
% 0.51/0.64 line 44:12 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.51/0.64 line 44:19 mismatched input ',' expecting '.'
% 0.51/0.64 line 44:27 token recognition error at: '''
% 0.51/0.64 line 44:28 token recognition error at: '>'
% 0.51/0.64 line 44:29 token recognition error at: '='
% 0.51/0.64 line 44:30 token recognition error at: '''
% 0.51/0.64 line 44:35 token recognition error at: '''
% 0.51/0.64 line 44:36 token recognition error at: '='
% 0.51/0.64 line 44:37 token recognition error at: '='
% 0.51/0.64 line 44:38 token recognition error at: '>'
% 0.51/0.64 line 44:39 token recognition error at: '''
% 0.51/0.64 line 47:4 token recognition error at: '''
% 0.51/0.64 line 47:5 token recognition error at: '>'
% 0.51/0.64 line 47:6 token recognition error at: '='
% 0.51/0.64 line 47:7 token recognition error at: '''
% 0.51/0.64 line 47:9 mismatched input 'X1' expecting {'~', LOWER_WORD}
% 0.51/0.64 line 47:12 token recognition error at: '''
% 0.51/0.64 line 47:13 token recognition error at: '='
% 0.51/0.64 line 47:14 token recognition error at: '='
% 0.51/0.64 line 47:15 token recognition error at: '>'
% 0.51/0.64 line 47:16 token recognition error at: '''
% 0.51/0.64 line 47:24 mismatched input ')' expecting '.'
% 0.51/0.64 line 47:29 token recognition error at: '''
% 0.51/0.64 line 47:30 token recognition error at: '>'
% 0.51/0.64 line 47:31 token recognition error at: '='
% 0.51/0.64 line 47:32 token recognition error at: '''
% 0.51/0.64 line 47:34 token recognition error at: '''
% 0.51/0.64 line 47:35 token recognition error at: '+'
% 0.51/0.64 line 47:36 token recognition error at: '''
% 0.51/0.64 line 50:4 token recognition error at: '''
% 0.51/0.64 line 50:5 token recognition error at: '>'
% 0.51/0.64 line 50:6 token recognition error at: '='
% 0.51/0.64 line 50:7 token recognition error at: '''
% 0.51/0.64 line 50:9 mismatched input 'X0' expecting {'~', LOWER_WORD}
% 0.51/0.64 line 50:12 token recognition error at: '''
% 0.51/0.64 line 50:13 token recognition error at: '0'
% 0.51/0.64 line 50:14 token recognition error at: '''
% 0.51/0.64 line 50:16 extraneous input ')' expecting '.'
% 0.51/0.64 line 53:4 token recognition error at: '''
% 0.51/0.64 line 53:5 token recognition error at: '>'
% 0.51/0.64 line 53:6 token recognition error at: '='
% 0.51/0.64 line 53:7 token recognition error at: '''
% 0.51/0.64 line 53:9 token recognition error at: '''
% 0.51/0.64 line 53:10 token recognition error at: '+'
% 0.51/0.64 line 53:11 token recognition error at: '''
% 0.51/0.64 line 53:12 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.51/0.64 line 53:20 token recognition error at: '''
% 0.51/0.64 line 53:21 token recognition error at: '+'
% 0.51/0.64 line 53:22 token recognition error at: '''
% 0.51/0.64 line 53:19 mismatched input ',' expecting '.'
% 0.51/0.64 line 53:35 token recognition error at: '''
% 0.51/0.64 line 53:36 token recognition error at: '>'
% 0.51/0.64 line 53:37 token recognition error at: '='
% 0.51/0.64 line 53:38 token recognition error at: '''
% 0.51/0.64 line 56:4 token recognition error at: '''
% 0.51/0.64 line 56:5 token recognition error at: '>'
% 0.51/0.64 line 56:6 token recognition error at: '='
% 0.51/0.64 line 56:7 token recognition error at: '''
% 0.51/0.64 line 56:9 token recognition error at: '''
% 0.51/0.64 line 56:10 token recognition error at: '='
% 0.51/0.64 line 56:11 token recognition error at: '='
% 0.51/0.64 line 56:12 token recognition error at: '>'
% 0.51/0.64 line 56:13 token recognition error at: '''
% 0.51/0.64 line 56:14 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.51/0.64 line 56:22 token recognition error at: '''
% 0.51/0.64 line 56:23 token recognition error at: '='
% 0.51/0.64 line 56:24 token recognition error at: '='
% 0.51/0.64 line 56:25 token recognition error at: '>'
% 0.51/0.64 line 56:26 token recognition error at: '''
% 0.51/0.64 line 56:21 mismatched input ',' expecting '.'
% 0.51/0.64 line 56:39 token recognition error at: '''
% 0.51/0.64 line 56:40 token recognition error at: '>'
% 0.51/0.64 line 56:41 token recognition error at: '='
% 0.51/0.64 line 56:42 token recognition error at: '''
% 0.51/0.64 line 59:4 token recognition error at: '''
% 0.51/0.64 line 59:5 token recognition error at: '>'
% 0.51/0.64 line 59:6 token recognition error at: '='
% 0.51/0.64 line 59:7 token recognition error at: '''
% 0.51/0.64 line 59:9 token recognition error at: '''
% 0.51/0.64 line 59:10 token recognition error at: '='
% 0.51/0.64 line 59:11 token recognition error at: '='
% 0.51/0.64 line 59:12 token recognition error at: '>'
% 0.51/0.64 line 59:13 token recognition error at: '''
% 0.51/0.64 line 59:14 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.51/0.64 line 59:22 token recognition error at: '''
% 0.51/0.64 line 59:23 token recognition error at: '='
% 0.51/0.64 line 59:24 token recognition error at: '='
% 0.51/0.64 line 59:25 token recognition error at: '>'
% 0.51/0.64 line 59:26 token recognition error at: '''
% 0.51/0.64 line 59:21 mismatched input ',' expecting '.'
% 0.51/0.64 line 59:39 token recognition error at: '''
% 0.51/0.64 line 59:40 token recognition error at: '>'
% 0.51/0.64 line 59:41 token recognition error at: '='
% 0.51/0.64 line 59:42 token recognition error at: '''
% 0.51/0.64 line 62:16 token recognition error at: '''
% 0.51/0.64 line 62:17 token recognition error at: '+'
% 0.51/0.64 line 62:18 token recognition error at: '''
% 0.51/0.64 line 62:19 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.51/0.64 line 62:23 token recognition error at: '''
% 0.51/0.64 line 62:24 token recognition error at: '='
% 0.51/0.64 line 62:25 token recognition error at: '='
% 0.51/0.64 line 62:26 token recognition error at: '>'
% 0.51/0.64 line 62:27 token recognition error at: '''
% 0.51/0.64 line 62:28 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.51/0.64 line 62:37 token recognition error at: '''
% 0.51/0.64 line 62:38 token recognition error at: '+'
% 0.51/0.64 line 62:39 token recognition error at: '''
% 0.51/0.64 line 62:36 mismatched input ',' expecting {',', ')'}
% 0.51/0.64 line 62:44 token recognition error at: '''
% 0.51/0.64 line 62:45 token recognition error at: '='
% 0.51/0.64 line 62:46 token recognition error at: '='
% 0.51/0.64 line 62:47 token recognition error at: '>'
% 0.51/0.64 line 62:48 token recognition error at: '''
% 0.51/0.64 line 65:22 token recognition error at: '''
% 0.51/0.64 line 65:23 token recognition error at: '='
% 0.51/0.64 line 65:24 token recognition error at: '='
% 0.51/0.64 line 65:25 token recognition error at: '>'
% 0.51/0.64 line 65:26 token recognition error at: '''
% 0.51/0.64 line 65:27 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.51/0.64 line 65:38 extraneous input ')' expecting '.'
% 0.51/0.65 line 68:17 token recognition error at: '''
% 0.51/0.65 line 68:18 token recognition error at: '0'
% 0.51/0.65 line 68:19 token recognition error at: '''
% 0.51/0.65 line 68:20 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.51/0.65 % SZS status Error
% 0.51/0.65 java.lang.NullPointerException: Cannot invoke "Pair.getSecond()" because "clause" is null
% 0.51/0.65 java.util.concurrent.ExecutionException: java.lang.NullPointerException: Cannot invoke "Pair.getSecond()" because "clause" is null
% 0.51/0.65 at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
% 0.51/0.65 at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:205)
% 0.51/0.65 at Main.main(Main.java:24)
% 0.51/0.65 Caused by: java.lang.NullPointerException: Cannot invoke "Pair.getSecond()" because "clause" is null
% 0.51/0.65 at Main.loadFormulas(Main.java:194)
% 0.51/0.65 at Main.runModelBuilder(Main.java:42)
% 0.51/0.65 at Main.lambda$main$0(Main.java:21)
% 0.51/0.65 at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
% 0.51/0.65 at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
% 0.51/0.65 at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
% 0.51/0.65 at java.base/java.lang.Thread.run(Thread.java:1583)
% 0.51/0.67 % FMB4L exiting
%------------------------------------------------------------------------------