%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : LCL896+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.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.87s 1.02s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL896+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.07 % Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.17/0.44 % Computer : n010.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Thu Sep 24 00:39:43 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.25/0.52 Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.zK7HQu1Bec/theBenchmark.cnf 300
% 0.87/0.91 line 11:49 token recognition error at: '''
% 0.87/0.91 line 11:50 token recognition error at: '>'
% 0.87/0.91 line 11:51 token recognition error at: '='
% 0.87/0.91 line 11:52 token recognition error at: '''
% 0.87/0.91 line 11:53 missing LOWER_WORD at '('
% 0.87/0.92 line 11:63 token recognition error at: '''
% 0.87/0.92 line 11:64 token recognition error at: '>'
% 0.87/0.92 line 11:65 token recognition error at: '='
% 0.87/0.92 line 11:66 token recognition error at: '''
% 0.87/0.92 line 11:67 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.87/0.92 line 11:74 extraneous input ')' expecting '.'
% 0.87/0.92 line 14:60 token recognition error at: '''
% 0.87/0.92 line 14:61 token recognition error at: '='
% 0.87/0.92 line 14:62 token recognition error at: '='
% 0.87/0.92 line 14:63 token recognition error at: '>'
% 0.87/0.92 line 14:64 token recognition error at: '''
% 0.87/0.92 line 14:65 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.87/0.92 line 14:73 token recognition error at: '''
% 0.87/0.92 line 14:74 token recognition error at: '='
% 0.87/0.92 line 14:75 token recognition error at: '='
% 0.87/0.92 line 14:76 token recognition error at: '>'
% 0.87/0.92 line 14:77 token recognition error at: '''
% 0.87/0.92 line 14:72 mismatched input ',' expecting {',', ')'}
% 0.87/0.92 line 17:60 token recognition error at: '''
% 0.87/0.92 line 17:61 token recognition error at: '+'
% 0.87/0.92 line 17:62 token recognition error at: '''
% 0.87/0.92 line 17:63 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.87/0.92 line 17:71 token recognition error at: '''
% 0.87/0.92 line 17:72 token recognition error at: '+'
% 0.87/0.92 line 17:73 token recognition error at: '''
% 0.87/0.92 line 17:70 mismatched input ',' expecting {',', ')'}
% 0.87/0.92 line 20:16 token recognition error at: '''
% 0.87/0.92 line 20:17 token recognition error at: '+'
% 0.87/0.92 line 20:18 token recognition error at: '''
% 0.87/0.93 line 20:20 token recognition error at: '''
% 0.87/0.93 line 20:21 token recognition error at: '+'
% 0.87/0.93 line 20:22 token recognition error at: '''
% 0.87/0.93 line 20:19 mismatched input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.87/0.93 line 20:30 mismatched input ',' expecting {',', ')'}
% 0.87/0.93 line 20:35 token recognition error at: '''
% 0.87/0.93 line 20:36 token recognition error at: '+'
% 0.87/0.93 line 20:37 token recognition error at: '''
% 0.87/0.93 line 20:42 token recognition error at: '''
% 0.87/0.93 line 20:43 token recognition error at: '+'
% 0.87/0.93 line 20:44 token recognition error at: '''
% 0.87/0.93 line 23:16 token recognition error at: '''
% 0.87/0.93 line 23:17 token recognition error at: '+'
% 0.87/0.93 line 23:18 token recognition error at: '''
% 0.87/0.93 line 23:19 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.87/0.93 line 23:27 token recognition error at: '''
% 0.87/0.93 line 23:28 token recognition error at: '+'
% 0.87/0.93 line 23:29 token recognition error at: '''
% 0.87/0.93 line 23:26 mismatched input ',' expecting {',', ')'}
% 0.87/0.93 line 26:16 token recognition error at: '''
% 0.87/0.93 line 26:17 token recognition error at: '+'
% 0.87/0.93 line 26:18 token recognition error at: '''
% 0.87/0.93 line 26:19 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.87/0.93 line 26:23 token recognition error at: '''
% 0.87/0.93 line 26:24 token recognition error at: '0'
% 0.87/0.93 line 26:25 token recognition error at: '''
% 0.87/0.93 line 26:26 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.87/0.93 line 26:27 mismatched input ',' expecting {')', '|'}
% 0.87/0.93 line 29:4 token recognition error at: '''
% 0.87/0.93 line 29:5 token recognition error at: '>'
% 0.87/0.93 line 29:6 token recognition error at: '='
% 0.87/0.93 line 29:7 token recognition error at: '''
% 0.87/0.93 line 29:9 mismatched input 'X0' expecting {'~', LOWER_WORD}
% 0.87/0.93 line 29:15 extraneous input ')' expecting '.'
% 0.87/0.94 line 32:4 token recognition error at: '''
% 0.87/0.94 line 32:5 token recognition error at: '>'
% 0.87/0.94 line 32:6 token recognition error at: '='
% 0.87/0.94 line 32:7 token recognition error at: '''
% 0.87/0.94 line 32:9 mismatched input 'X0' expecting {'~', LOWER_WORD}
% 0.87/0.94 line 32:19 token recognition error at: '''
% 0.87/0.94 line 32:20 token recognition error at: '>'
% 0.87/0.94 line 32:21 token recognition error at: '='
% 0.87/0.94 line 32:22 token recognition error at: '''
% 0.87/0.94 line 32:23 missing LOWER_WORD at '('
% 0.87/0.94 line 32:34 token recognition error at: '''
% 0.87/0.94 line 32:35 token recognition error at: '>'
% 0.87/0.94 line 32:36 token recognition error at: '='
% 0.87/0.94 line 32:37 token recognition error at: '''
% 0.87/0.94 line 32:38 missing LOWER_WORD at '('
% 0.87/0.94 line 32:46 missing ')' at '.'
% 0.87/0.94 line 35:26 token recognition error at: '''
% 0.87/0.94 line 35:27 token recognition error at: '>'
% 0.87/0.94 line 35:28 token recognition error at: '='
% 0.87/0.94 line 35:29 token recognition error at: '''
% 0.87/0.94 line 35:30 missing LOWER_WORD at '('
% 0.87/0.94 line 35:41 token recognition error at: '''
% 0.87/0.94 line 35:42 token recognition error at: '>'
% 0.87/0.94 line 35:43 token recognition error at: '='
% 0.87/0.94 line 35:44 token recognition error at: '''
% 0.87/0.94 line 35:45 missing LOWER_WORD at '('
% 0.87/0.94 line 38:4 token recognition error at: '''
% 0.87/0.94 line 38:5 token recognition error at: '>'
% 0.87/0.94 line 38:6 token recognition error at: '='
% 0.87/0.94 line 38:7 token recognition error at: '''
% 0.87/0.94 line 38:9 token recognition error at: '''
% 0.87/0.94 line 38:10 token recognition error at: '+'
% 0.87/0.94 line 38:11 token recognition error at: '''
% 0.87/0.94 line 38:12 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.87/0.95 line 38:19 mismatched input ',' expecting '.'
% 0.87/0.95 line 38:27 token recognition error at: '''
% 0.87/0.95 line 38:28 token recognition error at: '>'
% 0.87/0.95 line 38:29 token recognition error at: '='
% 0.87/0.95 line 38:30 token recognition error at: '''
% 0.87/0.95 line 38:35 token recognition error at: '''
% 0.87/0.95 line 38:36 token recognition error at: '='
% 0.87/0.95 line 38:37 token recognition error at: '='
% 0.87/0.95 line 38:38 token recognition error at: '>'
% 0.87/0.95 line 38:39 token recognition error at: '''
% 0.87/0.95 line 41:4 token recognition error at: '''
% 0.87/0.95 line 41:5 token recognition error at: '>'
% 0.87/0.95 line 41:6 token recognition error at: '='
% 0.87/0.95 line 41:7 token recognition error at: '''
% 0.87/0.95 line 41:9 mismatched input 'X1' expecting {'~', LOWER_WORD}
% 0.87/0.95 line 41:12 token recognition error at: '''
% 0.87/0.95 line 41:13 token recognition error at: '='
% 0.87/0.95 line 41:14 token recognition error at: '='
% 0.87/0.95 line 41:15 token recognition error at: '>'
% 0.87/0.95 line 41:16 token recognition error at: '''
% 0.87/0.95 line 41:24 mismatched input ')' expecting '.'
% 0.87/0.95 line 41:29 token recognition error at: '''
% 0.87/0.95 line 41:30 token recognition error at: '>'
% 0.87/0.95 line 41:31 token recognition error at: '='
% 0.87/0.95 line 41:32 token recognition error at: '''
% 0.87/0.95 line 41:34 token recognition error at: '''
% 0.87/0.95 line 41:35 token recognition error at: '+'
% 0.87/0.95 line 41:36 token recognition error at: '''
% 0.87/0.95 line 44:4 token recognition error at: '''
% 0.87/0.95 line 44:5 token recognition error at: '>'
% 0.87/0.95 line 44:6 token recognition error at: '='
% 0.87/0.95 line 44:7 token recognition error at: '''
% 0.87/0.95 line 44:9 mismatched input 'X0' expecting {'~', LOWER_WORD}
% 0.87/0.95 line 44:12 token recognition error at: '''
% 0.87/0.95 line 44:13 token recognition error at: '0'
% 0.87/0.95 line 44:14 token recognition error at: '''
% 0.87/0.95 line 44:16 extraneous input ')' expecting '.'
% 0.87/0.95 line 47:4 token recognition error at: '''
% 0.87/0.95 line 47:5 token recognition error at: '>'
% 0.87/0.95 line 47:6 token recognition error at: '='
% 0.87/0.95 line 47:7 token recognition error at: '''
% 0.87/0.95 line 47:9 token recognition error at: '''
% 0.87/0.95 line 47:10 token recognition error at: '+'
% 0.87/0.95 line 47:11 token recognition error at: '''
% 0.87/0.95 line 47:12 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.87/0.95 line 47:20 token recognition error at: '''
% 0.87/0.95 line 47:21 token recognition error at: '+'
% 0.87/0.95 line 47:22 token recognition error at: '''
% 0.87/0.95 line 47:19 mismatched input ',' expecting '.'
% 0.87/0.95 line 47:35 token recognition error at: '''
% 0.87/0.95 line 47:36 token recognition error at: '>'
% 0.87/0.96 line 47:37 token recognition error at: '='
% 0.87/0.96 line 47:38 token recognition error at: '''
% 0.87/0.96 line 50:4 token recognition error at: '''
% 0.87/0.96 line 50:5 token recognition error at: '>'
% 0.87/0.96 line 50:6 token recognition error at: '='
% 0.87/0.96 line 50:7 token recognition error at: '''
% 0.87/0.96 line 50:9 token recognition error at: '''
% 0.87/0.96 line 50:10 token recognition error at: '='
% 0.87/0.96 line 50:11 token recognition error at: '='
% 0.87/0.96 line 50:12 token recognition error at: '>'
% 0.87/0.96 line 50:13 token recognition error at: '''
% 0.87/0.96 line 50:14 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.87/0.96 line 50:22 token recognition error at: '''
% 0.87/0.96 line 50:23 token recognition error at: '='
% 0.87/0.96 line 50:24 token recognition error at: '='
% 0.87/0.96 line 50:25 token recognition error at: '>'
% 0.87/0.96 line 50:26 token recognition error at: '''
% 0.87/0.96 line 50:21 mismatched input ',' expecting '.'
% 0.87/0.96 line 50:39 token recognition error at: '''
% 0.87/0.96 line 50:40 token recognition error at: '>'
% 0.87/0.96 line 50:41 token recognition error at: '='
% 0.87/0.96 line 50:42 token recognition error at: '''
% 0.87/0.96 line 53:4 token recognition error at: '''
% 0.87/0.96 line 53:5 token recognition error at: '>'
% 0.87/0.96 line 53:6 token recognition error at: '='
% 0.87/0.96 line 53:7 token recognition error at: '''
% 0.87/0.96 line 53:9 token recognition error at: '''
% 0.87/0.96 line 53:10 token recognition error at: '='
% 0.87/0.96 line 53:11 token recognition error at: '='
% 0.87/0.96 line 53:12 token recognition error at: '>'
% 0.87/0.96 line 53:13 token recognition error at: '''
% 0.87/0.96 line 53:14 mismatched input '(' expecting {'~', LOWER_WORD}
% 0.87/0.96 line 53:22 token recognition error at: '''
% 0.87/0.96 line 53:23 token recognition error at: '='
% 0.87/0.96 line 53:24 token recognition error at: '='
% 0.87/0.96 line 53:25 token recognition error at: '>'
% 0.87/0.96 line 53:26 token recognition error at: '''
% 0.87/0.96 line 53:21 mismatched input ',' expecting '.'
% 0.87/0.96 line 53:39 token recognition error at: '''
% 0.87/0.96 line 53:40 token recognition error at: '>'
% 0.87/0.96 line 53:41 token recognition error at: '='
% 0.87/0.96 line 53:42 token recognition error at: '''
% 0.87/0.96 line 56:16 token recognition error at: '''
% 0.87/0.96 line 56:17 token recognition error at: '+'
% 0.87/0.96 line 56:18 token recognition error at: '''
% 0.87/0.96 line 56:20 token recognition error at: '''
% 0.87/0.96 line 56:21 token recognition error at: '+'
% 0.87/0.96 line 56:22 token recognition error at: '''
% 0.87/0.96 line 56:19 mismatched input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.87/0.96 line 56:27 token recognition error at: '''
% 0.87/0.96 line 56:28 token recognition error at: '='
% 0.87/0.96 line 56:29 token recognition error at: '='
% 0.87/0.96 line 56:30 token recognition error at: '>'
% 0.87/0.96 line 56:31 token recognition error at: '''
% 0.87/0.96 line 56:32 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.87/0.96 line 56:41 token recognition error at: '''
% 0.87/0.96 line 56:42 token recognition error at: '='
% 0.87/0.96 line 56:43 token recognition error at: '='
% 0.87/0.96 line 56:44 token recognition error at: '>'
% 0.87/0.97 line 56:45 token recognition error at: '''
% 0.87/0.97 line 56:40 mismatched input ',' expecting {',', ')'}
% 0.87/0.97 line 56:47 token recognition error at: '''
% 0.87/0.97 line 56:48 token recognition error at: '+'
% 0.87/0.97 line 56:49 token recognition error at: '''
% 0.87/0.97 line 56:54 token recognition error at: '''
% 0.87/0.97 line 56:55 token recognition error at: '='
% 0.87/0.97 line 56:56 token recognition error at: '='
% 0.87/0.97 line 56:57 token recognition error at: '>'
% 0.87/0.97 line 56:58 token recognition error at: '''
% 0.87/0.97 line 56:73 token recognition error at: '''
% 0.87/0.97 line 56:74 token recognition error at: '+'
% 0.87/0.97 line 56:75 token recognition error at: '''
% 0.87/0.97 line 56:80 token recognition error at: '''
% 0.87/0.97 line 56:81 token recognition error at: '='
% 0.87/0.97 line 56:82 token recognition error at: '='
% 0.87/0.97 line 56:83 token recognition error at: '>'
% 0.87/0.97 line 56:84 token recognition error at: '''
% 0.87/0.97 line 56:89 token recognition error at: '''
% 0.87/0.97 line 56:90 token recognition error at: '+'
% 0.87/0.97 line 56:91 token recognition error at: '''
% 0.87/0.97 line 56:96 token recognition error at: '''
% 0.87/0.97 line 56:97 token recognition error at: '='
% 0.87/0.97 line 56:98 token recognition error at: '='
% 0.87/0.97 line 56:99 token recognition error at: '>'
% 0.87/0.97 line 56:100 token recognition error at: '''
% 0.87/0.97 line 59:17 token recognition error at: '''
% 0.87/0.97 line 59:18 token recognition error at: '+'
% 0.87/0.97 line 59:19 token recognition error at: '''
% 0.87/0.97 line 59:20 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.87/0.97 line 59:25 token recognition error at: '''
% 0.87/0.97 line 59:26 token recognition error at: '='
% 0.87/0.97 line 59:27 token recognition error at: '='
% 0.87/0.97 line 59:28 token recognition error at: '>'
% 0.87/0.97 line 59:29 token recognition error at: '''
% 0.87/0.97 line 59:30 extraneous input '(' expecting {LOWER_WORD, UPPER_WORD}
% 0.87/0.97 line 59:41 token recognition error at: '''
% 0.87/0.97 line 59:42 token recognition error at: '+'
% 0.87/0.97 line 59:43 token recognition error at: '''
% 0.87/0.97 line 59:40 mismatched input ',' expecting {'(', ',', ')'}
% 0.87/0.97 line 59:49 token recognition error at: '''
% 0.87/0.97 line 59:50 token recognition error at: '='
% 0.87/0.97 line 59:51 token recognition error at: '='
% 0.87/0.98 line 59:52 token recognition error at: '>'
% 0.87/0.98 line 59:53 token recognition error at: '''
% 0.87/0.98 % SZS status Error
% 0.87/0.98 java.lang.NullPointerException: Cannot invoke "Pair.getSecond()" because "clause" is null
% 0.87/0.98 java.util.concurrent.ExecutionException: java.lang.NullPointerException: Cannot invoke "Pair.getSecond()" because "clause" is null
% 0.87/0.98 at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
% 0.87/0.98 at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:205)
% 0.87/0.98 at Main.main(Main.java:24)
% 0.87/0.98 Caused by: java.lang.NullPointerException: Cannot invoke "Pair.getSecond()" because "clause" is null
% 0.87/0.98 at Main.loadFormulas(Main.java:194)
% 0.87/0.98 at Main.runModelBuilder(Main.java:42)
% 0.87/0.98 at Main.lambda$main$0(Main.java:21)
% 0.87/0.98 at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
% 0.87/0.98 at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
% 0.87/0.98 at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
% 0.87/0.98 at java.base/java.lang.Thread.run(Thread.java:1583)
% 0.87/1.02 % FMB4L exiting
%------------------------------------------------------------------------------