%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SWX065+1 : TPTP v9.3.1. Released v9.1.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 03:32:18 PM UTC 2026
% Result : Unknown 0.22s 6.51s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX065+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/5.58 % Computer : n016.cluster.edu
% 0.08/5.58 % Model : x86_64 x86_64
% 0.08/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.58 % Memory : 8046.5625MB
% 0.08/5.58 % OS : Linux 6.8.0-71-generic
% 0.08/5.58 % CPULimit : 300
% 0.08/5.58 % WCLimit : 300
% 0.08/5.58 % DateTime : Thu Sep 24 23:28:19 UTC 2026
% 0.08/5.58 % CPUTime :
% 0.08/5.58 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.14/5.69 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.jA6czYryLm/theBenchmark.cnf 300
% 0.76/6.08 line 164:23 token recognition error at: '''
% 0.76/6.08 line 164:24 token recognition error at: '1'
% 0.76/6.08 line 164:25 token recognition error at: '''
% 0.76/6.08 line 164:26 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.08 line 167:23 token recognition error at: '''
% 0.76/6.08 line 167:24 token recognition error at: '0'
% 0.76/6.08 line 167:25 token recognition error at: '''
% 0.76/6.08 line 167:26 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.09 line 188:31 token recognition error at: '''
% 0.76/6.09 line 188:32 token recognition error at: '1'
% 0.76/6.09 line 188:33 token recognition error at: '''
% 0.76/6.09 line 188:34 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.09 line 191:31 token recognition error at: '''
% 0.76/6.09 line 191:32 token recognition error at: '0'
% 0.76/6.09 line 191:33 token recognition error at: '''
% 0.76/6.09 line 191:34 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.09 line 206:19 token recognition error at: '''
% 0.76/6.09 line 206:20 token recognition error at: '1'
% 0.76/6.09 line 206:21 token recognition error at: '''
% 0.76/6.09 line 206:23 token recognition error at: '''
% 0.76/6.09 line 206:24 token recognition error at: '0'
% 0.76/6.09 line 206:25 token recognition error at: '''
% 0.76/6.09 line 206:22 mismatched input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.09 line 206:26 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.09 line 209:19 token recognition error at: '''
% 0.76/6.09 line 209:20 token recognition error at: '1'
% 0.76/6.09 line 209:21 token recognition error at: '''
% 0.76/6.09 line 209:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.09 line 212:19 token recognition error at: '''
% 0.76/6.09 line 212:20 token recognition error at: '1'
% 0.76/6.09 line 212:21 token recognition error at: '''
% 0.76/6.09 line 212:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.09 line 215:19 token recognition error at: '''
% 0.76/6.09 line 215:20 token recognition error at: '1'
% 0.76/6.09 line 215:21 token recognition error at: '''
% 0.76/6.09 line 215:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.10 line 218:19 token recognition error at: '''
% 0.76/6.10 line 218:20 token recognition error at: '1'
% 0.76/6.10 line 218:21 token recognition error at: '''
% 0.76/6.10 line 218:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.10 line 221:19 token recognition error at: '''
% 0.76/6.10 line 221:20 token recognition error at: '0'
% 0.76/6.10 line 221:21 token recognition error at: '''
% 0.76/6.10 line 221:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.10 line 224:19 token recognition error at: '''
% 0.76/6.10 line 224:20 token recognition error at: '0'
% 0.76/6.10 line 224:21 token recognition error at: '''
% 0.76/6.10 line 224:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.10 line 227:19 token recognition error at: '''
% 0.76/6.10 line 227:20 token recognition error at: '0'
% 0.76/6.10 line 227:21 token recognition error at: '''
% 0.76/6.10 line 227:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.10 line 230:19 token recognition error at: '''
% 0.76/6.10 line 230:20 token recognition error at: '0'
% 0.76/6.10 line 230:21 token recognition error at: '''
% 0.76/6.10 line 230:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.10 line 281:7 token recognition error at: '''
% 0.76/6.10 line 281:8 token recognition error at: '1'
% 0.76/6.10 line 281:9 token recognition error at: '''
% 0.76/6.10 line 281:10 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.76/6.11 line 284:7 token recognition error at: '''
% 0.76/6.11 line 284:8 token recognition error at: '0'
% 0.76/6.11 line 284:9 token recognition error at: '''
% 0.76/6.11 line 284:10 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.13 line 611:12 token recognition error at: '''
% 1.08/6.14 line 611:13 token recognition error at: '1'
% 1.08/6.14 line 611:14 token recognition error at: '''
% 1.08/6.14 line 611:15 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.14 line 611:50 token recognition error at: '''
% 1.08/6.14 line 611:51 token recognition error at: '1'
% 1.08/6.14 line 611:52 token recognition error at: '''
% 1.08/6.14 line 611:53 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.14 line 641:35 token recognition error at: '''
% 1.08/6.14 line 641:36 token recognition error at: '1'
% 1.08/6.14 line 641:37 token recognition error at: '''
% 1.08/6.14 line 641:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.14 line 644:53 token recognition error at: '''
% 1.08/6.14 line 644:54 token recognition error at: '1'
% 1.08/6.14 line 644:55 token recognition error at: '''
% 1.08/6.14 line 644:56 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.14 line 647:19 token recognition error at: '''
% 1.08/6.14 line 647:20 token recognition error at: '1'
% 1.08/6.14 line 647:21 token recognition error at: '''
% 1.08/6.14 line 647:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.14 line 647:50 token recognition error at: '''
% 1.08/6.14 line 647:51 token recognition error at: '1'
% 1.08/6.14 line 647:52 token recognition error at: '''
% 1.08/6.14 line 647:53 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.14 line 653:18 token recognition error at: '''
% 1.08/6.14 line 653:19 token recognition error at: '1'
% 1.08/6.14 line 653:20 token recognition error at: '''
% 1.08/6.14 line 653:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.14 line 656:36 token recognition error at: '''
% 1.08/6.14 line 656:37 token recognition error at: '1'
% 1.08/6.14 line 656:38 token recognition error at: '''
% 1.08/6.14 line 656:39 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.15 line 659:20 token recognition error at: '''
% 1.08/6.15 line 659:21 token recognition error at: '0'
% 1.08/6.15 line 659:22 token recognition error at: '''
% 1.08/6.15 line 659:23 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.15 line 659:51 token recognition error at: '''
% 1.08/6.15 line 659:52 token recognition error at: '0'
% 1.08/6.15 line 659:53 token recognition error at: '''
% 1.08/6.15 line 659:54 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.15 line 665:18 token recognition error at: '''
% 1.08/6.15 line 665:19 token recognition error at: '0'
% 1.08/6.15 line 665:20 token recognition error at: '''
% 1.08/6.15 line 665:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.15 line 668:36 token recognition error at: '''
% 1.08/6.15 line 668:37 token recognition error at: '0'
% 1.08/6.15 line 668:38 token recognition error at: '''
% 1.08/6.15 line 668:39 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.15 line 671:20 token recognition error at: '''
% 1.08/6.15 line 671:21 token recognition error at: '0'
% 1.08/6.15 line 671:22 token recognition error at: '''
% 1.08/6.15 line 671:23 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.15 line 671:51 token recognition error at: '''
% 1.08/6.15 line 671:52 token recognition error at: '0'
% 1.08/6.15 line 671:53 token recognition error at: '''
% 1.08/6.15 line 671:54 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.15 line 677:18 token recognition error at: '''
% 1.08/6.15 line 677:19 token recognition error at: '0'
% 1.08/6.15 line 677:20 token recognition error at: '''
% 1.08/6.15 line 677:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.15 line 680:36 token recognition error at: '''
% 1.08/6.15 line 680:37 token recognition error at: '0'
% 1.08/6.15 line 680:38 token recognition error at: '''
% 1.08/6.15 line 680:39 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.15 line 683:17 token recognition error at: '''
% 1.08/6.15 line 683:18 token recognition error at: '0'
% 1.08/6.15 line 683:19 token recognition error at: '''
% 1.08/6.15 line 683:20 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.15 line 683:48 token recognition error at: '''
% 1.08/6.15 line 683:49 token recognition error at: '1'
% 1.08/6.15 line 683:50 token recognition error at: '''
% 1.08/6.15 line 683:51 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.15 line 689:18 token recognition error at: '''
% 1.08/6.15 line 689:19 token recognition error at: '0'
% 1.08/6.15 line 689:20 token recognition error at: '''
% 1.08/6.15 line 689:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.15 line 692:37 token recognition error at: '''
% 1.08/6.15 line 692:38 token recognition error at: '1'
% 1.08/6.15 line 692:39 token recognition error at: '''
% 1.08/6.15 line 692:40 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 695:17 token recognition error at: '''
% 1.08/6.16 line 695:18 token recognition error at: '1'
% 1.08/6.16 line 695:19 token recognition error at: '''
% 1.08/6.16 line 695:20 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 695:48 token recognition error at: '''
% 1.08/6.16 line 695:49 token recognition error at: '0'
% 1.08/6.16 line 695:50 token recognition error at: '''
% 1.08/6.16 line 695:51 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 701:18 token recognition error at: '''
% 1.08/6.16 line 701:19 token recognition error at: '1'
% 1.08/6.16 line 701:20 token recognition error at: '''
% 1.08/6.16 line 701:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 704:37 token recognition error at: '''
% 1.08/6.16 line 704:38 token recognition error at: '0'
% 1.08/6.16 line 704:39 token recognition error at: '''
% 1.08/6.16 line 704:40 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 707:15 token recognition error at: '''
% 1.08/6.16 line 707:16 token recognition error at: '0'
% 1.08/6.16 line 707:17 token recognition error at: '''
% 1.08/6.16 line 707:18 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 713:18 token recognition error at: '''
% 1.08/6.16 line 713:19 token recognition error at: '0'
% 1.08/6.16 line 713:20 token recognition error at: '''
% 1.08/6.16 line 713:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 719:15 token recognition error at: '''
% 1.08/6.16 line 719:16 token recognition error at: '1'
% 1.08/6.16 line 719:17 token recognition error at: '''
% 1.08/6.16 line 719:18 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 725:18 token recognition error at: '''
% 1.08/6.16 line 725:19 token recognition error at: '1'
% 1.08/6.16 line 725:20 token recognition error at: '''
% 1.08/6.16 line 725:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 731:19 token recognition error at: '''
% 1.08/6.16 line 731:20 token recognition error at: '0'
% 1.08/6.16 line 731:21 token recognition error at: '''
% 1.08/6.16 line 731:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 731:50 token recognition error at: '''
% 1.08/6.16 line 731:51 token recognition error at: '0'
% 1.08/6.16 line 731:52 token recognition error at: '''
% 1.08/6.16 line 731:53 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 731:78 token recognition error at: '''
% 1.08/6.16 line 731:79 token recognition error at: '0'
% 1.08/6.16 line 731:80 token recognition error at: '''
% 1.08/6.16 line 731:81 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 737:18 token recognition error at: '''
% 1.08/6.16 line 737:19 token recognition error at: '0'
% 1.08/6.16 line 737:20 token recognition error at: '''
% 1.08/6.16 line 737:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 740:37 token recognition error at: '''
% 1.08/6.16 line 740:38 token recognition error at: '0'
% 1.08/6.16 line 740:39 token recognition error at: '''
% 1.08/6.16 line 740:40 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.16 line 743:37 token recognition error at: '''
% 1.08/6.16 line 743:38 token recognition error at: '0'
% 1.08/6.16 line 743:39 token recognition error at: '''
% 1.08/6.17 line 743:40 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.17 line 746:19 token recognition error at: '''
% 1.08/6.17 line 746:20 token recognition error at: '1'
% 1.08/6.17 line 746:21 token recognition error at: '''
% 1.08/6.17 line 746:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.17 line 746:50 token recognition error at: '''
% 1.08/6.17 line 746:51 token recognition error at: '1'
% 1.08/6.17 line 746:52 token recognition error at: '''
% 1.08/6.17 line 746:53 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.17 line 746:78 token recognition error at: '''
% 1.08/6.17 line 746:79 token recognition error at: '1'
% 1.08/6.17 line 746:80 token recognition error at: '''
% 1.08/6.17 line 746:81 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.17 line 752:18 token recognition error at: '''
% 1.08/6.17 line 752:19 token recognition error at: '1'
% 1.08/6.17 line 752:20 token recognition error at: '''
% 1.08/6.17 line 752:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.17 line 755:37 token recognition error at: '''
% 1.08/6.17 line 755:38 token recognition error at: '1'
% 1.08/6.17 line 755:39 token recognition error at: '''
% 1.08/6.17 line 755:40 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.17 line 758:37 token recognition error at: '''
% 1.08/6.17 line 758:38 token recognition error at: '1'
% 1.08/6.17 line 758:39 token recognition error at: '''
% 1.08/6.17 line 758:40 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.17 line 770:53 token recognition error at: '''
% 1.08/6.17 line 770:54 token recognition error at: '1'
% 1.08/6.17 line 770:55 token recognition error at: '''
% 1.08/6.17 line 770:56 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.17 line 773:70 token recognition error at: '''
% 1.08/6.17 line 773:71 token recognition error at: '1'
% 1.08/6.17 line 773:72 token recognition error at: '''
% 1.08/6.17 line 773:73 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.17 line 779:21 token recognition error at: '''
% 1.08/6.17 line 779:22 token recognition error at: '1'
% 1.08/6.17 line 779:23 token recognition error at: '''
% 1.08/6.17 line 779:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.17 line 779:37 token recognition error at: '''
% 1.08/6.17 line 779:38 token recognition error at: '1'
% 1.08/6.17 line 779:39 token recognition error at: '''
% 1.08/6.17 line 779:40 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 809:35 token recognition error at: '''
% 1.08/6.18 line 809:36 token recognition error at: '1'
% 1.08/6.18 line 809:37 token recognition error at: '''
% 1.08/6.18 line 809:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 812:52 token recognition error at: '''
% 1.08/6.18 line 812:53 token recognition error at: '1'
% 1.08/6.18 line 812:54 token recognition error at: '''
% 1.08/6.18 line 812:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 815:21 token recognition error at: '''
% 1.08/6.18 line 815:22 token recognition error at: '1'
% 1.08/6.18 line 815:23 token recognition error at: '''
% 1.08/6.18 line 815:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 815:44 token recognition error at: '''
% 1.08/6.18 line 815:45 token recognition error at: '1'
% 1.08/6.18 line 815:46 token recognition error at: '''
% 1.08/6.18 line 815:47 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 821:35 token recognition error at: '''
% 1.08/6.18 line 821:36 token recognition error at: '0'
% 1.08/6.18 line 821:37 token recognition error at: '''
% 1.08/6.18 line 821:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 824:52 token recognition error at: '''
% 1.08/6.18 line 824:53 token recognition error at: '0'
% 1.08/6.18 line 824:54 token recognition error at: '''
% 1.08/6.18 line 824:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 827:21 token recognition error at: '''
% 1.08/6.18 line 827:22 token recognition error at: '0'
% 1.08/6.18 line 827:23 token recognition error at: '''
% 1.08/6.18 line 827:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 827:45 token recognition error at: '''
% 1.08/6.18 line 827:46 token recognition error at: '0'
% 1.08/6.18 line 827:47 token recognition error at: '''
% 1.08/6.18 line 827:48 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 833:35 token recognition error at: '''
% 1.08/6.18 line 833:36 token recognition error at: '0'
% 1.08/6.18 line 833:37 token recognition error at: '''
% 1.08/6.18 line 833:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 836:52 token recognition error at: '''
% 1.08/6.18 line 836:53 token recognition error at: '0'
% 1.08/6.18 line 836:54 token recognition error at: '''
% 1.08/6.18 line 836:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 839:21 token recognition error at: '''
% 1.08/6.18 line 839:22 token recognition error at: '0'
% 1.08/6.18 line 839:23 token recognition error at: '''
% 1.08/6.18 line 839:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 839:45 token recognition error at: '''
% 1.08/6.18 line 839:46 token recognition error at: '0'
% 1.08/6.18 line 839:47 token recognition error at: '''
% 1.08/6.18 line 839:48 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.18 line 845:35 token recognition error at: '''
% 1.08/6.18 line 845:36 token recognition error at: '0'
% 1.08/6.18 line 845:37 token recognition error at: '''
% 1.08/6.18 line 845:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 848:52 token recognition error at: '''
% 1.08/6.19 line 848:53 token recognition error at: '1'
% 1.08/6.19 line 848:54 token recognition error at: '''
% 1.08/6.19 line 848:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 851:21 token recognition error at: '''
% 1.08/6.19 line 851:22 token recognition error at: '1'
% 1.08/6.19 line 851:23 token recognition error at: '''
% 1.08/6.19 line 851:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 851:42 token recognition error at: '''
% 1.08/6.19 line 851:43 token recognition error at: '0'
% 1.08/6.19 line 851:44 token recognition error at: '''
% 1.08/6.19 line 851:45 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 857:35 token recognition error at: '''
% 1.08/6.19 line 857:36 token recognition error at: '1'
% 1.08/6.19 line 857:37 token recognition error at: '''
% 1.08/6.19 line 857:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 860:52 token recognition error at: '''
% 1.08/6.19 line 860:53 token recognition error at: '0'
% 1.08/6.19 line 860:54 token recognition error at: '''
% 1.08/6.19 line 860:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 863:21 token recognition error at: '''
% 1.08/6.19 line 863:22 token recognition error at: '0'
% 1.08/6.19 line 863:23 token recognition error at: '''
% 1.08/6.19 line 863:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 863:42 token recognition error at: '''
% 1.08/6.19 line 863:43 token recognition error at: '1'
% 1.08/6.19 line 863:44 token recognition error at: '''
% 1.08/6.19 line 863:45 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 869:35 token recognition error at: '''
% 1.08/6.19 line 869:36 token recognition error at: '0'
% 1.08/6.19 line 869:37 token recognition error at: '''
% 1.08/6.19 line 869:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 875:46 token recognition error at: '''
% 1.08/6.19 line 875:47 token recognition error at: '0'
% 1.08/6.19 line 875:48 token recognition error at: '''
% 1.08/6.19 line 875:49 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 881:35 token recognition error at: '''
% 1.08/6.19 line 881:36 token recognition error at: '1'
% 1.08/6.19 line 881:37 token recognition error at: '''
% 1.08/6.19 line 881:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 887:41 token recognition error at: '''
% 1.08/6.19 line 887:42 token recognition error at: '1'
% 1.08/6.19 line 887:43 token recognition error at: '''
% 1.08/6.19 line 887:44 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 893:35 token recognition error at: '''
% 1.08/6.19 line 893:36 token recognition error at: '0'
% 1.08/6.19 line 893:37 token recognition error at: '''
% 1.08/6.19 line 893:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 896:52 token recognition error at: '''
% 1.08/6.19 line 896:53 token recognition error at: '0'
% 1.08/6.19 line 896:54 token recognition error at: '''
% 1.08/6.19 line 896:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 899:52 token recognition error at: '''
% 1.08/6.19 line 899:53 token recognition error at: '0'
% 1.08/6.19 line 899:54 token recognition error at: '''
% 1.08/6.19 line 899:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 902:21 token recognition error at: '''
% 1.08/6.19 line 902:22 token recognition error at: '0'
% 1.08/6.19 line 902:23 token recognition error at: '''
% 1.08/6.19 line 902:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.19 line 902:45 token recognition error at: '''
% 1.08/6.19 line 902:46 token recognition error at: '0'
% 1.08/6.19 line 902:47 token recognition error at: '''
% 1.08/6.20 line 902:48 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.20 line 902:68 token recognition error at: '''
% 1.08/6.20 line 902:69 token recognition error at: '0'
% 1.08/6.20 line 902:70 token recognition error at: '''
% 1.08/6.20 line 902:71 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.20 line 908:35 token recognition error at: '''
% 1.08/6.20 line 908:36 token recognition error at: '1'
% 1.08/6.20 line 908:37 token recognition error at: '''
% 1.08/6.20 line 908:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.08/6.20 line 911:52 token recognition error at: '''
% 1.08/6.20 line 911:53 token recognition error at: '1'
% 1.08/6.20 line 911:54 token recognition error at: '''
% 1.08/6.20 line 911:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.20 line 914:52 token recognition error at: '''
% 1.35/6.20 line 914:53 token recognition error at: '1'
% 1.35/6.20 line 914:54 token recognition error at: '''
% 1.35/6.20 line 914:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.20 line 917:21 token recognition error at: '''
% 1.35/6.20 line 917:22 token recognition error at: '1'
% 1.35/6.20 line 917:23 token recognition error at: '''
% 1.35/6.20 line 917:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.20 line 917:45 token recognition error at: '''
% 1.35/6.20 line 917:46 token recognition error at: '1'
% 1.35/6.20 line 917:47 token recognition error at: '''
% 1.35/6.20 line 917:48 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.20 line 917:69 token recognition error at: '''
% 1.35/6.20 line 917:70 token recognition error at: '1'
% 1.35/6.20 line 917:71 token recognition error at: '''
% 1.35/6.20 line 917:72 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.20 line 929:53 token recognition error at: '''
% 1.35/6.20 line 929:54 token recognition error at: '1'
% 1.35/6.20 line 929:55 token recognition error at: '''
% 1.35/6.20 line 929:56 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.20 line 932:75 token recognition error at: '''
% 1.35/6.20 line 932:76 token recognition error at: '1'
% 1.35/6.20 line 932:77 token recognition error at: '''
% 1.35/6.20 line 932:78 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.20 line 938:26 token recognition error at: '''
% 1.35/6.20 line 938:27 token recognition error at: '1'
% 1.35/6.20 line 938:28 token recognition error at: '''
% 1.35/6.20 line 938:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.20 line 938:42 token recognition error at: '''
% 1.35/6.20 line 938:43 token recognition error at: '1'
% 1.35/6.20 line 938:44 token recognition error at: '''
% 1.35/6.20 line 938:45 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.20 line 968:35 token recognition error at: '''
% 1.35/6.20 line 968:36 token recognition error at: '1'
% 1.35/6.20 line 968:37 token recognition error at: '''
% 1.35/6.20 line 968:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 971:57 token recognition error at: '''
% 1.35/6.21 line 971:58 token recognition error at: '1'
% 1.35/6.21 line 971:59 token recognition error at: '''
% 1.35/6.21 line 971:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 974:26 token recognition error at: '''
% 1.35/6.21 line 974:27 token recognition error at: '1'
% 1.35/6.21 line 974:28 token recognition error at: '''
% 1.35/6.21 line 974:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 974:49 token recognition error at: '''
% 1.35/6.21 line 974:50 token recognition error at: '1'
% 1.35/6.21 line 974:51 token recognition error at: '''
% 1.35/6.21 line 974:52 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 980:35 token recognition error at: '''
% 1.35/6.21 line 980:36 token recognition error at: '0'
% 1.35/6.21 line 980:37 token recognition error at: '''
% 1.35/6.21 line 980:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 983:57 token recognition error at: '''
% 1.35/6.21 line 983:58 token recognition error at: '0'
% 1.35/6.21 line 983:59 token recognition error at: '''
% 1.35/6.21 line 983:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 986:26 token recognition error at: '''
% 1.35/6.21 line 986:27 token recognition error at: '0'
% 1.35/6.21 line 986:28 token recognition error at: '''
% 1.35/6.21 line 986:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 986:50 token recognition error at: '''
% 1.35/6.21 line 986:51 token recognition error at: '0'
% 1.35/6.21 line 986:52 token recognition error at: '''
% 1.35/6.21 line 986:53 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 992:35 token recognition error at: '''
% 1.35/6.21 line 992:36 token recognition error at: '0'
% 1.35/6.21 line 992:37 token recognition error at: '''
% 1.35/6.21 line 992:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 995:57 token recognition error at: '''
% 1.35/6.21 line 995:58 token recognition error at: '0'
% 1.35/6.21 line 995:59 token recognition error at: '''
% 1.35/6.21 line 995:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 998:26 token recognition error at: '''
% 1.35/6.21 line 998:27 token recognition error at: '0'
% 1.35/6.21 line 998:28 token recognition error at: '''
% 1.35/6.21 line 998:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 998:50 token recognition error at: '''
% 1.35/6.21 line 998:51 token recognition error at: '0'
% 1.35/6.21 line 998:52 token recognition error at: '''
% 1.35/6.21 line 998:53 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 1004:35 token recognition error at: '''
% 1.35/6.21 line 1004:36 token recognition error at: '0'
% 1.35/6.21 line 1004:37 token recognition error at: '''
% 1.35/6.21 line 1004:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 1007:57 token recognition error at: '''
% 1.35/6.21 line 1007:58 token recognition error at: '1'
% 1.35/6.21 line 1007:59 token recognition error at: '''
% 1.35/6.21 line 1007:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 1010:26 token recognition error at: '''
% 1.35/6.21 line 1010:27 token recognition error at: '1'
% 1.35/6.21 line 1010:28 token recognition error at: '''
% 1.35/6.21 line 1010:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 1010:47 token recognition error at: '''
% 1.35/6.21 line 1010:48 token recognition error at: '0'
% 1.35/6.21 line 1010:49 token recognition error at: '''
% 1.35/6.21 line 1010:50 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 1016:35 token recognition error at: '''
% 1.35/6.21 line 1016:36 token recognition error at: '1'
% 1.35/6.21 line 1016:37 token recognition error at: '''
% 1.35/6.21 line 1016:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 1019:57 token recognition error at: '''
% 1.35/6.21 line 1019:58 token recognition error at: '0'
% 1.35/6.21 line 1019:59 token recognition error at: '''
% 1.35/6.21 line 1019:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.21 line 1022:26 token recognition error at: '''
% 1.35/6.21 line 1022:27 token recognition error at: '0'
% 1.35/6.21 line 1022:28 token recognition error at: '''
% 1.35/6.22 line 1022:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1022:47 token recognition error at: '''
% 1.35/6.22 line 1022:48 token recognition error at: '1'
% 1.35/6.22 line 1022:49 token recognition error at: '''
% 1.35/6.22 line 1022:50 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1028:35 token recognition error at: '''
% 1.35/6.22 line 1028:36 token recognition error at: '0'
% 1.35/6.22 line 1028:37 token recognition error at: '''
% 1.35/6.22 line 1028:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1034:51 token recognition error at: '''
% 1.35/6.22 line 1034:52 token recognition error at: '0'
% 1.35/6.22 line 1034:53 token recognition error at: '''
% 1.35/6.22 line 1034:54 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1040:35 token recognition error at: '''
% 1.35/6.22 line 1040:36 token recognition error at: '1'
% 1.35/6.22 line 1040:37 token recognition error at: '''
% 1.35/6.22 line 1040:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1046:46 token recognition error at: '''
% 1.35/6.22 line 1046:47 token recognition error at: '1'
% 1.35/6.22 line 1046:48 token recognition error at: '''
% 1.35/6.22 line 1046:49 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1052:35 token recognition error at: '''
% 1.35/6.22 line 1052:36 token recognition error at: '0'
% 1.35/6.22 line 1052:37 token recognition error at: '''
% 1.35/6.22 line 1052:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1055:57 token recognition error at: '''
% 1.35/6.22 line 1055:58 token recognition error at: '0'
% 1.35/6.22 line 1055:59 token recognition error at: '''
% 1.35/6.22 line 1055:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1055:95 token recognition error at: '''
% 1.35/6.22 line 1055:96 token recognition error at: '0'
% 1.35/6.22 line 1055:97 token recognition error at: '''
% 1.35/6.22 line 1055:98 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1058:57 token recognition error at: '''
% 1.35/6.22 line 1058:58 token recognition error at: '0'
% 1.35/6.22 line 1058:59 token recognition error at: '''
% 1.35/6.22 line 1058:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1058:100 token recognition error at: '''
% 1.35/6.22 line 1058:101 token recognition error at: '0'
% 1.35/6.22 line 1058:102 token recognition error at: '''
% 1.35/6.22 line 1058:103 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1061:26 token recognition error at: '''
% 1.35/6.22 line 1061:27 token recognition error at: '0'
% 1.35/6.22 line 1061:28 token recognition error at: '''
% 1.35/6.22 line 1061:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1061:49 token recognition error at: '''
% 1.35/6.22 line 1061:50 token recognition error at: '0'
% 1.35/6.22 line 1061:51 token recognition error at: '''
% 1.35/6.22 line 1061:52 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1064:21 token recognition error at: '''
% 1.35/6.22 line 1064:22 token recognition error at: '0'
% 1.35/6.22 line 1064:23 token recognition error at: '''
% 1.35/6.22 line 1064:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1064:50 token recognition error at: '''
% 1.35/6.22 line 1064:51 token recognition error at: '0'
% 1.35/6.22 line 1064:52 token recognition error at: '''
% 1.35/6.22 line 1064:53 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1064:73 token recognition error at: '''
% 1.35/6.22 line 1064:74 token recognition error at: '0'
% 1.35/6.22 line 1064:75 token recognition error at: '''
% 1.35/6.22 line 1064:76 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.22 line 1070:35 token recognition error at: '''
% 1.35/6.22 line 1070:36 token recognition error at: '1'
% 1.35/6.22 line 1070:37 token recognition error at: '''
% 1.35/6.22 line 1070:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.23 line 1073:57 token recognition error at: '''
% 1.35/6.23 line 1073:58 token recognition error at: '1'
% 1.35/6.23 line 1073:59 token recognition error at: '''
% 1.35/6.23 line 1073:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.23 line 1073:95 token recognition error at: '''
% 1.35/6.23 line 1073:96 token recognition error at: '1'
% 1.35/6.23 line 1073:97 token recognition error at: '''
% 1.35/6.23 line 1073:98 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.23 line 1076:57 token recognition error at: '''
% 1.35/6.23 line 1076:58 token recognition error at: '1'
% 1.35/6.23 line 1076:59 token recognition error at: '''
% 1.35/6.23 line 1076:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.23 line 1076:100 token recognition error at: '''
% 1.35/6.23 line 1076:101 token recognition error at: '1'
% 1.35/6.23 line 1076:102 token recognition error at: '''
% 1.35/6.23 line 1076:103 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.23 line 1079:26 token recognition error at: '''
% 1.35/6.23 line 1079:27 token recognition error at: '1'
% 1.35/6.23 line 1079:28 token recognition error at: '''
% 1.35/6.23 line 1079:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.23 line 1079:50 token recognition error at: '''
% 1.35/6.23 line 1079:51 token recognition error at: '1'
% 1.35/6.23 line 1079:52 token recognition error at: '''
% 1.35/6.23 line 1079:53 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.23 line 1082:21 token recognition error at: '''
% 1.35/6.23 line 1082:22 token recognition error at: '1'
% 1.35/6.23 line 1082:23 token recognition error at: '''
% 1.35/6.23 line 1082:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.23 line 1082:50 token recognition error at: '''
% 1.35/6.23 line 1082:51 token recognition error at: '1'
% 1.35/6.23 line 1082:52 token recognition error at: '''
% 1.35/6.23 line 1082:53 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 1.35/6.23 line 1082:74 token recognition error at: '''
% 1.35/6.23 line 1082:75 token recognition error at: '1'
% 1.35/6.23 line 1082:76 token recognition error at: '''
% 1.35/6.23 line 1082:77 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 1.80/6.33 % domain size: 1
% 2.26/6.47 % SZS status Error
% 2.26/6.47 java.lang.NullPointerException: Cannot invoke "FOL.Term.getArgs()" because "arg" is null
% 2.26/6.47 java.util.concurrent.ExecutionException: java.lang.NullPointerException: Cannot invoke "FOL.Term.getArgs()" because "arg" is null
% 2.26/6.47 at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
% 2.26/6.47 at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:205)
% 2.26/6.47 at Main.main(Main.java:24)
% 2.26/6.47 Caused by: java.lang.NullPointerException: Cannot invoke "FOL.Term.getArgs()" because "arg" is null
% 2.26/6.47 at ModelBuilder.ground(ModelBuilder.java:28)
% 2.26/6.47 at Main.runModelBuilder(Main.java:57)
% 2.26/6.47 at Main.lambda$main$0(Main.java:21)
% 2.26/6.47 at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
% 2.26/6.47 at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
% 2.26/6.47 at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
% 2.26/6.47 at java.base/java.lang.Thread.run(Thread.java:1583)
% 0.22/6.51 % FMB4L exiting
%------------------------------------------------------------------------------