%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : LCL683+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n020.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 : Mon Sep 7 12:06:52 PM UTC 2026
% Result : CounterSatisfiable 62.24s 62.55s
% Output : Model 62.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL683+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.11/0.36 % Computer : n020.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 6 01:59:12 UTC 2026
% 0.11/0.37 % CPUTime :
% 62.24/62.55 GeoParameters:
% 62.24/62.55
% 62.24/62.55 tptp_input = 1
% 62.24/62.55 tptp_output = 0
% 62.24/62.55 nonempty = 1
% 62.24/62.55 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 62.24/62.55 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 62.24/62.55
% 62.24/62.55
% 62.24/62.55 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 62.24/62.55 % SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p
% 62.24/62.55
% 62.24/62.55 Interpretation 818:
% 62.24/62.55 Guesses:
% 62.24/62.55 0 : guesser 2, 1, ( | 1, 0 ), 0, 1m2s old, 0 lemmas
% 62.24/62.55 1 : guesser 24, 22, ( | 0, 2, 1 ), 445, 31s old, 0 lemmas
% 62.24/62.55 2 : guesser 41, 39, ( | 0, 2, 1 ), 517, 26s old, 0 lemmas
% 62.24/62.55 3 : guesser 42, 40, ( | 1, 2, 0 ), 517, 26s old, 0 lemmas
% 62.24/62.55 4 : guesser 43, 41, ( | 0, 2, 1 ), 517, 26s old, 0 lemmas
% 62.24/62.55 5 : guesser 44, 42, ( | 1, 0 ), 517, 26s old, 0 lemmas
% 62.24/62.55 6 : guesser 45, 43, ( | 0, 1 ), 517, 26s old, 0 lemmas
% 62.24/62.55 7 : guesser 46, 44, ( | 1, 0 ), 517, 26s old, 0 lemmas
% 62.24/62.55 8 : guesser 47, 45, ( | 1, 0 ), 517, 26s old, 0 lemmas
% 62.24/62.55 9 : guesser 48, 46, ( | 0, 1 ), 517, 26s old, 0 lemmas
% 62.24/62.55 10 : guesser 49, 47, ( | 1, 0 ), 517, 26s old, 0 lemmas
% 62.24/62.55 11 : guesser 50, 48, ( | 0, 1 ), 517, 26s old, 0 lemmas
% 62.24/62.55 12 : guesser 51, 49, ( | 1, 0 ), 517, 26s old, 0 lemmas
% 62.24/62.55 13 : guesser 52, 50, ( | 1, 0 ), 517, 26s old, 0 lemmas
% 62.24/62.55 14 : guesser 53, 51, ( | 1, 0 ), 517, 26s old, 0 lemmas
% 62.24/62.55 15 : guesser 54, 52, ( | 0, 1 ), 517, 26s old, 0 lemmas
% 62.24/62.55 16 : guesser 55, 53, ( | 1, 0 ), 517, 26s old, 0 lemmas
% 62.24/62.55 17 : guesser 56, 54, ( | 1, 0 ), 517, 26s old, 0 lemmas
% 62.24/62.55 18 : guesser 57, 55, ( | 1, 0 ), 517, 26s old, 0 lemmas
% 62.24/62.55 19 : guesser 58, 56, ( | 0, 1 ), 517, 26s old, 0 lemmas
% 62.24/62.55 20 : guesser 59, 57, ( | 1, 0 ), 517, 26s old, 0 lemmas
% 62.24/62.55 21 : guesser 60, 58, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 22 : guesser 61, 59, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 23 : guesser 62, 60, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 24 : guesser 63, 61, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 25 : guesser 64, 62, ( | 0, 2, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 26 : guesser 67, 65, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 27 : guesser 68, 66, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 28 : guesser 69, 67, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 29 : guesser 70, 68, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 30 : guesser 71, 69, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 31 : guesser 72, 70, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 32 : guesser 73, 71, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 33 : guesser 74, 72, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 34 : guesser 75, 73, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 35 : guesser 76, 74, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 36 : guesser 77, 75, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 37 : guesser 78, 76, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 38 : guesser 79, 77, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 39 : guesser 80, 78, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 40 : guesser 81, 79, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 41 : guesser 82, 80, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 42 : guesser 83, 81, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 43 : guesser 84, 82, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 44 : guesser 85, 83, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 45 : guesser 86, 84, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 46 : guesser 87, 85, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 47 : guesser 88, 86, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 48 : guesser 89, 87, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 49 : guesser 90, 88, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 50 : guesser 91, 89, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 51 : guesser 92, 90, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 52 : guesser 93, 91, ( | 0, 1 ), 517, 25s old, 0 lemmas
% 62.24/62.55 53 : guesser 94, 92, ( | 1, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 54 : guesser 95, 93, ( | 1, 2, 0 ), 517, 25s old, 0 lemmas
% 62.24/62.55 55 : guesser 97, 95, ( 1 | 2, 0 ), 518, 25s old, 1 lemmas
% 62.24/62.55 56 : guesser 121, 118, ( 1, 0 | 3, 2 ), 646, 15s old, 1 lemmas
% 62.24/62.55 57 : guesser 145, 141, ( | 0, 3, 2, 4, 1 ), 647, 15s old, 0 lemmas
% 62.24/62.55 58 : guesser 146, 142, ( 1, 0 | 3, 4, 2 ), 647, 15s old, 1 lemmas
% 62.24/62.55 59 : guesser 149, 145, ( | 2, 1, 0, 4, 3 ), 648, 15s old, 0 lemmas
% 62.24/62.55 60 : guesser 152, 148, ( 1, 0 | 3, 4, 2 ), 659, 14s old, 1 lemmas
% 62.24/62.55 61 : guesser 154, 150, ( | 3, 2, 1, 4, 0 ), 673, 13s old, 0 lemmas
% 62.24/62.55 62 : guesser 157, 153, ( | 3, 2, 1, 4, 0 ), 673, 13s old, 0 lemmas
% 62.24/62.55 63 : guesser 158, 154, ( | 3, 2, 1, 4, 0 ), 673, 13s old, 0 lemmas
% 62.24/62.55 64 : guesser 159, 155, ( | 2, 1, 0, 4, 3 ), 673, 13s old, 0 lemmas
% 62.24/62.55 65 : guesser 163, 159, ( 0 | 3, 2, 4, 1 ), 699, 12s old, 1 lemmas
% 62.24/62.55 66 : guesser 167, 163, ( | 0, 3, 2, 4, 1 ), 700, 11s old, 0 lemmas
% 62.24/62.55 67 : guesser 168, 164, ( | 2, 1, 0, 4, 3 ), 700, 11s old, 0 lemmas
% 62.24/62.55 68 : guesser 169, 165, ( | 3, 2, 1, 4, 0 ), 700, 11s old, 0 lemmas
% 62.24/62.55 69 : guesser 173, 169, ( 0 | 3, 2, 4, 1 ), 700, 11s old, 1 lemmas
% 62.24/62.55 70 : guesser 174, 170, ( 1, 0 | 3, 4, 2 ), 701, 11s old, 1 lemmas
% 62.24/62.55 71 : guesser 177, 173, ( | 3, 2, 1, 4, 0 ), 702, 11s old, 0 lemmas
% 62.24/62.55 72 : guesser 178, 174, ( | 3, 2, 1, 4, 0 ), 702, 11s old, 0 lemmas
% 62.24/62.55 73 : guesser 181, 177, ( 1, 0 | 3, 4, 2 ), 702, 11s old, 1 lemmas
% 62.24/62.55 74 : guesser 182, 178, ( | 3, 2, 1, 4, 0 ), 703, 11s old, 0 lemmas
% 62.24/62.55 75 : guesser 185, 181, ( | 2, 1, 0, 4, 3 ), 704, 11s old, 0 lemmas
% 62.24/62.55 76 : guesser 189, 185, ( 0 | 3, 2, 4, 1 ), 704, 11s old, 1 lemmas
% 62.24/62.55 77 : guesser 190, 186, ( | 3, 2, 1, 4, 0 ), 705, 11s old, 0 lemmas
% 62.24/62.55 78 : guesser 192, 188, ( | 1, 0, 3, 4, 2 ), 705, 11s old, 0 lemmas
% 62.24/62.55 79 : guesser 193, 189, ( | 0, 3, 2, 4, 1 ), 705, 11s old, 0 lemmas
% 62.24/62.55 80 : guesser 194, 190, ( | 3, 2, 1, 4, 0 ), 705, 11s old, 0 lemmas
% 62.24/62.55 81 : guesser 195, 191, ( 1, 0 | 3, 4, 2 ), 705, 11s old, 1 lemmas
% 62.24/62.55 82 : guesser 197, 193, ( | 2, 1, 0, 4, 3 ), 706, 11s old, 0 lemmas
% 62.24/62.55 83 : guesser 201, 197, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 84 : guesser 202, 198, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 85 : guesser 203, 199, ( | 1, 0 ), 706, 11s old, 0 lemmas
% 62.24/62.55 86 : guesser 204, 200, ( | 1, 0 ), 706, 11s old, 0 lemmas
% 62.24/62.55 87 : guesser 205, 201, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 88 : guesser 206, 202, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 89 : guesser 207, 203, ( | 1, 0 ), 706, 11s old, 0 lemmas
% 62.24/62.55 90 : guesser 208, 204, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 91 : guesser 209, 205, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 92 : guesser 210, 206, ( | 1, 0 ), 706, 11s old, 0 lemmas
% 62.24/62.55 93 : guesser 211, 207, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 94 : guesser 212, 208, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 95 : guesser 213, 209, ( | 1, 0 ), 706, 11s old, 0 lemmas
% 62.24/62.55 96 : guesser 214, 210, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 97 : guesser 215, 211, ( | 1, 0 ), 706, 11s old, 0 lemmas
% 62.24/62.55 98 : guesser 216, 212, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 99 : guesser 217, 213, ( | 1, 0 ), 706, 11s old, 0 lemmas
% 62.24/62.55 100 : guesser 218, 214, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 101 : guesser 219, 215, ( | 1, 0 ), 706, 11s old, 0 lemmas
% 62.24/62.55 102 : guesser 220, 216, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 103 : guesser 221, 217, ( | 0, 1 ), 706, 11s old, 0 lemmas
% 62.24/62.55 104 : guesser 222, 218, ( 0 | 3, 2, 4, 1 ), 706, 11s old, 1 lemmas
% 62.24/62.55 105 : guesser 223, 219, ( 0 | 3, 2, 4, 1 ), 707, 11s old, 1 lemmas
% 62.24/62.55 106 : guesser 224, 220, ( | 0, 1 ), 708, 11s old, 0 lemmas
% 62.24/62.55 107 : guesser 225, 221, ( | 1, 0 ), 708, 11s old, 0 lemmas
% 62.24/62.55 108 : guesser 226, 222, ( | 1, 0 ), 708, 11s old, 0 lemmas
% 62.24/62.55 109 : guesser 227, 223, ( | 0, 1 ), 708, 11s old, 0 lemmas
% 62.24/62.55 110 : guesser 228, 224, ( | 1, 0 ), 708, 11s old, 0 lemmas
% 62.24/62.55 111 : guesser 229, 225, ( | 1, 0 ), 708, 11s old, 0 lemmas
% 62.24/62.55 112 : guesser 230, 226, ( | 1, 0 ), 708, 11s old, 0 lemmas
% 62.24/62.55 113 : guesser 231, 227, ( | 1, 0 ), 708, 11s old, 0 lemmas
% 62.24/62.55 114 : guesser 232, 228, ( | 0, 1 ), 708, 11s old, 0 lemmas
% 62.24/62.55 115 : guesser 233, 229, ( | 1, 0 ), 708, 11s old, 0 lemmas
% 62.24/62.55 116 : guesser 234, 230, ( 2, 1, 0 | 4, 3 ), 708, 11s old, 1 lemmas
% 62.24/62.55 117 : guesser 258, 253, ( 3, 0 | 2, 4, 5, 1 ), 709, 10s old, 1 lemmas
% 62.24/62.55 118 : guesser 260, 255, ( | 4, 1, 3, 0, 5, 2 ), 710, 10s old, 0 lemmas
% 62.24/62.55 119 : guesser 261, 256, ( | 4, 1, 3, 0, 5, 2 ), 710, 10s old, 0 lemmas
% 62.24/62.55 120 : guesser 265, 260, ( 3, 0 | 2, 4, 5, 1 ), 711, 10s old, 1 lemmas
% 62.24/62.55 121 : guesser 266, 261, ( | 1, 3, 0, 2, 5, 4 ), 712, 10s old, 0 lemmas
% 62.24/62.55 122 : guesser 271, 266, ( | 2, 4, 1, 3, 5, 0 ), 712, 10s old, 0 lemmas
% 62.24/62.55 123 : guesser 272, 267, ( | 2, 4, 1, 3, 5, 0 ), 712, 10s old, 0 lemmas
% 62.24/62.55 124 : guesser 273, 268, ( | 4, 1, 3, 0, 5, 2 ), 712, 10s old, 0 lemmas
% 62.24/62.55 125 : guesser 276, 271, ( | 0, 2, 4, 1, 5, 3 ), 748, 6s old, 0 lemmas
% 62.24/62.55 126 : guesser 277, 272, ( | 4, 1, 3, 0, 5, 2 ), 748, 6s old, 0 lemmas
% 62.24/62.55 127 : guesser 279, 274, ( 0 | 2, 4, 1, 5, 3 ), 749, 6s old, 1 lemmas
% 62.24/62.55 128 : guesser 280, 275, ( | 3, 0, 2, 4, 5, 1 ), 750, 6s old, 0 lemmas
% 62.24/62.55 129 : guesser 281, 276, ( | 4, 1, 3, 0, 5, 2 ), 750, 6s old, 0 lemmas
% 62.24/62.55 130 : guesser 283, 278, ( | 3, 0, 2, 4, 5, 1 ), 751, 6s old, 0 lemmas
% 62.24/62.55 131 : guesser 284, 279, ( 2 | 4, 1, 3, 5, 0 ), 751, 6s old, 1 lemmas
% 62.24/62.55 132 : guesser 287, 282, ( | 3, 0, 2, 4, 5, 1 ), 776, 4s old, 0 lemmas
% 62.24/62.55 133 : guesser 288, 283, ( 1, 3, 0 | 2, 5, 4 ), 776, 4s old, 1 lemmas
% 62.24/62.55 134 : guesser 289, 284, ( | 4, 1, 3, 0, 5, 2 ), 777, 4s old, 0 lemmas
% 62.24/62.55 135 : guesser 293, 288, ( 3, 0 | 2, 4, 5, 1 ), 778, 4s old, 1 lemmas
% 62.24/62.55 136 : guesser 294, 289, ( 2 | 4, 1, 3, 5, 0 ), 779, 4s old, 1 lemmas
% 62.24/62.55 137 : guesser 297, 292, ( 1 | 3, 0, 2, 5, 4 ), 798, 2s old, 1 lemmas
% 62.24/62.55 138 : guesser 298, 293, ( | 4, 1, 3, 0, 5, 2 ), 799, 1s old, 0 lemmas
% 62.24/62.55 139 : guesser 299, 294, ( | 0, 2, 4, 1, 5, 3 ), 799, 1s old, 0 lemmas
% 62.24/62.55 140 : guesser 300, 295, ( 3, 0 | 2, 4, 5, 1 ), 799, 1s old, 1 lemmas
% 62.24/62.55 141 : guesser 301, 296, ( | 1, 3, 0, 2, 5, 4 ), 800, 1s old, 0 lemmas
% 62.24/62.55 142 : guesser 302, 297, ( | 2, 4, 1, 3, 5, 0 ), 800, 1s old, 0 lemmas
% 62.24/62.55 143 : guesser 303, 298, ( | 2, 4, 1, 3, 5, 0 ), 800, 1s old, 0 lemmas
% 62.24/62.55 144 : guesser 304, 299, ( | 3, 0, 2, 4, 5, 1 ), 800, 1s old, 0 lemmas
% 62.24/62.55 145 : guesser 305, 300, ( | 4, 1, 3, 0, 5, 2 ), 800, 1s old, 0 lemmas
% 62.24/62.55 146 : guesser 309, 304, ( | 4, 1, 3, 0, 5, 2 ), 801, 1s old, 0 lemmas
% 62.24/62.55 147 : guesser 313, 308, ( | 4, 1, 3, 0, 5, 2 ), 802, 1s old, 0 lemmas
% 62.24/62.55 148 : guesser 314, 309, ( | 3, 0, 2, 4, 5, 1 ), 802, 1s old, 0 lemmas
% 62.24/62.55 149 : guesser 315, 310, ( 0, 2 | 4, 1, 5, 3 ), 802, 1s old, 1 lemmas
% 62.24/62.55 150 : guesser 316, 311, ( 1, 3, 0 | 2, 5, 4 ), 803, 1s old, 1 lemmas
% 62.24/62.55 151 : guesser 317, 312, ( 2 | 4, 1, 3, 5, 0 ), 804, 1s old, 1 lemmas
% 62.24/62.55 152 : guesser 318, 313, ( 2 | 4, 1, 3, 5, 0 ), 805, 1s old, 1 lemmas
% 62.24/62.55 153 : guesser 321, 316, ( | 3, 0, 2, 4, 5, 1 ), 806, 1s old, 0 lemmas
% 62.24/62.55 154 : guesser 322, 317, ( | 3, 0, 2, 4, 5, 1 ), 806, 1s old, 0 lemmas
% 62.24/62.55 155 : guesser 323, 318, ( | 1, 3, 0, 2, 5, 4 ), 806, 1s old, 0 lemmas
% 62.24/62.55 156 : guesser 324, 319, ( | 4, 1, 3, 0, 5, 2 ), 806, 1s old, 0 lemmas
% 62.24/62.55 157 : guesser 325, 320, ( | 4, 1, 3, 0, 5, 2 ), 806, 1s old, 0 lemmas
% 62.24/62.55 158 : guesser 326, 321, ( | 2, 4, 1, 3, 5, 0 ), 806, 1s old, 0 lemmas
% 62.24/62.55 159 : guesser 327, 322, ( | 3, 0, 2, 4, 5, 1 ), 806, 1s old, 0 lemmas
% 62.24/62.55 160 : guesser 328, 323, ( | 4, 1, 3, 0, 5, 2 ), 806, 1s old, 0 lemmas
% 62.24/62.55 161 : guesser 329, 324, ( | 0, 1 ), 806, 1s old, 0 lemmas
% 62.24/62.55 162 : guesser 330, 325, ( | 0, 1 ), 806, 1s old, 0 lemmas
% 62.24/62.55 163 : guesser 331, 326, ( | 0, 1 ), 806, 1s old, 0 lemmas
% 62.24/62.55 164 : guesser 332, 327, ( | 0, 1 ), 806, 1s old, 0 lemmas
% 62.24/62.55 165 : guesser 333, 328, ( | 1, 0 ), 806, 1s old, 0 lemmas
% 62.24/62.55 166 : guesser 334, 329, ( | 1, 0 ), 806, 1s old, 0 lemmas
% 62.24/62.55 167 : guesser 335, 330, ( | 1, 0 ), 806, 1s old, 0 lemmas
% 62.24/62.55 168 : guesser 336, 331, ( | 1, 0 ), 806, 1s old, 0 lemmas
% 62.24/62.55 169 : guesser 337, 332, ( | 0, 1 ), 806, 1s old, 0 lemmas
% 62.24/62.55 170 : guesser 338, 333, ( | 1, 0 ), 806, 1s old, 0 lemmas
% 62.24/62.55 171 : guesser 339, 334, ( | 3, 0, 2, 4, 5, 1 ), 806, 1s old, 0 lemmas
% 62.24/62.55 172 : guesser 344, 339, ( | 4, 1, 3, 0, 5, 2 ), 806, 0s old, 0 lemmas
% 62.24/62.55 173 : guesser 345, 340, ( 0 | 2, 4, 1, 5, 3 ), 806, 0s old, 1 lemmas
% 62.24/62.55 174 : guesser 346, 341, ( | 4, 1, 3, 0, 5, 2 ), 807, 0s old, 0 lemmas
% 62.24/62.55 175 : guesser 347, 342, ( 0 | 2, 4, 1, 5, 3 ), 807, 0s old, 1 lemmas
% 62.24/62.55 176 : guesser 348, 343, ( 1, 3, 0 | 2, 5, 4 ), 808, 0s old, 1 lemmas
% 62.24/62.55 177 : guesser 349, 344, ( | 4, 1, 3, 0, 5, 2 ), 809, 0s old, 0 lemmas
% 62.24/62.55 178 : guesser 350, 345, ( 1 | 3, 0, 2, 5, 4 ), 809, 0s old, 1 lemmas
% 62.24/62.55 179 : guesser 351, 346, ( 3, 0 | 2, 4, 5, 1 ), 810, 0s old, 1 lemmas
% 62.24/62.55 180 : guesser 352, 347, ( 0, 2 | 4, 1, 5, 3 ), 811, 0s old, 1 lemmas
% 62.24/62.55 181 : guesser 353, 348, ( | 3, 0, 2, 4, 5, 1 ), 812, 0s old, 0 lemmas
% 62.24/62.55 182 : guesser 354, 349, ( | 2, 4, 1, 3, 5, 0 ), 812, 0s old, 0 lemmas
% 62.24/62.55 183 : guesser 355, 350, ( | 0, 2, 4, 1, 5, 3 ), 812, 0s old, 0 lemmas
% 62.24/62.55 184 : guesser 356, 351, ( | 0, 2, 4, 1, 5, 3 ), 812, 0s old, 0 lemmas
% 62.24/62.55 185 : guesser 357, 352, ( | 3, 0, 2, 4, 5, 1 ), 812, 0s old, 0 lemmas
% 62.24/62.55 186 : guesser 358, 353, ( 0 | 2, 4, 1, 5, 3 ), 812, 0s old, 1 lemmas
% 62.24/62.55 187 : guesser 359, 354, ( | 0, 2, 4, 1, 5, 3 ), 813, 0s old, 0 lemmas
% 62.24/62.55 188 : guesser 360, 355, ( 0 | 2, 4, 1, 5, 3 ), 813, 0s old, 1 lemmas
% 62.24/62.55 189 : guesser 361, 356, ( | 3, 0, 2, 4, 5, 1 ), 814, 0s old, 0 lemmas
% 62.24/62.55 190 : guesser 362, 357, ( | 4, 1, 3, 0, 5, 2 ), 814, 0s old, 0 lemmas
% 62.24/62.55 191 : guesser 363, 358, ( | 4, 1, 3, 0, 5, 2 ), 814, 0s old, 0 lemmas
% 62.24/62.55 192 : guesser 364, 359, ( | 3, 0, 2, 4, 5, 1 ), 814, 0s old, 0 lemmas
% 62.24/62.55 193 : guesser 365, 360, ( 1 | 3, 0, 2, 5, 4 ), 814, 0s old, 1 lemmas
% 62.24/62.55 194 : guesser 366, 361, ( 1 | 3, 0, 2, 5, 4 ), 815, 0s old, 1 lemmas
% 62.24/62.55 195 : guesser 367, 362, ( 4, 1, 3 | 0, 5, 2 ), 816, 0s old, 1 lemmas
% 62.24/62.55 196 : guesser 368, 363, ( 0 | 2, 4, 1, 5, 3 ), 817, 0s old, 1 lemmas
% 62.24/62.55 197 : guesser 369, 364, ( | 4, 1, 3, 0, 5, 2 ), 818, 0s old, 0 lemmas
% 62.24/62.55
% 62.24/62.55 Elements:
% 62.24/62.55 { E0, E1, E2, E3, E4 }
% 62.24/62.55
% 62.24/62.55 Atoms:
% 62.24/62.55 0 : #-{T} E0 { }
% 62.24/62.55 1 : r1-{T}(E0,E0) { }
% 62.24/62.55 2 : #-{T} E1 { 0 }
% 62.24/62.55 3 : pppp85-{T}(E1) { 0 }
% 62.24/62.55 4 : r1-{T}(E1,E1) { 0 }
% 62.24/62.55 5 : pppp84-{T}(E1) { 0 }
% 62.24/62.55 6 : p62-{T}(E1) { 0 }
% 62.24/62.55 7 : p64-{T}(E1) { 0 }
% 62.24/62.55 8 : p63-{T}(E1) { 0 }
% 62.24/62.55 9 : p66-{T}(E1) { 0 }
% 62.24/62.55 10 : p52-{T}(E1) { 0 }
% 62.24/62.55 11 : p56-{T}(E1) { 0 }
% 62.24/62.55 12 : p54-{T}(E1) { 0 }
% 62.24/62.55 13 : p42-{T}(E1) { 0 }
% 62.24/62.55 14 : p43-{T}(E1) { 0 }
% 62.24/62.55 15 : p32-{T}(E1) { 0 }
% 62.24/62.55 16 : p34-{T}(E1) { 0 }
% 62.24/62.55 17 : p46-{T}(E1) { 0 }
% 62.24/62.55 18 : p22-{T}(E1) { 0 }
% 62.24/62.55 19 : p14-{T}(E1) { 0 }
% 62.24/62.55 20 : p16-{T}(E1) { 0 }
% 62.24/62.55 21 : p24-{T}(E1) { 0 }
% 62.24/62.55 22 : p26-{T}(E1) { 0 }
% 62.24/62.55 23 : p44-{T}(E1) { 0 }
% 62.24/62.55 24 : pppp83-{T}(E1,E0) { 0, 1 }
% 62.24/62.55 25 : r1-{T}(E1,E0) { 0, 1 }
% 62.24/62.55 26 : p16-{T}(E0) { 0, 1 }
% 62.24/62.55 27 : p62-{T}(E0) { 0, 1 }
% 62.24/62.55 28 : p64-{T}(E0) { 0, 1 }
% 62.24/62.55 29 : p63-{T}(E0) { 0, 1 }
% 62.24/62.55 30 : p66-{T}(E0) { 0, 1 }
% 62.24/62.55 31 : p22-{T}(E0) { 0, 1 }
% 62.24/62.55 32 : p24-{T}(E0) { 0, 1 }
% 62.24/62.55 33 : p32-{T}(E0) { 0, 1 }
% 62.24/62.55 34 : p42-{T}(E0) { 0, 1 }
% 62.24/62.55 35 : p56-{T}(E0) { 0, 1 }
% 62.24/62.55 36 : p34-{T}(E0) { 0, 1 }
% 62.24/62.55 37 : p14-{T}(E0) { 0, 1 }
% 62.24/62.55 38 : p26-{T}(E0) { 0, 1 }
% 62.24/62.55 39 : p54-{T}(E0) { 0, 1 }
% 62.24/62.55 40 : p52-{T}(E0) { 0, 1 }
% 62.24/62.55 41 : pppp81-{T}(E1,E0) { 0, 2 }
% 62.24/62.55 42 : pppp79-{T}(E1,E1) { 0, 3 }
% 62.24/62.55 43 : pppp77-{T}(E1,E0) { 0, 4 }
% 62.24/62.55 44 : p11-{T}(E1) { 0, 5 }
% 62.24/62.55 45 : pppp88-{T}(E1) { 0, 6 }
% 62.24/62.55 46 : p13-{T}(E1) { 0, 7 }
% 62.24/62.55 47 : p15-{T}(E1) { 0, 8 }
% 62.24/62.55 48 : pppp93-{T}(E1) { 0, 9 }
% 62.24/62.55 49 : p21-{T}(E1) { 0, 10 }
% 62.24/62.55 50 : pppp99-{T}(E1) { 0, 11 }
% 62.24/62.55 51 : p23-{T}(E1) { 0, 12 }
% 62.24/62.55 52 : p25-{T}(E1) { 0, 13 }
% 62.24/62.55 53 : p31-{T}(E1) { 0, 14 }
% 62.24/62.55 54 : pppp114-{T}(E1) { 0, 15 }
% 62.24/62.55 55 : p33-{T}(E1) { 0, 16 }
% 62.24/62.55 56 : p35-{T}(E1) { 0, 17 }
% 62.24/62.55 57 : p41-{T}(E1) { 0, 18 }
% 62.24/62.55 58 : pppp135-{T}(E1) { 0, 19 }
% 62.24/62.55 59 : p45-{T}(E1) { 0, 20 }
% 62.24/62.55 60 : pppp140-{T}(E1) { 0, 21 }
% 62.24/62.55 61 : pppp141-{T}(E1) { 0, 22 }
% 62.24/62.55 62 : p53-{T}(E1) { 0, 23 }
% 62.24/62.55 63 : p55-{T}(E1) { 0, 24 }
% 62.24/62.55 64 : pppp82-{T}(E0,E0) { 0, 1, 25 }
% 62.24/62.55 65 : pppp86-{T}(E0) { 0, 1, 25 }
% 62.24/62.55 66 : pppp87-{T}(E0) { 0, 1, 25 }
% 62.24/62.55 67 : pppp88-{T}(E0) { 0, 1, 26 }
% 62.24/62.55 68 : pppp89-{T}(E0) { 0, 1, 27 }
% 62.24/62.55 69 : p13-{T}(E0) { 0, 1, 28 }
% 62.24/62.55 70 : pppp91-{T}(E0) { 0, 1, 29 }
% 62.24/62.55 71 : p15-{T}(E0) { 0, 1, 30 }
% 62.24/62.55 72 : pppp93-{T}(E0) { 0, 1, 31 }
% 62.24/62.55 73 : pppp94-{T}(E0) { 0, 1, 32 }
% 62.24/62.55 74 : pppp95-{T}(E0) { 0, 1, 33 }
% 62.24/62.55 75 : pppp96-{T}(E0) { 0, 1, 34 }
% 62.24/62.55 76 : p23-{T}(E0) { 0, 1, 35 }
% 62.24/62.55 77 : pppp104-{T}(E0) { 0, 1, 36 }
% 62.24/62.55 78 : p25-{T}(E0) { 0, 1, 37 }
% 62.24/62.55 79 : p31-{T}(E0) { 0, 1, 38 }
% 62.24/62.55 80 : p33-{T}(E0) { 0, 1, 39 }
% 62.24/62.55 81 : pppp119-{T}(E0) { 0, 1, 40 }
% 62.24/62.55 82 : pppp120-{T}(E0) { 0, 1, 41 }
% 62.24/62.55 83 : p41-{T}(E0) { 0, 1, 42 }
% 62.24/62.55 84 : pppp129-{T}(E0) { 0, 1, 43 }
% 62.24/62.55 85 : pppp130-{T}(E0) { 0, 1, 44 }
% 62.24/62.55 86 : p43-{T}(E0) { 0, 1, 45 }
% 62.24/62.55 87 : p45-{T}(E0) { 0, 1, 46 }
% 62.24/62.55 88 : p44-{T}(E0) { 0, 1, 47 }
% 62.24/62.55 89 : p46-{T}(E0) { 0, 1, 48 }
% 62.24/62.55 90 : p51-{T}(E0) { 0, 1, 49 }
% 62.24/62.55 91 : pppp145-{T}(E0) { 0, 1, 50 }
% 62.24/62.55 92 : pppp146-{T}(E0) { 0, 1, 51 }
% 62.24/62.55 93 : pppp150-{T}(E0) { 0, 1, 52 }
% 62.24/62.55 94 : p55-{T}(E0) { 0, 1, 53 }
% 62.24/62.55 95 : pppp80-{T}(E1,E0) { 0, 2, 54 }
% 62.24/62.55 96 : r1-{T}(E0,E1) { 0, 2, 54 }
% 62.24/62.55 97 : #-{T} E2 { 0, 3, 55 }
% 62.24/62.55 98 : pppp78-{T}(E2,E1) { 0, 3, 55 }
% 62.24/62.55 99 : r1-{T}(E2,E2) { 0, 3, 55 }
% 62.24/62.55 100 : r1-{T}(E1,E2) { 0, 3, 55 }
% 62.24/62.55 101 : p16-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 102 : p14-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 103 : p62-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 104 : p64-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 105 : p63-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 106 : p66-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 107 : pppp90-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 108 : pppp89-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 109 : p22-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 110 : p24-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 111 : p26-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 112 : p32-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 113 : p34-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 114 : p42-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 115 : p56-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 116 : p54-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 117 : p52-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 118 : r1-{T}(E0,E2) { 0, 2, 3, 54, 55 }
% 62.24/62.55 119 : p44-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 120 : p46-{T}(E2) { 0, 3, 55 }
% 62.24/62.55 121 : #-{T} E3 { 0, 4, 56 }
% 62.24/62.55 122 : pppp76-{T}(E3,E0) { 0, 4, 56 }
% 62.24/62.55 123 : r1-{T}(E3,E3) { 0, 4, 56 }
% 62.24/62.55 124 : r1-{T}(E0,E3) { 0, 4, 56 }
% 62.24/62.55 125 : r1-{T}(E1,E3) { 0, 1, 4, 56 }
% 62.24/62.55 126 : p62-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 127 : p64-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 128 : p16-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 129 : p14-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 130 : p63-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 131 : p66-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 132 : pppp91-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 133 : pppp92-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 134 : p22-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 135 : p24-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 136 : p26-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 137 : p32-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 138 : p34-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 139 : p42-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 140 : p56-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 141 : p54-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 142 : p52-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 143 : p44-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 144 : p46-{T}(E3) { 0, 1, 4, 56 }
% 62.24/62.55 145 : pppp73-{T}(E0,E1) { 0, 6, 57 }
% 62.24/62.55 146 : pppp68-{T}(E1,E3) { 0, 9, 58 }
% 62.24/62.55 147 : pppp109-{T}(E3) { 0, 1, 4, 9, 56, 58 }
% 62.24/62.55 148 : pppp110-{T}(E3) { 0, 1, 4, 9, 56, 58 }
% 62.24/62.55 149 : pppp62-{T}(E1,E2) { 0, 11, 59 }
% 62.24/62.55 150 : pppp109-{T}(E2) { 0, 3, 11, 55, 59 }
% 62.24/62.55 151 : pppp110-{T}(E2) { 0, 3, 11, 55, 59 }
% 62.24/62.55 152 : pppp47-{T}(E3,E1) { 0, 15, 60 }
% 62.24/62.55 153 : pppp126-{T}(E3) { 0, 1, 4, 15, 56, 60 }
% 62.24/62.55 154 : pppp26-{T}(E1,E3) { 0, 19, 61 }
% 62.24/62.55 155 : pppp140-{T}(E3) { 0, 1, 4, 19, 56, 61 }
% 62.24/62.55 156 : pppp141-{T}(E3) { 0, 1, 4, 19, 56, 61 }
% 62.24/62.55 157 : pppp21-{T}(E3,E1) { 0, 21, 62 }
% 62.24/62.55 158 : pppp20-{T}(E3,E1) { 0, 22, 63 }
% 62.24/62.55 159 : pppp75-{T}(E2,E0) { 0, 1, 25, 64 }
% 62.24/62.55 160 : pppp100-{T}(E2) { 0, 1, 3, 25, 55, 64 }
% 62.24/62.55 161 : pppp99-{T}(E2) { 0, 1, 3, 25, 55, 64 }
% 62.24/62.55 162 : pppp101-{T}(E2) { 0, 1, 3, 25, 55, 64 }
% 62.24/62.55 163 : pppp74-{T}(E3,E0) { 0, 1, 25, 65 }
% 62.24/62.55 164 : pppp106-{T}(E3) { 0, 1, 4, 25, 56, 65 }
% 62.24/62.55 165 : pppp105-{T}(E3) { 0, 1, 4, 25, 56, 65 }
% 62.24/62.55 166 : pppp104-{T}(E3) { 0, 1, 4, 25, 56, 65 }
% 62.24/62.55 167 : pppp73-{T}(E0,E0) { 0, 1, 26, 66 }
% 62.24/62.55 168 : pppp72-{T}(E2,E0) { 0, 1, 27, 67 }
% 62.24/62.55 169 : pppp70-{T}(E3,E0) { 0, 1, 29, 68 }
% 62.24/62.55 170 : pppp100-{T}(E3) { 0, 1, 4, 29, 56, 68 }
% 62.24/62.55 171 : pppp101-{T}(E3) { 0, 1, 4, 29, 56, 68 }
% 62.24/62.55 172 : pppp99-{T}(E3) { 0, 1, 4, 29, 56, 68 }
% 62.24/62.55 173 : pppp68-{T}(E0,E3) { 0, 1, 31, 69 }
% 62.24/62.55 174 : pppp67-{T}(E0,E3) { 0, 1, 32, 70 }
% 62.24/62.55 175 : pppp114-{T}(E3) { 0, 1, 4, 32, 56, 70 }
% 62.24/62.55 176 : pppp115-{T}(E3) { 0, 1, 4, 32, 56, 70 }
% 62.24/62.55 177 : pppp66-{T}(E0,E3) { 0, 1, 33, 71 }
% 62.24/62.55 178 : pppp65-{T}(E0,E3) { 0, 1, 34, 72 }
% 62.24/62.55 179 : pppp120-{T}(E3) { 0, 1, 4, 34, 56, 72 }
% 62.24/62.55 180 : pppp119-{T}(E3) { 0, 1, 4, 34, 56, 72 }
% 62.24/62.55 181 : pppp57-{T}(E0,E3) { 0, 1, 36, 73 }
% 62.24/62.55 182 : pppp42-{T}(E3,E0) { 0, 1, 40, 74 }
% 62.24/62.55 183 : pppp125-{T}(E3) { 0, 1, 4, 40, 56, 74 }
% 62.24/62.55 184 : pppp124-{T}(E3) { 0, 1, 4, 40, 56, 74 }
% 62.24/62.55 185 : pppp41-{T}(E2,E0) { 0, 1, 41, 75 }
% 62.24/62.55 186 : pppp137-{T}(E2) { 0, 1, 3, 41, 55, 75 }
% 62.24/62.55 187 : pppp136-{T}(E2) { 0, 1, 3, 41, 55, 75 }
% 62.24/62.55 188 : pppp135-{T}(E2) { 0, 1, 3, 41, 55, 75 }
% 62.24/62.55 189 : pppp32-{T}(E0,E3) { 0, 1, 43, 76 }
% 62.24/62.55 190 : pppp31-{T}(E0,E3) { 0, 1, 44, 77 }
% 62.24/62.55 191 : pppp145-{T}(E3) { 0, 1, 4, 44, 56, 77 }
% 62.24/62.55 192 : pppp16-{T}(E1,E0) { 0, 1, 50, 78 }
% 62.24/62.55 193 : pppp15-{T}(E0,E0) { 0, 1, 51, 79 }
% 62.24/62.55 194 : pppp11-{T}(E3,E0) { 0, 1, 52, 80 }
% 62.24/62.55 195 : pppp72-{T}(E3,E2) { 0, 3, 55, 81 }
% 62.24/62.55 196 : r1-{T}(E2,E3) { 0, 3, 55, 81 }
% 62.24/62.55 197 : pppp71-{T}(E2,E2) { 0, 3, 55, 82 }
% 62.24/62.55 198 : pppp104-{T}(E2) { 0, 3, 55, 82 }
% 62.24/62.55 199 : pppp105-{T}(E2) { 0, 3, 55, 82 }
% 62.24/62.55 200 : pppp106-{T}(E2) { 0, 3, 55, 82 }
% 62.24/62.55 201 : pppp86-{T}(E2) { 0, 3, 55, 83 }
% 62.24/62.55 202 : pppp87-{T}(E2) { 0, 3, 55, 84 }
% 62.24/62.55 203 : p12-{T}(E2) { 0, 3, 55, 85 }
% 62.24/62.55 204 : p15-{T}(E2) { 0, 3, 55, 86 }
% 62.24/62.55 205 : pppp93-{T}(E2) { 0, 3, 55, 87 }
% 62.24/62.55 206 : pppp94-{T}(E2) { 0, 3, 55, 88 }
% 62.24/62.55 207 : p21-{T}(E2) { 0, 3, 55, 89 }
% 62.24/62.55 208 : pppp114-{T}(E2) { 0, 3, 55, 90 }
% 62.24/62.55 209 : pppp115-{T}(E2) { 0, 3, 55, 91 }
% 62.24/62.55 210 : p35-{T}(E2) { 0, 3, 55, 92 }
% 62.24/62.55 211 : pppp124-{T}(E2) { 0, 3, 55, 93 }
% 62.24/62.55 212 : pppp125-{T}(E2) { 0, 3, 55, 94 }
% 62.24/62.55 213 : p41-{T}(E2) { 0, 3, 55, 95 }
% 62.24/62.55 214 : pppp129-{T}(E2) { 0, 3, 55, 96 }
% 62.24/62.55 215 : p43-{T}(E2) { 0, 3, 55, 97 }
% 62.24/62.55 216 : pppp140-{T}(E2) { 0, 3, 55, 98 }
% 62.24/62.55 217 : p51-{T}(E2) { 0, 3, 55, 99 }
% 62.24/62.55 218 : pppp145-{T}(E2) { 0, 3, 55, 100 }
% 62.24/62.55 219 : p53-{T}(E2) { 0, 3, 55, 101 }
% 62.24/62.55 220 : pppp150-{T}(E2) { 0, 3, 55, 102 }
% 62.24/62.55 221 : pppp151-{T}(E2) { 0, 3, 55, 103 }
% 62.24/62.55 222 : pppp70-{T}(E3,E3) { 0, 1, 4, 56, 104 }
% 62.24/62.55 223 : pppp69-{T}(E3,E3) { 0, 1, 4, 56, 105 }
% 62.24/62.55 224 : pppp86-{T}(E3) { 0, 1, 4, 56, 106 }
% 62.24/62.55 225 : p11-{T}(E3) { 0, 1, 4, 56, 107 }
% 62.24/62.55 226 : p12-{T}(E3) { 0, 1, 4, 56, 108 }
% 62.24/62.55 227 : pppp89-{T}(E3) { 0, 1, 4, 56, 109 }
% 62.24/62.55 228 : p13-{T}(E3) { 0, 1, 4, 56, 110 }
% 62.24/62.55 229 : p21-{T}(E3) { 0, 1, 4, 56, 111 }
% 62.24/62.55 230 : p43-{T}(E3) { 0, 1, 4, 56, 112 }
% 62.24/62.55 231 : p45-{T}(E3) { 0, 1, 4, 56, 113 }
% 62.24/62.55 232 : pppp146-{T}(E3) { 0, 1, 4, 56, 114 }
% 62.24/62.55 233 : p55-{T}(E3) { 0, 1, 4, 56, 115 }
% 62.24/62.55 234 : #-{T} E4 { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 235 : pppp52-{T}(E4,E3) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 236 : r1-{T}(E4,E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 237 : r1-{T}(E3,E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 238 : r1-{T}(E0,E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 239 : p62-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 240 : p64-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 241 : r1-{T}(E1,E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 242 : p63-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 243 : p66-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 244 : p16-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 245 : p14-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 246 : p22-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 247 : p24-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 248 : p26-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 249 : p32-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 250 : p34-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 251 : p42-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 252 : p56-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 253 : p54-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 254 : p52-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 255 : p44-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 256 : p46-{T}(E4) { 0, 1, 4, 9, 56, 58, 116 }
% 62.24/62.55 257 : r1-{T}(E2,E4) { 0, 1, 3, 4, 9, 55, 56, 58, 81, 116 }
% 62.24/62.55 258 : pppp51-{T}(E2,E3) { 0, 1, 4, 9, 56, 58, 117 }
% 62.24/62.55 259 : r1-{T}(E3,E2) { 0, 1, 4, 9, 56, 58, 117 }
% 62.24/62.55 260 : pppp52-{T}(E4,E2) { 0, 3, 11, 55, 59, 118 }
% 62.24/62.55 261 : pppp51-{T}(E4,E2) { 0, 3, 11, 55, 59, 119 }
% 62.24/62.55 262 : pppp135-{T}(E4) { 0, 1, 3, 4, 9, 11, 55, 56, 58, 59, 116, 119 }
% 62.24/62.55 263 : pppp137-{T}(E4) { 0, 1, 3, 4, 9, 11, 55, 56, 58, 59, 116, 119 }
% 62.24/62.55 264 : pppp136-{T}(E4) { 0, 1, 3, 4, 9, 11, 55, 56, 58, 59, 116, 119 }
% 62.24/62.55 265 : pppp35-{T}(E3,E2) { 0, 1, 4, 15, 56, 60, 120 }
% 62.24/62.55 266 : pppp21-{T}(E1,E3) { 0, 1, 4, 19, 56, 61, 121 }
% 62.24/62.55 267 : r1-{T}(E3,E1) { 0, 1, 4, 19, 56, 61, 121 }
% 62.24/62.55 268 : r1-{T}(E3,E0) { 0, 1, 4, 19, 56, 61, 121 }
% 62.24/62.55 269 : r1-{T}(E2,E1) { 0, 1, 3, 4, 19, 55, 56, 61, 81, 121 }
% 62.24/62.55 270 : r1-{T}(E2,E0) { 0, 1, 3, 4, 19, 55, 56, 61, 81, 121 }
% 62.24/62.55 271 : pppp20-{T}(E2,E3) { 0, 1, 4, 19, 56, 61, 122 }
% 62.24/62.55 272 : pppp62-{T}(E2,E2) { 0, 1, 3, 25, 55, 64, 123 }
% 62.24/62.55 273 : pppp61-{T}(E2,E4) { 0, 1, 3, 25, 55, 64, 124 }
% 62.24/62.55 274 : pppp114-{T}(E4) { 0, 1, 3, 4, 9, 25, 55, 56, 58, 64, 116, 124 }
% 62.24/62.55 275 : pppp115-{T}(E4) { 0, 1, 3, 4, 9, 25, 55, 56, 58, 64, 116, 124 }
% 62.24/62.55 276 : pppp60-{T}(E2,E0) { 0, 1, 3, 25, 55, 64, 125 }
% 62.24/62.55 277 : pppp57-{T}(E3,E4) { 0, 1, 4, 25, 56, 65, 126 }
% 62.24/62.55 278 : pppp110-{T}(E4) { 0, 1, 4, 9, 25, 56, 58, 65, 116, 126 }
% 62.24/62.55 279 : pppp56-{T}(E3,E2) { 0, 1, 4, 25, 56, 65, 127 }
% 62.24/62.55 280 : pppp55-{T}(E3,E3) { 0, 1, 4, 25, 56, 65, 128 }
% 62.24/62.55 281 : pppp62-{T}(E3,E4) { 0, 1, 4, 29, 56, 68, 129 }
% 62.24/62.55 282 : pppp109-{T}(E4) { 0, 1, 4, 9, 29, 56, 58, 68, 116, 129 }
% 62.24/62.55 283 : pppp61-{T}(E3,E3) { 0, 1, 4, 29, 56, 68, 130 }
% 62.24/62.55 284 : pppp60-{T}(E3,E4) { 0, 1, 4, 29, 56, 68, 131 }
% 62.24/62.55 285 : pppp119-{T}(E4) { 0, 1, 4, 9, 29, 56, 58, 68, 116, 131 }
% 62.24/62.55 286 : pppp120-{T}(E4) { 0, 1, 4, 9, 29, 56, 58, 68, 116, 131 }
% 62.24/62.55 287 : pppp47-{T}(E3,E3) { 0, 1, 4, 32, 56, 70, 132 }
% 62.24/62.55 288 : pppp46-{T}(E2,E3) { 0, 1, 4, 32, 56, 70, 133 }
% 62.24/62.55 289 : pppp42-{T}(E4,E3) { 0, 1, 4, 34, 56, 72, 134 }
% 62.24/62.55 290 : pppp125-{T}(E4) { 0, 1, 4, 9, 34, 56, 58, 72, 116, 134 }
% 62.24/62.55 291 : pppp124-{T}(E4) { 0, 1, 4, 9, 34, 56, 58, 72, 116, 134 }
% 62.24/62.55 292 : pppp126-{T}(E4) { 0, 1, 4, 9, 34, 56, 58, 72, 116, 134 }
% 62.24/62.55 293 : pppp41-{T}(E2,E3) { 0, 1, 4, 34, 56, 72, 135 }
% 62.24/62.55 294 : pppp37-{T}(E3,E4) { 0, 1, 4, 40, 56, 74, 136 }
% 62.24/62.55 295 : pppp141-{T}(E4) { 0, 1, 4, 9, 40, 56, 58, 74, 116, 136 }
% 62.24/62.55 296 : pppp140-{T}(E4) { 0, 1, 4, 9, 40, 56, 58, 74, 116, 136 }
% 62.24/62.55 297 : pppp36-{T}(E3,E3) { 0, 1, 4, 40, 56, 74, 137 }
% 62.24/62.55 298 : pppp26-{T}(E2,E4) { 0, 1, 3, 41, 55, 75, 138 }
% 62.24/62.55 299 : pppp25-{T}(E2,E0) { 0, 1, 3, 41, 55, 75, 139 }
% 62.24/62.55 300 : pppp24-{T}(E2,E2) { 0, 1, 3, 41, 55, 75, 140 }
% 62.24/62.55 301 : pppp16-{T}(E1,E3) { 0, 1, 4, 44, 56, 77, 141 }
% 62.24/62.55 302 : pppp57-{T}(E2,E2) { 0, 3, 55, 82, 142 }
% 62.24/62.55 303 : pppp56-{T}(E2,E2) { 0, 3, 55, 82, 143 }
% 62.24/62.55 304 : pppp55-{T}(E2,E3) { 0, 3, 55, 82, 144 }
% 62.24/62.55 305 : pppp75-{T}(E4,E2) { 0, 3, 55, 83, 145 }
% 62.24/62.55 306 : pppp100-{T}(E4) { 0, 1, 3, 4, 9, 55, 56, 58, 83, 116, 145 }
% 62.24/62.55 307 : pppp99-{T}(E4) { 0, 1, 3, 4, 9, 55, 56, 58, 83, 116, 145 }
% 62.24/62.55 308 : pppp101-{T}(E4) { 0, 1, 3, 4, 9, 55, 56, 58, 83, 116, 145 }
% 62.24/62.55 309 : pppp74-{T}(E4,E2) { 0, 3, 55, 84, 146 }
% 62.24/62.55 310 : pppp106-{T}(E4) { 0, 1, 3, 4, 9, 55, 56, 58, 84, 116, 146 }
% 62.24/62.55 311 : pppp105-{T}(E4) { 0, 1, 3, 4, 9, 55, 56, 58, 84, 116, 146 }
% 62.24/62.55 312 : pppp104-{T}(E4) { 0, 1, 3, 4, 9, 55, 56, 58, 84, 116, 146 }
% 62.24/62.55 313 : pppp68-{T}(E2,E4) { 0, 3, 55, 87, 147 }
% 62.24/62.55 314 : pppp67-{T}(E2,E3) { 0, 3, 55, 88, 148 }
% 62.24/62.55 315 : pppp47-{T}(E4,E2) { 0, 3, 55, 90, 149 }
% 62.24/62.55 316 : pppp46-{T}(E2,E2) { 0, 3, 55, 91, 150 }
% 62.24/62.55 317 : pppp37-{T}(E2,E4) { 0, 3, 55, 93, 151 }
% 62.24/62.55 318 : pppp36-{T}(E2,E4) { 0, 3, 55, 94, 152 }
% 62.24/62.55 319 : pppp146-{T}(E4) { 0, 1, 3, 4, 9, 55, 56, 58, 94, 116, 152 }
% 62.24/62.55 320 : pppp145-{T}(E4) { 0, 1, 3, 4, 9, 55, 56, 58, 94, 116, 152 }
% 62.24/62.55 321 : pppp32-{T}(E2,E3) { 0, 3, 55, 96, 153 }
% 62.24/62.55 322 : pppp21-{T}(E3,E2) { 0, 3, 55, 98, 154 }
% 62.24/62.55 323 : pppp16-{T}(E1,E2) { 0, 3, 55, 100, 155 }
% 62.24/62.55 324 : pppp11-{T}(E4,E2) { 0, 3, 55, 102, 156 }
% 62.24/62.55 325 : pppp10-{T}(E4,E2) { 0, 3, 55, 103, 157 }
% 62.24/62.55 326 : pppp75-{T}(E2,E3) { 0, 1, 4, 56, 106, 158 }
% 62.24/62.55 327 : pppp72-{T}(E3,E3) { 0, 1, 4, 56, 109, 159 }
% 62.24/62.55 328 : pppp15-{T}(E4,E3) { 0, 1, 4, 56, 114, 160 }
% 62.24/62.55 329 : pppp86-{T}(E4) { 0, 1, 4, 9, 56, 58, 116, 161 }
% 62.24/62.55 330 : pppp87-{T}(E4) { 0, 1, 4, 9, 56, 58, 116, 162 }
% 62.24/62.55 331 : pppp88-{T}(E4) { 0, 1, 4, 9, 56, 58, 116, 163 }
% 62.24/62.55 332 : pppp89-{T}(E4) { 0, 1, 4, 9, 56, 58, 116, 164 }
% 62.24/62.55 333 : p13-{T}(E4) { 0, 1, 4, 9, 56, 58, 116, 165 }
% 62.24/62.55 334 : p15-{T}(E4) { 0, 1, 4, 9, 56, 58, 116, 166 }
% 62.24/62.55 335 : p21-{T}(E4) { 0, 1, 4, 9, 56, 58, 116, 167 }
% 62.24/62.55 336 : p43-{T}(E4) { 0, 1, 4, 9, 56, 58, 116, 168 }
% 62.24/62.55 337 : pppp150-{T}(E4) { 0, 1, 4, 9, 56, 58, 116, 169 }
% 62.24/62.55 338 : p55-{T}(E4) { 0, 1, 4, 9, 56, 58, 116, 170 }
% 62.24/62.55 339 : pppp26-{T}(E4,E3) { 0, 1, 3, 4, 9, 11, 55, 56, 58, 59, 116, 119, 171 }
% 62.24/62.55 340 : r1-{T}(E4,E3) { 0, 1, 3, 4, 9, 11, 55, 56, 58, 59, 116, 119, 171 }
% 62.24/62.55 341 : r1-{T}(E4,E2) { 0, 1, 3, 4, 9, 11, 55, 56, 58, 59, 116, 117, 119, 171 }
% 62.24/62.55 342 : r1-{T}(E4,E1) { 0, 1, 3, 4, 9, 11, 19, 55, 56, 58, 59, 61, 116, 119, 121, 171 }
% 62.24/62.55 343 : r1-{T}(E4,E0) { 0, 1, 3, 4, 9, 11, 19, 55, 56, 58, 59, 61, 116, 119, 121, 171 }
% 62.24/62.55 344 : pppp25-{T}(E4,E4) { 0, 1, 3, 4, 9, 11, 55, 56, 58, 59, 116, 119, 172 }
% 62.24/62.55 345 : pppp24-{T}(E4,E2) { 0, 1, 3, 4, 9, 11, 55, 56, 58, 59, 116, 119, 173 }
% 62.24/62.55 346 : pppp47-{T}(E4,E4) { 0, 1, 3, 4, 9, 25, 55, 56, 58, 64, 116, 124, 174 }
% 62.24/62.55 347 : pppp46-{T}(E2,E4) { 0, 1, 3, 4, 9, 25, 55, 56, 58, 64, 116, 124, 175 }
% 62.24/62.55 348 : pppp51-{T}(E2,E4) { 0, 1, 4, 9, 25, 56, 58, 65, 116, 126, 176 }
% 62.24/62.55 349 : pppp52-{T}(E4,E4) { 0, 1, 4, 9, 29, 56, 58, 68, 116, 129, 177 }
% 62.24/62.55 350 : pppp42-{T}(E3,E4) { 0, 1, 4, 9, 29, 56, 58, 68, 116, 131, 178 }
% 62.24/62.55 351 : pppp41-{T}(E2,E4) { 0, 1, 4, 9, 29, 56, 58, 68, 116, 131, 179 }
% 62.24/62.55 352 : pppp37-{T}(E4,E4) { 0, 1, 4, 9, 34, 56, 58, 72, 116, 134, 180 }
% 62.24/62.55 353 : pppp36-{T}(E4,E3) { 0, 1, 4, 9, 34, 56, 58, 72, 116, 134, 181 }
% 62.24/62.55 354 : pppp35-{T}(E4,E2) { 0, 1, 4, 9, 34, 56, 58, 72, 116, 134, 182 }
% 62.24/62.55 355 : pppp21-{T}(E0,E4) { 0, 1, 4, 9, 40, 56, 58, 74, 116, 136, 183 }
% 62.24/62.55 356 : pppp20-{T}(E0,E4) { 0, 1, 4, 9, 40, 56, 58, 74, 116, 136, 184 }
% 62.24/62.55 357 : pppp62-{T}(E4,E3) { 0, 1, 3, 4, 9, 55, 56, 58, 83, 116, 145, 185 }
% 62.24/62.55 358 : pppp61-{T}(E4,E2) { 0, 1, 3, 4, 9, 55, 56, 58, 83, 116, 145, 186 }
% 62.24/62.55 359 : pppp60-{T}(E4,E0) { 0, 1, 3, 4, 9, 55, 56, 58, 83, 116, 145, 187 }
% 62.24/62.55 360 : pppp57-{T}(E4,E2) { 0, 1, 3, 4, 9, 55, 56, 58, 84, 116, 146, 188 }
% 62.24/62.55 361 : pppp56-{T}(E4,E3) { 0, 1, 3, 4, 9, 55, 56, 58, 84, 116, 146, 189 }
% 62.24/62.55 362 : pppp55-{T}(E4,E4) { 0, 1, 3, 4, 9, 55, 56, 58, 84, 116, 146, 190 }
% 62.24/62.55 363 : pppp16-{T}(E4,E4) { 0, 1, 3, 4, 9, 55, 56, 58, 94, 116, 152, 191 }
% 62.24/62.55 364 : pppp15-{T}(E3,E4) { 0, 1, 3, 4, 9, 55, 56, 58, 94, 116, 152, 192 }
% 62.24/62.55 365 : pppp75-{T}(E3,E4) { 0, 1, 4, 9, 56, 58, 116, 161, 193 }
% 62.24/62.55 366 : pppp74-{T}(E3,E4) { 0, 1, 4, 9, 56, 58, 116, 162, 194 }
% 62.24/62.55 367 : pppp73-{T}(E0,E4) { 0, 1, 4, 9, 56, 58, 116, 163, 195 }
% 62.24/62.55 368 : pppp72-{T}(E2,E4) { 0, 1, 4, 9, 56, 58, 116, 164, 196 }
% 62.24/62.55 369 : pppp11-{T}(E4,E4) { 0, 1, 4, 9, 56, 58, 116, 169, 197 }
% 62.24/62.55
% 62.24/62.55
% 62.24/62.55 % SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p
% 62.24/62.55
% 62.24/62.55 randbase = 1
%------------------------------------------------------------------------------