%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SWX067+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n012.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.13s 5.93s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX067+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/5.36 % Computer : n012.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Thu Sep 24 23:23:12 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/5.45 Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.LehSHLhHTG/theBenchmark.cnf 300
% 0.13/5.69 line 173:23 token recognition error at: '''
% 0.13/5.69 line 173:24 token recognition error at: '1'
% 0.13/5.69 line 173:25 token recognition error at: '''
% 0.13/5.69 line 173:26 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.69 line 176:23 token recognition error at: '''
% 0.13/5.69 line 176:24 token recognition error at: '0'
% 0.13/5.69 line 176:25 token recognition error at: '''
% 0.13/5.69 line 176:26 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 197:31 token recognition error at: '''
% 0.13/5.70 line 197:32 token recognition error at: '1'
% 0.13/5.70 line 197:33 token recognition error at: '''
% 0.13/5.70 line 197:34 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 200:31 token recognition error at: '''
% 0.13/5.70 line 200:32 token recognition error at: '0'
% 0.13/5.70 line 200:33 token recognition error at: '''
% 0.13/5.70 line 200:34 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 215:19 token recognition error at: '''
% 0.13/5.70 line 215:20 token recognition error at: '1'
% 0.13/5.70 line 215:21 token recognition error at: '''
% 0.13/5.70 line 215:23 token recognition error at: '''
% 0.13/5.70 line 215:24 token recognition error at: '0'
% 0.13/5.70 line 215:25 token recognition error at: '''
% 0.13/5.70 line 215:22 mismatched input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 215:26 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 218:19 token recognition error at: '''
% 0.13/5.70 line 218:20 token recognition error at: '1'
% 0.13/5.70 line 218:21 token recognition error at: '''
% 0.13/5.70 line 218:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 221:19 token recognition error at: '''
% 0.13/5.70 line 221:20 token recognition error at: '1'
% 0.13/5.70 line 221:21 token recognition error at: '''
% 0.13/5.70 line 221:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 224:19 token recognition error at: '''
% 0.13/5.70 line 224:20 token recognition error at: '1'
% 0.13/5.70 line 224:21 token recognition error at: '''
% 0.13/5.70 line 224:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 227:19 token recognition error at: '''
% 0.13/5.70 line 227:20 token recognition error at: '1'
% 0.13/5.70 line 227:21 token recognition error at: '''
% 0.13/5.70 line 227:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 230:19 token recognition error at: '''
% 0.13/5.70 line 230:20 token recognition error at: '0'
% 0.13/5.70 line 230:21 token recognition error at: '''
% 0.13/5.70 line 230:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 233:19 token recognition error at: '''
% 0.13/5.70 line 233:20 token recognition error at: '0'
% 0.13/5.70 line 233:21 token recognition error at: '''
% 0.13/5.70 line 233:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 236:19 token recognition error at: '''
% 0.13/5.70 line 236:20 token recognition error at: '0'
% 0.13/5.70 line 236:21 token recognition error at: '''
% 0.13/5.70 line 236:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 239:19 token recognition error at: '''
% 0.13/5.70 line 239:20 token recognition error at: '0'
% 0.13/5.70 line 239:21 token recognition error at: '''
% 0.13/5.70 line 239:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.70 line 290:7 token recognition error at: '''
% 0.13/5.70 line 290:8 token recognition error at: '1'
% 0.13/5.71 line 290:9 token recognition error at: '''
% 0.13/5.71 line 290:10 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.71 line 293:7 token recognition error at: '''
% 0.13/5.71 line 293:8 token recognition error at: '0'
% 0.13/5.71 line 293:9 token recognition error at: '''
% 0.13/5.71 line 293:10 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.72 line 620:12 token recognition error at: '''
% 0.13/5.72 line 620:13 token recognition error at: '1'
% 0.13/5.72 line 620:14 token recognition error at: '''
% 0.13/5.72 line 620:15 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.72 line 620:50 token recognition error at: '''
% 0.13/5.72 line 620:51 token recognition error at: '1'
% 0.13/5.72 line 620:52 token recognition error at: '''
% 0.13/5.72 line 620:53 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.72 line 650:35 token recognition error at: '''
% 0.13/5.72 line 650:36 token recognition error at: '1'
% 0.13/5.72 line 650:37 token recognition error at: '''
% 0.13/5.72 line 650:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.72 line 653:53 token recognition error at: '''
% 0.13/5.72 line 653:54 token recognition error at: '1'
% 0.13/5.72 line 653:55 token recognition error at: '''
% 0.13/5.72 line 653:56 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.72 line 656:19 token recognition error at: '''
% 0.13/5.72 line 656:20 token recognition error at: '1'
% 0.13/5.72 line 656:21 token recognition error at: '''
% 0.13/5.72 line 656:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.72 line 656:50 token recognition error at: '''
% 0.13/5.72 line 656:51 token recognition error at: '1'
% 0.13/5.72 line 656:52 token recognition error at: '''
% 0.13/5.72 line 656:53 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 662:18 token recognition error at: '''
% 0.13/5.73 line 662:19 token recognition error at: '1'
% 0.13/5.73 line 662:20 token recognition error at: '''
% 0.13/5.73 line 662:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 665:36 token recognition error at: '''
% 0.13/5.73 line 665:37 token recognition error at: '1'
% 0.13/5.73 line 665:38 token recognition error at: '''
% 0.13/5.73 line 665:39 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 668:20 token recognition error at: '''
% 0.13/5.73 line 668:21 token recognition error at: '0'
% 0.13/5.73 line 668:22 token recognition error at: '''
% 0.13/5.73 line 668:23 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 668:51 token recognition error at: '''
% 0.13/5.73 line 668:52 token recognition error at: '0'
% 0.13/5.73 line 668:53 token recognition error at: '''
% 0.13/5.73 line 668:54 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 674:18 token recognition error at: '''
% 0.13/5.73 line 674:19 token recognition error at: '0'
% 0.13/5.73 line 674:20 token recognition error at: '''
% 0.13/5.73 line 674:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 677:36 token recognition error at: '''
% 0.13/5.73 line 677:37 token recognition error at: '0'
% 0.13/5.73 line 677:38 token recognition error at: '''
% 0.13/5.73 line 677:39 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 680:20 token recognition error at: '''
% 0.13/5.73 line 680:21 token recognition error at: '0'
% 0.13/5.73 line 680:22 token recognition error at: '''
% 0.13/5.73 line 680:23 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 680:51 token recognition error at: '''
% 0.13/5.73 line 680:52 token recognition error at: '0'
% 0.13/5.73 line 680:53 token recognition error at: '''
% 0.13/5.73 line 680:54 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 686:18 token recognition error at: '''
% 0.13/5.73 line 686:19 token recognition error at: '0'
% 0.13/5.73 line 686:20 token recognition error at: '''
% 0.13/5.73 line 686:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 689:36 token recognition error at: '''
% 0.13/5.73 line 689:37 token recognition error at: '0'
% 0.13/5.73 line 689:38 token recognition error at: '''
% 0.13/5.73 line 689:39 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 692:17 token recognition error at: '''
% 0.13/5.73 line 692:18 token recognition error at: '0'
% 0.13/5.73 line 692:19 token recognition error at: '''
% 0.13/5.73 line 692:20 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 692:48 token recognition error at: '''
% 0.13/5.73 line 692:49 token recognition error at: '1'
% 0.13/5.73 line 692:50 token recognition error at: '''
% 0.13/5.73 line 692:51 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 698:18 token recognition error at: '''
% 0.13/5.73 line 698:19 token recognition error at: '0'
% 0.13/5.73 line 698:20 token recognition error at: '''
% 0.13/5.73 line 698:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 701:36 token recognition error at: '''
% 0.13/5.73 line 701:37 token recognition error at: '1'
% 0.13/5.73 line 701:38 token recognition error at: '''
% 0.13/5.73 line 701:39 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 704:17 token recognition error at: '''
% 0.13/5.73 line 704:18 token recognition error at: '1'
% 0.13/5.73 line 704:19 token recognition error at: '''
% 0.13/5.73 line 704:20 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 704:48 token recognition error at: '''
% 0.13/5.73 line 704:49 token recognition error at: '0'
% 0.13/5.73 line 704:50 token recognition error at: '''
% 0.13/5.73 line 704:51 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 710:18 token recognition error at: '''
% 0.13/5.73 line 710:19 token recognition error at: '1'
% 0.13/5.73 line 710:20 token recognition error at: '''
% 0.13/5.73 line 710:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 713:36 token recognition error at: '''
% 0.13/5.73 line 713:37 token recognition error at: '0'
% 0.13/5.73 line 713:38 token recognition error at: '''
% 0.13/5.73 line 713:39 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 716:15 token recognition error at: '''
% 0.13/5.73 line 716:16 token recognition error at: '0'
% 0.13/5.73 line 716:17 token recognition error at: '''
% 0.13/5.73 line 716:18 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 722:18 token recognition error at: '''
% 0.13/5.73 line 722:19 token recognition error at: '0'
% 0.13/5.73 line 722:20 token recognition error at: '''
% 0.13/5.73 line 722:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 728:15 token recognition error at: '''
% 0.13/5.73 line 728:16 token recognition error at: '1'
% 0.13/5.73 line 728:17 token recognition error at: '''
% 0.13/5.73 line 728:18 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 734:18 token recognition error at: '''
% 0.13/5.73 line 734:19 token recognition error at: '1'
% 0.13/5.73 line 734:20 token recognition error at: '''
% 0.13/5.73 line 734:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 740:19 token recognition error at: '''
% 0.13/5.73 line 740:20 token recognition error at: '0'
% 0.13/5.73 line 740:21 token recognition error at: '''
% 0.13/5.73 line 740:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.73 line 740:50 token recognition error at: '''
% 0.13/5.73 line 740:51 token recognition error at: '0'
% 0.13/5.74 line 740:52 token recognition error at: '''
% 0.13/5.74 line 740:53 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 740:78 token recognition error at: '''
% 0.13/5.74 line 740:79 token recognition error at: '0'
% 0.13/5.74 line 740:80 token recognition error at: '''
% 0.13/5.74 line 740:81 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 746:18 token recognition error at: '''
% 0.13/5.74 line 746:19 token recognition error at: '0'
% 0.13/5.74 line 746:20 token recognition error at: '''
% 0.13/5.74 line 746:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 749:36 token recognition error at: '''
% 0.13/5.74 line 749:37 token recognition error at: '0'
% 0.13/5.74 line 749:38 token recognition error at: '''
% 0.13/5.74 line 749:39 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 752:36 token recognition error at: '''
% 0.13/5.74 line 752:37 token recognition error at: '0'
% 0.13/5.74 line 752:38 token recognition error at: '''
% 0.13/5.74 line 752:39 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 755:19 token recognition error at: '''
% 0.13/5.74 line 755:20 token recognition error at: '1'
% 0.13/5.74 line 755:21 token recognition error at: '''
% 0.13/5.74 line 755:22 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 755:50 token recognition error at: '''
% 0.13/5.74 line 755:51 token recognition error at: '1'
% 0.13/5.74 line 755:52 token recognition error at: '''
% 0.13/5.74 line 755:53 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 755:78 token recognition error at: '''
% 0.13/5.74 line 755:79 token recognition error at: '1'
% 0.13/5.74 line 755:80 token recognition error at: '''
% 0.13/5.74 line 755:81 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 761:18 token recognition error at: '''
% 0.13/5.74 line 761:19 token recognition error at: '1'
% 0.13/5.74 line 761:20 token recognition error at: '''
% 0.13/5.74 line 761:21 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 764:37 token recognition error at: '''
% 0.13/5.74 line 764:38 token recognition error at: '1'
% 0.13/5.74 line 764:39 token recognition error at: '''
% 0.13/5.74 line 764:40 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 767:37 token recognition error at: '''
% 0.13/5.74 line 767:38 token recognition error at: '1'
% 0.13/5.74 line 767:39 token recognition error at: '''
% 0.13/5.74 line 767:40 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 779:53 token recognition error at: '''
% 0.13/5.74 line 779:54 token recognition error at: '1'
% 0.13/5.74 line 779:55 token recognition error at: '''
% 0.13/5.74 line 779:56 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 782:70 token recognition error at: '''
% 0.13/5.74 line 782:71 token recognition error at: '1'
% 0.13/5.74 line 782:72 token recognition error at: '''
% 0.13/5.74 line 782:73 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 788:21 token recognition error at: '''
% 0.13/5.74 line 788:22 token recognition error at: '1'
% 0.13/5.74 line 788:23 token recognition error at: '''
% 0.13/5.74 line 788:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 788:37 token recognition error at: '''
% 0.13/5.74 line 788:38 token recognition error at: '1'
% 0.13/5.74 line 788:39 token recognition error at: '''
% 0.13/5.74 line 788:40 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 818:35 token recognition error at: '''
% 0.13/5.74 line 818:36 token recognition error at: '1'
% 0.13/5.74 line 818:37 token recognition error at: '''
% 0.13/5.74 line 818:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 821:52 token recognition error at: '''
% 0.13/5.74 line 821:53 token recognition error at: '1'
% 0.13/5.74 line 821:54 token recognition error at: '''
% 0.13/5.74 line 821:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 824:21 token recognition error at: '''
% 0.13/5.74 line 824:22 token recognition error at: '1'
% 0.13/5.74 line 824:23 token recognition error at: '''
% 0.13/5.74 line 824:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 824:44 token recognition error at: '''
% 0.13/5.74 line 824:45 token recognition error at: '1'
% 0.13/5.74 line 824:46 token recognition error at: '''
% 0.13/5.74 line 824:47 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 830:35 token recognition error at: '''
% 0.13/5.74 line 830:36 token recognition error at: '0'
% 0.13/5.74 line 830:37 token recognition error at: '''
% 0.13/5.74 line 830:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.74 line 833:52 token recognition error at: '''
% 0.13/5.74 line 833:53 token recognition error at: '0'
% 0.13/5.74 line 833:54 token recognition error at: '''
% 0.13/5.74 line 833:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 836:21 token recognition error at: '''
% 0.13/5.75 line 836:22 token recognition error at: '0'
% 0.13/5.75 line 836:23 token recognition error at: '''
% 0.13/5.75 line 836:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 836:45 token recognition error at: '''
% 0.13/5.75 line 836:46 token recognition error at: '0'
% 0.13/5.75 line 836:47 token recognition error at: '''
% 0.13/5.75 line 836:48 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 842:35 token recognition error at: '''
% 0.13/5.75 line 842:36 token recognition error at: '0'
% 0.13/5.75 line 842:37 token recognition error at: '''
% 0.13/5.75 line 842:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 845:52 token recognition error at: '''
% 0.13/5.75 line 845:53 token recognition error at: '0'
% 0.13/5.75 line 845:54 token recognition error at: '''
% 0.13/5.75 line 845:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 848:21 token recognition error at: '''
% 0.13/5.75 line 848:22 token recognition error at: '0'
% 0.13/5.75 line 848:23 token recognition error at: '''
% 0.13/5.75 line 848:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 848:45 token recognition error at: '''
% 0.13/5.75 line 848:46 token recognition error at: '0'
% 0.13/5.75 line 848:47 token recognition error at: '''
% 0.13/5.75 line 848:48 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 854:35 token recognition error at: '''
% 0.13/5.75 line 854:36 token recognition error at: '0'
% 0.13/5.75 line 854:37 token recognition error at: '''
% 0.13/5.75 line 854:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 857:52 token recognition error at: '''
% 0.13/5.75 line 857:53 token recognition error at: '1'
% 0.13/5.75 line 857:54 token recognition error at: '''
% 0.13/5.75 line 857:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 860:21 token recognition error at: '''
% 0.13/5.75 line 860:22 token recognition error at: '1'
% 0.13/5.75 line 860:23 token recognition error at: '''
% 0.13/5.75 line 860:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 860:42 token recognition error at: '''
% 0.13/5.75 line 860:43 token recognition error at: '0'
% 0.13/5.75 line 860:44 token recognition error at: '''
% 0.13/5.75 line 860:45 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 866:35 token recognition error at: '''
% 0.13/5.75 line 866:36 token recognition error at: '1'
% 0.13/5.75 line 866:37 token recognition error at: '''
% 0.13/5.75 line 866:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 869:52 token recognition error at: '''
% 0.13/5.75 line 869:53 token recognition error at: '0'
% 0.13/5.75 line 869:54 token recognition error at: '''
% 0.13/5.75 line 869:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 872:21 token recognition error at: '''
% 0.13/5.75 line 872:22 token recognition error at: '0'
% 0.13/5.75 line 872:23 token recognition error at: '''
% 0.13/5.75 line 872:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 872:42 token recognition error at: '''
% 0.13/5.75 line 872:43 token recognition error at: '1'
% 0.13/5.75 line 872:44 token recognition error at: '''
% 0.13/5.75 line 872:45 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 878:35 token recognition error at: '''
% 0.13/5.75 line 878:36 token recognition error at: '0'
% 0.13/5.75 line 878:37 token recognition error at: '''
% 0.13/5.75 line 878:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 884:46 token recognition error at: '''
% 0.13/5.75 line 884:47 token recognition error at: '0'
% 0.13/5.75 line 884:48 token recognition error at: '''
% 0.13/5.75 line 884:49 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 890:35 token recognition error at: '''
% 0.13/5.75 line 890:36 token recognition error at: '1'
% 0.13/5.75 line 890:37 token recognition error at: '''
% 0.13/5.75 line 890:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 896:41 token recognition error at: '''
% 0.13/5.75 line 896:42 token recognition error at: '1'
% 0.13/5.75 line 896:43 token recognition error at: '''
% 0.13/5.75 line 896:44 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 902:35 token recognition error at: '''
% 0.13/5.75 line 902:36 token recognition error at: '0'
% 0.13/5.75 line 902:37 token recognition error at: '''
% 0.13/5.75 line 902:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 905:52 token recognition error at: '''
% 0.13/5.75 line 905:53 token recognition error at: '0'
% 0.13/5.75 line 905:54 token recognition error at: '''
% 0.13/5.75 line 905:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 908:52 token recognition error at: '''
% 0.13/5.75 line 908:53 token recognition error at: '0'
% 0.13/5.75 line 908:54 token recognition error at: '''
% 0.13/5.75 line 908:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 911:21 token recognition error at: '''
% 0.13/5.75 line 911:22 token recognition error at: '0'
% 0.13/5.75 line 911:23 token recognition error at: '''
% 0.13/5.75 line 911:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 911:45 token recognition error at: '''
% 0.13/5.75 line 911:46 token recognition error at: '0'
% 0.13/5.75 line 911:47 token recognition error at: '''
% 0.13/5.75 line 911:48 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 911:68 token recognition error at: '''
% 0.13/5.75 line 911:69 token recognition error at: '0'
% 0.13/5.75 line 911:70 token recognition error at: '''
% 0.13/5.75 line 911:71 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 917:35 token recognition error at: '''
% 0.13/5.75 line 917:36 token recognition error at: '1'
% 0.13/5.75 line 917:37 token recognition error at: '''
% 0.13/5.75 line 917:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 920:52 token recognition error at: '''
% 0.13/5.75 line 920:53 token recognition error at: '1'
% 0.13/5.75 line 920:54 token recognition error at: '''
% 0.13/5.75 line 920:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 923:52 token recognition error at: '''
% 0.13/5.75 line 923:53 token recognition error at: '1'
% 0.13/5.75 line 923:54 token recognition error at: '''
% 0.13/5.75 line 923:55 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 926:21 token recognition error at: '''
% 0.13/5.75 line 926:22 token recognition error at: '1'
% 0.13/5.75 line 926:23 token recognition error at: '''
% 0.13/5.75 line 926:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 926:45 token recognition error at: '''
% 0.13/5.75 line 926:46 token recognition error at: '1'
% 0.13/5.75 line 926:47 token recognition error at: '''
% 0.13/5.75 line 926:48 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.75 line 926:69 token recognition error at: '''
% 0.13/5.75 line 926:70 token recognition error at: '1'
% 0.13/5.76 line 926:71 token recognition error at: '''
% 0.13/5.76 line 926:72 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 938:53 token recognition error at: '''
% 0.13/5.76 line 938:54 token recognition error at: '1'
% 0.13/5.76 line 938:55 token recognition error at: '''
% 0.13/5.76 line 938:56 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 941:75 token recognition error at: '''
% 0.13/5.76 line 941:76 token recognition error at: '1'
% 0.13/5.76 line 941:77 token recognition error at: '''
% 0.13/5.76 line 941:78 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 947:26 token recognition error at: '''
% 0.13/5.76 line 947:27 token recognition error at: '1'
% 0.13/5.76 line 947:28 token recognition error at: '''
% 0.13/5.76 line 947:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 947:42 token recognition error at: '''
% 0.13/5.76 line 947:43 token recognition error at: '1'
% 0.13/5.76 line 947:44 token recognition error at: '''
% 0.13/5.76 line 947:45 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 977:35 token recognition error at: '''
% 0.13/5.76 line 977:36 token recognition error at: '1'
% 0.13/5.76 line 977:37 token recognition error at: '''
% 0.13/5.76 line 977:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 980:57 token recognition error at: '''
% 0.13/5.76 line 980:58 token recognition error at: '1'
% 0.13/5.76 line 980:59 token recognition error at: '''
% 0.13/5.76 line 980:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 983:26 token recognition error at: '''
% 0.13/5.76 line 983:27 token recognition error at: '1'
% 0.13/5.76 line 983:28 token recognition error at: '''
% 0.13/5.76 line 983:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 983:49 token recognition error at: '''
% 0.13/5.76 line 983:50 token recognition error at: '1'
% 0.13/5.76 line 983:51 token recognition error at: '''
% 0.13/5.76 line 983:52 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 989:35 token recognition error at: '''
% 0.13/5.76 line 989:36 token recognition error at: '0'
% 0.13/5.76 line 989:37 token recognition error at: '''
% 0.13/5.76 line 989:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 992:57 token recognition error at: '''
% 0.13/5.76 line 992:58 token recognition error at: '0'
% 0.13/5.76 line 992:59 token recognition error at: '''
% 0.13/5.76 line 992:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 995:26 token recognition error at: '''
% 0.13/5.76 line 995:27 token recognition error at: '0'
% 0.13/5.76 line 995:28 token recognition error at: '''
% 0.13/5.76 line 995:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 995:50 token recognition error at: '''
% 0.13/5.76 line 995:51 token recognition error at: '0'
% 0.13/5.76 line 995:52 token recognition error at: '''
% 0.13/5.76 line 995:53 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1001:35 token recognition error at: '''
% 0.13/5.76 line 1001:36 token recognition error at: '0'
% 0.13/5.76 line 1001:37 token recognition error at: '''
% 0.13/5.76 line 1001:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1004:57 token recognition error at: '''
% 0.13/5.76 line 1004:58 token recognition error at: '0'
% 0.13/5.76 line 1004:59 token recognition error at: '''
% 0.13/5.76 line 1004:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1007:26 token recognition error at: '''
% 0.13/5.76 line 1007:27 token recognition error at: '0'
% 0.13/5.76 line 1007:28 token recognition error at: '''
% 0.13/5.76 line 1007:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1007:50 token recognition error at: '''
% 0.13/5.76 line 1007:51 token recognition error at: '0'
% 0.13/5.76 line 1007:52 token recognition error at: '''
% 0.13/5.76 line 1007:53 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1013:35 token recognition error at: '''
% 0.13/5.76 line 1013:36 token recognition error at: '0'
% 0.13/5.76 line 1013:37 token recognition error at: '''
% 0.13/5.76 line 1013:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1016:57 token recognition error at: '''
% 0.13/5.76 line 1016:58 token recognition error at: '1'
% 0.13/5.76 line 1016:59 token recognition error at: '''
% 0.13/5.76 line 1016:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1019:26 token recognition error at: '''
% 0.13/5.76 line 1019:27 token recognition error at: '1'
% 0.13/5.76 line 1019:28 token recognition error at: '''
% 0.13/5.76 line 1019:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1019:47 token recognition error at: '''
% 0.13/5.76 line 1019:48 token recognition error at: '0'
% 0.13/5.76 line 1019:49 token recognition error at: '''
% 0.13/5.76 line 1019:50 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1025:35 token recognition error at: '''
% 0.13/5.76 line 1025:36 token recognition error at: '1'
% 0.13/5.76 line 1025:37 token recognition error at: '''
% 0.13/5.76 line 1025:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1028:57 token recognition error at: '''
% 0.13/5.76 line 1028:58 token recognition error at: '0'
% 0.13/5.76 line 1028:59 token recognition error at: '''
% 0.13/5.76 line 1028:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1031:26 token recognition error at: '''
% 0.13/5.76 line 1031:27 token recognition error at: '0'
% 0.13/5.76 line 1031:28 token recognition error at: '''
% 0.13/5.76 line 1031:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1031:47 token recognition error at: '''
% 0.13/5.76 line 1031:48 token recognition error at: '1'
% 0.13/5.76 line 1031:49 token recognition error at: '''
% 0.13/5.76 line 1031:50 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1037:35 token recognition error at: '''
% 0.13/5.76 line 1037:36 token recognition error at: '0'
% 0.13/5.76 line 1037:37 token recognition error at: '''
% 0.13/5.76 line 1037:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1043:51 token recognition error at: '''
% 0.13/5.76 line 1043:52 token recognition error at: '0'
% 0.13/5.76 line 1043:53 token recognition error at: '''
% 0.13/5.76 line 1043:54 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.76 line 1049:35 token recognition error at: '''
% 0.13/5.76 line 1049:36 token recognition error at: '1'
% 0.13/5.76 line 1049:37 token recognition error at: '''
% 0.13/5.76 line 1049:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1055:46 token recognition error at: '''
% 0.13/5.77 line 1055:47 token recognition error at: '1'
% 0.13/5.77 line 1055:48 token recognition error at: '''
% 0.13/5.77 line 1055:49 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1061:35 token recognition error at: '''
% 0.13/5.77 line 1061:36 token recognition error at: '0'
% 0.13/5.77 line 1061:37 token recognition error at: '''
% 0.13/5.77 line 1061:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1064:57 token recognition error at: '''
% 0.13/5.77 line 1064:58 token recognition error at: '0'
% 0.13/5.77 line 1064:59 token recognition error at: '''
% 0.13/5.77 line 1064:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1064:95 token recognition error at: '''
% 0.13/5.77 line 1064:96 token recognition error at: '0'
% 0.13/5.77 line 1064:97 token recognition error at: '''
% 0.13/5.77 line 1064:98 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1067:57 token recognition error at: '''
% 0.13/5.77 line 1067:58 token recognition error at: '0'
% 0.13/5.77 line 1067:59 token recognition error at: '''
% 0.13/5.77 line 1067:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1067:100 token recognition error at: '''
% 0.13/5.77 line 1067:101 token recognition error at: '0'
% 0.13/5.77 line 1067:102 token recognition error at: '''
% 0.13/5.77 line 1067:103 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1070:26 token recognition error at: '''
% 0.13/5.77 line 1070:27 token recognition error at: '0'
% 0.13/5.77 line 1070:28 token recognition error at: '''
% 0.13/5.77 line 1070:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1070:49 token recognition error at: '''
% 0.13/5.77 line 1070:50 token recognition error at: '0'
% 0.13/5.77 line 1070:51 token recognition error at: '''
% 0.13/5.77 line 1070:52 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1073:21 token recognition error at: '''
% 0.13/5.77 line 1073:22 token recognition error at: '0'
% 0.13/5.77 line 1073:23 token recognition error at: '''
% 0.13/5.77 line 1073:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1073:50 token recognition error at: '''
% 0.13/5.77 line 1073:51 token recognition error at: '0'
% 0.13/5.77 line 1073:52 token recognition error at: '''
% 0.13/5.77 line 1073:53 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1073:73 token recognition error at: '''
% 0.13/5.77 line 1073:74 token recognition error at: '0'
% 0.13/5.77 line 1073:75 token recognition error at: '''
% 0.13/5.77 line 1073:76 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1079:35 token recognition error at: '''
% 0.13/5.77 line 1079:36 token recognition error at: '1'
% 0.13/5.77 line 1079:37 token recognition error at: '''
% 0.13/5.77 line 1079:38 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1082:57 token recognition error at: '''
% 0.13/5.77 line 1082:58 token recognition error at: '1'
% 0.13/5.77 line 1082:59 token recognition error at: '''
% 0.13/5.77 line 1082:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1082:95 token recognition error at: '''
% 0.13/5.77 line 1082:96 token recognition error at: '1'
% 0.13/5.77 line 1082:97 token recognition error at: '''
% 0.13/5.77 line 1082:98 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1085:57 token recognition error at: '''
% 0.13/5.77 line 1085:58 token recognition error at: '1'
% 0.13/5.77 line 1085:59 token recognition error at: '''
% 0.13/5.77 line 1085:60 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1085:100 token recognition error at: '''
% 0.13/5.77 line 1085:101 token recognition error at: '1'
% 0.13/5.77 line 1085:102 token recognition error at: '''
% 0.13/5.77 line 1085:103 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1088:26 token recognition error at: '''
% 0.13/5.77 line 1088:27 token recognition error at: '1'
% 0.13/5.77 line 1088:28 token recognition error at: '''
% 0.13/5.77 line 1088:29 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1088:50 token recognition error at: '''
% 0.13/5.77 line 1088:51 token recognition error at: '1'
% 0.13/5.77 line 1088:52 token recognition error at: '''
% 0.13/5.77 line 1088:53 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1091:21 token recognition error at: '''
% 0.13/5.77 line 1091:22 token recognition error at: '1'
% 0.13/5.77 line 1091:23 token recognition error at: '''
% 0.13/5.77 line 1091:24 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1091:50 token recognition error at: '''
% 0.13/5.77 line 1091:51 token recognition error at: '1'
% 0.13/5.77 line 1091:52 token recognition error at: '''
% 0.13/5.77 line 1091:53 mismatched input ')' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.77 line 1091:74 token recognition error at: '''
% 0.13/5.77 line 1091:75 token recognition error at: '1'
% 0.13/5.77 line 1091:76 token recognition error at: '''
% 0.13/5.77 line 1091:77 extraneous input ',' expecting {LOWER_WORD, UPPER_WORD}
% 0.13/5.82 % domain size: 1
% 0.13/5.90 % SZS status Error
% 0.13/5.90 java.lang.NullPointerException: Cannot invoke "FOL.Term.getArgs()" because "arg" is null
% 0.13/5.90 java.util.concurrent.ExecutionException: java.lang.NullPointerException: Cannot invoke "FOL.Term.getArgs()" because "arg" is null
% 0.13/5.90 at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
% 0.13/5.90 at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:205)
% 0.13/5.90 at Main.main(Main.java:24)
% 0.13/5.90 Caused by: java.lang.NullPointerException: Cannot invoke "FOL.Term.getArgs()" because "arg" is null
% 0.13/5.90 at ModelBuilder.ground(ModelBuilder.java:28)
% 0.13/5.90 at Main.runModelBuilder(Main.java:57)
% 0.13/5.90 at Main.lambda$main$0(Main.java:21)
% 0.13/5.90 at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
% 0.13/5.90 at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
% 0.13/5.90 at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
% 0.13/5.90 at java.base/java.lang.Thread.run(Thread.java:1583)
% 0.13/5.92 % FMB4L exiting
%------------------------------------------------------------------------------